%------------------------------------------------------------------------------ % File : Etableau---0.67 % Problem : SWV502-1.030 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : etableau --auto --tsmdo --quicksat=10000 --tableau=1 --tableau-saturation=1 -s -p --tableau-cores=8 --cpu-limit=%d %s % Computer : n009.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 : 600s % DateTime : Wed Jul 20 18:21:30 EDT 2022 % Result : Satisfiable 61.41s 8.22s % Output : CNFRefutation 61.41s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SWV502-1.030 : TPTP v8.1.0. Released v4.0.0. % 0.12/0.13 % Command : etableau --auto --tsmdo --quicksat=10000 --tableau=1 --tableau-saturation=1 -s -p --tableau-cores=8 --cpu-limit=%d %s % 0.13/0.34 % Computer : n009.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Wed Jun 15 02:57:08 EDT 2022 % 0.13/0.34 % CPUTime : % 0.13/0.39 # No SInE strategy applied % 0.13/0.39 # Auto-Mode selected heuristic G_E___208_C18_F1_SE_CS_SP_PS_S5PRR_RG_S04AN % 0.13/0.39 # and selection function SelectComplexExceptUniqMaxHorn. % 0.13/0.39 # % 0.13/0.39 # Presaturation interreduction done % 0.13/0.39 # Number of axioms: 438 Number of unprocessed: 438 % 0.13/0.39 # Tableaux proof search. % 0.13/0.39 # APR header successfully linked. % 0.13/0.39 # Hello from C++ % 0.19/0.52 # The folding up rule is enabled... % 0.19/0.52 # Local unification is enabled... % 0.19/0.52 # Any saturation attempts will use folding labels... % 0.19/0.52 # 438 beginning clauses after preprocessing and clausification % 0.19/0.52 # Creating start rules for all 1 conjectures. % 0.19/0.52 # There are 1 start rule candidates: % 0.19/0.52 # Found 437 unit axioms. % 0.19/0.52 # 1 start rule tableaux created. % 0.19/0.52 # 1 extension rule candidate clauses % 0.19/0.52 # 437 unit axiom clauses % 0.19/0.52 % 0.19/0.52 # Requested 8, 32 cores available to the main process. % 0.19/0.52 # There are not enough tableaux to fork, creating more from the initial 1 % 0.19/0.52 # Creating equality axioms % 0.19/0.52 # Ran out of tableaux, making start rules for all clauses % 0.19/0.52 # Returning from population with 446 new_tableaux and 0 remaining starting tableaux. % 0.19/0.52 # We now have 446 tableaux to operate on % 61.41/8.21 # 11858 Satisfiable branch % 61.41/8.21 # Satisfiable branch found. % 61.41/8.22 # There were 1 total branch saturation attempts. % 61.41/8.22 # There were 0 of these attempts blocked. % 61.41/8.22 # There were 0 deferred branch saturation attempts. % 61.41/8.22 # There were 0 free duplicated saturations. % 61.41/8.22 # There were 0 total successful branch saturations. % 61.41/8.22 # There were 0 successful branch saturations in interreduction. % 61.41/8.22 # There were 0 successful branch saturations on the branch. % 61.41/8.22 # There were 0 successful branch saturations after the branch. % 61.41/8.22 # SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 61.41/8.22 # SZS output start for /export/starexec/sandbox/benchmark/theBenchmark.p % 61.41/8.22 # Begin clausification derivation % 61.41/8.22 % 61.41/8.22 # End clausification derivation % 61.41/8.22 # Begin listing active clauses obtained from FOF to CNF conversion % 61.41/8.22 cnf(i_0_439, plain, (select(store(X1,X2,X3),X2)=X3)). % 61.41/8.22 cnf(i_0_441, hypothesis, (i30!=i29)). % 61.41/8.22 cnf(i_0_443, hypothesis, (i28!=i29)). % 61.41/8.22 cnf(i_0_442, hypothesis, (i30!=i28)). % 61.41/8.22 cnf(i_0_445, hypothesis, (i27!=i29)). % 61.41/8.22 cnf(i_0_444, hypothesis, (i30!=i27)). % 61.41/8.22 cnf(i_0_446, hypothesis, (i27!=i28)). % 61.41/8.22 cnf(i_0_448, hypothesis, (i26!=i29)). % 61.41/8.22 cnf(i_0_447, hypothesis, (i30!=i26)). % 61.41/8.22 cnf(i_0_449, hypothesis, (i26!=i28)). % 61.41/8.22 cnf(i_0_450, hypothesis, (i26!=i27)). % 61.41/8.22 cnf(i_0_452, hypothesis, (i25!=i29)). % 61.41/8.22 cnf(i_0_451, hypothesis, (i30!=i25)). % 61.41/8.22 cnf(i_0_453, hypothesis, (i25!=i28)). % 61.41/8.22 cnf(i_0_454, hypothesis, (i25!=i27)). % 61.41/8.22 cnf(i_0_455, hypothesis, (i25!=i26)). % 61.41/8.22 cnf(i_0_457, hypothesis, (i24!=i29)). % 61.41/8.22 cnf(i_0_456, hypothesis, (i30!=i24)). % 61.41/8.22 cnf(i_0_458, hypothesis, (i24!=i28)). % 61.41/8.22 cnf(i_0_459, hypothesis, (i24!=i27)). % 61.41/8.22 cnf(i_0_460, hypothesis, (i24!=i26)). % 61.41/8.22 cnf(i_0_461, hypothesis, (i24!=i25)). % 61.41/8.22 cnf(i_0_463, hypothesis, (i23!=i29)). % 61.41/8.22 cnf(i_0_462, hypothesis, (i30!=i23)). % 61.41/8.22 cnf(i_0_464, hypothesis, (i23!=i28)). % 61.41/8.22 cnf(i_0_465, hypothesis, (i23!=i27)). % 61.41/8.22 cnf(i_0_466, hypothesis, (i23!=i26)). % 61.41/8.22 cnf(i_0_467, hypothesis, (i23!=i25)). % 61.41/8.22 cnf(i_0_468, hypothesis, (i23!=i24)). % 61.41/8.22 cnf(i_0_470, hypothesis, (i22!=i29)). % 61.41/8.22 cnf(i_0_469, hypothesis, (i30!=i22)). % 61.41/8.22 cnf(i_0_471, hypothesis, (i22!=i28)). % 61.41/8.22 cnf(i_0_472, hypothesis, (i22!=i27)). % 61.41/8.22 cnf(i_0_473, hypothesis, (i22!=i26)). % 61.41/8.22 cnf(i_0_474, hypothesis, (i22!=i25)). % 61.41/8.22 cnf(i_0_475, hypothesis, (i22!=i24)). % 61.41/8.22 cnf(i_0_476, hypothesis, (i22!=i23)). % 61.41/8.22 cnf(i_0_478, hypothesis, (i21!=i29)). % 61.41/8.22 cnf(i_0_477, hypothesis, (i30!=i21)). % 61.41/8.22 cnf(i_0_479, hypothesis, (i21!=i28)). % 61.41/8.22 cnf(i_0_480, hypothesis, (i21!=i27)). % 61.41/8.22 cnf(i_0_481, hypothesis, (i21!=i26)). % 61.41/8.22 cnf(i_0_482, hypothesis, (i21!=i25)). % 61.41/8.22 cnf(i_0_483, hypothesis, (i21!=i24)). % 61.41/8.22 cnf(i_0_484, hypothesis, (i21!=i23)). % 61.41/8.22 cnf(i_0_485, hypothesis, (i21!=i22)). % 61.41/8.22 cnf(i_0_487, hypothesis, (i20!=i29)). % 61.41/8.22 cnf(i_0_486, hypothesis, (i30!=i20)). % 61.41/8.22 cnf(i_0_488, hypothesis, (i20!=i28)). % 61.41/8.22 cnf(i_0_489, hypothesis, (i20!=i27)). % 61.41/8.22 cnf(i_0_490, hypothesis, (i20!=i26)). % 61.41/8.22 cnf(i_0_491, hypothesis, (i20!=i25)). % 61.41/8.22 cnf(i_0_492, hypothesis, (i20!=i24)). % 61.41/8.22 cnf(i_0_493, hypothesis, (i20!=i23)). % 61.41/8.22 cnf(i_0_494, hypothesis, (i20!=i22)). % 61.41/8.22 cnf(i_0_495, hypothesis, (i20!=i21)). % 61.41/8.22 cnf(i_0_497, hypothesis, (i19!=i29)). % 61.41/8.22 cnf(i_0_496, hypothesis, (i30!=i19)). % 61.41/8.22 cnf(i_0_498, hypothesis, (i19!=i28)). % 61.41/8.22 cnf(i_0_499, hypothesis, (i19!=i27)). % 61.41/8.22 cnf(i_0_500, hypothesis, (i19!=i26)). % 61.41/8.22 cnf(i_0_501, hypothesis, (i19!=i25)). % 61.41/8.22 cnf(i_0_502, hypothesis, (i19!=i24)). % 61.41/8.22 cnf(i_0_503, hypothesis, (i19!=i23)). % 61.41/8.22 cnf(i_0_504, hypothesis, (i19!=i22)). % 61.41/8.22 cnf(i_0_505, hypothesis, (i19!=i21)). % 61.41/8.22 cnf(i_0_506, hypothesis, (i19!=i20)). % 61.41/8.22 cnf(i_0_508, hypothesis, (i18!=i29)). % 61.41/8.22 cnf(i_0_507, hypothesis, (i30!=i18)). % 61.41/8.22 cnf(i_0_509, hypothesis, (i18!=i28)). % 61.41/8.22 cnf(i_0_510, hypothesis, (i18!=i27)). % 61.41/8.22 cnf(i_0_511, hypothesis, (i18!=i26)). % 61.41/8.22 cnf(i_0_512, hypothesis, (i18!=i25)). % 61.41/8.22 cnf(i_0_513, hypothesis, (i18!=i24)). % 61.41/8.22 cnf(i_0_514, hypothesis, (i18!=i23)). % 61.41/8.22 cnf(i_0_515, hypothesis, (i18!=i22)). % 61.41/8.22 cnf(i_0_516, hypothesis, (i18!=i21)). % 61.41/8.22 cnf(i_0_517, hypothesis, (i18!=i20)). % 61.41/8.22 cnf(i_0_518, hypothesis, (i18!=i19)). % 61.41/8.22 cnf(i_0_520, hypothesis, (i17!=i29)). % 61.41/8.22 cnf(i_0_519, hypothesis, (i30!=i17)). % 61.41/8.22 cnf(i_0_521, hypothesis, (i17!=i28)). % 61.41/8.22 cnf(i_0_522, hypothesis, (i17!=i27)). % 61.41/8.22 cnf(i_0_523, hypothesis, (i17!=i26)). % 61.41/8.22 cnf(i_0_524, hypothesis, (i17!=i25)). % 61.41/8.22 cnf(i_0_525, hypothesis, (i17!=i24)). % 61.41/8.22 cnf(i_0_526, hypothesis, (i17!=i23)). % 61.41/8.22 cnf(i_0_527, hypothesis, (i17!=i22)). % 61.41/8.22 cnf(i_0_528, hypothesis, (i17!=i21)). % 61.41/8.22 cnf(i_0_529, hypothesis, (i17!=i20)). % 61.41/8.22 cnf(i_0_530, hypothesis, (i17!=i19)). % 61.41/8.22 cnf(i_0_531, hypothesis, (i17!=i18)). % 61.41/8.22 cnf(i_0_533, hypothesis, (i16!=i29)). % 61.41/8.22 cnf(i_0_532, hypothesis, (i30!=i16)). % 61.41/8.22 cnf(i_0_534, hypothesis, (i16!=i28)). % 61.41/8.22 cnf(i_0_535, hypothesis, (i16!=i27)). % 61.41/8.22 cnf(i_0_536, hypothesis, (i16!=i26)). % 61.41/8.22 cnf(i_0_537, hypothesis, (i16!=i25)). % 61.41/8.22 cnf(i_0_538, hypothesis, (i16!=i24)). % 61.41/8.22 cnf(i_0_539, hypothesis, (i16!=i23)). % 61.41/8.22 cnf(i_0_540, hypothesis, (i16!=i22)). % 61.41/8.22 cnf(i_0_541, hypothesis, (i16!=i21)). % 61.41/8.22 cnf(i_0_542, hypothesis, (i16!=i20)). % 61.41/8.22 cnf(i_0_543, hypothesis, (i16!=i19)). % 61.41/8.22 cnf(i_0_544, hypothesis, (i16!=i18)). % 61.41/8.22 cnf(i_0_545, hypothesis, (i16!=i17)). % 61.41/8.22 cnf(i_0_547, hypothesis, (i15!=i29)). % 61.41/8.22 cnf(i_0_546, hypothesis, (i30!=i15)). % 61.41/8.22 cnf(i_0_548, hypothesis, (i15!=i28)). % 61.41/8.22 cnf(i_0_549, hypothesis, (i15!=i27)). % 61.41/8.22 cnf(i_0_550, hypothesis, (i15!=i26)). % 61.41/8.22 cnf(i_0_551, hypothesis, (i15!=i25)). % 61.41/8.22 cnf(i_0_552, hypothesis, (i15!=i24)). % 61.41/8.22 cnf(i_0_553, hypothesis, (i15!=i23)). % 61.41/8.22 cnf(i_0_554, hypothesis, (i15!=i22)). % 61.41/8.22 cnf(i_0_555, hypothesis, (i15!=i21)). % 61.41/8.22 cnf(i_0_556, hypothesis, (i15!=i20)). % 61.41/8.22 cnf(i_0_557, hypothesis, (i15!=i19)). % 61.41/8.22 cnf(i_0_558, hypothesis, (i15!=i18)). % 61.41/8.22 cnf(i_0_559, hypothesis, (i15!=i17)). % 61.41/8.22 cnf(i_0_560, hypothesis, (i15!=i16)). % 61.41/8.22 cnf(i_0_562, hypothesis, (i14!=i29)). % 61.41/8.22 cnf(i_0_561, hypothesis, (i30!=i14)). % 61.41/8.22 cnf(i_0_563, hypothesis, (i14!=i28)). % 61.41/8.22 cnf(i_0_564, hypothesis, (i14!=i27)). % 61.41/8.22 cnf(i_0_565, hypothesis, (i14!=i26)). % 61.41/8.22 cnf(i_0_566, hypothesis, (i14!=i25)). % 61.41/8.22 cnf(i_0_567, hypothesis, (i14!=i24)). % 61.41/8.22 cnf(i_0_568, hypothesis, (i14!=i23)). % 61.41/8.22 cnf(i_0_569, hypothesis, (i14!=i22)). % 61.41/8.22 cnf(i_0_570, hypothesis, (i14!=i21)). % 61.41/8.22 cnf(i_0_571, hypothesis, (i14!=i20)). % 61.41/8.22 cnf(i_0_572, hypothesis, (i14!=i19)). % 61.41/8.22 cnf(i_0_573, hypothesis, (i14!=i18)). % 61.41/8.22 cnf(i_0_574, hypothesis, (i14!=i17)). % 61.41/8.22 cnf(i_0_575, hypothesis, (i14!=i16)). % 61.41/8.22 cnf(i_0_576, hypothesis, (i14!=i15)). % 61.41/8.22 cnf(i_0_578, hypothesis, (i13!=i29)). % 61.41/8.22 cnf(i_0_577, hypothesis, (i30!=i13)). % 61.41/8.22 cnf(i_0_579, hypothesis, (i13!=i28)). % 61.41/8.22 cnf(i_0_580, hypothesis, (i13!=i27)). % 61.41/8.22 cnf(i_0_581, hypothesis, (i13!=i26)). % 61.41/8.22 cnf(i_0_582, hypothesis, (i13!=i25)). % 61.41/8.22 cnf(i_0_583, hypothesis, (i13!=i24)). % 61.41/8.22 cnf(i_0_584, hypothesis, (i13!=i23)). % 61.41/8.22 cnf(i_0_585, hypothesis, (i13!=i22)). % 61.41/8.22 cnf(i_0_586, hypothesis, (i13!=i21)). % 61.41/8.22 cnf(i_0_587, hypothesis, (i13!=i20)). % 61.41/8.22 cnf(i_0_588, hypothesis, (i13!=i19)). % 61.41/8.22 cnf(i_0_589, hypothesis, (i13!=i18)). % 61.41/8.22 cnf(i_0_590, hypothesis, (i13!=i17)). % 61.41/8.22 cnf(i_0_591, hypothesis, (i13!=i16)). % 61.41/8.22 cnf(i_0_592, hypothesis, (i13!=i15)). % 61.41/8.22 cnf(i_0_593, hypothesis, (i13!=i14)). % 61.41/8.22 cnf(i_0_595, hypothesis, (i12!=i29)). % 61.41/8.22 cnf(i_0_594, hypothesis, (i30!=i12)). % 61.41/8.22 cnf(i_0_596, hypothesis, (i12!=i28)). % 61.41/8.22 cnf(i_0_597, hypothesis, (i12!=i27)). % 61.41/8.22 cnf(i_0_598, hypothesis, (i12!=i26)). % 61.41/8.22 cnf(i_0_599, hypothesis, (i12!=i25)). % 61.41/8.22 cnf(i_0_600, hypothesis, (i12!=i24)). % 61.41/8.22 cnf(i_0_601, hypothesis, (i12!=i23)). % 61.41/8.22 cnf(i_0_602, hypothesis, (i12!=i22)). % 61.41/8.22 cnf(i_0_603, hypothesis, (i12!=i21)). % 61.41/8.22 cnf(i_0_604, hypothesis, (i12!=i20)). % 61.41/8.22 cnf(i_0_605, hypothesis, (i12!=i19)). % 61.41/8.22 cnf(i_0_606, hypothesis, (i12!=i18)). % 61.41/8.22 cnf(i_0_607, hypothesis, (i12!=i17)). % 61.41/8.22 cnf(i_0_608, hypothesis, (i12!=i16)). % 61.41/8.22 cnf(i_0_609, hypothesis, (i12!=i15)). % 61.41/8.22 cnf(i_0_610, hypothesis, (i12!=i14)). % 61.41/8.22 cnf(i_0_611, hypothesis, (i12!=i13)). % 61.41/8.22 cnf(i_0_613, hypothesis, (i11!=i29)). % 61.41/8.22 cnf(i_0_612, hypothesis, (i30!=i11)). % 61.41/8.22 cnf(i_0_614, hypothesis, (i11!=i28)). % 61.41/8.22 cnf(i_0_615, hypothesis, (i11!=i27)). % 61.41/8.22 cnf(i_0_616, hypothesis, (i11!=i26)). % 61.41/8.22 cnf(i_0_617, hypothesis, (i11!=i25)). % 61.41/8.22 cnf(i_0_618, hypothesis, (i11!=i24)). % 61.41/8.22 cnf(i_0_619, hypothesis, (i11!=i23)). % 61.41/8.22 cnf(i_0_620, hypothesis, (i11!=i22)). % 61.41/8.22 cnf(i_0_621, hypothesis, (i11!=i21)). % 61.41/8.22 cnf(i_0_622, hypothesis, (i11!=i20)). % 61.41/8.22 cnf(i_0_623, hypothesis, (i11!=i19)). % 61.41/8.22 cnf(i_0_624, hypothesis, (i11!=i18)). % 61.41/8.22 cnf(i_0_625, hypothesis, (i11!=i17)). % 61.41/8.22 cnf(i_0_626, hypothesis, (i11!=i16)). % 61.41/8.22 cnf(i_0_627, hypothesis, (i11!=i15)). % 61.41/8.22 cnf(i_0_628, hypothesis, (i11!=i14)). % 61.41/8.22 cnf(i_0_629, hypothesis, (i11!=i13)). % 61.41/8.22 cnf(i_0_630, hypothesis, (i11!=i12)). % 61.41/8.22 cnf(i_0_632, hypothesis, (i10!=i29)). % 61.41/8.22 cnf(i_0_631, hypothesis, (i30!=i10)). % 61.41/8.22 cnf(i_0_633, hypothesis, (i10!=i28)). % 61.41/8.22 cnf(i_0_634, hypothesis, (i10!=i27)). % 61.41/8.22 cnf(i_0_635, hypothesis, (i10!=i26)). % 61.41/8.22 cnf(i_0_636, hypothesis, (i10!=i25)). % 61.41/8.22 cnf(i_0_637, hypothesis, (i10!=i24)). % 61.41/8.22 cnf(i_0_638, hypothesis, (i10!=i23)). % 61.41/8.22 cnf(i_0_639, hypothesis, (i10!=i22)). % 61.41/8.22 cnf(i_0_640, hypothesis, (i10!=i21)). % 61.41/8.22 cnf(i_0_641, hypothesis, (i10!=i20)). % 61.41/8.22 cnf(i_0_642, hypothesis, (i10!=i19)). % 61.41/8.22 cnf(i_0_643, hypothesis, (i10!=i18)). % 61.41/8.22 cnf(i_0_644, hypothesis, (i10!=i17)). % 61.41/8.22 cnf(i_0_645, hypothesis, (i10!=i16)). % 61.41/8.22 cnf(i_0_646, hypothesis, (i10!=i15)). % 61.41/8.22 cnf(i_0_647, hypothesis, (i10!=i14)). % 61.41/8.22 cnf(i_0_648, hypothesis, (i10!=i13)). % 61.41/8.22 cnf(i_0_649, hypothesis, (i10!=i12)). % 61.41/8.22 cnf(i_0_650, hypothesis, (i10!=i11)). % 61.41/8.22 cnf(i_0_652, hypothesis, (i9!=i29)). % 61.41/8.22 cnf(i_0_651, hypothesis, (i30!=i9)). % 61.41/8.22 cnf(i_0_653, hypothesis, (i9!=i28)). % 61.41/8.22 cnf(i_0_654, hypothesis, (i9!=i27)). % 61.41/8.22 cnf(i_0_655, hypothesis, (i9!=i26)). % 61.41/8.22 cnf(i_0_656, hypothesis, (i9!=i25)). % 61.41/8.22 cnf(i_0_657, hypothesis, (i9!=i24)). % 61.41/8.22 cnf(i_0_658, hypothesis, (i9!=i23)). % 61.41/8.22 cnf(i_0_659, hypothesis, (i9!=i22)). % 61.41/8.22 cnf(i_0_660, hypothesis, (i9!=i21)). % 61.41/8.22 cnf(i_0_661, hypothesis, (i9!=i20)). % 61.41/8.22 cnf(i_0_662, hypothesis, (i9!=i19)). % 61.41/8.22 cnf(i_0_663, hypothesis, (i9!=i18)). % 61.41/8.22 cnf(i_0_664, hypothesis, (i9!=i17)). % 61.41/8.22 cnf(i_0_665, hypothesis, (i9!=i16)). % 61.41/8.22 cnf(i_0_666, hypothesis, (i9!=i15)). % 61.41/8.22 cnf(i_0_667, hypothesis, (i9!=i14)). % 61.41/8.22 cnf(i_0_668, hypothesis, (i9!=i13)). % 61.41/8.22 cnf(i_0_669, hypothesis, (i9!=i12)). % 61.41/8.22 cnf(i_0_670, hypothesis, (i9!=i11)). % 61.41/8.22 cnf(i_0_671, hypothesis, (i9!=i10)). % 61.41/8.22 cnf(i_0_673, hypothesis, (i8!=i29)). % 61.41/8.22 cnf(i_0_672, hypothesis, (i30!=i8)). % 61.41/8.22 cnf(i_0_674, hypothesis, (i8!=i28)). % 61.41/8.22 cnf(i_0_675, hypothesis, (i8!=i27)). % 61.41/8.22 cnf(i_0_676, hypothesis, (i8!=i26)). % 61.41/8.22 cnf(i_0_677, hypothesis, (i8!=i25)). % 61.41/8.22 cnf(i_0_678, hypothesis, (i8!=i24)). % 61.41/8.22 cnf(i_0_679, hypothesis, (i8!=i23)). % 61.41/8.22 cnf(i_0_680, hypothesis, (i8!=i22)). % 61.41/8.22 cnf(i_0_681, hypothesis, (i8!=i21)). % 61.41/8.22 cnf(i_0_682, hypothesis, (i8!=i20)). % 61.41/8.22 cnf(i_0_683, hypothesis, (i8!=i19)). % 61.41/8.22 cnf(i_0_684, hypothesis, (i8!=i18)). % 61.41/8.22 cnf(i_0_685, hypothesis, (i8!=i17)). % 61.41/8.22 cnf(i_0_686, hypothesis, (i8!=i16)). % 61.41/8.22 cnf(i_0_687, hypothesis, (i8!=i15)). % 61.41/8.22 cnf(i_0_688, hypothesis, (i8!=i14)). % 61.41/8.22 cnf(i_0_689, hypothesis, (i8!=i13)). % 61.41/8.22 cnf(i_0_690, hypothesis, (i8!=i12)). % 61.41/8.22 cnf(i_0_691, hypothesis, (i8!=i11)). % 61.41/8.22 cnf(i_0_692, hypothesis, (i8!=i10)). % 61.41/8.22 cnf(i_0_693, hypothesis, (i8!=i9)). % 61.41/8.22 cnf(i_0_695, hypothesis, (i7!=i29)). % 61.41/8.22 cnf(i_0_694, hypothesis, (i30!=i7)). % 61.41/8.22 cnf(i_0_696, hypothesis, (i7!=i28)). % 61.41/8.22 cnf(i_0_697, hypothesis, (i7!=i27)). % 61.41/8.22 cnf(i_0_698, hypothesis, (i7!=i26)). % 61.41/8.22 cnf(i_0_699, hypothesis, (i7!=i25)). % 61.41/8.22 cnf(i_0_700, hypothesis, (i7!=i24)). % 61.41/8.22 cnf(i_0_701, hypothesis, (i7!=i23)). % 61.41/8.22 cnf(i_0_702, hypothesis, (i7!=i22)). % 61.41/8.22 cnf(i_0_703, hypothesis, (i7!=i21)). % 61.41/8.22 cnf(i_0_704, hypothesis, (i7!=i20)). % 61.41/8.22 cnf(i_0_705, hypothesis, (i7!=i19)). % 61.41/8.22 cnf(i_0_706, hypothesis, (i7!=i18)). % 61.41/8.22 cnf(i_0_707, hypothesis, (i7!=i17)). % 61.41/8.22 cnf(i_0_708, hypothesis, (i7!=i16)). % 61.41/8.22 cnf(i_0_709, hypothesis, (i7!=i15)). % 61.41/8.22 cnf(i_0_710, hypothesis, (i7!=i14)). % 61.41/8.22 cnf(i_0_711, hypothesis, (i7!=i13)). % 61.41/8.22 cnf(i_0_712, hypothesis, (i7!=i12)). % 61.41/8.22 cnf(i_0_713, hypothesis, (i7!=i11)). % 61.41/8.22 cnf(i_0_714, hypothesis, (i7!=i10)). % 61.41/8.22 cnf(i_0_715, hypothesis, (i7!=i9)). % 61.41/8.22 cnf(i_0_716, hypothesis, (i7!=i8)). % 61.41/8.22 cnf(i_0_718, hypothesis, (i6!=i29)). % 61.41/8.22 cnf(i_0_717, hypothesis, (i30!=i6)). % 61.41/8.22 cnf(i_0_719, hypothesis, (i6!=i28)). % 61.41/8.22 cnf(i_0_720, hypothesis, (i6!=i27)). % 61.41/8.22 cnf(i_0_721, hypothesis, (i6!=i26)). % 61.41/8.22 cnf(i_0_722, hypothesis, (i6!=i25)). % 61.41/8.22 cnf(i_0_723, hypothesis, (i6!=i24)). % 61.41/8.22 cnf(i_0_724, hypothesis, (i6!=i23)). % 61.41/8.22 cnf(i_0_725, hypothesis, (i6!=i22)). % 61.41/8.22 cnf(i_0_726, hypothesis, (i6!=i21)). % 61.41/8.22 cnf(i_0_727, hypothesis, (i6!=i20)). % 61.41/8.22 cnf(i_0_728, hypothesis, (i6!=i19)). % 61.41/8.22 cnf(i_0_729, hypothesis, (i6!=i18)). % 61.41/8.22 cnf(i_0_730, hypothesis, (i6!=i17)). % 61.41/8.22 cnf(i_0_731, hypothesis, (i6!=i16)). % 61.41/8.22 cnf(i_0_732, hypothesis, (i6!=i15)). % 61.41/8.22 cnf(i_0_733, hypothesis, (i6!=i14)). % 61.41/8.22 cnf(i_0_734, hypothesis, (i6!=i13)). % 61.41/8.22 cnf(i_0_735, hypothesis, (i6!=i12)). % 61.41/8.22 cnf(i_0_736, hypothesis, (i6!=i11)). % 61.41/8.22 cnf(i_0_737, hypothesis, (i6!=i10)). % 61.41/8.22 cnf(i_0_738, hypothesis, (i6!=i9)). % 61.41/8.22 cnf(i_0_739, hypothesis, (i6!=i8)). % 61.41/8.22 cnf(i_0_740, hypothesis, (i6!=i7)). % 61.41/8.22 cnf(i_0_742, hypothesis, (i5!=i29)). % 61.41/8.22 cnf(i_0_741, hypothesis, (i30!=i5)). % 61.41/8.22 cnf(i_0_743, hypothesis, (i5!=i28)). % 61.41/8.22 cnf(i_0_744, hypothesis, (i5!=i27)). % 61.41/8.22 cnf(i_0_745, hypothesis, (i5!=i26)). % 61.41/8.22 cnf(i_0_746, hypothesis, (i5!=i25)). % 61.41/8.22 cnf(i_0_747, hypothesis, (i5!=i24)). % 61.41/8.22 cnf(i_0_748, hypothesis, (i5!=i23)). % 61.41/8.22 cnf(i_0_749, hypothesis, (i5!=i22)). % 61.41/8.22 cnf(i_0_750, hypothesis, (i5!=i21)). % 61.41/8.22 cnf(i_0_751, hypothesis, (i5!=i20)). % 61.41/8.22 cnf(i_0_752, hypothesis, (i5!=i19)). % 61.41/8.22 cnf(i_0_753, hypothesis, (i5!=i18)). % 61.41/8.22 cnf(i_0_754, hypothesis, (i5!=i17)). % 61.41/8.22 cnf(i_0_755, hypothesis, (i5!=i16)). % 61.41/8.22 cnf(i_0_756, hypothesis, (i5!=i15)). % 61.41/8.22 cnf(i_0_757, hypothesis, (i5!=i14)). % 61.41/8.22 cnf(i_0_758, hypothesis, (i5!=i13)). % 61.41/8.22 cnf(i_0_759, hypothesis, (i5!=i12)). % 61.41/8.22 cnf(i_0_760, hypothesis, (i5!=i11)). % 61.41/8.22 cnf(i_0_761, hypothesis, (i5!=i10)). % 61.41/8.22 cnf(i_0_762, hypothesis, (i5!=i9)). % 61.41/8.22 cnf(i_0_763, hypothesis, (i5!=i8)). % 61.41/8.22 cnf(i_0_764, hypothesis, (i5!=i7)). % 61.41/8.22 cnf(i_0_765, hypothesis, (i5!=i6)). % 61.41/8.22 cnf(i_0_767, hypothesis, (i4!=i29)). % 61.41/8.22 cnf(i_0_766, hypothesis, (i30!=i4)). % 61.41/8.22 cnf(i_0_768, hypothesis, (i4!=i28)). % 61.41/8.22 cnf(i_0_769, hypothesis, (i4!=i27)). % 61.41/8.22 cnf(i_0_770, hypothesis, (i4!=i26)). % 61.41/8.22 cnf(i_0_771, hypothesis, (i4!=i25)). % 61.41/8.22 cnf(i_0_772, hypothesis, (i4!=i24)). % 61.41/8.22 cnf(i_0_773, hypothesis, (i4!=i23)). % 61.41/8.22 cnf(i_0_774, hypothesis, (i4!=i22)). % 61.41/8.22 cnf(i_0_775, hypothesis, (i4!=i21)). % 61.41/8.22 cnf(i_0_776, hypothesis, (i4!=i20)). % 61.41/8.22 cnf(i_0_777, hypothesis, (i4!=i19)). % 61.41/8.22 cnf(i_0_778, hypothesis, (i4!=i18)). % 61.41/8.22 cnf(i_0_779, hypothesis, (i4!=i17)). % 61.41/8.22 cnf(i_0_780, hypothesis, (i4!=i16)). % 61.41/8.22 cnf(i_0_781, hypothesis, (i4!=i15)). % 61.41/8.22 cnf(i_0_782, hypothesis, (i4!=i14)). % 61.41/8.22 cnf(i_0_783, hypothesis, (i4!=i13)). % 61.41/8.22 cnf(i_0_784, hypothesis, (i4!=i12)). % 61.41/8.22 cnf(i_0_785, hypothesis, (i4!=i11)). % 61.41/8.22 cnf(i_0_786, hypothesis, (i4!=i10)). % 61.41/8.22 cnf(i_0_787, hypothesis, (i4!=i9)). % 61.41/8.22 cnf(i_0_788, hypothesis, (i4!=i8)). % 61.41/8.22 cnf(i_0_789, hypothesis, (i4!=i7)). % 61.41/8.22 cnf(i_0_790, hypothesis, (i4!=i6)). % 61.41/8.22 cnf(i_0_791, hypothesis, (i4!=i5)). % 61.41/8.22 cnf(i_0_793, hypothesis, (i3!=i29)). % 61.41/8.22 cnf(i_0_792, hypothesis, (i30!=i3)). % 61.41/8.22 cnf(i_0_794, hypothesis, (i3!=i28)). % 61.41/8.22 cnf(i_0_795, hypothesis, (i3!=i27)). % 61.41/8.22 cnf(i_0_796, hypothesis, (i3!=i26)). % 61.41/8.22 cnf(i_0_797, hypothesis, (i3!=i25)). % 61.41/8.22 cnf(i_0_798, hypothesis, (i3!=i24)). % 61.41/8.22 cnf(i_0_799, hypothesis, (i3!=i23)). % 61.41/8.22 cnf(i_0_800, hypothesis, (i3!=i22)). % 61.41/8.22 cnf(i_0_801, hypothesis, (i3!=i21)). % 61.41/8.22 cnf(i_0_802, hypothesis, (i3!=i20)). % 61.41/8.22 cnf(i_0_803, hypothesis, (i3!=i19)). % 61.41/8.22 cnf(i_0_804, hypothesis, (i3!=i18)). % 61.41/8.22 cnf(i_0_805, hypothesis, (i3!=i17)). % 61.41/8.22 cnf(i_0_806, hypothesis, (i3!=i16)). % 61.41/8.22 cnf(i_0_807, hypothesis, (i3!=i15)). % 61.41/8.22 cnf(i_0_808, hypothesis, (i3!=i14)). % 61.41/8.22 cnf(i_0_809, hypothesis, (i3!=i13)). % 61.41/8.22 cnf(i_0_810, hypothesis, (i3!=i12)). % 61.41/8.22 cnf(i_0_811, hypothesis, (i3!=i11)). % 61.41/8.22 cnf(i_0_812, hypothesis, (i3!=i10)). % 61.41/8.22 cnf(i_0_813, hypothesis, (i3!=i9)). % 61.41/8.22 cnf(i_0_814, hypothesis, (i3!=i8)). % 61.41/8.22 cnf(i_0_815, hypothesis, (i3!=i7)). % 61.41/8.22 cnf(i_0_816, hypothesis, (i3!=i6)). % 61.41/8.22 cnf(i_0_817, hypothesis, (i3!=i5)). % 61.41/8.22 cnf(i_0_818, hypothesis, (i3!=i4)). % 61.41/8.22 cnf(i_0_820, hypothesis, (i2!=i29)). % 61.41/8.22 cnf(i_0_819, hypothesis, (i30!=i2)). % 61.41/8.22 cnf(i_0_821, hypothesis, (i2!=i28)). % 61.41/8.22 cnf(i_0_822, hypothesis, (i2!=i27)). % 61.41/8.22 cnf(i_0_823, hypothesis, (i2!=i26)). % 61.41/8.22 cnf(i_0_824, hypothesis, (i2!=i25)). % 61.41/8.22 cnf(i_0_825, hypothesis, (i2!=i24)). % 61.41/8.22 cnf(i_0_826, hypothesis, (i2!=i23)). % 61.41/8.22 cnf(i_0_827, hypothesis, (i2!=i22)). % 61.41/8.22 cnf(i_0_828, hypothesis, (i2!=i21)). % 61.41/8.22 cnf(i_0_829, hypothesis, (i2!=i20)). % 61.41/8.22 cnf(i_0_830, hypothesis, (i2!=i19)). % 61.41/8.22 cnf(i_0_831, hypothesis, (i2!=i18)). % 61.41/8.22 cnf(i_0_832, hypothesis, (i2!=i17)). % 61.41/8.22 cnf(i_0_833, hypothesis, (i2!=i16)). % 61.41/8.22 cnf(i_0_834, hypothesis, (i2!=i15)). % 61.41/8.22 cnf(i_0_835, hypothesis, (i2!=i14)). % 61.41/8.22 cnf(i_0_836, hypothesis, (i2!=i13)). % 61.41/8.22 cnf(i_0_837, hypothesis, (i2!=i12)). % 61.41/8.22 cnf(i_0_838, hypothesis, (i2!=i11)). % 61.41/8.22 cnf(i_0_839, hypothesis, (i2!=i10)). % 61.41/8.22 cnf(i_0_840, hypothesis, (i2!=i9)). % 61.41/8.22 cnf(i_0_841, hypothesis, (i2!=i8)). % 61.41/8.22 cnf(i_0_842, hypothesis, (i2!=i7)). % 61.41/8.22 cnf(i_0_843, hypothesis, (i2!=i6)). % 61.41/8.22 cnf(i_0_844, hypothesis, (i2!=i5)). % 61.41/8.22 cnf(i_0_845, hypothesis, (i2!=i4)). % 61.41/8.22 cnf(i_0_846, hypothesis, (i2!=i3)). % 61.41/8.22 cnf(i_0_848, hypothesis, (i29!=i1)). % 61.41/8.22 cnf(i_0_847, hypothesis, (i30!=i1)). % 61.41/8.22 cnf(i_0_849, hypothesis, (i28!=i1)). % 61.41/8.22 cnf(i_0_850, hypothesis, (i27!=i1)). % 61.41/8.22 cnf(i_0_851, hypothesis, (i26!=i1)). % 61.41/8.22 cnf(i_0_852, hypothesis, (i25!=i1)). % 61.41/8.22 cnf(i_0_853, hypothesis, (i24!=i1)). % 61.41/8.22 cnf(i_0_854, hypothesis, (i23!=i1)). % 61.41/8.22 cnf(i_0_855, hypothesis, (i22!=i1)). % 61.41/8.22 cnf(i_0_856, hypothesis, (i21!=i1)). % 61.41/8.22 cnf(i_0_857, hypothesis, (i20!=i1)). % 61.41/8.22 cnf(i_0_858, hypothesis, (i19!=i1)). % 61.41/8.22 cnf(i_0_859, hypothesis, (i18!=i1)). % 61.41/8.22 cnf(i_0_860, hypothesis, (i17!=i1)). % 61.41/8.22 cnf(i_0_861, hypothesis, (i16!=i1)). % 61.41/8.22 cnf(i_0_862, hypothesis, (i15!=i1)). % 61.41/8.22 cnf(i_0_863, hypothesis, (i14!=i1)). % 61.41/8.22 cnf(i_0_864, hypothesis, (i13!=i1)). % 61.41/8.22 cnf(i_0_865, hypothesis, (i12!=i1)). % 61.41/8.22 cnf(i_0_866, hypothesis, (i11!=i1)). % 61.41/8.22 cnf(i_0_867, hypothesis, (i10!=i1)). % 61.41/8.22 cnf(i_0_868, hypothesis, (i9!=i1)). % 61.41/8.22 cnf(i_0_869, hypothesis, (i8!=i1)). % 61.41/8.22 cnf(i_0_870, hypothesis, (i7!=i1)). % 61.41/8.22 cnf(i_0_871, hypothesis, (i6!=i1)). % 61.41/8.22 cnf(i_0_872, hypothesis, (i5!=i1)). % 61.41/8.22 cnf(i_0_873, hypothesis, (i4!=i1)). % 61.41/8.22 cnf(i_0_874, hypothesis, (i3!=i1)). % 61.41/8.22 cnf(i_0_875, hypothesis, (i2!=i1)). % 61.41/8.22 cnf(i_0_876, negated_conjecture, (select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,i13,e13),i1,e1),i19,e19),i4,e4),i9,e9),i30,e30),i2,e2),i15,e15),i25,e25),i18,e18),i20,e20),i8,e8),i21,e21),i6,e6),i11,e11),i14,e14),i29,e29),i5,e5),i26,e26),i22,e22),i27,e27),i3,e3),i12,e12),i16,e16),i28,e28),i17,e17),i23,e23),i24,e24),i7,e7),i10,e10),sk(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,i1,e1),i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i13,e13),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i1,e1),store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,i13,e13),i1,e1),i19,e19),i4,e4),i9,e9),i30,e30),i2,e2),i15,e15),i25,e25),i18,e18),i20,e20),i8,e8),i21,e21),i6,e6),i11,e11),i14,e14),i29,e29),i5,e5),i26,e26),i22,e22),i27,e27),i3,e3),i12,e12),i16,e16),i28,e28),i17,e17),i23,e23),i24,e24),i7,e7),i10,e10)))!=select(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,i1,e1),i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i13,e13),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i1,e1),sk(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,i1,e1),i2,e2),i3,e3),i4,e4),i5,e5),i6,e6),i7,e7),i8,e8),i9,e9),i10,e10),i11,e11),i12,e12),i13,e13),i14,e14),i15,e15),i16,e16),i17,e17),i18,e18),i19,e19),i20,e20),i21,e21),i22,e22),i23,e23),i24,e24),i25,e25),i26,e26),i27,e27),i28,e28),i29,e29),i1,e1),store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(store(a1,i13,e13),i1,e1),i19,e19),i4,e4),i9,e9),i30,e30),i2,e2),i15,e15),i25,e25),i18,e18),i20,e20),i8,e8),i21,e21),i6,e6),i11,e11),i14,e14),i29,e29),i5,e5),i26,e26),i22,e22),i27,e27),i3,e3),i12,e12),i16,e16),i28,e28),i17,e17),i23,e23),i24,e24),i7,e7),i10,e10))))). % 61.41/8.22 cnf(i_0_440, plain, (select(store(X1,X2,X3),X4)=select(X1,X4)|X2=X4)). % 61.41/8.22 cnf(i_0_882, plain, (X5=X5)). % 61.41/8.22 # End listing active clauses. There is an equivalent clause to each of these in the clausification! % 61.41/8.22 # Begin printing tableau % 61.41/8.22 # Found 5 steps % 61.41/8.22 cnf(i_0_439, plain, (select(store(X11,X12,X7),X12)=X7), inference(start_rule)). % 61.41/8.22 cnf(i_0_889, plain, (select(store(X11,X12,X7),X12)=X7), inference(extension_rule, [i_0_887])). % 61.41/8.22 cnf(i_0_1343, plain, (select(store(X1,X7,store(X1,X7,X8)),X7)!=store(X1,X7,X8)), inference(closure_rule, [i_0_439])). % 61.41/8.22 cnf(i_0_1342, plain, (select(select(store(X1,X7,store(X1,X7,X8)),X7),select(store(X11,X12,X7),X12))=select(store(X1,X7,X8),X7)), inference(extension_rule, [i_0_885])). % 61.41/8.22 cnf(i_0_1356, plain, (select(store(X1,X7,X8),X7)!=X8), inference(closure_rule, [i_0_439])). % 61.41/8.22 # End printing tableau % 61.41/8.22 # SZS output end % 61.41/8.22 # Branches closed with saturation will be marked with an "s" % 61.41/8.23 # Child (11858) has found a proof. % 61.41/8.23 % 61.41/8.24 # Proof search is over... % 61.41/8.24 # Freeing feature tree %------------------------------------------------------------------------------