%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : GEO111+1 : TPTP v9.0.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n022.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 Jul 24 01:38:09 PM UTC 2025
% Result : Theorem 208.68s 26.53s
% Output : CNFRefutation 208.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 11
% Syntax : Number of formulae : 94 ( 18 unt; 0 def)
% Number of atoms : 239 ( 49 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 248 ( 103 ~; 107 |; 23 &)
% ( 7 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-4 aty)
% Number of functors : 12 ( 12 usr; 4 con; 0-4 aty)
% Number of variables : 106 ( 3 sgn 37 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(theorem_3_8_1,plain,
! [C,P,Q,R] :
( between_c(C,P,Q,R)
=> ( incident_c(P,C)
& incident_c(Q,C)
& incident_c(R,C)
& P != Q
& Q != R
& P != R ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',theorem_3_8_1) ).
fof(theorem_3_8_1_negated,plain,
~ ! [C,P,Q,R] :
( between_c(C,P,Q,R)
=> ( incident_c(P,C)
& incident_c(Q,C)
& incident_c(R,C)
& P != Q
& Q != R
& P != R ) ),
inference(negate_conjecture,[status(cth)],[theorem_3_8_1]) ).
cnf(52,plain,
( ~ incident_c(sK18,sK17)
| ~ incident_c(sK19,sK17)
| ~ incident_c(sK20,sK17)
| sK18 = sK19
| sK18 = sK20
| sK19 = sK20 ),
inference(cnf,[status(esa)],[theorem_3_8_1_negated]) ).
cnf(l0,plain,
( ~ incident_c(sK18,sK17)
| ~ incident_c(sK19,sK17)
| ~ incident_c(sK20,sK17)
| sK18 = sK19
| sK18 = sK20
| sK19 = sK20 ),
inference(instantiation,[status(thm)],[52]) ).
fof(part_of_defn,plain,
! [C,C1] :
( part_of(C1,C)
<=> ! [P] :
( incident_c(P,C1)
=> incident_c(P,C) ) ),
file('Axioms/GEO004+0.ax',part_of_defn) ).
cnf(0,plain,
( ~ part_of(X0,X1)
| ~ incident_c(X2,X0)
| incident_c(X2,X1) ),
inference(cnf,[status(esa)],[part_of_defn]) ).
cnf(l749,plain,
( ~ part_of(sK15(sK17,sK18,sK19,sK20),sK17)
| ~ incident_c(sK19,sK15(sK17,sK18,sK19,sK20))
| incident_c(sK19,sK17) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l1,plain,
( ~ part_of(sK15(sK17,sK18,sK19,sK20),sK17)
| ~ incident_c(sK18,sK15(sK17,sK18,sK19,sK20))
| incident_c(sK18,sK17) ),
inference(instantiation,[status(thm)],[0]) ).
fof(between_c_defn,plain,
! [C,P,Q,R] :
( between_c(C,P,Q,R)
<=> ( P != R
& ? [Cpp] :
( part_of(Cpp,C)
& end_point(P,Cpp)
& end_point(R,Cpp)
& inner_point(Q,Cpp) ) ) ),
file('Axioms/GEO004+1.ax',between_c_defn) ).
cnf(46,plain,
( ~ between_c(X0,X1,X2,X3)
| part_of(sK15(X0,X1,X2,X3),X0) ),
inference(cnf,[status(esa)],[between_c_defn]) ).
cnf(l2,plain,
( ~ between_c(sK17,sK18,sK19,sK20)
| part_of(sK15(sK17,sK18,sK19,sK20),sK17) ),
inference(instantiation,[status(thm)],[46]) ).
fof(end_point_defn,plain,
! [P,C] :
( end_point(P,C)
<=> ( incident_c(P,C)
& ! [C1,C2] :
( ( part_of(C1,C)
& part_of(C2,C)
& incident_c(P,C1)
& incident_c(P,C2) )
=> ( part_of(C1,C2)
| part_of(C2,C1) ) ) ) ),
file('Axioms/GEO004+0.ax',end_point_defn) ).
cnf(11,plain,
( ~ end_point(X0,X1)
| incident_c(X0,X1) ),
inference(cnf,[status(esa)],[end_point_defn]) ).
cnf(l44,plain,
( ~ end_point(sK18,sK15(sK17,sK18,sK19,sK20))
| incident_c(sK18,sK15(sK17,sK18,sK19,sK20)) ),
inference(instantiation,[status(thm)],[11]) ).
fof(inner_point_defn,plain,
! [P,C] :
( inner_point(P,C)
<=> ( incident_c(P,C)
& ~ end_point(P,C) ) ),
file('Axioms/GEO004+0.ax',inner_point_defn) ).
cnf(20,plain,
( ~ end_point(X0,X1)
| ~ inner_point(X0,X1) ),
inference(cnf,[status(esa)],[inner_point_defn]) ).
cnf(l801,plain,
( ~ end_point(sK20,sK15(sK17,sK18,sK19,sK20))
| ~ inner_point(sK20,sK15(sK17,sK18,sK19,sK20)) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(49,plain,
( ~ between_c(X0,X1,X2,X3)
| inner_point(X2,sK15(X0,X1,X2,X3)) ),
inference(cnf,[status(esa)],[between_c_defn]) ).
cnf(l837,plain,
( ~ between_c(sK17,sK18,sK19,sK20)
| inner_point(sK19,sK15(sK17,sK18,sK19,sK20)) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(47,plain,
( ~ between_c(X0,X1,X2,X3)
| end_point(X1,sK15(X0,X1,X2,X3)) ),
inference(cnf,[status(esa)],[between_c_defn]) ).
cnf(l48,plain,
( ~ between_c(sK17,sK18,sK19,sK20)
| end_point(sK18,sK15(sK17,sK18,sK19,sK20)) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l793,plain,
( ~ between_c(sK17,sK18,sK19,sK20)
| part_of(sK15(sK17,sK18,sK19,sK20),sK17) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(51,plain,
between_c(sK17,sK18,sK19,sK20),
inference(cnf,[status(esa)],[theorem_3_8_1_negated]) ).
cnf(l833,plain,
between_c(sK17,sK18,sK19,sK20),
inference(instantiation,[status(thm)],[51]) ).
cnf(l56,plain,
between_c(sK17,sK18,sK19,sK20),
inference(instantiation,[status(thm)],[51]) ).
cnf(48,plain,
( ~ between_c(X0,X1,X2,X3)
| end_point(X3,sK15(X0,X1,X2,X3)) ),
inference(cnf,[status(esa)],[between_c_defn]) ).
cnf(l941,plain,
( ~ between_c(sK17,sK18,sK19,sK20)
| end_point(sK20,sK15(sK17,sK18,sK19,sK20)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l752,plain,
( ~ part_of(sK15(sK17,sK18,sK19,sK20),sK17)
| ~ incident_c(sK20,sK15(sK17,sK18,sK19,sK20))
| incident_c(sK20,sK17) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l759,plain,
( ~ between_c(sK17,sK18,sK19,sK20)
| part_of(sK15(sK17,sK18,sK19,sK20),sK17) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(19,plain,
( ~ inner_point(X0,X1)
| incident_c(X0,X1) ),
inference(cnf,[status(esa)],[inner_point_defn]) ).
cnf(l771,plain,
( ~ inner_point(sK19,sK15(sK17,sK18,sK19,sK20))
| incident_c(sK19,sK15(sK17,sK18,sK19,sK20)) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l10,plain,
between_c(sK17,sK18,sK19,sK20),
inference(instantiation,[status(thm)],[51]) ).
cnf(l1209,plain,
between_c(sK17,sK18,sK19,sK20),
inference(instantiation,[status(thm)],[51]) ).
fof(c4,plain,
! [C,P] :
( inner_point(P,C)
=> ? [C1,C2] :
( meet(P,C1,C2)
& C = sum(C1,C2) ) ),
file('Axioms/GEO004+0.ax',c4) ).
cnf(37,plain,
( ~ inner_point(X0,X1)
| X1 = sum(sK10(X1,X0),sK11(X1,X0)) ),
inference(cnf,[status(esa)],[c4]) ).
cnf(l991,plain,
( ~ inner_point(sK9(sK15(sK17,sK18,sK19,sK20)),sK15(sK17,sK18,sK19,sK20))
| sK15(sK17,sK18,sK19,sK20) = sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l764,plain,
between_c(sK17,sK18,sK19,sK20),
inference(instantiation,[status(thm)],[51]) ).
cnf(l916,plain,
between_c(sK17,sK18,sK19,sK20),
inference(instantiation,[status(thm)],[51]) ).
cnf(l1034,plain,
( ~ between_c(sK17,sK18,sK19,sK20)
| end_point(sK18,sK15(sK17,sK18,sK19,sK20)) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l1149,plain,
between_c(sK17,sK18,sK19,sK20),
inference(instantiation,[status(thm)],[51]) ).
fof(c9,plain,
! [C,C1] :
( ! [P] :
( incident_c(P,C)
<=> incident_c(P,C1) )
=> C = C1 ),
file('Axioms/GEO004+0.ax',c9) ).
cnf(43,plain,
( incident_c(sK14(X0,X1),X0)
| incident_c(sK14(X0,X1),X1)
| X0 = X1 ),
inference(cnf,[status(esa)],[c9]) ).
cnf(l802,plain,
( incident_c(sK14(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))))
| incident_c(sK14(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))))),sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))))
| sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))) = sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))) ),
inference(instantiation,[status(thm)],[43]) ).
fof(sum_defn,plain,
! [C,C1,C2] :
( C = sum(C1,C2)
<=> ! [Q] :
( incident_c(Q,C)
<=> ( incident_c(Q,C1)
| incident_c(Q,C2) ) ) ),
file('Axioms/GEO004+0.ax',sum_defn) ).
cnf(5,plain,
( ~ incident_c(X0,X1)
| X2 != sum(X3,X1)
| incident_c(X0,X2) ),
inference(cnf,[status(esa)],[sum_defn]) ).
cnf(l1031,plain,
( ~ incident_c(sK14(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))))
| sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))) != sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))))
| incident_c(sK14(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))))),sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l777,plain,
( ~ between_c(sK17,sK18,sK19,sK20)
| inner_point(sK19,sK15(sK17,sK18,sK19,sK20)) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l775,plain,
( ~ end_point(sK20,sK15(sK17,sK18,sK19,sK20))
| incident_c(sK20,sK15(sK17,sK18,sK19,sK20)) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l786,plain,
between_c(sK17,sK18,sK19,sK20),
inference(instantiation,[status(thm)],[51]) ).
fof(c3,plain,
! [C] :
? [P] : inner_point(P,C),
file('Axioms/GEO004+0.ax',c3) ).
cnf(35,plain,
inner_point(sK9(X0),X0),
inference(cnf,[status(esa)],[c3]) ).
cnf(l1105,plain,
inner_point(sK9(sK15(sK17,sK18,sK19,sK20)),sK15(sK17,sK18,sK19,sK20)),
inference(instantiation,[status(thm)],[35]) ).
cnf(l788,plain,
( ~ between_c(sK17,sK18,sK19,sK20)
| end_point(sK20,sK15(sK17,sK18,sK19,sK20)) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l1191,plain,
( ~ inner_point(sK9(sK20),sK20)
| sK20 = sum(sK10(sK20,sK9(sK20)),sK11(sK20,sK9(sK20))) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l1355,plain,
between_c(sK17,sK18,sK19,sK20),
inference(instantiation,[status(thm)],[51]) ).
cnf(44,plain,
( ~ incident_c(sK14(X0,X1),X0)
| ~ incident_c(sK14(X0,X1),X1)
| X0 = X1 ),
inference(cnf,[status(esa)],[c9]) ).
cnf(l1038,plain,
( ~ incident_c(sK14(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))))
| ~ incident_c(sK14(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))))),sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))))
| sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))) = sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(l1195,plain,
inner_point(sK9(sK20),sK20),
inference(instantiation,[status(thm)],[35]) ).
cnf(l1205,plain,
( ~ inner_point(sK9(sK20),sK20)
| sK20 = sum(sK10(sK20,sK9(sK20)),sK11(sK20,sK9(sK20))) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(6,plain,
( incident_c(sK2(X0,X1,X2),X0)
| X0 = sum(X1,X2)
| sP0(X1,X0,X2) ),
inference(cnf,[status(esa)],[sum_defn]) ).
cnf(l1294,plain,
( incident_c(sK2(sK17,sK17,sK17),sK17)
| sK17 = sum(sK17,sK17)
| sP0(sK17,sK17,sK17) ),
inference(instantiation,[status(thm)],[6]) ).
fof(c5,plain,
! [C,P,Q,R] :
( ( end_point(P,C)
& end_point(Q,C)
& end_point(R,C) )
=> ( P = Q
| P = R
| Q = R ) ),
file('Axioms/GEO004+0.ax',c5) ).
cnf(38,plain,
( ~ end_point(X0,X1)
| ~ end_point(X2,X1)
| ~ end_point(X3,X1)
| X0 = X2
| X0 = X3
| X2 = X3 ),
inference(cnf,[status(esa)],[c5]) ).
cnf(l760,plain,
( ~ end_point(sK12(sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))),sK20),sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))))
| ~ end_point(sK20,sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))))
| ~ end_point(sK12(sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))),sK12(sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))),sK20)),sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))))
| sK12(sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))),sK20) = sK20
| sK12(sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))),sK20) = sK12(sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))),sK12(sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))),sK20))
| sK20 = sK12(sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))),sK12(sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))),sK20)) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l794,plain,
between_c(sK17,sK18,sK19,sK20),
inference(instantiation,[status(thm)],[51]) ).
cnf(10,plain,
( incident_c(sK2(X0,X1,X2),X1)
| incident_c(sK2(X0,X1,X2),X2)
| ~ sP0(X1,X0,X2) ),
inference(cnf,[status(esa)],[sum_defn]) ).
cnf(l1491,plain,
( incident_c(sK2(sK17,sK17,sK17),sK17)
| incident_c(sK2(sK17,sK17,sK17),sK17)
| ~ sP0(sK17,sK17,sK17) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(9,plain,
( ~ incident_c(sK2(X0,X1,X2),X0)
| ~ sP0(X1,X0,X2) ),
inference(cnf,[status(esa)],[sum_defn]) ).
cnf(l1662,plain,
( ~ incident_c(sK2(sK17,sK17,sK17),sK17)
| ~ sP0(sK17,sK17,sK17) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1665,plain,
( ~ incident_c(sK2(sK17,sK17,sK17),sK17)
| ~ sP0(sK17,sK17,sK17) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(3,plain,
( ~ incident_c(X0,X1)
| X1 != sum(X2,X3)
| incident_c(X0,X2)
| incident_c(X0,X3) ),
inference(cnf,[status(esa)],[sum_defn]) ).
cnf(l1007,plain,
( ~ incident_c(sK14(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))))),sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))))
| sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))) != sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))))
| incident_c(sK14(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))))
| incident_c(sK14(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l1166,plain,
( ~ between_c(sum(sK17,sK17),sK19,sK19,sK20)
| end_point(sK19,sK15(sum(sK17,sK17),sK19,sK19,sK20)) ),
inference(instantiation,[status(thm)],[47]) ).
fof(c6,plain,
! [C,P] :
( end_point(P,C)
=> ? [Q] :
( end_point(Q,C)
& P != Q ) ),
file('Axioms/GEO004+0.ax',c6) ).
cnf(40,plain,
( X0 != sK12(X1,X0)
| ~ end_point(X0,X1) ),
inference(cnf,[status(esa)],[c6]) ).
cnf(l1442,plain,
( sK20 != sK12(sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))),sK20)
| ~ end_point(sK20,sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))))) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(l910,plain,
( sK12(sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))),sK20) != sK12(sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))),sK12(sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))),sK20))
| ~ end_point(sK12(sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))),sK20),sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))))) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(45,plain,
( X0 != X1
| ~ between_c(X2,X0,X3,X1) ),
inference(cnf,[status(esa)],[between_c_defn]) ).
cnf(l2085,plain,
( sK20 != sK12(sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))),sK12(sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))),sK20))
| ~ between_c(sK17,sK20,sK19,sK12(sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))),sK12(sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))),sK20))) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(39,plain,
( ~ end_point(X0,X1)
| end_point(sK12(X1,X0),X1) ),
inference(cnf,[status(esa)],[c6]) ).
cnf(l872,plain,
( ~ end_point(sK12(sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))),sK20),sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))))
| end_point(sK12(sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))),sK12(sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))),sK20)),sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))))) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l2012,plain,
( ~ incident_c(sK14(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))))
| ~ incident_c(sK14(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))))),sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))))
| sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))) = sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(l870,plain,
( ~ end_point(sK20,sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))))
| end_point(sK12(sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))),sK20),sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))))) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l1426,plain,
( ~ end_point(sK20,sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))))
| end_point(sK12(sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))),sK20),sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))))) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l1180,plain,
( ~ end_point(sK19,sK15(sum(sK17,sK17),sK19,sK19,sK20))
| ~ inner_point(sK19,sK15(sum(sK17,sK17),sK19,sK19,sK20)) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1295,plain,
( ~ incident_c(sK2(sK17,sK17,sK17),sK17)
| ~ sP0(sK17,sK17,sK17) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1182,plain,
( ~ between_c(sum(sK17,sK17),sK19,sK19,sK20)
| inner_point(sK19,sK15(sum(sK17,sK17),sK19,sK19,sK20)) ),
inference(instantiation,[status(thm)],[49]) ).
cnf(l1987,plain,
( ~ end_point(sK20,sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))))
| end_point(sK12(sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))),sK20),sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))))) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(8,plain,
( ~ incident_c(sK2(X0,X1,X2),X2)
| X0 = sum(X1,X2)
| sP0(X1,X0,X2) ),
inference(cnf,[status(esa)],[sum_defn]) ).
cnf(l1507,plain,
( ~ incident_c(sK2(sK17,sK17,sK17),sK17)
| sK17 = sum(sK17,sK17)
| sP0(sK17,sK17,sK17) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1462,plain,
between_c(sK17,sK18,sK19,sK20),
inference(instantiation,[status(thm)],[51]) ).
cnf(l2250,plain,
( ~ incident_c(sK14(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))))
| ~ incident_c(sK14(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))))),sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))))
| sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))) = sum(sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20)))),sum(sK10(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))),sK11(sK15(sK17,sK18,sK19,sK20),sK9(sK15(sK17,sK18,sK19,sK20))))) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(l1223,plain,
inner_point(sK9(sK20),sK20),
inference(instantiation,[status(thm)],[35]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l749,l1,l2,l44,l801,l837,l48,l793,l833,l56,l941,l752,l759,l771,l10,l1209,l991,l764,l916,l1034,l1149,l802,l1031,l777,l775,l786,l1105,l788,l1191,l1355,l1038,l1195,l1205,l1294,l760,l794,l1491,l1662,l1665,l1007,l1166,l1442,l910,l2085,l872,l2012,l870,l1426,l1180,l1295,l1182,l1987,l1507,l1462,l2250,l1223]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : GEO111+1 : TPTP v9.0.0. Released v2.4.0.
% 0.11/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.33 % Computer : n022.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Sun Jul 20 11:10:19 EDT 2025
% 0.11/0.33 % CPUTime :
% 0.11/0.34 % launching worker at depth: 1
% 0.11/0.34 % launching worker at depth: 8
% 0.11/0.34 % launching worker at depth: 3
% 0.11/0.34 % launching worker at depth: 2
% 0.11/0.34 % launching worker at depth: 4
% 0.11/0.34 % launching worker at depth: 6
% 0.11/0.34 % launching worker at depth: 7
% 0.11/0.34 % launching worker at depth: 5
% 0.11/0.34 % launching worker at depth: 9
% 0.11/0.37 % launching worker at depth: 10
% 0.18/0.56 % launching worker at depth: 11
% 208.68/26.53 % SZS status Theorem for theBenchmark
% 208.68/26.53 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------