+ '[' 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~OLD.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~OLD.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~OLD.metta'
++ timeout --foreground --kill-after=5 --signal=SIGINT 121 time metta /opt/logicmoo_opencog/hyperon-wam/examples/baseline_compat/hyperon-pln_metta/hol/NatSimpleTest~OLD.metta
[()]
[(: Base_plus (=== (plus Z $y#139) $y#139))]
[(: (EqTrans Rec_plus (UnaryEqStruct Base_plus)) (=== (plus (S Z) Z) (S Z))), (: (EqTrans (EqTrans EqRefl Rec_plus) (UnaryEqStruct Base_plus)) (=== (plus (S Z) Z) (S Z))), (: (EqTrans (EqTrans Rec_plus EqRefl) (UnaryEqStruct Base_plus)) (=== (plus (S Z) Z) (S Z)))]
[(: (EqTrans Rec_plus (UnaryEqStruct Base_plus)) (=== (plus (S Z) (S Z)) (S (S Z)))), (: (EqTrans (EqTrans EqRefl Rec_plus) (UnaryEqStruct Base_plus)) (=== (plus (S Z) (S Z)) (S (S Z)))), (: (EqTrans (EqTrans Rec_plus EqRefl) (UnaryEqStruct Base_plus)) (=== (plus (S Z) (S Z)) (S (S Z))))]
[(: (EqTrans Rec_plus (UnaryEqStruct Base_plus)) (=== (plus (S Z) (S (S (S (S (S (S (S (S (S (S Z))))))))))) (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))), (: (EqTrans (EqTrans EqRefl Rec_plus) (UnaryEqStruct Base_plus)) (=== (plus (S Z) (S (S (S (S (S (S (S (S (S (S Z))))))))))) (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))), (: (EqTrans (EqTrans Rec_plus EqRefl) (UnaryEqStruct Base_plus)) (=== (plus (S Z) (S (S (S (S (S (S (S (S (S (S Z))))))))))) (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))]
[(let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans EqRefl $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans Rec_plus $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans EqRefl EqRefl) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans EqRefl Rec_plus) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans EqRefl (EqTrans EqRefl EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans EqRefl (BinaryEqStruct EqRefl EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans EqRefl (EqSym EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans Rec_plus EqRefl) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans Rec_plus (EqSym EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus Z (S (plus (S Z) (S (S Z))))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans Rec_plus (UnaryEqStruct EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (: (EqTrans (EqTrans Rec_plus (UnaryEqStruct Rec_plus)) (UnaryEqStruct (UnaryEqStruct Base_plus))) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqTrans EqRefl EqRefl) EqRefl) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqTrans EqRefl EqRefl) (BinaryEqStruct EqRefl EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus Z (S (plus (S Z) (S (S Z))))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqTrans EqRefl Rec_plus) (UnaryEqStruct EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (: (EqTrans (EqTrans (EqTrans EqRefl Rec_plus) (UnaryEqStruct Rec_plus)) (UnaryEqStruct (UnaryEqStruct Base_plus))) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))), (let* (((: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus Z (S (plus (S Z) (S (S Z))))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqTrans Rec_plus EqRefl) (UnaryEqStruct EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (: (EqTrans (EqTrans (EqTrans Rec_plus EqRefl) (UnaryEqStruct Rec_plus)) (UnaryEqStruct (UnaryEqStruct Base_plus))) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (BinaryEqStruct EqRefl EqRefl) EqRefl) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (BinaryEqStruct EqRefl EqRefl) Rec_plus) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (BinaryEqStruct EqRefl EqRefl) (EqTrans EqRefl EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (BinaryEqStruct EqRefl EqRefl) (EqTrans EqRefl Rec_plus)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (BinaryEqStruct EqRefl EqRefl) (EqTrans Rec_plus EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (BinaryEqStruct EqRefl EqRefl) (BinaryEqStruct EqRefl EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (BinaryEqStruct EqRefl EqRefl) (EqSym EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (BinaryEqStruct EqRefl EqRefl) (EqSym Base_plus)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqSym EqRefl) EqRefl) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqSym EqRefl) Rec_plus) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqSym EqRefl) (BinaryEqStruct EqRefl EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqSym EqRefl) (EqSym EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqSym Base_plus) (BinaryEqStruct EqRefl EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus Z (S (plus (S Z) (S (S Z))))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus Z (S (plus (S Z) (S (S Z))))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqTrans (EqSym Base_plus) (BinaryEqStruct EqRefl Rec_plus)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus Z (plus Z (plus (S (S Z)) (S (S Z))))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (BinaryEqStruct EqRefl EqRefl) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (BinaryEqStruct EqRefl (EqTrans EqRefl EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (BinaryEqStruct EqRefl (EqSym EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (plus Z (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (plus Z (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (BinaryEqStruct EqRefl (EqSym Base_plus)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (BinaryEqStruct EqRefl (UnaryEqStruct EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (BinaryEqStruct (EqTrans EqRefl EqRefl) EqRefl) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (BinaryEqStruct (EqTrans EqRefl EqRefl) (EqTrans EqRefl EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (BinaryEqStruct (EqTrans EqRefl EqRefl) (EqSym EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (plus Z (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (plus Z (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (BinaryEqStruct (EqTrans EqRefl EqRefl) (EqSym Base_plus)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (BinaryEqStruct (EqTrans EqRefl EqRefl) (UnaryEqStruct EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (BinaryEqStruct (EqSym EqRefl) EqRefl) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (BinaryEqStruct (EqSym EqRefl) (EqTrans EqRefl EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (BinaryEqStruct (EqSym EqRefl) (EqSym EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (plus Z (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (plus Z (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (BinaryEqStruct (EqSym EqRefl) (EqSym Base_plus)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (BinaryEqStruct (EqSym EqRefl) (UnaryEqStruct EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (plus Z (S (S Z))) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (plus Z (S (S Z))) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (BinaryEqStruct (EqSym Base_plus) EqRefl) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (plus Z (S (S Z))) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (plus Z (S (S Z))) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (BinaryEqStruct (EqSym Base_plus) (EqTrans EqRefl EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (plus Z (S (S Z))) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (plus Z (S (S Z))) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (BinaryEqStruct (EqSym Base_plus) (EqSym EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (plus Z (S (S Z))) (plus Z (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (plus Z (S (S Z))) (plus Z (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (BinaryEqStruct (EqSym Base_plus) (EqSym Base_plus)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (plus Z (S (S Z))) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (plus Z (S (S Z))) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (BinaryEqStruct (EqSym Base_plus) (UnaryEqStruct EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (BinaryEqStruct (UnaryEqStruct EqRefl) EqRefl) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (BinaryEqStruct (UnaryEqStruct EqRefl) (EqTrans EqRefl EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (BinaryEqStruct (UnaryEqStruct EqRefl) (EqSym EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (plus Z (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (plus Z (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (BinaryEqStruct (UnaryEqStruct EqRefl) (EqSym Base_plus)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (BinaryEqStruct (UnaryEqStruct EqRefl) (UnaryEqStruct EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqSym EqRefl) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqSym Base_plus) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqSym (EqTrans EqRefl EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus Z (plus (S (S Z)) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus Z (plus Z (plus (S (S Z)) (S (S Z))))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (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#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqSym (BinaryEqStruct EqRefl EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (plus Z (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (plus Z (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqSym (BinaryEqStruct EqRefl Base_plus)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (plus Z (S (S Z))) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (plus Z (S (S Z))) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqSym (BinaryEqStruct Base_plus EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (plus Z (S (S Z))) (plus Z (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (plus Z (S (S Z))) (plus Z (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqSym (BinaryEqStruct Base_plus Base_plus)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqSym (EqSym EqRefl)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) (synthesize (: $proof2#42462 (=== (S (plus (S Z) (S (S Z)))) (S (S (S (S Z)))))) kb rb (S (S Z))))) (: (EqTrans (EqSym (EqSym Rec_plus)) $proof2#42462) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z))))))), (let* (((: $proof#212022 (=== (S (S (S (S Z)))) (plus (S (S Z)) (S (S Z))))) (synthesize (: $proof#212022 (=== (S (S (S (S Z)))) (plus (S (S Z)) (S (S Z))))) kb rb (S (S Z))))) (: (EqSym $proof#212022) (=== (plus (S (S Z)) (S (S Z))) (S (S (S (S Z)))))))]
30.85user 0.01system 0:30.87elapsed 99%CPU (0avgtext+0avgdata 128752maxresident)k
0inputs+0outputs (0major+29012minor)pagefaults 0swaps