%------------------------------------------------------------------------------ % File : Etableau---0.67 % Problem : SYN419-1 : TPTP v8.1.0. Released v2.1.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 : n029.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 : Thu Jul 21 06:10:50 EDT 2022 % Result : Satisfiable 22.94s 3.41s % Output : CNFRefutation 22.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : SYN419-1 : TPTP v8.1.0. Released v2.1.0. % 0.08/0.14 % Command : etableau --auto --tsmdo --quicksat=10000 --tableau=1 --tableau-saturation=1 -s -p --tableau-cores=8 --cpu-limit=%d %s % 0.13/0.35 % Computer : n029.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Mon Jul 11 22:03:47 EDT 2022 % 0.13/0.35 % CPUTime : % 0.21/0.44 # No SInE strategy applied % 0.21/0.44 # Auto-Mode selected heuristic G_____X1276__C12_02_nc_F1_AE_CS_SP_RG_S04AN % 0.21/0.44 # and selection function SelectComplexExceptUniqMaxHorn. % 0.21/0.44 # % 0.21/0.44 # Presaturation interreduction done % 0.21/0.44 # Number of axioms: 436 Number of unprocessed: 396 % 0.21/0.44 # Tableaux proof search. % 0.21/0.44 # APR header successfully linked. % 0.21/0.44 # Hello from C++ % 0.21/0.46 # The folding up rule is enabled... % 0.21/0.46 # Local unification is enabled... % 0.21/0.46 # Any saturation attempts will use folding labels... % 0.21/0.46 # 396 beginning clauses after preprocessing and clausification % 0.21/0.46 # Creating start rules for all 396 conjectures. % 0.21/0.46 # There are 396 start rule candidates: % 0.21/0.46 # Found 1 unit axioms. % 0.21/0.46 # Unsuccessfully attempted saturation on 1 start tableaux, moving on. % 0.21/0.46 # 396 start rule tableaux created. % 0.21/0.46 # 395 extension rule candidate clauses % 0.21/0.46 # 1 unit axiom clauses % 0.21/0.46 % 0.21/0.46 # Requested 8, 32 cores available to the main process. % 22.94/3.40 # 5231 Satisfiable branch % 22.94/3.41 # Satisfiable branch found. % 22.94/3.41 # There were 1 total branch saturation attempts. % 22.94/3.41 # There were 0 of these attempts blocked. % 22.94/3.41 # There were 0 deferred branch saturation attempts. % 22.94/3.41 # There were 0 free duplicated saturations. % 22.94/3.41 # There were 0 total successful branch saturations. % 22.94/3.41 # There were 0 successful branch saturations in interreduction. % 22.94/3.41 # There were 0 successful branch saturations on the branch. % 22.94/3.41 # There were 0 successful branch saturations after the branch. % 22.94/3.41 # SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 22.94/3.41 # SZS output start for /export/starexec/sandbox/benchmark/theBenchmark.p % 22.94/3.41 # Begin clausification derivation % 22.94/3.41 % 22.94/3.41 # End clausification derivation % 22.94/3.41 # Begin listing active clauses obtained from FOF to CNF conversion % 22.94/3.41 cnf(i_0_438, negated_conjecture, (ndr1_0)). % 22.94/3.41 cnf(i_0_440, negated_conjecture, (c7_0|c8_0)). % 22.94/3.41 cnf(i_0_467, negated_conjecture, (c2_0|~c6_0)). % 22.94/3.41 cnf(i_0_466, negated_conjecture, (c5_0|~c6_0)). % 22.94/3.41 cnf(i_0_516, negated_conjecture, (c9_0|c8_0|~c6_0)). % 22.94/3.41 cnf(i_0_517, negated_conjecture, (c9_0|c1_0|~c8_0)). % 22.94/3.41 cnf(i_0_518, negated_conjecture, (c4_0|c1_0|~c8_0)). % 22.94/3.41 cnf(i_0_600, negated_conjecture, (c6_0|~c4_0|~c10_0)). % 22.94/3.41 cnf(i_0_597, negated_conjecture, (c8_0|~c9_0|~c1_0)). % 22.94/3.41 cnf(i_0_601, negated_conjecture, (c8_0|~c4_0|~c5_0)). % 22.94/3.41 cnf(i_0_598, negated_conjecture, (c2_0|~c3_0|~c1_0)). % 22.94/3.41 cnf(i_0_599, negated_conjecture, (c4_0|~c3_0|~c8_0)). % 22.94/3.41 cnf(i_0_596, negated_conjecture, (c3_0|~c4_0|~c5_0)). % 22.94/3.41 cnf(i_0_462, negated_conjecture, (ndr1_1(a177)|c6_0)). % 22.94/3.41 cnf(i_0_463, negated_conjecture, (c1_1(a177)|c6_0)). % 22.94/3.41 cnf(i_0_464, negated_conjecture, (c7_1(a162)|c8_0)). % 22.94/3.41 cnf(i_0_468, negated_conjecture, (ndr1_1(a258)|ssSkC25)). % 22.94/3.41 cnf(i_0_469, negated_conjecture, (c5_1(a258)|ssSkC25)). % 22.94/3.41 cnf(i_0_471, negated_conjecture, (c2_1(a239)|ssSkC23)). % 22.94/3.41 cnf(i_0_474, negated_conjecture, (ndr1_1(a224)|ssSkC19)). % 22.94/3.41 cnf(i_0_475, negated_conjecture, (c1_1(a222)|ssSkC18)). % 22.94/3.41 cnf(i_0_476, negated_conjecture, (c4_1(a222)|ssSkC18)). % 22.94/3.41 cnf(i_0_477, negated_conjecture, (c8_1(a215)|ssSkC16)). % 22.94/3.41 cnf(i_0_478, negated_conjecture, (ndr1_1(a212)|ssSkC15)). % 22.94/3.41 cnf(i_0_480, negated_conjecture, (ndr1_1(a200)|ssSkC11)). % 22.94/3.41 cnf(i_0_483, negated_conjecture, (c5_1(a185)|ssSkC8)). % 22.94/3.41 cnf(i_0_484, negated_conjecture, (ndr1_1(a179)|ssSkC6)). % 22.94/3.41 cnf(i_0_485, negated_conjecture, (c9_1(a174)|ssSkC5)). % 22.94/3.41 cnf(i_0_486, negated_conjecture, (c2_1(a169)|ssSkC3)). % 22.94/3.41 cnf(i_0_488, negated_conjecture, (ndr1_1(a149)|ssSkC1)). % 22.94/3.41 cnf(i_0_489, negated_conjecture, (c7_1(a147)|ssSkC0)). % 22.94/3.41 cnf(i_0_514, negated_conjecture, (c2_1(a157)|~c7_0)). % 22.94/3.41 cnf(i_0_549, negated_conjecture, (ssSkC4|~c1_1(a171))). % 22.94/3.41 cnf(i_0_550, negated_conjecture, (ssSkC4|~c8_1(a171))). % 22.94/3.41 cnf(i_0_512, negated_conjecture, (c8_0|~c2_1(a162))). % 22.94/3.41 cnf(i_0_519, negated_conjecture, (ssSkC26|~c9_1(a261))). % 22.94/3.41 cnf(i_0_520, negated_conjecture, (ssSkC25|~c8_1(a258))). % 22.94/3.41 cnf(i_0_510, negated_conjecture, (c7_1(a167)|c10_0|c6_0)). % 22.94/3.41 cnf(i_0_523, negated_conjecture, (ssSkC23|~c10_1(a239))). % 22.94/3.41 cnf(i_0_529, negated_conjecture, (ssSkC19|~c1_1(a224))). % 22.94/3.41 cnf(i_0_530, negated_conjecture, (ssSkC16|~c1_1(a215))). % 22.94/3.41 cnf(i_0_535, negated_conjecture, (ssSkC13|~c5_1(a206))). % 22.94/3.41 cnf(i_0_542, negated_conjecture, (ssSkC8|~c1_1(a185))). % 22.94/3.41 cnf(i_0_547, negated_conjecture, (ssSkC6|~c9_1(a179))). % 22.94/3.41 cnf(i_0_548, negated_conjecture, (ssSkC5|~c1_1(a174))). % 22.94/3.41 cnf(i_0_553, negated_conjecture, (ssSkC0|~c9_1(a147))). % 22.94/3.41 cnf(i_0_508, negated_conjecture, (~c5_1(a172)|~ssSkC4)). % 22.94/3.41 cnf(i_0_509, negated_conjecture, (c2_1(a167)|c10_0|c6_0)). % 22.94/3.41 cnf(i_0_491, negated_conjecture, (c1_1(a265)|c1_0|c2_0)). % 22.94/3.41 cnf(i_0_492, negated_conjecture, (c2_1(a265)|c1_0|c2_0)). % 22.94/3.41 cnf(i_0_495, negated_conjecture, (c5_1(a257)|c9_0|c10_0)). % 22.94/3.41 cnf(i_0_561, negated_conjecture, (ndr1_1(a251)|c6_0|~c7_0)). % 22.94/3.41 cnf(i_0_590, negated_conjecture, (c1_1(a168)|c6_0|~c1_0)). % 22.94/3.41 cnf(i_0_562, negated_conjecture, (c2_1(a251)|c6_0|~c7_0)). % 22.94/3.41 cnf(i_0_591, negated_conjecture, (c8_1(a168)|c6_0|~c1_0)). % 22.94/3.41 cnf(i_0_563, negated_conjecture, (ndr1_1(a247)|c7_0|~c9_0)). % 22.94/3.41 cnf(i_0_582, negated_conjecture, (ndr1_1(a190)|c7_0|~c10_0)). % 22.94/3.41 cnf(i_0_565, negated_conjecture, (c5_1(a245)|c7_0|~c9_0)). % 22.94/3.41 cnf(i_0_470, negated_conjecture, (ssSkP6(X1)|ndr1_1(X1))). % 22.94/3.41 cnf(i_0_472, negated_conjecture, (ssSkP5(X1)|ndr1_1(X1))). % 22.94/3.41 cnf(i_0_473, negated_conjecture, (ssSkP4(X1)|ndr1_1(X1))). % 22.94/3.41 cnf(i_0_479, negated_conjecture, (ssSkP3(X1)|ndr1_1(X1))). % 22.94/3.41 cnf(i_0_481, negated_conjecture, (ssSkP2(X1)|ndr1_1(X1))). % 22.94/3.41 cnf(i_0_564, negated_conjecture, (c9_1(a245)|c7_0|~c9_0)). % 22.94/3.41 cnf(i_0_493, negated_conjecture, (ndr1_1(a262)|c2_0|~ssSkC26)). % 22.94/3.41 cnf(i_0_494, negated_conjecture, (c5_1(a262)|c2_0|~ssSkC26)). % 22.94/3.41 cnf(i_0_554, negated_conjecture, (ndr1_1(a266)|c1_0|~c5_0)). % 22.94/3.41 cnf(i_0_579, negated_conjecture, (ndr1_1(a195)|c1_0|~c6_0)). % 22.94/3.41 cnf(i_0_580, negated_conjecture, (c7_1(a195)|c1_0|~c6_0)). % 22.94/3.41 cnf(i_0_581, negated_conjecture, (c2_1(a195)|c1_0|~c6_0)). % 22.94/3.41 cnf(i_0_498, negated_conjecture, (ndr1_1(a240)|c9_0|~ssSkC23)). % 22.94/3.41 cnf(i_0_592, negated_conjecture, (ndr1_1(a165)|c9_0|~c2_0)). % 22.94/3.41 cnf(i_0_570, negated_conjecture, (c4_0|c9_1(a234)|~c8_0)). % 22.94/3.41 cnf(i_0_504, negated_conjecture, (ndr1_1(a204)|~ssSkC12|~ssSkC11)). % 22.94/3.41 cnf(i_0_569, negated_conjecture, (ndr1_1(a237)|~ssSkC22|~c9_0)). % 22.94/3.41 cnf(i_0_571, negated_conjecture, (ndr1_1(a232)|~ssSkC21|~c10_0)). % 22.94/3.41 cnf(i_0_573, negated_conjecture, (ndr1_1(a216)|~c10_0|~ssSkC16)). % 22.94/3.41 cnf(i_0_586, negated_conjecture, (ndr1_1(a175)|~c5_0|~ssSkC5)). % 22.94/3.41 cnf(i_0_595, negated_conjecture, (ndr1_1(a152)|~c4_0|~ssSkC1)). % 22.94/3.41 cnf(i_0_662, negated_conjecture, (ndr1_1(a163)|~c9_0|~c1_0)). % 22.94/3.41 cnf(i_0_576, negated_conjecture, (c1_1(a207)|~ssSkC13|~c7_0)). % 22.94/3.41 cnf(i_0_588, negated_conjecture, (c1_1(a175)|~c5_0|~ssSkC5)). % 22.94/3.41 cnf(i_0_663, negated_conjecture, (c1_1(a163)|~c9_0|~c1_0)). % 22.94/3.41 cnf(i_0_657, negated_conjecture, (c7_1(a173)|~c5_0|~c8_0)). % 22.94/3.41 cnf(i_0_482, negated_conjecture, (ssSkP1(X1)|ndr1_1(X1))). % 22.94/3.41 cnf(i_0_487, negated_conjecture, (ssSkP0(X1)|ndr1_1(X1))). % 22.94/3.41 cnf(i_0_587, negated_conjecture, (c5_1(a175)|~c5_0|~ssSkC5)). % 22.94/3.41 cnf(i_0_575, negated_conjecture, (c9_1(a207)|~ssSkC13|~c7_0)). % 22.94/3.41 cnf(i_0_594, negated_conjecture, (c10_1(a160)|~ssSkC2|~c4_0)). % 22.94/3.41 cnf(i_0_572, negated_conjecture, (c6_1(a232)|~ssSkC21|~c10_0)). % 22.94/3.41 cnf(i_0_574, negated_conjecture, (c6_1(a207)|~ssSkC13|~c7_0)). % 22.94/3.41 cnf(i_0_658, negated_conjecture, (c6_1(a173)|~c5_0|~c8_0)). % 22.94/3.41 cnf(i_0_555, negated_conjecture, (c1_0|c2_0|~c7_1(a265))). % 22.94/3.41 cnf(i_0_559, negated_conjecture, (c9_0|c10_0|~c7_1(a257))). % 22.94/3.41 cnf(i_0_560, negated_conjecture, (c9_0|c10_0|~c2_1(a257))). % 22.94/3.41 cnf(i_0_635, negated_conjecture, (c6_0|~c9_1(a251)|~c7_0)). % 22.94/3.41 cnf(i_0_659, negated_conjecture, (c6_0|~c9_1(a168)|~c1_0)). % 22.94/3.41 cnf(i_0_638, negated_conjecture, (c7_0|~c8_1(a247)|~c9_0)). % 22.94/3.41 cnf(i_0_629, negated_conjecture, (c1_0|~c5_0|~c7_1(a266))). % 22.94/3.41 cnf(i_0_639, negated_conjecture, (c10_0|~c4_0|~c1_1(a246))). % 22.94/3.41 cnf(i_0_644, negated_conjecture, (c4_0|~c1_1(a234)|~c8_0)). % 22.94/3.41 cnf(i_0_686, negated_conjecture, (~c10_1(a173)|~c5_0|~c8_0)). % 22.94/3.41 cnf(i_0_578, negated_conjecture, (~c10_1(a204)|~ssSkC12|~ssSkC11)). % 22.94/3.41 cnf(i_0_667, negated_conjecture, (~c4_0|~c8_1(a152)|~ssSkC1)). % 22.94/3.41 cnf(i_0_664, negated_conjecture, (~ssSkC2|~c4_0|~c7_1(a160))). % 22.94/3.41 cnf(i_0_646, negated_conjecture, (~c3_0|~ssSkC17|~c7_1(a219))). % 22.94/3.41 cnf(i_0_647, negated_conjecture, (~c3_0|~ssSkC17|~c5_1(a219))). % 22.94/3.41 cnf(i_0_527, negated_conjecture, (c3_2(a224,a225)|ssSkC19)). % 22.94/3.41 cnf(i_0_528, negated_conjecture, (c9_2(a224,a225)|ssSkC19)). % 22.94/3.41 cnf(i_0_531, negated_conjecture, (c5_2(a212,a213)|ssSkC15)). % 22.94/3.41 cnf(i_0_532, negated_conjecture, (c4_2(a212,a213)|ssSkC15)). % 22.94/3.41 cnf(i_0_537, negated_conjecture, (c3_2(a200,a202)|ssSkC11)). % 22.94/3.41 cnf(i_0_538, negated_conjecture, (c9_2(a200,a202)|ssSkC11)). % 22.94/3.41 cnf(i_0_539, negated_conjecture, (c5_2(a200,a201)|ssSkC11)). % 22.94/3.41 cnf(i_0_536, negated_conjecture, (c2_2(a200,a202)|ssSkC11)). % 22.94/3.41 cnf(i_0_546, negated_conjecture, (c10_2(a179,a180)|ssSkC6)). % 22.94/3.41 cnf(i_0_543, negated_conjecture, (c3_2(a179,a181)|ssSkC6)). % 22.94/3.41 cnf(i_0_544, negated_conjecture, (c5_2(a179,a181)|ssSkC6)). % 22.94/3.41 cnf(i_0_545, negated_conjecture, (c5_2(a179,a180)|ssSkC6)). % 22.94/3.41 cnf(i_0_552, negated_conjecture, (c7_2(a149,a150)|ssSkC1)). % 22.94/3.41 cnf(i_0_585, negated_conjecture, (c6_0|~c7_2(a177,a178))). % 22.94/3.41 cnf(i_0_583, negated_conjecture, (c6_0|~c3_2(a177,a178))). % 22.94/3.41 cnf(i_0_584, negated_conjecture, (c6_0|~c9_2(a177,a178))). % 22.94/3.41 cnf(i_0_602, negated_conjecture, (ssSkC25|~c10_2(a258,a259))). % 22.94/3.41 cnf(i_0_603, negated_conjecture, (ssSkC25|~c6_2(a258,a259))). % 22.94/3.41 cnf(i_0_604, negated_conjecture, (ssSkC25|~c2_2(a258,a259))). % 22.94/3.41 cnf(i_0_609, negated_conjecture, (ssSkC19|~c4_2(a224,a225))). % 22.94/3.41 cnf(i_0_610, negated_conjecture, (ssSkC15|~c8_2(a212,a213))). % 22.94/3.41 cnf(i_0_612, negated_conjecture, (ssSkC11|~c7_2(a200,a201))). % 22.94/3.41 cnf(i_0_613, negated_conjecture, (ssSkC11|~c8_2(a200,a201))). % 22.94/3.41 cnf(i_0_618, negated_conjecture, (ssSkC6|~c8_2(a179,a180))). % 22.94/3.41 cnf(i_0_623, negated_conjecture, (ssSkC1|~c10_2(a149,a151))). % 22.94/3.41 cnf(i_0_624, negated_conjecture, (ssSkC1|~c9_2(a149,a150))). % 22.94/3.41 cnf(i_0_625, negated_conjecture, (ssSkC1|~c5_2(a149,a150))). % 22.94/3.41 cnf(i_0_621, negated_conjecture, (ssSkC1|~c4_2(a149,a151))). % 22.94/3.41 cnf(i_0_622, negated_conjecture, (ssSkC1|~c1_2(a149,a151))). % 22.94/3.41 cnf(i_0_521, negated_conjecture, (c10_2(X1,a254)|ssSkP6(X1))). % 22.94/3.41 cnf(i_0_522, negated_conjecture, (c6_2(X1,a254)|ssSkP6(X1))). % 22.94/3.41 cnf(i_0_525, negated_conjecture, (c6_2(X1,a230)|ssSkP5(X1))). % 22.94/3.41 cnf(i_0_524, negated_conjecture, (c7_2(X1,a230)|ssSkP5(X1))). % 22.94/3.41 cnf(i_0_526, negated_conjecture, (c3_2(X1,a226)|ssSkP4(X1))). % 22.94/3.41 cnf(i_0_695, negated_conjecture, (c4_1(X1)|c5_1(X1)|c5_0|~c9_0)). % 22.94/3.41 cnf(i_0_633, negated_conjecture, (c10_2(a251,a252)|c6_0|~c7_0)). % 22.94/3.41 cnf(i_0_634, negated_conjecture, (c1_2(a251,a252)|c6_0|~c7_0)). % 22.94/3.41 cnf(i_0_655, negated_conjecture, (c7_2(a190,a191)|c7_0|~c10_0)). % 22.94/3.41 cnf(i_0_637, negated_conjecture, (c3_2(a247,a248)|c7_0|~c9_0)). % 22.94/3.41 cnf(i_0_654, negated_conjecture, (c3_2(a190,a191)|c7_0|~c10_0)). % 22.94/3.41 cnf(i_0_636, negated_conjecture, (c5_2(a247,a248)|c7_0|~c9_0)). % 22.94/3.41 cnf(i_0_653, negated_conjecture, (c4_2(a190,a192)|c7_0|~c10_0)). % 22.94/3.41 cnf(i_0_558, negated_conjecture, (c10_2(a262,a263)|c2_0|~ssSkC26)). % 22.94/3.41 cnf(i_0_557, negated_conjecture, (c9_2(a262,a263)|c2_0|~ssSkC26)). % 22.94/3.41 cnf(i_0_556, negated_conjecture, (c8_2(a262,a263)|c2_0|~ssSkC26)). % 22.94/3.41 cnf(i_0_626, negated_conjecture, (c10_2(a266,a268)|c1_0|~c5_0)). % 22.94/3.41 cnf(i_0_651, negated_conjecture, (c10_2(a195,a196)|c1_0|~c6_0)). % 22.94/3.41 cnf(i_0_627, negated_conjecture, (c6_2(a266,a268)|c1_0|~c5_0)). % 22.94/3.41 cnf(i_0_628, negated_conjecture, (c7_2(a266,a267)|c1_0|~c5_0)). % 22.94/3.41 cnf(i_0_652, negated_conjecture, (c2_2(a195,a196)|c1_0|~c6_0)). % 22.94/3.41 cnf(i_0_567, negated_conjecture, (c3_2(a240,a241)|c9_0|~ssSkC23)). % 22.94/3.41 cnf(i_0_661, negated_conjecture, (c3_2(a165,a166)|c9_0|~c2_0)). % 22.94/3.41 cnf(i_0_568, negated_conjecture, (c9_2(a240,a241)|c9_0|~ssSkC23)). % 22.94/3.41 cnf(i_0_660, negated_conjecture, (c5_2(a165,a166)|c9_0|~c2_0)). % 22.94/3.41 cnf(i_0_566, negated_conjecture, (c8_2(a240,a242)|c9_0|~ssSkC23)). % 22.94/3.41 cnf(i_0_533, negated_conjecture, (c7_2(X1,a210)|ssSkP3(X1))). % 22.94/3.41 cnf(i_0_534, negated_conjecture, (c3_2(X1,a210)|ssSkP3(X1))). % 22.94/3.41 cnf(i_0_541, negated_conjecture, (c6_2(X1,a198)|ssSkP2(X1))). % 22.94/3.41 cnf(i_0_540, negated_conjecture, (c7_2(X1,a198)|ssSkP2(X1))). % 22.94/3.41 cnf(i_0_551, negated_conjecture, (c10_2(X1,a155)|ssSkP0(X1))). % 22.94/3.41 cnf(i_0_648, negated_conjecture, (c10_2(a216,a217)|~c10_0|~ssSkC16)). % 22.94/3.41 cnf(i_0_656, negated_conjecture, (c10_2(a175,a176)|~c5_0|~ssSkC5)). % 22.94/3.41 cnf(i_0_689, negated_conjecture, (c10_2(a163,a164)|~c9_0|~c1_0)). % 22.94/3.41 cnf(i_0_577, negated_conjecture, (c6_2(a204,a205)|~ssSkC12|~ssSkC11)). % 22.94/3.41 cnf(i_0_665, negated_conjecture, (c7_2(a152,a153)|~c4_0|~ssSkC1)). % 22.94/3.41 cnf(i_0_666, negated_conjecture, (c9_2(a152,a153)|~c4_0|~ssSkC1)). % 22.94/3.41 cnf(i_0_688, negated_conjecture, (c9_2(a163,a164)|~c9_0|~c1_0)). % 22.94/3.41 cnf(i_0_643, negated_conjecture, (c4_2(a237,a238)|~ssSkC22|~c9_0)). % 22.94/3.41 cnf(i_0_642, negated_conjecture, (c2_2(a237,a238)|~ssSkC22|~c9_0)). % 22.94/3.41 cnf(i_0_645, negated_conjecture, (c8_2(a232,a233)|~ssSkC21|~c10_0)). % 22.94/3.41 cnf(i_0_671, negated_conjecture, (c6_0|~c5_2(a251,a252)|~c7_0)). % 22.94/3.41 cnf(i_0_681, negated_conjecture, (c7_0|~c10_2(a190,a192)|~c10_0)). % 22.94/3.41 cnf(i_0_682, negated_conjecture, (c7_0|~c8_2(a190,a192)|~c10_0)). % 22.94/3.41 cnf(i_0_683, negated_conjecture, (c7_0|~c8_2(a190,a191)|~c10_0)). % 22.94/3.41 cnf(i_0_673, negated_conjecture, (c7_0|~c10_2(a247,a249)|~c9_0)). % 22.94/3.41 cnf(i_0_675, negated_conjecture, (c7_0|~c6_2(a247,a248)|~c9_0)). % 22.94/3.41 cnf(i_0_672, negated_conjecture, (c7_0|~c6_2(a247,a249)|~c9_0)). % 22.94/3.41 cnf(i_0_674, negated_conjecture, (c7_0|~c4_2(a247,a249)|~c9_0)). % 22.94/3.41 cnf(i_0_631, negated_conjecture, (c2_0|~c10_2(a262,a264)|~ssSkC26)). % 22.94/3.41 cnf(i_0_630, negated_conjecture, (c2_0|~c6_2(a262,a264)|~ssSkC26)). % 22.94/3.41 cnf(i_0_632, negated_conjecture, (c2_0|~c4_2(a262,a264)|~ssSkC26)). % 22.94/3.41 cnf(i_0_605, negated_conjecture, (ssSkP6(X1)|~c8_2(X1,a254))). % 22.94/3.41 cnf(i_0_606, negated_conjecture, (ssSkP5(X1)|~c3_2(X1,a230))). % 22.94/3.41 cnf(i_0_607, negated_conjecture, (ssSkP4(X1)|~c4_2(X1,a226))). % 22.94/3.41 cnf(i_0_608, negated_conjecture, (ssSkP4(X1)|~c8_2(X1,a226))). % 22.94/3.41 cnf(i_0_611, negated_conjecture, (ssSkP3(X1)|~c1_2(X1,a210))). % 22.94/3.41 cnf(i_0_696, negated_conjecture, (c4_1(X1)|c1_0|c2_0|~c7_1(X1))). % 22.94/3.41 cnf(i_0_680, negated_conjecture, (c1_0|~c1_2(a195,a196)|~c6_0)). % 22.94/3.41 cnf(i_0_669, negated_conjecture, (c1_0|~c9_2(a266,a267)|~c5_0)). % 22.94/3.41 cnf(i_0_670, negated_conjecture, (c1_0|~c5_2(a266,a267)|~c5_0)). % 22.94/3.41 cnf(i_0_668, negated_conjecture, (c1_0|~c2_2(a266,a268)|~c5_0)). % 22.94/3.41 cnf(i_0_640, negated_conjecture, (c9_0|~c7_2(a240,a242)|~ssSkC23)). % 22.94/3.41 cnf(i_0_641, negated_conjecture, (c9_0|~c4_2(a240,a241)|~ssSkC23)). % 22.94/3.41 cnf(i_0_687, negated_conjecture, (c9_0|~c2_2(a165,a166)|~c2_0)). % 22.94/3.41 cnf(i_0_678, negated_conjecture, (~c6_2(a216,a217)|~c10_0|~ssSkC16)). % 22.94/3.41 cnf(i_0_679, negated_conjecture, (~c8_2(a216,a217)|~c10_0|~ssSkC16)). % 22.94/3.41 cnf(i_0_650, negated_conjecture, (~c3_2(a204,a205)|~ssSkC12|~ssSkC11)). % 22.94/3.41 cnf(i_0_649, negated_conjecture, (~c9_2(a204,a205)|~ssSkC12|~ssSkC11)). % 22.94/3.41 cnf(i_0_685, negated_conjecture, (~c6_2(a175,a176)|~c5_0|~ssSkC5)). % 22.94/3.41 cnf(i_0_684, negated_conjecture, (~c4_2(a175,a176)|~c5_0|~ssSkC5)). % 22.94/3.41 cnf(i_0_690, negated_conjecture, (~c10_2(a152,a153)|~c4_0|~ssSkC1)). % 22.94/3.41 cnf(i_0_694, negated_conjecture, (~c5_2(a163,a164)|~c9_0|~c1_0)). % 22.94/3.41 cnf(i_0_677, negated_conjecture, (~c7_2(a232,a233)|~ssSkC21|~c10_0)). % 22.94/3.41 cnf(i_0_676, negated_conjecture, (~c7_2(a237,a238)|~ssSkC22|~c9_0)). % 22.94/3.41 cnf(i_0_614, negated_conjecture, (ssSkP2(X1)|~c5_2(X1,a198))). % 22.94/3.41 cnf(i_0_615, negated_conjecture, (ssSkP1(X1)|~c7_2(X1,a187))). % 22.94/3.41 cnf(i_0_617, negated_conjecture, (ssSkP1(X1)|~c2_2(X1,a187))). % 22.94/3.41 cnf(i_0_616, negated_conjecture, (ssSkP1(X1)|~c1_2(X1,a187))). % 22.94/3.41 cnf(i_0_620, negated_conjecture, (ssSkP0(X1)|~c4_2(X1,a155))). % 22.94/3.41 cnf(i_0_619, negated_conjecture, (ssSkP0(X1)|~c1_2(X1,a155))). % 22.94/3.41 cnf(i_0_692, negated_conjecture, (ndr1_1(X1)|c9_0|~c2_1(X1)|~ssSkC25)). % 22.94/3.41 cnf(i_0_693, negated_conjecture, (ndr1_1(X1)|~ssSkC14|~c5_1(X1)|~ssSkC15)). % 22.94/3.41 cnf(i_0_705, negated_conjecture, (ndr1_1(X1)|~c4_1(X1)|~c1_0|~ssSkC0)). % 22.94/3.41 cnf(i_0_703, negated_conjecture, (c6_2(X1,a260)|c9_0|~c2_1(X1)|~ssSkC25)). % 22.94/3.41 cnf(i_0_723, negated_conjecture, (c7_2(X1,a148)|~c4_1(X1)|~c1_0|~ssSkC0)). % 22.94/3.41 cnf(i_0_724, negated_conjecture, (c3_2(X1,a148)|~c4_1(X1)|~c1_0|~ssSkC0)). % 22.94/3.41 cnf(i_0_704, negated_conjecture, (c8_2(X1,a214)|~ssSkC14|~c5_1(X1)|~ssSkC15)). % 22.94/3.41 cnf(i_0_719, negated_conjecture, (c9_0|~c10_2(X1,a260)|~c2_1(X1)|~ssSkC25)). % 22.94/3.41 cnf(i_0_720, negated_conjecture, (c9_0|~c2_2(X1,a260)|~c2_1(X1)|~ssSkC25)). % 22.94/3.41 cnf(i_0_722, negated_conjecture, (~ssSkC14|~c6_2(X1,a214)|~c5_1(X1)|~ssSkC15)). % 22.94/3.41 cnf(i_0_721, negated_conjecture, (~ssSkC14|~c4_2(X1,a214)|~c5_1(X1)|~ssSkC15)). % 22.94/3.41 cnf(i_0_749, negated_conjecture, (~c5_2(X1,a148)|~c4_1(X1)|~c1_0|~ssSkC0)). % 22.94/3.41 cnf(i_0_699, negated_conjecture, (c6_1(X1)|c1_1(X1)|ndr1_1(X1)|ssSkC12)). % 22.94/3.41 cnf(i_0_700, negated_conjecture, (ssSkC7|c3_1(X1)|c5_1(X1)|ndr1_1(X1))). % 22.94/3.41 cnf(i_0_691, negated_conjecture, (c9_1(X1)|c2_1(X1)|ndr1_1(X1)|~ssSkC20)). % 22.94/3.41 cnf(i_0_697, negated_conjecture, (c10_1(X1)|ssSkC21|ndr1_1(X1))). % 22.94/3.41 cnf(i_0_698, negated_conjecture, (c3_1(X1)|ssSkC14|ndr1_1(X1))). % 22.94/3.41 cnf(i_0_706, negated_conjecture, (ssSkC24|c3_1(X1)|ndr1_1(X1)|~c1_1(X1))). % 22.94/3.41 cnf(i_0_731, negated_conjecture, (ssSkC9|ndr1_1(X1)|~c3_1(X1)|~c2_1(X1))). % 22.94/3.41 cnf(i_0_711, negated_conjecture, (c8_1(X1)|c5_1(X1)|ndr1_1(X1)|c8_0|~c3_0)). % 22.94/3.41 cnf(i_0_717, negated_conjecture, (c3_0|c8_1(X1)|c5_1(X1)|ndr1_1(X1)|~c1_0)). % 22.94/3.41 cnf(i_0_716, negated_conjecture, (c8_1(X1)|ndr1_1(X1)|c7_0|~c1_0)). % 22.94/3.41 cnf(i_0_702, negated_conjecture, (c8_1(X1)|ndr1_1(X1)|c10_0|~ssSkC19)). % 22.94/3.41 cnf(i_0_715, negated_conjecture, (c6_1(X1)|c5_0|ndr1_1(X1)|~c5_1(X1)|~ssSkC8)). % 22.94/3.41 cnf(i_0_737, negated_conjecture, (c10_1(X1)|c4_0|ndr1_1(X1)|~c5_1(X1)|~c6_0)). % 22.94/3.41 cnf(i_0_741, negated_conjecture, (c8_1(X1)|ndr1_1(X1)|~ssSkC9|~c10_1(X1)|~c10_0)). % 22.94/3.41 cnf(i_0_754, negated_conjecture, (c10_1(X1)|ndr1_1(X1)|~c3_0|~c4_0|~c9_1(X1))). % 22.94/3.41 cnf(i_0_714, negated_conjecture, (c6_1(X1)|ndr1_1(X1)|~ssSkC10|~c6_0)). % 22.94/3.41 cnf(i_0_747, negated_conjecture, (c3_0|c8_1(X1)|c7_0|~c9_1(X1)|~c1_1(X1))). % 22.94/3.41 cnf(i_0_764, negated_conjecture, (c2_1(X1)|c8_0|~c6_1(X1)|~c5_1(X1))). % 22.94/3.41 cnf(i_0_742, negated_conjecture, (c3_0|ndr1_1(X1)|~c7_1(X1)|~c8_0)). % 22.94/3.41 cnf(i_0_710, negated_conjecture, (c6_1(X1)|c10_2(X1,a203)|c1_1(X1)|ssSkC12)). % 22.94/3.41 cnf(i_0_709, negated_conjecture, (c6_1(X1)|c7_2(X1,a203)|c1_1(X1)|ssSkC12)). % 22.94/3.41 cnf(i_0_701, negated_conjecture, (c2_2(X1,a229)|c9_1(X1)|c2_1(X1)|~ssSkC20)). % 22.94/3.41 cnf(i_0_707, negated_conjecture, (c2_2(X1,a231)|c10_1(X1)|ssSkC21|~ssSkP5(X1))). % 22.94/3.41 cnf(i_0_708, negated_conjecture, (c3_1(X1)|ssSkC14|c9_2(X1,a211)|~ssSkP3(X1))). % 22.94/3.41 cnf(i_0_725, negated_conjecture, (ssSkC24|c3_1(X1)|c8_2(X1,a243)|~c1_1(X1))). % 22.94/3.41 cnf(i_0_730, negated_conjecture, (c6_1(X1)|c1_1(X1)|ssSkC12|~c3_2(X1,a203))). % 22.94/3.41 cnf(i_0_733, negated_conjecture, (ssSkC7|c3_1(X1)|c5_1(X1)|~c6_2(X1,a183))). % 22.94/3.41 cnf(i_0_732, negated_conjecture, (ssSkC7|c3_1(X1)|c5_1(X1)|~c2_2(X1,a183))). % 22.94/3.41 cnf(i_0_734, negated_conjecture, (ssSkC7|c3_1(X1)|c5_1(X1)|~c1_2(X1,a183))). % 22.94/3.41 cnf(i_0_712, negated_conjecture, (c9_1(X1)|c2_1(X1)|~ssSkC20|~c7_2(X1,a229))). % 22.94/3.41 cnf(i_0_726, negated_conjecture, (c10_1(X1)|ssSkC21|~c8_2(X1,a231)|~ssSkP5(X1))). % 22.94/3.41 cnf(i_0_727, negated_conjecture, (c10_1(X1)|ssSkC21|~c1_2(X1,a231)|~ssSkP5(X1))). % 22.94/3.41 cnf(i_0_728, negated_conjecture, (c3_1(X1)|ssSkC14|~c4_2(X1,a211)|~ssSkP3(X1))). % 22.94/3.41 cnf(i_0_729, negated_conjecture, (c3_1(X1)|ssSkC14|~c2_2(X1,a211)|~ssSkP3(X1))). % 22.94/3.41 cnf(i_0_751, negated_conjecture, (ssSkC24|c3_1(X1)|~c3_2(X1,a243)|~c1_1(X1))). % 22.94/3.41 cnf(i_0_750, negated_conjecture, (ssSkC24|c3_1(X1)|~c5_2(X1,a243)|~c1_1(X1))). % 22.94/3.41 cnf(i_0_769, negated_conjecture, (ssSkC9|~c3_1(X1)|~c10_2(X1,a193)|~c2_1(X1))). % 22.94/3.41 cnf(i_0_767, negated_conjecture, (ssSkC9|~c3_1(X1)|~c6_2(X1,a193)|~c2_1(X1))). % 22.94/3.41 cnf(i_0_768, negated_conjecture, (ssSkC9|~c3_1(X1)|~c3_2(X1,a193)|~c2_1(X1))). % 22.94/3.41 cnf(i_0_718, negated_conjecture, (c8_2(a206,X1)|c9_2(a206,X1)|ssSkC13|~ndr1_1(a206))). % 22.94/3.41 cnf(i_0_748, negated_conjecture, (c4_2(a200,X1)|ssSkC11|~c6_2(a200,X1))). % 22.94/3.41 cnf(i_0_765, negated_conjecture, (ssSkC16|~c4_2(a215,X1)|~c5_2(a215,X1)|~ndr1_1(a215))). % 22.94/3.41 cnf(i_0_746, negated_conjecture, (c6_2(X1,a154)|c3_0|c8_1(X1)|c5_1(X1)|~c1_0)). % 22.94/3.41 cnf(i_0_745, negated_conjecture, (c6_2(X1,a156)|c8_1(X1)|c7_0|~ssSkP0(X1)|~c1_0)). % 22.94/3.41 cnf(i_0_744, negated_conjecture, (c3_2(X1,a156)|c8_1(X1)|c7_0|~ssSkP0(X1)|~c1_0)). % 22.94/3.41 cnf(i_0_713, negated_conjecture, (c10_2(X1,a227)|c8_1(X1)|c10_0|~ssSkP4(X1)|~ssSkC19)). % 22.94/3.41 cnf(i_0_743, negated_conjecture, (c6_1(X1)|c9_2(X1,a186)|c5_0|~c5_1(X1)|~ssSkC8)). % 22.94/3.41 cnf(i_0_755, negated_conjecture, (c9_2(X1,a208)|c10_1(X1)|c4_0|~c5_1(X1)|~c6_0)). % 22.94/3.41 cnf(i_0_756, negated_conjecture, (c9_2(X1,a194)|c8_1(X1)|~ssSkC9|~c10_1(X1)|~c10_0)). % 22.94/3.41 cnf(i_0_739, negated_conjecture, (c6_1(X1)|c10_2(X1,a199)|~ssSkC10|~ssSkP2(X1)|~c6_0)). % 22.94/3.41 cnf(i_0_738, negated_conjecture, (c6_1(X1)|c7_2(X1,a199)|~ssSkC10|~ssSkP2(X1)|~c6_0)). % 22.94/3.41 cnf(i_0_740, negated_conjecture, (c6_1(X1)|c9_2(X1,a199)|~ssSkC10|~ssSkP2(X1)|~c6_0)). % 22.94/3.41 cnf(i_0_759, negated_conjecture, (c3_2(X1,a188)|c3_0|~ssSkP1(X1)|~c7_1(X1)|~c8_0)). % 22.94/3.41 cnf(i_0_758, negated_conjecture, (c9_2(X1,a188)|c3_0|~ssSkP1(X1)|~c7_1(X1)|~c8_0)). % 22.94/3.41 cnf(i_0_757, negated_conjecture, (c1_2(X1,a188)|c3_0|~ssSkP1(X1)|~c7_1(X1)|~c8_0)). % 22.94/3.41 cnf(i_0_753, negated_conjecture, (c8_1(X1)|c5_1(X1)|c8_0|~c9_2(X1,a256)|~c3_0)). % 22.94/3.41 cnf(i_0_752, negated_conjecture, (c8_1(X1)|c5_1(X1)|c8_0|~c8_2(X1,a256)|~c3_0)). % 22.94/3.41 cnf(i_0_762, negated_conjecture, (c3_0|c8_1(X1)|c5_1(X1)|~c10_2(X1,a154)|~c1_0)). % 22.94/3.41 cnf(i_0_763, negated_conjecture, (c3_0|c8_1(X1)|c5_1(X1)|~c3_2(X1,a154)|~c1_0)). % 22.94/3.41 cnf(i_0_736, negated_conjecture, (c8_1(X1)|c10_0|~c7_2(X1,a227)|~ssSkP4(X1)|~ssSkC19)). % 22.94/3.41 cnf(i_0_735, negated_conjecture, (c8_1(X1)|c10_0|~c1_2(X1,a227)|~ssSkP4(X1)|~ssSkC19)). % 22.94/3.41 cnf(i_0_760, negated_conjecture, (c6_1(X1)|c5_0|~c3_2(X1,a186)|~c5_1(X1)|~ssSkC8)). % 22.94/3.41 cnf(i_0_761, negated_conjecture, (c6_1(X1)|c5_0|~c2_2(X1,a186)|~c5_1(X1)|~ssSkC8)). % 22.94/3.41 cnf(i_0_766, negated_conjecture, (ssSkC3|~c6_2(a169,X1)|~c10_2(a169,X1)|~ndr1_1(a169))). % 22.94/3.41 cnf(i_0_770, negated_conjecture, (c10_1(X1)|c4_0|~c4_2(X1,a208)|~c5_1(X1)|~c6_0)). % 22.94/3.41 cnf(i_0_771, negated_conjecture, (c8_1(X1)|~ssSkC9|~c3_2(X1,a194)|~c10_1(X1)|~c10_0)). % 22.94/3.41 cnf(i_0_772, negated_conjecture, (c8_1(X1)|~ssSkC9|~c1_2(X1,a194)|~c10_1(X1)|~c10_0)). % 22.94/3.41 cnf(i_0_783, negated_conjecture, (c10_1(X1)|~c9_2(X1,a220)|~c3_0|~c4_0|~c9_1(X1))). % 22.94/3.41 cnf(i_0_782, negated_conjecture, (c10_1(X1)|~c4_2(X1,a220)|~c3_0|~c4_0|~c9_1(X1))). % 22.94/3.41 cnf(i_0_781, negated_conjecture, (c10_1(X1)|~c2_2(X1,a220)|~c3_0|~c4_0|~c9_1(X1))). % 22.94/3.41 cnf(i_0_779, negated_conjecture, (c3_2(a171,X1)|c7_2(a171,X1)|ssSkC4|~c10_2(a171,X1)|~ndr1_1(a171))). % 22.94/3.41 cnf(i_0_774, negated_conjecture, (c1_2(a261,X1)|c8_2(a261,X1)|ssSkC26|~c7_2(a261,X1)|~ndr1_1(a261))). % 22.94/3.41 cnf(i_0_775, negated_conjecture, (c8_2(a224,X1)|c4_2(a224,X1)|ssSkC19|~c9_2(a224,X1))). % 22.94/3.41 cnf(i_0_776, negated_conjecture, (c9_2(a212,X1)|c7_2(a212,X1)|ssSkC15|~c5_2(a212,X1))). % 22.94/3.41 cnf(i_0_777, negated_conjecture, (c2_2(a206,X1)|c6_2(a206,X1)|ssSkC13|~c4_2(a206,X1)|~ndr1_1(a206))). % 22.94/3.41 cnf(i_0_778, negated_conjecture, (c4_2(a174,X1)|c6_2(a174,X1)|ssSkC5|~c8_2(a174,X1)|~ndr1_1(a174))). % 22.94/3.41 cnf(i_0_787, negated_conjecture, (c2_2(a162,X1)|c8_0|~c1_2(a162,X1)|~c3_2(a162,X1)|~ndr1_1(a162))). % 22.94/3.41 cnf(i_0_788, negated_conjecture, (c2_2(a261,X1)|ssSkC26|~c1_2(a261,X1)|~c7_2(a261,X1)|~ndr1_1(a261))). % 22.94/3.41 cnf(i_0_789, negated_conjecture, (c3_2(a239,X1)|ssSkC23|~c2_2(a239,X1)|~c10_2(a239,X1)|~ndr1_1(a239))). % 22.94/3.41 cnf(i_0_791, negated_conjecture, (c1_2(a149,X1)|ssSkC1|~c4_2(a149,X1)|~c7_2(a149,X1))). % 22.94/3.41 cnf(i_0_798, negated_conjecture, (c3_2(a157,X1)|~c8_2(a157,X1)|~c9_2(a157,X1)|~ndr1_1(a157)|~c7_0)). % 22.94/3.41 cnf(i_0_785, negated_conjecture, (c5_2(a172,X1)|~c8_2(a172,X1)|~c4_2(a172,X1)|~ndr1_1(a172)|~ssSkC4)). % 22.94/3.41 cnf(i_0_795, negated_conjecture, (c6_0|~c2_2(a177,X1)|~c4_2(a177,X1)|~c6_2(a177,X1))). % 22.94/3.41 cnf(i_0_799, negated_conjecture, (ssSkC15|~c8_2(a212,X1)|~c4_2(a212,X1)|~c5_2(a212,X1))). % 22.94/3.41 cnf(i_0_800, negated_conjecture, (ssSkC8|~c8_2(a185,X1)|~c9_2(a185,X1)|~c10_2(a185,X1)|~ndr1_1(a185))). % 22.94/3.41 cnf(i_0_801, negated_conjecture, (ssSkC3|~c1_2(a169,X1)|~c8_2(a169,X1)|~c9_2(a169,X1)|~ndr1_1(a169))). % 22.94/3.41 cnf(i_0_780, negated_conjecture, (c5_2(a246,X1)|c7_2(a246,X1)|c6_2(a246,X1)|c10_0|~c4_0|~ndr1_1(a246))). % 22.94/3.41 cnf(i_0_784, negated_conjecture, (c1_2(a216,X1)|c3_2(a216,X1)|c10_2(a216,X1)|~c10_0|~ssSkC16)). % 22.94/3.41 cnf(i_0_786, negated_conjecture, (c1_2(a167,X1)|c10_2(a167,X1)|c10_0|c6_0|~c9_2(a167,X1)|~ndr1_1(a167))). % 22.94/3.41 cnf(i_0_773, negated_conjecture, (c1_2(X1,X2)|c8_2(X1,X2)|c7_2(X1,X2)|c1_0|c7_0|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_796, negated_conjecture, (c5_2(a165,X1)|c3_2(a165,X1)|c9_0|~c2_2(a165,X1)|~c2_0)). % 22.94/3.41 cnf(i_0_797, negated_conjecture, (c2_2(a160,X1)|c6_2(a160,X1)|~c4_2(a160,X1)|~ssSkC2|~c4_0|~ndr1_1(a160))). % 22.94/3.41 cnf(i_0_792, negated_conjecture, (c1_2(a237,X1)|c3_2(a237,X1)|~c2_2(a237,X1)|~ssSkC22|~c9_0)). % 22.94/3.41 cnf(i_0_793, negated_conjecture, (c8_2(a216,X1)|c5_2(a216,X1)|~c6_2(a216,X1)|~c10_0|~ssSkC16)). % 22.94/3.41 cnf(i_0_790, negated_conjecture, (c5_2(X1,X2)|c7_2(X1,a159)|c10_2(X1,X2)|ssSkC2|c2_1(X1)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_805, negated_conjecture, (c9_2(a245,X1)|c7_0|~c7_2(a245,X1)|~c10_2(a245,X1)|~ndr1_1(a245)|~c9_0)). % 22.94/3.41 cnf(i_0_804, negated_conjecture, (c10_2(a246,X1)|c10_0|~c5_2(a246,X1)|~c9_2(a246,X1)|~c4_0|~ndr1_1(a246))). % 22.94/3.41 cnf(i_0_807, negated_conjecture, (c8_2(a165,X1)|c9_0|~c4_2(a165,X1)|~c10_2(a165,X1)|~c2_0)). % 22.94/3.41 cnf(i_0_794, negated_conjecture, (c7_2(a204,X1)|~c8_2(a204,X1)|~c3_2(a204,X1)|~ssSkC12|~ssSkC11)). % 22.94/3.41 cnf(i_0_812, negated_conjecture, (c2_2(a163,X1)|~c4_2(a163,X1)|~c6_2(a163,X1)|~c9_0|~c1_0)). % 22.94/3.41 cnf(i_0_806, negated_conjecture, (c9_0|~c1_2(a240,X1)|~c5_2(a240,X1)|~c9_2(a240,X1)|~ssSkC23)). % 22.94/3.41 cnf(i_0_813, negated_conjecture, (~c2_2(a152,X1)|~c4_2(a152,X1)|~c10_2(a152,X1)|~c4_0|~ssSkC1)). % 22.94/3.41 cnf(i_0_811, negated_conjecture, (~c9_2(a232,X1)|~c3_2(a232,X1)|~c6_2(a232,X1)|~ssSkC21|~c10_0)). % 22.94/3.41 cnf(i_0_810, negated_conjecture, (~c4_2(a237,X1)|~c5_2(a237,X1)|~c6_2(a237,X1)|~ssSkC22|~c9_0)). % 22.94/3.41 cnf(i_0_814, negated_conjecture, (c8_2(X1,X2)|c4_1(X1)|c10_0|~c10_2(X1,X2)|~c4_0|~c9_1(X1)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_815, negated_conjecture, (c6_1(X1)|c7_2(X1,X2)|c5_0|~c3_2(X1,X2)|~c1_1(X1)|~ndr1_1(X1)|~c9_0)). % 22.94/3.41 cnf(i_0_802, negated_conjecture, (c5_2(X1,X2)|c10_2(X1,X2)|ssSkC2|c2_1(X1)|~c8_2(X1,a159)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_808, negated_conjecture, (c1_2(X1,a218)|c10_1(X1)|ssSkC17|~c9_2(X1,X2)|~c7_2(X1,X2)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_818, negated_conjecture, (c10_1(X1)|ssSkC17|~c5_2(X1,a218)|~c9_2(X1,X2)|~c7_2(X1,X2)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_817, negated_conjecture, (ssSkC20|c8_1(X1)|~c1_2(X1,a228)|~c8_2(X1,X2)|~c10_2(X1,X2)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_803, negated_conjecture, (c5_2(X1,X2)|c10_2(X1,X2)|ssSkC2|c2_1(X1)|~c5_2(X1,a159)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_809, negated_conjecture, (c7_2(X1,a218)|c10_1(X1)|ssSkC17|~c9_2(X1,X2)|~c7_2(X1,X2)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_816, negated_conjecture, (ssSkC20|c8_1(X1)|~c8_2(X1,X2)|~c10_2(X1,a228)|~c10_2(X1,X2)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_820, negated_conjecture, (c3_1(X1)|c3_2(X1,X2)|c7_2(X1,X2)|c10_2(X1,X2)|c9_0|~c10_1(X1)|~ndr1_1(X1)|~c6_0)). % 22.94/3.41 cnf(i_0_822, negated_conjecture, (ssSkC10|c2_2(X1,X2)|c6_2(X1,X2)|c10_2(X1,X2)|~c7_2(X1,a197)|~c9_1(X1)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_819, negated_conjecture, (c1_2(X1,X2)|c6_2(X1,X3)|c10_2(X1,X2)|~c10_2(X1,X3)|~c5_0|~ndr1_1(X1)|~c2_0)). % 22.94/3.41 cnf(i_0_824, negated_conjecture, (ssSkC10|c2_2(X1,X2)|c6_2(X1,X2)|c10_2(X1,X2)|~c5_2(X1,a197)|~c9_1(X1)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_823, negated_conjecture, (ssSkC10|c2_2(X1,X2)|c6_2(X1,X2)|c10_2(X1,X2)|~c8_2(X1,a197)|~c9_1(X1)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_833, negated_conjecture, (c1_2(X1,X2)|c10_1(X1)|~c4_2(X1,X2)|~c6_2(X1,X2)|~c4_0|~c7_1(X1)|~ndr1_1(X1)|~c2_0)). % 22.94/3.41 cnf(i_0_831, negated_conjecture, (c8_2(X1,X2)|ssSkC22|~c2_2(X1,X2)|~c10_2(X1,a236)|~c10_2(X1,X2)|~c7_1(X1)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_821, negated_conjecture, (c6_1(a170)|c5_2(X1,X2)|c9_2(X1,X2)|c3_2(X1,X3)|c6_2(X1,X2)|~c2_1(X1)|~ndr1_1(X1)|~ssSkC3)). % 22.94/3.41 cnf(i_0_830, negated_conjecture, (c8_2(X1,X2)|ssSkC22|~c2_2(X1,X2)|~c6_2(X1,a236)|~c10_2(X1,X2)|~c7_1(X1)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_825, negated_conjecture, (c1_2(X1,X2)|c9_2(X1,X2)|c10_1(X1)|c10_2(X1,a223)|~c7_2(X1,X2)|~ndr1_1(X1)|~ssSkC18|~c7_0)). % 22.94/3.41 cnf(i_0_828, negated_conjecture, (c1_2(X1,X2)|c9_2(X1,X2)|c10_1(X1)|~c7_2(X1,X2)|~c6_2(X1,a223)|~ndr1_1(X1)|~ssSkC18|~c7_0)). % 22.94/3.41 cnf(i_0_837, negated_conjecture, (c4_0|c8_1(a235)|~c4_2(X1,X2)|~c5_2(X1,X2)|~c10_2(X1,X2)|~c5_1(X1)|~c7_1(X1)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_839, negated_conjecture, (c9_2(X1,X2)|~ssSkC7|~c1_2(X1,X2)|~c7_2(X1,a184)|~c6_2(X1,X2)|~c4_1(X1)|~ndr1_1(X1)|~c7_0)). % 22.94/3.41 cnf(i_0_840, negated_conjecture, (c9_2(X1,X2)|~ssSkC7|~c1_2(X1,X2)|~c5_2(X1,a184)|~c6_2(X1,X2)|~c4_1(X1)|~ndr1_1(X1)|~c7_0)). % 22.94/3.41 cnf(i_0_841, negated_conjecture, (c3_0|c9_0|~c2_2(X1,X2)|~c9_2(X1,X2)|~c7_2(X1,X2)|~c10_2(X1,a161)|~c7_1(X1)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_842, negated_conjecture, (c3_0|c9_0|~c2_2(X1,X2)|~c9_2(X1,X2)|~c3_2(X1,a161)|~c7_2(X1,X2)|~c7_1(X1)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_843, negated_conjecture, (c3_0|c9_0|~c2_2(X1,X2)|~c4_2(X1,a161)|~c9_2(X1,X2)|~c7_2(X1,X2)|~c7_1(X1)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_829, negated_conjecture, (c8_2(X1,X2)|ssSkC22|~c8_2(X1,a236)|~c2_2(X1,X2)|~c10_2(X1,X2)|~c7_1(X1)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_826, negated_conjecture, (c1_2(X1,X2)|c9_2(X1,a223)|c9_2(X1,X2)|c10_1(X1)|~c7_2(X1,X2)|~ndr1_1(X1)|~ssSkC18|~c7_0)). % 22.94/3.41 cnf(i_0_832, negated_conjecture, (c9_2(X1,a184)|c9_2(X1,X2)|~ssSkC7|~c1_2(X1,X2)|~c6_2(X1,X2)|~c4_1(X1)|~ndr1_1(X1)|~c7_0)). % 22.94/3.41 cnf(i_0_846, negated_conjecture, (c4_0|~c4_2(X1,X2)|~c5_2(X1,X2)|~c10_2(X1,X2)|~c5_1(a235)|~c5_1(X1)|~c7_1(X1)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_827, negated_conjecture, (c5_2(X1,X2)|c9_2(X1,X2)|c3_2(X1,X3)|c6_2(X1,X2)|~c8_1(a170)|~c2_1(X1)|~ndr1_1(X1)|~ssSkC3)). % 22.94/3.41 cnf(i_0_834, negated_conjecture, (c3_1(X1)|c6_2(X2,X3)|c2_1(X2)|~c1_2(X2,X3)|~c4_2(X2,X3)|~c9_1(X1)|~c2_1(X1)|~ndr1_1(X2))). % 22.94/3.41 cnf(i_0_848, negated_conjecture, (c3_1(X1)|c8_2(X1,X2)|c5_2(X3,a221)|c5_1(X1)|~c4_2(X1,X2)|~c7_2(X1,X2)|~c7_1(X3)|~ndr1_1(X1)|~c8_0)). % 22.94/3.41 cnf(i_0_847, negated_conjecture, (c3_1(X1)|c1_2(X2,a221)|c8_2(X1,X3)|c5_1(X1)|~c4_2(X1,X3)|~c7_2(X1,X3)|~c7_1(X2)|~ndr1_1(X1)|~c8_0)). % 22.94/3.41 cnf(i_0_838, negated_conjecture, (c3_1(X1)|c8_2(X1,X2)|c5_1(X1)|ndr1_1(X3)|~c4_2(X1,X2)|~c7_2(X1,X2)|~c7_1(X3)|~ndr1_1(X1)|~c8_0)). % 22.94/3.41 cnf(i_0_851, negated_conjecture, (c3_1(X1)|c8_2(X1,X2)|c5_1(X1)|~c8_2(X3,a221)|~c4_2(X1,X2)|~c7_2(X1,X2)|~c7_1(X3)|~ndr1_1(X1)|~c8_0)). % 22.94/3.41 cnf(i_0_836, negated_conjecture, (c6_1(X1)|c9_2(X1,X2)|c3_2(X1,X3)|c6_2(X1,X3)|c1_1(a253)|c10_0|~c1_2(X1,X2)|~c8_2(X1,X3)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_835, negated_conjecture, (c6_1(X1)|c9_2(X1,X2)|c3_2(X1,X3)|c6_2(X1,X3)|c9_1(a253)|c10_0|~c1_2(X1,X2)|~c8_2(X1,X3)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_844, negated_conjecture, (c6_1(X1)|c9_2(X1,X2)|c3_2(X1,X3)|c6_2(X1,X3)|c10_0|~c1_2(X1,X2)|~c8_2(X1,X3)|~c5_1(a253)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_852, negated_conjecture, (c6_2(X1,a250)|c10_2(X1,X2)|c1_1(X3)|~c5_2(X1,X2)|~c3_2(X1,X2)|~c10_1(X3)|~c9_1(X1)|~c9_1(X3)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_853, negated_conjecture, (c2_2(X1,a250)|c10_2(X1,X2)|c1_1(X3)|~c5_2(X1,X2)|~c3_2(X1,X2)|~c10_1(X3)|~c9_1(X1)|~c9_1(X3)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_845, negated_conjecture, (c4_2(X1,X2)|c4_2(X1,X3)|c5_2(X1,a244)|c7_2(X1,X2)|c7_2(X1,X3)|~ssSkC24|~c8_2(X1,X3)|~c9_2(X1,X2)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_854, negated_conjecture, (c6_1(X1)|c8_2(X1,X2)|c6_2(X1,X2)|c9_1(X3)|c8_1(X4)|c7_1(X3)|ndr1_1(X4)|~c1_2(X1,X2)|~c9_1(X1)|~c2_1(X3)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_859, negated_conjecture, (c5_2(X1,X2)|c7_2(X1,X3)|~c4_2(X1,X2)|~c9_2(X1,X3)|~c9_2(X1,X2)|~c10_2(X1,X3)|~c8_1(X1)|~ndr1_1(X1)|~c7_0|~c6_0)). % 22.94/3.41 cnf(i_0_849, negated_conjecture, (c4_2(X1,X2)|c4_2(X1,X3)|c7_2(X1,X2)|c7_2(X1,X3)|~ssSkC24|~c8_2(X1,X3)|~c9_2(X1,X2)|~c3_2(X1,a244)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_858, negated_conjecture, (c4_2(X1,X2)|c10_2(X1,a209)|c7_0|~c8_2(X1,X3)|~c2_2(X1,X3)|~c4_2(X1,X3)|~c9_2(X1,X2)|~c10_2(X1,X2)|~ndr1_1(X1)|~c10_0)). % 22.94/3.41 cnf(i_0_863, negated_conjecture, (c4_2(X1,X2)|c7_0|~c8_2(X1,X3)|~c2_2(X1,X3)|~c4_2(X1,a209)|~c4_2(X1,X3)|~c9_2(X1,X2)|~c10_2(X1,X2)|~ndr1_1(X1)|~c10_0)). % 22.94/3.41 cnf(i_0_862, negated_conjecture, (c4_2(X1,X2)|c7_0|~c8_2(X1,X3)|~c2_2(X1,a209)|~c2_2(X1,X3)|~c4_2(X1,X3)|~c9_2(X1,X2)|~c10_2(X1,X2)|~ndr1_1(X1)|~c10_0)). % 22.94/3.41 cnf(i_0_850, negated_conjecture, (c4_2(X1,X2)|c4_2(X1,X3)|c7_2(X1,X2)|c7_2(X1,X3)|~ssSkC24|~c8_2(X1,a244)|~c8_2(X1,X3)|~c9_2(X1,X2)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_864, negated_conjecture, (c6_1(X1)|c6_2(X1,X2)|c8_1(X1)|c1_1(a189)|~c3_1(X3)|~c8_2(X3,X4)|~c2_2(X3,X4)|~c10_1(X3)|~c10_2(X1,X2)|~ndr1_1(X1)|~ndr1_1(X3))). % 22.94/3.41 cnf(i_0_866, negated_conjecture, (c6_1(X1)|c6_2(X1,X2)|c8_1(X1)|~c3_1(X3)|~c8_2(X3,X4)|~c2_2(X3,X4)|~c10_1(X3)|~c10_2(X1,X2)|~c5_1(a189)|~ndr1_1(X1)|~ndr1_1(X3))). % 22.94/3.41 cnf(i_0_867, negated_conjecture, (c6_1(X1)|c6_2(X1,X2)|c8_1(X1)|~c3_1(a189)|~c3_1(X3)|~c8_2(X3,X4)|~c2_2(X3,X4)|~c10_1(X3)|~c10_2(X1,X2)|~ndr1_1(X1)|~ndr1_1(X3))). % 22.94/3.41 cnf(i_0_855, negated_conjecture, (c3_2(X1,X2)|c3_2(X1,X3)|c7_2(X1,X3)|c10_2(X1,X3)|c8_1(X4)|c4_1(X4)|~c9_2(X1,a182)|~c6_2(X1,X2)|~c7_1(X4)|~ndr1_1(X1)|~ssSkC6)). % 22.94/3.41 cnf(i_0_856, negated_conjecture, (c3_2(X1,X2)|c3_2(X1,X3)|c7_2(X1,X3)|c10_2(X1,X3)|c8_1(X4)|c4_1(X4)|~c2_2(X1,a182)|~c6_2(X1,X2)|~c7_1(X4)|~ndr1_1(X1)|~ssSkC6)). % 22.94/3.41 cnf(i_0_857, negated_conjecture, (c6_1(X1)|c8_2(X1,X2)|c9_2(X3,a255)|c6_2(X1,X2)|c9_1(X4)|c8_1(X3)|c7_1(X4)|~c1_2(X1,X2)|~c9_1(X1)|~c2_1(X4)|~ssSkP6(X3)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_861, negated_conjecture, (c6_1(X1)|c8_2(X1,X2)|c6_2(X1,X2)|c9_1(X3)|c8_1(X4)|c7_1(X3)|~c1_2(X1,X2)|~c4_2(X4,a255)|~c9_1(X1)|~c2_1(X3)|~ssSkP6(X4)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_860, negated_conjecture, (c6_1(X1)|c8_2(X1,X2)|c6_2(X1,X2)|c9_1(X3)|c8_1(X4)|c7_1(X3)|~c1_2(X1,X2)|~c6_2(X4,a255)|~c9_1(X1)|~c2_1(X3)|~ssSkP6(X4)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_865, negated_conjecture, (c5_2(X1,X2)|c9_2(X1,X2)|c3_2(a170,X3)|c3_2(X1,X4)|c6_2(X1,X2)|~c9_2(a170,X3)|~c10_2(a170,X3)|~c2_1(X1)|~ndr1_1(a170)|~ndr1_1(X1)|~ssSkC3)). % 22.94/3.41 cnf(i_0_869, negated_conjecture, (c9_2(X1,X2)|c7_2(X3,X4)|c10_1(X3)|c6_2(X3,X4)|c5_1(X1)|~c3_2(X3,X4)|~c3_2(X1,X2)|~c10_1(X1)|~c6_2(X1,X2)|~c5_1(X3)|~ndr1_1(X3)|~ndr1_1(X1)|~c8_0)). % 22.94/3.41 cnf(i_0_868, negated_conjecture, (c8_2(X1,X2)|c8_2(X1,X3)|c9_2(X4,X5)|c7_2(X4,X5)|c7_2(X1,X3)|c3_0|c9_1(X4)|~c7_2(X1,X2)|~c6_2(X4,X5)|~c5_1(X4)|~c7_1(X1)|~ndr1_1(X1)|~ndr1_1(X4))). % 22.94/3.41 cnf(i_0_871, negated_conjecture, (c3_1(X1)|c3_1(X2)|c8_2(X1,X3)|c4_2(X1,X3)|c5_2(X2,a158)|c9_2(X2,X4)|c6_2(X1,X3)|c10_2(X2,X4)|~c2_2(X1,X5)|~c4_2(X1,X5)|~c3_2(X2,X4)|~c6_2(X1,X5)|~ndr1_1(X2)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_870, negated_conjecture, (c3_1(X1)|c3_1(X2)|c8_2(X1,X3)|c4_2(X1,X3)|c9_2(X2,a158)|c9_2(X2,X4)|c6_2(X1,X3)|c10_2(X2,X4)|~c2_2(X1,X5)|~c4_2(X1,X5)|~c3_2(X2,X4)|~c6_2(X1,X5)|~ndr1_1(X2)|~ndr1_1(X1))). % 22.94/3.41 cnf(i_0_872, negated_conjecture, (c3_1(X1)|c3_1(X2)|c8_2(X1,X3)|c4_2(X1,X3)|c9_2(X2,X4)|c6_2(X1,X3)|c10_2(X2,X4)|~c2_2(X1,X5)|~c4_2(X1,X5)|~c3_2(X2,X4)|~c6_2(X2,a158)|~c6_2(X1,X5)|~ndr1_1(X2)|~ndr1_1(X1))). % 22.94/3.41 # End listing active clauses. There is an equivalent clause to each of these in the clausification! % 22.94/3.41 # Begin printing tableau % 22.94/3.41 # Found 6 steps % 22.94/3.41 cnf(i_0_829, negated_conjecture, (c8_2(a204,a231)|ssSkC22|~c8_2(a204,a236)|~c2_2(a204,a231)|~c10_2(a204,a231)|~c7_1(a204)|~ndr1_1(a204)), inference(start_rule)). % 22.94/3.41 cnf(i_0_1242, plain, (c8_2(a204,a231)), inference(extension_rule, [i_0_794])). % 22.94/3.41 cnf(i_0_917355, plain, (c7_2(a204,a231)), inference(extension_rule, [i_0_843])). % 22.94/3.41 cnf(i_0_917464, plain, (c3_0), inference(extension_rule, [i_0_646])). % 22.94/3.41 cnf(i_0_917465, plain, (c9_0), inference(extension_rule, [i_0_694])). % 22.94/3.41 cnf(i_0_917466, plain, (~c2_2(a204,a231)), inference(extension_rule, [i_0_707])). % 22.94/3.41 # End printing tableau % 22.94/3.41 # SZS output end % 22.94/3.41 # Branches closed with saturation will be marked with an "s" % 22.94/3.42 # Child (5231) has found a proof. % 22.94/3.42 % 23.74/3.42 # Proof search is over... % 23.74/3.42 # Freeing feature tree %------------------------------------------------------------------------------