%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SEV608+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n031.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 06:52:35 PM UTC 2026
% Result : Theorem 43.66s 6.15s
% Output : CNFRefutation 43.66s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEV608+1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.14 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.35 % Computer : n031.cluster.edu
% 0.18/0.35 % Model : x86_64 x86_64
% 0.18/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.35 % Memory : 8042.1875MB
% 0.18/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.18/0.35 % CPULimit : 300
% 0.18/0.35 % WCLimit : 300
% 0.18/0.36 % DateTime : Tue May 5 05:28:08 EDT 2026
% 0.18/0.36 % CPUTime :
% 0.45/0.69 % launching worker at depth: 3
% 0.45/0.69 % launching worker at depth: 6
% 0.45/0.69 % launching worker at depth: 7
% 0.45/0.69 % launching worker at depth: 4
% 0.45/0.69 % launching worker at depth: 5
% 0.45/0.69 % launching worker at depth: 1
% 0.45/0.69 % launching worker at depth: 2
% 0.45/0.69 % launching worker at depth: 8
% 2.17/0.98 % launching worker at depth: 9
% 43.66/6.15 % SZS status Theorem for theBenchmark
% 43.66/6.15 % SZS output start CNFRefutation
% 43.66/6.15 fof('_HAMMER_GOAL', plain, ![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)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', '_HAMMER_GOAL')).
% 43.66/6.15 fof('_HAMMER_GOAL'_negated, plain, ~(![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))))))), inference(negate_conjecture, [status(cth)], ['_HAMMER_GOAL'])).
% 43.66/6.15 cnf(8704, plain, cCoq_2eInit_2eDatatypes_2enat___24t(sK2087), inference(cnf, [status(esa)], ['_HAMMER_GOAL'_negated])).
% 43.66/6.15 cnf(l0, plain, cCoq_2eInit_2eDatatypes_2enat___24t(sK2087), inference(instantiation, [status(thm)], [8704])).
% 43.66/6.15 fof('Color.select_terminates', plain, ![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)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'Color.select_terminates')).
% 43.66/6.15 cnf(6652, plain, 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_2eFSets_2eFSetPositive_2ePositiveSet_2eelt___24t(X2) | ~cColor_2egraph___24t(X1) | ~cCoq_2eInit_2eDatatypes_2enat___24t(X0) | 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)), inference(cnf, [status(esa)], ['Color.select_terminates'])).
% 43.66/6.15 cnf(l1, plain, cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2echoose___24a1(cColor_2esubset__nodes___24a2(cColor_2elow__deg___24a1(sK2087),sK2088)) != cCoq_2eInit_2eDatatypes_2eSome___24a2(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt,sK2089) | ~cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt___24t(sK2089) | ~cColor_2egraph___24t(sK2088) | ~cCoq_2eInit_2eDatatypes_2enat___24t(sK2087) | cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset,cColor_2eremove__node___24a2(sK2089,sK2088)),cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset,sK2088)), inference(instantiation, [status(thm)], [6652])).
% 43.66/6.15 cnf(8707, plain, cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2echoose___24a1(cColor_2esubset__nodes___24a2(cColor_2elow__deg___24a1(sK2087),sK2088)) = cCoq_2eInit_2eDatatypes_2eSome___24a2(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt,sK2089), inference(cnf, [status(esa)], ['_HAMMER_GOAL'_negated])).
% 43.66/6.15 cnf(l6, plain, cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2echoose___24a1(cColor_2esubset__nodes___24a2(cColor_2elow__deg___24a1(sK2087),sK2088)) = cCoq_2eInit_2eDatatypes_2eSome___24a2(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt,sK2089), inference(instantiation, [status(thm)], [8707])).
% 43.66/6.15 cnf(8706, plain, cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt___24t(sK2089), inference(cnf, [status(esa)], ['_HAMMER_GOAL'_negated])).
% 43.66/6.15 cnf(l3, plain, cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt___24t(sK2089), inference(instantiation, [status(thm)], [8706])).
% 43.66/6.15 cnf(8708, plain, ~cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset,cColor_2eremove__node___24a2(sK2089,sK2088)),cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset,sK2088)), inference(cnf, [status(esa)], ['_HAMMER_GOAL'_negated])).
% 43.66/6.15 cnf(l4, plain, ~cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset,cColor_2eremove__node___24a2(sK2089,sK2088)),cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset,sK2088)), inference(instantiation, [status(thm)], [8708])).
% 43.66/6.15 cnf(8705, plain, cColor_2egraph___24t(sK2088), inference(cnf, [status(esa)], ['_HAMMER_GOAL'_negated])).
% 43.66/6.15 cnf(l7, plain, cColor_2egraph___24t(sK2088), inference(instantiation, [status(thm)], [8705])).
% 43.66/6.15 cnf(final, plain, $false, inference(ground_refutation, [status(thm)], [l0, l1, l6, l3, l4, l7])).
% 43.66/6.15 % SZS output end CNFRefutation
%------------------------------------------------------------------------------