%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : RNG052+2 : TPTP v5.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art05.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 01:48:03 EST 2010
% Result : Theorem 6.32s
% Output : CNFRefutation 6.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 13
% Syntax : Number of formulae : 72 ( 24 unt; 0 def)
% Number of atoms : 196 ( 79 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 195 ( 71 ~; 84 |; 31 &)
% ( 0 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-2 aty)
% Number of variables : 41 ( 0 sgn 26 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(5,axiom,
aDimensionOf0(xs) = aDimensionOf0(xt),
file('/tmp/tmplaQwQj/sel_RNG052+2.p_1',m__1678_01) ).
fof(7,axiom,
( aScalar0(xE)
& xE = sdtasasdt0(xp,xq) ),
file('/tmp/tmplaQwQj/sel_RNG052+2.p_1',m__1820) ).
fof(14,axiom,
! [X1] :
( aNaturalNumber0(X1)
=> iLess0(X1,szszuzczcdt0(X1)) ),
file('/tmp/tmplaQwQj/sel_RNG052+2.p_1',mIH) ).
fof(26,axiom,
! [X1,X2] :
( ( aVector0(X1)
& aVector0(X2) )
=> ( ( aDimensionOf0(X1) = aDimensionOf0(X2)
& aDimensionOf0(X2) != sz00 )
=> aDimensionOf0(sziznziztdt0(X1)) = aDimensionOf0(sziznziztdt0(X2)) ) ),
file('/tmp/tmplaQwQj/sel_RNG052+2.p_1',mEqInit) ).
fof(30,axiom,
! [X1] :
( aVector0(X1)
=> aNaturalNumber0(aDimensionOf0(X1)) ),
file('/tmp/tmplaQwQj/sel_RNG052+2.p_1',mDimNat) ).
fof(39,axiom,
! [X1,X2] :
( ( aVector0(X1)
& aVector0(X2) )
=> ( aDimensionOf0(X1) = aDimensionOf0(X2)
=> ( iLess0(aDimensionOf0(X1),aDimensionOf0(xs))
=> sdtlseqdt0(sdtasdt0(sdtasasdt0(X1,X2),sdtasasdt0(X1,X2)),sdtasdt0(sdtasasdt0(X1,X1),sdtasasdt0(X2,X2))) ) ) ),
file('/tmp/tmplaQwQj/sel_RNG052+2.p_1',m__1652) ).
fof(42,conjecture,
sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)),
file('/tmp/tmplaQwQj/sel_RNG052+2.p_1',m__) ).
fof(44,axiom,
( aScalar0(xC)
& xC = sdtasasdt0(xp,xp) ),
file('/tmp/tmplaQwQj/sel_RNG052+2.p_1',m__1783) ).
fof(45,axiom,
aDimensionOf0(xs) != sz00,
file('/tmp/tmplaQwQj/sel_RNG052+2.p_1',m__1692) ).
fof(46,axiom,
( aScalar0(xD)
& xD = sdtasasdt0(xq,xq) ),
file('/tmp/tmplaQwQj/sel_RNG052+2.p_1',m__1800) ).
fof(47,axiom,
( aVector0(xs)
& aVector0(xt) ),
file('/tmp/tmplaQwQj/sel_RNG052+2.p_1',m__1678) ).
fof(48,axiom,
( aVector0(xq)
& szszuzczcdt0(aDimensionOf0(xq)) = aDimensionOf0(xt)
& ! [X1] :
( aNaturalNumber0(X1)
=> sdtlbdtrb0(xq,X1) = sdtlbdtrb0(xt,X1) )
& xq = sziznziztdt0(xt) ),
file('/tmp/tmplaQwQj/sel_RNG052+2.p_1',m__1726) ).
fof(50,axiom,
( aVector0(xp)
& szszuzczcdt0(aDimensionOf0(xp)) = aDimensionOf0(xs)
& ! [X1] :
( aNaturalNumber0(X1)
=> sdtlbdtrb0(xp,X1) = sdtlbdtrb0(xs,X1) )
& xp = sziznziztdt0(xs) ),
file('/tmp/tmplaQwQj/sel_RNG052+2.p_1',m__1709) ).
fof(57,negated_conjecture,
~ sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)),
inference(assume_negation,[status(cth)],[42]) ).
fof(58,negated_conjecture,
~ sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)),
inference(fof_simplification,[status(thm)],[57,theory(equality)]) ).
cnf(69,plain,
aDimensionOf0(xs) = aDimensionOf0(xt),
inference(split_conjunct,[status(thm)],[5]) ).
cnf(81,plain,
xE = sdtasasdt0(xp,xq),
inference(split_conjunct,[status(thm)],[7]) ).
fof(101,plain,
! [X1] :
( ~ aNaturalNumber0(X1)
| iLess0(X1,szszuzczcdt0(X1)) ),
inference(fof_nnf,[status(thm)],[14]) ).
fof(102,plain,
! [X2] :
( ~ aNaturalNumber0(X2)
| iLess0(X2,szszuzczcdt0(X2)) ),
inference(variable_rename,[status(thm)],[101]) ).
cnf(103,plain,
( iLess0(X1,szszuzczcdt0(X1))
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[102]) ).
fof(138,plain,
! [X1,X2] :
( ~ aVector0(X1)
| ~ aVector0(X2)
| aDimensionOf0(X1) != aDimensionOf0(X2)
| aDimensionOf0(X2) = sz00
| aDimensionOf0(sziznziztdt0(X1)) = aDimensionOf0(sziznziztdt0(X2)) ),
inference(fof_nnf,[status(thm)],[26]) ).
fof(139,plain,
! [X3,X4] :
( ~ aVector0(X3)
| ~ aVector0(X4)
| aDimensionOf0(X3) != aDimensionOf0(X4)
| aDimensionOf0(X4) = sz00
| aDimensionOf0(sziznziztdt0(X3)) = aDimensionOf0(sziznziztdt0(X4)) ),
inference(variable_rename,[status(thm)],[138]) ).
cnf(140,plain,
( aDimensionOf0(sziznziztdt0(X1)) = aDimensionOf0(sziznziztdt0(X2))
| aDimensionOf0(X2) = sz00
| aDimensionOf0(X1) != aDimensionOf0(X2)
| ~ aVector0(X2)
| ~ aVector0(X1) ),
inference(split_conjunct,[status(thm)],[139]) ).
fof(158,plain,
! [X1] :
( ~ aVector0(X1)
| aNaturalNumber0(aDimensionOf0(X1)) ),
inference(fof_nnf,[status(thm)],[30]) ).
fof(159,plain,
! [X2] :
( ~ aVector0(X2)
| aNaturalNumber0(aDimensionOf0(X2)) ),
inference(variable_rename,[status(thm)],[158]) ).
cnf(160,plain,
( aNaturalNumber0(aDimensionOf0(X1))
| ~ aVector0(X1) ),
inference(split_conjunct,[status(thm)],[159]) ).
fof(187,plain,
! [X1,X2] :
( ~ aVector0(X1)
| ~ aVector0(X2)
| aDimensionOf0(X1) != aDimensionOf0(X2)
| ~ iLess0(aDimensionOf0(X1),aDimensionOf0(xs))
| sdtlseqdt0(sdtasdt0(sdtasasdt0(X1,X2),sdtasasdt0(X1,X2)),sdtasdt0(sdtasasdt0(X1,X1),sdtasasdt0(X2,X2))) ),
inference(fof_nnf,[status(thm)],[39]) ).
fof(188,plain,
! [X3,X4] :
( ~ aVector0(X3)
| ~ aVector0(X4)
| aDimensionOf0(X3) != aDimensionOf0(X4)
| ~ iLess0(aDimensionOf0(X3),aDimensionOf0(xs))
| sdtlseqdt0(sdtasdt0(sdtasasdt0(X3,X4),sdtasasdt0(X3,X4)),sdtasdt0(sdtasasdt0(X3,X3),sdtasasdt0(X4,X4))) ),
inference(variable_rename,[status(thm)],[187]) ).
cnf(189,plain,
( sdtlseqdt0(sdtasdt0(sdtasasdt0(X1,X2),sdtasasdt0(X1,X2)),sdtasdt0(sdtasasdt0(X1,X1),sdtasasdt0(X2,X2)))
| ~ iLess0(aDimensionOf0(X1),aDimensionOf0(xs))
| aDimensionOf0(X1) != aDimensionOf0(X2)
| ~ aVector0(X2)
| ~ aVector0(X1) ),
inference(split_conjunct,[status(thm)],[188]) ).
cnf(196,negated_conjecture,
~ sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)),
inference(split_conjunct,[status(thm)],[58]) ).
cnf(202,plain,
xC = sdtasasdt0(xp,xp),
inference(split_conjunct,[status(thm)],[44]) ).
cnf(204,plain,
aDimensionOf0(xs) != sz00,
inference(split_conjunct,[status(thm)],[45]) ).
cnf(205,plain,
xD = sdtasasdt0(xq,xq),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(207,plain,
aVector0(xt),
inference(split_conjunct,[status(thm)],[47]) ).
cnf(208,plain,
aVector0(xs),
inference(split_conjunct,[status(thm)],[47]) ).
fof(209,plain,
( aVector0(xq)
& szszuzczcdt0(aDimensionOf0(xq)) = aDimensionOf0(xt)
& ! [X1] :
( ~ aNaturalNumber0(X1)
| sdtlbdtrb0(xq,X1) = sdtlbdtrb0(xt,X1) )
& xq = sziznziztdt0(xt) ),
inference(fof_nnf,[status(thm)],[48]) ).
fof(210,plain,
( aVector0(xq)
& szszuzczcdt0(aDimensionOf0(xq)) = aDimensionOf0(xt)
& ! [X2] :
( ~ aNaturalNumber0(X2)
| sdtlbdtrb0(xq,X2) = sdtlbdtrb0(xt,X2) )
& xq = sziznziztdt0(xt) ),
inference(variable_rename,[status(thm)],[209]) ).
fof(211,plain,
! [X2] :
( ( ~ aNaturalNumber0(X2)
| sdtlbdtrb0(xq,X2) = sdtlbdtrb0(xt,X2) )
& aVector0(xq)
& szszuzczcdt0(aDimensionOf0(xq)) = aDimensionOf0(xt)
& xq = sziznziztdt0(xt) ),
inference(shift_quantors,[status(thm)],[210]) ).
cnf(212,plain,
xq = sziznziztdt0(xt),
inference(split_conjunct,[status(thm)],[211]) ).
cnf(214,plain,
aVector0(xq),
inference(split_conjunct,[status(thm)],[211]) ).
fof(219,plain,
( aVector0(xp)
& szszuzczcdt0(aDimensionOf0(xp)) = aDimensionOf0(xs)
& ! [X1] :
( ~ aNaturalNumber0(X1)
| sdtlbdtrb0(xp,X1) = sdtlbdtrb0(xs,X1) )
& xp = sziznziztdt0(xs) ),
inference(fof_nnf,[status(thm)],[50]) ).
fof(220,plain,
( aVector0(xp)
& szszuzczcdt0(aDimensionOf0(xp)) = aDimensionOf0(xs)
& ! [X2] :
( ~ aNaturalNumber0(X2)
| sdtlbdtrb0(xp,X2) = sdtlbdtrb0(xs,X2) )
& xp = sziznziztdt0(xs) ),
inference(variable_rename,[status(thm)],[219]) ).
fof(221,plain,
! [X2] :
( ( ~ aNaturalNumber0(X2)
| sdtlbdtrb0(xp,X2) = sdtlbdtrb0(xs,X2) )
& aVector0(xp)
& szszuzczcdt0(aDimensionOf0(xp)) = aDimensionOf0(xs)
& xp = sziznziztdt0(xs) ),
inference(shift_quantors,[status(thm)],[220]) ).
cnf(222,plain,
xp = sziznziztdt0(xs),
inference(split_conjunct,[status(thm)],[221]) ).
cnf(223,plain,
szszuzczcdt0(aDimensionOf0(xp)) = aDimensionOf0(xs),
inference(split_conjunct,[status(thm)],[221]) ).
cnf(224,plain,
aVector0(xp),
inference(split_conjunct,[status(thm)],[221]) ).
cnf(277,plain,
( iLess0(aDimensionOf0(xp),aDimensionOf0(xs))
| ~ aNaturalNumber0(aDimensionOf0(xp)) ),
inference(spm,[status(thm)],[103,223,theory(equality)]) ).
cnf(833,plain,
( aDimensionOf0(sziznziztdt0(xt)) = aDimensionOf0(sziznziztdt0(X1))
| aDimensionOf0(X1) = sz00
| aDimensionOf0(xs) != aDimensionOf0(X1)
| ~ aVector0(X1)
| ~ aVector0(xt) ),
inference(spm,[status(thm)],[140,69,theory(equality)]) ).
cnf(835,plain,
( aDimensionOf0(xq) = aDimensionOf0(sziznziztdt0(X1))
| aDimensionOf0(X1) = sz00
| aDimensionOf0(xs) != aDimensionOf0(X1)
| ~ aVector0(X1)
| ~ aVector0(xt) ),
inference(rw,[status(thm)],[833,212,theory(equality)]) ).
cnf(836,plain,
( aDimensionOf0(xq) = aDimensionOf0(sziznziztdt0(X1))
| aDimensionOf0(X1) = sz00
| aDimensionOf0(xs) != aDimensionOf0(X1)
| ~ aVector0(X1)
| $false ),
inference(rw,[status(thm)],[835,207,theory(equality)]) ).
cnf(837,plain,
( aDimensionOf0(xq) = aDimensionOf0(sziznziztdt0(X1))
| aDimensionOf0(X1) = sz00
| aDimensionOf0(xs) != aDimensionOf0(X1)
| ~ aVector0(X1) ),
inference(cn,[status(thm)],[836,theory(equality)]) ).
cnf(1113,plain,
( sdtlseqdt0(sdtasdt0(sdtasasdt0(xp,X1),sdtasasdt0(xp,X1)),sdtasdt0(xC,sdtasasdt0(X1,X1)))
| aDimensionOf0(xp) != aDimensionOf0(X1)
| ~ iLess0(aDimensionOf0(xp),aDimensionOf0(xs))
| ~ aVector0(X1)
| ~ aVector0(xp) ),
inference(spm,[status(thm)],[189,202,theory(equality)]) ).
cnf(1127,plain,
( sdtlseqdt0(sdtasdt0(sdtasasdt0(xp,X1),sdtasasdt0(xp,X1)),sdtasdt0(xC,sdtasasdt0(X1,X1)))
| aDimensionOf0(xp) != aDimensionOf0(X1)
| ~ iLess0(aDimensionOf0(xp),aDimensionOf0(xs))
| ~ aVector0(X1)
| $false ),
inference(rw,[status(thm)],[1113,224,theory(equality)]) ).
cnf(1128,plain,
( sdtlseqdt0(sdtasdt0(sdtasasdt0(xp,X1),sdtasasdt0(xp,X1)),sdtasdt0(xC,sdtasasdt0(X1,X1)))
| aDimensionOf0(xp) != aDimensionOf0(X1)
| ~ iLess0(aDimensionOf0(xp),aDimensionOf0(xs))
| ~ aVector0(X1) ),
inference(cn,[status(thm)],[1127,theory(equality)]) ).
cnf(57122,plain,
( aDimensionOf0(xp) = aDimensionOf0(xq)
| aDimensionOf0(xs) = sz00
| ~ aVector0(xs) ),
inference(spm,[status(thm)],[837,222,theory(equality)]) ).
cnf(57131,plain,
( aDimensionOf0(xp) = aDimensionOf0(xq)
| aDimensionOf0(xs) = sz00
| $false ),
inference(rw,[status(thm)],[57122,208,theory(equality)]) ).
cnf(57132,plain,
( aDimensionOf0(xp) = aDimensionOf0(xq)
| aDimensionOf0(xs) = sz00 ),
inference(cn,[status(thm)],[57131,theory(equality)]) ).
cnf(57133,plain,
aDimensionOf0(xq) = aDimensionOf0(xp),
inference(sr,[status(thm)],[57132,204,theory(equality)]) ).
cnf(57137,plain,
( aNaturalNumber0(aDimensionOf0(xp))
| ~ aVector0(xq) ),
inference(spm,[status(thm)],[160,57133,theory(equality)]) ).
cnf(57155,plain,
( aNaturalNumber0(aDimensionOf0(xp))
| $false ),
inference(rw,[status(thm)],[57137,214,theory(equality)]) ).
cnf(57156,plain,
aNaturalNumber0(aDimensionOf0(xp)),
inference(cn,[status(thm)],[57155,theory(equality)]) ).
cnf(57170,plain,
( iLess0(aDimensionOf0(xp),aDimensionOf0(xs))
| $false ),
inference(rw,[status(thm)],[277,57156,theory(equality)]) ).
cnf(57171,plain,
iLess0(aDimensionOf0(xp),aDimensionOf0(xs)),
inference(cn,[status(thm)],[57170,theory(equality)]) ).
cnf(175304,plain,
( sdtlseqdt0(sdtasdt0(sdtasasdt0(xp,X1),sdtasasdt0(xp,X1)),sdtasdt0(xC,sdtasasdt0(X1,X1)))
| aDimensionOf0(xp) != aDimensionOf0(X1)
| $false
| ~ aVector0(X1) ),
inference(rw,[status(thm)],[1128,57171,theory(equality)]) ).
cnf(175305,plain,
( sdtlseqdt0(sdtasdt0(sdtasasdt0(xp,X1),sdtasasdt0(xp,X1)),sdtasdt0(xC,sdtasasdt0(X1,X1)))
| aDimensionOf0(xp) != aDimensionOf0(X1)
| ~ aVector0(X1) ),
inference(cn,[status(thm)],[175304,theory(equality)]) ).
cnf(175308,plain,
( sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,sdtasasdt0(xq,xq)))
| aDimensionOf0(xp) != aDimensionOf0(xq)
| ~ aVector0(xq) ),
inference(spm,[status(thm)],[175305,81,theory(equality)]) ).
cnf(175331,plain,
( sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD))
| aDimensionOf0(xp) != aDimensionOf0(xq)
| ~ aVector0(xq) ),
inference(rw,[status(thm)],[175308,205,theory(equality)]) ).
cnf(175332,plain,
( sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD))
| $false
| ~ aVector0(xq) ),
inference(rw,[status(thm)],[175331,57133,theory(equality)]) ).
cnf(175333,plain,
( sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD))
| $false
| $false ),
inference(rw,[status(thm)],[175332,214,theory(equality)]) ).
cnf(175334,plain,
sdtlseqdt0(sdtasdt0(xE,xE),sdtasdt0(xC,xD)),
inference(cn,[status(thm)],[175333,theory(equality)]) ).
cnf(175335,plain,
$false,
inference(sr,[status(thm)],[175334,196,theory(equality)]) ).
cnf(175336,plain,
$false,
175335,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/RNG/RNG052+2.p
% --creating new selector for []
% -running prover on /tmp/tmplaQwQj/sel_RNG052+2.p_1 with time limit 29
% -prover status Theorem
% Problem RNG052+2.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/RNG/RNG052+2.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/RNG/RNG052+2.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
%
%------------------------------------------------------------------------------