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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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.