%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : RNG047+2 : TPTP v5.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art04.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:47:01 EST 2010
% Result : Theorem 0.20s
% Output : CNFRefutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 4
% Syntax : Number of formulae : 31 ( 12 unt; 0 def)
% Number of atoms : 100 ( 49 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 106 ( 37 ~; 30 |; 28 &)
% ( 0 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 26 ( 0 sgn 19 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(17,axiom,
! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( szszuzczcdt0(X1) = szszuzczcdt0(X2)
=> X1 = X2 ) ),
file('/tmp/tmprBGJav/sel_RNG047+2.p_1',mSuccEqu) ).
fof(21,axiom,
! [X1] :
( aVector0(X1)
=> aNaturalNumber0(aDimensionOf0(X1)) ),
file('/tmp/tmprBGJav/sel_RNG047+2.p_1',mDimNat) ).
fof(22,axiom,
( aDimensionOf0(xs) = aDimensionOf0(xt)
& aDimensionOf0(xt) != sz00 ),
file('/tmp/tmprBGJav/sel_RNG047+2.p_1',m__1329_01) ).
fof(27,conjecture,
( ( aVector0(sziznziztdt0(xs))
& szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)
& ! [X1] :
( aNaturalNumber0(X1)
=> sdtlbdtrb0(sziznziztdt0(xs),X1) = sdtlbdtrb0(xs,X1) ) )
=> ( ( aVector0(sziznziztdt0(xt))
& szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt)
& ! [X1] :
( aNaturalNumber0(X1)
=> sdtlbdtrb0(sziznziztdt0(xt),X1) = sdtlbdtrb0(xt,X1) ) )
=> aDimensionOf0(sziznziztdt0(xs)) = aDimensionOf0(sziznziztdt0(xt)) ) ),
file('/tmp/tmprBGJav/sel_RNG047+2.p_1',m__) ).
fof(36,negated_conjecture,
~ ( ( aVector0(sziznziztdt0(xs))
& szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)
& ! [X1] :
( aNaturalNumber0(X1)
=> sdtlbdtrb0(sziznziztdt0(xs),X1) = sdtlbdtrb0(xs,X1) ) )
=> ( ( aVector0(sziznziztdt0(xt))
& szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt)
& ! [X1] :
( aNaturalNumber0(X1)
=> sdtlbdtrb0(sziznziztdt0(xt),X1) = sdtlbdtrb0(xt,X1) ) )
=> aDimensionOf0(sziznziztdt0(xs)) = aDimensionOf0(sziznziztdt0(xt)) ) ),
inference(assume_negation,[status(cth)],[27]) ).
fof(95,plain,
! [X1,X2] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| szszuzczcdt0(X1) != szszuzczcdt0(X2)
| X1 = X2 ),
inference(fof_nnf,[status(thm)],[17]) ).
fof(96,plain,
! [X3,X4] :
( ~ aNaturalNumber0(X3)
| ~ aNaturalNumber0(X4)
| szszuzczcdt0(X3) != szszuzczcdt0(X4)
| X3 = X4 ),
inference(variable_rename,[status(thm)],[95]) ).
cnf(97,plain,
( X1 = X2
| szszuzczcdt0(X1) != szszuzczcdt0(X2)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1) ),
inference(split_conjunct,[status(thm)],[96]) ).
fof(116,plain,
! [X1] :
( ~ aVector0(X1)
| aNaturalNumber0(aDimensionOf0(X1)) ),
inference(fof_nnf,[status(thm)],[21]) ).
fof(117,plain,
! [X2] :
( ~ aVector0(X2)
| aNaturalNumber0(aDimensionOf0(X2)) ),
inference(variable_rename,[status(thm)],[116]) ).
cnf(118,plain,
( aNaturalNumber0(aDimensionOf0(X1))
| ~ aVector0(X1) ),
inference(split_conjunct,[status(thm)],[117]) ).
cnf(120,plain,
aDimensionOf0(xs) = aDimensionOf0(xt),
inference(split_conjunct,[status(thm)],[22]) ).
fof(137,negated_conjecture,
( aVector0(sziznziztdt0(xs))
& szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)
& ! [X1] :
( ~ aNaturalNumber0(X1)
| sdtlbdtrb0(sziznziztdt0(xs),X1) = sdtlbdtrb0(xs,X1) )
& aVector0(sziznziztdt0(xt))
& szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt)
& ! [X1] :
( ~ aNaturalNumber0(X1)
| sdtlbdtrb0(sziznziztdt0(xt),X1) = sdtlbdtrb0(xt,X1) )
& aDimensionOf0(sziznziztdt0(xs)) != aDimensionOf0(sziznziztdt0(xt)) ),
inference(fof_nnf,[status(thm)],[36]) ).
fof(138,negated_conjecture,
( aVector0(sziznziztdt0(xs))
& szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs)
& ! [X2] :
( ~ aNaturalNumber0(X2)
| sdtlbdtrb0(sziznziztdt0(xs),X2) = sdtlbdtrb0(xs,X2) )
& aVector0(sziznziztdt0(xt))
& szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt)
& ! [X3] :
( ~ aNaturalNumber0(X3)
| sdtlbdtrb0(sziznziztdt0(xt),X3) = sdtlbdtrb0(xt,X3) )
& aDimensionOf0(sziznziztdt0(xs)) != aDimensionOf0(sziznziztdt0(xt)) ),
inference(variable_rename,[status(thm)],[137]) ).
fof(139,negated_conjecture,
! [X2,X3] :
( ( ~ aNaturalNumber0(X3)
| sdtlbdtrb0(sziznziztdt0(xt),X3) = sdtlbdtrb0(xt,X3) )
& aVector0(sziznziztdt0(xt))
& szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt)
& aDimensionOf0(sziznziztdt0(xs)) != aDimensionOf0(sziznziztdt0(xt))
& ( ~ aNaturalNumber0(X2)
| sdtlbdtrb0(sziznziztdt0(xs),X2) = sdtlbdtrb0(xs,X2) )
& aVector0(sziznziztdt0(xs))
& szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs) ),
inference(shift_quantors,[status(thm)],[138]) ).
cnf(140,negated_conjecture,
szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xs),
inference(split_conjunct,[status(thm)],[139]) ).
cnf(141,negated_conjecture,
aVector0(sziznziztdt0(xs)),
inference(split_conjunct,[status(thm)],[139]) ).
cnf(143,negated_conjecture,
aDimensionOf0(sziznziztdt0(xs)) != aDimensionOf0(sziznziztdt0(xt)),
inference(split_conjunct,[status(thm)],[139]) ).
cnf(144,negated_conjecture,
szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt))) = aDimensionOf0(xt),
inference(split_conjunct,[status(thm)],[139]) ).
cnf(145,negated_conjecture,
aVector0(sziznziztdt0(xt)),
inference(split_conjunct,[status(thm)],[139]) ).
cnf(176,negated_conjecture,
szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs))) = aDimensionOf0(xt),
inference(rw,[status(thm)],[140,120,theory(equality)]) ).
cnf(197,negated_conjecture,
( aDimensionOf0(sziznziztdt0(xs)) = X1
| aDimensionOf0(xt) != szszuzczcdt0(X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(aDimensionOf0(sziznziztdt0(xs))) ),
inference(spm,[status(thm)],[97,176,theory(equality)]) ).
cnf(674,negated_conjecture,
( aDimensionOf0(sziznziztdt0(xs)) = X1
| szszuzczcdt0(X1) != aDimensionOf0(xt)
| ~ aNaturalNumber0(X1)
| ~ aVector0(sziznziztdt0(xs)) ),
inference(spm,[status(thm)],[197,118,theory(equality)]) ).
cnf(675,negated_conjecture,
( aDimensionOf0(sziznziztdt0(xs)) = X1
| szszuzczcdt0(X1) != aDimensionOf0(xt)
| ~ aNaturalNumber0(X1)
| $false ),
inference(rw,[status(thm)],[674,141,theory(equality)]) ).
cnf(676,negated_conjecture,
( aDimensionOf0(sziznziztdt0(xs)) = X1
| szszuzczcdt0(X1) != aDimensionOf0(xt)
| ~ aNaturalNumber0(X1) ),
inference(cn,[status(thm)],[675,theory(equality)]) ).
cnf(677,negated_conjecture,
( aDimensionOf0(sziznziztdt0(xs)) = aDimensionOf0(sziznziztdt0(xt))
| ~ aNaturalNumber0(aDimensionOf0(sziznziztdt0(xt))) ),
inference(spm,[status(thm)],[676,144,theory(equality)]) ).
cnf(680,negated_conjecture,
~ aNaturalNumber0(aDimensionOf0(sziznziztdt0(xt))),
inference(sr,[status(thm)],[677,143,theory(equality)]) ).
cnf(681,negated_conjecture,
~ aVector0(sziznziztdt0(xt)),
inference(spm,[status(thm)],[680,118,theory(equality)]) ).
cnf(682,negated_conjecture,
$false,
inference(rw,[status(thm)],[681,145,theory(equality)]) ).
cnf(683,negated_conjecture,
$false,
inference(cn,[status(thm)],[682,theory(equality)]) ).
cnf(684,negated_conjecture,
$false,
683,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/RNG/RNG047+2.p
% --creating new selector for []
% -running prover on /tmp/tmprBGJav/sel_RNG047+2.p_1 with time limit 29
% -prover status Theorem
% Problem RNG047+2.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/RNG/RNG047+2.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/RNG/RNG047+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
%
%------------------------------------------------------------------------------