%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : GEO495+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 : n026.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:24 PM UTC 2026
% Result : Theorem 123.55s 99.82s
% Output : CNFRefutation 123.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 28
% Syntax : Number of formulae : 180 ( 68 unt; 0 def)
% Number of atoms : 428 ( 62 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 451 ( 203 ~; 220 |; 28 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-6 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-4 aty)
% Number of variables : 506 ( 15 sgn 295 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
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(aA1,axiom,
! [X1,X2] : s_e(X1,X2,X2,X1),
file('/export/starexec/sandbox/benchmark/Axioms/GEO011+0.ax',aA1) ).
fof(aSatz4_5,axiom,
! [X12,X15,X14,X20,X22] :
( ( ~ s_t(X12,X15,X14)
| ~ s_e(X12,X14,X20,X22)
| s_t(X20,insert(X12,X15,X20,X22),X22) )
& ( ~ s_t(X12,X15,X14)
| ~ s_e(X12,X14,X20,X22)
| s_e3(X12,X15,X14,X20,insert(X12,X15,X20,X22),X22) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz4_5) ).
fof(aSatz5_8,axiom,
! [X12,X15,X14,X17,X18,X19] :
( ~ le(X12,X15,X14,X17)
| ~ le(X14,X17,X18,X19)
| le(X12,X15,X18,X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz5_8) ).
fof(aSatz3_1,axiom,
! [X12,X15] : s_t(X12,X15,X15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz3_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(aSatz2_12,axiom,
! [X16,X12,X17,X15,X14] :
( X16 = X12
| ~ s_t(X16,X12,X17)
| ~ s_e(X12,X17,X15,X14)
| X17 = ext(X16,X12,X15,X14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz2_12) ).
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(aSatz5_9,conjecture,
! [X12,X15,X14,X17] :
( ~ le(X12,X15,X14,X17)
| ~ le(X14,X17,X12,X15)
| s_e(X12,X15,X14,X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz5_9) ).
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(aSatz5_7,axiom,
! [X12,X15] : le(X12,X15,X12,X15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz5_7) ).
fof(aSatz2_1,axiom,
! [X12,X15] : s_e(X12,X15,X12,X15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz2_1) ).
fof(aSatz5_5a,axiom,
! [X12,X15,X14,X17] :
( ( ~ le(X12,X15,X14,X17)
| s_t(X12,X15,ins(X14,X17,X12,X15)) )
& ( ~ le(X12,X15,X14,X17)
| s_e(X12,ins(X14,X17,X12,X15),X14,X17) )
& ( ~ le(X12,X15,X14,X17)
| ins(X14,X17,X12,X15) = ext(X12,X15,insert(X12,X15,X14,X17),X17) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz5_5a) ).
fof(aSatz4_3,axiom,
! [X12,X15,X14,X20,X21,X22] :
( ~ s_t(X12,X15,X14)
| ~ s_t(X20,X21,X22)
| ~ s_e(X12,X14,X20,X22)
| ~ s_e(X15,X14,X21,X22)
| s_e(X12,X15,X20,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz4_3) ).
fof(aSatz3_14b,axiom,
! [X15,X12] : X15 != ext(X12,X15,alpha,gamma),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz3_14b) ).
fof(aSatz5_5b,axiom,
! [X12,X15,X14,X17,X18] :
( le(X12,X15,X14,X17)
| ~ s_t(X12,X15,X18)
| ~ s_e(X12,X18,X14,X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz5_5b) ).
fof(aSatz2_2,axiom,
! [X12,X15,X14,X17] :
( ~ s_e(X12,X15,X14,X17)
| s_e(X14,X17,X12,X15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz2_2) ).
fof(aSatz3_3,axiom,
! [X20,X21] : s_t(X20,X20,X21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz3_3) ).
fof(aSatz3_5b,axiom,
! [X12,X15,X17,X14] :
( ~ s_t(X12,X15,X17)
| ~ s_t(X15,X14,X17)
| s_t(X12,X14,X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz3_5b) ).
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(aSatz2_14,axiom,
! [X12,X15,X14,X17] :
( ~ s_e(X12,X15,X14,X17)
| s_e(X15,X12,X17,X14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz2_14) ).
fof(aA2,axiom,
! [X1,X2,X3,X4,X5,X6] :
( ~ s_e(X1,X2,X3,X4)
| ~ s_e(X1,X2,X5,X6)
| s_e(X3,X4,X5,X6) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO011+0.ax',aA2) ).
fof(aSatz3_7a,axiom,
! [X12,X15,X14,X17] :
( ~ s_t(X12,X15,X14)
| ~ s_t(X15,X14,X17)
| X15 = X14
| s_t(X12,X14,X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz3_7a) ).
fof(d_Defn4_4,axiom,
! [X20,X31,X32,X21,X33,X34] :
( ( ~ s_e3(X20,X31,X32,X21,X33,X34)
| s_e(X20,X31,X21,X33) )
& ( ~ s_e3(X20,X31,X32,X21,X33,X34)
| s_e(X20,X32,X21,X34) )
& ( ~ s_e3(X20,X31,X32,X21,X33,X34)
| s_e(X31,X32,X33,X34) )
& ( ~ s_e(X20,X31,X21,X33)
| ~ s_e(X20,X32,X21,X34)
| ~ s_e(X31,X32,X33,X34)
| s_e3(X20,X31,X32,X21,X33,X34) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d_Defn4_4) ).
fof(aSatz4_6,axiom,
! [X12,X15,X14,X20,X21,X22] :
( ~ s_t(X12,X15,X14)
| ~ s_e3(X12,X15,X14,X20,X21,X22)
| s_t(X20,X21,X22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz4_6) ).
fof(aSatz2_8,axiom,
! [X12,X15] : s_e(X12,X12,X15,X15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz2_8) ).
fof(aA6,axiom,
! [X1,X2] :
( ~ s_t(X1,X2,X1)
| X1 = X2 ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO011+0.ax',aA6) ).
fof(aSatz3_4,axiom,
! [X12,X15,X14] :
( ~ s_t(X12,X15,X14)
| ~ s_t(X15,X12,X14)
| X12 = X15 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSatz3_4) ).
fof(c_0_28,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_29,plain,
! [X588,X589,X590,X591,X592] :
( ( ~ le(X588,X589,X590,X591)
| s_t(X590,insert(X588,X589,X590,X591),X591) )
& ( ~ le(X588,X589,X590,X591)
| s_e(X588,X589,X590,insert(X588,X589,X590,X591)) )
& ( ~ s_t(X590,X592,X591)
| ~ s_e(X588,X589,X590,X592)
| le(X588,X589,X590,X591) ) ),
inference(variable_rename,[status(thm)],[c_0_28]) ).
fof(c_0_30,plain,
! [X314,X315] : s_e(X314,X315,X315,X314),
inference(variable_rename,[status(thm)],[aA1]) ).
fof(c_0_31,plain,
! [X12,X15,X14,X20,X22] :
( ( ~ s_t(X12,X15,X14)
| ~ s_e(X12,X14,X20,X22)
| s_t(X20,insert(X12,X15,X20,X22),X22) )
& ( ~ s_t(X12,X15,X14)
| ~ s_e(X12,X14,X20,X22)
| s_e3(X12,X15,X14,X20,insert(X12,X15,X20,X22),X22) ) ),
inference(fof_simplification,[status(thm)],[aSatz4_5]) ).
fof(c_0_32,plain,
! [X12,X15,X14,X17,X18,X19] :
( ~ le(X12,X15,X14,X17)
| ~ le(X14,X17,X18,X19)
| le(X12,X15,X18,X19) ),
inference(fof_simplification,[status(thm)],[aSatz5_8]) ).
cnf(c_0_33,plain,
( le(X4,X5,X1,X3)
| ~ s_t(X1,X2,X3)
| ~ s_e(X4,X5,X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
cnf(c_0_34,plain,
s_e(X1,X2,X2,X1),
inference(split_conjunct,[status(thm)],[c_0_30]) ).
fof(c_0_35,plain,
! [X390,X391] : s_t(X390,X391,X391),
inference(variable_rename,[status(thm)],[aSatz3_1]) ).
fof(c_0_36,plain,
! [X448,X449,X450,X451,X452] :
( ( ~ s_t(X448,X449,X450)
| ~ s_e(X448,X450,X451,X452)
| s_t(X451,insert(X448,X449,X451,X452),X452) )
& ( ~ s_t(X448,X449,X450)
| ~ s_e(X448,X450,X451,X452)
| s_e3(X448,X449,X450,X451,insert(X448,X449,X451,X452),X452) ) ),
inference(variable_rename,[status(thm)],[c_0_31]) ).
fof(c_0_37,plain,
! [X551,X552,X553,X554] : insert(X551,X552,X553,X554) = ext(ext(X554,X553,alpha,gamma),X553,X551,X552),
inference(variable_rename,[status(thm)],[d_insert]) ).
fof(c_0_38,plain,
! [X16,X12,X17,X15,X14] :
( X16 = X12
| ~ s_t(X16,X12,X17)
| ~ s_e(X12,X17,X15,X14)
| X17 = ext(X16,X12,X15,X14) ),
inference(fof_simplification,[status(thm)],[aSatz2_12]) ).
fof(c_0_39,plain,
! [X12,X15,X14] :
( ~ s_t(X12,X15,X14)
| s_t(X14,X15,X12) ),
inference(fof_simplification,[status(thm)],[aSatz3_2]) ).
fof(c_0_40,plain,
! [X541,X542,X543,X544,X545,X546] :
( ~ le(X541,X542,X543,X544)
| ~ le(X543,X544,X545,X546)
| le(X541,X542,X545,X546) ),
inference(variable_rename,[status(thm)],[c_0_32]) ).
cnf(c_0_41,plain,
( le(X1,X2,X2,X3)
| ~ s_t(X2,X1,X3) ),
inference(spm,[status(thm)],[c_0_33,c_0_34]) ).
cnf(c_0_42,plain,
s_t(X1,X2,X2),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
fof(c_0_43,negated_conjecture,
~ ! [X12,X15,X14,X17] :
( ~ le(X12,X15,X14,X17)
| ~ le(X14,X17,X12,X15)
| s_e(X12,X15,X14,X17) ),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[aSatz5_9])]) ).
cnf(c_0_44,plain,
( s_t(X4,insert(X1,X2,X4,X5),X5)
| ~ s_t(X1,X2,X3)
| ~ s_e(X1,X3,X4,X5) ),
inference(split_conjunct,[status(thm)],[c_0_36]) ).
cnf(c_0_45,plain,
insert(X1,X2,X3,X4) = ext(ext(X4,X3,alpha,gamma),X3,X1,X2),
inference(split_conjunct,[status(thm)],[c_0_37]) ).
fof(c_0_46,plain,
! [X325,X326,X327,X328] :
( s_t(X325,X326,ext(X325,X326,X327,X328))
& s_e(X326,ext(X325,X326,X327,X328),X327,X328) ),
inference(variable_rename,[status(thm)],[aA4]) ).
cnf(c_0_47,plain,
( s_t(X3,insert(X1,X2,X3,X4),X4)
| ~ le(X1,X2,X3,X4) ),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
fof(c_0_48,plain,
! [X539,X540] : le(X539,X540,X539,X540),
inference(variable_rename,[status(thm)],[aSatz5_7]) ).
fof(c_0_49,plain,
! [X372,X373,X374,X375,X376] :
( X372 = X373
| ~ s_t(X372,X373,X374)
| ~ s_e(X373,X374,X375,X376)
| X374 = ext(X372,X373,X375,X376) ),
inference(variable_rename,[status(thm)],[c_0_38]) ).
fof(c_0_50,plain,
! [X344,X345] : s_e(X344,X345,X344,X345),
inference(variable_rename,[status(thm)],[aSatz2_1]) ).
fof(c_0_51,plain,
! [X392,X393,X394] :
( ~ s_t(X392,X393,X394)
| s_t(X394,X393,X392) ),
inference(variable_rename,[status(thm)],[c_0_39]) ).
fof(c_0_52,plain,
! [X12,X15,X14,X17] :
( ( ~ le(X12,X15,X14,X17)
| s_t(X12,X15,ins(X14,X17,X12,X15)) )
& ( ~ le(X12,X15,X14,X17)
| s_e(X12,ins(X14,X17,X12,X15),X14,X17) )
& ( ~ le(X12,X15,X14,X17)
| ins(X14,X17,X12,X15) = ext(X12,X15,insert(X12,X15,X14,X17),X17) ) ),
inference(fof_simplification,[status(thm)],[aSatz5_5a]) ).
cnf(c_0_53,plain,
( le(X1,X2,X5,X6)
| ~ le(X1,X2,X3,X4)
| ~ le(X3,X4,X5,X6) ),
inference(split_conjunct,[status(thm)],[c_0_40]) ).
cnf(c_0_54,plain,
le(X1,X2,X2,X1),
inference(spm,[status(thm)],[c_0_41,c_0_42]) ).
fof(c_0_55,negated_conjecture,
( le(esk1_0,esk2_0,esk3_0,esk4_0)
& le(esk3_0,esk4_0,esk1_0,esk2_0)
& ~ s_e(esk1_0,esk2_0,esk3_0,esk4_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_43])])]) ).
cnf(c_0_56,plain,
( s_t(X4,ext(ext(X5,X4,alpha,gamma),X4,X1,X2),X5)
| ~ s_t(X1,X2,X3)
| ~ s_e(X1,X3,X4,X5) ),
inference(rw,[status(thm)],[c_0_44,c_0_45]) ).
cnf(c_0_57,plain,
s_e(X1,ext(X2,X1,X3,X4),X3,X4),
inference(split_conjunct,[status(thm)],[c_0_46]) ).
cnf(c_0_58,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_47,c_0_45]) ).
cnf(c_0_59,plain,
le(X1,X2,X1,X2),
inference(split_conjunct,[status(thm)],[c_0_48]) ).
cnf(c_0_60,plain,
( X1 = X2
| X3 = ext(X1,X2,X4,X5)
| ~ s_t(X1,X2,X3)
| ~ s_e(X2,X3,X4,X5) ),
inference(split_conjunct,[status(thm)],[c_0_49]) ).
cnf(c_0_61,plain,
s_e(X1,X2,X1,X2),
inference(split_conjunct,[status(thm)],[c_0_50]) ).
cnf(c_0_62,plain,
( s_t(X3,X2,X1)
| ~ s_t(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_51]) ).
cnf(c_0_63,plain,
s_t(X1,X2,ext(X1,X2,X3,X4)),
inference(split_conjunct,[status(thm)],[c_0_46]) ).
fof(c_0_64,plain,
! [X522,X523,X524,X525] :
( ( ~ le(X522,X523,X524,X525)
| s_t(X522,X523,ins(X524,X525,X522,X523)) )
& ( ~ le(X522,X523,X524,X525)
| s_e(X522,ins(X524,X525,X522,X523),X524,X525) )
& ( ~ le(X522,X523,X524,X525)
| ins(X524,X525,X522,X523) = ext(X522,X523,insert(X522,X523,X524,X525),X525) ) ),
inference(variable_rename,[status(thm)],[c_0_52]) ).
cnf(c_0_65,plain,
( le(X1,X2,X3,X4)
| ~ le(X1,X2,X4,X3) ),
inference(spm,[status(thm)],[c_0_53,c_0_54]) ).
cnf(c_0_66,negated_conjecture,
le(esk3_0,esk4_0,esk1_0,esk2_0),
inference(split_conjunct,[status(thm)],[c_0_55]) ).
fof(c_0_67,plain,
! [X12,X15,X14,X20,X21,X22] :
( ~ s_t(X12,X15,X14)
| ~ s_t(X20,X21,X22)
| ~ s_e(X12,X14,X20,X22)
| ~ s_e(X15,X14,X21,X22)
| s_e(X12,X15,X20,X21) ),
inference(fof_simplification,[status(thm)],[aSatz4_3]) ).
cnf(c_0_68,plain,
( s_t(X1,ext(ext(X2,X1,alpha,gamma),X1,X3,X4),X2)
| ~ s_t(X3,X4,ext(X5,X3,X1,X2)) ),
inference(spm,[status(thm)],[c_0_56,c_0_57]) ).
cnf(c_0_69,plain,
s_t(X1,ext(ext(X2,X1,alpha,gamma),X1,X1,X2),X2),
inference(spm,[status(thm)],[c_0_58,c_0_59]) ).
cnf(c_0_70,plain,
( ext(X1,X2,X2,X3) = X3
| X1 = X2
| ~ s_t(X1,X2,X3) ),
inference(spm,[status(thm)],[c_0_60,c_0_61]) ).
cnf(c_0_71,plain,
s_t(ext(X1,X2,X3,X4),X2,X1),
inference(spm,[status(thm)],[c_0_62,c_0_63]) ).
fof(c_0_72,plain,
! [X426,X427] : X426 != ext(X427,X426,alpha,gamma),
inference(variable_rename,[status(thm)],[aSatz3_14b]) ).
cnf(c_0_73,plain,
( s_t(X1,X2,ins(X3,X4,X1,X2))
| ~ le(X1,X2,X3,X4) ),
inference(split_conjunct,[status(thm)],[c_0_64]) ).
cnf(c_0_74,negated_conjecture,
le(esk3_0,esk4_0,esk2_0,esk1_0),
inference(spm,[status(thm)],[c_0_65,c_0_66]) ).
fof(c_0_75,plain,
! [X442,X443,X444,X445,X446,X447] :
( ~ s_t(X442,X443,X444)
| ~ s_t(X445,X446,X447)
| ~ s_e(X442,X444,X445,X447)
| ~ s_e(X443,X444,X446,X447)
| s_e(X442,X443,X445,X446) ),
inference(variable_rename,[status(thm)],[c_0_67]) ).
cnf(c_0_76,plain,
s_t(X1,ext(ext(X2,X1,alpha,gamma),X1,X3,ext(ext(ext(X4,X3,X1,X2),X3,alpha,gamma),X3,X3,ext(X4,X3,X1,X2))),X2),
inference(spm,[status(thm)],[c_0_68,c_0_69]) ).
cnf(c_0_77,plain,
( ext(ext(X1,X2,X3,X4),X2,X2,X1) = X1
| ext(X1,X2,X3,X4) = X2 ),
inference(spm,[status(thm)],[c_0_70,c_0_71]) ).
cnf(c_0_78,plain,
X1 != ext(X2,X1,alpha,gamma),
inference(split_conjunct,[status(thm)],[c_0_72]) ).
cnf(c_0_79,negated_conjecture,
s_t(esk3_0,esk4_0,ins(esk2_0,esk1_0,esk3_0,esk4_0)),
inference(spm,[status(thm)],[c_0_73,c_0_74]) ).
fof(c_0_80,plain,
! [X12,X15,X14,X17,X18] :
( le(X12,X15,X14,X17)
| ~ s_t(X12,X15,X18)
| ~ s_e(X12,X18,X14,X17) ),
inference(fof_simplification,[status(thm)],[aSatz5_5b]) ).
fof(c_0_81,plain,
! [X12,X15,X14,X17] :
( ~ s_e(X12,X15,X14,X17)
| s_e(X14,X17,X12,X15) ),
inference(fof_simplification,[status(thm)],[aSatz2_2]) ).
cnf(c_0_82,plain,
( s_e(X1,X2,X4,X5)
| ~ s_t(X1,X2,X3)
| ~ s_t(X4,X5,X6)
| ~ s_e(X1,X3,X4,X6)
| ~ s_e(X2,X3,X5,X6) ),
inference(split_conjunct,[status(thm)],[c_0_75]) ).
cnf(c_0_83,plain,
s_t(X1,ext(ext(X2,X1,alpha,gamma),X1,X3,ext(X4,X3,X1,X2)),X2),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_76,c_0_77]),c_0_78]) ).
cnf(c_0_84,plain,
( ext(X1,X2,X3,X2) = X3
| X1 = X2
| ~ s_t(X1,X2,X3) ),
inference(spm,[status(thm)],[c_0_60,c_0_34]) ).
cnf(c_0_85,negated_conjecture,
s_t(ins(esk2_0,esk1_0,esk3_0,esk4_0),esk4_0,esk3_0),
inference(spm,[status(thm)],[c_0_62,c_0_79]) ).
fof(c_0_86,plain,
! [X526,X527,X528,X529,X530] :
( le(X526,X527,X528,X529)
| ~ s_t(X526,X527,X530)
| ~ s_e(X526,X530,X528,X529) ),
inference(variable_rename,[status(thm)],[c_0_80]) ).
cnf(c_0_87,plain,
( s_e(X1,ins(X3,X4,X1,X2),X3,X4)
| ~ le(X1,X2,X3,X4) ),
inference(split_conjunct,[status(thm)],[c_0_64]) ).
fof(c_0_88,plain,
! [X346,X347,X348,X349] :
( ~ s_e(X346,X347,X348,X349)
| s_e(X348,X349,X346,X347) ),
inference(variable_rename,[status(thm)],[c_0_81]) ).
cnf(c_0_89,plain,
( s_e(X1,X2,X3,X4)
| ~ s_t(X3,X4,X2)
| ~ s_t(X1,X2,X4)
| ~ s_e(X1,X4,X3,X2) ),
inference(spm,[status(thm)],[c_0_82,c_0_34]) ).
cnf(c_0_90,plain,
s_t(X1,ext(ext(X1,X2,alpha,gamma),X2,X3,ext(X4,X3,X2,X1)),X2),
inference(spm,[status(thm)],[c_0_62,c_0_83]) ).
cnf(c_0_91,negated_conjecture,
( ext(ins(esk2_0,esk1_0,esk3_0,esk4_0),esk4_0,esk3_0,esk4_0) = esk3_0
| ins(esk2_0,esk1_0,esk3_0,esk4_0) = esk4_0 ),
inference(spm,[status(thm)],[c_0_84,c_0_85]) ).
fof(c_0_92,plain,
! [X395,X396] : s_t(X395,X395,X396),
inference(variable_rename,[status(thm)],[aSatz3_3]) ).
fof(c_0_93,plain,
! [X12,X15,X17,X14] :
( ~ s_t(X12,X15,X17)
| ~ s_t(X15,X14,X17)
| s_t(X12,X14,X17) ),
inference(fof_simplification,[status(thm)],[aSatz3_5b]) ).
cnf(c_0_94,negated_conjecture,
le(esk1_0,esk2_0,esk3_0,esk4_0),
inference(split_conjunct,[status(thm)],[c_0_55]) ).
cnf(c_0_95,plain,
( le(X1,X2,X3,X4)
| ~ s_t(X1,X2,X5)
| ~ s_e(X1,X5,X3,X4) ),
inference(split_conjunct,[status(thm)],[c_0_86]) ).
cnf(c_0_96,negated_conjecture,
s_e(esk3_0,ins(esk1_0,esk2_0,esk3_0,esk4_0),esk1_0,esk2_0),
inference(spm,[status(thm)],[c_0_87,c_0_66]) ).
cnf(c_0_97,plain,
( s_e(X3,X4,X1,X2)
| ~ s_e(X1,X2,X3,X4) ),
inference(split_conjunct,[status(thm)],[c_0_88]) ).
fof(c_0_98,plain,
! [X1,X2,X3] :
( ~ s_e(X1,X2,X3,X3)
| X1 = X2 ),
inference(fof_simplification,[status(thm)],[aA3]) ).
cnf(c_0_99,plain,
( s_e(X1,X2,X3,ext(X4,X1,X3,X2))
| ~ s_t(X3,ext(X4,X1,X3,X2),X2)
| ~ s_t(X1,X2,ext(X4,X1,X3,X2)) ),
inference(spm,[status(thm)],[c_0_89,c_0_57]) ).
cnf(c_0_100,negated_conjecture,
( ins(esk2_0,esk1_0,esk3_0,esk4_0) = esk4_0
| s_t(esk4_0,ext(ext(esk4_0,esk3_0,alpha,gamma),esk3_0,esk4_0,esk3_0),esk3_0) ),
inference(spm,[status(thm)],[c_0_90,c_0_91]) ).
cnf(c_0_101,plain,
s_t(X1,X1,X2),
inference(split_conjunct,[status(thm)],[c_0_92]) ).
fof(c_0_102,plain,
! [X412,X413,X414,X415] :
( ~ s_t(X412,X413,X414)
| ~ s_t(X413,X415,X414)
| s_t(X412,X415,X414) ),
inference(variable_rename,[status(thm)],[c_0_93]) ).
cnf(c_0_103,negated_conjecture,
s_t(esk3_0,esk4_0,ins(esk1_0,esk2_0,esk3_0,esk4_0)),
inference(spm,[status(thm)],[c_0_73,c_0_66]) ).
cnf(c_0_104,negated_conjecture,
le(esk1_0,esk2_0,esk4_0,esk3_0),
inference(spm,[status(thm)],[c_0_65,c_0_94]) ).
cnf(c_0_105,negated_conjecture,
( le(esk3_0,X1,esk1_0,esk2_0)
| ~ s_t(esk3_0,X1,ins(esk1_0,esk2_0,esk3_0,esk4_0)) ),
inference(spm,[status(thm)],[c_0_95,c_0_96]) ).
cnf(c_0_106,plain,
s_e(X1,X2,X3,ext(X4,X3,X1,X2)),
inference(spm,[status(thm)],[c_0_97,c_0_57]) ).
fof(c_0_107,plain,
! [X322,X323,X324] :
( ~ s_e(X322,X323,X324,X324)
| X322 = X323 ),
inference(variable_rename,[status(thm)],[c_0_98]) ).
cnf(c_0_108,negated_conjecture,
( ins(esk2_0,esk1_0,esk3_0,esk4_0) = esk4_0
| s_e(esk3_0,esk3_0,esk4_0,ext(ext(esk4_0,esk3_0,alpha,gamma),esk3_0,esk4_0,esk3_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_99,c_0_100]),c_0_101])]) ).
cnf(c_0_109,plain,
( s_t(X1,X4,X3)
| ~ s_t(X1,X2,X3)
| ~ s_t(X2,X4,X3) ),
inference(split_conjunct,[status(thm)],[c_0_102]) ).
cnf(c_0_110,negated_conjecture,
s_t(ins(esk1_0,esk2_0,esk3_0,esk4_0),esk4_0,esk3_0),
inference(spm,[status(thm)],[c_0_62,c_0_103]) ).
cnf(c_0_111,plain,
( ins(X3,X4,X1,X2) = ext(X1,X2,insert(X1,X2,X3,X4),X4)
| ~ le(X1,X2,X3,X4) ),
inference(split_conjunct,[status(thm)],[c_0_64]) ).
cnf(c_0_112,negated_conjecture,
( le(X1,X2,esk4_0,esk3_0)
| ~ le(X1,X2,esk1_0,esk2_0) ),
inference(spm,[status(thm)],[c_0_53,c_0_104]) ).
cnf(c_0_113,negated_conjecture,
le(esk3_0,ins(esk1_0,esk2_0,esk3_0,esk4_0),esk1_0,esk2_0),
inference(spm,[status(thm)],[c_0_105,c_0_42]) ).
fof(c_0_114,plain,
! [X12,X15,X14,X17] :
( ~ s_e(X12,X15,X14,X17)
| s_e(X15,X12,X17,X14) ),
inference(fof_simplification,[status(thm)],[aSatz2_14]) ).
cnf(c_0_115,plain,
( s_e(X1,X2,X3,X4)
| ~ s_t(X3,X4,ext(X5,X4,X2,X6))
| ~ s_t(X1,X2,X6)
| ~ s_e(X1,X6,X3,ext(X5,X4,X2,X6)) ),
inference(spm,[status(thm)],[c_0_82,c_0_106]) ).
cnf(c_0_116,plain,
( X1 = X2
| ~ s_e(X1,X2,X3,X3) ),
inference(split_conjunct,[status(thm)],[c_0_107]) ).
cnf(c_0_117,negated_conjecture,
( ins(esk2_0,esk1_0,esk3_0,esk4_0) = esk4_0
| s_e(esk4_0,ext(ext(esk4_0,esk3_0,alpha,gamma),esk3_0,esk4_0,esk3_0),esk3_0,esk3_0) ),
inference(spm,[status(thm)],[c_0_97,c_0_108]) ).
cnf(c_0_118,negated_conjecture,
( s_t(X1,esk4_0,esk3_0)
| ~ s_t(X1,ins(esk1_0,esk2_0,esk3_0,esk4_0),esk3_0) ),
inference(spm,[status(thm)],[c_0_109,c_0_110]) ).
cnf(c_0_119,plain,
( ins(X3,X4,X1,X2) = ext(X1,X2,ext(ext(X4,X3,alpha,gamma),X3,X1,X2),X4)
| ~ le(X1,X2,X3,X4) ),
inference(rw,[status(thm)],[c_0_111,c_0_45]) ).
cnf(c_0_120,negated_conjecture,
le(esk3_0,ins(esk1_0,esk2_0,esk3_0,esk4_0),esk4_0,esk3_0),
inference(spm,[status(thm)],[c_0_112,c_0_113]) ).
fof(c_0_121,plain,
! [X380,X381,X382,X383] :
( ~ s_e(X380,X381,X382,X383)
| s_e(X381,X380,X383,X382) ),
inference(variable_rename,[status(thm)],[c_0_114]) ).
cnf(c_0_122,plain,
( s_e(X1,X2,X3,X3)
| ~ s_t(X1,X2,X4)
| ~ s_e(X1,X4,X3,ext(X5,X3,X2,X4)) ),
inference(spm,[status(thm)],[c_0_115,c_0_101]) ).
cnf(c_0_123,negated_conjecture,
( ext(ext(esk4_0,esk3_0,alpha,gamma),esk3_0,esk4_0,esk3_0) = esk4_0
| ins(esk2_0,esk1_0,esk3_0,esk4_0) = esk4_0 ),
inference(spm,[status(thm)],[c_0_116,c_0_117]) ).
cnf(c_0_124,negated_conjecture,
s_t(ext(esk3_0,ins(esk1_0,esk2_0,esk3_0,esk4_0),X1,X2),esk4_0,esk3_0),
inference(spm,[status(thm)],[c_0_118,c_0_71]) ).
cnf(c_0_125,negated_conjecture,
ext(esk3_0,ins(esk1_0,esk2_0,esk3_0,esk4_0),ext(ext(esk3_0,esk4_0,alpha,gamma),esk4_0,esk3_0,ins(esk1_0,esk2_0,esk3_0,esk4_0)),esk3_0) = ins(esk4_0,esk3_0,esk3_0,ins(esk1_0,esk2_0,esk3_0,esk4_0)),
inference(spm,[status(thm)],[c_0_119,c_0_120]) ).
cnf(c_0_126,plain,
( s_e(X2,X1,X4,X3)
| ~ s_e(X1,X2,X3,X4) ),
inference(split_conjunct,[status(thm)],[c_0_121]) ).
cnf(c_0_127,negated_conjecture,
s_e(esk3_0,ins(esk4_0,esk3_0,esk3_0,ins(esk1_0,esk2_0,esk3_0,esk4_0)),esk4_0,esk3_0),
inference(spm,[status(thm)],[c_0_87,c_0_120]) ).
fof(c_0_128,plain,
! [X1,X2,X3,X4,X5,X6] :
( ~ s_e(X1,X2,X3,X4)
| ~ s_e(X1,X2,X5,X6)
| s_e(X3,X4,X5,X6) ),
inference(fof_simplification,[status(thm)],[aA2]) ).
fof(c_0_129,plain,
! [X12,X15,X14,X17] :
( ~ s_t(X12,X15,X14)
| ~ s_t(X15,X14,X17)
| X15 = X14
| s_t(X12,X14,X17) ),
inference(fof_simplification,[status(thm)],[aSatz3_7a]) ).
cnf(c_0_130,negated_conjecture,
( ins(esk2_0,esk1_0,esk3_0,esk4_0) = esk4_0
| s_e(X1,esk4_0,esk3_0,esk3_0)
| ~ s_t(X1,esk4_0,esk3_0)
| ~ s_e(X1,esk3_0,esk3_0,esk4_0) ),
inference(spm,[status(thm)],[c_0_122,c_0_123]) ).
cnf(c_0_131,negated_conjecture,
s_t(ins(esk4_0,esk3_0,esk3_0,ins(esk1_0,esk2_0,esk3_0,esk4_0)),esk4_0,esk3_0),
inference(spm,[status(thm)],[c_0_124,c_0_125]) ).
cnf(c_0_132,negated_conjecture,
s_e(ins(esk4_0,esk3_0,esk3_0,ins(esk1_0,esk2_0,esk3_0,esk4_0)),esk3_0,esk3_0,esk4_0),
inference(spm,[status(thm)],[c_0_126,c_0_127]) ).
fof(c_0_133,plain,
! [X316,X317,X318,X319,X320,X321] :
( ~ s_e(X316,X317,X318,X319)
| ~ s_e(X316,X317,X320,X321)
| s_e(X318,X319,X320,X321) ),
inference(variable_rename,[status(thm)],[c_0_128]) ).
fof(c_0_134,plain,
! [X408,X409,X410,X411] :
( ~ s_t(X408,X409,X410)
| ~ s_t(X409,X410,X411)
| X409 = X410
| s_t(X408,X410,X411) ),
inference(variable_rename,[status(thm)],[c_0_129]) ).
cnf(c_0_135,negated_conjecture,
( ins(esk2_0,esk1_0,esk3_0,esk4_0) = esk4_0
| s_e(ins(esk4_0,esk3_0,esk3_0,ins(esk1_0,esk2_0,esk3_0,esk4_0)),esk4_0,esk3_0,esk3_0) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_130,c_0_131]),c_0_132])]) ).
fof(c_0_136,plain,
! [X20,X31,X32,X21,X33,X34] :
( ( ~ s_e3(X20,X31,X32,X21,X33,X34)
| s_e(X20,X31,X21,X33) )
& ( ~ s_e3(X20,X31,X32,X21,X33,X34)
| s_e(X20,X32,X21,X34) )
& ( ~ s_e3(X20,X31,X32,X21,X33,X34)
| s_e(X31,X32,X33,X34) )
& ( ~ s_e(X20,X31,X21,X33)
| ~ s_e(X20,X32,X21,X34)
| ~ s_e(X31,X32,X33,X34)
| s_e3(X20,X31,X32,X21,X33,X34) ) ),
inference(fof_simplification,[status(thm)],[d_Defn4_4]) ).
cnf(c_0_137,plain,
( s_e(X3,X4,X5,X6)
| ~ s_e(X1,X2,X3,X4)
| ~ s_e(X1,X2,X5,X6) ),
inference(split_conjunct,[status(thm)],[c_0_133]) ).
cnf(c_0_138,negated_conjecture,
s_e(esk3_0,ins(esk2_0,esk1_0,esk3_0,esk4_0),esk2_0,esk1_0),
inference(spm,[status(thm)],[c_0_87,c_0_74]) ).
cnf(c_0_139,plain,
( X2 = X3
| s_t(X1,X3,X4)
| ~ s_t(X1,X2,X3)
| ~ s_t(X2,X3,X4) ),
inference(split_conjunct,[status(thm)],[c_0_134]) ).
cnf(c_0_140,negated_conjecture,
s_t(esk3_0,ins(esk1_0,esk2_0,esk3_0,esk4_0),ins(esk4_0,esk3_0,esk3_0,ins(esk1_0,esk2_0,esk3_0,esk4_0))),
inference(spm,[status(thm)],[c_0_73,c_0_120]) ).
cnf(c_0_141,negated_conjecture,
( ins(esk4_0,esk3_0,esk3_0,ins(esk1_0,esk2_0,esk3_0,esk4_0)) = esk4_0
| ins(esk2_0,esk1_0,esk3_0,esk4_0) = esk4_0 ),
inference(spm,[status(thm)],[c_0_116,c_0_135]) ).
fof(c_0_142,plain,
! [X571,X572,X573,X574,X575,X576] :
( ( ~ s_e3(X571,X572,X573,X574,X575,X576)
| s_e(X571,X572,X574,X575) )
& ( ~ s_e3(X571,X572,X573,X574,X575,X576)
| s_e(X571,X573,X574,X576) )
& ( ~ s_e3(X571,X572,X573,X574,X575,X576)
| s_e(X572,X573,X575,X576) )
& ( ~ s_e(X571,X572,X574,X575)
| ~ s_e(X571,X573,X574,X576)
| ~ s_e(X572,X573,X575,X576)
| s_e3(X571,X572,X573,X574,X575,X576) ) ),
inference(variable_rename,[status(thm)],[c_0_136]) ).
cnf(c_0_143,plain,
( s_e(X1,X2,X3,X4)
| ~ s_e(X4,X3,X1,X2) ),
inference(spm,[status(thm)],[c_0_137,c_0_34]) ).
cnf(c_0_144,negated_conjecture,
s_e(esk1_0,ins(esk4_0,esk3_0,esk1_0,esk2_0),esk4_0,esk3_0),
inference(spm,[status(thm)],[c_0_87,c_0_104]) ).
cnf(c_0_145,negated_conjecture,
s_e(ins(esk2_0,esk1_0,esk3_0,esk4_0),esk3_0,esk1_0,esk2_0),
inference(spm,[status(thm)],[c_0_126,c_0_138]) ).
cnf(c_0_146,negated_conjecture,
( ins(esk1_0,esk2_0,esk3_0,esk4_0) = esk4_0
| s_t(X1,esk4_0,esk3_0)
| ~ s_t(X1,ins(esk1_0,esk2_0,esk3_0,esk4_0),esk4_0) ),
inference(spm,[status(thm)],[c_0_139,c_0_110]) ).
cnf(c_0_147,negated_conjecture,
( ins(esk2_0,esk1_0,esk3_0,esk4_0) = esk4_0
| s_t(esk3_0,ins(esk1_0,esk2_0,esk3_0,esk4_0),esk4_0) ),
inference(spm,[status(thm)],[c_0_140,c_0_141]) ).
fof(c_0_148,plain,
! [X12,X15,X14,X20,X21,X22] :
( ~ s_t(X12,X15,X14)
| ~ s_e3(X12,X15,X14,X20,X21,X22)
| s_t(X20,X21,X22) ),
inference(fof_simplification,[status(thm)],[aSatz4_6]) ).
cnf(c_0_149,plain,
( s_e3(X1,X2,X5,X3,X4,X6)
| ~ s_e(X1,X2,X3,X4)
| ~ s_e(X1,X5,X3,X6)
| ~ s_e(X2,X5,X4,X6) ),
inference(split_conjunct,[status(thm)],[c_0_142]) ).
cnf(c_0_150,negated_conjecture,
s_e(esk4_0,esk3_0,ins(esk4_0,esk3_0,esk1_0,esk2_0),esk1_0),
inference(spm,[status(thm)],[c_0_143,c_0_144]) ).
fof(c_0_151,plain,
! [X364,X365] : s_e(X364,X364,X365,X365),
inference(variable_rename,[status(thm)],[aSatz2_8]) ).
cnf(c_0_152,negated_conjecture,
s_e(ins(esk4_0,esk3_0,esk1_0,esk2_0),esk1_0,esk3_0,esk4_0),
inference(spm,[status(thm)],[c_0_126,c_0_144]) ).
fof(c_0_153,plain,
! [X1,X2] :
( ~ s_t(X1,X2,X1)
| X1 = X2 ),
inference(fof_simplification,[status(thm)],[aA6]) ).
cnf(c_0_154,negated_conjecture,
s_e(esk1_0,esk2_0,esk3_0,ins(esk2_0,esk1_0,esk3_0,esk4_0)),
inference(spm,[status(thm)],[c_0_143,c_0_145]) ).
cnf(c_0_155,negated_conjecture,
( ins(esk2_0,esk1_0,esk3_0,esk4_0) = esk4_0
| ins(esk1_0,esk2_0,esk3_0,esk4_0) = esk4_0
| s_t(esk3_0,esk4_0,esk3_0) ),
inference(spm,[status(thm)],[c_0_146,c_0_147]) ).
cnf(c_0_156,negated_conjecture,
~ s_e(esk1_0,esk2_0,esk3_0,esk4_0),
inference(split_conjunct,[status(thm)],[c_0_55]) ).
fof(c_0_157,plain,
! [X453,X454,X455,X456,X457,X458] :
( ~ s_t(X453,X454,X455)
| ~ s_e3(X453,X454,X455,X456,X457,X458)
| s_t(X456,X457,X458) ),
inference(variable_rename,[status(thm)],[c_0_148]) ).
cnf(c_0_158,negated_conjecture,
( s_e3(X1,esk4_0,esk3_0,X2,ins(esk4_0,esk3_0,esk1_0,esk2_0),esk1_0)
| ~ s_e(X1,esk4_0,X2,ins(esk4_0,esk3_0,esk1_0,esk2_0))
| ~ s_e(X1,esk3_0,X2,esk1_0) ),
inference(spm,[status(thm)],[c_0_149,c_0_150]) ).
cnf(c_0_159,plain,
s_e(X1,X1,X2,X2),
inference(split_conjunct,[status(thm)],[c_0_151]) ).
cnf(c_0_160,negated_conjecture,
s_e(esk3_0,esk4_0,esk1_0,ins(esk4_0,esk3_0,esk1_0,esk2_0)),
inference(spm,[status(thm)],[c_0_143,c_0_152]) ).
fof(c_0_161,plain,
! [X337,X338] :
( ~ s_t(X337,X338,X337)
| X337 = X338 ),
inference(variable_rename,[status(thm)],[c_0_153]) ).
cnf(c_0_162,negated_conjecture,
s_e(esk1_0,esk2_0,esk3_0,ins(esk1_0,esk2_0,esk3_0,esk4_0)),
inference(spm,[status(thm)],[c_0_97,c_0_96]) ).
cnf(c_0_163,negated_conjecture,
( ins(esk1_0,esk2_0,esk3_0,esk4_0) = esk4_0
| s_t(esk3_0,esk4_0,esk3_0) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_154,c_0_155]),c_0_156]) ).
fof(c_0_164,plain,
! [X12,X15,X14] :
( ~ s_t(X12,X15,X14)
| ~ s_t(X15,X12,X14)
| X12 = X15 ),
inference(fof_simplification,[status(thm)],[aSatz3_4]) ).
cnf(c_0_165,plain,
( s_t(X4,X5,X6)
| ~ s_t(X1,X2,X3)
| ~ s_e3(X1,X2,X3,X4,X5,X6) ),
inference(split_conjunct,[status(thm)],[c_0_157]) ).
cnf(c_0_166,negated_conjecture,
s_e3(esk3_0,esk4_0,esk3_0,esk1_0,ins(esk4_0,esk3_0,esk1_0,esk2_0),esk1_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_158,c_0_159]),c_0_160])]) ).
cnf(c_0_167,plain,
( X1 = X2
| ~ s_t(X1,X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_161]) ).
cnf(c_0_168,negated_conjecture,
s_t(esk3_0,esk4_0,esk3_0),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_162,c_0_163]),c_0_156]) ).
fof(c_0_169,plain,
! [X397,X398,X399] :
( ~ s_t(X397,X398,X399)
| ~ s_t(X398,X397,X399)
| X397 = X398 ),
inference(variable_rename,[status(thm)],[c_0_164]) ).
cnf(c_0_170,negated_conjecture,
( s_t(esk1_0,ins(esk4_0,esk3_0,esk1_0,esk2_0),esk1_0)
| ~ s_t(esk3_0,esk4_0,esk3_0) ),
inference(spm,[status(thm)],[c_0_165,c_0_166]) ).
cnf(c_0_171,negated_conjecture,
esk4_0 = esk3_0,
inference(spm,[status(thm)],[c_0_167,c_0_168]) ).
cnf(c_0_172,plain,
( X1 = X2
| ~ s_t(X1,X2,X3)
| ~ s_t(X2,X1,X3) ),
inference(split_conjunct,[status(thm)],[c_0_169]) ).
cnf(c_0_173,negated_conjecture,
s_t(esk1_0,esk2_0,ins(esk4_0,esk3_0,esk1_0,esk2_0)),
inference(spm,[status(thm)],[c_0_73,c_0_104]) ).
cnf(c_0_174,negated_conjecture,
s_t(esk1_0,ins(esk3_0,esk3_0,esk1_0,esk2_0),esk1_0),
inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_170,c_0_168])]),c_0_171]) ).
cnf(c_0_175,negated_conjecture,
( esk2_0 = esk1_0
| ~ s_t(esk2_0,esk1_0,ins(esk4_0,esk3_0,esk1_0,esk2_0)) ),
inference(spm,[status(thm)],[c_0_172,c_0_173]) ).
cnf(c_0_176,negated_conjecture,
ins(esk3_0,esk3_0,esk1_0,esk2_0) = esk1_0,
inference(spm,[status(thm)],[c_0_167,c_0_174]) ).
cnf(c_0_177,negated_conjecture,
~ s_e(esk1_0,esk2_0,esk3_0,esk3_0),
inference(rw,[status(thm)],[c_0_156,c_0_171]) ).
cnf(c_0_178,negated_conjecture,
esk2_0 = esk1_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_175,c_0_171]),c_0_176]),c_0_42])]) ).
cnf(c_0_179,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_177,c_0_178]),c_0_159])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GEO495+1 : TPTP v9.2.1. Released v7.0.0.
% 0.00/0.12 % 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.16/0.33 % Computer : n026.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Mon May 4 18:00:38 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 123.55/99.82 % Version : CSE_E---1.7
% 123.55/99.82 % Problem : theBenchmark.p
% 123.55/99.82 % SZS status Theorem for theBenchmark.p
% 123.55/99.82 % SZS output start CNFRefutation
% See solution above
% 123.78/100.04 % Total time : 91.914s
%------------------------------------------------------------------------------