%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : NLP001+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n015.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 : Fri Sep 25 02:16:09 PM UTC 2026
% Result : Theorem 2.17s 6.29s
% Output : CNFRefutation 2.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 3
% Syntax : Number of formulae : 100 ( 3 unt; 2 def)
% Number of atoms : 772 ( 0 equ)
% Maximal formula atoms : 56 ( 7 avg)
% Number of connectives : 964 ( 363 ~; 368 |; 229 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 37 ( 7 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 22 ( 21 usr; 8 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 126 ( 0 sgn 66 !; 60 ?; 30 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
( ( ? [X8,X9,X10,X11] :
( in(X9,X8)
& down(X9,X11)
& barrel(X9,X10)
& lonely(X11)
& way(X11)
& street(X11)
& old(X10)
& dirty(X10)
& white(X10)
& car(X10)
& chevy(X10)
& event(X9)
& city(X8)
& hollywood(X8) )
=> ? [X12,X13,X14,X15] :
( in(X13,X12)
& down(X13,X14)
& barrel(X13,X15)
& old(X15)
& dirty(X15)
& white(X15)
& car(X15)
& chevy(X15)
& lonely(X14)
& way(X14)
& street(X14)
& event(X13)
& city(X12)
& hollywood(X12) ) )
& ( ? [X0,X1,X2,X3] :
( in(X1,X0)
& down(X1,X2)
& barrel(X1,X3)
& old(X3)
& dirty(X3)
& white(X3)
& car(X3)
& chevy(X3)
& lonely(X2)
& way(X2)
& street(X2)
& event(X1)
& city(X0)
& hollywood(X0) )
=> ? [X4,X5,X6,X7] :
( in(X5,X4)
& down(X5,X7)
& barrel(X5,X6)
& lonely(X7)
& way(X7)
& street(X7)
& old(X6)
& dirty(X6)
& white(X6)
& car(X6)
& chevy(X6)
& event(X5)
& city(X4)
& hollywood(X4) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f2,negated_conjecture,
~ ( ( ? [X8,X9,X10,X11] :
( in(X9,X8)
& down(X9,X11)
& barrel(X9,X10)
& lonely(X11)
& way(X11)
& street(X11)
& old(X10)
& dirty(X10)
& white(X10)
& car(X10)
& chevy(X10)
& event(X9)
& city(X8)
& hollywood(X8) )
=> ? [X12,X13,X14,X15] :
( in(X13,X12)
& down(X13,X14)
& barrel(X13,X15)
& old(X15)
& dirty(X15)
& white(X15)
& car(X15)
& chevy(X15)
& lonely(X14)
& way(X14)
& street(X14)
& event(X13)
& city(X12)
& hollywood(X12) ) )
& ( ? [X0,X1,X2,X3] :
( in(X1,X0)
& down(X1,X2)
& barrel(X1,X3)
& old(X3)
& dirty(X3)
& white(X3)
& car(X3)
& chevy(X3)
& lonely(X2)
& way(X2)
& street(X2)
& event(X1)
& city(X0)
& hollywood(X0) )
=> ? [X4,X5,X6,X7] :
( in(X5,X4)
& down(X5,X7)
& barrel(X5,X6)
& lonely(X7)
& way(X7)
& street(X7)
& old(X6)
& dirty(X6)
& white(X6)
& car(X6)
& chevy(X6)
& event(X5)
& city(X4)
& hollywood(X4) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
( ( ? [X8,X9,X10,X11] :
( in(X9,X8)
& down(X9,X11)
& barrel(X9,X10)
& lonely(X11)
& way(X11)
& street(X11)
& old(X10)
& dirty(X10)
& white(X10)
& car(X10)
& chevy(X10)
& event(X9)
& city(X8)
& hollywood(X8) )
& ! [X12,X13,X14,X15] :
( ~ in(X13,X12)
| ~ down(X13,X14)
| ~ barrel(X13,X15)
| ~ old(X15)
| ~ dirty(X15)
| ~ white(X15)
| ~ car(X15)
| ~ chevy(X15)
| ~ lonely(X14)
| ~ way(X14)
| ~ street(X14)
| ~ event(X13)
| ~ city(X12)
| ~ hollywood(X12) ) )
| ( ? [X0,X1,X2,X3] :
( in(X1,X0)
& down(X1,X2)
& barrel(X1,X3)
& old(X3)
& dirty(X3)
& white(X3)
& car(X3)
& chevy(X3)
& lonely(X2)
& way(X2)
& street(X2)
& event(X1)
& city(X0)
& hollywood(X0) )
& ! [X4,X5,X6,X7] :
( ~ in(X5,X4)
| ~ down(X5,X7)
| ~ barrel(X5,X6)
| ~ lonely(X7)
| ~ way(X7)
| ~ street(X7)
| ~ old(X6)
| ~ dirty(X6)
| ~ white(X6)
| ~ car(X6)
| ~ chevy(X6)
| ~ event(X5)
| ~ city(X4)
| ~ hollywood(X4) ) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f7,plain,
( ~ sP1
| ? [X0,X1,X2,X3] :
( in(X1,X0)
& down(X1,X2)
& barrel(X1,X3)
& old(X3)
& dirty(X3)
& white(X3)
& car(X3)
& chevy(X3)
& lonely(X2)
& way(X2)
& street(X2)
& event(X1)
& city(X0)
& hollywood(X0) ) ),
inference(nnf_transformation,[],[f5]) ).
fof(f8,plain,
( ~ sP1
| ( in(sK3,sK2)
& down(sK3,sK4)
& barrel(sK3,sK5)
& old(sK5)
& dirty(sK5)
& white(sK5)
& car(sK5)
& chevy(sK5)
& lonely(sK4)
& way(sK4)
& street(sK4)
& event(sK3)
& city(sK2)
& hollywood(sK2) ) ),
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(f12,plain,
( ( sP0
& ! [X4,X5,X6,X7] :
( ~ in(X5,X4)
| ~ down(X5,X6)
| ~ barrel(X5,X7)
| ~ old(X7)
| ~ dirty(X7)
| ~ white(X7)
| ~ car(X7)
| ~ chevy(X7)
| ~ lonely(X6)
| ~ way(X6)
| ~ street(X6)
| ~ event(X5)
| ~ city(X4)
| ~ hollywood(X4) ) )
| ( sP1
& ! [X0,X1,X2,X3] :
( ~ in(X1,X0)
| ~ down(X1,X3)
| ~ barrel(X1,X2)
| ~ lonely(X3)
| ~ way(X3)
| ~ street(X3)
| ~ old(X2)
| ~ dirty(X2)
| ~ white(X2)
| ~ car(X2)
| ~ chevy(X2)
| ~ event(X1)
| ~ city(X0)
| ~ hollywood(X0) ) ) ),
inference(rectify,[],[f6]) ).
fof(f13,plain,
( ~ sP1
| in(sK3,sK2) ),
inference(cnf_transformation,[],[f8]) ).
fof(f14,plain,
( ~ sP1
| down(sK3,sK4) ),
inference(cnf_transformation,[],[f8]) ).
fof(f15,plain,
( ~ sP1
| barrel(sK3,sK5) ),
inference(cnf_transformation,[],[f8]) ).
fof(f16,plain,
( ~ sP1
| old(sK5) ),
inference(cnf_transformation,[],[f8]) ).
fof(f17,plain,
( ~ sP1
| dirty(sK5) ),
inference(cnf_transformation,[],[f8]) ).
fof(f18,plain,
( ~ sP1
| white(sK5) ),
inference(cnf_transformation,[],[f8]) ).
fof(f19,plain,
( ~ sP1
| car(sK5) ),
inference(cnf_transformation,[],[f8]) ).
fof(f20,plain,
( ~ sP1
| chevy(sK5) ),
inference(cnf_transformation,[],[f8]) ).
fof(f21,plain,
( ~ sP1
| lonely(sK4) ),
inference(cnf_transformation,[],[f8]) ).
fof(f22,plain,
( ~ sP1
| way(sK4) ),
inference(cnf_transformation,[],[f8]) ).
fof(f23,plain,
( ~ sP1
| street(sK4) ),
inference(cnf_transformation,[],[f8]) ).
fof(f24,plain,
( ~ sP1
| event(sK3) ),
inference(cnf_transformation,[],[f8]) ).
fof(f25,plain,
( ~ sP1
| city(sK2) ),
inference(cnf_transformation,[],[f8]) ).
fof(f26,plain,
( ~ sP1
| hollywood(sK2) ),
inference(cnf_transformation,[],[f8]) ).
fof(f41,plain,
( sP0
| sP1 ),
inference(cnf_transformation,[],[f12]) ).
fof(f42,plain,
! [X6,X7,X4,X5] :
( ~ in(X5,X4)
| ~ down(X5,X6)
| ~ barrel(X5,X7)
| ~ old(X7)
| ~ dirty(X7)
| ~ white(X7)
| ~ car(X7)
| ~ chevy(X7)
| ~ lonely(X6)
| ~ way(X6)
| ~ street(X6)
| ~ event(X5)
| ~ city(X4)
| ~ hollywood(X4)
| sP1 ),
inference(cnf_transformation,[],[f12]) ).
fof(f44,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ in(X5,X4)
| ~ down(X5,X6)
| ~ barrel(X5,X7)
| ~ old(X7)
| ~ dirty(X7)
| ~ white(X7)
| ~ car(X7)
| ~ chevy(X7)
| ~ lonely(X6)
| ~ way(X6)
| ~ street(X6)
| ~ event(X5)
| ~ city(X4)
| ~ hollywood(X4)
| ~ in(X1,X0)
| ~ down(X1,X3)
| ~ barrel(X1,X2)
| ~ lonely(X3)
| ~ way(X3)
| ~ street(X3)
| ~ old(X2)
| ~ dirty(X2)
| ~ white(X2)
| ~ car(X2)
| ~ chevy(X2)
| ~ event(X1)
| ~ city(X0)
| ~ hollywood(X0) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_49,plain,
( hollywood(sK2)
| ~ sP1 ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_50,plain,
( city(sK2)
| ~ sP1 ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_51,plain,
( event(sK3)
| ~ sP1 ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_52,plain,
( street(sK4)
| ~ sP1 ),
inference(cnf_transformation,[],[f23]) ).
tcf(c_53,plain,
( way(sK4)
| ~ sP1 ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_54,plain,
( lonely(sK4)
| ~ sP1 ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_55,plain,
( chevy(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_56,plain,
( car(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f19]) ).
tcf(c_57,plain,
( white(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_58,plain,
( dirty(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f17]) ).
tcf(c_59,plain,
( old(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_60,plain,
( barrel(sK3,sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_61,plain,
( down(sK3,sK4)
| ~ sP1 ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_62,plain,
( in(sK3,sK2)
| ~ sP1 ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_77,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( ~ old(X3)
| ~ old(X1)
| ~ dirty(X3)
| ~ dirty(X1)
| ~ white(X3)
| ~ white(X1)
| ~ car(X3)
| ~ car(X1)
| ~ chevy(X3)
| ~ chevy(X1)
| ~ lonely(X5)
| ~ lonely(X4)
| ~ way(X5)
| ~ way(X4)
| ~ street(X5)
| ~ street(X4)
| ~ event(X2)
| ~ event(X0)
| ~ city(X7)
| ~ city(X6)
| ~ hollywood(X7)
| ~ hollywood(X6)
| ~ in(X2,X7)
| ~ in(X0,X6)
| ~ down(X2,X5)
| ~ down(X0,X4)
| ~ barrel(X2,X3)
| ~ barrel(X0,X1) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_79,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP1
| ~ old(X1)
| ~ dirty(X1)
| ~ white(X1)
| ~ car(X1)
| ~ chevy(X1)
| ~ lonely(X2)
| ~ way(X2)
| ~ street(X2)
| ~ event(X0)
| ~ city(X3)
| ~ hollywood(X3)
| ~ in(X0,X3)
| ~ down(X0,X2)
| ~ barrel(X0,X1) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_80,negated_conjecture,
( sP0
| sP1 ),
inference(cnf_transformation,[],[f41]) ).
tcf(c_1873,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ iPr_def_10
| ~ hollywood(X1)
| ~ city(X1)
| ~ event(X0)
| ~ street(X2)
| ~ way(X2)
| ~ lonely(X2)
| ~ chevy(X3)
| ~ car(X3)
| ~ white(X3)
| ~ dirty(X3)
| ~ old(X3)
| ~ barrel(X0,X3)
| ~ down(X0,X2)
| ~ in(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_77]) ).
tcf(c_1874,negated_conjecture,
iPr_def_10,
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_77]) ).
tcf(c_1876,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP1
| ~ old(X1)
| ~ dirty(X1)
| ~ white(X1)
| ~ car(X1)
| ~ chevy(X1)
| ~ lonely(X2)
| ~ way(X2)
| ~ street(X2)
| ~ event(X0)
| ~ city(X3)
| ~ hollywood(X3)
| ~ in(X0,X3)
| ~ down(X0,X2)
| ~ barrel(X0,X1) ),
inference(demodulation,[status(thm)],[c_79]) ).
tcf(c_1878,negated_conjecture,
iPr_def_10,
inference(demodulation,[status(thm)],[c_1874]) ).
tcf(c_1880,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ iPr_def_10
| ~ old(X1)
| ~ dirty(X1)
| ~ white(X1)
| ~ car(X1)
| ~ chevy(X1)
| ~ lonely(X2)
| ~ way(X2)
| ~ street(X2)
| ~ event(X0)
| ~ city(X3)
| ~ hollywood(X3)
| ~ in(X0,X3)
| ~ down(X0,X2)
| ~ barrel(X0,X1) ),
inference(demodulation,[status(thm)],[c_1873]) ).
tcf(c_1882,plain,
! [X0: $i,X1: $i] :
( sP1
| ~ event(sK7)
| ~ city(sK6)
| ~ hollywood(sK6)
| ~ old(X0)
| ~ dirty(X0)
| ~ white(X0)
| ~ car(X0)
| ~ chevy(X0)
| ~ lonely(X1)
| ~ way(X1)
| ~ street(X1)
| ~ in(sK7,sK6)
| ~ down(sK7,X1)
| ~ barrel(sK7,X0) ),
inference(instantiation,[status(thm)],[c_1876]) ).
tcf(c_1887,plain,
! [X0: $i] :
( sP1
| ~ old(sK8)
| ~ dirty(sK8)
| ~ white(sK8)
| ~ car(sK8)
| ~ chevy(sK8)
| ~ event(sK7)
| ~ city(sK6)
| ~ hollywood(sK6)
| ~ lonely(X0)
| ~ way(X0)
| ~ street(X0)
| ~ in(sK7,sK6)
| ~ barrel(sK7,sK8)
| ~ down(sK7,X0) ),
inference(instantiation,[status(thm)],[c_1882]) ).
tcf(c_1890,plain,
( sP1
| ~ old(sK8)
| ~ dirty(sK8)
| ~ white(sK8)
| ~ car(sK8)
| ~ chevy(sK8)
| ~ lonely(sK9)
| ~ way(sK9)
| ~ street(sK9)
| ~ event(sK7)
| ~ city(sK6)
| ~ hollywood(sK6)
| ~ in(sK7,sK6)
| ~ down(sK7,sK9)
| ~ barrel(sK7,sK8) ),
inference(instantiation,[status(thm)],[c_1887]) ).
tcf(c_1895,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_10
| ~ event(sK3)
| ~ city(sK2)
| ~ hollywood(sK2)
| ~ old(X0)
| ~ dirty(X0)
| ~ white(X0)
| ~ car(X0)
| ~ chevy(X0)
| ~ lonely(X1)
| ~ way(X1)
| ~ street(X1)
| ~ in(sK3,sK2)
| ~ down(sK3,X1)
| ~ barrel(sK3,X0) ),
inference(instantiation,[status(thm)],[c_1880]) ).
tcf(c_1899,plain,
! [X0: $i] :
( ~ iPr_def_10
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ event(sK3)
| ~ city(sK2)
| ~ hollywood(sK2)
| ~ old(X0)
| ~ dirty(X0)
| ~ white(X0)
| ~ car(X0)
| ~ chevy(X0)
| ~ in(sK3,sK2)
| ~ down(sK3,sK4)
| ~ barrel(sK3,X0) ),
inference(instantiation,[status(thm)],[c_1895]) ).
tcf(c_1900,plain,
( ~ iPr_def_10
| ~ old(sK5)
| ~ dirty(sK5)
| ~ white(sK5)
| ~ car(sK5)
| ~ chevy(sK5)
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ event(sK3)
| ~ city(sK2)
| ~ hollywood(sK2)
| ~ in(sK3,sK2)
| ~ down(sK3,sK4)
| ~ barrel(sK3,sK5) ),
inference(instantiation,[status(thm)],[c_1899]) ).
fof(f4,definition,
( ~ sP0
| ? [X8,X9,X10,X11] :
( in(X9,X8)
& down(X9,X11)
& barrel(X9,X10)
& lonely(X11)
& way(X11)
& street(X11)
& old(X10)
& dirty(X10)
& white(X10)
& car(X10)
& chevy(X10)
& event(X9)
& city(X8)
& hollywood(X8) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f5,definition,
( ~ sP1
| ? [X0,X1,X2,X3] :
( in(X1,X0)
& down(X1,X2)
& barrel(X1,X3)
& old(X3)
& dirty(X3)
& white(X3)
& car(X3)
& chevy(X3)
& lonely(X2)
& way(X2)
& street(X2)
& event(X1)
& city(X0)
& hollywood(X0) ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f6,plain,
( ( sP0
& ! [X12,X13,X14,X15] :
( ~ in(X13,X12)
| ~ down(X13,X14)
| ~ barrel(X13,X15)
| ~ old(X15)
| ~ dirty(X15)
| ~ white(X15)
| ~ car(X15)
| ~ chevy(X15)
| ~ lonely(X14)
| ~ way(X14)
| ~ street(X14)
| ~ event(X13)
| ~ city(X12)
| ~ hollywood(X12) ) )
| ( sP1
& ! [X4,X5,X6,X7] :
( ~ in(X5,X4)
| ~ down(X5,X7)
| ~ barrel(X5,X6)
| ~ lonely(X7)
| ~ way(X7)
| ~ street(X7)
| ~ old(X6)
| ~ dirty(X6)
| ~ white(X6)
| ~ car(X6)
| ~ chevy(X6)
| ~ event(X5)
| ~ city(X4)
| ~ hollywood(X4) ) ) ),
inference(definition_folding,[],[f3,f5,f4]) ).
fof(f9,plain,
( ~ sP0
| ? [X8,X9,X10,X11] :
( in(X9,X8)
& down(X9,X11)
& barrel(X9,X10)
& lonely(X11)
& way(X11)
& street(X11)
& old(X10)
& dirty(X10)
& white(X10)
& car(X10)
& chevy(X10)
& event(X9)
& city(X8)
& hollywood(X8) ) ),
inference(nnf_transformation,[],[f4]) ).
fof(f10,plain,
( ~ sP0
| ? [X0,X1,X2,X3] :
( in(X1,X0)
& down(X1,X3)
& barrel(X1,X2)
& lonely(X3)
& way(X3)
& street(X3)
& old(X2)
& dirty(X2)
& white(X2)
& car(X2)
& chevy(X2)
& event(X1)
& city(X0)
& hollywood(X0) ) ),
inference(rectify,[],[f9]) ).
fof(f11,plain,
( ~ sP0
| ( in(sK7,sK6)
& down(sK7,sK9)
& barrel(sK7,sK8)
& lonely(sK9)
& way(sK9)
& street(sK9)
& old(sK8)
& dirty(sK8)
& white(sK8)
& car(sK8)
& chevy(sK8)
& event(sK7)
& city(sK6)
& hollywood(sK6) ) ),
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(f27,plain,
( ~ sP0
| in(sK7,sK6) ),
inference(cnf_transformation,[],[f11]) ).
fof(f28,plain,
( ~ sP0
| down(sK7,sK9) ),
inference(cnf_transformation,[],[f11]) ).
fof(f29,plain,
( ~ sP0
| barrel(sK7,sK8) ),
inference(cnf_transformation,[],[f11]) ).
fof(f30,plain,
( ~ sP0
| lonely(sK9) ),
inference(cnf_transformation,[],[f11]) ).
fof(f31,plain,
( ~ sP0
| way(sK9) ),
inference(cnf_transformation,[],[f11]) ).
fof(f32,plain,
( ~ sP0
| street(sK9) ),
inference(cnf_transformation,[],[f11]) ).
fof(f33,plain,
( ~ sP0
| old(sK8) ),
inference(cnf_transformation,[],[f11]) ).
fof(f34,plain,
( ~ sP0
| dirty(sK8) ),
inference(cnf_transformation,[],[f11]) ).
fof(f35,plain,
( ~ sP0
| white(sK8) ),
inference(cnf_transformation,[],[f11]) ).
fof(f36,plain,
( ~ sP0
| car(sK8) ),
inference(cnf_transformation,[],[f11]) ).
fof(f37,plain,
( ~ sP0
| chevy(sK8) ),
inference(cnf_transformation,[],[f11]) ).
fof(f38,plain,
( ~ sP0
| event(sK7) ),
inference(cnf_transformation,[],[f11]) ).
fof(f39,plain,
( ~ sP0
| city(sK6) ),
inference(cnf_transformation,[],[f11]) ).
fof(f40,plain,
( ~ sP0
| hollywood(sK6) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_63,plain,
( hollywood(sK6)
| ~ sP0 ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_64,plain,
( city(sK6)
| ~ sP0 ),
inference(cnf_transformation,[],[f39]) ).
tcf(c_65,plain,
( event(sK7)
| ~ sP0 ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_66,plain,
( chevy(sK8)
| ~ sP0 ),
inference(cnf_transformation,[],[f37]) ).
tcf(c_67,plain,
( car(sK8)
| ~ sP0 ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_68,plain,
( white(sK8)
| ~ sP0 ),
inference(cnf_transformation,[],[f35]) ).
tcf(c_69,plain,
( dirty(sK8)
| ~ sP0 ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_70,plain,
( old(sK8)
| ~ sP0 ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_71,plain,
( street(sK9)
| ~ sP0 ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_72,plain,
( way(sK9)
| ~ sP0 ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_73,plain,
( lonely(sK9)
| ~ sP0 ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_74,plain,
( barrel(sK7,sK8)
| ~ sP0 ),
inference(cnf_transformation,[],[f29]) ).
tcf(c_75,plain,
( down(sK7,sK9)
| ~ sP0 ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_76,plain,
( in(sK7,sK6)
| ~ sP0 ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_1089,plain,
( sP1
| in(sK7,sK6) ),
inference(resolution,[status(thm)],[c_80,c_76]) ).
tcf(c_1096,plain,
( sP1
| down(sK7,sK9) ),
inference(resolution,[status(thm)],[c_80,c_75]) ).
tcf(c_1103,plain,
( sP1
| barrel(sK7,sK8) ),
inference(resolution,[status(thm)],[c_80,c_74]) ).
tcf(c_1110,plain,
( sP1
| lonely(sK9) ),
inference(resolution,[status(thm)],[c_80,c_73]) ).
tcf(c_1117,plain,
( sP1
| way(sK9) ),
inference(resolution,[status(thm)],[c_80,c_72]) ).
tcf(c_1124,plain,
( sP1
| street(sK9) ),
inference(resolution,[status(thm)],[c_80,c_71]) ).
tcf(c_1131,plain,
( sP1
| old(sK8) ),
inference(resolution,[status(thm)],[c_80,c_70]) ).
tcf(c_1138,plain,
( sP1
| dirty(sK8) ),
inference(resolution,[status(thm)],[c_80,c_69]) ).
tcf(c_1145,plain,
( sP1
| white(sK8) ),
inference(resolution,[status(thm)],[c_80,c_68]) ).
tcf(c_1152,plain,
( sP1
| car(sK8) ),
inference(resolution,[status(thm)],[c_80,c_67]) ).
tcf(c_1159,plain,
( sP1
| chevy(sK8) ),
inference(resolution,[status(thm)],[c_80,c_66]) ).
tcf(c_1166,plain,
( sP1
| event(sK7) ),
inference(resolution,[status(thm)],[c_80,c_65]) ).
tcf(c_1173,plain,
( sP1
| city(sK6) ),
inference(resolution,[status(thm)],[c_80,c_64]) ).
tcf(c_1180,plain,
( sP1
| hollywood(sK6) ),
inference(resolution,[status(thm)],[c_80,c_63]) ).
tcf(c_1901,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_1900,c_1890,c_1878,c_1180,c_1173,c_1166,c_1159,c_1152,c_1145,c_1138,c_1131,c_1124,c_1117,c_1110,c_1103,c_1096,c_1089,c_60,c_61,c_62,c_49,c_50,c_51,c_52,c_53,c_54,c_55,c_56,c_57,c_58,c_59]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP001+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/5.38 % Computer : n015.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Thu Sep 24 01:39:03 UTC 2026
% 0.11/5.38 % CPUTime :
% 0.11/5.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.14/5.42 Running first-order theorem proving
% 0.14/5.42 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/5.43
% 0.14/5.43 % ======== iProver multi-core TPTP/SMT =========
% 0.14/5.43
% 0.14/5.43 % Detected problem language: tptp
% 0.14/5.44 % Proving...
% 2.17/6.29 % SZS status Started for theBenchmark.p
% 2.17/6.29 % SZS status Theorem for theBenchmark.p
% 2.17/6.29
% 2.17/6.29 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.17/6.29
% 2.17/6.29 % ------ iProver source info
% 2.17/6.29
% 2.17/6.29 % git: date: 2026-07-19 20:42:38 +0200
% 2.17/6.29 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.17/6.29 % git: non_committed_changes: false
% 2.17/6.29
% 2.17/6.29 % ------ Parsing...
% 2.17/6.29 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Option_epr_non_horn_non_eq
% 2.17/6.29 %
% 2.17/6.29
% 2.17/6.29 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e %
% 2.17/6.29
% 2.17/6.29 % ------ Preprocessing...% ------ preprocesses with Option_epr_non_horn_non_eq
% 2.17/6.29 gs_s sp: 2 0s gs_e snvd_s sp: 0 0s snvd_e
% 2.17/6.29 % ------ Proving...
% 2.17/6.29 % ------ Problem Properties
% 2.17/6.29
% 2.17/6.29 %
% 2.17/6.29 % clauses 33
% 2.17/6.29 % conjectures 5
% 2.17/6.29 % EPR 33
% 2.17/6.29 % Horn 32
% 2.17/6.29 % unary 1
% 2.17/6.29 % binary 29
% 2.17/6.29 % lits 104
% 2.17/6.29 % lits eq 0
% 2.17/6.29 % fd_pure 0
% 2.17/6.29 % fd_pseudo 0
% 2.17/6.29 % fd_cond 0
% 2.17/6.29 % fd_pseudo_cond 0
% 2.17/6.29 % AC symbols 0
% 2.17/6.29
% 2.17/6.29 % ------ Schedule EPR non Horn non eq is on
% 2.17/6.29
% 2.17/6.29 % ------ no equalities: superposition off
% 2.17/6.29
% 2.17/6.29 % ------ Input Options "--resolution_flag false" Time Limit: 70.
% 2.17/6.29
% 2.17/6.29
% 2.17/6.29 % ------
% 2.17/6.29 % Current options:
% 2.17/6.29 % ------
% 2.17/6.29
% 2.17/6.29
% 2.17/6.29 %
% 2.17/6.29
% 2.17/6.29 % ------ Proving...
% 2.17/6.29 %
% 2.17/6.29
% 2.17/6.29 % SZS status Theorem for theBenchmark.p
% 2.17/6.29
% 2.17/6.29 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 2.17/6.29
% 2.17/6.29
%------------------------------------------------------------------------------