%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NLP004+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 : n017.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:22 PM UTC 2026
% Result : Theorem 0.20s 0.49s
% Output : Refutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 95
% Syntax : Number of formulae : 510 ( 50 unt; 94 def)
% Number of atoms : 2502 ( 137 equ)
% Maximal formula atoms : 124 ( 4 avg)
% Number of connectives : 3330 (1338 ~;1378 |; 518 &)
% ( 92 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 83 ( 6 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 116 ( 114 usr; 95 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 20 con; 0-0 aty)
% Number of variables : 398 ( 0 sgn 248 !; 150 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
( ( ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( seat(X0)
& furniture(X0)
& front(X0)
& seat(X1)
& furniture(X1)
& front(X1)
& hollywood(X2)
& city(X2)
& event(X3)
& street(X4)
& way(X4)
& lonely(X4)
& chevy(X5)
& car(X5)
& white(X5)
& dirty(X5)
& old(X5)
& barrel(X3,X5)
& down(X3,X4)
& in(X3,X2)
& X6 != X7
& fellow(X6)
& man(X6)
& young(X6)
& fellow(X7)
& man(X7)
& young(X7)
& X6 = X8
& in(X8,X0)
& X7 = X9
& in(X9,X1) )
=> ? [X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
( seat(X10)
& furniture(X10)
& front(X10)
& seat(X11)
& furniture(X11)
& front(X11)
& hollywood(X12)
& city(X12)
& event(X13)
& chevy(X14)
& car(X14)
& white(X14)
& dirty(X14)
& old(X14)
& street(X15)
& way(X15)
& lonely(X15)
& barrel(X13,X14)
& down(X13,X15)
& in(X13,X12)
& X16 != X17
& fellow(X16)
& man(X16)
& young(X16)
& fellow(X17)
& man(X17)
& young(X17)
& X16 = X18
& in(X18,X10)
& X17 = X19
& in(X19,X11) ) )
& ( ? [X20,X21,X22,X23,X24,X25,X26,X27,X28,X29] :
( seat(X20)
& furniture(X20)
& front(X20)
& seat(X21)
& furniture(X21)
& front(X21)
& hollywood(X22)
& city(X22)
& event(X23)
& chevy(X24)
& car(X24)
& white(X24)
& dirty(X24)
& old(X24)
& street(X25)
& way(X25)
& lonely(X25)
& barrel(X23,X24)
& down(X23,X25)
& in(X23,X22)
& X26 != X27
& fellow(X26)
& man(X26)
& young(X26)
& fellow(X27)
& man(X27)
& young(X27)
& X26 = X28
& in(X28,X20)
& X27 = X29
& in(X29,X21) )
=> ? [X30,X31,X32,X33,X34,X35,X36,X37,X38,X39] :
( seat(X30)
& furniture(X30)
& front(X30)
& seat(X31)
& furniture(X31)
& front(X31)
& hollywood(X32)
& city(X32)
& event(X33)
& street(X34)
& way(X34)
& lonely(X34)
& chevy(X35)
& car(X35)
& white(X35)
& dirty(X35)
& old(X35)
& barrel(X33,X35)
& down(X33,X34)
& in(X33,X32)
& X36 != X37
& fellow(X36)
& man(X36)
& young(X36)
& fellow(X37)
& man(X37)
& young(X37)
& X36 = X38
& in(X38,X30)
& X37 = X39
& in(X39,X31) ) ) ),
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)
& seat(X1)
& furniture(X1)
& front(X1)
& hollywood(X2)
& city(X2)
& event(X3)
& street(X4)
& way(X4)
& lonely(X4)
& chevy(X5)
& car(X5)
& white(X5)
& dirty(X5)
& old(X5)
& barrel(X3,X5)
& down(X3,X4)
& in(X3,X2)
& X6 != X7
& fellow(X6)
& man(X6)
& young(X6)
& fellow(X7)
& man(X7)
& young(X7)
& X6 = X8
& in(X8,X0)
& X7 = X9
& in(X9,X1) )
=> ? [X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
( seat(X10)
& furniture(X10)
& front(X10)
& seat(X11)
& furniture(X11)
& front(X11)
& hollywood(X12)
& city(X12)
& event(X13)
& chevy(X14)
& car(X14)
& white(X14)
& dirty(X14)
& old(X14)
& street(X15)
& way(X15)
& lonely(X15)
& barrel(X13,X14)
& down(X13,X15)
& in(X13,X12)
& X16 != X17
& fellow(X16)
& man(X16)
& young(X16)
& fellow(X17)
& man(X17)
& young(X17)
& X16 = X18
& in(X18,X10)
& X17 = X19
& in(X19,X11) ) )
& ( ? [X20,X21,X22,X23,X24,X25,X26,X27,X28,X29] :
( seat(X20)
& furniture(X20)
& front(X20)
& seat(X21)
& furniture(X21)
& front(X21)
& hollywood(X22)
& city(X22)
& event(X23)
& chevy(X24)
& car(X24)
& white(X24)
& dirty(X24)
& old(X24)
& street(X25)
& way(X25)
& lonely(X25)
& barrel(X23,X24)
& down(X23,X25)
& in(X23,X22)
& X26 != X27
& fellow(X26)
& man(X26)
& young(X26)
& fellow(X27)
& man(X27)
& young(X27)
& X26 = X28
& in(X28,X20)
& X27 = X29
& in(X29,X21) )
=> ? [X30,X31,X32,X33,X34,X35,X36,X37,X38,X39] :
( seat(X30)
& furniture(X30)
& front(X30)
& seat(X31)
& furniture(X31)
& front(X31)
& hollywood(X32)
& city(X32)
& event(X33)
& street(X34)
& way(X34)
& lonely(X34)
& chevy(X35)
& car(X35)
& white(X35)
& dirty(X35)
& old(X35)
& barrel(X33,X35)
& down(X33,X34)
& in(X33,X32)
& X36 != X37
& fellow(X36)
& man(X36)
& young(X36)
& fellow(X37)
& man(X37)
& young(X37)
& X36 = X38
& in(X38,X30)
& X37 = X39
& in(X39,X31) ) ) ),
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)
| ~ seat(X11)
| ~ furniture(X11)
| ~ front(X11)
| ~ hollywood(X12)
| ~ city(X12)
| ~ event(X13)
| ~ chevy(X14)
| ~ car(X14)
| ~ white(X14)
| ~ dirty(X14)
| ~ old(X14)
| ~ street(X15)
| ~ way(X15)
| ~ lonely(X15)
| ~ barrel(X13,X14)
| ~ down(X13,X15)
| ~ in(X13,X12)
| X16 = X17
| ~ fellow(X16)
| ~ man(X16)
| ~ young(X16)
| ~ fellow(X17)
| ~ man(X17)
| ~ young(X17)
| X16 != X18
| ~ in(X18,X10)
| X17 != X19
| ~ in(X19,X11) )
& ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( seat(X0)
& furniture(X0)
& front(X0)
& seat(X1)
& furniture(X1)
& front(X1)
& hollywood(X2)
& city(X2)
& event(X3)
& street(X4)
& way(X4)
& lonely(X4)
& chevy(X5)
& car(X5)
& white(X5)
& dirty(X5)
& old(X5)
& barrel(X3,X5)
& down(X3,X4)
& in(X3,X2)
& X6 != X7
& fellow(X6)
& man(X6)
& young(X6)
& fellow(X7)
& man(X7)
& young(X7)
& X6 = X8
& in(X8,X0)
& X7 = X9
& in(X9,X1) ) )
| ( ! [X30,X31,X32,X33,X34,X35,X36,X37,X38,X39] :
( ~ seat(X30)
| ~ furniture(X30)
| ~ front(X30)
| ~ seat(X31)
| ~ furniture(X31)
| ~ front(X31)
| ~ hollywood(X32)
| ~ city(X32)
| ~ event(X33)
| ~ street(X34)
| ~ way(X34)
| ~ lonely(X34)
| ~ chevy(X35)
| ~ car(X35)
| ~ white(X35)
| ~ dirty(X35)
| ~ old(X35)
| ~ barrel(X33,X35)
| ~ down(X33,X34)
| ~ in(X33,X32)
| X36 = X37
| ~ fellow(X36)
| ~ man(X36)
| ~ young(X36)
| ~ fellow(X37)
| ~ man(X37)
| ~ young(X37)
| X36 != X38
| ~ in(X38,X30)
| X37 != X39
| ~ in(X39,X31) )
& ? [X20,X21,X22,X23,X24,X25,X26,X27,X28,X29] :
( seat(X20)
& furniture(X20)
& front(X20)
& seat(X21)
& furniture(X21)
& front(X21)
& hollywood(X22)
& city(X22)
& event(X23)
& chevy(X24)
& car(X24)
& white(X24)
& dirty(X24)
& old(X24)
& street(X25)
& way(X25)
& lonely(X25)
& barrel(X23,X24)
& down(X23,X25)
& in(X23,X22)
& X26 != X27
& fellow(X26)
& man(X26)
& young(X26)
& fellow(X27)
& man(X27)
& young(X27)
& X26 = X28
& in(X28,X20)
& X27 = X29
& in(X29,X21) ) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f4,definition,
( ? [X20,X21,X22,X23,X24,X25,X26,X27,X28,X29] :
( seat(X20)
& furniture(X20)
& front(X20)
& seat(X21)
& furniture(X21)
& front(X21)
& hollywood(X22)
& city(X22)
& event(X23)
& chevy(X24)
& car(X24)
& white(X24)
& dirty(X24)
& old(X24)
& street(X25)
& way(X25)
& lonely(X25)
& barrel(X23,X24)
& down(X23,X25)
& in(X23,X22)
& X26 != X27
& fellow(X26)
& man(X26)
& young(X26)
& fellow(X27)
& man(X27)
& young(X27)
& X26 = X28
& in(X28,X20)
& X27 = X29
& in(X29,X21) )
| ~ 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)
& seat(X1)
& furniture(X1)
& front(X1)
& hollywood(X2)
& city(X2)
& event(X3)
& street(X4)
& way(X4)
& lonely(X4)
& chevy(X5)
& car(X5)
& white(X5)
& dirty(X5)
& old(X5)
& barrel(X3,X5)
& down(X3,X4)
& in(X3,X2)
& X6 != X7
& fellow(X6)
& man(X6)
& young(X6)
& fellow(X7)
& man(X7)
& young(X7)
& X6 = X8
& in(X8,X0)
& X7 = X9
& in(X9,X1) )
| ~ 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)
| ~ seat(X11)
| ~ furniture(X11)
| ~ front(X11)
| ~ hollywood(X12)
| ~ city(X12)
| ~ event(X13)
| ~ chevy(X14)
| ~ car(X14)
| ~ white(X14)
| ~ dirty(X14)
| ~ old(X14)
| ~ street(X15)
| ~ way(X15)
| ~ lonely(X15)
| ~ barrel(X13,X14)
| ~ down(X13,X15)
| ~ in(X13,X12)
| X16 = X17
| ~ fellow(X16)
| ~ man(X16)
| ~ young(X16)
| ~ fellow(X17)
| ~ man(X17)
| ~ young(X17)
| X16 != X18
| ~ in(X18,X10)
| X17 != X19
| ~ in(X19,X11) )
& sP1 )
| ( ! [X30,X31,X32,X33,X34,X35,X36,X37,X38,X39] :
( ~ seat(X30)
| ~ furniture(X30)
| ~ front(X30)
| ~ seat(X31)
| ~ furniture(X31)
| ~ front(X31)
| ~ hollywood(X32)
| ~ city(X32)
| ~ event(X33)
| ~ street(X34)
| ~ way(X34)
| ~ lonely(X34)
| ~ chevy(X35)
| ~ car(X35)
| ~ white(X35)
| ~ dirty(X35)
| ~ old(X35)
| ~ barrel(X33,X35)
| ~ down(X33,X34)
| ~ in(X33,X32)
| X36 = X37
| ~ fellow(X36)
| ~ man(X36)
| ~ young(X36)
| ~ fellow(X37)
| ~ man(X37)
| ~ young(X37)
| X36 != X38
| ~ in(X38,X30)
| X37 != X39
| ~ in(X39,X31) )
& 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)
& seat(X1)
& furniture(X1)
& front(X1)
& hollywood(X2)
& city(X2)
& event(X3)
& street(X4)
& way(X4)
& lonely(X4)
& chevy(X5)
& car(X5)
& white(X5)
& dirty(X5)
& old(X5)
& barrel(X3,X5)
& down(X3,X4)
& in(X3,X2)
& X6 != X7
& fellow(X6)
& man(X6)
& young(X6)
& fellow(X7)
& man(X7)
& young(X7)
& X6 = X8
& in(X8,X0)
& X7 = X9
& in(X9,X1) )
| ~ sP1 ),
inference(nnf_transformation,[],[f5]) ).
fof(f8,plain,
( ( seat(sK2)
& furniture(sK2)
& front(sK2)
& seat(sK3)
& furniture(sK3)
& front(sK3)
& hollywood(sK4)
& city(sK4)
& event(sK5)
& street(sK6)
& way(sK6)
& lonely(sK6)
& chevy(sK7)
& car(sK7)
& white(sK7)
& dirty(sK7)
& old(sK7)
& barrel(sK5,sK7)
& down(sK5,sK6)
& in(sK5,sK4)
& sK8 != sK9
& fellow(sK8)
& man(sK8)
& young(sK8)
& fellow(sK9)
& man(sK9)
& young(sK9)
& sK8 = sK10
& in(sK10,sK2)
& sK9 = sK11
& in(sK11,sK3) )
| ~ 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)
& seat(X21)
& furniture(X21)
& front(X21)
& hollywood(X22)
& city(X22)
& event(X23)
& chevy(X24)
& car(X24)
& white(X24)
& dirty(X24)
& old(X24)
& street(X25)
& way(X25)
& lonely(X25)
& barrel(X23,X24)
& down(X23,X25)
& in(X23,X22)
& X26 != X27
& fellow(X26)
& man(X26)
& young(X26)
& fellow(X27)
& man(X27)
& young(X27)
& X26 = X28
& in(X28,X20)
& X27 = X29
& in(X29,X21) )
| ~ sP0 ),
inference(nnf_transformation,[],[f4]) ).
fof(f10,plain,
( ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( seat(X0)
& furniture(X0)
& front(X0)
& seat(X1)
& furniture(X1)
& front(X1)
& hollywood(X2)
& city(X2)
& event(X3)
& chevy(X4)
& car(X4)
& white(X4)
& dirty(X4)
& old(X4)
& street(X5)
& way(X5)
& lonely(X5)
& barrel(X3,X4)
& down(X3,X5)
& in(X3,X2)
& X6 != X7
& fellow(X6)
& man(X6)
& young(X6)
& fellow(X7)
& man(X7)
& young(X7)
& X6 = X8
& in(X8,X0)
& X7 = X9
& in(X9,X1) )
| ~ sP0 ),
inference(rectify,[],[f9]) ).
fof(f11,plain,
( ( seat(sK12)
& furniture(sK12)
& front(sK12)
& seat(sK13)
& furniture(sK13)
& front(sK13)
& hollywood(sK14)
& city(sK14)
& event(sK15)
& chevy(sK16)
& car(sK16)
& white(sK16)
& dirty(sK16)
& old(sK16)
& street(sK17)
& way(sK17)
& lonely(sK17)
& barrel(sK15,sK16)
& down(sK15,sK17)
& in(sK15,sK14)
& sK18 != sK19
& fellow(sK18)
& man(sK18)
& young(sK18)
& fellow(sK19)
& man(sK19)
& young(sK19)
& sK18 = sK20
& in(sK20,sK12)
& sK19 = sK21
& in(sK21,sK13) )
| ~ 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)
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ hollywood(X2)
| ~ city(X2)
| ~ event(X3)
| ~ chevy(X4)
| ~ car(X4)
| ~ white(X4)
| ~ dirty(X4)
| ~ old(X4)
| ~ street(X5)
| ~ way(X5)
| ~ lonely(X5)
| ~ barrel(X3,X4)
| ~ down(X3,X5)
| ~ in(X3,X2)
| X6 = X7
| ~ fellow(X6)
| ~ man(X6)
| ~ young(X6)
| ~ fellow(X7)
| ~ man(X7)
| ~ young(X7)
| X6 != X8
| ~ in(X8,X0)
| X7 != X9
| ~ in(X9,X1) )
& sP1 )
| ( ! [X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
( ~ seat(X10)
| ~ furniture(X10)
| ~ front(X10)
| ~ seat(X11)
| ~ furniture(X11)
| ~ front(X11)
| ~ hollywood(X12)
| ~ city(X12)
| ~ event(X13)
| ~ street(X14)
| ~ way(X14)
| ~ lonely(X14)
| ~ chevy(X15)
| ~ car(X15)
| ~ white(X15)
| ~ dirty(X15)
| ~ old(X15)
| ~ barrel(X13,X15)
| ~ down(X13,X14)
| ~ in(X13,X12)
| X16 = X17
| ~ fellow(X16)
| ~ man(X16)
| ~ young(X16)
| ~ fellow(X17)
| ~ man(X17)
| ~ young(X17)
| X16 != X18
| ~ in(X18,X10)
| X17 != X19
| ~ in(X19,X11) )
& sP0 ) ),
inference(rectify,[],[f6]) ).
fof(f13,plain,
( in(sK11,sK3)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f14,plain,
( sK9 = sK11
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f15,plain,
( in(sK10,sK2)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f16,plain,
( sK8 = sK10
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f17,plain,
( young(sK9)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f18,plain,
( man(sK9)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f19,plain,
( fellow(sK9)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f20,plain,
( young(sK8)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f21,plain,
( man(sK8)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f22,plain,
( fellow(sK8)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f23,plain,
( sK8 != sK9
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f24,plain,
( in(sK5,sK4)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f25,plain,
( down(sK5,sK6)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f26,plain,
( barrel(sK5,sK7)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f27,plain,
( old(sK7)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f28,plain,
( dirty(sK7)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f29,plain,
( white(sK7)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f30,plain,
( car(sK7)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f31,plain,
( chevy(sK7)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f32,plain,
( lonely(sK6)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f33,plain,
( way(sK6)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f34,plain,
( street(sK6)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f35,plain,
( event(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f36,plain,
( city(sK4)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f37,plain,
( hollywood(sK4)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f38,plain,
( front(sK3)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f39,plain,
( furniture(sK3)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f40,plain,
( seat(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,sK13)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f45,plain,
( sK19 = sK21
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f46,plain,
( in(sK20,sK12)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f47,plain,
( sK18 = sK20
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f48,plain,
( young(sK19)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f49,plain,
( man(sK19)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f50,plain,
( fellow(sK19)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f51,plain,
( young(sK18)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f52,plain,
( man(sK18)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f53,plain,
( fellow(sK18)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f54,plain,
( sK18 != sK19
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f55,plain,
( in(sK15,sK14)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f56,plain,
( down(sK15,sK17)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f57,plain,
( barrel(sK15,sK16)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f58,plain,
( lonely(sK17)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f59,plain,
( way(sK17)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f60,plain,
( street(sK17)
| ~ 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,
( event(sK15)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f67,plain,
( city(sK14)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f68,plain,
( hollywood(sK14)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f69,plain,
( front(sK13)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f70,plain,
( furniture(sK13)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f71,plain,
( seat(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)
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ hollywood(X2)
| ~ city(X2)
| ~ event(X3)
| ~ chevy(X4)
| ~ car(X4)
| ~ white(X4)
| ~ dirty(X4)
| ~ old(X4)
| ~ street(X5)
| ~ way(X5)
| ~ lonely(X5)
| ~ barrel(X3,X4)
| ~ down(X3,X5)
| ~ in(X3,X2)
| X6 = X7
| ~ fellow(X6)
| ~ man(X6)
| ~ young(X6)
| ~ fellow(X7)
| ~ man(X7)
| ~ young(X7)
| X6 != X8
| ~ in(X8,X0)
| X7 != X9
| ~ in(X9,X1)
| ~ seat(X10)
| ~ furniture(X10)
| ~ front(X10)
| ~ seat(X11)
| ~ furniture(X11)
| ~ front(X11)
| ~ hollywood(X12)
| ~ city(X12)
| ~ event(X13)
| ~ street(X14)
| ~ way(X14)
| ~ lonely(X14)
| ~ chevy(X15)
| ~ car(X15)
| ~ white(X15)
| ~ dirty(X15)
| ~ old(X15)
| ~ barrel(X13,X15)
| ~ down(X13,X14)
| ~ in(X13,X12)
| X16 = X17
| ~ fellow(X16)
| ~ man(X16)
| ~ young(X16)
| ~ fellow(X17)
| ~ man(X17)
| ~ young(X17)
| X16 != X18
| ~ in(X18,X10)
| X17 != X19
| ~ in(X19,X11) ),
inference(cnf_transformation,[],[f12]) ).
fof(f79,plain,
! [X2,X3,X10,X0,X11,X1,X8,X18,X9,X7,X14,X4,X16,X19,X17,X15,X5,X12,X13] :
( ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ hollywood(X2)
| ~ city(X2)
| ~ event(X3)
| ~ chevy(X4)
| ~ car(X4)
| ~ white(X4)
| ~ dirty(X4)
| ~ old(X4)
| ~ street(X5)
| ~ way(X5)
| ~ lonely(X5)
| ~ barrel(X3,X4)
| ~ down(X3,X5)
| ~ in(X3,X2)
| X7 = X8
| ~ fellow(X8)
| ~ man(X8)
| ~ young(X8)
| ~ fellow(X7)
| ~ man(X7)
| ~ young(X7)
| ~ in(X8,X0)
| X7 != X9
| ~ in(X9,X1)
| ~ seat(X10)
| ~ furniture(X10)
| ~ front(X10)
| ~ seat(X11)
| ~ furniture(X11)
| ~ front(X11)
| ~ hollywood(X12)
| ~ city(X12)
| ~ event(X13)
| ~ street(X14)
| ~ way(X14)
| ~ lonely(X14)
| ~ chevy(X15)
| ~ car(X15)
| ~ white(X15)
| ~ dirty(X15)
| ~ old(X15)
| ~ barrel(X13,X15)
| ~ down(X13,X14)
| ~ in(X13,X12)
| X16 = X17
| ~ fellow(X16)
| ~ man(X16)
| ~ young(X16)
| ~ fellow(X17)
| ~ man(X17)
| ~ young(X17)
| X16 != X18
| ~ in(X18,X10)
| X17 != X19
| ~ in(X19,X11) ),
inference(equality_resolution,[],[f78]) ).
fof(f80,plain,
! [X2,X3,X10,X0,X11,X1,X8,X18,X9,X16,X14,X4,X19,X17,X15,X5,X12,X13] :
( ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ hollywood(X2)
| ~ city(X2)
| ~ event(X3)
| ~ chevy(X4)
| ~ car(X4)
| ~ white(X4)
| ~ dirty(X4)
| ~ old(X4)
| ~ street(X5)
| ~ way(X5)
| ~ lonely(X5)
| ~ barrel(X3,X4)
| ~ down(X3,X5)
| ~ in(X3,X2)
| X8 = X9
| ~ fellow(X8)
| ~ man(X8)
| ~ young(X8)
| ~ fellow(X9)
| ~ man(X9)
| ~ young(X9)
| ~ in(X8,X0)
| ~ in(X9,X1)
| ~ seat(X10)
| ~ furniture(X10)
| ~ front(X10)
| ~ seat(X11)
| ~ furniture(X11)
| ~ front(X11)
| ~ hollywood(X12)
| ~ city(X12)
| ~ event(X13)
| ~ street(X14)
| ~ way(X14)
| ~ lonely(X14)
| ~ chevy(X15)
| ~ car(X15)
| ~ white(X15)
| ~ dirty(X15)
| ~ old(X15)
| ~ barrel(X13,X15)
| ~ down(X13,X14)
| ~ in(X13,X12)
| X16 = X17
| ~ fellow(X16)
| ~ man(X16)
| ~ young(X16)
| ~ fellow(X17)
| ~ man(X17)
| ~ young(X17)
| X16 != X18
| ~ in(X18,X10)
| X17 != X19
| ~ in(X19,X11) ),
inference(equality_resolution,[],[f79]) ).
fof(f81,plain,
! [X2,X3,X10,X0,X11,X1,X8,X18,X9,X19,X14,X4,X17,X15,X5,X12,X13] :
( ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ hollywood(X2)
| ~ city(X2)
| ~ event(X3)
| ~ chevy(X4)
| ~ car(X4)
| ~ white(X4)
| ~ dirty(X4)
| ~ old(X4)
| ~ street(X5)
| ~ way(X5)
| ~ lonely(X5)
| ~ barrel(X3,X4)
| ~ down(X3,X5)
| ~ in(X3,X2)
| X8 = X9
| ~ fellow(X8)
| ~ man(X8)
| ~ young(X8)
| ~ fellow(X9)
| ~ man(X9)
| ~ young(X9)
| ~ in(X8,X0)
| ~ in(X9,X1)
| ~ seat(X10)
| ~ furniture(X10)
| ~ front(X10)
| ~ seat(X11)
| ~ furniture(X11)
| ~ front(X11)
| ~ hollywood(X12)
| ~ city(X12)
| ~ event(X13)
| ~ street(X14)
| ~ way(X14)
| ~ lonely(X14)
| ~ chevy(X15)
| ~ car(X15)
| ~ white(X15)
| ~ dirty(X15)
| ~ old(X15)
| ~ barrel(X13,X15)
| ~ down(X13,X14)
| ~ in(X13,X12)
| X17 = X18
| ~ fellow(X18)
| ~ man(X18)
| ~ young(X18)
| ~ fellow(X17)
| ~ man(X17)
| ~ young(X17)
| ~ in(X18,X10)
| X17 != X19
| ~ in(X19,X11) ),
inference(equality_resolution,[],[f80]) ).
fof(f82,plain,
! [X2,X3,X10,X0,X11,X1,X8,X18,X9,X19,X14,X4,X15,X5,X12,X13] :
( ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ seat(X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ hollywood(X2)
| ~ city(X2)
| ~ event(X3)
| ~ chevy(X4)
| ~ car(X4)
| ~ white(X4)
| ~ dirty(X4)
| ~ old(X4)
| ~ street(X5)
| ~ way(X5)
| ~ lonely(X5)
| ~ barrel(X3,X4)
| ~ down(X3,X5)
| ~ in(X3,X2)
| X8 = X9
| ~ fellow(X8)
| ~ man(X8)
| ~ young(X8)
| ~ fellow(X9)
| ~ man(X9)
| ~ young(X9)
| ~ in(X8,X0)
| ~ in(X9,X1)
| ~ seat(X10)
| ~ furniture(X10)
| ~ front(X10)
| ~ seat(X11)
| ~ furniture(X11)
| ~ front(X11)
| ~ hollywood(X12)
| ~ city(X12)
| ~ event(X13)
| ~ street(X14)
| ~ way(X14)
| ~ lonely(X14)
| ~ chevy(X15)
| ~ car(X15)
| ~ white(X15)
| ~ dirty(X15)
| ~ old(X15)
| ~ barrel(X13,X15)
| ~ down(X13,X14)
| ~ in(X13,X12)
| X18 = X19
| ~ fellow(X18)
| ~ man(X18)
| ~ young(X18)
| ~ fellow(X19)
| ~ man(X19)
| ~ young(X19)
| ~ in(X18,X10)
| ~ in(X19,X11) ),
inference(equality_resolution,[],[f81]) ).
fof(f87,plain,
( ~ furniture(sK2)
| ~ sP1 ),
inference(consistent_polarity_flipping,[],[f42]) ).
fof(f88,plain,
( ~ furniture(sK3)
| ~ sP1 ),
inference(consistent_polarity_flipping,[],[f39]) ).
fof(f89,plain,
( ~ hollywood(sK4)
| ~ sP1 ),
inference(consistent_polarity_flipping,[],[f37]) ).
fof(f90,plain,
( ~ event(sK5)
| ~ sP1 ),
inference(consistent_polarity_flipping,[],[f35]) ).
fof(f91,plain,
( ~ street(sK6)
| ~ sP1 ),
inference(consistent_polarity_flipping,[],[f34]) ).
fof(f92,plain,
( ~ chevy(sK7)
| ~ sP1 ),
inference(consistent_polarity_flipping,[],[f31]) ).
fof(f93,plain,
( ~ white(sK7)
| ~ sP1 ),
inference(consistent_polarity_flipping,[],[f29]) ).
fof(f94,plain,
( ~ barrel(sK5,sK7)
| ~ sP1 ),
inference(consistent_polarity_flipping,[],[f26]) ).
fof(f95,plain,
( ~ down(sK5,sK6)
| ~ sP1 ),
inference(consistent_polarity_flipping,[],[f25]) ).
fof(f96,plain,
( ~ furniture(sK12)
| ~ sP0 ),
inference(consistent_polarity_flipping,[],[f73]) ).
fof(f97,plain,
( ~ furniture(sK13)
| ~ sP0 ),
inference(consistent_polarity_flipping,[],[f70]) ).
fof(f98,plain,
( ~ hollywood(sK14)
| ~ sP0 ),
inference(consistent_polarity_flipping,[],[f68]) ).
fof(f99,plain,
( ~ event(sK15)
| ~ sP0 ),
inference(consistent_polarity_flipping,[],[f66]) ).
fof(f100,plain,
( ~ chevy(sK16)
| ~ sP0 ),
inference(consistent_polarity_flipping,[],[f65]) ).
fof(f101,plain,
( ~ white(sK16)
| ~ sP0 ),
inference(consistent_polarity_flipping,[],[f63]) ).
fof(f102,plain,
( ~ street(sK17)
| ~ sP0 ),
inference(consistent_polarity_flipping,[],[f60]) ).
fof(f103,plain,
( ~ barrel(sK15,sK16)
| ~ sP0 ),
inference(consistent_polarity_flipping,[],[f57]) ).
fof(f104,plain,
( ~ down(sK15,sK17)
| ~ sP0 ),
inference(consistent_polarity_flipping,[],[f56]) ).
fof(f105,plain,
! [X2,X3,X10,X0,X11,X1,X8,X18,X9,X19,X14,X4,X15,X5,X12,X13] :
( ~ seat(X0)
| furniture(X0)
| ~ front(X0)
| ~ seat(X1)
| furniture(X1)
| ~ front(X1)
| hollywood(X2)
| ~ city(X2)
| event(X3)
| chevy(X4)
| ~ car(X4)
| white(X4)
| ~ dirty(X4)
| ~ old(X4)
| street(X5)
| ~ way(X5)
| ~ lonely(X5)
| barrel(X3,X4)
| down(X3,X5)
| ~ in(X3,X2)
| X8 = X9
| ~ fellow(X8)
| ~ man(X8)
| ~ young(X8)
| ~ fellow(X9)
| ~ man(X9)
| ~ young(X9)
| ~ in(X8,X0)
| ~ in(X9,X1)
| ~ seat(X10)
| furniture(X10)
| ~ front(X10)
| ~ seat(X11)
| furniture(X11)
| ~ front(X11)
| hollywood(X12)
| ~ city(X12)
| event(X13)
| street(X14)
| ~ way(X14)
| ~ lonely(X14)
| chevy(X15)
| ~ car(X15)
| white(X15)
| ~ dirty(X15)
| ~ old(X15)
| barrel(X13,X15)
| down(X13,X14)
| ~ in(X13,X12)
| X18 = X19
| ~ fellow(X18)
| ~ man(X18)
| ~ young(X18)
| ~ fellow(X19)
| ~ man(X19)
| ~ young(X19)
| ~ in(X18,X10)
| ~ in(X19,X11) ),
inference(consistent_polarity_flipping,[],[f82]) ).
fof(f109,definition,
( spl22_1
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl22_1])],[avatar_definition]) ).
fof(f113,definition,
( spl22_2
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl22_2])],[avatar_definition]) ).
fof(f116,plain,
( spl22_1
| spl22_2 ),
inference(avatar_split_clause,[],[f75,f113,f109]) ).
fof(f118,definition,
( spl22_3
<=> ! [X13,X14,X12,X15] :
( hollywood(X12)
| event(X13)
| ~ in(X13,X12)
| down(X13,X14)
| barrel(X13,X15)
| chevy(X15)
| ~ old(X15)
| ~ dirty(X15)
| white(X15)
| ~ car(X15)
| street(X14)
| ~ lonely(X14)
| ~ way(X14)
| ~ city(X12) ) ),
introduced(definition,[new_symbols(definition,[spl22_3])],[avatar_definition]) ).
fof(f119,plain,
( ! [X14,X15,X12,X13] :
( white(X15)
| event(X13)
| ~ in(X13,X12)
| down(X13,X14)
| barrel(X13,X15)
| chevy(X15)
| ~ old(X15)
| ~ dirty(X15)
| hollywood(X12)
| ~ car(X15)
| street(X14)
| ~ lonely(X14)
| ~ way(X14)
| ~ city(X12) )
| ~ spl22_3 ),
inference(avatar_component_clause,[],[f118]) ).
fof(f121,definition,
( spl22_4
<=> ! [X18,X11,X10,X19] :
( ~ seat(X10)
| ~ in(X19,X11)
| X18 = X19
| ~ in(X18,X10)
| ~ young(X19)
| ~ man(X19)
| ~ fellow(X19)
| ~ young(X18)
| ~ man(X18)
| ~ fellow(X18)
| ~ seat(X11)
| ~ front(X11)
| furniture(X11)
| ~ front(X10)
| furniture(X10) ) ),
introduced(definition,[new_symbols(definition,[spl22_4])],[avatar_definition]) ).
fof(f122,plain,
( ! [X10,X11,X18,X19] :
( furniture(X11)
| ~ in(X19,X11)
| X18 = X19
| ~ in(X18,X10)
| ~ young(X19)
| ~ man(X19)
| ~ fellow(X19)
| ~ young(X18)
| ~ man(X18)
| ~ fellow(X18)
| ~ seat(X11)
| ~ front(X11)
| ~ seat(X10)
| ~ front(X10)
| furniture(X10) )
| ~ spl22_4 ),
inference(avatar_component_clause,[],[f121]) ).
fof(f125,plain,
( spl22_3
| spl22_4
| spl22_3
| spl22_4 ),
inference(avatar_split_clause,[],[f105,f121,f118,f121,f118]) ).
fof(f127,definition,
( spl22_5
<=> in(sK21,sK13) ),
introduced(definition,[new_symbols(definition,[spl22_5])],[avatar_definition]) ).
fof(f129,plain,
( in(sK21,sK13)
| ~ spl22_5 ),
inference(avatar_component_clause,[],[f127]) ).
fof(f130,plain,
( ~ spl22_1
| spl22_5 ),
inference(avatar_split_clause,[],[f44,f127,f109]) ).
fof(f132,definition,
( spl22_6
<=> sK19 = sK21 ),
introduced(definition,[new_symbols(definition,[spl22_6])],[avatar_definition]) ).
fof(f134,plain,
( sK19 = sK21
| ~ spl22_6 ),
inference(avatar_component_clause,[],[f132]) ).
fof(f135,plain,
( ~ spl22_1
| spl22_6 ),
inference(avatar_split_clause,[],[f45,f132,f109]) ).
fof(f137,definition,
( spl22_7
<=> in(sK20,sK12) ),
introduced(definition,[new_symbols(definition,[spl22_7])],[avatar_definition]) ).
fof(f139,plain,
( in(sK20,sK12)
| ~ spl22_7 ),
inference(avatar_component_clause,[],[f137]) ).
fof(f140,plain,
( ~ spl22_1
| spl22_7 ),
inference(avatar_split_clause,[],[f46,f137,f109]) ).
fof(f142,definition,
( spl22_8
<=> sK18 = sK20 ),
introduced(definition,[new_symbols(definition,[spl22_8])],[avatar_definition]) ).
fof(f144,plain,
( sK18 = sK20
| ~ spl22_8 ),
inference(avatar_component_clause,[],[f142]) ).
fof(f145,plain,
( ~ spl22_1
| spl22_8 ),
inference(avatar_split_clause,[],[f47,f142,f109]) ).
fof(f147,definition,
( spl22_9
<=> young(sK19) ),
introduced(definition,[new_symbols(definition,[spl22_9])],[avatar_definition]) ).
fof(f150,plain,
( ~ spl22_1
| spl22_9 ),
inference(avatar_split_clause,[],[f48,f147,f109]) ).
fof(f152,definition,
( spl22_10
<=> man(sK19) ),
introduced(definition,[new_symbols(definition,[spl22_10])],[avatar_definition]) ).
fof(f155,plain,
( ~ spl22_1
| spl22_10 ),
inference(avatar_split_clause,[],[f49,f152,f109]) ).
fof(f157,definition,
( spl22_11
<=> fellow(sK19) ),
introduced(definition,[new_symbols(definition,[spl22_11])],[avatar_definition]) ).
fof(f160,plain,
( ~ spl22_1
| spl22_11 ),
inference(avatar_split_clause,[],[f50,f157,f109]) ).
fof(f162,definition,
( spl22_12
<=> young(sK18) ),
introduced(definition,[new_symbols(definition,[spl22_12])],[avatar_definition]) ).
fof(f165,plain,
( ~ spl22_1
| spl22_12 ),
inference(avatar_split_clause,[],[f51,f162,f109]) ).
fof(f167,definition,
( spl22_13
<=> man(sK18) ),
introduced(definition,[new_symbols(definition,[spl22_13])],[avatar_definition]) ).
fof(f170,plain,
( ~ spl22_1
| spl22_13 ),
inference(avatar_split_clause,[],[f52,f167,f109]) ).
fof(f172,definition,
( spl22_14
<=> fellow(sK18) ),
introduced(definition,[new_symbols(definition,[spl22_14])],[avatar_definition]) ).
fof(f175,plain,
( ~ spl22_1
| spl22_14 ),
inference(avatar_split_clause,[],[f53,f172,f109]) ).
fof(f177,definition,
( spl22_15
<=> sK18 = sK19 ),
introduced(definition,[new_symbols(definition,[spl22_15])],[avatar_definition]) ).
fof(f180,plain,
( ~ spl22_1
| ~ spl22_15 ),
inference(avatar_split_clause,[],[f54,f177,f109]) ).
fof(f182,definition,
( spl22_16
<=> in(sK15,sK14) ),
introduced(definition,[new_symbols(definition,[spl22_16])],[avatar_definition]) ).
fof(f184,plain,
( in(sK15,sK14)
| ~ spl22_16 ),
inference(avatar_component_clause,[],[f182]) ).
fof(f185,plain,
( ~ spl22_1
| spl22_16 ),
inference(avatar_split_clause,[],[f55,f182,f109]) ).
fof(f187,definition,
( spl22_17
<=> down(sK15,sK17) ),
introduced(definition,[new_symbols(definition,[spl22_17])],[avatar_definition]) ).
fof(f189,plain,
( ~ down(sK15,sK17)
| spl22_17 ),
inference(avatar_component_clause,[],[f187]) ).
fof(f190,plain,
( ~ spl22_1
| ~ spl22_17 ),
inference(avatar_split_clause,[],[f104,f187,f109]) ).
fof(f192,definition,
( spl22_18
<=> barrel(sK15,sK16) ),
introduced(definition,[new_symbols(definition,[spl22_18])],[avatar_definition]) ).
fof(f194,plain,
( ~ barrel(sK15,sK16)
| spl22_18 ),
inference(avatar_component_clause,[],[f192]) ).
fof(f195,plain,
( ~ spl22_1
| ~ spl22_18 ),
inference(avatar_split_clause,[],[f103,f192,f109]) ).
fof(f197,definition,
( spl22_19
<=> lonely(sK17) ),
introduced(definition,[new_symbols(definition,[spl22_19])],[avatar_definition]) ).
fof(f200,plain,
( ~ spl22_1
| spl22_19 ),
inference(avatar_split_clause,[],[f58,f197,f109]) ).
fof(f202,definition,
( spl22_20
<=> way(sK17) ),
introduced(definition,[new_symbols(definition,[spl22_20])],[avatar_definition]) ).
fof(f205,plain,
( ~ spl22_1
| spl22_20 ),
inference(avatar_split_clause,[],[f59,f202,f109]) ).
fof(f207,definition,
( spl22_21
<=> street(sK17) ),
introduced(definition,[new_symbols(definition,[spl22_21])],[avatar_definition]) ).
fof(f210,plain,
( ~ spl22_1
| ~ spl22_21 ),
inference(avatar_split_clause,[],[f102,f207,f109]) ).
fof(f212,definition,
( spl22_22
<=> old(sK16) ),
introduced(definition,[new_symbols(definition,[spl22_22])],[avatar_definition]) ).
fof(f215,plain,
( ~ spl22_1
| spl22_22 ),
inference(avatar_split_clause,[],[f61,f212,f109]) ).
fof(f217,definition,
( spl22_23
<=> dirty(sK16) ),
introduced(definition,[new_symbols(definition,[spl22_23])],[avatar_definition]) ).
fof(f220,plain,
( ~ spl22_1
| spl22_23 ),
inference(avatar_split_clause,[],[f62,f217,f109]) ).
fof(f222,definition,
( spl22_24
<=> white(sK16) ),
introduced(definition,[new_symbols(definition,[spl22_24])],[avatar_definition]) ).
fof(f224,plain,
( ~ white(sK16)
| spl22_24 ),
inference(avatar_component_clause,[],[f222]) ).
fof(f225,plain,
( ~ spl22_1
| ~ spl22_24 ),
inference(avatar_split_clause,[],[f101,f222,f109]) ).
fof(f227,definition,
( spl22_25
<=> car(sK16) ),
introduced(definition,[new_symbols(definition,[spl22_25])],[avatar_definition]) ).
fof(f230,plain,
( ~ spl22_1
| spl22_25 ),
inference(avatar_split_clause,[],[f64,f227,f109]) ).
fof(f232,definition,
( spl22_26
<=> chevy(sK16) ),
introduced(definition,[new_symbols(definition,[spl22_26])],[avatar_definition]) ).
fof(f235,plain,
( ~ spl22_1
| ~ spl22_26 ),
inference(avatar_split_clause,[],[f100,f232,f109]) ).
fof(f237,definition,
( spl22_27
<=> event(sK15) ),
introduced(definition,[new_symbols(definition,[spl22_27])],[avatar_definition]) ).
fof(f240,plain,
( ~ spl22_1
| ~ spl22_27 ),
inference(avatar_split_clause,[],[f99,f237,f109]) ).
fof(f242,definition,
( spl22_28
<=> city(sK14) ),
introduced(definition,[new_symbols(definition,[spl22_28])],[avatar_definition]) ).
fof(f245,plain,
( ~ spl22_1
| spl22_28 ),
inference(avatar_split_clause,[],[f67,f242,f109]) ).
fof(f247,definition,
( spl22_29
<=> hollywood(sK14) ),
introduced(definition,[new_symbols(definition,[spl22_29])],[avatar_definition]) ).
fof(f250,plain,
( ~ spl22_1
| ~ spl22_29 ),
inference(avatar_split_clause,[],[f98,f247,f109]) ).
fof(f252,definition,
( spl22_30
<=> front(sK13) ),
introduced(definition,[new_symbols(definition,[spl22_30])],[avatar_definition]) ).
fof(f255,plain,
( ~ spl22_1
| spl22_30 ),
inference(avatar_split_clause,[],[f69,f252,f109]) ).
fof(f257,definition,
( spl22_31
<=> furniture(sK13) ),
introduced(definition,[new_symbols(definition,[spl22_31])],[avatar_definition]) ).
fof(f259,plain,
( ~ furniture(sK13)
| spl22_31 ),
inference(avatar_component_clause,[],[f257]) ).
fof(f260,plain,
( ~ spl22_1
| ~ spl22_31 ),
inference(avatar_split_clause,[],[f97,f257,f109]) ).
fof(f262,definition,
( spl22_32
<=> seat(sK13) ),
introduced(definition,[new_symbols(definition,[spl22_32])],[avatar_definition]) ).
fof(f265,plain,
( ~ spl22_1
| spl22_32 ),
inference(avatar_split_clause,[],[f71,f262,f109]) ).
fof(f267,definition,
( spl22_33
<=> front(sK12) ),
introduced(definition,[new_symbols(definition,[spl22_33])],[avatar_definition]) ).
fof(f270,plain,
( ~ spl22_1
| spl22_33 ),
inference(avatar_split_clause,[],[f72,f267,f109]) ).
fof(f272,definition,
( spl22_34
<=> furniture(sK12) ),
introduced(definition,[new_symbols(definition,[spl22_34])],[avatar_definition]) ).
fof(f274,plain,
( ~ furniture(sK12)
| spl22_34 ),
inference(avatar_component_clause,[],[f272]) ).
fof(f275,plain,
( ~ spl22_1
| ~ spl22_34 ),
inference(avatar_split_clause,[],[f96,f272,f109]) ).
fof(f277,definition,
( spl22_35
<=> seat(sK12) ),
introduced(definition,[new_symbols(definition,[spl22_35])],[avatar_definition]) ).
fof(f280,plain,
( ~ spl22_1
| spl22_35 ),
inference(avatar_split_clause,[],[f74,f277,f109]) ).
fof(f282,definition,
( spl22_36
<=> in(sK11,sK3) ),
introduced(definition,[new_symbols(definition,[spl22_36])],[avatar_definition]) ).
fof(f284,plain,
( in(sK11,sK3)
| ~ spl22_36 ),
inference(avatar_component_clause,[],[f282]) ).
fof(f285,plain,
( ~ spl22_2
| spl22_36 ),
inference(avatar_split_clause,[],[f13,f282,f113]) ).
fof(f287,definition,
( spl22_37
<=> sK9 = sK11 ),
introduced(definition,[new_symbols(definition,[spl22_37])],[avatar_definition]) ).
fof(f289,plain,
( sK9 = sK11
| ~ spl22_37 ),
inference(avatar_component_clause,[],[f287]) ).
fof(f290,plain,
( ~ spl22_2
| spl22_37 ),
inference(avatar_split_clause,[],[f14,f287,f113]) ).
fof(f292,definition,
( spl22_38
<=> in(sK10,sK2) ),
introduced(definition,[new_symbols(definition,[spl22_38])],[avatar_definition]) ).
fof(f294,plain,
( in(sK10,sK2)
| ~ spl22_38 ),
inference(avatar_component_clause,[],[f292]) ).
fof(f295,plain,
( ~ spl22_2
| spl22_38 ),
inference(avatar_split_clause,[],[f15,f292,f113]) ).
fof(f297,definition,
( spl22_39
<=> sK8 = sK10 ),
introduced(definition,[new_symbols(definition,[spl22_39])],[avatar_definition]) ).
fof(f299,plain,
( sK8 = sK10
| ~ spl22_39 ),
inference(avatar_component_clause,[],[f297]) ).
fof(f300,plain,
( ~ spl22_2
| spl22_39 ),
inference(avatar_split_clause,[],[f16,f297,f113]) ).
fof(f302,definition,
( spl22_40
<=> young(sK9) ),
introduced(definition,[new_symbols(definition,[spl22_40])],[avatar_definition]) ).
fof(f305,plain,
( ~ spl22_2
| spl22_40 ),
inference(avatar_split_clause,[],[f17,f302,f113]) ).
fof(f307,definition,
( spl22_41
<=> man(sK9) ),
introduced(definition,[new_symbols(definition,[spl22_41])],[avatar_definition]) ).
fof(f310,plain,
( ~ spl22_2
| spl22_41 ),
inference(avatar_split_clause,[],[f18,f307,f113]) ).
fof(f312,definition,
( spl22_42
<=> fellow(sK9) ),
introduced(definition,[new_symbols(definition,[spl22_42])],[avatar_definition]) ).
fof(f315,plain,
( ~ spl22_2
| spl22_42 ),
inference(avatar_split_clause,[],[f19,f312,f113]) ).
fof(f317,definition,
( spl22_43
<=> young(sK8) ),
introduced(definition,[new_symbols(definition,[spl22_43])],[avatar_definition]) ).
fof(f320,plain,
( ~ spl22_2
| spl22_43 ),
inference(avatar_split_clause,[],[f20,f317,f113]) ).
fof(f322,definition,
( spl22_44
<=> man(sK8) ),
introduced(definition,[new_symbols(definition,[spl22_44])],[avatar_definition]) ).
fof(f325,plain,
( ~ spl22_2
| spl22_44 ),
inference(avatar_split_clause,[],[f21,f322,f113]) ).
fof(f327,definition,
( spl22_45
<=> fellow(sK8) ),
introduced(definition,[new_symbols(definition,[spl22_45])],[avatar_definition]) ).
fof(f330,plain,
( ~ spl22_2
| spl22_45 ),
inference(avatar_split_clause,[],[f22,f327,f113]) ).
fof(f332,definition,
( spl22_46
<=> sK8 = sK9 ),
introduced(definition,[new_symbols(definition,[spl22_46])],[avatar_definition]) ).
fof(f335,plain,
( ~ spl22_2
| ~ spl22_46 ),
inference(avatar_split_clause,[],[f23,f332,f113]) ).
fof(f337,definition,
( spl22_47
<=> in(sK5,sK4) ),
introduced(definition,[new_symbols(definition,[spl22_47])],[avatar_definition]) ).
fof(f339,plain,
( in(sK5,sK4)
| ~ spl22_47 ),
inference(avatar_component_clause,[],[f337]) ).
fof(f340,plain,
( ~ spl22_2
| spl22_47 ),
inference(avatar_split_clause,[],[f24,f337,f113]) ).
fof(f342,definition,
( spl22_48
<=> down(sK5,sK6) ),
introduced(definition,[new_symbols(definition,[spl22_48])],[avatar_definition]) ).
fof(f344,plain,
( ~ down(sK5,sK6)
| spl22_48 ),
inference(avatar_component_clause,[],[f342]) ).
fof(f345,plain,
( ~ spl22_2
| ~ spl22_48 ),
inference(avatar_split_clause,[],[f95,f342,f113]) ).
fof(f347,definition,
( spl22_49
<=> barrel(sK5,sK7) ),
introduced(definition,[new_symbols(definition,[spl22_49])],[avatar_definition]) ).
fof(f349,plain,
( ~ barrel(sK5,sK7)
| spl22_49 ),
inference(avatar_component_clause,[],[f347]) ).
fof(f350,plain,
( ~ spl22_2
| ~ spl22_49 ),
inference(avatar_split_clause,[],[f94,f347,f113]) ).
fof(f352,definition,
( spl22_50
<=> old(sK7) ),
introduced(definition,[new_symbols(definition,[spl22_50])],[avatar_definition]) ).
fof(f355,plain,
( ~ spl22_2
| spl22_50 ),
inference(avatar_split_clause,[],[f27,f352,f113]) ).
fof(f357,definition,
( spl22_51
<=> dirty(sK7) ),
introduced(definition,[new_symbols(definition,[spl22_51])],[avatar_definition]) ).
fof(f360,plain,
( ~ spl22_2
| spl22_51 ),
inference(avatar_split_clause,[],[f28,f357,f113]) ).
fof(f362,definition,
( spl22_52
<=> white(sK7) ),
introduced(definition,[new_symbols(definition,[spl22_52])],[avatar_definition]) ).
fof(f364,plain,
( ~ white(sK7)
| spl22_52 ),
inference(avatar_component_clause,[],[f362]) ).
fof(f365,plain,
( ~ spl22_2
| ~ spl22_52 ),
inference(avatar_split_clause,[],[f93,f362,f113]) ).
fof(f367,definition,
( spl22_53
<=> car(sK7) ),
introduced(definition,[new_symbols(definition,[spl22_53])],[avatar_definition]) ).
fof(f370,plain,
( ~ spl22_2
| spl22_53 ),
inference(avatar_split_clause,[],[f30,f367,f113]) ).
fof(f372,definition,
( spl22_54
<=> chevy(sK7) ),
introduced(definition,[new_symbols(definition,[spl22_54])],[avatar_definition]) ).
fof(f375,plain,
( ~ spl22_2
| ~ spl22_54 ),
inference(avatar_split_clause,[],[f92,f372,f113]) ).
fof(f377,definition,
( spl22_55
<=> lonely(sK6) ),
introduced(definition,[new_symbols(definition,[spl22_55])],[avatar_definition]) ).
fof(f380,plain,
( ~ spl22_2
| spl22_55 ),
inference(avatar_split_clause,[],[f32,f377,f113]) ).
fof(f382,definition,
( spl22_56
<=> way(sK6) ),
introduced(definition,[new_symbols(definition,[spl22_56])],[avatar_definition]) ).
fof(f385,plain,
( ~ spl22_2
| spl22_56 ),
inference(avatar_split_clause,[],[f33,f382,f113]) ).
fof(f387,definition,
( spl22_57
<=> street(sK6) ),
introduced(definition,[new_symbols(definition,[spl22_57])],[avatar_definition]) ).
fof(f390,plain,
( ~ spl22_2
| ~ spl22_57 ),
inference(avatar_split_clause,[],[f91,f387,f113]) ).
fof(f392,definition,
( spl22_58
<=> event(sK5) ),
introduced(definition,[new_symbols(definition,[spl22_58])],[avatar_definition]) ).
fof(f395,plain,
( ~ spl22_2
| ~ spl22_58 ),
inference(avatar_split_clause,[],[f90,f392,f113]) ).
fof(f397,definition,
( spl22_59
<=> city(sK4) ),
introduced(definition,[new_symbols(definition,[spl22_59])],[avatar_definition]) ).
fof(f400,plain,
( ~ spl22_2
| spl22_59 ),
inference(avatar_split_clause,[],[f36,f397,f113]) ).
fof(f402,definition,
( spl22_60
<=> hollywood(sK4) ),
introduced(definition,[new_symbols(definition,[spl22_60])],[avatar_definition]) ).
fof(f405,plain,
( ~ spl22_2
| ~ spl22_60 ),
inference(avatar_split_clause,[],[f89,f402,f113]) ).
fof(f407,definition,
( spl22_61
<=> front(sK3) ),
introduced(definition,[new_symbols(definition,[spl22_61])],[avatar_definition]) ).
fof(f410,plain,
( ~ spl22_2
| spl22_61 ),
inference(avatar_split_clause,[],[f38,f407,f113]) ).
fof(f412,definition,
( spl22_62
<=> furniture(sK3) ),
introduced(definition,[new_symbols(definition,[spl22_62])],[avatar_definition]) ).
fof(f414,plain,
( ~ furniture(sK3)
| spl22_62 ),
inference(avatar_component_clause,[],[f412]) ).
fof(f415,plain,
( ~ spl22_2
| ~ spl22_62 ),
inference(avatar_split_clause,[],[f88,f412,f113]) ).
fof(f417,definition,
( spl22_63
<=> seat(sK3) ),
introduced(definition,[new_symbols(definition,[spl22_63])],[avatar_definition]) ).
fof(f420,plain,
( ~ spl22_2
| spl22_63 ),
inference(avatar_split_clause,[],[f40,f417,f113]) ).
fof(f422,definition,
( spl22_64
<=> front(sK2) ),
introduced(definition,[new_symbols(definition,[spl22_64])],[avatar_definition]) ).
fof(f425,plain,
( ~ spl22_2
| spl22_64 ),
inference(avatar_split_clause,[],[f41,f422,f113]) ).
fof(f427,definition,
( spl22_65
<=> furniture(sK2) ),
introduced(definition,[new_symbols(definition,[spl22_65])],[avatar_definition]) ).
fof(f429,plain,
( ~ furniture(sK2)
| spl22_65 ),
inference(avatar_component_clause,[],[f427]) ).
fof(f430,plain,
( ~ spl22_2
| ~ spl22_65 ),
inference(avatar_split_clause,[],[f87,f427,f113]) ).
fof(f432,definition,
( spl22_66
<=> seat(sK2) ),
introduced(definition,[new_symbols(definition,[spl22_66])],[avatar_definition]) ).
fof(f435,plain,
( ~ spl22_2
| spl22_66 ),
inference(avatar_split_clause,[],[f43,f432,f113]) ).
fof(f436,plain,
( ! [X2,X0,X1] :
( event(X0)
| ~ in(X0,X1)
| down(X0,X2)
| barrel(X0,sK16)
| chevy(sK16)
| ~ old(sK16)
| ~ dirty(sK16)
| hollywood(X1)
| ~ car(sK16)
| street(X2)
| ~ lonely(X2)
| ~ way(X2)
| ~ city(X1) )
| ~ spl22_3
| spl22_24 ),
inference(resolution,[],[f119,f224]) ).
fof(f437,plain,
( ! [X2,X0,X1] :
( event(X0)
| ~ in(X0,X1)
| down(X0,X2)
| barrel(X0,sK7)
| chevy(sK7)
| ~ old(sK7)
| ~ dirty(sK7)
| hollywood(X1)
| ~ car(sK7)
| street(X2)
| ~ lonely(X2)
| ~ way(X2)
| ~ city(X1) )
| ~ spl22_3
| spl22_52 ),
inference(resolution,[],[f119,f364]) ).
fof(f439,definition,
( spl22_67
<=> ! [X2,X0,X1] :
( event(X0)
| ~ city(X1)
| ~ way(X2)
| ~ lonely(X2)
| street(X2)
| hollywood(X1)
| barrel(X0,sK7)
| down(X0,X2)
| ~ in(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl22_67])],[avatar_definition]) ).
fof(f440,plain,
( ! [X2,X0,X1] :
( barrel(X0,sK7)
| ~ city(X1)
| ~ way(X2)
| ~ lonely(X2)
| street(X2)
| hollywood(X1)
| event(X0)
| down(X0,X2)
| ~ in(X0,X1) )
| ~ spl22_67 ),
inference(avatar_component_clause,[],[f439]) ).
fof(f443,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(f444,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,[],[f443]) ).
fof(f445,plain,
( ~ spl22_25
| ~ spl22_23
| ~ spl22_22
| spl22_26
| spl22_68
| ~ spl22_3
| spl22_24 ),
inference(avatar_split_clause,[],[f436,f222,f118,f443,f232,f212,f217,f227]) ).
fof(f448,plain,
( ! [X0,X1] :
( ~ city(X0)
| ~ way(X1)
| ~ lonely(X1)
| street(X1)
| hollywood(X0)
| event(sK15)
| down(sK15,X1)
| ~ in(sK15,X0) )
| spl22_18
| ~ spl22_68 ),
inference(resolution,[],[f194,f444]) ).
fof(f450,definition,
( spl22_69
<=> ! [X1] :
( ~ way(X1)
| down(sK15,X1)
| street(X1)
| ~ lonely(X1) ) ),
introduced(definition,[new_symbols(definition,[spl22_69])],[avatar_definition]) ).
fof(f451,plain,
( ! [X1] :
( down(sK15,X1)
| ~ way(X1)
| street(X1)
| ~ lonely(X1) )
| ~ spl22_69 ),
inference(avatar_component_clause,[],[f450]) ).
fof(f453,definition,
( spl22_70
<=> ! [X0] :
( ~ city(X0)
| ~ in(sK15,X0)
| hollywood(X0) ) ),
introduced(definition,[new_symbols(definition,[spl22_70])],[avatar_definition]) ).
fof(f454,plain,
( ! [X0] :
( ~ in(sK15,X0)
| ~ city(X0)
| hollywood(X0) )
| ~ spl22_70 ),
inference(avatar_component_clause,[],[f453]) ).
fof(f455,plain,
( spl22_27
| spl22_69
| spl22_70
| spl22_18
| ~ spl22_68 ),
inference(avatar_split_clause,[],[f448,f443,f192,f453,f450,f237]) ).
fof(f456,plain,
( ~ city(sK14)
| hollywood(sK14)
| ~ spl22_16
| ~ spl22_70 ),
inference(resolution,[],[f454,f184]) ).
fof(f457,plain,
( spl22_29
| ~ spl22_28
| ~ spl22_16
| ~ spl22_70 ),
inference(avatar_split_clause,[],[f456,f453,f182,f242,f247]) ).
fof(f458,plain,
( ~ way(sK17)
| street(sK17)
| ~ lonely(sK17)
| spl22_17
| ~ spl22_69 ),
inference(resolution,[],[f451,f189]) ).
fof(f459,plain,
( ~ spl22_19
| spl22_21
| ~ spl22_20
| spl22_17
| ~ spl22_69 ),
inference(avatar_split_clause,[],[f458,f450,f187,f202,f207,f197]) ).
fof(f460,plain,
( ~ spl22_53
| ~ spl22_51
| ~ spl22_50
| spl22_54
| spl22_67
| ~ spl22_3
| spl22_52 ),
inference(avatar_split_clause,[],[f437,f362,f118,f439,f372,f352,f357,f367]) ).
fof(f464,plain,
( ! [X0,X1] :
( ~ city(X0)
| ~ way(X1)
| ~ lonely(X1)
| street(X1)
| hollywood(X0)
| event(sK5)
| down(sK5,X1)
| ~ in(sK5,X0) )
| spl22_49
| ~ spl22_67 ),
inference(resolution,[],[f349,f440]) ).
fof(f466,definition,
( spl22_71
<=> ! [X1] :
( ~ way(X1)
| down(sK5,X1)
| street(X1)
| ~ lonely(X1) ) ),
introduced(definition,[new_symbols(definition,[spl22_71])],[avatar_definition]) ).
fof(f467,plain,
( ! [X1] :
( down(sK5,X1)
| ~ way(X1)
| street(X1)
| ~ lonely(X1) )
| ~ spl22_71 ),
inference(avatar_component_clause,[],[f466]) ).
fof(f469,definition,
( spl22_72
<=> ! [X0] :
( ~ city(X0)
| ~ in(sK5,X0)
| hollywood(X0) ) ),
introduced(definition,[new_symbols(definition,[spl22_72])],[avatar_definition]) ).
fof(f470,plain,
( ! [X0] :
( ~ in(sK5,X0)
| ~ city(X0)
| hollywood(X0) )
| ~ spl22_72 ),
inference(avatar_component_clause,[],[f469]) ).
fof(f471,plain,
( spl22_58
| spl22_71
| spl22_72
| spl22_49
| ~ spl22_67 ),
inference(avatar_split_clause,[],[f464,f439,f347,f469,f466,f392]) ).
fof(f472,plain,
( ~ city(sK4)
| hollywood(sK4)
| ~ spl22_47
| ~ spl22_72 ),
inference(resolution,[],[f470,f339]) ).
fof(f473,plain,
( spl22_60
| ~ spl22_59
| ~ spl22_47
| ~ spl22_72 ),
inference(avatar_split_clause,[],[f472,f469,f337,f397,f402]) ).
fof(f474,plain,
( ~ way(sK6)
| street(sK6)
| ~ lonely(sK6)
| spl22_48
| ~ spl22_71 ),
inference(resolution,[],[f467,f344]) ).
fof(f475,plain,
( ~ spl22_55
| spl22_57
| ~ spl22_56
| spl22_48
| ~ spl22_71 ),
inference(avatar_split_clause,[],[f474,f466,f342,f382,f387,f377]) ).
fof(f477,plain,
( ! [X2,X0,X1] :
( ~ in(X0,sK3)
| X0 = X1
| ~ in(X1,X2)
| ~ young(X0)
| ~ man(X0)
| ~ fellow(X0)
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ seat(sK3)
| ~ front(sK3)
| ~ seat(X2)
| ~ front(X2)
| furniture(X2) )
| ~ spl22_4
| spl22_62 ),
inference(resolution,[],[f122,f414]) ).
fof(f479,plain,
( ! [X2,X0,X1] :
( ~ in(X0,sK13)
| X0 = X1
| ~ in(X1,X2)
| ~ young(X0)
| ~ man(X0)
| ~ fellow(X0)
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ seat(sK13)
| ~ front(sK13)
| ~ seat(X2)
| ~ front(X2)
| furniture(X2) )
| ~ spl22_4
| spl22_31 ),
inference(resolution,[],[f122,f259]) ).
fof(f481,definition,
( spl22_73
<=> ! [X2,X0,X1] :
( ~ in(X0,sK13)
| furniture(X2)
| ~ front(X2)
| ~ seat(X2)
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ in(X1,X2)
| X0 = X1 ) ),
introduced(definition,[new_symbols(definition,[spl22_73])],[avatar_definition]) ).
fof(f482,plain,
( ! [X2,X0,X1] :
( furniture(X2)
| ~ in(X0,sK13)
| ~ front(X2)
| ~ seat(X2)
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ in(X1,X2)
| X0 = X1 )
| ~ spl22_73 ),
inference(avatar_component_clause,[],[f481]) ).
fof(f483,plain,
( ~ spl22_30
| ~ spl22_32
| spl22_73
| ~ spl22_4
| spl22_31 ),
inference(avatar_split_clause,[],[f479,f257,f121,f481,f262,f252]) ).
fof(f489,definition,
( spl22_75
<=> ! [X2,X0,X1] :
( ~ in(X0,sK3)
| furniture(X2)
| ~ front(X2)
| ~ seat(X2)
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ in(X1,X2)
| X0 = X1 ) ),
introduced(definition,[new_symbols(definition,[spl22_75])],[avatar_definition]) ).
fof(f490,plain,
( ! [X2,X0,X1] :
( furniture(X2)
| ~ in(X0,sK3)
| ~ front(X2)
| ~ seat(X2)
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ in(X1,X2)
| X0 = X1 )
| ~ spl22_75 ),
inference(avatar_component_clause,[],[f489]) ).
fof(f491,plain,
( ~ spl22_61
| ~ spl22_63
| spl22_75
| ~ spl22_4
| spl22_62 ),
inference(avatar_split_clause,[],[f477,f412,f121,f489,f417,f407]) ).
fof(f498,plain,
( ! [X0,X1] :
( ~ in(X0,sK13)
| ~ front(sK12)
| ~ seat(sK12)
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ in(X1,sK12)
| X0 = X1 )
| spl22_34
| ~ spl22_73 ),
inference(resolution,[],[f482,f274]) ).
fof(f512,plain,
( ! [X0,X1] :
( ~ in(X0,sK3)
| ~ front(sK2)
| ~ seat(sK2)
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ in(X1,sK2)
| X0 = X1 )
| spl22_65
| ~ spl22_75 ),
inference(resolution,[],[f490,f429]) ).
fof(f521,definition,
( spl22_81
<=> ! [X0,X1] :
( ~ in(X0,sK3)
| X0 = X1
| ~ young(X0)
| ~ man(X0)
| ~ fellow(X0)
| ~ fellow(X1)
| ~ in(X1,sK2)
| ~ young(X1)
| ~ man(X1) ) ),
introduced(definition,[new_symbols(definition,[spl22_81])],[avatar_definition]) ).
fof(f522,plain,
( ! [X0,X1] :
( ~ in(X1,sK2)
| ~ in(X0,sK3)
| ~ young(X0)
| ~ man(X0)
| ~ fellow(X0)
| ~ fellow(X1)
| X0 = X1
| ~ young(X1)
| ~ man(X1) )
| ~ spl22_81 ),
inference(avatar_component_clause,[],[f521]) ).
fof(f523,plain,
( ~ spl22_66
| ~ spl22_64
| spl22_81
| spl22_65
| ~ spl22_75 ),
inference(avatar_split_clause,[],[f512,f489,f427,f521,f422,f432]) ).
fof(f529,definition,
( spl22_82
<=> fellow(sK11) ),
introduced(definition,[new_symbols(definition,[spl22_82])],[avatar_definition]) ).
fof(f531,plain,
( ~ fellow(sK11)
| spl22_82 ),
inference(avatar_component_clause,[],[f529]) ).
fof(f533,definition,
( spl22_83
<=> man(sK11) ),
introduced(definition,[new_symbols(definition,[spl22_83])],[avatar_definition]) ).
fof(f535,plain,
( ~ man(sK11)
| spl22_83 ),
inference(avatar_component_clause,[],[f533]) ).
fof(f537,definition,
( spl22_84
<=> young(sK11) ),
introduced(definition,[new_symbols(definition,[spl22_84])],[avatar_definition]) ).
fof(f539,plain,
( ~ young(sK11)
| spl22_84 ),
inference(avatar_component_clause,[],[f537]) ).
fof(f545,plain,
( ~ fellow(sK9)
| ~ spl22_37
| spl22_82 ),
inference(superposition,[],[f531,f289]) ).
fof(f546,plain,
( ~ spl22_42
| ~ spl22_37
| spl22_82 ),
inference(avatar_split_clause,[],[f545,f529,f287,f312]) ).
fof(f548,plain,
( ~ man(sK9)
| ~ spl22_37
| spl22_83 ),
inference(superposition,[],[f535,f289]) ).
fof(f549,plain,
( ~ spl22_41
| ~ spl22_37
| spl22_83 ),
inference(avatar_split_clause,[],[f548,f533,f287,f307]) ).
fof(f551,plain,
( ~ young(sK9)
| ~ spl22_37
| spl22_84 ),
inference(superposition,[],[f539,f289]) ).
fof(f552,plain,
( ~ spl22_40
| ~ spl22_37
| spl22_84 ),
inference(avatar_split_clause,[],[f551,f537,f287,f302]) ).
fof(f556,plain,
( ! [X0] :
( ~ in(X0,sK2)
| ~ young(sK11)
| ~ man(sK11)
| ~ fellow(sK11)
| ~ fellow(X0)
| sK11 = X0
| ~ young(X0)
| ~ man(X0) )
| ~ spl22_36
| ~ spl22_81 ),
inference(resolution,[],[f522,f284]) ).
fof(f558,definition,
( spl22_86
<=> ! [X0] :
( ~ in(X0,sK2)
| ~ man(X0)
| ~ young(X0)
| sK11 = X0
| ~ fellow(X0) ) ),
introduced(definition,[new_symbols(definition,[spl22_86])],[avatar_definition]) ).
fof(f559,plain,
( ! [X0] :
( ~ in(X0,sK2)
| ~ man(X0)
| ~ young(X0)
| sK11 = X0
| ~ fellow(X0) )
| ~ spl22_86 ),
inference(avatar_component_clause,[],[f558]) ).
fof(f560,plain,
( ~ spl22_82
| ~ spl22_83
| ~ spl22_84
| spl22_86
| ~ spl22_36
| ~ spl22_81 ),
inference(avatar_split_clause,[],[f556,f521,f282,f558,f537,f533,f529]) ).
fof(f562,definition,
( spl22_87
<=> man(sK10) ),
introduced(definition,[new_symbols(definition,[spl22_87])],[avatar_definition]) ).
fof(f564,plain,
( ~ man(sK10)
| spl22_87 ),
inference(avatar_component_clause,[],[f562]) ).
fof(f566,definition,
( spl22_88
<=> young(sK10) ),
introduced(definition,[new_symbols(definition,[spl22_88])],[avatar_definition]) ).
fof(f568,plain,
( ~ young(sK10)
| spl22_88 ),
inference(avatar_component_clause,[],[f566]) ).
fof(f570,definition,
( spl22_89
<=> fellow(sK10) ),
introduced(definition,[new_symbols(definition,[spl22_89])],[avatar_definition]) ).
fof(f572,plain,
( ~ fellow(sK10)
| spl22_89 ),
inference(avatar_component_clause,[],[f570]) ).
fof(f577,plain,
( ~ man(sK8)
| ~ spl22_39
| spl22_87 ),
inference(superposition,[],[f564,f299]) ).
fof(f578,plain,
( ~ spl22_44
| ~ spl22_39
| spl22_87 ),
inference(avatar_split_clause,[],[f577,f562,f297,f322]) ).
fof(f580,plain,
( ~ young(sK8)
| ~ spl22_39
| spl22_88 ),
inference(superposition,[],[f568,f299]) ).
fof(f581,plain,
( ~ spl22_43
| ~ spl22_39
| spl22_88 ),
inference(avatar_split_clause,[],[f580,f566,f297,f317]) ).
fof(f583,plain,
( ~ fellow(sK8)
| ~ spl22_39
| spl22_89 ),
inference(superposition,[],[f572,f299]) ).
fof(f584,plain,
( ~ spl22_45
| ~ spl22_39
| spl22_89 ),
inference(avatar_split_clause,[],[f583,f570,f297,f327]) ).
fof(f586,plain,
( ~ man(sK10)
| ~ young(sK10)
| sK10 = sK11
| ~ fellow(sK10)
| ~ spl22_38
| ~ spl22_86 ),
inference(resolution,[],[f559,f294]) ).
fof(f588,definition,
( spl22_91
<=> sK10 = sK11 ),
introduced(definition,[new_symbols(definition,[spl22_91])],[avatar_definition]) ).
fof(f590,plain,
( sK10 = sK11
| ~ spl22_91 ),
inference(avatar_component_clause,[],[f588]) ).
fof(f591,plain,
( ~ spl22_89
| spl22_91
| ~ spl22_88
| ~ spl22_87
| ~ spl22_38
| ~ spl22_86 ),
inference(avatar_split_clause,[],[f586,f558,f292,f562,f566,f588,f570]) ).
fof(f596,plain,
( sK9 = sK10
| ~ spl22_37
| ~ spl22_91 ),
inference(superposition,[],[f289,f590]) ).
fof(f602,plain,
( sK8 = sK9
| ~ spl22_37
| ~ spl22_39
| ~ spl22_91 ),
inference(superposition,[],[f299,f596]) ).
fof(f604,plain,
( spl22_46
| ~ spl22_37
| ~ spl22_39
| ~ spl22_91 ),
inference(avatar_split_clause,[],[f602,f588,f297,f287,f332]) ).
fof(f608,definition,
( spl22_92
<=> ! [X0,X1] :
( ~ in(X0,sK13)
| X0 = X1
| ~ young(X0)
| ~ man(X0)
| ~ fellow(X0)
| ~ fellow(X1)
| ~ in(X1,sK12)
| ~ young(X1)
| ~ man(X1) ) ),
introduced(definition,[new_symbols(definition,[spl22_92])],[avatar_definition]) ).
fof(f609,plain,
( ! [X0,X1] :
( ~ in(X1,sK12)
| ~ in(X0,sK13)
| ~ young(X0)
| ~ man(X0)
| ~ fellow(X0)
| ~ fellow(X1)
| X0 = X1
| ~ young(X1)
| ~ man(X1) )
| ~ spl22_92 ),
inference(avatar_component_clause,[],[f608]) ).
fof(f610,plain,
( ~ spl22_35
| ~ spl22_33
| spl22_92
| spl22_34
| ~ spl22_73 ),
inference(avatar_split_clause,[],[f498,f481,f272,f608,f267,f277]) ).
fof(f625,definition,
( spl22_94
<=> fellow(sK21) ),
introduced(definition,[new_symbols(definition,[spl22_94])],[avatar_definition]) ).
fof(f627,plain,
( ~ fellow(sK21)
| spl22_94 ),
inference(avatar_component_clause,[],[f625]) ).
fof(f629,definition,
( spl22_95
<=> man(sK21) ),
introduced(definition,[new_symbols(definition,[spl22_95])],[avatar_definition]) ).
fof(f631,plain,
( ~ man(sK21)
| spl22_95 ),
inference(avatar_component_clause,[],[f629]) ).
fof(f633,definition,
( spl22_96
<=> young(sK21) ),
introduced(definition,[new_symbols(definition,[spl22_96])],[avatar_definition]) ).
fof(f635,plain,
( ~ young(sK21)
| spl22_96 ),
inference(avatar_component_clause,[],[f633]) ).
fof(f641,plain,
( ~ fellow(sK19)
| ~ spl22_6
| spl22_94 ),
inference(superposition,[],[f627,f134]) ).
fof(f642,plain,
( ~ spl22_11
| ~ spl22_6
| spl22_94 ),
inference(avatar_split_clause,[],[f641,f625,f132,f157]) ).
fof(f644,plain,
( ~ man(sK19)
| ~ spl22_6
| spl22_95 ),
inference(superposition,[],[f631,f134]) ).
fof(f645,plain,
( ~ spl22_10
| ~ spl22_6
| spl22_95 ),
inference(avatar_split_clause,[],[f644,f629,f132,f152]) ).
fof(f647,plain,
( ~ young(sK19)
| ~ spl22_6
| spl22_96 ),
inference(superposition,[],[f635,f134]) ).
fof(f648,plain,
( ~ spl22_9
| ~ spl22_6
| spl22_96 ),
inference(avatar_split_clause,[],[f647,f633,f132,f147]) ).
fof(f735,plain,
( ! [X0] :
( ~ in(X0,sK12)
| ~ young(sK21)
| ~ man(sK21)
| ~ fellow(sK21)
| ~ fellow(X0)
| sK21 = X0
| ~ young(X0)
| ~ man(X0) )
| ~ spl22_5
| ~ spl22_92 ),
inference(resolution,[],[f609,f129]) ).
fof(f737,definition,
( spl22_106
<=> ! [X0] :
( ~ in(X0,sK12)
| ~ man(X0)
| ~ young(X0)
| sK21 = X0
| ~ fellow(X0) ) ),
introduced(definition,[new_symbols(definition,[spl22_106])],[avatar_definition]) ).
fof(f738,plain,
( ! [X0] :
( ~ in(X0,sK12)
| ~ man(X0)
| ~ young(X0)
| sK21 = X0
| ~ fellow(X0) )
| ~ spl22_106 ),
inference(avatar_component_clause,[],[f737]) ).
fof(f739,plain,
( ~ spl22_94
| ~ spl22_95
| ~ spl22_96
| spl22_106
| ~ spl22_5
| ~ spl22_92 ),
inference(avatar_split_clause,[],[f735,f608,f127,f737,f633,f629,f625]) ).
fof(f749,definition,
( spl22_109
<=> man(sK20) ),
introduced(definition,[new_symbols(definition,[spl22_109])],[avatar_definition]) ).
fof(f751,plain,
( ~ man(sK20)
| spl22_109 ),
inference(avatar_component_clause,[],[f749]) ).
fof(f753,definition,
( spl22_110
<=> young(sK20) ),
introduced(definition,[new_symbols(definition,[spl22_110])],[avatar_definition]) ).
fof(f755,plain,
( ~ young(sK20)
| spl22_110 ),
inference(avatar_component_clause,[],[f753]) ).
fof(f757,definition,
( spl22_111
<=> fellow(sK20) ),
introduced(definition,[new_symbols(definition,[spl22_111])],[avatar_definition]) ).
fof(f759,plain,
( ~ fellow(sK20)
| spl22_111 ),
inference(avatar_component_clause,[],[f757]) ).
fof(f764,plain,
( ~ man(sK18)
| ~ spl22_8
| spl22_109 ),
inference(superposition,[],[f751,f144]) ).
fof(f765,plain,
( ~ spl22_13
| ~ spl22_8
| spl22_109 ),
inference(avatar_split_clause,[],[f764,f749,f142,f167]) ).
fof(f767,plain,
( ~ young(sK18)
| ~ spl22_8
| spl22_110 ),
inference(superposition,[],[f755,f144]) ).
fof(f768,plain,
( ~ spl22_12
| ~ spl22_8
| spl22_110 ),
inference(avatar_split_clause,[],[f767,f753,f142,f162]) ).
fof(f770,plain,
( ~ fellow(sK18)
| ~ spl22_8
| spl22_111 ),
inference(superposition,[],[f759,f144]) ).
fof(f771,plain,
( ~ spl22_14
| ~ spl22_8
| spl22_111 ),
inference(avatar_split_clause,[],[f770,f757,f142,f172]) ).
fof(f773,plain,
( ~ man(sK20)
| ~ young(sK20)
| sK20 = sK21
| ~ fellow(sK20)
| ~ spl22_7
| ~ spl22_106 ),
inference(resolution,[],[f738,f139]) ).
fof(f775,definition,
( spl22_113
<=> sK20 = sK21 ),
introduced(definition,[new_symbols(definition,[spl22_113])],[avatar_definition]) ).
fof(f777,plain,
( sK20 = sK21
| ~ spl22_113 ),
inference(avatar_component_clause,[],[f775]) ).
fof(f778,plain,
( ~ spl22_111
| spl22_113
| ~ spl22_110
| ~ spl22_109
| ~ spl22_7
| ~ spl22_106 ),
inference(avatar_split_clause,[],[f773,f737,f137,f749,f753,f775,f757]) ).
fof(f783,plain,
( sK19 = sK20
| ~ spl22_6
| ~ spl22_113 ),
inference(superposition,[],[f134,f777]) ).
fof(f812,plain,
( sK18 = sK19
| ~ spl22_6
| ~ spl22_8
| ~ spl22_113 ),
inference(superposition,[],[f144,f783]) ).
fof(f817,plain,
( spl22_15
| ~ spl22_6
| ~ spl22_8
| ~ spl22_113 ),
inference(avatar_split_clause,[],[f812,f775,f142,f132,f177]) ).
cnf(s1,plain,
( spl22_1
| spl22_2 ),
inference(sat_conversion,[],[f116]) ).
cnf(s4,plain,
( spl22_3
| spl22_4
| spl22_3
| spl22_4 ),
inference(sat_conversion,[],[f125]) ).
cnf(s5,plain,
( spl22_3
| spl22_4 ),
inference(rat,[],[s4]) ).
cnf(s6,plain,
( ~ spl22_1
| spl22_5 ),
inference(sat_conversion,[],[f130]) ).
cnf(s7,plain,
( ~ spl22_1
| spl22_6 ),
inference(sat_conversion,[],[f135]) ).
cnf(s8,plain,
( ~ spl22_1
| spl22_7 ),
inference(sat_conversion,[],[f140]) ).
cnf(s9,plain,
( ~ spl22_1
| spl22_8 ),
inference(sat_conversion,[],[f145]) ).
cnf(s10,plain,
( ~ spl22_1
| spl22_9 ),
inference(sat_conversion,[],[f150]) ).
cnf(s11,plain,
( ~ spl22_1
| spl22_10 ),
inference(sat_conversion,[],[f155]) ).
cnf(s12,plain,
( ~ spl22_1
| spl22_11 ),
inference(sat_conversion,[],[f160]) ).
cnf(s13,plain,
( ~ spl22_1
| spl22_12 ),
inference(sat_conversion,[],[f165]) ).
cnf(s14,plain,
( ~ spl22_1
| spl22_13 ),
inference(sat_conversion,[],[f170]) ).
cnf(s15,plain,
( ~ spl22_1
| spl22_14 ),
inference(sat_conversion,[],[f175]) ).
cnf(s16,plain,
( ~ spl22_1
| ~ spl22_15 ),
inference(sat_conversion,[],[f180]) ).
cnf(s17,plain,
( ~ spl22_1
| spl22_16 ),
inference(sat_conversion,[],[f185]) ).
cnf(s18,plain,
( ~ spl22_1
| ~ spl22_17 ),
inference(sat_conversion,[],[f190]) ).
cnf(s19,plain,
( ~ spl22_1
| ~ spl22_18 ),
inference(sat_conversion,[],[f195]) ).
cnf(s20,plain,
( ~ spl22_1
| spl22_19 ),
inference(sat_conversion,[],[f200]) ).
cnf(s21,plain,
( ~ spl22_1
| spl22_20 ),
inference(sat_conversion,[],[f205]) ).
cnf(s22,plain,
( ~ spl22_1
| ~ spl22_21 ),
inference(sat_conversion,[],[f210]) ).
cnf(s23,plain,
( ~ spl22_1
| spl22_22 ),
inference(sat_conversion,[],[f215]) ).
cnf(s24,plain,
( ~ spl22_1
| spl22_23 ),
inference(sat_conversion,[],[f220]) ).
cnf(s25,plain,
( ~ spl22_1
| ~ spl22_24 ),
inference(sat_conversion,[],[f225]) ).
cnf(s26,plain,
( ~ spl22_1
| spl22_25 ),
inference(sat_conversion,[],[f230]) ).
cnf(s27,plain,
( ~ spl22_1
| ~ spl22_26 ),
inference(sat_conversion,[],[f235]) ).
cnf(s28,plain,
( ~ spl22_1
| ~ spl22_27 ),
inference(sat_conversion,[],[f240]) ).
cnf(s29,plain,
( ~ spl22_1
| spl22_28 ),
inference(sat_conversion,[],[f245]) ).
cnf(s30,plain,
( ~ spl22_1
| ~ spl22_29 ),
inference(sat_conversion,[],[f250]) ).
cnf(s31,plain,
( ~ spl22_1
| spl22_30 ),
inference(sat_conversion,[],[f255]) ).
cnf(s32,plain,
( ~ spl22_1
| ~ spl22_31 ),
inference(sat_conversion,[],[f260]) ).
cnf(s33,plain,
( ~ spl22_1
| spl22_32 ),
inference(sat_conversion,[],[f265]) ).
cnf(s34,plain,
( ~ spl22_1
| spl22_33 ),
inference(sat_conversion,[],[f270]) ).
cnf(s35,plain,
( ~ spl22_1
| ~ spl22_34 ),
inference(sat_conversion,[],[f275]) ).
cnf(s36,plain,
( ~ spl22_1
| spl22_35 ),
inference(sat_conversion,[],[f280]) ).
cnf(s37,plain,
( ~ spl22_2
| spl22_36 ),
inference(sat_conversion,[],[f285]) ).
cnf(s38,plain,
( ~ spl22_2
| spl22_37 ),
inference(sat_conversion,[],[f290]) ).
cnf(s39,plain,
( ~ spl22_2
| spl22_38 ),
inference(sat_conversion,[],[f295]) ).
cnf(s40,plain,
( ~ spl22_2
| spl22_39 ),
inference(sat_conversion,[],[f300]) ).
cnf(s41,plain,
( ~ spl22_2
| spl22_40 ),
inference(sat_conversion,[],[f305]) ).
cnf(s42,plain,
( ~ spl22_2
| spl22_41 ),
inference(sat_conversion,[],[f310]) ).
cnf(s43,plain,
( ~ spl22_2
| spl22_42 ),
inference(sat_conversion,[],[f315]) ).
cnf(s44,plain,
( ~ spl22_2
| spl22_43 ),
inference(sat_conversion,[],[f320]) ).
cnf(s45,plain,
( ~ spl22_2
| spl22_44 ),
inference(sat_conversion,[],[f325]) ).
cnf(s46,plain,
( ~ spl22_2
| spl22_45 ),
inference(sat_conversion,[],[f330]) ).
cnf(s47,plain,
( ~ spl22_2
| ~ spl22_46 ),
inference(sat_conversion,[],[f335]) ).
cnf(s48,plain,
( ~ spl22_2
| spl22_47 ),
inference(sat_conversion,[],[f340]) ).
cnf(s49,plain,
( ~ spl22_2
| ~ spl22_48 ),
inference(sat_conversion,[],[f345]) ).
cnf(s50,plain,
( ~ spl22_2
| ~ spl22_49 ),
inference(sat_conversion,[],[f350]) ).
cnf(s51,plain,
( ~ spl22_2
| spl22_50 ),
inference(sat_conversion,[],[f355]) ).
cnf(s52,plain,
( ~ spl22_2
| spl22_51 ),
inference(sat_conversion,[],[f360]) ).
cnf(s53,plain,
( ~ spl22_2
| ~ spl22_52 ),
inference(sat_conversion,[],[f365]) ).
cnf(s54,plain,
( ~ spl22_2
| spl22_53 ),
inference(sat_conversion,[],[f370]) ).
cnf(s55,plain,
( ~ spl22_2
| ~ spl22_54 ),
inference(sat_conversion,[],[f375]) ).
cnf(s56,plain,
( ~ spl22_2
| spl22_55 ),
inference(sat_conversion,[],[f380]) ).
cnf(s57,plain,
( ~ spl22_2
| spl22_56 ),
inference(sat_conversion,[],[f385]) ).
cnf(s58,plain,
( ~ spl22_2
| ~ spl22_57 ),
inference(sat_conversion,[],[f390]) ).
cnf(s59,plain,
( ~ spl22_2
| ~ spl22_58 ),
inference(sat_conversion,[],[f395]) ).
cnf(s60,plain,
( ~ spl22_2
| spl22_59 ),
inference(sat_conversion,[],[f400]) ).
cnf(s61,plain,
( ~ spl22_2
| ~ spl22_60 ),
inference(sat_conversion,[],[f405]) ).
cnf(s62,plain,
( ~ spl22_2
| spl22_61 ),
inference(sat_conversion,[],[f410]) ).
cnf(s63,plain,
( ~ spl22_2
| ~ spl22_62 ),
inference(sat_conversion,[],[f415]) ).
cnf(s64,plain,
( ~ spl22_2
| spl22_63 ),
inference(sat_conversion,[],[f420]) ).
cnf(s65,plain,
( ~ spl22_2
| spl22_64 ),
inference(sat_conversion,[],[f425]) ).
cnf(s66,plain,
( ~ spl22_2
| ~ spl22_65 ),
inference(sat_conversion,[],[f430]) ).
cnf(s67,plain,
( ~ spl22_2
| spl22_66 ),
inference(sat_conversion,[],[f435]) ).
cnf(s69,plain,
( ~ spl22_3
| ~ spl22_22
| ~ spl22_23
| spl22_24
| ~ spl22_25
| spl22_26
| spl22_68 ),
inference(sat_conversion,[],[f445]) ).
cnf(s70,plain,
( spl22_18
| spl22_27
| ~ spl22_68
| spl22_69
| spl22_70 ),
inference(sat_conversion,[],[f455]) ).
cnf(s71,plain,
( ~ spl22_16
| ~ spl22_28
| spl22_29
| ~ spl22_70 ),
inference(sat_conversion,[],[f457]) ).
cnf(s72,plain,
( spl22_17
| ~ spl22_19
| ~ spl22_20
| spl22_21
| ~ spl22_69 ),
inference(sat_conversion,[],[f459]) ).
cnf(s73,plain,
( ~ spl22_3
| ~ spl22_50
| ~ spl22_51
| spl22_52
| ~ spl22_53
| spl22_54
| spl22_67 ),
inference(sat_conversion,[],[f460]) ).
cnf(s74,plain,
( spl22_49
| spl22_58
| ~ spl22_67
| spl22_71
| spl22_72 ),
inference(sat_conversion,[],[f471]) ).
cnf(s75,plain,
( ~ spl22_47
| ~ spl22_59
| spl22_60
| ~ spl22_72 ),
inference(sat_conversion,[],[f473]) ).
cnf(s76,plain,
( spl22_48
| ~ spl22_55
| ~ spl22_56
| spl22_57
| ~ spl22_71 ),
inference(sat_conversion,[],[f475]) ).
cnf(s77,plain,
( ~ spl22_4
| ~ spl22_30
| spl22_31
| ~ spl22_32
| spl22_73 ),
inference(sat_conversion,[],[f483]) ).
cnf(s79,plain,
( ~ spl22_4
| ~ spl22_61
| spl22_62
| ~ spl22_63
| spl22_75 ),
inference(sat_conversion,[],[f491]) ).
cnf(s85,plain,
( ~ spl22_64
| spl22_65
| ~ spl22_66
| ~ spl22_75
| spl22_81 ),
inference(sat_conversion,[],[f523]) ).
cnf(s88,plain,
( ~ spl22_37
| ~ spl22_42
| spl22_82 ),
inference(sat_conversion,[],[f546]) ).
cnf(s89,plain,
( ~ spl22_37
| ~ spl22_41
| spl22_83 ),
inference(sat_conversion,[],[f549]) ).
cnf(s90,plain,
( ~ spl22_37
| ~ spl22_40
| spl22_84 ),
inference(sat_conversion,[],[f552]) ).
cnf(s91,plain,
( ~ spl22_36
| ~ spl22_81
| ~ spl22_82
| ~ spl22_83
| ~ spl22_84
| spl22_86 ),
inference(sat_conversion,[],[f560]) ).
cnf(s93,plain,
( ~ spl22_39
| ~ spl22_44
| spl22_87 ),
inference(sat_conversion,[],[f578]) ).
cnf(s94,plain,
( ~ spl22_39
| ~ spl22_43
| spl22_88 ),
inference(sat_conversion,[],[f581]) ).
cnf(s95,plain,
( ~ spl22_39
| ~ spl22_45
| spl22_89 ),
inference(sat_conversion,[],[f584]) ).
cnf(s96,plain,
( ~ spl22_38
| ~ spl22_86
| ~ spl22_87
| ~ spl22_88
| ~ spl22_89
| spl22_91 ),
inference(sat_conversion,[],[f591]) ).
cnf(s97,plain,
( ~ spl22_37
| ~ spl22_39
| spl22_46
| ~ spl22_91 ),
inference(sat_conversion,[],[f604]) ).
cnf(s101,plain,
( ~ spl22_33
| spl22_34
| ~ spl22_35
| ~ spl22_73
| spl22_92 ),
inference(sat_conversion,[],[f610]) ).
cnf(s107,plain,
( ~ spl22_6
| ~ spl22_11
| spl22_94 ),
inference(sat_conversion,[],[f642]) ).
cnf(s108,plain,
( ~ spl22_6
| ~ spl22_10
| spl22_95 ),
inference(sat_conversion,[],[f645]) ).
cnf(s109,plain,
( ~ spl22_6
| ~ spl22_9
| spl22_96 ),
inference(sat_conversion,[],[f648]) ).
cnf(s119,plain,
( ~ spl22_5
| ~ spl22_92
| ~ spl22_94
| ~ spl22_95
| ~ spl22_96
| spl22_106 ),
inference(sat_conversion,[],[f739]) ).
cnf(s123,plain,
( ~ spl22_8
| ~ spl22_13
| spl22_109 ),
inference(sat_conversion,[],[f765]) ).
cnf(s124,plain,
( ~ spl22_8
| ~ spl22_12
| spl22_110 ),
inference(sat_conversion,[],[f768]) ).
cnf(s125,plain,
( ~ spl22_8
| ~ spl22_14
| spl22_111 ),
inference(sat_conversion,[],[f771]) ).
cnf(s126,plain,
( ~ spl22_7
| ~ spl22_106
| ~ spl22_109
| ~ spl22_110
| ~ spl22_111
| spl22_113 ),
inference(sat_conversion,[],[f778]) ).
cnf(s130,plain,
( ~ spl22_6
| ~ spl22_8
| spl22_15
| ~ spl22_113 ),
inference(sat_conversion,[],[f817]) ).
cnf(s132,plain,
~ spl22_2,
inference(rat,[],[s79,s85,s5,s91,s73,s96,s74,s88,s89,s90,s97,s93,s94,s95,s75,s76,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(s133,plain,
spl22_1,
inference(rat,[],[s1,s132]) ).
cnf(s134,plain,
spl22_35,
inference(rat,[],[s36,s133]) ).
cnf(s135,plain,
~ spl22_34,
inference(rat,[],[s35,s133]) ).
cnf(s136,plain,
spl22_33,
inference(rat,[],[s34,s133]) ).
cnf(s137,plain,
spl22_32,
inference(rat,[],[s33,s133]) ).
cnf(s138,plain,
~ spl22_31,
inference(rat,[],[s32,s133]) ).
cnf(s139,plain,
spl22_30,
inference(rat,[],[s31,s133]) ).
cnf(s140,plain,
~ spl22_29,
inference(rat,[],[s30,s133]) ).
cnf(s141,plain,
spl22_28,
inference(rat,[],[s29,s133]) ).
cnf(s142,plain,
~ spl22_27,
inference(rat,[],[s28,s133]) ).
cnf(s143,plain,
~ spl22_26,
inference(rat,[],[s27,s133]) ).
cnf(s144,plain,
spl22_25,
inference(rat,[],[s26,s133]) ).
cnf(s145,plain,
~ spl22_24,
inference(rat,[],[s25,s133]) ).
cnf(s146,plain,
spl22_23,
inference(rat,[],[s24,s133]) ).
cnf(s147,plain,
spl22_22,
inference(rat,[],[s23,s133]) ).
cnf(s148,plain,
~ spl22_21,
inference(rat,[],[s22,s133]) ).
cnf(s149,plain,
spl22_20,
inference(rat,[],[s21,s133]) ).
cnf(s150,plain,
spl22_19,
inference(rat,[],[s20,s133]) ).
cnf(s151,plain,
~ spl22_18,
inference(rat,[],[s19,s133]) ).
cnf(s152,plain,
~ spl22_17,
inference(rat,[],[s18,s133]) ).
cnf(s153,plain,
spl22_16,
inference(rat,[],[s17,s133]) ).
cnf(s154,plain,
~ spl22_15,
inference(rat,[],[s16,s133]) ).
cnf(s155,plain,
spl22_14,
inference(rat,[],[s15,s133]) ).
cnf(s156,plain,
spl22_13,
inference(rat,[],[s14,s133]) ).
cnf(s157,plain,
spl22_12,
inference(rat,[],[s13,s133]) ).
cnf(s158,plain,
spl22_11,
inference(rat,[],[s12,s133]) ).
cnf(s159,plain,
spl22_10,
inference(rat,[],[s11,s133]) ).
cnf(s160,plain,
spl22_9,
inference(rat,[],[s10,s133]) ).
cnf(s161,plain,
spl22_8,
inference(rat,[],[s9,s133]) ).
cnf(s162,plain,
spl22_7,
inference(rat,[],[s8,s133]) ).
cnf(s163,plain,
spl22_6,
inference(rat,[],[s7,s133]) ).
cnf(s164,plain,
spl22_5,
inference(rat,[],[s6,s133]) ).
cnf(s165,plain,
~ spl22_69,
inference(rat,[],[s72,s150,s148,s149,s152]) ).
cnf(s166,plain,
~ spl22_70,
inference(rat,[],[s71,s141,s140,s153]) ).
cnf(s167,plain,
spl22_111,
inference(rat,[],[s125,s155,s161]) ).
cnf(s168,plain,
spl22_110,
inference(rat,[],[s124,s157,s161]) ).
cnf(s169,plain,
spl22_109,
inference(rat,[],[s123,s156,s161]) ).
cnf(s170,plain,
~ spl22_113,
inference(rat,[],[s130,s161,s154,s163]) ).
cnf(s171,plain,
spl22_96,
inference(rat,[],[s109,s160,s163]) ).
cnf(s172,plain,
spl22_95,
inference(rat,[],[s108,s159,s163]) ).
cnf(s173,plain,
spl22_94,
inference(rat,[],[s107,s158,s163]) ).
cnf(s174,plain,
~ spl22_68,
inference(rat,[],[s70,s166,s151,s142,s165]) ).
cnf(s175,plain,
~ spl22_106,
inference(rat,[],[s126,s162,s167,s168,s169,s170]) ).
cnf(s176,plain,
~ spl22_3,
inference(rat,[],[s69,s147,s143,s144,s145,s146,s174]) ).
cnf(s177,plain,
~ spl22_92,
inference(rat,[],[s119,s164,s171,s172,s173,s175]) ).
cnf(s178,plain,
spl22_4,
inference(rat,[],[s5,s176]) ).
cnf(s179,plain,
~ spl22_73,
inference(rat,[],[s101,s136,s135,s134,s177]) ).
cnf(s181,plain,
$false,
inference(rat,[],[s77,s139,s137,s138,s179,s178]) ).
fof(f818,plain,
$false,
inference(avatar_sat_refutation,[],[s181]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP004+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.12/0.41 % Computer : n017.cluster.edu
% 0.12/0.41 % Model : x86_64 x86_64
% 0.12/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.41 % Memory : 8046.5625MB
% 0.12/0.41 % OS : Linux 6.8.0-71-generic
% 0.12/0.41 % CPULimit : 300
% 0.12/0.41 % WCLimit : 300
% 0.12/0.41 % DateTime : Sun Sep 27 17:41:50 UTC 2026
% 0.12/0.41 % CPUTime :
% 0.12/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.45 Running first-order model finding
% 0.12/0.45 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.20/0.49 % (2832861)Will run a generic schedule for satisfiability detection.
% 0.20/0.49 % (2832872)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2151419046:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.20/0.49 % (2832867)% WARNING: option uhcvi not known.
% 0.20/0.49 % (2832872) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2832861-2832872"...
% 0.20/0.49 % (2832868)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2454933705:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.20/0.49 % (2832866)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2959304665_2999 on theBenchmark for (2999ds/0Mi)
% 0.20/0.49 % (2832870)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3255598615:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.20/0.49 % (2832867)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2657023596:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.20/0.49 % (2832869)dis+10_1_sil=32000:sp=arity:random_seed=3832907114:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.20/0.49 % (2832871)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2064881068:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.20/0.49 % (2832872)...printing done.
% 0.20/0.49 % (2832872)Refutation found. Thanks to Tanya!
% 0.20/0.49 % SZS status Theorem for theBenchmark
% 0.20/0.49 % SZS output start Proof for theBenchmark
% See solution above
% 0.20/0.50 % (2832872)------------------------------
% 0.20/0.50 % (2832872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.50 % (2832872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.50 % (2832872)CaDiCaL version: 2.1.3
% 0.20/0.50 % (2832872)Termination reason: Refutation
% 0.20/0.50 % (2832872)Time elapsed: 0.016 s
% 0.20/0.50 % (2832872)Peak memory usage: 13 MB
% 0.20/0.50 % (2832872)Instructions burned: 25 (million)
% 0.20/0.50 % (2832861)Success in time 0.037 s
% 0.20/0.50 % Vampire exiting
%------------------------------------------------------------------------------