+ '[' 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/NatTest.metta'
Doing: timeout --foreground --kill-after=5 --signal=SIGINT 121 time metta /opt/logicmoo_opencog/hyperon-wam/examples/baseline_compat/hyperon-pln_metta/hol/NatTest.metta
+ eval 'timeout --foreground --kill-after=5 --signal=SIGINT 121 time metta /opt/logicmoo_opencog/hyperon-wam/examples/baseline_compat/hyperon-pln_metta/hol/NatTest.metta'
++ timeout --foreground --kill-after=5 --signal=SIGINT 121 time metta /opt/logicmoo_opencog/hyperon-wam/examples/baseline_compat/hyperon-pln_metta/hol/NatTest.metta
[()]
[(: Base_plus (=== (plus Z $y#138) $y#138))]
[()]
[()]
[()]
[(: IndZRID_plus (-> (ZRID_plus $x#11449) (ZRID_plus (S $x#11449))))]
[(let* (((: $proof2#12875 (plus Z (ZRID_plus $x#13027))) (synthesize (: $proof2#12875 (plus Z (ZRID_plus $x#13027))) kb rb (S (S Z))))) (: (Repl0 Base_plus $proof2#12875) (ZRID_plus $x#13027))), (: (Repl0 (EqSym PropZRID_plus) Base_plus) (ZRID_plus Z)), (: (Repl0 (EqSym PropZRID_plus) (EqSym (EqSym Base_plus))) (ZRID_plus Z)), (let* (((: $proof2#12875 (plus Z (ZRID_plus $x#13659))) (synthesize (: $proof2#12875 (plus Z (ZRID_plus $x#13659))) kb rb (S (S Z))))) (: (Repl0 (EqSym (EqSym Base_plus)) $proof2#12875) (ZRID_plus $x#13659))), (: (Repl0 (EqSym (EqStruct1 Base_plus)) (Repl0 (EqSym PropZRID_plus) Base_plus)) (ZRID_plus (plus Z Z))), (let* (((: $proof2#12875 (ZRID_plus (=== (plus $x#13865 Z) $x#13865))) (synthesize (: $proof2#12875 (ZRID_plus (=== (plus $x#13865 Z) $x#13865))) kb rb (S (S Z))))) (: (Repl0 (EqSym (EqStruct1 PropZRID_plus)) $proof2#12875) (ZRID_plus (ZRID_plus $x#13865)))), (let* (((: $proof2#12875 (ZRID_plus (plus Z $y#14842))) (synthesize (: $proof2#12875 (ZRID_plus (plus Z $y#14842))) kb rb (S (S Z))))) (: (Repl0 (EqStruct1 Base_plus) $proof2#12875) (ZRID_plus $y#14842))), (let* (((: $proof2#12875 (ZRID_plus (ZRID_plus $x#14843))) (synthesize (: $proof2#12875 (ZRID_plus (ZRID_plus $x#14843))) kb rb (S (S Z))))) (: (Repl0 (EqStruct1 PropZRID_plus) $proof2#12875) (ZRID_plus (=== (plus $x#14843 Z) $x#14843)))), (: (Repl0 (EqStruct1 (EqSym Base_plus)) (Repl0 (EqSym PropZRID_plus) Base_plus)) (ZRID_plus (plus Z Z))), (let* (((: $proof2#12875 (ZRID_plus (=== (plus $x#15158 Z) $x#15158))) (synthesize (: $proof2#12875 (ZRID_plus (=== (plus $x#15158 Z) $x#15158))) kb rb (S (S Z))))) (: (Repl0 (EqStruct1 (EqSym PropZRID_plus)) $proof2#12875) (ZRID_plus (ZRID_plus $x#15158)))), (let* (((: $proof2#12875 (ZRID_plus ($op#15073 (plus Z $y#15448)))) (synthesize (: $proof2#12875 (ZRID_plus ($op#15073 (plus Z $y#15448)))) kb rb (S (S Z))))) (: (Repl0 (EqStruct1 (EqStruct1 Base_plus)) $proof2#12875) (ZRID_plus ($op#15073 $y#15448)))), (let* (((: $proof2#12875 (ZRID_plus ($op#15073 (ZRID_plus $x#15449)))) (synthesize (: $proof2#12875 (ZRID_plus ($op#15073 (ZRID_plus $x#15449)))) kb rb (S (S Z))))) (: (Repl0 (EqStruct1 (EqStruct1 PropZRID_plus)) $proof2#12875) (ZRID_plus ($op#15073 (=== (plus $x#15449 Z) $x#15449))))), (: (IndNat (Repl0 (EqSym PropZRID_plus) Base_plus) IndZRID_plus) (ZRID_plus $x))]
7.96user 0.03system 0:07.99elapsed 100%CPU (0avgtext+0avgdata 100332maxresident)k
0inputs+0outputs (0major+21889minor)pagefaults 0swaps