%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO528+1 : TPTP v9.3.1. Released v7.0.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:35 PM UTC 2026
% Result : Theorem 137.82s 17.85s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO528+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n007.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 20 17:11:20 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 137.82/17.85 % Refutation found
% 137.82/17.85 % SZS status Theorem for theBenchmark: Theorem is valid
% 137.82/17.85 % SZS output start CNFRefutation for theBenchmark
% 137.82/17.85 fof(f40,axiom,(
% 137.82/17.85 (! [Xa,Xb,Xc] :( ~ s_col(Xa,Xb,Xc)| s_col(Xb,Xc,Xa) ) )),
% 137.82/17.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 137.82/17.85 fof(f42,axiom,(
% 137.82/17.85 (! [Xa,Xb,Xc] :( ~ s_col(Xa,Xb,Xc)| s_col(Xc,Xb,Xa) ) )),
% 137.82/17.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 137.82/17.85 fof(f43,axiom,(
% 137.82/17.85 (! [Xa,Xb,Xc] :( ~ s_col(Xa,Xb,Xc)| s_col(Xb,Xa,Xc) ) )),
% 137.82/17.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 137.82/17.85 fof(f45,axiom,(
% 137.82/17.85 (! [Xa,Xb] : s_col(Xa,Xa,Xb) )),
% 137.82/17.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 137.82/17.85 fof(f46,axiom,(
% 137.82/17.85 (! [Xa,Xb] : s_col(Xa,Xb,Xa) )),
% 137.82/17.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 137.82/17.85 fof(f146,axiom,(
% 137.82/17.85 (! [Xa,Xb] : s_m(Xa,midpoint(Xa,Xb),Xb) )),
% 137.82/17.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 137.82/17.85 fof(f171,axiom,(
% 137.82/17.85 (! [Xa,Xp,Xq,Xb] :( ~ opposite(Xa,Xp,Xq,Xb)| ~ samesideline(Xa,Xb,Xp,Xq) ) )),
% 137.82/17.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 137.82/17.85 fof(f181,axiom,(
% 137.82/17.85 (! [Xp,Xq,Xr,Xcs] :( Xp = Xq| s_col(Xp,Xq,Xr)| s_col(Xp,Xq,Xcs)| samesideline(Xr,Xcs,Xp,Xq)| opposite(Xr,Xp,Xq,Xcs) ) )),
% 137.82/17.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 137.82/17.85 fof(f184,axiom,(
% 137.82/17.85 (! [Xa,Xb,Xp] :( ( Xa = Xb| s_col(Xa,Xb,midpoint(Xp,reflect(Xa,Xb,Xp))) )& ( Xa = Xb| Xp = reflect(Xa,Xb,Xp)| perp(Xa,Xb,Xp,reflect(Xa,Xb,Xp)) ) ) )),
% 137.82/17.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 137.82/17.85 fof(f186,axiom,(
% 137.82/17.85 (! [Xa,Xb,Xp,Xp1] :( Xa = Xb| reflect(Xa,Xb,Xp) != Xp1| reflect(Xa,Xb,Xp1) = Xp ) )),
% 137.82/17.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 137.82/17.85 fof(f190,axiom,(
% 137.82/17.85 (! [Xa,Xb,Xp] :( Xa = Xb| reflect(Xa,Xb,Xp) != Xp| s_col(Xa,Xb,Xp) ) )),
% 137.82/17.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 137.82/17.85 fof(f191,axiom,(
% 137.82/17.85 (! [Xa,Xb,Xp] :( Xa = Xb| ~ s_col(Xa,Xb,Xp)| reflect(Xa,Xb,Xp) = Xp ) )),
% 137.82/17.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 137.82/17.85 fof(f198,conjecture,(
% 137.82/17.85 (! [Xa,Xb,Xp,Xp1] :( Xa = Xb| reflect(Xa,Xb,Xp) != Xp1| s_col(Xa,Xb,Xp)| opposite(Xp,Xa,Xb,Xp1) ) )),
% 137.82/17.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 137.82/17.85 fof(f199,negated_conjecture,(
% 137.82/17.85 ~((! [Xa,Xb,Xp,Xp1] :( Xa = Xb| reflect(Xa,Xb,Xp) != Xp1| s_col(Xa,Xb,Xp)| opposite(Xp,Xa,Xb,Xp1) ) ))),
% 137.82/17.85 inference(negated_conjecture,[status(cth)],[f198])).
% 137.82/17.85 fof(f208,axiom,(
% 137.82/17.85 (! [Xa,Xm,Xb] :( ( ~ s_m(Xa,Xm,Xb)| s_t(Xa,Xm,Xb) )& ( ~ s_m(Xa,Xm,Xb)| s_e(Xm,Xa,Xm,Xb) )& ( ~ s_t(Xa,Xm,Xb)| ~ s_e(Xm,Xa,Xm,Xb)| s_m(Xa,Xm,Xb) ) ) )),
% 137.82/17.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 137.82/17.85 fof(f213,axiom,(
% 137.82/17.85 (! [Xp,Xq,Xa,Xb,Xt] :( ( Xp = Xq| s_col(Xp,Xq,Xa)| s_col(Xp,Xq,Xb)| ~ s_t(Xa,Xt,Xb)| ~ s_col(Xp,Xq,Xt)| opposite(Xa,Xp,Xq,Xb) )& ( ~ opposite(Xa,Xp,Xq,Xb)| ~ s_col(Xp,Xq,Xa) )& ( ~ opposite(Xa,Xp,Xq,Xb)| ~ s_col(Xp,Xq,Xb) )& ( ~ opposite(Xa,Xp,Xq,Xb)| s_t(Xa,il(Xa,Xb,Xp,Xq),Xb) )& ( ~ opposite(Xa,Xp,Xq,Xb)| s_col(Xp,Xq,il(Xa,Xb,Xp,Xq)) ) ) )),
% 137.82/17.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 137.82/17.85 fof(f214,axiom,(
% 137.82/17.85 (! [Xa,Xb,Xp,Xq,Xu,Xc,Xv] :( ( ~ samesideline(Xa,Xb,Xp,Xq)| s_col(Xp,Xq,ss1(Xa,Xb,Xp,Xq)) )& ( ~ samesideline(Xa,Xb,Xp,Xq)| s_col(Xp,Xq,ss2(Xa,Xb,Xp,Xq)) )& ( ~ samesideline(Xa,Xb,Xp,Xq)| s_t(Xa,ss1(Xa,Xb,Xp,Xq),ss3(Xa,Xb,Xp,Xq)) )& ( ~ samesideline(Xa,Xb,Xp,Xq)| s_t(Xb,ss2(Xa,Xb,Xp,Xq),ss3(Xa,Xb,Xp,Xq)) )& ( ~ samesideline(Xa,Xb,Xp,Xq)| Xa != ss1(Xa,Xb,Xp,Xq) )& ( ~ samesideline(Xa,Xb,Xp,Xq)| Xb != ss2(Xa,Xb,Xp,Xq) )& ( ~ samesideline(Xa,Xb,Xp,Xq)| ss3(Xa,Xb,Xp,Xq) != ss1(Xa,Xb,Xp,Xq) )& ( ~ samesideline(Xa,Xb,Xp,Xq)| ss3(Xa,Xb,Xp,Xq) != ss2(Xa,Xb,Xp,Xq) )& ( ~ samesideline(Xa,Xb,Xp,Xq)| Xp != Xq )& ( ~ samesideline(Xa,Xb,Xp,Xq)| ~ s_col(Xp,Xq,Xa) )& ( ~ samesideline(Xa,Xb,Xp,Xq)| ~ s_col(Xp,Xq,Xb) )& ( ~ s_t(Xa,Xu,Xc)| ~ s_t(Xb,Xv,Xc)| ~ s_col(Xp,Xq,Xu)| ~ s_col(Xp,Xq,Xv)| Xp = Xq| Xc = Xu| Xc = Xv| Xa = Xu| Xb = Xv| s_col(Xp,Xq,Xa)| s_col(Xp,Xq,Xb)| samesideline(Xa,Xb,Xp,Xq) ) ) )),
% 137.82/17.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 137.82/17.85 fof(f281,plain,(
% 137.82/17.85 ![X0,X1,X2]: (~s_col(X0,X1,X2)|s_col(X1,X2,X0))),
% 137.82/17.85 inference(cnf_transformation,[status(thm)],[f40])).
% 137.82/17.85 fof(f283,plain,(
% 137.82/17.85 ![X0,X1,X2]: (~s_col(X0,X1,X2)|s_col(X2,X1,X0))),
% 137.82/17.85 inference(cnf_transformation,[status(thm)],[f42])).
% 137.82/17.85 fof(f284,plain,(
% 137.82/17.85 ![X0,X1,X2]: (~s_col(X0,X1,X2)|s_col(X1,X0,X2))),
% 137.82/17.85 inference(cnf_transformation,[status(thm)],[f43])).
% 137.82/17.85 fof(f286,plain,(
% 137.82/17.85 ![X0,X1]: (s_col(X0,X0,X1))),
% 137.82/17.85 inference(cnf_transformation,[status(thm)],[f45])).
% 137.82/17.85 fof(f287,plain,(
% 137.82/17.85 ![X0,X1]: (s_col(X0,X1,X0))),
% 137.82/17.85 inference(cnf_transformation,[status(thm)],[f46])).
% 137.82/17.85 fof(f470,plain,(
% 137.82/17.85 ![X0,X1]: (s_m(X0,midpoint(X0,X1),X1))),
% 137.82/17.85 inference(cnf_transformation,[status(thm)],[f146])).
% 137.82/17.85 fof(f516,plain,(
% 137.82/17.85 ![X0,X1,X2,X3]: (~opposite(X0,X1,X2,X3)|~samesideline(X0,X3,X1,X2))),
% 137.82/17.85 inference(cnf_transformation,[status(thm)],[f171])).
% 137.82/17.85 fof(f533,plain,(
% 137.82/17.85 ![X0,X1,X2,X3]: (X0=X1|s_col(X0,X1,X2)|s_col(X0,X1,X3)|samesideline(X2,X3,X0,X1)|opposite(X2,X0,X1,X3))),
% 137.82/17.85 inference(cnf_transformation,[status(thm)],[f181])).
% 137.82/17.85 fof(f538,plain,(
% 137.82/17.85 (![Xa,Xb]: (Xa=Xb|(![Xp]: s_col(Xa,Xb,midpoint(Xp,reflect(Xa,Xb,Xp))))))&(![Xa,Xb,Xp]: ((Xa=Xb|Xp=reflect(Xa,Xb,Xp))|perp(Xa,Xb,Xp,reflect(Xa,Xb,Xp))))),
% 137.82/17.85 inference(miniscoping,[status(thm)],[f184])).
% 137.82/17.85 fof(f539,plain,(
% 137.82/17.85 ![X0,X1,X2]: (X0=X1|s_col(X0,X1,midpoint(X2,reflect(X0,X1,X2))))),
% 137.82/17.85 inference(cnf_transformation,[status(thm)],[f538])).
% 137.82/17.85 fof(f544,plain,(
% 137.82/17.85 ![X0,X1,X2,X3]: (X0=X1|~reflect(X0,X1,X2)=X3|reflect(X0,X1,X3)=X2)),
% 137.82/17.85 inference(cnf_transformation,[status(thm)],[f186])).
% 137.82/17.85 fof(f550,plain,(
% 137.82/17.85 ![X0,X1,X2]: (X0=X1|~reflect(X0,X1,X2)=X2|s_col(X0,X1,X2))),
% 137.82/17.85 inference(cnf_transformation,[status(thm)],[f190])).
% 137.82/17.85 fof(f551,plain,(
% 137.82/17.85 ![X0,X1,X2]: (X0=X1|~s_col(X0,X1,X2)|reflect(X0,X1,X2)=X2)),
% 137.82/17.85 inference(cnf_transformation,[status(thm)],[f191])).
% 137.82/17.85 fof(f564,plain,(
% 137.82/17.85 (?[Xa,Xb,Xp,Xp1]: (((~Xa=Xb&reflect(Xa,Xb,Xp)=Xp1)&~s_col(Xa,Xb,Xp))&~opposite(Xp,Xa,Xb,Xp1)))),
% 137.82/17.85 inference(pre_NNF_transformation,[status(thm)],[f199])).
% 137.82/17.85 fof(f565,plain,(
% 137.82/17.85 (((~sK0_skl=sK1_skl&reflect(sK0_skl,sK1_skl,sK2_skl)=sK3_skl)&~s_col(sK0_skl,sK1_skl,sK2_skl))&~opposite(sK2_skl,sK0_skl,sK1_skl,sK3_skl))),
% 137.82/17.85 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl]),skolemize(Xa,sK0_skl),skolemize(Xb,sK1_skl),skolemize(Xp,sK2_skl),skolemize(Xp1,sK3_skl)],[f564])).
% 137.82/17.85 fof(f566,plain,(
% 137.82/17.85 ~sK0_skl=sK1_skl),
% 137.82/17.85 inference(cnf_transformation,[status(thm)],[f565])).
% 137.82/17.85 fof(f567,plain,(
% 137.82/17.85 reflect(sK0_skl,sK1_skl,sK2_skl)=sK3_skl),
% 137.82/17.85 inference(cnf_transformation,[status(thm)],[f565])).
% 137.82/17.85 fof(f568,plain,(
% 137.82/17.85 ~s_col(sK0_skl,sK1_skl,sK2_skl)),
% 137.82/17.85 inference(cnf_transformation,[status(thm)],[f565])).
% 137.82/17.85 fof(f569,plain,(
% 137.82/17.85 ~opposite(sK2_skl,sK0_skl,sK1_skl,sK3_skl)),
% 137.82/17.85 inference(cnf_transformation,[status(thm)],[f565])).
% 137.82/17.85 fof(f613,plain,(
% 137.82/17.85 ((![Xa,Xm,Xb]: (~s_m(Xa,Xm,Xb)|s_t(Xa,Xm,Xb)))&(![Xa,Xm,Xb]: (~s_m(Xa,Xm,Xb)|s_e(Xm,Xa,Xm,Xb))))&(![Xa,Xm,Xb]: ((~s_t(Xa,Xm,Xb)|~s_e(Xm,Xa,Xm,Xb))|s_m(Xa,Xm,Xb)))),
% 137.82/17.85 inference(miniscoping,[status(thm)],[f208])).
% 137.82/17.85 fof(f614,plain,(
% 137.82/17.85 ![X0,X1,X2]: (~s_m(X0,X1,X2)|s_t(X0,X1,X2))),
% 137.82/17.85 inference(cnf_transformation,[status(thm)],[f613])).
% 137.82/17.85 fof(f640,plain,(
% 137.82/17.85 ((((![Xp,Xq,Xa,Xb]: ((![Xt]: ((((Xp=Xq|s_col(Xp,Xq,Xa))|s_col(Xp,Xq,Xb))|~s_t(Xa,Xt,Xb))|~s_col(Xp,Xq,Xt)))|opposite(Xa,Xp,Xq,Xb)))&(![Xp,Xq,Xa]: ((![Xb]: ~opposite(Xa,Xp,Xq,Xb))|~s_col(Xp,Xq,Xa))))&(![Xp,Xq,Xb]: ((![Xa]: ~opposite(Xa,Xp,Xq,Xb))|~s_col(Xp,Xq,Xb))))&(![Xp,Xq,Xa,Xb]: (~opposite(Xa,Xp,Xq,Xb)|s_t(Xa,il(Xa,Xb,Xp,Xq),Xb))))&(![Xp,Xq,Xa,Xb]: (~opposite(Xa,Xp,Xq,Xb)|s_col(Xp,Xq,il(Xa,Xb,Xp,Xq))))),
% 137.82/17.85 inference(miniscoping,[status(thm)],[f213])).
% 137.82/17.85 fof(f641,plain,(
% 137.82/17.85 ![X0,X1,X2,X3,X4]: (X0=X1|s_col(X0,X1,X2)|s_col(X0,X1,X3)|~s_t(X2,X4,X3)|~s_col(X0,X1,X4)|opposite(X2,X0,X1,X3))),
% 137.82/17.85 inference(cnf_transformation,[status(thm)],[f640])).
% 137.82/17.85 fof(f646,plain,(
% 137.82/17.85 (((((((((((![Xa,Xb,Xp,Xq]: (~samesideline(Xa,Xb,Xp,Xq)|s_col(Xp,Xq,ss1(Xa,Xb,Xp,Xq))))&(![Xa,Xb,Xp,Xq]: (~samesideline(Xa,Xb,Xp,Xq)|s_col(Xp,Xq,ss2(Xa,Xb,Xp,Xq)))))&(![Xa,Xb,Xp,Xq]: (~samesideline(Xa,Xb,Xp,Xq)|s_t(Xa,ss1(Xa,Xb,Xp,Xq),ss3(Xa,Xb,Xp,Xq)))))&(![Xa,Xb,Xp,Xq]: (~samesideline(Xa,Xb,Xp,Xq)|s_t(Xb,ss2(Xa,Xb,Xp,Xq),ss3(Xa,Xb,Xp,Xq)))))&(![Xa,Xb,Xp,Xq]: (~samesideline(Xa,Xb,Xp,Xq)|~Xa=ss1(Xa,Xb,Xp,Xq))))&(![Xa,Xb,Xp,Xq]: (~samesideline(Xa,Xb,Xp,Xq)|~Xb=ss2(Xa,Xb,Xp,Xq))))&(![Xa,Xb,Xp,Xq]: (~samesideline(Xa,Xb,Xp,Xq)|~ss3(Xa,Xb,Xp,Xq)=ss1(Xa,Xb,Xp,Xq))))&(![Xa,Xb,Xp,Xq]: (~samesideline(Xa,Xb,Xp,Xq)|~ss3(Xa,Xb,Xp,Xq)=ss2(Xa,Xb,Xp,Xq))))&(![Xp,Xq]: ((![Xa,Xb]: ~samesideline(Xa,Xb,Xp,Xq))|~Xp=Xq)))&(![Xa,Xp,Xq]: ((![Xb]: ~samesideline(Xa,Xb,Xp,Xq))|~s_col(Xp,Xq,Xa))))&(![Xb,Xp,Xq]: ((![Xa]: ~samesideline(Xa,Xb,Xp,Xq))|~s_col(Xp,Xq,Xb))))&(![Xa,Xb,Xp,Xq]: ((((![Xv]: ((![Xu]: ((![Xc]: ((((((~s_t(Xa,Xu,Xc)|~s_t(Xb,Xv,Xc))|~s_col(Xp,Xq,Xu))|~s_col(Xp,Xq,Xv))|Xp=Xq)|Xc=Xu)|Xc=Xv))|Xa=Xu))|Xb=Xv))|s_col(Xp,Xq,Xa))|s_col(Xp,Xq,Xb))|samesideline(Xa,Xb,Xp,Xq)))),
% 137.82/17.85 inference(miniscoping,[status(thm)],[f214])).
% 137.82/17.85 fof(f656,plain,(
% 137.82/17.85 ![X0,X1,X2,X3]: (~samesideline(X0,X1,X2,X3)|~s_col(X2,X3,X0))),
% 137.82/17.85 inference(cnf_transformation,[status(thm)],[f646])).
% 137.82/17.85 fof(f657,plain,(
% 137.82/17.85 ![X0,X1,X2,X3]: (~samesideline(X0,X1,X2,X3)|~s_col(X2,X3,X1))),
% 137.82/17.85 inference(cnf_transformation,[status(thm)],[f646])).
% 137.82/17.85 fof(f692,plain,(
% 137.82/17.85 ![X0,X1,X2]: (X0=X1|reflect(X0,X1,reflect(X0,X1,X2))=X2)),
% 137.82/17.85 inference(destructive_equality_resolution,[status(thm)],[f544])).
% 137.82/17.85 fof(f700,plain,(
% 137.82/17.85 ~s_col(sK2_skl,sK0_skl,sK1_skl)),
% 137.82/17.85 inference(resolution,[status(thm)],[f281,f568])).
% 137.82/17.85 fof(f701,plain,(
% 137.82/17.85 ~s_col(sK1_skl,sK2_skl,sK0_skl)),
% 137.82/17.85 inference(resolution,[status(thm)],[f700,f281])).
% 137.82/17.85 fof(f708,plain,(
% 137.82/17.85 ~s_col(sK0_skl,sK2_skl,sK1_skl)),
% 137.82/17.85 inference(resolution,[status(thm)],[f701,f283])).
% 137.82/17.85 fof(f723,plain,(
% 137.82/17.85 ![X0,X1]: (s_col(X0,X1,X1))),
% 137.82/17.85 inference(resolution,[status(thm)],[f284,f287])).
% 137.82/17.85 fof(f878,plain,(
% 137.82/17.85 ![X0,X1]: (s_t(X0,midpoint(X0,X1),X1))),
% 137.82/17.85 inference(resolution,[status(thm)],[f614,f470])).
% 137.82/17.85 fof(f911,definition,(
% 137.82/17.85 sQ8_spl <=> (sK0_skl=sK1_skl)),
% 137.82/17.85 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 137.82/17.85 fof(f912,plain,(
% 137.82/17.85 sK0_skl=sK1_skl|~sQ8_spl),
% 137.82/17.85 inference(component_clause,[status(thm)],[f911])).
% 137.82/17.85 fof(f926,plain,(
% 137.82/17.85 $false|~sQ8_spl),
% 137.82/17.85 inference(forward_subsumption_resolution,[status(thm)],[f912,f566])).
% 137.82/17.85 fof(f927,plain,(
% 137.82/17.85 ~sQ8_spl),
% 137.82/17.85 inference(contradiction_clause,[status(thm)],[f926])).
% 137.82/17.85 fof(f1007,definition,(
% 137.82/17.85 sQ15_spl <=> (sK2_skl=reflect(sK0_skl,sK1_skl,sK2_skl))),
% 137.82/17.85 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 137.82/17.85 fof(f1009,plain,(
% 137.82/17.85 ~sK2_skl=reflect(sK0_skl,sK1_skl,sK2_skl)|sQ15_spl),
% 137.82/17.85 inference(component_clause,[status(thm)],[f1007])).
% 137.82/17.85 fof(f1209,definition,(
% 137.82/17.85 sQ24_spl <=> (s_col(sK0_skl,sK1_skl,sK2_skl))),
% 137.82/17.85 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 137.82/17.85 fof(f1210,plain,(
% 137.82/17.85 s_col(sK0_skl,sK1_skl,sK2_skl)|~sQ24_spl),
% 137.82/17.85 inference(component_clause,[status(thm)],[f1209])).
% 137.82/17.85 fof(f1218,plain,(
% 137.82/17.85 $false|~sQ24_spl),
% 137.82/17.85 inference(forward_subsumption_resolution,[status(thm)],[f1210,f568])).
% 137.82/17.85 fof(f1219,plain,(
% 137.82/17.85 ~sQ24_spl),
% 137.82/17.85 inference(contradiction_clause,[status(thm)],[f1218])).
% 137.82/17.85 fof(f1251,plain,(
% 137.82/17.85 sK0_skl=sK1_skl|s_col(sK0_skl,sK1_skl,sK2_skl)|s_col(sK0_skl,sK1_skl,sK3_skl)|samesideline(sK2_skl,sK3_skl,sK0_skl,sK1_skl)),
% 137.82/17.85 inference(resolution,[status(thm)],[f569,f533])).
% 137.82/17.85 fof(f1252,definition,(
% 137.82/17.85 sQ28_spl <=> (s_col(sK0_skl,sK1_skl,sK3_skl))),
% 137.82/17.85 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 137.82/17.85 fof(f1253,plain,(
% 137.82/17.85 s_col(sK0_skl,sK1_skl,sK3_skl)|~sQ28_spl),
% 137.82/17.85 inference(component_clause,[status(thm)],[f1252])).
% 137.82/17.85 fof(f1255,definition,(
% 137.82/17.85 sQ29_spl <=> (samesideline(sK2_skl,sK3_skl,sK0_skl,sK1_skl))),
% 137.82/17.85 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 137.82/17.85 fof(f1256,plain,(
% 137.82/17.85 samesideline(sK2_skl,sK3_skl,sK0_skl,sK1_skl)|~sQ29_spl),
% 137.82/17.85 inference(component_clause,[status(thm)],[f1255])).
% 137.82/17.85 fof(f1258,plain,(
% 137.82/17.85 sQ8_spl|sQ24_spl|sQ28_spl|sQ29_spl),
% 137.82/17.85 inference(split_clause,[status(thm)],[f1251,f911,f1209,f1252,f1255])).
% 137.82/17.85 fof(f1259,plain,(
% 137.82/17.85 sK0_skl=sK1_skl|reflect(sK0_skl,sK1_skl,sK3_skl)=sK3_skl|~sQ28_spl),
% 137.82/17.85 inference(resolution,[status(thm)],[f1253,f551])).
% 137.82/17.85 fof(f1267,definition,(
% 137.82/17.85 sQ30_spl <=> (reflect(sK0_skl,sK1_skl,sK3_skl)=sK3_skl)),
% 137.82/17.85 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 137.82/17.85 fof(f1268,plain,(
% 137.82/17.85 reflect(sK0_skl,sK1_skl,sK3_skl)=sK3_skl|~sQ30_spl),
% 137.82/17.85 inference(component_clause,[status(thm)],[f1267])).
% 137.82/17.85 fof(f1270,plain,(
% 137.82/17.85 sQ8_spl|sQ30_spl|~sQ28_spl),
% 137.82/17.85 inference(split_clause,[status(thm)],[f1259,f911,f1267,f1252])).
% 137.82/17.85 fof(f1441,plain,(
% 137.82/17.85 sK0_skl=sK1_skl|~reflect(sK0_skl,sK1_skl,sK2_skl)=sK2_skl),
% 137.82/17.85 inference(resolution,[status(thm)],[f550,f568])).
% 137.82/17.85 fof(f1454,definition,(
% 137.82/17.85 sQ57_spl <=> (sK1_skl=sK2_skl)),
% 137.82/17.85 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 137.82/17.85 fof(f1455,plain,(
% 137.82/17.85 sK1_skl=sK2_skl|~sQ57_spl),
% 137.82/17.85 inference(component_clause,[status(thm)],[f1454])).
% 137.82/17.85 fof(f1465,definition,(
% 137.82/17.85 sQ60_spl <=> (sK2_skl=sK0_skl)),
% 137.82/17.85 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 137.82/17.85 fof(f1466,plain,(
% 137.82/17.85 sK2_skl=sK0_skl|~sQ60_spl),
% 137.82/17.85 inference(component_clause,[status(thm)],[f1465])).
% 137.82/17.85 fof(f1476,plain,(
% 137.82/17.85 sQ8_spl|~sQ15_spl),
% 137.82/17.85 inference(split_clause,[status(thm)],[f1441,f911,f1007])).
% 137.82/17.85 fof(f1480,plain,(
% 137.82/17.85 ~s_col(sK0_skl,sK0_skl,sK1_skl)|~sQ60_spl),
% 137.82/17.85 inference(backward_demodulation,[status(thm)],[f1466,f708])).
% 137.82/17.85 fof(f1488,plain,(
% 137.82/17.85 $false|~sQ60_spl),
% 137.82/17.85 inference(forward_subsumption_resolution,[status(thm)],[f1480,f286])).
% 137.82/17.85 fof(f1489,plain,(
% 137.82/17.85 ~sQ60_spl),
% 137.82/17.85 inference(contradiction_clause,[status(thm)],[f1488])).
% 137.82/17.85 fof(f1538,definition,(
% 137.82/17.85 sQ64_spl <=> (samesideline(sK1_skl,sK3_skl,sK0_skl,sK1_skl))),
% 137.82/17.85 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 137.82/17.85 fof(f1539,plain,(
% 137.82/17.85 samesideline(sK1_skl,sK3_skl,sK0_skl,sK1_skl)|~sQ64_spl),
% 137.82/17.85 inference(component_clause,[status(thm)],[f1538])).
% 137.82/17.85 fof(f1542,plain,(
% 137.82/17.85 ~s_col(sK0_skl,sK1_skl,sK1_skl)|~sQ57_spl),
% 137.82/17.85 inference(forward_demodulation,[status(thm)],[f1455,f708])).
% 137.82/17.85 fof(f1543,plain,(
% 137.82/17.85 $false|~sQ57_spl),
% 137.82/17.85 inference(forward_subsumption_resolution,[status(thm)],[f1542,f723])).
% 137.82/17.85 fof(f1544,plain,(
% 137.82/17.85 ~sQ57_spl),
% 137.82/17.85 inference(contradiction_clause,[status(thm)],[f1543])).
% 137.82/17.85 fof(f1551,plain,(
% 137.82/17.85 ![X0,X1,X2,X3,X4]: (X0=X1|s_col(X0,X1,X2)|s_col(X0,X1,X3)|~s_t(X2,X4,X3)|~s_col(X0,X1,X4)|~samesideline(X2,X3,X0,X1))),
% 137.82/17.85 inference(resolution,[status(thm)],[f641,f516])).
% 137.82/17.85 fof(f1558,plain,(
% 137.82/17.85 ![X0,X1,X2,X3,X4]: (X0=X1|s_col(X0,X1,X2)|~s_t(X2,X3,X4)|~s_col(X0,X1,X3)|~samesideline(X2,X4,X0,X1))),
% 137.82/17.85 inference(forward_subsumption_resolution,[status(thm)],[f1551,f657])).
% 137.82/17.85 fof(f1620,plain,(
% 137.82/17.85 sK0_skl=sK1_skl|reflect(sK0_skl,sK1_skl,sK3_skl)=sK2_skl),
% 137.82/17.85 inference(paramodulation,[status(thm)],[f567,f692])).
% 137.82/17.85 fof(f1631,definition,(
% 137.82/17.85 sQ66_spl <=> (reflect(sK0_skl,sK1_skl,sK3_skl)=sK2_skl)),
% 137.82/17.85 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 137.82/17.85 fof(f1632,plain,(
% 137.82/17.85 reflect(sK0_skl,sK1_skl,sK3_skl)=sK2_skl|~sQ66_spl),
% 137.82/17.85 inference(component_clause,[status(thm)],[f1631])).
% 137.82/17.85 fof(f1634,plain,(
% 137.82/17.85 sQ8_spl|sQ66_spl),
% 137.82/17.85 inference(split_clause,[status(thm)],[f1620,f911,f1631])).
% 137.82/17.85 fof(f1666,definition,(
% 137.82/17.85 ![X0]: (sQ67_spl <=> (~s_t(sK2_skl,X0,sK3_skl)|~s_col(sK0_skl,sK1_skl,X0)))),
% 137.82/17.85 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 137.82/17.85 fof(f1667,plain,(
% 137.82/17.85 ![X0]: (~s_t(sK2_skl,X0,sK3_skl)|~s_col(sK0_skl,sK1_skl,X0)|~sQ67_spl)),
% 137.82/17.85 inference(component_clause,[status(thm)],[f1666])).
% 137.82/17.85 fof(f2976,plain,(
% 137.82/17.85 ~sK2_skl=sK3_skl|sQ15_spl),
% 137.82/17.85 inference(forward_demodulation,[status(thm)],[f567,f1009])).
% 137.82/17.85 fof(f3460,plain,(
% 137.82/17.85 ~s_col(sK0_skl,sK1_skl,sK1_skl)|~sQ64_spl),
% 137.82/17.85 inference(resolution,[status(thm)],[f1539,f656])).
% 137.82/17.85 fof(f3461,plain,(
% 137.82/17.85 $false|~sQ64_spl),
% 137.82/17.85 inference(forward_subsumption_resolution,[status(thm)],[f3460,f723])).
% 137.82/17.85 fof(f3462,plain,(
% 137.82/17.85 ~sQ64_spl),
% 137.82/17.85 inference(contradiction_clause,[status(thm)],[f3461])).
% 137.82/17.85 fof(f3678,definition,(
% 137.82/17.85 sQ148_spl <=> (sK3_skl=sK3_skl)),
% 137.82/17.85 introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition])).
% 137.82/17.85 fof(f3680,plain,(
% 137.82/17.85 ~sK3_skl=sK3_skl|sQ148_spl),
% 137.82/17.85 inference(component_clause,[status(thm)],[f3678])).
% 137.82/17.85 fof(f3696,plain,(
% 137.82/17.85 $false|sQ148_spl),
% 137.82/17.85 inference(trivial_equality_resolution,[status(thm)],[f3680])).
% 137.82/17.85 fof(f3697,plain,(
% 137.82/17.85 sQ148_spl),
% 137.82/17.85 inference(contradiction_clause,[status(thm)],[f3696])).
% 137.82/17.85 fof(f3699,plain,(
% 137.82/17.85 sK2_skl=sK3_skl|~sQ66_spl|~sQ30_spl),
% 137.82/17.85 inference(forward_demodulation,[status(thm)],[f1632,f1268])).
% 137.82/17.85 fof(f3700,plain,(
% 137.82/17.85 $false|sQ15_spl|~sQ66_spl|~sQ30_spl),
% 137.82/17.85 inference(forward_subsumption_resolution,[status(thm)],[f3699,f2976])).
% 137.82/17.85 fof(f3701,plain,(
% 137.82/17.85 sQ15_spl|~sQ66_spl|~sQ30_spl),
% 137.82/17.85 inference(contradiction_clause,[status(thm)],[f3700])).
% 137.82/17.85 fof(f6196,plain,(
% 137.82/17.85 ![X0,X1,X2,X3,X4]: (X0=X1|~s_t(X2,X3,X4)|~s_col(X0,X1,X3)|~samesideline(X2,X4,X0,X1))),
% 137.82/17.85 inference(forward_subsumption_resolution,[status(thm)],[f1558,f656])).
% 137.82/17.85 fof(f6197,plain,(
% 137.82/17.85 ![X0]: (sK0_skl=sK1_skl|~s_t(sK2_skl,X0,sK3_skl)|~s_col(sK0_skl,sK1_skl,X0)|~sQ29_spl)),
% 137.82/17.85 inference(resolution,[status(thm)],[f6196,f1256])).
% 137.82/17.85 fof(f6198,plain,(
% 137.82/17.85 sQ8_spl|sQ67_spl|~sQ29_spl),
% 137.82/17.85 inference(split_clause,[status(thm)],[f6197,f911,f1666,f1255])).
% 137.82/17.85 fof(f6318,definition,(
% 137.82/17.85 sQ203_spl <=> (s_col(sK2_skl,sK2_skl,sK3_skl))),
% 137.82/17.85 introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition])).
% 137.82/17.85 fof(f6320,plain,(
% 137.82/17.85 ~s_col(sK2_skl,sK2_skl,sK3_skl)|sQ203_spl),
% 137.82/17.85 inference(component_clause,[status(thm)],[f6318])).
% 137.82/17.85 fof(f6322,plain,(
% 137.82/17.85 $false|sQ203_spl),
% 137.82/17.85 inference(forward_subsumption_resolution,[status(thm)],[f6320,f286])).
% 137.82/17.85 fof(f6323,plain,(
% 137.82/17.85 sQ203_spl),
% 137.82/17.85 inference(contradiction_clause,[status(thm)],[f6322])).
% 137.82/17.85 fof(f6329,definition,(
% 137.82/17.85 sQ205_spl <=> (s_col(sK3_skl,sK2_skl,sK2_skl))),
% 137.82/17.85 introduced(definition,[new_symbols(definition,[sQ205_spl])],[split_symbol_definition])).
% 137.82/17.85 fof(f6331,plain,(
% 137.82/17.85 ~s_col(sK3_skl,sK2_skl,sK2_skl)|sQ205_spl),
% 137.82/17.85 inference(component_clause,[status(thm)],[f6329])).
% 137.82/17.85 fof(f6333,plain,(
% 137.82/17.85 $false|sQ205_spl),
% 137.82/17.85 inference(forward_subsumption_resolution,[status(thm)],[f6331,f723])).
% 137.82/17.85 fof(f6334,plain,(
% 137.82/17.85 sQ205_spl),
% 137.82/17.85 inference(contradiction_clause,[status(thm)],[f6333])).
% 137.82/17.85 fof(f7512,definition,(
% 137.82/17.85 sQ223_spl <=> (s_col(sK0_skl,sK1_skl,sK0_skl))),
% 137.82/17.85 introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition])).
% 137.82/17.85 fof(f7514,plain,(
% 137.82/17.85 ~s_col(sK0_skl,sK1_skl,sK0_skl)|sQ223_spl),
% 137.82/17.85 inference(component_clause,[status(thm)],[f7512])).
% 137.82/17.85 fof(f7516,plain,(
% 137.82/17.85 $false|sQ223_spl),
% 137.82/17.85 inference(forward_subsumption_resolution,[status(thm)],[f7514,f287])).
% 137.82/17.85 fof(f7517,plain,(
% 137.82/17.85 sQ223_spl),
% 137.82/17.85 inference(contradiction_clause,[status(thm)],[f7516])).
% 137.82/17.85 fof(f8586,definition,(
% 137.82/17.85 sQ267_spl <=> (s_col(sK0_skl,sK2_skl,sK2_skl))),
% 137.82/17.85 introduced(definition,[new_symbols(definition,[sQ267_spl])],[split_symbol_definition])).
% 137.82/17.85 fof(f8588,plain,(
% 137.82/17.85 ~s_col(sK0_skl,sK2_skl,sK2_skl)|sQ267_spl),
% 137.82/17.85 inference(component_clause,[status(thm)],[f8586])).
% 137.82/17.85 fof(f8636,definition,(
% 137.82/17.85 sQ279_spl <=> (s_col(sK3_skl,sK0_skl,sK0_skl))),
% 137.82/17.85 introduced(definition,[new_symbols(definition,[sQ279_spl])],[split_symbol_definition])).
% 137.82/17.85 fof(f8638,plain,(
% 137.82/17.85 ~s_col(sK3_skl,sK0_skl,sK0_skl)|sQ279_spl),
% 137.82/17.85 inference(component_clause,[status(thm)],[f8636])).
% 137.82/17.85 fof(f8682,definition,(
% 137.82/17.85 sQ289_spl <=> (s_col(sK0_skl,sK3_skl,sK0_skl))),
% 137.82/17.85 introduced(definition,[new_symbols(definition,[sQ289_spl])],[split_symbol_definition])).
% 137.82/17.85 fof(f8684,plain,(
% 137.82/17.85 ~s_col(sK0_skl,sK3_skl,sK0_skl)|sQ289_spl),
% 137.82/17.85 inference(component_clause,[status(thm)],[f8682])).
% 137.82/17.85 fof(f9012,plain,(
% 137.82/17.85 $false|sQ289_spl),
% 137.82/17.85 inference(forward_subsumption_resolution,[status(thm)],[f8684,f287])).
% 137.82/17.85 fof(f9013,plain,(
% 137.82/17.85 sQ289_spl),
% 137.82/17.85 inference(contradiction_clause,[status(thm)],[f9012])).
% 137.82/17.85 fof(f9014,plain,(
% 137.82/17.85 $false|sQ279_spl),
% 137.82/17.85 inference(forward_subsumption_resolution,[status(thm)],[f8638,f723])).
% 137.82/17.85 fof(f9015,plain,(
% 137.82/17.85 sQ279_spl),
% 137.82/17.85 inference(contradiction_clause,[status(thm)],[f9014])).
% 137.82/17.85 fof(f9017,plain,(
% 137.82/17.85 $false|sQ267_spl),
% 137.82/17.85 inference(forward_subsumption_resolution,[status(thm)],[f8588,f723])).
% 137.82/17.85 fof(f9018,plain,(
% 137.82/17.85 sQ267_spl),
% 137.82/17.85 inference(contradiction_clause,[status(thm)],[f9017])).
% 137.82/17.85 fof(f9316,definition,(
% 137.82/17.85 sQ388_spl <=> (s_col(sK1_skl,sK2_skl,sK2_skl))),
% 137.82/17.85 introduced(definition,[new_symbols(definition,[sQ388_spl])],[split_symbol_definition])).
% 137.82/17.85 fof(f9318,plain,(
% 137.82/17.85 ~s_col(sK1_skl,sK2_skl,sK2_skl)|sQ388_spl),
% 137.82/17.85 inference(component_clause,[status(thm)],[f9316])).
% 137.82/17.85 fof(f9363,definition,(
% 137.82/17.85 sQ399_spl <=> (s_col(sK3_skl,sK1_skl,sK1_skl))),
% 137.82/17.85 introduced(definition,[new_symbols(definition,[sQ399_spl])],[split_symbol_definition])).
% 137.82/17.87 fof(f9365,plain,(
% 137.82/17.87 ~s_col(sK3_skl,sK1_skl,sK1_skl)|sQ399_spl),
% 137.82/17.87 inference(component_clause,[status(thm)],[f9363])).
% 137.82/17.87 fof(f9400,definition,(
% 137.82/17.87 sQ406_spl <=> (s_col(sK1_skl,sK3_skl,sK1_skl))),
% 137.82/17.87 introduced(definition,[new_symbols(definition,[sQ406_spl])],[split_symbol_definition])).
% 137.82/17.87 fof(f9402,plain,(
% 137.82/17.87 ~s_col(sK1_skl,sK3_skl,sK1_skl)|sQ406_spl),
% 137.82/17.87 inference(component_clause,[status(thm)],[f9400])).
% 137.82/17.87 fof(f9727,plain,(
% 137.82/17.87 $false|sQ406_spl),
% 137.82/17.87 inference(forward_subsumption_resolution,[status(thm)],[f9402,f287])).
% 137.82/17.87 fof(f9728,plain,(
% 137.82/17.87 sQ406_spl),
% 137.82/17.87 inference(contradiction_clause,[status(thm)],[f9727])).
% 137.82/17.87 fof(f9729,plain,(
% 137.82/17.87 $false|sQ399_spl),
% 137.82/17.87 inference(forward_subsumption_resolution,[status(thm)],[f9365,f723])).
% 137.82/17.87 fof(f9730,plain,(
% 137.82/17.87 sQ399_spl),
% 137.82/17.87 inference(contradiction_clause,[status(thm)],[f9729])).
% 137.82/17.87 fof(f9732,plain,(
% 137.82/17.87 $false|sQ388_spl),
% 137.82/17.87 inference(forward_subsumption_resolution,[status(thm)],[f9318,f723])).
% 137.82/17.87 fof(f9733,plain,(
% 137.82/17.87 sQ388_spl),
% 137.82/17.87 inference(contradiction_clause,[status(thm)],[f9732])).
% 137.82/17.87 fof(f10223,plain,(
% 137.82/17.87 sK0_skl=sK1_skl|s_col(sK0_skl,sK1_skl,midpoint(sK2_skl,sK3_skl))),
% 137.82/17.87 inference(paramodulation,[status(thm)],[f567,f539])).
% 137.82/17.87 fof(f10325,definition,(
% 137.82/17.87 sQ493_spl <=> (s_col(sK0_skl,sK1_skl,midpoint(sK2_skl,sK3_skl)))),
% 137.82/17.87 introduced(definition,[new_symbols(definition,[sQ493_spl])],[split_symbol_definition])).
% 137.82/17.87 fof(f10326,plain,(
% 137.82/17.87 s_col(sK0_skl,sK1_skl,midpoint(sK2_skl,sK3_skl))|~sQ493_spl),
% 137.82/17.87 inference(component_clause,[status(thm)],[f10325])).
% 137.82/17.87 fof(f10328,plain,(
% 137.82/17.87 sQ8_spl|sQ493_spl),
% 137.82/17.87 inference(split_clause,[status(thm)],[f10223,f911,f10325])).
% 137.82/17.87 fof(f10339,plain,(
% 137.82/17.87 ~s_t(sK2_skl,midpoint(sK2_skl,sK3_skl),sK3_skl)|~sQ493_spl|~sQ67_spl),
% 137.82/17.87 inference(resolution,[status(thm)],[f10326,f1667])).
% 137.82/17.87 fof(f10498,plain,(
% 137.82/17.87 $false|~sQ493_spl|~sQ67_spl),
% 137.82/17.87 inference(forward_subsumption_resolution,[status(thm)],[f10339,f878])).
% 137.82/17.87 fof(f10499,plain,(
% 137.82/17.87 ~sQ493_spl|~sQ67_spl),
% 137.82/17.87 inference(contradiction_clause,[status(thm)],[f10498])).
% 137.82/17.87 fof(f10500,plain,(
% 137.82/17.87 $false),
% 137.82/17.87 inference(sat_refutation,[status(thm)],[f927,f1219,f1258,f1270,f1476,f1489,f1544,f1634,f3462,f3697,f3701,f6198,f6323,f6334,f7517,f9013,f9015,f9018,f9728,f9730,f9733,f10328,f10499])).
% 137.82/17.87 % SZS output end CNFRefutation for theBenchmark.p
% 39.74/17.92 % Elapsed time: 17.531369 seconds
% 39.74/17.92 % CPU time: 138.618561 seconds
% 39.74/17.92 % Total memory used: 305.392 MB
% 39.74/17.92 % Net memory used: 272.191 MB
%------------------------------------------------------------------------------