%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NLP007+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n026.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:54 PM UTC 2026
% Result : Theorem 2.44s 1.30s
% Output : Refutation 3.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 81
% Syntax : Number of formulae : 488 ( 43 unt; 80 def)
% Number of atoms : 2552 ( 124 equ)
% Maximal formula atoms : 124 ( 5 avg)
% Number of connectives : 3602 (1538 ~;1464 |; 518 &)
% ( 78 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 83 ( 6 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 102 ( 100 usr; 81 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 20 con; 0-0 aty)
% Number of variables : 389 ( 0 sgn 239 !; 150 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
( ( ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( seat(X0)
& furniture(X0)
& front(X0)
& hollywood(X1)
& city(X1)
& event(X2)
& chevy(X3)
& car(X3)
& white(X3)
& dirty(X3)
& old(X3)
& street(X4)
& way(X4)
& lonely(X4)
& barrel(X2,X3)
& down(X2,X4)
& in(X2,X1)
& seat(X7)
& furniture(X7)
& front(X7)
& X5 != X6
& fellow(X5)
& man(X5)
& young(X5)
& fellow(X6)
& man(X6)
& young(X6)
& X5 = X8
& in(X8,X7)
& X6 = X9
& in(X9,X0) )
=> ? [X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
( seat(X10)
& furniture(X10)
& front(X10)
& hollywood(X11)
& city(X11)
& event(X12)
& chevy(X13)
& car(X13)
& white(X13)
& dirty(X13)
& old(X13)
& street(X14)
& way(X14)
& lonely(X14)
& barrel(X12,X13)
& down(X12,X14)
& in(X12,X11)
& seat(X17)
& furniture(X17)
& front(X17)
& X15 != X16
& fellow(X15)
& man(X15)
& young(X15)
& fellow(X16)
& man(X16)
& young(X16)
& X15 = X18
& in(X18,X10)
& X16 = X19
& in(X19,X17) ) )
& ( ? [X20,X21,X22,X23,X24,X25,X26,X27,X28,X29] :
( seat(X20)
& furniture(X20)
& front(X20)
& hollywood(X21)
& city(X21)
& event(X22)
& chevy(X23)
& car(X23)
& white(X23)
& dirty(X23)
& old(X23)
& street(X24)
& way(X24)
& lonely(X24)
& barrel(X22,X23)
& down(X22,X24)
& in(X22,X21)
& seat(X27)
& furniture(X27)
& front(X27)
& X25 != X26
& fellow(X25)
& man(X25)
& young(X25)
& fellow(X26)
& man(X26)
& young(X26)
& X25 = X28
& in(X28,X20)
& X26 = X29
& in(X29,X27) )
=> ? [X30,X31,X32,X33,X34,X35,X36,X37,X38,X39] :
( seat(X30)
& furniture(X30)
& front(X30)
& hollywood(X31)
& city(X31)
& event(X32)
& chevy(X33)
& car(X33)
& white(X33)
& dirty(X33)
& old(X33)
& street(X34)
& way(X34)
& lonely(X34)
& barrel(X32,X33)
& down(X32,X34)
& in(X32,X31)
& seat(X37)
& furniture(X37)
& front(X37)
& X35 != X36
& fellow(X35)
& man(X35)
& young(X35)
& fellow(X36)
& man(X36)
& young(X36)
& X35 = X38
& in(X38,X37)
& X36 = X39
& in(X39,X30) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f2,negated_conjecture,
~ ( ( ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( seat(X0)
& furniture(X0)
& front(X0)
& hollywood(X1)
& city(X1)
& event(X2)
& chevy(X3)
& car(X3)
& white(X3)
& dirty(X3)
& old(X3)
& street(X4)
& way(X4)
& lonely(X4)
& barrel(X2,X3)
& down(X2,X4)
& in(X2,X1)
& seat(X7)
& furniture(X7)
& front(X7)
& X5 != X6
& fellow(X5)
& man(X5)
& young(X5)
& fellow(X6)
& man(X6)
& young(X6)
& X5 = X8
& in(X8,X7)
& X6 = X9
& in(X9,X0) )
=> ? [X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
( seat(X10)
& furniture(X10)
& front(X10)
& hollywood(X11)
& city(X11)
& event(X12)
& chevy(X13)
& car(X13)
& white(X13)
& dirty(X13)
& old(X13)
& street(X14)
& way(X14)
& lonely(X14)
& barrel(X12,X13)
& down(X12,X14)
& in(X12,X11)
& seat(X17)
& furniture(X17)
& front(X17)
& X15 != X16
& fellow(X15)
& man(X15)
& young(X15)
& fellow(X16)
& man(X16)
& young(X16)
& X15 = X18
& in(X18,X10)
& X16 = X19
& in(X19,X17) ) )
& ( ? [X20,X21,X22,X23,X24,X25,X26,X27,X28,X29] :
( seat(X20)
& furniture(X20)
& front(X20)
& hollywood(X21)
& city(X21)
& event(X22)
& chevy(X23)
& car(X23)
& white(X23)
& dirty(X23)
& old(X23)
& street(X24)
& way(X24)
& lonely(X24)
& barrel(X22,X23)
& down(X22,X24)
& in(X22,X21)
& seat(X27)
& furniture(X27)
& front(X27)
& X25 != X26
& fellow(X25)
& man(X25)
& young(X25)
& fellow(X26)
& man(X26)
& young(X26)
& X25 = X28
& in(X28,X20)
& X26 = X29
& in(X29,X27) )
=> ? [X30,X31,X32,X33,X34,X35,X36,X37,X38,X39] :
( seat(X30)
& furniture(X30)
& front(X30)
& hollywood(X31)
& city(X31)
& event(X32)
& chevy(X33)
& car(X33)
& white(X33)
& dirty(X33)
& old(X33)
& street(X34)
& way(X34)
& lonely(X34)
& barrel(X32,X33)
& down(X32,X34)
& in(X32,X31)
& seat(X37)
& furniture(X37)
& front(X37)
& X35 != X36
& fellow(X35)
& man(X35)
& young(X35)
& fellow(X36)
& man(X36)
& young(X36)
& X35 = X38
& in(X38,X37)
& X36 = X39
& in(X39,X30) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
( ( ! [X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
( ~ seat(X10)
| ~ furniture(X10)
| ~ front(X10)
| ~ hollywood(X11)
| ~ city(X11)
| ~ event(X12)
| ~ chevy(X13)
| ~ car(X13)
| ~ white(X13)
| ~ dirty(X13)
| ~ old(X13)
| ~ street(X14)
| ~ way(X14)
| ~ lonely(X14)
| ~ barrel(X12,X13)
| ~ down(X12,X14)
| ~ in(X12,X11)
| ~ seat(X17)
| ~ furniture(X17)
| ~ front(X17)
| X15 = X16
| ~ fellow(X15)
| ~ man(X15)
| ~ young(X15)
| ~ fellow(X16)
| ~ man(X16)
| ~ young(X16)
| X15 != X18
| ~ in(X18,X10)
| X16 != X19
| ~ in(X19,X17) )
& ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( seat(X0)
& furniture(X0)
& front(X0)
& hollywood(X1)
& city(X1)
& event(X2)
& chevy(X3)
& car(X3)
& white(X3)
& dirty(X3)
& old(X3)
& street(X4)
& way(X4)
& lonely(X4)
& barrel(X2,X3)
& down(X2,X4)
& in(X2,X1)
& seat(X7)
& furniture(X7)
& front(X7)
& X5 != X6
& fellow(X5)
& man(X5)
& young(X5)
& fellow(X6)
& man(X6)
& young(X6)
& X5 = X8
& in(X8,X7)
& X6 = X9
& in(X9,X0) ) )
| ( ! [X30,X31,X32,X33,X34,X35,X36,X37,X38,X39] :
( ~ seat(X30)
| ~ furniture(X30)
| ~ front(X30)
| ~ hollywood(X31)
| ~ city(X31)
| ~ event(X32)
| ~ chevy(X33)
| ~ car(X33)
| ~ white(X33)
| ~ dirty(X33)
| ~ old(X33)
| ~ street(X34)
| ~ way(X34)
| ~ lonely(X34)
| ~ barrel(X32,X33)
| ~ down(X32,X34)
| ~ in(X32,X31)
| ~ seat(X37)
| ~ furniture(X37)
| ~ front(X37)
| X35 = X36
| ~ fellow(X35)
| ~ man(X35)
| ~ young(X35)
| ~ fellow(X36)
| ~ man(X36)
| ~ young(X36)
| X35 != X38
| ~ in(X38,X37)
| X36 != X39
| ~ in(X39,X30) )
& ? [X20,X21,X22,X23,X24,X25,X26,X27,X28,X29] :
( seat(X20)
& furniture(X20)
& front(X20)
& hollywood(X21)
& city(X21)
& event(X22)
& chevy(X23)
& car(X23)
& white(X23)
& dirty(X23)
& old(X23)
& street(X24)
& way(X24)
& lonely(X24)
& barrel(X22,X23)
& down(X22,X24)
& in(X22,X21)
& seat(X27)
& furniture(X27)
& front(X27)
& X25 != X26
& fellow(X25)
& man(X25)
& young(X25)
& fellow(X26)
& man(X26)
& young(X26)
& X25 = X28
& in(X28,X20)
& X26 = X29
& in(X29,X27) ) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f4,definition,
( ? [X20,X21,X22,X23,X24,X25,X26,X27,X28,X29] :
( seat(X20)
& furniture(X20)
& front(X20)
& hollywood(X21)
& city(X21)
& event(X22)
& chevy(X23)
& car(X23)
& white(X23)
& dirty(X23)
& old(X23)
& street(X24)
& way(X24)
& lonely(X24)
& barrel(X22,X23)
& down(X22,X24)
& in(X22,X21)
& seat(X27)
& furniture(X27)
& front(X27)
& X25 != X26
& fellow(X25)
& man(X25)
& young(X25)
& fellow(X26)
& man(X26)
& young(X26)
& X25 = X28
& in(X28,X20)
& X26 = X29
& in(X29,X27) )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f5,definition,
( ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( seat(X0)
& furniture(X0)
& front(X0)
& hollywood(X1)
& city(X1)
& event(X2)
& chevy(X3)
& car(X3)
& white(X3)
& dirty(X3)
& old(X3)
& street(X4)
& way(X4)
& lonely(X4)
& barrel(X2,X3)
& down(X2,X4)
& in(X2,X1)
& seat(X7)
& furniture(X7)
& front(X7)
& X5 != X6
& fellow(X5)
& man(X5)
& young(X5)
& fellow(X6)
& man(X6)
& young(X6)
& X5 = X8
& in(X8,X7)
& X6 = X9
& in(X9,X0) )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f6,plain,
( ( ! [X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
( ~ seat(X10)
| ~ furniture(X10)
| ~ front(X10)
| ~ hollywood(X11)
| ~ city(X11)
| ~ event(X12)
| ~ chevy(X13)
| ~ car(X13)
| ~ white(X13)
| ~ dirty(X13)
| ~ old(X13)
| ~ street(X14)
| ~ way(X14)
| ~ lonely(X14)
| ~ barrel(X12,X13)
| ~ down(X12,X14)
| ~ in(X12,X11)
| ~ seat(X17)
| ~ furniture(X17)
| ~ front(X17)
| X15 = X16
| ~ fellow(X15)
| ~ man(X15)
| ~ young(X15)
| ~ fellow(X16)
| ~ man(X16)
| ~ young(X16)
| X15 != X18
| ~ in(X18,X10)
| X16 != X19
| ~ in(X19,X17) )
& sP1 )
| ( ! [X30,X31,X32,X33,X34,X35,X36,X37,X38,X39] :
( ~ seat(X30)
| ~ furniture(X30)
| ~ front(X30)
| ~ hollywood(X31)
| ~ city(X31)
| ~ event(X32)
| ~ chevy(X33)
| ~ car(X33)
| ~ white(X33)
| ~ dirty(X33)
| ~ old(X33)
| ~ street(X34)
| ~ way(X34)
| ~ lonely(X34)
| ~ barrel(X32,X33)
| ~ down(X32,X34)
| ~ in(X32,X31)
| ~ seat(X37)
| ~ furniture(X37)
| ~ front(X37)
| X35 = X36
| ~ fellow(X35)
| ~ man(X35)
| ~ young(X35)
| ~ fellow(X36)
| ~ man(X36)
| ~ young(X36)
| X35 != X38
| ~ in(X38,X37)
| X36 != X39
| ~ in(X39,X30) )
& sP0 ) ),
inference(definition_folding,[],[f3,f5,f4]) ).
fof(f7,plain,
( ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( seat(X0)
& furniture(X0)
& front(X0)
& hollywood(X1)
& city(X1)
& event(X2)
& chevy(X3)
& car(X3)
& white(X3)
& dirty(X3)
& old(X3)
& street(X4)
& way(X4)
& lonely(X4)
& barrel(X2,X3)
& down(X2,X4)
& in(X2,X1)
& seat(X7)
& furniture(X7)
& front(X7)
& X5 != X6
& fellow(X5)
& man(X5)
& young(X5)
& fellow(X6)
& man(X6)
& young(X6)
& X5 = X8
& in(X8,X7)
& X6 = X9
& in(X9,X0) )
| ~ sP1 ),
inference(nnf_transformation,[],[f5]) ).
fof(f8,plain,
( ( seat(sK2)
& furniture(sK2)
& front(sK2)
& hollywood(sK3)
& city(sK3)
& event(sK4)
& chevy(sK5)
& car(sK5)
& white(sK5)
& dirty(sK5)
& old(sK5)
& street(sK6)
& way(sK6)
& lonely(sK6)
& barrel(sK4,sK5)
& down(sK4,sK6)
& in(sK4,sK3)
& seat(sK9)
& furniture(sK9)
& front(sK9)
& sK7 != sK8
& fellow(sK7)
& man(sK7)
& young(sK7)
& fellow(sK8)
& man(sK8)
& young(sK8)
& sK7 = sK10
& in(sK10,sK9)
& sK8 = sK11
& in(sK11,sK2) )
| ~ sP1 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4),skolemize(X3,sK5),skolemize(X4,sK6),skolemize(X5,sK7),skolemize(X6,sK8),skolemize(X7,sK9),skolemize(X8,sK10),skolemize(X9,sK11)],[f7]) ).
fof(f9,plain,
( ? [X20,X21,X22,X23,X24,X25,X26,X27,X28,X29] :
( seat(X20)
& furniture(X20)
& front(X20)
& hollywood(X21)
& city(X21)
& event(X22)
& chevy(X23)
& car(X23)
& white(X23)
& dirty(X23)
& old(X23)
& street(X24)
& way(X24)
& lonely(X24)
& barrel(X22,X23)
& down(X22,X24)
& in(X22,X21)
& seat(X27)
& furniture(X27)
& front(X27)
& X25 != X26
& fellow(X25)
& man(X25)
& young(X25)
& fellow(X26)
& man(X26)
& young(X26)
& X25 = X28
& in(X28,X20)
& X26 = X29
& in(X29,X27) )
| ~ sP0 ),
inference(nnf_transformation,[],[f4]) ).
fof(f10,plain,
( ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( seat(X0)
& furniture(X0)
& front(X0)
& hollywood(X1)
& city(X1)
& event(X2)
& chevy(X3)
& car(X3)
& white(X3)
& dirty(X3)
& old(X3)
& street(X4)
& way(X4)
& lonely(X4)
& barrel(X2,X3)
& down(X2,X4)
& in(X2,X1)
& seat(X7)
& furniture(X7)
& front(X7)
& X5 != X6
& fellow(X5)
& man(X5)
& young(X5)
& fellow(X6)
& man(X6)
& young(X6)
& X5 = X8
& in(X8,X0)
& X6 = X9
& in(X9,X7) )
| ~ sP0 ),
inference(rectify,[],[f9]) ).
fof(f11,plain,
( ( seat(sK12)
& furniture(sK12)
& front(sK12)
& hollywood(sK13)
& city(sK13)
& event(sK14)
& chevy(sK15)
& car(sK15)
& white(sK15)
& dirty(sK15)
& old(sK15)
& street(sK16)
& way(sK16)
& lonely(sK16)
& barrel(sK14,sK15)
& down(sK14,sK16)
& in(sK14,sK13)
& seat(sK19)
& furniture(sK19)
& front(sK19)
& sK17 != sK18
& fellow(sK17)
& man(sK17)
& young(sK17)
& fellow(sK18)
& man(sK18)
& young(sK18)
& sK17 = sK20
& in(sK20,sK12)
& sK18 = sK21
& in(sK21,sK19) )
| ~ sP0 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12,sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21]),skolemize(X0,sK12),skolemize(X1,sK13),skolemize(X2,sK14),skolemize(X3,sK15),skolemize(X4,sK16),skolemize(X5,sK17),skolemize(X6,sK18),skolemize(X7,sK19),skolemize(X8,sK20),skolemize(X9,sK21)],[f10]) ).
fof(f12,plain,
( ( ! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ hollywood(X1)
| ~ city(X1)
| ~ event(X2)
| ~ chevy(X3)
| ~ car(X3)
| ~ white(X3)
| ~ dirty(X3)
| ~ old(X3)
| ~ street(X4)
| ~ way(X4)
| ~ lonely(X4)
| ~ barrel(X2,X3)
| ~ down(X2,X4)
| ~ in(X2,X1)
| ~ seat(X7)
| ~ furniture(X7)
| ~ front(X7)
| X5 = X6
| ~ fellow(X5)
| ~ man(X5)
| ~ young(X5)
| ~ fellow(X6)
| ~ man(X6)
| ~ young(X6)
| X5 != X8
| ~ in(X8,X0)
| X6 != X9
| ~ in(X9,X7) )
& sP1 )
| ( ! [X10,X11,X12,X13,X14,X15,X16,X17,X18,X19] :
( ~ seat(X10)
| ~ furniture(X10)
| ~ front(X10)
| ~ hollywood(X11)
| ~ city(X11)
| ~ event(X12)
| ~ chevy(X13)
| ~ car(X13)
| ~ white(X13)
| ~ dirty(X13)
| ~ old(X13)
| ~ street(X14)
| ~ way(X14)
| ~ lonely(X14)
| ~ barrel(X12,X13)
| ~ down(X12,X14)
| ~ in(X12,X11)
| ~ seat(X17)
| ~ furniture(X17)
| ~ front(X17)
| X15 = X16
| ~ fellow(X15)
| ~ man(X15)
| ~ young(X15)
| ~ fellow(X16)
| ~ man(X16)
| ~ young(X16)
| X15 != X18
| ~ in(X18,X17)
| X16 != X19
| ~ in(X19,X10) )
& sP0 ) ),
inference(rectify,[],[f6]) ).
fof(f13,plain,
( in(sK11,sK2)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f14,plain,
( sK8 = sK11
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f15,plain,
( in(sK10,sK9)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f16,plain,
( sK7 = sK10
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f17,plain,
( young(sK8)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f18,plain,
( man(sK8)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f19,plain,
( fellow(sK8)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f20,plain,
( young(sK7)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f21,plain,
( man(sK7)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f22,plain,
( fellow(sK7)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f23,plain,
( sK7 != sK8
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f24,plain,
( front(sK9)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f25,plain,
( furniture(sK9)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f26,plain,
( seat(sK9)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f27,plain,
( in(sK4,sK3)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f28,plain,
( down(sK4,sK6)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f29,plain,
( barrel(sK4,sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f30,plain,
( lonely(sK6)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f31,plain,
( way(sK6)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f32,plain,
( street(sK6)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f33,plain,
( old(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f34,plain,
( dirty(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f35,plain,
( white(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f36,plain,
( car(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f37,plain,
( chevy(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f38,plain,
( event(sK4)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f39,plain,
( city(sK3)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f40,plain,
( hollywood(sK3)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f41,plain,
( front(sK2)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f42,plain,
( furniture(sK2)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f43,plain,
( seat(sK2)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f44,plain,
( in(sK21,sK19)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f45,plain,
( sK18 = sK21
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f46,plain,
( in(sK20,sK12)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f47,plain,
( sK17 = sK20
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f48,plain,
( young(sK18)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f49,plain,
( man(sK18)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f50,plain,
( fellow(sK18)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f51,plain,
( young(sK17)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f52,plain,
( man(sK17)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f53,plain,
( fellow(sK17)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f54,plain,
( sK17 != sK18
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f55,plain,
( front(sK19)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f56,plain,
( furniture(sK19)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f57,plain,
( seat(sK19)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f58,plain,
( in(sK14,sK13)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f59,plain,
( down(sK14,sK16)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f60,plain,
( barrel(sK14,sK15)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f61,plain,
( lonely(sK16)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f62,plain,
( way(sK16)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f63,plain,
( street(sK16)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f64,plain,
( old(sK15)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f65,plain,
( dirty(sK15)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f66,plain,
( white(sK15)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f67,plain,
( car(sK15)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f68,plain,
( chevy(sK15)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f69,plain,
( event(sK14)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f70,plain,
( city(sK13)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f71,plain,
( hollywood(sK13)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f72,plain,
( front(sK12)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f73,plain,
( furniture(sK12)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f74,plain,
( seat(sK12)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f75,plain,
( sP1
| sP0 ),
inference(cnf_transformation,[],[f12]) ).
fof(f78,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X5,X12,X13] :
( ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ hollywood(X1)
| ~ city(X1)
| ~ event(X2)
| ~ chevy(X3)
| ~ car(X3)
| ~ white(X3)
| ~ dirty(X3)
| ~ old(X3)
| ~ street(X4)
| ~ way(X4)
| ~ lonely(X4)
| ~ barrel(X2,X3)
| ~ down(X2,X4)
| ~ in(X2,X1)
| ~ seat(X7)
| ~ furniture(X7)
| ~ front(X7)
| X5 = X6
| ~ fellow(X5)
| ~ man(X5)
| ~ young(X5)
| ~ fellow(X6)
| ~ man(X6)
| ~ young(X6)
| X5 != X8
| ~ in(X8,X0)
| X6 != X9
| ~ in(X9,X7)
| ~ seat(X10)
| ~ furniture(X10)
| ~ front(X10)
| ~ hollywood(X11)
| ~ city(X11)
| ~ event(X12)
| ~ chevy(X13)
| ~ car(X13)
| ~ white(X13)
| ~ dirty(X13)
| ~ old(X13)
| ~ street(X14)
| ~ way(X14)
| ~ lonely(X14)
| ~ barrel(X12,X13)
| ~ down(X12,X14)
| ~ in(X12,X11)
| ~ seat(X17)
| ~ furniture(X17)
| ~ front(X17)
| X15 = X16
| ~ fellow(X15)
| ~ man(X15)
| ~ young(X15)
| ~ fellow(X16)
| ~ man(X16)
| ~ young(X16)
| X15 != X18
| ~ in(X18,X17)
| X16 != X19
| ~ in(X19,X10) ),
inference(cnf_transformation,[],[f12]) ).
fof(f79,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X18,X19,X17,X15,X12,X13] :
( ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ hollywood(X1)
| ~ city(X1)
| ~ event(X2)
| ~ chevy(X3)
| ~ car(X3)
| ~ white(X3)
| ~ dirty(X3)
| ~ old(X3)
| ~ street(X4)
| ~ way(X4)
| ~ lonely(X4)
| ~ barrel(X2,X3)
| ~ down(X2,X4)
| ~ in(X2,X1)
| ~ seat(X7)
| ~ furniture(X7)
| ~ front(X7)
| X6 = X8
| ~ fellow(X8)
| ~ man(X8)
| ~ young(X8)
| ~ fellow(X6)
| ~ man(X6)
| ~ young(X6)
| ~ in(X8,X0)
| X6 != X9
| ~ in(X9,X7)
| ~ seat(X10)
| ~ furniture(X10)
| ~ front(X10)
| ~ hollywood(X11)
| ~ city(X11)
| ~ event(X12)
| ~ chevy(X13)
| ~ car(X13)
| ~ white(X13)
| ~ dirty(X13)
| ~ old(X13)
| ~ street(X14)
| ~ way(X14)
| ~ lonely(X14)
| ~ barrel(X12,X13)
| ~ down(X12,X14)
| ~ in(X12,X11)
| ~ seat(X17)
| ~ furniture(X17)
| ~ front(X17)
| X15 = X16
| ~ fellow(X15)
| ~ man(X15)
| ~ young(X15)
| ~ fellow(X16)
| ~ man(X16)
| ~ young(X16)
| X15 != X18
| ~ in(X18,X17)
| X16 != X19
| ~ in(X19,X10) ),
inference(equality_resolution,[],[f78]) ).
fof(f80,plain,
! [X2,X3,X10,X0,X11,X1,X8,X18,X9,X7,X14,X4,X16,X19,X17,X15,X12,X13] :
( ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ hollywood(X1)
| ~ city(X1)
| ~ event(X2)
| ~ chevy(X3)
| ~ car(X3)
| ~ white(X3)
| ~ dirty(X3)
| ~ old(X3)
| ~ street(X4)
| ~ way(X4)
| ~ lonely(X4)
| ~ barrel(X2,X3)
| ~ down(X2,X4)
| ~ in(X2,X1)
| ~ seat(X7)
| ~ furniture(X7)
| ~ front(X7)
| X8 = X9
| ~ fellow(X8)
| ~ man(X8)
| ~ young(X8)
| ~ fellow(X9)
| ~ man(X9)
| ~ young(X9)
| ~ in(X8,X0)
| ~ in(X9,X7)
| ~ seat(X10)
| ~ furniture(X10)
| ~ front(X10)
| ~ hollywood(X11)
| ~ city(X11)
| ~ event(X12)
| ~ chevy(X13)
| ~ car(X13)
| ~ white(X13)
| ~ dirty(X13)
| ~ old(X13)
| ~ street(X14)
| ~ way(X14)
| ~ lonely(X14)
| ~ barrel(X12,X13)
| ~ down(X12,X14)
| ~ in(X12,X11)
| ~ seat(X17)
| ~ furniture(X17)
| ~ front(X17)
| X15 = X16
| ~ fellow(X15)
| ~ man(X15)
| ~ young(X15)
| ~ fellow(X16)
| ~ man(X16)
| ~ young(X16)
| X15 != X18
| ~ in(X18,X17)
| X16 != X19
| ~ in(X19,X10) ),
inference(equality_resolution,[],[f79]) ).
fof(f81,plain,
! [X2,X3,X10,X0,X11,X1,X8,X18,X9,X7,X14,X4,X16,X19,X17,X12,X13] :
( ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ hollywood(X1)
| ~ city(X1)
| ~ event(X2)
| ~ chevy(X3)
| ~ car(X3)
| ~ white(X3)
| ~ dirty(X3)
| ~ old(X3)
| ~ street(X4)
| ~ way(X4)
| ~ lonely(X4)
| ~ barrel(X2,X3)
| ~ down(X2,X4)
| ~ in(X2,X1)
| ~ seat(X7)
| ~ furniture(X7)
| ~ front(X7)
| X8 = X9
| ~ fellow(X8)
| ~ man(X8)
| ~ young(X8)
| ~ fellow(X9)
| ~ man(X9)
| ~ young(X9)
| ~ in(X8,X0)
| ~ in(X9,X7)
| ~ seat(X10)
| ~ furniture(X10)
| ~ front(X10)
| ~ hollywood(X11)
| ~ city(X11)
| ~ event(X12)
| ~ chevy(X13)
| ~ car(X13)
| ~ white(X13)
| ~ dirty(X13)
| ~ old(X13)
| ~ street(X14)
| ~ way(X14)
| ~ lonely(X14)
| ~ barrel(X12,X13)
| ~ down(X12,X14)
| ~ in(X12,X11)
| ~ seat(X17)
| ~ furniture(X17)
| ~ front(X17)
| X16 = X18
| ~ fellow(X18)
| ~ man(X18)
| ~ young(X18)
| ~ fellow(X16)
| ~ man(X16)
| ~ young(X16)
| ~ in(X18,X17)
| X16 != X19
| ~ in(X19,X10) ),
inference(equality_resolution,[],[f80]) ).
fof(f82,plain,
! [X2,X3,X10,X0,X11,X1,X8,X18,X9,X7,X14,X4,X19,X17,X12,X13] :
( ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ hollywood(X1)
| ~ city(X1)
| ~ event(X2)
| ~ chevy(X3)
| ~ car(X3)
| ~ white(X3)
| ~ dirty(X3)
| ~ old(X3)
| ~ street(X4)
| ~ way(X4)
| ~ lonely(X4)
| ~ barrel(X2,X3)
| ~ down(X2,X4)
| ~ in(X2,X1)
| ~ seat(X7)
| ~ furniture(X7)
| ~ front(X7)
| X8 = X9
| ~ fellow(X8)
| ~ man(X8)
| ~ young(X8)
| ~ fellow(X9)
| ~ man(X9)
| ~ young(X9)
| ~ in(X8,X0)
| ~ in(X9,X7)
| ~ seat(X10)
| ~ furniture(X10)
| ~ front(X10)
| ~ hollywood(X11)
| ~ city(X11)
| ~ event(X12)
| ~ chevy(X13)
| ~ car(X13)
| ~ white(X13)
| ~ dirty(X13)
| ~ old(X13)
| ~ street(X14)
| ~ way(X14)
| ~ lonely(X14)
| ~ barrel(X12,X13)
| ~ down(X12,X14)
| ~ in(X12,X11)
| ~ seat(X17)
| ~ furniture(X17)
| ~ front(X17)
| X18 = X19
| ~ fellow(X18)
| ~ man(X18)
| ~ young(X18)
| ~ fellow(X19)
| ~ man(X19)
| ~ young(X19)
| ~ in(X18,X17)
| ~ in(X19,X10) ),
inference(equality_resolution,[],[f81]) ).
fof(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
<=> ! [X11,X13,X14,X12] :
( ~ hollywood(X11)
| ~ event(X12)
| ~ in(X12,X11)
| ~ down(X12,X14)
| ~ barrel(X12,X13)
| ~ street(X14)
| ~ lonely(X14)
| ~ way(X14)
| ~ chevy(X13)
| ~ old(X13)
| ~ dirty(X13)
| ~ white(X13)
| ~ car(X13)
| ~ city(X11) ) ),
introduced(definition,[new_symbols(definition,[spl22_3])],[avatar_definition]) ).
fof(f98,plain,
( ! [X11,X14,X12,X13] :
( ~ lonely(X14)
| ~ event(X12)
| ~ in(X12,X11)
| ~ down(X12,X14)
| ~ barrel(X12,X13)
| ~ street(X14)
| ~ hollywood(X11)
| ~ way(X14)
| ~ chevy(X13)
| ~ old(X13)
| ~ dirty(X13)
| ~ white(X13)
| ~ car(X13)
| ~ city(X11) )
| ~ spl22_3 ),
inference(avatar_component_clause,[],[f97]) ).
fof(f100,definition,
( spl22_4
<=> ! [X18,X17,X10,X19] :
( ~ seat(X10)
| ~ seat(X17)
| ~ in(X19,X10)
| X18 = X19
| ~ in(X18,X17)
| ~ young(X19)
| ~ man(X19)
| ~ fellow(X19)
| ~ young(X18)
| ~ man(X18)
| ~ fellow(X18)
| ~ front(X17)
| ~ furniture(X17)
| ~ front(X10)
| ~ furniture(X10) ) ),
introduced(definition,[new_symbols(definition,[spl22_4])],[avatar_definition]) ).
fof(f101,plain,
( ! [X10,X18,X19,X17] :
( ~ young(X19)
| ~ seat(X17)
| ~ in(X19,X10)
| X18 = X19
| ~ in(X18,X17)
| ~ seat(X10)
| ~ man(X19)
| ~ fellow(X19)
| ~ young(X18)
| ~ man(X18)
| ~ fellow(X18)
| ~ front(X17)
| ~ furniture(X17)
| ~ 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,sK19) ),
introduced(definition,[new_symbols(definition,[spl22_5])],[avatar_definition]) ).
fof(f108,plain,
( in(sK21,sK19)
| ~ 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
<=> sK18 = sK21 ),
introduced(definition,[new_symbols(definition,[spl22_6])],[avatar_definition]) ).
fof(f113,plain,
( sK18 = 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
<=> sK17 = sK20 ),
introduced(definition,[new_symbols(definition,[spl22_8])],[avatar_definition]) ).
fof(f123,plain,
( sK17 = 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(sK18) ),
introduced(definition,[new_symbols(definition,[spl22_9])],[avatar_definition]) ).
fof(f128,plain,
( young(sK18)
| ~ 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(sK18) ),
introduced(definition,[new_symbols(definition,[spl22_10])],[avatar_definition]) ).
fof(f133,plain,
( man(sK18)
| ~ 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(sK18) ),
introduced(definition,[new_symbols(definition,[spl22_11])],[avatar_definition]) ).
fof(f138,plain,
( fellow(sK18)
| ~ 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(sK17) ),
introduced(definition,[new_symbols(definition,[spl22_12])],[avatar_definition]) ).
fof(f143,plain,
( young(sK17)
| ~ 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(sK17) ),
introduced(definition,[new_symbols(definition,[spl22_13])],[avatar_definition]) ).
fof(f148,plain,
( man(sK17)
| ~ 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(sK17) ),
introduced(definition,[new_symbols(definition,[spl22_14])],[avatar_definition]) ).
fof(f153,plain,
( fellow(sK17)
| ~ 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
<=> sK17 = sK18 ),
introduced(definition,[new_symbols(definition,[spl22_15])],[avatar_definition]) ).
fof(f158,plain,
( sK17 != sK18
| 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
<=> front(sK19) ),
introduced(definition,[new_symbols(definition,[spl22_16])],[avatar_definition]) ).
fof(f163,plain,
( front(sK19)
| ~ 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
<=> furniture(sK19) ),
introduced(definition,[new_symbols(definition,[spl22_17])],[avatar_definition]) ).
fof(f168,plain,
( furniture(sK19)
| ~ 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
<=> seat(sK19) ),
introduced(definition,[new_symbols(definition,[spl22_18])],[avatar_definition]) ).
fof(f173,plain,
( seat(sK19)
| ~ 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
<=> in(sK14,sK13) ),
introduced(definition,[new_symbols(definition,[spl22_19])],[avatar_definition]) ).
fof(f178,plain,
( in(sK14,sK13)
| ~ 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
<=> down(sK14,sK16) ),
introduced(definition,[new_symbols(definition,[spl22_20])],[avatar_definition]) ).
fof(f183,plain,
( down(sK14,sK16)
| ~ 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
<=> barrel(sK14,sK15) ),
introduced(definition,[new_symbols(definition,[spl22_21])],[avatar_definition]) ).
fof(f188,plain,
( barrel(sK14,sK15)
| ~ 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
<=> lonely(sK16) ),
introduced(definition,[new_symbols(definition,[spl22_22])],[avatar_definition]) ).
fof(f193,plain,
( lonely(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
<=> way(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
<=> street(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
<=> old(sK15) ),
introduced(definition,[new_symbols(definition,[spl22_25])],[avatar_definition]) ).
fof(f208,plain,
( old(sK15)
| ~ spl22_25 ),
inference(avatar_component_clause,[],[f206]) ).
fof(f209,plain,
( ~ spl22_1
| spl22_25 ),
inference(avatar_split_clause,[],[f64,f206,f88]) ).
fof(f211,definition,
( spl22_26
<=> dirty(sK15) ),
introduced(definition,[new_symbols(definition,[spl22_26])],[avatar_definition]) ).
fof(f213,plain,
( dirty(sK15)
| ~ spl22_26 ),
inference(avatar_component_clause,[],[f211]) ).
fof(f214,plain,
( ~ spl22_1
| spl22_26 ),
inference(avatar_split_clause,[],[f65,f211,f88]) ).
fof(f216,definition,
( spl22_27
<=> white(sK15) ),
introduced(definition,[new_symbols(definition,[spl22_27])],[avatar_definition]) ).
fof(f218,plain,
( white(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
<=> car(sK15) ),
introduced(definition,[new_symbols(definition,[spl22_28])],[avatar_definition]) ).
fof(f223,plain,
( car(sK15)
| ~ 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
<=> chevy(sK15) ),
introduced(definition,[new_symbols(definition,[spl22_29])],[avatar_definition]) ).
fof(f228,plain,
( chevy(sK15)
| ~ 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
<=> event(sK14) ),
introduced(definition,[new_symbols(definition,[spl22_30])],[avatar_definition]) ).
fof(f233,plain,
( event(sK14)
| ~ 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
<=> city(sK13) ),
introduced(definition,[new_symbols(definition,[spl22_31])],[avatar_definition]) ).
fof(f238,plain,
( city(sK13)
| ~ spl22_31 ),
inference(avatar_component_clause,[],[f236]) ).
fof(f239,plain,
( ~ spl22_1
| spl22_31 ),
inference(avatar_split_clause,[],[f70,f236,f88]) ).
fof(f241,definition,
( spl22_32
<=> hollywood(sK13) ),
introduced(definition,[new_symbols(definition,[spl22_32])],[avatar_definition]) ).
fof(f243,plain,
( hollywood(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(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,sK2) ),
introduced(definition,[new_symbols(definition,[spl22_36])],[avatar_definition]) ).
fof(f263,plain,
( in(sK11,sK2)
| ~ 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
<=> sK8 = sK11 ),
introduced(definition,[new_symbols(definition,[spl22_37])],[avatar_definition]) ).
fof(f268,plain,
( sK8 = 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,sK9) ),
introduced(definition,[new_symbols(definition,[spl22_38])],[avatar_definition]) ).
fof(f273,plain,
( in(sK10,sK9)
| ~ 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
<=> sK7 = sK10 ),
introduced(definition,[new_symbols(definition,[spl22_39])],[avatar_definition]) ).
fof(f278,plain,
( sK7 = 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(sK8) ),
introduced(definition,[new_symbols(definition,[spl22_40])],[avatar_definition]) ).
fof(f283,plain,
( young(sK8)
| ~ 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(sK8) ),
introduced(definition,[new_symbols(definition,[spl22_41])],[avatar_definition]) ).
fof(f288,plain,
( man(sK8)
| ~ 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(sK8) ),
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(sK7) ),
introduced(definition,[new_symbols(definition,[spl22_43])],[avatar_definition]) ).
fof(f298,plain,
( young(sK7)
| ~ 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(sK7) ),
introduced(definition,[new_symbols(definition,[spl22_44])],[avatar_definition]) ).
fof(f303,plain,
( man(sK7)
| ~ 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(sK7) ),
introduced(definition,[new_symbols(definition,[spl22_45])],[avatar_definition]) ).
fof(f308,plain,
( fellow(sK7)
| ~ 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
<=> sK7 = sK8 ),
introduced(definition,[new_symbols(definition,[spl22_46])],[avatar_definition]) ).
fof(f313,plain,
( sK7 != sK8
| 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
<=> front(sK9) ),
introduced(definition,[new_symbols(definition,[spl22_47])],[avatar_definition]) ).
fof(f318,plain,
( front(sK9)
| ~ 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
<=> furniture(sK9) ),
introduced(definition,[new_symbols(definition,[spl22_48])],[avatar_definition]) ).
fof(f323,plain,
( furniture(sK9)
| ~ 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
<=> seat(sK9) ),
introduced(definition,[new_symbols(definition,[spl22_49])],[avatar_definition]) ).
fof(f328,plain,
( seat(sK9)
| ~ 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
<=> in(sK4,sK3) ),
introduced(definition,[new_symbols(definition,[spl22_50])],[avatar_definition]) ).
fof(f333,plain,
( in(sK4,sK3)
| ~ 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
<=> down(sK4,sK6) ),
introduced(definition,[new_symbols(definition,[spl22_51])],[avatar_definition]) ).
fof(f338,plain,
( down(sK4,sK6)
| ~ spl22_51 ),
inference(avatar_component_clause,[],[f336]) ).
fof(f339,plain,
( ~ spl22_2
| spl22_51 ),
inference(avatar_split_clause,[],[f28,f336,f92]) ).
fof(f341,definition,
( spl22_52
<=> barrel(sK4,sK5) ),
introduced(definition,[new_symbols(definition,[spl22_52])],[avatar_definition]) ).
fof(f343,plain,
( barrel(sK4,sK5)
| ~ spl22_52 ),
inference(avatar_component_clause,[],[f341]) ).
fof(f344,plain,
( ~ spl22_2
| spl22_52 ),
inference(avatar_split_clause,[],[f29,f341,f92]) ).
fof(f346,definition,
( spl22_53
<=> lonely(sK6) ),
introduced(definition,[new_symbols(definition,[spl22_53])],[avatar_definition]) ).
fof(f348,plain,
( lonely(sK6)
| ~ spl22_53 ),
inference(avatar_component_clause,[],[f346]) ).
fof(f349,plain,
( ~ spl22_2
| spl22_53 ),
inference(avatar_split_clause,[],[f30,f346,f92]) ).
fof(f351,definition,
( spl22_54
<=> way(sK6) ),
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
<=> street(sK6) ),
introduced(definition,[new_symbols(definition,[spl22_55])],[avatar_definition]) ).
fof(f359,plain,
( ~ spl22_2
| spl22_55 ),
inference(avatar_split_clause,[],[f32,f356,f92]) ).
fof(f361,definition,
( spl22_56
<=> old(sK5) ),
introduced(definition,[new_symbols(definition,[spl22_56])],[avatar_definition]) ).
fof(f363,plain,
( old(sK5)
| ~ 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
<=> dirty(sK5) ),
introduced(definition,[new_symbols(definition,[spl22_57])],[avatar_definition]) ).
fof(f368,plain,
( dirty(sK5)
| ~ 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
<=> white(sK5) ),
introduced(definition,[new_symbols(definition,[spl22_58])],[avatar_definition]) ).
fof(f373,plain,
( white(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
<=> car(sK5) ),
introduced(definition,[new_symbols(definition,[spl22_59])],[avatar_definition]) ).
fof(f378,plain,
( car(sK5)
| ~ 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
<=> chevy(sK5) ),
introduced(definition,[new_symbols(definition,[spl22_60])],[avatar_definition]) ).
fof(f383,plain,
( chevy(sK5)
| ~ 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
<=> event(sK4) ),
introduced(definition,[new_symbols(definition,[spl22_61])],[avatar_definition]) ).
fof(f388,plain,
( event(sK4)
| ~ 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
<=> city(sK3) ),
introduced(definition,[new_symbols(definition,[spl22_62])],[avatar_definition]) ).
fof(f393,plain,
( city(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
<=> hollywood(sK3) ),
introduced(definition,[new_symbols(definition,[spl22_63])],[avatar_definition]) ).
fof(f398,plain,
( hollywood(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,sK6)
| ~ barrel(X0,X2)
| ~ street(sK6)
| ~ hollywood(X1)
| ~ way(sK6)
| ~ chevy(X2)
| ~ old(X2)
| ~ dirty(X2)
| ~ white(X2)
| ~ car(X2)
| ~ city(X1) )
| ~ spl22_3
| ~ spl22_53 ),
inference(resolution,[],[f348,f98]) ).
fof(f417,definition,
( spl22_67
<=> ! [X2,X0,X1] :
( ~ event(X0)
| ~ city(X1)
| ~ car(X2)
| ~ white(X2)
| ~ dirty(X2)
| ~ old(X2)
| ~ chevy(X2)
| ~ hollywood(X1)
| ~ barrel(X0,X2)
| ~ down(X0,sK6)
| ~ in(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl22_67])],[avatar_definition]) ).
fof(f418,plain,
( ! [X2,X0,X1] :
( ~ down(X0,sK6)
| ~ city(X1)
| ~ car(X2)
| ~ white(X2)
| ~ dirty(X2)
| ~ old(X2)
| ~ chevy(X2)
| ~ hollywood(X1)
| ~ barrel(X0,X2)
| ~ event(X0)
| ~ in(X0,X1) )
| ~ spl22_67 ),
inference(avatar_component_clause,[],[f417]) ).
fof(f419,plain,
( ~ spl22_54
| ~ spl22_55
| spl22_67
| ~ spl22_3
| ~ spl22_53 ),
inference(avatar_split_clause,[],[f415,f346,f97,f417,f356,f351]) ).
fof(f420,plain,
( ! [X2,X0,X1] :
( ~ event(X0)
| ~ in(X0,X1)
| ~ down(X0,sK16)
| ~ barrel(X0,X2)
| ~ street(sK16)
| ~ hollywood(X1)
| ~ way(sK16)
| ~ chevy(X2)
| ~ old(X2)
| ~ dirty(X2)
| ~ white(X2)
| ~ car(X2)
| ~ city(X1) )
| ~ spl22_3
| ~ spl22_22 ),
inference(resolution,[],[f193,f98]) ).
fof(f422,definition,
( spl22_68
<=> ! [X2,X0,X1] :
( ~ event(X0)
| ~ city(X1)
| ~ car(X2)
| ~ white(X2)
| ~ dirty(X2)
| ~ old(X2)
| ~ chevy(X2)
| ~ hollywood(X1)
| ~ barrel(X0,X2)
| ~ down(X0,sK16)
| ~ in(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl22_68])],[avatar_definition]) ).
fof(f423,plain,
( ! [X2,X0,X1] :
( ~ down(X0,sK16)
| ~ city(X1)
| ~ car(X2)
| ~ white(X2)
| ~ dirty(X2)
| ~ old(X2)
| ~ chevy(X2)
| ~ hollywood(X1)
| ~ barrel(X0,X2)
| ~ event(X0)
| ~ in(X0,X1) )
| ~ spl22_68 ),
inference(avatar_component_clause,[],[f422]) ).
fof(f424,plain,
( ~ spl22_23
| ~ spl22_24
| spl22_68
| ~ spl22_3
| ~ spl22_22 ),
inference(avatar_split_clause,[],[f420,f191,f97,f422,f201,f196]) ).
fof(f425,plain,
( in(sK18,sK19)
| ~ spl22_5
| ~ spl22_6 ),
inference(superposition,[],[f108,f113]) ).
fof(f426,plain,
( in(sK17,sK12)
| ~ spl22_7
| ~ spl22_8 ),
inference(superposition,[],[f118,f123]) ).
fof(f427,plain,
( ! [X0,X1] :
( ~ city(X0)
| ~ car(X1)
| ~ white(X1)
| ~ dirty(X1)
| ~ old(X1)
| ~ chevy(X1)
| ~ hollywood(X0)
| ~ barrel(sK14,X1)
| ~ event(sK14)
| ~ in(sK14,X0) )
| ~ spl22_20
| ~ spl22_68 ),
inference(resolution,[],[f183,f423]) ).
fof(f428,plain,
( ! [X0,X1] :
( ~ city(X0)
| ~ car(X1)
| ~ white(X1)
| ~ dirty(X1)
| ~ old(X1)
| ~ chevy(X1)
| ~ hollywood(X0)
| ~ barrel(sK14,X1)
| ~ in(sK14,X0) )
| ~ spl22_20
| ~ spl22_30
| ~ spl22_68 ),
inference(forward_subsumption_resolution,[],[f427,f233]) ).
fof(f430,definition,
( spl22_69
<=> ! [X1] :
( ~ car(X1)
| ~ barrel(sK14,X1)
| ~ chevy(X1)
| ~ old(X1)
| ~ dirty(X1)
| ~ white(X1) ) ),
introduced(definition,[new_symbols(definition,[spl22_69])],[avatar_definition]) ).
fof(f431,plain,
( ! [X1] :
( ~ barrel(sK14,X1)
| ~ car(X1)
| ~ chevy(X1)
| ~ old(X1)
| ~ dirty(X1)
| ~ white(X1) )
| ~ spl22_69 ),
inference(avatar_component_clause,[],[f430]) ).
fof(f433,definition,
( spl22_70
<=> ! [X0] :
( ~ city(X0)
| ~ in(sK14,X0)
| ~ hollywood(X0) ) ),
introduced(definition,[new_symbols(definition,[spl22_70])],[avatar_definition]) ).
fof(f434,plain,
( ! [X0] :
( ~ in(sK14,X0)
| ~ city(X0)
| ~ hollywood(X0) )
| ~ spl22_70 ),
inference(avatar_component_clause,[],[f433]) ).
fof(f435,plain,
( spl22_69
| spl22_70
| ~ spl22_20
| ~ spl22_30
| ~ spl22_68 ),
inference(avatar_split_clause,[],[f428,f422,f231,f181,f433,f430]) ).
fof(f436,plain,
( ~ city(sK13)
| ~ hollywood(sK13)
| ~ spl22_19
| ~ spl22_70 ),
inference(resolution,[],[f434,f178]) ).
fof(f437,plain,
( ~ hollywood(sK13)
| ~ spl22_19
| ~ spl22_31
| ~ spl22_70 ),
inference(forward_subsumption_resolution,[],[f436,f238]) ).
fof(f438,plain,
( $false
| ~ spl22_19
| ~ spl22_31
| ~ spl22_32
| ~ spl22_70 ),
inference(forward_subsumption_resolution,[],[f437,f243]) ).
fof(f439,plain,
( ~ spl22_19
| ~ spl22_31
| ~ spl22_32
| ~ spl22_70 ),
inference(avatar_contradiction_clause,[],[f438]) ).
fof(f440,plain,
( ~ car(sK15)
| ~ chevy(sK15)
| ~ old(sK15)
| ~ dirty(sK15)
| ~ white(sK15)
| ~ spl22_21
| ~ spl22_69 ),
inference(resolution,[],[f431,f188]) ).
fof(f441,plain,
( ~ chevy(sK15)
| ~ old(sK15)
| ~ dirty(sK15)
| ~ white(sK15)
| ~ spl22_21
| ~ spl22_28
| ~ spl22_69 ),
inference(forward_subsumption_resolution,[],[f440,f223]) ).
fof(f442,plain,
( ~ old(sK15)
| ~ dirty(sK15)
| ~ white(sK15)
| ~ spl22_21
| ~ spl22_28
| ~ spl22_29
| ~ spl22_69 ),
inference(forward_subsumption_resolution,[],[f441,f228]) ).
fof(f443,plain,
( ~ dirty(sK15)
| ~ white(sK15)
| ~ spl22_21
| ~ spl22_25
| ~ spl22_28
| ~ spl22_29
| ~ spl22_69 ),
inference(forward_subsumption_resolution,[],[f442,f208]) ).
fof(f444,plain,
( ~ white(sK15)
| ~ spl22_21
| ~ spl22_25
| ~ spl22_26
| ~ spl22_28
| ~ spl22_29
| ~ spl22_69 ),
inference(forward_subsumption_resolution,[],[f443,f213]) ).
fof(f445,plain,
( $false
| ~ spl22_21
| ~ spl22_25
| ~ spl22_26
| ~ spl22_27
| ~ spl22_28
| ~ spl22_29
| ~ spl22_69 ),
inference(forward_subsumption_resolution,[],[f444,f218]) ).
fof(f446,plain,
( ~ spl22_21
| ~ spl22_25
| ~ spl22_26
| ~ spl22_27
| ~ spl22_28
| ~ spl22_29
| ~ spl22_69 ),
inference(avatar_contradiction_clause,[],[f445]) ).
fof(f447,plain,
( in(sK8,sK2)
| ~ spl22_36
| ~ spl22_37 ),
inference(superposition,[],[f263,f268]) ).
fof(f448,plain,
( in(sK7,sK9)
| ~ spl22_38
| ~ spl22_39 ),
inference(superposition,[],[f273,f278]) ).
fof(f449,plain,
( ! [X0,X1] :
( ~ city(X0)
| ~ car(X1)
| ~ white(X1)
| ~ dirty(X1)
| ~ old(X1)
| ~ chevy(X1)
| ~ hollywood(X0)
| ~ barrel(sK4,X1)
| ~ event(sK4)
| ~ in(sK4,X0) )
| ~ spl22_51
| ~ spl22_67 ),
inference(resolution,[],[f338,f418]) ).
fof(f450,plain,
( ! [X0,X1] :
( ~ city(X0)
| ~ car(X1)
| ~ white(X1)
| ~ dirty(X1)
| ~ old(X1)
| ~ chevy(X1)
| ~ hollywood(X0)
| ~ barrel(sK4,X1)
| ~ in(sK4,X0) )
| ~ spl22_51
| ~ spl22_61
| ~ spl22_67 ),
inference(forward_subsumption_resolution,[],[f449,f388]) ).
fof(f452,definition,
( spl22_71
<=> ! [X1] :
( ~ car(X1)
| ~ barrel(sK4,X1)
| ~ chevy(X1)
| ~ old(X1)
| ~ dirty(X1)
| ~ white(X1) ) ),
introduced(definition,[new_symbols(definition,[spl22_71])],[avatar_definition]) ).
fof(f453,plain,
( ! [X1] :
( ~ barrel(sK4,X1)
| ~ car(X1)
| ~ chevy(X1)
| ~ old(X1)
| ~ dirty(X1)
| ~ white(X1) )
| ~ spl22_71 ),
inference(avatar_component_clause,[],[f452]) ).
fof(f455,definition,
( spl22_72
<=> ! [X0] :
( ~ city(X0)
| ~ in(sK4,X0)
| ~ hollywood(X0) ) ),
introduced(definition,[new_symbols(definition,[spl22_72])],[avatar_definition]) ).
fof(f456,plain,
( ! [X0] :
( ~ in(sK4,X0)
| ~ city(X0)
| ~ hollywood(X0) )
| ~ spl22_72 ),
inference(avatar_component_clause,[],[f455]) ).
fof(f457,plain,
( spl22_71
| spl22_72
| ~ spl22_51
| ~ spl22_61
| ~ spl22_67 ),
inference(avatar_split_clause,[],[f450,f417,f386,f336,f455,f452]) ).
fof(f458,plain,
( ~ car(sK5)
| ~ chevy(sK5)
| ~ old(sK5)
| ~ dirty(sK5)
| ~ white(sK5)
| ~ spl22_52
| ~ spl22_71 ),
inference(resolution,[],[f343,f453]) ).
fof(f459,plain,
( ~ chevy(sK5)
| ~ old(sK5)
| ~ dirty(sK5)
| ~ white(sK5)
| ~ spl22_52
| ~ spl22_59
| ~ spl22_71 ),
inference(forward_subsumption_resolution,[],[f458,f378]) ).
fof(f460,plain,
( ~ old(sK5)
| ~ dirty(sK5)
| ~ white(sK5)
| ~ spl22_52
| ~ spl22_59
| ~ spl22_60
| ~ spl22_71 ),
inference(forward_subsumption_resolution,[],[f459,f383]) ).
fof(f461,plain,
( ~ dirty(sK5)
| ~ white(sK5)
| ~ spl22_52
| ~ spl22_56
| ~ spl22_59
| ~ spl22_60
| ~ spl22_71 ),
inference(forward_subsumption_resolution,[],[f460,f363]) ).
fof(f462,plain,
( ~ white(sK5)
| ~ spl22_52
| ~ spl22_56
| ~ spl22_57
| ~ spl22_59
| ~ spl22_60
| ~ spl22_71 ),
inference(forward_subsumption_resolution,[],[f461,f368]) ).
fof(f463,plain,
( $false
| ~ spl22_52
| ~ spl22_56
| ~ spl22_57
| ~ spl22_58
| ~ spl22_59
| ~ spl22_60
| ~ spl22_71 ),
inference(forward_subsumption_resolution,[],[f462,f373]) ).
fof(f464,plain,
( ~ spl22_52
| ~ spl22_56
| ~ spl22_57
| ~ spl22_58
| ~ spl22_59
| ~ spl22_60
| ~ spl22_71 ),
inference(avatar_contradiction_clause,[],[f463]) ).
fof(f465,plain,
( ~ city(sK3)
| ~ hollywood(sK3)
| ~ spl22_50
| ~ spl22_72 ),
inference(resolution,[],[f456,f333]) ).
fof(f466,plain,
( ~ hollywood(sK3)
| ~ spl22_50
| ~ spl22_62
| ~ spl22_72 ),
inference(forward_subsumption_resolution,[],[f465,f393]) ).
fof(f467,plain,
( $false
| ~ spl22_50
| ~ spl22_62
| ~ spl22_63
| ~ spl22_72 ),
inference(forward_subsumption_resolution,[],[f466,f398]) ).
fof(f468,plain,
( ~ spl22_50
| ~ spl22_62
| ~ spl22_63
| ~ spl22_72 ),
inference(avatar_contradiction_clause,[],[f467]) ).
fof(f470,plain,
( ! [X2,X0,X1] :
( ~ seat(X0)
| ~ in(sK8,X1)
| sK8 = X2
| ~ in(X2,X0)
| ~ seat(X1)
| ~ man(sK8)
| ~ fellow(sK8)
| ~ young(X2)
| ~ man(X2)
| ~ fellow(X2)
| ~ front(X0)
| ~ furniture(X0)
| ~ front(X1)
| ~ furniture(X1) )
| ~ spl22_4
| ~ spl22_40 ),
inference(resolution,[],[f101,f283]) ).
fof(f477,plain,
( ! [X2,X0,X1] :
( ~ seat(X0)
| ~ in(sK8,X1)
| sK8 = X2
| ~ in(X2,X0)
| ~ seat(X1)
| ~ fellow(sK8)
| ~ young(X2)
| ~ man(X2)
| ~ fellow(X2)
| ~ front(X0)
| ~ furniture(X0)
| ~ front(X1)
| ~ furniture(X1) )
| ~ spl22_4
| ~ spl22_40
| ~ spl22_41 ),
inference(forward_subsumption_resolution,[],[f470,f288]) ).
fof(f484,definition,
( spl22_73
<=> ! [X1] :
( ~ in(sK18,X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ seat(X1) ) ),
introduced(definition,[new_symbols(definition,[spl22_73])],[avatar_definition]) ).
fof(f485,plain,
( ! [X1] :
( ~ in(sK18,X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ seat(X1) )
| ~ spl22_73 ),
inference(avatar_component_clause,[],[f484]) ).
fof(f487,definition,
( spl22_74
<=> ! [X2,X0] :
( ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ fellow(X2)
| ~ man(X2)
| ~ young(X2)
| sK18 = X2
| ~ in(X2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl22_74])],[avatar_definition]) ).
fof(f488,plain,
( ! [X2,X0] :
( ~ fellow(X2)
| ~ furniture(X0)
| ~ front(X0)
| ~ seat(X0)
| ~ man(X2)
| ~ young(X2)
| sK18 = X2
| ~ in(X2,X0) )
| ~ spl22_74 ),
inference(avatar_component_clause,[],[f487]) ).
fof(f491,definition,
( spl22_75
<=> ! [X1] :
( ~ in(sK17,X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ seat(X1) ) ),
introduced(definition,[new_symbols(definition,[spl22_75])],[avatar_definition]) ).
fof(f492,plain,
( ! [X1] :
( ~ in(sK17,X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ seat(X1) )
| ~ spl22_75 ),
inference(avatar_component_clause,[],[f491]) ).
fof(f498,definition,
( spl22_77
<=> ! [X1] :
( ~ in(sK8,X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ seat(X1) ) ),
introduced(definition,[new_symbols(definition,[spl22_77])],[avatar_definition]) ).
fof(f499,plain,
( ! [X1] :
( ~ in(sK8,X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ seat(X1) )
| ~ spl22_77 ),
inference(avatar_component_clause,[],[f498]) ).
fof(f501,definition,
( spl22_78
<=> ! [X2,X0] :
( ~ seat(X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ fellow(X2)
| ~ man(X2)
| ~ young(X2)
| sK8 = X2
| ~ in(X2,X0) ) ),
introduced(definition,[new_symbols(definition,[spl22_78])],[avatar_definition]) ).
fof(f502,plain,
( ! [X2,X0] :
( ~ young(X2)
| ~ furniture(X0)
| ~ front(X0)
| ~ fellow(X2)
| ~ man(X2)
| ~ seat(X0)
| sK8 = X2
| ~ in(X2,X0) )
| ~ spl22_78 ),
inference(avatar_component_clause,[],[f501]) ).
fof(f505,definition,
( spl22_79
<=> ! [X1] :
( ~ in(sK7,X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ seat(X1) ) ),
introduced(definition,[new_symbols(definition,[spl22_79])],[avatar_definition]) ).
fof(f506,plain,
( ! [X1] :
( ~ in(sK7,X1)
| ~ furniture(X1)
| ~ front(X1)
| ~ seat(X1) )
| ~ spl22_79 ),
inference(avatar_component_clause,[],[f505]) ).
fof(f511,plain,
( ! [X0] :
( ~ furniture(X0)
| ~ front(X0)
| ~ fellow(sK7)
| ~ man(sK7)
| ~ seat(X0)
| sK7 = sK8
| ~ in(sK7,X0) )
| ~ spl22_43
| ~ spl22_78 ),
inference(resolution,[],[f502,f298]) ).
fof(f514,plain,
( ~ furniture(sK12)
| ~ front(sK12)
| ~ seat(sK12)
| ~ spl22_7
| ~ spl22_8
| ~ spl22_75 ),
inference(resolution,[],[f426,f492]) ).
fof(f519,plain,
( ~ furniture(sK12)
| ~ seat(sK12)
| ~ spl22_7
| ~ spl22_8
| ~ spl22_33
| ~ spl22_75 ),
inference(forward_subsumption_resolution,[],[f514,f248]) ).
fof(f520,plain,
( ~ furniture(sK12)
| ~ spl22_7
| ~ spl22_8
| ~ spl22_33
| ~ spl22_35
| ~ spl22_75 ),
inference(forward_subsumption_resolution,[],[f519,f258]) ).
fof(f521,plain,
( ~ spl22_34
| ~ spl22_7
| ~ spl22_8
| ~ spl22_33
| ~ spl22_35
| ~ spl22_75 ),
inference(avatar_split_clause,[],[f520,f491,f256,f246,f121,f116,f251]) ).
fof(f522,plain,
( ~ furniture(sK9)
| ~ front(sK9)
| ~ seat(sK9)
| ~ spl22_38
| ~ spl22_39
| ~ spl22_79 ),
inference(resolution,[],[f448,f506]) ).
fof(f523,plain,
( ~ front(sK9)
| ~ seat(sK9)
| ~ spl22_38
| ~ spl22_39
| ~ spl22_48
| ~ spl22_79 ),
inference(forward_subsumption_resolution,[],[f522,f323]) ).
fof(f524,plain,
( ~ seat(sK9)
| ~ spl22_38
| ~ spl22_39
| ~ spl22_47
| ~ spl22_48
| ~ spl22_79 ),
inference(forward_subsumption_resolution,[],[f523,f318]) ).
fof(f525,plain,
( $false
| ~ spl22_38
| ~ spl22_39
| ~ spl22_47
| ~ spl22_48
| ~ spl22_49
| ~ spl22_79 ),
inference(forward_subsumption_resolution,[],[f524,f328]) ).
fof(f526,plain,
( ~ spl22_38
| ~ spl22_39
| ~ spl22_47
| ~ spl22_48
| ~ spl22_49
| ~ spl22_79 ),
inference(avatar_contradiction_clause,[],[f525]) ).
fof(f527,plain,
( ! [X0] :
( ~ furniture(X0)
| ~ front(X0)
| ~ man(sK7)
| ~ seat(X0)
| sK7 = sK8
| ~ in(sK7,X0) )
| ~ spl22_43
| ~ spl22_45
| ~ spl22_78 ),
inference(forward_subsumption_resolution,[],[f511,f308]) ).
fof(f528,plain,
( ! [X0] :
( ~ furniture(X0)
| ~ front(X0)
| ~ seat(X0)
| sK7 = sK8
| ~ in(sK7,X0) )
| ~ spl22_43
| ~ spl22_44
| ~ spl22_45
| ~ spl22_78 ),
inference(forward_subsumption_resolution,[],[f527,f303]) ).
fof(f529,plain,
( ! [X0] :
( ~ furniture(X0)
| ~ front(X0)
| ~ seat(X0)
| ~ in(sK7,X0) )
| ~ spl22_43
| ~ spl22_44
| ~ spl22_45
| spl22_46
| ~ spl22_78 ),
inference(forward_subsumption_resolution,[],[f528,f313]) ).
fof(f530,plain,
( spl22_79
| ~ spl22_43
| ~ spl22_44
| ~ spl22_45
| spl22_46
| ~ spl22_78 ),
inference(avatar_split_clause,[],[f529,f501,f311,f306,f301,f296,f505]) ).
fof(f531,plain,
( ~ furniture(sK2)
| ~ front(sK2)
| ~ seat(sK2)
| ~ spl22_36
| ~ spl22_37
| ~ spl22_77 ),
inference(resolution,[],[f499,f447]) ).
fof(f532,plain,
( ~ front(sK2)
| ~ seat(sK2)
| ~ spl22_36
| ~ spl22_37
| ~ spl22_65
| ~ spl22_77 ),
inference(forward_subsumption_resolution,[],[f531,f408]) ).
fof(f533,plain,
( ~ seat(sK2)
| ~ spl22_36
| ~ spl22_37
| ~ spl22_64
| ~ spl22_65
| ~ spl22_77 ),
inference(forward_subsumption_resolution,[],[f532,f403]) ).
fof(f534,plain,
( $false
| ~ spl22_36
| ~ spl22_37
| ~ spl22_64
| ~ spl22_65
| ~ spl22_66
| ~ spl22_77 ),
inference(forward_subsumption_resolution,[],[f533,f413]) ).
fof(f535,plain,
( ~ spl22_36
| ~ spl22_37
| ~ spl22_64
| ~ spl22_65
| ~ spl22_66
| ~ spl22_77 ),
inference(avatar_contradiction_clause,[],[f534]) ).
fof(f539,plain,
( ~ spl22_42
| spl22_77
| spl22_78
| ~ spl22_4
| ~ spl22_40
| ~ spl22_41 ),
inference(avatar_split_clause,[],[f477,f286,f281,f100,f501,f498,f291]) ).
fof(f543,plain,
( ~ furniture(sK19)
| ~ front(sK19)
| ~ seat(sK19)
| ~ spl22_5
| ~ spl22_6
| ~ spl22_73 ),
inference(resolution,[],[f485,f425]) ).
fof(f544,plain,
( ~ front(sK19)
| ~ seat(sK19)
| ~ spl22_5
| ~ spl22_6
| ~ spl22_17
| ~ spl22_73 ),
inference(forward_subsumption_resolution,[],[f543,f168]) ).
fof(f545,plain,
( ~ seat(sK19)
| ~ spl22_5
| ~ spl22_6
| ~ spl22_16
| ~ spl22_17
| ~ spl22_73 ),
inference(forward_subsumption_resolution,[],[f544,f163]) ).
fof(f546,plain,
( $false
| ~ spl22_5
| ~ spl22_6
| ~ spl22_16
| ~ spl22_17
| ~ spl22_18
| ~ spl22_73 ),
inference(forward_subsumption_resolution,[],[f545,f173]) ).
fof(f547,plain,
( ~ spl22_5
| ~ spl22_6
| ~ spl22_16
| ~ spl22_17
| ~ spl22_18
| ~ spl22_73 ),
inference(avatar_contradiction_clause,[],[f546]) ).
fof(f548,plain,
( ! [X2,X0,X1] :
( ~ seat(X0)
| ~ in(sK18,X1)
| sK18 = X2
| ~ in(X2,X0)
| ~ seat(X1)
| ~ man(sK18)
| ~ fellow(sK18)
| ~ young(X2)
| ~ man(X2)
| ~ fellow(X2)
| ~ front(X0)
| ~ furniture(X0)
| ~ front(X1)
| ~ furniture(X1) )
| ~ spl22_4
| ~ spl22_9 ),
inference(resolution,[],[f128,f101]) ).
fof(f549,plain,
( ! [X2,X0,X1] :
( ~ seat(X0)
| ~ in(sK18,X1)
| sK18 = X2
| ~ in(X2,X0)
| ~ seat(X1)
| ~ fellow(sK18)
| ~ young(X2)
| ~ man(X2)
| ~ fellow(X2)
| ~ front(X0)
| ~ furniture(X0)
| ~ front(X1)
| ~ furniture(X1) )
| ~ spl22_4
| ~ spl22_9
| ~ spl22_10 ),
inference(forward_subsumption_resolution,[],[f548,f133]) ).
fof(f550,plain,
( ! [X2,X0,X1] :
( ~ seat(X0)
| ~ in(sK18,X1)
| sK18 = X2
| ~ in(X2,X0)
| ~ seat(X1)
| ~ young(X2)
| ~ man(X2)
| ~ fellow(X2)
| ~ front(X0)
| ~ furniture(X0)
| ~ front(X1)
| ~ furniture(X1) )
| ~ spl22_4
| ~ spl22_9
| ~ spl22_10
| ~ spl22_11 ),
inference(forward_subsumption_resolution,[],[f549,f138]) ).
fof(f551,plain,
( spl22_73
| spl22_74
| ~ spl22_4
| ~ spl22_9
| ~ spl22_10
| ~ spl22_11 ),
inference(avatar_split_clause,[],[f550,f136,f131,f126,f100,f487,f484]) ).
fof(f553,plain,
( ! [X0] :
( ~ furniture(X0)
| ~ front(X0)
| ~ seat(X0)
| ~ man(sK17)
| ~ young(sK17)
| sK17 = sK18
| ~ in(sK17,X0) )
| ~ spl22_14
| ~ spl22_74 ),
inference(resolution,[],[f488,f153]) ).
fof(f555,plain,
( ! [X0] :
( ~ furniture(X0)
| ~ front(X0)
| ~ seat(X0)
| ~ young(sK17)
| sK17 = sK18
| ~ in(sK17,X0) )
| ~ spl22_13
| ~ spl22_14
| ~ spl22_74 ),
inference(forward_subsumption_resolution,[],[f553,f148]) ).
fof(f557,plain,
( ! [X0] :
( ~ furniture(X0)
| ~ front(X0)
| ~ seat(X0)
| sK17 = sK18
| ~ in(sK17,X0) )
| ~ spl22_12
| ~ spl22_13
| ~ spl22_14
| ~ spl22_74 ),
inference(forward_subsumption_resolution,[],[f555,f143]) ).
fof(f559,plain,
( ! [X0] :
( ~ furniture(X0)
| ~ front(X0)
| ~ seat(X0)
| ~ in(sK17,X0) )
| ~ spl22_12
| ~ spl22_13
| ~ spl22_14
| spl22_15
| ~ spl22_74 ),
inference(forward_subsumption_resolution,[],[f557,f158]) ).
fof(f565,plain,
( spl22_75
| ~ spl22_12
| ~ spl22_13
| ~ spl22_14
| spl22_15
| ~ spl22_74 ),
inference(avatar_split_clause,[],[f559,f487,f156,f151,f146,f141,f491]) ).
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_53
| ~ spl22_54
| ~ spl22_55
| spl22_67 ),
inference(sat_conversion,[],[f419]) ).
cnf(s69,plain,
( ~ spl22_3
| ~ spl22_22
| ~ spl22_23
| ~ spl22_24
| spl22_68 ),
inference(sat_conversion,[],[f424]) ).
cnf(s70,plain,
( ~ spl22_20
| ~ spl22_30
| ~ spl22_68
| spl22_69
| spl22_70 ),
inference(sat_conversion,[],[f435]) ).
cnf(s71,plain,
( ~ spl22_19
| ~ spl22_31
| ~ spl22_32
| ~ spl22_70 ),
inference(sat_conversion,[],[f439]) ).
cnf(s72,plain,
( ~ spl22_21
| ~ spl22_25
| ~ spl22_26
| ~ spl22_27
| ~ spl22_28
| ~ spl22_29
| ~ spl22_69 ),
inference(sat_conversion,[],[f446]) ).
cnf(s73,plain,
( ~ spl22_51
| ~ spl22_61
| ~ spl22_67
| spl22_71
| spl22_72 ),
inference(sat_conversion,[],[f457]) ).
cnf(s74,plain,
( ~ spl22_52
| ~ spl22_56
| ~ spl22_57
| ~ spl22_58
| ~ spl22_59
| ~ spl22_60
| ~ spl22_71 ),
inference(sat_conversion,[],[f464]) ).
cnf(s75,plain,
( ~ spl22_50
| ~ spl22_62
| ~ spl22_63
| ~ spl22_72 ),
inference(sat_conversion,[],[f468]) ).
cnf(s81,plain,
( ~ spl22_7
| ~ spl22_8
| ~ spl22_33
| ~ spl22_34
| ~ spl22_35
| ~ spl22_75 ),
inference(sat_conversion,[],[f521]) ).
cnf(s82,plain,
( ~ spl22_38
| ~ spl22_39
| ~ spl22_47
| ~ spl22_48
| ~ spl22_49
| ~ spl22_79 ),
inference(sat_conversion,[],[f526]) ).
cnf(s83,plain,
( ~ spl22_43
| ~ spl22_44
| ~ spl22_45
| spl22_46
| ~ spl22_78
| spl22_79 ),
inference(sat_conversion,[],[f530]) ).
cnf(s84,plain,
( ~ spl22_36
| ~ spl22_37
| ~ spl22_64
| ~ spl22_65
| ~ spl22_66
| ~ spl22_77 ),
inference(sat_conversion,[],[f535]) ).
cnf(s86,plain,
( ~ spl22_4
| ~ spl22_40
| ~ spl22_41
| ~ spl22_42
| spl22_77
| spl22_78 ),
inference(sat_conversion,[],[f539]) ).
cnf(s89,plain,
( ~ spl22_5
| ~ spl22_6
| ~ spl22_16
| ~ spl22_17
| ~ spl22_18
| ~ spl22_73 ),
inference(sat_conversion,[],[f547]) ).
cnf(s90,plain,
( ~ spl22_4
| ~ spl22_9
| ~ spl22_10
| ~ spl22_11
| spl22_73
| spl22_74 ),
inference(sat_conversion,[],[f551]) ).
cnf(s92,plain,
( ~ spl22_12
| ~ spl22_13
| ~ spl22_14
| spl22_15
| ~ spl22_74
| spl22_75 ),
inference(sat_conversion,[],[f565]) ).
cnf(s93,plain,
~ spl22_2,
inference(rat,[],[s5,s68,s86,s83,s73,s84,s82,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,s105,s101,s102,s103,s104,s109]) ).
cnf(s127,plain,
~ spl22_70,
inference(rat,[],[s71,s99,s98,s111]) ).
cnf(s128,plain,
~ spl22_75,
inference(rat,[],[s81,s122,s95,s96,s97,s123]) ).
cnf(s129,plain,
~ spl22_73,
inference(rat,[],[s89,s124,s112,s113,s114,s125]) ).
cnf(s130,plain,
~ spl22_68,
inference(rat,[],[s70,s110,s126,s100,s127]) ).
cnf(s131,plain,
~ spl22_74,
inference(rat,[],[s92,s118,s117,s115,s116,s128]) ).
cnf(s132,plain,
~ spl22_4,
inference(rat,[],[s90,s131,s121,s119,s120,s129]) ).
cnf(s133,plain,
~ spl22_3,
inference(rat,[],[s69,s108,s106,s107,s130]) ).
cnf(s134,plain,
$false,
inference(rat,[],[s5,s132,s133]) ).
fof(f566,plain,
$false,
inference(avatar_sat_refutation,[],[s134]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP007+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n026.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 17:49:41 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.44/1.30 % (3103090)Detected formulas, will run a generic FOF schedule.
% 2.44/1.30 % (3103099)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=617931411:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.44/1.30 % (3103099)Instruction limit reached!
% 2.44/1.30 % (3103099)------------------------------
% 2.44/1.30 % (3103099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.44/1.30 % (3103099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.44/1.30 % (3103099)CaDiCaL version: 2.1.3
% 2.44/1.30 % (3103099)Termination reason: Instruction limit
% 2.44/1.30 % (3103099)Termination phase: Saturation
% 2.44/1.30 % (3103099)Time elapsed: 0.022 s
% 2.44/1.30 % (3103099)Peak memory usage: 88 MB
% 2.44/1.30 % (3103099)Instructions burned: 122 (million)
% 2.44/1.30 % (3103100)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=751135196:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.44/1.30 % (3103097)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=17064135:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.44/1.30 % (3103101)dis-21_1_sil=8000:lcm=predicate:random_seed=969250346: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.44/1.30 % (3103098)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2716997290:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.44/1.30 % (3103096)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=2627184491:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.44/1.30 % (3103095)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=1701425260:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.44/1.30 % (3103101)Refutation not found, incomplete strategy
% 2.44/1.30 % (3103101)------------------------------
% 2.44/1.30 % (3103101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.44/1.30 % (3103101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.44/1.30 % (3103101)CaDiCaL version: 2.1.3
% 2.44/1.30 % (3103101)Termination reason: Refutation not found, incomplete strategy
% 2.44/1.30 % (3103101)Time elapsed: 0.004 s
% 2.44/1.30 % (3103101)Peak memory usage: 88 MB
% 2.44/1.30 % (3103101)Instructions burned: 5 (million)
% 2.44/1.30 % (3103100)First to succeed.
% 2.44/1.30 % (3103098)Refutation not found, incomplete strategy
% 2.44/1.30 % (3103098)------------------------------
% 2.44/1.30 % (3103098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.44/1.30 % (3103098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.44/1.30 % (3103098)CaDiCaL version: 2.1.3
% 2.44/1.30 % (3103098)Termination reason: Refutation not found, incomplete strategy
% 2.44/1.30 % (3103098)Time elapsed: 0.012 s
% 2.44/1.30 % (3103098)Peak memory usage: 88 MB
% 2.44/1.30 % (3103098)Instructions burned: 18 (million)
% 2.44/1.30 % (3103100)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3103090"
% 2.44/1.30 % (3103103)lrs+10_1_sil=8000:sp=occurrence:random_seed=2956164955:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 2.44/1.30 % (3103103)Also succeeded, but the first one will report.
% 2.44/1.30 % (3103101)------------------------------
% 2.44/1.30 % (3103101)------------------------------
% 2.44/1.30 % (3103098)------------------------------
% 2.44/1.30 % (3103098)------------------------------
% 2.44/1.30 % (3103100)Refutation found. Thanks to Tanya!
% 2.44/1.30 % SZS status Theorem for theBenchmark
% 2.44/1.30 % SZS output start Proof for theBenchmark
% See solution above
% 3.70/1.49 % (3103100)------------------------------
% 3.70/1.49 % (3103100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.70/1.50 % (3103100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.70/1.50 % (3103100)CaDiCaL version: 2.1.3
% 3.70/1.50 % (3103100)Termination reason: Refutation
% 3.70/1.50 % (3103100)Time elapsed: 0.015 s
% 3.70/1.50 % (3103100)Peak memory usage: 90 MB
% 3.70/1.50 % (3103100)Instructions burned: 21 (million)
% 3.70/1.50 % (3103100)------------------------------
% 3.70/1.50 % (3103100)------------------------------
% 3.70/1.50 % (3103090)Success in time 0.446 s
% 3.70/1.50 % Vampire exiting
%------------------------------------------------------------------------------