%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GEO523+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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:02 AM UTC 2026
% Result : Theorem 53.02s 15.70s
% Output : CNFRefutation 53.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 13
% Syntax : Number of formulae : 61 ( 25 unt; 0 def)
% Number of atoms : 136 ( 73 equ)
% Maximal formula atoms : 15 ( 2 avg)
% Number of connectives : 125 ( 50 ~; 65 |; 10 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-4 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-3 aty)
% Number of variables : 103 ( 3 sgn 43 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(aSatz3_1,axiom,
! [Xa,Xb] : s_t(Xa,Xb,Xb),
file('theBenchmark.p',aSatz3_1) ).
fof(aSatz3_4,axiom,
! [Xa,Xb,Xc] :
( Xa = Xb
| ~ s_t(Xb,Xa,Xc)
| ~ s_t(Xa,Xb,Xc) ),
file('theBenchmark.p',aSatz3_4) ).
fof(aSatz4_12b,axiom,
! [Xa,Xb] : s_col(Xa,Xb,Xa),
file('theBenchmark.p',aSatz4_12b) ).
fof(aSatz6_4b,axiom,
! [Xa,Xp,Xb] :
( s_t(Xa,Xp,Xb)
| ~ s_col(Xa,Xp,Xb)
| sameside(Xa,Xp,Xb) ),
file('theBenchmark.p',aSatz6_4b) ).
fof(aSatz7_2,axiom,
! [Xa,Xm,Xb] :
( s_m(Xb,Xm,Xa)
| ~ s_m(Xa,Xm,Xb) ),
file('theBenchmark.p',aSatz7_2) ).
fof(aSatz7_6,axiom,
! [Xp,Xa,Xq] :
( Xq = s(Xa,Xp)
| ~ s_m(Xp,Xa,Xq) ),
file('theBenchmark.p',aSatz7_6) ).
fof(aSatz7_18,axiom,
! [Xa,Xp,Xb] :
( Xa = Xb
| s(Xa,Xp) != s(Xb,Xp) ),
file('theBenchmark.p',aSatz7_18) ).
fof(aSatz8_22,axiom,
! [Xa,Xb] : s_m(Xa,midpoint(Xa,Xb),Xb),
file('theBenchmark.p',aSatz8_22) ).
fof(aExtPerp4,axiom,
! [Xa,Xb,Xp,Xq] :
( perp(Xa,Xb,Xq,Xp)
| ~ perp(Xa,Xb,Xp,Xq) ),
file('theBenchmark.p',aExtPerp4) ).
fof(aSatz10_2a,axiom,
! [Xa,Xb,Xp] :
( ( perp(Xa,Xb,Xp,reflect(Xa,Xb,Xp))
| Xp = reflect(Xa,Xb,Xp)
| Xa = Xb )
& ( s_col(Xa,Xb,midpoint(Xp,reflect(Xa,Xb,Xp)))
| Xa = Xb ) ),
file('theBenchmark.p',aSatz10_2a) ).
fof(aSatz10_2b,axiom,
! [Xa,Xb,Xp,Xp1] :
( ( Xp1 = reflect(Xa,Xb,Xp)
| Xp != Xp1
| ~ s_col(Xa,Xb,midpoint(Xp,Xp1))
| Xa = Xb )
& ( Xp1 = reflect(Xa,Xb,Xp)
| ~ perp(Xa,Xb,Xp,Xp1)
| ~ s_col(Xa,Xb,midpoint(Xp,Xp1))
| Xa = Xb ) ),
file('theBenchmark.p',aSatz10_2b) ).
fof(d_Defn6_1,axiom,
! [Xa,Xp,Xb] :
( ( sameside(Xa,Xp,Xb)
| Xb = Xp
| Xa = Xp
| ~ s_t(Xp,Xb,Xa) )
& ( sameside(Xa,Xp,Xb)
| xb = Xp
| Xa = Xp
| ~ s_t(Xp,Xa,Xb) )
& ( s_t(Xp,Xb,Xa)
| s_t(Xp,Xa,Xb)
| ~ sameside(Xa,Xp,Xb) )
& ( Xb != Xp
| ~ sameside(Xa,Xp,Xb) )
& ( Xa != Xp
| ~ sameside(Xa,Xp,Xb) ) ),
file('theBenchmark.p',d_Defn6_1) ).
fof(aSatz10_4,conjecture,
! [Xa,Xb,Xp,Xp1] :
( reflect(Xa,Xb,Xp1) = Xp
| reflect(Xa,Xb,Xp) != Xp1
| Xa = Xb ),
file('theBenchmark.p',aSatz10_4) ).
fof(aSatz10_4_neg,negated_conjecture,
~ ! [Xa,Xb,Xp,Xp1] :
( reflect(Xa,Xb,Xp1) = Xp
| reflect(Xa,Xb,Xp) != Xp1
| Xa = Xb ),
inference(assume_negation,[status(cth)],[aSatz10_4]) ).
cnf(c_293,plain,
( C != B
| ~ sameside(A,B,C) ),
inference(clausify,[status(thm)],[d_Defn6_1]) ).
cnf(c_346,plain,
s_t(A,B,B),
inference(clausify,[status(thm)],[aSatz3_1]) ).
cnf(c_349,plain,
( B = A
| ~ s_t(B,A,C)
| ~ s_t(A,B,C) ),
inference(clausify,[status(thm)],[aSatz3_4]) ).
cnf(c_363,plain,
s_col(A,B,A),
inference(clausify,[status(thm)],[aSatz4_12b]) ).
cnf(c_385,plain,
( s_t(A,B,C)
| ~ s_col(A,B,C)
| sameside(A,B,C) ),
inference(clausify,[status(thm)],[aSatz6_4b]) ).
cnf(c_400,plain,
( s_m(C,B,A)
| ~ s_m(A,B,C) ),
inference(clausify,[status(thm)],[aSatz7_2]) ).
cnf(c_405,plain,
( s(B,A) = C
| ~ s_m(A,B,C) ),
inference(clausify,[status(thm)],[aSatz7_6]) ).
cnf(c_417,plain,
( A = C
| s(A,B) != s(C,B) ),
inference(clausify,[status(thm)],[aSatz7_18]) ).
cnf(c_443,plain,
s_m(A,midpoint(A,B),B),
inference(clausify,[status(thm)],[aSatz8_22]) ).
cnf(c_449,plain,
( perp(A,B,D,C)
| ~ perp(A,B,C,D) ),
inference(clausify,[status(thm)],[aExtPerp4]) ).
cnf(c_475,plain,
( s_col(B,A,midpoint(C,reflect(B,A,C)))
| A = B ),
inference(clausify,[status(thm)],[aSatz10_2a]) ).
cnf(c_476,plain,
( perp(B,A,C,reflect(B,A,C))
| reflect(B,A,C) = C
| A = B ),
inference(clausify,[status(thm)],[aSatz10_2a]) ).
cnf(c_477,plain,
( reflect(B,A,C) = D
| ~ perp(B,A,C,D)
| ~ s_col(B,A,midpoint(C,D))
| A = B ),
inference(clausify,[status(thm)],[aSatz10_2b]) ).
cnf(c_478,plain,
( reflect(B,A,C) = D
| D != C
| ~ s_col(B,A,midpoint(C,D))
| A = B ),
inference(clausify,[status(thm)],[aSatz10_2b]) ).
fof(nnf_197,plain,
? [Xa,Xb,Xp,Xp1] :
( reflect(Xa,Xb,Xp1) != Xp
& reflect(Xa,Xb,Xp) = Xp1
& Xb != Xa ),
inference(fof_nnf,[status(thm)],[aSatz10_4_neg]) ).
fof(sk_aSatz10_4_neg,plain,
( reflect(sK1,sK0,sK3) != sK2
& reflect(sK1,sK0,sK2) = sK3
& sK0 != sK1 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3]),skolemize(Xa,sK1),skolemize(Xb,sK0),skolemize(Xp,sK2),skolemize(Xp1,sK3)],[nnf_197]) ).
cnf(c_488,negated_conjecture,
sK0 != sK1,
inference(split_conjunct,[status(thm)],[sk_aSatz10_4_neg]) ).
cnf(c_489,negated_conjecture,
reflect(sK1,sK0,sK2) = sK3,
inference(split_conjunct,[status(thm)],[sk_aSatz10_4_neg]) ).
cnf(c_490,negated_conjecture,
sK3 = reflect(sK1,sK0,sK2),
inference(copy,[status(thm)],[c_489]) ).
cnf(c_491,negated_conjecture,
reflect(sK1,sK0,sK3) != sK2,
inference(split_conjunct,[status(thm)],[sk_aSatz10_4_neg]) ).
cnf(c_4687,plain,
( s_t(A,B,A)
| sameside(A,B,A) ),
inference(resolve,[status(thm)],[c_385,c_363]) ).
cnf(c_14319,plain,
s(midpoint(A,B),A) = B,
inference(resolve,[status(thm)],[c_443,c_405]) ).
cnf(c_14322,plain,
s_m(A,midpoint(B,A),B),
inference(resolve,[status(thm)],[c_443,c_400]) ).
cnf(c_14477,plain,
s(midpoint(A,B),B) = A,
inference(resolve,[status(thm)],[c_14322,c_405]) ).
cnf(c_15584,plain,
midpoint(A,s(B,A)) = B,
inference(resolve,[status(thm)],[c_14319,c_417]) ).
cnf(c_15762,plain,
midpoint(A,B) = midpoint(B,A),
inference(paramod,[status(thm)],[c_14477,c_15584]) ).
cnf(c_15800,plain,
( A != B
| s_t(A,B,A) ),
inference(resolve,[status(thm)],[c_4687,c_293]) ).
cnf(c_15892,plain,
s_t(sK3,reflect(sK1,sK0,sK2),sK3),
inference(resolve,[status(thm)],[c_15800,c_490]) ).
cnf(c_17247,plain,
( sK3 = reflect(sK1,sK0,sK2)
| ~ s_t(reflect(sK1,sK0,sK2),sK3,sK3) ),
inference(resolve,[status(thm)],[c_15892,c_349]) ).
cnf(c_17248,plain,
( reflect(sK1,sK0,sK2) = sK3
| ~ s_t(reflect(sK1,sK0,sK2),sK3,sK3) ),
inference(copy,[status(thm)],[c_17247]) ).
cnf(c_16162,plain,
reflect(sK1,sK0,sK2) = sK3,
inference(resolve,[status(thm)],[c_346,c_17248]) ).
cnf(c_17249,plain,
( s_col(sK1,sK0,midpoint(sK2,sK3))
| sK0 = sK1 ),
inference(paramod,[status(thm)],[c_16162,c_475]) ).
cnf(c_16487,negated_conjecture,
s_col(sK1,sK0,midpoint(sK2,sK3)),
inference(resolve,[status(thm)],[c_488,c_17249]) ).
cnf(c_17250,plain,
( perp(sK1,sK0,sK2,sK3)
| reflect(sK1,sK0,sK2) = sK2
| sK0 = sK1 ),
inference(paramod,[status(thm)],[c_16162,c_476]) ).
cnf(c_16502,negated_conjecture,
( perp(sK1,sK0,sK2,sK3)
| reflect(sK1,sK0,sK2) = sK2 ),
inference(resolve,[status(thm)],[c_488,c_17250]) ).
cnf(c_16600,plain,
s_col(sK1,sK0,midpoint(sK3,sK2)),
inference(paramod,[status(thm)],[c_15762,c_16487]) ).
cnf(c_17251,plain,
( reflect(sK1,sK0,sK3) = sK2
| sK2 != sK3
| sK0 = sK1 ),
inference(resolve,[status(thm)],[c_16600,c_478]) ).
cnf(c_17252,plain,
( reflect(sK1,sK0,sK3) = sK2
| sK3 != sK2
| sK0 = sK1 ),
inference(copy,[status(thm)],[c_17251]) ).
cnf(c_17253,negated_conjecture,
( reflect(sK1,sK0,sK3) = sK2
| sK3 != sK2 ),
inference(resolve,[status(thm)],[c_488,c_17252]) ).
cnf(c_16815,negated_conjecture,
sK3 != sK2,
inference(resolve,[status(thm)],[c_491,c_17253]) ).
cnf(c_16951,plain,
reflect(sK1,sK0,sK2) != sK2,
inference(paramod,[status(thm)],[c_490,c_16815]) ).
cnf(c_16960,negated_conjecture,
perp(sK1,sK0,sK2,sK3),
inference(resolve,[status(thm)],[c_16951,c_16502]) ).
cnf(c_17216,plain,
perp(sK1,sK0,sK3,sK2),
inference(resolve,[status(thm)],[c_16960,c_449]) ).
cnf(c_17254,plain,
( reflect(sK1,sK0,sK3) = sK2
| ~ s_col(sK1,sK0,midpoint(sK3,sK2))
| sK0 = sK1 ),
inference(resolve,[status(thm)],[c_17216,c_477]) ).
cnf(c_17255,negated_conjecture,
( reflect(sK1,sK0,sK3) = sK2
| ~ s_col(sK1,sK0,midpoint(sK3,sK2)) ),
inference(resolve,[status(thm)],[c_488,c_17254]) ).
cnf(c_17256,negated_conjecture,
reflect(sK1,sK0,sK3) = sK2,
inference(resolve,[status(thm)],[c_16600,c_17255]) ).
cnf(c_17246,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_491,c_17256]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO523+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.41 % Computer : n011.cluster.edu
% 0.08/0.41 % Model : x86_64 x86_64
% 0.08/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.41 % Memory : 8046.5625MB
% 0.08/0.41 % OS : Linux 6.8.0-71-generic
% 0.08/0.41 % CPULimit : 300
% 0.08/0.41 % WCLimit : 300
% 0.08/0.41 % DateTime : Fri Sep 25 13:38:58 UTC 2026
% 0.08/0.41 % CPUTime :
% 0.08/0.41 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.41 % Process 2129172 was started by sandbox on n011,
% 0.08/0.41 % Fri Sep 25 13:38:58 2026
% 0.08/0.41 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.12/0.45
% 0.12/0.45 % From the command line: assign(max_seconds, 300).
% 0.12/0.45
% 0.12/0.45 % SInE: 152 to sos, 48 to usable, of 200 axioms (tolerance 2.00, depth 0 fixpoint).
% 53.02/15.70
% 53.02/15.70 % SZS status Theorem for theBenchmark
% 53.02/15.70
% 53.02/15.70 % Proof 1 at 2.76 (+ 0.60) seconds.
% 53.02/15.70 % Length of proof is 48.
% 53.02/15.70 % Level of proof is 12.
% 53.02/15.70 % Maximum clause weight is 212.000.
% 53.02/15.70 % Given clauses 493.
% 53.02/15.70
% 53.02/15.70 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------