%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : SWC153+1 : TPTP v5.0.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art09.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Sun Dec 26 10:24:07 EST 2010
% Result : Theorem 0.32s
% Output : CNFRefutation 0.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 2
% Syntax : Number of formulae : 73 ( 17 unt; 0 def)
% Number of atoms : 525 ( 54 equ)
% Maximal formula atoms : 48 ( 7 avg)
% Number of connectives : 742 ( 290 ~; 295 |; 124 &)
% ( 0 <=>; 33 =>; 0 <=; 0 <~>)
% Maximal formula depth : 31 ( 7 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 11 con; 0-2 aty)
% Number of variables : 133 ( 0 sgn 68 !; 38 ?)
% Comments :
%------------------------------------------------------------------------------
fof(6,axiom,
! [X1] :
( ssItem(X1)
=> ! [X2] :
( ssItem(X2)
=> ( ( leq(X1,X2)
& leq(X2,X1) )
=> X1 = X2 ) ) ),
file('/tmp/tmp8Rj2-E/sel_SWC153+1.p_1',ax29) ).
fof(24,conjecture,
! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> ! [X3] :
( ssList(X3)
=> ! [X4] :
( ssList(X4)
=> ( X4 != X2
| X3 != X1
| ? [X5] :
( ssItem(X5)
& ? [X6] :
( ssItem(X6)
& ? [X7] :
( ssList(X7)
& ? [X8] :
( ssList(X8)
& ? [X9] :
( ssList(X9)
& app(app(app(app(X7,cons(X5,nil)),X8),cons(X6,nil)),X9) = X3
& leq(X6,X5)
& ( ~ leq(X5,X6)
| ? [X10] :
( ssItem(X10)
& memberP(X8,X10)
& ( ~ leq(X5,X10)
| ~ leq(X10,X6) ) ) ) ) ) ) ) )
| ! [X11] :
( ssItem(X11)
=> ! [X12] :
( ssItem(X12)
=> ! [X13] :
( ssList(X13)
=> ! [X14] :
( ssList(X14)
=> ! [X15] :
( ssList(X15)
=> ( app(app(app(app(X13,cons(X11,nil)),X14),cons(X12,nil)),X15) != X1
| ~ leq(X12,X11)
| ( ! [X16] :
( ssItem(X16)
=> ( ~ memberP(X14,X16)
| ( leq(X16,X12)
& leq(X11,X16) ) ) )
& leq(X11,X12) ) ) ) ) ) ) ) ) ) ) ) ),
file('/tmp/tmp8Rj2-E/sel_SWC153+1.p_1',co1) ).
fof(25,negated_conjecture,
~ ! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> ! [X3] :
( ssList(X3)
=> ! [X4] :
( ssList(X4)
=> ( X4 != X2
| X3 != X1
| ? [X5] :
( ssItem(X5)
& ? [X6] :
( ssItem(X6)
& ? [X7] :
( ssList(X7)
& ? [X8] :
( ssList(X8)
& ? [X9] :
( ssList(X9)
& app(app(app(app(X7,cons(X5,nil)),X8),cons(X6,nil)),X9) = X3
& leq(X6,X5)
& ( ~ leq(X5,X6)
| ? [X10] :
( ssItem(X10)
& memberP(X8,X10)
& ( ~ leq(X5,X10)
| ~ leq(X10,X6) ) ) ) ) ) ) ) )
| ! [X11] :
( ssItem(X11)
=> ! [X12] :
( ssItem(X12)
=> ! [X13] :
( ssList(X13)
=> ! [X14] :
( ssList(X14)
=> ! [X15] :
( ssList(X15)
=> ( app(app(app(app(X13,cons(X11,nil)),X14),cons(X12,nil)),X15) != X1
| ~ leq(X12,X11)
| ( ! [X16] :
( ssItem(X16)
=> ( ~ memberP(X14,X16)
| ( leq(X16,X12)
& leq(X11,X16) ) ) )
& leq(X11,X12) ) ) ) ) ) ) ) ) ) ) ) ),
inference(assume_negation,[status(cth)],[24]) ).
fof(27,negated_conjecture,
~ ! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> ! [X3] :
( ssList(X3)
=> ! [X4] :
( ssList(X4)
=> ( X4 != X2
| X3 != X1
| ? [X5] :
( ssItem(X5)
& ? [X6] :
( ssItem(X6)
& ? [X7] :
( ssList(X7)
& ? [X8] :
( ssList(X8)
& ? [X9] :
( ssList(X9)
& app(app(app(app(X7,cons(X5,nil)),X8),cons(X6,nil)),X9) = X3
& leq(X6,X5)
& ( ~ leq(X5,X6)
| ? [X10] :
( ssItem(X10)
& memberP(X8,X10)
& ( ~ leq(X5,X10)
| ~ leq(X10,X6) ) ) ) ) ) ) ) )
| ! [X11] :
( ssItem(X11)
=> ! [X12] :
( ssItem(X12)
=> ! [X13] :
( ssList(X13)
=> ! [X14] :
( ssList(X14)
=> ! [X15] :
( ssList(X15)
=> ( app(app(app(app(X13,cons(X11,nil)),X14),cons(X12,nil)),X15) != X1
| ~ leq(X12,X11)
| ( ! [X16] :
( ssItem(X16)
=> ( ~ memberP(X14,X16)
| ( leq(X16,X12)
& leq(X11,X16) ) ) )
& leq(X11,X12) ) ) ) ) ) ) ) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[25,theory(equality)]) ).
fof(50,plain,
! [X1] :
( ~ ssItem(X1)
| ! [X2] :
( ~ ssItem(X2)
| ~ leq(X1,X2)
| ~ leq(X2,X1)
| X1 = X2 ) ),
inference(fof_nnf,[status(thm)],[6]) ).
fof(51,plain,
! [X3] :
( ~ ssItem(X3)
| ! [X4] :
( ~ ssItem(X4)
| ~ leq(X3,X4)
| ~ leq(X4,X3)
| X3 = X4 ) ),
inference(variable_rename,[status(thm)],[50]) ).
fof(52,plain,
! [X3,X4] :
( ~ ssItem(X4)
| ~ leq(X3,X4)
| ~ leq(X4,X3)
| X3 = X4
| ~ ssItem(X3) ),
inference(shift_quantors,[status(thm)],[51]) ).
cnf(53,plain,
( X1 = X2
| ~ ssItem(X1)
| ~ leq(X2,X1)
| ~ leq(X1,X2)
| ~ ssItem(X2) ),
inference(split_conjunct,[status(thm)],[52]) ).
fof(133,negated_conjecture,
? [X1] :
( ssList(X1)
& ? [X2] :
( ssList(X2)
& ? [X3] :
( ssList(X3)
& ? [X4] :
( ssList(X4)
& X4 = X2
& X3 = X1
& ! [X5] :
( ~ ssItem(X5)
| ! [X6] :
( ~ ssItem(X6)
| ! [X7] :
( ~ ssList(X7)
| ! [X8] :
( ~ ssList(X8)
| ! [X9] :
( ~ ssList(X9)
| app(app(app(app(X7,cons(X5,nil)),X8),cons(X6,nil)),X9) != X3
| ~ leq(X6,X5)
| ( leq(X5,X6)
& ! [X10] :
( ~ ssItem(X10)
| ~ memberP(X8,X10)
| ( leq(X5,X10)
& leq(X10,X6) ) ) ) ) ) ) ) )
& ? [X11] :
( ssItem(X11)
& ? [X12] :
( ssItem(X12)
& ? [X13] :
( ssList(X13)
& ? [X14] :
( ssList(X14)
& ? [X15] :
( ssList(X15)
& app(app(app(app(X13,cons(X11,nil)),X14),cons(X12,nil)),X15) = X1
& leq(X12,X11)
& ( ? [X16] :
( ssItem(X16)
& memberP(X14,X16)
& ( ~ leq(X16,X12)
| ~ leq(X11,X16) ) )
| ~ leq(X11,X12) ) ) ) ) ) ) ) ) ) ),
inference(fof_nnf,[status(thm)],[27]) ).
fof(134,negated_conjecture,
? [X17] :
( ssList(X17)
& ? [X18] :
( ssList(X18)
& ? [X19] :
( ssList(X19)
& ? [X20] :
( ssList(X20)
& X20 = X18
& X19 = X17
& ! [X21] :
( ~ ssItem(X21)
| ! [X22] :
( ~ ssItem(X22)
| ! [X23] :
( ~ ssList(X23)
| ! [X24] :
( ~ ssList(X24)
| ! [X25] :
( ~ ssList(X25)
| app(app(app(app(X23,cons(X21,nil)),X24),cons(X22,nil)),X25) != X19
| ~ leq(X22,X21)
| ( leq(X21,X22)
& ! [X26] :
( ~ ssItem(X26)
| ~ memberP(X24,X26)
| ( leq(X21,X26)
& leq(X26,X22) ) ) ) ) ) ) ) )
& ? [X27] :
( ssItem(X27)
& ? [X28] :
( ssItem(X28)
& ? [X29] :
( ssList(X29)
& ? [X30] :
( ssList(X30)
& ? [X31] :
( ssList(X31)
& app(app(app(app(X29,cons(X27,nil)),X30),cons(X28,nil)),X31) = X17
& leq(X28,X27)
& ( ? [X32] :
( ssItem(X32)
& memberP(X30,X32)
& ( ~ leq(X32,X28)
| ~ leq(X27,X32) ) )
| ~ leq(X27,X28) ) ) ) ) ) ) ) ) ) ),
inference(variable_rename,[status(thm)],[133]) ).
fof(135,negated_conjecture,
( ssList(esk7_0)
& ssList(esk8_0)
& ssList(esk9_0)
& ssList(esk10_0)
& esk10_0 = esk8_0
& esk9_0 = esk7_0
& ! [X21] :
( ~ ssItem(X21)
| ! [X22] :
( ~ ssItem(X22)
| ! [X23] :
( ~ ssList(X23)
| ! [X24] :
( ~ ssList(X24)
| ! [X25] :
( ~ ssList(X25)
| app(app(app(app(X23,cons(X21,nil)),X24),cons(X22,nil)),X25) != esk9_0
| ~ leq(X22,X21)
| ( leq(X21,X22)
& ! [X26] :
( ~ ssItem(X26)
| ~ memberP(X24,X26)
| ( leq(X21,X26)
& leq(X26,X22) ) ) ) ) ) ) ) )
& ssItem(esk11_0)
& ssItem(esk12_0)
& ssList(esk13_0)
& ssList(esk14_0)
& ssList(esk15_0)
& app(app(app(app(esk13_0,cons(esk11_0,nil)),esk14_0),cons(esk12_0,nil)),esk15_0) = esk7_0
& leq(esk12_0,esk11_0)
& ( ( ssItem(esk16_0)
& memberP(esk14_0,esk16_0)
& ( ~ leq(esk16_0,esk12_0)
| ~ leq(esk11_0,esk16_0) ) )
| ~ leq(esk11_0,esk12_0) ) ),
inference(skolemize,[status(esa)],[134]) ).
fof(136,negated_conjecture,
! [X21,X22,X23,X24,X25,X26] :
( ( ( ( ~ ssItem(X26)
| ~ memberP(X24,X26)
| ( leq(X21,X26)
& leq(X26,X22) ) )
& leq(X21,X22) )
| ~ ssList(X25)
| app(app(app(app(X23,cons(X21,nil)),X24),cons(X22,nil)),X25) != esk9_0
| ~ leq(X22,X21)
| ~ ssList(X24)
| ~ ssList(X23)
| ~ ssItem(X22)
| ~ ssItem(X21) )
& esk10_0 = esk8_0
& esk9_0 = esk7_0
& ssItem(esk11_0)
& ssItem(esk12_0)
& ssList(esk13_0)
& ssList(esk14_0)
& ssList(esk15_0)
& app(app(app(app(esk13_0,cons(esk11_0,nil)),esk14_0),cons(esk12_0,nil)),esk15_0) = esk7_0
& leq(esk12_0,esk11_0)
& ( ( ssItem(esk16_0)
& memberP(esk14_0,esk16_0)
& ( ~ leq(esk16_0,esk12_0)
| ~ leq(esk11_0,esk16_0) ) )
| ~ leq(esk11_0,esk12_0) )
& ssList(esk10_0)
& ssList(esk9_0)
& ssList(esk8_0)
& ssList(esk7_0) ),
inference(shift_quantors,[status(thm)],[135]) ).
fof(137,negated_conjecture,
! [X21,X22,X23,X24,X25,X26] :
( ( leq(X21,X26)
| ~ ssItem(X26)
| ~ memberP(X24,X26)
| ~ ssList(X25)
| app(app(app(app(X23,cons(X21,nil)),X24),cons(X22,nil)),X25) != esk9_0
| ~ leq(X22,X21)
| ~ ssList(X24)
| ~ ssList(X23)
| ~ ssItem(X22)
| ~ ssItem(X21) )
& ( leq(X26,X22)
| ~ ssItem(X26)
| ~ memberP(X24,X26)
| ~ ssList(X25)
| app(app(app(app(X23,cons(X21,nil)),X24),cons(X22,nil)),X25) != esk9_0
| ~ leq(X22,X21)
| ~ ssList(X24)
| ~ ssList(X23)
| ~ ssItem(X22)
| ~ ssItem(X21) )
& ( leq(X21,X22)
| ~ ssList(X25)
| app(app(app(app(X23,cons(X21,nil)),X24),cons(X22,nil)),X25) != esk9_0
| ~ leq(X22,X21)
| ~ ssList(X24)
| ~ ssList(X23)
| ~ ssItem(X22)
| ~ ssItem(X21) )
& esk10_0 = esk8_0
& esk9_0 = esk7_0
& ssItem(esk11_0)
& ssItem(esk12_0)
& ssList(esk13_0)
& ssList(esk14_0)
& ssList(esk15_0)
& app(app(app(app(esk13_0,cons(esk11_0,nil)),esk14_0),cons(esk12_0,nil)),esk15_0) = esk7_0
& leq(esk12_0,esk11_0)
& ( ssItem(esk16_0)
| ~ leq(esk11_0,esk12_0) )
& ( memberP(esk14_0,esk16_0)
| ~ leq(esk11_0,esk12_0) )
& ( ~ leq(esk16_0,esk12_0)
| ~ leq(esk11_0,esk16_0)
| ~ leq(esk11_0,esk12_0) )
& ssList(esk10_0)
& ssList(esk9_0)
& ssList(esk8_0)
& ssList(esk7_0) ),
inference(distribute,[status(thm)],[136]) ).
cnf(142,negated_conjecture,
( ~ leq(esk11_0,esk12_0)
| ~ leq(esk11_0,esk16_0)
| ~ leq(esk16_0,esk12_0) ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(143,negated_conjecture,
( memberP(esk14_0,esk16_0)
| ~ leq(esk11_0,esk12_0) ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(144,negated_conjecture,
( ssItem(esk16_0)
| ~ leq(esk11_0,esk12_0) ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(145,negated_conjecture,
leq(esk12_0,esk11_0),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(146,negated_conjecture,
app(app(app(app(esk13_0,cons(esk11_0,nil)),esk14_0),cons(esk12_0,nil)),esk15_0) = esk7_0,
inference(split_conjunct,[status(thm)],[137]) ).
cnf(147,negated_conjecture,
ssList(esk15_0),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(148,negated_conjecture,
ssList(esk14_0),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(149,negated_conjecture,
ssList(esk13_0),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(150,negated_conjecture,
ssItem(esk12_0),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(151,negated_conjecture,
ssItem(esk11_0),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(152,negated_conjecture,
esk9_0 = esk7_0,
inference(split_conjunct,[status(thm)],[137]) ).
cnf(154,negated_conjecture,
( leq(X1,X2)
| ~ ssItem(X1)
| ~ ssItem(X2)
| ~ ssList(X3)
| ~ ssList(X4)
| ~ leq(X2,X1)
| app(app(app(app(X3,cons(X1,nil)),X4),cons(X2,nil)),X5) != esk9_0
| ~ ssList(X5) ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(155,negated_conjecture,
( leq(X6,X2)
| ~ ssItem(X1)
| ~ ssItem(X2)
| ~ ssList(X3)
| ~ ssList(X4)
| ~ leq(X2,X1)
| app(app(app(app(X3,cons(X1,nil)),X4),cons(X2,nil)),X5) != esk9_0
| ~ ssList(X5)
| ~ memberP(X4,X6)
| ~ ssItem(X6) ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(156,negated_conjecture,
( leq(X1,X6)
| ~ ssItem(X1)
| ~ ssItem(X2)
| ~ ssList(X3)
| ~ ssList(X4)
| ~ leq(X2,X1)
| app(app(app(app(X3,cons(X1,nil)),X4),cons(X2,nil)),X5) != esk9_0
| ~ ssList(X5)
| ~ memberP(X4,X6)
| ~ ssItem(X6) ),
inference(split_conjunct,[status(thm)],[137]) ).
cnf(181,negated_conjecture,
app(app(app(app(esk13_0,cons(esk11_0,nil)),esk14_0),cons(esk12_0,nil)),esk15_0) = esk9_0,
inference(rw,[status(thm)],[146,152,theory(equality)]) ).
cnf(354,negated_conjecture,
( leq(esk11_0,esk12_0)
| ~ leq(esk12_0,esk11_0)
| ~ ssItem(esk12_0)
| ~ ssItem(esk11_0)
| ~ ssList(esk15_0)
| ~ ssList(esk14_0)
| ~ ssList(esk13_0) ),
inference(spm,[status(thm)],[154,181,theory(equality)]) ).
cnf(369,negated_conjecture,
( leq(esk11_0,esk12_0)
| $false
| ~ ssItem(esk12_0)
| ~ ssItem(esk11_0)
| ~ ssList(esk15_0)
| ~ ssList(esk14_0)
| ~ ssList(esk13_0) ),
inference(rw,[status(thm)],[354,145,theory(equality)]) ).
cnf(370,negated_conjecture,
( leq(esk11_0,esk12_0)
| $false
| $false
| ~ ssItem(esk11_0)
| ~ ssList(esk15_0)
| ~ ssList(esk14_0)
| ~ ssList(esk13_0) ),
inference(rw,[status(thm)],[369,150,theory(equality)]) ).
cnf(371,negated_conjecture,
( leq(esk11_0,esk12_0)
| $false
| $false
| $false
| ~ ssList(esk15_0)
| ~ ssList(esk14_0)
| ~ ssList(esk13_0) ),
inference(rw,[status(thm)],[370,151,theory(equality)]) ).
cnf(372,negated_conjecture,
( leq(esk11_0,esk12_0)
| ~ ssList(esk15_0)
| ~ ssList(esk14_0)
| ~ ssList(esk13_0) ),
inference(cn,[status(thm)],[371,theory(equality)]) ).
cnf(466,negated_conjecture,
( esk12_0 = esk11_0
| ~ leq(esk12_0,esk11_0)
| ~ ssItem(esk11_0)
| ~ ssItem(esk12_0)
| ~ ssList(esk15_0)
| ~ ssList(esk14_0)
| ~ ssList(esk13_0) ),
inference(spm,[status(thm)],[53,372,theory(equality)]) ).
cnf(470,negated_conjecture,
( esk12_0 = esk11_0
| $false
| ~ ssItem(esk11_0)
| ~ ssItem(esk12_0)
| ~ ssList(esk15_0)
| ~ ssList(esk14_0)
| ~ ssList(esk13_0) ),
inference(rw,[status(thm)],[466,145,theory(equality)]) ).
cnf(471,negated_conjecture,
( esk12_0 = esk11_0
| $false
| $false
| ~ ssItem(esk12_0)
| ~ ssList(esk15_0)
| ~ ssList(esk14_0)
| ~ ssList(esk13_0) ),
inference(rw,[status(thm)],[470,151,theory(equality)]) ).
cnf(472,negated_conjecture,
( esk12_0 = esk11_0
| $false
| $false
| $false
| ~ ssList(esk15_0)
| ~ ssList(esk14_0)
| ~ ssList(esk13_0) ),
inference(rw,[status(thm)],[471,150,theory(equality)]) ).
cnf(473,negated_conjecture,
( esk12_0 = esk11_0
| ~ ssList(esk15_0)
| ~ ssList(esk14_0)
| ~ ssList(esk13_0) ),
inference(cn,[status(thm)],[472,theory(equality)]) ).
cnf(479,negated_conjecture,
( esk12_0 = esk11_0
| ~ ssList(esk14_0)
| ~ ssList(esk13_0) ),
inference(spm,[status(thm)],[473,147,theory(equality)]) ).
cnf(480,negated_conjecture,
( esk12_0 = esk11_0
| ~ ssList(esk14_0) ),
inference(spm,[status(thm)],[479,149,theory(equality)]) ).
cnf(502,negated_conjecture,
esk12_0 = esk11_0,
inference(spm,[status(thm)],[480,148,theory(equality)]) ).
cnf(503,negated_conjecture,
app(app(app(app(esk13_0,cons(esk11_0,nil)),esk14_0),cons(esk11_0,nil)),esk15_0) = esk9_0,
inference(rw,[status(thm)],[181,502,theory(equality)]) ).
cnf(504,negated_conjecture,
leq(esk11_0,esk11_0),
inference(rw,[status(thm)],[145,502,theory(equality)]) ).
cnf(514,negated_conjecture,
( ~ leq(esk11_0,esk11_0)
| ~ leq(esk11_0,esk16_0)
| ~ leq(esk16_0,esk12_0) ),
inference(rw,[status(thm)],[142,502,theory(equality)]) ).
cnf(515,negated_conjecture,
( ~ leq(esk11_0,esk11_0)
| ~ leq(esk11_0,esk16_0)
| ~ leq(esk16_0,esk11_0) ),
inference(rw,[status(thm)],[514,502,theory(equality)]) ).
cnf(516,negated_conjecture,
( memberP(esk14_0,esk16_0)
| ~ leq(esk11_0,esk11_0) ),
inference(rw,[status(thm)],[143,502,theory(equality)]) ).
cnf(517,negated_conjecture,
( ssItem(esk16_0)
| ~ leq(esk11_0,esk11_0) ),
inference(rw,[status(thm)],[144,502,theory(equality)]) ).
cnf(521,negated_conjecture,
( ssItem(esk16_0)
| $false ),
inference(rw,[status(thm)],[517,504,theory(equality)]) ).
cnf(522,negated_conjecture,
ssItem(esk16_0),
inference(cn,[status(thm)],[521,theory(equality)]) ).
cnf(545,negated_conjecture,
( leq(X1,esk11_0)
| ~ memberP(esk14_0,X1)
| ~ leq(esk11_0,esk11_0)
| ~ ssItem(X1)
| ~ ssItem(esk11_0)
| ~ ssList(esk15_0)
| ~ ssList(esk14_0)
| ~ ssList(esk13_0) ),
inference(spm,[status(thm)],[155,503,theory(equality)]) ).
cnf(547,negated_conjecture,
( leq(esk11_0,X1)
| ~ memberP(esk14_0,X1)
| ~ leq(esk11_0,esk11_0)
| ~ ssItem(X1)
| ~ ssItem(esk11_0)
| ~ ssList(esk15_0)
| ~ ssList(esk14_0)
| ~ ssList(esk13_0) ),
inference(spm,[status(thm)],[156,503,theory(equality)]) ).
cnf(557,negated_conjecture,
( leq(X1,esk11_0)
| ~ memberP(esk14_0,X1)
| $false
| ~ ssItem(X1)
| ~ ssItem(esk11_0)
| ~ ssList(esk15_0)
| ~ ssList(esk14_0)
| ~ ssList(esk13_0) ),
inference(rw,[status(thm)],[545,504,theory(equality)]) ).
cnf(558,negated_conjecture,
( leq(X1,esk11_0)
| ~ memberP(esk14_0,X1)
| $false
| ~ ssItem(X1)
| $false
| ~ ssList(esk15_0)
| ~ ssList(esk14_0)
| ~ ssList(esk13_0) ),
inference(rw,[status(thm)],[557,151,theory(equality)]) ).
cnf(559,negated_conjecture,
( leq(X1,esk11_0)
| ~ memberP(esk14_0,X1)
| ~ ssItem(X1)
| ~ ssList(esk15_0)
| ~ ssList(esk14_0)
| ~ ssList(esk13_0) ),
inference(cn,[status(thm)],[558,theory(equality)]) ).
cnf(562,negated_conjecture,
( leq(esk11_0,X1)
| ~ memberP(esk14_0,X1)
| $false
| ~ ssItem(X1)
| ~ ssItem(esk11_0)
| ~ ssList(esk15_0)
| ~ ssList(esk14_0)
| ~ ssList(esk13_0) ),
inference(rw,[status(thm)],[547,504,theory(equality)]) ).
cnf(563,negated_conjecture,
( leq(esk11_0,X1)
| ~ memberP(esk14_0,X1)
| $false
| ~ ssItem(X1)
| $false
| ~ ssList(esk15_0)
| ~ ssList(esk14_0)
| ~ ssList(esk13_0) ),
inference(rw,[status(thm)],[562,151,theory(equality)]) ).
cnf(564,negated_conjecture,
( leq(esk11_0,X1)
| ~ memberP(esk14_0,X1)
| ~ ssItem(X1)
| ~ ssList(esk15_0)
| ~ ssList(esk14_0)
| ~ ssList(esk13_0) ),
inference(cn,[status(thm)],[563,theory(equality)]) ).
cnf(565,negated_conjecture,
( $false
| ~ leq(esk11_0,esk16_0)
| ~ leq(esk16_0,esk11_0) ),
inference(rw,[status(thm)],[515,504,theory(equality)]) ).
cnf(566,negated_conjecture,
( ~ leq(esk11_0,esk16_0)
| ~ leq(esk16_0,esk11_0) ),
inference(cn,[status(thm)],[565,theory(equality)]) ).
cnf(576,negated_conjecture,
( memberP(esk14_0,esk16_0)
| $false ),
inference(rw,[status(thm)],[516,504,theory(equality)]) ).
cnf(577,negated_conjecture,
memberP(esk14_0,esk16_0),
inference(cn,[status(thm)],[576,theory(equality)]) ).
cnf(613,negated_conjecture,
( ~ leq(esk11_0,esk16_0)
| ~ memberP(esk14_0,esk16_0)
| ~ ssItem(esk16_0)
| ~ ssList(esk15_0)
| ~ ssList(esk14_0)
| ~ ssList(esk13_0) ),
inference(spm,[status(thm)],[566,559,theory(equality)]) ).
cnf(618,negated_conjecture,
( ~ leq(esk11_0,esk16_0)
| $false
| ~ ssItem(esk16_0)
| ~ ssList(esk15_0)
| ~ ssList(esk14_0)
| ~ ssList(esk13_0) ),
inference(rw,[status(thm)],[613,577,theory(equality)]) ).
cnf(619,negated_conjecture,
( ~ leq(esk11_0,esk16_0)
| $false
| $false
| ~ ssList(esk15_0)
| ~ ssList(esk14_0)
| ~ ssList(esk13_0) ),
inference(rw,[status(thm)],[618,522,theory(equality)]) ).
cnf(620,negated_conjecture,
( ~ leq(esk11_0,esk16_0)
| ~ ssList(esk15_0)
| ~ ssList(esk14_0)
| ~ ssList(esk13_0) ),
inference(cn,[status(thm)],[619,theory(equality)]) ).
cnf(629,negated_conjecture,
( ~ ssList(esk15_0)
| ~ ssList(esk14_0)
| ~ ssList(esk13_0)
| ~ memberP(esk14_0,esk16_0)
| ~ ssItem(esk16_0) ),
inference(spm,[status(thm)],[620,564,theory(equality)]) ).
cnf(630,negated_conjecture,
( ~ ssList(esk15_0)
| ~ ssList(esk14_0)
| ~ ssList(esk13_0)
| $false
| ~ ssItem(esk16_0) ),
inference(rw,[status(thm)],[629,577,theory(equality)]) ).
cnf(631,negated_conjecture,
( ~ ssList(esk15_0)
| ~ ssList(esk14_0)
| ~ ssList(esk13_0)
| $false
| $false ),
inference(rw,[status(thm)],[630,522,theory(equality)]) ).
cnf(632,negated_conjecture,
( ~ ssList(esk15_0)
| ~ ssList(esk14_0)
| ~ ssList(esk13_0) ),
inference(cn,[status(thm)],[631,theory(equality)]) ).
cnf(639,negated_conjecture,
( ~ ssList(esk14_0)
| ~ ssList(esk13_0) ),
inference(spm,[status(thm)],[632,147,theory(equality)]) ).
cnf(640,negated_conjecture,
~ ssList(esk14_0),
inference(spm,[status(thm)],[639,149,theory(equality)]) ).
cnf(641,negated_conjecture,
$false,
inference(sr,[status(thm)],[148,640,theory(equality)]) ).
cnf(642,negated_conjecture,
$false,
641,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/SWC/SWC153+1.p
% --creating new selector for [SWC001+0.ax]
% -running prover on /tmp/tmp8Rj2-E/sel_SWC153+1.p_1 with time limit 29
% -prover status Theorem
% Problem SWC153+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/SWC/SWC153+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/SWC/SWC153+1.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% See solution above
% # SZS output end CNFRefutation
%
%------------------------------------------------------------------------------