%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NLP011+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n007.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 : Tue Sep 29 12:08:24 PM UTC 2026
% Result : Theorem 0.17s 0.47s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 81
% Syntax : Number of formulae : 466 ( 43 unt; 80 def)
% Number of atoms : 2327 ( 120 equ)
% Maximal formula atoms : 124 ( 4 avg)
% Number of connectives : 2907 (1046 ~;1261 |; 518 &)
% ( 78 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 83 ( 6 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 102 ( 100 usr; 81 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 20 con; 0-0 aty)
% Number of variables : 386 ( 0 sgn 236 !; 150 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
( ( ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( seat(X0)
& furniture(X0)
& front(X0)
& hollywood(X1)
& city(X1)
& event(X2)
& street(X3)
& way(X3)
& lonely(X3)
& chevy(X4)
& car(X4)
& white(X4)
& dirty(X4)
& old(X4)
& barrel(X2,X4)
& down(X2,X3)
& in(X2,X1)
& seat(X7)
& furniture(X7)
& front(X7)
& X5 != X6
& fellow(X5)
& man(X5)
& young(X5)
& fellow(X6)
& man(X6)
& young(X6)
& X5 = X8
& in(X8,X7)
& X6 = X9
& in(X9,X0) )
=> ? [X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
( seat(X10)
& furniture(X10)
& front(X10)
& hollywood(X11)
& city(X11)
& event(X12)
& street(X13)
& way(X13)
& lonely(X13)
& chevy(X14)
& car(X14)
& white(X14)
& dirty(X14)
& old(X14)
& barrel(X12,X14)
& down(X12,X13)
& in(X12,X11)
& seat(X17)
& furniture(X17)
& front(X17)
& X15 != X16
& fellow(X15)
& man(X15)
& young(X15)
& fellow(X16)
& man(X16)
& young(X16)
& X15 = X18
& in(X18,X10)
& X16 = X19
& in(X19,X17) ) )
& ( ? [X20,X21,X22,X23,X24,X25,X26,X27,X28,X29] :
( seat(X20)
& furniture(X20)
& front(X20)
& hollywood(X21)
& city(X21)
& event(X22)
& street(X23)
& way(X23)
& lonely(X23)
& chevy(X24)
& car(X24)
& white(X24)
& dirty(X24)
& old(X24)
& barrel(X22,X24)
& down(X22,X23)
& in(X22,X21)
& seat(X27)
& furniture(X27)
& front(X27)
& X25 != X26
& fellow(X25)
& man(X25)
& young(X25)
& fellow(X26)
& man(X26)
& young(X26)
& X25 = X28
& in(X28,X20)
& X26 = X29
& in(X29,X27) )
=> ? [X30,X31,X32,X33,X34,X35,X36,X37,X38,X39] :
( seat(X30)
& furniture(X30)
& front(X30)
& hollywood(X31)
& city(X31)
& event(X32)
& street(X33)
& way(X33)
& lonely(X33)
& chevy(X34)
& car(X34)
& white(X34)
& dirty(X34)
& old(X34)
& barrel(X32,X34)
& down(X32,X33)
& in(X32,X31)
& seat(X37)
& furniture(X37)
& front(X37)
& X35 != X36
& fellow(X35)
& man(X35)
& young(X35)
& fellow(X36)
& man(X36)
& young(X36)
& X35 = X38
& in(X38,X37)
& X36 = X39
& in(X39,X30) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f2,negated_conjecture,
~ ( ( ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( seat(X0)
& furniture(X0)
& front(X0)
& hollywood(X1)
& city(X1)
& event(X2)
& street(X3)
& way(X3)
& lonely(X3)
& chevy(X4)
& car(X4)
& white(X4)
& dirty(X4)
& old(X4)
& barrel(X2,X4)
& down(X2,X3)
& in(X2,X1)
& seat(X7)
& furniture(X7)
& front(X7)
& X5 != X6
& fellow(X5)
& man(X5)
& young(X5)
& fellow(X6)
& man(X6)
& young(X6)
& X5 = X8
& in(X8,X7)
& X6 = X9
& in(X9,X0) )
=> ? [X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
( seat(X10)
& furniture(X10)
& front(X10)
& hollywood(X11)
& city(X11)
& event(X12)
& street(X13)
& way(X13)
& lonely(X13)
& chevy(X14)
& car(X14)
& white(X14)
& dirty(X14)
& old(X14)
& barrel(X12,X14)
& down(X12,X13)
& in(X12,X11)
& seat(X17)
& furniture(X17)
& front(X17)
& X15 != X16
& fellow(X15)
& man(X15)
& young(X15)
& fellow(X16)
& man(X16)
& young(X16)
& X15 = X18
& in(X18,X10)
& X16 = X19
& in(X19,X17) ) )
& ( ? [X20,X21,X22,X23,X24,X25,X26,X27,X28,X29] :
( seat(X20)
& furniture(X20)
& front(X20)
& hollywood(X21)
& city(X21)
& event(X22)
& street(X23)
& way(X23)
& lonely(X23)
& chevy(X24)
& car(X24)
& white(X24)
& dirty(X24)
& old(X24)
& barrel(X22,X24)
& down(X22,X23)
& in(X22,X21)
& seat(X27)
& furniture(X27)
& front(X27)
& X25 != X26
& fellow(X25)
& man(X25)
& young(X25)
& fellow(X26)
& man(X26)
& young(X26)
& X25 = X28
& in(X28,X20)
& X26 = X29
& in(X29,X27) )
=> ? [X30,X31,X32,X33,X34,X35,X36,X37,X38,X39] :
( seat(X30)
& furniture(X30)
& front(X30)
& hollywood(X31)
& city(X31)
& event(X32)
& street(X33)
& way(X33)
& lonely(X33)
& chevy(X34)
& car(X34)
& white(X34)
& dirty(X34)
& old(X34)
& barrel(X32,X34)
& down(X32,X33)
& in(X32,X31)
& seat(X37)
& furniture(X37)
& front(X37)
& X35 != X36
& fellow(X35)
& man(X35)
& young(X35)
& fellow(X36)
& man(X36)
& young(X36)
& X35 = X38
& in(X38,X37)
& X36 = X39
& in(X39,X30) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
( ( ! [X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
( ~ seat(X10)
| ~ furniture(X10)
| ~ front(X10)
| ~ hollywood(X11)
| ~ city(X11)
| ~ event(X12)
| ~ street(X13)
| ~ way(X13)
| ~ lonely(X13)
| ~ chevy(X14)
| ~ car(X14)
| ~ white(X14)
| ~ dirty(X14)
| ~ old(X14)
| ~ barrel(X12,X14)
| ~ down(X12,X13)
| ~ in(X12,X11)
| ~ seat(X17)
| ~ furniture(X17)
| ~ front(X17)
| X15 = X16
| ~ fellow(X15)
| ~ man(X15)
| ~ young(X15)
| ~ fellow(X16)
| ~ man(X16)
| ~ young(X16)
| X15 != X18
| ~ in(X18,X10)
| X16 != X19
| ~ in(X19,X17) )
& ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( seat(X0)
& furniture(X0)
& front(X0)
& hollywood(X1)
& city(X1)
& event(X2)
& street(X3)
& way(X3)
& lonely(X3)
& chevy(X4)
& car(X4)
& white(X4)
& dirty(X4)
& old(X4)
& barrel(X2,X4)
& down(X2,X3)
& in(X2,X1)
& seat(X7)
& furniture(X7)
& front(X7)
& X5 != X6
& fellow(X5)
& man(X5)
& young(X5)
& fellow(X6)
& man(X6)
& young(X6)
& X5 = X8
& in(X8,X7)
& X6 = X9
& in(X9,X0) ) )
| ( ! [X30,X31,X32,X33,X34,X35,X36,X37,X38,X39] :
( ~ seat(X30)
| ~ furniture(X30)
| ~ front(X30)
| ~ hollywood(X31)
| ~ city(X31)
| ~ event(X32)
| ~ street(X33)
| ~ way(X33)
| ~ lonely(X33)
| ~ chevy(X34)
| ~ car(X34)
| ~ white(X34)
| ~ dirty(X34)
| ~ old(X34)
| ~ barrel(X32,X34)
| ~ down(X32,X33)
| ~ in(X32,X31)
| ~ seat(X37)
| ~ furniture(X37)
| ~ front(X37)
| X35 = X36
| ~ fellow(X35)
| ~ man(X35)
| ~ young(X35)
| ~ fellow(X36)
| ~ man(X36)
| ~ young(X36)
| X35 != X38
| ~ in(X38,X37)
| X36 != X39
| ~ in(X39,X30) )
& ? [X20,X21,X22,X23,X24,X25,X26,X27,X28,X29] :
( seat(X20)
& furniture(X20)
& front(X20)
& hollywood(X21)
& city(X21)
& event(X22)
& street(X23)
& way(X23)
& lonely(X23)
& chevy(X24)
& car(X24)
& white(X24)
& dirty(X24)
& old(X24)
& barrel(X22,X24)
& down(X22,X23)
& in(X22,X21)
& seat(X27)
& furniture(X27)
& front(X27)
& X25 != X26
& fellow(X25)
& man(X25)
& young(X25)
& fellow(X26)
& man(X26)
& young(X26)
& X25 = X28
& in(X28,X20)
& X26 = X29
& in(X29,X27) ) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f4,definition,
( ? [X20,X21,X22,X23,X24,X25,X26,X27,X28,X29] :
( seat(X20)
& furniture(X20)
& front(X20)
& hollywood(X21)
& city(X21)
& event(X22)
& street(X23)
& way(X23)
& lonely(X23)
& chevy(X24)
& car(X24)
& white(X24)
& dirty(X24)
& old(X24)
& barrel(X22,X24)
& down(X22,X23)
& in(X22,X21)
& seat(X27)
& furniture(X27)
& front(X27)
& X25 != X26
& fellow(X25)
& man(X25)
& young(X25)
& fellow(X26)
& man(X26)
& young(X26)
& X25 = X28
& in(X28,X20)
& X26 = X29
& in(X29,X27) )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f5,definition,
( ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( seat(X0)
& furniture(X0)
& front(X0)
& hollywood(X1)
& city(X1)
& event(X2)
& street(X3)
& way(X3)
& lonely(X3)
& chevy(X4)
& car(X4)
& white(X4)
& dirty(X4)
& old(X4)
& barrel(X2,X4)
& down(X2,X3)
& in(X2,X1)
& seat(X7)
& furniture(X7)
& front(X7)
& X5 != X6
& fellow(X5)
& man(X5)
& young(X5)
& fellow(X6)
& man(X6)
& young(X6)
& X5 = X8
& in(X8,X7)
& X6 = X9
& in(X9,X0) )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f6,plain,
( ( ! [X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
( ~ seat(X10)
| ~ furniture(X10)
| ~ front(X10)
| ~ hollywood(X11)
| ~ city(X11)
| ~ event(X12)
| ~ street(X13)
| ~ way(X13)
| ~ lonely(X13)
| ~ chevy(X14)
| ~ car(X14)
| ~ white(X14)
| ~ dirty(X14)
| ~ old(X14)
| ~ barrel(X12,X14)
| ~ down(X12,X13)
| ~ in(X12,X11)
| ~ seat(X17)
| ~ furniture(X17)
| ~ front(X17)
| X15 = X16
| ~ fellow(X15)
| ~ man(X15)
| ~ young(X15)
| ~ fellow(X16)
| ~ man(X16)
| ~ young(X16)
| X15 != X18
| ~ in(X18,X10)
| X16 != X19
| ~ in(X19,X17) )
& sP1 )
| ( ! [X30,X31,X32,X33,X34,X35,X36,X37,X38,X39] :
( ~ seat(X30)
| ~ furniture(X30)
| ~ front(X30)
| ~ hollywood(X31)
| ~ city(X31)
| ~ event(X32)
| ~ street(X33)
| ~ way(X33)
| ~ lonely(X33)
| ~ chevy(X34)
| ~ car(X34)
| ~ white(X34)
| ~ dirty(X34)
| ~ old(X34)
| ~ barrel(X32,X34)
| ~ down(X32,X33)
| ~ in(X32,X31)
| ~ seat(X37)
| ~ furniture(X37)
| ~ front(X37)
| X35 = X36
| ~ fellow(X35)
| ~ man(X35)
| ~ young(X35)
| ~ fellow(X36)
| ~ man(X36)
| ~ young(X36)
| X35 != X38
| ~ in(X38,X37)
| X36 != X39
| ~ in(X39,X30) )
& sP0 ) ),
inference(definition_folding,[],[f3,f5,f4]) ).
fof(f7,plain,
( ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( seat(X0)
& furniture(X0)
& front(X0)
& hollywood(X1)
& city(X1)
& event(X2)
& street(X3)
& way(X3)
& lonely(X3)
& chevy(X4)
& car(X4)
& white(X4)
& dirty(X4)
& old(X4)
& barrel(X2,X4)
& down(X2,X3)
& in(X2,X1)
& seat(X7)
& furniture(X7)
& front(X7)
& X5 != X6
& fellow(X5)
& man(X5)
& young(X5)
& fellow(X6)
& man(X6)
& young(X6)
& X5 = X8
& in(X8,X7)
& X6 = X9
& in(X9,X0) )
| ~ sP1 ),
inference(nnf_transformation,[],[f5]) ).
fof(f8,plain,
( ( seat(sK2)
& furniture(sK2)
& front(sK2)
& hollywood(sK3)
& city(sK3)
& event(sK4)
& street(sK5)
& way(sK5)
& lonely(sK5)
& chevy(sK6)
& car(sK6)
& white(sK6)
& dirty(sK6)
& old(sK6)
& barrel(sK4,sK6)
& down(sK4,sK5)
& in(sK4,sK3)
& seat(sK9)
& furniture(sK9)
& front(sK9)
& sK7 != sK8
& fellow(sK7)
& man(sK7)
& young(sK7)
& fellow(sK8)
& man(sK8)
& young(sK8)
& sK7 = sK10
& in(sK10,sK9)
& sK8 = sK11
& in(sK11,sK2) )
| ~ sP1 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4),skolemize(X3,sK5),skolemize(X4,sK6),skolemize(X5,sK7),skolemize(X6,sK8),skolemize(X7,sK9),skolemize(X8,sK10),skolemize(X9,sK11)],[f7]) ).
fof(f9,plain,
( ? [X20,X21,X22,X23,X24,X25,X26,X27,X28,X29] :
( seat(X20)
& furniture(X20)
& front(X20)
& hollywood(X21)
& city(X21)
& event(X22)
& street(X23)
& way(X23)
& lonely(X23)
& chevy(X24)
& car(X24)
& white(X24)
& dirty(X24)
& old(X24)
& barrel(X22,X24)
& down(X22,X23)
& in(X22,X21)
& seat(X27)
& furniture(X27)
& front(X27)
& X25 != X26
& fellow(X25)
& man(X25)
& young(X25)
& fellow(X26)
& man(X26)
& young(X26)
& X25 = X28
& in(X28,X20)
& X26 = X29
& in(X29,X27) )
| ~ sP0 ),
inference(nnf_transformation,[],[f4]) ).
fof(f10,plain,
( ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( seat(X0)
& furniture(X0)
& front(X0)
& hollywood(X1)
& city(X1)
& event(X2)
& street(X3)
& way(X3)
& lonely(X3)
& chevy(X4)
& car(X4)
& white(X4)
& dirty(X4)
& old(X4)
& barrel(X2,X4)
& down(X2,X3)
& in(X2,X1)
& seat(X7)
& furniture(X7)
& front(X7)
& X5 != X6
& fellow(X5)
& man(X5)
& young(X5)
& fellow(X6)
& man(X6)
& young(X6)
& X5 = X8
& in(X8,X0)
& X6 = X9
& in(X9,X7) )
| ~ sP0 ),
inference(rectify,[],[f9]) ).
fof(f11,plain,
( ( seat(sK12)
& furniture(sK12)
& front(sK12)
& hollywood(sK13)
& city(sK13)
& event(sK14)
& street(sK15)
& way(sK15)
& lonely(sK15)
& chevy(sK16)
& car(sK16)
& white(sK16)
& dirty(sK16)
& old(sK16)
& barrel(sK14,sK16)
& down(sK14,sK15)
& in(sK14,sK13)
& seat(sK19)
& furniture(sK19)
& front(sK19)
& sK17 != sK18
& fellow(sK17)
& man(sK17)
& young(sK17)
& fellow(sK18)
& man(sK18)
& young(sK18)
& sK17 = sK20
& in(sK20,sK12)
& sK18 = sK21
& in(sK21,sK19) )
| ~ sP0 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12,sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21]),skolemize(X0,sK12),skolemize(X1,sK13),skolemize(X2,sK14),skolemize(X3,sK15),skolemize(X4,sK16),skolemize(X5,sK17),skolemize(X6,sK18),skolemize(X7,sK19),skolemize(X8,sK20),skolemize(X9,sK21)],[f10]) ).
fof(f12,plain,
( ( ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ hollywood(X1)
| ~ city(X1)
| ~ event(X2)
| ~ street(X3)
| ~ way(X3)
| ~ lonely(X3)
| ~ chevy(X4)
| ~ car(X4)
| ~ white(X4)
| ~ dirty(X4)
| ~ old(X4)
| ~ barrel(X2,X4)
| ~ down(X2,X3)
| ~ in(X2,X1)
| ~ seat(X7)
| ~ furniture(X7)
| ~ front(X7)
| X5 = X6
| ~ fellow(X5)
| ~ man(X5)
| ~ young(X5)
| ~ fellow(X6)
| ~ man(X6)
| ~ young(X6)
| X5 != X8
| ~ in(X8,X0)
| X6 != X9
| ~ in(X9,X7) )
& sP1 )
| ( ! [X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
( ~ seat(X10)
| ~ furniture(X10)
| ~ front(X10)
| ~ hollywood(X11)
| ~ city(X11)
| ~ event(X12)
| ~ street(X13)
| ~ way(X13)
| ~ lonely(X13)
| ~ chevy(X14)
| ~ car(X14)
| ~ white(X14)
| ~ dirty(X14)
| ~ old(X14)
| ~ barrel(X12,X14)
| ~ down(X12,X13)
| ~ in(X12,X11)
| ~ seat(X17)
| ~ furniture(X17)
| ~ front(X17)
| X15 = X16
| ~ fellow(X15)
| ~ man(X15)
| ~ young(X15)
| ~ fellow(X16)
| ~ man(X16)
| ~ young(X16)
| X15 != X18
| ~ in(X18,X17)
| X16 != X19
| ~ in(X19,X10) )
& sP0 ) ),
inference(rectify,[],[f6]) ).
fof(f13,plain,
( in(sK11,sK2)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f14,plain,
( sK8 = sK11
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f15,plain,
( in(sK10,sK9)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f16,plain,
( sK7 = sK10
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f17,plain,
( young(sK8)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f18,plain,
( man(sK8)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f19,plain,
( fellow(sK8)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f20,plain,
( young(sK7)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f21,plain,
( man(sK7)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f22,plain,
( fellow(sK7)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f23,plain,
( sK7 != sK8
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f24,plain,
( front(sK9)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f25,plain,
( furniture(sK9)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f26,plain,
( seat(sK9)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f27,plain,
( in(sK4,sK3)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f28,plain,
( down(sK4,sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f29,plain,
( barrel(sK4,sK6)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f30,plain,
( old(sK6)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f31,plain,
( dirty(sK6)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f32,plain,
( white(sK6)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f33,plain,
( car(sK6)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f34,plain,
( chevy(sK6)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f35,plain,
( lonely(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f36,plain,
( way(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f37,plain,
( street(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f38,plain,
( event(sK4)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f39,plain,
( city(sK3)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f40,plain,
( hollywood(sK3)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f41,plain,
( front(sK2)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f42,plain,
( furniture(sK2)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f43,plain,
( seat(sK2)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f44,plain,
( in(sK21,sK19)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f45,plain,
( sK18 = sK21
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f46,plain,
( in(sK20,sK12)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f47,plain,
( sK17 = sK20
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f48,plain,
( young(sK18)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f49,plain,
( man(sK18)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f50,plain,
( fellow(sK18)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f51,plain,
( young(sK17)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f52,plain,
( man(sK17)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f53,plain,
( fellow(sK17)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f54,plain,
( sK17 != sK18
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f55,plain,
( front(sK19)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f56,plain,
( furniture(sK19)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f57,plain,
( seat(sK19)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f58,plain,
( in(sK14,sK13)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f59,plain,
( down(sK14,sK15)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f60,plain,
( barrel(sK14,sK16)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f61,plain,
( old(sK16)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f62,plain,
( dirty(sK16)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f63,plain,
( white(sK16)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f64,plain,
( car(sK16)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f65,plain,
( chevy(sK16)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f66,plain,
( lonely(sK15)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f67,plain,
( way(sK15)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f68,plain,
( street(sK15)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f69,plain,
( event(sK14)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f70,plain,
( city(sK13)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f71,plain,
( hollywood(sK13)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f72,plain,
( front(sK12)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f73,plain,
( furniture(sK12)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f74,plain,
( seat(sK12)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f75,plain,
( sP1
| sP0 ),
inference(cnf_transformation,[],[f12]) ).
fof(f78,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] :
( ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ hollywood(X1)
| ~ city(X1)
| ~ event(X2)
| ~ street(X3)
| ~ way(X3)
| ~ lonely(X3)
| ~ chevy(X4)
| ~ car(X4)
| ~ white(X4)
| ~ dirty(X4)
| ~ old(X4)
| ~ barrel(X2,X4)
| ~ down(X2,X3)
| ~ in(X2,X1)
| ~ seat(X7)
| ~ furniture(X7)
| ~ front(X7)
| X5 = X6
| ~ fellow(X5)
| ~ man(X5)
| ~ young(X5)
| ~ fellow(X6)
| ~ man(X6)
| ~ young(X6)
| X5 != X8
| ~ in(X8,X0)
| X6 != X9
| ~ in(X9,X7)
| ~ seat(X10)
| ~ furniture(X10)
| ~ front(X10)
| ~ hollywood(X11)
| ~ city(X11)
| ~ event(X12)
| ~ street(X13)
| ~ way(X13)
| ~ lonely(X13)
| ~ chevy(X14)
| ~ car(X14)
| ~ white(X14)
| ~ dirty(X14)
| ~ old(X14)
| ~ barrel(X12,X14)
| ~ down(X12,X13)
| ~ in(X12,X11)
| ~ seat(X17)
| ~ furniture(X17)
| ~ front(X17)
| X15 = X16
| ~ fellow(X15)
| ~ man(X15)
| ~ young(X15)
| ~ fellow(X16)
| ~ man(X16)
| ~ young(X16)
| X15 != X18
| ~ in(X18,X17)
| X16 != X19
| ~ in(X19,X10) ),
inference(cnf_transformation,[],[f12]) ).
fof(f79,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X12,X13] :
( ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ hollywood(X1)
| ~ city(X1)
| ~ event(X2)
| ~ street(X3)
| ~ way(X3)
| ~ lonely(X3)
| ~ chevy(X4)
| ~ car(X4)
| ~ white(X4)
| ~ dirty(X4)
| ~ old(X4)
| ~ barrel(X2,X4)
| ~ down(X2,X3)
| ~ in(X2,X1)
| ~ seat(X7)
| ~ furniture(X7)
| ~ front(X7)
| X6 = X8
| ~ fellow(X8)
| ~ man(X8)
| ~ young(X8)
| ~ fellow(X6)
| ~ man(X6)
| ~ young(X6)
| ~ in(X8,X0)
| X6 != X9
| ~ in(X9,X7)
| ~ seat(X10)
| ~ furniture(X10)
| ~ front(X10)
| ~ hollywood(X11)
| ~ city(X11)
| ~ event(X12)
| ~ street(X13)
| ~ way(X13)
| ~ lonely(X13)
| ~ chevy(X14)
| ~ car(X14)
| ~ white(X14)
| ~ dirty(X14)
| ~ old(X14)
| ~ barrel(X12,X14)
| ~ down(X12,X13)
| ~ in(X12,X11)
| ~ seat(X17)
| ~ furniture(X17)
| ~ front(X17)
| X15 = X16
| ~ fellow(X15)
| ~ man(X15)
| ~ young(X15)
| ~ fellow(X16)
| ~ man(X16)
| ~ young(X16)
| X15 != X18
| ~ in(X18,X17)
| X16 != X19
| ~ in(X19,X10) ),
inference(equality_resolution,[],[f78]) ).
fof(f80,plain,
! [X2,X3,X10,X0,X11,X1,X8,X18,X9,X7,X14,X4,X16,X19,X17,X15,X12,X13] :
( ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ hollywood(X1)
| ~ city(X1)
| ~ event(X2)
| ~ street(X3)
| ~ way(X3)
| ~ lonely(X3)
| ~ chevy(X4)
| ~ car(X4)
| ~ white(X4)
| ~ dirty(X4)
| ~ old(X4)
| ~ barrel(X2,X4)
| ~ down(X2,X3)
| ~ in(X2,X1)
| ~ seat(X7)
| ~ furniture(X7)
| ~ front(X7)
| X8 = X9
| ~ fellow(X8)
| ~ man(X8)
| ~ young(X8)
| ~ fellow(X9)
| ~ man(X9)
| ~ young(X9)
| ~ in(X8,X0)
| ~ in(X9,X7)
| ~ seat(X10)
| ~ furniture(X10)
| ~ front(X10)
| ~ hollywood(X11)
| ~ city(X11)
| ~ event(X12)
| ~ street(X13)
| ~ way(X13)
| ~ lonely(X13)
| ~ chevy(X14)
| ~ car(X14)
| ~ white(X14)
| ~ dirty(X14)
| ~ old(X14)
| ~ barrel(X12,X14)
| ~ down(X12,X13)
| ~ in(X12,X11)
| ~ seat(X17)
| ~ furniture(X17)
| ~ front(X17)
| X15 = X16
| ~ fellow(X15)
| ~ man(X15)
| ~ young(X15)
| ~ fellow(X16)
| ~ man(X16)
| ~ young(X16)
| X15 != X18
| ~ in(X18,X17)
| X16 != X19
| ~ in(X19,X10) ),
inference(equality_resolution,[],[f79]) ).
fof(f81,plain,
! [X2,X3,X10,X0,X11,X1,X8,X18,X9,X7,X14,X4,X16,X19,X17,X12,X13] :
( ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ hollywood(X1)
| ~ city(X1)
| ~ event(X2)
| ~ street(X3)
| ~ way(X3)
| ~ lonely(X3)
| ~ chevy(X4)
| ~ car(X4)
| ~ white(X4)
| ~ dirty(X4)
| ~ old(X4)
| ~ barrel(X2,X4)
| ~ down(X2,X3)
| ~ in(X2,X1)
| ~ seat(X7)
| ~ furniture(X7)
| ~ front(X7)
| X8 = X9
| ~ fellow(X8)
| ~ man(X8)
| ~ young(X8)
| ~ fellow(X9)
| ~ man(X9)
| ~ young(X9)
| ~ in(X8,X0)
| ~ in(X9,X7)
| ~ seat(X10)
| ~ furniture(X10)
| ~ front(X10)
| ~ hollywood(X11)
| ~ city(X11)
| ~ event(X12)
| ~ street(X13)
| ~ way(X13)
| ~ lonely(X13)
| ~ chevy(X14)
| ~ car(X14)
| ~ white(X14)
| ~ dirty(X14)
| ~ old(X14)
| ~ barrel(X12,X14)
| ~ down(X12,X13)
| ~ in(X12,X11)
| ~ seat(X17)
| ~ furniture(X17)
| ~ front(X17)
| X16 = X18
| ~ fellow(X18)
| ~ man(X18)
| ~ young(X18)
| ~ fellow(X16)
| ~ man(X16)
| ~ young(X16)
| ~ in(X18,X17)
| X16 != X19
| ~ in(X19,X10) ),
inference(equality_resolution,[],[f80]) ).
fof(f82,plain,
! [X2,X3,X10,X0,X11,X1,X8,X18,X9,X7,X14,X4,X19,X17,X12,X13] :
( ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ hollywood(X1)
| ~ city(X1)
| ~ event(X2)
| ~ street(X3)
| ~ way(X3)
| ~ lonely(X3)
| ~ chevy(X4)
| ~ car(X4)
| ~ white(X4)
| ~ dirty(X4)
| ~ old(X4)
| ~ barrel(X2,X4)
| ~ down(X2,X3)
| ~ in(X2,X1)
| ~ seat(X7)
| ~ furniture(X7)
| ~ front(X7)
| X8 = X9
| ~ fellow(X8)
| ~ man(X8)
| ~ young(X8)
| ~ fellow(X9)
| ~ man(X9)
| ~ young(X9)
| ~ in(X8,X0)
| ~ in(X9,X7)
| ~ seat(X10)
| ~ furniture(X10)
| ~ front(X10)
| ~ hollywood(X11)
| ~ city(X11)
| ~ event(X12)
| ~ street(X13)
| ~ way(X13)
| ~ lonely(X13)
| ~ chevy(X14)
| ~ car(X14)
| ~ white(X14)
| ~ dirty(X14)
| ~ old(X14)
| ~ barrel(X12,X14)
| ~ down(X12,X13)
| ~ in(X12,X11)
| ~ seat(X17)
| ~ furniture(X17)
| ~ front(X17)
| X18 = X19
| ~ fellow(X18)
| ~ man(X18)
| ~ young(X18)
| ~ fellow(X19)
| ~ man(X19)
| ~ young(X19)
| ~ in(X18,X17)
| ~ in(X19,X10) ),
inference(equality_resolution,[],[f81]) ).
fof(f87,plain,
( seat(sK2)
| sP1 ),
inference(consistent_polarity_flipping,[],[f43]) ).
fof(f88,plain,
( furniture(sK2)
| sP1 ),
inference(consistent_polarity_flipping,[],[f42]) ).
fof(f89,plain,
( ~ front(sK2)
| sP1 ),
inference(consistent_polarity_flipping,[],[f41]) ).
fof(f90,plain,
( ~ hollywood(sK3)
| sP1 ),
inference(consistent_polarity_flipping,[],[f40]) ).
fof(f91,plain,
( city(sK3)
| sP1 ),
inference(consistent_polarity_flipping,[],[f39]) ).
fof(f92,plain,
( event(sK4)
| sP1 ),
inference(consistent_polarity_flipping,[],[f38]) ).
fof(f93,plain,
( ~ street(sK5)
| sP1 ),
inference(consistent_polarity_flipping,[],[f37]) ).
fof(f94,plain,
( ~ way(sK5)
| sP1 ),
inference(consistent_polarity_flipping,[],[f36]) ).
fof(f95,plain,
( ~ lonely(sK5)
| sP1 ),
inference(consistent_polarity_flipping,[],[f35]) ).
fof(f96,plain,
( chevy(sK6)
| sP1 ),
inference(consistent_polarity_flipping,[],[f34]) ).
fof(f97,plain,
( ~ car(sK6)
| sP1 ),
inference(consistent_polarity_flipping,[],[f33]) ).
fof(f98,plain,
( white(sK6)
| sP1 ),
inference(consistent_polarity_flipping,[],[f32]) ).
fof(f99,plain,
( ~ dirty(sK6)
| sP1 ),
inference(consistent_polarity_flipping,[],[f31]) ).
fof(f100,plain,
( old(sK6)
| sP1 ),
inference(consistent_polarity_flipping,[],[f30]) ).
fof(f101,plain,
( ~ barrel(sK4,sK6)
| sP1 ),
inference(consistent_polarity_flipping,[],[f29]) ).
fof(f102,plain,
( ~ down(sK4,sK5)
| sP1 ),
inference(consistent_polarity_flipping,[],[f28]) ).
fof(f103,plain,
( ~ in(sK4,sK3)
| sP1 ),
inference(consistent_polarity_flipping,[],[f27]) ).
fof(f104,plain,
( seat(sK9)
| sP1 ),
inference(consistent_polarity_flipping,[],[f26]) ).
fof(f105,plain,
( furniture(sK9)
| sP1 ),
inference(consistent_polarity_flipping,[],[f25]) ).
fof(f106,plain,
( ~ front(sK9)
| sP1 ),
inference(consistent_polarity_flipping,[],[f24]) ).
fof(f107,plain,
( sK7 != sK8
| sP1 ),
inference(consistent_polarity_flipping,[],[f23]) ).
fof(f108,plain,
( ~ fellow(sK7)
| sP1 ),
inference(consistent_polarity_flipping,[],[f22]) ).
fof(f109,plain,
( ~ man(sK7)
| sP1 ),
inference(consistent_polarity_flipping,[],[f21]) ).
fof(f110,plain,
( young(sK7)
| sP1 ),
inference(consistent_polarity_flipping,[],[f20]) ).
fof(f111,plain,
( ~ fellow(sK8)
| sP1 ),
inference(consistent_polarity_flipping,[],[f19]) ).
fof(f112,plain,
( ~ man(sK8)
| sP1 ),
inference(consistent_polarity_flipping,[],[f18]) ).
fof(f113,plain,
( young(sK8)
| sP1 ),
inference(consistent_polarity_flipping,[],[f17]) ).
fof(f114,plain,
( sK7 = sK10
| sP1 ),
inference(consistent_polarity_flipping,[],[f16]) ).
fof(f115,plain,
( ~ in(sK10,sK9)
| sP1 ),
inference(consistent_polarity_flipping,[],[f15]) ).
fof(f116,plain,
( sK8 = sK11
| sP1 ),
inference(consistent_polarity_flipping,[],[f14]) ).
fof(f117,plain,
( ~ in(sK11,sK2)
| sP1 ),
inference(consistent_polarity_flipping,[],[f13]) ).
fof(f118,plain,
( ~ front(sK12)
| ~ sP0 ),
inference(consistent_polarity_flipping,[],[f72]) ).
fof(f119,plain,
( ~ hollywood(sK13)
| ~ sP0 ),
inference(consistent_polarity_flipping,[],[f71]) ).
fof(f120,plain,
( ~ street(sK15)
| ~ sP0 ),
inference(consistent_polarity_flipping,[],[f68]) ).
fof(f121,plain,
( ~ way(sK15)
| ~ sP0 ),
inference(consistent_polarity_flipping,[],[f67]) ).
fof(f122,plain,
( ~ lonely(sK15)
| ~ sP0 ),
inference(consistent_polarity_flipping,[],[f66]) ).
fof(f123,plain,
( ~ car(sK16)
| ~ sP0 ),
inference(consistent_polarity_flipping,[],[f64]) ).
fof(f124,plain,
( ~ dirty(sK16)
| ~ sP0 ),
inference(consistent_polarity_flipping,[],[f62]) ).
fof(f125,plain,
( ~ barrel(sK14,sK16)
| ~ sP0 ),
inference(consistent_polarity_flipping,[],[f60]) ).
fof(f126,plain,
( ~ down(sK14,sK15)
| ~ sP0 ),
inference(consistent_polarity_flipping,[],[f59]) ).
fof(f127,plain,
( ~ in(sK14,sK13)
| ~ sP0 ),
inference(consistent_polarity_flipping,[],[f58]) ).
fof(f128,plain,
( ~ front(sK19)
| ~ sP0 ),
inference(consistent_polarity_flipping,[],[f55]) ).
fof(f129,plain,
( ~ fellow(sK17)
| ~ sP0 ),
inference(consistent_polarity_flipping,[],[f53]) ).
fof(f130,plain,
( ~ man(sK17)
| ~ sP0 ),
inference(consistent_polarity_flipping,[],[f52]) ).
fof(f131,plain,
( ~ fellow(sK18)
| ~ sP0 ),
inference(consistent_polarity_flipping,[],[f50]) ).
fof(f132,plain,
( ~ man(sK18)
| ~ sP0 ),
inference(consistent_polarity_flipping,[],[f49]) ).
fof(f133,plain,
( ~ in(sK20,sK12)
| ~ sP0 ),
inference(consistent_polarity_flipping,[],[f46]) ).
fof(f134,plain,
( ~ in(sK21,sK19)
| ~ sP0 ),
inference(consistent_polarity_flipping,[],[f44]) ).
fof(f135,plain,
! [X2,X3,X10,X0,X11,X1,X8,X18,X9,X7,X14,X4,X19,X17,X12,X13] :
( ~ seat(X0)
| ~ furniture(X0)
| front(X0)
| hollywood(X1)
| ~ city(X1)
| ~ event(X2)
| street(X3)
| way(X3)
| lonely(X3)
| ~ chevy(X4)
| car(X4)
| ~ white(X4)
| dirty(X4)
| ~ old(X4)
| barrel(X2,X4)
| down(X2,X3)
| in(X2,X1)
| ~ seat(X7)
| ~ furniture(X7)
| front(X7)
| X8 = X9
| fellow(X8)
| man(X8)
| ~ young(X8)
| fellow(X9)
| man(X9)
| ~ young(X9)
| in(X8,X0)
| in(X9,X7)
| ~ seat(X10)
| ~ furniture(X10)
| front(X10)
| hollywood(X11)
| ~ city(X11)
| ~ event(X12)
| street(X13)
| way(X13)
| lonely(X13)
| ~ chevy(X14)
| car(X14)
| ~ white(X14)
| dirty(X14)
| ~ old(X14)
| barrel(X12,X14)
| down(X12,X13)
| in(X12,X11)
| ~ seat(X17)
| ~ furniture(X17)
| front(X17)
| X18 = X19
| fellow(X18)
| man(X18)
| ~ young(X18)
| fellow(X19)
| man(X19)
| ~ young(X19)
| in(X18,X17)
| in(X19,X10) ),
inference(consistent_polarity_flipping,[],[f82]) ).
fof(f138,plain,
( ~ sP1
| sP0 ),
inference(consistent_polarity_flipping,[],[f75]) ).
fof(f140,definition,
( spl22_1
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl22_1])],[avatar_definition]) ).
fof(f144,definition,
( spl22_2
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl22_2])],[avatar_definition]) ).
fof(f147,plain,
( spl22_1
| ~ spl22_2 ),
inference(avatar_split_clause,[],[f138,f144,f140]) ).
fof(f149,definition,
( spl22_3
<=> ! [X11,X13,X14,X12] :
( hollywood(X11)
| ~ event(X12)
| in(X12,X11)
| down(X12,X13)
| barrel(X12,X14)
| ~ chevy(X14)
| ~ old(X14)
| dirty(X14)
| ~ white(X14)
| car(X14)
| street(X13)
| lonely(X13)
| way(X13)
| ~ city(X11) ) ),
introduced(definition,[new_symbols(definition,[spl22_3])],[avatar_definition]) ).
fof(f150,plain,
( ! [X11,X14,X12,X13] :
( dirty(X14)
| ~ event(X12)
| in(X12,X11)
| down(X12,X13)
| barrel(X12,X14)
| ~ chevy(X14)
| ~ old(X14)
| hollywood(X11)
| ~ white(X14)
| car(X14)
| street(X13)
| lonely(X13)
| way(X13)
| ~ city(X11) )
| ~ spl22_3 ),
inference(avatar_component_clause,[],[f149]) ).
fof(f152,definition,
( spl22_4
<=> ! [X18,X17,X10,X19] :
( ~ seat(X10)
| ~ seat(X17)
| in(X19,X10)
| X18 = X19
| in(X18,X17)
| ~ young(X19)
| man(X19)
| fellow(X19)
| ~ young(X18)
| man(X18)
| fellow(X18)
| front(X17)
| ~ furniture(X17)
| front(X10)
| ~ furniture(X10) ) ),
introduced(definition,[new_symbols(definition,[spl22_4])],[avatar_definition]) ).
fof(f153,plain,
( ! [X10,X18,X19,X17] :
( man(X19)
| ~ seat(X17)
| in(X19,X10)
| X18 = X19
| in(X18,X17)
| ~ young(X19)
| ~ seat(X10)
| fellow(X19)
| ~ young(X18)
| man(X18)
| fellow(X18)
| front(X17)
| ~ furniture(X17)
| front(X10)
| ~ furniture(X10) )
| ~ spl22_4 ),
inference(avatar_component_clause,[],[f152]) ).
fof(f156,plain,
( spl22_3
| spl22_4
| spl22_3
| spl22_4 ),
inference(avatar_split_clause,[],[f135,f152,f149,f152,f149]) ).
fof(f158,definition,
( spl22_5
<=> in(sK21,sK19) ),
introduced(definition,[new_symbols(definition,[spl22_5])],[avatar_definition]) ).
fof(f160,plain,
( ~ in(sK21,sK19)
| spl22_5 ),
inference(avatar_component_clause,[],[f158]) ).
fof(f161,plain,
( ~ spl22_1
| ~ spl22_5 ),
inference(avatar_split_clause,[],[f134,f158,f140]) ).
fof(f163,definition,
( spl22_6
<=> sK18 = sK21 ),
introduced(definition,[new_symbols(definition,[spl22_6])],[avatar_definition]) ).
fof(f165,plain,
( sK18 = sK21
| ~ spl22_6 ),
inference(avatar_component_clause,[],[f163]) ).
fof(f166,plain,
( ~ spl22_1
| spl22_6 ),
inference(avatar_split_clause,[],[f45,f163,f140]) ).
fof(f168,definition,
( spl22_7
<=> in(sK20,sK12) ),
introduced(definition,[new_symbols(definition,[spl22_7])],[avatar_definition]) ).
fof(f170,plain,
( ~ in(sK20,sK12)
| spl22_7 ),
inference(avatar_component_clause,[],[f168]) ).
fof(f171,plain,
( ~ spl22_1
| ~ spl22_7 ),
inference(avatar_split_clause,[],[f133,f168,f140]) ).
fof(f173,definition,
( spl22_8
<=> sK17 = sK20 ),
introduced(definition,[new_symbols(definition,[spl22_8])],[avatar_definition]) ).
fof(f175,plain,
( sK17 = sK20
| ~ spl22_8 ),
inference(avatar_component_clause,[],[f173]) ).
fof(f176,plain,
( ~ spl22_1
| spl22_8 ),
inference(avatar_split_clause,[],[f47,f173,f140]) ).
fof(f178,definition,
( spl22_9
<=> young(sK18) ),
introduced(definition,[new_symbols(definition,[spl22_9])],[avatar_definition]) ).
fof(f181,plain,
( ~ spl22_1
| spl22_9 ),
inference(avatar_split_clause,[],[f48,f178,f140]) ).
fof(f183,definition,
( spl22_10
<=> man(sK18) ),
introduced(definition,[new_symbols(definition,[spl22_10])],[avatar_definition]) ).
fof(f185,plain,
( ~ man(sK18)
| spl22_10 ),
inference(avatar_component_clause,[],[f183]) ).
fof(f186,plain,
( ~ spl22_1
| ~ spl22_10 ),
inference(avatar_split_clause,[],[f132,f183,f140]) ).
fof(f188,definition,
( spl22_11
<=> fellow(sK18) ),
introduced(definition,[new_symbols(definition,[spl22_11])],[avatar_definition]) ).
fof(f191,plain,
( ~ spl22_1
| ~ spl22_11 ),
inference(avatar_split_clause,[],[f131,f188,f140]) ).
fof(f193,definition,
( spl22_12
<=> young(sK17) ),
introduced(definition,[new_symbols(definition,[spl22_12])],[avatar_definition]) ).
fof(f196,plain,
( ~ spl22_1
| spl22_12 ),
inference(avatar_split_clause,[],[f51,f193,f140]) ).
fof(f198,definition,
( spl22_13
<=> man(sK17) ),
introduced(definition,[new_symbols(definition,[spl22_13])],[avatar_definition]) ).
fof(f200,plain,
( ~ man(sK17)
| spl22_13 ),
inference(avatar_component_clause,[],[f198]) ).
fof(f201,plain,
( ~ spl22_1
| ~ spl22_13 ),
inference(avatar_split_clause,[],[f130,f198,f140]) ).
fof(f203,definition,
( spl22_14
<=> fellow(sK17) ),
introduced(definition,[new_symbols(definition,[spl22_14])],[avatar_definition]) ).
fof(f206,plain,
( ~ spl22_1
| ~ spl22_14 ),
inference(avatar_split_clause,[],[f129,f203,f140]) ).
fof(f208,definition,
( spl22_15
<=> sK17 = sK18 ),
introduced(definition,[new_symbols(definition,[spl22_15])],[avatar_definition]) ).
fof(f211,plain,
( ~ spl22_1
| ~ spl22_15 ),
inference(avatar_split_clause,[],[f54,f208,f140]) ).
fof(f213,definition,
( spl22_16
<=> front(sK19) ),
introduced(definition,[new_symbols(definition,[spl22_16])],[avatar_definition]) ).
fof(f216,plain,
( ~ spl22_1
| ~ spl22_16 ),
inference(avatar_split_clause,[],[f128,f213,f140]) ).
fof(f218,definition,
( spl22_17
<=> furniture(sK19) ),
introduced(definition,[new_symbols(definition,[spl22_17])],[avatar_definition]) ).
fof(f221,plain,
( ~ spl22_1
| spl22_17 ),
inference(avatar_split_clause,[],[f56,f218,f140]) ).
fof(f223,definition,
( spl22_18
<=> seat(sK19) ),
introduced(definition,[new_symbols(definition,[spl22_18])],[avatar_definition]) ).
fof(f226,plain,
( ~ spl22_1
| spl22_18 ),
inference(avatar_split_clause,[],[f57,f223,f140]) ).
fof(f228,definition,
( spl22_19
<=> in(sK14,sK13) ),
introduced(definition,[new_symbols(definition,[spl22_19])],[avatar_definition]) ).
fof(f230,plain,
( ~ in(sK14,sK13)
| spl22_19 ),
inference(avatar_component_clause,[],[f228]) ).
fof(f231,plain,
( ~ spl22_1
| ~ spl22_19 ),
inference(avatar_split_clause,[],[f127,f228,f140]) ).
fof(f233,definition,
( spl22_20
<=> down(sK14,sK15) ),
introduced(definition,[new_symbols(definition,[spl22_20])],[avatar_definition]) ).
fof(f235,plain,
( ~ down(sK14,sK15)
| spl22_20 ),
inference(avatar_component_clause,[],[f233]) ).
fof(f236,plain,
( ~ spl22_1
| ~ spl22_20 ),
inference(avatar_split_clause,[],[f126,f233,f140]) ).
fof(f238,definition,
( spl22_21
<=> barrel(sK14,sK16) ),
introduced(definition,[new_symbols(definition,[spl22_21])],[avatar_definition]) ).
fof(f240,plain,
( ~ barrel(sK14,sK16)
| spl22_21 ),
inference(avatar_component_clause,[],[f238]) ).
fof(f241,plain,
( ~ spl22_1
| ~ spl22_21 ),
inference(avatar_split_clause,[],[f125,f238,f140]) ).
fof(f243,definition,
( spl22_22
<=> old(sK16) ),
introduced(definition,[new_symbols(definition,[spl22_22])],[avatar_definition]) ).
fof(f246,plain,
( ~ spl22_1
| spl22_22 ),
inference(avatar_split_clause,[],[f61,f243,f140]) ).
fof(f248,definition,
( spl22_23
<=> dirty(sK16) ),
introduced(definition,[new_symbols(definition,[spl22_23])],[avatar_definition]) ).
fof(f250,plain,
( ~ dirty(sK16)
| spl22_23 ),
inference(avatar_component_clause,[],[f248]) ).
fof(f251,plain,
( ~ spl22_1
| ~ spl22_23 ),
inference(avatar_split_clause,[],[f124,f248,f140]) ).
fof(f253,definition,
( spl22_24
<=> white(sK16) ),
introduced(definition,[new_symbols(definition,[spl22_24])],[avatar_definition]) ).
fof(f256,plain,
( ~ spl22_1
| spl22_24 ),
inference(avatar_split_clause,[],[f63,f253,f140]) ).
fof(f258,definition,
( spl22_25
<=> car(sK16) ),
introduced(definition,[new_symbols(definition,[spl22_25])],[avatar_definition]) ).
fof(f261,plain,
( ~ spl22_1
| ~ spl22_25 ),
inference(avatar_split_clause,[],[f123,f258,f140]) ).
fof(f263,definition,
( spl22_26
<=> chevy(sK16) ),
introduced(definition,[new_symbols(definition,[spl22_26])],[avatar_definition]) ).
fof(f266,plain,
( ~ spl22_1
| spl22_26 ),
inference(avatar_split_clause,[],[f65,f263,f140]) ).
fof(f268,definition,
( spl22_27
<=> lonely(sK15) ),
introduced(definition,[new_symbols(definition,[spl22_27])],[avatar_definition]) ).
fof(f271,plain,
( ~ spl22_1
| ~ spl22_27 ),
inference(avatar_split_clause,[],[f122,f268,f140]) ).
fof(f273,definition,
( spl22_28
<=> way(sK15) ),
introduced(definition,[new_symbols(definition,[spl22_28])],[avatar_definition]) ).
fof(f276,plain,
( ~ spl22_1
| ~ spl22_28 ),
inference(avatar_split_clause,[],[f121,f273,f140]) ).
fof(f278,definition,
( spl22_29
<=> street(sK15) ),
introduced(definition,[new_symbols(definition,[spl22_29])],[avatar_definition]) ).
fof(f281,plain,
( ~ spl22_1
| ~ spl22_29 ),
inference(avatar_split_clause,[],[f120,f278,f140]) ).
fof(f283,definition,
( spl22_30
<=> event(sK14) ),
introduced(definition,[new_symbols(definition,[spl22_30])],[avatar_definition]) ).
fof(f286,plain,
( ~ spl22_1
| spl22_30 ),
inference(avatar_split_clause,[],[f69,f283,f140]) ).
fof(f288,definition,
( spl22_31
<=> city(sK13) ),
introduced(definition,[new_symbols(definition,[spl22_31])],[avatar_definition]) ).
fof(f291,plain,
( ~ spl22_1
| spl22_31 ),
inference(avatar_split_clause,[],[f70,f288,f140]) ).
fof(f293,definition,
( spl22_32
<=> hollywood(sK13) ),
introduced(definition,[new_symbols(definition,[spl22_32])],[avatar_definition]) ).
fof(f296,plain,
( ~ spl22_1
| ~ spl22_32 ),
inference(avatar_split_clause,[],[f119,f293,f140]) ).
fof(f298,definition,
( spl22_33
<=> front(sK12) ),
introduced(definition,[new_symbols(definition,[spl22_33])],[avatar_definition]) ).
fof(f301,plain,
( ~ spl22_1
| ~ spl22_33 ),
inference(avatar_split_clause,[],[f118,f298,f140]) ).
fof(f303,definition,
( spl22_34
<=> furniture(sK12) ),
introduced(definition,[new_symbols(definition,[spl22_34])],[avatar_definition]) ).
fof(f306,plain,
( ~ spl22_1
| spl22_34 ),
inference(avatar_split_clause,[],[f73,f303,f140]) ).
fof(f308,definition,
( spl22_35
<=> seat(sK12) ),
introduced(definition,[new_symbols(definition,[spl22_35])],[avatar_definition]) ).
fof(f311,plain,
( ~ spl22_1
| spl22_35 ),
inference(avatar_split_clause,[],[f74,f308,f140]) ).
fof(f313,definition,
( spl22_36
<=> in(sK11,sK2) ),
introduced(definition,[new_symbols(definition,[spl22_36])],[avatar_definition]) ).
fof(f315,plain,
( ~ in(sK11,sK2)
| spl22_36 ),
inference(avatar_component_clause,[],[f313]) ).
fof(f316,plain,
( spl22_2
| ~ spl22_36 ),
inference(avatar_split_clause,[],[f117,f313,f144]) ).
fof(f318,definition,
( spl22_37
<=> sK8 = sK11 ),
introduced(definition,[new_symbols(definition,[spl22_37])],[avatar_definition]) ).
fof(f320,plain,
( sK8 = sK11
| ~ spl22_37 ),
inference(avatar_component_clause,[],[f318]) ).
fof(f321,plain,
( spl22_2
| spl22_37 ),
inference(avatar_split_clause,[],[f116,f318,f144]) ).
fof(f323,definition,
( spl22_38
<=> in(sK10,sK9) ),
introduced(definition,[new_symbols(definition,[spl22_38])],[avatar_definition]) ).
fof(f325,plain,
( ~ in(sK10,sK9)
| spl22_38 ),
inference(avatar_component_clause,[],[f323]) ).
fof(f326,plain,
( spl22_2
| ~ spl22_38 ),
inference(avatar_split_clause,[],[f115,f323,f144]) ).
fof(f328,definition,
( spl22_39
<=> sK7 = sK10 ),
introduced(definition,[new_symbols(definition,[spl22_39])],[avatar_definition]) ).
fof(f330,plain,
( sK7 = sK10
| ~ spl22_39 ),
inference(avatar_component_clause,[],[f328]) ).
fof(f331,plain,
( spl22_2
| spl22_39 ),
inference(avatar_split_clause,[],[f114,f328,f144]) ).
fof(f333,definition,
( spl22_40
<=> young(sK8) ),
introduced(definition,[new_symbols(definition,[spl22_40])],[avatar_definition]) ).
fof(f336,plain,
( spl22_2
| spl22_40 ),
inference(avatar_split_clause,[],[f113,f333,f144]) ).
fof(f338,definition,
( spl22_41
<=> man(sK8) ),
introduced(definition,[new_symbols(definition,[spl22_41])],[avatar_definition]) ).
fof(f340,plain,
( ~ man(sK8)
| spl22_41 ),
inference(avatar_component_clause,[],[f338]) ).
fof(f341,plain,
( spl22_2
| ~ spl22_41 ),
inference(avatar_split_clause,[],[f112,f338,f144]) ).
fof(f343,definition,
( spl22_42
<=> fellow(sK8) ),
introduced(definition,[new_symbols(definition,[spl22_42])],[avatar_definition]) ).
fof(f346,plain,
( spl22_2
| ~ spl22_42 ),
inference(avatar_split_clause,[],[f111,f343,f144]) ).
fof(f348,definition,
( spl22_43
<=> young(sK7) ),
introduced(definition,[new_symbols(definition,[spl22_43])],[avatar_definition]) ).
fof(f351,plain,
( spl22_2
| spl22_43 ),
inference(avatar_split_clause,[],[f110,f348,f144]) ).
fof(f353,definition,
( spl22_44
<=> man(sK7) ),
introduced(definition,[new_symbols(definition,[spl22_44])],[avatar_definition]) ).
fof(f355,plain,
( ~ man(sK7)
| spl22_44 ),
inference(avatar_component_clause,[],[f353]) ).
fof(f356,plain,
( spl22_2
| ~ spl22_44 ),
inference(avatar_split_clause,[],[f109,f353,f144]) ).
fof(f358,definition,
( spl22_45
<=> fellow(sK7) ),
introduced(definition,[new_symbols(definition,[spl22_45])],[avatar_definition]) ).
fof(f361,plain,
( spl22_2
| ~ spl22_45 ),
inference(avatar_split_clause,[],[f108,f358,f144]) ).
fof(f363,definition,
( spl22_46
<=> sK7 = sK8 ),
introduced(definition,[new_symbols(definition,[spl22_46])],[avatar_definition]) ).
fof(f366,plain,
( spl22_2
| ~ spl22_46 ),
inference(avatar_split_clause,[],[f107,f363,f144]) ).
fof(f368,definition,
( spl22_47
<=> front(sK9) ),
introduced(definition,[new_symbols(definition,[spl22_47])],[avatar_definition]) ).
fof(f371,plain,
( spl22_2
| ~ spl22_47 ),
inference(avatar_split_clause,[],[f106,f368,f144]) ).
fof(f373,definition,
( spl22_48
<=> furniture(sK9) ),
introduced(definition,[new_symbols(definition,[spl22_48])],[avatar_definition]) ).
fof(f376,plain,
( spl22_2
| spl22_48 ),
inference(avatar_split_clause,[],[f105,f373,f144]) ).
fof(f378,definition,
( spl22_49
<=> seat(sK9) ),
introduced(definition,[new_symbols(definition,[spl22_49])],[avatar_definition]) ).
fof(f381,plain,
( spl22_2
| spl22_49 ),
inference(avatar_split_clause,[],[f104,f378,f144]) ).
fof(f383,definition,
( spl22_50
<=> in(sK4,sK3) ),
introduced(definition,[new_symbols(definition,[spl22_50])],[avatar_definition]) ).
fof(f385,plain,
( ~ in(sK4,sK3)
| spl22_50 ),
inference(avatar_component_clause,[],[f383]) ).
fof(f386,plain,
( spl22_2
| ~ spl22_50 ),
inference(avatar_split_clause,[],[f103,f383,f144]) ).
fof(f388,definition,
( spl22_51
<=> down(sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl22_51])],[avatar_definition]) ).
fof(f390,plain,
( ~ down(sK4,sK5)
| spl22_51 ),
inference(avatar_component_clause,[],[f388]) ).
fof(f391,plain,
( spl22_2
| ~ spl22_51 ),
inference(avatar_split_clause,[],[f102,f388,f144]) ).
fof(f393,definition,
( spl22_52
<=> barrel(sK4,sK6) ),
introduced(definition,[new_symbols(definition,[spl22_52])],[avatar_definition]) ).
fof(f395,plain,
( ~ barrel(sK4,sK6)
| spl22_52 ),
inference(avatar_component_clause,[],[f393]) ).
fof(f396,plain,
( spl22_2
| ~ spl22_52 ),
inference(avatar_split_clause,[],[f101,f393,f144]) ).
fof(f398,definition,
( spl22_53
<=> old(sK6) ),
introduced(definition,[new_symbols(definition,[spl22_53])],[avatar_definition]) ).
fof(f401,plain,
( spl22_2
| spl22_53 ),
inference(avatar_split_clause,[],[f100,f398,f144]) ).
fof(f403,definition,
( spl22_54
<=> dirty(sK6) ),
introduced(definition,[new_symbols(definition,[spl22_54])],[avatar_definition]) ).
fof(f405,plain,
( ~ dirty(sK6)
| spl22_54 ),
inference(avatar_component_clause,[],[f403]) ).
fof(f406,plain,
( spl22_2
| ~ spl22_54 ),
inference(avatar_split_clause,[],[f99,f403,f144]) ).
fof(f408,definition,
( spl22_55
<=> white(sK6) ),
introduced(definition,[new_symbols(definition,[spl22_55])],[avatar_definition]) ).
fof(f411,plain,
( spl22_2
| spl22_55 ),
inference(avatar_split_clause,[],[f98,f408,f144]) ).
fof(f413,definition,
( spl22_56
<=> car(sK6) ),
introduced(definition,[new_symbols(definition,[spl22_56])],[avatar_definition]) ).
fof(f416,plain,
( spl22_2
| ~ spl22_56 ),
inference(avatar_split_clause,[],[f97,f413,f144]) ).
fof(f418,definition,
( spl22_57
<=> chevy(sK6) ),
introduced(definition,[new_symbols(definition,[spl22_57])],[avatar_definition]) ).
fof(f421,plain,
( spl22_2
| spl22_57 ),
inference(avatar_split_clause,[],[f96,f418,f144]) ).
fof(f423,definition,
( spl22_58
<=> lonely(sK5) ),
introduced(definition,[new_symbols(definition,[spl22_58])],[avatar_definition]) ).
fof(f426,plain,
( spl22_2
| ~ spl22_58 ),
inference(avatar_split_clause,[],[f95,f423,f144]) ).
fof(f428,definition,
( spl22_59
<=> way(sK5) ),
introduced(definition,[new_symbols(definition,[spl22_59])],[avatar_definition]) ).
fof(f431,plain,
( spl22_2
| ~ spl22_59 ),
inference(avatar_split_clause,[],[f94,f428,f144]) ).
fof(f433,definition,
( spl22_60
<=> street(sK5) ),
introduced(definition,[new_symbols(definition,[spl22_60])],[avatar_definition]) ).
fof(f436,plain,
( spl22_2
| ~ spl22_60 ),
inference(avatar_split_clause,[],[f93,f433,f144]) ).
fof(f438,definition,
( spl22_61
<=> event(sK4) ),
introduced(definition,[new_symbols(definition,[spl22_61])],[avatar_definition]) ).
fof(f441,plain,
( spl22_2
| spl22_61 ),
inference(avatar_split_clause,[],[f92,f438,f144]) ).
fof(f443,definition,
( spl22_62
<=> city(sK3) ),
introduced(definition,[new_symbols(definition,[spl22_62])],[avatar_definition]) ).
fof(f446,plain,
( spl22_2
| spl22_62 ),
inference(avatar_split_clause,[],[f91,f443,f144]) ).
fof(f448,definition,
( spl22_63
<=> hollywood(sK3) ),
introduced(definition,[new_symbols(definition,[spl22_63])],[avatar_definition]) ).
fof(f451,plain,
( spl22_2
| ~ spl22_63 ),
inference(avatar_split_clause,[],[f90,f448,f144]) ).
fof(f453,definition,
( spl22_64
<=> front(sK2) ),
introduced(definition,[new_symbols(definition,[spl22_64])],[avatar_definition]) ).
fof(f456,plain,
( spl22_2
| ~ spl22_64 ),
inference(avatar_split_clause,[],[f89,f453,f144]) ).
fof(f458,definition,
( spl22_65
<=> furniture(sK2) ),
introduced(definition,[new_symbols(definition,[spl22_65])],[avatar_definition]) ).
fof(f461,plain,
( spl22_2
| spl22_65 ),
inference(avatar_split_clause,[],[f88,f458,f144]) ).
fof(f463,definition,
( spl22_66
<=> seat(sK2) ),
introduced(definition,[new_symbols(definition,[spl22_66])],[avatar_definition]) ).
fof(f466,plain,
( spl22_2
| spl22_66 ),
inference(avatar_split_clause,[],[f87,f463,f144]) ).
fof(f467,plain,
( ! [X2,X0,X1] :
( ~ event(X0)
| in(X0,X1)
| down(X0,X2)
| barrel(X0,sK16)
| ~ chevy(sK16)
| ~ old(sK16)
| hollywood(X1)
| ~ white(sK16)
| car(sK16)
| street(X2)
| lonely(X2)
| way(X2)
| ~ city(X1) )
| ~ spl22_3
| spl22_23 ),
inference(resolution,[],[f150,f250]) ).
fof(f468,plain,
( ! [X2,X0,X1] :
( ~ event(X0)
| in(X0,X1)
| down(X0,X2)
| barrel(X0,sK6)
| ~ chevy(sK6)
| ~ old(sK6)
| hollywood(X1)
| ~ white(sK6)
| car(sK6)
| street(X2)
| lonely(X2)
| way(X2)
| ~ city(X1) )
| ~ spl22_3
| spl22_54 ),
inference(resolution,[],[f150,f405]) ).
fof(f470,definition,
( spl22_67
<=> ! [X2,X0,X1] :
( ~ event(X0)
| ~ city(X1)
| way(X2)
| lonely(X2)
| street(X2)
| hollywood(X1)
| barrel(X0,sK6)
| down(X0,X2)
| in(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl22_67])],[avatar_definition]) ).
fof(f471,plain,
( ! [X2,X0,X1] :
( barrel(X0,sK6)
| ~ city(X1)
| way(X2)
| lonely(X2)
| street(X2)
| hollywood(X1)
| ~ event(X0)
| down(X0,X2)
| in(X0,X1) )
| ~ spl22_67 ),
inference(avatar_component_clause,[],[f470]) ).
fof(f472,plain,
( spl22_56
| ~ spl22_55
| ~ spl22_53
| ~ spl22_57
| spl22_67
| ~ spl22_3
| spl22_54 ),
inference(avatar_split_clause,[],[f468,f403,f149,f470,f418,f398,f408,f413]) ).
fof(f474,definition,
( spl22_68
<=> ! [X2,X0,X1] :
( ~ event(X0)
| ~ city(X1)
| way(X2)
| lonely(X2)
| street(X2)
| hollywood(X1)
| barrel(X0,sK16)
| down(X0,X2)
| in(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl22_68])],[avatar_definition]) ).
fof(f475,plain,
( ! [X2,X0,X1] :
( barrel(X0,sK16)
| ~ city(X1)
| way(X2)
| lonely(X2)
| street(X2)
| hollywood(X1)
| ~ event(X0)
| down(X0,X2)
| in(X0,X1) )
| ~ spl22_68 ),
inference(avatar_component_clause,[],[f474]) ).
fof(f476,plain,
( spl22_25
| ~ spl22_24
| ~ spl22_22
| ~ spl22_26
| spl22_68
| ~ spl22_3
| spl22_23 ),
inference(avatar_split_clause,[],[f467,f248,f149,f474,f263,f243,f253,f258]) ).
fof(f477,plain,
( ~ in(sK18,sK19)
| spl22_5
| ~ spl22_6 ),
inference(superposition,[],[f160,f165]) ).
fof(f478,plain,
( ~ in(sK17,sK12)
| spl22_7
| ~ spl22_8 ),
inference(superposition,[],[f170,f175]) ).
fof(f479,plain,
( ! [X0,X1] :
( ~ city(X0)
| way(X1)
| lonely(X1)
| street(X1)
| hollywood(X0)
| ~ event(sK14)
| down(sK14,X1)
| in(sK14,X0) )
| spl22_21
| ~ spl22_68 ),
inference(resolution,[],[f240,f475]) ).
fof(f481,definition,
( spl22_69
<=> ! [X1] :
( way(X1)
| down(sK14,X1)
| street(X1)
| lonely(X1) ) ),
introduced(definition,[new_symbols(definition,[spl22_69])],[avatar_definition]) ).
fof(f482,plain,
( ! [X1] :
( down(sK14,X1)
| way(X1)
| street(X1)
| lonely(X1) )
| ~ spl22_69 ),
inference(avatar_component_clause,[],[f481]) ).
fof(f484,definition,
( spl22_70
<=> ! [X0] :
( ~ city(X0)
| in(sK14,X0)
| hollywood(X0) ) ),
introduced(definition,[new_symbols(definition,[spl22_70])],[avatar_definition]) ).
fof(f485,plain,
( ! [X0] :
( in(sK14,X0)
| ~ city(X0)
| hollywood(X0) )
| ~ spl22_70 ),
inference(avatar_component_clause,[],[f484]) ).
fof(f486,plain,
( ~ spl22_30
| spl22_69
| spl22_70
| spl22_21
| ~ spl22_68 ),
inference(avatar_split_clause,[],[f479,f474,f238,f484,f481,f283]) ).
fof(f487,plain,
( ~ city(sK13)
| hollywood(sK13)
| spl22_19
| ~ spl22_70 ),
inference(resolution,[],[f485,f230]) ).
fof(f488,plain,
( spl22_32
| ~ spl22_31
| spl22_19
| ~ spl22_70 ),
inference(avatar_split_clause,[],[f487,f484,f228,f288,f293]) ).
fof(f489,plain,
( way(sK15)
| street(sK15)
| lonely(sK15)
| spl22_20
| ~ spl22_69 ),
inference(resolution,[],[f482,f235]) ).
fof(f490,plain,
( spl22_27
| spl22_29
| spl22_28
| spl22_20
| ~ spl22_69 ),
inference(avatar_split_clause,[],[f489,f481,f233,f273,f278,f268]) ).
fof(f491,plain,
( ~ in(sK8,sK2)
| spl22_36
| ~ spl22_37 ),
inference(superposition,[],[f315,f320]) ).
fof(f492,plain,
( ~ in(sK7,sK9)
| spl22_38
| ~ spl22_39 ),
inference(superposition,[],[f325,f330]) ).
fof(f493,plain,
( ! [X0,X1] :
( ~ city(X0)
| way(X1)
| lonely(X1)
| street(X1)
| hollywood(X0)
| ~ event(sK4)
| down(sK4,X1)
| in(sK4,X0) )
| spl22_52
| ~ spl22_67 ),
inference(resolution,[],[f395,f471]) ).
fof(f495,definition,
( spl22_71
<=> ! [X1] :
( way(X1)
| down(sK4,X1)
| street(X1)
| lonely(X1) ) ),
introduced(definition,[new_symbols(definition,[spl22_71])],[avatar_definition]) ).
fof(f496,plain,
( ! [X1] :
( down(sK4,X1)
| way(X1)
| street(X1)
| lonely(X1) )
| ~ spl22_71 ),
inference(avatar_component_clause,[],[f495]) ).
fof(f498,definition,
( spl22_72
<=> ! [X0] :
( ~ city(X0)
| in(sK4,X0)
| hollywood(X0) ) ),
introduced(definition,[new_symbols(definition,[spl22_72])],[avatar_definition]) ).
fof(f499,plain,
( ! [X0] :
( in(sK4,X0)
| ~ city(X0)
| hollywood(X0) )
| ~ spl22_72 ),
inference(avatar_component_clause,[],[f498]) ).
fof(f500,plain,
( ~ spl22_61
| spl22_71
| spl22_72
| spl22_52
| ~ spl22_67 ),
inference(avatar_split_clause,[],[f493,f470,f393,f498,f495,f438]) ).
fof(f501,plain,
( way(sK5)
| street(sK5)
| lonely(sK5)
| spl22_51
| ~ spl22_71 ),
inference(resolution,[],[f496,f390]) ).
fof(f502,plain,
( spl22_58
| spl22_60
| spl22_59
| spl22_51
| ~ spl22_71 ),
inference(avatar_split_clause,[],[f501,f495,f388,f428,f433,f423]) ).
fof(f503,plain,
( ~ city(sK3)
| hollywood(sK3)
| spl22_50
| ~ spl22_72 ),
inference(resolution,[],[f499,f385]) ).
fof(f504,plain,
( spl22_63
| ~ spl22_62
| spl22_50
| ~ spl22_72 ),
inference(avatar_split_clause,[],[f503,f498,f383,f443,f448]) ).
fof(f506,plain,
( ! [X2,X0,X1] :
( ~ seat(X0)
| in(sK8,X1)
| sK8 = X2
| in(X2,X0)
| ~ young(sK8)
| ~ seat(X1)
| fellow(sK8)
| ~ young(X2)
| man(X2)
| fellow(X2)
| front(X0)
| ~ furniture(X0)
| front(X1)
| ~ furniture(X1) )
| ~ spl22_4
| spl22_41 ),
inference(resolution,[],[f153,f340]) ).
fof(f508,plain,
( ! [X2,X0,X1] :
( ~ seat(X0)
| in(sK18,X1)
| sK18 = X2
| in(X2,X0)
| ~ young(sK18)
| ~ seat(X1)
| fellow(sK18)
| ~ young(X2)
| man(X2)
| fellow(X2)
| front(X0)
| ~ furniture(X0)
| front(X1)
| ~ furniture(X1) )
| ~ spl22_4
| spl22_10 ),
inference(resolution,[],[f153,f185]) ).
fof(f510,definition,
( spl22_73
<=> ! [X1] :
( in(sK18,X1)
| ~ furniture(X1)
| front(X1)
| ~ seat(X1) ) ),
introduced(definition,[new_symbols(definition,[spl22_73])],[avatar_definition]) ).
fof(f511,plain,
( ! [X1] :
( in(sK18,X1)
| ~ furniture(X1)
| front(X1)
| ~ seat(X1) )
| ~ spl22_73 ),
inference(avatar_component_clause,[],[f510]) ).
fof(f513,definition,
( spl22_74
<=> ! [X2,X0] :
( ~ seat(X0)
| ~ furniture(X0)
| front(X0)
| fellow(X2)
| man(X2)
| ~ young(X2)
| sK18 = X2
| in(X2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl22_74])],[avatar_definition]) ).
fof(f514,plain,
( ! [X2,X0] :
( man(X2)
| ~ furniture(X0)
| front(X0)
| fellow(X2)
| ~ seat(X0)
| ~ young(X2)
| sK18 = X2
| in(X2,X0) )
| ~ spl22_74 ),
inference(avatar_component_clause,[],[f513]) ).
fof(f515,plain,
( spl22_11
| ~ spl22_9
| spl22_73
| spl22_74
| ~ spl22_4
| spl22_10 ),
inference(avatar_split_clause,[],[f508,f183,f152,f513,f510,f178,f188]) ).
fof(f517,definition,
( spl22_75
<=> ! [X1] :
( in(sK17,X1)
| ~ furniture(X1)
| front(X1)
| ~ seat(X1) ) ),
introduced(definition,[new_symbols(definition,[spl22_75])],[avatar_definition]) ).
fof(f518,plain,
( ! [X1] :
( in(sK17,X1)
| ~ furniture(X1)
| front(X1)
| ~ seat(X1) )
| ~ spl22_75 ),
inference(avatar_component_clause,[],[f517]) ).
fof(f524,definition,
( spl22_77
<=> ! [X1] :
( in(sK8,X1)
| ~ furniture(X1)
| front(X1)
| ~ seat(X1) ) ),
introduced(definition,[new_symbols(definition,[spl22_77])],[avatar_definition]) ).
fof(f525,plain,
( ! [X1] :
( in(sK8,X1)
| ~ furniture(X1)
| front(X1)
| ~ seat(X1) )
| ~ spl22_77 ),
inference(avatar_component_clause,[],[f524]) ).
fof(f527,definition,
( spl22_78
<=> ! [X2,X0] :
( ~ seat(X0)
| ~ furniture(X0)
| front(X0)
| fellow(X2)
| man(X2)
| ~ young(X2)
| sK8 = X2
| in(X2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl22_78])],[avatar_definition]) ).
fof(f528,plain,
( ! [X2,X0] :
( man(X2)
| ~ furniture(X0)
| front(X0)
| fellow(X2)
| ~ seat(X0)
| ~ young(X2)
| sK8 = X2
| in(X2,X0) )
| ~ spl22_78 ),
inference(avatar_component_clause,[],[f527]) ).
fof(f529,plain,
( spl22_42
| ~ spl22_40
| spl22_77
| spl22_78
| ~ spl22_4
| spl22_41 ),
inference(avatar_split_clause,[],[f506,f338,f152,f527,f524,f333,f343]) ).
fof(f531,definition,
( spl22_79
<=> ! [X1] :
( in(sK7,X1)
| ~ furniture(X1)
| front(X1)
| ~ seat(X1) ) ),
introduced(definition,[new_symbols(definition,[spl22_79])],[avatar_definition]) ).
fof(f532,plain,
( ! [X1] :
( in(sK7,X1)
| ~ furniture(X1)
| front(X1)
| ~ seat(X1) )
| ~ spl22_79 ),
inference(avatar_component_clause,[],[f531]) ).
fof(f539,plain,
( ! [X0] :
( ~ furniture(X0)
| front(X0)
| fellow(sK17)
| ~ seat(X0)
| ~ young(sK17)
| sK17 = sK18
| in(sK17,X0) )
| spl22_13
| ~ spl22_74 ),
inference(resolution,[],[f514,f200]) ).
fof(f546,plain,
( ! [X0] :
( ~ furniture(X0)
| front(X0)
| fellow(sK7)
| ~ seat(X0)
| ~ young(sK7)
| sK7 = sK8
| in(sK7,X0) )
| spl22_44
| ~ spl22_78 ),
inference(resolution,[],[f528,f355]) ).
fof(f551,plain,
( ~ furniture(sK12)
| front(sK12)
| ~ seat(sK12)
| spl22_7
| ~ spl22_8
| ~ spl22_75 ),
inference(resolution,[],[f478,f518]) ).
fof(f552,plain,
( ~ spl22_35
| spl22_33
| ~ spl22_34
| spl22_7
| ~ spl22_8
| ~ spl22_75 ),
inference(avatar_split_clause,[],[f551,f517,f173,f168,f303,f298,f308]) ).
fof(f553,plain,
( ~ furniture(sK2)
| front(sK2)
| ~ seat(sK2)
| spl22_36
| ~ spl22_37
| ~ spl22_77 ),
inference(resolution,[],[f491,f525]) ).
fof(f554,plain,
( ~ spl22_66
| spl22_64
| ~ spl22_65
| spl22_36
| ~ spl22_37
| ~ spl22_77 ),
inference(avatar_split_clause,[],[f553,f524,f318,f313,f458,f453,f463]) ).
fof(f555,plain,
( ~ furniture(sK9)
| front(sK9)
| ~ seat(sK9)
| spl22_38
| ~ spl22_39
| ~ spl22_79 ),
inference(resolution,[],[f492,f532]) ).
fof(f556,plain,
( ~ spl22_49
| spl22_47
| ~ spl22_48
| spl22_38
| ~ spl22_39
| ~ spl22_79 ),
inference(avatar_split_clause,[],[f555,f531,f328,f323,f373,f368,f378]) ).
fof(f557,plain,
( spl22_46
| ~ spl22_43
| spl22_45
| spl22_79
| spl22_44
| ~ spl22_78 ),
inference(avatar_split_clause,[],[f546,f527,f353,f531,f358,f348,f363]) ).
fof(f563,plain,
( spl22_15
| ~ spl22_12
| spl22_14
| spl22_75
| spl22_13
| ~ spl22_74 ),
inference(avatar_split_clause,[],[f539,f513,f198,f517,f203,f193,f208]) ).
fof(f564,plain,
( ~ furniture(sK19)
| front(sK19)
| ~ seat(sK19)
| spl22_5
| ~ spl22_6
| ~ spl22_73 ),
inference(resolution,[],[f511,f477]) ).
fof(f565,plain,
( ~ spl22_18
| spl22_16
| ~ spl22_17
| spl22_5
| ~ spl22_6
| ~ spl22_73 ),
inference(avatar_split_clause,[],[f564,f510,f163,f158,f218,f213,f223]) ).
cnf(s1,plain,
( spl22_1
| ~ spl22_2 ),
inference(sat_conversion,[],[f147]) ).
cnf(s4,plain,
( spl22_3
| spl22_4
| spl22_3
| spl22_4 ),
inference(sat_conversion,[],[f156]) ).
cnf(s5,plain,
( spl22_3
| spl22_4 ),
inference(rat,[],[s4]) ).
cnf(s6,plain,
( ~ spl22_1
| ~ spl22_5 ),
inference(sat_conversion,[],[f161]) ).
cnf(s7,plain,
( ~ spl22_1
| spl22_6 ),
inference(sat_conversion,[],[f166]) ).
cnf(s8,plain,
( ~ spl22_1
| ~ spl22_7 ),
inference(sat_conversion,[],[f171]) ).
cnf(s9,plain,
( ~ spl22_1
| spl22_8 ),
inference(sat_conversion,[],[f176]) ).
cnf(s10,plain,
( ~ spl22_1
| spl22_9 ),
inference(sat_conversion,[],[f181]) ).
cnf(s11,plain,
( ~ spl22_1
| ~ spl22_10 ),
inference(sat_conversion,[],[f186]) ).
cnf(s12,plain,
( ~ spl22_1
| ~ spl22_11 ),
inference(sat_conversion,[],[f191]) ).
cnf(s13,plain,
( ~ spl22_1
| spl22_12 ),
inference(sat_conversion,[],[f196]) ).
cnf(s14,plain,
( ~ spl22_1
| ~ spl22_13 ),
inference(sat_conversion,[],[f201]) ).
cnf(s15,plain,
( ~ spl22_1
| ~ spl22_14 ),
inference(sat_conversion,[],[f206]) ).
cnf(s16,plain,
( ~ spl22_1
| ~ spl22_15 ),
inference(sat_conversion,[],[f211]) ).
cnf(s17,plain,
( ~ spl22_1
| ~ spl22_16 ),
inference(sat_conversion,[],[f216]) ).
cnf(s18,plain,
( ~ spl22_1
| spl22_17 ),
inference(sat_conversion,[],[f221]) ).
cnf(s19,plain,
( ~ spl22_1
| spl22_18 ),
inference(sat_conversion,[],[f226]) ).
cnf(s20,plain,
( ~ spl22_1
| ~ spl22_19 ),
inference(sat_conversion,[],[f231]) ).
cnf(s21,plain,
( ~ spl22_1
| ~ spl22_20 ),
inference(sat_conversion,[],[f236]) ).
cnf(s22,plain,
( ~ spl22_1
| ~ spl22_21 ),
inference(sat_conversion,[],[f241]) ).
cnf(s23,plain,
( ~ spl22_1
| spl22_22 ),
inference(sat_conversion,[],[f246]) ).
cnf(s24,plain,
( ~ spl22_1
| ~ spl22_23 ),
inference(sat_conversion,[],[f251]) ).
cnf(s25,plain,
( ~ spl22_1
| spl22_24 ),
inference(sat_conversion,[],[f256]) ).
cnf(s26,plain,
( ~ spl22_1
| ~ spl22_25 ),
inference(sat_conversion,[],[f261]) ).
cnf(s27,plain,
( ~ spl22_1
| spl22_26 ),
inference(sat_conversion,[],[f266]) ).
cnf(s28,plain,
( ~ spl22_1
| ~ spl22_27 ),
inference(sat_conversion,[],[f271]) ).
cnf(s29,plain,
( ~ spl22_1
| ~ spl22_28 ),
inference(sat_conversion,[],[f276]) ).
cnf(s30,plain,
( ~ spl22_1
| ~ spl22_29 ),
inference(sat_conversion,[],[f281]) ).
cnf(s31,plain,
( ~ spl22_1
| spl22_30 ),
inference(sat_conversion,[],[f286]) ).
cnf(s32,plain,
( ~ spl22_1
| spl22_31 ),
inference(sat_conversion,[],[f291]) ).
cnf(s33,plain,
( ~ spl22_1
| ~ spl22_32 ),
inference(sat_conversion,[],[f296]) ).
cnf(s34,plain,
( ~ spl22_1
| ~ spl22_33 ),
inference(sat_conversion,[],[f301]) ).
cnf(s35,plain,
( ~ spl22_1
| spl22_34 ),
inference(sat_conversion,[],[f306]) ).
cnf(s36,plain,
( ~ spl22_1
| spl22_35 ),
inference(sat_conversion,[],[f311]) ).
cnf(s37,plain,
( spl22_2
| ~ spl22_36 ),
inference(sat_conversion,[],[f316]) ).
cnf(s38,plain,
( spl22_2
| spl22_37 ),
inference(sat_conversion,[],[f321]) ).
cnf(s39,plain,
( spl22_2
| ~ spl22_38 ),
inference(sat_conversion,[],[f326]) ).
cnf(s40,plain,
( spl22_2
| spl22_39 ),
inference(sat_conversion,[],[f331]) ).
cnf(s41,plain,
( spl22_2
| spl22_40 ),
inference(sat_conversion,[],[f336]) ).
cnf(s42,plain,
( spl22_2
| ~ spl22_41 ),
inference(sat_conversion,[],[f341]) ).
cnf(s43,plain,
( spl22_2
| ~ spl22_42 ),
inference(sat_conversion,[],[f346]) ).
cnf(s44,plain,
( spl22_2
| spl22_43 ),
inference(sat_conversion,[],[f351]) ).
cnf(s45,plain,
( spl22_2
| ~ spl22_44 ),
inference(sat_conversion,[],[f356]) ).
cnf(s46,plain,
( spl22_2
| ~ spl22_45 ),
inference(sat_conversion,[],[f361]) ).
cnf(s47,plain,
( spl22_2
| ~ spl22_46 ),
inference(sat_conversion,[],[f366]) ).
cnf(s48,plain,
( spl22_2
| ~ spl22_47 ),
inference(sat_conversion,[],[f371]) ).
cnf(s49,plain,
( spl22_2
| spl22_48 ),
inference(sat_conversion,[],[f376]) ).
cnf(s50,plain,
( spl22_2
| spl22_49 ),
inference(sat_conversion,[],[f381]) ).
cnf(s51,plain,
( spl22_2
| ~ spl22_50 ),
inference(sat_conversion,[],[f386]) ).
cnf(s52,plain,
( spl22_2
| ~ spl22_51 ),
inference(sat_conversion,[],[f391]) ).
cnf(s53,plain,
( spl22_2
| ~ spl22_52 ),
inference(sat_conversion,[],[f396]) ).
cnf(s54,plain,
( spl22_2
| spl22_53 ),
inference(sat_conversion,[],[f401]) ).
cnf(s55,plain,
( spl22_2
| ~ spl22_54 ),
inference(sat_conversion,[],[f406]) ).
cnf(s56,plain,
( spl22_2
| spl22_55 ),
inference(sat_conversion,[],[f411]) ).
cnf(s57,plain,
( spl22_2
| ~ spl22_56 ),
inference(sat_conversion,[],[f416]) ).
cnf(s58,plain,
( spl22_2
| spl22_57 ),
inference(sat_conversion,[],[f421]) ).
cnf(s59,plain,
( spl22_2
| ~ spl22_58 ),
inference(sat_conversion,[],[f426]) ).
cnf(s60,plain,
( spl22_2
| ~ spl22_59 ),
inference(sat_conversion,[],[f431]) ).
cnf(s61,plain,
( spl22_2
| ~ spl22_60 ),
inference(sat_conversion,[],[f436]) ).
cnf(s62,plain,
( spl22_2
| spl22_61 ),
inference(sat_conversion,[],[f441]) ).
cnf(s63,plain,
( spl22_2
| spl22_62 ),
inference(sat_conversion,[],[f446]) ).
cnf(s64,plain,
( spl22_2
| ~ spl22_63 ),
inference(sat_conversion,[],[f451]) ).
cnf(s65,plain,
( spl22_2
| ~ spl22_64 ),
inference(sat_conversion,[],[f456]) ).
cnf(s66,plain,
( spl22_2
| spl22_65 ),
inference(sat_conversion,[],[f461]) ).
cnf(s67,plain,
( spl22_2
| spl22_66 ),
inference(sat_conversion,[],[f466]) ).
cnf(s68,plain,
( ~ spl22_3
| ~ spl22_53
| spl22_54
| ~ spl22_55
| spl22_56
| ~ spl22_57
| spl22_67 ),
inference(sat_conversion,[],[f472]) ).
cnf(s69,plain,
( ~ spl22_3
| ~ spl22_22
| spl22_23
| ~ spl22_24
| spl22_25
| ~ spl22_26
| spl22_68 ),
inference(sat_conversion,[],[f476]) ).
cnf(s70,plain,
( spl22_21
| ~ spl22_30
| ~ spl22_68
| spl22_69
| spl22_70 ),
inference(sat_conversion,[],[f486]) ).
cnf(s71,plain,
( spl22_19
| ~ spl22_31
| spl22_32
| ~ spl22_70 ),
inference(sat_conversion,[],[f488]) ).
cnf(s72,plain,
( spl22_20
| spl22_27
| spl22_28
| spl22_29
| ~ spl22_69 ),
inference(sat_conversion,[],[f490]) ).
cnf(s73,plain,
( spl22_52
| ~ spl22_61
| ~ spl22_67
| spl22_71
| spl22_72 ),
inference(sat_conversion,[],[f500]) ).
cnf(s74,plain,
( spl22_51
| spl22_58
| spl22_59
| spl22_60
| ~ spl22_71 ),
inference(sat_conversion,[],[f502]) ).
cnf(s75,plain,
( spl22_50
| ~ spl22_62
| spl22_63
| ~ spl22_72 ),
inference(sat_conversion,[],[f504]) ).
cnf(s76,plain,
( ~ spl22_4
| ~ spl22_9
| spl22_10
| spl22_11
| spl22_73
| spl22_74 ),
inference(sat_conversion,[],[f515]) ).
cnf(s78,plain,
( ~ spl22_4
| ~ spl22_40
| spl22_41
| spl22_42
| spl22_77
| spl22_78 ),
inference(sat_conversion,[],[f529]) ).
cnf(s82,plain,
( spl22_7
| ~ spl22_8
| spl22_33
| ~ spl22_34
| ~ spl22_35
| ~ spl22_75 ),
inference(sat_conversion,[],[f552]) ).
cnf(s83,plain,
( spl22_36
| ~ spl22_37
| spl22_64
| ~ spl22_65
| ~ spl22_66
| ~ spl22_77 ),
inference(sat_conversion,[],[f554]) ).
cnf(s84,plain,
( spl22_38
| ~ spl22_39
| spl22_47
| ~ spl22_48
| ~ spl22_49
| ~ spl22_79 ),
inference(sat_conversion,[],[f556]) ).
cnf(s85,plain,
( ~ spl22_43
| spl22_44
| spl22_45
| spl22_46
| ~ spl22_78
| spl22_79 ),
inference(sat_conversion,[],[f557]) ).
cnf(s87,plain,
( ~ spl22_12
| spl22_13
| spl22_14
| spl22_15
| ~ spl22_74
| spl22_75 ),
inference(sat_conversion,[],[f563]) ).
cnf(s88,plain,
( spl22_5
| ~ spl22_6
| spl22_16
| ~ spl22_17
| ~ spl22_18
| ~ spl22_73 ),
inference(sat_conversion,[],[f565]) ).
cnf(s89,plain,
spl22_2,
inference(rat,[],[s5,s68,s78,s85,s73,s83,s84,s75,s74,s37,s38,s39,s40,s41,s42,s43,s44,s45,s46,s47,s48,s49,s50,s51,s52,s53,s54,s55,s56,s57,s58,s59,s60,s61,s62,s63,s64,s65,s66,s67]) ).
cnf(s90,plain,
spl22_1,
inference(rat,[],[s1,s89]) ).
cnf(s91,plain,
spl22_35,
inference(rat,[],[s36,s90]) ).
cnf(s92,plain,
spl22_34,
inference(rat,[],[s35,s90]) ).
cnf(s93,plain,
~ spl22_33,
inference(rat,[],[s34,s90]) ).
cnf(s94,plain,
~ spl22_32,
inference(rat,[],[s33,s90]) ).
cnf(s95,plain,
spl22_31,
inference(rat,[],[s32,s90]) ).
cnf(s96,plain,
spl22_30,
inference(rat,[],[s31,s90]) ).
cnf(s97,plain,
~ spl22_29,
inference(rat,[],[s30,s90]) ).
cnf(s98,plain,
~ spl22_28,
inference(rat,[],[s29,s90]) ).
cnf(s99,plain,
~ spl22_27,
inference(rat,[],[s28,s90]) ).
cnf(s100,plain,
spl22_26,
inference(rat,[],[s27,s90]) ).
cnf(s101,plain,
~ spl22_25,
inference(rat,[],[s26,s90]) ).
cnf(s102,plain,
spl22_24,
inference(rat,[],[s25,s90]) ).
cnf(s103,plain,
~ spl22_23,
inference(rat,[],[s24,s90]) ).
cnf(s104,plain,
spl22_22,
inference(rat,[],[s23,s90]) ).
cnf(s105,plain,
~ spl22_21,
inference(rat,[],[s22,s90]) ).
cnf(s106,plain,
~ spl22_20,
inference(rat,[],[s21,s90]) ).
cnf(s107,plain,
~ spl22_19,
inference(rat,[],[s20,s90]) ).
cnf(s108,plain,
spl22_18,
inference(rat,[],[s19,s90]) ).
cnf(s109,plain,
spl22_17,
inference(rat,[],[s18,s90]) ).
cnf(s110,plain,
~ spl22_16,
inference(rat,[],[s17,s90]) ).
cnf(s111,plain,
~ spl22_15,
inference(rat,[],[s16,s90]) ).
cnf(s112,plain,
~ spl22_14,
inference(rat,[],[s15,s90]) ).
cnf(s113,plain,
~ spl22_13,
inference(rat,[],[s14,s90]) ).
cnf(s114,plain,
spl22_12,
inference(rat,[],[s13,s90]) ).
cnf(s115,plain,
~ spl22_11,
inference(rat,[],[s12,s90]) ).
cnf(s116,plain,
~ spl22_10,
inference(rat,[],[s11,s90]) ).
cnf(s117,plain,
spl22_9,
inference(rat,[],[s10,s90]) ).
cnf(s118,plain,
spl22_8,
inference(rat,[],[s9,s90]) ).
cnf(s119,plain,
~ spl22_7,
inference(rat,[],[s8,s90]) ).
cnf(s120,plain,
spl22_6,
inference(rat,[],[s7,s90]) ).
cnf(s121,plain,
~ spl22_5,
inference(rat,[],[s6,s90]) ).
cnf(s122,plain,
~ spl22_69,
inference(rat,[],[s72,s99,s97,s98,s106]) ).
cnf(s123,plain,
~ spl22_70,
inference(rat,[],[s71,s95,s94,s107]) ).
cnf(s124,plain,
~ spl22_75,
inference(rat,[],[s82,s118,s91,s92,s93,s119]) ).
cnf(s125,plain,
~ spl22_73,
inference(rat,[],[s88,s120,s108,s109,s110,s121]) ).
cnf(s126,plain,
~ spl22_68,
inference(rat,[],[s70,s123,s105,s96,s122]) ).
cnf(s127,plain,
~ spl22_74,
inference(rat,[],[s87,s114,s113,s111,s112,s124]) ).
cnf(s128,plain,
~ spl22_4,
inference(rat,[],[s76,s127,s117,s115,s116,s125]) ).
cnf(s129,plain,
~ spl22_3,
inference(rat,[],[s69,s104,s100,s101,s102,s103,s126]) ).
cnf(s130,plain,
$false,
inference(rat,[],[s5,s128,s129]) ).
fof(f566,plain,
$false,
inference(avatar_sat_refutation,[],[s130]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP011+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.37 % Computer : n007.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 17:45:25 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.41 Running first-order model finding
% 0.10/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.47 % (1687249)Will run a generic schedule for satisfiability detection.
% 0.17/0.47 % (1687254)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1002633420_2999 on theBenchmark for (2999ds/0Mi)
% 0.17/0.47 % (1687255)% WARNING: option uhcvi not known.
% 0.17/0.47 % Detected minimum model sizes of [1]
% 0.17/0.47 % Detected maximum model sizes of [20]
% 0.17/0.47 % TRYING [1]
% 0.17/0.47 % TRYING [2]
% 0.17/0.47 % TRYING [3]
% 0.17/0.47 % TRYING [4]
% 0.17/0.47 % (1687259)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=198695684:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.17/0.47 % (1687255)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=215433572:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.17/0.47 % (1687256)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2862733884:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.17/0.47 % (1687257)dis+10_1_sil=32000:sp=arity:random_seed=1682221475:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.17/0.47 % (1687258)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1314588211:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.17/0.47 % (1687260)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4046496535:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.17/0.47 % TRYING [5]
% 0.17/0.47 % TRYING [6]
% 0.17/0.47 % (1687260) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1687249-1687260"...
% 0.17/0.47 % (1687257) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1687249-1687257"...
% 0.17/0.47 % (1687259) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1687249-1687259"...
% 0.17/0.47 % (1687260)...printing done.
% 0.17/0.47 % (1687257)...printing done.
% 0.17/0.47 % TRYING [7]
% 0.17/0.47 % (1687260)Refutation found. Thanks to Tanya!
% 0.17/0.47 % SZS status Theorem for theBenchmark
% 0.17/0.47 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/0.48 % (1687260)------------------------------
% 0.17/0.48 % (1687260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.17/0.48 % (1687260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/0.48 % (1687260)CaDiCaL version: 2.1.3
% 0.17/0.48 % (1687260)Termination reason: Refutation
% 0.17/0.48 % (1687260)Time elapsed: 0.012 s
% 0.17/0.48 % (1687260)Peak memory usage: 13 MB
% 0.17/0.48 % (1687260)Instructions burned: 18 (million)
% 0.17/0.48 % (1687249)Success in time 0.055 s
% 0.17/0.48 % Vampire exiting
%------------------------------------------------------------------------------