%------------------------------------------------------------------------------
% File : Vampire---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 THM
% Computer : n002.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:06:38 PM UTC 2026
% Result : Theorem 2.77s 1.30s
% Output : Refutation 3.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 80
% Syntax : Number of formulae : 479 ( 43 unt; 79 def)
% Number of atoms : 2515 ( 130 equ)
% Maximal formula atoms : 124 ( 5 avg)
% Number of connectives : 3537 (1501 ~;1437 |; 518 &)
% ( 77 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 83 ( 6 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 101 ( 99 usr; 80 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)
& 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(f88,definition,
( spl22_1
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl22_1])],[avatar_definition]) ).
fof(f92,definition,
( spl22_2
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl22_2])],[avatar_definition]) ).
fof(f95,plain,
( spl22_1
| spl22_2 ),
inference(avatar_split_clause,[],[f75,f92,f88]) ).
fof(f97,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(f98,plain,
( ! [X14,X15,X12,X13] :
( ~ old(X15)
| ~ event(X13)
| ~ in(X13,X12)
| ~ down(X13,X14)
| ~ barrel(X13,X15)
| ~ chevy(X15)
| ~ hollywood(X12)
| ~ dirty(X15)
| ~ white(X15)
| ~ car(X15)
| ~ street(X14)
| ~ lonely(X14)
| ~ way(X14)
| ~ city(X12) )
| ~ spl22_3 ),
inference(avatar_component_clause,[],[f97]) ).
fof(f100,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(f101,plain,
( ! [X10,X11,X18,X19] :
( ~ young(X19)
| ~ in(X19,X11)
| X18 = X19
| ~ in(X18,X10)
| ~ seat(X10)
| ~ man(X19)
| ~ fellow(X19)
| ~ young(X18)
| ~ man(X18)
| ~ fellow(X18)
| ~ seat(X11)
| ~ front(X11)
| ~ furniture(X11)
| ~ front(X10)
| ~ furniture(X10) )
| ~ spl22_4 ),
inference(avatar_component_clause,[],[f100]) ).
fof(f104,plain,
( spl22_3
| spl22_4
| spl22_3
| spl22_4 ),
inference(avatar_split_clause,[],[f82,f100,f97,f100,f97]) ).
fof(f106,definition,
( spl22_5
<=> in(sK21,sK13) ),
introduced(definition,[new_symbols(definition,[spl22_5])],[avatar_definition]) ).
fof(f108,plain,
( in(sK21,sK13)
| ~ spl22_5 ),
inference(avatar_component_clause,[],[f106]) ).
fof(f109,plain,
( ~ spl22_1
| spl22_5 ),
inference(avatar_split_clause,[],[f44,f106,f88]) ).
fof(f111,definition,
( spl22_6
<=> sK19 = sK21 ),
introduced(definition,[new_symbols(definition,[spl22_6])],[avatar_definition]) ).
fof(f113,plain,
( sK19 = sK21
| ~ spl22_6 ),
inference(avatar_component_clause,[],[f111]) ).
fof(f114,plain,
( ~ spl22_1
| spl22_6 ),
inference(avatar_split_clause,[],[f45,f111,f88]) ).
fof(f116,definition,
( spl22_7
<=> in(sK20,sK12) ),
introduced(definition,[new_symbols(definition,[spl22_7])],[avatar_definition]) ).
fof(f118,plain,
( in(sK20,sK12)
| ~ spl22_7 ),
inference(avatar_component_clause,[],[f116]) ).
fof(f119,plain,
( ~ spl22_1
| spl22_7 ),
inference(avatar_split_clause,[],[f46,f116,f88]) ).
fof(f121,definition,
( spl22_8
<=> sK18 = sK20 ),
introduced(definition,[new_symbols(definition,[spl22_8])],[avatar_definition]) ).
fof(f123,plain,
( sK18 = sK20
| ~ spl22_8 ),
inference(avatar_component_clause,[],[f121]) ).
fof(f124,plain,
( ~ spl22_1
| spl22_8 ),
inference(avatar_split_clause,[],[f47,f121,f88]) ).
fof(f126,definition,
( spl22_9
<=> young(sK19) ),
introduced(definition,[new_symbols(definition,[spl22_9])],[avatar_definition]) ).
fof(f128,plain,
( young(sK19)
| ~ spl22_9 ),
inference(avatar_component_clause,[],[f126]) ).
fof(f129,plain,
( ~ spl22_1
| spl22_9 ),
inference(avatar_split_clause,[],[f48,f126,f88]) ).
fof(f131,definition,
( spl22_10
<=> man(sK19) ),
introduced(definition,[new_symbols(definition,[spl22_10])],[avatar_definition]) ).
fof(f133,plain,
( man(sK19)
| ~ spl22_10 ),
inference(avatar_component_clause,[],[f131]) ).
fof(f134,plain,
( ~ spl22_1
| spl22_10 ),
inference(avatar_split_clause,[],[f49,f131,f88]) ).
fof(f136,definition,
( spl22_11
<=> fellow(sK19) ),
introduced(definition,[new_symbols(definition,[spl22_11])],[avatar_definition]) ).
fof(f138,plain,
( fellow(sK19)
| ~ spl22_11 ),
inference(avatar_component_clause,[],[f136]) ).
fof(f139,plain,
( ~ spl22_1
| spl22_11 ),
inference(avatar_split_clause,[],[f50,f136,f88]) ).
fof(f141,definition,
( spl22_12
<=> young(sK18) ),
introduced(definition,[new_symbols(definition,[spl22_12])],[avatar_definition]) ).
fof(f143,plain,
( young(sK18)
| ~ spl22_12 ),
inference(avatar_component_clause,[],[f141]) ).
fof(f144,plain,
( ~ spl22_1
| spl22_12 ),
inference(avatar_split_clause,[],[f51,f141,f88]) ).
fof(f146,definition,
( spl22_13
<=> man(sK18) ),
introduced(definition,[new_symbols(definition,[spl22_13])],[avatar_definition]) ).
fof(f148,plain,
( man(sK18)
| ~ spl22_13 ),
inference(avatar_component_clause,[],[f146]) ).
fof(f149,plain,
( ~ spl22_1
| spl22_13 ),
inference(avatar_split_clause,[],[f52,f146,f88]) ).
fof(f151,definition,
( spl22_14
<=> fellow(sK18) ),
introduced(definition,[new_symbols(definition,[spl22_14])],[avatar_definition]) ).
fof(f153,plain,
( fellow(sK18)
| ~ spl22_14 ),
inference(avatar_component_clause,[],[f151]) ).
fof(f154,plain,
( ~ spl22_1
| spl22_14 ),
inference(avatar_split_clause,[],[f53,f151,f88]) ).
fof(f156,definition,
( spl22_15
<=> sK18 = sK19 ),
introduced(definition,[new_symbols(definition,[spl22_15])],[avatar_definition]) ).
fof(f158,plain,
( sK18 != sK19
| spl22_15 ),
inference(avatar_component_clause,[],[f156]) ).
fof(f159,plain,
( ~ spl22_1
| ~ spl22_15 ),
inference(avatar_split_clause,[],[f54,f156,f88]) ).
fof(f161,definition,
( spl22_16
<=> in(sK15,sK14) ),
introduced(definition,[new_symbols(definition,[spl22_16])],[avatar_definition]) ).
fof(f163,plain,
( in(sK15,sK14)
| ~ spl22_16 ),
inference(avatar_component_clause,[],[f161]) ).
fof(f164,plain,
( ~ spl22_1
| spl22_16 ),
inference(avatar_split_clause,[],[f55,f161,f88]) ).
fof(f166,definition,
( spl22_17
<=> down(sK15,sK17) ),
introduced(definition,[new_symbols(definition,[spl22_17])],[avatar_definition]) ).
fof(f168,plain,
( down(sK15,sK17)
| ~ spl22_17 ),
inference(avatar_component_clause,[],[f166]) ).
fof(f169,plain,
( ~ spl22_1
| spl22_17 ),
inference(avatar_split_clause,[],[f56,f166,f88]) ).
fof(f171,definition,
( spl22_18
<=> barrel(sK15,sK16) ),
introduced(definition,[new_symbols(definition,[spl22_18])],[avatar_definition]) ).
fof(f173,plain,
( barrel(sK15,sK16)
| ~ spl22_18 ),
inference(avatar_component_clause,[],[f171]) ).
fof(f174,plain,
( ~ spl22_1
| spl22_18 ),
inference(avatar_split_clause,[],[f57,f171,f88]) ).
fof(f176,definition,
( spl22_19
<=> lonely(sK17) ),
introduced(definition,[new_symbols(definition,[spl22_19])],[avatar_definition]) ).
fof(f178,plain,
( lonely(sK17)
| ~ spl22_19 ),
inference(avatar_component_clause,[],[f176]) ).
fof(f179,plain,
( ~ spl22_1
| spl22_19 ),
inference(avatar_split_clause,[],[f58,f176,f88]) ).
fof(f181,definition,
( spl22_20
<=> way(sK17) ),
introduced(definition,[new_symbols(definition,[spl22_20])],[avatar_definition]) ).
fof(f183,plain,
( way(sK17)
| ~ spl22_20 ),
inference(avatar_component_clause,[],[f181]) ).
fof(f184,plain,
( ~ spl22_1
| spl22_20 ),
inference(avatar_split_clause,[],[f59,f181,f88]) ).
fof(f186,definition,
( spl22_21
<=> street(sK17) ),
introduced(definition,[new_symbols(definition,[spl22_21])],[avatar_definition]) ).
fof(f188,plain,
( street(sK17)
| ~ spl22_21 ),
inference(avatar_component_clause,[],[f186]) ).
fof(f189,plain,
( ~ spl22_1
| spl22_21 ),
inference(avatar_split_clause,[],[f60,f186,f88]) ).
fof(f191,definition,
( spl22_22
<=> old(sK16) ),
introduced(definition,[new_symbols(definition,[spl22_22])],[avatar_definition]) ).
fof(f193,plain,
( old(sK16)
| ~ spl22_22 ),
inference(avatar_component_clause,[],[f191]) ).
fof(f194,plain,
( ~ spl22_1
| spl22_22 ),
inference(avatar_split_clause,[],[f61,f191,f88]) ).
fof(f196,definition,
( spl22_23
<=> dirty(sK16) ),
introduced(definition,[new_symbols(definition,[spl22_23])],[avatar_definition]) ).
fof(f199,plain,
( ~ spl22_1
| spl22_23 ),
inference(avatar_split_clause,[],[f62,f196,f88]) ).
fof(f201,definition,
( spl22_24
<=> white(sK16) ),
introduced(definition,[new_symbols(definition,[spl22_24])],[avatar_definition]) ).
fof(f204,plain,
( ~ spl22_1
| spl22_24 ),
inference(avatar_split_clause,[],[f63,f201,f88]) ).
fof(f206,definition,
( spl22_25
<=> car(sK16) ),
introduced(definition,[new_symbols(definition,[spl22_25])],[avatar_definition]) ).
fof(f209,plain,
( ~ spl22_1
| spl22_25 ),
inference(avatar_split_clause,[],[f64,f206,f88]) ).
fof(f211,definition,
( spl22_26
<=> chevy(sK16) ),
introduced(definition,[new_symbols(definition,[spl22_26])],[avatar_definition]) ).
fof(f214,plain,
( ~ spl22_1
| spl22_26 ),
inference(avatar_split_clause,[],[f65,f211,f88]) ).
fof(f216,definition,
( spl22_27
<=> event(sK15) ),
introduced(definition,[new_symbols(definition,[spl22_27])],[avatar_definition]) ).
fof(f218,plain,
( event(sK15)
| ~ spl22_27 ),
inference(avatar_component_clause,[],[f216]) ).
fof(f219,plain,
( ~ spl22_1
| spl22_27 ),
inference(avatar_split_clause,[],[f66,f216,f88]) ).
fof(f221,definition,
( spl22_28
<=> city(sK14) ),
introduced(definition,[new_symbols(definition,[spl22_28])],[avatar_definition]) ).
fof(f223,plain,
( city(sK14)
| ~ spl22_28 ),
inference(avatar_component_clause,[],[f221]) ).
fof(f224,plain,
( ~ spl22_1
| spl22_28 ),
inference(avatar_split_clause,[],[f67,f221,f88]) ).
fof(f226,definition,
( spl22_29
<=> hollywood(sK14) ),
introduced(definition,[new_symbols(definition,[spl22_29])],[avatar_definition]) ).
fof(f228,plain,
( hollywood(sK14)
| ~ spl22_29 ),
inference(avatar_component_clause,[],[f226]) ).
fof(f229,plain,
( ~ spl22_1
| spl22_29 ),
inference(avatar_split_clause,[],[f68,f226,f88]) ).
fof(f231,definition,
( spl22_30
<=> front(sK13) ),
introduced(definition,[new_symbols(definition,[spl22_30])],[avatar_definition]) ).
fof(f233,plain,
( front(sK13)
| ~ spl22_30 ),
inference(avatar_component_clause,[],[f231]) ).
fof(f234,plain,
( ~ spl22_1
| spl22_30 ),
inference(avatar_split_clause,[],[f69,f231,f88]) ).
fof(f236,definition,
( spl22_31
<=> furniture(sK13) ),
introduced(definition,[new_symbols(definition,[spl22_31])],[avatar_definition]) ).
fof(f239,plain,
( ~ spl22_1
| spl22_31 ),
inference(avatar_split_clause,[],[f70,f236,f88]) ).
fof(f241,definition,
( spl22_32
<=> seat(sK13) ),
introduced(definition,[new_symbols(definition,[spl22_32])],[avatar_definition]) ).
fof(f243,plain,
( seat(sK13)
| ~ spl22_32 ),
inference(avatar_component_clause,[],[f241]) ).
fof(f244,plain,
( ~ spl22_1
| spl22_32 ),
inference(avatar_split_clause,[],[f71,f241,f88]) ).
fof(f246,definition,
( spl22_33
<=> front(sK12) ),
introduced(definition,[new_symbols(definition,[spl22_33])],[avatar_definition]) ).
fof(f248,plain,
( front(sK12)
| ~ spl22_33 ),
inference(avatar_component_clause,[],[f246]) ).
fof(f249,plain,
( ~ spl22_1
| spl22_33 ),
inference(avatar_split_clause,[],[f72,f246,f88]) ).
fof(f251,definition,
( spl22_34
<=> furniture(sK12) ),
introduced(definition,[new_symbols(definition,[spl22_34])],[avatar_definition]) ).
fof(f253,plain,
( furniture(sK12)
| ~ spl22_34 ),
inference(avatar_component_clause,[],[f251]) ).
fof(f254,plain,
( ~ spl22_1
| spl22_34 ),
inference(avatar_split_clause,[],[f73,f251,f88]) ).
fof(f256,definition,
( spl22_35
<=> seat(sK12) ),
introduced(definition,[new_symbols(definition,[spl22_35])],[avatar_definition]) ).
fof(f258,plain,
( seat(sK12)
| ~ spl22_35 ),
inference(avatar_component_clause,[],[f256]) ).
fof(f259,plain,
( ~ spl22_1
| spl22_35 ),
inference(avatar_split_clause,[],[f74,f256,f88]) ).
fof(f261,definition,
( spl22_36
<=> in(sK11,sK3) ),
introduced(definition,[new_symbols(definition,[spl22_36])],[avatar_definition]) ).
fof(f263,plain,
( in(sK11,sK3)
| ~ spl22_36 ),
inference(avatar_component_clause,[],[f261]) ).
fof(f264,plain,
( ~ spl22_2
| spl22_36 ),
inference(avatar_split_clause,[],[f13,f261,f92]) ).
fof(f266,definition,
( spl22_37
<=> sK9 = sK11 ),
introduced(definition,[new_symbols(definition,[spl22_37])],[avatar_definition]) ).
fof(f268,plain,
( sK9 = sK11
| ~ spl22_37 ),
inference(avatar_component_clause,[],[f266]) ).
fof(f269,plain,
( ~ spl22_2
| spl22_37 ),
inference(avatar_split_clause,[],[f14,f266,f92]) ).
fof(f271,definition,
( spl22_38
<=> in(sK10,sK2) ),
introduced(definition,[new_symbols(definition,[spl22_38])],[avatar_definition]) ).
fof(f273,plain,
( in(sK10,sK2)
| ~ spl22_38 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f274,plain,
( ~ spl22_2
| spl22_38 ),
inference(avatar_split_clause,[],[f15,f271,f92]) ).
fof(f276,definition,
( spl22_39
<=> sK8 = sK10 ),
introduced(definition,[new_symbols(definition,[spl22_39])],[avatar_definition]) ).
fof(f278,plain,
( sK8 = sK10
| ~ spl22_39 ),
inference(avatar_component_clause,[],[f276]) ).
fof(f279,plain,
( ~ spl22_2
| spl22_39 ),
inference(avatar_split_clause,[],[f16,f276,f92]) ).
fof(f281,definition,
( spl22_40
<=> young(sK9) ),
introduced(definition,[new_symbols(definition,[spl22_40])],[avatar_definition]) ).
fof(f283,plain,
( young(sK9)
| ~ spl22_40 ),
inference(avatar_component_clause,[],[f281]) ).
fof(f284,plain,
( ~ spl22_2
| spl22_40 ),
inference(avatar_split_clause,[],[f17,f281,f92]) ).
fof(f286,definition,
( spl22_41
<=> man(sK9) ),
introduced(definition,[new_symbols(definition,[spl22_41])],[avatar_definition]) ).
fof(f288,plain,
( man(sK9)
| ~ spl22_41 ),
inference(avatar_component_clause,[],[f286]) ).
fof(f289,plain,
( ~ spl22_2
| spl22_41 ),
inference(avatar_split_clause,[],[f18,f286,f92]) ).
fof(f291,definition,
( spl22_42
<=> fellow(sK9) ),
introduced(definition,[new_symbols(definition,[spl22_42])],[avatar_definition]) ).
fof(f294,plain,
( ~ spl22_2
| spl22_42 ),
inference(avatar_split_clause,[],[f19,f291,f92]) ).
fof(f296,definition,
( spl22_43
<=> young(sK8) ),
introduced(definition,[new_symbols(definition,[spl22_43])],[avatar_definition]) ).
fof(f298,plain,
( young(sK8)
| ~ spl22_43 ),
inference(avatar_component_clause,[],[f296]) ).
fof(f299,plain,
( ~ spl22_2
| spl22_43 ),
inference(avatar_split_clause,[],[f20,f296,f92]) ).
fof(f301,definition,
( spl22_44
<=> man(sK8) ),
introduced(definition,[new_symbols(definition,[spl22_44])],[avatar_definition]) ).
fof(f303,plain,
( man(sK8)
| ~ spl22_44 ),
inference(avatar_component_clause,[],[f301]) ).
fof(f304,plain,
( ~ spl22_2
| spl22_44 ),
inference(avatar_split_clause,[],[f21,f301,f92]) ).
fof(f306,definition,
( spl22_45
<=> fellow(sK8) ),
introduced(definition,[new_symbols(definition,[spl22_45])],[avatar_definition]) ).
fof(f308,plain,
( fellow(sK8)
| ~ spl22_45 ),
inference(avatar_component_clause,[],[f306]) ).
fof(f309,plain,
( ~ spl22_2
| spl22_45 ),
inference(avatar_split_clause,[],[f22,f306,f92]) ).
fof(f311,definition,
( spl22_46
<=> sK8 = sK9 ),
introduced(definition,[new_symbols(definition,[spl22_46])],[avatar_definition]) ).
fof(f313,plain,
( sK8 != sK9
| spl22_46 ),
inference(avatar_component_clause,[],[f311]) ).
fof(f314,plain,
( ~ spl22_2
| ~ spl22_46 ),
inference(avatar_split_clause,[],[f23,f311,f92]) ).
fof(f316,definition,
( spl22_47
<=> in(sK5,sK4) ),
introduced(definition,[new_symbols(definition,[spl22_47])],[avatar_definition]) ).
fof(f318,plain,
( in(sK5,sK4)
| ~ spl22_47 ),
inference(avatar_component_clause,[],[f316]) ).
fof(f319,plain,
( ~ spl22_2
| spl22_47 ),
inference(avatar_split_clause,[],[f24,f316,f92]) ).
fof(f321,definition,
( spl22_48
<=> down(sK5,sK6) ),
introduced(definition,[new_symbols(definition,[spl22_48])],[avatar_definition]) ).
fof(f323,plain,
( down(sK5,sK6)
| ~ spl22_48 ),
inference(avatar_component_clause,[],[f321]) ).
fof(f324,plain,
( ~ spl22_2
| spl22_48 ),
inference(avatar_split_clause,[],[f25,f321,f92]) ).
fof(f326,definition,
( spl22_49
<=> barrel(sK5,sK7) ),
introduced(definition,[new_symbols(definition,[spl22_49])],[avatar_definition]) ).
fof(f328,plain,
( barrel(sK5,sK7)
| ~ spl22_49 ),
inference(avatar_component_clause,[],[f326]) ).
fof(f329,plain,
( ~ spl22_2
| spl22_49 ),
inference(avatar_split_clause,[],[f26,f326,f92]) ).
fof(f331,definition,
( spl22_50
<=> old(sK7) ),
introduced(definition,[new_symbols(definition,[spl22_50])],[avatar_definition]) ).
fof(f333,plain,
( old(sK7)
| ~ spl22_50 ),
inference(avatar_component_clause,[],[f331]) ).
fof(f334,plain,
( ~ spl22_2
| spl22_50 ),
inference(avatar_split_clause,[],[f27,f331,f92]) ).
fof(f336,definition,
( spl22_51
<=> dirty(sK7) ),
introduced(definition,[new_symbols(definition,[spl22_51])],[avatar_definition]) ).
fof(f339,plain,
( ~ spl22_2
| spl22_51 ),
inference(avatar_split_clause,[],[f28,f336,f92]) ).
fof(f341,definition,
( spl22_52
<=> white(sK7) ),
introduced(definition,[new_symbols(definition,[spl22_52])],[avatar_definition]) ).
fof(f344,plain,
( ~ spl22_2
| spl22_52 ),
inference(avatar_split_clause,[],[f29,f341,f92]) ).
fof(f346,definition,
( spl22_53
<=> car(sK7) ),
introduced(definition,[new_symbols(definition,[spl22_53])],[avatar_definition]) ).
fof(f349,plain,
( ~ spl22_2
| spl22_53 ),
inference(avatar_split_clause,[],[f30,f346,f92]) ).
fof(f351,definition,
( spl22_54
<=> chevy(sK7) ),
introduced(definition,[new_symbols(definition,[spl22_54])],[avatar_definition]) ).
fof(f354,plain,
( ~ spl22_2
| spl22_54 ),
inference(avatar_split_clause,[],[f31,f351,f92]) ).
fof(f356,definition,
( spl22_55
<=> lonely(sK6) ),
introduced(definition,[new_symbols(definition,[spl22_55])],[avatar_definition]) ).
fof(f358,plain,
( lonely(sK6)
| ~ spl22_55 ),
inference(avatar_component_clause,[],[f356]) ).
fof(f359,plain,
( ~ spl22_2
| spl22_55 ),
inference(avatar_split_clause,[],[f32,f356,f92]) ).
fof(f361,definition,
( spl22_56
<=> way(sK6) ),
introduced(definition,[new_symbols(definition,[spl22_56])],[avatar_definition]) ).
fof(f363,plain,
( way(sK6)
| ~ spl22_56 ),
inference(avatar_component_clause,[],[f361]) ).
fof(f364,plain,
( ~ spl22_2
| spl22_56 ),
inference(avatar_split_clause,[],[f33,f361,f92]) ).
fof(f366,definition,
( spl22_57
<=> street(sK6) ),
introduced(definition,[new_symbols(definition,[spl22_57])],[avatar_definition]) ).
fof(f368,plain,
( street(sK6)
| ~ spl22_57 ),
inference(avatar_component_clause,[],[f366]) ).
fof(f369,plain,
( ~ spl22_2
| spl22_57 ),
inference(avatar_split_clause,[],[f34,f366,f92]) ).
fof(f371,definition,
( spl22_58
<=> event(sK5) ),
introduced(definition,[new_symbols(definition,[spl22_58])],[avatar_definition]) ).
fof(f373,plain,
( event(sK5)
| ~ spl22_58 ),
inference(avatar_component_clause,[],[f371]) ).
fof(f374,plain,
( ~ spl22_2
| spl22_58 ),
inference(avatar_split_clause,[],[f35,f371,f92]) ).
fof(f376,definition,
( spl22_59
<=> city(sK4) ),
introduced(definition,[new_symbols(definition,[spl22_59])],[avatar_definition]) ).
fof(f378,plain,
( city(sK4)
| ~ spl22_59 ),
inference(avatar_component_clause,[],[f376]) ).
fof(f379,plain,
( ~ spl22_2
| spl22_59 ),
inference(avatar_split_clause,[],[f36,f376,f92]) ).
fof(f381,definition,
( spl22_60
<=> hollywood(sK4) ),
introduced(definition,[new_symbols(definition,[spl22_60])],[avatar_definition]) ).
fof(f383,plain,
( hollywood(sK4)
| ~ spl22_60 ),
inference(avatar_component_clause,[],[f381]) ).
fof(f384,plain,
( ~ spl22_2
| spl22_60 ),
inference(avatar_split_clause,[],[f37,f381,f92]) ).
fof(f386,definition,
( spl22_61
<=> front(sK3) ),
introduced(definition,[new_symbols(definition,[spl22_61])],[avatar_definition]) ).
fof(f388,plain,
( front(sK3)
| ~ spl22_61 ),
inference(avatar_component_clause,[],[f386]) ).
fof(f389,plain,
( ~ spl22_2
| spl22_61 ),
inference(avatar_split_clause,[],[f38,f386,f92]) ).
fof(f391,definition,
( spl22_62
<=> furniture(sK3) ),
introduced(definition,[new_symbols(definition,[spl22_62])],[avatar_definition]) ).
fof(f393,plain,
( furniture(sK3)
| ~ spl22_62 ),
inference(avatar_component_clause,[],[f391]) ).
fof(f394,plain,
( ~ spl22_2
| spl22_62 ),
inference(avatar_split_clause,[],[f39,f391,f92]) ).
fof(f396,definition,
( spl22_63
<=> seat(sK3) ),
introduced(definition,[new_symbols(definition,[spl22_63])],[avatar_definition]) ).
fof(f398,plain,
( seat(sK3)
| ~ spl22_63 ),
inference(avatar_component_clause,[],[f396]) ).
fof(f399,plain,
( ~ spl22_2
| spl22_63 ),
inference(avatar_split_clause,[],[f40,f396,f92]) ).
fof(f401,definition,
( spl22_64
<=> front(sK2) ),
introduced(definition,[new_symbols(definition,[spl22_64])],[avatar_definition]) ).
fof(f403,plain,
( front(sK2)
| ~ spl22_64 ),
inference(avatar_component_clause,[],[f401]) ).
fof(f404,plain,
( ~ spl22_2
| spl22_64 ),
inference(avatar_split_clause,[],[f41,f401,f92]) ).
fof(f406,definition,
( spl22_65
<=> furniture(sK2) ),
introduced(definition,[new_symbols(definition,[spl22_65])],[avatar_definition]) ).
fof(f408,plain,
( furniture(sK2)
| ~ spl22_65 ),
inference(avatar_component_clause,[],[f406]) ).
fof(f409,plain,
( ~ spl22_2
| spl22_65 ),
inference(avatar_split_clause,[],[f42,f406,f92]) ).
fof(f411,definition,
( spl22_66
<=> seat(sK2) ),
introduced(definition,[new_symbols(definition,[spl22_66])],[avatar_definition]) ).
fof(f413,plain,
( seat(sK2)
| ~ spl22_66 ),
inference(avatar_component_clause,[],[f411]) ).
fof(f414,plain,
( ~ spl22_2
| spl22_66 ),
inference(avatar_split_clause,[],[f43,f411,f92]) ).
fof(f415,plain,
( ! [X2,X0,X1] :
( ~ event(X0)
| ~ in(X0,X1)
| ~ down(X0,X2)
| ~ barrel(X0,sK7)
| ~ chevy(sK7)
| ~ hollywood(X1)
| ~ dirty(sK7)
| ~ white(sK7)
| ~ car(sK7)
| ~ street(X2)
| ~ lonely(X2)
| ~ way(X2)
| ~ city(X1) )
| ~ spl22_3
| ~ spl22_50 ),
inference(resolution,[],[f333,f98]) ).
fof(f417,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(f418,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,[],[f417]) ).
fof(f419,plain,
( ~ spl22_53
| ~ spl22_52
| ~ spl22_51
| ~ spl22_54
| spl22_67
| ~ spl22_3
| ~ spl22_50 ),
inference(avatar_split_clause,[],[f415,f331,f97,f417,f351,f336,f341,f346]) ).
fof(f420,plain,
( ! [X2,X0,X1] :
( ~ event(X0)
| ~ in(X0,X1)
| ~ down(X0,X2)
| ~ barrel(X0,sK16)
| ~ chevy(sK16)
| ~ hollywood(X1)
| ~ dirty(sK16)
| ~ white(sK16)
| ~ car(sK16)
| ~ street(X2)
| ~ lonely(X2)
| ~ way(X2)
| ~ city(X1) )
| ~ spl22_3
| ~ spl22_22 ),
inference(resolution,[],[f193,f98]) ).
fof(f422,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(f423,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,[],[f422]) ).
fof(f424,plain,
( ~ spl22_25
| ~ spl22_24
| ~ spl22_23
| ~ spl22_26
| spl22_68
| ~ spl22_3
| ~ spl22_22 ),
inference(avatar_split_clause,[],[f420,f191,f97,f422,f211,f196,f201,f206]) ).
fof(f425,plain,
( in(sK19,sK13)
| ~ spl22_5
| ~ spl22_6 ),
inference(superposition,[],[f108,f113]) ).
fof(f426,plain,
( in(sK18,sK12)
| ~ spl22_7
| ~ spl22_8 ),
inference(superposition,[],[f118,f123]) ).
fof(f427,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,[],[f173,f423]) ).
fof(f428,plain,
( ! [X0,X1] :
( ~ city(X0)
| ~ way(X1)
| ~ lonely(X1)
| ~ street(X1)
| ~ hollywood(X0)
| ~ down(sK15,X1)
| ~ in(sK15,X0) )
| ~ spl22_18
| ~ spl22_27
| ~ spl22_68 ),
inference(forward_subsumption_resolution,[],[f427,f218]) ).
fof(f430,definition,
( spl22_69
<=> ! [X1] :
( ~ way(X1)
| ~ down(sK15,X1)
| ~ street(X1)
| ~ lonely(X1) ) ),
introduced(definition,[new_symbols(definition,[spl22_69])],[avatar_definition]) ).
fof(f431,plain,
( ! [X1] :
( ~ down(sK15,X1)
| ~ way(X1)
| ~ street(X1)
| ~ lonely(X1) )
| ~ spl22_69 ),
inference(avatar_component_clause,[],[f430]) ).
fof(f433,definition,
( spl22_70
<=> ! [X0] :
( ~ city(X0)
| ~ in(sK15,X0)
| ~ hollywood(X0) ) ),
introduced(definition,[new_symbols(definition,[spl22_70])],[avatar_definition]) ).
fof(f434,plain,
( ! [X0] :
( ~ in(sK15,X0)
| ~ city(X0)
| ~ hollywood(X0) )
| ~ spl22_70 ),
inference(avatar_component_clause,[],[f433]) ).
fof(f435,plain,
( spl22_69
| spl22_70
| ~ spl22_18
| ~ spl22_27
| ~ spl22_68 ),
inference(avatar_split_clause,[],[f428,f422,f216,f171,f433,f430]) ).
fof(f436,plain,
( ~ city(sK14)
| ~ hollywood(sK14)
| ~ spl22_16
| ~ spl22_70 ),
inference(resolution,[],[f434,f163]) ).
fof(f437,plain,
( ~ hollywood(sK14)
| ~ spl22_16
| ~ spl22_28
| ~ spl22_70 ),
inference(forward_subsumption_resolution,[],[f436,f223]) ).
fof(f438,plain,
( $false
| ~ spl22_16
| ~ spl22_28
| ~ spl22_29
| ~ spl22_70 ),
inference(forward_subsumption_resolution,[],[f437,f228]) ).
fof(f439,plain,
( ~ spl22_16
| ~ spl22_28
| ~ spl22_29
| ~ spl22_70 ),
inference(avatar_contradiction_clause,[],[f438]) ).
fof(f440,plain,
( ~ way(sK17)
| ~ street(sK17)
| ~ lonely(sK17)
| ~ spl22_17
| ~ spl22_69 ),
inference(resolution,[],[f431,f168]) ).
fof(f441,plain,
( ~ street(sK17)
| ~ lonely(sK17)
| ~ spl22_17
| ~ spl22_20
| ~ spl22_69 ),
inference(forward_subsumption_resolution,[],[f440,f183]) ).
fof(f442,plain,
( ~ lonely(sK17)
| ~ spl22_17
| ~ spl22_20
| ~ spl22_21
| ~ spl22_69 ),
inference(forward_subsumption_resolution,[],[f441,f188]) ).
fof(f443,plain,
( $false
| ~ spl22_17
| ~ spl22_19
| ~ spl22_20
| ~ spl22_21
| ~ spl22_69 ),
inference(forward_subsumption_resolution,[],[f442,f178]) ).
fof(f444,plain,
( ~ spl22_17
| ~ spl22_19
| ~ spl22_20
| ~ spl22_21
| ~ spl22_69 ),
inference(avatar_contradiction_clause,[],[f443]) ).
fof(f445,plain,
( in(sK9,sK3)
| ~ spl22_36
| ~ spl22_37 ),
inference(superposition,[],[f263,f268]) ).
fof(f447,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,[],[f328,f418]) ).
fof(f448,plain,
( ! [X0,X1] :
( ~ city(X0)
| ~ way(X1)
| ~ lonely(X1)
| ~ street(X1)
| ~ hollywood(X0)
| ~ down(sK5,X1)
| ~ in(sK5,X0) )
| ~ spl22_49
| ~ spl22_58
| ~ spl22_67 ),
inference(forward_subsumption_resolution,[],[f447,f373]) ).
fof(f450,definition,
( spl22_71
<=> ! [X1] :
( ~ way(X1)
| ~ down(sK5,X1)
| ~ street(X1)
| ~ lonely(X1) ) ),
introduced(definition,[new_symbols(definition,[spl22_71])],[avatar_definition]) ).
fof(f451,plain,
( ! [X1] :
( ~ down(sK5,X1)
| ~ way(X1)
| ~ street(X1)
| ~ lonely(X1) )
| ~ spl22_71 ),
inference(avatar_component_clause,[],[f450]) ).
fof(f453,definition,
( spl22_72
<=> ! [X0] :
( ~ city(X0)
| ~ in(sK5,X0)
| ~ hollywood(X0) ) ),
introduced(definition,[new_symbols(definition,[spl22_72])],[avatar_definition]) ).
fof(f454,plain,
( ! [X0] :
( ~ in(sK5,X0)
| ~ city(X0)
| ~ hollywood(X0) )
| ~ spl22_72 ),
inference(avatar_component_clause,[],[f453]) ).
fof(f455,plain,
( spl22_71
| spl22_72
| ~ spl22_49
| ~ spl22_58
| ~ spl22_67 ),
inference(avatar_split_clause,[],[f448,f417,f371,f326,f453,f450]) ).
fof(f456,plain,
( ~ way(sK6)
| ~ street(sK6)
| ~ lonely(sK6)
| ~ spl22_48
| ~ spl22_71 ),
inference(resolution,[],[f451,f323]) ).
fof(f457,plain,
( ~ street(sK6)
| ~ lonely(sK6)
| ~ spl22_48
| ~ spl22_56
| ~ spl22_71 ),
inference(forward_subsumption_resolution,[],[f456,f363]) ).
fof(f458,plain,
( ~ lonely(sK6)
| ~ spl22_48
| ~ spl22_56
| ~ spl22_57
| ~ spl22_71 ),
inference(forward_subsumption_resolution,[],[f457,f368]) ).
fof(f459,plain,
( $false
| ~ spl22_48
| ~ spl22_55
| ~ spl22_56
| ~ spl22_57
| ~ spl22_71 ),
inference(forward_subsumption_resolution,[],[f458,f358]) ).
fof(f460,plain,
( ~ spl22_48
| ~ spl22_55
| ~ spl22_56
| ~ spl22_57
| ~ spl22_71 ),
inference(avatar_contradiction_clause,[],[f459]) ).
fof(f461,plain,
( ~ city(sK4)
| ~ hollywood(sK4)
| ~ spl22_47
| ~ spl22_72 ),
inference(resolution,[],[f454,f318]) ).
fof(f462,plain,
( ~ hollywood(sK4)
| ~ spl22_47
| ~ spl22_59
| ~ spl22_72 ),
inference(forward_subsumption_resolution,[],[f461,f378]) ).
fof(f463,plain,
( $false
| ~ spl22_47
| ~ spl22_59
| ~ spl22_60
| ~ spl22_72 ),
inference(forward_subsumption_resolution,[],[f462,f383]) ).
fof(f464,plain,
( ~ spl22_47
| ~ spl22_59
| ~ spl22_60
| ~ spl22_72 ),
inference(avatar_contradiction_clause,[],[f463]) ).
fof(f466,plain,
( ! [X2,X0,X1] :
( ~ in(sK9,X0)
| sK9 = X1
| ~ in(X1,X2)
| ~ seat(X2)
| ~ man(sK9)
| ~ fellow(sK9)
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ seat(X0)
| ~ front(X0)
| ~ furniture(X0)
| ~ front(X2)
| ~ furniture(X2) )
| ~ spl22_4
| ~ spl22_40 ),
inference(resolution,[],[f101,f283]) ).
fof(f468,plain,
( ! [X2,X0,X1] :
( ~ in(sK19,X0)
| sK19 = X1
| ~ in(X1,X2)
| ~ seat(X2)
| ~ man(sK19)
| ~ fellow(sK19)
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ seat(X0)
| ~ front(X0)
| ~ furniture(X0)
| ~ front(X2)
| ~ furniture(X2) )
| ~ spl22_4
| ~ spl22_9 ),
inference(resolution,[],[f101,f128]) ).
fof(f471,plain,
( ! [X2,X0,X1] :
( ~ in(sK19,X0)
| sK19 = X1
| ~ in(X1,X2)
| ~ seat(X2)
| ~ fellow(sK19)
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ seat(X0)
| ~ front(X0)
| ~ furniture(X0)
| ~ front(X2)
| ~ furniture(X2) )
| ~ spl22_4
| ~ spl22_9
| ~ spl22_10 ),
inference(forward_subsumption_resolution,[],[f468,f133]) ).
fof(f473,plain,
( ! [X2,X0,X1] :
( ~ in(sK9,X0)
| sK9 = X1
| ~ in(X1,X2)
| ~ seat(X2)
| ~ fellow(sK9)
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ seat(X0)
| ~ front(X0)
| ~ furniture(X0)
| ~ front(X2)
| ~ furniture(X2) )
| ~ spl22_4
| ~ spl22_40
| ~ spl22_41 ),
inference(forward_subsumption_resolution,[],[f466,f288]) ).
fof(f475,plain,
( ! [X2,X0,X1] :
( ~ in(sK19,X0)
| sK19 = X1
| ~ in(X1,X2)
| ~ seat(X2)
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ seat(X0)
| ~ front(X0)
| ~ furniture(X0)
| ~ front(X2)
| ~ furniture(X2) )
| ~ spl22_4
| ~ spl22_9
| ~ spl22_10
| ~ spl22_11 ),
inference(forward_subsumption_resolution,[],[f471,f138]) ).
fof(f480,definition,
( spl22_73
<=> ! [X2,X1] :
( sK19 = X1
| ~ furniture(X2)
| ~ front(X2)
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ seat(X2)
| ~ in(X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl22_73])],[avatar_definition]) ).
fof(f481,plain,
( ! [X2,X1] :
( ~ fellow(X1)
| ~ furniture(X2)
| ~ front(X2)
| sK19 = X1
| ~ man(X1)
| ~ young(X1)
| ~ seat(X2)
| ~ in(X1,X2) )
| ~ spl22_73 ),
inference(avatar_component_clause,[],[f480]) ).
fof(f483,definition,
( spl22_74
<=> ! [X0] :
( ~ in(sK19,X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ seat(X0) ) ),
introduced(definition,[new_symbols(definition,[spl22_74])],[avatar_definition]) ).
fof(f484,plain,
( ! [X0] :
( ~ in(sK19,X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ seat(X0) )
| ~ spl22_74 ),
inference(avatar_component_clause,[],[f483]) ).
fof(f485,plain,
( spl22_73
| spl22_74
| ~ spl22_4
| ~ spl22_9
| ~ spl22_10
| ~ spl22_11 ),
inference(avatar_split_clause,[],[f475,f136,f131,f126,f100,f483,f480]) ).
fof(f490,definition,
( spl22_76
<=> ! [X0] :
( ~ in(sK18,X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ seat(X0) ) ),
introduced(definition,[new_symbols(definition,[spl22_76])],[avatar_definition]) ).
fof(f491,plain,
( ! [X0] :
( ~ in(sK18,X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ seat(X0) )
| ~ spl22_76 ),
inference(avatar_component_clause,[],[f490]) ).
fof(f494,definition,
( spl22_77
<=> ! [X2,X1] :
( sK9 = X1
| ~ furniture(X2)
| ~ front(X2)
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ seat(X2)
| ~ in(X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl22_77])],[avatar_definition]) ).
fof(f495,plain,
( ! [X2,X1] :
( ~ furniture(X2)
| sK9 = X1
| ~ front(X2)
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ seat(X2)
| ~ in(X1,X2) )
| ~ spl22_77 ),
inference(avatar_component_clause,[],[f494]) ).
fof(f497,definition,
( spl22_78
<=> ! [X0] :
( ~ in(sK9,X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ seat(X0) ) ),
introduced(definition,[new_symbols(definition,[spl22_78])],[avatar_definition]) ).
fof(f498,plain,
( ! [X0] :
( ~ in(sK9,X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ seat(X0) )
| ~ spl22_78 ),
inference(avatar_component_clause,[],[f497]) ).
fof(f507,plain,
( ~ furniture(sK13)
| ~ front(sK13)
| ~ seat(sK13)
| ~ spl22_5
| ~ spl22_6
| ~ spl22_74 ),
inference(resolution,[],[f484,f425]) ).
fof(f512,plain,
( ~ furniture(sK13)
| ~ seat(sK13)
| ~ spl22_5
| ~ spl22_6
| ~ spl22_30
| ~ spl22_74 ),
inference(forward_subsumption_resolution,[],[f507,f233]) ).
fof(f513,plain,
( ~ furniture(sK13)
| ~ spl22_5
| ~ spl22_6
| ~ spl22_30
| ~ spl22_32
| ~ spl22_74 ),
inference(forward_subsumption_resolution,[],[f512,f243]) ).
fof(f514,plain,
( ~ spl22_31
| ~ spl22_5
| ~ spl22_6
| ~ spl22_30
| ~ spl22_32
| ~ spl22_74 ),
inference(avatar_split_clause,[],[f513,f483,f241,f231,f111,f106,f236]) ).
fof(f524,plain,
( ! [X0] :
( sK9 = X0
| ~ front(sK2)
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(sK2)
| ~ in(X0,sK2) )
| ~ spl22_65
| ~ spl22_77 ),
inference(resolution,[],[f495,f408]) ).
fof(f529,plain,
( ! [X0] :
( sK9 = X0
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(sK2)
| ~ in(X0,sK2) )
| ~ spl22_64
| ~ spl22_65
| ~ spl22_77 ),
inference(forward_subsumption_resolution,[],[f524,f403]) ).
fof(f532,plain,
( ! [X0] :
( ~ in(X0,sK2)
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| sK9 = X0 )
| ~ spl22_64
| ~ spl22_65
| ~ spl22_66
| ~ spl22_77 ),
inference(forward_subsumption_resolution,[],[f529,f413]) ).
fof(f577,plain,
( ~ fellow(sK10)
| ~ man(sK10)
| ~ young(sK10)
| sK9 = sK10
| ~ spl22_38
| ~ spl22_64
| ~ spl22_65
| ~ spl22_66
| ~ spl22_77 ),
inference(resolution,[],[f532,f273]) ).
fof(f578,plain,
( ~ fellow(sK8)
| ~ man(sK10)
| ~ young(sK10)
| sK9 = sK10
| ~ spl22_38
| ~ spl22_39
| ~ spl22_64
| ~ spl22_65
| ~ spl22_66
| ~ spl22_77 ),
inference(forward_demodulation,[],[f577,f278]) ).
fof(f580,plain,
( ~ man(sK10)
| ~ young(sK10)
| sK9 = sK10
| ~ spl22_38
| ~ spl22_39
| ~ spl22_45
| ~ spl22_64
| ~ spl22_65
| ~ spl22_66
| ~ spl22_77 ),
inference(forward_subsumption_resolution,[],[f578,f308]) ).
fof(f582,plain,
( ~ man(sK8)
| ~ young(sK10)
| sK9 = sK10
| ~ spl22_38
| ~ spl22_39
| ~ spl22_45
| ~ spl22_64
| ~ spl22_65
| ~ spl22_66
| ~ spl22_77 ),
inference(forward_demodulation,[],[f580,f278]) ).
fof(f584,plain,
( ~ young(sK10)
| sK9 = sK10
| ~ spl22_38
| ~ spl22_39
| ~ spl22_44
| ~ spl22_45
| ~ spl22_64
| ~ spl22_65
| ~ spl22_66
| ~ spl22_77 ),
inference(forward_subsumption_resolution,[],[f582,f303]) ).
fof(f587,plain,
( ~ young(sK8)
| sK9 = sK10
| ~ spl22_38
| ~ spl22_39
| ~ spl22_44
| ~ spl22_45
| ~ spl22_64
| ~ spl22_65
| ~ spl22_66
| ~ spl22_77 ),
inference(forward_demodulation,[],[f584,f278]) ).
fof(f588,plain,
( sK9 = sK10
| ~ spl22_38
| ~ spl22_39
| ~ spl22_43
| ~ spl22_44
| ~ spl22_45
| ~ spl22_64
| ~ spl22_65
| ~ spl22_66
| ~ spl22_77 ),
inference(forward_subsumption_resolution,[],[f587,f298]) ).
fof(f589,plain,
( sK8 = sK9
| ~ spl22_38
| ~ spl22_39
| ~ spl22_43
| ~ spl22_44
| ~ spl22_45
| ~ spl22_64
| ~ spl22_65
| ~ spl22_66
| ~ spl22_77 ),
inference(forward_demodulation,[],[f588,f278]) ).
fof(f590,plain,
( $false
| ~ spl22_38
| ~ spl22_39
| ~ spl22_43
| ~ spl22_44
| ~ spl22_45
| spl22_46
| ~ spl22_64
| ~ spl22_65
| ~ spl22_66
| ~ spl22_77 ),
inference(forward_subsumption_resolution,[],[f589,f313]) ).
fof(f591,plain,
( ~ spl22_38
| ~ spl22_39
| ~ spl22_43
| ~ spl22_44
| ~ spl22_45
| spl22_46
| ~ spl22_64
| ~ spl22_65
| ~ spl22_66
| ~ spl22_77 ),
inference(avatar_contradiction_clause,[],[f590]) ).
fof(f592,plain,
( ~ furniture(sK3)
| ~ front(sK3)
| ~ seat(sK3)
| ~ spl22_36
| ~ spl22_37
| ~ spl22_78 ),
inference(resolution,[],[f498,f445]) ).
fof(f595,plain,
( ~ front(sK3)
| ~ seat(sK3)
| ~ spl22_36
| ~ spl22_37
| ~ spl22_62
| ~ spl22_78 ),
inference(forward_subsumption_resolution,[],[f592,f393]) ).
fof(f597,plain,
( ~ seat(sK3)
| ~ spl22_36
| ~ spl22_37
| ~ spl22_61
| ~ spl22_62
| ~ spl22_78 ),
inference(forward_subsumption_resolution,[],[f595,f388]) ).
fof(f600,plain,
( $false
| ~ spl22_36
| ~ spl22_37
| ~ spl22_61
| ~ spl22_62
| ~ spl22_63
| ~ spl22_78 ),
inference(forward_subsumption_resolution,[],[f597,f398]) ).
fof(f601,plain,
( ~ spl22_36
| ~ spl22_37
| ~ spl22_61
| ~ spl22_62
| ~ spl22_63
| ~ spl22_78 ),
inference(avatar_contradiction_clause,[],[f600]) ).
fof(f602,plain,
( ~ spl22_42
| spl22_77
| spl22_78
| ~ spl22_4
| ~ spl22_40
| ~ spl22_41 ),
inference(avatar_split_clause,[],[f473,f286,f281,f100,f497,f494,f291]) ).
fof(f640,plain,
( ! [X0] :
( ~ furniture(X0)
| ~ front(X0)
| sK18 = sK19
| ~ man(sK18)
| ~ young(sK18)
| ~ seat(X0)
| ~ in(sK18,X0) )
| ~ spl22_14
| ~ spl22_73 ),
inference(resolution,[],[f481,f153]) ).
fof(f642,plain,
( ! [X0] :
( ~ furniture(X0)
| ~ front(X0)
| ~ man(sK18)
| ~ young(sK18)
| ~ seat(X0)
| ~ in(sK18,X0) )
| ~ spl22_14
| spl22_15
| ~ spl22_73 ),
inference(forward_subsumption_resolution,[],[f640,f158]) ).
fof(f644,plain,
( ! [X0] :
( ~ furniture(X0)
| ~ front(X0)
| ~ young(sK18)
| ~ seat(X0)
| ~ in(sK18,X0) )
| ~ spl22_13
| ~ spl22_14
| spl22_15
| ~ spl22_73 ),
inference(forward_subsumption_resolution,[],[f642,f148]) ).
fof(f646,plain,
( ! [X0] :
( ~ furniture(X0)
| ~ front(X0)
| ~ seat(X0)
| ~ in(sK18,X0) )
| ~ spl22_12
| ~ spl22_13
| ~ spl22_14
| spl22_15
| ~ spl22_73 ),
inference(forward_subsumption_resolution,[],[f644,f143]) ).
fof(f654,plain,
( spl22_76
| ~ spl22_12
| ~ spl22_13
| ~ spl22_14
| spl22_15
| ~ spl22_73 ),
inference(avatar_split_clause,[],[f646,f480,f156,f151,f146,f141,f490]) ).
fof(f660,plain,
( ~ furniture(sK12)
| ~ front(sK12)
| ~ seat(sK12)
| ~ spl22_7
| ~ spl22_8
| ~ spl22_76 ),
inference(resolution,[],[f491,f426]) ).
fof(f661,plain,
( ~ front(sK12)
| ~ seat(sK12)
| ~ spl22_7
| ~ spl22_8
| ~ spl22_34
| ~ spl22_76 ),
inference(forward_subsumption_resolution,[],[f660,f253]) ).
fof(f662,plain,
( ~ seat(sK12)
| ~ spl22_7
| ~ spl22_8
| ~ spl22_33
| ~ spl22_34
| ~ spl22_76 ),
inference(forward_subsumption_resolution,[],[f661,f248]) ).
fof(f663,plain,
( $false
| ~ spl22_7
| ~ spl22_8
| ~ spl22_33
| ~ spl22_34
| ~ spl22_35
| ~ spl22_76 ),
inference(forward_subsumption_resolution,[],[f662,f258]) ).
fof(f664,plain,
( ~ spl22_7
| ~ spl22_8
| ~ spl22_33
| ~ spl22_34
| ~ spl22_35
| ~ spl22_76 ),
inference(avatar_contradiction_clause,[],[f663]) ).
cnf(s1,plain,
( spl22_1
| spl22_2 ),
inference(sat_conversion,[],[f95]) ).
cnf(s4,plain,
( spl22_3
| spl22_4
| spl22_3
| spl22_4 ),
inference(sat_conversion,[],[f104]) ).
cnf(s5,plain,
( spl22_3
| spl22_4 ),
inference(rat,[],[s4]) ).
cnf(s6,plain,
( ~ spl22_1
| spl22_5 ),
inference(sat_conversion,[],[f109]) ).
cnf(s7,plain,
( ~ spl22_1
| spl22_6 ),
inference(sat_conversion,[],[f114]) ).
cnf(s8,plain,
( ~ spl22_1
| spl22_7 ),
inference(sat_conversion,[],[f119]) ).
cnf(s9,plain,
( ~ spl22_1
| spl22_8 ),
inference(sat_conversion,[],[f124]) ).
cnf(s10,plain,
( ~ spl22_1
| spl22_9 ),
inference(sat_conversion,[],[f129]) ).
cnf(s11,plain,
( ~ spl22_1
| spl22_10 ),
inference(sat_conversion,[],[f134]) ).
cnf(s12,plain,
( ~ spl22_1
| spl22_11 ),
inference(sat_conversion,[],[f139]) ).
cnf(s13,plain,
( ~ spl22_1
| spl22_12 ),
inference(sat_conversion,[],[f144]) ).
cnf(s14,plain,
( ~ spl22_1
| spl22_13 ),
inference(sat_conversion,[],[f149]) ).
cnf(s15,plain,
( ~ spl22_1
| spl22_14 ),
inference(sat_conversion,[],[f154]) ).
cnf(s16,plain,
( ~ spl22_1
| ~ spl22_15 ),
inference(sat_conversion,[],[f159]) ).
cnf(s17,plain,
( ~ spl22_1
| spl22_16 ),
inference(sat_conversion,[],[f164]) ).
cnf(s18,plain,
( ~ spl22_1
| spl22_17 ),
inference(sat_conversion,[],[f169]) ).
cnf(s19,plain,
( ~ spl22_1
| spl22_18 ),
inference(sat_conversion,[],[f174]) ).
cnf(s20,plain,
( ~ spl22_1
| spl22_19 ),
inference(sat_conversion,[],[f179]) ).
cnf(s21,plain,
( ~ spl22_1
| spl22_20 ),
inference(sat_conversion,[],[f184]) ).
cnf(s22,plain,
( ~ spl22_1
| spl22_21 ),
inference(sat_conversion,[],[f189]) ).
cnf(s23,plain,
( ~ spl22_1
| spl22_22 ),
inference(sat_conversion,[],[f194]) ).
cnf(s24,plain,
( ~ spl22_1
| spl22_23 ),
inference(sat_conversion,[],[f199]) ).
cnf(s25,plain,
( ~ spl22_1
| spl22_24 ),
inference(sat_conversion,[],[f204]) ).
cnf(s26,plain,
( ~ spl22_1
| spl22_25 ),
inference(sat_conversion,[],[f209]) ).
cnf(s27,plain,
( ~ spl22_1
| spl22_26 ),
inference(sat_conversion,[],[f214]) ).
cnf(s28,plain,
( ~ spl22_1
| spl22_27 ),
inference(sat_conversion,[],[f219]) ).
cnf(s29,plain,
( ~ spl22_1
| spl22_28 ),
inference(sat_conversion,[],[f224]) ).
cnf(s30,plain,
( ~ spl22_1
| spl22_29 ),
inference(sat_conversion,[],[f229]) ).
cnf(s31,plain,
( ~ spl22_1
| spl22_30 ),
inference(sat_conversion,[],[f234]) ).
cnf(s32,plain,
( ~ spl22_1
| spl22_31 ),
inference(sat_conversion,[],[f239]) ).
cnf(s33,plain,
( ~ spl22_1
| spl22_32 ),
inference(sat_conversion,[],[f244]) ).
cnf(s34,plain,
( ~ spl22_1
| spl22_33 ),
inference(sat_conversion,[],[f249]) ).
cnf(s35,plain,
( ~ spl22_1
| spl22_34 ),
inference(sat_conversion,[],[f254]) ).
cnf(s36,plain,
( ~ spl22_1
| spl22_35 ),
inference(sat_conversion,[],[f259]) ).
cnf(s37,plain,
( ~ spl22_2
| spl22_36 ),
inference(sat_conversion,[],[f264]) ).
cnf(s38,plain,
( ~ spl22_2
| spl22_37 ),
inference(sat_conversion,[],[f269]) ).
cnf(s39,plain,
( ~ spl22_2
| spl22_38 ),
inference(sat_conversion,[],[f274]) ).
cnf(s40,plain,
( ~ spl22_2
| spl22_39 ),
inference(sat_conversion,[],[f279]) ).
cnf(s41,plain,
( ~ spl22_2
| spl22_40 ),
inference(sat_conversion,[],[f284]) ).
cnf(s42,plain,
( ~ spl22_2
| spl22_41 ),
inference(sat_conversion,[],[f289]) ).
cnf(s43,plain,
( ~ spl22_2
| spl22_42 ),
inference(sat_conversion,[],[f294]) ).
cnf(s44,plain,
( ~ spl22_2
| spl22_43 ),
inference(sat_conversion,[],[f299]) ).
cnf(s45,plain,
( ~ spl22_2
| spl22_44 ),
inference(sat_conversion,[],[f304]) ).
cnf(s46,plain,
( ~ spl22_2
| spl22_45 ),
inference(sat_conversion,[],[f309]) ).
cnf(s47,plain,
( ~ spl22_2
| ~ spl22_46 ),
inference(sat_conversion,[],[f314]) ).
cnf(s48,plain,
( ~ spl22_2
| spl22_47 ),
inference(sat_conversion,[],[f319]) ).
cnf(s49,plain,
( ~ spl22_2
| spl22_48 ),
inference(sat_conversion,[],[f324]) ).
cnf(s50,plain,
( ~ spl22_2
| spl22_49 ),
inference(sat_conversion,[],[f329]) ).
cnf(s51,plain,
( ~ spl22_2
| spl22_50 ),
inference(sat_conversion,[],[f334]) ).
cnf(s52,plain,
( ~ spl22_2
| spl22_51 ),
inference(sat_conversion,[],[f339]) ).
cnf(s53,plain,
( ~ spl22_2
| spl22_52 ),
inference(sat_conversion,[],[f344]) ).
cnf(s54,plain,
( ~ spl22_2
| spl22_53 ),
inference(sat_conversion,[],[f349]) ).
cnf(s55,plain,
( ~ spl22_2
| spl22_54 ),
inference(sat_conversion,[],[f354]) ).
cnf(s56,plain,
( ~ spl22_2
| spl22_55 ),
inference(sat_conversion,[],[f359]) ).
cnf(s57,plain,
( ~ spl22_2
| spl22_56 ),
inference(sat_conversion,[],[f364]) ).
cnf(s58,plain,
( ~ spl22_2
| spl22_57 ),
inference(sat_conversion,[],[f369]) ).
cnf(s59,plain,
( ~ spl22_2
| spl22_58 ),
inference(sat_conversion,[],[f374]) ).
cnf(s60,plain,
( ~ spl22_2
| spl22_59 ),
inference(sat_conversion,[],[f379]) ).
cnf(s61,plain,
( ~ spl22_2
| spl22_60 ),
inference(sat_conversion,[],[f384]) ).
cnf(s62,plain,
( ~ spl22_2
| spl22_61 ),
inference(sat_conversion,[],[f389]) ).
cnf(s63,plain,
( ~ spl22_2
| spl22_62 ),
inference(sat_conversion,[],[f394]) ).
cnf(s64,plain,
( ~ spl22_2
| spl22_63 ),
inference(sat_conversion,[],[f399]) ).
cnf(s65,plain,
( ~ spl22_2
| spl22_64 ),
inference(sat_conversion,[],[f404]) ).
cnf(s66,plain,
( ~ spl22_2
| spl22_65 ),
inference(sat_conversion,[],[f409]) ).
cnf(s67,plain,
( ~ spl22_2
| spl22_66 ),
inference(sat_conversion,[],[f414]) ).
cnf(s68,plain,
( ~ spl22_3
| ~ spl22_50
| ~ spl22_51
| ~ spl22_52
| ~ spl22_53
| ~ spl22_54
| spl22_67 ),
inference(sat_conversion,[],[f419]) ).
cnf(s69,plain,
( ~ spl22_3
| ~ spl22_22
| ~ spl22_23
| ~ spl22_24
| ~ spl22_25
| ~ spl22_26
| spl22_68 ),
inference(sat_conversion,[],[f424]) ).
cnf(s70,plain,
( ~ spl22_18
| ~ spl22_27
| ~ spl22_68
| spl22_69
| spl22_70 ),
inference(sat_conversion,[],[f435]) ).
cnf(s71,plain,
( ~ spl22_16
| ~ spl22_28
| ~ spl22_29
| ~ spl22_70 ),
inference(sat_conversion,[],[f439]) ).
cnf(s72,plain,
( ~ spl22_17
| ~ spl22_19
| ~ spl22_20
| ~ spl22_21
| ~ spl22_69 ),
inference(sat_conversion,[],[f444]) ).
cnf(s73,plain,
( ~ spl22_49
| ~ spl22_58
| ~ spl22_67
| spl22_71
| spl22_72 ),
inference(sat_conversion,[],[f455]) ).
cnf(s74,plain,
( ~ spl22_48
| ~ spl22_55
| ~ spl22_56
| ~ spl22_57
| ~ spl22_71 ),
inference(sat_conversion,[],[f460]) ).
cnf(s75,plain,
( ~ spl22_47
| ~ spl22_59
| ~ spl22_60
| ~ spl22_72 ),
inference(sat_conversion,[],[f464]) ).
cnf(s76,plain,
( ~ spl22_4
| ~ spl22_9
| ~ spl22_10
| ~ spl22_11
| spl22_73
| spl22_74 ),
inference(sat_conversion,[],[f485]) ).
cnf(s81,plain,
( ~ spl22_5
| ~ spl22_6
| ~ spl22_30
| ~ spl22_31
| ~ spl22_32
| ~ spl22_74 ),
inference(sat_conversion,[],[f514]) ).
cnf(s83,plain,
( ~ spl22_38
| ~ spl22_39
| ~ spl22_43
| ~ spl22_44
| ~ spl22_45
| spl22_46
| ~ spl22_64
| ~ spl22_65
| ~ spl22_66
| ~ spl22_77 ),
inference(sat_conversion,[],[f591]) ).
cnf(s85,plain,
( ~ spl22_36
| ~ spl22_37
| ~ spl22_61
| ~ spl22_62
| ~ spl22_63
| ~ spl22_78 ),
inference(sat_conversion,[],[f601]) ).
cnf(s86,plain,
( ~ spl22_4
| ~ spl22_40
| ~ spl22_41
| ~ spl22_42
| spl22_77
| spl22_78 ),
inference(sat_conversion,[],[f602]) ).
cnf(s91,plain,
( ~ spl22_12
| ~ spl22_13
| ~ spl22_14
| spl22_15
| ~ spl22_73
| spl22_76 ),
inference(sat_conversion,[],[f654]) ).
cnf(s92,plain,
( ~ spl22_7
| ~ spl22_8
| ~ spl22_33
| ~ spl22_34
| ~ spl22_35
| ~ spl22_76 ),
inference(sat_conversion,[],[f664]) ).
cnf(s93,plain,
~ spl22_2,
inference(rat,[],[s5,s68,s86,s73,s85,s83,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(s94,plain,
spl22_1,
inference(rat,[],[s1,s93]) ).
cnf(s95,plain,
spl22_35,
inference(rat,[],[s36,s94]) ).
cnf(s96,plain,
spl22_34,
inference(rat,[],[s35,s94]) ).
cnf(s97,plain,
spl22_33,
inference(rat,[],[s34,s94]) ).
cnf(s98,plain,
spl22_32,
inference(rat,[],[s33,s94]) ).
cnf(s99,plain,
spl22_31,
inference(rat,[],[s32,s94]) ).
cnf(s100,plain,
spl22_30,
inference(rat,[],[s31,s94]) ).
cnf(s101,plain,
spl22_29,
inference(rat,[],[s30,s94]) ).
cnf(s102,plain,
spl22_28,
inference(rat,[],[s29,s94]) ).
cnf(s103,plain,
spl22_27,
inference(rat,[],[s28,s94]) ).
cnf(s104,plain,
spl22_26,
inference(rat,[],[s27,s94]) ).
cnf(s105,plain,
spl22_25,
inference(rat,[],[s26,s94]) ).
cnf(s106,plain,
spl22_24,
inference(rat,[],[s25,s94]) ).
cnf(s107,plain,
spl22_23,
inference(rat,[],[s24,s94]) ).
cnf(s108,plain,
spl22_22,
inference(rat,[],[s23,s94]) ).
cnf(s109,plain,
spl22_21,
inference(rat,[],[s22,s94]) ).
cnf(s110,plain,
spl22_20,
inference(rat,[],[s21,s94]) ).
cnf(s111,plain,
spl22_19,
inference(rat,[],[s20,s94]) ).
cnf(s112,plain,
spl22_18,
inference(rat,[],[s19,s94]) ).
cnf(s113,plain,
spl22_17,
inference(rat,[],[s18,s94]) ).
cnf(s114,plain,
spl22_16,
inference(rat,[],[s17,s94]) ).
cnf(s115,plain,
~ spl22_15,
inference(rat,[],[s16,s94]) ).
cnf(s116,plain,
spl22_14,
inference(rat,[],[s15,s94]) ).
cnf(s117,plain,
spl22_13,
inference(rat,[],[s14,s94]) ).
cnf(s118,plain,
spl22_12,
inference(rat,[],[s13,s94]) ).
cnf(s119,plain,
spl22_11,
inference(rat,[],[s12,s94]) ).
cnf(s120,plain,
spl22_10,
inference(rat,[],[s11,s94]) ).
cnf(s121,plain,
spl22_9,
inference(rat,[],[s10,s94]) ).
cnf(s122,plain,
spl22_8,
inference(rat,[],[s9,s94]) ).
cnf(s123,plain,
spl22_7,
inference(rat,[],[s8,s94]) ).
cnf(s124,plain,
spl22_6,
inference(rat,[],[s7,s94]) ).
cnf(s125,plain,
spl22_5,
inference(rat,[],[s6,s94]) ).
cnf(s126,plain,
~ spl22_69,
inference(rat,[],[s72,s111,s109,s110,s113]) ).
cnf(s127,plain,
~ spl22_70,
inference(rat,[],[s71,s102,s101,s114]) ).
cnf(s128,plain,
~ spl22_76,
inference(rat,[],[s92,s122,s95,s96,s97,s123]) ).
cnf(s129,plain,
~ spl22_74,
inference(rat,[],[s81,s124,s98,s99,s100,s125]) ).
cnf(s130,plain,
~ spl22_68,
inference(rat,[],[s70,s127,s112,s103,s126]) ).
cnf(s131,plain,
~ spl22_73,
inference(rat,[],[s91,s118,s117,s115,s116,s128]) ).
cnf(s132,plain,
~ spl22_3,
inference(rat,[],[s69,s108,s104,s105,s106,s107,s130]) ).
cnf(s133,plain,
~ spl22_4,
inference(rat,[],[s76,s129,s121,s119,s120,s131]) ).
cnf(s134,plain,
$false,
inference(rat,[],[s5,s133,s132]) ).
fof(f665,plain,
$false,
inference(avatar_sat_refutation,[],[s134]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP004+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n002.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 17:49:07 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.40 Running first-order theorem proving
% 0.11/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.77/1.30 % (3775721)Detected formulas, will run a generic FOF schedule.
% 2.77/1.30 % (3775728)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1857171784:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.77/1.30 % (3775730)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2483119209:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.77/1.30 % (3775729)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1974758750:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.77/1.30 % (3775731)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4127158668:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.77/1.30 % (3775727)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2291861660:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.77/1.30 % (3775726)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=539876349:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.77/1.30 % (3775732)dis-21_1_sil=8000:lcm=predicate:random_seed=2889456197:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 2.77/1.30 % (3775732)Refutation not found, incomplete strategy
% 2.77/1.30 % (3775732)------------------------------
% 2.77/1.30 % (3775732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.77/1.30 % (3775732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.77/1.30 % (3775732)CaDiCaL version: 2.1.3
% 2.77/1.30 % (3775732)Termination reason: Refutation not found, incomplete strategy
% 2.77/1.30 % (3775732)Time elapsed: 0.004 s
% 2.77/1.30 % (3775732)Peak memory usage: 88 MB
% 2.77/1.30 % (3775732)Instructions burned: 5 (million)
% 2.77/1.30 % (3775729)Refutation not found, incomplete strategy
% 2.77/1.30 % (3775729)------------------------------
% 2.77/1.30 % (3775729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.77/1.30 % (3775729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.77/1.30 % (3775729)CaDiCaL version: 2.1.3
% 2.77/1.30 % (3775729)Termination reason: Refutation not found, incomplete strategy
% 2.77/1.30 % (3775729)Time elapsed: 0.008 s
% 2.77/1.30 % (3775729)Peak memory usage: 88 MB
% 2.77/1.30 % (3775729)Instructions burned: 13 (million)
% 2.77/1.30 % (3775731)First to succeed.
% 2.77/1.30 % (3775731)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3775721"
% 2.77/1.30 % (3775730)Instruction limit reached!
% 2.77/1.30 % (3775730)------------------------------
% 2.77/1.30 % (3775730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.77/1.30 % (3775730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.77/1.30 % (3775730)CaDiCaL version: 2.1.3
% 2.77/1.30 % (3775730)Termination reason: Instruction limit
% 2.77/1.30 % (3775730)Termination phase: Saturation
% 2.77/1.30 % (3775730)Time elapsed: 0.043 s
% 2.77/1.30 % (3775730)Peak memory usage: 88 MB
% 2.77/1.30 % (3775730)Instructions burned: 121 (million)
% 2.77/1.30 % (3775740)lrs+10_1_sil=8000:sp=occurrence:random_seed=2804922128:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 2.77/1.30 % (3775740)Also succeeded, but the first one will report.
% 2.77/1.30 % (3775729)------------------------------
% 2.77/1.30 % (3775729)------------------------------
% 2.77/1.30 % (3775732)------------------------------
% 2.77/1.30 % (3775732)------------------------------
% 2.77/1.30 % (3775731)Refutation found. Thanks to Tanya!
% 2.77/1.30 % SZS status Theorem for theBenchmark
% 2.77/1.30 % SZS output start Proof for theBenchmark
% See solution above
% 3.72/1.49 % (3775731)------------------------------
% 3.72/1.49 % (3775731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.72/1.49 % (3775731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.72/1.49 % (3775731)CaDiCaL version: 2.1.3
% 3.72/1.49 % (3775731)Termination reason: Refutation
% 3.72/1.49 % (3775731)Time elapsed: 0.016 s
% 3.72/1.49 % (3775731)Peak memory usage: 90 MB
% 3.72/1.49 % (3775731)Instructions burned: 23 (million)
% 3.72/1.49 % (3775731)------------------------------
% 3.72/1.49 % (3775731)------------------------------
% 3.72/1.49 % (3775721)Success in time 0.455 s
% 3.72/1.49 % Vampire exiting
%------------------------------------------------------------------------------