%------------------------------------------------------------------------------ % File : Etableau---0.67 % Problem : SWV498-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 : n014.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Wed Jul 20 18:21:27 EDT 2022 % Result : Satisfiable 0.19s 0.52s % Output : CNFRefutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SWV498-1.030 : TPTP v8.1.0. Released v4.0.0. % 0.10/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 : n014.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.34 % DateTime : Wed Jun 15 08:13:21 EDT 2022 % 0.12/0.34 % CPUTime : % 0.12/0.38 # No SInE strategy applied % 0.12/0.38 # Auto-Mode selected heuristic G_E___208_C18_F1_SE_CS_SP_PS_S5PRR_RG_S04AN % 0.12/0.38 # and selection function SelectComplexExceptUniqMaxHorn. % 0.12/0.38 # % 0.12/0.38 # Presaturation interreduction done % 0.12/0.38 # Number of axioms: 498 Number of unprocessed: 498 % 0.12/0.38 # Tableaux proof search. % 0.12/0.38 # APR header successfully linked. % 0.12/0.38 # Hello from C++ % 0.19/0.50 # The folding up rule is enabled... % 0.19/0.50 # Local unification is enabled... % 0.19/0.50 # Any saturation attempts will use folding labels... % 0.19/0.50 # 498 beginning clauses after preprocessing and clausification % 0.19/0.50 # Creating start rules for all 1 conjectures. % 0.19/0.50 # There are 1 start rule candidates: % 0.19/0.50 # Found 497 unit axioms. % 0.19/0.50 # 1 start rule tableaux created. % 0.19/0.50 # 1 extension rule candidate clauses % 0.19/0.50 # 497 unit axiom clauses % 0.19/0.50 % 0.19/0.50 # Requested 8, 32 cores available to the main process. % 0.19/0.50 # There are not enough tableaux to fork, creating more from the initial 1 % 0.19/0.50 # Creating equality axioms % 0.19/0.50 # Ran out of tableaux, making start rules for all clauses % 0.19/0.50 # Returning from population with 505 new_tableaux and 0 remaining starting tableaux. % 0.19/0.50 # We now have 505 tableaux to operate on % 0.19/0.52 # 21634 Satisfiable branch % 0.19/0.52 # Satisfiable branch found. % 0.19/0.52 # There were 1 total branch saturation attempts. % 0.19/0.52 # There were 0 of these attempts blocked. % 0.19/0.52 # There were 0 deferred branch saturation attempts. % 0.19/0.52 # There were 0 free duplicated saturations. % 0.19/0.52 # There were 0 total successful branch saturations. % 0.19/0.52 # There were 0 successful branch saturations in interreduction. % 0.19/0.52 # There were 0 successful branch saturations on the branch. % 0.19/0.52 # There were 0 successful branch saturations after the branch. % 0.19/0.52 # SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.52 # SZS output start for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.52 # Begin clausification derivation % 0.19/0.52 % 0.19/0.52 # End clausification derivation % 0.19/0.52 # Begin listing active clauses obtained from FOF to CNF conversion % 0.19/0.52 cnf(i_0_530, hypothesis, (store(a_1046,i1,e1)=a_1047)). % 0.19/0.52 cnf(i_0_560, hypothesis, (store(a_1076,i10,e10)=a_1077)). % 0.19/0.52 cnf(i_0_501, hypothesis, (store(a1,i1,e1)=a_1018)). % 0.19/0.52 cnf(i_0_502, hypothesis, (store(a_1018,i2,e2)=a_1019)). % 0.19/0.52 cnf(i_0_503, hypothesis, (store(a_1019,i3,e3)=a_1020)). % 0.19/0.52 cnf(i_0_504, hypothesis, (store(a_1020,i4,e4)=a_1021)). % 0.19/0.52 cnf(i_0_505, hypothesis, (store(a_1021,i5,e5)=a_1022)). % 0.19/0.52 cnf(i_0_506, hypothesis, (store(a_1022,i6,e6)=a_1023)). % 0.19/0.52 cnf(i_0_507, hypothesis, (store(a_1023,i7,e7)=a_1024)). % 0.19/0.52 cnf(i_0_508, hypothesis, (store(a_1024,i8,e8)=a_1025)). % 0.19/0.52 cnf(i_0_509, hypothesis, (store(a_1025,i9,e9)=a_1026)). % 0.19/0.52 cnf(i_0_510, hypothesis, (store(a_1026,i10,e10)=a_1027)). % 0.19/0.52 cnf(i_0_511, hypothesis, (store(a_1027,i11,e11)=a_1028)). % 0.19/0.52 cnf(i_0_512, hypothesis, (store(a_1028,i12,e12)=a_1029)). % 0.19/0.52 cnf(i_0_513, hypothesis, (store(a_1029,i13,e13)=a_1030)). % 0.19/0.52 cnf(i_0_514, hypothesis, (store(a_1030,i14,e14)=a_1031)). % 0.19/0.52 cnf(i_0_515, hypothesis, (store(a_1031,i15,e15)=a_1032)). % 0.19/0.52 cnf(i_0_516, hypothesis, (store(a_1032,i16,e16)=a_1033)). % 0.19/0.52 cnf(i_0_517, hypothesis, (store(a_1033,i17,e17)=a_1034)). % 0.19/0.52 cnf(i_0_518, hypothesis, (store(a_1034,i18,e18)=a_1035)). % 0.19/0.52 cnf(i_0_519, hypothesis, (store(a_1035,i19,e19)=a_1036)). % 0.19/0.52 cnf(i_0_520, hypothesis, (store(a_1036,i20,e20)=a_1037)). % 0.19/0.52 cnf(i_0_521, hypothesis, (store(a_1037,i21,e21)=a_1038)). % 0.19/0.52 cnf(i_0_522, hypothesis, (store(a_1038,i22,e22)=a_1039)). % 0.19/0.52 cnf(i_0_523, hypothesis, (store(a_1039,i23,e23)=a_1040)). % 0.19/0.52 cnf(i_0_524, hypothesis, (store(a_1040,i24,e24)=a_1041)). % 0.19/0.52 cnf(i_0_525, hypothesis, (store(a_1041,i25,e25)=a_1042)). % 0.19/0.52 cnf(i_0_526, hypothesis, (store(a_1042,i26,e26)=a_1043)). % 0.19/0.52 cnf(i_0_527, hypothesis, (store(a_1043,i27,e27)=a_1044)). % 0.19/0.52 cnf(i_0_528, hypothesis, (store(a_1044,i28,e28)=a_1045)). % 0.19/0.52 cnf(i_0_529, hypothesis, (store(a_1045,i29,e29)=a_1046)). % 0.19/0.52 cnf(i_0_531, hypothesis, (store(a1,i13,e13)=a_1048)). % 0.19/0.52 cnf(i_0_532, hypothesis, (store(a_1048,i1,e1)=a_1049)). % 0.19/0.52 cnf(i_0_533, hypothesis, (store(a_1049,i19,e19)=a_1050)). % 0.19/0.52 cnf(i_0_534, hypothesis, (store(a_1050,i4,e4)=a_1051)). % 0.19/0.52 cnf(i_0_535, hypothesis, (store(a_1051,i9,e9)=a_1052)). % 0.19/0.52 cnf(i_0_536, hypothesis, (store(a_1052,i30,e30)=a_1053)). % 0.19/0.52 cnf(i_0_537, hypothesis, (store(a_1053,i2,e2)=a_1054)). % 0.19/0.52 cnf(i_0_538, hypothesis, (store(a_1054,i15,e15)=a_1055)). % 0.19/0.52 cnf(i_0_539, hypothesis, (store(a_1055,i25,e25)=a_1056)). % 0.19/0.52 cnf(i_0_540, hypothesis, (store(a_1056,i18,e18)=a_1057)). % 0.19/0.52 cnf(i_0_541, hypothesis, (store(a_1057,i20,e20)=a_1058)). % 0.19/0.52 cnf(i_0_542, hypothesis, (store(a_1058,i8,e8)=a_1059)). % 0.19/0.52 cnf(i_0_543, hypothesis, (store(a_1059,i21,e21)=a_1060)). % 0.19/0.52 cnf(i_0_544, hypothesis, (store(a_1060,i6,e6)=a_1061)). % 0.19/0.52 cnf(i_0_545, hypothesis, (store(a_1061,i11,e11)=a_1062)). % 0.19/0.52 cnf(i_0_546, hypothesis, (store(a_1062,i14,e14)=a_1063)). % 0.19/0.52 cnf(i_0_547, hypothesis, (store(a_1063,i29,e29)=a_1064)). % 0.19/0.52 cnf(i_0_548, hypothesis, (store(a_1064,i5,e5)=a_1065)). % 0.19/0.52 cnf(i_0_549, hypothesis, (store(a_1065,i26,e26)=a_1066)). % 0.19/0.52 cnf(i_0_550, hypothesis, (store(a_1066,i22,e22)=a_1067)). % 0.19/0.52 cnf(i_0_551, hypothesis, (store(a_1067,i27,e27)=a_1068)). % 0.19/0.52 cnf(i_0_552, hypothesis, (store(a_1068,i3,e3)=a_1069)). % 0.19/0.52 cnf(i_0_553, hypothesis, (store(a_1069,i12,e12)=a_1070)). % 0.19/0.52 cnf(i_0_554, hypothesis, (store(a_1070,i16,e16)=a_1071)). % 0.19/0.52 cnf(i_0_555, hypothesis, (store(a_1071,i28,e28)=a_1072)). % 0.19/0.52 cnf(i_0_556, hypothesis, (store(a_1072,i17,e17)=a_1073)). % 0.19/0.52 cnf(i_0_557, hypothesis, (store(a_1073,i23,e23)=a_1074)). % 0.19/0.52 cnf(i_0_558, hypothesis, (store(a_1074,i24,e24)=a_1075)). % 0.19/0.52 cnf(i_0_559, hypothesis, (store(a_1075,i7,e7)=a_1076)). % 0.19/0.52 cnf(i_0_499, plain, (select(store(X1,X2,X3),X2)=X3)). % 0.19/0.52 cnf(i_0_996, negated_conjecture, (a_1077!=a_1047)). % 0.19/0.52 cnf(i_0_995, hypothesis, (i2!=i1)). % 0.19/0.52 cnf(i_0_994, hypothesis, (i3!=i1)). % 0.19/0.52 cnf(i_0_966, hypothesis, (i3!=i2)). % 0.19/0.52 cnf(i_0_993, hypothesis, (i4!=i1)). % 0.19/0.52 cnf(i_0_965, hypothesis, (i4!=i2)). % 0.19/0.52 cnf(i_0_938, hypothesis, (i4!=i3)). % 0.19/0.52 cnf(i_0_992, hypothesis, (i5!=i1)). % 0.19/0.52 cnf(i_0_964, hypothesis, (i5!=i2)). % 0.19/0.52 cnf(i_0_937, hypothesis, (i5!=i3)). % 0.19/0.52 cnf(i_0_911, hypothesis, (i5!=i4)). % 0.19/0.52 cnf(i_0_991, hypothesis, (i6!=i1)). % 0.19/0.52 cnf(i_0_963, hypothesis, (i6!=i2)). % 0.19/0.52 cnf(i_0_936, hypothesis, (i6!=i3)). % 0.19/0.52 cnf(i_0_910, hypothesis, (i6!=i4)). % 0.19/0.52 cnf(i_0_885, hypothesis, (i6!=i5)). % 0.19/0.52 cnf(i_0_990, hypothesis, (i7!=i1)). % 0.19/0.52 cnf(i_0_962, hypothesis, (i7!=i2)). % 0.19/0.52 cnf(i_0_935, hypothesis, (i7!=i3)). % 0.19/0.52 cnf(i_0_909, hypothesis, (i7!=i4)). % 0.19/0.52 cnf(i_0_884, hypothesis, (i7!=i5)). % 0.19/0.52 cnf(i_0_860, hypothesis, (i7!=i6)). % 0.19/0.52 cnf(i_0_989, hypothesis, (i8!=i1)). % 0.19/0.52 cnf(i_0_961, hypothesis, (i8!=i2)). % 0.19/0.52 cnf(i_0_934, hypothesis, (i8!=i3)). % 0.19/0.52 cnf(i_0_908, hypothesis, (i8!=i4)). % 0.19/0.52 cnf(i_0_883, hypothesis, (i8!=i5)). % 0.19/0.52 cnf(i_0_859, hypothesis, (i8!=i6)). % 0.19/0.52 cnf(i_0_836, hypothesis, (i8!=i7)). % 0.19/0.52 cnf(i_0_988, hypothesis, (i9!=i1)). % 0.19/0.52 cnf(i_0_960, hypothesis, (i9!=i2)). % 0.19/0.52 cnf(i_0_933, hypothesis, (i9!=i3)). % 0.19/0.52 cnf(i_0_907, hypothesis, (i9!=i4)). % 0.19/0.52 cnf(i_0_882, hypothesis, (i9!=i5)). % 0.19/0.52 cnf(i_0_858, hypothesis, (i9!=i6)). % 0.19/0.52 cnf(i_0_835, hypothesis, (i9!=i7)). % 0.19/0.52 cnf(i_0_813, hypothesis, (i9!=i8)). % 0.19/0.52 cnf(i_0_987, hypothesis, (i10!=i1)). % 0.19/0.52 cnf(i_0_959, hypothesis, (i10!=i2)). % 0.19/0.52 cnf(i_0_932, hypothesis, (i10!=i3)). % 0.19/0.52 cnf(i_0_906, hypothesis, (i10!=i4)). % 0.19/0.52 cnf(i_0_881, hypothesis, (i10!=i5)). % 0.19/0.52 cnf(i_0_857, hypothesis, (i10!=i6)). % 0.19/0.52 cnf(i_0_834, hypothesis, (i10!=i7)). % 0.19/0.52 cnf(i_0_812, hypothesis, (i10!=i8)). % 0.19/0.52 cnf(i_0_791, hypothesis, (i10!=i9)). % 0.19/0.52 cnf(i_0_986, hypothesis, (i11!=i1)). % 0.19/0.52 cnf(i_0_958, hypothesis, (i11!=i2)). % 0.19/0.52 cnf(i_0_931, hypothesis, (i11!=i3)). % 0.19/0.52 cnf(i_0_905, hypothesis, (i11!=i4)). % 0.19/0.52 cnf(i_0_880, hypothesis, (i11!=i5)). % 0.19/0.52 cnf(i_0_856, hypothesis, (i11!=i6)). % 0.19/0.52 cnf(i_0_833, hypothesis, (i11!=i7)). % 0.19/0.52 cnf(i_0_811, hypothesis, (i11!=i8)). % 0.19/0.52 cnf(i_0_790, hypothesis, (i11!=i9)). % 0.19/0.52 cnf(i_0_770, hypothesis, (i11!=i10)). % 0.19/0.52 cnf(i_0_985, hypothesis, (i12!=i1)). % 0.19/0.52 cnf(i_0_957, hypothesis, (i12!=i2)). % 0.19/0.52 cnf(i_0_930, hypothesis, (i12!=i3)). % 0.19/0.52 cnf(i_0_904, hypothesis, (i12!=i4)). % 0.19/0.52 cnf(i_0_879, hypothesis, (i12!=i5)). % 0.19/0.52 cnf(i_0_855, hypothesis, (i12!=i6)). % 0.19/0.52 cnf(i_0_832, hypothesis, (i12!=i7)). % 0.19/0.52 cnf(i_0_810, hypothesis, (i12!=i8)). % 0.19/0.52 cnf(i_0_789, hypothesis, (i12!=i9)). % 0.19/0.52 cnf(i_0_769, hypothesis, (i12!=i10)). % 0.19/0.52 cnf(i_0_750, hypothesis, (i12!=i11)). % 0.19/0.52 cnf(i_0_984, hypothesis, (i13!=i1)). % 0.19/0.52 cnf(i_0_956, hypothesis, (i13!=i2)). % 0.19/0.52 cnf(i_0_929, hypothesis, (i13!=i3)). % 0.19/0.52 cnf(i_0_903, hypothesis, (i13!=i4)). % 0.19/0.52 cnf(i_0_878, hypothesis, (i13!=i5)). % 0.19/0.52 cnf(i_0_854, hypothesis, (i13!=i6)). % 0.19/0.52 cnf(i_0_831, hypothesis, (i13!=i7)). % 0.19/0.52 cnf(i_0_809, hypothesis, (i13!=i8)). % 0.19/0.52 cnf(i_0_788, hypothesis, (i13!=i9)). % 0.19/0.52 cnf(i_0_768, hypothesis, (i13!=i10)). % 0.19/0.52 cnf(i_0_749, hypothesis, (i13!=i11)). % 0.19/0.52 cnf(i_0_731, hypothesis, (i13!=i12)). % 0.19/0.52 cnf(i_0_983, hypothesis, (i14!=i1)). % 0.19/0.52 cnf(i_0_955, hypothesis, (i14!=i2)). % 0.19/0.52 cnf(i_0_928, hypothesis, (i14!=i3)). % 0.19/0.52 cnf(i_0_902, hypothesis, (i14!=i4)). % 0.19/0.52 cnf(i_0_877, hypothesis, (i14!=i5)). % 0.19/0.52 cnf(i_0_853, hypothesis, (i14!=i6)). % 0.19/0.52 cnf(i_0_830, hypothesis, (i14!=i7)). % 0.19/0.52 cnf(i_0_808, hypothesis, (i14!=i8)). % 0.19/0.52 cnf(i_0_787, hypothesis, (i14!=i9)). % 0.19/0.52 cnf(i_0_767, hypothesis, (i14!=i10)). % 0.19/0.52 cnf(i_0_748, hypothesis, (i14!=i11)). % 0.19/0.52 cnf(i_0_730, hypothesis, (i14!=i12)). % 0.19/0.52 cnf(i_0_713, hypothesis, (i14!=i13)). % 0.19/0.52 cnf(i_0_982, hypothesis, (i15!=i1)). % 0.19/0.52 cnf(i_0_954, hypothesis, (i15!=i2)). % 0.19/0.52 cnf(i_0_927, hypothesis, (i15!=i3)). % 0.19/0.52 cnf(i_0_901, hypothesis, (i15!=i4)). % 0.19/0.52 cnf(i_0_876, hypothesis, (i15!=i5)). % 0.19/0.52 cnf(i_0_852, hypothesis, (i15!=i6)). % 0.19/0.52 cnf(i_0_829, hypothesis, (i15!=i7)). % 0.19/0.52 cnf(i_0_807, hypothesis, (i15!=i8)). % 0.19/0.52 cnf(i_0_786, hypothesis, (i15!=i9)). % 0.19/0.52 cnf(i_0_766, hypothesis, (i15!=i10)). % 0.19/0.52 cnf(i_0_747, hypothesis, (i15!=i11)). % 0.19/0.52 cnf(i_0_729, hypothesis, (i15!=i12)). % 0.19/0.52 cnf(i_0_712, hypothesis, (i15!=i13)). % 0.19/0.52 cnf(i_0_696, hypothesis, (i15!=i14)). % 0.19/0.52 cnf(i_0_981, hypothesis, (i16!=i1)). % 0.19/0.52 cnf(i_0_953, hypothesis, (i16!=i2)). % 0.19/0.52 cnf(i_0_926, hypothesis, (i16!=i3)). % 0.19/0.52 cnf(i_0_900, hypothesis, (i16!=i4)). % 0.19/0.52 cnf(i_0_875, hypothesis, (i16!=i5)). % 0.19/0.52 cnf(i_0_851, hypothesis, (i16!=i6)). % 0.19/0.52 cnf(i_0_828, hypothesis, (i16!=i7)). % 0.19/0.52 cnf(i_0_806, hypothesis, (i16!=i8)). % 0.19/0.52 cnf(i_0_785, hypothesis, (i16!=i9)). % 0.19/0.52 cnf(i_0_765, hypothesis, (i16!=i10)). % 0.19/0.52 cnf(i_0_746, hypothesis, (i16!=i11)). % 0.19/0.52 cnf(i_0_728, hypothesis, (i16!=i12)). % 0.19/0.52 cnf(i_0_711, hypothesis, (i16!=i13)). % 0.19/0.52 cnf(i_0_695, hypothesis, (i16!=i14)). % 0.19/0.52 cnf(i_0_680, hypothesis, (i16!=i15)). % 0.19/0.52 cnf(i_0_980, hypothesis, (i17!=i1)). % 0.19/0.52 cnf(i_0_952, hypothesis, (i17!=i2)). % 0.19/0.52 cnf(i_0_925, hypothesis, (i17!=i3)). % 0.19/0.52 cnf(i_0_899, hypothesis, (i17!=i4)). % 0.19/0.52 cnf(i_0_874, hypothesis, (i17!=i5)). % 0.19/0.52 cnf(i_0_850, hypothesis, (i17!=i6)). % 0.19/0.52 cnf(i_0_827, hypothesis, (i17!=i7)). % 0.19/0.52 cnf(i_0_805, hypothesis, (i17!=i8)). % 0.19/0.52 cnf(i_0_784, hypothesis, (i17!=i9)). % 0.19/0.52 cnf(i_0_764, hypothesis, (i17!=i10)). % 0.19/0.52 cnf(i_0_745, hypothesis, (i17!=i11)). % 0.19/0.52 cnf(i_0_727, hypothesis, (i17!=i12)). % 0.19/0.52 cnf(i_0_710, hypothesis, (i17!=i13)). % 0.19/0.52 cnf(i_0_694, hypothesis, (i17!=i14)). % 0.19/0.52 cnf(i_0_679, hypothesis, (i17!=i15)). % 0.19/0.52 cnf(i_0_665, hypothesis, (i17!=i16)). % 0.19/0.52 cnf(i_0_979, hypothesis, (i18!=i1)). % 0.19/0.52 cnf(i_0_951, hypothesis, (i18!=i2)). % 0.19/0.52 cnf(i_0_924, hypothesis, (i18!=i3)). % 0.19/0.52 cnf(i_0_898, hypothesis, (i18!=i4)). % 0.19/0.52 cnf(i_0_873, hypothesis, (i18!=i5)). % 0.19/0.52 cnf(i_0_849, hypothesis, (i18!=i6)). % 0.19/0.52 cnf(i_0_826, hypothesis, (i18!=i7)). % 0.19/0.52 cnf(i_0_804, hypothesis, (i18!=i8)). % 0.19/0.52 cnf(i_0_783, hypothesis, (i18!=i9)). % 0.19/0.52 cnf(i_0_763, hypothesis, (i18!=i10)). % 0.19/0.52 cnf(i_0_744, hypothesis, (i18!=i11)). % 0.19/0.52 cnf(i_0_726, hypothesis, (i18!=i12)). % 0.19/0.52 cnf(i_0_709, hypothesis, (i18!=i13)). % 0.19/0.52 cnf(i_0_693, hypothesis, (i18!=i14)). % 0.19/0.52 cnf(i_0_678, hypothesis, (i18!=i15)). % 0.19/0.52 cnf(i_0_664, hypothesis, (i18!=i16)). % 0.19/0.52 cnf(i_0_651, hypothesis, (i18!=i17)). % 0.19/0.52 cnf(i_0_978, hypothesis, (i19!=i1)). % 0.19/0.52 cnf(i_0_950, hypothesis, (i19!=i2)). % 0.19/0.52 cnf(i_0_923, hypothesis, (i19!=i3)). % 0.19/0.52 cnf(i_0_897, hypothesis, (i19!=i4)). % 0.19/0.52 cnf(i_0_872, hypothesis, (i19!=i5)). % 0.19/0.52 cnf(i_0_848, hypothesis, (i19!=i6)). % 0.19/0.52 cnf(i_0_825, hypothesis, (i19!=i7)). % 0.19/0.52 cnf(i_0_803, hypothesis, (i19!=i8)). % 0.19/0.52 cnf(i_0_782, hypothesis, (i19!=i9)). % 0.19/0.52 cnf(i_0_762, hypothesis, (i19!=i10)). % 0.19/0.52 cnf(i_0_743, hypothesis, (i19!=i11)). % 0.19/0.52 cnf(i_0_725, hypothesis, (i19!=i12)). % 0.19/0.52 cnf(i_0_708, hypothesis, (i19!=i13)). % 0.19/0.52 cnf(i_0_692, hypothesis, (i19!=i14)). % 0.19/0.52 cnf(i_0_677, hypothesis, (i19!=i15)). % 0.19/0.52 cnf(i_0_663, hypothesis, (i19!=i16)). % 0.19/0.52 cnf(i_0_650, hypothesis, (i19!=i17)). % 0.19/0.52 cnf(i_0_638, hypothesis, (i19!=i18)). % 0.19/0.52 cnf(i_0_977, hypothesis, (i20!=i1)). % 0.19/0.52 cnf(i_0_949, hypothesis, (i20!=i2)). % 0.19/0.52 cnf(i_0_922, hypothesis, (i20!=i3)). % 0.19/0.52 cnf(i_0_896, hypothesis, (i20!=i4)). % 0.19/0.52 cnf(i_0_871, hypothesis, (i20!=i5)). % 0.19/0.52 cnf(i_0_847, hypothesis, (i20!=i6)). % 0.19/0.52 cnf(i_0_824, hypothesis, (i20!=i7)). % 0.19/0.52 cnf(i_0_802, hypothesis, (i20!=i8)). % 0.19/0.52 cnf(i_0_781, hypothesis, (i20!=i9)). % 0.19/0.52 cnf(i_0_761, hypothesis, (i20!=i10)). % 0.19/0.52 cnf(i_0_742, hypothesis, (i20!=i11)). % 0.19/0.52 cnf(i_0_724, hypothesis, (i20!=i12)). % 0.19/0.52 cnf(i_0_707, hypothesis, (i20!=i13)). % 0.19/0.52 cnf(i_0_691, hypothesis, (i20!=i14)). % 0.19/0.52 cnf(i_0_676, hypothesis, (i20!=i15)). % 0.19/0.52 cnf(i_0_662, hypothesis, (i20!=i16)). % 0.19/0.52 cnf(i_0_649, hypothesis, (i20!=i17)). % 0.19/0.52 cnf(i_0_637, hypothesis, (i20!=i18)). % 0.19/0.52 cnf(i_0_626, hypothesis, (i20!=i19)). % 0.19/0.52 cnf(i_0_976, hypothesis, (i21!=i1)). % 0.19/0.52 cnf(i_0_948, hypothesis, (i21!=i2)). % 0.19/0.52 cnf(i_0_921, hypothesis, (i21!=i3)). % 0.19/0.52 cnf(i_0_895, hypothesis, (i21!=i4)). % 0.19/0.52 cnf(i_0_870, hypothesis, (i21!=i5)). % 0.19/0.52 cnf(i_0_846, hypothesis, (i21!=i6)). % 0.19/0.52 cnf(i_0_823, hypothesis, (i21!=i7)). % 0.19/0.52 cnf(i_0_801, hypothesis, (i21!=i8)). % 0.19/0.52 cnf(i_0_780, hypothesis, (i21!=i9)). % 0.19/0.52 cnf(i_0_760, hypothesis, (i21!=i10)). % 0.19/0.52 cnf(i_0_741, hypothesis, (i21!=i11)). % 0.19/0.52 cnf(i_0_723, hypothesis, (i21!=i12)). % 0.19/0.52 cnf(i_0_706, hypothesis, (i21!=i13)). % 0.19/0.52 cnf(i_0_690, hypothesis, (i21!=i14)). % 0.19/0.52 cnf(i_0_675, hypothesis, (i21!=i15)). % 0.19/0.52 cnf(i_0_661, hypothesis, (i21!=i16)). % 0.19/0.52 cnf(i_0_648, hypothesis, (i21!=i17)). % 0.19/0.52 cnf(i_0_636, hypothesis, (i21!=i18)). % 0.19/0.52 cnf(i_0_625, hypothesis, (i21!=i19)). % 0.19/0.52 cnf(i_0_615, hypothesis, (i21!=i20)). % 0.19/0.52 cnf(i_0_975, hypothesis, (i22!=i1)). % 0.19/0.52 cnf(i_0_947, hypothesis, (i22!=i2)). % 0.19/0.52 cnf(i_0_920, hypothesis, (i22!=i3)). % 0.19/0.52 cnf(i_0_894, hypothesis, (i22!=i4)). % 0.19/0.52 cnf(i_0_869, hypothesis, (i22!=i5)). % 0.19/0.52 cnf(i_0_845, hypothesis, (i22!=i6)). % 0.19/0.52 cnf(i_0_822, hypothesis, (i22!=i7)). % 0.19/0.52 cnf(i_0_800, hypothesis, (i22!=i8)). % 0.19/0.52 cnf(i_0_779, hypothesis, (i22!=i9)). % 0.19/0.52 cnf(i_0_759, hypothesis, (i22!=i10)). % 0.19/0.52 cnf(i_0_740, hypothesis, (i22!=i11)). % 0.19/0.52 cnf(i_0_722, hypothesis, (i22!=i12)). % 0.19/0.52 cnf(i_0_705, hypothesis, (i22!=i13)). % 0.19/0.52 cnf(i_0_689, hypothesis, (i22!=i14)). % 0.19/0.52 cnf(i_0_674, hypothesis, (i22!=i15)). % 0.19/0.52 cnf(i_0_660, hypothesis, (i22!=i16)). % 0.19/0.52 cnf(i_0_647, hypothesis, (i22!=i17)). % 0.19/0.52 cnf(i_0_635, hypothesis, (i22!=i18)). % 0.19/0.52 cnf(i_0_624, hypothesis, (i22!=i19)). % 0.19/0.52 cnf(i_0_614, hypothesis, (i22!=i20)). % 0.19/0.52 cnf(i_0_605, hypothesis, (i22!=i21)). % 0.19/0.52 cnf(i_0_974, hypothesis, (i23!=i1)). % 0.19/0.52 cnf(i_0_946, hypothesis, (i23!=i2)). % 0.19/0.52 cnf(i_0_919, hypothesis, (i23!=i3)). % 0.19/0.52 cnf(i_0_893, hypothesis, (i23!=i4)). % 0.19/0.52 cnf(i_0_868, hypothesis, (i23!=i5)). % 0.19/0.52 cnf(i_0_844, hypothesis, (i23!=i6)). % 0.19/0.52 cnf(i_0_821, hypothesis, (i23!=i7)). % 0.19/0.52 cnf(i_0_799, hypothesis, (i23!=i8)). % 0.19/0.52 cnf(i_0_778, hypothesis, (i23!=i9)). % 0.19/0.52 cnf(i_0_758, hypothesis, (i23!=i10)). % 0.19/0.52 cnf(i_0_739, hypothesis, (i23!=i11)). % 0.19/0.52 cnf(i_0_721, hypothesis, (i23!=i12)). % 0.19/0.52 cnf(i_0_704, hypothesis, (i23!=i13)). % 0.19/0.52 cnf(i_0_688, hypothesis, (i23!=i14)). % 0.19/0.52 cnf(i_0_673, hypothesis, (i23!=i15)). % 0.19/0.52 cnf(i_0_659, hypothesis, (i23!=i16)). % 0.19/0.52 cnf(i_0_646, hypothesis, (i23!=i17)). % 0.19/0.52 cnf(i_0_634, hypothesis, (i23!=i18)). % 0.19/0.52 cnf(i_0_623, hypothesis, (i23!=i19)). % 0.19/0.52 cnf(i_0_613, hypothesis, (i23!=i20)). % 0.19/0.52 cnf(i_0_604, hypothesis, (i23!=i21)). % 0.19/0.52 cnf(i_0_596, hypothesis, (i23!=i22)). % 0.19/0.52 cnf(i_0_973, hypothesis, (i24!=i1)). % 0.19/0.52 cnf(i_0_945, hypothesis, (i24!=i2)). % 0.19/0.52 cnf(i_0_918, hypothesis, (i24!=i3)). % 0.19/0.52 cnf(i_0_892, hypothesis, (i24!=i4)). % 0.19/0.52 cnf(i_0_867, hypothesis, (i24!=i5)). % 0.19/0.52 cnf(i_0_843, hypothesis, (i24!=i6)). % 0.19/0.52 cnf(i_0_820, hypothesis, (i24!=i7)). % 0.19/0.52 cnf(i_0_798, hypothesis, (i24!=i8)). % 0.19/0.52 cnf(i_0_777, hypothesis, (i24!=i9)). % 0.19/0.52 cnf(i_0_757, hypothesis, (i24!=i10)). % 0.19/0.52 cnf(i_0_738, hypothesis, (i24!=i11)). % 0.19/0.52 cnf(i_0_720, hypothesis, (i24!=i12)). % 0.19/0.52 cnf(i_0_703, hypothesis, (i24!=i13)). % 0.19/0.52 cnf(i_0_687, hypothesis, (i24!=i14)). % 0.19/0.52 cnf(i_0_672, hypothesis, (i24!=i15)). % 0.19/0.52 cnf(i_0_658, hypothesis, (i24!=i16)). % 0.19/0.52 cnf(i_0_645, hypothesis, (i24!=i17)). % 0.19/0.52 cnf(i_0_633, hypothesis, (i24!=i18)). % 0.19/0.52 cnf(i_0_622, hypothesis, (i24!=i19)). % 0.19/0.52 cnf(i_0_612, hypothesis, (i24!=i20)). % 0.19/0.52 cnf(i_0_603, hypothesis, (i24!=i21)). % 0.19/0.52 cnf(i_0_595, hypothesis, (i24!=i22)). % 0.19/0.52 cnf(i_0_588, hypothesis, (i24!=i23)). % 0.19/0.52 cnf(i_0_972, hypothesis, (i25!=i1)). % 0.19/0.52 cnf(i_0_944, hypothesis, (i25!=i2)). % 0.19/0.52 cnf(i_0_917, hypothesis, (i25!=i3)). % 0.19/0.52 cnf(i_0_891, hypothesis, (i25!=i4)). % 0.19/0.52 cnf(i_0_866, hypothesis, (i25!=i5)). % 0.19/0.52 cnf(i_0_842, hypothesis, (i25!=i6)). % 0.19/0.52 cnf(i_0_819, hypothesis, (i25!=i7)). % 0.19/0.52 cnf(i_0_797, hypothesis, (i25!=i8)). % 0.19/0.52 cnf(i_0_776, hypothesis, (i25!=i9)). % 0.19/0.52 cnf(i_0_756, hypothesis, (i25!=i10)). % 0.19/0.52 cnf(i_0_737, hypothesis, (i25!=i11)). % 0.19/0.52 cnf(i_0_719, hypothesis, (i25!=i12)). % 0.19/0.52 cnf(i_0_702, hypothesis, (i25!=i13)). % 0.19/0.52 cnf(i_0_686, hypothesis, (i25!=i14)). % 0.19/0.52 cnf(i_0_671, hypothesis, (i25!=i15)). % 0.19/0.52 cnf(i_0_657, hypothesis, (i25!=i16)). % 0.19/0.52 cnf(i_0_644, hypothesis, (i25!=i17)). % 0.19/0.52 cnf(i_0_632, hypothesis, (i25!=i18)). % 0.19/0.52 cnf(i_0_621, hypothesis, (i25!=i19)). % 0.19/0.52 cnf(i_0_611, hypothesis, (i25!=i20)). % 0.19/0.52 cnf(i_0_602, hypothesis, (i25!=i21)). % 0.19/0.52 cnf(i_0_594, hypothesis, (i25!=i22)). % 0.19/0.52 cnf(i_0_587, hypothesis, (i25!=i23)). % 0.19/0.52 cnf(i_0_581, hypothesis, (i25!=i24)). % 0.19/0.52 cnf(i_0_971, hypothesis, (i26!=i1)). % 0.19/0.52 cnf(i_0_943, hypothesis, (i26!=i2)). % 0.19/0.52 cnf(i_0_916, hypothesis, (i26!=i3)). % 0.19/0.52 cnf(i_0_890, hypothesis, (i26!=i4)). % 0.19/0.52 cnf(i_0_865, hypothesis, (i26!=i5)). % 0.19/0.52 cnf(i_0_841, hypothesis, (i26!=i6)). % 0.19/0.52 cnf(i_0_818, hypothesis, (i26!=i7)). % 0.19/0.52 cnf(i_0_796, hypothesis, (i26!=i8)). % 0.19/0.52 cnf(i_0_775, hypothesis, (i26!=i9)). % 0.19/0.52 cnf(i_0_755, hypothesis, (i26!=i10)). % 0.19/0.52 cnf(i_0_736, hypothesis, (i26!=i11)). % 0.19/0.52 cnf(i_0_718, hypothesis, (i26!=i12)). % 0.19/0.52 cnf(i_0_701, hypothesis, (i26!=i13)). % 0.19/0.52 cnf(i_0_685, hypothesis, (i26!=i14)). % 0.19/0.52 cnf(i_0_670, hypothesis, (i26!=i15)). % 0.19/0.52 cnf(i_0_656, hypothesis, (i26!=i16)). % 0.19/0.52 cnf(i_0_643, hypothesis, (i26!=i17)). % 0.19/0.52 cnf(i_0_631, hypothesis, (i26!=i18)). % 0.19/0.52 cnf(i_0_620, hypothesis, (i26!=i19)). % 0.19/0.52 cnf(i_0_610, hypothesis, (i26!=i20)). % 0.19/0.52 cnf(i_0_601, hypothesis, (i26!=i21)). % 0.19/0.52 cnf(i_0_593, hypothesis, (i26!=i22)). % 0.19/0.52 cnf(i_0_586, hypothesis, (i26!=i23)). % 0.19/0.52 cnf(i_0_580, hypothesis, (i26!=i24)). % 0.19/0.52 cnf(i_0_575, hypothesis, (i26!=i25)). % 0.19/0.52 cnf(i_0_970, hypothesis, (i27!=i1)). % 0.19/0.52 cnf(i_0_942, hypothesis, (i27!=i2)). % 0.19/0.52 cnf(i_0_915, hypothesis, (i27!=i3)). % 0.19/0.52 cnf(i_0_889, hypothesis, (i27!=i4)). % 0.19/0.52 cnf(i_0_864, hypothesis, (i27!=i5)). % 0.19/0.52 cnf(i_0_840, hypothesis, (i27!=i6)). % 0.19/0.52 cnf(i_0_817, hypothesis, (i27!=i7)). % 0.19/0.52 cnf(i_0_795, hypothesis, (i27!=i8)). % 0.19/0.52 cnf(i_0_774, hypothesis, (i27!=i9)). % 0.19/0.52 cnf(i_0_754, hypothesis, (i27!=i10)). % 0.19/0.52 cnf(i_0_735, hypothesis, (i27!=i11)). % 0.19/0.52 cnf(i_0_717, hypothesis, (i27!=i12)). % 0.19/0.52 cnf(i_0_700, hypothesis, (i27!=i13)). % 0.19/0.52 cnf(i_0_684, hypothesis, (i27!=i14)). % 0.19/0.52 cnf(i_0_669, hypothesis, (i27!=i15)). % 0.19/0.52 cnf(i_0_655, hypothesis, (i27!=i16)). % 0.19/0.52 cnf(i_0_642, hypothesis, (i27!=i17)). % 0.19/0.52 cnf(i_0_630, hypothesis, (i27!=i18)). % 0.19/0.52 cnf(i_0_619, hypothesis, (i27!=i19)). % 0.19/0.52 cnf(i_0_609, hypothesis, (i27!=i20)). % 0.19/0.52 cnf(i_0_600, hypothesis, (i27!=i21)). % 0.19/0.52 cnf(i_0_592, hypothesis, (i27!=i22)). % 0.19/0.52 cnf(i_0_585, hypothesis, (i27!=i23)). % 0.19/0.52 cnf(i_0_579, hypothesis, (i27!=i24)). % 0.19/0.52 cnf(i_0_574, hypothesis, (i27!=i25)). % 0.19/0.52 cnf(i_0_570, hypothesis, (i27!=i26)). % 0.19/0.52 cnf(i_0_969, hypothesis, (i28!=i1)). % 0.19/0.52 cnf(i_0_941, hypothesis, (i28!=i2)). % 0.19/0.52 cnf(i_0_914, hypothesis, (i28!=i3)). % 0.19/0.52 cnf(i_0_888, hypothesis, (i28!=i4)). % 0.19/0.52 cnf(i_0_863, hypothesis, (i28!=i5)). % 0.19/0.52 cnf(i_0_839, hypothesis, (i28!=i6)). % 0.19/0.52 cnf(i_0_816, hypothesis, (i28!=i7)). % 0.19/0.52 cnf(i_0_794, hypothesis, (i28!=i8)). % 0.19/0.52 cnf(i_0_773, hypothesis, (i28!=i9)). % 0.19/0.52 cnf(i_0_753, hypothesis, (i28!=i10)). % 0.19/0.52 cnf(i_0_734, hypothesis, (i28!=i11)). % 0.19/0.52 cnf(i_0_716, hypothesis, (i28!=i12)). % 0.19/0.52 cnf(i_0_699, hypothesis, (i28!=i13)). % 0.19/0.52 cnf(i_0_683, hypothesis, (i28!=i14)). % 0.19/0.52 cnf(i_0_668, hypothesis, (i28!=i15)). % 0.19/0.52 cnf(i_0_654, hypothesis, (i28!=i16)). % 0.19/0.52 cnf(i_0_641, hypothesis, (i28!=i17)). % 0.19/0.52 cnf(i_0_629, hypothesis, (i28!=i18)). % 0.19/0.52 cnf(i_0_618, hypothesis, (i28!=i19)). % 0.19/0.52 cnf(i_0_608, hypothesis, (i28!=i20)). % 0.19/0.52 cnf(i_0_599, hypothesis, (i28!=i21)). % 0.19/0.52 cnf(i_0_591, hypothesis, (i28!=i22)). % 0.19/0.52 cnf(i_0_584, hypothesis, (i28!=i23)). % 0.19/0.52 cnf(i_0_578, hypothesis, (i28!=i24)). % 0.19/0.52 cnf(i_0_573, hypothesis, (i28!=i25)). % 0.19/0.52 cnf(i_0_569, hypothesis, (i28!=i26)). % 0.19/0.52 cnf(i_0_566, hypothesis, (i28!=i27)). % 0.19/0.52 cnf(i_0_968, hypothesis, (i29!=i1)). % 0.19/0.52 cnf(i_0_940, hypothesis, (i29!=i2)). % 0.19/0.52 cnf(i_0_913, hypothesis, (i29!=i3)). % 0.19/0.52 cnf(i_0_887, hypothesis, (i29!=i4)). % 0.19/0.52 cnf(i_0_862, hypothesis, (i29!=i5)). % 0.19/0.52 cnf(i_0_838, hypothesis, (i29!=i6)). % 0.19/0.52 cnf(i_0_815, hypothesis, (i29!=i7)). % 0.19/0.52 cnf(i_0_793, hypothesis, (i29!=i8)). % 0.19/0.52 cnf(i_0_772, hypothesis, (i29!=i9)). % 0.19/0.52 cnf(i_0_752, hypothesis, (i29!=i10)). % 0.19/0.52 cnf(i_0_733, hypothesis, (i29!=i11)). % 0.19/0.52 cnf(i_0_715, hypothesis, (i29!=i12)). % 0.19/0.52 cnf(i_0_698, hypothesis, (i29!=i13)). % 0.19/0.52 cnf(i_0_682, hypothesis, (i29!=i14)). % 0.19/0.52 cnf(i_0_667, hypothesis, (i29!=i15)). % 0.19/0.52 cnf(i_0_653, hypothesis, (i29!=i16)). % 0.19/0.52 cnf(i_0_640, hypothesis, (i29!=i17)). % 0.19/0.52 cnf(i_0_628, hypothesis, (i29!=i18)). % 0.19/0.52 cnf(i_0_617, hypothesis, (i29!=i19)). % 0.19/0.52 cnf(i_0_607, hypothesis, (i29!=i20)). % 0.19/0.52 cnf(i_0_598, hypothesis, (i29!=i21)). % 0.19/0.52 cnf(i_0_590, hypothesis, (i29!=i22)). % 0.19/0.52 cnf(i_0_583, hypothesis, (i29!=i23)). % 0.19/0.52 cnf(i_0_577, hypothesis, (i29!=i24)). % 0.19/0.52 cnf(i_0_572, hypothesis, (i29!=i25)). % 0.19/0.52 cnf(i_0_568, hypothesis, (i29!=i26)). % 0.19/0.52 cnf(i_0_565, hypothesis, (i29!=i27)). % 0.19/0.52 cnf(i_0_563, hypothesis, (i29!=i28)). % 0.19/0.52 cnf(i_0_967, hypothesis, (i30!=i1)). % 0.19/0.52 cnf(i_0_939, hypothesis, (i30!=i2)). % 0.19/0.52 cnf(i_0_912, hypothesis, (i30!=i3)). % 0.19/0.52 cnf(i_0_886, hypothesis, (i30!=i4)). % 0.19/0.52 cnf(i_0_861, hypothesis, (i30!=i5)). % 0.19/0.52 cnf(i_0_837, hypothesis, (i30!=i6)). % 0.19/0.52 cnf(i_0_814, hypothesis, (i30!=i7)). % 0.19/0.52 cnf(i_0_792, hypothesis, (i30!=i8)). % 0.19/0.52 cnf(i_0_771, hypothesis, (i30!=i9)). % 0.19/0.52 cnf(i_0_751, hypothesis, (i30!=i10)). % 0.19/0.52 cnf(i_0_732, hypothesis, (i30!=i11)). % 0.19/0.52 cnf(i_0_714, hypothesis, (i30!=i12)). % 0.19/0.52 cnf(i_0_697, hypothesis, (i30!=i13)). % 0.19/0.52 cnf(i_0_681, hypothesis, (i30!=i14)). % 0.19/0.52 cnf(i_0_666, hypothesis, (i30!=i15)). % 0.19/0.52 cnf(i_0_652, hypothesis, (i30!=i16)). % 0.19/0.52 cnf(i_0_639, hypothesis, (i30!=i17)). % 0.19/0.52 cnf(i_0_627, hypothesis, (i30!=i18)). % 0.19/0.52 cnf(i_0_616, hypothesis, (i30!=i19)). % 0.19/0.52 cnf(i_0_606, hypothesis, (i30!=i20)). % 0.19/0.52 cnf(i_0_597, hypothesis, (i30!=i21)). % 0.19/0.52 cnf(i_0_589, hypothesis, (i30!=i22)). % 0.19/0.52 cnf(i_0_582, hypothesis, (i30!=i23)). % 0.19/0.52 cnf(i_0_576, hypothesis, (i30!=i24)). % 0.19/0.52 cnf(i_0_571, hypothesis, (i30!=i25)). % 0.19/0.52 cnf(i_0_567, hypothesis, (i30!=i26)). % 0.19/0.52 cnf(i_0_564, hypothesis, (i30!=i27)). % 0.19/0.52 cnf(i_0_562, hypothesis, (i30!=i28)). % 0.19/0.52 cnf(i_0_561, hypothesis, (i30!=i29)). % 0.19/0.52 cnf(i_0_500, plain, (select(store(X1,X2,X3),X4)=select(X1,X4)|X2=X4)). % 0.19/0.52 cnf(i_0_1002, plain, (X5=X5)). % 0.19/0.52 # End listing active clauses. There is an equivalent clause to each of these in the clausification! % 0.19/0.52 # Begin printing tableau % 0.19/0.52 # Found 5 steps % 0.19/0.52 cnf(i_0_530, hypothesis, (store(a_1046,i1,e1)=a_1047), inference(start_rule)). % 0.19/0.52 cnf(i_0_1008, plain, (store(a_1046,i1,e1)=a_1047), inference(extension_rule, [i_0_1005])). % 0.19/0.52 cnf(i_0_1516, plain, (store(a_1046,i1,e1)!=a_1047), inference(closure_rule, [i_0_530])). % 0.19/0.52 cnf(i_0_1514, plain, (store(a_1046,i1,e1)=store(a_1046,i1,e1)), inference(extension_rule, [i_0_1007])). % 0.19/0.52 cnf(i_0_1587, plain, (store(a_1046,i1,e1)!=a_1047), inference(closure_rule, [i_0_530])). % 0.19/0.52 # End printing tableau % 0.19/0.52 # SZS output end % 0.19/0.52 # Branches closed with saturation will be marked with an "s" % 0.19/0.53 # 21629 Satisfiable branch % 0.19/0.53 # 21631 Satisfiable branch % 0.19/0.53 # 21633 Satisfiable branch % 0.19/0.53 # Satisfiable branch found. % 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 0 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 0 successful branch saturations after the branch. % 0.19/0.53 # SZS status Satisfiable 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_530, hypothesis, (store(a_1046,i1,e1)=a_1047)). % 0.19/0.53 cnf(i_0_560, hypothesis, (store(a_1076,i10,e10)=a_1077)). % 0.19/0.53 cnf(i_0_501, hypothesis, (store(a1,i1,e1)=a_1018)). % 0.19/0.53 cnf(i_0_502, hypothesis, (store(a_1018,i2,e2)=a_1019)). % 0.19/0.53 cnf(i_0_503, hypothesis, (store(a_1019,i3,e3)=a_1020)). % 0.19/0.53 cnf(i_0_504, hypothesis, (store(a_1020,i4,e4)=a_1021)). % 0.19/0.53 cnf(i_0_505, hypothesis, (store(a_1021,i5,e5)=a_1022)). % 0.19/0.53 cnf(i_0_506, hypothesis, (store(a_1022,i6,e6)=a_1023)). % 0.19/0.53 cnf(i_0_507, hypothesis, (store(a_1023,i7,e7)=a_1024)). % 0.19/0.53 cnf(i_0_508, hypothesis, (store(a_1024,i8,e8)=a_1025)). % 0.19/0.53 cnf(i_0_509, hypothesis, (store(a_1025,i9,e9)=a_1026)). % 0.19/0.53 cnf(i_0_510, hypothesis, (store(a_1026,i10,e10)=a_1027)). % 0.19/0.53 cnf(i_0_511, hypothesis, (store(a_1027,i11,e11)=a_1028)). % 0.19/0.53 cnf(i_0_512, hypothesis, (store(a_1028,i12,e12)=a_1029)). % 0.19/0.53 cnf(i_0_513, hypothesis, (store(a_1029,i13,e13)=a_1030)). % 0.19/0.53 cnf(i_0_514, hypothesis, (store(a_1030,i14,e14)=a_1031)). % 0.19/0.53 cnf(i_0_515, hypothesis, (store(a_1031,i15,e15)=a_1032)). % 0.19/0.53 cnf(i_0_516, hypothesis, (store(a_1032,i16,e16)=a_1033)). % 0.19/0.53 cnf(i_0_517, hypothesis, (store(a_1033,i17,e17)=a_1034)). % 0.19/0.53 cnf(i_0_518, hypothesis, (store(a_1034,i18,e18)=a_1035)). % 0.19/0.53 cnf(i_0_519, hypothesis, (store(a_1035,i19,e19)=a_1036)). % 0.19/0.53 cnf(i_0_520, hypothesis, (store(a_1036,i20,e20)=a_1037)). % 0.19/0.53 cnf(i_0_521, hypothesis, (store(a_1037,i21,e21)=a_1038)). % 0.19/0.53 cnf(i_0_522, hypothesis, (store(a_1038,i22,e22)=a_1039)). % 0.19/0.53 cnf(i_0_523, hypothesis, (store(a_1039,i23,e23)=a_1040)). % 0.19/0.53 cnf(i_0_524, hypothesis, (store(a_1040,i24,e24)=a_1041)). % 0.19/0.53 cnf(i_0_525, hypothesis, (store(a_1041,i25,e25)=a_1042)). % 0.19/0.53 cnf(i_0_526, hypothesis, (store(a_1042,i26,e26)=a_1043)). % 0.19/0.53 cnf(i_0_527, hypothesis, (store(a_1043,i27,e27)=a_1044)). % 0.19/0.53 cnf(i_0_528, hypothesis, (store(a_1044,i28,e28)=a_1045)). % 0.19/0.53 cnf(i_0_529, hypothesis, (store(a_1045,i29,e29)=a_1046)). % 0.19/0.53 cnf(i_0_531, hypothesis, (store(a1,i13,e13)=a_1048)). % 0.19/0.53 cnf(i_0_532, hypothesis, (store(a_1048,i1,e1)=a_1049)). % 0.19/0.53 cnf(i_0_533, hypothesis, (store(a_1049,i19,e19)=a_1050)). % 0.19/0.53 cnf(i_0_534, hypothesis, (store(a_1050,i4,e4)=a_1051)). % 0.19/0.53 cnf(i_0_535, hypothesis, (store(a_1051,i9,e9)=a_1052)). % 0.19/0.53 cnf(i_0_536, hypothesis, (store(a_1052,i30,e30)=a_1053)). % 0.19/0.53 cnf(i_0_537, hypothesis, (store(a_1053,i2,e2)=a_1054)). % 0.19/0.53 cnf(i_0_538, hypothesis, (store(a_1054,i15,e15)=a_1055)). % 0.19/0.53 cnf(i_0_539, hypothesis, (store(a_1055,i25,e25)=a_1056)). % 0.19/0.53 cnf(i_0_540, hypothesis, (store(a_1056,i18,e18)=a_1057)). % 0.19/0.53 cnf(i_0_541, hypothesis, (store(a_1057,i20,e20)=a_1058)). % 0.19/0.53 cnf(i_0_542, hypothesis, (store(a_1058,i8,e8)=a_1059)). % 0.19/0.53 cnf(i_0_543, hypothesis, (store(a_1059,i21,e21)=a_1060)). % 0.19/0.53 cnf(i_0_544, hypothesis, (store(a_1060,i6,e6)=a_1061)). % 0.19/0.53 cnf(i_0_545, hypothesis, (store(a_1061,i11,e11)=a_1062)). % 0.19/0.53 cnf(i_0_546, hypothesis, (store(a_1062,i14,e14)=a_1063)). % 0.19/0.53 cnf(i_0_547, hypothesis, (store(a_1063,i29,e29)=a_1064)). % 0.19/0.53 cnf(i_0_548, hypothesis, (store(a_1064,i5,e5)=a_1065)). % 0.19/0.53 cnf(i_0_549, hypothesis, (store(a_1065,i26,e26)=a_1066)). % 0.19/0.53 cnf(i_0_550, hypothesis, (store(a_1066,i22,e22)=a_1067)). % 0.19/0.53 cnf(i_0_551, hypothesis, (store(a_1067,i27,e27)=a_1068)). % 0.19/0.53 cnf(i_0_552, hypothesis, (store(a_1068,i3,e3)=a_1069)). % 0.19/0.53 cnf(i_0_553, hypothesis, (store(a_1069,i12,e12)=a_1070)). % 0.19/0.53 cnf(i_0_554, hypothesis, (store(a_1070,i16,e16)=a_1071)). % 0.19/0.53 cnf(i_0_555, hypothesis, (store(a_1071,i28,e28)=a_1072)). % 0.19/0.53 cnf(i_0_556, hypothesis, (store(a_1072,i17,e17)=a_1073)). % 0.19/0.53 cnf(i_0_557, hypothesis, (store(a_1073,i23,e23)=a_1074)). % 0.19/0.53 cnf(i_0_558, hypothesis, (store(a_1074,i24,e24)=a_1075)). % 0.19/0.53 cnf(i_0_559, hypothesis, (store(a_1075,i7,e7)=a_1076)). % 0.19/0.53 cnf(i_0_499, plain, (select(store(X1,X2,X3),X2)=X3)). % 0.19/0.53 cnf(i_0_996, negated_conjecture, (a_1077!=a_1047)). % 0.19/0.53 cnf(i_0_995, hypothesis, (i2!=i1)). % 0.19/0.53 cnf(i_0_994, hypothesis, (i3!=i1)). % 0.19/0.53 cnf(i_0_966, hypothesis, (i3!=i2)). % 0.19/0.53 cnf(i_0_993, hypothesis, (i4!=i1)). % 0.19/0.53 cnf(i_0_965, hypothesis, (i4!=i2)). % 0.19/0.53 cnf(i_0_938, hypothesis, (i4!=i3)). % 0.19/0.53 cnf(i_0_992, hypothesis, (i5!=i1)). % 0.19/0.53 cnf(i_0_964, hypothesis, (i5!=i2)). % 0.19/0.53 cnf(i_0_937, hypothesis, (i5!=i3)). % 0.19/0.53 cnf(i_0_911, hypothesis, (i5!=i4)). % 0.19/0.53 cnf(i_0_991, hypothesis, (i6!=i1)). % 0.19/0.53 cnf(i_0_963, hypothesis, (i6!=i2)). % 0.19/0.53 cnf(i_0_936, hypothesis, (i6!=i3)). % 0.19/0.53 cnf(i_0_910, hypothesis, (i6!=i4)). % 0.19/0.53 cnf(i_0_885, hypothesis, (i6!=i5)). % 0.19/0.53 cnf(i_0_990, hypothesis, (i7!=i1)). % 0.19/0.53 cnf(i_0_962, hypothesis, (i7!=i2)). % 0.19/0.53 cnf(i_0_935, hypothesis, (i7!=i3)). % 0.19/0.53 cnf(i_0_909, hypothesis, (i7!=i4)). % 0.19/0.53 cnf(i_0_884, hypothesis, (i7!=i5)). % 0.19/0.53 cnf(i_0_860, hypothesis, (i7!=i6)). % 0.19/0.53 cnf(i_0_989, hypothesis, (i8!=i1)). % 0.19/0.53 cnf(i_0_961, hypothesis, (i8!=i2)). % 0.19/0.53 cnf(i_0_934, hypothesis, (i8!=i3)). % 0.19/0.53 cnf(i_0_908, hypothesis, (i8!=i4)). % 0.19/0.53 cnf(i_0_883, hypothesis, (i8!=i5)). % 0.19/0.53 cnf(i_0_859, hypothesis, (i8!=i6)). % 0.19/0.53 cnf(i_0_836, hypothesis, (i8!=i7)). % 0.19/0.53 cnf(i_0_988, hypothesis, (i9!=i1)). % 0.19/0.53 cnf(i_0_960, hypothesis, (i9!=i2)). % 0.19/0.53 cnf(i_0_933, hypothesis, (i9!=i3)). % 0.19/0.53 cnf(i_0_907, hypothesis, (i9!=i4)). % 0.19/0.53 cnf(i_0_882, hypothesis, (i9!=i5)). % 0.19/0.53 cnf(i_0_858, hypothesis, (i9!=i6)). % 0.19/0.53 cnf(i_0_835, hypothesis, (i9!=i7)). % 0.19/0.53 cnf(i_0_813, hypothesis, (i9!=i8)). % 0.19/0.53 cnf(i_0_987, hypothesis, (i10!=i1)). % 0.19/0.53 cnf(i_0_959, hypothesis, (i10!=i2)). % 0.19/0.53 cnf(i_0_932, hypothesis, (i10!=i3)). % 0.19/0.53 cnf(i_0_906, hypothesis, (i10!=i4)). % 0.19/0.53 cnf(i_0_881, hypothesis, (i10!=i5)). % 0.19/0.53 cnf(i_0_857, hypothesis, (i10!=i6)). % 0.19/0.53 cnf(i_0_834, hypothesis, (i10!=i7)). % 0.19/0.53 cnf(i_0_812, hypothesis, (i10!=i8)). % 0.19/0.53 cnf(i_0_791, hypothesis, (i10!=i9)). % 0.19/0.53 cnf(i_0_986, hypothesis, (i11!=i1)). % 0.19/0.53 cnf(i_0_958, hypothesis, (i11!=i2)). % 0.19/0.53 cnf(i_0_931, hypothesis, (i11!=i3)). % 0.19/0.53 cnf(i_0_905, hypothesis, (i11!=i4)). % 0.19/0.53 cnf(i_0_880, hypothesis, (i11!=i5)). % 0.19/0.53 cnf(i_0_856, hypothesis, (i11!=i6)). % 0.19/0.53 cnf(i_0_833, hypothesis, (i11!=i7)). % 0.19/0.53 cnf(i_0_811, hypothesis, (i11!=i8)). % 0.19/0.53 cnf(i_0_790, hypothesis, (i11!=i9)). % 0.19/0.53 cnf(i_0_770, hypothesis, (i11!=i10)). % 0.19/0.53 cnf(i_0_985, hypothesis, (i12!=i1)). % 0.19/0.53 cnf(i_0_957, hypothesis, (i12!=i2)). % 0.19/0.53 cnf(i_0_930, hypothesis, (i12!=i3)). % 0.19/0.53 cnf(i_0_904, hypothesis, (i12!=i4)). % 0.19/0.53 cnf(i_0_879, hypothesis, (i12!=i5)). % 0.19/0.53 cnf(i_0_855, hypothesis, (i12!=i6)). % 0.19/0.53 cnf(i_0_832, hypothesis, (i12!=i7)). % 0.19/0.53 cnf(i_0_810, hypothesis, (i12!=i8)). % 0.19/0.53 cnf(i_0_789, hypothesis, (i12!=i9)). % 0.19/0.53 cnf(i_0_769, hypothesis, (i12!=i10)). % 0.19/0.53 cnf(i_0_750, hypothesis, (i12!=i11)). % 0.19/0.53 cnf(i_0_984, hypothesis, (i13!=i1)). % 0.19/0.53 cnf(i_0_956, hypothesis, (i13!=i2)). % 0.19/0.53 cnf(i_0_929, hypothesis, (i13!=i3)). % 0.19/0.53 cnf(i_0_903, hypothesis, (i13!=i4)). % 0.19/0.53 cnf(i_0_878, hypothesis, (i13!=i5)). % 0.19/0.53 cnf(i_0_854, hypothesis, (i13!=i6)). % 0.19/0.53 cnf(i_0_831, hypothesis, (i13!=i7)). % 0.19/0.53 cnf(i_0_809, hypothesis, (i13!=i8)). % 0.19/0.53 cnf(i_0_788, hypothesis, (i13!=i9)). % 0.19/0.53 cnf(i_0_768, hypothesis, (i13!=i10)). % 0.19/0.53 cnf(i_0_749, hypothesis, (i13!=i11)). % 0.19/0.53 cnf(i_0_731, hypothesis, (i13!=i12)). % 0.19/0.53 cnf(i_0_983, hypothesis, (i14!=i1)). % 0.19/0.53 cnf(i_0_955, hypothesis, (i14!=i2)). % 0.19/0.53 cnf(i_0_928, hypothesis, (i14!=i3)). % 0.19/0.53 cnf(i_0_902, hypothesis, (i14!=i4)). % 0.19/0.53 cnf(i_0_877, hypothesis, (i14!=i5)). % 0.19/0.53 cnf(i_0_853, hypothesis, (i14!=i6)). % 0.19/0.53 cnf(i_0_830, hypothesis, (i14!=i7)). % 0.19/0.53 cnf(i_0_808, hypothesis, (i14!=i8)). % 0.19/0.53 cnf(i_0_787, hypothesis, (i14!=i9)). % 0.19/0.53 cnf(i_0_767, hypothesis, (i14!=i10)). % 0.19/0.53 cnf(i_0_748, hypothesis, (i14!=i11)). % 0.19/0.53 cnf(i_0_730, hypothesis, (i14!=i12)). % 0.19/0.53 cnf(i_0_713, hypothesis, (i14!=i13)). % 0.19/0.53 cnf(i_0_982, hypothesis, (i15!=i1)). % 0.19/0.53 cnf(i_0_954, hypothesis, (i15!=i2)). % 0.19/0.53 cnf(i_0_927, hypothesis, (i15!=i3)). % 0.19/0.53 cnf(i_0_901, hypothesis, (i15!=i4)). % 0.19/0.53 cnf(i_0_876, hypothesis, (i15!=i5)). % 0.19/0.53 cnf(i_0_852, hypothesis, (i15!=i6)). % 0.19/0.53 cnf(i_0_829, hypothesis, (i15!=i7)). % 0.19/0.53 cnf(i_0_807, hypothesis, (i15!=i8)). % 0.19/0.53 cnf(i_0_786, hypothesis, (i15!=i9)). % 0.19/0.53 cnf(i_0_766, hypothesis, (i15!=i10)). % 0.19/0.53 cnf(i_0_747, hypothesis, (i15!=i11)). % 0.19/0.53 cnf(i_0_729, hypothesis, (i15!=i12)). % 0.19/0.53 cnf(i_0_712, hypothesis, (i15!=i13)). % 0.19/0.53 cnf(i_0_696, hypothesis, (i15!=i14)). % 0.19/0.53 cnf(i_0_981, hypothesis, (i16!=i1)). % 0.19/0.53 cnf(i_0_953, hypothesis, (i16!=i2)). % 0.19/0.53 cnf(i_0_926, hypothesis, (i16!=i3)). % 0.19/0.53 cnf(i_0_900, hypothesis, (i16!=i4)). % 0.19/0.53 cnf(i_0_875, hypothesis, (i16!=i5)). % 0.19/0.53 cnf(i_0_851, hypothesis, (i16!=i6)). % 0.19/0.53 cnf(i_0_828, hypothesis, (i16!=i7)). % 0.19/0.53 cnf(i_0_806, hypothesis, (i16!=i8)). % 0.19/0.53 cnf(i_0_785, hypothesis, (i16!=i9)). % 0.19/0.53 cnf(i_0_765, hypothesis, (i16!=i10)). % 0.19/0.53 cnf(i_0_746, hypothesis, (i16!=i11)). % 0.19/0.53 cnf(i_0_728, hypothesis, (i16!=i12)). % 0.19/0.53 cnf(i_0_711, hypothesis, (i16!=i13)). % 0.19/0.53 cnf(i_0_695, hy# Child (21634) has found a proof. % 0.19/0.53 % 0.19/0.55 # Proof search is over... % 0.19/0.55 # Freeing feature tree %------------------------------------------------------------------------------