%-------------------------------------------------------------------------- % File : SYN439-1 : TPTP v2.4.1. Released v2.1.0. % Domain : Syntactic (Translated) % Problem : ALC, N=4, R=1, L=48, K=3, D=1, P=0, Index=090 % Version : Especial. % English : % Refs : [OS95] Ohlbach & Schmidt (1995), Functional Translation and S % : [WGR96] Weidenbach et al. (1996), SPASS and FLOTTER % : [HS97] Hustadt & Schmidt (1997), On Evaluating Decision Proce % : [Wei97] Weidenbach (1997), Email to G. Sutcliffe % Source : [Wei97] % Names : alc-4-1-48-3-1-090.cnf [Wei97] % Status : unsatisfiable % Rating : 0.25 v2.4.0, 0.50 v2.3.0, 0.67 v2.2.1, 1.00 v2.1.0 % Syntax : Number of clauses : 260 ( 48 non-Horn; 0 unit; 249 RR) % Number of literals : 773 ( 0 equality) % Maximal clause size : 10 ( 2 average) % Number of predicates : 58 ( 54 propositional; 0-1 arity) % Number of functors : 53 ( 53 constant; 0-0 arity) % Number of variables : 81 ( 0 singleton) % Maximal term depth : 1 ( 1 average) % Comments : These ALC problems have been translated from propositional % multi-modal K logic formulae generated according to the scheme % described in [HS97], using the optimized functional translation % described in [OS95]. The finite model property holds, the % Herbrand Universe is finite, they are decidable (the complexity % is PSPACE-complete), resolution + subsumption + condensing is a % decision procedure, and the translated formulae belong to the % (CNF-translation of the) Bernays-Schoenfinkel class [Wei97]. % : Translated from FOF using FLOTTER [WGR96]. % : tptp2X -f tptp SYN439-1.p %-------------------------------------------------------------------------- input_clause(clause1,conjecture, [-- hskp52, ++ ndr1_0]). input_clause(clause2,conjecture, [-- hskp51, ++ ndr1_0]). input_clause(clause3,conjecture, [-- hskp50, ++ ndr1_0]). input_clause(clause4,conjecture, [-- hskp49, ++ ndr1_0]). input_clause(clause5,conjecture, [-- hskp48, ++ ndr1_0]). input_clause(clause6,conjecture, [-- hskp47, ++ ndr1_0]). input_clause(clause7,conjecture, [-- hskp46, ++ ndr1_0]). input_clause(clause8,conjecture, [-- hskp45, ++ ndr1_0]). input_clause(clause9,conjecture, [-- hskp44, ++ ndr1_0]). input_clause(clause10,conjecture, [-- hskp43, ++ ndr1_0]). input_clause(clause11,conjecture, [-- hskp42, ++ ndr1_0]). input_clause(clause12,conjecture, [-- hskp41, ++ ndr1_0]). input_clause(clause13,conjecture, [-- hskp40, ++ ndr1_0]). input_clause(clause14,conjecture, [-- hskp39, ++ ndr1_0]). input_clause(clause15,conjecture, [-- hskp38, ++ ndr1_0]). input_clause(clause16,conjecture, [-- hskp37, ++ ndr1_0]). input_clause(clause17,conjecture, [-- hskp36, ++ ndr1_0]). input_clause(clause18,conjecture, [-- hskp35, ++ ndr1_0]). input_clause(clause19,conjecture, [-- hskp34, ++ ndr1_0]). input_clause(clause20,conjecture, [-- hskp33, ++ ndr1_0]). input_clause(clause21,conjecture, [-- hskp32, ++ ndr1_0]). input_clause(clause22,conjecture, [-- hskp31, ++ ndr1_0]). input_clause(clause23,conjecture, [-- hskp30, ++ ndr1_0]). input_clause(clause24,conjecture, [-- hskp29, ++ ndr1_0]). input_clause(clause25,conjecture, [-- hskp28, ++ ndr1_0]). input_clause(clause26,conjecture, [-- hskp27, ++ ndr1_0]). input_clause(clause27,conjecture, [-- hskp26, ++ ndr1_0]). input_clause(clause28,conjecture, [-- hskp25, ++ ndr1_0]). input_clause(clause29,conjecture, [-- hskp24, ++ ndr1_0]). input_clause(clause30,conjecture, [-- hskp23, ++ ndr1_0]). input_clause(clause31,conjecture, [-- hskp22, ++ ndr1_0]). input_clause(clause32,conjecture, [-- hskp21, ++ ndr1_0]). input_clause(clause33,conjecture, [-- hskp20, ++ ndr1_0]). input_clause(clause34,conjecture, [-- hskp19, ++ ndr1_0]). input_clause(clause35,conjecture, [-- hskp18, ++ ndr1_0]). input_clause(clause36,conjecture, [-- hskp17, ++ ndr1_0]). input_clause(clause37,conjecture, [-- hskp16, ++ ndr1_0]). input_clause(clause38,conjecture, [-- hskp15, ++ ndr1_0]). input_clause(clause39,conjecture, [-- hskp14, ++ ndr1_0]). input_clause(clause40,conjecture, [-- hskp13, ++ ndr1_0]). input_clause(clause41,conjecture, [-- hskp12, ++ ndr1_0]). input_clause(clause42,conjecture, [-- hskp11, ++ ndr1_0]). input_clause(clause43,conjecture, [-- hskp10, ++ ndr1_0]). input_clause(clause44,conjecture, [-- hskp9, ++ ndr1_0]). input_clause(clause45,conjecture, [-- hskp8, ++ ndr1_0]). input_clause(clause46,conjecture, [-- hskp7, ++ ndr1_0]). input_clause(clause47,conjecture, [-- hskp6, ++ ndr1_0]). input_clause(clause48,conjecture, [-- hskp5, ++ ndr1_0]). input_clause(clause49,conjecture, [-- hskp4, ++ ndr1_0]). input_clause(clause50,conjecture, [-- hskp3, ++ ndr1_0]). input_clause(clause51,conjecture, [-- hskp2, ++ ndr1_0]). input_clause(clause52,conjecture, [-- hskp1, ++ ndr1_0]). input_clause(clause53,conjecture, [-- hskp0, ++ ndr1_0]). input_clause(clause54,conjecture, [++ hskp36, ++ hskp34, ++ hskp3]). input_clause(clause55,conjecture, [++ hskp16, ++ hskp17, ++ hskp18]). input_clause(clause56,conjecture, [++ hskp6, ++ hskp27, ++ hskp4]). input_clause(clause57,conjecture, [++ hskp40, ++ hskp31, ++ hskp52]). input_clause(clause58,conjecture, [-- hskp52, ++ c2_1(a595)]). input_clause(clause59,conjecture, [-- hskp52, ++ c1_1(a595)]). input_clause(clause60,conjecture, [-- hskp51, ++ c0_1(a583)]). input_clause(clause61,conjecture, [-- hskp51, ++ c3_1(a583)]). input_clause(clause62,conjecture, [-- hskp50, ++ c0_1(a574)]). input_clause(clause63,conjecture, [-- hskp50, ++ c1_1(a574)]). input_clause(clause64,conjecture, [-- hskp49, ++ c2_1(a568)]). input_clause(clause65,conjecture, [-- hskp48, ++ c1_1(a566)]). input_clause(clause66,conjecture, [-- hskp47, ++ c0_1(a564)]). input_clause(clause67,conjecture, [-- hskp47, ++ c1_1(a564)]). input_clause(clause68,conjecture, [-- hskp46, ++ c1_1(a562)]). input_clause(clause69,conjecture, [-- hskp45, ++ c0_1(a561)]). input_clause(clause70,conjecture, [-- hskp44, ++ c0_1(a559)]). input_clause(clause71,conjecture, [-- hskp44, ++ c2_1(a559)]). input_clause(clause72,conjecture, [-- hskp43, ++ c3_1(a557)]). input_clause(clause73,conjecture, [-- hskp43, ++ c0_1(a557)]). input_clause(clause74,conjecture, [-- hskp42, ++ c1_1(a556)]). input_clause(clause75,conjecture, [-- hskp42, ++ c3_1(a556)]). input_clause(clause76,conjecture, [-- hskp41, ++ c3_1(a555)]). input_clause(clause77,conjecture, [-- hskp41, ++ c0_1(a555)]). input_clause(clause78,conjecture, [-- hskp40, ++ c3_1(a551)]). input_clause(clause79,conjecture, [-- hskp40, ++ c2_1(a551)]). input_clause(clause80,conjecture, [-- hskp39, ++ c3_1(a549)]). input_clause(clause81,conjecture, [-- hskp39, ++ c2_1(a549)]). input_clause(clause82,conjecture, [-- hskp39, ++ c1_1(a549)]). input_clause(clause83,conjecture, [-- hskp38, ++ c2_1(a547)]). input_clause(clause84,conjecture, [-- hskp38, ++ c1_1(a547)]). input_clause(clause85,conjecture, [-- hskp38, ++ c0_1(a547)]). input_clause(clause86,conjecture, [-- hskp37, ++ c1_1(a544)]). input_clause(clause87,conjecture, [-- hskp36, ++ c0_1(a541)]). input_clause(clause88,conjecture, [-- hskp36, ++ c1_1(a541)]). input_clause(clause89,conjecture, [-- hskp36, ++ c2_1(a541)]). input_clause(clause90,conjecture, [-- hskp35, ++ c2_1(a538)]). input_clause(clause91,conjecture, [-- hskp35, ++ c1_1(a538)]). input_clause(clause92,conjecture, [-- hskp35, ++ c3_1(a538)]). input_clause(clause93,conjecture, [-- hskp34, ++ c0_1(a537)]). input_clause(clause94,conjecture, [-- hskp34, ++ c3_1(a537)]). input_clause(clause95,conjecture, [-- hskp33, ++ c1_1(a536)]). input_clause(clause96,conjecture, [-- hskp33, ++ c2_1(a536)]). input_clause(clause97,conjecture, [-- hskp33, ++ c0_1(a536)]). input_clause(clause98,conjecture, [-- hskp32, ++ c0_1(a596)]). input_clause(clause99,conjecture, [-- hskp30, ++ c1_1(a591)]). input_clause(clause100,conjecture, [-- hskp28, ++ c2_1(a589)]). input_clause(clause101,conjecture, [-- hskp28, ++ c3_1(a589)]). input_clause(clause102,conjecture, [-- hskp27, ++ c1_1(a586)]). input_clause(clause103,conjecture, [-- hskp26, ++ c0_1(a584)]). input_clause(clause104,conjecture, [-- hskp26, ++ c1_1(a584)]). input_clause(clause105,conjecture, [-- hskp24, ++ c2_1(a581)]). input_clause(clause106,conjecture, [-- hskp23, ++ c3_1(a578)]). input_clause(clause107,conjecture, [-- hskp22, ++ c1_1(a577)]). input_clause(clause108,conjecture, [-- hskp21, ++ c1_1(a576)]). input_clause(clause109,conjecture, [-- hskp18, ++ c0_1(a572)]). input_clause(clause110,conjecture, [-- hskp17, ++ c0_1(a571)]). input_clause(clause111,conjecture, [-- hskp17, ++ c3_1(a571)]). input_clause(clause112,conjecture, [-- hskp16, ++ c3_1(a570)]). input_clause(clause113,conjecture, [-- hskp16, ++ c1_1(a570)]). input_clause(clause114,conjecture, [-- hskp14, ++ c0_1(a567)]). input_clause(clause115,conjecture, [-- hskp13, ++ c3_1(a565)]). input_clause(clause116,conjecture, [-- hskp13, ++ c2_1(a565)]). input_clause(clause117,conjecture, [-- hskp12, ++ c3_1(a563)]). input_clause(clause118,conjecture, [-- hskp11, ++ c1_1(a560)]). input_clause(clause119,conjecture, [-- hskp10, ++ c3_1(a558)]). input_clause(clause120,conjecture, [-- hskp7, ++ c0_1(a550)]). input_clause(clause121,conjecture, [-- hskp7, ++ c3_1(a550)]). input_clause(clause122,conjecture, [-- hskp6, ++ c3_1(a548)]). input_clause(clause123,conjecture, [-- hskp5, ++ c2_1(a546)]). input_clause(clause124,conjecture, [-- hskp4, ++ c1_1(a545)]). input_clause(clause125,conjecture, [-- hskp2, ++ c2_1(a540)]). input_clause(clause126,conjecture, [-- hskp2, ++ c1_1(a540)]). input_clause(clause127,conjecture, [-- hskp0, ++ c1_1(a535)]). input_clause(clause128,conjecture, [-- hskp0, ++ c0_1(a535)]). input_clause(clause129,conjecture, [-- c0_1(a595), -- hskp52]). input_clause(clause130,conjecture, [-- c2_1(a583), -- hskp51]). input_clause(clause131,conjecture, [-- c3_1(a574), -- hskp50]). input_clause(clause132,conjecture, [-- c0_1(a568), -- hskp49]). input_clause(clause133,conjecture, [-- c1_1(a568), -- hskp49]). input_clause(clause134,conjecture, [-- c3_1(a566), -- hskp48]). input_clause(clause135,conjecture, [-- c2_1(a566), -- hskp48]). input_clause(clause136,conjecture, [-- c2_1(a564), -- hskp47]). input_clause(clause137,conjecture, [-- c3_1(a562), -- hskp46]). input_clause(clause138,conjecture, [-- c0_1(a562), -- hskp46]). input_clause(clause139,conjecture, [-- c3_1(a561), -- hskp45]). input_clause(clause140,conjecture, [-- c2_1(a561), -- hskp45]). input_clause(clause141,conjecture, [-- c3_1(a559), -- hskp44]). input_clause(clause142,conjecture, [-- c1_1(a557), -- hskp43]). input_clause(clause143,conjecture, [-- c2_1(a556), -- hskp42]). input_clause(clause144,conjecture, [-- c2_1(a555), -- hskp41]). input_clause(clause145,conjecture, [-- c0_1(a551), -- hskp40]). input_clause(clause146,conjecture, [-- c2_1(a544), -- hskp37]). input_clause(clause147,conjecture, [-- c3_1(a544), -- hskp37]). input_clause(clause148,conjecture, [-- c1_1(a537), -- hskp34]). input_clause(clause149,conjecture, [-- c3_1(a596), -- hskp32]). input_clause(clause150,conjecture, [-- c2_1(a596), -- hskp32]). input_clause(clause151,conjecture, [-- c0_1(a594), -- hskp31]). input_clause(clause152,conjecture, [-- c3_1(a594), -- hskp31]). input_clause(clause153,conjecture, [-- c1_1(a594), -- hskp31]). input_clause(clause154,conjecture, [-- c2_1(a591), -- hskp30]). input_clause(clause155,conjecture, [-- c0_1(a591), -- hskp30]). input_clause(clause156,conjecture, [-- c3_1(a590), -- hskp29]). input_clause(clause157,conjecture, [-- c0_1(a590), -- hskp29]). input_clause(clause158,conjecture, [-- c1_1(a590), -- hskp29]). input_clause(clause159,conjecture, [-- c0_1(a589), -- hskp28]). input_clause(clause160,conjecture, [-- c0_1(a586), -- hskp27]). input_clause(clause161,conjecture, [-- c3_1(a586), -- hskp27]). input_clause(clause162,conjecture, [-- c3_1(a584), -- hskp26]). input_clause(clause163,conjecture, [-- c3_1(a582), -- hskp25]). input_clause(clause164,conjecture, [-- c2_1(a582), -- hskp25]). input_clause(clause165,conjecture, [-- c1_1(a582), -- hskp25]). input_clause(clause166,conjecture, [-- c1_1(a581), -- hskp24]). input_clause(clause167,conjecture, [-- c3_1(a581), -- hskp24]). input_clause(clause168,conjecture, [-- c0_1(a578), -- hskp23]). input_clause(clause169,conjecture, [-- c1_1(a578), -- hskp23]). input_clause(clause170,conjecture, [-- c3_1(a577), -- hskp22]). input_clause(clause171,conjecture, [-- c0_1(a577), -- hskp22]). input_clause(clause172,conjecture, [-- c0_1(a576), -- hskp21]). input_clause(clause173,conjecture, [-- c3_1(a576), -- hskp21]). input_clause(clause174,conjecture, [-- c2_1(a575), -- hskp20]). input_clause(clause175,conjecture, [-- c0_1(a575), -- hskp20]). input_clause(clause176,conjecture, [-- c3_1(a575), -- hskp20]). input_clause(clause177,conjecture, [-- c2_1(a573), -- hskp19]). input_clause(clause178,conjecture, [-- c0_1(a573), -- hskp19]). input_clause(clause179,conjecture, [-- c1_1(a573), -- hskp19]). input_clause(clause180,conjecture, [-- c3_1(a572), -- hskp18]). input_clause(clause181,conjecture, [-- c1_1(a572), -- hskp18]). input_clause(clause182,conjecture, [-- c2_1(a571), -- hskp17]). input_clause(clause183,conjecture, [-- c0_1(a570), -- hskp16]). input_clause(clause184,conjecture, [-- c0_1(a569), -- hskp15]). input_clause(clause185,conjecture, [-- c1_1(a569), -- hskp15]). input_clause(clause186,conjecture, [-- c2_1(a569), -- hskp15]). input_clause(clause187,conjecture, [-- c1_1(a567), -- hskp14]). input_clause(clause188,conjecture, [-- c3_1(a567), -- hskp14]). input_clause(clause189,conjecture, [-- c1_1(a565), -- hskp13]). input_clause(clause190,conjecture, [-- c0_1(a563), -- hskp12]). input_clause(clause191,conjecture, [-- c2_1(a563), -- hskp12]). input_clause(clause192,conjecture, [-- c3_1(a560), -- hskp11]). input_clause(clause193,conjecture, [-- c0_1(a560), -- hskp11]). input_clause(clause194,conjecture, [-- c1_1(a558), -- hskp10]). input_clause(clause195,conjecture, [-- c0_1(a558), -- hskp10]). input_clause(clause196,conjecture, [-- c0_1(a554), -- hskp9]). input_clause(clause197,conjecture, [-- c2_1(a554), -- hskp9]). input_clause(clause198,conjecture, [-- c1_1(a554), -- hskp9]). input_clause(clause199,conjecture, [-- c3_1(a552), -- hskp8]). input_clause(clause200,conjecture, [-- c1_1(a552), -- hskp8]). input_clause(clause201,conjecture, [-- c2_1(a552), -- hskp8]). input_clause(clause202,conjecture, [-- c1_1(a550), -- hskp7]). input_clause(clause203,conjecture, [-- c2_1(a548), -- hskp6]). input_clause(clause204,conjecture, [-- c0_1(a548), -- hskp6]). input_clause(clause205,conjecture, [-- c3_1(a546), -- hskp5]). input_clause(clause206,conjecture, [-- c1_1(a546), -- hskp5]). input_clause(clause207,conjecture, [-- c2_1(a545), -- hskp4]). input_clause(clause208,conjecture, [-- c0_1(a545), -- hskp4]). input_clause(clause209,conjecture, [-- c1_1(a543), -- hskp3]). input_clause(clause210,conjecture, [-- c0_1(a543), -- hskp3]). input_clause(clause211,conjecture, [-- c3_1(a543), -- hskp3]). input_clause(clause212,conjecture, [-- c3_1(a540), -- hskp2]). input_clause(clause213,conjecture, [-- c2_1(a539), -- hskp1]). input_clause(clause214,conjecture, [-- c1_1(a539), -- hskp1]). input_clause(clause215,conjecture, [-- c0_1(a539), -- hskp1]). input_clause(clause216,conjecture, [-- c2_1(a535), -- hskp0]). input_clause(clause217,conjecture, [-- ndr1_0, ++ hskp28, ++ c1_1(U), ++ c0_1(U), ++ c2_1(U)]). input_clause(clause218,conjecture, [-- c3_1(U), -- ndr1_0, ++ c0_1(U), ++ c2_1(U), ++ hskp44, ++ hskp11]). input_clause(clause219,conjecture, [-- c2_1(U), -- ndr1_0, ++ c1_1(U), ++ c0_1(U), ++ hskp13, ++ hskp48]). input_clause(clause220,conjecture, [-- c0_1(U), -- ndr1_0, ++ c2_1(U), ++ c1_1(U), ++ hskp19, ++ hskp50]). input_clause(clause221,conjecture, [-- c0_1(U), -- ndr1_0, ++ c3_1(U), ++ c2_1(U), ++ hskp39, ++ hskp24]). input_clause(clause222,conjecture, [-- c3_1(U), -- ndr1_0, ++ c2_1(U), ++ c1_1(U), ++ hskp29, ++ hskp30]). input_clause(clause223,conjecture, [-- c2_1(U), -- c0_1(U), -- ndr1_0, ++ c1_1(U), ++ hskp7, ++ hskp40]). input_clause(clause224,conjecture, [-- c1_1(U), -- c3_1(U), -- ndr1_0, ++ c0_1(U), ++ hskp9, ++ hskp41]). input_clause(clause225,conjecture, [-- c3_1(U), -- c1_1(U), -- ndr1_0, ++ c2_1(U), ++ hskp20, ++ hskp21]). input_clause(clause226,conjecture, [-- c1_1(U), -- c0_1(U), -- ndr1_0, ++ c3_1(U), ++ hskp22, ++ hskp23]). input_clause(clause227,conjecture, [-- c3_1(U), -- c1_1(U), -- c0_1(U), -- ndr1_0, ++ hskp1, ++ hskp2]). input_clause(clause228,conjecture, [-- c3_1(U), -- ndr1_0, ++ c0_1(U), ++ c2_1(U), ++ c3_1(V), ++ c1_1(V), ++ c2_1(V), ++ hskp38]). input_clause(clause229,conjecture, [-- c1_1(U), -- ndr1_0, ++ c2_1(U), ++ c0_1(U), ++ c3_1(V), ++ c2_1(V), ++ c1_1(V), ++ hskp14]). input_clause(clause230,conjecture, [-- c1_1(U), -- c0_1(U), -- ndr1_0, ++ c3_1(U), ++ c2_1(V), ++ c3_1(V), ++ c0_1(V), ++ hskp33]). input_clause(clause231,conjecture, [-- c1_1(U), -- c3_1(U), -- ndr1_0, ++ c0_1(U), ++ c0_1(V), ++ c1_1(V), ++ c2_1(V), ++ hskp6]). input_clause(clause232,conjecture, [-- c0_1(U), -- c1_1(U), -- ndr1_0, ++ c2_1(U), ++ c2_1(V), ++ c0_1(V), ++ c3_1(V), ++ hskp45]). input_clause(clause233,conjecture, [-- c3_1(U), -- c1_1(U), -- ndr1_0, ++ c2_1(U), ++ c1_1(V), ++ c2_1(V), ++ c3_1(V), ++ hskp12]). input_clause(clause234,conjecture, [-- c0_1(U), -- c3_1(U), -- ndr1_0, ++ c1_1(U), ++ c3_1(V), ++ c2_1(V), ++ c1_1(V), ++ hskp51]). input_clause(clause235,conjecture, [-- c1_1(U), -- ndr1_0, -- c3_1(V), ++ c0_1(U), ++ c3_1(U), ++ c0_1(V), ++ c1_1(V), ++ hskp26]). input_clause(clause236,conjecture, [-- c2_1(U), -- c1_1(U), -- c0_1(U), -- ndr1_0, ++ c1_1(V), ++ c2_1(V), ++ c3_1(V), ++ hskp0]). input_clause(clause237,conjecture, [-- ndr1_0, -- c1_1(U), -- c2_1(U), -- c3_1(U), ++ c1_1(V), ++ c2_1(V), ++ c3_1(V), ++ hskp34]). input_clause(clause238,conjecture, [-- c0_1(U), -- ndr1_0, -- c2_1(V), -- c1_1(V), ++ c1_1(U), ++ c2_1(U), ++ c3_1(V), ++ hskp35]). input_clause(clause239,conjecture, [-- c2_1(U), -- c0_1(U), -- ndr1_0, -- c0_1(V), ++ c1_1(U), ++ c1_1(V), ++ c3_1(V), ++ hskp37]). input_clause(clause240,conjecture, [-- c3_1(U), -- ndr1_0, -- c2_1(V), -- c1_1(V), ++ c1_1(U), ++ c2_1(U), ++ c3_1(V), ++ hskp5]). input_clause(clause241,conjecture, [-- c3_1(U), -- c1_1(U), -- ndr1_0, -- c1_1(V), ++ c2_1(U), ++ c3_1(V), ++ c0_1(V), ++ hskp39]). input_clause(clause242,conjecture, [-- c0_1(U), -- c3_1(U), -- ndr1_0, -- c2_1(V), ++ c1_1(U), ++ c0_1(V), ++ c1_1(V), ++ hskp8]). input_clause(clause243,conjecture, [-- c0_1(U), -- ndr1_0, -- c2_1(V), -- c1_1(V), ++ c1_1(U), ++ c2_1(U), ++ c0_1(V), ++ hskp43]). input_clause(clause244,conjecture, [-- c0_1(U), -- ndr1_0, -- c0_1(V), -- c3_1(V), ++ c2_1(U), ++ c3_1(U), ++ c2_1(V), ++ hskp49]). input_clause(clause245,conjecture, [-- c1_1(U), -- ndr1_0, -- c2_1(V), -- c3_1(V), ++ c3_1(U), ++ c2_1(U), ++ c1_1(V), ++ hskp15]). input_clause(clause246,conjecture, [-- c1_1(U), -- c3_1(U), -- ndr1_0, -- c3_1(V), ++ c2_1(U), ++ c2_1(V), ++ c0_1(V), ++ hskp46]). input_clause(clause247,conjecture, [-- c2_1(U), -- c3_1(U), -- c1_1(U), -- ndr1_0, -- c1_1(V), ++ c3_1(V), ++ c0_1(V), ++ hskp4]). input_clause(clause248,conjecture, [-- c2_1(U), -- c0_1(U), -- ndr1_0, -- c2_1(V), -- c1_1(V), ++ c1_1(U), ++ c0_1(V), ++ hskp46]). input_clause(clause249,conjecture, [-- c2_1(U), -- c1_1(U), -- ndr1_0, -- c2_1(V), -- c3_1(V), ++ c3_1(U), ++ c0_1(V), ++ hskp47]). input_clause(clause250,conjecture, [-- c1_1(U), -- c0_1(U), -- c2_1(U), -- ndr1_0, -- c1_1(V), ++ c3_1(V), ++ c0_1(V), ++ hskp34]). input_clause(clause251,conjecture, [-- c1_1(U), -- c2_1(U), -- c3_1(U), -- ndr1_0, -- c2_1(V), ++ c3_1(V), ++ c0_1(V), ++ hskp46]). input_clause(clause252,conjecture, [-- c1_1(U), -- c0_1(U), -- ndr1_0, -- c1_1(V), -- c2_1(V), ++ c3_1(U), ++ c3_1(V), ++ hskp32]). input_clause(clause253,conjecture, [-- c1_1(U), -- c2_1(U), -- c3_1(U), -- ndr1_0, -- c2_1(V), -- c3_1(V), ++ c1_1(V), ++ hskp38]). input_clause(clause254,conjecture, [-- c1_1(U), -- c3_1(U), -- ndr1_0, -- c2_1(V), -- c0_1(V), -- c1_1(V), ++ c2_1(U), ++ hskp42]). input_clause(clause255,conjecture, [-- c0_1(U), -- c3_1(U), -- c2_1(U), -- ndr1_0, -- c2_1(V), -- c1_1(V), ++ c0_1(V), ++ hskp10]). input_clause(clause256,conjecture, [-- c2_1(U), -- c3_1(U), -- c1_1(U), -- ndr1_0, -- c1_1(V), -- c3_1(V), ++ c2_1(V), ++ hskp25]). input_clause(clause257,conjecture, [-- c2_1(U), -- ndr1_0, -- c3_1(V), -- c1_1(W), -- c0_1(W), ++ c0_1(U), ++ c3_1(U), ++ c0_1(V), ++ c1_1(V), ++ c2_1(W)]). input_clause(clause258,conjecture, [-- c1_1(U), -- c3_1(U), -- ndr1_0, -- c2_1(V), -- c3_1(V), ++ c2_1(U), ++ c2_1(W), ++ c3_1(W), ++ c1_1(W), ++ c1_1(V)]). input_clause(clause259,conjecture, [-- c0_1(U), -- c3_1(U), -- ndr1_0, -- c2_1(V), -- c0_1(W), -- c3_1(W), ++ c2_1(U), ++ c1_1(V), ++ c3_1(V), ++ c1_1(W)]). input_clause(clause260,conjecture, [-- c0_1(U), -- c1_1(U), -- c2_1(U), -- ndr1_0, -- c3_1(V), -- c1_1(W), -- c0_1(W), ++ c2_1(V), ++ c1_1(V), ++ c2_1(W)]). %--------------------------------------------------------------------------