%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : RNG126+1 : TPTP v5.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art11.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 3.00GHz @ 3000MHz
% Memory : 2006MB
% OS : Linux 2.6.31.5-127.fc12.i686.PAE
% CPULimit : 300s
% DateTime : Sun Dec 26 02:40:02 EST 2010
% Result : Theorem 5.14s
% Output : CNFRefutation 5.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 12
% Syntax : Number of formulae : 77 ( 21 unt; 0 def)
% Number of atoms : 413 ( 28 equ)
% Maximal formula atoms : 32 ( 5 avg)
% Number of connectives : 556 ( 220 ~; 223 |; 99 &)
% ( 4 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 6 con; 0-3 aty)
% Number of variables : 124 ( 0 sgn 86 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(1,axiom,
( aDivisorOf0(xu,xa)
& aDivisorOf0(xu,xb) ),
file('/tmp/tmp7kQ2ij/sel_RNG126+1.p_1',m__2373) ).
fof(7,axiom,
aGcdOfAnd0(xc,xa,xb),
file('/tmp/tmp7kQ2ij/sel_RNG126+1.p_1',m__2129) ).
fof(9,axiom,
! [X1,X2] :
( ( aElement0(X1)
& aElement0(X2) )
=> ( doDivides0(X1,X2)
<=> ? [X3] :
( aElement0(X3)
& sdtasdt0(X1,X3) = X2 ) ) ),
file('/tmp/tmp7kQ2ij/sel_RNG126+1.p_1',mDefDiv) ).
fof(11,axiom,
( aElementOf0(xu,xI)
& xu != sz00
& ! [X1] :
( ( aElementOf0(X1,xI)
& X1 != sz00 )
=> ~ iLess0(sbrdtbr0(X1),sbrdtbr0(xu)) ) ),
file('/tmp/tmp7kQ2ij/sel_RNG126+1.p_1',m__2273) ).
fof(20,axiom,
! [X1] :
( aElement0(X1)
=> ! [X2] :
( aDivisorOf0(X2,X1)
<=> ( aElement0(X2)
& doDivides0(X2,X1) ) ) ),
file('/tmp/tmp7kQ2ij/sel_RNG126+1.p_1',mDefDvs) ).
fof(25,axiom,
( aIdeal0(xI)
& xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)) ),
file('/tmp/tmp7kQ2ij/sel_RNG126+1.p_1',m__2174) ).
fof(26,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/tmp7kQ2ij/sel_RNG126+1.p_1',mDefIdeal) ).
fof(35,axiom,
! [X1,X2] :
( ( aElement0(X1)
& aElement0(X2) )
=> ! [X3] :
( aGcdOfAnd0(X3,X1,X2)
<=> ( aDivisorOf0(X3,X1)
& aDivisorOf0(X3,X2)
& ! [X4] :
( ( aDivisorOf0(X4,X1)
& aDivisorOf0(X4,X2) )
=> doDivides0(X4,X3) ) ) ) ),
file('/tmp/tmp7kQ2ij/sel_RNG126+1.p_1',mDefGCD) ).
fof(36,axiom,
( aElement0(xa)
& aElement0(xb) ),
file('/tmp/tmp7kQ2ij/sel_RNG126+1.p_1',m__2091) ).
fof(39,axiom,
! [X1,X2] :
( ( aElement0(X1)
& aElement0(X2) )
=> sdtasdt0(X1,X2) = sdtasdt0(X2,X1) ),
file('/tmp/tmp7kQ2ij/sel_RNG126+1.p_1',mMulComm) ).
fof(43,axiom,
doDivides0(xu,xc),
file('/tmp/tmp7kQ2ij/sel_RNG126+1.p_1',m__2744) ).
fof(48,conjecture,
aElementOf0(xc,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))),
file('/tmp/tmp7kQ2ij/sel_RNG126+1.p_1',m__) ).
fof(49,negated_conjecture,
~ aElementOf0(xc,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))),
inference(assume_negation,[status(cth)],[48]) ).
fof(50,plain,
( aElementOf0(xu,xI)
& xu != sz00
& ! [X1] :
( ( aElementOf0(X1,xI)
& X1 != sz00 )
=> ~ iLess0(sbrdtbr0(X1),sbrdtbr0(xu)) ) ),
inference(fof_simplification,[status(thm)],[11,theory(equality)]) ).
fof(51,negated_conjecture,
~ aElementOf0(xc,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))),
inference(fof_simplification,[status(thm)],[49,theory(equality)]) ).
cnf(53,plain,
aDivisorOf0(xu,xa),
inference(split_conjunct,[status(thm)],[1]) ).
cnf(80,plain,
aGcdOfAnd0(xc,xa,xb),
inference(split_conjunct,[status(thm)],[7]) ).
fof(86,plain,
! [X1,X2] :
( ~ aElement0(X1)
| ~ aElement0(X2)
| ( ( ~ doDivides0(X1,X2)
| ? [X3] :
( aElement0(X3)
& sdtasdt0(X1,X3) = X2 ) )
& ( ! [X3] :
( ~ aElement0(X3)
| sdtasdt0(X1,X3) != X2 )
| doDivides0(X1,X2) ) ) ),
inference(fof_nnf,[status(thm)],[9]) ).
fof(87,plain,
! [X4,X5] :
( ~ aElement0(X4)
| ~ aElement0(X5)
| ( ( ~ doDivides0(X4,X5)
| ? [X6] :
( aElement0(X6)
& sdtasdt0(X4,X6) = X5 ) )
& ( ! [X7] :
( ~ aElement0(X7)
| sdtasdt0(X4,X7) != X5 )
| doDivides0(X4,X5) ) ) ),
inference(variable_rename,[status(thm)],[86]) ).
fof(88,plain,
! [X4,X5] :
( ~ aElement0(X4)
| ~ aElement0(X5)
| ( ( ~ doDivides0(X4,X5)
| ( aElement0(esk3_2(X4,X5))
& sdtasdt0(X4,esk3_2(X4,X5)) = X5 ) )
& ( ! [X7] :
( ~ aElement0(X7)
| sdtasdt0(X4,X7) != X5 )
| doDivides0(X4,X5) ) ) ),
inference(skolemize,[status(esa)],[87]) ).
fof(89,plain,
! [X4,X5,X7] :
( ( ( ~ aElement0(X7)
| sdtasdt0(X4,X7) != X5
| doDivides0(X4,X5) )
& ( ~ doDivides0(X4,X5)
| ( aElement0(esk3_2(X4,X5))
& sdtasdt0(X4,esk3_2(X4,X5)) = X5 ) ) )
| ~ aElement0(X4)
| ~ aElement0(X5) ),
inference(shift_quantors,[status(thm)],[88]) ).
fof(90,plain,
! [X4,X5,X7] :
( ( ~ aElement0(X7)
| sdtasdt0(X4,X7) != X5
| doDivides0(X4,X5)
| ~ aElement0(X4)
| ~ aElement0(X5) )
& ( aElement0(esk3_2(X4,X5))
| ~ doDivides0(X4,X5)
| ~ aElement0(X4)
| ~ aElement0(X5) )
& ( sdtasdt0(X4,esk3_2(X4,X5)) = X5
| ~ doDivides0(X4,X5)
| ~ aElement0(X4)
| ~ aElement0(X5) ) ),
inference(distribute,[status(thm)],[89]) ).
cnf(91,plain,
( sdtasdt0(X2,esk3_2(X2,X1)) = X1
| ~ aElement0(X1)
| ~ aElement0(X2)
| ~ doDivides0(X2,X1) ),
inference(split_conjunct,[status(thm)],[90]) ).
cnf(92,plain,
( aElement0(esk3_2(X2,X1))
| ~ aElement0(X1)
| ~ aElement0(X2)
| ~ doDivides0(X2,X1) ),
inference(split_conjunct,[status(thm)],[90]) ).
fof(102,plain,
( aElementOf0(xu,xI)
& xu != sz00
& ! [X1] :
( ~ aElementOf0(X1,xI)
| X1 = sz00
| ~ iLess0(sbrdtbr0(X1),sbrdtbr0(xu)) ) ),
inference(fof_nnf,[status(thm)],[50]) ).
fof(103,plain,
( aElementOf0(xu,xI)
& xu != sz00
& ! [X2] :
( ~ aElementOf0(X2,xI)
| X2 = sz00
| ~ iLess0(sbrdtbr0(X2),sbrdtbr0(xu)) ) ),
inference(variable_rename,[status(thm)],[102]) ).
fof(104,plain,
! [X2] :
( ( ~ aElementOf0(X2,xI)
| X2 = sz00
| ~ iLess0(sbrdtbr0(X2),sbrdtbr0(xu)) )
& aElementOf0(xu,xI)
& xu != sz00 ),
inference(shift_quantors,[status(thm)],[103]) ).
cnf(106,plain,
aElementOf0(xu,xI),
inference(split_conjunct,[status(thm)],[104]) ).
fof(136,plain,
! [X1] :
( ~ aElement0(X1)
| ! [X2] :
( ( ~ aDivisorOf0(X2,X1)
| ( aElement0(X2)
& doDivides0(X2,X1) ) )
& ( ~ aElement0(X2)
| ~ doDivides0(X2,X1)
| aDivisorOf0(X2,X1) ) ) ),
inference(fof_nnf,[status(thm)],[20]) ).
fof(137,plain,
! [X3] :
( ~ aElement0(X3)
| ! [X4] :
( ( ~ aDivisorOf0(X4,X3)
| ( aElement0(X4)
& doDivides0(X4,X3) ) )
& ( ~ aElement0(X4)
| ~ doDivides0(X4,X3)
| aDivisorOf0(X4,X3) ) ) ),
inference(variable_rename,[status(thm)],[136]) ).
fof(138,plain,
! [X3,X4] :
( ( ( ~ aDivisorOf0(X4,X3)
| ( aElement0(X4)
& doDivides0(X4,X3) ) )
& ( ~ aElement0(X4)
| ~ doDivides0(X4,X3)
| aDivisorOf0(X4,X3) ) )
| ~ aElement0(X3) ),
inference(shift_quantors,[status(thm)],[137]) ).
fof(139,plain,
! [X3,X4] :
( ( aElement0(X4)
| ~ aDivisorOf0(X4,X3)
| ~ aElement0(X3) )
& ( doDivides0(X4,X3)
| ~ aDivisorOf0(X4,X3)
| ~ aElement0(X3) )
& ( ~ aElement0(X4)
| ~ doDivides0(X4,X3)
| aDivisorOf0(X4,X3)
| ~ aElement0(X3) ) ),
inference(distribute,[status(thm)],[138]) ).
cnf(142,plain,
( aElement0(X2)
| ~ aElement0(X1)
| ~ aDivisorOf0(X2,X1) ),
inference(split_conjunct,[status(thm)],[139]) ).
cnf(158,plain,
xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)),
inference(split_conjunct,[status(thm)],[25]) ).
cnf(159,plain,
aIdeal0(xI),
inference(split_conjunct,[status(thm)],[25]) ).
fof(160,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)],[26]) ).
fof(161,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)],[160]) ).
fof(162,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(esk9_1(X4),X4)
& ( ( aElementOf0(esk10_1(X4),X4)
& ~ aElementOf0(sdtpldt0(esk9_1(X4),esk10_1(X4)),X4) )
| ( aElement0(esk11_1(X4))
& ~ aElementOf0(sdtasdt0(esk11_1(X4),esk9_1(X4)),X4) ) ) )
| aIdeal0(X4) ) ),
inference(skolemize,[status(esa)],[161]) ).
fof(163,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(esk9_1(X4),X4)
& ( ( aElementOf0(esk10_1(X4),X4)
& ~ aElementOf0(sdtpldt0(esk9_1(X4),esk10_1(X4)),X4) )
| ( aElement0(esk11_1(X4))
& ~ aElementOf0(sdtasdt0(esk11_1(X4),esk9_1(X4)),X4) ) ) )
| aIdeal0(X4) ) ),
inference(shift_quantors,[status(thm)],[162]) ).
fof(164,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(esk9_1(X4),X4)
| ~ aSet0(X4)
| aIdeal0(X4) )
& ( aElement0(esk11_1(X4))
| aElementOf0(esk10_1(X4),X4)
| ~ aSet0(X4)
| aIdeal0(X4) )
& ( ~ aElementOf0(sdtasdt0(esk11_1(X4),esk9_1(X4)),X4)
| aElementOf0(esk10_1(X4),X4)
| ~ aSet0(X4)
| aIdeal0(X4) )
& ( aElement0(esk11_1(X4))
| ~ aElementOf0(sdtpldt0(esk9_1(X4),esk10_1(X4)),X4)
| ~ aSet0(X4)
| aIdeal0(X4) )
& ( ~ aElementOf0(sdtasdt0(esk11_1(X4),esk9_1(X4)),X4)
| ~ aElementOf0(sdtpldt0(esk9_1(X4),esk10_1(X4)),X4)
| ~ aSet0(X4)
| aIdeal0(X4) ) ),
inference(distribute,[status(thm)],[163]) ).
cnf(172,plain,
( aElementOf0(sdtasdt0(X3,X2),X1)
| ~ aIdeal0(X1)
| ~ aElementOf0(X2,X1)
| ~ aElement0(X3) ),
inference(split_conjunct,[status(thm)],[164]) ).
fof(209,plain,
! [X1,X2] :
( ~ aElement0(X1)
| ~ aElement0(X2)
| ! [X3] :
( ( ~ aGcdOfAnd0(X3,X1,X2)
| ( aDivisorOf0(X3,X1)
& aDivisorOf0(X3,X2)
& ! [X4] :
( ~ aDivisorOf0(X4,X1)
| ~ aDivisorOf0(X4,X2)
| doDivides0(X4,X3) ) ) )
& ( ~ aDivisorOf0(X3,X1)
| ~ aDivisorOf0(X3,X2)
| ? [X4] :
( aDivisorOf0(X4,X1)
& aDivisorOf0(X4,X2)
& ~ doDivides0(X4,X3) )
| aGcdOfAnd0(X3,X1,X2) ) ) ),
inference(fof_nnf,[status(thm)],[35]) ).
fof(210,plain,
! [X5,X6] :
( ~ aElement0(X5)
| ~ aElement0(X6)
| ! [X7] :
( ( ~ aGcdOfAnd0(X7,X5,X6)
| ( aDivisorOf0(X7,X5)
& aDivisorOf0(X7,X6)
& ! [X8] :
( ~ aDivisorOf0(X8,X5)
| ~ aDivisorOf0(X8,X6)
| doDivides0(X8,X7) ) ) )
& ( ~ aDivisorOf0(X7,X5)
| ~ aDivisorOf0(X7,X6)
| ? [X9] :
( aDivisorOf0(X9,X5)
& aDivisorOf0(X9,X6)
& ~ doDivides0(X9,X7) )
| aGcdOfAnd0(X7,X5,X6) ) ) ),
inference(variable_rename,[status(thm)],[209]) ).
fof(211,plain,
! [X5,X6] :
( ~ aElement0(X5)
| ~ aElement0(X6)
| ! [X7] :
( ( ~ aGcdOfAnd0(X7,X5,X6)
| ( aDivisorOf0(X7,X5)
& aDivisorOf0(X7,X6)
& ! [X8] :
( ~ aDivisorOf0(X8,X5)
| ~ aDivisorOf0(X8,X6)
| doDivides0(X8,X7) ) ) )
& ( ~ aDivisorOf0(X7,X5)
| ~ aDivisorOf0(X7,X6)
| ( aDivisorOf0(esk18_3(X5,X6,X7),X5)
& aDivisorOf0(esk18_3(X5,X6,X7),X6)
& ~ doDivides0(esk18_3(X5,X6,X7),X7) )
| aGcdOfAnd0(X7,X5,X6) ) ) ),
inference(skolemize,[status(esa)],[210]) ).
fof(212,plain,
! [X5,X6,X7,X8] :
( ( ( ( ( ~ aDivisorOf0(X8,X5)
| ~ aDivisorOf0(X8,X6)
| doDivides0(X8,X7) )
& aDivisorOf0(X7,X5)
& aDivisorOf0(X7,X6) )
| ~ aGcdOfAnd0(X7,X5,X6) )
& ( ~ aDivisorOf0(X7,X5)
| ~ aDivisorOf0(X7,X6)
| ( aDivisorOf0(esk18_3(X5,X6,X7),X5)
& aDivisorOf0(esk18_3(X5,X6,X7),X6)
& ~ doDivides0(esk18_3(X5,X6,X7),X7) )
| aGcdOfAnd0(X7,X5,X6) ) )
| ~ aElement0(X5)
| ~ aElement0(X6) ),
inference(shift_quantors,[status(thm)],[211]) ).
fof(213,plain,
! [X5,X6,X7,X8] :
( ( ~ aDivisorOf0(X8,X5)
| ~ aDivisorOf0(X8,X6)
| doDivides0(X8,X7)
| ~ aGcdOfAnd0(X7,X5,X6)
| ~ aElement0(X5)
| ~ aElement0(X6) )
& ( aDivisorOf0(X7,X5)
| ~ aGcdOfAnd0(X7,X5,X6)
| ~ aElement0(X5)
| ~ aElement0(X6) )
& ( aDivisorOf0(X7,X6)
| ~ aGcdOfAnd0(X7,X5,X6)
| ~ aElement0(X5)
| ~ aElement0(X6) )
& ( aDivisorOf0(esk18_3(X5,X6,X7),X5)
| ~ aDivisorOf0(X7,X5)
| ~ aDivisorOf0(X7,X6)
| aGcdOfAnd0(X7,X5,X6)
| ~ aElement0(X5)
| ~ aElement0(X6) )
& ( aDivisorOf0(esk18_3(X5,X6,X7),X6)
| ~ aDivisorOf0(X7,X5)
| ~ aDivisorOf0(X7,X6)
| aGcdOfAnd0(X7,X5,X6)
| ~ aElement0(X5)
| ~ aElement0(X6) )
& ( ~ doDivides0(esk18_3(X5,X6,X7),X7)
| ~ aDivisorOf0(X7,X5)
| ~ aDivisorOf0(X7,X6)
| aGcdOfAnd0(X7,X5,X6)
| ~ aElement0(X5)
| ~ aElement0(X6) ) ),
inference(distribute,[status(thm)],[212]) ).
cnf(218,plain,
( aDivisorOf0(X3,X2)
| ~ aElement0(X1)
| ~ aElement0(X2)
| ~ aGcdOfAnd0(X3,X2,X1) ),
inference(split_conjunct,[status(thm)],[213]) ).
cnf(220,plain,
aElement0(xb),
inference(split_conjunct,[status(thm)],[36]) ).
cnf(221,plain,
aElement0(xa),
inference(split_conjunct,[status(thm)],[36]) ).
fof(235,plain,
! [X1,X2] :
( ~ aElement0(X1)
| ~ aElement0(X2)
| sdtasdt0(X1,X2) = sdtasdt0(X2,X1) ),
inference(fof_nnf,[status(thm)],[39]) ).
fof(236,plain,
! [X3,X4] :
( ~ aElement0(X3)
| ~ aElement0(X4)
| sdtasdt0(X3,X4) = sdtasdt0(X4,X3) ),
inference(variable_rename,[status(thm)],[235]) ).
cnf(237,plain,
( sdtasdt0(X1,X2) = sdtasdt0(X2,X1)
| ~ aElement0(X2)
| ~ aElement0(X1) ),
inference(split_conjunct,[status(thm)],[236]) ).
cnf(248,plain,
doDivides0(xu,xc),
inference(split_conjunct,[status(thm)],[43]) ).
cnf(274,negated_conjecture,
~ aElementOf0(xc,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))),
inference(split_conjunct,[status(thm)],[51]) ).
cnf(289,plain,
( aElement0(xu)
| ~ aElement0(xa) ),
inference(spm,[status(thm)],[142,53,theory(equality)]) ).
cnf(291,plain,
( aElement0(xu)
| $false ),
inference(rw,[status(thm)],[289,221,theory(equality)]) ).
cnf(292,plain,
aElement0(xu),
inference(cn,[status(thm)],[291,theory(equality)]) ).
cnf(337,negated_conjecture,
~ aElementOf0(xc,xI),
inference(rw,[status(thm)],[274,158,theory(equality)]) ).
cnf(420,plain,
( aDivisorOf0(xc,xa)
| ~ aElement0(xa)
| ~ aElement0(xb) ),
inference(spm,[status(thm)],[218,80,theory(equality)]) ).
cnf(421,plain,
( aDivisorOf0(xc,xa)
| $false
| ~ aElement0(xb) ),
inference(rw,[status(thm)],[420,221,theory(equality)]) ).
cnf(422,plain,
( aDivisorOf0(xc,xa)
| $false
| $false ),
inference(rw,[status(thm)],[421,220,theory(equality)]) ).
cnf(423,plain,
aDivisorOf0(xc,xa),
inference(cn,[status(thm)],[422,theory(equality)]) ).
cnf(446,plain,
( aElementOf0(sdtasdt0(X2,X1),X3)
| ~ aIdeal0(X3)
| ~ aElement0(X1)
| ~ aElementOf0(X2,X3)
| ~ aElement0(X2) ),
inference(spm,[status(thm)],[172,237,theory(equality)]) ).
cnf(737,plain,
( aElement0(xc)
| ~ aElement0(xa) ),
inference(spm,[status(thm)],[142,423,theory(equality)]) ).
cnf(738,plain,
( aElement0(xc)
| $false ),
inference(rw,[status(thm)],[737,221,theory(equality)]) ).
cnf(739,plain,
aElement0(xc),
inference(cn,[status(thm)],[738,theory(equality)]) ).
cnf(2183,plain,
( aElementOf0(X2,X3)
| ~ aIdeal0(X3)
| ~ aElement0(esk3_2(X1,X2))
| ~ aElement0(X1)
| ~ aElementOf0(X1,X3)
| ~ doDivides0(X1,X2)
| ~ aElement0(X2) ),
inference(spm,[status(thm)],[446,91,theory(equality)]) ).
cnf(126982,plain,
( aElementOf0(X2,X3)
| ~ doDivides0(X1,X2)
| ~ aIdeal0(X3)
| ~ aElement0(X1)
| ~ aElement0(X2)
| ~ aElementOf0(X1,X3) ),
inference(csr,[status(thm)],[2183,92]) ).
cnf(126983,plain,
( aElementOf0(xc,X1)
| ~ aIdeal0(X1)
| ~ aElement0(xu)
| ~ aElement0(xc)
| ~ aElementOf0(xu,X1) ),
inference(spm,[status(thm)],[126982,248,theory(equality)]) ).
cnf(127114,plain,
( aElementOf0(xc,X1)
| ~ aIdeal0(X1)
| $false
| ~ aElement0(xc)
| ~ aElementOf0(xu,X1) ),
inference(rw,[status(thm)],[126983,292,theory(equality)]) ).
cnf(127115,plain,
( aElementOf0(xc,X1)
| ~ aIdeal0(X1)
| $false
| $false
| ~ aElementOf0(xu,X1) ),
inference(rw,[status(thm)],[127114,739,theory(equality)]) ).
cnf(127116,plain,
( aElementOf0(xc,X1)
| ~ aIdeal0(X1)
| ~ aElementOf0(xu,X1) ),
inference(cn,[status(thm)],[127115,theory(equality)]) ).
cnf(127337,plain,
( aElementOf0(xc,xI)
| ~ aElementOf0(xu,xI) ),
inference(spm,[status(thm)],[127116,159,theory(equality)]) ).
cnf(127341,plain,
( aElementOf0(xc,xI)
| $false ),
inference(rw,[status(thm)],[127337,106,theory(equality)]) ).
cnf(127342,plain,
aElementOf0(xc,xI),
inference(cn,[status(thm)],[127341,theory(equality)]) ).
cnf(127343,plain,
$false,
inference(sr,[status(thm)],[127342,337,theory(equality)]) ).
cnf(127344,plain,
$false,
127343,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% /home/graph/tptp/Systems/SInE---0.4/Source/sine.py:10: DeprecationWarning: the sets module is deprecated
% from sets import Set
% % SZS status Started for /home/graph/tptp/TPTP/Problems/RNG/RNG126+1.p
% --creating new selector for []
% -running prover on /tmp/tmp7kQ2ij/sel_RNG126+1.p_1 with time limit 29
% -prover status Theorem
% Problem RNG126+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/RNG/RNG126+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/RNG/RNG126+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
%
%------------------------------------------------------------------------------