%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO274+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 : n005.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.09s 0.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO274+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.09/0.38 % Computer : n005.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Sun Sep 20 14:59:48 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.41 % Drodi V4.1.1
% 0.09/0.45 % Refutation found
% 0.09/0.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.45 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.45 fof(f1,conjecture,(
% 0.09/0.45 (! [Vdthex] :( ( ron(vd1089,Vdthex)& ron(vd1080,Vdthex)& rline(Vdthex) )=> Vdthex = vd1092 ) )),
% 0.09/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.45 fof(f2,negated_conjecture,(
% 0.09/0.45 ~((! [Vdthex] :( ( ron(vd1089,Vdthex)& ron(vd1080,Vdthex)& rline(Vdthex) )=> Vdthex = vd1092 ) ))),
% 0.09/0.45 inference(negated_conjecture,[status(cth)],[f1])).
% 0.09/0.45 fof(f3,axiom,(
% 0.09/0.45 ( ron(vd1089,vd1092)& ron(vd1080,vd1092)& rline(vd1092) ) ),
% 0.09/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.45 fof(f4,axiom,(
% 0.09/0.45 vf(vd1089,vd1080) = vf(vd1085,vd1080) ),
% 0.09/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.45 fof(f5,axiom,(
% 0.09/0.45 vf(vd1089,vd1085) = vf(vd1089,vd1080) ),
% 0.09/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.45 fof(f6,axiom,(
% 0.09/0.45 rpoint(vd1089) ),
% 0.09/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.45 fof(f7,axiom,(
% 0.09/0.45 vd1085 = vd1086 ),
% 0.09/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.45 fof(f8,axiom,(
% 0.09/0.45 vd1085 != vd1080 ),
% 0.09/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.45 fof(f9,axiom,(
% 0.09/0.45 rpoint(vd1086) ),
% 0.09/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.45 fof(f10,axiom,(
% 0.09/0.45 (? [Vd1083] :( vd1080 = Vd1083& rpoint(Vd1083) ) )),
% 0.09/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.45 fof(f12,axiom,(
% 0.09/0.45 (! [Vd748,Vd749] :( ( (? [Vd752] :( Vd749 = Vd752& rpoint(Vd752) ))& (? [Vd751] :( Vd748 = Vd751& rpoint(Vd751) ) ))=> ( vf(Vd748,Vd749) = v0<=> Vd748 = Vd749 ) ) )),
% 0.09/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.45 fof(f35,axiom,(
% 0.09/0.45 v0 = vd684 ),
% 0.09/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.45 fof(f67,axiom,(
% 0.09/0.45 (! [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.09/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.09/0.45 fof(f119,plain,(
% 0.09/0.45 (?[Vdthex]: (((ron(vd1089,Vdthex)&ron(vd1080,Vdthex))&rline(Vdthex))&~Vdthex=vd1092))),
% 0.09/0.45 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.09/0.45 fof(f120,plain,(
% 0.09/0.45 (((ron(vd1089,sK0_skl)&ron(vd1080,sK0_skl))&rline(sK0_skl))&~sK0_skl=vd1092)),
% 0.09/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Vdthex,sK0_skl)],[f119])).
% 0.09/0.45 fof(f121,plain,(
% 0.09/0.45 ron(vd1089,sK0_skl)),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f120])).
% 0.09/0.45 fof(f122,plain,(
% 0.09/0.45 ron(vd1080,sK0_skl)),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f120])).
% 0.09/0.45 fof(f123,plain,(
% 0.09/0.45 rline(sK0_skl)),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f120])).
% 0.09/0.45 fof(f124,plain,(
% 0.09/0.45 ~sK0_skl=vd1092),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f120])).
% 0.09/0.45 fof(f125,plain,(
% 0.09/0.45 ron(vd1089,vd1092)),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f3])).
% 0.09/0.45 fof(f126,plain,(
% 0.09/0.45 ron(vd1080,vd1092)),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f3])).
% 0.09/0.45 fof(f127,plain,(
% 0.09/0.45 rline(vd1092)),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f3])).
% 0.09/0.45 fof(f128,plain,(
% 0.09/0.45 vf(vd1089,vd1080)=vf(vd1085,vd1080)),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f4])).
% 0.09/0.45 fof(f129,plain,(
% 0.09/0.45 vf(vd1089,vd1085)=vf(vd1089,vd1080)),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f5])).
% 0.09/0.45 fof(f130,plain,(
% 0.09/0.45 rpoint(vd1089)),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f6])).
% 0.09/0.45 fof(f131,plain,(
% 0.09/0.45 vd1085=vd1086),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f7])).
% 0.09/0.45 fof(f132,plain,(
% 0.09/0.45 ~vd1085=vd1080),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f8])).
% 0.09/0.45 fof(f133,plain,(
% 0.09/0.45 rpoint(vd1086)),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f9])).
% 0.09/0.45 fof(f134,plain,(
% 0.09/0.45 (vd1080=sK1_skl&rpoint(sK1_skl))),
% 0.09/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(Vd1083,sK1_skl)],[f10])).
% 0.09/0.45 fof(f135,plain,(
% 0.09/0.45 vd1080=sK1_skl),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f134])).
% 0.09/0.45 fof(f136,plain,(
% 0.09/0.45 rpoint(sK1_skl)),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f134])).
% 0.09/0.45 fof(f139,plain,(
% 0.09/0.45 ![Vd748,Vd749]: (((![Vd752]: (~Vd749=Vd752|~rpoint(Vd752)))|(![Vd751]: (~Vd748=Vd751|~rpoint(Vd751))))|(vf(Vd748,Vd749)=v0<=>Vd748=Vd749))),
% 0.09/0.45 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.09/0.45 fof(f140,plain,(
% 0.09/0.45 ![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.09/0.45 inference(NNF_transformation,[status(thm)],[f139])).
% 0.09/0.45 fof(f141,plain,(
% 0.09/0.45 ![X0,X1,X2,X3]: (~X0=X1|~rpoint(X1)|~X2=X3|~rpoint(X3)|~vf(X2,X0)=v0|X2=X0)),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f140])).
% 0.09/0.45 fof(f142,plain,(
% 0.09/0.45 ![X0,X1,X2,X3]: (~X0=X1|~rpoint(X1)|~X2=X3|~rpoint(X3)|vf(X2,X0)=v0|~X2=X0)),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f140])).
% 0.09/0.45 fof(f219,plain,(
% 0.09/0.45 v0=vd684),
% 0.09/0.45 inference(cnf_transformation,[status(thm)],[f35])).
% 0.09/0.45 fof(f321,plain,(
% 0.09/0.45 ![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.09/0.45 inference(pre_NNF_transformation,[status(thm)],[f67])).
% 0.09/0.45 fof(f322,plain,(
% 0.09/0.45 ![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.09/0.45 inference(miniscoping,[status(thm)],[f321])).
% 0.09/0.45 fof(f323,plain,(
% 0.09/0.45 ![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.09/0.45 inference(cnf_transformation,[status(thm)],[f322])).
% 0.09/0.45 fof(f663,plain,(
% 0.09/0.45 ![X0,X1]: (~rpoint(X0)|~rpoint(X1)|~vf(X1,X0)=v0|X1=X0)),
% 0.09/0.45 inference(destructive_equality_resolution,[status(thm)],[f141])).
% 0.09/0.45 fof(f664,plain,(
% 0.09/0.45 ![X1]: (~rpoint(X1)|~rpoint(X1)|vf(X1,X1)=v0)),
% 0.09/0.45 inference(destructive_equality_resolution,[status(thm)],[f142])).
% 0.09/0.45 fof(f665,plain,(
% 0.09/0.45 ![X0]: (~rpoint(X0)|vf(X0,X0)=v0)),
% 0.09/0.45 inference(duplicate_literals_removal,[status(thm)],[f664])).
% 0.09/0.45 fof(f729,plain,(
% 0.09/0.45 ![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.09/0.45 inference(destructive_equality_resolution,[status(thm)],[f323])).
% 0.09/0.45 fof(f883,plain,(
% 0.09/0.45 ![X0,X1]: (~ron(vd1089,X0)|~ron(X1,X0)|~ron(X1,vd1092)|~rline(X0)|~rline(vd1092)|X1=vd1089|~rpoint(vd1089)|~rpoint(X1)|vd1092=X0)),
% 0.09/0.45 inference(resolution,[status(thm)],[f729,f125])).
% 0.09/0.45 fof(f901,definition,(
% 0.09/0.45 sQ9_spl <=> (rline(vd1092))),
% 0.09/0.45 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.09/0.45 fof(f903,plain,(
% 0.09/0.45 ~rline(vd1092)|sQ9_spl),
% 0.09/0.45 inference(component_clause,[status(thm)],[f901])).
% 0.09/0.45 fof(f907,definition,(
% 0.09/0.45 sQ11_spl <=> (rpoint(vd1080))),
% 0.09/0.45 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.09/0.45 fof(f909,plain,(
% 0.09/0.45 ~rpoint(vd1080)|sQ11_spl),
% 0.09/0.45 inference(component_clause,[status(thm)],[f907])).
% 0.09/0.45 fof(f918,definition,(
% 0.09/0.45 sQ14_spl <=> (ron(vd1080,sK0_skl))),
% 0.09/0.45 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.09/0.45 fof(f920,plain,(
% 0.09/0.45 ~ron(vd1080,sK0_skl)|sQ14_spl),
% 0.09/0.45 inference(component_clause,[status(thm)],[f918])).
% 0.09/0.45 fof(f921,definition,(
% 0.09/0.45 sQ15_spl <=> (rline(sK0_skl))),
% 0.09/0.45 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.09/0.45 fof(f923,plain,(
% 0.09/0.45 ~rline(sK0_skl)|sQ15_spl),
% 0.09/0.45 inference(component_clause,[status(thm)],[f921])).
% 0.09/0.45 fof(f938,definition,(
% 0.09/0.45 sQ20_spl <=> (rpoint(vd1089))),
% 0.09/0.45 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.09/0.45 fof(f940,plain,(
% 0.09/0.45 ~rpoint(vd1089)|sQ20_spl),
% 0.09/0.45 inference(component_clause,[status(thm)],[f938])).
% 0.09/0.45 fof(f942,definition,(
% 0.09/0.45 ![X0,X1]: (sQ21_spl <=> (~ron(vd1089,X0)|~ron(X1,X0)|~ron(X1,vd1092)|~rline(X0)|X1=vd1089|~rpoint(X1)|vd1092=X0))),
% 0.09/0.45 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.09/0.45 fof(f943,plain,(
% 0.09/0.45 ![X0,X1]: (~ron(vd1089,X0)|~ron(X1,X0)|~ron(X1,vd1092)|~rline(X0)|X1=vd1089|~rpoint(X1)|vd1092=X0|~sQ21_spl)),
% 0.09/0.45 inference(component_clause,[status(thm)],[f942])).
% 0.09/0.45 fof(f945,plain,(
% 0.09/0.45 sQ21_spl|~sQ9_spl|~sQ20_spl),
% 0.09/0.45 inference(split_clause,[status(thm)],[f883,f942,f901,f938])).
% 0.09/0.45 fof(f978,plain,(
% 0.09/0.45 $false|sQ20_spl),
% 0.09/0.45 inference(forward_subsumption_resolution,[status(thm)],[f940,f130])).
% 0.09/0.45 fof(f979,plain,(
% 0.09/0.45 sQ20_spl),
% 0.09/0.45 inference(contradiction_clause,[status(thm)],[f978])).
% 0.09/0.45 fof(f980,plain,(
% 0.09/0.45 $false|sQ15_spl),
% 0.09/0.45 inference(forward_subsumption_resolution,[status(thm)],[f923,f123])).
% 0.09/0.45 fof(f981,plain,(
% 0.09/0.45 sQ15_spl),
% 0.09/0.45 inference(contradiction_clause,[status(thm)],[f980])).
% 0.09/0.45 fof(f982,plain,(
% 0.09/0.45 $false|sQ9_spl),
% 0.09/0.45 inference(forward_subsumption_resolution,[status(thm)],[f903,f127])).
% 0.09/0.45 fof(f983,plain,(
% 0.09/0.45 sQ9_spl),
% 0.09/0.45 inference(contradiction_clause,[status(thm)],[f982])).
% 0.09/0.45 fof(f986,definition,(
% 0.09/0.45 ![X0]: (sQ28_spl <=> (~ron(X0,vd1092)|~ron(X0,sK0_skl)|X0=vd1089|~rpoint(X0)))),
% 0.09/0.45 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.09/0.45 fof(f987,plain,(
% 0.09/0.45 ![X0]: (~ron(X0,vd1092)|~ron(X0,sK0_skl)|X0=vd1089|~rpoint(X0)|~sQ28_spl)),
% 0.09/0.45 inference(component_clause,[status(thm)],[f986])).
% 0.09/0.45 fof(f989,definition,(
% 0.09/0.45 sQ29_spl <=> (sK0_skl=vd1092)),
% 0.09/0.45 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.09/0.45 fof(f990,plain,(
% 0.09/0.45 sK0_skl=vd1092|~sQ29_spl),
% 0.09/0.45 inference(component_clause,[status(thm)],[f989])).
% 0.09/0.45 fof(f994,plain,(
% 0.09/0.45 ~ron(vd1080,sK0_skl)|vd1080=vd1089|~rpoint(vd1080)|~sQ28_spl),
% 0.09/0.45 inference(resolution,[status(thm)],[f987,f126])).
% 0.09/0.45 fof(f996,definition,(
% 0.09/0.45 sQ30_spl <=> (vd1080=vd1089)),
% 0.09/0.45 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.09/0.45 fof(f997,plain,(
% 0.09/0.45 vd1080=vd1089|~sQ30_spl),
% 0.09/0.45 inference(component_clause,[status(thm)],[f996])).
% 0.09/0.45 fof(f999,plain,(
% 0.09/0.45 ~sQ14_spl|sQ30_spl|~sQ11_spl|~sQ28_spl),
% 0.09/0.45 inference(split_clause,[status(thm)],[f994,f918,f996,f907,f986])).
% 0.09/0.45 fof(f1002,plain,(
% 0.09/0.45 ![X0]: (~ron(X0,sK0_skl)|~ron(X0,vd1092)|~rline(sK0_skl)|X0=vd1089|~rpoint(X0)|vd1092=sK0_skl|~sQ21_spl)),
% 0.09/0.45 inference(resolution,[status(thm)],[f943,f121])).
% 0.09/0.45 fof(f1004,plain,(
% 0.09/0.45 sQ28_spl|~sQ15_spl|sQ29_spl|~sQ21_spl),
% 0.09/0.45 inference(split_clause,[status(thm)],[f1002,f986,f921,f989,f942])).
% 0.09/0.45 fof(f1005,plain,(
% 0.09/0.45 $false|~sQ29_spl),
% 0.09/0.45 inference(forward_subsumption_resolution,[status(thm)],[f990,f124])).
% 0.09/0.45 fof(f1006,plain,(
% 0.09/0.45 ~sQ29_spl),
% 0.09/0.45 inference(contradiction_clause,[status(thm)],[f1005])).
% 0.09/0.45 fof(f1056,plain,(
% 0.09/0.45 ~vd1086=vd1080),
% 0.09/0.45 inference(forward_demodulation,[status(thm)],[f131,f132])).
% 0.09/0.45 fof(f1057,plain,(
% 0.09/0.45 ~vd1086=sK1_skl),
% 0.09/0.45 inference(backward_demodulation,[status(thm)],[f135,f1056])).
% 0.09/0.45 fof(f1058,plain,(
% 0.09/0.45 ~rpoint(sK1_skl)|sQ11_spl),
% 0.09/0.45 inference(backward_demodulation,[status(thm)],[f135,f909])).
% 0.09/0.45 fof(f1060,plain,(
% 0.09/0.45 ron(sK1_skl,sK0_skl)),
% 0.09/0.45 inference(backward_demodulation,[status(thm)],[f135,f122])).
% 0.09/0.45 fof(f1065,plain,(
% 0.09/0.45 $false|sQ11_spl),
% 0.09/0.45 inference(forward_subsumption_resolution,[status(thm)],[f1058,f136])).
% 0.09/0.45 fof(f1066,plain,(
% 0.09/0.45 sQ11_spl),
% 0.09/0.45 inference(contradiction_clause,[status(thm)],[f1065])).
% 0.09/0.45 fof(f1067,plain,(
% 0.09/0.45 ~ron(sK1_skl,sK0_skl)|sQ14_spl),
% 0.09/0.45 inference(forward_demodulation,[status(thm)],[f135,f920])).
% 0.09/0.45 fof(f1073,plain,(
% 0.09/0.45 vf(vd1089,sK1_skl)=vf(vd1085,vd1080)),
% 0.09/0.45 inference(forward_demodulation,[status(thm)],[f135,f128])).
% 0.09/0.45 fof(f1074,plain,(
% 0.09/0.45 vf(vd1089,sK1_skl)=vf(vd1086,vd1080)),
% 0.09/0.45 inference(forward_demodulation,[status(thm)],[f131,f1073])).
% 0.09/0.45 fof(f1075,plain,(
% 0.09/0.45 vf(vd1089,sK1_skl)=vf(vd1086,sK1_skl)),
% 0.09/0.45 inference(forward_demodulation,[status(thm)],[f135,f1074])).
% 0.09/0.45 fof(f1076,plain,(
% 0.09/0.45 vf(vd1089,vd1086)=vf(vd1089,vd1080)),
% 0.09/0.45 inference(forward_demodulation,[status(thm)],[f131,f129])).
% 0.09/0.45 fof(f1077,plain,(
% 0.09/0.45 vf(vd1089,vd1086)=vf(vd1089,sK1_skl)),
% 0.09/0.45 inference(forward_demodulation,[status(thm)],[f135,f1076])).
% 0.09/0.45 fof(f1078,plain,(
% 0.09/0.45 vf(vd1089,vd1086)=vf(vd1086,sK1_skl)),
% 0.09/0.45 inference(forward_demodulation,[status(thm)],[f1075,f1077])).
% 0.09/0.45 fof(f1096,definition,(
% 0.09/0.45 sQ33_spl <=> (rpoint(sK1_skl))),
% 0.09/0.45 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.09/0.45 fof(f1098,plain,(
% 0.09/0.45 ~rpoint(sK1_skl)|sQ33_spl),
% 0.09/0.45 inference(component_clause,[status(thm)],[f1096])).
% 0.09/0.45 fof(f1108,plain,(
% 0.09/0.45 $false|sQ33_spl),
% 0.09/0.45 inference(forward_subsumption_resolution,[status(thm)],[f1098,f136])).
% 0.09/0.45 fof(f1109,plain,(
% 0.09/0.45 sQ33_spl),
% 0.09/0.45 inference(contradiction_clause,[status(thm)],[f1108])).
% 0.09/0.45 fof(f1110,plain,(
% 0.09/0.45 $false|sQ14_spl),
% 0.09/0.45 inference(forward_subsumption_resolution,[status(thm)],[f1067,f1060])).
% 0.09/0.45 fof(f1111,plain,(
% 0.09/0.45 sQ14_spl),
% 0.09/0.45 inference(contradiction_clause,[status(thm)],[f1110])).
% 0.09/0.45 fof(f1112,plain,(
% 0.09/0.45 sK1_skl=vd1089|~sQ30_spl),
% 0.09/0.45 inference(forward_demodulation,[status(thm)],[f135,f997])).
% 0.09/0.45 fof(f1114,plain,(
% 0.09/0.45 vf(sK1_skl,vd1086)=vf(vd1086,sK1_skl)|~sQ30_spl),
% 0.09/0.45 inference(backward_demodulation,[status(thm)],[f1112,f1078])).
% 0.09/0.45 fof(f1115,plain,(
% 0.09/0.45 vf(sK1_skl,sK1_skl)=vf(vd1086,sK1_skl)|~sQ30_spl),
% 0.09/0.45 inference(backward_demodulation,[status(thm)],[f1112,f1075])).
% 0.09/0.45 fof(f1138,plain,(
% 0.09/0.45 vf(sK1_skl,vd1086)=vf(sK1_skl,sK1_skl)|~sQ30_spl),
% 0.09/0.45 inference(backward_demodulation,[status(thm)],[f1115,f1114])).
% 0.09/0.45 fof(f1181,plain,(
% 0.09/0.45 ![X0,X1]: (~rpoint(X0)|~rpoint(X1)|~vf(X1,X0)=vd684|X1=X0)),
% 0.09/0.45 inference(forward_demodulation,[status(thm)],[f219,f663])).
% 0.09/0.45 fof(f1184,plain,(
% 0.09/0.45 ~rpoint(vd1086)|~rpoint(sK1_skl)|~vf(sK1_skl,sK1_skl)=vd684|sK1_skl=vd1086|~sQ30_spl),
% 0.09/0.45 inference(paramodulation,[status(thm)],[f1138,f1181])).
% 0.09/0.45 fof(f1206,definition,(
% 0.09/0.45 sQ46_spl <=> (rpoint(vd1086))),
% 0.09/0.45 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.09/0.45 fof(f1208,plain,(
% 0.09/0.45 ~rpoint(vd1086)|sQ46_spl),
% 0.09/0.45 inference(component_clause,[status(thm)],[f1206])).
% 0.09/0.45 fof(f1209,definition,(
% 0.09/0.45 sQ47_spl <=> (vf(sK1_skl,sK1_skl)=vd684)),
% 0.09/0.45 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.09/0.45 fof(f1211,plain,(
% 0.09/0.45 ~vf(sK1_skl,sK1_skl)=vd684|sQ47_spl),
% 0.09/0.45 inference(component_clause,[status(thm)],[f1209])).
% 0.09/0.45 fof(f1212,definition,(
% 0.09/0.45 sQ48_spl <=> (sK1_skl=vd1086)),
% 0.09/0.45 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.09/0.45 fof(f1213,plain,(
% 0.09/0.45 sK1_skl=vd1086|~sQ48_spl),
% 0.09/0.45 inference(component_clause,[status(thm)],[f1212])).
% 0.09/0.45 fof(f1215,plain,(
% 0.09/0.45 ~sQ46_spl|~sQ33_spl|~sQ47_spl|sQ48_spl|~sQ30_spl),
% 0.09/0.45 inference(split_clause,[status(thm)],[f1184,f1206,f1096,f1209,f1212,f996])).
% 0.09/0.45 fof(f1226,plain,(
% 0.09/0.45 $false|~sQ48_spl),
% 0.09/0.45 inference(forward_subsumption_resolution,[status(thm)],[f1213,f1057])).
% 0.09/0.45 fof(f1227,plain,(
% 0.09/0.45 ~sQ48_spl),
% 0.09/0.45 inference(contradiction_clause,[status(thm)],[f1226])).
% 0.09/0.45 fof(f1228,plain,(
% 0.09/0.45 $false|sQ46_spl),
% 0.09/0.45 inference(forward_subsumption_resolution,[status(thm)],[f1208,f133])).
% 0.09/0.45 fof(f1229,plain,(
% 0.09/0.45 sQ46_spl),
% 0.09/0.45 inference(contradiction_clause,[status(thm)],[f1228])).
% 0.09/0.45 fof(f1235,plain,(
% 0.09/0.45 ![X0]: (~rpoint(X0)|vf(X0,X0)=vd684)),
% 0.09/0.45 inference(forward_demodulation,[status(thm)],[f219,f665])).
% 0.09/0.45 fof(f1240,plain,(
% 0.09/0.45 vf(sK1_skl,sK1_skl)=vd684),
% 0.09/0.45 inference(resolution,[status(thm)],[f1235,f136])).
% 0.09/0.45 fof(f1864,plain,(
% 0.09/0.45 $false|sQ47_spl),
% 0.09/0.45 inference(forward_subsumption_resolution,[status(thm)],[f1240,f1211])).
% 0.09/0.45 fof(f1865,plain,(
% 0.09/0.45 sQ47_spl),
% 0.09/0.45 inference(contradiction_clause,[status(thm)],[f1864])).
% 0.09/0.45 fof(f1866,plain,(
% 0.09/0.45 $false),
% 0.09/0.45 inference(sat_refutation,[status(thm)],[f945,f979,f981,f983,f999,f1004,f1006,f1066,f1109,f1111,f1215,f1227,f1229,f1865])).
% 0.09/0.45 % SZS output end CNFRefutation for theBenchmark.p
% 0.19/0.48 % Elapsed time: 0.095580 seconds
% 0.19/0.48 % CPU time: 0.313813 seconds
% 0.19/0.48 % Total memory used: 119.479 MB
% 0.19/0.48 % Net memory used: 118.942 MB
%------------------------------------------------------------------------------