%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GEO521+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 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:21:23 PM UTC 2026
% Result : Theorem 220.65s 34.18s
% Output : CNFRefutation 220.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 17
% Syntax : Number of formulae : 106 ( 38 unt; 0 def)
% Number of atoms : 268 ( 75 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 272 ( 110 ~; 144 |; 18 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-4 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-3 aty)
% Number of variables : 205 ( 0 sgn 201 !; 4 ?; 88 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : s_e(X0,X1,X1,X0),
file('/export/starexec/sandbox/benchmark/Axioms/GEO011+0.ax',aA1) ).
fof(f9,axiom,
! [X0,X1,X2,X3,X4,X5] :
( s_t(X5,X2,X4)
| s_t(X4,X5,X2)
| s_t(X2,X4,X5)
| ~ s_e(X5,X0,X5,X1)
| ~ s_e(X4,X0,X4,X1)
| ~ s_e(X2,X0,X3,X1)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aA9) ).
fof(f21,axiom,
! [X0,X1] : s_t(X0,X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz3_1) ).
fof(f94,axiom,
! [X0,X1,X2] :
( s_m(X2,X1,X0)
| ~ s_m(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz7_2) ).
fof(f97,axiom,
! [X0,X1] : s_m(X0,X1,s(X1,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz7_4a) ).
fof(f100,axiom,
! [X0,X1] : s(X0,s(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz7_7) ).
fof(f101,axiom,
! [X0,X1,X2,X3] :
( X1 = X3
| s(X0,X3) != X2
| s(X0,X1) != X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz7_8) ).
fof(f103,axiom,
! [X0,X1] :
( X1 = X0
| s(X0,X1) != X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz7_10a) ).
fof(f104,axiom,
! [X0,X1] :
( X1 != X0
| s(X0,X1) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz7_10b) ).
fof(f136,axiom,
! [X0,X1,X2,X3,X4] :
( ( ~ perp(X0,X1,X4,X2)
| s_r(X4,X2,X3)
| X3 = X2
| ~ s_col(X0,X1,X3)
| ~ s_col(X0,X1,X2)
| X0 = X1 )
& ( ~ perp(X0,X1,X4,X2)
| ~ s_col(X0,X1,X4)
| X3 = X2
| ~ s_col(X0,X1,X3)
| ~ s_col(X0,X1,X2)
| X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz8_16a) ).
fof(f139,axiom,
! [X0,X1,X2] :
( ( perp(X0,X1,X2,foot(X0,X1,X2))
| s_col(X0,X1,X2) )
& ( s_col(X0,X1,foot(X0,X1,X2))
| s_col(X0,X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz8_18) ).
fof(f142,axiom,
! [X0,X1,X2,X3] :
( perp(X1,X0,X2,X3)
| ~ perp(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aperp1) ).
fof(f180,conjecture,
! [X0,X1,X2,X3] :
( X0 != foot(X0,X1,X2)
| opposite(X2,X0,X1,X3)
| samesideline(X2,X3,X0,X1)
| s_col(X0,X1,X3)
| s_col(X0,X1,X2)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aLemma9_13f_case1) ).
fof(f181,negated_conjecture,
~ ! [X0,X1,X2,X3] :
( X0 != foot(X0,X1,X2)
| opposite(X2,X0,X1,X3)
| samesideline(X2,X3,X0,X1)
| s_col(X0,X1,X3)
| s_col(X0,X1,X2)
| X0 = X1 ),
inference(negated_conjecture,[status(cth)],[f180]) ).
fof(f186,axiom,
! [X0,X1,X2] :
( ( ~ s_t(X2,X0,X1)
| s_col(X0,X1,X2) )
& ( ~ s_t(X1,X2,X0)
| s_col(X0,X1,X2) )
& ( ~ s_t(X0,X1,X2)
| s_col(X0,X1,X2) )
& ( s_t(X2,X0,X1)
| s_t(X1,X2,X0)
| s_t(X0,X1,X2)
| ~ s_col(X0,X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d_Defn4_10) ).
fof(f190,axiom,
! [X0,X1,X2] :
( ( s_m(X0,X1,X2)
| ~ s_e(X1,X0,X1,X2)
| ~ s_t(X0,X1,X2) )
& ( s_e(X1,X0,X1,X2)
| ~ s_m(X0,X1,X2) )
& ( s_t(X0,X1,X2)
| ~ s_m(X0,X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d_Defn7_1) ).
fof(f192,axiom,
! [X0,X1,X2] :
( ( ~ s_e(X0,X2,X0,s(X1,X2))
| s_r(X0,X1,X2) )
& ( s_e(X0,X2,X0,s(X1,X2))
| ~ s_r(X0,X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d_Defn8_1) ).
fof(f197,plain,
? [X0,X1,X2,X3] :
( foot(X0,X1,X2) = X0
& ~ opposite(X2,X0,X1,X3)
& ~ samesideline(X2,X3,X0,X1)
& ~ s_col(X0,X1,X3)
& ~ s_col(X0,X1,X2)
& X0 != X1 ),
inference(ennf_transformation,[],[f181]) ).
fof(f198,plain,
( sK0 = foot(sK0,sK1,sK2)
& ~ opposite(sK2,sK0,sK1,sK3)
& ~ samesideline(sK2,sK3,sK0,sK1)
& ~ s_col(sK0,sK1,sK3)
& ~ s_col(sK0,sK1,sK2)
& sK0 != sK1 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3)],[f197]) ).
fof(f199,plain,
sK0 = foot(sK0,sK1,sK2),
inference(cnf_transformation,[],[f198]) ).
fof(f203,plain,
~ s_col(sK0,sK1,sK2),
inference(cnf_transformation,[],[f198]) ).
fof(f204,plain,
sK0 != sK1,
inference(cnf_transformation,[],[f198]) ).
fof(f220,plain,
! [X2,X0,X1] :
( ~ s_t(X2,X0,X1)
| s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f186]) ).
fof(f221,plain,
! [X2,X0,X1] :
( ~ s_t(X1,X2,X0)
| s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f186]) ).
fof(f222,plain,
! [X2,X0,X1] :
( ~ s_t(X0,X1,X2)
| s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f186]) ).
fof(f251,plain,
! [X2,X0,X1] :
( perp(X0,X1,X2,foot(X0,X1,X2))
| s_col(X0,X1,X2) ),
inference(cnf_transformation,[],[f139]) ).
fof(f263,plain,
! [X0,X1] : s_t(X0,X1,X1),
inference(cnf_transformation,[],[f21]) ).
fof(f266,plain,
! [X2,X3,X0,X1,X4,X5] :
( s_t(X5,X2,X4)
| s_t(X4,X5,X2)
| s_t(X2,X4,X5)
| ~ s_e(X5,X0,X5,X1)
| ~ s_e(X4,X0,X4,X1)
| ~ s_e(X2,X0,X3,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f9]) ).
fof(f278,plain,
! [X0,X1] : s_e(X0,X1,X1,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f297,plain,
! [X2,X0,X1] :
( s_e(X1,X0,X1,X2)
| ~ s_m(X0,X1,X2) ),
inference(cnf_transformation,[],[f190]) ).
fof(f298,plain,
! [X2,X0,X1] :
( s_t(X0,X1,X2)
| ~ s_m(X0,X1,X2) ),
inference(cnf_transformation,[],[f190]) ).
fof(f306,plain,
! [X0,X1] : s_m(X0,X1,s(X1,X0)),
inference(cnf_transformation,[],[f97]) ).
fof(f309,plain,
! [X2,X0,X1] :
( s_m(X2,X1,X0)
| ~ s_m(X0,X1,X2) ),
inference(cnf_transformation,[],[f94]) ).
fof(f314,plain,
! [X2,X3,X0,X1] :
( perp(X1,X0,X2,X3)
| ~ perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f142]) ).
fof(f319,plain,
! [X2,X0,X1] :
( s_e(X0,X2,X0,s(X1,X2))
| ~ s_r(X0,X1,X2) ),
inference(cnf_transformation,[],[f192]) ).
fof(f330,plain,
! [X0,X1] :
( X0 != X1
| s(X0,X1) = X1 ),
inference(cnf_transformation,[],[f104]) ).
fof(f331,plain,
! [X0,X1] :
( X0 = X1
| s(X0,X1) != X1 ),
inference(cnf_transformation,[],[f103]) ).
fof(f333,plain,
! [X2,X3,X0,X1] :
( X1 = X3
| s(X0,X3) != X2
| s(X0,X1) != X2 ),
inference(cnf_transformation,[],[f101]) ).
fof(f334,plain,
! [X0,X1] : s(X0,s(X0,X1)) = X1,
inference(cnf_transformation,[],[f100]) ).
fof(f346,plain,
! [X2,X3,X0,X1,X4] :
( ~ perp(X0,X1,X4,X2)
| s_r(X4,X2,X3)
| X2 = X3
| ~ s_col(X0,X1,X3)
| ~ s_col(X0,X1,X2)
| X0 = X1 ),
inference(cnf_transformation,[],[f136]) ).
fof(f359,plain,
! [X1] : s(X1,X1) = X1,
inference(equality_resolution,[],[f330]) ).
fof(f360,plain,
! [X3,X0,X1] :
( X1 = X3
| s(X0,X1) != s(X0,X3) ),
inference(equality_resolution,[],[f333]) ).
tcf(c_49,negated_conjecture,
sK0 != sK1,
inference(cnf_transformation,[],[f204]) ).
tcf(c_50,negated_conjecture,
~ s_col(sK0,sK1,sK2),
inference(cnf_transformation,[],[f203]) ).
tcf(c_54,negated_conjecture,
foot(sK0,sK1,sK2) = sK0,
inference(cnf_transformation,[],[f199]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_col(X0,X1,X2)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f222]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_col(X2,X0,X1)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f221]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_col(X1,X2,X0)
| ~ s_t(X0,X1,X2) ),
inference(cnf_transformation,[],[f220]) ).
tcf(c_102,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_col(X0,X1,X2)
| perp(X0,X1,X2,foot(X0,X1,X2)) ),
inference(cnf_transformation,[],[f251]) ).
tcf(c_113,plain,
! [X0: $i,X1: $i] : s_t(X0,X1,X1),
inference(cnf_transformation,[],[f263]) ).
tcf(c_116,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( s_t(X5,X0,X4)
| s_t(X4,X5,X0)
| s_t(X0,X4,X5)
| ( X1 = X3 )
| ~ s_e(X5,X1,X5,X3)
| ~ s_e(X4,X1,X4,X3)
| ~ s_e(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f266]) ).
tcf(c_128,plain,
! [X0: $i,X1: $i] : s_e(X0,X1,X1,X0),
inference(cnf_transformation,[],[f278]) ).
tcf(c_146,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_t(X0,X1,X2)
| ~ s_m(X0,X1,X2) ),
inference(cnf_transformation,[],[f298]) ).
tcf(c_147,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_e(X1,X0,X1,X2)
| ~ s_m(X0,X1,X2) ),
inference(cnf_transformation,[],[f297]) ).
tcf(c_156,plain,
! [X0: $i,X1: $i] : s_m(X0,X1,s(X1,X0)),
inference(cnf_transformation,[],[f306]) ).
tcf(c_159,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_m(X2,X1,X0)
| ~ s_m(X0,X1,X2) ),
inference(cnf_transformation,[],[f309]) ).
tcf(c_164,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( perp(X1,X0,X2,X3)
| ~ perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f314]) ).
tcf(c_168,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_e(X0,X2,X0,s(X1,X2))
| ~ s_r(X0,X1,X2) ),
inference(cnf_transformation,[],[f319]) ).
tcf(c_180,plain,
! [X0: $i] : s(X0,X0) = X0,
inference(cnf_transformation,[],[f359]) ).
tcf(c_181,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ( s(X0,X1) != X1 ) ),
inference(cnf_transformation,[],[f331]) ).
tcf(c_183,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X1 = X2 )
| ( s(X0,X1) != s(X0,X2) ) ),
inference(cnf_transformation,[],[f360]) ).
tcf(c_184,plain,
! [X0: $i,X1: $i] : s(X0,s(X0,X1)) = X1,
inference(cnf_transformation,[],[f334]) ).
tcf(c_197,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( s_r(X2,X3,X4)
| ( X3 = X4 )
| ( X0 = X1 )
| ~ s_col(X0,X1,X4)
| ~ s_col(X0,X1,X3)
| ~ perp(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f346]) ).
tcf(c_211,plain,
s(sK0,sK0) = sK0,
inference(instantiation,[status(thm)],[c_180]) ).
tcf(c_3617,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_5396,plain,
! [X0: $i,X1: $i] : s_col(X0,X1,X1),
inference(superposition,[status(thm)],[c_113,c_71]) ).
tcf(c_5473,plain,
! [X0: $i,X1: $i] : s_t(X0,X1,s(X1,X0)),
inference(superposition,[status(thm)],[c_156,c_146]) ).
tcf(c_5483,plain,
! [X0: $i,X1: $i] : s_col(X0,X1,s(X1,X0)),
inference(superposition,[status(thm)],[c_5473,c_71]) ).
tcf(c_6044,plain,
( s_col(sK0,sK1,sK2)
| perp(sK0,sK1,sK2,sK0) ),
inference(superposition,[status(thm)],[c_54,c_102]) ).
tcf(c_6048,plain,
perp(sK0,sK1,sK2,sK0),
inference(forward_subsumption_resolution,[status(thm)],[c_6044,c_50]) ).
tcf(c_6056,plain,
perp(sK1,sK0,sK2,sK0),
inference(superposition,[status(thm)],[c_6048,c_164]) ).
tcf(c_6376,plain,
( ( sK0 = sK1 )
| ( s(sK0,sK1) != sK1 ) ),
inference(instantiation,[status(thm)],[c_181]) ).
tcf(c_6397,plain,
( s_col(sK0,sK1,sK2)
| ~ s_t(sK0,sK1,sK2) ),
inference(instantiation,[status(thm)],[c_71]) ).
tcf(c_6399,plain,
( s_col(sK0,sK1,sK2)
| ~ s_t(sK1,sK2,sK0) ),
inference(instantiation,[status(thm)],[c_72]) ).
tcf(c_6413,plain,
( s_col(sK0,sK1,sK2)
| ~ s_t(sK2,sK0,sK1) ),
inference(instantiation,[status(thm)],[c_73]) ).
tcf(c_6592,plain,
! [X0: $i] :
( ( sK0 = sK1 )
| ( s(X0,sK0) != s(X0,sK1) ) ),
inference(instantiation,[status(thm)],[c_183]) ).
tcf(c_6593,plain,
( ( sK0 = sK1 )
| ( s(sK0,sK0) != s(sK0,sK1) ) ),
inference(instantiation,[status(thm)],[c_6592]) ).
tcf(c_11078,plain,
! [X0: $i,X1: $i] :
( ( s(X0,sK0) = s(X0,sK1) )
| ( s(X0,sK1) != X1 )
| ( s(X0,sK0) != X1 ) ),
inference(instantiation,[status(thm)],[c_3617]) ).
tcf(c_11079,plain,
( ( s(sK0,sK0) = s(sK0,sK1) )
| ( s(sK0,sK1) != sK0 )
| ( s(sK0,sK0) != sK0 ) ),
inference(instantiation,[status(thm)],[c_11078]) ).
tcf(c_13716,plain,
! [X0: $i,X1: $i] :
( s_m(X1,X0,sK1)
| ~ s_m(sK1,X0,X1) ),
inference(instantiation,[status(thm)],[c_159]) ).
tcf(c_18888,plain,
! [X0: $i] :
( s_r(sK2,sK0,X0)
| ( sK0 = sK1 )
| ( X0 = sK0 )
| ~ s_col(sK1,sK0,sK0)
| ~ s_col(sK1,sK0,X0) ),
inference(superposition,[status(thm)],[c_6056,c_197]) ).
tcf(c_18907,plain,
! [X0: $i] :
( s_r(sK2,sK0,X0)
| ( X0 = sK0 )
| ~ s_col(sK1,sK0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_18888,c_49,c_5396]) ).
tcf(c_19653,plain,
( s_r(sK2,sK0,s(sK0,sK1))
| ( s(sK0,sK1) = sK0 ) ),
inference(superposition,[status(thm)],[c_5483,c_18907]) ).
tcf(c_31393,plain,
! [X0: $i] :
( s_m(s(X0,sK1),X0,sK1)
| ~ s_m(sK1,X0,s(X0,sK1)) ),
inference(instantiation,[status(thm)],[c_13716]) ).
tcf(c_31394,plain,
! [X0: $i] : s_m(sK1,X0,s(X0,sK1)),
inference(instantiation,[status(thm)],[c_156]) ).
tcf(c_31395,plain,
( s_m(s(sK0,sK1),sK0,sK1)
| ~ s_m(sK1,sK0,s(sK0,sK1)) ),
inference(instantiation,[status(thm)],[c_31393]) ).
tcf(c_31396,plain,
s_m(sK1,sK0,s(sK0,sK1)),
inference(instantiation,[status(thm)],[c_31394]) ).
tcf(c_33824,plain,
( s_e(sK0,s(sK0,sK1),sK0,sK1)
| ~ s_m(s(sK0,sK1),sK0,sK1) ),
inference(instantiation,[status(thm)],[c_147]) ).
tcf(c_66681,plain,
! [X0: $i,X1: $i] : s_col(X0,X1,X1),
inference(superposition,[status(thm)],[c_113,c_71]) ).
tcf(c_66783,plain,
! [X0: $i,X1: $i] : s_t(X0,X1,s(X1,X0)),
inference(superposition,[status(thm)],[c_156,c_146]) ).
tcf(c_66832,plain,
! [X0: $i,X1: $i] : s_col(X0,X1,s(X1,X0)),
inference(superposition,[status(thm)],[c_66783,c_71]) ).
tcf(c_67094,plain,
( s_col(sK0,sK1,sK2)
| perp(sK0,sK1,sK2,sK0) ),
inference(superposition,[status(thm)],[c_54,c_102]) ).
tcf(c_67095,plain,
perp(sK0,sK1,sK2,sK0),
inference(forward_subsumption_resolution,[status(thm)],[c_67094,c_50]) ).
tcf(c_67173,plain,
perp(sK1,sK0,sK2,sK0),
inference(superposition,[status(thm)],[c_67095,c_164]) ).
tcf(c_67282,plain,
! [X0: $i,X1: $i,X2: $i] :
( s_e(X0,s(X1,X2),X0,X2)
| ~ s_r(X0,X1,s(X1,X2)) ),
inference(superposition,[status(thm)],[c_184,c_168]) ).
tcf(c_94295,plain,
! [X0: $i] :
( s_r(sK2,sK0,X0)
| ( sK0 = sK1 )
| ( X0 = sK0 )
| ~ s_col(sK1,sK0,sK0)
| ~ s_col(sK1,sK0,X0) ),
inference(superposition,[status(thm)],[c_67173,c_197]) ).
tcf(c_94311,plain,
! [X0: $i] :
( s_r(sK2,sK0,X0)
| ( X0 = sK0 )
| ~ s_col(sK1,sK0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_94295,c_49,c_66681]) ).
tcf(c_97492,plain,
( s_r(sK2,sK0,s(sK0,sK1))
| ( s(sK0,sK1) = sK0 ) ),
inference(superposition,[status(thm)],[c_66832,c_94311]) ).
tcf(c_98495,plain,
s_r(sK2,sK0,s(sK0,sK1)),
inference(global_subsumption_just,[status(thm)],[c_97492,c_49,c_211,c_6593,c_11079,c_19653]) ).
tcf(c_98499,plain,
s_e(sK2,s(sK0,sK1),sK2,sK1),
inference(superposition,[status(thm)],[c_98495,c_67282]) ).
tcf(c_687089,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( s_t(X3,X0,X2)
| s_t(X2,X3,X0)
| s_t(X0,X2,X3)
| ( s(sK0,sK1) = sK1 )
| ~ s_e(X3,s(sK0,sK1),X3,sK1)
| ~ s_e(X2,s(sK0,sK1),X2,sK1)
| ~ s_e(X0,s(sK0,sK1),X1,sK1) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_755718,plain,
! [X0: $i] : s_e(sK1,X0,X0,sK1),
inference(instantiation,[status(thm)],[c_128]) ).
tcf(c_799603,plain,
! [X0: $i] :
( s_t(sK2,sK0,sK1)
| s_t(sK1,sK2,sK0)
| s_t(sK0,sK1,sK2)
| ( s(sK0,sK1) = sK1 )
| ~ s_e(sK2,s(sK0,sK1),sK2,sK1)
| ~ s_e(sK0,s(sK0,sK1),sK0,sK1)
| ~ s_e(sK1,s(sK0,sK1),X0,sK1) ),
inference(instantiation,[status(thm)],[c_687089]) ).
tcf(c_879035,plain,
s_e(sK1,s(sK0,sK1),s(sK0,sK1),sK1),
inference(instantiation,[status(thm)],[c_755718]) ).
tcf(c_879037,plain,
( s_t(sK2,sK0,sK1)
| s_t(sK1,sK2,sK0)
| s_t(sK0,sK1,sK2)
| ( s(sK0,sK1) = sK1 )
| ~ s_e(sK2,s(sK0,sK1),sK2,sK1)
| ~ s_e(sK0,s(sK0,sK1),sK0,sK1)
| ~ s_e(sK1,s(sK0,sK1),s(sK0,sK1),sK1) ),
inference(instantiation,[status(thm)],[c_799603]) ).
tcf(c_879038,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_879037,c_879035,c_98499,c_33824,c_31396,c_31395,c_6413,c_6399,c_6397,c_6376,c_49,c_50]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GEO521+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.02 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 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:17:06 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.03/0.31 Running first-order theorem proving
% 0.03/0.31 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.32
% 0.03/0.32 % ======== iProver multi-core TPTP/SMT =========
% 0.03/0.32
% 0.03/0.32 % Detected problem language: tptp
% 0.07/0.33 % Proving...
% 220.65/34.18 % SZS status Started for theBenchmark.p
% 220.65/34.18 % SZS status Theorem for theBenchmark.p
% 220.65/34.18
% 220.65/34.18 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 220.65/34.18
% 220.65/34.18 % ------ iProver source info
% 220.65/34.18
% 220.65/34.18 % git: date: 2026-07-19 20:42:38 +0200
% 220.65/34.18 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 220.65/34.18 % git: non_committed_changes: false
% 220.65/34.18
% 220.65/34.18 % ------ Parsing...
% 220.65/34.18 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 220.65/34.18
% 220.65/34.18 % ------ Preprocessing... sup_sim: 0 sf_s rm: 19 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 3 0s sf_e pe_s pe_e %
% 220.65/34.18
% 220.65/34.18 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 220.65/34.18
% 220.65/34.18 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 220.65/34.18 % ------ Proving...
% 220.65/34.18 % ------ Problem Properties
% 220.65/34.18
% 220.65/34.18 %
% 220.65/34.18 % clauses 126
% 220.65/34.18 % conjectures 4
% 220.65/34.18 % EPR 104
% 220.65/34.18 % Horn 91
% 220.65/34.18 % unary 19
% 220.65/34.18 % binary 46
% 220.65/34.18 % lits 391
% 220.65/34.19 % lits eq 78
% 220.65/34.19 % fd_pure 0
% 220.65/34.19 % fd_pseudo 0
% 220.65/34.19 % fd_cond 0
% 220.65/34.19 % fd_pseudo_cond 47
% 220.65/34.19 % AC symbols 0
% 220.65/34.19
% 220.65/34.19 % ------ Schedule dynamic 5 is on
% 220.65/34.19
% 220.65/34.19 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 220.65/34.19
% 220.65/34.19
% 220.65/34.19 % ------
% 220.65/34.19 % Current options:
% 220.65/34.19 % ------
% 220.65/34.19
% 220.65/34.19
% 220.65/34.19 %
% 220.65/34.19
% 220.65/34.19 % ------ Proving...
% 220.65/34.19 % Proof_search_loop: time out after: 5658 full_loop iterations
% 220.65/34.19
% 220.65/34.19 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" Time Limit: 15.
% 220.65/34.19
% 220.65/34.19
% 220.65/34.19 % ------
% 220.65/34.19 % Current options:
% 220.65/34.19 % ------
% 220.65/34.19
% 220.65/34.19
% 220.65/34.19 %
% 220.65/34.19
% 220.65/34.19 % ------ Proving...
% 220.65/34.19 % Proof_search_loop: time out after: 8863 full_loop iterations
% 220.65/34.19
% 220.65/34.19 % ------ Option_1: Negative Selections Time Limit: 35.
% 220.65/34.19
% 220.65/34.19
% 220.65/34.19 % ------
% 220.65/34.19 % Current options:
% 220.65/34.19 % ------
% 220.65/34.19
% 220.65/34.19
% 220.65/34.19 %
% 220.65/34.19
% 220.65/34.19 % ------ Proving...
% 220.65/34.19 %
% 220.65/34.19
% 220.65/34.19 % SZS status Theorem for theBenchmark.p
% 220.65/34.19
% 220.65/34.19 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 220.65/34.19
% 220.65/34.19
%------------------------------------------------------------------------------