%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GEO126+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:17:08 AM UTC 2026
% Result : Theorem 10.50s 1.73s
% Output : CNFRefutation 10.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 11
% Syntax : Number of formulae : 88 ( 26 unt; 0 def)
% Number of atoms : 221 ( 59 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 203 ( 70 ~; 89 |; 33 &)
% ( 8 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 1 con; 0-2 aty)
% Number of variables : 157 ( 3 sgn 72 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(end_point_defn,axiom,
! [P,C] :
( end_point(P,C)
<=> ( ! [C1,C2] :
( ( incident_c(P,C2)
& incident_c(P,C1)
& part_of(C2,C)
& part_of(C1,C) )
=> ( part_of(C2,C1)
| part_of(C1,C2) ) )
& incident_c(P,C) ) ),
file('theBenchmark.p',end_point_defn) ).
fof(inner_point_defn,axiom,
! [P,C] :
( inner_point(P,C)
<=> ( ~ end_point(P,C)
& incident_c(P,C) ) ),
file('theBenchmark.p',inner_point_defn) ).
fof(closed_defn,axiom,
! [C] :
( closed(C)
<=> ~ ? [P] : end_point(P,C) ),
file('theBenchmark.p',closed_defn) ).
fof(open_defn,axiom,
! [C] :
( open(C)
<=> ? [P] : end_point(P,C) ),
file('theBenchmark.p',open_defn) ).
fof(c3,axiom,
! [C] :
? [P] : inner_point(P,C),
file('theBenchmark.p',c3) ).
fof(c4,axiom,
! [C,P] :
( inner_point(P,C)
=> ? [C1,C2] :
( C = sum(C1,C2)
& meet(P,C1,C2) ) ),
file('theBenchmark.p',c4) ).
fof(start_point_defn,axiom,
! [P,O] :
( start_point(P,O)
<=> ( ! [Q] :
( ( incident_o(Q,O)
& P != Q )
=> ordered_by(O,P,Q) )
& incident_o(P,O) ) ),
file('theBenchmark.p',start_point_defn) ).
fof(o2,axiom,
! [O] :
? [C] :
( ! [P] :
( incident_o(P,O)
<=> incident_c(P,C) )
& open(C) ),
file('theBenchmark.p',o2) ).
fof(o4,axiom,
! [O] :
? [P] : start_point(P,O),
file('theBenchmark.p',o4) ).
fof(underlying_curve_defn,axiom,
! [C,O] :
( C = underlying_curve(O)
<=> ! [P] :
( incident_o(P,O)
<=> incident_c(P,C) ) ),
file('theBenchmark.p',underlying_curve_defn) ).
fof(theorem_4_11,conjecture,
! [O] :
? [P,Q] :
( P != Q
& ordered_by(O,P,Q) ),
file('theBenchmark.p',theorem_4_11) ).
fof(theorem_4_11_neg,negated_conjecture,
~ ! [O] :
? [P,Q] :
( P != Q
& ordered_by(O,P,Q) ),
inference(assume_negation,[status(cth)],[theorem_4_11]) ).
cnf(c_30,plain,
( ~ end_point(A,B)
| ~ inner_point(A,B) ),
inference(clausify,[status(thm)],[inner_point_defn]) ).
cnf(c_31,plain,
( incident_c(A,B)
| ~ inner_point(A,B) ),
inference(clausify,[status(thm)],[inner_point_defn]) ).
fof(nnf_10,plain,
! [C] :
? [P] : inner_point(P,C),
inference(fof_nnf,[status(thm)],[c3]) ).
fof(sk_c3,plain,
! [C] : inner_point(sK0(C),C),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(P,sK0(C))],[nnf_10]) ).
cnf(c_32,plain,
inner_point(sK0(A),A),
inference(split_conjunct,[status(thm)],[sk_c3]) ).
fof(nnf_11,plain,
! [C,P] :
( ? [C1,C2] :
( sum(C1,C2) = C
& meet(P,C1,C2) )
| ~ inner_point(P,C) ),
inference(fof_nnf,[status(thm)],[c4]) ).
fof(sk_c4_sk,plain,
! [C,P] :
( ( sum(sK1(C,P),sK2(C,P)) = C
& meet(P,sK1(C,P),sK2(C,P)) )
| ~ inner_point(P,C) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2]),skolemize(C1,sK1(C,P)),skolemize(C2,sK2(C,P))],[nnf_11]) ).
fof(sk_c4,plain,
( ! [VAR_0,VAR_1] :
( sum(sK1(VAR_1,VAR_0),sK2(VAR_1,VAR_0)) = VAR_1
| ~ inner_point(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( meet(VAR_0,sK1(VAR_1,VAR_0),sK2(VAR_1,VAR_0))
| ~ inner_point(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_c4_sk]) ).
cnf(c_34,plain,
( sum(sK1(B,A),sK2(B,A)) = B
| ~ inner_point(A,B) ),
inference(split_conjunct,[status(thm)],[sk_c4]) ).
fof(nnf_6,plain,
! [C] :
( ( ? [P] : end_point(P,C)
| closed(C) )
& ( ! [X0] : ~ end_point(X0,C)
| ~ closed(C) ) ),
inference(fof_nnf,[status(thm)],[closed_defn]) ).
fof(sk_closed_defn_sk,plain,
! [C] :
( ( end_point(sK3(C),C)
| closed(C) )
& ( ! [X0] : ~ end_point(X0,C)
| ~ closed(C) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(P,sK3(C))],[nnf_6]) ).
fof(sk_closed_defn,plain,
( ! [VAR_0] :
( end_point(sK3(VAR_0),VAR_0)
| closed(VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ end_point(VAR_1,VAR_0)
| ~ closed(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_closed_defn_sk]) ).
cnf(c_37,plain,
( end_point(sK3(A),A)
| closed(A) ),
inference(split_conjunct,[status(thm)],[sk_closed_defn]) ).
cnf(c_39,plain,
( ~ end_point(B,A)
| ~ closed(A) ),
inference(split_conjunct,[status(thm)],[sk_closed_defn]) ).
fof(nnf_7,plain,
! [C] :
( ( ! [P] : ~ end_point(P,C)
| open(C) )
& ( ? [X0] : end_point(X0,C)
| ~ open(C) ) ),
inference(fof_nnf,[status(thm)],[open_defn]) ).
fof(sk_open_defn_sk,plain,
! [C] :
( ( ! [P] : ~ end_point(P,C)
| open(C) )
& ( end_point(sK4(C),C)
| ~ open(C) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X0,sK4(C))],[nnf_7]) ).
fof(sk_open_defn,plain,
( ! [VAR_0,VAR_1] :
( ~ end_point(VAR_1,VAR_0)
| open(VAR_0) )
& ! [VAR_0] :
( end_point(sK4(VAR_0),VAR_0)
| ~ open(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_open_defn_sk]) ).
cnf(c_41,plain,
( end_point(sK4(A),A)
| ~ open(A) ),
inference(split_conjunct,[status(thm)],[sk_open_defn]) ).
fof(nnf_22,plain,
! [O] :
? [C] :
( ! [P] :
( ( ~ incident_c(P,C)
| incident_o(P,O) )
& ( incident_c(P,C)
| ~ incident_o(P,O) ) )
& open(C) ),
inference(fof_nnf,[status(thm)],[o2]) ).
fof(sk_o2,plain,
! [O] :
( ! [P] :
( ( ~ incident_c(P,sK5(O))
| incident_o(P,O) )
& ( incident_c(P,sK5(O))
| ~ incident_o(P,O) ) )
& open(sK5(O)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(C,sK5(O))],[nnf_22]) ).
cnf(c_43,plain,
open(sK5(A)),
inference(split_conjunct,[status(thm)],[sk_o2]) ).
cnf(c_59,plain,
( ordered_by(B,A,C)
| ~ incident_o(C,B)
| C = A
| ~ start_point(A,B) ),
inference(clausify,[status(thm)],[start_point_defn]) ).
fof(nnf_24,plain,
! [O] :
? [P] : start_point(P,O),
inference(fof_nnf,[status(thm)],[o4]) ).
fof(sk_o4,plain,
! [O] : start_point(sK6(O),O),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(P,sK6(O))],[nnf_24]) ).
cnf(c_63,plain,
start_point(sK6(A),A),
inference(split_conjunct,[status(thm)],[sk_o4]) ).
cnf(c_92,plain,
( end_point(sK3(B),B)
| ~ end_point(A,B) ),
inference(resolve,[status(thm)],[c_39,c_37]) ).
cnf(c_103,plain,
( incident_c(A,B)
| ~ end_point(A,B) ),
inference(clausify,[status(thm)],[end_point_defn]) ).
cnf(c_132,plain,
( incident_c(A,sK5(B))
| ~ incident_o(A,B) ),
inference(split_conjunct,[status(thm)],[sk_o2]) ).
cnf(c_133,plain,
( ~ incident_c(A,sK5(B))
| incident_o(A,B) ),
inference(split_conjunct,[status(thm)],[sk_o2]) ).
fof(nnf_27,plain,
! [C,O] :
( ( ? [P] :
( ( ~ incident_c(P,C)
| ~ incident_o(P,O) )
& ( incident_c(P,C)
| incident_o(P,O) ) )
| underlying_curve(O) = C )
& ( ! [X0] :
( ( ~ incident_c(X0,C)
| incident_o(X0,O) )
& ( incident_c(X0,C)
| ~ incident_o(X0,O) ) )
| underlying_curve(O) != C ) ),
inference(fof_nnf,[status(thm)],[underlying_curve_defn]) ).
fof(sk_underlying_curve_defn_sk,plain,
! [C,O] :
( ( ( ( ~ incident_c(sK7(C,O),C)
| ~ incident_o(sK7(C,O),O) )
& ( incident_c(sK7(C,O),C)
| incident_o(sK7(C,O),O) ) )
| underlying_curve(O) = C )
& ( ! [X0] :
( ( ~ incident_c(X0,C)
| incident_o(X0,O) )
& ( incident_c(X0,C)
| ~ incident_o(X0,O) ) )
| underlying_curve(O) != C ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(P,sK7(C,O))],[nnf_27]) ).
fof(sk_underlying_curve_defn,plain,
( ! [VAR_0,VAR_1] :
( ~ incident_c(sK7(VAR_1,VAR_0),VAR_1)
| ~ incident_o(sK7(VAR_1,VAR_0),VAR_0)
| underlying_curve(VAR_0) = VAR_1 )
& ! [VAR_0,VAR_1] :
( incident_c(sK7(VAR_1,VAR_0),VAR_1)
| incident_o(sK7(VAR_1,VAR_0),VAR_0)
| underlying_curve(VAR_0) = VAR_1 )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ incident_c(VAR_2,VAR_1)
| incident_o(VAR_2,VAR_0)
| underlying_curve(VAR_0) != VAR_1 )
& ! [VAR_0,VAR_1,VAR_2] :
( incident_c(VAR_2,VAR_1)
| ~ incident_o(VAR_2,VAR_0)
| underlying_curve(VAR_0) != VAR_1 ) ),
inference(cnf_transformation,[status(thm)],[sk_underlying_curve_defn_sk]) ).
cnf(c_137,plain,
( ~ incident_c(C,B)
| incident_o(C,A)
| underlying_curve(A) != B ),
inference(split_conjunct,[status(thm)],[sk_underlying_curve_defn]) ).
cnf(c_138,plain,
( incident_c(sK7(B,A),B)
| incident_o(sK7(B,A),A)
| underlying_curve(A) = B ),
inference(split_conjunct,[status(thm)],[sk_underlying_curve_defn]) ).
cnf(c_139,plain,
( ~ incident_c(sK7(B,A),B)
| ~ incident_o(sK7(B,A),A)
| underlying_curve(A) = B ),
inference(split_conjunct,[status(thm)],[sk_underlying_curve_defn]) ).
fof(nnf_28,plain,
? [O] :
! [P,Q] :
( Q = P
| ~ ordered_by(O,P,Q) ),
inference(fof_nnf,[status(thm)],[theorem_4_11_neg]) ).
fof(sk_theorem_4_11_neg,plain,
! [P,Q] :
( Q = P
| ~ ordered_by(sK8,P,Q) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(O,sK8)],[nnf_28]) ).
cnf(c_140,negated_conjecture,
( B = A
| ~ ordered_by(sK8,A,B) ),
inference(split_conjunct,[status(thm)],[sk_theorem_4_11_neg]) ).
cnf(c_141,plain,
~ end_point(sK0(A),A),
inference(resolve,[status(thm)],[c_32,c_30]) ).
cnf(c_142,plain,
incident_c(sK0(A),A),
inference(resolve,[status(thm)],[c_32,c_31]) ).
cnf(c_145,plain,
sum(sK1(A,sK0(A)),sK2(A,sK0(A))) = A,
inference(resolve,[status(thm)],[c_34,c_32]) ).
cnf(c_156,plain,
end_point(sK4(sK5(A)),sK5(A)),
inference(resolve,[status(thm)],[c_43,c_41]) ).
cnf(c_169,plain,
( ordered_by(B,sK6(B),A)
| ~ incident_o(A,B)
| A = sK6(B) ),
inference(resolve,[status(thm)],[c_63,c_59]) ).
cnf(c_170,plain,
( ordered_by(A,sK6(A),B)
| ~ incident_o(B,A)
| sK6(A) = B ),
inference(copy,[status(thm)],[c_169]) ).
cnf(c_414,plain,
( incident_c(sK7(B,A),sK5(A))
| incident_c(sK7(B,A),B)
| underlying_curve(A) = B ),
inference(resolve,[status(thm)],[c_138,c_132]) ).
cnf(c_7667,plain,
( incident_c(sK7(sK5(A),A),sK5(A))
| underlying_curve(A) = sK5(A) ),
inference(factor,[status(thm)],[c_414]) ).
cnf(c_419,plain,
( incident_c(sK7(sK5(A),A),sK5(A))
| sK5(A) = underlying_curve(A) ),
inference(copy,[status(thm)],[c_7667]) ).
cnf(c_422,plain,
( incident_o(sK0(B),A)
| underlying_curve(A) != B ),
inference(resolve,[status(thm)],[c_142,c_137]) ).
cnf(c_465,plain,
end_point(sK3(sK5(A)),sK5(A)),
inference(resolve,[status(thm)],[c_156,c_92]) ).
cnf(c_839,plain,
incident_c(sK3(sK5(A)),sK5(A)),
inference(resolve,[status(thm)],[c_465,c_103]) ).
cnf(c_853,plain,
incident_o(sK3(sK5(A)),A),
inference(resolve,[status(thm)],[c_839,c_133]) ).
cnf(c_876,plain,
( ordered_by(A,sK6(A),sK3(sK5(A)))
| sK6(A) = sK3(sK5(A)) ),
inference(resolve,[status(thm)],[c_853,c_170]) ).
cnf(c_7668,plain,
A = sum(sK1(A,sK0(A)),sK2(A,sK0(A))),
inference(copy,[status(thm)],[c_145]) ).
cnf(c_7669,plain,
incident_o(sK0(sum(sK1(underlying_curve(A),sK0(underlying_curve(A))),sK2(underlying_curve(A),sK0(underlying_curve(A))))),A),
inference(resolve,[status(thm)],[c_422,c_7668]) ).
cnf(c_988,plain,
incident_o(sK0(underlying_curve(A)),A),
inference(paramod,[status(thm)],[c_145,c_7669]) ).
cnf(c_989,plain,
( ordered_by(A,sK6(A),sK0(underlying_curve(A)))
| sK6(A) = sK0(underlying_curve(A)) ),
inference(resolve,[status(thm)],[c_988,c_170]) ).
cnf(c_2613,plain,
( incident_o(sK7(sK5(A),A),A)
| sK5(A) = underlying_curve(A) ),
inference(resolve,[status(thm)],[c_419,c_133]) ).
cnf(c_7670,plain,
( ~ incident_c(sK7(sK5(A),A),sK5(A))
| underlying_curve(A) = sK5(A)
| sK5(A) = underlying_curve(A) ),
inference(resolve,[status(thm)],[c_2613,c_139]) ).
cnf(c_7671,plain,
( ~ incident_c(sK7(sK5(A),A),sK5(A))
| sK5(A) = underlying_curve(A)
| sK5(A) = underlying_curve(A) ),
inference(copy,[status(thm)],[c_7670]) ).
cnf(c_2632,plain,
( ~ incident_c(sK7(sK5(A),A),sK5(A))
| sK5(A) = underlying_curve(A) ),
inference(copy,[status(thm)],[c_7671]) ).
cnf(c_7672,plain,
( sK5(A) = underlying_curve(A)
| sK5(A) = underlying_curve(A) ),
inference(resolve,[status(thm)],[c_2632,c_419]) ).
cnf(c_4522,plain,
sK5(A) = underlying_curve(A),
inference(copy,[status(thm)],[c_7672]) ).
cnf(c_7673,plain,
( ordered_by(A,sK6(A),sK3(sK5(A)))
| sK6(A) = sK3(underlying_curve(A)) ),
inference(paramod,[status(thm)],[c_4522,c_876]) ).
cnf(c_5211,plain,
( ordered_by(A,sK6(A),sK3(underlying_curve(A)))
| sK6(A) = sK3(underlying_curve(A)) ),
inference(paramod,[status(thm)],[c_4522,c_7673]) ).
cnf(c_7674,plain,
end_point(sK3(underlying_curve(A)),sK5(A)),
inference(paramod,[status(thm)],[c_4522,c_465]) ).
cnf(c_5310,plain,
end_point(sK3(underlying_curve(A)),underlying_curve(A)),
inference(paramod,[status(thm)],[c_4522,c_7674]) ).
cnf(c_7675,negated_conjecture,
( sK0(underlying_curve(sK8)) = sK6(sK8)
| sK6(sK8) = sK0(underlying_curve(sK8)) ),
inference(resolve,[status(thm)],[c_989,c_140]) ).
cnf(c_7676,negated_conjecture,
( sK6(sK8) = sK0(underlying_curve(sK8))
| sK6(sK8) = sK0(underlying_curve(sK8)) ),
inference(copy,[status(thm)],[c_7675]) ).
cnf(c_6293,negated_conjecture,
sK6(sK8) = sK0(underlying_curve(sK8)),
inference(copy,[status(thm)],[c_7676]) ).
cnf(c_7677,negated_conjecture,
( sK3(underlying_curve(sK8)) = sK6(sK8)
| sK6(sK8) = sK3(underlying_curve(sK8)) ),
inference(resolve,[status(thm)],[c_5211,c_140]) ).
cnf(c_7678,negated_conjecture,
( sK3(underlying_curve(sK8)) = sK6(sK8)
| sK0(underlying_curve(sK8)) = sK3(underlying_curve(sK8)) ),
inference(paramod,[status(thm)],[c_6293,c_7677]) ).
cnf(c_7679,negated_conjecture,
( sK3(underlying_curve(sK8)) = sK0(underlying_curve(sK8))
| sK0(underlying_curve(sK8)) = sK3(underlying_curve(sK8)) ),
inference(paramod,[status(thm)],[c_6293,c_7678]) ).
cnf(c_7680,negated_conjecture,
( sK0(underlying_curve(sK8)) = sK3(underlying_curve(sK8))
| sK0(underlying_curve(sK8)) = sK3(underlying_curve(sK8)) ),
inference(copy,[status(thm)],[c_7679]) ).
cnf(c_7652,negated_conjecture,
sK0(underlying_curve(sK8)) = sK3(underlying_curve(sK8)),
inference(copy,[status(thm)],[c_7680]) ).
cnf(c_7681,plain,
~ end_point(sK3(underlying_curve(sK8)),underlying_curve(sK8)),
inference(paramod,[status(thm)],[c_7652,c_141]) ).
cnf(c_7666,plain,
$false,
inference(resolve,[status(thm)],[c_5310,c_7681]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO126+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n016.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Fri Sep 25 12:55:45 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 2414711 was started by sandbox2 on n016,
% 0.10/0.37 % Fri Sep 25 12:55:45 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.38
% 0.10/0.38 % From the command line: assign(max_seconds, 300).
% 10.50/1.73
% 10.50/1.73 % given #500 (T,wt=10): 5191 underlying_curve(A) != underlying_curve(B) | incident_o(f8(underlying_curve(A)),B). [back_rewrite(1015),rewrite([4522(1)])].
% 10.50/1.73
% 10.50/1.73 % SZS status Theorem for theBenchmark
% 10.50/1.73
% 10.50/1.73 % Proof 1 at 1.07 (+ 0.27) seconds.
% 10.50/1.73 % Length of proof is 52.
% 10.50/1.73 % Level of proof is 9.
% 10.50/1.73 % Maximum clause weight is 15.000.
% 10.50/1.73 % Given clauses 742.
% 10.50/1.73
% 10.50/1.73 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------