%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEV673+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 : n002.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:51 PM UTC 2026
% Result : Theorem 166.57s 160.05s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV673+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.09/15.58 % Computer : n002.cluster.edu
% 0.09/15.58 % Model : x86_64 x86_64
% 0.09/15.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/15.58 % Memory : 8046.5625MB
% 0.09/15.58 % OS : Linux 6.8.0-71-generic
% 0.09/15.58 % CPULimit : 300
% 0.09/15.58 % WCLimit : 300
% 0.09/15.58 % DateTime : Mon Sep 21 07:38:19 UTC 2026
% 0.09/15.59 % CPUTime :
% 141.25/156.75 % Drodi V4.1.1
% 166.57/160.05 % Refutation found
% 166.57/160.05 % SZS status Theorem for theBenchmark: Theorem is valid
% 166.57/160.05 % SZS output start CNFRefutation for theBenchmark
% 166.57/160.05 fof(f255,axiom,(
% 166.57/160.05 (! [V0__N,V1__M] : cSubstitution_2esubst__r___24a2(V0__N,V1__M) = cSubstitution_2esubst__rec__r___24a3(V1__M,V0__N,cCoq_2eInit_2eDatatypes_2eO) )),
% 166.57/160.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 166.57/160.05 fof(f834,axiom,(
% 166.57/160.05 cCoq_2eInit_2eDatatypes_2enat___24t(cCoq_2eInit_2eDatatypes_2eO) ),
% 166.57/160.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 166.57/160.05 fof(f1233,axiom,(
% 166.57/160.05 (! [V0__n] :( cCoq_2eInit_2eDatatypes_2enat___24t(V0__n)=> cCoq_2eInit_2eNat_2eadd___24a2(cCoq_2eInit_2eDatatypes_2eO,V0__n) = V0__n ) )),
% 166.57/160.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 166.57/160.05 fof(f1783,axiom,(
% 166.57/160.05 (! [V0__U] :( cLambda_2eRedexes_2eredexes___24t(V0__U)=> (! [V1__V] :( cLambda_2eRedexes_2eredexes___24t(V1__V)=> (! [V2__W] :( cLambda_2eRedexes_2eredexes___24t(V2__W)=> (! [V3__n] :( cCoq_2eInit_2eDatatypes_2enat___24t(V3__n)=> (! [V4__p] :( cCoq_2eInit_2eDatatypes_2enat___24t(V4__p)=> cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__rec__r___24a3(V1__V,V0__U,V4__p),V2__W,cCoq_2eInit_2eNat_2eadd___24a2(V4__p,V3__n)) = cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__rec__r___24a3(V1__V,V2__W,cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eNat_2eadd___24a2(V4__p,V3__n))),cSubstitution_2esubst__rec__r___24a3(V0__U,V2__W,V3__n),V4__p) ) )) )) )) )) )),
% 166.57/160.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 166.57/160.05 fof(f2702,conjecture,(
% 166.57/160.05 (! [V0__U] :( cLambda_2eRedexes_2eredexes___24t(V0__U)=> (! [V1__V] :( cLambda_2eRedexes_2eredexes___24t(V1__V)=> (! [V2__W] :( cLambda_2eRedexes_2eredexes___24t(V2__W)=> (! [V3__n] :( cCoq_2eInit_2eDatatypes_2enat___24t(V3__n)=> cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__rec__r___24a3(V1__V,V0__U,cCoq_2eInit_2eDatatypes_2eO),V2__W,V3__n) = cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__rec__r___24a3(V1__V,V2__W,cCoq_2eInit_2eDatatypes_2eS___24a1(V3__n)),cSubstitution_2esubst__rec__r___24a3(V0__U,V2__W,V3__n),cCoq_2eInit_2eDatatypes_2eO) ) )) )) )) )),
% 166.57/160.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 166.57/160.05 fof(f2703,negated_conjecture,(
% 166.57/160.05 ~((! [V0__U] :( cLambda_2eRedexes_2eredexes___24t(V0__U)=> (! [V1__V] :( cLambda_2eRedexes_2eredexes___24t(V1__V)=> (! [V2__W] :( cLambda_2eRedexes_2eredexes___24t(V2__W)=> (! [V3__n] :( cCoq_2eInit_2eDatatypes_2enat___24t(V3__n)=> cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__rec__r___24a3(V1__V,V0__U,cCoq_2eInit_2eDatatypes_2eO),V2__W,V3__n) = cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__rec__r___24a3(V1__V,V2__W,cCoq_2eInit_2eDatatypes_2eS___24a1(V3__n)),cSubstitution_2esubst__rec__r___24a3(V0__U,V2__W,V3__n),cCoq_2eInit_2eDatatypes_2eO) ) )) )) )) ))),
% 166.57/160.05 inference(negated_conjecture,[status(cth)],[f2702])).
% 166.57/160.05 fof(f4245,plain,(
% 166.57/160.05 ![X0,X1]: (cSubstitution_2esubst__r___24a2(X0,X1)=cSubstitution_2esubst__rec__r___24a3(X1,X0,cCoq_2eInit_2eDatatypes_2eO))),
% 166.57/160.05 inference(cnf_transformation,[status(thm)],[f255])).
% 166.57/160.05 fof(f7497,plain,(
% 166.57/160.05 cCoq_2eInit_2eDatatypes_2enat___24t(cCoq_2eInit_2eDatatypes_2eO)),
% 166.57/160.05 inference(cnf_transformation,[status(thm)],[f834])).
% 166.57/160.05 fof(f8126,plain,(
% 166.57/160.05 ![V0__n]: (~cCoq_2eInit_2eDatatypes_2enat___24t(V0__n)|cCoq_2eInit_2eNat_2eadd___24a2(cCoq_2eInit_2eDatatypes_2eO,V0__n)=V0__n)),
% 166.57/160.05 inference(pre_NNF_transformation,[status(thm)],[f1233])).
% 166.57/160.05 fof(f8127,plain,(
% 166.57/160.05 ![X0]: (~cCoq_2eInit_2eDatatypes_2enat___24t(X0)|cCoq_2eInit_2eNat_2eadd___24a2(cCoq_2eInit_2eDatatypes_2eO,X0)=X0)),
% 166.57/160.05 inference(cnf_transformation,[status(thm)],[f8126])).
% 166.57/160.05 fof(f9654,plain,(
% 166.57/160.05 ![V0__U]: (~cLambda_2eRedexes_2eredexes___24t(V0__U)|(![V1__V]: (~cLambda_2eRedexes_2eredexes___24t(V1__V)|(![V2__W]: (~cLambda_2eRedexes_2eredexes___24t(V2__W)|(![V3__n]: (~cCoq_2eInit_2eDatatypes_2enat___24t(V3__n)|(![V4__p]: (~cCoq_2eInit_2eDatatypes_2enat___24t(V4__p)|cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__rec__r___24a3(V1__V,V0__U,V4__p),V2__W,cCoq_2eInit_2eNat_2eadd___24a2(V4__p,V3__n))=cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__rec__r___24a3(V1__V,V2__W,cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eNat_2eadd___24a2(V4__p,V3__n))),cSubstitution_2esubst__rec__r___24a3(V0__U,V2__W,V3__n),V4__p))))))))))),
% 166.57/160.05 inference(pre_NNF_transformation,[status(thm)],[f1783])).
% 166.57/160.05 fof(f9655,plain,(
% 166.57/160.05 ![X0,X1,X2,X3,X4]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eRedexes_2eredexes___24t(X2)|~cCoq_2eInit_2eDatatypes_2enat___24t(X3)|~cCoq_2eInit_2eDatatypes_2enat___24t(X4)|cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__rec__r___24a3(X1,X0,X4),X2,cCoq_2eInit_2eNat_2eadd___24a2(X4,X3))=cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__rec__r___24a3(X1,X2,cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eNat_2eadd___24a2(X4,X3))),cSubstitution_2esubst__rec__r___24a3(X0,X2,X3),X4))),
% 166.57/160.05 inference(cnf_transformation,[status(thm)],[f9654])).
% 166.57/160.05 fof(f11717,plain,(
% 166.57/160.05 (?[V0__U]: (cLambda_2eRedexes_2eredexes___24t(V0__U)&(?[V1__V]: (cLambda_2eRedexes_2eredexes___24t(V1__V)&(?[V2__W]: (cLambda_2eRedexes_2eredexes___24t(V2__W)&(?[V3__n]: (cCoq_2eInit_2eDatatypes_2enat___24t(V3__n)&~cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__rec__r___24a3(V1__V,V0__U,cCoq_2eInit_2eDatatypes_2eO),V2__W,V3__n)=cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__rec__r___24a3(V1__V,V2__W,cCoq_2eInit_2eDatatypes_2eS___24a1(V3__n)),cSubstitution_2esubst__rec__r___24a3(V0__U,V2__W,V3__n),cCoq_2eInit_2eDatatypes_2eO)))))))))),
% 166.57/160.05 inference(pre_NNF_transformation,[status(thm)],[f2703])).
% 166.57/160.05 fof(f11718,plain,(
% 166.57/160.05 (cLambda_2eRedexes_2eredexes___24t(sK1229_skl)&(cLambda_2eRedexes_2eredexes___24t(sK1230_skl)&(cLambda_2eRedexes_2eredexes___24t(sK1231_skl)&(cCoq_2eInit_2eDatatypes_2enat___24t(sK1232_skl)&~cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__rec__r___24a3(sK1230_skl,sK1229_skl,cCoq_2eInit_2eDatatypes_2eO),sK1231_skl,sK1232_skl)=cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__rec__r___24a3(sK1230_skl,sK1231_skl,cCoq_2eInit_2eDatatypes_2eS___24a1(sK1232_skl)),cSubstitution_2esubst__rec__r___24a3(sK1229_skl,sK1231_skl,sK1232_skl),cCoq_2eInit_2eDatatypes_2eO)))))),
% 166.57/160.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK1229_skl,sK1230_skl,sK1231_skl,sK1232_skl]),skolemize(V0__U,sK1229_skl),skolemize(V1__V,sK1230_skl),skolemize(V2__W,sK1231_skl),skolemize(V3__n,sK1232_skl)],[f11717])).
% 166.57/160.05 fof(f11719,plain,(
% 166.57/160.05 cLambda_2eRedexes_2eredexes___24t(sK1229_skl)),
% 166.57/160.05 inference(cnf_transformation,[status(thm)],[f11718])).
% 166.57/160.05 fof(f11720,plain,(
% 166.57/160.05 cLambda_2eRedexes_2eredexes___24t(sK1230_skl)),
% 166.57/160.05 inference(cnf_transformation,[status(thm)],[f11718])).
% 166.57/160.05 fof(f11721,plain,(
% 166.57/160.05 cLambda_2eRedexes_2eredexes___24t(sK1231_skl)),
% 166.57/160.05 inference(cnf_transformation,[status(thm)],[f11718])).
% 166.57/160.05 fof(f11722,plain,(
% 166.57/160.05 cCoq_2eInit_2eDatatypes_2enat___24t(sK1232_skl)),
% 166.57/160.05 inference(cnf_transformation,[status(thm)],[f11718])).
% 166.57/160.05 fof(f11723,plain,(
% 166.57/160.05 ~cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__rec__r___24a3(sK1230_skl,sK1229_skl,cCoq_2eInit_2eDatatypes_2eO),sK1231_skl,sK1232_skl)=cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__rec__r___24a3(sK1230_skl,sK1231_skl,cCoq_2eInit_2eDatatypes_2eS___24a1(sK1232_skl)),cSubstitution_2esubst__rec__r___24a3(sK1229_skl,sK1231_skl,sK1232_skl),cCoq_2eInit_2eDatatypes_2eO)),
% 166.57/160.05 inference(cnf_transformation,[status(thm)],[f11718])).
% 166.57/160.05 fof(f16795,plain,(
% 166.57/160.05 ![X0,X1,X2,X3]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eRedexes_2eredexes___24t(X2)|~cCoq_2eInit_2eDatatypes_2enat___24t(X3)|cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__rec__r___24a3(X1,X0,cCoq_2eInit_2eDatatypes_2eO),X2,cCoq_2eInit_2eNat_2eadd___24a2(cCoq_2eInit_2eDatatypes_2eO,X3))=cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__rec__r___24a3(X1,X2,cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eNat_2eadd___24a2(cCoq_2eInit_2eDatatypes_2eO,X3))),cSubstitution_2esubst__rec__r___24a3(X0,X2,X3),cCoq_2eInit_2eDatatypes_2eO))),
% 166.57/160.05 inference(resolution,[status(thm)],[f9655,f7497])).
% 166.57/160.05 fof(f16819,plain,(
% 166.57/160.05 ~cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__r___24a2(sK1229_skl,sK1230_skl),sK1231_skl,sK1232_skl)=cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__rec__r___24a3(sK1230_skl,sK1231_skl,cCoq_2eInit_2eDatatypes_2eS___24a1(sK1232_skl)),cSubstitution_2esubst__rec__r___24a3(sK1229_skl,sK1231_skl,sK1232_skl),cCoq_2eInit_2eDatatypes_2eO)),
% 166.57/160.05 inference(backward_demodulation,[status(thm)],[f4245,f11723])).
% 166.57/160.05 fof(f16820,plain,(
% 166.57/160.05 ~cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__r___24a2(sK1229_skl,sK1230_skl),sK1231_skl,sK1232_skl)=cSubstitution_2esubst__r___24a2(cSubstitution_2esubst__rec__r___24a3(sK1229_skl,sK1231_skl,sK1232_skl),cSubstitution_2esubst__rec__r___24a3(sK1230_skl,sK1231_skl,cCoq_2eInit_2eDatatypes_2eS___24a1(sK1232_skl)))),
% 166.57/160.05 inference(forward_demodulation,[status(thm)],[f4245,f16819])).
% 166.57/160.05 fof(f16864,plain,(
% 166.57/160.05 ![X0,X1,X2,X3]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eRedexes_2eredexes___24t(X2)|~cCoq_2eInit_2eDatatypes_2enat___24t(X3)|cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__r___24a2(X0,X1),X2,cCoq_2eInit_2eNat_2eadd___24a2(cCoq_2eInit_2eDatatypes_2eO,X3))=cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__rec__r___24a3(X1,X2,cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eNat_2eadd___24a2(cCoq_2eInit_2eDatatypes_2eO,X3))),cSubstitution_2esubst__rec__r___24a3(X0,X2,X3),cCoq_2eInit_2eDatatypes_2eO))),
% 166.57/160.05 inference(forward_demodulation,[status(thm)],[f4245,f16795])).
% 166.57/160.05 fof(f16865,plain,(
% 166.57/160.05 ![X0,X1,X2,X3]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eRedexes_2eredexes___24t(X2)|~cCoq_2eInit_2eDatatypes_2enat___24t(X3)|cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__r___24a2(X0,X1),X2,cCoq_2eInit_2eNat_2eadd___24a2(cCoq_2eInit_2eDatatypes_2eO,X3))=cSubstitution_2esubst__r___24a2(cSubstitution_2esubst__rec__r___24a3(X0,X2,X3),cSubstitution_2esubst__rec__r___24a3(X1,X2,cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eNat_2eadd___24a2(cCoq_2eInit_2eDatatypes_2eO,X3)))))),
% 166.57/160.05 inference(forward_demodulation,[status(thm)],[f4245,f16864])).
% 166.57/160.05 fof(f16867,plain,(
% 166.57/160.05 ![X0,X1,X2]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eRedexes_2eredexes___24t(X2)|cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__r___24a2(X0,X1),X2,cCoq_2eInit_2eNat_2eadd___24a2(cCoq_2eInit_2eDatatypes_2eO,sK1232_skl))=cSubstitution_2esubst__r___24a2(cSubstitution_2esubst__rec__r___24a3(X0,X2,sK1232_skl),cSubstitution_2esubst__rec__r___24a3(X1,X2,cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eNat_2eadd___24a2(cCoq_2eInit_2eDatatypes_2eO,sK1232_skl)))))),
% 166.57/160.05 inference(resolution,[status(thm)],[f16865,f11722])).
% 166.57/160.05 fof(f17033,plain,(
% 166.57/160.05 cCoq_2eInit_2eNat_2eadd___24a2(cCoq_2eInit_2eDatatypes_2eO,sK1232_skl)=sK1232_skl),
% 166.57/160.05 inference(resolution,[status(thm)],[f8127,f11722])).
% 166.57/160.05 fof(f17142,plain,(
% 166.57/160.05 ![X0,X1,X2]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eRedexes_2eredexes___24t(X2)|cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__r___24a2(X0,X1),X2,cCoq_2eInit_2eNat_2eadd___24a2(cCoq_2eInit_2eDatatypes_2eO,sK1232_skl))=cSubstitution_2esubst__r___24a2(cSubstitution_2esubst__rec__r___24a3(X0,X2,sK1232_skl),cSubstitution_2esubst__rec__r___24a3(X1,X2,cCoq_2eInit_2eDatatypes_2eS___24a1(sK1232_skl))))),
% 166.57/160.05 inference(backward_demodulation,[status(thm)],[f17033,f16867])).
% 166.57/160.05 fof(f17144,plain,(
% 166.57/160.05 ![X0,X1,X2]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2eredexes___24t(X1)|~cLambda_2eRedexes_2eredexes___24t(X2)|cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__r___24a2(X0,X1),X2,sK1232_skl)=cSubstitution_2esubst__r___24a2(cSubstitution_2esubst__rec__r___24a3(X0,X2,sK1232_skl),cSubstitution_2esubst__rec__r___24a3(X1,X2,cCoq_2eInit_2eDatatypes_2eS___24a1(sK1232_skl))))),
% 166.57/160.05 inference(forward_demodulation,[status(thm)],[f17033,f17142])).
% 166.57/160.05 fof(f17596,plain,(
% 166.57/160.05 ![X0,X1]: (~cLambda_2eRedexes_2eredexes___24t(X0)|~cLambda_2eRedexes_2eredexes___24t(X1)|cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__r___24a2(X0,sK1230_skl),X1,sK1232_skl)=cSubstitution_2esubst__r___24a2(cSubstitution_2esubst__rec__r___24a3(X0,X1,sK1232_skl),cSubstitution_2esubst__rec__r___24a3(sK1230_skl,X1,cCoq_2eInit_2eDatatypes_2eS___24a1(sK1232_skl))))),
% 161.36/160.15 inference(resolution,[status(thm)],[f17144,f11720])).
% 161.36/160.15 fof(f18051,plain,(
% 161.36/160.15 ![X0]: (~cLambda_2eRedexes_2eredexes___24t(X0)|cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__r___24a2(X0,sK1230_skl),sK1231_skl,sK1232_skl)=cSubstitution_2esubst__r___24a2(cSubstitution_2esubst__rec__r___24a3(X0,sK1231_skl,sK1232_skl),cSubstitution_2esubst__rec__r___24a3(sK1230_skl,sK1231_skl,cCoq_2eInit_2eDatatypes_2eS___24a1(sK1232_skl))))),
% 161.36/160.15 inference(resolution,[status(thm)],[f17596,f11721])).
% 161.36/160.15 fof(f18324,plain,(
% 161.36/160.15 cSubstitution_2esubst__rec__r___24a3(cSubstitution_2esubst__r___24a2(sK1229_skl,sK1230_skl),sK1231_skl,sK1232_skl)=cSubstitution_2esubst__r___24a2(cSubstitution_2esubst__rec__r___24a3(sK1229_skl,sK1231_skl,sK1232_skl),cSubstitution_2esubst__rec__r___24a3(sK1230_skl,sK1231_skl,cCoq_2eInit_2eDatatypes_2eS___24a1(sK1232_skl)))),
% 161.36/160.15 inference(resolution,[status(thm)],[f18051,f11719])).
% 161.36/160.15 fof(f18325,plain,(
% 161.36/160.15 $false),
% 161.36/160.15 inference(forward_subsumption_resolution,[status(thm)],[f18324,f16820])).
% 161.36/160.15 % SZS output end CNFRefutation for theBenchmark.p
% 161.36/160.17 % Elapsed time: 144.570375 seconds
% 161.36/160.17 % CPU time: 167.141869 seconds
% 161.36/160.17 % Total memory used: 4.422 GB
% 161.36/160.17 % Net memory used: 4.401 GB
%------------------------------------------------------------------------------