%------------------------------------------------------------------------------
% 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/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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 : Unsatisfiable 3.14s 0.84s
% Output : CNFRefutation 3.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 20
% Syntax : Number of formulae : 98 ( 31 unt; 0 def)
% Number of atoms : 201 ( 62 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 176 ( 73 ~; 103 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 3 con; 0-2 aty)
% Number of variables : 102 ( 9 sgn 34 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(inner_point_defn_22,axiom,
! [VAR_0,VAR_1] :
( ~ end_point(VAR_0,VAR_1)
| ~ inner_point(VAR_0,VAR_1) ),
file('theBenchmark.p',inner_point_defn_22) ).
cnf(c_2,plain,
( ~ end_point(A,B)
| ~ inner_point(A,B) ),
inference(clausify,[status(thm)],[inner_point_defn_22]) ).
fof(inner_point_defn_21,axiom,
! [VAR_0,VAR_1] :
( incident_c(VAR_0,VAR_1)
| ~ inner_point(VAR_0,VAR_1) ),
file('theBenchmark.p',inner_point_defn_21) ).
cnf(c_3,plain,
( incident_c(A,B)
| ~ inner_point(A,B) ),
inference(clausify,[status(thm)],[inner_point_defn_21]) ).
fof(c3_37,axiom,
! [VAR_0] : inner_point(ax0_sk8(VAR_0),VAR_0),
file('theBenchmark.p',c3_37) ).
cnf(c_4,plain,
inner_point(ax0_sk8(A),A),
inference(clausify,[status(thm)],[c3_37]) ).
fof(closed_defn_32,axiom,
! [VAR_0] :
( closed(VAR_0)
| end_point(ax0_sk6(VAR_0),VAR_0) ),
file('theBenchmark.p',closed_defn_32) ).
cnf(c_9,plain,
( closed(A)
| end_point(ax0_sk6(A),A) ),
inference(clausify,[status(thm)],[closed_defn_32]) ).
fof(closed_defn_31,axiom,
! [VAR_0,VAR_1] :
( ~ end_point(VAR_1,VAR_0)
| ~ closed(VAR_0) ),
file('theBenchmark.p',closed_defn_31) ).
cnf(c_11,plain,
( ~ end_point(B,A)
| ~ closed(A) ),
inference(clausify,[status(thm)],[closed_defn_31]) ).
fof(open_defn_33,axiom,
! [VAR_0] :
( end_point(ax0_sk7(VAR_0),VAR_0)
| ~ open(VAR_0) ),
file('theBenchmark.p',open_defn_33) ).
cnf(c_13,plain,
( end_point(ax0_sk7(A),A)
| ~ open(A) ),
inference(clausify,[status(thm)],[open_defn_33]) ).
fof(o2_19,axiom,
! [VAR_0] : open(ax2_sk3(VAR_0)),
file('theBenchmark.p',o2_19) ).
cnf(c_15,plain,
open(ax2_sk3(A)),
inference(clausify,[status(thm)],[o2_19]) ).
fof(start_point_defn_9,axiom,
! [VAR_0,VAR_1] :
( start_point(VAR_0,VAR_1)
| VAR_0 != ax2_sk1(VAR_1,VAR_0)
| ~ incident_o(VAR_0,VAR_1) ),
file('theBenchmark.p',start_point_defn_9) ).
cnf(c_32,plain,
( start_point(A,B)
| A != ax2_sk1(B,A)
| ~ incident_o(A,B) ),
inference(clausify,[status(thm)],[start_point_defn_9]) ).
fof(start_point_defn_8,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ordered_by(VAR_1,VAR_0,VAR_2)
| ~ incident_o(VAR_2,VAR_1)
| VAR_0 = VAR_2
| ~ start_point(VAR_0,VAR_1) ),
file('theBenchmark.p',start_point_defn_8) ).
cnf(c_33,plain,
( ordered_by(B,A,C)
| ~ incident_o(C,B)
| A = C
| ~ start_point(A,B) ),
inference(clausify,[status(thm)],[start_point_defn_8]) ).
fof(start_point_defn_10,axiom,
! [VAR_0,VAR_1] :
( start_point(VAR_0,VAR_1)
| incident_o(ax2_sk1(VAR_1,VAR_0),VAR_1)
| ~ incident_o(VAR_0,VAR_1) ),
file('theBenchmark.p',start_point_defn_10) ).
cnf(c_35,plain,
( start_point(A,B)
| incident_o(ax2_sk1(B,A),B)
| ~ incident_o(A,B) ),
inference(clausify,[status(thm)],[start_point_defn_10]) ).
fof(o4_29,axiom,
! [VAR_0] : start_point(ax2_sk6(VAR_0),VAR_0),
file('theBenchmark.p',o4_29) ).
cnf(c_37,plain,
start_point(ax2_sk6(A),A),
inference(clausify,[status(thm)],[o4_29]) ).
cnf(c_67,plain,
( end_point(ax0_sk6(B),B)
| ~ end_point(A,B) ),
inference(resolve,[status(thm)],[c_11,c_9]) ).
fof(end_point_defn_13,axiom,
! [VAR_0,VAR_1] :
( incident_c(VAR_0,VAR_1)
| ~ end_point(VAR_0,VAR_1) ),
file('theBenchmark.p',end_point_defn_13) ).
cnf(c_88,plain,
( incident_c(A,B)
| ~ end_point(A,B) ),
inference(clausify,[status(thm)],[end_point_defn_13]) ).
fof(c6_41,axiom,
! [VAR_0,VAR_1] :
( end_point(ax0_sk11(VAR_0,VAR_1),VAR_1)
| ~ end_point(VAR_0,VAR_1) ),
file('theBenchmark.p',c6_41) ).
cnf(c_105,plain,
( end_point(ax0_sk11(A,B),B)
| ~ end_point(A,B) ),
inference(clausify,[status(thm)],[c6_41]) ).
fof(c6_42,axiom,
! [VAR_0,VAR_1] :
( VAR_0 != ax0_sk11(VAR_0,VAR_1)
| ~ end_point(VAR_0,VAR_1) ),
file('theBenchmark.p',c6_42) ).
cnf(c_106,plain,
( A != ax0_sk11(A,B)
| ~ end_point(A,B) ),
inference(clausify,[status(thm)],[c6_42]) ).
cnf(c_107,plain,
( ax0_sk11(A,B) != A
| ~ end_point(A,B) ),
inference(copy,[status(thm)],[c_106]) ).
fof(o1_17,axiom,
! [VAR_0,VAR_1,VAR_2] :
( incident_o(VAR_1,VAR_0)
| ~ ordered_by(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',o1_17) ).
cnf(c_115,plain,
( incident_o(B,A)
| ~ ordered_by(A,B,C) ),
inference(clausify,[status(thm)],[o1_17]) ).
fof(o1_18,axiom,
! [VAR_0,VAR_1,VAR_2] :
( incident_o(VAR_2,VAR_0)
| ~ ordered_by(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',o1_18) ).
cnf(c_116,plain,
( incident_o(C,A)
| ~ ordered_by(A,B,C) ),
inference(clausify,[status(thm)],[o1_18]) ).
fof(o2_21,axiom,
! [VAR_0,VAR_1] :
( incident_o(VAR_0,VAR_1)
| ~ incident_c(VAR_0,ax2_sk3(VAR_1)) ),
file('theBenchmark.p',o2_21) ).
cnf(c_118,plain,
( incident_o(A,B)
| ~ incident_c(A,ax2_sk3(B)) ),
inference(clausify,[status(thm)],[o2_21]) ).
fof(theorem_4_12_133,axiom,
( ordered_by(sk25,sk27,sk26)
| ordered_by(sk25,sk26,sk27)
| incident_o(sk26,sk25) ),
file('theBenchmark.p',theorem_4_12_133) ).
cnf(c_131,plain,
( ordered_by(sk25,sk27,sk26)
| ordered_by(sk25,sk26,sk27)
| incident_o(sk26,sk25) ),
inference(clausify,[status(thm)],[theorem_4_12_133]) ).
fof(theorem_4_12_137,axiom,
! [VAR_0] :
( ~ incident_o(sk26,sk25)
| ~ ordered_by(sk25,sk26,VAR_0) ),
file('theBenchmark.p',theorem_4_12_137) ).
cnf(c_134,plain,
( ~ incident_o(sk26,sk25)
| ~ ordered_by(sk25,sk26,A) ),
inference(clausify,[status(thm)],[theorem_4_12_137]) ).
fof(theorem_4_12_138,axiom,
! [VAR_0] :
( ~ incident_o(sk26,sk25)
| ~ ordered_by(sk25,VAR_0,sk26) ),
file('theBenchmark.p',theorem_4_12_138) ).
cnf(c_135,plain,
( ~ incident_o(sk26,sk25)
| ~ ordered_by(sk25,A,sk26) ),
inference(clausify,[status(thm)],[theorem_4_12_138]) ).
cnf(c_136,plain,
~ end_point(ax0_sk8(A),A),
inference(resolve,[status(thm)],[c_4,c_2]) ).
cnf(c_137,plain,
incident_c(ax0_sk8(A),A),
inference(resolve,[status(thm)],[c_4,c_3]) ).
cnf(c_154,plain,
end_point(ax0_sk7(ax2_sk3(A)),ax2_sk3(A)),
inference(resolve,[status(thm)],[c_15,c_13]) ).
cnf(c_164,plain,
( ordered_by(B,A,C)
| ~ incident_o(C,B)
| A = C
| A != ax2_sk1(B,A)
| ~ incident_o(A,B) ),
inference(resolve,[status(thm)],[c_32,c_33]) ).
cnf(c_165,plain,
( ordered_by(B,A,C)
| ~ incident_o(C,B)
| A = C
| ax2_sk1(B,A) != A
| ~ incident_o(A,B) ),
inference(copy,[status(thm)],[c_164]) ).
cnf(c_166,plain,
( ordered_by(B,A,C)
| ~ incident_o(C,B)
| A = C
| incident_o(ax2_sk1(B,A),B)
| ~ incident_o(A,B) ),
inference(resolve,[status(thm)],[c_35,c_33]) ).
cnf(c_168,plain,
( ordered_by(A,ax2_sk6(A),B)
| ~ incident_o(B,A)
| ax2_sk6(A) = B ),
inference(resolve,[status(thm)],[c_37,c_33]) ).
cnf(c_2681,plain,
( incident_o(sk26,sk25)
| ordered_by(sk25,sk26,sk27)
| incident_o(sk26,sk25) ),
inference(resolve,[status(thm)],[c_131,c_116]) ).
cnf(c_418,plain,
( ordered_by(sk25,sk26,sk27)
| incident_o(sk26,sk25) ),
inference(copy,[status(thm)],[c_2681]) ).
cnf(c_420,plain,
incident_o(ax0_sk8(ax2_sk3(A)),A),
inference(resolve,[status(thm)],[c_137,c_118]) ).
cnf(c_462,plain,
end_point(ax0_sk6(ax2_sk3(A)),ax2_sk3(A)),
inference(resolve,[status(thm)],[c_154,c_67]) ).
cnf(c_823,plain,
ax0_sk11(ax0_sk6(ax2_sk3(A)),ax2_sk3(A)) != ax0_sk6(ax2_sk3(A)),
inference(resolve,[status(thm)],[c_462,c_107]) ).
cnf(c_824,plain,
end_point(ax0_sk11(ax0_sk6(ax2_sk3(A)),ax2_sk3(A)),ax2_sk3(A)),
inference(resolve,[status(thm)],[c_462,c_105]) ).
cnf(c_826,plain,
incident_c(ax0_sk6(ax2_sk3(A)),ax2_sk3(A)),
inference(resolve,[status(thm)],[c_462,c_88]) ).
cnf(c_840,plain,
incident_o(ax0_sk6(ax2_sk3(A)),A),
inference(resolve,[status(thm)],[c_826,c_118]) ).
cnf(c_2682,plain,
( incident_o(sk26,sk25)
| incident_o(sk26,sk25) ),
inference(resolve,[status(thm)],[c_418,c_115]) ).
cnf(c_875,plain,
incident_o(sk26,sk25),
inference(copy,[status(thm)],[c_2682]) ).
cnf(c_876,plain,
~ ordered_by(sk25,A,sk26),
inference(resolve,[status(thm)],[c_875,c_135]) ).
cnf(c_877,plain,
~ ordered_by(sk25,sk26,A),
inference(resolve,[status(thm)],[c_875,c_134]) ).
cnf(c_2683,plain,
( ordered_by(sk25,ax2_sk6(sk25),sk26)
| ax2_sk6(sk25) = sk26 ),
inference(resolve,[status(thm)],[c_875,c_168]) ).
cnf(c_878,plain,
ax2_sk6(sk25) = sk26,
inference(resolve,[status(thm)],[c_876,c_2683]) ).
cnf(c_2684,plain,
( ordered_by(sk25,sk26,A)
| ~ incident_o(A,sk25)
| sk26 = A
| incident_o(ax2_sk1(sk25,sk26),sk25) ),
inference(resolve,[status(thm)],[c_875,c_166]) ).
cnf(c_880,plain,
( ~ incident_o(A,sk25)
| sk26 = A
| incident_o(ax2_sk1(sk25,sk26),sk25) ),
inference(resolve,[status(thm)],[c_877,c_2684]) ).
cnf(c_2685,plain,
( ordered_by(sk25,sk26,A)
| ~ incident_o(A,sk25)
| sk26 = A
| ax2_sk1(sk25,sk26) != sk26 ),
inference(resolve,[status(thm)],[c_875,c_165]) ).
cnf(c_882,plain,
( ~ incident_o(A,sk25)
| sk26 = A
| ax2_sk1(sk25,sk26) != sk26 ),
inference(resolve,[status(thm)],[c_877,c_2685]) ).
cnf(c_1563,plain,
incident_c(ax0_sk11(ax0_sk6(ax2_sk3(A)),ax2_sk3(A)),ax2_sk3(A)),
inference(resolve,[status(thm)],[c_824,c_88]) ).
cnf(c_1743,plain,
incident_o(ax0_sk11(ax0_sk6(ax2_sk3(A)),ax2_sk3(A)),A),
inference(resolve,[status(thm)],[c_1563,c_118]) ).
cnf(c_2686,plain,
( sk26 = ax0_sk6(ax2_sk3(sk25))
| incident_o(ax2_sk1(sk25,sk26),sk25) ),
inference(resolve,[status(thm)],[c_880,c_840]) ).
cnf(c_2457,plain,
( ax0_sk6(ax2_sk3(sk25)) = sk26
| incident_o(ax2_sk1(sk25,sk26),sk25) ),
inference(copy,[status(thm)],[c_2686]) ).
cnf(c_2687,plain,
( sk26 = ax0_sk8(ax2_sk3(sk25))
| incident_o(ax2_sk1(sk25,sk26),sk25) ),
inference(resolve,[status(thm)],[c_880,c_420]) ).
cnf(c_2459,plain,
( ax0_sk8(ax2_sk3(sk25)) = sk26
| incident_o(ax2_sk1(sk25,sk26),sk25) ),
inference(copy,[status(thm)],[c_2687]) ).
cnf(c_2688,plain,
( ordered_by(sk25,ax2_sk6(sk25),ax2_sk1(sk25,sk26))
| ax2_sk6(sk25) = ax2_sk1(sk25,sk26)
| ax0_sk6(ax2_sk3(sk25)) = sk26 ),
inference(resolve,[status(thm)],[c_2457,c_168]) ).
cnf(c_2689,plain,
( ordered_by(sk25,ax2_sk6(sk25),ax2_sk1(sk25,sk26))
| sk26 = ax2_sk1(sk25,sk26)
| ax0_sk6(ax2_sk3(sk25)) = sk26 ),
inference(paramod,[status(thm)],[c_878,c_2688]) ).
cnf(c_2690,plain,
( ordered_by(sk25,sk26,ax2_sk1(sk25,sk26))
| sk26 = ax2_sk1(sk25,sk26)
| ax0_sk6(ax2_sk3(sk25)) = sk26 ),
inference(paramod,[status(thm)],[c_878,c_2689]) ).
cnf(c_2691,plain,
( ordered_by(sk25,sk26,ax2_sk1(sk25,sk26))
| ax2_sk1(sk25,sk26) = sk26
| ax0_sk6(ax2_sk3(sk25)) = sk26 ),
inference(copy,[status(thm)],[c_2690]) ).
cnf(c_2474,plain,
( ax2_sk1(sk25,sk26) = sk26
| ax0_sk6(ax2_sk3(sk25)) = sk26 ),
inference(resolve,[status(thm)],[c_877,c_2691]) ).
cnf(c_2692,plain,
( ordered_by(sk25,ax2_sk6(sk25),ax2_sk1(sk25,sk26))
| ax2_sk6(sk25) = ax2_sk1(sk25,sk26)
| ax0_sk8(ax2_sk3(sk25)) = sk26 ),
inference(resolve,[status(thm)],[c_2459,c_168]) ).
cnf(c_2693,plain,
( ordered_by(sk25,ax2_sk6(sk25),ax2_sk1(sk25,sk26))
| sk26 = ax2_sk1(sk25,sk26)
| ax0_sk8(ax2_sk3(sk25)) = sk26 ),
inference(paramod,[status(thm)],[c_878,c_2692]) ).
cnf(c_2694,plain,
( ordered_by(sk25,sk26,ax2_sk1(sk25,sk26))
| sk26 = ax2_sk1(sk25,sk26)
| ax0_sk8(ax2_sk3(sk25)) = sk26 ),
inference(paramod,[status(thm)],[c_878,c_2693]) ).
cnf(c_2695,plain,
( ordered_by(sk25,sk26,ax2_sk1(sk25,sk26))
| ax2_sk1(sk25,sk26) = sk26
| ax0_sk8(ax2_sk3(sk25)) = sk26 ),
inference(copy,[status(thm)],[c_2694]) ).
cnf(c_2498,plain,
( ax2_sk1(sk25,sk26) = sk26
| ax0_sk8(ax2_sk3(sk25)) = sk26 ),
inference(resolve,[status(thm)],[c_877,c_2695]) ).
cnf(c_2564,plain,
( end_point(sk26,ax2_sk3(sk25))
| ax2_sk1(sk25,sk26) = sk26 ),
inference(paramod,[status(thm)],[c_2474,c_462]) ).
cnf(c_2598,plain,
( ~ end_point(sk26,ax2_sk3(sk25))
| ax2_sk1(sk25,sk26) = sk26 ),
inference(paramod,[status(thm)],[c_2498,c_136]) ).
cnf(c_2696,plain,
( ax2_sk1(sk25,sk26) = sk26
| ax2_sk1(sk25,sk26) = sk26 ),
inference(resolve,[status(thm)],[c_2598,c_2564]) ).
cnf(c_2631,plain,
ax2_sk1(sk25,sk26) = sk26,
inference(copy,[status(thm)],[c_2696]) ).
cnf(c_2697,plain,
( ~ incident_o(A,sk25)
| sk26 = A
| sk26 != sk26 ),
inference(paramod,[status(thm)],[c_2631,c_882]) ).
cnf(c_2636,plain,
( ~ incident_o(A,sk25)
| sk26 = A ),
inference(copy,[status(thm)],[c_2697]) ).
cnf(c_2698,plain,
sk26 = ax0_sk11(ax0_sk6(ax2_sk3(sk25)),ax2_sk3(sk25)),
inference(resolve,[status(thm)],[c_2636,c_1743]) ).
cnf(c_2639,plain,
ax0_sk11(ax0_sk6(ax2_sk3(sk25)),ax2_sk3(sk25)) = sk26,
inference(copy,[status(thm)],[c_2698]) ).
cnf(c_2699,plain,
sk26 = ax0_sk6(ax2_sk3(sk25)),
inference(resolve,[status(thm)],[c_2636,c_840]) ).
cnf(c_2647,plain,
ax0_sk6(ax2_sk3(sk25)) = sk26,
inference(copy,[status(thm)],[c_2699]) ).
cnf(c_2653,plain,
ax0_sk11(sk26,ax2_sk3(sk25)) = sk26,
inference(paramod,[status(thm)],[c_2647,c_2639]) ).
cnf(c_2700,plain,
ax0_sk11(sk26,ax2_sk3(sk25)) != ax0_sk6(ax2_sk3(sk25)),
inference(paramod,[status(thm)],[c_2647,c_823]) ).
cnf(c_2701,plain,
sk26 != ax0_sk6(ax2_sk3(sk25)),
inference(paramod,[status(thm)],[c_2653,c_2700]) ).
cnf(c_2702,plain,
sk26 != sk26,
inference(paramod,[status(thm)],[c_2647,c_2701]) ).
cnf(c_2680,plain,
$false,
inference(copy,[status(thm)],[c_2702]) ).
%------------------------------------------------------------------------------
%----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/sandbox2/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n026.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Fri Sep 25 12:53:39 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.38 % Process 2558231 was started by sandbox2 on n026,
% 0.11/0.38 % Fri Sep 25 12:53:39 2026
% 0.11/0.38 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.11/0.38
% 0.11/0.38 % From the command line: assign(max_seconds, 300).
% 3.14/0.84
% 3.14/0.84 % SZS status Unsatisfiable for theBenchmark
% 3.14/0.84
% 3.14/0.84 % Proof 1 at 0.33 (+ 0.11) seconds.
% 3.14/0.84 % Length of proof is 56.
% 3.14/0.84 % Level of proof is 12.
% 3.14/0.84 % Maximum clause weight is 18.000.
% 3.14/0.84 % Given clauses 344.
% 3.14/0.84
% 3.14/0.84 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------