%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : GEO499+1 : TPTP v9.2.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:21:25 PM UTC 2026
% Result : Theorem 10.53s 6.98s
% Output : CNFRefutation 10.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 19
% Syntax : Number of formulae : 131 ( 21 unt; 0 def)
% Number of atoms : 386 ( 89 equ)
% Maximal formula atoms : 15 ( 2 avg)
% Number of connectives : 430 ( 175 ~; 216 |; 39 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-4 aty)
% Number of functors : 10 ( 10 usr; 7 con; 0-4 aty)
% Number of variables : 358 ( 10 sgn 174 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d_Defn6_1,axiom,
! [X12,X13,X15] :
( ( ~ sameside(X12,X13,X15)
| X12 != X13 )
& ( ~ sameside(X12,X13,X15)
| X15 != X13 )
& ( ~ sameside(X12,X13,X15)
| s_t(X13,X12,X15)
| s_t(X13,X15,X12) )
& ( ~ s_t(X13,X12,X15)
| X12 = X13
| xb = X13
| sameside(X12,X13,X15) )
& ( ~ s_t(X13,X15,X12)
| X12 = X13
| X15 = X13
| sameside(X12,X13,X15) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d_Defn6_1) ).
fof(aSatz6_4a,axiom,
! [X12,X13,X15] :
( ( ~ sameside(X12,X13,X15)
| s_col(X12,X13,X15) )
& ( ~ sameside(X12,X13,X15)
| ~ s_t(X12,X13,X15) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz6_4a) ).
fof(aA4,axiom,
! [X1,X2,X7,X4] :
( s_t(X1,X2,ext(X1,X2,X7,X4))
& s_e(X2,ext(X1,X2,X7,X4),X7,X4) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO011+0.ax',aA4) ).
fof(aSatz3_6a,axiom,
! [X12,X15,X14,X17] :
( ~ s_t(X12,X15,X14)
| ~ s_t(X12,X14,X17)
| s_t(X15,X14,X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz3_6a) ).
fof(aA3,axiom,
! [X1,X2,X3] :
( ~ s_e(X1,X2,X3,X3)
| X1 = X2 ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO011+0.ax',aA3) ).
fof(aSatz7_15a,axiom,
! [X13,X16,X27,X12] :
( ~ s_t(X13,X16,X27)
| s_t(s(X12,X13),s(X12,X16),s(X12,X27)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz7_15a) ).
fof(aSatz7_7,axiom,
! [X12,X13] : s(X12,s(X12,X13)) = X13,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz7_7) ).
fof(aSatz3_2,axiom,
! [X12,X15,X14] :
( ~ s_t(X12,X15,X14)
| s_t(X14,X15,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz3_2) ).
fof(aSatz3_6b,axiom,
! [X12,X15,X14,X17] :
( ~ s_t(X12,X15,X14)
| ~ s_t(X12,X14,X17)
| s_t(X12,X15,X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz3_6b) ).
fof(d_Defn5_4,axiom,
! [X12,X15,X14,X17,X2] :
( ( ~ le(X12,X15,X14,X17)
| s_t(X14,insert(X12,X15,X14,X17),X17) )
& ( ~ le(X12,X15,X14,X17)
| s_e(X12,X15,X14,insert(X12,X15,X14,X17)) )
& ( ~ s_t(X14,X2,X17)
| ~ s_e(X12,X15,X14,X2)
| le(X12,X15,X14,X17) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d_Defn5_4) ).
fof(d_Defn7_1,axiom,
! [X12,X29,X15] :
( ( ~ s_m(X12,X29,X15)
| s_t(X12,X29,X15) )
& ( ~ s_m(X12,X29,X15)
| s_e(X29,X12,X29,X15) )
& ( ~ s_t(X12,X29,X15)
| ~ s_e(X29,X12,X29,X15)
| s_m(X12,X29,X15) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d_Defn7_1) ).
fof(d_insert,axiom,
! [X12,X15,X20,X22] : insert(X12,X15,X20,X22) = ext(ext(X22,X20,alpha,gamma),X20,X12,X15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d_insert) ).
fof(aSatz5_12a1,axiom,
! [X12,X15,X14] :
( ~ s_col(X12,X15,X14)
| ~ s_t(X12,X15,X14)
| le(X12,X15,X12,X14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz5_12a1) ).
fof(d_Defn4_10,axiom,
! [X12,X15,X14] :
( ( ~ s_col(X12,X15,X14)
| s_t(X12,X15,X14)
| s_t(X15,X14,X12)
| s_t(X14,X12,X15) )
& ( s_col(X12,X15,X14)
| ~ s_t(X12,X15,X14) )
& ( s_col(X12,X15,X14)
| ~ s_t(X15,X14,X12) )
& ( s_col(X12,X15,X14)
| ~ s_t(X14,X12,X15) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d_Defn4_10) ).
fof(aSatz3_3,axiom,
! [X20,X21] : s_t(X20,X20,X21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz3_3) ).
fof(aSatz7_4b,axiom,
! [X13,X12,X27,X16] :
( ~ s_m(X13,X12,X27)
| ~ s_m(X13,X12,X16)
| X27 = X16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz7_4b) ).
fof(aSatz7_15b,conjecture,
! [X13,X16,X27,X12] :
( s_t(X13,X16,X27)
| ~ s_t(s(X12,X13),s(X12,X16),s(X12,X27)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz7_15b) ).
fof(aSatz3_5a,axiom,
! [X12,X15,X17,X14] :
( ~ s_t(X12,X15,X17)
| ~ s_t(X15,X14,X17)
| s_t(X12,X15,X14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz3_5a) ).
fof(aSatz3_1,axiom,
! [X12,X15] : s_t(X12,X15,X15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz3_1) ).
fof(c_0_19,plain,
! [X12,X13,X15] :
( ( ~ sameside(X12,X13,X15)
| X12 != X13 )
& ( ~ sameside(X12,X13,X15)
| X15 != X13 )
& ( ~ sameside(X12,X13,X15)
| s_t(X13,X12,X15)
| s_t(X13,X15,X12) )
& ( ~ s_t(X13,X12,X15)
| X12 = X13
| xb = X13
| sameside(X12,X13,X15) )
& ( ~ s_t(X13,X15,X12)
| X12 = X13
| X15 = X13
| sameside(X12,X13,X15) ) ),
inference(fof_simplification,[status(thm)],[d_Defn6_1]) ).
fof(c_0_20,plain,
! [X12,X13,X15] :
( ( ~ sameside(X12,X13,X15)
| s_col(X12,X13,X15) )
& ( ~ sameside(X12,X13,X15)
| ~ s_t(X12,X13,X15) ) ),
inference(fof_simplification,[status(thm)],[aSatz6_4a]) ).
fof(c_0_21,plain,
! [X919,X920,X921] :
( ( ~ sameside(X919,X920,X921)
| X919 != X920 )
& ( ~ sameside(X919,X920,X921)
| X921 != X920 )
& ( ~ sameside(X919,X920,X921)
| s_t(X920,X919,X921)
| s_t(X920,X921,X919) )
& ( ~ s_t(X920,X919,X921)
| X919 = X920
| xb = X920
| sameside(X919,X920,X921) )
& ( ~ s_t(X920,X921,X919)
| X919 = X920
| X921 = X920
| sameside(X919,X920,X921) ) ),
inference(variable_rename,[status(thm)],[c_0_19]) ).
fof(c_0_22,plain,
! [X497,X498,X499,X500] :
( s_t(X497,X498,ext(X497,X498,X499,X500))
& s_e(X498,ext(X497,X498,X499,X500),X499,X500) ),
inference(variable_rename,[status(thm)],[aA4]) ).
fof(c_0_23,plain,
! [X12,X15,X14,X17] :
( ~ s_t(X12,X15,X14)
| ~ s_t(X12,X14,X17)
| s_t(X15,X14,X17) ),
inference(fof_simplification,[status(thm)],[aSatz3_6a]) ).
fof(c_0_24,plain,
! [X757,X758,X759] :
( ( ~ sameside(X757,X758,X759)
| s_col(X757,X758,X759) )
& ( ~ sameside(X757,X758,X759)
| ~ s_t(X757,X758,X759) ) ),
inference(variable_rename,[status(thm)],[c_0_20]) ).
cnf(c_0_25,plain,
( X3 = X1
| X2 = X1
| sameside(X3,X1,X2)
| ~ s_t(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_21]) ).
cnf(c_0_26,plain,
s_t(X1,X2,ext(X1,X2,X3,X4)),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
fof(c_0_27,plain,
! [X576,X577,X578,X579] :
( ~ s_t(X576,X577,X578)
| ~ s_t(X576,X578,X579)
| s_t(X577,X578,X579) ),
inference(variable_rename,[status(thm)],[c_0_23]) ).
fof(c_0_28,plain,
! [X1,X2,X3] :
( ~ s_e(X1,X2,X3,X3)
| X1 = X2 ),
inference(fof_simplification,[status(thm)],[aA3]) ).
cnf(c_0_29,plain,
( ~ sameside(X1,X2,X3)
| ~ s_t(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_24]) ).
cnf(c_0_30,plain,
( ext(X1,X2,X3,X4) = X1
| X1 = X2
| sameside(ext(X1,X2,X3,X4),X1,X2) ),
inference(spm,[status(thm)],[c_0_25,c_0_26]) ).
cnf(c_0_31,plain,
( s_t(X2,X3,X4)
| ~ s_t(X1,X2,X3)
| ~ s_t(X1,X3,X4) ),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
fof(c_0_32,plain,
! [X494,X495,X496] :
( ~ s_e(X494,X495,X496,X496)
| X494 = X495 ),
inference(variable_rename,[status(thm)],[c_0_28]) ).
fof(c_0_33,plain,
! [X13,X16,X27,X12] :
( ~ s_t(X13,X16,X27)
| s_t(s(X12,X13),s(X12,X16),s(X12,X27)) ),
inference(fof_simplification,[status(thm)],[aSatz7_15a]) ).
cnf(c_0_34,plain,
( ext(X1,X2,X3,X4) = X1
| X1 = X2
| ~ s_t(ext(X1,X2,X3,X4),X1,X2) ),
inference(spm,[status(thm)],[c_0_29,c_0_30]) ).
cnf(c_0_35,plain,
( s_t(X1,X2,ext(X3,X2,X4,X5))
| ~ s_t(X3,X1,X2) ),
inference(spm,[status(thm)],[c_0_31,c_0_26]) ).
cnf(c_0_36,plain,
( X1 = X2
| ~ s_e(X1,X2,X3,X3) ),
inference(split_conjunct,[status(thm)],[c_0_32]) ).
cnf(c_0_37,plain,
s_e(X1,ext(X2,X1,X3,X4),X3,X4),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
fof(c_0_38,plain,
! [X869,X870,X871,X872] :
( ~ s_t(X869,X870,X871)
| s_t(s(X872,X869),s(X872,X870),s(X872,X871)) ),
inference(variable_rename,[status(thm)],[c_0_33]) ).
fof(c_0_39,plain,
! [X853,X854] : s(X853,s(X853,X854)) = X854,
inference(variable_rename,[status(thm)],[aSatz7_7]) ).
fof(c_0_40,plain,
! [X12,X15,X14] :
( ~ s_t(X12,X15,X14)
| s_t(X14,X15,X12) ),
inference(fof_simplification,[status(thm)],[aSatz3_2]) ).
cnf(c_0_41,plain,
( ext(X1,ext(X2,X1,X3,X4),X5,X6) = X1
| ext(X2,X1,X3,X4) = X1
| ~ s_t(X2,ext(X1,ext(X2,X1,X3,X4),X5,X6),X1) ),
inference(spm,[status(thm)],[c_0_34,c_0_35]) ).
cnf(c_0_42,plain,
ext(X1,X2,X3,X3) = X2,
inference(spm,[status(thm)],[c_0_36,c_0_37]) ).
cnf(c_0_43,plain,
( s_t(s(X4,X1),s(X4,X2),s(X4,X3))
| ~ s_t(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_44,plain,
s(X1,s(X1,X2)) = X2,
inference(split_conjunct,[status(thm)],[c_0_39]) ).
fof(c_0_45,plain,
! [X564,X565,X566] :
( ~ s_t(X564,X565,X566)
| s_t(X566,X565,X564) ),
inference(variable_rename,[status(thm)],[c_0_40]) ).
fof(c_0_46,plain,
! [X12,X15,X14,X17] :
( ~ s_t(X12,X15,X14)
| ~ s_t(X12,X14,X17)
| s_t(X12,X15,X17) ),
inference(fof_simplification,[status(thm)],[aSatz3_6b]) ).
cnf(c_0_47,plain,
( ext(X1,X2,X3,X4) = X2
| ~ s_t(X1,ext(X1,X2,X3,X4),X2) ),
inference(spm,[status(thm)],[c_0_41,c_0_42]) ).
cnf(c_0_48,plain,
( s_t(s(X1,X2),X3,s(X1,X4))
| ~ s_t(X2,s(X1,X3),X4) ),
inference(spm,[status(thm)],[c_0_43,c_0_44]) ).
cnf(c_0_49,plain,
( s_t(X3,X2,X1)
| ~ s_t(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_45]) ).
fof(c_0_50,plain,
! [X588,X589,X590,X591] :
( ~ s_t(X588,X589,X590)
| ~ s_t(X588,X590,X591)
| s_t(X588,X589,X591) ),
inference(variable_rename,[status(thm)],[c_0_46]) ).
fof(c_0_51,plain,
! [X12,X15,X14,X17,X2] :
( ( ~ le(X12,X15,X14,X17)
| s_t(X14,insert(X12,X15,X14,X17),X17) )
& ( ~ le(X12,X15,X14,X17)
| s_e(X12,X15,X14,insert(X12,X15,X14,X17)) )
& ( ~ s_t(X14,X2,X17)
| ~ s_e(X12,X15,X14,X2)
| le(X12,X15,X14,X17) ) ),
inference(fof_simplification,[status(thm)],[d_Defn5_4]) ).
fof(c_0_52,plain,
! [X12,X29,X15] :
( ( ~ s_m(X12,X29,X15)
| s_t(X12,X29,X15) )
& ( ~ s_m(X12,X29,X15)
| s_e(X29,X12,X29,X15) )
& ( ~ s_t(X12,X29,X15)
| ~ s_e(X29,X12,X29,X15)
| s_m(X12,X29,X15) ) ),
inference(fof_simplification,[status(thm)],[d_Defn7_1]) ).
cnf(c_0_53,plain,
( ext(s(X1,X2),s(X1,X3),X4,X5) = s(X1,X3)
| ~ s_t(X2,s(X1,ext(s(X1,X2),s(X1,X3),X4,X5)),X3) ),
inference(spm,[status(thm)],[c_0_47,c_0_48]) ).
cnf(c_0_54,plain,
( s_t(s(X1,X2),s(X1,X3),s(X1,X4))
| ~ s_t(X4,X3,X2) ),
inference(spm,[status(thm)],[c_0_49,c_0_43]) ).
cnf(c_0_55,plain,
( s_t(X1,X2,X4)
| ~ s_t(X1,X2,X3)
| ~ s_t(X1,X3,X4) ),
inference(split_conjunct,[status(thm)],[c_0_50]) ).
fof(c_0_56,plain,
! [X914,X915,X916,X917,X918] :
( ( ~ le(X914,X915,X916,X917)
| s_t(X916,insert(X914,X915,X916,X917),X917) )
& ( ~ le(X914,X915,X916,X917)
| s_e(X914,X915,X916,insert(X914,X915,X916,X917)) )
& ( ~ s_t(X916,X918,X917)
| ~ s_e(X914,X915,X916,X918)
| le(X914,X915,X916,X917) ) ),
inference(variable_rename,[status(thm)],[c_0_51]) ).
fof(c_0_57,plain,
! [X877,X878,X879,X880] : insert(X877,X878,X879,X880) = ext(ext(X880,X879,alpha,gamma),X879,X877,X878),
inference(variable_rename,[status(thm)],[d_insert]) ).
fof(c_0_58,plain,
! [X922,X923,X924] :
( ( ~ s_m(X922,X923,X924)
| s_t(X922,X923,X924) )
& ( ~ s_m(X922,X923,X924)
| s_e(X923,X922,X923,X924) )
& ( ~ s_t(X922,X923,X924)
| ~ s_e(X923,X922,X923,X924)
| s_m(X922,X923,X924) ) ),
inference(variable_rename,[status(thm)],[c_0_52]) ).
cnf(c_0_59,plain,
( ext(X1,X2,X3,X4) = X2
| ~ s_t(X2,ext(X1,X2,X3,X4),X1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_53,c_0_54]),c_0_44]),c_0_44]),c_0_44]),c_0_44]),c_0_44]) ).
cnf(c_0_60,plain,
( s_t(X1,X2,ext(X1,X3,X4,X5))
| ~ s_t(X1,X2,X3) ),
inference(spm,[status(thm)],[c_0_55,c_0_26]) ).
cnf(c_0_61,plain,
( s_t(X3,insert(X1,X2,X3,X4),X4)
| ~ le(X1,X2,X3,X4) ),
inference(split_conjunct,[status(thm)],[c_0_56]) ).
cnf(c_0_62,plain,
insert(X1,X2,X3,X4) = ext(ext(X4,X3,alpha,gamma),X3,X1,X2),
inference(split_conjunct,[status(thm)],[c_0_57]) ).
fof(c_0_63,plain,
! [X12,X15,X14] :
( ~ s_col(X12,X15,X14)
| ~ s_t(X12,X15,X14)
| le(X12,X15,X12,X14) ),
inference(fof_simplification,[status(thm)],[aSatz5_12a1]) ).
fof(c_0_64,plain,
! [X12,X15,X14] :
( ( ~ s_col(X12,X15,X14)
| s_t(X12,X15,X14)
| s_t(X15,X14,X12)
| s_t(X14,X12,X15) )
& ( s_col(X12,X15,X14)
| ~ s_t(X12,X15,X14) )
& ( s_col(X12,X15,X14)
| ~ s_t(X15,X14,X12) )
& ( s_col(X12,X15,X14)
| ~ s_t(X14,X12,X15) ) ),
inference(fof_simplification,[status(thm)],[d_Defn4_10]) ).
cnf(c_0_65,plain,
( s_m(X1,X2,X3)
| ~ s_t(X1,X2,X3)
| ~ s_e(X2,X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_58]) ).
cnf(c_0_66,plain,
( ext(ext(X1,X2,X3,X4),X1,X5,X6) = X1
| ~ s_t(X1,ext(ext(X1,X2,X3,X4),X1,X5,X6),X2) ),
inference(spm,[status(thm)],[c_0_59,c_0_60]) ).
cnf(c_0_67,plain,
( s_t(X3,ext(ext(X4,X3,alpha,gamma),X3,X1,X2),X4)
| ~ le(X1,X2,X3,X4) ),
inference(rw,[status(thm)],[c_0_61,c_0_62]) ).
fof(c_0_68,plain,
! [X567,X568] : s_t(X567,X567,X568),
inference(variable_rename,[status(thm)],[aSatz3_3]) ).
fof(c_0_69,plain,
! [X730,X731,X732] :
( ~ s_col(X730,X731,X732)
| ~ s_t(X730,X731,X732)
| le(X730,X731,X730,X732) ),
inference(variable_rename,[status(thm)],[c_0_63]) ).
fof(c_0_70,plain,
! [X903,X904,X905] :
( ( ~ s_col(X903,X904,X905)
| s_t(X903,X904,X905)
| s_t(X904,X905,X903)
| s_t(X905,X903,X904) )
& ( s_col(X903,X904,X905)
| ~ s_t(X903,X904,X905) )
& ( s_col(X903,X904,X905)
| ~ s_t(X904,X905,X903) )
& ( s_col(X903,X904,X905)
| ~ s_t(X905,X903,X904) ) ),
inference(variable_rename,[status(thm)],[c_0_64]) ).
fof(c_0_71,plain,
! [X13,X12,X27,X16] :
( ~ s_m(X13,X12,X27)
| ~ s_m(X13,X12,X16)
| X27 = X16 ),
inference(fof_simplification,[status(thm)],[aSatz7_4b]) ).
cnf(c_0_72,plain,
( s_m(ext(X1,X2,X2,X3),X2,X3)
| ~ s_t(ext(X1,X2,X2,X3),X2,X3) ),
inference(spm,[status(thm)],[c_0_65,c_0_37]) ).
cnf(c_0_73,plain,
( ext(ext(X1,X1,alpha,gamma),X1,X2,X3) = X1
| ~ le(X2,X3,X1,X1) ),
inference(spm,[status(thm)],[c_0_66,c_0_67]) ).
cnf(c_0_74,plain,
s_t(X1,X1,X2),
inference(split_conjunct,[status(thm)],[c_0_68]) ).
cnf(c_0_75,plain,
( le(X1,X2,X1,X3)
| ~ s_col(X1,X2,X3)
| ~ s_t(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_69]) ).
cnf(c_0_76,plain,
( s_col(X1,X2,X3)
| ~ s_t(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_70]) ).
fof(c_0_77,plain,
! [X846,X847,X848,X849] :
( ~ s_m(X846,X847,X848)
| ~ s_m(X846,X847,X849)
| X848 = X849 ),
inference(variable_rename,[status(thm)],[c_0_71]) ).
cnf(c_0_78,plain,
( s_m(X1,X1,X2)
| ~ le(X1,X2,X1,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_72,c_0_73]),c_0_74])]) ).
cnf(c_0_79,plain,
( le(X1,X2,X1,X3)
| ~ s_t(X1,X2,X3) ),
inference(csr,[status(thm)],[c_0_75,c_0_76]) ).
cnf(c_0_80,plain,
( X3 = X4
| ~ s_m(X1,X2,X3)
| ~ s_m(X1,X2,X4) ),
inference(split_conjunct,[status(thm)],[c_0_77]) ).
cnf(c_0_81,plain,
( s_m(X1,X1,X2)
| ~ s_t(X1,X2,X1) ),
inference(spm,[status(thm)],[c_0_78,c_0_79]) ).
cnf(c_0_82,plain,
( X1 = X2
| ~ s_m(X3,X3,X1)
| ~ s_t(X3,X2,X3) ),
inference(spm,[status(thm)],[c_0_80,c_0_81]) ).
fof(c_0_83,negated_conjecture,
~ ! [X13,X16,X27,X12] :
( s_t(X13,X16,X27)
| ~ s_t(s(X12,X13),s(X12,X16),s(X12,X27)) ),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[aSatz7_15b])]) ).
cnf(c_0_84,plain,
( X1 = X2
| ~ s_t(X3,X2,X3)
| ~ s_t(X3,X1,X3) ),
inference(spm,[status(thm)],[c_0_82,c_0_81]) ).
fof(c_0_85,negated_conjecture,
( ~ s_t(esk1_0,esk2_0,esk3_0)
& s_t(s(esk4_0,esk1_0),s(esk4_0,esk2_0),s(esk4_0,esk3_0)) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_83])])]) ).
cnf(c_0_86,plain,
( X1 = X2
| ~ s_t(s(X3,X4),X1,s(X3,X4))
| ~ s_t(X4,s(X3,X2),X4) ),
inference(spm,[status(thm)],[c_0_84,c_0_48]) ).
fof(c_0_87,plain,
! [X12,X15,X17,X14] :
( ~ s_t(X12,X15,X17)
| ~ s_t(X15,X14,X17)
| s_t(X12,X15,X14) ),
inference(fof_simplification,[status(thm)],[aSatz3_5a]) ).
cnf(c_0_88,plain,
( X2 = X1
| xb = X1
| sameside(X2,X1,X3)
| ~ s_t(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_21]) ).
cnf(c_0_89,negated_conjecture,
s_t(s(esk4_0,esk1_0),s(esk4_0,esk2_0),s(esk4_0,esk3_0)),
inference(split_conjunct,[status(thm)],[c_0_85]) ).
cnf(c_0_90,plain,
( X1 = X2
| ~ s_t(X3,s(X4,X2),X3)
| ~ s_t(X3,s(X4,X1),X3) ),
inference(spm,[status(thm)],[c_0_86,c_0_48]) ).
fof(c_0_91,plain,
! [X572,X573,X574,X575] :
( ~ s_t(X572,X573,X574)
| ~ s_t(X573,X575,X574)
| s_t(X572,X573,X575) ),
inference(variable_rename,[status(thm)],[c_0_87]) ).
cnf(c_0_92,plain,
( s(X1,X2) = s(X1,X3)
| s(X1,X2) = xb
| sameside(s(X1,X3),s(X1,X2),s(X1,X4))
| ~ s_t(X2,X3,X4) ),
inference(spm,[status(thm)],[c_0_88,c_0_43]) ).
cnf(c_0_93,negated_conjecture,
s_t(s(esk4_0,esk3_0),s(esk4_0,esk2_0),s(esk4_0,esk1_0)),
inference(spm,[status(thm)],[c_0_49,c_0_89]) ).
cnf(c_0_94,plain,
( X1 = X2
| ~ s_t(s(X3,X2),s(X3,X1),s(X3,X2)) ),
inference(spm,[status(thm)],[c_0_90,c_0_74]) ).
cnf(c_0_95,plain,
( s_t(X1,X2,X4)
| ~ s_t(X1,X2,X3)
| ~ s_t(X2,X4,X3) ),
inference(split_conjunct,[status(thm)],[c_0_91]) ).
cnf(c_0_96,negated_conjecture,
( s(X1,s(esk4_0,esk3_0)) = s(X1,s(esk4_0,esk2_0))
| s(X1,s(esk4_0,esk3_0)) = xb
| sameside(s(X1,s(esk4_0,esk2_0)),s(X1,s(esk4_0,esk3_0)),s(X1,s(esk4_0,esk1_0))) ),
inference(spm,[status(thm)],[c_0_92,c_0_93]) ).
cnf(c_0_97,plain,
( s(X1,X2) = X3
| ~ s_t(s(X1,X3),X2,s(X1,X3)) ),
inference(spm,[status(thm)],[c_0_94,c_0_44]) ).
cnf(c_0_98,negated_conjecture,
( s_t(X1,s(esk4_0,esk3_0),s(esk4_0,esk2_0))
| ~ s_t(X1,s(esk4_0,esk3_0),s(esk4_0,esk1_0)) ),
inference(spm,[status(thm)],[c_0_95,c_0_93]) ).
cnf(c_0_99,negated_conjecture,
( s_t(X1,s(esk4_0,esk2_0),s(esk4_0,esk1_0))
| ~ s_t(s(esk4_0,esk3_0),X1,s(esk4_0,esk2_0)) ),
inference(spm,[status(thm)],[c_0_31,c_0_93]) ).
cnf(c_0_100,plain,
( s_col(X1,X2,X3)
| ~ sameside(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_24]) ).
cnf(c_0_101,negated_conjecture,
( esk3_0 = xb
| esk3_0 = esk2_0
| sameside(esk2_0,esk3_0,esk1_0) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_96,c_0_44]),c_0_44]),c_0_44]),c_0_44]),c_0_44]),c_0_44]) ).
cnf(c_0_102,negated_conjecture,
( esk3_0 = esk2_0
| ~ s_t(s(esk4_0,esk2_0),s(esk4_0,esk3_0),s(esk4_0,esk1_0)) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_97,c_0_98]),c_0_44]) ).
cnf(c_0_103,plain,
( s_t(X1,s(X2,X3),s(X2,X4))
| ~ s_t(s(X2,X1),X3,X4) ),
inference(spm,[status(thm)],[c_0_43,c_0_44]) ).
cnf(c_0_104,negated_conjecture,
( s(X1,s(esk4_0,esk2_0)) = s(X1,s(esk4_0,esk1_0))
| s(X1,s(esk4_0,esk1_0)) = xb
| sameside(s(X1,s(esk4_0,esk2_0)),s(X1,s(esk4_0,esk1_0)),s(X1,s(esk4_0,esk3_0))) ),
inference(spm,[status(thm)],[c_0_92,c_0_89]) ).
cnf(c_0_105,negated_conjecture,
( s_t(X1,s(esk4_0,esk1_0),s(esk4_0,esk2_0))
| ~ s_t(X1,s(esk4_0,esk1_0),s(esk4_0,esk3_0)) ),
inference(spm,[status(thm)],[c_0_95,c_0_89]) ).
cnf(c_0_106,plain,
( s(X1,X2) = X3
| ~ s_t(X2,s(X1,X3),X2) ),
inference(spm,[status(thm)],[c_0_86,c_0_74]) ).
cnf(c_0_107,negated_conjecture,
( s_t(s(esk4_0,X1),s(esk4_0,esk2_0),s(esk4_0,esk1_0))
| ~ s_t(esk3_0,X1,esk2_0) ),
inference(spm,[status(thm)],[c_0_99,c_0_43]) ).
cnf(c_0_108,plain,
( s_t(X1,X2,X3)
| s_t(X2,X3,X1)
| s_t(X3,X1,X2)
| ~ s_col(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_70]) ).
cnf(c_0_109,negated_conjecture,
( esk3_0 = esk2_0
| esk3_0 = xb
| s_col(esk2_0,esk3_0,esk1_0) ),
inference(spm,[status(thm)],[c_0_100,c_0_101]) ).
cnf(c_0_110,negated_conjecture,
~ s_t(esk1_0,esk2_0,esk3_0),
inference(split_conjunct,[status(thm)],[c_0_85]) ).
cnf(c_0_111,negated_conjecture,
( esk3_0 = esk2_0
| ~ s_t(esk2_0,esk3_0,esk1_0) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_102,c_0_103]),c_0_44]) ).
cnf(c_0_112,plain,
( s_t(X2,X1,X3)
| s_t(X2,X3,X1)
| ~ sameside(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_21]) ).
cnf(c_0_113,negated_conjecture,
( esk1_0 = xb
| esk2_0 = esk1_0
| sameside(esk2_0,esk1_0,esk3_0) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_104,c_0_44]),c_0_44]),c_0_44]),c_0_44]),c_0_44]),c_0_44]) ).
cnf(c_0_114,negated_conjecture,
( s_t(s(esk4_0,X1),s(esk4_0,esk1_0),s(esk4_0,esk2_0))
| ~ s_t(X1,esk1_0,esk3_0) ),
inference(spm,[status(thm)],[c_0_105,c_0_43]) ).
cnf(c_0_115,negated_conjecture,
( esk2_0 = esk1_0
| ~ s_t(esk3_0,esk1_0,esk2_0) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_106,c_0_107]),c_0_44]) ).
cnf(c_0_116,negated_conjecture,
( esk3_0 = xb
| esk3_0 = esk2_0
| s_t(esk3_0,esk1_0,esk2_0) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_108,c_0_109]),c_0_110]),c_0_111]) ).
fof(c_0_117,plain,
! [X562,X563] : s_t(X562,X563,X563),
inference(variable_rename,[status(thm)],[aSatz3_1]) ).
cnf(c_0_118,negated_conjecture,
( esk3_0 = esk2_0
| ~ s_t(esk1_0,esk3_0,esk2_0) ),
inference(spm,[status(thm)],[c_0_102,c_0_54]) ).
cnf(c_0_119,negated_conjecture,
( esk2_0 = esk1_0
| esk1_0 = xb
| s_t(esk1_0,esk3_0,esk2_0) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_112,c_0_113]),c_0_110]) ).
cnf(c_0_120,negated_conjecture,
( s_t(s(esk4_0,esk1_0),s(esk4_0,esk2_0),s(esk4_0,esk1_0))
| ~ s_t(esk3_0,esk1_0,esk3_0) ),
inference(spm,[status(thm)],[c_0_99,c_0_114]) ).
cnf(c_0_121,negated_conjecture,
( esk3_0 = esk2_0
| esk3_0 = xb
| esk2_0 = esk1_0 ),
inference(spm,[status(thm)],[c_0_115,c_0_116]) ).
cnf(c_0_122,plain,
s_t(X1,X2,X2),
inference(split_conjunct,[status(thm)],[c_0_117]) ).
cnf(c_0_123,negated_conjecture,
( esk1_0 = xb
| esk2_0 = esk1_0
| esk3_0 = esk2_0 ),
inference(spm,[status(thm)],[c_0_118,c_0_119]) ).
cnf(c_0_124,negated_conjecture,
( esk2_0 = esk1_0
| ~ s_t(esk3_0,esk1_0,esk3_0) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_106,c_0_120]),c_0_44]) ).
cnf(c_0_125,negated_conjecture,
( esk2_0 = esk1_0
| esk3_0 = xb ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_110,c_0_121]),c_0_122])]) ).
cnf(c_0_126,negated_conjecture,
( esk2_0 = esk1_0
| esk1_0 = xb ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_110,c_0_123]),c_0_122])]) ).
cnf(c_0_127,negated_conjecture,
( esk2_0 = esk1_0
| ~ s_t(xb,esk1_0,xb) ),
inference(spm,[status(thm)],[c_0_124,c_0_125]) ).
cnf(c_0_128,negated_conjecture,
esk1_0 = xb,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_110,c_0_126]),c_0_74])]) ).
cnf(c_0_129,negated_conjecture,
esk2_0 = xb,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_127,c_0_128]),c_0_128]),c_0_74])]) ).
cnf(c_0_130,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_110,c_0_128]),c_0_129]),c_0_74])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : GEO499+1 : TPTP v9.2.1. Released v7.0.0.
% 0.00/0.11 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.32 % Computer : n004.cluster.edu
% 0.15/0.32 % Model : x86_64 x86_64
% 0.15/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.32 % Memory : 8042.1875MB
% 0.15/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.32 % CPULimit : 300
% 0.15/0.32 % WCLimit : 300
% 0.15/0.32 % DateTime : Mon May 4 17:59:47 EDT 2026
% 0.15/0.32 % CPUTime :
% 0.15/0.33 % start to proof: theBenchmark
% 10.53/6.98 % Version : CSE_E---1.7
% 10.53/6.98 % Problem : theBenchmark.p
% 10.53/6.98 % SZS status Theorem for theBenchmark.p
% 10.53/6.98 % SZS output start CNFRefutation
% See solution above
% 10.53/7.02 % Total time : 5.376s
%------------------------------------------------------------------------------