%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : SYO654-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.X1deEnLBfx true
% Computer : n006.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:05 PM UTC 2025
% Result : Unsatisfiable 48.05s 13.03s
% Output : Refutation 48.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.20 % Problem : SYO654-1 : TPTP v9.2.0. Released v7.3.0.
% 0.11/0.23 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.X1deEnLBfx true
% 0.11/0.43 % Computer : n006.cluster.edu
% 0.11/0.43 % Model : x86_64 x86_64
% 0.11/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.43 % Memory : 8042.1875MB
% 0.11/0.43 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.43 % CPULimit : 300
% 0.11/0.43 % WCLimit : 300
% 0.11/0.43 % DateTime : Wed Oct 1 18:13:53 EDT 2025
% 0.11/0.43 % CPUTime :
% 0.11/0.43 % Running portfolio for 300 s
% 0.11/0.43 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.43 % Number of cores: 8
% 0.11/0.44 % Python version: Python 3.6.8
% 0.11/0.44 % Running in FO mode
% 0.26/0.70 % Total configuration time : 435
% 0.26/0.70 % Estimated wc time : 1092
% 0.26/0.70 % Estimated cpu time (7 cpus) : 156.0
% 0.26/0.84 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.26/0.84 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.26/0.84 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.26/0.85 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.26/0.85 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.26/0.85 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 0.26/0.85 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 1.89/1.26 % /export/starexec/sandbox/solver/bin/fo/fo1_lcnf.sh running for 50s
% 1.98/1.30 % /export/starexec/sandbox/solver/bin/fo/fo17_bce.sh running for 50s
% 1.98/1.32 % /export/starexec/sandbox/solver/bin/fo/fo8.sh running for 50s
% 48.05/13.03 % Solved by fo/fo17_bce.sh.
% 48.05/13.03 % BCE start: 267
% 48.05/13.03 % BCE eliminated: 0
% 48.05/13.03 % PE start: 267
% 48.05/13.03 logic: neq
% 48.05/13.03 % PE eliminated: 0
% 48.05/13.03 % done 639 iterations in 11.603s
% 48.05/13.03 % SZS status Unsatisfiable for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 48.05/13.03 % SZS output start Refutation
% 48.05/13.03 thf(0_type, type, 0: $i).
% 48.05/13.03 thf(suc_type, type, suc: $i > $i).
% 48.05/13.03 thf(LE_type, type, LE: $i > $i > $o).
% 48.05/13.03 thf(f_type, type, f: $i > $i).
% 48.05/13.03 thf(s_type, type, s: $i > $i).
% 48.05/13.03 thf(iLEQ_type, type, iLEQ: $i > $i > $o).
% 48.05/13.03 thf(z_type, type, z: $i).
% 48.05/13.03 thf(E_type, type, E: $i > $i > $o).
% 48.05/13.03 thf(clause_20481, axiom, (~( LE @ ( f @ z ) @ 0 ))).
% 48.05/13.03 thf(zip_derived_cl10, plain, (~ (LE @ (f @ z) @ 0)),
% 48.05/13.03 inference('cnf', [status(esa)], [clause_20481])).
% 48.05/13.03 thf(clause_33306, axiom,
% 48.05/13.03 (( ~( LE @ ( f @ ( suc @ ( suc @ ( suc @ ( suc @ B_10 ) ) ) ) ) @ ( s @ 0 ) ) ) |
% 48.05/13.03 ( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ ( suc @ B_10 ) ) ) ) ) ) |
% 48.05/13.03 ( LE @ ( f @ B_10 ) @ 0 ))).
% 48.05/13.03 thf(zip_derived_cl27, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 (~ (LE @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))) @ (s @ 0))
% 48.05/13.03 | (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 48.05/13.03 | (LE @ (f @ X0) @ 0))),
% 48.05/13.03 inference('cnf', [status(esa)], [clause_33306])).
% 48.05/13.03 thf(clause_39108, axiom, (LE @ ( f @ A ) @ ( s @ 0 ))).
% 48.05/13.03 thf(zip_derived_cl64, plain, (![X0 : $i]: (LE @ (f @ X0) @ (s @ 0))),
% 48.05/13.03 inference('cnf', [status(esa)], [clause_39108])).
% 48.05/13.03 thf(zip_derived_cl297, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 ( (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 48.05/13.03 | (LE @ (f @ X0) @ 0))),
% 48.05/13.03 inference('demod', [status(thm)], [zip_derived_cl27, zip_derived_cl64])).
% 48.05/13.03 thf(clause_42473, axiom,
% 48.05/13.03 (( ~( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ A_1 ) ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ A_1 ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ A_1 ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ A_1 ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ A_1 ) @ ( f @ ( suc @ ( suc @ A_1 ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ A_1 ) @ ( f @ ( suc @ A_1 ) ) ) ) |
% 48.05/13.03 ( E @ ( f @ A_1 ) @ ( f @ ( suc @ ( suc @ ( suc @ A_1 ) ) ) ) ) |
% 48.05/13.03 ( iLEQ @ ( suc @ A_1 ) @ ( suc @ A_1 ) ))).
% 48.05/13.03 thf(zip_derived_cl234, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 (~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 48.05/13.03 inference('cnf', [status(esa)], [clause_42473])).
% 48.05/13.03 thf(clause_33398, axiom,
% 48.05/13.03 (( ~( E @ 0 @ ( f @ ( suc @ ( suc @ A_1 ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ A_1 ) ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ A_1 ) @ ( f @ ( suc @ A_1 ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ A_1 ) ) ) |
% 48.05/13.03 ( E @ ( f @ A_1 ) @ ( f @ ( suc @ ( suc @ A_1 ) ) ) ) |
% 48.05/13.03 ( iLEQ @ ( suc @ A_1 ) @ ( suc @ A_1 ) ))).
% 48.05/13.03 thf(zip_derived_cl195, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 (~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 48.05/13.03 inference('cnf', [status(esa)], [clause_33398])).
% 48.05/13.03 thf(clause_6843, axiom,
% 48.05/13.03 (( ~( E @ 0 @ ( f @ A_1 ) ) ) | ( ~( E @ 0 @ ( f @ ( suc @ A_1 ) ) ) ) |
% 48.05/13.03 ( E @ ( f @ A_1 ) @ ( f @ ( suc @ A_1 ) ) ) |
% 48.05/13.03 ( iLEQ @ ( suc @ A_1 ) @ ( suc @ A_1 ) ))).
% 48.05/13.03 thf(zip_derived_cl71, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 (~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 48.05/13.03 inference('cnf', [status(esa)], [clause_6843])).
% 48.05/13.03 thf(zip_derived_cl312, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 ( (iLEQ @ (suc @ X0) @ (suc @ X0))
% 48.05/13.03 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0)))))),
% 48.05/13.03 inference('clc', [status(thm)], [zip_derived_cl195, zip_derived_cl71])).
% 48.05/13.03 thf(zip_derived_cl317, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 ( (iLEQ @ (suc @ X0) @ (suc @ X0))
% 48.05/13.03 | (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0))))))),
% 48.05/13.03 inference('clc', [status(thm)], [zip_derived_cl234, zip_derived_cl312])).
% 48.05/13.03 thf(zip_derived_cl71, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 (~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 48.05/13.03 inference('cnf', [status(esa)], [clause_6843])).
% 48.05/13.03 thf(zip_derived_cl318, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 (~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 48.05/13.03 inference('clc', [status(thm)], [zip_derived_cl317, zip_derived_cl71])).
% 48.05/13.03 thf(clause_19660, axiom,
% 48.05/13.03 (( ~( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ A_1 ) ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ A_1 ) ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ A_1 ) @ ( f @ ( suc @ ( suc @ ( suc @ A_1 ) ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ A_1 ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ A_1 ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ A_1 ) @ ( f @ ( suc @ ( suc @ A_1 ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ A_1 ) @ ( f @ ( suc @ A_1 ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ ( suc @ A_1 ) ) ) ) ) ) ) |
% 48.05/13.03 ( iLEQ @ ( suc @ A_1 ) @ ( suc @ A_1 ) ))).
% 48.05/13.03 thf(zip_derived_cl258, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 (~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 48.05/13.03 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 48.05/13.03 inference('cnf', [status(esa)], [clause_19660])).
% 48.05/13.03 thf(zip_derived_cl325, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 ( (iLEQ @ (suc @ X0) @ (suc @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 48.05/13.03 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl318, zip_derived_cl258])).
% 48.05/13.03 thf(zip_derived_cl336, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 (~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 48.05/13.03 inference('simplify', [status(thm)], [zip_derived_cl325])).
% 48.05/13.03 thf(zip_derived_cl71, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 (~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 48.05/13.03 inference('cnf', [status(esa)], [clause_6843])).
% 48.05/13.03 thf(zip_derived_cl341, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 ( (iLEQ @ (suc @ X0) @ (suc @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X0)))))))),
% 48.05/13.03 inference('clc', [status(thm)], [zip_derived_cl336, zip_derived_cl71])).
% 48.05/13.03 thf(zip_derived_cl312, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 ( (iLEQ @ (suc @ X0) @ (suc @ X0))
% 48.05/13.03 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0)))))),
% 48.05/13.03 inference('clc', [status(thm)], [zip_derived_cl195, zip_derived_cl71])).
% 48.05/13.03 thf(zip_derived_cl342, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 (~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 48.05/13.03 inference('clc', [status(thm)], [zip_derived_cl341, zip_derived_cl312])).
% 48.05/13.03 thf(zip_derived_cl343, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 ( (LE @ (f @ X0) @ 0)
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl297, zip_derived_cl342])).
% 48.05/13.03 thf(clause_29553, axiom,
% 48.05/13.03 (( ~( LE @ ( f @ ( suc @ ( suc @ ( suc @ B_10 ) ) ) ) @ ( s @ 0 ) ) ) |
% 48.05/13.03 ( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ B_10 ) ) ) ) ) |
% 48.05/13.03 ( LE @ ( f @ B_10 ) @ 0 ))).
% 48.05/13.03 thf(zip_derived_cl183, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 (~ (LE @ (f @ (suc @ (suc @ (suc @ X0)))) @ (s @ 0))
% 48.05/13.03 | (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | (LE @ (f @ X0) @ 0))),
% 48.05/13.03 inference('cnf', [status(esa)], [clause_29553])).
% 48.05/13.03 thf(zip_derived_cl64, plain, (![X0 : $i]: (LE @ (f @ X0) @ (s @ 0))),
% 48.05/13.03 inference('cnf', [status(esa)], [clause_39108])).
% 48.05/13.03 thf(zip_derived_cl291, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 ( (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0))))) | (LE @ (f @ X0) @ 0))),
% 48.05/13.03 inference('demod', [status(thm)], [zip_derived_cl183, zip_derived_cl64])).
% 48.05/13.03 thf(zip_derived_cl344, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 ( (iLEQ @ (suc @ X0) @ (suc @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | (LE @ (f @ X0) @ 0))),
% 48.05/13.03 inference('clc', [status(thm)], [zip_derived_cl343, zip_derived_cl291])).
% 48.05/13.03 thf(clause_2640, axiom,
% 48.05/13.03 (( ~( LE @ ( f @ B_10 ) @ ( s @ 0 ) ) ) | ( E @ 0 @ ( f @ B_10 ) ) |
% 48.05/13.03 ( LE @ ( f @ B_10 ) @ 0 ))).
% 48.05/13.03 thf(zip_derived_cl87, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 (~ (LE @ (f @ X0) @ (s @ 0))
% 48.05/13.03 | (E @ 0 @ (f @ X0))
% 48.05/13.03 | (LE @ (f @ X0) @ 0))),
% 48.05/13.03 inference('cnf', [status(esa)], [clause_2640])).
% 48.05/13.03 thf(zip_derived_cl64, plain, (![X0 : $i]: (LE @ (f @ X0) @ (s @ 0))),
% 48.05/13.03 inference('cnf', [status(esa)], [clause_39108])).
% 48.05/13.03 thf(zip_derived_cl267, plain,
% 48.05/13.03 (![X0 : $i]: ( (E @ 0 @ (f @ X0)) | (LE @ (f @ X0) @ 0))),
% 48.05/13.03 inference('demod', [status(thm)], [zip_derived_cl87, zip_derived_cl64])).
% 48.05/13.03 thf(zip_derived_cl345, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 ( (LE @ (f @ X0) @ 0)
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 48.05/13.03 inference('clc', [status(thm)], [zip_derived_cl344, zip_derived_cl267])).
% 48.05/13.03 thf(clause_37984, axiom,
% 48.05/13.03 (( ~( LE @ ( f @ ( suc @ B_10 ) ) @ ( s @ 0 ) ) ) |
% 48.05/13.03 ( E @ 0 @ ( f @ ( suc @ B_10 ) ) ) | ( LE @ ( f @ B_10 ) @ 0 ))).
% 48.05/13.03 thf(zip_derived_cl230, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 (~ (LE @ (f @ (suc @ X0)) @ (s @ 0))
% 48.05/13.03 | (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | (LE @ (f @ X0) @ 0))),
% 48.05/13.03 inference('cnf', [status(esa)], [clause_37984])).
% 48.05/13.03 thf(zip_derived_cl64, plain, (![X0 : $i]: (LE @ (f @ X0) @ (s @ 0))),
% 48.05/13.03 inference('cnf', [status(esa)], [clause_39108])).
% 48.05/13.03 thf(zip_derived_cl279, plain,
% 48.05/13.03 (![X0 : $i]: ( (E @ 0 @ (f @ (suc @ X0))) | (LE @ (f @ X0) @ 0))),
% 48.05/13.03 inference('demod', [status(thm)], [zip_derived_cl230, zip_derived_cl64])).
% 48.05/13.03 thf(zip_derived_cl346, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 ( (iLEQ @ (suc @ X0) @ (suc @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | (LE @ (f @ X0) @ 0))),
% 48.05/13.03 inference('clc', [status(thm)], [zip_derived_cl345, zip_derived_cl279])).
% 48.05/13.03 thf(clause_828, axiom,
% 48.05/13.03 (( ~( LE @ ( f @ ( suc @ ( suc @ B_10 ) ) ) @ ( s @ 0 ) ) ) |
% 48.05/13.03 ( E @ 0 @ ( f @ ( suc @ ( suc @ B_10 ) ) ) ) | ( LE @ ( f @ B_10 ) @ 0 ))).
% 48.05/13.03 thf(zip_derived_cl242, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 (~ (LE @ (f @ (suc @ (suc @ X0))) @ (s @ 0))
% 48.05/13.03 | (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | (LE @ (f @ X0) @ 0))),
% 48.05/13.03 inference('cnf', [status(esa)], [clause_828])).
% 48.05/13.03 thf(zip_derived_cl64, plain, (![X0 : $i]: (LE @ (f @ X0) @ (s @ 0))),
% 48.05/13.03 inference('cnf', [status(esa)], [clause_39108])).
% 48.05/13.03 thf(zip_derived_cl287, plain,
% 48.05/13.03 (![X0 : $i]: ( (E @ 0 @ (f @ (suc @ (suc @ X0)))) | (LE @ (f @ X0) @ 0))),
% 48.05/13.03 inference('demod', [status(thm)], [zip_derived_cl242, zip_derived_cl64])).
% 48.05/13.03 thf(zip_derived_cl347, plain,
% 48.05/13.03 (![X0 : $i]: ( (LE @ (f @ X0) @ 0) | (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 48.05/13.03 inference('clc', [status(thm)], [zip_derived_cl346, zip_derived_cl287])).
% 48.05/13.03 thf(zip_derived_cl10, plain, (~ (LE @ (f @ z) @ 0)),
% 48.05/13.03 inference('cnf', [status(esa)], [clause_20481])).
% 48.05/13.03 thf(zip_derived_cl348, plain, ( (iLEQ @ (suc @ z) @ (suc @ z))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl347, zip_derived_cl10])).
% 48.05/13.03 thf(clause_4416, axiom,
% 48.05/13.03 (( ~( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ A_1 ) ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ B_11 ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ B_11 ) ) ) ) ) ) |
% 48.05/13.03 ( ~( iLEQ @ ( suc @ B_12 ) @ ( suc @ B_13 ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ B_11 ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ A_1 ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ A_1 ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ B_11 ) ) ) | ( ~( E @ 0 @ ( f @ A_1 ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ B_13 ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ B_11 ) @ ( f @ ( suc @ ( suc @ B_11 ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ B_12 ) ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ B_13 ) @ ( f @ ( suc @ ( suc @ B_13 ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ B_12 ) @ ( f @ ( suc @ ( suc @ B_12 ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ A_1 ) @ ( f @ ( suc @ ( suc @ A_1 ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ B_12 ) @ ( f @ ( suc @ B_12 ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ B_12 ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ A_1 ) @ ( f @ ( suc @ A_1 ) ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ B_11 ) @ ( f @ ( suc @ B_11 ) ) ) ) |
% 48.05/13.03 ( ~( iLEQ @ ( suc @ A_1 ) @ ( suc @ B_11 ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ B_13 ) ) ) ) | ( ~( E @ 0 @ ( f @ B_12 ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ B_13 ) ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ B_13 ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ B_13 ) @ ( f @ ( suc @ B_13 ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ B_12 ) ) ) ) ) ) |
% 48.05/13.03 ( ~( iLEQ @ ( suc @ B_11 ) @ ( suc @ B_12 ) ) ) |
% 48.05/13.03 ( E @ ( f @ A_1 ) @ ( f @ ( suc @ ( suc @ ( suc @ A_1 ) ) ) ) ) |
% 48.05/13.03 ( E @ ( f @ B_11 ) @ ( f @ ( suc @ ( suc @ ( suc @ B_11 ) ) ) ) ) |
% 48.05/13.03 ( E @ ( f @ B_12 ) @ ( f @ ( suc @ ( suc @ ( suc @ B_12 ) ) ) ) ) |
% 48.05/13.03 ( E @ ( f @ B_13 ) @ ( f @ ( suc @ ( suc @ ( suc @ B_13 ) ) ) ) ))).
% 48.05/13.03 thf(zip_derived_cl259, plain,
% 48.05/13.03 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 48.05/13.03 (~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X1)))))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X2) @ (suc @ X3))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X1))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X1))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X3))
% 48.05/13.03 | ~ (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X2)))
% 48.05/13.03 | ~ (E @ (f @ X3) @ (f @ (suc @ (suc @ X3))))
% 48.05/13.03 | ~ (E @ (f @ X2) @ (f @ (suc @ (suc @ X2))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ (f @ X2) @ (f @ (suc @ X2)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X2))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X3)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X2))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X3)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X3))))
% 48.05/13.03 | ~ (E @ (f @ X3) @ (f @ (suc @ X3)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X2)))))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X1) @ (suc @ X2))
% 48.05/13.03 | (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | (E @ (f @ X1) @ (f @ (suc @ (suc @ (suc @ X1)))))
% 48.05/13.03 | (E @ (f @ X2) @ (f @ (suc @ (suc @ (suc @ X2)))))
% 48.05/13.03 | (E @ (f @ X3) @ (f @ (suc @ (suc @ (suc @ X3))))))),
% 48.05/13.03 inference('cnf', [status(esa)], [clause_4416])).
% 48.05/13.03 thf(zip_derived_cl1887, plain,
% 48.05/13.03 (![X0 : $i, X1 : $i]:
% 48.05/13.03 ( (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | (E @ (f @ X1) @ (f @ (suc @ (suc @ (suc @ X1)))))
% 48.05/13.03 | (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | (E @ (f @ X1) @ (f @ (suc @ (suc @ (suc @ X1)))))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X1)))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X1))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X1) @ (suc @ X0))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X1))))
% 48.05/13.03 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 48.05/13.03 | ~ (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X1))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X1))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X1))))))),
% 48.05/13.03 inference('eq_fact', [status(thm)], [zip_derived_cl259])).
% 48.05/13.03 thf(zip_derived_cl1888, plain,
% 48.05/13.03 (![X0 : $i, X1 : $i]:
% 48.05/13.03 (~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X1))))
% 48.05/13.03 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X1) @ (suc @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X1))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X1)))))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 48.05/13.03 | (E @ (f @ X1) @ (f @ (suc @ (suc @ (suc @ X1)))))
% 48.05/13.03 | (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0))))))),
% 48.05/13.03 inference('simplify', [status(thm)], [zip_derived_cl1887])).
% 48.05/13.03 thf(zip_derived_cl1893, plain,
% 48.05/13.03 ((~ (E @ 0 @ (f @ z))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ z)))
% 48.05/13.03 | ~ (E @ (f @ z) @ (f @ (suc @ (suc @ z))))
% 48.05/13.03 | ~ (E @ (f @ z) @ (f @ (suc @ (suc @ z))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ z))))
% 48.05/13.03 | ~ (E @ (f @ z) @ (f @ (suc @ z)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ z)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ z))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ z)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ z))))
% 48.05/13.03 | ~ (E @ (f @ z) @ (f @ (suc @ z)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ z)))))
% 48.05/13.03 | (E @ (f @ z) @ (f @ (suc @ (suc @ (suc @ z)))))
% 48.05/13.03 | (E @ (f @ z) @ (f @ (suc @ (suc @ (suc @ z))))))),
% 48.05/13.03 inference('s_sup-', [status(thm)],
% 48.05/13.03 [zip_derived_cl348, zip_derived_cl1888])).
% 48.05/13.03 thf(zip_derived_cl267, plain,
% 48.05/13.03 (![X0 : $i]: ( (E @ 0 @ (f @ X0)) | (LE @ (f @ X0) @ 0))),
% 48.05/13.03 inference('demod', [status(thm)], [zip_derived_cl87, zip_derived_cl64])).
% 48.05/13.03 thf(zip_derived_cl10, plain, (~ (LE @ (f @ z) @ 0)),
% 48.05/13.03 inference('cnf', [status(esa)], [clause_20481])).
% 48.05/13.03 thf(zip_derived_cl268, plain, ( (E @ 0 @ (f @ z))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl267, zip_derived_cl10])).
% 48.05/13.03 thf(zip_derived_cl279, plain,
% 48.05/13.03 (![X0 : $i]: ( (E @ 0 @ (f @ (suc @ X0))) | (LE @ (f @ X0) @ 0))),
% 48.05/13.03 inference('demod', [status(thm)], [zip_derived_cl230, zip_derived_cl64])).
% 48.05/13.03 thf(zip_derived_cl10, plain, (~ (LE @ (f @ z) @ 0)),
% 48.05/13.03 inference('cnf', [status(esa)], [clause_20481])).
% 48.05/13.03 thf(zip_derived_cl280, plain, ( (E @ 0 @ (f @ (suc @ z)))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl279, zip_derived_cl10])).
% 48.05/13.03 thf(zip_derived_cl348, plain, ( (iLEQ @ (suc @ z) @ (suc @ z))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl347, zip_derived_cl10])).
% 48.05/13.03 thf(clause_27210, axiom,
% 48.05/13.03 (( ~( E @ 0 @ ( f @ ( suc @ B_11 ) ) ) ) |
% 48.05/13.03 ( ~( iLEQ @ ( suc @ B_12 ) @ ( suc @ B_13 ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ B_11 ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ A_1 ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ A_1 ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ B_11 ) ) ) | ( ~( E @ 0 @ ( f @ A_1 ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ B_13 ) ) ) | ( ~( E @ 0 @ ( f @ ( suc @ B_12 ) ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ B_12 ) @ ( f @ ( suc @ B_12 ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ B_12 ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ A_1 ) @ ( f @ ( suc @ A_1 ) ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ B_11 ) @ ( f @ ( suc @ B_11 ) ) ) ) |
% 48.05/13.03 ( ~( iLEQ @ ( suc @ A_1 ) @ ( suc @ B_11 ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ B_13 ) ) ) ) | ( ~( E @ 0 @ ( f @ B_12 ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ B_13 ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ B_13 ) @ ( f @ ( suc @ B_13 ) ) ) ) |
% 48.05/13.03 ( ~( iLEQ @ ( suc @ B_11 ) @ ( suc @ B_12 ) ) ) |
% 48.05/13.03 ( E @ ( f @ A_1 ) @ ( f @ ( suc @ ( suc @ A_1 ) ) ) ) |
% 48.05/13.03 ( E @ ( f @ B_11 ) @ ( f @ ( suc @ ( suc @ B_11 ) ) ) ) |
% 48.05/13.03 ( E @ ( f @ B_12 ) @ ( f @ ( suc @ ( suc @ B_12 ) ) ) ) |
% 48.05/13.03 ( E @ ( f @ B_13 ) @ ( f @ ( suc @ ( suc @ B_13 ) ) ) ))).
% 48.05/13.03 thf(zip_derived_cl250, plain,
% 48.05/13.03 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 48.05/13.03 (~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X1) @ (suc @ X2))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X3)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X3))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X3))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X2))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X1))))
% 48.05/13.03 | ~ (E @ (f @ X3) @ (f @ (suc @ X3)))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X3) @ (suc @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X2)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X1))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X2))))
% 48.05/13.03 | ~ (E @ (f @ X2) @ (f @ (suc @ X2)))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 48.05/13.03 | (E @ (f @ X3) @ (f @ (suc @ (suc @ X3))))
% 48.05/13.03 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 48.05/13.03 | (E @ (f @ X2) @ (f @ (suc @ (suc @ X2)))))),
% 48.05/13.03 inference('cnf', [status(esa)], [clause_27210])).
% 48.05/13.03 thf(zip_derived_cl784, plain,
% 48.05/13.03 (![X0 : $i, X1 : $i]:
% 48.05/13.03 ( (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 48.05/13.03 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X1))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X1) @ (suc @ X0))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X1))))
% 48.05/13.03 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X1))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X1))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0))))),
% 48.05/13.03 inference('eq_fact', [status(thm)], [zip_derived_cl250])).
% 48.05/13.03 thf(zip_derived_cl785, plain,
% 48.05/13.03 (![X0 : $i, X1 : $i]:
% 48.05/13.03 (~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X1))))
% 48.05/13.03 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X1) @ (suc @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X1))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 48.05/13.03 | (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 48.05/13.03 | (E @ (f @ X0) @ (f @ (suc @ (suc @ X0)))))),
% 48.05/13.03 inference('simplify', [status(thm)], [zip_derived_cl784])).
% 48.05/13.03 thf(zip_derived_cl790, plain,
% 48.05/13.03 ((~ (E @ 0 @ (f @ z))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ z)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ z))))
% 48.05/13.03 | ~ (E @ (f @ z) @ (f @ (suc @ z)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ z)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ z))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ z))))
% 48.05/13.03 | ~ (E @ (f @ z) @ (f @ (suc @ z)))
% 48.05/13.03 | (E @ (f @ z) @ (f @ (suc @ (suc @ z))))
% 48.05/13.03 | (E @ (f @ z) @ (f @ (suc @ (suc @ z)))))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl348, zip_derived_cl785])).
% 48.05/13.03 thf(zip_derived_cl268, plain, ( (E @ 0 @ (f @ z))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl267, zip_derived_cl10])).
% 48.05/13.03 thf(zip_derived_cl280, plain, ( (E @ 0 @ (f @ (suc @ z)))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl279, zip_derived_cl10])).
% 48.05/13.03 thf(zip_derived_cl287, plain,
% 48.05/13.03 (![X0 : $i]: ( (E @ 0 @ (f @ (suc @ (suc @ X0)))) | (LE @ (f @ X0) @ 0))),
% 48.05/13.03 inference('demod', [status(thm)], [zip_derived_cl242, zip_derived_cl64])).
% 48.05/13.03 thf(zip_derived_cl10, plain, (~ (LE @ (f @ z) @ 0)),
% 48.05/13.03 inference('cnf', [status(esa)], [clause_20481])).
% 48.05/13.03 thf(zip_derived_cl288, plain, ( (E @ 0 @ (f @ (suc @ (suc @ z))))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl287, zip_derived_cl10])).
% 48.05/13.03 thf(zip_derived_cl348, plain, ( (iLEQ @ (suc @ z) @ (suc @ z))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl347, zip_derived_cl10])).
% 48.05/13.03 thf(clause_2022, axiom,
% 48.05/13.03 (( ~( E @ 0 @ ( f @ ( suc @ B_11 ) ) ) ) |
% 48.05/13.03 ( ~( iLEQ @ ( suc @ B_12 ) @ ( suc @ B_13 ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ A_1 ) ) ) ) | ( ~( E @ 0 @ ( f @ B_11 ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ A_1 ) ) ) | ( ~( E @ 0 @ ( f @ B_13 ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ B_12 ) ) ) ) |
% 48.05/13.03 ( ~( iLEQ @ ( suc @ A_1 ) @ ( suc @ B_11 ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ B_13 ) ) ) ) | ( ~( E @ 0 @ ( f @ B_12 ) ) ) |
% 48.05/13.03 ( ~( iLEQ @ ( suc @ B_11 ) @ ( suc @ B_12 ) ) ) |
% 48.05/13.03 ( E @ ( f @ A_1 ) @ ( f @ ( suc @ A_1 ) ) ) |
% 48.05/13.03 ( E @ ( f @ B_11 ) @ ( f @ ( suc @ B_11 ) ) ) |
% 48.05/13.03 ( E @ ( f @ B_12 ) @ ( f @ ( suc @ B_12 ) ) ) |
% 48.05/13.03 ( E @ ( f @ B_13 ) @ ( f @ ( suc @ B_13 ) ) ))).
% 48.05/13.03 thf(zip_derived_cl221, plain,
% 48.05/13.03 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 48.05/13.03 (~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X1) @ (suc @ X2))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X3)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X3))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X2))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X3) @ (suc @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X2)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X1))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 48.05/13.03 | (E @ (f @ X3) @ (f @ (suc @ X3)))
% 48.05/13.03 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | (E @ (f @ X1) @ (f @ (suc @ X1)))
% 48.05/13.03 | (E @ (f @ X2) @ (f @ (suc @ X2))))),
% 48.05/13.03 inference('cnf', [status(esa)], [clause_2022])).
% 48.05/13.03 thf(zip_derived_cl351, plain,
% 48.05/13.03 (![X0 : $i, X1 : $i]:
% 48.05/13.03 ( (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | (E @ (f @ X1) @ (f @ (suc @ X1)))
% 48.05/13.03 | (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | (E @ (f @ X1) @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X1))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X1) @ (suc @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X1))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0))))),
% 48.05/13.03 inference('eq_fact', [status(thm)], [zip_derived_cl221])).
% 48.05/13.03 thf(zip_derived_cl352, plain,
% 48.05/13.03 (![X0 : $i, X1 : $i]:
% 48.05/13.03 (~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X1) @ (suc @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X1))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X0) @ (suc @ X1))
% 48.05/13.03 | (E @ (f @ X1) @ (f @ (suc @ X1)))
% 48.05/13.03 | (E @ (f @ X0) @ (f @ (suc @ X0))))),
% 48.05/13.03 inference('simplify', [status(thm)], [zip_derived_cl351])).
% 48.05/13.03 thf(zip_derived_cl361, plain,
% 48.05/13.03 ((~ (E @ 0 @ (f @ z))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ z)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ z)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ z))
% 48.05/13.03 | (E @ (f @ z) @ (f @ (suc @ z)))
% 48.05/13.03 | (E @ (f @ z) @ (f @ (suc @ z))))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl348, zip_derived_cl352])).
% 48.05/13.03 thf(zip_derived_cl268, plain, ( (E @ 0 @ (f @ z))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl267, zip_derived_cl10])).
% 48.05/13.03 thf(zip_derived_cl280, plain, ( (E @ 0 @ (f @ (suc @ z)))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl279, zip_derived_cl10])).
% 48.05/13.03 thf(zip_derived_cl280, plain, ( (E @ 0 @ (f @ (suc @ z)))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl279, zip_derived_cl10])).
% 48.05/13.03 thf(zip_derived_cl268, plain, ( (E @ 0 @ (f @ z))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl267, zip_derived_cl10])).
% 48.05/13.03 thf(zip_derived_cl363, plain,
% 48.05/13.03 (( (E @ (f @ z) @ (f @ (suc @ z))) | (E @ (f @ z) @ (f @ (suc @ z))))),
% 48.05/13.03 inference('demod', [status(thm)],
% 48.05/13.03 [zip_derived_cl361, zip_derived_cl268, zip_derived_cl280,
% 48.05/13.03 zip_derived_cl280, zip_derived_cl268])).
% 48.05/13.03 thf(zip_derived_cl364, plain, ( (E @ (f @ z) @ (f @ (suc @ z)))),
% 48.05/13.03 inference('simplify', [status(thm)], [zip_derived_cl363])).
% 48.05/13.03 thf(zip_derived_cl280, plain, ( (E @ 0 @ (f @ (suc @ z)))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl279, zip_derived_cl10])).
% 48.05/13.03 thf(zip_derived_cl268, plain, ( (E @ 0 @ (f @ z))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl267, zip_derived_cl10])).
% 48.05/13.03 thf(zip_derived_cl288, plain, ( (E @ 0 @ (f @ (suc @ (suc @ z))))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl287, zip_derived_cl10])).
% 48.05/13.03 thf(zip_derived_cl364, plain, ( (E @ (f @ z) @ (f @ (suc @ z)))),
% 48.05/13.03 inference('simplify', [status(thm)], [zip_derived_cl363])).
% 48.05/13.03 thf(zip_derived_cl792, plain,
% 48.05/13.03 (( (E @ (f @ z) @ (f @ (suc @ (suc @ z))))
% 48.05/13.03 | (E @ (f @ z) @ (f @ (suc @ (suc @ z)))))),
% 48.05/13.03 inference('demod', [status(thm)],
% 48.05/13.03 [zip_derived_cl790, zip_derived_cl268, zip_derived_cl280,
% 48.05/13.03 zip_derived_cl288, zip_derived_cl364, zip_derived_cl280,
% 48.05/13.03 zip_derived_cl268, zip_derived_cl288, zip_derived_cl364])).
% 48.05/13.03 thf(zip_derived_cl793, plain, ( (E @ (f @ z) @ (f @ (suc @ (suc @ z))))),
% 48.05/13.03 inference('simplify', [status(thm)], [zip_derived_cl792])).
% 48.05/13.03 thf(zip_derived_cl793, plain, ( (E @ (f @ z) @ (f @ (suc @ (suc @ z))))),
% 48.05/13.03 inference('simplify', [status(thm)], [zip_derived_cl792])).
% 48.05/13.03 thf(zip_derived_cl288, plain, ( (E @ 0 @ (f @ (suc @ (suc @ z))))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl287, zip_derived_cl10])).
% 48.05/13.03 thf(zip_derived_cl364, plain, ( (E @ (f @ z) @ (f @ (suc @ z)))),
% 48.05/13.03 inference('simplify', [status(thm)], [zip_derived_cl363])).
% 48.05/13.03 thf(zip_derived_cl280, plain, ( (E @ 0 @ (f @ (suc @ z)))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl279, zip_derived_cl10])).
% 48.05/13.03 thf(zip_derived_cl268, plain, ( (E @ 0 @ (f @ z))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl267, zip_derived_cl10])).
% 48.05/13.03 thf(zip_derived_cl291, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 ( (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0))))) | (LE @ (f @ X0) @ 0))),
% 48.05/13.03 inference('demod', [status(thm)], [zip_derived_cl183, zip_derived_cl64])).
% 48.05/13.03 thf(zip_derived_cl10, plain, (~ (LE @ (f @ z) @ 0)),
% 48.05/13.03 inference('cnf', [status(esa)], [clause_20481])).
% 48.05/13.03 thf(zip_derived_cl292, plain, ( (E @ 0 @ (f @ (suc @ (suc @ (suc @ z)))))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl291, zip_derived_cl10])).
% 48.05/13.03 thf(zip_derived_cl288, plain, ( (E @ 0 @ (f @ (suc @ (suc @ z))))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl287, zip_derived_cl10])).
% 48.05/13.03 thf(zip_derived_cl364, plain, ( (E @ (f @ z) @ (f @ (suc @ z)))),
% 48.05/13.03 inference('simplify', [status(thm)], [zip_derived_cl363])).
% 48.05/13.03 thf(zip_derived_cl292, plain, ( (E @ 0 @ (f @ (suc @ (suc @ (suc @ z)))))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl291, zip_derived_cl10])).
% 48.05/13.03 thf(zip_derived_cl1895, plain,
% 48.05/13.03 (( (E @ (f @ z) @ (f @ (suc @ (suc @ (suc @ z)))))
% 48.05/13.03 | (E @ (f @ z) @ (f @ (suc @ (suc @ (suc @ z))))))),
% 48.05/13.03 inference('demod', [status(thm)],
% 48.05/13.03 [zip_derived_cl1893, zip_derived_cl268, zip_derived_cl280,
% 48.05/13.03 zip_derived_cl793, zip_derived_cl793, zip_derived_cl288,
% 48.05/13.03 zip_derived_cl364, zip_derived_cl280, zip_derived_cl268,
% 48.05/13.03 zip_derived_cl292, zip_derived_cl288, zip_derived_cl364,
% 48.05/13.03 zip_derived_cl292])).
% 48.05/13.03 thf(zip_derived_cl1896, plain,
% 48.05/13.03 ( (E @ (f @ z) @ (f @ (suc @ (suc @ (suc @ z)))))),
% 48.05/13.03 inference('simplify', [status(thm)], [zip_derived_cl1895])).
% 48.05/13.03 thf(clause_30990, axiom,
% 48.05/13.03 (( ~( E @ ( f @ B_13 ) @ ( f @ ( suc @ ( suc @ ( suc @ B_13 ) ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ A_1 ) ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ B_11 ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ B_11 ) ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ B_12 ) @ ( f @ ( suc @ ( suc @ ( suc @ B_12 ) ) ) ) ) ) |
% 48.05/13.03 ( ~( iLEQ @ ( suc @ B_12 ) @ ( suc @ B_13 ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ B_11 ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ A_1 ) ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ A_1 ) @ ( f @ ( suc @ ( suc @ ( suc @ A_1 ) ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ A_1 ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ B_11 ) ) ) | ( ~( E @ 0 @ ( f @ A_1 ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ B_13 ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ B_11 ) @ ( f @ ( suc @ ( suc @ B_11 ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ B_12 ) ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ B_13 ) @ ( f @ ( suc @ ( suc @ B_13 ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ B_12 ) @ ( f @ ( suc @ ( suc @ B_12 ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ A_1 ) @ ( f @ ( suc @ ( suc @ A_1 ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ B_12 ) @ ( f @ ( suc @ B_12 ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ B_12 ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ A_1 ) @ ( f @ ( suc @ A_1 ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ ( suc @ B_11 ) ) ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ B_11 ) @ ( f @ ( suc @ ( suc @ ( suc @ B_11 ) ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ ( suc @ B_13 ) ) ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ B_11 ) @ ( f @ ( suc @ B_11 ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ ( suc @ B_12 ) ) ) ) ) ) ) |
% 48.05/13.03 ( ~( iLEQ @ ( suc @ A_1 ) @ ( suc @ B_11 ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ B_13 ) ) ) ) | ( ~( E @ 0 @ ( f @ B_12 ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ ( suc @ A_1 ) ) ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ B_13 ) ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ B_13 ) ) ) ) ) |
% 48.05/13.03 ( ~( E @ ( f @ B_13 ) @ ( f @ ( suc @ B_13 ) ) ) ) |
% 48.05/13.03 ( ~( E @ 0 @ ( f @ ( suc @ ( suc @ ( suc @ B_12 ) ) ) ) ) ) |
% 48.05/13.03 ( ~( iLEQ @ ( suc @ B_11 ) @ ( suc @ B_12 ) ) ))).
% 48.05/13.03 thf(zip_derived_cl59, plain,
% 48.05/13.03 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 48.05/13.03 (~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X1)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X2)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X2)))))
% 48.05/13.03 | ~ (E @ (f @ X3) @ (f @ (suc @ (suc @ (suc @ X3)))))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X3) @ (suc @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X2))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (E @ (f @ X1) @ (f @ (suc @ (suc @ (suc @ X1)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X1))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X2))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X1))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ (f @ X2) @ (f @ (suc @ (suc @ X2))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X3)))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ (f @ X3) @ (f @ (suc @ (suc @ X3))))
% 48.05/13.03 | ~ (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 48.05/13.03 | ~ (E @ (f @ X3) @ (f @ (suc @ X3)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X3))))
% 48.05/13.03 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X2))))))
% 48.05/13.03 | ~ (E @ (f @ X2) @ (f @ (suc @ (suc @ (suc @ X2)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 48.05/13.03 | ~ (E @ (f @ X2) @ (f @ (suc @ X2)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X3))))))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X1) @ (suc @ X2))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X3))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X1))))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X3)))))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X2) @ (suc @ X3)))),
% 48.05/13.03 inference('cnf', [status(esa)], [clause_30990])).
% 48.05/13.03 thf(zip_derived_cl269, plain,
% 48.05/13.03 (![X0 : $i, X1 : $i, X2 : $i]:
% 48.05/13.03 (~ (iLEQ @ (suc @ X1) @ (suc @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X2))))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X2) @ (suc @ X1))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 48.05/13.03 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 48.05/13.03 | ~ (E @ (f @ X1) @ (f @ (suc @ (suc @ (suc @ X1)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X1))))))
% 48.05/13.03 | ~ (E @ (f @ X2) @ (f @ (suc @ X2)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ (f @ X2) @ (f @ (suc @ (suc @ X2))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X2))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X1))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X2))))
% 48.05/13.03 | ~ (E @ (f @ X2) @ (f @ (suc @ (suc @ (suc @ X2)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X2)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X1))))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X1)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X2))))))),
% 48.05/13.03 inference('eq_fact', [status(thm)], [zip_derived_cl59])).
% 48.05/13.03 thf(zip_derived_cl272, plain,
% 48.05/13.03 (![X0 : $i, X1 : $i, X2 : $i]:
% 48.05/13.03 (~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X2)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X1)))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X1))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X2)))
% 48.05/13.03 | ~ (E @ (f @ X2) @ (f @ (suc @ (suc @ (suc @ X2)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X2))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X1))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X2))
% 48.05/13.03 | ~ (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ (f @ X2) @ (f @ (suc @ (suc @ X2))))
% 48.05/13.03 | ~ (E @ (f @ X2) @ (f @ (suc @ X2)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X1))))))
% 48.05/13.03 | ~ (E @ (f @ X1) @ (f @ (suc @ (suc @ (suc @ X1)))))
% 48.05/13.03 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X2) @ (suc @ X1))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X2))))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X1) @ (suc @ X0)))),
% 48.05/13.03 inference('simplify', [status(thm)], [zip_derived_cl269])).
% 48.05/13.03 thf(zip_derived_cl282, plain,
% 48.05/13.03 (![X0 : $i, X1 : $i]:
% 48.05/13.03 (~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X1))))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X1) @ (suc @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 48.05/13.03 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X1))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X1))))
% 48.05/13.03 | ~ (E @ (f @ X1) @ (f @ (suc @ (suc @ (suc @ X1)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X1))))))),
% 48.05/13.03 inference('eq_fact', [status(thm)], [zip_derived_cl272])).
% 48.05/13.03 thf(zip_derived_cl284, plain,
% 48.05/13.03 (![X0 : $i, X1 : $i]:
% 48.05/13.03 (~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X1)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (E @ (f @ X1) @ (f @ (suc @ (suc @ (suc @ X1)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X1))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X1))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ (f @ X1) @ (f @ (suc @ (suc @ X1))))
% 48.05/13.03 | ~ (E @ (f @ X1) @ (f @ (suc @ X1)))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X1) @ (suc @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X1))))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 48.05/13.03 inference('simplify', [status(thm)], [zip_derived_cl282])).
% 48.05/13.03 thf(zip_derived_cl285, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 (~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0))))))),
% 48.05/13.03 inference('eq_fact', [status(thm)], [zip_derived_cl284])).
% 48.05/13.03 thf(zip_derived_cl286, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 (~ (E @ (f @ X0) @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ X0))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ X0))))
% 48.05/13.03 | ~ (E @ (f @ X0) @ (f @ (suc @ X0)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ X0)))))
% 48.05/13.03 | ~ (iLEQ @ (suc @ X0) @ (suc @ X0)))),
% 48.05/13.03 inference('simplify', [status(thm)], [zip_derived_cl285])).
% 48.05/13.03 thf(zip_derived_cl2016, plain,
% 48.05/13.03 ((~ (E @ (f @ z) @ (f @ (suc @ (suc @ z))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ z)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ z))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ z))))))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ z))))
% 48.05/13.03 | ~ (E @ (f @ z) @ (f @ (suc @ z)))
% 48.05/13.03 | ~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ z)))))
% 48.05/13.03 | ~ (iLEQ @ (suc @ z) @ (suc @ z)))),
% 48.05/13.03 inference('s_sup-', [status(thm)],
% 48.05/13.03 [zip_derived_cl1896, zip_derived_cl286])).
% 48.05/13.03 thf(zip_derived_cl793, plain, ( (E @ (f @ z) @ (f @ (suc @ (suc @ z))))),
% 48.05/13.03 inference('simplify', [status(thm)], [zip_derived_cl792])).
% 48.05/13.03 thf(zip_derived_cl280, plain, ( (E @ 0 @ (f @ (suc @ z)))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl279, zip_derived_cl10])).
% 48.05/13.03 thf(zip_derived_cl268, plain, ( (E @ 0 @ (f @ z))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl267, zip_derived_cl10])).
% 48.05/13.03 thf(zip_derived_cl288, plain, ( (E @ 0 @ (f @ (suc @ (suc @ z))))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl287, zip_derived_cl10])).
% 48.05/13.03 thf(zip_derived_cl364, plain, ( (E @ (f @ z) @ (f @ (suc @ z)))),
% 48.05/13.03 inference('simplify', [status(thm)], [zip_derived_cl363])).
% 48.05/13.03 thf(zip_derived_cl292, plain, ( (E @ 0 @ (f @ (suc @ (suc @ (suc @ z)))))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl291, zip_derived_cl10])).
% 48.05/13.03 thf(zip_derived_cl348, plain, ( (iLEQ @ (suc @ z) @ (suc @ z))),
% 48.05/13.03 inference('s_sup-', [status(thm)], [zip_derived_cl347, zip_derived_cl10])).
% 48.05/13.03 thf(zip_derived_cl2227, plain,
% 48.05/13.03 (~ (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ z))))))),
% 48.05/13.03 inference('demod', [status(thm)],
% 48.05/13.03 [zip_derived_cl2016, zip_derived_cl793, zip_derived_cl280,
% 48.05/13.03 zip_derived_cl268, zip_derived_cl288, zip_derived_cl364,
% 48.05/13.03 zip_derived_cl292, zip_derived_cl348])).
% 48.05/13.03 thf(zip_derived_cl297, plain,
% 48.05/13.03 (![X0 : $i]:
% 48.05/13.03 ( (E @ 0 @ (f @ (suc @ (suc @ (suc @ (suc @ X0))))))
% 48.05/13.03 | (LE @ (f @ X0) @ 0))),
% 48.05/13.03 inference('demod', [status(thm)], [zip_derived_cl27, zip_derived_cl64])).
% 48.05/13.03 thf(zip_derived_cl2319, plain, ( (LE @ (f @ z) @ 0)),
% 48.05/13.03 inference('s_sup+', [status(thm)],
% 48.05/13.03 [zip_derived_cl2227, zip_derived_cl297])).
% 48.05/13.03 thf(zip_derived_cl2322, plain, ($false),
% 48.05/13.03 inference('demod', [status(thm)], [zip_derived_cl10, zip_derived_cl2319])).
% 48.05/13.03
% 48.05/13.03 % SZS output end Refutation
% 48.05/13.03
% 48.05/13.03
% 48.05/13.03 % Terminating...
% 48.25/13.15 % Runner terminated.
% 48.25/13.16 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------