%------------------------------------------------------------------------------ % File : Etableau---0.67 % Problem : SWV571-1.049 : 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 : n026.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:22:43 EDT 2022 % Result : Unsatisfiable 0.19s 0.53s % Output : CNFRefutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWV571-1.049 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.13 % Command : etableau --auto --tsmdo --quicksat=10000 --tableau=1 --tableau-saturation=1 -s -p --tableau-cores=8 --cpu-limit=%d %s % 0.12/0.33 % Computer : n026.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Wed Jun 15 08:09:22 EDT 2022 % 0.12/0.34 % CPUTime : % 0.19/0.38 # No SInE strategy applied % 0.19/0.38 # Auto-Mode selected heuristic G_E___208_C18_F1_SE_CS_SP_PS_S5PRR_RG_S04AN % 0.19/0.38 # and selection function SelectComplexExceptUniqMaxHorn. % 0.19/0.38 # % 0.19/0.38 # Presaturation interreduction done % 0.19/0.38 # Number of axioms: 363 Number of unprocessed: 363 % 0.19/0.38 # Tableaux proof search. % 0.19/0.38 # APR header successfully linked. % 0.19/0.38 # Hello from C++ % 0.19/0.47 # The folding up rule is enabled... % 0.19/0.47 # Local unification is enabled... % 0.19/0.47 # Any saturation attempts will use folding labels... % 0.19/0.47 # 363 beginning clauses after preprocessing and clausification % 0.19/0.47 # Creating start rules for all 1 conjectures. % 0.19/0.47 # There are 1 start rule candidates: % 0.19/0.47 # Found 362 unit axioms. % 0.19/0.47 # 1 start rule tableaux created. % 0.19/0.47 # 1 extension rule candidate clauses % 0.19/0.47 # 362 unit axiom clauses % 0.19/0.47 % 0.19/0.47 # Requested 8, 32 cores available to the main process. % 0.19/0.47 # There are not enough tableaux to fork, creating more from the initial 1 % 0.19/0.47 # Creating equality axioms % 0.19/0.47 # Ran out of tableaux, making start rules for all clauses % 0.19/0.47 # Returning from population with 372 new_tableaux and 0 remaining starting tableaux. % 0.19/0.47 # We now have 372 tableaux to operate on % 0.19/0.53 # There were 1 total branch saturation attempts. % 0.19/0.53 # There were 0 of these attempts blocked. % 0.19/0.53 # There were 0 deferred branch saturation attempts. % 0.19/0.53 # There were 0 free duplicated saturations. % 0.19/0.53 # There were 1 total successful branch saturations. % 0.19/0.53 # There were 0 successful branch saturations in interreduction. % 0.19/0.53 # There were 0 successful branch saturations on the branch. % 0.19/0.53 # There were 1 successful branch saturations after the branch. % 0.19/0.53 # SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.53 # SZS output start for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.53 # Begin clausification derivation % 0.19/0.53 % 0.19/0.53 # End clausification derivation % 0.19/0.53 # Begin listing active clauses obtained from FOF to CNF conversion % 0.19/0.53 cnf(i_0_676, hypothesis, (queue_1=q0)). % 0.19/0.53 cnf(i_0_693, hypothesis, (queue_103=q24)). % 0.19/0.53 cnf(i_0_694, hypothesis, (queue_109=q25)). % 0.19/0.53 cnf(i_0_695, hypothesis, (queue_115=q26)). % 0.19/0.53 cnf(i_0_696, hypothesis, (queue_121=q27)). % 0.19/0.53 cnf(i_0_697, hypothesis, (queue_127=q28)). % 0.19/0.53 cnf(i_0_678, hypothesis, (queue_13=q10)). % 0.19/0.53 cnf(i_0_698, hypothesis, (queue_133=q29)). % 0.19/0.53 cnf(i_0_699, hypothesis, (queue_139=q3)). % 0.19/0.53 cnf(i_0_700, hypothesis, (queue_145=q30)). % 0.19/0.53 cnf(i_0_701, hypothesis, (queue_151=q31)). % 0.19/0.53 cnf(i_0_702, hypothesis, (queue_157=q32)). % 0.19/0.53 cnf(i_0_703, hypothesis, (queue_163=q33)). % 0.19/0.53 cnf(i_0_704, hypothesis, (queue_169=q34)). % 0.19/0.53 cnf(i_0_705, hypothesis, (queue_175=q35)). % 0.19/0.53 cnf(i_0_706, hypothesis, (queue_181=q36)). % 0.19/0.53 cnf(i_0_707, hypothesis, (queue_187=q37)). % 0.19/0.53 cnf(i_0_679, hypothesis, (queue_19=q11)). % 0.19/0.53 cnf(i_0_708, hypothesis, (queue_193=q38)). % 0.19/0.53 cnf(i_0_709, hypothesis, (queue_199=q39)). % 0.19/0.53 cnf(i_0_710, hypothesis, (queue_205=q4)). % 0.19/0.53 cnf(i_0_711, hypothesis, (queue_211=q40)). % 0.19/0.53 cnf(i_0_712, hypothesis, (queue_217=q41)). % 0.19/0.53 cnf(i_0_713, hypothesis, (queue_223=q42)). % 0.19/0.53 cnf(i_0_714, hypothesis, (queue_229=q43)). % 0.19/0.53 cnf(i_0_715, hypothesis, (queue_235=q44)). % 0.19/0.53 cnf(i_0_716, hypothesis, (queue_241=q45)). % 0.19/0.53 cnf(i_0_717, hypothesis, (queue_247=q46)). % 0.19/0.53 cnf(i_0_680, hypothesis, (queue_25=q12)). % 0.19/0.53 cnf(i_0_718, hypothesis, (queue_253=q47)). % 0.19/0.53 cnf(i_0_719, hypothesis, (queue_259=q48)). % 0.19/0.53 cnf(i_0_720, hypothesis, (queue_265=q49)). % 0.19/0.53 cnf(i_0_721, hypothesis, (queue_271=q5)). % 0.19/0.53 cnf(i_0_722, hypothesis, (queue_277=q6)). % 0.19/0.53 cnf(i_0_723, hypothesis, (queue_283=q7)). % 0.19/0.53 cnf(i_0_724, hypothesis, (queue_289=q8)). % 0.19/0.53 cnf(i_0_725, hypothesis, (queue_295=q9)). % 0.19/0.53 cnf(i_0_681, hypothesis, (queue_31=q13)). % 0.19/0.53 cnf(i_0_682, hypothesis, (queue_37=q14)). % 0.19/0.53 cnf(i_0_683, hypothesis, (queue_43=q15)). % 0.19/0.53 cnf(i_0_684, hypothesis, (queue_49=q16)). % 0.19/0.53 cnf(i_0_685, hypothesis, (queue_55=q17)). % 0.19/0.53 cnf(i_0_686, hypothesis, (queue_61=q18)). % 0.19/0.53 cnf(i_0_687, hypothesis, (queue_67=q19)). % 0.19/0.53 cnf(i_0_677, hypothesis, (queue_7=q1)). % 0.19/0.53 cnf(i_0_688, hypothesis, (queue_73=q2)). % 0.19/0.53 cnf(i_0_689, hypothesis, (queue_79=q20)). % 0.19/0.53 cnf(i_0_690, hypothesis, (queue_85=q21)). % 0.19/0.53 cnf(i_0_691, hypothesis, (queue_91=q22)). % 0.19/0.53 cnf(i_0_692, hypothesis, (queue_97=q23)). % 0.19/0.53 cnf(i_0_476, hypothesis, (s(index_99)=index_102)). % 0.19/0.53 cnf(i_0_478, hypothesis, (s(index_105)=index_108)). % 0.19/0.53 cnf(i_0_480, hypothesis, (s(index_111)=index_114)). % 0.19/0.53 cnf(i_0_482, hypothesis, (s(index_9)=index_12)). % 0.19/0.53 cnf(i_0_483, hypothesis, (s(index_117)=index_120)). % 0.19/0.53 cnf(i_0_485, hypothesis, (s(index_123)=index_126)). % 0.19/0.53 cnf(i_0_487, hypothesis, (s(index_129)=index_132)). % 0.19/0.53 cnf(i_0_489, hypothesis, (s(index_135)=index_138)). % 0.19/0.53 cnf(i_0_491, hypothesis, (s(index_141)=index_144)). % 0.19/0.53 cnf(i_0_494, hypothesis, (s(index_147)=index_150)). % 0.19/0.53 cnf(i_0_496, hypothesis, (s(index_153)=index_156)). % 0.19/0.53 cnf(i_0_498, hypothesis, (s(index_159)=index_162)). % 0.19/0.53 cnf(i_0_500, hypothesis, (s(index_165)=index_168)). % 0.19/0.53 cnf(i_0_502, hypothesis, (s(index_171)=index_174)). % 0.19/0.53 cnf(i_0_504, hypothesis, (s(index_15)=index_18)). % 0.19/0.53 cnf(i_0_505, hypothesis, (s(index_177)=index_180)). % 0.19/0.53 cnf(i_0_507, hypothesis, (s(index_183)=index_186)). % 0.19/0.53 cnf(i_0_509, hypothesis, (s(index_189)=index_192)). % 0.19/0.53 cnf(i_0_511, hypothesis, (s(index_195)=index_198)). % 0.19/0.53 cnf(i_0_513, hypothesis, (s(index_201)=index_204)). % 0.19/0.53 cnf(i_0_516, hypothesis, (s(index_207)=index_210)). % 0.19/0.53 cnf(i_0_518, hypothesis, (s(index_213)=index_216)). % 0.19/0.53 cnf(i_0_520, hypothesis, (s(index_219)=index_222)). % 0.19/0.53 cnf(i_0_522, hypothesis, (s(index_225)=index_228)). % 0.19/0.53 cnf(i_0_524, hypothesis, (s(index_231)=index_234)). % 0.19/0.53 cnf(i_0_526, hypothesis, (s(index_21)=index_24)). % 0.19/0.53 cnf(i_0_527, hypothesis, (s(index_237)=index_240)). % 0.19/0.53 cnf(i_0_529, hypothesis, (s(index_243)=index_246)). % 0.19/0.53 cnf(i_0_531, hypothesis, (s(index_249)=index_252)). % 0.19/0.53 cnf(i_0_533, hypothesis, (s(index_255)=index_258)). % 0.19/0.53 cnf(i_0_535, hypothesis, (s(index_261)=index_264)). % 0.19/0.53 cnf(i_0_538, hypothesis, (s(index_267)=index_270)). % 0.19/0.53 cnf(i_0_540, hypothesis, (s(index_273)=index_276)). % 0.19/0.53 cnf(i_0_542, hypothesis, (s(index_279)=index_282)). % 0.19/0.53 cnf(i_0_544, hypothesis, (s(index_285)=index_288)). % 0.19/0.53 cnf(i_0_546, hypothesis, (s(index_291)=index_294)). % 0.19/0.53 cnf(i_0_550, hypothesis, (s(index_27)=index_30)). % 0.19/0.53 cnf(i_0_553, hypothesis, (s(index_33)=index_36)). % 0.19/0.53 cnf(i_0_555, hypothesis, (s(index_39)=index_42)). % 0.19/0.53 cnf(i_0_557, hypothesis, (s(index_45)=index_48)). % 0.19/0.53 cnf(i_0_559, hypothesis, (s(index_51)=index_54)). % 0.19/0.53 cnf(i_0_561, hypothesis, (s(index_3)=index_6)). % 0.19/0.53 cnf(i_0_562, hypothesis, (s(index_57)=index_60)). % 0.19/0.53 cnf(i_0_564, hypothesis, (s(index_63)=index_66)). % 0.19/0.53 cnf(i_0_566, hypothesis, (s(index_69)=index_72)). % 0.19/0.53 cnf(i_0_568, hypothesis, (s(index_75)=index_78)). % 0.19/0.53 cnf(i_0_570, hypothesis, (s(index_81)=index_84)). % 0.19/0.53 cnf(i_0_573, hypothesis, (s(index_87)=index_90)). % 0.19/0.53 cnf(i_0_575, hypothesis, (s(index_93)=index_96)). % 0.19/0.53 cnf(i_0_551, hypothesis, (s(index_300)=index_299)). % 0.19/0.53 cnf(i_0_370, plain, (s(p(X1))=X1)). % 0.19/0.53 cnf(i_0_369, plain, (p(s(X1))=X1)). % 0.19/0.53 cnf(i_0_465, hypothesis, (select(q9,seq)=earray_8)). % 0.19/0.53 cnf(i_0_572, hypothesis, (select(q9,tail)=index_9)). % 0.19/0.53 cnf(i_0_473, hypothesis, (select(earray_296,index_297)=elem_298)). % 0.19/0.53 cnf(i_0_474, hypothesis, (select(earray_296,index_300)=elem_301)). % 0.19/0.53 cnf(i_0_472, hypothesis, (select(q23,seq)=earray_98)). % 0.19/0.53 cnf(i_0_576, hypothesis, (select(q23,tail)=index_99)). % 0.19/0.53 cnf(i_0_376, hypothesis, (select(q24,seq)=earray_104)). % 0.19/0.53 cnf(i_0_477, hypothesis, (select(q24,tail)=index_105)). % 0.19/0.53 cnf(i_0_378, hypothesis, (select(q25,seq)=earray_110)). % 0.19/0.53 cnf(i_0_479, hypothesis, (select(q25,tail)=index_111)). % 0.19/0.53 cnf(i_0_380, hypothesis, (select(q26,seq)=earray_116)). % 0.19/0.53 cnf(i_0_481, hypothesis, (select(q26,tail)=index_117)). % 0.19/0.53 cnf(i_0_382, hypothesis, (select(q27,seq)=earray_122)). % 0.19/0.53 cnf(i_0_484, hypothesis, (select(q27,tail)=index_123)). % 0.19/0.53 cnf(i_0_384, hypothesis, (select(q28,seq)=earray_128)). % 0.19/0.53 cnf(i_0_486, hypothesis, (select(q28,tail)=index_129)). % 0.19/0.53 cnf(i_0_386, hypothesis, (select(q2,seq)=earray_134)). % 0.19/0.53 cnf(i_0_488, hypothesis, (select(q2,tail)=index_135)). % 0.19/0.53 cnf(i_0_388, hypothesis, (select(q10,seq)=earray_14)). % 0.19/0.53 cnf(i_0_389, hypothesis, (select(q29,seq)=earray_140)). % 0.19/0.53 cnf(i_0_490, hypothesis, (select(q29,tail)=index_141)). % 0.19/0.53 cnf(i_0_391, hypothesis, (select(q30,seq)=earray_146)). % 0.19/0.53 cnf(i_0_492, hypothesis, (select(q30,tail)=index_147)). % 0.19/0.53 cnf(i_0_393, hypothesis, (select(q31,seq)=earray_152)). % 0.19/0.53 cnf(i_0_495, hypothesis, (select(q31,tail)=index_153)). % 0.19/0.53 cnf(i_0_395, hypothesis, (select(q32,seq)=earray_158)). % 0.19/0.53 cnf(i_0_493, hypothesis, (select(q10,tail)=index_15)). % 0.19/0.53 cnf(i_0_497, hypothesis, (select(q32,tail)=index_159)). % 0.19/0.53 cnf(i_0_398, hypothesis, (select(q33,seq)=earray_164)). % 0.19/0.53 cnf(i_0_499, hypothesis, (select(q33,tail)=index_165)). % 0.19/0.53 cnf(i_0_400, hypothesis, (select(q34,seq)=earray_170)). % 0.19/0.53 cnf(i_0_501, hypothesis, (select(q34,tail)=index_171)). % 0.19/0.53 cnf(i_0_402, hypothesis, (select(q35,seq)=earray_176)). % 0.19/0.53 cnf(i_0_503, hypothesis, (select(q35,tail)=index_177)). % 0.19/0.53 cnf(i_0_404, hypothesis, (select(q36,seq)=earray_182)). % 0.19/0.53 cnf(i_0_506, hypothesis, (select(q36,tail)=index_183)). % 0.19/0.53 cnf(i_0_406, hypothesis, (select(q37,seq)=earray_188)). % 0.19/0.53 cnf(i_0_508, hypothesis, (select(q37,tail)=index_189)). % 0.19/0.53 cnf(i_0_408, hypothesis, (select(q38,seq)=earray_194)). % 0.19/0.53 cnf(i_0_510, hypothesis, (select(q38,tail)=index_195)). % 0.19/0.53 cnf(i_0_410, hypothesis, (select(q0,seq)=earray_2)). % 0.19/0.53 cnf(i_0_411, hypothesis, (select(q11,seq)=earray_20)). % 0.19/0.53 cnf(i_0_412, hypothesis, (select(q3,seq)=earray_200)). % 0.19/0.53 cnf(i_0_512, hypothesis, (select(q3,tail)=index_201)). % 0.19/0.53 cnf(i_0_414, hypothesis, (select(q39,seq)=earray_206)). % 0.19/0.53 cnf(i_0_514, hypothesis, (select(q39,tail)=index_207)). % 0.19/0.53 cnf(i_0_416, hypothesis, (select(q40,seq)=earray_212)). % 0.19/0.53 cnf(i_0_517, hypothesis, (select(q40,tail)=index_213)). % 0.19/0.53 cnf(i_0_418, hypothesis, (select(q41,seq)=earray_218)). % 0.19/0.53 cnf(i_0_515, hypothesis, (select(q11,tail)=index_21)). % 0.19/0.53 cnf(i_0_519, hypothesis, (select(q41,tail)=index_219)). % 0.19/0.53 cnf(i_0_421, hypothesis, (select(q42,seq)=earray_224)). % 0.19/0.53 cnf(i_0_521, hypothesis, (select(q42,tail)=index_225)). % 0.19/0.53 cnf(i_0_423, hypothesis, (select(q43,seq)=earray_230)). % 0.19/0.53 cnf(i_0_523, hypothesis, (select(q43,tail)=index_231)). % 0.19/0.53 cnf(i_0_425, hypothesis, (select(q44,seq)=earray_236)). % 0.19/0.53 cnf(i_0_525, hypothesis, (select(q44,tail)=index_237)). % 0.19/0.53 cnf(i_0_427, hypothesis, (select(q45,seq)=earray_242)). % 0.19/0.53 cnf(i_0_528, hypothesis, (select(q45,tail)=index_243)). % 0.19/0.53 cnf(i_0_429, hypothesis, (select(q46,seq)=earray_248)). % 0.19/0.53 cnf(i_0_530, hypothesis, (select(q46,tail)=index_249)). % 0.19/0.53 cnf(i_0_431, hypothesis, (select(q47,seq)=earray_254)). % 0.19/0.53 cnf(i_0_532, hypothesis, (select(q47,tail)=index_255)). % 0.19/0.53 cnf(i_0_433, hypothesis, (select(q12,seq)=earray_26)). % 0.19/0.53 cnf(i_0_434, hypothesis, (select(q48,seq)=earray_260)). % 0.19/0.53 cnf(i_0_534, hypothesis, (select(q48,tail)=index_261)). % 0.19/0.53 cnf(i_0_436, hypothesis, (select(q4,seq)=earray_266)). % 0.19/0.53 cnf(i_0_536, hypothesis, (select(q4,tail)=index_267)). % 0.19/0.53 cnf(i_0_438, hypothesis, (select(q5,seq)=earray_272)). % 0.19/0.53 cnf(i_0_539, hypothesis, (select(q5,tail)=index_273)). % 0.19/0.53 cnf(i_0_440, hypothesis, (select(q6,seq)=earray_278)). % 0.19/0.53 cnf(i_0_537, hypothesis, (select(q12,tail)=index_27)). % 0.19/0.53 cnf(i_0_541, hypothesis, (select(q6,tail)=index_279)). % 0.19/0.53 cnf(i_0_443, hypothesis, (select(q7,seq)=earray_284)). % 0.19/0.53 cnf(i_0_543, hypothesis, (select(q7,tail)=index_285)). % 0.19/0.53 cnf(i_0_445, hypothesis, (select(q8,seq)=earray_290)). % 0.19/0.53 cnf(i_0_545, hypothesis, (select(q8,tail)=index_291)). % 0.19/0.53 cnf(i_0_447, hypothesis, (select(q49,seq)=earray_296)). % 0.19/0.53 cnf(i_0_448, hypothesis, (select(q13,seq)=earray_32)). % 0.19/0.53 cnf(i_0_552, hypothesis, (select(q13,tail)=index_33)). % 0.19/0.53 cnf(i_0_450, hypothesis, (select(q14,seq)=earray_38)). % 0.19/0.53 cnf(i_0_549, hypothesis, (select(q0,tail)=index_3)). % 0.19/0.53 cnf(i_0_554, hypothesis, (select(q14,tail)=index_39)). % 0.19/0.53 cnf(i_0_453, hypothesis, (select(q15,seq)=earray_44)). % 0.19/0.53 cnf(i_0_556, hypothesis, (select(q15,tail)=index_45)). % 0.19/0.53 cnf(i_0_455, hypothesis, (select(q16,seq)=earray_50)). % 0.19/0.53 cnf(i_0_558, hypothesis, (select(q16,tail)=index_51)). % 0.19/0.53 cnf(i_0_457, hypothesis, (select(q17,seq)=earray_56)). % 0.19/0.53 cnf(i_0_560, hypothesis, (select(q17,tail)=index_57)). % 0.19/0.53 cnf(i_0_459, hypothesis, (select(q18,seq)=earray_62)). % 0.19/0.53 cnf(i_0_563, hypothesis, (select(q18,tail)=index_63)). % 0.19/0.53 cnf(i_0_461, hypothesis, (select(q1,seq)=earray_68)). % 0.19/0.53 cnf(i_0_565, hypothesis, (select(q1,tail)=index_69)). % 0.19/0.53 cnf(i_0_463, hypothesis, (select(q19,seq)=earray_74)). % 0.19/0.53 cnf(i_0_567, hypothesis, (select(q19,tail)=index_75)). % 0.19/0.53 cnf(i_0_466, hypothesis, (select(q20,seq)=earray_80)). % 0.19/0.53 cnf(i_0_569, hypothesis, (select(q20,tail)=index_81)). % 0.19/0.53 cnf(i_0_468, hypothesis, (select(q21,seq)=earray_86)). % 0.19/0.53 cnf(i_0_571, hypothesis, (select(q21,tail)=index_87)). % 0.19/0.53 cnf(i_0_470, hypothesis, (select(q22,seq)=earray_92)). % 0.19/0.53 cnf(i_0_574, hypothesis, (select(q22,tail)=index_93)). % 0.19/0.53 cnf(i_0_547, hypothesis, (select(q49,head)=index_297)). % 0.19/0.53 cnf(i_0_475, hypothesis, (select(q,tail)=index_0)). % 0.19/0.53 cnf(i_0_548, hypothesis, (select(q49,tail)=index_299)). % 0.19/0.53 cnf(i_0_373, plain, (s(s(s(X1)))=X1)). % 0.19/0.53 cnf(i_0_374, hypothesis, (store(earray_8,index_9,e9)=earray_10)). % 0.19/0.53 cnf(i_0_375, hypothesis, (store(earray_98,index_99,e23)=earray_100)). % 0.19/0.53 cnf(i_0_377, hypothesis, (store(earray_104,index_105,e24)=earray_106)). % 0.19/0.53 cnf(i_0_379, hypothesis, (store(earray_110,index_111,e25)=earray_112)). % 0.19/0.53 cnf(i_0_381, hypothesis, (store(earray_116,index_117,e26)=earray_118)). % 0.19/0.53 cnf(i_0_383, hypothesis, (store(earray_122,index_123,e27)=earray_124)). % 0.19/0.53 cnf(i_0_385, hypothesis, (store(earray_128,index_129,e28)=earray_130)). % 0.19/0.53 cnf(i_0_387, hypothesis, (store(earray_134,index_135,e2)=earray_136)). % 0.19/0.53 cnf(i_0_390, hypothesis, (store(earray_140,index_141,e29)=earray_142)). % 0.19/0.53 cnf(i_0_392, hypothesis, (store(earray_146,index_147,e30)=earray_148)). % 0.19/0.53 cnf(i_0_394, hypothesis, (store(earray_152,index_153,e31)=earray_154)). % 0.19/0.53 cnf(i_0_396, hypothesis, (store(earray_14,index_15,e10)=earray_16)). % 0.19/0.53 cnf(i_0_397, hypothesis, (store(earray_158,index_159,e32)=earray_160)). % 0.19/0.53 cnf(i_0_399, hypothesis, (store(earray_164,index_165,e33)=earray_166)). % 0.19/0.53 cnf(i_0_401, hypothesis, (store(earray_170,index_171,e34)=earray_172)). % 0.19/0.53 cnf(i_0_403, hypothesis, (store(earray_176,index_177,e35)=earray_178)). % 0.19/0.53 cnf(i_0_405, hypothesis, (store(earray_182,index_183,e36)=earray_184)). % 0.19/0.53 cnf(i_0_407, hypothesis, (store(earray_188,index_189,e37)=earray_190)). % 0.19/0.53 cnf(i_0_409, hypothesis, (store(earray_194,index_195,e38)=earray_196)). % 0.19/0.53 cnf(i_0_413, hypothesis, (store(earray_200,index_201,e3)=earray_202)). % 0.19/0.53 cnf(i_0_415, hypothesis, (store(earray_206,index_207,e39)=earray_208)). % 0.19/0.53 cnf(i_0_417, hypothesis, (store(earray_212,index_213,e40)=earray_214)). % 0.19/0.53 cnf(i_0_419, hypothesis, (store(earray_20,index_21,e11)=earray_22)). % 0.19/0.53 cnf(i_0_420, hypothesis, (store(earray_218,index_219,e41)=earray_220)). % 0.19/0.53 cnf(i_0_422, hypothesis, (store(earray_224,index_225,e42)=earray_226)). % 0.19/0.53 cnf(i_0_424, hypothesis, (store(earray_230,index_231,e43)=earray_232)). % 0.19/0.53 cnf(i_0_426, hypothesis, (store(earray_236,index_237,e44)=earray_238)). % 0.19/0.53 cnf(i_0_428, hypothesis, (store(earray_242,index_243,e45)=earray_244)). % 0.19/0.53 cnf(i_0_430, hypothesis, (store(earray_248,index_249,e46)=earray_250)). % 0.19/0.53 cnf(i_0_432, hypothesis, (store(earray_254,index_255,e47)=earray_256)). % 0.19/0.53 cnf(i_0_435, hypothesis, (store(earray_260,index_261,e48)=earray_262)). % 0.19/0.53 cnf(i_0_437, hypothesis, (store(earray_266,index_267,e4)=earray_268)). % 0.19/0.53 cnf(i_0_439, hypothesis, (store(earray_272,index_273,e5)=earray_274)). % 0.19/0.53 cnf(i_0_441, hypothesis, (store(earray_26,index_27,e12)=earray_28)). % 0.19/0.53 cnf(i_0_442, hypothesis, (store(earray_278,index_279,e6)=earray_280)). % 0.19/0.53 cnf(i_0_444, hypothesis, (store(earray_284,index_285,e7)=earray_286)). % 0.19/0.53 cnf(i_0_446, hypothesis, (store(earray_290,index_291,e8)=earray_292)). % 0.19/0.53 cnf(i_0_449, hypothesis, (store(earray_32,index_33,e13)=earray_34)). % 0.19/0.53 cnf(i_0_451, hypothesis, (store(earray_2,index_3,e0)=earray_4)). % 0.19/0.53 cnf(i_0_452, hypothesis, (store(earray_38,index_39,e14)=earray_40)). % 0.19/0.53 cnf(i_0_454, hypothesis, (store(earray_44,index_45,e15)=earray_46)). % 0.19/0.53 cnf(i_0_456, hypothesis, (store(earray_50,index_51,e16)=earray_52)). % 0.19/0.53 cnf(i_0_458, hypothesis, (store(earray_56,index_57,e17)=earray_58)). % 0.19/0.53 cnf(i_0_460, hypothesis, (store(earray_62,index_63,e18)=earray_64)). % 0.19/0.53 cnf(i_0_462, hypothesis, (store(earray_68,index_69,e1)=earray_70)). % 0.19/0.53 cnf(i_0_464, hypothesis, (store(earray_74,index_75,e19)=earray_76)). % 0.19/0.53 cnf(i_0_467, hypothesis, (store(earray_80,index_81,e20)=earray_82)). % 0.19/0.53 cnf(i_0_469, hypothesis, (store(earray_86,index_87,e21)=earray_88)). % 0.19/0.53 cnf(i_0_471, hypothesis, (store(earray_92,index_93,e22)=earray_94)). % 0.19/0.53 cnf(i_0_577, hypothesis, (store(q,head,index_0)=q0)). % 0.19/0.53 cnf(i_0_578, hypothesis, (store(q23,seq,earray_100)=queue_101)). % 0.19/0.53 cnf(i_0_579, hypothesis, (store(queue_101,tail,index_102)=q24)). % 0.19/0.53 cnf(i_0_580, hypothesis, (store(q24,seq,earray_106)=queue_107)). % 0.19/0.53 cnf(i_0_581, hypothesis, (store(queue_107,tail,index_108)=q25)). % 0.19/0.53 cnf(i_0_582, hypothesis, (store(q9,seq,earray_10)=queue_11)). % 0.19/0.53 cnf(i_0_583, hypothesis, (store(q25,seq,earray_112)=queue_113)). % 0.19/0.53 cnf(i_0_584, hypothesis, (store(queue_113,tail,index_114)=q26)). % 0.19/0.53 cnf(i_0_585, hypothesis, (store(q26,seq,earray_118)=queue_119)). % 0.19/0.53 cnf(i_0_586, hypothesis, (store(queue_119,tail,index_120)=q27)). % 0.19/0.53 cnf(i_0_587, hypothesis, (store(q27,seq,earray_124)=queue_125)). % 0.19/0.53 cnf(i_0_588, hypothesis, (store(queue_125,tail,index_126)=q28)). % 0.19/0.53 cnf(i_0_589, hypothesis, (store(queue_11,tail,index_12)=q10)). % 0.19/0.53 cnf(i_0_590, hypothesis, (store(q28,seq,earray_130)=queue_131)). % 0.19/0.53 cnf(i_0_591, hypothesis, (store(queue_131,tail,index_132)=q29)). % 0.19/0.53 cnf(i_0_592, hypothesis, (store(q2,seq,earray_136)=queue_137)). % 0.19/0.53 cnf(i_0_593, hypothesis, (store(queue_137,tail,index_138)=q3)). % 0.19/0.53 cnf(i_0_594, hypothesis, (store(q29,seq,earray_142)=queue_143)). % 0.19/0.53 cnf(i_0_595, hypothesis, (store(queue_143,tail,index_144)=q30)). % 0.19/0.53 cnf(i_0_596, hypothesis, (store(q30,seq,earray_148)=queue_149)). % 0.19/0.53 cnf(i_0_597, hypothesis, (store(queue_149,tail,index_150)=q31)). % 0.19/0.53 cnf(i_0_598, hypothesis, (store(q31,seq,earray_154)=queue_155)). % 0.19/0.53 cnf(i_0_599, hypothesis, (store(queue_155,tail,index_156)=q32)). % 0.19/0.53 cnf(i_0_600, hypothesis, (store(q32,seq,earray_160)=queue_161)). % 0.19/0.53 cnf(i_0_601, hypothesis, (store(queue_161,tail,index_162)=q33)). % 0.19/0.53 cnf(i_0_602, hypothesis, (store(q33,seq,earray_166)=queue_167)). % 0.19/0.53 cnf(i_0_603, hypothesis, (store(queue_167,tail,index_168)=q34)). % 0.19/0.53 cnf(i_0_604, hypothesis, (store(q10,seq,earray_16)=queue_17)). % 0.19/0.53 cnf(i_0_605, hypothesis, (store(q34,seq,earray_172)=queue_173)). % 0.19/0.53 cnf(i_0_606, hypothesis, (store(queue_173,tail,index_174)=q35)). % 0.19/0.53 cnf(i_0_607, hypothesis, (store(q35,seq,earray_178)=queue_179)). % 0.19/0.53 cnf(i_0_608, hypothesis, (store(queue_179,tail,index_180)=q36)). % 0.19/0.53 cnf(i_0_609, hypothesis, (store(q36,seq,earray_184)=queue_185)). % 0.19/0.53 cnf(i_0_610, hypothesis, (store(queue_185,tail,index_186)=q37)). % 0.19/0.53 cnf(i_0_611, hypothesis, (store(queue_17,tail,index_18)=q11)). % 0.19/0.53 cnf(i_0_612, hypothesis, (store(q37,seq,earray_190)=queue_191)). % 0.19/0.53 cnf(i_0_613, hypothesis, (store(queue_191,tail,index_192)=q38)). % 0.19/0.53 cnf(i_0_614, hypothesis, (store(q38,seq,earray_196)=queue_197)). % 0.19/0.53 cnf(i_0_615, hypothesis, (store(queue_197,tail,index_198)=q39)). % 0.19/0.53 cnf(i_0_616, hypothesis, (store(q3,seq,earray_202)=queue_203)). % 0.19/0.53 cnf(i_0_617, hypothesis, (store(queue_203,tail,index_204)=q4)). % 0.19/0.53 cnf(i_0_618, hypothesis, (store(q39,seq,earray_208)=queue_209)). % 0.19/0.53 cnf(i_0_619, hypothesis, (store(queue_209,tail,index_210)=q40)). % 0.19/0.53 cnf(i_0_620, hypothesis, (store(q40,seq,earray_214)=queue_215)). % 0.19/0.53 cnf(i_0_621, hypothesis, (store(queue_215,tail,index_216)=q41)). % 0.19/0.53 cnf(i_0_622, hypothesis, (store(q41,seq,earray_220)=queue_221)). % 0.19/0.53 cnf(i_0_623, hypothesis, (store(queue_221,tail,index_222)=q42)). % 0.19/0.53 cnf(i_0_624, hypothesis, (store(q42,seq,earray_226)=queue_227)). % 0.19/0.53 cnf(i_0_625, hypothesis, (store(queue_227,tail,index_228)=q43)). % 0.19/0.53 cnf(i_0_626, hypothesis, (store(q11,seq,earray_22)=queue_23)). % 0.19/0.53 cnf(i_0_627, hypothesis, (store(q43,seq,earray_232)=queue_233)). % 0.19/0.53 cnf(i_0_628, hypothesis, (store(queue_233,tail,index_234)=q44)). % 0.19/0.53 cnf(i_0_629, hypothesis, (store(q44,seq,earray_238)=queue_239)). % 0.19/0.53 cnf(i_0_630, hypothesis, (store(queue_239,tail,index_240)=q45)). % 0.19/0.53 cnf(i_0_631, hypothesis, (store(q45,seq,earray_244)=queue_245)). % 0.19/0.53 cnf(i_0_632, hypothesis, (store(queue_245,tail,index_246)=q46)). % 0.19/0.53 cnf(i_0_633, hypothesis, (store(queue_23,tail,index_24)=q12)). % 0.19/0.53 cnf(i_0_634, hypothesis, (store(q46,seq,earray_250)=queue_251)). % 0.19/0.53 cnf(i_0_635, hypothesis, (store(queue_251,tail,index_252)=q47)). % 0.19/0.53 cnf(i_0_636, hypothesis, (store(q47,seq,earray_256)=queue_257)). % 0.19/0.53 cnf(i_0_637, hypothesis, (store(queue_257,tail,index_258)=q48)). % 0.19/0.53 cnf(i_0_638, hypothesis, (store(q48,seq,earray_262)=queue_263)). % 0.19/0.53 cnf(i_0_639, hypothesis, (store(queue_263,tail,index_264)=q49)). % 0.19/0.53 cnf(i_0_640, hypothesis, (store(q4,seq,earray_268)=queue_269)). % 0.19/0.53 cnf(i_0_641, hypothesis, (store(queue_269,tail,index_270)=q5)). % 0.19/0.53 cnf(i_0_642, hypothesis, (store(q5,seq,earray_274)=queue_275)). % 0.19/0.53 cnf(i_0_643, hypothesis, (store(queue_275,tail,index_276)=q6)). % 0.19/0.53 cnf(i_0_644, hypothesis, (store(q6,seq,earray_280)=queue_281)). % 0.19/0.53 cnf(i_0_645, hypothesis, (store(queue_281,tail,index_282)=q7)). % 0.19/0.53 cnf(i_0_646, hypothesis, (store(q7,seq,earray_286)=queue_287)). % 0.19/0.53 cnf(i_0_647, hypothesis, (store(queue_287,tail,index_288)=q8)). % 0.19/0.53 cnf(i_0_648, hypothesis, (store(q12,seq,earray_28)=queue_29)). % 0.19/0.53 cnf(i_0_649, hypothesis, (store(q8,seq,earray_292)=queue_293)). % 0.19/0.53 cnf(i_0_650, hypothesis, (store(queue_293,tail,index_294)=q9)). % 0.19/0.53 cnf(i_0_651, hypothesis, (store(queue_29,tail,index_30)=q13)). % 0.19/0.53 cnf(i_0_652, hypothesis, (store(q13,seq,earray_34)=queue_35)). % 0.19/0.53 cnf(i_0_653, hypothesis, (store(queue_35,tail,index_36)=q14)). % 0.19/0.53 cnf(i_0_654, hypothesis, (store(q14,seq,earray_40)=queue_41)). % 0.19/0.53 cnf(i_0_655, hypothesis, (store(queue_41,tail,index_42)=q15)). % 0.19/0.53 cnf(i_0_656, hypothesis, (store(q15,seq,earray_46)=queue_47)). % 0.19/0.53 cnf(i_0_657, hypothesis, (store(queue_47,tail,index_48)=q16)). % 0.19/0.53 cnf(i_0_658, hypothesis, (store(q0,seq,earray_4)=queue_5)). % 0.19/0.53 cnf(i_0_659, hypothesis, (store(q16,seq,earray_52)=queue_53)). % 0.19/0.53 cnf(i_0_660, hypothesis, (store(queue_53,tail,index_54)=q17)). % 0.19/0.53 cnf(i_0_661, hypothesis, (store(q17,seq,earray_58)=queue_59)). % 0.19/0.53 cnf(i_0_662, hypothesis, (store(queue_59,tail,index_60)=q18)). % 0.19/0.53 cnf(i_0_663, hypothesis, (store(q18,seq,earray_64)=queue_65)). % 0.19/0.53 cnf(i_0_664, hypothesis, (store(queue_65,tail,index_66)=q19)). % 0.19/0.53 cnf(i_0_665, hypothesis, (store(queue_5,tail,index_6)=q1)). % 0.19/0.53 cnf(i_0_666, hypothesis, (store(q1,seq,earray_70)=queue_71)). % 0.19/0.53 cnf(i_0_667, hypothesis, (store(queue_71,tail,index_72)=q2)). % 0.19/0.53 cnf(i_0_668, hypothesis, (store(q19,seq,earray_76)=queue_77)). % 0.19/0.53 cnf(i_0_669, hypothesis, (store(queue_77,tail,index_78)=q20)). % 0.19/0.53 cnf(i_0_670, hypothesis, (store(q20,seq,earray_82)=queue_83)). % 0.19/0.53 cnf(i_0_671, hypothesis, (store(queue_83,tail,index_84)=q21)). % 0.19/0.53 cnf(i_0_672, hypothesis, (store(q21,seq,earray_88)=queue_89)). % 0.19/0.53 cnf(i_0_673, hypothesis, (store(queue_89,tail,index_90)=q22)). % 0.19/0.53 cnf(i_0_674, hypothesis, (store(q22,seq,earray_94)=queue_95)). % 0.19/0.53 cnf(i_0_675, hypothesis, (store(queue_95,tail,index_96)=q23)). % 0.19/0.53 cnf(i_0_364, plain, (select(store(X1,X2,X3),X2)=X3)). % 0.19/0.53 cnf(i_0_726, negated_conjecture, (elem_301!=elem_298)). % 0.19/0.53 cnf(i_0_366, plain, (head!=tail)). % 0.19/0.53 cnf(i_0_367, plain, (head!=seq)). % 0.19/0.53 cnf(i_0_368, plain, (seq!=tail)). % 0.19/0.53 cnf(i_0_372, plain, (s(X1)!=X1)). % 0.19/0.53 cnf(i_0_371, plain, (s(s(X1))!=X1)). % 0.19/0.53 cnf(i_0_365, plain, (select(store(X1,X2,X3),X4)=select(X1,X4)|X2=X4)). % 0.19/0.53 cnf(i_0_732, plain, (X5=X5)). % 0.19/0.53 # End listing active clauses. There is an equivalent clause to each of these in the clausification! % 0.19/0.53 # Begin printing tableau % 0.19/0.53 # Found 7 steps % 0.19/0.53 cnf(i_0_676, hypothesis, (queue_1=q0), inference(start_rule)). % 0.19/0.53 cnf(i_0_740, plain, (queue_1=q0), inference(extension_rule, [i_0_736])). % 0.19/0.53 cnf(i_0_1116, plain, (queue_1!=q0), inference(closure_rule, [i_0_676])). % 0.19/0.53 cnf(i_0_1117, plain, (queue_1!=q0), inference(closure_rule, [i_0_676])). % 0.19/0.53 cnf(i_0_1114, plain, (store(queue_1,queue_1,queue_1)=store(q0,q0,q0)), inference(extension_rule, [i_0_735])). % 0.19/0.53 cnf(i_0_1131, plain, (store(queue_1,queue_1,queue_1)=s(store(queue_1,queue_1,queue_1))), inference(closure_rule, [i_0_372])). % 0.19/0.53 cnf(i_0_1133, plain, (store(q0,q0,q0)!=s(store(queue_1,queue_1,queue_1))), inference(etableau_closure_rule, [i_0_1133, ...])). % 0.19/0.53 # End printing tableau % 0.19/0.53 # SZS output end % 0.19/0.53 # Branches closed with saturation will be marked with an "s" % 0.19/0.54 # Child (10939) has found a proof. % 0.19/0.54 % 0.74/0.55 # Proof search is over... % 0.74/0.55 # Freeing feature tree %------------------------------------------------------------------------------