%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GEO507+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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:18:01 AM UTC 2026
% Result : Theorem 92.92s 13.52s
% Output : CNFRefutation 92.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 8
% Syntax : Number of formulae : 39 ( 17 unt; 0 def)
% Number of atoms : 104 ( 17 equ)
% Maximal formula atoms : 30 ( 2 avg)
% Number of connectives : 117 ( 52 ~; 53 |; 12 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-5 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-5 aty)
% Number of variables : 91 ( 9 sgn 35 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(aSatz3_3,axiom,
! [Xa1,Xb1] : s_t(Xa1,Xa1,Xb1),
file('theBenchmark.p',aSatz3_3) ).
fof(aSatz4_11a,axiom,
! [Xa,Xb,Xc] :
( s_col(Xb,Xc,Xa)
| ~ s_col(Xa,Xb,Xc) ),
file('theBenchmark.p',aSatz4_11a) ).
fof(aSatz4_12b,axiom,
! [Xa,Xb] : s_col(Xa,Xb,Xa),
file('theBenchmark.p',aSatz4_12b) ).
fof(aSatz8_6,axiom,
! [Xa,Xb,Xc,Xa1] :
( Xb = Xc
| ~ s_t(Xa,Xc,Xa1)
| ~ s_r(Xa1,Xb,Xc)
| ~ s_r(Xa,Xb,Xc) ),
file('theBenchmark.p',aSatz8_6) ).
fof(aSatz8_12b,axiom,
! [Xa,Xb,Xp,Xq] :
( perp(Xp,Xq,Xa,Xb)
| ~ perp(Xa,Xb,Xp,Xq) ),
file('theBenchmark.p',aSatz8_12b) ).
fof(d_Defn8_11b,axiom,
! [Xp,Xq,Xp1,Xq1,X] :
( ( ~ perpAt(Xp,Xq,X,Xp1,Xq1)
| perp(Xp,Xq,Xp1,Xq1) )
& ( perpAt(Xp,Xq,il(Xp,Xq,Xp1,Xq1),Xp1,Xq1)
| ~ perp(Xp,Xq,Xp1,Xq1) ) ),
file('theBenchmark.p',d_Defn8_11b) ).
fof(d_Defn8_11a,axiom,
! [Y,Z,X,Y1,Z1,U,V] :
( ( ~ s_r(f811(Y,Z,Y1,Z1,X),X,g811(Y,Z,Y1,Z1,X))
| ~ s_col(Y1,Z1,X)
| ~ s_col(Y,Z,X)
| Y1 = Z1
| Y = Z
| perpAt(Y,Z,X,Y1,Z1) )
& ( s_col(Y1,Z1,g811(Y,Z,Y1,Z1,X))
| ~ s_col(Y1,Z1,X)
| ~ s_col(Y,Z,X)
| Y1 = Z1
| Y = Z
| perpAt(Y,Z,X,Y1,Z1) )
& ( s_col(Y,Z,f811(Y,Z,Y1,Z1,X))
| ~ s_col(Y1,Z1,X)
| ~ s_col(Y,Z,X)
| Y1 = Z1
| Y = Z
| perpAt(Y,Z,X,Y1,Z1) )
& ( s_r(U,X,V)
| ~ s_col(Y1,Z1,V)
| ~ s_col(Y,Z,U)
| ~ perpAt(Y,Z,X,Y1,Z1) )
& ( Y1 != Z1
| ~ perpAt(Y,Z,X,Y1,Z1) )
& ( Y != Z
| ~ perpAt(Y,Z,X,Y1,Z1) )
& ( s_col(Y1,Z1,X)
| ~ perpAt(Y,Z,X,Y1,Z1) )
& ( s_col(Y,Z,X)
| ~ perpAt(Y,Z,X,Y1,Z1) ) ),
file('theBenchmark.p',d_Defn8_11a) ).
fof(aSatz8_14a,conjecture,
! [Xa,Xb,Xp,Xq] :
( ~ s_col(Xa,Xb,Xq)
| ~ s_col(Xa,Xb,Xp)
| ~ perp(Xa,Xb,Xp,Xq) ),
file('theBenchmark.p',aSatz8_14a) ).
fof(aSatz8_14a_neg,negated_conjecture,
~ ! [Xa,Xb,Xp,Xq] :
( ~ s_col(Xa,Xb,Xq)
| ~ s_col(Xa,Xb,Xp)
| ~ perp(Xa,Xb,Xp,Xq) ),
inference(assume_negation,[status(cth)],[aSatz8_14a]) ).
cnf(c_203,plain,
( B != A
| ~ perpAt(A,B,C,D,E) ),
inference(clausify,[status(thm)],[d_Defn8_11a]) ).
cnf(c_205,plain,
( s_r(F,C,V6)
| ~ s_col(D,E,V6)
| ~ s_col(A,B,F)
| ~ perpAt(A,B,C,D,E) ),
inference(clausify,[status(thm)],[d_Defn8_11a]) ).
cnf(c_232,plain,
s_t(A,A,B),
inference(clausify,[status(thm)],[aSatz3_3]) ).
cnf(c_250,plain,
( s_col(B,C,A)
| ~ s_col(A,B,C) ),
inference(clausify,[status(thm)],[aSatz4_11a]) ).
cnf(c_256,plain,
s_col(A,B,A),
inference(clausify,[status(thm)],[aSatz4_12b]) ).
cnf(c_322,plain,
( B = C
| ~ s_t(A,C,D)
| ~ s_r(D,B,C)
| ~ s_r(A,B,C) ),
inference(clausify,[status(thm)],[aSatz8_6]) ).
cnf(c_328,plain,
( perp(C,D,A,B)
| ~ perp(A,B,C,D) ),
inference(clausify,[status(thm)],[aSatz8_12b]) ).
cnf(c_349,plain,
( perpAt(A,B,il(A,B,C,D),C,D)
| ~ perp(A,B,C,D) ),
inference(clausify,[status(thm)],[d_Defn8_11b]) ).
fof(nnf_141,plain,
? [Xa,Xb,Xp,Xq] :
( s_col(Xa,Xb,Xq)
& s_col(Xa,Xb,Xp)
& perp(Xa,Xb,Xp,Xq) ),
inference(fof_nnf,[status(thm)],[aSatz8_14a_neg]) ).
fof(sk_aSatz8_14a_neg,plain,
( s_col(sK0,sK1,sK3)
& s_col(sK0,sK1,sK2)
& perp(sK0,sK1,sK2,sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3]),skolemize(Xa,sK0),skolemize(Xb,sK1),skolemize(Xp,sK2),skolemize(Xq,sK3)],[nnf_141]) ).
cnf(c_351,negated_conjecture,
perp(sK0,sK1,sK2,sK3),
inference(split_conjunct,[status(thm)],[sk_aSatz8_14a_neg]) ).
cnf(c_352,negated_conjecture,
s_col(sK0,sK1,sK2),
inference(split_conjunct,[status(thm)],[sk_aSatz8_14a_neg]) ).
cnf(c_353,negated_conjecture,
s_col(sK0,sK1,sK3),
inference(split_conjunct,[status(thm)],[sk_aSatz8_14a_neg]) ).
cnf(c_369,plain,
( B = C
| ~ s_t(A,C,A)
| ~ s_r(A,B,C) ),
inference(factor,[status(thm)],[c_322]) ).
cnf(c_400,plain,
( s_r(A,C,F)
| ~ s_col(D,E,F)
| ~ perpAt(A,B,C,D,E) ),
inference(resolve,[status(thm)],[c_256,c_205]) ).
cnf(c_425,plain,
( s_r(D,C,sK3)
| ~ s_col(A,B,D)
| ~ perpAt(A,B,C,sK0,sK1) ),
inference(resolve,[status(thm)],[c_353,c_205]) ).
cnf(c_435,plain,
s_col(A,B,B),
inference(resolve,[status(thm)],[c_250,c_256]) ).
cnf(c_625,plain,
perp(sK2,sK3,sK0,sK1),
inference(resolve,[status(thm)],[c_328,c_351]) ).
cnf(c_1052,plain,
( s_r(A,C,sK2)
| ~ perpAt(A,B,C,sK0,sK1) ),
inference(resolve,[status(thm)],[c_400,c_352]) ).
cnf(c_1086,plain,
( s_r(B,C,sK3)
| ~ perpAt(A,B,C,sK0,sK1) ),
inference(resolve,[status(thm)],[c_425,c_435]) ).
cnf(c_12268,plain,
perpAt(sK2,sK3,il(sK2,sK3,sK0,sK1),sK0,sK1),
inference(resolve,[status(thm)],[c_349,c_625]) ).
cnf(c_12303,plain,
s_r(sK3,il(sK2,sK3,sK0,sK1),sK3),
inference(resolve,[status(thm)],[c_12268,c_1086]) ).
cnf(c_12305,plain,
s_r(sK2,il(sK2,sK3,sK0,sK1),sK2),
inference(resolve,[status(thm)],[c_12268,c_1052]) ).
cnf(c_12318,plain,
sK3 != sK2,
inference(resolve,[status(thm)],[c_12268,c_203]) ).
cnf(c_16160,plain,
( il(sK2,sK3,sK0,sK1) = sK3
| ~ s_t(sK3,sK3,sK3) ),
inference(resolve,[status(thm)],[c_12303,c_369]) ).
cnf(c_16109,plain,
il(sK2,sK3,sK0,sK1) = sK3,
inference(resolve,[status(thm)],[c_232,c_16160]) ).
cnf(c_16149,plain,
s_r(sK2,sK3,sK2),
inference(paramod,[status(thm)],[c_16109,c_12305]) ).
cnf(c_16161,plain,
( sK3 = sK2
| ~ s_t(sK2,sK2,sK2) ),
inference(resolve,[status(thm)],[c_16149,c_369]) ).
cnf(c_16162,plain,
sK3 = sK2,
inference(resolve,[status(thm)],[c_232,c_16161]) ).
cnf(c_16159,plain,
$false,
inference(resolve,[status(thm)],[c_12318,c_16162]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO507+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.58 % Computer : n006.cluster.edu
% 0.09/0.58 % Model : x86_64 x86_64
% 0.09/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.58 % Memory : 8046.5625MB
% 0.09/0.58 % OS : Linux 6.8.0-71-generic
% 0.09/0.58 % CPULimit : 300
% 0.09/0.58 % WCLimit : 300
% 0.09/0.58 % DateTime : Fri Sep 25 13:36:58 UTC 2026
% 0.09/0.58 % CPUTime :
% 0.09/0.58 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.58 % Process 3030512 was started by sandbox2 on n006,
% 0.09/0.58 % Fri Sep 25 13:36:58 2026
% 0.09/0.58 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.62
% 0.09/0.62 % From the command line: assign(max_seconds, 300).
% 0.09/0.62
% 0.09/0.62 % SInE: 125 to sos, 18 to usable, of 143 axioms (tolerance 2.00, depth 0 fixpoint).
% 92.92/13.52
% 92.92/13.52 % given #500 (W,wt=21): 2787 s_t(c1,c3,c2) | s_col(c3,c1,c63(c1,c3,c2)). [resolve(1542,b,254,a)].
% 92.92/13.52
% 92.92/13.52 % given #1000 (T,wt=21): 8648 c2 = c1 | c3 = c2 | -perpAt(c4,c1,A,c4,c2) | s_r(c2,A,c3). [resolve(8461,c,492,b)].
% 92.92/13.52
% 92.92/13.52 % given #1500 (T,wt=19): 11364 c4 = c2 | -s_t(c4,c2,c4) | c2 = c1 | sameside(c1,c2,c4). [resolve(361,c,353,a)].
% 92.92/13.52
% 92.92/13.52 % given #2000 (W,wt=24): 9888 c3 = c2 | c4 = c3 | c2 = c1 | -perpAt(c3,c1,A,c2,c4) | s_r(c4,A,c1). [resolve(9837,d,451,b)].
% 92.92/13.52
% 92.92/13.52 % given #2500 (T,wt=24): 10641 c4 = c1 | c4 = c3 | c2 = c1 | -perpAt(c4,c3,A,c2,c1) | s_r(c2,A,c3). [resolve(10625,c,541,b)].
% 92.92/13.52
% 92.92/13.52 % SZS status Theorem for theBenchmark
% 92.92/13.52
% 92.92/13.52 % Proof 1 at 3.80 (+ 0.70) seconds.
% 92.92/13.52 % Length of proof is 33.
% 92.92/13.52 % Level of proof is 7.
% 92.92/13.52 % Maximum clause weight is 220.000.
% 92.92/13.52 % Given clauses 2871.
% 92.92/13.52
% 92.92/13.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------