+ '[' 0 -eq 1 ']'
+ echo 'Doing: timeout --foreground --kill-after=5 --signal=SIGINT 121 time metta /opt/logicmoo_opencog/hyperon-wam/examples/baseline_compat/hyperon-pln_metta/hol/NatSimpleTest.metta'
Doing: timeout --foreground --kill-after=5 --signal=SIGINT 121 time metta /opt/logicmoo_opencog/hyperon-wam/examples/baseline_compat/hyperon-pln_metta/hol/NatSimpleTest.metta
+ eval 'timeout --foreground --kill-after=5 --signal=SIGINT 121 time metta /opt/logicmoo_opencog/hyperon-wam/examples/baseline_compat/hyperon-pln_metta/hol/NatSimpleTest.metta'
++ timeout --foreground --kill-after=5 --signal=SIGINT 121 time metta /opt/logicmoo_opencog/hyperon-wam/examples/baseline_compat/hyperon-pln_metta/hol/NatSimpleTest.metta
[()]
[(: Base_plus (=== (plus Z $y#139) $y#139))]
[()]
[()]
[()]
[(let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans EqRefl $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans Rec_plus $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans EqRefl EqRefl) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans EqRefl Rec_plus) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans EqRefl (EqTrans EqRefl EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans EqRefl (EqTrans EqRefl Rec_plus)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans EqRefl (EqTrans Rec_plus EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans EqRefl (EqStruct2 EqRefl EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans EqRefl (EqSym EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans EqRefl (EqSym Base_plus)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans Rec_plus EqRefl) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans Rec_plus (EqTrans EqRefl EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans Rec_plus (EqSym EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus Z (S (plus (S Z) (S (S Z))))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus Z (S (plus (S Z) (S (S Z))))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans Rec_plus (EqSym Base_plus)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans Rec_plus (EqSym Rec_plus)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans Rec_plus (EqStruct1 EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (: (EqTrans (EqTrans Rec_plus (EqStruct1 Rec_plus)) (EqStruct1 (EqStruct1 Base_plus))) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqTrans EqRefl EqRefl) EqRefl) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqTrans EqRefl EqRefl) Rec_plus) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqTrans EqRefl EqRefl) (EqTrans EqRefl EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqTrans EqRefl EqRefl) (EqTrans EqRefl Rec_plus)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqTrans EqRefl EqRefl) (EqTrans Rec_plus EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqTrans EqRefl EqRefl) (EqStruct2 EqRefl EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqTrans EqRefl EqRefl) (EqSym EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqTrans EqRefl EqRefl) (EqSym Base_plus)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqTrans EqRefl Rec_plus) EqRefl) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqTrans EqRefl Rec_plus) (EqTrans EqRefl EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqTrans EqRefl Rec_plus) (EqSym EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus Z (S (plus (S Z) (S (S Z))))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus Z (S (plus (S Z) (S (S Z))))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqTrans EqRefl Rec_plus) (EqSym Base_plus)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqTrans EqRefl Rec_plus) (EqSym Rec_plus)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqTrans EqRefl Rec_plus) (EqStruct1 EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (: (EqTrans (EqTrans (EqTrans EqRefl Rec_plus) (EqStruct1 Rec_plus)) (EqStruct1 (EqStruct1 Base_plus))) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))), (let* (((: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqTrans Rec_plus EqRefl) EqRefl) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqTrans Rec_plus EqRefl) (EqTrans EqRefl EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqTrans Rec_plus EqRefl) (EqSym EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus Z (S (plus (S Z) (S (S Z))))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus Z (S (plus (S Z) (S (S Z))))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqTrans Rec_plus EqRefl) (EqSym Base_plus)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqTrans Rec_plus EqRefl) (EqSym Rec_plus)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqTrans Rec_plus EqRefl) (EqStruct1 EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (: (EqTrans (EqTrans (EqTrans Rec_plus EqRefl) (EqStruct1 Rec_plus)) (EqStruct1 (EqStruct1 Base_plus))) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqStruct2 EqRefl EqRefl) EqRefl) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqStruct2 EqRefl EqRefl) Rec_plus) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqStruct2 EqRefl EqRefl) (EqTrans EqRefl EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqStruct2 EqRefl EqRefl) (EqTrans EqRefl Rec_plus)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqStruct2 EqRefl EqRefl) (EqTrans Rec_plus EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqStruct2 EqRefl EqRefl) (EqStruct2 EqRefl EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqStruct2 EqRefl EqRefl) (EqSym EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqStruct2 EqRefl EqRefl) (EqSym Base_plus)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqSym EqRefl) EqRefl) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqSym EqRefl) Rec_plus) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqSym EqRefl) (EqTrans EqRefl EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqSym EqRefl) (EqTrans EqRefl Rec_plus)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqSym EqRefl) (EqTrans Rec_plus EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqSym EqRefl) (EqStruct2 EqRefl EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqSym EqRefl) (EqSym EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqSym EqRefl) (EqSym Base_plus)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqSym Base_plus) EqRefl) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqSym Base_plus) Base_plus) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqSym Base_plus) (EqTrans EqRefl EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqSym Base_plus) (EqTrans EqRefl Base_plus)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqSym Base_plus) (EqTrans Base_plus EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqSym Base_plus) (EqTrans Base_plus Rec_plus)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqSym Base_plus) (EqStruct2 EqRefl EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus Z (S (plus (S Z) (S (S Z))))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus Z (S (plus (S Z) (S (S Z))))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqSym Base_plus) (EqStruct2 EqRefl Rec_plus)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqSym Base_plus) (EqSym EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus Z (plus Z (plus (S (S Z)) (S (S Z))))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus Z (plus Z (plus (S (S Z)) (S (S Z))))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqSym Base_plus) (EqSym Base_plus)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqStruct2 EqRefl EqRefl) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqStruct2 EqRefl (EqTrans EqRefl EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqStruct2 EqRefl (EqSym EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (plus Z (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (plus Z (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqStruct2 EqRefl (EqSym Base_plus)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqStruct2 EqRefl (EqStruct1 EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqStruct2 (EqTrans EqRefl EqRefl) EqRefl) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqStruct2 (EqTrans EqRefl EqRefl) (EqTrans EqRefl EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqStruct2 (EqTrans EqRefl EqRefl) (EqSym EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (plus Z (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (plus Z (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqStruct2 (EqTrans EqRefl EqRefl) (EqSym Base_plus)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqStruct2 (EqTrans EqRefl EqRefl) (EqStruct1 EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqStruct2 (EqSym EqRefl) EqRefl) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqStruct2 (EqSym EqRefl) (EqTrans EqRefl EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqStruct2 (EqSym EqRefl) (EqSym EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (plus Z (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (plus Z (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqStruct2 (EqSym EqRefl) (EqSym Base_plus)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqStruct2 (EqSym EqRefl) (EqStruct1 EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (plus Z (S (S Z))) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (plus Z (S (S Z))) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqStruct2 (EqSym Base_plus) EqRefl) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (plus Z (S (S Z))) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (plus Z (S (S Z))) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqStruct2 (EqSym Base_plus) (EqTrans EqRefl EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (plus Z (S (S Z))) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (plus Z (S (S Z))) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqStruct2 (EqSym Base_plus) (EqSym EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (plus Z (S (S Z))) (plus Z (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (plus Z (S (S Z))) (plus Z (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqStruct2 (EqSym Base_plus) (EqSym Base_plus)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (plus Z (S (S Z))) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (plus Z (S (S Z))) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqStruct2 (EqSym Base_plus) (EqStruct1 EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqStruct2 (EqStruct1 EqRefl) EqRefl) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqStruct2 (EqStruct1 EqRefl) (EqTrans EqRefl EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqStruct2 (EqStruct1 EqRefl) (EqSym EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (plus Z (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (plus Z (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqStruct2 (EqStruct1 EqRefl) (EqSym Base_plus)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqStruct2 (EqStruct1 EqRefl) (EqStruct1 EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqSym EqRefl) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqSym Base_plus) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqSym (EqTrans EqRefl EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqSym (EqTrans EqRefl Base_plus)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqSym (EqTrans Base_plus EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus Z (plus Z (plus (S (S Z)) (S (S Z))))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus Z (plus Z (plus (S (S Z)) (S (S Z))))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqSym (EqTrans Base_plus Base_plus)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqSym (EqStruct2 EqRefl EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (plus Z (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (plus Z (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqSym (EqStruct2 EqRefl Base_plus)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (plus Z (S (S Z))) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (plus Z (S (S Z))) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqSym (EqStruct2 Base_plus EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (plus Z (S (S Z))) (plus Z (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (plus Z (S (S Z))) (plus Z (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqSym (EqStruct2 Base_plus Base_plus)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqSym (EqSym EqRefl)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#35975 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqSym (EqSym Rec_plus)) $proof2#35975) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof#205584 (=== (S (S (S (S Z)))) (plus (S (S Z)) (S (S Z))))) (synthesize (: $proof#205584 (=== (S (S (S (S Z)))) (plus (S (S Z)) (S (S Z))))) kb rb (S (S Z))))) (: (EqSym $proof#205584) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))))]
20.52user 0.02system 0:20.54elapsed 99%CPU (0avgtext+0avgdata 119280maxresident)k
0inputs+0outputs (0major+26608minor)pagefaults 0swaps