%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : NLP009+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n008.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:14:27 PM UTC 2026
% Result : Theorem 49.02s 6.70s
% Output : Proof 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 201
% Number of leaves : 1
% Syntax : Number of formulae : 483 ( 59 unt; 0 def)
% Number of atoms : 1610 ( 176 equ)
% Maximal formula atoms : 112 ( 3 avg)
% Number of connectives : 1556 ( 429 ~; 793 |; 330 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 76 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 133 ( 131 usr; 55 prp; 0-18 aty)
% Number of functors : 18 ( 18 usr; 18 con; 0-0 aty)
% Number of variables : 1347 ( 852 sgn 36 !; 90 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f0,conjecture,
( ( ? [X13,X14,X15,X16,X17,X18,X19,X20,X21] :
( in(X21,X19)
& X18 = X21
& in(X20,X19)
& X17 = X20
& young(X18)
& man(X18)
& fellow(X18)
& young(X17)
& man(X17)
& fellow(X17)
& X17 != X18
& front(X19)
& furniture(X19)
& seat(X19)
& in(X14,X13)
& down(X14,X16)
& barrel(X14,X15)
& lonely(X16)
& way(X16)
& street(X16)
& old(X15)
& dirty(X15)
& white(X15)
& car(X15)
& chevy(X15)
& event(X14)
& city(X13)
& hollywood(X13) )
=> ? [X22,X23,X24,X25,X26,X27,X28,X29,X30] :
( in(X30,X28)
& X27 = X30
& in(X29,X28)
& X26 = X29
& young(X27)
& man(X27)
& fellow(X27)
& young(X26)
& man(X26)
& fellow(X26)
& X26 != X27
& front(X28)
& furniture(X28)
& seat(X28)
& in(X23,X22)
& down(X23,X24)
& barrel(X23,X25)
& old(X25)
& dirty(X25)
& white(X25)
& car(X25)
& chevy(X25)
& lonely(X24)
& way(X24)
& street(X24)
& event(X23)
& city(X22)
& hollywood(X22) ) )
& ( ? [U,V,W,X,Y,Z,X1,X2,X3] :
( in(X3,X1)
& Z = X3
& in(X2,X1)
& Y = X2
& young(Z)
& man(Z)
& fellow(Z)
& young(Y)
& man(Y)
& fellow(Y)
& Y != Z
& front(X1)
& furniture(X1)
& seat(X1)
& in(V,U)
& down(V,W)
& barrel(V,X)
& old(X)
& dirty(X)
& white(X)
& car(X)
& chevy(X)
& lonely(W)
& way(W)
& street(W)
& event(V)
& city(U)
& hollywood(U) )
=> ? [X4,X5,X6,X7,X8,X9,X10,X11,X12] :
( in(X12,X10)
& X9 = X12
& in(X11,X10)
& X8 = X11
& young(X9)
& man(X9)
& fellow(X9)
& young(X8)
& man(X8)
& fellow(X8)
& X8 != X9
& front(X10)
& furniture(X10)
& seat(X10)
& in(X5,X4)
& down(X5,X7)
& barrel(X5,X6)
& lonely(X7)
& way(X7)
& street(X7)
& old(X6)
& dirty(X6)
& white(X6)
& car(X6)
& chevy(X6)
& event(X5)
& city(X4)
& hollywood(X4) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f0_neg,negated_conjecture,
~ ( ( ? [X13,X14,X15,X16,X17,X18,X19,X20,X21] :
( in(X21,X19)
& X18 = X21
& in(X20,X19)
& X17 = X20
& young(X18)
& man(X18)
& fellow(X18)
& young(X17)
& man(X17)
& fellow(X17)
& X17 != X18
& front(X19)
& furniture(X19)
& seat(X19)
& in(X14,X13)
& down(X14,X16)
& barrel(X14,X15)
& lonely(X16)
& way(X16)
& street(X16)
& old(X15)
& dirty(X15)
& white(X15)
& car(X15)
& chevy(X15)
& event(X14)
& city(X13)
& hollywood(X13) )
=> ? [X22,X23,X24,X25,X26,X27,X28,X29,X30] :
( in(X30,X28)
& X27 = X30
& in(X29,X28)
& X26 = X29
& young(X27)
& man(X27)
& fellow(X27)
& young(X26)
& man(X26)
& fellow(X26)
& X26 != X27
& front(X28)
& furniture(X28)
& seat(X28)
& in(X23,X22)
& down(X23,X24)
& barrel(X23,X25)
& old(X25)
& dirty(X25)
& white(X25)
& car(X25)
& chevy(X25)
& lonely(X24)
& way(X24)
& street(X24)
& event(X23)
& city(X22)
& hollywood(X22) ) )
& ( ? [U,V,W,X,Y,Z,X1,X2,X3] :
( in(X3,X1)
& Z = X3
& in(X2,X1)
& Y = X2
& young(Z)
& man(Z)
& fellow(Z)
& young(Y)
& man(Y)
& fellow(Y)
& Y != Z
& front(X1)
& furniture(X1)
& seat(X1)
& in(V,U)
& down(V,W)
& barrel(V,X)
& old(X)
& dirty(X)
& white(X)
& car(X)
& chevy(X)
& lonely(W)
& way(W)
& street(W)
& event(V)
& city(U)
& hollywood(U) )
=> ? [X4,X5,X6,X7,X8,X9,X10,X11,X12] :
( in(X12,X10)
& X9 = X12
& in(X11,X10)
& X8 = X11
& young(X9)
& man(X9)
& fellow(X9)
& young(X8)
& man(X8)
& fellow(X8)
& X8 != X9
& front(X10)
& furniture(X10)
& seat(X10)
& in(X5,X4)
& down(X5,X7)
& barrel(X5,X6)
& lonely(X7)
& way(X7)
& street(X7)
& old(X6)
& dirty(X6)
& white(X6)
& car(X6)
& chevy(X6)
& event(X5)
& city(X4)
& hollywood(X4) ) ) ),
inference(negated_conjecture,[status(cth)],[f0]) ).
fof(f0_nnf,plain,
( ( ! [X22,X23,X24,X25,X26,X27,X28,X29,X30] :
( ~ in(X30,X28)
| X27 != X30
| ~ in(X29,X28)
| X26 != X29
| ~ young(X27)
| ~ man(X27)
| ~ fellow(X27)
| ~ young(X26)
| ~ man(X26)
| ~ fellow(X26)
| X26 = X27
| ~ front(X28)
| ~ furniture(X28)
| ~ seat(X28)
| ~ in(X23,X22)
| ~ down(X23,X24)
| ~ barrel(X23,X25)
| ~ old(X25)
| ~ dirty(X25)
| ~ white(X25)
| ~ car(X25)
| ~ chevy(X25)
| ~ lonely(X24)
| ~ way(X24)
| ~ street(X24)
| ~ event(X23)
| ~ city(X22)
| ~ hollywood(X22) )
& ? [X13,X14,X15,X16,X17,X18,X19,X20,X21] :
( in(X21,X19)
& X18 = X21
& in(X20,X19)
& X17 = X20
& young(X18)
& man(X18)
& fellow(X18)
& young(X17)
& man(X17)
& fellow(X17)
& X17 != X18
& front(X19)
& furniture(X19)
& seat(X19)
& in(X14,X13)
& down(X14,X16)
& barrel(X14,X15)
& lonely(X16)
& way(X16)
& street(X16)
& old(X15)
& dirty(X15)
& white(X15)
& car(X15)
& chevy(X15)
& event(X14)
& city(X13)
& hollywood(X13) ) )
| ( ! [X4,X5,X6,X7,X8,X9,X10,X11,X12] :
( ~ in(X12,X10)
| X9 != X12
| ~ in(X11,X10)
| X8 != X11
| ~ young(X9)
| ~ man(X9)
| ~ fellow(X9)
| ~ young(X8)
| ~ man(X8)
| ~ fellow(X8)
| X8 = X9
| ~ front(X10)
| ~ furniture(X10)
| ~ seat(X10)
| ~ in(X5,X4)
| ~ down(X5,X7)
| ~ barrel(X5,X6)
| ~ lonely(X7)
| ~ way(X7)
| ~ street(X7)
| ~ old(X6)
| ~ dirty(X6)
| ~ white(X6)
| ~ car(X6)
| ~ chevy(X6)
| ~ event(X5)
| ~ city(X4)
| ~ hollywood(X4) )
& ? [U,V,W,X,Y,Z,X1,X2,X3] :
( in(X3,X1)
& Z = X3
& in(X2,X1)
& Y = X2
& young(Z)
& man(Z)
& fellow(Z)
& young(Y)
& man(Y)
& fellow(Y)
& Y != Z
& front(X1)
& furniture(X1)
& seat(X1)
& in(V,U)
& down(V,W)
& barrel(V,X)
& old(X)
& dirty(X)
& white(X)
& car(X)
& chevy(X)
& lonely(W)
& way(W)
& street(W)
& event(V)
& city(U)
& hollywood(U) ) ) ),
inference(nnf_transformation,[status(thm)],[f0_neg]) ).
fof(f0_sk,plain,
! [X4,X5,X6,X7,X10,X8,X9,X11,X12,X22,X23,X24,X25,X28,X26,X27,X29,X30] :
( ( ( ~ in(X30,X28)
| X27 != X30
| ~ in(X29,X28)
| X26 != X29
| ~ young(X27)
| ~ man(X27)
| ~ fellow(X27)
| ~ young(X26)
| ~ man(X26)
| ~ fellow(X26)
| X26 = X27
| ~ front(X28)
| ~ furniture(X28)
| ~ seat(X28)
| ~ in(X23,X22)
| ~ down(X23,X24)
| ~ barrel(X23,X25)
| ~ old(X25)
| ~ dirty(X25)
| ~ white(X25)
| ~ car(X25)
| ~ chevy(X25)
| ~ lonely(X24)
| ~ way(X24)
| ~ street(X24)
| ~ event(X23)
| ~ city(X22)
| ~ hollywood(X22) )
& in(sk17,sk15)
& sk14 = sk17
& in(sk16,sk15)
& sk13 = sk16
& young(sk14)
& man(sk14)
& fellow(sk14)
& young(sk13)
& man(sk13)
& fellow(sk13)
& sk13 != sk14
& front(sk15)
& furniture(sk15)
& seat(sk15)
& in(sk10,sk9)
& down(sk10,sk12)
& barrel(sk10,sk11)
& lonely(sk12)
& way(sk12)
& street(sk12)
& old(sk11)
& dirty(sk11)
& white(sk11)
& car(sk11)
& chevy(sk11)
& event(sk10)
& city(sk9)
& hollywood(sk9) )
| ( ( ~ in(X12,X10)
| X9 != X12
| ~ in(X11,X10)
| X8 != X11
| ~ young(X9)
| ~ man(X9)
| ~ fellow(X9)
| ~ young(X8)
| ~ man(X8)
| ~ fellow(X8)
| X8 = X9
| ~ front(X10)
| ~ furniture(X10)
| ~ seat(X10)
| ~ in(X5,X4)
| ~ down(X5,X7)
| ~ barrel(X5,X6)
| ~ lonely(X7)
| ~ way(X7)
| ~ street(X7)
| ~ old(X6)
| ~ dirty(X6)
| ~ white(X6)
| ~ car(X6)
| ~ chevy(X6)
| ~ event(X5)
| ~ city(X4)
| ~ hollywood(X4) )
& in(sk8,sk6)
& sk5 = sk8
& in(sk7,sk6)
& sk4 = sk7
& young(sk5)
& man(sk5)
& fellow(sk5)
& young(sk4)
& man(sk4)
& fellow(sk4)
& sk4 != sk5
& front(sk6)
& furniture(sk6)
& seat(sk6)
& in(sk1,sk0)
& down(sk1,sk2)
& barrel(sk1,sk3)
& old(sk3)
& dirty(sk3)
& white(sk3)
& car(sk3)
& chevy(sk3)
& lonely(sk2)
& way(sk2)
& street(sk2)
& event(sk1)
& city(sk0)
& hollywood(sk0) ) ),
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])],[f0_nnf]) ).
cnf(c330,plain,
( def109(X27,X28,X29,X30,X33,X31,X32,X34,X35)
| def54(X9,X10,X11,X12,X15,X13,X14,X16,X17)
| ~ def110(X9,X10,X11,X12,X15,X13,X14,X16,X17,X27,X28,X29,X30,X33,X31,X32,X34,X35) ),
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])],[f0_sk]) ).
cnf(c333,plain,
def110(X9,X10,X11,X12,X15,X13,X14,X16,X17,X27,X28,X29,X30,X33,X31,X32,X34,X35),
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])],[f0_sk]) ).
cnf(p1094,plain,
( def109(X9,X10,X11,X12,X13,X14,X15,X16,X17)
| def54(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
inference(resolution,[status(thm)],[c330,c333]) ).
cnf(c162,plain,
( def26
| ~ def54(X9,X10,X11,X12,X15,X13,X14,X16,X17) ),
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])],[f0_sk]) ).
cnf(p1095,plain,
( def26
| def109(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
inference(resolution,[status(thm)],[p1094,c162]) ).
cnf(c327,plain,
( def81
| ~ def109(X27,X28,X29,X30,X33,X31,X32,X34,X35) ),
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])],[f0_sk]) ).
cnf(p1099,plain,
( def81
| def26 ),
inference(resolution,[status(thm)],[p1095,c327]) ).
cnf(c243,plain,
( def80
| ~ def81 ),
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])],[f0_sk]) ).
cnf(p1101,plain,
( def80
| def26 ),
inference(resolution,[status(thm)],[p1099,c243]) ).
cnf(c240,plain,
( def79
| ~ def80 ),
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])],[f0_sk]) ).
cnf(p1103,plain,
( def79
| def26 ),
inference(resolution,[status(thm)],[p1101,c240]) ).
cnf(c237,plain,
( def78
| ~ def79 ),
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])],[f0_sk]) ).
cnf(p1105,plain,
( def78
| def26 ),
inference(resolution,[status(thm)],[p1103,c237]) ).
cnf(c235,plain,
( sk13 = sk16
| ~ def78 ),
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])],[f0_sk]) ).
cnf(p1108,plain,
( sk13 = sk16
| def26 ),
inference(resolution,[status(thm)],[p1105,c235]) ).
cnf(c241,plain,
( sk14 = sk17
| ~ def80 ),
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])],[f0_sk]) ).
cnf(p1104,plain,
( sk14 = sk17
| def26 ),
inference(resolution,[status(thm)],[p1101,c241]) ).
cnf(c328,plain,
( def108(X27,X28,X29,X30,X33,X31,X32,X34,X35)
| ~ def109(X27,X28,X29,X30,X33,X31,X32,X34,X35) ),
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])],[f0_sk]) ).
cnf(p1100,plain,
( def108(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| def26 ),
inference(resolution,[status(thm)],[p1095,c328]) ).
cnf(c324,plain,
( ~ in(X35,X33)
| def107(X27,X28,X29,X30,X33,X31,X32,X34,X35)
| ~ def108(X27,X28,X29,X30,X33,X31,X32,X34,X35) ),
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])],[f0_sk]) ).
cnf(p1200,plain,
( ~ in(X8,X4)
| def107(X0,X1,X2,X3,X4,X5,X6,X7,X8)
| def26 ),
inference(resolution,[status(thm)],[p1100,c324]) ).
cnf(c244,plain,
( in(sk17,sk15)
| ~ def81 ),
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])],[f0_sk]) ).
cnf(p1102,plain,
( in(sk17,sk15)
| def26 ),
inference(resolution,[status(thm)],[p1099,c244]) ).
cnf(p1204,plain,
( def26
| def107(X0,X1,X2,X3,sk15,X4,X5,X6,sk17)
| def26 ),
inference(resolution,[status(thm)],[p1200,p1102]) ).
cnf(p1209,plain,
( def107(X0,X1,X2,X3,sk15,X4,X5,X6,sk17)
| def26 ),
inference(factoring,[status(thm)],[p1204]) ).
cnf(c321,plain,
( X32 != X35
| def106(X27,X28,X29,X30,X33,X31,X32,X34)
| ~ def107(X27,X28,X29,X30,X33,X31,X32,X34,X35) ),
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])],[f0_sk]) ).
cnf(p1093,plain,
( def106(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ def107(X0,X1,X2,X3,X4,X5,X6,X7,X6) ),
inference(equality_resolution,[status(thm)],[c321]) ).
cnf(p1211,plain,
( def106(X0,X1,X2,X3,sk15,X4,sk17,X5)
| def26 ),
inference(resolution,[status(thm)],[p1209,p1093]) ).
cnf(c318,plain,
( ~ in(X34,X33)
| def105(X27,X28,X29,X30,X33,X31,X32,X34)
| ~ def106(X27,X28,X29,X30,X33,X31,X32,X34) ),
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])],[f0_sk]) ).
cnf(p1213,plain,
( ~ in(X5,sk15)
| def105(X0,X1,X2,X3,sk15,X4,sk17,X5)
| def26 ),
inference(resolution,[status(thm)],[p1211,c318]) ).
cnf(c238,plain,
( in(sk16,sk15)
| ~ def79 ),
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])],[f0_sk]) ).
cnf(p1106,plain,
( in(sk16,sk15)
| def26 ),
inference(resolution,[status(thm)],[p1103,c238]) ).
cnf(p1239,plain,
( def26
| def105(X0,X1,X2,X3,sk15,X4,sk17,sk16)
| def26 ),
inference(resolution,[status(thm)],[p1213,p1106]) ).
cnf(p1245,plain,
( def105(X0,X1,X2,X3,sk15,X4,sk17,sk16)
| def26 ),
inference(factoring,[status(thm)],[p1239]) ).
cnf(c315,plain,
( X31 != X34
| def104(X27,X28,X29,X30,X33,X31,X32)
| ~ def105(X27,X28,X29,X30,X33,X31,X32,X34) ),
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])],[f0_sk]) ).
cnf(p1091,plain,
( def104(X0,X1,X2,X3,X4,X5,X6)
| ~ def105(X0,X1,X2,X3,X4,X5,X6,X5) ),
inference(equality_resolution,[status(thm)],[c315]) ).
cnf(p1247,plain,
( def104(X0,X1,X2,X3,sk15,sk16,sk17)
| def26 ),
inference(resolution,[status(thm)],[p1245,p1091]) ).
cnf(p1251,plain,
( def104(X0,X1,X2,X3,sk15,sk16,sk14)
| def26
| def26 ),
inference(superposition,[status(thm)],[p1104,p1247]) ).
cnf(p1255,plain,
( def104(X0,X1,X2,X3,sk15,sk16,sk14)
| def26 ),
inference(factoring,[status(thm)],[p1251]) ).
cnf(c312,plain,
( ~ young(X32)
| def103(X27,X28,X29,X30,X33,X31,X32)
| ~ def104(X27,X28,X29,X30,X33,X31,X32) ),
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])],[f0_sk]) ).
cnf(p1257,plain,
( ~ young(sk14)
| def103(X0,X1,X2,X3,sk15,sk16,sk14)
| def26 ),
inference(resolution,[status(thm)],[p1255,c312]) ).
cnf(c234,plain,
( def77
| ~ def78 ),
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])],[f0_sk]) ).
cnf(p1107,plain,
( def77
| def26 ),
inference(resolution,[status(thm)],[p1105,c234]) ).
cnf(c232,plain,
( young(sk14)
| ~ def77 ),
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])],[f0_sk]) ).
cnf(p1110,plain,
( young(sk14)
| def26 ),
inference(resolution,[status(thm)],[p1107,c232]) ).
cnf(p1280,plain,
( def26
| def103(X0,X1,X2,X3,sk15,sk16,sk14)
| def26 ),
inference(resolution,[status(thm)],[p1257,p1110]) ).
cnf(p1281,plain,
( def103(X0,X1,X2,X3,sk15,sk16,sk14)
| def26 ),
inference(factoring,[status(thm)],[p1280]) ).
cnf(c309,plain,
( ~ man(X32)
| def102(X27,X28,X29,X30,X33,X31,X32)
| ~ def103(X27,X28,X29,X30,X33,X31,X32) ),
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])],[f0_sk]) ).
cnf(p1282,plain,
( ~ man(sk14)
| def102(X0,X1,X2,X3,sk15,sk16,sk14)
| def26 ),
inference(resolution,[status(thm)],[p1281,c309]) ).
cnf(c231,plain,
( def76
| ~ def77 ),
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])],[f0_sk]) ).
cnf(p1109,plain,
( def76
| def26 ),
inference(resolution,[status(thm)],[p1107,c231]) ).
cnf(c229,plain,
( man(sk14)
| ~ def76 ),
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])],[f0_sk]) ).
cnf(p1112,plain,
( man(sk14)
| def26 ),
inference(resolution,[status(thm)],[p1109,c229]) ).
cnf(p1294,plain,
( def26
| def102(X0,X1,X2,X3,sk15,sk16,sk14)
| def26 ),
inference(resolution,[status(thm)],[p1282,p1112]) ).
cnf(p1295,plain,
( def102(X0,X1,X2,X3,sk15,sk16,sk14)
| def26 ),
inference(factoring,[status(thm)],[p1294]) ).
cnf(c306,plain,
( ~ fellow(X32)
| def101(X27,X28,X29,X30,X33,X31,X32)
| ~ def102(X27,X28,X29,X30,X33,X31,X32) ),
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])],[f0_sk]) ).
cnf(p1296,plain,
( ~ fellow(sk14)
| def101(X0,X1,X2,X3,sk15,sk16,sk14)
| def26 ),
inference(resolution,[status(thm)],[p1295,c306]) ).
cnf(c228,plain,
( def75
| ~ def76 ),
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])],[f0_sk]) ).
cnf(p1111,plain,
( def75
| def26 ),
inference(resolution,[status(thm)],[p1109,c228]) ).
cnf(c226,plain,
( fellow(sk14)
| ~ def75 ),
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])],[f0_sk]) ).
cnf(p1114,plain,
( fellow(sk14)
| def26 ),
inference(resolution,[status(thm)],[p1111,c226]) ).
cnf(p1303,plain,
( def26
| def101(X0,X1,X2,X3,sk15,sk16,sk14)
| def26 ),
inference(resolution,[status(thm)],[p1296,p1114]) ).
cnf(p1304,plain,
( def101(X0,X1,X2,X3,sk15,sk16,sk14)
| def26 ),
inference(factoring,[status(thm)],[p1303]) ).
cnf(p1306,plain,
( def101(X0,X1,X2,X3,sk15,sk13,sk14)
| def26
| def26 ),
inference(superposition,[status(thm)],[p1108,p1304]) ).
cnf(p1307,plain,
( def101(X0,X1,X2,X3,sk15,sk13,sk14)
| def26 ),
inference(factoring,[status(thm)],[p1306]) ).
cnf(c303,plain,
( ~ young(X31)
| def100(X27,X28,X29,X30,X33,X31,X32)
| ~ def101(X27,X28,X29,X30,X33,X31,X32) ),
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])],[f0_sk]) ).
cnf(p1308,plain,
( ~ young(sk13)
| def100(X0,X1,X2,X3,sk15,sk13,sk14)
| def26 ),
inference(resolution,[status(thm)],[p1307,c303]) ).
cnf(c225,plain,
( def74
| ~ def75 ),
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])],[f0_sk]) ).
cnf(p1113,plain,
( def74
| def26 ),
inference(resolution,[status(thm)],[p1111,c225]) ).
cnf(c223,plain,
( young(sk13)
| ~ def74 ),
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])],[f0_sk]) ).
cnf(p1116,plain,
( young(sk13)
| def26 ),
inference(resolution,[status(thm)],[p1113,c223]) ).
cnf(p1313,plain,
( def26
| def100(X0,X1,X2,X3,sk15,sk13,sk14)
| def26 ),
inference(resolution,[status(thm)],[p1308,p1116]) ).
cnf(p1314,plain,
( def100(X0,X1,X2,X3,sk15,sk13,sk14)
| def26 ),
inference(factoring,[status(thm)],[p1313]) ).
cnf(c300,plain,
( ~ man(X31)
| def99(X27,X28,X29,X30,X33,X31,X32)
| ~ def100(X27,X28,X29,X30,X33,X31,X32) ),
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])],[f0_sk]) ).
cnf(p1315,plain,
( ~ man(sk13)
| def99(X0,X1,X2,X3,sk15,sk13,sk14)
| def26 ),
inference(resolution,[status(thm)],[p1314,c300]) ).
cnf(c222,plain,
( def73
| ~ def74 ),
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])],[f0_sk]) ).
cnf(p1115,plain,
( def73
| def26 ),
inference(resolution,[status(thm)],[p1113,c222]) ).
cnf(c220,plain,
( man(sk13)
| ~ def73 ),
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])],[f0_sk]) ).
cnf(p1118,plain,
( man(sk13)
| def26 ),
inference(resolution,[status(thm)],[p1115,c220]) ).
cnf(p1317,plain,
( def26
| def99(X0,X1,X2,X3,sk15,sk13,sk14)
| def26 ),
inference(resolution,[status(thm)],[p1315,p1118]) ).
cnf(p1318,plain,
( def99(X0,X1,X2,X3,sk15,sk13,sk14)
| def26 ),
inference(factoring,[status(thm)],[p1317]) ).
cnf(c297,plain,
( ~ fellow(X31)
| def98(X27,X28,X29,X30,X33,X31,X32)
| ~ def99(X27,X28,X29,X30,X33,X31,X32) ),
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])],[f0_sk]) ).
cnf(p1319,plain,
( ~ fellow(sk13)
| def98(X0,X1,X2,X3,sk15,sk13,sk14)
| def26 ),
inference(resolution,[status(thm)],[p1318,c297]) ).
cnf(c219,plain,
( def72
| ~ def73 ),
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])],[f0_sk]) ).
cnf(p1117,plain,
( def72
| def26 ),
inference(resolution,[status(thm)],[p1115,c219]) ).
cnf(c217,plain,
( fellow(sk13)
| ~ def72 ),
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])],[f0_sk]) ).
cnf(p1120,plain,
( fellow(sk13)
| def26 ),
inference(resolution,[status(thm)],[p1117,c217]) ).
cnf(p1320,plain,
( def26
| def98(X0,X1,X2,X3,sk15,sk13,sk14)
| def26 ),
inference(resolution,[status(thm)],[p1319,p1120]) ).
cnf(p1321,plain,
( def98(X0,X1,X2,X3,sk15,sk13,sk14)
| def26 ),
inference(factoring,[status(thm)],[p1320]) ).
cnf(c294,plain,
( X31 = X32
| def97(X27,X28,X29,X30,X33)
| ~ def98(X27,X28,X29,X30,X33,X31,X32) ),
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])],[f0_sk]) ).
cnf(p1322,plain,
( sk13 = sk14
| def97(X0,X1,X2,X3,sk15)
| def26 ),
inference(resolution,[status(thm)],[p1321,c294]) ).
cnf(c291,plain,
( ~ front(X33)
| def96(X27,X28,X29,X30,X33)
| ~ def97(X27,X28,X29,X30,X33) ),
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])],[f0_sk]) ).
cnf(p1324,plain,
( ~ front(sk15)
| def96(X0,X1,X2,X3,sk15)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1322,c291]) ).
cnf(c216,plain,
( def71
| ~ def72 ),
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])],[f0_sk]) ).
cnf(p1119,plain,
( def71
| def26 ),
inference(resolution,[status(thm)],[p1117,c216]) ).
cnf(c213,plain,
( def70
| ~ def71 ),
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])],[f0_sk]) ).
cnf(p1121,plain,
( def70
| def26 ),
inference(resolution,[status(thm)],[p1119,c213]) ).
cnf(c211,plain,
( front(sk15)
| ~ def70 ),
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])],[f0_sk]) ).
cnf(p1124,plain,
( front(sk15)
| def26 ),
inference(resolution,[status(thm)],[p1121,c211]) ).
cnf(p1448,plain,
( def26
| def96(X0,X1,X2,X3,sk15)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1324,p1124]) ).
cnf(p1449,plain,
( def96(X0,X1,X2,X3,sk15)
| sk13 = sk14
| def26 ),
inference(factoring,[status(thm)],[p1448]) ).
cnf(c288,plain,
( ~ furniture(X33)
| def95(X27,X28,X29,X30,X33)
| ~ def96(X27,X28,X29,X30,X33) ),
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])],[f0_sk]) ).
cnf(p1450,plain,
( ~ furniture(sk15)
| def95(X0,X1,X2,X3,sk15)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1449,c288]) ).
cnf(c210,plain,
( def69
| ~ def70 ),
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])],[f0_sk]) ).
cnf(p1123,plain,
( def69
| def26 ),
inference(resolution,[status(thm)],[p1121,c210]) ).
cnf(c208,plain,
( furniture(sk15)
| ~ def69 ),
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])],[f0_sk]) ).
cnf(p1126,plain,
( furniture(sk15)
| def26 ),
inference(resolution,[status(thm)],[p1123,c208]) ).
cnf(p1494,plain,
( def26
| def95(X0,X1,X2,X3,sk15)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1450,p1126]) ).
cnf(p1495,plain,
( def95(X0,X1,X2,X3,sk15)
| sk13 = sk14
| def26 ),
inference(factoring,[status(thm)],[p1494]) ).
cnf(c285,plain,
( ~ seat(X33)
| def94(X27,X28,X29,X30)
| ~ def95(X27,X28,X29,X30,X33) ),
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])],[f0_sk]) ).
cnf(p1496,plain,
( ~ seat(sk15)
| def94(X0,X1,X2,X3)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1495,c285]) ).
cnf(c207,plain,
( def68
| ~ def69 ),
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])],[f0_sk]) ).
cnf(p1125,plain,
( def68
| def26 ),
inference(resolution,[status(thm)],[p1123,c207]) ).
cnf(c205,plain,
( seat(sk15)
| ~ def68 ),
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])],[f0_sk]) ).
cnf(p1128,plain,
( seat(sk15)
| def26 ),
inference(resolution,[status(thm)],[p1125,c205]) ).
cnf(p1497,plain,
( def26
| def94(X0,X1,X2,X3)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1496,p1128]) ).
cnf(p1498,plain,
( def94(X0,X1,X2,X3)
| sk13 = sk14
| def26 ),
inference(factoring,[status(thm)],[p1497]) ).
cnf(c282,plain,
( ~ in(X28,X27)
| def93(X27,X28,X29,X30)
| ~ def94(X27,X28,X29,X30) ),
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])],[f0_sk]) ).
cnf(p1500,plain,
( ~ in(X1,X0)
| def93(X0,X1,X2,X3)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1498,c282]) ).
cnf(c204,plain,
( def67
| ~ def68 ),
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])],[f0_sk]) ).
cnf(p1127,plain,
( def67
| def26 ),
inference(resolution,[status(thm)],[p1125,c204]) ).
cnf(c202,plain,
( in(sk10,sk9)
| ~ def67 ),
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])],[f0_sk]) ).
cnf(p1130,plain,
( in(sk10,sk9)
| def26 ),
inference(resolution,[status(thm)],[p1127,c202]) ).
cnf(p1603,plain,
( def26
| def93(sk9,sk10,X0,X1)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1500,p1130]) ).
cnf(p1610,plain,
( def93(sk9,sk10,X0,X1)
| sk13 = sk14
| def26 ),
inference(factoring,[status(thm)],[p1603]) ).
cnf(c279,plain,
( ~ down(X28,X29)
| def92(X27,X28,X29,X30)
| ~ def93(X27,X28,X29,X30) ),
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])],[f0_sk]) ).
cnf(p1611,plain,
( ~ down(sk10,X0)
| def92(sk9,sk10,X0,X1)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1610,c279]) ).
cnf(c201,plain,
( def66
| ~ def67 ),
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])],[f0_sk]) ).
cnf(p1129,plain,
( def66
| def26 ),
inference(resolution,[status(thm)],[p1127,c201]) ).
cnf(c199,plain,
( down(sk10,sk12)
| ~ def66 ),
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])],[f0_sk]) ).
cnf(p1131,plain,
( down(sk10,sk12)
| def26 ),
inference(resolution,[status(thm)],[p1129,c199]) ).
cnf(p1704,plain,
( def26
| def92(sk9,sk10,sk12,X0)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1611,p1131]) ).
cnf(p1705,plain,
( def92(sk9,sk10,sk12,X0)
| sk13 = sk14
| def26 ),
inference(factoring,[status(thm)],[p1704]) ).
cnf(c276,plain,
( ~ barrel(X28,X30)
| def91(X27,X28,X29,X30)
| ~ def92(X27,X28,X29,X30) ),
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])],[f0_sk]) ).
cnf(p1706,plain,
( ~ barrel(sk10,X0)
| def91(sk9,sk10,sk12,X0)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1705,c276]) ).
cnf(c198,plain,
( def65
| ~ def66 ),
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])],[f0_sk]) ).
cnf(p1132,plain,
( def65
| def26 ),
inference(resolution,[status(thm)],[p1129,c198]) ).
cnf(c196,plain,
( barrel(sk10,sk11)
| ~ def65 ),
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])],[f0_sk]) ).
cnf(p1134,plain,
( barrel(sk10,sk11)
| def26 ),
inference(resolution,[status(thm)],[p1132,c196]) ).
cnf(p1790,plain,
( def26
| def91(sk9,sk10,sk12,sk11)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1706,p1134]) ).
cnf(p1791,plain,
( def91(sk9,sk10,sk12,sk11)
| sk13 = sk14
| def26 ),
inference(factoring,[status(thm)],[p1790]) ).
cnf(c273,plain,
( ~ old(X30)
| def90(X27,X28,X29,X30)
| ~ def91(X27,X28,X29,X30) ),
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])],[f0_sk]) ).
cnf(p1792,plain,
( ~ old(sk11)
| def90(sk9,sk10,sk12,sk11)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1791,c273]) ).
cnf(c195,plain,
( def64
| ~ def65 ),
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])],[f0_sk]) ).
cnf(p1133,plain,
( def64
| def26 ),
inference(resolution,[status(thm)],[p1132,c195]) ).
cnf(c192,plain,
( def63
| ~ def64 ),
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])],[f0_sk]) ).
cnf(p1135,plain,
( def63
| def26 ),
inference(resolution,[status(thm)],[p1133,c192]) ).
cnf(c189,plain,
( def62
| ~ def63 ),
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])],[f0_sk]) ).
cnf(p1137,plain,
( def62
| def26 ),
inference(resolution,[status(thm)],[p1135,c189]) ).
cnf(c186,plain,
( def61
| ~ def62 ),
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])],[f0_sk]) ).
cnf(p1139,plain,
( def61
| def26 ),
inference(resolution,[status(thm)],[p1137,c186]) ).
cnf(c184,plain,
( old(sk11)
| ~ def61 ),
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])],[f0_sk]) ).
cnf(p1142,plain,
( old(sk11)
| def26 ),
inference(resolution,[status(thm)],[p1139,c184]) ).
cnf(p1793,plain,
( def26
| def90(sk9,sk10,sk12,sk11)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1792,p1142]) ).
cnf(p1794,plain,
( def90(sk9,sk10,sk12,sk11)
| sk13 = sk14
| def26 ),
inference(factoring,[status(thm)],[p1793]) ).
cnf(c270,plain,
( ~ dirty(X30)
| def89(X27,X28,X29,X30)
| ~ def90(X27,X28,X29,X30) ),
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])],[f0_sk]) ).
cnf(p1795,plain,
( ~ dirty(sk11)
| def89(sk9,sk10,sk12,sk11)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1794,c270]) ).
cnf(c183,plain,
( def60
| ~ def61 ),
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])],[f0_sk]) ).
cnf(p1141,plain,
( def60
| def26 ),
inference(resolution,[status(thm)],[p1139,c183]) ).
cnf(c181,plain,
( dirty(sk11)
| ~ def60 ),
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])],[f0_sk]) ).
cnf(p1144,plain,
( dirty(sk11)
| def26 ),
inference(resolution,[status(thm)],[p1141,c181]) ).
cnf(p1796,plain,
( def26
| def89(sk9,sk10,sk12,sk11)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1795,p1144]) ).
cnf(p1797,plain,
( def89(sk9,sk10,sk12,sk11)
| sk13 = sk14
| def26 ),
inference(factoring,[status(thm)],[p1796]) ).
cnf(c267,plain,
( ~ white(X30)
| def88(X27,X28,X29,X30)
| ~ def89(X27,X28,X29,X30) ),
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])],[f0_sk]) ).
cnf(p1798,plain,
( ~ white(sk11)
| def88(sk9,sk10,sk12,sk11)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1797,c267]) ).
cnf(c180,plain,
( def59
| ~ def60 ),
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])],[f0_sk]) ).
cnf(p1143,plain,
( def59
| def26 ),
inference(resolution,[status(thm)],[p1141,c180]) ).
cnf(c178,plain,
( white(sk11)
| ~ def59 ),
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])],[f0_sk]) ).
cnf(p1146,plain,
( white(sk11)
| def26 ),
inference(resolution,[status(thm)],[p1143,c178]) ).
cnf(p1799,plain,
( def26
| def88(sk9,sk10,sk12,sk11)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1798,p1146]) ).
cnf(p1800,plain,
( def88(sk9,sk10,sk12,sk11)
| sk13 = sk14
| def26 ),
inference(factoring,[status(thm)],[p1799]) ).
cnf(c264,plain,
( ~ car(X30)
| def87(X27,X28,X29,X30)
| ~ def88(X27,X28,X29,X30) ),
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])],[f0_sk]) ).
cnf(p1801,plain,
( ~ car(sk11)
| def87(sk9,sk10,sk12,sk11)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1800,c264]) ).
cnf(c177,plain,
( def58
| ~ def59 ),
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])],[f0_sk]) ).
cnf(p1145,plain,
( def58
| def26 ),
inference(resolution,[status(thm)],[p1143,c177]) ).
cnf(c175,plain,
( car(sk11)
| ~ def58 ),
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])],[f0_sk]) ).
cnf(p1148,plain,
( car(sk11)
| def26 ),
inference(resolution,[status(thm)],[p1145,c175]) ).
cnf(p1802,plain,
( def26
| def87(sk9,sk10,sk12,sk11)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1801,p1148]) ).
cnf(p1803,plain,
( def87(sk9,sk10,sk12,sk11)
| sk13 = sk14
| def26 ),
inference(factoring,[status(thm)],[p1802]) ).
cnf(c261,plain,
( ~ chevy(X30)
| def86(X27,X28,X29)
| ~ def87(X27,X28,X29,X30) ),
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])],[f0_sk]) ).
cnf(p1804,plain,
( ~ chevy(sk11)
| def86(sk9,sk10,sk12)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1803,c261]) ).
cnf(c174,plain,
( def57
| ~ def58 ),
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])],[f0_sk]) ).
cnf(p1147,plain,
( def57
| def26 ),
inference(resolution,[status(thm)],[p1145,c174]) ).
cnf(c172,plain,
( chevy(sk11)
| ~ def57 ),
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])],[f0_sk]) ).
cnf(p1150,plain,
( chevy(sk11)
| def26 ),
inference(resolution,[status(thm)],[p1147,c172]) ).
cnf(p1805,plain,
( def26
| def86(sk9,sk10,sk12)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1804,p1150]) ).
cnf(p1806,plain,
( def86(sk9,sk10,sk12)
| sk13 = sk14
| def26 ),
inference(factoring,[status(thm)],[p1805]) ).
cnf(c258,plain,
( ~ lonely(X29)
| def85(X27,X28,X29)
| ~ def86(X27,X28,X29) ),
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])],[f0_sk]) ).
cnf(p1808,plain,
( ~ lonely(sk12)
| def85(sk9,sk10,sk12)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1806,c258]) ).
cnf(c193,plain,
( lonely(sk12)
| ~ def64 ),
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])],[f0_sk]) ).
cnf(p1136,plain,
( lonely(sk12)
| def26 ),
inference(resolution,[status(thm)],[p1133,c193]) ).
cnf(p1813,plain,
( def26
| def85(sk9,sk10,sk12)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1808,p1136]) ).
cnf(p1814,plain,
( def85(sk9,sk10,sk12)
| sk13 = sk14
| def26 ),
inference(factoring,[status(thm)],[p1813]) ).
cnf(c255,plain,
( ~ way(X29)
| def84(X27,X28,X29)
| ~ def85(X27,X28,X29) ),
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])],[f0_sk]) ).
cnf(p1815,plain,
( ~ way(sk12)
| def84(sk9,sk10,sk12)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1814,c255]) ).
cnf(c190,plain,
( way(sk12)
| ~ def63 ),
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])],[f0_sk]) ).
cnf(p1138,plain,
( way(sk12)
| def26 ),
inference(resolution,[status(thm)],[p1135,c190]) ).
cnf(p1816,plain,
( def26
| def84(sk9,sk10,sk12)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1815,p1138]) ).
cnf(p1817,plain,
( def84(sk9,sk10,sk12)
| sk13 = sk14
| def26 ),
inference(factoring,[status(thm)],[p1816]) ).
cnf(c252,plain,
( ~ street(X29)
| def83(X27,X28)
| ~ def84(X27,X28,X29) ),
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])],[f0_sk]) ).
cnf(p1818,plain,
( ~ street(sk12)
| def83(sk9,sk10)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1817,c252]) ).
cnf(c187,plain,
( street(sk12)
| ~ def62 ),
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])],[f0_sk]) ).
cnf(p1140,plain,
( street(sk12)
| def26 ),
inference(resolution,[status(thm)],[p1137,c187]) ).
cnf(p1819,plain,
( def26
| def83(sk9,sk10)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1818,p1140]) ).
cnf(p1820,plain,
( def83(sk9,sk10)
| sk13 = sk14
| def26 ),
inference(factoring,[status(thm)],[p1819]) ).
cnf(c249,plain,
( ~ event(X28)
| def82(X27)
| ~ def83(X27,X28) ),
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])],[f0_sk]) ).
cnf(p1822,plain,
( ~ event(sk10)
| def82(sk9)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1820,c249]) ).
cnf(c171,plain,
( def56
| ~ def57 ),
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])],[f0_sk]) ).
cnf(p1149,plain,
( def56
| def26 ),
inference(resolution,[status(thm)],[p1147,c171]) ).
cnf(c169,plain,
( event(sk10)
| ~ def56 ),
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])],[f0_sk]) ).
cnf(p1152,plain,
( event(sk10)
| def26 ),
inference(resolution,[status(thm)],[p1149,c169]) ).
cnf(p1826,plain,
( def26
| def82(sk9)
| sk13 = sk14
| def26 ),
inference(resolution,[status(thm)],[p1822,p1152]) ).
cnf(p1827,plain,
( def82(sk9)
| sk13 = sk14
| def26 ),
inference(factoring,[status(thm)],[p1826]) ).
cnf(c214,plain,
( sk13 != sk14
| ~ def71 ),
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])],[f0_sk]) ).
cnf(p1122,plain,
( sk13 != sk14
| def26 ),
inference(resolution,[status(thm)],[p1119,c214]) ).
cnf(p1831,plain,
( def26
| def82(sk9)
| def26 ),
inference(resolution,[status(thm)],[p1827,p1122]) ).
cnf(p1832,plain,
( def82(sk9)
| def26 ),
inference(factoring,[status(thm)],[p1831]) ).
cnf(c246,plain,
( ~ city(X27)
| ~ hollywood(X27)
| ~ def82(X27) ),
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])],[f0_sk]) ).
cnf(p1834,plain,
( ~ city(sk9)
| ~ hollywood(sk9)
| def26 ),
inference(resolution,[status(thm)],[p1832,c246]) ).
cnf(c168,plain,
( def55
| ~ def56 ),
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])],[f0_sk]) ).
cnf(p1151,plain,
( def55
| def26 ),
inference(resolution,[status(thm)],[p1149,c168]) ).
cnf(c165,plain,
( hollywood(sk9)
| ~ def55 ),
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])],[f0_sk]) ).
cnf(p1153,plain,
( hollywood(sk9)
| def26 ),
inference(resolution,[status(thm)],[p1151,c165]) ).
cnf(p1839,plain,
( def26
| ~ city(sk9)
| def26 ),
inference(resolution,[status(thm)],[p1834,p1153]) ).
cnf(p1840,plain,
( ~ city(sk9)
| def26 ),
inference(factoring,[status(thm)],[p1839]) ).
cnf(c166,plain,
( city(sk9)
| ~ def55 ),
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])],[f0_sk]) ).
cnf(p1154,plain,
( city(sk9)
| def26 ),
inference(resolution,[status(thm)],[p1151,c166]) ).
cnf(p1841,plain,
( def26
| def26 ),
inference(resolution,[status(thm)],[p1840,p1154]) ).
cnf(p1842,plain,
def26,
inference(factoring,[status(thm)],[p1841]) ).
cnf(c78,plain,
( def25
| ~ def26 ),
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])],[f0_sk]) ).
cnf(p1843,plain,
def25,
inference(resolution,[status(thm)],[p1842,c78]) ).
cnf(c75,plain,
( def24
| ~ def25 ),
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])],[f0_sk]) ).
cnf(p1846,plain,
def24,
inference(resolution,[status(thm)],[p1843,c75]) ).
cnf(c72,plain,
( def23
| ~ def24 ),
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])],[f0_sk]) ).
cnf(p1849,plain,
def23,
inference(resolution,[status(thm)],[p1846,c72]) ).
cnf(c70,plain,
( sk4 = sk7
| ~ def23 ),
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])],[f0_sk]) ).
cnf(p1851,plain,
sk4 = sk7,
inference(resolution,[status(thm)],[p1849,c70]) ).
cnf(c76,plain,
( sk5 = sk8
| ~ def25 ),
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])],[f0_sk]) ).
cnf(p1847,plain,
sk5 = sk8,
inference(resolution,[status(thm)],[p1843,c76]) ).
cnf(c163,plain,
( def53(X9,X10,X11,X12,X15,X13,X14,X16,X17)
| ~ def54(X9,X10,X11,X12,X15,X13,X14,X16,X17) ),
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])],[f0_sk]) ).
cnf(p1097,plain,
( def53(X9,X10,X11,X12,X13,X14,X15,X16,X17)
| def109(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
inference(resolution,[status(thm)],[p1094,c163]) ).
cnf(c159,plain,
( ~ in(X17,X15)
| def52(X9,X10,X11,X12,X15,X13,X14,X16,X17)
| ~ def53(X9,X10,X11,X12,X15,X13,X14,X16,X17) ),
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])],[f0_sk]) ).
cnf(p2768,plain,
( ~ in(X17,X13)
| def52(X9,X10,X11,X12,X13,X14,X15,X16,X17)
| def109(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
inference(resolution,[status(thm)],[p1097,c159]) ).
cnf(c79,plain,
( in(sk8,sk6)
| ~ def26 ),
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])],[f0_sk]) ).
cnf(p1844,plain,
in(sk8,sk6),
inference(resolution,[status(thm)],[p1842,c79]) ).
cnf(p2836,plain,
( def52(X9,X10,X11,X12,sk6,X13,X14,X15,sk8)
| def109(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
inference(resolution,[status(thm)],[p2768,p1844]) ).
cnf(c156,plain,
( X14 != X17
| def51(X9,X10,X11,X12,X15,X13,X14,X16)
| ~ def52(X9,X10,X11,X12,X15,X13,X14,X16,X17) ),
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])],[f0_sk]) ).
cnf(p1092,plain,
( def51(X0,X1,X2,X3,X4,X5,X6,X7)
| ~ def52(X0,X1,X2,X3,X4,X5,X6,X7,X6) ),
inference(equality_resolution,[status(thm)],[c156]) ).
cnf(p2848,plain,
( def51(X9,X10,X11,X12,sk6,X13,sk8,X14)
| def109(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
inference(resolution,[status(thm)],[p2836,p1092]) ).
cnf(c153,plain,
( ~ in(X16,X15)
| def50(X9,X10,X11,X12,X15,X13,X14,X16)
| ~ def51(X9,X10,X11,X12,X15,X13,X14,X16) ),
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])],[f0_sk]) ).
cnf(p2851,plain,
( ~ in(X14,sk6)
| def50(X9,X10,X11,X12,sk6,X13,sk8,X14)
| def109(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
inference(resolution,[status(thm)],[p2848,c153]) ).
cnf(c73,plain,
( in(sk7,sk6)
| ~ def24 ),
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])],[f0_sk]) ).
cnf(p1848,plain,
in(sk7,sk6),
inference(resolution,[status(thm)],[p1846,c73]) ).
cnf(p2967,plain,
( def50(X9,X10,X11,X12,sk6,X13,sk8,sk7)
| def109(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
inference(resolution,[status(thm)],[p2851,p1848]) ).
cnf(c150,plain,
( X13 != X16
| def49(X9,X10,X11,X12,X15,X13,X14)
| ~ def50(X9,X10,X11,X12,X15,X13,X14,X16) ),
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])],[f0_sk]) ).
cnf(p1090,plain,
( def49(X0,X1,X2,X3,X4,X5,X6)
| ~ def50(X0,X1,X2,X3,X4,X5,X6,X5) ),
inference(equality_resolution,[status(thm)],[c150]) ).
cnf(p2975,plain,
( def49(X9,X10,X11,X12,sk6,sk7,sk8)
| def109(X0,X1,X2,X3,X4,X5,X6,X7,X8) ),
inference(resolution,[status(thm)],[p2967,p1090]) ).
cnf(p2979,plain,
( def108(X4,X5,X6,X7,X8,X9,X10,X11,X12)
| def49(X0,X1,X2,X3,sk6,sk7,sk8) ),
inference(resolution,[status(thm)],[p2975,c328]) ).
cnf(p2984,plain,
( ~ in(X12,X8)
| def107(X4,X5,X6,X7,X8,X9,X10,X11,X12)
| def49(X0,X1,X2,X3,sk6,sk7,sk8) ),
inference(resolution,[status(thm)],[p2979,c324]) ).
cnf(p3251,plain,
( def107(X4,X5,X6,X7,sk6,X8,X9,X10,sk8)
| def49(X0,X1,X2,X3,sk6,sk7,sk8) ),
inference(resolution,[status(thm)],[p2984,p1844]) ).
cnf(p3264,plain,
( def106(X4,X5,X6,X7,sk6,X8,sk8,X9)
| def49(X0,X1,X2,X3,sk6,sk7,sk8) ),
inference(resolution,[status(thm)],[p3251,p1093]) ).
cnf(p3270,plain,
( ~ in(X9,sk6)
| def105(X4,X5,X6,X7,sk6,X8,sk8,X9)
| def49(X0,X1,X2,X3,sk6,sk7,sk8) ),
inference(resolution,[status(thm)],[p3264,c318]) ).
cnf(p6093,plain,
( def105(X4,X5,X6,X7,sk6,X8,sk8,sk7)
| def49(X0,X1,X2,X3,sk6,sk7,sk8) ),
inference(resolution,[status(thm)],[p3270,p1848]) ).
cnf(p6105,plain,
( def104(X4,X5,X6,X7,sk6,sk7,sk8)
| def49(X0,X1,X2,X3,sk6,sk7,sk8) ),
inference(resolution,[status(thm)],[p6093,p1091]) ).
cnf(p6113,plain,
( def104(X4,X5,X6,X7,sk6,sk7,sk8)
| def49(X0,X1,X2,X3,sk6,sk7,sk5) ),
inference(superposition,[status(thm)],[p1847,p6105]) ).
cnf(c147,plain,
( ~ young(X14)
| def48(X9,X10,X11,X12,X15,X13,X14)
| ~ def49(X9,X10,X11,X12,X15,X13,X14) ),
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])],[f0_sk]) ).
cnf(p6119,plain,
( ~ young(sk5)
| def48(X4,X5,X6,X7,sk6,sk7,sk5)
| def104(X0,X1,X2,X3,sk6,sk7,sk8) ),
inference(resolution,[status(thm)],[p6113,c147]) ).
cnf(c69,plain,
( def22
| ~ def23 ),
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])],[f0_sk]) ).
cnf(p1850,plain,
def22,
inference(resolution,[status(thm)],[p1849,c69]) ).
cnf(c67,plain,
( young(sk5)
| ~ def22 ),
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])],[f0_sk]) ).
cnf(p1853,plain,
young(sk5),
inference(resolution,[status(thm)],[p1850,c67]) ).
cnf(p6750,plain,
( def48(X4,X5,X6,X7,sk6,sk7,sk5)
| def104(X0,X1,X2,X3,sk6,sk7,sk8) ),
inference(resolution,[status(thm)],[p6119,p1853]) ).
cnf(c144,plain,
( ~ man(X14)
| def47(X9,X10,X11,X12,X15,X13,X14)
| ~ def48(X9,X10,X11,X12,X15,X13,X14) ),
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])],[f0_sk]) ).
cnf(p6752,plain,
( ~ man(sk5)
| def47(X4,X5,X6,X7,sk6,sk7,sk5)
| def104(X0,X1,X2,X3,sk6,sk7,sk8) ),
inference(resolution,[status(thm)],[p6750,c144]) ).
cnf(c66,plain,
( def21
| ~ def22 ),
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])],[f0_sk]) ).
cnf(p1852,plain,
def21,
inference(resolution,[status(thm)],[p1850,c66]) ).
cnf(c64,plain,
( man(sk5)
| ~ def21 ),
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])],[f0_sk]) ).
cnf(p1855,plain,
man(sk5),
inference(resolution,[status(thm)],[p1852,c64]) ).
cnf(p7170,plain,
( def47(X4,X5,X6,X7,sk6,sk7,sk5)
| def104(X0,X1,X2,X3,sk6,sk7,sk8) ),
inference(resolution,[status(thm)],[p6752,p1855]) ).
cnf(c141,plain,
( ~ fellow(X14)
| def46(X9,X10,X11,X12,X15,X13,X14)
| ~ def47(X9,X10,X11,X12,X15,X13,X14) ),
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])],[f0_sk]) ).
cnf(p7172,plain,
( ~ fellow(sk5)
| def46(X4,X5,X6,X7,sk6,sk7,sk5)
| def104(X0,X1,X2,X3,sk6,sk7,sk8) ),
inference(resolution,[status(thm)],[p7170,c141]) ).
cnf(c63,plain,
( def20
| ~ def21 ),
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])],[f0_sk]) ).
cnf(p1854,plain,
def20,
inference(resolution,[status(thm)],[p1852,c63]) ).
cnf(c61,plain,
( fellow(sk5)
| ~ def20 ),
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])],[f0_sk]) ).
cnf(p1857,plain,
fellow(sk5),
inference(resolution,[status(thm)],[p1854,c61]) ).
cnf(p7512,plain,
( def46(X4,X5,X6,X7,sk6,sk7,sk5)
| def104(X0,X1,X2,X3,sk6,sk7,sk8) ),
inference(resolution,[status(thm)],[p7172,p1857]) ).
cnf(p7516,plain,
( def46(X4,X5,X6,X7,sk6,sk7,sk5)
| def104(X0,X1,X2,X3,sk6,sk7,sk5) ),
inference(superposition,[status(thm)],[p1847,p7512]) ).
cnf(p7521,plain,
( ~ young(sk5)
| def103(X4,X5,X6,X7,sk6,sk7,sk5)
| def46(X0,X1,X2,X3,sk6,sk7,sk5) ),
inference(resolution,[status(thm)],[p7516,c312]) ).
cnf(p7989,plain,
( def103(X4,X5,X6,X7,sk6,sk7,sk5)
| def46(X0,X1,X2,X3,sk6,sk7,sk5) ),
inference(resolution,[status(thm)],[p7521,p1853]) ).
cnf(p7991,plain,
( ~ man(sk5)
| def102(X4,X5,X6,X7,sk6,sk7,sk5)
| def46(X0,X1,X2,X3,sk6,sk7,sk5) ),
inference(resolution,[status(thm)],[p7989,c309]) ).
cnf(p8259,plain,
( def102(X4,X5,X6,X7,sk6,sk7,sk5)
| def46(X0,X1,X2,X3,sk6,sk7,sk5) ),
inference(resolution,[status(thm)],[p7991,p1855]) ).
cnf(p8261,plain,
( ~ fellow(sk5)
| def101(X4,X5,X6,X7,sk6,sk7,sk5)
| def46(X0,X1,X2,X3,sk6,sk7,sk5) ),
inference(resolution,[status(thm)],[p8259,c306]) ).
cnf(p8743,plain,
( def101(X4,X5,X6,X7,sk6,sk7,sk5)
| def46(X0,X1,X2,X3,sk6,sk7,sk5) ),
inference(resolution,[status(thm)],[p8261,p1857]) ).
cnf(p8746,plain,
( def101(X4,X5,X6,X7,sk6,sk7,sk5)
| def46(X0,X1,X2,X3,sk6,sk4,sk5) ),
inference(superposition,[status(thm)],[p1851,p8743]) ).
cnf(c138,plain,
( ~ young(X13)
| def45(X9,X10,X11,X12,X15,X13,X14)
| ~ def46(X9,X10,X11,X12,X15,X13,X14) ),
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])],[f0_sk]) ).
cnf(p8748,plain,
( ~ young(sk4)
| def45(X4,X5,X6,X7,sk6,sk4,sk5)
| def101(X0,X1,X2,X3,sk6,sk7,sk5) ),
inference(resolution,[status(thm)],[p8746,c138]) ).
cnf(c60,plain,
( def19
| ~ def20 ),
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])],[f0_sk]) ).
cnf(p1856,plain,
def19,
inference(resolution,[status(thm)],[p1854,c60]) ).
cnf(c58,plain,
( young(sk4)
| ~ def19 ),
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])],[f0_sk]) ).
cnf(p1859,plain,
young(sk4),
inference(resolution,[status(thm)],[p1856,c58]) ).
cnf(p9167,plain,
( def45(X4,X5,X6,X7,sk6,sk4,sk5)
| def101(X0,X1,X2,X3,sk6,sk7,sk5) ),
inference(resolution,[status(thm)],[p8748,p1859]) ).
cnf(c135,plain,
( ~ man(X13)
| def44(X9,X10,X11,X12,X15,X13,X14)
| ~ def45(X9,X10,X11,X12,X15,X13,X14) ),
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])],[f0_sk]) ).
cnf(p9168,plain,
( ~ man(sk4)
| def44(X4,X5,X6,X7,sk6,sk4,sk5)
| def101(X0,X1,X2,X3,sk6,sk7,sk5) ),
inference(resolution,[status(thm)],[p9167,c135]) ).
cnf(c57,plain,
( def18
| ~ def19 ),
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])],[f0_sk]) ).
cnf(p1858,plain,
def18,
inference(resolution,[status(thm)],[p1856,c57]) ).
cnf(c55,plain,
( man(sk4)
| ~ def18 ),
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])],[f0_sk]) ).
cnf(p1861,plain,
man(sk4),
inference(resolution,[status(thm)],[p1858,c55]) ).
cnf(p9717,plain,
( def44(X4,X5,X6,X7,sk6,sk4,sk5)
| def101(X0,X1,X2,X3,sk6,sk7,sk5) ),
inference(resolution,[status(thm)],[p9168,p1861]) ).
cnf(c132,plain,
( ~ fellow(X13)
| def43(X9,X10,X11,X12,X15,X13,X14)
| ~ def44(X9,X10,X11,X12,X15,X13,X14) ),
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])],[f0_sk]) ).
cnf(p9718,plain,
( ~ fellow(sk4)
| def43(X4,X5,X6,X7,sk6,sk4,sk5)
| def101(X0,X1,X2,X3,sk6,sk7,sk5) ),
inference(resolution,[status(thm)],[p9717,c132]) ).
cnf(c54,plain,
( def17
| ~ def18 ),
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])],[f0_sk]) ).
cnf(p1860,plain,
def17,
inference(resolution,[status(thm)],[p1858,c54]) ).
cnf(c52,plain,
( fellow(sk4)
| ~ def17 ),
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])],[f0_sk]) ).
cnf(p1863,plain,
fellow(sk4),
inference(resolution,[status(thm)],[p1860,c52]) ).
cnf(p10135,plain,
( def43(X4,X5,X6,X7,sk6,sk4,sk5)
| def101(X0,X1,X2,X3,sk6,sk7,sk5) ),
inference(resolution,[status(thm)],[p9718,p1863]) ).
cnf(p10138,plain,
( def43(X4,X5,X6,X7,sk6,sk4,sk5)
| def101(X0,X1,X2,X3,sk6,sk4,sk5) ),
inference(superposition,[status(thm)],[p1851,p10135]) ).
cnf(p10140,plain,
( ~ young(sk4)
| def100(X4,X5,X6,X7,sk6,sk4,sk5)
| def43(X0,X1,X2,X3,sk6,sk4,sk5) ),
inference(resolution,[status(thm)],[p10138,c303]) ).
cnf(p10694,plain,
( def100(X4,X5,X6,X7,sk6,sk4,sk5)
| def43(X0,X1,X2,X3,sk6,sk4,sk5) ),
inference(resolution,[status(thm)],[p10140,p1859]) ).
cnf(p10696,plain,
( ~ man(sk4)
| def99(X4,X5,X6,X7,sk6,sk4,sk5)
| def43(X0,X1,X2,X3,sk6,sk4,sk5) ),
inference(resolution,[status(thm)],[p10694,c300]) ).
cnf(p11070,plain,
( def99(X4,X5,X6,X7,sk6,sk4,sk5)
| def43(X0,X1,X2,X3,sk6,sk4,sk5) ),
inference(resolution,[status(thm)],[p10696,p1861]) ).
cnf(p11072,plain,
( ~ fellow(sk4)
| def98(X4,X5,X6,X7,sk6,sk4,sk5)
| def43(X0,X1,X2,X3,sk6,sk4,sk5) ),
inference(resolution,[status(thm)],[p11070,c297]) ).
cnf(p11471,plain,
( def98(X4,X5,X6,X7,sk6,sk4,sk5)
| def43(X0,X1,X2,X3,sk6,sk4,sk5) ),
inference(resolution,[status(thm)],[p11072,p1863]) ).
cnf(c129,plain,
( X13 = X14
| def42(X9,X10,X11,X12,X15)
| ~ def43(X9,X10,X11,X12,X15,X13,X14) ),
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])],[f0_sk]) ).
cnf(p11472,plain,
( sk4 = sk5
| def42(X4,X5,X6,X7,sk6)
| def98(X0,X1,X2,X3,sk6,sk4,sk5) ),
inference(resolution,[status(thm)],[p11471,c129]) ).
cnf(p11476,plain,
( sk4 = sk5
| def97(X4,X5,X6,X7,sk6)
| sk4 = sk5
| def42(X0,X1,X2,X3,sk6) ),
inference(resolution,[status(thm)],[p11472,c294]) ).
cnf(p13153,plain,
( def97(X4,X5,X6,X7,sk6)
| sk4 = sk5
| def42(X0,X1,X2,X3,sk6) ),
inference(factoring,[status(thm)],[p11476]) ).
cnf(c126,plain,
( ~ front(X15)
| def41(X9,X10,X11,X12,X15)
| ~ def42(X9,X10,X11,X12,X15) ),
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])],[f0_sk]) ).
cnf(p13156,plain,
( ~ front(sk6)
| def41(X4,X5,X6,X7,sk6)
| def97(X0,X1,X2,X3,sk6)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p13153,c126]) ).
cnf(c51,plain,
( def16
| ~ def17 ),
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])],[f0_sk]) ).
cnf(p1862,plain,
def16,
inference(resolution,[status(thm)],[p1860,c51]) ).
cnf(c48,plain,
( def15
| ~ def16 ),
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])],[f0_sk]) ).
cnf(p1865,plain,
def15,
inference(resolution,[status(thm)],[p1862,c48]) ).
cnf(c46,plain,
( front(sk6)
| ~ def15 ),
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])],[f0_sk]) ).
cnf(p1867,plain,
front(sk6),
inference(resolution,[status(thm)],[p1865,c46]) ).
cnf(p13199,plain,
( def41(X4,X5,X6,X7,sk6)
| def97(X0,X1,X2,X3,sk6)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p13156,p1867]) ).
cnf(c123,plain,
( ~ furniture(X15)
| def40(X9,X10,X11,X12,X15)
| ~ def41(X9,X10,X11,X12,X15) ),
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])],[f0_sk]) ).
cnf(p13201,plain,
( ~ furniture(sk6)
| def40(X4,X5,X6,X7,sk6)
| def97(X0,X1,X2,X3,sk6)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p13199,c123]) ).
cnf(c45,plain,
( def14
| ~ def15 ),
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])],[f0_sk]) ).
cnf(p1866,plain,
def14,
inference(resolution,[status(thm)],[p1865,c45]) ).
cnf(c43,plain,
( furniture(sk6)
| ~ def14 ),
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])],[f0_sk]) ).
cnf(p1869,plain,
furniture(sk6),
inference(resolution,[status(thm)],[p1866,c43]) ).
cnf(p13238,plain,
( def40(X4,X5,X6,X7,sk6)
| def97(X0,X1,X2,X3,sk6)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p13201,p1869]) ).
cnf(c120,plain,
( ~ seat(X15)
| def39(X9,X10,X11,X12)
| ~ def40(X9,X10,X11,X12,X15) ),
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])],[f0_sk]) ).
cnf(p13239,plain,
( ~ seat(sk6)
| def39(X4,X5,X6,X7)
| def97(X0,X1,X2,X3,sk6)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p13238,c120]) ).
cnf(c42,plain,
( def13
| ~ def14 ),
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])],[f0_sk]) ).
cnf(p1868,plain,
def13,
inference(resolution,[status(thm)],[p1866,c42]) ).
cnf(c40,plain,
( seat(sk6)
| ~ def13 ),
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])],[f0_sk]) ).
cnf(p1871,plain,
seat(sk6),
inference(resolution,[status(thm)],[p1868,c40]) ).
cnf(p13242,plain,
( def39(X4,X5,X6,X7)
| def97(X0,X1,X2,X3,sk6)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p13239,p1871]) ).
cnf(p13246,plain,
( ~ front(sk6)
| def96(X4,X5,X6,X7,sk6)
| def39(X0,X1,X2,X3)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p13242,c291]) ).
cnf(p13276,plain,
( def96(X4,X5,X6,X7,sk6)
| def39(X0,X1,X2,X3)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p13246,p1867]) ).
cnf(p13279,plain,
( ~ furniture(sk6)
| def95(X4,X5,X6,X7,sk6)
| def39(X0,X1,X2,X3)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p13276,c288]) ).
cnf(p13298,plain,
( def95(X4,X5,X6,X7,sk6)
| def39(X0,X1,X2,X3)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p13279,p1869]) ).
cnf(p13301,plain,
( ~ seat(sk6)
| def94(X4,X5,X6,X7)
| def39(X0,X1,X2,X3)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p13298,c285]) ).
cnf(p13308,plain,
( def94(X4,X5,X6,X7)
| def39(X0,X1,X2,X3)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p13301,p1871]) ).
cnf(p13312,plain,
( ~ in(X5,X4)
| def93(X4,X5,X6,X7)
| def39(X0,X1,X2,X3)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p13308,c282]) ).
cnf(c39,plain,
( def12
| ~ def13 ),
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])],[f0_sk]) ).
cnf(p1870,plain,
def12,
inference(resolution,[status(thm)],[p1868,c39]) ).
cnf(c37,plain,
( in(sk1,sk0)
| ~ def12 ),
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])],[f0_sk]) ).
cnf(p1872,plain,
in(sk1,sk0),
inference(resolution,[status(thm)],[p1870,c37]) ).
cnf(p13635,plain,
( def93(sk0,sk1,X4,X5)
| def39(X0,X1,X2,X3)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p13312,p1872]) ).
cnf(p13651,plain,
( ~ down(sk1,X4)
| def92(sk0,sk1,X4,X5)
| def39(X0,X1,X2,X3)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p13635,c279]) ).
cnf(c36,plain,
( def11
| ~ def12 ),
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])],[f0_sk]) ).
cnf(p1873,plain,
def11,
inference(resolution,[status(thm)],[p1870,c36]) ).
cnf(c34,plain,
( down(sk1,sk2)
| ~ def11 ),
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])],[f0_sk]) ).
cnf(p1875,plain,
down(sk1,sk2),
inference(resolution,[status(thm)],[p1873,c34]) ).
cnf(p14276,plain,
( def92(sk0,sk1,sk2,X4)
| def39(X0,X1,X2,X3)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p13651,p1875]) ).
cnf(p14279,plain,
( ~ barrel(sk1,X4)
| def91(sk0,sk1,sk2,X4)
| def39(X0,X1,X2,X3)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14276,c276]) ).
cnf(c33,plain,
( def10
| ~ def11 ),
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])],[f0_sk]) ).
cnf(p1874,plain,
def10,
inference(resolution,[status(thm)],[p1873,c33]) ).
cnf(c31,plain,
( barrel(sk1,sk3)
| ~ def10 ),
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])],[f0_sk]) ).
cnf(p1877,plain,
barrel(sk1,sk3),
inference(resolution,[status(thm)],[p1874,c31]) ).
cnf(p14616,plain,
( def91(sk0,sk1,sk2,sk3)
| def39(X0,X1,X2,X3)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14279,p1877]) ).
cnf(p14618,plain,
( ~ old(sk3)
| def90(sk0,sk1,sk2,sk3)
| def39(X0,X1,X2,X3)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14616,c273]) ).
cnf(c30,plain,
( def9
| ~ def10 ),
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])],[f0_sk]) ).
cnf(p1876,plain,
def9,
inference(resolution,[status(thm)],[p1874,c30]) ).
cnf(c28,plain,
( old(sk3)
| ~ def9 ),
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])],[f0_sk]) ).
cnf(p1879,plain,
old(sk3),
inference(resolution,[status(thm)],[p1876,c28]) ).
cnf(p14623,plain,
( def90(sk0,sk1,sk2,sk3)
| def39(X0,X1,X2,X3)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14618,p1879]) ).
cnf(p14625,plain,
( ~ dirty(sk3)
| def89(sk0,sk1,sk2,sk3)
| def39(X0,X1,X2,X3)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14623,c270]) ).
cnf(c27,plain,
( def8
| ~ def9 ),
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])],[f0_sk]) ).
cnf(p1878,plain,
def8,
inference(resolution,[status(thm)],[p1876,c27]) ).
cnf(c25,plain,
( dirty(sk3)
| ~ def8 ),
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])],[f0_sk]) ).
cnf(p1880,plain,
dirty(sk3),
inference(resolution,[status(thm)],[p1878,c25]) ).
cnf(p14631,plain,
( def89(sk0,sk1,sk2,sk3)
| def39(X0,X1,X2,X3)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14625,p1880]) ).
cnf(p14633,plain,
( ~ white(sk3)
| def88(sk0,sk1,sk2,sk3)
| def39(X0,X1,X2,X3)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14631,c267]) ).
cnf(c24,plain,
( def7
| ~ def8 ),
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])],[f0_sk]) ).
cnf(p1881,plain,
def7,
inference(resolution,[status(thm)],[p1878,c24]) ).
cnf(c22,plain,
( white(sk3)
| ~ def7 ),
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])],[f0_sk]) ).
cnf(p1883,plain,
white(sk3),
inference(resolution,[status(thm)],[p1881,c22]) ).
cnf(p14640,plain,
( def88(sk0,sk1,sk2,sk3)
| def39(X0,X1,X2,X3)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14633,p1883]) ).
cnf(p14642,plain,
( ~ car(sk3)
| def87(sk0,sk1,sk2,sk3)
| def39(X0,X1,X2,X3)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14640,c264]) ).
cnf(c21,plain,
( def6
| ~ def7 ),
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])],[f0_sk]) ).
cnf(p1882,plain,
def6,
inference(resolution,[status(thm)],[p1881,c21]) ).
cnf(c19,plain,
( car(sk3)
| ~ def6 ),
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])],[f0_sk]) ).
cnf(p1885,plain,
car(sk3),
inference(resolution,[status(thm)],[p1882,c19]) ).
cnf(p14650,plain,
( def87(sk0,sk1,sk2,sk3)
| def39(X0,X1,X2,X3)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14642,p1885]) ).
cnf(p14652,plain,
( ~ chevy(sk3)
| def86(sk0,sk1,sk2)
| def39(X0,X1,X2,X3)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14650,c261]) ).
cnf(c18,plain,
( def5
| ~ def6 ),
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])],[f0_sk]) ).
cnf(p1884,plain,
def5,
inference(resolution,[status(thm)],[p1882,c18]) ).
cnf(c16,plain,
( chevy(sk3)
| ~ def5 ),
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])],[f0_sk]) ).
cnf(p1887,plain,
chevy(sk3),
inference(resolution,[status(thm)],[p1884,c16]) ).
cnf(p14657,plain,
( def86(sk0,sk1,sk2)
| def39(X0,X1,X2,X3)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14652,p1887]) ).
cnf(c117,plain,
( ~ in(X10,X9)
| def38(X9,X10,X11,X12)
| ~ def39(X9,X10,X11,X12) ),
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])],[f0_sk]) ).
cnf(p14659,plain,
( ~ in(X1,X0)
| def38(X0,X1,X2,X3)
| def86(sk0,sk1,sk2)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14657,c117]) ).
cnf(p14677,plain,
( def38(sk0,sk1,X0,X1)
| def86(sk0,sk1,sk2)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14659,p1872]) ).
cnf(c114,plain,
( ~ down(X10,X12)
| def37(X9,X10,X11,X12)
| ~ def38(X9,X10,X11,X12) ),
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])],[f0_sk]) ).
cnf(p14687,plain,
( ~ down(sk1,X1)
| def37(sk0,sk1,X0,X1)
| def86(sk0,sk1,sk2)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14677,c114]) ).
cnf(p14703,plain,
( def37(sk0,sk1,X0,sk2)
| def86(sk0,sk1,sk2)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14687,p1875]) ).
cnf(c111,plain,
( ~ barrel(X10,X11)
| def36(X9,X10,X11,X12)
| ~ def37(X9,X10,X11,X12) ),
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])],[f0_sk]) ).
cnf(p14704,plain,
( ~ barrel(sk1,X0)
| def36(sk0,sk1,X0,sk2)
| def86(sk0,sk1,sk2)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14703,c111]) ).
cnf(p14715,plain,
( def36(sk0,sk1,sk3,sk2)
| def86(sk0,sk1,sk2)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14704,p1877]) ).
cnf(c108,plain,
( ~ lonely(X12)
| def35(X9,X10,X11,X12)
| ~ def36(X9,X10,X11,X12) ),
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])],[f0_sk]) ).
cnf(p14716,plain,
( ~ lonely(sk2)
| def35(sk0,sk1,sk3,sk2)
| def86(sk0,sk1,sk2)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14715,c108]) ).
cnf(c15,plain,
( def4
| ~ def5 ),
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])],[f0_sk]) ).
cnf(p1886,plain,
def4,
inference(resolution,[status(thm)],[p1884,c15]) ).
cnf(c13,plain,
( lonely(sk2)
| ~ def4 ),
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])],[f0_sk]) ).
cnf(p1889,plain,
lonely(sk2),
inference(resolution,[status(thm)],[p1886,c13]) ).
cnf(p14717,plain,
( def35(sk0,sk1,sk3,sk2)
| def86(sk0,sk1,sk2)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14716,p1889]) ).
cnf(c105,plain,
( ~ way(X12)
| def34(X9,X10,X11,X12)
| ~ def35(X9,X10,X11,X12) ),
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])],[f0_sk]) ).
cnf(p14718,plain,
( ~ way(sk2)
| def34(sk0,sk1,sk3,sk2)
| def86(sk0,sk1,sk2)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14717,c105]) ).
cnf(c12,plain,
( def3
| ~ def4 ),
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])],[f0_sk]) ).
cnf(p1888,plain,
def3,
inference(resolution,[status(thm)],[p1886,c12]) ).
cnf(c10,plain,
( way(sk2)
| ~ def3 ),
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])],[f0_sk]) ).
cnf(p1891,plain,
way(sk2),
inference(resolution,[status(thm)],[p1888,c10]) ).
cnf(p14719,plain,
( def34(sk0,sk1,sk3,sk2)
| def86(sk0,sk1,sk2)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14718,p1891]) ).
cnf(c102,plain,
( ~ street(X12)
| def33(X9,X10,X11)
| ~ def34(X9,X10,X11,X12) ),
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])],[f0_sk]) ).
cnf(p14720,plain,
( ~ street(sk2)
| def33(sk0,sk1,sk3)
| def86(sk0,sk1,sk2)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14719,c102]) ).
cnf(c9,plain,
( def2
| ~ def3 ),
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])],[f0_sk]) ).
cnf(p1890,plain,
def2,
inference(resolution,[status(thm)],[p1888,c9]) ).
cnf(c7,plain,
( street(sk2)
| ~ def2 ),
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])],[f0_sk]) ).
cnf(p1893,plain,
street(sk2),
inference(resolution,[status(thm)],[p1890,c7]) ).
cnf(p14721,plain,
( def33(sk0,sk1,sk3)
| def86(sk0,sk1,sk2)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14720,p1893]) ).
cnf(p14723,plain,
( ~ lonely(sk2)
| def85(sk0,sk1,sk2)
| def33(sk0,sk1,sk3)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14721,c258]) ).
cnf(p14735,plain,
( def85(sk0,sk1,sk2)
| def33(sk0,sk1,sk3)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14723,p1889]) ).
cnf(p14736,plain,
( ~ way(sk2)
| def84(sk0,sk1,sk2)
| def33(sk0,sk1,sk3)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14735,c255]) ).
cnf(p14737,plain,
( def84(sk0,sk1,sk2)
| def33(sk0,sk1,sk3)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14736,p1891]) ).
cnf(p14738,plain,
( ~ street(sk2)
| def83(sk0,sk1)
| def33(sk0,sk1,sk3)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14737,c252]) ).
cnf(p14739,plain,
( def83(sk0,sk1)
| def33(sk0,sk1,sk3)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14738,p1893]) ).
cnf(c99,plain,
( ~ old(X11)
| def32(X9,X10,X11)
| ~ def33(X9,X10,X11) ),
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])],[f0_sk]) ).
cnf(p14741,plain,
( ~ old(sk3)
| def32(sk0,sk1,sk3)
| def83(sk0,sk1)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14739,c99]) ).
cnf(p14751,plain,
( def32(sk0,sk1,sk3)
| def83(sk0,sk1)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14741,p1879]) ).
cnf(c96,plain,
( ~ dirty(X11)
| def31(X9,X10,X11)
| ~ def32(X9,X10,X11) ),
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])],[f0_sk]) ).
cnf(p14752,plain,
( ~ dirty(sk3)
| def31(sk0,sk1,sk3)
| def83(sk0,sk1)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14751,c96]) ).
cnf(p14753,plain,
( def31(sk0,sk1,sk3)
| def83(sk0,sk1)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14752,p1880]) ).
cnf(c93,plain,
( ~ white(X11)
| def30(X9,X10,X11)
| ~ def31(X9,X10,X11) ),
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])],[f0_sk]) ).
cnf(p14754,plain,
( ~ white(sk3)
| def30(sk0,sk1,sk3)
| def83(sk0,sk1)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14753,c93]) ).
cnf(p14755,plain,
( def30(sk0,sk1,sk3)
| def83(sk0,sk1)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14754,p1883]) ).
cnf(c90,plain,
( ~ car(X11)
| def29(X9,X10,X11)
| ~ def30(X9,X10,X11) ),
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])],[f0_sk]) ).
cnf(p14756,plain,
( ~ car(sk3)
| def29(sk0,sk1,sk3)
| def83(sk0,sk1)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14755,c90]) ).
cnf(p14757,plain,
( def29(sk0,sk1,sk3)
| def83(sk0,sk1)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14756,p1885]) ).
cnf(c87,plain,
( ~ chevy(X11)
| def28(X9,X10)
| ~ def29(X9,X10,X11) ),
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])],[f0_sk]) ).
cnf(p14758,plain,
( ~ chevy(sk3)
| def28(sk0,sk1)
| def83(sk0,sk1)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14757,c87]) ).
cnf(p14759,plain,
( def28(sk0,sk1)
| def83(sk0,sk1)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14758,p1887]) ).
cnf(p14761,plain,
( ~ event(sk1)
| def82(sk0)
| def28(sk0,sk1)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14759,c249]) ).
cnf(c6,plain,
( def1
| ~ def2 ),
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])],[f0_sk]) ).
cnf(p1892,plain,
def1,
inference(resolution,[status(thm)],[p1890,c6]) ).
cnf(c4,plain,
( event(sk1)
| ~ def1 ),
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])],[f0_sk]) ).
cnf(p1895,plain,
event(sk1),
inference(resolution,[status(thm)],[p1892,c4]) ).
cnf(p14765,plain,
( def82(sk0)
| def28(sk0,sk1)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14761,p1895]) ).
cnf(c84,plain,
( ~ event(X10)
| def27(X9)
| ~ def28(X9,X10) ),
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])],[f0_sk]) ).
cnf(p14767,plain,
( ~ event(sk1)
| def27(sk0)
| def82(sk0)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14765,c84]) ).
cnf(p14773,plain,
( def27(sk0)
| def82(sk0)
| sk4 = sk5 ),
inference(resolution,[status(thm)],[p14767,p1895]) ).
cnf(c49,plain,
( sk4 != sk5
| ~ def16 ),
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])],[f0_sk]) ).
cnf(p1864,plain,
sk4 != sk5,
inference(resolution,[status(thm)],[p1862,c49]) ).
cnf(p14777,plain,
( def27(sk0)
| def82(sk0) ),
inference(resolution,[status(thm)],[p14773,p1864]) ).
cnf(p14779,plain,
( ~ city(sk0)
| ~ hollywood(sk0)
| def27(sk0) ),
inference(resolution,[status(thm)],[p14777,c246]) ).
cnf(c3,plain,
( def0
| ~ def1 ),
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])],[f0_sk]) ).
cnf(p1894,plain,
def0,
inference(resolution,[status(thm)],[p1892,c3]) ).
cnf(c0,plain,
( hollywood(sk0)
| ~ def0 ),
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])],[f0_sk]) ).
cnf(p1896,plain,
hollywood(sk0),
inference(resolution,[status(thm)],[p1894,c0]) ).
cnf(p14784,plain,
( ~ city(sk0)
| def27(sk0) ),
inference(resolution,[status(thm)],[p14779,p1896]) ).
cnf(c1,plain,
( city(sk0)
| ~ def0 ),
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])],[f0_sk]) ).
cnf(p1897,plain,
city(sk0),
inference(resolution,[status(thm)],[p1894,c1]) ).
cnf(p14785,plain,
def27(sk0),
inference(resolution,[status(thm)],[p14784,p1897]) ).
cnf(c81,plain,
( ~ city(X9)
| ~ hollywood(X9)
| ~ def27(X9) ),
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])],[f0_sk]) ).
cnf(p14787,plain,
( ~ city(sk0)
| ~ hollywood(sk0) ),
inference(resolution,[status(thm)],[p14785,c81]) ).
cnf(p14794,plain,
~ city(sk0),
inference(resolution,[status(thm)],[p14787,p1896]) ).
cnf(p14795,plain,
$false,
inference(resolution,[status(thm)],[p14794,p1897]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP009+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n008.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 01:38:39 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 49.02/6.70 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 49.02/6.70 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------