%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : GEO271+1 : TPTP v5.0.0. Released v4.1.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %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 : Wed Dec 29 05:26:45 EST 2010
% Result : Theorem 42.37s
% Output : Solution 42.37s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP18260/GEO271+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP18260/GEO271+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP18260/GEO271+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 18356
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% PrfWatch: 1.92 CPU 2.01 WC
% PrfWatch: 3.91 CPU 4.01 WC
% PrfWatch: 5.91 CPU 6.02 WC
% PrfWatch: 7.89 CPU 8.02 WC
% PrfWatch: 9.89 CPU 10.03 WC
% PrfWatch: 11.88 CPU 12.03 WC
% PrfWatch: 13.87 CPU 14.04 WC
% PrfWatch: 15.49 CPU 16.04 WC
% PrfWatch: 17.13 CPU 18.05 WC
% PrfWatch: 19.12 CPU 20.05 WC
% PrfWatch: 21.12 CPU 22.06 WC
% PrfWatch: 23.10 CPU 24.06 WC
% PrfWatch: 25.09 CPU 26.07 WC
% PrfWatch: 27.08 CPU 28.07 WC
% # Preprocessing time : 0.075 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 29.06 CPU 30.08 WC
% PrfWatch: 30.69 CPU 32.08 WC
% PrfWatch: 32.35 CPU 34.08 WC
% PrfWatch: 34.33 CPU 36.09 WC
% PrfWatch: 36.32 CPU 38.09 WC
% PrfWatch: 38.32 CPU 40.10 WC
% PrfWatch: 40.31 CPU 42.10 WC
% # SZS output start CNFRefutation.
% fof(1, axiom,((ron(vd1057,vd1061)&rcenter(vd1055,vd1061))&rcircle(vd1061)),file('/tmp/SRASS.s.p', 'and(pred(comma_conjunct2(the(211)), 0), and(pred(comma_conjunct1(the(211)), 0), pred(the(211), 0)))')).
% fof(3, axiom,![X5]:![X6]:(((~(X5=X6)&?[X7]:(X6=X7&rpoint(X7)))&?[X8]:(X5=X8&rpoint(X8)))=>?[X9]:((ron(X6,X9)&rcenter(X5,X9))&rcircle(X9))),file('/tmp/SRASS.s.p', 'qu(cond(axiom(53), 0), imp(cond(axiom(53), 0)))')).
% fof(6, axiom,![X21]:![X22]:![X23]:![X24]:(((((ron(X23,X21)&X23=X24)&rpoint(X24))&X21=X22)&rcircle(X22))=>?[X25]:((~(X25=X23)&ron(X25,X21))&rpoint(X25))),file('/tmp/SRASS.s.p', 'qu(cond(axiom(43), 0), imp(cond(axiom(43), 0)))')).
% fof(8, axiom,![X29]:![X30]:![X31]:![X32]:![X33]:![X34]:((((((ron(X33,X32)&X33=X34)&rpoint(X34))&rcenter(X31,X32))&X29=X30)&rpoint(X30))=>(vf(X31,X29)=vf(X31,X33)<=>ron(X29,X32))),file('/tmp/SRASS.s.p', 'qu(cond(axiom(184), 0), imp(cond(axiom(184), 0)))')).
% fof(9, axiom,![X35]:![X36]:![X37]:![X38]:![X39]:(((((((vf(X37,X35)=vf(X37,X36)&ron(X36,X39))&ron(X35,X38))&rcenter(X37,X39))&rcenter(X37,X38))&?[X40]:(X36=X40&rpoint(X40)))&?[X41]:(X35=X41&rpoint(X41)))=>X38=X39),file('/tmp/SRASS.s.p', 'qu(cond(axiom(182), 0), imp(cond(axiom(182), 0)))')).
% fof(11, axiom,![X46]:![X47]:(((rintersect(X46,X47)&?[X48]:(X47=X48&rcircle(X48)))&?[X49]:(X46=X49&rcircle(X49)))=>?[X50]:?[X51]:((((((~(X50=X51)&ron(X51,X47))&ron(X51,X46))&rpoint(X51))&ron(X50,X47))&ron(X50,X46))&rpoint(X50))),file('/tmp/SRASS.s.p', 'qu(cond(axiom(67), 0), imp(cond(axiom(67), 0)))')).
% fof(14, axiom,![X60]:![X61]:(rcenter(X60,X61)=>rinside(X60,X61)),file('/tmp/SRASS.s.p', 'qu(cond(axiom(77), 0), imp(cond(axiom(77), 0)))')).
% fof(15, axiom,![X62]:![X63]:((?[X64]:(X63=X64&rpoint(X64))&?[X65]:(X62=X65&rpoint(X65)))=>vf(X62,X63)=vf(X63,X62)),file('/tmp/SRASS.s.p', 'qu(cond(axiom(166), 0), imp(cond(axiom(166), 0)))')).
% fof(32, axiom,((((vd1057=vd1058&~(vd1055=vd1057))&rpoint(vd1058))&vd1055=vd1056)&rpoint(vd1056)),file('/tmp/SRASS.s.p', '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(61, axiom,![X403]:![X404]:![X405]:![X406]:((((((ron(X404,X406)&rinside(X403,X406))&rinside(X404,X405))&ron(X403,X405))&?[X407]:(X404=X407&rpoint(X407)))&?[X408]:(X403=X408&rpoint(X408)))=>rintersect(X405,X406)),file('/tmp/SRASS.s.p', 'qu(cond(axiom(135), 0), imp(cond(axiom(135), 0)))')).
% fof(105, conjecture,![X727]:(((ron(vd1057,X727)&rcenter(vd1055,X727))&rcircle(X727))=>X727=vd1061),file('/tmp/SRASS.s.p', 'qu(theu(the(211), 1), imp(the(211)))')).
% fof(106, negated_conjecture,~(![X727]:(((ron(vd1057,X727)&rcenter(vd1055,X727))&rcircle(X727))=>X727=vd1061)),inference(assume_negation,[status(cth)],[105])).
% cnf(138,plain,(rcircle(vd1061)),inference(split_conjunct,[status(thm)],[1])).
% cnf(139,plain,(rcenter(vd1055,vd1061)),inference(split_conjunct,[status(thm)],[1])).
% cnf(140,plain,(ron(vd1057,vd1061)),inference(split_conjunct,[status(thm)],[1])).
% fof(144, plain,![X5]:![X6]:(((X5=X6|![X7]:(~(X6=X7)|~(rpoint(X7))))|![X8]:(~(X5=X8)|~(rpoint(X8))))|?[X9]:((ron(X6,X9)&rcenter(X5,X9))&rcircle(X9))),inference(fof_nnf,[status(thm)],[3])).
% fof(145, plain,![X10]:![X11]:(((X10=X11|![X12]:(~(X11=X12)|~(rpoint(X12))))|![X13]:(~(X10=X13)|~(rpoint(X13))))|?[X14]:((ron(X11,X14)&rcenter(X10,X14))&rcircle(X14))),inference(variable_rename,[status(thm)],[144])).
% fof(146, plain,![X10]:![X11]:(((X10=X11|![X12]:(~(X11=X12)|~(rpoint(X12))))|![X13]:(~(X10=X13)|~(rpoint(X13))))|((ron(X11,esk1_2(X10,X11))&rcenter(X10,esk1_2(X10,X11)))&rcircle(esk1_2(X10,X11)))),inference(skolemize,[status(esa)],[145])).
% fof(147, plain,![X10]:![X11]:![X12]:![X13]:(((~(X10=X13)|~(rpoint(X13)))|((~(X11=X12)|~(rpoint(X12)))|X10=X11))|((ron(X11,esk1_2(X10,X11))&rcenter(X10,esk1_2(X10,X11)))&rcircle(esk1_2(X10,X11)))),inference(shift_quantors,[status(thm)],[146])).
% fof(148, plain,![X10]:![X11]:![X12]:![X13]:(((ron(X11,esk1_2(X10,X11))|((~(X10=X13)|~(rpoint(X13)))|((~(X11=X12)|~(rpoint(X12)))|X10=X11)))&(rcenter(X10,esk1_2(X10,X11))|((~(X10=X13)|~(rpoint(X13)))|((~(X11=X12)|~(rpoint(X12)))|X10=X11))))&(rcircle(esk1_2(X10,X11))|((~(X10=X13)|~(rpoint(X13)))|((~(X11=X12)|~(rpoint(X12)))|X10=X11)))),inference(distribute,[status(thm)],[147])).
% cnf(149,plain,(X1=X2|rcircle(esk1_2(X1,X2))|~rpoint(X3)|X2!=X3|~rpoint(X4)|X1!=X4),inference(split_conjunct,[status(thm)],[148])).
% cnf(150,plain,(X1=X2|rcenter(X1,esk1_2(X1,X2))|~rpoint(X3)|X2!=X3|~rpoint(X4)|X1!=X4),inference(split_conjunct,[status(thm)],[148])).
% cnf(151,plain,(X1=X2|ron(X2,esk1_2(X1,X2))|~rpoint(X3)|X2!=X3|~rpoint(X4)|X1!=X4),inference(split_conjunct,[status(thm)],[148])).
% fof(169, plain,![X21]:![X22]:![X23]:![X24]:(((((~(ron(X23,X21))|~(X23=X24))|~(rpoint(X24)))|~(X21=X22))|~(rcircle(X22)))|?[X25]:((~(X25=X23)&ron(X25,X21))&rpoint(X25))),inference(fof_nnf,[status(thm)],[6])).
% fof(170, plain,![X26]:![X27]:![X28]:![X29]:(((((~(ron(X28,X26))|~(X28=X29))|~(rpoint(X29)))|~(X26=X27))|~(rcircle(X27)))|?[X30]:((~(X30=X28)&ron(X30,X26))&rpoint(X30))),inference(variable_rename,[status(thm)],[169])).
% fof(171, plain,![X26]:![X27]:![X28]:![X29]:(((((~(ron(X28,X26))|~(X28=X29))|~(rpoint(X29)))|~(X26=X27))|~(rcircle(X27)))|((~(esk5_4(X26,X27,X28,X29)=X28)&ron(esk5_4(X26,X27,X28,X29),X26))&rpoint(esk5_4(X26,X27,X28,X29)))),inference(skolemize,[status(esa)],[170])).
% fof(172, plain,![X26]:![X27]:![X28]:![X29]:(((~(esk5_4(X26,X27,X28,X29)=X28)|((((~(ron(X28,X26))|~(X28=X29))|~(rpoint(X29)))|~(X26=X27))|~(rcircle(X27))))&(ron(esk5_4(X26,X27,X28,X29),X26)|((((~(ron(X28,X26))|~(X28=X29))|~(rpoint(X29)))|~(X26=X27))|~(rcircle(X27)))))&(rpoint(esk5_4(X26,X27,X28,X29))|((((~(ron(X28,X26))|~(X28=X29))|~(rpoint(X29)))|~(X26=X27))|~(rcircle(X27))))),inference(distribute,[status(thm)],[171])).
% cnf(173,plain,(rpoint(esk5_4(X2,X1,X4,X3))|~rcircle(X1)|X2!=X1|~rpoint(X3)|X4!=X3|~ron(X4,X2)),inference(split_conjunct,[status(thm)],[172])).
% cnf(174,plain,(ron(esk5_4(X2,X1,X4,X3),X2)|~rcircle(X1)|X2!=X1|~rpoint(X3)|X4!=X3|~ron(X4,X2)),inference(split_conjunct,[status(thm)],[172])).
% fof(182, plain,![X29]:![X30]:![X31]:![X32]:![X33]:![X34]:((((((~(ron(X33,X32))|~(X33=X34))|~(rpoint(X34)))|~(rcenter(X31,X32)))|~(X29=X30))|~(rpoint(X30)))|((~(vf(X31,X29)=vf(X31,X33))|ron(X29,X32))&(~(ron(X29,X32))|vf(X31,X29)=vf(X31,X33)))),inference(fof_nnf,[status(thm)],[8])).
% fof(183, plain,![X35]:![X36]:![X37]:![X38]:![X39]:![X40]:((((((~(ron(X39,X38))|~(X39=X40))|~(rpoint(X40)))|~(rcenter(X37,X38)))|~(X35=X36))|~(rpoint(X36)))|((~(vf(X37,X35)=vf(X37,X39))|ron(X35,X38))&(~(ron(X35,X38))|vf(X37,X35)=vf(X37,X39)))),inference(variable_rename,[status(thm)],[182])).
% fof(184, plain,![X35]:![X36]:![X37]:![X38]:![X39]:![X40]:(((~(vf(X37,X35)=vf(X37,X39))|ron(X35,X38))|(((((~(ron(X39,X38))|~(X39=X40))|~(rpoint(X40)))|~(rcenter(X37,X38)))|~(X35=X36))|~(rpoint(X36))))&((~(ron(X35,X38))|vf(X37,X35)=vf(X37,X39))|(((((~(ron(X39,X38))|~(X39=X40))|~(rpoint(X40)))|~(rcenter(X37,X38)))|~(X35=X36))|~(rpoint(X36))))),inference(distribute,[status(thm)],[183])).
% cnf(185,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)],[184])).
% cnf(186,plain,(ron(X2,X4)|~rpoint(X1)|X2!=X1|~rcenter(X3,X4)|~rpoint(X5)|X6!=X5|~ron(X6,X4)|vf(X3,X2)!=vf(X3,X6)),inference(split_conjunct,[status(thm)],[184])).
% fof(187, plain,![X35]:![X36]:![X37]:![X38]:![X39]:(((((((~(vf(X37,X35)=vf(X37,X36))|~(ron(X36,X39)))|~(ron(X35,X38)))|~(rcenter(X37,X39)))|~(rcenter(X37,X38)))|![X40]:(~(X36=X40)|~(rpoint(X40))))|![X41]:(~(X35=X41)|~(rpoint(X41))))|X38=X39),inference(fof_nnf,[status(thm)],[9])).
% fof(188, plain,![X42]:![X43]:![X44]:![X45]:![X46]:(((((((~(vf(X44,X42)=vf(X44,X43))|~(ron(X43,X46)))|~(ron(X42,X45)))|~(rcenter(X44,X46)))|~(rcenter(X44,X45)))|![X47]:(~(X43=X47)|~(rpoint(X47))))|![X48]:(~(X42=X48)|~(rpoint(X48))))|X45=X46),inference(variable_rename,[status(thm)],[187])).
% fof(189, plain,![X42]:![X43]:![X44]:![X45]:![X46]:![X47]:![X48]:(((~(X42=X48)|~(rpoint(X48)))|((~(X43=X47)|~(rpoint(X47)))|((((~(vf(X44,X42)=vf(X44,X43))|~(ron(X43,X46)))|~(ron(X42,X45)))|~(rcenter(X44,X46)))|~(rcenter(X44,X45)))))|X45=X46),inference(shift_quantors,[status(thm)],[188])).
% cnf(190,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)],[189])).
% fof(194, plain,![X46]:![X47]:(((~(rintersect(X46,X47))|![X48]:(~(X47=X48)|~(rcircle(X48))))|![X49]:(~(X46=X49)|~(rcircle(X49))))|?[X50]:?[X51]:((((((~(X50=X51)&ron(X51,X47))&ron(X51,X46))&rpoint(X51))&ron(X50,X47))&ron(X50,X46))&rpoint(X50))),inference(fof_nnf,[status(thm)],[11])).
% fof(195, plain,![X52]:![X53]:(((~(rintersect(X52,X53))|![X54]:(~(X53=X54)|~(rcircle(X54))))|![X55]:(~(X52=X55)|~(rcircle(X55))))|?[X56]:?[X57]:((((((~(X56=X57)&ron(X57,X53))&ron(X57,X52))&rpoint(X57))&ron(X56,X53))&ron(X56,X52))&rpoint(X56))),inference(variable_rename,[status(thm)],[194])).
% fof(196, plain,![X52]:![X53]:(((~(rintersect(X52,X53))|![X54]:(~(X53=X54)|~(rcircle(X54))))|![X55]:(~(X52=X55)|~(rcircle(X55))))|((((((~(esk7_2(X52,X53)=esk8_2(X52,X53))&ron(esk8_2(X52,X53),X53))&ron(esk8_2(X52,X53),X52))&rpoint(esk8_2(X52,X53)))&ron(esk7_2(X52,X53),X53))&ron(esk7_2(X52,X53),X52))&rpoint(esk7_2(X52,X53)))),inference(skolemize,[status(esa)],[195])).
% fof(197, plain,![X52]:![X53]:![X54]:![X55]:(((~(X52=X55)|~(rcircle(X55)))|((~(X53=X54)|~(rcircle(X54)))|~(rintersect(X52,X53))))|((((((~(esk7_2(X52,X53)=esk8_2(X52,X53))&ron(esk8_2(X52,X53),X53))&ron(esk8_2(X52,X53),X52))&rpoint(esk8_2(X52,X53)))&ron(esk7_2(X52,X53),X53))&ron(esk7_2(X52,X53),X52))&rpoint(esk7_2(X52,X53)))),inference(shift_quantors,[status(thm)],[196])).
% fof(198, plain,![X52]:![X53]:![X54]:![X55]:(((((((~(esk7_2(X52,X53)=esk8_2(X52,X53))|((~(X52=X55)|~(rcircle(X55)))|((~(X53=X54)|~(rcircle(X54)))|~(rintersect(X52,X53)))))&(ron(esk8_2(X52,X53),X53)|((~(X52=X55)|~(rcircle(X55)))|((~(X53=X54)|~(rcircle(X54)))|~(rintersect(X52,X53))))))&(ron(esk8_2(X52,X53),X52)|((~(X52=X55)|~(rcircle(X55)))|((~(X53=X54)|~(rcircle(X54)))|~(rintersect(X52,X53))))))&(rpoint(esk8_2(X52,X53))|((~(X52=X55)|~(rcircle(X55)))|((~(X53=X54)|~(rcircle(X54)))|~(rintersect(X52,X53))))))&(ron(esk7_2(X52,X53),X53)|((~(X52=X55)|~(rcircle(X55)))|((~(X53=X54)|~(rcircle(X54)))|~(rintersect(X52,X53))))))&(ron(esk7_2(X52,X53),X52)|((~(X52=X55)|~(rcircle(X55)))|((~(X53=X54)|~(rcircle(X54)))|~(rintersect(X52,X53))))))&(rpoint(esk7_2(X52,X53))|((~(X52=X55)|~(rcircle(X55)))|((~(X53=X54)|~(rcircle(X54)))|~(rintersect(X52,X53)))))),inference(distribute,[status(thm)],[197])).
% cnf(202,plain,(rpoint(esk8_2(X1,X2))|~rintersect(X1,X2)|~rcircle(X3)|X2!=X3|~rcircle(X4)|X1!=X4),inference(split_conjunct,[status(thm)],[198])).
% cnf(203,plain,(ron(esk8_2(X1,X2),X1)|~rintersect(X1,X2)|~rcircle(X3)|X2!=X3|~rcircle(X4)|X1!=X4),inference(split_conjunct,[status(thm)],[198])).
% fof(220, plain,![X60]:![X61]:(~(rcenter(X60,X61))|rinside(X60,X61)),inference(fof_nnf,[status(thm)],[14])).
% fof(221, plain,![X62]:![X63]:(~(rcenter(X62,X63))|rinside(X62,X63)),inference(variable_rename,[status(thm)],[220])).
% cnf(222,plain,(rinside(X1,X2)|~rcenter(X1,X2)),inference(split_conjunct,[status(thm)],[221])).
% fof(223, plain,![X62]:![X63]:((![X64]:(~(X63=X64)|~(rpoint(X64)))|![X65]:(~(X62=X65)|~(rpoint(X65))))|vf(X62,X63)=vf(X63,X62)),inference(fof_nnf,[status(thm)],[15])).
% fof(224, plain,![X66]:![X67]:((![X68]:(~(X67=X68)|~(rpoint(X68)))|![X69]:(~(X66=X69)|~(rpoint(X69))))|vf(X66,X67)=vf(X67,X66)),inference(variable_rename,[status(thm)],[223])).
% fof(225, plain,![X66]:![X67]:![X68]:![X69]:(((~(X66=X69)|~(rpoint(X69)))|(~(X67=X68)|~(rpoint(X68))))|vf(X66,X67)=vf(X67,X66)),inference(shift_quantors,[status(thm)],[224])).
% cnf(226,plain,(vf(X1,X2)=vf(X2,X1)|~rpoint(X3)|X2!=X3|~rpoint(X4)|X1!=X4),inference(split_conjunct,[status(thm)],[225])).
% cnf(321,plain,(rpoint(vd1056)),inference(split_conjunct,[status(thm)],[32])).
% cnf(322,plain,(vd1055=vd1056),inference(split_conjunct,[status(thm)],[32])).
% cnf(323,plain,(rpoint(vd1058)),inference(split_conjunct,[status(thm)],[32])).
% cnf(324,plain,(vd1055!=vd1057),inference(split_conjunct,[status(thm)],[32])).
% cnf(325,plain,(vd1057=vd1058),inference(split_conjunct,[status(thm)],[32])).
% fof(501, plain,![X403]:![X404]:![X405]:![X406]:((((((~(ron(X404,X406))|~(rinside(X403,X406)))|~(rinside(X404,X405)))|~(ron(X403,X405)))|![X407]:(~(X404=X407)|~(rpoint(X407))))|![X408]:(~(X403=X408)|~(rpoint(X408))))|rintersect(X405,X406)),inference(fof_nnf,[status(thm)],[61])).
% fof(502, plain,![X409]:![X410]:![X411]:![X412]:((((((~(ron(X410,X412))|~(rinside(X409,X412)))|~(rinside(X410,X411)))|~(ron(X409,X411)))|![X413]:(~(X410=X413)|~(rpoint(X413))))|![X414]:(~(X409=X414)|~(rpoint(X414))))|rintersect(X411,X412)),inference(variable_rename,[status(thm)],[501])).
% fof(503, plain,![X409]:![X410]:![X411]:![X412]:![X413]:![X414]:(((~(X409=X414)|~(rpoint(X414)))|((~(X410=X413)|~(rpoint(X413)))|(((~(ron(X410,X412))|~(rinside(X409,X412)))|~(rinside(X410,X411)))|~(ron(X409,X411)))))|rintersect(X411,X412)),inference(shift_quantors,[status(thm)],[502])).
% cnf(504,plain,(rintersect(X1,X2)|~ron(X3,X1)|~rinside(X4,X1)|~rinside(X3,X2)|~ron(X4,X2)|~rpoint(X5)|X4!=X5|~rpoint(X6)|X3!=X6),inference(split_conjunct,[status(thm)],[503])).
% fof(749, negated_conjecture,?[X727]:(((ron(vd1057,X727)&rcenter(vd1055,X727))&rcircle(X727))&~(X727=vd1061)),inference(fof_nnf,[status(thm)],[106])).
% fof(750, negated_conjecture,?[X728]:(((ron(vd1057,X728)&rcenter(vd1055,X728))&rcircle(X728))&~(X728=vd1061)),inference(variable_rename,[status(thm)],[749])).
% fof(751, negated_conjecture,(((ron(vd1057,esk49_0)&rcenter(vd1055,esk49_0))&rcircle(esk49_0))&~(esk49_0=vd1061)),inference(skolemize,[status(esa)],[750])).
% cnf(752,negated_conjecture,(esk49_0!=vd1061),inference(split_conjunct,[status(thm)],[751])).
% cnf(753,negated_conjecture,(rcircle(esk49_0)),inference(split_conjunct,[status(thm)],[751])).
% cnf(754,negated_conjecture,(rcenter(vd1055,esk49_0)),inference(split_conjunct,[status(thm)],[751])).
% cnf(755,negated_conjecture,(ron(vd1057,esk49_0)),inference(split_conjunct,[status(thm)],[751])).
% cnf(756,plain,(rpoint(vd1057)),inference(rw,[status(thm)],[323,325,theory(equality)])).
% cnf(757,plain,(rpoint(vd1055)),inference(rw,[status(thm)],[321,322,theory(equality)])).
% cnf(759,negated_conjecture,(rinside(vd1055,esk49_0)),inference(spm,[status(thm)],[222,754,theory(equality)])).
% cnf(807,plain,(rpoint(esk8_2(X1,X2))|X1!=X3|~rintersect(X1,X2)|~rcircle(X3)|~rcircle(X2)),inference(er,[status(thm)],[202,theory(equality)])).
% cnf(808,plain,(rpoint(esk8_2(X1,X2))|~rintersect(X1,X2)|~rcircle(X1)|~rcircle(X2)),inference(er,[status(thm)],[807,theory(equality)])).
% cnf(817,plain,(ron(esk8_2(X1,X2),X1)|X1!=X3|~rintersect(X1,X2)|~rcircle(X3)|~rcircle(X2)),inference(er,[status(thm)],[203,theory(equality)])).
% cnf(818,plain,(ron(esk8_2(X1,X2),X1)|~rintersect(X1,X2)|~rcircle(X1)|~rcircle(X2)),inference(er,[status(thm)],[817,theory(equality)])).
% cnf(821,plain,(vf(X1,X2)=vf(X2,X1)|X1!=X3|~rpoint(X3)|~rpoint(X2)),inference(er,[status(thm)],[226,theory(equality)])).
% cnf(822,plain,(vf(X1,X2)=vf(X2,X1)|~rpoint(X1)|~rpoint(X2)),inference(er,[status(thm)],[821,theory(equality)])).
% cnf(823,plain,(X1=X2|rcircle(esk1_2(X1,X2))|X1!=X3|~rpoint(X3)|~rpoint(X2)),inference(er,[status(thm)],[149,theory(equality)])).
% cnf(824,plain,(X1=X2|rcircle(esk1_2(X1,X2))|~rpoint(X1)|~rpoint(X2)),inference(er,[status(thm)],[823,theory(equality)])).
% cnf(854,plain,(X1=X2|ron(X2,esk1_2(X1,X2))|X1!=X3|~rpoint(X3)|~rpoint(X2)),inference(er,[status(thm)],[151,theory(equality)])).
% cnf(855,plain,(X1=X2|ron(X2,esk1_2(X1,X2))|~rpoint(X1)|~rpoint(X2)),inference(er,[status(thm)],[854,theory(equality)])).
% cnf(860,plain,(X1=X2|rcenter(X1,esk1_2(X1,X2))|X1!=X3|~rpoint(X3)|~rpoint(X2)),inference(er,[status(thm)],[150,theory(equality)])).
% cnf(861,plain,(X1=X2|rcenter(X1,esk1_2(X1,X2))|~rpoint(X1)|~rpoint(X2)),inference(er,[status(thm)],[860,theory(equality)])).
% cnf(880,plain,(rpoint(esk5_4(X1,X2,X3,X3))|X2!=X1|~rpoint(X3)|~rcircle(X2)|~ron(X3,X1)),inference(er,[status(thm)],[173,theory(equality)])).
% cnf(881,plain,(rpoint(esk5_4(X1,X1,X2,X2))|~rpoint(X2)|~rcircle(X1)|~ron(X2,X1)),inference(er,[status(thm)],[880,theory(equality)])).
% cnf(884,plain,(ron(esk5_4(X1,X2,X3,X3),X1)|X2!=X1|~rpoint(X3)|~rcircle(X2)|~ron(X3,X1)),inference(er,[status(thm)],[174,theory(equality)])).
% cnf(885,plain,(ron(esk5_4(X1,X1,X2,X2),X1)|~rpoint(X2)|~rcircle(X1)|~ron(X2,X1)),inference(er,[status(thm)],[884,theory(equality)])).
% cnf(939,plain,(vf(X1,X2)=vf(X1,X3)|X4!=X2|~rpoint(X3)|~rpoint(X4)|~rcenter(X1,X5)|~ron(X3,X5)|~ron(X2,X5)),inference(er,[status(thm)],[185,theory(equality)])).
% cnf(940,plain,(vf(X1,X2)=vf(X1,X3)|~rpoint(X3)|~rpoint(X2)|~rcenter(X1,X4)|~ron(X3,X4)|~ron(X2,X4)),inference(er,[status(thm)],[939,theory(equality)])).
% cnf(957,plain,(ron(X1,X2)|vf(X3,X1)!=vf(X3,X4)|X5!=X1|~rpoint(X4)|~rpoint(X5)|~rcenter(X3,X2)|~ron(X4,X2)),inference(er,[status(thm)],[186,theory(equality)])).
% cnf(958,plain,(ron(X1,X2)|vf(X3,X1)!=vf(X3,X4)|~rpoint(X4)|~rpoint(X1)|~rcenter(X3,X2)|~ron(X4,X2)),inference(er,[status(thm)],[957,theory(equality)])).
% cnf(984,plain,(rintersect(X1,X2)|X3!=X4|~rinside(X5,X1)|~rinside(X3,X2)|~rpoint(X4)|~rpoint(X5)|~ron(X5,X2)|~ron(X3,X1)),inference(er,[status(thm)],[504,theory(equality)])).
% cnf(985,plain,(rintersect(X1,X2)|~rinside(X3,X1)|~rinside(X4,X2)|~rpoint(X4)|~rpoint(X3)|~ron(X3,X2)|~ron(X4,X1)),inference(er,[status(thm)],[984,theory(equality)])).
% cnf(1022,plain,(X1=X2|vf(X3,X4)!=vf(X3,X5)|X4!=X6|~rpoint(X6)|~rpoint(X5)|~rcenter(X3,X2)|~rcenter(X3,X1)|~ron(X5,X2)|~ron(X4,X1)),inference(er,[status(thm)],[190,theory(equality)])).
% cnf(1023,plain,(X1=X2|vf(X3,X4)!=vf(X3,X5)|~rpoint(X4)|~rpoint(X5)|~rcenter(X3,X2)|~rcenter(X3,X1)|~ron(X5,X2)|~ron(X4,X1)),inference(er,[status(thm)],[1022,theory(equality)])).
% cnf(1907,plain,(rinside(X1,esk1_2(X1,X2))|X1=X2|~rpoint(X1)|~rpoint(X2)),inference(spm,[status(thm)],[222,861,theory(equality)])).
% cnf(2029,negated_conjecture,(rpoint(esk5_4(esk49_0,esk49_0,vd1057,vd1057))|~rpoint(vd1057)|~rcircle(esk49_0)),inference(spm,[status(thm)],[881,755,theory(equality)])).
% cnf(2030,plain,(rpoint(esk5_4(vd1061,vd1061,vd1057,vd1057))|~rpoint(vd1057)|~rcircle(vd1061)),inference(spm,[status(thm)],[881,140,theory(equality)])).
% cnf(2034,negated_conjecture,(rpoint(esk5_4(esk49_0,esk49_0,vd1057,vd1057))|$false|~rcircle(esk49_0)),inference(rw,[status(thm)],[2029,756,theory(equality)])).
% cnf(2035,negated_conjecture,(rpoint(esk5_4(esk49_0,esk49_0,vd1057,vd1057))|$false|$false),inference(rw,[status(thm)],[2034,753,theory(equality)])).
% cnf(2036,negated_conjecture,(rpoint(esk5_4(esk49_0,esk49_0,vd1057,vd1057))),inference(cn,[status(thm)],[2035,theory(equality)])).
% cnf(2037,plain,(rpoint(esk5_4(vd1061,vd1061,vd1057,vd1057))|$false|~rcircle(vd1061)),inference(rw,[status(thm)],[2030,756,theory(equality)])).
% cnf(2038,plain,(rpoint(esk5_4(vd1061,vd1061,vd1057,vd1057))|$false|$false),inference(rw,[status(thm)],[2037,138,theory(equality)])).
% cnf(2039,plain,(rpoint(esk5_4(vd1061,vd1061,vd1057,vd1057))),inference(cn,[status(thm)],[2038,theory(equality)])).
% cnf(2044,negated_conjecture,(ron(esk5_4(esk49_0,esk49_0,vd1057,vd1057),esk49_0)|~rpoint(vd1057)|~rcircle(esk49_0)),inference(spm,[status(thm)],[885,755,theory(equality)])).
% cnf(2045,plain,(ron(esk5_4(vd1061,vd1061,vd1057,vd1057),vd1061)|~rpoint(vd1057)|~rcircle(vd1061)),inference(spm,[status(thm)],[885,140,theory(equality)])).
% cnf(2049,negated_conjecture,(ron(esk5_4(esk49_0,esk49_0,vd1057,vd1057),esk49_0)|$false|~rcircle(esk49_0)),inference(rw,[status(thm)],[2044,756,theory(equality)])).
% cnf(2050,negated_conjecture,(ron(esk5_4(esk49_0,esk49_0,vd1057,vd1057),esk49_0)|$false|$false),inference(rw,[status(thm)],[2049,753,theory(equality)])).
% cnf(2051,negated_conjecture,(ron(esk5_4(esk49_0,esk49_0,vd1057,vd1057),esk49_0)),inference(cn,[status(thm)],[2050,theory(equality)])).
% cnf(2052,plain,(ron(esk5_4(vd1061,vd1061,vd1057,vd1057),vd1061)|$false|~rcircle(vd1061)),inference(rw,[status(thm)],[2045,756,theory(equality)])).
% cnf(2053,plain,(ron(esk5_4(vd1061,vd1061,vd1057,vd1057),vd1061)|$false|$false),inference(rw,[status(thm)],[2052,138,theory(equality)])).
% cnf(2054,plain,(ron(esk5_4(vd1061,vd1061,vd1057,vd1057),vd1061)),inference(cn,[status(thm)],[2053,theory(equality)])).
% cnf(2586,negated_conjecture,(vf(vd1055,X1)=vf(vd1055,X2)|~rpoint(X2)|~rpoint(X1)|~ron(X2,esk49_0)|~ron(X1,esk49_0)),inference(spm,[status(thm)],[940,754,theory(equality)])).
% cnf(2587,plain,(vf(vd1055,X1)=vf(vd1055,X2)|~rpoint(X2)|~rpoint(X1)|~ron(X2,vd1061)|~ron(X1,vd1061)),inference(spm,[status(thm)],[940,139,theory(equality)])).
% cnf(2599,negated_conjecture,(vf(vd1055,X1)=vf(vd1055,vd1057)|~rpoint(vd1057)|~rpoint(X1)|~ron(X1,esk49_0)),inference(spm,[status(thm)],[2586,755,theory(equality)])).
% cnf(2606,negated_conjecture,(vf(vd1055,X1)=vf(vd1055,vd1057)|$false|~rpoint(X1)|~ron(X1,esk49_0)),inference(rw,[status(thm)],[2599,756,theory(equality)])).
% cnf(2607,negated_conjecture,(vf(vd1055,X1)=vf(vd1055,vd1057)|~rpoint(X1)|~ron(X1,esk49_0)),inference(cn,[status(thm)],[2606,theory(equality)])).
% cnf(2616,negated_conjecture,(vf(vd1055,esk5_4(esk49_0,esk49_0,vd1057,vd1057))=vf(vd1055,vd1057)|~rpoint(esk5_4(esk49_0,esk49_0,vd1057,vd1057))),inference(spm,[status(thm)],[2607,2051,theory(equality)])).
% cnf(2620,negated_conjecture,(vf(vd1055,esk5_4(esk49_0,esk49_0,vd1057,vd1057))=vf(vd1055,vd1057)|$false),inference(rw,[status(thm)],[2616,2036,theory(equality)])).
% cnf(2621,negated_conjecture,(vf(vd1055,esk5_4(esk49_0,esk49_0,vd1057,vd1057))=vf(vd1055,vd1057)),inference(cn,[status(thm)],[2620,theory(equality)])).
% cnf(2662,negated_conjecture,(ron(X1,X2)|vf(vd1055,X1)!=vf(vd1055,vd1057)|~rpoint(esk5_4(esk49_0,esk49_0,vd1057,vd1057))|~rpoint(X1)|~rcenter(vd1055,X2)|~ron(esk5_4(esk49_0,esk49_0,vd1057,vd1057),X2)),inference(spm,[status(thm)],[958,2621,theory(equality)])).
% cnf(2670,negated_conjecture,(ron(X1,X2)|vf(vd1055,X1)!=vf(vd1055,vd1057)|$false|~rpoint(X1)|~rcenter(vd1055,X2)|~ron(esk5_4(esk49_0,esk49_0,vd1057,vd1057),X2)),inference(rw,[status(thm)],[2662,2036,theory(equality)])).
% cnf(2671,negated_conjecture,(ron(X1,X2)|vf(vd1055,X1)!=vf(vd1055,vd1057)|~rpoint(X1)|~rcenter(vd1055,X2)|~ron(esk5_4(esk49_0,esk49_0,vd1057,vd1057),X2)),inference(cn,[status(thm)],[2670,theory(equality)])).
% cnf(2744,plain,(vf(vd1055,X1)=vf(vd1055,vd1057)|~rpoint(vd1057)|~rpoint(X1)|~ron(X1,vd1061)),inference(spm,[status(thm)],[2587,140,theory(equality)])).
% cnf(2751,plain,(vf(vd1055,X1)=vf(vd1055,vd1057)|$false|~rpoint(X1)|~ron(X1,vd1061)),inference(rw,[status(thm)],[2744,756,theory(equality)])).
% cnf(2752,plain,(vf(vd1055,X1)=vf(vd1055,vd1057)|~rpoint(X1)|~ron(X1,vd1061)),inference(cn,[status(thm)],[2751,theory(equality)])).
% cnf(2761,plain,(vf(vd1055,esk5_4(vd1061,vd1061,vd1057,vd1057))=vf(vd1055,vd1057)|~rpoint(esk5_4(vd1061,vd1061,vd1057,vd1057))),inference(spm,[status(thm)],[2752,2054,theory(equality)])).
% cnf(2765,plain,(vf(vd1055,esk5_4(vd1061,vd1061,vd1057,vd1057))=vf(vd1055,vd1057)|$false),inference(rw,[status(thm)],[2761,2039,theory(equality)])).
% cnf(2766,plain,(vf(vd1055,esk5_4(vd1061,vd1061,vd1057,vd1057))=vf(vd1055,vd1057)),inference(cn,[status(thm)],[2765,theory(equality)])).
% cnf(2772,plain,(ron(X1,X2)|vf(vd1055,X1)!=vf(vd1055,vd1057)|~rpoint(esk5_4(vd1061,vd1061,vd1057,vd1057))|~rpoint(X1)|~rcenter(vd1055,X2)|~ron(esk5_4(vd1061,vd1061,vd1057,vd1057),X2)),inference(spm,[status(thm)],[958,2766,theory(equality)])).
% cnf(2785,plain,(ron(X1,X2)|vf(vd1055,X1)!=vf(vd1055,vd1057)|$false|~rpoint(X1)|~rcenter(vd1055,X2)|~ron(esk5_4(vd1061,vd1061,vd1057,vd1057),X2)),inference(rw,[status(thm)],[2772,2039,theory(equality)])).
% cnf(2786,plain,(ron(X1,X2)|vf(vd1055,X1)!=vf(vd1055,vd1057)|~rpoint(X1)|~rcenter(vd1055,X2)|~ron(esk5_4(vd1061,vd1061,vd1057,vd1057),X2)),inference(cn,[status(thm)],[2785,theory(equality)])).
% cnf(2858,negated_conjecture,(ron(X1,X2)|vf(vd1055,X1)!=vf(vd1057,vd1055)|~rpoint(X1)|~rcenter(vd1055,X2)|~ron(esk5_4(esk49_0,esk49_0,vd1057,vd1057),X2)|~rpoint(vd1055)|~rpoint(vd1057)),inference(spm,[status(thm)],[2671,822,theory(equality)])).
% cnf(2871,negated_conjecture,(ron(X1,X2)|vf(vd1055,X1)!=vf(vd1057,vd1055)|~rpoint(X1)|~rcenter(vd1055,X2)|~ron(esk5_4(esk49_0,esk49_0,vd1057,vd1057),X2)|$false|~rpoint(vd1057)),inference(rw,[status(thm)],[2858,757,theory(equality)])).
% cnf(2872,negated_conjecture,(ron(X1,X2)|vf(vd1055,X1)!=vf(vd1057,vd1055)|~rpoint(X1)|~rcenter(vd1055,X2)|~ron(esk5_4(esk49_0,esk49_0,vd1057,vd1057),X2)|$false|$false),inference(rw,[status(thm)],[2871,756,theory(equality)])).
% cnf(2873,negated_conjecture,(ron(X1,X2)|vf(vd1055,X1)!=vf(vd1057,vd1055)|~rpoint(X1)|~rcenter(vd1055,X2)|~ron(esk5_4(esk49_0,esk49_0,vd1057,vd1057),X2)),inference(cn,[status(thm)],[2872,theory(equality)])).
% cnf(2909,negated_conjecture,(rintersect(esk49_0,X1)|~rinside(X2,X1)|~rpoint(X2)|~rpoint(vd1055)|~ron(vd1055,X1)|~ron(X2,esk49_0)),inference(spm,[status(thm)],[985,759,theory(equality)])).
% cnf(2912,negated_conjecture,(rintersect(esk49_0,X1)|~rinside(X2,X1)|~rpoint(X2)|$false|~ron(vd1055,X1)|~ron(X2,esk49_0)),inference(rw,[status(thm)],[2909,757,theory(equality)])).
% cnf(2913,negated_conjecture,(rintersect(esk49_0,X1)|~rinside(X2,X1)|~rpoint(X2)|~ron(vd1055,X1)|~ron(X2,esk49_0)),inference(cn,[status(thm)],[2912,theory(equality)])).
% cnf(3062,negated_conjecture,(rintersect(esk49_0,esk1_2(X1,vd1055))|X1=vd1055|~rinside(X2,esk1_2(X1,vd1055))|~rpoint(X2)|~ron(X2,esk49_0)|~rpoint(X1)|~rpoint(vd1055)),inference(spm,[status(thm)],[2913,855,theory(equality)])).
% cnf(3067,negated_conjecture,(rintersect(esk49_0,esk1_2(X1,vd1055))|X1=vd1055|~rinside(X2,esk1_2(X1,vd1055))|~rpoint(X2)|~ron(X2,esk49_0)|~rpoint(X1)|$false),inference(rw,[status(thm)],[3062,757,theory(equality)])).
% cnf(3068,negated_conjecture,(rintersect(esk49_0,esk1_2(X1,vd1055))|X1=vd1055|~rinside(X2,esk1_2(X1,vd1055))|~rpoint(X2)|~ron(X2,esk49_0)|~rpoint(X1)),inference(cn,[status(thm)],[3067,theory(equality)])).
% cnf(3228,negated_conjecture,(ron(X1,vd1061)|vf(vd1055,X1)!=vf(vd1057,vd1055)|~rpoint(X1)|~ron(esk5_4(esk49_0,esk49_0,vd1057,vd1057),vd1061)),inference(spm,[status(thm)],[2873,139,theory(equality)])).
% cnf(3348,negated_conjecture,(ron(esk5_4(esk49_0,esk49_0,vd1057,vd1057),X1)|~rpoint(esk5_4(esk49_0,esk49_0,vd1057,vd1057))|~rcenter(vd1055,X1)|~ron(esk5_4(vd1061,vd1061,vd1057,vd1057),X1)),inference(spm,[status(thm)],[2786,2621,theory(equality)])).
% cnf(3366,negated_conjecture,(ron(esk5_4(esk49_0,esk49_0,vd1057,vd1057),X1)|$false|~rcenter(vd1055,X1)|~ron(esk5_4(vd1061,vd1061,vd1057,vd1057),X1)),inference(rw,[status(thm)],[3348,2036,theory(equality)])).
% cnf(3367,negated_conjecture,(ron(esk5_4(esk49_0,esk49_0,vd1057,vd1057),X1)|~rcenter(vd1055,X1)|~ron(esk5_4(vd1061,vd1061,vd1057,vd1057),X1)),inference(cn,[status(thm)],[3366,theory(equality)])).
% cnf(3395,negated_conjecture,(ron(esk5_4(esk49_0,esk49_0,vd1057,vd1057),vd1061)|~ron(esk5_4(vd1061,vd1061,vd1057,vd1057),vd1061)),inference(spm,[status(thm)],[3367,139,theory(equality)])).
% cnf(3401,negated_conjecture,(ron(esk5_4(esk49_0,esk49_0,vd1057,vd1057),vd1061)|$false),inference(rw,[status(thm)],[3395,2054,theory(equality)])).
% cnf(3402,negated_conjecture,(ron(esk5_4(esk49_0,esk49_0,vd1057,vd1057),vd1061)),inference(cn,[status(thm)],[3401,theory(equality)])).
% cnf(3410,negated_conjecture,(ron(X1,vd1061)|vf(vd1055,X1)!=vf(vd1057,vd1055)|~rpoint(X1)|$false),inference(rw,[status(thm)],[3228,3402,theory(equality)])).
% cnf(3411,negated_conjecture,(ron(X1,vd1061)|vf(vd1055,X1)!=vf(vd1057,vd1055)|~rpoint(X1)),inference(cn,[status(thm)],[3410,theory(equality)])).
% cnf(4233,plain,(X1=X2|~rpoint(X3)|~rcenter(X4,X2)|~rcenter(X4,X1)|~ron(X3,X2)|~ron(X3,X1)),inference(er,[status(thm)],[1023,theory(equality)])).
% cnf(203101,negated_conjecture,(X1=vd1055|rintersect(esk49_0,esk1_2(X1,vd1055))|~rinside(vd1057,esk1_2(X1,vd1055))|~rpoint(vd1057)|~rpoint(X1)),inference(spm,[status(thm)],[3068,755,theory(equality)])).
% cnf(203571,negated_conjecture,(X1=vd1055|rintersect(esk49_0,esk1_2(X1,vd1055))|~rinside(vd1057,esk1_2(X1,vd1055))|$false|~rpoint(X1)),inference(rw,[status(thm)],[203101,756,theory(equality)])).
% cnf(203572,negated_conjecture,(X1=vd1055|rintersect(esk49_0,esk1_2(X1,vd1055))|~rinside(vd1057,esk1_2(X1,vd1055))|~rpoint(X1)),inference(cn,[status(thm)],[203571,theory(equality)])).
% cnf(204519,negated_conjecture,(vd1057=vd1055|rintersect(esk49_0,esk1_2(vd1057,vd1055))|~rpoint(vd1057)|~rpoint(vd1055)),inference(spm,[status(thm)],[203572,1907,theory(equality)])).
% cnf(204520,negated_conjecture,(vd1057=vd1055|rintersect(esk49_0,esk1_2(vd1057,vd1055))|$false|~rpoint(vd1055)),inference(rw,[status(thm)],[204519,756,theory(equality)])).
% cnf(204521,negated_conjecture,(vd1057=vd1055|rintersect(esk49_0,esk1_2(vd1057,vd1055))|$false|$false),inference(rw,[status(thm)],[204520,757,theory(equality)])).
% cnf(204522,negated_conjecture,(vd1057=vd1055|rintersect(esk49_0,esk1_2(vd1057,vd1055))),inference(cn,[status(thm)],[204521,theory(equality)])).
% cnf(204523,negated_conjecture,(rintersect(esk49_0,esk1_2(vd1057,vd1055))),inference(sr,[status(thm)],[204522,324,theory(equality)])).
% cnf(204525,negated_conjecture,(rpoint(esk8_2(esk49_0,esk1_2(vd1057,vd1055)))|~rcircle(esk49_0)|~rcircle(esk1_2(vd1057,vd1055))),inference(spm,[status(thm)],[808,204523,theory(equality)])).
% cnf(204529,negated_conjecture,(ron(esk8_2(esk49_0,esk1_2(vd1057,vd1055)),esk49_0)|~rcircle(esk49_0)|~rcircle(esk1_2(vd1057,vd1055))),inference(spm,[status(thm)],[818,204523,theory(equality)])).
% cnf(204554,negated_conjecture,(rpoint(esk8_2(esk49_0,esk1_2(vd1057,vd1055)))|$false|~rcircle(esk1_2(vd1057,vd1055))),inference(rw,[status(thm)],[204525,753,theory(equality)])).
% cnf(204555,negated_conjecture,(rpoint(esk8_2(esk49_0,esk1_2(vd1057,vd1055)))|~rcircle(esk1_2(vd1057,vd1055))),inference(cn,[status(thm)],[204554,theory(equality)])).
% cnf(204562,negated_conjecture,(ron(esk8_2(esk49_0,esk1_2(vd1057,vd1055)),esk49_0)|$false|~rcircle(esk1_2(vd1057,vd1055))),inference(rw,[status(thm)],[204529,753,theory(equality)])).
% cnf(204563,negated_conjecture,(ron(esk8_2(esk49_0,esk1_2(vd1057,vd1055)),esk49_0)|~rcircle(esk1_2(vd1057,vd1055))),inference(cn,[status(thm)],[204562,theory(equality)])).
% cnf(204676,negated_conjecture,(ron(esk8_2(esk49_0,esk1_2(vd1057,vd1055)),esk49_0)|vd1057=vd1055|~rpoint(vd1057)|~rpoint(vd1055)),inference(spm,[status(thm)],[204563,824,theory(equality)])).
% cnf(204677,negated_conjecture,(ron(esk8_2(esk49_0,esk1_2(vd1057,vd1055)),esk49_0)|vd1057=vd1055|$false|~rpoint(vd1055)),inference(rw,[status(thm)],[204676,756,theory(equality)])).
% cnf(204678,negated_conjecture,(ron(esk8_2(esk49_0,esk1_2(vd1057,vd1055)),esk49_0)|vd1057=vd1055|$false|$false),inference(rw,[status(thm)],[204677,757,theory(equality)])).
% cnf(204679,negated_conjecture,(ron(esk8_2(esk49_0,esk1_2(vd1057,vd1055)),esk49_0)|vd1057=vd1055),inference(cn,[status(thm)],[204678,theory(equality)])).
% cnf(204680,negated_conjecture,(ron(esk8_2(esk49_0,esk1_2(vd1057,vd1055)),esk49_0)),inference(sr,[status(thm)],[204679,324,theory(equality)])).
% cnf(204739,negated_conjecture,(vf(vd1055,esk8_2(esk49_0,esk1_2(vd1057,vd1055)))=vf(vd1055,vd1057)|~rpoint(esk8_2(esk49_0,esk1_2(vd1057,vd1055)))),inference(spm,[status(thm)],[2607,204680,theory(equality)])).
% cnf(204774,negated_conjecture,(rpoint(esk8_2(esk49_0,esk1_2(vd1057,vd1055)))|vd1057=vd1055|~rpoint(vd1057)|~rpoint(vd1055)),inference(spm,[status(thm)],[204555,824,theory(equality)])).
% cnf(204775,negated_conjecture,(rpoint(esk8_2(esk49_0,esk1_2(vd1057,vd1055)))|vd1057=vd1055|$false|~rpoint(vd1055)),inference(rw,[status(thm)],[204774,756,theory(equality)])).
% cnf(204776,negated_conjecture,(rpoint(esk8_2(esk49_0,esk1_2(vd1057,vd1055)))|vd1057=vd1055|$false|$false),inference(rw,[status(thm)],[204775,757,theory(equality)])).
% cnf(204777,negated_conjecture,(rpoint(esk8_2(esk49_0,esk1_2(vd1057,vd1055)))|vd1057=vd1055),inference(cn,[status(thm)],[204776,theory(equality)])).
% cnf(204778,negated_conjecture,(rpoint(esk8_2(esk49_0,esk1_2(vd1057,vd1055)))),inference(sr,[status(thm)],[204777,324,theory(equality)])).
% cnf(206817,negated_conjecture,(vf(vd1055,esk8_2(esk49_0,esk1_2(vd1057,vd1055)))=vf(vd1055,vd1057)|$false),inference(rw,[status(thm)],[204739,204778,theory(equality)])).
% cnf(206818,negated_conjecture,(vf(vd1055,esk8_2(esk49_0,esk1_2(vd1057,vd1055)))=vf(vd1055,vd1057)),inference(cn,[status(thm)],[206817,theory(equality)])).
% cnf(206839,negated_conjecture,(ron(esk8_2(esk49_0,esk1_2(vd1057,vd1055)),vd1061)|vf(vd1055,vd1057)!=vf(vd1057,vd1055)|~rpoint(esk8_2(esk49_0,esk1_2(vd1057,vd1055)))),inference(spm,[status(thm)],[3411,206818,theory(equality)])).
% cnf(206896,negated_conjecture,(ron(esk8_2(esk49_0,esk1_2(vd1057,vd1055)),vd1061)|vf(vd1055,vd1057)!=vf(vd1057,vd1055)|$false),inference(rw,[status(thm)],[206839,204778,theory(equality)])).
% cnf(206897,negated_conjecture,(ron(esk8_2(esk49_0,esk1_2(vd1057,vd1055)),vd1061)|vf(vd1055,vd1057)!=vf(vd1057,vd1055)),inference(cn,[status(thm)],[206896,theory(equality)])).
% cnf(206914,negated_conjecture,(ron(esk8_2(esk49_0,esk1_2(vd1057,vd1055)),vd1061)|~rpoint(vd1055)|~rpoint(vd1057)),inference(spm,[status(thm)],[206897,822,theory(equality)])).
% cnf(206916,negated_conjecture,(ron(esk8_2(esk49_0,esk1_2(vd1057,vd1055)),vd1061)|$false|~rpoint(vd1057)),inference(rw,[status(thm)],[206914,757,theory(equality)])).
% cnf(206917,negated_conjecture,(ron(esk8_2(esk49_0,esk1_2(vd1057,vd1055)),vd1061)|$false|$false),inference(rw,[status(thm)],[206916,756,theory(equality)])).
% cnf(206918,negated_conjecture,(ron(esk8_2(esk49_0,esk1_2(vd1057,vd1055)),vd1061)),inference(cn,[status(thm)],[206917,theory(equality)])).
% cnf(526958,negated_conjecture,(X1=esk49_0|~rpoint(X2)|~rcenter(vd1055,X1)|~ron(X2,esk49_0)|~ron(X2,X1)),inference(spm,[status(thm)],[4233,754,theory(equality)])).
% cnf(526962,negated_conjecture,(vd1061=esk49_0|~rpoint(X1)|~ron(X1,esk49_0)|~ron(X1,vd1061)),inference(spm,[status(thm)],[526958,139,theory(equality)])).
% cnf(526965,negated_conjecture,(~rpoint(X1)|~ron(X1,esk49_0)|~ron(X1,vd1061)),inference(sr,[status(thm)],[526962,752,theory(equality)])).
% cnf(526976,negated_conjecture,(~rpoint(esk8_2(esk49_0,esk1_2(vd1057,vd1055)))|~ron(esk8_2(esk49_0,esk1_2(vd1057,vd1055)),vd1061)),inference(spm,[status(thm)],[526965,204680,theory(equality)])).
% cnf(528550,negated_conjecture,($false|~ron(esk8_2(esk49_0,esk1_2(vd1057,vd1055)),vd1061)),inference(rw,[status(thm)],[526976,204778,theory(equality)])).
% cnf(528551,negated_conjecture,($false|$false),inference(rw,[status(thm)],[528550,206918,theory(equality)])).
% cnf(528552,negated_conjecture,($false),inference(cn,[status(thm)],[528551,theory(equality)])).
% cnf(528553,negated_conjecture,($false),528552,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 7174
% # ...of these trivial : 134
% # ...subsumed : 860
% # ...remaining for further processing: 6180
% # Other redundant clauses eliminated : 1088
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 56
% # Backward-rewritten : 159
% # Generated clauses : 341651
% # ...of the previous two non-trivial : 338898
% # Contextual simplify-reflections : 102
% # Paramodulations : 341375
% # Factorizations : 8
% # Equation resolutions : 1124
% # Current number of processed clauses: 5733
% # Positive orientable unit clauses: 4168
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 8
% # Non-unit-clauses : 1557
% # Current number of unprocessed clauses: 322361
% # ...number of literals in the above : 2765749
% # Clause-clause subsumption calls (NU) : 75357
% # Rec. Clause-clause subsumption calls : 30635
% # Unit Clause-clause subsumption calls : 6962
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 2384313
% # Indexed BW rewrite successes : 153
% # Backwards rewriting index: 603 leaves, 14.58+/-127.629 terms/leaf
% # Paramod-from index: 166 leaves, 25.81+/-164.668 terms/leaf
% # Paramod-into index: 319 leaves, 24.07+/-169.033 terms/leaf
% # -------------------------------------------------
% # User time : 27.474 s
% # System time : 0.760 s
% # Total time : 28.234 s
% # Maximum resident set size: 0 pages
% PrfWatch: 40.97 CPU 42.78 WC
% FINAL PrfWatch: 40.97 CPU 42.78 WC
% SZS output end Solution for /tmp/SystemOnTPTP18260/GEO271+1.tptp
%
%------------------------------------------------------------------------------