Definition. We define False to be ∀p : prop, p of type prop.
In Proofgold the corresponding term root is 1db705... and object id is 266ad5...
Definition. We define not to be λA : prop ⇒ A → False of type prop → prop.
In Proofgold the corresponding term root is f30435... and object id is 0dc3c7...
Notation. We use ¬ as a prefix operator with priority 700 corresponding to applying term not.
Definition. We define and to be λA B : prop ⇒ ∀p : prop, (A → B → p) → p of type prop → prop → prop.
In Proofgold the corresponding term root is 2ba7d0... and object id is 37da83...
Notation. We use ∧ as an infix operator with priority 780 and which associates to the left corresponding to applying term and.
Definition. We define or to be λA B : prop ⇒ ∀p : prop, (A → p) → (B → p) → p of type prop → prop → prop.
In Proofgold the corresponding term root is 957746... and object id is 86ae64...
Notation. We use ∨ as an infix operator with priority 785 and which associates to the left corresponding to applying term or.
Beginning of Section Eq
Variable A : SType
Definition. We define eq to be λx y : A ⇒ ∀Q : A → A → prop, Q x y → Q y x of type A → A → prop.
Definition. We define neq to be λx y : A ⇒ ¬ eq x y of type A → A → prop.
End of Section Eq
Notation. We use = as an infix operator with priority 502 and no associativity corresponding to applying term eq.
Notation. We use ≠ as an infix operator with priority 502 and no associativity corresponding to applying term neq.
Beginning of Section Ex
Variable A : SType
Definition. We define ex to be λQ : A → prop ⇒ ∀P : prop, (∀x : A, Q x → P) → P of type (A → prop) → prop.
End of Section Ex
Notation. We use ∃ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using ex.
Primitive. The name In is a term of type set → set → prop.
Notation. We use ∈ as an infix operator with priority 500 and no associativity corresponding to applying term In. Furthermore, we may write ∀ x ∈ A, B to mean ∀ x : set, x ∈ A → B.
Definition. We define Subq to be λA B ⇒ ∀x ∈ A, x ∈ B of type set → set → prop.
In Proofgold the corresponding term root is 81c0ef... and object id is 317007...
Notation. We use ⊆ as an infix operator with priority 500 and no associativity corresponding to applying term Subq. Furthermore, we may write ∀ x ⊆ A, B to mean ∀ x : set, x ⊆ A → B.
Notation. We use ∃ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using ex and handling ∈ or ⊆ ascriptions using and.
Primitive. The name 𝒫 is a term of type set → set.
Primitive. The name Empty is a term of type set.
Primitive. The name ordsucc is a term of type set → set.
In Proofgold the corresponding term root is 65d883... and object id is 1452f7...
Notation. Natural numbers 0,1,2,... are notation for the terms formed using Empty as 0 and forming successors with ordsucc.
Definition. We define bij to be λX Y f ⇒ (∀u ∈ X, f u ∈ Y) ∧ (∀u v ∈ X, f u = f v → u = v) ∧ (∀w ∈ Y, ∃u ∈ X, f u = w) of type set → set → (set → set) → prop.
In Proofgold the corresponding term root is 76bef6... and object id is f7d93b...
Definition. We define equip to be λX Y : set ⇒ ∃f : set → set, bij X Y f of type set → set → prop.
In Proofgold the corresponding term root is eb4419... and object id is 7f2bf6...
Definition. We define TwoRamseyProp to be λM N V ⇒ ∀R : set → set → prop, (∀x y, R x y → R y x) → ((∃X ⊆ V, equip M X ∧ (∀x y ∈ X, x ≠ y → R x y)) ∨ (∃Y ⊆ V, equip N Y ∧ (∀x y ∈ Y, x ≠ y → ¬ R x y))) of type set → set → set → prop.
In Proofgold the corresponding term root is c5d86c... and object id is faf73f...
Theorem. (not_TwoRamseyProp_3_3_5)
¬ TwoRamseyProp 3 3 5
In Proofgold the corresponding term root is 7e6323... and proposition id is 683750...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_3_6)
TwoRamseyProp 3 3 6
In Proofgold the corresponding term root is 52b0e2... and proposition id is 202630...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_3_4_8)
¬ TwoRamseyProp 3 4 8
In Proofgold the corresponding term root is ab5814... and proposition id is 9df0ee...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_3_5_13)
¬ TwoRamseyProp 3 5 13
In Proofgold the corresponding term root is 7e98ad... and proposition id is ae1d6a...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_3_6_17)
¬ TwoRamseyProp 3 6 17
In Proofgold the corresponding term root is 0b6b9f... and proposition id is 511201...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_3_7_22)
¬ TwoRamseyProp 3 7 22
In Proofgold the corresponding term root is 781928... and proposition id is 9e7335...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_3_8_27)
¬ TwoRamseyProp 3 8 27
In Proofgold the corresponding term root is a70f2e... and proposition id is 828bca...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_3_9_35)
¬ TwoRamseyProp 3 9 35
In Proofgold the corresponding term root is d13ea9... and proposition id is ad1c84...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_3_10_39)
¬ TwoRamseyProp 3 10 39
In Proofgold the corresponding term root is f07e7a... and proposition id is cbbd38...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_4_4_17)
¬ TwoRamseyProp 4 4 17
In Proofgold the corresponding term root is ac13dc... and proposition id is 5039e3...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_4_5_24)
¬ TwoRamseyProp 4 5 24
In Proofgold the corresponding term root is 9ca421... and proposition id is 515036...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_4_6_35)
¬ TwoRamseyProp 4 6 35
In Proofgold the corresponding term root is d40bf7... and proposition id is b7a051...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_4_7_48)
¬ TwoRamseyProp 4 7 48
In Proofgold the corresponding term root is 6fa829... and proposition id is 7db35f...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_4_8_58)
¬ TwoRamseyProp 4 8 58
In Proofgold the corresponding term root is 902a09... and proposition id is 2044fd...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_4_9_72)
¬ TwoRamseyProp 4 9 72
In Proofgold the corresponding term root is e27002... and proposition id is cecb1a...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_5_5_42)
¬ TwoRamseyProp 5 5 42
In Proofgold the corresponding term root is 719f58... and proposition id is c7463a...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_5_6_57)
¬ TwoRamseyProp 5 6 57
In Proofgold the corresponding term root is 845185... and proposition id is 580f9d...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_5_7_79)
¬ TwoRamseyProp 5 7 79
In Proofgold the corresponding term root is 527b93... and proposition id is 6a8180...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_5_8_100)
¬ TwoRamseyProp 5 8 100
In Proofgold the corresponding term root is 482b10... and proposition id is 10514b...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_6_6_101)
¬ TwoRamseyProp 6 6 101
In Proofgold the corresponding term root is 9ca7da... and proposition id is ccd3e7...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_6_7_114)
¬ TwoRamseyProp 6 7 114
In Proofgold the corresponding term root is d69655... and proposition id is d6f6b1...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_4_9)
TwoRamseyProp 3 4 9
In Proofgold the corresponding term root is d90d6a... and proposition id is 8aad15...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_5_14)
TwoRamseyProp 3 5 14
In Proofgold the corresponding term root is 3e761f... and proposition id is 9131ef...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_6_18)
TwoRamseyProp 3 6 18
In Proofgold the corresponding term root is 81b8e4... and proposition id is ab81a1...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_7_23)
TwoRamseyProp 3 7 23
In Proofgold the corresponding term root is c400bb... and proposition id is 2265c1...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_8_28)
TwoRamseyProp 3 8 28
In Proofgold the corresponding term root is afae62... and proposition id is a89eaa...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_9_36)
TwoRamseyProp 3 9 36
In Proofgold the corresponding term root is cc11e3... and proposition id is 5b30ba...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_10_42)
TwoRamseyProp 3 10 42
In Proofgold the corresponding term root is ff9a0d... and proposition id is 6f9cfa...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_4_18)
TwoRamseyProp 4 4 18
In Proofgold the corresponding term root is b1412b... and proposition id is e3dc1f...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_5_25)
TwoRamseyProp 4 5 25
In Proofgold the corresponding term root is 73be68... and proposition id is cc7495...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_6_41)
TwoRamseyProp 4 6 41
In Proofgold the corresponding term root is bb42d4... and proposition id is 8ecff7...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_7_61)
TwoRamseyProp 4 7 61
In Proofgold the corresponding term root is 5ef5f1... and proposition id is 019f14...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_8_84)
TwoRamseyProp 4 8 84
In Proofgold the corresponding term root is 8709c0... and proposition id is ae49e3...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_9_115)
TwoRamseyProp 4 9 115
In Proofgold the corresponding term root is 5a92ff... and proposition id is 0df9d6...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_5_5_48)
TwoRamseyProp 5 5 48
In Proofgold the corresponding term root is abf150... and proposition id is 4c7566...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_5_6_87)
TwoRamseyProp 5 6 87
In Proofgold the corresponding term root is 43db24... and proposition id is bfcef2...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_5_7_143)
TwoRamseyProp 5 7 143
In Proofgold the corresponding term root is 656f91... and proposition id is 67a94c...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_5_8_216)
TwoRamseyProp 5 8 216
In Proofgold the corresponding term root is 516a20... and proposition id is f57af5...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_6_6_165)
TwoRamseyProp 6 6 165
In Proofgold the corresponding term root is 10e700... and proposition id is 184bf0...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_6_7_298)
TwoRamseyProp 6 7 298
In Proofgold the corresponding term root is ea7d2e... and proposition id is 6bc284...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_3_5_Power_3)
¬ TwoRamseyProp 3 5 (𝒫 3)
In Proofgold the corresponding term root is 2e14db... and proposition id is 6bca80...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_3_6_Power_3)
¬ TwoRamseyProp 3 6 (𝒫 3)
In Proofgold the corresponding term root is edbe38... and proposition id is ff5905...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_3_6_Power_4)
¬ TwoRamseyProp 3 6 (𝒫 4)
In Proofgold the corresponding term root is 47c913... and proposition id is 4618e3...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_3_7_Power_3)
¬ TwoRamseyProp 3 7 (𝒫 3)
In Proofgold the corresponding term root is 453f42... and proposition id is 54668e...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_3_7_Power_4)
¬ TwoRamseyProp 3 7 (𝒫 4)
In Proofgold the corresponding term root is 0b06fe... and proposition id is 1d99f6...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_3_8_Power_3)
¬ TwoRamseyProp 3 8 (𝒫 3)
In Proofgold the corresponding term root is 8e31e6... and proposition id is df26ed...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_3_8_Power_4)
¬ TwoRamseyProp 3 8 (𝒫 4)
In Proofgold the corresponding term root is 7c4c3c... and proposition id is b6366b...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_3_9_Power_3)
¬ TwoRamseyProp 3 9 (𝒫 3)
In Proofgold the corresponding term root is 9579d1... and proposition id is 69d43f...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_3_9_Power_4)
¬ TwoRamseyProp 3 9 (𝒫 4)
In Proofgold the corresponding term root is a44fd9... and proposition id is f990b2...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_3_9_Power_5)
¬ TwoRamseyProp 3 9 (𝒫 5)
In Proofgold the corresponding term root is f978c0... and proposition id is 976d22...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_3_10_Power_3)
¬ TwoRamseyProp 3 10 (𝒫 3)
In Proofgold the corresponding term root is edae1d... and proposition id is 7f9092...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_3_10_Power_4)
¬ TwoRamseyProp 3 10 (𝒫 4)
In Proofgold the corresponding term root is c50224... and proposition id is a1e0f8...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_3_10_Power_5)
¬ TwoRamseyProp 3 10 (𝒫 5)
In Proofgold the corresponding term root is 1279fc... and proposition id is 0c824e...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_4_4_Power_3)
¬ TwoRamseyProp 4 4 (𝒫 3)
In Proofgold the corresponding term root is d1fac1... and proposition id is ce62b4...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_4_4_Power_4)
¬ TwoRamseyProp 4 4 (𝒫 4)
In Proofgold the corresponding term root is 1accba... and proposition id is 485cd3...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_4_5_Power_3)
¬ TwoRamseyProp 4 5 (𝒫 3)
In Proofgold the corresponding term root is efe4e3... and proposition id is fe9726...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_4_5_Power_4)
¬ TwoRamseyProp 4 5 (𝒫 4)
In Proofgold the corresponding term root is 73633b... and proposition id is 5b30ad...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_4_6_Power_3)
¬ TwoRamseyProp 4 6 (𝒫 3)
In Proofgold the corresponding term root is b0e56c... and proposition id is 33278e...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_4_6_Power_4)
¬ TwoRamseyProp 4 6 (𝒫 4)
In Proofgold the corresponding term root is 277385... and proposition id is f5ebc7...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_4_6_Power_5)
¬ TwoRamseyProp 4 6 (𝒫 5)
In Proofgold the corresponding term root is 57e1a8... and proposition id is 403921...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_4_7_Power_3)
¬ TwoRamseyProp 4 7 (𝒫 3)
In Proofgold the corresponding term root is 9b0d43... and proposition id is e18649...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_4_7_Power_4)
¬ TwoRamseyProp 4 7 (𝒫 4)
In Proofgold the corresponding term root is d0d0d1... and proposition id is a19688...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_4_7_Power_5)
¬ TwoRamseyProp 4 7 (𝒫 5)
In Proofgold the corresponding term root is ea6e80... and proposition id is 02137e...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_4_8_Power_3)
¬ TwoRamseyProp 4 8 (𝒫 3)
In Proofgold the corresponding term root is 4a26d1... and proposition id is 95a553...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_4_8_Power_4)
¬ TwoRamseyProp 4 8 (𝒫 4)
In Proofgold the corresponding term root is 219cd9... and proposition id is fa29be...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_4_8_Power_5)
¬ TwoRamseyProp 4 8 (𝒫 5)
In Proofgold the corresponding term root is 18bbd7... and proposition id is e31cbf...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_4_9_Power_3)
¬ TwoRamseyProp 4 9 (𝒫 3)
In Proofgold the corresponding term root is 998ace... and proposition id is 8b7695...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_4_9_Power_4)
¬ TwoRamseyProp 4 9 (𝒫 4)
In Proofgold the corresponding term root is 630214... and proposition id is 5914c2...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_4_9_Power_5)
¬ TwoRamseyProp 4 9 (𝒫 5)
In Proofgold the corresponding term root is 9b8168... and proposition id is 0100d5...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_4_9_Power_6)
¬ TwoRamseyProp 4 9 (𝒫 6)
In Proofgold the corresponding term root is ab00f3... and proposition id is aaf471...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_5_5_Power_3)
¬ TwoRamseyProp 5 5 (𝒫 3)
In Proofgold the corresponding term root is b77097... and proposition id is cd2fd6...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_5_5_Power_4)
¬ TwoRamseyProp 5 5 (𝒫 4)
In Proofgold the corresponding term root is c835f4... and proposition id is 1ef3ea...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_5_5_Power_5)
¬ TwoRamseyProp 5 5 (𝒫 5)
In Proofgold the corresponding term root is ce5e33... and proposition id is 181da7...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_5_6_Power_3)
¬ TwoRamseyProp 5 6 (𝒫 3)
In Proofgold the corresponding term root is cc9745... and proposition id is eff2ca...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_5_6_Power_4)
¬ TwoRamseyProp 5 6 (𝒫 4)
In Proofgold the corresponding term root is 5bd107... and proposition id is c0836f...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_5_6_Power_5)
¬ TwoRamseyProp 5 6 (𝒫 5)
In Proofgold the corresponding term root is 1aa41b... and proposition id is 5c1220...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_5_7_Power_3)
¬ TwoRamseyProp 5 7 (𝒫 3)
In Proofgold the corresponding term root is 1c506f... and proposition id is 73405e...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_5_7_Power_4)
¬ TwoRamseyProp 5 7 (𝒫 4)
In Proofgold the corresponding term root is 9229f6... and proposition id is c6b256...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_5_7_Power_5)
¬ TwoRamseyProp 5 7 (𝒫 5)
In Proofgold the corresponding term root is 3a7b9b... and proposition id is c9771a...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_5_7_Power_6)
¬ TwoRamseyProp 5 7 (𝒫 6)
In Proofgold the corresponding term root is 63d422... and proposition id is 5b9e15...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_5_8_Power_3)
¬ TwoRamseyProp 5 8 (𝒫 3)
In Proofgold the corresponding term root is 87e3ca... and proposition id is 419786...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_5_8_Power_4)
¬ TwoRamseyProp 5 8 (𝒫 4)
In Proofgold the corresponding term root is 3b8817... and proposition id is f4df6c...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_5_8_Power_5)
¬ TwoRamseyProp 5 8 (𝒫 5)
In Proofgold the corresponding term root is 4630a8... and proposition id is 6f401a...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_5_8_Power_6)
¬ TwoRamseyProp 5 8 (𝒫 6)
In Proofgold the corresponding term root is 659e09... and proposition id is cd9fa7...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_6_6_Power_3)
¬ TwoRamseyProp 6 6 (𝒫 3)
In Proofgold the corresponding term root is 7675d8... and proposition id is 3de2e9...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_6_6_Power_4)
¬ TwoRamseyProp 6 6 (𝒫 4)
In Proofgold the corresponding term root is 1e8eab... and proposition id is 3ce96f...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_6_6_Power_5)
¬ TwoRamseyProp 6 6 (𝒫 5)
In Proofgold the corresponding term root is 0b03aa... and proposition id is 4f8d9a...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_6_6_Power_6)
¬ TwoRamseyProp 6 6 (𝒫 6)
In Proofgold the corresponding term root is 7369ec... and proposition id is 129ce3...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_6_7_Power_3)
¬ TwoRamseyProp 6 7 (𝒫 3)
In Proofgold the corresponding term root is f4f107... and proposition id is 84f84f...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_6_7_Power_4)
¬ TwoRamseyProp 6 7 (𝒫 4)
In Proofgold the corresponding term root is 045e6f... and proposition id is c642e7...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_6_7_Power_5)
¬ TwoRamseyProp 6 7 (𝒫 5)
In Proofgold the corresponding term root is 8e2596... and proposition id is 404dff...
Proof:
The rest of the proof is missing.

Theorem. (not_TwoRamseyProp_6_7_Power_6)
¬ TwoRamseyProp 6 7 (𝒫 6)
In Proofgold the corresponding term root is 77aa69... and proposition id is 65eeb0...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_4_Power_4)
TwoRamseyProp 3 4 (𝒫 4)
In Proofgold the corresponding term root is 69f73a... and proposition id is 6b5452...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_4_Power_5)
TwoRamseyProp 3 4 (𝒫 5)
In Proofgold the corresponding term root is 424e90... and proposition id is d31094...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_4_Power_6)
TwoRamseyProp 3 4 (𝒫 6)
In Proofgold the corresponding term root is a47766... and proposition id is 49eee6...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_4_Power_7)
TwoRamseyProp 3 4 (𝒫 7)
In Proofgold the corresponding term root is 12cd06... and proposition id is 1c6e1a...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_4_Power_8)
TwoRamseyProp 3 4 (𝒫 8)
In Proofgold the corresponding term root is 08f55d... and proposition id is ec12e9...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_5_Power_4)
TwoRamseyProp 3 5 (𝒫 4)
In Proofgold the corresponding term root is 2f03fa... and proposition id is 18babb...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_5_Power_5)
TwoRamseyProp 3 5 (𝒫 5)
In Proofgold the corresponding term root is 44db1f... and proposition id is 0d1dae...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_5_Power_6)
TwoRamseyProp 3 5 (𝒫 6)
In Proofgold the corresponding term root is 852693... and proposition id is 4f6e8c...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_5_Power_7)
TwoRamseyProp 3 5 (𝒫 7)
In Proofgold the corresponding term root is 9603e0... and proposition id is 761361...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_5_Power_8)
TwoRamseyProp 3 5 (𝒫 8)
In Proofgold the corresponding term root is 2cd0df... and proposition id is 7253f9...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_6_Power_5)
TwoRamseyProp 3 6 (𝒫 5)
In Proofgold the corresponding term root is fd92fd... and proposition id is 832803...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_6_Power_6)
TwoRamseyProp 3 6 (𝒫 6)
In Proofgold the corresponding term root is 579b84... and proposition id is 8f331d...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_6_Power_7)
TwoRamseyProp 3 6 (𝒫 7)
In Proofgold the corresponding term root is e9d8bf... and proposition id is eb9268...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_6_Power_8)
TwoRamseyProp 3 6 (𝒫 8)
In Proofgold the corresponding term root is 270620... and proposition id is 9b67a5...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_7_Power_5)
TwoRamseyProp 3 7 (𝒫 5)
In Proofgold the corresponding term root is 9b6110... and proposition id is eb1da3...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_7_Power_6)
TwoRamseyProp 3 7 (𝒫 6)
In Proofgold the corresponding term root is 3243c9... and proposition id is 50f801...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_7_Power_7)
TwoRamseyProp 3 7 (𝒫 7)
In Proofgold the corresponding term root is 6158c2... and proposition id is e94f44...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_7_Power_8)
TwoRamseyProp 3 7 (𝒫 8)
In Proofgold the corresponding term root is f84df8... and proposition id is 2562e3...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_8_Power_5)
TwoRamseyProp 3 8 (𝒫 5)
In Proofgold the corresponding term root is d27407... and proposition id is 736840...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_8_Power_6)
TwoRamseyProp 3 8 (𝒫 6)
In Proofgold the corresponding term root is 033604... and proposition id is b54fd3...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_8_Power_7)
TwoRamseyProp 3 8 (𝒫 7)
In Proofgold the corresponding term root is a8d43b... and proposition id is 8c0bd9...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_8_Power_8)
TwoRamseyProp 3 8 (𝒫 8)
In Proofgold the corresponding term root is dd4496... and proposition id is fb3a49...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_9_Power_6)
TwoRamseyProp 3 9 (𝒫 6)
In Proofgold the corresponding term root is ad7806... and proposition id is f15c1f...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_9_Power_7)
TwoRamseyProp 3 9 (𝒫 7)
In Proofgold the corresponding term root is 35f644... and proposition id is 05bae7...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_9_Power_8)
TwoRamseyProp 3 9 (𝒫 8)
In Proofgold the corresponding term root is 5c35dd... and proposition id is 1dda3f...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_10_Power_6)
TwoRamseyProp 3 10 (𝒫 6)
In Proofgold the corresponding term root is 52f5ab... and proposition id is 8d9bb9...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_10_Power_7)
TwoRamseyProp 3 10 (𝒫 7)
In Proofgold the corresponding term root is 33f2cb... and proposition id is 5b8f6d...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_10_Power_8)
TwoRamseyProp 3 10 (𝒫 8)
In Proofgold the corresponding term root is d1c9f7... and proposition id is 637fa7...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_4_Power_5)
TwoRamseyProp 4 4 (𝒫 5)
In Proofgold the corresponding term root is 05e5d9... and proposition id is 6008ae...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_4_Power_6)
TwoRamseyProp 4 4 (𝒫 6)
In Proofgold the corresponding term root is 1a64a6... and proposition id is 511cf1...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_4_Power_7)
TwoRamseyProp 4 4 (𝒫 7)
In Proofgold the corresponding term root is b40f3a... and proposition id is 391315...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_4_Power_8)
TwoRamseyProp 4 4 (𝒫 8)
In Proofgold the corresponding term root is 75c916... and proposition id is f7b3e4...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_5_Power_5)
TwoRamseyProp 4 5 (𝒫 5)
In Proofgold the corresponding term root is 503a90... and proposition id is e75c1c...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_5_Power_6)
TwoRamseyProp 4 5 (𝒫 6)
In Proofgold the corresponding term root is a8740b... and proposition id is b2de67...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_5_Power_7)
TwoRamseyProp 4 5 (𝒫 7)
In Proofgold the corresponding term root is f54562... and proposition id is c33473...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_5_Power_8)
TwoRamseyProp 4 5 (𝒫 8)
In Proofgold the corresponding term root is d89be6... and proposition id is 2bb9ef...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_6_Power_6)
TwoRamseyProp 4 6 (𝒫 6)
In Proofgold the corresponding term root is a518e8... and proposition id is 1e5e44...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_6_Power_7)
TwoRamseyProp 4 6 (𝒫 7)
In Proofgold the corresponding term root is ad7270... and proposition id is 38245a...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_6_Power_8)
TwoRamseyProp 4 6 (𝒫 8)
In Proofgold the corresponding term root is 941028... and proposition id is d76fcb...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_7_Power_6)
TwoRamseyProp 4 7 (𝒫 6)
In Proofgold the corresponding term root is bc5303... and proposition id is 0ea3e8...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_7_Power_7)
TwoRamseyProp 4 7 (𝒫 7)
In Proofgold the corresponding term root is 1b726b... and proposition id is e53402...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_7_Power_8)
TwoRamseyProp 4 7 (𝒫 8)
In Proofgold the corresponding term root is bf3f21... and proposition id is c5000f...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_8_Power_7)
TwoRamseyProp 4 8 (𝒫 7)
In Proofgold the corresponding term root is 7a12f6... and proposition id is 8fd18b...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_8_Power_8)
TwoRamseyProp 4 8 (𝒫 8)
In Proofgold the corresponding term root is 08eff5... and proposition id is 67bf86...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_9_Power_7)
TwoRamseyProp 4 9 (𝒫 7)
In Proofgold the corresponding term root is e4ef51... and proposition id is 75d1df...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_9_Power_8)
TwoRamseyProp 4 9 (𝒫 8)
In Proofgold the corresponding term root is c710f2... and proposition id is 262f11...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_5_5_Power_6)
TwoRamseyProp 5 5 (𝒫 6)
In Proofgold the corresponding term root is 8b9837... and proposition id is 921240...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_5_5_Power_7)
TwoRamseyProp 5 5 (𝒫 7)
In Proofgold the corresponding term root is 35cb87... and proposition id is fa2986...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_5_5_Power_8)
TwoRamseyProp 5 5 (𝒫 8)
In Proofgold the corresponding term root is e6c870... and proposition id is 5a0aee...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_5_6_Power_7)
TwoRamseyProp 5 6 (𝒫 7)
In Proofgold the corresponding term root is 2d548a... and proposition id is 4005bf...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_5_6_Power_8)
TwoRamseyProp 5 6 (𝒫 8)
In Proofgold the corresponding term root is 3e3542... and proposition id is 5b6f13...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_5_7_Power_8)
TwoRamseyProp 5 7 (𝒫 8)
In Proofgold the corresponding term root is e2647f... and proposition id is c6e221...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_5_8_Power_8)
TwoRamseyProp 5 8 (𝒫 8)
In Proofgold the corresponding term root is 384300... and proposition id is 31b50b...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_6_6_Power_8)
TwoRamseyProp 6 6 (𝒫 8)
In Proofgold the corresponding term root is 447712... and proposition id is c30d48...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_10_40)
TwoRamseyProp 3 10 40
In Proofgold the corresponding term root is 819cb8... and proposition id is f3e4ef...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_3_10_41)
TwoRamseyProp 3 10 41
In Proofgold the corresponding term root is 2f991f... and proposition id is 47305a...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_6_36)
TwoRamseyProp 4 6 36
In Proofgold the corresponding term root is ecf55c... and proposition id is 9cb5e1...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_6_40)
TwoRamseyProp 4 6 40
In Proofgold the corresponding term root is cca9c8... and proposition id is 130f84...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_7_49)
TwoRamseyProp 4 7 49
In Proofgold the corresponding term root is 339a49... and proposition id is 9a8e3c...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_7_60)
TwoRamseyProp 4 7 60
In Proofgold the corresponding term root is b0a10d... and proposition id is 937b9a...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_8_59)
TwoRamseyProp 4 8 59
In Proofgold the corresponding term root is a4013a... and proposition id is 750bb8...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_8_83)
TwoRamseyProp 4 8 83
In Proofgold the corresponding term root is ef7fe9... and proposition id is faf2bb...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_9_73)
TwoRamseyProp 4 9 73
In Proofgold the corresponding term root is eb38e5... and proposition id is 0b30c5...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_4_9_114)
TwoRamseyProp 4 9 114
In Proofgold the corresponding term root is 875b53... and proposition id is beb3ce...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_5_5_43)
TwoRamseyProp 5 5 43
In Proofgold the corresponding term root is fa1f88... and proposition id is e5b639...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_5_5_47)
TwoRamseyProp 5 5 47
In Proofgold the corresponding term root is e26c1c... and proposition id is e11650...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_5_6_58)
TwoRamseyProp 5 6 58
In Proofgold the corresponding term root is c460b3... and proposition id is b51440...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_5_6_86)
TwoRamseyProp 5 6 86
In Proofgold the corresponding term root is 9d293f... and proposition id is dba4bd...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_5_7_80)
TwoRamseyProp 5 7 80
In Proofgold the corresponding term root is 6ec438... and proposition id is c8d15a...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_5_7_142)
TwoRamseyProp 5 7 142
In Proofgold the corresponding term root is cb2ea4... and proposition id is 89daf3...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_5_8_101)
TwoRamseyProp 5 8 101
In Proofgold the corresponding term root is 83ea87... and proposition id is 11f946...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_5_8_215)
TwoRamseyProp 5 8 215
In Proofgold the corresponding term root is 5d1e89... and proposition id is 3f0856...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_6_6_102)
TwoRamseyProp 6 6 102
In Proofgold the corresponding term root is d70e2c... and proposition id is 13553e...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_6_6_164)
TwoRamseyProp 6 6 164
In Proofgold the corresponding term root is 1db0b3... and proposition id is 54fb46...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_6_7_115)
TwoRamseyProp 6 7 115
In Proofgold the corresponding term root is 814a85... and proposition id is 9c5ae9...
Proof:
The rest of the proof is missing.

Theorem. (TwoRamseyProp_6_7_297)
TwoRamseyProp 6 7 297
In Proofgold the corresponding term root is 33269e... and proposition id is bb403e...
Proof:
The rest of the proof is missing.