%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SYO668-1 : TPTP v9.2.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.I9nClhy4bL true
% Computer : n001.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 : Thu Oct 2 05:08:06 PM UTC 2025
% Result : Unsatisfiable 4.32s 1.45s
% Output : Refutation 4.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.32 % Problem : SYO668-1 : TPTP v9.2.0. Released v7.3.0.
% 0.11/0.33 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.I9nClhy4bL true
% 0.13/0.55 % Computer : n001.cluster.edu
% 0.13/0.55 % Model : x86_64 x86_64
% 0.13/0.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.55 % Memory : 8042.1875MB
% 0.13/0.55 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.55 % CPULimit : 300
% 0.13/0.55 % WCLimit : 300
% 0.13/0.55 % DateTime : Wed Oct 1 17:53:23 EDT 2025
% 0.13/0.55 % CPUTime :
% 0.13/0.55 % Running portfolio for 300 s
% 0.13/0.55 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.55 % Number of cores: 8
% 0.13/0.55 % Python version: Python 3.6.8
% 0.13/0.55 % Running in FO mode
% 0.20/0.84 % Total configuration time : 435
% 0.20/0.84 % Estimated wc time : 1092
% 0.20/0.84 % Estimated cpu time (7 cpus) : 156.0
% 0.20/0.90 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.20/0.92 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.20/0.92 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.20/0.94 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.20/0.94 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.20/0.95 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.20/0.96 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 4.32/1.45 % Solved by fo/fo4.sh.
% 4.32/1.45 % done 321 iterations in 0.450s
% 4.32/1.45 % SZS status Unsatisfiable for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 4.32/1.45 % SZS output start Refutation
% 4.32/1.45 thf(z_type, type, z: $i).
% 4.32/1.45 thf(suc_type, type, suc: $i > $i).
% 4.32/1.45 thf(f_type, type, f: $i > $i).
% 4.32/1.45 thf(0_type, type, 0: $i).
% 4.32/1.45 thf(E_type, type, E: $i > $i > $o).
% 4.32/1.45 thf(s_type, type, s: $i > $i).
% 4.32/1.45 thf(LE_type, type, LE: $i > $i > $o).
% 4.32/1.45 thf(clause_48, axiom, (~( LE @ ( f @ z ) @ 0 ))).
% 4.32/1.45 thf(zip_derived_cl34, plain, (~ (LE @ (f @ z) @ 0)),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_48])).
% 4.32/1.45 thf(clause_74, axiom,
% 4.32/1.45 (( ~( LE @ ( f @ ( suc @ ( suc @ ( suc @ ( suc @ B_1 ) ) ) ) ) @ ( s @ 0 ) ) ) |
% 4.32/1.45 ( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ ( suc @ B_1 ) ) ) ) ) ) |
% 4.32/1.45 ( LE @ ( f @ B_1 ) @ 0 ))).
% 4.32/1.45 thf(zip_derived_cl5, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (LE @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))) @ (s @ 0))
% 4.32/1.45 | (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | (LE @ (f @ X0) @ 0))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_74])).
% 4.32/1.45 thf(clause_17, axiom,
% 4.32/1.45 (( ~( LE @
% 4.32/1.45 ( f @ ( suc @ ( suc @ ( suc @ ( suc @ B_0 ) ) ) ) ) @
% 4.32/1.45 ( s @ ( s @ 0 ) ) ) ) |
% 4.32/1.45 ( E @ ( s @ 0 ) @ ( f @ ( suc @ ( suc @ ( suc @ ( suc @ B_0 ) ) ) ) ) ) |
% 4.32/1.45 ( LE @ ( f @ B_0 ) @ ( s @ 0 ) ))).
% 4.32/1.45 thf(zip_derived_cl7, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (LE @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))) @ (s @ (s @ 0)))
% 4.32/1.45 | (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ 0)))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_17])).
% 4.32/1.45 thf(clause_73, axiom,
% 4.32/1.45 (( ~( LE @
% 4.32/1.45 ( f @ ( suc @ ( suc @ ( suc @ ( suc @ B ) ) ) ) ) @
% 4.32/1.45 ( s @ ( s @ ( s @ 0 ) ) ) ) ) |
% 4.32/1.45 ( E @
% 4.32/1.45 ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ ( suc @ ( suc @ ( suc @ B ) ) ) ) ) ) |
% 4.32/1.45 ( LE @ ( f @ B ) @ ( s @ ( s @ 0 ) ) ))).
% 4.32/1.45 thf(zip_derived_cl32, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (LE @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))) @
% 4.32/1.45 (s @ (s @ (s @ 0))))
% 4.32/1.45 | (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_73])).
% 4.32/1.45 thf(clause_102, axiom, (LE @ ( f @ A ) @ ( s @ ( s @ ( s @ 0 ) ) ))).
% 4.32/1.45 thf(zip_derived_cl25, plain,
% 4.32/1.45 (![X0 : $i]: (LE @ (f @ X0) @ (s @ (s @ (s @ 0))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_102])).
% 4.32/1.45 thf(zip_derived_cl121, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl32, zip_derived_cl25])).
% 4.32/1.45 thf(clause_25, axiom,
% 4.32/1.45 (( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ A_1 ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ A_1 ) ) ) ) |
% 4.32/1.45 ( ~( E @
% 4.32/1.45 ( s @ ( s @ 0 ) ) @
% 4.32/1.45 ( f @ ( suc @ ( suc @ ( suc @ ( suc @ A_1 ) ) ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( f @ A_1 ) @ ( f @ ( suc @ ( suc @ ( suc @ A_1 ) ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( f @ A_1 ) @ ( f @ ( suc @ ( suc @ A_1 ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ ( suc @ ( suc @ A_1 ) ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( f @ A_1 ) @ ( f @ ( suc @ A_1 ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ ( suc @ A_1 ) ) ) ) ) |
% 4.32/1.45 ( E @ ( f @ A_1 ) @ ( f @ ( suc @ ( suc @ ( suc @ ( suc @ A_1 ) ) ) ) ) ))).
% 4.32/1.45 thf(zip_derived_cl16, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ (suc @ X0)))))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_25])).
% 4.32/1.45 thf(clause_21, axiom,
% 4.32/1.45 (( ~( LE @
% 4.32/1.45 ( f @ ( suc @ ( suc @ ( suc @ ( suc @ ( suc @ B ) ) ) ) ) ) @
% 4.32/1.45 ( s @ ( s @ ( s @ 0 ) ) ) ) ) |
% 4.32/1.45 ( E @
% 4.32/1.45 ( s @ ( s @ 0 ) ) @
% 4.32/1.45 ( f @ ( suc @ ( suc @ ( suc @ ( suc @ ( suc @ B ) ) ) ) ) ) ) |
% 4.32/1.45 ( LE @ ( f @ B ) @ ( s @ ( s @ 0 ) ) ))).
% 4.32/1.45 thf(zip_derived_cl12, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (LE @ (f @ (suc @ (suc @ (suc @ (suc @ (suc @ X0)))))) @
% 4.32/1.45 (s @ (s @ (s @ 0))))
% 4.32/1.45 | (E @ (s @ (s @ 0)) @
% 4.32/1.45 (f @ (suc @ (suc @ (suc @ (suc @ (suc @ X0)))))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_21])).
% 4.32/1.45 thf(zip_derived_cl25, plain,
% 4.32/1.45 (![X0 : $i]: (LE @ (f @ X0) @ (s @ (s @ (s @ 0))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_102])).
% 4.32/1.45 thf(zip_derived_cl130, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (s @ (s @ 0)) @
% 4.32/1.45 (f @ (suc @ (suc @ (suc @ (suc @ (suc @ X0)))))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl12, zip_derived_cl25])).
% 4.32/1.45 thf(clause_32, axiom,
% 4.32/1.45 (( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ A_1 ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ A_1 ) ) ) ) |
% 4.32/1.45 ( ~( E @
% 4.32/1.45 ( s @ ( s @ 0 ) ) @
% 4.32/1.45 ( f @ ( suc @ ( suc @ ( suc @ ( suc @ A_1 ) ) ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( f @ A_1 ) @ ( f @ ( suc @ ( suc @ ( suc @ A_1 ) ) ) ) ) ) |
% 4.32/1.45 ( ~( E @
% 4.32/1.45 ( s @ ( s @ 0 ) ) @
% 4.32/1.45 ( f @ ( suc @ ( suc @ ( suc @ ( suc @ ( suc @ A_1 ) ) ) ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( f @ A_1 ) @ ( f @ ( suc @ ( suc @ A_1 ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ ( suc @ ( suc @ A_1 ) ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( f @ A_1 ) @ ( f @ ( suc @ A_1 ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( f @ A_1 ) @ ( f @ ( suc @ ( suc @ ( suc @ ( suc @ A_1 ) ) ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ ( suc @ A_1 ) ) ) ) ))).
% 4.32/1.45 thf(zip_derived_cl26, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @
% 4.32/1.45 (f @ (suc @ (suc @ (suc @ (suc @ (suc @ X0)))))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0)))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_32])).
% 4.32/1.45 thf(zip_derived_cl144, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (LE @ (f @ X0) @ (s @ (s @ 0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ X0)))),
% 4.32/1.45 inference('sup-', [status(thm)], [zip_derived_cl130, zip_derived_cl26])).
% 4.32/1.45 thf(zip_derived_cl491, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('sup-', [status(thm)], [zip_derived_cl16, zip_derived_cl144])).
% 4.32/1.45 thf(zip_derived_cl505, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (LE @ (f @ X0) @ (s @ (s @ 0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0)))))),
% 4.32/1.45 inference('simplify', [status(thm)], [zip_derived_cl491])).
% 4.32/1.45 thf(zip_derived_cl743, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (LE @ (f @ X0) @ (s @ (s @ 0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('sup-', [status(thm)], [zip_derived_cl121, zip_derived_cl505])).
% 4.32/1.45 thf(zip_derived_cl754, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('simplify', [status(thm)], [zip_derived_cl743])).
% 4.32/1.45 thf(clause_2, axiom,
% 4.32/1.45 (( ~( LE @ ( f @ B ) @ ( s @ ( s @ ( s @ 0 ) ) ) ) ) |
% 4.32/1.45 ( E @ ( s @ ( s @ 0 ) ) @ ( f @ B ) ) |
% 4.32/1.45 ( LE @ ( f @ B ) @ ( s @ ( s @ 0 ) ) ))).
% 4.32/1.45 thf(zip_derived_cl14, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (LE @ (f @ X0) @ (s @ (s @ (s @ 0))))
% 4.32/1.45 | (E @ (s @ (s @ 0)) @ (f @ X0))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_2])).
% 4.32/1.45 thf(zip_derived_cl25, plain,
% 4.32/1.45 (![X0 : $i]: (LE @ (f @ X0) @ (s @ (s @ (s @ 0))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_102])).
% 4.32/1.45 thf(zip_derived_cl35, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (s @ (s @ 0)) @ (f @ X0)) | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl14, zip_derived_cl25])).
% 4.32/1.45 thf(zip_derived_cl760, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (LE @ (f @ X0) @ (s @ (s @ 0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0))))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl754, zip_derived_cl35])).
% 4.32/1.45 thf(clause_10, axiom,
% 4.32/1.45 (( ~( LE @ ( f @ ( suc @ ( suc @ B ) ) ) @ ( s @ ( s @ ( s @ 0 ) ) ) ) ) |
% 4.32/1.45 ( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ ( suc @ B ) ) ) ) |
% 4.32/1.45 ( LE @ ( f @ B ) @ ( s @ ( s @ 0 ) ) ))).
% 4.32/1.45 thf(zip_derived_cl27, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (LE @ (f @ (suc @ (suc @ X0))) @ (s @ (s @ (s @ 0))))
% 4.32/1.45 | (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_10])).
% 4.32/1.45 thf(zip_derived_cl25, plain,
% 4.32/1.45 (![X0 : $i]: (LE @ (f @ X0) @ (s @ (s @ (s @ 0))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_102])).
% 4.32/1.45 thf(zip_derived_cl61, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl27, zip_derived_cl25])).
% 4.32/1.45 thf(zip_derived_cl761, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl760, zip_derived_cl61])).
% 4.32/1.45 thf(clause_83, axiom,
% 4.32/1.45 (( ~( LE @ ( f @ ( suc @ B ) ) @ ( s @ ( s @ ( s @ 0 ) ) ) ) ) |
% 4.32/1.45 ( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ B ) ) ) |
% 4.32/1.45 ( LE @ ( f @ B ) @ ( s @ ( s @ 0 ) ) ))).
% 4.32/1.45 thf(zip_derived_cl21, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (LE @ (f @ (suc @ X0)) @ (s @ (s @ (s @ 0))))
% 4.32/1.45 | (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_83])).
% 4.32/1.45 thf(zip_derived_cl25, plain,
% 4.32/1.45 (![X0 : $i]: (LE @ (f @ X0) @ (s @ (s @ (s @ 0))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_102])).
% 4.32/1.45 thf(zip_derived_cl41, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl21, zip_derived_cl25])).
% 4.32/1.45 thf(zip_derived_cl762, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (LE @ (f @ X0) @ (s @ (s @ 0)))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0))))))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl761, zip_derived_cl41])).
% 4.32/1.45 thf(zip_derived_cl41, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl21, zip_derived_cl25])).
% 4.32/1.45 thf(clause_40, axiom,
% 4.32/1.45 (( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ A_1 ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ A_1 ) ) ) ) |
% 4.32/1.45 ( E @ ( f @ A_1 ) @ ( f @ ( suc @ A_1 ) ) ))).
% 4.32/1.45 thf(zip_derived_cl9, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ X0))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_40])).
% 4.32/1.45 thf(zip_derived_cl42, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (LE @ (f @ X0) @ (s @ (s @ 0)))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ X0)))),
% 4.32/1.45 inference('sup-', [status(thm)], [zip_derived_cl41, zip_derived_cl9])).
% 4.32/1.45 thf(zip_derived_cl35, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (s @ (s @ 0)) @ (f @ X0)) | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl14, zip_derived_cl25])).
% 4.32/1.45 thf(zip_derived_cl44, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (f @ X0) @ (f @ (suc @ X0))) | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl42, zip_derived_cl35])).
% 4.32/1.45 thf(zip_derived_cl763, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl762, zip_derived_cl44])).
% 4.32/1.45 thf(clause_50, axiom,
% 4.32/1.45 (( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ A_1 ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ A_1 ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( f @ A_1 ) @ ( f @ ( suc @ ( suc @ A_1 ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ ( suc @ ( suc @ A_1 ) ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( f @ A_1 ) @ ( f @ ( suc @ A_1 ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ ( suc @ A_1 ) ) ) ) ) |
% 4.32/1.45 ( E @ ( f @ A_1 ) @ ( f @ ( suc @ ( suc @ ( suc @ A_1 ) ) ) ) ))).
% 4.32/1.45 thf(zip_derived_cl29, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0))))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_50])).
% 4.32/1.45 thf(clause_88, axiom,
% 4.32/1.45 (( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ ( suc @ A_1 ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ A_1 ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( f @ A_1 ) @ ( f @ ( suc @ A_1 ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ ( s @ 0 ) ) @ ( f @ A_1 ) ) ) |
% 4.32/1.45 ( E @ ( f @ A_1 ) @ ( f @ ( suc @ ( suc @ A_1 ) ) ) ))).
% 4.32/1.45 thf(zip_derived_cl4, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0)))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_88])).
% 4.32/1.45 thf(zip_derived_cl9, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ X0))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_40])).
% 4.32/1.45 thf(zip_derived_cl80, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0)))))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl4, zip_derived_cl9])).
% 4.32/1.45 thf(zip_derived_cl217, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ X0)))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl29, zip_derived_cl80])).
% 4.32/1.45 thf(zip_derived_cl9, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ X0))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_40])).
% 4.32/1.45 thf(zip_derived_cl218, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0))))))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl217, zip_derived_cl9])).
% 4.32/1.45 thf(clause_76, axiom,
% 4.32/1.45 (( ~( LE @
% 4.32/1.45 ( f @ ( suc @ ( suc @ ( suc @ B ) ) ) ) @ ( s @ ( s @ ( s @ 0 ) ) ) ) ) |
% 4.32/1.45 ( E @ ( s @ ( s @ 0 ) ) @ ( f @ ( suc @ ( suc @ ( suc @ B ) ) ) ) ) |
% 4.32/1.45 ( LE @ ( f @ B ) @ ( s @ ( s @ 0 ) ) ))).
% 4.32/1.45 thf(zip_derived_cl15, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (LE @ (f @ (suc @ (suc @ (suc @ X0)))) @ (s @ (s @ (s @ 0))))
% 4.32/1.45 | (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_76])).
% 4.32/1.45 thf(zip_derived_cl25, plain,
% 4.32/1.45 (![X0 : $i]: (LE @ (f @ X0) @ (s @ (s @ (s @ 0))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_102])).
% 4.32/1.45 thf(zip_derived_cl67, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl15, zip_derived_cl25])).
% 4.32/1.45 thf(zip_derived_cl226, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('sup+', [status(thm)], [zip_derived_cl218, zip_derived_cl67])).
% 4.32/1.45 thf(zip_derived_cl61, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl27, zip_derived_cl25])).
% 4.32/1.45 thf(zip_derived_cl259, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (LE @ (f @ X0) @ (s @ (s @ 0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0))))))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl226, zip_derived_cl61])).
% 4.32/1.45 thf(zip_derived_cl35, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (s @ (s @ 0)) @ (f @ X0)) | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl14, zip_derived_cl25])).
% 4.32/1.45 thf(zip_derived_cl260, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl259, zip_derived_cl35])).
% 4.32/1.45 thf(zip_derived_cl41, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl21, zip_derived_cl25])).
% 4.32/1.45 thf(zip_derived_cl261, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (LE @ (f @ X0) @ (s @ (s @ 0)))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0))))))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl260, zip_derived_cl41])).
% 4.32/1.45 thf(zip_derived_cl764, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (LE @ (f @ X0) @ (s @ (s @ 0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0)))))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl763, zip_derived_cl261])).
% 4.32/1.45 thf(zip_derived_cl67, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl15, zip_derived_cl25])).
% 4.32/1.45 thf(zip_derived_cl765, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl764, zip_derived_cl67])).
% 4.32/1.45 thf(zip_derived_cl80, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0)))))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl4, zip_derived_cl9])).
% 4.32/1.45 thf(zip_derived_cl61, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (s @ (s @ 0)) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl27, zip_derived_cl25])).
% 4.32/1.45 thf(zip_derived_cl82, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ X0))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('sup+', [status(thm)], [zip_derived_cl80, zip_derived_cl61])).
% 4.32/1.45 thf(zip_derived_cl41, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (s @ (s @ 0)) @ (f @ (suc @ X0)))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl21, zip_derived_cl25])).
% 4.32/1.45 thf(zip_derived_cl95, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (LE @ (f @ X0) @ (s @ (s @ 0)))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ (s @ 0)) @ (f @ X0)))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl82, zip_derived_cl41])).
% 4.32/1.45 thf(zip_derived_cl35, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (s @ (s @ 0)) @ (f @ X0)) | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl14, zip_derived_cl25])).
% 4.32/1.45 thf(zip_derived_cl96, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ (s @ 0))))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl95, zip_derived_cl35])).
% 4.32/1.45 thf(zip_derived_cl766, plain, (![X0 : $i]: (LE @ (f @ X0) @ (s @ (s @ 0)))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl765, zip_derived_cl96])).
% 4.32/1.45 thf(zip_derived_cl767, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ 0)))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl7, zip_derived_cl766])).
% 4.32/1.45 thf(clause_19, axiom,
% 4.32/1.45 (( ~( E @ ( f @ A_2 ) @ ( f @ ( suc @ ( suc @ A_2 ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ A_2 ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ ( suc @ ( suc @ ( suc @ A_2 ) ) ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( f @ A_2 ) @ ( f @ ( suc @ ( suc @ ( suc @ A_2 ) ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ ( suc @ A_2 ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ ( suc @ ( suc @ A_2 ) ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( f @ A_2 ) @ ( f @ ( suc @ A_2 ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ 0 ) @ ( f @ A_2 ) ) ) |
% 4.32/1.45 ( E @ ( f @ A_2 ) @ ( f @ ( suc @ ( suc @ ( suc @ ( suc @ A_2 ) ) ) ) ) ))).
% 4.32/1.45 thf(zip_derived_cl28, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ X0))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ (suc @ X0)))))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_19])).
% 4.32/1.45 thf(clause_20, axiom,
% 4.32/1.45 (( ~( LE @
% 4.32/1.45 ( f @ ( suc @ ( suc @ ( suc @ ( suc @ ( suc @ B_0 ) ) ) ) ) ) @
% 4.32/1.45 ( s @ ( s @ 0 ) ) ) ) |
% 4.32/1.45 ( E @
% 4.32/1.45 ( s @ 0 ) @
% 4.32/1.45 ( f @ ( suc @ ( suc @ ( suc @ ( suc @ ( suc @ B_0 ) ) ) ) ) ) ) |
% 4.32/1.45 ( LE @ ( f @ B_0 ) @ ( s @ 0 ) ))).
% 4.32/1.45 thf(zip_derived_cl19, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (LE @ (f @ (suc @ (suc @ (suc @ (suc @ (suc @ X0)))))) @
% 4.32/1.45 (s @ (s @ 0)))
% 4.32/1.45 | (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ (suc @ (suc @ X0)))))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ 0)))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_20])).
% 4.32/1.45 thf(zip_derived_cl766, plain, (![X0 : $i]: (LE @ (f @ X0) @ (s @ (s @ 0)))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl765, zip_derived_cl96])).
% 4.32/1.45 thf(zip_derived_cl770, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ (suc @ (suc @ X0)))))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ 0)))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl19, zip_derived_cl766])).
% 4.32/1.45 thf(clause_35, axiom,
% 4.32/1.45 (( ~( E @ ( f @ A_2 ) @ ( f @ ( suc @ ( suc @ A_2 ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ A_2 ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ ( suc @ ( suc @ ( suc @ A_2 ) ) ) ) ) ) ) |
% 4.32/1.45 ( ~( E @
% 4.32/1.45 ( s @ 0 ) @
% 4.32/1.45 ( f @ ( suc @ ( suc @ ( suc @ ( suc @ ( suc @ A_2 ) ) ) ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( f @ A_2 ) @ ( f @ ( suc @ ( suc @ ( suc @ ( suc @ A_2 ) ) ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( f @ A_2 ) @ ( f @ ( suc @ ( suc @ ( suc @ A_2 ) ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ ( suc @ A_2 ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ ( suc @ ( suc @ A_2 ) ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( f @ A_2 ) @ ( f @ ( suc @ A_2 ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ 0 ) @ ( f @ A_2 ) ) ))).
% 4.32/1.45 thf(zip_derived_cl8, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ (suc @ (suc @ X0)))))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ X0)))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_35])).
% 4.32/1.45 thf(zip_derived_cl842, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (LE @ (f @ X0) @ (s @ 0))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ X0))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0)))))),
% 4.32/1.45 inference('sup-', [status(thm)], [zip_derived_cl770, zip_derived_cl8])).
% 4.32/1.45 thf(zip_derived_cl1192, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (s @ 0) @ (f @ X0))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ X0))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ 0)))),
% 4.32/1.45 inference('sup-', [status(thm)], [zip_derived_cl28, zip_derived_cl842])).
% 4.32/1.45 thf(zip_derived_cl1206, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (LE @ (f @ X0) @ (s @ 0))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ X0)))),
% 4.32/1.45 inference('simplify', [status(thm)], [zip_derived_cl1192])).
% 4.32/1.45 thf(zip_derived_cl1232, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (LE @ (f @ X0) @ (s @ 0))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ X0))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ 0)))),
% 4.32/1.45 inference('sup-', [status(thm)], [zip_derived_cl767, zip_derived_cl1206])).
% 4.32/1.45 thf(zip_derived_cl1252, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ X0))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ 0)))),
% 4.32/1.45 inference('simplify', [status(thm)], [zip_derived_cl1232])).
% 4.32/1.45 thf(clause_60, axiom,
% 4.32/1.45 (( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ ( suc @ A_2 ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ A_2 ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( f @ A_2 ) @ ( f @ ( suc @ A_2 ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ 0 ) @ ( f @ A_2 ) ) ) |
% 4.32/1.45 ( E @ ( f @ A_2 ) @ ( f @ ( suc @ ( suc @ A_2 ) ) ) ))).
% 4.32/1.45 thf(zip_derived_cl22, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ X0))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0)))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_60])).
% 4.32/1.45 thf(clause_41, axiom,
% 4.32/1.45 (( ~( E @ ( s @ 0 ) @ ( f @ A_2 ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ A_2 ) ) ) ) |
% 4.32/1.45 ( E @ ( f @ A_2 ) @ ( f @ ( suc @ A_2 ) ) ))).
% 4.32/1.45 thf(zip_derived_cl18, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (s @ 0) @ (f @ X0))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ X0))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_41])).
% 4.32/1.45 thf(zip_derived_cl120, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ X0))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0)))))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl22, zip_derived_cl18])).
% 4.32/1.45 thf(zip_derived_cl1301, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (LE @ (f @ X0) @ (s @ 0))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ X0))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ X0))))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl1252, zip_derived_cl120])).
% 4.32/1.45 thf(clause_39, axiom,
% 4.32/1.45 (( ~( LE @ ( f @ B_0 ) @ ( s @ ( s @ 0 ) ) ) ) |
% 4.32/1.45 ( E @ ( s @ 0 ) @ ( f @ B_0 ) ) | ( LE @ ( f @ B_0 ) @ ( s @ 0 ) ))).
% 4.32/1.45 thf(zip_derived_cl10, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (LE @ (f @ X0) @ (s @ (s @ 0)))
% 4.32/1.45 | (E @ (s @ 0) @ (f @ X0))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ 0)))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_39])).
% 4.32/1.45 thf(zip_derived_cl766, plain, (![X0 : $i]: (LE @ (f @ X0) @ (s @ (s @ 0)))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl765, zip_derived_cl96])).
% 4.32/1.45 thf(zip_derived_cl768, plain,
% 4.32/1.45 (![X0 : $i]: ( (E @ (s @ 0) @ (f @ X0)) | (LE @ (f @ X0) @ (s @ 0)))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl10, zip_derived_cl766])).
% 4.32/1.45 thf(zip_derived_cl1302, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ 0)))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl1301, zip_derived_cl768])).
% 4.32/1.45 thf(clause_3, axiom,
% 4.32/1.45 (( ~( LE @ ( f @ ( suc @ B_0 ) ) @ ( s @ ( s @ 0 ) ) ) ) |
% 4.32/1.45 ( E @ ( s @ 0 ) @ ( f @ ( suc @ B_0 ) ) ) |
% 4.32/1.45 ( LE @ ( f @ B_0 ) @ ( s @ 0 ) ))).
% 4.32/1.45 thf(zip_derived_cl24, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (LE @ (f @ (suc @ X0)) @ (s @ (s @ 0)))
% 4.32/1.45 | (E @ (s @ 0) @ (f @ (suc @ X0)))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ 0)))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_3])).
% 4.32/1.45 thf(zip_derived_cl766, plain, (![X0 : $i]: (LE @ (f @ X0) @ (s @ (s @ 0)))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl765, zip_derived_cl96])).
% 4.32/1.45 thf(zip_derived_cl772, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (s @ 0) @ (f @ (suc @ X0))) | (LE @ (f @ X0) @ (s @ 0)))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl24, zip_derived_cl766])).
% 4.32/1.45 thf(zip_derived_cl1303, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (LE @ (f @ X0) @ (s @ 0))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0))))))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl1302, zip_derived_cl772])).
% 4.32/1.45 thf(zip_derived_cl772, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (s @ 0) @ (f @ (suc @ X0))) | (LE @ (f @ X0) @ (s @ 0)))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl24, zip_derived_cl766])).
% 4.32/1.45 thf(zip_derived_cl18, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (s @ 0) @ (f @ X0))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ X0))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_41])).
% 4.32/1.45 thf(zip_derived_cl780, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (LE @ (f @ X0) @ (s @ 0))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ X0)))),
% 4.32/1.45 inference('sup-', [status(thm)], [zip_derived_cl772, zip_derived_cl18])).
% 4.32/1.45 thf(zip_derived_cl768, plain,
% 4.32/1.45 (![X0 : $i]: ( (E @ (s @ 0) @ (f @ X0)) | (LE @ (f @ X0) @ (s @ 0)))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl10, zip_derived_cl766])).
% 4.32/1.45 thf(zip_derived_cl788, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (f @ X0) @ (f @ (suc @ X0))) | (LE @ (f @ X0) @ (s @ 0)))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl780, zip_derived_cl768])).
% 4.32/1.45 thf(zip_derived_cl1304, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ 0)))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl1303, zip_derived_cl788])).
% 4.32/1.45 thf(clause_56, axiom,
% 4.32/1.45 (( ~( LE @ ( f @ ( suc @ ( suc @ ( suc @ B_0 ) ) ) ) @ ( s @ ( s @ 0 ) ) ) ) |
% 4.32/1.45 ( E @ ( s @ 0 ) @ ( f @ ( suc @ ( suc @ ( suc @ B_0 ) ) ) ) ) |
% 4.32/1.45 ( LE @ ( f @ B_0 ) @ ( s @ 0 ) ))).
% 4.32/1.45 thf(zip_derived_cl23, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (LE @ (f @ (suc @ (suc @ (suc @ X0)))) @ (s @ (s @ 0)))
% 4.32/1.45 | (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ 0)))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_56])).
% 4.32/1.45 thf(zip_derived_cl766, plain, (![X0 : $i]: (LE @ (f @ X0) @ (s @ (s @ 0)))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl765, zip_derived_cl96])).
% 4.32/1.45 thf(zip_derived_cl771, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ 0)))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl23, zip_derived_cl766])).
% 4.32/1.45 thf(clause_53, axiom,
% 4.32/1.45 (( ~( E @ ( f @ A_2 ) @ ( f @ ( suc @ ( suc @ A_2 ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ A_2 ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ ( suc @ A_2 ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ 0 ) @ ( f @ ( suc @ ( suc @ ( suc @ A_2 ) ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( f @ A_2 ) @ ( f @ ( suc @ A_2 ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( s @ 0 ) @ ( f @ A_2 ) ) ) |
% 4.32/1.45 ( E @ ( f @ A_2 ) @ ( f @ ( suc @ ( suc @ ( suc @ A_2 ) ) ) ) ))).
% 4.32/1.45 thf(zip_derived_cl13, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ X0))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0))))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_53])).
% 4.32/1.45 thf(zip_derived_cl120, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ X0))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0)))))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl22, zip_derived_cl18])).
% 4.32/1.45 thf(zip_derived_cl147, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ X0))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ X0))))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl13, zip_derived_cl120])).
% 4.32/1.45 thf(zip_derived_cl18, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (s @ 0) @ (f @ X0))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ X0))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_41])).
% 4.32/1.45 thf(zip_derived_cl148, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ X0))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0))))))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl147, zip_derived_cl18])).
% 4.32/1.45 thf(zip_derived_cl807, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (LE @ (f @ X0) @ (s @ 0))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ X0))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ X0))))),
% 4.32/1.45 inference('sup-', [status(thm)], [zip_derived_cl771, zip_derived_cl148])).
% 4.32/1.45 thf(zip_derived_cl768, plain,
% 4.32/1.45 (![X0 : $i]: ( (E @ (s @ 0) @ (f @ X0)) | (LE @ (f @ X0) @ (s @ 0)))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl10, zip_derived_cl766])).
% 4.32/1.45 thf(zip_derived_cl881, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (s @ 0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ 0)))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl807, zip_derived_cl768])).
% 4.32/1.45 thf(zip_derived_cl772, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (s @ 0) @ (f @ (suc @ X0))) | (LE @ (f @ X0) @ (s @ 0)))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl24, zip_derived_cl766])).
% 4.32/1.45 thf(zip_derived_cl882, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (LE @ (f @ X0) @ (s @ 0))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0)))))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl881, zip_derived_cl772])).
% 4.32/1.45 thf(clause_87, axiom,
% 4.32/1.45 (( ~( LE @ ( f @ ( suc @ ( suc @ B_0 ) ) ) @ ( s @ ( s @ 0 ) ) ) ) |
% 4.32/1.45 ( E @ ( s @ 0 ) @ ( f @ ( suc @ ( suc @ B_0 ) ) ) ) |
% 4.32/1.45 ( LE @ ( f @ B_0 ) @ ( s @ 0 ) ))).
% 4.32/1.45 thf(zip_derived_cl17, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (LE @ (f @ (suc @ (suc @ X0))) @ (s @ (s @ 0)))
% 4.32/1.45 | (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ 0)))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_87])).
% 4.32/1.45 thf(zip_derived_cl766, plain, (![X0 : $i]: (LE @ (f @ X0) @ (s @ (s @ 0)))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl765, zip_derived_cl96])).
% 4.32/1.45 thf(zip_derived_cl769, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ 0)))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl17, zip_derived_cl766])).
% 4.32/1.45 thf(zip_derived_cl883, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ 0)))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl882, zip_derived_cl769])).
% 4.32/1.45 thf(zip_derived_cl1305, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (LE @ (f @ X0) @ (s @ 0))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0)))))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl1304, zip_derived_cl883])).
% 4.32/1.45 thf(zip_derived_cl771, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (s @ 0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ 0)))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl23, zip_derived_cl766])).
% 4.32/1.45 thf(zip_derived_cl1306, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ 0)))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl1305, zip_derived_cl771])).
% 4.32/1.45 thf(zip_derived_cl769, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (s @ 0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | (LE @ (f @ X0) @ (s @ 0)))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl17, zip_derived_cl766])).
% 4.32/1.45 thf(zip_derived_cl1307, plain, (![X0 : $i]: (LE @ (f @ X0) @ (s @ 0))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl1306, zip_derived_cl769])).
% 4.32/1.45 thf(zip_derived_cl1311, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | (LE @ (f @ X0) @ 0))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl5, zip_derived_cl1307])).
% 4.32/1.45 thf(clause_18, axiom,
% 4.32/1.45 (( ~( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ ( suc @ A_3 ) ) ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( f @ A_3 ) @ ( f @ ( suc @ ( suc @ A_3 ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ A_3 ) ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ 0 @ ( f @ A_3 ) ) ) |
% 4.32/1.45 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ A_3 ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ 0 @ ( f @ ( suc @ A_3 ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( f @ A_3 ) @ ( f @ ( suc @ A_3 ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( f @ A_3 ) @ ( f @ ( suc @ ( suc @ ( suc @ A_3 ) ) ) ) ) ) |
% 4.32/1.45 ( E @ ( f @ A_3 ) @ ( f @ ( suc @ ( suc @ ( suc @ ( suc @ A_3 ) ) ) ) ) ))).
% 4.32/1.45 thf(zip_derived_cl6, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ X0))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ (suc @ X0)))))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_18])).
% 4.32/1.45 thf(clause_5, axiom,
% 4.32/1.45 (( ~( LE @
% 4.32/1.45 ( f @ ( suc @ ( suc @ ( suc @ ( suc @ ( suc @ B_1 ) ) ) ) ) ) @
% 4.32/1.45 ( s @ 0 ) ) ) |
% 4.32/1.45 ( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ ( suc @ ( suc @ B_1 ) ) ) ) ) ) ) |
% 4.32/1.45 ( LE @ ( f @ B_1 ) @ 0 ))).
% 4.32/1.45 thf(zip_derived_cl20, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (LE @ (f @ (suc @ (suc @ (suc @ (suc @ (suc @ X0)))))) @ (s @ 0))
% 4.32/1.45 | (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ (suc @ X0)))))))
% 4.32/1.45 | (LE @ (f @ X0) @ 0))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_5])).
% 4.32/1.45 thf(zip_derived_cl1307, plain, (![X0 : $i]: (LE @ (f @ X0) @ (s @ 0))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl1306, zip_derived_cl769])).
% 4.32/1.45 thf(zip_derived_cl1312, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ (suc @ X0)))))))
% 4.32/1.45 | (LE @ (f @ X0) @ 0))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl20, zip_derived_cl1307])).
% 4.32/1.45 thf(clause_31, axiom,
% 4.32/1.45 (( ~( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ ( suc @ A_3 ) ) ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( f @ A_3 ) @ ( f @ ( suc @ ( suc @ A_3 ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ ( suc @ ( suc @ A_3 ) ) ) ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ A_3 ) ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ 0 @ ( f @ A_3 ) ) ) |
% 4.32/1.45 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ A_3 ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ 0 @ ( f @ ( suc @ A_3 ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( f @ A_3 ) @ ( f @ ( suc @ A_3 ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( f @ A_3 ) @ ( f @ ( suc @ ( suc @ ( suc @ ( suc @ A_3 ) ) ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( f @ A_3 ) @ ( f @ ( suc @ ( suc @ ( suc @ A_3 ) ) ) ) ) ))).
% 4.32/1.45 thf(zip_derived_cl0, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ (suc @ X0)))))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ X0))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0))))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_31])).
% 4.32/1.45 thf(zip_derived_cl1319, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (LE @ (f @ X0) @ 0)
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ X0))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X0)))))))),
% 4.32/1.45 inference('sup-', [status(thm)], [zip_derived_cl1312, zip_derived_cl0])).
% 4.32/1.45 thf(zip_derived_cl1371, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ X0))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ X0))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | (LE @ (f @ X0) @ 0))),
% 4.32/1.45 inference('sup-', [status(thm)], [zip_derived_cl6, zip_derived_cl1319])).
% 4.32/1.45 thf(zip_derived_cl1374, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (LE @ (f @ X0) @ 0)
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ X0))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0))))))),
% 4.32/1.45 inference('simplify', [status(thm)], [zip_derived_cl1371])).
% 4.32/1.45 thf(zip_derived_cl1387, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (LE @ (f @ X0) @ 0)
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ X0))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | (LE @ (f @ X0) @ 0))),
% 4.32/1.45 inference('sup-', [status(thm)], [zip_derived_cl1311, zip_derived_cl1374])).
% 4.32/1.45 thf(zip_derived_cl1394, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ X0))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | (LE @ (f @ X0) @ 0))),
% 4.32/1.45 inference('simplify', [status(thm)], [zip_derived_cl1387])).
% 4.32/1.45 thf(clause_45, axiom,
% 4.32/1.45 (( ~( E @ 0 @ ( f @ ( suc @ ( suc @ A_3 ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ 0 @ ( f @ ( suc @ A_3 ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( f @ A_3 ) @ ( f @ ( suc @ A_3 ) ) ) ) |
% 4.32/1.45 ( ~( E @ 0 @ ( f @ A_3 ) ) ) |
% 4.32/1.45 ( E @ ( f @ A_3 ) @ ( f @ ( suc @ ( suc @ A_3 ) ) ) ))).
% 4.32/1.45 thf(zip_derived_cl11, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ 0 @ (f @ X0))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0)))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_45])).
% 4.32/1.45 thf(clause_43, axiom,
% 4.32/1.45 (( ~( E @ 0 @ ( f @ A_3 ) ) ) | ( ~( E @ 0 @ ( f @ ( suc @ A_3 ) ) ) ) |
% 4.32/1.45 ( E @ ( f @ A_3 ) @ ( f @ ( suc @ A_3 ) ) ))).
% 4.32/1.45 thf(zip_derived_cl31, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ 0 @ (f @ X0))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ X0))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_43])).
% 4.32/1.45 thf(zip_derived_cl60, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ X0))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0)))))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl11, zip_derived_cl31])).
% 4.32/1.45 thf(zip_derived_cl1398, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (LE @ (f @ X0) @ 0)
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ X0))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0))))))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl1394, zip_derived_cl60])).
% 4.32/1.45 thf(clause_59, axiom,
% 4.32/1.45 (( ~( E @ ( f @ A_3 ) @ ( f @ ( suc @ ( suc @ A_3 ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ A_3 ) ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ 0 @ ( f @ A_3 ) ) ) |
% 4.32/1.45 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ A_3 ) ) ) ) ) |
% 4.32/1.45 ( ~( E @ 0 @ ( f @ ( suc @ A_3 ) ) ) ) |
% 4.32/1.45 ( ~( E @ ( f @ A_3 ) @ ( f @ ( suc @ A_3 ) ) ) ) |
% 4.32/1.45 ( E @ ( f @ A_3 ) @ ( f @ ( suc @ ( suc @ ( suc @ A_3 ) ) ) ) ))).
% 4.32/1.45 thf(zip_derived_cl30, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ X0))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0))))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_59])).
% 4.32/1.45 thf(zip_derived_cl60, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ X0))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0)))))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl11, zip_derived_cl31])).
% 4.32/1.45 thf(zip_derived_cl137, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ X0))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0))))))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl30, zip_derived_cl60])).
% 4.32/1.45 thf(zip_derived_cl31, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ 0 @ (f @ X0))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ X0))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_43])).
% 4.32/1.45 thf(zip_derived_cl138, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ X0))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0))))))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl137, zip_derived_cl31])).
% 4.32/1.45 thf(zip_derived_cl1399, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ X0))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | (LE @ (f @ X0) @ 0))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl1398, zip_derived_cl138])).
% 4.32/1.45 thf(clause_82, axiom,
% 4.32/1.45 (( ~( LE @ ( f @ ( suc @ ( suc @ ( suc @ B_1 ) ) ) ) @ ( s @ 0 ) ) ) |
% 4.32/1.45 ( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ B_1 ) ) ) ) ) |
% 4.32/1.45 ( LE @ ( f @ B_1 ) @ 0 ))).
% 4.32/1.45 thf(zip_derived_cl33, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (LE @ (f @ (suc @ (suc @ (suc @ X0)))) @ (s @ 0))
% 4.32/1.45 | (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 4.32/1.45 | (LE @ (f @ X0) @ 0))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_82])).
% 4.32/1.45 thf(zip_derived_cl1307, plain, (![X0 : $i]: (LE @ (f @ X0) @ (s @ 0))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl1306, zip_derived_cl769])).
% 4.32/1.45 thf(zip_derived_cl1313, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0))))) | (LE @ (f @ X0) @ 0))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl33, zip_derived_cl1307])).
% 4.32/1.45 thf(zip_derived_cl1400, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (LE @ (f @ X0) @ 0)
% 4.32/1.45 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ X0)))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl1399, zip_derived_cl1313])).
% 4.32/1.45 thf(zip_derived_cl31, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ 0 @ (f @ X0))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 4.32/1.45 | (E @ (f @ X0) @ (f @ (suc @ X0))))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_43])).
% 4.32/1.45 thf(zip_derived_cl1401, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ 0 @ (f @ X0))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 4.32/1.45 | (LE @ (f @ X0) @ 0))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl1400, zip_derived_cl31])).
% 4.32/1.45 thf(clause_27, axiom,
% 4.32/1.45 (( ~( LE @ ( f @ B_1 ) @ ( s @ 0 ) ) ) | ( E @ 0 @ ( f @ B_1 ) ) |
% 4.32/1.45 ( LE @ ( f @ B_1 ) @ 0 ))).
% 4.32/1.45 thf(zip_derived_cl2, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (LE @ (f @ X0) @ (s @ 0))
% 4.32/1.45 | (E @ 0 @ (f @ X0))
% 4.32/1.45 | (LE @ (f @ X0) @ 0))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_27])).
% 4.32/1.45 thf(zip_derived_cl1307, plain, (![X0 : $i]: (LE @ (f @ X0) @ (s @ 0))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl1306, zip_derived_cl769])).
% 4.32/1.45 thf(zip_derived_cl1309, plain,
% 4.32/1.45 (![X0 : $i]: ( (E @ 0 @ (f @ X0)) | (LE @ (f @ X0) @ 0))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl2, zip_derived_cl1307])).
% 4.32/1.45 thf(zip_derived_cl1402, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 ( (LE @ (f @ X0) @ 0)
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 4.32/1.45 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0)))))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl1401, zip_derived_cl1309])).
% 4.32/1.45 thf(clause_101, axiom,
% 4.32/1.45 (( ~( LE @ ( f @ ( suc @ B_1 ) ) @ ( s @ 0 ) ) ) |
% 4.32/1.45 ( E @ 0 @ ( f @ ( suc @ B_1 ) ) ) | ( LE @ ( f @ B_1 ) @ 0 ))).
% 4.32/1.45 thf(zip_derived_cl1, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (LE @ (f @ (suc @ X0)) @ (s @ 0))
% 4.32/1.45 | (E @ 0 @ (f @ (suc @ X0)))
% 4.32/1.45 | (LE @ (f @ X0) @ 0))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_101])).
% 4.32/1.45 thf(zip_derived_cl1307, plain, (![X0 : $i]: (LE @ (f @ X0) @ (s @ 0))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl1306, zip_derived_cl769])).
% 4.32/1.45 thf(zip_derived_cl1308, plain,
% 4.32/1.45 (![X0 : $i]: ( (E @ 0 @ (f @ (suc @ X0))) | (LE @ (f @ X0) @ 0))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl1, zip_derived_cl1307])).
% 4.32/1.45 thf(zip_derived_cl1403, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (E @ 0 @ (f @ (suc @ (suc @ X0)))) | (LE @ (f @ X0) @ 0))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl1402, zip_derived_cl1308])).
% 4.32/1.45 thf(clause_37, axiom,
% 4.32/1.45 (( ~( LE @ ( f @ ( suc @ ( suc @ B_1 ) ) ) @ ( s @ 0 ) ) ) |
% 4.32/1.45 ( E @ 0 @ ( f @ ( suc @ ( suc @ B_1 ) ) ) ) | ( LE @ ( f @ B_1 ) @ 0 ))).
% 4.32/1.45 thf(zip_derived_cl3, plain,
% 4.32/1.45 (![X0 : $i]:
% 4.32/1.45 (~ (LE @ (f @ (suc @ (suc @ X0))) @ (s @ 0))
% 4.32/1.45 | (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 4.32/1.45 | (LE @ (f @ X0) @ 0))),
% 4.32/1.45 inference('cnf', [status(esa)], [clause_37])).
% 4.32/1.45 thf(zip_derived_cl1307, plain, (![X0 : $i]: (LE @ (f @ X0) @ (s @ 0))),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl1306, zip_derived_cl769])).
% 4.32/1.45 thf(zip_derived_cl1310, plain,
% 4.32/1.45 (![X0 : $i]: ( (E @ 0 @ (f @ (suc @ (suc @ X0)))) | (LE @ (f @ X0) @ 0))),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl3, zip_derived_cl1307])).
% 4.32/1.45 thf(zip_derived_cl1404, plain, (![X0 : $i]: (LE @ (f @ X0) @ 0)),
% 4.32/1.45 inference('clc', [status(thm)], [zip_derived_cl1403, zip_derived_cl1310])).
% 4.32/1.45 thf(zip_derived_cl1405, plain, ($false),
% 4.32/1.45 inference('demod', [status(thm)], [zip_derived_cl34, zip_derived_cl1404])).
% 4.32/1.45
% 4.32/1.45 % SZS output end Refutation
% 4.32/1.45
% 4.32/1.45
% 4.32/1.45 % Terminating...
% 5.25/1.56 % Runner terminated.
% 5.25/1.57 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------