%------------------------------------------------------------------------------ % File : Etableau---0.67 % Problem : SWV568-1.050 : 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 : n008.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 3.66s 1.20s % Output : CNFRefutation 3.90s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : SWV568-1.050 : TPTP v8.1.0. Released v4.0.0. % 0.06/0.12 % 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 : n008.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 : Tue Jun 14 14:50:22 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.39 # No SInE strategy applied % 0.12/0.39 # Auto-Mode selected heuristic G_E___208_C18_F1_SE_CS_SP_PS_S5PRR_RG_S04AN % 0.12/0.39 # and selection function SelectComplexExceptUniqMaxHorn. % 0.12/0.39 # % 0.12/0.39 # Presaturation interreduction done % 0.12/0.39 # Number of axioms: 498 Number of unprocessed: 498 % 0.12/0.39 # Tableaux proof search. % 0.12/0.39 # APR header successfully linked. % 0.12/0.39 # Hello from C++ % 0.61/0.78 # The folding up rule is enabled... % 0.61/0.78 # Local unification is enabled... % 0.61/0.78 # Any saturation attempts will use folding labels... % 0.61/0.78 # 498 beginning clauses after preprocessing and clausification % 0.61/0.78 # Creating start rules for all 1 conjectures. % 0.61/0.78 # There are 1 start rule candidates: % 0.61/0.78 # Found 497 unit axioms. % 0.61/0.78 # 1 start rule tableaux created. % 0.61/0.78 # 1 extension rule candidate clauses % 0.61/0.78 # 497 unit axiom clauses % 0.61/0.78 % 0.61/0.78 # Requested 8, 32 cores available to the main process. % 0.61/0.78 # There are not enough tableaux to fork, creating more from the initial 1 % 0.61/0.78 # Creating equality axioms % 0.61/0.78 # Ran out of tableaux, making start rules for all clauses % 0.61/0.78 # Returning from population with 515 new_tableaux and 0 remaining starting tableaux. % 0.61/0.78 # We now have 515 tableaux to operate on % 3.66/1.20 # There were 1 total branch saturation attempts. % 3.66/1.20 # There were 0 of these attempts blocked. % 3.66/1.20 # There were 0 deferred branch saturation attempts. % 3.66/1.20 # There were 0 free duplicated saturations. % 3.66/1.20 # There were 1 total successful branch saturations. % 3.66/1.20 # There were 0 successful branch saturations in interreduction. % 3.66/1.20 # There were 0 successful branch saturations on the branch. % 3.66/1.20 # There were 1 successful branch saturations after the branch. % 3.66/1.20 # SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.66/1.20 # SZS output start for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.66/1.20 # Begin clausification derivation % 3.66/1.20 % 3.66/1.20 # End clausification derivation % 3.66/1.20 # Begin listing active clauses obtained from FOF to CNF conversion % 3.66/1.20 cnf(i_0_945, hypothesis, (queue_1=q0)). % 3.66/1.20 cnf(i_0_960, hypothesis, (queue_103=q22)). % 3.66/1.20 cnf(i_0_961, hypothesis, (queue_109=q23)). % 3.66/1.20 cnf(i_0_962, hypothesis, (queue_118=q24)). % 3.66/1.20 cnf(i_0_963, hypothesis, (queue_124=q25)). % 3.66/1.20 cnf(i_0_947, hypothesis, (queue_13=q10)). % 3.66/1.20 cnf(i_0_964, hypothesis, (queue_130=q26)). % 3.66/1.20 cnf(i_0_965, hypothesis, (queue_139=q27)). % 3.66/1.20 cnf(i_0_966, hypothesis, (queue_145=q28)). % 3.66/1.20 cnf(i_0_967, hypothesis, (queue_151=q29)). % 3.66/1.20 cnf(i_0_968, hypothesis, (queue_160=q3)). % 3.66/1.20 cnf(i_0_969, hypothesis, (queue_169=q30)). % 3.66/1.20 cnf(i_0_970, hypothesis, (queue_175=q31)). % 3.66/1.20 cnf(i_0_971, hypothesis, (queue_181=q32)). % 3.66/1.20 cnf(i_0_948, hypothesis, (queue_19=q11)). % 3.66/1.20 cnf(i_0_972, hypothesis, (queue_190=q33)). % 3.66/1.20 cnf(i_0_973, hypothesis, (queue_196=q34)). % 3.66/1.20 cnf(i_0_974, hypothesis, (queue_202=q35)). % 3.66/1.20 cnf(i_0_975, hypothesis, (queue_211=q36)). % 3.66/1.20 cnf(i_0_976, hypothesis, (queue_217=q37)). % 3.66/1.20 cnf(i_0_977, hypothesis, (queue_223=q38)). % 3.66/1.20 cnf(i_0_978, hypothesis, (queue_232=q39)). % 3.66/1.20 cnf(i_0_979, hypothesis, (queue_238=q4)). % 3.66/1.20 cnf(i_0_980, hypothesis, (queue_244=q40)). % 3.66/1.20 cnf(i_0_981, hypothesis, (queue_250=q41)). % 3.66/1.20 cnf(i_0_982, hypothesis, (queue_259=q42)). % 3.66/1.20 cnf(i_0_983, hypothesis, (queue_265=q43)). % 3.66/1.20 cnf(i_0_984, hypothesis, (queue_271=q44)). % 3.66/1.20 cnf(i_0_949, hypothesis, (queue_28=q12)). % 3.66/1.20 cnf(i_0_985, hypothesis, (queue_280=q45)). % 3.66/1.20 cnf(i_0_986, hypothesis, (queue_286=q46)). % 3.66/1.20 cnf(i_0_987, hypothesis, (queue_292=q47)). % 3.66/1.20 cnf(i_0_988, hypothesis, (queue_301=q48)). % 3.66/1.20 cnf(i_0_989, hypothesis, (queue_307=q49)). % 3.66/1.20 cnf(i_0_990, hypothesis, (queue_313=q5)). % 3.66/1.20 cnf(i_0_991, hypothesis, (queue_319=q50)). % 3.66/1.20 cnf(i_0_992, hypothesis, (queue_328=q6)). % 3.66/1.20 cnf(i_0_993, hypothesis, (queue_334=q7)). % 3.66/1.20 cnf(i_0_950, hypothesis, (queue_34=q13)). % 3.66/1.20 cnf(i_0_994, hypothesis, (queue_340=q8)). % 3.66/1.20 cnf(i_0_995, hypothesis, (queue_349=q9)). % 3.66/1.20 cnf(i_0_951, hypothesis, (queue_40=q14)). % 3.66/1.20 cnf(i_0_952, hypothesis, (queue_49=q15)). % 3.66/1.20 cnf(i_0_953, hypothesis, (queue_55=q16)). % 3.66/1.20 cnf(i_0_954, hypothesis, (queue_61=q17)). % 3.66/1.20 cnf(i_0_946, hypothesis, (queue_7=q1)). % 3.66/1.20 cnf(i_0_955, hypothesis, (queue_70=q18)). % 3.66/1.20 cnf(i_0_956, hypothesis, (queue_76=q19)). % 3.66/1.20 cnf(i_0_957, hypothesis, (queue_82=q2)). % 3.66/1.20 cnf(i_0_958, hypothesis, (queue_88=q20)). % 3.66/1.20 cnf(i_0_959, hypothesis, (queue_97=q21)). % 3.66/1.20 cnf(i_0_687, hypothesis, (rselect_seq(q9)=earray_8)). % 3.66/1.20 cnf(i_0_822, hypothesis, (rselect_tail(q9)=index_9)). % 3.66/1.20 cnf(i_0_692, hypothesis, (rselect_seq(q21)=earray_98)). % 3.66/1.20 cnf(i_0_827, hypothesis, (rselect_tail(q21)=index_99)). % 3.66/1.20 cnf(i_0_594, hypothesis, (rselect_seq(q22)=earray_104)). % 3.66/1.20 cnf(i_0_696, hypothesis, (rselect_tail(q22)=index_105)). % 3.66/1.20 cnf(i_0_596, hypothesis, (rselect_seq(q23)=earray_110)). % 3.66/1.20 cnf(i_0_698, hypothesis, (rselect_tail(q23)=index_111)). % 3.66/1.20 cnf(i_0_598, hypothesis, (rselect_seq(q24)=earray_119)). % 3.66/1.20 cnf(i_0_703, hypothesis, (rselect_tail(q24)=index_120)). % 3.66/1.20 cnf(i_0_600, hypothesis, (rselect_seq(q25)=earray_125)). % 3.66/1.20 cnf(i_0_705, hypothesis, (rselect_tail(q25)=index_126)). % 3.66/1.20 cnf(i_0_602, hypothesis, (rselect_seq(q26)=earray_131)). % 3.66/1.20 cnf(i_0_707, hypothesis, (rselect_tail(q26)=index_132)). % 3.66/1.20 cnf(i_0_604, hypothesis, (rselect_seq(q10)=earray_14)). % 3.66/1.20 cnf(i_0_605, hypothesis, (rselect_seq(q27)=earray_140)). % 3.66/1.20 cnf(i_0_711, hypothesis, (rselect_tail(q27)=index_141)). % 3.66/1.20 cnf(i_0_607, hypothesis, (rselect_seq(q28)=earray_146)). % 3.66/1.20 cnf(i_0_713, hypothesis, (rselect_tail(q28)=index_147)). % 3.66/1.20 cnf(i_0_609, hypothesis, (rselect_seq(q2)=earray_152)). % 3.66/1.20 cnf(i_0_716, hypothesis, (rselect_tail(q2)=index_153)). % 3.66/1.20 cnf(i_0_714, hypothesis, (rselect_tail(q10)=index_15)). % 3.66/1.20 cnf(i_0_612, hypothesis, (rselect_seq(q29)=earray_161)). % 3.66/1.20 cnf(i_0_720, hypothesis, (rselect_tail(q29)=index_162)). % 3.66/1.20 cnf(i_0_614, hypothesis, (rselect_seq(q30)=earray_170)). % 3.66/1.20 cnf(i_0_724, hypothesis, (rselect_tail(q30)=index_171)). % 3.66/1.20 cnf(i_0_616, hypothesis, (rselect_seq(q31)=earray_176)). % 3.66/1.20 cnf(i_0_726, hypothesis, (rselect_tail(q31)=index_177)). % 3.66/1.20 cnf(i_0_618, hypothesis, (rselect_seq(q32)=earray_182)). % 3.66/1.20 cnf(i_0_729, hypothesis, (rselect_tail(q32)=index_183)). % 3.66/1.20 cnf(i_0_620, hypothesis, (rselect_seq(q33)=earray_191)). % 3.66/1.20 cnf(i_0_733, hypothesis, (rselect_tail(q33)=index_192)). % 3.66/1.20 cnf(i_0_622, hypothesis, (rselect_seq(q34)=earray_197)). % 3.66/1.20 cnf(i_0_735, hypothesis, (rselect_tail(q34)=index_198)). % 3.66/1.20 cnf(i_0_624, hypothesis, (rselect_seq(q0)=earray_2)). % 3.66/1.20 cnf(i_0_625, hypothesis, (rselect_seq(q11)=earray_20)). % 3.66/1.20 cnf(i_0_626, hypothesis, (rselect_seq(q35)=earray_203)). % 3.66/1.20 cnf(i_0_737, hypothesis, (rselect_tail(q35)=index_204)). % 3.66/1.20 cnf(i_0_628, hypothesis, (rselect_seq(q36)=earray_212)). % 3.66/1.20 cnf(i_0_742, hypothesis, (rselect_tail(q36)=index_213)). % 3.66/1.20 cnf(i_0_630, hypothesis, (rselect_seq(q37)=earray_218)). % 3.66/1.20 cnf(i_0_740, hypothesis, (rselect_tail(q11)=index_21)). % 3.66/1.20 cnf(i_0_744, hypothesis, (rselect_tail(q37)=index_219)). % 3.66/1.20 cnf(i_0_633, hypothesis, (rselect_seq(q38)=earray_224)). % 3.66/1.20 cnf(i_0_746, hypothesis, (rselect_tail(q38)=index_225)). % 3.66/1.20 cnf(i_0_635, hypothesis, (rselect_seq(q3)=earray_233)). % 3.66/1.20 cnf(i_0_750, hypothesis, (rselect_tail(q3)=index_234)). % 3.66/1.20 cnf(i_0_637, hypothesis, (rselect_seq(q39)=earray_239)). % 3.66/1.20 cnf(i_0_753, hypothesis, (rselect_tail(q39)=index_240)). % 3.66/1.20 cnf(i_0_639, hypothesis, (rselect_seq(q40)=earray_245)). % 3.66/1.20 cnf(i_0_755, hypothesis, (rselect_tail(q40)=index_246)). % 3.66/1.20 cnf(i_0_641, hypothesis, (rselect_seq(q41)=earray_251)). % 3.66/1.20 cnf(i_0_757, hypothesis, (rselect_tail(q41)=index_252)). % 3.66/1.20 cnf(i_0_643, hypothesis, (rselect_seq(q42)=earray_260)). % 3.66/1.20 cnf(i_0_762, hypothesis, (rselect_tail(q42)=index_261)). % 3.66/1.20 cnf(i_0_645, hypothesis, (rselect_seq(q43)=earray_266)). % 3.66/1.20 cnf(i_0_764, hypothesis, (rselect_tail(q43)=index_267)). % 3.66/1.20 cnf(i_0_647, hypothesis, (rselect_seq(q44)=earray_272)). % 3.66/1.20 cnf(i_0_767, hypothesis, (rselect_tail(q44)=index_273)). % 3.66/1.20 cnf(i_0_649, hypothesis, (rselect_seq(q45)=earray_281)). % 3.66/1.20 cnf(i_0_771, hypothesis, (rselect_tail(q45)=index_282)). % 3.66/1.20 cnf(i_0_651, hypothesis, (rselect_seq(q46)=earray_287)). % 3.66/1.20 cnf(i_0_773, hypothesis, (rselect_tail(q46)=index_288)). % 3.66/1.20 cnf(i_0_653, hypothesis, (rselect_seq(q12)=earray_29)). % 3.66/1.20 cnf(i_0_654, hypothesis, (rselect_seq(q47)=earray_293)). % 3.66/1.20 cnf(i_0_775, hypothesis, (rselect_tail(q47)=index_294)). % 3.66/1.20 cnf(i_0_656, hypothesis, (rselect_seq(q48)=earray_302)). % 3.66/1.20 cnf(i_0_781, hypothesis, (rselect_tail(q48)=index_303)). % 3.66/1.20 cnf(i_0_658, hypothesis, (rselect_seq(q4)=earray_308)). % 3.66/1.20 cnf(i_0_779, hypothesis, (rselect_tail(q12)=index_30)). % 3.66/1.20 cnf(i_0_783, hypothesis, (rselect_tail(q4)=index_309)). % 3.66/1.20 cnf(i_0_661, hypothesis, (rselect_seq(q49)=earray_314)). % 3.66/1.20 cnf(i_0_785, hypothesis, (rselect_tail(q49)=index_315)). % 3.66/1.20 cnf(i_0_663, hypothesis, (rselect_seq(q5)=earray_320)). % 3.66/1.20 cnf(i_0_787, hypothesis, (rselect_tail(q5)=index_321)). % 3.66/1.20 cnf(i_0_665, hypothesis, (rselect_seq(q6)=earray_329)). % 3.66/1.20 cnf(i_0_792, hypothesis, (rselect_tail(q6)=index_330)). % 3.66/1.20 cnf(i_0_667, hypothesis, (rselect_seq(q7)=earray_335)). % 3.66/1.20 cnf(i_0_794, hypothesis, (rselect_tail(q7)=index_336)). % 3.66/1.20 cnf(i_0_669, hypothesis, (rselect_seq(q8)=earray_341)). % 3.66/1.20 cnf(i_0_796, hypothesis, (rselect_tail(q8)=index_342)). % 3.66/1.20 cnf(i_0_671, hypothesis, (rselect_seq(q13)=earray_35)). % 3.66/1.20 cnf(i_0_672, hypothesis, (rselect_seq(q50)=earray_350)). % 3.66/1.20 cnf(i_0_801, hypothesis, (rselect_tail(q13)=index_36)). % 3.66/1.20 cnf(i_0_778, hypothesis, (rselect_tail(q0)=index_3)). % 3.66/1.20 cnf(i_0_675, hypothesis, (rselect_seq(q14)=earray_41)). % 3.66/1.20 cnf(i_0_803, hypothesis, (rselect_tail(q14)=index_42)). % 3.66/1.20 cnf(i_0_677, hypothesis, (rselect_seq(q15)=earray_50)). % 3.66/1.20 cnf(i_0_807, hypothesis, (rselect_tail(q15)=index_51)). % 3.66/1.20 cnf(i_0_679, hypothesis, (rselect_seq(q16)=earray_56)). % 3.66/1.20 cnf(i_0_809, hypothesis, (rselect_tail(q16)=index_57)). % 3.66/1.20 cnf(i_0_681, hypothesis, (rselect_seq(q17)=earray_62)). % 3.66/1.20 cnf(i_0_812, hypothesis, (rselect_tail(q17)=index_63)). % 3.66/1.20 cnf(i_0_683, hypothesis, (rselect_seq(q18)=earray_71)). % 3.66/1.20 cnf(i_0_816, hypothesis, (rselect_tail(q18)=index_72)). % 3.66/1.20 cnf(i_0_685, hypothesis, (rselect_seq(q1)=earray_77)). % 3.66/1.20 cnf(i_0_818, hypothesis, (rselect_tail(q1)=index_78)). % 3.66/1.20 cnf(i_0_688, hypothesis, (rselect_seq(q19)=earray_83)). % 3.66/1.20 cnf(i_0_820, hypothesis, (rselect_tail(q19)=index_84)). % 3.66/1.20 cnf(i_0_690, hypothesis, (rselect_seq(q20)=earray_89)). % 3.66/1.20 cnf(i_0_823, hypothesis, (rselect_tail(q20)=index_90)). % 3.66/1.20 cnf(i_0_800, hypothesis, (rselect_head(q50)=index_351)). % 3.66/1.20 cnf(i_0_694, hypothesis, (rselect_tail(q)=index_0)). % 3.66/1.20 cnf(i_0_695, hypothesis, (s(index_99)=index_102)). % 3.66/1.20 cnf(i_0_697, hypothesis, (s(index_105)=index_108)). % 3.66/1.20 cnf(i_0_699, hypothesis, (s(index_111)=index_114)). % 3.66/1.20 cnf(i_0_700, hypothesis, (rselect_head(queue_115)=index_116)). % 3.66/1.20 cnf(i_0_701, hypothesis, (s(index_116)=index_117)). % 3.66/1.20 cnf(i_0_702, hypothesis, (s(index_9)=index_12)). % 3.66/1.20 cnf(i_0_704, hypothesis, (s(index_120)=index_123)). % 3.66/1.20 cnf(i_0_706, hypothesis, (s(index_126)=index_129)). % 3.66/1.20 cnf(i_0_708, hypothesis, (s(index_132)=index_135)). % 3.66/1.20 cnf(i_0_709, hypothesis, (rselect_head(queue_136)=index_137)). % 3.66/1.20 cnf(i_0_710, hypothesis, (s(index_137)=index_138)). % 3.66/1.20 cnf(i_0_712, hypothesis, (s(index_141)=index_144)). % 3.66/1.20 cnf(i_0_715, hypothesis, (s(index_147)=index_150)). % 3.66/1.20 cnf(i_0_717, hypothesis, (s(index_153)=index_156)). % 3.66/1.20 cnf(i_0_718, hypothesis, (rselect_head(queue_157)=index_158)). % 3.66/1.20 cnf(i_0_719, hypothesis, (s(index_158)=index_159)). % 3.66/1.20 cnf(i_0_721, hypothesis, (s(index_162)=index_165)). % 3.66/1.20 cnf(i_0_722, hypothesis, (rselect_head(queue_166)=index_167)). % 3.66/1.20 cnf(i_0_723, hypothesis, (s(index_167)=index_168)). % 3.66/1.20 cnf(i_0_725, hypothesis, (s(index_171)=index_174)). % 3.66/1.20 cnf(i_0_727, hypothesis, (s(index_15)=index_18)). % 3.66/1.20 cnf(i_0_728, hypothesis, (s(index_177)=index_180)). % 3.66/1.20 cnf(i_0_730, hypothesis, (s(index_183)=index_186)). % 3.66/1.20 cnf(i_0_731, hypothesis, (rselect_head(queue_187)=index_188)). % 3.66/1.20 cnf(i_0_732, hypothesis, (s(index_188)=index_189)). % 3.66/1.20 cnf(i_0_734, hypothesis, (s(index_192)=index_195)). % 3.66/1.20 cnf(i_0_736, hypothesis, (s(index_198)=index_201)). % 3.66/1.20 cnf(i_0_738, hypothesis, (s(index_204)=index_207)). % 3.66/1.20 cnf(i_0_739, hypothesis, (rselect_head(queue_208)=index_209)). % 3.66/1.20 cnf(i_0_741, hypothesis, (s(index_209)=index_210)). % 3.66/1.20 cnf(i_0_743, hypothesis, (s(index_213)=index_216)). % 3.66/1.20 cnf(i_0_745, hypothesis, (s(index_219)=index_222)). % 3.66/1.20 cnf(i_0_747, hypothesis, (s(index_225)=index_228)). % 3.66/1.20 cnf(i_0_748, hypothesis, (rselect_head(queue_229)=index_230)). % 3.66/1.20 cnf(i_0_749, hypothesis, (s(index_230)=index_231)). % 3.66/1.20 cnf(i_0_751, hypothesis, (s(index_234)=index_237)). % 3.66/1.20 cnf(i_0_752, hypothesis, (s(index_21)=index_24)). % 3.66/1.20 cnf(i_0_754, hypothesis, (s(index_240)=index_243)). % 3.66/1.20 cnf(i_0_756, hypothesis, (s(index_246)=index_249)). % 3.66/1.20 cnf(i_0_758, hypothesis, (s(index_252)=index_255)). % 3.66/1.20 cnf(i_0_759, hypothesis, (rselect_head(queue_256)=index_257)). % 3.66/1.20 cnf(i_0_760, hypothesis, (s(index_257)=index_258)). % 3.66/1.20 cnf(i_0_761, hypothesis, (rselect_head(queue_25)=index_26)). % 3.66/1.20 cnf(i_0_763, hypothesis, (s(index_261)=index_264)). % 3.66/1.20 cnf(i_0_765, hypothesis, (s(index_26)=index_27)). % 3.66/1.20 cnf(i_0_766, hypothesis, (s(index_267)=index_270)). % 3.66/1.20 cnf(i_0_768, hypothesis, (s(index_273)=index_276)). % 3.66/1.20 cnf(i_0_769, hypothesis, (rselect_head(queue_277)=index_278)). % 3.66/1.20 cnf(i_0_770, hypothesis, (s(index_278)=index_279)). % 3.66/1.20 cnf(i_0_772, hypothesis, (s(index_282)=index_285)). % 3.66/1.20 cnf(i_0_774, hypothesis, (s(index_288)=index_291)). % 3.66/1.20 cnf(i_0_776, hypothesis, (s(index_294)=index_297)). % 3.66/1.20 cnf(i_0_777, hypothesis, (rselect_head(queue_298)=index_299)). % 3.66/1.20 cnf(i_0_780, hypothesis, (s(index_299)=index_300)). % 3.66/1.20 cnf(i_0_782, hypothesis, (s(index_303)=index_306)). % 3.66/1.20 cnf(i_0_784, hypothesis, (s(index_309)=index_312)). % 3.66/1.20 cnf(i_0_786, hypothesis, (s(index_315)=index_318)). % 3.66/1.20 cnf(i_0_788, hypothesis, (s(index_321)=index_324)). % 3.66/1.20 cnf(i_0_789, hypothesis, (rselect_head(queue_325)=index_326)). % 3.66/1.20 cnf(i_0_790, hypothesis, (s(index_326)=index_327)). % 3.66/1.20 cnf(i_0_791, hypothesis, (s(index_30)=index_33)). % 3.66/1.20 cnf(i_0_793, hypothesis, (s(index_330)=index_333)). % 3.66/1.20 cnf(i_0_795, hypothesis, (s(index_336)=index_339)). % 3.66/1.20 cnf(i_0_797, hypothesis, (s(index_342)=index_345)). % 3.66/1.20 cnf(i_0_798, hypothesis, (rselect_head(queue_346)=index_347)). % 3.66/1.20 cnf(i_0_799, hypothesis, (s(index_347)=index_348)). % 3.66/1.20 cnf(i_0_802, hypothesis, (s(index_36)=index_39)). % 3.66/1.20 cnf(i_0_804, hypothesis, (s(index_42)=index_45)). % 3.66/1.20 cnf(i_0_805, hypothesis, (rselect_head(queue_46)=index_47)). % 3.66/1.20 cnf(i_0_806, hypothesis, (s(index_47)=index_48)). % 3.66/1.20 cnf(i_0_808, hypothesis, (s(index_51)=index_54)). % 3.66/1.20 cnf(i_0_810, hypothesis, (s(index_3)=index_6)). % 3.66/1.20 cnf(i_0_811, hypothesis, (s(index_57)=index_60)). % 3.66/1.20 cnf(i_0_813, hypothesis, (s(index_63)=index_66)). % 3.66/1.20 cnf(i_0_814, hypothesis, (rselect_head(queue_67)=index_68)). % 3.66/1.20 cnf(i_0_815, hypothesis, (s(index_68)=index_69)). % 3.66/1.20 cnf(i_0_817, hypothesis, (s(index_72)=index_75)). % 3.66/1.20 cnf(i_0_819, hypothesis, (s(index_78)=index_81)). % 3.66/1.20 cnf(i_0_821, hypothesis, (s(index_84)=index_87)). % 3.66/1.20 cnf(i_0_824, hypothesis, (s(index_90)=index_93)). % 3.66/1.20 cnf(i_0_825, hypothesis, (rselect_head(queue_94)=index_95)). % 3.66/1.20 cnf(i_0_826, hypothesis, (s(index_95)=index_96)). % 3.66/1.20 cnf(i_0_693, hypothesis, (select(earray_350,index_351)=elem_352)). % 3.66/1.20 cnf(i_0_835, hypothesis, (rstore_tail(queue_113,index_114)=queue_115)). % 3.66/1.20 cnf(i_0_843, hypothesis, (rstore_tail(queue_134,index_135)=queue_136)). % 3.66/1.20 cnf(i_0_850, hypothesis, (rstore_tail(queue_155,index_156)=queue_157)). % 3.66/1.20 cnf(i_0_853, hypothesis, (rstore_tail(queue_164,index_165)=queue_166)). % 3.66/1.20 cnf(i_0_861, hypothesis, (rstore_tail(queue_185,index_186)=queue_187)). % 3.66/1.20 cnf(i_0_869, hypothesis, (rstore_tail(queue_206,index_207)=queue_208)). % 3.66/1.20 cnf(i_0_876, hypothesis, (rstore_tail(queue_227,index_228)=queue_229)). % 3.66/1.20 cnf(i_0_887, hypothesis, (rstore_tail(queue_254,index_255)=queue_256)). % 3.66/1.20 cnf(i_0_884, hypothesis, (rstore_tail(queue_23,index_24)=queue_25)). % 3.66/1.20 cnf(i_0_894, hypothesis, (rstore_tail(queue_275,index_276)=queue_277)). % 3.66/1.20 cnf(i_0_902, hypothesis, (rstore_tail(queue_296,index_297)=queue_298)). % 3.66/1.20 cnf(i_0_912, hypothesis, (rstore_tail(queue_323,index_324)=queue_325)). % 3.66/1.20 cnf(i_0_920, hypothesis, (rstore_tail(queue_344,index_345)=queue_346)). % 3.66/1.20 cnf(i_0_925, hypothesis, (rstore_tail(queue_44,index_45)=queue_46)). % 3.66/1.20 cnf(i_0_933, hypothesis, (rstore_tail(queue_65,index_66)=queue_67)). % 3.66/1.20 cnf(i_0_943, hypothesis, (rstore_tail(queue_92,index_93)=queue_94)). % 3.66/1.20 cnf(i_0_828, hypothesis, (rstore_head(q,index_0)=q0)). % 3.66/1.20 cnf(i_0_829, hypothesis, (rstore_seq(q21,earray_100)=queue_101)). % 3.66/1.20 cnf(i_0_830, hypothesis, (rstore_tail(queue_101,index_102)=q22)). % 3.66/1.20 cnf(i_0_831, hypothesis, (rstore_seq(q22,earray_106)=queue_107)). % 3.66/1.20 cnf(i_0_832, hypothesis, (rstore_tail(queue_107,index_108)=q23)). % 3.66/1.20 cnf(i_0_833, hypothesis, (rstore_seq(q9,earray_10)=queue_11)). % 3.66/1.20 cnf(i_0_834, hypothesis, (rstore_seq(q23,earray_112)=queue_113)). % 3.66/1.20 cnf(i_0_836, hypothesis, (rstore_head(queue_115,index_117)=q24)). % 3.66/1.20 cnf(i_0_837, hypothesis, (rstore_seq(q24,earray_121)=queue_122)). % 3.66/1.20 cnf(i_0_838, hypothesis, (rstore_tail(queue_122,index_123)=q25)). % 3.66/1.20 cnf(i_0_839, hypothesis, (rstore_seq(q25,earray_127)=queue_128)). % 3.66/1.20 cnf(i_0_840, hypothesis, (rstore_tail(queue_11,index_12)=q10)). % 3.66/1.20 cnf(i_0_841, hypothesis, (rstore_tail(queue_128,index_129)=q26)). % 3.66/1.20 cnf(i_0_842, hypothesis, (rstore_seq(q26,earray_133)=queue_134)). % 3.66/1.20 cnf(i_0_844, hypothesis, (rstore_head(queue_136,index_138)=q27)). % 3.66/1.20 cnf(i_0_845, hypothesis, (rstore_seq(q27,earray_142)=queue_143)). % 3.66/1.20 cnf(i_0_846, hypothesis, (rstore_tail(queue_143,index_144)=q28)). % 3.66/1.20 cnf(i_0_847, hypothesis, (rstore_seq(q28,earray_148)=queue_149)). % 3.66/1.20 cnf(i_0_848, hypothesis, (rstore_tail(queue_149,index_150)=q29)). % 3.66/1.20 cnf(i_0_849, hypothesis, (rstore_seq(q2,earray_154)=queue_155)). % 3.66/1.20 cnf(i_0_851, hypothesis, (rstore_head(queue_157,index_159)=q3)). % 3.66/1.20 cnf(i_0_852, hypothesis, (rstore_seq(q29,earray_163)=queue_164)). % 3.66/1.20 cnf(i_0_854, hypothesis, (rstore_head(queue_166,index_168)=q30)). % 3.66/1.20 cnf(i_0_855, hypothesis, (rstore_seq(q10,earray_16)=queue_17)). % 3.66/1.20 cnf(i_0_856, hypothesis, (rstore_seq(q30,earray_172)=queue_173)). % 3.66/1.20 cnf(i_0_857, hypothesis, (rstore_tail(queue_173,index_174)=q31)). % 3.66/1.20 cnf(i_0_858, hypothesis, (rstore_seq(q31,earray_178)=queue_179)). % 3.66/1.20 cnf(i_0_859, hypothesis, (rstore_tail(queue_179,index_180)=q32)). % 3.66/1.20 cnf(i_0_860, hypothesis, (rstore_seq(q32,earray_184)=queue_185)). % 3.66/1.20 cnf(i_0_862, hypothesis, (rstore_tail(queue_17,index_18)=q11)). % 3.66/1.20 cnf(i_0_863, hypothesis, (rstore_head(queue_187,index_189)=q33)). % 3.66/1.20 cnf(i_0_864, hypothesis, (rstore_seq(q33,earray_193)=queue_194)). % 3.66/1.20 cnf(i_0_865, hypothesis, (rstore_tail(queue_194,index_195)=q34)). % 3.66/1.20 cnf(i_0_866, hypothesis, (rstore_seq(q34,earray_199)=queue_200)). % 3.66/1.20 cnf(i_0_867, hypothesis, (rstore_tail(queue_200,index_201)=q35)). % 3.66/1.20 cnf(i_0_868, hypothesis, (rstore_seq(q35,earray_205)=queue_206)). % 3.66/1.20 cnf(i_0_870, hypothesis, (rstore_head(queue_208,index_210)=q36)). % 3.66/1.20 cnf(i_0_871, hypothesis, (rstore_seq(q36,earray_214)=queue_215)). % 3.66/1.20 cnf(i_0_872, hypothesis, (rstore_tail(queue_215,index_216)=q37)). % 3.66/1.20 cnf(i_0_873, hypothesis, (rstore_seq(q37,earray_220)=queue_221)). % 3.66/1.20 cnf(i_0_874, hypothesis, (rstore_tail(queue_221,index_222)=q38)). % 3.66/1.20 cnf(i_0_875, hypothesis, (rstore_seq(q38,earray_226)=queue_227)). % 3.66/1.20 cnf(i_0_877, hypothesis, (rstore_seq(q11,earray_22)=queue_23)). % 3.66/1.20 cnf(i_0_878, hypothesis, (rstore_head(queue_229,index_231)=q39)). % 3.66/1.20 cnf(i_0_879, hypothesis, (rstore_seq(q3,earray_235)=queue_236)). % 3.66/1.20 cnf(i_0_880, hypothesis, (rstore_tail(queue_236,index_237)=q4)). % 3.66/1.20 cnf(i_0_881, hypothesis, (rstore_seq(q39,earray_241)=queue_242)). % 3.66/1.20 cnf(i_0_882, hypothesis, (rstore_tail(queue_242,index_243)=q40)). % 3.66/1.20 cnf(i_0_883, hypothesis, (rstore_seq(q40,earray_247)=queue_248)). % 3.66/1.20 cnf(i_0_885, hypothesis, (rstore_tail(queue_248,index_249)=q41)). % 3.66/1.20 cnf(i_0_886, hypothesis, (rstore_seq(q41,earray_253)=queue_254)). % 3.66/1.20 cnf(i_0_888, hypothesis, (rstore_head(queue_256,index_258)=q42)). % 3.66/1.20 cnf(i_0_889, hypothesis, (rstore_seq(q42,earray_262)=queue_263)). % 3.66/1.20 cnf(i_0_890, hypothesis, (rstore_tail(queue_263,index_264)=q43)). % 3.66/1.20 cnf(i_0_891, hypothesis, (rstore_seq(q43,earray_268)=queue_269)). % 3.66/1.20 cnf(i_0_892, hypothesis, (rstore_tail(queue_269,index_270)=q44)). % 3.66/1.20 cnf(i_0_893, hypothesis, (rstore_seq(q44,earray_274)=queue_275)). % 3.66/1.20 cnf(i_0_895, hypothesis, (rstore_head(queue_25,index_27)=q12)). % 3.66/1.20 cnf(i_0_896, hypothesis, (rstore_head(queue_277,index_279)=q45)). % 3.66/1.20 cnf(i_0_897, hypothesis, (rstore_seq(q45,earray_283)=queue_284)). % 3.66/1.20 cnf(i_0_898, hypothesis, (rstore_tail(queue_284,index_285)=q46)). % 3.66/1.20 cnf(i_0_899, hypothesis, (rstore_seq(q46,earray_289)=queue_290)). % 3.66/1.20 cnf(i_0_900, hypothesis, (rstore_tail(queue_290,index_291)=q47)). % 3.66/1.20 cnf(i_0_901, hypothesis, (rstore_seq(q47,earray_295)=queue_296)). % 3.66/1.20 cnf(i_0_903, hypothesis, (rstore_head(queue_298,index_300)=q48)). % 3.66/1.20 cnf(i_0_904, hypothesis, (rstore_seq(q48,earray_304)=queue_305)). % 3.66/1.20 cnf(i_0_905, hypothesis, (rstore_tail(queue_305,index_306)=q49)). % 3.66/1.20 cnf(i_0_906, hypothesis, (rstore_seq(q4,earray_310)=queue_311)). % 3.66/1.20 cnf(i_0_907, hypothesis, (rstore_tail(queue_311,index_312)=q5)). % 3.66/1.20 cnf(i_0_908, hypothesis, (rstore_seq(q49,earray_316)=queue_317)). % 3.66/1.20 cnf(i_0_909, hypothesis, (rstore_tail(queue_317,index_318)=q50)). % 3.66/1.20 cnf(i_0_910, hypothesis, (rstore_seq(q12,earray_31)=queue_32)). % 3.66/1.20 cnf(i_0_911, hypothesis, (rstore_seq(q5,earray_322)=queue_323)). % 3.66/1.20 cnf(i_0_913, hypothesis, (rstore_head(queue_325,index_327)=q6)). % 3.66/1.20 cnf(i_0_914, hypothesis, (rstore_seq(q6,earray_331)=queue_332)). % 3.66/1.20 cnf(i_0_915, hypothesis, (rstore_tail(queue_332,index_333)=q7)). % 3.66/1.20 cnf(i_0_916, hypothesis, (rstore_seq(q7,earray_337)=queue_338)). % 3.66/1.20 cnf(i_0_917, hypothesis, (rstore_tail(queue_32,index_33)=q13)). % 3.66/1.20 cnf(i_0_918, hypothesis, (rstore_tail(queue_338,index_339)=q8)). % 3.66/1.20 cnf(i_0_919, hypothesis, (rstore_seq(q8,earray_343)=queue_344)). % 3.66/1.20 cnf(i_0_921, hypothesis, (rstore_head(queue_346,index_348)=q9)). % 3.66/1.20 cnf(i_0_922, hypothesis, (rstore_seq(q13,earray_37)=queue_38)). % 3.66/1.20 cnf(i_0_923, hypothesis, (rstore_tail(queue_38,index_39)=q14)). % 3.66/1.20 cnf(i_0_924, hypothesis, (rstore_seq(q14,earray_43)=queue_44)). % 3.66/1.20 cnf(i_0_926, hypothesis, (rstore_head(queue_46,index_48)=q15)). % 3.66/1.20 cnf(i_0_927, hypothesis, (rstore_seq(q0,earray_4)=queue_5)). % 3.66/1.20 cnf(i_0_928, hypothesis, (rstore_seq(q15,earray_52)=queue_53)). % 3.66/1.20 cnf(i_0_929, hypothesis, (rstore_tail(queue_53,index_54)=q16)). % 3.66/1.20 cnf(i_0_930, hypothesis, (rstore_seq(q16,earray_58)=queue_59)). % 3.66/1.20 cnf(i_0_931, hypothesis, (rstore_tail(queue_59,index_60)=q17)). % 3.66/1.20 cnf(i_0_932, hypothesis, (rstore_seq(q17,earray_64)=queue_65)). % 3.66/1.20 cnf(i_0_934, hypothesis, (rstore_tail(queue_5,index_6)=q1)). % 3.66/1.20 cnf(i_0_935, hypothesis, (rstore_head(queue_67,index_69)=q18)). % 3.66/1.20 cnf(i_0_936, hypothesis, (rstore_seq(q18,earray_73)=queue_74)). % 3.66/1.20 cnf(i_0_937, hypothesis, (rstore_tail(queue_74,index_75)=q19)). % 3.66/1.20 cnf(i_0_938, hypothesis, (rstore_seq(q1,earray_79)=queue_80)). % 3.66/1.20 cnf(i_0_939, hypothesis, (rstore_tail(queue_80,index_81)=q2)). % 3.66/1.20 cnf(i_0_940, hypothesis, (rstore_seq(q19,earray_85)=queue_86)). % 3.66/1.20 cnf(i_0_941, hypothesis, (rstore_tail(queue_86,index_87)=q20)). % 3.66/1.20 cnf(i_0_942, hypothesis, (rstore_seq(q20,earray_91)=queue_92)). % 3.66/1.20 cnf(i_0_944, hypothesis, (rstore_head(queue_94,index_96)=q21)). % 3.66/1.20 cnf(i_0_501, plain, (rselect_seq(rstore_seq(X1,X2))=X2)). % 3.66/1.20 cnf(i_0_502, plain, (rselect_head(rstore_head(X1,X2))=X2)). % 3.66/1.20 cnf(i_0_680, hypothesis, (store(earray_56,index_57,e16)=earray_58)). % 3.66/1.20 cnf(i_0_503, plain, (rselect_tail(rstore_tail(X1,X2))=X2)). % 3.66/1.20 cnf(i_0_592, hypothesis, (store(earray_8,index_9,e9)=earray_10)). % 3.66/1.20 cnf(i_0_593, hypothesis, (store(earray_98,index_99,e21)=earray_100)). % 3.66/1.20 cnf(i_0_595, hypothesis, (store(earray_104,index_105,e22)=earray_106)). % 3.66/1.20 cnf(i_0_504, plain, (rselect_seq(rstore_head(X1,X2))=rselect_seq(X1))). % 3.66/1.20 cnf(i_0_597, hypothesis, (store(earray_110,index_111,e23)=earray_112)). % 3.66/1.20 cnf(i_0_505, plain, (rselect_seq(rstore_tail(X1,X2))=rselect_seq(X1))). % 3.66/1.20 cnf(i_0_507, plain, (rselect_head(rstore_seq(X1,X2))=rselect_head(X1))). % 3.66/1.20 cnf(i_0_506, plain, (rselect_head(rstore_tail(X1,X2))=rselect_head(X1))). % 3.66/1.20 cnf(i_0_599, hypothesis, (store(earray_119,index_120,e24)=earray_121)). % 3.66/1.20 cnf(i_0_601, hypothesis, (store(earray_125,index_126,e25)=earray_127)). % 3.66/1.20 cnf(i_0_603, hypothesis, (store(earray_131,index_132,e26)=earray_133)). % 3.66/1.20 cnf(i_0_606, hypothesis, (store(earray_140,index_141,e27)=earray_142)). % 3.66/1.20 cnf(i_0_608, hypothesis, (store(earray_146,index_147,e28)=earray_148)). % 3.66/1.20 cnf(i_0_508, plain, (rselect_tail(rstore_seq(X1,X2))=rselect_tail(X1))). % 3.66/1.20 cnf(i_0_610, hypothesis, (store(earray_152,index_153,e2)=earray_154)). % 3.66/1.20 cnf(i_0_509, plain, (rselect_tail(rstore_head(X1,X2))=rselect_tail(X1))). % 3.66/1.20 cnf(i_0_611, hypothesis, (store(earray_14,index_15,e10)=earray_16)). % 3.66/1.20 cnf(i_0_613, hypothesis, (store(earray_161,index_162,e29)=earray_163)). % 3.66/1.20 cnf(i_0_615, hypothesis, (store(earray_170,index_171,e30)=earray_172)). % 3.66/1.20 cnf(i_0_617, hypothesis, (store(earray_176,index_177,e31)=earray_178)). % 3.66/1.20 cnf(i_0_619, hypothesis, (store(earray_182,index_183,e32)=earray_184)). % 3.66/1.20 cnf(i_0_621, hypothesis, (store(earray_191,index_192,e33)=earray_193)). % 3.66/1.20 cnf(i_0_623, hypothesis, (store(earray_197,index_198,e34)=earray_199)). % 3.66/1.20 cnf(i_0_627, hypothesis, (store(earray_203,index_204,e35)=earray_205)). % 3.66/1.20 cnf(i_0_629, hypothesis, (store(earray_212,index_213,e36)=earray_214)). % 3.66/1.20 cnf(i_0_631, hypothesis, (store(earray_20,index_21,e11)=earray_22)). % 3.66/1.20 cnf(i_0_632, hypothesis, (store(earray_218,index_219,e37)=earray_220)). % 3.66/1.20 cnf(i_0_634, hypothesis, (store(earray_224,index_225,e38)=earray_226)). % 3.66/1.20 cnf(i_0_636, hypothesis, (store(earray_233,index_234,e3)=earray_235)). % 3.66/1.20 cnf(i_0_638, hypothesis, (store(earray_239,index_240,e39)=earray_241)). % 3.66/1.20 cnf(i_0_640, hypothesis, (store(earray_245,index_246,e40)=earray_247)). % 3.66/1.20 cnf(i_0_642, hypothesis, (store(earray_251,index_252,e41)=earray_253)). % 3.66/1.20 cnf(i_0_644, hypothesis, (store(earray_260,index_261,e42)=earray_262)). % 3.66/1.20 cnf(i_0_646, hypothesis, (store(earray_266,index_267,e43)=earray_268)). % 3.66/1.20 cnf(i_0_648, hypothesis, (store(earray_272,index_273,e44)=earray_274)). % 3.66/1.20 cnf(i_0_650, hypothesis, (store(earray_281,index_282,e45)=earray_283)). % 3.66/1.20 cnf(i_0_652, hypothesis, (store(earray_287,index_288,e46)=earray_289)). % 3.66/1.20 cnf(i_0_655, hypothesis, (store(earray_293,index_294,e47)=earray_295)). % 3.66/1.20 cnf(i_0_657, hypothesis, (store(earray_302,index_303,e48)=earray_304)). % 3.66/1.20 cnf(i_0_659, hypothesis, (store(earray_29,index_30,e12)=earray_31)). % 3.90/1.20 cnf(i_0_660, hypothesis, (store(earray_308,index_309,e4)=earray_310)). % 3.90/1.20 cnf(i_0_662, hypothesis, (store(earray_314,index_315,e49)=earray_316)). % 3.90/1.20 cnf(i_0_664, hypothesis, (store(earray_320,index_321,e5)=earray_322)). % 3.90/1.20 cnf(i_0_666, hypothesis, (store(earray_329,index_330,e6)=earray_331)). % 3.90/1.20 cnf(i_0_668, hypothesis, (store(earray_335,index_336,e7)=earray_337)). % 3.90/1.20 cnf(i_0_670, hypothesis, (store(earray_341,index_342,e8)=earray_343)). % 3.90/1.20 cnf(i_0_673, hypothesis, (store(earray_35,index_36,e13)=earray_37)). % 3.90/1.20 cnf(i_0_674, hypothesis, (store(earray_2,index_3,e0)=earray_4)). % 3.90/1.20 cnf(i_0_676, hypothesis, (store(earray_41,index_42,e14)=earray_43)). % 3.90/1.20 cnf(i_0_678, hypothesis, (store(earray_50,index_51,e15)=earray_52)). % 3.90/1.20 cnf(i_0_682, hypothesis, (store(earray_62,index_63,e17)=earray_64)). % 3.90/1.20 cnf(i_0_684, hypothesis, (store(earray_71,index_72,e18)=earray_73)). % 3.90/1.20 cnf(i_0_686, hypothesis, (store(earray_77,index_78,e1)=earray_79)). % 3.90/1.20 cnf(i_0_689, hypothesis, (store(earray_83,index_84,e19)=earray_85)). % 3.90/1.20 cnf(i_0_691, hypothesis, (store(earray_89,index_90,e20)=earray_91)). % 3.90/1.20 cnf(i_0_499, plain, (select(store(X1,X2,X3),X2)=X3)). % 3.90/1.20 cnf(i_0_996, negated_conjecture, (e16!=elem_352)). % 3.90/1.20 cnf(i_0_591, plain, (s(X1)!=X1)). % 3.90/1.20 cnf(i_0_590, plain, (s(s(X1))!=X1)). % 3.90/1.20 cnf(i_0_589, plain, (s(s(s(X1)))!=X1)). % 3.90/1.20 cnf(i_0_588, plain, (s(s(s(s(X1))))!=X1)). % 3.90/1.20 cnf(i_0_587, plain, (s(s(s(s(s(X1)))))!=X1)). % 3.90/1.20 cnf(i_0_586, plain, (s(s(s(s(s(s(X1))))))!=X1)). % 3.90/1.20 cnf(i_0_585, plain, (s(s(s(s(s(s(s(X1)))))))!=X1)). % 3.90/1.20 cnf(i_0_584, plain, (s(s(s(s(s(s(s(s(X1))))))))!=X1)). % 3.90/1.20 cnf(i_0_583, plain, (s(s(s(s(s(s(s(s(s(X1)))))))))!=X1)). % 3.90/1.20 cnf(i_0_582, plain, (s(s(s(s(s(s(s(s(s(s(X1))))))))))!=X1)). % 3.90/1.20 cnf(i_0_581, plain, (s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))!=X1)). % 3.90/1.20 cnf(i_0_580, plain, (s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_579, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_578, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_577, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_576, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_575, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_574, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_573, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_572, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_571, plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_570, 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)). % 3.90/1.20 cnf(i_0_569, 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)). % 3.90/1.20 cnf(i_0_568, 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)). % 3.90/1.20 cnf(i_0_567, 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)). % 3.90/1.20 cnf(i_0_566, 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)). % 3.90/1.20 cnf(i_0_565, 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)). % 3.90/1.20 cnf(i_0_564, 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)). % 3.90/1.20 cnf(i_0_563, 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)). % 3.90/1.20 cnf(i_0_562, 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)). % 3.90/1.20 cnf(i_0_561, 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)). % 3.90/1.20 cnf(i_0_560, 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)). % 3.90/1.20 cnf(i_0_559, 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)). % 3.90/1.20 cnf(i_0_558, 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)). % 3.90/1.20 cnf(i_0_557, 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)). % 3.90/1.20 cnf(i_0_556, 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)). % 3.90/1.20 cnf(i_0_555, 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)). % 3.90/1.20 cnf(i_0_554, 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)). % 3.90/1.20 cnf(i_0_553, 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)). % 3.90/1.20 cnf(i_0_552, 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)). % 3.90/1.20 cnf(i_0_551, 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)). % 3.90/1.20 cnf(i_0_550, 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)). % 3.90/1.20 cnf(i_0_549, 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)). % 3.90/1.20 cnf(i_0_548, 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)). % 3.90/1.20 cnf(i_0_547, 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)). % 3.90/1.20 cnf(i_0_546, 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)). % 3.90/1.20 cnf(i_0_545, 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)). % 3.90/1.20 cnf(i_0_544, 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)). % 3.90/1.20 cnf(i_0_543, 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)). % 3.90/1.20 cnf(i_0_542, 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)). % 3.90/1.20 cnf(i_0_541, 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(s(X1)))))))))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_540, 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(s(s(X1))))))))))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_539, 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(s(s(s(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_538, 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(s(s(s(s(X1))))))))))))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_537, 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(s(s(s(s(s(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_536, 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(s(s(s(s(s(s(X1))))))))))))))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_535, 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(s(s(s(s(s(s(s(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_534, 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(s(s(s(s(s(s(s(s(X1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_533, 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(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_532, 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(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_531, 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(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_530, 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(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_529, 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(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_528, 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(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_527, 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(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_526, 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(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_525, 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(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_524, 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(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_523, 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(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_522, 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(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_521, 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(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_520, 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(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))!=X1)). % 3.90/1.20 cnf(i_0_519, 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(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)). % 3.90/1.20 cnf(i_0_518, 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(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)). % 3.90/1.20 cnf(i_0_517, 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(s(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)). % 3.90/1.20 cnf(i_0_516, 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(s(s(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)). % 3.90/1.20 cnf(i_0_515, 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(s(s(s(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)). % 3.90/1.20 cnf(i_0_514, 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(s(s(s(s(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)). % 3.90/1.20 cnf(i_0_513, 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(s(s(s(s(s(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)). % 3.90/1.20 cnf(i_0_512, 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(s(s(s(s(s(s(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)). % 3.90/1.20 cnf(i_0_511, 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(s(s(s(s(s(s(s(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)). % 3.90/1.20 cnf(i_0_510, 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(s(s(s(s(s(s(s(s(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)). % 3.90/1.20 cnf(i_0_500, plain, (select(store(X1,X2,X3),X4)=select(X1,X4)|X2=X4)). % 3.90/1.20 cnf(i_0_1002, plain, (X5=X5)). % 3.90/1.20 # End listing active clauses. There is an equivalent clause to each of these in the clausification! % 3.90/1.20 # Begin printing tableau % 3.90/1.20 # Found 6 steps % 3.90/1.20 cnf(i_0_945, hypothesis, (queue_1=q0), inference(start_rule)). % 3.90/1.20 cnf(i_0_1015, plain, (queue_1=q0), inference(extension_rule, [i_0_1010])). % 3.90/1.20 cnf(i_0_1538, plain, (queue_1!=q0), inference(closure_rule, [i_0_945])). % 3.90/1.20 cnf(i_0_1536, plain, (rstore_head(queue_1,queue_1)=rstore_head(q0,q0)), inference(extension_rule, [i_0_1005])). % 3.90/1.20 cnf(i_0_1554, plain, (rstore_head(queue_1,queue_1)=s(rstore_head(queue_1,queue_1))), inference(closure_rule, [i_0_591])). % 3.90/1.20 cnf(i_0_1556, plain, (rstore_head(q0,q0)!=s(rstore_head(queue_1,queue_1))), inference(etableau_closure_rule, [i_0_1556, ...])). % 3.90/1.20 # End printing tableau % 3.90/1.20 # SZS output end % 3.90/1.20 # Branches closed with saturation will be marked with an "s" % 3.90/1.22 # Child (27981) has found a proof. % 3.90/1.22 % 3.90/1.23 # Proof search is over... % 3.90/1.23 # Freeing feature tree %------------------------------------------------------------------------------