%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : PUZ077+1 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:32:03 PM UTC 2026
% Result : Theorem 11.61s 1.97s
% Output : Proof 11.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 4
% Syntax : Number of formulae : 168 ( 26 unt; 0 def)
% Number of atoms : 1460 ( 915 equ)
% Maximal formula atoms : 362 ( 8 avg)
% Number of connectives : 1862 ( 570 ~; 706 |; 583 &)
% ( 3 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 96 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 66 ( 64 usr; 1 prp; 0-38 aty)
% Number of functors : 137 ( 137 usr; 100 con; 0-2 aty)
% Number of variables : 1047 ( 420 sgn 92 !; 74 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [TLH34901,TLH34900] :
( duewest(TLH34900,TLH34901)
<=> ( ? [TLH34930,TLH34931,TLH34932,TLH34933,TLH34934,TLH34935,TLH34936,TLH34937] :
( west(TLH34937,TLH34901)
& west(TLH34936,TLH34937)
& west(TLH34935,TLH34936)
& west(TLH34934,TLH34935)
& west(TLH34933,TLH34934)
& west(TLH34932,TLH34933)
& west(TLH34931,TLH34932)
& west(TLH34930,TLH34931)
& west(TLH34900,TLH34930) )
| ? [TLH34923,TLH34924,TLH34925,TLH34926,TLH34927,TLH34928,TLH34929] :
( west(TLH34929,TLH34901)
& west(TLH34928,TLH34929)
& west(TLH34927,TLH34928)
& west(TLH34926,TLH34927)
& west(TLH34925,TLH34926)
& west(TLH34924,TLH34925)
& west(TLH34923,TLH34924)
& west(TLH34900,TLH34923) )
| ? [TLH34917,TLH34918,TLH34919,TLH34920,TLH34921,TLH34922] :
( west(TLH34922,TLH34901)
& west(TLH34921,TLH34922)
& west(TLH34920,TLH34921)
& west(TLH34919,TLH34920)
& west(TLH34918,TLH34919)
& west(TLH34917,TLH34918)
& west(TLH34900,TLH34917) )
| ? [TLH34912,TLH34913,TLH34914,TLH34915,TLH34916] :
( west(TLH34916,TLH34901)
& west(TLH34915,TLH34916)
& west(TLH34914,TLH34915)
& west(TLH34913,TLH34914)
& west(TLH34912,TLH34913)
& west(TLH34900,TLH34912) )
| ? [TLH34908,TLH34909,TLH34910,TLH34911] :
( west(TLH34911,TLH34901)
& west(TLH34910,TLH34911)
& west(TLH34909,TLH34910)
& west(TLH34908,TLH34909)
& west(TLH34900,TLH34908) )
| ? [TLH34905,TLH34906,TLH34907] :
( west(TLH34907,TLH34901)
& west(TLH34906,TLH34907)
& west(TLH34905,TLH34906)
& west(TLH34900,TLH34905) )
| ? [TLH34903,TLH34904] :
( west(TLH34904,TLH34901)
& west(TLH34903,TLH34904)
& west(TLH34900,TLH34903) )
| ? [TLH34902] :
( west(TLH34902,TLH34901)
& west(TLH34900,TLH34902) )
| west(TLH34900,TLH34901) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tlhfof34977) ).
fof(f2_nnf,plain,
! [TLH34901,TLH34900] :
( ( ( ! [TLH34930,TLH34931,TLH34932,TLH34933,TLH34934,TLH34935,TLH34936,TLH34937] :
( ~ west(TLH34937,TLH34901)
| ~ west(TLH34936,TLH34937)
| ~ west(TLH34935,TLH34936)
| ~ west(TLH34934,TLH34935)
| ~ west(TLH34933,TLH34934)
| ~ west(TLH34932,TLH34933)
| ~ west(TLH34931,TLH34932)
| ~ west(TLH34930,TLH34931)
| ~ west(TLH34900,TLH34930) )
& ! [TLH34923,TLH34924,TLH34925,TLH34926,TLH34927,TLH34928,TLH34929] :
( ~ west(TLH34929,TLH34901)
| ~ west(TLH34928,TLH34929)
| ~ west(TLH34927,TLH34928)
| ~ west(TLH34926,TLH34927)
| ~ west(TLH34925,TLH34926)
| ~ west(TLH34924,TLH34925)
| ~ west(TLH34923,TLH34924)
| ~ west(TLH34900,TLH34923) )
& ! [TLH34917,TLH34918,TLH34919,TLH34920,TLH34921,TLH34922] :
( ~ west(TLH34922,TLH34901)
| ~ west(TLH34921,TLH34922)
| ~ west(TLH34920,TLH34921)
| ~ west(TLH34919,TLH34920)
| ~ west(TLH34918,TLH34919)
| ~ west(TLH34917,TLH34918)
| ~ west(TLH34900,TLH34917) )
& ! [TLH34912,TLH34913,TLH34914,TLH34915,TLH34916] :
( ~ west(TLH34916,TLH34901)
| ~ west(TLH34915,TLH34916)
| ~ west(TLH34914,TLH34915)
| ~ west(TLH34913,TLH34914)
| ~ west(TLH34912,TLH34913)
| ~ west(TLH34900,TLH34912) )
& ! [TLH34908,TLH34909,TLH34910,TLH34911] :
( ~ west(TLH34911,TLH34901)
| ~ west(TLH34910,TLH34911)
| ~ west(TLH34909,TLH34910)
| ~ west(TLH34908,TLH34909)
| ~ west(TLH34900,TLH34908) )
& ! [TLH34905,TLH34906,TLH34907] :
( ~ west(TLH34907,TLH34901)
| ~ west(TLH34906,TLH34907)
| ~ west(TLH34905,TLH34906)
| ~ west(TLH34900,TLH34905) )
& ! [TLH34903,TLH34904] :
( ~ west(TLH34904,TLH34901)
| ~ west(TLH34903,TLH34904)
| ~ west(TLH34900,TLH34903) )
& ! [TLH34902] :
( ~ west(TLH34902,TLH34901)
| ~ west(TLH34900,TLH34902) )
& ~ west(TLH34900,TLH34901) )
| duewest(TLH34900,TLH34901) )
& ( ? [TLH34930,TLH34931,TLH34932,TLH34933,TLH34934,TLH34935,TLH34936,TLH34937] :
( west(TLH34937,TLH34901)
& west(TLH34936,TLH34937)
& west(TLH34935,TLH34936)
& west(TLH34934,TLH34935)
& west(TLH34933,TLH34934)
& west(TLH34932,TLH34933)
& west(TLH34931,TLH34932)
& west(TLH34930,TLH34931)
& west(TLH34900,TLH34930) )
| ? [TLH34923,TLH34924,TLH34925,TLH34926,TLH34927,TLH34928,TLH34929] :
( west(TLH34929,TLH34901)
& west(TLH34928,TLH34929)
& west(TLH34927,TLH34928)
& west(TLH34926,TLH34927)
& west(TLH34925,TLH34926)
& west(TLH34924,TLH34925)
& west(TLH34923,TLH34924)
& west(TLH34900,TLH34923) )
| ? [TLH34917,TLH34918,TLH34919,TLH34920,TLH34921,TLH34922] :
( west(TLH34922,TLH34901)
& west(TLH34921,TLH34922)
& west(TLH34920,TLH34921)
& west(TLH34919,TLH34920)
& west(TLH34918,TLH34919)
& west(TLH34917,TLH34918)
& west(TLH34900,TLH34917) )
| ? [TLH34912,TLH34913,TLH34914,TLH34915,TLH34916] :
( west(TLH34916,TLH34901)
& west(TLH34915,TLH34916)
& west(TLH34914,TLH34915)
& west(TLH34913,TLH34914)
& west(TLH34912,TLH34913)
& west(TLH34900,TLH34912) )
| ? [TLH34908,TLH34909,TLH34910,TLH34911] :
( west(TLH34911,TLH34901)
& west(TLH34910,TLH34911)
& west(TLH34909,TLH34910)
& west(TLH34908,TLH34909)
& west(TLH34900,TLH34908) )
| ? [TLH34905,TLH34906,TLH34907] :
( west(TLH34907,TLH34901)
& west(TLH34906,TLH34907)
& west(TLH34905,TLH34906)
& west(TLH34900,TLH34905) )
| ? [TLH34903,TLH34904] :
( west(TLH34904,TLH34901)
& west(TLH34903,TLH34904)
& west(TLH34900,TLH34903) )
| ? [TLH34902] :
( west(TLH34902,TLH34901)
& west(TLH34900,TLH34902) )
| west(TLH34900,TLH34901)
| ~ duewest(TLH34900,TLH34901) ) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [TLH34900,TLH34901,TLH34902,TLH34903,TLH34904,TLH34905,TLH34906,TLH34907,TLH34908,TLH34909,TLH34910,TLH34911,TLH34912,TLH34913,TLH34914,TLH34915,TLH34916,TLH34917,TLH34918,TLH34919,TLH34920,TLH34921,TLH34922,TLH34923,TLH34924,TLH34925,TLH34926,TLH34927,TLH34928,TLH34929,TLH34930,TLH34931,TLH34932,TLH34933,TLH34934,TLH34935,TLH34936,TLH34937] :
( ( ( ( ~ west(TLH34937,TLH34901)
| ~ west(TLH34936,TLH34937)
| ~ west(TLH34935,TLH34936)
| ~ west(TLH34934,TLH34935)
| ~ west(TLH34933,TLH34934)
| ~ west(TLH34932,TLH34933)
| ~ west(TLH34931,TLH34932)
| ~ west(TLH34930,TLH34931)
| ~ west(TLH34900,TLH34930) )
& ( ~ west(TLH34929,TLH34901)
| ~ west(TLH34928,TLH34929)
| ~ west(TLH34927,TLH34928)
| ~ west(TLH34926,TLH34927)
| ~ west(TLH34925,TLH34926)
| ~ west(TLH34924,TLH34925)
| ~ west(TLH34923,TLH34924)
| ~ west(TLH34900,TLH34923) )
& ( ~ west(TLH34922,TLH34901)
| ~ west(TLH34921,TLH34922)
| ~ west(TLH34920,TLH34921)
| ~ west(TLH34919,TLH34920)
| ~ west(TLH34918,TLH34919)
| ~ west(TLH34917,TLH34918)
| ~ west(TLH34900,TLH34917) )
& ( ~ west(TLH34916,TLH34901)
| ~ west(TLH34915,TLH34916)
| ~ west(TLH34914,TLH34915)
| ~ west(TLH34913,TLH34914)
| ~ west(TLH34912,TLH34913)
| ~ west(TLH34900,TLH34912) )
& ( ~ west(TLH34911,TLH34901)
| ~ west(TLH34910,TLH34911)
| ~ west(TLH34909,TLH34910)
| ~ west(TLH34908,TLH34909)
| ~ west(TLH34900,TLH34908) )
& ( ~ west(TLH34907,TLH34901)
| ~ west(TLH34906,TLH34907)
| ~ west(TLH34905,TLH34906)
| ~ west(TLH34900,TLH34905) )
& ( ~ west(TLH34904,TLH34901)
| ~ west(TLH34903,TLH34904)
| ~ west(TLH34900,TLH34903) )
& ( ~ west(TLH34902,TLH34901)
| ~ west(TLH34900,TLH34902) )
& ~ west(TLH34900,TLH34901) )
| duewest(TLH34900,TLH34901) )
& ( ( west(sk35(TLH34901,TLH34900),TLH34901)
& west(sk34(TLH34901,TLH34900),sk35(TLH34901,TLH34900))
& west(sk33(TLH34901,TLH34900),sk34(TLH34901,TLH34900))
& west(sk32(TLH34901,TLH34900),sk33(TLH34901,TLH34900))
& west(sk31(TLH34901,TLH34900),sk32(TLH34901,TLH34900))
& west(sk30(TLH34901,TLH34900),sk31(TLH34901,TLH34900))
& west(sk29(TLH34901,TLH34900),sk30(TLH34901,TLH34900))
& west(sk28(TLH34901,TLH34900),sk29(TLH34901,TLH34900))
& west(TLH34900,sk28(TLH34901,TLH34900)) )
| ( west(sk27(TLH34901,TLH34900),TLH34901)
& west(sk26(TLH34901,TLH34900),sk27(TLH34901,TLH34900))
& west(sk25(TLH34901,TLH34900),sk26(TLH34901,TLH34900))
& west(sk24(TLH34901,TLH34900),sk25(TLH34901,TLH34900))
& west(sk23(TLH34901,TLH34900),sk24(TLH34901,TLH34900))
& west(sk22(TLH34901,TLH34900),sk23(TLH34901,TLH34900))
& west(sk21(TLH34901,TLH34900),sk22(TLH34901,TLH34900))
& west(TLH34900,sk21(TLH34901,TLH34900)) )
| ( west(sk20(TLH34901,TLH34900),TLH34901)
& west(sk19(TLH34901,TLH34900),sk20(TLH34901,TLH34900))
& west(sk18(TLH34901,TLH34900),sk19(TLH34901,TLH34900))
& west(sk17(TLH34901,TLH34900),sk18(TLH34901,TLH34900))
& west(sk16(TLH34901,TLH34900),sk17(TLH34901,TLH34900))
& west(sk15(TLH34901,TLH34900),sk16(TLH34901,TLH34900))
& west(TLH34900,sk15(TLH34901,TLH34900)) )
| ( west(sk14(TLH34901,TLH34900),TLH34901)
& west(sk13(TLH34901,TLH34900),sk14(TLH34901,TLH34900))
& west(sk12(TLH34901,TLH34900),sk13(TLH34901,TLH34900))
& west(sk11(TLH34901,TLH34900),sk12(TLH34901,TLH34900))
& west(sk10(TLH34901,TLH34900),sk11(TLH34901,TLH34900))
& west(TLH34900,sk10(TLH34901,TLH34900)) )
| ( west(sk9(TLH34901,TLH34900),TLH34901)
& west(sk8(TLH34901,TLH34900),sk9(TLH34901,TLH34900))
& west(sk7(TLH34901,TLH34900),sk8(TLH34901,TLH34900))
& west(sk6(TLH34901,TLH34900),sk7(TLH34901,TLH34900))
& west(TLH34900,sk6(TLH34901,TLH34900)) )
| ( west(sk5(TLH34901,TLH34900),TLH34901)
& west(sk4(TLH34901,TLH34900),sk5(TLH34901,TLH34900))
& west(sk3(TLH34901,TLH34900),sk4(TLH34901,TLH34900))
& west(TLH34900,sk3(TLH34901,TLH34900)) )
| ( west(sk2(TLH34901,TLH34900),TLH34901)
& west(sk1(TLH34901,TLH34900),sk2(TLH34901,TLH34900))
& west(TLH34900,sk1(TLH34901,TLH34900)) )
| ( west(sk0(TLH34901,TLH34900),TLH34901)
& west(TLH34900,sk0(TLH34901,TLH34900)) )
| west(TLH34900,TLH34901)
| ~ duewest(TLH34900,TLH34901) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2,sk3,sk4,sk5,sk6,sk7,sk8,sk9,sk10,sk11,sk12,sk13,sk14,sk15,sk16,sk17,sk18,sk19,sk20,sk21,sk22,sk23,sk24,sk25,sk26,sk27,sk28,sk29,sk30,sk31,sk32,sk33,sk34,sk35])],[f2_nnf]) ).
cnf(c2441,plain,
def812(X1,X0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def722,def723,def724,def725,def726,def727,def728,def729,def730,def731,def732,def733,def734,def735,def736,def737,def738,def739,def740,def741,def742,def743,def744,def745,def746,def747,def748,def749,def750,def751,def752,def753,def754,def755,def756,def757,def758,def759,def760,def761,def762,def763,def764,def765,def766,def767,def768,def769,def770,def771,def772,def773,def774,def775,def776,def777,def778,def779,def780,def781,def782,def783,def784,def785,def786,def787,def788,def789,def790,def791,def792,def793,def794,def795,def796,def797,def798,def799,def800,def801,def802,def803,def804,def805,def806,def807,def808,def809,def810,def811,def812])],[f2_sk]) ).
cnf(c2439,plain,
( def811(X1,X0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37)
| ~ def812(X1,X0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def722,def723,def724,def725,def726,def727,def728,def729,def730,def731,def732,def733,def734,def735,def736,def737,def738,def739,def740,def741,def742,def743,def744,def745,def746,def747,def748,def749,def750,def751,def752,def753,def754,def755,def756,def757,def758,def759,def760,def761,def762,def763,def764,def765,def766,def767,def768,def769,def770,def771,def772,def773,def774,def775,def776,def777,def778,def779,def780,def781,def782,def783,def784,def785,def786,def787,def788,def789,def790,def791,def792,def793,def794,def795,def796,def797,def798,def799,def800,def801,def802,def803,def804,def805,def806,def807,def808,def809,def810,def811,def812])],[f2_sk]) ).
cnf(p4954,plain,
def811(X1,X0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37),
inference(resolution,[status(thm)],[c2441,c2439]) ).
cnf(c2435,plain,
( def810(X1,X0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37)
| duewest(X1,X0)
| ~ def811(X1,X0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def722,def723,def724,def725,def726,def727,def728,def729,def730,def731,def732,def733,def734,def735,def736,def737,def738,def739,def740,def741,def742,def743,def744,def745,def746,def747,def748,def749,def750,def751,def752,def753,def754,def755,def756,def757,def758,def759,def760,def761,def762,def763,def764,def765,def766,def767,def768,def769,def770,def771,def772,def773,def774,def775,def776,def777,def778,def779,def780,def781,def782,def783,def784,def785,def786,def787,def788,def789,def790,def791,def792,def793,def794,def795,def796,def797,def798,def799,def800,def801,def802,def803,def804,def805,def806,def807,def808,def809,def810,def811,def812])],[f2_sk]) ).
cnf(p7102,plain,
( def810(X1,X0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37)
| duewest(X0,X1) ),
inference(resolution,[status(thm)],[p4954,c2435]) ).
cnf(c2433,plain,
( def809(X1,X30,X31,X32,X33,X34,X35,X36,X37,X0)
| ~ def810(X1,X0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def722,def723,def724,def725,def726,def727,def728,def729,def730,def731,def732,def733,def734,def735,def736,def737,def738,def739,def740,def741,def742,def743,def744,def745,def746,def747,def748,def749,def750,def751,def752,def753,def754,def755,def756,def757,def758,def759,def760,def761,def762,def763,def764,def765,def766,def767,def768,def769,def770,def771,def772,def773,def774,def775,def776,def777,def778,def779,def780,def781,def782,def783,def784,def785,def786,def787,def788,def789,def790,def791,def792,def793,def794,def795,def796,def797,def798,def799,def800,def801,def802,def803,def804,def805,def806,def807,def808,def809,def810,def811,def812])],[f2_sk]) ).
cnf(p7545,plain,
( def809(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11)
| duewest(X0,X1) ),
inference(resolution,[status(thm)],[p7102,c2433]) ).
fof(f5,axiom,
! [Y,X] :
( westof(X,Y)
<=> ( ? [Z] :
( duewest(Z,Y)
& vert(X,Z) )
| duewest(X,Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tlhfof34980) ).
fof(f5_nnf,plain,
! [Y,X] :
( ( ( ! [Z] :
( ~ duewest(Z,Y)
| ~ vert(X,Z) )
& ~ duewest(X,Y) )
| westof(X,Y) )
& ( ? [Z] :
( duewest(Z,Y)
& vert(X,Z) )
| duewest(X,Y)
| ~ westof(X,Y) ) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X,Y,Z] :
( ( ( ( ~ duewest(Z,Y)
| ~ vert(X,Z) )
& ~ duewest(X,Y) )
| westof(X,Y) )
& ( ( duewest(sk72(Y,X),Y)
& vert(X,sk72(Y,X)) )
| duewest(X,Y)
| ~ westof(X,Y) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk72])],[f5_nnf]) ).
cnf(c2721,plain,
( ~ duewest(X1,X0)
| westof(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p8108,plain,
( westof(X10,X11)
| def809(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9) ),
inference(resolution,[status(thm)],[p7545,c2721]) ).
fof(f6,conjecture,
westof(cell1,cell100),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tlhfof34981) ).
fof(f6_neg,negated_conjecture,
~ westof(cell1,cell100),
inference(negated_conjecture,[status(cth)],[f6]) ).
fof(f6_nnf,plain,
~ westof(cell1,cell100),
inference(nnf_transformation,[status(thm)],[f6_neg]) ).
fof(f6_sk,plain,
~ westof(cell1,cell100),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c2723,plain,
~ westof(cell1,cell100),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p9029,plain,
def809(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9),
inference(resolution,[status(thm)],[p8108,c2723]) ).
cnf(c2432,plain,
( def801(X1,X0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29)
| ~ def810(X1,X0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def722,def723,def724,def725,def726,def727,def728,def729,def730,def731,def732,def733,def734,def735,def736,def737,def738,def739,def740,def741,def742,def743,def744,def745,def746,def747,def748,def749,def750,def751,def752,def753,def754,def755,def756,def757,def758,def759,def760,def761,def762,def763,def764,def765,def766,def767,def768,def769,def770,def771,def772,def773,def774,def775,def776,def777,def778,def779,def780,def781,def782,def783,def784,def785,def786,def787,def788,def789,def790,def791,def792,def793,def794,def795,def796,def797,def798,def799,def800,def801,def802,def803,def804,def805,def806,def807,def808,def809,def810,def811,def812])],[f2_sk]) ).
cnf(p7543,plain,
( def801(X1,X0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29)
| duewest(X0,X1) ),
inference(resolution,[status(thm)],[p7102,c2432]) ).
cnf(c2434,plain,
( def810(X1,X0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37)
| ~ def809(X1,X30,X31,X32,X33,X34,X35,X36,X37,X0)
| ~ def801(X1,X0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def722,def723,def724,def725,def726,def727,def728,def729,def730,def731,def732,def733,def734,def735,def736,def737,def738,def739,def740,def741,def742,def743,def744,def745,def746,def747,def748,def749,def750,def751,def752,def753,def754,def755,def756,def757,def758,def759,def760,def761,def762,def763,def764,def765,def766,def767,def768,def769,def770,def771,def772,def773,def774,def775,def776,def777,def778,def779,def780,def781,def782,def783,def784,def785,def786,def787,def788,def789,def790,def791,def792,def793,def794,def795,def796,def797,def798,def799,def800,def801,def802,def803,def804,def805,def806,def807,def808,def809,def810,def811,def812])],[f2_sk]) ).
cnf(p8096,plain,
( def810(X1,X0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37)
| ~ def809(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11)
| duewest(X0,X1) ),
inference(resolution,[status(thm)],[p7543,c2434]) ).
cnf(p9031,plain,
( def810(X1,X0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37)
| duewest(X0,X1) ),
inference(resolution,[status(thm)],[p9029,p8096]) ).
cnf(p9841,plain,
( def801(X1,X0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29)
| duewest(X0,X1) ),
inference(resolution,[status(thm)],[p9031,c2432]) ).
cnf(c2405,plain,
( def793(X1,X0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| ~ def801(X1,X0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def722,def723,def724,def725,def726,def727,def728,def729,def730,def731,def732,def733,def734,def735,def736,def737,def738,def739,def740,def741,def742,def743,def744,def745,def746,def747,def748,def749,def750,def751,def752,def753,def754,def755,def756,def757,def758,def759,def760,def761,def762,def763,def764,def765,def766,def767,def768,def769,def770,def771,def772,def773,def774,def775,def776,def777,def778,def779,def780,def781,def782,def783,def784,def785,def786,def787,def788,def789,def790,def791,def792,def793,def794,def795,def796,def797,def798,def799,def800,def801,def802,def803,def804,def805,def806,def807,def808,def809,def810,def811,def812])],[f2_sk]) ).
cnf(p9843,plain,
( def793(X1,X0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22)
| duewest(X0,X1) ),
inference(resolution,[status(thm)],[p9841,c2405]) ).
cnf(c2381,plain,
( def786(X1,X0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| ~ def793(X1,X0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def722,def723,def724,def725,def726,def727,def728,def729,def730,def731,def732,def733,def734,def735,def736,def737,def738,def739,def740,def741,def742,def743,def744,def745,def746,def747,def748,def749,def750,def751,def752,def753,def754,def755,def756,def757,def758,def759,def760,def761,def762,def763,def764,def765,def766,def767,def768,def769,def770,def771,def772,def773,def774,def775,def776,def777,def778,def779,def780,def781,def782,def783,def784,def785,def786,def787,def788,def789,def790,def791,def792,def793,def794,def795,def796,def797,def798,def799,def800,def801,def802,def803,def804,def805,def806,def807,def808,def809,def810,def811,def812])],[f2_sk]) ).
cnf(p9849,plain,
( def786(X1,X0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16)
| duewest(X0,X1) ),
inference(resolution,[status(thm)],[p9843,c2381]) ).
cnf(c2360,plain,
( def780(X1,X0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11)
| ~ def786(X1,X0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def722,def723,def724,def725,def726,def727,def728,def729,def730,def731,def732,def733,def734,def735,def736,def737,def738,def739,def740,def741,def742,def743,def744,def745,def746,def747,def748,def749,def750,def751,def752,def753,def754,def755,def756,def757,def758,def759,def760,def761,def762,def763,def764,def765,def766,def767,def768,def769,def770,def771,def772,def773,def774,def775,def776,def777,def778,def779,def780,def781,def782,def783,def784,def785,def786,def787,def788,def789,def790,def791,def792,def793,def794,def795,def796,def797,def798,def799,def800,def801,def802,def803,def804,def805,def806,def807,def808,def809,def810,def811,def812])],[f2_sk]) ).
cnf(p9853,plain,
( def780(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13)
| duewest(X0,X1) ),
inference(resolution,[status(thm)],[p9849,c2360]) ).
cnf(c2343,plain,
( def779(X1,X8,X9,X10,X11,X0)
| ~ def780(X1,X0,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def722,def723,def724,def725,def726,def727,def728,def729,def730,def731,def732,def733,def734,def735,def736,def737,def738,def739,def740,def741,def742,def743,def744,def745,def746,def747,def748,def749,def750,def751,def752,def753,def754,def755,def756,def757,def758,def759,def760,def761,def762,def763,def764,def765,def766,def767,def768,def769,def770,def771,def772,def773,def774,def775,def776,def777,def778,def779,def780,def781,def782,def783,def784,def785,def786,def787,def788,def789,def790,def791,def792,def793,def794,def795,def796,def797,def798,def799,def800,def801,def802,def803,def804,def805,def806,def807,def808,def809,def810,def811,def812])],[f2_sk]) ).
cnf(p12743,plain,
( def779(X2,X3,X4,X5,X6,X7)
| duewest(X0,X1) ),
inference(resolution,[status(thm)],[p9853,c2343]) ).
cnf(p12749,plain,
( westof(X6,X7)
| def779(X0,X1,X2,X3,X4,X5) ),
inference(resolution,[status(thm)],[p12743,c2721]) ).
cnf(p12752,plain,
def779(X0,X1,X2,X3,X4,X5),
inference(resolution,[status(thm)],[p12749,c2723]) ).
cnf(c2339,plain,
( ~ west(X11,X0)
| def778(X1,X8,X9,X10,X11)
| ~ def779(X1,X8,X9,X10,X11,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def722,def723,def724,def725,def726,def727,def728,def729,def730,def731,def732,def733,def734,def735,def736,def737,def738,def739,def740,def741,def742,def743,def744,def745,def746,def747,def748,def749,def750,def751,def752,def753,def754,def755,def756,def757,def758,def759,def760,def761,def762,def763,def764,def765,def766,def767,def768,def769,def770,def771,def772,def773,def774,def775,def776,def777,def778,def779,def780,def781,def782,def783,def784,def785,def786,def787,def788,def789,def790,def791,def792,def793,def794,def795,def796,def797,def798,def799,def800,def801,def802,def803,def804,def805,def806,def807,def808,def809,def810,def811,def812])],[f2_sk]) ).
cnf(p12753,plain,
( ~ west(X4,X5)
| def778(X0,X1,X2,X3,X4) ),
inference(resolution,[status(thm)],[p12752,c2339]) ).
fof(f0,axiom,
! [TLH34896,TLH34897] :
( west(TLH34897,TLH34896)
<=> ( ( TLH34896 = cell100
& TLH34897 = cell90 )
| ( TLH34896 = cell99
& TLH34897 = cell89 )
| ( TLH34896 = cell98
& TLH34897 = cell88 )
| ( TLH34896 = cell97
& TLH34897 = cell87 )
| ( TLH34896 = cell96
& TLH34897 = cell86 )
| ( TLH34896 = cell95
& TLH34897 = cell85 )
| ( TLH34896 = cell94
& TLH34897 = cell84 )
| ( TLH34896 = cell93
& TLH34897 = cell83 )
| ( TLH34896 = cell92
& TLH34897 = cell82 )
| ( TLH34896 = cell91
& TLH34897 = cell81 )
| ( TLH34896 = cell90
& TLH34897 = cell80 )
| ( TLH34896 = cell89
& TLH34897 = cell79 )
| ( TLH34896 = cell88
& TLH34897 = cell78 )
| ( TLH34896 = cell87
& TLH34897 = cell77 )
| ( TLH34896 = cell86
& TLH34897 = cell76 )
| ( TLH34896 = cell85
& TLH34897 = cell75 )
| ( TLH34896 = cell84
& TLH34897 = cell74 )
| ( TLH34896 = cell83
& TLH34897 = cell73 )
| ( TLH34896 = cell82
& TLH34897 = cell72 )
| ( TLH34896 = cell81
& TLH34897 = cell71 )
| ( TLH34896 = cell80
& TLH34897 = cell70 )
| ( TLH34896 = cell79
& TLH34897 = cell69 )
| ( TLH34896 = cell78
& TLH34897 = cell68 )
| ( TLH34896 = cell77
& TLH34897 = cell67 )
| ( TLH34896 = cell76
& TLH34897 = cell66 )
| ( TLH34896 = cell75
& TLH34897 = cell65 )
| ( TLH34896 = cell74
& TLH34897 = cell64 )
| ( TLH34896 = cell73
& TLH34897 = cell63 )
| ( TLH34896 = cell72
& TLH34897 = cell62 )
| ( TLH34896 = cell71
& TLH34897 = cell61 )
| ( TLH34896 = cell70
& TLH34897 = cell60 )
| ( TLH34896 = cell69
& TLH34897 = cell59 )
| ( TLH34896 = cell68
& TLH34897 = cell58 )
| ( TLH34896 = cell67
& TLH34897 = cell57 )
| ( TLH34896 = cell66
& TLH34897 = cell56 )
| ( TLH34896 = cell65
& TLH34897 = cell55 )
| ( TLH34896 = cell64
& TLH34897 = cell54 )
| ( TLH34896 = cell63
& TLH34897 = cell53 )
| ( TLH34896 = cell62
& TLH34897 = cell52 )
| ( TLH34896 = cell61
& TLH34897 = cell51 )
| ( TLH34896 = cell60
& TLH34897 = cell50 )
| ( TLH34896 = cell59
& TLH34897 = cell49 )
| ( TLH34896 = cell58
& TLH34897 = cell48 )
| ( TLH34896 = cell57
& TLH34897 = cell47 )
| ( TLH34896 = cell56
& TLH34897 = cell46 )
| ( TLH34896 = cell55
& TLH34897 = cell45 )
| ( TLH34896 = cell54
& TLH34897 = cell44 )
| ( TLH34896 = cell53
& TLH34897 = cell43 )
| ( TLH34896 = cell52
& TLH34897 = cell42 )
| ( TLH34896 = cell51
& TLH34897 = cell41 )
| ( TLH34896 = cell50
& TLH34897 = cell40 )
| ( TLH34896 = cell49
& TLH34897 = cell39 )
| ( TLH34896 = cell48
& TLH34897 = cell38 )
| ( TLH34896 = cell47
& TLH34897 = cell37 )
| ( TLH34896 = cell46
& TLH34897 = cell36 )
| ( TLH34896 = cell45
& TLH34897 = cell35 )
| ( TLH34896 = cell44
& TLH34897 = cell34 )
| ( TLH34896 = cell43
& TLH34897 = cell33 )
| ( TLH34896 = cell42
& TLH34897 = cell32 )
| ( TLH34896 = cell41
& TLH34897 = cell31 )
| ( TLH34896 = cell40
& TLH34897 = cell30 )
| ( TLH34896 = cell39
& TLH34897 = cell29 )
| ( TLH34896 = cell38
& TLH34897 = cell28 )
| ( TLH34896 = cell37
& TLH34897 = cell27 )
| ( TLH34896 = cell36
& TLH34897 = cell26 )
| ( TLH34896 = cell35
& TLH34897 = cell25 )
| ( TLH34896 = cell34
& TLH34897 = cell24 )
| ( TLH34896 = cell33
& TLH34897 = cell23 )
| ( TLH34896 = cell32
& TLH34897 = cell22 )
| ( TLH34896 = cell31
& TLH34897 = cell21 )
| ( TLH34896 = cell30
& TLH34897 = cell20 )
| ( TLH34896 = cell29
& TLH34897 = cell19 )
| ( TLH34896 = cell28
& TLH34897 = cell18 )
| ( TLH34896 = cell27
& TLH34897 = cell17 )
| ( TLH34896 = cell26
& TLH34897 = cell16 )
| ( TLH34896 = cell25
& TLH34897 = cell15 )
| ( TLH34896 = cell24
& TLH34897 = cell14 )
| ( TLH34896 = cell23
& TLH34897 = cell13 )
| ( TLH34896 = cell22
& TLH34897 = cell12 )
| ( TLH34896 = cell21
& TLH34897 = cell11 )
| ( TLH34896 = cell20
& TLH34897 = cell10 )
| ( TLH34896 = cell19
& TLH34897 = cell9 )
| ( TLH34896 = cell18
& TLH34897 = cell8 )
| ( TLH34896 = cell17
& TLH34897 = cell7 )
| ( TLH34896 = cell16
& TLH34897 = cell6 )
| ( TLH34896 = cell15
& TLH34897 = cell5 )
| ( TLH34896 = cell14
& TLH34897 = cell4 )
| ( TLH34896 = cell13
& TLH34897 = cell3 )
| ( TLH34896 = cell12
& TLH34897 = cell2 )
| ( TLH34896 = cell11
& TLH34897 = cell1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tlhfof34975) ).
fof(f0_nnf,plain,
! [TLH34896,TLH34897] :
( ( ( ( TLH34896 != cell100
| TLH34897 != cell90 )
& ( TLH34896 != cell99
| TLH34897 != cell89 )
& ( TLH34896 != cell98
| TLH34897 != cell88 )
& ( TLH34896 != cell97
| TLH34897 != cell87 )
& ( TLH34896 != cell96
| TLH34897 != cell86 )
& ( TLH34896 != cell95
| TLH34897 != cell85 )
& ( TLH34896 != cell94
| TLH34897 != cell84 )
& ( TLH34896 != cell93
| TLH34897 != cell83 )
& ( TLH34896 != cell92
| TLH34897 != cell82 )
& ( TLH34896 != cell91
| TLH34897 != cell81 )
& ( TLH34896 != cell90
| TLH34897 != cell80 )
& ( TLH34896 != cell89
| TLH34897 != cell79 )
& ( TLH34896 != cell88
| TLH34897 != cell78 )
& ( TLH34896 != cell87
| TLH34897 != cell77 )
& ( TLH34896 != cell86
| TLH34897 != cell76 )
& ( TLH34896 != cell85
| TLH34897 != cell75 )
& ( TLH34896 != cell84
| TLH34897 != cell74 )
& ( TLH34896 != cell83
| TLH34897 != cell73 )
& ( TLH34896 != cell82
| TLH34897 != cell72 )
& ( TLH34896 != cell81
| TLH34897 != cell71 )
& ( TLH34896 != cell80
| TLH34897 != cell70 )
& ( TLH34896 != cell79
| TLH34897 != cell69 )
& ( TLH34896 != cell78
| TLH34897 != cell68 )
& ( TLH34896 != cell77
| TLH34897 != cell67 )
& ( TLH34896 != cell76
| TLH34897 != cell66 )
& ( TLH34896 != cell75
| TLH34897 != cell65 )
& ( TLH34896 != cell74
| TLH34897 != cell64 )
& ( TLH34896 != cell73
| TLH34897 != cell63 )
& ( TLH34896 != cell72
| TLH34897 != cell62 )
& ( TLH34896 != cell71
| TLH34897 != cell61 )
& ( TLH34896 != cell70
| TLH34897 != cell60 )
& ( TLH34896 != cell69
| TLH34897 != cell59 )
& ( TLH34896 != cell68
| TLH34897 != cell58 )
& ( TLH34896 != cell67
| TLH34897 != cell57 )
& ( TLH34896 != cell66
| TLH34897 != cell56 )
& ( TLH34896 != cell65
| TLH34897 != cell55 )
& ( TLH34896 != cell64
| TLH34897 != cell54 )
& ( TLH34896 != cell63
| TLH34897 != cell53 )
& ( TLH34896 != cell62
| TLH34897 != cell52 )
& ( TLH34896 != cell61
| TLH34897 != cell51 )
& ( TLH34896 != cell60
| TLH34897 != cell50 )
& ( TLH34896 != cell59
| TLH34897 != cell49 )
& ( TLH34896 != cell58
| TLH34897 != cell48 )
& ( TLH34896 != cell57
| TLH34897 != cell47 )
& ( TLH34896 != cell56
| TLH34897 != cell46 )
& ( TLH34896 != cell55
| TLH34897 != cell45 )
& ( TLH34896 != cell54
| TLH34897 != cell44 )
& ( TLH34896 != cell53
| TLH34897 != cell43 )
& ( TLH34896 != cell52
| TLH34897 != cell42 )
& ( TLH34896 != cell51
| TLH34897 != cell41 )
& ( TLH34896 != cell50
| TLH34897 != cell40 )
& ( TLH34896 != cell49
| TLH34897 != cell39 )
& ( TLH34896 != cell48
| TLH34897 != cell38 )
& ( TLH34896 != cell47
| TLH34897 != cell37 )
& ( TLH34896 != cell46
| TLH34897 != cell36 )
& ( TLH34896 != cell45
| TLH34897 != cell35 )
& ( TLH34896 != cell44
| TLH34897 != cell34 )
& ( TLH34896 != cell43
| TLH34897 != cell33 )
& ( TLH34896 != cell42
| TLH34897 != cell32 )
& ( TLH34896 != cell41
| TLH34897 != cell31 )
& ( TLH34896 != cell40
| TLH34897 != cell30 )
& ( TLH34896 != cell39
| TLH34897 != cell29 )
& ( TLH34896 != cell38
| TLH34897 != cell28 )
& ( TLH34896 != cell37
| TLH34897 != cell27 )
& ( TLH34896 != cell36
| TLH34897 != cell26 )
& ( TLH34896 != cell35
| TLH34897 != cell25 )
& ( TLH34896 != cell34
| TLH34897 != cell24 )
& ( TLH34896 != cell33
| TLH34897 != cell23 )
& ( TLH34896 != cell32
| TLH34897 != cell22 )
& ( TLH34896 != cell31
| TLH34897 != cell21 )
& ( TLH34896 != cell30
| TLH34897 != cell20 )
& ( TLH34896 != cell29
| TLH34897 != cell19 )
& ( TLH34896 != cell28
| TLH34897 != cell18 )
& ( TLH34896 != cell27
| TLH34897 != cell17 )
& ( TLH34896 != cell26
| TLH34897 != cell16 )
& ( TLH34896 != cell25
| TLH34897 != cell15 )
& ( TLH34896 != cell24
| TLH34897 != cell14 )
& ( TLH34896 != cell23
| TLH34897 != cell13 )
& ( TLH34896 != cell22
| TLH34897 != cell12 )
& ( TLH34896 != cell21
| TLH34897 != cell11 )
& ( TLH34896 != cell20
| TLH34897 != cell10 )
& ( TLH34896 != cell19
| TLH34897 != cell9 )
& ( TLH34896 != cell18
| TLH34897 != cell8 )
& ( TLH34896 != cell17
| TLH34897 != cell7 )
& ( TLH34896 != cell16
| TLH34897 != cell6 )
& ( TLH34896 != cell15
| TLH34897 != cell5 )
& ( TLH34896 != cell14
| TLH34897 != cell4 )
& ( TLH34896 != cell13
| TLH34897 != cell3 )
& ( TLH34896 != cell12
| TLH34897 != cell2 )
& ( TLH34896 != cell11
| TLH34897 != cell1 ) )
| west(TLH34897,TLH34896) )
& ( ( TLH34896 = cell100
& TLH34897 = cell90 )
| ( TLH34896 = cell99
& TLH34897 = cell89 )
| ( TLH34896 = cell98
& TLH34897 = cell88 )
| ( TLH34896 = cell97
& TLH34897 = cell87 )
| ( TLH34896 = cell96
& TLH34897 = cell86 )
| ( TLH34896 = cell95
& TLH34897 = cell85 )
| ( TLH34896 = cell94
& TLH34897 = cell84 )
| ( TLH34896 = cell93
& TLH34897 = cell83 )
| ( TLH34896 = cell92
& TLH34897 = cell82 )
| ( TLH34896 = cell91
& TLH34897 = cell81 )
| ( TLH34896 = cell90
& TLH34897 = cell80 )
| ( TLH34896 = cell89
& TLH34897 = cell79 )
| ( TLH34896 = cell88
& TLH34897 = cell78 )
| ( TLH34896 = cell87
& TLH34897 = cell77 )
| ( TLH34896 = cell86
& TLH34897 = cell76 )
| ( TLH34896 = cell85
& TLH34897 = cell75 )
| ( TLH34896 = cell84
& TLH34897 = cell74 )
| ( TLH34896 = cell83
& TLH34897 = cell73 )
| ( TLH34896 = cell82
& TLH34897 = cell72 )
| ( TLH34896 = cell81
& TLH34897 = cell71 )
| ( TLH34896 = cell80
& TLH34897 = cell70 )
| ( TLH34896 = cell79
& TLH34897 = cell69 )
| ( TLH34896 = cell78
& TLH34897 = cell68 )
| ( TLH34896 = cell77
& TLH34897 = cell67 )
| ( TLH34896 = cell76
& TLH34897 = cell66 )
| ( TLH34896 = cell75
& TLH34897 = cell65 )
| ( TLH34896 = cell74
& TLH34897 = cell64 )
| ( TLH34896 = cell73
& TLH34897 = cell63 )
| ( TLH34896 = cell72
& TLH34897 = cell62 )
| ( TLH34896 = cell71
& TLH34897 = cell61 )
| ( TLH34896 = cell70
& TLH34897 = cell60 )
| ( TLH34896 = cell69
& TLH34897 = cell59 )
| ( TLH34896 = cell68
& TLH34897 = cell58 )
| ( TLH34896 = cell67
& TLH34897 = cell57 )
| ( TLH34896 = cell66
& TLH34897 = cell56 )
| ( TLH34896 = cell65
& TLH34897 = cell55 )
| ( TLH34896 = cell64
& TLH34897 = cell54 )
| ( TLH34896 = cell63
& TLH34897 = cell53 )
| ( TLH34896 = cell62
& TLH34897 = cell52 )
| ( TLH34896 = cell61
& TLH34897 = cell51 )
| ( TLH34896 = cell60
& TLH34897 = cell50 )
| ( TLH34896 = cell59
& TLH34897 = cell49 )
| ( TLH34896 = cell58
& TLH34897 = cell48 )
| ( TLH34896 = cell57
& TLH34897 = cell47 )
| ( TLH34896 = cell56
& TLH34897 = cell46 )
| ( TLH34896 = cell55
& TLH34897 = cell45 )
| ( TLH34896 = cell54
& TLH34897 = cell44 )
| ( TLH34896 = cell53
& TLH34897 = cell43 )
| ( TLH34896 = cell52
& TLH34897 = cell42 )
| ( TLH34896 = cell51
& TLH34897 = cell41 )
| ( TLH34896 = cell50
& TLH34897 = cell40 )
| ( TLH34896 = cell49
& TLH34897 = cell39 )
| ( TLH34896 = cell48
& TLH34897 = cell38 )
| ( TLH34896 = cell47
& TLH34897 = cell37 )
| ( TLH34896 = cell46
& TLH34897 = cell36 )
| ( TLH34896 = cell45
& TLH34897 = cell35 )
| ( TLH34896 = cell44
& TLH34897 = cell34 )
| ( TLH34896 = cell43
& TLH34897 = cell33 )
| ( TLH34896 = cell42
& TLH34897 = cell32 )
| ( TLH34896 = cell41
& TLH34897 = cell31 )
| ( TLH34896 = cell40
& TLH34897 = cell30 )
| ( TLH34896 = cell39
& TLH34897 = cell29 )
| ( TLH34896 = cell38
& TLH34897 = cell28 )
| ( TLH34896 = cell37
& TLH34897 = cell27 )
| ( TLH34896 = cell36
& TLH34897 = cell26 )
| ( TLH34896 = cell35
& TLH34897 = cell25 )
| ( TLH34896 = cell34
& TLH34897 = cell24 )
| ( TLH34896 = cell33
& TLH34897 = cell23 )
| ( TLH34896 = cell32
& TLH34897 = cell22 )
| ( TLH34896 = cell31
& TLH34897 = cell21 )
| ( TLH34896 = cell30
& TLH34897 = cell20 )
| ( TLH34896 = cell29
& TLH34897 = cell19 )
| ( TLH34896 = cell28
& TLH34897 = cell18 )
| ( TLH34896 = cell27
& TLH34897 = cell17 )
| ( TLH34896 = cell26
& TLH34897 = cell16 )
| ( TLH34896 = cell25
& TLH34897 = cell15 )
| ( TLH34896 = cell24
& TLH34897 = cell14 )
| ( TLH34896 = cell23
& TLH34897 = cell13 )
| ( TLH34896 = cell22
& TLH34897 = cell12 )
| ( TLH34896 = cell21
& TLH34897 = cell11 )
| ( TLH34896 = cell20
& TLH34897 = cell10 )
| ( TLH34896 = cell19
& TLH34897 = cell9 )
| ( TLH34896 = cell18
& TLH34897 = cell8 )
| ( TLH34896 = cell17
& TLH34897 = cell7 )
| ( TLH34896 = cell16
& TLH34897 = cell6 )
| ( TLH34896 = cell15
& TLH34897 = cell5 )
| ( TLH34896 = cell14
& TLH34897 = cell4 )
| ( TLH34896 = cell13
& TLH34897 = cell3 )
| ( TLH34896 = cell12
& TLH34897 = cell2 )
| ( TLH34896 = cell11
& TLH34897 = cell1 )
| ~ west(TLH34897,TLH34896) ) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [TLH34897,TLH34896] :
( ( ( ( TLH34896 != cell100
| TLH34897 != cell90 )
& ( TLH34896 != cell99
| TLH34897 != cell89 )
& ( TLH34896 != cell98
| TLH34897 != cell88 )
& ( TLH34896 != cell97
| TLH34897 != cell87 )
& ( TLH34896 != cell96
| TLH34897 != cell86 )
& ( TLH34896 != cell95
| TLH34897 != cell85 )
& ( TLH34896 != cell94
| TLH34897 != cell84 )
& ( TLH34896 != cell93
| TLH34897 != cell83 )
& ( TLH34896 != cell92
| TLH34897 != cell82 )
& ( TLH34896 != cell91
| TLH34897 != cell81 )
& ( TLH34896 != cell90
| TLH34897 != cell80 )
& ( TLH34896 != cell89
| TLH34897 != cell79 )
& ( TLH34896 != cell88
| TLH34897 != cell78 )
& ( TLH34896 != cell87
| TLH34897 != cell77 )
& ( TLH34896 != cell86
| TLH34897 != cell76 )
& ( TLH34896 != cell85
| TLH34897 != cell75 )
& ( TLH34896 != cell84
| TLH34897 != cell74 )
& ( TLH34896 != cell83
| TLH34897 != cell73 )
& ( TLH34896 != cell82
| TLH34897 != cell72 )
& ( TLH34896 != cell81
| TLH34897 != cell71 )
& ( TLH34896 != cell80
| TLH34897 != cell70 )
& ( TLH34896 != cell79
| TLH34897 != cell69 )
& ( TLH34896 != cell78
| TLH34897 != cell68 )
& ( TLH34896 != cell77
| TLH34897 != cell67 )
& ( TLH34896 != cell76
| TLH34897 != cell66 )
& ( TLH34896 != cell75
| TLH34897 != cell65 )
& ( TLH34896 != cell74
| TLH34897 != cell64 )
& ( TLH34896 != cell73
| TLH34897 != cell63 )
& ( TLH34896 != cell72
| TLH34897 != cell62 )
& ( TLH34896 != cell71
| TLH34897 != cell61 )
& ( TLH34896 != cell70
| TLH34897 != cell60 )
& ( TLH34896 != cell69
| TLH34897 != cell59 )
& ( TLH34896 != cell68
| TLH34897 != cell58 )
& ( TLH34896 != cell67
| TLH34897 != cell57 )
& ( TLH34896 != cell66
| TLH34897 != cell56 )
& ( TLH34896 != cell65
| TLH34897 != cell55 )
& ( TLH34896 != cell64
| TLH34897 != cell54 )
& ( TLH34896 != cell63
| TLH34897 != cell53 )
& ( TLH34896 != cell62
| TLH34897 != cell52 )
& ( TLH34896 != cell61
| TLH34897 != cell51 )
& ( TLH34896 != cell60
| TLH34897 != cell50 )
& ( TLH34896 != cell59
| TLH34897 != cell49 )
& ( TLH34896 != cell58
| TLH34897 != cell48 )
& ( TLH34896 != cell57
| TLH34897 != cell47 )
& ( TLH34896 != cell56
| TLH34897 != cell46 )
& ( TLH34896 != cell55
| TLH34897 != cell45 )
& ( TLH34896 != cell54
| TLH34897 != cell44 )
& ( TLH34896 != cell53
| TLH34897 != cell43 )
& ( TLH34896 != cell52
| TLH34897 != cell42 )
& ( TLH34896 != cell51
| TLH34897 != cell41 )
& ( TLH34896 != cell50
| TLH34897 != cell40 )
& ( TLH34896 != cell49
| TLH34897 != cell39 )
& ( TLH34896 != cell48
| TLH34897 != cell38 )
& ( TLH34896 != cell47
| TLH34897 != cell37 )
& ( TLH34896 != cell46
| TLH34897 != cell36 )
& ( TLH34896 != cell45
| TLH34897 != cell35 )
& ( TLH34896 != cell44
| TLH34897 != cell34 )
& ( TLH34896 != cell43
| TLH34897 != cell33 )
& ( TLH34896 != cell42
| TLH34897 != cell32 )
& ( TLH34896 != cell41
| TLH34897 != cell31 )
& ( TLH34896 != cell40
| TLH34897 != cell30 )
& ( TLH34896 != cell39
| TLH34897 != cell29 )
& ( TLH34896 != cell38
| TLH34897 != cell28 )
& ( TLH34896 != cell37
| TLH34897 != cell27 )
& ( TLH34896 != cell36
| TLH34897 != cell26 )
& ( TLH34896 != cell35
| TLH34897 != cell25 )
& ( TLH34896 != cell34
| TLH34897 != cell24 )
& ( TLH34896 != cell33
| TLH34897 != cell23 )
& ( TLH34896 != cell32
| TLH34897 != cell22 )
& ( TLH34896 != cell31
| TLH34897 != cell21 )
& ( TLH34896 != cell30
| TLH34897 != cell20 )
& ( TLH34896 != cell29
| TLH34897 != cell19 )
& ( TLH34896 != cell28
| TLH34897 != cell18 )
& ( TLH34896 != cell27
| TLH34897 != cell17 )
& ( TLH34896 != cell26
| TLH34897 != cell16 )
& ( TLH34896 != cell25
| TLH34897 != cell15 )
& ( TLH34896 != cell24
| TLH34897 != cell14 )
& ( TLH34896 != cell23
| TLH34897 != cell13 )
& ( TLH34896 != cell22
| TLH34897 != cell12 )
& ( TLH34896 != cell21
| TLH34897 != cell11 )
& ( TLH34896 != cell20
| TLH34897 != cell10 )
& ( TLH34896 != cell19
| TLH34897 != cell9 )
& ( TLH34896 != cell18
| TLH34897 != cell8 )
& ( TLH34896 != cell17
| TLH34897 != cell7 )
& ( TLH34896 != cell16
| TLH34897 != cell6 )
& ( TLH34896 != cell15
| TLH34897 != cell5 )
& ( TLH34896 != cell14
| TLH34897 != cell4 )
& ( TLH34896 != cell13
| TLH34897 != cell3 )
& ( TLH34896 != cell12
| TLH34897 != cell2 )
& ( TLH34896 != cell11
| TLH34897 != cell1 ) )
| west(TLH34897,TLH34896) )
& ( ( TLH34896 = cell100
& TLH34897 = cell90 )
| ( TLH34896 = cell99
& TLH34897 = cell89 )
| ( TLH34896 = cell98
& TLH34897 = cell88 )
| ( TLH34896 = cell97
& TLH34897 = cell87 )
| ( TLH34896 = cell96
& TLH34897 = cell86 )
| ( TLH34896 = cell95
& TLH34897 = cell85 )
| ( TLH34896 = cell94
& TLH34897 = cell84 )
| ( TLH34896 = cell93
& TLH34897 = cell83 )
| ( TLH34896 = cell92
& TLH34897 = cell82 )
| ( TLH34896 = cell91
& TLH34897 = cell81 )
| ( TLH34896 = cell90
& TLH34897 = cell80 )
| ( TLH34896 = cell89
& TLH34897 = cell79 )
| ( TLH34896 = cell88
& TLH34897 = cell78 )
| ( TLH34896 = cell87
& TLH34897 = cell77 )
| ( TLH34896 = cell86
& TLH34897 = cell76 )
| ( TLH34896 = cell85
& TLH34897 = cell75 )
| ( TLH34896 = cell84
& TLH34897 = cell74 )
| ( TLH34896 = cell83
& TLH34897 = cell73 )
| ( TLH34896 = cell82
& TLH34897 = cell72 )
| ( TLH34896 = cell81
& TLH34897 = cell71 )
| ( TLH34896 = cell80
& TLH34897 = cell70 )
| ( TLH34896 = cell79
& TLH34897 = cell69 )
| ( TLH34896 = cell78
& TLH34897 = cell68 )
| ( TLH34896 = cell77
& TLH34897 = cell67 )
| ( TLH34896 = cell76
& TLH34897 = cell66 )
| ( TLH34896 = cell75
& TLH34897 = cell65 )
| ( TLH34896 = cell74
& TLH34897 = cell64 )
| ( TLH34896 = cell73
& TLH34897 = cell63 )
| ( TLH34896 = cell72
& TLH34897 = cell62 )
| ( TLH34896 = cell71
& TLH34897 = cell61 )
| ( TLH34896 = cell70
& TLH34897 = cell60 )
| ( TLH34896 = cell69
& TLH34897 = cell59 )
| ( TLH34896 = cell68
& TLH34897 = cell58 )
| ( TLH34896 = cell67
& TLH34897 = cell57 )
| ( TLH34896 = cell66
& TLH34897 = cell56 )
| ( TLH34896 = cell65
& TLH34897 = cell55 )
| ( TLH34896 = cell64
& TLH34897 = cell54 )
| ( TLH34896 = cell63
& TLH34897 = cell53 )
| ( TLH34896 = cell62
& TLH34897 = cell52 )
| ( TLH34896 = cell61
& TLH34897 = cell51 )
| ( TLH34896 = cell60
& TLH34897 = cell50 )
| ( TLH34896 = cell59
& TLH34897 = cell49 )
| ( TLH34896 = cell58
& TLH34897 = cell48 )
| ( TLH34896 = cell57
& TLH34897 = cell47 )
| ( TLH34896 = cell56
& TLH34897 = cell46 )
| ( TLH34896 = cell55
& TLH34897 = cell45 )
| ( TLH34896 = cell54
& TLH34897 = cell44 )
| ( TLH34896 = cell53
& TLH34897 = cell43 )
| ( TLH34896 = cell52
& TLH34897 = cell42 )
| ( TLH34896 = cell51
& TLH34897 = cell41 )
| ( TLH34896 = cell50
& TLH34897 = cell40 )
| ( TLH34896 = cell49
& TLH34897 = cell39 )
| ( TLH34896 = cell48
& TLH34897 = cell38 )
| ( TLH34896 = cell47
& TLH34897 = cell37 )
| ( TLH34896 = cell46
& TLH34897 = cell36 )
| ( TLH34896 = cell45
& TLH34897 = cell35 )
| ( TLH34896 = cell44
& TLH34897 = cell34 )
| ( TLH34896 = cell43
& TLH34897 = cell33 )
| ( TLH34896 = cell42
& TLH34897 = cell32 )
| ( TLH34896 = cell41
& TLH34897 = cell31 )
| ( TLH34896 = cell40
& TLH34897 = cell30 )
| ( TLH34896 = cell39
& TLH34897 = cell29 )
| ( TLH34896 = cell38
& TLH34897 = cell28 )
| ( TLH34896 = cell37
& TLH34897 = cell27 )
| ( TLH34896 = cell36
& TLH34897 = cell26 )
| ( TLH34896 = cell35
& TLH34897 = cell25 )
| ( TLH34896 = cell34
& TLH34897 = cell24 )
| ( TLH34896 = cell33
& TLH34897 = cell23 )
| ( TLH34896 = cell32
& TLH34897 = cell22 )
| ( TLH34896 = cell31
& TLH34897 = cell21 )
| ( TLH34896 = cell30
& TLH34897 = cell20 )
| ( TLH34896 = cell29
& TLH34897 = cell19 )
| ( TLH34896 = cell28
& TLH34897 = cell18 )
| ( TLH34896 = cell27
& TLH34897 = cell17 )
| ( TLH34896 = cell26
& TLH34897 = cell16 )
| ( TLH34896 = cell25
& TLH34897 = cell15 )
| ( TLH34896 = cell24
& TLH34897 = cell14 )
| ( TLH34896 = cell23
& TLH34897 = cell13 )
| ( TLH34896 = cell22
& TLH34897 = cell12 )
| ( TLH34896 = cell21
& TLH34897 = cell11 )
| ( TLH34896 = cell20
& TLH34897 = cell10 )
| ( TLH34896 = cell19
& TLH34897 = cell9 )
| ( TLH34896 = cell18
& TLH34897 = cell8 )
| ( TLH34896 = cell17
& TLH34897 = cell7 )
| ( TLH34896 = cell16
& TLH34897 = cell6 )
| ( TLH34896 = cell15
& TLH34897 = cell5 )
| ( TLH34896 = cell14
& TLH34897 = cell4 )
| ( TLH34896 = cell13
& TLH34897 = cell3 )
| ( TLH34896 = cell12
& TLH34897 = cell2 )
| ( TLH34896 = cell11
& TLH34897 = cell1 )
| ~ west(TLH34897,TLH34896) ) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c1077,plain,
( def358(X1,X0)
| west(X1,X0)
| ~ def359(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(c1081,plain,
( def359(X1,X0)
| ~ def360(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(c1083,plain,
def360(X1,X0),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p2536,plain,
def359(X0,X1),
inference(resolution,[status(thm)],[c1081,c1083]) ).
cnf(p2687,plain,
( def358(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[c1077,p2536]) ).
cnf(c1075,plain,
( def357(X1,X0)
| ~ def358(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p5087,plain,
( def357(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p2687,c1075]) ).
cnf(c1071,plain,
( X0 != cell100
| X1 != cell90
| ~ def357(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p2685,plain,
( X0 != cell100
| ~ def357(cell90,X0) ),
inference(equality_resolution,[status(thm)],[c1071]) ).
cnf(p5085,plain,
~ def357(cell90,cell100),
inference(equality_resolution,[status(thm)],[p2685]) ).
cnf(p7118,plain,
west(cell90,cell100),
inference(resolution,[status(thm)],[p5087,p5085]) ).
cnf(p12754,plain,
def778(X0,X1,X2,X3,cell90),
inference(resolution,[status(thm)],[p12753,p7118]) ).
cnf(c2336,plain,
( ~ west(X10,X11)
| def777(X1,X8,X9,X10)
| ~ def778(X1,X8,X9,X10,X11) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def722,def723,def724,def725,def726,def727,def728,def729,def730,def731,def732,def733,def734,def735,def736,def737,def738,def739,def740,def741,def742,def743,def744,def745,def746,def747,def748,def749,def750,def751,def752,def753,def754,def755,def756,def757,def758,def759,def760,def761,def762,def763,def764,def765,def766,def767,def768,def769,def770,def771,def772,def773,def774,def775,def776,def777,def778,def779,def780,def781,def782,def783,def784,def785,def786,def787,def788,def789,def790,def791,def792,def793,def794,def795,def796,def797,def798,def799,def800,def801,def802,def803,def804,def805,def806,def807,def808,def809,def810,def811,def812])],[f2_sk]) ).
cnf(p12803,plain,
( ~ west(X3,cell90)
| def777(X0,X1,X2,X3) ),
inference(resolution,[status(thm)],[p12754,c2336]) ).
cnf(c1074,plain,
( def356(X1,X0)
| ~ def358(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p5086,plain,
( def356(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p2687,c1074]) ).
cnf(c1068,plain,
( def354(X1,X0)
| ~ def356(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p7111,plain,
( def354(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p5086,c1068]) ).
cnf(c1062,plain,
( def352(X1,X0)
| ~ def354(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p7275,plain,
( def352(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p7111,c1062]) ).
cnf(c1056,plain,
( def350(X1,X0)
| ~ def352(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p7309,plain,
( def350(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p7275,c1056]) ).
cnf(c1050,plain,
( def348(X1,X0)
| ~ def350(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p7354,plain,
( def348(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p7309,c1050]) ).
cnf(c1044,plain,
( def346(X1,X0)
| ~ def348(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p7395,plain,
( def346(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p7354,c1044]) ).
cnf(c1038,plain,
( def344(X1,X0)
| ~ def346(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p7430,plain,
( def344(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p7395,c1038]) ).
cnf(c1032,plain,
( def342(X1,X0)
| ~ def344(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p7464,plain,
( def342(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p7430,c1032]) ).
cnf(c1026,plain,
( def340(X1,X0)
| ~ def342(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p7497,plain,
( def340(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p7464,c1026]) ).
cnf(c1020,plain,
( def338(X1,X0)
| ~ def340(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p7531,plain,
( def338(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p7497,c1020]) ).
cnf(c1015,plain,
( def337(X1,X0)
| ~ def338(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p7569,plain,
( def337(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p7531,c1015]) ).
cnf(c1011,plain,
( X0 != cell90
| X1 != cell80
| ~ def337(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p2665,plain,
( X0 != cell90
| ~ def337(cell80,X0) ),
inference(equality_resolution,[status(thm)],[c1011]) ).
cnf(p5075,plain,
~ def337(cell80,cell90),
inference(equality_resolution,[status(thm)],[p2665]) ).
cnf(p7606,plain,
west(cell80,cell90),
inference(resolution,[status(thm)],[p7569,p5075]) ).
cnf(p12872,plain,
def777(X0,X1,X2,cell80),
inference(resolution,[status(thm)],[p12803,p7606]) ).
cnf(c2333,plain,
( ~ west(X9,X10)
| def776(X1,X8,X9)
| ~ def777(X1,X8,X9,X10) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def722,def723,def724,def725,def726,def727,def728,def729,def730,def731,def732,def733,def734,def735,def736,def737,def738,def739,def740,def741,def742,def743,def744,def745,def746,def747,def748,def749,def750,def751,def752,def753,def754,def755,def756,def757,def758,def759,def760,def761,def762,def763,def764,def765,def766,def767,def768,def769,def770,def771,def772,def773,def774,def775,def776,def777,def778,def779,def780,def781,def782,def783,def784,def785,def786,def787,def788,def789,def790,def791,def792,def793,def794,def795,def796,def797,def798,def799,def800,def801,def802,def803,def804,def805,def806,def807,def808,def809,def810,def811,def812])],[f2_sk]) ).
cnf(p12875,plain,
( ~ west(X2,cell80)
| def776(X0,X1,X2) ),
inference(resolution,[status(thm)],[p12872,c2333]) ).
cnf(c1014,plain,
( def336(X1,X0)
| ~ def338(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p7568,plain,
( def336(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p7531,c1014]) ).
cnf(c1008,plain,
( def334(X1,X0)
| ~ def336(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p7602,plain,
( def334(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p7568,c1008]) ).
cnf(c1002,plain,
( def332(X1,X0)
| ~ def334(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p7635,plain,
( def332(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p7602,c1002]) ).
cnf(c996,plain,
( def330(X1,X0)
| ~ def332(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p7669,plain,
( def330(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p7635,c996]) ).
cnf(c990,plain,
( def328(X1,X0)
| ~ def330(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p7700,plain,
( def328(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p7669,c990]) ).
cnf(c984,plain,
( def326(X1,X0)
| ~ def328(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p7732,plain,
( def326(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p7700,c984]) ).
cnf(c978,plain,
( def324(X1,X0)
| ~ def326(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p7769,plain,
( def324(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p7732,c978]) ).
cnf(c972,plain,
( def322(X1,X0)
| ~ def324(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p7805,plain,
( def322(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p7769,c972]) ).
cnf(c966,plain,
( def320(X1,X0)
| ~ def322(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p7841,plain,
( def320(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p7805,c966]) ).
cnf(c960,plain,
( def318(X1,X0)
| ~ def320(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p7879,plain,
( def318(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p7841,c960]) ).
cnf(c955,plain,
( def317(X1,X0)
| ~ def318(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p7922,plain,
( def317(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p7879,c955]) ).
cnf(c951,plain,
( X0 != cell80
| X1 != cell70
| ~ def317(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p2645,plain,
( X0 != cell80
| ~ def317(cell70,X0) ),
inference(equality_resolution,[status(thm)],[c951]) ).
cnf(p5065,plain,
~ def317(cell70,cell80),
inference(equality_resolution,[status(thm)],[p2645]) ).
cnf(p7963,plain,
west(cell70,cell80),
inference(resolution,[status(thm)],[p7922,p5065]) ).
cnf(p12877,plain,
def776(X0,X1,cell70),
inference(resolution,[status(thm)],[p12875,p7963]) ).
cnf(c2330,plain,
( ~ west(X8,X9)
| ~ west(X1,X8)
| ~ def776(X1,X8,X9) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def722,def723,def724,def725,def726,def727,def728,def729,def730,def731,def732,def733,def734,def735,def736,def737,def738,def739,def740,def741,def742,def743,def744,def745,def746,def747,def748,def749,def750,def751,def752,def753,def754,def755,def756,def757,def758,def759,def760,def761,def762,def763,def764,def765,def766,def767,def768,def769,def770,def771,def772,def773,def774,def775,def776,def777,def778,def779,def780,def781,def782,def783,def784,def785,def786,def787,def788,def789,def790,def791,def792,def793,def794,def795,def796,def797,def798,def799,def800,def801,def802,def803,def804,def805,def806,def807,def808,def809,def810,def811,def812])],[f2_sk]) ).
cnf(p12878,plain,
( ~ west(X1,cell70)
| ~ west(X0,X1) ),
inference(resolution,[status(thm)],[p12877,c2330]) ).
cnf(c954,plain,
( def316(X1,X0)
| ~ def318(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p7921,plain,
( def316(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p7879,c954]) ).
cnf(c948,plain,
( def314(X1,X0)
| ~ def316(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p7959,plain,
( def314(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p7921,c948]) ).
cnf(c942,plain,
( def312(X1,X0)
| ~ def314(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p7990,plain,
( def312(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p7959,c942]) ).
cnf(c936,plain,
( def310(X1,X0)
| ~ def312(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p8022,plain,
( def310(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p7990,c936]) ).
cnf(c930,plain,
( def308(X1,X0)
| ~ def310(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p8053,plain,
( def308(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p8022,c930]) ).
cnf(c924,plain,
( def306(X1,X0)
| ~ def308(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p8085,plain,
( def306(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p8053,c924]) ).
cnf(c918,plain,
( def304(X1,X0)
| ~ def306(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p8133,plain,
( def304(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p8085,c918]) ).
cnf(c912,plain,
( def302(X1,X0)
| ~ def304(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p8178,plain,
( def302(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p8133,c912]) ).
cnf(c906,plain,
( def300(X1,X0)
| ~ def302(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p8211,plain,
( def300(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p8178,c906]) ).
cnf(c900,plain,
( def298(X1,X0)
| ~ def300(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p8243,plain,
( def298(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p8211,c900]) ).
cnf(c894,plain,
( def296(X1,X0)
| ~ def298(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p8275,plain,
( def296(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p8243,c894]) ).
cnf(c888,plain,
( def294(X1,X0)
| ~ def296(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p8306,plain,
( def294(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p8275,c888]) ).
cnf(c882,plain,
( def292(X1,X0)
| ~ def294(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p8337,plain,
( def292(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p8306,c882]) ).
cnf(c876,plain,
( def290(X1,X0)
| ~ def292(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p8387,plain,
( def290(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p8337,c876]) ).
cnf(c870,plain,
( def288(X1,X0)
| ~ def290(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p8431,plain,
( def288(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p8387,c870]) ).
cnf(c864,plain,
( def286(X1,X0)
| ~ def288(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p8483,plain,
( def286(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p8431,c864]) ).
cnf(c858,plain,
( def284(X1,X0)
| ~ def286(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p8525,plain,
( def284(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p8483,c858]) ).
cnf(c852,plain,
( def282(X1,X0)
| ~ def284(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p8570,plain,
( def282(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p8525,c852]) ).
cnf(c846,plain,
( def280(X1,X0)
| ~ def282(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p8615,plain,
( def280(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p8570,c846]) ).
cnf(c840,plain,
( def278(X1,X0)
| ~ def280(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p8657,plain,
( def278(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p8615,c840]) ).
cnf(c835,plain,
( def277(X1,X0)
| ~ def278(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p8697,plain,
( def277(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p8657,c835]) ).
cnf(c831,plain,
( X0 != cell60
| X1 != cell50
| ~ def277(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p2605,plain,
( X0 != cell60
| ~ def277(cell50,X0) ),
inference(equality_resolution,[status(thm)],[c831]) ).
cnf(p5045,plain,
~ def277(cell50,cell60),
inference(equality_resolution,[status(thm)],[p2605]) ).
cnf(p8740,plain,
west(cell50,cell60),
inference(resolution,[status(thm)],[p8697,p5045]) ).
cnf(p12923,plain,
~ west(cell60,cell70),
inference(resolution,[status(thm)],[p12878,p8740]) ).
cnf(c895,plain,
( def297(X1,X0)
| ~ def298(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p8276,plain,
( def297(X0,X1)
| west(X0,X1) ),
inference(resolution,[status(thm)],[p8243,c895]) ).
cnf(c891,plain,
( X0 != cell70
| X1 != cell60
| ~ def297(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360])],[f0_sk]) ).
cnf(p2625,plain,
( X0 != cell70
| ~ def297(cell60,X0) ),
inference(equality_resolution,[status(thm)],[c891]) ).
cnf(p5055,plain,
~ def297(cell60,cell70),
inference(equality_resolution,[status(thm)],[p2625]) ).
cnf(p8310,plain,
west(cell60,cell70),
inference(resolution,[status(thm)],[p8276,p5055]) ).
cnf(p12950,plain,
$false,
inference(resolution,[status(thm)],[p12923,p8310]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : PUZ077+1 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.05 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.12/0.39 % Computer : n003.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Thu Sep 24 06:58:05 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 11.61/1.97 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.61/1.97 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------