%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO340+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 : n008.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:23 PM UTC 2026
% Result : Theorem 55.63s 7.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO340+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.36 % Computer : n008.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 15:30:09 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 55.63/7.45 % Refutation found
% 55.63/7.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 55.63/7.45 % SZS output start CNFRefutation for theBenchmark
% 55.63/7.45 fof(f1,conjecture,(
% 55.63/7.45 ~ (? [Vd1394] :( Vd1394 != vd1386& vf(vd1385,vd1386) = vf(vd1385,Vd1394)& vf(vd1384,vd1386) = vf(vd1384,Vd1394)& rS(vd1386,Vd1394,vd1391)& rpoint(Vd1394) ) )),
% 55.63/7.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 55.63/7.45 fof(f2,negated_conjecture,(
% 55.63/7.45 ~(~ (? [Vd1394] :( Vd1394 != vd1386& vf(vd1385,vd1386) = vf(vd1385,Vd1394)& vf(vd1384,vd1386) = vf(vd1384,Vd1394)& rS(vd1386,Vd1394,vd1391)& rpoint(Vd1394) ) ))),
% 55.63/7.45 inference(negated_conjecture,[status(cth)],[f1])).
% 55.63/7.45 fof(f3,axiom,(
% 55.63/7.45 ( vd1391 = vd1392& ron(vd1385,vd1391)& ron(vd1384,vd1391)& rline(vd1392)& vd1385 != vd1386& vd1384 != vd1386& vd1384 != vd1385& (? [Vd1390] :( vd1386 = Vd1390& rpoint(Vd1390) ))& (? [Vd1389] :( vd1385 = Vd1389& rpoint(Vd1389) ))& (? [Vd1388] :( vd1384 = Vd1388& rpoint(Vd1388) ) )) ),
% 55.63/7.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 55.63/7.45 fof(f4,axiom,(
% 55.63/7.45 (! [Vd1399,Vd1400,Vd1401,Vd1406,Vd1407] :( ( Vd1406 = Vd1407& ron(Vd1400,Vd1406)& ron(Vd1399,Vd1406)& rline(Vd1407)& Vd1400 != Vd1401& Vd1399 != Vd1401& Vd1399 != Vd1400& (? [Vd1405] :( Vd1401 = Vd1405& rpoint(Vd1405) ))& (? [Vd1404] :( Vd1400 = Vd1404& rpoint(Vd1404) ))& (? [Vd1403] :( Vd1399 = Vd1403& rpoint(Vd1403) ) ))=> (! [Vd1409] :( ( Vd1409 != Vd1401& vf(Vd1400,Vd1401) = vf(Vd1400,Vd1409)& vf(Vd1399,Vd1401) = vf(Vd1399,Vd1409)& rS(Vd1401,Vd1409,Vd1406)& rpoint(Vd1409) )=> (! [Vd1415] :( Vd1415 = vskolem1416(Vd1409,Vd1399,Vd1400,Vd1401,Vd1406,Vd1407)=> (! [Vd1418] : Vd1418 != vskolem1419(Vd1415,Vd1409,Vd1399,Vd1400,Vd1401,Vd1406,Vd1407) )) )) )) )),
% 55.63/7.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 55.63/7.45 fof(f30,axiom,(
% 55.63/7.45 (! [Vd761,Vd762] :( ( (? [Vd765] :( Vd762 = Vd765& rpoint(Vd765) ))& (? [Vd764] :( Vd761 = Vd764& rpoint(Vd764) ) ))=> vf(Vd761,Vd762) = vf(Vd762,Vd761) ) )),
% 55.63/7.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 55.63/7.45 fof(f31,axiom,(
% 55.63/7.45 (! [Vd748,Vd749] :( ( (? [Vd752] :( Vd749 = Vd752& rpoint(Vd752) ))& (? [Vd751] :( Vd748 = Vd751& rpoint(Vd751) ) ))=> ( vf(Vd748,Vd749) = v0<=> Vd748 = Vd749 ) ) )),
% 55.63/7.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 55.63/7.45 fof(f113,axiom,(
% 55.63/7.45 rpoint(vd14) ),
% 55.63/7.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 55.63/7.45 fof(f126,plain,(
% 55.63/7.45 ((((~sK0_skl=vd1386&vf(vd1385,vd1386)=vf(vd1385,sK0_skl))&vf(vd1384,vd1386)=vf(vd1384,sK0_skl))&rS(vd1386,sK0_skl,vd1391))&rpoint(sK0_skl))),
% 55.63/7.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Vd1394,sK0_skl)],[f2])).
% 55.63/7.45 fof(f127,plain,(
% 55.63/7.45 ~sK0_skl=vd1386),
% 55.63/7.45 inference(cnf_transformation,[status(thm)],[f126])).
% 55.63/7.45 fof(f128,plain,(
% 55.63/7.45 vf(vd1385,vd1386)=vf(vd1385,sK0_skl)),
% 55.63/7.45 inference(cnf_transformation,[status(thm)],[f126])).
% 55.63/7.45 fof(f129,plain,(
% 55.63/7.45 vf(vd1384,vd1386)=vf(vd1384,sK0_skl)),
% 55.63/7.45 inference(cnf_transformation,[status(thm)],[f126])).
% 55.63/7.45 fof(f130,plain,(
% 55.63/7.45 rS(vd1386,sK0_skl,vd1391)),
% 55.63/7.45 inference(cnf_transformation,[status(thm)],[f126])).
% 55.63/7.45 fof(f131,plain,(
% 55.63/7.45 rpoint(sK0_skl)),
% 55.63/7.45 inference(cnf_transformation,[status(thm)],[f126])).
% 55.63/7.45 fof(f132,plain,(
% 55.63/7.45 ((((((((vd1391=vd1392&ron(vd1385,vd1391))&ron(vd1384,vd1391))&rline(vd1392))&~vd1385=vd1386)&~vd1384=vd1386)&~vd1384=vd1385)&(vd1386=sK1_skl&rpoint(sK1_skl)))&(vd1385=sK2_skl&rpoint(sK2_skl)))&(vd1384=sK3_skl&rpoint(sK3_skl))),
% 55.63/7.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl,sK3_skl]),skolemize(Vd1390,sK1_skl),skolemize(Vd1389,sK2_skl),skolemize(Vd1388,sK3_skl)],[f3])).
% 55.63/7.45 fof(f133,plain,(
% 55.63/7.45 vd1391=vd1392),
% 55.63/7.45 inference(cnf_transformation,[status(thm)],[f132])).
% 55.63/7.45 fof(f134,plain,(
% 55.63/7.45 ron(vd1385,vd1391)),
% 55.63/7.45 inference(cnf_transformation,[status(thm)],[f132])).
% 55.63/7.45 fof(f135,plain,(
% 55.63/7.45 ron(vd1384,vd1391)),
% 55.63/7.45 inference(cnf_transformation,[status(thm)],[f132])).
% 55.63/7.45 fof(f136,plain,(
% 55.63/7.45 rline(vd1392)),
% 55.63/7.45 inference(cnf_transformation,[status(thm)],[f132])).
% 55.63/7.45 fof(f137,plain,(
% 55.63/7.45 ~vd1385=vd1386),
% 55.63/7.45 inference(cnf_transformation,[status(thm)],[f132])).
% 55.63/7.45 fof(f138,plain,(
% 55.63/7.45 ~vd1384=vd1386),
% 55.63/7.45 inference(cnf_transformation,[status(thm)],[f132])).
% 55.63/7.45 fof(f139,plain,(
% 55.63/7.45 ~vd1384=vd1385),
% 55.63/7.45 inference(cnf_transformation,[status(thm)],[f132])).
% 55.63/7.45 fof(f140,plain,(
% 55.63/7.45 vd1386=sK1_skl),
% 55.63/7.45 inference(cnf_transformation,[status(thm)],[f132])).
% 55.63/7.45 fof(f141,plain,(
% 55.63/7.45 rpoint(sK1_skl)),
% 55.63/7.45 inference(cnf_transformation,[status(thm)],[f132])).
% 55.63/7.45 fof(f142,plain,(
% 55.63/7.45 vd1385=sK2_skl),
% 55.63/7.45 inference(cnf_transformation,[status(thm)],[f132])).
% 55.63/7.45 fof(f143,plain,(
% 55.63/7.45 rpoint(sK2_skl)),
% 55.63/7.45 inference(cnf_transformation,[status(thm)],[f132])).
% 55.63/7.45 fof(f144,plain,(
% 55.63/7.45 vd1384=sK3_skl),
% 55.63/7.45 inference(cnf_transformation,[status(thm)],[f132])).
% 55.63/7.45 fof(f145,plain,(
% 55.63/7.45 rpoint(sK3_skl)),
% 55.63/7.45 inference(cnf_transformation,[status(thm)],[f132])).
% 55.63/7.45 fof(f146,plain,(
% 55.63/7.45 ![Vd1399,Vd1400,Vd1401,Vd1406,Vd1407]: ((((((((((~Vd1406=Vd1407|~ron(Vd1400,Vd1406))|~ron(Vd1399,Vd1406))|~rline(Vd1407))|Vd1400=Vd1401)|Vd1399=Vd1401)|Vd1399=Vd1400)|(![Vd1405]: (~Vd1401=Vd1405|~rpoint(Vd1405))))|(![Vd1404]: (~Vd1400=Vd1404|~rpoint(Vd1404))))|(![Vd1403]: (~Vd1399=Vd1403|~rpoint(Vd1403))))|(![Vd1409]: (((((Vd1409=Vd1401|~vf(Vd1400,Vd1401)=vf(Vd1400,Vd1409))|~vf(Vd1399,Vd1401)=vf(Vd1399,Vd1409))|~rS(Vd1401,Vd1409,Vd1406))|~rpoint(Vd1409))|(![Vd1415]: (~Vd1415=vskolem1416(Vd1409,Vd1399,Vd1400,Vd1401,Vd1406,Vd1407)|(![Vd1418]: ~Vd1418=vskolem1419(Vd1415,Vd1409,Vd1399,Vd1400,Vd1401,Vd1406,Vd1407)))))))),
% 55.63/7.45 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 55.63/7.45 fof(f147,plain,(
% 55.63/7.45 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10]: (~X0=X1|~ron(X2,X0)|~ron(X3,X0)|~rline(X1)|X2=X4|X3=X4|X3=X2|~X4=X5|~rpoint(X5)|~X2=X6|~rpoint(X6)|~X3=X7|~rpoint(X7)|X8=X4|~vf(X2,X4)=vf(X2,X8)|~vf(X3,X4)=vf(X3,X8)|~rS(X4,X8,X0)|~rpoint(X8)|~X9=vskolem1416(X8,X3,X2,X4,X0,X1)|~X10=vskolem1419(X9,X8,X3,X2,X4,X0,X1))),
% 55.63/7.45 inference(cnf_transformation,[status(thm)],[f146])).
% 55.63/7.45 fof(f230,plain,(
% 55.63/7.45 ![Vd761,Vd762]: (((![Vd765]: (~Vd762=Vd765|~rpoint(Vd765)))|(![Vd764]: (~Vd761=Vd764|~rpoint(Vd764))))|vf(Vd761,Vd762)=vf(Vd762,Vd761))),
% 55.63/7.45 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 55.63/7.45 fof(f231,plain,(
% 55.63/7.45 ![X0,X1,X2,X3]: (~X0=X1|~rpoint(X1)|~X2=X3|~rpoint(X3)|vf(X2,X0)=vf(X0,X2))),
% 55.63/7.45 inference(cnf_transformation,[status(thm)],[f230])).
% 55.63/7.45 fof(f232,plain,(
% 55.63/7.45 ![Vd748,Vd749]: (((![Vd752]: (~Vd749=Vd752|~rpoint(Vd752)))|(![Vd751]: (~Vd748=Vd751|~rpoint(Vd751))))|(vf(Vd748,Vd749)=v0<=>Vd748=Vd749))),
% 55.63/7.45 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 55.63/7.45 fof(f233,plain,(
% 55.63/7.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)))),
% 55.63/7.45 inference(NNF_transformation,[status(thm)],[f232])).
% 55.63/7.45 fof(f235,plain,(
% 55.63/7.45 ![X0,X1,X2,X3]: (~X0=X1|~rpoint(X1)|~X2=X3|~rpoint(X3)|vf(X2,X0)=v0|~X2=X0)),
% 55.63/7.45 inference(cnf_transformation,[status(thm)],[f233])).
% 55.63/7.45 fof(f609,plain,(
% 55.63/7.45 rpoint(vd14)),
% 55.63/7.45 inference(cnf_transformation,[status(thm)],[f113])).
% 55.63/7.45 fof(f720,plain,(
% 55.63/7.45 ![X0,X1,X2,X3,X4]: (~ron(X0,X1)|~ron(X2,X1)|~rline(X1)|X0=X3|X2=X3|X2=X0|~rpoint(X3)|~rpoint(X0)|~rpoint(X2)|X4=X3|~vf(X0,X3)=vf(X0,X4)|~vf(X2,X3)=vf(X2,X4)|~rS(X3,X4,X1)|~rpoint(X4))),
% 55.63/7.45 inference(destructive_equality_resolution,[status(thm)],[f147])).
% 55.63/7.45 fof(f765,plain,(
% 55.63/7.45 ![X0,X1]: (~rpoint(X0)|~rpoint(X1)|vf(X1,X0)=vf(X0,X1))),
% 55.63/7.45 inference(destructive_equality_resolution,[status(thm)],[f231])).
% 55.63/7.45 fof(f767,plain,(
% 55.63/7.45 ![X1]: (~rpoint(X1)|~rpoint(X1)|vf(X1,X1)=v0)),
% 55.63/7.45 inference(destructive_equality_resolution,[status(thm)],[f235])).
% 55.63/7.45 fof(f768,plain,(
% 55.63/7.45 ![X0]: (~rpoint(X0)|vf(X0,X0)=v0)),
% 55.63/7.45 inference(duplicate_literals_removal,[status(thm)],[f767])).
% 55.63/7.45 fof(f967,definition,(
% 55.63/7.45 sQ8_spl <=> (rline(vd1391))),
% 55.63/7.45 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 55.63/7.45 fof(f969,plain,(
% 55.63/7.45 ~rline(vd1391)|sQ8_spl),
% 55.63/7.45 inference(component_clause,[status(thm)],[f967])).
% 55.63/7.45 fof(f970,definition,(
% 55.63/7.45 sQ9_spl <=> (rpoint(sK0_skl))),
% 55.63/7.45 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 55.63/7.45 fof(f972,plain,(
% 55.63/7.45 ~rpoint(sK0_skl)|sQ9_spl),
% 55.63/7.45 inference(component_clause,[status(thm)],[f970])).
% 55.63/7.45 fof(f973,definition,(
% 55.63/7.45 sQ10_spl <=> (rpoint(vd1386))),
% 55.63/7.45 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 55.63/7.45 fof(f975,plain,(
% 55.63/7.45 ~rpoint(vd1386)|sQ10_spl),
% 55.63/7.45 inference(component_clause,[status(thm)],[f973])).
% 55.63/7.45 fof(f989,definition,(
% 55.63/7.45 sQ14_spl <=> (sK0_skl=vd1386)),
% 55.63/7.45 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 55.63/7.45 fof(f990,plain,(
% 55.63/7.45 sK0_skl=vd1386|~sQ14_spl),
% 55.63/7.45 inference(component_clause,[status(thm)],[f989])).
% 55.63/7.45 fof(f993,plain,(
% 55.63/7.45 $false|sQ9_spl),
% 55.63/7.45 inference(forward_subsumption_resolution,[status(thm)],[f972,f131])).
% 55.63/7.45 fof(f994,plain,(
% 55.63/7.45 sQ9_spl),
% 55.63/7.45 inference(contradiction_clause,[status(thm)],[f993])).
% 55.63/7.45 fof(f1001,plain,(
% 55.63/7.45 rpoint(vd1386)),
% 55.63/7.45 inference(forward_demodulation,[status(thm)],[f140,f141])).
% 55.63/7.45 fof(f1002,plain,(
% 55.63/7.45 ![X0]: (~rpoint(X0)|vf(vd1386,X0)=vf(X0,vd1386))),
% 55.63/7.45 inference(resolution,[status(thm)],[f1001,f765])).
% 55.63/7.45 fof(f1003,plain,(
% 55.63/7.45 rpoint(vd1385)),
% 55.63/7.45 inference(forward_demodulation,[status(thm)],[f142,f143])).
% 55.63/7.45 fof(f1005,plain,(
% 55.63/7.45 rpoint(vd1384)),
% 55.63/7.45 inference(forward_demodulation,[status(thm)],[f144,f145])).
% 55.63/7.45 fof(f1010,plain,(
% 55.63/7.45 vf(sK0_skl,sK0_skl)=v0),
% 55.63/7.45 inference(resolution,[status(thm)],[f768,f131])).
% 55.63/7.45 fof(f1035,plain,(
% 55.63/7.45 rline(vd1391)),
% 55.63/7.45 inference(forward_demodulation,[status(thm)],[f133,f136])).
% 55.63/7.45 fof(f1036,plain,(
% 55.63/7.45 ![X0,X1]: (~ron(X0,X1)|~ron(vd1384,X1)|~rline(X1)|X0=vd1386|vd1384=vd1386|vd1384=X0|~rpoint(vd1386)|~rpoint(X0)|~rpoint(vd1384)|sK0_skl=vd1386|~vf(X0,vd1386)=vf(X0,sK0_skl)|~rS(vd1386,sK0_skl,X1)|~rpoint(sK0_skl))),
% 55.63/7.45 inference(resolution,[status(thm)],[f720,f129])).
% 55.63/7.45 fof(f1045,definition,(
% 55.63/7.45 ![X0,X1]: (sQ16_spl <=> (~ron(X0,X1)|~ron(vd1384,X1)|~rline(X1)|X0=vd1386|vd1384=X0|~rpoint(X0)|~vf(X0,vd1386)=vf(X0,sK0_skl)|~rS(vd1386,sK0_skl,X1)))),
% 55.63/7.45 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 55.63/7.45 fof(f1046,plain,(
% 55.63/7.45 ![X0,X1]: (~ron(X0,X1)|~ron(vd1384,X1)|~rline(X1)|X0=vd1386|vd1384=X0|~rpoint(X0)|~vf(X0,vd1386)=vf(X0,sK0_skl)|~rS(vd1386,sK0_skl,X1)|~sQ16_spl)),
% 55.63/7.45 inference(component_clause,[status(thm)],[f1045])).
% 55.63/7.45 fof(f1048,definition,(
% 55.63/7.45 sQ17_spl <=> (vd1384=vd1386)),
% 55.63/7.45 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 55.63/7.45 fof(f1049,plain,(
% 55.63/7.45 vd1384=vd1386|~sQ17_spl),
% 55.63/7.45 inference(component_clause,[status(thm)],[f1048])).
% 55.63/7.45 fof(f1051,definition,(
% 55.63/7.45 sQ18_spl <=> (rpoint(vd1384))),
% 55.63/7.45 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 55.63/7.45 fof(f1053,plain,(
% 55.63/7.45 ~rpoint(vd1384)|sQ18_spl),
% 55.63/7.45 inference(component_clause,[status(thm)],[f1051])).
% 55.63/7.45 fof(f1054,plain,(
% 55.63/7.45 sQ16_spl|sQ17_spl|~sQ10_spl|~sQ18_spl|sQ14_spl|~sQ9_spl),
% 55.63/7.45 inference(split_clause,[status(thm)],[f1036,f1045,f1048,f973,f1051,f989,f970])).
% 55.63/7.45 fof(f1058,definition,(
% 55.63/7.45 sQ20_spl <=> (vd1385=vd1386)),
% 55.63/7.45 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 55.63/7.45 fof(f1059,plain,(
% 55.63/7.45 vd1385=vd1386|~sQ20_spl),
% 55.63/7.45 inference(component_clause,[status(thm)],[f1058])).
% 55.63/7.45 fof(f1061,definition,(
% 55.63/7.45 sQ21_spl <=> (rpoint(vd1385))),
% 55.63/7.45 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 55.63/7.45 fof(f1063,plain,(
% 55.63/7.45 ~rpoint(vd1385)|sQ21_spl),
% 55.63/7.45 inference(component_clause,[status(thm)],[f1061])).
% 55.63/7.45 fof(f1095,plain,(
% 55.63/7.45 $false|sQ18_spl),
% 55.63/7.45 inference(forward_subsumption_resolution,[status(thm)],[f1053,f1005])).
% 55.63/7.45 fof(f1096,plain,(
% 55.63/7.45 sQ18_spl),
% 55.63/7.45 inference(contradiction_clause,[status(thm)],[f1095])).
% 55.63/7.45 fof(f1097,plain,(
% 55.63/7.45 $false|sQ21_spl),
% 55.63/7.45 inference(forward_subsumption_resolution,[status(thm)],[f1063,f1003])).
% 55.63/7.45 fof(f1098,plain,(
% 55.63/7.45 sQ21_spl),
% 55.63/7.45 inference(contradiction_clause,[status(thm)],[f1097])).
% 55.63/7.45 fof(f1207,plain,(
% 55.63/7.45 $false|sQ10_spl),
% 55.63/7.45 inference(forward_subsumption_resolution,[status(thm)],[f975,f1001])).
% 55.63/7.45 fof(f1208,plain,(
% 55.63/7.45 sQ10_spl),
% 55.63/7.45 inference(contradiction_clause,[status(thm)],[f1207])).
% 55.63/7.45 fof(f1209,plain,(
% 55.63/7.45 $false|sQ8_spl),
% 55.63/7.45 inference(forward_subsumption_resolution,[status(thm)],[f969,f1035])).
% 55.63/7.45 fof(f1210,plain,(
% 55.63/7.45 sQ8_spl),
% 55.63/7.45 inference(contradiction_clause,[status(thm)],[f1209])).
% 55.63/7.45 fof(f1211,plain,(
% 55.63/7.45 $false|~sQ14_spl),
% 55.63/7.45 inference(forward_subsumption_resolution,[status(thm)],[f990,f127])).
% 55.63/7.45 fof(f1212,plain,(
% 55.63/7.45 ~sQ14_spl),
% 55.63/7.45 inference(contradiction_clause,[status(thm)],[f1211])).
% 55.63/7.45 fof(f1328,definition,(
% 55.63/7.45 sQ63_spl <=> (ron(vd1384,vd1391))),
% 55.63/7.45 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 55.63/7.45 fof(f1330,plain,(
% 55.63/7.45 ~ron(vd1384,vd1391)|sQ63_spl),
% 55.63/7.45 inference(component_clause,[status(thm)],[f1328])).
% 55.63/7.45 fof(f1398,plain,(
% 55.63/7.45 $false|~sQ17_spl),
% 55.63/7.45 inference(forward_subsumption_resolution,[status(thm)],[f1049,f138])).
% 55.63/7.45 fof(f1399,plain,(
% 55.63/7.45 ~sQ17_spl),
% 55.63/7.45 inference(contradiction_clause,[status(thm)],[f1398])).
% 55.63/7.45 fof(f1411,definition,(
% 55.63/7.45 sQ79_spl <=> (vd1385=vd1384)),
% 55.63/7.45 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 55.63/7.45 fof(f1412,plain,(
% 55.63/7.45 vd1385=vd1384|~sQ79_spl),
% 55.63/7.45 inference(component_clause,[status(thm)],[f1411])).
% 55.63/7.45 fof(f1423,plain,(
% 55.63/7.45 $false|~sQ20_spl),
% 55.63/7.45 inference(forward_subsumption_resolution,[status(thm)],[f1059,f137])).
% 55.63/7.45 fof(f1424,plain,(
% 55.63/7.45 ~sQ20_spl),
% 55.63/7.45 inference(contradiction_clause,[status(thm)],[f1423])).
% 55.63/7.45 fof(f1425,plain,(
% 55.63/7.45 $false|~sQ79_spl),
% 55.63/7.45 inference(forward_subsumption_resolution,[status(thm)],[f1412,f139])).
% 55.63/7.45 fof(f1426,plain,(
% 55.63/7.45 ~sQ79_spl),
% 55.63/7.45 inference(contradiction_clause,[status(thm)],[f1425])).
% 55.63/7.45 fof(f1497,plain,(
% 55.63/7.45 $false|sQ63_spl),
% 55.63/7.45 inference(forward_subsumption_resolution,[status(thm)],[f1330,f135])).
% 55.63/7.45 fof(f1498,plain,(
% 55.63/7.45 sQ63_spl),
% 55.63/7.45 inference(contradiction_clause,[status(thm)],[f1497])).
% 55.63/7.45 fof(f2210,definition,(
% 55.63/7.45 sQ197_spl <=> (ron(vd1385,vd1391))),
% 55.63/7.45 introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition])).
% 55.63/7.45 fof(f2212,plain,(
% 55.63/7.45 ~ron(vd1385,vd1391)|sQ197_spl),
% 55.63/7.45 inference(component_clause,[status(thm)],[f2210])).
% 55.63/7.45 fof(f3400,plain,(
% 55.63/7.45 vf(vd1386,vd1384)=vf(vd1384,vd1386)),
% 55.63/7.45 inference(resolution,[status(thm)],[f1002,f1005])).
% 55.63/7.45 fof(f3401,plain,(
% 55.63/7.45 vf(vd1386,vd1385)=vf(vd1385,vd1386)),
% 55.63/7.45 inference(resolution,[status(thm)],[f1002,f1003])).
% 55.63/7.45 fof(f3403,plain,(
% 55.63/7.45 vf(vd1386,vd1384)=vf(vd1384,sK0_skl)),
% 55.63/7.45 inference(backward_demodulation,[status(thm)],[f3400,f129])).
% 55.63/7.45 fof(f3466,plain,(
% 55.63/7.45 vf(vd1386,vd1385)=vf(vd1385,sK0_skl)),
% 55.63/7.45 inference(backward_demodulation,[status(thm)],[f3401,f128])).
% 55.63/7.45 fof(f4000,plain,(
% 55.63/7.45 $false|sQ197_spl),
% 55.63/7.45 inference(forward_subsumption_resolution,[status(thm)],[f2212,f134])).
% 55.63/7.45 fof(f4001,plain,(
% 55.63/7.45 sQ197_spl),
% 55.63/7.45 inference(contradiction_clause,[status(thm)],[f4000])).
% 55.63/7.45 fof(f4344,definition,(
% 55.63/7.45 sQ493_spl <=> (vf(sK0_skl,sK0_skl)=v0)),
% 55.63/7.45 introduced(definition,[new_symbols(definition,[sQ493_spl])],[split_symbol_definition])).
% 55.63/7.45 fof(f4346,plain,(
% 55.63/7.45 ~vf(sK0_skl,sK0_skl)=v0|sQ493_spl),
% 55.63/7.45 inference(component_clause,[status(thm)],[f4344])).
% 55.63/7.45 fof(f4653,definition,(
% 55.63/7.45 sQ541_spl <=> (vf(vd1384,vd1386)=vf(vd1384,sK0_skl))),
% 55.63/7.45 introduced(definition,[new_symbols(definition,[sQ541_spl])],[split_symbol_definition])).
% 55.63/7.45 fof(f4655,plain,(
% 55.63/7.45 ~vf(vd1384,vd1386)=vf(vd1384,sK0_skl)|sQ541_spl),
% 55.63/7.45 inference(component_clause,[status(thm)],[f4653])).
% 55.63/7.45 fof(f4678,plain,(
% 55.63/7.45 ![X0]: (~ron(vd1385,X0)|~ron(vd1384,X0)|~rline(X0)|vd1385=vd1386|vd1384=vd1385|~rpoint(vd1385)|~vf(vd1385,vd1386)=vf(vd1386,vd1385)|~rS(vd1386,sK0_skl,X0)|~sQ16_spl)),
% 55.63/7.45 inference(paramodulation,[status(thm)],[f3466,f1046])).
% 55.63/7.45 fof(f4687,definition,(
% 55.63/7.45 ![X0]: (sQ548_spl <=> (~ron(vd1385,X0)|~ron(vd1384,X0)|~rline(X0)|~rS(vd1386,sK0_skl,X0)))),
% 55.63/7.45 introduced(definition,[new_symbols(definition,[sQ548_spl])],[split_symbol_definition])).
% 55.63/7.45 fof(f4688,plain,(
% 55.63/7.45 ![X0]: (~ron(vd1385,X0)|~ron(vd1384,X0)|~rline(X0)|~rS(vd1386,sK0_skl,X0)|~sQ548_spl)),
% 55.63/7.45 inference(component_clause,[status(thm)],[f4687])).
% 55.63/7.45 fof(f4690,definition,(
% 55.63/7.45 sQ549_spl <=> (vf(vd1385,vd1386)=vf(vd1386,vd1385))),
% 55.63/7.45 introduced(definition,[new_symbols(definition,[sQ549_spl])],[split_symbol_definition])).
% 55.63/7.45 fof(f4692,plain,(
% 55.63/7.45 ~vf(vd1385,vd1386)=vf(vd1386,vd1385)|sQ549_spl),
% 55.63/7.45 inference(component_clause,[status(thm)],[f4690])).
% 55.63/7.45 fof(f4693,plain,(
% 55.63/7.45 sQ548_spl|sQ20_spl|sQ79_spl|~sQ21_spl|~sQ549_spl|~sQ16_spl),
% 55.63/7.45 inference(split_clause,[status(thm)],[f4678,f4687,f1058,f1411,f1061,f4690,f1045])).
% 55.63/7.45 fof(f4705,plain,(
% 55.63/7.45 ~vf(vd1386,vd1385)=vf(vd1386,vd1385)|sQ549_spl),
% 55.63/7.45 inference(forward_demodulation,[status(thm)],[f3401,f4692])).
% 55.63/7.45 fof(f4706,plain,(
% 55.63/7.45 $false|sQ549_spl),
% 55.63/7.45 inference(trivial_equality_resolution,[status(thm)],[f4705])).
% 55.63/7.45 fof(f4707,plain,(
% 55.63/7.45 sQ549_spl),
% 55.63/7.45 inference(contradiction_clause,[status(thm)],[f4706])).
% 55.63/7.46 fof(f5345,definition,(
% 55.63/7.46 ![X0]: (sQ659_spl <=> (~rpoint(X0)))),
% 55.63/7.46 introduced(definition,[new_symbols(definition,[sQ659_spl])],[split_symbol_definition])).
% 55.63/7.46 fof(f5346,plain,(
% 55.63/7.46 ![X0]: (~rpoint(X0)|~sQ659_spl)),
% 55.63/7.46 inference(component_clause,[status(thm)],[f5345])).
% 55.63/7.46 fof(f5352,plain,(
% 55.63/7.46 $false|~sQ659_spl),
% 55.63/7.46 inference(backward_subsumption_resolution,[status(thm)],[f131,f5346])).
% 55.63/7.46 fof(f5356,plain,(
% 55.63/7.46 ~sQ659_spl),
% 55.63/7.46 inference(contradiction_clause,[status(thm)],[f5352])).
% 55.63/7.46 fof(f5447,plain,(
% 55.63/7.46 ~v0=v0|sQ493_spl),
% 55.63/7.46 inference(forward_demodulation,[status(thm)],[f1010,f4346])).
% 55.63/7.46 fof(f5448,plain,(
% 55.63/7.46 $false|sQ493_spl),
% 55.63/7.46 inference(trivial_equality_resolution,[status(thm)],[f5447])).
% 55.63/7.46 fof(f5449,plain,(
% 55.63/7.46 sQ493_spl),
% 55.63/7.46 inference(contradiction_clause,[status(thm)],[f5448])).
% 55.63/7.46 fof(f5462,plain,(
% 55.63/7.46 ~vf(vd1386,vd1384)=vf(vd1384,sK0_skl)|sQ541_spl),
% 55.63/7.46 inference(forward_demodulation,[status(thm)],[f3400,f4655])).
% 55.63/7.46 fof(f5463,plain,(
% 55.63/7.46 ~vf(vd1386,vd1384)=vf(vd1386,vd1384)|sQ541_spl),
% 55.63/7.46 inference(forward_demodulation,[status(thm)],[f3403,f5462])).
% 55.63/7.46 fof(f5464,plain,(
% 55.63/7.46 $false|sQ541_spl),
% 55.63/7.46 inference(trivial_equality_resolution,[status(thm)],[f5463])).
% 55.63/7.46 fof(f5465,plain,(
% 55.63/7.46 sQ541_spl),
% 55.63/7.46 inference(contradiction_clause,[status(thm)],[f5464])).
% 55.63/7.46 fof(f7815,plain,(
% 55.63/7.46 vf(vd14,vd14)=v0),
% 55.63/7.46 inference(resolution,[status(thm)],[f609,f768])).
% 55.63/7.46 fof(f7851,definition,(
% 55.63/7.46 sQ1021_spl <=> (vf(vd14,vd14)=vf(vd14,vd14))),
% 55.63/7.46 introduced(definition,[new_symbols(definition,[sQ1021_spl])],[split_symbol_definition])).
% 55.63/7.46 fof(f7853,plain,(
% 55.63/7.46 ~vf(vd14,vd14)=vf(vd14,vd14)|sQ1021_spl),
% 55.63/7.46 inference(component_clause,[status(thm)],[f7851])).
% 55.63/7.46 fof(f8118,definition,(
% 55.63/7.46 sQ1072_spl <=> (rpoint(vd14))),
% 55.63/7.46 introduced(definition,[new_symbols(definition,[sQ1072_spl])],[split_symbol_definition])).
% 55.63/7.46 fof(f8120,plain,(
% 55.63/7.46 ~rpoint(vd14)|sQ1072_spl),
% 55.63/7.46 inference(component_clause,[status(thm)],[f8118])).
% 55.63/7.46 fof(f9423,plain,(
% 55.63/7.46 $false|sQ1072_spl),
% 55.63/7.46 inference(forward_subsumption_resolution,[status(thm)],[f8120,f609])).
% 55.63/7.46 fof(f9424,plain,(
% 55.63/7.46 sQ1072_spl),
% 55.63/7.46 inference(contradiction_clause,[status(thm)],[f9423])).
% 55.63/7.46 fof(f9786,plain,(
% 55.63/7.46 ~v0=vf(vd14,vd14)|sQ1021_spl),
% 55.63/7.46 inference(forward_demodulation,[status(thm)],[f7815,f7853])).
% 55.63/7.46 fof(f9787,plain,(
% 55.63/7.46 ~v0=v0|sQ1021_spl),
% 55.63/7.46 inference(forward_demodulation,[status(thm)],[f7815,f9786])).
% 55.63/7.46 fof(f9788,plain,(
% 55.63/7.46 $false|sQ1021_spl),
% 55.63/7.46 inference(trivial_equality_resolution,[status(thm)],[f9787])).
% 55.63/7.46 fof(f9789,plain,(
% 55.63/7.46 sQ1021_spl),
% 55.63/7.46 inference(contradiction_clause,[status(thm)],[f9788])).
% 55.63/7.46 fof(f13582,plain,(
% 55.63/7.46 ~ron(vd1385,vd1391)|~ron(vd1384,vd1391)|~rline(vd1391)|~sQ548_spl),
% 55.63/7.46 inference(resolution,[status(thm)],[f4688,f130])).
% 55.63/7.46 fof(f13583,plain,(
% 55.63/7.46 ~sQ197_spl|~sQ63_spl|~sQ8_spl|~sQ548_spl),
% 55.63/7.46 inference(split_clause,[status(thm)],[f13582,f2210,f1328,f967,f4687])).
% 55.63/7.46 fof(f13584,plain,(
% 55.63/7.46 $false),
% 55.63/7.46 inference(sat_refutation,[status(thm)],[f994,f1054,f1096,f1098,f1208,f1210,f1212,f1399,f1424,f1426,f1498,f4001,f4693,f4707,f5356,f5449,f5465,f9424,f9789,f13583])).
% 55.63/7.46 % SZS output end CNFRefutation for theBenchmark.p
% 55.63/7.48 % Elapsed time: 7.100321 seconds
% 55.63/7.48 % CPU time: 56.070024 seconds
% 55.63/7.48 % Total memory used: 263.522 MB
% 55.63/7.48 % Net memory used: 247.999 MB
%------------------------------------------------------------------------------