%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : GEO494+1 : TPTP v7.0.0. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : n099.star.cs.uiowa.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz
% Memory : 32218.75MB
% OS : Linux 3.10.0-327.36.3.el7.x86_64
% CPULimit : 300s
% DateTime : Fri Jan 20 10:18:34 EST 2017
% Result : Theorem 94.64s
% Output : CNFRefutation 94.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 30
% Syntax : Number of formulae : 251 ( 46 unt; 0 def)
% Number of atoms : 667 ( 73 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 750 ( 334 ~; 393 |; 23 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-6 aty)
% Number of functors : 11 ( 11 usr; 8 con; 0-4 aty)
% Number of variables : 892 ( 73 sgn 331 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(2,axiom,
! [X1,X2,X9,X7] :
( s_t(X1,X2,ext(X1,X2,X9,X7))
& s_e(X2,ext(X1,X2,X9,X7),X9,X7) ),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',aA4) ).
fof(3,axiom,
! [X1,X2] :
( ~ s_t(X1,X2,X1)
| equal(X1,X2) ),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',aA6) ).
fof(4,axiom,
! [X1,X2] : s_e(X1,X2,X2,X1),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',aA1) ).
fof(5,axiom,
! [X1,X2,X5] :
( ~ s_e(X1,X2,X5,X5)
| equal(X1,X2) ),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',aA3) ).
fof(6,axiom,
! [X1,X2,X5,X7,X10,X11] :
( ~ s_e(X1,X2,X5,X7)
| ~ s_e(X1,X2,X10,X11)
| s_e(X5,X7,X10,X11) ),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',aA2) ).
fof(8,axiom,
! [X12,X13,X14,X15] :
( ~ s_t(X12,X13,X14)
| ~ s_t(X12,X14,X15)
| s_t(X12,X13,X15) ),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',aSatz3_6b) ).
fof(9,axiom,
! [X12,X13,X14,X16,X17] :
( ( ~ s_t(X12,X13,X14)
| ~ s_e(X12,X14,X16,X17)
| s_t(X16,insert(X12,X13,X16,X17),X17) )
& ( ~ s_t(X12,X13,X14)
| ~ s_e(X12,X14,X16,X17)
| s_e3(X12,X13,X14,X16,insert(X12,X13,X16,X17),X17) ) ),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',aSatz4_5) ).
fof(11,axiom,
! [X12,X13,X14,X15] :
( ~ s_t(X12,X13,X14)
| ~ s_t(X12,X14,X15)
| s_t(X13,X14,X15) ),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',aSatz3_6a) ).
fof(16,axiom,
! [X12,X14,X13,X17] :
( ~ s_t(X12,X14,X13)
| ~ s_e(X12,X14,X12,X17)
| ~ s_e(X13,X14,X13,X17)
| equal(X14,X17) ),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',aSatz4_19) ).
fof(23,axiom,
! [X12,X13,X14,X15,X2] :
( ( ~ le(X12,X13,X14,X15)
| s_t(X14,insert(X12,X13,X14,X15),X15) )
& ( ~ le(X12,X13,X14,X15)
| s_e(X12,X13,X14,insert(X12,X13,X14,X15)) )
& ( ~ s_t(X14,X2,X15)
| ~ s_e(X12,X13,X14,X2)
| le(X12,X13,X14,X15) ) ),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',d_Defn5_4) ).
fof(27,axiom,
! [X12,X13,X14] :
( ~ s_t(X12,X13,X14)
| ~ s_t(X13,X12,X14)
| equal(X12,X13) ),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',aSatz3_4) ).
fof(28,axiom,
! [X16,X18] : s_t(X16,X16,X18),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',aSatz3_3) ).
fof(29,axiom,
! [X12,X13,X14] :
( ~ s_t(X12,X13,X14)
| s_t(X14,X13,X12) ),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',aSatz3_2) ).
fof(30,axiom,
! [X12,X13] : s_t(X12,X13,X13),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',aSatz3_1) ).
fof(31,axiom,
! [X12,X13,X14,X15] :
( ( ~ le(X12,X13,X14,X15)
| s_t(X12,X13,ins(X14,X15,X12,X13)) )
& ( ~ le(X12,X13,X14,X15)
| s_e(X12,ins(X14,X15,X12,X13),X14,X15) )
& ( ~ le(X12,X13,X14,X15)
| equal(ins(X14,X15,X12,X13),ext(X12,X13,insert(X12,X13,X14,X15),X15)) ) ),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',aSatz5_5a) ).
fof(33,axiom,
! [X12,X13,X14,X15] :
( ~ s_e(X12,X13,X14,X15)
| s_e(X12,X13,X15,X14) ),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',aSatz2_5) ).
fof(34,axiom,
! [X12,X13,X14,X15] :
( ~ s_e(X12,X13,X14,X15)
| s_e(X14,X15,X12,X13) ),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',aSatz2_2) ).
fof(36,axiom,
! [X12,X13] : s_e(X12,X13,X12,X13),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',aSatz2_1) ).
fof(39,axiom,
! [X13,X12] : ~ equal(X13,ext(X12,X13,alpha,gamma)),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',aSatz3_14b) ).
fof(41,axiom,
! [X12,X13,X15,X14] :
( ~ s_t(X12,X13,X15)
| ~ s_t(X13,X14,X15)
| s_t(X12,X14,X15) ),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',aSatz3_5b) ).
fof(42,axiom,
! [X12,X13,X15,X14] :
( ~ s_t(X12,X13,X15)
| ~ s_t(X13,X14,X15)
| s_t(X12,X13,X14) ),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',aSatz3_5a) ).
fof(46,axiom,
! [X12,X13,X14,X15] :
( ~ s_e(X12,X13,X14,X15)
| s_e(X13,X12,X15,X14) ),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',aSatz2_14) ).
fof(47,axiom,
! [X12,X13,X14,X32,X33,X34] :
( ~ s_t(X12,X13,X14)
| ~ s_t(X32,X33,X34)
| ~ s_e(X12,X13,X33,X34)
| ~ s_e(X13,X14,X32,X33)
| s_e(X12,X14,X32,X34) ),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',aSatz2_15) ).
fof(51,axiom,
! [X25,X12,X15,X13,X14] :
( equal(X25,X12)
| ~ s_t(X25,X12,X15)
| ~ s_e(X12,X15,X13,X14)
| equal(X15,ext(X25,X12,X13,X14)) ),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',aSatz2_12) ).
fof(53,axiom,
! [X12,X13,X14,X15,X30] :
( le(X12,X13,X14,X15)
| ~ s_t(X12,X13,X30)
| ~ s_e(X12,X30,X14,X15) ),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',aSatz5_5b) ).
fof(54,axiom,
! [X12,X13,X16,X17] : equal(insert(X12,X13,X16,X17),ext(ext(X17,X16,alpha,gamma),X16,X12,X13)),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',d_insert) ).
fof(60,conjecture,
! [X12,X13,X14,X15,X30,X31] :
( ~ le(X12,X13,X14,X15)
| ~ le(X14,X15,X30,X31)
| le(X12,X13,X30,X31) ),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',aSatz5_8) ).
fof(61,axiom,
! [X12,X13] : s_e(X12,X12,X13,X13),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',aSatz2_8) ).
fof(63,axiom,
! [X12,X13,X14,X15,X16,X18,X17,X24] :
( ~ le(X12,X13,X14,X15)
| ~ s_e(X12,X13,X16,X18)
| ~ s_e(X14,X15,X17,X24)
| le(X16,X18,X17,X24) ),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',aSatz5_6) ).
fof(64,axiom,
! [X12,X13,X14,X15] :
( equal(X12,X13)
| ~ s_t(X12,X13,X14)
| ~ s_t(X12,X13,X15)
| s_t(X12,X14,X15)
| s_t(X12,X15,X14) ),
file('/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2',aSatz5_1) ).
fof(67,negated_conjecture,
~ ! [X12,X13,X14,X15,X30,X31] :
( ~ le(X12,X13,X14,X15)
| ~ le(X14,X15,X30,X31)
| le(X12,X13,X30,X31) ),
inference(assume_negation,[status(cth)],[60]) ).
fof(69,plain,
! [X1,X2] :
( ~ s_t(X1,X2,X1)
| equal(X1,X2) ),
inference(fof_simplification,[status(thm)],[3,theory(equality)]) ).
fof(70,plain,
! [X1,X2,X5] :
( ~ s_e(X1,X2,X5,X5)
| equal(X1,X2) ),
inference(fof_simplification,[status(thm)],[5,theory(equality)]) ).
fof(71,plain,
! [X1,X2,X5,X7,X10,X11] :
( ~ s_e(X1,X2,X5,X7)
| ~ s_e(X1,X2,X10,X11)
| s_e(X5,X7,X10,X11) ),
inference(fof_simplification,[status(thm)],[6,theory(equality)]) ).
fof(73,plain,
! [X12,X13,X14,X15] :
( ~ s_t(X12,X13,X14)
| ~ s_t(X12,X14,X15)
| s_t(X12,X13,X15) ),
inference(fof_simplification,[status(thm)],[8,theory(equality)]) ).
fof(74,plain,
! [X12,X13,X14,X16,X17] :
( ( ~ s_t(X12,X13,X14)
| ~ s_e(X12,X14,X16,X17)
| s_t(X16,insert(X12,X13,X16,X17),X17) )
& ( ~ s_t(X12,X13,X14)
| ~ s_e(X12,X14,X16,X17)
| s_e3(X12,X13,X14,X16,insert(X12,X13,X16,X17),X17) ) ),
inference(fof_simplification,[status(thm)],[9,theory(equality)]) ).
fof(76,plain,
! [X12,X13,X14,X15] :
( ~ s_t(X12,X13,X14)
| ~ s_t(X12,X14,X15)
| s_t(X13,X14,X15) ),
inference(fof_simplification,[status(thm)],[11,theory(equality)]) ).
fof(81,plain,
! [X12,X14,X13,X17] :
( ~ s_t(X12,X14,X13)
| ~ s_e(X12,X14,X12,X17)
| ~ s_e(X13,X14,X13,X17)
| equal(X14,X17) ),
inference(fof_simplification,[status(thm)],[16,theory(equality)]) ).
fof(87,plain,
! [X12,X13,X14,X15,X2] :
( ( ~ le(X12,X13,X14,X15)
| s_t(X14,insert(X12,X13,X14,X15),X15) )
& ( ~ le(X12,X13,X14,X15)
| s_e(X12,X13,X14,insert(X12,X13,X14,X15)) )
& ( ~ s_t(X14,X2,X15)
| ~ s_e(X12,X13,X14,X2)
| le(X12,X13,X14,X15) ) ),
inference(fof_simplification,[status(thm)],[23,theory(equality)]) ).
fof(89,plain,
! [X12,X13,X14] :
( ~ s_t(X12,X13,X14)
| ~ s_t(X13,X12,X14)
| equal(X12,X13) ),
inference(fof_simplification,[status(thm)],[27,theory(equality)]) ).
fof(90,plain,
! [X12,X13,X14] :
( ~ s_t(X12,X13,X14)
| s_t(X14,X13,X12) ),
inference(fof_simplification,[status(thm)],[29,theory(equality)]) ).
fof(91,plain,
! [X12,X13,X14,X15] :
( ( ~ le(X12,X13,X14,X15)
| s_t(X12,X13,ins(X14,X15,X12,X13)) )
& ( ~ le(X12,X13,X14,X15)
| s_e(X12,ins(X14,X15,X12,X13),X14,X15) )
& ( ~ le(X12,X13,X14,X15)
| equal(ins(X14,X15,X12,X13),ext(X12,X13,insert(X12,X13,X14,X15),X15)) ) ),
inference(fof_simplification,[status(thm)],[31,theory(equality)]) ).
fof(93,plain,
! [X12,X13,X14,X15] :
( ~ s_e(X12,X13,X14,X15)
| s_e(X12,X13,X15,X14) ),
inference(fof_simplification,[status(thm)],[33,theory(equality)]) ).
fof(94,plain,
! [X12,X13,X14,X15] :
( ~ s_e(X12,X13,X14,X15)
| s_e(X14,X15,X12,X13) ),
inference(fof_simplification,[status(thm)],[34,theory(equality)]) ).
fof(98,plain,
! [X12,X13,X15,X14] :
( ~ s_t(X12,X13,X15)
| ~ s_t(X13,X14,X15)
| s_t(X12,X14,X15) ),
inference(fof_simplification,[status(thm)],[41,theory(equality)]) ).
fof(99,plain,
! [X12,X13,X15,X14] :
( ~ s_t(X12,X13,X15)
| ~ s_t(X13,X14,X15)
| s_t(X12,X13,X14) ),
inference(fof_simplification,[status(thm)],[42,theory(equality)]) ).
fof(102,plain,
! [X12,X13,X14,X15] :
( ~ s_e(X12,X13,X14,X15)
| s_e(X13,X12,X15,X14) ),
inference(fof_simplification,[status(thm)],[46,theory(equality)]) ).
fof(103,plain,
! [X12,X13,X14,X32,X33,X34] :
( ~ s_t(X12,X13,X14)
| ~ s_t(X32,X33,X34)
| ~ s_e(X12,X13,X33,X34)
| ~ s_e(X13,X14,X32,X33)
| s_e(X12,X14,X32,X34) ),
inference(fof_simplification,[status(thm)],[47,theory(equality)]) ).
fof(106,plain,
! [X25,X12,X15,X13,X14] :
( equal(X25,X12)
| ~ s_t(X25,X12,X15)
| ~ s_e(X12,X15,X13,X14)
| equal(X15,ext(X25,X12,X13,X14)) ),
inference(fof_simplification,[status(thm)],[51,theory(equality)]) ).
fof(108,plain,
! [X12,X13,X14,X15,X30] :
( le(X12,X13,X14,X15)
| ~ s_t(X12,X13,X30)
| ~ s_e(X12,X30,X14,X15) ),
inference(fof_simplification,[status(thm)],[53,theory(equality)]) ).
fof(114,negated_conjecture,
~ ! [X12,X13,X14,X15,X30,X31] :
( ~ le(X12,X13,X14,X15)
| ~ le(X14,X15,X30,X31)
| le(X12,X13,X30,X31) ),
inference(fof_simplification,[status(thm)],[67,theory(equality)]) ).
fof(115,plain,
! [X12,X13,X14,X15,X16,X18,X17,X24] :
( ~ le(X12,X13,X14,X15)
| ~ s_e(X12,X13,X16,X18)
| ~ s_e(X14,X15,X17,X24)
| le(X16,X18,X17,X24) ),
inference(fof_simplification,[status(thm)],[63,theory(equality)]) ).
fof(116,plain,
! [X12,X13,X14,X15] :
( equal(X12,X13)
| ~ s_t(X12,X13,X14)
| ~ s_t(X12,X13,X15)
| s_t(X12,X14,X15)
| s_t(X12,X15,X14) ),
inference(fof_simplification,[status(thm)],[64,theory(equality)]) ).
fof(121,plain,
! [X10,X11,X12,X13] :
( s_t(X10,X11,ext(X10,X11,X12,X13))
& s_e(X11,ext(X10,X11,X12,X13),X12,X13) ),
inference(variable_rename,[status(thm)],[2]) ).
cnf(122,plain,
s_e(X1,ext(X2,X1,X3,X4),X3,X4),
inference(split_conjunct,[status(thm)],[121]) ).
cnf(123,plain,
s_t(X1,X2,ext(X1,X2,X3,X4)),
inference(split_conjunct,[status(thm)],[121]) ).
fof(124,plain,
! [X3,X4] :
( ~ s_t(X3,X4,X3)
| equal(X3,X4) ),
inference(variable_rename,[status(thm)],[69]) ).
cnf(125,plain,
( X1 = X2
| ~ s_t(X1,X2,X1) ),
inference(split_conjunct,[status(thm)],[124]) ).
fof(126,plain,
! [X3,X4] : s_e(X3,X4,X4,X3),
inference(variable_rename,[status(thm)],[4]) ).
cnf(127,plain,
s_e(X1,X2,X2,X1),
inference(split_conjunct,[status(thm)],[126]) ).
fof(128,plain,
! [X6,X7,X8] :
( ~ s_e(X6,X7,X8,X8)
| equal(X6,X7) ),
inference(variable_rename,[status(thm)],[70]) ).
cnf(129,plain,
( X1 = X2
| ~ s_e(X1,X2,X3,X3) ),
inference(split_conjunct,[status(thm)],[128]) ).
fof(130,plain,
! [X12,X13,X14,X15,X16,X17] :
( ~ s_e(X12,X13,X14,X15)
| ~ s_e(X12,X13,X16,X17)
| s_e(X14,X15,X16,X17) ),
inference(variable_rename,[status(thm)],[71]) ).
cnf(131,plain,
( s_e(X1,X2,X3,X4)
| ~ s_e(X5,X6,X3,X4)
| ~ s_e(X5,X6,X1,X2) ),
inference(split_conjunct,[status(thm)],[130]) ).
fof(135,plain,
! [X16,X17,X18,X19] :
( ~ s_t(X16,X17,X18)
| ~ s_t(X16,X18,X19)
| s_t(X16,X17,X19) ),
inference(variable_rename,[status(thm)],[73]) ).
cnf(136,plain,
( s_t(X1,X2,X3)
| ~ s_t(X1,X4,X3)
| ~ s_t(X1,X2,X4) ),
inference(split_conjunct,[status(thm)],[135]) ).
fof(137,plain,
! [X18,X19,X20,X21,X22] :
( ( ~ s_t(X18,X19,X20)
| ~ s_e(X18,X20,X21,X22)
| s_t(X21,insert(X18,X19,X21,X22),X22) )
& ( ~ s_t(X18,X19,X20)
| ~ s_e(X18,X20,X21,X22)
| s_e3(X18,X19,X20,X21,insert(X18,X19,X21,X22),X22) ) ),
inference(variable_rename,[status(thm)],[74]) ).
cnf(139,plain,
( s_t(X1,insert(X2,X3,X1,X4),X4)
| ~ s_e(X2,X5,X1,X4)
| ~ s_t(X2,X3,X5) ),
inference(split_conjunct,[status(thm)],[137]) ).
fof(142,plain,
! [X16,X17,X18,X19] :
( ~ s_t(X16,X17,X18)
| ~ s_t(X16,X18,X19)
| s_t(X17,X18,X19) ),
inference(variable_rename,[status(thm)],[76]) ).
cnf(143,plain,
( s_t(X1,X2,X3)
| ~ s_t(X4,X2,X3)
| ~ s_t(X4,X1,X2) ),
inference(split_conjunct,[status(thm)],[142]) ).
fof(159,plain,
! [X18,X19,X20,X21] :
( ~ s_t(X18,X19,X20)
| ~ s_e(X18,X19,X18,X21)
| ~ s_e(X20,X19,X20,X21)
| equal(X19,X21) ),
inference(variable_rename,[status(thm)],[81]) ).
cnf(160,plain,
( X1 = X2
| ~ s_e(X3,X1,X3,X2)
| ~ s_e(X4,X1,X4,X2)
| ~ s_t(X4,X1,X3) ),
inference(split_conjunct,[status(thm)],[159]) ).
fof(184,plain,
! [X16,X17,X18,X19,X20] :
( ( ~ le(X16,X17,X18,X19)
| s_t(X18,insert(X16,X17,X18,X19),X19) )
& ( ~ le(X16,X17,X18,X19)
| s_e(X16,X17,X18,insert(X16,X17,X18,X19)) )
& ( ~ s_t(X18,X20,X19)
| ~ s_e(X16,X17,X18,X20)
| le(X16,X17,X18,X19) ) ),
inference(variable_rename,[status(thm)],[87]) ).
cnf(185,plain,
( le(X1,X2,X3,X4)
| ~ s_e(X1,X2,X3,X5)
| ~ s_t(X3,X5,X4) ),
inference(split_conjunct,[status(thm)],[184]) ).
cnf(187,plain,
( s_t(X1,insert(X2,X3,X1,X4),X4)
| ~ le(X2,X3,X1,X4) ),
inference(split_conjunct,[status(thm)],[184]) ).
fof(192,plain,
! [X15,X16,X17] :
( ~ s_t(X15,X16,X17)
| ~ s_t(X16,X15,X17)
| equal(X15,X16) ),
inference(variable_rename,[status(thm)],[89]) ).
cnf(193,plain,
( X1 = X2
| ~ s_t(X2,X1,X3)
| ~ s_t(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[192]) ).
fof(194,plain,
! [X19,X20] : s_t(X19,X19,X20),
inference(variable_rename,[status(thm)],[28]) ).
cnf(195,plain,
s_t(X1,X1,X2),
inference(split_conjunct,[status(thm)],[194]) ).
fof(196,plain,
! [X15,X16,X17] :
( ~ s_t(X15,X16,X17)
| s_t(X17,X16,X15) ),
inference(variable_rename,[status(thm)],[90]) ).
cnf(197,plain,
( s_t(X1,X2,X3)
| ~ s_t(X3,X2,X1) ),
inference(split_conjunct,[status(thm)],[196]) ).
fof(198,plain,
! [X14,X15] : s_t(X14,X15,X15),
inference(variable_rename,[status(thm)],[30]) ).
cnf(199,plain,
s_t(X1,X2,X2),
inference(split_conjunct,[status(thm)],[198]) ).
fof(200,plain,
! [X16,X17,X18,X19] :
( ( ~ le(X16,X17,X18,X19)
| s_t(X16,X17,ins(X18,X19,X16,X17)) )
& ( ~ le(X16,X17,X18,X19)
| s_e(X16,ins(X18,X19,X16,X17),X18,X19) )
& ( ~ le(X16,X17,X18,X19)
| equal(ins(X18,X19,X16,X17),ext(X16,X17,insert(X16,X17,X18,X19),X19)) ) ),
inference(variable_rename,[status(thm)],[91]) ).
cnf(201,plain,
( ins(X1,X2,X3,X4) = ext(X3,X4,insert(X3,X4,X1,X2),X2)
| ~ le(X3,X4,X1,X2) ),
inference(split_conjunct,[status(thm)],[200]) ).
cnf(202,plain,
( s_e(X1,ins(X2,X3,X1,X4),X2,X3)
| ~ le(X1,X4,X2,X3) ),
inference(split_conjunct,[status(thm)],[200]) ).
cnf(203,plain,
( s_t(X1,X2,ins(X3,X4,X1,X2))
| ~ le(X1,X2,X3,X4) ),
inference(split_conjunct,[status(thm)],[200]) ).
fof(206,plain,
! [X16,X17,X18,X19] :
( ~ s_e(X16,X17,X18,X19)
| s_e(X16,X17,X19,X18) ),
inference(variable_rename,[status(thm)],[93]) ).
cnf(207,plain,
( s_e(X1,X2,X3,X4)
| ~ s_e(X1,X2,X4,X3) ),
inference(split_conjunct,[status(thm)],[206]) ).
fof(208,plain,
! [X16,X17,X18,X19] :
( ~ s_e(X16,X17,X18,X19)
| s_e(X18,X19,X16,X17) ),
inference(variable_rename,[status(thm)],[94]) ).
cnf(209,plain,
( s_e(X1,X2,X3,X4)
| ~ s_e(X3,X4,X1,X2) ),
inference(split_conjunct,[status(thm)],[208]) ).
fof(212,plain,
! [X14,X15] : s_e(X14,X15,X14,X15),
inference(variable_rename,[status(thm)],[36]) ).
cnf(213,plain,
s_e(X1,X2,X1,X2),
inference(split_conjunct,[status(thm)],[212]) ).
fof(218,plain,
! [X14,X15] : ~ equal(X14,ext(X15,X14,alpha,gamma)),
inference(variable_rename,[status(thm)],[39]) ).
cnf(219,plain,
X1 != ext(X2,X1,alpha,gamma),
inference(split_conjunct,[status(thm)],[218]) ).
fof(222,plain,
! [X16,X17,X18,X19] :
( ~ s_t(X16,X17,X18)
| ~ s_t(X17,X19,X18)
| s_t(X16,X19,X18) ),
inference(variable_rename,[status(thm)],[98]) ).
cnf(223,plain,
( s_t(X1,X2,X3)
| ~ s_t(X4,X2,X3)
| ~ s_t(X1,X4,X3) ),
inference(split_conjunct,[status(thm)],[222]) ).
fof(224,plain,
! [X16,X17,X18,X19] :
( ~ s_t(X16,X17,X18)
| ~ s_t(X17,X19,X18)
| s_t(X16,X17,X19) ),
inference(variable_rename,[status(thm)],[99]) ).
cnf(225,plain,
( s_t(X1,X2,X3)
| ~ s_t(X2,X3,X4)
| ~ s_t(X1,X2,X4) ),
inference(split_conjunct,[status(thm)],[224]) ).
fof(236,plain,
! [X16,X17,X18,X19] :
( ~ s_e(X16,X17,X18,X19)
| s_e(X17,X16,X19,X18) ),
inference(variable_rename,[status(thm)],[102]) ).
cnf(237,plain,
( s_e(X1,X2,X3,X4)
| ~ s_e(X2,X1,X4,X3) ),
inference(split_conjunct,[status(thm)],[236]) ).
fof(238,plain,
! [X35,X36,X37,X38,X39,X40] :
( ~ s_t(X35,X36,X37)
| ~ s_t(X38,X39,X40)
| ~ s_e(X35,X36,X39,X40)
| ~ s_e(X36,X37,X38,X39)
| s_e(X35,X37,X38,X40) ),
inference(variable_rename,[status(thm)],[103]) ).
cnf(239,plain,
( s_e(X1,X2,X3,X4)
| ~ s_e(X5,X2,X3,X6)
| ~ s_e(X1,X5,X6,X4)
| ~ s_t(X3,X6,X4)
| ~ s_t(X1,X5,X2) ),
inference(split_conjunct,[status(thm)],[238]) ).
fof(246,plain,
! [X26,X27,X28,X29,X30] :
( equal(X26,X27)
| ~ s_t(X26,X27,X28)
| ~ s_e(X27,X28,X29,X30)
| equal(X28,ext(X26,X27,X29,X30)) ),
inference(variable_rename,[status(thm)],[106]) ).
cnf(247,plain,
( X1 = ext(X2,X3,X4,X5)
| X2 = X3
| ~ s_e(X3,X1,X4,X5)
| ~ s_t(X2,X3,X1) ),
inference(split_conjunct,[status(thm)],[246]) ).
fof(250,plain,
! [X31,X32,X33,X34,X35] :
( le(X31,X32,X33,X34)
| ~ s_t(X31,X32,X35)
| ~ s_e(X31,X35,X33,X34) ),
inference(variable_rename,[status(thm)],[108]) ).
cnf(251,plain,
( le(X1,X5,X3,X4)
| ~ s_e(X1,X2,X3,X4)
| ~ s_t(X1,X5,X2) ),
inference(split_conjunct,[status(thm)],[250]) ).
fof(252,plain,
! [X18,X19,X20,X21] : equal(insert(X18,X19,X20,X21),ext(ext(X21,X20,alpha,gamma),X20,X18,X19)),
inference(variable_rename,[status(thm)],[54]) ).
cnf(253,plain,
insert(X1,X2,X3,X4) = ext(ext(X4,X3,alpha,gamma),X3,X1,X2),
inference(split_conjunct,[status(thm)],[252]) ).
fof(264,negated_conjecture,
? [X12,X13,X14,X15,X30,X31] :
( le(X12,X13,X14,X15)
& le(X14,X15,X30,X31)
& ~ le(X12,X13,X30,X31) ),
inference(fof_nnf,[status(thm)],[114]) ).
fof(265,negated_conjecture,
? [X32,X33,X34,X35,X36,X37] :
( le(X32,X33,X34,X35)
& le(X34,X35,X36,X37)
& ~ le(X32,X33,X36,X37) ),
inference(variable_rename,[status(thm)],[264]) ).
fof(266,negated_conjecture,
( le(esk1_0,esk2_0,esk3_0,esk4_0)
& le(esk3_0,esk4_0,esk5_0,esk6_0)
& ~ le(esk1_0,esk2_0,esk5_0,esk6_0) ),
inference(skolemize,[status(esa)],[265]) ).
cnf(267,negated_conjecture,
~ le(esk1_0,esk2_0,esk5_0,esk6_0),
inference(split_conjunct,[status(thm)],[266]) ).
cnf(268,negated_conjecture,
le(esk3_0,esk4_0,esk5_0,esk6_0),
inference(split_conjunct,[status(thm)],[266]) ).
cnf(269,negated_conjecture,
le(esk1_0,esk2_0,esk3_0,esk4_0),
inference(split_conjunct,[status(thm)],[266]) ).
fof(270,plain,
! [X14,X15] : s_e(X14,X14,X15,X15),
inference(variable_rename,[status(thm)],[61]) ).
cnf(271,plain,
s_e(X1,X1,X2,X2),
inference(split_conjunct,[status(thm)],[270]) ).
fof(274,plain,
! [X25,X26,X27,X28,X29,X30,X31,X32] :
( ~ le(X25,X26,X27,X28)
| ~ s_e(X25,X26,X29,X30)
| ~ s_e(X27,X28,X31,X32)
| le(X29,X30,X31,X32) ),
inference(variable_rename,[status(thm)],[115]) ).
cnf(275,plain,
( le(X1,X2,X3,X4)
| ~ s_e(X5,X6,X3,X4)
| ~ s_e(X7,X8,X1,X2)
| ~ le(X7,X8,X5,X6) ),
inference(split_conjunct,[status(thm)],[274]) ).
fof(276,plain,
! [X16,X17,X18,X19] :
( equal(X16,X17)
| ~ s_t(X16,X17,X18)
| ~ s_t(X16,X17,X19)
| s_t(X16,X18,X19)
| s_t(X16,X19,X18) ),
inference(variable_rename,[status(thm)],[116]) ).
cnf(277,plain,
( s_t(X1,X2,X3)
| s_t(X1,X3,X2)
| X1 = X4
| ~ s_t(X1,X4,X2)
| ~ s_t(X1,X4,X3) ),
inference(split_conjunct,[status(thm)],[276]) ).
cnf(282,plain,
( s_t(X1,ext(ext(X4,X1,alpha,gamma),X1,X2,X3),X4)
| ~ le(X2,X3,X1,X4) ),
inference(rw,[status(thm)],[187,253,theory(equality)]),
[unfolding] ).
cnf(284,plain,
( ext(X3,X4,ext(ext(X2,X1,alpha,gamma),X1,X3,X4),X2) = ins(X1,X2,X3,X4)
| ~ le(X3,X4,X1,X2) ),
inference(rw,[status(thm)],[201,253,theory(equality)]),
[unfolding] ).
cnf(285,plain,
( s_t(X1,ext(ext(X4,X1,alpha,gamma),X1,X2,X3),X4)
| ~ s_t(X2,X3,X5)
| ~ s_e(X2,X5,X1,X4) ),
inference(rw,[status(thm)],[139,253,theory(equality)]),
[unfolding] ).
cnf(290,plain,
s_t(ext(X1,X2,X3,X4),X2,X1),
inference(spm,[status(thm)],[197,123,theory(equality)]) ).
cnf(324,plain,
X1 = ext(X2,X1,X3,X3),
inference(spm,[status(thm)],[129,122,theory(equality)]) ).
cnf(330,plain,
s_e(X1,X2,X3,ext(X4,X3,X1,X2)),
inference(spm,[status(thm)],[209,122,theory(equality)]) ).
cnf(336,plain,
( s_t(X1,X2,ext(X3,X2,X4,X5))
| ~ s_t(X3,X1,X2) ),
inference(spm,[status(thm)],[143,123,theory(equality)]) ).
cnf(359,plain,
( s_t(ins(X1,X2,X3,X4),X4,X3)
| ~ le(X3,X4,X1,X2) ),
inference(spm,[status(thm)],[197,203,theory(equality)]) ).
cnf(361,plain,
( s_t(X1,X2,ins(X3,X4,X5,X2))
| ~ s_t(X5,X1,X2)
| ~ le(X5,X2,X3,X4) ),
inference(spm,[status(thm)],[143,203,theory(equality)]) ).
cnf(365,plain,
( s_t(X1,X2,ins(X3,X4,X5,X2))
| ~ s_t(X1,X5,ins(X3,X4,X5,X2))
| ~ le(X5,X2,X3,X4) ),
inference(spm,[status(thm)],[223,203,theory(equality)]) ).
cnf(370,plain,
( s_t(X1,X2,X3)
| ~ s_t(X1,X2,ins(X4,X5,X2,X3))
| ~ le(X2,X3,X4,X5) ),
inference(spm,[status(thm)],[225,203,theory(equality)]) ).
cnf(374,plain,
( s_t(X1,X2,ext(X1,X3,X4,X5))
| ~ s_t(X1,X2,X3) ),
inference(spm,[status(thm)],[136,123,theory(equality)]) ).
cnf(376,plain,
( X1 = ins(X2,X2,X1,X3)
| ~ le(X1,X3,X2,X2) ),
inference(spm,[status(thm)],[129,202,theory(equality)]) ).
cnf(378,plain,
( s_e(ins(X1,X2,X3,X4),X3,X2,X1)
| ~ le(X3,X4,X1,X2) ),
inference(spm,[status(thm)],[237,202,theory(equality)]) ).
cnf(384,plain,
( le(X1,X2,X3,X4)
| ~ s_t(X1,X2,ext(X5,X1,X3,X4)) ),
inference(spm,[status(thm)],[251,122,theory(equality)]) ).
cnf(385,plain,
( le(X1,X2,X3,X4)
| ~ s_t(X1,X2,ins(X3,X4,X1,X5))
| ~ le(X1,X5,X3,X4) ),
inference(spm,[status(thm)],[251,202,theory(equality)]) ).
cnf(390,plain,
( le(X1,X2,X2,X3)
| ~ s_t(X2,X1,X3) ),
inference(spm,[status(thm)],[185,127,theory(equality)]) ).
cnf(392,plain,
( le(X1,X1,X2,X3)
| ~ s_t(X2,X2,X3) ),
inference(spm,[status(thm)],[185,271,theory(equality)]) ).
cnf(395,plain,
( le(X1,X1,X2,X3)
| $false ),
inference(rw,[status(thm)],[392,195,theory(equality)]) ).
cnf(396,plain,
le(X1,X1,X2,X3),
inference(cn,[status(thm)],[395,theory(equality)]) ).
cnf(403,plain,
( s_e(X1,X2,X3,X4)
| ~ s_e(X5,ext(X6,X5,X3,X4),X1,X2) ),
inference(spm,[status(thm)],[131,122,theory(equality)]) ).
cnf(421,plain,
( ext(X1,X2,X2,X3) = X3
| ~ s_t(X2,ext(X1,X2,X2,X3),X4)
| ~ s_e(X4,ext(X1,X2,X2,X3),X4,X3) ),
inference(spm,[status(thm)],[160,122,theory(equality)]) ).
cnf(423,plain,
( ext(X1,X2,X3,X2) = X3
| X1 = X2
| ~ s_t(X1,X2,X3) ),
inference(spm,[status(thm)],[247,127,theory(equality)]) ).
cnf(430,plain,
( X1 = ext(ext(X1,X1,alpha,gamma),X1,X2,X3)
| ~ le(X2,X3,X1,X1) ),
inference(spm,[status(thm)],[125,282,theory(equality)]) ).
cnf(431,plain,
( s_t(X1,ext(ext(X1,X2,alpha,gamma),X2,X3,X4),X2)
| ~ le(X3,X4,X2,X1) ),
inference(spm,[status(thm)],[197,282,theory(equality)]) ).
cnf(432,plain,
( ext(ext(X1,X2,alpha,gamma),X2,X3,X4) = X2
| ~ s_t(ext(ext(X1,X2,alpha,gamma),X2,X3,X4),X2,X1)
| ~ le(X3,X4,X2,X1) ),
inference(spm,[status(thm)],[193,282,theory(equality)]) ).
cnf(463,plain,
( X1 = X2
| s_t(X1,X3,ins(X4,X5,X1,X2))
| s_t(X1,ins(X4,X5,X1,X2),X3)
| ~ s_t(X1,X2,X3)
| ~ le(X1,X2,X4,X5) ),
inference(spm,[status(thm)],[277,203,theory(equality)]) ).
cnf(465,plain,
( le(X1,X2,X3,X4)
| ~ le(X2,X1,X5,X6)
| ~ s_e(X5,X6,X3,X4) ),
inference(spm,[status(thm)],[275,127,theory(equality)]) ).
cnf(468,plain,
( le(X1,X2,X3,X4)
| ~ le(X5,ext(X6,X5,X1,X2),X7,X8)
| ~ s_e(X7,X8,X3,X4) ),
inference(spm,[status(thm)],[275,122,theory(equality)]) ).
cnf(504,plain,
( s_t(X1,ext(ext(X2,X1,alpha,gamma),X1,X3,X4),X2)
| ~ s_t(X3,X4,ins(X1,X2,X3,X5))
| ~ le(X3,X5,X1,X2) ),
inference(spm,[status(thm)],[285,202,theory(equality)]) ).
cnf(653,plain,
s_e(X1,X2,ext(X3,X4,X1,X2),X4),
inference(spm,[status(thm)],[207,330,theory(equality)]) ).
cnf(655,plain,
( le(X1,X2,X3,X4)
| ~ s_t(X3,ext(X5,X3,X1,X2),X4) ),
inference(spm,[status(thm)],[185,330,theory(equality)]) ).
cnf(658,plain,
( X1 = ext(X2,X3,X3,X1)
| ~ s_t(X3,X1,X4)
| ~ s_e(X4,X1,X4,ext(X2,X3,X3,X1)) ),
inference(spm,[status(thm)],[160,330,theory(equality)]) ).
cnf(796,plain,
( s_e(ext(ext(X1,X2,alpha,gamma),X2,X3,X4),X1,ins(X2,X1,X3,X4),X4)
| ~ le(X3,X4,X2,X1) ),
inference(spm,[status(thm)],[653,284,theory(equality)]) ).
cnf(846,plain,
( s_t(ext(X1,X2,X3,X4),X2,X5)
| ~ s_t(X1,X5,X2) ),
inference(spm,[status(thm)],[197,336,theory(equality)]) ).
cnf(950,plain,
( ext(X1,X2,X1,X3) = ins(X2,X3,X1,X2)
| ext(X3,X2,alpha,gamma) = X2
| ~ le(X1,X2,X2,X3)
| ~ s_t(ext(X3,X2,alpha,gamma),X2,X1) ),
inference(spm,[status(thm)],[284,423,theory(equality)]) ).
cnf(965,plain,
( ext(X1,X2,X1,X3) = ins(X2,X3,X1,X2)
| ~ le(X1,X2,X2,X3)
| ~ s_t(ext(X3,X2,alpha,gamma),X2,X1) ),
inference(sr,[status(thm)],[950,219,theory(equality)]) ).
cnf(1125,plain,
( ins(X2,X1,X1,X2) = X2
| ~ le(X1,X2,X2,X1)
| ~ s_t(ext(X1,X2,alpha,gamma),X2,X1) ),
inference(spm,[status(thm)],[324,965,theory(equality)]) ).
cnf(1126,plain,
( s_e(X1,X2,X3,ins(X3,X2,X1,X3))
| ~ le(X1,X3,X3,X2)
| ~ s_t(ext(X2,X3,alpha,gamma),X3,X1) ),
inference(spm,[status(thm)],[330,965,theory(equality)]) ).
cnf(1141,plain,
( ext(X2,X1,X2,X1) = X2
| ~ le(X2,X1,X1,X1)
| ~ s_t(ext(X1,X1,alpha,gamma),X1,X2) ),
inference(spm,[status(thm)],[376,965,theory(equality)]) ).
cnf(1146,plain,
( ins(X2,X1,X1,X2) = X2
| ~ le(X1,X2,X2,X1)
| $false ),
inference(rw,[status(thm)],[1125,290,theory(equality)]) ).
cnf(1147,plain,
( ins(X2,X1,X1,X2) = X2
| ~ le(X1,X2,X2,X1) ),
inference(cn,[status(thm)],[1146,theory(equality)]) ).
cnf(1173,plain,
( s_t(X1,X2,X4)
| ~ le(X4,X2,X3,X3)
| ~ s_t(X1,X4,X4) ),
inference(spm,[status(thm)],[365,376,theory(equality)]) ).
cnf(1182,plain,
( s_t(X1,X2,X4)
| ~ le(X4,X2,X3,X3)
| $false ),
inference(rw,[status(thm)],[1173,199,theory(equality)]) ).
cnf(1183,plain,
( s_t(X1,X2,X4)
| ~ le(X4,X2,X3,X3) ),
inference(cn,[status(thm)],[1182,theory(equality)]) ).
cnf(1305,plain,
( s_e(X1,X2,X3,X4)
| ~ s_t(X3,ins(X3,X2,X5,X3),X4)
| ~ s_t(X1,X5,X2)
| ~ s_e(X1,X5,ins(X3,X2,X5,X3),X4)
| ~ le(X5,X3,X3,X2)
| ~ s_t(ext(X2,X3,alpha,gamma),X3,X5) ),
inference(spm,[status(thm)],[239,1126,theory(equality)]) ).
cnf(1473,plain,
( s_t(X1,X2,X3)
| ~ le(X2,X3,X4,X4)
| ~ s_t(X1,X2,X2) ),
inference(spm,[status(thm)],[370,376,theory(equality)]) ).
cnf(1484,plain,
( s_t(X1,X2,X3)
| ~ le(X2,X3,X4,X4)
| $false ),
inference(rw,[status(thm)],[1473,199,theory(equality)]) ).
cnf(1485,plain,
( s_t(X1,X2,X3)
| ~ le(X2,X3,X4,X4) ),
inference(cn,[status(thm)],[1484,theory(equality)]) ).
cnf(1844,plain,
( le(ins(X1,X2,X3,X4),X5,X2,X1)
| ~ s_t(ins(X1,X2,X3,X4),X5,X3)
| ~ le(X3,X4,X1,X2) ),
inference(spm,[status(thm)],[251,378,theory(equality)]) ).
cnf(1948,plain,
( ext(X1,X2,X1,X2) = X1
| ~ le(X1,X2,X2,X2)
| ~ s_t(X2,X1,X2) ),
inference(spm,[status(thm)],[1141,846,theory(equality)]) ).
cnf(2055,plain,
le(X1,ext(X2,X1,X3,X4),X3,X4),
inference(spm,[status(thm)],[384,199,theory(equality)]) ).
cnf(2070,plain,
( le(X1,X2,X3,X4)
| ~ s_t(X1,X2,X1) ),
inference(spm,[status(thm)],[384,374,theory(equality)]) ).
cnf(2101,plain,
( le(X1,X3,X3,X1)
| X2 = X1
| ~ s_t(X2,X1,X3) ),
inference(spm,[status(thm)],[2055,423,theory(equality)]) ).
cnf(2119,plain,
( le(ins(X1,X2,X3,X4),X4,X5,X6)
| ~ le(X3,X4,X1,X2)
| ~ s_t(X3,ins(X1,X2,X3,X4),X4) ),
inference(spm,[status(thm)],[2070,361,theory(equality)]) ).
cnf(2127,plain,
( le(X1,ins(X2,X3,X1,X4),X2,X3)
| ~ le(X1,X4,X2,X3) ),
inference(spm,[status(thm)],[385,199,theory(equality)]) ).
cnf(2152,plain,
( ext(X1,X2,X3,X4) = X2
| le(X2,X1,X1,X2) ),
inference(spm,[status(thm)],[2101,290,theory(equality)]) ).
cnf(2173,plain,
( s_e(X1,X1,X3,X4)
| le(X1,X2,X2,X1) ),
inference(spm,[status(thm)],[122,2152,theory(equality)]) ).
cnf(2236,plain,
( s_e(X1,X2,X3,X3)
| le(X3,X4,X4,X3) ),
inference(spm,[status(thm)],[209,2173,theory(equality)]) ).
cnf(2322,plain,
( X1 = X2
| le(X3,X4,X4,X3) ),
inference(spm,[status(thm)],[129,2236,theory(equality)]) ).
cnf(2455,plain,
( le(X4,X5,X5,X4)
| X3 != X2 ),
inference(spm,[status(thm)],[219,2322,theory(equality)]) ).
cnf(2603,plain,
le(X1,X2,X2,X1),
inference(er,[status(thm)],[2455,theory(equality)]) ).
cnf(2630,plain,
( ins(X1,X2,X2,X1) = X1
| $false ),
inference(rw,[status(thm)],[1147,2603,theory(equality)]) ).
cnf(2631,plain,
ins(X1,X2,X2,X1) = X1,
inference(cn,[status(thm)],[2630,theory(equality)]) ).
cnf(2753,plain,
( ext(X1,X2,X1,X2) = X1
| ~ le(X1,X2,X2,X2) ),
inference(csr,[status(thm)],[1948,1485]) ).
cnf(2759,plain,
( ext(X1,X2,X1,X2) = X1
| ~ s_t(X2,X1,X2) ),
inference(spm,[status(thm)],[2753,390,theory(equality)]) ).
cnf(3014,plain,
s_e(X1,ext(X2,X1,X3,ext(X4,X3,X5,X6)),X5,X6),
inference(spm,[status(thm)],[403,330,theory(equality)]) ).
cnf(3036,plain,
s_e(ext(X1,X2,X3,ext(X4,X3,X5,X6)),X2,X6,X5),
inference(spm,[status(thm)],[237,3014,theory(equality)]) ).
cnf(3585,plain,
( ext(X1,X2,X2,X3) = X3
| ~ s_t(X2,ext(X1,X2,X2,X3),X2) ),
inference(spm,[status(thm)],[421,122,theory(equality)]) ).
cnf(3952,plain,
( ext(X1,X2,X3,X3) = ins(X3,X3,X1,X2)
| ~ le(X1,X2,X3,X3) ),
inference(spm,[status(thm)],[284,430,theory(equality)]) ).
cnf(4008,plain,
( X2 = ins(X3,X3,X1,X2)
| ~ le(X1,X2,X3,X3) ),
inference(rw,[status(thm)],[3952,324,theory(equality)]) ).
cnf(4208,plain,
( X3 = X2
| ext(X1,X2,alpha,gamma) = X2
| ~ le(X3,X2,X2,X1)
| ~ s_t(X3,X2,X1)
| ~ s_t(ext(X1,X2,alpha,gamma),X2,X3) ),
inference(spm,[status(thm)],[432,423,theory(equality)]) ).
cnf(4222,plain,
( X3 = X2
| ~ le(X3,X2,X2,X1)
| ~ s_t(X3,X2,X1)
| ~ s_t(ext(X1,X2,alpha,gamma),X2,X3) ),
inference(sr,[status(thm)],[4208,219,theory(equality)]) ).
cnf(4759,plain,
( X1 = X2
| ~ le(X1,X2,X2,X3)
| ~ s_t(X1,X2,X3)
| ~ s_t(X3,X1,X2) ),
inference(spm,[status(thm)],[4222,846,theory(equality)]) ).
cnf(4860,plain,
( X1 = X2
| ~ s_t(X1,X2,X3)
| ~ s_t(X3,X1,X2)
| ~ s_t(X2,X1,X3) ),
inference(spm,[status(thm)],[4759,390,theory(equality)]) ).
cnf(4870,plain,
( X1 = X2
| ~ s_t(X1,X2,X3)
| ~ s_t(X3,X1,X2) ),
inference(csr,[status(thm)],[4860,197]) ).
cnf(4885,plain,
( X1 = X2
| ~ s_t(ext(X1,X3,X4,X5),X1,X2)
| ~ s_t(X1,X2,X3) ),
inference(spm,[status(thm)],[4870,374,theory(equality)]) ).
cnf(5218,negated_conjecture,
( esk1_0 = esk2_0
| s_t(esk1_0,ins(esk3_0,esk4_0,esk1_0,esk2_0),X1)
| s_t(esk1_0,X1,ins(esk3_0,esk4_0,esk1_0,esk2_0))
| ~ s_t(esk1_0,esk2_0,X1) ),
inference(spm,[status(thm)],[463,269,theory(equality)]) ).
cnf(5314,plain,
( X1 = X2
| ~ s_t(X1,X1,X2)
| ~ s_t(X1,X2,X3)
| ~ s_t(X3,X1,X3) ),
inference(spm,[status(thm)],[4885,2759,theory(equality)]) ).
cnf(5321,plain,
( X1 = X2
| $false
| ~ s_t(X1,X2,X3)
| ~ s_t(X3,X1,X3) ),
inference(rw,[status(thm)],[5314,195,theory(equality)]) ).
cnf(5322,plain,
( X1 = X2
| ~ s_t(X1,X2,X3)
| ~ s_t(X3,X1,X3) ),
inference(cn,[status(thm)],[5321,theory(equality)]) ).
cnf(5357,plain,
( le(X1,X2,X3,X4)
| ~ le(X2,X1,X4,X3) ),
inference(spm,[status(thm)],[465,127,theory(equality)]) ).
cnf(5358,plain,
( le(X1,X2,X3,X4)
| ~ le(X2,X1,X3,X4) ),
inference(spm,[status(thm)],[465,213,theory(equality)]) ).
cnf(5380,plain,
( le(X1,X2,X3,X4)
| ~ le(X2,X1,X5,ins(X3,X4,X5,X6))
| ~ le(X5,X6,X3,X4) ),
inference(spm,[status(thm)],[465,202,theory(equality)]) ).
cnf(5410,plain,
( X1 = ext(ext(X1,X2,alpha,gamma),X2,X3,X4)
| ~ s_t(X2,X1,X2)
| ~ le(X3,X4,X2,X1) ),
inference(spm,[status(thm)],[5322,431,theory(equality)]) ).
cnf(5596,plain,
( le(X1,X2,X3,X4)
| ~ s_e(ext(X6,X5,X1,X2),X5,X3,X4) ),
inference(spm,[status(thm)],[468,2603,theory(equality)]) ).
cnf(5653,plain,
le(X1,ext(X2,X1,X3,X4),X4,X3),
inference(spm,[status(thm)],[5596,3036,theory(equality)]) ).
cnf(5776,plain,
( le(X1,X2,X3,X4)
| ~ s_e(X2,X1,X3,X4) ),
inference(spm,[status(thm)],[468,5653,theory(equality)]) ).
cnf(5848,plain,
( s_t(X1,X2,X3)
| ~ s_e(X2,X3,X4,X4) ),
inference(spm,[status(thm)],[1183,5776,theory(equality)]) ).
cnf(7157,plain,
( s_t(X1,ins(X2,X2,X3,X4),X3)
| ~ le(X3,X4,X2,X2) ),
inference(spm,[status(thm)],[5848,378,theory(equality)]) ).
cnf(13264,plain,
le(X1,X2,X3,ext(X3,ext(X4,X3,X1,X2),X5,X6)),
inference(spm,[status(thm)],[655,123,theory(equality)]) ).
cnf(13276,plain,
( le(X1,X2,X3,ext(X3,X4,X5,X6))
| ~ s_t(X3,ext(X7,X3,X1,X2),X4) ),
inference(spm,[status(thm)],[655,374,theory(equality)]) ).
cnf(14473,plain,
( ext(X1,X2,X2,X3) = X3
| ~ s_t(X2,X3,X2) ),
inference(spm,[status(thm)],[658,330,theory(equality)]) ).
cnf(46581,plain,
( s_e(ext(ext(X1,X2,alpha,gamma),X2,X1,X2),X1,X2,X2)
| ~ le(X1,X2,X2,X1)
| ~ s_t(ext(X1,X2,alpha,gamma),X2,X1)
| ~ s_t(X2,ins(X2,X1,X1,X2),X2)
| ~ s_t(ext(ext(X1,X2,alpha,gamma),X2,X1,X2),X1,X1) ),
inference(spm,[status(thm)],[1305,796,theory(equality)]) ).
cnf(46615,plain,
( s_e(ext(ext(X1,X2,alpha,gamma),X2,X1,X2),X1,X2,X2)
| $false
| ~ s_t(ext(X1,X2,alpha,gamma),X2,X1)
| ~ s_t(X2,ins(X2,X1,X1,X2),X2)
| ~ s_t(ext(ext(X1,X2,alpha,gamma),X2,X1,X2),X1,X1) ),
inference(rw,[status(thm)],[46581,2603,theory(equality)]) ).
cnf(46616,plain,
( s_e(ext(ext(X1,X2,alpha,gamma),X2,X1,X2),X1,X2,X2)
| $false
| $false
| ~ s_t(X2,ins(X2,X1,X1,X2),X2)
| ~ s_t(ext(ext(X1,X2,alpha,gamma),X2,X1,X2),X1,X1) ),
inference(rw,[status(thm)],[46615,290,theory(equality)]) ).
cnf(46617,plain,
( s_e(ext(ext(X1,X2,alpha,gamma),X2,X1,X2),X1,X2,X2)
| $false
| $false
| $false
| ~ s_t(ext(ext(X1,X2,alpha,gamma),X2,X1,X2),X1,X1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[46616,2631,theory(equality)]),195,theory(equality)]) ).
cnf(46618,plain,
( s_e(ext(ext(X1,X2,alpha,gamma),X2,X1,X2),X1,X2,X2)
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[46617,199,theory(equality)]) ).
cnf(46619,plain,
s_e(ext(ext(X1,X2,alpha,gamma),X2,X1,X2),X1,X2,X2),
inference(cn,[status(thm)],[46618,theory(equality)]) ).
cnf(46646,plain,
ext(ext(X1,X2,alpha,gamma),X2,X1,X2) = X1,
inference(spm,[status(thm)],[129,46619,theory(equality)]) ).
cnf(46980,plain,
le(X1,X2,X2,ext(X2,X1,X3,X4)),
inference(spm,[status(thm)],[13264,46646,theory(equality)]) ).
cnf(48589,plain,
le(X1,X2,ext(X1,X2,X3,X4),X1),
inference(spm,[status(thm)],[5357,46980,theory(equality)]) ).
cnf(48659,plain,
( le(X1,X2,X3,X1)
| ~ s_t(X2,X3,X2) ),
inference(spm,[status(thm)],[48589,14473,theory(equality)]) ).
cnf(49582,plain,
( le(X1,X2,ins(X3,X3,X2,X4),X1)
| ~ le(X2,X4,X3,X3) ),
inference(spm,[status(thm)],[48659,7157,theory(equality)]) ).
cnf(55885,plain,
( le(X1,X2,X4,X1)
| ~ le(X2,X4,X3,X3) ),
inference(spm,[status(thm)],[49582,4008,theory(equality)]) ).
cnf(70860,plain,
( le(ins(X1,X2,X3,X4),X4,X2,X1)
| ~ le(X3,X4,X1,X2) ),
inference(spm,[status(thm)],[1844,359,theory(equality)]) ).
cnf(364306,negated_conjecture,
( esk2_0 = esk1_0
| s_t(esk1_0,esk2_0,ins(esk3_0,esk4_0,esk1_0,esk2_0))
| s_t(esk1_0,ins(esk3_0,esk4_0,esk1_0,esk2_0),esk2_0) ),
inference(spm,[status(thm)],[5218,199,theory(equality)]) ).
cnf(399801,plain,
( X1 = X3
| ~ s_t(X2,X1,X2)
| ~ le(X2,X3,X2,X1) ),
inference(spm,[status(thm)],[3585,5410,theory(equality)]) ).
cnf(401423,plain,
( X1 = ins(X2,X1,X2,X3)
| ~ s_t(X2,X1,X2)
| ~ le(X2,X3,X2,X1) ),
inference(spm,[status(thm)],[399801,2127,theory(equality)]) ).
cnf(566461,negated_conjecture,
( le(ins(esk3_0,esk4_0,esk1_0,esk2_0),esk2_0,X1,X2)
| esk2_0 = esk1_0
| s_t(esk1_0,esk2_0,ins(esk3_0,esk4_0,esk1_0,esk2_0))
| ~ le(esk1_0,esk2_0,esk3_0,esk4_0) ),
inference(spm,[status(thm)],[2119,364306,theory(equality)]) ).
cnf(566580,negated_conjecture,
( le(ins(esk3_0,esk4_0,esk1_0,esk2_0),esk2_0,X1,X2)
| esk2_0 = esk1_0
| s_t(esk1_0,esk2_0,ins(esk3_0,esk4_0,esk1_0,esk2_0))
| $false ),
inference(rw,[status(thm)],[566461,269,theory(equality)]) ).
cnf(566581,negated_conjecture,
( le(ins(esk3_0,esk4_0,esk1_0,esk2_0),esk2_0,X1,X2)
| esk2_0 = esk1_0
| s_t(esk1_0,esk2_0,ins(esk3_0,esk4_0,esk1_0,esk2_0)) ),
inference(cn,[status(thm)],[566580,theory(equality)]) ).
cnf(632242,negated_conjecture,
( le(X1,ins(esk3_0,esk4_0,esk1_0,esk2_0),esk2_0,X1)
| esk2_0 = esk1_0
| s_t(esk1_0,esk2_0,ins(esk3_0,esk4_0,esk1_0,esk2_0)) ),
inference(spm,[status(thm)],[55885,566581,theory(equality)]) ).
cnf(664591,plain,
( le(X2,X3,X2,X1)
| ~ le(X1,X3,X1,X2)
| ~ s_t(X1,X2,X1) ),
inference(spm,[status(thm)],[70860,401423,theory(equality)]) ).
cnf(673374,negated_conjecture,
( le(esk2_0,ins(esk3_0,esk4_0,esk1_0,esk2_0),esk2_0,esk2_0)
| esk2_0 = esk1_0
| s_t(esk1_0,esk2_0,ins(esk3_0,esk4_0,esk1_0,esk2_0))
| ~ s_t(esk2_0,esk2_0,esk2_0) ),
inference(spm,[status(thm)],[664591,632242,theory(equality)]) ).
cnf(673573,negated_conjecture,
( le(esk2_0,ins(esk3_0,esk4_0,esk1_0,esk2_0),esk2_0,esk2_0)
| esk2_0 = esk1_0
| s_t(esk1_0,esk2_0,ins(esk3_0,esk4_0,esk1_0,esk2_0))
| $false ),
inference(rw,[status(thm)],[673374,195,theory(equality)]) ).
cnf(673574,negated_conjecture,
( le(esk2_0,ins(esk3_0,esk4_0,esk1_0,esk2_0),esk2_0,esk2_0)
| esk2_0 = esk1_0
| s_t(esk1_0,esk2_0,ins(esk3_0,esk4_0,esk1_0,esk2_0)) ),
inference(cn,[status(thm)],[673573,theory(equality)]) ).
cnf(682610,negated_conjecture,
( esk2_0 = esk1_0
| s_t(esk1_0,esk2_0,ins(esk3_0,esk4_0,esk1_0,esk2_0)) ),
inference(csr,[status(thm)],[673574,1485]) ).
cnf(682629,negated_conjecture,
( s_t(esk3_0,ext(ext(esk4_0,esk3_0,alpha,gamma),esk3_0,esk1_0,esk2_0),esk4_0)
| esk2_0 = esk1_0
| ~ le(esk1_0,esk2_0,esk3_0,esk4_0) ),
inference(spm,[status(thm)],[504,682610,theory(equality)]) ).
cnf(682767,negated_conjecture,
( s_t(esk3_0,ext(ext(esk4_0,esk3_0,alpha,gamma),esk3_0,esk1_0,esk2_0),esk4_0)
| esk2_0 = esk1_0
| $false ),
inference(rw,[status(thm)],[682629,269,theory(equality)]) ).
cnf(682768,negated_conjecture,
( s_t(esk3_0,ext(ext(esk4_0,esk3_0,alpha,gamma),esk3_0,esk1_0,esk2_0),esk4_0)
| esk2_0 = esk1_0 ),
inference(cn,[status(thm)],[682767,theory(equality)]) ).
cnf(1593765,negated_conjecture,
( le(esk1_0,esk2_0,esk3_0,ext(esk3_0,esk4_0,X1,X2))
| esk2_0 = esk1_0 ),
inference(spm,[status(thm)],[13276,682768,theory(equality)]) ).
cnf(1593936,negated_conjecture,
( esk2_0 = esk1_0
| le(esk1_0,esk2_0,esk3_0,ins(X2,X1,esk3_0,esk4_0))
| ~ le(esk3_0,esk4_0,X2,X1) ),
inference(spm,[status(thm)],[1593765,284,theory(equality)]) ).
cnf(1777628,negated_conjecture,
( le(esk2_0,esk1_0,X1,X2)
| esk2_0 = esk1_0
| ~ le(esk3_0,esk4_0,X1,X2) ),
inference(spm,[status(thm)],[5380,1593936,theory(equality)]) ).
cnf(1778019,negated_conjecture,
( esk2_0 = esk1_0
| le(esk2_0,esk1_0,esk5_0,esk6_0) ),
inference(spm,[status(thm)],[1777628,268,theory(equality)]) ).
cnf(1778713,negated_conjecture,
( le(esk1_0,esk2_0,esk5_0,esk6_0)
| esk2_0 = esk1_0 ),
inference(spm,[status(thm)],[5358,1778019,theory(equality)]) ).
cnf(1778766,negated_conjecture,
esk2_0 = esk1_0,
inference(sr,[status(thm)],[1778713,267,theory(equality)]) ).
cnf(1778785,negated_conjecture,
$false,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[267,1778766,theory(equality)]),396,theory(equality)]) ).
cnf(1778786,negated_conjecture,
$false,
inference(cn,[status(thm)],[1778785,theory(equality)]) ).
cnf(1778787,negated_conjecture,
$false,
1778786,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO494+1 : TPTP v7.0.0. Released v7.0.0.
% 0.00/0.04 % Command : Source/sine.py -e eprover -t %d %s
% 0.03/0.24 % Computer : n099.star.cs.uiowa.edu
% 0.03/0.24 % Model : x86_64 x86_64
% 0.03/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.03/0.24 % Memory : 32218.75MB
% 0.03/0.24 % OS : Linux 3.10.0-327.36.3.el7.x86_64
% 0.03/0.24 % CPULimit : 300
% 0.03/0.24 % DateTime : Fri Jan 20 05:32:49 CST 2017
% 0.03/0.24 % CPUTime :
% 0.09/2.01 % SZS status Started for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/2.01 --creating new selector for [GEO011+0.ax]
% 29.11/31.25 eprover: CPU time limit exceeded, terminating
% 94.64/99.25 -running prover on /export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_1 with time limit 29
% 94.64/99.25 -running prover with command ['/export/starexec/sandbox2/solver/bin/Source/./Source/PROVER/eproof.working', '-s', '-tLPO4', '-xAuto', '-tAuto', '--memory-limit=768', '--tptp3-format', '--cpu-limit=29', '/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_1']
% 94.64/99.25 -prover status ResourceOut
% 94.64/99.25 -running prover on /export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2 with time limit 80
% 94.64/99.25 -running prover with command ['/export/starexec/sandbox2/solver/bin/Source/./Source/PROVER/eproof.working', '-s', '-tLPO4', '-xAuto', '-tAuto', '--memory-limit=768', '--tptp3-format', '--cpu-limit=80', '/export/starexec/sandbox2/tmp/tmpKm_JmG/sel_theBenchmark.p_2']
% 94.64/99.25 -prover status Theorem
% 94.64/99.25 Problem theBenchmark.p solved in phase 1.
% 94.64/99.25 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 94.64/99.25 % SZS status Ended for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 94.64/99.25 Solved 1 out of 1.
% 94.64/99.25 # Problem is unsatisfiable (or provable), constructing proof object
% 94.64/99.25 # SZS status Theorem
% 94.64/99.25 # SZS output start CNFRefutation.
% See solution above
% 94.71/99.27 # SZS output end CNFRefutation
%------------------------------------------------------------------------------