%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NLP009+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 : n012.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:55 PM UTC 2026
% Result : Theorem 2.55s 1.11s
% Output : Refutation 3.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 69
% Syntax : Number of formulae : 428 ( 37 unt; 68 def)
% Number of atoms : 2341 ( 131 equ)
% Maximal formula atoms : 112 ( 5 avg)
% Number of connectives : 3337 (1424 ~;1376 |; 467 &)
% ( 66 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 75 ( 6 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 90 ( 88 usr; 69 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 18 con; 0-0 aty)
% Number of variables : 351 ( 0 sgn 216 !; 135 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
( ( ? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( hollywood(X0)
& city(X0)
& event(X1)
& street(X2)
& way(X2)
& lonely(X2)
& chevy(X3)
& car(X3)
& white(X3)
& dirty(X3)
& old(X3)
& barrel(X1,X3)
& down(X1,X2)
& in(X1,X0)
& seat(X6)
& furniture(X6)
& front(X6)
& X4 != X5
& fellow(X4)
& man(X4)
& young(X4)
& fellow(X5)
& man(X5)
& young(X5)
& X4 = X7
& in(X7,X6)
& X5 = X8
& in(X8,X6) )
=> ? [X9,X10,X11,X12,X13,X14,X15,X16,X17] :
( hollywood(X9)
& city(X9)
& event(X10)
& chevy(X11)
& car(X11)
& white(X11)
& dirty(X11)
& old(X11)
& street(X12)
& way(X12)
& lonely(X12)
& barrel(X10,X11)
& down(X10,X12)
& in(X10,X9)
& seat(X15)
& furniture(X15)
& front(X15)
& X13 != X14
& fellow(X13)
& man(X13)
& young(X13)
& fellow(X14)
& man(X14)
& young(X14)
& X13 = X16
& in(X16,X15)
& X14 = X17
& in(X17,X15) ) )
& ( ? [X18,X19,X20,X21,X22,X23,X24,X25,X26] :
( hollywood(X18)
& city(X18)
& event(X19)
& chevy(X20)
& car(X20)
& white(X20)
& dirty(X20)
& old(X20)
& street(X21)
& way(X21)
& lonely(X21)
& barrel(X19,X20)
& down(X19,X21)
& in(X19,X18)
& seat(X24)
& furniture(X24)
& front(X24)
& X22 != X23
& fellow(X22)
& man(X22)
& young(X22)
& fellow(X23)
& man(X23)
& young(X23)
& X22 = X25
& in(X25,X24)
& X23 = X26
& in(X26,X24) )
=> ? [X27,X28,X29,X30,X31,X32,X33,X34,X35] :
( hollywood(X27)
& city(X27)
& event(X28)
& street(X29)
& way(X29)
& lonely(X29)
& chevy(X30)
& car(X30)
& white(X30)
& dirty(X30)
& old(X30)
& barrel(X28,X30)
& down(X28,X29)
& in(X28,X27)
& seat(X33)
& furniture(X33)
& front(X33)
& X31 != X32
& fellow(X31)
& man(X31)
& young(X31)
& fellow(X32)
& man(X32)
& young(X32)
& X31 = X34
& in(X34,X33)
& X32 = X35
& in(X35,X33) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f2,negated_conjecture,
~ ( ( ? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( hollywood(X0)
& city(X0)
& event(X1)
& street(X2)
& way(X2)
& lonely(X2)
& chevy(X3)
& car(X3)
& white(X3)
& dirty(X3)
& old(X3)
& barrel(X1,X3)
& down(X1,X2)
& in(X1,X0)
& seat(X6)
& furniture(X6)
& front(X6)
& X4 != X5
& fellow(X4)
& man(X4)
& young(X4)
& fellow(X5)
& man(X5)
& young(X5)
& X4 = X7
& in(X7,X6)
& X5 = X8
& in(X8,X6) )
=> ? [X9,X10,X11,X12,X13,X14,X15,X16,X17] :
( hollywood(X9)
& city(X9)
& event(X10)
& chevy(X11)
& car(X11)
& white(X11)
& dirty(X11)
& old(X11)
& street(X12)
& way(X12)
& lonely(X12)
& barrel(X10,X11)
& down(X10,X12)
& in(X10,X9)
& seat(X15)
& furniture(X15)
& front(X15)
& X13 != X14
& fellow(X13)
& man(X13)
& young(X13)
& fellow(X14)
& man(X14)
& young(X14)
& X13 = X16
& in(X16,X15)
& X14 = X17
& in(X17,X15) ) )
& ( ? [X18,X19,X20,X21,X22,X23,X24,X25,X26] :
( hollywood(X18)
& city(X18)
& event(X19)
& chevy(X20)
& car(X20)
& white(X20)
& dirty(X20)
& old(X20)
& street(X21)
& way(X21)
& lonely(X21)
& barrel(X19,X20)
& down(X19,X21)
& in(X19,X18)
& seat(X24)
& furniture(X24)
& front(X24)
& X22 != X23
& fellow(X22)
& man(X22)
& young(X22)
& fellow(X23)
& man(X23)
& young(X23)
& X22 = X25
& in(X25,X24)
& X23 = X26
& in(X26,X24) )
=> ? [X27,X28,X29,X30,X31,X32,X33,X34,X35] :
( hollywood(X27)
& city(X27)
& event(X28)
& street(X29)
& way(X29)
& lonely(X29)
& chevy(X30)
& car(X30)
& white(X30)
& dirty(X30)
& old(X30)
& barrel(X28,X30)
& down(X28,X29)
& in(X28,X27)
& seat(X33)
& furniture(X33)
& front(X33)
& X31 != X32
& fellow(X31)
& man(X31)
& young(X31)
& fellow(X32)
& man(X32)
& young(X32)
& X31 = X34
& in(X34,X33)
& X32 = X35
& in(X35,X33) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
( ( ! [X9,X10,X11,X12,X13,X14,X15,X16,X17] :
( ~ hollywood(X9)
| ~ city(X9)
| ~ event(X10)
| ~ chevy(X11)
| ~ car(X11)
| ~ white(X11)
| ~ dirty(X11)
| ~ old(X11)
| ~ street(X12)
| ~ way(X12)
| ~ lonely(X12)
| ~ barrel(X10,X11)
| ~ down(X10,X12)
| ~ in(X10,X9)
| ~ seat(X15)
| ~ furniture(X15)
| ~ front(X15)
| X13 = X14
| ~ fellow(X13)
| ~ man(X13)
| ~ young(X13)
| ~ fellow(X14)
| ~ man(X14)
| ~ young(X14)
| X13 != X16
| ~ in(X16,X15)
| X14 != X17
| ~ in(X17,X15) )
& ? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( hollywood(X0)
& city(X0)
& event(X1)
& street(X2)
& way(X2)
& lonely(X2)
& chevy(X3)
& car(X3)
& white(X3)
& dirty(X3)
& old(X3)
& barrel(X1,X3)
& down(X1,X2)
& in(X1,X0)
& seat(X6)
& furniture(X6)
& front(X6)
& X4 != X5
& fellow(X4)
& man(X4)
& young(X4)
& fellow(X5)
& man(X5)
& young(X5)
& X4 = X7
& in(X7,X6)
& X5 = X8
& in(X8,X6) ) )
| ( ! [X27,X28,X29,X30,X31,X32,X33,X34,X35] :
( ~ hollywood(X27)
| ~ city(X27)
| ~ event(X28)
| ~ street(X29)
| ~ way(X29)
| ~ lonely(X29)
| ~ chevy(X30)
| ~ car(X30)
| ~ white(X30)
| ~ dirty(X30)
| ~ old(X30)
| ~ barrel(X28,X30)
| ~ down(X28,X29)
| ~ in(X28,X27)
| ~ seat(X33)
| ~ furniture(X33)
| ~ front(X33)
| X31 = X32
| ~ fellow(X31)
| ~ man(X31)
| ~ young(X31)
| ~ fellow(X32)
| ~ man(X32)
| ~ young(X32)
| X31 != X34
| ~ in(X34,X33)
| X32 != X35
| ~ in(X35,X33) )
& ? [X18,X19,X20,X21,X22,X23,X24,X25,X26] :
( hollywood(X18)
& city(X18)
& event(X19)
& chevy(X20)
& car(X20)
& white(X20)
& dirty(X20)
& old(X20)
& street(X21)
& way(X21)
& lonely(X21)
& barrel(X19,X20)
& down(X19,X21)
& in(X19,X18)
& seat(X24)
& furniture(X24)
& front(X24)
& X22 != X23
& fellow(X22)
& man(X22)
& young(X22)
& fellow(X23)
& man(X23)
& young(X23)
& X22 = X25
& in(X25,X24)
& X23 = X26
& in(X26,X24) ) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f4,definition,
( ? [X18,X19,X20,X21,X22,X23,X24,X25,X26] :
( hollywood(X18)
& city(X18)
& event(X19)
& chevy(X20)
& car(X20)
& white(X20)
& dirty(X20)
& old(X20)
& street(X21)
& way(X21)
& lonely(X21)
& barrel(X19,X20)
& down(X19,X21)
& in(X19,X18)
& seat(X24)
& furniture(X24)
& front(X24)
& X22 != X23
& fellow(X22)
& man(X22)
& young(X22)
& fellow(X23)
& man(X23)
& young(X23)
& X22 = X25
& in(X25,X24)
& X23 = X26
& in(X26,X24) )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f5,definition,
( ? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( hollywood(X0)
& city(X0)
& event(X1)
& street(X2)
& way(X2)
& lonely(X2)
& chevy(X3)
& car(X3)
& white(X3)
& dirty(X3)
& old(X3)
& barrel(X1,X3)
& down(X1,X2)
& in(X1,X0)
& seat(X6)
& furniture(X6)
& front(X6)
& X4 != X5
& fellow(X4)
& man(X4)
& young(X4)
& fellow(X5)
& man(X5)
& young(X5)
& X4 = X7
& in(X7,X6)
& X5 = X8
& in(X8,X6) )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f6,plain,
( ( ! [X9,X10,X11,X12,X13,X14,X15,X16,X17] :
( ~ hollywood(X9)
| ~ city(X9)
| ~ event(X10)
| ~ chevy(X11)
| ~ car(X11)
| ~ white(X11)
| ~ dirty(X11)
| ~ old(X11)
| ~ street(X12)
| ~ way(X12)
| ~ lonely(X12)
| ~ barrel(X10,X11)
| ~ down(X10,X12)
| ~ in(X10,X9)
| ~ seat(X15)
| ~ furniture(X15)
| ~ front(X15)
| X13 = X14
| ~ fellow(X13)
| ~ man(X13)
| ~ young(X13)
| ~ fellow(X14)
| ~ man(X14)
| ~ young(X14)
| X13 != X16
| ~ in(X16,X15)
| X14 != X17
| ~ in(X17,X15) )
& sP1 )
| ( ! [X27,X28,X29,X30,X31,X32,X33,X34,X35] :
( ~ hollywood(X27)
| ~ city(X27)
| ~ event(X28)
| ~ street(X29)
| ~ way(X29)
| ~ lonely(X29)
| ~ chevy(X30)
| ~ car(X30)
| ~ white(X30)
| ~ dirty(X30)
| ~ old(X30)
| ~ barrel(X28,X30)
| ~ down(X28,X29)
| ~ in(X28,X27)
| ~ seat(X33)
| ~ furniture(X33)
| ~ front(X33)
| X31 = X32
| ~ fellow(X31)
| ~ man(X31)
| ~ young(X31)
| ~ fellow(X32)
| ~ man(X32)
| ~ young(X32)
| X31 != X34
| ~ in(X34,X33)
| X32 != X35
| ~ in(X35,X33) )
& sP0 ) ),
inference(definition_folding,[],[f3,f5,f4]) ).
fof(f7,plain,
( ? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( hollywood(X0)
& city(X0)
& event(X1)
& street(X2)
& way(X2)
& lonely(X2)
& chevy(X3)
& car(X3)
& white(X3)
& dirty(X3)
& old(X3)
& barrel(X1,X3)
& down(X1,X2)
& in(X1,X0)
& seat(X6)
& furniture(X6)
& front(X6)
& X4 != X5
& fellow(X4)
& man(X4)
& young(X4)
& fellow(X5)
& man(X5)
& young(X5)
& X4 = X7
& in(X7,X6)
& X5 = X8
& in(X8,X6) )
| ~ sP1 ),
inference(nnf_transformation,[],[f5]) ).
fof(f8,plain,
( ( hollywood(sK2)
& city(sK2)
& event(sK3)
& street(sK4)
& way(sK4)
& lonely(sK4)
& chevy(sK5)
& car(sK5)
& white(sK5)
& dirty(sK5)
& old(sK5)
& barrel(sK3,sK5)
& down(sK3,sK4)
& in(sK3,sK2)
& seat(sK8)
& furniture(sK8)
& front(sK8)
& sK6 != sK7
& fellow(sK6)
& man(sK6)
& young(sK6)
& fellow(sK7)
& man(sK7)
& young(sK7)
& sK6 = sK9
& in(sK9,sK8)
& sK7 = sK10
& in(sK10,sK8) )
| ~ sP1 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10]),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)],[f7]) ).
fof(f9,plain,
( ? [X18,X19,X20,X21,X22,X23,X24,X25,X26] :
( hollywood(X18)
& city(X18)
& event(X19)
& chevy(X20)
& car(X20)
& white(X20)
& dirty(X20)
& old(X20)
& street(X21)
& way(X21)
& lonely(X21)
& barrel(X19,X20)
& down(X19,X21)
& in(X19,X18)
& seat(X24)
& furniture(X24)
& front(X24)
& X22 != X23
& fellow(X22)
& man(X22)
& young(X22)
& fellow(X23)
& man(X23)
& young(X23)
& X22 = X25
& in(X25,X24)
& X23 = X26
& in(X26,X24) )
| ~ sP0 ),
inference(nnf_transformation,[],[f4]) ).
fof(f10,plain,
( ? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( hollywood(X0)
& city(X0)
& event(X1)
& chevy(X2)
& car(X2)
& white(X2)
& dirty(X2)
& old(X2)
& street(X3)
& way(X3)
& lonely(X3)
& barrel(X1,X2)
& down(X1,X3)
& in(X1,X0)
& seat(X6)
& furniture(X6)
& front(X6)
& X4 != X5
& fellow(X4)
& man(X4)
& young(X4)
& fellow(X5)
& man(X5)
& young(X5)
& X4 = X7
& in(X7,X6)
& X5 = X8
& in(X8,X6) )
| ~ sP0 ),
inference(rectify,[],[f9]) ).
fof(f11,plain,
( ( hollywood(sK11)
& city(sK11)
& event(sK12)
& chevy(sK13)
& car(sK13)
& white(sK13)
& dirty(sK13)
& old(sK13)
& street(sK14)
& way(sK14)
& lonely(sK14)
& barrel(sK12,sK13)
& down(sK12,sK14)
& in(sK12,sK11)
& seat(sK17)
& furniture(sK17)
& front(sK17)
& sK15 != sK16
& fellow(sK15)
& man(sK15)
& young(sK15)
& fellow(sK16)
& man(sK16)
& young(sK16)
& sK15 = sK18
& in(sK18,sK17)
& sK16 = sK19
& in(sK19,sK17) )
| ~ sP0 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11,sK12,sK13,sK14,sK15,sK16,sK17,sK18,sK19]),skolemize(X0,sK11),skolemize(X1,sK12),skolemize(X2,sK13),skolemize(X3,sK14),skolemize(X4,sK15),skolemize(X5,sK16),skolemize(X6,sK17),skolemize(X7,sK18),skolemize(X8,sK19)],[f10]) ).
fof(f12,plain,
( ( ! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ~ hollywood(X0)
| ~ city(X0)
| ~ event(X1)
| ~ chevy(X2)
| ~ car(X2)
| ~ white(X2)
| ~ dirty(X2)
| ~ old(X2)
| ~ street(X3)
| ~ way(X3)
| ~ lonely(X3)
| ~ barrel(X1,X2)
| ~ down(X1,X3)
| ~ in(X1,X0)
| ~ seat(X6)
| ~ furniture(X6)
| ~ front(X6)
| X4 = X5
| ~ fellow(X4)
| ~ man(X4)
| ~ young(X4)
| ~ fellow(X5)
| ~ man(X5)
| ~ young(X5)
| X4 != X7
| ~ in(X7,X6)
| X5 != X8
| ~ in(X8,X6) )
& sP1 )
| ( ! [X9,X10,X11,X12,X13,X14,X15,X16,X17] :
( ~ hollywood(X9)
| ~ city(X9)
| ~ event(X10)
| ~ street(X11)
| ~ way(X11)
| ~ lonely(X11)
| ~ chevy(X12)
| ~ car(X12)
| ~ white(X12)
| ~ dirty(X12)
| ~ old(X12)
| ~ barrel(X10,X12)
| ~ down(X10,X11)
| ~ in(X10,X9)
| ~ seat(X15)
| ~ furniture(X15)
| ~ front(X15)
| X13 = X14
| ~ fellow(X13)
| ~ man(X13)
| ~ young(X13)
| ~ fellow(X14)
| ~ man(X14)
| ~ young(X14)
| X13 != X16
| ~ in(X16,X15)
| X14 != X17
| ~ in(X17,X15) )
& sP0 ) ),
inference(rectify,[],[f6]) ).
fof(f13,plain,
( in(sK10,sK8)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f14,plain,
( sK7 = sK10
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f15,plain,
( in(sK9,sK8)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f16,plain,
( sK6 = sK9
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f17,plain,
( young(sK7)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f18,plain,
( man(sK7)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f19,plain,
( fellow(sK7)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f20,plain,
( young(sK6)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f21,plain,
( man(sK6)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f22,plain,
( fellow(sK6)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f23,plain,
( sK6 != sK7
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f24,plain,
( front(sK8)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f25,plain,
( furniture(sK8)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f26,plain,
( seat(sK8)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f27,plain,
( in(sK3,sK2)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f28,plain,
( down(sK3,sK4)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f29,plain,
( barrel(sK3,sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f30,plain,
( old(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f31,plain,
( dirty(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f32,plain,
( white(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f33,plain,
( car(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f34,plain,
( chevy(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f35,plain,
( lonely(sK4)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f36,plain,
( way(sK4)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f37,plain,
( street(sK4)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f38,plain,
( event(sK3)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f39,plain,
( city(sK2)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f40,plain,
( hollywood(sK2)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f41,plain,
( in(sK19,sK17)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f42,plain,
( sK16 = sK19
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f43,plain,
( in(sK18,sK17)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f44,plain,
( sK15 = sK18
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f45,plain,
( young(sK16)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f46,plain,
( man(sK16)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f47,plain,
( fellow(sK16)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f48,plain,
( young(sK15)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f49,plain,
( man(sK15)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f50,plain,
( fellow(sK15)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f51,plain,
( sK15 != sK16
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f52,plain,
( front(sK17)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f53,plain,
( furniture(sK17)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f54,plain,
( seat(sK17)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f55,plain,
( in(sK12,sK11)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f56,plain,
( down(sK12,sK14)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f57,plain,
( barrel(sK12,sK13)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f58,plain,
( lonely(sK14)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f59,plain,
( way(sK14)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f60,plain,
( street(sK14)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f61,plain,
( old(sK13)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f62,plain,
( dirty(sK13)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f63,plain,
( white(sK13)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f64,plain,
( car(sK13)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f65,plain,
( chevy(sK13)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f66,plain,
( event(sK12)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f67,plain,
( city(sK11)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f68,plain,
( hollywood(sK11)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f69,plain,
( sP1
| sP0 ),
inference(cnf_transformation,[],[f12]) ).
fof(f72,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X16,X17,X15,X5,X12,X13] :
( ~ hollywood(X0)
| ~ city(X0)
| ~ event(X1)
| ~ chevy(X2)
| ~ car(X2)
| ~ white(X2)
| ~ dirty(X2)
| ~ old(X2)
| ~ street(X3)
| ~ way(X3)
| ~ lonely(X3)
| ~ barrel(X1,X2)
| ~ down(X1,X3)
| ~ in(X1,X0)
| ~ seat(X6)
| ~ furniture(X6)
| ~ front(X6)
| X4 = X5
| ~ fellow(X4)
| ~ man(X4)
| ~ young(X4)
| ~ fellow(X5)
| ~ man(X5)
| ~ young(X5)
| X4 != X7
| ~ in(X7,X6)
| X5 != X8
| ~ in(X8,X6)
| ~ hollywood(X9)
| ~ city(X9)
| ~ event(X10)
| ~ street(X11)
| ~ way(X11)
| ~ lonely(X11)
| ~ chevy(X12)
| ~ car(X12)
| ~ white(X12)
| ~ dirty(X12)
| ~ old(X12)
| ~ barrel(X10,X12)
| ~ down(X10,X11)
| ~ in(X10,X9)
| ~ seat(X15)
| ~ furniture(X15)
| ~ front(X15)
| X13 = X14
| ~ fellow(X13)
| ~ man(X13)
| ~ young(X13)
| ~ fellow(X14)
| ~ man(X14)
| ~ young(X14)
| X13 != X16
| ~ in(X16,X15)
| X14 != X17
| ~ in(X17,X15) ),
inference(cnf_transformation,[],[f12]) ).
fof(f73,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X16,X17,X15,X5,X12,X13] :
( ~ hollywood(X0)
| ~ city(X0)
| ~ event(X1)
| ~ chevy(X2)
| ~ car(X2)
| ~ white(X2)
| ~ dirty(X2)
| ~ old(X2)
| ~ street(X3)
| ~ way(X3)
| ~ lonely(X3)
| ~ barrel(X1,X2)
| ~ down(X1,X3)
| ~ in(X1,X0)
| ~ seat(X6)
| ~ furniture(X6)
| ~ front(X6)
| X5 = X7
| ~ fellow(X7)
| ~ man(X7)
| ~ young(X7)
| ~ fellow(X5)
| ~ man(X5)
| ~ young(X5)
| ~ in(X7,X6)
| X5 != X8
| ~ in(X8,X6)
| ~ hollywood(X9)
| ~ city(X9)
| ~ event(X10)
| ~ street(X11)
| ~ way(X11)
| ~ lonely(X11)
| ~ chevy(X12)
| ~ car(X12)
| ~ white(X12)
| ~ dirty(X12)
| ~ old(X12)
| ~ barrel(X10,X12)
| ~ down(X10,X11)
| ~ in(X10,X9)
| ~ seat(X15)
| ~ furniture(X15)
| ~ front(X15)
| X13 = X14
| ~ fellow(X13)
| ~ man(X13)
| ~ young(X13)
| ~ fellow(X14)
| ~ man(X14)
| ~ young(X14)
| X13 != X16
| ~ in(X16,X15)
| X14 != X17
| ~ in(X17,X15) ),
inference(equality_resolution,[],[f72]) ).
fof(f74,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X16,X17,X15,X12,X13] :
( ~ hollywood(X0)
| ~ city(X0)
| ~ event(X1)
| ~ chevy(X2)
| ~ car(X2)
| ~ white(X2)
| ~ dirty(X2)
| ~ old(X2)
| ~ street(X3)
| ~ way(X3)
| ~ lonely(X3)
| ~ barrel(X1,X2)
| ~ down(X1,X3)
| ~ in(X1,X0)
| ~ seat(X6)
| ~ furniture(X6)
| ~ front(X6)
| X7 = X8
| ~ fellow(X7)
| ~ man(X7)
| ~ young(X7)
| ~ fellow(X8)
| ~ man(X8)
| ~ young(X8)
| ~ in(X7,X6)
| ~ in(X8,X6)
| ~ hollywood(X9)
| ~ city(X9)
| ~ event(X10)
| ~ street(X11)
| ~ way(X11)
| ~ lonely(X11)
| ~ chevy(X12)
| ~ car(X12)
| ~ white(X12)
| ~ dirty(X12)
| ~ old(X12)
| ~ barrel(X10,X12)
| ~ down(X10,X11)
| ~ in(X10,X9)
| ~ seat(X15)
| ~ furniture(X15)
| ~ front(X15)
| X13 = X14
| ~ fellow(X13)
| ~ man(X13)
| ~ young(X13)
| ~ fellow(X14)
| ~ man(X14)
| ~ young(X14)
| X13 != X16
| ~ in(X16,X15)
| X14 != X17
| ~ in(X17,X15) ),
inference(equality_resolution,[],[f73]) ).
fof(f75,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X16,X17,X15,X12] :
( ~ hollywood(X0)
| ~ city(X0)
| ~ event(X1)
| ~ chevy(X2)
| ~ car(X2)
| ~ white(X2)
| ~ dirty(X2)
| ~ old(X2)
| ~ street(X3)
| ~ way(X3)
| ~ lonely(X3)
| ~ barrel(X1,X2)
| ~ down(X1,X3)
| ~ in(X1,X0)
| ~ seat(X6)
| ~ furniture(X6)
| ~ front(X6)
| X7 = X8
| ~ fellow(X7)
| ~ man(X7)
| ~ young(X7)
| ~ fellow(X8)
| ~ man(X8)
| ~ young(X8)
| ~ in(X7,X6)
| ~ in(X8,X6)
| ~ hollywood(X9)
| ~ city(X9)
| ~ event(X10)
| ~ street(X11)
| ~ way(X11)
| ~ lonely(X11)
| ~ chevy(X12)
| ~ car(X12)
| ~ white(X12)
| ~ dirty(X12)
| ~ old(X12)
| ~ barrel(X10,X12)
| ~ down(X10,X11)
| ~ in(X10,X9)
| ~ seat(X15)
| ~ furniture(X15)
| ~ front(X15)
| X14 = X16
| ~ fellow(X16)
| ~ man(X16)
| ~ young(X16)
| ~ fellow(X14)
| ~ man(X14)
| ~ young(X14)
| ~ in(X16,X15)
| X14 != X17
| ~ in(X17,X15) ),
inference(equality_resolution,[],[f74]) ).
fof(f76,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X16,X17,X15,X12] :
( ~ hollywood(X0)
| ~ city(X0)
| ~ event(X1)
| ~ chevy(X2)
| ~ car(X2)
| ~ white(X2)
| ~ dirty(X2)
| ~ old(X2)
| ~ street(X3)
| ~ way(X3)
| ~ lonely(X3)
| ~ barrel(X1,X2)
| ~ down(X1,X3)
| ~ in(X1,X0)
| ~ seat(X6)
| ~ furniture(X6)
| ~ front(X6)
| X7 = X8
| ~ fellow(X7)
| ~ man(X7)
| ~ young(X7)
| ~ fellow(X8)
| ~ man(X8)
| ~ young(X8)
| ~ in(X7,X6)
| ~ in(X8,X6)
| ~ hollywood(X9)
| ~ city(X9)
| ~ event(X10)
| ~ street(X11)
| ~ way(X11)
| ~ lonely(X11)
| ~ chevy(X12)
| ~ car(X12)
| ~ white(X12)
| ~ dirty(X12)
| ~ old(X12)
| ~ barrel(X10,X12)
| ~ down(X10,X11)
| ~ in(X10,X9)
| ~ seat(X15)
| ~ furniture(X15)
| ~ front(X15)
| X16 = X17
| ~ fellow(X16)
| ~ man(X16)
| ~ young(X16)
| ~ fellow(X17)
| ~ man(X17)
| ~ young(X17)
| ~ in(X16,X15)
| ~ in(X17,X15) ),
inference(equality_resolution,[],[f75]) ).
fof(f82,definition,
( spl20_1
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl20_1])],[avatar_definition]) ).
fof(f86,definition,
( spl20_2
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl20_2])],[avatar_definition]) ).
fof(f89,plain,
( spl20_1
| spl20_2 ),
inference(avatar_split_clause,[],[f69,f86,f82]) ).
fof(f91,definition,
( spl20_3
<=> ! [X16,X17,X15] :
( ~ seat(X15)
| ~ in(X17,X15)
| X16 = X17
| ~ in(X16,X15)
| ~ young(X17)
| ~ man(X17)
| ~ fellow(X17)
| ~ young(X16)
| ~ man(X16)
| ~ fellow(X16)
| ~ front(X15)
| ~ furniture(X15) ) ),
introduced(definition,[new_symbols(definition,[spl20_3])],[avatar_definition]) ).
fof(f92,plain,
( ! [X16,X17,X15] :
( ~ man(X17)
| ~ in(X17,X15)
| X16 = X17
| ~ in(X16,X15)
| ~ young(X17)
| ~ seat(X15)
| ~ fellow(X17)
| ~ young(X16)
| ~ man(X16)
| ~ fellow(X16)
| ~ front(X15)
| ~ furniture(X15) )
| ~ spl20_3 ),
inference(avatar_component_clause,[],[f91]) ).
fof(f94,definition,
( spl20_4
<=> ! [X10,X11,X12,X9] :
( ~ hollywood(X9)
| ~ event(X10)
| ~ in(X10,X9)
| ~ down(X10,X11)
| ~ barrel(X10,X12)
| ~ chevy(X12)
| ~ old(X12)
| ~ dirty(X12)
| ~ white(X12)
| ~ car(X12)
| ~ street(X11)
| ~ lonely(X11)
| ~ way(X11)
| ~ city(X9) ) ),
introduced(definition,[new_symbols(definition,[spl20_4])],[avatar_definition]) ).
fof(f95,plain,
( ! [X10,X11,X9,X12] :
( ~ old(X12)
| ~ event(X10)
| ~ in(X10,X9)
| ~ down(X10,X11)
| ~ barrel(X10,X12)
| ~ chevy(X12)
| ~ hollywood(X9)
| ~ dirty(X12)
| ~ white(X12)
| ~ car(X12)
| ~ street(X11)
| ~ lonely(X11)
| ~ way(X11)
| ~ city(X9) )
| ~ spl20_4 ),
inference(avatar_component_clause,[],[f94]) ).
fof(f98,plain,
( spl20_3
| spl20_4
| spl20_3
| spl20_4 ),
inference(avatar_split_clause,[],[f76,f94,f91,f94,f91]) ).
fof(f100,definition,
( spl20_5
<=> in(sK19,sK17) ),
introduced(definition,[new_symbols(definition,[spl20_5])],[avatar_definition]) ).
fof(f102,plain,
( in(sK19,sK17)
| ~ spl20_5 ),
inference(avatar_component_clause,[],[f100]) ).
fof(f103,plain,
( ~ spl20_1
| spl20_5 ),
inference(avatar_split_clause,[],[f41,f100,f82]) ).
fof(f105,definition,
( spl20_6
<=> sK16 = sK19 ),
introduced(definition,[new_symbols(definition,[spl20_6])],[avatar_definition]) ).
fof(f107,plain,
( sK16 = sK19
| ~ spl20_6 ),
inference(avatar_component_clause,[],[f105]) ).
fof(f108,plain,
( ~ spl20_1
| spl20_6 ),
inference(avatar_split_clause,[],[f42,f105,f82]) ).
fof(f110,definition,
( spl20_7
<=> in(sK18,sK17) ),
introduced(definition,[new_symbols(definition,[spl20_7])],[avatar_definition]) ).
fof(f112,plain,
( in(sK18,sK17)
| ~ spl20_7 ),
inference(avatar_component_clause,[],[f110]) ).
fof(f113,plain,
( ~ spl20_1
| spl20_7 ),
inference(avatar_split_clause,[],[f43,f110,f82]) ).
fof(f115,definition,
( spl20_8
<=> sK15 = sK18 ),
introduced(definition,[new_symbols(definition,[spl20_8])],[avatar_definition]) ).
fof(f117,plain,
( sK15 = sK18
| ~ spl20_8 ),
inference(avatar_component_clause,[],[f115]) ).
fof(f118,plain,
( ~ spl20_1
| spl20_8 ),
inference(avatar_split_clause,[],[f44,f115,f82]) ).
fof(f120,definition,
( spl20_9
<=> young(sK16) ),
introduced(definition,[new_symbols(definition,[spl20_9])],[avatar_definition]) ).
fof(f122,plain,
( young(sK16)
| ~ spl20_9 ),
inference(avatar_component_clause,[],[f120]) ).
fof(f123,plain,
( ~ spl20_1
| spl20_9 ),
inference(avatar_split_clause,[],[f45,f120,f82]) ).
fof(f125,definition,
( spl20_10
<=> man(sK16) ),
introduced(definition,[new_symbols(definition,[spl20_10])],[avatar_definition]) ).
fof(f127,plain,
( man(sK16)
| ~ spl20_10 ),
inference(avatar_component_clause,[],[f125]) ).
fof(f128,plain,
( ~ spl20_1
| spl20_10 ),
inference(avatar_split_clause,[],[f46,f125,f82]) ).
fof(f130,definition,
( spl20_11
<=> fellow(sK16) ),
introduced(definition,[new_symbols(definition,[spl20_11])],[avatar_definition]) ).
fof(f132,plain,
( fellow(sK16)
| ~ spl20_11 ),
inference(avatar_component_clause,[],[f130]) ).
fof(f133,plain,
( ~ spl20_1
| spl20_11 ),
inference(avatar_split_clause,[],[f47,f130,f82]) ).
fof(f135,definition,
( spl20_12
<=> young(sK15) ),
introduced(definition,[new_symbols(definition,[spl20_12])],[avatar_definition]) ).
fof(f137,plain,
( young(sK15)
| ~ spl20_12 ),
inference(avatar_component_clause,[],[f135]) ).
fof(f138,plain,
( ~ spl20_1
| spl20_12 ),
inference(avatar_split_clause,[],[f48,f135,f82]) ).
fof(f140,definition,
( spl20_13
<=> man(sK15) ),
introduced(definition,[new_symbols(definition,[spl20_13])],[avatar_definition]) ).
fof(f142,plain,
( man(sK15)
| ~ spl20_13 ),
inference(avatar_component_clause,[],[f140]) ).
fof(f143,plain,
( ~ spl20_1
| spl20_13 ),
inference(avatar_split_clause,[],[f49,f140,f82]) ).
fof(f145,definition,
( spl20_14
<=> fellow(sK15) ),
introduced(definition,[new_symbols(definition,[spl20_14])],[avatar_definition]) ).
fof(f148,plain,
( ~ spl20_1
| spl20_14 ),
inference(avatar_split_clause,[],[f50,f145,f82]) ).
fof(f150,definition,
( spl20_15
<=> sK15 = sK16 ),
introduced(definition,[new_symbols(definition,[spl20_15])],[avatar_definition]) ).
fof(f152,plain,
( sK15 != sK16
| spl20_15 ),
inference(avatar_component_clause,[],[f150]) ).
fof(f153,plain,
( ~ spl20_1
| ~ spl20_15 ),
inference(avatar_split_clause,[],[f51,f150,f82]) ).
fof(f155,definition,
( spl20_16
<=> front(sK17) ),
introduced(definition,[new_symbols(definition,[spl20_16])],[avatar_definition]) ).
fof(f157,plain,
( front(sK17)
| ~ spl20_16 ),
inference(avatar_component_clause,[],[f155]) ).
fof(f158,plain,
( ~ spl20_1
| spl20_16 ),
inference(avatar_split_clause,[],[f52,f155,f82]) ).
fof(f160,definition,
( spl20_17
<=> furniture(sK17) ),
introduced(definition,[new_symbols(definition,[spl20_17])],[avatar_definition]) ).
fof(f162,plain,
( furniture(sK17)
| ~ spl20_17 ),
inference(avatar_component_clause,[],[f160]) ).
fof(f163,plain,
( ~ spl20_1
| spl20_17 ),
inference(avatar_split_clause,[],[f53,f160,f82]) ).
fof(f165,definition,
( spl20_18
<=> seat(sK17) ),
introduced(definition,[new_symbols(definition,[spl20_18])],[avatar_definition]) ).
fof(f167,plain,
( seat(sK17)
| ~ spl20_18 ),
inference(avatar_component_clause,[],[f165]) ).
fof(f168,plain,
( ~ spl20_1
| spl20_18 ),
inference(avatar_split_clause,[],[f54,f165,f82]) ).
fof(f170,definition,
( spl20_19
<=> in(sK12,sK11) ),
introduced(definition,[new_symbols(definition,[spl20_19])],[avatar_definition]) ).
fof(f172,plain,
( in(sK12,sK11)
| ~ spl20_19 ),
inference(avatar_component_clause,[],[f170]) ).
fof(f173,plain,
( ~ spl20_1
| spl20_19 ),
inference(avatar_split_clause,[],[f55,f170,f82]) ).
fof(f175,definition,
( spl20_20
<=> down(sK12,sK14) ),
introduced(definition,[new_symbols(definition,[spl20_20])],[avatar_definition]) ).
fof(f177,plain,
( down(sK12,sK14)
| ~ spl20_20 ),
inference(avatar_component_clause,[],[f175]) ).
fof(f178,plain,
( ~ spl20_1
| spl20_20 ),
inference(avatar_split_clause,[],[f56,f175,f82]) ).
fof(f180,definition,
( spl20_21
<=> barrel(sK12,sK13) ),
introduced(definition,[new_symbols(definition,[spl20_21])],[avatar_definition]) ).
fof(f182,plain,
( barrel(sK12,sK13)
| ~ spl20_21 ),
inference(avatar_component_clause,[],[f180]) ).
fof(f183,plain,
( ~ spl20_1
| spl20_21 ),
inference(avatar_split_clause,[],[f57,f180,f82]) ).
fof(f185,definition,
( spl20_22
<=> lonely(sK14) ),
introduced(definition,[new_symbols(definition,[spl20_22])],[avatar_definition]) ).
fof(f187,plain,
( lonely(sK14)
| ~ spl20_22 ),
inference(avatar_component_clause,[],[f185]) ).
fof(f188,plain,
( ~ spl20_1
| spl20_22 ),
inference(avatar_split_clause,[],[f58,f185,f82]) ).
fof(f190,definition,
( spl20_23
<=> way(sK14) ),
introduced(definition,[new_symbols(definition,[spl20_23])],[avatar_definition]) ).
fof(f192,plain,
( way(sK14)
| ~ spl20_23 ),
inference(avatar_component_clause,[],[f190]) ).
fof(f193,plain,
( ~ spl20_1
| spl20_23 ),
inference(avatar_split_clause,[],[f59,f190,f82]) ).
fof(f195,definition,
( spl20_24
<=> street(sK14) ),
introduced(definition,[new_symbols(definition,[spl20_24])],[avatar_definition]) ).
fof(f197,plain,
( street(sK14)
| ~ spl20_24 ),
inference(avatar_component_clause,[],[f195]) ).
fof(f198,plain,
( ~ spl20_1
| spl20_24 ),
inference(avatar_split_clause,[],[f60,f195,f82]) ).
fof(f200,definition,
( spl20_25
<=> old(sK13) ),
introduced(definition,[new_symbols(definition,[spl20_25])],[avatar_definition]) ).
fof(f202,plain,
( old(sK13)
| ~ spl20_25 ),
inference(avatar_component_clause,[],[f200]) ).
fof(f203,plain,
( ~ spl20_1
| spl20_25 ),
inference(avatar_split_clause,[],[f61,f200,f82]) ).
fof(f205,definition,
( spl20_26
<=> dirty(sK13) ),
introduced(definition,[new_symbols(definition,[spl20_26])],[avatar_definition]) ).
fof(f207,plain,
( dirty(sK13)
| ~ spl20_26 ),
inference(avatar_component_clause,[],[f205]) ).
fof(f208,plain,
( ~ spl20_1
| spl20_26 ),
inference(avatar_split_clause,[],[f62,f205,f82]) ).
fof(f210,definition,
( spl20_27
<=> white(sK13) ),
introduced(definition,[new_symbols(definition,[spl20_27])],[avatar_definition]) ).
fof(f212,plain,
( white(sK13)
| ~ spl20_27 ),
inference(avatar_component_clause,[],[f210]) ).
fof(f213,plain,
( ~ spl20_1
| spl20_27 ),
inference(avatar_split_clause,[],[f63,f210,f82]) ).
fof(f215,definition,
( spl20_28
<=> car(sK13) ),
introduced(definition,[new_symbols(definition,[spl20_28])],[avatar_definition]) ).
fof(f217,plain,
( car(sK13)
| ~ spl20_28 ),
inference(avatar_component_clause,[],[f215]) ).
fof(f218,plain,
( ~ spl20_1
| spl20_28 ),
inference(avatar_split_clause,[],[f64,f215,f82]) ).
fof(f220,definition,
( spl20_29
<=> chevy(sK13) ),
introduced(definition,[new_symbols(definition,[spl20_29])],[avatar_definition]) ).
fof(f222,plain,
( chevy(sK13)
| ~ spl20_29 ),
inference(avatar_component_clause,[],[f220]) ).
fof(f223,plain,
( ~ spl20_1
| spl20_29 ),
inference(avatar_split_clause,[],[f65,f220,f82]) ).
fof(f225,definition,
( spl20_30
<=> event(sK12) ),
introduced(definition,[new_symbols(definition,[spl20_30])],[avatar_definition]) ).
fof(f227,plain,
( event(sK12)
| ~ spl20_30 ),
inference(avatar_component_clause,[],[f225]) ).
fof(f228,plain,
( ~ spl20_1
| spl20_30 ),
inference(avatar_split_clause,[],[f66,f225,f82]) ).
fof(f230,definition,
( spl20_31
<=> city(sK11) ),
introduced(definition,[new_symbols(definition,[spl20_31])],[avatar_definition]) ).
fof(f232,plain,
( city(sK11)
| ~ spl20_31 ),
inference(avatar_component_clause,[],[f230]) ).
fof(f233,plain,
( ~ spl20_1
| spl20_31 ),
inference(avatar_split_clause,[],[f67,f230,f82]) ).
fof(f235,definition,
( spl20_32
<=> hollywood(sK11) ),
introduced(definition,[new_symbols(definition,[spl20_32])],[avatar_definition]) ).
fof(f237,plain,
( hollywood(sK11)
| ~ spl20_32 ),
inference(avatar_component_clause,[],[f235]) ).
fof(f238,plain,
( ~ spl20_1
| spl20_32 ),
inference(avatar_split_clause,[],[f68,f235,f82]) ).
fof(f240,definition,
( spl20_33
<=> in(sK10,sK8) ),
introduced(definition,[new_symbols(definition,[spl20_33])],[avatar_definition]) ).
fof(f242,plain,
( in(sK10,sK8)
| ~ spl20_33 ),
inference(avatar_component_clause,[],[f240]) ).
fof(f243,plain,
( ~ spl20_2
| spl20_33 ),
inference(avatar_split_clause,[],[f13,f240,f86]) ).
fof(f245,definition,
( spl20_34
<=> sK7 = sK10 ),
introduced(definition,[new_symbols(definition,[spl20_34])],[avatar_definition]) ).
fof(f247,plain,
( sK7 = sK10
| ~ spl20_34 ),
inference(avatar_component_clause,[],[f245]) ).
fof(f248,plain,
( ~ spl20_2
| spl20_34 ),
inference(avatar_split_clause,[],[f14,f245,f86]) ).
fof(f250,definition,
( spl20_35
<=> in(sK9,sK8) ),
introduced(definition,[new_symbols(definition,[spl20_35])],[avatar_definition]) ).
fof(f252,plain,
( in(sK9,sK8)
| ~ spl20_35 ),
inference(avatar_component_clause,[],[f250]) ).
fof(f253,plain,
( ~ spl20_2
| spl20_35 ),
inference(avatar_split_clause,[],[f15,f250,f86]) ).
fof(f255,definition,
( spl20_36
<=> sK6 = sK9 ),
introduced(definition,[new_symbols(definition,[spl20_36])],[avatar_definition]) ).
fof(f257,plain,
( sK6 = sK9
| ~ spl20_36 ),
inference(avatar_component_clause,[],[f255]) ).
fof(f258,plain,
( ~ spl20_2
| spl20_36 ),
inference(avatar_split_clause,[],[f16,f255,f86]) ).
fof(f260,definition,
( spl20_37
<=> young(sK7) ),
introduced(definition,[new_symbols(definition,[spl20_37])],[avatar_definition]) ).
fof(f262,plain,
( young(sK7)
| ~ spl20_37 ),
inference(avatar_component_clause,[],[f260]) ).
fof(f263,plain,
( ~ spl20_2
| spl20_37 ),
inference(avatar_split_clause,[],[f17,f260,f86]) ).
fof(f265,definition,
( spl20_38
<=> man(sK7) ),
introduced(definition,[new_symbols(definition,[spl20_38])],[avatar_definition]) ).
fof(f267,plain,
( man(sK7)
| ~ spl20_38 ),
inference(avatar_component_clause,[],[f265]) ).
fof(f268,plain,
( ~ spl20_2
| spl20_38 ),
inference(avatar_split_clause,[],[f18,f265,f86]) ).
fof(f270,definition,
( spl20_39
<=> fellow(sK7) ),
introduced(definition,[new_symbols(definition,[spl20_39])],[avatar_definition]) ).
fof(f273,plain,
( ~ spl20_2
| spl20_39 ),
inference(avatar_split_clause,[],[f19,f270,f86]) ).
fof(f275,definition,
( spl20_40
<=> young(sK6) ),
introduced(definition,[new_symbols(definition,[spl20_40])],[avatar_definition]) ).
fof(f277,plain,
( young(sK6)
| ~ spl20_40 ),
inference(avatar_component_clause,[],[f275]) ).
fof(f278,plain,
( ~ spl20_2
| spl20_40 ),
inference(avatar_split_clause,[],[f20,f275,f86]) ).
fof(f280,definition,
( spl20_41
<=> man(sK6) ),
introduced(definition,[new_symbols(definition,[spl20_41])],[avatar_definition]) ).
fof(f282,plain,
( man(sK6)
| ~ spl20_41 ),
inference(avatar_component_clause,[],[f280]) ).
fof(f283,plain,
( ~ spl20_2
| spl20_41 ),
inference(avatar_split_clause,[],[f21,f280,f86]) ).
fof(f285,definition,
( spl20_42
<=> fellow(sK6) ),
introduced(definition,[new_symbols(definition,[spl20_42])],[avatar_definition]) ).
fof(f287,plain,
( fellow(sK6)
| ~ spl20_42 ),
inference(avatar_component_clause,[],[f285]) ).
fof(f288,plain,
( ~ spl20_2
| spl20_42 ),
inference(avatar_split_clause,[],[f22,f285,f86]) ).
fof(f290,definition,
( spl20_43
<=> sK6 = sK7 ),
introduced(definition,[new_symbols(definition,[spl20_43])],[avatar_definition]) ).
fof(f292,plain,
( sK6 != sK7
| spl20_43 ),
inference(avatar_component_clause,[],[f290]) ).
fof(f293,plain,
( ~ spl20_2
| ~ spl20_43 ),
inference(avatar_split_clause,[],[f23,f290,f86]) ).
fof(f295,definition,
( spl20_44
<=> front(sK8) ),
introduced(definition,[new_symbols(definition,[spl20_44])],[avatar_definition]) ).
fof(f297,plain,
( front(sK8)
| ~ spl20_44 ),
inference(avatar_component_clause,[],[f295]) ).
fof(f298,plain,
( ~ spl20_2
| spl20_44 ),
inference(avatar_split_clause,[],[f24,f295,f86]) ).
fof(f300,definition,
( spl20_45
<=> furniture(sK8) ),
introduced(definition,[new_symbols(definition,[spl20_45])],[avatar_definition]) ).
fof(f302,plain,
( furniture(sK8)
| ~ spl20_45 ),
inference(avatar_component_clause,[],[f300]) ).
fof(f303,plain,
( ~ spl20_2
| spl20_45 ),
inference(avatar_split_clause,[],[f25,f300,f86]) ).
fof(f305,definition,
( spl20_46
<=> seat(sK8) ),
introduced(definition,[new_symbols(definition,[spl20_46])],[avatar_definition]) ).
fof(f307,plain,
( seat(sK8)
| ~ spl20_46 ),
inference(avatar_component_clause,[],[f305]) ).
fof(f308,plain,
( ~ spl20_2
| spl20_46 ),
inference(avatar_split_clause,[],[f26,f305,f86]) ).
fof(f310,definition,
( spl20_47
<=> in(sK3,sK2) ),
introduced(definition,[new_symbols(definition,[spl20_47])],[avatar_definition]) ).
fof(f312,plain,
( in(sK3,sK2)
| ~ spl20_47 ),
inference(avatar_component_clause,[],[f310]) ).
fof(f313,plain,
( ~ spl20_2
| spl20_47 ),
inference(avatar_split_clause,[],[f27,f310,f86]) ).
fof(f315,definition,
( spl20_48
<=> down(sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl20_48])],[avatar_definition]) ).
fof(f317,plain,
( down(sK3,sK4)
| ~ spl20_48 ),
inference(avatar_component_clause,[],[f315]) ).
fof(f318,plain,
( ~ spl20_2
| spl20_48 ),
inference(avatar_split_clause,[],[f28,f315,f86]) ).
fof(f320,definition,
( spl20_49
<=> barrel(sK3,sK5) ),
introduced(definition,[new_symbols(definition,[spl20_49])],[avatar_definition]) ).
fof(f322,plain,
( barrel(sK3,sK5)
| ~ spl20_49 ),
inference(avatar_component_clause,[],[f320]) ).
fof(f323,plain,
( ~ spl20_2
| spl20_49 ),
inference(avatar_split_clause,[],[f29,f320,f86]) ).
fof(f325,definition,
( spl20_50
<=> old(sK5) ),
introduced(definition,[new_symbols(definition,[spl20_50])],[avatar_definition]) ).
fof(f327,plain,
( old(sK5)
| ~ spl20_50 ),
inference(avatar_component_clause,[],[f325]) ).
fof(f328,plain,
( ~ spl20_2
| spl20_50 ),
inference(avatar_split_clause,[],[f30,f325,f86]) ).
fof(f330,definition,
( spl20_51
<=> dirty(sK5) ),
introduced(definition,[new_symbols(definition,[spl20_51])],[avatar_definition]) ).
fof(f332,plain,
( dirty(sK5)
| ~ spl20_51 ),
inference(avatar_component_clause,[],[f330]) ).
fof(f333,plain,
( ~ spl20_2
| spl20_51 ),
inference(avatar_split_clause,[],[f31,f330,f86]) ).
fof(f335,definition,
( spl20_52
<=> white(sK5) ),
introduced(definition,[new_symbols(definition,[spl20_52])],[avatar_definition]) ).
fof(f337,plain,
( white(sK5)
| ~ spl20_52 ),
inference(avatar_component_clause,[],[f335]) ).
fof(f338,plain,
( ~ spl20_2
| spl20_52 ),
inference(avatar_split_clause,[],[f32,f335,f86]) ).
fof(f340,definition,
( spl20_53
<=> car(sK5) ),
introduced(definition,[new_symbols(definition,[spl20_53])],[avatar_definition]) ).
fof(f342,plain,
( car(sK5)
| ~ spl20_53 ),
inference(avatar_component_clause,[],[f340]) ).
fof(f343,plain,
( ~ spl20_2
| spl20_53 ),
inference(avatar_split_clause,[],[f33,f340,f86]) ).
fof(f345,definition,
( spl20_54
<=> chevy(sK5) ),
introduced(definition,[new_symbols(definition,[spl20_54])],[avatar_definition]) ).
fof(f347,plain,
( chevy(sK5)
| ~ spl20_54 ),
inference(avatar_component_clause,[],[f345]) ).
fof(f348,plain,
( ~ spl20_2
| spl20_54 ),
inference(avatar_split_clause,[],[f34,f345,f86]) ).
fof(f350,definition,
( spl20_55
<=> lonely(sK4) ),
introduced(definition,[new_symbols(definition,[spl20_55])],[avatar_definition]) ).
fof(f352,plain,
( lonely(sK4)
| ~ spl20_55 ),
inference(avatar_component_clause,[],[f350]) ).
fof(f353,plain,
( ~ spl20_2
| spl20_55 ),
inference(avatar_split_clause,[],[f35,f350,f86]) ).
fof(f355,definition,
( spl20_56
<=> way(sK4) ),
introduced(definition,[new_symbols(definition,[spl20_56])],[avatar_definition]) ).
fof(f357,plain,
( way(sK4)
| ~ spl20_56 ),
inference(avatar_component_clause,[],[f355]) ).
fof(f358,plain,
( ~ spl20_2
| spl20_56 ),
inference(avatar_split_clause,[],[f36,f355,f86]) ).
fof(f360,definition,
( spl20_57
<=> street(sK4) ),
introduced(definition,[new_symbols(definition,[spl20_57])],[avatar_definition]) ).
fof(f362,plain,
( street(sK4)
| ~ spl20_57 ),
inference(avatar_component_clause,[],[f360]) ).
fof(f363,plain,
( ~ spl20_2
| spl20_57 ),
inference(avatar_split_clause,[],[f37,f360,f86]) ).
fof(f365,definition,
( spl20_58
<=> event(sK3) ),
introduced(definition,[new_symbols(definition,[spl20_58])],[avatar_definition]) ).
fof(f368,plain,
( ~ spl20_2
| spl20_58 ),
inference(avatar_split_clause,[],[f38,f365,f86]) ).
fof(f370,definition,
( spl20_59
<=> city(sK2) ),
introduced(definition,[new_symbols(definition,[spl20_59])],[avatar_definition]) ).
fof(f372,plain,
( city(sK2)
| ~ spl20_59 ),
inference(avatar_component_clause,[],[f370]) ).
fof(f373,plain,
( ~ spl20_2
| spl20_59 ),
inference(avatar_split_clause,[],[f39,f370,f86]) ).
fof(f375,definition,
( spl20_60
<=> hollywood(sK2) ),
introduced(definition,[new_symbols(definition,[spl20_60])],[avatar_definition]) ).
fof(f377,plain,
( hollywood(sK2)
| ~ spl20_60 ),
inference(avatar_component_clause,[],[f375]) ).
fof(f378,plain,
( ~ spl20_2
| spl20_60 ),
inference(avatar_split_clause,[],[f40,f375,f86]) ).
fof(f381,plain,
( ! [X0,X1] :
( ~ in(sK7,X0)
| sK7 = X1
| ~ in(X1,X0)
| ~ young(sK7)
| ~ seat(X0)
| ~ fellow(sK7)
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ front(X0)
| ~ furniture(X0) )
| ~ spl20_3
| ~ spl20_38 ),
inference(resolution,[],[f267,f92]) ).
fof(f382,plain,
( ! [X0,X1] :
( ~ in(sK7,X0)
| sK7 = X1
| ~ in(X1,X0)
| ~ seat(X0)
| ~ fellow(sK7)
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ front(X0)
| ~ furniture(X0) )
| ~ spl20_3
| ~ spl20_37
| ~ spl20_38 ),
inference(forward_subsumption_resolution,[],[f381,f262]) ).
fof(f384,definition,
( spl20_61
<=> ! [X0,X1] :
( ~ in(sK7,X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ seat(X0)
| sK7 = X1
| ~ in(X1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl20_61])],[avatar_definition]) ).
fof(f385,plain,
( ! [X0,X1] :
( ~ in(sK7,X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ seat(X0)
| sK7 = X1
| ~ in(X1,X0) )
| ~ spl20_61 ),
inference(avatar_component_clause,[],[f384]) ).
fof(f386,plain,
( ~ spl20_39
| spl20_61
| ~ spl20_3
| ~ spl20_37
| ~ spl20_38 ),
inference(avatar_split_clause,[],[f382,f265,f260,f91,f384,f270]) ).
fof(f393,plain,
( ! [X0,X1] :
( ~ in(sK15,X0)
| sK15 = X1
| ~ in(X1,X0)
| ~ young(sK15)
| ~ seat(X0)
| ~ fellow(sK15)
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ front(X0)
| ~ furniture(X0) )
| ~ spl20_3
| ~ spl20_13 ),
inference(resolution,[],[f142,f92]) ).
fof(f394,plain,
( ! [X0,X1] :
( ~ in(sK15,X0)
| sK15 = X1
| ~ in(X1,X0)
| ~ seat(X0)
| ~ fellow(sK15)
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ front(X0)
| ~ furniture(X0) )
| ~ spl20_3
| ~ spl20_12
| ~ spl20_13 ),
inference(forward_subsumption_resolution,[],[f393,f137]) ).
fof(f396,definition,
( spl20_63
<=> ! [X0,X1] :
( ~ in(sK15,X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ seat(X0)
| sK15 = X1
| ~ in(X1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl20_63])],[avatar_definition]) ).
fof(f397,plain,
( ! [X0,X1] :
( ~ in(sK15,X0)
| ~ furniture(X0)
| ~ front(X0)
| ~ fellow(X1)
| ~ man(X1)
| ~ young(X1)
| ~ seat(X0)
| sK15 = X1
| ~ in(X1,X0) )
| ~ spl20_63 ),
inference(avatar_component_clause,[],[f396]) ).
fof(f398,plain,
( ~ spl20_14
| spl20_63
| ~ spl20_3
| ~ spl20_12
| ~ spl20_13 ),
inference(avatar_split_clause,[],[f394,f140,f135,f91,f396,f145]) ).
fof(f407,plain,
( in(sK16,sK17)
| ~ spl20_5
| ~ spl20_6 ),
inference(superposition,[],[f102,f107]) ).
fof(f408,plain,
( in(sK15,sK17)
| ~ spl20_7
| ~ spl20_8 ),
inference(superposition,[],[f112,f117]) ).
fof(f409,plain,
( in(sK7,sK8)
| ~ spl20_33
| ~ spl20_34 ),
inference(superposition,[],[f242,f247]) ).
fof(f410,plain,
( in(sK6,sK8)
| ~ spl20_35
| ~ spl20_36 ),
inference(superposition,[],[f252,f257]) ).
fof(f415,plain,
( ! [X0] :
( ~ furniture(sK17)
| ~ front(sK17)
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(sK17)
| sK15 = X0
| ~ in(X0,sK17) )
| ~ spl20_7
| ~ spl20_8
| ~ spl20_63 ),
inference(resolution,[],[f408,f397]) ).
fof(f416,plain,
( ! [X0] :
( ~ front(sK17)
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(sK17)
| sK15 = X0
| ~ in(X0,sK17) )
| ~ spl20_7
| ~ spl20_8
| ~ spl20_17
| ~ spl20_63 ),
inference(forward_subsumption_resolution,[],[f415,f162]) ).
fof(f417,plain,
( ! [X0] :
( ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(sK17)
| sK15 = X0
| ~ in(X0,sK17) )
| ~ spl20_7
| ~ spl20_8
| ~ spl20_16
| ~ spl20_17
| ~ spl20_63 ),
inference(forward_subsumption_resolution,[],[f416,f157]) ).
fof(f418,plain,
( ! [X0] :
( ~ young(X0)
| ~ man(X0)
| ~ fellow(X0)
| sK15 = X0
| ~ in(X0,sK17) )
| ~ spl20_7
| ~ spl20_8
| ~ spl20_16
| ~ spl20_17
| ~ spl20_18
| ~ spl20_63 ),
inference(forward_subsumption_resolution,[],[f417,f167]) ).
fof(f461,plain,
( ! [X0] :
( ~ furniture(sK8)
| ~ front(sK8)
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(sK8)
| sK7 = X0
| ~ in(X0,sK8) )
| ~ spl20_33
| ~ spl20_34
| ~ spl20_61 ),
inference(resolution,[],[f409,f385]) ).
fof(f462,plain,
( ! [X0] :
( ~ front(sK8)
| ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(sK8)
| sK7 = X0
| ~ in(X0,sK8) )
| ~ spl20_33
| ~ spl20_34
| ~ spl20_45
| ~ spl20_61 ),
inference(forward_subsumption_resolution,[],[f461,f302]) ).
fof(f463,plain,
( ! [X0] :
( ~ fellow(X0)
| ~ man(X0)
| ~ young(X0)
| ~ seat(sK8)
| sK7 = X0
| ~ in(X0,sK8) )
| ~ spl20_33
| ~ spl20_34
| ~ spl20_44
| ~ spl20_45
| ~ spl20_61 ),
inference(forward_subsumption_resolution,[],[f462,f297]) ).
fof(f464,plain,
( ! [X0] :
( ~ young(X0)
| ~ man(X0)
| ~ fellow(X0)
| sK7 = X0
| ~ in(X0,sK8) )
| ~ spl20_33
| ~ spl20_34
| ~ spl20_44
| ~ spl20_45
| ~ spl20_46
| ~ spl20_61 ),
inference(forward_subsumption_resolution,[],[f463,f307]) ).
fof(f465,plain,
( ~ man(sK6)
| ~ fellow(sK6)
| sK6 = sK7
| ~ in(sK6,sK8)
| ~ spl20_33
| ~ spl20_34
| ~ spl20_40
| ~ spl20_44
| ~ spl20_45
| ~ spl20_46
| ~ spl20_61 ),
inference(resolution,[],[f464,f277]) ).
fof(f469,plain,
( ~ fellow(sK6)
| sK6 = sK7
| ~ in(sK6,sK8)
| ~ spl20_33
| ~ spl20_34
| ~ spl20_40
| ~ spl20_41
| ~ spl20_44
| ~ spl20_45
| ~ spl20_46
| ~ spl20_61 ),
inference(forward_subsumption_resolution,[],[f465,f282]) ).
fof(f471,plain,
( sK6 = sK7
| ~ in(sK6,sK8)
| ~ spl20_33
| ~ spl20_34
| ~ spl20_40
| ~ spl20_41
| ~ spl20_42
| ~ spl20_44
| ~ spl20_45
| ~ spl20_46
| ~ spl20_61 ),
inference(forward_subsumption_resolution,[],[f469,f287]) ).
fof(f477,plain,
( ~ in(sK6,sK8)
| ~ spl20_33
| ~ spl20_34
| ~ spl20_40
| ~ spl20_41
| ~ spl20_42
| spl20_43
| ~ spl20_44
| ~ spl20_45
| ~ spl20_46
| ~ spl20_61 ),
inference(forward_subsumption_resolution,[],[f471,f292]) ).
fof(f490,plain,
( $false
| ~ spl20_33
| ~ spl20_34
| ~ spl20_35
| ~ spl20_36
| ~ spl20_40
| ~ spl20_41
| ~ spl20_42
| spl20_43
| ~ spl20_44
| ~ spl20_45
| ~ spl20_46
| ~ spl20_61 ),
inference(forward_subsumption_resolution,[],[f477,f410]) ).
fof(f491,plain,
( ~ spl20_33
| ~ spl20_34
| ~ spl20_35
| ~ spl20_36
| ~ spl20_40
| ~ spl20_41
| ~ spl20_42
| spl20_43
| ~ spl20_44
| ~ spl20_45
| ~ spl20_46
| ~ spl20_61 ),
inference(avatar_contradiction_clause,[],[f490]) ).
fof(f492,plain,
( ! [X2,X0,X1] :
( ~ event(X0)
| ~ in(X0,X1)
| ~ down(X0,X2)
| ~ barrel(X0,sK13)
| ~ chevy(sK13)
| ~ hollywood(X1)
| ~ dirty(sK13)
| ~ white(sK13)
| ~ car(sK13)
| ~ street(X2)
| ~ lonely(X2)
| ~ way(X2)
| ~ city(X1) )
| ~ spl20_4
| ~ spl20_25 ),
inference(resolution,[],[f95,f202]) ).
fof(f493,plain,
( ! [X2,X0,X1] :
( ~ event(X0)
| ~ in(X0,X1)
| ~ down(X0,X2)
| ~ barrel(X0,sK5)
| ~ chevy(sK5)
| ~ hollywood(X1)
| ~ dirty(sK5)
| ~ white(sK5)
| ~ car(sK5)
| ~ street(X2)
| ~ lonely(X2)
| ~ way(X2)
| ~ city(X1) )
| ~ spl20_4
| ~ spl20_50 ),
inference(resolution,[],[f95,f327]) ).
fof(f494,plain,
( ! [X2,X0,X1] :
( ~ event(X0)
| ~ in(X0,X1)
| ~ down(X0,X2)
| ~ barrel(X0,sK5)
| ~ hollywood(X1)
| ~ dirty(sK5)
| ~ white(sK5)
| ~ car(sK5)
| ~ street(X2)
| ~ lonely(X2)
| ~ way(X2)
| ~ city(X1) )
| ~ spl20_4
| ~ spl20_50
| ~ spl20_54 ),
inference(forward_subsumption_resolution,[],[f493,f347]) ).
fof(f495,plain,
( ! [X2,X0,X1] :
( ~ event(X0)
| ~ in(X0,X1)
| ~ down(X0,X2)
| ~ barrel(X0,sK13)
| ~ hollywood(X1)
| ~ dirty(sK13)
| ~ white(sK13)
| ~ car(sK13)
| ~ street(X2)
| ~ lonely(X2)
| ~ way(X2)
| ~ city(X1) )
| ~ spl20_4
| ~ spl20_25
| ~ spl20_29 ),
inference(forward_subsumption_resolution,[],[f492,f222]) ).
fof(f496,plain,
( ! [X2,X0,X1] :
( ~ event(X0)
| ~ in(X0,X1)
| ~ down(X0,X2)
| ~ barrel(X0,sK5)
| ~ hollywood(X1)
| ~ white(sK5)
| ~ car(sK5)
| ~ street(X2)
| ~ lonely(X2)
| ~ way(X2)
| ~ city(X1) )
| ~ spl20_4
| ~ spl20_50
| ~ spl20_51
| ~ spl20_54 ),
inference(forward_subsumption_resolution,[],[f494,f332]) ).
fof(f497,plain,
( ! [X2,X0,X1] :
( ~ event(X0)
| ~ in(X0,X1)
| ~ down(X0,X2)
| ~ barrel(X0,sK13)
| ~ hollywood(X1)
| ~ white(sK13)
| ~ car(sK13)
| ~ street(X2)
| ~ lonely(X2)
| ~ way(X2)
| ~ city(X1) )
| ~ spl20_4
| ~ spl20_25
| ~ spl20_26
| ~ spl20_29 ),
inference(forward_subsumption_resolution,[],[f495,f207]) ).
fof(f498,plain,
( ! [X2,X0,X1] :
( ~ event(X0)
| ~ in(X0,X1)
| ~ down(X0,X2)
| ~ barrel(X0,sK5)
| ~ hollywood(X1)
| ~ car(sK5)
| ~ street(X2)
| ~ lonely(X2)
| ~ way(X2)
| ~ city(X1) )
| ~ spl20_4
| ~ spl20_50
| ~ spl20_51
| ~ spl20_52
| ~ spl20_54 ),
inference(forward_subsumption_resolution,[],[f496,f337]) ).
fof(f499,plain,
( ! [X2,X0,X1] :
( ~ event(X0)
| ~ in(X0,X1)
| ~ down(X0,X2)
| ~ barrel(X0,sK13)
| ~ hollywood(X1)
| ~ car(sK13)
| ~ street(X2)
| ~ lonely(X2)
| ~ way(X2)
| ~ city(X1) )
| ~ spl20_4
| ~ spl20_25
| ~ spl20_26
| ~ spl20_27
| ~ spl20_29 ),
inference(forward_subsumption_resolution,[],[f497,f212]) ).
fof(f500,plain,
( ! [X2,X0,X1] :
( ~ barrel(X0,sK5)
| ~ in(X0,X1)
| ~ down(X0,X2)
| ~ event(X0)
| ~ hollywood(X1)
| ~ street(X2)
| ~ lonely(X2)
| ~ way(X2)
| ~ city(X1) )
| ~ spl20_4
| ~ spl20_50
| ~ spl20_51
| ~ spl20_52
| ~ spl20_53
| ~ spl20_54 ),
inference(forward_subsumption_resolution,[],[f498,f342]) ).
fof(f501,plain,
( ! [X2,X0,X1] :
( ~ barrel(X0,sK13)
| ~ in(X0,X1)
| ~ down(X0,X2)
| ~ event(X0)
| ~ hollywood(X1)
| ~ street(X2)
| ~ lonely(X2)
| ~ way(X2)
| ~ city(X1) )
| ~ spl20_4
| ~ spl20_25
| ~ spl20_26
| ~ spl20_27
| ~ spl20_28
| ~ spl20_29 ),
inference(forward_subsumption_resolution,[],[f499,f217]) ).
fof(f502,plain,
( ! [X0,X1] :
( ~ in(sK3,X0)
| ~ down(sK3,X1)
| ~ event(sK3)
| ~ hollywood(X0)
| ~ street(X1)
| ~ lonely(X1)
| ~ way(X1)
| ~ city(X0) )
| ~ spl20_4
| ~ spl20_49
| ~ spl20_50
| ~ spl20_51
| ~ spl20_52
| ~ spl20_53
| ~ spl20_54 ),
inference(resolution,[],[f500,f322]) ).
fof(f505,definition,
( spl20_70
<=> ! [X1] :
( ~ down(sK3,X1)
| ~ way(X1)
| ~ lonely(X1)
| ~ street(X1) ) ),
introduced(definition,[new_symbols(definition,[spl20_70])],[avatar_definition]) ).
fof(f506,plain,
( ! [X1] :
( ~ down(sK3,X1)
| ~ way(X1)
| ~ lonely(X1)
| ~ street(X1) )
| ~ spl20_70 ),
inference(avatar_component_clause,[],[f505]) ).
fof(f508,definition,
( spl20_71
<=> ! [X0] :
( ~ in(sK3,X0)
| ~ city(X0)
| ~ hollywood(X0) ) ),
introduced(definition,[new_symbols(definition,[spl20_71])],[avatar_definition]) ).
fof(f509,plain,
( ! [X0] :
( ~ in(sK3,X0)
| ~ city(X0)
| ~ hollywood(X0) )
| ~ spl20_71 ),
inference(avatar_component_clause,[],[f508]) ).
fof(f511,plain,
( ! [X0,X1] :
( ~ in(sK12,X0)
| ~ down(sK12,X1)
| ~ event(sK12)
| ~ hollywood(X0)
| ~ street(X1)
| ~ lonely(X1)
| ~ way(X1)
| ~ city(X0) )
| ~ spl20_4
| ~ spl20_21
| ~ spl20_25
| ~ spl20_26
| ~ spl20_27
| ~ spl20_28
| ~ spl20_29 ),
inference(resolution,[],[f501,f182]) ).
fof(f514,definition,
( spl20_72
<=> ! [X1] :
( ~ down(sK12,X1)
| ~ way(X1)
| ~ lonely(X1)
| ~ street(X1) ) ),
introduced(definition,[new_symbols(definition,[spl20_72])],[avatar_definition]) ).
fof(f515,plain,
( ! [X1] :
( ~ down(sK12,X1)
| ~ way(X1)
| ~ lonely(X1)
| ~ street(X1) )
| ~ spl20_72 ),
inference(avatar_component_clause,[],[f514]) ).
fof(f517,definition,
( spl20_73
<=> ! [X0] :
( ~ in(sK12,X0)
| ~ city(X0)
| ~ hollywood(X0) ) ),
introduced(definition,[new_symbols(definition,[spl20_73])],[avatar_definition]) ).
fof(f518,plain,
( ! [X0] :
( ~ in(sK12,X0)
| ~ city(X0)
| ~ hollywood(X0) )
| ~ spl20_73 ),
inference(avatar_component_clause,[],[f517]) ).
fof(f524,plain,
( ~ way(sK4)
| ~ lonely(sK4)
| ~ street(sK4)
| ~ spl20_48
| ~ spl20_70 ),
inference(resolution,[],[f506,f317]) ).
fof(f525,plain,
( ~ lonely(sK4)
| ~ street(sK4)
| ~ spl20_48
| ~ spl20_56
| ~ spl20_70 ),
inference(forward_subsumption_resolution,[],[f524,f357]) ).
fof(f526,plain,
( ~ street(sK4)
| ~ spl20_48
| ~ spl20_55
| ~ spl20_56
| ~ spl20_70 ),
inference(forward_subsumption_resolution,[],[f525,f352]) ).
fof(f527,plain,
( $false
| ~ spl20_48
| ~ spl20_55
| ~ spl20_56
| ~ spl20_57
| ~ spl20_70 ),
inference(forward_subsumption_resolution,[],[f526,f362]) ).
fof(f528,plain,
( ~ spl20_48
| ~ spl20_55
| ~ spl20_56
| ~ spl20_57
| ~ spl20_70 ),
inference(avatar_contradiction_clause,[],[f527]) ).
fof(f529,plain,
( ~ city(sK2)
| ~ hollywood(sK2)
| ~ spl20_47
| ~ spl20_71 ),
inference(resolution,[],[f509,f312]) ).
fof(f530,plain,
( ~ hollywood(sK2)
| ~ spl20_47
| ~ spl20_59
| ~ spl20_71 ),
inference(forward_subsumption_resolution,[],[f529,f372]) ).
fof(f531,plain,
( $false
| ~ spl20_47
| ~ spl20_59
| ~ spl20_60
| ~ spl20_71 ),
inference(forward_subsumption_resolution,[],[f530,f377]) ).
fof(f532,plain,
( ~ spl20_47
| ~ spl20_59
| ~ spl20_60
| ~ spl20_71 ),
inference(avatar_contradiction_clause,[],[f531]) ).
fof(f534,plain,
( ! [X0,X1] :
( ~ in(sK12,X0)
| ~ down(sK12,X1)
| ~ hollywood(X0)
| ~ street(X1)
| ~ lonely(X1)
| ~ way(X1)
| ~ city(X0) )
| ~ spl20_4
| ~ spl20_21
| ~ spl20_25
| ~ spl20_26
| ~ spl20_27
| ~ spl20_28
| ~ spl20_29
| ~ spl20_30 ),
inference(forward_subsumption_resolution,[],[f511,f227]) ).
fof(f536,plain,
( ~ spl20_58
| spl20_70
| spl20_71
| ~ spl20_4
| ~ spl20_49
| ~ spl20_50
| ~ spl20_51
| ~ spl20_52
| ~ spl20_53
| ~ spl20_54 ),
inference(avatar_split_clause,[],[f502,f345,f340,f335,f330,f325,f320,f94,f508,f505,f365]) ).
fof(f537,plain,
( spl20_72
| spl20_73
| ~ spl20_4
| ~ spl20_21
| ~ spl20_25
| ~ spl20_26
| ~ spl20_27
| ~ spl20_28
| ~ spl20_29
| ~ spl20_30 ),
inference(avatar_split_clause,[],[f534,f225,f220,f215,f210,f205,f200,f180,f94,f517,f514]) ).
fof(f538,plain,
( ~ man(sK16)
| ~ fellow(sK16)
| sK15 = sK16
| ~ in(sK16,sK17)
| ~ spl20_7
| ~ spl20_8
| ~ spl20_9
| ~ spl20_16
| ~ spl20_17
| ~ spl20_18
| ~ spl20_63 ),
inference(resolution,[],[f122,f418]) ).
fof(f539,plain,
( ~ fellow(sK16)
| sK15 = sK16
| ~ in(sK16,sK17)
| ~ spl20_7
| ~ spl20_8
| ~ spl20_9
| ~ spl20_10
| ~ spl20_16
| ~ spl20_17
| ~ spl20_18
| ~ spl20_63 ),
inference(forward_subsumption_resolution,[],[f538,f127]) ).
fof(f540,plain,
( sK15 = sK16
| ~ in(sK16,sK17)
| ~ spl20_7
| ~ spl20_8
| ~ spl20_9
| ~ spl20_10
| ~ spl20_11
| ~ spl20_16
| ~ spl20_17
| ~ spl20_18
| ~ spl20_63 ),
inference(forward_subsumption_resolution,[],[f539,f132]) ).
fof(f541,plain,
( ~ in(sK16,sK17)
| ~ spl20_7
| ~ spl20_8
| ~ spl20_9
| ~ spl20_10
| ~ spl20_11
| spl20_15
| ~ spl20_16
| ~ spl20_17
| ~ spl20_18
| ~ spl20_63 ),
inference(forward_subsumption_resolution,[],[f540,f152]) ).
fof(f542,plain,
( $false
| ~ spl20_5
| ~ spl20_6
| ~ spl20_7
| ~ spl20_8
| ~ spl20_9
| ~ spl20_10
| ~ spl20_11
| spl20_15
| ~ spl20_16
| ~ spl20_17
| ~ spl20_18
| ~ spl20_63 ),
inference(forward_subsumption_resolution,[],[f541,f407]) ).
fof(f543,plain,
( ~ spl20_5
| ~ spl20_6
| ~ spl20_7
| ~ spl20_8
| ~ spl20_9
| ~ spl20_10
| ~ spl20_11
| spl20_15
| ~ spl20_16
| ~ spl20_17
| ~ spl20_18
| ~ spl20_63 ),
inference(avatar_contradiction_clause,[],[f542]) ).
fof(f544,plain,
( ~ city(sK11)
| ~ hollywood(sK11)
| ~ spl20_19
| ~ spl20_73 ),
inference(resolution,[],[f518,f172]) ).
fof(f545,plain,
( ~ hollywood(sK11)
| ~ spl20_19
| ~ spl20_31
| ~ spl20_73 ),
inference(forward_subsumption_resolution,[],[f544,f232]) ).
fof(f546,plain,
( $false
| ~ spl20_19
| ~ spl20_31
| ~ spl20_32
| ~ spl20_73 ),
inference(forward_subsumption_resolution,[],[f545,f237]) ).
fof(f547,plain,
( ~ spl20_19
| ~ spl20_31
| ~ spl20_32
| ~ spl20_73 ),
inference(avatar_contradiction_clause,[],[f546]) ).
fof(f548,plain,
( ~ way(sK14)
| ~ lonely(sK14)
| ~ street(sK14)
| ~ spl20_20
| ~ spl20_72 ),
inference(resolution,[],[f515,f177]) ).
fof(f549,plain,
( ~ lonely(sK14)
| ~ street(sK14)
| ~ spl20_20
| ~ spl20_23
| ~ spl20_72 ),
inference(forward_subsumption_resolution,[],[f548,f192]) ).
fof(f550,plain,
( ~ street(sK14)
| ~ spl20_20
| ~ spl20_22
| ~ spl20_23
| ~ spl20_72 ),
inference(forward_subsumption_resolution,[],[f549,f187]) ).
fof(f551,plain,
( $false
| ~ spl20_20
| ~ spl20_22
| ~ spl20_23
| ~ spl20_24
| ~ spl20_72 ),
inference(forward_subsumption_resolution,[],[f550,f197]) ).
fof(f552,plain,
( ~ spl20_20
| ~ spl20_22
| ~ spl20_23
| ~ spl20_24
| ~ spl20_72 ),
inference(avatar_contradiction_clause,[],[f551]) ).
cnf(s1,plain,
( spl20_1
| spl20_2 ),
inference(sat_conversion,[],[f89]) ).
cnf(s4,plain,
( spl20_3
| spl20_4
| spl20_3
| spl20_4 ),
inference(sat_conversion,[],[f98]) ).
cnf(s5,plain,
( spl20_3
| spl20_4 ),
inference(rat,[],[s4]) ).
cnf(s6,plain,
( ~ spl20_1
| spl20_5 ),
inference(sat_conversion,[],[f103]) ).
cnf(s7,plain,
( ~ spl20_1
| spl20_6 ),
inference(sat_conversion,[],[f108]) ).
cnf(s8,plain,
( ~ spl20_1
| spl20_7 ),
inference(sat_conversion,[],[f113]) ).
cnf(s9,plain,
( ~ spl20_1
| spl20_8 ),
inference(sat_conversion,[],[f118]) ).
cnf(s10,plain,
( ~ spl20_1
| spl20_9 ),
inference(sat_conversion,[],[f123]) ).
cnf(s11,plain,
( ~ spl20_1
| spl20_10 ),
inference(sat_conversion,[],[f128]) ).
cnf(s12,plain,
( ~ spl20_1
| spl20_11 ),
inference(sat_conversion,[],[f133]) ).
cnf(s13,plain,
( ~ spl20_1
| spl20_12 ),
inference(sat_conversion,[],[f138]) ).
cnf(s14,plain,
( ~ spl20_1
| spl20_13 ),
inference(sat_conversion,[],[f143]) ).
cnf(s15,plain,
( ~ spl20_1
| spl20_14 ),
inference(sat_conversion,[],[f148]) ).
cnf(s16,plain,
( ~ spl20_1
| ~ spl20_15 ),
inference(sat_conversion,[],[f153]) ).
cnf(s17,plain,
( ~ spl20_1
| spl20_16 ),
inference(sat_conversion,[],[f158]) ).
cnf(s18,plain,
( ~ spl20_1
| spl20_17 ),
inference(sat_conversion,[],[f163]) ).
cnf(s19,plain,
( ~ spl20_1
| spl20_18 ),
inference(sat_conversion,[],[f168]) ).
cnf(s20,plain,
( ~ spl20_1
| spl20_19 ),
inference(sat_conversion,[],[f173]) ).
cnf(s21,plain,
( ~ spl20_1
| spl20_20 ),
inference(sat_conversion,[],[f178]) ).
cnf(s22,plain,
( ~ spl20_1
| spl20_21 ),
inference(sat_conversion,[],[f183]) ).
cnf(s23,plain,
( ~ spl20_1
| spl20_22 ),
inference(sat_conversion,[],[f188]) ).
cnf(s24,plain,
( ~ spl20_1
| spl20_23 ),
inference(sat_conversion,[],[f193]) ).
cnf(s25,plain,
( ~ spl20_1
| spl20_24 ),
inference(sat_conversion,[],[f198]) ).
cnf(s26,plain,
( ~ spl20_1
| spl20_25 ),
inference(sat_conversion,[],[f203]) ).
cnf(s27,plain,
( ~ spl20_1
| spl20_26 ),
inference(sat_conversion,[],[f208]) ).
cnf(s28,plain,
( ~ spl20_1
| spl20_27 ),
inference(sat_conversion,[],[f213]) ).
cnf(s29,plain,
( ~ spl20_1
| spl20_28 ),
inference(sat_conversion,[],[f218]) ).
cnf(s30,plain,
( ~ spl20_1
| spl20_29 ),
inference(sat_conversion,[],[f223]) ).
cnf(s31,plain,
( ~ spl20_1
| spl20_30 ),
inference(sat_conversion,[],[f228]) ).
cnf(s32,plain,
( ~ spl20_1
| spl20_31 ),
inference(sat_conversion,[],[f233]) ).
cnf(s33,plain,
( ~ spl20_1
| spl20_32 ),
inference(sat_conversion,[],[f238]) ).
cnf(s34,plain,
( ~ spl20_2
| spl20_33 ),
inference(sat_conversion,[],[f243]) ).
cnf(s35,plain,
( ~ spl20_2
| spl20_34 ),
inference(sat_conversion,[],[f248]) ).
cnf(s36,plain,
( ~ spl20_2
| spl20_35 ),
inference(sat_conversion,[],[f253]) ).
cnf(s37,plain,
( ~ spl20_2
| spl20_36 ),
inference(sat_conversion,[],[f258]) ).
cnf(s38,plain,
( ~ spl20_2
| spl20_37 ),
inference(sat_conversion,[],[f263]) ).
cnf(s39,plain,
( ~ spl20_2
| spl20_38 ),
inference(sat_conversion,[],[f268]) ).
cnf(s40,plain,
( ~ spl20_2
| spl20_39 ),
inference(sat_conversion,[],[f273]) ).
cnf(s41,plain,
( ~ spl20_2
| spl20_40 ),
inference(sat_conversion,[],[f278]) ).
cnf(s42,plain,
( ~ spl20_2
| spl20_41 ),
inference(sat_conversion,[],[f283]) ).
cnf(s43,plain,
( ~ spl20_2
| spl20_42 ),
inference(sat_conversion,[],[f288]) ).
cnf(s44,plain,
( ~ spl20_2
| ~ spl20_43 ),
inference(sat_conversion,[],[f293]) ).
cnf(s45,plain,
( ~ spl20_2
| spl20_44 ),
inference(sat_conversion,[],[f298]) ).
cnf(s46,plain,
( ~ spl20_2
| spl20_45 ),
inference(sat_conversion,[],[f303]) ).
cnf(s47,plain,
( ~ spl20_2
| spl20_46 ),
inference(sat_conversion,[],[f308]) ).
cnf(s48,plain,
( ~ spl20_2
| spl20_47 ),
inference(sat_conversion,[],[f313]) ).
cnf(s49,plain,
( ~ spl20_2
| spl20_48 ),
inference(sat_conversion,[],[f318]) ).
cnf(s50,plain,
( ~ spl20_2
| spl20_49 ),
inference(sat_conversion,[],[f323]) ).
cnf(s51,plain,
( ~ spl20_2
| spl20_50 ),
inference(sat_conversion,[],[f328]) ).
cnf(s52,plain,
( ~ spl20_2
| spl20_51 ),
inference(sat_conversion,[],[f333]) ).
cnf(s53,plain,
( ~ spl20_2
| spl20_52 ),
inference(sat_conversion,[],[f338]) ).
cnf(s54,plain,
( ~ spl20_2
| spl20_53 ),
inference(sat_conversion,[],[f343]) ).
cnf(s55,plain,
( ~ spl20_2
| spl20_54 ),
inference(sat_conversion,[],[f348]) ).
cnf(s56,plain,
( ~ spl20_2
| spl20_55 ),
inference(sat_conversion,[],[f353]) ).
cnf(s57,plain,
( ~ spl20_2
| spl20_56 ),
inference(sat_conversion,[],[f358]) ).
cnf(s58,plain,
( ~ spl20_2
| spl20_57 ),
inference(sat_conversion,[],[f363]) ).
cnf(s59,plain,
( ~ spl20_2
| spl20_58 ),
inference(sat_conversion,[],[f368]) ).
cnf(s60,plain,
( ~ spl20_2
| spl20_59 ),
inference(sat_conversion,[],[f373]) ).
cnf(s61,plain,
( ~ spl20_2
| spl20_60 ),
inference(sat_conversion,[],[f378]) ).
cnf(s62,plain,
( ~ spl20_3
| ~ spl20_37
| ~ spl20_38
| ~ spl20_39
| spl20_61 ),
inference(sat_conversion,[],[f386]) ).
cnf(s64,plain,
( ~ spl20_3
| ~ spl20_12
| ~ spl20_13
| ~ spl20_14
| spl20_63 ),
inference(sat_conversion,[],[f398]) ).
cnf(s75,plain,
( ~ spl20_33
| ~ spl20_34
| ~ spl20_35
| ~ spl20_36
| ~ spl20_40
| ~ spl20_41
| ~ spl20_42
| spl20_43
| ~ spl20_44
| ~ spl20_45
| ~ spl20_46
| ~ spl20_61 ),
inference(sat_conversion,[],[f491]) ).
cnf(s79,plain,
( ~ spl20_48
| ~ spl20_55
| ~ spl20_56
| ~ spl20_57
| ~ spl20_70 ),
inference(sat_conversion,[],[f528]) ).
cnf(s80,plain,
( ~ spl20_47
| ~ spl20_59
| ~ spl20_60
| ~ spl20_71 ),
inference(sat_conversion,[],[f532]) ).
cnf(s83,plain,
( ~ spl20_4
| ~ spl20_49
| ~ spl20_50
| ~ spl20_51
| ~ spl20_52
| ~ spl20_53
| ~ spl20_54
| ~ spl20_58
| spl20_70
| spl20_71 ),
inference(sat_conversion,[],[f536]) ).
cnf(s84,plain,
( ~ spl20_4
| ~ spl20_21
| ~ spl20_25
| ~ spl20_26
| ~ spl20_27
| ~ spl20_28
| ~ spl20_29
| ~ spl20_30
| spl20_72
| spl20_73 ),
inference(sat_conversion,[],[f537]) ).
cnf(s85,plain,
( ~ spl20_5
| ~ spl20_6
| ~ spl20_7
| ~ spl20_8
| ~ spl20_9
| ~ spl20_10
| ~ spl20_11
| spl20_15
| ~ spl20_16
| ~ spl20_17
| ~ spl20_18
| ~ spl20_63 ),
inference(sat_conversion,[],[f543]) ).
cnf(s86,plain,
( ~ spl20_19
| ~ spl20_31
| ~ spl20_32
| ~ spl20_73 ),
inference(sat_conversion,[],[f547]) ).
cnf(s87,plain,
( ~ spl20_20
| ~ spl20_22
| ~ spl20_23
| ~ spl20_24
| ~ spl20_72 ),
inference(sat_conversion,[],[f552]) ).
cnf(s88,plain,
~ spl20_2,
inference(rat,[],[s5,s62,s83,s75,s80,s79,s34,s35,s36,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]) ).
cnf(s89,plain,
spl20_1,
inference(rat,[],[s1,s88]) ).
cnf(s90,plain,
spl20_32,
inference(rat,[],[s33,s89]) ).
cnf(s91,plain,
spl20_31,
inference(rat,[],[s32,s89]) ).
cnf(s92,plain,
spl20_30,
inference(rat,[],[s31,s89]) ).
cnf(s93,plain,
spl20_29,
inference(rat,[],[s30,s89]) ).
cnf(s94,plain,
spl20_28,
inference(rat,[],[s29,s89]) ).
cnf(s95,plain,
spl20_27,
inference(rat,[],[s28,s89]) ).
cnf(s96,plain,
spl20_26,
inference(rat,[],[s27,s89]) ).
cnf(s97,plain,
spl20_25,
inference(rat,[],[s26,s89]) ).
cnf(s98,plain,
spl20_24,
inference(rat,[],[s25,s89]) ).
cnf(s99,plain,
spl20_23,
inference(rat,[],[s24,s89]) ).
cnf(s100,plain,
spl20_22,
inference(rat,[],[s23,s89]) ).
cnf(s101,plain,
spl20_21,
inference(rat,[],[s22,s89]) ).
cnf(s102,plain,
spl20_20,
inference(rat,[],[s21,s89]) ).
cnf(s103,plain,
spl20_19,
inference(rat,[],[s20,s89]) ).
cnf(s104,plain,
spl20_18,
inference(rat,[],[s19,s89]) ).
cnf(s105,plain,
spl20_17,
inference(rat,[],[s18,s89]) ).
cnf(s106,plain,
spl20_16,
inference(rat,[],[s17,s89]) ).
cnf(s107,plain,
~ spl20_15,
inference(rat,[],[s16,s89]) ).
cnf(s108,plain,
spl20_14,
inference(rat,[],[s15,s89]) ).
cnf(s109,plain,
spl20_13,
inference(rat,[],[s14,s89]) ).
cnf(s110,plain,
spl20_12,
inference(rat,[],[s13,s89]) ).
cnf(s111,plain,
spl20_11,
inference(rat,[],[s12,s89]) ).
cnf(s112,plain,
spl20_10,
inference(rat,[],[s11,s89]) ).
cnf(s113,plain,
spl20_9,
inference(rat,[],[s10,s89]) ).
cnf(s114,plain,
spl20_8,
inference(rat,[],[s9,s89]) ).
cnf(s115,plain,
spl20_7,
inference(rat,[],[s8,s89]) ).
cnf(s116,plain,
spl20_6,
inference(rat,[],[s7,s89]) ).
cnf(s117,plain,
spl20_5,
inference(rat,[],[s6,s89]) ).
cnf(s118,plain,
~ spl20_72,
inference(rat,[],[s87,s100,s98,s99,s102]) ).
cnf(s119,plain,
~ spl20_73,
inference(rat,[],[s86,s91,s90,s103]) ).
cnf(s120,plain,
~ spl20_63,
inference(rat,[],[s85,s116,s104,s105,s106,s107,s111,s112,s113,s114,s115,s117]) ).
cnf(s122,plain,
~ spl20_4,
inference(rat,[],[s84,s119,s101,s92,s93,s94,s95,s96,s97,s118]) ).
cnf(s123,plain,
~ spl20_3,
inference(rat,[],[s64,s110,s108,s109,s120]) ).
cnf(s124,plain,
$false,
inference(rat,[],[s5,s122,s123]) ).
fof(f553,plain,
$false,
inference(avatar_sat_refutation,[],[s124]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NLP009+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.34 % Computer : n012.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Sun Sep 27 17:46:49 UTC 2026
% 0.10/0.34 % CPUTime :
% 0.10/0.34 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.36 Running first-order theorem proving
% 0.10/0.36 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.55/1.11 % (2621244)Detected formulas, will run a generic FOF schedule.
% 2.55/1.11 % (2621254)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=428332841:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.55/1.11 % (2621253)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=799908551:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.55/1.11 % (2621251)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=757025882:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.55/1.11 % (2621252)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=801559031:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.55/1.11 % (2621250)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=1008420813:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.55/1.11 % (2621249)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=1723648605:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.55/1.11 % (2621254)First to succeed.
% 2.55/1.11 % (2621254)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2621244"
% 2.55/1.11 % (2621252)Refutation not found, incomplete strategy
% 2.55/1.11 % (2621252)------------------------------
% 2.55/1.11 % (2621252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.55/1.11 % (2621252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.55/1.11 % (2621252)CaDiCaL version: 2.1.3
% 2.55/1.11 % (2621252)Termination reason: Refutation not found, incomplete strategy
% 2.55/1.11 % (2621252)Time elapsed: 0.009 s
% 2.55/1.11 % (2621252)Peak memory usage: 88 MB
% 2.55/1.11 % (2621252)Instructions burned: 15 (million)
% 2.55/1.11 % (2621253)Instruction limit reached!
% 2.55/1.11 % (2621253)------------------------------
% 2.55/1.11 % (2621253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.55/1.11 % (2621253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.55/1.11 % (2621253)CaDiCaL version: 2.1.3
% 2.55/1.11 % (2621253)Termination reason: Instruction limit
% 2.55/1.11 % (2621253)Termination phase: Saturation
% 2.55/1.11 % (2621253)Time elapsed: 0.024 s
% 2.55/1.11 % (2621253)Peak memory usage: 88 MB
% 2.55/1.11 % (2621253)Instructions burned: 121 (million)
% 2.55/1.11 % (2621255)dis-21_1_sil=8000:lcm=predicate:random_seed=2500759126: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.55/1.11 % (2621255)Refutation not found, incomplete strategy
% 2.55/1.11 % (2621255)------------------------------
% 2.55/1.11 % (2621255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.55/1.11 % (2621255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.55/1.11 % (2621255)CaDiCaL version: 2.1.3
% 2.55/1.11 % (2621255)Termination reason: Refutation not found, incomplete strategy
% 2.55/1.11 % (2621255)Time elapsed: 0.003 s
% 2.55/1.11 % (2621255)Peak memory usage: 88 MB
% 2.55/1.11 % (2621255)Instructions burned: 4 (million)
% 2.55/1.11 % (2621262)lrs+10_1_sil=8000:sp=occurrence:random_seed=1808733146:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 2.55/1.11 % (2621262)Also succeeded, but the first one will report.
% 2.55/1.11 % (2621252)------------------------------
% 2.55/1.11 % (2621252)------------------------------
% 2.55/1.11 % (2621254)Refutation found. Thanks to Tanya!
% 2.55/1.11 % SZS status Theorem for theBenchmark
% 2.55/1.11 % SZS output start Proof for theBenchmark
% See solution above
% 3.27/1.24 % (2621254)------------------------------
% 3.27/1.24 % (2621254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.27/1.24 % (2621254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.27/1.24 % (2621254)CaDiCaL version: 2.1.3
% 3.27/1.24 % (2621254)Termination reason: Refutation
% 3.27/1.24 % (2621254)Time elapsed: 0.013 s
% 3.27/1.24 % (2621254)Peak memory usage: 90 MB
% 3.27/1.24 % (2621254)Instructions burned: 21 (million)
% 3.27/1.24 % (2621254)------------------------------
% 3.27/1.24 % (2621254)------------------------------
% 3.27/1.24 % (2621244)Success in time 0.408 s
% 3.27/1.24 % Vampire exiting
%------------------------------------------------------------------------------