%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SEV608+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n022.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:56:00 PM UTC 2026
% Result : Theorem 0.98s 1.17s
% Output : Proof 1.26s
% 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.12 % Command : run_E %s %d THM
% 0.14/0.32 % Computer : n022.cluster.edu
% 0.14/0.32 % Model : x86_64 x86_64
% 0.14/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.32 % Memory : 8042.1875MB
% 0.14/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % WCLimit : 300
% 0.14/0.33 % DateTime : Tue May 5 05:26:22 EDT 2026
% 0.14/0.33 % CPUTime :
% 0.98/1.17 % SZS status Theorem
% 0.98/1.17 % SZS output start Proof
% 0.98/1.17 tff(cCoq_2eInit_2eDatatypes_2eSome___24a2_type, type, (
% 0.98/1.17 cCoq_2eInit_2eDatatypes_2eSome___24a2: ( $i * $i ) > $i)).
% 0.98/1.17 tff(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt_type, type, (
% 0.98/1.17 cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt: $i)).
% 0.98/1.17 tff(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2echoose___24a1_type, type, (
% 0.98/1.17 cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2echoose___24a1: $i > $i)).
% 0.98/1.17 tff(cColor_2esubset__nodes___24a2_type, type, (
% 0.98/1.17 cColor_2esubset__nodes___24a2: ( $i * $i ) > $i)).
% 0.98/1.17 tff(cColor_2elow__deg___24a1_type, type, (
% 0.98/1.17 cColor_2elow__deg___24a1: $i > $i)).
% 0.98/1.17 tff(cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt___24t_type, type, (
% 0.98/1.17 cCoq_2eFSets_2eFSetPositive_2ePositiveSet_2eelt___24t: $i > $o)).
% 0.98/1.17 tff(cCoq_2eInit_2ePeano_2elt___24a2_type, type, (
% 0.98/1.17 cCoq_2eInit_2ePeano_2elt___24a2: ( $i * $i ) > $o)).
% 0.98/1.17 tff(cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2_type, type, (
% 0.98/1.17 cCoq_2eFSets_2eFMapPositive_2ePositiveMap_2ecardinal___24a2: ( $i * $i ) > $i)).
% 0.98/1.17 tff(cColor_2enodeset_type, type, (
% 0.98/1.17 cColor_2enodeset: $i)).
% 0.98/1.17 tff(cColor_2eremove__node___24a2_type, type, (
% 0.98/1.17 cColor_2eremove__node___24a2: ( $i * $i ) > $i)).
% 0.98/1.17 tff(cColor_2egraph___24t_type, type, (
% 0.98/1.17 cColor_2egraph___24t: $i > $o)).
% 0.98/1.17 tff(cCoq_2eInit_2eDatatypes_2enat___24t_type, type, (
% 0.98/1.17 cCoq_2eInit_2eDatatypes_2enat___24t: $i > $o)).
% 0.98/1.17 tff(1,plain,
% 0.98/1.17 ((~![V0__K: $i] : (cCoq_2eInit_2eDatatypes_2enat___24t(V0__K) => ![V1__g: $i] : (cColor_2egraph___24t(V1__g) => ![V2__n: $i] : (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))))))) <=> (~![V0__K: $i] : ((~cCoq_2eInit_2eDatatypes_2enat___24t(V0__K)) | ![V1__g: $i] : ((~cColor_2egraph___24t(V1__g)) | ![V2__n: $i] : (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)) | (~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)))))))),
% 0.98/1.17 inference(rewrite,[status(thm)],[])).
% 0.98/1.17 tff(2,axiom,(~![V0__K: $i] : (cCoq_2eInit_2eDatatypes_2enat___24t(V0__K) => ![V1__g: $i] : (cColor_2egraph___24t(V1__g) => ![V2__n: $i] : (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'')).
% 0.98/1.17 tff(3,plain,
% 0.98/1.17 (~![V0__K: $i] : ((~cCoq_2eInit_2eDatatypes_2enat___24t(V0__K)) | ![V1__g: $i] : ((~cColor_2egraph___24t(V1__g)) | ![V2__n: $i] : (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)) | (~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))))))),
% 0.98/1.17 inference(modus_ponens,[status(thm)],[2, 1])).
% 0.98/1.17 tff(4,plain,
% 0.98/1.17 (^[V0__K: $i] : trans(monotonicity(quant_intro(proof_bind(^[V1__g: $i] : trans(monotonicity(quant_intro(proof_bind(^[V2__n: $i] : trans(monotonicity(rewrite(((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))) <=> ((~(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)))), ((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)))) <=> (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)))))), rewrite((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)))) <=> (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)) | (~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_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)))) <=> (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)) | (~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))))))), (![V2__n: $i] : (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)))) <=> ![V2__n: $i] : (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)) | (~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)))))), ((cColor_2egraph___24t(V1__g) => ![V2__n: $i] : (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))))) <=> (cColor_2egraph___24t(V1__g) => ![V2__n: $i] : (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)) | (~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))))))), rewrite((cColor_2egraph___24t(V1__g) => ![V2__n: $i] : (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)) | (~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))))) <=> ((~cColor_2egraph___24t(V1__g)) | ![V2__n: $i] : (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)) | (~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)))))), ((cColor_2egraph___24t(V1__g) => ![V2__n: $i] : (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))))) <=> ((~cColor_2egraph___24t(V1__g)) | ![V2__n: $i] : (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)) | (~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)))))))), (![V1__g: $i] : (cColor_2egraph___24t(V1__g) => ![V2__n: $i] : (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))))) <=> ![V1__g: $i] : ((~cColor_2egraph___24t(V1__g)) | ![V2__n: $i] : (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)) | (~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_2eDatatypes_2enat___24t(V0__K) => ![V1__g: $i] : (cColor_2egraph___24t(V1__g) => ![V2__n: $i] : (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)))))) <=> (cCoq_2eInit_2eDatatypes_2enat___24t(V0__K) => ![V1__g: $i] : ((~cColor_2egraph___24t(V1__g)) | ![V2__n: $i] : (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)) | (~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)))))))), rewrite((cCoq_2eInit_2eDatatypes_2enat___24t(V0__K) => ![V1__g: $i] : ((~cColor_2egraph___24t(V1__g)) | ![V2__n: $i] : (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)) | (~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_2eDatatypes_2enat___24t(V0__K)) | ![V1__g: $i] : ((~cColor_2egraph___24t(V1__g)) | ![V2__n: $i] : (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)) | (~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_2eDatatypes_2enat___24t(V0__K) => ![V1__g: $i] : (cColor_2egraph___24t(V1__g) => ![V2__n: $i] : (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)))))) <=> ((~cCoq_2eInit_2eDatatypes_2enat___24t(V0__K)) | ![V1__g: $i] : ((~cColor_2egraph___24t(V1__g)) | ![V2__n: $i] : (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)) | (~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))))))))),
% 0.98/1.17 inference(bind,[status(th)],[])).
% 0.98/1.17 tff(5,plain,
% 0.98/1.17 (![V0__K: $i] : (cCoq_2eInit_2eDatatypes_2enat___24t(V0__K) => ![V1__g: $i] : (cColor_2egraph___24t(V1__g) => ![V2__n: $i] : (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)))))) <=> ![V0__K: $i] : ((~cCoq_2eInit_2eDatatypes_2enat___24t(V0__K)) | ![V1__g: $i] : ((~cColor_2egraph___24t(V1__g)) | ![V2__n: $i] : (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)) | (~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))))))),
% 0.98/1.17 inference(quant_intro,[status(thm)],[4])).
% 0.98/1.17 tff(6,axiom,(![V0__K: $i] : (cCoq_2eInit_2eDatatypes_2enat___24t(V0__K) => ![V1__g: $i] : (cColor_2egraph___24t(V1__g) => ![V2__n: $i] : (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'')).
% 1.26/1.42 tff(7,plain,
% 1.26/1.42 (![V0__K: $i] : ((~cCoq_2eInit_2eDatatypes_2enat___24t(V0__K)) | ![V1__g: $i] : ((~cColor_2egraph___24t(V1__g)) | ![V2__n: $i] : (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)) | (~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))))))),
% 1.26/1.42 inference(modus_ponens,[status(thm)],[6, 5])).
% 1.26/1.42 tff(8,plain,
% 1.26/1.42 ($false),
% 1.26/1.42 inference(unit_resolution,[status(thm)],[7, 3])).
% 1.26/1.42 % SZS output end Proof
% 1.26/1.43 % E exiting
%------------------------------------------------------------------------------