SRASS---0.1.THM-Sol.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : SRASS---0.1
% Problem  : GEO290+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 : 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 : Wed Dec 29 05:29:49 EST 2010

% Result   : Theorem 34.00s
% Output   : Solution 34.00s
% 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/SystemOnTPTP26913/GEO290+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM       ... 
% found
% SZS status THM for /tmp/SystemOnTPTP26913/GEO290+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP26913/GEO290+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 27009
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% PrfWatch: 1.93 CPU 2.01 WC
% PrfWatch: 3.92 CPU 4.02 WC
% PrfWatch: 5.91 CPU 6.02 WC
% PrfWatch: 7.90 CPU 8.03 WC
% PrfWatch: 9.89 CPU 10.03 WC
% PrfWatch: 11.89 CPU 12.04 WC
% PrfWatch: 13.87 CPU 14.04 WC
% PrfWatch: 15.87 CPU 16.05 WC
% PrfWatch: 17.85 CPU 18.05 WC
% PrfWatch: 19.84 CPU 20.06 WC
% PrfWatch: 21.84 CPU 22.06 WC
% # Preprocessing time     : 0.080 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 23.82 CPU 24.07 WC
% PrfWatch: 25.81 CPU 26.07 WC
% PrfWatch: 27.80 CPU 28.08 WC
% PrfWatch: 29.80 CPU 30.08 WC
% PrfWatch: 31.44 CPU 32.08 WC
% # SZS output start CNFRefutation.
% fof(1, axiom,~(rR(vd1186,vd1199,vd1185)),file('/tmp/SRASS.s.p', 'neg(neg(conjunct2(conjunct2(comma_conjunct2(plural(271))))))')).
% fof(2, axiom,~(vd1199=vd1185),file('/tmp/SRASS.s.p', 'holds(275, 1217, 0)')).
% fof(3, axiom,?[X1]:(vd1199=X1&rpoint(X1)),file('/tmp/SRASS.s.p', 'qe(s1(plural(271)))')).
% fof(7, axiom,![X26]:![X27]:![X28]:((((rR(X27,X26,X28)&?[X29]:(X28=X29&rpoint(X29)))&?[X30]:(X27=X30&rpoint(X30)))&?[X31]:(X26=X31&rpoint(X31)))=>(((~(rR(X26,X27,X28))&~(X26=X28))&~(X26=X27))&rR(X27,X28,X26))),file('/tmp/SRASS.s.p', 'qu(cond(axiom(81), 0), imp(cond(axiom(81), 0)))')).
% fof(8, axiom,vf(vd1199,vd1200)=vf(vd1185,vd1186),file('/tmp/SRASS.s.p', 'holds(273, 1215, 0)')).
% fof(19, axiom,vd1200=vd1186,file('/tmp/SRASS.s.p', 'holds(conjunct1(comma_conjunct2(plural(271))), 1212, 0)')).
% fof(20, axiom,ron(vd1185,vd1197),file('/tmp/SRASS.s.p', 'pred(s3(plural(274)), 0)')).
% fof(22, axiom,ron(vd1186,vd1197),file('/tmp/SRASS.s.p', 'pred(s2(plural(269)), 0)')).
% fof(23, axiom,?[X93]:(vd1200=X93&rpoint(X93)),file('/tmp/SRASS.s.p', 'qe(s2(plural(271)))')).
% fof(24, axiom,![X94]:![X95]:((?[X96]:(X95=X96&rpoint(X96))&?[X97]:(X94=X97&rpoint(X97)))=>vf(X94,X95)=vf(X95,X94)),file('/tmp/SRASS.s.p', 'qu(cond(axiom(166), 0), imp(cond(axiom(166), 0)))')).
% fof(25, axiom,ron(vd1199,vd1197),file('/tmp/SRASS.s.p', 'pred(s1(plural(274)), 0)')).
% fof(28, axiom,![X98]:![X99]:![X100]:![X101]:![X102]:(((((((((((X101=X102&ron(X100,X101))&ron(X99,X101))&ron(X98,X101))&rline(X102))&~(X99=X100))&~(X98=X100))&~(X98=X99))&?[X103]:(X100=X103&rpoint(X103)))&?[X104]:(X99=X104&rpoint(X104)))&?[X105]:(X98=X105&rpoint(X105)))=>((rR(X99,X98,X100)|rR(X98,X99,X100))|rR(X100,X98,X99))),file('/tmp/SRASS.s.p', 'qu(cond(axiom(91), 0), imp(cond(axiom(91), 0)))')).
% fof(32, axiom,![X131]:![X132]:![X133]:![X134]:(((((((~(X133=X134)&ron(X134,X131))&ron(X133,X131))&?[X135]:(X134=X135&rpoint(X135)))&?[X136]:(X133=X136&rpoint(X136)))&X131=X132)&rline(X132))=>?[X137]:(rR(X134,X133,X137)&rpoint(X137))),file('/tmp/SRASS.s.p', 'qu(cond(axiom(29), 0), imp(cond(axiom(29), 0)))')).
% fof(35, axiom,![X158]:![X159]:![X160]:![X161]:(((((((~(X160=X161)&ron(X161,X158))&ron(X160,X158))&?[X162]:(X161=X162&rpoint(X162)))&?[X163]:(X160=X163&rpoint(X163)))&X158=X159)&rline(X159))=>?[X164]:(rR(X164,X160,X161)&rpoint(X164))),file('/tmp/SRASS.s.p', 'qu(cond(axiom(23), 0), imp(cond(axiom(23), 0)))')).
% fof(52, axiom,rline(vd1197),file('/tmp/SRASS.s.p', 'pred(269, 0)')).
% fof(60, axiom,![X324]:![X325]:![X326]:((((rR(X325,X324,X326)&?[X327]:(X326=X327&rpoint(X327)))&?[X328]:(X325=X328&rpoint(X328)))&?[X329]:(X324=X329&rpoint(X329)))=>vplus(vf(X324,X325),vf(X325,X326))=vf(X324,X326)),file('/tmp/SRASS.s.p', 'qu(cond(axiom(180), 0), imp(cond(axiom(180), 0)))')).
% fof(75, axiom,![X441]:![X442]:((?[X443]:(X442=X443&rpoint(X443))&?[X444]:(X441=X444&rpoint(X444)))=>?[X445]:(vf(X441,X442)=X445&rreal(X445))),file('/tmp/SRASS.s.p', 'qu(cond(axiom(160), 0), imp(cond(axiom(160), 0)))')).
% fof(81, axiom,![X506]:![X507]:((?[X508]:(X507=X508&rpoint(X508))&?[X509]:(X506=X509&rpoint(X509)))=>(vf(X506,X507)=v0<=>X506=X507)),file('/tmp/SRASS.s.p', 'qu(cond(axiom(162), 0), imp(cond(axiom(162), 0)))')).
% fof(86, axiom,((((((((((((~(?[X518]:(((ron(vd1187,X518)&ron(vd1186,X518))&ron(vd1185,X518))&rline(X518)))&vangle(vd1179,vd1178,vd1180)=vangle(vd1186,vd1185,vd1187))&vf(vd1178,vd1180)=vf(vd1185,vd1187))&vf(vd1178,vd1179)=vf(vd1185,vd1186))&?[X519]:(vd1187=X519&rpoint(X519)))&?[X520]:(vd1186=X520&rpoint(X520)))&?[X521]:(vd1185=X521&rpoint(X521)))&~(vd1179=vd1180))&~(vd1178=vd1180))&~(vd1178=vd1179))&?[X522]:(vd1180=X522&rpoint(X522)))&?[X523]:(vd1179=X523&rpoint(X523)))&?[X524]:(vd1178=X524&rpoint(X524))),file('/tmp/SRASS.s.p', 'and(neg(neg(conjunct2(conjunct2(conjunct2(plural(comma_conjunct2(268))))))), and(holds(conjunct1(conjunct2(conjunct2(plural(comma_conjunct2(268))))), 1194, 0), and(holds(conjunct1(conjunct2(plural(comma_conjunct2(268)))), 1193, 0), and(holds(conjunct1(plural(comma_conjunct2(268))), 1192, 0), and(qe(s3(plural(comma_conjunct2(268)))), and(qe(s2(plural(comma_conjunct2(268)))), and(qe(s1(plural(comma_conjunct2(268)))), and(pred(comma_conjunct1(268), 9), and(pred(comma_conjunct1(268), 8), and(pred(comma_conjunct1(268), 7), and(qe(s3(plural(268))), and(qe(s2(plural(268))), qe(s1(plural(268)))))))))))))))')).
% fof(91, axiom,![X534]:![X535]:![X536]:![X537]:((((ron(X535,X537)&rcenter(X536,X537))&?[X538]:(X535=X538&rpoint(X538)))&?[X539]:(X534=X539&rpoint(X539)))=>(rless(vf(X536,X534),vf(X536,X535))<=>rinside(X534,X537))),file('/tmp/SRASS.s.p', 'qu(cond(axiom(186), 0), imp(cond(axiom(186), 0)))')).
% fof(101, axiom,![X577]:![X578]:![X579]:![X580]:![X581]:![X582]:((((((ron(X581,X580)&X581=X582)&rpoint(X582))&rcenter(X579,X580))&X577=X578)&rpoint(X578))=>(vf(X579,X577)=vf(X579,X581)<=>ron(X577,X580))),file('/tmp/SRASS.s.p', 'qu(cond(axiom(184), 0), imp(cond(axiom(184), 0)))')).
% fof(110, axiom,![X634]:![X635]:![X636]:![X637]:![X638]:![X639]:(((((((vplus(X634,X638)=vplus(X636,X638)&X638=X639)&rreal(X639))&X636=X637)&rreal(X637))&X634=X635)&rreal(X635))=>X634=X636),file('/tmp/SRASS.s.p', 'ass(cond(156, 0), 0)')).
% fof(113, axiom,![X652]:![X653]:![X654]:![X655]:((((X654=X655&rreal(X655))&X652=X653)&rreal(X653))=>((rless(X652,X654)|X652=X654)|rless(X654,X652))),file('/tmp/SRASS.s.p', 'qu(cond(axiom(145), 0), imp(cond(axiom(145), 0)))')).
% fof(114, axiom,![X656]:![X657]:![X658]:![X659]:((((X658=X659&rreal(X659))&X656=X657)&rreal(X657))=>vplus(X656,X658)=vplus(X658,X656)),file('/tmp/SRASS.s.p', 'qu(cond(axiom(143), 0), imp(cond(axiom(143), 0)))')).
% fof(115, axiom,![X660]:![X661]:![X662]:![X663]:((((X662=X663&rreal(X663))&X660=X661)&rreal(X661))=>?[X664]:(vplus(X660,X662)=X664&rreal(X664))),file('/tmp/SRASS.s.p', 'qu(cond(axiom(139), 0), imp(cond(axiom(139), 0)))')).
% fof(119, axiom,![X673]:![X674]:![X675]:![X676]:(((((rinside(X673,X675)&X675=X676)&rcircle(X676))&X673=X674)&rpoint(X674))=>~(ron(X673,X675))),file('/tmp/SRASS.s.p', 'qu(cond(axiom(79), 0), imp(cond(axiom(79), 0)))')).
% fof(121, axiom,![X683]:![X684]:(((~(X683=X684)&?[X685]:(X684=X685&rpoint(X685)))&?[X686]:(X683=X686&rpoint(X686)))=>?[X687]:((ron(X684,X687)&rcenter(X683,X687))&rcircle(X687))),file('/tmp/SRASS.s.p', 'qu(cond(axiom(53), 0), imp(cond(axiom(53), 0)))')).
% fof(135, conjecture,(rR(vd1199,vd1185,vd1186)|rR(vd1185,vd1199,vd1186)),file('/tmp/SRASS.s.p', 'dis(276)')).
% fof(136, negated_conjecture,~((rR(vd1199,vd1185,vd1186)|rR(vd1185,vd1199,vd1186))),inference(assume_negation,[status(cth)],[135])).
% fof(137, plain,~(rR(vd1186,vd1199,vd1185)),inference(fof_simplification,[status(thm)],[1,theory(equality)])).
% fof(139, plain,![X26]:![X27]:![X28]:((((rR(X27,X26,X28)&?[X29]:(X28=X29&rpoint(X29)))&?[X30]:(X27=X30&rpoint(X30)))&?[X31]:(X26=X31&rpoint(X31)))=>(((~(rR(X26,X27,X28))&~(X26=X28))&~(X26=X27))&rR(X27,X28,X26))),inference(fof_simplification,[status(thm)],[7,theory(equality)])).
% fof(168, plain,![X673]:![X674]:![X675]:![X676]:(((((rinside(X673,X675)&X675=X676)&rcircle(X676))&X673=X674)&rpoint(X674))=>~(ron(X673,X675))),inference(fof_simplification,[status(thm)],[119,theory(equality)])).
% cnf(170,plain,(~rR(vd1186,vd1199,vd1185)),inference(split_conjunct,[status(thm)],[137])).
% cnf(171,plain,(vd1199!=vd1185),inference(split_conjunct,[status(thm)],[2])).
% fof(172, plain,?[X2]:(vd1199=X2&rpoint(X2)),inference(variable_rename,[status(thm)],[3])).
% fof(173, plain,(vd1199=esk1_0&rpoint(esk1_0)),inference(skolemize,[status(esa)],[172])).
% cnf(174,plain,(rpoint(esk1_0)),inference(split_conjunct,[status(thm)],[173])).
% cnf(175,plain,(vd1199=esk1_0),inference(split_conjunct,[status(thm)],[173])).
% fof(188, plain,![X26]:![X27]:![X28]:((((~(rR(X27,X26,X28))|![X29]:(~(X28=X29)|~(rpoint(X29))))|![X30]:(~(X27=X30)|~(rpoint(X30))))|![X31]:(~(X26=X31)|~(rpoint(X31))))|(((~(rR(X26,X27,X28))&~(X26=X28))&~(X26=X27))&rR(X27,X28,X26))),inference(fof_nnf,[status(thm)],[139])).
% fof(189, plain,![X32]:![X33]:![X34]:((((~(rR(X33,X32,X34))|![X35]:(~(X34=X35)|~(rpoint(X35))))|![X36]:(~(X33=X36)|~(rpoint(X36))))|![X37]:(~(X32=X37)|~(rpoint(X37))))|(((~(rR(X32,X33,X34))&~(X32=X34))&~(X32=X33))&rR(X33,X34,X32))),inference(variable_rename,[status(thm)],[188])).
% fof(190, plain,![X32]:![X33]:![X34]:![X35]:![X36]:![X37]:(((~(X32=X37)|~(rpoint(X37)))|((~(X33=X36)|~(rpoint(X36)))|((~(X34=X35)|~(rpoint(X35)))|~(rR(X33,X32,X34)))))|(((~(rR(X32,X33,X34))&~(X32=X34))&~(X32=X33))&rR(X33,X34,X32))),inference(shift_quantors,[status(thm)],[189])).
% fof(191, plain,![X32]:![X33]:![X34]:![X35]:![X36]:![X37]:((((~(rR(X32,X33,X34))|((~(X32=X37)|~(rpoint(X37)))|((~(X33=X36)|~(rpoint(X36)))|((~(X34=X35)|~(rpoint(X35)))|~(rR(X33,X32,X34))))))&(~(X32=X34)|((~(X32=X37)|~(rpoint(X37)))|((~(X33=X36)|~(rpoint(X36)))|((~(X34=X35)|~(rpoint(X35)))|~(rR(X33,X32,X34)))))))&(~(X32=X33)|((~(X32=X37)|~(rpoint(X37)))|((~(X33=X36)|~(rpoint(X36)))|((~(X34=X35)|~(rpoint(X35)))|~(rR(X33,X32,X34)))))))&(rR(X33,X34,X32)|((~(X32=X37)|~(rpoint(X37)))|((~(X33=X36)|~(rpoint(X36)))|((~(X34=X35)|~(rpoint(X35)))|~(rR(X33,X32,X34))))))),inference(distribute,[status(thm)],[190])).
% cnf(192,plain,(rR(X1,X3,X2)|~rR(X1,X2,X3)|~rpoint(X4)|X3!=X4|~rpoint(X5)|X1!=X5|~rpoint(X6)|X2!=X6),inference(split_conjunct,[status(thm)],[191])).
% cnf(196,plain,(vf(vd1199,vd1200)=vf(vd1185,vd1186)),inference(split_conjunct,[status(thm)],[8])).
% cnf(272,plain,(vd1200=vd1186),inference(split_conjunct,[status(thm)],[19])).
% cnf(273,plain,(ron(vd1185,vd1197)),inference(split_conjunct,[status(thm)],[20])).
% cnf(275,plain,(ron(vd1186,vd1197)),inference(split_conjunct,[status(thm)],[22])).
% fof(276, plain,?[X94]:(vd1200=X94&rpoint(X94)),inference(variable_rename,[status(thm)],[23])).
% fof(277, plain,(vd1200=esk11_0&rpoint(esk11_0)),inference(skolemize,[status(esa)],[276])).
% cnf(278,plain,(rpoint(esk11_0)),inference(split_conjunct,[status(thm)],[277])).
% cnf(279,plain,(vd1200=esk11_0),inference(split_conjunct,[status(thm)],[277])).
% fof(280, plain,![X94]:![X95]:((![X96]:(~(X95=X96)|~(rpoint(X96)))|![X97]:(~(X94=X97)|~(rpoint(X97))))|vf(X94,X95)=vf(X95,X94)),inference(fof_nnf,[status(thm)],[24])).
% fof(281, plain,![X98]:![X99]:((![X100]:(~(X99=X100)|~(rpoint(X100)))|![X101]:(~(X98=X101)|~(rpoint(X101))))|vf(X98,X99)=vf(X99,X98)),inference(variable_rename,[status(thm)],[280])).
% fof(282, plain,![X98]:![X99]:![X100]:![X101]:(((~(X98=X101)|~(rpoint(X101)))|(~(X99=X100)|~(rpoint(X100))))|vf(X98,X99)=vf(X99,X98)),inference(shift_quantors,[status(thm)],[281])).
% cnf(283,plain,(vf(X1,X2)=vf(X2,X1)|~rpoint(X3)|X2!=X3|~rpoint(X4)|X1!=X4),inference(split_conjunct,[status(thm)],[282])).
% cnf(284,plain,(ron(vd1199,vd1197)),inference(split_conjunct,[status(thm)],[25])).
% fof(287, plain,![X98]:![X99]:![X100]:![X101]:![X102]:(((((((((((~(X101=X102)|~(ron(X100,X101)))|~(ron(X99,X101)))|~(ron(X98,X101)))|~(rline(X102)))|X99=X100)|X98=X100)|X98=X99)|![X103]:(~(X100=X103)|~(rpoint(X103))))|![X104]:(~(X99=X104)|~(rpoint(X104))))|![X105]:(~(X98=X105)|~(rpoint(X105))))|((rR(X99,X98,X100)|rR(X98,X99,X100))|rR(X100,X98,X99))),inference(fof_nnf,[status(thm)],[28])).
% fof(288, plain,![X106]:![X107]:![X108]:![X109]:![X110]:(((((((((((~(X109=X110)|~(ron(X108,X109)))|~(ron(X107,X109)))|~(ron(X106,X109)))|~(rline(X110)))|X107=X108)|X106=X108)|X106=X107)|![X111]:(~(X108=X111)|~(rpoint(X111))))|![X112]:(~(X107=X112)|~(rpoint(X112))))|![X113]:(~(X106=X113)|~(rpoint(X113))))|((rR(X107,X106,X108)|rR(X106,X107,X108))|rR(X108,X106,X107))),inference(variable_rename,[status(thm)],[287])).
% fof(289, plain,![X106]:![X107]:![X108]:![X109]:![X110]:![X111]:![X112]:![X113]:(((~(X106=X113)|~(rpoint(X113)))|((~(X107=X112)|~(rpoint(X112)))|((~(X108=X111)|~(rpoint(X111)))|(((((((~(X109=X110)|~(ron(X108,X109)))|~(ron(X107,X109)))|~(ron(X106,X109)))|~(rline(X110)))|X107=X108)|X106=X108)|X106=X107))))|((rR(X107,X106,X108)|rR(X106,X107,X108))|rR(X108,X106,X107))),inference(shift_quantors,[status(thm)],[288])).
% cnf(290,plain,(rR(X1,X2,X3)|rR(X2,X3,X1)|rR(X3,X2,X1)|X2=X3|X2=X1|X3=X1|~rline(X4)|~ron(X2,X5)|~ron(X3,X5)|~ron(X1,X5)|X5!=X4|~rpoint(X6)|X1!=X6|~rpoint(X7)|X3!=X7|~rpoint(X8)|X2!=X8),inference(split_conjunct,[status(thm)],[289])).
% fof(307, plain,![X131]:![X132]:![X133]:![X134]:(((((((X133=X134|~(ron(X134,X131)))|~(ron(X133,X131)))|![X135]:(~(X134=X135)|~(rpoint(X135))))|![X136]:(~(X133=X136)|~(rpoint(X136))))|~(X131=X132))|~(rline(X132)))|?[X137]:(rR(X134,X133,X137)&rpoint(X137))),inference(fof_nnf,[status(thm)],[32])).
% fof(308, plain,![X138]:![X139]:![X140]:![X141]:(((((((X140=X141|~(ron(X141,X138)))|~(ron(X140,X138)))|![X142]:(~(X141=X142)|~(rpoint(X142))))|![X143]:(~(X140=X143)|~(rpoint(X143))))|~(X138=X139))|~(rline(X139)))|?[X144]:(rR(X141,X140,X144)&rpoint(X144))),inference(variable_rename,[status(thm)],[307])).
% fof(309, plain,![X138]:![X139]:![X140]:![X141]:(((((((X140=X141|~(ron(X141,X138)))|~(ron(X140,X138)))|![X142]:(~(X141=X142)|~(rpoint(X142))))|![X143]:(~(X140=X143)|~(rpoint(X143))))|~(X138=X139))|~(rline(X139)))|(rR(X141,X140,esk13_4(X138,X139,X140,X141))&rpoint(esk13_4(X138,X139,X140,X141)))),inference(skolemize,[status(esa)],[308])).
% fof(310, plain,![X138]:![X139]:![X140]:![X141]:![X142]:![X143]:(((((~(X140=X143)|~(rpoint(X143)))|((~(X141=X142)|~(rpoint(X142)))|((X140=X141|~(ron(X141,X138)))|~(ron(X140,X138)))))|~(X138=X139))|~(rline(X139)))|(rR(X141,X140,esk13_4(X138,X139,X140,X141))&rpoint(esk13_4(X138,X139,X140,X141)))),inference(shift_quantors,[status(thm)],[309])).
% fof(311, plain,![X138]:![X139]:![X140]:![X141]:![X142]:![X143]:((rR(X141,X140,esk13_4(X138,X139,X140,X141))|((((~(X140=X143)|~(rpoint(X143)))|((~(X141=X142)|~(rpoint(X142)))|((X140=X141|~(ron(X141,X138)))|~(ron(X140,X138)))))|~(X138=X139))|~(rline(X139))))&(rpoint(esk13_4(X138,X139,X140,X141))|((((~(X140=X143)|~(rpoint(X143)))|((~(X141=X142)|~(rpoint(X142)))|((X140=X141|~(ron(X141,X138)))|~(ron(X140,X138)))))|~(X138=X139))|~(rline(X139))))),inference(distribute,[status(thm)],[310])).
% cnf(312,plain,(X3=X4|rpoint(esk13_4(X2,X1,X3,X4))|~rline(X1)|X2!=X1|~ron(X3,X2)|~ron(X4,X2)|~rpoint(X5)|X4!=X5|~rpoint(X6)|X3!=X6),inference(split_conjunct,[status(thm)],[311])).
% cnf(313,plain,(X3=X4|rR(X4,X3,esk13_4(X2,X1,X3,X4))|~rline(X1)|X2!=X1|~ron(X3,X2)|~ron(X4,X2)|~rpoint(X5)|X4!=X5|~rpoint(X6)|X3!=X6),inference(split_conjunct,[status(thm)],[311])).
% fof(331, plain,![X158]:![X159]:![X160]:![X161]:(((((((X160=X161|~(ron(X161,X158)))|~(ron(X160,X158)))|![X162]:(~(X161=X162)|~(rpoint(X162))))|![X163]:(~(X160=X163)|~(rpoint(X163))))|~(X158=X159))|~(rline(X159)))|?[X164]:(rR(X164,X160,X161)&rpoint(X164))),inference(fof_nnf,[status(thm)],[35])).
% fof(332, plain,![X165]:![X166]:![X167]:![X168]:(((((((X167=X168|~(ron(X168,X165)))|~(ron(X167,X165)))|![X169]:(~(X168=X169)|~(rpoint(X169))))|![X170]:(~(X167=X170)|~(rpoint(X170))))|~(X165=X166))|~(rline(X166)))|?[X171]:(rR(X171,X167,X168)&rpoint(X171))),inference(variable_rename,[status(thm)],[331])).
% fof(333, plain,![X165]:![X166]:![X167]:![X168]:(((((((X167=X168|~(ron(X168,X165)))|~(ron(X167,X165)))|![X169]:(~(X168=X169)|~(rpoint(X169))))|![X170]:(~(X167=X170)|~(rpoint(X170))))|~(X165=X166))|~(rline(X166)))|(rR(esk16_4(X165,X166,X167,X168),X167,X168)&rpoint(esk16_4(X165,X166,X167,X168)))),inference(skolemize,[status(esa)],[332])).
% fof(334, plain,![X165]:![X166]:![X167]:![X168]:![X169]:![X170]:(((((~(X167=X170)|~(rpoint(X170)))|((~(X168=X169)|~(rpoint(X169)))|((X167=X168|~(ron(X168,X165)))|~(ron(X167,X165)))))|~(X165=X166))|~(rline(X166)))|(rR(esk16_4(X165,X166,X167,X168),X167,X168)&rpoint(esk16_4(X165,X166,X167,X168)))),inference(shift_quantors,[status(thm)],[333])).
% fof(335, plain,![X165]:![X166]:![X167]:![X168]:![X169]:![X170]:((rR(esk16_4(X165,X166,X167,X168),X167,X168)|((((~(X167=X170)|~(rpoint(X170)))|((~(X168=X169)|~(rpoint(X169)))|((X167=X168|~(ron(X168,X165)))|~(ron(X167,X165)))))|~(X165=X166))|~(rline(X166))))&(rpoint(esk16_4(X165,X166,X167,X168))|((((~(X167=X170)|~(rpoint(X170)))|((~(X168=X169)|~(rpoint(X169)))|((X167=X168|~(ron(X168,X165)))|~(ron(X167,X165)))))|~(X165=X166))|~(rline(X166))))),inference(distribute,[status(thm)],[334])).
% cnf(336,plain,(X3=X4|rpoint(esk16_4(X2,X1,X3,X4))|~rline(X1)|X2!=X1|~ron(X3,X2)|~ron(X4,X2)|~rpoint(X5)|X4!=X5|~rpoint(X6)|X3!=X6),inference(split_conjunct,[status(thm)],[335])).
% cnf(337,plain,(X3=X4|rR(esk16_4(X2,X1,X3,X4),X3,X4)|~rline(X1)|X2!=X1|~ron(X3,X2)|~ron(X4,X2)|~rpoint(X5)|X4!=X5|~rpoint(X6)|X3!=X6),inference(split_conjunct,[status(thm)],[335])).
% cnf(416,plain,(rline(vd1197)),inference(split_conjunct,[status(thm)],[52])).
% fof(453, plain,![X324]:![X325]:![X326]:((((~(rR(X325,X324,X326))|![X327]:(~(X326=X327)|~(rpoint(X327))))|![X328]:(~(X325=X328)|~(rpoint(X328))))|![X329]:(~(X324=X329)|~(rpoint(X329))))|vplus(vf(X324,X325),vf(X325,X326))=vf(X324,X326)),inference(fof_nnf,[status(thm)],[60])).
% fof(454, plain,![X330]:![X331]:![X332]:((((~(rR(X331,X330,X332))|![X333]:(~(X332=X333)|~(rpoint(X333))))|![X334]:(~(X331=X334)|~(rpoint(X334))))|![X335]:(~(X330=X335)|~(rpoint(X335))))|vplus(vf(X330,X331),vf(X331,X332))=vf(X330,X332)),inference(variable_rename,[status(thm)],[453])).
% fof(455, plain,![X330]:![X331]:![X332]:![X333]:![X334]:![X335]:(((~(X330=X335)|~(rpoint(X335)))|((~(X331=X334)|~(rpoint(X334)))|((~(X332=X333)|~(rpoint(X333)))|~(rR(X331,X330,X332)))))|vplus(vf(X330,X331),vf(X331,X332))=vf(X330,X332)),inference(shift_quantors,[status(thm)],[454])).
% cnf(456,plain,(vplus(vf(X1,X2),vf(X2,X3))=vf(X1,X3)|~rR(X2,X1,X3)|~rpoint(X4)|X3!=X4|~rpoint(X5)|X2!=X5|~rpoint(X6)|X1!=X6),inference(split_conjunct,[status(thm)],[455])).
% fof(533, plain,![X441]:![X442]:((![X443]:(~(X442=X443)|~(rpoint(X443)))|![X444]:(~(X441=X444)|~(rpoint(X444))))|?[X445]:(vf(X441,X442)=X445&rreal(X445))),inference(fof_nnf,[status(thm)],[75])).
% fof(534, plain,![X446]:![X447]:((![X448]:(~(X447=X448)|~(rpoint(X448)))|![X449]:(~(X446=X449)|~(rpoint(X449))))|?[X450]:(vf(X446,X447)=X450&rreal(X450))),inference(variable_rename,[status(thm)],[533])).
% fof(535, plain,![X446]:![X447]:((![X448]:(~(X447=X448)|~(rpoint(X448)))|![X449]:(~(X446=X449)|~(rpoint(X449))))|(vf(X446,X447)=esk28_2(X446,X447)&rreal(esk28_2(X446,X447)))),inference(skolemize,[status(esa)],[534])).
% fof(536, plain,![X446]:![X447]:![X448]:![X449]:(((~(X446=X449)|~(rpoint(X449)))|(~(X447=X448)|~(rpoint(X448))))|(vf(X446,X447)=esk28_2(X446,X447)&rreal(esk28_2(X446,X447)))),inference(shift_quantors,[status(thm)],[535])).
% fof(537, plain,![X446]:![X447]:![X448]:![X449]:((vf(X446,X447)=esk28_2(X446,X447)|((~(X446=X449)|~(rpoint(X449)))|(~(X447=X448)|~(rpoint(X448)))))&(rreal(esk28_2(X446,X447))|((~(X446=X449)|~(rpoint(X449)))|(~(X447=X448)|~(rpoint(X448)))))),inference(distribute,[status(thm)],[536])).
% cnf(538,plain,(rreal(esk28_2(X4,X2))|~rpoint(X1)|X2!=X1|~rpoint(X3)|X4!=X3),inference(split_conjunct,[status(thm)],[537])).
% cnf(539,plain,(vf(X4,X2)=esk28_2(X4,X2)|~rpoint(X1)|X2!=X1|~rpoint(X3)|X4!=X3),inference(split_conjunct,[status(thm)],[537])).
% fof(599, plain,![X506]:![X507]:((![X508]:(~(X507=X508)|~(rpoint(X508)))|![X509]:(~(X506=X509)|~(rpoint(X509))))|((~(vf(X506,X507)=v0)|X506=X507)&(~(X506=X507)|vf(X506,X507)=v0))),inference(fof_nnf,[status(thm)],[81])).
% fof(600, plain,![X510]:![X511]:((![X512]:(~(X511=X512)|~(rpoint(X512)))|![X513]:(~(X510=X513)|~(rpoint(X513))))|((~(vf(X510,X511)=v0)|X510=X511)&(~(X510=X511)|vf(X510,X511)=v0))),inference(variable_rename,[status(thm)],[599])).
% fof(601, plain,![X510]:![X511]:![X512]:![X513]:(((~(X510=X513)|~(rpoint(X513)))|(~(X511=X512)|~(rpoint(X512))))|((~(vf(X510,X511)=v0)|X510=X511)&(~(X510=X511)|vf(X510,X511)=v0))),inference(shift_quantors,[status(thm)],[600])).
% fof(602, plain,![X510]:![X511]:![X512]:![X513]:(((~(vf(X510,X511)=v0)|X510=X511)|((~(X510=X513)|~(rpoint(X513)))|(~(X511=X512)|~(rpoint(X512)))))&((~(X510=X511)|vf(X510,X511)=v0)|((~(X510=X513)|~(rpoint(X513)))|(~(X511=X512)|~(rpoint(X512)))))),inference(distribute,[status(thm)],[601])).
% cnf(603,plain,(vf(X4,X2)=v0|~rpoint(X1)|X2!=X1|~rpoint(X3)|X4!=X3|X4!=X2),inference(split_conjunct,[status(thm)],[602])).
% cnf(604,plain,(X4=X2|~rpoint(X1)|X2!=X1|~rpoint(X3)|X4!=X3|vf(X4,X2)!=v0),inference(split_conjunct,[status(thm)],[602])).
% fof(621, plain,((((((((((((![X518]:(((~(ron(vd1187,X518))|~(ron(vd1186,X518)))|~(ron(vd1185,X518)))|~(rline(X518)))&vangle(vd1179,vd1178,vd1180)=vangle(vd1186,vd1185,vd1187))&vf(vd1178,vd1180)=vf(vd1185,vd1187))&vf(vd1178,vd1179)=vf(vd1185,vd1186))&?[X519]:(vd1187=X519&rpoint(X519)))&?[X520]:(vd1186=X520&rpoint(X520)))&?[X521]:(vd1185=X521&rpoint(X521)))&~(vd1179=vd1180))&~(vd1178=vd1180))&~(vd1178=vd1179))&?[X522]:(vd1180=X522&rpoint(X522)))&?[X523]:(vd1179=X523&rpoint(X523)))&?[X524]:(vd1178=X524&rpoint(X524))),inference(fof_nnf,[status(thm)],[86])).
% fof(622, plain,((((((((((((![X525]:(((~(ron(vd1187,X525))|~(ron(vd1186,X525)))|~(ron(vd1185,X525)))|~(rline(X525)))&vangle(vd1179,vd1178,vd1180)=vangle(vd1186,vd1185,vd1187))&vf(vd1178,vd1180)=vf(vd1185,vd1187))&vf(vd1178,vd1179)=vf(vd1185,vd1186))&?[X526]:(vd1187=X526&rpoint(X526)))&?[X527]:(vd1186=X527&rpoint(X527)))&?[X528]:(vd1185=X528&rpoint(X528)))&~(vd1179=vd1180))&~(vd1178=vd1180))&~(vd1178=vd1179))&?[X529]:(vd1180=X529&rpoint(X529)))&?[X530]:(vd1179=X530&rpoint(X530)))&?[X531]:(vd1178=X531&rpoint(X531))),inference(variable_rename,[status(thm)],[621])).
% fof(623, plain,((((((((((((![X525]:(((~(ron(vd1187,X525))|~(ron(vd1186,X525)))|~(ron(vd1185,X525)))|~(rline(X525)))&vangle(vd1179,vd1178,vd1180)=vangle(vd1186,vd1185,vd1187))&vf(vd1178,vd1180)=vf(vd1185,vd1187))&vf(vd1178,vd1179)=vf(vd1185,vd1186))&(vd1187=esk35_0&rpoint(esk35_0)))&(vd1186=esk36_0&rpoint(esk36_0)))&(vd1185=esk37_0&rpoint(esk37_0)))&~(vd1179=vd1180))&~(vd1178=vd1180))&~(vd1178=vd1179))&(vd1180=esk38_0&rpoint(esk38_0)))&(vd1179=esk39_0&rpoint(esk39_0)))&(vd1178=esk40_0&rpoint(esk40_0))),inference(skolemize,[status(esa)],[622])).
% fof(624, plain,![X525]:(((((((((((((((~(ron(vd1187,X525))|~(ron(vd1186,X525)))|~(ron(vd1185,X525)))|~(rline(X525)))&vangle(vd1179,vd1178,vd1180)=vangle(vd1186,vd1185,vd1187))&vf(vd1178,vd1180)=vf(vd1185,vd1187))&vf(vd1178,vd1179)=vf(vd1185,vd1186))&(vd1187=esk35_0&rpoint(esk35_0)))&(vd1186=esk36_0&rpoint(esk36_0)))&(vd1185=esk37_0&rpoint(esk37_0)))&~(vd1179=vd1180))&~(vd1178=vd1180))&~(vd1178=vd1179))&(vd1180=esk38_0&rpoint(esk38_0)))&(vd1179=esk39_0&rpoint(esk39_0)))&(vd1178=esk40_0&rpoint(esk40_0))),inference(shift_quantors,[status(thm)],[623])).
% cnf(625,plain,(rpoint(esk40_0)),inference(split_conjunct,[status(thm)],[624])).
% cnf(626,plain,(vd1178=esk40_0),inference(split_conjunct,[status(thm)],[624])).
% cnf(627,plain,(rpoint(esk39_0)),inference(split_conjunct,[status(thm)],[624])).
% cnf(628,plain,(vd1179=esk39_0),inference(split_conjunct,[status(thm)],[624])).
% cnf(634,plain,(rpoint(esk37_0)),inference(split_conjunct,[status(thm)],[624])).
% cnf(635,plain,(vd1185=esk37_0),inference(split_conjunct,[status(thm)],[624])).
% cnf(640,plain,(vf(vd1178,vd1179)=vf(vd1185,vd1186)),inference(split_conjunct,[status(thm)],[624])).
% fof(653, plain,![X534]:![X535]:![X536]:![X537]:((((~(ron(X535,X537))|~(rcenter(X536,X537)))|![X538]:(~(X535=X538)|~(rpoint(X538))))|![X539]:(~(X534=X539)|~(rpoint(X539))))|((~(rless(vf(X536,X534),vf(X536,X535)))|rinside(X534,X537))&(~(rinside(X534,X537))|rless(vf(X536,X534),vf(X536,X535))))),inference(fof_nnf,[status(thm)],[91])).
% fof(654, plain,![X540]:![X541]:![X542]:![X543]:((((~(ron(X541,X543))|~(rcenter(X542,X543)))|![X544]:(~(X541=X544)|~(rpoint(X544))))|![X545]:(~(X540=X545)|~(rpoint(X545))))|((~(rless(vf(X542,X540),vf(X542,X541)))|rinside(X540,X543))&(~(rinside(X540,X543))|rless(vf(X542,X540),vf(X542,X541))))),inference(variable_rename,[status(thm)],[653])).
% fof(655, plain,![X540]:![X541]:![X542]:![X543]:![X544]:![X545]:(((~(X540=X545)|~(rpoint(X545)))|((~(X541=X544)|~(rpoint(X544)))|(~(ron(X541,X543))|~(rcenter(X542,X543)))))|((~(rless(vf(X542,X540),vf(X542,X541)))|rinside(X540,X543))&(~(rinside(X540,X543))|rless(vf(X542,X540),vf(X542,X541))))),inference(shift_quantors,[status(thm)],[654])).
% fof(656, plain,![X540]:![X541]:![X542]:![X543]:![X544]:![X545]:(((~(rless(vf(X542,X540),vf(X542,X541)))|rinside(X540,X543))|((~(X540=X545)|~(rpoint(X545)))|((~(X541=X544)|~(rpoint(X544)))|(~(ron(X541,X543))|~(rcenter(X542,X543))))))&((~(rinside(X540,X543))|rless(vf(X542,X540),vf(X542,X541)))|((~(X540=X545)|~(rpoint(X545)))|((~(X541=X544)|~(rpoint(X544)))|(~(ron(X541,X543))|~(rcenter(X542,X543))))))),inference(distribute,[status(thm)],[655])).
% cnf(658,plain,(rinside(X6,X2)|~rcenter(X1,X2)|~ron(X3,X2)|~rpoint(X4)|X3!=X4|~rpoint(X5)|X6!=X5|~rless(vf(X1,X6),vf(X1,X3))),inference(split_conjunct,[status(thm)],[656])).
% fof(695, plain,![X577]:![X578]:![X579]:![X580]:![X581]:![X582]:((((((~(ron(X581,X580))|~(X581=X582))|~(rpoint(X582)))|~(rcenter(X579,X580)))|~(X577=X578))|~(rpoint(X578)))|((~(vf(X579,X577)=vf(X579,X581))|ron(X577,X580))&(~(ron(X577,X580))|vf(X579,X577)=vf(X579,X581)))),inference(fof_nnf,[status(thm)],[101])).
% fof(696, plain,![X583]:![X584]:![X585]:![X586]:![X587]:![X588]:((((((~(ron(X587,X586))|~(X587=X588))|~(rpoint(X588)))|~(rcenter(X585,X586)))|~(X583=X584))|~(rpoint(X584)))|((~(vf(X585,X583)=vf(X585,X587))|ron(X583,X586))&(~(ron(X583,X586))|vf(X585,X583)=vf(X585,X587)))),inference(variable_rename,[status(thm)],[695])).
% fof(697, plain,![X583]:![X584]:![X585]:![X586]:![X587]:![X588]:(((~(vf(X585,X583)=vf(X585,X587))|ron(X583,X586))|(((((~(ron(X587,X586))|~(X587=X588))|~(rpoint(X588)))|~(rcenter(X585,X586)))|~(X583=X584))|~(rpoint(X584))))&((~(ron(X583,X586))|vf(X585,X583)=vf(X585,X587))|(((((~(ron(X587,X586))|~(X587=X588))|~(rpoint(X588)))|~(rcenter(X585,X586)))|~(X583=X584))|~(rpoint(X584))))),inference(distribute,[status(thm)],[696])).
% cnf(698,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)],[697])).
% cnf(699,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)],[697])).
% fof(736, plain,![X634]:![X635]:![X636]:![X637]:![X638]:![X639]:(((((((~(vplus(X634,X638)=vplus(X636,X638))|~(X638=X639))|~(rreal(X639)))|~(X636=X637))|~(rreal(X637)))|~(X634=X635))|~(rreal(X635)))|X634=X636),inference(fof_nnf,[status(thm)],[110])).
% fof(737, plain,![X640]:![X641]:![X642]:![X643]:![X644]:![X645]:(((((((~(vplus(X640,X644)=vplus(X642,X644))|~(X644=X645))|~(rreal(X645)))|~(X642=X643))|~(rreal(X643)))|~(X640=X641))|~(rreal(X641)))|X640=X642),inference(variable_rename,[status(thm)],[736])).
% cnf(738,plain,(X1=X2|~rreal(X3)|X1!=X3|~rreal(X4)|X2!=X4|~rreal(X5)|X6!=X5|vplus(X1,X6)!=vplus(X2,X6)),inference(split_conjunct,[status(thm)],[737])).
% fof(745, plain,![X652]:![X653]:![X654]:![X655]:((((~(X654=X655)|~(rreal(X655)))|~(X652=X653))|~(rreal(X653)))|((rless(X652,X654)|X652=X654)|rless(X654,X652))),inference(fof_nnf,[status(thm)],[113])).
% fof(746, plain,![X656]:![X657]:![X658]:![X659]:((((~(X658=X659)|~(rreal(X659)))|~(X656=X657))|~(rreal(X657)))|((rless(X656,X658)|X656=X658)|rless(X658,X656))),inference(variable_rename,[status(thm)],[745])).
% cnf(747,plain,(rless(X1,X2)|X2=X1|rless(X2,X1)|~rreal(X3)|X2!=X3|~rreal(X4)|X1!=X4),inference(split_conjunct,[status(thm)],[746])).
% fof(748, plain,![X656]:![X657]:![X658]:![X659]:((((~(X658=X659)|~(rreal(X659)))|~(X656=X657))|~(rreal(X657)))|vplus(X656,X658)=vplus(X658,X656)),inference(fof_nnf,[status(thm)],[114])).
% fof(749, plain,![X660]:![X661]:![X662]:![X663]:((((~(X662=X663)|~(rreal(X663)))|~(X660=X661))|~(rreal(X661)))|vplus(X660,X662)=vplus(X662,X660)),inference(variable_rename,[status(thm)],[748])).
% cnf(750,plain,(vplus(X1,X2)=vplus(X2,X1)|~rreal(X3)|X1!=X3|~rreal(X4)|X2!=X4),inference(split_conjunct,[status(thm)],[749])).
% fof(751, plain,![X660]:![X661]:![X662]:![X663]:((((~(X662=X663)|~(rreal(X663)))|~(X660=X661))|~(rreal(X661)))|?[X664]:(vplus(X660,X662)=X664&rreal(X664))),inference(fof_nnf,[status(thm)],[115])).
% fof(752, plain,![X665]:![X666]:![X667]:![X668]:((((~(X667=X668)|~(rreal(X668)))|~(X665=X666))|~(rreal(X666)))|?[X669]:(vplus(X665,X667)=X669&rreal(X669))),inference(variable_rename,[status(thm)],[751])).
% fof(753, plain,![X665]:![X666]:![X667]:![X668]:((((~(X667=X668)|~(rreal(X668)))|~(X665=X666))|~(rreal(X666)))|(vplus(X665,X667)=esk47_4(X665,X666,X667,X668)&rreal(esk47_4(X665,X666,X667,X668)))),inference(skolemize,[status(esa)],[752])).
% fof(754, plain,![X665]:![X666]:![X667]:![X668]:((vplus(X665,X667)=esk47_4(X665,X666,X667,X668)|(((~(X667=X668)|~(rreal(X668)))|~(X665=X666))|~(rreal(X666))))&(rreal(esk47_4(X665,X666,X667,X668))|(((~(X667=X668)|~(rreal(X668)))|~(X665=X666))|~(rreal(X666))))),inference(distribute,[status(thm)],[753])).
% cnf(755,plain,(rreal(esk47_4(X2,X1,X4,X3))|~rreal(X1)|X2!=X1|~rreal(X3)|X4!=X3),inference(split_conjunct,[status(thm)],[754])).
% cnf(756,plain,(vplus(X2,X4)=esk47_4(X2,X1,X4,X3)|~rreal(X1)|X2!=X1|~rreal(X3)|X4!=X3),inference(split_conjunct,[status(thm)],[754])).
% fof(765, plain,![X673]:![X674]:![X675]:![X676]:(((((~(rinside(X673,X675))|~(X675=X676))|~(rcircle(X676)))|~(X673=X674))|~(rpoint(X674)))|~(ron(X673,X675))),inference(fof_nnf,[status(thm)],[168])).
% fof(766, plain,![X677]:![X678]:![X679]:![X680]:(((((~(rinside(X677,X679))|~(X679=X680))|~(rcircle(X680)))|~(X677=X678))|~(rpoint(X678)))|~(ron(X677,X679))),inference(variable_rename,[status(thm)],[765])).
% cnf(767,plain,(~ron(X1,X2)|~rpoint(X3)|X1!=X3|~rcircle(X4)|X2!=X4|~rinside(X1,X2)),inference(split_conjunct,[status(thm)],[766])).
% fof(780, plain,![X683]:![X684]:(((X683=X684|![X685]:(~(X684=X685)|~(rpoint(X685))))|![X686]:(~(X683=X686)|~(rpoint(X686))))|?[X687]:((ron(X684,X687)&rcenter(X683,X687))&rcircle(X687))),inference(fof_nnf,[status(thm)],[121])).
% fof(781, plain,![X688]:![X689]:(((X688=X689|![X690]:(~(X689=X690)|~(rpoint(X690))))|![X691]:(~(X688=X691)|~(rpoint(X691))))|?[X692]:((ron(X689,X692)&rcenter(X688,X692))&rcircle(X692))),inference(variable_rename,[status(thm)],[780])).
% fof(782, plain,![X688]:![X689]:(((X688=X689|![X690]:(~(X689=X690)|~(rpoint(X690))))|![X691]:(~(X688=X691)|~(rpoint(X691))))|((ron(X689,esk50_2(X688,X689))&rcenter(X688,esk50_2(X688,X689)))&rcircle(esk50_2(X688,X689)))),inference(skolemize,[status(esa)],[781])).
% fof(783, plain,![X688]:![X689]:![X690]:![X691]:(((~(X688=X691)|~(rpoint(X691)))|((~(X689=X690)|~(rpoint(X690)))|X688=X689))|((ron(X689,esk50_2(X688,X689))&rcenter(X688,esk50_2(X688,X689)))&rcircle(esk50_2(X688,X689)))),inference(shift_quantors,[status(thm)],[782])).
% fof(784, plain,![X688]:![X689]:![X690]:![X691]:(((ron(X689,esk50_2(X688,X689))|((~(X688=X691)|~(rpoint(X691)))|((~(X689=X690)|~(rpoint(X690)))|X688=X689)))&(rcenter(X688,esk50_2(X688,X689))|((~(X688=X691)|~(rpoint(X691)))|((~(X689=X690)|~(rpoint(X690)))|X688=X689))))&(rcircle(esk50_2(X688,X689))|((~(X688=X691)|~(rpoint(X691)))|((~(X689=X690)|~(rpoint(X690)))|X688=X689)))),inference(distribute,[status(thm)],[783])).
% cnf(785,plain,(X1=X2|rcircle(esk50_2(X1,X2))|~rpoint(X3)|X2!=X3|~rpoint(X4)|X1!=X4),inference(split_conjunct,[status(thm)],[784])).
% cnf(786,plain,(X1=X2|rcenter(X1,esk50_2(X1,X2))|~rpoint(X3)|X2!=X3|~rpoint(X4)|X1!=X4),inference(split_conjunct,[status(thm)],[784])).
% cnf(787,plain,(X1=X2|ron(X2,esk50_2(X1,X2))|~rpoint(X3)|X2!=X3|~rpoint(X4)|X1!=X4),inference(split_conjunct,[status(thm)],[784])).
% fof(854, negated_conjecture,(~(rR(vd1199,vd1185,vd1186))&~(rR(vd1185,vd1199,vd1186))),inference(fof_nnf,[status(thm)],[136])).
% cnf(855,negated_conjecture,(~rR(vd1185,vd1199,vd1186)),inference(split_conjunct,[status(thm)],[854])).
% cnf(856,negated_conjecture,(~rR(vd1199,vd1185,vd1186)),inference(split_conjunct,[status(thm)],[854])).
% cnf(857,plain,(esk11_0=vd1186),inference(rw,[status(thm)],[279,272,theory(equality)])).
% cnf(858,plain,(rpoint(vd1199)),inference(rw,[status(thm)],[174,175,theory(equality)])).
% cnf(859,plain,(rpoint(vd1186)),inference(rw,[status(thm)],[278,857,theory(equality)])).
% cnf(862,plain,(rpoint(vd1185)),inference(rw,[status(thm)],[634,635,theory(equality)])).
% cnf(864,plain,(rpoint(vd1179)),inference(rw,[status(thm)],[627,628,theory(equality)])).
% cnf(865,plain,(rpoint(vd1178)),inference(rw,[status(thm)],[625,626,theory(equality)])).
% cnf(872,plain,(vf(vd1185,vd1186)=vf(vd1199,vd1186)),inference(rw,[status(thm)],[196,272,theory(equality)])).
% cnf(873,plain,(vf(vd1178,vd1179)=vf(vd1199,vd1186)),inference(rw,[status(thm)],[640,872,theory(equality)])).
% cnf(895,plain,(vf(X1,X2)=v0|X2!=X1|X3!=X2|~rpoint(X1)|~rpoint(X3)),inference(er,[status(thm)],[603,theory(equality)])).
% cnf(896,plain,(vf(X1,X1)=v0|X2!=X1|~rpoint(X1)|~rpoint(X2)),inference(er,[status(thm)],[895,theory(equality)])).
% cnf(897,plain,(vf(X1,X1)=v0|~rpoint(X1)),inference(er,[status(thm)],[896,theory(equality)])).
% cnf(913,plain,(X1=X2|vf(X2,X1)!=v0|X3!=X1|~rpoint(X2)|~rpoint(X3)),inference(er,[status(thm)],[604,theory(equality)])).
% cnf(914,plain,(X1=X2|vf(X2,X1)!=v0|~rpoint(X2)|~rpoint(X1)),inference(er,[status(thm)],[913,theory(equality)])).
% cnf(915,plain,(rreal(esk28_2(X1,X2))|X3!=X2|~rpoint(X1)|~rpoint(X3)),inference(er,[status(thm)],[538,theory(equality)])).
% cnf(916,plain,(rreal(esk28_2(X1,X2))|~rpoint(X1)|~rpoint(X2)),inference(er,[status(thm)],[915,theory(equality)])).
% cnf(917,plain,(X1!=X2|~rinside(X1,X3)|~rcircle(X3)|~ron(X1,X3)|~rpoint(X2)),inference(er,[status(thm)],[767,theory(equality)])).
% cnf(918,plain,(~rinside(X1,X2)|~rcircle(X2)|~ron(X1,X2)|~rpoint(X1)),inference(er,[status(thm)],[917,theory(equality)])).
% cnf(929,plain,(vf(X1,X2)=vf(X2,X1)|X1!=X3|~rpoint(X3)|~rpoint(X2)),inference(er,[status(thm)],[283,theory(equality)])).
% cnf(930,plain,(vf(X1,X2)=vf(X2,X1)|~rpoint(X1)|~rpoint(X2)),inference(er,[status(thm)],[929,theory(equality)])).
% cnf(931,plain,(vplus(X1,X2)=vplus(X2,X1)|X1!=X3|~rreal(X2)|~rreal(X3)),inference(er,[status(thm)],[750,theory(equality)])).
% cnf(932,plain,(vplus(X1,X2)=vplus(X2,X1)|~rreal(X2)|~rreal(X1)),inference(er,[status(thm)],[931,theory(equality)])).
% cnf(933,plain,(esk28_2(X1,X2)=vf(X1,X2)|X3!=X2|~rpoint(X1)|~rpoint(X3)),inference(er,[status(thm)],[539,theory(equality)])).
% cnf(934,plain,(esk28_2(X1,X2)=vf(X1,X2)|~rpoint(X1)|~rpoint(X2)),inference(er,[status(thm)],[933,theory(equality)])).
% cnf(952,plain,(X1=X2|rcircle(esk50_2(X1,X2))|X1!=X3|~rpoint(X3)|~rpoint(X2)),inference(er,[status(thm)],[785,theory(equality)])).
% cnf(953,plain,(X1=X2|rcircle(esk50_2(X1,X2))|~rpoint(X1)|~rpoint(X2)),inference(er,[status(thm)],[952,theory(equality)])).
% cnf(954,plain,(X1=X2|rless(X1,X2)|rless(X2,X1)|X1!=X3|~rreal(X3)|~rreal(X2)),inference(er,[status(thm)],[747,theory(equality)])).
% cnf(955,plain,(X1=X2|rless(X1,X2)|rless(X2,X1)|~rreal(X1)|~rreal(X2)),inference(er,[status(thm)],[954,theory(equality)])).
% cnf(956,plain,(rreal(esk47_4(X1,X2,X3,X3))|X2!=X1|~rreal(X3)|~rreal(X2)),inference(er,[status(thm)],[755,theory(equality)])).
% cnf(957,plain,(rreal(esk47_4(X1,X1,X2,X2))|~rreal(X2)|~rreal(X1)),inference(er,[status(thm)],[956,theory(equality)])).
% cnf(977,plain,(X1=X2|ron(X2,esk50_2(X1,X2))|X1!=X3|~rpoint(X3)|~rpoint(X2)),inference(er,[status(thm)],[787,theory(equality)])).
% cnf(978,plain,(X1=X2|ron(X2,esk50_2(X1,X2))|~rpoint(X1)|~rpoint(X2)),inference(er,[status(thm)],[977,theory(equality)])).
% cnf(981,plain,(X1=X2|rcenter(X1,esk50_2(X1,X2))|X1!=X3|~rpoint(X3)|~rpoint(X2)),inference(er,[status(thm)],[786,theory(equality)])).
% cnf(982,plain,(X1=X2|rcenter(X1,esk50_2(X1,X2))|~rpoint(X1)|~rpoint(X2)),inference(er,[status(thm)],[981,theory(equality)])).
% cnf(1004,plain,(esk47_4(X1,X2,X3,X3)=vplus(X1,X3)|X2!=X1|~rreal(X3)|~rreal(X2)),inference(er,[status(thm)],[756,theory(equality)])).
% cnf(1005,plain,(esk47_4(X1,X1,X2,X2)=vplus(X1,X2)|~rreal(X2)|~rreal(X1)),inference(er,[status(thm)],[1004,theory(equality)])).
% cnf(1006,plain,(X1=X2|vplus(X1,X3)!=vplus(X2,X3)|X2!=X4|X1!=X5|~rreal(X3)|~rreal(X4)|~rreal(X5)),inference(er,[status(thm)],[738,theory(equality)])).
% cnf(1007,plain,(X1=X2|vplus(X1,X3)!=vplus(X2,X3)|X1!=X4|~rreal(X3)|~rreal(X2)|~rreal(X4)),inference(er,[status(thm)],[1006,theory(equality)])).
% cnf(1008,plain,(X1=X2|vplus(X1,X3)!=vplus(X2,X3)|~rreal(X3)|~rreal(X2)|~rreal(X1)),inference(er,[status(thm)],[1007,theory(equality)])).
% cnf(1009,plain,(rR(X1,X2,X3)|X3!=X4|X1!=X5|~rpoint(X4)|~rpoint(X5)|~rpoint(X2)|~rR(X1,X3,X2)),inference(er,[status(thm)],[192,theory(equality)])).
% cnf(1010,plain,(rR(X1,X2,X3)|X1!=X4|~rpoint(X3)|~rpoint(X4)|~rpoint(X2)|~rR(X1,X3,X2)),inference(er,[status(thm)],[1009,theory(equality)])).
% cnf(1011,plain,(rR(X1,X2,X3)|~rpoint(X3)|~rpoint(X1)|~rpoint(X2)|~rR(X1,X3,X2)),inference(er,[status(thm)],[1010,theory(equality)])).
% cnf(1084,plain,(vf(X1,X2)=vf(X1,X3)|X4!=X2|~rcenter(X1,X5)|~ron(X3,X5)|~ron(X2,X5)|~rpoint(X3)|~rpoint(X4)),inference(er,[status(thm)],[698,theory(equality)])).
% cnf(1085,plain,(vf(X1,X2)=vf(X1,X3)|~rcenter(X1,X4)|~ron(X3,X4)|~ron(X2,X4)|~rpoint(X3)|~rpoint(X2)),inference(er,[status(thm)],[1084,theory(equality)])).
% cnf(1113,plain,(ron(X1,X2)|vf(X3,X1)!=vf(X3,X4)|X5!=X1|~rcenter(X3,X2)|~ron(X4,X2)|~rpoint(X4)|~rpoint(X5)),inference(er,[status(thm)],[699,theory(equality)])).
% cnf(1114,plain,(ron(X1,X2)|vf(X3,X1)!=vf(X3,X4)|~rcenter(X3,X2)|~ron(X4,X2)|~rpoint(X4)|~rpoint(X1)),inference(er,[status(thm)],[1113,theory(equality)])).
% cnf(1128,plain,(rinside(X1,X2)|X3!=X4|~rcenter(X5,X2)|~rless(vf(X5,X1),vf(X5,X3))|~ron(X3,X2)|~rpoint(X1)|~rpoint(X4)),inference(er,[status(thm)],[658,theory(equality)])).
% cnf(1129,plain,(rinside(X1,X2)|~rcenter(X3,X2)|~rless(vf(X3,X1),vf(X3,X4))|~ron(X4,X2)|~rpoint(X1)|~rpoint(X4)),inference(er,[status(thm)],[1128,theory(equality)])).
% cnf(1200,plain,(vplus(vf(X1,X2),vf(X2,X3))=vf(X1,X3)|X2!=X4|X1!=X5|~rpoint(X5)|~rpoint(X4)|~rpoint(X3)|~rR(X2,X1,X3)),inference(er,[status(thm)],[456,theory(equality)])).
% cnf(1201,plain,(vplus(vf(X1,X2),vf(X2,X3))=vf(X1,X3)|X1!=X4|~rpoint(X4)|~rpoint(X2)|~rpoint(X3)|~rR(X2,X1,X3)),inference(er,[status(thm)],[1200,theory(equality)])).
% cnf(1202,plain,(vplus(vf(X1,X2),vf(X2,X3))=vf(X1,X3)|~rpoint(X1)|~rpoint(X2)|~rpoint(X3)|~rR(X2,X1,X3)),inference(er,[status(thm)],[1201,theory(equality)])).
% cnf(1203,plain,(X1=X2|rpoint(esk13_4(X3,X4,X1,X2))|X1!=X5|X4!=X3|~rline(X4)|~ron(X2,X3)|~ron(X1,X3)|~rpoint(X5)|~rpoint(X2)),inference(er,[status(thm)],[312,theory(equality)])).
% cnf(1204,plain,(X1=X2|rpoint(esk13_4(X3,X4,X1,X2))|X4!=X3|~rline(X4)|~ron(X2,X3)|~ron(X1,X3)|~rpoint(X1)|~rpoint(X2)),inference(er,[status(thm)],[1203,theory(equality)])).
% cnf(1205,plain,(X1=X2|rpoint(esk13_4(X3,X3,X1,X2))|~rline(X3)|~ron(X2,X3)|~ron(X1,X3)|~rpoint(X1)|~rpoint(X2)),inference(er,[status(thm)],[1204,theory(equality)])).
% cnf(1206,plain,(X1=X2|rpoint(esk16_4(X3,X4,X1,X2))|X1!=X5|X4!=X3|~rline(X4)|~ron(X2,X3)|~ron(X1,X3)|~rpoint(X5)|~rpoint(X2)),inference(er,[status(thm)],[336,theory(equality)])).
% cnf(1207,plain,(X1=X2|rpoint(esk16_4(X3,X4,X1,X2))|X4!=X3|~rline(X4)|~ron(X2,X3)|~ron(X1,X3)|~rpoint(X1)|~rpoint(X2)),inference(er,[status(thm)],[1206,theory(equality)])).
% cnf(1208,plain,(X1=X2|rpoint(esk16_4(X3,X3,X1,X2))|~rline(X3)|~ron(X2,X3)|~ron(X1,X3)|~rpoint(X1)|~rpoint(X2)),inference(er,[status(thm)],[1207,theory(equality)])).
% cnf(1225,plain,(X1=X2|rR(X2,X1,esk13_4(X3,X4,X1,X2))|X1!=X5|X4!=X3|~rline(X4)|~ron(X2,X3)|~ron(X1,X3)|~rpoint(X5)|~rpoint(X2)),inference(er,[status(thm)],[313,theory(equality)])).
% cnf(1226,plain,(X1=X2|rR(X2,X1,esk13_4(X3,X4,X1,X2))|X4!=X3|~rline(X4)|~ron(X2,X3)|~ron(X1,X3)|~rpoint(X1)|~rpoint(X2)),inference(er,[status(thm)],[1225,theory(equality)])).
% cnf(1227,plain,(X1=X2|rR(X2,X1,esk13_4(X3,X3,X1,X2))|~rline(X3)|~ron(X2,X3)|~ron(X1,X3)|~rpoint(X1)|~rpoint(X2)),inference(er,[status(thm)],[1226,theory(equality)])).
% cnf(1228,plain,(X1=X2|rR(esk16_4(X3,X4,X1,X2),X1,X2)|X1!=X5|X4!=X3|~rline(X4)|~ron(X2,X3)|~ron(X1,X3)|~rpoint(X5)|~rpoint(X2)),inference(er,[status(thm)],[337,theory(equality)])).
% cnf(1229,plain,(X1=X2|rR(esk16_4(X3,X4,X1,X2),X1,X2)|X4!=X3|~rline(X4)|~ron(X2,X3)|~ron(X1,X3)|~rpoint(X1)|~rpoint(X2)),inference(er,[status(thm)],[1228,theory(equality)])).
% cnf(1230,plain,(X1=X2|rR(esk16_4(X3,X3,X1,X2),X1,X2)|~rline(X3)|~ron(X2,X3)|~ron(X1,X3)|~rpoint(X1)|~rpoint(X2)),inference(er,[status(thm)],[1229,theory(equality)])).
% cnf(1448,plain,(X1=X2|X1=X3|X2=X3|rR(X1,X2,X3)|rR(X2,X3,X1)|rR(X3,X2,X1)|X3!=X4|X2!=X5|X1!=X6|~rline(X7)|~ron(X3,X7)|~ron(X2,X7)|~ron(X1,X7)|~rpoint(X5)|~rpoint(X4)|~rpoint(X6)),inference(er,[status(thm)],[290,theory(equality)])).
% cnf(1449,plain,(X1=X2|X1=X3|X2=X3|rR(X1,X2,X3)|rR(X2,X3,X1)|rR(X3,X2,X1)|X2!=X4|X1!=X5|~rline(X6)|~ron(X3,X6)|~ron(X2,X6)|~ron(X1,X6)|~rpoint(X4)|~rpoint(X3)|~rpoint(X5)),inference(er,[status(thm)],[1448,theory(equality)])).
% cnf(1450,plain,(X1=X2|X1=X3|X2=X3|rR(X1,X2,X3)|rR(X2,X3,X1)|rR(X3,X2,X1)|X1!=X4|~rline(X5)|~ron(X3,X5)|~ron(X2,X5)|~ron(X1,X5)|~rpoint(X2)|~rpoint(X3)|~rpoint(X4)),inference(er,[status(thm)],[1449,theory(equality)])).
% cnf(1451,plain,(X1=X2|X1=X3|X2=X3|rR(X1,X2,X3)|rR(X2,X3,X1)|rR(X3,X2,X1)|~rline(X4)|~ron(X3,X4)|~ron(X2,X4)|~ron(X1,X4)|~rpoint(X2)|~rpoint(X3)|~rpoint(X1)),inference(er,[status(thm)],[1450,theory(equality)])).
% cnf(2038,plain,(rreal(vf(X1,X2))|~rpoint(X1)|~rpoint(X2)),inference(spm,[status(thm)],[916,934,theory(equality)])).
% cnf(2041,plain,(rreal(vf(vd1199,vd1186))|~rpoint(vd1178)|~rpoint(vd1179)),inference(spm,[status(thm)],[2038,873,theory(equality)])).
% cnf(2051,plain,(rreal(vf(vd1199,vd1186))|$false|~rpoint(vd1179)),inference(rw,[status(thm)],[2041,865,theory(equality)])).
% cnf(2052,plain,(rreal(vf(vd1199,vd1186))|$false|$false),inference(rw,[status(thm)],[2051,864,theory(equality)])).
% cnf(2053,plain,(rreal(vf(vd1199,vd1186))),inference(cn,[status(thm)],[2052,theory(equality)])).
% cnf(2150,plain,(X1=X2|vplus(X1,X3)!=vplus(X3,X2)|~rreal(X3)|~rreal(X2)|~rreal(X1)),inference(spm,[status(thm)],[1008,932,theory(equality)])).
% cnf(2266,plain,(rreal(vplus(X1,X2))|~rreal(X2)|~rreal(X1)),inference(spm,[status(thm)],[957,1005,theory(equality)])).
% cnf(2578,plain,(vf(X1,X2)=vf(X1,X3)|X1=X4|~ron(X3,esk50_2(X1,X4))|~ron(X2,esk50_2(X1,X4))|~rpoint(X3)|~rpoint(X2)|~rpoint(X1)|~rpoint(X4)),inference(spm,[status(thm)],[1085,982,theory(equality)])).
% cnf(2700,plain,(ron(X1,X2)|vf(X3,X1)!=vf(X4,X3)|~rcenter(X3,X2)|~ron(X4,X2)|~rpoint(X4)|~rpoint(X1)|~rpoint(X3)),inference(spm,[status(thm)],[1114,930,theory(equality)])).
% cnf(2709,plain,(ron(X1,X2)|vf(X1,X3)!=vf(X3,X4)|~rcenter(X3,X2)|~ron(X4,X2)|~rpoint(X4)|~rpoint(X1)|~rpoint(X3)),inference(spm,[status(thm)],[1114,930,theory(equality)])).
% cnf(2856,plain,(rinside(X1,X2)|~rcenter(vd1185,X2)|~rless(vf(vd1185,X1),vf(vd1199,vd1186))|~ron(vd1186,X2)|~rpoint(X1)|~rpoint(vd1186)),inference(spm,[status(thm)],[1129,872,theory(equality)])).
% cnf(2865,plain,(rinside(vd1186,X1)|~rcenter(vd1185,X1)|~rless(vf(vd1199,vd1186),vf(vd1185,X2))|~ron(X2,X1)|~rpoint(vd1186)|~rpoint(X2)),inference(spm,[status(thm)],[1129,872,theory(equality)])).
% cnf(2881,plain,(rinside(X1,X2)|~rcenter(vd1185,X2)|~rless(vf(vd1185,X1),vf(vd1199,vd1186))|~ron(vd1186,X2)|~rpoint(X1)|$false),inference(rw,[status(thm)],[2856,859,theory(equality)])).
% cnf(2882,plain,(rinside(X1,X2)|~rcenter(vd1185,X2)|~rless(vf(vd1185,X1),vf(vd1199,vd1186))|~ron(vd1186,X2)|~rpoint(X1)),inference(cn,[status(thm)],[2881,theory(equality)])).
% cnf(2893,plain,(rinside(vd1186,X1)|~rcenter(vd1185,X1)|~rless(vf(vd1199,vd1186),vf(vd1185,X2))|~ron(X2,X1)|$false|~rpoint(X2)),inference(rw,[status(thm)],[2865,859,theory(equality)])).
% cnf(2894,plain,(rinside(vd1186,X1)|~rcenter(vd1185,X1)|~rless(vf(vd1199,vd1186),vf(vd1185,X2))|~ron(X2,X1)|~rpoint(X2)),inference(cn,[status(thm)],[2893,theory(equality)])).
% cnf(2895,plain,(rinside(vd1186,esk50_2(vd1185,X1))|vd1185=X1|~rless(vf(vd1199,vd1186),vf(vd1185,X2))|~ron(X2,esk50_2(vd1185,X1))|~rpoint(X2)|~rpoint(vd1185)|~rpoint(X1)),inference(spm,[status(thm)],[2894,982,theory(equality)])).
% cnf(2896,plain,(rinside(vd1186,esk50_2(vd1185,X1))|vd1185=X1|~rless(vf(vd1199,vd1186),vf(vd1185,X2))|~ron(X2,esk50_2(vd1185,X1))|~rpoint(X2)|$false|~rpoint(X1)),inference(rw,[status(thm)],[2895,862,theory(equality)])).
% cnf(2897,plain,(rinside(vd1186,esk50_2(vd1185,X1))|vd1185=X1|~rless(vf(vd1199,vd1186),vf(vd1185,X2))|~ron(X2,esk50_2(vd1185,X1))|~rpoint(X2)|~rpoint(X1)),inference(cn,[status(thm)],[2896,theory(equality)])).
% cnf(2898,plain,(rinside(X1,esk50_2(vd1185,X2))|vd1185=X2|~rless(vf(vd1185,X1),vf(vd1199,vd1186))|~ron(vd1186,esk50_2(vd1185,X2))|~rpoint(X1)|~rpoint(vd1185)|~rpoint(X2)),inference(spm,[status(thm)],[2882,982,theory(equality)])).
% cnf(2899,plain,(rinside(X1,esk50_2(vd1185,X2))|vd1185=X2|~rless(vf(vd1185,X1),vf(vd1199,vd1186))|~ron(vd1186,esk50_2(vd1185,X2))|~rpoint(X1)|$false|~rpoint(X2)),inference(rw,[status(thm)],[2898,862,theory(equality)])).
% cnf(2900,plain,(rinside(X1,esk50_2(vd1185,X2))|vd1185=X2|~rless(vf(vd1185,X1),vf(vd1199,vd1186))|~ron(vd1186,esk50_2(vd1185,X2))|~rpoint(X1)|~rpoint(X2)),inference(cn,[status(thm)],[2899,theory(equality)])).
% cnf(2904,plain,(vd1185=vd1186|rinside(X1,esk50_2(vd1185,vd1186))|~rless(vf(vd1185,X1),vf(vd1199,vd1186))|~rpoint(X1)|~rpoint(vd1186)|~rpoint(vd1185)),inference(spm,[status(thm)],[2900,978,theory(equality)])).
% cnf(2905,plain,(vd1185=vd1186|rinside(X1,esk50_2(vd1185,vd1186))|~rless(vf(vd1185,X1),vf(vd1199,vd1186))|~rpoint(X1)|$false|~rpoint(vd1185)),inference(rw,[status(thm)],[2904,859,theory(equality)])).
% cnf(2906,plain,(vd1185=vd1186|rinside(X1,esk50_2(vd1185,vd1186))|~rless(vf(vd1185,X1),vf(vd1199,vd1186))|~rpoint(X1)|$false|$false),inference(rw,[status(thm)],[2905,862,theory(equality)])).
% cnf(2907,plain,(vd1185=vd1186|rinside(X1,esk50_2(vd1185,vd1186))|~rless(vf(vd1185,X1),vf(vd1199,vd1186))|~rpoint(X1)),inference(cn,[status(thm)],[2906,theory(equality)])).
% cnf(2908,plain,(vd1186=vd1185|rinside(X1,esk50_2(vd1185,vd1186))|~rless(vf(X1,vd1185),vf(vd1199,vd1186))|~rpoint(X1)|~rpoint(vd1185)),inference(spm,[status(thm)],[2907,930,theory(equality)])).
% cnf(2915,plain,(vd1186=vd1185|rinside(X1,esk50_2(vd1185,vd1186))|~rless(vf(X1,vd1185),vf(vd1199,vd1186))|~rpoint(X1)|$false),inference(rw,[status(thm)],[2908,862,theory(equality)])).
% cnf(2916,plain,(vd1186=vd1185|rinside(X1,esk50_2(vd1185,vd1186))|~rless(vf(X1,vd1185),vf(vd1199,vd1186))|~rpoint(X1)),inference(cn,[status(thm)],[2915,theory(equality)])).
% cnf(2957,plain,(vd1186=vd1185|rinside(X1,esk50_2(vd1185,vd1186))|vf(vd1199,vd1186)=vf(X1,vd1185)|rless(vf(vd1199,vd1186),vf(X1,vd1185))|~rpoint(X1)|~rreal(vf(vd1199,vd1186))|~rreal(vf(X1,vd1185))),inference(spm,[status(thm)],[2916,955,theory(equality)])).
% cnf(2965,plain,(vd1186=vd1185|rinside(X1,esk50_2(vd1185,vd1186))|vf(vd1199,vd1186)=vf(X1,vd1185)|rless(vf(vd1199,vd1186),vf(X1,vd1185))|~rpoint(X1)|$false|~rreal(vf(X1,vd1185))),inference(rw,[status(thm)],[2957,2053,theory(equality)])).
% cnf(2966,plain,(vd1186=vd1185|rinside(X1,esk50_2(vd1185,vd1186))|vf(vd1199,vd1186)=vf(X1,vd1185)|rless(vf(vd1199,vd1186),vf(X1,vd1185))|~rpoint(X1)|~rreal(vf(X1,vd1185))),inference(cn,[status(thm)],[2965,theory(equality)])).
% cnf(3290,plain,(vd1185=X1|rinside(vd1186,esk50_2(vd1185,X1))|~rless(vf(vd1199,vd1186),vf(vd1185,X1))|~rpoint(X1)|~rpoint(vd1185)),inference(spm,[status(thm)],[2897,978,theory(equality)])).
% cnf(3291,plain,(vd1185=X1|rinside(vd1186,esk50_2(vd1185,X1))|~rless(vf(vd1199,vd1186),vf(vd1185,X1))|~rpoint(X1)|$false),inference(rw,[status(thm)],[3290,862,theory(equality)])).
% cnf(3292,plain,(vd1185=X1|rinside(vd1186,esk50_2(vd1185,X1))|~rless(vf(vd1199,vd1186),vf(vd1185,X1))|~rpoint(X1)),inference(cn,[status(thm)],[3291,theory(equality)])).
% cnf(3294,plain,(vd1185=X1|rinside(vd1186,esk50_2(vd1185,X1))|~rless(vf(vd1199,vd1186),vf(X1,vd1185))|~rpoint(X1)|~rpoint(vd1185)),inference(spm,[status(thm)],[3292,930,theory(equality)])).
% cnf(3300,plain,(vd1185=X1|rinside(vd1186,esk50_2(vd1185,X1))|~rless(vf(vd1199,vd1186),vf(X1,vd1185))|~rpoint(X1)|$false),inference(rw,[status(thm)],[3294,862,theory(equality)])).
% cnf(3301,plain,(vd1185=X1|rinside(vd1186,esk50_2(vd1185,X1))|~rless(vf(vd1199,vd1186),vf(X1,vd1185))|~rpoint(X1)),inference(cn,[status(thm)],[3300,theory(equality)])).
% cnf(3733,plain,(vf(vd1199,vd1186)=vf(X1,vd1185)|vd1186=vd1185|rless(vf(vd1199,vd1186),vf(X1,vd1185))|rinside(X1,esk50_2(vd1185,vd1186))|~rpoint(X1)|~rpoint(vd1185)),inference(spm,[status(thm)],[2966,2038,theory(equality)])).
% cnf(3742,plain,(vf(vd1199,vd1186)=vf(X1,vd1185)|vd1186=vd1185|rless(vf(vd1199,vd1186),vf(X1,vd1185))|rinside(X1,esk50_2(vd1185,vd1186))|~rpoint(X1)|$false),inference(rw,[status(thm)],[3733,862,theory(equality)])).
% cnf(3743,plain,(vf(vd1199,vd1186)=vf(X1,vd1185)|vd1186=vd1185|rless(vf(vd1199,vd1186),vf(X1,vd1185))|rinside(X1,esk50_2(vd1185,vd1186))|~rpoint(X1)),inference(cn,[status(thm)],[3742,theory(equality)])).
% cnf(3745,plain,(vf(vd1199,vd1186)=vf(X1,vd1185)|vd1186=vd1185|rless(vf(vd1199,vd1186),vf(X1,vd1185))|~rcircle(esk50_2(vd1185,vd1186))|~ron(X1,esk50_2(vd1185,vd1186))|~rpoint(X1)),inference(spm,[status(thm)],[918,3743,theory(equality)])).
% cnf(3749,plain,(vf(vd1199,vd1186)=vf(X1,vd1185)|vd1186=vd1185|rless(vf(vd1199,vd1186),vf(X1,vd1185))|~ron(X1,esk50_2(vd1185,vd1186))|~rpoint(X1)|~rpoint(vd1185)|~rpoint(vd1186)),inference(spm,[status(thm)],[3745,953,theory(equality)])).
% cnf(3750,plain,(vf(vd1199,vd1186)=vf(X1,vd1185)|vd1186=vd1185|rless(vf(vd1199,vd1186),vf(X1,vd1185))|~ron(X1,esk50_2(vd1185,vd1186))|~rpoint(X1)|$false|~rpoint(vd1186)),inference(rw,[status(thm)],[3749,862,theory(equality)])).
% cnf(3751,plain,(vf(vd1199,vd1186)=vf(X1,vd1185)|vd1186=vd1185|rless(vf(vd1199,vd1186),vf(X1,vd1185))|~ron(X1,esk50_2(vd1185,vd1186))|~rpoint(X1)|$false|$false),inference(rw,[status(thm)],[3750,859,theory(equality)])).
% cnf(3752,plain,(vf(vd1199,vd1186)=vf(X1,vd1185)|vd1186=vd1185|rless(vf(vd1199,vd1186),vf(X1,vd1185))|~ron(X1,esk50_2(vd1185,vd1186))|~rpoint(X1)),inference(cn,[status(thm)],[3751,theory(equality)])).
% cnf(3755,plain,(vf(vd1199,vd1186)=vf(vd1186,vd1185)|vd1186=vd1185|rless(vf(vd1199,vd1186),vf(vd1186,vd1185))|~rpoint(vd1186)|~rpoint(vd1185)),inference(spm,[status(thm)],[3752,978,theory(equality)])).
% cnf(3756,plain,(vf(vd1199,vd1186)=vf(vd1186,vd1185)|vd1186=vd1185|rless(vf(vd1199,vd1186),vf(vd1186,vd1185))|$false|~rpoint(vd1185)),inference(rw,[status(thm)],[3755,859,theory(equality)])).
% cnf(3757,plain,(vf(vd1199,vd1186)=vf(vd1186,vd1185)|vd1186=vd1185|rless(vf(vd1199,vd1186),vf(vd1186,vd1185))|$false|$false),inference(rw,[status(thm)],[3756,862,theory(equality)])).
% cnf(3758,plain,(vf(vd1199,vd1186)=vf(vd1186,vd1185)|vd1186=vd1185|rless(vf(vd1199,vd1186),vf(vd1186,vd1185))),inference(cn,[status(thm)],[3757,theory(equality)])).
% cnf(3762,plain,(vd1185=vd1186|rinside(vd1186,esk50_2(vd1185,vd1186))|vf(vd1186,vd1185)=vf(vd1199,vd1186)|~rpoint(vd1186)),inference(spm,[status(thm)],[3301,3758,theory(equality)])).
% cnf(3771,plain,(vd1185=vd1186|rinside(vd1186,esk50_2(vd1185,vd1186))|vf(vd1186,vd1185)=vf(vd1199,vd1186)|$false),inference(rw,[status(thm)],[3762,859,theory(equality)])).
% cnf(3772,plain,(vd1185=vd1186|rinside(vd1186,esk50_2(vd1185,vd1186))|vf(vd1186,vd1185)=vf(vd1199,vd1186)),inference(cn,[status(thm)],[3771,theory(equality)])).
% cnf(3783,plain,(vf(vd1186,vd1185)=vf(vd1199,vd1186)|vd1186=vd1185|~rcircle(esk50_2(vd1185,vd1186))|~ron(vd1186,esk50_2(vd1185,vd1186))|~rpoint(vd1186)),inference(spm,[status(thm)],[918,3772,theory(equality)])).
% cnf(3787,plain,(vf(vd1186,vd1185)=vf(vd1199,vd1186)|vd1186=vd1185|~rcircle(esk50_2(vd1185,vd1186))|~ron(vd1186,esk50_2(vd1185,vd1186))|$false),inference(rw,[status(thm)],[3783,859,theory(equality)])).
% cnf(3788,plain,(vf(vd1186,vd1185)=vf(vd1199,vd1186)|vd1186=vd1185|~rcircle(esk50_2(vd1185,vd1186))|~ron(vd1186,esk50_2(vd1185,vd1186))),inference(cn,[status(thm)],[3787,theory(equality)])).
% cnf(3795,plain,(vf(vd1186,vd1185)=vf(vd1199,vd1186)|vd1186=vd1185|~ron(vd1186,esk50_2(vd1185,vd1186))|~rpoint(vd1185)|~rpoint(vd1186)),inference(spm,[status(thm)],[3788,953,theory(equality)])).
% cnf(3796,plain,(vf(vd1186,vd1185)=vf(vd1199,vd1186)|vd1186=vd1185|~ron(vd1186,esk50_2(vd1185,vd1186))|$false|~rpoint(vd1186)),inference(rw,[status(thm)],[3795,862,theory(equality)])).
% cnf(3797,plain,(vf(vd1186,vd1185)=vf(vd1199,vd1186)|vd1186=vd1185|~ron(vd1186,esk50_2(vd1185,vd1186))|$false|$false),inference(rw,[status(thm)],[3796,859,theory(equality)])).
% cnf(3798,plain,(vf(vd1186,vd1185)=vf(vd1199,vd1186)|vd1186=vd1185|~ron(vd1186,esk50_2(vd1185,vd1186))),inference(cn,[status(thm)],[3797,theory(equality)])).
% cnf(3799,plain,(vf(vd1186,vd1185)=vf(vd1199,vd1186)|vd1186=vd1185|~rpoint(vd1185)|~rpoint(vd1186)),inference(spm,[status(thm)],[3798,978,theory(equality)])).
% cnf(3800,plain,(vf(vd1186,vd1185)=vf(vd1199,vd1186)|vd1186=vd1185|$false|~rpoint(vd1186)),inference(rw,[status(thm)],[3799,862,theory(equality)])).
% cnf(3801,plain,(vf(vd1186,vd1185)=vf(vd1199,vd1186)|vd1186=vd1185|$false|$false),inference(rw,[status(thm)],[3800,859,theory(equality)])).
% cnf(3802,plain,(vf(vd1186,vd1185)=vf(vd1199,vd1186)|vd1186=vd1185),inference(cn,[status(thm)],[3801,theory(equality)])).
% cnf(3884,plain,(X1=vd1185|rpoint(esk13_4(vd1197,vd1197,X1,vd1185))|~rline(vd1197)|~ron(X1,vd1197)|~rpoint(X1)|~rpoint(vd1185)),inference(spm,[status(thm)],[1205,273,theory(equality)])).
% cnf(3914,plain,(X1=vd1185|rpoint(esk13_4(vd1197,vd1197,X1,vd1185))|$false|~ron(X1,vd1197)|~rpoint(X1)|~rpoint(vd1185)),inference(rw,[status(thm)],[3884,416,theory(equality)])).
% cnf(3915,plain,(X1=vd1185|rpoint(esk13_4(vd1197,vd1197,X1,vd1185))|$false|~ron(X1,vd1197)|~rpoint(X1)|$false),inference(rw,[status(thm)],[3914,862,theory(equality)])).
% cnf(3916,plain,(X1=vd1185|rpoint(esk13_4(vd1197,vd1197,X1,vd1185))|~ron(X1,vd1197)|~rpoint(X1)),inference(cn,[status(thm)],[3915,theory(equality)])).
% cnf(3937,plain,(vd1199=vd1185|rpoint(esk13_4(vd1197,vd1197,vd1199,vd1185))|~rpoint(vd1199)),inference(spm,[status(thm)],[3916,284,theory(equality)])).
% cnf(3953,plain,(vd1199=vd1185|rpoint(esk13_4(vd1197,vd1197,vd1199,vd1185))|$false),inference(rw,[status(thm)],[3937,858,theory(equality)])).
% cnf(3954,plain,(vd1199=vd1185|rpoint(esk13_4(vd1197,vd1197,vd1199,vd1185))),inference(cn,[status(thm)],[3953,theory(equality)])).
% cnf(3955,plain,(rpoint(esk13_4(vd1197,vd1197,vd1199,vd1185))),inference(sr,[status(thm)],[3954,171,theory(equality)])).
% cnf(4001,plain,(X1=vd1185|rpoint(esk16_4(vd1197,vd1197,X1,vd1185))|~rline(vd1197)|~ron(X1,vd1197)|~rpoint(X1)|~rpoint(vd1185)),inference(spm,[status(thm)],[1208,273,theory(equality)])).
% cnf(4031,plain,(X1=vd1185|rpoint(esk16_4(vd1197,vd1197,X1,vd1185))|$false|~ron(X1,vd1197)|~rpoint(X1)|~rpoint(vd1185)),inference(rw,[status(thm)],[4001,416,theory(equality)])).
% cnf(4032,plain,(X1=vd1185|rpoint(esk16_4(vd1197,vd1197,X1,vd1185))|$false|~ron(X1,vd1197)|~rpoint(X1)|$false),inference(rw,[status(thm)],[4031,862,theory(equality)])).
% cnf(4033,plain,(X1=vd1185|rpoint(esk16_4(vd1197,vd1197,X1,vd1185))|~ron(X1,vd1197)|~rpoint(X1)),inference(cn,[status(thm)],[4032,theory(equality)])).
% cnf(4082,plain,(vd1199=vd1185|rpoint(esk16_4(vd1197,vd1197,vd1199,vd1185))|~rpoint(vd1199)),inference(spm,[status(thm)],[4033,284,theory(equality)])).
% cnf(4098,plain,(vd1199=vd1185|rpoint(esk16_4(vd1197,vd1197,vd1199,vd1185))|$false),inference(rw,[status(thm)],[4082,858,theory(equality)])).
% cnf(4099,plain,(vd1199=vd1185|rpoint(esk16_4(vd1197,vd1197,vd1199,vd1185))),inference(cn,[status(thm)],[4098,theory(equality)])).
% cnf(4100,plain,(rpoint(esk16_4(vd1197,vd1197,vd1199,vd1185))),inference(sr,[status(thm)],[4099,171,theory(equality)])).
% cnf(4526,plain,(X1=vd1185|rR(vd1185,X1,esk13_4(vd1197,vd1197,X1,vd1185))|~rline(vd1197)|~ron(X1,vd1197)|~rpoint(X1)|~rpoint(vd1185)),inference(spm,[status(thm)],[1227,273,theory(equality)])).
% cnf(4556,plain,(X1=vd1185|rR(vd1185,X1,esk13_4(vd1197,vd1197,X1,vd1185))|$false|~ron(X1,vd1197)|~rpoint(X1)|~rpoint(vd1185)),inference(rw,[status(thm)],[4526,416,theory(equality)])).
% cnf(4557,plain,(X1=vd1185|rR(vd1185,X1,esk13_4(vd1197,vd1197,X1,vd1185))|$false|~ron(X1,vd1197)|~rpoint(X1)|$false),inference(rw,[status(thm)],[4556,862,theory(equality)])).
% cnf(4558,plain,(X1=vd1185|rR(vd1185,X1,esk13_4(vd1197,vd1197,X1,vd1185))|~ron(X1,vd1197)|~rpoint(X1)),inference(cn,[status(thm)],[4557,theory(equality)])).
% cnf(4576,plain,(vd1199=vd1185|rR(vd1185,vd1199,esk13_4(vd1197,vd1197,vd1199,vd1185))|~rpoint(vd1199)),inference(spm,[status(thm)],[4558,284,theory(equality)])).
% cnf(4592,plain,(vd1199=vd1185|rR(vd1185,vd1199,esk13_4(vd1197,vd1197,vd1199,vd1185))|$false),inference(rw,[status(thm)],[4576,858,theory(equality)])).
% cnf(4593,plain,(vd1199=vd1185|rR(vd1185,vd1199,esk13_4(vd1197,vd1197,vd1199,vd1185))),inference(cn,[status(thm)],[4592,theory(equality)])).
% cnf(4594,plain,(rR(vd1185,vd1199,esk13_4(vd1197,vd1197,vd1199,vd1185))),inference(sr,[status(thm)],[4593,171,theory(equality)])).
% cnf(4598,plain,(rR(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)|~rpoint(vd1199)|~rpoint(vd1185)|~rpoint(esk13_4(vd1197,vd1197,vd1199,vd1185))),inference(spm,[status(thm)],[1011,4594,theory(equality)])).
% cnf(4599,plain,(vplus(vf(vd1199,vd1185),vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)))=vf(vd1199,esk13_4(vd1197,vd1197,vd1199,vd1185))|~rpoint(vd1199)|~rpoint(vd1185)|~rpoint(esk13_4(vd1197,vd1197,vd1199,vd1185))),inference(spm,[status(thm)],[1202,4594,theory(equality)])).
% cnf(4612,plain,(rR(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)|$false|~rpoint(vd1185)|~rpoint(esk13_4(vd1197,vd1197,vd1199,vd1185))),inference(rw,[status(thm)],[4598,858,theory(equality)])).
% cnf(4613,plain,(rR(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)|$false|$false|~rpoint(esk13_4(vd1197,vd1197,vd1199,vd1185))),inference(rw,[status(thm)],[4612,862,theory(equality)])).
% cnf(4614,plain,(rR(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)|$false|$false|$false),inference(rw,[status(thm)],[4613,3955,theory(equality)])).
% cnf(4615,plain,(rR(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)),inference(cn,[status(thm)],[4614,theory(equality)])).
% cnf(4616,plain,(vplus(vf(vd1199,vd1185),vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)))=vf(vd1199,esk13_4(vd1197,vd1197,vd1199,vd1185))|$false|~rpoint(vd1185)|~rpoint(esk13_4(vd1197,vd1197,vd1199,vd1185))),inference(rw,[status(thm)],[4599,858,theory(equality)])).
% cnf(4617,plain,(vplus(vf(vd1199,vd1185),vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)))=vf(vd1199,esk13_4(vd1197,vd1197,vd1199,vd1185))|$false|$false|~rpoint(esk13_4(vd1197,vd1197,vd1199,vd1185))),inference(rw,[status(thm)],[4616,862,theory(equality)])).
% cnf(4618,plain,(vplus(vf(vd1199,vd1185),vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)))=vf(vd1199,esk13_4(vd1197,vd1197,vd1199,vd1185))|$false|$false|$false),inference(rw,[status(thm)],[4617,3955,theory(equality)])).
% cnf(4619,plain,(vplus(vf(vd1199,vd1185),vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)))=vf(vd1199,esk13_4(vd1197,vd1197,vd1199,vd1185))),inference(cn,[status(thm)],[4618,theory(equality)])).
% cnf(4654,plain,(vplus(vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1185),vf(vd1185,vd1199))=vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)|~rpoint(esk13_4(vd1197,vd1197,vd1199,vd1185))|~rpoint(vd1185)|~rpoint(vd1199)),inference(spm,[status(thm)],[1202,4615,theory(equality)])).
% cnf(4672,plain,(vplus(vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1185),vf(vd1185,vd1199))=vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)|$false|~rpoint(vd1185)|~rpoint(vd1199)),inference(rw,[status(thm)],[4654,3955,theory(equality)])).
% cnf(4673,plain,(vplus(vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1185),vf(vd1185,vd1199))=vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)|$false|$false|~rpoint(vd1199)),inference(rw,[status(thm)],[4672,862,theory(equality)])).
% cnf(4674,plain,(vplus(vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1185),vf(vd1185,vd1199))=vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)|$false|$false|$false),inference(rw,[status(thm)],[4673,858,theory(equality)])).
% cnf(4675,plain,(vplus(vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1185),vf(vd1185,vd1199))=vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)),inference(cn,[status(thm)],[4674,theory(equality)])).
% cnf(4767,plain,(X1=vd1185|rR(esk16_4(vd1197,vd1197,X1,vd1185),X1,vd1185)|~rline(vd1197)|~ron(X1,vd1197)|~rpoint(X1)|~rpoint(vd1185)),inference(spm,[status(thm)],[1230,273,theory(equality)])).
% cnf(4797,plain,(X1=vd1185|rR(esk16_4(vd1197,vd1197,X1,vd1185),X1,vd1185)|$false|~ron(X1,vd1197)|~rpoint(X1)|~rpoint(vd1185)),inference(rw,[status(thm)],[4767,416,theory(equality)])).
% cnf(4798,plain,(X1=vd1185|rR(esk16_4(vd1197,vd1197,X1,vd1185),X1,vd1185)|$false|~ron(X1,vd1197)|~rpoint(X1)|$false),inference(rw,[status(thm)],[4797,862,theory(equality)])).
% cnf(4799,plain,(X1=vd1185|rR(esk16_4(vd1197,vd1197,X1,vd1185),X1,vd1185)|~ron(X1,vd1197)|~rpoint(X1)),inference(cn,[status(thm)],[4798,theory(equality)])).
% cnf(4863,plain,(vf(vd1199,vd1185)=X1|vf(vd1199,esk13_4(vd1197,vd1197,vd1199,vd1185))!=vplus(vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)),X1)|~rreal(vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)))|~rreal(X1)|~rreal(vf(vd1199,vd1185))),inference(spm,[status(thm)],[2150,4619,theory(equality)])).
% cnf(4877,plain,(vplus(vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1185),vf(vd1199,vd1185))=vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)|~rpoint(vd1185)|~rpoint(vd1199)),inference(spm,[status(thm)],[4675,930,theory(equality)])).
% cnf(4879,plain,(vplus(vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)),vf(vd1185,vd1199))=vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)|~rpoint(esk13_4(vd1197,vd1197,vd1199,vd1185))|~rpoint(vd1185)),inference(spm,[status(thm)],[4675,930,theory(equality)])).
% cnf(4881,plain,(vplus(vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1185),vf(vd1199,vd1185))=vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)|$false|~rpoint(vd1199)),inference(rw,[status(thm)],[4877,862,theory(equality)])).
% cnf(4882,plain,(vplus(vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1185),vf(vd1199,vd1185))=vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)|$false|$false),inference(rw,[status(thm)],[4881,858,theory(equality)])).
% cnf(4883,plain,(vplus(vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1185),vf(vd1199,vd1185))=vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)),inference(cn,[status(thm)],[4882,theory(equality)])).
% cnf(4887,plain,(vplus(vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)),vf(vd1185,vd1199))=vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)|$false|~rpoint(vd1185)),inference(rw,[status(thm)],[4879,3955,theory(equality)])).
% cnf(4888,plain,(vplus(vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)),vf(vd1185,vd1199))=vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)|$false|$false),inference(rw,[status(thm)],[4887,862,theory(equality)])).
% cnf(4889,plain,(vplus(vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)),vf(vd1185,vd1199))=vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)),inference(cn,[status(thm)],[4888,theory(equality)])).
% cnf(7879,plain,(vd1199=vd1185|rR(esk16_4(vd1197,vd1197,vd1199,vd1185),vd1199,vd1185)|~rpoint(vd1199)),inference(spm,[status(thm)],[4799,284,theory(equality)])).
% cnf(7903,plain,(vd1199=vd1185|rR(esk16_4(vd1197,vd1197,vd1199,vd1185),vd1199,vd1185)|$false),inference(rw,[status(thm)],[7879,858,theory(equality)])).
% cnf(7904,plain,(vd1199=vd1185|rR(esk16_4(vd1197,vd1197,vd1199,vd1185),vd1199,vd1185)),inference(cn,[status(thm)],[7903,theory(equality)])).
% cnf(7905,plain,(rR(esk16_4(vd1197,vd1197,vd1199,vd1185),vd1199,vd1185)),inference(sr,[status(thm)],[7904,171,theory(equality)])).
% cnf(7909,plain,(rR(esk16_4(vd1197,vd1197,vd1199,vd1185),vd1185,vd1199)|~rpoint(vd1199)|~rpoint(esk16_4(vd1197,vd1197,vd1199,vd1185))|~rpoint(vd1185)),inference(spm,[status(thm)],[1011,7905,theory(equality)])).
% cnf(7910,plain,(vplus(vf(vd1199,esk16_4(vd1197,vd1197,vd1199,vd1185)),vf(esk16_4(vd1197,vd1197,vd1199,vd1185),vd1185))=vf(vd1199,vd1185)|~rpoint(vd1199)|~rpoint(esk16_4(vd1197,vd1197,vd1199,vd1185))|~rpoint(vd1185)),inference(spm,[status(thm)],[1202,7905,theory(equality)])).
% cnf(7930,plain,(rR(esk16_4(vd1197,vd1197,vd1199,vd1185),vd1185,vd1199)|$false|~rpoint(esk16_4(vd1197,vd1197,vd1199,vd1185))|~rpoint(vd1185)),inference(rw,[status(thm)],[7909,858,theory(equality)])).
% cnf(7931,plain,(rR(esk16_4(vd1197,vd1197,vd1199,vd1185),vd1185,vd1199)|$false|$false|~rpoint(vd1185)),inference(rw,[status(thm)],[7930,4100,theory(equality)])).
% cnf(7932,plain,(rR(esk16_4(vd1197,vd1197,vd1199,vd1185),vd1185,vd1199)|$false|$false|$false),inference(rw,[status(thm)],[7931,862,theory(equality)])).
% cnf(7933,plain,(rR(esk16_4(vd1197,vd1197,vd1199,vd1185),vd1185,vd1199)),inference(cn,[status(thm)],[7932,theory(equality)])).
% cnf(7934,plain,(vplus(vf(vd1199,esk16_4(vd1197,vd1197,vd1199,vd1185)),vf(esk16_4(vd1197,vd1197,vd1199,vd1185),vd1185))=vf(vd1199,vd1185)|$false|~rpoint(esk16_4(vd1197,vd1197,vd1199,vd1185))|~rpoint(vd1185)),inference(rw,[status(thm)],[7910,858,theory(equality)])).
% cnf(7935,plain,(vplus(vf(vd1199,esk16_4(vd1197,vd1197,vd1199,vd1185)),vf(esk16_4(vd1197,vd1197,vd1199,vd1185),vd1185))=vf(vd1199,vd1185)|$false|$false|~rpoint(vd1185)),inference(rw,[status(thm)],[7934,4100,theory(equality)])).
% cnf(7936,plain,(vplus(vf(vd1199,esk16_4(vd1197,vd1197,vd1199,vd1185)),vf(esk16_4(vd1197,vd1197,vd1199,vd1185),vd1185))=vf(vd1199,vd1185)|$false|$false|$false),inference(rw,[status(thm)],[7935,862,theory(equality)])).
% cnf(7937,plain,(vplus(vf(vd1199,esk16_4(vd1197,vd1197,vd1199,vd1185)),vf(esk16_4(vd1197,vd1197,vd1199,vd1185),vd1185))=vf(vd1199,vd1185)),inference(cn,[status(thm)],[7936,theory(equality)])).
% cnf(7998,plain,(vplus(vf(vd1185,esk16_4(vd1197,vd1197,vd1199,vd1185)),vf(esk16_4(vd1197,vd1197,vd1199,vd1185),vd1199))=vf(vd1185,vd1199)|~rpoint(vd1185)|~rpoint(esk16_4(vd1197,vd1197,vd1199,vd1185))|~rpoint(vd1199)),inference(spm,[status(thm)],[1202,7933,theory(equality)])).
% cnf(8023,plain,(vplus(vf(vd1185,esk16_4(vd1197,vd1197,vd1199,vd1185)),vf(esk16_4(vd1197,vd1197,vd1199,vd1185),vd1199))=vf(vd1185,vd1199)|$false|~rpoint(esk16_4(vd1197,vd1197,vd1199,vd1185))|~rpoint(vd1199)),inference(rw,[status(thm)],[7998,862,theory(equality)])).
% cnf(8024,plain,(vplus(vf(vd1185,esk16_4(vd1197,vd1197,vd1199,vd1185)),vf(esk16_4(vd1197,vd1197,vd1199,vd1185),vd1199))=vf(vd1185,vd1199)|$false|$false|~rpoint(vd1199)),inference(rw,[status(thm)],[8023,4100,theory(equality)])).
% cnf(8025,plain,(vplus(vf(vd1185,esk16_4(vd1197,vd1197,vd1199,vd1185)),vf(esk16_4(vd1197,vd1197,vd1199,vd1185),vd1199))=vf(vd1185,vd1199)|$false|$false|$false),inference(rw,[status(thm)],[8024,858,theory(equality)])).
% cnf(8026,plain,(vplus(vf(vd1185,esk16_4(vd1197,vd1197,vd1199,vd1185)),vf(esk16_4(vd1197,vd1197,vd1199,vd1185),vd1199))=vf(vd1185,vd1199)),inference(cn,[status(thm)],[8025,theory(equality)])).
% cnf(8723,plain,(rreal(vf(vd1199,vd1185))|~rreal(vf(esk16_4(vd1197,vd1197,vd1199,vd1185),vd1185))|~rreal(vf(vd1199,esk16_4(vd1197,vd1197,vd1199,vd1185)))),inference(spm,[status(thm)],[2266,7937,theory(equality)])).
% cnf(8740,plain,(rreal(vf(vd1185,vd1199))|~rreal(vf(esk16_4(vd1197,vd1197,vd1199,vd1185),vd1199))|~rreal(vf(vd1185,esk16_4(vd1197,vd1197,vd1199,vd1185)))),inference(spm,[status(thm)],[2266,8026,theory(equality)])).
% cnf(8758,plain,(rreal(vf(vd1199,vd1185))|~rreal(vf(vd1199,esk16_4(vd1197,vd1197,vd1199,vd1185)))|~rpoint(esk16_4(vd1197,vd1197,vd1199,vd1185))|~rpoint(vd1185)),inference(spm,[status(thm)],[8723,2038,theory(equality)])).
% cnf(8765,plain,(rreal(vf(vd1199,vd1185))|~rreal(vf(vd1199,esk16_4(vd1197,vd1197,vd1199,vd1185)))|$false|~rpoint(vd1185)),inference(rw,[status(thm)],[8758,4100,theory(equality)])).
% cnf(8766,plain,(rreal(vf(vd1199,vd1185))|~rreal(vf(vd1199,esk16_4(vd1197,vd1197,vd1199,vd1185)))|$false|$false),inference(rw,[status(thm)],[8765,862,theory(equality)])).
% cnf(8767,plain,(rreal(vf(vd1199,vd1185))|~rreal(vf(vd1199,esk16_4(vd1197,vd1197,vd1199,vd1185)))),inference(cn,[status(thm)],[8766,theory(equality)])).
% cnf(8768,plain,(rreal(vf(vd1199,vd1185))|~rpoint(vd1199)|~rpoint(esk16_4(vd1197,vd1197,vd1199,vd1185))),inference(spm,[status(thm)],[8767,2038,theory(equality)])).
% cnf(8769,plain,(rreal(vf(vd1199,vd1185))|$false|~rpoint(esk16_4(vd1197,vd1197,vd1199,vd1185))),inference(rw,[status(thm)],[8768,858,theory(equality)])).
% cnf(8770,plain,(rreal(vf(vd1199,vd1185))|$false|$false),inference(rw,[status(thm)],[8769,4100,theory(equality)])).
% cnf(8771,plain,(rreal(vf(vd1199,vd1185))),inference(cn,[status(thm)],[8770,theory(equality)])).
% cnf(8775,plain,(rreal(vf(vd1185,vd1199))|~rreal(vf(vd1185,esk16_4(vd1197,vd1197,vd1199,vd1185)))|~rpoint(esk16_4(vd1197,vd1197,vd1199,vd1185))|~rpoint(vd1199)),inference(spm,[status(thm)],[8740,2038,theory(equality)])).
% cnf(8782,plain,(rreal(vf(vd1185,vd1199))|~rreal(vf(vd1185,esk16_4(vd1197,vd1197,vd1199,vd1185)))|$false|~rpoint(vd1199)),inference(rw,[status(thm)],[8775,4100,theory(equality)])).
% cnf(8783,plain,(rreal(vf(vd1185,vd1199))|~rreal(vf(vd1185,esk16_4(vd1197,vd1197,vd1199,vd1185)))|$false|$false),inference(rw,[status(thm)],[8782,858,theory(equality)])).
% cnf(8784,plain,(rreal(vf(vd1185,vd1199))|~rreal(vf(vd1185,esk16_4(vd1197,vd1197,vd1199,vd1185)))),inference(cn,[status(thm)],[8783,theory(equality)])).
% cnf(8855,plain,(rreal(vf(vd1185,vd1199))|~rpoint(vd1185)|~rpoint(esk16_4(vd1197,vd1197,vd1199,vd1185))),inference(spm,[status(thm)],[8784,2038,theory(equality)])).
% cnf(8856,plain,(rreal(vf(vd1185,vd1199))|$false|~rpoint(esk16_4(vd1197,vd1197,vd1199,vd1185))),inference(rw,[status(thm)],[8855,862,theory(equality)])).
% cnf(8857,plain,(rreal(vf(vd1185,vd1199))|$false|$false),inference(rw,[status(thm)],[8856,4100,theory(equality)])).
% cnf(8858,plain,(rreal(vf(vd1185,vd1199))),inference(cn,[status(thm)],[8857,theory(equality)])).
% cnf(12523,plain,(X1=vd1185|X2=vd1185|X2=X1|rR(vd1185,X1,X2)|rR(X1,vd1185,X2)|rR(X2,X1,vd1185)|~rline(vd1197)|~ron(X1,vd1197)|~ron(X2,vd1197)|~rpoint(X1)|~rpoint(vd1185)|~rpoint(X2)),inference(spm,[status(thm)],[1451,273,theory(equality)])).
% cnf(12577,plain,(X1=vd1185|X2=vd1185|X2=X1|rR(vd1185,X1,X2)|rR(X1,vd1185,X2)|rR(X2,X1,vd1185)|$false|~ron(X1,vd1197)|~ron(X2,vd1197)|~rpoint(X1)|~rpoint(vd1185)|~rpoint(X2)),inference(rw,[status(thm)],[12523,416,theory(equality)])).
% cnf(12578,plain,(X1=vd1185|X2=vd1185|X2=X1|rR(vd1185,X1,X2)|rR(X1,vd1185,X2)|rR(X2,X1,vd1185)|$false|~ron(X1,vd1197)|~ron(X2,vd1197)|~rpoint(X1)|$false|~rpoint(X2)),inference(rw,[status(thm)],[12577,862,theory(equality)])).
% cnf(12579,plain,(X1=vd1185|X2=vd1185|X2=X1|rR(vd1185,X1,X2)|rR(X1,vd1185,X2)|rR(X2,X1,vd1185)|~ron(X1,vd1197)|~ron(X2,vd1197)|~rpoint(X1)|~rpoint(X2)),inference(cn,[status(thm)],[12578,theory(equality)])).
% cnf(20476,plain,(vplus(vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)),vf(vd1199,vd1185))=vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)|~rpoint(esk13_4(vd1197,vd1197,vd1199,vd1185))|~rpoint(vd1185)),inference(spm,[status(thm)],[4883,930,theory(equality)])).
% cnf(20501,plain,(vplus(vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)),vf(vd1199,vd1185))=vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)|$false|~rpoint(vd1185)),inference(rw,[status(thm)],[20476,3955,theory(equality)])).
% cnf(20502,plain,(vplus(vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)),vf(vd1199,vd1185))=vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)|$false|$false),inference(rw,[status(thm)],[20501,862,theory(equality)])).
% cnf(20503,plain,(vplus(vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)),vf(vd1199,vd1185))=vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)),inference(cn,[status(thm)],[20502,theory(equality)])).
% cnf(21011,plain,(vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)=vplus(vf(vd1199,vd1185),vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)))|~rreal(vf(vd1199,vd1185))|~rreal(vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)))),inference(spm,[status(thm)],[932,20503,theory(equality)])).
% cnf(21022,plain,(vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)=vf(vd1199,esk13_4(vd1197,vd1197,vd1199,vd1185))|~rreal(vf(vd1199,vd1185))|~rreal(vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)))),inference(rw,[status(thm)],[21011,4619,theory(equality)])).
% cnf(21023,plain,(vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)=vf(vd1199,esk13_4(vd1197,vd1197,vd1199,vd1185))|$false|~rreal(vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)))),inference(rw,[status(thm)],[21022,8771,theory(equality)])).
% cnf(21024,plain,(vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)=vf(vd1199,esk13_4(vd1197,vd1197,vd1199,vd1185))|~rreal(vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)))),inference(cn,[status(thm)],[21023,theory(equality)])).
% cnf(21129,plain,(vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)=vf(vd1199,esk13_4(vd1197,vd1197,vd1199,vd1185))|~rpoint(vd1185)|~rpoint(esk13_4(vd1197,vd1197,vd1199,vd1185))),inference(spm,[status(thm)],[21024,2038,theory(equality)])).
% cnf(21130,plain,(vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)=vf(vd1199,esk13_4(vd1197,vd1197,vd1199,vd1185))|$false|~rpoint(esk13_4(vd1197,vd1197,vd1199,vd1185))),inference(rw,[status(thm)],[21129,862,theory(equality)])).
% cnf(21131,plain,(vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)=vf(vd1199,esk13_4(vd1197,vd1197,vd1199,vd1185))|$false|$false),inference(rw,[status(thm)],[21130,3955,theory(equality)])).
% cnf(21132,plain,(vf(esk13_4(vd1197,vd1197,vd1199,vd1185),vd1199)=vf(vd1199,esk13_4(vd1197,vd1197,vd1199,vd1185))),inference(cn,[status(thm)],[21131,theory(equality)])).
% cnf(21161,plain,(vplus(vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)),vf(vd1185,vd1199))=vf(vd1199,esk13_4(vd1197,vd1197,vd1199,vd1185))),inference(rw,[status(thm)],[4889,21132,theory(equality)])).
% cnf(35397,plain,(ron(vd1185,X1)|vd1186=vd1185|vf(vd1199,vd1186)!=vf(X2,vd1186)|~rcenter(vd1186,X1)|~ron(X2,X1)|~rpoint(X2)|~rpoint(vd1185)|~rpoint(vd1186)),inference(spm,[status(thm)],[2700,3802,theory(equality)])).
% cnf(35440,plain,(ron(vd1185,X1)|vd1186=vd1185|vf(vd1199,vd1186)!=vf(X2,vd1186)|~rcenter(vd1186,X1)|~ron(X2,X1)|~rpoint(X2)|$false|~rpoint(vd1186)),inference(rw,[status(thm)],[35397,862,theory(equality)])).
% cnf(35441,plain,(ron(vd1185,X1)|vd1186=vd1185|vf(vd1199,vd1186)!=vf(X2,vd1186)|~rcenter(vd1186,X1)|~ron(X2,X1)|~rpoint(X2)|$false|$false),inference(rw,[status(thm)],[35440,859,theory(equality)])).
% cnf(35442,plain,(ron(vd1185,X1)|vd1186=vd1185|vf(vd1199,vd1186)!=vf(X2,vd1186)|~rcenter(vd1186,X1)|~ron(X2,X1)|~rpoint(X2)),inference(cn,[status(thm)],[35441,theory(equality)])).
% cnf(37574,plain,(ron(X1,X2)|vd1186=vd1185|vf(X1,vd1186)!=vf(vd1199,vd1186)|~rcenter(vd1186,X2)|~ron(vd1185,X2)|~rpoint(vd1185)|~rpoint(X1)|~rpoint(vd1186)),inference(spm,[status(thm)],[2709,3802,theory(equality)])).
% cnf(37616,plain,(ron(X1,X2)|vd1186=vd1185|vf(X1,vd1186)!=vf(vd1199,vd1186)|~rcenter(vd1186,X2)|~ron(vd1185,X2)|$false|~rpoint(X1)|~rpoint(vd1186)),inference(rw,[status(thm)],[37574,862,theory(equality)])).
% cnf(37617,plain,(ron(X1,X2)|vd1186=vd1185|vf(X1,vd1186)!=vf(vd1199,vd1186)|~rcenter(vd1186,X2)|~ron(vd1185,X2)|$false|~rpoint(X1)|$false),inference(rw,[status(thm)],[37616,859,theory(equality)])).
% cnf(37618,plain,(ron(X1,X2)|vd1186=vd1185|vf(X1,vd1186)!=vf(vd1199,vd1186)|~rcenter(vd1186,X2)|~ron(vd1185,X2)|~rpoint(X1)),inference(cn,[status(thm)],[37617,theory(equality)])).
% cnf(39570,plain,(vd1186=vd1185|ron(vd1185,X1)|~rcenter(vd1186,X1)|~ron(vd1199,X1)|~rpoint(vd1199)),inference(er,[status(thm)],[35442,theory(equality)])).
% cnf(39576,plain,(vd1186=vd1185|ron(vd1185,X1)|~rcenter(vd1186,X1)|~ron(vd1199,X1)|$false),inference(rw,[status(thm)],[39570,858,theory(equality)])).
% cnf(39577,plain,(vd1186=vd1185|ron(vd1185,X1)|~rcenter(vd1186,X1)|~ron(vd1199,X1)),inference(cn,[status(thm)],[39576,theory(equality)])).
% cnf(39588,plain,(vd1186=vd1185|ron(vd1185,esk50_2(vd1186,X1))|vd1186=X1|~ron(vd1199,esk50_2(vd1186,X1))|~rpoint(vd1186)|~rpoint(X1)),inference(spm,[status(thm)],[39577,982,theory(equality)])).
% cnf(39589,plain,(vd1186=vd1185|ron(vd1185,esk50_2(vd1186,X1))|vd1186=X1|~ron(vd1199,esk50_2(vd1186,X1))|$false|~rpoint(X1)),inference(rw,[status(thm)],[39588,859,theory(equality)])).
% cnf(39590,plain,(vd1186=vd1185|ron(vd1185,esk50_2(vd1186,X1))|vd1186=X1|~ron(vd1199,esk50_2(vd1186,X1))|~rpoint(X1)),inference(cn,[status(thm)],[39589,theory(equality)])).
% cnf(55720,plain,(vd1186=vd1185|ron(vd1199,X1)|~rcenter(vd1186,X1)|~ron(vd1185,X1)|~rpoint(vd1199)),inference(er,[status(thm)],[37618,theory(equality)])).
% cnf(55726,plain,(vd1186=vd1185|ron(vd1199,X1)|~rcenter(vd1186,X1)|~ron(vd1185,X1)|$false),inference(rw,[status(thm)],[55720,858,theory(equality)])).
% cnf(55727,plain,(vd1186=vd1185|ron(vd1199,X1)|~rcenter(vd1186,X1)|~ron(vd1185,X1)),inference(cn,[status(thm)],[55726,theory(equality)])).
% cnf(55738,plain,(vd1186=vd1185|ron(vd1199,esk50_2(vd1186,X1))|vd1186=X1|~ron(vd1185,esk50_2(vd1186,X1))|~rpoint(vd1186)|~rpoint(X1)),inference(spm,[status(thm)],[55727,982,theory(equality)])).
% cnf(55739,plain,(vd1186=vd1185|ron(vd1199,esk50_2(vd1186,X1))|vd1186=X1|~ron(vd1185,esk50_2(vd1186,X1))|$false|~rpoint(X1)),inference(rw,[status(thm)],[55738,859,theory(equality)])).
% cnf(55740,plain,(vd1186=vd1185|ron(vd1199,esk50_2(vd1186,X1))|vd1186=X1|~ron(vd1185,esk50_2(vd1186,X1))|~rpoint(X1)),inference(cn,[status(thm)],[55739,theory(equality)])).
% cnf(55741,plain,(vd1186=vd1185|ron(vd1199,esk50_2(vd1186,vd1185))|~rpoint(vd1185)|~rpoint(vd1186)),inference(spm,[status(thm)],[55740,978,theory(equality)])).
% cnf(55744,plain,(vd1186=vd1185|ron(vd1199,esk50_2(vd1186,vd1185))|$false|~rpoint(vd1186)),inference(rw,[status(thm)],[55741,862,theory(equality)])).
% cnf(55745,plain,(vd1186=vd1185|ron(vd1199,esk50_2(vd1186,vd1185))|$false|$false),inference(rw,[status(thm)],[55744,859,theory(equality)])).
% cnf(55746,plain,(vd1186=vd1185|ron(vd1199,esk50_2(vd1186,vd1185))),inference(cn,[status(thm)],[55745,theory(equality)])).
% cnf(55799,plain,(vf(vd1186,X1)=vf(vd1186,vd1199)|vd1186=vd1185|~ron(X1,esk50_2(vd1186,vd1185))|~rpoint(vd1199)|~rpoint(X1)|~rpoint(vd1186)|~rpoint(vd1185)),inference(spm,[status(thm)],[2578,55746,theory(equality)])).
% cnf(55832,plain,(vd1186=vd1185|ron(vd1185,esk50_2(vd1186,vd1185))|~rpoint(vd1185)),inference(spm,[status(thm)],[39590,55746,theory(equality)])).
% cnf(55929,plain,(vf(vd1186,X1)=vf(vd1186,vd1199)|vd1186=vd1185|~ron(X1,esk50_2(vd1186,vd1185))|$false|~rpoint(X1)|~rpoint(vd1186)|~rpoint(vd1185)),inference(rw,[status(thm)],[55799,858,theory(equality)])).
% cnf(55930,plain,(vf(vd1186,X1)=vf(vd1186,vd1199)|vd1186=vd1185|~ron(X1,esk50_2(vd1186,vd1185))|$false|~rpoint(X1)|$false|~rpoint(vd1185)),inference(rw,[status(thm)],[55929,859,theory(equality)])).
% cnf(55931,plain,(vf(vd1186,X1)=vf(vd1186,vd1199)|vd1186=vd1185|~ron(X1,esk50_2(vd1186,vd1185))|$false|~rpoint(X1)|$false|$false),inference(rw,[status(thm)],[55930,862,theory(equality)])).
% cnf(55932,plain,(vf(vd1186,X1)=vf(vd1186,vd1199)|vd1186=vd1185|~ron(X1,esk50_2(vd1186,vd1185))|~rpoint(X1)),inference(cn,[status(thm)],[55931,theory(equality)])).
% cnf(55939,plain,(vd1186=vd1185|ron(vd1185,esk50_2(vd1186,vd1185))|$false),inference(rw,[status(thm)],[55832,862,theory(equality)])).
% cnf(55940,plain,(vd1186=vd1185|ron(vd1185,esk50_2(vd1186,vd1185))),inference(cn,[status(thm)],[55939,theory(equality)])).
% cnf(56180,plain,(vf(vd1186,vd1185)=vf(vd1186,vd1199)|vd1186=vd1185|~rpoint(vd1185)),inference(spm,[status(thm)],[55932,55940,theory(equality)])).
% cnf(56185,plain,(vf(vd1186,vd1185)=vf(vd1186,vd1199)|vd1186=vd1185|$false),inference(rw,[status(thm)],[56180,862,theory(equality)])).
% cnf(56186,plain,(vf(vd1186,vd1185)=vf(vd1186,vd1199)|vd1186=vd1185),inference(cn,[status(thm)],[56185,theory(equality)])).
% cnf(56201,plain,(vd1185=vd1186|vf(vd1186,vd1199)!=v0|~rpoint(vd1186)|~rpoint(vd1185)),inference(spm,[status(thm)],[914,56186,theory(equality)])).
% cnf(56293,plain,(vd1185=vd1186|vf(vd1186,vd1199)!=v0|$false|~rpoint(vd1185)),inference(rw,[status(thm)],[56201,859,theory(equality)])).
% cnf(56294,plain,(vd1185=vd1186|vf(vd1186,vd1199)!=v0|$false|$false),inference(rw,[status(thm)],[56293,862,theory(equality)])).
% cnf(56295,plain,(vd1185=vd1186|vf(vd1186,vd1199)!=v0),inference(cn,[status(thm)],[56294,theory(equality)])).
% cnf(144654,plain,(vf(vd1199,vd1185)=X1|vplus(vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)),X1)!=vf(vd1199,esk13_4(vd1197,vd1197,vd1199,vd1185))|~rreal(vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)))|~rreal(X1)|$false),inference(rw,[status(thm)],[4863,8771,theory(equality)])).
% cnf(144655,plain,(vf(vd1199,vd1185)=X1|vplus(vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)),X1)!=vf(vd1199,esk13_4(vd1197,vd1197,vd1199,vd1185))|~rreal(vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)))|~rreal(X1)),inference(cn,[status(thm)],[144654,theory(equality)])).
% cnf(144656,plain,(vf(vd1199,vd1185)=X1|vplus(vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)),X1)!=vf(vd1199,esk13_4(vd1197,vd1197,vd1199,vd1185))|~rreal(X1)|~rpoint(vd1185)|~rpoint(esk13_4(vd1197,vd1197,vd1199,vd1185))),inference(spm,[status(thm)],[144655,2038,theory(equality)])).
% cnf(144657,plain,(vf(vd1199,vd1185)=X1|vplus(vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)),X1)!=vf(vd1199,esk13_4(vd1197,vd1197,vd1199,vd1185))|~rreal(X1)|$false|~rpoint(esk13_4(vd1197,vd1197,vd1199,vd1185))),inference(rw,[status(thm)],[144656,862,theory(equality)])).
% cnf(144658,plain,(vf(vd1199,vd1185)=X1|vplus(vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)),X1)!=vf(vd1199,esk13_4(vd1197,vd1197,vd1199,vd1185))|~rreal(X1)|$false|$false),inference(rw,[status(thm)],[144657,3955,theory(equality)])).
% cnf(144659,plain,(vf(vd1199,vd1185)=X1|vplus(vf(vd1185,esk13_4(vd1197,vd1197,vd1199,vd1185)),X1)!=vf(vd1199,esk13_4(vd1197,vd1197,vd1199,vd1185))|~rreal(X1)),inference(cn,[status(thm)],[144658,theory(equality)])).
% cnf(150289,plain,(vf(vd1199,vd1185)=vf(vd1185,vd1199)|~rreal(vf(vd1185,vd1199))),inference(spm,[status(thm)],[144659,21161,theory(equality)])).
% cnf(150292,plain,(vf(vd1199,vd1185)=vf(vd1185,vd1199)|$false),inference(rw,[status(thm)],[150289,8858,theory(equality)])).
% cnf(150293,plain,(vf(vd1199,vd1185)=vf(vd1185,vd1199)),inference(cn,[status(thm)],[150292,theory(equality)])).
% cnf(150305,plain,(vd1199=vd1185|vf(vd1199,vd1185)!=v0|~rpoint(vd1185)|~rpoint(vd1199)),inference(spm,[status(thm)],[914,150293,theory(equality)])).
% cnf(150410,plain,(vd1199=vd1185|vf(vd1199,vd1185)!=v0|$false|~rpoint(vd1199)),inference(rw,[status(thm)],[150305,862,theory(equality)])).
% cnf(150411,plain,(vd1199=vd1185|vf(vd1199,vd1185)!=v0|$false|$false),inference(rw,[status(thm)],[150410,858,theory(equality)])).
% cnf(150412,plain,(vd1199=vd1185|vf(vd1199,vd1185)!=v0),inference(cn,[status(thm)],[150411,theory(equality)])).
% cnf(150413,plain,(vf(vd1199,vd1185)!=v0),inference(sr,[status(thm)],[150412,171,theory(equality)])).
% cnf(464520,plain,(X1=vd1185|vd1199=vd1185|X1=vd1199|rR(X1,vd1199,vd1185)|rR(vd1199,vd1185,X1)|rR(vd1185,vd1199,X1)|~ron(X1,vd1197)|~rpoint(vd1199)|~rpoint(X1)),inference(spm,[status(thm)],[12579,284,theory(equality)])).
% cnf(464763,plain,(X1=vd1185|vd1199=vd1185|X1=vd1199|rR(X1,vd1199,vd1185)|rR(vd1199,vd1185,X1)|rR(vd1185,vd1199,X1)|~ron(X1,vd1197)|$false|~rpoint(X1)),inference(rw,[status(thm)],[464520,858,theory(equality)])).
% cnf(464764,plain,(X1=vd1185|vd1199=vd1185|X1=vd1199|rR(X1,vd1199,vd1185)|rR(vd1199,vd1185,X1)|rR(vd1185,vd1199,X1)|~ron(X1,vd1197)|~rpoint(X1)),inference(cn,[status(thm)],[464763,theory(equality)])).
% cnf(464765,plain,(X1=vd1185|X1=vd1199|rR(X1,vd1199,vd1185)|rR(vd1199,vd1185,X1)|rR(vd1185,vd1199,X1)|~ron(X1,vd1197)|~rpoint(X1)),inference(sr,[status(thm)],[464764,171,theory(equality)])).
% cnf(464915,plain,(vd1186=vd1199|vd1186=vd1185|rR(vd1185,vd1199,vd1186)|rR(vd1199,vd1185,vd1186)|rR(vd1186,vd1199,vd1185)|~rpoint(vd1186)),inference(spm,[status(thm)],[464765,275,theory(equality)])).
% cnf(465161,plain,(vd1186=vd1199|vd1186=vd1185|rR(vd1185,vd1199,vd1186)|rR(vd1199,vd1185,vd1186)|rR(vd1186,vd1199,vd1185)|$false),inference(rw,[status(thm)],[464915,859,theory(equality)])).
% cnf(465162,plain,(vd1186=vd1199|vd1186=vd1185|rR(vd1185,vd1199,vd1186)|rR(vd1199,vd1185,vd1186)|rR(vd1186,vd1199,vd1185)),inference(cn,[status(thm)],[465161,theory(equality)])).
% cnf(465163,plain,(vd1186=vd1199|vd1186=vd1185|rR(vd1199,vd1185,vd1186)|rR(vd1186,vd1199,vd1185)),inference(sr,[status(thm)],[465162,855,theory(equality)])).
% cnf(465164,plain,(vd1186=vd1199|vd1186=vd1185|rR(vd1186,vd1199,vd1185)),inference(sr,[status(thm)],[465163,856,theory(equality)])).
% cnf(465165,plain,(vd1186=vd1199|vd1186=vd1185),inference(sr,[status(thm)],[465164,170,theory(equality)])).
% cnf(465170,plain,(vf(vd1185,vd1185)=vf(vd1199,vd1185)|vd1186=vd1199),inference(spm,[status(thm)],[872,465165,theory(equality)])).
% cnf(468455,plain,(vf(vd1199,vd1185)=v0|vd1186=vd1199|~rpoint(vd1185)),inference(spm,[status(thm)],[897,465170,theory(equality)])).
% cnf(468568,plain,(vf(vd1199,vd1185)=v0|vd1186=vd1199|$false),inference(rw,[status(thm)],[468455,862,theory(equality)])).
% cnf(468569,plain,(vf(vd1199,vd1185)=v0|vd1186=vd1199),inference(cn,[status(thm)],[468568,theory(equality)])).
% cnf(468570,plain,(vd1186=vd1199),inference(sr,[status(thm)],[468569,150413,theory(equality)])).
% cnf(475952,plain,(vd1199=vd1185|vf(vd1186,vd1199)!=v0),inference(rw,[status(thm)],[56295,468570,theory(equality)])).
% cnf(475953,plain,(vd1199=vd1185|vf(vd1199,vd1199)!=v0),inference(rw,[status(thm)],[475952,468570,theory(equality)])).
% cnf(475954,plain,(vf(vd1199,vd1199)!=v0),inference(sr,[status(thm)],[475953,171,theory(equality)])).
% cnf(479476,plain,(~rpoint(vd1199)),inference(spm,[status(thm)],[475954,897,theory(equality)])).
% cnf(479481,plain,($false),inference(rw,[status(thm)],[479476,858,theory(equality)])).
% cnf(479482,plain,($false),inference(cn,[status(thm)],[479481,theory(equality)])).
% cnf(479483,plain,($false),479482,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses                  : 21454
% # ...of these trivial                : 33
% # ...subsumed                        : 12180
% # ...remaining for further processing: 9241
% # Other redundant clauses eliminated : 1112
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed                  : 2139
% # Backward-rewritten                 : 3821
% # Generated clauses                  : 166732
% # ...of the previous two non-trivial : 163801
% # Contextual simplify-reflections    : 8681
% # Paramodulations                    : 166346
% # Factorizations                     : 97
% # Equation resolutions               : 1161
% # Current number of processed clauses: 3041
% #    Positive orientable unit clauses: 395
% #    Positive unorientable unit clauses: 0
% #    Negative unit clauses           : 597
% #    Non-unit-clauses                : 2049
% # Current number of unprocessed clauses: 41926
% # ...number of literals in the above : 271014
% # Clause-clause subsumption calls (NU) : 1449363
% # Rec. Clause-clause subsumption calls : 641310
% # Unit Clause-clause subsumption calls : 84436
% # Rewrite failures with RHS unbound  : 0
% # Indexed BW rewrite attempts        : 29880
% # Indexed BW rewrite successes       : 20
% # Backwards rewriting index:   897 leaves,   4.25+/-9.296 terms/leaf
% # Paramod-from index:          270 leaves,   3.46+/-6.754 terms/leaf
% # Paramod-into index:          535 leaves,   4.30+/-9.105 terms/leaf
% # -------------------------------------------------
% # User time              : 22.952 s
% # System time            : 0.520 s
% # Total time             : 23.471 s
% # Maximum resident set size: 0 pages
% PrfWatch: 32.34 CPU 33.04 WC
% FINAL PrfWatch: 32.34 CPU 33.04 WC
% SZS output end Solution for /tmp/SystemOnTPTP26913/GEO290+1.tptp
% 
%------------------------------------------------------------------------------