%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : HWV068-1 : TPTP v9.2.0. Bugfixed v5.5.1.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.l2bb0Gh4qq true
% Computer : n020.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 04:37:48 PM UTC 2025
% Result : Unsatisfiable 280.06s 41.12s
% Output : Refutation 280.06s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : HWV068-1 : TPTP v9.2.0. Bugfixed v5.5.1.
% 0.06/0.13 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.l2bb0Gh4qq true
% 0.13/0.34 % Computer : n020.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Oct 1 11:27:53 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.13/0.34 % Running portfolio for 300 s
% 0.13/0.34 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.35 % Number of cores: 8
% 0.13/0.35 % Python version: Python 3.6.8
% 0.13/0.35 % Running in FO mode
% 0.54/0.68 % Total configuration time : 435
% 0.54/0.68 % Estimated wc time : 1092
% 0.54/0.68 % Estimated cpu time (7 cpus) : 156.0
% 0.54/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.54/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.54/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.54/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.54/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.55/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.55/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 20.39/3.56 % /export/starexec/sandbox2/solver/bin/fo/fo1_lcnf.sh running for 50s
% 20.39/3.58 % /export/starexec/sandbox2/solver/bin/fo/fo17_bce.sh running for 50s
% 280.06/41.12 % Solved by fo/fo17_bce.sh.
% 280.06/41.12 % BCE start: 49913
% 280.06/41.12 % BCE eliminated: 0
% 280.06/41.12 % PE start: 49913
% 280.06/41.12 logic: eq
% 280.06/41.12 % PE eliminated: 21197
% 280.06/41.12 % done 6743 iterations in 37.514s
% 280.06/41.12 % SZS status Unsatisfiable for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 280.06/41.12 % SZS output start Refutation
% 280.06/41.12 thf(esk16333_4_type, type, esk16333_4: $i > $i > $i > $i > $o).
% 280.06/41.12 thf(p_type, type, p: $i > $o).
% 280.06/41.12 thf(esk16220_4_type, type, esk16220_4: $i > $i > $i > $i > $o).
% 280.06/41.12 thf(esk16222_4_type, type, esk16222_4: $i > $i > $i > $i > $o).
% 280.06/41.12 thf(esk16569_4_type, type, esk16569_4: $i > $i > $i > $i > $o).
% 280.06/41.12 thf(esk17147_4_type, type, esk17147_4: $i > $i > $i > $i > $o).
% 280.06/41.12 thf(esk17157_4_type, type, esk17157_4: $i > $i > $i > $i > $o).
% 280.06/41.12 thf(esk16348_4_type, type, esk16348_4: $i > $i > $i > $i > $o).
% 280.06/41.12 thf(esk16221_4_type, type, esk16221_4: $i > $i > $i > $i > $o).
% 280.06/41.12 thf(esk17148_4_type, type, esk17148_4: $i > $i > $i > $i > $o).
% 280.06/41.12 thf(esk1_0_type, type, esk1_0: $o).
% 280.06/41.12 thf(esk2_0_type, type, esk2_0: $o).
% 280.06/41.12 thf(esk16516_4_type, type, esk16516_4: $i > $i > $i > $i > $o).
% 280.06/41.12 thf(esk16349_4_type, type, esk16349_4: $i > $i > $i > $i > $o).
% 280.06/41.12 thf(esk16347_4_type, type, esk16347_4: $i > $i > $i > $i > $o).
% 280.06/41.12 thf(esk16219_4_type, type, esk16219_4: $i > $i > $i > $i > $o).
% 280.06/41.12 thf(esk17504_4_type, type, esk17504_4: $i > $i > $i > $i > $o).
% 280.06/41.12 thf(true_type, type, true: $i).
% 280.06/41.12 thf(esk17564_4_type, type, esk17564_4: $i > $i > $i > $i > $o).
% 280.06/41.12 thf(i_0_45914, axiom,
% 280.06/41.12 (( ~( esk17147_4 @ X1 @ X2 @ X3 @ X4 ) ) |
% 280.06/41.12 ( esk16222_4 @ X1 @ X2 @ X3 @ X4 ))).
% 280.06/41.12 thf(zip_derived_cl45913, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 (~ (esk17147_4 @ X0 @ X1 @ X2 @ X3)
% 280.06/41.12 | (esk16222_4 @ X0 @ X1 @ X2 @ X3))),
% 280.06/41.12 inference('cnf', [status(esa)], [i_0_45914])).
% 280.06/41.12 thf(i_0_33259, axiom,
% 280.06/41.12 (( esk16221_4 @ X1 @ X2 @ X3 @ X4 ) | ( esk16220_4 @ X1 @ X2 @ X3 @ X4 ) |
% 280.06/41.12 ( ~( esk16222_4 @ X1 @ X2 @ X3 @ X4 ) ))).
% 280.06/41.12 thf(zip_derived_cl33258, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 ( (esk16221_4 @ X0 @ X1 @ X2 @ X3)
% 280.06/41.12 | (esk16220_4 @ X0 @ X1 @ X2 @ X3)
% 280.06/41.12 | ~ (esk16222_4 @ X0 @ X1 @ X2 @ X3))),
% 280.06/41.12 inference('cnf', [status(esa)], [i_0_33259])).
% 280.06/41.12 thf(zip_derived_cl316858, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 (~ (esk17147_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | (esk16220_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | (esk16221_4 @ X3 @ X2 @ X1 @ X0))),
% 280.06/41.12 inference('dp-resolution', [status(thm)],
% 280.06/41.12 [zip_derived_cl45913, zip_derived_cl33258])).
% 280.06/41.12 thf(i_0_40910, axiom,
% 280.06/41.12 (( esk16569_4 @ X1 @ X2 @ X3 @ X4 ) |
% 280.06/41.12 ( ~( esk16221_4 @ X1 @ X2 @ X3 @ X4 ) ))).
% 280.06/41.12 thf(zip_derived_cl40909, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 ( (esk16569_4 @ X0 @ X1 @ X2 @ X3)
% 280.06/41.12 | ~ (esk16221_4 @ X0 @ X1 @ X2 @ X3))),
% 280.06/41.12 inference('cnf', [status(esa)], [i_0_40910])).
% 280.06/41.12 thf(zip_derived_cl323576, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 ( (esk16220_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | ~ (esk17147_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | (esk16569_4 @ X3 @ X2 @ X1 @ X0))),
% 280.06/41.12 inference('dp-resolution', [status(thm)],
% 280.06/41.12 [zip_derived_cl316858, zip_derived_cl40909])).
% 280.06/41.12 thf(i_0_47728, axiom,
% 280.06/41.12 (( esk16349_4 @ X1 @ X2 @ X3 @ X4 ) |
% 280.06/41.12 ( ~( esk16220_4 @ X1 @ X2 @ X3 @ X4 ) ))).
% 280.06/41.12 thf(zip_derived_cl47727, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 ( (esk16349_4 @ X0 @ X1 @ X2 @ X3)
% 280.06/41.12 | ~ (esk16220_4 @ X0 @ X1 @ X2 @ X3))),
% 280.06/41.12 inference('cnf', [status(esa)], [i_0_47728])).
% 280.06/41.12 thf(i_0_25870, axiom,
% 280.06/41.12 (( ~( esk16349_4 @ X1 @ X2 @ X3 @ X4 ) ) |
% 280.06/41.12 ( esk16348_4 @ X1 @ X2 @ X3 @ X4 ) | ( esk16347_4 @ X1 @ X2 @ X3 @ X4 ))).
% 280.06/41.12 thf(zip_derived_cl25869, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 (~ (esk16349_4 @ X0 @ X1 @ X2 @ X3)
% 280.06/41.12 | (esk16348_4 @ X0 @ X1 @ X2 @ X3)
% 280.06/41.12 | (esk16347_4 @ X0 @ X1 @ X2 @ X3))),
% 280.06/41.12 inference('cnf', [status(esa)], [i_0_25870])).
% 280.06/41.12 thf(zip_derived_cl320475, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 (~ (esk16220_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | (esk16347_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | (esk16348_4 @ X3 @ X2 @ X1 @ X0))),
% 280.06/41.12 inference('dp-resolution', [status(thm)],
% 280.06/41.12 [zip_derived_cl47727, zip_derived_cl25869])).
% 280.06/41.12 thf(i_0_26220, axiom,
% 280.06/41.12 (( esk17148_4 @ X1 @ X2 @ X3 @ X4 ) |
% 280.06/41.12 ( ~( esk16347_4 @ X1 @ X2 @ X3 @ X4 ) ))).
% 280.06/41.12 thf(zip_derived_cl26219, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 ( (esk17148_4 @ X0 @ X1 @ X2 @ X3)
% 280.06/41.12 | ~ (esk16347_4 @ X0 @ X1 @ X2 @ X3))),
% 280.06/41.12 inference('cnf', [status(esa)], [i_0_26220])).
% 280.06/41.12 thf(zip_derived_cl330291, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 ( (esk16348_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | ~ (esk16220_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | (esk17148_4 @ X3 @ X2 @ X1 @ X0))),
% 280.06/41.12 inference('dp-resolution', [status(thm)],
% 280.06/41.12 [zip_derived_cl320475, zip_derived_cl26219])).
% 280.06/41.12 thf(i_0_32779, axiom,
% 280.06/41.12 (( ~( esk16348_4 @ X1 @ X2 @ X3 @ X4 ) ) |
% 280.06/41.12 ( esk17504_4 @ X1 @ X2 @ X3 @ X4 ))).
% 280.06/41.12 thf(zip_derived_cl32778, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 (~ (esk16348_4 @ X0 @ X1 @ X2 @ X3)
% 280.06/41.12 | (esk17504_4 @ X0 @ X1 @ X2 @ X3))),
% 280.06/41.12 inference('cnf', [status(esa)], [i_0_32779])).
% 280.06/41.12 thf(zip_derived_cl349018, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 ( (esk17148_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | ~ (esk16220_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | (esk17504_4 @ X3 @ X2 @ X1 @ X0))),
% 280.06/41.12 inference('dp-resolution', [status(thm)],
% 280.06/41.12 [zip_derived_cl330291, zip_derived_cl32778])).
% 280.06/41.12 thf(zip_derived_cl367637, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 ( (esk16569_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | ~ (esk17147_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | (esk17504_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | (esk17148_4 @ X3 @ X2 @ X1 @ X0))),
% 280.06/41.12 inference('dp-resolution', [status(thm)],
% 280.06/41.12 [zip_derived_cl323576, zip_derived_cl349018])).
% 280.06/41.12 thf(zip_derived_cl316858, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 (~ (esk17147_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | (esk16220_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | (esk16221_4 @ X3 @ X2 @ X1 @ X0))),
% 280.06/41.12 inference('dp-resolution', [status(thm)],
% 280.06/41.12 [zip_derived_cl45913, zip_derived_cl33258])).
% 280.06/41.12 thf(i_0_41865, axiom,
% 280.06/41.12 (( ~( esk16221_4 @ X1 @ X2 @ X3 @ X4 ) ) |
% 280.06/41.12 ( esk17157_4 @ X1 @ X2 @ X3 @ X4 ))).
% 280.06/41.12 thf(zip_derived_cl41864, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 (~ (esk16221_4 @ X0 @ X1 @ X2 @ X3)
% 280.06/41.12 | (esk17157_4 @ X0 @ X1 @ X2 @ X3))),
% 280.06/41.12 inference('cnf', [status(esa)], [i_0_41865])).
% 280.06/41.12 thf(zip_derived_cl323577, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 ( (esk16220_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | ~ (esk17147_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | (esk17157_4 @ X3 @ X2 @ X1 @ X0))),
% 280.06/41.12 inference('dp-resolution', [status(thm)],
% 280.06/41.12 [zip_derived_cl316858, zip_derived_cl41864])).
% 280.06/41.12 thf(i_0_7619, axiom,
% 280.06/41.12 (( ~( esk16220_4 @ X1 @ X2 @ X3 @ X4 ) ) |
% 280.06/41.12 ( esk16219_4 @ X1 @ X2 @ X3 @ X4 ))).
% 280.06/41.12 thf(zip_derived_cl7618, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 (~ (esk16220_4 @ X0 @ X1 @ X2 @ X3)
% 280.06/41.12 | (esk16219_4 @ X0 @ X1 @ X2 @ X3))),
% 280.06/41.12 inference('cnf', [status(esa)], [i_0_7619])).
% 280.06/41.12 thf(i_0_40536, axiom,
% 280.06/41.12 (( ~( esk16219_4 @ X1 @ X2 @ X3 @ X4 ) ) |
% 280.06/41.12 ( ~( esk16569_4 @ X1 @ X2 @ X3 @ X4 ) ))).
% 280.06/41.12 thf(zip_derived_cl40535, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 (~ (esk16219_4 @ X0 @ X1 @ X2 @ X3)
% 280.06/41.12 | ~ (esk16569_4 @ X0 @ X1 @ X2 @ X3))),
% 280.06/41.12 inference('cnf', [status(esa)], [i_0_40536])).
% 280.06/41.12 thf(zip_derived_cl306746, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 (~ (esk16220_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | ~ (esk16569_4 @ X3 @ X2 @ X1 @ X0))),
% 280.06/41.12 inference('dp-resolution', [status(thm)],
% 280.06/41.12 [zip_derived_cl7618, zip_derived_cl40535])).
% 280.06/41.12 thf(zip_derived_cl367640, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 ( (esk17157_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | ~ (esk17147_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | ~ (esk16569_4 @ X3 @ X2 @ X1 @ X0))),
% 280.06/41.12 inference('dp-resolution', [status(thm)],
% 280.06/41.12 [zip_derived_cl323577, zip_derived_cl306746])).
% 280.06/41.12 thf(i_0_3266, axiom,
% 280.06/41.12 (( esk16516_4 @ X1 @ X2 @ X3 @ X4 ) |
% 280.06/41.12 ( ~( esk17157_4 @ X1 @ X2 @ X3 @ X4 ) ))).
% 280.06/41.12 thf(zip_derived_cl3265, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 ( (esk16516_4 @ X0 @ X1 @ X2 @ X3)
% 280.06/41.12 | ~ (esk17157_4 @ X0 @ X1 @ X2 @ X3))),
% 280.06/41.12 inference('cnf', [status(esa)], [i_0_3266])).
% 280.06/41.12 thf(i_0_21184, axiom, (~( esk16516_4 @ X1 @ X2 @ X3 @ X4 ))).
% 280.06/41.12 thf(zip_derived_cl21183, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 ~ (esk16516_4 @ X0 @ X1 @ X2 @ X3)),
% 280.06/41.12 inference('cnf', [status(esa)], [i_0_21184])).
% 280.06/41.12 thf(zip_derived_cl553356, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 ~ (esk17157_4 @ X0 @ X1 @ X2 @ X3)),
% 280.06/41.12 inference('demod', [status(thm)],
% 280.06/41.12 [zip_derived_cl3265, zip_derived_cl21183])).
% 280.06/41.12 thf(zip_derived_cl559527, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 (~ (esk16569_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | ~ (esk17147_4 @ X3 @ X2 @ X1 @ X0))),
% 280.06/41.12 inference('clc', [status(thm)],
% 280.06/41.12 [zip_derived_cl367640, zip_derived_cl553356])).
% 280.06/41.12 thf(zip_derived_cl563681, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 ( (esk17148_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | (esk17504_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | ~ (esk17147_4 @ X3 @ X2 @ X1 @ X0))),
% 280.06/41.12 inference('clc', [status(thm)],
% 280.06/41.12 [zip_derived_cl367637, zip_derived_cl559527])).
% 280.06/41.12 thf(i_0_22074, axiom,
% 280.06/41.12 (( esk17564_4 @ X1 @ X2 @ X3 @ X4 ) |
% 280.06/41.12 ( ~( esk17148_4 @ X1 @ X2 @ X3 @ X4 ) ))).
% 280.06/41.12 thf(zip_derived_cl22073, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 ( (esk17564_4 @ X0 @ X1 @ X2 @ X3)
% 280.06/41.12 | ~ (esk17148_4 @ X0 @ X1 @ X2 @ X3))),
% 280.06/41.12 inference('cnf', [status(esa)], [i_0_22074])).
% 280.06/41.12 thf(zip_derived_cl563682, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 (~ (esk17147_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | (esk17504_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | (esk17564_4 @ X3 @ X2 @ X1 @ X0))),
% 280.06/41.12 inference('s_sup-', [status(thm)],
% 280.06/41.12 [zip_derived_cl563681, zip_derived_cl22073])).
% 280.06/41.12 thf(i_0_20513, axiom,
% 280.06/41.12 (( ~( esk17504_4 @ X1 @ X2 @ X3 @ X4 ) ) |
% 280.06/41.12 ( esk16333_4 @ X1 @ X2 @ X3 @ X4 ))).
% 280.06/41.12 thf(zip_derived_cl20512, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 (~ (esk17504_4 @ X0 @ X1 @ X2 @ X3)
% 280.06/41.12 | (esk16333_4 @ X0 @ X1 @ X2 @ X3))),
% 280.06/41.12 inference('cnf', [status(esa)], [i_0_20513])).
% 280.06/41.12 thf(zip_derived_cl563689, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 ( (esk17564_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | ~ (esk17147_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | (esk16333_4 @ X3 @ X2 @ X1 @ X0))),
% 280.06/41.12 inference('s_sup-', [status(thm)],
% 280.06/41.12 [zip_derived_cl563682, zip_derived_cl20512])).
% 280.06/41.12 thf(i_0_14736, axiom,
% 280.06/41.12 (( ~( p @ X3 ) ) | ( ~( esk16333_4 @ X1 @ X2 @ X3 @ X4 ) ) |
% 280.06/41.12 ( ~( p @ X2 ) ) | ( esk1_0 ) | ( ~( p @ X1 ) ) | ( ~( p @ X4 ) ))).
% 280.06/41.12 thf(zip_derived_cl14735, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 (~ (p @ X0)
% 280.06/41.12 | ~ (esk16333_4 @ X1 @ X2 @ X0 @ X3)
% 280.06/41.12 | ~ (p @ X2)
% 280.06/41.12 | (esk1_0)
% 280.06/41.12 | ~ (p @ X1)
% 280.06/41.12 | ~ (p @ X3))),
% 280.06/41.12 inference('cnf', [status(esa)], [i_0_14736])).
% 280.06/41.12 thf(i_0_37238, axiom, (~( esk1_0 ))).
% 280.06/41.12 thf(zip_derived_cl37237, plain, (~ (esk1_0)),
% 280.06/41.12 inference('cnf', [status(esa)], [i_0_37238])).
% 280.06/41.12 thf(zip_derived_cl553498, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 (~ (p @ X0)
% 280.06/41.12 | ~ (esk16333_4 @ X1 @ X2 @ X0 @ X3)
% 280.06/41.12 | ~ (p @ X2)
% 280.06/41.12 | ~ (p @ X1)
% 280.06/41.12 | ~ (p @ X3))),
% 280.06/41.12 inference('demod', [status(thm)],
% 280.06/41.12 [zip_derived_cl14735, zip_derived_cl37237])).
% 280.06/41.12 thf(zip_derived_cl563693, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 (~ (esk17147_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | (esk17564_4 @ X3 @ X2 @ X1 @ X0)
% 280.06/41.12 | ~ (p @ X1)
% 280.06/41.12 | ~ (p @ X2)
% 280.06/41.12 | ~ (p @ X3)
% 280.06/41.12 | ~ (p @ X0))),
% 280.06/41.12 inference('s_sup-', [status(thm)],
% 280.06/41.12 [zip_derived_cl563689, zip_derived_cl553498])).
% 280.06/41.12 thf(i_0_34555, axiom,
% 280.06/41.12 (( ~( p @ X1 ) ) | ( ~( p @ X3 ) ) | ( ~( p @ X4 ) ) |
% 280.06/41.12 ( esk17147_4 @ X1 @ X2 @ X3 @ X4 ) | ( ~( esk2_0 ) ) | ( ~( p @ X2 ) ))).
% 280.06/41.12 thf(zip_derived_cl34554, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 (~ (p @ X0)
% 280.06/41.12 | ~ (p @ X1)
% 280.06/41.12 | ~ (p @ X2)
% 280.06/41.12 | (esk17147_4 @ X0 @ X3 @ X1 @ X2)
% 280.06/41.12 | ~ (esk2_0)
% 280.06/41.12 | ~ (p @ X3))),
% 280.06/41.12 inference('cnf', [status(esa)], [i_0_34555])).
% 280.06/41.12 thf(i_0_4556, axiom, (esk2_0)).
% 280.06/41.12 thf(zip_derived_cl4555, plain, ( (esk2_0)),
% 280.06/41.12 inference('cnf', [status(esa)], [i_0_4556])).
% 280.06/41.12 thf(zip_derived_cl554280, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 (~ (p @ X0)
% 280.06/41.12 | ~ (p @ X1)
% 280.06/41.12 | ~ (p @ X2)
% 280.06/41.12 | (esk17147_4 @ X0 @ X3 @ X1 @ X2)
% 280.06/41.12 | ~ (p @ X3))),
% 280.06/41.12 inference('demod', [status(thm)],
% 280.06/41.12 [zip_derived_cl34554, zip_derived_cl4555])).
% 280.06/41.12 thf(zip_derived_cl563698, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 (~ (p @ X0)
% 280.06/41.12 | ~ (p @ X3)
% 280.06/41.12 | ~ (p @ X2)
% 280.06/41.12 | ~ (p @ X1)
% 280.06/41.12 | (esk17564_4 @ X3 @ X2 @ X1 @ X0))),
% 280.06/41.12 inference('clc', [status(thm)],
% 280.06/41.12 [zip_derived_cl563693, zip_derived_cl554280])).
% 280.06/41.12 thf(i_0_43176, axiom,
% 280.06/41.12 (( ~( p @ X4 ) ) | ( esk1_0 ) | ( ~( p @ X1 ) ) |
% 280.06/41.12 ( ~( esk17564_4 @ X1 @ X2 @ X3 @ X4 ) ) | ( ~( p @ X3 ) ) |
% 280.06/41.12 ( ~( p @ X2 ) ))).
% 280.06/41.12 thf(zip_derived_cl43175, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 (~ (p @ X0)
% 280.06/41.12 | (esk1_0)
% 280.06/41.12 | ~ (p @ X1)
% 280.06/41.12 | ~ (esk17564_4 @ X1 @ X2 @ X3 @ X0)
% 280.06/41.12 | ~ (p @ X3)
% 280.06/41.12 | ~ (p @ X2))),
% 280.06/41.12 inference('cnf', [status(esa)], [i_0_43176])).
% 280.06/41.12 thf(zip_derived_cl37237, plain, (~ (esk1_0)),
% 280.06/41.12 inference('cnf', [status(esa)], [i_0_37238])).
% 280.06/41.12 thf(zip_derived_cl553783, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 (~ (p @ X0)
% 280.06/41.12 | ~ (p @ X1)
% 280.06/41.12 | ~ (esk17564_4 @ X1 @ X2 @ X3 @ X0)
% 280.06/41.12 | ~ (p @ X3)
% 280.06/41.12 | ~ (p @ X2))),
% 280.06/41.12 inference('demod', [status(thm)],
% 280.06/41.12 [zip_derived_cl43175, zip_derived_cl37237])).
% 280.06/41.12 thf(zip_derived_cl563699, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 280.06/41.12 (~ (p @ X1) | ~ (p @ X2) | ~ (p @ X3) | ~ (p @ X0))),
% 280.06/41.12 inference('clc', [status(thm)],
% 280.06/41.12 [zip_derived_cl563698, zip_derived_cl553783])).
% 280.06/41.12 thf(zip_derived_cl563700, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i, X2 : $i]: (~ (p @ X0) | ~ (p @ X1) | ~ (p @ X2))),
% 280.06/41.12 inference('condensation', [status(thm)], [zip_derived_cl563699])).
% 280.06/41.12 thf(zip_derived_cl563701, plain,
% 280.06/41.12 (![X0 : $i, X1 : $i]: (~ (p @ X0) | ~ (p @ X1))),
% 280.06/41.12 inference('condensation', [status(thm)], [zip_derived_cl563700])).
% 280.06/41.12 thf(zip_derived_cl563702, plain, (![X0 : $i]: ~ (p @ X0)),
% 280.06/41.12 inference('condensation', [status(thm)], [zip_derived_cl563701])).
% 280.06/41.12 thf(rule_true, axiom, (p @ true)).
% 280.06/41.12 thf(zip_derived_cl49910, plain, ( (p @ true)),
% 280.06/41.12 inference('cnf', [status(esa)], [rule_true])).
% 280.06/41.12 thf(zip_derived_cl563810, plain, ($false),
% 280.06/41.12 inference('s_sup+', [status(thm)],
% 280.06/41.12 [zip_derived_cl563702, zip_derived_cl49910])).
% 280.06/41.12
% 280.06/41.12 % SZS output end Refutation
% 280.06/41.12
% 280.06/41.12
% 280.06/41.12 % Terminating...
% 280.66/41.16 % Runner terminated.
% 280.66/41.17 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------