+ '[' 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/NatStandaloneTest.metta'
Doing: timeout --foreground --kill-after=5 --signal=SIGINT 121 time metta /opt/logicmoo_opencog/hyperon-wam/examples/baseline_compat/hyperon-pln_metta/hol/NatStandaloneTest.metta
+ eval 'timeout --foreground --kill-after=5 --signal=SIGINT 121 time metta /opt/logicmoo_opencog/hyperon-wam/examples/baseline_compat/hyperon-pln_metta/hol/NatStandaloneTest.metta'
++ timeout --foreground --kill-after=5 --signal=SIGINT 121 time metta /opt/logicmoo_opencog/hyperon-wam/examples/baseline_compat/hyperon-pln_metta/hol/NatStandaloneTest.metta
[()]
[()]
[()]
[()]
[()]
[()]
[()]
[()]
[()]
[()]
[()]
[()]
[()]
[(let* (((: $prfarg#54187 (plus Z (=== (=== (plus $x Z) $x) (=== (plus (S $x) Z) (S $x))))) (bc (: $prfarg#54187 (plus Z (=== (=== (plus $x Z) $x) (=== (plus (S $x) Z) (S $x))))) (S (S Z))))) (: (((. Replace0) (Replace0 plusBase)) $prfarg#54187) (-> (=== (plus $x Z) $x) (=== (plus (S $x) Z) (S $x))))), (let* (((: $prfarg#54187 (=== (=== (plus (S $x) Z) (S $x)) (=== (plus $x Z) $x))) (bc (: $prfarg#54187 (=== (=== (plus (S $x) Z) (S $x)) (=== (plus $x Z) $x))) (S (S Z))))) (: (((. Replace0) Sym) $prfarg#54187) (-> (=== (plus $x Z) $x) (=== (plus (S $x) Z) (S $x))))), (let* (((: $prfarg#54187 (plus Z (-> (=== (plus $x Z) $x) (=== (plus (S $x) Z) (S $x))))) (bc (: $prfarg#54187 (plus Z (-> (=== (plus $x Z) $x) (=== (plus (S $x) Z) (S $x))))) (S (S Z))))) (: ((Replace0 plusBase) $prfarg#54187) (-> (=== (plus $x Z) $x) (=== (plus (S $x) Z) (S $x))))), (: ((. (Trans plusRec)) Cong) (-> (=== (plus $x Z) $x) (=== (plus (S $x) Z) (S $x)))), (let* (((: $prfarg#54187 (-> (=== (plus $x Z) $x) (plusRightId (S $x)))) (bc (: $prfarg#54187 (-> (=== (plus $x Z) $x) (plusRightId (S $x)))) (S (S Z))))) (: ((. (Replace0 plusRightIdProp)) $prfarg#54187) (-> (=== (plus $x Z) $x) (=== (plus (S $x) Z) (S $x))))), (let* (((: $prfarg#54187 (-> (=== (plus $x Z) $x) (plus Z (=== (plus (S $x) Z) (S $x))))) (bc (: $prfarg#54187 (-> (=== (plus $x Z) $x) (plus Z (=== (plus (S $x) Z) (S $x))))) (S (S Z))))) (: ((. (Replace0 plusBase)) $prfarg#54187) (-> (=== (plus $x Z) $x) (=== (plus (S $x) Z) (S $x))))), (let* (((: $prfarg#54187 (-> (=== (plus $x Z) $x) (=== (S $x) (plus (S $x) Z)))) (bc (: $prfarg#54187 (-> (=== (plus $x Z) $x) (=== (S $x) (plus (S $x) Z)))) (S (S Z))))) (: ((. Sym) $prfarg#54187) (-> (=== (plus $x Z) $x) (=== (plus (S $x) Z) (S $x))))), (let* (((: $prfarg#54187 (=== (=== (plus $x Z) $x) (=== (plus (S $x) Z) (S $x)))) (bc (: $prfarg#54187 (=== (=== (plus $x Z) $x) (=== (plus (S $x) Z) (S $x)))) (S (S Z))))) (: (Replace0 $prfarg#54187) (-> (=== (plus $x Z) $x) (=== (plus (S $x) Z) (S $x)))))]
[(: (Replace0 (Cong ((Trans plusRec) ((Trans (Cong plusBase)) (Cong (Sym plusRec)))))) (-> (plusRightId (plus (S Z) $x'#124505)) (plusRightId (S (plus (S Z) $x'#124505))))), (: (Replace0 (Cong ((Trans plusRec) ((Trans (Cong plusBase)) (Cong plusBase))))) (-> (plusRightId (plus (S Z) $x'#124505)) (plusRightId (S (plus (S Z) $x'#124505))))), (: (Replace0 (Cong ((Trans plusRec) ((Trans (Cong plusBase)) (Sym (Cong plusRec)))))) (-> (plusRightId (plus (S Z) $x'#124505)) (plusRightId (S (plus (S Z) $x'#124505))))), (: (Replace0 (Cong ((Trans plusRec) (Cong ((Trans plusBase) (Sym plusRec)))))) (-> (plusRightId (plus (S Z) $y#144144)) (plusRightId (S (plus (S Z) $y#144144))))), (: (Replace0 (Cong ((Trans plusRec) (Cong ((Trans plusBase) plusBase))))) (-> (plusRightId (plus (S Z) $y#144144)) (plusRightId (S (plus (S Z) $y#144144))))), (: (Replace0 (Cong ((Trans plusBase) ((Trans (Sym plusBase)) ((Trans plusBase) (Cong plusBase)))))) (-> (plusRightId (plus Z $y#187257)) (plusRightId (S (plus Z $y#187257))))), (: (Replace0 (Cong ((Trans plusBase) ((Trans (Sym plusBase)) ((Trans plusBase) plusRec))))) (-> (plusRightId (plus Z $y#187257)) (plusRightId (S (plus Z $y#187257))))), (: (Replace0 (Cong ((Trans plusBase) ((Trans (Sym plusBase)) ((Trans plusBase) plusBase))))) (-> (plusRightId (plus Z $y#187257)) (plusRightId (S (plus Z $y#187257))))), (: (Replace0 (Cong (Cong ((Trans (Sym plusBase)) ((Trans plusBase) (Cong plusRec)))))) (-> (plusRightId (S (S (plus $x#234949 $y#234950)))) (plusRightId (S (S (S (plus $x#234949 $y#234950))))))), (: (Replace0 (Cong (Cong ((Trans (Sym plusBase)) ((Trans plusBase) (Cong plusRightIdProp)))))) (-> (plusRightId (S (=== (plus $x#234951 Z) $x#234951))) (plusRightId (S (S (=== (plus $x#234951 Z) $x#234951)))))), (: (Replace0 (Cong (Cong ((Trans (Sym plusBase)) ((Trans plusBase) (Cong plusBase)))))) (-> (plusRightId (S $y#234250)) (plusRightId (S (S $y#234250))))), (: (Replace0 (Cong (Cong ((Trans (Sym plusBase)) ((Trans plusBase) plusRec))))) (-> (plusRightId (S (plus $x#235249 $y#235250))) (plusRightId (S (S (plus $x#235249 $y#235250)))))), (: (Replace0 (Cong (Cong ((Trans (Sym plusBase)) ((Trans plusBase) plusBase))))) (-> (plusRightId (S $y#234250)) (plusRightId (S (S $y#234250))))), (: (Replace0 (Cong ((Trans (Sym plusBase)) ((Trans plusBase) (Cong plusRec))))) (-> (plusRightId (S (plus $x#464500 $y#464501))) (plusRightId (S (S (plus $x#464500 $y#464501)))))), (: (Replace0 (Cong ((Trans (Sym plusBase)) ((Trans plusBase) (Cong plusRightIdProp))))) (-> (plusRightId (=== (plus $x#464502 Z) $x#464502)) (plusRightId (S (=== (plus $x#464502 Z) $x#464502))))), (: (Replace0 (Cong ((Trans (Sym plusBase)) ((Trans plusBase) (Cong plusBase))))) (-> (plusRightId $y#463801) (plusRightId (S $y#463801)))), (: (Replace0 (Cong ((Trans (Sym plusBase)) ((Trans plusBase) plusRec)))) (-> (plusRightId (plus $x#464800 $y#464801)) (plusRightId (S (plus $x#464800 $y#464801))))), (: (Replace0 (Cong ((Trans (Sym plusBase)) ((Trans plusBase) plusBase)))) (-> (plusRightId $y#463801) (plusRightId (S $y#463801)))), (: ((. (Replace0 (Sym plusRightIdProp))) ((. (Trans plusRec)) ((. Cong) (Replace0 plusRightIdProp)))) (-> (plusRightId $x) (plusRightId (S $x))))]
[()]