%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : GEO290+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.OI1SHq2kpe true
% Computer : n002.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:36 PM UTC 2025
% Result : Theorem 0.52s 0.98s
% Output : Refutation 0.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GEO290+1 : TPTP v9.2.0. Released v4.1.0.
% 0.07/0.14 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.OI1SHq2kpe true
% 0.13/0.36 % Computer : n002.cluster.edu
% 0.13/0.36 % Model : x86_64 x86_64
% 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.36 % Memory : 8042.1875MB
% 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.36 % CPULimit : 300
% 0.13/0.36 % WCLimit : 300
% 0.13/0.36 % DateTime : Wed Oct 1 17:37:38 EDT 2025
% 0.13/0.36 % CPUTime :
% 0.13/0.36 % Running portfolio for 300 s
% 0.13/0.36 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.36 % Number of cores: 8
% 0.13/0.36 % Python version: Python 3.6.8
% 0.13/0.36 % Running in FO mode
% 0.50/0.62 % Total configuration time : 435
% 0.50/0.62 % Estimated wc time : 1092
% 0.50/0.62 % Estimated cpu time (7 cpus) : 156.0
% 0.51/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.51/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.51/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.51/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.51/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.51/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 0.51/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.52/0.98 % Solved by fo/fo5.sh.
% 0.52/0.98 % done 235 iterations in 0.209s
% 0.52/0.98 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 0.52/0.98 % SZS output start Refutation
% 0.52/0.98 thf(rR_type, type, rR: $i > $i > $i > $o).
% 0.52/0.98 thf(vd1178_type, type, vd1178: $i).
% 0.52/0.98 thf(v0_type, type, v0: $i).
% 0.52/0.98 thf(vd1185_type, type, vd1185: $i).
% 0.52/0.98 thf(vd1197_type, type, vd1197: $i).
% 0.52/0.98 thf(vd1200_type, type, vd1200: $i).
% 0.52/0.98 thf(vd1199_type, type, vd1199: $i).
% 0.52/0.98 thf(vd1180_type, type, vd1180: $i).
% 0.52/0.98 thf(vangle_type, type, vangle: $i > $i > $i > $i).
% 0.52/0.98 thf(rpoint_type, type, rpoint: $i > $o).
% 0.52/0.98 thf(sk__3_type, type, sk__3: $i).
% 0.52/0.98 thf(sk__4_type, type, sk__4: $i).
% 0.52/0.98 thf(vd1187_type, type, vd1187: $i).
% 0.52/0.98 thf(sk__1_type, type, sk__1: $i).
% 0.52/0.98 thf(vd1186_type, type, vd1186: $i).
% 0.52/0.98 thf(sk__2_type, type, sk__2: $i).
% 0.52/0.98 thf(vd1179_type, type, vd1179: $i).
% 0.52/0.98 thf(vf_type, type, vf: $i > $i > $i).
% 0.52/0.98 thf(vd684_type, type, vd684: $i).
% 0.52/0.98 thf(sk__6_type, type, sk__6: $i).
% 0.52/0.98 thf(ron_type, type, ron: $i > $i > $o).
% 0.52/0.98 thf(rline_type, type, rline: $i > $o).
% 0.52/0.98 thf('qu(cond(axiom(162), 0), imp(cond(axiom(162), 0)))', axiom,
% 0.52/0.98 (![Vd748:$i,Vd749:$i]:
% 0.52/0.98 ( ( ( ?[Vd752:$i]: ( ( rpoint @ Vd752 ) & ( ( Vd749 ) = ( Vd752 ) ) ) ) &
% 0.52/0.98 ( ?[Vd751:$i]: ( ( rpoint @ Vd751 ) & ( ( Vd748 ) = ( Vd751 ) ) ) ) ) =>
% 0.52/0.98 ( ( ( vf @ Vd748 @ Vd749 ) = ( v0 ) ) <=> ( ( Vd748 ) = ( Vd749 ) ) ) ))).
% 0.52/0.98 thf(zip_derived_cl52, plain,
% 0.52/0.98 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 0.52/0.98 (((X1) != (X0))
% 0.52/0.98 | ~ (rpoint @ X0)
% 0.52/0.98 | ~ (rpoint @ X2)
% 0.52/0.98 | ((X3) != (X2))
% 0.52/0.98 | ((vf @ X1 @ X3) = (v0))
% 0.52/0.98 | ((X1) != (X3)))),
% 0.52/0.98 inference('cnf', [status(esa)],
% 0.52/0.98 [qu(cond(axiom(162), 0), imp(cond(axiom(162), 0)))])).
% 0.52/0.98 thf('pred(axiom(137), 2)', axiom, (( v0 ) = ( vd684 ))).
% 0.52/0.98 thf(zip_derived_cl134, plain, (((v0) = (vd684))),
% 0.52/0.98 inference('cnf', [status(esa)], [pred(axiom(137), 2)])).
% 0.52/0.98 thf(zip_derived_cl666, plain,
% 0.52/0.98 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 0.52/0.98 (((X1) != (X0))
% 0.52/0.98 | ~ (rpoint @ X0)
% 0.52/0.98 | ~ (rpoint @ X2)
% 0.52/0.98 | ((X3) != (X2))
% 0.52/0.98 | ((vf @ X1 @ X3) = (vd684))
% 0.52/0.98 | ((X1) != (X3)))),
% 0.52/0.98 inference('demod', [status(thm)], [zip_derived_cl52, zip_derived_cl134])).
% 0.52/0.98 thf(zip_derived_cl667, plain,
% 0.52/0.98 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.52/0.98 (((X0) != (X1))
% 0.52/0.98 | ((vf @ X0 @ X1) = (vd684))
% 0.52/0.98 | ((X1) != (X2))
% 0.52/0.98 | ~ (rpoint @ X2)
% 0.52/0.98 | ~ (rpoint @ X0))),
% 0.52/0.98 inference('eq_res', [status(thm)], [zip_derived_cl666])).
% 0.52/0.98 thf(zip_derived_cl684, plain,
% 0.52/0.98 (![X0 : $i, X1 : $i]:
% 0.52/0.98 (~ (rpoint @ X0)
% 0.52/0.98 | ~ (rpoint @ X1)
% 0.52/0.98 | ((X0) != (X1))
% 0.52/0.98 | ((vf @ X0 @ X0) = (vd684)))),
% 0.52/0.98 inference('eq_res', [status(thm)], [zip_derived_cl667])).
% 0.52/0.98 thf(zip_derived_cl685, plain,
% 0.52/0.98 (![X0 : $i]:
% 0.52/0.98 (((vf @ X0 @ X0) = (vd684)) | ~ (rpoint @ X0) | ~ (rpoint @ X0))),
% 0.52/0.98 inference('eq_res', [status(thm)], [zip_derived_cl684])).
% 0.52/0.98 thf(zip_derived_cl686, plain,
% 0.52/0.98 (![X0 : $i]: (~ (rpoint @ X0) | ((vf @ X0 @ X0) = (vd684)))),
% 0.52/0.98 inference('simplify', [status(thm)], [zip_derived_cl685])).
% 0.52/0.98 thf('holds(conjunct1(conjunct2(conjunct2(conjunct2(plural(271))))), 1209, 0)', axiom,
% 0.52/0.98 (( vf @ vd1178 @ vd1179 ) = ( vf @ vd1199 @ vd1200 ))).
% 0.52/0.98 thf(zip_derived_cl18, plain,
% 0.52/0.98 (((vf @ vd1178 @ vd1179) = (vf @ vd1199 @ vd1200))),
% 0.52/0.98 inference('cnf', [status(esa)],
% 0.52/0.98 [holds(conjunct1(conjunct2(conjunct2(conjunct2(plural(271))))), 1209, 0)])).
% 0.52/0.98 thf('and(neg(neg(conjunct2(conjunct2(conjunct2(plural(comma_conjunct2(268))))))), and(holds(conjunct1(conjunct2(conjunct2(plural(comma_conjunct2(268))))), 1194, 0), and(holds(conjunct1(conjunct2(plural(comma_conjunct2(268)))), 1193, 0), and(holds(conjunct1(plural(comma_conjunct2(268))), 1192, 0), and(qe(s3(plural(comma_conjunct2(268)))), and(qe(s2(plural(comma_conjunct2(268)))), and(qe(s1(plural(comma_conjunct2(268)))), and(pred(comma_conjunct1(268), 9), and(pred(comma_conjunct1(268), 8), and(pred(comma_conjunct1(268), 7), and(qe(s3(plural(268))), and(qe(s2(plural(268))), qe(s1(plural(268)))))))))))))))', axiom,
% 0.52/0.98 (( ?[Vd1182:$i]: ( ( rpoint @ Vd1182 ) & ( ( vd1178 ) = ( Vd1182 ) ) ) ) &
% 0.52/0.98 ( ?[Vd1183:$i]: ( ( rpoint @ Vd1183 ) & ( ( vd1179 ) = ( Vd1183 ) ) ) ) &
% 0.52/0.98 ( ?[Vd1184:$i]: ( ( rpoint @ Vd1184 ) & ( ( vd1180 ) = ( Vd1184 ) ) ) ) &
% 0.52/0.98 ( ( vd1178 ) != ( vd1179 ) ) & ( ( vd1178 ) != ( vd1180 ) ) &
% 0.52/0.98 ( ( vd1179 ) != ( vd1180 ) ) &
% 0.52/0.98 ( ?[Vd1189:$i]: ( ( rpoint @ Vd1189 ) & ( ( vd1185 ) = ( Vd1189 ) ) ) ) &
% 0.52/0.98 ( ?[Vd1190:$i]: ( ( rpoint @ Vd1190 ) & ( ( vd1186 ) = ( Vd1190 ) ) ) ) &
% 0.52/0.98 ( ?[Vd1191:$i]: ( ( rpoint @ Vd1191 ) & ( ( vd1187 ) = ( Vd1191 ) ) ) ) &
% 0.52/0.98 ( ( vf @ vd1178 @ vd1179 ) = ( vf @ vd1185 @ vd1186 ) ) &
% 0.52/0.98 ( ( vf @ vd1178 @ vd1180 ) = ( vf @ vd1185 @ vd1187 ) ) &
% 0.52/0.98 ( ( vangle @ vd1179 @ vd1178 @ vd1180 ) =
% 0.52/0.98 ( vangle @ vd1186 @ vd1185 @ vd1187 ) ) &
% 0.52/0.98 ( ~( ?[Vd1195:$i]:
% 0.52/0.98 ( ( rline @ Vd1195 ) & ( ron @ vd1185 @ Vd1195 ) &
% 0.52/0.98 ( ron @ vd1186 @ Vd1195 ) & ( ron @ vd1187 @ Vd1195 ) ) ) ))).
% 0.52/0.98 thf(zip_derived_cl47, plain, (((vd1178) = (sk__3))),
% 0.52/0.98 inference('cnf', [status(esa)],
% 0.52/0.98 [and(neg(neg(conjunct2(conjunct2(conjunct2(plural(comma_conjunct2(268))))))), and(holds(conjunct1(conjunct2(conjunct2(plural(comma_conjunct2(268))))), 1194, 0), and(holds(conjunct1(conjunct2(plural(comma_conjunct2(268)))), 1193, 0), and(holds(conjunct1(plural(comma_conjunct2(268))), 1192, 0), and(qe(s3(plural(comma_conjunct2(268)))), and(qe(s2(plural(comma_conjunct2(268)))), and(qe(s1(plural(comma_conjunct2(268)))), and(pred(comma_conjunct1(268), 9), and(pred(comma_conjunct1(268), 8), and(pred(comma_conjunct1(268), 7), and(qe(s3(plural(268))), and(qe(s2(plural(268))), qe(s1(plural(268)))))))))))))))])).
% 0.52/0.98 thf(zip_derived_cl45, plain, (((vd1179) = (sk__4))),
% 0.52/0.98 inference('cnf', [status(esa)],
% 0.52/0.98 [and(neg(neg(conjunct2(conjunct2(conjunct2(plural(comma_conjunct2(268))))))), and(holds(conjunct1(conjunct2(conjunct2(plural(comma_conjunct2(268))))), 1194, 0), and(holds(conjunct1(conjunct2(plural(comma_conjunct2(268)))), 1193, 0), and(holds(conjunct1(plural(comma_conjunct2(268))), 1192, 0), and(qe(s3(plural(comma_conjunct2(268)))), and(qe(s2(plural(comma_conjunct2(268)))), and(qe(s1(plural(comma_conjunct2(268)))), and(pred(comma_conjunct1(268), 9), and(pred(comma_conjunct1(268), 8), and(pred(comma_conjunct1(268), 7), and(qe(s3(plural(268))), and(qe(s2(plural(268))), qe(s1(plural(268)))))))))))))))])).
% 0.52/0.98 thf(qe(s1(plural(271))), axiom,
% 0.52/0.98 (?[Vd1203:$i]: ( ( rpoint @ Vd1203 ) & ( ( vd1199 ) = ( Vd1203 ) ) ))).
% 0.52/0.98 thf(zip_derived_cl26, plain, (((vd1199) = (sk__2))),
% 0.52/0.98 inference('cnf', [status(esa)], [qe(s1(plural(271)))])).
% 0.52/0.98 thf(qe(s2(plural(271))), axiom,
% 0.52/0.98 (?[Vd1204:$i]: ( ( rpoint @ Vd1204 ) & ( ( vd1200 ) = ( Vd1204 ) ) ))).
% 0.52/0.98 thf(zip_derived_cl24, plain, (((vd1200) = (sk__1))),
% 0.52/0.98 inference('cnf', [status(esa)], [qe(s2(plural(271)))])).
% 0.52/0.98 thf(zip_derived_cl386, plain,
% 0.52/0.98 (((vf @ sk__3 @ sk__4) = (vf @ sk__2 @ sk__1))),
% 0.52/0.98 inference('demod', [status(thm)],
% 0.52/0.98 [zip_derived_cl18, zip_derived_cl47, zip_derived_cl45,
% 0.52/0.98 zip_derived_cl26, zip_derived_cl24])).
% 0.52/0.98 thf('pred(s1(plural(269)), 0)', axiom, (ron @ vd1185 @ vd1197)).
% 0.52/0.98 thf(zip_derived_cl5, plain, ( (ron @ vd1185 @ vd1197)),
% 0.52/0.98 inference('cnf', [status(esa)], [pred(s1(plural(269)), 0)])).
% 0.52/0.98 thf(zip_derived_cl38, plain, (((vd1185) = (sk__6))),
% 0.52/0.98 inference('cnf', [status(esa)],
% 0.52/0.98 [and(neg(neg(conjunct2(conjunct2(conjunct2(plural(comma_conjunct2(268))))))), and(holds(conjunct1(conjunct2(conjunct2(plural(comma_conjunct2(268))))), 1194, 0), and(holds(conjunct1(conjunct2(plural(comma_conjunct2(268)))), 1193, 0), and(holds(conjunct1(plural(comma_conjunct2(268))), 1192, 0), and(qe(s3(plural(comma_conjunct2(268)))), and(qe(s2(plural(comma_conjunct2(268)))), and(qe(s1(plural(comma_conjunct2(268)))), and(pred(comma_conjunct1(268), 9), and(pred(comma_conjunct1(268), 8), and(pred(comma_conjunct1(268), 7), and(qe(s3(plural(268))), and(qe(s2(plural(268))), qe(s1(plural(268)))))))))))))))])).
% 0.52/0.98 thf(zip_derived_cl318, plain, ( (ron @ sk__6 @ vd1197)),
% 0.52/0.98 inference('demod', [status(thm)], [zip_derived_cl5, zip_derived_cl38])).
% 0.52/0.98 thf('pred(s2(plural(274)), 0)', axiom, (ron @ vd1200 @ vd1197)).
% 0.52/0.98 thf(zip_derived_cl4, plain, ( (ron @ vd1200 @ vd1197)),
% 0.52/0.98 inference('cnf', [status(esa)], [pred(s2(plural(274)), 0)])).
% 0.52/0.98 thf(zip_derived_cl24, plain, (((vd1200) = (sk__1))),
% 0.52/0.98 inference('cnf', [status(esa)], [qe(s2(plural(271)))])).
% 0.52/0.98 thf(zip_derived_cl312, plain, ( (ron @ sk__1 @ vd1197)),
% 0.52/0.98 inference('demod', [status(thm)], [zip_derived_cl4, zip_derived_cl24])).
% 0.52/0.98 thf('pred(s1(plural(274)), 0)', axiom, (ron @ vd1199 @ vd1197)).
% 0.52/0.98 thf(zip_derived_cl6, plain, ( (ron @ vd1199 @ vd1197)),
% 0.52/0.98 inference('cnf', [status(esa)], [pred(s1(plural(274)), 0)])).
% 0.52/0.98 thf(zip_derived_cl26, plain, (((vd1199) = (sk__2))),
% 0.52/0.98 inference('cnf', [status(esa)], [qe(s1(plural(271)))])).
% 0.52/0.98 thf(zip_derived_cl320, plain, ( (ron @ sk__2 @ vd1197)),
% 0.52/0.98 inference('demod', [status(thm)], [zip_derived_cl6, zip_derived_cl26])).
% 0.52/0.98 thf('qu(cond(axiom(91), 0), imp(cond(axiom(91), 0)))', axiom,
% 0.52/0.98 (![Vd396:$i,Vd397:$i,Vd398:$i,Vd403:$i,Vd404:$i]:
% 0.52/0.98 ( ( ( ( Vd403 ) = ( Vd404 ) ) & ( ron @ Vd398 @ Vd403 ) &
% 0.52/0.98 ( ron @ Vd397 @ Vd403 ) & ( ron @ Vd396 @ Vd403 ) &
% 0.52/0.98 ( rline @ Vd404 ) & ( ( Vd397 ) != ( Vd398 ) ) &
% 0.52/0.98 ( ( Vd396 ) != ( Vd398 ) ) & ( ( Vd396 ) != ( Vd397 ) ) &
% 0.52/0.98 ( ?[Vd402:$i]: ( ( rpoint @ Vd402 ) & ( ( Vd398 ) = ( Vd402 ) ) ) ) &
% 0.52/0.98 ( ?[Vd401:$i]: ( ( rpoint @ Vd401 ) & ( ( Vd397 ) = ( Vd401 ) ) ) ) &
% 0.52/0.98 ( ?[Vd400:$i]: ( ( rpoint @ Vd400 ) & ( ( Vd396 ) = ( Vd400 ) ) ) ) ) =>
% 0.52/0.98 ( ( rR @ Vd397 @ Vd396 @ Vd398 ) | ( rR @ Vd396 @ Vd397 @ Vd398 ) |
% 0.52/0.98 ( rR @ Vd398 @ Vd396 @ Vd397 ) ) ))).
% 0.52/0.98 thf(zip_derived_cl9, plain,
% 0.52/0.98 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i, X6 : $i, X7 : $i]:
% 0.52/0.98 ( (rR @ X0 @ X1 @ X2)
% 0.52/0.98 | (rR @ X1 @ X2 @ X0)
% 0.52/0.98 | (rR @ X2 @ X1 @ X0)
% 0.52/0.98 | ((X1) != (X3))
% 0.52/0.98 | ~ (rpoint @ X3)
% 0.52/0.98 | ((X2) != (X4))
% 0.52/0.98 | ~ (rpoint @ X4)
% 0.52/0.98 | ((X0) != (X5))
% 0.52/0.98 | ~ (rpoint @ X5)
% 0.52/0.98 | ((X1) = (X2))
% 0.52/0.98 | ((X1) = (X0))
% 0.52/0.98 | ((X2) = (X0))
% 0.52/0.98 | ~ (ron @ X1 @ X6)
% 0.52/0.98 | ~ (ron @ X2 @ X6)
% 0.52/0.98 | ~ (ron @ X0 @ X6)
% 0.52/0.98 | ((X6) != (X7))
% 0.52/0.98 | ~ (rline @ X7))),
% 0.52/0.98 inference('cnf', [status(esa)],
% 0.52/0.98 [qu(cond(axiom(91), 0), imp(cond(axiom(91), 0)))])).
% 0.52/0.98 thf(zip_derived_cl329, plain,
% 0.52/0.98 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i, X6 : $i]:
% 0.52/0.98 (~ (rline @ X0)
% 0.52/0.98 | ((X1) != (X0))
% 0.52/0.98 | ~ (ron @ X2 @ X1)
% 0.52/0.98 | ~ (ron @ X3 @ X1)
% 0.52/0.98 | ~ (ron @ X4 @ X1)
% 0.52/0.98 | ((X3) = (X2))
% 0.52/0.98 | ((X4) = (X2))
% 0.52/0.98 | ((X4) = (X3))
% 0.52/0.98 | ~ (rpoint @ X5)
% 0.52/0.98 | ((X2) != (X5))
% 0.52/0.98 | ~ (rpoint @ X6)
% 0.52/0.98 | ((X3) != (X6))
% 0.52/0.98 | ~ (rpoint @ X4)
% 0.52/0.98 | (rR @ X3 @ X4 @ X2)
% 0.52/0.98 | (rR @ X4 @ X3 @ X2)
% 0.52/0.98 | (rR @ X2 @ X4 @ X3))),
% 0.52/0.98 inference('eq_res', [status(thm)], [zip_derived_cl9])).
% 0.52/0.98 thf(zip_derived_cl330, plain,
% 0.52/0.98 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 0.52/0.98 ( (rR @ X2 @ X1 @ X0)
% 0.52/0.98 | (rR @ X1 @ X0 @ X2)
% 0.52/0.98 | (rR @ X0 @ X1 @ X2)
% 0.52/0.98 | ~ (rpoint @ X1)
% 0.52/0.98 | ((X0) != (X3))
% 0.52/0.98 | ~ (rpoint @ X3)
% 0.52/0.98 | ((X2) != (X4))
% 0.52/0.98 | ~ (rpoint @ X4)
% 0.52/0.98 | ((X1) = (X0))
% 0.52/0.98 | ((X1) = (X2))
% 0.52/0.98 | ((X0) = (X2))
% 0.52/0.98 | ~ (ron @ X1 @ X5)
% 0.52/0.98 | ~ (ron @ X0 @ X5)
% 0.52/0.98 | ~ (ron @ X2 @ X5)
% 0.52/0.98 | ~ (rline @ X5))),
% 0.52/0.98 inference('eq_res', [status(thm)], [zip_derived_cl329])).
% 0.52/0.98 thf(zip_derived_cl331, plain,
% 0.52/0.98 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 0.52/0.98 (~ (rline @ X0)
% 0.52/0.98 | ~ (ron @ X1 @ X0)
% 0.52/0.98 | ~ (ron @ X2 @ X0)
% 0.52/0.98 | ~ (ron @ X3 @ X0)
% 0.52/0.98 | ((X2) = (X1))
% 0.52/0.98 | ((X3) = (X1))
% 0.52/0.98 | ((X3) = (X2))
% 0.52/0.98 | ~ (rpoint @ X4)
% 0.52/0.98 | ((X1) != (X4))
% 0.52/0.98 | ~ (rpoint @ X2)
% 0.52/0.98 | ~ (rpoint @ X3)
% 0.52/0.98 | (rR @ X2 @ X3 @ X1)
% 0.52/0.98 | (rR @ X3 @ X2 @ X1)
% 0.52/0.98 | (rR @ X1 @ X3 @ X2))),
% 0.52/0.98 inference('eq_res', [status(thm)], [zip_derived_cl330])).
% 0.52/0.98 thf(zip_derived_cl332, plain,
% 0.52/0.98 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 0.52/0.98 ( (rR @ X2 @ X1 @ X0)
% 0.52/0.98 | (rR @ X1 @ X0 @ X2)
% 0.52/0.98 | (rR @ X0 @ X1 @ X2)
% 0.52/0.98 | ~ (rpoint @ X1)
% 0.52/0.98 | ~ (rpoint @ X0)
% 0.52/0.98 | ~ (rpoint @ X2)
% 0.52/0.98 | ((X1) = (X0))
% 0.52/0.98 | ((X1) = (X2))
% 0.52/0.98 | ((X0) = (X2))
% 0.52/0.98 | ~ (ron @ X1 @ X3)
% 0.52/0.98 | ~ (ron @ X0 @ X3)
% 0.52/0.98 | ~ (ron @ X2 @ X3)
% 0.52/0.98 | ~ (rline @ X3))),
% 0.52/0.98 inference('eq_res', [status(thm)], [zip_derived_cl331])).
% 0.52/0.98 thf(zip_derived_cl334, plain,
% 0.52/0.98 (![X0 : $i, X1 : $i]:
% 0.52/0.98 (~ (rline @ vd1197)
% 0.52/0.98 | ~ (ron @ X0 @ vd1197)
% 0.52/0.98 | ~ (ron @ X1 @ vd1197)
% 0.52/0.98 | ((X1) = (X0))
% 0.52/0.98 | ((sk__2) = (X0))
% 0.52/0.98 | ((sk__2) = (X1))
% 0.52/0.98 | ~ (rpoint @ X0)
% 0.52/0.98 | ~ (rpoint @ X1)
% 0.52/0.98 | ~ (rpoint @ sk__2)
% 0.52/0.98 | (rR @ X1 @ sk__2 @ X0)
% 0.52/0.98 | (rR @ sk__2 @ X1 @ X0)
% 0.52/0.98 | (rR @ X0 @ sk__2 @ X1))),
% 0.52/0.98 inference('sup-', [status(thm)], [zip_derived_cl320, zip_derived_cl332])).
% 0.52/0.98 thf('pred(269, 0)', axiom, (rline @ vd1197)).
% 0.52/0.98 thf(zip_derived_cl12, plain, ( (rline @ vd1197)),
% 0.52/0.98 inference('cnf', [status(esa)], [pred(269, 0)])).
% 0.52/0.98 thf(zip_derived_cl27, plain, ( (rpoint @ sk__2)),
% 0.52/0.98 inference('cnf', [status(esa)], [qe(s1(plural(271)))])).
% 0.52/0.98 thf(zip_derived_cl341, plain,
% 0.52/0.98 (![X0 : $i, X1 : $i]:
% 0.52/0.98 (~ (ron @ X0 @ vd1197)
% 0.52/0.98 | ~ (ron @ X1 @ vd1197)
% 0.52/0.98 | ((X1) = (X0))
% 0.52/0.98 | ((sk__2) = (X0))
% 0.52/0.98 | ((sk__2) = (X1))
% 0.52/0.98 | ~ (rpoint @ X0)
% 0.52/0.98 | ~ (rpoint @ X1)
% 0.52/0.98 | (rR @ X1 @ sk__2 @ X0)
% 0.52/0.98 | (rR @ sk__2 @ X1 @ X0)
% 0.52/0.98 | (rR @ X0 @ sk__2 @ X1))),
% 0.52/0.98 inference('demod', [status(thm)],
% 0.52/0.98 [zip_derived_cl334, zip_derived_cl12, zip_derived_cl27])).
% 0.52/0.98 thf(zip_derived_cl390, plain,
% 0.52/0.98 (![X0 : $i]:
% 0.52/0.98 ( (rR @ sk__1 @ sk__2 @ X0)
% 0.52/0.98 | (rR @ sk__2 @ X0 @ sk__1)
% 0.52/0.98 | (rR @ X0 @ sk__2 @ sk__1)
% 0.52/0.98 | ~ (rpoint @ X0)
% 0.52/0.98 | ~ (rpoint @ sk__1)
% 0.52/0.98 | ((sk__2) = (X0))
% 0.52/0.98 | ((sk__2) = (sk__1))
% 0.52/0.98 | ((X0) = (sk__1))
% 0.52/0.98 | ~ (ron @ X0 @ vd1197))),
% 0.52/0.98 inference('sup-', [status(thm)], [zip_derived_cl312, zip_derived_cl341])).
% 0.52/0.98 thf(zip_derived_cl25, plain, ( (rpoint @ sk__1)),
% 0.52/0.98 inference('cnf', [status(esa)], [qe(s2(plural(271)))])).
% 0.52/0.98 thf(zip_derived_cl395, plain,
% 0.52/0.98 (![X0 : $i]:
% 0.52/0.98 ( (rR @ sk__1 @ sk__2 @ X0)
% 0.52/0.98 | (rR @ sk__2 @ X0 @ sk__1)
% 0.52/0.98 | (rR @ X0 @ sk__2 @ sk__1)
% 0.52/0.98 | ~ (rpoint @ X0)
% 0.52/0.98 | ((sk__2) = (X0))
% 0.52/0.98 | ((sk__2) = (sk__1))
% 0.52/0.98 | ((X0) = (sk__1))
% 0.52/0.98 | ~ (ron @ X0 @ vd1197))),
% 0.52/0.98 inference('demod', [status(thm)], [zip_derived_cl390, zip_derived_cl25])).
% 0.52/0.98 thf(zip_derived_cl498, plain,
% 0.52/0.98 ((((sk__6) = (sk__1))
% 0.52/0.98 | ((sk__2) = (sk__1))
% 0.52/0.98 | ((sk__2) = (sk__6))
% 0.52/0.98 | ~ (rpoint @ sk__6)
% 0.52/0.98 | (rR @ sk__6 @ sk__2 @ sk__1)
% 0.52/0.98 | (rR @ sk__2 @ sk__6 @ sk__1)
% 0.52/0.98 | (rR @ sk__1 @ sk__2 @ sk__6))),
% 0.52/0.98 inference('sup-', [status(thm)], [zip_derived_cl318, zip_derived_cl395])).
% 0.52/0.98 thf(zip_derived_cl37, plain, ( (rpoint @ sk__6)),
% 0.52/0.98 inference('cnf', [status(esa)],
% 0.52/0.98 [and(neg(neg(conjunct2(conjunct2(conjunct2(plural(comma_conjunct2(268))))))), and(holds(conjunct1(conjunct2(conjunct2(plural(comma_conjunct2(268))))), 1194, 0), and(holds(conjunct1(conjunct2(plural(comma_conjunct2(268)))), 1193, 0), and(holds(conjunct1(plural(comma_conjunct2(268))), 1192, 0), and(qe(s3(plural(comma_conjunct2(268)))), and(qe(s2(plural(comma_conjunct2(268)))), and(qe(s1(plural(comma_conjunct2(268)))), and(pred(comma_conjunct1(268), 9), and(pred(comma_conjunct1(268), 8), and(pred(comma_conjunct1(268), 7), and(qe(s3(plural(268))), and(qe(s2(plural(268))), qe(s1(plural(268)))))))))))))))])).
% 0.52/0.98 thf(dis(276), conjecture,
% 0.52/0.98 (( rR @ vd1199 @ vd1185 @ vd1186 ) | ( rR @ vd1185 @ vd1199 @ vd1186 ))).
% 0.52/0.98 thf(zf_stmt_0, negated_conjecture,
% 0.52/0.98 (~( ( rR @ vd1199 @ vd1185 @ vd1186 ) | ( rR @ vd1185 @ vd1199 @ vd1186 ) )),
% 0.52/0.98 inference('cnf.neg', [status(esa)], [dis(276)])).
% 0.52/0.98 thf(zip_derived_cl1, plain, (~ (rR @ vd1199 @ vd1185 @ vd1186)),
% 0.52/0.98 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.52/0.98 thf('holds(conjunct1(comma_conjunct2(plural(271))), 1212, 0)', axiom,
% 0.52/0.98 (( vd1200 ) = ( vd1186 ))).
% 0.52/0.98 thf(zip_derived_cl7, plain, (((vd1200) = (vd1186))),
% 0.52/0.98 inference('cnf', [status(esa)],
% 0.52/0.98 [holds(conjunct1(comma_conjunct2(plural(271))), 1212, 0)])).
% 0.52/0.98 thf(zip_derived_cl296, plain, (~ (rR @ vd1199 @ vd1185 @ vd1200)),
% 0.52/0.98 inference('demod', [status(thm)], [zip_derived_cl1, zip_derived_cl7])).
% 0.52/0.98 thf(zip_derived_cl26, plain, (((vd1199) = (sk__2))),
% 0.52/0.98 inference('cnf', [status(esa)], [qe(s1(plural(271)))])).
% 0.52/0.98 thf(zip_derived_cl24, plain, (((vd1200) = (sk__1))),
% 0.52/0.98 inference('cnf', [status(esa)], [qe(s2(plural(271)))])).
% 0.52/0.98 thf(zip_derived_cl301, plain, (~ (rR @ sk__2 @ vd1185 @ sk__1)),
% 0.52/0.98 inference('demod', [status(thm)],
% 0.52/0.98 [zip_derived_cl296, zip_derived_cl26, zip_derived_cl24])).
% 0.52/0.98 thf(zip_derived_cl38, plain, (((vd1185) = (sk__6))),
% 0.52/0.98 inference('cnf', [status(esa)],
% 0.52/0.98 [and(neg(neg(conjunct2(conjunct2(conjunct2(plural(comma_conjunct2(268))))))), and(holds(conjunct1(conjunct2(conjunct2(plural(comma_conjunct2(268))))), 1194, 0), and(holds(conjunct1(conjunct2(plural(comma_conjunct2(268)))), 1193, 0), and(holds(conjunct1(plural(comma_conjunct2(268))), 1192, 0), and(qe(s3(plural(comma_conjunct2(268)))), and(qe(s2(plural(comma_conjunct2(268)))), and(qe(s1(plural(comma_conjunct2(268)))), and(pred(comma_conjunct1(268), 9), and(pred(comma_conjunct1(268), 8), and(pred(comma_conjunct1(268), 7), and(qe(s3(plural(268))), and(qe(s2(plural(268))), qe(s1(plural(268)))))))))))))))])).
% 0.52/0.98 thf(zip_derived_cl306, plain, (~ (rR @ sk__2 @ sk__6 @ sk__1)),
% 0.52/0.98 inference('demod', [status(thm)], [zip_derived_cl301, zip_derived_cl38])).
% 0.52/0.98 thf(neg(neg(conjunct2(conjunct2(comma_conjunct2(plural(271)))))), axiom,
% 0.52/0.98 (~( rR @ vd1186 @ vd1199 @ vd1185 ))).
% 0.52/0.98 thf(zip_derived_cl14, plain, (~ (rR @ vd1186 @ vd1199 @ vd1185)),
% 0.52/0.98 inference('cnf', [status(esa)],
% 0.52/0.98 [neg(neg(conjunct2(conjunct2(comma_conjunct2(plural(271))))))])).
% 0.52/0.98 thf(zip_derived_cl7, plain, (((vd1200) = (vd1186))),
% 0.52/0.98 inference('cnf', [status(esa)],
% 0.52/0.98 [holds(conjunct1(comma_conjunct2(plural(271))), 1212, 0)])).
% 0.52/0.98 thf(zip_derived_cl297, plain, (~ (rR @ vd1200 @ vd1199 @ vd1185)),
% 0.52/0.98 inference('demod', [status(thm)], [zip_derived_cl14, zip_derived_cl7])).
% 0.52/0.98 thf(zip_derived_cl24, plain, (((vd1200) = (sk__1))),
% 0.52/0.98 inference('cnf', [status(esa)], [qe(s2(plural(271)))])).
% 0.52/0.98 thf(zip_derived_cl26, plain, (((vd1199) = (sk__2))),
% 0.52/0.98 inference('cnf', [status(esa)], [qe(s1(plural(271)))])).
% 0.52/0.98 thf(zip_derived_cl302, plain, (~ (rR @ sk__1 @ sk__2 @ vd1185)),
% 0.52/0.98 inference('demod', [status(thm)],
% 0.52/0.98 [zip_derived_cl297, zip_derived_cl24, zip_derived_cl26])).
% 0.52/0.98 thf(zip_derived_cl38, plain, (((vd1185) = (sk__6))),
% 0.52/0.98 inference('cnf', [status(esa)],
% 0.52/0.98 [and(neg(neg(conjunct2(conjunct2(conjunct2(plural(comma_conjunct2(268))))))), and(holds(conjunct1(conjunct2(conjunct2(plural(comma_conjunct2(268))))), 1194, 0), and(holds(conjunct1(conjunct2(plural(comma_conjunct2(268)))), 1193, 0), and(holds(conjunct1(plural(comma_conjunct2(268))), 1192, 0), and(qe(s3(plural(comma_conjunct2(268)))), and(qe(s2(plural(comma_conjunct2(268)))), and(qe(s1(plural(comma_conjunct2(268)))), and(pred(comma_conjunct1(268), 9), and(pred(comma_conjunct1(268), 8), and(pred(comma_conjunct1(268), 7), and(qe(s3(plural(268))), and(qe(s2(plural(268))), qe(s1(plural(268)))))))))))))))])).
% 0.52/0.98 thf(zip_derived_cl307, plain, (~ (rR @ sk__1 @ sk__2 @ sk__6)),
% 0.52/0.98 inference('demod', [status(thm)], [zip_derived_cl302, zip_derived_cl38])).
% 0.52/0.98 thf(zip_derived_cl505, plain,
% 0.52/0.98 ((((sk__6) = (sk__1))
% 0.52/0.98 | ((sk__2) = (sk__1))
% 0.52/0.98 | ((sk__2) = (sk__6))
% 0.52/0.98 | (rR @ sk__6 @ sk__2 @ sk__1))),
% 0.52/0.98 inference('demod', [status(thm)],
% 0.52/0.98 [zip_derived_cl498, zip_derived_cl37, zip_derived_cl306,
% 0.52/0.98 zip_derived_cl307])).
% 0.52/0.98 thf('holds(275, 1217, 0)', axiom, (( vd1199 ) != ( vd1185 ))).
% 0.52/0.98 thf(zip_derived_cl2, plain, (((vd1199) != (vd1185))),
% 0.52/0.98 inference('cnf', [status(esa)], [holds(275, 1217, 0)])).
% 0.52/0.98 thf(zip_derived_cl26, plain, (((vd1199) = (sk__2))),
% 0.52/0.98 inference('cnf', [status(esa)], [qe(s1(plural(271)))])).
% 0.52/0.98 thf(zip_derived_cl299, plain, (((sk__2) != (vd1185))),
% 0.52/0.98 inference('demod', [status(thm)], [zip_derived_cl2, zip_derived_cl26])).
% 0.52/0.98 thf(zip_derived_cl38, plain, (((vd1185) = (sk__6))),
% 0.52/0.98 inference('cnf', [status(esa)],
% 0.52/0.98 [and(neg(neg(conjunct2(conjunct2(conjunct2(plural(comma_conjunct2(268))))))), and(holds(conjunct1(conjunct2(conjunct2(plural(comma_conjunct2(268))))), 1194, 0), and(holds(conjunct1(conjunct2(plural(comma_conjunct2(268)))), 1193, 0), and(holds(conjunct1(plural(comma_conjunct2(268))), 1192, 0), and(qe(s3(plural(comma_conjunct2(268)))), and(qe(s2(plural(comma_conjunct2(268)))), and(qe(s1(plural(comma_conjunct2(268)))), and(pred(comma_conjunct1(268), 9), and(pred(comma_conjunct1(268), 8), and(pred(comma_conjunct1(268), 7), and(qe(s3(plural(268))), and(qe(s2(plural(268))), qe(s1(plural(268)))))))))))))))])).
% 0.52/0.98 thf(zip_derived_cl304, plain, (((sk__2) != (sk__6))),
% 0.52/0.98 inference('demod', [status(thm)], [zip_derived_cl299, zip_derived_cl38])).
% 0.52/0.98 thf(zip_derived_cl506, plain,
% 0.52/0.98 ((((sk__6) = (sk__1))
% 0.52/0.98 | ((sk__2) = (sk__1))
% 0.52/0.98 | (rR @ sk__6 @ sk__2 @ sk__1))),
% 0.52/0.98 inference('simplify_reflect-', [status(thm)],
% 0.52/0.98 [zip_derived_cl505, zip_derived_cl304])).
% 0.52/0.98 thf(zip_derived_cl0, plain, (~ (rR @ vd1185 @ vd1199 @ vd1186)),
% 0.52/0.98 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.52/0.98 thf(zip_derived_cl7, plain, (((vd1200) = (vd1186))),
% 0.52/0.98 inference('cnf', [status(esa)],
% 0.52/0.98 [holds(conjunct1(comma_conjunct2(plural(271))), 1212, 0)])).
% 0.52/0.98 thf(zip_derived_cl295, plain, (~ (rR @ vd1185 @ vd1199 @ vd1200)),
% 0.52/0.98 inference('demod', [status(thm)], [zip_derived_cl0, zip_derived_cl7])).
% 0.52/0.98 thf(zip_derived_cl26, plain, (((vd1199) = (sk__2))),
% 0.52/0.98 inference('cnf', [status(esa)], [qe(s1(plural(271)))])).
% 0.52/0.98 thf(zip_derived_cl24, plain, (((vd1200) = (sk__1))),
% 0.52/0.98 inference('cnf', [status(esa)], [qe(s2(plural(271)))])).
% 0.52/0.98 thf(zip_derived_cl300, plain, (~ (rR @ vd1185 @ sk__2 @ sk__1)),
% 0.52/0.98 inference('demod', [status(thm)],
% 0.52/0.98 [zip_derived_cl295, zip_derived_cl26, zip_derived_cl24])).
% 0.52/0.98 thf(zip_derived_cl38, plain, (((vd1185) = (sk__6))),
% 0.52/0.98 inference('cnf', [status(esa)],
% 0.52/0.98 [and(neg(neg(conjunct2(conjunct2(conjunct2(plural(comma_conjunct2(268))))))), and(holds(conjunct1(conjunct2(conjunct2(plural(comma_conjunct2(268))))), 1194, 0), and(holds(conjunct1(conjunct2(plural(comma_conjunct2(268)))), 1193, 0), and(holds(conjunct1(plural(comma_conjunct2(268))), 1192, 0), and(qe(s3(plural(comma_conjunct2(268)))), and(qe(s2(plural(comma_conjunct2(268)))), and(qe(s1(plural(comma_conjunct2(268)))), and(pred(comma_conjunct1(268), 9), and(pred(comma_conjunct1(268), 8), and(pred(comma_conjunct1(268), 7), and(qe(s3(plural(268))), and(qe(s2(plural(268))), qe(s1(plural(268)))))))))))))))])).
% 0.52/0.98 thf(zip_derived_cl305, plain, (~ (rR @ sk__6 @ sk__2 @ sk__1)),
% 0.52/0.98 inference('demod', [status(thm)], [zip_derived_cl300, zip_derived_cl38])).
% 0.52/0.98 thf(zip_derived_cl532, plain, ((((sk__2) = (sk__1)) | ((sk__6) = (sk__1)))),
% 0.52/0.98 inference('clc', [status(thm)], [zip_derived_cl506, zip_derived_cl305])).
% 0.52/0.98 thf('holds(273, 1215, 0)', axiom,
% 0.52/0.98 (( vf @ vd1199 @ vd1200 ) = ( vf @ vd1185 @ vd1186 ))).
% 0.52/0.98 thf(zip_derived_cl10, plain,
% 0.52/0.98 (((vf @ vd1199 @ vd1200) = (vf @ vd1185 @ vd1186))),
% 0.52/0.98 inference('cnf', [status(esa)], [holds(273, 1215, 0)])).
% 0.52/0.98 thf(zip_derived_cl26, plain, (((vd1199) = (sk__2))),
% 0.52/0.98 inference('cnf', [status(esa)], [qe(s1(plural(271)))])).
% 0.52/0.98 thf(zip_derived_cl24, plain, (((vd1200) = (sk__1))),
% 0.52/0.98 inference('cnf', [status(esa)], [qe(s2(plural(271)))])).
% 0.52/0.98 thf(zip_derived_cl38, plain, (((vd1185) = (sk__6))),
% 0.52/0.98 inference('cnf', [status(esa)],
% 0.52/0.98 [and(neg(neg(conjunct2(conjunct2(conjunct2(plural(comma_conjunct2(268))))))), and(holds(conjunct1(conjunct2(conjunct2(plural(comma_conjunct2(268))))), 1194, 0), and(holds(conjunct1(conjunct2(plural(comma_conjunct2(268)))), 1193, 0), and(holds(conjunct1(plural(comma_conjunct2(268))), 1192, 0), and(qe(s3(plural(comma_conjunct2(268)))), and(qe(s2(plural(comma_conjunct2(268)))), and(qe(s1(plural(comma_conjunct2(268)))), and(pred(comma_conjunct1(268), 9), and(pred(comma_conjunct1(268), 8), and(pred(comma_conjunct1(268), 7), and(qe(s3(plural(268))), and(qe(s2(plural(268))), qe(s1(plural(268)))))))))))))))])).
% 0.52/0.98 thf(zip_derived_cl7, plain, (((vd1200) = (vd1186))),
% 0.52/0.98 inference('cnf', [status(esa)],
% 0.52/0.98 [holds(conjunct1(comma_conjunct2(plural(271))), 1212, 0)])).
% 0.52/0.98 thf(zip_derived_cl24, plain, (((vd1200) = (sk__1))),
% 0.52/0.98 inference('cnf', [status(esa)], [qe(s2(plural(271)))])).
% 0.52/0.98 thf(zip_derived_cl298, plain, (((sk__1) = (vd1186))),
% 0.52/0.98 inference('demod', [status(thm)], [zip_derived_cl7, zip_derived_cl24])).
% 0.52/0.98 thf(zip_derived_cl328, plain,
% 0.52/0.98 (((vf @ sk__2 @ sk__1) = (vf @ sk__6 @ sk__1))),
% 0.52/0.98 inference('demod', [status(thm)],
% 0.52/0.98 [zip_derived_cl10, zip_derived_cl26, zip_derived_cl24,
% 0.52/0.98 zip_derived_cl38, zip_derived_cl298])).
% 0.52/0.98 thf(zip_derived_cl540, plain,
% 0.52/0.98 ((((vf @ sk__2 @ sk__1) = (vf @ sk__1 @ sk__1)) | ((sk__2) = (sk__1)))),
% 0.52/0.98 inference('sup+', [status(thm)], [zip_derived_cl532, zip_derived_cl328])).
% 0.52/0.98 thf(zip_derived_cl595, plain,
% 0.52/0.98 (((vf @ sk__2 @ sk__1) = (vf @ sk__1 @ sk__1))),
% 0.52/0.98 inference('condensation', [status(thm)], [zip_derived_cl540])).
% 0.52/0.98 thf(zip_derived_cl597, plain,
% 0.52/0.98 (((vf @ sk__3 @ sk__4) = (vf @ sk__1 @ sk__1))),
% 0.52/0.98 inference('demod', [status(thm)], [zip_derived_cl386, zip_derived_cl595])).
% 0.52/0.98 thf(zip_derived_cl51, plain,
% 0.52/0.98 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 0.52/0.98 (((X1) != (X0))
% 0.52/0.98 | ~ (rpoint @ X0)
% 0.52/0.98 | ~ (rpoint @ X2)
% 0.52/0.98 | ((X3) != (X2))
% 0.52/0.98 | ((X1) = (X3))
% 0.52/0.98 | ((vf @ X1 @ X3) != (v0)))),
% 0.52/0.98 inference('cnf', [status(esa)],
% 0.52/0.98 [qu(cond(axiom(162), 0), imp(cond(axiom(162), 0)))])).
% 0.52/0.98 thf(zip_derived_cl134, plain, (((v0) = (vd684))),
% 0.52/0.98 inference('cnf', [status(esa)], [pred(axiom(137), 2)])).
% 0.52/0.98 thf(zip_derived_cl632, plain,
% 0.52/0.98 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 0.52/0.98 (((X1) != (X0))
% 0.52/0.98 | ~ (rpoint @ X0)
% 0.52/0.98 | ~ (rpoint @ X2)
% 0.52/0.98 | ((X3) != (X2))
% 0.52/0.98 | ((X1) = (X3))
% 0.52/0.98 | ((vf @ X1 @ X3) != (vd684)))),
% 0.52/0.98 inference('demod', [status(thm)], [zip_derived_cl51, zip_derived_cl134])).
% 0.52/0.98 thf(zip_derived_cl635, plain,
% 0.52/0.98 (![X0 : $i, X1 : $i]:
% 0.52/0.98 (((vf @ sk__1 @ sk__1) != (vd684))
% 0.52/0.98 | ((sk__3) = (sk__4))
% 0.52/0.98 | ((sk__4) != (X0))
% 0.52/0.98 | ~ (rpoint @ X0)
% 0.52/0.98 | ~ (rpoint @ X1)
% 0.52/0.98 | ((sk__3) != (X1)))),
% 0.52/0.98 inference('sup-', [status(thm)], [zip_derived_cl597, zip_derived_cl632])).
% 0.52/0.98 thf(zip_derived_cl41, plain, (((vd1178) != (vd1179))),
% 0.52/0.98 inference('cnf', [status(esa)],
% 0.52/0.98 [and(neg(neg(conjunct2(conjunct2(conjunct2(plural(comma_conjunct2(268))))))), and(holds(conjunct1(conjunct2(conjunct2(plural(comma_conjunct2(268))))), 1194, 0), and(holds(conjunct1(conjunct2(plural(comma_conjunct2(268)))), 1193, 0), and(holds(conjunct1(plural(comma_conjunct2(268))), 1192, 0), and(qe(s3(plural(comma_conjunct2(268)))), and(qe(s2(plural(comma_conjunct2(268)))), and(qe(s1(plural(comma_conjunct2(268)))), and(pred(comma_conjunct1(268), 9), and(pred(comma_conjunct1(268), 8), and(pred(comma_conjunct1(268), 7), and(qe(s3(plural(268))), and(qe(s2(plural(268))), qe(s1(plural(268)))))))))))))))])).
% 0.52/0.98 thf(zip_derived_cl45, plain, (((vd1179) = (sk__4))),
% 0.52/0.98 inference('cnf', [status(esa)],
% 0.52/0.98 [and(neg(neg(conjunct2(conjunct2(conjunct2(plural(comma_conjunct2(268))))))), and(holds(conjunct1(conjunct2(conjunct2(plural(comma_conjunct2(268))))), 1194, 0), and(holds(conjunct1(conjunct2(plural(comma_conjunct2(268)))), 1193, 0), and(holds(conjunct1(plural(comma_conjunct2(268))), 1192, 0), and(qe(s3(plural(comma_conjunct2(268)))), and(qe(s2(plural(comma_conjunct2(268)))), and(qe(s1(plural(comma_conjunct2(268)))), and(pred(comma_conjunct1(268), 9), and(pred(comma_conjunct1(268), 8), and(pred(comma_conjunct1(268), 7), and(qe(s3(plural(268))), and(qe(s2(plural(268))), qe(s1(plural(268)))))))))))))))])).
% 0.52/0.98 thf(zip_derived_cl311, plain, (((vd1178) != (sk__4))),
% 0.52/0.98 inference('demod', [status(thm)], [zip_derived_cl41, zip_derived_cl45])).
% 0.52/0.98 thf(zip_derived_cl47, plain, (((vd1178) = (sk__3))),
% 0.52/0.98 inference('cnf', [status(esa)],
% 0.52/0.98 [and(neg(neg(conjunct2(conjunct2(conjunct2(plural(comma_conjunct2(268))))))), and(holds(conjunct1(conjunct2(conjunct2(plural(comma_conjunct2(268))))), 1194, 0), and(holds(conjunct1(conjunct2(plural(comma_conjunct2(268)))), 1193, 0), and(holds(conjunct1(plural(comma_conjunct2(268))), 1192, 0), and(qe(s3(plural(comma_conjunct2(268)))), and(qe(s2(plural(comma_conjunct2(268)))), and(qe(s1(plural(comma_conjunct2(268)))), and(pred(comma_conjunct1(268), 9), and(pred(comma_conjunct1(268), 8), and(pred(comma_conjunct1(268), 7), and(qe(s3(plural(268))), and(qe(s2(plural(268))), qe(s1(plural(268)))))))))))))))])).
% 0.52/0.98 thf(zip_derived_cl315, plain, (((sk__3) != (sk__4))),
% 0.52/0.98 inference('demod', [status(thm)], [zip_derived_cl311, zip_derived_cl47])).
% 0.52/0.98 thf(zip_derived_cl640, plain,
% 0.52/0.98 (![X0 : $i, X1 : $i]:
% 0.52/0.98 (((vf @ sk__1 @ sk__1) != (vd684))
% 0.52/0.98 | ((sk__4) != (X0))
% 0.52/0.98 | ~ (rpoint @ X0)
% 0.52/0.98 | ~ (rpoint @ X1)
% 0.52/0.98 | ((sk__3) != (X1)))),
% 0.52/0.98 inference('simplify_reflect-', [status(thm)],
% 0.52/0.98 [zip_derived_cl635, zip_derived_cl315])).
% 0.52/0.98 thf(zip_derived_cl696, plain,
% 0.52/0.98 (![X0 : $i, X1 : $i]:
% 0.52/0.98 (((vd684) != (vd684))
% 0.52/0.98 | ~ (rpoint @ sk__1)
% 0.52/0.98 | ((sk__3) != (X0))
% 0.52/0.98 | ~ (rpoint @ X0)
% 0.52/0.98 | ~ (rpoint @ X1)
% 0.52/0.98 | ((sk__4) != (X1)))),
% 0.52/0.98 inference('sup-', [status(thm)], [zip_derived_cl686, zip_derived_cl640])).
% 0.52/0.98 thf(zip_derived_cl25, plain, ( (rpoint @ sk__1)),
% 0.52/0.98 inference('cnf', [status(esa)], [qe(s2(plural(271)))])).
% 0.52/0.98 thf(zip_derived_cl702, plain,
% 0.52/0.98 (![X0 : $i, X1 : $i]:
% 0.52/0.98 (((vd684) != (vd684))
% 0.52/0.98 | ((sk__3) != (X0))
% 0.52/0.98 | ~ (rpoint @ X0)
% 0.52/0.98 | ~ (rpoint @ X1)
% 0.52/0.98 | ((sk__4) != (X1)))),
% 0.52/0.98 inference('demod', [status(thm)], [zip_derived_cl696, zip_derived_cl25])).
% 0.52/0.98 thf(zip_derived_cl703, plain,
% 0.52/0.98 (![X0 : $i, X1 : $i]:
% 0.52/0.98 (((sk__4) != (X1))
% 0.52/0.98 | ~ (rpoint @ X1)
% 0.52/0.98 | ~ (rpoint @ X0)
% 0.52/0.98 | ((sk__3) != (X0)))),
% 0.52/0.98 inference('simplify', [status(thm)], [zip_derived_cl702])).
% 0.52/0.98 thf(zip_derived_cl704, plain,
% 0.52/0.98 (![X0 : $i]: (((sk__3) != (X0)) | ~ (rpoint @ X0) | ~ (rpoint @ sk__4))),
% 0.52/0.98 inference('eq_res', [status(thm)], [zip_derived_cl703])).
% 0.52/0.98 thf(zip_derived_cl44, plain, ( (rpoint @ sk__4)),
% 0.52/0.98 inference('cnf', [status(esa)],
% 0.52/0.98 [and(neg(neg(conjunct2(conjunct2(conjunct2(plural(comma_conjunct2(268))))))), and(holds(conjunct1(conjunct2(conjunct2(plural(comma_conjunct2(268))))), 1194, 0), and(holds(conjunct1(conjunct2(plural(comma_conjunct2(268)))), 1193, 0), and(holds(conjunct1(plural(comma_conjunct2(268))), 1192, 0), and(qe(s3(plural(comma_conjunct2(268)))), and(qe(s2(plural(comma_conjunct2(268)))), and(qe(s1(plural(comma_conjunct2(268)))), and(pred(comma_conjunct1(268), 9), and(pred(comma_conjunct1(268), 8), and(pred(comma_conjunct1(268), 7), and(qe(s3(plural(268))), and(qe(s2(plural(268))), qe(s1(plural(268)))))))))))))))])).
% 0.52/0.98 thf(zip_derived_cl705, plain,
% 0.52/0.98 (![X0 : $i]: (((sk__3) != (X0)) | ~ (rpoint @ X0))),
% 0.52/0.98 inference('demod', [status(thm)], [zip_derived_cl704, zip_derived_cl44])).
% 0.52/0.98 thf(zip_derived_cl706, plain, (~ (rpoint @ sk__3)),
% 0.52/0.98 inference('eq_res', [status(thm)], [zip_derived_cl705])).
% 0.52/0.98 thf(zip_derived_cl46, plain, ( (rpoint @ sk__3)),
% 0.52/0.98 inference('cnf', [status(esa)],
% 0.52/0.98 [and(neg(neg(conjunct2(conjunct2(conjunct2(plural(comma_conjunct2(268))))))), and(holds(conjunct1(conjunct2(conjunct2(plural(comma_conjunct2(268))))), 1194, 0), and(holds(conjunct1(conjunct2(plural(comma_conjunct2(268)))), 1193, 0), and(holds(conjunct1(plural(comma_conjunct2(268))), 1192, 0), and(qe(s3(plural(comma_conjunct2(268)))), and(qe(s2(plural(comma_conjunct2(268)))), and(qe(s1(plural(comma_conjunct2(268)))), and(pred(comma_conjunct1(268), 9), and(pred(comma_conjunct1(268), 8), and(pred(comma_conjunct1(268), 7), and(qe(s3(plural(268))), and(qe(s2(plural(268))), qe(s1(plural(268)))))))))))))))])).
% 0.52/0.98 thf(zip_derived_cl707, plain, ($false),
% 0.52/0.98 inference('demod', [status(thm)], [zip_derived_cl706, zip_derived_cl46])).
% 0.52/0.98
% 0.52/0.98 % SZS output end Refutation
% 0.52/0.98
% 0.52/0.98
% 0.52/0.98 % Terminating...
% 0.53/1.04 % Runner terminated.
% 1.62/1.07 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------