%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NLP001+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 : n001.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:35 PM UTC 2026
% Result : Theorem 2.42s 1.23s
% Output : Refutation 3.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 24
% Syntax : Number of formulae : 210 ( 12 unt; 23 def)
% Number of atoms : 1168 ( 0 equ)
% Maximal formula atoms : 56 ( 5 avg)
% Number of connectives : 1724 ( 766 ~; 704 |; 229 &)
% ( 21 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 37 ( 6 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 38 ( 37 usr; 15 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 8 con; 0-0 aty)
% Number of variables : 189 ( 0 sgn 129 !; 60 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
( ( ? [X0,X1,X2,X3] :
( 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) )
=> ? [X4,X5,X6,X7] :
( hollywood(X4)
& city(X4)
& event(X5)
& chevy(X6)
& car(X6)
& white(X6)
& dirty(X6)
& old(X6)
& street(X7)
& way(X7)
& lonely(X7)
& barrel(X5,X6)
& down(X5,X7)
& in(X5,X4) ) )
& ( ? [X8,X9,X10,X11] :
( hollywood(X8)
& city(X8)
& event(X9)
& chevy(X10)
& car(X10)
& white(X10)
& dirty(X10)
& old(X10)
& street(X11)
& way(X11)
& lonely(X11)
& barrel(X9,X10)
& down(X9,X11)
& in(X9,X8) )
=> ? [X12,X13,X14,X15] :
( hollywood(X12)
& city(X12)
& event(X13)
& street(X14)
& way(X14)
& lonely(X14)
& chevy(X15)
& car(X15)
& white(X15)
& dirty(X15)
& old(X15)
& barrel(X13,X15)
& down(X13,X14)
& in(X13,X12) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f2,negated_conjecture,
~ ( ( ? [X0,X1,X2,X3] :
( 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) )
=> ? [X4,X5,X6,X7] :
( hollywood(X4)
& city(X4)
& event(X5)
& chevy(X6)
& car(X6)
& white(X6)
& dirty(X6)
& old(X6)
& street(X7)
& way(X7)
& lonely(X7)
& barrel(X5,X6)
& down(X5,X7)
& in(X5,X4) ) )
& ( ? [X8,X9,X10,X11] :
( hollywood(X8)
& city(X8)
& event(X9)
& chevy(X10)
& car(X10)
& white(X10)
& dirty(X10)
& old(X10)
& street(X11)
& way(X11)
& lonely(X11)
& barrel(X9,X10)
& down(X9,X11)
& in(X9,X8) )
=> ? [X12,X13,X14,X15] :
( hollywood(X12)
& city(X12)
& event(X13)
& street(X14)
& way(X14)
& lonely(X14)
& chevy(X15)
& car(X15)
& white(X15)
& dirty(X15)
& old(X15)
& barrel(X13,X15)
& down(X13,X14)
& in(X13,X12) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
( ( ! [X4,X5,X6,X7] :
( ~ hollywood(X4)
| ~ city(X4)
| ~ event(X5)
| ~ chevy(X6)
| ~ car(X6)
| ~ white(X6)
| ~ dirty(X6)
| ~ old(X6)
| ~ street(X7)
| ~ way(X7)
| ~ lonely(X7)
| ~ barrel(X5,X6)
| ~ down(X5,X7)
| ~ in(X5,X4) )
& ? [X0,X1,X2,X3] :
( 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) ) )
| ( ! [X12,X13,X14,X15] :
( ~ hollywood(X12)
| ~ city(X12)
| ~ event(X13)
| ~ street(X14)
| ~ way(X14)
| ~ lonely(X14)
| ~ chevy(X15)
| ~ car(X15)
| ~ white(X15)
| ~ dirty(X15)
| ~ old(X15)
| ~ barrel(X13,X15)
| ~ down(X13,X14)
| ~ in(X13,X12) )
& ? [X8,X9,X10,X11] :
( hollywood(X8)
& city(X8)
& event(X9)
& chevy(X10)
& car(X10)
& white(X10)
& dirty(X10)
& old(X10)
& street(X11)
& way(X11)
& lonely(X11)
& barrel(X9,X10)
& down(X9,X11)
& in(X9,X8) ) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f4,definition,
( ? [X8,X9,X10,X11] :
( hollywood(X8)
& city(X8)
& event(X9)
& chevy(X10)
& car(X10)
& white(X10)
& dirty(X10)
& old(X10)
& street(X11)
& way(X11)
& lonely(X11)
& barrel(X9,X10)
& down(X9,X11)
& in(X9,X8) )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f5,definition,
( ? [X0,X1,X2,X3] :
( 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) )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f6,plain,
( ( ! [X4,X5,X6,X7] :
( ~ hollywood(X4)
| ~ city(X4)
| ~ event(X5)
| ~ chevy(X6)
| ~ car(X6)
| ~ white(X6)
| ~ dirty(X6)
| ~ old(X6)
| ~ street(X7)
| ~ way(X7)
| ~ lonely(X7)
| ~ barrel(X5,X6)
| ~ down(X5,X7)
| ~ in(X5,X4) )
& sP1 )
| ( ! [X12,X13,X14,X15] :
( ~ hollywood(X12)
| ~ city(X12)
| ~ event(X13)
| ~ street(X14)
| ~ way(X14)
| ~ lonely(X14)
| ~ chevy(X15)
| ~ car(X15)
| ~ white(X15)
| ~ dirty(X15)
| ~ old(X15)
| ~ barrel(X13,X15)
| ~ down(X13,X14)
| ~ in(X13,X12) )
& sP0 ) ),
inference(definition_folding,[],[f3,f5,f4]) ).
fof(f7,plain,
( ? [X0,X1,X2,X3] :
( 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) )
| ~ 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) )
| ~ sP1 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4),skolemize(X3,sK5)],[f7]) ).
fof(f9,plain,
( ? [X8,X9,X10,X11] :
( hollywood(X8)
& city(X8)
& event(X9)
& chevy(X10)
& car(X10)
& white(X10)
& dirty(X10)
& old(X10)
& street(X11)
& way(X11)
& lonely(X11)
& barrel(X9,X10)
& down(X9,X11)
& in(X9,X8) )
| ~ sP0 ),
inference(nnf_transformation,[],[f4]) ).
fof(f10,plain,
( ? [X0,X1,X2,X3] :
( 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) )
| ~ sP0 ),
inference(rectify,[],[f9]) ).
fof(f11,plain,
( ( hollywood(sK6)
& city(sK6)
& event(sK7)
& chevy(sK8)
& car(sK8)
& white(sK8)
& dirty(sK8)
& old(sK8)
& street(sK9)
& way(sK9)
& lonely(sK9)
& barrel(sK7,sK8)
& down(sK7,sK9)
& in(sK7,sK6) )
| ~ sP0 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7,sK8,sK9]),skolemize(X0,sK6),skolemize(X1,sK7),skolemize(X2,sK8),skolemize(X3,sK9)],[f10]) ).
fof(f12,plain,
( ( ! [X0,X1,X2,X3] :
( ~ 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) )
& sP1 )
| ( ! [X4,X5,X6,X7] :
( ~ hollywood(X4)
| ~ city(X4)
| ~ event(X5)
| ~ street(X6)
| ~ way(X6)
| ~ lonely(X6)
| ~ chevy(X7)
| ~ car(X7)
| ~ white(X7)
| ~ dirty(X7)
| ~ old(X7)
| ~ barrel(X5,X7)
| ~ down(X5,X6)
| ~ in(X5,X4) )
& sP0 ) ),
inference(rectify,[],[f6]) ).
fof(f13,plain,
( in(sK3,sK2)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f14,plain,
( down(sK3,sK4)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f15,plain,
( barrel(sK3,sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f16,plain,
( old(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f17,plain,
( dirty(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f18,plain,
( white(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f19,plain,
( car(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f20,plain,
( chevy(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f21,plain,
( lonely(sK4)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f22,plain,
( way(sK4)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f23,plain,
( street(sK4)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f24,plain,
( event(sK3)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f25,plain,
( city(sK2)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f26,plain,
( hollywood(sK2)
| ~ sP1 ),
inference(cnf_transformation,[],[f8]) ).
fof(f27,plain,
( in(sK7,sK6)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f28,plain,
( down(sK7,sK9)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f29,plain,
( barrel(sK7,sK8)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f30,plain,
( lonely(sK9)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f31,plain,
( way(sK9)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f32,plain,
( street(sK9)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f33,plain,
( old(sK8)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f34,plain,
( dirty(sK8)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f35,plain,
( white(sK8)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f36,plain,
( car(sK8)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f37,plain,
( chevy(sK8)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f38,plain,
( event(sK7)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f39,plain,
( city(sK6)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f40,plain,
( hollywood(sK6)
| ~ sP0 ),
inference(cnf_transformation,[],[f11]) ).
fof(f41,plain,
( sP1
| sP0 ),
inference(cnf_transformation,[],[f12]) ).
fof(f42,plain,
! [X6,X7,X4,X5] :
( sP1
| ~ hollywood(X4)
| ~ city(X4)
| ~ event(X5)
| ~ street(X6)
| ~ way(X6)
| ~ lonely(X6)
| ~ chevy(X7)
| ~ car(X7)
| ~ white(X7)
| ~ dirty(X7)
| ~ old(X7)
| ~ barrel(X5,X7)
| ~ down(X5,X6)
| ~ in(X5,X4) ),
inference(cnf_transformation,[],[f12]) ).
fof(f43,plain,
! [X2,X3,X0,X1] :
( ~ 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)
| sP0 ),
inference(cnf_transformation,[],[f12]) ).
fof(f44,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ 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)
| ~ hollywood(X4)
| ~ city(X4)
| ~ event(X5)
| ~ street(X6)
| ~ way(X6)
| ~ lonely(X6)
| ~ chevy(X7)
| ~ car(X7)
| ~ white(X7)
| ~ dirty(X7)
| ~ old(X7)
| ~ barrel(X5,X7)
| ~ down(X5,X6)
| ~ in(X5,X4) ),
inference(cnf_transformation,[],[f12]) ).
fof(f45,plain,
! [X2,X1] :
( ~ barrel(X1,X2)
| ~ car(X2)
| ~ white(X2)
| ~ dirty(X2)
| ~ old(X2)
| ~ chevy(X2)
| sP10(X1) ),
inference(cnf_transformation,[],[f45_D]) ).
fof(f45_D,definition,
! [X1] :
( ! [X2] :
( ~ barrel(X1,X2)
| ~ car(X2)
| ~ white(X2)
| ~ dirty(X2)
| ~ old(X2)
| ~ chevy(X2) )
<=> ~ sP10(X1) ),
introduced(definition,[new_symbols(definition,[sP10])],[general_splitting_component_introduction]) ).
fof(f46,plain,
! [X3,X0,X1,X6,X7,X4,X5] :
( ~ hollywood(X0)
| ~ city(X0)
| ~ event(X1)
| ~ street(X3)
| ~ way(X3)
| ~ lonely(X3)
| ~ down(X1,X3)
| ~ in(X1,X0)
| ~ hollywood(X4)
| ~ city(X4)
| ~ event(X5)
| ~ street(X6)
| ~ way(X6)
| ~ lonely(X6)
| ~ chevy(X7)
| ~ car(X7)
| ~ white(X7)
| ~ dirty(X7)
| ~ old(X7)
| ~ barrel(X5,X7)
| ~ down(X5,X6)
| ~ in(X5,X4)
| ~ sP10(X1) ),
inference(general_splitting,[],[f44,f45_D]) ).
fof(f47,plain,
! [X3,X1] :
( ~ down(X1,X3)
| ~ way(X3)
| ~ lonely(X3)
| ~ street(X3)
| sP11(X1) ),
inference(cnf_transformation,[],[f47_D]) ).
fof(f47_D,definition,
! [X1] :
( ! [X3] :
( ~ down(X1,X3)
| ~ way(X3)
| ~ lonely(X3)
| ~ street(X3) )
<=> ~ sP11(X1) ),
introduced(definition,[new_symbols(definition,[sP11])],[general_splitting_component_introduction]) ).
fof(f48,plain,
! [X0,X1,X6,X7,X4,X5] :
( ~ hollywood(X0)
| ~ city(X0)
| ~ event(X1)
| ~ in(X1,X0)
| ~ hollywood(X4)
| ~ city(X4)
| ~ event(X5)
| ~ street(X6)
| ~ way(X6)
| ~ lonely(X6)
| ~ chevy(X7)
| ~ car(X7)
| ~ white(X7)
| ~ dirty(X7)
| ~ old(X7)
| ~ barrel(X5,X7)
| ~ down(X5,X6)
| ~ in(X5,X4)
| ~ sP10(X1)
| ~ sP11(X1) ),
inference(general_splitting,[],[f46,f47_D]) ).
fof(f49,plain,
! [X0,X1] :
( ~ in(X1,X0)
| ~ city(X0)
| ~ hollywood(X0)
| sP12(X1) ),
inference(cnf_transformation,[],[f49_D]) ).
fof(f49_D,definition,
! [X1] :
( ! [X0] :
( ~ in(X1,X0)
| ~ city(X0)
| ~ hollywood(X0) )
<=> ~ sP12(X1) ),
introduced(definition,[new_symbols(definition,[sP12])],[general_splitting_component_introduction]) ).
fof(f50,plain,
! [X1,X6,X7,X4,X5] :
( ~ event(X1)
| ~ hollywood(X4)
| ~ city(X4)
| ~ event(X5)
| ~ street(X6)
| ~ way(X6)
| ~ lonely(X6)
| ~ chevy(X7)
| ~ car(X7)
| ~ white(X7)
| ~ dirty(X7)
| ~ old(X7)
| ~ barrel(X5,X7)
| ~ down(X5,X6)
| ~ in(X5,X4)
| ~ sP10(X1)
| ~ sP11(X1)
| ~ sP12(X1) ),
inference(general_splitting,[],[f48,f49_D]) ).
fof(f51,plain,
! [X1] :
( ~ event(X1)
| ~ sP10(X1)
| ~ sP11(X1)
| ~ sP12(X1)
| sP13 ),
inference(cnf_transformation,[],[f51_D]) ).
fof(f51_D,definition,
( ! [X1] :
( ~ event(X1)
| ~ sP10(X1)
| ~ sP11(X1)
| ~ sP12(X1) )
<=> ~ sP13 ),
introduced(definition,[new_symbols(definition,[sP13])],[general_splitting_component_introduction]) ).
fof(f52,plain,
! [X6,X7,X4,X5] :
( ~ hollywood(X4)
| ~ city(X4)
| ~ event(X5)
| ~ street(X6)
| ~ way(X6)
| ~ lonely(X6)
| ~ chevy(X7)
| ~ car(X7)
| ~ white(X7)
| ~ dirty(X7)
| ~ old(X7)
| ~ barrel(X5,X7)
| ~ down(X5,X6)
| ~ in(X5,X4)
| ~ sP13 ),
inference(general_splitting,[],[f50,f51_D]) ).
fof(f53,plain,
! [X6,X5] :
( ~ down(X5,X6)
| ~ way(X6)
| ~ lonely(X6)
| ~ street(X6)
| sP14(X5) ),
inference(cnf_transformation,[],[f53_D]) ).
fof(f53_D,definition,
! [X5] :
( ! [X6] :
( ~ down(X5,X6)
| ~ way(X6)
| ~ lonely(X6)
| ~ street(X6) )
<=> ~ sP14(X5) ),
introduced(definition,[new_symbols(definition,[sP14])],[general_splitting_component_introduction]) ).
fof(f54,plain,
! [X7,X4,X5] :
( ~ hollywood(X4)
| ~ city(X4)
| ~ event(X5)
| ~ chevy(X7)
| ~ car(X7)
| ~ white(X7)
| ~ dirty(X7)
| ~ old(X7)
| ~ barrel(X5,X7)
| ~ in(X5,X4)
| ~ sP13
| ~ sP14(X5) ),
inference(general_splitting,[],[f52,f53_D]) ).
fof(f55,plain,
! [X7,X5] :
( ~ barrel(X5,X7)
| ~ car(X7)
| ~ white(X7)
| ~ dirty(X7)
| ~ old(X7)
| ~ chevy(X7)
| sP15(X5) ),
inference(cnf_transformation,[],[f55_D]) ).
fof(f55_D,definition,
! [X5] :
( ! [X7] :
( ~ barrel(X5,X7)
| ~ car(X7)
| ~ white(X7)
| ~ dirty(X7)
| ~ old(X7)
| ~ chevy(X7) )
<=> ~ sP15(X5) ),
introduced(definition,[new_symbols(definition,[sP15])],[general_splitting_component_introduction]) ).
fof(f56,plain,
! [X4,X5] :
( ~ hollywood(X4)
| ~ city(X4)
| ~ event(X5)
| ~ in(X5,X4)
| ~ sP13
| ~ sP14(X5)
| ~ sP15(X5) ),
inference(general_splitting,[],[f54,f55_D]) ).
fof(f57,plain,
! [X2,X1] :
( ~ barrel(X1,X2)
| ~ car(X2)
| ~ white(X2)
| ~ dirty(X2)
| ~ old(X2)
| ~ chevy(X2)
| sP16(X1) ),
inference(cnf_transformation,[],[f57_D]) ).
fof(f57_D,definition,
! [X1] :
( ! [X2] :
( ~ barrel(X1,X2)
| ~ car(X2)
| ~ white(X2)
| ~ dirty(X2)
| ~ old(X2)
| ~ chevy(X2) )
<=> ~ sP16(X1) ),
introduced(definition,[new_symbols(definition,[sP16])],[general_splitting_component_introduction]) ).
fof(f58,plain,
! [X3,X0,X1] :
( ~ hollywood(X0)
| ~ city(X0)
| ~ event(X1)
| ~ street(X3)
| ~ way(X3)
| ~ lonely(X3)
| ~ down(X1,X3)
| ~ in(X1,X0)
| sP0
| ~ sP16(X1) ),
inference(general_splitting,[],[f43,f57_D]) ).
fof(f59,plain,
! [X3,X1] :
( ~ down(X1,X3)
| ~ way(X3)
| ~ lonely(X3)
| ~ street(X3)
| sP17(X1) ),
inference(cnf_transformation,[],[f59_D]) ).
fof(f59_D,definition,
! [X1] :
( ! [X3] :
( ~ down(X1,X3)
| ~ way(X3)
| ~ lonely(X3)
| ~ street(X3) )
<=> ~ sP17(X1) ),
introduced(definition,[new_symbols(definition,[sP17])],[general_splitting_component_introduction]) ).
fof(f60,plain,
! [X0,X1] :
( ~ hollywood(X0)
| ~ city(X0)
| ~ event(X1)
| ~ in(X1,X0)
| sP0
| ~ sP16(X1)
| ~ sP17(X1) ),
inference(general_splitting,[],[f58,f59_D]) ).
fof(f61,plain,
! [X6,X5] :
( ~ down(X5,X6)
| ~ way(X6)
| ~ lonely(X6)
| ~ street(X6)
| sP18(X5) ),
inference(cnf_transformation,[],[f61_D]) ).
fof(f61_D,definition,
! [X5] :
( ! [X6] :
( ~ down(X5,X6)
| ~ way(X6)
| ~ lonely(X6)
| ~ street(X6) )
<=> ~ sP18(X5) ),
introduced(definition,[new_symbols(definition,[sP18])],[general_splitting_component_introduction]) ).
fof(f62,plain,
! [X7,X4,X5] :
( sP1
| ~ hollywood(X4)
| ~ city(X4)
| ~ event(X5)
| ~ chevy(X7)
| ~ car(X7)
| ~ white(X7)
| ~ dirty(X7)
| ~ old(X7)
| ~ barrel(X5,X7)
| ~ in(X5,X4)
| ~ sP18(X5) ),
inference(general_splitting,[],[f42,f61_D]) ).
fof(f63,plain,
! [X7,X5] :
( ~ barrel(X5,X7)
| ~ car(X7)
| ~ white(X7)
| ~ dirty(X7)
| ~ old(X7)
| ~ chevy(X7)
| sP19(X5) ),
inference(cnf_transformation,[],[f63_D]) ).
fof(f63_D,definition,
! [X5] :
( ! [X7] :
( ~ barrel(X5,X7)
| ~ car(X7)
| ~ white(X7)
| ~ dirty(X7)
| ~ old(X7)
| ~ chevy(X7) )
<=> ~ sP19(X5) ),
introduced(definition,[new_symbols(definition,[sP19])],[general_splitting_component_introduction]) ).
fof(f64,plain,
! [X4,X5] :
( sP1
| ~ hollywood(X4)
| ~ city(X4)
| ~ event(X5)
| ~ in(X5,X4)
| ~ sP18(X5)
| ~ sP19(X5) ),
inference(general_splitting,[],[f62,f63_D]) ).
fof(f66,definition,
( spl20_1
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl20_1])],[avatar_definition]) ).
fof(f68,plain,
( sP0
| ~ spl20_1 ),
inference(avatar_component_clause,[],[f66]) ).
fof(f70,definition,
( spl20_2
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl20_2])],[avatar_definition]) ).
fof(f72,plain,
( sP1
| ~ spl20_2 ),
inference(avatar_component_clause,[],[f70]) ).
fof(f73,plain,
( spl20_1
| spl20_2 ),
inference(avatar_split_clause,[],[f41,f70,f66]) ).
fof(f75,definition,
( spl20_3
<=> sP13 ),
introduced(definition,[new_symbols(definition,[spl20_3])],[avatar_definition]) ).
fof(f79,definition,
( spl20_4
<=> ! [X1] :
( ~ event(X1)
| ~ sP12(X1)
| ~ sP11(X1)
| ~ sP10(X1) ) ),
introduced(definition,[new_symbols(definition,[spl20_4])],[avatar_definition]) ).
fof(f80,plain,
( ! [X1] :
( ~ sP12(X1)
| ~ event(X1)
| ~ sP11(X1)
| ~ sP10(X1) )
| ~ spl20_4 ),
inference(avatar_component_clause,[],[f79]) ).
fof(f81,plain,
( spl20_3
| spl20_4 ),
inference(avatar_split_clause,[],[f51,f79,f75]) ).
fof(f83,definition,
( spl20_5
<=> ! [X4,X5] :
( ~ hollywood(X4)
| ~ sP15(X5)
| ~ sP14(X5)
| ~ event(X5)
| ~ in(X5,X4)
| ~ city(X4) ) ),
introduced(definition,[new_symbols(definition,[spl20_5])],[avatar_definition]) ).
fof(f84,plain,
( ! [X4,X5] :
( ~ in(X5,X4)
| ~ sP15(X5)
| ~ sP14(X5)
| ~ event(X5)
| ~ hollywood(X4)
| ~ city(X4) )
| ~ spl20_5 ),
inference(avatar_component_clause,[],[f83]) ).
fof(f85,plain,
( ~ spl20_3
| spl20_5 ),
inference(avatar_split_clause,[],[f56,f83,f75]) ).
fof(f87,definition,
( spl20_6
<=> ! [X0,X1] :
( ~ hollywood(X0)
| ~ sP17(X1)
| ~ sP16(X1)
| ~ event(X1)
| ~ in(X1,X0)
| ~ city(X0) ) ),
introduced(definition,[new_symbols(definition,[spl20_6])],[avatar_definition]) ).
fof(f88,plain,
( ! [X0,X1] :
( ~ in(X1,X0)
| ~ sP17(X1)
| ~ sP16(X1)
| ~ event(X1)
| ~ hollywood(X0)
| ~ city(X0) )
| ~ spl20_6 ),
inference(avatar_component_clause,[],[f87]) ).
fof(f89,plain,
( spl20_1
| spl20_6 ),
inference(avatar_split_clause,[],[f60,f87,f66]) ).
fof(f91,definition,
( spl20_7
<=> ! [X4,X5] :
( ~ hollywood(X4)
| ~ sP19(X5)
| ~ sP18(X5)
| ~ event(X5)
| ~ in(X5,X4)
| ~ city(X4) ) ),
introduced(definition,[new_symbols(definition,[spl20_7])],[avatar_definition]) ).
fof(f92,plain,
( ! [X4,X5] :
( ~ in(X5,X4)
| ~ sP19(X5)
| ~ sP18(X5)
| ~ event(X5)
| ~ hollywood(X4)
| ~ city(X4) )
| ~ spl20_7 ),
inference(avatar_component_clause,[],[f91]) ).
fof(f93,plain,
( spl20_7
| spl20_2 ),
inference(avatar_split_clause,[],[f64,f70,f91]) ).
fof(f94,plain,
( ~ city(sK2)
| ~ hollywood(sK2)
| sP12(sK3)
| ~ sP1 ),
inference(resolution,[],[f49,f13]) ).
fof(f97,plain,
( ~ hollywood(sK2)
| sP12(sK3)
| ~ sP1 ),
inference(forward_subsumption_resolution,[],[f94,f25]) ).
fof(f99,plain,
( sP12(sK3)
| ~ sP1 ),
inference(forward_subsumption_resolution,[],[f97,f26]) ).
fof(f105,plain,
( sP12(sK3)
| ~ spl20_2 ),
inference(forward_subsumption_resolution,[],[f99,f72]) ).
fof(f106,plain,
( ~ way(sK4)
| ~ lonely(sK4)
| ~ street(sK4)
| sP11(sK3)
| ~ sP1 ),
inference(resolution,[],[f47,f14]) ).
fof(f108,plain,
( ~ lonely(sK4)
| ~ street(sK4)
| sP11(sK3)
| ~ sP1 ),
inference(forward_subsumption_resolution,[],[f106,f22]) ).
fof(f109,plain,
( ~ street(sK4)
| sP11(sK3)
| ~ sP1 ),
inference(forward_subsumption_resolution,[],[f108,f21]) ).
fof(f110,plain,
( sP11(sK3)
| ~ sP1 ),
inference(forward_subsumption_resolution,[],[f109,f23]) ).
fof(f111,plain,
( sP11(sK3)
| ~ spl20_2 ),
inference(forward_subsumption_resolution,[],[f110,f72]) ).
fof(f112,plain,
( ~ event(sK3)
| ~ sP11(sK3)
| ~ sP10(sK3)
| ~ spl20_2
| ~ spl20_4 ),
inference(resolution,[],[f105,f80]) ).
fof(f113,plain,
( ~ event(sK3)
| ~ sP10(sK3)
| ~ spl20_2
| ~ spl20_4 ),
inference(forward_subsumption_resolution,[],[f112,f111]) ).
fof(f115,definition,
( spl20_9
<=> sP10(sK3) ),
introduced(definition,[new_symbols(definition,[spl20_9])],[avatar_definition]) ).
fof(f117,plain,
( ~ sP10(sK3)
| spl20_9 ),
inference(avatar_component_clause,[],[f115]) ).
fof(f119,definition,
( spl20_10
<=> event(sK3) ),
introduced(definition,[new_symbols(definition,[spl20_10])],[avatar_definition]) ).
fof(f120,plain,
( event(sK3)
| ~ spl20_10 ),
inference(avatar_component_clause,[],[f119]) ).
fof(f121,plain,
( ~ event(sK3)
| spl20_10 ),
inference(avatar_component_clause,[],[f119]) ).
fof(f123,plain,
( ~ way(sK4)
| ~ lonely(sK4)
| ~ street(sK4)
| sP14(sK3)
| ~ sP1 ),
inference(resolution,[],[f53,f14]) ).
fof(f125,plain,
( ~ lonely(sK4)
| ~ street(sK4)
| sP14(sK3)
| ~ sP1 ),
inference(forward_subsumption_resolution,[],[f123,f22]) ).
fof(f126,plain,
( ~ street(sK4)
| sP14(sK3)
| ~ sP1 ),
inference(forward_subsumption_resolution,[],[f125,f21]) ).
fof(f127,plain,
( sP14(sK3)
| ~ sP1 ),
inference(forward_subsumption_resolution,[],[f126,f23]) ).
fof(f129,plain,
( ~ way(sK4)
| ~ lonely(sK4)
| ~ street(sK4)
| sP17(sK3)
| ~ sP1 ),
inference(resolution,[],[f59,f14]) ).
fof(f131,plain,
( ~ lonely(sK4)
| ~ street(sK4)
| sP17(sK3)
| ~ sP1 ),
inference(forward_subsumption_resolution,[],[f129,f22]) ).
fof(f132,plain,
( ~ street(sK4)
| sP17(sK3)
| ~ sP1 ),
inference(forward_subsumption_resolution,[],[f131,f21]) ).
fof(f133,plain,
( sP17(sK3)
| ~ sP1 ),
inference(forward_subsumption_resolution,[],[f132,f23]) ).
fof(f134,plain,
( sP17(sK3)
| ~ spl20_2 ),
inference(forward_subsumption_resolution,[],[f133,f72]) ).
fof(f136,plain,
( ~ way(sK9)
| ~ lonely(sK9)
| ~ street(sK9)
| sP18(sK7)
| ~ sP0 ),
inference(resolution,[],[f61,f28]) ).
fof(f141,plain,
( ~ sP17(sK3)
| ~ sP16(sK3)
| ~ event(sK3)
| ~ hollywood(sK2)
| ~ city(sK2)
| ~ sP1
| ~ spl20_6 ),
inference(resolution,[],[f88,f13]) ).
fof(f143,plain,
( ~ sP16(sK3)
| ~ event(sK3)
| ~ hollywood(sK2)
| ~ city(sK2)
| ~ sP1
| ~ spl20_2
| ~ spl20_6 ),
inference(forward_subsumption_resolution,[],[f141,f134]) ).
fof(f144,plain,
( ~ sP16(sK3)
| ~ hollywood(sK2)
| ~ city(sK2)
| ~ sP1
| ~ spl20_2
| ~ spl20_6 ),
inference(forward_subsumption_resolution,[],[f143,f24]) ).
fof(f145,plain,
( ~ sP16(sK3)
| ~ city(sK2)
| ~ sP1
| ~ spl20_2
| ~ spl20_6 ),
inference(forward_subsumption_resolution,[],[f144,f26]) ).
fof(f146,plain,
( ~ sP16(sK3)
| ~ sP1
| ~ spl20_2
| ~ spl20_6 ),
inference(forward_subsumption_resolution,[],[f145,f25]) ).
fof(f147,plain,
( ~ sP16(sK3)
| ~ spl20_2
| ~ spl20_6 ),
inference(forward_subsumption_resolution,[],[f146,f72]) ).
fof(f148,plain,
( ~ car(sK5)
| ~ white(sK5)
| ~ dirty(sK5)
| ~ old(sK5)
| ~ chevy(sK5)
| sP10(sK3)
| ~ sP1 ),
inference(resolution,[],[f45,f15]) ).
fof(f150,plain,
( ~ white(sK5)
| ~ dirty(sK5)
| ~ old(sK5)
| ~ chevy(sK5)
| sP10(sK3)
| ~ sP1 ),
inference(forward_subsumption_resolution,[],[f148,f19]) ).
fof(f151,plain,
( ~ dirty(sK5)
| ~ old(sK5)
| ~ chevy(sK5)
| sP10(sK3)
| ~ sP1 ),
inference(forward_subsumption_resolution,[],[f150,f18]) ).
fof(f152,plain,
( ~ old(sK5)
| ~ chevy(sK5)
| sP10(sK3)
| ~ sP1 ),
inference(forward_subsumption_resolution,[],[f151,f17]) ).
fof(f153,plain,
( ~ chevy(sK5)
| sP10(sK3)
| ~ sP1 ),
inference(forward_subsumption_resolution,[],[f152,f16]) ).
fof(f154,plain,
( sP10(sK3)
| ~ sP1 ),
inference(forward_subsumption_resolution,[],[f153,f20]) ).
fof(f155,plain,
( ~ sP1
| spl20_9 ),
inference(forward_subsumption_resolution,[],[f154,f117]) ).
fof(f156,plain,
( $false
| ~ spl20_2
| spl20_9 ),
inference(forward_subsumption_resolution,[],[f155,f72]) ).
fof(f157,plain,
( ~ spl20_2
| spl20_9 ),
inference(avatar_contradiction_clause,[],[f156]) ).
fof(f161,plain,
( ~ lonely(sK9)
| ~ street(sK9)
| sP18(sK7)
| ~ sP0 ),
inference(forward_subsumption_resolution,[],[f136,f31]) ).
fof(f167,plain,
( ~ street(sK9)
| sP18(sK7)
| ~ sP0 ),
inference(forward_subsumption_resolution,[],[f161,f30]) ).
fof(f173,plain,
( sP18(sK7)
| ~ sP0 ),
inference(forward_subsumption_resolution,[],[f167,f32]) ).
fof(f189,plain,
( ~ sP19(sK7)
| ~ sP18(sK7)
| ~ event(sK7)
| ~ hollywood(sK6)
| ~ city(sK6)
| ~ sP0
| ~ spl20_7 ),
inference(resolution,[],[f92,f27]) ).
fof(f190,plain,
( ~ car(sK5)
| ~ white(sK5)
| ~ dirty(sK5)
| ~ old(sK5)
| ~ chevy(sK5)
| sP15(sK3)
| ~ sP1 ),
inference(resolution,[],[f55,f15]) ).
fof(f198,plain,
( ~ car(sK5)
| ~ white(sK5)
| ~ dirty(sK5)
| ~ old(sK5)
| ~ chevy(sK5)
| sP16(sK3)
| ~ sP1 ),
inference(resolution,[],[f57,f15]) ).
fof(f208,plain,
( ~ spl20_9
| ~ spl20_10
| ~ spl20_2
| ~ spl20_4 ),
inference(avatar_split_clause,[],[f113,f79,f70,f119,f115]) ).
fof(f214,plain,
( ~ white(sK5)
| ~ dirty(sK5)
| ~ old(sK5)
| ~ chevy(sK5)
| sP15(sK3)
| ~ sP1 ),
inference(forward_subsumption_resolution,[],[f190,f19]) ).
fof(f215,plain,
( ~ white(sK5)
| ~ dirty(sK5)
| ~ old(sK5)
| ~ chevy(sK5)
| sP16(sK3)
| ~ sP1 ),
inference(forward_subsumption_resolution,[],[f198,f19]) ).
fof(f229,plain,
( ~ dirty(sK5)
| ~ old(sK5)
| ~ chevy(sK5)
| sP15(sK3)
| ~ sP1 ),
inference(forward_subsumption_resolution,[],[f214,f18]) ).
fof(f230,plain,
( ~ dirty(sK5)
| ~ old(sK5)
| ~ chevy(sK5)
| sP16(sK3)
| ~ sP1 ),
inference(forward_subsumption_resolution,[],[f215,f18]) ).
fof(f231,plain,
( ~ old(sK5)
| ~ chevy(sK5)
| sP15(sK3)
| ~ sP1 ),
inference(forward_subsumption_resolution,[],[f229,f17]) ).
fof(f232,plain,
( ~ old(sK5)
| ~ chevy(sK5)
| sP16(sK3)
| ~ sP1 ),
inference(forward_subsumption_resolution,[],[f230,f17]) ).
fof(f233,plain,
( ~ chevy(sK5)
| sP15(sK3)
| ~ sP1 ),
inference(forward_subsumption_resolution,[],[f231,f16]) ).
fof(f234,plain,
( ~ chevy(sK5)
| sP16(sK3)
| ~ sP1 ),
inference(forward_subsumption_resolution,[],[f232,f16]) ).
fof(f235,plain,
( sP15(sK3)
| ~ sP1 ),
inference(forward_subsumption_resolution,[],[f233,f20]) ).
fof(f236,plain,
( sP16(sK3)
| ~ sP1 ),
inference(forward_subsumption_resolution,[],[f234,f20]) ).
fof(f238,plain,
( ~ sP1
| ~ spl20_2
| ~ spl20_6 ),
inference(forward_subsumption_resolution,[],[f236,f147]) ).
fof(f239,plain,
( $false
| ~ spl20_2
| ~ spl20_6 ),
inference(forward_subsumption_resolution,[],[f238,f72]) ).
fof(f240,plain,
( ~ spl20_2
| ~ spl20_6 ),
inference(avatar_contradiction_clause,[],[f239]) ).
fof(f253,definition,
( spl20_16
<=> sP14(sK3) ),
introduced(definition,[new_symbols(definition,[spl20_16])],[avatar_definition]) ).
fof(f255,plain,
( sP14(sK3)
| ~ spl20_16 ),
inference(avatar_component_clause,[],[f253]) ).
fof(f256,plain,
( ~ spl20_2
| spl20_16 ),
inference(avatar_split_clause,[],[f127,f253,f70]) ).
fof(f268,definition,
( spl20_19
<=> sP15(sK3) ),
introduced(definition,[new_symbols(definition,[spl20_19])],[avatar_definition]) ).
fof(f270,plain,
( sP15(sK3)
| ~ spl20_19 ),
inference(avatar_component_clause,[],[f268]) ).
fof(f271,plain,
( ~ spl20_2
| spl20_19 ),
inference(avatar_split_clause,[],[f235,f268,f70]) ).
fof(f280,plain,
( sP18(sK7)
| ~ spl20_1 ),
inference(forward_subsumption_resolution,[],[f173,f68]) ).
fof(f282,plain,
( ~ sP19(sK7)
| ~ sP18(sK7)
| ~ hollywood(sK6)
| ~ city(sK6)
| ~ sP0
| ~ spl20_7 ),
inference(forward_subsumption_resolution,[],[f189,f38]) ).
fof(f288,plain,
( ~ sP19(sK7)
| ~ hollywood(sK6)
| ~ city(sK6)
| ~ sP0
| ~ spl20_1
| ~ spl20_7 ),
inference(forward_subsumption_resolution,[],[f282,f280]) ).
fof(f289,plain,
( ~ sP19(sK7)
| ~ city(sK6)
| ~ sP0
| ~ spl20_1
| ~ spl20_7 ),
inference(forward_subsumption_resolution,[],[f288,f40]) ).
fof(f290,plain,
( ~ sP19(sK7)
| ~ sP0
| ~ spl20_1
| ~ spl20_7 ),
inference(forward_subsumption_resolution,[],[f289,f39]) ).
fof(f291,plain,
( ~ sP19(sK7)
| ~ spl20_1
| ~ spl20_7 ),
inference(forward_subsumption_resolution,[],[f290,f68]) ).
fof(f293,plain,
( ~ car(sK8)
| ~ white(sK8)
| ~ dirty(sK8)
| ~ old(sK8)
| ~ chevy(sK8)
| sP19(sK7)
| ~ sP0 ),
inference(resolution,[],[f63,f29]) ).
fof(f294,plain,
( ~ white(sK8)
| ~ dirty(sK8)
| ~ old(sK8)
| ~ chevy(sK8)
| sP19(sK7)
| ~ sP0 ),
inference(forward_subsumption_resolution,[],[f293,f36]) ).
fof(f295,plain,
( ~ dirty(sK8)
| ~ old(sK8)
| ~ chevy(sK8)
| sP19(sK7)
| ~ sP0 ),
inference(forward_subsumption_resolution,[],[f294,f35]) ).
fof(f296,plain,
( ~ old(sK8)
| ~ chevy(sK8)
| sP19(sK7)
| ~ sP0 ),
inference(forward_subsumption_resolution,[],[f295,f34]) ).
fof(f297,plain,
( ~ chevy(sK8)
| sP19(sK7)
| ~ sP0 ),
inference(forward_subsumption_resolution,[],[f296,f33]) ).
fof(f298,plain,
( sP19(sK7)
| ~ sP0 ),
inference(forward_subsumption_resolution,[],[f297,f37]) ).
fof(f299,plain,
( ~ sP0
| ~ spl20_1
| ~ spl20_7 ),
inference(forward_subsumption_resolution,[],[f298,f291]) ).
fof(f300,plain,
( $false
| ~ spl20_1
| ~ spl20_7 ),
inference(forward_subsumption_resolution,[],[f299,f68]) ).
fof(f301,plain,
( ~ spl20_1
| ~ spl20_7 ),
inference(avatar_contradiction_clause,[],[f300]) ).
fof(f310,plain,
( ~ sP1
| spl20_10 ),
inference(resolution,[],[f121,f24]) ).
fof(f311,plain,
( $false
| ~ spl20_2
| spl20_10 ),
inference(forward_subsumption_resolution,[],[f310,f72]) ).
fof(f312,plain,
( ~ spl20_2
| spl20_10 ),
inference(avatar_contradiction_clause,[],[f311]) ).
fof(f313,plain,
( ~ sP15(sK3)
| ~ sP14(sK3)
| ~ event(sK3)
| ~ hollywood(sK2)
| ~ city(sK2)
| ~ sP1
| ~ spl20_5 ),
inference(resolution,[],[f84,f13]) ).
fof(f315,plain,
( ~ sP14(sK3)
| ~ event(sK3)
| ~ hollywood(sK2)
| ~ city(sK2)
| ~ sP1
| ~ spl20_5
| ~ spl20_19 ),
inference(forward_subsumption_resolution,[],[f313,f270]) ).
fof(f316,plain,
( ~ event(sK3)
| ~ hollywood(sK2)
| ~ city(sK2)
| ~ sP1
| ~ spl20_5
| ~ spl20_16
| ~ spl20_19 ),
inference(forward_subsumption_resolution,[],[f315,f255]) ).
fof(f317,plain,
( ~ hollywood(sK2)
| ~ city(sK2)
| ~ sP1
| ~ spl20_5
| ~ spl20_10
| ~ spl20_16
| ~ spl20_19 ),
inference(forward_subsumption_resolution,[],[f316,f120]) ).
fof(f318,plain,
( ~ city(sK2)
| ~ sP1
| ~ spl20_5
| ~ spl20_10
| ~ spl20_16
| ~ spl20_19 ),
inference(forward_subsumption_resolution,[],[f317,f26]) ).
fof(f319,plain,
( ~ sP1
| ~ spl20_5
| ~ spl20_10
| ~ spl20_16
| ~ spl20_19 ),
inference(forward_subsumption_resolution,[],[f318,f25]) ).
fof(f320,plain,
( $false
| ~ spl20_2
| ~ spl20_5
| ~ spl20_10
| ~ spl20_16
| ~ spl20_19 ),
inference(forward_subsumption_resolution,[],[f319,f72]) ).
fof(f321,plain,
( ~ spl20_2
| ~ spl20_5
| ~ spl20_10
| ~ spl20_16
| ~ spl20_19 ),
inference(avatar_contradiction_clause,[],[f320]) ).
cnf(s1,plain,
( spl20_1
| spl20_2 ),
inference(sat_conversion,[],[f73]) ).
cnf(s2,plain,
( spl20_3
| spl20_4 ),
inference(sat_conversion,[],[f81]) ).
cnf(s3,plain,
( ~ spl20_3
| spl20_5 ),
inference(sat_conversion,[],[f85]) ).
cnf(s4,plain,
( spl20_1
| spl20_6 ),
inference(sat_conversion,[],[f89]) ).
cnf(s5,plain,
( spl20_2
| spl20_7 ),
inference(sat_conversion,[],[f93]) ).
cnf(s8,plain,
( ~ spl20_2
| spl20_9 ),
inference(sat_conversion,[],[f157]) ).
cnf(s10,plain,
( ~ spl20_2
| ~ spl20_4
| ~ spl20_9
| ~ spl20_10 ),
inference(sat_conversion,[],[f208]) ).
cnf(s12,plain,
( ~ spl20_2
| ~ spl20_6 ),
inference(sat_conversion,[],[f240]) ).
cnf(s16,plain,
( ~ spl20_2
| spl20_16 ),
inference(sat_conversion,[],[f256]) ).
cnf(s19,plain,
( ~ spl20_2
| spl20_19 ),
inference(sat_conversion,[],[f271]) ).
cnf(s23,plain,
( ~ spl20_1
| ~ spl20_7 ),
inference(sat_conversion,[],[f301]) ).
cnf(s24,plain,
( ~ spl20_2
| spl20_10 ),
inference(sat_conversion,[],[f312]) ).
cnf(s25,plain,
( ~ spl20_2
| ~ spl20_5
| ~ spl20_10
| ~ spl20_16
| ~ spl20_19 ),
inference(sat_conversion,[],[f321]) ).
cnf(s26,plain,
spl20_1,
inference(rat,[],[s12,s1,s4]) ).
cnf(s27,plain,
~ spl20_7,
inference(rat,[],[s23,s26]) ).
cnf(s32,plain,
spl20_2,
inference(rat,[],[s5,s27]) ).
cnf(s33,plain,
spl20_10,
inference(rat,[],[s24,s32]) ).
cnf(s35,plain,
spl20_19,
inference(rat,[],[s19,s32]) ).
cnf(s38,plain,
spl20_16,
inference(rat,[],[s16,s32]) ).
cnf(s41,plain,
spl20_9,
inference(rat,[],[s8,s32]) ).
cnf(s42,plain,
~ spl20_5,
inference(rat,[],[s25,s35,s38,s33,s32]) ).
cnf(s43,plain,
~ spl20_4,
inference(rat,[],[s10,s33,s32,s41]) ).
cnf(s44,plain,
~ spl20_3,
inference(rat,[],[s3,s42]) ).
cnf(s45,plain,
$false,
inference(rat,[],[s2,s43,s44]) ).
fof(f322,plain,
$false,
inference(avatar_sat_refutation,[],[s45]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NLP001+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n001.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:52:01 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.42 Running first-order theorem proving
% 0.11/0.42 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.42/1.23 % (3833929)Detected formulas, will run a generic FOF schedule.
% 2.42/1.23 % (3834038)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1295008602:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.42/1.23 % (3834038)First to succeed.
% 2.42/1.23 % (3834038)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3833929"
% 2.42/1.23 % (3834040)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4028564228:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.42/1.23 % (3834037)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=829113892:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.42/1.23 % (3834035)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=2445746558:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.42/1.23 % (3834041)dis-21_1_sil=8000:lcm=predicate:random_seed=1941437209: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.42/1.23 % (3834036)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=3270999638:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.42/1.23 % (3834041)Also succeeded, but the first one will report.
% 2.42/1.23 % (3834040)Also succeeded, but the first one will report.
% 2.42/1.23 % (3834039)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1958441630:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.42/1.23 % (3834039)Also succeeded, but the first one will report.
% 2.42/1.23 % (3834038)Refutation found. Thanks to Tanya!
% 2.42/1.23 % SZS status Theorem for theBenchmark
% 2.42/1.23 % SZS output start Proof for theBenchmark
% See solution above
% 3.05/1.47 % (3834038)------------------------------
% 3.05/1.47 % (3834038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.05/1.47 % (3834038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.05/1.47 % (3834038)CaDiCaL version: 2.1.3
% 3.05/1.47 % (3834038)Termination reason: Refutation
% 3.05/1.47 % (3834038)Time elapsed: 0.005 s
% 3.05/1.47 % (3834038)Peak memory usage: 89 MB
% 3.05/1.47 % (3834038)Instructions burned: 10 (million)
% 3.05/1.47 % (3834038)------------------------------
% 3.05/1.47 % (3834038)------------------------------
% 3.05/1.47 % (3833929)Success in time 0.341 s
% 3.05/1.47 % Vampire exiting
%------------------------------------------------------------------------------