%------------------------------------------------------------------------------ % File : Etableau---0.67 % Problem : SYN547+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 : n010.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:22 EDT 2022 % Result : CounterSatisfiable 23.51s 3.56s % Output : CNFRefutation 23.51s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SYN547+1 : TPTP v8.1.0. Released v2.1.0. % 0.06/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 : n010.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 23:53:45 EDT 2022 % 0.12/0.34 % CPUTime : % 0.36/0.53 # No SInE strategy applied % 0.36/0.53 # Auto-Mode selected heuristic G_E___208_C02AMC_F1_SE_CS_SP_PS_S5PRR_RG_S04AN % 0.36/0.53 # and selection function SelectComplexExceptUniqMaxHorn. % 0.36/0.53 # % 0.36/0.53 # Presaturation interreduction done % 0.36/0.53 # Number of axioms: 975 Number of unprocessed: 600 % 0.36/0.53 # Tableaux proof search. % 0.36/0.53 # APR header successfully linked. % 0.36/0.53 # Hello from C++ % 0.38/0.56 # The folding up rule is enabled... % 0.38/0.56 # Local unification is enabled... % 0.38/0.56 # Any saturation attempts will use folding labels... % 0.38/0.56 # 600 beginning clauses after preprocessing and clausification % 0.38/0.56 # Creating start rules for all 509 conjectures. % 0.38/0.56 # There are 509 start rule candidates: % 0.38/0.56 # Found 18 unit axioms. % 0.38/0.56 # Unsuccessfully attempted saturation on 1 start tableaux, moving on. % 0.38/0.56 # 509 start rule tableaux created. % 0.38/0.56 # 582 extension rule candidate clauses % 0.38/0.56 # 18 unit axiom clauses % 0.38/0.56 % 0.38/0.56 # Requested 8, 32 cores available to the main process. % 23.51/3.55 # 6920 Satisfiable branch % 23.51/3.56 # Satisfiable branch found. % 23.51/3.56 # There were 1 total branch saturation attempts. % 23.51/3.56 # There were 0 of these attempts blocked. % 23.51/3.56 # There were 0 deferred branch saturation attempts. % 23.51/3.56 # There were 0 free duplicated saturations. % 23.51/3.56 # There were 0 total successful branch saturations. % 23.51/3.56 # There were 0 successful branch saturations in interreduction. % 23.51/3.56 # There were 0 successful branch saturations on the branch. % 23.51/3.56 # There were 0 successful branch saturations after the branch. % 23.51/3.56 # SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 23.51/3.56 # SZS output start for /export/starexec/sandbox/benchmark/theBenchmark.p % 23.51/3.56 # Begin clausification derivation % 23.51/3.56 % 23.51/3.56 # End clausification derivation % 23.51/3.56 # Begin listing active clauses obtained from FOF to CNF conversion % 23.51/3.56 cnf(i_0_25, negated_conjecture, (ndr1_0)). % 23.51/3.56 cnf(i_0_1047, negated_conjecture, (c3_0)). % 23.51/3.56 cnf(i_0_26, negated_conjecture, (c6_0)). % 23.51/3.56 cnf(i_0_940, negated_conjecture, (c8_0)). % 23.51/3.56 cnf(i_0_135, negated_conjecture, (c4_1(a570))). % 23.51/3.56 cnf(i_0_133, negated_conjecture, (ndr1_1(a570))). % 23.51/3.56 cnf(i_0_134, negated_conjecture, (c5_1(a570))). % 23.51/3.56 cnf(i_0_130, negated_conjecture, (c3_2(a570,a571))). % 23.51/3.56 cnf(i_0_131, negated_conjecture, (c1_2(a570,a571))). % 23.51/3.56 cnf(i_0_132, negated_conjecture, (c2_2(a570,a571))). % 23.51/3.56 cnf(i_0_579, negated_conjecture, (ndr1_1(a520))). % 23.51/3.56 cnf(i_0_577, negated_conjecture, (c2_2(a520,a521))). % 23.51/3.56 cnf(i_0_1084, negated_conjecture, (~c5_0)). % 23.51/3.56 cnf(i_0_271, negated_conjecture, (~c1_0)). % 23.51/3.56 cnf(i_0_580, negated_conjecture, (~c2_1(a520))). % 23.51/3.56 cnf(i_0_581, negated_conjecture, (~c5_1(a520))). % 23.51/3.56 cnf(i_0_578, negated_conjecture, (~c4_2(a520,a521))). % 23.51/3.56 cnf(i_0_576, negated_conjecture, (~c1_2(a520,a521))). % 23.51/3.56 cnf(i_0_75, negated_conjecture, (~c4_0|~c7_0)). % 23.51/3.56 cnf(i_0_81, negated_conjecture, (~c6_1(a581)|~c2_0)). % 23.51/3.56 cnf(i_0_1085, negated_conjecture, (~c8_1(a466)|~c2_0)). % 23.51/3.56 cnf(i_0_1077, negated_conjecture, (~c4_0|~c4_1(a468))). % 23.51/3.56 cnf(i_0_267, negated_conjecture, (~c4_0|~c2_1(a561))). % 23.51/3.56 cnf(i_0_1076, negated_conjecture, (~c4_0|~c3_1(a468))). % 23.51/3.56 cnf(i_0_268, negated_conjecture, (~c4_0|~c5_1(a561))). % 23.51/3.56 cnf(i_0_933, negated_conjecture, (~c4_0|~c2_1(a496))). % 23.51/3.56 cnf(i_0_1078, negated_conjecture, (c6_1(a468)|~c4_0)). % 23.51/3.56 cnf(i_0_279, negated_conjecture, (c6_1(a558)|~c7_0)). % 23.51/3.56 cnf(i_0_80, negated_conjecture, (c8_1(a581)|~c2_0)). % 23.51/3.56 cnf(i_0_10, negated_conjecture, (c2_0|~c7_0)). % 23.51/3.56 cnf(i_0_321, negated_conjecture, (~c4_0|~c2_1(a549))). % 23.51/3.56 cnf(i_0_1086, negated_conjecture, (c1_1(a466)|~c2_0)). % 23.51/3.56 cnf(i_0_280, negated_conjecture, (c1_1(a558)|~c7_0)). % 23.51/3.56 cnf(i_0_19, negated_conjecture, (c3_1(a600)|~c1_1(a601))). % 23.51/3.56 cnf(i_0_943, negated_conjecture, (epred1_0|~c3_2(a494,a495))). % 23.51/3.56 cnf(i_0_916, negated_conjecture, (epred2_0|~c4_0|~c2_1(a505))). % 23.51/3.56 cnf(i_0_1341, plain, (~epred4_0|~c1_1(a597)|~c6_1(a596))). % 23.51/3.56 cnf(i_0_327, negated_conjecture, (~c4_0|~c1_2(a549,a550))). % 23.51/3.56 cnf(i_0_936, negated_conjecture, (~c4_0|~c4_2(a496,a497))). % 23.51/3.56 cnf(i_0_941, negated_conjecture, (epred1_0|c4_1(a494))). % 23.51/3.56 cnf(i_0_944, negated_conjecture, (epred1_0|ndr1_1(a494))). % 23.51/3.56 cnf(i_0_945, negated_conjecture, (epred1_0|c1_1(a494))). % 23.51/3.56 cnf(i_0_20, negated_conjecture, (c7_1(a601)|c3_1(a600))). % 23.51/3.56 cnf(i_0_1280, plain, (ndr1_1(X1)|~epred2_0)). % 23.51/3.56 cnf(i_0_18, negated_conjecture, (c5_1(a601)|c3_1(a600))). % 23.51/3.56 cnf(i_0_937, negated_conjecture, (ndr1_1(a496)|~c4_0)). % 23.51/3.56 cnf(i_0_325, negated_conjecture, (ndr1_1(a549)|~c4_0)). % 23.51/3.56 cnf(i_0_1034, negated_conjecture, (c7_0|~c3_2(a475,a476)|~c2_0)). % 23.51/3.56 cnf(i_0_898, negated_conjecture, (~c4_0|~c6_2(a509,a511))). % 23.51/3.56 cnf(i_0_902, negated_conjecture, (~c4_0|~c8_2(a509,a510))). % 23.51/3.56 cnf(i_0_139, negated_conjecture, (c4_1(a569)|~c7_0|~c4_1(a568))). % 23.51/3.56 cnf(i_0_899, negated_conjecture, (~c4_0|~c5_2(a509,a511))). % 23.51/3.56 cnf(i_0_901, negated_conjecture, (~c4_0|~c1_2(a509,a510))). % 23.51/3.56 cnf(i_0_914, negated_conjecture, (epred2_0|~c4_0|~c8_2(a505,a506))). % 23.51/3.56 cnf(i_0_912, negated_conjecture, (epred2_0|~c4_0|~c1_2(a505,a506))). % 23.51/3.56 cnf(i_0_942, negated_conjecture, (epred1_0|c8_2(a494,a495))). % 23.51/3.56 cnf(i_0_1337, plain, (~epred4_0|~c1_2(a597,a599)|~c6_1(a596))). % 23.51/3.56 cnf(i_0_1340, plain, (ndr1_1(a597)|~epred4_0|~c6_1(a596))). % 23.51/3.56 cnf(i_0_1032, negated_conjecture, (c7_0|ndr1_1(a475)|~c2_0)). % 23.51/3.56 cnf(i_0_900, negated_conjecture, (ndr1_1(a509)|~c4_0)). % 23.51/3.56 cnf(i_0_1331, plain, (c7_1(a596)|~epred4_0|~c1_1(a597))). % 23.51/3.56 cnf(i_0_927, negated_conjecture, (c2_0|~c8_2(a498,a499))). % 23.51/3.56 cnf(i_0_925, negated_conjecture, (c2_0|ndr1_1(a498))). % 23.51/3.56 cnf(i_0_922, negated_conjecture, (c2_0|~c7_2(a498,a500))). % 23.51/3.56 cnf(i_0_915, negated_conjecture, (ndr1_1(a505)|~c4_0)). % 23.51/3.56 cnf(i_0_926, negated_conjecture, (c7_1(a498)|c2_0)). % 23.51/3.56 cnf(i_0_137, negated_conjecture, (c3_1(a569)|~c7_0|~c4_1(a568))). % 23.51/3.56 cnf(i_0_426, negated_conjecture, (c1_1(a538)|~c5_1(a537)|~c7_1(a536))). % 23.51/3.56 cnf(i_0_328, negated_conjecture, (c4_2(a549,a550)|~c4_0)). % 23.51/3.56 cnf(i_0_934, negated_conjecture, (c6_2(a496,a497)|~c4_0)). % 23.51/3.56 cnf(i_0_326, negated_conjecture, (c6_2(a549,a550)|~c4_0)). % 23.51/3.56 cnf(i_0_323, negated_conjecture, (c8_2(a549,a551)|~c4_0)). % 23.51/3.56 cnf(i_0_322, negated_conjecture, (c5_2(a549,a551)|~c4_0)). % 23.51/3.56 cnf(i_0_935, negated_conjecture, (c3_2(a496,a497)|~c4_0)). % 23.51/3.56 cnf(i_0_1327, plain, (c7_1(a596)|~epred4_0|~c1_2(a597,a599))). % 23.51/3.56 cnf(i_0_324, negated_conjecture, (c2_2(a549,a551)|~c4_0)). % 23.51/3.56 cnf(i_0_1031, negated_conjecture, (c7_0|c4_2(a475,a477)|~c2_0)). % 23.51/3.56 cnf(i_0_903, negated_conjecture, (c4_2(a509,a510)|~c4_0)). % 23.51/3.56 cnf(i_0_1030, negated_conjecture, (c7_0|c6_2(a475,a477)|~c2_0)). % 23.51/3.56 cnf(i_0_1330, plain, (c7_1(a596)|ndr1_1(a597)|~epred4_0)). % 23.51/3.56 cnf(i_0_1033, negated_conjecture, (c7_0|c7_2(a475,a476)|~c2_0)). % 23.51/3.56 cnf(i_0_1029, negated_conjecture, (c7_0|c7_2(a475,a477)|~c2_0)). % 23.51/3.56 cnf(i_0_1035, negated_conjecture, (c7_0|c5_2(a475,a476)|~c2_0)). % 23.51/3.56 cnf(i_0_897, negated_conjecture, (c3_2(a509,a511)|~c4_0)). % 23.51/3.56 cnf(i_0_1223, plain, (~epred2_0|~c5_2(X1,a504)|~c8_2(X1,a502)|~c4_2(X1,a503))). % 23.51/3.56 cnf(i_0_1221, plain, (~epred2_0|~c3_2(X1,a504)|~c8_2(X1,a502)|~c4_2(X1,a503))). % 23.51/3.56 cnf(i_0_1239, plain, (~epred2_0|~c5_2(X1,a504)|~c7_2(X1,a502)|~c4_2(X1,a503))). % 23.51/3.56 cnf(i_0_1237, plain, (~epred2_0|~c3_2(X1,a504)|~c7_2(X1,a502)|~c4_2(X1,a503))). % 23.51/3.56 cnf(i_0_1255, plain, (~epred2_0|~c1_2(X1,a502)|~c5_2(X1,a504)|~c4_2(X1,a503))). % 23.51/3.56 cnf(i_0_913, negated_conjecture, (epred2_0|c6_2(a505,a506)|~c4_0)). % 23.51/3.56 cnf(i_0_1253, plain, (~epred2_0|~c1_2(X1,a502)|~c3_2(X1,a504)|~c4_2(X1,a503))). % 23.51/3.56 cnf(i_0_1227, plain, (~epred2_0|~c3_2(X1,a503)|~c5_2(X1,a504)|~c8_2(X1,a502))). % 23.51/3.56 cnf(i_0_1225, plain, (~epred2_0|~c3_2(X1,a503)|~c3_2(X1,a504)|~c8_2(X1,a502))). % 23.51/3.56 cnf(i_0_1243, plain, (~epred2_0|~c3_2(X1,a503)|~c5_2(X1,a504)|~c7_2(X1,a502))). % 23.51/3.56 cnf(i_0_422, negated_conjecture, (c1_1(a538)|c4_1(a537)|~c7_1(a536))). % 23.51/3.56 cnf(i_0_410, negated_conjecture, (c5_1(a536)|c1_1(a538)|~c5_1(a537))). % 23.51/3.56 cnf(i_0_406, negated_conjecture, (c5_1(a536)|c1_1(a538)|c4_1(a537))). % 23.51/3.56 cnf(i_0_923, negated_conjecture, (c2_0|c4_2(a498,a500))). % 23.51/3.56 cnf(i_0_1241, plain, (~epred2_0|~c3_2(X1,a503)|~c3_2(X1,a504)|~c7_2(X1,a502))). % 23.51/3.56 cnf(i_0_1259, plain, (~epred2_0|~c1_2(X1,a502)|~c3_2(X1,a503)|~c5_2(X1,a504))). % 23.51/3.56 cnf(i_0_1257, plain, (~epred2_0|~c1_2(X1,a502)|~c3_2(X1,a503)|~c3_2(X1,a504))). % 23.51/3.56 cnf(i_0_924, negated_conjecture, (c2_0|c8_2(a498,a500))). % 23.51/3.56 cnf(i_0_928, negated_conjecture, (c2_0|c7_2(a498,a499))). % 23.51/3.56 cnf(i_0_929, negated_conjecture, (c3_2(a498,a499)|c2_0)). % 23.51/3.56 cnf(i_0_223, negated_conjecture, (c7_1(a564)|c6_1(a565)|~c8_2(a566,a567))). % 23.51/3.56 cnf(i_0_224, negated_conjecture, (c7_1(a564)|c6_1(a565)|ndr1_1(a566))). % 23.51/3.56 cnf(i_0_168, negated_conjecture, (c5_1(a564)|c6_1(a565)|ndr1_1(a566))). % 23.51/3.56 cnf(i_0_1321, plain, (~epred4_0|~c1_1(a597)|~c1_2(a596,X1)|~c4_2(a596,X1)|~ndr1_1(a596))). % 23.51/3.56 cnf(i_0_210, negated_conjecture, (c7_1(a564)|c2_1(a565)|ndr1_1(a566))). % 23.51/3.56 cnf(i_0_221, negated_conjecture, (c7_1(a564)|c6_1(a565)|~c1_2(a566,a567))). % 23.51/3.56 cnf(i_0_167, negated_conjecture, (c5_1(a564)|c6_1(a565)|~c8_2(a566,a567))). % 23.51/3.56 cnf(i_0_165, negated_conjecture, (c5_1(a564)|c6_1(a565)|~c1_2(a566,a567))). % 23.51/3.56 cnf(i_0_209, negated_conjecture, (c7_1(a564)|c2_1(a565)|~c8_2(a566,a567))). % 23.51/3.56 cnf(i_0_154, negated_conjecture, (c5_1(a564)|c2_1(a565)|ndr1_1(a566))). % 23.51/3.56 cnf(i_0_217, negated_conjecture, (c7_1(a564)|c3_1(a565)|ndr1_1(a566))). % 23.51/3.56 cnf(i_0_1344, plain, (c4_2(a597,a598)|~epred4_0|~c6_1(a596))). % 23.51/3.56 cnf(i_0_1342, plain, (c7_2(a597,a598)|~epred4_0|~c6_1(a596))). % 23.51/3.56 cnf(i_0_161, negated_conjecture, (c5_1(a564)|c3_1(a565)|ndr1_1(a566))). % 23.51/3.56 cnf(i_0_207, negated_conjecture, (c7_1(a564)|c2_1(a565)|~c1_2(a566,a567))). % 23.51/3.56 cnf(i_0_153, negated_conjecture, (c5_1(a564)|c2_1(a565)|~c8_2(a566,a567))). % 23.51/3.56 cnf(i_0_151, negated_conjecture, (c5_1(a564)|c2_1(a565)|~c1_2(a566,a567))). % 23.51/3.56 cnf(i_0_216, negated_conjecture, (c7_1(a564)|c3_1(a565)|~c8_2(a566,a567))). % 23.51/3.56 cnf(i_0_220, negated_conjecture, (c1_1(a566)|c7_1(a564)|c6_1(a565))). % 23.51/3.56 cnf(i_0_164, negated_conjecture, (c5_1(a564)|c1_1(a566)|c6_1(a565))). % 23.51/3.56 cnf(i_0_1338, plain, (c5_2(a597,a599)|~epred4_0|~c6_1(a596))). % 23.51/3.56 cnf(i_0_1343, plain, (c3_2(a597,a598)|~epred4_0|~c6_1(a596))). % 23.51/3.56 cnf(i_0_1339, plain, (c3_2(a597,a599)|~epred4_0|~c6_1(a596))). % 23.51/3.56 cnf(i_0_206, negated_conjecture, (c1_1(a566)|c7_1(a564)|c2_1(a565))). % 23.51/3.56 cnf(i_0_214, negated_conjecture, (c7_1(a564)|c3_1(a565)|~c1_2(a566,a567))). % 23.51/3.56 cnf(i_0_160, negated_conjecture, (c5_1(a564)|c3_1(a565)|~c8_2(a566,a567))). % 23.51/3.56 cnf(i_0_158, negated_conjecture, (c5_1(a564)|c3_1(a565)|~c1_2(a566,a567))). % 23.51/3.56 cnf(i_0_150, negated_conjecture, (c5_1(a564)|c1_1(a566)|c2_1(a565))). % 23.51/3.56 cnf(i_0_213, negated_conjecture, (c1_1(a566)|c7_1(a564)|c3_1(a565))). % 23.51/3.56 cnf(i_0_157, negated_conjecture, (c5_1(a564)|c1_1(a566)|c3_1(a565))). % 23.51/3.56 cnf(i_0_1334, plain, (c7_1(a596)|c4_2(a597,a598)|~epred4_0)). % 23.51/3.56 cnf(i_0_222, negated_conjecture, (c7_1(a564)|c6_1(a565)|c6_2(a566,a567))). % 23.51/3.56 cnf(i_0_166, negated_conjecture, (c5_1(a564)|c6_1(a565)|c6_2(a566,a567))). % 23.51/3.56 cnf(i_0_208, negated_conjecture, (c7_1(a564)|c2_1(a565)|c6_2(a566,a567))). % 23.51/3.56 cnf(i_0_152, negated_conjecture, (c5_1(a564)|c2_1(a565)|c6_2(a566,a567))). % 23.51/3.56 cnf(i_0_215, negated_conjecture, (c7_1(a564)|c3_1(a565)|c6_2(a566,a567))). % 23.51/3.56 cnf(i_0_159, negated_conjecture, (c5_1(a564)|c3_1(a565)|c6_2(a566,a567))). % 23.51/3.56 cnf(i_0_1332, plain, (c7_1(a596)|c7_2(a597,a598)|~epred4_0)). % 23.51/3.56 cnf(i_0_1328, plain, (c7_1(a596)|c5_2(a597,a599)|~epred4_0)). % 23.51/3.56 cnf(i_0_1333, plain, (c7_1(a596)|c3_2(a597,a598)|~epred4_0)). % 23.51/3.56 cnf(i_0_374, negated_conjecture, (ndr1_1(a544)|ndr1_1(a542)|~c8_1(X1)|~c2_1(X1))). % 23.51/3.56 cnf(i_0_380, negated_conjecture, (c2_1(a542)|ndr1_1(a544)|~c8_1(X1)|~c2_1(X1))). % 23.51/3.56 cnf(i_0_360, negated_conjecture, (~c8_1(X1)|~c2_1(X1)|~c4_2(a542,a543)|~c4_2(a544,a545))). % 23.51/3.56 cnf(i_0_361, negated_conjecture, (~c8_1(X1)|~c2_1(X1)|~c7_2(a544,a545)|~c4_2(a542,a543))). % 23.51/3.56 cnf(i_0_1329, plain, (c7_1(a596)|c3_2(a597,a599)|~epred4_0)). % 23.51/3.56 cnf(i_0_309, negated_conjecture, (c7_0|~c5_1(X1)|~c8_1(a552)|~c3_2(X1,a553)|~c4_1(X1))). % 23.51/3.56 cnf(i_0_311, negated_conjecture, (c7_0|~c5_1(X1)|~c2_2(X1,a553)|~c8_1(a552)|~c4_1(X1))). % 23.51/3.56 cnf(i_0_359, negated_conjecture, (~c8_1(X1)|~c3_2(a544,a545)|~c2_1(X1)|~c4_2(a542,a543))). % 23.51/3.56 cnf(i_0_372, negated_conjecture, (ndr1_1(a542)|~c8_1(X1)|~c2_1(X1)|~c4_2(a544,a545))). % 23.51/3.56 cnf(i_0_373, negated_conjecture, (ndr1_1(a542)|~c8_1(X1)|~c2_1(X1)|~c7_2(a544,a545))). % 23.51/3.56 cnf(i_0_371, negated_conjecture, (ndr1_1(a542)|~c8_1(X1)|~c3_2(a544,a545)|~c2_1(X1))). % 23.51/3.56 cnf(i_0_9, negated_conjecture, (c7_1(X1)|c2_1(X1)|ndr1_1(X1)|~c7_0)). % 23.51/3.56 cnf(i_0_269, negated_conjecture, (c8_2(a561,X1)|c4_2(a561,X1)|~c4_0|~ndr1_1(a561))). % 23.51/3.56 cnf(i_0_1317, plain, (~epred4_0|~c1_2(a597,a599)|~c1_2(a596,X1)|~c4_2(a596,X1)|~ndr1_1(a596))). % 23.51/3.56 cnf(i_0_362, negated_conjecture, (ndr1_1(a544)|~c8_1(X1)|~c2_1(X1)|~c4_2(a542,a543))). % 23.51/3.56 cnf(i_0_378, negated_conjecture, (c2_1(a542)|~c8_1(X1)|~c2_1(X1)|~c4_2(a544,a545))). % 23.51/3.56 cnf(i_0_379, negated_conjecture, (c2_1(a542)|~c8_1(X1)|~c2_1(X1)|~c7_2(a544,a545))). % 23.51/3.56 cnf(i_0_377, negated_conjecture, (c2_1(a542)|~c8_1(X1)|~c3_2(a544,a545)|~c2_1(X1))). % 23.51/3.56 cnf(i_0_79, negated_conjecture, (c1_1(X1)|c3_1(X1)|ndr1_1(X1)|~c4_0)). % 23.51/3.56 cnf(i_0_16, negated_conjecture, (c7_1(a601)|c7_2(a600,X1)|~c1_2(a600,X1)|~ndr1_1(a600))). % 23.51/3.56 cnf(i_0_14, negated_conjecture, (c5_1(a601)|c7_2(a600,X1)|~c1_2(a600,X1)|~ndr1_1(a600))). % 23.51/3.56 cnf(i_0_366, negated_conjecture, (c8_2(a542,a543)|~c8_1(X1)|~c2_1(X1)|~c4_2(a544,a545))). % 23.51/3.56 cnf(i_0_367, negated_conjecture, (c8_2(a542,a543)|~c8_1(X1)|~c2_1(X1)|~c7_2(a544,a545))). % 23.51/3.56 cnf(i_0_399, negated_conjecture, (c5_1(X1)|c1_1(X1)|c6_1(X1)|ndr1_1(a539)|~c7_0)). % 23.51/3.56 cnf(i_0_15, negated_conjecture, (c7_2(a600,X1)|~c1_1(a601)|~c1_2(a600,X1)|~ndr1_1(a600))). % 23.51/3.56 cnf(i_0_312, negated_conjecture, (c7_0|ndr1_1(X1)|~c5_1(X1)|~c8_1(a552)|~c4_1(X1))). % 23.51/3.56 cnf(i_0_78, negated_conjecture, (c1_1(X1)|c3_1(X1)|~c4_0|~c5_2(X1,a582))). % 23.51/3.56 cnf(i_0_1320, plain, (ndr1_1(a597)|~epred4_0|~c1_2(a596,X1)|~c4_2(a596,X1)|~ndr1_1(a596))). % 23.51/3.56 cnf(i_0_365, negated_conjecture, (c8_2(a542,a543)|~c8_1(X1)|~c3_2(a544,a545)|~c2_1(X1))). % 23.51/3.56 cnf(i_0_368, negated_conjecture, (c8_2(a542,a543)|ndr1_1(a544)|~c8_1(X1)|~c2_1(X1))). % 23.51/3.56 cnf(i_0_1222, plain, (c8_2(X1,a504)|~epred2_0|~c8_2(X1,a502)|~c4_2(X1,a503))). % 23.51/3.56 cnf(i_0_305, negated_conjecture, (c6_1(a552)|c7_0|~c5_1(X1)|~c3_2(X1,a553)|~c4_1(X1))). % 23.51/3.56 cnf(i_0_307, negated_conjecture, (c6_1(a552)|c7_0|~c5_1(X1)|~c2_2(X1,a553)|~c4_1(X1))). % 23.51/3.56 cnf(i_0_400, negated_conjecture, (c5_1(X1)|c1_1(X1)|c6_1(a539)|c6_1(X1)|~c7_0)). % 23.51/3.56 cnf(i_0_143, negated_conjecture, (c6_2(a568,X1)|c4_2(a568,X1)|c4_1(a569)|~c7_0|~ndr1_1(a568))). % 23.51/3.56 cnf(i_0_1238, plain, (c8_2(X1,a504)|~epred2_0|~c7_2(X1,a502)|~c4_2(X1,a503))). % 23.51/3.56 cnf(i_0_1254, plain, (c8_2(X1,a504)|~epred2_0|~c1_2(X1,a502)|~c4_2(X1,a503))). % 23.51/3.56 cnf(i_0_1226, plain, (c8_2(X1,a504)|~epred2_0|~c3_2(X1,a503)|~c8_2(X1,a502))). % 23.51/3.56 cnf(i_0_1242, plain, (c8_2(X1,a504)|~epred2_0|~c3_2(X1,a503)|~c7_2(X1,a502))). % 23.51/3.56 cnf(i_0_141, negated_conjecture, (c3_1(a569)|c6_2(a568,X1)|c4_2(a568,X1)|~c7_0|~ndr1_1(a568))). % 23.51/3.56 cnf(i_0_964, negated_conjecture, (c5_1(X1)|ndr1_1(X1)|c4_1(a488)|~c2_1(X1))). % 23.51/3.56 cnf(i_0_1219, plain, (c1_2(X1,a503)|~epred2_0|~c5_2(X1,a504)|~c8_2(X1,a502))). % 23.51/3.56 cnf(i_0_1217, plain, (c1_2(X1,a503)|~epred2_0|~c3_2(X1,a504)|~c8_2(X1,a502))). % 23.51/3.56 cnf(i_0_1235, plain, (c1_2(X1,a503)|~epred2_0|~c5_2(X1,a504)|~c7_2(X1,a502))). % 23.51/3.56 cnf(i_0_1233, plain, (c1_2(X1,a503)|~epred2_0|~c3_2(X1,a504)|~c7_2(X1,a502))). % 23.51/3.56 cnf(i_0_430, negated_conjecture, (c1_1(a538)|~c7_1(a536)|~c2_2(a537,X1)|~c3_2(a537,X1)|~c7_2(a537,X1)|~ndr1_1(a537))). % 23.51/3.56 cnf(i_0_308, negated_conjecture, (c6_1(a552)|c7_0|ndr1_1(X1)|~c5_1(X1)|~c4_1(X1))). % 23.51/3.56 cnf(i_0_414, negated_conjecture, (c5_1(a536)|c1_1(a538)|~c2_2(a537,X1)|~c3_2(a537,X1)|~c7_2(a537,X1)|~ndr1_1(a537))). % 23.51/3.56 cnf(i_0_965, negated_conjecture, (c5_1(X1)|ndr1_1(X1)|~c3_1(a488)|~c2_1(X1))). % 23.51/3.56 cnf(i_0_1251, plain, (c1_2(X1,a503)|~epred2_0|~c1_2(X1,a502)|~c5_2(X1,a504))). % 23.51/3.56 cnf(i_0_1249, plain, (c1_2(X1,a503)|~epred2_0|~c1_2(X1,a502)|~c3_2(X1,a504))). % 23.51/3.56 cnf(i_0_1127, negated_conjecture, (ndr1_1(X1)|~c8_1(X2)|~c3_1(X2)|~c6_2(X2,a459))). % 23.51/3.56 cnf(i_0_1123, negated_conjecture, (ndr1_1(X1)|~c8_1(X2)|~c3_1(X2)|~c3_2(X2,a459))). % 23.51/3.56 cnf(i_0_7, negated_conjecture, (c7_1(X1)|c2_1(X1)|c4_2(X1,a602)|~c7_0)). % 23.51/3.56 cnf(i_0_8, negated_conjecture, (c7_1(X1)|c3_2(X1,a602)|c2_1(X1)|~c7_0)). % 23.51/3.56 cnf(i_0_1131, negated_conjecture, (ndr1_1(X1)|ndr1_1(X2)|~c8_1(X2)|~c3_1(X2))). % 23.51/3.56 cnf(i_0_6, negated_conjecture, (c7_1(X1)|c2_1(X1)|~c7_0|~c7_2(X1,a602))). % 23.51/3.56 cnf(i_0_77, negated_conjecture, (c1_1(X1)|c3_1(X1)|c3_2(X1,a582)|~c4_0)). % 23.51/3.56 cnf(i_0_76, negated_conjecture, (c1_1(X1)|c2_2(X1,a582)|c3_1(X1)|~c4_0)). % 23.51/3.56 cnf(i_0_938, negated_conjecture, (c3_2(a496,X1)|~c4_0|~c2_2(a496,X1)|~c8_2(a496,X1))). % 23.51/3.56 cnf(i_0_403, negated_conjecture, (c5_1(X1)|c1_1(X1)|c6_1(X1)|c8_2(a539,a540)|~c7_0)). % 23.51/3.56 cnf(i_0_1258, plain, (c8_2(X1,a504)|~epred2_0|~c1_2(X1,a502)|~c3_2(X1,a503))). % 23.51/3.56 cnf(i_0_310, negated_conjecture, (c7_0|c7_2(X1,a553)|~c5_1(X1)|~c8_1(a552)|~c4_1(X1))). % 23.51/3.56 cnf(i_0_396, negated_conjecture, (c5_1(X1)|c1_1(X1)|c6_1(X1)|c8_2(a539,a541)|~c7_0)). % 23.51/3.56 cnf(i_0_907, negated_conjecture, (~c3_2(X1,X2)|~c2_1(a508)|~c7_2(X1,X2)|~c4_2(X1,X2)|~ndr1_1(X1)|~c4_1(X1))). % 23.51/3.56 cnf(i_0_1324, plain, (c4_2(a597,a598)|~epred4_0|~c1_2(a596,X1)|~c4_2(a596,X1)|~ndr1_1(a596))). % 23.51/3.56 cnf(i_0_1322, plain, (c7_2(a597,a598)|~epred4_0|~c1_2(a596,X1)|~c4_2(a596,X1)|~ndr1_1(a596))). % 23.51/3.56 cnf(i_0_1318, plain, (c5_2(a597,a599)|~epred4_0|~c1_2(a596,X1)|~c4_2(a596,X1)|~ndr1_1(a596))). % 23.51/3.56 cnf(i_0_401, negated_conjecture, (c5_1(X1)|c1_1(X1)|c3_2(a539,a540)|c6_1(X1)|~c7_0)). % 23.51/3.56 cnf(i_0_1323, plain, (c3_2(a597,a598)|~epred4_0|~c1_2(a596,X1)|~c4_2(a596,X1)|~ndr1_1(a596))). % 23.51/3.56 cnf(i_0_1319, plain, (c3_2(a597,a599)|~epred4_0|~c1_2(a596,X1)|~c4_2(a596,X1)|~ndr1_1(a596))). % 23.51/3.56 cnf(i_0_306, negated_conjecture, (c6_1(a552)|c7_0|c7_2(X1,a553)|~c5_1(X1)|~c4_1(X1))). % 23.51/3.56 cnf(i_0_956, negated_conjecture, (c5_1(X1)|c4_2(X1,a487)|c4_1(a488)|~c2_1(X1))). % 23.51/3.56 cnf(i_0_1218, plain, (c1_2(X1,a503)|c8_2(X1,a504)|~epred2_0|~c8_2(X1,a502))). % 23.51/3.56 cnf(i_0_1234, plain, (c1_2(X1,a503)|c8_2(X1,a504)|~epred2_0|~c7_2(X1,a502))). % 23.51/3.56 cnf(i_0_960, negated_conjecture, (c5_1(X1)|c1_2(X1,a487)|c4_1(a488)|~c2_1(X1))). % 23.51/3.56 cnf(i_0_957, negated_conjecture, (c5_1(X1)|c4_2(X1,a487)|~c3_1(a488)|~c2_1(X1))). % 23.51/3.56 cnf(i_0_961, negated_conjecture, (c5_1(X1)|c1_2(X1,a487)|~c3_1(a488)|~c2_1(X1))). % 23.51/3.56 cnf(i_0_1126, negated_conjecture, (c8_2(X1,a460)|~c8_1(X2)|~c3_1(X2)|~c6_2(X2,a459))). % 23.51/3.56 cnf(i_0_1122, negated_conjecture, (c8_2(X1,a460)|~c8_1(X2)|~c3_1(X2)|~c3_2(X2,a459))). % 23.51/3.56 cnf(i_0_138, negated_conjecture, (c3_2(a569,X1)|c6_2(a569,X1)|~c7_0|~c4_2(a569,X1)|~ndr1_1(a569)|~c4_1(a568))). % 23.51/3.56 cnf(i_0_1125, negated_conjecture, (c5_2(X1,a460)|~c8_1(X2)|~c3_1(X2)|~c6_2(X2,a459))). % 23.51/3.56 cnf(i_0_1121, negated_conjecture, (c5_2(X1,a460)|~c8_1(X2)|~c3_1(X2)|~c3_2(X2,a459))). % 23.51/3.56 cnf(i_0_1124, negated_conjecture, (c1_2(X1,a460)|~c8_1(X2)|~c3_1(X2)|~c6_2(X2,a459))). % 23.51/3.56 cnf(i_0_1120, negated_conjecture, (c1_2(X1,a460)|~c8_1(X2)|~c3_1(X2)|~c3_2(X2,a459))). % 23.51/3.56 cnf(i_0_219, negated_conjecture, (c7_1(a564)|c6_1(a565)|c5_2(a566,X1)|~c2_2(a566,X1)|~c1_2(a566,X1))). % 23.51/3.56 cnf(i_0_163, negated_conjecture, (c5_1(a564)|c6_1(a565)|c5_2(a566,X1)|~c2_2(a566,X1)|~c1_2(a566,X1))). % 23.51/3.56 cnf(i_0_205, negated_conjecture, (c7_1(a564)|c2_1(a565)|c5_2(a566,X1)|~c2_2(a566,X1)|~c1_2(a566,X1))). % 23.51/3.56 cnf(i_0_149, negated_conjecture, (c5_1(a564)|c2_1(a565)|c5_2(a566,X1)|~c2_2(a566,X1)|~c1_2(a566,X1))). % 23.51/3.56 cnf(i_0_402, negated_conjecture, (c5_1(X1)|c1_1(X1)|c6_1(X1)|~c7_0|~c5_2(a539,a540))). % 23.51/3.56 cnf(i_0_1130, negated_conjecture, (c8_2(X1,a460)|ndr1_1(X2)|~c8_1(X2)|~c3_1(X2))). % 23.51/3.56 cnf(i_0_1129, negated_conjecture, (c5_2(X1,a460)|ndr1_1(X2)|~c8_1(X2)|~c3_1(X2))). % 23.51/3.56 cnf(i_0_1128, negated_conjecture, (c1_2(X1,a460)|ndr1_1(X2)|~c8_1(X2)|~c3_1(X2))). % 23.51/3.56 cnf(i_0_82, negated_conjecture, (c2_2(a581,X1)|c7_2(a581,X1)|c8_2(a581,X1)|~c2_0|~ndr1_1(a581))). % 23.51/3.56 cnf(i_0_212, negated_conjecture, (c7_1(a564)|c3_1(a565)|c5_2(a566,X1)|~c2_2(a566,X1)|~c1_2(a566,X1))). % 23.51/3.56 cnf(i_0_156, negated_conjecture, (c5_1(a564)|c3_1(a565)|c5_2(a566,X1)|~c2_2(a566,X1)|~c1_2(a566,X1))). % 23.51/3.56 cnf(i_0_397, negated_conjecture, (c5_1(X1)|c1_1(X1)|c6_1(X1)|~c7_0|~c5_2(a539,a541))). % 23.51/3.56 cnf(i_0_906, negated_conjecture, (c1_1(a508)|~c3_2(X1,X2)|~c7_2(X1,X2)|~c4_2(X1,X2)|~ndr1_1(X1)|~c4_1(X1))). % 23.51/3.56 cnf(i_0_1043, negated_conjecture, (~c1_2(X1,X2)|~c3_1(X3)|~c3_2(X3,a473)|~c7_0|~c8_2(X1,X2)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1046, negated_conjecture, (ndr1_1(X1)|~c1_2(X2,X3)|~c3_1(X1)|~c7_0|~c8_2(X2,X3)|~c4_2(X2,X3)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_1250, plain, (c1_2(X1,a503)|c8_2(X1,a504)|~epred2_0|~c1_2(X1,a502))). % 23.51/3.56 cnf(i_0_428, negated_conjecture, (c2_2(a538,X1)|c3_2(a538,X1)|~c5_1(a537)|~c7_1(a536)|~c7_2(a538,X1)|~ndr1_1(a538))). % 23.51/3.56 cnf(i_0_398, negated_conjecture, (c5_1(X1)|c1_1(X1)|c6_1(X1)|~c2_2(a539,a541)|~c7_0)). % 23.51/3.56 cnf(i_0_1119, negated_conjecture, (c7_2(X1,a459)|ndr1_1(X2)|~c8_1(X1)|~c3_1(X1))). % 23.51/3.56 cnf(i_0_1037, negated_conjecture, (c7_0|c5_2(a475,X1)|c4_2(a475,X1)|~c2_0|~c8_2(a475,X1))). % 23.51/3.56 cnf(i_0_424, negated_conjecture, (c2_2(a538,X1)|c3_2(a538,X1)|c4_1(a537)|~c7_1(a536)|~c7_2(a538,X1)|~ndr1_1(a538))). % 23.51/3.56 cnf(i_0_412, negated_conjecture, (c5_1(a536)|c2_2(a538,X1)|c3_2(a538,X1)|~c5_1(a537)|~c7_2(a538,X1)|~ndr1_1(a538))). % 23.51/3.56 cnf(i_0_408, negated_conjecture, (c5_1(a536)|c2_2(a538,X1)|c3_2(a538,X1)|c4_1(a537)|~c7_2(a538,X1)|~ndr1_1(a538))). % 23.51/3.56 cnf(i_0_1118, negated_conjecture, (c7_2(X1,a459)|c8_2(X2,a460)|~c8_1(X1)|~c3_1(X1))). % 23.51/3.56 cnf(i_0_1134, negated_conjecture, (c3_2(X1,X2)|c2_1(X1)|~c6_1(a458)|~c6_1(X1)|~c7_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1132, negated_conjecture, (c3_2(X1,X2)|c2_1(X1)|~c2_1(a458)|~c6_1(X1)|~c7_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_385, negated_conjecture, (c7_2(a542,X1)|~c8_1(X2)|~c2_1(X2)|~c7_2(a544,a545)|~c4_2(a542,X1))). % 23.51/3.56 cnf(i_0_383, negated_conjecture, (c7_2(a542,X1)|~c8_1(X2)|~c3_2(a544,a545)|~c2_1(X2)|~c4_2(a542,X1))). % 23.51/3.56 cnf(i_0_427, negated_conjecture, (c7_2(a538,X1)|c8_2(a538,X1)|~c5_1(a537)|~c7_1(a536)|~c1_2(a538,X1)|~ndr1_1(a538))). % 23.51/3.56 cnf(i_0_1117, negated_conjecture, (c5_2(X1,a460)|c7_2(X2,a459)|~c8_1(X2)|~c3_1(X2))). % 23.51/3.56 cnf(i_0_386, negated_conjecture, (c7_2(a542,X1)|ndr1_1(a544)|~c8_1(X2)|~c2_1(X2)|~c4_2(a542,X1))). % 23.51/3.56 cnf(i_0_1116, negated_conjecture, (c1_2(X1,a460)|c7_2(X2,a459)|~c8_1(X2)|~c3_1(X2))). % 23.51/3.56 cnf(i_0_423, negated_conjecture, (c7_2(a538,X1)|c8_2(a538,X1)|c4_1(a537)|~c7_1(a536)|~c1_2(a538,X1)|~ndr1_1(a538))). % 23.51/3.56 cnf(i_0_442, negated_conjecture, (c1_1(a538)|c3_2(a536,X1)|c5_2(a536,X1)|~c5_1(a537)|~c7_2(a536,X1)|~ndr1_1(a536))). % 23.51/3.56 cnf(i_0_411, negated_conjecture, (c5_1(a536)|c7_2(a538,X1)|c8_2(a538,X1)|~c5_1(a537)|~c1_2(a538,X1)|~ndr1_1(a538))). % 23.51/3.56 cnf(i_0_375, negated_conjecture, (c1_2(a544,X1)|c4_2(a544,X1)|ndr1_1(a542)|~c8_1(X2)|~c2_1(X2))). % 23.51/3.56 cnf(i_0_438, negated_conjecture, (c1_1(a538)|c3_2(a536,X1)|c5_2(a536,X1)|c4_1(a537)|~c7_2(a536,X1)|~ndr1_1(a536))). % 23.51/3.56 cnf(i_0_1133, negated_conjecture, (c3_2(X1,X2)|c2_1(X1)|c4_1(a458)|~c6_1(X1)|~c7_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_352, negated_conjecture, (c3_2(X1,X2)|~c1_1(X1)|~c8_2(X1,X2)|~c6_2(X1,X2)|~c4_2(X1,a548)|~ndr1_1(X1)|~c4_1(a546))). % 23.51/3.56 cnf(i_0_351, negated_conjecture, (c3_2(X1,X2)|~c1_1(X1)|~c7_2(X1,a548)|~c8_2(X1,X2)|~c6_2(X1,X2)|~ndr1_1(X1)|~c4_1(a546))). % 23.51/3.56 cnf(i_0_384, negated_conjecture, (c7_2(a542,X1)|~c8_1(X2)|~c2_1(X2)|~c4_2(a544,a545)|~c4_2(a542,X1))). % 23.51/3.56 cnf(i_0_407, negated_conjecture, (c5_1(a536)|c7_2(a538,X1)|c8_2(a538,X1)|c4_1(a537)|~c1_2(a538,X1)|~ndr1_1(a538))). % 23.51/3.56 cnf(i_0_195, negated_conjecture, (c3_2(a564,X1)|c6_1(a565)|c8_2(a564,X1)|~c1_2(a564,X1)|~c8_2(a566,a567)|~ndr1_1(a564))). % 23.51/3.56 cnf(i_0_193, negated_conjecture, (c3_2(a564,X1)|c6_1(a565)|c8_2(a564,X1)|~c1_2(a566,a567)|~c1_2(a564,X1)|~ndr1_1(a564))). % 23.51/3.56 cnf(i_0_181, negated_conjecture, (c3_2(a564,X1)|c2_1(a565)|c8_2(a564,X1)|~c1_2(a564,X1)|~c8_2(a566,a567)|~ndr1_1(a564))). % 23.51/3.56 cnf(i_0_179, negated_conjecture, (c3_2(a564,X1)|c2_1(a565)|c8_2(a564,X1)|~c1_2(a566,a567)|~c1_2(a564,X1)|~ndr1_1(a564))). % 23.51/3.56 cnf(i_0_381, negated_conjecture, (c1_2(a544,X1)|c2_1(a542)|c4_2(a544,X1)|~c8_1(X2)|~c2_1(X2))). % 23.51/3.56 cnf(i_0_196, negated_conjecture, (c3_2(a564,X1)|c6_1(a565)|c8_2(a564,X1)|ndr1_1(a566)|~c1_2(a564,X1)|~ndr1_1(a564))). % 23.51/3.56 cnf(i_0_705, negated_conjecture, (c5_2(X1,X2)|~c1_1(a514)|~c1_2(a512,a513)|~c3_2(X1,a515)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_657, negated_conjecture, (c5_2(X1,X2)|~c1_1(a514)|~c2_2(a512,a513)|~c3_2(X1,a515)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_711, negated_conjecture, (c5_2(X1,X2)|~c1_1(a514)|~c2_2(X1,a515)|~c1_2(a512,a513)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_182, negated_conjecture, (c3_2(a564,X1)|c2_1(a565)|c8_2(a564,X1)|ndr1_1(a566)|~c1_2(a564,X1)|~ndr1_1(a564))). % 23.51/3.56 cnf(i_0_188, negated_conjecture, (c3_1(a565)|c3_2(a564,X1)|c8_2(a564,X1)|~c1_2(a564,X1)|~c8_2(a566,a567)|~ndr1_1(a564))). % 23.51/3.56 cnf(i_0_186, negated_conjecture, (c3_1(a565)|c3_2(a564,X1)|c8_2(a564,X1)|~c1_2(a566,a567)|~c1_2(a564,X1)|~ndr1_1(a564))). % 23.51/3.56 cnf(i_0_189, negated_conjecture, (c3_1(a565)|c3_2(a564,X1)|c8_2(a564,X1)|ndr1_1(a566)|~c1_2(a564,X1)|~ndr1_1(a564))). % 23.51/3.56 cnf(i_0_192, negated_conjecture, (c1_1(a566)|c3_2(a564,X1)|c6_1(a565)|c8_2(a564,X1)|~c1_2(a564,X1)|~ndr1_1(a564))). % 23.51/3.56 cnf(i_0_178, negated_conjecture, (c1_1(a566)|c3_2(a564,X1)|c2_1(a565)|c8_2(a564,X1)|~c1_2(a564,X1)|~ndr1_1(a564))). % 23.51/3.56 cnf(i_0_185, negated_conjecture, (c1_1(a566)|c3_1(a565)|c3_2(a564,X1)|c8_2(a564,X1)|~c1_2(a564,X1)|~ndr1_1(a564))). % 23.51/3.56 cnf(i_0_663, negated_conjecture, (c5_2(X1,X2)|~c1_1(a514)|~c2_2(a512,a513)|~c2_2(X1,a515)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_704, negated_conjecture, (c5_2(X1,X2)|~c1_1(a514)|~c2_2(X1,a516)|~c1_2(a512,a513)|~c3_2(X1,a515)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_656, negated_conjecture, (c5_2(X1,X2)|~c1_1(a514)|~c2_2(a512,a513)|~c2_2(X1,a516)|~c3_2(X1,a515)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_710, negated_conjecture, (c5_2(X1,X2)|~c1_1(a514)|~c2_2(X1,a515)|~c2_2(X1,a516)|~c1_2(a512,a513)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_194, negated_conjecture, (c3_2(a564,X1)|c6_1(a565)|c8_2(a564,X1)|c6_2(a566,a567)|~c1_2(a564,X1)|~ndr1_1(a564))). % 23.51/3.56 cnf(i_0_180, negated_conjecture, (c3_2(a564,X1)|c2_1(a565)|c8_2(a564,X1)|c6_2(a566,a567)|~c1_2(a564,X1)|~ndr1_1(a564))). % 23.51/3.56 cnf(i_0_187, negated_conjecture, (c3_1(a565)|c3_2(a564,X1)|c8_2(a564,X1)|c6_2(a566,a567)|~c1_2(a564,X1)|~ndr1_1(a564))). % 23.51/3.56 cnf(i_0_363, negated_conjecture, (c1_2(a544,X1)|c4_2(a544,X1)|~c8_1(X2)|~c2_1(X2)|~c4_2(a542,a543))). % 23.51/3.56 cnf(i_0_369, negated_conjecture, (c1_2(a544,X1)|c8_2(a542,a543)|c4_2(a544,X1)|~c8_1(X2)|~c2_1(X2))). % 23.51/3.56 cnf(i_0_126, negated_conjecture, (c2_2(X1,a572)|c2_2(X1,X2)|c5_2(X1,X2)|~ndr1_1(X1)|~c4_1(X1))). % 23.51/3.56 cnf(i_0_662, negated_conjecture, (c5_2(X1,X2)|~c1_1(a514)|~c2_2(a512,a513)|~c2_2(X1,a515)|~c2_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1044, negated_conjecture, (c4_2(X1,a473)|~c1_2(X2,X3)|~c3_1(X1)|~c7_0|~c8_2(X2,X3)|~c4_2(X2,X3)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_1045, negated_conjecture, (c8_2(X1,a473)|~c1_2(X2,X3)|~c3_1(X1)|~c7_0|~c8_2(X2,X3)|~c4_2(X2,X3)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_1191, plain, (c3_2(X1,X2)|~epred1_0|~c5_2(X1,X2)|~c8_2(X1,X2)|~c6_2(X1,a492)|~c6_2(X1,a493)|~ndr1_1(X1)|~c4_1(a491))). % 23.51/3.56 cnf(i_0_128, negated_conjecture, (c2_2(X1,X2)|c5_2(X1,X2)|~c6_2(X1,a572)|~ndr1_1(X1)|~c4_1(X1))). % 23.51/3.56 cnf(i_0_491, negated_conjecture, (c1_1(X1)|c8_1(X1)|~c3_2(a530,X2)|~c6_1(X1)|~c2_0|~c8_2(a530,X2)|~c6_2(a530,X2)|~ndr1_1(a530))). % 23.51/3.56 cnf(i_0_432, negated_conjecture, (c2_2(a538,X1)|c3_2(a538,X1)|~c7_1(a536)|~c2_2(a537,X2)|~c3_2(a537,X2)|~c7_2(a537,X2)|~c7_2(a538,X1)|~ndr1_1(a537)|~ndr1_1(a538))). % 23.51/3.56 cnf(i_0_753, negated_conjecture, (c5_2(X1,X2)|ndr1_1(a512)|~c1_1(a514)|~c3_2(X1,a515)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_490, negated_conjecture, (c1_1(X1)|c8_1(X1)|c7_2(a530,X2)|c8_2(a530,X2)|c4_2(a530,X2)|~c6_1(X1)|~c2_0|~ndr1_1(a530))). % 23.51/3.56 cnf(i_0_1189, plain, (c3_2(X1,X2)|~epred1_0|~c2_2(X1,a493)|~c5_2(X1,X2)|~c8_2(X1,X2)|~c6_2(X1,a492)|~ndr1_1(X1)|~c4_1(a491))). % 23.51/3.56 cnf(i_0_1187, plain, (c3_2(X1,X2)|~epred1_0|~c5_2(X1,X2)|~c7_2(X1,a492)|~c8_2(X1,X2)|~c6_2(X1,a493)|~ndr1_1(X1)|~c4_1(a491))). % 23.51/3.56 cnf(i_0_1185, plain, (c3_2(X1,X2)|~epred1_0|~c2_2(X1,a493)|~c5_2(X1,X2)|~c7_2(X1,a492)|~c8_2(X1,X2)|~ndr1_1(X1)|~c4_1(a491))). % 23.51/3.56 cnf(i_0_1159, plain, (c3_2(X1,X2)|~epred1_0|~c5_1(a491)|~c5_2(X1,X2)|~c8_2(X1,X2)|~c6_2(X1,a492)|~c6_2(X1,a493)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_759, negated_conjecture, (c5_2(X1,X2)|ndr1_1(a512)|~c1_1(a514)|~c2_2(X1,a515)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_752, negated_conjecture, (c5_2(X1,X2)|ndr1_1(a512)|~c1_1(a514)|~c2_2(X1,a516)|~c3_2(X1,a515)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_758, negated_conjecture, (c5_2(X1,X2)|ndr1_1(a512)|~c1_1(a514)|~c2_2(X1,a515)|~c2_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_801, negated_conjecture, (c6_1(a512)|c5_2(X1,X2)|~c1_1(a514)|~c3_2(X1,a515)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_127, negated_conjecture, (c2_2(X1,X2)|c5_2(X1,X2)|~c5_2(X1,a572)|~ndr1_1(X1)|~c4_1(X1))). % 23.51/3.56 cnf(i_0_1157, plain, (c3_2(X1,X2)|~epred1_0|~c5_1(a491)|~c2_2(X1,a493)|~c5_2(X1,X2)|~c8_2(X1,X2)|~c6_2(X1,a492)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1155, plain, (c3_2(X1,X2)|~epred1_0|~c5_1(a491)|~c5_2(X1,X2)|~c7_2(X1,a492)|~c8_2(X1,X2)|~c6_2(X1,a493)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1153, plain, (c3_2(X1,X2)|~epred1_0|~c5_1(a491)|~c2_2(X1,a493)|~c5_2(X1,X2)|~c7_2(X1,a492)|~c8_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_332, negated_conjecture, (c3_2(X1,X2)|~c1_1(X1)|~c8_2(a546,a547)|~c8_2(X1,X2)|~c6_2(X1,X2)|~c4_2(X1,a548)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_807, negated_conjecture, (c6_1(a512)|c5_2(X1,X2)|~c1_1(a514)|~c2_2(X1,a515)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_800, negated_conjecture, (c6_1(a512)|c5_2(X1,X2)|~c1_1(a514)|~c2_2(X1,a516)|~c3_2(X1,a515)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_806, negated_conjecture, (c6_1(a512)|c5_2(X1,X2)|~c1_1(a514)|~c2_2(X1,a515)|~c2_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_416, negated_conjecture, (c5_1(a536)|c2_2(a538,X1)|c3_2(a538,X1)|~c2_2(a537,X2)|~c3_2(a537,X2)|~c7_2(a537,X2)|~c7_2(a538,X1)|~ndr1_1(a537)|~ndr1_1(a538))). % 23.51/3.56 cnf(i_0_316, negated_conjecture, (c2_2(a552,X1)|c7_0|c8_2(a552,X1)|c6_2(a552,X1)|ndr1_1(X2)|~c5_1(X2)|~ndr1_1(a552)|~c4_1(X2))). % 23.51/3.56 cnf(i_0_768, negated_conjecture, (c5_1(a514)|c5_2(X1,X2)|c7_2(X1,a515)|ndr1_1(a512)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_340, negated_conjecture, (c3_2(X1,X2)|~c1_1(X1)|~c2_2(a546,a547)|~c8_2(X1,X2)|~c6_2(X1,X2)|~c4_2(X1,a548)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_331, negated_conjecture, (c3_2(X1,X2)|~c1_1(X1)|~c7_2(X1,a548)|~c8_2(a546,a547)|~c8_2(X1,X2)|~c6_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_339, negated_conjecture, (c3_2(X1,X2)|~c1_1(X1)|~c2_2(a546,a547)|~c7_2(X1,a548)|~c8_2(X1,X2)|~c6_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_353, negated_conjecture, (c2_2(X1,a548)|c3_2(X1,X2)|~c1_1(X1)|~c8_2(X1,X2)|~c6_2(X1,X2)|~ndr1_1(X1)|~c4_1(a546))). % 23.51/3.56 cnf(i_0_767, negated_conjecture, (c5_1(a514)|c5_2(X1,X2)|c7_2(X1,a515)|ndr1_1(a512)|~c2_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_717, negated_conjecture, (c5_1(a514)|c5_2(X1,X2)|~c1_2(a512,a513)|~c3_2(X1,a515)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_669, negated_conjecture, (c5_1(a514)|c5_2(X1,X2)|~c2_2(a512,a513)|~c3_2(X1,a515)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_723, negated_conjecture, (c5_1(a514)|c5_2(X1,X2)|~c2_2(X1,a515)|~c1_2(a512,a513)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_675, negated_conjecture, (c5_1(a514)|c5_2(X1,X2)|~c2_2(a512,a513)|~c2_2(X1,a515)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_920, negated_conjecture, (c5_1(a501)|c1_1(X1)|c1_2(X1,X2)|c7_0|c7_2(X1,X2)|c6_2(X1,X2)|~c2_1(X1)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_816, negated_conjecture, (c5_1(a514)|c6_1(a512)|c5_2(X1,X2)|c7_2(X1,a515)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1298, plain, (c3_1(a587)|c5_2(X1,X2)|~epred3_0|~c2_2(X1,X2)|~c1_2(X1,a588)|~c7_2(X1,a589)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_815, negated_conjecture, (c5_1(a514)|c6_1(a512)|c5_2(X1,X2)|c7_2(X1,a515)|~c2_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_716, negated_conjecture, (c5_1(a514)|c5_2(X1,X2)|~c2_2(X1,a516)|~c1_2(a512,a513)|~c3_2(X1,a515)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_668, negated_conjecture, (c5_1(a514)|c5_2(X1,X2)|~c2_2(a512,a513)|~c2_2(X1,a516)|~c3_2(X1,a515)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_722, negated_conjecture, (c5_1(a514)|c5_2(X1,X2)|~c2_2(X1,a515)|~c2_2(X1,a516)|~c1_2(a512,a513)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_674, negated_conjecture, (c5_1(a514)|c5_2(X1,X2)|~c2_2(a512,a513)|~c2_2(X1,a515)|~c2_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_120, negated_conjecture, (c5_1(X1)|c7_2(X1,X2)|c8_2(X1,X2)|c6_2(X1,X2)|ndr1_1(a574)|~c6_1(X1)|~c2_0|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_756, negated_conjecture, (c5_2(X1,X2)|c7_2(X1,a515)|ndr1_1(a512)|~c1_1(a514)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_344, negated_conjecture, (c3_2(X1,X2)|ndr1_1(a546)|~c1_1(X1)|~c8_2(X1,X2)|~c6_2(X1,X2)|~c4_2(X1,a548)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_343, negated_conjecture, (c3_2(X1,X2)|ndr1_1(a546)|~c1_1(X1)|~c7_2(X1,a548)|~c8_2(X1,X2)|~c6_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_341, negated_conjecture, (c2_2(X1,a548)|c3_2(X1,X2)|~c1_1(X1)|~c2_2(a546,a547)|~c8_2(X1,X2)|~c6_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_755, negated_conjecture, (c5_2(X1,X2)|c7_2(X1,a515)|ndr1_1(a512)|~c1_1(a514)|~c2_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_142, negated_conjecture, (c3_2(a569,X1)|c6_2(a569,X1)|c6_2(a568,X2)|c4_2(a568,X2)|~c7_0|~c4_2(a569,X1)|~ndr1_1(a568)|~ndr1_1(a569))). % 23.51/3.56 cnf(i_0_765, negated_conjecture, (c5_1(a514)|c5_2(X1,X2)|ndr1_1(a512)|~c3_2(X1,a515)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_771, negated_conjecture, (c5_1(a514)|c5_2(X1,X2)|ndr1_1(a512)|~c2_2(X1,a515)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_764, negated_conjecture, (c5_1(a514)|c5_2(X1,X2)|ndr1_1(a512)|~c2_2(X1,a516)|~c3_2(X1,a515)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_919, negated_conjecture, (c1_1(X1)|c1_2(X1,X2)|c7_0|c7_2(X1,X2)|c6_2(X1,X2)|~c2_1(X1)|~c6_1(a501)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_804, negated_conjecture, (c6_1(a512)|c5_2(X1,X2)|c7_2(X1,a515)|~c1_1(a514)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1297, plain, (c3_1(a587)|c5_2(X1,X2)|~epred3_0|~c2_2(X1,X2)|~c1_2(X1,a588)|~c5_2(X1,a589)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_708, negated_conjecture, (c5_2(X1,X2)|c7_2(X1,a515)|~c1_1(a514)|~c1_2(a512,a513)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_660, negated_conjecture, (c5_2(X1,X2)|c7_2(X1,a515)|~c1_1(a514)|~c2_2(a512,a513)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_707, negated_conjecture, (c5_2(X1,X2)|c7_2(X1,a515)|~c1_1(a514)|~c2_2(X1,a516)|~c1_2(a512,a513)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_803, negated_conjecture, (c6_1(a512)|c5_2(X1,X2)|c7_2(X1,a515)|~c1_1(a514)|~c2_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_770, negated_conjecture, (c5_1(a514)|c5_2(X1,X2)|ndr1_1(a512)|~c2_2(X1,a515)|~c2_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_813, negated_conjecture, (c5_1(a514)|c6_1(a512)|c5_2(X1,X2)|~c3_2(X1,a515)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_819, negated_conjecture, (c5_1(a514)|c6_1(a512)|c5_2(X1,X2)|~c2_2(X1,a515)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_812, negated_conjecture, (c5_1(a514)|c6_1(a512)|c5_2(X1,X2)|~c2_2(X1,a516)|~c3_2(X1,a515)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_918, negated_conjecture, (c1_1(X1)|c1_2(X1,X2)|c7_0|c7_2(X1,X2)|c6_2(X1,X2)|~c8_1(a501)|~c2_1(X1)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_818, negated_conjecture, (c5_1(a514)|c6_1(a512)|c5_2(X1,X2)|~c2_2(X1,a515)|~c2_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_659, negated_conjecture, (c5_2(X1,X2)|c7_2(X1,a515)|~c1_1(a514)|~c2_2(a512,a513)|~c2_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_345, negated_conjecture, (c2_2(X1,a548)|c3_2(X1,X2)|ndr1_1(a546)|~c1_1(X1)|~c8_2(X1,X2)|~c6_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_609, negated_conjecture, (c3_2(a512,a513)|c5_2(X1,X2)|~c1_1(a514)|~c3_2(X1,a515)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_615, negated_conjecture, (c3_2(a512,a513)|c5_2(X1,X2)|~c1_1(a514)|~c2_2(X1,a515)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_608, negated_conjecture, (c3_2(a512,a513)|c5_2(X1,X2)|~c1_1(a514)|~c2_2(X1,a516)|~c3_2(X1,a515)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_614, negated_conjecture, (c3_2(a512,a513)|c5_2(X1,X2)|~c1_1(a514)|~c2_2(X1,a515)|~c2_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_492, negated_conjecture, (c1_1(X1)|c8_1(X1)|c7_2(a530,X2)|~c6_1(X1)|~c2_0|~c6_2(a530,X2)|~c4_2(a530,X2)|~ndr1_1(a530))). % 23.51/3.56 cnf(i_0_963, negated_conjecture, (c5_1(X1)|c2_2(a488,X2)|c5_2(a488,X2)|ndr1_1(X1)|~c2_1(X1)|~c6_2(a488,X2)|~ndr1_1(a488))). % 23.51/3.56 cnf(i_0_624, negated_conjecture, (c5_1(a514)|c3_2(a512,a513)|c5_2(X1,X2)|c7_2(X1,a515)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1190, plain, (c1_2(X1,a493)|c3_2(X1,X2)|~epred1_0|~c5_2(X1,X2)|~c8_2(X1,X2)|~c6_2(X1,a492)|~ndr1_1(X1)|~c4_1(a491))). % 23.51/3.56 cnf(i_0_1186, plain, (c1_2(X1,a493)|c3_2(X1,X2)|~epred1_0|~c5_2(X1,X2)|~c7_2(X1,a492)|~c8_2(X1,X2)|~ndr1_1(X1)|~c4_1(a491))). % 23.51/3.56 cnf(i_0_1158, plain, (c1_2(X1,a493)|c3_2(X1,X2)|~epred1_0|~c5_1(a491)|~c5_2(X1,X2)|~c8_2(X1,X2)|~c6_2(X1,a492)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1154, plain, (c1_2(X1,a493)|c3_2(X1,X2)|~epred1_0|~c5_1(a491)|~c5_2(X1,X2)|~c7_2(X1,a492)|~c8_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_623, negated_conjecture, (c5_1(a514)|c3_2(a512,a513)|c5_2(X1,X2)|c7_2(X1,a515)|~c2_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_431, negated_conjecture, (c7_2(a538,X1)|c8_2(a538,X1)|~c7_1(a536)|~c2_2(a537,X2)|~c1_2(a538,X1)|~c3_2(a537,X2)|~c7_2(a537,X2)|~ndr1_1(a537)|~ndr1_1(a538))). % 23.51/3.56 cnf(i_0_621, negated_conjecture, (c5_1(a514)|c3_2(a512,a513)|c5_2(X1,X2)|~c3_2(X1,a515)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_627, negated_conjecture, (c5_1(a514)|c3_2(a512,a513)|c5_2(X1,X2)|~c2_2(X1,a515)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_115, negated_conjecture, (c5_1(X1)|c7_2(X1,X2)|c8_2(X1,X2)|c6_2(X1,X2)|~c3_1(a574)|~c6_1(X1)|~c2_0|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_612, negated_conjecture, (c3_2(a512,a513)|c5_2(X1,X2)|c7_2(X1,a515)|~c1_1(a514)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_333, negated_conjecture, (c2_2(X1,a548)|c3_2(X1,X2)|~c1_1(X1)|~c8_2(a546,a547)|~c8_2(X1,X2)|~c6_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_336, negated_conjecture, (c3_2(X1,X2)|c7_2(a546,a547)|~c1_1(X1)|~c8_2(X1,X2)|~c6_2(X1,X2)|~c4_2(X1,a548)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1299, plain, (c3_1(a587)|c5_2(X1,X2)|c8_2(X1,a589)|~epred3_0|~c2_2(X1,X2)|~c1_2(X1,a588)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_611, negated_conjecture, (c3_2(a512,a513)|c5_2(X1,X2)|c7_2(X1,a515)|~c1_1(a514)|~c2_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_620, negated_conjecture, (c5_1(a514)|c3_2(a512,a513)|c5_2(X1,X2)|~c2_2(X1,a516)|~c3_2(X1,a515)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_626, negated_conjecture, (c5_1(a514)|c3_2(a512,a513)|c5_2(X1,X2)|~c2_2(X1,a515)|~c2_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_446, negated_conjecture, (c1_1(a538)|c3_2(a536,X1)|c5_2(a536,X1)|~c2_2(a537,X2)|~c3_2(a537,X2)|~c7_2(a536,X1)|~c7_2(a537,X2)|~ndr1_1(a536)|~ndr1_1(a537))). % 23.51/3.56 cnf(i_0_415, negated_conjecture, (c5_1(a536)|c7_2(a538,X1)|c8_2(a538,X1)|~c2_2(a537,X2)|~c1_2(a538,X1)|~c3_2(a537,X2)|~c7_2(a537,X2)|~ndr1_1(a537)|~ndr1_1(a538))). % 23.51/3.56 cnf(i_0_314, negated_conjecture, (c2_2(a552,X1)|c7_0|c7_2(X2,a553)|c8_2(a552,X1)|c6_2(a552,X1)|~c5_1(X2)|~ndr1_1(a552)|~c4_1(X2))). % 23.51/3.56 cnf(i_0_720, negated_conjecture, (c5_1(a514)|c5_2(X1,X2)|c7_2(X1,a515)|~c1_2(a512,a513)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_40, negated_conjecture, (c2_2(X1,X2)|c7_0|c6_2(X1,X2)|~c6_1(a592)|~c6_1(X1)|~c7_2(X1,X2)|~c4_2(X1,a593)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_41, negated_conjecture, (c2_2(X1,X2)|c7_0|c6_2(X1,X2)|~c6_1(a592)|~c6_1(X1)|~c7_2(X1,a593)|~c7_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_672, negated_conjecture, (c5_1(a514)|c5_2(X1,X2)|c7_2(X1,a515)|~c2_2(a512,a513)|~c6_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_313, negated_conjecture, (c2_2(a552,X1)|c7_0|c8_2(a552,X1)|c6_2(a552,X1)|~c5_1(X2)|~c3_2(X2,a553)|~ndr1_1(a552)|~c4_1(X2))). % 23.51/3.56 cnf(i_0_315, negated_conjecture, (c2_2(a552,X1)|c7_0|c8_2(a552,X1)|c6_2(a552,X1)|~c5_1(X2)|~c2_2(X2,a553)|~ndr1_1(a552)|~c4_1(X2))). % 23.51/3.56 cnf(i_0_719, negated_conjecture, (c5_1(a514)|c5_2(X1,X2)|c7_2(X1,a515)|~c2_2(X1,a516)|~c1_2(a512,a513)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_671, negated_conjecture, (c5_1(a514)|c5_2(X1,X2)|c7_2(X1,a515)|~c2_2(a512,a513)|~c2_2(X1,a516)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_282, negated_conjecture, (c5_1(X1)|c7_1(X2)|c2_2(X2,X3)|c1_2(X2,a557)|c8_2(X2,X3)|~c3_1(X1)|~c6_1(X1)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_955, negated_conjecture, (c5_1(X1)|c2_2(a488,X2)|c5_2(a488,X2)|c4_2(X1,a487)|~c2_1(X1)|~c6_2(a488,X2)|~ndr1_1(a488))). % 23.51/3.56 cnf(i_0_1083, negated_conjecture, (c8_1(X1)|c8_2(X1,X2)|ndr1_1(X3)|~c8_1(X3)|~c2_1(X1)|~c6_1(X3)|~c7_2(X1,X2)|~c4_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_42, negated_conjecture, (c2_2(X1,X2)|c7_0|c8_2(X1,a593)|c6_2(X1,X2)|~c6_1(a592)|~c6_1(X1)|~c7_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1195, plain, (c3_2(X1,X2)|c4_2(X1,a492)|~epred1_0|~c5_2(X1,X2)|~c8_2(X1,X2)|~c6_2(X1,a493)|~ndr1_1(X1)|~c4_1(a491))). % 23.51/3.56 cnf(i_0_1193, plain, (c3_2(X1,X2)|c4_2(X1,a492)|~epred1_0|~c2_2(X1,a493)|~c5_2(X1,X2)|~c8_2(X1,X2)|~ndr1_1(X1)|~c4_1(a491))). % 23.51/3.56 cnf(i_0_959, negated_conjecture, (c5_1(X1)|c2_2(a488,X2)|c1_2(X1,a487)|c5_2(a488,X2)|~c2_1(X1)|~c6_2(a488,X2)|~ndr1_1(a488))). % 23.51/3.56 cnf(i_0_387, negated_conjecture, (c1_2(a544,X1)|c7_2(a542,X2)|c4_2(a544,X1)|~c8_1(X3)|~c2_1(X3)|~c4_2(a542,X2))). % 23.51/3.56 cnf(i_0_191, negated_conjecture, (c3_2(a564,X1)|c6_1(a565)|c5_2(a566,X2)|c8_2(a564,X1)|~c2_2(a566,X2)|~c1_2(a564,X1)|~c1_2(a566,X2)|~ndr1_1(a564))). % 23.51/3.56 cnf(i_0_177, negated_conjecture, (c3_2(a564,X1)|c2_1(a565)|c5_2(a566,X2)|c8_2(a564,X1)|~c2_2(a566,X2)|~c1_2(a564,X1)|~c1_2(a566,X2)|~ndr1_1(a564))). % 23.51/3.56 cnf(i_0_119, negated_conjecture, (c5_1(X1)|c7_2(X1,X2)|c8_2(X1,X2)|c6_2(X1,X2)|~c6_1(X1)|~c2_0|~c6_2(a574,a575)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1163, plain, (c3_2(X1,X2)|c4_2(X1,a492)|~epred1_0|~c5_1(a491)|~c5_2(X1,X2)|~c8_2(X1,X2)|~c6_2(X1,a493)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1161, plain, (c3_2(X1,X2)|c4_2(X1,a492)|~epred1_0|~c5_1(a491)|~c2_2(X1,a493)|~c5_2(X1,X2)|~c8_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_480, negated_conjecture, (c3_1(a532)|c2_1(X1)|c7_2(X1,X2)|c4_1(X1)|~c2_2(X1,X2)|~c3_1(a533)|~c6_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_478, negated_conjecture, (c1_1(a532)|c2_1(X1)|c7_2(X1,X2)|c4_1(X1)|~c2_2(X1,X2)|~c3_1(a533)|~c6_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_118, negated_conjecture, (c5_1(X1)|c7_2(X1,X2)|c8_2(X1,X2)|c6_2(X1,X2)|~c1_2(a574,a575)|~c6_1(X1)|~c2_0|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_184, negated_conjecture, (c3_1(a565)|c3_2(a564,X1)|c5_2(a566,X2)|c8_2(a564,X1)|~c2_2(a566,X2)|~c1_2(a564,X1)|~c1_2(a566,X2)|~ndr1_1(a564))). % 23.51/3.56 cnf(i_0_444, negated_conjecture, (c2_2(a538,X1)|c3_2(a538,X1)|c3_2(a536,X2)|c5_2(a536,X2)|~c5_1(a537)|~c7_2(a536,X2)|~c7_2(a538,X1)|~ndr1_1(a536)|~ndr1_1(a538))). % 23.51/3.56 cnf(i_0_1295, plain, (c3_1(a587)|c5_2(X1,a588)|c5_2(X1,X2)|c8_2(X1,a589)|~epred3_0|~c2_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_986, negated_conjecture, (c8_1(X1)|c8_2(X1,a481)|c4_2(X1,X2)|ndr1_1(a482)|~c3_2(X1,X2)|~c6_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1294, plain, (c3_1(a587)|c5_2(X1,a588)|c5_2(X1,X2)|~epred3_0|~c2_2(X1,X2)|~c7_2(X1,a589)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1293, plain, (c3_1(a587)|c5_2(X1,a588)|c5_2(X1,X2)|~epred3_0|~c2_2(X1,X2)|~c5_2(X1,a589)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_335, negated_conjecture, (c3_2(X1,X2)|c7_2(a546,a547)|~c1_1(X1)|~c7_2(X1,a548)|~c8_2(X1,X2)|~c6_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_984, negated_conjecture, (c8_1(X1)|c8_2(X1,a481)|c4_2(X1,X2)|~c3_2(X1,X2)|~c6_2(a482,a484)|~c6_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_440, negated_conjecture, (c2_2(a538,X1)|c3_2(a538,X1)|c3_2(a536,X2)|c5_2(a536,X2)|c4_1(a537)|~c7_2(a536,X2)|~c7_2(a538,X1)|~ndr1_1(a536)|~ndr1_1(a538))). % 23.51/3.56 cnf(i_0_443, negated_conjecture, (c3_2(a536,X1)|c5_2(a536,X1)|c7_2(a538,X2)|c8_2(a538,X2)|~c5_1(a537)|~c1_2(a538,X2)|~c7_2(a536,X1)|~ndr1_1(a536)|~ndr1_1(a538))). % 23.51/3.56 cnf(i_0_439, negated_conjecture, (c3_2(a536,X1)|c5_2(a536,X1)|c7_2(a538,X2)|c8_2(a538,X2)|c4_1(a537)|~c1_2(a538,X2)|~c7_2(a536,X1)|~ndr1_1(a536)|~ndr1_1(a538))). % 23.51/3.56 cnf(i_0_117, negated_conjecture, (c5_1(X1)|c7_2(X1,X2)|c8_2(X1,X2)|c6_2(X1,X2)|c4_2(a574,a575)|~c6_1(X1)|~c2_0|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_996, negated_conjecture, (c2_2(X1,a481)|c8_1(X1)|c4_2(X1,X2)|ndr1_1(a482)|~c3_2(X1,X2)|~c6_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_994, negated_conjecture, (c2_2(X1,a481)|c8_1(X1)|c4_2(X1,X2)|~c3_2(X1,X2)|~c6_2(a482,a484)|~c6_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_563, negated_conjecture, (c8_1(X1)|c3_2(X1,X2)|c6_1(X3)|~c3_1(X3)|~c2_0|~c6_2(X3,a525)|~c6_2(X1,X2)|~c4_2(X1,X2)|~ndr1_1(X1)|~c4_1(X1))). % 23.51/3.56 cnf(i_0_562, negated_conjecture, (c8_1(X1)|c3_2(X1,X2)|c6_1(X3)|~c2_2(X3,a525)|~c3_1(X3)|~c2_0|~c6_2(X1,X2)|~c4_2(X1,X2)|~ndr1_1(X1)|~c4_1(X1))). % 23.51/3.56 cnf(i_0_565, negated_conjecture, (c8_1(X1)|c3_2(X1,X2)|c6_1(X3)|ndr1_1(X3)|~c3_1(X3)|~c2_0|~c6_2(X1,X2)|~c4_2(X1,X2)|~ndr1_1(X1)|~c4_1(X1))). % 23.51/3.56 cnf(i_0_337, negated_conjecture, (c2_2(X1,a548)|c3_2(X1,X2)|c7_2(a546,a547)|~c1_1(X1)|~c8_2(X1,X2)|~c6_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_988, negated_conjecture, (c8_1(X1)|c8_2(a482,a483)|c8_2(X1,a481)|c4_2(X1,X2)|~c3_2(X1,X2)|~c6_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_985, negated_conjecture, (c8_1(X1)|c5_2(a482,a484)|c8_2(X1,a481)|c4_2(X1,X2)|~c3_2(X1,X2)|~c6_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_990, negated_conjecture, (c8_1(X1)|c3_2(a482,a483)|c8_2(X1,a481)|c4_2(X1,X2)|~c3_2(X1,X2)|~c6_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_989, negated_conjecture, (c2_2(a482,a483)|c8_1(X1)|c8_2(X1,a481)|c4_2(X1,X2)|~c3_2(X1,X2)|~c6_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1194, plain, (c1_2(X1,a493)|c3_2(X1,X2)|c4_2(X1,a492)|~epred1_0|~c5_2(X1,X2)|~c8_2(X1,X2)|~ndr1_1(X1)|~c4_1(a491))). % 23.51/3.56 cnf(i_0_1162, plain, (c1_2(X1,a493)|c3_2(X1,X2)|c4_2(X1,a492)|~epred1_0|~c5_1(a491)|~c5_2(X1,X2)|~c8_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_983, negated_conjecture, (c8_1(X1)|c8_2(X1,a481)|c4_2(X1,X2)|~c3_2(X1,X2)|~c6_2(X1,X2)|~c4_2(a482,a484)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_998, negated_conjecture, (c2_2(X1,a481)|c8_1(X1)|c8_2(a482,a483)|c4_2(X1,X2)|~c3_2(X1,X2)|~c6_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_995, negated_conjecture, (c2_2(X1,a481)|c8_1(X1)|c5_2(a482,a484)|c4_2(X1,X2)|~c3_2(X1,X2)|~c6_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1000, negated_conjecture, (c2_2(X1,a481)|c8_1(X1)|c3_2(a482,a483)|c4_2(X1,X2)|~c3_2(X1,X2)|~c6_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_999, negated_conjecture, (c2_2(a482,a483)|c2_2(X1,a481)|c8_1(X1)|c4_2(X1,X2)|~c3_2(X1,X2)|~c6_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_993, negated_conjecture, (c2_2(X1,a481)|c8_1(X1)|c4_2(X1,X2)|~c3_2(X1,X2)|~c6_2(X1,X2)|~c4_2(a482,a484)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_284, negated_conjecture, (c5_1(X1)|c7_1(X2)|c2_2(X2,X3)|c8_2(X2,X3)|~c3_1(X1)|~c6_1(X1)|~c6_2(X2,a557)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_283, negated_conjecture, (c5_1(X1)|c7_1(X2)|c2_2(X2,X3)|c8_2(X2,X3)|~c2_2(X2,a557)|~c3_1(X1)|~c6_1(X1)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_1082, negated_conjecture, (c8_1(X1)|c8_2(X2,a467)|c8_2(X1,X3)|~c8_1(X2)|~c2_1(X1)|~c6_1(X2)|~c7_2(X1,X3)|~c4_2(X1,X3)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1080, negated_conjecture, (c8_1(X1)|c3_2(X2,a467)|c8_2(X1,X3)|~c8_1(X2)|~c2_1(X1)|~c6_1(X2)|~c7_2(X1,X3)|~c4_2(X1,X3)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1081, negated_conjecture, (c2_2(X1,a467)|c8_1(X2)|c8_2(X2,X3)|~c8_1(X1)|~c2_1(X2)|~c6_1(X1)|~c7_2(X2,X3)|~c4_2(X2,X3)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_1013, negated_conjecture, (c1_2(X1,X2)|c3_1(X3)|c3_2(X1,X2)|~c8_1(X1)|~c2_1(X3)|~c7_2(X1,a479)|~c8_2(X1,X2)|~c6_2(X3,a480)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_74, negated_conjecture, (c5_1(X1)|c7_1(X1)|c7_1(X2)|c7_2(X2,X3)|ndr1_1(X1)|c4_1(X2)|~c2_2(X2,X3)|~c6_2(X2,X3)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_729, negated_conjecture, (c5_2(X1,X2)|c6_2(a514,X3)|~c1_2(a512,a513)|~c3_2(X1,a515)|~c8_2(a514,X3)|~c6_2(X1,a516)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_681, negated_conjecture, (c5_2(X1,X2)|c6_2(a514,X3)|~c2_2(a512,a513)|~c3_2(X1,a515)|~c8_2(a514,X3)|~c6_2(X1,a516)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_735, negated_conjecture, (c5_2(X1,X2)|c6_2(a514,X3)|~c2_2(X1,a515)|~c1_2(a512,a513)|~c8_2(a514,X3)|~c6_2(X1,a516)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_687, negated_conjecture, (c5_2(X1,X2)|c6_2(a514,X3)|~c2_2(a512,a513)|~c2_2(X1,a515)|~c8_2(a514,X3)|~c6_2(X1,a516)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_73, negated_conjecture, (c5_1(X1)|c7_1(X1)|c7_1(X2)|c7_2(X1,a583)|c7_2(X2,X3)|c4_1(X2)|~c2_2(X2,X3)|~c6_2(X2,X3)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_471, negated_conjecture, (c1_2(X1,X2)|c6_1(X1)|c7_2(X1,X2)|~c2_2(X1,X2)|~c1_2(X1,X3)|~c3_2(X1,X3)|~c2_1(a534)|~c6_2(X1,X3)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_59, negated_conjecture, (epred3_0|c2_2(X1,X2)|c6_1(X1)|c8_2(X1,X3)|c6_2(X1,X2)|~c2_2(X1,X3)|~c8_2(X1,X2)|~c4_2(X1,X3)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_486, negated_conjecture, (c5_1(X1)|c3_2(X1,X2)|c3_2(X1,X3)|c6_2(X1,X3)|~c1_2(X1,X2)|~c6_1(a531)|~c7_2(X1,X3)|~c8_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_487, negated_conjecture, (c5_1(X1)|c3_2(X1,X2)|c3_2(X1,X3)|c6_2(X1,X3)|~c5_1(a531)|~c1_2(X1,X2)|~c7_2(X1,X3)|~c8_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_71, negated_conjecture, (c5_1(X1)|c7_1(X1)|c7_1(X2)|c2_2(X1,a583)|c7_2(X2,X3)|c4_1(X2)|~c2_2(X2,X3)|~c6_2(X2,X3)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_728, negated_conjecture, (c5_2(X1,X2)|c6_2(a514,X3)|~c2_2(X1,a516)|~c1_2(a512,a513)|~c3_2(X1,a515)|~c8_2(a514,X3)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_680, negated_conjecture, (c5_2(X1,X2)|c6_2(a514,X3)|~c2_2(a512,a513)|~c2_2(X1,a516)|~c3_2(X1,a515)|~c8_2(a514,X3)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_734, negated_conjecture, (c5_2(X1,X2)|c6_2(a514,X3)|~c2_2(X1,a515)|~c2_2(X1,a516)|~c1_2(a512,a513)|~c8_2(a514,X3)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_686, negated_conjecture, (c5_2(X1,X2)|c6_2(a514,X3)|~c2_2(a512,a513)|~c2_2(X1,a515)|~c2_2(X1,a516)|~c8_2(a514,X3)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_12, negated_conjecture, (c1_2(X1,X2)|c8_1(X1)|c8_1(X3)|c3_1(X3)|c3_2(X1,X2)|c4_1(X1)|~c1_1(X3)|~c8_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_72, negated_conjecture, (c5_1(X1)|c7_1(X1)|c7_1(X2)|c7_2(X2,X3)|c4_1(X2)|~c2_2(X2,X3)|~c6_2(X2,X3)|~c4_2(X1,a583)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_1016, negated_conjecture, (c1_2(X1,X2)|c3_1(X3)|c3_2(X1,X2)|ndr1_1(X3)|~c8_1(X1)|~c2_1(X3)|~c7_2(X1,a479)|~c8_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_564, negated_conjecture, (c8_1(X1)|c3_2(X1,X2)|c6_1(X3)|c7_2(X3,a525)|~c3_1(X3)|~c2_0|~c6_2(X1,X2)|~c4_2(X1,X2)|~ndr1_1(X1)|~c4_1(X1))). % 23.51/3.56 cnf(i_0_474, negated_conjecture, (c1_2(X1,X2)|c6_1(X1)|c7_2(X1,X2)|~c2_2(X1,X2)|~c1_2(X1,X3)|~c3_2(X1,X3)|~c6_2(a534,a535)|~c6_2(X1,X3)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1286, plain, (c1_2(a587,X1)|c5_2(X2,X3)|~epred3_0|~c2_2(X2,X3)|~c1_2(X2,a588)|~c5_2(a587,X1)|~c7_2(X2,a589)|~c8_2(a587,X1)|~ndr1_1(a587)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_1020, negated_conjecture, (c1_2(X1,X2)|c3_1(X3)|c3_2(X1,X2)|c6_2(X1,a479)|ndr1_1(X3)|~c8_1(X1)|~c2_1(X3)|~c8_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_777, negated_conjecture, (c5_2(X1,X2)|c6_2(a514,X3)|ndr1_1(a512)|~c3_2(X1,a515)|~c8_2(a514,X3)|~c6_2(X1,a516)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_783, negated_conjecture, (c5_2(X1,X2)|c6_2(a514,X3)|ndr1_1(a512)|~c2_2(X1,a515)|~c8_2(a514,X3)|~c6_2(X1,a516)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_776, negated_conjecture, (c5_2(X1,X2)|c6_2(a514,X3)|ndr1_1(a512)|~c2_2(X1,a516)|~c3_2(X1,a515)|~c8_2(a514,X3)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_782, negated_conjecture, (c5_2(X1,X2)|c6_2(a514,X3)|ndr1_1(a512)|~c2_2(X1,a515)|~c2_2(X1,a516)|~c8_2(a514,X3)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1017, negated_conjecture, (c1_2(X1,X2)|c3_1(X3)|c3_2(X1,X2)|c6_2(X1,a479)|~c8_1(X1)|~c2_1(X3)|~c8_2(X1,X2)|~c6_2(X3,a480)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_348, negated_conjecture, (c3_2(X1,X2)|c8_2(a546,X3)|~c1_1(X1)|~c1_2(a546,X3)|~c8_2(X1,X2)|~c6_2(X1,X2)|~c4_2(X1,a548)|~c4_2(a546,X3)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_347, negated_conjecture, (c3_2(X1,X2)|c8_2(a546,X3)|~c1_1(X1)|~c1_2(a546,X3)|~c7_2(X1,a548)|~c8_2(X1,X2)|~c6_2(X1,X2)|~c4_2(a546,X3)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_475, negated_conjecture, (c1_2(X1,X2)|c6_1(X1)|c7_2(X1,X2)|ndr1_1(a534)|~c2_2(X1,X2)|~c1_2(X1,X3)|~c3_2(X1,X3)|~c6_2(X1,X3)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1018, negated_conjecture, (c1_2(X1,X2)|c3_1(X3)|c3_2(X1,X2)|c6_2(X1,a479)|c4_2(X3,a480)|~c8_1(X1)|~c2_1(X3)|~c8_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_825, negated_conjecture, (c6_1(a512)|c5_2(X1,X2)|c6_2(a514,X3)|~c3_2(X1,a515)|~c8_2(a514,X3)|~c6_2(X1,a516)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_831, negated_conjecture, (c6_1(a512)|c5_2(X1,X2)|c6_2(a514,X3)|~c2_2(X1,a515)|~c8_2(a514,X3)|~c6_2(X1,a516)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_824, negated_conjecture, (c6_1(a512)|c5_2(X1,X2)|c6_2(a514,X3)|~c2_2(X1,a516)|~c3_2(X1,a515)|~c8_2(a514,X3)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_830, negated_conjecture, (c6_1(a512)|c5_2(X1,X2)|c6_2(a514,X3)|~c2_2(X1,a515)|~c2_2(X1,a516)|~c8_2(a514,X3)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1019, negated_conjecture, (c1_2(X1,X2)|c3_1(X3)|c3_2(X3,a480)|c3_2(X1,X2)|c6_2(X1,a479)|~c8_1(X1)|~c2_1(X3)|~c8_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_38, negated_conjecture, (c2_2(X1,X2)|c3_2(a592,X3)|c7_0|c8_2(X1,a593)|c6_2(X1,X2)|~c6_1(X1)|~c5_2(a592,X3)|~c7_2(X1,X2)|~ndr1_1(a592)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_476, negated_conjecture, (c1_2(X1,X2)|c8_1(a534)|c6_1(X1)|c7_2(X1,X2)|~c2_2(X1,X2)|~c1_2(X1,X3)|~c3_2(X1,X3)|~c6_2(X1,X3)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_488, negated_conjecture, (c5_1(X1)|c3_2(X1,X2)|c3_2(X1,X3)|c6_2(X1,X3)|c4_1(a531)|~c1_2(X1,X2)|~c7_2(X1,X3)|~c8_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1285, plain, (c1_2(a587,X1)|c5_2(X2,X3)|~epred3_0|~c2_2(X2,X3)|~c1_2(X2,a588)|~c5_2(X2,a589)|~c5_2(a587,X1)|~c8_2(a587,X1)|~ndr1_1(a587)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_272, negated_conjecture, (c2_2(X1,X2)|c3_2(X1,X3)|c7_2(X1,X2)|c8_2(X1,X2)|~c2_2(X1,X3)|~c8_1(X1)|~c6_1(a559)|~c6_2(X1,X3)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_780, negated_conjecture, (c5_2(X1,X2)|c7_2(X1,a515)|c6_2(a514,X3)|ndr1_1(a512)|~c8_2(a514,X3)|~c6_2(X1,a516)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_633, negated_conjecture, (c3_2(a512,a513)|c5_2(X1,X2)|c6_2(a514,X3)|~c3_2(X1,a515)|~c8_2(a514,X3)|~c6_2(X1,a516)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_639, negated_conjecture, (c3_2(a512,a513)|c5_2(X1,X2)|c6_2(a514,X3)|~c2_2(X1,a515)|~c8_2(a514,X3)|~c6_2(X1,a516)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_632, negated_conjecture, (c3_2(a512,a513)|c5_2(X1,X2)|c6_2(a514,X3)|~c2_2(X1,a516)|~c3_2(X1,a515)|~c8_2(a514,X3)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_638, negated_conjecture, (c3_2(a512,a513)|c5_2(X1,X2)|c6_2(a514,X3)|~c2_2(X1,a515)|~c2_2(X1,a516)|~c8_2(a514,X3)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1014, negated_conjecture, (c1_2(X1,X2)|c3_1(X3)|c3_2(X1,X2)|c4_2(X3,a480)|~c8_1(X1)|~c2_1(X3)|~c7_2(X1,a479)|~c8_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_779, negated_conjecture, (c5_2(X1,X2)|c7_2(X1,a515)|c6_2(a514,X3)|ndr1_1(a512)|~c2_2(X1,a516)|~c8_2(a514,X3)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_349, negated_conjecture, (c2_2(X1,a548)|c3_2(X1,X2)|c8_2(a546,X3)|~c1_1(X1)|~c1_2(a546,X3)|~c8_2(X1,X2)|~c6_2(X1,X2)|~c4_2(a546,X3)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_36, negated_conjecture, (c2_2(X1,X2)|c3_2(a592,X3)|c7_0|c6_2(X1,X2)|~c6_1(X1)|~c5_2(a592,X3)|~c7_2(X1,X2)|~c4_2(X1,a593)|~ndr1_1(a592)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_37, negated_conjecture, (c2_2(X1,X2)|c3_2(a592,X3)|c7_0|c6_2(X1,X2)|~c6_1(X1)|~c5_2(a592,X3)|~c7_2(X1,a593)|~c7_2(X1,X2)|~ndr1_1(a592)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1287, plain, (c1_2(a587,X1)|c5_2(X2,X3)|c8_2(X2,a589)|~epred3_0|~c2_2(X2,X3)|~c1_2(X2,a588)|~c5_2(a587,X1)|~c8_2(a587,X1)|~ndr1_1(a587)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_828, negated_conjecture, (c6_1(a512)|c5_2(X1,X2)|c7_2(X1,a515)|c6_2(a514,X3)|~c8_2(a514,X3)|~c6_2(X1,a516)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_732, negated_conjecture, (c5_2(X1,X2)|c7_2(X1,a515)|c6_2(a514,X3)|~c1_2(a512,a513)|~c8_2(a514,X3)|~c6_2(X1,a516)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_684, negated_conjecture, (c5_2(X1,X2)|c7_2(X1,a515)|c6_2(a514,X3)|~c2_2(a512,a513)|~c8_2(a514,X3)|~c6_2(X1,a516)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_731, negated_conjecture, (c5_2(X1,X2)|c7_2(X1,a515)|c6_2(a514,X3)|~c2_2(X1,a516)|~c1_2(a512,a513)|~c8_2(a514,X3)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_683, negated_conjecture, (c5_2(X1,X2)|c7_2(X1,a515)|c6_2(a514,X3)|~c2_2(a512,a513)|~c2_2(X1,a516)|~c8_2(a514,X3)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1015, negated_conjecture, (c1_2(X1,X2)|c3_1(X3)|c3_2(X3,a480)|c3_2(X1,X2)|~c8_1(X1)|~c2_1(X3)|~c7_2(X1,a479)|~c8_2(X1,X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_827, negated_conjecture, (c6_1(a512)|c5_2(X1,X2)|c7_2(X1,a515)|c6_2(a514,X3)|~c2_2(X1,a516)|~c8_2(a514,X3)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_472, negated_conjecture, (c1_2(X1,X2)|c6_1(X1)|c7_2(X1,X2)|c8_2(a534,a535)|~c2_2(X1,X2)|~c1_2(X1,X3)|~c3_2(X1,X3)|~c6_2(X1,X3)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_275, negated_conjecture, (c2_2(X1,X2)|c3_2(X1,X3)|c7_2(X1,X2)|c8_2(X1,X2)|ndr1_1(a559)|~c2_2(X1,X3)|~c8_1(X1)|~c6_2(X1,X3)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_276, negated_conjecture, (c7_1(a559)|c2_2(X1,X2)|c3_2(X1,X3)|c7_2(X1,X2)|c8_2(X1,X2)|~c2_2(X1,X3)|~c8_1(X1)|~c6_2(X1,X3)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_116, negated_conjecture, (c5_1(X1)|c7_2(X1,X2)|c8_2(X1,X2)|c6_2(X1,X2)|~c2_2(a574,X3)|~c3_2(a574,X3)|~c6_1(X1)|~c2_0|~c4_2(a574,X3)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_636, negated_conjecture, (c3_2(a512,a513)|c5_2(X1,X2)|c7_2(X1,a515)|c6_2(a514,X3)|~c8_2(a514,X3)|~c6_2(X1,a516)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_635, negated_conjecture, (c3_2(a512,a513)|c5_2(X1,X2)|c7_2(X1,a515)|c6_2(a514,X3)|~c2_2(X1,a516)|~c8_2(a514,X3)|~c4_2(a514,X3)|~c4_2(X1,X2)|~ndr1_1(a514)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_448, negated_conjecture, (c2_2(a538,X1)|c3_2(a538,X1)|c3_2(a536,X2)|c5_2(a536,X2)|~c2_2(a537,X3)|~c3_2(a537,X3)|~c7_2(a536,X2)|~c7_2(a537,X3)|~c7_2(a538,X1)|~ndr1_1(a536)|~ndr1_1(a537)|~ndr1_1(a538))). % 23.51/3.56 cnf(i_0_447, negated_conjecture, (c3_2(a536,X1)|c5_2(a536,X1)|c7_2(a538,X2)|c8_2(a538,X2)|~c2_2(a537,X3)|~c1_2(a538,X2)|~c3_2(a537,X3)|~c7_2(a536,X1)|~c7_2(a537,X3)|~ndr1_1(a536)|~ndr1_1(a537)|~ndr1_1(a538))). % 23.51/3.56 cnf(i_0_482, negated_conjecture, (c2_1(X1)|c7_2(a532,X2)|c7_2(X1,X3)|c4_1(X1)|~c2_2(X1,X3)|~c3_1(a533)|~c8_2(a532,X2)|~c6_2(X1,X3)|~c4_2(a532,X2)|~ndr1_1(a532)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_123, negated_conjecture, (c2_2(X1,X2)|c1_2(X1,X2)|c8_1(X1)|c3_1(a573)|c5_2(X1,X3)|c4_2(X1,X3)|~c3_2(X1,X2)|~c7_2(X1,X3)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_124, negated_conjecture, (c1_1(a573)|c2_2(X1,X2)|c1_2(X1,X2)|c8_1(X1)|c5_2(X1,X3)|c4_2(X1,X3)|~c3_2(X1,X2)|~c7_2(X1,X3)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1282, plain, (c1_2(a587,X1)|c5_2(X2,a588)|c5_2(X2,X3)|~epred3_0|~c2_2(X2,X3)|~c5_2(a587,X1)|~c7_2(X2,a589)|~c8_2(a587,X1)|~ndr1_1(a587)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_1281, plain, (c1_2(a587,X1)|c5_2(X2,a588)|c5_2(X2,X3)|~epred3_0|~c2_2(X2,X3)|~c5_2(X2,a589)|~c5_2(a587,X1)|~c8_2(a587,X1)|~ndr1_1(a587)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_473, negated_conjecture, (c1_2(X1,X2)|c6_1(X1)|c7_2(X1,X2)|c4_2(a534,a535)|~c2_2(X1,X2)|~c1_2(X1,X3)|~c3_2(X1,X3)|~c6_2(X1,X3)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_987, negated_conjecture, (c2_2(a482,X1)|c8_1(X2)|c8_2(X2,a481)|c4_2(X2,X3)|~c3_2(X2,X3)|~c8_2(a482,X1)|~c6_2(a482,X1)|~c6_2(X2,X3)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_46, negated_conjecture, (c2_2(X1,X2)|c7_0|c5_2(a592,X3)|c8_2(X1,a593)|c6_2(a592,X3)|c6_2(X1,X2)|~c1_2(a592,X3)|~c6_1(X1)|~c7_2(X1,X2)|~ndr1_1(a592)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_997, negated_conjecture, (c2_2(a482,X1)|c2_2(X2,a481)|c8_1(X2)|c4_2(X2,X3)|~c3_2(X2,X3)|~c8_2(a482,X1)|~c6_2(a482,X1)|~c6_2(X2,X3)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_44, negated_conjecture, (c2_2(X1,X2)|c7_0|c5_2(a592,X3)|c6_2(a592,X3)|c6_2(X1,X2)|~c1_2(a592,X3)|~c6_1(X1)|~c7_2(X1,X2)|~c4_2(X1,a593)|~ndr1_1(a592)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_45, negated_conjecture, (c2_2(X1,X2)|c7_0|c5_2(a592,X3)|c6_2(a592,X3)|c6_2(X1,X2)|~c1_2(a592,X3)|~c6_1(X1)|~c7_2(X1,a593)|~c7_2(X1,X2)|~ndr1_1(a592)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_274, negated_conjecture, (c2_2(X1,X2)|c3_2(X1,X3)|c7_2(X1,X2)|c8_2(X1,X2)|c4_2(a559,a560)|~c2_2(X1,X3)|~c8_1(X1)|~c6_2(X1,X3)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1283, plain, (c1_2(a587,X1)|c5_2(X2,a588)|c5_2(X2,X3)|c8_2(X2,a589)|~epred3_0|~c2_2(X2,X3)|~c5_2(a587,X1)|~c8_2(a587,X1)|~ndr1_1(a587)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_273, negated_conjecture, (c2_2(X1,X2)|c3_2(X1,X3)|c7_2(a559,a560)|c7_2(X1,X2)|c8_2(X1,X2)|~c2_2(X1,X3)|~c8_1(X1)|~c6_2(X1,X3)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_932, negated_conjecture, (c1_1(X1)|c2_2(X2,X3)|c2_2(X2,X4)|c1_2(X2,X4)|c2_1(X1)|c2_0|~c5_1(X2)|~c1_2(X2,X3)|~c5_2(X2,X4)|~c7_2(X2,X3)|~ndr1_1(X2)|~c4_1(X1))). % 23.51/3.56 cnf(i_0_1175, plain, (c3_2(a491,X1)|c3_2(X2,X3)|c6_2(a491,X1)|c4_2(a491,X1)|~epred1_0|~c5_2(X2,X3)|~c8_2(X2,X3)|~c6_2(X2,a492)|~c6_2(X2,a493)|~ndr1_1(a491)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_1173, plain, (c3_2(a491,X1)|c3_2(X2,X3)|c6_2(a491,X1)|c4_2(a491,X1)|~epred1_0|~c2_2(X2,a493)|~c5_2(X2,X3)|~c8_2(X2,X3)|~c6_2(X2,a492)|~ndr1_1(a491)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_1171, plain, (c3_2(a491,X1)|c3_2(X2,X3)|c6_2(a491,X1)|c4_2(a491,X1)|~epred1_0|~c5_2(X2,X3)|~c7_2(X2,a492)|~c8_2(X2,X3)|~c6_2(X2,a493)|~ndr1_1(a491)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_1174, plain, (c1_2(X1,a493)|c3_2(a491,X2)|c3_2(X1,X3)|c6_2(a491,X2)|c4_2(a491,X2)|~epred1_0|~c5_2(X1,X3)|~c8_2(X1,X3)|~c6_2(X1,a492)|~ndr1_1(a491)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1169, plain, (c3_2(a491,X1)|c3_2(X2,X3)|c6_2(a491,X1)|c4_2(a491,X1)|~epred1_0|~c2_2(X2,a493)|~c5_2(X2,X3)|~c7_2(X2,a492)|~c8_2(X2,X3)|~ndr1_1(a491)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_1170, plain, (c1_2(X1,a493)|c3_2(a491,X2)|c3_2(X1,X3)|c6_2(a491,X2)|c4_2(a491,X2)|~epred1_0|~c5_2(X1,X3)|~c7_2(X1,a492)|~c8_2(X1,X3)|~ndr1_1(a491)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_520, negated_conjecture, (c2_2(X1,X2)|c3_2(X3,X4)|c3_2(X1,X2)|c2_1(X3)|c8_2(X3,X4)|c6_2(X3,a528)|~c4_0|~c1_2(X1,a527)|~c1_2(X1,X2)|~c3_2(X1,a526)|~c7_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3))). % 23.51/3.56 cnf(i_0_519, negated_conjecture, (c2_2(X1,a528)|c2_2(X2,X3)|c3_2(X1,X4)|c3_2(X2,X3)|c2_1(X1)|c8_2(X1,X4)|~c4_0|~c1_2(X2,a527)|~c1_2(X2,X3)|~c3_2(X2,a526)|~c7_2(X1,X4)|~ndr1_1(X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1178, plain, (c1_2(X1,a493)|c3_2(a491,X2)|c3_2(X1,X3)|c6_2(a491,X2)|c4_2(a491,X2)|c4_2(X1,a492)|~epred1_0|~c5_2(X1,X3)|~c8_2(X1,X3)|~ndr1_1(a491)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1179, plain, (c3_2(a491,X1)|c3_2(X2,X3)|c6_2(a491,X1)|c4_2(a491,X1)|c4_2(X2,a492)|~epred1_0|~c5_2(X2,X3)|~c8_2(X2,X3)|~c6_2(X2,a493)|~ndr1_1(a491)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_518, negated_conjecture, (c2_2(X1,X2)|c3_2(X3,X4)|c3_2(X1,X2)|c2_1(X3)|c8_2(X3,X4)|~c4_0|~c1_2(X1,a527)|~c1_2(X1,X2)|~c3_2(X1,a526)|~c5_2(X3,a528)|~c7_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3))). % 23.51/3.56 cnf(i_0_1177, plain, (c3_2(a491,X1)|c3_2(X2,X3)|c6_2(a491,X1)|c4_2(a491,X1)|c4_2(X2,a492)|~epred1_0|~c2_2(X2,a493)|~c5_2(X2,X3)|~c8_2(X2,X3)|~ndr1_1(a491)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_1042, negated_conjecture, (c1_2(X1,X2)|c8_1(X3)|c6_1(X1)|c4_2(X1,X2)|c4_2(X3,X4)|ndr1_1(X5)|~c5_1(X5)|~c7_1(X1)|~c3_1(X3)|~c3_2(X3,X4)|~c6_2(X3,X4)|~c6_2(X1,X2)|~ndr1_1(X3)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_522, negated_conjecture, (c2_2(X1,X2)|c3_2(X3,X4)|c3_2(X1,X2)|c2_1(X3)|c8_2(X3,X4)|~c4_0|~c2_2(X1,a527)|~c1_2(X1,X2)|~c3_2(X1,a526)|~c5_2(X3,a528)|~c7_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3))). % 23.51/3.56 cnf(i_0_122, negated_conjecture, (c2_2(X1,X2)|c1_2(X1,X2)|c8_1(X1)|c5_2(a573,X3)|c5_2(X1,X4)|c4_2(X1,X4)|~c2_2(a573,X3)|~c3_2(X1,X2)|~c7_2(X1,X4)|~c6_2(a573,X3)|~ndr1_1(a573)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_524, negated_conjecture, (c2_2(X1,X2)|c3_2(X3,X4)|c3_2(X1,X2)|c2_1(X3)|c8_2(X3,X4)|c6_2(X3,a528)|~c4_0|~c2_2(X1,a527)|~c1_2(X1,X2)|~c3_2(X1,a526)|~c7_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3))). % 23.51/3.56 cnf(i_0_523, negated_conjecture, (c2_2(X1,a528)|c2_2(X2,X3)|c3_2(X1,X4)|c3_2(X2,X3)|c2_1(X1)|c8_2(X1,X4)|~c4_0|~c2_2(X2,a527)|~c1_2(X2,X3)|~c3_2(X2,a526)|~c7_2(X1,X4)|~ndr1_1(X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_516, negated_conjecture, (c2_2(X1,X2)|c3_2(X3,X4)|c3_2(X1,X2)|c2_1(X3)|c8_2(X3,X4)|c6_2(X3,a528)|c4_2(X1,a527)|~c4_0|~c1_2(X1,X2)|~c3_2(X1,a526)|~c7_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3))). % 23.51/3.56 cnf(i_0_515, negated_conjecture, (c2_2(X1,a528)|c2_2(X2,X3)|c3_2(X1,X4)|c3_2(X2,X3)|c2_1(X1)|c8_2(X1,X4)|c4_2(X2,a527)|~c4_0|~c1_2(X2,X3)|~c3_2(X2,a526)|~c7_2(X1,X4)|~ndr1_1(X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_108, negated_conjecture, (c7_1(X1)|c2_2(X2,X3)|c3_2(X2,X4)|c3_2(X2,X5)|c5_2(X2,X5)|c8_2(X2,X4)|c6_2(X2,X3)|ndr1_1(a577)|ndr1_1(X1)|~c1_1(X1)|~c2_2(X2,X4)|~c1_2(X2,X5)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_500, negated_conjecture, (c2_2(X1,X2)|c3_2(X3,X4)|c3_2(X1,X2)|c2_1(X3)|c8_2(X1,a526)|c8_2(X3,X4)|c6_2(X3,a528)|c4_2(X1,a527)|~c4_0|~c1_2(X1,X2)|~c7_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3))). % 23.51/3.56 cnf(i_0_1041, negated_conjecture, (c1_2(X1,X2)|c8_1(X3)|c6_1(X1)|c6_2(X4,a474)|c4_2(X1,X2)|c4_2(X3,X5)|~c5_1(X4)|~c7_1(X1)|~c3_1(X3)|~c3_2(X3,X5)|~c6_2(X3,X5)|~c6_2(X1,X2)|~ndr1_1(X3)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1040, negated_conjecture, (c1_2(X1,X2)|c8_1(X3)|c6_1(X1)|c7_2(X4,a474)|c4_2(X1,X2)|c4_2(X3,X5)|~c5_1(X4)|~c7_1(X1)|~c3_1(X3)|~c3_2(X3,X5)|~c6_2(X3,X5)|~c6_2(X1,X2)|~ndr1_1(X3)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_1039, negated_conjecture, (c1_2(X1,a474)|c1_2(X2,X3)|c8_1(X4)|c6_1(X2)|c4_2(X2,X3)|c4_2(X4,X5)|~c5_1(X1)|~c7_1(X2)|~c3_1(X4)|~c3_2(X4,X5)|~c6_2(X4,X5)|~c6_2(X2,X3)|~ndr1_1(X4)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_514, negated_conjecture, (c2_2(X1,X2)|c3_2(X3,X4)|c3_2(X1,X2)|c2_1(X3)|c8_2(X3,X4)|c4_2(X1,a527)|~c4_0|~c1_2(X1,X2)|~c3_2(X1,a526)|~c5_2(X3,a528)|~c7_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3))). % 23.51/3.56 cnf(i_0_532, negated_conjecture, (c2_2(X1,X2)|c3_2(X3,X4)|c3_2(X1,X2)|c2_1(X3)|c7_2(X1,a526)|c8_2(X3,X4)|c6_2(X3,a528)|c4_2(X1,a527)|~c4_0|~c1_2(X1,X2)|~c7_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3))). % 23.51/3.56 cnf(i_0_504, negated_conjecture, (c2_2(X1,X2)|c3_2(X3,X4)|c3_2(X1,X2)|c2_1(X3)|c8_2(X1,a526)|c8_2(X3,X4)|c6_2(X3,a528)|~c4_0|~c1_2(X1,a527)|~c1_2(X1,X2)|~c7_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3))). % 23.51/3.56 cnf(i_0_508, negated_conjecture, (c2_2(X1,X2)|c3_2(X3,X4)|c3_2(X1,X2)|c2_1(X3)|c8_2(X1,a526)|c8_2(X3,X4)|c6_2(X3,a528)|~c4_0|~c2_2(X1,a527)|~c1_2(X1,X2)|~c7_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3))). % 23.51/3.56 cnf(i_0_536, negated_conjecture, (c2_2(X1,X2)|c3_2(X3,X4)|c3_2(X1,X2)|c2_1(X3)|c7_2(X1,a526)|c8_2(X3,X4)|c6_2(X3,a528)|~c4_0|~c1_2(X1,a527)|~c1_2(X1,X2)|~c7_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3))). % 23.51/3.56 cnf(i_0_540, negated_conjecture, (c2_2(X1,X2)|c3_2(X3,X4)|c3_2(X1,X2)|c2_1(X3)|c7_2(X1,a526)|c8_2(X3,X4)|c6_2(X3,a528)|~c4_0|~c2_2(X1,a527)|~c1_2(X1,X2)|~c7_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3))). % 23.51/3.56 cnf(i_0_499, negated_conjecture, (c2_2(X1,a528)|c2_2(X2,X3)|c3_2(X1,X4)|c3_2(X2,X3)|c2_1(X1)|c8_2(X2,a526)|c8_2(X1,X4)|c4_2(X2,a527)|~c4_0|~c1_2(X2,X3)|~c7_2(X1,X4)|~ndr1_1(X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_502, negated_conjecture, (c2_2(X1,X2)|c3_2(X3,X4)|c3_2(X1,X2)|c2_1(X3)|c8_2(X1,a526)|c8_2(X3,X4)|~c4_0|~c1_2(X1,a527)|~c1_2(X1,X2)|~c5_2(X3,a528)|~c7_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3))). % 23.51/3.56 cnf(i_0_506, negated_conjecture, (c2_2(X1,X2)|c3_2(X3,X4)|c3_2(X1,X2)|c2_1(X3)|c8_2(X1,a526)|c8_2(X3,X4)|~c4_0|~c2_2(X1,a527)|~c1_2(X1,X2)|~c5_2(X3,a528)|~c7_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3))). % 23.51/3.56 cnf(i_0_534, negated_conjecture, (c2_2(X1,X2)|c3_2(X3,X4)|c3_2(X1,X2)|c2_1(X3)|c7_2(X1,a526)|c8_2(X3,X4)|~c4_0|~c1_2(X1,a527)|~c1_2(X1,X2)|~c5_2(X3,a528)|~c7_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3))). % 23.51/3.56 cnf(i_0_538, negated_conjecture, (c2_2(X1,X2)|c3_2(X3,X4)|c3_2(X1,X2)|c2_1(X3)|c7_2(X1,a526)|c8_2(X3,X4)|~c4_0|~c2_2(X1,a527)|~c1_2(X1,X2)|~c5_2(X3,a528)|~c7_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3))). % 23.51/3.56 cnf(i_0_531, negated_conjecture, (c2_2(X1,a528)|c2_2(X2,X3)|c3_2(X1,X4)|c3_2(X2,X3)|c2_1(X1)|c7_2(X2,a526)|c8_2(X1,X4)|c4_2(X2,a527)|~c4_0|~c1_2(X2,X3)|~c7_2(X1,X4)|~ndr1_1(X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_503, negated_conjecture, (c2_2(X1,a528)|c2_2(X2,X3)|c3_2(X1,X4)|c3_2(X2,X3)|c2_1(X1)|c8_2(X2,a526)|c8_2(X1,X4)|~c4_0|~c1_2(X2,a527)|~c1_2(X2,X3)|~c7_2(X1,X4)|~ndr1_1(X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_507, negated_conjecture, (c2_2(X1,a528)|c2_2(X2,X3)|c3_2(X1,X4)|c3_2(X2,X3)|c2_1(X1)|c8_2(X2,a526)|c8_2(X1,X4)|~c4_0|~c2_2(X2,a527)|~c1_2(X2,X3)|~c7_2(X1,X4)|~ndr1_1(X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_535, negated_conjecture, (c2_2(X1,a528)|c2_2(X2,X3)|c3_2(X1,X4)|c3_2(X2,X3)|c2_1(X1)|c7_2(X2,a526)|c8_2(X1,X4)|~c4_0|~c1_2(X2,a527)|~c1_2(X2,X3)|~c7_2(X1,X4)|~ndr1_1(X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_539, negated_conjecture, (c2_2(X1,a528)|c2_2(X2,X3)|c3_2(X1,X4)|c3_2(X2,X3)|c2_1(X1)|c7_2(X2,a526)|c8_2(X1,X4)|~c4_0|~c2_2(X2,a527)|~c1_2(X2,X3)|~c7_2(X1,X4)|~ndr1_1(X2)|~ndr1_1(X1))). % 23.51/3.56 cnf(i_0_113, negated_conjecture, (c7_1(X1)|c2_2(X2,X3)|c3_2(X2,X4)|c3_2(X2,X5)|c5_2(X2,X5)|c8_2(X2,X4)|c6_2(X2,X3)|ndr1_1(X1)|~c1_1(X1)|~c7_1(a577)|~c2_2(X2,X4)|~c1_2(X2,X5)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_498, negated_conjecture, (c2_2(X1,X2)|c3_2(X3,X4)|c3_2(X1,X2)|c2_1(X3)|c8_2(X1,a526)|c8_2(X3,X4)|c4_2(X1,a527)|~c4_0|~c1_2(X1,X2)|~c5_2(X3,a528)|~c7_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3))). % 23.51/3.56 cnf(i_0_530, negated_conjecture, (c2_2(X1,X2)|c3_2(X3,X4)|c3_2(X1,X2)|c2_1(X3)|c7_2(X1,a526)|c8_2(X3,X4)|c4_2(X1,a527)|~c4_0|~c1_2(X1,X2)|~c5_2(X3,a528)|~c7_2(X3,X4)|~ndr1_1(X1)|~ndr1_1(X3))). % 23.51/3.56 cnf(i_0_95, negated_conjecture, (c7_1(X1)|c2_2(X2,X3)|c3_2(X2,X4)|c3_2(X2,X5)|c5_2(X2,X5)|c8_2(X2,X4)|c6_2(X2,X3)|~c1_1(X1)|~c7_1(a577)|~c2_2(X2,X4)|~c1_2(X2,X5)|~c8_2(X1,a576)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_89, negated_conjecture, (c7_1(X1)|c2_2(X2,X3)|c3_2(X2,X4)|c3_2(X2,X5)|c5_2(X2,X5)|c8_2(X2,X4)|c6_2(X2,X3)|~c1_1(X1)|~c2_2(X2,X4)|~c1_2(X2,X5)|~c8_2(X1,a576)|~c6_2(a577,a579)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_88, negated_conjecture, (c7_1(X1)|c2_2(X2,X3)|c3_2(X2,X4)|c3_2(X2,X5)|c5_2(X2,X5)|c8_2(X2,X4)|c6_2(X2,X3)|~c1_1(X1)|~c2_2(X2,X4)|~c1_2(X2,X5)|~c8_2(a577,a579)|~c8_2(X1,a576)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_109, negated_conjecture, (c7_1(X1)|c2_2(X2,X3)|c3_2(X2,X4)|c3_2(X2,X5)|c5_2(X2,X5)|c8_2(X2,X4)|c6_2(a577,a578)|c6_2(X2,X3)|ndr1_1(X1)|~c1_1(X1)|~c2_2(X2,X4)|~c1_2(X2,X5)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_90, negated_conjecture, (c7_1(X1)|c2_2(X2,X3)|c3_2(X2,X4)|c3_2(X2,X5)|c5_2(X2,X5)|c8_2(X2,X4)|c6_2(X2,X3)|ndr1_1(a577)|~c1_1(X1)|~c2_2(X2,X4)|~c1_2(X2,X5)|~c8_2(X1,a576)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_91, negated_conjecture, (c7_1(X1)|c2_2(X2,X3)|c3_2(X2,X4)|c3_2(X2,X5)|c5_2(X2,X5)|c8_2(X2,X4)|c6_2(a577,a578)|c6_2(X2,X3)|~c1_1(X1)|~c2_2(X2,X4)|~c1_2(X2,X5)|~c8_2(X1,a576)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_93, negated_conjecture, (c7_1(X1)|c2_2(X2,X3)|c3_2(X2,X4)|c3_2(X2,X5)|c5_2(X2,X5)|c8_2(a577,a578)|c8_2(X2,X4)|c6_2(X2,X3)|~c1_1(X1)|~c2_2(X2,X4)|~c1_2(X2,X5)|~c8_2(X1,a576)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_111, negated_conjecture, (c7_1(X1)|c2_2(X2,X3)|c3_2(X2,X4)|c3_2(X2,X5)|c5_2(X2,X5)|c8_2(a577,a578)|c8_2(X2,X4)|c6_2(X2,X3)|ndr1_1(X1)|~c1_1(X1)|~c2_2(X2,X4)|~c1_2(X2,X5)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_110, negated_conjecture, (c7_1(X1)|c2_2(X2,X3)|c1_2(a577,a578)|c3_2(X2,X4)|c3_2(X2,X5)|c5_2(X2,X5)|c8_2(X2,X4)|c6_2(X2,X3)|ndr1_1(X1)|~c1_1(X1)|~c2_2(X2,X4)|~c1_2(X2,X5)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_107, negated_conjecture, (c7_1(X1)|c2_2(X2,X3)|c3_2(X2,X4)|c3_2(X2,X5)|c5_2(X2,X5)|c8_2(X2,X4)|c6_2(X2,X3)|ndr1_1(X1)|~c1_1(X1)|~c2_2(X2,X4)|~c1_2(X2,X5)|~c6_2(a577,a579)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_106, negated_conjecture, (c7_1(X1)|c2_2(X2,X3)|c3_2(X2,X4)|c3_2(X2,X5)|c5_2(X2,X5)|c8_2(X2,X4)|c6_2(X2,X3)|ndr1_1(X1)|~c1_1(X1)|~c2_2(X2,X4)|~c1_2(X2,X5)|~c8_2(a577,a579)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_104, negated_conjecture, (c7_1(X1)|c2_2(X2,X3)|c3_2(X2,X4)|c3_2(X2,X5)|c5_2(X2,X5)|c8_2(X2,X4)|c6_2(X2,X3)|c4_2(X1,a576)|~c1_1(X1)|~c7_1(a577)|~c2_2(X2,X4)|~c1_2(X2,X5)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_92, negated_conjecture, (c7_1(X1)|c2_2(X2,X3)|c1_2(a577,a578)|c3_2(X2,X4)|c3_2(X2,X5)|c5_2(X2,X5)|c8_2(X2,X4)|c6_2(X2,X3)|~c1_1(X1)|~c2_2(X2,X4)|~c1_2(X2,X5)|~c8_2(X1,a576)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_99, negated_conjecture, (c7_1(X1)|c2_2(X2,X3)|c3_2(X2,X4)|c3_2(X2,X5)|c5_2(X2,X5)|c8_2(X2,X4)|c6_2(X2,X3)|c4_2(X1,a576)|ndr1_1(a577)|~c1_1(X1)|~c2_2(X2,X4)|~c1_2(X2,X5)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_98, negated_conjecture, (c7_1(X1)|c2_2(X2,X3)|c3_2(X2,X4)|c3_2(X2,X5)|c5_2(X2,X5)|c8_2(X2,X4)|c6_2(X2,X3)|c4_2(X1,a576)|~c1_1(X1)|~c2_2(X2,X4)|~c1_2(X2,X5)|~c6_2(a577,a579)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_97, negated_conjecture, (c7_1(X1)|c2_2(X2,X3)|c3_2(X2,X4)|c3_2(X2,X5)|c5_2(X2,X5)|c8_2(X2,X4)|c6_2(X2,X3)|c4_2(X1,a576)|~c1_1(X1)|~c2_2(X2,X4)|~c1_2(X2,X5)|~c8_2(a577,a579)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_100, negated_conjecture, (c7_1(X1)|c2_2(X2,X3)|c3_2(X2,X4)|c3_2(X2,X5)|c5_2(X2,X5)|c8_2(X2,X4)|c6_2(a577,a578)|c6_2(X2,X3)|c4_2(X1,a576)|~c1_1(X1)|~c2_2(X2,X4)|~c1_2(X2,X5)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_102, negated_conjecture, (c7_1(X1)|c2_2(X2,X3)|c3_2(X2,X4)|c3_2(X2,X5)|c5_2(X2,X5)|c8_2(a577,a578)|c8_2(X2,X4)|c6_2(X2,X3)|c4_2(X1,a576)|~c1_1(X1)|~c2_2(X2,X4)|~c1_2(X2,X5)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_101, negated_conjecture, (c7_1(X1)|c2_2(X2,X3)|c1_2(a577,a578)|c3_2(X2,X4)|c3_2(X2,X5)|c5_2(X2,X5)|c8_2(X2,X4)|c6_2(X2,X3)|c4_2(X1,a576)|~c1_1(X1)|~c2_2(X2,X4)|~c1_2(X2,X5)|~ndr1_1(X2))). % 23.51/3.56 cnf(i_0_1088, negated_conjecture, (c1_1(X1)|c1_2(X2,X3)|c1_2(X1,X4)|c8_1(X5)|c8_1(X2)|c3_2(X1,X4)|c2_1(X1)|c5_2(X5,X6)|c7_2(X1,X4)|~c1_1(X2)|~c2_2(X2,X3)|~c7_2(X5,a465)|~c7_2(X5,X6)|~c6_2(X2,X3)|~c6_2(X5,X6)|~ndr1_1(X1)|~ndr1_1(X2)|~ndr1_1(X5))). % 23.51/3.56 cnf(i_0_1090, negated_conjecture, (c1_1(X1)|c1_2(X2,X3)|c1_2(X1,X4)|c8_1(X5)|c8_1(X2)|c3_2(X1,X4)|c2_1(X1)|c5_2(X5,X6)|c7_2(X1,X4)|~c1_1(X2)|~c2_2(X2,X3)|~c1_2(X5,a465)|~c7_2(X5,X6)|~c6_2(X2,X3)|~c6_2(X5,X6)|~ndr1_1(X1)|~ndr1_1(X2)|~ndr1_1(X5))). % 23.51/3.56 cnf(i_0_1089, negated_conjecture, (c1_1(X1)|c1_2(X2,X3)|c1_2(X1,X4)|c8_1(X5)|c8_1(X2)|c3_2(X1,X4)|c2_1(X1)|c5_2(X5,X6)|c7_2(X1,X4)|~c1_1(X2)|~c2_2(X2,X3)|~c5_2(X5,a465)|~c7_2(X5,X6)|~c6_2(X2,X3)|~c6_2(X5,X6)|~ndr1_1(X1)|~ndr1_1(X2)|~ndr1_1(X5))). % 23.51/3.56 # End listing active clauses. There is an equivalent clause to each of these in the clausification! % 23.51/3.56 # Begin printing tableau % 23.51/3.56 # Found 5 steps % 23.51/3.56 cnf(i_0_134, negated_conjecture, (c5_1(a570)), inference(start_rule)). % 23.51/3.56 cnf(i_0_4728, plain, (c5_1(a570)), inference(extension_rule, [i_0_308])). % 23.51/3.56 cnf(i_0_2627906, plain, (~c4_1(a570)), inference(closure_rule, [i_0_135])). % 23.51/3.56 cnf(i_0_2627902, plain, (c6_1(a552)), inference(extension_rule, [i_0_283])). % 23.51/3.56 cnf(i_0_2629021, plain, (~ndr1_1(a520)), inference(closure_rule, [i_0_579])). % 23.51/3.56 # End printing tableau % 23.51/3.56 # SZS output end % 23.51/3.56 # Branches closed with saturation will be marked with an "s" % 23.51/3.57 # Child (6920) has found a proof. % 23.51/3.57 % 23.51/3.57 # Proof search is over... % 23.51/3.57 # Freeing feature tree %------------------------------------------------------------------------------