%------------------------------------------------------------------------------ % File : Etableau---0.67 % Problem : SYN544+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 : n024.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:12:20 EDT 2022 % Result : CounterSatisfiable 30.69s 4.39s % Output : CNFRefutation 30.69s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN544+1 : TPTP v8.1.0. Released v2.1.0. % 0.03/0.13 % Command : etableau --auto --tsmdo --quicksat=10000 --tableau=1 --tableau-saturation=1 -s -p --tableau-cores=8 --cpu-limit=%d %s % 0.12/0.34 % Computer : n024.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Mon Jul 11 15:00:43 EDT 2022 % 0.12/0.34 % CPUTime : % 0.19/0.51 # No SInE strategy applied % 0.19/0.51 # Auto-Mode selected heuristic G_E___208_C02AMC_F1_SE_CS_SP_PS_S5PRR_RG_S04AN % 0.19/0.51 # and selection function SelectComplexExceptUniqMaxHorn. % 0.19/0.51 # % 0.19/0.51 # Presaturation interreduction done % 0.19/0.51 # Number of axioms: 919 Number of unprocessed: 576 % 0.19/0.51 # Tableaux proof search. % 0.19/0.51 # APR header successfully linked. % 0.19/0.51 # Hello from C++ % 0.19/0.54 # The folding up rule is enabled... % 0.19/0.54 # Local unification is enabled... % 0.19/0.54 # Any saturation attempts will use folding labels... % 0.19/0.54 # 576 beginning clauses after preprocessing and clausification % 0.19/0.54 # Creating start rules for all 387 conjectures. % 0.19/0.54 # There are 387 start rule candidates: % 0.19/0.54 # Found 23 unit axioms. % 0.19/0.54 # Unsuccessfully attempted saturation on 1 start tableaux, moving on. % 0.19/0.54 # 387 start rule tableaux created. % 0.19/0.54 # 553 extension rule candidate clauses % 0.19/0.54 # 23 unit axiom clauses % 0.19/0.54 % 0.19/0.54 # Requested 8, 32 cores available to the main process. % 30.69/4.38 # 9650 Satisfiable branch % 30.69/4.39 # Satisfiable branch found. % 30.69/4.39 # There were 1 total branch saturation attempts. % 30.69/4.39 # There were 0 of these attempts blocked. % 30.69/4.39 # There were 0 deferred branch saturation attempts. % 30.69/4.39 # There were 0 free duplicated saturations. % 30.69/4.39 # There were 0 total successful branch saturations. % 30.69/4.39 # There were 0 successful branch saturations in interreduction. % 30.69/4.39 # There were 0 successful branch saturations on the branch. % 30.69/4.39 # There were 0 successful branch saturations after the branch. % 30.69/4.39 # SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 30.69/4.39 # SZS output start for /export/starexec/sandbox/benchmark/theBenchmark.p % 30.69/4.39 # Begin clausification derivation % 30.69/4.39 % 30.69/4.39 # End clausification derivation % 30.69/4.39 # Begin listing active clauses obtained from FOF to CNF conversion % 30.69/4.39 cnf(i_0_26, negated_conjecture, (ndr1_0)). % 30.69/4.39 cnf(i_0_314, negated_conjecture, (c4_0)). % 30.69/4.39 cnf(i_0_315, negated_conjecture, (c6_0)). % 30.69/4.39 cnf(i_0_25, negated_conjecture, (c5_1(a136))). % 30.69/4.39 cnf(i_0_23, negated_conjecture, (ndr1_1(a136))). % 30.69/4.39 cnf(i_0_22, negated_conjecture, (c1_2(a136,a137))). % 30.69/4.39 cnf(i_0_21, negated_conjecture, (c3_2(a136,a137))). % 30.69/4.39 cnf(i_0_20, negated_conjecture, (c5_2(a136,a137))). % 30.69/4.39 cnf(i_0_616, negated_conjecture, (c7_0)). % 30.69/4.39 cnf(i_0_101, negated_conjecture, (ndr1_1(a122))). % 30.69/4.39 cnf(i_0_97, negated_conjecture, (c8_1(a122))). % 30.69/4.39 cnf(i_0_126, negated_conjecture, (c8_1(a117))). % 30.69/4.39 cnf(i_0_100, negated_conjecture, (c5_2(a122,a123))). % 30.69/4.39 cnf(i_0_575, negated_conjecture, (c5_1(a51))). % 30.69/4.39 cnf(i_0_502, negated_conjecture, (c3_1(a59))). % 30.69/4.39 cnf(i_0_3, negated_conjecture, (~c2_0)). % 30.69/4.39 cnf(i_0_1, negated_conjecture, (~c3_0)). % 30.69/4.39 cnf(i_0_96, negated_conjecture, (~c1_1(a122))). % 30.69/4.39 cnf(i_0_127, negated_conjecture, (~c2_1(a117))). % 30.69/4.39 cnf(i_0_99, negated_conjecture, (~c1_2(a122,a123))). % 30.69/4.39 cnf(i_0_98, negated_conjecture, (~c3_2(a122,a123))). % 30.69/4.39 cnf(i_0_574, negated_conjecture, (~c7_1(a51))). % 30.69/4.39 cnf(i_0_503, negated_conjecture, (~c4_1(a59))). % 30.69/4.39 cnf(i_0_570, negated_conjecture, (epred5_0|~c5_0)). % 30.69/4.39 cnf(i_0_378, negated_conjecture, (~c6_1(a81)|~c1_0)). % 30.69/4.39 cnf(i_0_585, negated_conjecture, (c8_0|~c6_1(a47))). % 30.69/4.39 cnf(i_0_377, negated_conjecture, (c7_1(a81)|~c1_0)). % 30.69/4.39 cnf(i_0_382, negated_conjecture, (ndr1_1(a81)|~c1_0)). % 30.69/4.39 cnf(i_0_584, negated_conjecture, (c8_0|ndr1_1(a47))). % 30.69/4.39 cnf(i_0_108, negated_conjecture, (c5_1(a121)|~c5_1(a120))). % 30.69/4.39 cnf(i_0_586, negated_conjecture, (c8_0|~c1_2(a47,a48))). % 30.69/4.39 cnf(i_0_688, negated_conjecture, (~c8_0|~c2_1(a16))). % 30.69/4.39 cnf(i_0_687, negated_conjecture, (~c8_1(a16)|~c8_0)). % 30.69/4.39 cnf(i_0_582, negated_conjecture, (c8_0|~c1_2(a47,a49))). % 30.69/4.39 cnf(i_0_588, negated_conjecture, (c8_0|~c2_2(a47,a48))). % 30.69/4.39 cnf(i_0_583, negated_conjecture, (c8_0|~c2_2(a47,a49))). % 30.69/4.39 cnf(i_0_896, plain, (~epred4_0|~c4_1(a35)|~c1_1(a37))). % 30.69/4.39 cnf(i_0_901, plain, (~epred4_0|~c6_1(a37)|~c4_1(a35))). % 30.69/4.39 cnf(i_0_622, negated_conjecture, (epred4_0|~c4_2(a39,a40))). % 30.69/4.39 cnf(i_0_619, negated_conjecture, (epred4_0|~c5_2(a39,a41))). % 30.69/4.39 cnf(i_0_617, negated_conjecture, (epred4_0|~c2_2(a39,a41))). % 30.69/4.39 cnf(i_0_650, negated_conjecture, (epred3_0|ndr1_1(a29))). % 30.69/4.39 cnf(i_0_620, negated_conjecture, (epred4_0|ndr1_1(a39))). % 30.69/4.39 cnf(i_0_107, negated_conjecture, (c3_1(a121)|~c5_1(a120))). % 30.69/4.39 cnf(i_0_581, negated_conjecture, (c8_0|c7_2(a47,a49))). % 30.69/4.39 cnf(i_0_587, negated_conjecture, (c8_2(a47,a48)|c8_0)). % 30.69/4.39 cnf(i_0_333, negated_conjecture, (c1_0|~c4_1(a85)|~c7_1(a83))). % 30.69/4.39 cnf(i_0_368, negated_conjecture, (c1_0|~c4_1(a85)|~c3_1(a83))). % 30.69/4.39 cnf(i_0_797, plain, (ndr1_1(X1)|~epred1_0)). % 30.69/4.39 cnf(i_0_651, negated_conjecture, (epred3_0|c1_2(a29,a30))). % 30.69/4.39 cnf(i_0_653, negated_conjecture, (epred3_0|c7_2(a29,a30))). % 30.69/4.39 cnf(i_0_648, negated_conjecture, (epred3_0|c6_2(a29,a31))). % 30.69/4.39 cnf(i_0_466, negated_conjecture, (c5_1(a65)|~c1_0|~c3_1(a66))). % 30.69/4.39 cnf(i_0_649, negated_conjecture, (epred3_0|c5_2(a29,a31))). % 30.69/4.39 cnf(i_0_652, negated_conjecture, (epred3_0|c2_2(a29,a30))). % 30.69/4.39 cnf(i_0_381, negated_conjecture, (c4_2(a81,a82)|~c1_0)). % 30.69/4.39 cnf(i_0_618, negated_conjecture, (epred4_0|c6_2(a39,a41))). % 30.69/4.39 cnf(i_0_854, plain, (~epred3_0|~c4_2(a27,a28)|~c2_1(a24))). % 30.69/4.39 cnf(i_0_623, negated_conjecture, (epred4_0|c3_2(a39,a40))). % 30.69/4.39 cnf(i_0_379, negated_conjecture, (c3_2(a81,a82)|~c1_0)). % 30.69/4.39 cnf(i_0_380, negated_conjecture, (c8_2(a81,a82)|~c1_0)). % 30.69/4.39 cnf(i_0_624, negated_conjecture, (epred4_0|c5_2(a39,a40))). % 30.69/4.39 cnf(i_0_856, plain, (~epred3_0|~c6_2(a27,a28)|~c2_1(a24))). % 30.69/4.39 cnf(i_0_903, plain, (~epred4_0|~c1_1(a37)|~c4_2(a35,a36))). % 30.69/4.39 cnf(i_0_910, plain, (~epred4_0|~c3_2(a35,a36)|~c1_1(a37))). % 30.69/4.39 cnf(i_0_917, plain, (~epred4_0|~c2_2(a35,a36)|~c1_1(a37))). % 30.69/4.39 cnf(i_0_210, negated_conjecture, (c3_1(a103)|c5_0|~c8_0)). % 30.69/4.39 cnf(i_0_686, negated_conjecture, (c1_1(a16)|~c8_0)). % 30.69/4.39 cnf(i_0_908, plain, (~epred4_0|~c6_1(a37)|~c4_2(a35,a36))). % 30.69/4.39 cnf(i_0_915, plain, (~epred4_0|~c6_1(a37)|~c3_2(a35,a36))). % 30.69/4.39 cnf(i_0_922, plain, (~epred4_0|~c6_1(a37)|~c2_2(a35,a36))). % 30.69/4.39 cnf(i_0_1043, plain, (~epred7_0|~c4_1(a141)|~c1_2(a143,a144))). % 30.69/4.39 cnf(i_0_356, negated_conjecture, (c1_0|ndr1_1(a83)|c7_1(a85))). % 30.69/4.39 cnf(i_0_458, negated_conjecture, (c6_1(a65)|~c1_0|~c3_1(a66))). % 30.69/4.39 cnf(i_0_328, negated_conjecture, (c1_0|c7_1(a85)|~c7_1(a83))). % 30.69/4.39 cnf(i_0_361, negated_conjecture, (c1_0|ndr1_1(a83)|~c4_1(a85))). % 30.69/4.39 cnf(i_0_332, negated_conjecture, (c1_0|ndr1_1(a85)|~c7_1(a83))). % 30.69/4.39 cnf(i_0_360, negated_conjecture, (c1_0|ndr1_1(a85)|ndr1_1(a83))). % 30.69/4.39 cnf(i_0_1042, plain, (~epred7_0|~c4_1(a141)|~c5_2(a143,a144))). % 30.69/4.39 cnf(i_0_1045, plain, (c5_1(a143)|~epred7_0|~c4_1(a141))). % 30.69/4.39 cnf(i_0_857, plain, (ndr1_1(a27)|~epred3_0|~c2_1(a24))). % 30.69/4.39 cnf(i_0_363, negated_conjecture, (c1_0|c7_1(a85)|~c3_1(a83))). % 30.69/4.39 cnf(i_0_367, negated_conjecture, (c1_0|ndr1_1(a85)|~c3_1(a83))). % 30.69/4.39 cnf(i_0_924, plain, (ndr1_1(a35)|~epred4_0|~c1_1(a37))). % 30.69/4.39 cnf(i_0_929, plain, (ndr1_1(a35)|~epred4_0|~c6_1(a37))). % 30.69/4.39 cnf(i_0_900, plain, (ndr1_1(a37)|~epred4_0|~c4_1(a35))). % 30.69/4.39 cnf(i_0_1044, plain, (ndr1_1(a143)|~epred7_0|~c4_1(a141))). % 30.69/4.39 cnf(i_0_330, negated_conjecture, (c1_0|~c1_2(a85,a86)|~c7_1(a83))). % 30.69/4.39 cnf(i_0_331, negated_conjecture, (c1_0|~c8_2(a85,a86)|~c7_1(a83))). % 30.69/4.39 cnf(i_0_365, negated_conjecture, (c1_0|~c3_1(a83)|~c1_2(a85,a86))). % 30.69/4.39 cnf(i_0_366, negated_conjecture, (c1_0|~c3_1(a83)|~c8_2(a85,a86))). % 30.69/4.39 cnf(i_0_859, plain, (c8_1(a27)|~epred3_0|~c2_1(a24))). % 30.69/4.39 cnf(i_0_347, negated_conjecture, (c1_0|~c4_1(a85)|~c2_2(a83,a84))). % 30.69/4.39 cnf(i_0_840, plain, (~epred3_0|~c7_2(a24,a26)|~c4_2(a27,a28))). % 30.69/4.39 cnf(i_0_875, plain, (~epred3_0|~c6_2(a24,a25)|~c4_2(a27,a28))). % 30.69/4.39 cnf(i_0_826, plain, (~epred3_0|~c6_2(a24,a26)|~c4_2(a27,a28))). % 30.69/4.39 cnf(i_0_842, plain, (~epred3_0|~c6_2(a27,a28)|~c7_2(a24,a26))). % 30.69/4.39 cnf(i_0_877, plain, (~epred3_0|~c6_2(a24,a25)|~c6_2(a27,a28))). % 30.69/4.39 cnf(i_0_344, negated_conjecture, (c1_0|~c2_2(a83,a84)|~c1_2(a85,a86))). % 30.69/4.39 cnf(i_0_828, plain, (~epred3_0|~c6_2(a24,a26)|~c6_2(a27,a28))). % 30.69/4.39 cnf(i_0_1025, plain, (~epred7_0|~c3_2(a141,a142)|~c1_2(a143,a144))). % 30.69/4.39 cnf(i_0_1024, plain, (~epred7_0|~c5_2(a143,a144)|~c3_2(a141,a142))). % 30.69/4.39 cnf(i_0_444, negated_conjecture, (ndr1_1(X1)|~c3_1(X1)|~c8_0)). % 30.69/4.39 cnf(i_0_345, negated_conjecture, (c1_0|~c8_2(a85,a86)|~c2_2(a83,a84))). % 30.69/4.39 cnf(i_0_342, negated_conjecture, (c1_0|c7_1(a85)|~c2_2(a83,a84))). % 30.69/4.39 cnf(i_0_358, negated_conjecture, (c1_0|ndr1_1(a83)|~c1_2(a85,a86))). % 30.69/4.39 cnf(i_0_359, negated_conjecture, (c1_0|ndr1_1(a83)|~c8_2(a85,a86))). % 30.69/4.39 cnf(i_0_32, negated_conjecture, (c8_1(X1)|~c1_1(a134)|~c2_1(X1))). % 30.69/4.39 cnf(i_0_346, negated_conjecture, (c1_0|ndr1_1(a85)|~c2_2(a83,a84))). % 30.69/4.39 cnf(i_0_965, plain, (ndr1_1(a53)|c5_1(a52)|~epred5_0)). % 30.69/4.39 cnf(i_0_335, negated_conjecture, (c1_0|c3_2(a83,a84)|c7_1(a85))). % 30.69/4.39 cnf(i_0_349, negated_conjecture, (c1_0|c5_2(a83,a84)|c7_1(a85))). % 30.69/4.39 cnf(i_0_329, negated_conjecture, (c1_0|c7_2(a85,a86)|~c7_1(a83))). % 30.69/4.39 cnf(i_0_364, negated_conjecture, (c1_0|c7_2(a85,a86)|~c3_1(a83))). % 30.69/4.39 cnf(i_0_340, negated_conjecture, (c1_0|c3_2(a83,a84)|~c4_1(a85))). % 30.69/4.39 cnf(i_0_354, negated_conjecture, (c1_0|c5_2(a83,a84)|~c4_1(a85))). % 30.69/4.39 cnf(i_0_357, negated_conjecture, (c1_0|c7_2(a85,a86)|ndr1_1(a83))). % 30.69/4.39 cnf(i_0_967, plain, (c5_1(a52)|~epred5_0|~c7_2(a53,a54))). % 30.69/4.39 cnf(i_0_968, plain, (c5_1(a52)|~epred5_0|~c8_2(a53,a54))). % 30.69/4.39 cnf(i_0_1027, plain, (c5_1(a143)|~epred7_0|~c3_2(a141,a142))). % 30.69/4.39 cnf(i_0_847, plain, (ndr1_1(a24)|~epred3_0|~c4_2(a27,a28))). % 30.69/4.39 cnf(i_0_339, negated_conjecture, (c1_0|c3_2(a83,a84)|ndr1_1(a85))). % 30.69/4.39 cnf(i_0_343, negated_conjecture, (c1_0|c7_2(a85,a86)|~c2_2(a83,a84))). % 30.69/4.39 cnf(i_0_338, negated_conjecture, (c1_0|c3_2(a83,a84)|~c8_2(a85,a86))). % 30.69/4.39 cnf(i_0_352, negated_conjecture, (c1_0|c5_2(a83,a84)|~c8_2(a85,a86))). % 30.69/4.39 cnf(i_0_337, negated_conjecture, (c1_0|c3_2(a83,a84)|~c1_2(a85,a86))). % 30.69/4.39 cnf(i_0_966, plain, (c1_1(a53)|c5_1(a52)|~epred5_0)). % 30.69/4.39 cnf(i_0_353, negated_conjecture, (c1_0|c5_2(a83,a84)|ndr1_1(a85))). % 30.69/4.39 cnf(i_0_849, plain, (ndr1_1(a24)|~epred3_0|~c6_2(a27,a28))). % 30.69/4.39 cnf(i_0_843, plain, (ndr1_1(a27)|~epred3_0|~c7_2(a24,a26))). % 30.69/4.39 cnf(i_0_351, negated_conjecture, (c1_0|c5_2(a83,a84)|~c1_2(a85,a86))). % 30.69/4.39 cnf(i_0_336, negated_conjecture, (c1_0|c3_2(a83,a84)|c7_2(a85,a86))). % 30.69/4.39 cnf(i_0_350, negated_conjecture, (c1_0|c5_2(a83,a84)|c7_2(a85,a86))). % 30.69/4.39 cnf(i_0_629, negated_conjecture, (~c7_2(a34,X1)|~ndr1_1(a34))). % 30.69/4.39 cnf(i_0_1033, plain, (ndr1_1(a141)|c5_1(a143)|~epred7_0)). % 30.69/4.39 cnf(i_0_878, plain, (ndr1_1(a27)|~epred3_0|~c6_2(a24,a25))). % 30.69/4.39 cnf(i_0_829, plain, (ndr1_1(a27)|~epred3_0|~c6_2(a24,a26))). % 30.69/4.39 cnf(i_0_907, plain, (ndr1_1(a37)|~epred4_0|~c4_2(a35,a36))). % 30.69/4.39 cnf(i_0_914, plain, (ndr1_1(a37)|~epred4_0|~c3_2(a35,a36))). % 30.69/4.39 cnf(i_0_1039, plain, (c8_1(a141)|c5_1(a143)|~epred7_0)). % 30.69/4.39 cnf(i_0_135, negated_conjecture, (~c8_1(X1)|~c7_2(X1,a115))). % 30.69/4.39 cnf(i_0_136, negated_conjecture, (~c8_1(X1)|~c3_2(X1,a115))). % 30.69/4.39 cnf(i_0_134, negated_conjecture, (~c8_1(X1)|~c8_2(X1,a115))). % 30.69/4.39 cnf(i_0_43, negated_conjecture, (~c6_1(a129)|~c1_0|~c1_1(X1)|~c4_2(X1,a128))). % 30.69/4.39 cnf(i_0_850, plain, (ndr1_1(a27)|ndr1_1(a24)|~epred3_0)). % 30.69/4.39 cnf(i_0_921, plain, (ndr1_1(a37)|~epred4_0|~c2_2(a35,a36))). % 30.69/4.39 cnf(i_0_1031, plain, (ndr1_1(a141)|~epred7_0|~c1_2(a143,a144))). % 30.69/4.39 cnf(i_0_1030, plain, (ndr1_1(a141)|~epred7_0|~c5_2(a143,a144))). % 30.69/4.39 cnf(i_0_1026, plain, (ndr1_1(a143)|~epred7_0|~c3_2(a141,a142))). % 30.69/4.39 cnf(i_0_852, plain, (c8_1(a27)|ndr1_1(a24)|~epred3_0)). % 30.69/4.39 cnf(i_0_63, negated_conjecture, (~c6_1(a129)|~c1_0|~c1_1(X1)|~c7_2(X1,a128))). % 30.69/4.39 cnf(i_0_53, negated_conjecture, (~c6_1(a129)|~c1_0|~c8_2(X1,a128)|~c1_1(X1))). % 30.69/4.39 cnf(i_0_310, negated_conjecture, (epred6_0|~c6_2(a93,X1)|~c7_2(a93,X1)|~ndr1_1(a93))). % 30.69/4.39 cnf(i_0_45, negated_conjecture, (~c1_0|~c1_1(X1)|~c7_2(a129,a131)|~c4_2(X1,a128))). % 30.69/4.39 cnf(i_0_928, plain, (ndr1_1(a37)|ndr1_1(a35)|~epred4_0)). % 30.69/4.39 cnf(i_0_845, plain, (c8_1(a27)|~epred3_0|~c7_2(a24,a26))). % 30.69/4.39 cnf(i_0_880, plain, (c8_1(a27)|~epred3_0|~c6_2(a24,a25))). % 30.69/4.39 cnf(i_0_831, plain, (c8_1(a27)|~epred3_0|~c6_2(a24,a26))). % 30.69/4.39 cnf(i_0_949, plain, (c8_1(a52)|~epred5_0|~c7_2(a53,a54))). % 30.69/4.39 cnf(i_0_947, plain, (c8_1(a52)|ndr1_1(a53)|~epred5_0)). % 30.69/4.39 cnf(i_0_50, negated_conjecture, (~c1_0|~c1_1(X1)|~c6_2(a129,a130)|~c4_2(X1,a128))). % 30.69/4.39 cnf(i_0_49, negated_conjecture, (~c1_0|~c8_2(a129,a130)|~c1_1(X1)|~c4_2(X1,a128))). % 30.69/4.39 cnf(i_0_55, negated_conjecture, (~c1_0|~c8_2(X1,a128)|~c1_1(X1)|~c7_2(a129,a131))). % 30.69/4.39 cnf(i_0_47, negated_conjecture, (ndr1_1(a129)|~c1_0|~c1_1(X1)|~c4_2(X1,a128))). % 30.69/4.39 cnf(i_0_1032, plain, (ndr1_1(a143)|ndr1_1(a141)|~epred7_0)). % 30.69/4.39 cnf(i_0_950, plain, (c8_1(a52)|~epred5_0|~c8_2(a53,a54))). % 30.69/4.39 cnf(i_0_1037, plain, (c8_1(a141)|~epred7_0|~c1_2(a143,a144))). % 30.69/4.39 cnf(i_0_1036, plain, (c8_1(a141)|~epred7_0|~c5_2(a143,a144))). % 30.69/4.39 cnf(i_0_393, negated_conjecture, (c7_1(X1)|~c8_1(X1))). % 30.69/4.39 cnf(i_0_1038, plain, (c8_1(a141)|ndr1_1(a143)|~epred7_0)). % 30.69/4.39 cnf(i_0_67, negated_conjecture, (ndr1_1(a129)|~c1_0|~c1_1(X1)|~c7_2(X1,a128))). % 30.69/4.39 cnf(i_0_57, negated_conjecture, (ndr1_1(a129)|~c1_0|~c8_2(X1,a128)|~c1_1(X1))). % 30.69/4.39 cnf(i_0_948, plain, (c8_1(a52)|c1_1(a53)|~epred5_0)). % 30.69/4.39 cnf(i_0_137, negated_conjecture, (ndr1_1(X1)|~c8_1(X1))). % 30.69/4.39 cnf(i_0_31, negated_conjecture, (c8_1(X1)|ndr1_1(a134)|~c2_1(X1))). % 30.69/4.39 cnf(i_0_73, negated_conjecture, (ndr1_1(X1)|~c6_1(a129)|~c1_0|~c1_1(X1))). % 30.69/4.39 cnf(i_0_46, negated_conjecture, (c1_2(a129,a131)|~c1_0|~c1_1(X1)|~c4_2(X1,a128))). % 30.69/4.39 cnf(i_0_428, negated_conjecture, (c4_1(X1)|c5_0|ndr1_1(X1)|~c8_0)). % 30.69/4.39 cnf(i_0_30, negated_conjecture, (c8_1(X1)|~c4_2(a134,a135)|~c2_1(X1))). % 30.69/4.39 cnf(i_0_439, negated_conjecture, (~c3_1(X1)|~c8_0|~c6_2(X1,a70)|~c1_2(X1,a69))). % 30.69/4.39 cnf(i_0_435, negated_conjecture, (~c3_1(X1)|~c8_0|~c6_2(X1,a69)|~c6_2(X1,a70))). % 30.69/4.39 cnf(i_0_781, plain, (~epred1_0|~c7_2(X1,a3)|~c1_2(X1,a2)|~c4_2(X1,a1))). % 30.69/4.39 cnf(i_0_66, negated_conjecture, (c1_2(a129,a131)|~c1_0|~c1_1(X1)|~c7_2(X1,a128))). % 30.69/4.39 cnf(i_0_56, negated_conjecture, (c1_2(a129,a131)|~c1_0|~c8_2(X1,a128)|~c1_1(X1))). % 30.69/4.39 cnf(i_0_48, negated_conjecture, (c3_2(a129,a130)|~c1_0|~c1_1(X1)|~c4_2(X1,a128))). % 30.69/4.39 cnf(i_0_68, negated_conjecture, (c3_2(a129,a130)|~c1_0|~c1_1(X1)|~c7_2(X1,a128))). % 30.69/4.39 cnf(i_0_769, plain, (~epred1_0|~c7_2(X1,a3)|~c1_2(X1,a1)|~c1_2(X1,a2))). % 30.69/4.39 cnf(i_0_861, plain, (c1_2(a24,a25)|~epred3_0|~c4_2(a27,a28))). % 30.69/4.39 cnf(i_0_863, plain, (c1_2(a24,a25)|~epred3_0|~c6_2(a27,a28))). % 30.69/4.39 cnf(i_0_868, plain, (c3_2(a24,a25)|~epred3_0|~c4_2(a27,a28))). % 30.69/4.39 cnf(i_0_58, negated_conjecture, (c3_2(a129,a130)|~c1_0|~c8_2(X1,a128)|~c1_1(X1))). % 30.69/4.39 cnf(i_0_44, negated_conjecture, (c8_2(a129,a131)|~c1_0|~c1_1(X1)|~c4_2(X1,a128))). % 30.69/4.39 cnf(i_0_65, negated_conjecture, (~c1_0|~c1_1(X1)|~c7_2(a129,a131)|~c7_2(X1,a128))). % 30.69/4.39 cnf(i_0_70, negated_conjecture, (~c1_0|~c1_1(X1)|~c6_2(a129,a130)|~c7_2(X1,a128))). % 30.69/4.39 cnf(i_0_870, plain, (c3_2(a24,a25)|~epred3_0|~c6_2(a27,a28))). % 30.69/4.39 cnf(i_0_904, plain, (c3_2(a37,a38)|~epred4_0|~c4_2(a35,a36))). % 30.69/4.39 cnf(i_0_918, plain, (c3_2(a37,a38)|~epred4_0|~c2_2(a35,a36))). % 30.69/4.39 cnf(i_0_906, plain, (c5_2(a37,a38)|~epred4_0|~c4_2(a35,a36))). % 30.69/4.39 cnf(i_0_69, negated_conjecture, (~c1_0|~c8_2(a129,a130)|~c1_1(X1)|~c7_2(X1,a128))). % 30.69/4.39 cnf(i_0_60, negated_conjecture, (~c1_0|~c8_2(X1,a128)|~c1_1(X1)|~c6_2(a129,a130))). % 30.69/4.39 cnf(i_0_59, negated_conjecture, (~c1_0|~c8_2(a129,a130)|~c8_2(X1,a128)|~c1_1(X1))). % 30.69/4.39 cnf(i_0_64, negated_conjecture, (c8_2(a129,a131)|~c1_0|~c1_1(X1)|~c7_2(X1,a128))). % 30.69/4.39 cnf(i_0_920, plain, (c5_2(a37,a38)|~epred4_0|~c2_2(a35,a36))). % 30.69/4.39 cnf(i_0_833, plain, (c2_2(a24,a26)|~epred3_0|~c4_2(a27,a28))). % 30.69/4.39 cnf(i_0_77, negated_conjecture, (ndr1_1(a129)|ndr1_1(X1)|~c1_0|~c1_1(X1))). % 30.69/4.39 cnf(i_0_969, plain, (c4_2(a53,a54)|c5_1(a52)|~epred5_0)). % 30.69/4.39 cnf(i_0_54, negated_conjecture, (c8_2(a129,a131)|~c1_0|~c8_2(X1,a128)|~c1_1(X1))). % 30.69/4.39 cnf(i_0_621, negated_conjecture, (epred4_0|c7_2(a39,X1)|~c8_2(a39,X1))). % 30.69/4.39 cnf(i_0_311, negated_conjecture, (epred6_0|c6_2(a93,X1)|~c4_2(a93,X1)|~ndr1_1(a93))). % 30.69/4.39 cnf(i_0_75, negated_conjecture, (ndr1_1(X1)|~c1_0|~c1_1(X1)|~c7_2(a129,a131))). % 30.69/4.39 cnf(i_0_1011, plain, (ndr1_1(a90)|ndr1_1(X1)|c5_1(X1)|~epred6_0)). % 30.69/4.39 cnf(i_0_963, plain, (c6_2(a53,a55)|c5_1(a52)|~epred5_0)). % 30.69/4.39 cnf(i_0_898, plain, (c4_2(a37,a38)|~epred4_0|~c4_1(a35))). % 30.69/4.39 cnf(i_0_897, plain, (c3_2(a37,a38)|~epred4_0|~c4_1(a35))). % 30.69/4.39 cnf(i_0_899, plain, (c5_2(a37,a38)|~epred4_0|~c4_1(a35))). % 30.69/4.39 cnf(i_0_855, plain, (c2_2(a27,a28)|~epred3_0|~c2_1(a24))). % 30.69/4.39 cnf(i_0_964, plain, (c2_2(a53,a55)|c5_1(a52)|~epred5_0)). % 30.69/4.39 cnf(i_0_80, negated_conjecture, (ndr1_1(X1)|~c1_0|~c1_1(X1)|~c6_2(a129,a130))). % 30.69/4.39 cnf(i_0_79, negated_conjecture, (ndr1_1(X1)|~c1_0|~c8_2(a129,a130)|~c1_1(X1))). % 30.69/4.39 cnf(i_0_28, negated_conjecture, (c8_1(X1)|c3_2(a134,a135)|~c2_1(X1))). % 30.69/4.39 cnf(i_0_29, negated_conjecture, (c8_1(X1)|c8_2(a134,a135)|~c2_1(X1))). % 30.69/4.39 cnf(i_0_1021, plain, (c8_2(a141,a142)|c5_1(a143)|~epred7_0)). % 30.69/4.39 cnf(i_0_1041, plain, (c2_2(a143,a144)|~epred7_0|~c4_1(a141))). % 30.69/4.39 cnf(i_0_848, plain, (c2_2(a27,a28)|ndr1_1(a24)|~epred3_0)). % 30.69/4.39 cnf(i_0_76, negated_conjecture, (c1_2(a129,a131)|ndr1_1(X1)|~c1_0|~c1_1(X1))). % 30.69/4.39 cnf(i_0_78, negated_conjecture, (c3_2(a129,a130)|ndr1_1(X1)|~c1_0|~c1_1(X1))). % 30.69/4.39 cnf(i_0_74, negated_conjecture, (c8_2(a129,a131)|ndr1_1(X1)|~c1_0|~c1_1(X1))). % 30.69/4.39 cnf(i_0_864, plain, (c1_2(a24,a25)|ndr1_1(a27)|~epred3_0)). % 30.69/4.39 cnf(i_0_871, plain, (c3_2(a24,a25)|ndr1_1(a27)|~epred3_0)). % 30.69/4.39 cnf(i_0_836, plain, (c2_2(a24,a26)|ndr1_1(a27)|~epred3_0)). % 30.69/4.39 cnf(i_0_926, plain, (c4_2(a37,a38)|ndr1_1(a35)|~epred4_0)). % 30.69/4.39 cnf(i_0_761, negated_conjecture, (epred1_0|c2_1(X1)|~c5_0|~c5_1(X1)|~c7_1(X1))). % 30.69/4.39 cnf(i_0_992, plain, (c5_1(X1)|~epred6_0|~c3_2(a90,a92)|~c7_2(X1,a89))). % 30.69/4.39 cnf(i_0_577, negated_conjecture, (c6_1(X1)|c2_1(X1)|~c8_0|~c5_1(X1))). % 30.69/4.39 cnf(i_0_925, plain, (c3_2(a37,a38)|ndr1_1(a35)|~epred4_0)). % 30.69/4.39 cnf(i_0_104, negated_conjecture, (c5_1(a121)|~c5_2(a120,X1)|~c7_2(a120,X1)|~c1_2(a120,X1)|~ndr1_1(a120))). % 30.69/4.39 cnf(i_0_103, negated_conjecture, (c3_1(a121)|~c5_2(a120,X1)|~c7_2(a120,X1)|~c1_2(a120,X1)|~ndr1_1(a120))). % 30.69/4.39 cnf(i_0_927, plain, (c5_2(a37,a38)|ndr1_1(a35)|~epred4_0)). % 30.69/4.39 cnf(i_0_1029, plain, (c2_2(a143,a144)|ndr1_1(a141)|~epred7_0)). % 30.69/4.39 cnf(i_0_905, plain, (c4_2(a37,a38)|~epred4_0|~c4_2(a35,a36))). % 30.69/4.39 cnf(i_0_912, plain, (c4_2(a37,a38)|~epred4_0|~c3_2(a35,a36))). % 30.69/4.39 cnf(i_0_919, plain, (c4_2(a37,a38)|~epred4_0|~c2_2(a35,a36))). % 30.69/4.39 cnf(i_0_911, plain, (c3_2(a37,a38)|~epred4_0|~c3_2(a35,a36))). % 30.69/4.39 cnf(i_0_1020, plain, (c8_2(a141,a142)|ndr1_1(a143)|~epred7_0)). % 30.69/4.39 cnf(i_0_434, negated_conjecture, (c7_2(X1,a70)|~c3_1(X1)|~c8_0|~c6_2(X1,a69))). % 30.69/4.39 cnf(i_0_431, negated_conjecture, (c5_2(X1,a69)|~c3_1(X1)|~c8_0|~c6_2(X1,a70))). % 30.69/4.39 cnf(i_0_476, negated_conjecture, (c6_1(X1)|~c5_2(X1,a63)|~c1_1(a64)|~c7_1(X1))). % 30.69/4.39 cnf(i_0_866, plain, (c8_1(a27)|c1_2(a24,a25)|~epred3_0)). % 30.69/4.39 cnf(i_0_873, plain, (c8_1(a27)|c3_2(a24,a25)|~epred3_0)). % 30.69/4.39 cnf(i_0_913, plain, (c5_2(a37,a38)|~epred4_0|~c3_2(a35,a36))). % 30.69/4.39 cnf(i_0_835, plain, (c2_2(a24,a26)|~epred3_0|~c6_2(a27,a28))). % 30.69/4.39 cnf(i_0_841, plain, (c2_2(a27,a28)|~epred3_0|~c7_2(a24,a26))). % 30.69/4.39 cnf(i_0_876, plain, (c2_2(a27,a28)|~epred3_0|~c6_2(a24,a25))). % 30.69/4.39 cnf(i_0_838, plain, (c8_1(a27)|c2_2(a24,a26)|~epred3_0)). % 30.69/4.39 cnf(i_0_484, negated_conjecture, (c6_1(X1)|~c2_2(X1,a63)|~c1_1(a64)|~c7_1(X1))). % 30.69/4.39 cnf(i_0_423, negated_conjecture, (c4_1(X1)|c5_0|~c8_0|~c1_2(X1,a71)|~c1_2(X1,a72))). % 30.69/4.39 cnf(i_0_419, negated_conjecture, (c4_1(X1)|c5_0|~c8_0|~c3_2(X1,a71)|~c1_2(X1,a72))). % 30.69/4.39 cnf(i_0_951, plain, (c8_1(a52)|c4_2(a53,a54)|~epred5_0)). % 30.69/4.39 cnf(i_0_945, plain, (c8_1(a52)|c6_2(a53,a55)|~epred5_0)). % 30.69/4.39 cnf(i_0_827, plain, (c2_2(a27,a28)|~epred3_0|~c6_2(a24,a26))). % 30.69/4.39 cnf(i_0_1023, plain, (c2_2(a143,a144)|~epred7_0|~c3_2(a141,a142))). % 30.69/4.39 cnf(i_0_1019, plain, (c8_2(a141,a142)|~epred7_0|~c1_2(a143,a144))). % 30.69/4.39 cnf(i_0_1018, plain, (c8_2(a141,a142)|~epred7_0|~c5_2(a143,a144))). % 30.69/4.39 cnf(i_0_946, plain, (c8_1(a52)|c2_2(a53,a55)|~epred5_0)). % 30.69/4.39 cnf(i_0_504, negated_conjecture, (c5_2(a59,X1)|c7_2(a59,X1)|~ndr1_1(a59))). % 30.69/4.39 cnf(i_0_112, negated_conjecture, (c1_2(a120,X1)|c5_1(a121)|~c8_2(a120,X1)|~c6_2(a120,X1)|~ndr1_1(a120))). % 30.69/4.39 cnf(i_0_111, negated_conjecture, (c3_1(a121)|c1_2(a120,X1)|~c8_2(a120,X1)|~c6_2(a120,X1)|~ndr1_1(a120))). % 30.69/4.39 cnf(i_0_1035, plain, (c8_1(a141)|c2_2(a143,a144)|~epred7_0)). % 30.69/4.39 cnf(i_0_150, negated_conjecture, (c3_1(X1)|ndr1_1(X1)|~c1_0|~c8_1(a113)|~c7_1(X1))). % 30.69/4.39 cnf(i_0_993, plain, (ndr1_1(a90)|c5_1(X1)|~epred6_0|~c7_2(X1,a89))). % 30.69/4.39 cnf(i_0_862, plain, (c2_2(a27,a28)|c1_2(a24,a25)|~epred3_0)). % 30.69/4.39 cnf(i_0_209, negated_conjecture, (c8_2(a103,X1)|c5_0|~c8_0|~c5_2(a103,X1)|~c4_2(a103,X1)|~ndr1_1(a103))). % 30.69/4.39 cnf(i_0_437, negated_conjecture, (c4_2(X1,a70)|~c3_1(X1)|~c8_0|~c1_2(X1,a69))). % 30.69/4.39 cnf(i_0_433, negated_conjecture, (c4_2(X1,a70)|~c3_1(X1)|~c8_0|~c6_2(X1,a69))). % 30.69/4.39 cnf(i_0_402, negated_conjecture, (c3_1(X1)|c5_0|c7_1(X1)|~c2_1(X1))). % 30.69/4.39 cnf(i_0_869, plain, (c2_2(a27,a28)|c3_2(a24,a25)|~epred3_0)). % 30.69/4.39 cnf(i_0_991, plain, (c5_1(X1)|~epred6_0|~c7_2(X1,a89)|~c4_2(a90,a92))). % 30.69/4.39 cnf(i_0_208, negated_conjecture, (c6_1(X1)|c4_1(X1)|c8_0|~c8_1(X1))). % 30.69/4.39 cnf(i_0_775, plain, (c4_2(X1,a2)|~epred1_0|~c7_2(X1,a3)|~c4_2(X1,a1))). % 30.69/4.39 cnf(i_0_834, plain, (c2_2(a27,a28)|c2_2(a24,a26)|~epred3_0)). % 30.69/4.39 cnf(i_0_438, negated_conjecture, (c7_2(X1,a70)|~c3_1(X1)|~c8_0|~c1_2(X1,a69))). % 30.69/4.39 cnf(i_0_634, negated_conjecture, (c1_1(X1)|ndr1_1(X1)|c2_1(a32)|~c1_0|~c4_1(X1))). % 30.69/4.39 cnf(i_0_1017, plain, (c8_2(a141,a142)|c2_2(a143,a144)|~epred7_0)). % 30.69/4.39 cnf(i_0_778, plain, (c7_2(X1,a2)|~epred1_0|~c7_2(X1,a3)|~c4_2(X1,a1))). % 30.69/4.39 cnf(i_0_766, plain, (c7_2(X1,a2)|~epred1_0|~c7_2(X1,a3)|~c1_2(X1,a1))). % 30.69/4.39 cnf(i_0_780, plain, (c6_2(X1,a3)|~epred1_0|~c1_2(X1,a2)|~c4_2(X1,a1))). % 30.69/4.39 cnf(i_0_146, negated_conjecture, (c3_1(X1)|ndr1_1(X1)|~c1_0|~c4_1(a113)|~c7_1(X1))). % 30.69/4.39 cnf(i_0_453, negated_conjecture, (c6_1(X1)|ndr1_1(X1)|c2_1(X1)|c5_1(a68))). % 30.69/4.39 cnf(i_0_455, negated_conjecture, (c6_1(X1)|ndr1_1(X1)|c2_1(a68)|c2_1(X1))). % 30.69/4.39 cnf(i_0_488, negated_conjecture, (c6_1(X1)|ndr1_1(X1)|~c1_1(a64)|~c7_1(X1))). % 30.69/4.39 cnf(i_0_1009, plain, (ndr1_1(X1)|c5_1(X1)|~epred6_0|~c4_2(a90,a92))). % 30.69/4.39 cnf(i_0_1010, plain, (ndr1_1(X1)|c5_1(X1)|~epred6_0|~c3_2(a90,a92))). % 30.69/4.39 cnf(i_0_995, plain, (c1_2(a90,a91)|c5_1(X1)|~epred6_0|~c7_2(X1,a89))). % 30.69/4.39 cnf(i_0_24, negated_conjecture, (c8_2(a136,X1)|c3_2(a136,X1)|c7_2(a136,X1))). % 30.69/4.39 cnf(i_0_449, negated_conjecture, (c6_1(X1)|c2_1(X1)|c5_1(a68)|~c4_2(X1,a67))). % 30.69/4.39 cnf(i_0_445, negated_conjecture, (c6_1(X1)|c2_1(X1)|c5_1(a68)|~c7_2(X1,a67))). % 30.69/4.39 cnf(i_0_451, negated_conjecture, (c6_1(X1)|c2_1(a68)|c2_1(X1)|~c4_2(X1,a67))). % 30.69/4.39 cnf(i_0_447, negated_conjecture, (c6_1(X1)|c2_1(a68)|c2_1(X1)|~c7_2(X1,a67))). % 30.69/4.39 cnf(i_0_1013, plain, (c1_2(a90,a91)|ndr1_1(X1)|c5_1(X1)|~epred6_0)). % 30.69/4.39 cnf(i_0_984, plain, (c1_2(X1,a89)|ndr1_1(a90)|c5_1(X1)|~epred6_0)). % 30.69/4.39 cnf(i_0_994, plain, (c3_2(a90,a91)|c5_1(X1)|~epred6_0|~c7_2(X1,a89))). % 30.69/4.39 cnf(i_0_763, plain, (c4_2(X1,a2)|~epred1_0|~c7_2(X1,a3)|~c1_2(X1,a1))). % 30.69/4.39 cnf(i_0_768, plain, (c6_2(X1,a3)|~epred1_0|~c1_2(X1,a1)|~c1_2(X1,a2))). % 30.69/4.39 cnf(i_0_958, plain, (~epred5_0|~c8_2(a52,X1)|~c5_2(a52,X1)|~c7_2(a53,a54)|~c7_2(a52,X1)|~ndr1_1(a52))). % 30.69/4.39 cnf(i_0_647, negated_conjecture, (epred3_0|c5_2(a29,X1)|c1_2(a29,X1)|~c6_2(a29,X1))). % 30.69/4.39 cnf(i_0_312, negated_conjecture, (epred6_0|c8_2(a93,X1)|c5_2(a93,X1)|~c6_2(a93,X1)|~ndr1_1(a93))). % 30.69/4.39 cnf(i_0_1008, plain, (c7_2(a90,a92)|ndr1_1(X1)|c5_1(X1)|~epred6_0)). % 30.69/4.39 cnf(i_0_1002, plain, (c2_2(X1,a89)|ndr1_1(a90)|c5_1(X1)|~epred6_0)). % 30.69/4.39 cnf(i_0_1012, plain, (c3_2(a90,a91)|ndr1_1(X1)|c5_1(X1)|~epred6_0)). % 30.69/4.39 cnf(i_0_715, negated_conjecture, (c6_2(X1,X2)|~c4_1(X1)|~c8_0|~c2_2(X1,X2)|~ndr1_1(X1)|~c5_1(X1))). % 30.69/4.39 cnf(i_0_148, negated_conjecture, (c3_1(X1)|c1_2(X1,a114)|~c1_0|~c8_1(a113)|~c7_1(X1))). % 30.69/4.39 cnf(i_0_144, negated_conjecture, (c3_1(X1)|c1_2(X1,a114)|~c1_0|~c4_1(a113)|~c7_1(X1))). % 30.69/4.39 cnf(i_0_149, negated_conjecture, (c3_1(X1)|c5_2(X1,a114)|~c1_0|~c8_1(a113)|~c7_1(X1))). % 30.69/4.39 cnf(i_0_145, negated_conjecture, (c3_1(X1)|c5_2(X1,a114)|~c1_0|~c4_1(a113)|~c7_1(X1))). % 30.69/4.39 cnf(i_0_1001, plain, (c2_2(X1,a89)|c5_1(X1)|~epred6_0|~c3_2(a90,a92))). % 30.69/4.39 cnf(i_0_956, plain, (ndr1_1(a53)|~epred5_0|~c8_2(a52,X1)|~c5_2(a52,X1)|~c7_2(a52,X1)|~ndr1_1(a52))). % 30.69/4.39 cnf(i_0_957, plain, (c1_1(a53)|~epred5_0|~c8_2(a52,X1)|~c5_2(a52,X1)|~c7_2(a52,X1)|~ndr1_1(a52))). % 30.69/4.39 cnf(i_0_147, negated_conjecture, (c3_1(X1)|c8_2(X1,a114)|~c1_0|~c8_1(a113)|~c7_1(X1))). % 30.69/4.39 cnf(i_0_143, negated_conjecture, (c3_1(X1)|c8_2(X1,a114)|~c1_0|~c4_1(a113)|~c7_1(X1))). % 30.69/4.39 cnf(i_0_429, negated_conjecture, (c5_2(X1,a69)|c4_2(X1,a70)|~c3_1(X1)|~c8_0)). % 30.69/4.39 cnf(i_0_191, negated_conjecture, (c7_1(X1)|~c8_2(X1,X2)|~c5_2(X1,X2)|~c7_2(X1,a108)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_192, negated_conjecture, (c7_1(X1)|~c8_2(X1,X2)|~c5_2(X1,a108)|~c5_2(X1,X2)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_774, plain, (c6_2(X1,a3)|c4_2(X1,a2)|~epred1_0|~c4_2(X1,a1))). % 30.69/4.39 cnf(i_0_777, plain, (c6_2(X1,a3)|c7_2(X1,a2)|~epred1_0|~c4_2(X1,a1))). % 30.69/4.39 cnf(i_0_430, negated_conjecture, (c5_2(X1,a69)|c7_2(X1,a70)|~c3_1(X1)|~c8_0)). % 30.69/4.39 cnf(i_0_480, negated_conjecture, (c6_1(X1)|c4_2(X1,a63)|~c1_1(a64)|~c7_1(X1))). % 30.69/4.39 cnf(i_0_421, negated_conjecture, (c4_1(X1)|c5_0|c7_2(X1,a72)|~c8_0|~c1_2(X1,a71))). % 30.69/4.39 cnf(i_0_417, negated_conjecture, (c4_1(X1)|c5_0|c7_2(X1,a72)|~c8_0|~c3_2(X1,a71))). % 30.69/4.39 cnf(i_0_959, plain, (~epred5_0|~c8_2(a53,a54)|~c8_2(a52,X1)|~c5_2(a52,X1)|~c7_2(a52,X1)|~ndr1_1(a52))). % 30.69/4.39 cnf(i_0_931, plain, (c8_2(a35,X1)|~epred4_0|~c2_2(a35,X1)|~c1_1(a37)|~c1_2(a35,X1))). % 30.69/4.39 cnf(i_0_936, plain, (c8_2(a35,X1)|~epred4_0|~c6_1(a37)|~c2_2(a35,X1)|~c1_2(a35,X1))). % 30.69/4.39 cnf(i_0_415, negated_conjecture, (c4_1(X1)|c5_2(X1,a71)|c5_0|~c8_0|~c1_2(X1,a72))). % 30.69/4.39 cnf(i_0_422, negated_conjecture, (c4_1(X1)|c8_2(X1,a72)|c5_0|~c8_0|~c1_2(X1,a71))). % 30.69/4.39 cnf(i_0_418, negated_conjecture, (c4_1(X1)|c8_2(X1,a72)|c5_0|~c8_0|~c3_2(X1,a71))). % 30.69/4.39 cnf(i_0_633, negated_conjecture, (c1_1(X1)|c4_2(X1,a33)|c2_1(a32)|~c1_0|~c4_1(X1))). % 30.69/4.39 cnf(i_0_982, plain, (c1_2(X1,a89)|c5_1(X1)|~epred6_0|~c4_2(a90,a92))). % 30.69/4.39 cnf(i_0_983, plain, (c1_2(X1,a89)|c5_1(X1)|~epred6_0|~c3_2(a90,a92))). % 30.69/4.39 cnf(i_0_1000, plain, (c2_2(X1,a89)|c5_1(X1)|~epred6_0|~c4_2(a90,a92))). % 30.69/4.39 cnf(i_0_762, plain, (c6_2(X1,a3)|c4_2(X1,a2)|~epred1_0|~c1_2(X1,a1))). % 30.69/4.39 cnf(i_0_632, negated_conjecture, (c1_1(X1)|c1_2(X1,a33)|c2_1(a32)|~c1_0|~c4_1(X1))). % 30.69/4.39 cnf(i_0_631, negated_conjecture, (c3_2(X1,a33)|c1_1(X1)|c2_1(a32)|~c1_0|~c4_1(X1))). % 30.69/4.39 cnf(i_0_468, negated_conjecture, (c5_2(a66,X1)|c3_2(a66,X1)|c5_1(a65)|~c1_0|~c8_2(a66,X1)|~ndr1_1(a66))). % 30.69/4.39 cnf(i_0_460, negated_conjecture, (c6_1(a65)|c5_2(a66,X1)|c3_2(a66,X1)|~c1_0|~c8_2(a66,X1)|~ndr1_1(a66))). % 30.69/4.39 cnf(i_0_309, negated_conjecture, (c4_1(X1)|c1_1(X1)|c5_0|ndr1_1(X2)|~c2_1(X2)|~c5_1(X1))). % 30.69/4.39 cnf(i_0_413, negated_conjecture, (c4_1(X1)|c5_2(X1,a71)|c5_0|c7_2(X1,a72)|~c8_0)). % 30.69/4.39 cnf(i_0_765, plain, (c6_2(X1,a3)|c7_2(X1,a2)|~epred1_0|~c1_2(X1,a1))). % 30.69/4.39 cnf(i_0_414, negated_conjecture, (c4_1(X1)|c8_2(X1,a72)|c5_2(X1,a71)|c5_0|~c8_0)). % 30.69/4.39 cnf(i_0_109, negated_conjecture, (c8_2(a121,X1)|c5_2(a121,X1)|~c7_2(a121,X1)|~ndr1_1(a121)|~c5_1(a120))). % 30.69/4.39 cnf(i_0_627, negated_conjecture, (c1_2(a34,X1)|c4_2(a34,X1)|~c8_2(a34,X1)|~ndr1_1(a34))). % 30.69/4.39 cnf(i_0_986, plain, (c1_2(a90,a91)|c1_2(X1,a89)|c5_1(X1)|~epred6_0)). % 30.69/4.39 cnf(i_0_1004, plain, (c2_2(X1,a89)|c1_2(a90,a91)|c5_1(X1)|~epred6_0)). % 30.69/4.39 cnf(i_0_990, plain, (c7_2(a90,a92)|c5_1(X1)|~epred6_0|~c7_2(X1,a89))). % 30.69/4.39 cnf(i_0_38, negated_conjecture, (c7_2(X1,X2)|~c8_2(X1,X2)|~c8_0|~c1_1(X1)|~c6_2(X1,a132)|~c4_2(X1,X2)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_40, negated_conjecture, (c7_2(X1,X2)|~c8_2(X1,X2)|~c8_0|~c3_2(X1,a132)|~c1_1(X1)|~c4_2(X1,X2)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_39, negated_conjecture, (c7_2(X1,X2)|~c8_2(X1,a132)|~c8_2(X1,X2)|~c8_0|~c1_1(X1)|~c4_2(X1,X2)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_999, plain, (c2_2(X1,a89)|c7_2(a90,a92)|c5_1(X1)|~epred6_0)). % 30.69/4.39 cnf(i_0_573, negated_conjecture, (c3_2(a51,X1)|c4_2(a51,X1)|~c5_2(a51,X1)|~ndr1_1(a51))). % 30.69/4.39 cnf(i_0_628, negated_conjecture, (c2_2(a34,X1)|~c1_2(a34,X1)|~ndr1_1(a34))). % 30.69/4.39 cnf(i_0_467, negated_conjecture, (c2_2(a66,X1)|c3_2(a66,X1)|c5_1(a65)|~c1_0|~c8_2(a66,X1)|~ndr1_1(a66))). % 30.69/4.39 cnf(i_0_459, negated_conjecture, (c6_1(a65)|c2_2(a66,X1)|c3_2(a66,X1)|~c1_0|~c8_2(a66,X1)|~ndr1_1(a66))). % 30.69/4.39 cnf(i_0_981, plain, (c7_2(a90,a92)|c1_2(X1,a89)|c5_1(X1)|~epred6_0)). % 30.69/4.39 cnf(i_0_1003, plain, (c2_2(X1,a89)|c3_2(a90,a91)|c5_1(X1)|~epred6_0)). % 30.69/4.39 cnf(i_0_935, plain, (c8_2(a35,X1)|ndr1_1(a37)|~epred4_0|~c2_2(a35,X1)|~c1_2(a35,X1))). % 30.69/4.39 cnf(i_0_985, plain, (c3_2(a90,a91)|c1_2(X1,a89)|c5_1(X1)|~epred6_0)). % 30.69/4.39 cnf(i_0_997, plain, (c5_1(X1)|~epred6_0|~c2_2(a90,X2)|~c6_2(a90,X2)|~c7_2(X1,a89)|~c1_2(a90,X2))). % 30.69/4.39 cnf(i_0_858, plain, (c8_2(a27,X1)|c5_2(a27,X1)|~epred3_0|~c7_2(a27,X1)|~c2_1(a24))). % 30.69/4.39 cnf(i_0_211, negated_conjecture, (c5_2(a103,X1)|c5_0|c1_2(a103,X1)|c4_2(a103,X1)|~c8_0|~ndr1_1(a103))). % 30.69/4.39 cnf(i_0_932, plain, (c8_2(a35,X1)|c3_2(a37,a38)|~epred4_0|~c2_2(a35,X1)|~c1_2(a35,X1))). % 30.69/4.39 cnf(i_0_934, plain, (c8_2(a35,X1)|c5_2(a37,a38)|~epred4_0|~c2_2(a35,X1)|~c1_2(a35,X1))). % 30.69/4.39 cnf(i_0_960, plain, (c4_2(a53,a54)|~epred5_0|~c8_2(a52,X1)|~c5_2(a52,X1)|~c7_2(a52,X1)|~ndr1_1(a52))). % 30.69/4.39 cnf(i_0_462, negated_conjecture, (c5_2(a65,X1)|c1_2(a65,X1)|c4_2(a65,X1)|~c1_0|~c3_1(a66)|~ndr1_1(a65))). % 30.69/4.39 cnf(i_0_27, negated_conjecture, (c8_1(X1)|c8_2(a134,X2)|c1_2(a134,X2)|~c2_1(X1))). % 30.69/4.39 cnf(i_0_851, plain, (c8_2(a27,X1)|c5_2(a27,X1)|ndr1_1(a24)|~epred3_0|~c7_2(a27,X1))). % 30.69/4.39 cnf(i_0_954, plain, (c6_2(a53,a55)|~epred5_0|~c8_2(a52,X1)|~c5_2(a52,X1)|~c7_2(a52,X1)|~ndr1_1(a52))). % 30.69/4.39 cnf(i_0_955, plain, (c2_2(a53,a55)|~epred5_0|~c8_2(a52,X1)|~c5_2(a52,X1)|~c7_2(a52,X1)|~ndr1_1(a52))). % 30.69/4.39 cnf(i_0_1015, plain, (ndr1_1(X1)|c5_1(X1)|~epred6_0|~c2_2(a90,X2)|~c6_2(a90,X2)|~c1_2(a90,X2))). % 30.69/4.39 cnf(i_0_193, negated_conjecture, (c6_2(X1,a108)|c7_1(X1)|~c8_2(X1,X2)|~c5_2(X1,X2)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_642, negated_conjecture, (c1_1(X1)|c1_2(a32,X2)|c4_2(a32,X2)|ndr1_1(X1)|~c1_0|~c4_1(X1)|~ndr1_1(a32))). % 30.69/4.39 cnf(i_0_450, negated_conjecture, (c6_1(X1)|c6_2(a68,X2)|c7_2(a68,X2)|c2_1(X1)|~c4_2(X1,a67)|~ndr1_1(a68))). % 30.69/4.39 cnf(i_0_446, negated_conjecture, (c6_1(X1)|c6_2(a68,X2)|c7_2(a68,X2)|c2_1(X1)|~c7_2(X1,a67)|~ndr1_1(a68))). % 30.69/4.39 cnf(i_0_844, plain, (c8_2(a27,X1)|c5_2(a27,X1)|~epred3_0|~c7_2(a24,a26)|~c7_2(a27,X1))). % 30.69/4.39 cnf(i_0_661, negated_conjecture, (c8_0|c5_0|c1_2(X1,X2)|~c8_2(X1,X2)|~c5_2(X1,X2)|~c3_2(X1,a23)|~c7_2(X1,a22)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_303, negated_conjecture, (c4_1(X1)|c1_1(X1)|c5_0|c1_2(X2,a95)|~c5_2(X2,a94)|~c2_1(X2)|~c5_1(X1))). % 30.69/4.39 cnf(i_0_304, negated_conjecture, (c4_1(X1)|c5_2(X2,a95)|c1_1(X1)|c5_0|~c5_2(X2,a94)|~c2_1(X2)|~c5_1(X1))). % 30.69/4.39 cnf(i_0_105, negated_conjecture, (c8_2(a121,X1)|c5_2(a121,X1)|~c5_2(a120,X2)|~c7_2(a120,X2)|~c7_2(a121,X1)|~c1_2(a120,X2)|~ndr1_1(a120)|~ndr1_1(a121))). % 30.69/4.39 cnf(i_0_641, negated_conjecture, (c1_1(X1)|c1_2(a32,X2)|c4_2(a32,X2)|c4_2(X1,a33)|~c1_0|~c4_1(X1)|~ndr1_1(a32))). % 30.69/4.39 cnf(i_0_454, negated_conjecture, (c6_1(X1)|c6_2(a68,X2)|c7_2(a68,X2)|ndr1_1(X1)|c2_1(X1)|~ndr1_1(a68))). % 30.69/4.39 cnf(i_0_760, negated_conjecture, (ndr1_1(X1)|c2_1(X2)|~c8_0|~c2_2(X2,X3)|~c5_2(X2,X3)|~c1_1(X2)|~c1_1(X1)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_206, negated_conjecture, (c5_2(X1,X2)|c5_0|c6_2(X1,X2)|~c6_1(X1)|~c2_2(X1,X2)|~ndr1_1(X1)|~c2_1(X1)|~c5_1(a104))). % 30.69/4.39 cnf(i_0_812, plain, (c5_2(X1,X2)|c1_2(X1,X2)|~epred2_0|~c2_2(X1,a13)|~c1_1(X1)|~ndr1_1(X1)|~c7_1(a14))). % 30.69/4.39 cnf(i_0_805, plain, (c5_2(X1,X2)|c1_2(X1,X2)|~epred2_0|~c8_2(X1,a13)|~c1_1(X1)|~ndr1_1(X1)|~c7_1(a14))). % 30.69/4.39 cnf(i_0_865, plain, (c8_2(a27,X1)|c5_2(a27,X1)|c1_2(a24,a25)|~epred3_0|~c7_2(a27,X1))). % 30.69/4.39 cnf(i_0_640, negated_conjecture, (c1_1(X1)|c1_2(a32,X2)|c1_2(X1,a33)|c4_2(a32,X2)|~c1_0|~c4_1(X1)|~ndr1_1(a32))). % 30.69/4.39 cnf(i_0_639, negated_conjecture, (c3_2(X1,a33)|c1_1(X1)|c1_2(a32,X2)|c4_2(a32,X2)|~c1_0|~c4_1(X1)|~ndr1_1(a32))). % 30.69/4.39 cnf(i_0_302, negated_conjecture, (c4_1(X1)|c1_1(X1)|c5_0|c6_2(X2,a95)|~c5_2(X2,a94)|~c2_1(X2)|~c5_1(X1))). % 30.69/4.39 cnf(i_0_477, negated_conjecture, (c6_1(X1)|c8_2(a64,X2)|c4_2(a64,X2)|~c2_2(a64,X2)|~c5_2(X1,a63)|~ndr1_1(a64)|~c7_1(X1))). % 30.69/4.39 cnf(i_0_299, negated_conjecture, (c4_1(X1)|c1_1(X1)|c5_0|c6_2(X2,a94)|c1_2(X2,a95)|~c2_1(X2)|~c5_1(X1))). % 30.69/4.39 cnf(i_0_872, plain, (c8_2(a27,X1)|c5_2(a27,X1)|c3_2(a24,a25)|~epred3_0|~c7_2(a27,X1))). % 30.69/4.39 cnf(i_0_817, plain, (c5_2(X1,X2)|c1_2(X1,X2)|~epred2_0|~c2_2(X1,a13)|~c1_1(X1)|~ndr1_1(X1)|~c2_1(a14))). % 30.69/4.39 cnf(i_0_810, plain, (c5_2(X1,X2)|c1_2(X1,X2)|~epred2_0|~c8_2(X1,a13)|~c1_1(X1)|~ndr1_1(X1)|~c2_1(a14))). % 30.69/4.39 cnf(i_0_879, plain, (c8_2(a27,X1)|c5_2(a27,X1)|~epred3_0|~c6_2(a24,a25)|~c7_2(a27,X1))). % 30.69/4.39 cnf(i_0_295, negated_conjecture, (c4_1(X1)|c2_2(X2,a94)|c1_1(X1)|c5_0|c1_2(X2,a95)|~c2_1(X2)|~c5_1(X1))). % 30.69/4.39 cnf(i_0_485, negated_conjecture, (c6_1(X1)|c8_2(a64,X2)|c4_2(a64,X2)|~c2_2(X1,a63)|~c2_2(a64,X2)|~ndr1_1(a64)|~c7_1(X1))). % 30.69/4.39 cnf(i_0_142, negated_conjecture, (c3_1(X1)|c8_2(a113,X2)|c7_2(a113,X2)|ndr1_1(X1)|~c1_0|~c4_2(a113,X2)|~ndr1_1(a113)|~c7_1(X1))). % 30.69/4.39 cnf(i_0_113, negated_conjecture, (c8_2(a121,X1)|c5_2(a121,X1)|c1_2(a120,X2)|~c8_2(a120,X2)|~c6_2(a120,X2)|~c7_2(a121,X1)|~ndr1_1(a120)|~ndr1_1(a121))). % 30.69/4.39 cnf(i_0_638, negated_conjecture, (c1_1(X1)|c6_2(a32,X2)|c1_2(a32,X2)|ndr1_1(X1)|~c1_0|~c4_1(X1)|~c3_2(a32,X2)|~ndr1_1(a32))). % 30.69/4.39 cnf(i_0_298, negated_conjecture, (c4_1(X1)|c1_1(X1)|c5_0|c6_2(X2,a95)|c6_2(X2,a94)|~c2_1(X2)|~c5_1(X1))). % 30.69/4.39 cnf(i_0_300, negated_conjecture, (c4_1(X1)|c5_2(X2,a95)|c1_1(X1)|c5_0|c6_2(X2,a94)|~c2_1(X2)|~c5_1(X1))). % 30.69/4.39 cnf(i_0_830, plain, (c8_2(a27,X1)|c5_2(a27,X1)|~epred3_0|~c6_2(a24,a26)|~c7_2(a27,X1))). % 30.69/4.39 cnf(i_0_397, negated_conjecture, (c8_0|c7_2(X1,X2)|c1_2(X1,X2)|c7_1(X1)|~c3_1(X1)|~c3_2(X1,X2)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_662, negated_conjecture, (c8_0|c5_0|c1_2(X1,X2)|~c8_2(X1,X2)|~c5_2(X1,X2)|~c6_2(X1,a23)|~c7_2(X1,a22)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_294, negated_conjecture, (c4_1(X1)|c2_2(X2,a94)|c1_1(X1)|c5_0|c6_2(X2,a95)|~c2_1(X2)|~c5_1(X1))). % 30.69/4.39 cnf(i_0_296, negated_conjecture, (c4_1(X1)|c2_2(X2,a94)|c5_2(X2,a95)|c1_1(X1)|c5_0|~c2_1(X2)|~c5_1(X1))). % 30.69/4.39 cnf(i_0_140, negated_conjecture, (c3_1(X1)|c8_2(a113,X2)|c7_2(a113,X2)|c1_2(X1,a114)|~c1_0|~c4_2(a113,X2)|~ndr1_1(a113)|~c7_1(X1))). % 30.69/4.39 cnf(i_0_141, negated_conjecture, (c3_1(X1)|c8_2(a113,X2)|c5_2(X1,a114)|c7_2(a113,X2)|~c1_0|~c4_2(a113,X2)|~ndr1_1(a113)|~c7_1(X1))). % 30.69/4.39 cnf(i_0_139, negated_conjecture, (c3_1(X1)|c8_2(a113,X2)|c8_2(X1,a114)|c7_2(a113,X2)|~c1_0|~c4_2(a113,X2)|~ndr1_1(a113)|~c7_1(X1))). % 30.69/4.39 cnf(i_0_802, plain, (c5_2(X1,X2)|c6_2(X1,a13)|c1_2(X1,X2)|ndr1_1(a14)|~epred2_0|~c1_1(X1)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_837, plain, (c8_2(a27,X1)|c2_2(a24,a26)|c5_2(a27,X1)|~epred3_0|~c7_2(a27,X1))). % 30.69/4.39 cnf(i_0_660, negated_conjecture, (c8_0|c5_0|c1_2(X1,X2)|~c8_2(X1,X2)|~c2_2(X1,a23)|~c5_2(X1,X2)|~c7_2(X1,a22)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_658, negated_conjecture, (c8_0|c5_0|c1_2(X1,X2)|~c8_2(X1,X2)|~c5_2(X1,X2)|~c6_2(X1,a22)|~c6_2(X1,a23)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_657, negated_conjecture, (c8_0|c5_0|c1_2(X1,X2)|~c8_2(X1,X2)|~c5_2(X1,X2)|~c3_2(X1,a23)|~c6_2(X1,a22)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_656, negated_conjecture, (c8_0|c5_0|c1_2(X1,X2)|~c8_2(X1,X2)|~c2_2(X1,a23)|~c5_2(X1,X2)|~c6_2(X1,a22)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_933, plain, (c8_2(a35,X1)|c4_2(a37,a38)|~epred4_0|~c2_2(a35,X1)|~c1_2(a35,X1))). % 30.69/4.39 cnf(i_0_475, negated_conjecture, (c6_1(X1)|c6_2(a64,X2)|c1_2(a64,X2)|c4_2(a64,X2)|~c5_2(X1,a63)|~ndr1_1(a64)|~c7_1(X1))). % 30.69/4.39 cnf(i_0_483, negated_conjecture, (c6_1(X1)|c6_2(a64,X2)|c1_2(a64,X2)|c4_2(a64,X2)|~c2_2(X1,a63)|~ndr1_1(a64)|~c7_1(X1))). % 30.69/4.39 cnf(i_0_489, negated_conjecture, (c6_1(X1)|c8_2(a64,X2)|c4_2(a64,X2)|ndr1_1(X1)|~c2_2(a64,X2)|~ndr1_1(a64)|~c7_1(X1))). % 30.69/4.39 cnf(i_0_637, negated_conjecture, (c1_1(X1)|c6_2(a32,X2)|c1_2(a32,X2)|c4_2(X1,a33)|~c1_0|~c4_1(X1)|~c3_2(a32,X2)|~ndr1_1(a32))). % 30.69/4.39 cnf(i_0_487, negated_conjecture, (c6_1(X1)|c6_2(a64,X2)|c1_2(a64,X2)|c4_2(a64,X2)|ndr1_1(X1)|~ndr1_1(a64)|~c7_1(X1))). % 30.69/4.39 cnf(i_0_813, plain, (c5_2(X1,X2)|c1_2(X1,X2)|~epred2_0|~c2_2(X1,a13)|~c1_1(X1)|~c7_2(a14,a15)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_806, plain, (c5_2(X1,X2)|c1_2(X1,X2)|~epred2_0|~c8_2(X1,a13)|~c1_1(X1)|~c7_2(a14,a15)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_479, negated_conjecture, (c6_1(X1)|c6_2(a64,X2)|c1_2(a64,X2)|c4_2(a64,X2)|c4_2(X1,a63)|~ndr1_1(a64)|~c7_1(X1))). % 30.69/4.39 cnf(i_0_636, negated_conjecture, (c1_1(X1)|c6_2(a32,X2)|c1_2(a32,X2)|c1_2(X1,a33)|~c1_0|~c4_1(X1)|~c3_2(a32,X2)|~ndr1_1(a32))). % 30.69/4.39 cnf(i_0_635, negated_conjecture, (c3_2(X1,a33)|c1_1(X1)|c6_2(a32,X2)|c1_2(a32,X2)|~c1_0|~c4_1(X1)|~c3_2(a32,X2)|~ndr1_1(a32))). % 30.69/4.39 cnf(i_0_481, negated_conjecture, (c6_1(X1)|c8_2(a64,X2)|c4_2(a64,X2)|c4_2(X1,a63)|~c2_2(a64,X2)|~ndr1_1(a64)|~c7_1(X1))). % 30.69/4.39 cnf(i_0_464, negated_conjecture, (c5_2(a66,X1)|c5_2(a65,X2)|c3_2(a66,X1)|c1_2(a65,X2)|c4_2(a65,X2)|~c1_0|~c8_2(a66,X1)|~ndr1_1(a65)|~ndr1_1(a66))). % 30.69/4.39 cnf(i_0_798, plain, (c5_2(X1,X2)|c6_2(X1,a13)|c1_2(X1,X2)|~epred2_0|~c1_1(X1)|~ndr1_1(X1)|~c7_1(a14))). % 30.69/4.39 cnf(i_0_292, negated_conjecture, (c6_1(X1)|c2_2(X1,X2)|c1_1(X1)|c4_2(X1,X2)|c2_1(a96)|~c1_2(X1,X2)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_988, plain, (c1_2(X1,a89)|c5_1(X1)|~epred6_0|~c2_2(a90,X2)|~c6_2(a90,X2)|~c1_2(a90,X2))). % 30.69/4.39 cnf(i_0_1006, plain, (c2_2(X1,a89)|c5_1(X1)|~epred6_0|~c2_2(a90,X2)|~c6_2(a90,X2)|~c1_2(a90,X2))). % 30.69/4.39 cnf(i_0_537, negated_conjecture, (ndr1_1(X1)|c5_1(X2)|~c3_1(X1)|~c2_2(X2,a56)|~c6_2(X2,X3)|~c1_2(X2,X3)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_816, plain, (c5_2(X1,X2)|c1_2(X1,X2)|ndr1_1(a14)|~epred2_0|~c2_2(X1,a13)|~c1_1(X1)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_290, negated_conjecture, (c6_1(X1)|c2_2(X1,X2)|c1_1(X1)|c4_2(X1,X2)|ndr1_1(a96)|~c1_2(X1,X2)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_463, negated_conjecture, (c2_2(a66,X1)|c5_2(a65,X2)|c3_2(a66,X1)|c1_2(a65,X2)|c4_2(a65,X2)|~c1_0|~c8_2(a66,X1)|~ndr1_1(a65)|~ndr1_1(a66))). % 30.69/4.39 cnf(i_0_803, plain, (c5_2(X1,X2)|c6_2(X1,a13)|c1_2(X1,X2)|~epred2_0|~c1_1(X1)|~ndr1_1(X1)|~c2_1(a14))). % 30.69/4.39 cnf(i_0_291, negated_conjecture, (c6_1(X1)|c3_1(a96)|c2_2(X1,X2)|c1_1(X1)|c4_2(X1,X2)|~c1_2(X1,X2)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_809, plain, (c5_2(X1,X2)|c1_2(X1,X2)|ndr1_1(a14)|~epred2_0|~c8_2(X1,a13)|~c1_1(X1)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_755, negated_conjecture, (c2_1(X1)|~c8_0|~c2_2(X1,X2)|~c5_2(X1,X2)|~c1_1(X1)|~c1_1(X3)|~c4_2(X3,a4)|~c4_2(X3,a5)|~c4_2(X1,X2)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_678, negated_conjecture, (c3_1(X1)|c2_2(X1,X2)|c1_1(a18)|c2_1(X1)|~c7_2(X1,X2)|~c1_2(X1,X2)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_679, negated_conjecture, (c6_1(a18)|c3_1(X1)|c2_2(X1,X2)|c2_1(X1)|~c7_2(X1,X2)|~c1_2(X1,X2)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_801, plain, (c5_2(X1,X2)|c6_2(a14,a15)|c6_2(X1,a13)|c1_2(X1,X2)|~epred2_0|~c1_1(X1)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_753, negated_conjecture, (c2_1(X1)|~c8_0|~c2_2(X1,X2)|~c5_2(X3,a5)|~c5_2(X1,X2)|~c1_1(X1)|~c1_1(X3)|~c4_2(X3,a4)|~c4_2(X1,X2)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_747, negated_conjecture, (c2_1(X1)|~c8_0|~c2_2(X1,X2)|~c5_2(X1,X2)|~c1_1(X1)|~c1_1(X3)|~c7_2(X3,a4)|~c4_2(X3,a5)|~c4_2(X1,X2)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_751, negated_conjecture, (c2_1(X1)|~c8_0|~c2_2(X1,X2)|~c5_2(X1,X2)|~c3_2(X3,a4)|~c1_1(X1)|~c1_1(X3)|~c4_2(X3,a5)|~c4_2(X1,X2)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_745, negated_conjecture, (c2_1(X1)|~c8_0|~c2_2(X1,X2)|~c5_2(X3,a5)|~c5_2(X1,X2)|~c1_1(X1)|~c1_1(X3)|~c7_2(X3,a4)|~c4_2(X1,X2)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_289, negated_conjecture, (c6_1(X1)|c2_2(X1,X2)|c1_1(X1)|c7_2(a96,a97)|c4_2(X1,X2)|~c1_2(X1,X2)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_800, plain, (c5_2(X1,X2)|c3_2(a14,a15)|c6_2(X1,a13)|c1_2(X1,X2)|~epred2_0|~c1_1(X1)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_749, negated_conjecture, (c2_1(X1)|~c8_0|~c2_2(X1,X2)|~c5_2(X3,a5)|~c5_2(X1,X2)|~c3_2(X3,a4)|~c1_1(X1)|~c1_1(X3)|~c4_2(X1,X2)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_799, plain, (c5_2(X1,X2)|c6_2(X1,a13)|c1_2(X1,X2)|~epred2_0|~c1_1(X1)|~c7_2(a14,a15)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_716, negated_conjecture, (c1_0|c7_2(X1,X2)|c7_1(X1)|~c8_2(X1,X3)|~c8_2(X1,X2)|~c2_2(X1,X3)|~c4_2(X1,X3)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_287, negated_conjecture, (c6_1(X1)|c2_2(X1,X2)|c1_1(X1)|c4_2(X1,X2)|~c1_2(a96,a97)|~c1_2(X1,X2)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_815, plain, (c5_2(X1,X2)|c6_2(a14,a15)|c1_2(X1,X2)|~epred2_0|~c2_2(X1,a13)|~c1_1(X1)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_288, negated_conjecture, (c6_1(X1)|c2_2(X1,X2)|c1_1(X1)|c4_2(X1,X2)|~c6_2(a96,a97)|~c1_2(X1,X2)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_814, plain, (c5_2(X1,X2)|c3_2(a14,a15)|c1_2(X1,X2)|~epred2_0|~c2_2(X1,a13)|~c1_1(X1)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_807, plain, (c5_2(X1,X2)|c3_2(a14,a15)|c1_2(X1,X2)|~epred2_0|~c8_2(X1,a13)|~c1_1(X1)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_532, negated_conjecture, (c8_0|c5_1(X1)|~c3_1(X2)|~c2_2(X1,a56)|~c3_2(X2,a58)|~c6_2(X1,X3)|~c7_2(X2,a57)|~c1_2(X1,X3)|~c4_2(X1,X3)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_531, negated_conjecture, (c8_0|c5_1(X1)|~c3_1(X2)|~c2_2(X1,a56)|~c5_2(X2,a58)|~c6_2(X1,X3)|~c7_2(X2,a57)|~c1_2(X1,X3)|~c4_2(X1,X3)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_521, negated_conjecture, (c7_2(X1,a56)|ndr1_1(X2)|c5_1(X1)|~c3_1(X2)|~c6_2(X1,X3)|~c1_2(X1,X3)|~c4_2(X1,X3)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_553, negated_conjecture, (c3_2(X1,a56)|ndr1_1(X2)|c5_1(X1)|~c3_1(X2)|~c6_2(X1,X3)|~c1_2(X1,X3)|~c4_2(X1,X3)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_754, negated_conjecture, (c3_2(X1,a5)|c2_1(X2)|~c8_0|~c2_2(X2,X3)|~c5_2(X2,X3)|~c1_1(X2)|~c1_1(X1)|~c4_2(X1,a4)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_746, negated_conjecture, (c3_2(X1,a5)|c2_1(X2)|~c8_0|~c2_2(X2,X3)|~c5_2(X2,X3)|~c1_1(X2)|~c1_1(X1)|~c7_2(X1,a4)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_808, plain, (c5_2(X1,X2)|c6_2(a14,a15)|c1_2(X1,X2)|~epred2_0|~c8_2(X1,a13)|~c1_1(X1)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_494, negated_conjecture, (c5_2(X1,X2)|c1_1(X3)|c6_2(X1,X2)|ndr1_1(a60)|~c4_1(X3)|~c3_1(X1)|~c3_2(X1,X2)|~ndr1_1(X1)|~c2_1(X1))). % 30.69/4.39 cnf(i_0_572, negated_conjecture, (c1_1(X1)|c4_2(X1,X2)|c2_1(X3)|~c6_1(X1)|~c3_1(X3)|~c3_2(X1,X2)|~c6_2(X1,X2)|~ndr1_1(X1)|~c7_1(X3))). % 30.69/4.39 cnf(i_0_750, negated_conjecture, (c3_2(X1,a5)|c2_1(X2)|~c8_0|~c2_2(X2,X3)|~c5_2(X2,X3)|~c3_2(X1,a4)|~c1_1(X2)|~c1_1(X1)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_516, negated_conjecture, (c8_0|c7_2(X1,a56)|c5_1(X1)|~c3_1(X2)|~c3_2(X2,a58)|~c6_2(X1,X3)|~c7_2(X2,a57)|~c1_2(X1,X3)|~c4_2(X1,X3)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_515, negated_conjecture, (c8_0|c7_2(X1,a56)|c5_1(X1)|~c3_1(X2)|~c5_2(X2,a58)|~c6_2(X1,X3)|~c7_2(X2,a57)|~c1_2(X1,X3)|~c4_2(X1,X3)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_548, negated_conjecture, (c8_0|c3_2(X1,a56)|c5_1(X1)|~c3_1(X2)|~c3_2(X2,a58)|~c6_2(X1,X3)|~c7_2(X2,a57)|~c1_2(X1,X3)|~c4_2(X1,X3)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_133, negated_conjecture, (c4_1(X1)|c4_1(X2)|c6_2(X2,X3)|c1_2(X2,X3)|ndr1_1(X1)|c7_1(X2)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_491, negated_conjecture, (c5_2(X1,X2)|c3_2(a60,a62)|c1_1(X3)|c6_2(X1,X2)|~c4_1(X3)|~c3_1(X1)|~c3_2(X1,X2)|~ndr1_1(X1)|~c2_1(X1))). % 30.69/4.39 cnf(i_0_547, negated_conjecture, (c8_0|c3_2(X1,a56)|c5_1(X1)|~c3_1(X2)|~c5_2(X2,a58)|~c6_2(X1,X3)|~c7_2(X2,a57)|~c1_2(X1,X3)|~c4_2(X1,X3)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_681, negated_conjecture, (c8_2(X1,X2)|c5_2(X1,X2)|c1_1(X1)|c7_2(X1,X3)|~c2_2(X1,X2)|~c2_2(X1,X3)|~c5_0|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_493, negated_conjecture, (c5_2(X1,X2)|c1_1(X3)|c6_2(X1,X2)|~c4_1(X3)|~c3_1(X1)|~c3_2(X1,X2)|~c4_2(a60,a62)|~ndr1_1(X1)|~c2_1(X1))). % 30.69/4.39 cnf(i_0_496, negated_conjecture, (c5_2(a60,a61)|c5_2(X1,X2)|c1_1(X3)|c6_2(X1,X2)|~c4_1(X3)|~c3_1(X1)|~c3_2(X1,X2)|~ndr1_1(X1)|~c2_1(X1))). % 30.69/4.39 cnf(i_0_530, negated_conjecture, (c8_0|c6_2(X1,a58)|c5_1(X2)|~c3_1(X1)|~c2_2(X2,a56)|~c6_2(X2,X3)|~c7_2(X1,a57)|~c1_2(X2,X3)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_524, negated_conjecture, (c8_0|c5_2(X1,a57)|c5_1(X2)|~c3_1(X1)|~c2_2(X2,a56)|~c3_2(X1,a58)|~c6_2(X2,X3)|~c1_2(X2,X3)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_523, negated_conjecture, (c8_0|c5_2(X1,a57)|c5_1(X2)|~c3_1(X1)|~c2_2(X2,a56)|~c5_2(X1,a58)|~c6_2(X2,X3)|~c1_2(X2,X3)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_528, negated_conjecture, (c8_0|c2_2(X1,a57)|c5_1(X2)|~c3_1(X1)|~c2_2(X2,a56)|~c3_2(X1,a58)|~c6_2(X2,X3)|~c1_2(X2,X3)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_131, negated_conjecture, (c4_1(X1)|c4_1(X2)|c8_1(X1)|c6_2(X2,X3)|c1_2(X1,a116)|c1_2(X2,X3)|c7_1(X2)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_497, negated_conjecture, (c8_2(a60,a61)|c5_2(X1,X2)|c1_1(X3)|c6_2(X1,X2)|~c4_1(X3)|~c3_1(X1)|~c3_2(X1,X2)|~ndr1_1(X1)|~c2_1(X1))). % 30.69/4.39 cnf(i_0_498, negated_conjecture, (c5_2(X1,X2)|c1_1(X3)|c6_2(X1,X2)|~c4_1(X3)|~c3_1(X1)|~c2_2(a60,a61)|~c3_2(X1,X2)|~ndr1_1(X1)|~c2_1(X1))). % 30.69/4.39 cnf(i_0_132, negated_conjecture, (c4_1(X1)|c4_1(X2)|c8_1(X1)|c2_2(X1,a116)|c6_2(X2,X3)|c1_2(X2,X3)|c7_1(X2)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_527, negated_conjecture, (c8_0|c2_2(X1,a57)|c5_1(X2)|~c3_1(X1)|~c2_2(X2,a56)|~c5_2(X1,a58)|~c6_2(X2,X3)|~c1_2(X2,X3)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_492, negated_conjecture, (c2_2(a60,a62)|c5_2(X1,X2)|c1_1(X3)|c6_2(X1,X2)|~c4_1(X3)|~c3_1(X1)|~c3_2(X1,X2)|~ndr1_1(X1)|~c2_1(X1))). % 30.69/4.39 cnf(i_0_130, negated_conjecture, (c4_1(X1)|c4_1(X2)|c8_1(X1)|c6_2(X2,X3)|c1_2(X2,X3)|c7_1(X2)|~c5_2(X1,a116)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_735, negated_conjecture, (c3_2(X1,X2)|c5_0|c1_2(X1,a7)|c4_2(X1,X2)|~c8_1(X1)|~c3_1(X3)|~c2_2(X1,X2)|~c7_2(X3,a6)|~c2_1(X3))). % 30.69/4.39 cnf(i_0_743, negated_conjecture, (c3_2(X1,X2)|c5_0|c1_2(X1,a7)|c4_2(X1,X2)|ndr1_1(X3)|~c8_1(X1)|~c3_1(X3)|~c2_2(X1,X2)|~c2_1(X3))). % 30.69/4.39 cnf(i_0_205, negated_conjecture, (c8_2(a104,X1)|c5_2(X2,X3)|c5_0|c6_2(X2,X3)|~c6_1(X2)|~c2_2(X2,X3)|~c1_2(a104,X1)|~ndr1_1(a104)|~ndr1_1(X2)|~c2_1(X2))). % 30.69/4.39 cnf(i_0_514, negated_conjecture, (c8_0|c6_2(X1,a58)|c7_2(X2,a56)|c5_1(X2)|~c3_1(X1)|~c6_2(X2,X3)|~c7_2(X1,a57)|~c1_2(X2,X3)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_508, negated_conjecture, (c8_0|c5_2(X1,a57)|c7_2(X2,a56)|c5_1(X2)|~c3_1(X1)|~c3_2(X1,a58)|~c6_2(X2,X3)|~c1_2(X2,X3)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_507, negated_conjecture, (c8_0|c5_2(X1,a57)|c7_2(X2,a56)|c5_1(X2)|~c3_1(X1)|~c5_2(X1,a58)|~c6_2(X2,X3)|~c1_2(X2,X3)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_742, negated_conjecture, (c3_2(X1,X2)|c5_0|c6_2(X1,a7)|c4_2(X1,X2)|ndr1_1(X3)|~c8_1(X1)|~c3_1(X3)|~c2_2(X1,X2)|~c2_1(X3))). % 30.69/4.39 cnf(i_0_741, negated_conjecture, (c3_2(X1,a7)|c3_2(X1,X2)|c5_0|c4_2(X1,X2)|ndr1_1(X3)|~c8_1(X1)|~c3_1(X3)|~c2_2(X1,X2)|~c2_1(X3))). % 30.69/4.39 cnf(i_0_734, negated_conjecture, (c3_2(X1,X2)|c5_0|c6_2(X1,a7)|c4_2(X1,X2)|~c8_1(X1)|~c3_1(X3)|~c2_2(X1,X2)|~c7_2(X3,a6)|~c2_1(X3))). % 30.69/4.39 cnf(i_0_733, negated_conjecture, (c3_2(X1,a7)|c3_2(X1,X2)|c5_0|c4_2(X1,X2)|~c8_1(X1)|~c3_1(X3)|~c2_2(X1,X2)|~c7_2(X3,a6)|~c2_1(X3))). % 30.69/4.39 cnf(i_0_512, negated_conjecture, (c8_0|c2_2(X1,a57)|c7_2(X2,a56)|c5_1(X2)|~c3_1(X1)|~c3_2(X1,a58)|~c6_2(X2,X3)|~c1_2(X2,X3)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_511, negated_conjecture, (c8_0|c2_2(X1,a57)|c7_2(X2,a56)|c5_1(X2)|~c3_1(X1)|~c5_2(X1,a58)|~c6_2(X2,X3)|~c1_2(X2,X3)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_739, negated_conjecture, (c2_2(X1,a6)|c3_2(X2,X3)|c5_0|c1_2(X2,a7)|c4_2(X2,X3)|~c8_1(X2)|~c3_1(X1)|~c2_2(X2,X3)|~c2_1(X1))). % 30.69/4.39 cnf(i_0_546, negated_conjecture, (c8_0|c3_2(X1,a56)|c6_2(X2,a58)|c5_1(X1)|~c3_1(X2)|~c6_2(X1,X3)|~c7_2(X2,a57)|~c1_2(X1,X3)|~c4_2(X1,X3)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_522, negated_conjecture, (c8_0|c5_2(X1,a57)|c6_2(X1,a58)|c5_1(X2)|~c3_1(X1)|~c2_2(X2,a56)|~c6_2(X2,X3)|~c1_2(X2,X3)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_526, negated_conjecture, (c8_0|c2_2(X1,a57)|c6_2(X1,a58)|c5_1(X2)|~c3_1(X1)|~c2_2(X2,a56)|~c6_2(X2,X3)|~c1_2(X2,X3)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_540, negated_conjecture, (c8_0|c5_2(X1,a57)|c3_2(X2,a56)|c5_1(X2)|~c3_1(X1)|~c3_2(X1,a58)|~c6_2(X2,X3)|~c1_2(X2,X3)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_731, negated_conjecture, (c8_2(X1,a6)|c3_2(X2,X3)|c5_0|c1_2(X2,a7)|c4_2(X2,X3)|~c8_1(X2)|~c3_1(X1)|~c2_2(X2,X3)|~c2_1(X1))). % 30.69/4.39 cnf(i_0_738, negated_conjecture, (c2_2(X1,a6)|c3_2(X2,X3)|c5_0|c6_2(X2,a7)|c4_2(X2,X3)|~c8_1(X2)|~c3_1(X1)|~c2_2(X2,X3)|~c2_1(X1))). % 30.69/4.39 cnf(i_0_539, negated_conjecture, (c8_0|c5_2(X1,a57)|c3_2(X2,a56)|c5_1(X2)|~c3_1(X1)|~c5_2(X1,a58)|~c6_2(X2,X3)|~c1_2(X2,X3)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_544, negated_conjecture, (c8_0|c2_2(X1,a57)|c3_2(X2,a56)|c5_1(X2)|~c3_1(X1)|~c3_2(X1,a58)|~c6_2(X2,X3)|~c1_2(X2,X3)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_543, negated_conjecture, (c8_0|c2_2(X1,a57)|c3_2(X2,a56)|c5_1(X2)|~c3_1(X1)|~c5_2(X1,a58)|~c6_2(X2,X3)|~c1_2(X2,X3)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_281, negated_conjecture, (c3_2(X1,X2)|c6_2(X3,X4)|c7_1(X1)|~c8_0|~c2_2(X3,X4)|~c5_2(X1,X2)|~c6_2(X3,a99)|~c1_2(X1,X2)|~c1_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3)|~c2_1(X1))). % 30.69/4.39 cnf(i_0_730, negated_conjecture, (c8_2(X1,a6)|c3_2(X2,X3)|c5_0|c6_2(X2,a7)|c4_2(X2,X3)|~c8_1(X2)|~c3_1(X1)|~c2_2(X2,X3)|~c2_1(X1))). % 30.69/4.39 cnf(i_0_737, negated_conjecture, (c2_2(X1,a6)|c3_2(X2,a7)|c3_2(X2,X3)|c5_0|c4_2(X2,X3)|~c8_1(X2)|~c3_1(X1)|~c2_2(X2,X3)|~c2_1(X1))). % 30.69/4.39 cnf(i_0_729, negated_conjecture, (c8_2(X1,a6)|c3_2(X2,a7)|c3_2(X2,X3)|c5_0|c4_2(X2,X3)|~c8_1(X2)|~c3_1(X1)|~c2_2(X2,X3)|~c2_1(X1))). % 30.69/4.39 cnf(i_0_280, negated_conjecture, (c3_2(X1,X2)|c6_2(X3,X4)|c7_1(X1)|~c8_0|~c2_2(X3,X4)|~c5_2(X3,a99)|~c5_2(X1,X2)|~c1_2(X1,X2)|~c1_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3)|~c2_1(X1))). % 30.69/4.39 cnf(i_0_42, negated_conjecture, (c8_1(X1)|c3_2(X2,X3)|c7_2(X2,X3)|c2_1(X1)|~c6_1(X4)|~c4_1(X4)|~c8_1(X2)|~c2_2(X2,X3)|~c1_1(X2)|~c5_1(X4)|~c7_1(X1))). % 30.69/4.39 cnf(i_0_506, negated_conjecture, (c8_0|c5_2(X1,a57)|c6_2(X1,a58)|c7_2(X2,a56)|c5_1(X2)|~c3_1(X1)|~c6_2(X2,X3)|~c1_2(X2,X3)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_510, negated_conjecture, (c8_0|c2_2(X1,a57)|c6_2(X1,a58)|c7_2(X2,a56)|c5_1(X2)|~c3_1(X1)|~c6_2(X2,X3)|~c1_2(X2,X3)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_538, negated_conjecture, (c8_0|c5_2(X1,a57)|c3_2(X2,a56)|c6_2(X1,a58)|c5_1(X2)|~c3_1(X1)|~c6_2(X2,X3)|~c1_2(X2,X3)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_542, negated_conjecture, (c8_0|c2_2(X1,a57)|c3_2(X2,a56)|c6_2(X1,a58)|c5_1(X2)|~c3_1(X1)|~c6_2(X2,X3)|~c1_2(X2,X3)|~c4_2(X2,X3)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_84, negated_conjecture, (c3_1(a127)|c8_2(X1,X2)|c3_2(X1,X3)|c6_2(X1,X2)|c4_2(X1,X3)|~c4_1(X1)|~c8_2(X1,X3)|~c7_2(X1,X2)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_85, negated_conjecture, (c8_1(a127)|c8_2(X1,X2)|c3_2(X1,X3)|c6_2(X1,X2)|c4_2(X1,X3)|~c4_1(X1)|~c8_2(X1,X3)|~c7_2(X1,X2)|~ndr1_1(X1))). % 30.69/4.39 cnf(i_0_83, negated_conjecture, (c8_2(X1,X2)|c3_2(X1,X3)|c6_2(X1,X2)|c4_2(X1,X3)|~c4_1(X1)|~c8_2(X1,X3)|~c7_2(X1,X2)|~ndr1_1(X1)|~c5_1(a127))). % 30.69/4.39 cnf(i_0_279, negated_conjecture, (c3_2(X1,X2)|c6_2(X3,X4)|c4_2(X3,a99)|c7_1(X1)|~c8_0|~c2_2(X3,X4)|~c5_2(X1,X2)|~c1_2(X1,X2)|~c1_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3)|~c2_1(X1))). % 30.69/4.39 cnf(i_0_495, negated_conjecture, (c5_2(a60,X1)|c5_2(X2,X3)|c1_1(X4)|c6_2(X2,X3)|~c4_1(X4)|~c3_1(X2)|~c2_2(a60,X1)|~c3_2(X2,X3)|~c7_2(a60,X1)|~ndr1_1(X2)|~c2_1(X2))). % 30.69/4.39 cnf(i_0_240, negated_conjecture, (c8_1(X1)|c2_2(X2,X3)|c5_2(X1,a100)|c7_2(X2,a102)|c7_2(X2,a101)|c7_2(X1,X4)|c4_2(X2,X3)|c4_2(X1,X4)|~c2_2(X1,X4)|~c5_0|~ndr1_1(X1)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_235, negated_conjecture, (c8_1(X1)|c2_2(X2,X3)|c5_2(X1,a100)|c7_2(X1,X4)|c4_2(X2,X3)|c4_2(X1,X4)|~c2_2(X2,a101)|~c2_2(X1,X4)|~c5_0|~c1_2(X2,a102)|~ndr1_1(X1)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_219, negated_conjecture, (c8_1(X1)|c2_2(X1,a100)|c2_2(X2,X3)|c7_2(X1,X4)|c4_2(X2,X3)|c4_2(X1,X4)|~c2_2(X2,a101)|~c2_2(X1,X4)|~c5_0|~c1_2(X2,a102)|~ndr1_1(X1)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_278, negated_conjecture, (c4_1(X1)|c3_1(X1)|c2_2(X2,X3)|c6_2(X2,X3)|c7_2(X2,X4)|c7_1(X2)|~c1_0|~c8_2(X2,X4)|~c5_2(X2,X4)|~c3_2(X2,X3)|~c1_1(X1)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_239, negated_conjecture, (c8_1(X1)|c2_2(X2,X3)|c5_2(X1,a100)|c7_2(X2,a101)|c7_2(X1,X4)|c4_2(X2,X3)|c4_2(X1,X4)|~c2_2(X1,X4)|~c5_0|~c1_2(X2,a102)|~ndr1_1(X1)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_248, negated_conjecture, (c8_1(X1)|c2_2(X2,X3)|c7_2(X2,a102)|c7_2(X1,X4)|c4_2(X2,a101)|c4_2(X1,a100)|c4_2(X2,X3)|c4_2(X1,X4)|~c2_2(X1,X4)|~c5_0|~ndr1_1(X1)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_224, negated_conjecture, (c8_1(X1)|c2_2(X1,a100)|c2_2(X2,X3)|c7_2(X2,a102)|c7_2(X2,a101)|c7_2(X1,X4)|c4_2(X2,X3)|c4_2(X1,X4)|~c2_2(X1,X4)|~c5_0|~ndr1_1(X1)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_327, negated_conjecture, (c3_1(X1)|c8_2(X2,X3)|c7_2(X2,X3)|c1_2(X1,X4)|c4_2(X1,X4)|ndr1_1(X5)|~c6_2(X1,X4)|~c4_2(X2,X3)|~ndr1_1(X1)|~ndr1_1(X2)|~c2_1(X1)|~c5_1(X2)|~c7_1(X2)|~c7_1(X5))). % 30.69/4.39 cnf(i_0_234, negated_conjecture, (c8_1(X1)|c2_2(X2,X3)|c5_2(X1,a100)|c7_2(X1,X4)|c4_2(X2,X3)|c4_2(X1,X4)|~c2_2(X2,a101)|~c2_2(X1,X4)|~c5_0|~c4_2(X2,a102)|~ndr1_1(X1)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_218, negated_conjecture, (c8_1(X1)|c2_2(X1,a100)|c2_2(X2,X3)|c7_2(X1,X4)|c4_2(X2,X3)|c4_2(X1,X4)|~c2_2(X2,a101)|~c2_2(X1,X4)|~c5_0|~c4_2(X2,a102)|~ndr1_1(X1)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_223, negated_conjecture, (c8_1(X1)|c2_2(X1,a100)|c2_2(X2,X3)|c7_2(X2,a101)|c7_2(X1,X4)|c4_2(X2,X3)|c4_2(X1,X4)|~c2_2(X1,X4)|~c5_0|~c1_2(X2,a102)|~ndr1_1(X1)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_236, negated_conjecture, (c8_1(X1)|c2_2(X2,X3)|c5_2(X1,a100)|c7_2(X2,a102)|c7_2(X1,X4)|c4_2(X2,X3)|c4_2(X1,X4)|~c2_2(X2,a101)|~c2_2(X1,X4)|~c5_0|~ndr1_1(X1)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_220, negated_conjecture, (c8_1(X1)|c2_2(X1,a100)|c2_2(X2,X3)|c7_2(X2,a102)|c7_2(X1,X4)|c4_2(X2,X3)|c4_2(X1,X4)|~c2_2(X2,a101)|~c2_2(X1,X4)|~c5_0|~ndr1_1(X1)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_251, negated_conjecture, (c8_1(X1)|c2_2(X2,X3)|c7_2(X1,X4)|c4_2(X1,a100)|c4_2(X2,X3)|c4_2(X1,X4)|~c2_2(X2,a101)|~c2_2(X1,X4)|~c5_0|~c1_2(X2,a102)|~ndr1_1(X1)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_230, negated_conjecture, (c8_1(X1)|c2_2(X2,X3)|c5_2(X1,a100)|c7_2(X1,X4)|c4_2(X2,a101)|c4_2(X2,X3)|c4_2(X1,X4)|~c2_2(X1,X4)|~c5_0|~c4_2(X2,a102)|~ndr1_1(X1)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_214, negated_conjecture, (c8_1(X1)|c2_2(X1,a100)|c2_2(X2,X3)|c7_2(X1,X4)|c4_2(X2,a101)|c4_2(X2,X3)|c4_2(X1,X4)|~c2_2(X1,X4)|~c5_0|~c4_2(X2,a102)|~ndr1_1(X1)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_256, negated_conjecture, (c8_1(X1)|c2_2(X2,X3)|c7_2(X2,a102)|c7_2(X2,a101)|c7_2(X1,X4)|c4_2(X1,a100)|c4_2(X2,X3)|c4_2(X1,X4)|~c2_2(X1,X4)|~c5_0|~ndr1_1(X1)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_232, negated_conjecture, (c8_1(X1)|c2_2(X2,X3)|c5_2(X1,a100)|c7_2(X2,a102)|c7_2(X1,X4)|c4_2(X2,a101)|c4_2(X2,X3)|c4_2(X1,X4)|~c2_2(X1,X4)|~c5_0|~ndr1_1(X1)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_238, negated_conjecture, (c8_1(X1)|c2_2(X2,X3)|c5_2(X1,a100)|c7_2(X2,a101)|c7_2(X1,X4)|c4_2(X2,X3)|c4_2(X1,X4)|~c2_2(X1,X4)|~c5_0|~c4_2(X2,a102)|~ndr1_1(X1)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_222, negated_conjecture, (c8_1(X1)|c2_2(X1,a100)|c2_2(X2,X3)|c7_2(X2,a101)|c7_2(X1,X4)|c4_2(X2,X3)|c4_2(X1,X4)|~c2_2(X1,X4)|~c5_0|~c4_2(X2,a102)|~ndr1_1(X1)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_250, negated_conjecture, (c8_1(X1)|c2_2(X2,X3)|c7_2(X1,X4)|c4_2(X1,a100)|c4_2(X2,X3)|c4_2(X1,X4)|~c2_2(X2,a101)|~c2_2(X1,X4)|~c5_0|~c4_2(X2,a102)|~ndr1_1(X1)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_216, negated_conjecture, (c8_1(X1)|c2_2(X1,a100)|c2_2(X2,X3)|c7_2(X2,a102)|c7_2(X1,X4)|c4_2(X2,a101)|c4_2(X2,X3)|c4_2(X1,X4)|~c2_2(X1,X4)|~c5_0|~ndr1_1(X1)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_255, negated_conjecture, (c8_1(X1)|c2_2(X2,X3)|c7_2(X2,a101)|c7_2(X1,X4)|c4_2(X1,a100)|c4_2(X2,X3)|c4_2(X1,X4)|~c2_2(X1,X4)|~c5_0|~c1_2(X2,a102)|~ndr1_1(X1)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_252, negated_conjecture, (c8_1(X1)|c2_2(X2,X3)|c7_2(X2,a102)|c7_2(X1,X4)|c4_2(X1,a100)|c4_2(X2,X3)|c4_2(X1,X4)|~c2_2(X2,a101)|~c2_2(X1,X4)|~c5_0|~ndr1_1(X1)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_231, negated_conjecture, (c8_1(X1)|c2_2(X2,X3)|c5_2(X1,a100)|c7_2(X1,X4)|c4_2(X2,a101)|c4_2(X2,X3)|c4_2(X1,X4)|~c2_2(X1,X4)|~c5_0|~c1_2(X2,a102)|~ndr1_1(X1)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_215, negated_conjecture, (c8_1(X1)|c2_2(X1,a100)|c2_2(X2,X3)|c7_2(X1,X4)|c4_2(X2,a101)|c4_2(X2,X3)|c4_2(X1,X4)|~c2_2(X1,X4)|~c5_0|~c1_2(X2,a102)|~ndr1_1(X1)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_246, negated_conjecture, (c8_1(X1)|c2_2(X2,X3)|c7_2(X1,X4)|c4_2(X2,a101)|c4_2(X1,a100)|c4_2(X2,X3)|c4_2(X1,X4)|~c2_2(X1,X4)|~c5_0|~c4_2(X2,a102)|~ndr1_1(X1)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_247, negated_conjecture, (c8_1(X1)|c2_2(X2,X3)|c7_2(X1,X4)|c4_2(X2,a101)|c4_2(X1,a100)|c4_2(X2,X3)|c4_2(X1,X4)|~c2_2(X1,X4)|~c5_0|~c1_2(X2,a102)|~ndr1_1(X1)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_317, negated_conjecture, (c3_1(X1)|c8_2(X2,X3)|c7_2(X2,X3)|c1_2(X4,a87)|c1_2(X1,X5)|c4_2(X1,X5)|~c6_2(X1,X5)|~c7_2(X4,a88)|~c4_2(X2,X3)|~ndr1_1(X1)|~ndr1_1(X2)|~c2_1(X1)|~c5_1(X2)|~c7_1(X2)|~c7_1(X4))). % 30.69/4.39 cnf(i_0_320, negated_conjecture, (c3_1(X1)|c8_2(X2,X3)|c5_2(X4,a87)|c7_2(X2,X3)|c1_2(X1,X5)|c4_2(X1,X5)|~c6_2(X1,X5)|~c7_2(X4,a88)|~c4_2(X2,X3)|~ndr1_1(X1)|~ndr1_1(X2)|~c2_1(X1)|~c5_1(X2)|~c7_1(X2)|~c7_1(X4))). % 30.69/4.39 cnf(i_0_254, negated_conjecture, (c8_1(X1)|c2_2(X2,X3)|c7_2(X2,a101)|c7_2(X1,X4)|c4_2(X1,a100)|c4_2(X2,X3)|c4_2(X1,X4)|~c2_2(X1,X4)|~c5_0|~c4_2(X2,a102)|~ndr1_1(X1)|~ndr1_1(X2))). % 30.69/4.39 cnf(i_0_323, negated_conjecture, (c3_1(X1)|c8_2(X2,a87)|c8_2(X3,X4)|c7_2(X3,X4)|c1_2(X1,X5)|c4_2(X1,X5)|~c6_2(X1,X5)|~c7_2(X2,a88)|~c4_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3)|~c2_1(X1)|~c5_1(X3)|~c7_1(X3)|~c7_1(X2))). % 30.69/4.39 cnf(i_0_316, negated_conjecture, (c3_1(X1)|c8_2(X2,X3)|c7_2(X2,X3)|c1_2(X4,a88)|c1_2(X4,a87)|c1_2(X1,X5)|c4_2(X1,X5)|~c6_2(X1,X5)|~c4_2(X2,X3)|~ndr1_1(X1)|~ndr1_1(X2)|~c2_1(X1)|~c5_1(X2)|~c7_1(X2)|~c7_1(X4))). % 30.69/4.39 cnf(i_0_319, negated_conjecture, (c3_1(X1)|c8_2(X2,X3)|c5_2(X4,a87)|c7_2(X2,X3)|c1_2(X4,a88)|c1_2(X1,X5)|c4_2(X1,X5)|~c6_2(X1,X5)|~c4_2(X2,X3)|~ndr1_1(X1)|~ndr1_1(X2)|~c2_1(X1)|~c5_1(X2)|~c7_1(X2)|~c7_1(X4))). % 30.69/4.39 cnf(i_0_322, negated_conjecture, (c3_1(X1)|c8_2(X2,a87)|c8_2(X3,X4)|c7_2(X3,X4)|c1_2(X2,a88)|c1_2(X1,X5)|c4_2(X1,X5)|~c6_2(X1,X5)|~c4_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3)|~c2_1(X1)|~c5_1(X3)|~c7_1(X3)|~c7_1(X2))). % 30.69/4.39 cnf(i_0_603, negated_conjecture, (c3_1(X1)|c8_2(X1,X2)|c5_2(X3,X4)|c5_2(X1,X2)|c3_2(X1,X5)|c6_2(X1,X5)|c1_2(X1,X2)|c4_2(X3,X4)|c4_2(X1,X5)|~c3_2(X3,a46)|~c6_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3)|~c2_1(a44)|~c7_1(X3))). % 30.69/4.39 cnf(i_0_604, negated_conjecture, (c3_1(X1)|c8_2(X1,X2)|c5_2(X3,X4)|c5_2(X1,X2)|c3_2(X1,X5)|c6_2(X1,X5)|c1_2(X1,X2)|c4_2(X3,X4)|c4_2(X1,X5)|~c8_2(X3,a46)|~c6_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3)|~c2_1(a44)|~c7_1(X3))). % 30.69/4.39 cnf(i_0_594, negated_conjecture, (c3_1(X1)|c8_2(X1,X2)|c5_2(X3,X4)|c5_2(X1,X2)|c3_2(X1,X5)|c6_2(X1,X5)|c1_2(X1,X2)|c4_2(X3,X4)|c4_2(X1,X5)|~c8_2(a44,a45)|~c3_2(X3,a46)|~c6_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3)|~c7_1(X3))). % 30.69/4.39 cnf(i_0_595, negated_conjecture, (c3_1(X1)|c8_2(X1,X2)|c5_2(X3,X4)|c5_2(X1,X2)|c3_2(X1,X5)|c6_2(X1,X5)|c1_2(X1,X2)|c4_2(X3,X4)|c4_2(X1,X5)|~c8_2(a44,a45)|~c8_2(X3,a46)|~c6_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3)|~c7_1(X3))). % 30.69/4.39 cnf(i_0_600, negated_conjecture, (c3_1(X1)|c8_2(X1,X2)|c5_2(X3,X4)|c5_2(X1,X2)|c3_2(X1,X5)|c6_2(X1,X5)|c1_2(X1,X2)|c4_2(X3,X4)|c4_2(X1,X5)|ndr1_1(a44)|~c3_2(X3,a46)|~c6_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3)|~c7_1(X3))). % 30.69/4.39 cnf(i_0_601, negated_conjecture, (c3_1(X1)|c8_2(X1,X2)|c5_2(X3,X4)|c5_2(X1,X2)|c3_2(X1,X5)|c6_2(X1,X5)|c1_2(X1,X2)|c4_2(X3,X4)|c4_2(X1,X5)|ndr1_1(a44)|~c8_2(X3,a46)|~c6_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3)|~c7_1(X3))). % 30.69/4.39 cnf(i_0_597, negated_conjecture, (c3_1(X1)|c8_2(X1,X2)|c5_2(a44,a45)|c5_2(X3,X4)|c5_2(X1,X2)|c3_2(X1,X5)|c6_2(X1,X5)|c1_2(X1,X2)|c4_2(X3,X4)|c4_2(X1,X5)|~c3_2(X3,a46)|~c6_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3)|~c7_1(X3))). % 30.69/4.39 cnf(i_0_598, negated_conjecture, (c3_1(X1)|c8_2(X1,X2)|c5_2(a44,a45)|c5_2(X3,X4)|c5_2(X1,X2)|c3_2(X1,X5)|c6_2(X1,X5)|c1_2(X1,X2)|c4_2(X3,X4)|c4_2(X1,X5)|~c8_2(X3,a46)|~c6_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3)|~c7_1(X3))). % 30.69/4.39 cnf(i_0_591, negated_conjecture, (c3_1(X1)|c8_2(X1,X2)|c5_2(X3,X4)|c5_2(X1,X2)|c3_2(X1,X5)|c6_2(X1,X5)|c1_2(X1,X2)|c4_2(X3,X4)|c4_2(X1,X5)|~c5_2(a44,X6)|~c3_2(X3,a46)|~c6_2(X3,X4)|~c4_2(a44,X6)|~ndr1_1(X1)|~ndr1_1(X3)|~c7_1(X3))). % 30.69/4.39 cnf(i_0_592, negated_conjecture, (c3_1(X1)|c8_2(X1,X2)|c5_2(X3,X4)|c5_2(X1,X2)|c3_2(X1,X5)|c6_2(X1,X5)|c1_2(X1,X2)|c4_2(X3,X4)|c4_2(X1,X5)|~c8_2(X3,a46)|~c5_2(a44,X6)|~c6_2(X3,X4)|~c4_2(a44,X6)|~ndr1_1(X1)|~ndr1_1(X3)|~c7_1(X3))). % 30.69/4.39 # End listing active clauses. There is an equivalent clause to each of these in the clausification! % 30.69/4.39 # Begin printing tableau % 30.69/4.39 # Found 6 steps % 30.69/4.39 cnf(i_0_96, negated_conjecture, (~c1_1(a122)), inference(start_rule)). % 30.69/4.39 cnf(i_0_3450, plain, (~c1_1(a122)), inference(extension_rule, [i_0_291])). % 30.69/4.39 cnf(i_0_2796977, plain, (~ndr1_1(a122)), inference(closure_rule, [i_0_101])). % 30.69/4.39 cnf(i_0_2796971, plain, (c6_1(a122)), inference(extension_rule, [i_0_42])). % 30.69/4.39 cnf(i_0_2798982, plain, (c2_1(a117)), inference(closure_rule, [i_0_127])). % 30.69/4.39 cnf(i_0_2798985, plain, (~c8_1(a117)), inference(closure_rule, [i_0_126])). % 30.69/4.39 # End printing tableau % 30.69/4.39 # SZS output end % 30.69/4.39 # Branches closed with saturation will be marked with an "s" % 30.69/4.40 # Child (9650) has found a proof. % 30.69/4.40 % 30.69/4.40 # Proof search is over... % 30.69/4.40 # Freeing feature tree %------------------------------------------------------------------------------