----- Prover9 July-2005C, 7 July 2005 ----- Process 1252 was started by amdus on vam1627, Wed Jul 13 01:20:11 2005 The command was "bin/prover9 -f inconsistent502.in". % Reading from file inconsistent502.in set(auto). % set(auto) -> set(auto1). % set(auto1) -> set(auto_inference). % set(auto1) -> set(fof_reduction). % set(auto1) -> set(predicate_elimination). % set(auto1) -> set(unfold_eq). % set(unfold_eq) -> assign(unfold_eq_limit, 2147483647). % set(unfold_eq) -> clear(fold_eq). % set(auto1) -> set(inverse_order). % set(auto1) -> assign(new_constants, 1). % assign(new_constants, 1) -> clear(x_proofs). % assign(new_constants, 1) -> clear(rx_proofs). % set(auto1) -> assign(lex_dep_demod_lim, 11). % set(auto1) -> set(lex_dep_demod_sane). % set(auto1) -> assign(max_weight, 100). % set(auto1) -> assign(age_part, 1). % set(auto1) -> assign(weight_part, 2). % set(auto1) -> assign(weight_neg_part, 2). % set(auto1) -> assign(sos_limit, 10000). % set(auto1) -> clear(x_proofs). % set(auto1) -> assign(stats, lots). % set(auto1) -> assign(max_megs, 200). % set(auto1) -> clear(clocks). formulas(sos). e_t = e_plus4 | e_t = e_plus3 | e_t = e_plus9. e_t = e_plus4 | e_t = e_plus3 | e_t = e_plus6. e_t = e_minus9 | e_t = e_plus4 | e_t = e_plus3. e_t = e_minus7 | e_t = e_plus9 | e_t = e_plus5. e_t = e_plus2 | e_t = e_minus1 | e_t = e_plus4. e_t = e_plus8 | e_t = e_minus4 | e_t = e_plus2. e_t = e_plus4 | e_t = e_plus1 | e_t = e_plus3. e_t = e_plus5 | e_t = e_plus2 | e_t = e_plus9. e_t = e_plus6 | e_t = e_minus7 | e_t = e_minus8. e_t = e_minus2 | e_t = e_minus3 | e_t = e_plus1. e_t = e_minus6 | e_t = e_plus1 | e_t = e_minus9. e_t = e_minus4 | e_t = e_plus1 | e_t = e_plus9. e_t = e_plus6 | e_t = e_minus2 | e_t = e_plus9. e_t = e_minus7 | e_t = e_minus3 | e_t = e_minus4. e_t = e_minus3 | e_t = e_plus6 | e_t = e_minus4. e_t = e_plus8 | e_t = e_minus7 | e_t = e_plus3. e_t = e_plus7 | e_t = e_minus9 | e_t = e_minus2. e_t = e_minus9 | e_t = e_minus4 | e_t = e_minus8. e_t = e_plus9 | e_t = e_minus4 | e_t = e_plus5. e_t = e_plus4 | e_t = e_minus8 | e_t = e_plus6. e_t = e_plus2 | e_t = e_minus5 | e_t = e_minus7. e_t = e_plus6 | e_t = e_minus4 | e_t = e_minus1. e_t = e_plus4 | e_t = e_minus6 | e_t = e_minus2. e_t = e_plus4 | e_t = e_plus6 | e_t = e_minus5. e_t = e_plus1 | e_t = e_minus4 | e_t = e_minus6. e_t = e_plus8 | e_t = e_minus4 | e_t = e_plus6. e_t = e_minus4 | e_t = e_plus9 | e_t = e_minus8. e_t = e_plus6 | e_t = e_minus2 | e_t = e_minus7. e_t = e_minus3 | e_t = e_plus8 | e_t = e_plus7. e_t = e_plus1 | e_t = e_plus9 | e_t = e_minus6. e_t = e_minus9 | e_t = e_plus3 | e_t = e_minus2. e_t = e_plus2 | e_t = e_plus1 | e_t = e_minus6. e_t = e_minus8 | e_t = e_minus2 | e_t = e_plus3. e_t = e_plus9 | e_t = e_minus8 | e_t = e_plus3. e_t = e_plus1 | e_t = e_plus7 | e_t = e_plus4. e_t = e_plus7 | e_t = e_minus4 | e_t = e_plus9. e_t = e_minus7 | e_t = e_minus6 | e_t = e_plus9. e_t = e_plus6 | e_t = e_plus3 | e_t = e_minus4. e_t = e_minus5 | e_t = e_plus3 | e_t = e_minus9. e_t = e_minus3 | e_t = e_plus8 | e_t = e_plus2. e_t = e_minus5 | e_t = e_minus2 | e_t = e_minus9. e_t = e_plus1 | e_t = e_plus2 | e_t = e_minus4. e_t = e_minus5 | e_t = e_plus8 | e_t = e_plus7. e_t = e_minus8 | e_t = e_minus5 | e_t = e_minus3. e_t = e_minus3 | e_t = e_plus5 | e_t = e_minus8. e_plus1 != e_minus1. e_plus2 != e_minus2. e_plus3 != e_minus3. e_plus4 != e_minus4. e_plus5 != e_minus5. e_plus6 != e_minus6. e_plus7 != e_minus7. e_plus8 != e_minus8. e_plus9 != e_minus9. end_of_list. % Finished reading the input. % Attempting problem reduction; original problem has = <199,54>. % Fid_call limit; jumping home. % Problem reduction (17.43 seconds) failed; reverting to ordinary search. % Entering prover search function. % Assigned IDs to 54 clauses. % Predicate elimination: (none). % Relation symbol precedence: lex([ = ]). % Function symbol precedence: lex([ e_t, e_minus4, e_plus9, e_plus3, e_plus6, e_plus1, e_plus4, e_minus2, e_minus8, e_minus3, e_minus7, e_minus9, e_plus2, e_minus5, e_minus6, e_plus8, e_plus7, e_plus5, e_minus1 ]). % After inverse_order: % Function symbol precedence: lex([ e_t, e_minus4, e_plus9, e_plus3, e_plus6, e_plus1, e_plus4, e_minus2, e_minus8, e_minus3, e_minus7, e_minus9, e_plus2, e_minus5, e_minus6, e_plus8, e_plus7, e_plus5, e_minus1 ]). % Unfolding symbols: (none). % Auto inference settings: % set(paramodulation). % (positive equality literals) % set(paramodulation) -> set(back_demod). % set(binary_resolution). % (non-Horn) % set(neg_ur_resolution). % (less than 100 clauses) % Reasonable options, based on the structure of the clauses: % set(factor), because non-Horn % set(back_unit_deletion), because non-Horn % set(back_unit_deletion) -> set(unit_deletion). % Clauses after input processing: clauses(usable). end_of_list. clauses(sos). 55 e_plus4 = e_t | e_plus3 = e_t | e_plus9 = e_t. [clausify] 56 e_plus4 = e_t | e_plus3 = e_t | e_plus6 = e_t. [clausify] 57 e_minus9 = e_t | e_plus4 = e_t | e_plus3 = e_t. [clausify] 58 e_minus7 = e_t | e_plus9 = e_t | e_plus5 = e_t. [clausify] 59 e_plus2 = e_t | e_minus1 = e_t | e_plus4 = e_t. [clausify] 60 e_plus8 = e_t | e_minus4 = e_t | e_plus2 = e_t. [clausify] 61 e_plus4 = e_t | e_plus1 = e_t | e_plus3 = e_t. [clausify] 62 e_plus5 = e_t | e_plus2 = e_t | e_plus9 = e_t. [clausify] 63 e_plus6 = e_t | e_minus7 = e_t | e_minus8 = e_t. [clausify] 64 e_minus2 = e_t | e_minus3 = e_t | e_plus1 = e_t. [clausify] 65 e_minus6 = e_t | e_plus1 = e_t | e_minus9 = e_t. [clausify] 66 e_minus4 = e_t | e_plus1 = e_t | e_plus9 = e_t. [clausify] 67 e_plus6 = e_t | e_minus2 = e_t | e_plus9 = e_t. [clausify] 68 e_minus7 = e_t | e_minus3 = e_t | e_minus4 = e_t. [clausify] 69 e_minus3 = e_t | e_plus6 = e_t | e_minus4 = e_t. [clausify] 70 e_plus8 = e_t | e_minus7 = e_t | e_plus3 = e_t. [clausify] 71 e_plus7 = e_t | e_minus9 = e_t | e_minus2 = e_t. [clausify] 72 e_minus9 = e_t | e_minus4 = e_t | e_minus8 = e_t. [clausify] 73 e_plus9 = e_t | e_minus4 = e_t | e_plus5 = e_t. [clausify] 74 e_plus4 = e_t | e_minus8 = e_t | e_plus6 = e_t. [clausify] 75 e_plus2 = e_t | e_minus5 = e_t | e_minus7 = e_t. [clausify] 76 e_plus6 = e_t | e_minus4 = e_t | e_minus1 = e_t. [clausify] 77 e_plus4 = e_t | e_minus6 = e_t | e_minus2 = e_t. [clausify] 78 e_plus4 = e_t | e_plus6 = e_t | e_minus5 = e_t. [clausify] 79 e_plus1 = e_t | e_minus4 = e_t | e_minus6 = e_t. [clausify] 80 e_plus8 = e_t | e_minus4 = e_t | e_plus6 = e_t. [clausify] 81 e_minus4 = e_t | e_plus9 = e_t | e_minus8 = e_t. [clausify] 82 e_plus6 = e_t | e_minus2 = e_t | e_minus7 = e_t. [clausify] 83 e_minus3 = e_t | e_plus8 = e_t | e_plus7 = e_t. [clausify] 84 e_plus1 = e_t | e_plus9 = e_t | e_minus6 = e_t. [clausify] 85 e_minus9 = e_t | e_plus3 = e_t | e_minus2 = e_t. [clausify] 86 e_plus2 = e_t | e_plus1 = e_t | e_minus6 = e_t. [clausify] 87 e_minus8 = e_t | e_minus2 = e_t | e_plus3 = e_t. [clausify] 88 e_plus9 = e_t | e_minus8 = e_t | e_plus3 = e_t. [clausify] 89 e_plus1 = e_t | e_plus7 = e_t | e_plus4 = e_t. [clausify] 90 e_plus7 = e_t | e_minus4 = e_t | e_plus9 = e_t. [clausify] 91 e_minus7 = e_t | e_minus6 = e_t | e_plus9 = e_t. [clausify] 92 e_plus6 = e_t | e_plus3 = e_t | e_minus4 = e_t. [clausify] 93 e_minus5 = e_t | e_plus3 = e_t | e_minus9 = e_t. [clausify] 94 e_minus3 = e_t | e_plus8 = e_t | e_plus2 = e_t. [clausify] 95 e_minus5 = e_t | e_minus2 = e_t | e_minus9 = e_t. [clausify] 96 e_plus1 = e_t | e_plus2 = e_t | e_minus4 = e_t. [clausify] 97 e_minus5 = e_t | e_plus8 = e_t | e_plus7 = e_t. [clausify] 98 e_minus8 = e_t | e_minus5 = e_t | e_minus3 = e_t. [clausify] 99 e_minus3 = e_t | e_plus5 = e_t | e_minus8 = e_t. [clausify] 100 e_minus1 != e_plus1. [copy 46 flip a] 101 e_plus2 != e_minus2. [copy 47 flip a] 102 e_minus3 != e_plus3. [clausify] 103 e_plus4 != e_minus4. [copy 49 flip a] 104 e_plus5 != e_minus5. [copy 50 flip a] 105 e_minus6 != e_plus6. [clausify] 106 e_plus7 != e_minus7. [clausify] 107 e_plus8 != e_minus8. [copy 53 flip a] 108 e_minus9 != e_plus9. [clausify] end_of_list. clauses(demodulators). end_of_list. clauses(goals). end_of_list. % Starting search at 17.43 seconds. given #1 (wt=9): 55 e_plus4 = e_t | e_plus3 = e_t | e_plus9 = e_t. [clausify] given #2 (wt=9): 56 e_plus4 = e_t | e_plus3 = e_t | e_plus6 = e_t. [clausify] given #3 (wt=9): 57 e_minus9 = e_t | e_plus4 = e_t | e_plus3 = e_t. [clausify] given #4 (wt=9): 58 e_minus7 = e_t | e_plus9 = e_t | e_plus5 = e_t. [clausify] given #5 (wt=9): 59 e_plus2 = e_t | e_minus1 = e_t | e_plus4 = e_t. [clausify] given #6 (wt=9): 60 e_plus8 = e_t | e_minus4 = e_t | e_plus2 = e_t. [clausify] given #7 (wt=9): 61 e_plus4 = e_t | e_plus1 = e_t | e_plus3 = e_t. [clausify] given #8 (wt=9): 62 e_plus5 = e_t | e_plus2 = e_t | e_plus9 = e_t. [clausify] given #9 (wt=9): 63 e_plus6 = e_t | e_minus7 = e_t | e_minus8 = e_t. [clausify] given #10 (wt=9): 64 e_minus2 = e_t | e_minus3 = e_t | e_plus1 = e_t. [clausify] given #11 (wt=9): 65 e_minus6 = e_t | e_plus1 = e_t | e_minus9 = e_t. [clausify] given #12 (wt=9): 66 e_minus4 = e_t | e_plus1 = e_t | e_plus9 = e_t. [clausify] given #13 (wt=9): 67 e_plus6 = e_t | e_minus2 = e_t | e_plus9 = e_t. [clausify] given #14 (wt=9): 68 e_minus7 = e_t | e_minus3 = e_t | e_minus4 = e_t. [clausify] given #15 (wt=9): 69 e_minus3 = e_t | e_plus6 = e_t | e_minus4 = e_t. [clausify] given #16 (wt=9): 70 e_plus8 = e_t | e_minus7 = e_t | e_plus3 = e_t. [clausify] given #17 (wt=9): 71 e_plus7 = e_t | e_minus9 = e_t | e_minus2 = e_t. [clausify] given #18 (wt=9): 72 e_minus9 = e_t | e_minus4 = e_t | e_minus8 = e_t. [clausify] given #19 (wt=9): 73 e_plus9 = e_t | e_minus4 = e_t | e_plus5 = e_t. [clausify] given #20 (wt=9): 74 e_plus4 = e_t | e_minus8 = e_t | e_plus6 = e_t. [clausify] given #21 (wt=9): 75 e_plus2 = e_t | e_minus5 = e_t | e_minus7 = e_t. [clausify] given #22 (wt=9): 76 e_plus6 = e_t | e_minus4 = e_t | e_minus1 = e_t. [clausify] given #23 (wt=9): 77 e_plus4 = e_t | e_minus6 = e_t | e_minus2 = e_t. [clausify] given #24 (wt=9): 78 e_plus4 = e_t | e_plus6 = e_t | e_minus5 = e_t. [clausify] given #25 (wt=9): 79 e_plus1 = e_t | e_minus4 = e_t | e_minus6 = e_t. [clausify] given #26 (wt=9): 80 e_plus8 = e_t | e_minus4 = e_t | e_plus6 = e_t. [clausify] given #27 (wt=9): 81 e_minus4 = e_t | e_plus9 = e_t | e_minus8 = e_t. [clausify] given #28 (wt=9): 82 e_plus6 = e_t | e_minus2 = e_t | e_minus7 = e_t. [clausify] given #29 (wt=9): 83 e_minus3 = e_t | e_plus8 = e_t | e_plus7 = e_t. [clausify] given #30 (wt=9): 84 e_plus1 = e_t | e_plus9 = e_t | e_minus6 = e_t. [clausify] given #31 (wt=9): 85 e_minus9 = e_t | e_plus3 = e_t | e_minus2 = e_t. [clausify] given #32 (wt=9): 86 e_plus2 = e_t | e_plus1 = e_t | e_minus6 = e_t. [clausify] given #33 (wt=9): 87 e_minus8 = e_t | e_minus2 = e_t | e_plus3 = e_t. [clausify] given #34 (wt=9): 88 e_plus9 = e_t | e_minus8 = e_t | e_plus3 = e_t. [clausify] given #35 (wt=9): 89 e_plus1 = e_t | e_plus7 = e_t | e_plus4 = e_t. [clausify] given #36 (wt=9): 90 e_plus7 = e_t | e_minus4 = e_t | e_plus9 = e_t. [clausify] given #37 (wt=9): 91 e_minus7 = e_t | e_minus6 = e_t | e_plus9 = e_t. [clausify] given #38 (wt=9): 92 e_plus6 = e_t | e_plus3 = e_t | e_minus4 = e_t. [clausify] given #39 (wt=9): 93 e_minus5 = e_t | e_plus3 = e_t | e_minus9 = e_t. [clausify] given #40 (wt=9): 94 e_minus3 = e_t | e_plus8 = e_t | e_plus2 = e_t. [clausify] given #41 (wt=9): 95 e_minus5 = e_t | e_minus2 = e_t | e_minus9 = e_t. [clausify] given #42 (wt=9): 96 e_plus1 = e_t | e_plus2 = e_t | e_minus4 = e_t. [clausify] given #43 (wt=9): 97 e_minus5 = e_t | e_plus8 = e_t | e_plus7 = e_t. [clausify] given #44 (wt=9): 98 e_minus8 = e_t | e_minus5 = e_t | e_minus3 = e_t. [clausify] given #45 (wt=9): 99 e_minus3 = e_t | e_plus5 = e_t | e_minus8 = e_t. [clausify] given #46 (wt=3): 100 e_minus1 != e_plus1. [copy 46 flip a] given #47 (wt=3): 101 e_plus2 != e_minus2. [copy 47 flip a] given #48 (wt=3): 102 e_minus3 != e_plus3. [clausify] given #49 (wt=3): 103 e_plus4 != e_minus4. [copy 49 flip a] given #50 (wt=3): 104 e_plus5 != e_minus5. [copy 50 flip a] given #51 (wt=3): 105 e_minus6 != e_plus6. [clausify] given #52 (wt=3): 106 e_plus7 != e_minus7. [clausify] given #53 (wt=3): 107 e_plus8 != e_minus8. [copy 53 flip a] given #54 (wt=3): 108 e_minus9 != e_plus9. [clausify] given #55 (wt=9): 109 e_plus2 = e_t | e_plus4 = e_t | e_plus1 != e_t. [para (59 (b 1) 100 (a 1)) flip c] given #56 (wt=9): 110 e_minus4 = e_t | e_plus9 = e_t | e_minus1 != e_t. [para (66 (b 1) 100 (a 2))] given #57 (wt=9): 111 e_plus6 = e_t | e_minus4 = e_t | e_plus1 != e_t. [para (76 (c 1) 100 (a 1)) flip c] given #58 (wt=9): 112 e_plus6 = e_t | e_plus9 = e_t | e_plus2 != e_t. [para (67 (b 1) 101 (a 2))] given #59 (wt=9): 113 e_plus1 = e_t | e_minus4 = e_t | e_minus2 != e_t. [para (96 (b 1) 101 (a 1)) flip c] given #60 (wt=9): 114 e_minus2 = e_t | e_plus1 = e_t | e_plus3 != e_t. [para (64 (b 1) 102 (a 1)) flip c] given #61 (wt=9): 115 e_plus6 = e_t | e_minus4 = e_t | e_plus3 != e_t. [para (69 (a 1) 102 (a 1)) flip c] given #62 (wt=9): 116 e_plus3 = e_t | e_plus9 = e_t | e_minus4 != e_t. [para (55 (a 1) 103 (a 1)) flip c] given #63 (wt=9): 117 e_plus3 = e_t | e_plus6 = e_t | e_minus4 != e_t. [para (56 (a 1) 103 (a 1)) flip c] given #64 (wt=9): 118 e_plus1 = e_t | e_plus3 = e_t | e_minus4 != e_t. [para (61 (a 1) 103 (a 1)) flip c] given #65 (wt=9): 119 e_minus7 = e_t | e_plus9 = e_t | e_minus5 != e_t. [para (58 (c 1) 104 (a 1)) flip c] given #66 (wt=9): 120 e_plus2 = e_t | e_plus9 = e_t | e_minus5 != e_t. [para (62 (a 1) 104 (a 1)) flip c] given #67 (wt=9): 121 e_plus9 = e_t | e_minus4 = e_t | e_minus5 != e_t. [para (73 (c 1) 104 (a 1)) flip c] given #68 (wt=9): 122 e_plus2 = e_t | e_minus7 = e_t | e_plus5 != e_t. [para (75 (b 1) 104 (a 2))] given #69 (wt=9): 123 e_plus4 = e_t | e_plus6 = e_t | e_plus5 != e_t. [para (78 (c 1) 104 (a 2))] given #70 (wt=9): 124 e_plus3 = e_t | e_minus9 = e_t | e_plus5 != e_t. [para (93 (a 1) 104 (a 2))] given #71 (wt=9): 125 e_minus2 = e_t | e_minus9 = e_t | e_plus5 != e_t. [para (95 (a 1) 104 (a 2))] given #72 (wt=9): 126 e_minus8 = e_t | e_minus3 = e_t | e_plus5 != e_t. [para (98 (b 1) 104 (a 2))] given #73 (wt=6): 170 e_minus8 = e_t | e_minus3 = e_t. [resolve (126 c 99 b) merge c merge d] given #74 (wt=6): 171 e_minus8 = e_t | e_plus3 != e_t. [para (170 (b 1) 102 (a 1)) flip b] given #75 (wt=9): 128 e_plus1 = e_t | e_minus9 = e_t | e_plus6 != e_t. [para (65 (a 1) 105 (a 1)) flip c] given #76 (wt=9): 129 e_plus4 = e_t | e_minus2 = e_t | e_plus6 != e_t. [para (77 (b 1) 105 (a 1)) flip c] given #77 (wt=9): 130 e_plus1 = e_t | e_minus4 = e_t | e_plus6 != e_t. [para (79 (c 1) 105 (a 1)) flip c] given #78 (wt=9): 131 e_plus1 = e_t | e_plus9 = e_t | e_plus6 != e_t. [para (84 (c 1) 105 (a 1)) flip c] given #79 (wt=9): 132 e_plus2 = e_t | e_plus1 = e_t | e_plus6 != e_t. [para (86 (c 1) 105 (a 1)) flip c] given #80 (wt=9): 133 e_minus7 = e_t | e_plus9 = e_t | e_plus6 != e_t. [para (91 (b 1) 105 (a 1)) flip c] given #81 (wt=9): 134 e_plus3 = e_t | e_minus4 = e_t | e_minus6 != e_t. [para (92 (a 1) 105 (a 2))] given #82 (wt=9): 135 e_plus6 = e_t | e_minus8 = e_t | e_plus7 != e_t. [para (63 (b 1) 106 (a 2))] given #83 (wt=9): 136 e_minus3 = e_t | e_minus4 = e_t | e_plus7 != e_t. [para (68 (a 1) 106 (a 2))] given #84 (wt=9): 137 e_minus9 = e_t | e_minus2 = e_t | e_minus7 != e_t. [para (71 (a 1) 106 (a 1)) flip c] given #85 (wt=9): 138 e_plus6 = e_t | e_minus2 = e_t | e_plus7 != e_t. [para (82 (c 1) 106 (a 2))] given #86 (wt=9): 139 e_minus3 = e_t | e_plus8 = e_t | e_minus7 != e_t. [para (83 (c 1) 106 (a 1)) flip c] given #87 (wt=9): 140 e_plus1 = e_t | e_plus4 = e_t | e_minus7 != e_t. [para (89 (b 1) 106 (a 1)) flip c] given #88 (wt=9): 141 e_minus4 = e_t | e_plus9 = e_t | e_minus7 != e_t. [para (90 (a 1) 106 (a 1)) flip c] given #89 (wt=9): 142 e_minus5 = e_t | e_plus8 = e_t | e_minus7 != e_t. [para (97 (c 1) 106 (a 1)) flip c] given #90 (wt=9): 143 e_minus4 = e_t | e_plus2 = e_t | e_minus8 != e_t. [para (60 (a 1) 107 (a 1)) flip c] given #91 (wt=9): 144 e_minus7 = e_t | e_plus3 = e_t | e_minus8 != e_t. [para (70 (a 1) 107 (a 1)) flip c] given #92 (wt=9): 145 e_plus4 = e_t | e_plus6 = e_t | e_plus8 != e_t. [para (74 (b 1) 107 (a 2))] given #93 (wt=9): 146 e_minus4 = e_t | e_plus6 = e_t | e_minus8 != e_t. [para (80 (a 1) 107 (a 1)) flip c] given #94 (wt=9): 147 e_minus4 = e_t | e_plus9 = e_t | e_plus8 != e_t. [para (81 (c 1) 107 (a 2))] given #95 (wt=9): 148 e_minus2 = e_t | e_plus3 = e_t | e_plus8 != e_t. [para (87 (a 1) 107 (a 2))] given #96 (wt=9): 149 e_plus9 = e_t | e_plus3 = e_t | e_plus8 != e_t. [para (88 (b 1) 107 (a 2))] given #97 (wt=9): 150 e_minus3 = e_t | e_plus2 = e_t | e_minus8 != e_t. [para (94 (b 1) 107 (a 1)) flip c] given #98 (wt=9): 151 e_plus4 = e_t | e_plus3 = e_t | e_plus9 != e_t. [para (57 (a 1) 108 (a 1)) flip c] given #99 (wt=9): 152 e_minus4 = e_t | e_minus8 = e_t | e_plus9 != e_t. [para (72 (a 1) 108 (a 1)) flip c] given #100 (wt=9): 153 e_plus3 = e_t | e_minus2 = e_t | e_plus9 != e_t. [para (85 (a 1) 108 (a 1)) flip c] given #101 (wt=9): 155 e_minus4 = e_t | e_plus9 = e_t | e_plus6 = e_t. [resolve (110 c 76 c) merge d] given #102 (wt=9): 160 e_minus7 = e_t | e_plus9 = e_t | e_plus2 = e_t. [resolve (119 c 75 b) merge d] given #103 (wt=9): 174 e_plus1 = e_t | e_minus4 = e_t | e_plus3 = e_t. [resolve (130 c 92 a) merge d] given #104 (wt=9): 179 e_minus3 = e_t | e_minus4 = e_t | e_plus9 = e_t. [resolve (136 c 90 a) merge c] given #105 (wt=9): 181 e_minus3 = e_t | e_minus4 = e_t | e_plus8 = e_t. [resolve (136 c 83 c) merge c] given #106 (wt=12): 157 e_minus7 = e_t | e_plus9 = e_t | e_minus2 = e_t | e_minus9 = e_t. [resolve (119 c 95 a)] given #107 (wt=9): 183 e_minus9 = e_t | e_minus2 = e_t | e_plus6 = e_t. [resolve (137 c 82 c) merge d] given #108 (wt=9): 189 e_minus4 = e_t | e_plus2 = e_t | e_plus9 = e_t. [resolve (143 c 81 c) merge c] given #109 (wt=9): 191 e_minus7 = e_t | e_plus3 = e_t | e_plus9 = e_t. [resolve (144 c 88 b) merge d] given #110 (wt=9): 192 e_minus7 = e_t | e_plus3 = e_t | e_minus2 = e_t. [resolve (144 c 87 a) merge d] given #111 (wt=12): 162 e_plus2 = e_t | e_plus9 = e_t | e_minus2 = e_t | e_minus9 = e_t. [resolve (120 c 95 a)] given #112 (wt=9): 194 e_plus4 = e_t | e_plus6 = e_t | e_minus4 = e_t. [resolve (145 c 80 a) merge d] given #113 (wt=9): 197 e_minus4 = e_t | e_plus9 = e_t | e_minus7 = e_t. [resolve (155 c 133 c) merge d] given #114 (wt=6): 217 e_minus4 = e_t | e_plus9 = e_t. [resolve (197 c 141 c) merge c merge d] given #115 (wt=6): 219 e_minus4 = e_t | e_minus8 = e_t. [resolve (217 b 152 c) merge b] given #116 (wt=12): 163 e_plus2 = e_t | e_plus9 = e_t | e_plus3 = e_t | e_minus9 = e_t. [resolve (120 c 93 a)] given #117 (wt=6): 221 e_minus4 = e_t | e_minus9 != e_t. [para (217 (b 1) 108 (a 2))] given #118 (wt=6): 223 e_minus4 = e_t | e_plus6 = e_t. [resolve (219 b 146 c) merge b] given #119 (wt=6): 225 e_minus4 = e_t | e_plus2 = e_t. [resolve (219 b 143 c) merge b] given #120 (wt=6): 226 e_minus4 = e_t | e_plus8 != e_t. [para (219 (b 1) 107 (a 2))] given #121 (wt=12): 164 e_plus2 = e_t | e_plus9 = e_t | e_plus4 = e_t | e_plus6 = e_t. [resolve (120 c 78 c)] given #122 (wt=6): 229 e_minus4 = e_t | e_plus1 = e_t. [resolve (223 b 130 c) merge c] given #123 (wt=6): 231 e_minus4 = e_t | e_minus6 != e_t. [para (223 (b 1) 105 (a 2))] given #124 (wt=6): 232 e_minus4 = e_t | e_minus2 != e_t. [para (225 (b 1) 101 (a 1)) flip b] given #125 (wt=6): 233 e_minus4 = e_t | e_minus3 = e_t. [resolve (226 b 181 c) merge c] given #126 (wt=12): 176 e_plus6 = e_t | e_minus8 = e_t | e_minus5 = e_t | e_plus8 = e_t. [resolve (135 c 97 c)] given #127 (wt=6): 235 e_minus4 = e_t | e_minus1 != e_t. [para (229 (b 1) 100 (a 2))] given #128 (wt=6): 236 e_minus4 = e_t | e_plus3 != e_t. [para (233 (b 1) 102 (a 1)) flip b] given #129 (wt=9): 200 e_minus7 = e_t | e_plus9 = e_t | e_plus6 = e_t. [resolve (160 c 112 c) merge d] given #130 (wt=9): 201 e_minus7 = e_t | e_plus9 = e_t | e_minus2 != e_t. [para (160 (c 1) 101 (a 1)) flip c] given #131 (wt=12): 184 e_plus6 = e_t | e_minus2 = e_t | e_minus5 = e_t | e_plus8 = e_t. [resolve (138 c 97 c)] given #132 (wt=9): 207 e_minus2 = e_t | e_plus6 = e_t | e_plus9 != e_t. [para (183 (a 1) 108 (a 1)) flip c] given #133 (wt=9): 212 e_plus3 = e_t | e_plus9 = e_t | e_plus7 != e_t. [para (191 (a 1) 106 (a 2))] given #134 (wt=9): 215 e_plus3 = e_t | e_minus2 = e_t | e_plus7 != e_t. [para (192 (a 1) 106 (a 2))] given #135 (wt=9): 218 e_minus4 = e_t | e_plus3 = e_t | e_minus2 = e_t. [resolve (217 b 153 c)] given #136 (wt=12): 185 e_plus6 = e_t | e_minus2 = e_t | e_plus1 = e_t | e_plus4 = e_t. [resolve (138 c 89 b)] given #137 (wt=6): 242 e_minus4 = e_t | e_plus3 = e_t. [resolve (218 c 232 b) merge c] given #138 (wt=3): 248 e_plus4 != e_t. [back_demod 103 demod (244)] given #139 (wt=3): 244 e_minus4 = e_t. [resolve (242 b 236 b) merge b] given #140 (wt=6): 245 e_plus1 = e_t | e_plus3 = e_t. [back_demod 118 demod (244) xx c] given #141 (wt=12): 186 e_plus6 = e_t | e_minus2 = e_t | e_minus3 = e_t | e_plus8 = e_t. [resolve (138 c 83 c)] given #142 (wt=6): 246 e_plus3 = e_t | e_plus6 = e_t. [back_demod 117 demod (244) xx c] given #143 (wt=6): 247 e_plus3 = e_t | e_plus9 = e_t. [back_demod 116 demod (244) xx c] given #144 (wt=6): 250 e_plus9 = e_t | e_plus6 = e_t. [back_unit_del 234 unit_del (b 248)] given #145 (wt=6): 253 e_plus3 = e_t | e_plus9 != e_t. [back_unit_del 151 unit_del (a 248)] given #146 (wt=12): 195 e_minus2 = e_t | e_plus3 = e_t | e_minus3 = e_t | e_plus2 = e_t. [resolve (148 c 94 b)] given #147 (wt=6): 254 e_plus6 = e_t | e_plus8 != e_t. [back_unit_del 145 unit_del (a 248)] given #148 (wt=6): 255 e_plus1 = e_t | e_minus7 != e_t. [back_unit_del 140 unit_del (b 248)] given #149 (wt=6): 256 e_minus2 = e_t | e_plus6 != e_t. [back_unit_del 129 unit_del (a 248)] given #150 (wt=6): 257 e_plus6 = e_t | e_plus5 != e_t. [back_unit_del 123 unit_del (a 248)] given #151 (wt=9): 249 e_plus6 = e_t | e_plus1 = e_t | e_plus2 != e_t. [back_unit_del 243 unit_del (c 248)] given #152 (wt=6): 258 e_plus2 = e_t | e_plus1 != e_t. [back_unit_del 109 unit_del (b 248)] given #153 (wt=6): 259 e_plus1 = e_t | e_plus7 = e_t. [back_unit_del 89 unit_del (c 248)] given #154 (wt=6): 260 e_plus6 = e_t | e_minus5 = e_t. [back_unit_del 78 unit_del (a 248)] given #155 (wt=6): 261 e_minus6 = e_t | e_minus2 = e_t. [back_unit_del 77 unit_del (a 248)] given #156 (wt=9): 251 e_plus6 = e_t | e_minus3 = e_t | e_plus2 = e_t. [back_unit_del 193 unit_del (a 248)] given #157 (wt=6): 262 e_minus8 = e_t | e_plus6 = e_t. [back_unit_del 74 unit_del (a 248)] given #158 (wt=6): 263 e_plus2 = e_t | e_minus1 = e_t. [back_unit_del 59 unit_del (c 248)] given #159 (wt=6): 264 e_minus9 = e_t | e_plus3 = e_t. [back_unit_del 57 unit_del (b 248)] given #160 (wt=6): 265 e_plus3 = e_t | e_minus1 != e_t. [para (245 (a 1) 100 (a 2))] given #161 (wt=9): 252 e_plus6 = e_t | e_minus2 = e_t | e_plus1 = e_t. [back_unit_del 185 unit_del (d 248)] given #162 (wt=6): 267 e_plus3 = e_t | e_minus6 != e_t. [para (246 (b 1) 105 (a 2))] given #163 (wt=6): 268 e_plus9 = e_t | e_minus8 = e_t. [resolve (247 a 171 b)] given #164 (wt=6): 270 e_plus9 = e_t | e_minus3 != e_t. [para (247 (a 1) 102 (a 2))] given #165 (wt=6): 271 e_plus9 = e_t | e_minus7 = e_t. [resolve (250 b 133 c) merge c] given #166 (wt=6): 273 e_plus9 = e_t | e_plus1 = e_t. [resolve (250 b 131 c) merge c] given #167 (wt=6): 274 e_plus9 = e_t | e_minus6 != e_t. [para (250 (b 1) 105 (a 2))] given #168 (wt=6): 276 e_minus2 = e_t | e_plus9 = e_t. [resolve (256 b 250 b)] given #169 (wt=6): 277 e_minus2 = e_t | e_plus3 = e_t. [resolve (256 b 246 b)] given #170 (wt=6): 278 e_plus2 = e_t | e_plus3 = e_t. [resolve (258 b 245 a)] given #171 (wt=9): 275 e_plus6 = e_t | e_minus2 = e_t | e_minus3 = e_t. [resolve (254 b 186 d) merge b] given #172 (wt=6): 282 e_plus9 = e_t | e_plus8 != e_t. [para (268 (b 1) 107 (a 2))] given #173 (wt=6): 285 e_plus9 = e_t | e_plus7 != e_t. [para (271 (b 1) 106 (a 2))] given #174 (wt=6): 286 e_plus9 = e_t | e_plus2 = e_t. [resolve (273 b 258 b)] given #175 (wt=6): 287 e_plus9 = e_t | e_minus1 != e_t. [para (273 (b 1) 100 (a 2))] given #176 (wt=9): 279 e_plus6 = e_t | e_minus3 = e_t | e_plus1 = e_t. [resolve (251 c 249 c) merge c] given #177 (wt=6): 288 e_plus9 = e_t | e_plus2 != e_t. [para (276 (a 1) 101 (a 2))] -------- Proof 1 -------- (17.48 + 0.03 seconds) -------- PROOF -------- Length of proof is 88. Maximum clause weight is 12. 46 e_plus1 != e_minus1. [clausify] 47 e_minus2 != e_plus2. [clausify] 49 e_minus4 != e_plus4. [clausify] 50 e_minus5 != e_plus5. [clausify] 53 e_minus8 != e_plus8. [clausify] 57 e_minus9 = e_t | e_plus4 = e_t | e_plus3 = e_t. [clausify] 59 e_plus2 = e_t | e_minus1 = e_t | e_plus4 = e_t. [clausify] 60 e_plus8 = e_t | e_minus4 = e_t | e_plus2 = e_t. [clausify] 62 e_plus5 = e_t | e_plus2 = e_t | e_plus9 = e_t. [clausify] 66 e_minus4 = e_t | e_plus1 = e_t | e_plus9 = e_t. [clausify] 67 e_plus6 = e_t | e_minus2 = e_t | e_plus9 = e_t. [clausify] 68 e_minus7 = e_t | e_minus3 = e_t | e_minus4 = e_t. [clausify] 71 e_plus7 = e_t | e_minus9 = e_t | e_minus2 = e_t. [clausify] 72 e_minus9 = e_t | e_minus4 = e_t | e_minus8 = e_t. [clausify] 76 e_plus6 = e_t | e_minus4 = e_t | e_minus1 = e_t. [clausify] 77 e_plus4 = e_t | e_minus6 = e_t | e_minus2 = e_t. [clausify] 78 e_plus4 = e_t | e_plus6 = e_t | e_minus5 = e_t. [clausify] 82 e_plus6 = e_t | e_minus2 = e_t | e_minus7 = e_t. [clausify] 83 e_minus3 = e_t | e_plus8 = e_t | e_plus7 = e_t. [clausify] 84 e_plus1 = e_t | e_plus9 = e_t | e_minus6 = e_t. [clausify] 85 e_minus9 = e_t | e_plus3 = e_t | e_minus2 = e_t. [clausify] 90 e_plus7 = e_t | e_minus4 = e_t | e_plus9 = e_t. [clausify] 91 e_minus7 = e_t | e_minus6 = e_t | e_plus9 = e_t. [clausify] 94 e_minus3 = e_t | e_plus8 = e_t | e_plus2 = e_t. [clausify] 98 e_minus8 = e_t | e_minus5 = e_t | e_minus3 = e_t. [clausify] 99 e_minus3 = e_t | e_plus5 = e_t | e_minus8 = e_t. [clausify] 100 e_minus1 != e_plus1. [copy 46 flip a] 101 e_plus2 != e_minus2. [copy 47 flip a] 102 e_minus3 != e_plus3. [clausify] 103 e_plus4 != e_minus4. [copy 49 flip a] 104 e_plus5 != e_minus5. [copy 50 flip a] 105 e_minus6 != e_plus6. [clausify] 106 e_plus7 != e_minus7. [clausify] 107 e_plus8 != e_minus8. [copy 53 flip a] 108 e_minus9 != e_plus9. [clausify] 109 e_plus2 = e_t | e_plus4 = e_t | e_plus1 != e_t. [para (59 (b 1) 100 (a 1)) flip c] 110 e_minus4 = e_t | e_plus9 = e_t | e_minus1 != e_t. [para (66 (b 1) 100 (a 2))] 112 e_plus6 = e_t | e_plus9 = e_t | e_plus2 != e_t. [para (67 (b 1) 101 (a 2))] 120 e_plus2 = e_t | e_plus9 = e_t | e_minus5 != e_t. [para (62 (a 1) 104 (a 1)) flip c] 126 e_minus8 = e_t | e_minus3 = e_t | e_plus5 != e_t. [para (98 (b 1) 104 (a 2))] 129 e_plus4 = e_t | e_minus2 = e_t | e_plus6 != e_t. [para (77 (b 1) 105 (a 1)) flip c] 131 e_plus1 = e_t | e_plus9 = e_t | e_plus6 != e_t. [para (84 (c 1) 105 (a 1)) flip c] 133 e_minus7 = e_t | e_plus9 = e_t | e_plus6 != e_t. [para (91 (b 1) 105 (a 1)) flip c] 136 e_minus3 = e_t | e_minus4 = e_t | e_plus7 != e_t. [para (68 (a 1) 106 (a 2))] 137 e_minus9 = e_t | e_minus2 = e_t | e_minus7 != e_t. [para (71 (a 1) 106 (a 1)) flip c] 141 e_minus4 = e_t | e_plus9 = e_t | e_minus7 != e_t. [para (90 (a 1) 106 (a 1)) flip c] 143 e_minus4 = e_t | e_plus2 = e_t | e_minus8 != e_t. [para (60 (a 1) 107 (a 1)) flip c] 150 e_minus3 = e_t | e_plus2 = e_t | e_minus8 != e_t. [para (94 (b 1) 107 (a 1)) flip c] 151 e_plus4 = e_t | e_plus3 = e_t | e_plus9 != e_t. [para (57 (a 1) 108 (a 1)) flip c] 152 e_minus4 = e_t | e_minus8 = e_t | e_plus9 != e_t. [para (72 (a 1) 108 (a 1)) flip c] 153 e_plus3 = e_t | e_minus2 = e_t | e_plus9 != e_t. [para (85 (a 1) 108 (a 1)) flip c] 155 e_minus4 = e_t | e_plus9 = e_t | e_plus6 = e_t. [resolve (110 c 76 c) merge d] 164 e_plus2 = e_t | e_plus9 = e_t | e_plus4 = e_t | e_plus6 = e_t. [resolve (120 c 78 c)] 170 e_minus8 = e_t | e_minus3 = e_t. [resolve (126 c 99 b) merge c merge d] 171 e_minus8 = e_t | e_plus3 != e_t. [para (170 (b 1) 102 (a 1)) flip b] 181 e_minus3 = e_t | e_minus4 = e_t | e_plus8 = e_t. [resolve (136 c 83 c) merge c] 183 e_minus9 = e_t | e_minus2 = e_t | e_plus6 = e_t. [resolve (137 c 82 c) merge d] 197 e_minus4 = e_t | e_plus9 = e_t | e_minus7 = e_t. [resolve (155 c 133 c) merge d] 207 e_minus2 = e_t | e_plus6 = e_t | e_plus9 != e_t. [para (183 (a 1) 108 (a 1)) flip c] 217 e_minus4 = e_t | e_plus9 = e_t. [resolve (197 c 141 c) merge c merge d] 218 e_minus4 = e_t | e_plus3 = e_t | e_minus2 = e_t. [resolve (217 b 153 c)] 219 e_minus4 = e_t | e_minus8 = e_t. [resolve (217 b 152 c) merge b] 225 e_minus4 = e_t | e_plus2 = e_t. [resolve (219 b 143 c) merge b] 226 e_minus4 = e_t | e_plus8 != e_t. [para (219 (b 1) 107 (a 2))] 232 e_minus4 = e_t | e_minus2 != e_t. [para (225 (b 1) 101 (a 1)) flip b] 233 e_minus4 = e_t | e_minus3 = e_t. [resolve (226 b 181 c) merge c] 234 e_plus9 = e_t | e_plus4 = e_t | e_plus6 = e_t. [resolve (164 a 112 c) merge d merge e] 236 e_minus4 = e_t | e_plus3 != e_t. [para (233 (b 1) 102 (a 1)) flip b] 242 e_minus4 = e_t | e_plus3 = e_t. [resolve (218 c 232 b) merge c] 244 e_minus4 = e_t. [resolve (242 b 236 b) merge b] 248 e_plus4 != e_t. [back_demod 103 demod (244)] 250 e_plus9 = e_t | e_plus6 = e_t. [back_unit_del 234 unit_del (b 248)] 253 e_plus3 = e_t | e_plus9 != e_t. [back_unit_del 151 unit_del (a 248)] 256 e_minus2 = e_t | e_plus6 != e_t. [back_unit_del 129 unit_del (a 248)] 258 e_plus2 = e_t | e_plus1 != e_t. [back_unit_del 109 unit_del (b 248)] 273 e_plus9 = e_t | e_plus1 = e_t. [resolve (250 b 131 c) merge c] 276 e_minus2 = e_t | e_plus9 = e_t. [resolve (256 b 250 b)] 286 e_plus9 = e_t | e_plus2 = e_t. [resolve (273 b 258 b)] 288 e_plus9 = e_t | e_plus2 != e_t. [para (276 (a 1) 101 (a 2))] 294 e_plus9 = e_t. [resolve (288 b 286 b) merge b] 295 e_plus3 = e_t. [back_demod 253 demod (294) xx b] 296 e_minus2 = e_t | e_plus6 = e_t. [back_demod 207 demod (294) xx c] 299 e_minus8 = e_t. [back_demod 171 demod (295) xx b] 301 e_minus3 != e_t. [back_demod 102 demod (295)] 308 e_plus2 = e_t. [back_demod 150 demod (299) xx c unit_del (a 301)] 313 e_minus2 != e_t. [back_demod 101 demod (308) flip a] 317 e_plus6 = e_t. [back_unit_del 296 unit_del (a 313)] 319 $F. [back_unit_del 256 demod (317) xx b unit_del (a 313)] -------- end of proof ------- Given=177. Generated=972. Kept=264. Proofs=1. Usable=7. Sos=12. Demods=10. Goals=0. Limbo=6, Disabled=293. Hints=0. Weight_deleted=0. Literals_deleted=0. Forward_subsumed=707. Back_subsumed=188. Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. New_demodulators=10 (0 lex), Back_demodulated=16. Back_unit_deleted=35. Demod_attempts=2345. Demod_rewrites=35. Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. Nonunit_fsub_feature_tests=435. Nonunit_bsub_feature_tests=426. Megabytes=7.34. User_CPU=17.48, System_CPU=0.03, Wall_clock=18. THEOREM PROVED Exiting with 1 proof. Process 1252 exit (max_proofs) Wed Jul 13 01:20:29 2005