%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEV678+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/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 142.49s 152.94s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV678+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/10.39 % Computer : n002.cluster.edu
% 0.12/10.39 % Model : x86_64 x86_64
% 0.12/10.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/10.39 % Memory : 8046.5625MB
% 0.12/10.39 % OS : Linux 6.8.0-71-generic
% 0.12/10.39 % CPULimit : 300
% 0.12/10.39 % WCLimit : 300
% 0.12/10.39 % DateTime : Mon Sep 21 07:38:28 UTC 2026
% 0.15/10.40 % CPUTime :
% 142.33/152.63 % Drodi V4.1.1
% 142.49/152.94 % Refutation found
% 142.49/152.94 % SZS status Theorem for theBenchmark: Theorem is valid
% 142.49/152.94 % SZS output start CNFRefutation for theBenchmark
% 142.49/152.94 fof(f267,axiom,(
% 142.49/152.94 ( p(cUseAuto_2emyFact)<=> (! [V0__x] :( cCoq_2eInit_2eDatatypes_2enat___24t(V0__x)=> ( cCoq_2eInit_2ePeano_2ele___24a2(V0__x,cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eO))))=> cUseAuto_2eP___24a1(V0__x) ) ) )) ),
% 142.49/152.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 142.49/152.94 fof(f277,axiom,(
% 142.49/152.94 cCoq_2eInit_2eDatatypes_2etrue != cCoq_2eInit_2eDatatypes_2efalse ),
% 142.49/152.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 142.49/152.94 fof(f1413,axiom,(
% 142.49/152.94 cCoq_2eNumbers_2eBinNums_2epositive___24t(cCoq_2eNumbers_2eBinNums_2exH) ),
% 142.49/152.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 142.49/152.94 fof(f1688,axiom,(
% 142.49/152.94 cProp___24t(cUseAuto_2emyFact) ),
% 142.49/152.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 142.49/152.94 fof(f2925,conjecture,(
% 142.49/152.94 ( (! [V0__x] :( cCoq_2eInit_2eDatatypes_2enat___24t(V0__x)=> cUseAuto_2eP___24a1(V0__x) ))=> p(cUseAuto_2emyFact) ) ),
% 142.49/152.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 142.49/152.94 fof(f2926,negated_conjecture,(
% 142.49/152.94 ~(( (! [V0__x] :( cCoq_2eInit_2eDatatypes_2enat___24t(V0__x)=> cUseAuto_2eP___24a1(V0__x) ))=> p(cUseAuto_2emyFact) ) )),
% 142.49/152.94 inference(negated_conjecture,[status(cth)],[f2925])).
% 142.49/152.94 fof(f4523,plain,(
% 142.49/152.94 p(cUseAuto_2emyFact)<=>(![V0__x]: (~cCoq_2eInit_2eDatatypes_2enat___24t(V0__x)|(~cCoq_2eInit_2ePeano_2ele___24a2(V0__x,cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eO))))|cUseAuto_2eP___24a1(V0__x))))),
% 142.49/152.94 inference(pre_NNF_transformation,[status(thm)],[f267])).
% 142.49/152.94 fof(f4524,plain,(
% 142.49/152.94 (~p(cUseAuto_2emyFact)|(![V0__x]: (~cCoq_2eInit_2eDatatypes_2enat___24t(V0__x)|(~cCoq_2eInit_2ePeano_2ele___24a2(V0__x,cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eO))))|cUseAuto_2eP___24a1(V0__x)))))&(p(cUseAuto_2emyFact)|(?[V0__x]: (cCoq_2eInit_2eDatatypes_2enat___24t(V0__x)&(cCoq_2eInit_2ePeano_2ele___24a2(V0__x,cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eO))))&~cUseAuto_2eP___24a1(V0__x)))))),
% 142.49/152.94 inference(NNF_transformation,[status(thm)],[f4523])).
% 142.49/152.94 fof(f4525,plain,(
% 142.49/152.94 (~p(cUseAuto_2emyFact)|(![V0__x]: (~cCoq_2eInit_2eDatatypes_2enat___24t(V0__x)|(~cCoq_2eInit_2ePeano_2ele___24a2(V0__x,cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eO))))|cUseAuto_2eP___24a1(V0__x)))))&(p(cUseAuto_2emyFact)|(cCoq_2eInit_2eDatatypes_2enat___24t(sK206_skl)&(cCoq_2eInit_2ePeano_2ele___24a2(sK206_skl,cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eS___24a1(cCoq_2eInit_2eDatatypes_2eO))))&~cUseAuto_2eP___24a1(sK206_skl))))),
% 142.49/152.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK206_skl]),skolemize(V0__x,sK206_skl)],[f4524])).
% 142.49/152.94 fof(f4527,plain,(
% 142.49/152.94 p(cUseAuto_2emyFact)|cCoq_2eInit_2eDatatypes_2enat___24t(sK206_skl)),
% 142.49/152.94 inference(cnf_transformation,[status(thm)],[f4525])).
% 142.49/152.94 fof(f4529,plain,(
% 142.49/152.94 p(cUseAuto_2emyFact)|~cUseAuto_2eP___24a1(sK206_skl)),
% 142.49/152.94 inference(cnf_transformation,[status(thm)],[f4525])).
% 142.49/152.94 fof(f4541,plain,(
% 142.49/152.94 ~cCoq_2eInit_2eDatatypes_2etrue=cCoq_2eInit_2eDatatypes_2efalse),
% 142.49/152.94 inference(cnf_transformation,[status(thm)],[f277])).
% 142.49/152.94 fof(f9421,plain,(
% 142.49/152.94 cCoq_2eNumbers_2eBinNums_2epositive___24t(cCoq_2eNumbers_2eBinNums_2exH)),
% 142.49/152.94 inference(cnf_transformation,[status(thm)],[f1413])).
% 142.49/152.94 fof(f9696,plain,(
% 142.49/152.94 cProp___24t(cUseAuto_2emyFact)),
% 142.49/152.94 inference(cnf_transformation,[status(thm)],[f1688])).
% 142.49/152.94 fof(f12907,plain,(
% 142.49/152.94 ((![V0__x]: (~cCoq_2eInit_2eDatatypes_2enat___24t(V0__x)|cUseAuto_2eP___24a1(V0__x)))&~p(cUseAuto_2emyFact))),
% 142.49/152.94 inference(pre_NNF_transformation,[status(thm)],[f2926])).
% 142.49/152.94 fof(f12908,plain,(
% 142.49/152.94 ![X0]: (~cCoq_2eInit_2eDatatypes_2enat___24t(X0)|cUseAuto_2eP___24a1(X0))),
% 142.49/152.94 inference(cnf_transformation,[status(thm)],[f12907])).
% 142.49/152.94 fof(f12909,plain,(
% 142.49/153.01 ~p(cUseAuto_2emyFact)),
% 142.49/153.01 inference(cnf_transformation,[status(thm)],[f12907])).
% 142.49/153.01 fof(f19011,definition,(
% 142.49/153.01 sQ11_spl <=> (p(cUseAuto_2emyFact))),
% 142.49/153.01 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 142.49/153.01 fof(f19012,plain,(
% 142.49/153.01 p(cUseAuto_2emyFact)|~sQ11_spl),
% 142.49/153.01 inference(component_clause,[status(thm)],[f19011])).
% 142.49/153.01 fof(f19018,definition,(
% 142.49/153.01 sQ13_spl <=> (cCoq_2eInit_2eDatatypes_2enat___24t(sK206_skl))),
% 142.49/153.01 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 142.49/153.01 fof(f19019,plain,(
% 142.49/153.01 cCoq_2eInit_2eDatatypes_2enat___24t(sK206_skl)|~sQ13_spl),
% 142.49/153.01 inference(component_clause,[status(thm)],[f19018])).
% 142.49/153.01 fof(f19021,plain,(
% 142.49/153.01 sQ11_spl|sQ13_spl),
% 142.49/153.01 inference(split_clause,[status(thm)],[f4527,f19011,f19018])).
% 142.49/153.01 fof(f19026,definition,(
% 142.49/153.01 sQ15_spl <=> (cUseAuto_2eP___24a1(sK206_skl))),
% 142.49/153.01 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 142.49/153.01 fof(f19028,plain,(
% 142.49/153.01 ~cUseAuto_2eP___24a1(sK206_skl)|sQ15_spl),
% 142.49/153.01 inference(component_clause,[status(thm)],[f19026])).
% 142.49/153.01 fof(f19029,plain,(
% 142.49/153.01 sQ11_spl|~sQ15_spl),
% 142.49/153.01 inference(split_clause,[status(thm)],[f4529,f19011,f19026])).
% 142.49/153.01 fof(f19188,definition,(
% 142.49/153.01 ![X2]: (sQ56_spl <=> (~cProp___24t(X2)))),
% 142.49/153.01 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 142.49/153.01 fof(f19189,plain,(
% 142.49/153.01 ![X0]: (~cProp___24t(X0)|~sQ56_spl)),
% 142.49/153.01 inference(component_clause,[status(thm)],[f19188])).
% 142.49/153.01 fof(f19263,definition,(
% 142.49/153.01 ![X2]: (sQ75_spl <=> (~cCoq_2eNumbers_2eBinNums_2epositive___24t(X2)))),
% 142.49/153.01 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 142.49/153.01 fof(f19264,plain,(
% 142.49/153.01 ![X0]: (~cCoq_2eNumbers_2eBinNums_2epositive___24t(X0)|~sQ75_spl)),
% 142.49/153.01 inference(component_clause,[status(thm)],[f19263])).
% 142.49/153.01 fof(f20237,plain,(
% 142.49/153.01 $false|~sQ11_spl),
% 142.49/153.01 inference(forward_subsumption_resolution,[status(thm)],[f19012,f12909])).
% 142.49/153.01 fof(f20238,plain,(
% 142.49/153.01 ~sQ11_spl),
% 142.49/153.01 inference(contradiction_clause,[status(thm)],[f20237])).
% 142.49/153.01 fof(f20245,plain,(
% 142.49/153.01 $false|~sQ56_spl),
% 142.49/153.01 inference(backward_subsumption_resolution,[status(thm)],[f9696,f19189])).
% 142.49/153.01 fof(f20246,plain,(
% 142.49/153.01 ~sQ56_spl),
% 142.49/153.01 inference(contradiction_clause,[status(thm)],[f20245])).
% 142.49/153.01 fof(f20545,plain,(
% 142.49/153.01 $false|~sQ75_spl),
% 142.49/153.01 inference(forward_subsumption_resolution,[status(thm)],[f9421,f19264])).
% 142.49/153.01 fof(f20546,plain,(
% 142.49/153.01 ~sQ75_spl),
% 142.49/153.01 inference(contradiction_clause,[status(thm)],[f20545])).
% 142.49/153.01 fof(f20711,definition,(
% 142.49/153.01 sQ131_spl <=> (cCoq_2eInit_2eDatatypes_2etrue=cCoq_2eInit_2eDatatypes_2efalse)),
% 142.49/153.01 introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition])).
% 142.49/153.01 fof(f20712,plain,(
% 142.49/153.01 cCoq_2eInit_2eDatatypes_2etrue=cCoq_2eInit_2eDatatypes_2efalse|~sQ131_spl),
% 142.49/153.01 inference(component_clause,[status(thm)],[f20711])).
% 142.49/153.01 fof(f20990,plain,(
% 142.49/153.01 $false|~sQ131_spl),
% 142.49/153.01 inference(forward_subsumption_resolution,[status(thm)],[f20712,f4541])).
% 142.49/153.01 fof(f20991,plain,(
% 142.49/153.01 ~sQ131_spl),
% 142.49/153.01 inference(contradiction_clause,[status(thm)],[f20990])).
% 142.49/153.01 fof(f21251,plain,(
% 142.49/153.01 cUseAuto_2eP___24a1(sK206_skl)|~sQ13_spl),
% 142.49/153.01 inference(resolution,[status(thm)],[f19019,f12908])).
% 142.49/153.01 fof(f21363,plain,(
% 142.49/153.01 $false|sQ15_spl|~sQ13_spl),
% 142.49/153.01 inference(forward_subsumption_resolution,[status(thm)],[f21251,f19028])).
% 142.49/153.01 fof(f21364,plain,(
% 142.49/153.01 sQ15_spl|~sQ13_spl),
% 142.49/153.01 inference(contradiction_clause,[status(thm)],[f21363])).
% 142.49/153.01 fof(f21365,plain,(
% 142.49/153.01 $false),
% 142.49/153.01 inference(sat_refutation,[status(thm)],[f19021,f19029,f20238,f20246,f20546,f20991,f21364])).
% 142.49/153.01 % SZS output end CNFRefutation for theBenchmark.p
% 142.51/153.10 % Elapsed time: 142.682200 seconds
% 142.51/153.10 % CPU time: 144.663149 seconds
% 142.51/153.10 % Total memory used: 3.874 GB
% 142.51/153.10 % Net memory used: 3.870 GB
%------------------------------------------------------------------------------