%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEV608+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 : n003.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 164.01s 164.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV608+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.07/0.35 % Computer : n003.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 21 07:31:01 UTC 2026
% 0.07/0.36 % CPUTime :
% 163.89/164.15 % Drodi V4.1.1
% 164.01/164.38 % Refutation found
% 164.01/164.38 % SZS status Theorem for theBenchmark: Theorem is valid
% 164.01/164.38 % SZS output start CNFRefutation for theBenchmark
% 164.01/164.38 fof(f1538,axiom,(
% 164.01/164.38 (! [V0__K] :( cCoq_2eInit_2eDatatypes_2enat___24t(V0__K)=> (! [V1__g] :( cColor_2egraph___24t(V1__g)=> (! [V2__n] :( cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt___24t(V2__n)=> ( cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2echoose___24a1(cColor_2esubset__nodes___24a2(cColor_2elow__deg___24a1(V0__K),V1__g)) = cCoq_2eInit_2eDatatypes_2eSome___24a2(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt,V2__n)=> cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset,cColor_2eremove__node___24a2(V2__n,V1__g)),cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset,V1__g)) ) ) )) )) )),
% 164.01/164.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 164.01/164.38 fof(f2868,conjecture,(
% 164.01/164.38 (! [V0__K] :( cCoq_2eInit_2eDatatypes_2enat___24t(V0__K)=> (! [V1__g] :( cColor_2egraph___24t(V1__g)=> (! [V2__n] :( cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt___24t(V2__n)=> ( cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2echoose___24a1(cColor_2esubset__nodes___24a2(cColor_2elow__deg___24a1(V0__K),V1__g)) = cCoq_2eInit_2eDatatypes_2eSome___24a2(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt,V2__n)=> cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset,cColor_2eremove__node___24a2(V2__n,V1__g)),cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset,V1__g)) ) ) )) )) )),
% 164.01/164.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 164.01/164.38 fof(f2869,negated_conjecture,(
% 164.01/164.38 ~((! [V0__K] :( cCoq_2eInit_2eDatatypes_2enat___24t(V0__K)=> (! [V1__g] :( cColor_2egraph___24t(V1__g)=> (! [V2__n] :( cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt___24t(V2__n)=> ( cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2echoose___24a1(cColor_2esubset__nodes___24a2(cColor_2elow__deg___24a1(V0__K),V1__g)) = cCoq_2eInit_2eDatatypes_2eSome___24a2(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt,V2__n)=> cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset,cColor_2eremove__node___24a2(V2__n,V1__g)),cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset,V1__g)) ) ) )) )) ))),
% 164.01/164.38 inference(negated_conjecture,[status(cth)],[f2868])).
% 164.01/164.38 fof(f10124,plain,(
% 164.01/164.38 ![V0__K]: (~cCoq_2eInit_2eDatatypes_2enat___24t(V0__K)|(![V1__g]: (~cColor_2egraph___24t(V1__g)|(![V2__n]: (~cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt___24t(V2__n)|(~cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2echoose___24a1(cColor_2esubset__nodes___24a2(cColor_2elow__deg___24a1(V0__K),V1__g))=cCoq_2eInit_2eDatatypes_2eSome___24a2(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt,V2__n)|cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset,cColor_2eremove__node___24a2(V2__n,V1__g)),cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset,V1__g))))))))),
% 164.01/164.38 inference(pre_NNF_transformation,[status(thm)],[f1538])).
% 164.01/164.38 fof(f10125,plain,(
% 164.01/164.38 ![X0,X1,X2]: (~cCoq_2eInit_2eDatatypes_2enat___24t(X0)|~cColor_2egraph___24t(X1)|~cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt___24t(X2)|~cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2echoose___24a1(cColor_2esubset__nodes___24a2(cColor_2elow__deg___24a1(X0),X1))=cCoq_2eInit_2eDatatypes_2eSome___24a2(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt,X2)|cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset,cColor_2eremove__node___24a2(X2,X1)),cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset,X1)))),
% 164.01/164.38 inference(cnf_transformation,[status(thm)],[f10124])).
% 164.01/164.38 fof(f13607,plain,(
% 164.01/164.38 (?[V0__K]: (cCoq_2eInit_2eDatatypes_2enat___24t(V0__K)&(?[V1__g]: (cColor_2egraph___24t(V1__g)&(?[V2__n]: (cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt___24t(V2__n)&(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2echoose___24a1(cColor_2esubset__nodes___24a2(cColor_2elow__deg___24a1(V0__K),V1__g))=cCoq_2eInit_2eDatatypes_2eSome___24a2(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt,V2__n)&~cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset,cColor_2eremove__node___24a2(V2__n,V1__g)),cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset,V1__g)))))))))),
% 164.01/164.38 inference(pre_NNF_transformation,[status(thm)],[f2869])).
% 164.01/164.38 fof(f13608,plain,(
% 164.01/164.38 (cCoq_2eInit_2eDatatypes_2enat___24t(sK1737_skl)&(cColor_2egraph___24t(sK1738_skl)&(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt___24t(sK1739_skl)&(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2echoose___24a1(cColor_2esubset__nodes___24a2(cColor_2elow__deg___24a1(sK1737_skl),sK1738_skl))=cCoq_2eInit_2eDatatypes_2eSome___24a2(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt,sK1739_skl)&~cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset,cColor_2eremove__node___24a2(sK1739_skl,sK1738_skl)),cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset,sK1738_skl))))))),
% 164.01/164.38 inference(skolemize,[status(esa),new_symbols(skolem,[sK1737_skl,sK1738_skl,sK1739_skl]),skolemize(V0__K,sK1737_skl),skolemize(V1__g,sK1738_skl),skolemize(V2__n,sK1739_skl)],[f13607])).
% 164.01/164.38 fof(f13609,plain,(
% 164.01/164.38 cCoq_2eInit_2eDatatypes_2enat___24t(sK1737_skl)),
% 164.01/164.38 inference(cnf_transformation,[status(thm)],[f13608])).
% 164.01/164.38 fof(f13610,plain,(
% 164.01/164.38 cColor_2egraph___24t(sK1738_skl)),
% 164.01/164.38 inference(cnf_transformation,[status(thm)],[f13608])).
% 164.01/164.38 fof(f13611,plain,(
% 164.01/164.38 cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt___24t(sK1739_skl)),
% 164.01/164.38 inference(cnf_transformation,[status(thm)],[f13608])).
% 164.01/164.38 fof(f13612,plain,(
% 164.01/164.38 cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2echoose___24a1(cColor_2esubset__nodes___24a2(cColor_2elow__deg___24a1(sK1737_skl),sK1738_skl))=cCoq_2eInit_2eDatatypes_2eSome___24a2(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt,sK1739_skl)),
% 164.01/164.38 inference(cnf_transformation,[status(thm)],[f13608])).
% 164.01/164.38 fof(f13613,plain,(
% 164.01/164.38 ~cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset,cColor_2eremove__node___24a2(sK1739_skl,sK1738_skl)),cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset,sK1738_skl))),
% 164.01/164.38 inference(cnf_transformation,[status(thm)],[f13608])).
% 164.01/164.38 fof(f23148,plain,(
% 164.01/164.38 ![X0]: (~cCoq_2eInit_2eDatatypes_2enat___24t(X0)|~cColor_2egraph___24t(sK1738_skl)|~cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt___24t(sK1739_skl)|~cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2echoose___24a1(cColor_2esubset__nodes___24a2(cColor_2elow__deg___24a1(X0),sK1738_skl))=cCoq_2eInit_2eDatatypes_2eSome___24a2(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt,sK1739_skl))),
% 164.01/164.38 inference(resolution,[status(thm)],[f10125,f13613])).
% 164.01/164.38 fof(f23149,plain,(
% 164.01/164.38 ![X0]: (~cCoq_2eInit_2eDatatypes_2enat___24t(X0)|~cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt___24t(sK1739_skl)|~cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2echoose___24a1(cColor_2esubset__nodes___24a2(cColor_2elow__deg___24a1(X0),sK1738_skl))=cCoq_2eInit_2eDatatypes_2eSome___24a2(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt,sK1739_skl))),
% 164.01/164.38 inference(forward_subsumption_resolution,[status(thm)],[f23148,f13610])).
% 164.01/164.38 fof(f23154,plain,(
% 164.01/164.38 ![X0]: (~cCoq_2eInit_2eDatatypes_2enat___24t(X0)|~cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2echoose___24a1(cColor_2esubset__nodes___24a2(cColor_2elow__deg___24a1(X0),sK1738_skl))=cCoq_2eInit_2eDatatypes_2eSome___24a2(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt,sK1739_skl))),
% 164.01/164.38 inference(forward_subsumption_resolution,[status(thm)],[f23149,f13611])).
% 164.01/164.38 fof(f23155,plain,(
% 164.01/164.38 ~cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2echoose___24a1(cColor_2esubset__nodes___24a2(cColor_2elow__deg___24a1(sK1737_skl),sK1738_skl))=cCoq_2eInit_2eDatatypes_2eSome___24a2(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt,sK1739_skl)),
% 164.01/164.38 inference(resolution,[status(thm)],[f23154,f13609])).
% 164.01/164.38 fof(f23156,plain,(
% 164.01/164.38 ~cCoq_2eInit_2eDatatypes_2eSome___24a2(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt,sK1739_skl)=cCoq_2eInit_2eDatatypes_2eSome___24a2(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt,sK1739_skl)),
% 164.01/164.38 inference(forward_demodulation,[status(thm)],[f13612,f23155])).
% 164.04/164.50 fof(f23157,plain,(
% 164.04/164.50 $false),
% 164.04/164.50 inference(trivial_equality_resolution,[status(thm)],[f23156])).
% 164.04/164.50 % SZS output end CNFRefutation for theBenchmark.p
% 164.07/164.60 % Elapsed time: 164.202622 seconds
% 164.07/164.60 % CPU time: 165.618667 seconds
% 164.07/164.60 % Total memory used: 4.182 GB
% 164.07/164.60 % Net memory used: 4.177 GB
%------------------------------------------------------------------------------