%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO277+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:26:18 PM UTC 2026
% Result : Theorem 0.95s 0.64s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO277+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n017.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 20 14:58:10 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.39 % Drodi V4.1.1
% 0.95/0.64 % Refutation found
% 0.95/0.64 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.95/0.64 % SZS output start CNFRefutation for theBenchmark
% 0.95/0.64 fof(f1,conjecture,(
% 0.95/0.64 (! [Vdthex] :( ( ron(vd1085,Vdthex)& ron(vd1089,Vdthex)& rline(Vdthex) )=> Vdthex = vd1099 ) )),
% 0.95/0.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.95/0.64 fof(f2,negated_conjecture,(
% 0.95/0.64 ~((! [Vdthex] :( ( ron(vd1085,Vdthex)& ron(vd1089,Vdthex)& rline(Vdthex) )=> Vdthex = vd1099 ) ))),
% 0.95/0.64 inference(negated_conjecture,[status(cth)],[f1])).
% 0.95/0.64 fof(f3,axiom,(
% 0.95/0.64 ( ron(vd1085,vd1099)& ron(vd1089,vd1099)& rline(vd1099) ) ),
% 0.95/0.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.95/0.64 fof(f9,axiom,(
% 0.95/0.64 rpoint(vd1089) ),
% 0.95/0.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.95/0.64 fof(f10,axiom,(
% 0.95/0.64 vd1085 = vd1086 ),
% 0.95/0.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.95/0.64 fof(f11,axiom,(
% 0.95/0.64 rpoint(vd1086) ),
% 0.95/0.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.95/0.64 fof(f14,axiom,(
% 0.95/0.64 vf(vd1089,vd1085) = vf(vd1089,vd1080) ),
% 0.95/0.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.95/0.64 fof(f15,axiom,(
% 0.95/0.64 vd1085 != vd1081 ),
% 0.95/0.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.95/0.64 fof(f16,axiom,(
% 0.95/0.64 vd1085 != vd1080 ),
% 0.95/0.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.95/0.64 fof(f19,axiom,(
% 0.95/0.64 ( ron(vd1081,vskolem1095)& rcenter(vd1080,vskolem1095)& rcircle(vskolem1095) ) ),
% 0.95/0.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.95/0.64 fof(f23,axiom,(
% 0.95/0.64 (? [Vd1084] :( vd1081 = Vd1084& rpoint(Vd1084) ) )),
% 0.95/0.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.95/0.64 fof(f24,axiom,(
% 0.95/0.64 (? [Vd1083] :( vd1080 = Vd1083& rpoint(Vd1083) ) )),
% 0.95/0.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.95/0.64 fof(f36,axiom,(
% 0.95/0.64 (! [Vd748,Vd749] :( ( (? [Vd752] :( Vd749 = Vd752& rpoint(Vd752) ))& (? [Vd751] :( Vd748 = Vd751& rpoint(Vd751) ) ))=> ( vf(Vd748,Vd749) = v0<=> Vd748 = Vd749 ) ) )),
% 0.95/0.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.95/0.64 fof(f38,axiom,(
% 0.95/0.64 (! [Vd314,Vd315,Vd319,Vd320] :( ( ron(Vd315,Vd320)& ron(Vd315,Vd319)& ron(Vd314,Vd320)& ron(Vd314,Vd319)& (? [Vd324] :( Vd320 = Vd324& rline(Vd324) ))& (? [Vd323] :( Vd319 = Vd323& rline(Vd323) ))& Vd314 != Vd315& (? [Vd318] :( Vd315 = Vd318& rpoint(Vd318) ))& (? [Vd317] :( Vd314 = Vd317& rpoint(Vd317) ) ))=> Vd319 = Vd320 ) )),
% 0.95/0.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.95/0.64 fof(f53,axiom,(
% 0.95/0.64 v0 = vd684 ),
% 0.95/0.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.95/0.64 fof(f54,axiom,(
% 0.95/0.64 rreal(vd684) ),
% 0.95/0.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.95/0.64 fof(f104,axiom,(
% 0.95/0.64 (! [Vd52,Vd53] :( ( Vd52 = Vd53& rline(Vd53) )=> (? [Vd54] :( ron(Vd54,Vd52)& rpoint(Vd54) ) )) )),
% 0.95/0.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.95/0.64 fof(f108,axiom,(
% 0.95/0.64 (! [Vd15,Vd16] :( ( Vd15 = Vd16& rpoint(Vd16) )=> (? [Vd17] :( Vd17 != Vd15& rpoint(Vd17) ) )) )),
% 0.95/0.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.95/0.64 fof(f109,axiom,(
% 0.95/0.64 rpoint(vd14) ),
% 0.95/0.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.95/0.64 fof(f129,plain,(
% 0.95/0.64 (?[Vdthex]: (((ron(vd1085,Vdthex)&ron(vd1089,Vdthex))&rline(Vdthex))&~Vdthex=vd1099))),
% 0.95/0.64 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.95/0.64 fof(f130,plain,(
% 0.95/0.64 (((ron(vd1085,sK0_skl)&ron(vd1089,sK0_skl))&rline(sK0_skl))&~sK0_skl=vd1099)),
% 0.95/0.64 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Vdthex,sK0_skl)],[f129])).
% 0.95/0.64 fof(f131,plain,(
% 0.95/0.64 ron(vd1085,sK0_skl)),
% 0.95/0.64 inference(cnf_transformation,[status(thm)],[f130])).
% 0.95/0.64 fof(f132,plain,(
% 0.95/0.64 ron(vd1089,sK0_skl)),
% 0.95/0.64 inference(cnf_transformation,[status(thm)],[f130])).
% 0.95/0.64 fof(f133,plain,(
% 0.95/0.64 rline(sK0_skl)),
% 0.95/0.64 inference(cnf_transformation,[status(thm)],[f130])).
% 0.95/0.64 fof(f134,plain,(
% 0.95/0.64 ~sK0_skl=vd1099),
% 0.95/0.64 inference(cnf_transformation,[status(thm)],[f130])).
% 0.95/0.64 fof(f135,plain,(
% 0.95/0.64 ron(vd1085,vd1099)),
% 0.95/0.64 inference(cnf_transformation,[status(thm)],[f3])).
% 0.95/0.64 fof(f136,plain,(
% 0.95/0.64 ron(vd1089,vd1099)),
% 0.95/0.64 inference(cnf_transformation,[status(thm)],[f3])).
% 0.95/0.64 fof(f137,plain,(
% 0.95/0.64 rline(vd1099)),
% 0.95/0.64 inference(cnf_transformation,[status(thm)],[f3])).
% 0.95/0.64 fof(f145,plain,(
% 0.95/0.64 rpoint(vd1089)),
% 0.95/0.64 inference(cnf_transformation,[status(thm)],[f9])).
% 0.95/0.64 fof(f146,plain,(
% 0.95/0.64 vd1085=vd1086),
% 0.95/0.64 inference(cnf_transformation,[status(thm)],[f10])).
% 0.95/0.64 fof(f147,plain,(
% 0.95/0.64 rpoint(vd1086)),
% 0.95/0.64 inference(cnf_transformation,[status(thm)],[f11])).
% 0.95/0.64 fof(f154,plain,(
% 0.95/0.64 vf(vd1089,vd1085)=vf(vd1089,vd1080)),
% 0.95/0.64 inference(cnf_transformation,[status(thm)],[f14])).
% 0.95/0.64 fof(f155,plain,(
% 0.95/0.64 ~vd1085=vd1081),
% 0.95/0.64 inference(cnf_transformation,[status(thm)],[f15])).
% 0.95/0.64 fof(f156,plain,(
% 0.95/0.64 ~vd1085=vd1080),
% 0.95/0.64 inference(cnf_transformation,[status(thm)],[f16])).
% 0.95/0.64 fof(f162,plain,(
% 0.95/0.64 rcircle(vskolem1095)),
% 0.95/0.64 inference(cnf_transformation,[status(thm)],[f19])).
% 0.95/0.64 fof(f167,plain,(
% 0.95/0.64 (vd1081=sK2_skl&rpoint(sK2_skl))),
% 0.95/0.64 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(Vd1084,sK2_skl)],[f23])).
% 0.95/0.64 fof(f168,plain,(
% 0.95/0.64 vd1081=sK2_skl),
% 0.95/0.64 inference(cnf_transformation,[status(thm)],[f167])).
% 0.95/0.64 fof(f170,plain,(
% 0.95/0.64 (vd1080=sK3_skl&rpoint(sK3_skl))),
% 0.95/0.64 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(Vd1083,sK3_skl)],[f24])).
% 0.95/0.64 fof(f171,plain,(
% 0.95/0.64 vd1080=sK3_skl),
% 0.95/0.64 inference(cnf_transformation,[status(thm)],[f170])).
% 0.95/0.64 fof(f172,plain,(
% 0.95/0.64 rpoint(sK3_skl)),
% 0.95/0.64 inference(cnf_transformation,[status(thm)],[f170])).
% 0.95/0.64 fof(f219,plain,(
% 0.95/0.64 ![Vd748,Vd749]: (((![Vd752]: (~Vd749=Vd752|~rpoint(Vd752)))|(![Vd751]: (~Vd748=Vd751|~rpoint(Vd751))))|(vf(Vd748,Vd749)=v0<=>Vd748=Vd749))),
% 0.95/0.64 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.95/0.64 fof(f220,plain,(
% 0.95/0.64 ![Vd748,Vd749]: (((![Vd752]: (~Vd749=Vd752|~rpoint(Vd752)))|(![Vd751]: (~Vd748=Vd751|~rpoint(Vd751))))|((~vf(Vd748,Vd749)=v0|Vd748=Vd749)&(vf(Vd748,Vd749)=v0|~Vd748=Vd749)))),
% 0.95/0.64 inference(NNF_transformation,[status(thm)],[f219])).
% 0.95/0.64 fof(f221,plain,(
% 0.95/0.64 ![X0,X1,X2,X3]: (~X0=X1|~rpoint(X1)|~X2=X3|~rpoint(X3)|~vf(X2,X0)=v0|X2=X0)),
% 0.95/0.64 inference(cnf_transformation,[status(thm)],[f220])).
% 0.95/0.64 fof(f222,plain,(
% 0.95/0.64 ![X0,X1,X2,X3]: (~X0=X1|~rpoint(X1)|~X2=X3|~rpoint(X3)|vf(X2,X0)=v0|~X2=X0)),
% 0.95/0.64 inference(cnf_transformation,[status(thm)],[f220])).
% 0.95/0.64 fof(f226,plain,(
% 0.95/0.64 ![Vd314,Vd315,Vd319,Vd320]: (((((((((~ron(Vd315,Vd320)|~ron(Vd315,Vd319))|~ron(Vd314,Vd320))|~ron(Vd314,Vd319))|(![Vd324]: (~Vd320=Vd324|~rline(Vd324))))|(![Vd323]: (~Vd319=Vd323|~rline(Vd323))))|Vd314=Vd315)|(![Vd318]: (~Vd315=Vd318|~rpoint(Vd318))))|(![Vd317]: (~Vd314=Vd317|~rpoint(Vd317))))|Vd319=Vd320)),
% 0.95/0.64 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 0.95/0.64 fof(f227,plain,(
% 0.95/0.64 ![Vd319,Vd320]: ((![Vd314]: ((![Vd315]: (((((((~ron(Vd315,Vd320)|~ron(Vd315,Vd319))|~ron(Vd314,Vd320))|~ron(Vd314,Vd319))|(![Vd324]: (~Vd320=Vd324|~rline(Vd324))))|(![Vd323]: (~Vd319=Vd323|~rline(Vd323))))|Vd314=Vd315)|(![Vd318]: (~Vd315=Vd318|~rpoint(Vd318)))))|(![Vd317]: (~Vd314=Vd317|~rpoint(Vd317)))))|Vd319=Vd320)),
% 0.95/0.64 inference(miniscoping,[status(thm)],[f226])).
% 0.95/0.64 fof(f228,plain,(
% 0.95/0.64 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~ron(X0,X1)|~ron(X0,X2)|~ron(X3,X1)|~ron(X3,X2)|~X1=X4|~rline(X4)|~X2=X5|~rline(X5)|X3=X0|~X0=X6|~rpoint(X6)|~X3=X7|~rpoint(X7)|X2=X1)),
% 0.95/0.64 inference(cnf_transformation,[status(thm)],[f227])).
% 0.95/0.64 fof(f284,plain,(
% 0.95/0.64 v0=vd684),
% 0.95/0.64 inference(cnf_transformation,[status(thm)],[f53])).
% 0.95/0.64 fof(f285,plain,(
% 0.95/0.64 rreal(vd684)),
% 0.95/0.64 inference(cnf_transformation,[status(thm)],[f54])).
% 0.95/0.64 fof(f516,plain,(
% 0.95/0.64 ![Vd52,Vd53]: ((~Vd52=Vd53|~rline(Vd53))|(?[Vd54]: (ron(Vd54,Vd52)&rpoint(Vd54))))),
% 0.95/0.64 inference(pre_NNF_transformation,[status(thm)],[f104])).
% 0.95/0.64 fof(f517,plain,(
% 0.95/0.64 ![Vd52]: ((![Vd53]: (~Vd52=Vd53|~rline(Vd53)))|(?[Vd54]: (ron(Vd54,Vd52)&rpoint(Vd54))))),
% 0.95/0.64 inference(miniscoping,[status(thm)],[f516])).
% 0.95/0.64 fof(f518,plain,(
% 0.95/0.64 ![Vd52]: ((![Vd53]: (~Vd52=Vd53|~rline(Vd53)))|(ron(sK39_skl(Vd52),Vd52)&rpoint(sK39_skl(Vd52))))),
% 0.95/0.64 inference(skolemize,[status(esa),new_symbols(skolem,[sK39_skl]),skolemize(Vd54,sK39_skl(Vd52))],[f517])).
% 0.95/0.64 fof(f520,plain,(
% 0.95/0.64 ![X0,X1]: (~X0=X1|~rline(X1)|rpoint(sK39_skl(X0)))),
% 0.95/0.64 inference(cnf_transformation,[status(thm)],[f518])).
% 0.95/0.64 fof(f539,plain,(
% 0.95/0.64 ![Vd15,Vd16]: ((~Vd15=Vd16|~rpoint(Vd16))|(?[Vd17]: (~Vd17=Vd15&rpoint(Vd17))))),
% 0.95/0.64 inference(pre_NNF_transformation,[status(thm)],[f108])).
% 0.95/0.64 fof(f540,plain,(
% 0.95/0.64 ![Vd15]: ((![Vd16]: (~Vd15=Vd16|~rpoint(Vd16)))|(?[Vd17]: (~Vd17=Vd15&rpoint(Vd17))))),
% 0.95/0.64 inference(miniscoping,[status(thm)],[f539])).
% 0.95/0.64 fof(f541,plain,(
% 0.95/0.64 ![Vd15]: ((![Vd16]: (~Vd15=Vd16|~rpoint(Vd16)))|(~sK43_skl(Vd15)=Vd15&rpoint(sK43_skl(Vd15))))),
% 0.95/0.64 inference(skolemize,[status(esa),new_symbols(skolem,[sK43_skl]),skolemize(Vd17,sK43_skl(Vd15))],[f540])).
% 0.95/0.64 fof(f542,plain,(
% 0.95/0.64 ![X0,X1]: (~X0=X1|~rpoint(X1)|~sK43_skl(X0)=X0)),
% 0.95/0.64 inference(cnf_transformation,[status(thm)],[f541])).
% 0.95/0.64 fof(f543,plain,(
% 0.95/0.64 ![X0,X1]: (~X0=X1|~rpoint(X1)|rpoint(sK43_skl(X0)))),
% 0.95/0.64 inference(cnf_transformation,[status(thm)],[f541])).
% 0.95/0.64 fof(f544,plain,(
% 0.95/0.64 rpoint(vd14)),
% 0.95/0.64 inference(cnf_transformation,[status(thm)],[f109])).
% 0.95/0.64 fof(f716,plain,(
% 0.95/0.64 ![X0,X1]: (~rpoint(X0)|~rpoint(X1)|~vf(X1,X0)=v0|X1=X0)),
% 0.95/0.64 inference(destructive_equality_resolution,[status(thm)],[f221])).
% 0.95/0.64 fof(f717,plain,(
% 0.95/0.64 ![X1]: (~rpoint(X1)|~rpoint(X1)|vf(X1,X1)=v0)),
% 0.95/0.64 inference(destructive_equality_resolution,[status(thm)],[f222])).
% 0.95/0.64 fof(f718,plain,(
% 0.95/0.64 ![X0]: (~rpoint(X0)|vf(X0,X0)=v0)),
% 0.95/0.64 inference(duplicate_literals_removal,[status(thm)],[f717])).
% 0.95/0.64 fof(f720,plain,(
% 0.95/0.64 ![X0,X1,X2,X3]: (~ron(X0,X1)|~ron(X0,X2)|~ron(X3,X1)|~ron(X3,X2)|~rline(X1)|~rline(X2)|X3=X0|~rpoint(X0)|~rpoint(X3)|X2=X1)),
% 0.95/0.64 inference(destructive_equality_resolution,[status(thm)],[f228])).
% 0.95/0.64 fof(f846,plain,(
% 0.95/0.64 ![X0]: (~rline(X0)|rpoint(sK39_skl(X0)))),
% 0.95/0.64 inference(destructive_equality_resolution,[status(thm)],[f520])).
% 0.95/0.64 fof(f859,plain,(
% 0.95/0.64 ![X0]: (~rpoint(X0)|~sK43_skl(X0)=X0)),
% 0.95/0.64 inference(destructive_equality_resolution,[status(thm)],[f542])).
% 0.95/0.64 fof(f860,plain,(
% 0.95/0.64 ![X0]: (~rpoint(X0)|rpoint(sK43_skl(X0)))),
% 0.95/0.64 inference(destructive_equality_resolution,[status(thm)],[f543])).
% 0.95/0.64 fof(f907,plain,(
% 0.95/0.64 ![X0,X1]: (~ron(vd1089,X0)|~ron(X1,X0)|~ron(X1,sK0_skl)|~rline(X0)|~rline(sK0_skl)|X1=vd1089|~rpoint(vd1089)|~rpoint(X1)|sK0_skl=X0)),
% 0.95/0.64 inference(resolution,[status(thm)],[f720,f132])).
% 0.95/0.64 fof(f927,definition,(
% 0.95/0.64 sQ9_spl <=> (rline(vd1099))),
% 0.95/0.64 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.95/0.64 fof(f929,plain,(
% 0.95/0.64 ~rline(vd1099)|sQ9_spl),
% 0.95/0.64 inference(component_clause,[status(thm)],[f927])).
% 0.95/0.64 fof(f933,definition,(
% 0.95/0.64 sQ11_spl <=> (rpoint(vd1089))),
% 0.95/0.64 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.95/0.64 fof(f935,plain,(
% 0.95/0.64 ~rpoint(vd1089)|sQ11_spl),
% 0.95/0.64 inference(component_clause,[status(thm)],[f933])).
% 0.95/0.64 fof(f947,definition,(
% 0.95/0.64 sQ15_spl <=> (rline(sK0_skl))),
% 0.95/0.64 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.95/0.64 fof(f949,plain,(
% 0.95/0.64 ~rline(sK0_skl)|sQ15_spl),
% 0.95/0.64 inference(component_clause,[status(thm)],[f947])).
% 0.95/0.64 fof(f954,definition,(
% 0.95/0.64 ![X0,X1]: (sQ17_spl <=> (~ron(vd1089,X0)|~ron(X1,X0)|~ron(X1,sK0_skl)|~rline(X0)|X1=vd1089|~rpoint(X1)|sK0_skl=X0))),
% 0.95/0.64 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.95/0.64 fof(f955,plain,(
% 0.95/0.64 ![X0,X1]: (~ron(vd1089,X0)|~ron(X1,X0)|~ron(X1,sK0_skl)|~rline(X0)|X1=vd1089|~rpoint(X1)|sK0_skl=X0|~sQ17_spl)),
% 0.95/0.64 inference(component_clause,[status(thm)],[f954])).
% 0.95/0.64 fof(f957,plain,(
% 0.95/0.64 sQ17_spl|~sQ15_spl|~sQ11_spl),
% 0.95/0.64 inference(split_clause,[status(thm)],[f907,f954,f947,f933])).
% 0.95/0.64 fof(f964,definition,(
% 0.95/0.64 sQ20_spl <=> (rpoint(vd1085))),
% 0.95/0.64 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.95/0.64 fof(f966,plain,(
% 0.95/0.64 ~rpoint(vd1085)|sQ20_spl),
% 0.95/0.64 inference(component_clause,[status(thm)],[f964])).
% 0.95/0.64 fof(f972,definition,(
% 0.95/0.64 sQ22_spl <=> (ron(vd1085,sK0_skl))),
% 0.95/0.64 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.95/0.64 fof(f974,plain,(
% 0.95/0.64 ~ron(vd1085,sK0_skl)|sQ22_spl),
% 0.95/0.64 inference(component_clause,[status(thm)],[f972])).
% 0.95/0.64 fof(f1004,plain,(
% 0.95/0.64 $false|sQ15_spl),
% 0.95/0.64 inference(forward_subsumption_resolution,[status(thm)],[f949,f133])).
% 0.95/0.64 fof(f1005,plain,(
% 0.95/0.64 sQ15_spl),
% 0.95/0.64 inference(contradiction_clause,[status(thm)],[f1004])).
% 0.95/0.64 fof(f1006,plain,(
% 0.95/0.64 $false|sQ11_spl),
% 0.95/0.64 inference(forward_subsumption_resolution,[status(thm)],[f935,f145])).
% 0.95/0.64 fof(f1007,plain,(
% 0.95/0.64 sQ11_spl),
% 0.95/0.64 inference(contradiction_clause,[status(thm)],[f1006])).
% 0.95/0.64 fof(f1008,plain,(
% 0.95/0.64 $false|sQ9_spl),
% 0.95/0.64 inference(forward_subsumption_resolution,[status(thm)],[f929,f137])).
% 0.95/0.64 fof(f1009,plain,(
% 0.95/0.64 sQ9_spl),
% 0.95/0.64 inference(contradiction_clause,[status(thm)],[f1008])).
% 0.95/0.64 fof(f1010,plain,(
% 0.95/0.64 ![X0]: (~ron(X0,vd1099)|~ron(X0,sK0_skl)|~rline(vd1099)|X0=vd1089|~rpoint(X0)|sK0_skl=vd1099|~sQ17_spl)),
% 0.95/0.64 inference(resolution,[status(thm)],[f955,f136])).
% 0.95/0.64 fof(f1012,definition,(
% 0.95/0.64 ![X0]: (sQ28_spl <=> (~ron(X0,vd1099)|~ron(X0,sK0_skl)|X0=vd1089|~rpoint(X0)))),
% 0.95/0.64 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.95/0.64 fof(f1013,plain,(
% 0.95/0.64 ![X0]: (~ron(X0,vd1099)|~ron(X0,sK0_skl)|X0=vd1089|~rpoint(X0)|~sQ28_spl)),
% 0.95/0.64 inference(component_clause,[status(thm)],[f1012])).
% 0.95/0.64 fof(f1015,definition,(
% 0.95/0.64 sQ29_spl <=> (sK0_skl=vd1099)),
% 0.95/0.64 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.95/0.64 fof(f1016,plain,(
% 0.95/0.64 sK0_skl=vd1099|~sQ29_spl),
% 0.95/0.64 inference(component_clause,[status(thm)],[f1015])).
% 0.95/0.64 fof(f1018,plain,(
% 0.95/0.64 sQ28_spl|~sQ9_spl|sQ29_spl|~sQ17_spl),
% 0.95/0.64 inference(split_clause,[status(thm)],[f1010,f1012,f927,f1015,f954])).
% 0.95/0.64 fof(f1021,plain,(
% 0.95/0.64 ~ron(vd1085,sK0_skl)|vd1085=vd1089|~rpoint(vd1085)|~sQ28_spl),
% 0.95/0.64 inference(resolution,[status(thm)],[f1013,f135])).
% 0.95/0.64 fof(f1023,definition,(
% 0.95/0.64 sQ30_spl <=> (vd1085=vd1089)),
% 0.95/0.64 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.95/0.64 fof(f1024,plain,(
% 0.95/0.64 vd1085=vd1089|~sQ30_spl),
% 0.95/0.64 inference(component_clause,[status(thm)],[f1023])).
% 0.95/0.64 fof(f1026,plain,(
% 0.95/0.64 ~sQ22_spl|sQ30_spl|~sQ20_spl|~sQ28_spl),
% 0.95/0.64 inference(split_clause,[status(thm)],[f1021,f972,f1023,f964,f1012])).
% 0.95/0.64 fof(f1031,plain,(
% 0.95/0.64 $false|~sQ29_spl),
% 0.95/0.64 inference(forward_subsumption_resolution,[status(thm)],[f1016,f134])).
% 0.95/0.64 fof(f1032,plain,(
% 0.95/0.64 ~sQ29_spl),
% 0.95/0.64 inference(contradiction_clause,[status(thm)],[f1031])).
% 0.95/0.64 fof(f1042,plain,(
% 0.95/0.64 ~rpoint(vd1086)|sQ20_spl),
% 0.95/0.64 inference(backward_demodulation,[status(thm)],[f146,f966])).
% 0.95/0.64 fof(f1043,plain,(
% 0.95/0.64 vf(vd1089,vd1086)=vf(vd1089,vd1080)),
% 0.95/0.64 inference(backward_demodulation,[status(thm)],[f146,f154])).
% 0.95/0.64 fof(f1045,plain,(
% 0.95/0.64 ~vd1086=vd1080),
% 0.95/0.64 inference(backward_demodulation,[status(thm)],[f146,f156])).
% 0.95/0.64 fof(f1047,plain,(
% 0.95/0.64 ron(vd1086,sK0_skl)),
% 0.95/0.64 inference(backward_demodulation,[status(thm)],[f146,f131])).
% 0.95/0.64 fof(f1048,plain,(
% 0.95/0.64 ~vd1086=vd1081),
% 0.95/0.64 inference(forward_demodulation,[status(thm)],[f146,f155])).
% 0.95/0.64 fof(f1054,plain,(
% 0.95/0.64 ~vd1086=sK2_skl),
% 0.95/0.64 inference(backward_demodulation,[status(thm)],[f168,f1048])).
% 0.95/0.64 fof(f1074,plain,(
% 0.95/0.64 ~ron(vd1086,sK0_skl)|sQ22_spl),
% 0.95/0.64 inference(forward_demodulation,[status(thm)],[f146,f974])).
% 0.95/0.64 fof(f1075,plain,(
% 0.95/0.64 $false|sQ22_spl),
% 0.95/0.64 inference(forward_subsumption_resolution,[status(thm)],[f1074,f1047])).
% 0.95/0.64 fof(f1076,plain,(
% 0.95/0.64 sQ22_spl),
% 0.95/0.64 inference(contradiction_clause,[status(thm)],[f1075])).
% 0.95/0.64 fof(f1085,plain,(
% 0.95/0.64 $false|sQ20_spl),
% 0.95/0.64 inference(forward_subsumption_resolution,[status(thm)],[f1042,f147])).
% 0.95/0.64 fof(f1086,plain,(
% 0.95/0.64 sQ20_spl),
% 0.95/0.64 inference(contradiction_clause,[status(thm)],[f1085])).
% 0.95/0.64 fof(f1087,plain,(
% 0.95/0.64 vd1086=vd1089|~sQ30_spl),
% 0.95/0.64 inference(forward_demodulation,[status(thm)],[f146,f1024])).
% 0.95/0.64 fof(f1093,plain,(
% 0.95/0.64 ~vd1086=sK3_skl),
% 0.95/0.64 inference(forward_demodulation,[status(thm)],[f171,f1045])).
% 0.95/0.64 fof(f1105,definition,(
% 0.95/0.64 sQ35_spl <=> (rpoint(vd1086))),
% 0.95/0.64 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.95/0.64 fof(f1107,plain,(
% 0.95/0.64 ~rpoint(vd1086)|sQ35_spl),
% 0.95/0.64 inference(component_clause,[status(thm)],[f1105])).
% 0.95/0.64 fof(f1109,plain,(
% 0.95/0.64 $false|sQ35_spl),
% 0.95/0.64 inference(forward_subsumption_resolution,[status(thm)],[f1107,f147])).
% 0.95/0.64 fof(f1110,plain,(
% 0.95/0.64 sQ35_spl),
% 0.95/0.64 inference(contradiction_clause,[status(thm)],[f1109])).
% 0.95/0.64 fof(f1171,plain,(
% 0.95/0.64 vf(vd1086,vd1086)=vf(vd1089,vd1080)|~sQ30_spl),
% 0.95/0.64 inference(forward_demodulation,[status(thm)],[f1087,f1043])).
% 0.95/0.64 fof(f1172,plain,(
% 0.95/0.64 vf(vd1086,vd1086)=vf(vd1086,vd1080)|~sQ30_spl),
% 0.95/0.64 inference(forward_demodulation,[status(thm)],[f1087,f1171])).
% 0.95/0.64 fof(f1173,plain,(
% 0.95/0.64 vf(vd1086,vd1086)=vf(vd1086,sK3_skl)|~sQ30_spl),
% 0.95/0.64 inference(forward_demodulation,[status(thm)],[f171,f1172])).
% 0.95/0.64 fof(f1191,definition,(
% 0.95/0.64 sQ46_spl <=> (rpoint(sK3_skl))),
% 0.95/0.64 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.95/0.64 fof(f1193,plain,(
% 0.95/0.64 ~rpoint(sK3_skl)|sQ46_spl),
% 0.95/0.64 inference(component_clause,[status(thm)],[f1191])).
% 0.95/0.64 fof(f1206,plain,(
% 0.95/0.64 $false|sQ46_spl),
% 0.95/0.64 inference(forward_subsumption_resolution,[status(thm)],[f1193,f172])).
% 0.95/0.64 fof(f1207,plain,(
% 0.95/0.64 sQ46_spl),
% 0.95/0.64 inference(contradiction_clause,[status(thm)],[f1206])).
% 0.95/0.64 fof(f1334,definition,(
% 0.95/0.64 sQ62_spl <=> (sK3_skl=vd1086)),
% 0.95/0.64 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.95/0.64 fof(f1335,plain,(
% 0.95/0.64 sK3_skl=vd1086|~sQ62_spl),
% 0.95/0.64 inference(component_clause,[status(thm)],[f1334])).
% 0.95/0.64 fof(f1423,definition,(
% 0.95/0.64 sQ72_spl <=> (rcircle(vskolem1095))),
% 0.95/0.64 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 0.95/0.64 fof(f1425,plain,(
% 0.95/0.64 ~rcircle(vskolem1095)|sQ72_spl),
% 0.95/0.64 inference(component_clause,[status(thm)],[f1423])).
% 0.95/0.64 fof(f1537,plain,(
% 0.95/0.64 $false|~sQ62_spl),
% 0.95/0.64 inference(forward_subsumption_resolution,[status(thm)],[f1335,f1093])).
% 0.95/0.64 fof(f1538,plain,(
% 0.95/0.64 ~sQ62_spl),
% 0.95/0.64 inference(contradiction_clause,[status(thm)],[f1537])).
% 0.95/0.64 fof(f1601,plain,(
% 0.95/0.64 rpoint(sK39_skl(sK0_skl))),
% 0.95/0.64 inference(resolution,[status(thm)],[f846,f133])).
% 0.95/0.64 fof(f1610,plain,(
% 0.95/0.64 rpoint(sK43_skl(sK39_skl(sK0_skl)))),
% 0.95/0.64 inference(resolution,[status(thm)],[f860,f1601])).
% 0.95/0.64 fof(f1771,definition,(
% 0.95/0.64 sQ99_spl <=> (sK43_skl(sK39_skl(sK0_skl))=sK39_skl(sK0_skl))),
% 0.95/0.64 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 0.95/0.64 fof(f1772,plain,(
% 0.95/0.64 sK43_skl(sK39_skl(sK0_skl))=sK39_skl(sK0_skl)|~sQ99_spl),
% 0.95/0.64 inference(component_clause,[status(thm)],[f1771])).
% 0.95/0.64 fof(f2619,plain,(
% 0.95/0.64 $false|sQ72_spl),
% 0.95/0.64 inference(forward_subsumption_resolution,[status(thm)],[f1425,f162])).
% 0.95/0.64 fof(f2620,plain,(
% 0.95/0.64 sQ72_spl),
% 0.95/0.64 inference(contradiction_clause,[status(thm)],[f2619])).
% 0.95/0.64 fof(f2653,definition,(
% 0.95/0.64 sQ229_spl <=> (vd1086=sK2_skl)),
% 0.95/0.64 introduced(definition,[new_symbols(definition,[sQ229_spl])],[split_symbol_definition])).
% 0.95/0.64 fof(f2654,plain,(
% 0.95/0.64 vd1086=sK2_skl|~sQ229_spl),
% 0.95/0.64 inference(component_clause,[status(thm)],[f2653])).
% 0.95/0.64 fof(f2674,plain,(
% 0.95/0.64 $false|~sQ229_spl),
% 0.95/0.64 inference(forward_subsumption_resolution,[status(thm)],[f2654,f1054])).
% 0.95/0.64 fof(f2675,plain,(
% 0.95/0.64 ~sQ229_spl),
% 0.95/0.64 inference(contradiction_clause,[status(thm)],[f2674])).
% 0.95/0.64 fof(f3457,plain,(
% 0.95/0.64 ![X0,X1]: (~rpoint(X0)|~rpoint(X1)|~vf(X1,X0)=vd684|X1=X0)),
% 0.95/0.64 inference(forward_demodulation,[status(thm)],[f284,f716])).
% 0.95/0.64 fof(f3463,plain,(
% 0.95/0.64 ![X0]: (~rpoint(X0)|vf(X0,X0)=vd684)),
% 0.95/0.64 inference(forward_demodulation,[status(thm)],[f284,f718])).
% 0.95/0.64 fof(f3480,plain,(
% 0.95/0.64 vf(vd1086,vd1086)=vd684),
% 0.95/0.64 inference(resolution,[status(thm)],[f3463,f147])).
% 0.95/0.64 fof(f3482,definition,(
% 0.95/0.64 ![X0]: (sQ309_spl <=> (~rreal(X0)))),
% 0.95/0.64 introduced(definition,[new_symbols(definition,[sQ309_spl])],[split_symbol_definition])).
% 0.95/0.64 fof(f3483,plain,(
% 0.95/0.64 ![X0]: (~rreal(X0)|~sQ309_spl)),
% 0.95/0.64 inference(component_clause,[status(thm)],[f3482])).
% 0.95/0.64 fof(f3521,plain,(
% 0.95/0.64 ~rpoint(sK39_skl(sK0_skl))|~sQ99_spl),
% 0.95/0.64 inference(resolution,[status(thm)],[f1772,f859])).
% 0.95/0.64 fof(f3523,plain,(
% 0.95/0.64 $false|~sQ99_spl),
% 0.95/0.64 inference(forward_subsumption_resolution,[status(thm)],[f3521,f1601])).
% 0.95/0.64 fof(f3524,plain,(
% 0.95/0.64 ~sQ99_spl),
% 0.95/0.64 inference(contradiction_clause,[status(thm)],[f3523])).
% 0.95/0.64 fof(f3551,plain,(
% 0.95/0.64 $false|~sQ309_spl),
% 0.95/0.64 inference(backward_subsumption_resolution,[status(thm)],[f285,f3483])).
% 0.95/0.64 fof(f3552,plain,(
% 0.95/0.64 ~sQ309_spl),
% 0.95/0.64 inference(contradiction_clause,[status(thm)],[f3551])).
% 0.95/0.64 fof(f3742,definition,(
% 0.95/0.64 sQ322_spl <=> (rpoint(vd14))),
% 0.95/0.64 introduced(definition,[new_symbols(definition,[sQ322_spl])],[split_symbol_definition])).
% 0.95/0.64 fof(f3744,plain,(
% 0.95/0.64 ~rpoint(vd14)|sQ322_spl),
% 0.95/0.64 inference(component_clause,[status(thm)],[f3742])).
% 0.95/0.64 fof(f3752,plain,(
% 0.95/0.64 $false|sQ322_spl),
% 0.95/0.64 inference(forward_subsumption_resolution,[status(thm)],[f3744,f544])).
% 0.95/0.64 fof(f3753,plain,(
% 0.95/0.64 sQ322_spl),
% 0.95/0.64 inference(contradiction_clause,[status(thm)],[f3752])).
% 0.95/0.64 fof(f3840,definition,(
% 0.95/0.64 sQ325_spl <=> (rpoint(sK43_skl(sK39_skl(sK0_skl))))),
% 0.95/0.64 introduced(definition,[new_symbols(definition,[sQ325_spl])],[split_symbol_definition])).
% 0.95/0.64 fof(f3842,plain,(
% 0.95/0.64 ~rpoint(sK43_skl(sK39_skl(sK0_skl)))|sQ325_spl),
% 0.95/0.64 inference(component_clause,[status(thm)],[f3840])).
% 0.95/0.64 fof(f3844,plain,(
% 0.95/0.64 $false|sQ325_spl),
% 0.95/0.64 inference(forward_subsumption_resolution,[status(thm)],[f3842,f1610])).
% 0.95/0.65 fof(f3845,plain,(
% 0.95/0.65 sQ325_spl),
% 0.95/0.65 inference(contradiction_clause,[status(thm)],[f3844])).
% 0.95/0.65 fof(f3887,plain,(
% 0.95/0.65 vd684=vf(vd1086,sK3_skl)|~sQ30_spl),
% 0.95/0.65 inference(backward_demodulation,[status(thm)],[f3480,f1173])).
% 0.95/0.65 fof(f3904,plain,(
% 0.95/0.65 ~rpoint(sK3_skl)|~rpoint(vd1086)|vd1086=sK3_skl|~sQ30_spl),
% 0.95/0.65 inference(resolution,[status(thm)],[f3887,f3457])).
% 0.95/0.65 fof(f3908,plain,(
% 0.95/0.65 ~sQ46_spl|~sQ35_spl|sQ62_spl|~sQ30_spl),
% 0.95/0.65 inference(split_clause,[status(thm)],[f3904,f1191,f1105,f1334,f1023])).
% 0.95/0.65 fof(f3915,plain,(
% 0.95/0.65 $false),
% 0.95/0.65 inference(sat_refutation,[status(thm)],[f957,f1005,f1007,f1009,f1018,f1026,f1032,f1076,f1086,f1110,f1207,f1538,f2620,f2675,f3524,f3552,f3753,f3845,f3908])).
% 0.95/0.65 % SZS output end CNFRefutation for theBenchmark.p
% 0.95/0.66 % Elapsed time: 0.295101 seconds
% 0.95/0.66 % CPU time: 1.966081 seconds
% 0.95/0.66 % Total memory used: 142.060 MB
% 0.95/0.66 % Net memory used: 139.319 MB
%------------------------------------------------------------------------------