%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEV608+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n009.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:53:11 PM UTC 2026
% Result : Theorem 5.81s 7.62s
% Output : Proof 5.81s
% 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.00/0.13 % Command : leancop_casc.sh %s %d
% 0.17/0.34 % Computer : n009.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34 % CPULimit : 300
% 0.17/0.34 % WCLimit : 300
% 0.17/0.34 % DateTime : Tue May 5 05:25:55 EDT 2026
% 0.17/0.35 % CPUTime :
% 4.45/4.58 *** Overflow of the global/trail stack in spite of garbage collection!
% 4.45/4.58 You can use the "-g kBytes" (GLOBALSIZE) option to have a larger stack.
% 4.45/4.58 Peak sizes were: global stack 130976 kbytes, trail stack 4192 kbytes
% 5.81/7.62 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.81/7.62 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.81/7.63
% 5.81/7.63 %-----------------------------------------------------
% 5.81/7.63 fof('_HAMMER_GOAL', conjecture, ! [_1110183] : (cCoq_2eInit_2eDatatypes_2enat___24t(_1110183) => ! [_1110198] : (cColor_2egraph___24t(_1110198) => ! [_1110213] : (cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt___24t(_1110213) => cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2echoose___24a1(cColor_2esubset__nodes___24a2(cColor_2elow__deg___24a1(_1110183), _1110198)) = cCoq_2eInit_2eDatatypes_2eSome___24a2(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt, _1110213) => cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset, cColor_2eremove__node___24a2(_1110213, _1110198)), cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset, _1110198))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', '_HAMMER_GOAL')).
% 5.81/7.63 fof('Color.select_terminates', axiom, ! [_1113670] : (cCoq_2eInit_2eDatatypes_2enat___24t(_1113670) => ! [_1113685] : (cColor_2egraph___24t(_1113685) => ! [_1113700] : (cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt___24t(_1113700) => cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2echoose___24a1(cColor_2esubset__nodes___24a2(cColor_2elow__deg___24a1(_1113670), _1113685)) = cCoq_2eInit_2eDatatypes_2eSome___24a2(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt, _1113700) => cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset, cColor_2eremove__node___24a2(_1113700, _1113685)), cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset, _1113685))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'Color.select_terminates')).
% 5.81/7.63
% 5.81/7.63 cnf(1, plain, [-(cCoq_2eInit_2eDatatypes_2enat___24t(4222 ^ []))], clausify('_HAMMER_GOAL')).
% 5.81/7.63 cnf(2, plain, [-(cColor_2egraph___24t(4223 ^ []))], clausify('_HAMMER_GOAL')).
% 5.81/7.63 cnf(3, plain, [-(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt___24t(4224 ^ []))], clausify('_HAMMER_GOAL')).
% 5.81/7.63 cnf(4, plain, [-(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2echoose___24a1(cColor_2esubset__nodes___24a2(cColor_2elow__deg___24a1(4222 ^ []), 4223 ^ [])) = cCoq_2eInit_2eDatatypes_2eSome___24a2(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt, 4224 ^ []))], clausify('_HAMMER_GOAL')).
% 5.81/7.63 cnf(5, plain, [cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset, cColor_2eremove__node___24a2(4224 ^ [], 4223 ^ [])), cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset, 4223 ^ []))], clausify('_HAMMER_GOAL')).
% 5.81/7.63 cnf(6, plain, [cCoq_2eInit_2eDatatypes_2enat___24t(_511579), cColor_2egraph___24t(_511582), cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt___24t(_511585), cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2echoose___24a1(cColor_2esubset__nodes___24a2(cColor_2elow__deg___24a1(_511579), _511582)) = cCoq_2eInit_2eDatatypes_2eSome___24a2(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt, _511585), -(cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset, cColor_2eremove__node___24a2(_511585, _511582)), cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset, _511582)))], clausify('Color.select_terminates')).
% 5.81/7.63
% 5.81/7.63 cnf('1',plain,[-(cCoq_2eInit_2eDatatypes_2enat___24t(4222 ^ []))],start(1)).
% 5.81/7.63 cnf('1.1',plain,[cCoq_2eInit_2eDatatypes_2enat___24t(4222 ^ []), cColor_2egraph___24t(4223 ^ []), cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt___24t(4224 ^ []), cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2echoose___24a1(cColor_2esubset__nodes___24a2(cColor_2elow__deg___24a1(4222 ^ []), 4223 ^ [])) = cCoq_2eInit_2eDatatypes_2eSome___24a2(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt, 4224 ^ []), -(cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset, cColor_2eremove__node___24a2(4224 ^ [], 4223 ^ [])), cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset, 4223 ^ [])))],extension(6,bind([[_511579, _511585, _511582], [4222 ^ [], 4224 ^ [], 4223 ^ []]]))).
% 5.81/7.63 cnf('1.1.1',plain,[-(cColor_2egraph___24t(4223 ^ []))],extension(2)).
% 5.81/7.63 cnf('1.1.2',plain,[-(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt___24t(4224 ^ []))],extension(3)).
% 5.81/7.63 cnf('1.1.3',plain,[-(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2echoose___24a1(cColor_2esubset__nodes___24a2(cColor_2elow__deg___24a1(4222 ^ []), 4223 ^ [])) = cCoq_2eInit_2eDatatypes_2eSome___24a2(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt, 4224 ^ []))],extension(4)).
% 5.81/7.63 cnf('1.1.4',plain,[cCoq_2eInit_2ePeano_2elt___24a2(cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset, cColor_2eremove__node___24a2(4224 ^ [], 4223 ^ [])), cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2(cColor_2enodeset, 4223 ^ []))],extension(5)).
% 5.81/7.63 %-----------------------------------------------------
% 5.81/7.64
% 5.81/7.64 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------