
=========================================================
ALLOY ANALYZER STATE DUMP AT Sat Jun 01 20:46:05 EDT 2002
=========================================================

Alloy build date:  Thu Feb 28 19:26:22 EST 2002 



Message: Uncaught exception
Exception: 
java.lang.NullPointerException
	at alloy.transl.TranslVisitor._saveTransl(TranslVisitor.java:268)
	at alloy.transl.TranslVisitor.visit(TranslVisitor.java:690)
	at alloy.ast.BinaryExpr.acceptReturnVisitor(BinaryExpr.java:105)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.transl.TranslVisitor.visit(TranslVisitor.java:674)
	at alloy.ast.BinaryExpr.acceptReturnVisitor(BinaryExpr.java:105)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.transl.TranslVisitor.visit(TranslVisitor.java:673)
	at alloy.ast.BinaryExpr.acceptReturnVisitor(BinaryExpr.java:105)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.transl.TranslVisitor.visit(TranslVisitor.java:674)
	at alloy.ast.BinaryExpr.acceptReturnVisitor(BinaryExpr.java:105)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.transl.TranslVisitor.visit(TranslVisitor.java:674)
	at alloy.ast.BinaryExpr.acceptReturnVisitor(BinaryExpr.java:105)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.transl.TranslVisitor.visit(TranslVisitor.java:674)
	at alloy.ast.BinaryExpr.acceptReturnVisitor(BinaryExpr.java:105)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.transl.TranslVisitor.visit(TranslVisitor.java:436)
	at alloy.ast.ElemFormula.acceptReturnVisitor(ElemFormula.java:105)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.transl.TranslVisitor.visit(TranslVisitor.java:495)
	at alloy.ast.NegFormula.acceptReturnVisitor(NegFormula.java:69)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.transl.TranslVisitor.visit(TranslVisitor.java:458)
	at alloy.ast.FormulaSeq.acceptReturnVisitor(FormulaSeq.java:69)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.transl.TranslVisitor.visit(TranslVisitor.java:474)
	at alloy.ast.BinaryFormula.acceptReturnVisitor(BinaryFormula.java:105)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.transl.TranslVisitor.visit(TranslVisitor.java:458)
	at alloy.ast.FormulaSeq.acceptReturnVisitor(FormulaSeq.java:69)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.transl.TranslVisitor.visit(TranslVisitor.java:458)
	at alloy.ast.FormulaSeq.acceptReturnVisitor(FormulaSeq.java:69)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.transl.TranslVisitor.visit(TranslVisitor.java:458)
	at alloy.ast.FormulaSeq.acceptReturnVisitor(FormulaSeq.java:69)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.transl.TranslVisitor.visit(TranslVisitor.java:458)
	at alloy.ast.FormulaSeq.acceptReturnVisitor(FormulaSeq.java:69)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.transl.TranslVisitor.translate(TranslVisitor.java:311)
	at alloy.api.AlloyRunner.translateCommand(AlloyRunner.java:411)
	at alloy.gui.AlloyGUI$10.construct(AlloyGUI.java:1265)
	at alloy.util.SwingWorker$2.run(SwingWorker.java:128)
	at java.lang.Thread.run(Unknown Source)

------------------------------------------------------------
Object: actionCommand
------------------------------------------------------------

Execute

------------------------------------------------------------
Object: curGUIState
------------------------------------------------------------

_enabledMenuItems=[] progressSpinning=true solveRunning=true

------------------------------------------------------------
Object: savedGUIState
------------------------------------------------------------

_enabledMenuItems=[javax.swing.JCheckBoxMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@784427,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=javax.swing.plaf.metal.MetalIconFactory$CheckBoxMenuItemIcon@5c1f04,text=Specify primary relations], javax.swing.JMenuItem[,1,24,151x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4272bc,flags=1568,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Open], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4272bc,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Change Tab Width], javax.swing.JMenuItem[,1,66,151x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4272bc,flags=1568,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Save], javax.swing.JMenuItem[,1,3,139x21,disabled,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4272bc,flags=1568,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Build], javax.swing.JMenuItem[,1,87,151x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4272bc,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Save As...], javax.swing.JCheckBoxMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@784427,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=javax.swing.plaf.metal.MetalIconFactory$CheckBoxMenuItemIcon@5c1f04,text=Print status messages], javax.swing.JMenuItem[,1,108,151x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4272bc,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Save Copy As...], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4272bc,flags=1568,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Paste], javax.swing.JRadioButtonMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@758cd1,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=javax.swing.plaf.metal.MetalIconFactory$RadioButtonMenuItemIcon@7ac852,text=run showme for 4 ], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4272bc,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Change Text Font], javax.swing.JMenuItem[,1,3,151x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4272bc,flags=1568,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=New], javax.swing.JMenuItem[,1,45,151x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4272bc,flags=1568,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Reload], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4272bc,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Send model to developers...], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4272bc,flags=1568,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Undo], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4272bc,flags=1568,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Copy], javax.swing.JMenuItem[,1,24,139x21,disabled,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4272bc,flags=1568,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Execute], javax.swing.JCheckBoxMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@784427,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=javax.swing.plaf.metal.MetalIconFactory$CheckBoxMenuItemIcon@5c1f04,text=Remember Tree Modality], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4272bc,flags=1568,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Redo], javax.swing.JMenuItem[,1,133,151x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4272bc,flags=1568,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Quit], javax.swing.JMenuItem[,1,45,139x21,disabled,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4272bc,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Edit Instance], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4272bc,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Change Tree Font], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4272bc,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Delete], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4272bc,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Options...], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4272bc,flags=1568,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Cut], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4272bc,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=About...]] progressSpinning=false solveRunning=false


------------------------------------------------------------
File: C:\kopi\jalloyOut.als
------------------------------------------------------------

module jalloyOut
sig Bit {}

static part sig TR, NR extends Bit {}

sig boolean {}

static part sig true, false extends boolean {}

sig Nat {less: set Nat}

sig RBNode {}

sig RBTree1 {}

static sig state {
    i1_0 : option Nat,
    yyy1_0, yyy1_1 : option RBNode,
    t2_0, t2_1 : option RBTree1,
    t3_0, t3_1 : option RBTree1,
    this1_0 : RBTree1,
    kl4_0, kl4_1, kl4_2, kl4_3 : option RBNode,
    x4_0, x4_1, x4_2, x4_3 : option RBNode,
    z3_0, z3_1 : option RBNode,
    this4_0 : RBTree1,
    z2_0, z2_1 : option RBNode,
    i0_0, i0_1 : option Nat,
    t1_0 : option RBTree1,
    this3_0 : RBTree1,
    z4_0, z4_1 : option RBNode,
    y2_0, y2_1 : option RBNode,
    hh1_0, hh1_1, hh1_2 : option RBNode,
    yy1_0, yy1_1 : option RBNode,
    ret0_0 : RBNode,
    y3_0, y3_1 : option RBNode,
    this2_0 : RBTree1,
    this0_0 : RBNode,
parent_RBNode : RBNode ->? RBNode,
isRed_RBNode : RBNode ->? boolean,
right_RBNode : RBNode ->? RBNode,
root_RBTree1 : RBTree1 ->? RBNode,
key_RBNode : RBNode ->? Nat,
left_RBNode : RBNode ->? RBNode,
    E166_57_0, E165_61_0, E229_56_0, E211_41_0, E203_47_0, E205_43_0, E130_73_0, E95_89_0, E190_40_0, E123_83_0, E146_24_0, E134, E143_12_0, E138_17_0, E199_36_0, E192_37_0, E136, E154_11_0, E227_51_0, E185_37_0, E125_79_0, E198, E210_45_0, E132_11_1, E151_7_0, E214, E120_74_0, E169_58_0, E172_58_0, E221_63_0, E139_18_0, E189_39_0, E152_27_0, E174_59_0, E226_52_0, E129_70_0, E230_53_0, E182_36_0, E171_56_0, E147_27_0, E117_99_0, E98_84_0, E150_30_0, E114_95_0, E111_93_0, E206_39_0, E209_37_0, E137_21_0, E196_40_0, E222_56_0, E184_42_0, E194_41_0, E193_45_0, E131_76_0, E142_8_0, E141_28_0, E204_38_0, E180, E216_61_0, E224_55_0, E213_40_0, E179_53_0, E124_80_0, E225_59_0, E200_42_0, E223_58_0, E145_16_0, E110_88_0, E218_54_0, E191_35_0, E148_16_0, E215, E133_12_1, E161_19_0, E170_63_0, E158_23_0, E202_37_0, E144_23_0, E212_46_0, E121_96_0, E113_69_0, E176_51_0, E127_95_0, E103_71_0, E119_100_0, E157_25_0, E140_11_0, E195_46_0, E197, E220_58_0, E219_53_0, E102_104_0, E181, E96_70_0, E173_55_0, E188_43_0, E163, E232, E97_91_0, E105_89_0, E160_26_0, E175_52_0, E207_40_0, E217_57_0, E109_71_0, E128_92_0, E208_35_0, E135, E122_77_0, E168_53_0, E149_25_0, E177_62_0, E153_9_0, E99_72_0, E126_75_0, E231, E178_56_0, E100_90_0, E104_70_0, E187_38_0, E164, E115_79_0, E155_14_0, E186_47_0, E201_42_0, E162_9_0, E101_73_0, E156_18_0, E228_62_0, E167_54_0, E159_10_0, E183_42_0 : option Bit
}
fun RBInsert () { with state { 
    (some E109_71_0 <=> some E99_72_0)
    (some E216_61_0 + E217_57_0 + E225_59_0 <=> some E228_62_0)
    (some E215 <=> some E214)
    (some E103_71_0 <=> some E110_88_0)
    (some E130_73_0 <=> some E120_74_0)
    (some E230_53_0 + E218_54_0 <=> some E224_55_0)
    (some E207_40_0 <=> some E211_41_0)
    (some E154_11_0 <=> some E143_12_0)
    (some E194_41_0 + E188_43_0 + E193_45_0 <=> some E195_46_0)
    (some E181 <=> some E180)
    (some E219_53_0 <=> some E218_54_0)
    (some E132_11_1 <=> some E133_12_1)
    (some E98_84_0 <=> some E181)
    (some E180 <=> some E176_51_0)
    (some E131_76_0 <=> some E122_77_0)
    (some E192_37_0 + E187_38_0 <=> some E189_39_0)
    (some E222_56_0 <=> some E217_57_0)
    (some E115_79_0 + E186_47_0 <=> some E123_83_0)
    (some E176_51_0 <=> some E175_52_0)
    (some E119_100_0 <=> some E215)
    (some E100_90_0 <=> some E97_91_0)
    (some E229_56_0 <=> some E223_58_0 + E220_58_0)
    (some E208_35_0 <=> some E199_36_0)
    (some E183_42_0 <=> some E188_43_0)
    (some E159_10_0 <=> some E154_11_0 + E140_11_0)
    (some E157_25_0 <=> some E152_27_0 + E147_27_0)
    (some E111_93_0 + E203_47_0 + E122_77_0 + E170_63_0 <=> some E102_104_0)
    (some E173_55_0 <=> some E171_56_0 + E178_56_0)
    (some E196_40_0 <=> some E183_42_0 + E184_42_0)
    (some E127_95_0 <=> some E121_96_0)
    (some E105_89_0 <=> some E114_95_0 + E127_95_0)
    (some E155_14_0 + E153_9_0 + E143_12_0 <=> some E148_16_0 + E145_16_0)
    (some E113_69_0 <=> some E96_70_0 + E129_70_0)
    (some E200_42_0 <=> some E205_43_0)
    (some E182_36_0 <=> some E192_37_0 + E185_37_0)
    (some E172_58_0 <=> some E174_59_0)
    (some E139_18_0 <=> some E161_19_0)
    (some E151_7_0 <=> some E142_8_0)
    (some E189_39_0 <=> some E190_40_0 + E196_40_0)
    (some E133_12_1 <=> some E164)
    (some E138_17_0 <=> some E156_18_0 + E139_18_0)
    (some E148_16_0 <=> some E138_17_0)
    (some E140_11_0 <=> some E155_14_0)
    (some E126_75_0 <=> some E131_76_0)
    (some E184_42_0 <=> some E193_45_0)
    (some E135 <=> some E134)
    (some E121_96_0 <=> some E232)
    (some E224_55_0 <=> some E229_56_0 + E222_56_0)
    (some E147_27_0 <=> some E150_30_0)
    (some E99_72_0 <=> some E101_73_0 + E130_73_0)
    (some E171_56_0 <=> some E166_57_0)
    (some E101_73_0 <=> some E115_79_0 + E125_79_0)
    (some E162_9_0 <=> some E159_10_0)
    (some E156_18_0 <=> some E137_21_0)
    (some E125_79_0 <=> some E124_80_0)
    (some E220_58_0 <=> some E216_61_0)
    (some E166_57_0 + E174_59_0 + E165_61_0 <=> some E177_62_0)
    (some E136 <=> some E135)
    (some E129_70_0 <=> some E109_71_0 + E103_71_0)
    (some E95_89_0 <=> some E100_90_0)
    (some E231 <=> some E227_51_0)
    (some E117_99_0 <=> some E119_100_0)
    (some E142_8_0 <=> some E153_9_0 + E162_9_0)
    (some E190_40_0 <=> some E194_41_0)
    (some E228_62_0 <=> some E221_63_0)
    (some E195_46_0 <=> some E186_47_0)
    (some E168_53_0 <=> some E167_54_0)
    (some E136)
    (some E128_92_0 <=> some E111_93_0)
    (some E212_46_0 <=> some E203_47_0)
    (some E163 <=> some E151_7_0)
    (some E110_88_0 <=> some E105_89_0 + E95_89_0)
    (some E221_63_0 + E114_95_0 <=> some E117_99_0)
    (some E144_23_0 + E160_26_0 + E141_28_0 + E150_30_0 <=> some E113_69_0)
    (some E226_52_0 <=> some E219_53_0 + E230_53_0)
    (some E197 <=> some E191_35_0)
    (some E120_74_0 <=> some E126_75_0)
    (some E198 <=> some E197)
    (some E167_54_0 + E179_53_0 <=> some E173_55_0)
    (some E149_25_0 <=> some E160_26_0)
    (some E214 <=> some E208_35_0)
    (some E177_62_0 <=> some E170_63_0)
    (some E169_58_0 <=> some E165_61_0)
    (some E124_80_0 <=> some E198)
    (some E158_23_0 <=> some E146_24_0)
    (some E206_39_0 <=> some E207_40_0 + E213_40_0)
    (some E102_104_0 <=> some E104_70_0)
    (some E191_35_0 <=> some E182_36_0)
    (some E175_52_0 <=> some E168_53_0 + E179_53_0)
    (some E201_42_0 <=> some E210_45_0)
    (some E209_37_0 + E204_38_0 <=> some E206_39_0)
    (some E137_21_0 + E161_19_0 + E145_16_0 <=> some E144_23_0 + E158_23_0)
    (some E227_51_0 <=> some E226_52_0)
    (some E232 <=> some E231)
    (some E164 <=> some E163)
    (some E146_24_0 <=> some E149_25_0 + E157_25_0)
    (some E152_27_0 <=> some E141_28_0)
    (some E223_58_0 <=> some E225_59_0)
    (some E97_91_0 <=> some E128_92_0)
    (some E185_37_0 <=> some E187_38_0)
    (some E211_41_0 + E205_43_0 + E210_45_0 <=> some E212_46_0)
    (some E202_37_0 <=> some E204_38_0)
    (some E123_83_0 <=> some E98_84_0)
    (some E213_40_0 <=> some E201_42_0 + E200_42_0)
    (some E134 <=> some E132_11_1)
    (some E199_36_0 <=> some E202_37_0 + E209_37_0)
    (some E178_56_0 <=> some E172_58_0 + E169_58_0)

    (some E229_56_0 => {
        !((no z3_1.(parent_RBNode ++ ((y3_1 & {o: RBNode | some E224_55_0}) -> (z3_1.(parent_RBNode ++ ((y3_1.(right_RBNode) & {o: RBNode | some E218_54_0}) -> (z3_1 & {o: RBNode | some E218_54_0}))) & {o: RBNode | some E224_55_0})))))    })
    (some E130_73_0 => {
        (some yyy1_1) && yyy1_1.(isRed_RBNode) = true    })
    (some E95_89_0 => {
        (some yy1_1) && yy1_1.(isRed_RBNode) = true    })
    (some E190_40_0 => {
        (no z2_1.(parent_RBNode ++ ((y2_1 & {o: RBNode | some E189_39_0}) -> (z2_1.(parent_RBNode ++ ((y2_1.(left_RBNode) & {o: RBNode | some E187_38_0}) -> (z2_1 & {o: RBNode | some E187_38_0}))) & {o: RBNode | some E189_39_0}))))    })
    (some E134 => {
        i0_1 = i1_0    })
    (some E143_12_0 => {
        x4_2 = x4_1.(left_RBNode)    })
    (some E138_17_0 => {
        kl4_3 = x4_2    })
    (some E192_37_0 => {
        !((some y2_1.(left_RBNode)))    })
    (some E136 => {
        hh1_1 = ret0_0    })
    (some E154_11_0 => {
        z4_1.(key_RBNode) in x4_1.(key_RBNode).less    })
    (some E227_51_0 => {
        y3_1 = z3_1.(left_RBNode)    })
    (some E185_37_0 => {
        (some y2_1.(left_RBNode))    })
    (some E125_79_0 => {
        hh1_1 = hh1_1.(parent_RBNode).(right_RBNode)    })
    (some E198 => {
        z2_1 = hh1_2    })
    (some E151_7_0 => {
        (no kl4_1)    })
    (some E214 => {
        t2_1 = t1_0    })
    (some E169_58_0 => {
        !(z3_1 = z3_1.(parent_RBNode).(right_RBNode))    })
    (some E172_58_0 => {
        z3_1 = z3_1.(parent_RBNode).(right_RBNode)    })
    (some E139_18_0 => {
        z4_1.(key_RBNode) in x4_2.(key_RBNode).less    })
    (some E152_27_0 => {
        z4_1.(key_RBNode) in kl4_3.(key_RBNode).less    })
    (some E129_70_0 => {
        hh1_1 != t1_0.(root_RBTree1) && hh1_1.(parent_RBNode).(isRed_RBNode ++ ((hh1_1 & {o: RBNode | some E113_69_0}) -> (true & {o: boolean | some E113_69_0}))) = true    })
    (some E230_53_0 => {
        !((some y3_1.(right_RBNode)))    })
    (some E171_56_0 => {
        (no z3_1.(parent_RBNode ++ ((y3_1 & {o: RBNode | some E173_55_0}) -> (z3_1.(parent_RBNode ++ ((y3_1.(right_RBNode) & {o: RBNode | some E167_54_0}) -> (z3_1 & {o: RBNode | some E167_54_0}))) & {o: RBNode | some E173_55_0}))))    })
    (some E147_27_0 => {
        !(z4_1.(key_RBNode) in kl4_3.(key_RBNode).less)    })
    (some E114_95_0 => {
        !(hh1_1 = hh1_1.(parent_RBNode).(left_RBNode))
        y3_1 = y3_0
        t3_1 = t3_0
        z3_1 = z3_0
        hh1_2 = hh1_1    })
    (some E111_93_0 => {
        hh1_2 = hh1_1.(parent_RBNode).(parent_RBNode)
        y3_1 = y3_0
        yyy1_1 = yyy1_0
        y2_1 = y2_0
        t3_1 = t3_0
        t2_1 = t2_0
        z3_1 = z3_0
        z2_1 = z2_0    })
    (some E209_37_0 => {
        !((some y2_1.(left_RBNode)))    })
    (some E137_21_0 => {
        x4_3 = x4_2.(right_RBNode)    })
    (some E196_40_0 => {
        !((no z2_1.(parent_RBNode ++ ((y2_1 & {o: RBNode | some E189_39_0}) -> (z2_1.(parent_RBNode ++ ((y2_1.(left_RBNode) & {o: RBNode | some E187_38_0}) -> (z2_1 & {o: RBNode | some E187_38_0}))) & {o: RBNode | some E189_39_0})))))    })
    (some E222_56_0 => {
        (no z3_1.(parent_RBNode ++ ((y3_1 & {o: RBNode | some E224_55_0}) -> (z3_1.(parent_RBNode ++ ((y3_1.(right_RBNode) & {o: RBNode | some E218_54_0}) -> (z3_1 & {o: RBNode | some E218_54_0}))) & {o: RBNode | some E224_55_0}))))    })
    (some E184_42_0 => {
        !(z2_1 = z2_1.(parent_RBNode).(left_RBNode))    })
    (some E142_8_0 => {
        x4_1 = this4_0.(root_RBTree1)    })
    (some E180 => {
        t3_1 = t1_0    })
    (some E213_40_0 => {
        !((no z2_1.(parent_RBNode ++ ((y2_1 & {o: RBNode | some E206_39_0}) -> (z2_1.(parent_RBNode ++ ((y2_1.(left_RBNode) & {o: RBNode | some E204_38_0}) -> (z2_1 & {o: RBNode | some E204_38_0}))) & {o: RBNode | some E206_39_0})))))    })
    (some E179_53_0 => {
        !((some y3_1.(right_RBNode)))    })
    (some E124_80_0 => {
        hh1_2 = hh1_1.(parent_RBNode)    })
    (some E200_42_0 => {
        z2_1 = z2_1.(parent_RBNode).(left_RBNode)    })
    (some E223_58_0 => {
        z3_1 = z3_1.(parent_RBNode).(right_RBNode)    })
    (some E145_16_0 => {
        !((some x4_2))
        x4_3 = x4_2
        kl4_3 = kl4_2    })
    (some E110_88_0 => {
        yy1_1 = hh1_1.(parent_RBNode).(parent_RBNode).(left_RBNode)    })
    (some E191_35_0 => {
        y2_1 = z2_1.(right_RBNode)    })
    (some E148_16_0 => {
        (some x4_2)    })
    (some E215 => {
        z2_1 = hh1_2.(parent_RBNode).(parent_RBNode)    })
    (some E161_19_0 => {
        x4_3 = x4_2.(left_RBNode)    })
    (some E158_23_0 => {
        (no x4_3)    })
    (some E202_37_0 => {
        (some y2_1.(left_RBNode))    })
    (some E144_23_0 => {
        !((no x4_3))    })
    (some E121_96_0 => {
        hh1_2 = hh1_1.(parent_RBNode)    })
    (some E176_51_0 => {
        y3_1 = z3_1.(left_RBNode)    })
    (some E127_95_0 => {
        hh1_1 = hh1_1.(parent_RBNode).(left_RBNode)    })
    (some E103_71_0 => {
        !(hh1_1.(parent_RBNode) = hh1_1.(parent_RBNode).(parent_RBNode).(left_RBNode))    })
    (some E157_25_0 => {
        !((no kl4_3))    })
    (some E140_11_0 => {
        !(z4_1.(key_RBNode) in x4_1.(key_RBNode).less)    })
    (some E197 => {
        t2_1 = t1_0    })
    (some E220_58_0 => {
        !(z3_1 = z3_1.(parent_RBNode).(right_RBNode))    })
    (some E219_53_0 => {
        (some y3_1.(right_RBNode))    })
    (some E181 => {
        z3_1 = hh1_2.(parent_RBNode).(parent_RBNode)    })
    (some E96_70_0 => {
        !(hh1_1 != t1_0.(root_RBTree1) && hh1_1.(parent_RBNode).(isRed_RBNode ++ ((hh1_1 & {o: RBNode | some E113_69_0}) -> (true & {o: boolean | some E113_69_0}))) = true)
        yy1_1 = yy1_0
        y3_1 = y3_0
        yyy1_1 = yyy1_0
        y2_1 = y2_0
        t3_1 = t3_0
        t2_1 = t2_0
        z3_1 = z3_0
        z2_1 = z2_0
        hh1_2 = hh1_1    })
    (some E163 => {
        z4_1 = hh1_1    })
    (some E232 => {
        z3_1 = hh1_2    })
    (some E105_89_0 => {
        !((some yy1_1) && yy1_1.(isRed_RBNode) = true)    })
    (some E207_40_0 => {
        (no z2_1.(parent_RBNode ++ ((y2_1 & {o: RBNode | some E206_39_0}) -> (z2_1.(parent_RBNode ++ ((y2_1.(left_RBNode) & {o: RBNode | some E204_38_0}) -> (z2_1 & {o: RBNode | some E204_38_0}))) & {o: RBNode | some E206_39_0}))))    })
    (some E109_71_0 => {
        hh1_1.(parent_RBNode) = hh1_1.(parent_RBNode).(parent_RBNode).(left_RBNode)    })
    (some E208_35_0 => {
        y2_1 = z2_1.(right_RBNode)    })
    (some E135 => {
        ret0_0 = this0_0    })
    (some E122_77_0 => {
        hh1_2 = hh1_1.(parent_RBNode).(parent_RBNode)
        yy1_1 = yy1_0
        y3_1 = y3_0
        y2_1 = y2_0
        t3_1 = t3_0
        t2_1 = t2_0
        z3_1 = z3_0
        z2_1 = z2_0    })
    (some E168_53_0 => {
        (some y3_1.(right_RBNode))    })
    (some E149_25_0 => {
        (no kl4_3)    })
    (some E153_9_0 => {
        !((some x4_1))
        x4_2 = x4_1
        kl4_2 = kl4_1    })
    (some E99_72_0 => {
        yyy1_1 = hh1_1.(parent_RBNode).(parent_RBNode).(right_RBNode)    })
    (some E231 => {
        t3_1 = t1_0    })
    (some E178_56_0 => {
        !((no z3_1.(parent_RBNode ++ ((y3_1 & {o: RBNode | some E173_55_0}) -> (z3_1.(parent_RBNode ++ ((y3_1.(right_RBNode) & {o: RBNode | some E167_54_0}) -> (z3_1 & {o: RBNode | some E167_54_0}))) & {o: RBNode | some E173_55_0})))))    })
    (some E104_70_0 => {
        !(hh1_2 != t1_0.(root_RBTree1) && hh1_2.(parent_RBNode).(isRed_RBNode ++ ((t1_0.(root_RBTree1) & {o: RBNode | some E102_104_0}) -> (false & {o: boolean | some E102_104_0}))) = true)    })
    (some E164 => {
        this4_0 = t1_0    })
    (some E115_79_0 => {
        !(hh1_1 = hh1_1.(parent_RBNode).(right_RBNode))
        y2_1 = y2_0
        t2_1 = t2_0
        z2_1 = z2_0
        hh1_2 = hh1_1    })
    (some E155_14_0 => {
        x4_2 = x4_1.(right_RBNode)    })
    (some E201_42_0 => {
        !(z2_1 = z2_1.(parent_RBNode).(left_RBNode))    })
    (some E162_9_0 => {
        (some x4_1)    })
    (some E101_73_0 => {
        !((some yyy1_1) && yyy1_1.(isRed_RBNode) = true)    })
    (some E156_18_0 => {
        !(z4_1.(key_RBNode) in x4_2.(key_RBNode).less)    })
    (some E159_10_0 => {
        kl4_2 = x4_1    })
    (some E183_42_0 => {
        z2_1 = z2_1.(parent_RBNode).(left_RBNode)    })
}}

fun showme () {
  RBInsert()
}

run showme for 4



#System properties
#Sat Jun 01 20:46:05 EDT 2002
java.runtime.name=Java(TM) 2 Runtime Environment, Standard Edition
sun.boot.library.path=C\:\\Program Files\\JavaSoft\\JRE\\1.3.1\\bin
java.vm.version=1.3.1_01
java.vm.vendor=Sun Microsystems Inc.
java.vendor.url=http\://java.sun.com/
path.separator=;
java.vm.name=Java HotSpot(TM) Client VM
file.encoding.pkg=sun.io
java.vm.specification.name=Java Virtual Machine Specification
user.dir=C\:\\alloy1\\newalloy
java.runtime.version=1.3.1_01
java.awt.graphicsenv=sun.awt.Win32GraphicsEnvironment
os.arch=x86
java.io.tmpdir=C\:\\DOCUME~1\\ADMINI~1\\LOCALS~1\\Temp\\
line.separator=\r\n
java.vm.specification.vendor=Sun Microsystems Inc.
java.awt.fonts=
os.name=Windows 2000
java.library.path=C\:\\Program Files\\JavaSoft\\JRE\\1.3.1\\bin;.;C\:\\WINNT\\System32;C\:\\WINNT;C\:\\Program Files\\JavaSoft\\JRE\\1.3.1\\bin;C\:\\PROGRA~1\\KERBEROS;C\:\\WINNT\\system32;C\:\\WINNT;C\:\\WINNT\\System32\\Wbem;C\:\\PROGRAM FILES\\THINKPAD\\UTILITIES;C\:\\jdk1.3.1_01\\bin;C\:\\Program Files\\SecureCRT 3.0;C\:\\cygwin\\bin
java.specification.name=Java Platform API Specification
java.class.version=47.0
os.version=5.0
user.home=C\:\\Documents and Settings\\Administrator
user.timezone=America/New_York
java.awt.printerjob=sun.awt.windows.WPrinterJob
file.encoding=Cp1252
java.specification.version=1.3
java.class.path=C\:\\alloy1\\newalloy\\alloy.jar
user.name=Administrator
java.vm.specification.version=1.0
java.home=C\:\\Program Files\\JavaSoft\\JRE\\1.3.1
user.language=en
java.specification.vendor=Sun Microsystems Inc.
awt.toolkit=sun.awt.windows.WToolkit
java.vm.info=mixed mode
java.version=1.3.1_01
java.ext.dirs=C\:\\Program Files\\JavaSoft\\JRE\\1.3.1\\lib\\ext
sun.boot.class.path=C\:\\Program Files\\JavaSoft\\JRE\\1.3.1\\lib\\rt.jar;C\:\\Program Files\\JavaSoft\\JRE\\1.3.1\\lib\\i18n.jar;C\:\\Program Files\\JavaSoft\\JRE\\1.3.1\\lib\\sunrsasign.jar;C\:\\Program Files\\JavaSoft\\JRE\\1.3.1\\classes
java.vendor=Sun Microsystems Inc.
file.separator=\\
java.vendor.url.bug=http\://java.sun.com/cgi-bin/bugreport.cgi
sun.io.unicode.encoding=UnicodeLittle
sun.cpu.endian=little
user.region=US
sun.cpu.isalist=pentium i486 i386

Global parameters: 
GROUP MAIN "Main options"
PARAM solver enum MCHAFF "SAT solver to use"
ENUM solver MCHAFF "Use mChaff solver"
ENUM solver ZCHAFF "Use zChaff solver"
ENUM solver BERKMIN "Use BerkMin solver"
PARAM sharbool bool 1 "Detect shared boolean subformulas"
PARAM skoluniv bool 0 "Skolemize inside universal quantifiers"
PARAM usesymm bool 1 "Add symmetry-breaking constraints"
PARAM randseed int 0 "Random seed; 0 to use current time"
PARAM multsol bool 0 "Enumeration of solutions"
PARAM infoMsgs bool 1 "Print progress/debug info"
PARAM progressInterval int 4 "How often to print debug info"
PARAM modulePath path "models:." "Path for resolving relative module names"
PARAM maxBoolNodes int 20000 "Max # of Boolean nodes to allocate"
PARAM enumBatchSize int 1 "Enumerate this many solutions at a time"
ENDGROUP
GROUP SYMM "Symmetry-breaking options"
PARAM maxComparLen int 20 "Max comparator length"
PARAM maxrand int 25 "# of random symmetries to break"
PARAM percrand int 0 "Percent of random symmetries to break (0-100)"
ENDGROUP
GROUP DEVEL "Experimental options"
PARAM bindir string "" "Where to find platform-specific binaries"
PARAM compalloc bool 0 "Compact variable allocation"
PARAM ringsymm bool 0 "Special symmetry-breaking for stable_mutex_ring"
PARAM gaugevarord bool 0 "Gauge variable order"
ENDGROUP


Free memory: 3811728
Total memory: 17010688

Args passed on command-line: 
=========================================================


