%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : GEO306+1 : TPTP v9.2.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.d0sOa7G7js true
% Computer : n025.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:34:38 PM UTC 2025
% Result : Theorem 17.25s 4.11s
% Output : Refutation 17.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.09 % Problem : GEO306+1 : TPTP v9.2.0. Released v4.1.0.
% 0.04/0.10 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.d0sOa7G7js true
% 0.08/0.31 % Computer : n025.cluster.edu
% 0.08/0.31 % Model : x86_64 x86_64
% 0.08/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.31 % Memory : 8042.1875MB
% 0.08/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.31 % CPULimit : 300
% 0.08/0.31 % WCLimit : 300
% 0.08/0.31 % DateTime : Wed Oct 1 17:32:23 EDT 2025
% 0.15/0.31 % CPUTime :
% 0.15/0.31 % Running portfolio for 300 s
% 0.15/0.31 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.31 % Number of cores: 8
% 0.15/0.31 % Python version: Python 3.6.8
% 0.15/0.31 % Running in FO mode
% 0.16/0.55 % Total configuration time : 435
% 0.16/0.55 % Estimated wc time : 1092
% 0.16/0.55 % Estimated cpu time (7 cpus) : 156.0
% 1.11/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 1.11/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 1.11/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 1.11/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 1.15/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 1.15/0.77 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 1.15/0.80 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 5.86/1.79 % /export/starexec/sandbox2/solver/bin/fo/fo1_lcnf.sh running for 50s
% 17.25/4.11 % Solved by fo/fo1_av.sh.
% 17.25/4.11 % done 1079 iterations in 3.314s
% 17.25/4.11 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 17.25/4.11 % SZS output start Refutation
% 17.25/4.11 thf(rless_type, type, rless: $i > $i > $o).
% 17.25/4.11 thf(vd1302_type, type, vd1302: $i).
% 17.25/4.11 thf(sk__2_type, type, sk__2: $i).
% 17.25/4.11 thf(vd1303_type, type, vd1303: $i).
% 17.25/4.11 thf(sk__type, type, sk_: $i).
% 17.25/4.11 thf(vd1299_type, type, vd1299: $i).
% 17.25/4.11 thf(rpoint_type, type, rpoint: $i > $o).
% 17.25/4.11 thf(vd1287_type, type, vd1287: $i).
% 17.25/4.11 thf(vd1300_type, type, vd1300: $i).
% 17.25/4.11 thf(sk__1_type, type, sk__1: $i).
% 17.25/4.11 thf(vf_type, type, vf: $i > $i > $i).
% 17.25/4.11 thf(vskolem1120_type, type, vskolem1120: $i > $i > $i > $i > $i > $i > $i >
% 17.25/4.11 $i > $i).
% 17.25/4.11 thf(vd1288_type, type, vd1288: $i).
% 17.25/4.11 thf(vd1289_type, type, vd1289: $i).
% 17.25/4.11 thf(rR_type, type, rR: $i > $i > $i > $o).
% 17.25/4.11 thf('holds(351, 1305, 0)', axiom,
% 17.25/4.11 (rless @ ( vf @ vd1287 @ vd1299 ) @ ( vf @ vd1287 @ vd1302 ))).
% 17.25/4.11 thf(zip_derived_cl1, plain,
% 17.25/4.11 ( (rless @ (vf @ vd1287 @ vd1299) @ (vf @ vd1287 @ vd1302))),
% 17.25/4.11 inference('cnf', [status(esa)], [holds(351, 1305, 0)])).
% 17.25/4.11 thf('ass(cond(goal(238), 0), 2)', axiom,
% 17.25/4.11 (![Vd1109:$i,Vd1110:$i,Vd1111:$i,Vd1112:$i,Vd1113:$i,Vd1114:$i,Vd1115:$i,
% 17.25/4.11 Vd1116:$i]:
% 17.25/4.11 ( ( ( rless @ ( vf @ Vd1113 @ Vd1115 ) @ ( vf @ Vd1109 @ Vd1111 ) ) &
% 17.25/4.11 ( ( Vd1113 ) != ( Vd1115 ) ) & ( ( Vd1109 ) != ( Vd1111 ) ) &
% 17.25/4.11 ( ( Vd1115 ) = ( Vd1116 ) ) & ( rpoint @ Vd1116 ) &
% 17.25/4.11 ( ( Vd1113 ) = ( Vd1114 ) ) & ( rpoint @ Vd1114 ) &
% 17.25/4.11 ( ( Vd1111 ) = ( Vd1112 ) ) & ( rpoint @ Vd1112 ) &
% 17.25/4.11 ( ( Vd1109 ) = ( Vd1110 ) ) & ( rpoint @ Vd1110 ) ) =>
% 17.25/4.11 ( rpoint @
% 17.25/4.11 ( vskolem1120 @
% 17.25/4.11 Vd1109 @ Vd1110 @ Vd1111 @ Vd1112 @ Vd1113 @ Vd1114 @ Vd1115 @
% 17.25/4.11 Vd1116 ) ) ))).
% 17.25/4.11 thf(zip_derived_cl29, plain,
% 17.25/4.11 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i, X6 : $i, X7 : $i]:
% 17.25/4.11 (~ (rpoint @ X0)
% 17.25/4.11 | ((X1) != (X0))
% 17.25/4.11 | ~ (rpoint @ X2)
% 17.25/4.11 | ((X3) != (X2))
% 17.25/4.11 | ~ (rpoint @ X4)
% 17.25/4.11 | ((X5) != (X4))
% 17.25/4.11 | ((X1) = (X3))
% 17.25/4.11 | ((X5) = (X6))
% 17.25/4.11 | ~ (rless @ (vf @ X5 @ X6) @ (vf @ X1 @ X3))
% 17.25/4.11 | ((X6) != (X7))
% 17.25/4.11 | ~ (rpoint @ X7)
% 17.25/4.11 | (rpoint @ (vskolem1120 @ X1 @ X0 @ X3 @ X2 @ X5 @ X4 @ X6 @ X7)))),
% 17.25/4.11 inference('cnf', [status(esa)], [ass(cond(goal(238), 0), 2)])).
% 17.25/4.11 thf('ass(cond(goal(238), 0), 0)', axiom,
% 17.25/4.11 (![Vd1109:$i,Vd1110:$i,Vd1111:$i,Vd1112:$i,Vd1113:$i,Vd1114:$i,Vd1115:$i,
% 17.25/4.11 Vd1116:$i]:
% 17.25/4.11 ( ( ( rless @ ( vf @ Vd1113 @ Vd1115 ) @ ( vf @ Vd1109 @ Vd1111 ) ) &
% 17.25/4.11 ( ( Vd1113 ) != ( Vd1115 ) ) & ( ( Vd1109 ) != ( Vd1111 ) ) &
% 17.25/4.11 ( ( Vd1115 ) = ( Vd1116 ) ) & ( rpoint @ Vd1116 ) &
% 17.25/4.11 ( ( Vd1113 ) = ( Vd1114 ) ) & ( rpoint @ Vd1114 ) &
% 17.25/4.11 ( ( Vd1111 ) = ( Vd1112 ) ) & ( rpoint @ Vd1112 ) &
% 17.25/4.11 ( ( Vd1109 ) = ( Vd1110 ) ) & ( rpoint @ Vd1110 ) ) =>
% 17.25/4.11 ( ( vf @
% 17.25/4.11 Vd1109 @
% 17.25/4.11 ( vskolem1120 @
% 17.25/4.11 Vd1109 @ Vd1110 @ Vd1111 @ Vd1112 @ Vd1113 @ Vd1114 @ Vd1115 @
% 17.25/4.11 Vd1116 ) ) =
% 17.25/4.11 ( vf @ Vd1113 @ Vd1115 ) ) ))).
% 17.25/4.11 thf(zip_derived_cl27, plain,
% 17.25/4.11 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i, X6 : $i, X7 : $i]:
% 17.25/4.11 (~ (rpoint @ X0)
% 17.25/4.11 | ((X1) != (X0))
% 17.25/4.11 | ~ (rpoint @ X2)
% 17.25/4.11 | ((X3) != (X2))
% 17.25/4.11 | ~ (rpoint @ X4)
% 17.25/4.11 | ((X5) != (X4))
% 17.25/4.11 | ((X1) = (X3))
% 17.25/4.11 | ((X5) = (X6))
% 17.25/4.11 | ~ (rless @ (vf @ X5 @ X6) @ (vf @ X1 @ X3))
% 17.25/4.11 | ((X6) != (X7))
% 17.25/4.11 | ~ (rpoint @ X7)
% 17.25/4.11 | ((vf @ X1 @ (vskolem1120 @ X1 @ X0 @ X3 @ X2 @ X5 @ X4 @ X6 @ X7))
% 17.25/4.11 = (vf @ X5 @ X6)))),
% 17.25/4.11 inference('cnf', [status(esa)], [ass(cond(goal(238), 0), 0)])).
% 17.25/4.11 thf('ass(cond(goal(238), 0), 1)', axiom,
% 17.25/4.11 (![Vd1109:$i,Vd1110:$i,Vd1111:$i,Vd1112:$i,Vd1113:$i,Vd1114:$i,Vd1115:$i,
% 17.25/4.11 Vd1116:$i]:
% 17.25/4.11 ( ( ( rless @ ( vf @ Vd1113 @ Vd1115 ) @ ( vf @ Vd1109 @ Vd1111 ) ) &
% 17.25/4.11 ( ( Vd1113 ) != ( Vd1115 ) ) & ( ( Vd1109 ) != ( Vd1111 ) ) &
% 17.25/4.11 ( ( Vd1115 ) = ( Vd1116 ) ) & ( rpoint @ Vd1116 ) &
% 17.25/4.11 ( ( Vd1113 ) = ( Vd1114 ) ) & ( rpoint @ Vd1114 ) &
% 17.25/4.11 ( ( Vd1111 ) = ( Vd1112 ) ) & ( rpoint @ Vd1112 ) &
% 17.25/4.11 ( ( Vd1109 ) = ( Vd1110 ) ) & ( rpoint @ Vd1110 ) ) =>
% 17.25/4.11 ( rR @
% 17.25/4.11 ( vskolem1120 @
% 17.25/4.11 Vd1109 @ Vd1110 @ Vd1111 @ Vd1112 @ Vd1113 @ Vd1114 @ Vd1115 @
% 17.25/4.11 Vd1116 ) @
% 17.25/4.11 Vd1109 @ Vd1111 ) ))).
% 17.25/4.11 thf(zip_derived_cl28, plain,
% 17.25/4.11 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i, X6 : $i, X7 : $i]:
% 17.25/4.11 (~ (rpoint @ X0)
% 17.25/4.11 | ((X1) != (X0))
% 17.25/4.11 | ~ (rpoint @ X2)
% 17.25/4.11 | ((X3) != (X2))
% 17.25/4.11 | ~ (rpoint @ X4)
% 17.25/4.11 | ((X5) != (X4))
% 17.25/4.11 | ((X1) = (X3))
% 17.25/4.11 | ((X5) = (X6))
% 17.25/4.11 | ~ (rless @ (vf @ X5 @ X6) @ (vf @ X1 @ X3))
% 17.25/4.11 | ((X6) != (X7))
% 17.25/4.11 | ~ (rpoint @ X7)
% 17.25/4.11 | (rR @ (vskolem1120 @ X1 @ X0 @ X3 @ X2 @ X5 @ X4 @ X6 @ X7) @
% 17.25/4.11 X1 @ X3))),
% 17.25/4.11 inference('cnf', [status(esa)], [ass(cond(goal(238), 0), 1)])).
% 17.25/4.11 thf(qe(352), conjecture,
% 17.25/4.11 (?[Vd1306:$i]:
% 17.25/4.11 ( ( rpoint @ Vd1306 ) & ( rR @ Vd1306 @ vd1287 @ vd1302 ) &
% 17.25/4.11 ( ( vf @ vd1287 @ vd1299 ) = ( vf @ vd1287 @ Vd1306 ) ) ))).
% 17.25/4.11 thf(zf_stmt_0, negated_conjecture,
% 17.25/4.11 (~( ?[Vd1306:$i]:
% 17.25/4.11 ( ( rpoint @ Vd1306 ) & ( rR @ Vd1306 @ vd1287 @ vd1302 ) &
% 17.25/4.11 ( ( vf @ vd1287 @ vd1299 ) = ( vf @ vd1287 @ Vd1306 ) ) ) )),
% 17.25/4.11 inference('cnf.neg', [status(esa)], [qe(352)])).
% 17.25/4.11 thf(zip_derived_cl0, plain,
% 17.25/4.11 (![X0 : $i]:
% 17.25/4.11 (~ (rpoint @ X0)
% 17.25/4.11 | ~ (rR @ X0 @ vd1287 @ vd1302)
% 17.25/4.11 | ((vf @ vd1287 @ vd1299) != (vf @ vd1287 @ X0)))),
% 17.25/4.11 inference('cnf', [status(esa)], [zf_stmt_0])).
% 17.25/4.11 thf(zip_derived_cl346, plain,
% 17.25/4.11 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 17.25/4.11 (~ (rpoint @ X0)
% 17.25/4.11 | ((X1) != (X0))
% 17.25/4.11 | ~ (rless @ (vf @ X3 @ X1) @ (vf @ vd1287 @ vd1302))
% 17.25/4.11 | ((X3) = (X1))
% 17.25/4.11 | ((vd1287) = (vd1302))
% 17.25/4.11 | ((X3) != (X2))
% 17.25/4.11 | ~ (rpoint @ X2)
% 17.25/4.11 | ((vd1302) != (X4))
% 17.25/4.11 | ~ (rpoint @ X4)
% 17.25/4.11 | ((vd1287) != (X5))
% 17.25/4.11 | ~ (rpoint @ X5)
% 17.25/4.11 | ~ (rpoint @
% 17.25/4.11 (vskolem1120 @ vd1287 @ X5 @ vd1302 @ X4 @ X3 @ X2 @ X1 @ X0))
% 17.25/4.11 | ((vf @ vd1287 @ vd1299)
% 17.25/4.11 != (vf @ vd1287 @
% 17.25/4.11 (vskolem1120 @ vd1287 @ X5 @ vd1302 @ X4 @ X3 @ X2 @ X1 @ X0))))),
% 17.25/4.11 inference('s_sup-', [status(thm)], [zip_derived_cl28, zip_derived_cl0])).
% 17.25/4.11 thf('and(pred(conjunct2(348), 4), and(holds(conjunct2(348), 1304, 0), and(pred(conjunct2(348), 1), holds(conjunct1(348), 1301, 0))))', axiom,
% 17.25/4.11 (( rR @ vd1288 @ vd1287 @ vd1299 ) & ( rpoint @ vd1303 ) &
% 17.25/4.11 ( rR @ vd1289 @ vd1287 @ vd1302 ) & ( ( vd1302 ) = ( vd1303 ) ))).
% 17.25/4.11 thf(zip_derived_cl6, plain, ( (rR @ vd1289 @ vd1287 @ vd1302)),
% 17.25/4.11 inference('cnf', [status(esa)],
% 17.25/4.11 [and(pred(conjunct2(348), 4), and(holds(conjunct2(348), 1304, 0), and(pred(conjunct2(348), 1), holds(conjunct1(348), 1301, 0))))])).
% 17.25/4.11 thf('qu(cond(axiom(81), 0), imp(cond(axiom(81), 0)))', axiom,
% 17.25/4.11 (![Vd340:$i,Vd341:$i,Vd342:$i]:
% 17.25/4.11 ( ( ( rR @ Vd341 @ Vd340 @ Vd342 ) &
% 17.25/4.11 ( ?[Vd346:$i]: ( ( rpoint @ Vd346 ) & ( ( Vd342 ) = ( Vd346 ) ) ) ) &
% 17.25/4.11 ( ?[Vd345:$i]: ( ( rpoint @ Vd345 ) & ( ( Vd341 ) = ( Vd345 ) ) ) ) &
% 17.25/4.11 ( ?[Vd344:$i]: ( ( rpoint @ Vd344 ) & ( ( Vd340 ) = ( Vd344 ) ) ) ) ) =>
% 17.25/4.11 ( ( ~( rR @ Vd340 @ Vd341 @ Vd342 ) ) & ( ( Vd340 ) != ( Vd342 ) ) &
% 17.25/4.11 ( ( Vd340 ) != ( Vd341 ) ) & ( rR @ Vd341 @ Vd342 @ Vd340 ) ) ))).
% 17.25/4.11 thf(zip_derived_cl82, plain,
% 17.25/4.11 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 17.25/4.11 (((X1) != (X0))
% 17.25/4.11 | ~ (rpoint @ X0)
% 17.25/4.11 | ((X3) != (X2))
% 17.25/4.11 | ~ (rpoint @ X2)
% 17.25/4.11 | ~ (rR @ X3 @ X1 @ X4)
% 17.25/4.11 | ~ (rpoint @ X5)
% 17.25/4.11 | ((X4) != (X5))
% 17.25/4.11 | ((X1) != (X4)))),
% 17.25/4.11 inference('cnf', [status(esa)],
% 17.25/4.11 [qu(cond(axiom(81), 0), imp(cond(axiom(81), 0)))])).
% 17.25/4.11 thf(zip_derived_cl509, plain,
% 17.25/4.11 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 17.25/4.11 (((X0) != (X1))
% 17.25/4.11 | ((X1) != (X2))
% 17.25/4.11 | ~ (rpoint @ X2)
% 17.25/4.11 | ~ (rR @ X3 @ X0 @ X1)
% 17.25/4.11 | ~ (rpoint @ X4)
% 17.25/4.11 | ((X3) != (X4))
% 17.25/4.11 | ~ (rpoint @ X0))),
% 17.25/4.11 inference('eq_res', [status(thm)], [zip_derived_cl82])).
% 17.25/4.11 thf(zip_derived_cl514, plain,
% 17.25/4.11 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 17.25/4.11 (~ (rpoint @ X0)
% 17.25/4.11 | ((X1) != (X2))
% 17.25/4.11 | ~ (rpoint @ X2)
% 17.25/4.11 | ~ (rR @ X1 @ X0 @ X3)
% 17.25/4.11 | ~ (rpoint @ X3)
% 17.25/4.11 | ((X0) != (X3)))),
% 17.25/4.11 inference('eq_res', [status(thm)], [zip_derived_cl509])).
% 17.25/4.11 thf(zip_derived_cl515, plain,
% 17.25/4.11 (![X0 : $i, X1 : $i, X2 : $i]:
% 17.25/4.11 (((X0) != (X1))
% 17.25/4.11 | ~ (rpoint @ X1)
% 17.25/4.11 | ~ (rR @ X2 @ X0 @ X1)
% 17.25/4.11 | ~ (rpoint @ X2)
% 17.25/4.11 | ~ (rpoint @ X0))),
% 17.25/4.11 inference('eq_res', [status(thm)], [zip_derived_cl514])).
% 17.25/4.11 thf(zip_derived_cl519, plain,
% 17.25/4.11 ((((vd1287) != (vd1302))
% 17.25/4.11 | ~ (rpoint @ vd1302)
% 17.25/4.11 | ~ (rpoint @ vd1289)
% 17.25/4.11 | ~ (rpoint @ vd1287))),
% 17.25/4.11 inference('s_sup-', [status(thm)], [zip_derived_cl6, zip_derived_cl515])).
% 17.25/4.11 thf(zip_derived_cl5, plain, ( (rpoint @ vd1303)),
% 17.25/4.11 inference('cnf', [status(esa)],
% 17.25/4.11 [and(pred(conjunct2(348), 4), and(holds(conjunct2(348), 1304, 0), and(pred(conjunct2(348), 1), holds(conjunct1(348), 1301, 0))))])).
% 17.25/4.11 thf(zip_derived_cl7, plain, (((vd1302) = (vd1303))),
% 17.25/4.11 inference('cnf', [status(esa)],
% 17.25/4.11 [and(pred(conjunct2(348), 4), and(holds(conjunct2(348), 1304, 0), and(pred(conjunct2(348), 1), holds(conjunct1(348), 1301, 0))))])).
% 17.25/4.11 thf(zip_derived_cl310, plain, ( (rpoint @ vd1302)),
% 17.25/4.11 inference('demod', [status(thm)], [zip_derived_cl5, zip_derived_cl7])).
% 17.25/4.11 thf('and(holds(conjunct2(345), 1294, 0), and(pred(conjunct1(345), 9), and(pred(conjunct1(345), 8), and(pred(conjunct1(345), 7), and(qe(s3(plural(345))), and(qe(s2(plural(345))), qe(s1(plural(345)))))))))', axiom,
% 17.25/4.11 (( ?[Vd1291:$i]: ( ( rpoint @ Vd1291 ) & ( ( vd1287 ) = ( Vd1291 ) ) ) ) &
% 17.25/4.11 ( ?[Vd1292:$i]: ( ( rpoint @ Vd1292 ) & ( ( vd1288 ) = ( Vd1292 ) ) ) ) &
% 17.25/4.11 ( ?[Vd1293:$i]: ( ( rpoint @ Vd1293 ) & ( ( vd1289 ) = ( Vd1293 ) ) ) ) &
% 17.25/4.11 ( ( vd1287 ) != ( vd1288 ) ) & ( ( vd1287 ) != ( vd1289 ) ) &
% 17.25/4.11 ( ( vd1288 ) != ( vd1289 ) ) &
% 17.25/4.11 ( ( vf @ vd1287 @ vd1288 ) = ( vf @ vd1287 @ vd1289 ) ))).
% 17.25/4.11 thf(zip_derived_cl15, plain, ( (rpoint @ sk__2)),
% 17.25/4.11 inference('cnf', [status(esa)],
% 17.25/4.11 [and(holds(conjunct2(345), 1294, 0), and(pred(conjunct1(345), 9), and(pred(conjunct1(345), 8), and(pred(conjunct1(345), 7), and(qe(s3(plural(345))), and(qe(s2(plural(345))), qe(s1(plural(345)))))))))])).
% 17.25/4.11 thf(zip_derived_cl16, plain, (((vd1289) = (sk__2))),
% 17.25/4.11 inference('cnf', [status(esa)],
% 17.25/4.11 [and(holds(conjunct2(345), 1294, 0), and(pred(conjunct1(345), 9), and(pred(conjunct1(345), 8), and(pred(conjunct1(345), 7), and(qe(s3(plural(345))), and(qe(s2(plural(345))), qe(s1(plural(345)))))))))])).
% 17.25/4.11 thf(zip_derived_cl322, plain, ( (rpoint @ vd1289)),
% 17.25/4.11 inference('demod', [status(thm)], [zip_derived_cl15, zip_derived_cl16])).
% 17.25/4.11 thf(zip_derived_cl19, plain, ( (rpoint @ sk_)),
% 17.25/4.11 inference('cnf', [status(esa)],
% 17.25/4.11 [and(holds(conjunct2(345), 1294, 0), and(pred(conjunct1(345), 9), and(pred(conjunct1(345), 8), and(pred(conjunct1(345), 7), and(qe(s3(plural(345))), and(qe(s2(plural(345))), qe(s1(plural(345)))))))))])).
% 17.25/4.11 thf(zip_derived_cl20, plain, (((vd1287) = (sk_))),
% 17.25/4.11 inference('cnf', [status(esa)],
% 17.25/4.11 [and(holds(conjunct2(345), 1294, 0), and(pred(conjunct1(345), 9), and(pred(conjunct1(345), 8), and(pred(conjunct1(345), 7), and(qe(s3(plural(345))), and(qe(s2(plural(345))), qe(s1(plural(345)))))))))])).
% 17.25/4.11 thf(zip_derived_cl329, plain, ( (rpoint @ vd1287)),
% 17.25/4.11 inference('demod', [status(thm)], [zip_derived_cl19, zip_derived_cl20])).
% 17.25/4.11 thf(zip_derived_cl522, plain, (((vd1287) != (vd1302))),
% 17.25/4.11 inference('demod', [status(thm)],
% 17.25/4.11 [zip_derived_cl519, zip_derived_cl310, zip_derived_cl322,
% 17.25/4.11 zip_derived_cl329])).
% 17.25/4.11 thf(zip_derived_cl2142, plain,
% 17.25/4.11 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 17.25/4.11 (~ (rpoint @ X0)
% 17.25/4.11 | ((X1) != (X0))
% 17.25/4.11 | ~ (rless @ (vf @ X3 @ X1) @ (vf @ vd1287 @ vd1302))
% 17.25/4.11 | ((X3) = (X1))
% 17.25/4.11 | ((X3) != (X2))
% 17.25/4.11 | ~ (rpoint @ X2)
% 17.25/4.11 | ((vd1302) != (X4))
% 17.25/4.11 | ~ (rpoint @ X4)
% 17.25/4.11 | ((vd1287) != (X5))
% 17.25/4.11 | ~ (rpoint @ X5)
% 17.25/4.11 | ~ (rpoint @
% 17.25/4.11 (vskolem1120 @ vd1287 @ X5 @ vd1302 @ X4 @ X3 @ X2 @ X1 @ X0))
% 17.25/4.11 | ((vf @ vd1287 @ vd1299)
% 17.25/4.11 != (vf @ vd1287 @
% 17.25/4.11 (vskolem1120 @ vd1287 @ X5 @ vd1302 @ X4 @ X3 @ X2 @ X1 @ X0))))),
% 17.25/4.11 inference('simplify_reflect-', [status(thm)],
% 17.25/4.11 [zip_derived_cl346, zip_derived_cl522])).
% 17.25/4.11 thf(zip_derived_cl2144, plain,
% 17.25/4.11 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 17.25/4.11 (~ (rpoint @ X2)
% 17.25/4.11 | ((X0) != (X2))
% 17.25/4.11 | ~ (rless @ (vf @ X1 @ X0) @ (vf @ vd1287 @ vd1302))
% 17.25/4.11 | ((X1) = (X0))
% 17.25/4.11 | ((vd1287) = (vd1302))
% 17.25/4.11 | ((X1) != (X3))
% 17.25/4.11 | ~ (rpoint @ X3)
% 17.25/4.11 | ((vd1302) != (X4))
% 17.25/4.11 | ~ (rpoint @ X4)
% 17.25/4.11 | ((vd1287) != (X5))
% 17.25/4.11 | ~ (rpoint @ X5)
% 17.25/4.11 | ~ (rpoint @ X2)
% 17.25/4.11 | ((X0) != (X2))
% 17.25/4.11 | ~ (rless @ (vf @ X1 @ X0) @ (vf @ vd1287 @ vd1302))
% 17.25/4.11 | ((X1) = (X0))
% 17.25/4.11 | ((X1) != (X3))
% 17.25/4.11 | ~ (rpoint @ X3)
% 17.25/4.11 | ((vd1302) != (X4))
% 17.25/4.11 | ~ (rpoint @ X4)
% 17.25/4.11 | ((vd1287) != (X5))
% 17.25/4.11 | ~ (rpoint @ X5)
% 17.25/4.11 | ~ (rpoint @
% 17.25/4.11 (vskolem1120 @ vd1287 @ X5 @ vd1302 @ X4 @ X1 @ X3 @ X0 @ X2))
% 17.25/4.11 | ((vf @ vd1287 @ vd1299) != (vf @ X1 @ X0)))),
% 17.25/4.11 inference('s_sup-', [status(thm)], [zip_derived_cl27, zip_derived_cl2142])).
% 17.25/4.11 thf(zip_derived_cl2147, plain,
% 17.25/4.11 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 17.25/4.11 (((vf @ vd1287 @ vd1299) != (vf @ X1 @ X0))
% 17.25/4.11 | ~ (rpoint @
% 17.25/4.11 (vskolem1120 @ vd1287 @ X5 @ vd1302 @ X4 @ X1 @ X3 @ X0 @ X2))
% 17.25/4.11 | ~ (rpoint @ X5)
% 17.25/4.11 | ((vd1287) != (X5))
% 17.25/4.11 | ~ (rpoint @ X4)
% 17.25/4.11 | ((vd1302) != (X4))
% 17.25/4.11 | ~ (rpoint @ X3)
% 17.25/4.11 | ((X1) != (X3))
% 17.25/4.11 | ((vd1287) = (vd1302))
% 17.25/4.11 | ((X1) = (X0))
% 17.25/4.11 | ~ (rless @ (vf @ X1 @ X0) @ (vf @ vd1287 @ vd1302))
% 17.25/4.11 | ((X0) != (X2))
% 17.25/4.11 | ~ (rpoint @ X2))),
% 17.25/4.11 inference('simplify', [status(thm)], [zip_derived_cl2144])).
% 17.25/4.11 thf(zip_derived_cl522, plain, (((vd1287) != (vd1302))),
% 17.25/4.11 inference('demod', [status(thm)],
% 17.25/4.11 [zip_derived_cl519, zip_derived_cl310, zip_derived_cl322,
% 17.25/4.11 zip_derived_cl329])).
% 17.25/4.11 thf(zip_derived_cl2148, plain,
% 17.25/4.11 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 17.25/4.11 (((vf @ vd1287 @ vd1299) != (vf @ X1 @ X0))
% 17.25/4.11 | ~ (rpoint @
% 17.25/4.11 (vskolem1120 @ vd1287 @ X5 @ vd1302 @ X4 @ X1 @ X3 @ X0 @ X2))
% 17.25/4.11 | ~ (rpoint @ X5)
% 17.25/4.11 | ((vd1287) != (X5))
% 17.25/4.11 | ~ (rpoint @ X4)
% 17.25/4.11 | ((vd1302) != (X4))
% 17.25/4.11 | ~ (rpoint @ X3)
% 17.25/4.11 | ((X1) != (X3))
% 17.25/4.11 | ((X1) = (X0))
% 17.25/4.11 | ~ (rless @ (vf @ X1 @ X0) @ (vf @ vd1287 @ vd1302))
% 17.25/4.11 | ((X0) != (X2))
% 17.25/4.11 | ~ (rpoint @ X2))),
% 17.25/4.11 inference('simplify_reflect-', [status(thm)],
% 17.25/4.11 [zip_derived_cl2147, zip_derived_cl522])).
% 17.25/4.11 thf(zip_derived_cl2160, plain,
% 17.25/4.11 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 17.25/4.11 (~ (rpoint @ X0)
% 17.25/4.11 | ((X1) != (X0))
% 17.25/4.11 | ~ (rless @ (vf @ X3 @ X1) @ (vf @ vd1287 @ vd1302))
% 17.25/4.11 | ((X3) = (X1))
% 17.25/4.11 | ((vd1287) = (vd1302))
% 17.25/4.11 | ((X3) != (X2))
% 17.25/4.11 | ~ (rpoint @ X2)
% 17.25/4.11 | ((vd1302) != (X4))
% 17.25/4.11 | ~ (rpoint @ X4)
% 17.25/4.11 | ((vd1287) != (X5))
% 17.25/4.11 | ~ (rpoint @ X5)
% 17.25/4.11 | ((vf @ vd1287 @ vd1299) != (vf @ X3 @ X1))
% 17.25/4.11 | ~ (rpoint @ X5)
% 17.25/4.11 | ((vd1287) != (X5))
% 17.25/4.11 | ~ (rpoint @ X4)
% 17.25/4.11 | ((vd1302) != (X4))
% 17.25/4.11 | ~ (rpoint @ X2)
% 17.25/4.11 | ((X3) != (X2))
% 17.25/4.11 | ((X3) = (X1))
% 17.25/4.11 | ~ (rless @ (vf @ X3 @ X1) @ (vf @ vd1287 @ vd1302))
% 17.25/4.11 | ((X1) != (X0))
% 17.25/4.11 | ~ (rpoint @ X0))),
% 17.25/4.11 inference('s_sup-', [status(thm)], [zip_derived_cl29, zip_derived_cl2148])).
% 17.25/4.11 thf(zip_derived_cl2161, plain,
% 17.25/4.11 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 17.25/4.11 (((vf @ vd1287 @ vd1299) != (vf @ X3 @ X1))
% 17.25/4.11 | ~ (rpoint @ X5)
% 17.25/4.11 | ((vd1287) != (X5))
% 17.25/4.11 | ~ (rpoint @ X4)
% 17.25/4.11 | ((vd1302) != (X4))
% 17.25/4.11 | ~ (rpoint @ X2)
% 17.25/4.11 | ((X3) != (X2))
% 17.25/4.11 | ((vd1287) = (vd1302))
% 17.25/4.11 | ((X3) = (X1))
% 17.25/4.11 | ~ (rless @ (vf @ X3 @ X1) @ (vf @ vd1287 @ vd1302))
% 17.25/4.11 | ((X1) != (X0))
% 17.25/4.11 | ~ (rpoint @ X0))),
% 17.25/4.11 inference('simplify', [status(thm)], [zip_derived_cl2160])).
% 17.25/4.11 thf(zip_derived_cl522, plain, (((vd1287) != (vd1302))),
% 17.25/4.11 inference('demod', [status(thm)],
% 17.25/4.11 [zip_derived_cl519, zip_derived_cl310, zip_derived_cl322,
% 17.25/4.11 zip_derived_cl329])).
% 17.25/4.11 thf(zip_derived_cl2162, plain,
% 17.25/4.11 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 17.25/4.11 (((vf @ vd1287 @ vd1299) != (vf @ X3 @ X1))
% 17.25/4.11 | ~ (rpoint @ X5)
% 17.25/4.11 | ((vd1287) != (X5))
% 17.25/4.11 | ~ (rpoint @ X4)
% 17.25/4.11 | ((vd1302) != (X4))
% 17.25/4.11 | ~ (rpoint @ X2)
% 17.25/4.11 | ((X3) != (X2))
% 17.25/4.11 | ((X3) = (X1))
% 17.25/4.11 | ~ (rless @ (vf @ X3 @ X1) @ (vf @ vd1287 @ vd1302))
% 17.25/4.11 | ((X1) != (X0))
% 17.25/4.11 | ~ (rpoint @ X0))),
% 17.25/4.11 inference('simplify_reflect-', [status(thm)],
% 17.25/4.11 [zip_derived_cl2161, zip_derived_cl522])).
% 17.25/4.11 thf(zip_derived_cl2167, plain,
% 17.25/4.11 ((![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 17.25/4.11 (~ (rpoint @ X0)
% 17.25/4.11 | ((vf @ vd1287 @ vd1299) != (vf @ X3 @ X1))
% 17.25/4.11 | ((X1) != (X0))
% 17.25/4.11 | ((X3) = (X1))
% 17.25/4.11 | ((X3) != (X2))
% 17.25/4.11 | ~ (rpoint @ X2)
% 17.25/4.11 | ~ (rless @ (vf @ X3 @ X1) @ (vf @ vd1287 @ vd1302))))
% 17.25/4.11 <= ((![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 17.25/4.11 (~ (rpoint @ X0)
% 17.25/4.11 | ((vf @ vd1287 @ vd1299) != (vf @ X3 @ X1))
% 17.25/4.11 | ((X1) != (X0))
% 17.25/4.11 | ((X3) = (X1))
% 17.25/4.11 | ((X3) != (X2))
% 17.25/4.11 | ~ (rpoint @ X2)
% 17.25/4.11 | ~ (rless @ (vf @ X3 @ X1) @ (vf @ vd1287 @ vd1302)))))),
% 17.25/4.11 inference('split', [status(esa)], [zip_derived_cl2162])).
% 17.25/4.11 thf(zip_derived_cl329, plain, ( (rpoint @ vd1287)),
% 17.25/4.11 inference('demod', [status(thm)], [zip_derived_cl19, zip_derived_cl20])).
% 17.25/4.11 thf(zip_derived_cl2165, plain,
% 17.25/4.11 ((![X5 : $i]: (((vd1287) != (X5)) | ~ (rpoint @ X5)))
% 17.25/4.11 <= ((![X5 : $i]: (((vd1287) != (X5)) | ~ (rpoint @ X5))))),
% 17.25/4.11 inference('split', [status(esa)], [zip_derived_cl2162])).
% 17.25/4.11 thf(zip_derived_cl2195, plain,
% 17.25/4.11 ((((vd1287) != (vd1287)))
% 17.25/4.11 <= ((![X5 : $i]: (((vd1287) != (X5)) | ~ (rpoint @ X5))))),
% 17.25/4.11 inference('s_sup-', [status(thm)],
% 17.25/4.11 [zip_derived_cl329, zip_derived_cl2165])).
% 17.25/4.11 thf('0', plain, (~ (![X5 : $i]: (((vd1287) != (X5)) | ~ (rpoint @ X5)))),
% 17.25/4.11 inference('simplify', [status(thm)], [zip_derived_cl2195])).
% 17.25/4.11 thf(zip_derived_cl310, plain, ( (rpoint @ vd1302)),
% 17.25/4.11 inference('demod', [status(thm)], [zip_derived_cl5, zip_derived_cl7])).
% 17.25/4.11 thf(zip_derived_cl2166, plain,
% 17.25/4.11 ((![X4 : $i]: (((vd1302) != (X4)) | ~ (rpoint @ X4)))
% 17.25/4.11 <= ((![X4 : $i]: (((vd1302) != (X4)) | ~ (rpoint @ X4))))),
% 17.25/4.11 inference('split', [status(esa)], [zip_derived_cl2162])).
% 17.25/4.11 thf(zip_derived_cl2253, plain,
% 17.25/4.11 ((((vd1302) != (vd1302)))
% 17.25/4.11 <= ((![X4 : $i]: (((vd1302) != (X4)) | ~ (rpoint @ X4))))),
% 17.25/4.11 inference('s_sup-', [status(thm)],
% 17.25/4.11 [zip_derived_cl310, zip_derived_cl2166])).
% 17.25/4.11 thf('1', plain, (~ (![X4 : $i]: (((vd1302) != (X4)) | ~ (rpoint @ X4)))),
% 17.25/4.11 inference('simplify', [status(thm)], [zip_derived_cl2253])).
% 17.25/4.11 thf('2', plain,
% 17.25/4.11 ((![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 17.25/4.11 (~ (rpoint @ X0)
% 17.25/4.11 | ((vf @ vd1287 @ vd1299) != (vf @ X3 @ X1))
% 17.25/4.11 | ((X1) != (X0))
% 17.25/4.11 | ((X3) = (X1))
% 17.25/4.11 | ((X3) != (X2))
% 17.25/4.11 | ~ (rpoint @ X2)
% 17.25/4.11 | ~ (rless @ (vf @ X3 @ X1) @ (vf @ vd1287 @ vd1302)))) |
% 17.25/4.11 (![X4 : $i]: (((vd1302) != (X4)) | ~ (rpoint @ X4))) |
% 17.25/4.11 (![X5 : $i]: (((vd1287) != (X5)) | ~ (rpoint @ X5)))),
% 17.25/4.11 inference('split', [status(esa)], [zip_derived_cl2162])).
% 17.25/4.11 thf('3', plain,
% 17.25/4.11 ((![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 17.25/4.11 (~ (rpoint @ X0)
% 17.25/4.11 | ((vf @ vd1287 @ vd1299) != (vf @ X3 @ X1))
% 17.25/4.11 | ((X1) != (X0))
% 17.25/4.11 | ((X3) = (X1))
% 17.25/4.11 | ((X3) != (X2))
% 17.25/4.11 | ~ (rpoint @ X2)
% 17.25/4.11 | ~ (rless @ (vf @ X3 @ X1) @ (vf @ vd1287 @ vd1302))))),
% 17.25/4.11 inference('sat_resolution*', [status(thm)], ['0', '1', '2'])).
% 17.25/4.11 thf(zip_derived_cl2281, plain,
% 17.25/4.11 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 17.25/4.11 (~ (rpoint @ X0)
% 17.25/4.11 | ((vf @ vd1287 @ vd1299) != (vf @ X3 @ X1))
% 17.25/4.11 | ((X1) != (X0))
% 17.25/4.11 | ((X3) = (X1))
% 17.25/4.11 | ((X3) != (X2))
% 17.25/4.11 | ~ (rpoint @ X2)
% 17.25/4.11 | ~ (rless @ (vf @ X3 @ X1) @ (vf @ vd1287 @ vd1302)))),
% 17.25/4.11 inference('simpl_trail', [status(thm)], [zip_derived_cl2167, '3'])).
% 17.25/4.11 thf(zip_derived_cl2282, plain,
% 17.25/4.11 (![X0 : $i, X1 : $i, X2 : $i]:
% 17.25/4.11 (~ (rless @ (vf @ X1 @ X0) @ (vf @ vd1287 @ vd1302))
% 17.25/4.11 | ~ (rpoint @ X2)
% 17.25/4.11 | ((X1) != (X2))
% 17.25/4.11 | ((X1) = (X0))
% 17.25/4.11 | ((vf @ vd1287 @ vd1299) != (vf @ X1 @ X0))
% 17.25/4.11 | ~ (rpoint @ X0))),
% 17.25/4.11 inference('eq_res', [status(thm)], [zip_derived_cl2281])).
% 17.25/4.11 thf(zip_derived_cl2292, plain,
% 17.25/4.11 (![X0 : $i, X1 : $i]:
% 17.25/4.11 (~ (rpoint @ X0)
% 17.25/4.11 | ((vf @ vd1287 @ vd1299) != (vf @ X1 @ X0))
% 17.25/4.11 | ((X1) = (X0))
% 17.25/4.11 | ~ (rpoint @ X1)
% 17.25/4.11 | ~ (rless @ (vf @ X1 @ X0) @ (vf @ vd1287 @ vd1302)))),
% 17.25/4.11 inference('eq_res', [status(thm)], [zip_derived_cl2282])).
% 17.25/4.11 thf(zip_derived_cl2294, plain,
% 17.25/4.11 ((~ (rpoint @ vd1299)
% 17.25/4.11 | ((vf @ vd1287 @ vd1299) != (vf @ vd1287 @ vd1299))
% 17.25/4.11 | ((vd1287) = (vd1299))
% 17.25/4.11 | ~ (rpoint @ vd1287))),
% 17.25/4.11 inference('s_sup-', [status(thm)], [zip_derived_cl1, zip_derived_cl2292])).
% 17.25/4.11 thf('pred(348, 1)', axiom, (rpoint @ vd1300)).
% 17.25/4.11 thf(zip_derived_cl23, plain, ( (rpoint @ vd1300)),
% 17.25/4.11 inference('cnf', [status(esa)], [pred(348, 1)])).
% 17.25/4.11 thf('pred(348, 4)', axiom, (( vd1299 ) = ( vd1300 ))).
% 17.25/4.11 thf(zip_derived_cl22, plain, (((vd1299) = (vd1300))),
% 17.25/4.11 inference('cnf', [status(esa)], [pred(348, 4)])).
% 17.25/4.11 thf(zip_derived_cl330, plain, ( (rpoint @ vd1299)),
% 17.25/4.11 inference('demod', [status(thm)], [zip_derived_cl23, zip_derived_cl22])).
% 17.25/4.11 thf(zip_derived_cl329, plain, ( (rpoint @ vd1287)),
% 17.25/4.11 inference('demod', [status(thm)], [zip_derived_cl19, zip_derived_cl20])).
% 17.25/4.11 thf(zip_derived_cl2304, plain,
% 17.25/4.11 ((((vf @ vd1287 @ vd1299) != (vf @ vd1287 @ vd1299))
% 17.25/4.11 | ((vd1287) = (vd1299)))),
% 17.25/4.11 inference('demod', [status(thm)],
% 17.25/4.11 [zip_derived_cl2294, zip_derived_cl330, zip_derived_cl329])).
% 17.25/4.11 thf(zip_derived_cl2305, plain, (((vd1287) = (vd1299))),
% 17.25/4.11 inference('simplify', [status(thm)], [zip_derived_cl2304])).
% 17.25/4.11 thf(zip_derived_cl4, plain, ( (rR @ vd1288 @ vd1287 @ vd1299)),
% 17.25/4.11 inference('cnf', [status(esa)],
% 17.25/4.11 [and(pred(conjunct2(348), 4), and(holds(conjunct2(348), 1304, 0), and(pred(conjunct2(348), 1), holds(conjunct1(348), 1301, 0))))])).
% 17.25/4.11 thf(zip_derived_cl515, plain,
% 17.25/4.11 (![X0 : $i, X1 : $i, X2 : $i]:
% 17.25/4.11 (((X0) != (X1))
% 17.25/4.11 | ~ (rpoint @ X1)
% 17.25/4.11 | ~ (rR @ X2 @ X0 @ X1)
% 17.25/4.11 | ~ (rpoint @ X2)
% 17.25/4.11 | ~ (rpoint @ X0))),
% 17.25/4.11 inference('eq_res', [status(thm)], [zip_derived_cl514])).
% 17.25/4.11 thf(zip_derived_cl520, plain,
% 17.25/4.11 ((((vd1287) != (vd1299))
% 17.25/4.11 | ~ (rpoint @ vd1299)
% 17.25/4.11 | ~ (rpoint @ vd1288)
% 17.25/4.11 | ~ (rpoint @ vd1287))),
% 17.25/4.11 inference('s_sup-', [status(thm)], [zip_derived_cl4, zip_derived_cl515])).
% 17.25/4.11 thf(zip_derived_cl330, plain, ( (rpoint @ vd1299)),
% 17.25/4.11 inference('demod', [status(thm)], [zip_derived_cl23, zip_derived_cl22])).
% 17.25/4.11 thf(zip_derived_cl17, plain, ( (rpoint @ sk__1)),
% 17.25/4.11 inference('cnf', [status(esa)],
% 17.25/4.11 [and(holds(conjunct2(345), 1294, 0), and(pred(conjunct1(345), 9), and(pred(conjunct1(345), 8), and(pred(conjunct1(345), 7), and(qe(s3(plural(345))), and(qe(s2(plural(345))), qe(s1(plural(345)))))))))])).
% 17.25/4.11 thf(zip_derived_cl18, plain, (((vd1288) = (sk__1))),
% 17.25/4.11 inference('cnf', [status(esa)],
% 17.25/4.11 [and(holds(conjunct2(345), 1294, 0), and(pred(conjunct1(345), 9), and(pred(conjunct1(345), 8), and(pred(conjunct1(345), 7), and(qe(s3(plural(345))), and(qe(s2(plural(345))), qe(s1(plural(345)))))))))])).
% 17.25/4.11 thf(zip_derived_cl328, plain, ( (rpoint @ vd1288)),
% 17.25/4.11 inference('demod', [status(thm)], [zip_derived_cl17, zip_derived_cl18])).
% 17.25/4.11 thf(zip_derived_cl329, plain, ( (rpoint @ vd1287)),
% 17.25/4.11 inference('demod', [status(thm)], [zip_derived_cl19, zip_derived_cl20])).
% 17.25/4.11 thf(zip_derived_cl523, plain, (((vd1287) != (vd1299))),
% 17.25/4.11 inference('demod', [status(thm)],
% 17.25/4.11 [zip_derived_cl520, zip_derived_cl330, zip_derived_cl328,
% 17.25/4.11 zip_derived_cl329])).
% 17.25/4.11 thf(zip_derived_cl2306, plain, ($false),
% 17.25/4.11 inference('simplify_reflect-', [status(thm)],
% 17.25/4.11 [zip_derived_cl2305, zip_derived_cl523])).
% 17.25/4.11
% 17.25/4.11 % SZS output end Refutation
% 17.25/4.11
% 17.25/4.11
% 17.25/4.11 % Terminating...
% 17.50/4.25 % Runner terminated.
% 17.50/4.27 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------