%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : RNG098+1 : TPTP v5.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art03.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 02:20:38 EST 2010
% Result : Theorem 4.11s
% Output : CNFRefutation 4.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 12
% Syntax : Number of formulae : 70 ( 21 unt; 0 def)
% Number of atoms : 250 ( 22 equ)
% Maximal formula atoms : 29 ( 3 avg)
% Number of connectives : 298 ( 118 ~; 124 |; 47 &)
% ( 1 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-2 aty)
% Number of variables : 74 ( 0 sgn 51 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(1,axiom,
( aElement0(xx)
& aElement0(xy) ),
file('/tmp/tmpYuWJZm/sel_RNG098+1.p_1',m__1217) ).
fof(2,axiom,
! [X1] :
( aSet0(X1)
=> ! [X2] :
( aElementOf0(X2,X1)
=> aElement0(X2) ) ),
file('/tmp/tmpYuWJZm/sel_RNG098+1.p_1',mEOfElem) ).
fof(7,axiom,
! [X1,X2,X3] :
( ( aElement0(X1)
& aElement0(X2)
& aElement0(X3) )
=> ( sdtasdt0(X1,sdtpldt0(X2,X3)) = sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3))
& sdtasdt0(sdtpldt0(X2,X3),X1) = sdtpldt0(sdtasdt0(X2,X1),sdtasdt0(X3,X1)) ) ),
file('/tmp/tmpYuWJZm/sel_RNG098+1.p_1',mAMDistr) ).
fof(8,axiom,
sdtpldt0(xw,smndt0(xx)) = sdtpldt0(sdtasdt0(xy,xa),sdtpldt0(sdtasdt0(xx,xb),smndt0(xx))),
file('/tmp/tmpYuWJZm/sel_RNG098+1.p_1',m__1374) ).
fof(10,axiom,
aElementOf0(sdtasdt0(xx,sdtpldt0(xb,smndt0(sz10))),xI),
file('/tmp/tmpYuWJZm/sel_RNG098+1.p_1',m__1393) ).
fof(11,axiom,
( aElementOf0(xa,xI)
& aElementOf0(xb,xJ)
& sdtpldt0(xa,xb) = sz10 ),
file('/tmp/tmpYuWJZm/sel_RNG098+1.p_1',m__1294) ).
fof(19,axiom,
aElement0(sz10),
file('/tmp/tmpYuWJZm/sel_RNG098+1.p_1',mSortsC_01) ).
fof(20,axiom,
! [X1] :
( aIdeal0(X1)
<=> ( aSet0(X1)
& ! [X2] :
( aElementOf0(X2,X1)
=> ( ! [X3] :
( aElementOf0(X3,X1)
=> aElementOf0(sdtpldt0(X2,X3),X1) )
& ! [X3] :
( aElement0(X3)
=> aElementOf0(sdtasdt0(X3,X2),X1) ) ) ) ) ),
file('/tmp/tmpYuWJZm/sel_RNG098+1.p_1',mDefIdeal) ).
fof(24,axiom,
( aIdeal0(xI)
& aIdeal0(xJ) ),
file('/tmp/tmpYuWJZm/sel_RNG098+1.p_1',m__1205) ).
fof(31,axiom,
! [X1] :
( aElement0(X1)
=> ( sdtasdt0(smndt0(sz10),X1) = smndt0(X1)
& smndt0(X1) = sdtasdt0(X1,smndt0(sz10)) ) ),
file('/tmp/tmpYuWJZm/sel_RNG098+1.p_1',mMulMnOne) ).
fof(32,axiom,
! [X1] :
( aElement0(X1)
=> aElement0(smndt0(X1)) ),
file('/tmp/tmpYuWJZm/sel_RNG098+1.p_1',mSortsU) ).
fof(35,conjecture,
aElementOf0(sdtpldt0(xw,smndt0(xx)),xI),
file('/tmp/tmpYuWJZm/sel_RNG098+1.p_1',m__) ).
fof(36,negated_conjecture,
~ aElementOf0(sdtpldt0(xw,smndt0(xx)),xI),
inference(assume_negation,[status(cth)],[35]) ).
fof(37,negated_conjecture,
~ aElementOf0(sdtpldt0(xw,smndt0(xx)),xI),
inference(fof_simplification,[status(thm)],[36,theory(equality)]) ).
cnf(38,plain,
aElement0(xy),
inference(split_conjunct,[status(thm)],[1]) ).
cnf(39,plain,
aElement0(xx),
inference(split_conjunct,[status(thm)],[1]) ).
fof(40,plain,
! [X1] :
( ~ aSet0(X1)
| ! [X2] :
( ~ aElementOf0(X2,X1)
| aElement0(X2) ) ),
inference(fof_nnf,[status(thm)],[2]) ).
fof(41,plain,
! [X3] :
( ~ aSet0(X3)
| ! [X4] :
( ~ aElementOf0(X4,X3)
| aElement0(X4) ) ),
inference(variable_rename,[status(thm)],[40]) ).
fof(42,plain,
! [X3,X4] :
( ~ aElementOf0(X4,X3)
| aElement0(X4)
| ~ aSet0(X3) ),
inference(shift_quantors,[status(thm)],[41]) ).
cnf(43,plain,
( aElement0(X2)
| ~ aSet0(X1)
| ~ aElementOf0(X2,X1) ),
inference(split_conjunct,[status(thm)],[42]) ).
fof(56,plain,
! [X1,X2,X3] :
( ~ aElement0(X1)
| ~ aElement0(X2)
| ~ aElement0(X3)
| ( sdtasdt0(X1,sdtpldt0(X2,X3)) = sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3))
& sdtasdt0(sdtpldt0(X2,X3),X1) = sdtpldt0(sdtasdt0(X2,X1),sdtasdt0(X3,X1)) ) ),
inference(fof_nnf,[status(thm)],[7]) ).
fof(57,plain,
! [X4,X5,X6] :
( ~ aElement0(X4)
| ~ aElement0(X5)
| ~ aElement0(X6)
| ( sdtasdt0(X4,sdtpldt0(X5,X6)) = sdtpldt0(sdtasdt0(X4,X5),sdtasdt0(X4,X6))
& sdtasdt0(sdtpldt0(X5,X6),X4) = sdtpldt0(sdtasdt0(X5,X4),sdtasdt0(X6,X4)) ) ),
inference(variable_rename,[status(thm)],[56]) ).
fof(58,plain,
! [X4,X5,X6] :
( ( sdtasdt0(X4,sdtpldt0(X5,X6)) = sdtpldt0(sdtasdt0(X4,X5),sdtasdt0(X4,X6))
| ~ aElement0(X4)
| ~ aElement0(X5)
| ~ aElement0(X6) )
& ( sdtasdt0(sdtpldt0(X5,X6),X4) = sdtpldt0(sdtasdt0(X5,X4),sdtasdt0(X6,X4))
| ~ aElement0(X4)
| ~ aElement0(X5)
| ~ aElement0(X6) ) ),
inference(distribute,[status(thm)],[57]) ).
cnf(60,plain,
( sdtasdt0(X3,sdtpldt0(X2,X1)) = sdtpldt0(sdtasdt0(X3,X2),sdtasdt0(X3,X1))
| ~ aElement0(X1)
| ~ aElement0(X2)
| ~ aElement0(X3) ),
inference(split_conjunct,[status(thm)],[58]) ).
cnf(61,plain,
sdtpldt0(xw,smndt0(xx)) = sdtpldt0(sdtasdt0(xy,xa),sdtpldt0(sdtasdt0(xx,xb),smndt0(xx))),
inference(split_conjunct,[status(thm)],[8]) ).
cnf(70,plain,
aElementOf0(sdtasdt0(xx,sdtpldt0(xb,smndt0(sz10))),xI),
inference(split_conjunct,[status(thm)],[10]) ).
cnf(72,plain,
aElementOf0(xb,xJ),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(73,plain,
aElementOf0(xa,xI),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(95,plain,
aElement0(sz10),
inference(split_conjunct,[status(thm)],[19]) ).
fof(96,plain,
! [X1] :
( ( ~ aIdeal0(X1)
| ( aSet0(X1)
& ! [X2] :
( ~ aElementOf0(X2,X1)
| ( ! [X3] :
( ~ aElementOf0(X3,X1)
| aElementOf0(sdtpldt0(X2,X3),X1) )
& ! [X3] :
( ~ aElement0(X3)
| aElementOf0(sdtasdt0(X3,X2),X1) ) ) ) ) )
& ( ~ aSet0(X1)
| ? [X2] :
( aElementOf0(X2,X1)
& ( ? [X3] :
( aElementOf0(X3,X1)
& ~ aElementOf0(sdtpldt0(X2,X3),X1) )
| ? [X3] :
( aElement0(X3)
& ~ aElementOf0(sdtasdt0(X3,X2),X1) ) ) )
| aIdeal0(X1) ) ),
inference(fof_nnf,[status(thm)],[20]) ).
fof(97,plain,
! [X4] :
( ( ~ aIdeal0(X4)
| ( aSet0(X4)
& ! [X5] :
( ~ aElementOf0(X5,X4)
| ( ! [X6] :
( ~ aElementOf0(X6,X4)
| aElementOf0(sdtpldt0(X5,X6),X4) )
& ! [X7] :
( ~ aElement0(X7)
| aElementOf0(sdtasdt0(X7,X5),X4) ) ) ) ) )
& ( ~ aSet0(X4)
| ? [X8] :
( aElementOf0(X8,X4)
& ( ? [X9] :
( aElementOf0(X9,X4)
& ~ aElementOf0(sdtpldt0(X8,X9),X4) )
| ? [X10] :
( aElement0(X10)
& ~ aElementOf0(sdtasdt0(X10,X8),X4) ) ) )
| aIdeal0(X4) ) ),
inference(variable_rename,[status(thm)],[96]) ).
fof(98,plain,
! [X4] :
( ( ~ aIdeal0(X4)
| ( aSet0(X4)
& ! [X5] :
( ~ aElementOf0(X5,X4)
| ( ! [X6] :
( ~ aElementOf0(X6,X4)
| aElementOf0(sdtpldt0(X5,X6),X4) )
& ! [X7] :
( ~ aElement0(X7)
| aElementOf0(sdtasdt0(X7,X5),X4) ) ) ) ) )
& ( ~ aSet0(X4)
| ( aElementOf0(esk3_1(X4),X4)
& ( ( aElementOf0(esk4_1(X4),X4)
& ~ aElementOf0(sdtpldt0(esk3_1(X4),esk4_1(X4)),X4) )
| ( aElement0(esk5_1(X4))
& ~ aElementOf0(sdtasdt0(esk5_1(X4),esk3_1(X4)),X4) ) ) )
| aIdeal0(X4) ) ),
inference(skolemize,[status(esa)],[97]) ).
fof(99,plain,
! [X4,X5,X6,X7] :
( ( ( ( ( ( ~ aElement0(X7)
| aElementOf0(sdtasdt0(X7,X5),X4) )
& ( ~ aElementOf0(X6,X4)
| aElementOf0(sdtpldt0(X5,X6),X4) ) )
| ~ aElementOf0(X5,X4) )
& aSet0(X4) )
| ~ aIdeal0(X4) )
& ( ~ aSet0(X4)
| ( aElementOf0(esk3_1(X4),X4)
& ( ( aElementOf0(esk4_1(X4),X4)
& ~ aElementOf0(sdtpldt0(esk3_1(X4),esk4_1(X4)),X4) )
| ( aElement0(esk5_1(X4))
& ~ aElementOf0(sdtasdt0(esk5_1(X4),esk3_1(X4)),X4) ) ) )
| aIdeal0(X4) ) ),
inference(shift_quantors,[status(thm)],[98]) ).
fof(100,plain,
! [X4,X5,X6,X7] :
( ( ~ aElement0(X7)
| aElementOf0(sdtasdt0(X7,X5),X4)
| ~ aElementOf0(X5,X4)
| ~ aIdeal0(X4) )
& ( ~ aElementOf0(X6,X4)
| aElementOf0(sdtpldt0(X5,X6),X4)
| ~ aElementOf0(X5,X4)
| ~ aIdeal0(X4) )
& ( aSet0(X4)
| ~ aIdeal0(X4) )
& ( aElementOf0(esk3_1(X4),X4)
| ~ aSet0(X4)
| aIdeal0(X4) )
& ( aElement0(esk5_1(X4))
| aElementOf0(esk4_1(X4),X4)
| ~ aSet0(X4)
| aIdeal0(X4) )
& ( ~ aElementOf0(sdtasdt0(esk5_1(X4),esk3_1(X4)),X4)
| aElementOf0(esk4_1(X4),X4)
| ~ aSet0(X4)
| aIdeal0(X4) )
& ( aElement0(esk5_1(X4))
| ~ aElementOf0(sdtpldt0(esk3_1(X4),esk4_1(X4)),X4)
| ~ aSet0(X4)
| aIdeal0(X4) )
& ( ~ aElementOf0(sdtasdt0(esk5_1(X4),esk3_1(X4)),X4)
| ~ aElementOf0(sdtpldt0(esk3_1(X4),esk4_1(X4)),X4)
| ~ aSet0(X4)
| aIdeal0(X4) ) ),
inference(distribute,[status(thm)],[99]) ).
cnf(106,plain,
( aSet0(X1)
| ~ aIdeal0(X1) ),
inference(split_conjunct,[status(thm)],[100]) ).
cnf(107,plain,
( aElementOf0(sdtpldt0(X2,X3),X1)
| ~ aIdeal0(X1)
| ~ aElementOf0(X2,X1)
| ~ aElementOf0(X3,X1) ),
inference(split_conjunct,[status(thm)],[100]) ).
cnf(108,plain,
( aElementOf0(sdtasdt0(X3,X2),X1)
| ~ aIdeal0(X1)
| ~ aElementOf0(X2,X1)
| ~ aElement0(X3) ),
inference(split_conjunct,[status(thm)],[100]) ).
cnf(131,plain,
aIdeal0(xJ),
inference(split_conjunct,[status(thm)],[24]) ).
cnf(132,plain,
aIdeal0(xI),
inference(split_conjunct,[status(thm)],[24]) ).
fof(151,plain,
! [X1] :
( ~ aElement0(X1)
| ( sdtasdt0(smndt0(sz10),X1) = smndt0(X1)
& smndt0(X1) = sdtasdt0(X1,smndt0(sz10)) ) ),
inference(fof_nnf,[status(thm)],[31]) ).
fof(152,plain,
! [X2] :
( ~ aElement0(X2)
| ( sdtasdt0(smndt0(sz10),X2) = smndt0(X2)
& smndt0(X2) = sdtasdt0(X2,smndt0(sz10)) ) ),
inference(variable_rename,[status(thm)],[151]) ).
fof(153,plain,
! [X2] :
( ( sdtasdt0(smndt0(sz10),X2) = smndt0(X2)
| ~ aElement0(X2) )
& ( smndt0(X2) = sdtasdt0(X2,smndt0(sz10))
| ~ aElement0(X2) ) ),
inference(distribute,[status(thm)],[152]) ).
cnf(154,plain,
( smndt0(X1) = sdtasdt0(X1,smndt0(sz10))
| ~ aElement0(X1) ),
inference(split_conjunct,[status(thm)],[153]) ).
fof(156,plain,
! [X1] :
( ~ aElement0(X1)
| aElement0(smndt0(X1)) ),
inference(fof_nnf,[status(thm)],[32]) ).
fof(157,plain,
! [X2] :
( ~ aElement0(X2)
| aElement0(smndt0(X2)) ),
inference(variable_rename,[status(thm)],[156]) ).
cnf(158,plain,
( aElement0(smndt0(X1))
| ~ aElement0(X1) ),
inference(split_conjunct,[status(thm)],[157]) ).
cnf(176,negated_conjecture,
~ aElementOf0(sdtpldt0(xw,smndt0(xx)),xI),
inference(split_conjunct,[status(thm)],[37]) ).
cnf(178,plain,
aSet0(xJ),
inference(spm,[status(thm)],[106,131,theory(equality)]) ).
cnf(192,plain,
( aElement0(xb)
| ~ aSet0(xJ) ),
inference(spm,[status(thm)],[43,72,theory(equality)]) ).
cnf(304,plain,
( aElementOf0(sdtpldt0(xw,smndt0(xx)),X1)
| ~ aIdeal0(X1)
| ~ aElementOf0(sdtpldt0(sdtasdt0(xx,xb),smndt0(xx)),X1)
| ~ aElementOf0(sdtasdt0(xy,xa),X1) ),
inference(spm,[status(thm)],[107,61,theory(equality)]) ).
cnf(404,plain,
( sdtpldt0(sdtasdt0(X1,X2),smndt0(X1)) = sdtasdt0(X1,sdtpldt0(X2,smndt0(sz10)))
| ~ aElement0(X1)
| ~ aElement0(X2)
| ~ aElement0(smndt0(sz10)) ),
inference(spm,[status(thm)],[60,154,theory(equality)]) ).
cnf(504,plain,
( aElement0(xb)
| $false ),
inference(rw,[status(thm)],[192,178,theory(equality)]) ).
cnf(505,plain,
aElement0(xb),
inference(cn,[status(thm)],[504,theory(equality)]) ).
cnf(17865,plain,
( aElementOf0(sdtpldt0(sdtasdt0(xx,xb),smndt0(xx)),xI)
| ~ aElement0(smndt0(sz10))
| ~ aElement0(xx)
| ~ aElement0(xb) ),
inference(spm,[status(thm)],[70,404,theory(equality)]) ).
cnf(17985,plain,
( aElementOf0(sdtpldt0(sdtasdt0(xx,xb),smndt0(xx)),xI)
| ~ aElement0(smndt0(sz10))
| $false
| ~ aElement0(xb) ),
inference(rw,[status(thm)],[17865,39,theory(equality)]) ).
cnf(17986,plain,
( aElementOf0(sdtpldt0(sdtasdt0(xx,xb),smndt0(xx)),xI)
| ~ aElement0(smndt0(sz10))
| $false
| $false ),
inference(rw,[status(thm)],[17985,505,theory(equality)]) ).
cnf(17987,plain,
( aElementOf0(sdtpldt0(sdtasdt0(xx,xb),smndt0(xx)),xI)
| ~ aElement0(smndt0(sz10)) ),
inference(cn,[status(thm)],[17986,theory(equality)]) ).
cnf(89668,plain,
( aElementOf0(sdtpldt0(xw,smndt0(xx)),xI)
| ~ aIdeal0(xI)
| ~ aElementOf0(sdtasdt0(xy,xa),xI)
| ~ aElement0(smndt0(sz10)) ),
inference(spm,[status(thm)],[304,17987,theory(equality)]) ).
cnf(89677,plain,
( aElementOf0(sdtpldt0(xw,smndt0(xx)),xI)
| $false
| ~ aElementOf0(sdtasdt0(xy,xa),xI)
| ~ aElement0(smndt0(sz10)) ),
inference(rw,[status(thm)],[89668,132,theory(equality)]) ).
cnf(89678,plain,
( aElementOf0(sdtpldt0(xw,smndt0(xx)),xI)
| ~ aElementOf0(sdtasdt0(xy,xa),xI)
| ~ aElement0(smndt0(sz10)) ),
inference(cn,[status(thm)],[89677,theory(equality)]) ).
cnf(89679,plain,
( ~ aElementOf0(sdtasdt0(xy,xa),xI)
| ~ aElement0(smndt0(sz10)) ),
inference(sr,[status(thm)],[89678,176,theory(equality)]) ).
cnf(120433,plain,
( ~ aElementOf0(sdtasdt0(xy,xa),xI)
| ~ aElement0(sz10) ),
inference(spm,[status(thm)],[89679,158,theory(equality)]) ).
cnf(120434,plain,
( ~ aElementOf0(sdtasdt0(xy,xa),xI)
| $false ),
inference(rw,[status(thm)],[120433,95,theory(equality)]) ).
cnf(120435,plain,
~ aElementOf0(sdtasdt0(xy,xa),xI),
inference(cn,[status(thm)],[120434,theory(equality)]) ).
cnf(120439,plain,
( ~ aIdeal0(xI)
| ~ aElementOf0(xa,xI)
| ~ aElement0(xy) ),
inference(spm,[status(thm)],[120435,108,theory(equality)]) ).
cnf(120450,plain,
( $false
| ~ aElementOf0(xa,xI)
| ~ aElement0(xy) ),
inference(rw,[status(thm)],[120439,132,theory(equality)]) ).
cnf(120451,plain,
( $false
| $false
| ~ aElement0(xy) ),
inference(rw,[status(thm)],[120450,73,theory(equality)]) ).
cnf(120452,plain,
( $false
| $false
| $false ),
inference(rw,[status(thm)],[120451,38,theory(equality)]) ).
cnf(120453,plain,
$false,
inference(cn,[status(thm)],[120452,theory(equality)]) ).
cnf(120454,plain,
$false,
120453,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/RNG/RNG098+1.p
% --creating new selector for []
% -running prover on /tmp/tmpYuWJZm/sel_RNG098+1.p_1 with time limit 29
% -prover status Theorem
% Problem RNG098+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/RNG/RNG098+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/RNG/RNG098+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
%
%------------------------------------------------------------------------------