%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO270+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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 9.41s 1.62s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO270+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n007.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 14:58:05 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.39 % Drodi V4.1.1
% 9.41/1.62 % Refutation found
% 9.41/1.62 % SZS status Theorem for theBenchmark: Theorem is valid
% 9.41/1.62 % SZS output start CNFRefutation for theBenchmark
% 9.41/1.62 fof(f1,conjecture,(
% 9.41/1.62 (? [Vd1052] :( vf(vd1049,Vd1052) = vf(Vd1052,vd1047)& vf(vd1047,vd1049) = vf(vd1049,Vd1052)& rpoint(Vd1052) ) )),
% 9.41/1.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.41/1.62 fof(f2,negated_conjecture,(
% 9.41/1.62 ~((? [Vd1052] :( vf(vd1049,Vd1052) = vf(Vd1052,vd1047)& vf(vd1047,vd1049) = vf(vd1049,Vd1052)& rpoint(Vd1052) ) ))),
% 9.41/1.62 inference(negated_conjecture,[status(cth)],[f1])).
% 9.41/1.62 fof(f3,axiom,(
% 9.41/1.62 ( vd1049 = vd1050& vd1047 != vd1049& rpoint(vd1050)& vd1047 = vd1048& rpoint(vd1048) ) ),
% 9.41/1.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.41/1.62 fof(f5,axiom,(
% 9.41/1.62 (! [Vd1055,Vd1056,Vd1057,Vd1058] :( ( Vd1057 = Vd1058& Vd1055 != Vd1057& rpoint(Vd1058)& Vd1055 = Vd1056& rpoint(Vd1056) )=> (! [Vd1060] :( Vd1060 = vskolem1061(Vd1055,Vd1056,Vd1057,Vd1058)=> (! [Vd1062] :( Vd1062 = vskolem1063(Vd1060,Vd1055,Vd1056,Vd1057,Vd1058)=> vf(Vd1055,Vd1057) = vf(Vd1057,vskolem1064(Vd1062,Vd1060,Vd1055,Vd1056,Vd1057,Vd1058)) ) )) )) )),
% 9.41/1.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.41/1.62 fof(f7,axiom,(
% 9.41/1.62 (! [Vd1055,Vd1056,Vd1057,Vd1058] :( ( Vd1057 = Vd1058& Vd1055 != Vd1057& rpoint(Vd1058)& Vd1055 = Vd1056& rpoint(Vd1056) )=> (! [Vd1060] :( Vd1060 = vskolem1061(Vd1055,Vd1056,Vd1057,Vd1058)=> (! [Vd1062] :( Vd1062 = vskolem1063(Vd1060,Vd1055,Vd1056,Vd1057,Vd1058)=> vf(Vd1055,Vd1057) = vf(Vd1055,vskolem1064(Vd1062,Vd1060,Vd1055,Vd1056,Vd1057,Vd1058)) ) )) )) )),
% 9.41/1.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.41/1.62 fof(f10,axiom,(
% 9.41/1.62 (! [Vd1055,Vd1056,Vd1057,Vd1058] :( ( Vd1057 = Vd1058& Vd1055 != Vd1057& rpoint(Vd1058)& Vd1055 = Vd1056& rpoint(Vd1056) )=> (! [Vd1060] :( Vd1060 = vskolem1061(Vd1055,Vd1056,Vd1057,Vd1058)=> (! [Vd1062] :( Vd1062 = vskolem1063(Vd1060,Vd1055,Vd1056,Vd1057,Vd1058)=> rpoint(vskolem1064(Vd1062,Vd1060,Vd1055,Vd1056,Vd1057,Vd1058)) ) )) )) )),
% 9.41/1.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.41/1.62 fof(f17,axiom,(
% 9.41/1.62 (! [Vd761,Vd762] :( ( (? [Vd765] :( Vd762 = Vd765& rpoint(Vd765) ))& (? [Vd764] :( Vd761 = Vd764& rpoint(Vd764) ) ))=> vf(Vd761,Vd762) = vf(Vd762,Vd761) ) )),
% 9.41/1.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.41/1.62 fof(f53,axiom,(
% 9.41/1.62 rreal(vd684) ),
% 9.41/1.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.41/1.62 fof(f115,axiom,(
% 9.41/1.62 rpoint(vd14) ),
% 9.41/1.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.41/1.62 fof(f118,plain,(
% 9.41/1.62 (![Vd1052]: ((~vf(vd1049,Vd1052)=vf(Vd1052,vd1047)|~vf(vd1047,vd1049)=vf(vd1049,Vd1052))|~rpoint(Vd1052)))),
% 9.41/1.62 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 9.41/1.62 fof(f119,plain,(
% 9.41/1.62 ![X0]: (~vf(vd1049,X0)=vf(X0,vd1047)|~vf(vd1047,vd1049)=vf(vd1049,X0)|~rpoint(X0))),
% 9.41/1.62 inference(cnf_transformation,[status(thm)],[f118])).
% 9.41/1.62 fof(f120,plain,(
% 9.41/1.62 vd1049=vd1050),
% 9.41/1.62 inference(cnf_transformation,[status(thm)],[f3])).
% 9.41/1.62 fof(f121,plain,(
% 9.41/1.62 ~vd1047=vd1049),
% 9.41/1.62 inference(cnf_transformation,[status(thm)],[f3])).
% 9.41/1.62 fof(f122,plain,(
% 9.41/1.62 rpoint(vd1050)),
% 9.41/1.62 inference(cnf_transformation,[status(thm)],[f3])).
% 9.41/1.62 fof(f123,plain,(
% 9.41/1.62 vd1047=vd1048),
% 9.41/1.62 inference(cnf_transformation,[status(thm)],[f3])).
% 9.41/1.62 fof(f124,plain,(
% 9.41/1.62 rpoint(vd1048)),
% 9.41/1.62 inference(cnf_transformation,[status(thm)],[f3])).
% 9.41/1.62 fof(f127,plain,(
% 9.41/1.62 ![Vd1055,Vd1056,Vd1057,Vd1058]: (((((~Vd1057=Vd1058|Vd1055=Vd1057)|~rpoint(Vd1058))|~Vd1055=Vd1056)|~rpoint(Vd1056))|(![Vd1060]: (~Vd1060=vskolem1061(Vd1055,Vd1056,Vd1057,Vd1058)|(![Vd1062]: (~Vd1062=vskolem1063(Vd1060,Vd1055,Vd1056,Vd1057,Vd1058)|vf(Vd1055,Vd1057)=vf(Vd1057,vskolem1064(Vd1062,Vd1060,Vd1055,Vd1056,Vd1057,Vd1058)))))))),
% 9.41/1.62 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 9.41/1.62 fof(f128,plain,(
% 9.41/1.62 ![X0,X1,X2,X3,X4,X5]: (~X0=X1|X2=X0|~rpoint(X1)|~X2=X3|~rpoint(X3)|~X4=vskolem1061(X2,X3,X0,X1)|~X5=vskolem1063(X4,X2,X3,X0,X1)|vf(X2,X0)=vf(X0,vskolem1064(X5,X4,X2,X3,X0,X1)))),
% 9.41/1.62 inference(cnf_transformation,[status(thm)],[f127])).
% 9.41/1.62 fof(f131,plain,(
% 9.41/1.62 ![Vd1055,Vd1056,Vd1057,Vd1058]: (((((~Vd1057=Vd1058|Vd1055=Vd1057)|~rpoint(Vd1058))|~Vd1055=Vd1056)|~rpoint(Vd1056))|(![Vd1060]: (~Vd1060=vskolem1061(Vd1055,Vd1056,Vd1057,Vd1058)|(![Vd1062]: (~Vd1062=vskolem1063(Vd1060,Vd1055,Vd1056,Vd1057,Vd1058)|vf(Vd1055,Vd1057)=vf(Vd1055,vskolem1064(Vd1062,Vd1060,Vd1055,Vd1056,Vd1057,Vd1058)))))))),
% 9.41/1.62 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 9.41/1.62 fof(f132,plain,(
% 9.41/1.62 ![X0,X1,X2,X3,X4,X5]: (~X0=X1|X2=X0|~rpoint(X1)|~X2=X3|~rpoint(X3)|~X4=vskolem1061(X2,X3,X0,X1)|~X5=vskolem1063(X4,X2,X3,X0,X1)|vf(X2,X0)=vf(X2,vskolem1064(X5,X4,X2,X3,X0,X1)))),
% 9.41/1.62 inference(cnf_transformation,[status(thm)],[f131])).
% 9.41/1.62 fof(f137,plain,(
% 9.41/1.62 ![Vd1055,Vd1056,Vd1057,Vd1058]: (((((~Vd1057=Vd1058|Vd1055=Vd1057)|~rpoint(Vd1058))|~Vd1055=Vd1056)|~rpoint(Vd1056))|(![Vd1060]: (~Vd1060=vskolem1061(Vd1055,Vd1056,Vd1057,Vd1058)|(![Vd1062]: (~Vd1062=vskolem1063(Vd1060,Vd1055,Vd1056,Vd1057,Vd1058)|rpoint(vskolem1064(Vd1062,Vd1060,Vd1055,Vd1056,Vd1057,Vd1058)))))))),
% 9.41/1.62 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 9.41/1.62 fof(f138,plain,(
% 9.41/1.62 ![X0,X1,X2,X3,X4,X5]: (~X0=X1|X2=X0|~rpoint(X1)|~X2=X3|~rpoint(X3)|~X4=vskolem1061(X2,X3,X0,X1)|~X5=vskolem1063(X4,X2,X3,X0,X1)|rpoint(vskolem1064(X5,X4,X2,X3,X0,X1)))),
% 9.41/1.62 inference(cnf_transformation,[status(thm)],[f137])).
% 9.41/1.62 fof(f158,plain,(
% 9.41/1.62 ![Vd761,Vd762]: (((![Vd765]: (~Vd762=Vd765|~rpoint(Vd765)))|(![Vd764]: (~Vd761=Vd764|~rpoint(Vd764))))|vf(Vd761,Vd762)=vf(Vd762,Vd761))),
% 9.41/1.62 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 9.41/1.62 fof(f159,plain,(
% 9.41/1.62 ![X0,X1,X2,X3]: (~X0=X1|~rpoint(X1)|~X2=X3|~rpoint(X3)|vf(X2,X0)=vf(X0,X2))),
% 9.41/1.62 inference(cnf_transformation,[status(thm)],[f158])).
% 9.41/1.62 fof(f288,plain,(
% 9.41/1.62 rreal(vd684)),
% 9.41/1.62 inference(cnf_transformation,[status(thm)],[f53])).
% 9.41/1.62 fof(f585,plain,(
% 9.41/1.62 rpoint(vd14)),
% 9.41/1.62 inference(cnf_transformation,[status(thm)],[f115])).
% 9.41/1.62 fof(f668,plain,(
% 9.41/1.62 ![X0,X1]: (X0=X1|~rpoint(X1)|~rpoint(X0)|vf(X0,X1)=vf(X1,vskolem1064(vskolem1063(vskolem1061(X0,X0,X1,X1),X0,X0,X1,X1),vskolem1061(X0,X0,X1,X1),X0,X0,X1,X1)))),
% 9.41/1.62 inference(destructive_equality_resolution,[status(thm)],[f128])).
% 9.41/1.62 fof(f670,plain,(
% 9.41/1.62 ![X0,X1]: (X0=X1|~rpoint(X1)|~rpoint(X0)|vf(X0,X1)=vf(X0,vskolem1064(vskolem1063(vskolem1061(X0,X0,X1,X1),X0,X0,X1,X1),vskolem1061(X0,X0,X1,X1),X0,X0,X1,X1)))),
% 9.41/1.62 inference(destructive_equality_resolution,[status(thm)],[f132])).
% 9.41/1.62 fof(f673,plain,(
% 9.41/1.62 ![X0,X1]: (X0=X1|~rpoint(X1)|~rpoint(X0)|rpoint(vskolem1064(vskolem1063(vskolem1061(X0,X0,X1,X1),X0,X0,X1,X1),vskolem1061(X0,X0,X1,X1),X0,X0,X1,X1)))),
% 9.41/1.62 inference(destructive_equality_resolution,[status(thm)],[f138])).
% 9.41/1.62 fof(f685,plain,(
% 9.41/1.62 ![X0,X1]: (~rpoint(X0)|~rpoint(X1)|vf(X1,X0)=vf(X0,X1))),
% 9.41/1.62 inference(destructive_equality_resolution,[status(thm)],[f159])).
% 9.41/1.62 fof(f896,plain,(
% 9.41/1.62 ~vd1047=vd1050),
% 9.41/1.62 inference(backward_demodulation,[status(thm)],[f120,f121])).
% 9.41/1.62 fof(f897,plain,(
% 9.41/1.62 ![X0]: (~vf(vd1049,X0)=vf(X0,vd1047)|~vf(vd1047,vd1049)=vf(vd1050,X0)|~rpoint(X0))),
% 9.41/1.62 inference(backward_demodulation,[status(thm)],[f120,f119])).
% 9.41/1.62 fof(f898,plain,(
% 9.41/1.62 ![X0]: (~vf(vd1050,X0)=vf(X0,vd1047)|~vf(vd1047,vd1049)=vf(vd1050,X0)|~rpoint(X0))),
% 9.41/1.62 inference(forward_demodulation,[status(thm)],[f120,f897])).
% 9.41/1.62 fof(f899,plain,(
% 9.41/1.62 ![X0]: (~vf(vd1050,X0)=vf(X0,vd1047)|~vf(vd1047,vd1050)=vf(vd1050,X0)|~rpoint(X0))),
% 9.41/1.62 inference(forward_demodulation,[status(thm)],[f120,f898])).
% 9.41/1.62 fof(f903,plain,(
% 9.41/1.62 ![X0]: (~rpoint(X0)|vf(vd1050,X0)=vf(X0,vd1050))),
% 9.41/1.62 inference(resolution,[status(thm)],[f122,f685])).
% 9.41/1.62 fof(f904,plain,(
% 9.41/1.62 ~vd1048=vd1050),
% 9.41/1.62 inference(backward_demodulation,[status(thm)],[f123,f896])).
% 9.41/1.62 fof(f908,plain,(
% 9.41/1.62 ![X0]: (~rpoint(X0)|vf(vd1048,X0)=vf(X0,vd1048))),
% 9.41/1.62 inference(resolution,[status(thm)],[f124,f685])).
% 9.41/1.62 fof(f909,plain,(
% 9.41/1.62 ![X0]: (~vf(vd1050,X0)=vf(X0,vd1048)|~vf(vd1047,vd1050)=vf(vd1050,X0)|~rpoint(X0))),
% 9.41/1.62 inference(forward_demodulation,[status(thm)],[f123,f899])).
% 9.41/1.62 fof(f910,plain,(
% 9.41/1.62 ![X0]: (~vf(vd1050,X0)=vf(X0,vd1048)|~vf(vd1048,vd1050)=vf(vd1050,X0)|~rpoint(X0))),
% 9.41/1.62 inference(forward_demodulation,[status(thm)],[f123,f909])).
% 9.41/1.62 fof(f911,plain,(
% 9.41/1.62 vf(vd1050,vd1048)=vf(vd1048,vd1050)),
% 9.41/1.62 inference(resolution,[status(thm)],[f903,f124])).
% 9.41/1.62 fof(f931,plain,(
% 9.41/1.62 ![X0]: (X0=vd1048|~rpoint(X0)|vf(X0,vd1048)=vf(vd1048,vskolem1064(vskolem1063(vskolem1061(X0,X0,vd1048,vd1048),X0,X0,vd1048,vd1048),vskolem1061(X0,X0,vd1048,vd1048),X0,X0,vd1048,vd1048)))),
% 9.41/1.62 inference(resolution,[status(thm)],[f668,f124])).
% 9.41/1.62 fof(f935,plain,(
% 9.41/1.62 ![X0]: (X0=vd1048|~rpoint(X0)|vf(X0,vd1048)=vf(X0,vskolem1064(vskolem1063(vskolem1061(X0,X0,vd1048,vd1048),X0,X0,vd1048,vd1048),vskolem1061(X0,X0,vd1048,vd1048),X0,X0,vd1048,vd1048)))),
% 9.41/1.62 inference(resolution,[status(thm)],[f670,f124])).
% 9.41/1.62 fof(f947,plain,(
% 9.41/1.62 ![X0]: (X0=vd1048|~rpoint(X0)|rpoint(vskolem1064(vskolem1063(vskolem1061(X0,X0,vd1048,vd1048),X0,X0,vd1048,vd1048),vskolem1061(X0,X0,vd1048,vd1048),X0,X0,vd1048,vd1048)))),
% 9.41/1.62 inference(resolution,[status(thm)],[f673,f124])).
% 9.41/1.62 fof(f977,definition,(
% 9.41/1.62 sQ12_spl <=> (vd1050=vd1048)),
% 9.41/1.62 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 9.41/1.62 fof(f978,plain,(
% 9.41/1.62 vd1050=vd1048|~sQ12_spl),
% 9.41/1.62 inference(component_clause,[status(thm)],[f977])).
% 9.41/1.62 fof(f1093,plain,(
% 9.41/1.62 $false|~sQ12_spl),
% 9.41/1.62 inference(forward_subsumption_resolution,[status(thm)],[f978,f904])).
% 9.41/1.62 fof(f1094,plain,(
% 9.41/1.62 ~sQ12_spl),
% 9.41/1.62 inference(contradiction_clause,[status(thm)],[f1093])).
% 9.41/1.62 fof(f1319,plain,(
% 9.41/1.62 vf(vd1050,vd14)=vf(vd14,vd1050)),
% 9.41/1.62 inference(resolution,[status(thm)],[f585,f903])).
% 9.41/1.62 fof(f1335,definition,(
% 9.41/1.62 sQ23_spl <=> (rpoint(vd14))),
% 9.41/1.62 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 9.41/1.62 fof(f1337,plain,(
% 9.41/1.62 ~rpoint(vd14)|sQ23_spl),
% 9.41/1.62 inference(component_clause,[status(thm)],[f1335])).
% 9.41/1.62 fof(f1353,plain,(
% 9.41/1.62 $false|sQ23_spl),
% 9.41/1.62 inference(forward_subsumption_resolution,[status(thm)],[f1337,f585])).
% 9.41/1.62 fof(f1354,plain,(
% 9.41/1.62 sQ23_spl),
% 9.41/1.62 inference(contradiction_clause,[status(thm)],[f1353])).
% 9.41/1.62 fof(f1469,definition,(
% 9.41/1.62 sQ39_spl <=> (vf(vd14,vd1050)=vf(vd1050,vd14))),
% 9.41/1.62 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 9.41/1.62 fof(f1471,plain,(
% 9.41/1.62 ~vf(vd14,vd1050)=vf(vd1050,vd14)|sQ39_spl),
% 9.41/1.62 inference(component_clause,[status(thm)],[f1469])).
% 9.41/1.62 fof(f1481,plain,(
% 9.41/1.62 ~vf(vd14,vd1050)=vf(vd14,vd1050)|sQ39_spl),
% 9.41/1.62 inference(forward_demodulation,[status(thm)],[f1319,f1471])).
% 9.41/1.62 fof(f1482,plain,(
% 9.41/1.62 $false|sQ39_spl),
% 9.41/1.62 inference(trivial_equality_resolution,[status(thm)],[f1481])).
% 9.41/1.62 fof(f1483,plain,(
% 9.41/1.62 sQ39_spl),
% 9.41/1.62 inference(contradiction_clause,[status(thm)],[f1482])).
% 9.41/1.62 fof(f1550,plain,(
% 9.41/1.62 vd1050=vd1048|vf(vd1050,vd1048)=vf(vd1048,vskolem1064(vskolem1063(vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048))),
% 9.41/1.62 inference(resolution,[status(thm)],[f931,f122])).
% 9.41/1.62 fof(f1555,definition,(
% 9.41/1.62 sQ50_spl <=> (vf(vd1050,vd1048)=vf(vd1048,vskolem1064(vskolem1063(vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048)))),
% 9.41/1.62 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 9.41/1.62 fof(f1556,plain,(
% 9.41/1.62 vf(vd1050,vd1048)=vf(vd1048,vskolem1064(vskolem1063(vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048))|~sQ50_spl),
% 9.41/1.62 inference(component_clause,[status(thm)],[f1555])).
% 9.41/1.62 fof(f1558,plain,(
% 9.41/1.62 sQ12_spl|sQ50_spl),
% 9.41/1.62 inference(split_clause,[status(thm)],[f1550,f977,f1555])).
% 9.41/1.62 fof(f1559,plain,(
% 9.41/1.62 vf(vd1048,vd1050)=vf(vd1048,vskolem1064(vskolem1063(vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048))|~sQ50_spl),
% 9.41/1.62 inference(forward_demodulation,[status(thm)],[f911,f1556])).
% 9.41/1.62 fof(f1582,definition,(
% 9.41/1.62 sQ55_spl <=> (rpoint(vskolem1064(vskolem1063(vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048)))),
% 9.41/1.62 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 9.41/1.62 fof(f1583,plain,(
% 9.41/1.62 rpoint(vskolem1064(vskolem1063(vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048))|~sQ55_spl),
% 9.41/1.62 inference(component_clause,[status(thm)],[f1582])).
% 9.41/1.62 fof(f1599,plain,(
% 9.41/1.62 vd1050=vd1048|vf(vd1050,vd1048)=vf(vd1050,vskolem1064(vskolem1063(vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048))),
% 9.41/1.62 inference(resolution,[status(thm)],[f935,f122])).
% 9.41/1.62 fof(f1604,definition,(
% 9.41/1.62 sQ59_spl <=> (vf(vd1050,vd1048)=vf(vd1050,vskolem1064(vskolem1063(vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048)))),
% 9.41/1.62 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 9.41/1.62 fof(f1605,plain,(
% 9.41/1.62 vf(vd1050,vd1048)=vf(vd1050,vskolem1064(vskolem1063(vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048))|~sQ59_spl),
% 9.41/1.62 inference(component_clause,[status(thm)],[f1604])).
% 9.41/1.62 fof(f1607,plain,(
% 9.41/1.62 sQ12_spl|sQ59_spl),
% 9.41/1.62 inference(split_clause,[status(thm)],[f1599,f977,f1604])).
% 9.41/1.62 fof(f1608,plain,(
% 9.41/1.62 vf(vd1048,vd1050)=vf(vd1050,vskolem1064(vskolem1063(vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048))|~sQ59_spl),
% 9.41/1.62 inference(forward_demodulation,[status(thm)],[f911,f1605])).
% 9.41/1.62 fof(f1671,definition,(
% 9.41/1.62 sQ65_spl <=> (rreal(vd684))),
% 9.41/1.62 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 9.41/1.62 fof(f1673,plain,(
% 9.41/1.62 ~rreal(vd684)|sQ65_spl),
% 9.41/1.62 inference(component_clause,[status(thm)],[f1671])).
% 9.41/1.62 fof(f1679,plain,(
% 9.41/1.62 $false|sQ65_spl),
% 9.41/1.62 inference(forward_subsumption_resolution,[status(thm)],[f1673,f288])).
% 9.41/1.62 fof(f1680,plain,(
% 9.41/1.62 sQ65_spl),
% 9.41/1.62 inference(contradiction_clause,[status(thm)],[f1679])).
% 9.41/1.62 fof(f1687,plain,(
% 9.41/1.62 vd1050=vd1048|rpoint(vskolem1064(vskolem1063(vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048))),
% 9.41/1.62 inference(resolution,[status(thm)],[f947,f122])).
% 9.41/1.62 fof(f1689,plain,(
% 9.41/1.62 sQ12_spl|sQ55_spl),
% 9.41/1.62 inference(split_clause,[status(thm)],[f1687,f977,f1582])).
% 9.41/1.62 fof(f1722,plain,(
% 9.41/1.62 ~vf(vd1050,vskolem1064(vskolem1063(vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048))=vf(vskolem1064(vskolem1063(vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vd1048)|~vf(vd1048,vd1050)=vf(vd1050,vskolem1064(vskolem1063(vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048))|~sQ55_spl),
% 9.41/1.62 inference(resolution,[status(thm)],[f1583,f910])).
% 9.41/1.62 fof(f1723,plain,(
% 9.41/1.62 vf(vd1048,vskolem1064(vskolem1063(vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048))=vf(vskolem1064(vskolem1063(vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vd1048)|~sQ55_spl),
% 9.41/1.62 inference(resolution,[status(thm)],[f1583,f908])).
% 9.41/1.62 fof(f1858,definition,(
% 9.41/1.62 sQ84_spl <=> (vf(vd1050,vskolem1064(vskolem1063(vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048))=vf(vskolem1064(vskolem1063(vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vd1048))),
% 9.41/1.62 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 9.41/1.62 fof(f1860,plain,(
% 9.41/1.62 ~vf(vd1050,vskolem1064(vskolem1063(vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048))=vf(vskolem1064(vskolem1063(vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vd1048)|sQ84_spl),
% 9.41/1.62 inference(component_clause,[status(thm)],[f1858])).
% 9.41/1.62 fof(f1861,definition,(
% 9.41/1.62 sQ85_spl <=> (vf(vd1048,vd1050)=vf(vd1050,vskolem1064(vskolem1063(vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048)))),
% 9.41/1.64 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 9.41/1.64 fof(f1863,plain,(
% 9.41/1.64 ~vf(vd1048,vd1050)=vf(vd1050,vskolem1064(vskolem1063(vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048))|sQ85_spl),
% 9.41/1.64 inference(component_clause,[status(thm)],[f1861])).
% 9.41/1.64 fof(f1864,plain,(
% 9.41/1.64 ~sQ84_spl|~sQ85_spl|~sQ55_spl),
% 9.41/1.64 inference(split_clause,[status(thm)],[f1722,f1858,f1861,f1582])).
% 9.41/1.64 fof(f1865,plain,(
% 9.41/1.64 vf(vd1048,vd1050)=vf(vskolem1064(vskolem1063(vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vd1048)|~sQ50_spl|~sQ55_spl),
% 9.41/1.64 inference(forward_demodulation,[status(thm)],[f1559,f1723])).
% 9.41/1.64 fof(f1871,plain,(
% 9.41/1.64 ~vf(vd1048,vd1050)=vf(vskolem1064(vskolem1063(vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vskolem1061(vd1050,vd1050,vd1048,vd1048),vd1050,vd1050,vd1048,vd1048),vd1048)|~sQ59_spl|sQ84_spl),
% 9.41/1.64 inference(forward_demodulation,[status(thm)],[f1608,f1860])).
% 9.41/1.64 fof(f2356,plain,(
% 9.41/1.64 $false|~sQ59_spl|sQ84_spl|~sQ50_spl|~sQ55_spl),
% 9.41/1.64 inference(forward_subsumption_resolution,[status(thm)],[f1865,f1871])).
% 9.41/1.64 fof(f2357,plain,(
% 9.41/1.64 ~sQ59_spl|sQ84_spl|~sQ50_spl|~sQ55_spl),
% 9.41/1.64 inference(contradiction_clause,[status(thm)],[f2356])).
% 9.41/1.64 fof(f2358,plain,(
% 9.41/1.64 ~vf(vd1048,vd1050)=vf(vd1048,vd1050)|~sQ59_spl|sQ85_spl),
% 9.41/1.64 inference(forward_demodulation,[status(thm)],[f1608,f1863])).
% 9.41/1.64 fof(f2359,plain,(
% 9.41/1.64 $false|~sQ59_spl|sQ85_spl),
% 9.41/1.64 inference(trivial_equality_resolution,[status(thm)],[f2358])).
% 9.41/1.64 fof(f2360,plain,(
% 9.41/1.64 ~sQ59_spl|sQ85_spl),
% 9.41/1.64 inference(contradiction_clause,[status(thm)],[f2359])).
% 9.41/1.64 fof(f2361,plain,(
% 9.41/1.64 $false),
% 9.41/1.64 inference(sat_refutation,[status(thm)],[f1094,f1354,f1483,f1558,f1607,f1680,f1689,f1864,f2357,f2360])).
% 9.41/1.64 % SZS output end CNFRefutation for theBenchmark.p
% 9.41/1.66 % Elapsed time: 1.286679 seconds
% 9.41/1.66 % CPU time: 9.772125 seconds
% 9.41/1.66 % Total memory used: 219.960 MB
% 9.41/1.66 % Net memory used: 212.951 MB
%------------------------------------------------------------------------------