%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GEO127+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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 2.94s 0.84s
% Output : CNFRefutation 2.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 11
% Syntax : Number of formulae : 112 ( 34 unt; 0 def)
% Number of atoms : 302 ( 71 equ)
% Maximal formula atoms : 15 ( 2 avg)
% Number of connectives : 296 ( 106 ~; 137 |; 41 &)
% ( 8 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 3 con; 0-2 aty)
% Number of variables : 160 ( 9 sgn 75 !; 18 ?)
% 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(c6,axiom,
! [C,P] :
( end_point(P,C)
=> ? [Q] :
( P != Q
& end_point(Q,C) ) ),
file('theBenchmark.p',c6) ).
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(o1,axiom,
! [O,P,Q] :
( ordered_by(O,P,Q)
=> ( incident_o(Q,O)
& incident_o(P,O) ) ),
file('theBenchmark.p',o1) ).
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(theorem_4_12,conjecture,
! [O,P] :
( incident_o(P,O)
<=> ? [Q] :
( ordered_by(O,Q,P)
| ordered_by(O,P,Q) ) ),
file('theBenchmark.p',theorem_4_12) ).
fof(theorem_4_12_neg,negated_conjecture,
~ ! [O,P] :
( incident_o(P,O)
<=> ? [Q] :
( ordered_by(O,Q,P)
| ordered_by(O,P,Q) ) ),
inference(assume_negation,[status(cth)],[theorem_4_12]) ).
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_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(sK1(C),C)
| closed(C) )
& ( ! [X0] : ~ end_point(X0,C)
| ~ closed(C) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(P,sK1(C))],[nnf_6]) ).
fof(sk_closed_defn,plain,
( ! [VAR_0] :
( end_point(sK1(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(sK1(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(sK2(C),C)
| ~ open(C) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X0,sK2(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(sK2(VAR_0),VAR_0)
| ~ open(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_open_defn_sk]) ).
cnf(c_41,plain,
( end_point(sK2(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,sK3(O))
| incident_o(P,O) )
& ( incident_c(P,sK3(O))
| ~ incident_o(P,O) ) )
& open(sK3(O)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(C,sK3(O))],[nnf_22]) ).
cnf(c_43,plain,
open(sK3(A)),
inference(split_conjunct,[status(thm)],[sk_o2]) ).
fof(nnf_19,plain,
! [P,O] :
( ( ? [Q] :
( ~ ordered_by(O,P,Q)
& incident_o(Q,O)
& Q != P )
| ~ incident_o(P,O)
| start_point(P,O) )
& ( ( ! [X0] :
( ordered_by(O,P,X0)
| ~ incident_o(X0,O)
| X0 = P )
& incident_o(P,O) )
| ~ start_point(P,O) ) ),
inference(fof_nnf,[status(thm)],[start_point_defn]) ).
fof(sk_start_point_defn_sk,plain,
! [P,O] :
( ( ( ~ ordered_by(O,P,sK4(P,O))
& incident_o(sK4(P,O),O)
& sK4(P,O) != P )
| ~ incident_o(P,O)
| start_point(P,O) )
& ( ( ! [X0] :
( ordered_by(O,P,X0)
| ~ incident_o(X0,O)
| X0 = P )
& incident_o(P,O) )
| ~ start_point(P,O) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(Q,sK4(P,O))],[nnf_19]) ).
fof(sk_start_point_defn,plain,
( ! [VAR_0,VAR_1] :
( ~ ordered_by(VAR_1,VAR_0,sK4(VAR_0,VAR_1))
| ~ incident_o(VAR_0,VAR_1)
| start_point(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( incident_o(sK4(VAR_0,VAR_1),VAR_1)
| ~ incident_o(VAR_0,VAR_1)
| start_point(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( sK4(VAR_0,VAR_1) != VAR_0
| ~ incident_o(VAR_0,VAR_1)
| start_point(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( ordered_by(VAR_1,VAR_0,VAR_2)
| ~ incident_o(VAR_2,VAR_1)
| VAR_2 = VAR_0
| ~ start_point(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( incident_o(VAR_0,VAR_1)
| ~ start_point(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_start_point_defn_sk]) ).
cnf(c_58,plain,
( sK4(A,B) != A
| ~ incident_o(A,B)
| start_point(A,B) ),
inference(split_conjunct,[status(thm)],[sk_start_point_defn]) ).
cnf(c_59,plain,
( ordered_by(B,A,C)
| ~ incident_o(C,B)
| C = A
| ~ start_point(A,B) ),
inference(split_conjunct,[status(thm)],[sk_start_point_defn]) ).
cnf(c_61,plain,
( incident_o(sK4(A,B),B)
| ~ incident_o(A,B)
| start_point(A,B) ),
inference(split_conjunct,[status(thm)],[sk_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(sK5(O),O),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(P,sK5(O))],[nnf_24]) ).
cnf(c_63,plain,
start_point(sK5(A),A),
inference(split_conjunct,[status(thm)],[sk_o4]) ).
cnf(c_92,plain,
( end_point(sK1(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]) ).
fof(nnf_13,plain,
! [C,P] :
( ? [Q] :
( Q != P
& end_point(Q,C) )
| ~ end_point(P,C) ),
inference(fof_nnf,[status(thm)],[c6]) ).
fof(sk_c6_sk,plain,
! [C,P] :
( ( sK6(C,P) != P
& end_point(sK6(C,P),C) )
| ~ end_point(P,C) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(Q,sK6(C,P))],[nnf_13]) ).
fof(sk_c6,plain,
( ! [VAR_0,VAR_1] :
( sK6(VAR_1,VAR_0) != VAR_0
| ~ end_point(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( end_point(sK6(VAR_1,VAR_0),VAR_1)
| ~ end_point(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_c6_sk]) ).
cnf(c_120,plain,
( end_point(sK6(B,A),B)
| ~ end_point(A,B) ),
inference(split_conjunct,[status(thm)],[sk_c6]) ).
cnf(c_121,plain,
( sK6(B,A) != A
| ~ end_point(A,B) ),
inference(split_conjunct,[status(thm)],[sk_c6]) ).
cnf(c_130,plain,
( incident_o(B,A)
| ~ ordered_by(A,B,C) ),
inference(clausify,[status(thm)],[o1]) ).
cnf(c_131,plain,
( incident_o(C,A)
| ~ ordered_by(A,B,C) ),
inference(clausify,[status(thm)],[o1]) ).
cnf(c_133,plain,
( ~ incident_c(A,sK3(B))
| incident_o(A,B) ),
inference(split_conjunct,[status(thm)],[sk_o2]) ).
fof(nnf_28,plain,
? [O,P] :
( ( ! [Q] :
( ~ ordered_by(O,Q,P)
& ~ ordered_by(O,P,Q) )
| ~ incident_o(P,O) )
& ( ? [X0] :
( ordered_by(O,X0,P)
| ordered_by(O,P,X0) )
| incident_o(P,O) ) ),
inference(fof_nnf,[status(thm)],[theorem_4_12_neg]) ).
fof(sk_theorem_4_12_neg_sk,plain,
( ( ! [Q] :
( ~ ordered_by(sK8,Q,sK7)
& ~ ordered_by(sK8,sK7,Q) )
| ~ incident_o(sK7,sK8) )
& ( ordered_by(sK8,sK9,sK7)
| ordered_by(sK8,sK7,sK9)
| incident_o(sK7,sK8) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK8,sK9]),skolemize(O,sK8),skolemize(P,sK7),skolemize(X0,sK9)],[nnf_28]) ).
fof(sk_theorem_4_12_neg,plain,
( ! [VAR_0] :
( ~ ordered_by(sK8,VAR_0,sK7)
| ~ incident_o(sK7,sK8) )
& ! [VAR_0] :
( ~ ordered_by(sK8,sK7,VAR_0)
| ~ incident_o(sK7,sK8) )
& ( ordered_by(sK8,sK9,sK7)
| ordered_by(sK8,sK7,sK9)
| incident_o(sK7,sK8) ) ),
inference(cnf_transformation,[status(thm)],[sk_theorem_4_12_neg_sk]) ).
cnf(c_140,negated_conjecture,
( ordered_by(sK8,sK9,sK7)
| ordered_by(sK8,sK7,sK9)
| incident_o(sK7,sK8) ),
inference(split_conjunct,[status(thm)],[sk_theorem_4_12_neg]) ).
cnf(c_141,negated_conjecture,
( ~ ordered_by(sK8,sK7,A)
| ~ incident_o(sK7,sK8) ),
inference(split_conjunct,[status(thm)],[sk_theorem_4_12_neg]) ).
cnf(c_142,negated_conjecture,
( ~ ordered_by(sK8,A,sK7)
| ~ incident_o(sK7,sK8) ),
inference(split_conjunct,[status(thm)],[sk_theorem_4_12_neg]) ).
cnf(c_143,plain,
~ end_point(sK0(A),A),
inference(resolve,[status(thm)],[c_32,c_30]) ).
cnf(c_144,plain,
incident_c(sK0(A),A),
inference(resolve,[status(thm)],[c_32,c_31]) ).
cnf(c_158,plain,
end_point(sK2(sK3(A)),sK3(A)),
inference(resolve,[status(thm)],[c_43,c_41]) ).
cnf(c_168,plain,
( ordered_by(B,A,C)
| ~ incident_o(C,B)
| C = A
| sK4(A,B) != A
| ~ incident_o(A,B) ),
inference(resolve,[status(thm)],[c_58,c_59]) ).
cnf(c_169,plain,
( ordered_by(B,A,C)
| ~ incident_o(C,B)
| C = A
| incident_o(sK4(A,B),B)
| ~ incident_o(A,B) ),
inference(resolve,[status(thm)],[c_61,c_59]) ).
cnf(c_171,plain,
( ordered_by(B,sK5(B),A)
| ~ incident_o(A,B)
| A = sK5(B) ),
inference(resolve,[status(thm)],[c_63,c_59]) ).
cnf(c_172,plain,
( ordered_by(A,sK5(A),B)
| ~ incident_o(B,A)
| sK5(A) = B ),
inference(copy,[status(thm)],[c_171]) ).
cnf(c_2695,negated_conjecture,
( incident_o(sK7,sK8)
| ordered_by(sK8,sK7,sK9)
| incident_o(sK7,sK8) ),
inference(resolve,[status(thm)],[c_140,c_131]) ).
cnf(c_422,negated_conjecture,
( ordered_by(sK8,sK7,sK9)
| incident_o(sK7,sK8) ),
inference(copy,[status(thm)],[c_2695]) ).
cnf(c_424,plain,
incident_o(sK0(sK3(A)),A),
inference(resolve,[status(thm)],[c_144,c_133]) ).
cnf(c_466,plain,
end_point(sK1(sK3(A)),sK3(A)),
inference(resolve,[status(thm)],[c_158,c_92]) ).
cnf(c_837,plain,
sK6(sK3(A),sK1(sK3(A))) != sK1(sK3(A)),
inference(resolve,[status(thm)],[c_466,c_121]) ).
cnf(c_838,plain,
end_point(sK6(sK3(A),sK1(sK3(A))),sK3(A)),
inference(resolve,[status(thm)],[c_466,c_120]) ).
cnf(c_840,plain,
incident_c(sK1(sK3(A)),sK3(A)),
inference(resolve,[status(thm)],[c_466,c_103]) ).
cnf(c_854,plain,
incident_o(sK1(sK3(A)),A),
inference(resolve,[status(thm)],[c_840,c_133]) ).
cnf(c_2696,plain,
( incident_o(sK7,sK8)
| incident_o(sK7,sK8) ),
inference(resolve,[status(thm)],[c_422,c_130]) ).
cnf(c_889,plain,
incident_o(sK7,sK8),
inference(copy,[status(thm)],[c_2696]) ).
cnf(c_890,negated_conjecture,
~ ordered_by(sK8,A,sK7),
inference(resolve,[status(thm)],[c_889,c_142]) ).
cnf(c_891,negated_conjecture,
~ ordered_by(sK8,sK7,A),
inference(resolve,[status(thm)],[c_889,c_141]) ).
cnf(c_2697,plain,
( ordered_by(sK8,sK5(sK8),sK7)
| sK5(sK8) = sK7 ),
inference(resolve,[status(thm)],[c_889,c_172]) ).
cnf(c_892,negated_conjecture,
sK5(sK8) = sK7,
inference(resolve,[status(thm)],[c_890,c_2697]) ).
cnf(c_2698,plain,
( ordered_by(sK8,sK7,A)
| ~ incident_o(A,sK8)
| A = sK7
| incident_o(sK4(sK7,sK8),sK8) ),
inference(resolve,[status(thm)],[c_889,c_169]) ).
cnf(c_2699,plain,
( ordered_by(sK8,sK7,A)
| ~ incident_o(A,sK8)
| sK7 = A
| incident_o(sK4(sK7,sK8),sK8) ),
inference(copy,[status(thm)],[c_2698]) ).
cnf(c_894,negated_conjecture,
( ~ incident_o(A,sK8)
| sK7 = A
| incident_o(sK4(sK7,sK8),sK8) ),
inference(resolve,[status(thm)],[c_891,c_2699]) ).
cnf(c_2700,plain,
( ordered_by(sK8,sK7,A)
| ~ incident_o(A,sK8)
| A = sK7
| sK4(sK7,sK8) != sK7 ),
inference(resolve,[status(thm)],[c_889,c_168]) ).
cnf(c_2701,plain,
( ordered_by(sK8,sK7,A)
| ~ incident_o(A,sK8)
| sK7 = A
| sK4(sK7,sK8) != sK7 ),
inference(copy,[status(thm)],[c_2700]) ).
cnf(c_896,negated_conjecture,
( ~ incident_o(A,sK8)
| sK7 = A
| sK4(sK7,sK8) != sK7 ),
inference(resolve,[status(thm)],[c_891,c_2701]) ).
cnf(c_1577,plain,
incident_c(sK6(sK3(A),sK1(sK3(A))),sK3(A)),
inference(resolve,[status(thm)],[c_838,c_103]) ).
cnf(c_1757,plain,
incident_o(sK6(sK3(A),sK1(sK3(A))),A),
inference(resolve,[status(thm)],[c_1577,c_133]) ).
cnf(c_2702,plain,
( sK7 = sK1(sK3(sK8))
| incident_o(sK4(sK7,sK8),sK8) ),
inference(resolve,[status(thm)],[c_894,c_854]) ).
cnf(c_2471,plain,
( sK1(sK3(sK8)) = sK7
| incident_o(sK4(sK7,sK8),sK8) ),
inference(copy,[status(thm)],[c_2702]) ).
cnf(c_2703,plain,
( sK7 = sK0(sK3(sK8))
| incident_o(sK4(sK7,sK8),sK8) ),
inference(resolve,[status(thm)],[c_894,c_424]) ).
cnf(c_2473,plain,
( sK0(sK3(sK8)) = sK7
| incident_o(sK4(sK7,sK8),sK8) ),
inference(copy,[status(thm)],[c_2703]) ).
cnf(c_2704,plain,
( ordered_by(sK8,sK5(sK8),sK4(sK7,sK8))
| sK5(sK8) = sK4(sK7,sK8)
| sK1(sK3(sK8)) = sK7 ),
inference(resolve,[status(thm)],[c_2471,c_172]) ).
cnf(c_2705,plain,
( ordered_by(sK8,sK5(sK8),sK4(sK7,sK8))
| sK7 = sK4(sK7,sK8)
| sK1(sK3(sK8)) = sK7 ),
inference(paramod,[status(thm)],[c_892,c_2704]) ).
cnf(c_2706,plain,
( ordered_by(sK8,sK7,sK4(sK7,sK8))
| sK7 = sK4(sK7,sK8)
| sK1(sK3(sK8)) = sK7 ),
inference(paramod,[status(thm)],[c_892,c_2705]) ).
cnf(c_2707,plain,
( ordered_by(sK8,sK7,sK4(sK7,sK8))
| sK4(sK7,sK8) = sK7
| sK1(sK3(sK8)) = sK7 ),
inference(copy,[status(thm)],[c_2706]) ).
cnf(c_2488,negated_conjecture,
( sK4(sK7,sK8) = sK7
| sK1(sK3(sK8)) = sK7 ),
inference(resolve,[status(thm)],[c_891,c_2707]) ).
cnf(c_2708,plain,
( ordered_by(sK8,sK5(sK8),sK4(sK7,sK8))
| sK5(sK8) = sK4(sK7,sK8)
| sK0(sK3(sK8)) = sK7 ),
inference(resolve,[status(thm)],[c_2473,c_172]) ).
cnf(c_2709,plain,
( ordered_by(sK8,sK5(sK8),sK4(sK7,sK8))
| sK7 = sK4(sK7,sK8)
| sK0(sK3(sK8)) = sK7 ),
inference(paramod,[status(thm)],[c_892,c_2708]) ).
cnf(c_2710,plain,
( ordered_by(sK8,sK7,sK4(sK7,sK8))
| sK7 = sK4(sK7,sK8)
| sK0(sK3(sK8)) = sK7 ),
inference(paramod,[status(thm)],[c_892,c_2709]) ).
cnf(c_2711,plain,
( ordered_by(sK8,sK7,sK4(sK7,sK8))
| sK4(sK7,sK8) = sK7
| sK0(sK3(sK8)) = sK7 ),
inference(copy,[status(thm)],[c_2710]) ).
cnf(c_2512,negated_conjecture,
( sK4(sK7,sK8) = sK7
| sK0(sK3(sK8)) = sK7 ),
inference(resolve,[status(thm)],[c_891,c_2711]) ).
cnf(c_2578,plain,
( end_point(sK7,sK3(sK8))
| sK4(sK7,sK8) = sK7 ),
inference(paramod,[status(thm)],[c_2488,c_466]) ).
cnf(c_2612,plain,
( ~ end_point(sK7,sK3(sK8))
| sK4(sK7,sK8) = sK7 ),
inference(paramod,[status(thm)],[c_2512,c_143]) ).
cnf(c_2712,plain,
( sK4(sK7,sK8) = sK7
| sK4(sK7,sK8) = sK7 ),
inference(resolve,[status(thm)],[c_2612,c_2578]) ).
cnf(c_2645,plain,
sK4(sK7,sK8) = sK7,
inference(copy,[status(thm)],[c_2712]) ).
cnf(c_2713,negated_conjecture,
( ~ incident_o(A,sK8)
| sK7 = A
| sK7 != sK7 ),
inference(paramod,[status(thm)],[c_2645,c_896]) ).
cnf(c_2650,negated_conjecture,
( ~ incident_o(A,sK8)
| sK7 = A ),
inference(copy,[status(thm)],[c_2713]) ).
cnf(c_2714,plain,
sK7 = sK6(sK3(sK8),sK1(sK3(sK8))),
inference(resolve,[status(thm)],[c_2650,c_1757]) ).
cnf(c_2653,plain,
sK6(sK3(sK8),sK1(sK3(sK8))) = sK7,
inference(copy,[status(thm)],[c_2714]) ).
cnf(c_2715,plain,
sK7 = sK1(sK3(sK8)),
inference(resolve,[status(thm)],[c_2650,c_854]) ).
cnf(c_2661,plain,
sK1(sK3(sK8)) = sK7,
inference(copy,[status(thm)],[c_2715]) ).
cnf(c_2667,plain,
sK6(sK3(sK8),sK7) = sK7,
inference(paramod,[status(thm)],[c_2661,c_2653]) ).
cnf(c_2716,plain,
sK6(sK3(sK8),sK7) != sK1(sK3(sK8)),
inference(paramod,[status(thm)],[c_2661,c_837]) ).
cnf(c_2717,plain,
sK7 != sK1(sK3(sK8)),
inference(paramod,[status(thm)],[c_2667,c_2716]) ).
cnf(c_2718,plain,
sK7 != sK7,
inference(paramod,[status(thm)],[c_2661,c_2717]) ).
cnf(c_2694,plain,
$false,
inference(copy,[status(thm)],[c_2718]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO127+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.38 % Computer : n004.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Fri Sep 25 12:51:07 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.12/0.39 % Process 3202453 was started by sandbox on n004,
% 0.12/0.39 % Fri Sep 25 12:51:07 2026
% 0.12/0.39 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.12/0.40
% 0.12/0.40 % From the command line: assign(max_seconds, 300).
% 2.94/0.84
% 2.94/0.84 % SZS status Theorem for theBenchmark
% 2.94/0.84
% 2.94/0.84 % Proof 1 at 0.32 (+ 0.09) seconds.
% 2.94/0.84 % Length of proof is 66.
% 2.94/0.84 % Level of proof is 13.
% 2.94/0.84 % Maximum clause weight is 18.000.
% 2.94/0.84 % Given clauses 342.
% 2.94/0.84
% 2.94/0.84 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------