%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEV609+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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 02:33:47 PM UTC 2026
% Result : Theorem 193.16s 25.18s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV609+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n020.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 07:30:19 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.46/0.74 % Drodi V4.1.1
% 193.16/25.18 % Refutation found
% 193.16/25.18 % SZS status Theorem for theBenchmark: Theorem is valid
% 193.16/25.18 % SZS output start CNFRefutation for theBenchmark
% 193.16/25.18 fof(f1859,axiom,(
% 193.16/25.18 (! [V0__U] :( cLambda_2eRedexes_2eredexes___24t(V0__U)=> (! [V1__V] :( cLambda_2eRedexes_2eredexes___24t(V1__V)=> (! [V2__W] :( cLambda_2eRedexes_2eredexes___24t(V2__W)=> ( cLambda_2eRedexes_2esub___24a2(V1__V,V0__U)=> (! [V4__UV] :( cLambda_2eRedexes_2eredexes___24t(V4__UV)=> ( cLambda_2eResiduals_2eresiduals___24a3(V0__U,V1__V,V4__UV)=> (! [V6__WV] :( cLambda_2eRedexes_2eredexes___24t(V6__WV)=> ( cLambda_2eResiduals_2eresiduals___24a3(V2__W,V1__V,V6__WV)=> (! [V8__WU] :( cLambda_2eRedexes_2eredexes___24t(V8__WU)=> ( cLambda_2eResiduals_2eresiduals___24a3(V2__W,V0__U,V8__WU)=> cLambda_2eResiduals_2eresiduals___24a3(V6__WV,V4__UV,V8__WU) ) ) )) ) )) ) )) ) )) )) )),
% 193.16/25.18 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 193.16/25.18 fof(f1873,axiom,(
% 193.16/25.18 (! [V0__U] :( cLambda_2eRedexes_2eredexes___24t(V0__U)=> (! [V1__V] :( cLambda_2eRedexes_2eredexes___24t(V1__V)=> ( cLambda_2eRedexes_2ecomp___24a2(V0__U,V1__V)=> cLambda_2eRedexes_2ecomp___24a2(V1__V,V0__U) ) ) )) )),
% 193.16/25.19 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 193.16/25.19 fof(f1874,axiom,(
% 193.16/25.19 (! [V0__U] :( cLambda_2eRedexes_2eredexes___24t(V0__U)=> (! [V1__V] :( cLambda_2eRedexes_2eredexes___24t(V1__V)=> ( cLambda_2eRedexes_2ecomp___24a2(V0__U,V1__V)=> (! [V3__W] :( cLambda_2eRedexes_2eredexes___24t(V3__W)=> ( cLambda_2eRedexes_2ecomp___24a2(V1__V,V3__W)=> cLambda_2eRedexes_2ecomp___24a2(V0__U,V3__W) ) ) )) ) )) )),
% 193.16/25.19 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 193.16/25.19 fof(f1892,axiom,(
% 193.16/25.19 (! [V0__U] :( cLambda_2eRedexes_2eredexes___24t(V0__U)=> (! [V1__V] :( cLambda_2eRedexes_2eredexes___24t(V1__V)=> (! [V2__W] :( cLambda_2eRedexes_2eredexes___24t(V2__W)=> ( cLambda_2eResiduals_2eresiduals___24a3(V0__U,V1__V,V2__W)=> cLambda_2eRedexes_2ecomp___24a2(V0__U,V1__V) ) ) )) )) )),
% 193.16/25.19 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 193.16/25.19 fof(f1893,axiom,(
% 193.16/25.19 (! [V0__U] :( cLambda_2eRedexes_2eredexes___24t(V0__U)=> (! [V1__V] :( cLambda_2eRedexes_2eredexes___24t(V1__V)=> (! [V2__W] :( cLambda_2eRedexes_2eredexes___24t(V2__W)=> ( cLambda_2eResiduals_2eresiduals___24a3(V0__U,V1__V,V2__W)=> (! [V4__W_27] :( cLambda_2eRedexes_2eredexes___24t(V4__W_27)=> ( cLambda_2eResiduals_2eresiduals___24a3(V0__U,V1__V,V4__W_27)=> V4__W_27 = V2__W ) ) )) ) )) )) )),
% 193.16/25.19 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 193.16/25.19 fof(f1895,axiom,(
% 193.16/25.19 (! [V0__U] :( cLambda_2eRedexes_2eredexes___24t(V0__U)=> (! [V1__V] :( cLambda_2eRedexes_2eredexes___24t(V1__V)=> ( cLambda_2eRedexes_2ecomp___24a2(V0__U,V1__V)=> ( cLambda_2eRedexes_2eregular___24a1(V1__V)=> (? [V4__W] :( cLambda_2eRedexes_2eredexes___24t(V4__W)& cLambda_2eResiduals_2eresiduals___24a3(V0__U,V1__V,V4__W) ) )) ) ) )) )),
% 193.16/25.19 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 193.16/25.19 fof(f2901,conjecture,(
% 193.16/25.19 (! [V0__U] :( cLambda_2eRedexes_2eredexes___24t(V0__U)=> (! [V1__V] :( cLambda_2eRedexes_2eredexes___24t(V1__V)=> (! [V2__W] :( cLambda_2eRedexes_2eredexes___24t(V2__W)=> ( cLambda_2eRedexes_2esub___24a2(V1__V,V0__U)=> ( cLambda_2eRedexes_2eregular___24a1(V0__U)=> (! [V5__UV] :( cLambda_2eRedexes_2eredexes___24t(V5__UV)=> ( cLambda_2eResiduals_2eresiduals___24a3(V0__U,V1__V,V5__UV)=> (! [V7__WV] :( cLambda_2eRedexes_2eredexes___24t(V7__WV)=> ( cLambda_2eResiduals_2eresiduals___24a3(V2__W,V1__V,V7__WV)=> (! [V9__WU] :( cLambda_2eRedexes_2eredexes___24t(V9__WU)=> ( cLambda_2eResiduals_2eresiduals___24a3(V7__WV,V5__UV,V9__WU)=> cLambda_2eResiduals_2eresiduals___24a3(V2__W,V0__U,V9__WU) ) ) )) ) )) ) )) ) ) )) )) )),
% 193.16/25.19 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 193.16/25.19 fof(f2902,negated_conjecture,(
% 193.16/25.19 ~((! [V0__U] :( cLambda_2eRedexes_2eredexes___24t(V0__U)=> (! [V1__V] :( cLambda_2eRedexes_2eredexes___24t(V1__V)=> (! [V2__W] :( cLambda_2eRedexes_2eredexes___24t(V2__W)=> ( cLambda_2eRedexes_2esub___24a2(V1__V,V0__U)=> ( cLambda_2eRedexes_2eregular___24a1(V0__U)=> (! [V5__UV] :( cLambda_2eRedexes_2eredexes___24t(V5__UV)=> ( cLambda_2eResiduals_2eresiduals___24a3(V0__U,V1__V,V5__UV)=> (! [V7__WV] :( cLambda_2eRedexes_2eredexes___24t(V7__WV)=> ( cLambda_2eResiduals_2eresiduals___24a3(V2__W,V1__V,V7__WV)=> (! [V9__WU] :( cLambda_2eRedexes_2eredexes___24t(V9__WU)=> ( cLambda_2eResiduals_2eresiduals___24a3(V7__WV,V5__UV,V9__WU)=> cLambda_2eResiduals_2eresiduals___24a3(V2__W,V0__U,V9__WU) ) ) )) ) )) ) )) ) ) )) )) ))),
% 193.16/25.19 inference(negated_conjecture,[status(cth)],[f2901])).
% 193.16/25.19 fof(f10387,plain,(
% 193.16/25.19 ![V0__U]: (~cLambda_2eRedexes_2eredexes___24t(V0__U)|(![V1__V]: (~cLambda_2eRedexes_2eredexes___24t(V1__V)|(![V2__W]: (~cLambda_2eRedexes_2eredexes___24t(V2__W)|(~cLambda_2eRedexes_2esub___24a2(V1__V,V0__U)|(![V4__UV]: (~cLambda_2eRedexes_2eredexes___24t(V4__UV)|(~cLambda_2eResiduals_2eresiduals___24a3(V0__U,V1__V,V4__UV)|(![V6__WV]: (~cLambda_2eRedexes_2eredexes___24t(V6__WV)|(~cLambda_2eResiduals_2eresiduals___24a3(V2__W,V1__V,V6__WV)|(![V8__WU]: (~cLambda_2eRedexes_2eredexes___24t(V8__WU)|(~cLambda_2eResiduals_2eresiduals___24a3(V2__W,V0__U,V8__WU)|cLambda_2eResiduals_2eresiduals___24a3(V6__WV,V4__UV,V8__WU))))))))))))))))),
% 193.16/25.19 inference(pre_NNF_transformation,[status(thm)],[f1859])).
% 193.16/25.19 fof(f10388,plain,(
% 193.16/25.19 ![X0,X1,X2,X3,X4,X5]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eRedexes_2eredexes___24t(X2)|~cLambda_2eRedexes_2esub___24a2(X1,X0)|~cLambda_2eRedexes_2eredexes___24t(X3)|~cLambda_2eResiduals_2eresiduals___24a3(X0,X1,X3)|~cLambda_2eRedexes_2eredexes___24t(X4)|~cLambda_2eResiduals_2eresiduals___24a3(X2,X1,X4)|~cLambda_2eRedexes_2eredexes___24t(X5)|~cLambda_2eResiduals_2eresiduals___24a3(X2,X0,X5)|cLambda_2eResiduals_2eresiduals___24a3(X4,X3,X5))),
% 193.16/25.19 inference(cnf_transformation,[status(thm)],[f10387])).
% 193.16/25.19 fof(f10430,plain,(
% 193.16/25.19 ![V0__U]: (~cLambda_2eRedexes_2eredexes___24t(V0__U)|(![V1__V]: (~cLambda_2eRedexes_2eredexes___24t(V1__V)|(~cLambda_2eRedexes_2ecomp___24a2(V0__U,V1__V)|cLambda_2eRedexes_2ecomp___24a2(V1__V,V0__U)))))),
% 193.16/25.19 inference(pre_NNF_transformation,[status(thm)],[f1873])).
% 193.16/25.19 fof(f10431,plain,(
% 193.16/25.19 ![X0,X1]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eRedexes_2ecomp___24a2(X0,X1)|cLambda_2eRedexes_2ecomp___24a2(X1,X0))),
% 193.16/25.19 inference(cnf_transformation,[status(thm)],[f10430])).
% 193.16/25.19 fof(f10432,plain,(
% 193.16/25.19 ![V0__U]: (~cLambda_2eRedexes_2eredexes___24t(V0__U)|(![V1__V]: (~cLambda_2eRedexes_2eredexes___24t(V1__V)|(~cLambda_2eRedexes_2ecomp___24a2(V0__U,V1__V)|(![V3__W]: (~cLambda_2eRedexes_2eredexes___24t(V3__W)|(~cLambda_2eRedexes_2ecomp___24a2(V1__V,V3__W)|cLambda_2eRedexes_2ecomp___24a2(V0__U,V3__W))))))))),
% 193.16/25.19 inference(pre_NNF_transformation,[status(thm)],[f1874])).
% 193.16/25.19 fof(f10433,plain,(
% 193.16/25.19 ![X0,X1,X2]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eRedexes_2ecomp___24a2(X0,X1)|~cLambda_2eRedexes_2eredexes___24t(X2)|~cLambda_2eRedexes_2ecomp___24a2(X1,X2)|cLambda_2eRedexes_2ecomp___24a2(X0,X2))),
% 193.16/25.19 inference(cnf_transformation,[status(thm)],[f10432])).
% 193.16/25.19 fof(f10510,plain,(
% 193.16/25.19 ![V0__U]: (~cLambda_2eRedexes_2eredexes___24t(V0__U)|(![V1__V]: (~cLambda_2eRedexes_2eredexes___24t(V1__V)|(![V2__W]: (~cLambda_2eRedexes_2eredexes___24t(V2__W)|(~cLambda_2eResiduals_2eresiduals___24a3(V0__U,V1__V,V2__W)|cLambda_2eRedexes_2ecomp___24a2(V0__U,V1__V)))))))),
% 193.16/25.19 inference(pre_NNF_transformation,[status(thm)],[f1892])).
% 193.16/25.19 fof(f10511,plain,(
% 193.16/25.19 ![X0,X1,X2]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eRedexes_2eredexes___24t(X2)|~cLambda_2eResiduals_2eresiduals___24a3(X0,X1,X2)|cLambda_2eRedexes_2ecomp___24a2(X0,X1))),
% 193.16/25.19 inference(cnf_transformation,[status(thm)],[f10510])).
% 193.16/25.19 fof(f10512,plain,(
% 193.16/25.19 ![V0__U]: (~cLambda_2eRedexes_2eredexes___24t(V0__U)|(![V1__V]: (~cLambda_2eRedexes_2eredexes___24t(V1__V)|(![V2__W]: (~cLambda_2eRedexes_2eredexes___24t(V2__W)|(~cLambda_2eResiduals_2eresiduals___24a3(V0__U,V1__V,V2__W)|(![V4__W_27]: (~cLambda_2eRedexes_2eredexes___24t(V4__W_27)|(~cLambda_2eResiduals_2eresiduals___24a3(V0__U,V1__V,V4__W_27)|V4__W_27=V2__W)))))))))),
% 193.16/25.19 inference(pre_NNF_transformation,[status(thm)],[f1893])).
% 193.16/25.19 fof(f10513,plain,(
% 193.16/25.19 ![X0,X1,X2,X3]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eRedexes_2eredexes___24t(X2)|~cLambda_2eResiduals_2eresiduals___24a3(X0,X1,X2)|~cLambda_2eRedexes_2eredexes___24t(X3)|~cLambda_2eResiduals_2eresiduals___24a3(X0,X1,X3)|X3=X2)),
% 193.16/25.19 inference(cnf_transformation,[status(thm)],[f10512])).
% 193.16/25.19 fof(f10532,plain,(
% 193.16/25.19 ![V0__U]: (~cLambda_2eRedexes_2eredexes___24t(V0__U)|(![V1__V]: (~cLambda_2eRedexes_2eredexes___24t(V1__V)|(~cLambda_2eRedexes_2ecomp___24a2(V0__U,V1__V)|(~cLambda_2eRedexes_2eregular___24a1(V1__V)|(?[V4__W]: (cLambda_2eRedexes_2eredexes___24t(V4__W)&cLambda_2eResiduals_2eresiduals___24a3(V0__U,V1__V,V4__W))))))))),
% 193.16/25.19 inference(pre_NNF_transformation,[status(thm)],[f1895])).
% 193.16/25.19 fof(f10533,plain,(
% 193.16/25.19 ![V0__U]: (~cLambda_2eRedexes_2eredexes___24t(V0__U)|(![V1__V]: (~cLambda_2eRedexes_2eredexes___24t(V1__V)|(~cLambda_2eRedexes_2ecomp___24a2(V0__U,V1__V)|(~cLambda_2eRedexes_2eregular___24a1(V1__V)|(cLambda_2eRedexes_2eredexes___24t(sK1334_skl(V1__V,V0__U))&cLambda_2eResiduals_2eresiduals___24a3(V0__U,V1__V,sK1334_skl(V1__V,V0__U))))))))),
% 193.16/25.19 inference(skolemize,[status(esa),new_symbols(skolem,[sK1334_skl]),skolemize(V4__W,sK1334_skl(V1__V,V0__U))],[f10532])).
% 193.16/25.19 fof(f10534,plain,(
% 193.16/25.19 ![X0,X1]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eRedexes_2ecomp___24a2(X0,X1)|~cLambda_2eRedexes_2eregular___24a1(X1)|cLambda_2eRedexes_2eredexes___24t(sK1334_skl(X1,X0)))),
% 193.16/25.19 inference(cnf_transformation,[status(thm)],[f10533])).
% 193.16/25.19 fof(f10535,plain,(
% 193.16/25.19 ![X0,X1]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eRedexes_2ecomp___24a2(X0,X1)|~cLambda_2eRedexes_2eregular___24a1(X1)|cLambda_2eResiduals_2eresiduals___24a3(X0,X1,sK1334_skl(X1,X0)))),
% 193.16/25.19 inference(cnf_transformation,[status(thm)],[f10533])).
% 193.16/25.19 fof(f13317,plain,(
% 193.16/25.19 (?[V0__U]: (cLambda_2eRedexes_2eredexes___24t(V0__U)&(?[V1__V]: (cLambda_2eRedexes_2eredexes___24t(V1__V)&(?[V2__W]: (cLambda_2eRedexes_2eredexes___24t(V2__W)&(cLambda_2eRedexes_2esub___24a2(V1__V,V0__U)&(cLambda_2eRedexes_2eregular___24a1(V0__U)&(?[V5__UV]: (cLambda_2eRedexes_2eredexes___24t(V5__UV)&(cLambda_2eResiduals_2eresiduals___24a3(V0__U,V1__V,V5__UV)&(?[V7__WV]: (cLambda_2eRedexes_2eredexes___24t(V7__WV)&(cLambda_2eResiduals_2eresiduals___24a3(V2__W,V1__V,V7__WV)&(?[V9__WU]: (cLambda_2eRedexes_2eredexes___24t(V9__WU)&(cLambda_2eResiduals_2eresiduals___24a3(V7__WV,V5__UV,V9__WU)&~cLambda_2eResiduals_2eresiduals___24a3(V2__W,V0__U,V9__WU))))))))))))))))))),
% 193.16/25.19 inference(pre_NNF_transformation,[status(thm)],[f2902])).
% 193.16/25.19 fof(f13318,plain,(
% 193.16/25.19 (cLambda_2eRedexes_2eredexes___24t(sK1335_skl)&(cLambda_2eRedexes_2eredexes___24t(sK1336_skl)&(cLambda_2eRedexes_2eredexes___24t(sK1337_skl)&(cLambda_2eRedexes_2esub___24a2(sK1336_skl,sK1335_skl)&(cLambda_2eRedexes_2eregular___24a1(sK1335_skl)&(cLambda_2eRedexes_2eredexes___24t(sK1338_skl)&(cLambda_2eResiduals_2eresiduals___24a3(sK1335_skl,sK1336_skl,sK1338_skl)&(cLambda_2eRedexes_2eredexes___24t(sK1339_skl)&(cLambda_2eResiduals_2eresiduals___24a3(sK1337_skl,sK1336_skl,sK1339_skl)&(cLambda_2eRedexes_2eredexes___24t(sK1340_skl)&(cLambda_2eResiduals_2eresiduals___24a3(sK1339_skl,sK1338_skl,sK1340_skl)&~cLambda_2eResiduals_2eresiduals___24a3(sK1337_skl,sK1335_skl,sK1340_skl))))))))))))),
% 193.16/25.19 inference(skolemize,[status(esa),new_symbols(skolem,[sK1335_skl,sK1336_skl,sK1337_skl,sK1338_skl,sK1339_skl,sK1340_skl]),skolemize(V0__U,sK1335_skl),skolemize(V1__V,sK1336_skl),skolemize(V2__W,sK1337_skl),skolemize(V5__UV,sK1338_skl),skolemize(V7__WV,sK1339_skl),skolemize(V9__WU,sK1340_skl)],[f13317])).
% 193.16/25.19 fof(f13319,plain,(
% 193.16/25.19 cLambda_2eRedexes_2eredexes___24t(sK1335_skl)),
% 193.16/25.19 inference(cnf_transformation,[status(thm)],[f13318])).
% 193.16/25.19 fof(f13320,plain,(
% 193.16/25.19 cLambda_2eRedexes_2eredexes___24t(sK1336_skl)),
% 193.16/25.19 inference(cnf_transformation,[status(thm)],[f13318])).
% 193.16/25.19 fof(f13321,plain,(
% 193.16/25.19 cLambda_2eRedexes_2eredexes___24t(sK1337_skl)),
% 193.16/25.19 inference(cnf_transformation,[status(thm)],[f13318])).
% 193.16/25.19 fof(f13322,plain,(
% 193.16/25.19 cLambda_2eRedexes_2esub___24a2(sK1336_skl,sK1335_skl)),
% 193.16/25.19 inference(cnf_transformation,[status(thm)],[f13318])).
% 193.16/25.19 fof(f13323,plain,(
% 193.16/25.19 cLambda_2eRedexes_2eregular___24a1(sK1335_skl)),
% 193.16/25.19 inference(cnf_transformation,[status(thm)],[f13318])).
% 193.16/25.19 fof(f13324,plain,(
% 193.16/25.19 cLambda_2eRedexes_2eredexes___24t(sK1338_skl)),
% 193.16/25.19 inference(cnf_transformation,[status(thm)],[f13318])).
% 193.16/25.19 fof(f13325,plain,(
% 193.16/25.19 cLambda_2eResiduals_2eresiduals___24a3(sK1335_skl,sK1336_skl,sK1338_skl)),
% 193.16/25.19 inference(cnf_transformation,[status(thm)],[f13318])).
% 193.16/25.19 fof(f13326,plain,(
% 193.16/25.19 cLambda_2eRedexes_2eredexes___24t(sK1339_skl)),
% 193.16/25.19 inference(cnf_transformation,[status(thm)],[f13318])).
% 193.16/25.19 fof(f13327,plain,(
% 193.16/25.19 cLambda_2eResiduals_2eresiduals___24a3(sK1337_skl,sK1336_skl,sK1339_skl)),
% 193.16/25.19 inference(cnf_transformation,[status(thm)],[f13318])).
% 193.16/25.19 fof(f13328,plain,(
% 193.16/25.19 cLambda_2eRedexes_2eredexes___24t(sK1340_skl)),
% 193.16/25.19 inference(cnf_transformation,[status(thm)],[f13318])).
% 193.16/25.19 fof(f13329,plain,(
% 193.16/25.19 cLambda_2eResiduals_2eresiduals___24a3(sK1339_skl,sK1338_skl,sK1340_skl)),
% 193.16/25.19 inference(cnf_transformation,[status(thm)],[f13318])).
% 193.16/25.19 fof(f13330,plain,(
% 193.16/25.19 ~cLambda_2eResiduals_2eresiduals___24a3(sK1337_skl,sK1335_skl,sK1340_skl)),
% 193.16/25.19 inference(cnf_transformation,[status(thm)],[f13318])).
% 193.16/25.19 fof(f17773,plain,(
% 193.16/25.19 ![X0,X1,X2,X3]: (~cLambda_2eRedexes_2eredexes___24t(sK1335_skl)|~cLambda_2eRedexes_2eredexes___24t(sK1336_skl)|~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eResiduals_2eresiduals___24a3(sK1335_skl,sK1336_skl,X1)|~cLambda_2eRedexes_2eredexes___24t(X2)|~cLambda_2eResiduals_2eresiduals___24a3(X0,sK1336_skl,X2)|~cLambda_2eRedexes_2eredexes___24t(X3)|~cLambda_2eResiduals_2eresiduals___24a3(X0,sK1335_skl,X3)|cLambda_2eResiduals_2eresiduals___24a3(X2,X1,X3))),
% 193.16/25.19 inference(resolution,[status(thm)],[f10388,f13322])).
% 193.16/25.19 fof(f17774,plain,(
% 193.16/25.19 ![X0,X1,X2,X3]: (~cLambda_2eRedexes_2eredexes___24t(sK1336_skl)|~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eResiduals_2eresiduals___24a3(sK1335_skl,sK1336_skl,X1)|~cLambda_2eRedexes_2eredexes___24t(X2)|~cLambda_2eResiduals_2eresiduals___24a3(X0,sK1336_skl,X2)|~cLambda_2eRedexes_2eredexes___24t(X3)|~cLambda_2eResiduals_2eresiduals___24a3(X0,sK1335_skl,X3)|cLambda_2eResiduals_2eresiduals___24a3(X2,X1,X3))),
% 193.16/25.19 inference(forward_subsumption_resolution,[status(thm)],[f17773,f13319])).
% 193.16/25.19 fof(f17779,plain,(
% 193.16/25.19 ![X0]: (~cLambda_2eRedexes_2eredexes___24t(sK1339_skl)|~cLambda_2eRedexes_2eredexes___24t(sK1338_skl)|~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eResiduals_2eresiduals___24a3(sK1339_skl,sK1338_skl,X0)|~cLambda_2eRedexes_2eredexes___24t(sK1340_skl)|sK1340_skl=X0)),
% 193.16/25.19 inference(resolution,[status(thm)],[f13329,f10513])).
% 193.16/25.19 fof(f17782,plain,(
% 193.16/25.19 ![X0]: (~cLambda_2eRedexes_2eredexes___24t(sK1338_skl)|~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eResiduals_2eresiduals___24a3(sK1339_skl,sK1338_skl,X0)|~cLambda_2eRedexes_2eredexes___24t(sK1340_skl)|sK1340_skl=X0)),
% 193.16/25.19 inference(forward_subsumption_resolution,[status(thm)],[f17779,f13326])).
% 193.16/25.19 fof(f17785,plain,(
% 193.16/25.19 ![X0]: (~cLambda_2eRedexes_2eredexes___24t(sK1338_skl)|~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eResiduals_2eresiduals___24a3(sK1339_skl,sK1338_skl,X0)|sK1340_skl=X0)),
% 193.16/25.19 inference(resolution,[status(thm)],[f17782,f13328])).
% 193.16/25.19 fof(f17786,plain,(
% 193.16/25.19 ![X0]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eResiduals_2eresiduals___24a3(sK1339_skl,sK1338_skl,X0)|sK1340_skl=X0)),
% 193.16/25.19 inference(forward_subsumption_resolution,[status(thm)],[f17785,f13324])).
% 193.16/25.19 fof(f18194,plain,(
% 193.16/25.19 ~cLambda_2eRedexes_2eredexes___24t(sK1337_skl)|~cLambda_2eRedexes_2eredexes___24t(sK1336_skl)|~cLambda_2eRedexes_2eredexes___24t(sK1339_skl)|cLambda_2eRedexes_2ecomp___24a2(sK1337_skl,sK1336_skl)),
% 193.16/25.19 inference(resolution,[status(thm)],[f10511,f13327])).
% 193.16/25.19 fof(f18195,plain,(
% 193.16/25.19 ~cLambda_2eRedexes_2eredexes___24t(sK1335_skl)|~cLambda_2eRedexes_2eredexes___24t(sK1336_skl)|~cLambda_2eRedexes_2eredexes___24t(sK1338_skl)|cLambda_2eRedexes_2ecomp___24a2(sK1335_skl,sK1336_skl)),
% 193.16/25.19 inference(resolution,[status(thm)],[f10511,f13325])).
% 193.16/25.19 fof(f18198,plain,(
% 193.16/25.19 ~cLambda_2eRedexes_2eredexes___24t(sK1336_skl)|~cLambda_2eRedexes_2eredexes___24t(sK1339_skl)|cLambda_2eRedexes_2ecomp___24a2(sK1337_skl,sK1336_skl)),
% 193.16/25.19 inference(forward_subsumption_resolution,[status(thm)],[f18194,f13321])).
% 193.16/25.19 fof(f18199,plain,(
% 193.16/25.19 ~cLambda_2eRedexes_2eredexes___24t(sK1336_skl)|~cLambda_2eRedexes_2eredexes___24t(sK1338_skl)|cLambda_2eRedexes_2ecomp___24a2(sK1335_skl,sK1336_skl)),
% 193.16/25.19 inference(forward_subsumption_resolution,[status(thm)],[f18195,f13319])).
% 193.16/25.19 fof(f18207,plain,(
% 193.16/25.19 ~cLambda_2eRedexes_2eredexes___24t(sK1336_skl)|cLambda_2eRedexes_2ecomp___24a2(sK1337_skl,sK1336_skl)),
% 193.16/25.19 inference(resolution,[status(thm)],[f18198,f13326])).
% 193.16/25.19 fof(f18208,plain,(
% 193.16/25.19 cLambda_2eRedexes_2ecomp___24a2(sK1337_skl,sK1336_skl)),
% 193.16/25.19 inference(forward_subsumption_resolution,[status(thm)],[f18207,f13320])).
% 193.16/25.19 fof(f18213,plain,(
% 193.16/25.19 ~cLambda_2eRedexes_2eredexes___24t(sK1336_skl)|cLambda_2eRedexes_2ecomp___24a2(sK1335_skl,sK1336_skl)),
% 193.16/25.19 inference(resolution,[status(thm)],[f18199,f13324])).
% 193.16/25.19 fof(f18214,plain,(
% 193.16/25.19 cLambda_2eRedexes_2ecomp___24a2(sK1335_skl,sK1336_skl)),
% 193.16/25.19 inference(forward_subsumption_resolution,[status(thm)],[f18213,f13320])).
% 193.16/25.19 fof(f18663,plain,(
% 193.16/25.19 ![X0,X1,X2]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eRedexes_2ecomp___24a2(X0,X1)|~cLambda_2eRedexes_2eredexes___24t(X2)|cLambda_2eRedexes_2ecomp___24a2(X0,X2)|~cLambda_2eRedexes_2eredexes___24t(X2)|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eRedexes_2ecomp___24a2(X2,X1))),
% 193.16/25.19 inference(resolution,[status(thm)],[f10433,f10431])).
% 193.16/25.19 fof(f18669,plain,(
% 193.16/25.19 ![X0,X1,X2]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eRedexes_2ecomp___24a2(X0,X1)|~cLambda_2eRedexes_2eredexes___24t(X2)|cLambda_2eRedexes_2ecomp___24a2(X0,X2)|~cLambda_2eRedexes_2ecomp___24a2(X2,X1))),
% 193.16/25.19 inference(duplicate_literals_removal,[status(thm)],[f18663])).
% 193.16/25.19 fof(f18677,plain,(
% 193.16/25.19 ![X0,X1]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eRedexes_2eregular___24a1(X1)|cLambda_2eResiduals_2eresiduals___24a3(X0,X1,sK1334_skl(X1,X0))|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2ecomp___24a2(X1,X0))),
% 193.16/25.19 inference(resolution,[status(thm)],[f10535,f10431])).
% 193.16/25.19 fof(f18683,plain,(
% 193.16/25.19 ![X0,X1]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eRedexes_2eregular___24a1(X1)|cLambda_2eResiduals_2eresiduals___24a3(X0,X1,sK1334_skl(X1,X0))|~cLambda_2eRedexes_2ecomp___24a2(X1,X0))),
% 193.16/25.19 inference(duplicate_literals_removal,[status(thm)],[f18677])).
% 193.16/25.19 fof(f18705,plain,(
% 193.16/25.19 ![X0]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2eredexes___24t(sK1336_skl)|~cLambda_2eRedexes_2ecomp___24a2(X0,sK1336_skl)|~cLambda_2eRedexes_2eredexes___24t(sK1335_skl)|cLambda_2eRedexes_2ecomp___24a2(X0,sK1335_skl))),
% 193.16/25.19 inference(resolution,[status(thm)],[f18669,f18214])).
% 193.16/25.19 fof(f18706,plain,(
% 193.16/25.19 ![X0]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2eredexes___24t(sK1336_skl)|~cLambda_2eRedexes_2ecomp___24a2(X0,sK1336_skl)|~cLambda_2eRedexes_2eredexes___24t(sK1337_skl)|cLambda_2eRedexes_2ecomp___24a2(X0,sK1337_skl))),
% 193.16/25.19 inference(resolution,[status(thm)],[f18669,f18208])).
% 193.16/25.19 fof(f18711,plain,(
% 193.16/25.19 ![X0]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2ecomp___24a2(X0,sK1336_skl)|~cLambda_2eRedexes_2eredexes___24t(sK1335_skl)|cLambda_2eRedexes_2ecomp___24a2(X0,sK1335_skl))),
% 193.16/25.19 inference(forward_subsumption_resolution,[status(thm)],[f18705,f13320])).
% 193.16/25.19 fof(f18712,plain,(
% 193.16/25.19 ![X0]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2ecomp___24a2(X0,sK1336_skl)|~cLambda_2eRedexes_2eredexes___24t(sK1337_skl)|cLambda_2eRedexes_2ecomp___24a2(X0,sK1337_skl))),
% 193.16/25.19 inference(forward_subsumption_resolution,[status(thm)],[f18706,f13320])).
% 193.16/25.19 fof(f18722,plain,(
% 193.16/25.19 ![X0]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2ecomp___24a2(X0,sK1336_skl)|cLambda_2eRedexes_2ecomp___24a2(X0,sK1335_skl))),
% 193.16/25.19 inference(resolution,[status(thm)],[f18711,f13319])).
% 193.16/25.19 fof(f18723,plain,(
% 193.16/25.19 ![X0]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2ecomp___24a2(X0,sK1336_skl)|cLambda_2eRedexes_2ecomp___24a2(X0,sK1337_skl))),
% 193.16/25.19 inference(resolution,[status(thm)],[f18712,f13321])).
% 193.16/25.19 fof(f18743,plain,(
% 193.16/25.19 ~cLambda_2eRedexes_2eredexes___24t(sK1337_skl)|cLambda_2eRedexes_2ecomp___24a2(sK1337_skl,sK1335_skl)),
% 193.16/25.19 inference(resolution,[status(thm)],[f18722,f18208])).
% 193.16/25.19 fof(f18746,plain,(
% 193.16/25.19 cLambda_2eRedexes_2ecomp___24a2(sK1337_skl,sK1335_skl)),
% 193.16/25.19 inference(forward_subsumption_resolution,[status(thm)],[f18743,f13321])).
% 193.16/25.19 fof(f18753,plain,(
% 193.16/25.19 ~cLambda_2eRedexes_2eredexes___24t(sK1337_skl)|~cLambda_2eRedexes_2eredexes___24t(sK1335_skl)|~cLambda_2eRedexes_2eregular___24a1(sK1335_skl)|cLambda_2eResiduals_2eresiduals___24a3(sK1337_skl,sK1335_skl,sK1334_skl(sK1335_skl,sK1337_skl))),
% 193.16/25.19 inference(resolution,[status(thm)],[f18746,f10535])).
% 193.16/25.19 fof(f18764,plain,(
% 193.16/25.19 ~cLambda_2eRedexes_2eredexes___24t(sK1337_skl)|~cLambda_2eRedexes_2eredexes___24t(sK1335_skl)|~cLambda_2eRedexes_2eregular___24a1(sK1335_skl)|cLambda_2eRedexes_2eredexes___24t(sK1334_skl(sK1335_skl,sK1337_skl))),
% 193.16/25.19 inference(resolution,[status(thm)],[f18746,f10534])).
% 193.16/25.19 fof(f18768,plain,(
% 193.16/25.19 ~cLambda_2eRedexes_2eredexes___24t(sK1335_skl)|~cLambda_2eRedexes_2eregular___24a1(sK1335_skl)|cLambda_2eResiduals_2eresiduals___24a3(sK1337_skl,sK1335_skl,sK1334_skl(sK1335_skl,sK1337_skl))),
% 193.16/25.19 inference(forward_subsumption_resolution,[status(thm)],[f18753,f13321])).
% 193.16/25.19 fof(f18779,plain,(
% 193.16/25.19 ~cLambda_2eRedexes_2eredexes___24t(sK1335_skl)|~cLambda_2eRedexes_2eregular___24a1(sK1335_skl)|cLambda_2eRedexes_2eredexes___24t(sK1334_skl(sK1335_skl,sK1337_skl))),
% 193.16/25.19 inference(forward_subsumption_resolution,[status(thm)],[f18764,f13321])).
% 193.16/25.19 fof(f18819,plain,(
% 193.16/25.19 ~cLambda_2eRedexes_2eredexes___24t(sK1335_skl)|cLambda_2eRedexes_2ecomp___24a2(sK1335_skl,sK1337_skl)),
% 193.16/25.19 inference(resolution,[status(thm)],[f18723,f18214])).
% 193.16/25.19 fof(f18823,plain,(
% 193.16/25.19 cLambda_2eRedexes_2ecomp___24a2(sK1335_skl,sK1337_skl)),
% 193.16/25.19 inference(forward_subsumption_resolution,[status(thm)],[f18819,f13319])).
% 193.16/25.19 fof(f18868,plain,(
% 193.16/25.19 ![X0,X1,X2]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2eredexes___24t(sK1335_skl)|~cLambda_2eRedexes_2eregular___24a1(sK1335_skl)|~cLambda_2eRedexes_2ecomp___24a2(sK1335_skl,X0)|~cLambda_2eRedexes_2eredexes___24t(sK1336_skl)|~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eResiduals_2eresiduals___24a3(sK1335_skl,sK1336_skl,X1)|~cLambda_2eRedexes_2eredexes___24t(X2)|~cLambda_2eResiduals_2eresiduals___24a3(X0,sK1336_skl,X2)|~cLambda_2eRedexes_2eredexes___24t(sK1334_skl(sK1335_skl,X0))|cLambda_2eResiduals_2eresiduals___24a3(X2,X1,sK1334_skl(sK1335_skl,X0)))),
% 193.16/25.19 inference(resolution,[status(thm)],[f18683,f17774])).
% 193.16/25.19 fof(f18877,plain,(
% 193.16/25.19 ![X0,X1,X2]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2eredexes___24t(sK1335_skl)|~cLambda_2eRedexes_2eregular___24a1(sK1335_skl)|~cLambda_2eRedexes_2ecomp___24a2(sK1335_skl,X0)|~cLambda_2eRedexes_2eredexes___24t(sK1336_skl)|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eResiduals_2eresiduals___24a3(sK1335_skl,sK1336_skl,X1)|~cLambda_2eRedexes_2eredexes___24t(X2)|~cLambda_2eResiduals_2eresiduals___24a3(X0,sK1336_skl,X2)|~cLambda_2eRedexes_2eredexes___24t(sK1334_skl(sK1335_skl,X0))|cLambda_2eResiduals_2eresiduals___24a3(X2,X1,sK1334_skl(sK1335_skl,X0)))),
% 193.16/25.19 inference(duplicate_literals_removal,[status(thm)],[f18868])).
% 193.16/25.19 fof(f18878,plain,(
% 193.16/25.19 ![X0,X1,X2]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2eregular___24a1(sK1335_skl)|~cLambda_2eRedexes_2ecomp___24a2(sK1335_skl,X0)|~cLambda_2eRedexes_2eredexes___24t(sK1336_skl)|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eResiduals_2eresiduals___24a3(sK1335_skl,sK1336_skl,X1)|~cLambda_2eRedexes_2eredexes___24t(X2)|~cLambda_2eResiduals_2eresiduals___24a3(X0,sK1336_skl,X2)|~cLambda_2eRedexes_2eredexes___24t(sK1334_skl(sK1335_skl,X0))|cLambda_2eResiduals_2eresiduals___24a3(X2,X1,sK1334_skl(sK1335_skl,X0)))),
% 193.16/25.19 inference(forward_subsumption_resolution,[status(thm)],[f18877,f13319])).
% 193.16/25.19 fof(f19103,plain,(
% 193.16/25.19 ![X0,X1,X2]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2ecomp___24a2(sK1335_skl,X0)|~cLambda_2eRedexes_2eredexes___24t(sK1336_skl)|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eResiduals_2eresiduals___24a3(sK1335_skl,sK1336_skl,X1)|~cLambda_2eRedexes_2eredexes___24t(X2)|~cLambda_2eResiduals_2eresiduals___24a3(X0,sK1336_skl,X2)|~cLambda_2eRedexes_2eredexes___24t(sK1334_skl(sK1335_skl,X0))|cLambda_2eResiduals_2eresiduals___24a3(X2,X1,sK1334_skl(sK1335_skl,X0)))),
% 193.16/25.19 inference(resolution,[status(thm)],[f18878,f13323])).
% 193.16/25.19 fof(f19104,plain,(
% 193.16/25.19 ![X0,X1,X2]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2ecomp___24a2(sK1335_skl,X0)|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eResiduals_2eresiduals___24a3(sK1335_skl,sK1336_skl,X1)|~cLambda_2eRedexes_2eredexes___24t(X2)|~cLambda_2eResiduals_2eresiduals___24a3(X0,sK1336_skl,X2)|~cLambda_2eRedexes_2eredexes___24t(sK1334_skl(sK1335_skl,X0))|cLambda_2eResiduals_2eresiduals___24a3(X2,X1,sK1334_skl(sK1335_skl,X0)))),
% 193.16/25.19 inference(forward_subsumption_resolution,[status(thm)],[f19103,f13320])).
% 193.16/25.19 fof(f19256,plain,(
% 193.16/25.19 ~cLambda_2eRedexes_2eredexes___24t(sK1335_skl)|cLambda_2eRedexes_2eredexes___24t(sK1334_skl(sK1335_skl,sK1337_skl))),
% 193.16/25.19 inference(resolution,[status(thm)],[f18779,f13323])).
% 193.16/25.19 fof(f19257,plain,(
% 193.16/25.19 cLambda_2eRedexes_2eredexes___24t(sK1334_skl(sK1335_skl,sK1337_skl))),
% 193.16/25.19 inference(forward_subsumption_resolution,[status(thm)],[f19256,f13319])).
% 193.16/25.19 fof(f19970,plain,(
% 193.16/25.19 ![X0,X1]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2ecomp___24a2(sK1335_skl,X0)|~cLambda_2eRedexes_2eredexes___24t(sK1338_skl)|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eResiduals_2eresiduals___24a3(X0,sK1336_skl,X1)|~cLambda_2eRedexes_2eredexes___24t(sK1334_skl(sK1335_skl,X0))|cLambda_2eResiduals_2eresiduals___24a3(X1,sK1338_skl,sK1334_skl(sK1335_skl,X0)))),
% 193.16/25.19 inference(resolution,[status(thm)],[f19104,f13325])).
% 193.16/25.19 fof(f19972,plain,(
% 193.16/25.19 ![X0,X1]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2ecomp___24a2(sK1335_skl,X0)|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eResiduals_2eresiduals___24a3(X0,sK1336_skl,X1)|~cLambda_2eRedexes_2eredexes___24t(sK1334_skl(sK1335_skl,X0))|cLambda_2eResiduals_2eresiduals___24a3(X1,sK1338_skl,sK1334_skl(sK1335_skl,X0)))),
% 193.16/25.19 inference(forward_subsumption_resolution,[status(thm)],[f19970,f13324])).
% 193.16/25.19 fof(f19974,plain,(
% 193.16/25.19 ![X0]: (~cLambda_2eRedexes_2eredexes___24t(sK1337_skl)|~cLambda_2eRedexes_2ecomp___24a2(sK1335_skl,sK1337_skl)|~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eResiduals_2eresiduals___24a3(sK1337_skl,sK1336_skl,X0)|cLambda_2eResiduals_2eresiduals___24a3(X0,sK1338_skl,sK1334_skl(sK1335_skl,sK1337_skl)))),
% 193.16/25.19 inference(resolution,[status(thm)],[f19972,f19257])).
% 193.16/25.19 fof(f19977,plain,(
% 193.16/25.19 ![X0]: (~cLambda_2eRedexes_2ecomp___24a2(sK1335_skl,sK1337_skl)|~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eResiduals_2eresiduals___24a3(sK1337_skl,sK1336_skl,X0)|cLambda_2eResiduals_2eresiduals___24a3(X0,sK1338_skl,sK1334_skl(sK1335_skl,sK1337_skl)))),
% 193.16/25.19 inference(forward_subsumption_resolution,[status(thm)],[f19974,f13321])).
% 193.16/25.19 fof(f19981,plain,(
% 193.16/25.19 ![X0]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eResiduals_2eresiduals___24a3(sK1337_skl,sK1336_skl,X0)|cLambda_2eResiduals_2eresiduals___24a3(X0,sK1338_skl,sK1334_skl(sK1335_skl,sK1337_skl)))),
% 193.16/25.19 inference(resolution,[status(thm)],[f19977,f18823])).
% 193.16/25.19 fof(f19983,plain,(
% 193.16/25.19 ~cLambda_2eRedexes_2eredexes___24t(sK1339_skl)|cLambda_2eResiduals_2eresiduals___24a3(sK1339_skl,sK1338_skl,sK1334_skl(sK1335_skl,sK1337_skl))),
% 193.16/25.19 inference(resolution,[status(thm)],[f19981,f13327])).
% 193.16/25.19 fof(f19985,plain,(
% 193.16/25.19 cLambda_2eResiduals_2eresiduals___24a3(sK1339_skl,sK1338_skl,sK1334_skl(sK1335_skl,sK1337_skl))),
% 193.16/25.19 inference(forward_subsumption_resolution,[status(thm)],[f19983,f13326])).
% 193.16/25.19 fof(f20002,plain,(
% 193.16/25.19 ~cLambda_2eRedexes_2eredexes___24t(sK1334_skl(sK1335_skl,sK1337_skl))|sK1340_skl=sK1334_skl(sK1335_skl,sK1337_skl)),
% 193.16/25.19 inference(resolution,[status(thm)],[f19985,f17786])).
% 193.16/25.19 fof(f20031,plain,(
% 193.16/25.19 ~cLambda_2eRedexes_2eredexes___24t(sK1335_skl)|~cLambda_2eRedexes_2eregular___24a1(sK1335_skl)|cLambda_2eResiduals_2eresiduals___24a3(sK1337_skl,sK1335_skl,sK1340_skl)),
% 193.16/25.19 inference(backward_demodulation,[status(thm)],[f20032,f18768])).
% 193.16/25.19 fof(f20032,plain,(
% 193.16/25.19 sK1340_skl=sK1334_skl(sK1335_skl,sK1337_skl)),
% 153.05/25.39 inference(forward_subsumption_resolution,[status(thm)],[f20002,f19257])).
% 153.05/25.39 fof(f20064,plain,(
% 153.05/25.39 ~cLambda_2eRedexes_2eregular___24a1(sK1335_skl)|cLambda_2eResiduals_2eresiduals___24a3(sK1337_skl,sK1335_skl,sK1340_skl)),
% 153.05/25.39 inference(forward_subsumption_resolution,[status(thm)],[f20031,f13319])).
% 153.05/25.39 fof(f20065,plain,(
% 153.05/25.39 cLambda_2eResiduals_2eresiduals___24a3(sK1337_skl,sK1335_skl,sK1340_skl)),
% 153.05/25.39 inference(resolution,[status(thm)],[f20064,f13323])).
% 153.05/25.39 fof(f20066,plain,(
% 153.05/25.39 $false),
% 153.05/25.39 inference(forward_subsumption_resolution,[status(thm)],[f20065,f13330])).
% 153.05/25.39 % SZS output end CNFRefutation for theBenchmark.p
% 7.22/25.43 % Elapsed time: 25.035634 seconds
% 7.22/25.43 % CPU time: 194.780632 seconds
% 7.22/25.43 % Total memory used: 1.254 GB
% 7.22/25.43 % Net memory used: 1.217 GB
%------------------------------------------------------------------------------