%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : LCL160-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.pvOqUamHTx true
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 01:35:18 PM UTC 2026
% Result : Unsatisfiable 36.43s 5.82s
% Output : Refutation 36.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL160-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.05 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.pvOqUamHTx true
% 0.09/0.35 % Computer : n010.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Fri Sep 4 15:18:08 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 % Running portfolio for 300 s
% 0.09/0.35 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.36 % Number of cores: 8
% 0.13/0.36 % Python version: Python 3.12.3
% 0.13/0.36 % Running in FO mode
% 0.46/0.63 % Total configuration time : 435
% 0.46/0.63 % Estimated wc time : 1092
% 0.46/0.63 % Estimated cpu time (7 cpus) : 156.0
% 0.46/0.71 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.46/0.78 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.46/0.78 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.46/0.78 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.46/0.78 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.46/0.78 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.46/0.80 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 36.43/5.82 % Solved by fo/fo4.sh.
% 36.43/5.82 % done 1907 iterations in 4.982s
% 36.43/5.82 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 36.43/5.82 % SZS output start Refutation
% 36.43/5.82 thf(and_type, type, and: $i > $i > $i).
% 36.43/5.82 thf(xor_type, type, xor: $i > $i > $i).
% 36.43/5.82 thf(x_type, type, x: $i).
% 36.43/5.82 thf(or_type, type, or: $i > $i > $i).
% 36.43/5.82 thf(y_type, type, y: $i).
% 36.43/5.82 thf(truth_type, type, truth: $i).
% 36.43/5.82 thf(implies_type, type, implies: $i > $i > $i).
% 36.43/5.82 thf(falsehood_type, type, falsehood: $i).
% 36.43/5.82 thf(and_star_type, type, and_star: $i > $i > $i).
% 36.43/5.82 thf(not_type, type, not: $i > $i).
% 36.43/5.82 thf(prove_alternative_wajsberg_axiom, conjecture,
% 36.43/5.82 (( and_star @ ( xor @ ( and_star @ ( xor @ truth @ x ) @ y ) @ truth ) @ y ) =
% 36.43/5.82 ( and_star @ ( xor @ ( and_star @ ( xor @ truth @ y ) @ x ) @ truth ) @ x ))).
% 36.43/5.82 thf(zf_stmt_0, negated_conjecture,
% 36.43/5.82 (( and_star @ ( xor @ ( and_star @ ( xor @ truth @ x ) @ y ) @ truth ) @ y ) !=
% 36.43/5.82 ( and_star @ ( xor @ ( and_star @ ( xor @ truth @ y ) @ x ) @ truth ) @ x )),
% 36.43/5.82 inference('cnf.neg', [status(esa)], [prove_alternative_wajsberg_axiom])).
% 36.43/5.82 thf(zip_derived_cl16, plain,
% 36.43/5.82 (((and_star @ (xor @ (and_star @ (xor @ truth @ x) @ y) @ truth) @ y)
% 36.43/5.82 != (and_star @ (xor @ (and_star @ (xor @ truth @ y) @ x) @ truth) @ x))),
% 36.43/5.82 inference('cnf', [status(esa)], [zf_stmt_0])).
% 36.43/5.82 thf(xor_commutativity, axiom, (( xor @ X @ Y ) = ( xor @ Y @ X ))).
% 36.43/5.82 thf(zip_derived_cl11, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((xor @ X1 @ X0) = (xor @ X0 @ X1))),
% 36.43/5.82 inference('cnf', [status(esa)], [xor_commutativity])).
% 36.43/5.82 thf(zip_derived_cl11, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((xor @ X1 @ X0) = (xor @ X0 @ X1))),
% 36.43/5.82 inference('cnf', [status(esa)], [xor_commutativity])).
% 36.43/5.82 thf(zip_derived_cl11, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((xor @ X1 @ X0) = (xor @ X0 @ X1))),
% 36.43/5.82 inference('cnf', [status(esa)], [xor_commutativity])).
% 36.43/5.82 thf(zip_derived_cl11, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((xor @ X1 @ X0) = (xor @ X0 @ X1))),
% 36.43/5.82 inference('cnf', [status(esa)], [xor_commutativity])).
% 36.43/5.82 thf(zip_derived_cl18, plain,
% 36.43/5.82 (((and_star @ (xor @ truth @ (and_star @ (xor @ x @ truth) @ y)) @ y)
% 36.43/5.82 != (and_star @ (xor @ truth @ (and_star @ (xor @ y @ truth) @ x)) @ x))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl16, zip_derived_cl11, zip_derived_cl11,
% 36.43/5.82 zip_derived_cl11, zip_derived_cl11])).
% 36.43/5.82 thf(and_star_commutativity, axiom,
% 36.43/5.82 (( and_star @ X @ Y ) = ( and_star @ Y @ X ))).
% 36.43/5.82 thf(zip_derived_cl14, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((and_star @ X1 @ X0) = (and_star @ X0 @ X1))),
% 36.43/5.82 inference('cnf', [status(esa)], [and_star_commutativity])).
% 36.43/5.82 thf(zip_derived_cl14, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((and_star @ X1 @ X0) = (and_star @ X0 @ X1))),
% 36.43/5.82 inference('cnf', [status(esa)], [and_star_commutativity])).
% 36.43/5.82 thf(zip_derived_cl14, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((and_star @ X1 @ X0) = (and_star @ X0 @ X1))),
% 36.43/5.82 inference('cnf', [status(esa)], [and_star_commutativity])).
% 36.43/5.82 thf(zip_derived_cl14, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((and_star @ X1 @ X0) = (and_star @ X0 @ X1))),
% 36.43/5.82 inference('cnf', [status(esa)], [and_star_commutativity])).
% 36.43/5.82 thf(zip_derived_cl19, plain,
% 36.43/5.82 (((and_star @ y @ (xor @ truth @ (and_star @ y @ (xor @ x @ truth))))
% 36.43/5.82 != (and_star @ x @ (xor @ truth @ (and_star @ x @ (xor @ y @ truth)))))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl18, zip_derived_cl14, zip_derived_cl14,
% 36.43/5.82 zip_derived_cl14, zip_derived_cl14])).
% 36.43/5.82 thf(false_definition, axiom, (( not @ truth ) = ( falsehood ))).
% 36.43/5.82 thf(zip_derived_cl15, plain, (((not @ truth) = (falsehood))),
% 36.43/5.82 inference('cnf', [status(esa)], [false_definition])).
% 36.43/5.82 thf(and_star_definition, axiom,
% 36.43/5.82 (( and_star @ X @ Y ) = ( not @ ( or @ ( not @ X ) @ ( not @ Y ) ) ))).
% 36.43/5.82 thf(zip_derived_cl12, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((and_star @ X0 @ X1) = (not @ (or @ (not @ X0) @ (not @ X1))))),
% 36.43/5.82 inference('cnf', [status(esa)], [and_star_definition])).
% 36.43/5.82 thf(zip_derived_cl161, plain,
% 36.43/5.82 (![X0 : $i]:
% 36.43/5.82 ((and_star @ X0 @ truth) = (not @ (or @ (not @ X0) @ falsehood)))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl15, zip_derived_cl12])).
% 36.43/5.82 thf(wajsberg_1, axiom, (( implies @ truth @ X ) = ( X ))).
% 36.43/5.82 thf(zip_derived_cl0, plain, (![X0 : $i]: ((implies @ truth @ X0) = (X0))),
% 36.43/5.82 inference('cnf', [status(esa)], [wajsberg_1])).
% 36.43/5.82 thf(wajsberg_2, axiom,
% 36.43/5.82 (( implies @
% 36.43/5.82 ( implies @ X @ Y ) @
% 36.43/5.82 ( implies @ ( implies @ Y @ Z ) @ ( implies @ X @ Z ) ) ) =
% 36.43/5.82 ( truth ))).
% 36.43/5.82 thf(zip_derived_cl1, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i, X2 : $i]:
% 36.43/5.82 ((implies @ (implies @ X0 @ X1) @
% 36.43/5.82 (implies @ (implies @ X1 @ X2) @ (implies @ X0 @ X2))) = (truth))),
% 36.43/5.82 inference('cnf', [status(esa)], [wajsberg_2])).
% 36.43/5.82 thf(zip_derived_cl26, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((implies @ (implies @ truth @ X1) @
% 36.43/5.82 (implies @ (implies @ X1 @ X0) @ X0)) = (truth))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl0, zip_derived_cl1])).
% 36.43/5.82 thf(zip_derived_cl0, plain, (![X0 : $i]: ((implies @ truth @ X0) = (X0))),
% 36.43/5.82 inference('cnf', [status(esa)], [wajsberg_1])).
% 36.43/5.82 thf(zip_derived_cl37, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((implies @ X1 @ (implies @ (implies @ X1 @ X0) @ X0)) = (truth))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl26, zip_derived_cl0])).
% 36.43/5.82 thf(zip_derived_cl0, plain, (![X0 : $i]: ((implies @ truth @ X0) = (X0))),
% 36.43/5.82 inference('cnf', [status(esa)], [wajsberg_1])).
% 36.43/5.82 thf(zip_derived_cl50, plain,
% 36.43/5.82 (![X0 : $i]: ((truth) = (implies @ (implies @ truth @ X0) @ X0))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl37, zip_derived_cl0])).
% 36.43/5.82 thf(zip_derived_cl0, plain, (![X0 : $i]: ((implies @ truth @ X0) = (X0))),
% 36.43/5.82 inference('cnf', [status(esa)], [wajsberg_1])).
% 36.43/5.82 thf(zip_derived_cl62, plain, (![X0 : $i]: ((truth) = (implies @ X0 @ X0))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl50, zip_derived_cl0])).
% 36.43/5.82 thf(or_definition, axiom, (( or @ X @ Y ) = ( implies @ ( not @ X ) @ Y ))).
% 36.43/5.82 thf(zip_derived_cl4, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((or @ X0 @ X1) = (implies @ (not @ X0) @ X1))),
% 36.43/5.82 inference('cnf', [status(esa)], [or_definition])).
% 36.43/5.82 thf(zip_derived_cl70, plain,
% 36.43/5.82 (![X0 : $i]: ((or @ X0 @ (not @ X0)) = (truth))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl62, zip_derived_cl4])).
% 36.43/5.82 thf(zip_derived_cl62, plain, (![X0 : $i]: ((truth) = (implies @ X0 @ X0))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl50, zip_derived_cl0])).
% 36.43/5.82 thf(zip_derived_cl15, plain, (((not @ truth) = (falsehood))),
% 36.43/5.82 inference('cnf', [status(esa)], [false_definition])).
% 36.43/5.82 thf(zip_derived_cl4, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((or @ X0 @ X1) = (implies @ (not @ X0) @ X1))),
% 36.43/5.82 inference('cnf', [status(esa)], [or_definition])).
% 36.43/5.82 thf(zip_derived_cl17, plain,
% 36.43/5.82 (![X0 : $i]: ((or @ truth @ X0) = (implies @ falsehood @ X0))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl15, zip_derived_cl4])).
% 36.43/5.82 thf(zip_derived_cl71, plain, (((or @ truth @ falsehood) = (truth))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl62, zip_derived_cl17])).
% 36.43/5.82 thf(or_associativity, axiom,
% 36.43/5.82 (( or @ ( or @ X @ Y ) @ Z ) = ( or @ X @ ( or @ Y @ Z ) ))).
% 36.43/5.82 thf(zip_derived_cl5, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i, X2 : $i]:
% 36.43/5.82 ((or @ (or @ X0 @ X1) @ X2) = (or @ X0 @ (or @ X1 @ X2)))),
% 36.43/5.82 inference('cnf', [status(esa)], [or_associativity])).
% 36.43/5.82 thf(zip_derived_cl121, plain,
% 36.43/5.82 (![X0 : $i]: ((or @ truth @ X0) = (or @ truth @ (or @ falsehood @ X0)))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl71, zip_derived_cl5])).
% 36.43/5.82 thf(zip_derived_cl173, plain,
% 36.43/5.82 (((or @ truth @ (not @ falsehood)) = (or @ truth @ truth))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl70, zip_derived_cl121])).
% 36.43/5.82 thf(zip_derived_cl17, plain,
% 36.43/5.82 (![X0 : $i]: ((or @ truth @ X0) = (implies @ falsehood @ X0))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl15, zip_derived_cl4])).
% 36.43/5.82 thf(zip_derived_cl37, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((implies @ X1 @ (implies @ (implies @ X1 @ X0) @ X0)) = (truth))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl26, zip_derived_cl0])).
% 36.43/5.82 thf(zip_derived_cl57, plain,
% 36.43/5.82 (![X0 : $i]:
% 36.43/5.82 ((implies @ falsehood @ (implies @ (or @ truth @ X0) @ X0)) = (truth))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl17, zip_derived_cl37])).
% 36.43/5.82 thf(zip_derived_cl176, plain,
% 36.43/5.82 (((implies @ falsehood @
% 36.43/5.82 (implies @ (or @ truth @ truth) @ (not @ falsehood))) = (truth))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl173, zip_derived_cl57])).
% 36.43/5.82 thf(wajsberg_3, axiom,
% 36.43/5.82 (( implies @ ( implies @ X @ Y ) @ Y ) =
% 36.43/5.82 ( implies @ ( implies @ Y @ X ) @ X ))).
% 36.43/5.82 thf(zip_derived_cl2, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((implies @ (implies @ X1 @ X0) @ X0)
% 36.43/5.82 = (implies @ (implies @ X0 @ X1) @ X1))),
% 36.43/5.82 inference('cnf', [status(esa)], [wajsberg_3])).
% 36.43/5.82 thf(zip_derived_cl226, plain,
% 36.43/5.82 (((implies @
% 36.43/5.82 (implies @ (implies @ (or @ truth @ truth) @ (not @ falsehood)) @
% 36.43/5.82 falsehood) @
% 36.43/5.82 falsehood)
% 36.43/5.82 = (implies @ truth @
% 36.43/5.82 (implies @ (or @ truth @ truth) @ (not @ falsehood))))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl176, zip_derived_cl2])).
% 36.43/5.82 thf(zip_derived_cl0, plain, (![X0 : $i]: ((implies @ truth @ X0) = (X0))),
% 36.43/5.82 inference('cnf', [status(esa)], [wajsberg_1])).
% 36.43/5.82 thf(zip_derived_cl235, plain,
% 36.43/5.82 (((implies @
% 36.43/5.82 (implies @ (implies @ (or @ truth @ truth) @ (not @ falsehood)) @
% 36.43/5.82 falsehood) @
% 36.43/5.82 falsehood) = (implies @ (or @ truth @ truth) @ (not @ falsehood)))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl226, zip_derived_cl0])).
% 36.43/5.82 thf(or_commutativity, axiom, (( or @ X @ Y ) = ( or @ Y @ X ))).
% 36.43/5.82 thf(zip_derived_cl6, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((or @ X1 @ X0) = (or @ X0 @ X1))),
% 36.43/5.82 inference('cnf', [status(esa)], [or_commutativity])).
% 36.43/5.82 thf(zip_derived_cl37, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((implies @ X1 @ (implies @ (implies @ X1 @ X0) @ X0)) = (truth))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl26, zip_derived_cl0])).
% 36.43/5.82 thf(zip_derived_cl17, plain,
% 36.43/5.82 (![X0 : $i]: ((or @ truth @ X0) = (implies @ falsehood @ X0))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl15, zip_derived_cl4])).
% 36.43/5.82 thf(zip_derived_cl52, plain,
% 36.43/5.82 (![X0 : $i]:
% 36.43/5.82 ((or @ truth @ (implies @ (implies @ falsehood @ X0) @ X0)) = (truth))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl37, zip_derived_cl17])).
% 36.43/5.82 thf(zip_derived_cl17, plain,
% 36.43/5.82 (![X0 : $i]: ((or @ truth @ X0) = (implies @ falsehood @ X0))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl15, zip_derived_cl4])).
% 36.43/5.82 thf(zip_derived_cl64, plain,
% 36.43/5.82 (![X0 : $i]:
% 36.43/5.82 ((or @ truth @ (implies @ (or @ truth @ X0) @ X0)) = (truth))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl52, zip_derived_cl17])).
% 36.43/5.82 thf(zip_derived_cl79, plain,
% 36.43/5.82 (![X0 : $i]:
% 36.43/5.82 ((or @ truth @ (implies @ (or @ X0 @ truth) @ X0)) = (truth))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl6, zip_derived_cl64])).
% 36.43/5.82 thf(zip_derived_cl0, plain, (![X0 : $i]: ((implies @ truth @ X0) = (X0))),
% 36.43/5.82 inference('cnf', [status(esa)], [wajsberg_1])).
% 36.43/5.82 thf(zip_derived_cl2, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((implies @ (implies @ X1 @ X0) @ X0)
% 36.43/5.82 = (implies @ (implies @ X0 @ X1) @ X1))),
% 36.43/5.82 inference('cnf', [status(esa)], [wajsberg_3])).
% 36.43/5.82 thf(zip_derived_cl195, plain,
% 36.43/5.82 (![X0 : $i]:
% 36.43/5.82 ((implies @ X0 @ X0) = (implies @ (implies @ X0 @ truth) @ truth))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl0, zip_derived_cl2])).
% 36.43/5.82 thf(zip_derived_cl62, plain, (![X0 : $i]: ((truth) = (implies @ X0 @ X0))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl50, zip_derived_cl0])).
% 36.43/5.82 thf(zip_derived_cl209, plain,
% 36.43/5.82 (![X0 : $i]: ((truth) = (implies @ (implies @ X0 @ truth) @ truth))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl195, zip_derived_cl62])).
% 36.43/5.82 thf(zip_derived_cl37, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((implies @ X1 @ (implies @ (implies @ X1 @ X0) @ X0)) = (truth))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl26, zip_derived_cl0])).
% 36.43/5.82 thf(zip_derived_cl251, plain,
% 36.43/5.82 (![X0 : $i]: ((implies @ X0 @ truth) = (truth))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl209, zip_derived_cl37])).
% 36.43/5.82 thf(zip_derived_cl4, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((or @ X0 @ X1) = (implies @ (not @ X0) @ X1))),
% 36.43/5.82 inference('cnf', [status(esa)], [or_definition])).
% 36.43/5.82 thf(zip_derived_cl329, plain, (![X0 : $i]: ((or @ X0 @ truth) = (truth))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl251, zip_derived_cl4])).
% 36.43/5.82 thf(zip_derived_cl0, plain, (![X0 : $i]: ((implies @ truth @ X0) = (X0))),
% 36.43/5.82 inference('cnf', [status(esa)], [wajsberg_1])).
% 36.43/5.82 thf(zip_derived_cl342, plain, (![X0 : $i]: ((or @ truth @ X0) = (truth))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl79, zip_derived_cl329, zip_derived_cl0])).
% 36.43/5.82 thf(zip_derived_cl0, plain, (![X0 : $i]: ((implies @ truth @ X0) = (X0))),
% 36.43/5.82 inference('cnf', [status(esa)], [wajsberg_1])).
% 36.43/5.82 thf(zip_derived_cl4, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((or @ X0 @ X1) = (implies @ (not @ X0) @ X1))),
% 36.43/5.82 inference('cnf', [status(esa)], [or_definition])).
% 36.43/5.82 thf(zip_derived_cl342, plain, (![X0 : $i]: ((or @ truth @ X0) = (truth))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl79, zip_derived_cl329, zip_derived_cl0])).
% 36.43/5.82 thf(zip_derived_cl0, plain, (![X0 : $i]: ((implies @ truth @ X0) = (X0))),
% 36.43/5.82 inference('cnf', [status(esa)], [wajsberg_1])).
% 36.43/5.82 thf(zip_derived_cl467, plain,
% 36.43/5.82 (((implies @ (or @ falsehood @ falsehood) @ falsehood)
% 36.43/5.82 = (not @ falsehood))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl235, zip_derived_cl342, zip_derived_cl0,
% 36.43/5.82 zip_derived_cl4, zip_derived_cl342, zip_derived_cl0])).
% 36.43/5.82 thf(zip_derived_cl0, plain, (![X0 : $i]: ((implies @ truth @ X0) = (X0))),
% 36.43/5.82 inference('cnf', [status(esa)], [wajsberg_1])).
% 36.43/5.82 thf(wajsberg_4, axiom,
% 36.43/5.82 (( implies @ ( implies @ ( not @ X ) @ ( not @ Y ) ) @ ( implies @ Y @ X ) ) =
% 36.43/5.82 ( truth ))).
% 36.43/5.82 thf(zip_derived_cl3, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((implies @ (implies @ (not @ X0) @ (not @ X1)) @ (implies @ X1 @ X0))
% 36.43/5.82 = (truth))),
% 36.43/5.82 inference('cnf', [status(esa)], [wajsberg_4])).
% 36.43/5.82 thf(zip_derived_cl4, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((or @ X0 @ X1) = (implies @ (not @ X0) @ X1))),
% 36.43/5.82 inference('cnf', [status(esa)], [or_definition])).
% 36.43/5.82 thf(zip_derived_cl267, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((implies @ (or @ X0 @ (not @ X1)) @ (implies @ X1 @ X0)) = (truth))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl3, zip_derived_cl4])).
% 36.43/5.82 thf(zip_derived_cl279, plain,
% 36.43/5.82 (![X0 : $i]: ((implies @ (or @ X0 @ (not @ truth)) @ X0) = (truth))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl0, zip_derived_cl267])).
% 36.43/5.82 thf(zip_derived_cl15, plain, (((not @ truth) = (falsehood))),
% 36.43/5.82 inference('cnf', [status(esa)], [false_definition])).
% 36.43/5.82 thf(zip_derived_cl295, plain,
% 36.43/5.82 (![X0 : $i]: ((implies @ (or @ X0 @ falsehood) @ X0) = (truth))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl279, zip_derived_cl15])).
% 36.43/5.82 thf(zip_derived_cl652, plain, (((truth) = (not @ falsehood))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl467, zip_derived_cl295])).
% 36.43/5.82 thf(zip_derived_cl4, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((or @ X0 @ X1) = (implies @ (not @ X0) @ X1))),
% 36.43/5.82 inference('cnf', [status(esa)], [or_definition])).
% 36.43/5.82 thf(zip_derived_cl674, plain,
% 36.43/5.82 (![X0 : $i]: ((or @ falsehood @ X0) = (implies @ truth @ X0))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl652, zip_derived_cl4])).
% 36.43/5.82 thf(zip_derived_cl0, plain, (![X0 : $i]: ((implies @ truth @ X0) = (X0))),
% 36.43/5.82 inference('cnf', [status(esa)], [wajsberg_1])).
% 36.43/5.82 thf(zip_derived_cl683, plain, (![X0 : $i]: ((or @ falsehood @ X0) = (X0))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl674, zip_derived_cl0])).
% 36.43/5.82 thf(zip_derived_cl6, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((or @ X1 @ X0) = (or @ X0 @ X1))),
% 36.43/5.82 inference('cnf', [status(esa)], [or_commutativity])).
% 36.43/5.82 thf(zip_derived_cl706, plain, (![X0 : $i]: ((or @ X0 @ falsehood) = (X0))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl683, zip_derived_cl6])).
% 36.43/5.82 thf(zip_derived_cl815, plain,
% 36.43/5.82 (![X0 : $i]: ((and_star @ X0 @ truth) = (not @ (not @ X0)))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl161, zip_derived_cl706])).
% 36.43/5.82 thf(xor_definition, axiom,
% 36.43/5.82 (( xor @ X @ Y ) =
% 36.43/5.82 ( or @ ( and @ X @ ( not @ Y ) ) @ ( and @ ( not @ X ) @ Y ) ))).
% 36.43/5.82 thf(zip_derived_cl10, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((xor @ X0 @ X1)
% 36.43/5.82 = (or @ (and @ X0 @ (not @ X1)) @ (and @ (not @ X0) @ X1)))),
% 36.43/5.82 inference('cnf', [status(esa)], [xor_definition])).
% 36.43/5.82 thf(and_definition, axiom,
% 36.43/5.82 (( and @ X @ Y ) = ( not @ ( or @ ( not @ X ) @ ( not @ Y ) ) ))).
% 36.43/5.82 thf(zip_derived_cl7, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((and @ X0 @ X1) = (not @ (or @ (not @ X0) @ (not @ X1))))),
% 36.43/5.82 inference('cnf', [status(esa)], [and_definition])).
% 36.43/5.82 thf(zip_derived_cl12, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((and_star @ X0 @ X1) = (not @ (or @ (not @ X0) @ (not @ X1))))),
% 36.43/5.82 inference('cnf', [status(esa)], [and_star_definition])).
% 36.43/5.82 thf(zip_derived_cl153, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((and @ X0 @ X1) = (and_star @ X0 @ X1))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl7, zip_derived_cl12])).
% 36.43/5.82 thf(zip_derived_cl153, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((and @ X0 @ X1) = (and_star @ X0 @ X1))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl7, zip_derived_cl12])).
% 36.43/5.82 thf(zip_derived_cl303, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((xor @ X0 @ X1)
% 36.43/5.82 = (or @ (and_star @ X0 @ (not @ X1)) @ (and_star @ (not @ X0) @ X1)))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl10, zip_derived_cl153, zip_derived_cl153])).
% 36.43/5.82 thf(zip_derived_cl819, plain,
% 36.43/5.82 (![X0 : $i]:
% 36.43/5.82 ((xor @ X0 @ truth)
% 36.43/5.82 = (or @ (and_star @ X0 @ (not @ truth)) @ (not @ (not @ (not @ X0)))))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl815, zip_derived_cl303])).
% 36.43/5.82 thf(zip_derived_cl15, plain, (((not @ truth) = (falsehood))),
% 36.43/5.82 inference('cnf', [status(esa)], [false_definition])).
% 36.43/5.82 thf(zip_derived_cl652, plain, (((truth) = (not @ falsehood))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl467, zip_derived_cl295])).
% 36.43/5.82 thf(zip_derived_cl12, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((and_star @ X0 @ X1) = (not @ (or @ (not @ X0) @ (not @ X1))))),
% 36.43/5.82 inference('cnf', [status(esa)], [and_star_definition])).
% 36.43/5.82 thf(zip_derived_cl680, plain,
% 36.43/5.82 (![X0 : $i]:
% 36.43/5.82 ((and_star @ X0 @ falsehood) = (not @ (or @ (not @ X0) @ truth)))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl652, zip_derived_cl12])).
% 36.43/5.82 thf(zip_derived_cl329, plain, (![X0 : $i]: ((or @ X0 @ truth) = (truth))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl251, zip_derived_cl4])).
% 36.43/5.82 thf(zip_derived_cl15, plain, (((not @ truth) = (falsehood))),
% 36.43/5.82 inference('cnf', [status(esa)], [false_definition])).
% 36.43/5.82 thf(zip_derived_cl685, plain,
% 36.43/5.82 (![X0 : $i]: ((and_star @ X0 @ falsehood) = (falsehood))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl680, zip_derived_cl329, zip_derived_cl15])).
% 36.43/5.82 thf(zip_derived_cl683, plain, (![X0 : $i]: ((or @ falsehood @ X0) = (X0))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl674, zip_derived_cl0])).
% 36.43/5.82 thf(zip_derived_cl823, plain,
% 36.43/5.82 (![X0 : $i]: ((xor @ X0 @ truth) = (not @ (not @ (not @ X0))))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl819, zip_derived_cl15, zip_derived_cl685,
% 36.43/5.82 zip_derived_cl683])).
% 36.43/5.82 thf(zip_derived_cl4, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((or @ X0 @ X1) = (implies @ (not @ X0) @ X1))),
% 36.43/5.82 inference('cnf', [status(esa)], [or_definition])).
% 36.43/5.82 thf(zip_derived_cl17, plain,
% 36.43/5.82 (![X0 : $i]: ((or @ truth @ X0) = (implies @ falsehood @ X0))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl15, zip_derived_cl4])).
% 36.43/5.82 thf(zip_derived_cl342, plain, (![X0 : $i]: ((or @ truth @ X0) = (truth))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl79, zip_derived_cl329, zip_derived_cl0])).
% 36.43/5.82 thf(zip_derived_cl357, plain,
% 36.43/5.82 (![X0 : $i]: ((truth) = (implies @ falsehood @ X0))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl17, zip_derived_cl342])).
% 36.43/5.82 thf(zip_derived_cl2, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((implies @ (implies @ X1 @ X0) @ X0)
% 36.43/5.82 = (implies @ (implies @ X0 @ X1) @ X1))),
% 36.43/5.82 inference('cnf', [status(esa)], [wajsberg_3])).
% 36.43/5.82 thf(zip_derived_cl483, plain,
% 36.43/5.82 (![X0 : $i]:
% 36.43/5.82 ((implies @ (implies @ X0 @ falsehood) @ falsehood)
% 36.43/5.82 = (implies @ truth @ X0))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl357, zip_derived_cl2])).
% 36.43/5.82 thf(zip_derived_cl0, plain, (![X0 : $i]: ((implies @ truth @ X0) = (X0))),
% 36.43/5.82 inference('cnf', [status(esa)], [wajsberg_1])).
% 36.43/5.82 thf(zip_derived_cl493, plain,
% 36.43/5.82 (![X0 : $i]: ((implies @ (implies @ X0 @ falsehood) @ falsehood) = (X0))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl483, zip_derived_cl0])).
% 36.43/5.82 thf(zip_derived_cl1257, plain,
% 36.43/5.82 (![X0 : $i]: ((implies @ (or @ X0 @ falsehood) @ falsehood) = (not @ X0))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl4, zip_derived_cl493])).
% 36.43/5.82 thf(zip_derived_cl706, plain, (![X0 : $i]: ((or @ X0 @ falsehood) = (X0))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl683, zip_derived_cl6])).
% 36.43/5.82 thf(zip_derived_cl1263, plain,
% 36.43/5.82 (![X0 : $i]: ((implies @ X0 @ falsehood) = (not @ X0))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl1257, zip_derived_cl706])).
% 36.43/5.82 thf(zip_derived_cl2, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((implies @ (implies @ X1 @ X0) @ X0)
% 36.43/5.82 = (implies @ (implies @ X0 @ X1) @ X1))),
% 36.43/5.82 inference('cnf', [status(esa)], [wajsberg_3])).
% 36.43/5.82 thf(zip_derived_cl1287, plain,
% 36.43/5.82 (![X0 : $i]:
% 36.43/5.82 ((implies @ (implies @ falsehood @ X0) @ X0)
% 36.43/5.82 = (not @ (implies @ X0 @ falsehood)))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl1263, zip_derived_cl2])).
% 36.43/5.82 thf(zip_derived_cl357, plain,
% 36.43/5.82 (![X0 : $i]: ((truth) = (implies @ falsehood @ X0))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl17, zip_derived_cl342])).
% 36.43/5.82 thf(zip_derived_cl0, plain, (![X0 : $i]: ((implies @ truth @ X0) = (X0))),
% 36.43/5.82 inference('cnf', [status(esa)], [wajsberg_1])).
% 36.43/5.82 thf(zip_derived_cl1263, plain,
% 36.43/5.82 (![X0 : $i]: ((implies @ X0 @ falsehood) = (not @ X0))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl1257, zip_derived_cl706])).
% 36.43/5.82 thf(zip_derived_cl1309, plain, (![X0 : $i]: ((X0) = (not @ (not @ X0)))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl1287, zip_derived_cl357, zip_derived_cl0,
% 36.43/5.82 zip_derived_cl1263])).
% 36.43/5.82 thf(zip_derived_cl1317, plain,
% 36.43/5.82 (![X0 : $i]: ((xor @ X0 @ truth) = (not @ X0))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl823, zip_derived_cl1309])).
% 36.43/5.82 thf(zip_derived_cl1317, plain,
% 36.43/5.82 (![X0 : $i]: ((xor @ X0 @ truth) = (not @ X0))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl823, zip_derived_cl1309])).
% 36.43/5.82 thf(zip_derived_cl1547, plain,
% 36.43/5.82 (((and_star @ y @ (xor @ truth @ (and_star @ y @ (not @ x))))
% 36.43/5.82 != (and_star @ x @ (xor @ truth @ (and_star @ x @ (not @ y)))))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl19, zip_derived_cl1317, zip_derived_cl1317])).
% 36.43/5.82 thf(zip_derived_cl815, plain,
% 36.43/5.82 (![X0 : $i]: ((and_star @ X0 @ truth) = (not @ (not @ X0)))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl161, zip_derived_cl706])).
% 36.43/5.82 thf(zip_derived_cl14, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((and_star @ X1 @ X0) = (and_star @ X0 @ X1))),
% 36.43/5.82 inference('cnf', [status(esa)], [and_star_commutativity])).
% 36.43/5.82 thf(zip_derived_cl817, plain,
% 36.43/5.82 (![X0 : $i]: ((and_star @ truth @ X0) = (not @ (not @ X0)))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl815, zip_derived_cl14])).
% 36.43/5.82 thf(zip_derived_cl303, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((xor @ X0 @ X1)
% 36.43/5.82 = (or @ (and_star @ X0 @ (not @ X1)) @ (and_star @ (not @ X0) @ X1)))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl10, zip_derived_cl153, zip_derived_cl153])).
% 36.43/5.82 thf(zip_derived_cl831, plain,
% 36.43/5.82 (![X0 : $i]:
% 36.43/5.82 ((xor @ truth @ X0)
% 36.43/5.82 = (or @ (not @ (not @ (not @ X0))) @ (and_star @ (not @ truth) @ X0)))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl817, zip_derived_cl303])).
% 36.43/5.82 thf(zip_derived_cl15, plain, (((not @ truth) = (falsehood))),
% 36.43/5.82 inference('cnf', [status(esa)], [false_definition])).
% 36.43/5.82 thf(zip_derived_cl652, plain, (((truth) = (not @ falsehood))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl467, zip_derived_cl295])).
% 36.43/5.82 thf(zip_derived_cl12, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((and_star @ X0 @ X1) = (not @ (or @ (not @ X0) @ (not @ X1))))),
% 36.43/5.82 inference('cnf', [status(esa)], [and_star_definition])).
% 36.43/5.82 thf(zip_derived_cl675, plain,
% 36.43/5.82 (![X0 : $i]:
% 36.43/5.82 ((and_star @ falsehood @ X0) = (not @ (or @ truth @ (not @ X0))))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl652, zip_derived_cl12])).
% 36.43/5.82 thf(zip_derived_cl342, plain, (![X0 : $i]: ((or @ truth @ X0) = (truth))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl79, zip_derived_cl329, zip_derived_cl0])).
% 36.43/5.82 thf(zip_derived_cl15, plain, (((not @ truth) = (falsehood))),
% 36.43/5.82 inference('cnf', [status(esa)], [false_definition])).
% 36.43/5.82 thf(zip_derived_cl684, plain,
% 36.43/5.82 (![X0 : $i]: ((and_star @ falsehood @ X0) = (falsehood))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl675, zip_derived_cl342, zip_derived_cl15])).
% 36.43/5.82 thf(zip_derived_cl706, plain, (![X0 : $i]: ((or @ X0 @ falsehood) = (X0))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl683, zip_derived_cl6])).
% 36.43/5.82 thf(zip_derived_cl836, plain,
% 36.43/5.82 (![X0 : $i]: ((xor @ truth @ X0) = (not @ (not @ (not @ X0))))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl831, zip_derived_cl15, zip_derived_cl684,
% 36.43/5.82 zip_derived_cl706])).
% 36.43/5.82 thf(zip_derived_cl1309, plain, (![X0 : $i]: ((X0) = (not @ (not @ X0)))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl1287, zip_derived_cl357, zip_derived_cl0,
% 36.43/5.82 zip_derived_cl1263])).
% 36.43/5.82 thf(zip_derived_cl1318, plain,
% 36.43/5.82 (![X0 : $i]: ((xor @ truth @ X0) = (not @ X0))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl836, zip_derived_cl1309])).
% 36.43/5.82 thf(zip_derived_cl1318, plain,
% 36.43/5.82 (![X0 : $i]: ((xor @ truth @ X0) = (not @ X0))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl836, zip_derived_cl1309])).
% 36.43/5.82 thf(zip_derived_cl1579, plain,
% 36.43/5.82 (((and_star @ y @ (not @ (and_star @ y @ (not @ x))))
% 36.43/5.82 != (and_star @ x @ (not @ (and_star @ x @ (not @ y)))))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl1547, zip_derived_cl1318, zip_derived_cl1318])).
% 36.43/5.82 thf(zip_derived_cl12, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((and_star @ X0 @ X1) = (not @ (or @ (not @ X0) @ (not @ X1))))),
% 36.43/5.82 inference('cnf', [status(esa)], [and_star_definition])).
% 36.43/5.82 thf(zip_derived_cl823, plain,
% 36.43/5.82 (![X0 : $i]: ((xor @ X0 @ truth) = (not @ (not @ (not @ X0))))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl819, zip_derived_cl15, zip_derived_cl685,
% 36.43/5.82 zip_derived_cl683])).
% 36.43/5.82 thf(zip_derived_cl836, plain,
% 36.43/5.82 (![X0 : $i]: ((xor @ truth @ X0) = (not @ (not @ (not @ X0))))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl831, zip_derived_cl15, zip_derived_cl684,
% 36.43/5.82 zip_derived_cl706])).
% 36.43/5.82 thf(zip_derived_cl1060, plain,
% 36.43/5.82 (![X0 : $i]: ((xor @ truth @ (not @ X0)) = (not @ (xor @ X0 @ truth)))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl823, zip_derived_cl836])).
% 36.43/5.82 thf(zip_derived_cl1317, plain,
% 36.43/5.82 (![X0 : $i]: ((xor @ X0 @ truth) = (not @ X0))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl823, zip_derived_cl1309])).
% 36.43/5.82 thf(zip_derived_cl1309, plain, (![X0 : $i]: ((X0) = (not @ (not @ X0)))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl1287, zip_derived_cl357, zip_derived_cl0,
% 36.43/5.82 zip_derived_cl1263])).
% 36.43/5.82 thf(zip_derived_cl1550, plain,
% 36.43/5.82 (![X0 : $i]: ((xor @ truth @ (not @ X0)) = (X0))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl1060, zip_derived_cl1317, zip_derived_cl1309])).
% 36.43/5.82 thf(zip_derived_cl1660, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((xor @ truth @ (and_star @ X1 @ X0)) = (or @ (not @ X1) @ (not @ X0)))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl12, zip_derived_cl1550])).
% 36.43/5.82 thf(zip_derived_cl1318, plain,
% 36.43/5.82 (![X0 : $i]: ((xor @ truth @ X0) = (not @ X0))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl836, zip_derived_cl1309])).
% 36.43/5.82 thf(zip_derived_cl1663, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((not @ (and_star @ X1 @ X0)) = (or @ (not @ X1) @ (not @ X0)))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl1660, zip_derived_cl1318])).
% 36.43/5.82 thf(zip_derived_cl1309, plain, (![X0 : $i]: ((X0) = (not @ (not @ X0)))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl1287, zip_derived_cl357, zip_derived_cl0,
% 36.43/5.82 zip_derived_cl1263])).
% 36.43/5.82 thf(zip_derived_cl4, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((or @ X0 @ X1) = (implies @ (not @ X0) @ X1))),
% 36.43/5.82 inference('cnf', [status(esa)], [or_definition])).
% 36.43/5.82 thf(zip_derived_cl1319, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((or @ (not @ X0) @ X1) = (implies @ X0 @ X1))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl1309, zip_derived_cl4])).
% 36.43/5.82 thf(zip_derived_cl2892, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((not @ (and_star @ X1 @ X0)) = (implies @ X1 @ (not @ X0)))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl1663, zip_derived_cl1319])).
% 36.43/5.82 thf(zip_derived_cl1309, plain, (![X0 : $i]: ((X0) = (not @ (not @ X0)))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl1287, zip_derived_cl357, zip_derived_cl0,
% 36.43/5.82 zip_derived_cl1263])).
% 36.43/5.82 thf(zip_derived_cl2892, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((not @ (and_star @ X1 @ X0)) = (implies @ X1 @ (not @ X0)))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl1663, zip_derived_cl1319])).
% 36.43/5.82 thf(zip_derived_cl1309, plain, (![X0 : $i]: ((X0) = (not @ (not @ X0)))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl1287, zip_derived_cl357, zip_derived_cl0,
% 36.43/5.82 zip_derived_cl1263])).
% 36.43/5.82 thf(zip_derived_cl2893, plain,
% 36.43/5.82 (((and_star @ y @ (implies @ y @ x))
% 36.43/5.82 != (and_star @ x @ (implies @ x @ y)))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl1579, zip_derived_cl2892, zip_derived_cl1309,
% 36.43/5.82 zip_derived_cl2892, zip_derived_cl1309])).
% 36.43/5.82 thf(zip_derived_cl4, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((or @ X0 @ X1) = (implies @ (not @ X0) @ X1))),
% 36.43/5.82 inference('cnf', [status(esa)], [or_definition])).
% 36.43/5.82 thf(zip_derived_cl2, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((implies @ (implies @ X1 @ X0) @ X0)
% 36.43/5.82 = (implies @ (implies @ X0 @ X1) @ X1))),
% 36.43/5.82 inference('cnf', [status(esa)], [wajsberg_3])).
% 36.43/5.82 thf(zip_derived_cl196, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((implies @ (or @ X1 @ X0) @ X0)
% 36.43/5.82 = (implies @ (implies @ X0 @ (not @ X1)) @ (not @ X1)))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl4, zip_derived_cl2])).
% 36.43/5.82 thf(zip_derived_cl12, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((and_star @ X0 @ X1) = (not @ (or @ (not @ X0) @ (not @ X1))))),
% 36.43/5.82 inference('cnf', [status(esa)], [and_star_definition])).
% 36.43/5.82 thf(zip_derived_cl1319, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((or @ (not @ X0) @ X1) = (implies @ X0 @ X1))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl1309, zip_derived_cl4])).
% 36.43/5.82 thf(zip_derived_cl1742, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((and_star @ X0 @ X1) = (not @ (implies @ X0 @ (not @ X1))))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl12, zip_derived_cl1319])).
% 36.43/5.82 thf(zip_derived_cl7290, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((and_star @ (or @ X0 @ (not @ X1)) @ X1)
% 36.43/5.82 = (not @
% 36.43/5.82 (implies @ (implies @ (not @ X1) @ (not @ X0)) @ (not @ X0))))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl196, zip_derived_cl1742])).
% 36.43/5.82 thf(zip_derived_cl1319, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((or @ (not @ X0) @ X1) = (implies @ X0 @ X1))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl1309, zip_derived_cl4])).
% 36.43/5.82 thf(zip_derived_cl6, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((or @ X1 @ X0) = (or @ X0 @ X1))),
% 36.43/5.82 inference('cnf', [status(esa)], [or_commutativity])).
% 36.43/5.82 thf(zip_derived_cl1744, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((or @ X0 @ (not @ X1)) = (implies @ X1 @ X0))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl1319, zip_derived_cl6])).
% 36.43/5.82 thf(zip_derived_cl14, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((and_star @ X1 @ X0) = (and_star @ X0 @ X1))),
% 36.43/5.82 inference('cnf', [status(esa)], [and_star_commutativity])).
% 36.43/5.82 thf(zip_derived_cl1309, plain, (![X0 : $i]: ((X0) = (not @ (not @ X0)))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl1287, zip_derived_cl357, zip_derived_cl0,
% 36.43/5.82 zip_derived_cl1263])).
% 36.43/5.82 thf(zip_derived_cl1744, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((or @ X0 @ (not @ X1)) = (implies @ X1 @ X0))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl1319, zip_derived_cl6])).
% 36.43/5.82 thf(zip_derived_cl1319, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]: ((or @ (not @ X0) @ X1) = (implies @ X0 @ X1))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl1309, zip_derived_cl4])).
% 36.43/5.82 thf(zip_derived_cl1784, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((implies @ X1 @ (not @ X0)) = (implies @ X0 @ (not @ X1)))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl1744, zip_derived_cl1319])).
% 36.43/5.82 thf(zip_derived_cl2191, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((implies @ X1 @ X0) = (implies @ (not @ X0) @ (not @ X1)))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl1309, zip_derived_cl1784])).
% 36.43/5.82 thf(zip_derived_cl1784, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((implies @ X1 @ (not @ X0)) = (implies @ X0 @ (not @ X1)))),
% 36.43/5.82 inference('sup+', [status(thm)], [zip_derived_cl1744, zip_derived_cl1319])).
% 36.43/5.82 thf(zip_derived_cl1742, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((and_star @ X0 @ X1) = (not @ (implies @ X0 @ (not @ X1))))),
% 36.43/5.82 inference('demod', [status(thm)], [zip_derived_cl12, zip_derived_cl1319])).
% 36.43/5.82 thf(zip_derived_cl7476, plain,
% 36.43/5.82 (![X0 : $i, X1 : $i]:
% 36.43/5.82 ((and_star @ X1 @ (implies @ X1 @ X0))
% 36.43/5.82 = (and_star @ X0 @ (implies @ X0 @ X1)))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl7290, zip_derived_cl1744, zip_derived_cl14,
% 36.43/5.82 zip_derived_cl2191, zip_derived_cl1784, zip_derived_cl1742])).
% 36.43/5.82 thf(zip_derived_cl17462, plain,
% 36.43/5.82 (((and_star @ y @ (implies @ y @ x))
% 36.43/5.82 != (and_star @ y @ (implies @ y @ x)))),
% 36.43/5.82 inference('demod', [status(thm)],
% 36.43/5.82 [zip_derived_cl2893, zip_derived_cl7476])).
% 36.43/5.82 thf(zip_derived_cl17463, plain, ($false),
% 36.43/5.82 inference('simplify', [status(thm)], [zip_derived_cl17462])).
% 36.43/5.82
% 36.43/5.82 % SZS output end Refutation
% 36.43/5.82
% 36.43/5.82
% 36.43/5.82 % /export/starexec/sandbox/solver/bin/fo/fo1_lcnf.sh running for 50s
% 36.43/5.82 % Terminating...
% 36.43/5.87 % Runner terminated.
% 36.43/5.89 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------