%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : NUM541+1 : TPTP v7.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : n105.star.cs.uiowa.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz
% Memory : 32218.625MB
% OS : Linux 3.10.0-693.2.2.el7.x86_64
% CPULimit : 300s
% DateTime : Mon Jan 8 15:21:43 EST 2018
% Result : Theorem 0.06s
% Output : CNFRefutation 0.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 13
% Syntax : Number of formulae : 160 ( 10 unt; 0 def)
% Number of atoms : 689 ( 93 equ)
% Maximal formula atoms : 32 ( 4 avg)
% Number of connectives : 898 ( 369 ~; 453 |; 57 &)
% ( 5 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% Number of variables : 143 ( 0 sgn 71 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(6,axiom,
! [X1] :
( aElementOf0(X1,szNzAzT0)
=> ( aElementOf0(szszuzczcdt0(X1),szNzAzT0)
& ~ equal(szszuzczcdt0(X1),sz00) ) ),
file('/export/starexec/sandbox2/tmp/tmp7lVAns/sel_theBenchmark.p_1',mSuccNum) ).
fof(16,axiom,
! [X1] :
( aElementOf0(X1,szNzAzT0)
=> ( equal(X1,sz00)
| ? [X2] :
( aElementOf0(X2,szNzAzT0)
& equal(X1,szszuzczcdt0(X2)) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp7lVAns/sel_theBenchmark.p_1',mNatExtra) ).
fof(21,axiom,
( aElementOf0(xm,szNzAzT0)
& aElementOf0(xn,szNzAzT0) ),
file('/export/starexec/sandbox2/tmp/tmp7lVAns/sel_theBenchmark.p_1',m__1936) ).
fof(22,axiom,
! [X1] :
( aElementOf0(X1,szNzAzT0)
=> sdtlseqdt0(X1,X1) ),
file('/export/starexec/sandbox2/tmp/tmp7lVAns/sel_theBenchmark.p_1',mLessRefl) ).
fof(24,axiom,
! [X1,X2] :
( ( aElementOf0(X1,szNzAzT0)
& aElementOf0(X2,szNzAzT0) )
=> ( sdtlseqdt0(X1,X2)
<=> sdtlseqdt0(szszuzczcdt0(X1),szszuzczcdt0(X2)) ) ),
file('/export/starexec/sandbox2/tmp/tmp7lVAns/sel_theBenchmark.p_1',mSuccLess) ).
fof(31,axiom,
! [X1] :
( aElementOf0(X1,szNzAzT0)
=> sdtlseqdt0(X1,szszuzczcdt0(X1)) ),
file('/export/starexec/sandbox2/tmp/tmp7lVAns/sel_theBenchmark.p_1',mLessSucc) ).
fof(35,axiom,
! [X1] :
( aElementOf0(X1,szNzAzT0)
=> ! [X2] :
( equal(X2,slbdtrb0(X1))
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
<=> ( aElementOf0(X3,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X3),X1) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp7lVAns/sel_theBenchmark.p_1',mDefSeg) ).
fof(36,conjecture,
( aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn)))
<=> ( aElementOf0(xm,slbdtrb0(xn))
| equal(xm,xn) ) ),
file('/export/starexec/sandbox2/tmp/tmp7lVAns/sel_theBenchmark.p_1',m__) ).
fof(43,axiom,
! [X1,X2] :
( ( aElementOf0(X1,szNzAzT0)
& aElementOf0(X2,szNzAzT0) )
=> ( sdtlseqdt0(X1,X2)
| sdtlseqdt0(szszuzczcdt0(X2),X1) ) ),
file('/export/starexec/sandbox2/tmp/tmp7lVAns/sel_theBenchmark.p_1',mLessTotal) ).
fof(44,axiom,
! [X1,X2] :
( ( aElementOf0(X1,szNzAzT0)
& aElementOf0(X2,szNzAzT0) )
=> ( ( sdtlseqdt0(X1,X2)
& sdtlseqdt0(X2,X1) )
=> equal(X1,X2) ) ),
file('/export/starexec/sandbox2/tmp/tmp7lVAns/sel_theBenchmark.p_1',mLessASymm) ).
fof(51,axiom,
! [X1,X2,X3] :
( ( aElementOf0(X1,szNzAzT0)
& aElementOf0(X2,szNzAzT0)
& aElementOf0(X3,szNzAzT0) )
=> ( ( sdtlseqdt0(X1,X2)
& sdtlseqdt0(X2,X3) )
=> sdtlseqdt0(X1,X3) ) ),
file('/export/starexec/sandbox2/tmp/tmp7lVAns/sel_theBenchmark.p_1',mLessTrans) ).
fof(52,axiom,
! [X1,X2] :
( ( aElementOf0(X1,szNzAzT0)
& aElementOf0(X2,szNzAzT0) )
=> ( equal(szszuzczcdt0(X1),szszuzczcdt0(X2))
=> equal(X1,X2) ) ),
file('/export/starexec/sandbox2/tmp/tmp7lVAns/sel_theBenchmark.p_1',mSuccEquSucc) ).
fof(53,axiom,
! [X1] :
( aElementOf0(X1,szNzAzT0)
=> ~ equal(X1,szszuzczcdt0(X1)) ),
file('/export/starexec/sandbox2/tmp/tmp7lVAns/sel_theBenchmark.p_1',mNatNSucc) ).
fof(55,negated_conjecture,
~ ( aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn)))
<=> ( aElementOf0(xm,slbdtrb0(xn))
| equal(xm,xn) ) ),
inference(assume_negation,[status(cth)],[36]) ).
fof(72,plain,
! [X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ( aElementOf0(szszuzczcdt0(X1),szNzAzT0)
& ~ equal(szszuzczcdt0(X1),sz00) ) ),
inference(fof_nnf,[status(thm)],[6]) ).
fof(73,plain,
! [X2] :
( ~ aElementOf0(X2,szNzAzT0)
| ( aElementOf0(szszuzczcdt0(X2),szNzAzT0)
& ~ equal(szszuzczcdt0(X2),sz00) ) ),
inference(variable_rename,[status(thm)],[72]) ).
fof(74,plain,
! [X2] :
( ( aElementOf0(szszuzczcdt0(X2),szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0) )
& ( ~ equal(szszuzczcdt0(X2),sz00)
| ~ aElementOf0(X2,szNzAzT0) ) ),
inference(distribute,[status(thm)],[73]) ).
cnf(75,plain,
( ~ aElementOf0(X1,szNzAzT0)
| szszuzczcdt0(X1) != sz00 ),
inference(split_conjunct,[status(thm)],[74]) ).
cnf(76,plain,
( aElementOf0(szszuzczcdt0(X1),szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[74]) ).
fof(132,plain,
! [X1] :
( ~ aElementOf0(X1,szNzAzT0)
| equal(X1,sz00)
| ? [X2] :
( aElementOf0(X2,szNzAzT0)
& equal(X1,szszuzczcdt0(X2)) ) ),
inference(fof_nnf,[status(thm)],[16]) ).
fof(133,plain,
! [X3] :
( ~ aElementOf0(X3,szNzAzT0)
| equal(X3,sz00)
| ? [X4] :
( aElementOf0(X4,szNzAzT0)
& equal(X3,szszuzczcdt0(X4)) ) ),
inference(variable_rename,[status(thm)],[132]) ).
fof(134,plain,
! [X3] :
( ~ aElementOf0(X3,szNzAzT0)
| equal(X3,sz00)
| ( aElementOf0(esk5_1(X3),szNzAzT0)
& equal(X3,szszuzczcdt0(esk5_1(X3))) ) ),
inference(skolemize,[status(esa)],[133]) ).
fof(135,plain,
! [X3] :
( ( aElementOf0(esk5_1(X3),szNzAzT0)
| equal(X3,sz00)
| ~ aElementOf0(X3,szNzAzT0) )
& ( equal(X3,szszuzczcdt0(esk5_1(X3)))
| equal(X3,sz00)
| ~ aElementOf0(X3,szNzAzT0) ) ),
inference(distribute,[status(thm)],[134]) ).
cnf(136,plain,
( X1 = sz00
| X1 = szszuzczcdt0(esk5_1(X1))
| ~ aElementOf0(X1,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[135]) ).
cnf(137,plain,
( X1 = sz00
| aElementOf0(esk5_1(X1),szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[135]) ).
cnf(152,plain,
aElementOf0(xn,szNzAzT0),
inference(split_conjunct,[status(thm)],[21]) ).
cnf(153,plain,
aElementOf0(xm,szNzAzT0),
inference(split_conjunct,[status(thm)],[21]) ).
fof(154,plain,
! [X1] :
( ~ aElementOf0(X1,szNzAzT0)
| sdtlseqdt0(X1,X1) ),
inference(fof_nnf,[status(thm)],[22]) ).
fof(155,plain,
! [X2] :
( ~ aElementOf0(X2,szNzAzT0)
| sdtlseqdt0(X2,X2) ),
inference(variable_rename,[status(thm)],[154]) ).
cnf(156,plain,
( sdtlseqdt0(X1,X1)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[155]) ).
fof(160,plain,
! [X1,X2] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0)
| ( ( ~ sdtlseqdt0(X1,X2)
| sdtlseqdt0(szszuzczcdt0(X1),szszuzczcdt0(X2)) )
& ( ~ sdtlseqdt0(szszuzczcdt0(X1),szszuzczcdt0(X2))
| sdtlseqdt0(X1,X2) ) ) ),
inference(fof_nnf,[status(thm)],[24]) ).
fof(161,plain,
! [X3,X4] :
( ~ aElementOf0(X3,szNzAzT0)
| ~ aElementOf0(X4,szNzAzT0)
| ( ( ~ sdtlseqdt0(X3,X4)
| sdtlseqdt0(szszuzczcdt0(X3),szszuzczcdt0(X4)) )
& ( ~ sdtlseqdt0(szszuzczcdt0(X3),szszuzczcdt0(X4))
| sdtlseqdt0(X3,X4) ) ) ),
inference(variable_rename,[status(thm)],[160]) ).
fof(162,plain,
! [X3,X4] :
( ( ~ sdtlseqdt0(X3,X4)
| sdtlseqdt0(szszuzczcdt0(X3),szszuzczcdt0(X4))
| ~ aElementOf0(X3,szNzAzT0)
| ~ aElementOf0(X4,szNzAzT0) )
& ( ~ sdtlseqdt0(szszuzczcdt0(X3),szszuzczcdt0(X4))
| sdtlseqdt0(X3,X4)
| ~ aElementOf0(X3,szNzAzT0)
| ~ aElementOf0(X4,szNzAzT0) ) ),
inference(distribute,[status(thm)],[161]) ).
cnf(163,plain,
( sdtlseqdt0(X2,X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X2),szszuzczcdt0(X1)) ),
inference(split_conjunct,[status(thm)],[162]) ).
cnf(164,plain,
( sdtlseqdt0(szszuzczcdt0(X2),szszuzczcdt0(X1))
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0)
| ~ sdtlseqdt0(X2,X1) ),
inference(split_conjunct,[status(thm)],[162]) ).
fof(190,plain,
! [X1] :
( ~ aElementOf0(X1,szNzAzT0)
| sdtlseqdt0(X1,szszuzczcdt0(X1)) ),
inference(fof_nnf,[status(thm)],[31]) ).
fof(191,plain,
! [X2] :
( ~ aElementOf0(X2,szNzAzT0)
| sdtlseqdt0(X2,szszuzczcdt0(X2)) ),
inference(variable_rename,[status(thm)],[190]) ).
cnf(192,plain,
( sdtlseqdt0(X1,szszuzczcdt0(X1))
| ~ aElementOf0(X1,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[191]) ).
fof(206,plain,
! [X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ! [X2] :
( ( ~ equal(X2,slbdtrb0(X1))
| ( aSet0(X2)
& ! [X3] :
( ( ~ aElementOf0(X3,X2)
| ( aElementOf0(X3,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X3),X1) ) )
& ( ~ aElementOf0(X3,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X3),X1)
| aElementOf0(X3,X2) ) ) ) )
& ( ~ aSet0(X2)
| ? [X3] :
( ( ~ aElementOf0(X3,X2)
| ~ aElementOf0(X3,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X3),X1) )
& ( aElementOf0(X3,X2)
| ( aElementOf0(X3,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X3),X1) ) ) )
| equal(X2,slbdtrb0(X1)) ) ) ),
inference(fof_nnf,[status(thm)],[35]) ).
fof(207,plain,
! [X4] :
( ~ aElementOf0(X4,szNzAzT0)
| ! [X5] :
( ( ~ equal(X5,slbdtrb0(X4))
| ( aSet0(X5)
& ! [X6] :
( ( ~ aElementOf0(X6,X5)
| ( aElementOf0(X6,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X6),X4) ) )
& ( ~ aElementOf0(X6,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X6),X4)
| aElementOf0(X6,X5) ) ) ) )
& ( ~ aSet0(X5)
| ? [X7] :
( ( ~ aElementOf0(X7,X5)
| ~ aElementOf0(X7,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X7),X4) )
& ( aElementOf0(X7,X5)
| ( aElementOf0(X7,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X7),X4) ) ) )
| equal(X5,slbdtrb0(X4)) ) ) ),
inference(variable_rename,[status(thm)],[206]) ).
fof(208,plain,
! [X4] :
( ~ aElementOf0(X4,szNzAzT0)
| ! [X5] :
( ( ~ equal(X5,slbdtrb0(X4))
| ( aSet0(X5)
& ! [X6] :
( ( ~ aElementOf0(X6,X5)
| ( aElementOf0(X6,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X6),X4) ) )
& ( ~ aElementOf0(X6,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X6),X4)
| aElementOf0(X6,X5) ) ) ) )
& ( ~ aSet0(X5)
| ( ( ~ aElementOf0(esk8_2(X4,X5),X5)
| ~ aElementOf0(esk8_2(X4,X5),szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(esk8_2(X4,X5)),X4) )
& ( aElementOf0(esk8_2(X4,X5),X5)
| ( aElementOf0(esk8_2(X4,X5),szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(esk8_2(X4,X5)),X4) ) ) )
| equal(X5,slbdtrb0(X4)) ) ) ),
inference(skolemize,[status(esa)],[207]) ).
fof(209,plain,
! [X4,X5,X6] :
( ( ( ( ( ~ aElementOf0(X6,X5)
| ( aElementOf0(X6,szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(X6),X4) ) )
& ( ~ aElementOf0(X6,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X6),X4)
| aElementOf0(X6,X5) )
& aSet0(X5) )
| ~ equal(X5,slbdtrb0(X4)) )
& ( ~ aSet0(X5)
| ( ( ~ aElementOf0(esk8_2(X4,X5),X5)
| ~ aElementOf0(esk8_2(X4,X5),szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(esk8_2(X4,X5)),X4) )
& ( aElementOf0(esk8_2(X4,X5),X5)
| ( aElementOf0(esk8_2(X4,X5),szNzAzT0)
& sdtlseqdt0(szszuzczcdt0(esk8_2(X4,X5)),X4) ) ) )
| equal(X5,slbdtrb0(X4)) ) )
| ~ aElementOf0(X4,szNzAzT0) ),
inference(shift_quantors,[status(thm)],[208]) ).
fof(210,plain,
! [X4,X5,X6] :
( ( aElementOf0(X6,szNzAzT0)
| ~ aElementOf0(X6,X5)
| ~ equal(X5,slbdtrb0(X4))
| ~ aElementOf0(X4,szNzAzT0) )
& ( sdtlseqdt0(szszuzczcdt0(X6),X4)
| ~ aElementOf0(X6,X5)
| ~ equal(X5,slbdtrb0(X4))
| ~ aElementOf0(X4,szNzAzT0) )
& ( ~ aElementOf0(X6,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(X6),X4)
| aElementOf0(X6,X5)
| ~ equal(X5,slbdtrb0(X4))
| ~ aElementOf0(X4,szNzAzT0) )
& ( aSet0(X5)
| ~ equal(X5,slbdtrb0(X4))
| ~ aElementOf0(X4,szNzAzT0) )
& ( ~ aElementOf0(esk8_2(X4,X5),X5)
| ~ aElementOf0(esk8_2(X4,X5),szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(esk8_2(X4,X5)),X4)
| ~ aSet0(X5)
| equal(X5,slbdtrb0(X4))
| ~ aElementOf0(X4,szNzAzT0) )
& ( aElementOf0(esk8_2(X4,X5),szNzAzT0)
| aElementOf0(esk8_2(X4,X5),X5)
| ~ aSet0(X5)
| equal(X5,slbdtrb0(X4))
| ~ aElementOf0(X4,szNzAzT0) )
& ( sdtlseqdt0(szszuzczcdt0(esk8_2(X4,X5)),X4)
| aElementOf0(esk8_2(X4,X5),X5)
| ~ aSet0(X5)
| equal(X5,slbdtrb0(X4))
| ~ aElementOf0(X4,szNzAzT0) ) ),
inference(distribute,[status(thm)],[209]) ).
cnf(215,plain,
( aElementOf0(X3,X2)
| ~ aElementOf0(X1,szNzAzT0)
| X2 != slbdtrb0(X1)
| ~ sdtlseqdt0(szszuzczcdt0(X3),X1)
| ~ aElementOf0(X3,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[210]) ).
cnf(216,plain,
( sdtlseqdt0(szszuzczcdt0(X3),X1)
| ~ aElementOf0(X1,szNzAzT0)
| X2 != slbdtrb0(X1)
| ~ aElementOf0(X3,X2) ),
inference(split_conjunct,[status(thm)],[210]) ).
fof(218,negated_conjecture,
( ( ~ aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn)))
| ( ~ aElementOf0(xm,slbdtrb0(xn))
& ~ equal(xm,xn) ) )
& ( aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn)))
| aElementOf0(xm,slbdtrb0(xn))
| equal(xm,xn) ) ),
inference(fof_nnf,[status(thm)],[55]) ).
fof(219,negated_conjecture,
( ( ~ aElementOf0(xm,slbdtrb0(xn))
| ~ aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))) )
& ( ~ equal(xm,xn)
| ~ aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))) )
& ( aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn)))
| aElementOf0(xm,slbdtrb0(xn))
| equal(xm,xn) ) ),
inference(distribute,[status(thm)],[218]) ).
cnf(220,negated_conjecture,
( xm = xn
| aElementOf0(xm,slbdtrb0(xn))
| aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))) ),
inference(split_conjunct,[status(thm)],[219]) ).
cnf(221,negated_conjecture,
( ~ aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn)))
| xm != xn ),
inference(split_conjunct,[status(thm)],[219]) ).
cnf(222,negated_conjecture,
( ~ aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn)))
| ~ aElementOf0(xm,slbdtrb0(xn)) ),
inference(split_conjunct,[status(thm)],[219]) ).
fof(242,plain,
! [X1,X2] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0)
| sdtlseqdt0(X1,X2)
| sdtlseqdt0(szszuzczcdt0(X2),X1) ),
inference(fof_nnf,[status(thm)],[43]) ).
fof(243,plain,
! [X3,X4] :
( ~ aElementOf0(X3,szNzAzT0)
| ~ aElementOf0(X4,szNzAzT0)
| sdtlseqdt0(X3,X4)
| sdtlseqdt0(szszuzczcdt0(X4),X3) ),
inference(variable_rename,[status(thm)],[242]) ).
cnf(244,plain,
( sdtlseqdt0(szszuzczcdt0(X1),X2)
| sdtlseqdt0(X2,X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[243]) ).
fof(245,plain,
! [X1,X2] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X2,X1)
| equal(X1,X2) ),
inference(fof_nnf,[status(thm)],[44]) ).
fof(246,plain,
! [X3,X4] :
( ~ aElementOf0(X3,szNzAzT0)
| ~ aElementOf0(X4,szNzAzT0)
| ~ sdtlseqdt0(X3,X4)
| ~ sdtlseqdt0(X4,X3)
| equal(X3,X4) ),
inference(variable_rename,[status(thm)],[245]) ).
cnf(247,plain,
( X1 = X2
| ~ sdtlseqdt0(X2,X1)
| ~ sdtlseqdt0(X1,X2)
| ~ aElementOf0(X2,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[246]) ).
fof(280,plain,
! [X1,X2,X3] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0)
| ~ aElementOf0(X3,szNzAzT0)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X2,X3)
| sdtlseqdt0(X1,X3) ),
inference(fof_nnf,[status(thm)],[51]) ).
fof(281,plain,
! [X4,X5,X6] :
( ~ aElementOf0(X4,szNzAzT0)
| ~ aElementOf0(X5,szNzAzT0)
| ~ aElementOf0(X6,szNzAzT0)
| ~ sdtlseqdt0(X4,X5)
| ~ sdtlseqdt0(X5,X6)
| sdtlseqdt0(X4,X6) ),
inference(variable_rename,[status(thm)],[280]) ).
cnf(282,plain,
( sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X3,X2)
| ~ sdtlseqdt0(X1,X3)
| ~ aElementOf0(X2,szNzAzT0)
| ~ aElementOf0(X3,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[281]) ).
fof(283,plain,
! [X1,X2] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0)
| ~ equal(szszuzczcdt0(X1),szszuzczcdt0(X2))
| equal(X1,X2) ),
inference(fof_nnf,[status(thm)],[52]) ).
fof(284,plain,
! [X3,X4] :
( ~ aElementOf0(X3,szNzAzT0)
| ~ aElementOf0(X4,szNzAzT0)
| ~ equal(szszuzczcdt0(X3),szszuzczcdt0(X4))
| equal(X3,X4) ),
inference(variable_rename,[status(thm)],[283]) ).
cnf(285,plain,
( X1 = X2
| szszuzczcdt0(X1) != szszuzczcdt0(X2)
| ~ aElementOf0(X2,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[284]) ).
fof(286,plain,
! [X1] :
( ~ aElementOf0(X1,szNzAzT0)
| ~ equal(X1,szszuzczcdt0(X1)) ),
inference(fof_nnf,[status(thm)],[53]) ).
fof(287,plain,
! [X2] :
( ~ aElementOf0(X2,szNzAzT0)
| ~ equal(X2,szszuzczcdt0(X2)) ),
inference(variable_rename,[status(thm)],[286]) ).
cnf(288,plain,
( X1 != szszuzczcdt0(X1)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(split_conjunct,[status(thm)],[287]) ).
cnf(358,plain,
( esk5_1(X1) = X2
| sz00 = X1
| X1 != szszuzczcdt0(X2)
| ~ aElementOf0(X2,szNzAzT0)
| ~ aElementOf0(esk5_1(X1),szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(spm,[status(thm)],[285,136,theory(equality)]) ).
cnf(376,negated_conjecture,
( sdtlseqdt0(szszuzczcdt0(xm),X1)
| xn = xm
| aElementOf0(xm,slbdtrb0(xn))
| slbdtrb0(X1) != slbdtrb0(szszuzczcdt0(xn))
| ~ aElementOf0(X1,szNzAzT0) ),
inference(spm,[status(thm)],[216,220,theory(equality)]) ).
cnf(393,plain,
( aElementOf0(X1,X2)
| slbdtrb0(szszuzczcdt0(X1)) != X2
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(X1),szNzAzT0) ),
inference(spm,[status(thm)],[215,156,theory(equality)]) ).
cnf(396,plain,
( aElementOf0(X1,X2)
| slbdtrb0(szszuzczcdt0(X3)) != X2
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(X3),szNzAzT0)
| ~ sdtlseqdt0(X1,X3)
| ~ aElementOf0(X3,szNzAzT0) ),
inference(spm,[status(thm)],[215,164,theory(equality)]) ).
cnf(404,plain,
( aElementOf0(X1,X2)
| sdtlseqdt0(X3,X1)
| slbdtrb0(X3) != X2
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X3,szNzAzT0) ),
inference(spm,[status(thm)],[215,244,theory(equality)]) ).
cnf(419,plain,
( szszuzczcdt0(X1) = X1
| ~ sdtlseqdt0(szszuzczcdt0(X1),X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(X1),szNzAzT0) ),
inference(spm,[status(thm)],[247,192,theory(equality)]) ).
cnf(650,negated_conjecture,
( xn = xm
| sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn))
| aElementOf0(xm,slbdtrb0(xn))
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(er,[status(thm)],[376,theory(equality)]) ).
cnf(651,negated_conjecture,
( sdtlseqdt0(xm,xn)
| xn = xm
| aElementOf0(xm,slbdtrb0(xn))
| ~ aElementOf0(xm,szNzAzT0)
| ~ aElementOf0(xn,szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(spm,[status(thm)],[163,650,theory(equality)]) ).
cnf(653,negated_conjecture,
( szszuzczcdt0(xn) = szszuzczcdt0(xm)
| xn = xm
| aElementOf0(xm,slbdtrb0(xn))
| ~ sdtlseqdt0(szszuzczcdt0(xn),szszuzczcdt0(xm))
| ~ aElementOf0(szszuzczcdt0(xm),szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(spm,[status(thm)],[247,650,theory(equality)]) ).
cnf(655,negated_conjecture,
( sdtlseqdt0(xm,xn)
| xn = xm
| aElementOf0(xm,slbdtrb0(xn))
| $false
| ~ aElementOf0(xn,szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(rw,[status(thm)],[651,153,theory(equality)]) ).
cnf(656,negated_conjecture,
( sdtlseqdt0(xm,xn)
| xn = xm
| aElementOf0(xm,slbdtrb0(xn))
| $false
| $false
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(rw,[status(thm)],[655,152,theory(equality)]) ).
cnf(657,negated_conjecture,
( sdtlseqdt0(xm,xn)
| xn = xm
| aElementOf0(xm,slbdtrb0(xn))
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(cn,[status(thm)],[656,theory(equality)]) ).
cnf(663,negated_conjecture,
( sdtlseqdt0(szszuzczcdt0(xm),X1)
| xn = xm
| sdtlseqdt0(xm,xn)
| slbdtrb0(X1) != slbdtrb0(xn)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(spm,[status(thm)],[216,657,theory(equality)]) ).
cnf(672,negated_conjecture,
( szszuzczcdt0(xn) = szszuzczcdt0(xm)
| xn = xm
| aElementOf0(xm,slbdtrb0(xn))
| sdtlseqdt0(szszuzczcdt0(xm),xn)
| ~ aElementOf0(szszuzczcdt0(xm),szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| ~ aElementOf0(xn,szNzAzT0) ),
inference(spm,[status(thm)],[653,244,theory(equality)]) ).
cnf(677,negated_conjecture,
( szszuzczcdt0(xn) = szszuzczcdt0(xm)
| xn = xm
| aElementOf0(xm,slbdtrb0(xn))
| sdtlseqdt0(szszuzczcdt0(xm),xn)
| ~ aElementOf0(szszuzczcdt0(xm),szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| $false ),
inference(rw,[status(thm)],[672,152,theory(equality)]) ).
cnf(678,negated_conjecture,
( szszuzczcdt0(xn) = szszuzczcdt0(xm)
| xn = xm
| aElementOf0(xm,slbdtrb0(xn))
| sdtlseqdt0(szszuzczcdt0(xm),xn)
| ~ aElementOf0(szszuzczcdt0(xm),szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(cn,[status(thm)],[677,theory(equality)]) ).
cnf(689,negated_conjecture,
( aElementOf0(xm,X1)
| szszuzczcdt0(xn) = szszuzczcdt0(xm)
| xn = xm
| aElementOf0(xm,slbdtrb0(xn))
| slbdtrb0(xn) != X1
| ~ aElementOf0(xm,szNzAzT0)
| ~ aElementOf0(xn,szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xm),szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(spm,[status(thm)],[215,678,theory(equality)]) ).
cnf(692,negated_conjecture,
( aElementOf0(xm,X1)
| szszuzczcdt0(xn) = szszuzczcdt0(xm)
| xn = xm
| aElementOf0(xm,slbdtrb0(xn))
| slbdtrb0(xn) != X1
| $false
| ~ aElementOf0(xn,szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xm),szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(rw,[status(thm)],[689,153,theory(equality)]) ).
cnf(693,negated_conjecture,
( aElementOf0(xm,X1)
| szszuzczcdt0(xn) = szszuzczcdt0(xm)
| xn = xm
| aElementOf0(xm,slbdtrb0(xn))
| slbdtrb0(xn) != X1
| $false
| $false
| ~ aElementOf0(szszuzczcdt0(xm),szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(rw,[status(thm)],[692,152,theory(equality)]) ).
cnf(694,negated_conjecture,
( aElementOf0(xm,X1)
| szszuzczcdt0(xn) = szszuzczcdt0(xm)
| xn = xm
| aElementOf0(xm,slbdtrb0(xn))
| slbdtrb0(xn) != X1
| ~ aElementOf0(szszuzczcdt0(xm),szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(cn,[status(thm)],[693,theory(equality)]) ).
cnf(699,negated_conjecture,
( szszuzczcdt0(xn) = szszuzczcdt0(xm)
| xn = xm
| aElementOf0(xm,slbdtrb0(xn))
| ~ aElementOf0(szszuzczcdt0(xm),szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(er,[status(thm)],[694,theory(equality)]) ).
cnf(814,plain,
( szszuzczcdt0(X1) = X1
| ~ sdtlseqdt0(szszuzczcdt0(X1),X1)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(csr,[status(thm)],[419,76]) ).
cnf(815,plain,
( ~ sdtlseqdt0(szszuzczcdt0(X1),X1)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(csr,[status(thm)],[814,288]) ).
cnf(940,plain,
( aElementOf0(X1,X2)
| slbdtrb0(szszuzczcdt0(X1)) != X2
| ~ aElementOf0(X1,szNzAzT0) ),
inference(csr,[status(thm)],[393,76]) ).
cnf(941,plain,
( aElementOf0(X1,slbdtrb0(szszuzczcdt0(X1)))
| ~ aElementOf0(X1,szNzAzT0) ),
inference(er,[status(thm)],[940,theory(equality)]) ).
cnf(987,plain,
( esk5_1(X1) = X2
| sz00 = X1
| X1 != szszuzczcdt0(X2)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0) ),
inference(csr,[status(thm)],[358,137]) ).
cnf(988,plain,
( esk5_1(szszuzczcdt0(X1)) = X1
| sz00 = szszuzczcdt0(X1)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(X1),szNzAzT0) ),
inference(er,[status(thm)],[987,theory(equality)]) ).
cnf(1410,plain,
( esk5_1(szszuzczcdt0(X1)) = X1
| szszuzczcdt0(X1) = sz00
| ~ aElementOf0(X1,szNzAzT0) ),
inference(csr,[status(thm)],[988,76]) ).
cnf(1411,plain,
( esk5_1(szszuzczcdt0(X1)) = X1
| ~ aElementOf0(X1,szNzAzT0) ),
inference(csr,[status(thm)],[1410,75]) ).
cnf(2093,plain,
( aElementOf0(X1,X2)
| slbdtrb0(szszuzczcdt0(X3)) != X2
| ~ sdtlseqdt0(X1,X3)
| ~ aElementOf0(X3,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(csr,[status(thm)],[396,76]) ).
cnf(2094,plain,
( aElementOf0(X1,slbdtrb0(szszuzczcdt0(X2)))
| ~ sdtlseqdt0(X1,X2)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(X2,szNzAzT0) ),
inference(er,[status(thm)],[2093,theory(equality)]) ).
cnf(2551,plain,
( sdtlseqdt0(X1,X2)
| aElementOf0(X2,slbdtrb0(X1))
| ~ aElementOf0(X2,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(er,[status(thm)],[404,theory(equality)]) ).
cnf(3215,negated_conjecture,
( xn != xm
| ~ sdtlseqdt0(xm,xn)
| ~ aElementOf0(xm,szNzAzT0)
| ~ aElementOf0(xn,szNzAzT0) ),
inference(spm,[status(thm)],[221,2094,theory(equality)]) ).
cnf(3216,negated_conjecture,
( ~ aElementOf0(xm,slbdtrb0(xn))
| ~ sdtlseqdt0(xm,xn)
| ~ aElementOf0(xm,szNzAzT0)
| ~ aElementOf0(xn,szNzAzT0) ),
inference(spm,[status(thm)],[222,2094,theory(equality)]) ).
cnf(3230,negated_conjecture,
( xn != xm
| ~ sdtlseqdt0(xm,xn)
| $false
| ~ aElementOf0(xn,szNzAzT0) ),
inference(rw,[status(thm)],[3215,153,theory(equality)]) ).
cnf(3231,negated_conjecture,
( xn != xm
| ~ sdtlseqdt0(xm,xn)
| $false
| $false ),
inference(rw,[status(thm)],[3230,152,theory(equality)]) ).
cnf(3232,negated_conjecture,
( xn != xm
| ~ sdtlseqdt0(xm,xn) ),
inference(cn,[status(thm)],[3231,theory(equality)]) ).
cnf(3233,negated_conjecture,
( ~ aElementOf0(xm,slbdtrb0(xn))
| ~ sdtlseqdt0(xm,xn)
| $false
| ~ aElementOf0(xn,szNzAzT0) ),
inference(rw,[status(thm)],[3216,153,theory(equality)]) ).
cnf(3234,negated_conjecture,
( ~ aElementOf0(xm,slbdtrb0(xn))
| ~ sdtlseqdt0(xm,xn)
| $false
| $false ),
inference(rw,[status(thm)],[3233,152,theory(equality)]) ).
cnf(3235,negated_conjecture,
( ~ aElementOf0(xm,slbdtrb0(xn))
| ~ sdtlseqdt0(xm,xn) ),
inference(cn,[status(thm)],[3234,theory(equality)]) ).
cnf(3237,negated_conjecture,
( szszuzczcdt0(xn) = szszuzczcdt0(xm)
| xn = xm
| ~ sdtlseqdt0(xm,xn)
| ~ aElementOf0(szszuzczcdt0(xm),szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(spm,[status(thm)],[3235,699,theory(equality)]) ).
cnf(3532,negated_conjecture,
( szszuzczcdt0(xn) = szszuzczcdt0(xm)
| ~ sdtlseqdt0(xm,xn)
| ~ aElementOf0(szszuzczcdt0(xm),szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(csr,[status(thm)],[3237,3232]) ).
cnf(3533,negated_conjecture,
( szszuzczcdt0(xn) = szszuzczcdt0(xm)
| ~ sdtlseqdt0(xm,xn)
| ~ aElementOf0(szszuzczcdt0(xm),szNzAzT0)
| ~ aElementOf0(xn,szNzAzT0) ),
inference(spm,[status(thm)],[3532,76,theory(equality)]) ).
cnf(3537,negated_conjecture,
( szszuzczcdt0(xn) = szszuzczcdt0(xm)
| ~ sdtlseqdt0(xm,xn)
| ~ aElementOf0(szszuzczcdt0(xm),szNzAzT0)
| $false ),
inference(rw,[status(thm)],[3533,152,theory(equality)]) ).
cnf(3538,negated_conjecture,
( szszuzczcdt0(xn) = szszuzczcdt0(xm)
| ~ sdtlseqdt0(xm,xn)
| ~ aElementOf0(szszuzczcdt0(xm),szNzAzT0) ),
inference(cn,[status(thm)],[3537,theory(equality)]) ).
cnf(3539,negated_conjecture,
( szszuzczcdt0(xn) = szszuzczcdt0(xm)
| ~ sdtlseqdt0(xm,xn)
| ~ aElementOf0(xm,szNzAzT0) ),
inference(spm,[status(thm)],[3538,76,theory(equality)]) ).
cnf(3543,negated_conjecture,
( szszuzczcdt0(xn) = szszuzczcdt0(xm)
| ~ sdtlseqdt0(xm,xn)
| $false ),
inference(rw,[status(thm)],[3539,153,theory(equality)]) ).
cnf(3544,negated_conjecture,
( szszuzczcdt0(xn) = szszuzczcdt0(xm)
| ~ sdtlseqdt0(xm,xn) ),
inference(cn,[status(thm)],[3543,theory(equality)]) ).
cnf(3582,negated_conjecture,
( esk5_1(szszuzczcdt0(xm)) = xn
| ~ aElementOf0(xn,szNzAzT0)
| ~ sdtlseqdt0(xm,xn) ),
inference(spm,[status(thm)],[1411,3544,theory(equality)]) ).
cnf(3645,negated_conjecture,
( esk5_1(szszuzczcdt0(xm)) = xn
| $false
| ~ sdtlseqdt0(xm,xn) ),
inference(rw,[status(thm)],[3582,152,theory(equality)]) ).
cnf(3646,negated_conjecture,
( esk5_1(szszuzczcdt0(xm)) = xn
| ~ sdtlseqdt0(xm,xn) ),
inference(cn,[status(thm)],[3645,theory(equality)]) ).
cnf(3737,negated_conjecture,
( xn = xm
| ~ aElementOf0(xm,szNzAzT0)
| ~ sdtlseqdt0(xm,xn) ),
inference(spm,[status(thm)],[1411,3646,theory(equality)]) ).
cnf(3761,negated_conjecture,
( xn = xm
| $false
| ~ sdtlseqdt0(xm,xn) ),
inference(rw,[status(thm)],[3737,153,theory(equality)]) ).
cnf(3762,negated_conjecture,
( xn = xm
| ~ sdtlseqdt0(xm,xn) ),
inference(cn,[status(thm)],[3761,theory(equality)]) ).
cnf(3777,negated_conjecture,
~ sdtlseqdt0(xm,xn),
inference(csr,[status(thm)],[3762,3232]) ).
cnf(4166,negated_conjecture,
( sdtlseqdt0(szszuzczcdt0(xn),xm)
| ~ aElementOf0(xm,slbdtrb0(xn))
| ~ aElementOf0(xm,szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(spm,[status(thm)],[222,2551,theory(equality)]) ).
cnf(4183,negated_conjecture,
( sdtlseqdt0(szszuzczcdt0(xn),xm)
| ~ aElementOf0(xm,slbdtrb0(xn))
| $false
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(rw,[status(thm)],[4166,153,theory(equality)]) ).
cnf(4184,negated_conjecture,
( sdtlseqdt0(szszuzczcdt0(xn),xm)
| ~ aElementOf0(xm,slbdtrb0(xn))
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(cn,[status(thm)],[4183,theory(equality)]) ).
cnf(4239,negated_conjecture,
( sdtlseqdt0(X1,xm)
| ~ sdtlseqdt0(X1,szszuzczcdt0(xn))
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| ~ aElementOf0(xm,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(xm,slbdtrb0(xn)) ),
inference(spm,[status(thm)],[282,4184,theory(equality)]) ).
cnf(4248,negated_conjecture,
( sdtlseqdt0(X1,xm)
| ~ sdtlseqdt0(X1,szszuzczcdt0(xn))
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| $false
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(xm,slbdtrb0(xn)) ),
inference(rw,[status(thm)],[4239,153,theory(equality)]) ).
cnf(4249,negated_conjecture,
( sdtlseqdt0(X1,xm)
| ~ sdtlseqdt0(X1,szszuzczcdt0(xn))
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0)
| ~ aElementOf0(xm,slbdtrb0(xn)) ),
inference(cn,[status(thm)],[4248,theory(equality)]) ).
cnf(4900,negated_conjecture,
( sdtlseqdt0(xn,xm)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| ~ aElementOf0(xm,slbdtrb0(xn))
| ~ aElementOf0(xn,szNzAzT0) ),
inference(spm,[status(thm)],[4249,192,theory(equality)]) ).
cnf(4918,negated_conjecture,
( sdtlseqdt0(xn,xm)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| ~ aElementOf0(xm,slbdtrb0(xn))
| $false ),
inference(rw,[status(thm)],[4900,152,theory(equality)]) ).
cnf(4919,negated_conjecture,
( sdtlseqdt0(xn,xm)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| ~ aElementOf0(xm,slbdtrb0(xn)) ),
inference(cn,[status(thm)],[4918,theory(equality)]) ).
cnf(4928,negated_conjecture,
( sdtlseqdt0(xn,xm)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| ~ aElementOf0(xm,szNzAzT0)
| ~ aElementOf0(xn,szNzAzT0) ),
inference(spm,[status(thm)],[4919,2551,theory(equality)]) ).
cnf(4936,negated_conjecture,
( sdtlseqdt0(xn,xm)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| $false
| ~ aElementOf0(xn,szNzAzT0) ),
inference(rw,[status(thm)],[4928,153,theory(equality)]) ).
cnf(4937,negated_conjecture,
( sdtlseqdt0(xn,xm)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| $false
| $false ),
inference(rw,[status(thm)],[4936,152,theory(equality)]) ).
cnf(4938,negated_conjecture,
( sdtlseqdt0(xn,xm)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(cn,[status(thm)],[4937,theory(equality)]) ).
cnf(4939,negated_conjecture,
( sdtlseqdt0(xn,xm)
| ~ aElementOf0(xn,szNzAzT0) ),
inference(spm,[status(thm)],[4938,76,theory(equality)]) ).
cnf(4944,negated_conjecture,
( sdtlseqdt0(xn,xm)
| $false ),
inference(rw,[status(thm)],[4939,152,theory(equality)]) ).
cnf(4945,negated_conjecture,
sdtlseqdt0(xn,xm),
inference(cn,[status(thm)],[4944,theory(equality)]) ).
cnf(4947,negated_conjecture,
( sdtlseqdt0(X1,xm)
| ~ sdtlseqdt0(X1,xn)
| ~ aElementOf0(xn,szNzAzT0)
| ~ aElementOf0(xm,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(spm,[status(thm)],[282,4945,theory(equality)]) ).
cnf(4967,negated_conjecture,
( sdtlseqdt0(X1,xm)
| ~ sdtlseqdt0(X1,xn)
| $false
| ~ aElementOf0(xm,szNzAzT0)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(rw,[status(thm)],[4947,152,theory(equality)]) ).
cnf(4968,negated_conjecture,
( sdtlseqdt0(X1,xm)
| ~ sdtlseqdt0(X1,xn)
| $false
| $false
| ~ aElementOf0(X1,szNzAzT0) ),
inference(rw,[status(thm)],[4967,153,theory(equality)]) ).
cnf(4969,negated_conjecture,
( sdtlseqdt0(X1,xm)
| ~ sdtlseqdt0(X1,xn)
| ~ aElementOf0(X1,szNzAzT0) ),
inference(cn,[status(thm)],[4968,theory(equality)]) ).
cnf(5022,negated_conjecture,
( sdtlseqdt0(szszuzczcdt0(xm),xm)
| xn = xm
| sdtlseqdt0(xm,xn)
| ~ aElementOf0(szszuzczcdt0(xm),szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| ~ aElementOf0(xn,szNzAzT0) ),
inference(spm,[status(thm)],[4969,663,theory(equality)]) ).
cnf(5049,negated_conjecture,
( sdtlseqdt0(szszuzczcdt0(xm),xm)
| xn = xm
| sdtlseqdt0(xm,xn)
| ~ aElementOf0(szszuzczcdt0(xm),szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0)
| $false ),
inference(rw,[status(thm)],[5022,152,theory(equality)]) ).
cnf(5050,negated_conjecture,
( sdtlseqdt0(szszuzczcdt0(xm),xm)
| xn = xm
| sdtlseqdt0(xm,xn)
| ~ aElementOf0(szszuzczcdt0(xm),szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(cn,[status(thm)],[5049,theory(equality)]) ).
cnf(5051,negated_conjecture,
( sdtlseqdt0(szszuzczcdt0(xm),xm)
| xn = xm
| ~ aElementOf0(szszuzczcdt0(xm),szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(sr,[status(thm)],[5050,3777,theory(equality)]) ).
cnf(5071,negated_conjecture,
( xn = xm
| ~ aElementOf0(xm,szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xm),szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(spm,[status(thm)],[815,5051,theory(equality)]) ).
cnf(5079,negated_conjecture,
( xn = xm
| $false
| ~ aElementOf0(szszuzczcdt0(xm),szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(rw,[status(thm)],[5071,153,theory(equality)]) ).
cnf(5080,negated_conjecture,
( xn = xm
| ~ aElementOf0(szszuzczcdt0(xm),szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(xn),szNzAzT0) ),
inference(cn,[status(thm)],[5079,theory(equality)]) ).
cnf(5084,negated_conjecture,
( xn = xm
| ~ aElementOf0(szszuzczcdt0(xm),szNzAzT0)
| ~ aElementOf0(xn,szNzAzT0) ),
inference(spm,[status(thm)],[5080,76,theory(equality)]) ).
cnf(5089,negated_conjecture,
( xn = xm
| ~ aElementOf0(szszuzczcdt0(xm),szNzAzT0)
| $false ),
inference(rw,[status(thm)],[5084,152,theory(equality)]) ).
cnf(5090,negated_conjecture,
( xn = xm
| ~ aElementOf0(szszuzczcdt0(xm),szNzAzT0) ),
inference(cn,[status(thm)],[5089,theory(equality)]) ).
cnf(5091,negated_conjecture,
( xn = xm
| ~ aElementOf0(xm,szNzAzT0) ),
inference(spm,[status(thm)],[5090,76,theory(equality)]) ).
cnf(5095,negated_conjecture,
( xn = xm
| $false ),
inference(rw,[status(thm)],[5091,153,theory(equality)]) ).
cnf(5096,negated_conjecture,
xn = xm,
inference(cn,[status(thm)],[5095,theory(equality)]) ).
cnf(5415,negated_conjecture,
( $false
| ~ aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))) ),
inference(rw,[status(thm)],[221,5096,theory(equality)]) ).
cnf(5416,negated_conjecture,
( $false
| ~ aElementOf0(xm,slbdtrb0(szszuzczcdt0(xm))) ),
inference(rw,[status(thm)],[5415,5096,theory(equality)]) ).
cnf(5417,negated_conjecture,
~ aElementOf0(xm,slbdtrb0(szszuzczcdt0(xm))),
inference(cn,[status(thm)],[5416,theory(equality)]) ).
cnf(5418,negated_conjecture,
~ aElementOf0(xm,szNzAzT0),
inference(spm,[status(thm)],[5417,941,theory(equality)]) ).
cnf(5421,negated_conjecture,
$false,
inference(rw,[status(thm)],[5418,153,theory(equality)]) ).
cnf(5422,negated_conjecture,
$false,
inference(cn,[status(thm)],[5421,theory(equality)]) ).
cnf(5423,negated_conjecture,
$false,
5422,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM541+1 : TPTP v7.0.0. Released v4.0.0.
% 0.00/0.04 % Command : Source/sine.py -e eprover -t %d %s
% 0.02/0.23 % Computer : n105.star.cs.uiowa.edu
% 0.02/0.23 % Model : x86_64 x86_64
% 0.02/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.02/0.23 % Memory : 32218.625MB
% 0.02/0.23 % OS : Linux 3.10.0-693.2.2.el7.x86_64
% 0.02/0.23 % CPULimit : 300
% 0.02/0.23 % DateTime : Fri Jan 5 08:04:30 CST 2018
% 0.02/0.23 % CPUTime :
% 0.02/0.27 % SZS status Started for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.02/0.27 --creating new selector for []
% 0.06/0.49 -running prover on /export/starexec/sandbox2/tmp/tmp7lVAns/sel_theBenchmark.p_1 with time limit 29
% 0.06/0.49 -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/tmp7lVAns/sel_theBenchmark.p_1']
% 0.06/0.49 -prover status Theorem
% 0.06/0.49 Problem theBenchmark.p solved in phase 0.
% 0.06/0.49 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.06/0.49 % SZS status Ended for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.06/0.49 Solved 1 out of 1.
% 0.06/0.49 # Problem is unsatisfiable (or provable), constructing proof object
% 0.06/0.49 # SZS status Theorem
% 0.06/0.49 # SZS output start CNFRefutation.
% See solution above
% 0.06/0.50 # SZS output end CNFRefutation
%------------------------------------------------------------------------------