%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : SWX208+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n029.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue May 5 07:08:37 PM UTC 2026 % Result : Unknown 0.71s 0.98s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : SWX208+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.10 % Command : run_zenon_modulo %d %s % 0.11/0.30 % Computer : n029.cluster.edu % 0.11/0.30 % Model : x86_64 x86_64 % 0.11/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.30 % Memory : 8042.1875MB % 0.11/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.30 % CPULimit : 300 % 0.11/0.30 % WCLimit : 300 % 0.11/0.30 % DateTime : Tue May 5 11:37:59 EDT 2026 % 0.11/0.30 % CPUTime : % 0.71/0.97 Zenon error: exhausted search space without finding a proof % 0.71/0.97 (* Current branch: % 0.71/0.97 ((left (dIG4)) != (min10 (s (s (s (s (s (z)))))))) % 0.71/0.97 ((cons zenon_X0 (nil)) != (showNum (z))) % 0.71/0.97 ((left (dIG7)) != (min10 (s (s (z))))) % 0.71/0.97 ((left zenon_X18) != (min10 (s (z)))) % 0.71/0.97 ((min10 (s (s (s (s (s (s (z)))))))) != (min10 (s (s (s (z)))))) % 0.71/0.97 ((x) != (add zenon_X3 zenon_X4)) % 0.71/0.97 ((right zenon_X36) != (min10 (s (s (s (s (s (s (s (s (z))))))))))) % 0.71/0.97 ((s (s (s (s (s (s (s (s (z))))))))) != (s (s (s (s (z)))))) % 0.71/0.97 ((right zenon_X34) != (min10 (s (s (s (s (z))))))) % 0.71/0.97 ((show zenon_X30) != (show zenon_X31)) % 0.71/0.97 ((s (s (s (s (s (z)))))) != (s (z))) % 0.71/0.97 ((left (dIG7)) != (right zenon_X40)) % 0.71/0.97 ((right zenon_X34) != (min10 (s (s (s (s (s (s (z))))))))) % 0.71/0.97 ((right zenon_X32) != (min10 (s (s (z))))) % 0.71/0.97 ((left (dIG3)) != (min10 (s (s (s (s (s (s (s (s (s (z)))))))))))) % 0.71/0.97 ((left (dIG2)) != (min10 (s (s (s (s (s (s (s (z)))))))))) % 0.71/0.97 ((left (dIG6)) != (right zenon_X40)) % 0.71/0.97 ((left (dIG1)) != (min10 (s (s (s (s (s (s (s (z)))))))))) % 0.71/0.97 ((s (s (s (s (s (z)))))) != (z)) % 0.71/0.97 ((dIG3) != (dIG4)) % 0.71/0.97 ((pAR1) != (dIG1)) % 0.71/0.97 ((right zenon_X32) != (min10 (z))) % 0.71/0.97 ((showNum (z)) = (cons (dIG0) (nil))) % 0.71/0.97 ((left zenon_X18) != (min10 (s (s (s (s (s (s (s (z)))))))))) % 0.71/0.97 ((right zenon_X33) != (min10 (s (s (s (s (s (s (s (s (z))))))))))) % 0.71/0.97 ((dIG1) != (dIG8)) % 0.71/0.97 ((pAR2) != (cHARX)) % 0.71/0.97 ((left (dIG1)) != (left zenon_X18)) % 0.71/0.97 ((left (dIG1)) != (min10 (s (s (z))))) % 0.71/0.97 ((left (dIG1)) != (min10 (s (s (s (s (s (s (z))))))))) % 0.71/0.97 ((left (dIG7)) != (left zenon_X18)) % 0.71/0.97 ((left (dIG1)) != (min10 (z))) % 0.71/0.97 ((right zenon_X39) != (min10 (s (s (s (s (z))))))) % 0.71/0.97 ((left (dIG3)) != (right zenon_X32)) % 0.71/0.97 ((min10 (s (z))) != (min10 (z))) % 0.71/0.97 ((left (dIG9)) != (left (dIG3))) % 0.71/0.97 ((left zenon_X18) != (min10 (z))) % 0.71/0.97 ((right zenon_X37) != (min10 (s (s (s (z)))))) % 0.71/0.97 ((left (dIG8)) != (left (dIG3))) % 0.71/0.97 ((right zenon_X33) != (min10 (s (s (s (s (s (s (z))))))))) % 0.71/0.97 ((min10 (s (s (s (s (s (s (s (s (z)))))))))) = (left (dIG8))) % 0.71/0.97 ((left zenon_X18) != (min10 (s (s (s (s (s (s (s (s (s (z)))))))))))) % 0.71/0.97 ((left (dIG5)) != (left (dIG3))) % 0.71/0.97 ((showF (x)) = (show (x))) % 0.71/0.97 ((right zenon_X34) != (min10 (s (s (s (s (s (s (s (s (z))))))))))) % 0.71/0.97 ((left (dIG8)) != (min10 (s (s (s (s (s (s (s (z)))))))))) % 0.71/0.97 ((left (dIG0)) != (min10 (s (s (z))))) % 0.71/0.97 ((left (dIG9)) != (min10 (s (z)))) % 0.71/0.97 ((left (dIG6)) != (min10 (s (s (s (z)))))) % 0.71/0.97 ((pAR2) != (dIG4)) % 0.71/0.97 ((left (dIG9)) != (min10 (s (s (s (z)))))) % 0.71/0.97 ((min10 (s (s (s (s (s (s (s (s (z)))))))))) != (min10 (s (s (s (s (s (z)))))))) % 0.71/0.97 ((left (dIG3)) != (right zenon_X36)) % 0.71/0.97 ((pLUS) != (dIG3)) % 0.71/0.97 ((right zenon_X38) != (min10 (s (s (s (s (z))))))) % 0.71/0.97 ((s (s (z))) != (x2 (z) (z))) % 0.71/0.97 ((left (dIG9)) != (left (dIG1))) % 0.71/0.97 ((left (dIG4)) != (min10 (s (s (s (s (s (s (s (s (s (z)))))))))))) % 0.71/0.97 ((left (dIG4)) != (right zenon_X37)) % 0.71/0.97 ((min10 (s (s (s (z))))) != (min10 (s (z)))) % 0.71/0.97 ((left (dIG3)) != (right zenon_X37)) % 0.71/0.97 ((left (dIG9)) != (right zenon_X38)) % 0.71/0.97 ((right zenon_X37) != (min10 (s (s (s (s (z))))))) % 0.71/0.97 ((right zenon_X38) != (min10 (s (s (s (s (s (s (s (z)))))))))) % 0.71/0.97 ((s (s (s (s (s (s (s (s (s (z)))))))))) != (s (z))) % 0.71/0.97 ((dIG0) != (dIG8)) % 0.71/0.97 ((left (dIG4)) != (right zenon_X36)) % 0.71/0.97 ((right zenon_X35) != (min10 (s (s (s (s (s (s (z))))))))) % 0.71/0.97 ((pLUS) != (mULT)) % 0.71/0.97 ((min10 (s (s (s (s (s (s (s (s (s (z))))))))))) != (min10 (s (s (s (s (s (s (s (z)))))))))) % 0.71/0.97 ((cons (cHARX) (nil)) != (show zenon_X31)) % 0.71/0.97 ((s (s (s (s (s (z)))))) != (s (s (s (s (z)))))) % 0.71/0.97 ((dIG3) != (dIG7)) % 0.71/0.97 ((dIG0) != zenon_X18) % 0.71/0.97 ((cons (cHARX) (nil)) != (showF zenon_X31)) % 0.71/0.97 ((left (dIG3)) != (left (dIG0))) % 0.71/0.97 ((left (dIG0)) != (min10 (s (s (s (s (s (z)))))))) % 0.71/0.97 ((left (dIG6)) != (min10 (s (s (s (s (s (s (s (s (z))))))))))) % 0.71/0.97 ((nil) != (cons (dIG0) zenon_X42)) % 0.71/0.97 ((left (dIG7)) != (min10 (s (s (s (s (s (s (z))))))))) % 0.71/0.97 ((left (dIG8)) != (min10 (s (s (s (s (s (z)))))))) % 0.71/0.97 ((right zenon_X39) != (min10 (s (s (s (s (s (s (s (s (z))))))))))) % 0.71/0.97 ((cons (dIG0) (nil)) != (cons (cHARX) zenon_X43)) % 0.71/0.97 ((min10 (s (s (s (s (s (s (s (s (s (z))))))))))) != (min10 (s (z)))) % 0.71/0.97 ((left (dIG6)) != (min10 (s (s (s (s (z))))))) % 0.71/0.97 ((right zenon_X32) != (min10 (s (s (s (z)))))) % 0.71/0.97 ((s (s (s (s (s (s (s (z)))))))) != (s (s (z)))) % 0.71/0.97 ((cons (cHARX) (nil)) != (showF zenon_X30)) % 0.71/0.97 ((left (dIG7)) != (min10 (s (s (s (s (s (z)))))))) % 0.71/0.97 ((left (dIG3)) != (min10 (z))) % 0.71/0.97 ((show zenon_X31) != (showF zenon_X30)) % 0.71/0.97 ((left (dIG5)) != (min10 (s (s (s (z)))))) % 0.71/0.97 ((dIG3) != (dIG6)) % 0.71/0.97 ((cons (cHARX) (nil)) != (cons (dIG0) zenon_X42)) % 0.71/0.97 ((left (dIG9)) != (left (dIG2))) % 0.71/0.97 ((left (dIG9)) != (min10 (s (s (s (s (s (s (s (s (z))))))))))) % 0.71/0.97 ((left (dIG5)) != (min10 (s (s (s (s (s (s (s (s (z))))))))))) % 0.71/0.97 ((left (dIG7)) != (right zenon_X35)) % 0.71/0.97 ((s (s (s (s (s (s (z))))))) != (x2 (z) (z))) % 0.71/0.97 ((mULT) != (dIG8)) % 0.71/0.97 ((left (dIG0)) != (right zenon_X32)) % 0.71/0.97 ((left (dIG2)) != (min10 (z))) % 0.71/0.97 ((left (dIG4)) != (min10 (s (s (s (z)))))) % 0.71/0.97 ((s (s (s (s (s (s (s (s (z))))))))) != (z)) % 0.71/0.97 ((cons (pAR1) (cons (pAR1) (cons (cHARX) (cons (pLUS) (cons (dIG5) (cons (pAR2) (cons (pLUS) (cons (dIG7) (cons (pAR2) (cons (mULT) (cons (cHARX) (nil)))))))))))) != (showF zenon_X31)) % 0.71/0.97 ((left (dIG5)) != (right zenon_X35)) % 0.71/0.97 ((left (dIG1)) != (min10 (s (s (s (z)))))) % 0.71/0.97 ((left (dIG5)) != (right zenon_X33)) % 0.71/0.97 ((pAR1) != (dIG9)) % 0.71/0.97 ((dIG0) != (dIG4)) % 0.71/0.97 ((left (dIG7)) != (right zenon_X38)) % 0.71/0.97 ((showF zenon_X30) = (show zenon_X30)) % 0.71/0.97 ((left (dIG8)) != (right zenon_X35)) % 0.71/0.97 ((left (dIG1)) != (min10 (s (s (s (s (s (s (s (s (z))))))))))) % 0.71/0.97 ((dIG2) != (dIG6)) % 0.71/0.97 ((min10 (s (s (s (s (s (z))))))) != (min10 (s (s (z))))) % 0.71/0.97 ((mULT) != (dIG1)) % 0.71/0.97 ((left (dIG6)) != (right zenon_X41)) % 0.71/0.97 ((x) != (mul zenon_X5 zenon_X6)) % 0.71/0.97 ((left (dIG1)) != (right zenon_X32)) % 0.71/0.97 ((dIG4) != (dIG6)) % 0.71/0.97 ((left (dIG8)) != (right zenon_X38)) % 0.71/0.97 ((cons (cHARX) (nil)) != (cons zenon_X0 zenon_X1)) % 0.71/0.97 ((left (dIG5)) != (min10 (s (s (s (s (s (s (z))))))))) % 0.71/0.97 ((cons (dIG0) (nil)) != (showF (x))) % 0.71/0.97 ((left (dIG5)) != (right zenon_X34)) % 0.71/0.97 ((min10 (s (s (s (s (s (s (s (s (z)))))))))) != (min10 (s (s (s (s (z))))))) % 0.71/0.97 ((left (dIG7)) != (left (dIG0))) % 0.71/0.97 ((min10 (s (s (s (s (s (s (s (s (s (z))))))))))) != (min10 (s (s (s (s (z))))))) % 0.71/0.97 ((s (s (s (s (s (s (s (s (s (z)))))))))) != (s (s (s (s (s (s (s (z))))))))) % 0.71/0.97 ((s (s (s (s (s (s (s (s (z))))))))) != (x2 (z) (z))) % 0.71/0.97 ((show zenon_X30) != (cons (pAR1) (cons (pAR1) (cons (cHARX) (cons (pLUS) (cons (dIG5) (cons (pAR2) (cons (pLUS) (cons (dIG7) (cons (pAR2) (cons (mULT) (cons (cHARX) (nil))))))))))))) % 0.71/0.97 ((left (dIG4)) != (min10 (s (s (s (s (s (s (z))))))))) % 0.71/0.97 ((left (dIG6)) != (right zenon_X33)) % 0.71/0.97 ((left (dIG8)) != (left (dIG2))) % 0.71/0.97 ((min10 (s (s (s (s (s (s (s (s (s (z))))))))))) != (min10 (s (s (z))))) % 0.71/0.97 ((dIG5) != (dIG9)) % 0.71/0.97 ((dIG9) != zenon_X18) % 0.71/0.97 ((left (dIG7)) != (right zenon_X41)) % 0.71/0.97 ((pAR2) != (dIG8)) % 0.71/0.97 ((left (dIG5)) != (min10 (z))) % 0.71/0.97 ((left (dIG6)) != (left (dIG3))) % 0.71/0.97 ((dIG0) != (dIG2)) % 0.71/0.97 ((left (dIG7)) != (min10 (s (s (s (z)))))) % 0.71/0.97 ((dIG6) != (dIG9)) % 0.71/0.97 ((right zenon_X32) != (min10 (s (s (s (s (z))))))) % 0.71/0.97 ((x) != (num zenon_X7)) % 0.71/0.97 ((right zenon_X37) != (min10 (s (s (s (s (s (z)))))))) % 0.71/0.97 ((left (dIG6)) != (right zenon_X39)) % 0.71/0.97 ((show (x)) != (showF zenon_X31)) % 0.71/0.97 ((left (dIG2)) != (right zenon_X35)) % 0.71/0.97 ((showF zenon_X30) != (showF (x))) % 0.71/0.97 ((dIG4) != (dIG9)) % 0.71/0.97 ((left (dIG8)) != (right zenon_X33)) % 0.71/0.97 ((left (dIG5)) != (right zenon_X41)) % 0.71/0.97 ((min10 (s (s (s (s (s (z))))))) != (min10 (s (z)))) % 0.71/0.97 ((right zenon_X40) != (min10 (s (s (s (s (s (s (s (z)))))))))) % 0.71/0.97 ((dIG3) != (dIG8)) % 0.71/0.97 ((pLUS) != (dIG0)) % 0.71/0.97 ((left (dIG9)) != (right zenon_X36)) % 0.71/0.97 ((left (dIG6)) != (right zenon_X36)) % 0.71/0.97 ((min10 (s (s (s (s (s (s (s (z))))))))) != (min10 (s (s (s (z)))))) % 0.71/0.97 ((dIG7) != (dIG9)) % 0.71/0.97 ((left (dIG7)) != (min10 (s (s (s (s (s (s (s (s (s (z)))))))))))) % 0.71/0.97 ((left (dIG2)) != (left (dIG1))) % 0.71/0.97 ((add zenon_X8 zenon_X9) != (mul zenon_X10 zenon_X11)) % 0.71/0.97 ((left (dIG7)) != (min10 (s (z)))) % 0.71/0.97 ((pLUS) != (dIG2)) % 0.71/0.97 ((left zenon_X18) != (min10 (s (s (s (s (s (z)))))))) % 0.71/0.97 ((s (s (s (s (s (s (s (z)))))))) != (s (s (s (z))))) % 0.71/0.97 ((cons (dIG0) (nil)) != (cons (pAR1) (cons (pAR1) (cons (cHARX) (cons (pLUS) (cons (dIG5) (cons (pAR2) (cons (pLUS) (cons (dIG7) (cons (pAR2) (cons (mULT) (cons (cHARX) (nil))))))))))))) % 0.71/0.97 ((mULT) != (dIG2)) % 0.71/0.97 ((s (z)) != (z)) % 0.71/0.97 ((left (dIG2)) != (left zenon_X18)) % 0.71/0.97 ((dIG6) != zenon_X18) % 0.71/0.97 ((min10 (s (z))) = (left (dIG1))) % 0.71/0.97 ((s (s (s (s (s (s (s (z)))))))) != (z)) % 0.71/0.97 ((right zenon_X32) != (min10 (s (s (s (s (s (s (z))))))))) % 0.71/0.97 ((right zenon_X40) != (min10 (s (s (s (s (s (s (s (s (s (z)))))))))))) % 0.71/0.97 ((left (dIG8)) != (right zenon_X41)) % 0.71/0.97 ((left (dIG8)) != (min10 (z))) % 0.71/0.97 ((right zenon_X39) != (min10 (s (s (s (s (s (s (z))))))))) % 0.71/0.97 ((cons (pAR1) (cons (pAR1) (cons (cHARX) (cons (pLUS) (cons (dIG5) (cons (pAR2) (cons (pLUS) (cons (dIG7) (cons (pAR2) (cons (mULT) (cons (cHARX) (nil)))))))))))) != (showF (x))) % 0.71/0.97 ((right zenon_X39) != (min10 (s (s (s (s (s (s (s (z)))))))))) % 0.71/0.97 ((cons zenon_X0 zenon_X1) != (showF (x))) % 0.71/0.97 ((left (dIG9)) != (left (dIG7))) % 0.71/0.97 ((right zenon_X37) != (min10 (s (s (s (s (s (s (s (s (z))))))))))) % 0.71/0.97 ((left (dIG8)) != (min10 (s (z)))) % 0.71/0.97 ((pAR2) != (dIG7)) % 0.71/0.97 ((right zenon_X35) != (min10 (s (s (s (s (z))))))) % 0.71/0.97 ((left (dIG9)) != (min10 (s (s (s (s (z))))))) % 0.71/0.97 ((left (dIG9)) != (min10 (s (s (s (s (s (z)))))))) % 0.71/0.97 ((pAR1) != (dIG2)) % 0.71/0.97 ((left (dIG2)) != (min10 (s (s (s (s (z))))))) % 0.71/0.97 ((min10 (s (s (z)))) != (min10 (s (z)))) % 0.71/0.97 ((pAR1) != (dIG4)) % 0.71/0.97 ((dIG2) != zenon_X18) % 0.71/0.97 ((min10 (s (s (s (s (s (z))))))) != (min10 (s (s (s (s (z))))))) % 0.71/0.97 ((left (dIG4)) != (right zenon_X34)) % 0.71/0.97 ((pAR2) != (dIG1)) % 0.71/0.97 ((pLUS) != (dIG7)) % 0.71/0.97 ((left (dIG7)) != (left (dIG2))) % 0.71/0.97 ((left (dIG8)) != (left (dIG5))) % 0.71/0.97 ((pAR2) != (pLUS)) % 0.71/0.97 ((add zenon_X12 zenon_X13) != (num zenon_X14)) % 0.71/0.97 ((left (dIG4)) != (min10 (s (s (z))))) % 0.71/0.97 ((left (dIG7)) != (min10 (s (s (s (s (s (s (s (s (z))))))))))) % 0.71/0.97 ((dIG1) != (dIG6)) % 0.71/0.97 ((min10 (s (s (s (s (z)))))) != (min10 (s (s (z))))) % 0.71/0.97 ((left (dIG5)) != (right zenon_X39)) % 0.71/0.97 ((left (dIG9)) != (right zenon_X39)) % 0.71/0.97 ((nil) != (cons zenon_X0 zenon_X1)) % 0.71/0.97 ((min10 (s (s (s (s (s (s (s (z))))))))) != (min10 (s (s (s (s (s (z)))))))) % 0.71/0.97 ((cHARX) != (dIG0)) % 0.71/0.97 ((z) != (s zenon_X2)) % 0.71/0.97 ((left (dIG7)) != (min10 (z))) % 0.71/0.97 ((left (dIG8)) != (right zenon_X34)) % 0.71/0.97 ((left (dIG7)) != (min10 (s (s (s (s (z))))))) % 0.71/0.97 ((pAR2) != (dIG9)) % 0.71/0.97 ((right zenon_X32) != (min10 (s (s (s (s (s (s (s (s (s (z)))))))))))) % 0.71/0.97 ((cons (dIG0) (nil)) != (cons zenon_X0 zenon_X1)) % 0.71/0.97 ((left (dIG0)) != (min10 (s (s (s (s (z))))))) % 0.71/0.97 ((right zenon_X36) != (min10 (s (s (s (s (s (s (s (z)))))))))) % 0.71/0.97 ((left (dIG8)) != (left zenon_X18)) % 0.71/0.97 ((mul zenon_X15 zenon_X16) != (num zenon_X17)) % 0.71/0.97 ((cons (dIG0) zenon_X42) != (show (x))) % 0.71/0.97 ((left (dIG0)) != (min10 (s (s (s (z)))))) % 0.71/0.97 ((s (s (s (s (s (s (z))))))) != (s (s (s (s (z)))))) % 0.71/0.97 ((min10 (s (s (s (s (s (s (s (s (z)))))))))) != (min10 (z))) % 0.71/0.97 ((s (s (s (s (s (s (s (s (s (z)))))))))) != (s (s (s (s (s (s (s (s (z)))))))))) % 0.71/0.97 ((right zenon_X33) != (min10 (s (s (s (z)))))) % 0.71/0.97 ((min10 (s (s (s (s (s (s (s (s (s (z))))))))))) != (min10 (s (s (s (s (s (z)))))))) % 0.71/0.97 ((right zenon_X36) != (min10 (s (s (s (s (s (z)))))))) % 0.71/0.97 ((dIG1) != (dIG4)) % 0.71/0.97 ((min10 (s (s (s (s (z)))))) = (left (dIG4))) % 0.71/0.97 ((dIG1) != (dIG9)) % 0.71/0.97 ((right zenon_X40) != (min10 (s (s (s (s (s (s (z))))))))) % 0.71/0.97 ((s (s (s (s (s (s (s (s (s (z)))))))))) != (z)) % 0.71/0.97 ((s (s (s (s (s (s (s (s (z))))))))) != (s (s (s (s (s (s (z)))))))) % 0.71/0.97 ((min10 (s (s (s (s (s (s (s (s (s (z))))))))))) = (left (dIG9))) % 0.71/0.97 ((s (s (s (s (s (z)))))) != (x2 (z) (z))) % 0.71/0.97 ((pAR1) != (dIG6)) % 0.71/0.97 ((pAR1) != (dIG7)) % 0.71/0.97 ((left (dIG5)) != (right zenon_X32)) % 0.71/0.97 ((min10 (s (s (s (z))))) != (min10 (s (s (z))))) % 0.71/0.97 ((right zenon_X34) != (min10 (s (s (s (s (s (z)))))))) % 0.71/0.97 ((right zenon_X37) != (min10 (s (s (s (s (s (s (z))))))))) % 0.71/0.97 ((min10 (s (s (s (s (s (s (s (s (z)))))))))) != (min10 (s (s (s (s (s (s (s (z)))))))))) % 0.71/0.97 ((min10 (s (s (s (z))))) = (left (dIG3))) % 0.71/0.97 ((s (s (s (s (s (s (s (s (z))))))))) != (s (s (z)))) % 0.71/0.97 ((showF zenon_X31) = (show zenon_X31)) % 0.71/0.97 ((left (dIG3)) != (min10 (s (s (s (s (z))))))) % 0.71/0.97 ((left (dIG9)) != (left (dIG4))) % 0.71/0.97 ((left (dIG3)) != (min10 (s (s (s (s (s (s (s (z)))))))))) % 0.71/0.97 ((min10 (s (s (s (s (s (s (s (s (s (z))))))))))) != (min10 (s (s (s (z)))))) % 0.71/0.97 ((right zenon_X37) != (min10 (s (s (s (s (s (s (s (z)))))))))) % 0.71/0.97 ((left (dIG1)) != (left (dIG0))) % 0.71/0.97 ((left (dIG5)) != (min10 (s (s (z))))) % 0.71/0.97 ((left (dIG5)) != (left (dIG0))) % 0.71/0.97 ((dIG0) != (dIG6)) % 0.71/0.97 ((right zenon_X35) != (min10 (s (s (z))))) % 0.71/0.97 ((dIG3) != (dIG9)) % 0.71/0.97 ((right zenon_X41) != (min10 (s (s (s (s (s (s (s (s (z))))))))))) % 0.71/0.97 ((left (dIG5)) != (left zenon_X18)) % 0.71/0.97 ((nil) != (showNum (z))) % 0.71/0.97 ((left (dIG8)) != (left (dIG1))) % 0.71/0.97 ((show zenon_X30) != (showF (x))) % 0.71/0.97 ((s (s (s (s (z))))) != (x2 (z) (z))) % 0.71/0.97 ((left (dIG8)) != (min10 (s (s (s (s (z))))))) % 0.71/0.97 ((nil) != (show (x))) % 0.71/0.97 ((min10 (s (s (s (s (s (s (z)))))))) != (min10 (s (z)))) % 0.71/0.97 ((pAR1) != (cHARX)) % 0.71/0.97 ((left (dIG4)) != (right zenon_X35)) % 0.71/0.97 ((left (dIG6)) != (right zenon_X38)) % 0.71/0.97 ((s (s (s (s (s (s (z))))))) != (s (s (z)))) % 0.71/0.97 ((s (s (s (s (s (s (s (s (s (z)))))))))) != (s (s (s (s (s (z))))))) % 0.71/0.97 ((pAR2) != (dIG5)) % 0.71/0.97 ((left (dIG2)) != (right zenon_X34)) % 0.71/0.97 ((cons (dIG0) zenon_X42) != (showNum (z))) % 0.71/0.97 ((s (s (s (s (s (s (s (s (s (z)))))))))) != (s (s (s (s (s (s (z)))))))) % 0.71/0.97 ((right zenon_X35) != (min10 (s (s (s (z)))))) % 0.71/0.97 ((pAR2) != (dIG0)) % 0.71/0.97 ((left (dIG3)) != (left (dIG1))) % 0.71/0.97 ((left (dIG1)) != (min10 (s (s (s (s (s (z)))))))) % 0.71/0.97 ((right zenon_X40) != (min10 (s (s (s (s (s (z)))))))) % 0.71/0.97 ((mULT) != (dIG5)) % 0.71/0.97 ((right zenon_X36) != (min10 (s (s (s (s (s (s (z))))))))) % 0.71/0.97 ((s (s (z))) != (s (z))) % 0.71/0.97 ((left (dIG8)) != (left (dIG7))) % 0.71/0.97 ((min10 (s (s (s (s (s (s (s (s (s (z))))))))))) != (min10 (s (s (s (s (s (s (z))))))))) % 0.71/0.97 ((min10 (s (s (s (s (s (s (s (z))))))))) != (min10 (s (z)))) % 0.71/0.97 ((min10 (s (s (z)))) = (left (dIG2))) % 0.71/0.97 ((s (s (s (s (s (s (s (s (z))))))))) != (s (s (s (s (s (s (s (z))))))))) % 0.71/0.97 ((s (s (s (s (s (s (s (z)))))))) != (s (z))) % 0.71/0.97 ((show zenon_X31) != (show (x))) % 0.71/0.97 ((pLUS) != (dIG1)) % 0.71/0.97 ((right zenon_X32) != (min10 (s (s (s (s (s (s (s (z)))))))))) % 0.71/0.97 ((s (s (s (s (s (s (s (s (s (z)))))))))) != (s (s (s (z))))) % 0.71/0.97 ((cons (cHARX) (nil)) != (cons (cHARX) zenon_X43)) % 0.71/0.97 ((right zenon_X33) != (min10 (s (s (s (s (s (z)))))))) % 0.71/0.97 ((pLUS) != (dIG5)) % 0.71/0.97 ((s (s (s (s (z))))) != (z)) % 0.71/0.97 ((nil) != (cons zenon_X0 (nil))) % 0.71/0.97 ((dIG8) != zenon_X18) % 0.71/0.97 ((left (dIG7)) != (left (dIG4))) % 0.71/0.97 ((s (s (s (s (z))))) != (s (z))) % 0.71/0.97 ((mULT) != (dIG4)) % 0.71/0.97 ((cons (cHARX) (nil)) != (cons (pAR1) (cons (pAR1) (cons (cHARX) (cons (pLUS) (cons (dIG5) (cons (pAR2) (cons (pLUS) (cons (dIG7) (cons (pAR2) (cons (mULT) (cons (cHARX) (nil))))))))))))) % 0.71/0.97 ((left (dIG4)) != (right zenon_X33)) % 0.71/0.97 ((s (s (s (z)))) != (s (s (z)))) % 0.71/0.97 ((left zenon_X18) != (min10 (s (s (s (s (s (s (z))))))))) % 0.71/0.97 ((left (dIG6)) != (min10 (s (s (s (s (s (s (s (z)))))))))) % 0.71/0.97 ((s (s (s (z)))) != (s (z))) % 0.71/0.97 ((min10 (s (s (s (s (z)))))) != (min10 (z))) % 0.71/0.97 ((s (s (s (s (s (s (z))))))) != (z)) % 0.71/0.97 ((left (dIG2)) != (min10 (s (s (s (z)))))) % 0.71/0.97 ((left (dIG3)) != (min10 (s (s (s (s (s (z)))))))) % 0.71/0.97 ((nil) != zenon_X42) % 0.71/0.97 ((cons (cHARX) (nil)) != (showNum (z))) % 0.71/0.97 ((min10 (s (s (s (s (s (s (z)))))))) != (min10 (s (s (s (s (z))))))) % 0.71/0.97 ((left (dIG0)) != (min10 (s (s (s (s (s (s (s (z)))))))))) % 0.71/0.97 ((left (dIG8)) != (min10 (s (s (s (z)))))) % 0.71/0.97 ((cons zenon_X0 (nil)) != (show (x))) % 0.71/0.97 ((s (z)) != (x2 (z) (z))) % 0.71/0.97 ((dIG0) != (dIG5)) % 0.71/0.97 ((cons (cHARX) (nil)) != (cons zenon_X0 (nil))) % 0.71/0.97 ((left (dIG7)) != (left (dIG3))) % 0.71/0.97 ((right zenon_X33) != (min10 (s (z)))) % 0.71/0.97 ((s (s (s (z)))) != (z)) % 0.71/0.97 ((right zenon_X38) != (min10 (s (s (s (s (s (s (z))))))))) % 0.71/0.97 ((right zenon_X35) != (min10 (s (s (s (s (s (s (s (s (z))))))))))) % 0.71/0.97 ((dIG4) != zenon_X18) % 0.71/0.97 ((cHARX) != (dIG9)) % 0.71/0.97 ((min10 (s (s (s (s (s (s (s (z))))))))) != (min10 (z))) % 0.71/0.97 ((dIG1) != (dIG2)) % 0.71/0.97 ((left (dIG7)) != (left (dIG1))) % 0.71/0.97 ((left (dIG5)) != (left (dIG4))) % 0.71/0.97 ((left (dIG3)) != (left zenon_X18)) % 0.71/0.97 ((nil) != (cons (cHARX) zenon_X43)) % 0.71/0.97 ((left (dIG9)) != (left (dIG5))) % 0.71/0.97 ((left (dIG3)) != (left (dIG2))) % 0.71/0.97 ((nil) != zenon_X43) % 0.71/0.97 ((left (dIG2)) != (right zenon_X33)) % 0.71/0.97 ((cons (cHARX) (nil)) != (show zenon_X30)) % 0.71/0.97 ((cons (cHARX) zenon_X43) != (showF (x))) % 0.71/0.97 ((left (dIG7)) != (right zenon_X33)) % 0.71/0.97 ((left (dIG9)) != (right zenon_X34)) % 0.71/0.97 ((dIG0) != (dIG7)) % 0.71/0.97 ((left (dIG3)) != (min10 (s (s (z))))) % 0.71/0.97 ((left (dIG4)) != (min10 (s (s (s (s (s (s (s (z)))))))))) % 0.71/0.97 ((dIG3) != (dIG5)) % 0.71/0.97 ((pAR1) != (dIG5)) % 0.71/0.97 ((cons (pAR1) (cons (pAR1) (cons (cHARX) (cons (pLUS) (cons (dIG5) (cons (pAR2) (cons (pLUS) (cons (dIG7) (cons (pAR2) (cons (mULT) (cons (cHARX) (nil)))))))))))) != (showNum (z))) % 0.71/0.97 ((left (dIG9)) != (right zenon_X40)) % 0.71/0.97 ((left (dIG6)) != (right zenon_X35)) % 0.71/0.97 ((left (dIG8)) != (left (dIG0))) % 0.71/0.97 ((nil) != (cons (dIG0) (nil))) % 0.71/0.97 ((left zenon_X18) != (min10 (s (s (z))))) % 0.71/0.97 ((dIG3) != zenon_X18) % 0.71/0.97 ((right zenon_X41) != (min10 (s (s (s (s (s (s (z))))))))) % 0.71/0.97 ((dIG4) != (dIG5)) % 0.71/0.97 ((left (dIG6)) != (left (dIG2))) % 0.71/0.97 ((left (dIG4)) != (min10 (z))) % 0.71/0.97 ((s (s (s (s (z))))) != (s (s (s (z))))) % 0.71/0.97 ((right zenon_X35) != (min10 (s (s (s (s (s (s (s (s (s (z)))))))))))) % 0.71/0.97 ((cons (cHARX) (nil)) != (cons (dIG0) (nil))) % 0.71/0.97 ((left (dIG6)) != (min10 (z))) % 0.71/0.97 ((left (dIG0)) != (left zenon_X18)) % 0.71/0.97 ((cHARX) != zenon_X0) % 0.71/0.97 ((mULT) != (dIG0)) % 0.71/0.97 ((left (dIG1)) != (right zenon_X33)) % 0.71/0.97 ((left (dIG9)) != (right zenon_X37)) % 0.71/0.97 ((dIG2) != (dIG8)) % 0.71/0.97 ((s (s (s (s (s (z)))))) != (s (s (s (z))))) % 0.71/0.97 ((left (dIG6)) != (right zenon_X34)) % 0.71/0.97 ((min10 (s (s (s (s (s (s (s (s (z)))))))))) != (min10 (s (s (s (z)))))) % 0.71/0.97 ((s (s (s (s (s (s (z))))))) != (s (s (s (s (s (z))))))) % 0.71/0.97 ((s (s (z))) != (z)) % 0.71/0.97 ((left (dIG5)) != (right zenon_X37)) % 0.71/0.97 ((min10 (z)) = (left (dIG0))) % 0.71/0.97 ((left (dIG4)) != (left (dIG3))) % 0.71/0.97 ((min10 (s (s (s (s (s (s (s (z))))))))) != (min10 (s (s (s (s (s (s (z))))))))) % 0.71/0.97 ((min10 (s (s (s (s (s (s (s (z))))))))) = (left (dIG7))) % 0.71/0.97 ((left (dIG7)) != (right zenon_X36)) % 0.71/0.97 ((showF zenon_X31) != (showF (x))) % 0.71/0.97 ((right zenon_X36) != (min10 (s (s (s (z)))))) % 0.71/0.97 ((cHARX) != (dIG6)) % 0.71/0.97 ((min10 (s (s (s (s (s (s (z)))))))) != (min10 (z))) % 0.71/0.97 ((s (s (s (s (s (s (s (z)))))))) != (s (s (s (s (s (z))))))) % 0.71/0.97 ((right zenon_X32) != (min10 (s (z)))) % 0.71/0.97 ((left (dIG3)) != (min10 (s (z)))) % 0.71/0.97 ((show zenon_X30) != (showF zenon_X31)) % 0.71/0.97 ((dIG1) != (dIG5)) % 0.71/0.97 ((left (dIG4)) != (right zenon_X38)) % 0.71/0.97 ((mULT) != (cHARX)) % 0.71/0.97 ((right zenon_X33) != (min10 (s (s (z))))) % 0.71/0.97 ((cons (pAR1) (cons (pAR1) (cons (cHARX) (cons (pLUS) (cons (dIG5) (cons (pAR2) (cons (pLUS) (cons (dIG7) (cons (pAR2) (cons (mULT) (cons (cHARX) (nil)))))))))))) != (show (x))) % 0.71/0.97 ((left (dIG6)) != (left (dIG5))) % 0.71/0.97 ((left (dIG5)) != (right zenon_X36)) % 0.71/0.97 ((cHARX) != (dIG2)) % 0.71/0.97 ((left (dIG6)) != (right zenon_X32)) % 0.71/0.97 ((right zenon_X34) != (min10 (s (s (s (s (s (s (s (s (s (z)))))))))))) % 0.71/0.97 ((left (dIG2)) != (min10 (s (s (s (s (s (s (s (s (s (z)))))))))))) % 0.71/0.97 ((left (dIG2)) != (right zenon_X32)) % 0.71/0.97 ((pAR1) != (dIG8)) % 0.71/0.97 ((right zenon_X32) != (min10 (s (s (s (s (s (s (s (s (z))))))))))) % 0.71/0.97 ((left (dIG9)) != (right zenon_X41)) % 0.71/0.97 ((pLUS) != (dIG8)) % 0.71/0.97 ((s (s (s (s (s (s (z))))))) != (s (s (s (z))))) % 0.71/0.97 ((left zenon_X18) != (min10 (s (s (s (s (s (s (s (s (z))))))))))) % 0.71/0.97 ((dIG7) != (dIG8)) % 0.71/0.97 ((left (dIG4)) != (left (dIG1))) % 0.71/0.97 ((left (dIG8)) != (min10 (s (s (s (s (s (s (s (s (s (z)))))))))))) % 0.71/0.97 ((showF zenon_X30) != (showF zenon_X31)) % 0.71/0.97 ((min10 (s (s (s (s (s (s (s (z))))))))) != (min10 (s (s (z))))) % 0.71/0.97 ((s (s (s (s (s (s (z))))))) != (s (z))) % 0.71/0.97 ((left (dIG5)) != (min10 (s (s (s (s (s (s (s (s (s (z)))))))))))) % 0.71/0.97 ((show zenon_X31) != (showF (x))) % 0.71/0.97 ((dIG5) != (dIG7)) % 0.71/0.97 ((left (dIG4)) != (min10 (s (s (s (s (s (s (s (s (z))))))))))) % 0.71/0.97 ((min10 (s (s (s (s (s (s (z)))))))) = (left (dIG6))) % 0.71/0.97 ((left (dIG4)) != (min10 (s (z)))) % 0.71/0.97 ((left (dIG3)) != (min10 (s (s (s (s (s (s (z))))))))) % 0.71/0.97 ((left (dIG6)) != (min10 (s (s (s (s (s (z)))))))) % 0.71/0.97 ((s (s (s (s (s (s (s (s (s (z)))))))))) != (x2 (z) (z))) % 0.71/0.97 ((cHARX) != (dIG4)) % 0.71/0.97 ((dIG5) != zenon_X18) % 0.71/0.97 ((left (dIG2)) != (min10 (s (z)))) % 0.71/0.97 ((mULT) != (dIG7)) % 0.71/0.97 ((s (s (s (s (z))))) != (s (s (z)))) % 0.71/0.97 ((left (dIG8)) != (right zenon_X36)) % 0.71/0.97 ((left (dIG8)) != (left (dIG6))) % 0.71/0.97 ((min10 (s (s (s (s (s (z))))))) != (min10 (s (s (s (z)))))) % 0.71/0.97 ((dIG6) != (dIG8)) % 0.71/0.97 ((mULT) != (dIG3)) % 0.71/0.97 ((left (dIG9)) != (right zenon_X32)) % 0.71/0.97 ((right zenon_X38) != (min10 (s (s (s (s (s (s (s (s (z))))))))))) % 0.71/0.97 ((left (dIG5)) != (min10 (s (z)))) % 0.71/0.97 ((left (dIG8)) != (right zenon_X32)) % 0.71/0.97 ((right zenon_X34) != (min10 (s (s (s (z)))))) % 0.71/0.97 ((left (dIG7)) != (right zenon_X37)) % 0.71/0.97 ((left (dIG8)) != (min10 (s (s (s (s (s (s (z))))))))) % 0.71/0.97 ((right zenon_X41) != (min10 (s (s (s (s (s (z)))))))) % 0.71/0.97 ((min10 (s (s (s (z))))) != (min10 (z))) % 0.71/0.98 ((right zenon_X33) != (min10 (s (s (s (s (s (s (s (s (s (z)))))))))))) % 0.71/0.98 ((s (s (s (s (s (s (s (s (s (z)))))))))) != (s (s (s (s (z)))))) % 0.71/0.98 ((dIG2) != (dIG5)) % 0.71/0.98 ((left (dIG6)) != (left zenon_X18)) % 0.71/0.98 ((left (dIG4)) != (right zenon_X32)) % 0.71/0.98 ((left (dIG9)) != (min10 (z))) % 0.71/0.98 ((right zenon_X40) != (min10 (s (s (s (s (s (s (s (s (z))))))))))) % 0.71/0.98 ((cons (dIG0) (nil)) != (show (x))) % 0.71/0.98 ((cons (cHARX) zenon_X43) != (showNum (z))) % 0.71/0.98 ((left (dIG8)) != (min10 (s (s (z))))) % 0.71/0.98 (zenon_X30 != zenon_X31) % 0.71/0.98 ((right zenon_X38) != (min10 (s (s (s (s (s (s (s (s (s (z)))))))))))) % 0.71/0.98 ((s (s (s (s (s (z)))))) != (s (s (z)))) % 0.71/0.98 ((left (dIG4)) != (left (dIG2))) % 0.71/0.98 ((left (dIG9)) != (min10 (s (s (z))))) % 0.71/0.98 ((left (dIG6)) != (left (dIG4))) % 0.71/0.98 ((showNumnum zenon_X26 (s zenon_X27)) = (showNumnum (cons zenon_X28 zenon_X26) zenon_X29)) % 0.71/0.98 ((min10 (s (s (z)))) != (min10 (z))) % 0.71/0.98 ((left (dIG5)) != (right zenon_X40)) % 0.71/0.98 ((left (dIG5)) != (right zenon_X38)) % 0.71/0.98 ((pLUS) != (dIG9)) % 0.71/0.98 ((min10 (s (s (s (s (s (s (z)))))))) != (min10 (s (s (s (s (s (z)))))))) % 0.71/0.98 ((cons zenon_X0 zenon_X1) != (showNum (z))) % 0.71/0.98 ((right zenon_X41) != (min10 (s (s (s (s (s (s (s (z)))))))))) % 0.71/0.98 ((dIG0) != (dIG1)) % 0.71/0.98 ((left (dIG4)) != (left zenon_X18)) % 0.71/0.98 ((cHARX) != (dIG1)) % 0.71/0.98 ((right zenon_X33) != (min10 (s (s (s (s (s (s (s (z)))))))))) % 0.71/0.98 ((right zenon_X41) != (min10 (s (s (s (s (s (s (s (s (s (z)))))))))))) % 0.71/0.98 ((cHARX) != (dIG8)) % 0.71/0.98 ((left (dIG6)) != (right zenon_X37)) % 0.71/0.98 ((min10 (s (s (s (s (s (s (s (s (s (z))))))))))) != (min10 (z))) % 0.71/0.98 ((showNum (z)) != (showF (x))) % 0.71/0.98 ((dIG4) != (dIG7)) % 0.71/0.98 ((cons zenon_X0 zenon_X1) != (show (x))) % 0.71/0.98 ((left (dIG7)) != (left (dIG5))) % 0.71/0.98 ((cons (dIG0) (nil)) != (cons (dIG0) zenon_X42)) % 0.71/0.98 ((right zenon_X33) != (min10 (s (s (s (s (z))))))) % 0.71/0.98 ((dIG1) != zenon_X18) % 0.71/0.98 ((left (dIG3)) != (right zenon_X33)) % 0.71/0.98 ((min10 (s (s (s (s (s (s (s (z))))))))) != (min10 (s (s (s (s (z))))))) % 0.71/0.98 ((show zenon_X31) != (cons (pAR1) (cons (pAR1) (cons (cHARX) (cons (pLUS) (cons (dIG5) (cons (pAR2) (cons (pLUS) (cons (dIG7) (cons (pAR2) (cons (mULT) (cons (cHARX) (nil))))))))))))) % 0.71/0.98 ((dIG2) != (dIG7)) % 0.71/0.98 ((left (dIG8)) != (right zenon_X40)) % 0.71/0.98 ((min10 (s (s (s (s (z)))))) != (min10 (s (z)))) % 0.71/0.98 ((left (dIG1)) != (min10 (s (s (s (s (z))))))) % 0.71/0.98 ((min10 (s (s (s (s (s (z))))))) = (left (dIG5))) % 0.71/0.98 ((s (s (s (z)))) != (x2 (z) (z))) % 0.71/0.98 ((right zenon_X34) != (min10 (s (s (s (s (s (s (s (z)))))))))) % 0.71/0.98 ((left (dIG8)) != (right zenon_X37)) % 0.71/0.98 ((cons (dIG0) (nil)) != (cons zenon_X0 (nil))) % 0.71/0.98 ((left (dIG7)) != (right zenon_X32)) % 0.71/0.98 ((min10 (s (s (s (s (s (z))))))) != (min10 (z))) % 0.71/0.98 ((left (dIG3)) != (min10 (s (s (s (s (s (s (s (s (z))))))))))) % 0.71/0.98 ((left (dIG0)) != (min10 (s (s (s (s (s (s (z))))))))) % 0.71/0.98 ((left zenon_X18) != (right zenon_X19)) % 0.71/0.98 ((min10 (s (s (s (s (s (s (s (s (s (z))))))))))) != (min10 (s (s (s (s (s (s (s (s (z))))))))))) % 0.71/0.98 ((pAR2) != (dIG3)) % 0.71/0.98 ((left (dIG9)) != (left (dIG8))) % 0.71/0.98 ((right zenon_X32) != (min10 (s (s (s (s (s (z)))))))) % 0.71/0.98 ((left (dIG2)) != (min10 (s (s (s (s (s (s (z))))))))) % 0.71/0.98 ((left (dIG9)) != (right zenon_X33)) % 0.71/0.98 ((left (dIG0)) != (min10 (s (z)))) % 0.71/0.98 ((nil) != (cons (cHARX) (nil))) % 0.71/0.98 ((dIG4) != (dIG8)) % 0.71/0.98 ((min10 (s (s (s (s (z)))))) != (min10 (s (s (s (z)))))) % 0.71/0.98 ((left (dIG2)) != (min10 (s (s (s (s (s (s (s (s (z))))))))))) % 0.71/0.98 ((dIG8) != (dIG9)) % 0.71/0.98 ((pAR2) != (dIG6)) % 0.71/0.98 ((left (dIG9)) != (left (dIG6))) % 0.71/0.98 ((pAR2) != (dIG2)) % 0.71/0.98 ((pLUS) != (dIG4)) % 0.71/0.98 ((min10 (s (s (s (s (s (s (s (s (z)))))))))) != (min10 (s (z)))) % 0.71/0.98 ((right zenon_X39) != (min10 (s (s (s (s (s (s (s (s (s (z)))))))))))) % 0.71/0.98 ((mULT) != (dIG9)) % 0.71/0.98 ((cons (pAR1) (cons (pAR1) (cons (cHARX) (cons (pLUS) (cons (dIG5) (cons (pAR2) (cons (pLUS) (cons (dIG7) (cons (pAR2) (cons (mULT) (cons (cHARX) (nil)))))))))))) != (showF zenon_X30)) % 0.71/0.98 ((right zenon_X36) != (min10 (s (s (s (s (z))))))) % 0.71/0.98 ((left (dIG5)) != (left (dIG1))) % 0.71/0.98 ((pAR1) != (mULT)) % 0.71/0.98 ((left (dIG6)) != (left (dIG0))) % 0.71/0.98 ((s (s (s (s (s (s (s (s (z))))))))) != (s (z))) % 0.71/0.98 ((dIG5) != (dIG8)) % 0.71/0.98 ((pLUS) != (cHARX)) % 0.71/0.98 ((left (dIG9)) != (left zenon_X18)) % 0.71/0.98 ((s (s (s (s (s (s (s (s (z))))))))) != (s (s (s (z))))) % 0.71/0.98 ((dIG0) != (dIG3)) % 0.71/0.98 ((left zenon_X18) != (min10 (s (s (s (z)))))) % 0.71/0.98 ((pAR1) != (dIG3)) % 0.71/0.98 ((dIG0) != zenon_X0) % 0.71/0.98 ((right zenon_X38) != (min10 (s (s (s (s (s (z)))))))) % 0.71/0.98 ((s (s (s (s (s (s (s (s (z))))))))) != (s (s (s (s (s (z))))))) % 0.71/0.98 ((dIG5) != (dIG6)) % 0.71/0.98 ((left (dIG5)) != (left (dIG2))) % 0.71/0.98 ((s (s (s (s (s (s (s (s (s (z)))))))))) != (s (s (z)))) % 0.71/0.98 ((left (dIG2)) != (min10 (s (s (s (s (s (z)))))))) % 0.71/0.98 ((mod10 zenon_X20) = (pair2 zenon_X21 (z))) % 0.71/0.98 ((right zenon_X37) != (min10 (s (s (s (s (s (s (s (s (s (z)))))))))))) % 0.71/0.98 ((right zenon_X35) != (min10 (s (s (s (s (s (s (s (z)))))))))) % 0.71/0.98 ((s (s (s (s (s (s (s (z)))))))) != (s (s (s (s (s (s (z)))))))) % 0.71/0.98 ((dIG0) != (dIG9)) % 0.71/0.98 ((cHARX) != (dIG3)) % 0.71/0.98 ((nil) != zenon_X1) % 0.71/0.98 ((right zenon_X35) != (min10 (s (s (s (s (s (z)))))))) % 0.71/0.98 ((show (x)) != (showF zenon_X30)) % 0.71/0.98 ((min10 (s (s (s (s (s (s (s (s (z)))))))))) != (min10 (s (s (z))))) % 0.71/0.98 ((right zenon_X34) != (min10 (s (s (z))))) % 0.71/0.98 ((left (dIG9)) != (min10 (s (s (s (s (s (s (z))))))))) % 0.71/0.98 ((show (x)) != (showNum (z))) % 0.71/0.98 ((left (dIG3)) != (right zenon_X34)) % 0.71/0.98 ((dIG1) != (dIG3)) % 0.71/0.98 ((left (dIG3)) != (right zenon_X35)) % 0.71/0.98 ((pAR1) != (pAR2)) % 0.71/0.98 ((left (dIG6)) != (min10 (s (s (z))))) % 0.71/0.98 ((dIG2) != (dIG9)) % 0.71/0.98 ((dIG7) != zenon_X18) % 0.71/0.98 ((left (dIG8)) != (left (dIG4))) % 0.71/0.98 ((left (dIG9)) != (min10 (s (s (s (s (s (s (s (z)))))))))) % 0.71/0.98 ((cHARX) != (dIG7)) % 0.71/0.98 ((left (dIG4)) != (left (dIG0))) % 0.71/0.98 ((nil) != (showF (x))) % 0.71/0.98 ((left (dIG5)) != (min10 (s (s (s (s (z))))))) % 0.71/0.98 ((left (dIG0)) != (min10 (s (s (s (s (s (s (s (s (s (z)))))))))))) % 0.71/0.98 ((left (dIG9)) != (right zenon_X35)) % 0.71/0.98 ((s (s (s (s (s (s (s (z)))))))) != (x2 (z) (z))) % 0.71/0.98 ((left (dIG5)) != (min10 (s (s (s (s (s (s (s (z)))))))))) % 0.71/0.98 ((mULT) != (dIG6)) % 0.71/0.98 (zenon_X30 != (x)) % 0.71/0.98 ((pAR1) != (pLUS)) % 0.71/0.98 ((left (dIG9)) != (left (dIG0))) % 0.71/0.98 ((left (dIG1)) != (min10 (s (s (s (s (s (s (s (s (s (z)))))))))))) % 0.71/0.98 ((pAR1) != (dIG0)) % 0.71/0.98 ((left (dIG7)) != (right zenon_X34)) % 0.71/0.98 ((pAR2) != (mULT)) % 0.71/0.98 ((dIG2) != (dIG3)) % 0.71/0.98 ((dIG1) != (dIG7)) % 0.71/0.98 ((mod10 zenon_X22) = (pair2 zenon_X24 (s zenon_X25))) % 0.71/0.98 ((left (dIG7)) != (left (dIG6))) % 0.71/0.98 ((cons zenon_X0 (nil)) != (showF (x))) % 0.71/0.98 ((left (dIG2)) != (left (dIG0))) % 0.71/0.98 ((left (dIG4)) != (right zenon_X39)) % 0.71/0.98 ((min10 (s (s (s (s (s (s (s (s (z)))))))))) != (min10 (s (s (s (s (s (s (z))))))))) % 0.71/0.98 ((left (dIG6)) != (left (dIG1))) % 0.71/0.98 ((s zenon_X2) != (x2 (z) (z))) % 0.71/0.98 ((cHARX) != (dIG5)) % 0.71/0.98 ((show zenon_X30) != (show (x))) % 0.71/0.98 ((dIG6) != (dIG7)) % 0.71/0.98 ((cons (dIG0) zenon_X42) != (showF (x))) % 0.71/0.98 ((x2 (z) (z)) = (z)) % 0.71/0.98 ((left zenon_X18) != (min10 (s (s (s (s (z))))))) % 0.71/0.98 ((left (dIG7)) != (right zenon_X39)) % 0.71/0.98 ((right zenon_X36) != (min10 (s (s (s (s (s (s (s (s (s (z)))))))))))) % 0.71/0.98 ((pLUS) != (dIG6)) % 0.71/0.98 ((left (dIG6)) != (min10 (s (s (s (s (s (s (s (s (s (z)))))))))))) % 0.71/0.98 ((cons (cHARX) zenon_X43) != (show (x))) % 0.71/0.98 ((min10 (s (s (s (s (s (s (z)))))))) != (min10 (s (s (z))))) % 0.71/0.98 ((dIG2) != (dIG4)) % 0.71/0.98 ((left (dIG6)) != (min10 (s (z)))) % 0.71/0.98 ((right zenon_X39) != (min10 (s (s (s (s (s (z)))))))) % 0.71/0.98 ((s (s (s (s (s (s (s (z)))))))) != (s (s (s (s (z)))))) % 0.71/0.98 ((left (dIG8)) != (right zenon_X39)) % 0.71/0.98 (zenon_X31 != (x)) % 0.71/0.98 ((left (dIG0)) != (min10 (s (s (s (s (s (s (s (s (z))))))))))) % 0.71/0.98 ((show (x)) = (cons (cHARX) (nil))) % 0.71/0.98 *) % 0.71/0.98 (* NO-PROOF *) % 0.71/0.98 % SZS status GaveUp % 0.71/0.98 Number of rewrites on terms: 0 % 0.71/0.98 Number of rewrites on props: 0 % 0.71/0.98 nodes searched: 6241 % 0.71/0.98 max branch formulas: 657 % 0.71/0.98 proof nodes created: 264 % 0.71/0.98 formulas created: 8180 % 0.71/0.98 %------------------------------------------------------------------------------