Changes to FORPI based on reviewers comments

examples/proofs/Random Proofs/21 Nov 2016 Compressed - 22 Aug 2017/random-results-Tue Aug 22 02-44-42 EDT 2017-proof-1000-rpi-.txt

@@ -0,0 +1,172 @@
+1: { ⊢ (p103 V98), (p26 c34 V94), (p103 V0), (p102 V0)} 	: Axiom()[]
+2: { ⊢ (p26 c34 V94), (p103 V0), (p102 V0)} 	: Contraction(1)[]
+3: {(p26 V95 V96), (p26 c34 c5) ⊢ } 	: Axiom()[]
+4: {(p26 c34 c5) ⊢ } 	: Contraction(3)[]
+5: { ⊢ (p103 V0), (p102 V0)} 	: UnifyingResolution(2, 4)[]
+6: {(p103 V0) ⊢ (p104 V0 V93 V97), (p26 V97 V93)} 	: Axiom()[]
+7: {(p104 V0 V93 c34) ⊢ } 	: Axiom()[]
+8: {(p103 V0) ⊢ (p26 c34 V93)} 	: UnifyingResolution(6, 7)[]
+9: {(p103 V0) ⊢ } 	: UnifyingResolution(8, 4)[]
+10: { ⊢ (p102 V0)} 	: UnifyingResolution(5, 9)[]
+11: { ⊢ (p17 (f6 c32 c16 c18))} 	: Axiom()[]
+12: {(p17 (f6 V101 V102 V103)) ⊢ (p106 V0), (p105 V0)} 	: Axiom()[]
+13: { ⊢ (p106 V0), (p105 V0)} 	: UnifyingResolution(11, 12)[]
+14: {(p17 (f6 c32 V99 V100)), (p106 V0) ⊢ } 	: Axiom()[]
+15: {(p106 V0) ⊢ } 	: UnifyingResolution(11, 14)[]
+16: { ⊢ (p105 V0)} 	: UnifyingResolution(13, 15)[]
+17: {(p105 V0) ⊢ (p107 V0 V0), (p101 V0)} 	: Axiom()[]
+18: {(p107 V0 V0), (p102 V0) ⊢ } 	: Axiom()[]
+19: {(p105 V0), (p102 V0) ⊢ (p101 V0)} 	: UnifyingResolution(17, 18)[]
+20: {(p102 V0) ⊢ (p101 V0)} 	: UnifyingResolution(16, 19)[]
+21: { ⊢ (p101 V0)} 	: UnifyingResolution(10, 20)[]
+22: { ⊢ (p39 c36)} 	: Axiom()[]
+23: {(p39 V112) ⊢ (p111 V108 c35 V108), (p109 V108)} 	: Axiom()[]
+24: { ⊢ (p111 V108 c35 V108), (p109 V108)} 	: UnifyingResolution(22, 23)[]
+25: {(p39 V111), (p111 V108 V110 V108) ⊢ (p34 (f12 V108 V110 c19) c28)} 	: Axiom()[]
+26: {(p111 V108 V110 V108) ⊢ (p34 (f12 V108 V110 c19) c28)} 	: UnifyingResolution(22, 25)[]
+27: { ⊢ (p109 V108), (p34 (f12 V108 c35 c19) c28)} 	: UnifyingResolution(24, 26)[]
+28: {(p109 V109) ⊢ (p110 V109)} 	: Axiom()[]
+29: {(p110 c39) ⊢ } 	: Axiom()[]
+30: {(p109 c39) ⊢ } 	: UnifyingResolution(28, 29)[]
+31: { ⊢ (p34 (f12 c39 c35 c19) c28)} 	: UnifyingResolution(27, 30)[]
+32: { ⊢ (p113 c11 c8)} 	: Axiom()[]
+33: {(p113 V122 V121) ⊢ (p71 V121 V122 c1 c17)} 	: Axiom()[]
+34: { ⊢ (p71 c8 c11 c1 c17)} 	: UnifyingResolution(32, 33)[]
+35: { ⊢ (p114 V115 V114)} 	: Axiom()[]
+36: {(p114 V115 V114), (p71 V114 V115 V116 V117) ⊢ (p112 c39)} 	: Axiom()[]
+37: {(p71 V114 V115 V116 V117) ⊢ (p112 c39)} 	: UnifyingResolution(35, 36)[]
+38: { ⊢ (p112 c39)} 	: UnifyingResolution(34, 37)[]
+39: {(p34 (f12 V113 V104 c19) c28) ⊢ (p115 V113 V104 V113 V118 c8)} 	: Axiom()[]
+40: {(p115 V113 V104 V113 V118 V123), (p71 V123 V118 V119 V120), (p112 V113) ⊢ (p108 V0)} 	: Axiom()[]
+41: {(p34 (f12 V113 V104 c19) c28), (p71 c8 V118 V119 V120), (p112 V113) ⊢ (p108 V0)} 	: UnifyingResolution(39, 40)[]
+42: {(p34 (f12 V113 V104 c19) c28), (p112 V113) ⊢ (p108 V0)} 	: UnifyingResolution(34, 41)[]
+43: {(p34 (f12 c39 V104 c19) c28) ⊢ (p108 V0)} 	: UnifyingResolution(38, 42)[]
+44: { ⊢ (p108 V0)} 	: UnifyingResolution(31, 43)[]
+45: {(p108 V0) ⊢ (p118 V0 V106 V105), (p100 V0)} 	: Axiom()[]
+46: {(p118 V0 V106 V105), (p34 (f12 V105 V106 c19) V107) ⊢ (p116 V0 V0)} 	: Axiom()[]
+47: {(p108 V0), (p34 (f12 V105 V106 c19) V107) ⊢ (p100 V0), (p116 V0 V0)} 	: UnifyingResolution(45, 46)[]
+48: {(p116 V0 V0) ⊢ (p117 V0 V0)} 	: Axiom()[]
+49: {(p117 V0 V0), (p101 V0) ⊢ } 	: Axiom()[]
+50: {(p116 V0 V0), (p101 V0) ⊢ } 	: UnifyingResolution(48, 49)[]
+51: {(p34 (f12 V105 V106 c19) V107), (p108 V0), (p101 V0) ⊢ (p100 V0)} 	: UnifyingResolution(47, 50)[]
+52: {(p108 V0), (p101 V0) ⊢ (p100 V0)} 	: UnifyingResolution(31, 51)[]
+53: {(p101 V0) ⊢ (p100 V0)} 	: UnifyingResolution(44, 52)[]
+54: { ⊢ (p100 V0)} 	: UnifyingResolution(21, 53)[]
+55: { ⊢ (p70 V138 c7), (p127 V0 V0), (p96 V128 V129), (p124 V0 V0)} 	: Axiom()[]
+56: {(p70 c6 c7) ⊢ } 	: Axiom()[]
+57: { ⊢ (p127 V0 V0), (p96 V128 V129), (p124 V0 V0)} 	: UnifyingResolution(55, 56)[]
+58: {(p127 V0 V0) ⊢ (p70 c6 V137), (p120 V0)} 	: Axiom()[]
+59: {(p127 V0 V0) ⊢ (p120 V0)} 	: UnifyingResolution(58, 56)[]
+60: { ⊢ (p124 V0 V0), (p96 V128 V129), (p120 V0)} 	: UnifyingResolution(57, 59)[]
+61: { ⊢ (p14 c18 c41)} 	: Axiom()[]
+62: {(p14 c18 V132), (p96 V130 c14) ⊢ (p125 V130)} 	: Axiom()[]
+63: {(p96 V130 c14) ⊢ (p125 V130)} 	: UnifyingResolution(61, 62)[]
+64: {(p14 c18 V131), (p125 c9) ⊢ } 	: Axiom()[]
+65: {(p125 c9) ⊢ } 	: UnifyingResolution(61, 64)[]
+66: {(p96 c9 c14) ⊢ } 	: UnifyingResolution(63, 65)[]
+67: { ⊢ (p124 V0 V0), (p120 V0)} 	: UnifyingResolution(60, 66)[]
+68: { ⊢ (p2 (f4 c26) c24 c12)} 	: Axiom()[]
+69: {(p2 (f4 V133) V134 V135) ⊢ (p126 V0 V0), (p119 V0)} 	: Axiom()[]
+70: { ⊢ (p126 V0 V0), (p119 V0)} 	: UnifyingResolution(68, 69)[]
+71: {(p2 (f4 c26) V136 c12), (p126 V0 V0), (p124 V0 V0) ⊢ (p96 c9 V127)} 	: Axiom()[]
+72: {(p126 V0 V0), (p124 V0 V0) ⊢ (p96 c9 V127)} 	: UnifyingResolution(68, 71)[]
+73: {(p124 V0 V0) ⊢ (p119 V0), (p96 c9 V127)} 	: UnifyingResolution(70, 72)[]
+74: {(p124 V0 V0) ⊢ (p119 V0)} 	: UnifyingResolution(73, 66)[]
+75: { ⊢ (p120 V0), (p119 V0)} 	: UnifyingResolution(67, 74)[]
+76: {(p120 V0) ⊢ (p81 V125 V126), (p123 V0), (p121 V0)} 	: Axiom()[]
+77: {(p81 V1 V71) ⊢ } 	: Axiom()[]
+78: {(p120 V0) ⊢ (p123 V0), (p121 V0)} 	: UnifyingResolution(76, 77)[]
+79: {(p123 V0) ⊢ (p81 V1 V124)} 	: Axiom()[]
+80: {(p123 V0) ⊢ } 	: UnifyingResolution(79, 77)[]
+81: {(p120 V0) ⊢ (p121 V0)} 	: UnifyingResolution(78, 80)[]
+82: {(p121 V0) ⊢ (p122 V0)} 	: Axiom()[]
+83: {(p122 V0) ⊢ } 	: Axiom()[]
+84: {(p121 V0) ⊢ } 	: UnifyingResolution(82, 83)[]
+85: {(p120 V0) ⊢ } 	: UnifyingResolution(81, 84)[]
+86: { ⊢ (p119 V0)} 	: UnifyingResolution(75, 85)[]
+87: { ⊢ (p135 V0 V0), (p128 V0 V0)} 	: Axiom()[]
+88: {(p135 V0 V0), (p119 V0) ⊢ (p133 V0 V0)} 	: Axiom()[]
+89: {(p119 V0) ⊢ (p128 V0 V0), (p133 V0 V0)} 	: UnifyingResolution(87, 88)[]
+90: {(p133 V0 V0) ⊢ (p134 V0), (p99 V0)} 	: Axiom()[]
+91: {(p134 V0) ⊢ } 	: Axiom()[]
+92: {(p133 V0 V0) ⊢ (p99 V0)} 	: UnifyingResolution(90, 91)[]
+93: {(p119 V0) ⊢ (p128 V0 V0), (p99 V0)} 	: UnifyingResolution(89, 92)[]
+94: { ⊢ (p130 c10 c4)} 	: Axiom()[]
+95: {(p130 V146 V147) ⊢ (p51 V146 (f9 V147) c14 c22 c23)} 	: Axiom()[]
+96: { ⊢ (p51 c10 (f9 c4) c14 c22 c23)} 	: UnifyingResolution(94, 95)[]
+97: {(p51 V139 (f9 V140) c14 c22 V141) ⊢ (p131 V0 V139), (p129 V0 V0)} 	: Axiom()[]
+98: {(p131 V0 V139), (p100 V0) ⊢ } 	: Axiom()[]
+99: {(p51 V139 (f9 V140) c14 c22 V141), (p100 V0) ⊢ (p129 V0 V0)} 	: UnifyingResolution(97, 98)[]
+100: {(p100 V0) ⊢ (p129 V0 V0)} 	: UnifyingResolution(96, 99)[]
+101: {(p128 V0 V0) ⊢ (p132 V0 V0 V142)} 	: Axiom()[]
+102: {(p132 V0 V0 V142), (p51 V142 (f9 V143) V144 V145 c23), (p129 V0 V0) ⊢ } 	: Axiom()[]
+103: {(p128 V0 V0), (p51 V142 (f9 V143) V144 V145 c23), (p129 V0 V0) ⊢ } 	: UnifyingResolution(101, 102)[]
+104: {(p128 V0 V0), (p129 V0 V0) ⊢ } 	: UnifyingResolution(96, 103)[]
+105: {(p100 V0), (p128 V0 V0) ⊢ } 	: UnifyingResolution(100, 104)[]
+106: {(p119 V0), (p100 V0) ⊢ (p99 V0)} 	: UnifyingResolution(93, 105)[]
+107: {(p100 V0) ⊢ (p99 V0)} 	: UnifyingResolution(86, 106)[]
+108: { ⊢ (p99 V0)} 	: UnifyingResolution(54, 107)[]
+109: { ⊢ (p151 V0 V148 V0 V148), (p149 V0 V148 V0 V148)} 	: Axiom()[]
+110: {(p151 V0 V148 V0 V148) ⊢ (p148 V0 V148 V0)} 	: Axiom()[]
+111: { ⊢ (p149 V0 V148 V0 V148), (p148 V0 V148 V0)} 	: UnifyingResolution(109, 110)[]
+112: {(p149 V0 V148 V0 V148) ⊢ (p150 V0 V148), (p12 V148 V0)} 	: Axiom()[]
+113: {(p150 V0 V148) ⊢ } 	: Axiom()[]
+114: {(p149 V0 V148 V0 V148) ⊢ (p12 V148 V0)} 	: UnifyingResolution(112, 113)[]
+115: { ⊢ (p148 V0 V148 V0), (p12 V148 V0)} 	: UnifyingResolution(111, 114)[]
+116: {(p148 V0 V148 V0) ⊢ (p152 V0 V148 V0 V148), (p12 V156 V157), (p12 V154 V155)} 	: Axiom()[]
+117: {(p152 V0 V148 V0 V148), (p99 V0) ⊢ (p136 V0 V148)} 	: Axiom()[]
+118: {(p148 V0 V148 V0), (p99 V0) ⊢ (p12 V154 V155), (p12 V156 V157), (p136 V0 V148)} 	: UnifyingResolution(116, 117)[]
+119: {(p148 V0 V148 V0), (p99 V0) ⊢ (p12 V154 V155), (p136 V0 V148)} 	: Contraction(118)[]
+120: {(p99 V0) ⊢ (p12 V148 V0), (p12 V154 V155), (p136 V0 V148)} 	: UnifyingResolution(115, 119)[]
+121: {(p99 V0) ⊢ (p136 V0 V148), (p12 V148 V0)} 	: Contraction(120)[]
+122: { ⊢ (p140 V150 V151 V0 V153 V150), (p138 V0 V153 V150 V151)} 	: Axiom()[]
+123: {(p140 V150 V151 V0 c0 V150) ⊢ (p137 V150 V151)} 	: Axiom()[]
+124: { ⊢ (p138 V0 c0 V150 V151), (p137 V150 V151)} 	: UnifyingResolution(122, 123)[]
+125: {(p138 V0 V152 V150 V151) ⊢ (p139 V0 V152 V150), (p137 V0 V152)} 	: Axiom()[]
+126: {(p139 V0 V152 V150) ⊢ } 	: Axiom()[]
+127: {(p138 V0 V152 V150 V151) ⊢ (p137 V0 V152)} 	: UnifyingResolution(125, 126)[]
+128: { ⊢ (p137 V150 V151), (p137 V0 c0)} 	: UnifyingResolution(124, 127)[]
+129: { ⊢ (p137 V0 c0)} 	: Contraction(128)[]
+130: {(p136 V0 V149) ⊢ (p144 V0 V149 V0 V149), (p142 V0 V149)} 	: Axiom()[]
+131: {(p144 V0 V149 V0 V149) ⊢ (p141 V0 V149 V0 V149)} 	: Axiom()[]
+132: {(p136 V0 V149) ⊢ (p142 V0 V149), (p141 V0 V149 V0 V149)} 	: UnifyingResolution(130, 131)[]
+133: { ⊢ (p143 V0 V149)} 	: Axiom()[]
+134: {(p143 V0 V149), (p142 V0 V149) ⊢ } 	: Axiom()[]
+135: {(p142 V0 V149) ⊢ } 	: UnifyingResolution(133, 134)[]
+136: {(p136 V0 V149) ⊢ (p141 V0 V149 V0 V149)} 	: UnifyingResolution(132, 135)[]
+137: { ⊢ (p147 V0 V149)} 	: Axiom()[]
+138: {(p147 V0 V149), (p141 V0 V149 V0 V149) ⊢ (p145 V0 V149 V0 V149)} 	: Axiom()[]
+139: {(p141 V0 V149 V0 V149) ⊢ (p145 V0 V149 V0 V149)} 	: UnifyingResolution(137, 138)[]
+140: {(p137 V0 V149) ⊢ (p146 V0 V149 V0 V149)} 	: Axiom()[]
+141: {(p146 V0 V149 V0 V149), (p145 V0 V149 V0 V149) ⊢ } 	: Axiom()[]
+142: {(p137 V0 V149), (p145 V0 V149 V0 V149) ⊢ } 	: UnifyingResolution(140, 141)[]
+143: {(p141 V0 V149 V0 V149), (p137 V0 V149) ⊢ } 	: UnifyingResolution(139, 142)[]
+144: {(p136 V0 V149), (p137 V0 V149) ⊢ } 	: UnifyingResolution(136, 143)[]
+145: {(p136 V0 c0) ⊢ } 	: UnifyingResolution(129, 144)[]
+146: {(p99 V0) ⊢ (p12 c0 V0)} 	: UnifyingResolution(121, 145)[]
+147: { ⊢ (p12 c0 V0)} 	: UnifyingResolution(108, 146)[]
+148: { ⊢ (p39 c25)} 	: Axiom()[]
+149: {(p39 V40) ⊢ (p8 V40 V40)} 	: Axiom()[]
+150: { ⊢ (p8 c25 c25)} 	: UnifyingResolution(148, 149)[]
+151: {(p12 V32 V33) ⊢ (p41 V33 V32 V33 V39), (p34 V32 V33)} 	: Axiom()[]
+152: {(p41 V33 V32 V33 V39), (p8 V39 V39) ⊢ (p38 V33 V32)} 	: Axiom()[]
+153: {(p12 V32 V33), (p8 V39 V39) ⊢ (p34 V32 V33), (p38 V33 V32)} 	: UnifyingResolution(151, 152)[]
+154: {(p12 V32 V33) ⊢ (p34 V32 V33), (p38 V33 V32)} 	: UnifyingResolution(150, 153)[]
+155: { ⊢ (p6 c21)} 	: Axiom()[]
+156: {(p6 V41), (p8 V38 V38) ⊢ (p40 V32 V33 V38)} 	: Axiom()[]
+157: {(p8 V38 V38) ⊢ (p40 V32 V33 V38)} 	: UnifyingResolution(155, 156)[]
+158: {(p6 c21), (p40 V32 V33 V38), (p38 V33 V32) ⊢ } 	: Axiom()[]
+159: {(p40 V32 V33 V38), (p38 V33 V32) ⊢ } 	: UnifyingResolution(155, 158)[]
+160: {(p8 V38 V38), (p38 V33 V32) ⊢ } 	: UnifyingResolution(157, 159)[]
+161: {(p38 V33 V32) ⊢ } 	: UnifyingResolution(150, 160)[]
+162: {(p12 V32 V33) ⊢ (p34 V32 V33)} 	: UnifyingResolution(154, 161)[]
+163: { ⊢ (p36 c0 c30)} 	: Axiom()[]
+164: {(p36 V36 V37) ⊢ (p35 V36 V37)} 	: Axiom()[]
+165: { ⊢ (p35 c0 c30)} 	: UnifyingResolution(163, 164)[]
+166: {(p35 V34 V35) ⊢ (p37 V35 V34 V35 V34)} 	: Axiom()[]
+167: {(p37 V35 V34 V35 V34), (p34 V34 V35) ⊢ } 	: Axiom()[]
+168: {(p35 V34 V35), (p34 V34 V35) ⊢ } 	: UnifyingResolution(166, 167)[]
+169: {(p34 c0 c30) ⊢ } 	: UnifyingResolution(165, 168)[]
+170: {(p12 c0 c30) ⊢ } 	: UnifyingResolution(162, 169)[]
+171: { ⊢ } 	: UnifyingResolution(147, 170)[]
+