%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GEO500+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/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:03 PM UTC 2026
% Result : Theorem 77.88s 10.16s
% Output : Proof 77.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 28
% Syntax : Number of formulae : 206 ( 151 unt; 0 def)
% Number of atoms : 353 ( 199 equ)
% Maximal formula atoms : 15 ( 1 avg)
% Number of connectives : 292 ( 145 ~; 106 |; 41 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-4 aty)
% Number of functors : 16 ( 16 usr; 9 con; 0-4 aty)
% Number of variables : 364 ( 10 sgn 147 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(t48,plain,
ifeq(not(X1),true,X1,false) = false,
introduced(definition) ).
cnf(t1927,plain,
ifeq(not(X1),true,X1,false) = false,
inference(orient,[status(thm)],[t48]) ).
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/sandbox2/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]) ).
cnf(t120,plain,
or(not(sameside(X1,X2,X3)),not(s_t(X1,X2,X3))) = true,
inference(equality_encoding,[status(esa)],[c84]) ).
cnf(t1675,plain,
or(not(sameside(X1,X2,X3)),not(s_t(X1,X2,X3))) = true,
inference(orient,[status(thm)],[t120]) ).
cnf(t57,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
introduced(definition) ).
cnf(t263,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
inference(orient,[status(thm)],[t57]) ).
fof(f73,axiom,
! [Xa,Xp] :
( sameside(Xa,Xp,Xa)
| Xa = Xp ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz6_5) ).
fof(f73_nnf,plain,
! [Xa,Xp] :
( sameside(Xa,Xp,Xa)
| Xa = Xp ),
inference(nnf_transformation,[status(thm)],[f73]) ).
fof(f73_sk,plain,
! [Xa,Xp] :
( sameside(Xa,Xp,Xa)
| Xa = Xp ),
inference(skolemisation,[status(esa)],[f73_nnf]) ).
cnf(c86,plain,
( sameside(X0,X1,X0)
| X0 = X1 ),
inference(cnf_transformation,[status(esa)],[f73_sk]) ).
cnf(t102,plain,
or(eq(X1,X2),eq(sameside(X1,X2,X1),true)) = true,
inference(equality_encoding,[status(esa)],[c86]) ).
cnf(t1659,plain,
or(eq(X1,X2),eq(sameside(X1,X2,X1),true)) = true,
inference(orient,[status(thm)],[t102]) ).
fof(f110,conjecture,
! [Xa,Xb,Xp] :
( Xa = Xb
| s(Xa,s(Xb,Xp)) != s(Xb,s(Xa,Xp)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz7_19) ).
fof(f110_neg,negated_conjecture,
~ ! [Xa,Xb,Xp] :
( Xa = Xb
| s(Xa,s(Xb,Xp)) != s(Xb,s(Xa,Xp)) ),
inference(negated_conjecture,[status(cth)],[f110]) ).
fof(f110_nnf,plain,
? [Xa,Xb,Xp] :
( Xa != Xb
& s(Xa,s(Xb,Xp)) = s(Xb,s(Xa,Xp)) ),
inference(nnf_transformation,[status(thm)],[f110_neg]) ).
fof(f110_sk,plain,
( sk0 != sk1
& s(sk0,s(sk1,sk2)) = s(sk1,s(sk0,sk2)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2])],[f110_nnf]) ).
cnf(c125,plain,
sk0 != sk1,
inference(cnf_transformation,[status(esa)],[f110_sk]) ).
cnf(t6,plain,
eq(sk0,sk1) = false,
inference(equality_encoding,[status(esa)],[c125]) ).
cnf(t2469,plain,
eq(sk0,sk1) = false,
inference(orient,[status(thm)],[t6]) ).
cnf(t2471,plain,
true = or(false,eq(sameside(sk0,sk1,sk0),true)),
inference(cp,[status(thm)],[t1659,t2469]) ).
cnf(t9,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t283,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t9]) ).
cnf(t30839,plain,
true = eq(sameside(sk0,sk1,sk0),true),
inference(step,[status(thm)],[t2471,t283]) ).
cnf(t3067,plain,
eq(sameside(sk0,sk1,sk0),true) = true,
inference(orient,[status(thm)],[t30839]) ).
cnf(t3068,plain,
true = ifeq(true,true,sameside(sk0,sk1,sk0),true),
inference(cp,[status(thm)],[t263,t3067]) ).
cnf(t26,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t26]) ).
cnf(t30840,plain,
true = sameside(sk0,sk1,sk0),
inference(step,[status(thm)],[t3068,t256]) ).
cnf(t3077,plain,
sameside(sk0,sk1,sk0) = true,
inference(orient,[status(thm)],[t30840]) ).
cnf(t3078,plain,
true = or(not(true),not(s_t(sk0,sk1,sk0))),
inference(cp,[status(thm)],[t1675,t3077]) ).
cnf(t1,plain,
not(true) = false,
introduced(definition) ).
cnf(t2545,plain,
not(true) = false,
inference(orient,[status(thm)],[t1]) ).
cnf(t30841,plain,
true = or(false,not(s_t(sk0,sk1,sk0))),
inference(step,[status(thm)],[t3078,t2545]) ).
cnf(t30842,plain,
true = not(s_t(sk0,sk1,sk0)),
inference(step,[status(thm)],[t30841,t283]) ).
cnf(t3092,plain,
not(s_t(sk0,sk1,sk0)) = true,
inference(orient,[status(thm)],[t30842]) ).
cnf(t3093,plain,
false = ifeq(true,true,s_t(sk0,sk1,sk0),false),
inference(cp,[status(thm)],[t1927,t3092]) ).
cnf(t30843,plain,
false = s_t(sk0,sk1,sk0),
inference(step,[status(thm)],[t3093,t256]) ).
cnf(t3094,plain,
s_t(sk0,sk1,sk0) = false,
inference(orient,[status(thm)],[t30843]) ).
fof(f109,axiom,
! [Xa,Xp,Xb] :
( Xa = Xb
| s(Xa,Xp) != s(Xb,Xp) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz7_18) ).
fof(f109_nnf,plain,
! [Xa,Xp,Xb] :
( Xa = Xb
| s(Xa,Xp) != s(Xb,Xp) ),
inference(nnf_transformation,[status(thm)],[f109]) ).
fof(f109_sk,plain,
! [Xa,Xp,Xb] :
( Xa = Xb
| s(Xa,Xp) != s(Xb,Xp) ),
inference(skolemisation,[status(esa)],[f109_nnf]) ).
cnf(c123,plain,
( X0 = X2
| s(X0,X1) != s(X2,X1) ),
inference(cnf_transformation,[status(esa)],[f109_sk]) ).
cnf(t78,plain,
ifeq(s(X1,X2),s(X3,X2),X1,X3) = X3,
inference(equality_encoding,[status(esa)],[c123]) ).
cnf(t271,plain,
ifeq(s(X1,X2),s(X3,X2),X1,X3) = X3,
inference(orient,[status(thm)],[t78]) ).
fof(f102,axiom,
! [Xa,Xp] :
( Xp != Xa
| s(Xa,Xp) = Xp ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz7_10b) ).
fof(f102_nnf,plain,
! [Xa,Xp] :
( Xp != Xa
| s(Xa,Xp) = Xp ),
inference(nnf_transformation,[status(thm)],[f102]) ).
fof(f102_sk,plain,
! [Xa,Xp] :
( Xp != Xa
| s(Xa,Xp) = Xp ),
inference(skolemisation,[status(esa)],[f102_nnf]) ).
cnf(c116,plain,
( X1 != X0
| s(X0,X1) = X1 ),
inference(cnf_transformation,[status(esa)],[f102_sk]) ).
cnf(hi106,axiom,
ifeq(X0,X1,s(X1,X0),X0) = X0,
inference(equality_encoding,[status(esa)],[c116]) ).
cnf(hi189,axiom,
or(X0,false) = X0,
introduced(definition) ).
cnf(t39,plain,
s(or(X1,false),X1) = X1,
inference(hyper_resolution,[status(thm)],[hi106,hi189]) ).
cnf(t7,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t282,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t30798,plain,
s(X1,X1) = X1,
inference(step,[status(thm)],[t39,t282]) ).
cnf(t293,plain,
s(X1,X1) = X1,
inference(orient,[status(thm)],[t30798]) ).
cnf(t295,plain,
X1 = ifeq(s(X2,X1),X1,X2,X1),
inference(cp,[status(thm)],[t271,t293]) ).
cnf(t3428,plain,
ifeq(s(X1,X2),X2,X1,X2) = X2,
inference(orient,[status(thm)],[t295]) ).
fof(f98,axiom,
! [Xa,Xp] : s(Xa,s(Xa,Xp)) = Xp,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz7_7) ).
fof(f98_nnf,plain,
! [Xa,Xp] : s(Xa,s(Xa,Xp)) = Xp,
inference(nnf_transformation,[status(thm)],[f98]) ).
fof(f98_sk,plain,
! [Xa,Xp] : s(Xa,s(Xa,Xp)) = Xp,
inference(skolemisation,[status(esa)],[f98_nnf]) ).
cnf(c112,plain,
s(X0,s(X0,X1)) = X1,
inference(cnf_transformation,[status(esa)],[f98_sk]) ).
cnf(t37,plain,
s(X1,s(X1,X2)) = X2,
inference(equality_encoding,[status(esa)],[c112]) ).
cnf(t284,plain,
s(X1,s(X1,X2)) = X2,
inference(orient,[status(thm)],[t37]) ).
cnf(t3429,plain,
s(X1,X2) = ifeq(X2,s(X1,X2),X1,s(X1,X2)),
inference(cp,[status(thm)],[t3428,t284]) ).
cnf(t10015,plain,
ifeq(X1,s(X2,X1),X2,s(X2,X1)) = s(X2,X1),
inference(orient,[status(thm)],[t3429]) ).
fof(f108,axiom,
! [Xp,Xa,Xq,Xb] :
( Xa = Xb
| ~ s_m(Xp,Xb,Xq)
| ~ s_m(Xp,Xa,Xq) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz7_17) ).
fof(f108_nnf,plain,
! [Xp,Xa,Xq,Xb] :
( Xa = Xb
| ~ s_m(Xp,Xb,Xq)
| ~ s_m(Xp,Xa,Xq) ),
inference(nnf_transformation,[status(thm)],[f108]) ).
fof(f108_sk,plain,
! [Xp,Xa,Xq,Xb] :
( Xa = Xb
| ~ s_m(Xp,Xb,Xq)
| ~ s_m(Xp,Xa,Xq) ),
inference(skolemisation,[status(esa)],[f108_nnf]) ).
cnf(c122,plain,
( X1 = X3
| ~ s_m(X0,X3,X2)
| ~ s_m(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f108_sk]) ).
cnf(t146,plain,
ifeq(s_m(X1,X2,X3),true,ifeq(s_m(X1,X4,X3),true,X2,X4),X4) = X4,
inference(equality_encoding,[status(esa)],[c122]) ).
cnf(t276,plain,
ifeq(s_m(X1,X2,X3),true,ifeq(s_m(X1,X4,X3),true,X2,X4),X4) = X4,
inference(orient,[status(thm)],[t146]) ).
fof(f95,axiom,
! [Xp,Xa] : s_m(Xp,Xa,s(Xa,Xp)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz7_4a) ).
fof(f95_nnf,plain,
! [Xp,Xa] : s_m(Xp,Xa,s(Xa,Xp)),
inference(nnf_transformation,[status(thm)],[f95]) ).
fof(f95_sk,plain,
! [Xp,Xa] : s_m(Xp,Xa,s(Xa,Xp)),
inference(skolemisation,[status(esa)],[f95_nnf]) ).
cnf(c109,plain,
s_m(X0,X1,s(X1,X0)),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(t50,plain,
s_m(X1,X2,s(X2,X1)) = true,
inference(equality_encoding,[status(esa)],[c109]) ).
cnf(t1860,plain,
s_m(X1,X2,s(X2,X1)) = true,
inference(orient,[status(thm)],[t50]) ).
cnf(t1862,plain,
true = s_m(s(X1,X2),X1,X2),
inference(cp,[status(thm)],[t1860,t284]) ).
cnf(t2652,plain,
s_m(s(X1,X2),X1,X2) = true,
inference(orient,[status(thm)],[t1862]) ).
cnf(t2657,plain,
X1 = ifeq(s_m(s(X1,X2),X3,X2),true,ifeq(true,true,X3,X1),X1),
inference(cp,[status(thm)],[t276,t2652]) ).
cnf(t31207,plain,
X1 = ifeq(s_m(s(X1,X2),X3,X2),true,X3,X1),
inference(step,[status(thm)],[t2657,t256]) ).
cnf(t10433,plain,
ifeq(s_m(s(X1,X2),X3,X2),true,X3,X1) = X1,
inference(orient,[status(thm)],[t31207]) ).
fof(f119,axiom,
! [Xa,Xm,Xb] :
( ( s_m(Xa,Xm,Xb)
| ~ s_e(Xm,Xa,Xm,Xb)
| ~ s_t(Xa,Xm,Xb) )
& ( s_e(Xm,Xa,Xm,Xb)
| ~ s_m(Xa,Xm,Xb) )
& ( s_t(Xa,Xm,Xb)
| ~ s_m(Xa,Xm,Xb) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d_Defn7_1) ).
fof(f119_nnf,plain,
! [Xa,Xm,Xb] :
( ( s_m(Xa,Xm,Xb)
| ~ s_e(Xm,Xa,Xm,Xb)
| ~ s_t(Xa,Xm,Xb) )
& ( s_e(Xm,Xa,Xm,Xb)
| ~ s_m(Xa,Xm,Xb) )
& ( s_t(Xa,Xm,Xb)
| ~ s_m(Xa,Xm,Xb) ) ),
inference(nnf_transformation,[status(thm)],[f119]) ).
fof(f119_sk,plain,
! [Xa,Xm,Xb] :
( ( s_m(Xa,Xm,Xb)
| ~ s_e(Xm,Xa,Xm,Xb)
| ~ s_t(Xa,Xm,Xb) )
& ( s_e(Xm,Xa,Xm,Xb)
| ~ s_m(Xa,Xm,Xb) )
& ( s_t(Xa,Xm,Xb)
| ~ s_m(Xa,Xm,Xb) ) ),
inference(skolemisation,[status(esa)],[f119_nnf]) ).
cnf(c164,plain,
( s_m(X0,X1,X2)
| ~ s_e(X1,X0,X1,X2)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f119_sk]) ).
cnf(t195,plain,
ifeq(s_t(X1,X2,X3),true,ifeq(s_e(X2,X1,X2,X3),true,s_m(X1,X2,X3),true),true) = true,
inference(equality_encoding,[status(esa)],[c164]) ).
cnf(t343,plain,
ifeq(s_t(X1,X2,X3),true,ifeq(s_e(X2,X1,X2,X3),true,s_m(X1,X2,X3),true),true) = true,
inference(orient,[status(thm)],[t195]) ).
fof(f17,axiom,
! [Xa,Xb,Xc,Xd] :
( s_e(Xb,Xa,Xd,Xc)
| ~ s_e(Xa,Xb,Xc,Xd) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz2_14) ).
fof(f17_nnf,plain,
! [Xa,Xb,Xc,Xd] :
( s_e(Xb,Xa,Xd,Xc)
| ~ s_e(Xa,Xb,Xc,Xd) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [Xa,Xb,Xc,Xd] :
( s_e(Xb,Xa,Xd,Xc)
| ~ s_e(Xa,Xb,Xc,Xd) ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c21,plain,
( s_e(X1,X0,X3,X2)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(t131,plain,
ifeq(s_e(X1,X2,X3,X4),true,s_e(X2,X1,X4,X3),true) = true,
inference(equality_encoding,[status(esa)],[c21]) ).
cnf(t400,plain,
ifeq(s_e(X1,X2,X3,X4),true,s_e(X2,X1,X4,X3),true) = true,
inference(orient,[status(thm)],[t131]) ).
fof(f106,axiom,
! [Xp,Xq,Xr,Xcs,Xa] :
( s_e(s(Xa,Xp),s(Xa,Xq),s(Xa,Xr),s(Xa,Xcs))
| ~ s_e(Xp,Xq,Xr,Xcs) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz7_16a) ).
fof(f106_nnf,plain,
! [Xp,Xq,Xr,Xcs,Xa] :
( s_e(s(Xa,Xp),s(Xa,Xq),s(Xa,Xr),s(Xa,Xcs))
| ~ s_e(Xp,Xq,Xr,Xcs) ),
inference(nnf_transformation,[status(thm)],[f106]) ).
fof(f106_sk,plain,
! [Xp,Xq,Xr,Xcs,Xa] :
( s_e(s(Xa,Xp),s(Xa,Xq),s(Xa,Xr),s(Xa,Xcs))
| ~ s_e(Xp,Xq,Xr,Xcs) ),
inference(skolemisation,[status(esa)],[f106_nnf]) ).
cnf(c120,plain,
( s_e(s(X4,X0),s(X4,X1),s(X4,X2),s(X4,X3))
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f106_sk]) ).
cnf(t208,plain,
ifeq(s_e(X1,X2,X3,X4),true,s_e(s(X5,X1),s(X5,X2),s(X5,X3),s(X5,X4)),true) = true,
inference(equality_encoding,[status(esa)],[c120]) ).
cnf(t418,plain,
ifeq(s_e(X1,X2,X3,X4),true,s_e(s(X5,X1),s(X5,X2),s(X5,X3),s(X5,X4)),true) = true,
inference(orient,[status(thm)],[t208]) ).
cnf(t420,plain,
true = ifeq(s_e(s(X1,X2),X3,X4,X5),true,s_e(X2,s(X1,X3),s(X1,X4),s(X1,X5)),true),
inference(cp,[status(thm)],[t418,t284]) ).
cnf(t29882,plain,
ifeq(s_e(s(X1,X2),X3,X4,X5),true,s_e(X2,s(X1,X3),s(X1,X4),s(X1,X5)),true) = true,
inference(orient,[status(thm)],[t420]) ).
fof(f103,axiom,
! [Xp,Xq,Xa] : s_e(Xp,Xq,s(Xa,Xp),s(Xa,Xq)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz7_13) ).
fof(f103_nnf,plain,
! [Xp,Xq,Xa] : s_e(Xp,Xq,s(Xa,Xp),s(Xa,Xq)),
inference(nnf_transformation,[status(thm)],[f103]) ).
fof(f103_sk,plain,
! [Xp,Xq,Xa] : s_e(Xp,Xq,s(Xa,Xp),s(Xa,Xq)),
inference(skolemisation,[status(esa)],[f103_nnf]) ).
cnf(c117,plain,
s_e(X0,X1,s(X2,X0),s(X2,X1)),
inference(cnf_transformation,[status(esa)],[f103_sk]) ).
cnf(t86,plain,
s_e(X1,X2,s(X3,X1),s(X3,X2)) = true,
inference(equality_encoding,[status(esa)],[c117]) ).
cnf(t1410,plain,
s_e(X1,X2,s(X3,X1),s(X3,X2)) = true,
inference(orient,[status(thm)],[t86]) ).
cnf(t1413,plain,
true = s_e(X1,X2,s(X2,X1),X2),
inference(cp,[status(thm)],[t1410,t293]) ).
cnf(t3497,plain,
s_e(X1,X2,s(X2,X1),X2) = true,
inference(orient,[status(thm)],[t1413]) ).
cnf(t3498,plain,
true = s_e(s(X1,X2),X1,X2,X1),
inference(cp,[status(thm)],[t3497,t284]) ).
cnf(t4411,plain,
s_e(s(X1,X2),X1,X2,X1) = true,
inference(orient,[status(thm)],[t3498]) ).
cnf(c124,plain,
s(sk0,s(sk1,sk2)) = s(sk1,s(sk0,sk2)),
inference(cnf_transformation,[status(esa)],[f110_sk]) ).
cnf(t81,plain,
s(sk1,s(sk0,sk2)) = s(sk0,s(sk1,sk2)),
inference(equality_encoding,[status(esa)],[c124]) ).
cnf(t2549,plain,
s(sk0,s(sk1,sk2)) = s(sk1,s(sk0,sk2)),
inference(orient,[status(thm)],[t81]) ).
cnf(t4412,plain,
true = s_e(s(sk1,s(sk0,sk2)),sk0,s(sk1,sk2),sk0),
inference(cp,[status(thm)],[t4411,t2549]) ).
cnf(t11885,plain,
s_e(s(sk1,s(sk0,sk2)),sk0,s(sk1,sk2),sk0) = true,
inference(orient,[status(thm)],[t4412]) ).
cnf(t29883,plain,
true = ifeq(true,true,s_e(s(sk0,sk2),s(sk1,sk0),s(sk1,s(sk1,sk2)),s(sk1,sk0)),true),
inference(cp,[status(thm)],[t29882,t11885]) ).
cnf(t31969,plain,
true = s_e(s(sk0,sk2),s(sk1,sk0),s(sk1,s(sk1,sk2)),s(sk1,sk0)),
inference(step,[status(thm)],[t29883,t256]) ).
cnf(t31970,plain,
true = s_e(s(sk0,sk2),s(sk1,sk0),sk2,s(sk1,sk0)),
inference(step,[status(thm)],[t31969,t284]) ).
cnf(t29949,plain,
s_e(s(sk0,sk2),s(sk1,sk0),sk2,s(sk1,sk0)) = true,
inference(orient,[status(thm)],[t31970]) ).
cnf(t29952,plain,
true = ifeq(true,true,s_e(s(sk1,sk0),s(sk0,sk2),s(sk1,sk0),sk2),true),
inference(cp,[status(thm)],[t400,t29949]) ).
cnf(t31978,plain,
true = s_e(s(sk1,sk0),s(sk0,sk2),s(sk1,sk0),sk2),
inference(step,[status(thm)],[t29952,t256]) ).
cnf(t30180,plain,
s_e(s(sk1,sk0),s(sk0,sk2),s(sk1,sk0),sk2) = true,
inference(orient,[status(thm)],[t31978]) ).
cnf(t30189,plain,
true = ifeq(s_t(s(sk0,sk2),s(sk1,sk0),sk2),true,ifeq(true,true,s_m(s(sk0,sk2),s(sk1,sk0),sk2),true),true),
inference(cp,[status(thm)],[t343,t30180]) ).
fof(f104,axiom,
! [Xp,Xq,Xr,Xa] :
( s_t(s(Xa,Xp),s(Xa,Xq),s(Xa,Xr))
| ~ s_t(Xp,Xq,Xr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz7_15a) ).
fof(f104_nnf,plain,
! [Xp,Xq,Xr,Xa] :
( s_t(s(Xa,Xp),s(Xa,Xq),s(Xa,Xr))
| ~ s_t(Xp,Xq,Xr) ),
inference(nnf_transformation,[status(thm)],[f104]) ).
fof(f104_sk,plain,
! [Xp,Xq,Xr,Xa] :
( s_t(s(Xa,Xp),s(Xa,Xq),s(Xa,Xr))
| ~ s_t(Xp,Xq,Xr) ),
inference(skolemisation,[status(esa)],[f104_nnf]) ).
cnf(c118,plain,
( s_t(s(X3,X0),s(X3,X1),s(X3,X2))
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f104_sk]) ).
cnf(t184,plain,
ifeq(s_t(X1,X2,X3),true,s_t(s(X4,X1),s(X4,X2),s(X4,X3)),true) = true,
inference(equality_encoding,[status(esa)],[c118]) ).
cnf(t357,plain,
ifeq(s_t(X1,X2,X3),true,s_t(s(X4,X1),s(X4,X2),s(X4,X3)),true) = true,
inference(orient,[status(thm)],[t184]) ).
cnf(t359,plain,
true = ifeq(s_t(s(X1,X2),X3,X4),true,s_t(X2,s(X1,X3),s(X1,X4)),true),
inference(cp,[status(thm)],[t357,t284]) ).
cnf(t14184,plain,
ifeq(s_t(s(X1,X2),X3,X4),true,s_t(X2,s(X1,X3),s(X1,X4)),true) = true,
inference(orient,[status(thm)],[t359]) ).
cnf(c162,plain,
( s_t(X0,X1,X2)
| ~ s_m(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f119_sk]) ).
cnf(t113,plain,
ifeq(s_m(X1,X2,X3),true,s_t(X1,X2,X3),true) = true,
inference(equality_encoding,[status(esa)],[c162]) ).
cnf(t525,plain,
ifeq(s_m(X1,X2,X3),true,s_t(X1,X2,X3),true) = true,
inference(orient,[status(thm)],[t113]) ).
cnf(t2655,plain,
true = ifeq(true,true,s_t(s(X1,X2),X1,X2),true),
inference(cp,[status(thm)],[t525,t2652]) ).
cnf(t30846,plain,
true = s_t(s(X1,X2),X1,X2),
inference(step,[status(thm)],[t2655,t256]) ).
cnf(t3177,plain,
s_t(s(X1,X2),X1,X2) = true,
inference(orient,[status(thm)],[t30846]) ).
cnf(t3178,plain,
true = s_t(s(sk1,s(sk0,sk2)),sk0,s(sk1,sk2)),
inference(cp,[status(thm)],[t3177,t2549]) ).
cnf(t10525,plain,
s_t(s(sk1,s(sk0,sk2)),sk0,s(sk1,sk2)) = true,
inference(orient,[status(thm)],[t3178]) ).
cnf(t14186,plain,
true = ifeq(true,true,s_t(s(sk0,sk2),s(sk1,sk0),s(sk1,s(sk1,sk2))),true),
inference(cp,[status(thm)],[t14184,t10525]) ).
cnf(t31354,plain,
true = s_t(s(sk0,sk2),s(sk1,sk0),s(sk1,s(sk1,sk2))),
inference(step,[status(thm)],[t14186,t256]) ).
cnf(t31355,plain,
true = s_t(s(sk0,sk2),s(sk1,sk0),sk2),
inference(step,[status(thm)],[t31354,t284]) ).
cnf(t14284,plain,
s_t(s(sk0,sk2),s(sk1,sk0),sk2) = true,
inference(orient,[status(thm)],[t31355]) ).
cnf(t31979,plain,
true = ifeq(true,true,ifeq(true,true,s_m(s(sk0,sk2),s(sk1,sk0),sk2),true),true),
inference(step,[status(thm)],[t30189,t14284]) ).
cnf(t31980,plain,
true = ifeq(true,true,s_m(s(sk0,sk2),s(sk1,sk0),sk2),true),
inference(step,[status(thm)],[t31979,t256]) ).
cnf(t31981,plain,
true = s_m(s(sk0,sk2),s(sk1,sk0),sk2),
inference(step,[status(thm)],[t31980,t256]) ).
cnf(t30234,plain,
s_m(s(sk0,sk2),s(sk1,sk0),sk2) = true,
inference(orient,[status(thm)],[t31981]) ).
cnf(t30238,plain,
sk0 = ifeq(true,true,s(sk1,sk0),sk0),
inference(cp,[status(thm)],[t10433,t30234]) ).
cnf(t31982,plain,
sk0 = s(sk1,sk0),
inference(step,[status(thm)],[t30238,t256]) ).
cnf(t30246,plain,
s(sk1,sk0) = sk0,
inference(orient,[status(thm)],[t31982]) ).
cnf(t30258,plain,
s(sk1,sk0) = ifeq(sk0,sk0,sk1,s(sk1,sk0)),
inference(cp,[status(thm)],[t10015,t30246]) ).
cnf(t31991,plain,
sk0 = ifeq(sk0,sk0,sk1,s(sk1,sk0)),
inference(step,[status(thm)],[t30258,t30246]) ).
cnf(t31992,plain,
sk0 = sk1,
inference(step,[status(thm)],[t31991,t256]) ).
cnf(t30514,plain,
sk0 = sk1,
inference(orient,[status(thm)],[t31992]) ).
cnf(t31993,plain,
s_t(sk1,sk1,sk0) = false,
inference(step,[status(thm)],[t3094,t30514]) ).
fof(f21,axiom,
! [Xa1,Xb1] : s_t(Xa1,Xa1,Xb1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aSatz3_3) ).
fof(f21_nnf,plain,
! [Xa1,Xb1] : s_t(Xa1,Xa1,Xb1),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [Xa1,Xb1] : s_t(Xa1,Xa1,Xb1),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c25,plain,
s_t(X0,X0,X1),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(t20,plain,
s_t(X1,X1,X2) = true,
inference(equality_encoding,[status(esa)],[c25]) ).
cnf(t782,plain,
s_t(X1,X1,X2) = true,
inference(orient,[status(thm)],[t20]) ).
cnf(t31994,plain,
true = false,
inference(step,[status(thm)],[t31993,t782]) ).
cnf(t30515,plain,
true = false,
inference(rw,[status(thm)],[t31994]) ).
cnf(t30535,plain,
false = true,
inference(orient,[status(thm)],[t30515]) ).
fof(f7,axiom,
( ~ s_t(gamma,alpha,beta)
& ~ s_t(beta,gamma,alpha)
& ~ s_t(alpha,beta,gamma) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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(f118,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/sandbox2/benchmark/theBenchmark.p',d_Defn6_1) ).
fof(f118_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)],[f118]) ).
fof(f118_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)],[f118_nnf]) ).
cnf(c157,plain,
( X0 != X1
| ~ sameside(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f118_sk]) ).
cnf(c158,plain,
( X2 != X1
| ~ sameside(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f118_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c9,c10,c11,c33,c34,c35,c37,c77,c78,c79,c84,c125,c157,c158]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t30535]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO500+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.07/0.33 % Computer : n012.cluster.edu
% 0.07/0.33 % Model : x86_64 x86_64
% 0.07/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.33 % Memory : 8046.5625MB
% 0.07/0.33 % OS : Linux 6.8.0-71-generic
% 0.07/0.33 % CPULimit : 300
% 0.07/0.33 % WCLimit : 300
% 0.07/0.33 % DateTime : Wed Sep 23 12:13:21 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.07/0.34 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 77.88/10.16 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 77.88/10.16 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------