%------------------------------------------------------------------------------ % File : Etableau---0.67 % Problem : SYN453-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 : n026.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:11:15 EDT 2022 % Result : Satisfiable 66.46s 8.80s % Output : CNFRefutation 66.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN453-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.13/0.34 % Computer : n026.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Tue Jul 12 09:14:57 EDT 2022 % 0.13/0.34 % CPUTime : % 0.19/0.38 # No SInE strategy applied % 0.19/0.38 # Auto-Mode selected heuristic G_N___023_B07_F1_SP_PI_Q7_CS_SP_CO_S5PRR_S0Y % 0.19/0.38 # and selection function SelectMaxLComplexAvoidPosPred. % 0.19/0.38 # % 0.19/0.38 # Number of axioms: 344 Number of unprocessed: 344 % 0.19/0.38 # Tableaux proof search. % 0.19/0.38 # APR header successfully linked. % 0.19/0.38 # Hello from C++ % 0.19/0.39 # The folding up rule is enabled... % 0.19/0.39 # Local unification is enabled... % 0.19/0.39 # Any saturation attempts will use folding labels... % 0.19/0.39 # 344 beginning clauses after preprocessing and clausification % 0.19/0.39 # Creating start rules for all 344 conjectures. % 0.19/0.39 # There are 344 start rule candidates: % 0.19/0.39 # Found 0 unit axioms. % 0.19/0.39 # Unsuccessfully attempted saturation on 1 start tableaux, moving on. % 0.19/0.39 # 344 start rule tableaux created. % 0.19/0.39 # 344 extension rule candidate clauses % 0.19/0.39 # 0 unit axiom clauses % 0.19/0.39 % 0.19/0.39 # Requested 8, 32 cores available to the main process. % 66.46/8.79 # 4675 Satisfiable branch % 66.46/8.80 # Satisfiable branch found. % 66.46/8.80 # There were 9 total branch saturation attempts. % 66.46/8.80 # There were 0 of these attempts blocked. % 66.46/8.80 # There were 0 deferred branch saturation attempts. % 66.46/8.80 # There were 0 free duplicated saturations. % 66.46/8.80 # There were 2 total successful branch saturations. % 66.46/8.80 # There were 2 successful branch saturations in interreduction. % 66.46/8.80 # There were 0 successful branch saturations on the branch. % 66.46/8.80 # There were 0 successful branch saturations after the branch. % 66.46/8.80 # SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 66.46/8.80 # SZS output start for /export/starexec/sandbox/benchmark/theBenchmark.p % 66.46/8.80 # Begin clausification derivation % 66.46/8.80 % 66.46/8.80 # End clausification derivation % 66.46/8.80 # Begin listing active clauses obtained from FOF to CNF conversion % 66.46/8.80 cnf(i_0_345, negated_conjecture, (ndr1_0|~hskp70)). % 66.46/8.80 cnf(i_0_346, negated_conjecture, (ndr1_0|~hskp69)). % 66.46/8.80 cnf(i_0_347, negated_conjecture, (ndr1_0|~hskp68)). % 66.46/8.80 cnf(i_0_348, negated_conjecture, (ndr1_0|~hskp67)). % 66.46/8.80 cnf(i_0_349, negated_conjecture, (ndr1_0|~hskp66)). % 66.46/8.80 cnf(i_0_350, negated_conjecture, (ndr1_0|~hskp65)). % 66.46/8.80 cnf(i_0_351, negated_conjecture, (ndr1_0|~hskp64)). % 66.46/8.80 cnf(i_0_352, negated_conjecture, (ndr1_0|~hskp63)). % 66.46/8.80 cnf(i_0_353, negated_conjecture, (ndr1_0|~hskp62)). % 66.46/8.80 cnf(i_0_354, negated_conjecture, (ndr1_0|~hskp61)). % 66.46/8.80 cnf(i_0_355, negated_conjecture, (ndr1_0|~hskp60)). % 66.46/8.80 cnf(i_0_356, negated_conjecture, (ndr1_0|~hskp59)). % 66.46/8.80 cnf(i_0_357, negated_conjecture, (ndr1_0|~hskp58)). % 66.46/8.80 cnf(i_0_358, negated_conjecture, (ndr1_0|~hskp57)). % 66.46/8.80 cnf(i_0_359, negated_conjecture, (ndr1_0|~hskp56)). % 66.46/8.80 cnf(i_0_360, negated_conjecture, (ndr1_0|~hskp55)). % 66.46/8.80 cnf(i_0_361, negated_conjecture, (ndr1_0|~hskp54)). % 66.46/8.80 cnf(i_0_362, negated_conjecture, (ndr1_0|~hskp53)). % 66.46/8.80 cnf(i_0_363, negated_conjecture, (ndr1_0|~hskp52)). % 66.46/8.80 cnf(i_0_364, negated_conjecture, (ndr1_0|~hskp51)). % 66.46/8.80 cnf(i_0_365, negated_conjecture, (ndr1_0|~hskp50)). % 66.46/8.80 cnf(i_0_366, negated_conjecture, (ndr1_0|~hskp49)). % 66.46/8.80 cnf(i_0_367, negated_conjecture, (ndr1_0|~hskp48)). % 66.46/8.80 cnf(i_0_368, negated_conjecture, (ndr1_0|~hskp47)). % 66.46/8.80 cnf(i_0_369, negated_conjecture, (ndr1_0|~hskp46)). % 66.46/8.80 cnf(i_0_370, negated_conjecture, (ndr1_0|~hskp45)). % 66.46/8.80 cnf(i_0_371, negated_conjecture, (ndr1_0|~hskp44)). % 66.46/8.80 cnf(i_0_372, negated_conjecture, (ndr1_0|~hskp43)). % 66.46/8.80 cnf(i_0_373, negated_conjecture, (ndr1_0|~hskp42)). % 66.46/8.80 cnf(i_0_374, negated_conjecture, (ndr1_0|~hskp41)). % 66.46/8.80 cnf(i_0_375, negated_conjecture, (ndr1_0|~hskp40)). % 66.46/8.80 cnf(i_0_376, negated_conjecture, (ndr1_0|~hskp39)). % 66.46/8.80 cnf(i_0_377, negated_conjecture, (ndr1_0|~hskp38)). % 66.46/8.80 cnf(i_0_378, negated_conjecture, (ndr1_0|~hskp37)). % 66.46/8.80 cnf(i_0_379, negated_conjecture, (ndr1_0|~hskp36)). % 66.46/8.80 cnf(i_0_380, negated_conjecture, (ndr1_0|~hskp35)). % 66.46/8.80 cnf(i_0_381, negated_conjecture, (ndr1_0|~hskp34)). % 66.46/8.80 cnf(i_0_382, negated_conjecture, (ndr1_0|~hskp33)). % 66.46/8.80 cnf(i_0_383, negated_conjecture, (ndr1_0|~hskp32)). % 66.46/8.80 cnf(i_0_384, negated_conjecture, (ndr1_0|~hskp31)). % 66.46/8.80 cnf(i_0_385, negated_conjecture, (ndr1_0|~hskp30)). % 66.46/8.80 cnf(i_0_386, negated_conjecture, (ndr1_0|~hskp29)). % 66.46/8.80 cnf(i_0_387, negated_conjecture, (ndr1_0|~hskp28)). % 66.46/8.80 cnf(i_0_388, negated_conjecture, (ndr1_0|~hskp27)). % 66.46/8.80 cnf(i_0_389, negated_conjecture, (ndr1_0|~hskp26)). % 66.46/8.80 cnf(i_0_390, negated_conjecture, (ndr1_0|~hskp25)). % 66.46/8.80 cnf(i_0_391, negated_conjecture, (ndr1_0|~hskp24)). % 66.46/8.80 cnf(i_0_392, negated_conjecture, (ndr1_0|~hskp23)). % 66.46/8.80 cnf(i_0_393, negated_conjecture, (ndr1_0|~hskp22)). % 66.46/8.80 cnf(i_0_394, negated_conjecture, (ndr1_0|~hskp21)). % 66.46/8.80 cnf(i_0_395, negated_conjecture, (ndr1_0|~hskp20)). % 66.46/8.80 cnf(i_0_396, negated_conjecture, (ndr1_0|~hskp19)). % 66.46/8.80 cnf(i_0_397, negated_conjecture, (ndr1_0|~hskp18)). % 66.46/8.80 cnf(i_0_398, negated_conjecture, (ndr1_0|~hskp17)). % 66.46/8.80 cnf(i_0_399, negated_conjecture, (ndr1_0|~hskp16)). % 66.46/8.80 cnf(i_0_400, negated_conjecture, (ndr1_0|~hskp15)). % 66.46/8.80 cnf(i_0_401, negated_conjecture, (ndr1_0|~hskp14)). % 66.46/8.80 cnf(i_0_402, negated_conjecture, (ndr1_0|~hskp13)). % 66.46/8.80 cnf(i_0_403, negated_conjecture, (ndr1_0|~hskp12)). % 66.46/8.80 cnf(i_0_404, negated_conjecture, (ndr1_0|~hskp11)). % 66.46/8.80 cnf(i_0_405, negated_conjecture, (ndr1_0|~hskp10)). % 66.46/8.80 cnf(i_0_406, negated_conjecture, (ndr1_0|~hskp9)). % 66.46/8.80 cnf(i_0_407, negated_conjecture, (ndr1_0|~hskp8)). % 66.46/8.80 cnf(i_0_408, negated_conjecture, (ndr1_0|~hskp7)). % 66.46/8.80 cnf(i_0_409, negated_conjecture, (ndr1_0|~hskp6)). % 66.46/8.80 cnf(i_0_410, negated_conjecture, (ndr1_0|~hskp5)). % 66.46/8.80 cnf(i_0_411, negated_conjecture, (ndr1_0|~hskp4)). % 66.46/8.80 cnf(i_0_412, negated_conjecture, (ndr1_0|~hskp3)). % 66.46/8.80 cnf(i_0_413, negated_conjecture, (ndr1_0|~hskp2)). % 66.46/8.80 cnf(i_0_414, negated_conjecture, (ndr1_0|~hskp1)). % 66.46/8.80 cnf(i_0_415, negated_conjecture, (ndr1_0|~hskp0)). % 66.46/8.80 cnf(i_0_423, negated_conjecture, (hskp69|hskp68|hskp21)). % 66.46/8.80 cnf(i_0_421, negated_conjecture, (hskp59|hskp58|hskp23)). % 66.46/8.80 cnf(i_0_420, negated_conjecture, (hskp57|hskp56|hskp55)). % 66.46/8.80 cnf(i_0_418, negated_conjecture, (hskp53|hskp18|hskp17)). % 66.46/8.80 cnf(i_0_417, negated_conjecture, (hskp50|hskp49|hskp48)). % 66.46/8.80 cnf(i_0_422, negated_conjecture, (hskp49|hskp26|hskp6)). % 66.46/8.80 cnf(i_0_419, negated_conjecture, (hskp47|hskp41|hskp19)). % 66.46/8.80 cnf(i_0_416, negated_conjecture, (hskp45|hskp38|hskp13)). % 66.46/8.80 cnf(i_0_424, negated_conjecture, (c2_1(a2078)|~hskp70)). % 66.46/8.80 cnf(i_0_433, negated_conjecture, (c2_1(a2067)|~hskp66)). % 66.46/8.80 cnf(i_0_438, negated_conjecture, (c2_1(a2059)|~hskp63)). % 66.46/8.80 cnf(i_0_443, negated_conjecture, (c2_1(a2054)|~hskp61)). % 66.46/8.80 cnf(i_0_448, negated_conjecture, (c2_1(a2052)|~hskp59)). % 66.46/8.80 cnf(i_0_455, negated_conjecture, (c2_1(a2046)|~hskp55)). % 66.46/8.80 cnf(i_0_456, negated_conjecture, (c2_1(a2037)|~hskp54)). % 66.46/8.80 cnf(i_0_458, negated_conjecture, (c2_1(a2035)|~hskp53)). % 66.46/8.80 cnf(i_0_460, negated_conjecture, (c2_1(a2033)|~hskp52)). % 66.46/8.80 cnf(i_0_461, negated_conjecture, (c2_1(a2030)|~hskp51)). % 66.46/8.80 cnf(i_0_464, negated_conjecture, (c2_1(a2029)|~hskp50)). % 66.46/8.80 cnf(i_0_470, negated_conjecture, (c2_1(a2026)|~hskp47)). % 66.46/8.80 cnf(i_0_474, negated_conjecture, (c2_1(a2022)|~hskp45)). % 66.46/8.80 cnf(i_0_476, negated_conjecture, (c2_1(a2018)|~hskp44)). % 66.46/8.80 cnf(i_0_478, negated_conjecture, (c2_1(a2017)|~hskp43)). % 66.46/8.80 cnf(i_0_480, negated_conjecture, (c2_1(a2010)|~hskp42)). % 66.46/8.80 cnf(i_0_486, negated_conjecture, (c2_1(a2004)|~hskp39)). % 66.46/8.80 cnf(i_0_492, negated_conjecture, (c2_1(a1996)|~hskp35)). % 66.46/8.80 cnf(i_0_497, negated_conjecture, (c2_1(a1993)|~hskp33)). % 66.46/8.80 cnf(i_0_501, negated_conjecture, (c2_1(a2079)|~hskp29)). % 66.46/8.80 cnf(i_0_503, negated_conjecture, (c2_1(a2069)|~hskp28)). % 66.46/8.80 cnf(i_0_507, negated_conjecture, (c2_1(a2065)|~hskp26)). % 66.46/8.80 cnf(i_0_508, negated_conjecture, (c2_1(a2057)|~hskp24)). % 66.46/8.80 cnf(i_0_509, negated_conjecture, (c2_1(a2045)|~hskp22)). % 66.46/8.80 cnf(i_0_518, negated_conjecture, (c2_1(a2023)|~hskp14)). % 66.46/8.80 cnf(i_0_522, negated_conjecture, (c2_1(a2016)|~hskp11)). % 66.46/8.80 cnf(i_0_527, negated_conjecture, (c2_1(a2006)|~hskp5)). % 66.46/8.80 cnf(i_0_425, negated_conjecture, (c0_1(a2078)|~hskp70)). % 66.46/8.80 cnf(i_0_427, negated_conjecture, (c0_1(a2074)|~hskp69)). % 66.46/8.80 cnf(i_0_429, negated_conjecture, (c0_1(a2073)|~hskp68)). % 66.46/8.80 cnf(i_0_431, negated_conjecture, (c0_1(a2067)|~hskp66)). % 66.46/8.80 cnf(i_0_434, negated_conjecture, (c0_1(a2063)|~hskp65)). % 66.46/8.80 cnf(i_0_445, negated_conjecture, (c0_1(a2053)|~hskp60)). % 66.46/8.80 cnf(i_0_447, negated_conjecture, (c0_1(a2052)|~hskp59)). % 66.46/8.80 cnf(i_0_450, negated_conjecture, (c0_1(a2048)|~hskp57)). % 66.46/8.80 cnf(i_0_452, negated_conjecture, (c0_1(a2047)|~hskp56)). % 66.46/8.80 cnf(i_0_453, negated_conjecture, (c0_1(a2046)|~hskp55)). % 66.46/8.80 cnf(i_0_465, negated_conjecture, (c0_1(a2028)|~hskp49)). % 66.46/8.80 cnf(i_0_469, negated_conjecture, (c0_1(a2027)|~hskp48)). % 66.46/8.80 cnf(i_0_471, negated_conjecture, (c0_1(a2026)|~hskp47)). % 66.46/8.80 cnf(i_0_473, negated_conjecture, (c0_1(a2025)|~hskp46)). % 66.46/8.80 cnf(i_0_477, negated_conjecture, (c0_1(a2018)|~hskp44)). % 66.46/8.80 cnf(i_0_483, negated_conjecture, (c0_1(a2007)|~hskp41)). % 66.46/8.80 cnf(i_0_484, negated_conjecture, (c0_1(a2005)|~hskp40)). % 66.46/8.80 cnf(i_0_485, negated_conjecture, (c0_1(a2004)|~hskp39)). % 66.46/8.80 cnf(i_0_494, negated_conjecture, (c0_1(a1996)|~hskp35)). % 66.46/8.80 cnf(i_0_495, negated_conjecture, (c0_1(a1995)|~hskp34)). % 66.46/8.80 cnf(i_0_499, negated_conjecture, (c0_1(a1993)|~hskp33)). % 66.46/8.80 cnf(i_0_504, negated_conjecture, (c0_1(a2068)|~hskp27)). % 66.46/8.80 cnf(i_0_514, negated_conjecture, (c0_1(a2038)|~hskp19)). % 66.46/8.80 cnf(i_0_516, negated_conjecture, (c0_1(a2036)|~hskp18)). % 66.46/8.80 cnf(i_0_517, negated_conjecture, (c0_1(a2032)|~hskp16)). % 66.46/8.80 cnf(i_0_519, negated_conjecture, (c0_1(a2023)|~hskp14)). % 66.46/8.80 cnf(i_0_521, negated_conjecture, (c0_1(a2016)|~hskp11)). % 66.46/8.80 cnf(i_0_525, negated_conjecture, (c0_1(a2011)|~hskp7)). % 66.46/8.80 cnf(i_0_530, negated_conjecture, (c0_1(a1998)|~hskp1)). % 66.46/8.80 cnf(i_0_532, negated_conjecture, (c0_1(a1994)|~hskp0)). % 66.46/8.80 cnf(i_0_426, negated_conjecture, (c3_1(a2078)|~hskp70)). % 66.46/8.80 cnf(i_0_430, negated_conjecture, (c3_1(a2070)|~hskp67)). % 66.46/8.80 cnf(i_0_432, negated_conjecture, (c3_1(a2067)|~hskp66)). % 66.46/8.80 cnf(i_0_436, negated_conjecture, (c3_1(a2061)|~hskp64)). % 66.46/8.80 cnf(i_0_441, negated_conjecture, (c3_1(a2058)|~hskp62)). % 66.46/8.80 cnf(i_0_444, negated_conjecture, (c3_1(a2054)|~hskp61)). % 66.46/8.80 cnf(i_0_449, negated_conjecture, (c3_1(a2051)|~hskp58)). % 66.46/8.80 cnf(i_0_451, negated_conjecture, (c3_1(a2047)|~hskp56)). % 66.46/8.80 cnf(i_0_457, negated_conjecture, (c3_1(a2037)|~hskp54)). % 66.46/8.80 cnf(i_0_466, negated_conjecture, (c3_1(a2028)|~hskp49)). % 66.46/8.80 cnf(i_0_468, negated_conjecture, (c3_1(a2027)|~hskp48)). % 66.46/8.80 cnf(i_0_472, negated_conjecture, (c3_1(a2025)|~hskp46)). % 66.46/8.80 cnf(i_0_475, negated_conjecture, (c3_1(a2022)|~hskp45)). % 66.46/8.80 cnf(i_0_479, negated_conjecture, (c3_1(a2010)|~hskp42)). % 66.46/8.80 cnf(i_0_481, negated_conjecture, (c3_1(a2007)|~hskp41)). % 66.46/8.80 cnf(i_0_488, negated_conjecture, (c3_1(a2003)|~hskp38)). % 66.46/8.80 cnf(i_0_489, negated_conjecture, (c3_1(a2002)|~hskp37)). % 66.46/8.80 cnf(i_0_493, negated_conjecture, (c3_1(a1996)|~hskp35)). % 66.46/8.80 cnf(i_0_500, negated_conjecture, (c3_1(a2079)|~hskp29)). % 66.46/8.80 cnf(i_0_506, negated_conjecture, (c3_1(a2065)|~hskp26)). % 66.46/8.80 cnf(i_0_510, negated_conjecture, (c3_1(a2044)|~hskp21)). % 66.46/8.80 cnf(i_0_512, negated_conjecture, (c3_1(a2041)|~hskp20)). % 66.46/8.80 cnf(i_0_515, negated_conjecture, (c3_1(a2036)|~hskp18)). % 66.46/8.80 cnf(i_0_523, negated_conjecture, (c3_1(a2015)|~hskp10)). % 66.46/8.80 cnf(i_0_526, negated_conjecture, (c3_1(a2009)|~hskp6)). % 66.46/8.80 cnf(i_0_531, negated_conjecture, (c3_1(a1998)|~hskp1)). % 66.46/8.80 cnf(i_0_428, negated_conjecture, (c1_1(a2073)|~hskp68)). % 66.46/8.80 cnf(i_0_435, negated_conjecture, (c1_1(a2063)|~hskp65)). % 66.46/8.80 cnf(i_0_437, negated_conjecture, (c1_1(a2061)|~hskp64)). % 66.46/8.80 cnf(i_0_439, negated_conjecture, (c1_1(a2059)|~hskp63)). % 66.46/8.80 cnf(i_0_440, negated_conjecture, (c1_1(a2058)|~hskp62)). % 66.46/8.80 cnf(i_0_442, negated_conjecture, (c1_1(a2054)|~hskp61)). % 66.46/8.80 cnf(i_0_446, negated_conjecture, (c1_1(a2053)|~hskp60)). % 66.46/8.80 cnf(i_0_454, negated_conjecture, (c1_1(a2046)|~hskp55)). % 66.46/8.80 cnf(i_0_459, negated_conjecture, (c1_1(a2035)|~hskp53)). % 66.46/8.80 cnf(i_0_462, negated_conjecture, (c1_1(a2030)|~hskp51)). % 66.46/8.80 cnf(i_0_463, negated_conjecture, (c1_1(a2029)|~hskp50)). % 66.46/8.80 cnf(i_0_467, negated_conjecture, (c1_1(a2027)|~hskp48)). % 66.46/8.80 cnf(i_0_482, negated_conjecture, (c1_1(a2007)|~hskp41)). % 66.46/8.80 cnf(i_0_487, negated_conjecture, (c1_1(a2004)|~hskp39)). % 66.46/8.80 cnf(i_0_490, negated_conjecture, (c1_1(a2002)|~hskp37)). % 66.46/8.80 cnf(i_0_491, negated_conjecture, (c1_1(a1997)|~hskp36)). % 66.46/8.80 cnf(i_0_496, negated_conjecture, (c1_1(a1995)|~hskp34)). % 66.46/8.80 cnf(i_0_498, negated_conjecture, (c1_1(a1993)|~hskp33)). % 66.46/8.80 cnf(i_0_502, negated_conjecture, (c1_1(a2069)|~hskp28)). % 66.46/8.80 cnf(i_0_505, negated_conjecture, (c1_1(a2068)|~hskp27)). % 66.46/8.80 cnf(i_0_511, negated_conjecture, (c1_1(a2041)|~hskp20)). % 66.46/8.80 cnf(i_0_513, negated_conjecture, (c1_1(a2038)|~hskp19)). % 66.46/8.80 cnf(i_0_520, negated_conjecture, (c1_1(a2020)|~hskp13)). % 66.46/8.80 cnf(i_0_524, negated_conjecture, (c1_1(a2015)|~hskp10)). % 66.46/8.80 cnf(i_0_528, negated_conjecture, (c1_1(a2000)|~hskp3)). % 66.46/8.80 cnf(i_0_529, negated_conjecture, (c1_1(a1999)|~hskp2)). % 66.46/8.80 cnf(i_0_533, negated_conjecture, (~hskp69|~c2_1(a2074))). % 66.46/8.80 cnf(i_0_534, negated_conjecture, (~hskp69|~c3_1(a2074))). % 66.46/8.80 cnf(i_0_535, negated_conjecture, (~hskp68|~c2_1(a2073))). % 66.46/8.80 cnf(i_0_537, negated_conjecture, (~hskp67|~c0_1(a2070))). % 66.46/8.80 cnf(i_0_536, negated_conjecture, (~hskp67|~c1_1(a2070))). % 66.46/8.80 cnf(i_0_538, negated_conjecture, (~hskp65|~c3_1(a2063))). % 66.46/8.80 cnf(i_0_539, negated_conjecture, (~hskp64|~c2_1(a2061))). % 66.46/8.80 cnf(i_0_540, negated_conjecture, (~hskp63|~c3_1(a2059))). % 66.46/8.80 cnf(i_0_541, negated_conjecture, (~hskp62|~c2_1(a2058))). % 66.46/8.80 cnf(i_0_542, negated_conjecture, (~hskp60|~c2_1(a2053))). % 66.46/8.80 cnf(i_0_543, negated_conjecture, (~hskp59|~c1_1(a2052))). % 66.46/8.80 cnf(i_0_544, negated_conjecture, (~hskp58|~c2_1(a2051))). % 66.46/8.80 cnf(i_0_545, negated_conjecture, (~hskp58|~c1_1(a2051))). % 66.46/8.80 cnf(i_0_546, negated_conjecture, (~hskp57|~c3_1(a2048))). % 66.46/8.80 cnf(i_0_547, negated_conjecture, (~hskp57|~c1_1(a2048))). % 66.46/8.80 cnf(i_0_548, negated_conjecture, (~hskp56|~c2_1(a2047))). % 66.46/8.80 cnf(i_0_549, negated_conjecture, (~hskp54|~c0_1(a2037))). % 66.46/8.80 cnf(i_0_550, negated_conjecture, (~hskp53|~c0_1(a2035))). % 66.46/8.80 cnf(i_0_551, negated_conjecture, (~hskp52|~c3_1(a2033))). % 66.46/8.80 cnf(i_0_552, negated_conjecture, (~hskp52|~c1_1(a2033))). % 66.46/8.80 cnf(i_0_553, negated_conjecture, (~hskp51|~c0_1(a2030))). % 66.46/8.80 cnf(i_0_554, negated_conjecture, (~hskp50|~c3_1(a2029))). % 66.46/8.80 cnf(i_0_555, negated_conjecture, (~hskp49|~c1_1(a2028))). % 66.46/8.80 cnf(i_0_556, negated_conjecture, (~hskp47|~c3_1(a2026))). % 66.46/8.80 cnf(i_0_557, negated_conjecture, (~hskp46|~c2_1(a2025))). % 66.46/8.80 cnf(i_0_558, negated_conjecture, (~hskp45|~c0_1(a2022))). % 66.46/8.80 cnf(i_0_559, negated_conjecture, (~hskp44|~c1_1(a2018))). % 66.46/8.80 cnf(i_0_561, negated_conjecture, (~hskp43|~c0_1(a2017))). % 66.46/8.80 cnf(i_0_560, negated_conjecture, (~hskp43|~c1_1(a2017))). % 66.46/8.80 cnf(i_0_562, negated_conjecture, (~hskp42|~c0_1(a2010))). % 66.46/8.80 cnf(i_0_564, negated_conjecture, (~hskp40|~c3_1(a2005))). % 66.46/8.80 cnf(i_0_563, negated_conjecture, (~hskp40|~c1_1(a2005))). % 66.46/8.80 cnf(i_0_566, negated_conjecture, (~hskp38|~c2_1(a2003))). % 66.46/8.80 cnf(i_0_565, negated_conjecture, (~hskp38|~c1_1(a2003))). % 66.46/8.80 cnf(i_0_567, negated_conjecture, (~hskp37|~c0_1(a2002))). % 66.46/8.80 cnf(i_0_568, negated_conjecture, (~hskp36|~c2_1(a1997))). % 66.46/8.80 cnf(i_0_569, negated_conjecture, (~hskp36|~c3_1(a1997))). % 66.46/8.80 cnf(i_0_570, negated_conjecture, (~hskp34|~c3_1(a1995))). % 66.46/8.80 cnf(i_0_571, negated_conjecture, (~hskp32|~c2_1(a2083))). % 66.46/8.80 cnf(i_0_572, negated_conjecture, (~hskp32|~c3_1(a2083))). % 66.46/8.80 cnf(i_0_573, negated_conjecture, (~hskp32|~c1_1(a2083))). % 66.46/8.80 cnf(i_0_576, negated_conjecture, (~hskp31|~c2_1(a2081))). % 66.46/8.80 cnf(i_0_575, negated_conjecture, (~hskp31|~c3_1(a2081))). % 66.46/8.80 cnf(i_0_574, negated_conjecture, (~hskp31|~c1_1(a2081))). % 66.46/8.80 cnf(i_0_579, negated_conjecture, (~hskp30|~c2_1(a2080))). % 66.46/8.80 cnf(i_0_578, negated_conjecture, (~hskp30|~c0_1(a2080))). % 66.46/8.80 cnf(i_0_577, negated_conjecture, (~hskp30|~c1_1(a2080))). % 66.46/8.80 cnf(i_0_580, negated_conjecture, (~hskp29|~c1_1(a2079))). % 66.46/8.80 cnf(i_0_581, negated_conjecture, (~hskp28|~c0_1(a2069))). % 66.46/8.80 cnf(i_0_582, negated_conjecture, (~hskp27|~c2_1(a2068))). % 66.46/8.80 cnf(i_0_583, negated_conjecture, (~hskp26|~c0_1(a2065))). % 66.46/8.80 cnf(i_0_586, negated_conjecture, (~hskp25|~c2_1(a2062))). % 66.46/8.80 cnf(i_0_584, negated_conjecture, (~hskp25|~c3_1(a2062))). % 66.46/8.80 cnf(i_0_585, negated_conjecture, (~hskp25|~c1_1(a2062))). % 66.46/8.80 cnf(i_0_588, negated_conjecture, (~hskp24|~c0_1(a2057))). % 66.46/8.80 cnf(i_0_587, negated_conjecture, (~hskp24|~c3_1(a2057))). % 66.46/8.80 cnf(i_0_589, negated_conjecture, (~hskp23|~c2_1(a2050))). % 66.46/8.80 cnf(i_0_590, negated_conjecture, (~hskp23|~c0_1(a2050))). % 66.46/8.80 cnf(i_0_591, negated_conjecture, (~hskp23|~c3_1(a2050))). % 66.46/8.80 cnf(i_0_592, negated_conjecture, (~hskp22|~c0_1(a2045))). % 66.46/8.80 cnf(i_0_593, negated_conjecture, (~hskp22|~c3_1(a2045))). % 66.46/8.80 cnf(i_0_595, negated_conjecture, (~hskp21|~c0_1(a2044))). % 66.46/8.80 cnf(i_0_594, negated_conjecture, (~hskp21|~c1_1(a2044))). % 66.46/8.80 cnf(i_0_596, negated_conjecture, (~hskp20|~c0_1(a2041))). % 66.46/8.80 cnf(i_0_597, negated_conjecture, (~hskp19|~c3_1(a2038))). % 66.46/8.80 cnf(i_0_598, negated_conjecture, (~hskp18|~c1_1(a2036))). % 66.46/8.80 cnf(i_0_599, negated_conjecture, (~hskp17|~c2_1(a2034))). % 66.46/8.80 cnf(i_0_601, negated_conjecture, (~hskp17|~c0_1(a2034))). % 66.46/8.80 cnf(i_0_600, negated_conjecture, (~hskp17|~c1_1(a2034))). % 66.46/8.80 cnf(i_0_603, negated_conjecture, (~hskp16|~c2_1(a2032))). % 66.46/8.80 cnf(i_0_602, negated_conjecture, (~hskp16|~c1_1(a2032))). % 66.46/8.80 cnf(i_0_604, negated_conjecture, (~hskp15|~c2_1(a2031))). % 66.46/8.80 cnf(i_0_606, negated_conjecture, (~hskp15|~c0_1(a2031))). % 66.46/8.80 cnf(i_0_605, negated_conjecture, (~hskp15|~c3_1(a2031))). % 66.46/8.80 cnf(i_0_607, negated_conjecture, (~hskp14|~c3_1(a2023))). % 66.46/8.80 cnf(i_0_609, negated_conjecture, (~hskp13|~c2_1(a2020))). % 66.46/8.80 cnf(i_0_608, negated_conjecture, (~hskp13|~c3_1(a2020))). % 66.46/8.80 cnf(i_0_611, negated_conjecture, (~hskp12|~c2_1(a2019))). % 66.46/8.80 cnf(i_0_612, negated_conjecture, (~hskp12|~c0_1(a2019))). % 66.46/8.80 cnf(i_0_610, negated_conjecture, (~hskp12|~c1_1(a2019))). % 66.46/8.80 cnf(i_0_613, negated_conjecture, (~hskp11|~c1_1(a2016))). % 66.46/8.80 cnf(i_0_614, negated_conjecture, (~hskp10|~c0_1(a2015))). % 66.46/8.80 cnf(i_0_616, negated_conjecture, (~hskp9|~c2_1(a2014))). % 66.46/8.80 cnf(i_0_617, negated_conjecture, (~hskp9|~c0_1(a2014))). % 66.46/8.80 cnf(i_0_615, negated_conjecture, (~hskp9|~c3_1(a2014))). % 66.46/8.80 cnf(i_0_619, negated_conjecture, (~hskp8|~c0_1(a2013))). % 66.46/8.80 cnf(i_0_618, negated_conjecture, (~hskp8|~c3_1(a2013))). % 66.46/8.80 cnf(i_0_620, negated_conjecture, (~hskp8|~c1_1(a2013))). % 66.46/8.80 cnf(i_0_622, negated_conjecture, (~hskp7|~c2_1(a2011))). % 66.46/8.80 cnf(i_0_621, negated_conjecture, (~hskp7|~c3_1(a2011))). % 66.46/8.80 cnf(i_0_623, negated_conjecture, (~hskp6|~c0_1(a2009))). % 66.46/8.80 cnf(i_0_624, negated_conjecture, (~hskp6|~c1_1(a2009))). % 66.46/8.80 cnf(i_0_626, negated_conjecture, (~hskp5|~c0_1(a2006))). % 66.46/8.80 cnf(i_0_625, negated_conjecture, (~hskp5|~c1_1(a2006))). % 66.46/8.80 cnf(i_0_628, negated_conjecture, (~hskp4|~c2_1(a2001))). % 66.46/8.80 cnf(i_0_627, negated_conjecture, (~hskp4|~c3_1(a2001))). % 66.46/8.80 cnf(i_0_629, negated_conjecture, (~hskp4|~c1_1(a2001))). % 66.46/8.80 cnf(i_0_631, negated_conjecture, (~hskp3|~c0_1(a2000))). % 66.46/8.80 cnf(i_0_630, negated_conjecture, (~hskp3|~c3_1(a2000))). % 66.46/8.80 cnf(i_0_632, negated_conjecture, (~hskp2|~c2_1(a1999))). % 66.46/8.80 cnf(i_0_633, negated_conjecture, (~hskp2|~c3_1(a1999))). % 66.46/8.80 cnf(i_0_634, negated_conjecture, (~hskp1|~c1_1(a1998))). % 66.46/8.80 cnf(i_0_636, negated_conjecture, (~hskp0|~c3_1(a1994))). % 66.46/8.80 cnf(i_0_635, negated_conjecture, (~hskp0|~c1_1(a1994))). % 66.46/8.80 cnf(i_0_638, negated_conjecture, (hskp64|hskp2|c2_1(X1)|c0_1(X1)|c3_1(X1)|~ndr1_0)). % 66.46/8.80 cnf(i_0_639, negated_conjecture, (hskp47|hskp31|c0_1(X1)|c3_1(X1)|c1_1(X1)|~ndr1_0)). % 66.46/8.80 cnf(i_0_637, negated_conjecture, (hskp41|hskp37|c2_1(X1)|c3_1(X1)|c1_1(X1)|~ndr1_0)). % 66.46/8.80 cnf(i_0_648, negated_conjecture, (hskp70|hskp29|c0_1(X1)|c1_1(X1)|~ndr1_0|~c2_1(X1))). % 66.46/8.80 cnf(i_0_647, negated_conjecture, (hskp65|hskp25|c2_1(X1)|c0_1(X1)|~ndr1_0|~c3_1(X1))). % 66.46/8.80 cnf(i_0_646, negated_conjecture, (hskp63|hskp62|c0_1(X1)|c1_1(X1)|~ndr1_0|~c3_1(X1))). % 66.46/8.80 cnf(i_0_645, negated_conjecture, (hskp61|hskp60|c0_1(X1)|c3_1(X1)|~ndr1_0|~c2_1(X1))). % 66.46/8.80 cnf(i_0_644, negated_conjecture, (hskp52|hskp16|c2_1(X1)|c1_1(X1)|~ndr1_0|~c0_1(X1))). % 66.46/8.80 cnf(i_0_643, negated_conjecture, (hskp51|hskp15|c3_1(X1)|c1_1(X1)|~ndr1_0|~c0_1(X1))). % 66.46/8.80 cnf(i_0_642, negated_conjecture, (hskp40|hskp5|c0_1(X1)|c3_1(X1)|~ndr1_0|~c2_1(X1))). % 66.46/8.80 cnf(i_0_641, negated_conjecture, (hskp37|hskp4|c0_1(X1)|c1_1(X1)|~ndr1_0|~c2_1(X1))). % 66.46/8.80 cnf(i_0_640, negated_conjecture, (hskp35|hskp34|c2_1(X1)|c3_1(X1)|~ndr1_0|~c1_1(X1))). % 66.46/8.80 cnf(i_0_655, negated_conjecture, (hskp67|hskp10|c2_1(X1)|~ndr1_0|~c0_1(X1)|~c1_1(X1))). % 66.46/8.80 cnf(i_0_654, negated_conjecture, (hskp59|hskp33|c0_1(X1)|~ndr1_0|~c2_1(X1)|~c1_1(X1))). % 66.46/8.80 cnf(i_0_656, negated_conjecture, (hskp54|hskp48|c2_1(X1)|~ndr1_0|~c0_1(X1)|~c3_1(X1))). % 66.46/8.80 cnf(i_0_652, negated_conjecture, (hskp48|hskp43|c0_1(X1)|~ndr1_0|~c2_1(X1)|~c1_1(X1))). % 66.46/8.80 cnf(i_0_651, negated_conjecture, (hskp46|hskp5|c2_1(X1)|~ndr1_0|~c3_1(X1)|~c1_1(X1))). % 66.46/8.80 cnf(i_0_650, negated_conjecture, (hskp44|hskp12|c2_1(X1)|~ndr1_0|~c0_1(X1)|~c3_1(X1))). % 66.46/8.80 cnf(i_0_649, negated_conjecture, (hskp36|hskp1|c3_1(X1)|~ndr1_0|~c2_1(X1)|~c0_1(X1))). % 66.46/8.80 cnf(i_0_657, negated_conjecture, (hskp32|hskp10|c3_1(X1)|~ndr1_0|~c2_1(X1)|~c0_1(X1))). % 66.46/8.80 cnf(i_0_653, negated_conjecture, (hskp22|hskp21|c0_1(X1)|~ndr1_0|~c2_1(X1)|~c1_1(X1))). % 66.46/8.80 cnf(i_0_658, negated_conjecture, (hskp8|hskp2|~ndr1_0|~c0_1(X1)|~c3_1(X1)|~c1_1(X1))). % 66.46/8.80 cnf(i_0_661, negated_conjecture, (hskp20|c2_1(X1)|c0_1(X2)|c3_1(X2)|c3_1(X1)|c1_1(X2)|~ndr1_0|~c1_1(X1))). % 66.46/8.80 cnf(i_0_660, negated_conjecture, (hskp14|c2_1(X2)|c2_1(X1)|c0_1(X2)|c3_1(X1)|c1_1(X2)|~ndr1_0|~c0_1(X1))). % 66.46/8.80 cnf(i_0_659, negated_conjecture, (hskp7|c2_1(X2)|c0_1(X2)|c0_1(X1)|c1_1(X2)|c1_1(X1)|~ndr1_0|~c2_1(X1))). % 66.46/8.80 cnf(i_0_666, negated_conjecture, (hskp66|c2_1(X2)|c0_1(X2)|c3_1(X1)|c1_1(X2)|~ndr1_0|~c0_1(X1)|~c1_1(X1))). % 66.46/8.80 cnf(i_0_665, negated_conjecture, (hskp47|c0_1(X2)|c3_1(X2)|c3_1(X1)|c1_1(X1)|~ndr1_0|~c2_1(X2)|~c0_1(X1))). % 66.46/8.80 cnf(i_0_664, negated_conjecture, (hskp43|c2_1(X2)|c0_1(X2)|c0_1(X1)|c3_1(X1)|~ndr1_0|~c1_1(X2)|~c1_1(X1))). % 66.46/8.80 cnf(i_0_663, negated_conjecture, (hskp11|c2_1(X2)|c2_1(X1)|c0_1(X2)|c3_1(X1)|~ndr1_0|~c0_1(X1)|~c3_1(X2))). % 66.46/8.80 cnf(i_0_662, negated_conjecture, (hskp3|c0_1(X2)|c0_1(X1)|c3_1(X2)|c1_1(X2)|~ndr1_0|~c3_1(X1)|~c1_1(X1))). % 66.46/8.80 cnf(i_0_673, negated_conjecture, (hskp54|c2_1(X2)|c3_1(X1)|c1_1(X1)|~ndr1_0|~c2_1(X1)|~c0_1(X2)|~c3_1(X2))). % 66.46/8.80 cnf(i_0_670, negated_conjecture, (hskp39|c2_1(X2)|c0_1(X2)|c1_1(X1)|~ndr1_0|~c2_1(X1)|~c0_1(X1)|~c1_1(X2))). % 66.46/8.80 cnf(i_0_669, negated_conjecture, (hskp38|c2_1(X1)|c0_1(X1)|c1_1(X2)|~ndr1_0|~c0_1(X2)|~c3_1(X2)|~c1_1(X1))). % 66.46/8.80 cnf(i_0_667, negated_conjecture, (hskp33|c0_1(X2)|c1_1(X2)|c1_1(X1)|~ndr1_0|~c2_1(X2)|~c2_1(X1)|~c3_1(X1))). % 66.46/8.80 cnf(i_0_675, negated_conjecture, (hskp28|c2_1(X1)|c3_1(X2)|c1_1(X2)|~ndr1_0|~c0_1(X2)|~c0_1(X1)|~c1_1(X1))). % 66.46/8.80 cnf(i_0_674, negated_conjecture, (hskp27|c2_1(X2)|c0_1(X1)|c3_1(X2)|~ndr1_0|~c2_1(X1)|~c3_1(X1)|~c1_1(X2))). % 66.46/8.80 cnf(i_0_676, negated_conjecture, (hskp20|c0_1(X2)|c3_1(X1)|c1_1(X1)|~ndr1_0|~c2_1(X2)|~c0_1(X1)|~c1_1(X2))). % 66.46/8.80 cnf(i_0_672, negated_conjecture, (hskp9|c2_1(X1)|c0_1(X2)|c3_1(X2)|~ndr1_0|~c2_1(X2)|~c0_1(X1)|~c1_1(X1))). % 66.46/8.80 cnf(i_0_671, negated_conjecture, (hskp6|c3_1(X1)|c1_1(X2)|c1_1(X1)|~ndr1_0|~c0_1(X2)|~c0_1(X1)|~c3_1(X2))). % 66.46/8.80 cnf(i_0_668, negated_conjecture, (hskp2|c0_1(X1)|c3_1(X1)|c1_1(X2)|~ndr1_0|~c2_1(X2)|~c3_1(X2)|~c1_1(X1))). % 66.46/8.80 cnf(i_0_679, negated_conjecture, (hskp42|c2_1(X2)|c1_1(X2)|~ndr1_0|~c0_1(X1)|~c3_1(X2)|~c3_1(X1)|~c1_1(X1))). % 66.46/8.80 cnf(i_0_677, negated_conjecture, (hskp10|c2_1(X1)|c3_1(X2)|~ndr1_0|~c0_1(X2)|~c0_1(X1)|~c3_1(X1)|~c1_1(X2))). % 66.46/8.80 cnf(i_0_678, negated_conjecture, (c2_1(X1)|~ndr1_0|~c0_1(X2)|~c3_1(X2)|~c3_1(X1)|~c1_1(X2)|~c1_1(X1))). % 66.46/8.80 cnf(i_0_681, negated_conjecture, (hskp56|c0_1(X2)|~ndr1_0|~c2_1(X1)|~c0_1(X1)|~c3_1(X2)|~c3_1(X1)|~c1_1(X2))). % 66.46/8.80 cnf(i_0_680, negated_conjecture, (hskp42|c1_1(X1)|~ndr1_0|~c2_1(X2)|~c2_1(X1)|~c0_1(X2)|~c0_1(X1)|~c3_1(X2))). % 66.46/8.80 cnf(i_0_683, negated_conjecture, (hskp30|c3_1(X1)|~ndr1_0|~c0_1(X2)|~c0_1(X1)|~c3_1(X2)|~c1_1(X2)|~c1_1(X1))). % 66.46/8.80 cnf(i_0_682, negated_conjecture, (hskp24|c2_1(X1)|~ndr1_0|~c2_1(X2)|~c0_1(X2)|~c0_1(X1)|~c1_1(X2)|~c1_1(X1))). % 66.46/8.80 cnf(i_0_684, negated_conjecture, (hskp0|~ndr1_0|~c2_1(X2)|~c2_1(X1)|~c0_1(X1)|~c3_1(X2)|~c1_1(X2)|~c1_1(X1))). % 66.46/8.80 cnf(i_0_685, negated_conjecture, (c2_1(X3)|c3_1(X3)|c3_1(X2)|c1_1(X3)|c1_1(X1)|~ndr1_0|~c2_1(X2)|~c2_1(X1)|~c0_1(X1)|~c1_1(X2))). % 66.46/8.80 cnf(i_0_686, negated_conjecture, (c2_1(X1)|c0_1(X3)|c0_1(X1)|~ndr1_0|~c2_1(X3)|~c2_1(X2)|~c0_1(X2)|~c3_1(X2)|~c1_1(X3)|~c1_1(X1))). % 66.46/8.80 cnf(i_0_687, negated_conjecture, (c2_1(X1)|c0_1(X2)|c3_1(X2)|~ndr1_0|~c2_1(X3)|~c0_1(X3)|~c0_1(X1)|~c3_1(X1)|~c1_1(X3)|~c1_1(X2))). % 66.46/8.80 cnf(i_0_688, negated_conjecture, (c1_1(X3)|c1_1(X1)|~ndr1_0|~c2_1(X1)|~c0_1(X3)|~c0_1(X2)|~c0_1(X1)|~c3_1(X3)|~c3_1(X2)|~c1_1(X2))). % 66.46/8.80 # End listing active clauses. There is an equivalent clause to each of these in the clausification! % 66.46/8.80 # Begin printing tableau % 66.46/8.80 # Found 9 steps % 66.46/8.80 cnf(i_0_632, negated_conjecture, (~hskp2|~c2_1(a1999)), inference(start_rule)). % 66.46/8.80 cnf(i_0_1023937, plain, (c2_1(a1995)), inference(closure_rule, [i_0_0])). % 66.46/8.80 cnf(i_0_1023938, plain, (c0_1(a1995)), inference(closure_rule, [i_0_0])). % 66.46/8.80 cnf(i_0_1076, plain, (~hskp2), inference(extension_rule, [i_0_638])). % 66.46/8.80 cnf(i_0_1023935, plain, (hskp64), inference(extension_rule, [i_0_539])). % 66.46/8.80 cnf(i_0_1024234, plain, (~c2_1(a2061)), inference(extension_rule, [i_0_664])). % 66.46/8.80 cnf(i_0_1023939, plain, (c3_1(a1995)), inference(extension_rule, [i_0_570])). % 66.46/8.80 cnf(i_0_1146240, plain, (~hskp34), inference(extension_rule, [i_0_640])). % 66.46/8.80 cnf(i_0_1023940, plain, (~ndr1_0), inference(etableau_closure_rule, [i_0_1023940, ...])). % 66.46/8.80 # End printing tableau % 66.46/8.80 # SZS output end % 66.46/8.80 # Branches closed with saturation will be marked with an "s" % 66.46/8.81 # Child (4675) has found a proof. % 66.46/8.81 % 66.46/8.81 # Proof search is over... % 66.46/8.81 # Freeing feature tree %------------------------------------------------------------------------------