%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : GEO271+1 : TPTP v5.0.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art09.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:13:06 EST 2010
% Result : Theorem 1.62s
% Output : CNFRefutation 1.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 7
% Syntax : Number of formulae : 56 ( 14 unt; 0 def)
% Number of atoms : 264 ( 70 equ)
% Maximal formula atoms : 16 ( 4 avg)
% Number of connectives : 383 ( 175 ~; 166 |; 35 &)
% ( 3 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 3 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-2 aty)
% Number of variables : 117 ( 0 sgn 54 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(24,axiom,
! [X200,X201,X202,X203,X204] :
( ( vf(X202,X200) = vf(X202,X201)
& ron(X201,X204)
& ron(X200,X203)
& rcenter(X202,X204)
& rcenter(X202,X203)
& ? [X205] :
( X201 = X205
& rpoint(X205) )
& ? [X206] :
( X200 = X206
& rpoint(X206) ) )
=> X203 = X204 ),
file('/tmp/tmp6UZWA9/sel_GEO271+1.p_1','qu(cond(axiom(182), 0), imp(cond(axiom(182), 0)))') ).
fof(55,conjecture,
! [X410] :
( ( ron(vd1057,X410)
& rcenter(vd1055,X410)
& rcircle(X410) )
=> X410 = vd1061 ),
file('/tmp/tmp6UZWA9/sel_GEO271+1.p_1','qu(theu(the(211), 1), imp(the(211)))') ).
fof(71,axiom,
( ron(vd1057,vd1061)
& rcenter(vd1055,vd1061)
& rcircle(vd1061) ),
file('/tmp/tmp6UZWA9/sel_GEO271+1.p_1','and(pred(comma_conjunct2(the(211)), 0), and(pred(comma_conjunct1(the(211)), 0), pred(the(211), 0)))') ).
fof(94,axiom,
( vd1057 = vd1058
& vd1055 != vd1057
& rpoint(vd1058)
& vd1055 = vd1056
& rpoint(vd1056) ),
file('/tmp/tmp6UZWA9/sel_GEO271+1.p_1','and(pred(conjunct2(210), 4), and(holds(conjunct2(210), 1059, 0), and(pred(conjunct2(210), 1), and(pred(conjunct1(210), 2), pred(conjunct1(210), 1)))))') ).
fof(103,axiom,
! [X717,X718,X719,X720,X721,X722] :
( ( ron(X721,X720)
& X721 = X722
& rpoint(X722)
& rcenter(X719,X720)
& X717 = X718
& rpoint(X718) )
=> ( vf(X719,X717) = vf(X719,X721)
<=> ron(X717,X720) ) ),
file('/tmp/tmp6UZWA9/sel_GEO271+1.p_1','qu(cond(axiom(184), 0), imp(cond(axiom(184), 0)))') ).
fof(105,negated_conjecture,
~ ! [X410] :
( ( ron(vd1057,X410)
& rcenter(vd1055,X410)
& rcircle(X410) )
=> X410 = vd1061 ),
inference(assume_negation,[status(cth)],[55]) ).
fof(303,plain,
! [X200,X201,X202,X203,X204] :
( vf(X202,X200) != vf(X202,X201)
| ~ ron(X201,X204)
| ~ ron(X200,X203)
| ~ rcenter(X202,X204)
| ~ rcenter(X202,X203)
| ! [X205] :
( X201 != X205
| ~ rpoint(X205) )
| ! [X206] :
( X200 != X206
| ~ rpoint(X206) )
| X203 = X204 ),
inference(fof_nnf,[status(thm)],[24]) ).
fof(304,plain,
! [X207,X208,X209,X210,X211] :
( vf(X209,X207) != vf(X209,X208)
| ~ ron(X208,X211)
| ~ ron(X207,X210)
| ~ rcenter(X209,X211)
| ~ rcenter(X209,X210)
| ! [X212] :
( X208 != X212
| ~ rpoint(X212) )
| ! [X213] :
( X207 != X213
| ~ rpoint(X213) )
| X210 = X211 ),
inference(variable_rename,[status(thm)],[303]) ).
fof(305,plain,
! [X207,X208,X209,X210,X211,X212,X213] :
( X207 != X213
| ~ rpoint(X213)
| X208 != X212
| ~ rpoint(X212)
| vf(X209,X207) != vf(X209,X208)
| ~ ron(X208,X211)
| ~ ron(X207,X210)
| ~ rcenter(X209,X211)
| ~ rcenter(X209,X210)
| X210 = X211 ),
inference(shift_quantors,[status(thm)],[304]) ).
cnf(306,plain,
( X1 = X2
| ~ rcenter(X3,X1)
| ~ rcenter(X3,X2)
| ~ ron(X4,X1)
| ~ ron(X5,X2)
| vf(X3,X4) != vf(X3,X5)
| ~ rpoint(X6)
| X5 != X6
| ~ rpoint(X7)
| X4 != X7 ),
inference(split_conjunct,[status(thm)],[305]) ).
fof(473,negated_conjecture,
? [X410] :
( ron(vd1057,X410)
& rcenter(vd1055,X410)
& rcircle(X410)
& X410 != vd1061 ),
inference(fof_nnf,[status(thm)],[105]) ).
fof(474,negated_conjecture,
? [X411] :
( ron(vd1057,X411)
& rcenter(vd1055,X411)
& rcircle(X411)
& X411 != vd1061 ),
inference(variable_rename,[status(thm)],[473]) ).
fof(475,negated_conjecture,
( ron(vd1057,esk29_0)
& rcenter(vd1055,esk29_0)
& rcircle(esk29_0)
& esk29_0 != vd1061 ),
inference(skolemize,[status(esa)],[474]) ).
cnf(476,negated_conjecture,
esk29_0 != vd1061,
inference(split_conjunct,[status(thm)],[475]) ).
cnf(478,negated_conjecture,
rcenter(vd1055,esk29_0),
inference(split_conjunct,[status(thm)],[475]) ).
cnf(479,negated_conjecture,
ron(vd1057,esk29_0),
inference(split_conjunct,[status(thm)],[475]) ).
cnf(572,plain,
rcenter(vd1055,vd1061),
inference(split_conjunct,[status(thm)],[71]) ).
cnf(573,plain,
ron(vd1057,vd1061),
inference(split_conjunct,[status(thm)],[71]) ).
cnf(698,plain,
rpoint(vd1058),
inference(split_conjunct,[status(thm)],[94]) ).
cnf(700,plain,
vd1057 = vd1058,
inference(split_conjunct,[status(thm)],[94]) ).
fof(742,plain,
! [X717,X718,X719,X720,X721,X722] :
( ~ ron(X721,X720)
| X721 != X722
| ~ rpoint(X722)
| ~ rcenter(X719,X720)
| X717 != X718
| ~ rpoint(X718)
| ( ( vf(X719,X717) != vf(X719,X721)
| ron(X717,X720) )
& ( ~ ron(X717,X720)
| vf(X719,X717) = vf(X719,X721) ) ) ),
inference(fof_nnf,[status(thm)],[103]) ).
fof(743,plain,
! [X723,X724,X725,X726,X727,X728] :
( ~ ron(X727,X726)
| X727 != X728
| ~ rpoint(X728)
| ~ rcenter(X725,X726)
| X723 != X724
| ~ rpoint(X724)
| ( ( vf(X725,X723) != vf(X725,X727)
| ron(X723,X726) )
& ( ~ ron(X723,X726)
| vf(X725,X723) = vf(X725,X727) ) ) ),
inference(variable_rename,[status(thm)],[742]) ).
fof(744,plain,
! [X723,X724,X725,X726,X727,X728] :
( ( vf(X725,X723) != vf(X725,X727)
| ron(X723,X726)
| ~ ron(X727,X726)
| X727 != X728
| ~ rpoint(X728)
| ~ rcenter(X725,X726)
| X723 != X724
| ~ rpoint(X724) )
& ( ~ ron(X723,X726)
| vf(X725,X723) = vf(X725,X727)
| ~ ron(X727,X726)
| X727 != X728
| ~ rpoint(X728)
| ~ rcenter(X725,X726)
| X723 != X724
| ~ rpoint(X724) ) ),
inference(distribute,[status(thm)],[743]) ).
cnf(745,plain,
( vf(X3,X2) = vf(X3,X6)
| ~ rpoint(X1)
| X2 != X1
| ~ rcenter(X3,X4)
| ~ rpoint(X5)
| X6 != X5
| ~ ron(X6,X4)
| ~ ron(X2,X4) ),
inference(split_conjunct,[status(thm)],[744]) ).
cnf(754,plain,
rpoint(vd1057),
inference(rw,[status(thm)],[698,700,theory(equality)]) ).
cnf(922,plain,
( vf(X1,X2) = vf(X1,X3)
| X4 != X2
| ~ rcenter(X1,X5)
| ~ rpoint(X3)
| ~ rpoint(X4)
| ~ ron(X3,X5)
| ~ ron(X2,X5) ),
inference(er,[status(thm)],[745,theory(equality)]) ).
cnf(923,plain,
( vf(X1,X2) = vf(X1,X3)
| ~ rcenter(X1,X4)
| ~ rpoint(X3)
| ~ rpoint(X2)
| ~ ron(X3,X4)
| ~ ron(X2,X4) ),
inference(er,[status(thm)],[922,theory(equality)]) ).
cnf(1018,plain,
( X1 = X2
| vf(X3,X4) != vf(X3,X5)
| X4 != X6
| ~ rcenter(X3,X2)
| ~ rcenter(X3,X1)
| ~ rpoint(X6)
| ~ rpoint(X5)
| ~ ron(X5,X2)
| ~ ron(X4,X1) ),
inference(er,[status(thm)],[306,theory(equality)]) ).
cnf(1019,plain,
( X1 = X2
| vf(X3,X4) != vf(X3,X5)
| ~ rcenter(X3,X2)
| ~ rcenter(X3,X1)
| ~ rpoint(X4)
| ~ rpoint(X5)
| ~ ron(X5,X2)
| ~ ron(X4,X1) ),
inference(er,[status(thm)],[1018,theory(equality)]) ).
cnf(2143,plain,
( vf(vd1055,X1) = vf(vd1055,X2)
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ ron(X2,vd1061)
| ~ ron(X1,vd1061) ),
inference(spm,[status(thm)],[923,572,theory(equality)]) ).
cnf(2144,negated_conjecture,
( vf(vd1055,X1) = vf(vd1055,X2)
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ ron(X2,esk29_0)
| ~ ron(X1,esk29_0) ),
inference(spm,[status(thm)],[923,478,theory(equality)]) ).
cnf(2404,negated_conjecture,
( vf(vd1055,X3) = vf(vd1055,X2)
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ ron(X2,vd1061)
| ~ ron(X1,vd1061)
| ~ rpoint(X3)
| ~ ron(X3,esk29_0)
| ~ ron(X1,esk29_0) ),
inference(spm,[status(thm)],[2143,2144,theory(equality)]) ).
cnf(2944,plain,
( X1 = vd1061
| vf(vd1055,X2) != vf(vd1055,X3)
| ~ rcenter(vd1055,X1)
| ~ rpoint(X2)
| ~ rpoint(X3)
| ~ ron(X3,vd1061)
| ~ ron(X2,X1) ),
inference(spm,[status(thm)],[1019,572,theory(equality)]) ).
cnf(9665,negated_conjecture,
( vf(vd1055,X1) = vf(vd1055,X2)
| ~ rpoint(X2)
| ~ rpoint(vd1057)
| ~ rpoint(X1)
| ~ ron(X2,vd1061)
| ~ ron(vd1057,vd1061)
| ~ ron(X1,esk29_0) ),
inference(spm,[status(thm)],[2404,479,theory(equality)]) ).
cnf(9697,negated_conjecture,
( vf(vd1055,X1) = vf(vd1055,X2)
| ~ rpoint(X2)
| $false
| ~ rpoint(X1)
| ~ ron(X2,vd1061)
| ~ ron(vd1057,vd1061)
| ~ ron(X1,esk29_0) ),
inference(rw,[status(thm)],[9665,754,theory(equality)]) ).
cnf(9698,negated_conjecture,
( vf(vd1055,X1) = vf(vd1055,X2)
| ~ rpoint(X2)
| $false
| ~ rpoint(X1)
| ~ ron(X2,vd1061)
| $false
| ~ ron(X1,esk29_0) ),
inference(rw,[status(thm)],[9697,573,theory(equality)]) ).
cnf(9699,negated_conjecture,
( vf(vd1055,X1) = vf(vd1055,X2)
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ ron(X2,vd1061)
| ~ ron(X1,esk29_0) ),
inference(cn,[status(thm)],[9698,theory(equality)]) ).
cnf(15833,negated_conjecture,
( esk29_0 = vd1061
| vf(vd1055,X1) != vf(vd1055,X2)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ ron(X2,vd1061)
| ~ ron(X1,esk29_0) ),
inference(spm,[status(thm)],[2944,478,theory(equality)]) ).
cnf(15835,negated_conjecture,
( vf(vd1055,X1) != vf(vd1055,X2)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ ron(X2,vd1061)
| ~ ron(X1,esk29_0) ),
inference(sr,[status(thm)],[15833,476,theory(equality)]) ).
cnf(15838,negated_conjecture,
( ~ rpoint(X1)
| ~ rpoint(X2)
| ~ ron(X2,vd1061)
| ~ ron(X1,esk29_0) ),
inference(csr,[status(thm)],[15835,9699]) ).
fof(15839,plain,
( ~ epred3_0
<=> ! [X1] :
( ~ ron(X1,esk29_0)
| ~ rpoint(X1) ) ),
introduced(definition),
[split] ).
cnf(15840,plain,
( epred3_0
| ~ ron(X1,esk29_0)
| ~ rpoint(X1) ),
inference(split_equiv,[status(thm)],[15839]) ).
fof(15841,plain,
( ~ epred4_0
<=> ! [X2] :
( ~ ron(X2,vd1061)
| ~ rpoint(X2) ) ),
introduced(definition),
[split] ).
cnf(15842,plain,
( epred4_0
| ~ ron(X2,vd1061)
| ~ rpoint(X2) ),
inference(split_equiv,[status(thm)],[15841]) ).
cnf(15843,negated_conjecture,
( ~ epred4_0
| ~ epred3_0 ),
inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[15838,15839,theory(equality)]),15841,theory(equality)]),
[split] ).
cnf(15844,negated_conjecture,
( epred3_0
| ~ rpoint(vd1057) ),
inference(spm,[status(thm)],[15840,479,theory(equality)]) ).
cnf(15876,negated_conjecture,
( epred3_0
| $false ),
inference(rw,[status(thm)],[15844,754,theory(equality)]) ).
cnf(15877,negated_conjecture,
epred3_0,
inference(cn,[status(thm)],[15876,theory(equality)]) ).
cnf(15907,negated_conjecture,
( ~ epred4_0
| $false ),
inference(rw,[status(thm)],[15843,15877,theory(equality)]) ).
cnf(15908,negated_conjecture,
~ epred4_0,
inference(cn,[status(thm)],[15907,theory(equality)]) ).
cnf(15909,negated_conjecture,
( epred4_0
| ~ rpoint(vd1057) ),
inference(spm,[status(thm)],[15842,573,theory(equality)]) ).
cnf(15941,negated_conjecture,
( epred4_0
| $false ),
inference(rw,[status(thm)],[15909,754,theory(equality)]) ).
cnf(15942,negated_conjecture,
epred4_0,
inference(cn,[status(thm)],[15941,theory(equality)]) ).
cnf(15973,negated_conjecture,
$false,
inference(rw,[status(thm)],[15908,15942,theory(equality)]) ).
cnf(15974,negated_conjecture,
$false,
inference(cn,[status(thm)],[15973,theory(equality)]) ).
cnf(15975,negated_conjecture,
$false,
15974,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/GEO/GEO271+1.p
% --creating new selector for []
% -running prover on /tmp/tmp6UZWA9/sel_GEO271+1.p_1 with time limit 29
% -prover status Theorem
% Problem GEO271+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/GEO/GEO271+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/GEO/GEO271+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
%
%------------------------------------------------------------------------------