%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : GEO342+1 : TPTP v5.0.0. Released v4.1.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 : Sat Dec 25 09:46:36 EST 2010
% Result : Theorem 0.56s
% Output : CNFRefutation 0.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 3
% Syntax : Number of formulae : 40 ( 10 unt; 0 def)
% Number of atoms : 192 ( 74 equ)
% Maximal formula atoms : 18 ( 4 avg)
% Number of connectives : 242 ( 90 ~; 95 |; 56 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 8 con; 0-2 aty)
% Number of variables : 70 ( 0 sgn 24 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(33,axiom,
! [X276,X277] :
( ( X276 != X277
& ? [X278] :
( X277 = X278
& rpoint(X278) )
& ? [X279] :
( X276 = X279
& rpoint(X279) ) )
=> ? [X280] :
( ron(X277,X280)
& ron(X276,X280)
& rline(X280) ) ),
file('/tmp/tmpHFDdO-/sel_GEO342+1.p_1','qu(cond(axiom(51), 0), imp(cond(axiom(51), 0)))') ).
fof(39,axiom,
( vd1406 = vd1407
& ron(vd1400,vd1406)
& ron(vd1399,vd1406)
& rline(vd1407)
& vd1400 != vd1401
& vd1399 != vd1401
& vd1399 != vd1400
& ? [X316] :
( vd1401 = X316
& rpoint(X316) )
& ? [X317] :
( vd1400 = X317
& rpoint(X317) )
& ? [X318] :
( vd1399 = X318
& rpoint(X318) ) ),
file('/tmp/tmpHFDdO-/sel_GEO342+1.p_1','and(pred(conjunct2(405), 5), and(pred(s2(plural(conjunct2(405))), 0), and(pred(s1(plural(conjunct2(405))), 0), and(pred(conjunct2(405), 1), and(pred(conjunct1(405), 9), and(pred(conjunct1(405), 8), and(pred(conjunct1(405), 7), and(qe(s3(plural(405))), and(qe(s2(plural(405))), qe(s1(plural(405))))))))))))') ).
fof(57,conjecture,
? [X425] :
( ron(vd1399,X425)
& ron(vd1401,X425)
& rline(X425) ),
file('/tmp/tmpHFDdO-/sel_GEO342+1.p_1','qe(thee(the(408), 1))') ).
fof(116,negated_conjecture,
~ ? [X425] :
( ron(vd1399,X425)
& ron(vd1401,X425)
& rline(X425) ),
inference(assume_negation,[status(cth)],[57]) ).
fof(371,plain,
! [X276,X277] :
( X276 = X277
| ! [X278] :
( X277 != X278
| ~ rpoint(X278) )
| ! [X279] :
( X276 != X279
| ~ rpoint(X279) )
| ? [X280] :
( ron(X277,X280)
& ron(X276,X280)
& rline(X280) ) ),
inference(fof_nnf,[status(thm)],[33]) ).
fof(372,plain,
! [X281,X282] :
( X281 = X282
| ! [X283] :
( X282 != X283
| ~ rpoint(X283) )
| ! [X284] :
( X281 != X284
| ~ rpoint(X284) )
| ? [X285] :
( ron(X282,X285)
& ron(X281,X285)
& rline(X285) ) ),
inference(variable_rename,[status(thm)],[371]) ).
fof(373,plain,
! [X281,X282] :
( X281 = X282
| ! [X283] :
( X282 != X283
| ~ rpoint(X283) )
| ! [X284] :
( X281 != X284
| ~ rpoint(X284) )
| ( ron(X282,esk20_2(X281,X282))
& ron(X281,esk20_2(X281,X282))
& rline(esk20_2(X281,X282)) ) ),
inference(skolemize,[status(esa)],[372]) ).
fof(374,plain,
! [X281,X282,X283,X284] :
( X281 != X284
| ~ rpoint(X284)
| X282 != X283
| ~ rpoint(X283)
| X281 = X282
| ( ron(X282,esk20_2(X281,X282))
& ron(X281,esk20_2(X281,X282))
& rline(esk20_2(X281,X282)) ) ),
inference(shift_quantors,[status(thm)],[373]) ).
fof(375,plain,
! [X281,X282,X283,X284] :
( ( ron(X282,esk20_2(X281,X282))
| X281 != X284
| ~ rpoint(X284)
| X282 != X283
| ~ rpoint(X283)
| X281 = X282 )
& ( ron(X281,esk20_2(X281,X282))
| X281 != X284
| ~ rpoint(X284)
| X282 != X283
| ~ rpoint(X283)
| X281 = X282 )
& ( rline(esk20_2(X281,X282))
| X281 != X284
| ~ rpoint(X284)
| X282 != X283
| ~ rpoint(X283)
| X281 = X282 ) ),
inference(distribute,[status(thm)],[374]) ).
cnf(376,plain,
( X1 = X2
| rline(esk20_2(X1,X2))
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X4)
| X1 != X4 ),
inference(split_conjunct,[status(thm)],[375]) ).
cnf(377,plain,
( X1 = X2
| ron(X1,esk20_2(X1,X2))
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X4)
| X1 != X4 ),
inference(split_conjunct,[status(thm)],[375]) ).
cnf(378,plain,
( X1 = X2
| ron(X2,esk20_2(X1,X2))
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X4)
| X1 != X4 ),
inference(split_conjunct,[status(thm)],[375]) ).
fof(401,plain,
( vd1406 = vd1407
& ron(vd1400,vd1406)
& ron(vd1399,vd1406)
& rline(vd1407)
& vd1400 != vd1401
& vd1399 != vd1401
& vd1399 != vd1400
& ? [X319] :
( vd1401 = X319
& rpoint(X319) )
& ? [X320] :
( vd1400 = X320
& rpoint(X320) )
& ? [X321] :
( vd1399 = X321
& rpoint(X321) ) ),
inference(variable_rename,[status(thm)],[39]) ).
fof(402,plain,
( vd1406 = vd1407
& ron(vd1400,vd1406)
& ron(vd1399,vd1406)
& rline(vd1407)
& vd1400 != vd1401
& vd1399 != vd1401
& vd1399 != vd1400
& vd1401 = esk22_0
& rpoint(esk22_0)
& vd1400 = esk23_0
& rpoint(esk23_0)
& vd1399 = esk24_0
& rpoint(esk24_0) ),
inference(skolemize,[status(esa)],[401]) ).
cnf(403,plain,
rpoint(esk24_0),
inference(split_conjunct,[status(thm)],[402]) ).
cnf(404,plain,
vd1399 = esk24_0,
inference(split_conjunct,[status(thm)],[402]) ).
cnf(407,plain,
rpoint(esk22_0),
inference(split_conjunct,[status(thm)],[402]) ).
cnf(408,plain,
vd1401 = esk22_0,
inference(split_conjunct,[status(thm)],[402]) ).
cnf(410,plain,
vd1399 != vd1401,
inference(split_conjunct,[status(thm)],[402]) ).
fof(498,negated_conjecture,
! [X425] :
( ~ ron(vd1399,X425)
| ~ ron(vd1401,X425)
| ~ rline(X425) ),
inference(fof_nnf,[status(thm)],[116]) ).
fof(499,negated_conjecture,
! [X426] :
( ~ ron(vd1399,X426)
| ~ ron(vd1401,X426)
| ~ rline(X426) ),
inference(variable_rename,[status(thm)],[498]) ).
cnf(500,negated_conjecture,
( ~ rline(X1)
| ~ ron(vd1401,X1)
| ~ ron(vd1399,X1) ),
inference(split_conjunct,[status(thm)],[499]) ).
cnf(802,plain,
rpoint(vd1401),
inference(rw,[status(thm)],[407,408,theory(equality)]) ).
cnf(804,plain,
rpoint(vd1399),
inference(rw,[status(thm)],[403,404,theory(equality)]) ).
cnf(841,plain,
( X1 = X2
| rline(esk20_2(X1,X2))
| X1 != X3
| ~ rpoint(X3)
| ~ rpoint(X2) ),
inference(er,[status(thm)],[376,theory(equality)]) ).
cnf(842,plain,
( X1 = X2
| rline(esk20_2(X1,X2))
| ~ rpoint(X1)
| ~ rpoint(X2) ),
inference(er,[status(thm)],[841,theory(equality)]) ).
cnf(856,plain,
( X1 = X2
| ron(X2,esk20_2(X1,X2))
| X1 != X3
| ~ rpoint(X3)
| ~ rpoint(X2) ),
inference(er,[status(thm)],[378,theory(equality)]) ).
cnf(857,plain,
( X1 = X2
| ron(X2,esk20_2(X1,X2))
| ~ rpoint(X1)
| ~ rpoint(X2) ),
inference(er,[status(thm)],[856,theory(equality)]) ).
cnf(858,plain,
( X1 = X2
| ron(X1,esk20_2(X1,X2))
| X1 != X3
| ~ rpoint(X3)
| ~ rpoint(X2) ),
inference(er,[status(thm)],[377,theory(equality)]) ).
cnf(859,plain,
( X1 = X2
| ron(X1,esk20_2(X1,X2))
| ~ rpoint(X1)
| ~ rpoint(X2) ),
inference(er,[status(thm)],[858,theory(equality)]) ).
cnf(1945,negated_conjecture,
( X1 = X2
| ~ ron(vd1399,esk20_2(X1,X2))
| ~ ron(vd1401,esk20_2(X1,X2))
| ~ rpoint(X1)
| ~ rpoint(X2) ),
inference(spm,[status(thm)],[500,842,theory(equality)]) ).
cnf(1973,negated_conjecture,
( X1 = vd1399
| ~ rpoint(X1)
| ~ rpoint(vd1399)
| ~ ron(vd1401,esk20_2(X1,vd1399)) ),
inference(spm,[status(thm)],[1945,857,theory(equality)]) ).
cnf(1974,negated_conjecture,
( X1 = vd1399
| ~ rpoint(X1)
| $false
| ~ ron(vd1401,esk20_2(X1,vd1399)) ),
inference(rw,[status(thm)],[1973,804,theory(equality)]) ).
cnf(1975,negated_conjecture,
( X1 = vd1399
| ~ rpoint(X1)
| ~ ron(vd1401,esk20_2(X1,vd1399)) ),
inference(cn,[status(thm)],[1974,theory(equality)]) ).
cnf(1994,negated_conjecture,
( vd1401 = vd1399
| ~ rpoint(vd1401)
| ~ rpoint(vd1399) ),
inference(spm,[status(thm)],[1975,859,theory(equality)]) ).
cnf(1997,negated_conjecture,
( vd1401 = vd1399
| $false
| ~ rpoint(vd1399) ),
inference(rw,[status(thm)],[1994,802,theory(equality)]) ).
cnf(1998,negated_conjecture,
( vd1401 = vd1399
| $false
| $false ),
inference(rw,[status(thm)],[1997,804,theory(equality)]) ).
cnf(1999,negated_conjecture,
vd1401 = vd1399,
inference(cn,[status(thm)],[1998,theory(equality)]) ).
cnf(2000,negated_conjecture,
$false,
inference(sr,[status(thm)],[1999,410,theory(equality)]) ).
cnf(2001,negated_conjecture,
$false,
2000,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/GEO/GEO342+1.p
% --creating new selector for []
% -running prover on /tmp/tmpHFDdO-/sel_GEO342+1.p_1 with time limit 29
% -prover status Theorem
% Problem GEO342+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/GEO/GEO342+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/GEO/GEO342+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
%
%------------------------------------------------------------------------------