%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GEO524+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n012.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 : Fri Sep 25 01:18:05 PM UTC 2026
% Result : Theorem 52.78s 7.26s
% Output : Proof 52.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 20
% Syntax : Number of formulae : 115 ( 54 unt; 0 def)
% Number of atoms : 520 ( 182 equ)
% Maximal formula atoms : 34 ( 4 avg)
% Number of connectives : 737 ( 332 ~; 278 |; 127 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-5 aty)
% Number of functors : 24 ( 24 usr; 10 con; 0-5 aty)
% Number of variables : 273 ( 25 sgn 146 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f188,conjecture,
! [Xa,Xb,Xp,Xq] :
( Xp = Xq
| reflect(Xa,Xb,Xp) != reflect(Xa,Xb,Xq)
| Xa = Xb ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz10_7) ).
fof(f188_neg,negated_conjecture,
~ ! [Xa,Xb,Xp,Xq] :
( Xp = Xq
| reflect(Xa,Xb,Xp) != reflect(Xa,Xb,Xq)
| Xa = Xb ),
inference(negated_conjecture,[status(cth)],[f188]) ).
fof(f188_nnf,plain,
? [Xa,Xb,Xp,Xq] :
( Xp != Xq
& reflect(Xa,Xb,Xp) = reflect(Xa,Xb,Xq)
& Xa != Xb ),
inference(nnf_transformation,[status(thm)],[f188_neg]) ).
fof(f188_sk,plain,
( sk2 != sk3
& reflect(sk0,sk1,sk2) = reflect(sk0,sk1,sk3)
& sk0 != sk1 ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2,sk3])],[f188_nnf]) ).
cnf(c221,plain,
sk2 != sk3,
inference(cnf_transformation,[status(esa)],[f188_sk]) ).
cnf(t4,plain,
eq(sk2,sk3) = false,
inference(equality_encoding,[status(esa)],[c221]) ).
cnf(t372,plain,
eq(sk2,sk3) = false,
inference(orient,[status(thm)],[t4]) ).
cnf(t74,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
introduced(definition) ).
cnf(t143,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
inference(orient,[status(thm)],[t74]) ).
fof(f186,axiom,
! [Xa,Xb,Xp] :
( reflect(Xa,Xb,reflect(Xa,Xb,Xp)) = Xp
| Xa = Xb ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz10_5) ).
fof(f186_nnf,plain,
! [Xa,Xb,Xp] :
( reflect(Xa,Xb,reflect(Xa,Xb,Xp)) = Xp
| Xa = Xb ),
inference(nnf_transformation,[status(thm)],[f186]) ).
fof(f186_sk,plain,
! [Xa,Xb,Xp] :
( reflect(Xa,Xb,reflect(Xa,Xb,Xp)) = Xp
| Xa = Xb ),
inference(skolemisation,[status(esa)],[f186_nnf]) ).
cnf(c217,plain,
( reflect(X0,X1,reflect(X0,X1,X2)) = X2
| X0 = X1 ),
inference(cnf_transformation,[status(esa)],[f186_sk]) ).
cnf(t124,plain,
or(eq(X1,X2),eq(reflect(X1,X2,reflect(X1,X2,X3)),X3)) = true,
inference(equality_encoding,[status(esa)],[c217]) ).
cnf(t151,plain,
or(eq(X1,X2),eq(reflect(X1,X2,reflect(X1,X2,X3)),X3)) = true,
inference(orient,[status(thm)],[t124]) ).
cnf(c219,plain,
sk0 != sk1,
inference(cnf_transformation,[status(esa)],[f188_sk]) ).
cnf(t3,plain,
eq(sk0,sk1) = false,
inference(equality_encoding,[status(esa)],[c219]) ).
cnf(t363,plain,
eq(sk0,sk1) = false,
inference(orient,[status(thm)],[t3]) ).
cnf(t365,plain,
true = or(false,eq(reflect(sk0,sk1,reflect(sk0,sk1,X1)),X1)),
inference(cp,[status(thm)],[t151,t363]) ).
cnf(t9,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t140,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t9]) ).
cnf(t495,plain,
true = eq(reflect(sk0,sk1,reflect(sk0,sk1,X1)),X1),
inference(step,[status(thm)],[t365,t140]) ).
cnf(t425,plain,
eq(reflect(sk0,sk1,reflect(sk0,sk1,X1)),X1) = true,
inference(orient,[status(thm)],[t495]) ).
cnf(t427,plain,
X1 = ifeq(true,true,reflect(sk0,sk1,reflect(sk0,sk1,X1)),X1),
inference(cp,[status(thm)],[t143,t425]) ).
cnf(t36,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t142,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t36]) ).
cnf(t496,plain,
X1 = reflect(sk0,sk1,reflect(sk0,sk1,X1)),
inference(step,[status(thm)],[t427,t142]) ).
cnf(t430,plain,
reflect(sk0,sk1,reflect(sk0,sk1,X1)) = X1,
inference(orient,[status(thm)],[t496]) ).
cnf(c220,plain,
reflect(sk0,sk1,sk2) = reflect(sk0,sk1,sk3),
inference(cnf_transformation,[status(esa)],[f188_sk]) ).
cnf(t80,plain,
reflect(sk0,sk1,sk3) = reflect(sk0,sk1,sk2),
inference(equality_encoding,[status(esa)],[c220]) ).
cnf(t397,plain,
reflect(sk0,sk1,sk2) = reflect(sk0,sk1,sk3),
inference(orient,[status(thm)],[t80]) ).
cnf(t431,plain,
sk2 = reflect(sk0,sk1,reflect(sk0,sk1,sk3)),
inference(cp,[status(thm)],[t430,t397]) ).
cnf(t499,plain,
sk2 = sk3,
inference(step,[status(thm)],[t431,t430]) ).
cnf(t443,plain,
sk2 = sk3,
inference(orient,[status(thm)],[t499]) ).
cnf(t501,plain,
eq(sk3,sk3) = false,
inference(step,[status(thm)],[t372,t443]) ).
cnf(t2,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t147,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t2]) ).
cnf(t502,plain,
true = false,
inference(step,[status(thm)],[t501,t147]) ).
cnf(t445,plain,
true = false,
inference(rw,[status(thm)],[t502]) ).
cnf(t447,plain,
false = true,
inference(orient,[status(thm)],[t445]) ).
fof(f7,axiom,
( ~ s_t(gamma,alpha,beta)
& ~ s_t(beta,gamma,alpha)
& ~ s_t(alpha,beta,gamma) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aA8) ).
fof(f7_nnf,plain,
( ~ s_t(gamma,alpha,beta)
& ~ s_t(beta,gamma,alpha)
& ~ s_t(alpha,beta,gamma) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
( ~ s_t(gamma,alpha,beta)
& ~ s_t(beta,gamma,alpha)
& ~ s_t(alpha,beta,gamma) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c9,plain,
~ s_t(alpha,beta,gamma),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(c10,plain,
~ s_t(beta,gamma,alpha),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(c11,plain,
~ s_t(gamma,alpha,beta),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
fof(f29,axiom,
alpha != beta,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz3_13a) ).
fof(f29_nnf,plain,
alpha != beta,
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
alpha != beta,
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c33,plain,
alpha != beta,
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
fof(f30,axiom,
beta != gamma,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz3_13b) ).
fof(f30_nnf,plain,
beta != gamma,
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
beta != gamma,
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c34,plain,
beta != gamma,
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
fof(f31,axiom,
alpha != gamma,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz3_13c) ).
fof(f31_nnf,plain,
alpha != gamma,
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
alpha != gamma,
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c35,plain,
alpha != gamma,
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
fof(f33,axiom,
! [Xb,Xa] : Xb != ext(Xa,Xb,alpha,gamma),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz3_14b) ).
fof(f33_nnf,plain,
! [Xb,Xa] : Xb != ext(Xa,Xb,alpha,gamma),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
! [Xb,Xa] : Xb != ext(Xa,Xb,alpha,gamma),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c37,plain,
X0 != ext(X1,X0,alpha,gamma),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
fof(f69,axiom,
! [Xa,Xp,Xb] :
( ( s_t(Xb,Xp,c63(Xa,Xp,Xb))
| ~ sameside(Xa,Xp,Xb) )
& ( s_t(Xa,Xp,c63(Xa,Xp,Xb))
| ~ sameside(Xa,Xp,Xb) )
& ( c63(Xa,Xp,Xb) != Xp
| ~ sameside(Xa,Xp,Xb) )
& ( Xb != Xp
| ~ sameside(Xa,Xp,Xb) )
& ( Xa != Xp
| ~ sameside(Xa,Xp,Xb) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz6_3a) ).
fof(f69_nnf,plain,
! [Xa,Xp,Xb] :
( ( s_t(Xb,Xp,c63(Xa,Xp,Xb))
| ~ sameside(Xa,Xp,Xb) )
& ( s_t(Xa,Xp,c63(Xa,Xp,Xb))
| ~ sameside(Xa,Xp,Xb) )
& ( c63(Xa,Xp,Xb) != Xp
| ~ sameside(Xa,Xp,Xb) )
& ( Xb != Xp
| ~ sameside(Xa,Xp,Xb) )
& ( Xa != Xp
| ~ sameside(Xa,Xp,Xb) ) ),
inference(nnf_transformation,[status(thm)],[f69]) ).
fof(f69_sk,plain,
! [Xa,Xp,Xb] :
( ( s_t(Xb,Xp,c63(Xa,Xp,Xb))
| ~ sameside(Xa,Xp,Xb) )
& ( s_t(Xa,Xp,c63(Xa,Xp,Xb))
| ~ sameside(Xa,Xp,Xb) )
& ( c63(Xa,Xp,Xb) != Xp
| ~ sameside(Xa,Xp,Xb) )
& ( Xb != Xp
| ~ sameside(Xa,Xp,Xb) )
& ( Xa != Xp
| ~ sameside(Xa,Xp,Xb) ) ),
inference(skolemisation,[status(esa)],[f69_nnf]) ).
cnf(c77,plain,
( X0 != X1
| ~ sameside(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f69_sk]) ).
cnf(c78,plain,
( X2 != X1
| ~ sameside(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f69_sk]) ).
cnf(c79,plain,
( c63(X0,X1,X2) != X1
| ~ sameside(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f69_sk]) ).
fof(f71,axiom,
! [Xa,Xp,Xb] :
( ( ~ s_t(Xa,Xp,Xb)
| ~ sameside(Xa,Xp,Xb) )
& ( s_col(Xa,Xp,Xb)
| ~ sameside(Xa,Xp,Xb) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz6_4a) ).
fof(f71_nnf,plain,
! [Xa,Xp,Xb] :
( ( ~ s_t(Xa,Xp,Xb)
| ~ sameside(Xa,Xp,Xb) )
& ( s_col(Xa,Xp,Xb)
| ~ sameside(Xa,Xp,Xb) ) ),
inference(nnf_transformation,[status(thm)],[f71]) ).
fof(f71_sk,plain,
! [Xa,Xp,Xb] :
( ( ~ s_t(Xa,Xp,Xb)
| ~ sameside(Xa,Xp,Xb) )
& ( s_col(Xa,Xp,Xb)
| ~ sameside(Xa,Xp,Xb) ) ),
inference(skolemisation,[status(esa)],[f71_nnf]) ).
cnf(c84,plain,
( ~ s_t(X0,X1,X2)
| ~ sameside(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f71_sk]) ).
fof(f128,axiom,
! [Xa,Xb,Xc,Xp,Xq] :
( ( s_r(f813(Xa,Xb,Xp,Xq,Xc),Xc,g813(Xa,Xb,Xp,Xq,Xc))
| ~ perpAt(Xa,Xb,Xc,Xp,Xq) )
& ( Xc != g813(Xa,Xb,Xp,Xq,Xc)
| ~ perpAt(Xa,Xb,Xc,Xp,Xq) )
& ( Xc != f813(Xa,Xb,Xp,Xq,Xc)
| ~ perpAt(Xa,Xb,Xc,Xp,Xq) )
& ( s_col(Xp,Xq,g813(Xa,Xb,Xp,Xq,Xc))
| ~ perpAt(Xa,Xb,Xc,Xp,Xq) )
& ( s_col(Xa,Xb,f813(Xa,Xb,Xp,Xq,Xc))
| ~ perpAt(Xa,Xb,Xc,Xp,Xq) )
& ( s_col(Xa,Xb,Xc)
| ~ perpAt(Xa,Xb,Xc,Xp,Xq) )
& ( s_col(Xp,Xq,Xc)
| ~ perpAt(Xa,Xb,Xc,Xp,Xq) )
& ( Xp != Xq
| ~ perpAt(Xa,Xb,Xc,Xp,Xq) )
& ( Xa != Xb
| ~ perpAt(Xa,Xb,Xc,Xp,Xq) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz8_13a) ).
fof(f128_nnf,plain,
! [Xa,Xb,Xc,Xp,Xq] :
( ( s_r(f813(Xa,Xb,Xp,Xq,Xc),Xc,g813(Xa,Xb,Xp,Xq,Xc))
| ~ perpAt(Xa,Xb,Xc,Xp,Xq) )
& ( Xc != g813(Xa,Xb,Xp,Xq,Xc)
| ~ perpAt(Xa,Xb,Xc,Xp,Xq) )
& ( Xc != f813(Xa,Xb,Xp,Xq,Xc)
| ~ perpAt(Xa,Xb,Xc,Xp,Xq) )
& ( s_col(Xp,Xq,g813(Xa,Xb,Xp,Xq,Xc))
| ~ perpAt(Xa,Xb,Xc,Xp,Xq) )
& ( s_col(Xa,Xb,f813(Xa,Xb,Xp,Xq,Xc))
| ~ perpAt(Xa,Xb,Xc,Xp,Xq) )
& ( s_col(Xa,Xb,Xc)
| ~ perpAt(Xa,Xb,Xc,Xp,Xq) )
& ( s_col(Xp,Xq,Xc)
| ~ perpAt(Xa,Xb,Xc,Xp,Xq) )
& ( Xp != Xq
| ~ perpAt(Xa,Xb,Xc,Xp,Xq) )
& ( Xa != Xb
| ~ perpAt(Xa,Xb,Xc,Xp,Xq) ) ),
inference(nnf_transformation,[status(thm)],[f128]) ).
fof(f128_sk,plain,
! [Xa,Xb,Xc,Xp,Xq] :
( ( s_r(f813(Xa,Xb,Xp,Xq,Xc),Xc,g813(Xa,Xb,Xp,Xq,Xc))
| ~ perpAt(Xa,Xb,Xc,Xp,Xq) )
& ( Xc != g813(Xa,Xb,Xp,Xq,Xc)
| ~ perpAt(Xa,Xb,Xc,Xp,Xq) )
& ( Xc != f813(Xa,Xb,Xp,Xq,Xc)
| ~ perpAt(Xa,Xb,Xc,Xp,Xq) )
& ( s_col(Xp,Xq,g813(Xa,Xb,Xp,Xq,Xc))
| ~ perpAt(Xa,Xb,Xc,Xp,Xq) )
& ( s_col(Xa,Xb,f813(Xa,Xb,Xp,Xq,Xc))
| ~ perpAt(Xa,Xb,Xc,Xp,Xq) )
& ( s_col(Xa,Xb,Xc)
| ~ perpAt(Xa,Xb,Xc,Xp,Xq) )
& ( s_col(Xp,Xq,Xc)
| ~ perpAt(Xa,Xb,Xc,Xp,Xq) )
& ( Xp != Xq
| ~ perpAt(Xa,Xb,Xc,Xp,Xq) )
& ( Xa != Xb
| ~ perpAt(Xa,Xb,Xc,Xp,Xq) ) ),
inference(skolemisation,[status(esa)],[f128_nnf]) ).
cnf(c142,plain,
( X0 != X1
| ~ perpAt(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(esa)],[f128_sk]) ).
cnf(c143,plain,
( X3 != X4
| ~ perpAt(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(esa)],[f128_sk]) ).
cnf(c148,plain,
( X2 != f813(X0,X1,X3,X4,X2)
| ~ perpAt(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(esa)],[f128_sk]) ).
cnf(c149,plain,
( X2 != g813(X0,X1,X3,X4,X2)
| ~ perpAt(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(esa)],[f128_sk]) ).
fof(f130,axiom,
! [Xa,Xb,Xp,Xq] :
( ~ s_col(Xa,Xb,Xq)
| ~ s_col(Xa,Xb,Xp)
| ~ perp(Xa,Xb,Xp,Xq) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz8_14a) ).
fof(f130_nnf,plain,
! [Xa,Xb,Xp,Xq] :
( ~ s_col(Xa,Xb,Xq)
| ~ s_col(Xa,Xb,Xp)
| ~ perp(Xa,Xb,Xp,Xq) ),
inference(nnf_transformation,[status(thm)],[f130]) ).
fof(f130_sk,plain,
! [Xa,Xb,Xp,Xq] :
( ~ s_col(Xa,Xb,Xq)
| ~ s_col(Xa,Xb,Xp)
| ~ perp(Xa,Xb,Xp,Xq) ),
inference(skolemisation,[status(esa)],[f130_nnf]) ).
cnf(c152,plain,
( ~ s_col(X0,X1,X3)
| ~ s_col(X0,X1,X2)
| ~ perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f130_sk]) ).
fof(f170,axiom,
! [Xa,Xp,Xq,Xb] :
( ~ samesideline(Xa,Xb,Xp,Xq)
| ~ opposite(Xa,Xp,Xq,Xb) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz9_9) ).
fof(f170_nnf,plain,
! [Xa,Xp,Xq,Xb] :
( ~ samesideline(Xa,Xb,Xp,Xq)
| ~ opposite(Xa,Xp,Xq,Xb) ),
inference(nnf_transformation,[status(thm)],[f170]) ).
fof(f170_sk,plain,
! [Xa,Xp,Xq,Xb] :
( ~ samesideline(Xa,Xb,Xp,Xq)
| ~ opposite(Xa,Xp,Xq,Xb) ),
inference(skolemisation,[status(esa)],[f170_nnf]) ).
cnf(c199,plain,
( ~ samesideline(X0,X3,X1,X2)
| ~ opposite(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f170_sk]) ).
fof(f196,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('/export/starexec/sandbox/benchmark/theBenchmark.p',d_Defn6_1) ).
fof(f196_nnf,plain,
! [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) ) ),
inference(nnf_transformation,[status(thm)],[f196]) ).
fof(f196_sk,plain,
! [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) ) ),
inference(skolemisation,[status(esa)],[f196_nnf]) ).
cnf(c253,plain,
( X0 != X1
| ~ sameside(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f196_sk]) ).
cnf(c254,plain,
( X2 != X1
| ~ sameside(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f196_sk]) ).
fof(f200,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('/export/starexec/sandbox/benchmark/theBenchmark.p',d_Defn8_11a) ).
fof(f200_nnf,plain,
! [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) ) ),
inference(nnf_transformation,[status(thm)],[f200]) ).
fof(f200_sk,plain,
! [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) ) ),
inference(skolemisation,[status(esa)],[f200_nnf]) ).
cnf(c272,plain,
( X0 != X1
| ~ perpAt(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(esa)],[f200_sk]) ).
cnf(c273,plain,
( X3 != X4
| ~ perpAt(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[status(esa)],[f200_sk]) ).
fof(f202,axiom,
! [Xp,Xq,Xa,Xb,Xt] :
( ( s_col(Xp,Xq,il(Xa,Xb,Xp,Xq))
| ~ opposite(Xa,Xp,Xq,Xb) )
& ( s_t(Xa,il(Xa,Xb,Xp,Xq),Xb)
| ~ opposite(Xa,Xp,Xq,Xb) )
& ( ~ s_col(Xp,Xq,Xb)
| ~ opposite(Xa,Xp,Xq,Xb) )
& ( ~ s_col(Xp,Xq,Xa)
| ~ opposite(Xa,Xp,Xq,Xb) )
& ( opposite(Xa,Xp,Xq,Xb)
| ~ s_col(Xp,Xq,Xt)
| ~ s_t(Xa,Xt,Xb)
| s_col(Xp,Xq,Xb)
| s_col(Xp,Xq,Xa)
| Xp = Xq ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d_Defn9_1) ).
fof(f202_nnf,plain,
! [Xp,Xq,Xa,Xb,Xt] :
( ( s_col(Xp,Xq,il(Xa,Xb,Xp,Xq))
| ~ opposite(Xa,Xp,Xq,Xb) )
& ( s_t(Xa,il(Xa,Xb,Xp,Xq),Xb)
| ~ opposite(Xa,Xp,Xq,Xb) )
& ( ~ s_col(Xp,Xq,Xb)
| ~ opposite(Xa,Xp,Xq,Xb) )
& ( ~ s_col(Xp,Xq,Xa)
| ~ opposite(Xa,Xp,Xq,Xb) )
& ( opposite(Xa,Xp,Xq,Xb)
| ~ s_col(Xp,Xq,Xt)
| ~ s_t(Xa,Xt,Xb)
| s_col(Xp,Xq,Xb)
| s_col(Xp,Xq,Xa)
| Xp = Xq ) ),
inference(nnf_transformation,[status(thm)],[f202]) ).
fof(f202_sk,plain,
! [Xp,Xq,Xa,Xb,Xt] :
( ( s_col(Xp,Xq,il(Xa,Xb,Xp,Xq))
| ~ opposite(Xa,Xp,Xq,Xb) )
& ( s_t(Xa,il(Xa,Xb,Xp,Xq),Xb)
| ~ opposite(Xa,Xp,Xq,Xb) )
& ( ~ s_col(Xp,Xq,Xb)
| ~ opposite(Xa,Xp,Xq,Xb) )
& ( ~ s_col(Xp,Xq,Xa)
| ~ opposite(Xa,Xp,Xq,Xb) )
& ( opposite(Xa,Xp,Xq,Xb)
| ~ s_col(Xp,Xq,Xt)
| ~ s_t(Xa,Xt,Xb)
| s_col(Xp,Xq,Xb)
| s_col(Xp,Xq,Xa)
| Xp = Xq ) ),
inference(skolemisation,[status(esa)],[f202_nnf]) ).
cnf(c281,plain,
( ~ s_col(X0,X1,X2)
| ~ opposite(X2,X0,X1,X3) ),
inference(cnf_transformation,[status(esa)],[f202_sk]) ).
cnf(c282,plain,
( ~ s_col(X0,X1,X3)
| ~ opposite(X2,X0,X1,X3) ),
inference(cnf_transformation,[status(esa)],[f202_sk]) ).
fof(f203,axiom,
! [Xa,Xb,Xp,Xq,Xu,Xc,Xv] :
( ( samesideline(Xa,Xb,Xp,Xq)
| s_col(Xp,Xq,Xb)
| s_col(Xp,Xq,Xa)
| Xb = Xv
| Xa = Xu
| Xc = Xv
| Xc = Xu
| Xp = Xq
| ~ s_col(Xp,Xq,Xv)
| ~ s_col(Xp,Xq,Xu)
| ~ s_t(Xb,Xv,Xc)
| ~ s_t(Xa,Xu,Xc) )
& ( ~ s_col(Xp,Xq,Xb)
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( ~ s_col(Xp,Xq,Xa)
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( Xp != Xq
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( ss3(Xa,Xb,Xp,Xq) != ss2(Xa,Xb,Xp,Xq)
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( ss3(Xa,Xb,Xp,Xq) != ss1(Xa,Xb,Xp,Xq)
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( Xb != ss2(Xa,Xb,Xp,Xq)
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( Xa != ss1(Xa,Xb,Xp,Xq)
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( s_t(Xb,ss2(Xa,Xb,Xp,Xq),ss3(Xa,Xb,Xp,Xq))
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( s_t(Xa,ss1(Xa,Xb,Xp,Xq),ss3(Xa,Xb,Xp,Xq))
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( s_col(Xp,Xq,ss2(Xa,Xb,Xp,Xq))
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( s_col(Xp,Xq,ss1(Xa,Xb,Xp,Xq))
| ~ samesideline(Xa,Xb,Xp,Xq) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d_Defn9_7) ).
fof(f203_nnf,plain,
! [Xa,Xb,Xp,Xq,Xu,Xc,Xv] :
( ( samesideline(Xa,Xb,Xp,Xq)
| s_col(Xp,Xq,Xb)
| s_col(Xp,Xq,Xa)
| Xb = Xv
| Xa = Xu
| Xc = Xv
| Xc = Xu
| Xp = Xq
| ~ s_col(Xp,Xq,Xv)
| ~ s_col(Xp,Xq,Xu)
| ~ s_t(Xb,Xv,Xc)
| ~ s_t(Xa,Xu,Xc) )
& ( ~ s_col(Xp,Xq,Xb)
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( ~ s_col(Xp,Xq,Xa)
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( Xp != Xq
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( ss3(Xa,Xb,Xp,Xq) != ss2(Xa,Xb,Xp,Xq)
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( ss3(Xa,Xb,Xp,Xq) != ss1(Xa,Xb,Xp,Xq)
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( Xb != ss2(Xa,Xb,Xp,Xq)
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( Xa != ss1(Xa,Xb,Xp,Xq)
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( s_t(Xb,ss2(Xa,Xb,Xp,Xq),ss3(Xa,Xb,Xp,Xq))
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( s_t(Xa,ss1(Xa,Xb,Xp,Xq),ss3(Xa,Xb,Xp,Xq))
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( s_col(Xp,Xq,ss2(Xa,Xb,Xp,Xq))
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( s_col(Xp,Xq,ss1(Xa,Xb,Xp,Xq))
| ~ samesideline(Xa,Xb,Xp,Xq) ) ),
inference(nnf_transformation,[status(thm)],[f203]) ).
fof(f203_sk,plain,
! [Xa,Xb,Xp,Xq,Xu,Xc,Xv] :
( ( samesideline(Xa,Xb,Xp,Xq)
| s_col(Xp,Xq,Xb)
| s_col(Xp,Xq,Xa)
| Xb = Xv
| Xa = Xu
| Xc = Xv
| Xc = Xu
| Xp = Xq
| ~ s_col(Xp,Xq,Xv)
| ~ s_col(Xp,Xq,Xu)
| ~ s_t(Xb,Xv,Xc)
| ~ s_t(Xa,Xu,Xc) )
& ( ~ s_col(Xp,Xq,Xb)
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( ~ s_col(Xp,Xq,Xa)
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( Xp != Xq
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( ss3(Xa,Xb,Xp,Xq) != ss2(Xa,Xb,Xp,Xq)
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( ss3(Xa,Xb,Xp,Xq) != ss1(Xa,Xb,Xp,Xq)
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( Xb != ss2(Xa,Xb,Xp,Xq)
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( Xa != ss1(Xa,Xb,Xp,Xq)
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( s_t(Xb,ss2(Xa,Xb,Xp,Xq),ss3(Xa,Xb,Xp,Xq))
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( s_t(Xa,ss1(Xa,Xb,Xp,Xq),ss3(Xa,Xb,Xp,Xq))
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( s_col(Xp,Xq,ss2(Xa,Xb,Xp,Xq))
| ~ samesideline(Xa,Xb,Xp,Xq) )
& ( s_col(Xp,Xq,ss1(Xa,Xb,Xp,Xq))
| ~ samesideline(Xa,Xb,Xp,Xq) ) ),
inference(skolemisation,[status(esa)],[f203_nnf]) ).
cnf(c289,plain,
( X0 != ss1(X0,X1,X2,X3)
| ~ samesideline(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f203_sk]) ).
cnf(c290,plain,
( X1 != ss2(X0,X1,X2,X3)
| ~ samesideline(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f203_sk]) ).
cnf(c291,plain,
( ss3(X0,X1,X2,X3) != ss1(X0,X1,X2,X3)
| ~ samesideline(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f203_sk]) ).
cnf(c292,plain,
( ss3(X0,X1,X2,X3) != ss2(X0,X1,X2,X3)
| ~ samesideline(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f203_sk]) ).
cnf(c293,plain,
( X2 != X3
| ~ samesideline(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f203_sk]) ).
cnf(c294,plain,
( ~ s_col(X2,X3,X0)
| ~ samesideline(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f203_sk]) ).
cnf(c295,plain,
( ~ s_col(X2,X3,X1)
| ~ samesideline(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f203_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c9,c10,c11,c33,c34,c35,c37,c77,c78,c79,c84,c142,c143,c148,c149,c152,c199,c219,c221,c253,c254,c272,c273,c281,c282,c289,c290,c291,c292,c293,c294,c295]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t447]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GEO524+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.02 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Wed Sep 23 12:18:05 UTC 2026
% 0.03/0.29 % CPUTime :
% 0.03/0.29 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 52.78/7.26 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 52.78/7.26 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------