%------------------------------------------------------------------------------ % File : Etableau---0.67 % Problem : SWV569-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 : n019.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:41 EDT 2022 % Result : Unsatisfiable 1.38s 0.64s % Output : CNFRefutation 1.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.12 % Problem : SWV569-1.030 : TPTP v8.1.0. Released v4.0.0. % 0.09/0.12 % Command : etableau --auto --tsmdo --quicksat=10000 --tableau=1 --tableau-saturation=1 -s -p --tableau-cores=8 --cpu-limit=%d %s % 0.13/0.33 % Computer : n019.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Thu Jun 16 01:03:24 EDT 2022 % 0.13/0.33 % CPUTime : % 0.13/0.38 # No SInE strategy applied % 0.13/0.38 # Auto-Mode selected heuristic G_E___208_C18_F1_SE_CS_SP_PS_S5PRR_RG_S04AN % 0.13/0.38 # and selection function SelectComplexExceptUniqMaxHorn. % 0.13/0.38 # % 0.13/0.38 # Presaturation interreduction done % 0.13/0.38 # Number of axioms: 302 Number of unprocessed: 302 % 0.13/0.38 # Tableaux proof search. % 0.13/0.38 # APR header successfully linked. % 0.13/0.38 # Hello from C++ % 0.20/0.50 # The folding up rule is enabled... % 0.20/0.50 # Local unification is enabled... % 0.20/0.50 # Any saturation attempts will use folding labels... % 0.20/0.50 # 302 beginning clauses after preprocessing and clausification % 0.20/0.50 # Creating start rules for all 1 conjectures. % 0.20/0.50 # There are 1 start rule candidates: % 0.20/0.50 # Found 301 unit axioms. % 0.20/0.50 # 1 start rule tableaux created. % 0.20/0.50 # 1 extension rule candidate clauses % 0.20/0.50 # 301 unit axiom clauses % 0.20/0.50 % 0.20/0.50 # Requested 8, 32 cores available to the main process. % 0.20/0.50 # There are not enough tableaux to fork, creating more from the initial 1 % 0.20/0.50 # Creating equality axioms % 0.20/0.50 # Ran out of tableaux, making start rules for all clauses % 0.20/0.50 # Returning from population with 310 new_tableaux and 0 remaining starting tableaux. % 0.20/0.50 # We now have 310 tableaux to operate on % 1.38/0.64 # There were 1 total branch saturation attempts. % 1.38/0.64 # There were 0 of these attempts blocked. % 1.38/0.64 # There were 0 deferred branch saturation attempts. % 1.38/0.64 # There were 0 free duplicated saturations. % 1.38/0.64 # There were 1 total successful branch saturations. % 1.38/0.64 # There were 0 successful branch saturations in interreduction. % 1.38/0.64 # There were 0 successful branch saturations on the branch. % 1.38/0.64 # There were 1 successful branch saturations after the branch. % 1.38/0.64 # SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 1.38/0.64 # SZS output start for /export/starexec/sandbox/benchmark/theBenchmark.p % 1.38/0.64 # Begin clausification derivation % 1.38/0.64 % 1.38/0.64 # End clausification derivation % 1.38/0.64 # Begin listing active clauses obtained from FOF to CNF conversion % 1.38/0.64 cnf(i_0_573, hypothesis, (queue_1=q0)). % 1.38/0.64 cnf(i_0_588, hypothesis, (queue_103=q22)). % 1.38/0.64 cnf(i_0_589, hypothesis, (queue_109=q23)). % 1.38/0.64 cnf(i_0_590, hypothesis, (queue_118=q24)). % 1.38/0.64 cnf(i_0_591, hypothesis, (queue_124=q25)). % 1.38/0.64 cnf(i_0_575, hypothesis, (queue_13=q10)). % 1.38/0.64 cnf(i_0_592, hypothesis, (queue_130=q26)). % 1.38/0.64 cnf(i_0_593, hypothesis, (queue_139=q27)). % 1.38/0.64 cnf(i_0_594, hypothesis, (queue_145=q28)). % 1.38/0.64 cnf(i_0_595, hypothesis, (queue_151=q29)). % 1.38/0.64 cnf(i_0_596, hypothesis, (queue_160=q3)). % 1.38/0.64 cnf(i_0_597, hypothesis, (queue_169=q30)). % 1.38/0.64 cnf(i_0_598, hypothesis, (queue_175=q4)). % 1.38/0.64 cnf(i_0_599, hypothesis, (queue_181=q5)). % 1.38/0.64 cnf(i_0_576, hypothesis, (queue_19=q11)). % 1.38/0.64 cnf(i_0_600, hypothesis, (queue_190=q6)). % 1.38/0.64 cnf(i_0_601, hypothesis, (queue_196=q7)). % 1.38/0.64 cnf(i_0_602, hypothesis, (queue_202=q8)). % 1.38/0.64 cnf(i_0_603, hypothesis, (queue_211=q9)). % 1.38/0.64 cnf(i_0_577, hypothesis, (queue_28=q12)). % 1.38/0.64 cnf(i_0_578, hypothesis, (queue_34=q13)). % 1.38/0.64 cnf(i_0_579, hypothesis, (queue_40=q14)). % 1.38/0.64 cnf(i_0_580, hypothesis, (queue_49=q15)). % 1.38/0.64 cnf(i_0_581, hypothesis, (queue_55=q16)). % 1.38/0.64 cnf(i_0_582, hypothesis, (queue_61=q17)). % 1.38/0.64 cnf(i_0_574, hypothesis, (queue_7=q1)). % 1.38/0.64 cnf(i_0_583, hypothesis, (queue_70=q18)). % 1.38/0.64 cnf(i_0_584, hypothesis, (queue_76=q19)). % 1.38/0.64 cnf(i_0_585, hypothesis, (queue_82=q2)). % 1.38/0.64 cnf(i_0_586, hypothesis, (queue_88=q20)). % 1.38/0.64 cnf(i_0_587, hypothesis, (queue_97=q21)). % 1.38/0.64 cnf(i_0_421, hypothesis, (s(index_99)=index_102)). % 1.38/0.64 cnf(i_0_423, hypothesis, (s(index_105)=index_108)). % 1.38/0.64 cnf(i_0_425, hypothesis, (s(index_111)=index_114)). % 1.38/0.64 cnf(i_0_427, hypothesis, (s(index_116)=index_117)). % 1.38/0.64 cnf(i_0_428, hypothesis, (s(index_9)=index_12)). % 1.38/0.64 cnf(i_0_430, hypothesis, (s(index_120)=index_123)). % 1.38/0.64 cnf(i_0_432, hypothesis, (s(index_126)=index_129)). % 1.38/0.64 cnf(i_0_434, hypothesis, (s(index_132)=index_135)). % 1.38/0.64 cnf(i_0_436, hypothesis, (s(index_137)=index_138)). % 1.38/0.64 cnf(i_0_438, hypothesis, (s(index_141)=index_144)). % 1.38/0.64 cnf(i_0_441, hypothesis, (s(index_147)=index_150)). % 1.38/0.64 cnf(i_0_443, hypothesis, (s(index_153)=index_156)). % 1.38/0.64 cnf(i_0_445, hypothesis, (s(index_158)=index_159)). % 1.38/0.64 cnf(i_0_447, hypothesis, (s(index_162)=index_165)). % 1.38/0.64 cnf(i_0_449, hypothesis, (s(index_167)=index_168)). % 1.38/0.64 cnf(i_0_451, hypothesis, (s(index_171)=index_174)). % 1.38/0.64 cnf(i_0_453, hypothesis, (s(index_15)=index_18)). % 1.38/0.64 cnf(i_0_454, hypothesis, (s(index_177)=index_180)). % 1.38/0.64 cnf(i_0_456, hypothesis, (s(index_183)=index_186)). % 1.38/0.64 cnf(i_0_458, hypothesis, (s(index_188)=index_189)). % 1.38/0.64 cnf(i_0_460, hypothesis, (s(index_192)=index_195)). % 1.38/0.64 cnf(i_0_462, hypothesis, (s(index_198)=index_201)). % 1.38/0.64 cnf(i_0_464, hypothesis, (s(index_204)=index_207)). % 1.38/0.64 cnf(i_0_467, hypothesis, (s(index_209)=index_210)). % 1.38/0.64 cnf(i_0_469, hypothesis, (s(index_21)=index_24)). % 1.38/0.64 cnf(i_0_471, hypothesis, (s(index_26)=index_27)). % 1.38/0.64 cnf(i_0_474, hypothesis, (s(index_30)=index_33)). % 1.38/0.64 cnf(i_0_476, hypothesis, (s(index_36)=index_39)). % 1.38/0.64 cnf(i_0_478, hypothesis, (s(index_42)=index_45)). % 1.38/0.64 cnf(i_0_480, hypothesis, (s(index_47)=index_48)). % 1.38/0.64 cnf(i_0_482, hypothesis, (s(index_51)=index_54)). % 1.38/0.64 cnf(i_0_484, hypothesis, (s(index_3)=index_6)). % 1.38/0.64 cnf(i_0_485, hypothesis, (s(index_57)=index_60)). % 1.38/0.64 cnf(i_0_487, hypothesis, (s(index_63)=index_66)). % 1.38/0.64 cnf(i_0_489, hypothesis, (s(index_68)=index_69)). % 1.38/0.64 cnf(i_0_491, hypothesis, (s(index_72)=index_75)). % 1.38/0.64 cnf(i_0_493, hypothesis, (s(index_78)=index_81)). % 1.38/0.64 cnf(i_0_495, hypothesis, (s(index_84)=index_87)). % 1.38/0.64 cnf(i_0_498, hypothesis, (s(index_90)=index_93)). % 1.38/0.64 cnf(i_0_500, hypothesis, (s(index_95)=index_96)). % 1.38/0.64 cnf(i_0_419, hypothesis, (select(earray_212,index_213)=elem_214)). % 1.38/0.64 cnf(i_0_413, hypothesis, (select(q9,seq)=earray_8)). % 1.38/0.64 cnf(i_0_496, hypothesis, (select(q9,tail)=index_9)). % 1.38/0.64 cnf(i_0_418, hypothesis, (select(q21,seq)=earray_98)). % 1.38/0.64 cnf(i_0_501, hypothesis, (select(q21,tail)=index_99)). % 1.38/0.64 cnf(i_0_360, hypothesis, (select(q22,seq)=earray_104)). % 1.38/0.64 cnf(i_0_422, hypothesis, (select(q22,tail)=index_105)). % 1.38/0.64 cnf(i_0_362, hypothesis, (select(q23,seq)=earray_110)). % 1.38/0.64 cnf(i_0_424, hypothesis, (select(q23,tail)=index_111)). % 1.38/0.64 cnf(i_0_364, hypothesis, (select(q24,seq)=earray_119)). % 1.38/0.64 cnf(i_0_429, hypothesis, (select(q24,tail)=index_120)). % 1.38/0.64 cnf(i_0_366, hypothesis, (select(q25,seq)=earray_125)). % 1.38/0.64 cnf(i_0_431, hypothesis, (select(q25,tail)=index_126)). % 1.38/0.64 cnf(i_0_368, hypothesis, (select(q26,seq)=earray_131)). % 1.38/0.64 cnf(i_0_433, hypothesis, (select(q26,tail)=index_132)). % 1.38/0.64 cnf(i_0_370, hypothesis, (select(q10,seq)=earray_14)). % 1.38/0.64 cnf(i_0_371, hypothesis, (select(q27,seq)=earray_140)). % 1.38/0.64 cnf(i_0_437, hypothesis, (select(q27,tail)=index_141)). % 1.38/0.64 cnf(i_0_373, hypothesis, (select(q28,seq)=earray_146)). % 1.38/0.64 cnf(i_0_439, hypothesis, (select(q28,tail)=index_147)). % 1.38/0.64 cnf(i_0_375, hypothesis, (select(q2,seq)=earray_152)). % 1.38/0.64 cnf(i_0_442, hypothesis, (select(q2,tail)=index_153)). % 1.38/0.64 cnf(i_0_440, hypothesis, (select(q10,tail)=index_15)). % 1.38/0.64 cnf(i_0_378, hypothesis, (select(q29,seq)=earray_161)). % 1.38/0.64 cnf(i_0_446, hypothesis, (select(q29,tail)=index_162)). % 1.38/0.64 cnf(i_0_380, hypothesis, (select(q3,seq)=earray_170)). % 1.38/0.64 cnf(i_0_450, hypothesis, (select(q3,tail)=index_171)). % 1.38/0.64 cnf(i_0_382, hypothesis, (select(q4,seq)=earray_176)). % 1.38/0.64 cnf(i_0_452, hypothesis, (select(q4,tail)=index_177)). % 1.38/0.64 cnf(i_0_384, hypothesis, (select(q5,seq)=earray_182)). % 1.38/0.64 cnf(i_0_455, hypothesis, (select(q5,tail)=index_183)). % 1.38/0.64 cnf(i_0_386, hypothesis, (select(q6,seq)=earray_191)). % 1.38/0.64 cnf(i_0_459, hypothesis, (select(q6,tail)=index_192)). % 1.38/0.64 cnf(i_0_388, hypothesis, (select(q7,seq)=earray_197)). % 1.38/0.64 cnf(i_0_461, hypothesis, (select(q7,tail)=index_198)). % 1.38/0.64 cnf(i_0_390, hypothesis, (select(q0,seq)=earray_2)). % 1.38/0.64 cnf(i_0_391, hypothesis, (select(q11,seq)=earray_20)). % 1.38/0.64 cnf(i_0_392, hypothesis, (select(q8,seq)=earray_203)). % 1.38/0.64 cnf(i_0_463, hypothesis, (select(q8,tail)=index_204)). % 1.38/0.64 cnf(i_0_394, hypothesis, (select(q30,seq)=earray_212)). % 1.38/0.64 cnf(i_0_466, hypothesis, (select(q11,tail)=index_21)). % 1.38/0.64 cnf(i_0_396, hypothesis, (select(q12,seq)=earray_29)). % 1.38/0.64 cnf(i_0_473, hypothesis, (select(q12,tail)=index_30)). % 1.38/0.64 cnf(i_0_398, hypothesis, (select(q13,seq)=earray_35)). % 1.38/0.64 cnf(i_0_475, hypothesis, (select(q13,tail)=index_36)). % 1.38/0.64 cnf(i_0_472, hypothesis, (select(q0,tail)=index_3)). % 1.38/0.64 cnf(i_0_401, hypothesis, (select(q14,seq)=earray_41)). % 1.38/0.64 cnf(i_0_477, hypothesis, (select(q14,tail)=index_42)). % 1.38/0.64 cnf(i_0_403, hypothesis, (select(q15,seq)=earray_50)). % 1.38/0.64 cnf(i_0_481, hypothesis, (select(q15,tail)=index_51)). % 1.38/0.64 cnf(i_0_405, hypothesis, (select(q16,seq)=earray_56)). % 1.38/0.64 cnf(i_0_483, hypothesis, (select(q16,tail)=index_57)). % 1.38/0.64 cnf(i_0_407, hypothesis, (select(q17,seq)=earray_62)). % 1.38/0.64 cnf(i_0_486, hypothesis, (select(q17,tail)=index_63)). % 1.38/0.64 cnf(i_0_409, hypothesis, (select(q18,seq)=earray_71)). % 1.38/0.64 cnf(i_0_490, hypothesis, (select(q18,tail)=index_72)). % 1.38/0.64 cnf(i_0_411, hypothesis, (select(q1,seq)=earray_77)). % 1.38/0.64 cnf(i_0_492, hypothesis, (select(q1,tail)=index_78)). % 1.38/0.64 cnf(i_0_414, hypothesis, (select(q19,seq)=earray_83)). % 1.38/0.64 cnf(i_0_494, hypothesis, (select(q19,tail)=index_84)). % 1.38/0.64 cnf(i_0_416, hypothesis, (select(q20,seq)=earray_89)). % 1.38/0.64 cnf(i_0_497, hypothesis, (select(q20,tail)=index_90)). % 1.38/0.64 cnf(i_0_468, hypothesis, (select(q30,head)=index_213)). % 1.38/0.64 cnf(i_0_420, hypothesis, (select(q,tail)=index_0)). % 1.38/0.64 cnf(i_0_426, hypothesis, (select(queue_115,head)=index_116)). % 1.38/0.64 cnf(i_0_435, hypothesis, (select(queue_136,head)=index_137)). % 1.38/0.64 cnf(i_0_444, hypothesis, (select(queue_157,head)=index_158)). % 1.38/0.64 cnf(i_0_448, hypothesis, (select(queue_166,head)=index_167)). % 1.38/0.64 cnf(i_0_457, hypothesis, (select(queue_187,head)=index_188)). % 1.38/0.64 cnf(i_0_465, hypothesis, (select(queue_208,head)=index_209)). % 1.38/0.64 cnf(i_0_470, hypothesis, (select(queue_25,head)=index_26)). % 1.38/0.64 cnf(i_0_479, hypothesis, (select(queue_46,head)=index_47)). % 1.38/0.64 cnf(i_0_488, hypothesis, (select(queue_67,head)=index_68)). % 1.38/0.64 cnf(i_0_499, hypothesis, (select(queue_94,head)=index_95)). % 1.38/0.64 cnf(i_0_377, hypothesis, (store(earray_14,index_15,e10)=earray_16)). % 1.38/0.64 cnf(i_0_358, hypothesis, (store(earray_8,index_9,e9)=earray_10)). % 1.38/0.64 cnf(i_0_359, hypothesis, (store(earray_98,index_99,e21)=earray_100)). % 1.38/0.64 cnf(i_0_361, hypothesis, (store(earray_104,index_105,e22)=earray_106)). % 1.38/0.64 cnf(i_0_363, hypothesis, (store(earray_110,index_111,e23)=earray_112)). % 1.38/0.64 cnf(i_0_365, hypothesis, (store(earray_119,index_120,e24)=earray_121)). % 1.38/0.64 cnf(i_0_367, hypothesis, (store(earray_125,index_126,e25)=earray_127)). % 1.38/0.64 cnf(i_0_369, hypothesis, (store(earray_131,index_132,e26)=earray_133)). % 1.38/0.64 cnf(i_0_372, hypothesis, (store(earray_140,index_141,e27)=earray_142)). % 1.38/0.64 cnf(i_0_374, hypothesis, (store(earray_146,index_147,e28)=earray_148)). % 1.38/0.64 cnf(i_0_376, hypothesis, (store(earray_152,index_153,e2)=earray_154)). % 1.38/0.64 cnf(i_0_379, hypothesis, (store(earray_161,index_162,e29)=earray_163)). % 1.38/0.64 cnf(i_0_381, hypothesis, (store(earray_170,index_171,e3)=earray_172)). % 1.38/0.64 cnf(i_0_383, hypothesis, (store(earray_176,index_177,e4)=earray_178)). % 1.38/0.64 cnf(i_0_385, hypothesis, (store(earray_182,index_183,e5)=earray_184)). % 1.38/0.64 cnf(i_0_387, hypothesis, (store(earray_191,index_192,e6)=earray_193)). % 1.38/0.64 cnf(i_0_389, hypothesis, (store(earray_197,index_198,e7)=earray_199)). % 1.38/0.64 cnf(i_0_393, hypothesis, (store(earray_203,index_204,e8)=earray_205)). % 1.38/0.64 cnf(i_0_395, hypothesis, (store(earray_20,index_21,e11)=earray_22)). % 1.38/0.64 cnf(i_0_397, hypothesis, (store(earray_29,index_30,e12)=earray_31)). % 1.38/0.64 cnf(i_0_399, hypothesis, (store(earray_35,index_36,e13)=earray_37)). % 1.38/0.64 cnf(i_0_400, hypothesis, (store(earray_2,index_3,e0)=earray_4)). % 1.38/0.64 cnf(i_0_402, hypothesis, (store(earray_41,index_42,e14)=earray_43)). % 1.38/0.64 cnf(i_0_404, hypothesis, (store(earray_50,index_51,e15)=earray_52)). % 1.38/0.64 cnf(i_0_406, hypothesis, (store(earray_56,index_57,e16)=earray_58)). % 1.38/0.64 cnf(i_0_408, hypothesis, (store(earray_62,index_63,e17)=earray_64)). % 1.38/0.64 cnf(i_0_410, hypothesis, (store(earray_71,index_72,e18)=earray_73)). % 1.38/0.64 cnf(i_0_412, hypothesis, (store(earray_77,index_78,e1)=earray_79)). % 1.38/0.64 cnf(i_0_415, hypothesis, (store(earray_83,index_84,e19)=earray_85)). % 1.38/0.64 cnf(i_0_417, hypothesis, (store(earray_89,index_90,e20)=earray_91)). % 1.38/0.64 cnf(i_0_509, hypothesis, (store(queue_113,tail,index_114)=queue_115)). % 1.38/0.64 cnf(i_0_517, hypothesis, (store(queue_134,tail,index_135)=queue_136)). % 1.38/0.64 cnf(i_0_524, hypothesis, (store(queue_155,tail,index_156)=queue_157)). % 1.38/0.64 cnf(i_0_527, hypothesis, (store(queue_164,tail,index_165)=queue_166)). % 1.38/0.64 cnf(i_0_535, hypothesis, (store(queue_185,tail,index_186)=queue_187)). % 1.38/0.64 cnf(i_0_543, hypothesis, (store(queue_206,tail,index_207)=queue_208)). % 1.38/0.64 cnf(i_0_546, hypothesis, (store(queue_23,tail,index_24)=queue_25)). % 1.38/0.64 cnf(i_0_553, hypothesis, (store(queue_44,tail,index_45)=queue_46)). % 1.38/0.64 cnf(i_0_561, hypothesis, (store(queue_65,tail,index_66)=queue_67)). % 1.38/0.64 cnf(i_0_571, hypothesis, (store(queue_92,tail,index_93)=queue_94)). % 1.38/0.64 cnf(i_0_502, hypothesis, (store(q,head,index_0)=q0)). % 1.38/0.64 cnf(i_0_503, hypothesis, (store(q21,seq,earray_100)=queue_101)). % 1.38/0.64 cnf(i_0_504, hypothesis, (store(queue_101,tail,index_102)=q22)). % 1.38/0.64 cnf(i_0_505, hypothesis, (store(q22,seq,earray_106)=queue_107)). % 1.38/0.64 cnf(i_0_506, hypothesis, (store(queue_107,tail,index_108)=q23)). % 1.38/0.64 cnf(i_0_507, hypothesis, (store(q9,seq,earray_10)=queue_11)). % 1.38/0.64 cnf(i_0_508, hypothesis, (store(q23,seq,earray_112)=queue_113)). % 1.38/0.64 cnf(i_0_510, hypothesis, (store(queue_115,head,index_117)=q24)). % 1.38/0.64 cnf(i_0_511, hypothesis, (store(q24,seq,earray_121)=queue_122)). % 1.38/0.64 cnf(i_0_512, hypothesis, (store(queue_122,tail,index_123)=q25)). % 1.38/0.64 cnf(i_0_513, hypothesis, (store(q25,seq,earray_127)=queue_128)). % 1.38/0.64 cnf(i_0_514, hypothesis, (store(queue_11,tail,index_12)=q10)). % 1.38/0.64 cnf(i_0_515, hypothesis, (store(queue_128,tail,index_129)=q26)). % 1.38/0.64 cnf(i_0_516, hypothesis, (store(q26,seq,earray_133)=queue_134)). % 1.38/0.64 cnf(i_0_518, hypothesis, (store(queue_136,head,index_138)=q27)). % 1.38/0.64 cnf(i_0_519, hypothesis, (store(q27,seq,earray_142)=queue_143)). % 1.38/0.64 cnf(i_0_520, hypothesis, (store(queue_143,tail,index_144)=q28)). % 1.38/0.64 cnf(i_0_521, hypothesis, (store(q28,seq,earray_148)=queue_149)). % 1.38/0.64 cnf(i_0_522, hypothesis, (store(queue_149,tail,index_150)=q29)). % 1.38/0.64 cnf(i_0_523, hypothesis, (store(q2,seq,earray_154)=queue_155)). % 1.38/0.64 cnf(i_0_525, hypothesis, (store(queue_157,head,index_159)=q3)). % 1.38/0.64 cnf(i_0_526, hypothesis, (store(q29,seq,earray_163)=queue_164)). % 1.38/0.64 cnf(i_0_528, hypothesis, (store(queue_166,head,index_168)=q30)). % 1.38/0.64 cnf(i_0_529, hypothesis, (store(q10,seq,earray_16)=queue_17)). % 1.38/0.64 cnf(i_0_530, hypothesis, (store(q3,seq,earray_172)=queue_173)). % 1.38/0.64 cnf(i_0_531, hypothesis, (store(queue_173,tail,index_174)=q4)). % 1.38/0.64 cnf(i_0_532, hypothesis, (store(q4,seq,earray_178)=queue_179)). % 1.38/0.64 cnf(i_0_533, hypothesis, (store(queue_179,tail,index_180)=q5)). % 1.38/0.64 cnf(i_0_534, hypothesis, (store(q5,seq,earray_184)=queue_185)). % 1.38/0.64 cnf(i_0_536, hypothesis, (store(queue_17,tail,index_18)=q11)). % 1.38/0.64 cnf(i_0_537, hypothesis, (store(queue_187,head,index_189)=q6)). % 1.38/0.64 cnf(i_0_538, hypothesis, (store(q6,seq,earray_193)=queue_194)). % 1.38/0.64 cnf(i_0_539, hypothesis, (store(queue_194,tail,index_195)=q7)). % 1.38/0.64 cnf(i_0_540, hypothesis, (store(q7,seq,earray_199)=queue_200)). % 1.38/0.64 cnf(i_0_541, hypothesis, (store(queue_200,tail,index_201)=q8)). % 1.38/0.64 cnf(i_0_542, hypothesis, (store(q8,seq,earray_205)=queue_206)). % 1.38/0.64 cnf(i_0_544, hypothesis, (store(queue_208,head,index_210)=q9)). % 1.38/0.64 cnf(i_0_545, hypothesis, (store(q11,seq,earray_22)=queue_23)). % 1.38/0.64 cnf(i_0_547, hypothesis, (store(queue_25,head,index_27)=q12)). % 1.38/0.64 cnf(i_0_548, hypothesis, (store(q12,seq,earray_31)=queue_32)). % 1.38/0.64 cnf(i_0_549, hypothesis, (store(queue_32,tail,index_33)=q13)). % 1.38/0.64 cnf(i_0_550, hypothesis, (store(q13,seq,earray_37)=queue_38)). % 1.38/0.64 cnf(i_0_551, hypothesis, (store(queue_38,tail,index_39)=q14)). % 1.38/0.64 cnf(i_0_552, hypothesis, (store(q14,seq,earray_43)=queue_44)). % 1.38/0.64 cnf(i_0_554, hypothesis, (store(queue_46,head,index_48)=q15)). % 1.38/0.64 cnf(i_0_555, hypothesis, (store(q0,seq,earray_4)=queue_5)). % 1.38/0.64 cnf(i_0_556, hypothesis, (store(q15,seq,earray_52)=queue_53)). % 1.38/0.64 cnf(i_0_557, hypothesis, (store(queue_53,tail,index_54)=q16)). % 1.38/0.64 cnf(i_0_558, hypothesis, (store(q16,seq,earray_58)=queue_59)). % 1.38/0.64 cnf(i_0_559, hypothesis, (store(queue_59,tail,index_60)=q17)). % 1.38/0.64 cnf(i_0_560, hypothesis, (store(q17,seq,earray_64)=queue_65)). % 1.38/0.64 cnf(i_0_562, hypothesis, (store(queue_5,tail,index_6)=q1)). % 1.38/0.64 cnf(i_0_563, hypothesis, (store(queue_67,head,index_69)=q18)). % 1.38/0.64 cnf(i_0_564, hypothesis, (store(q18,seq,earray_73)=queue_74)). % 1.38/0.64 cnf(i_0_565, hypothesis, (store(queue_74,tail,index_75)=q19)). % 1.38/0.64 cnf(i_0_566, hypothesis, (store(q1,seq,earray_79)=queue_80)). % 1.38/0.64 cnf(i_0_567, hypothesis, (store(queue_80,tail,index_81)=q2)). % 1.38/0.64 cnf(i_0_568, hypothesis, (store(q19,seq,earray_85)=queue_86)). % 1.38/0.64 cnf(i_0_569, hypothesis, (store(queue_86,tail,index_87)=q20)). % 1.38/0.64 cnf(i_0_570, hypothesis, (store(q20,seq,earray_91)=queue_92)). % 1.38/0.64 cnf(i_0_572, hypothesis, (store(queue_94,head,index_96)=q21)). % 1.38/0.64 cnf(i_0_303, plain, (select(store(X1,X2,X3),X2)=X3)). % 1.38/0.64 cnf(i_0_604, negated_conjecture, (e10!=elem_214)). % 1.38/0.64 cnf(i_0_305, plain, (head!=tail)). % 1.38/0.64 cnf(i_0_306, plain, (head!=seq)). % 1.38/0.64 cnf(i_0_307, plain, (tail!=seq)). % 1.38/0.64 cnf(i_0_357, plain, (s(X1)!=X1)). % 1.38/0.64 cnf(i_0_356, plain, (s(s(X1))!=X1)). % 1.38/0.64 cnf(i_0_355, plain, (s(s(s(X1)))!=X1)). % 1.38/0.64 cnf(i_0_354, plain, (s(s(s(s(X1))))!=X1)). % 1.38/0.64 cnf(i_0_353, plain, (s(s(s(s(s(X1)))))!=X1)). % 1.38/0.64 cnf(i_0_352, plain, (s(s(s(s(s(s(X1))))))!=X1)). % 1.38/0.64 cnf(i_0_351, plain, (s(s(s(s(s(s(s(X1)))))))!=X1)). % 1.38/0.64 cnf(i_0_350, plain, (s(s(s(s(s(s(s(s(X1))))))))!=X1)). % 1.38/0.64 cnf(i_0_349, plain, (s(s(s(s(s(s(s(s(s(X1)))))))))!=X1)). % 1.38/0.64 cnf(i_0_348, plain, (s(s(s(s(s(s(s(s(s(s(X1))))))))))!=X1)). % 1.38/0.64 cnf(i_0_347, plain, (s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))!=X1)). % 1.38/0.64 cnf(i_0_346, plain, (s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_345, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_344, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_343, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_342, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_341, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_340, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_339, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_338, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_337, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_336, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_335, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_334, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_333, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_332, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_331, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_330, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_329, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_328, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_327, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_326, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_325, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_324, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_323, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_322, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_321, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_320, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_319, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_318, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_317, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))))))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_316, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))))))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_315, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))))))))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_314, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_313, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_312, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_311, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_310, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_309, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_308, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 1.38/0.64 cnf(i_0_304, plain, (select(store(X1,X2,X3),X4)=select(X1,X4)|X2=X4)). % 1.38/0.64 cnf(i_0_610, plain, (X5=X5)). % 1.38/0.64 # End listing active clauses. There is an equivalent clause to each of these in the clausification! % 1.38/0.64 # Begin printing tableau % 1.38/0.64 # Found 6 steps % 1.38/0.64 cnf(i_0_573, hypothesis, (queue_1=q0), inference(start_rule)). % 1.38/0.64 cnf(i_0_617, plain, (queue_1=q0), inference(extension_rule, [i_0_613])). % 1.38/0.64 cnf(i_0_928, plain, (queue_1!=q0), inference(closure_rule, [i_0_573])). % 1.38/0.64 cnf(i_0_927, plain, (q0=q0), inference(extension_rule, [i_0_613])). % 1.38/0.64 cnf(i_0_945, plain, (q0=s(q0)), inference(closure_rule, [i_0_357])). % 1.38/0.64 cnf(i_0_947, plain, (q0!=s(q0)), inference(etableau_closure_rule, [i_0_947, ...])). % 1.38/0.64 # End printing tableau % 1.38/0.64 # SZS output end % 1.38/0.64 # Branches closed with saturation will be marked with an "s" % 1.38/0.65 # Child (23082) has found a proof. % 1.38/0.65 % 1.38/0.65 # Proof search is over... % 1.38/0.65 # Freeing feature tree %------------------------------------------------------------------------------