%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : NLP009+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 : 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 : Fri Sep 25 02:16:12 PM UTC 2026
% Result : Theorem 0.54s 0.96s
% Output : CNFRefutation 0.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 4
% Syntax : Number of formulae : 193 ( 1 unt; 2 def)
% Number of atoms : 1715 ( 128 equ)
% Maximal formula atoms : 112 ( 8 avg)
% Number of connectives : 2277 ( 900 ~; 906 |; 467 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 75 ( 9 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 : 39 ( 37 usr; 18 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 9 con; 0-0 aty)
% Number of variables : 335 ( 0 sgn 200 !; 135 ?; 66 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
( ( ? [X18,X19,X20,X21,X22,X23,X24,X25,X26] :
( in(X26,X24)
& X23 = X26
& in(X25,X24)
& X22 = X25
& young(X23)
& man(X23)
& fellow(X23)
& young(X22)
& man(X22)
& fellow(X22)
& X22 != X23
& front(X24)
& furniture(X24)
& seat(X24)
& in(X19,X18)
& down(X19,X21)
& barrel(X19,X20)
& lonely(X21)
& way(X21)
& street(X21)
& old(X20)
& dirty(X20)
& white(X20)
& car(X20)
& chevy(X20)
& event(X19)
& city(X18)
& hollywood(X18) )
=> ? [X27,X28,X29,X30,X31,X32,X33,X34,X35] :
( in(X35,X33)
& X32 = X35
& in(X34,X33)
& X31 = X34
& young(X32)
& man(X32)
& fellow(X32)
& young(X31)
& man(X31)
& fellow(X31)
& X31 != X32
& front(X33)
& furniture(X33)
& seat(X33)
& in(X28,X27)
& down(X28,X29)
& barrel(X28,X30)
& old(X30)
& dirty(X30)
& white(X30)
& car(X30)
& chevy(X30)
& lonely(X29)
& way(X29)
& street(X29)
& event(X28)
& city(X27)
& hollywood(X27) ) )
& ( ? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( in(X8,X6)
& X5 = X8
& in(X7,X6)
& X4 = X7
& young(X5)
& man(X5)
& fellow(X5)
& young(X4)
& man(X4)
& fellow(X4)
& X4 != X5
& front(X6)
& furniture(X6)
& seat(X6)
& 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) )
=> ? [X9,X10,X11,X12,X13,X14,X15,X16,X17] :
( in(X17,X15)
& X14 = X17
& in(X16,X15)
& X13 = X16
& young(X14)
& man(X14)
& fellow(X14)
& young(X13)
& man(X13)
& fellow(X13)
& X13 != X14
& front(X15)
& furniture(X15)
& seat(X15)
& in(X10,X9)
& down(X10,X12)
& barrel(X10,X11)
& lonely(X12)
& way(X12)
& street(X12)
& old(X11)
& dirty(X11)
& white(X11)
& car(X11)
& chevy(X11)
& event(X10)
& city(X9)
& hollywood(X9) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f2,negated_conjecture,
~ ( ( ? [X18,X19,X20,X21,X22,X23,X24,X25,X26] :
( in(X26,X24)
& X23 = X26
& in(X25,X24)
& X22 = X25
& young(X23)
& man(X23)
& fellow(X23)
& young(X22)
& man(X22)
& fellow(X22)
& X22 != X23
& front(X24)
& furniture(X24)
& seat(X24)
& in(X19,X18)
& down(X19,X21)
& barrel(X19,X20)
& lonely(X21)
& way(X21)
& street(X21)
& old(X20)
& dirty(X20)
& white(X20)
& car(X20)
& chevy(X20)
& event(X19)
& city(X18)
& hollywood(X18) )
=> ? [X27,X28,X29,X30,X31,X32,X33,X34,X35] :
( in(X35,X33)
& X32 = X35
& in(X34,X33)
& X31 = X34
& young(X32)
& man(X32)
& fellow(X32)
& young(X31)
& man(X31)
& fellow(X31)
& X31 != X32
& front(X33)
& furniture(X33)
& seat(X33)
& in(X28,X27)
& down(X28,X29)
& barrel(X28,X30)
& old(X30)
& dirty(X30)
& white(X30)
& car(X30)
& chevy(X30)
& lonely(X29)
& way(X29)
& street(X29)
& event(X28)
& city(X27)
& hollywood(X27) ) )
& ( ? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( in(X8,X6)
& X5 = X8
& in(X7,X6)
& X4 = X7
& young(X5)
& man(X5)
& fellow(X5)
& young(X4)
& man(X4)
& fellow(X4)
& X4 != X5
& front(X6)
& furniture(X6)
& seat(X6)
& 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) )
=> ? [X9,X10,X11,X12,X13,X14,X15,X16,X17] :
( in(X17,X15)
& X14 = X17
& in(X16,X15)
& X13 = X16
& young(X14)
& man(X14)
& fellow(X14)
& young(X13)
& man(X13)
& fellow(X13)
& X13 != X14
& front(X15)
& furniture(X15)
& seat(X15)
& in(X10,X9)
& down(X10,X12)
& barrel(X10,X11)
& lonely(X12)
& way(X12)
& street(X12)
& old(X11)
& dirty(X11)
& white(X11)
& car(X11)
& chevy(X11)
& event(X10)
& city(X9)
& hollywood(X9) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
( ( ? [X18,X19,X20,X21,X22,X23,X24,X25,X26] :
( in(X26,X24)
& X23 = X26
& in(X25,X24)
& X22 = X25
& young(X23)
& man(X23)
& fellow(X23)
& young(X22)
& man(X22)
& fellow(X22)
& X22 != X23
& front(X24)
& furniture(X24)
& seat(X24)
& in(X19,X18)
& down(X19,X21)
& barrel(X19,X20)
& lonely(X21)
& way(X21)
& street(X21)
& old(X20)
& dirty(X20)
& white(X20)
& car(X20)
& chevy(X20)
& event(X19)
& city(X18)
& hollywood(X18) )
& ! [X27,X28,X29,X30,X31,X32,X33,X34,X35] :
( ~ in(X35,X33)
| X32 != X35
| ~ in(X34,X33)
| X31 != X34
| ~ young(X32)
| ~ man(X32)
| ~ fellow(X32)
| ~ young(X31)
| ~ man(X31)
| ~ fellow(X31)
| X31 = X32
| ~ front(X33)
| ~ furniture(X33)
| ~ seat(X33)
| ~ in(X28,X27)
| ~ down(X28,X29)
| ~ barrel(X28,X30)
| ~ old(X30)
| ~ dirty(X30)
| ~ white(X30)
| ~ car(X30)
| ~ chevy(X30)
| ~ lonely(X29)
| ~ way(X29)
| ~ street(X29)
| ~ event(X28)
| ~ city(X27)
| ~ hollywood(X27) ) )
| ( ? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( in(X8,X6)
& X5 = X8
& in(X7,X6)
& X4 = X7
& young(X5)
& man(X5)
& fellow(X5)
& young(X4)
& man(X4)
& fellow(X4)
& X4 != X5
& front(X6)
& furniture(X6)
& seat(X6)
& 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) )
& ! [X9,X10,X11,X12,X13,X14,X15,X16,X17] :
( ~ in(X17,X15)
| X14 != X17
| ~ in(X16,X15)
| X13 != X16
| ~ young(X14)
| ~ man(X14)
| ~ fellow(X14)
| ~ young(X13)
| ~ man(X13)
| ~ fellow(X13)
| X13 = X14
| ~ front(X15)
| ~ furniture(X15)
| ~ seat(X15)
| ~ in(X10,X9)
| ~ down(X10,X12)
| ~ barrel(X10,X11)
| ~ lonely(X12)
| ~ way(X12)
| ~ street(X12)
| ~ old(X11)
| ~ dirty(X11)
| ~ white(X11)
| ~ car(X11)
| ~ chevy(X11)
| ~ event(X10)
| ~ city(X9)
| ~ hollywood(X9) ) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f7,plain,
( ~ sP1
| ? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( in(X8,X6)
& X5 = X8
& in(X7,X6)
& X4 = X7
& young(X5)
& man(X5)
& fellow(X5)
& young(X4)
& man(X4)
& fellow(X4)
& X4 != X5
& front(X6)
& furniture(X6)
& seat(X6)
& 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(sK10,sK8)
& sK7 = sK10
& in(sK9,sK8)
& sK6 = sK9
& young(sK7)
& man(sK7)
& fellow(sK7)
& young(sK6)
& man(sK6)
& fellow(sK6)
& sK6 != sK7
& front(sK8)
& furniture(sK8)
& seat(sK8)
& 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,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(f12,plain,
( ( sP0
& ! [X9,X10,X11,X12,X13,X14,X15,X16,X17] :
( ~ in(X17,X15)
| X14 != X17
| ~ in(X16,X15)
| X13 != X16
| ~ young(X14)
| ~ man(X14)
| ~ fellow(X14)
| ~ young(X13)
| ~ man(X13)
| ~ fellow(X13)
| X13 = X14
| ~ front(X15)
| ~ furniture(X15)
| ~ seat(X15)
| ~ in(X10,X9)
| ~ down(X10,X11)
| ~ barrel(X10,X12)
| ~ old(X12)
| ~ dirty(X12)
| ~ white(X12)
| ~ car(X12)
| ~ chevy(X12)
| ~ lonely(X11)
| ~ way(X11)
| ~ street(X11)
| ~ event(X10)
| ~ city(X9)
| ~ hollywood(X9) ) )
| ( sP1
& ! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ~ in(X8,X6)
| X5 != X8
| ~ in(X7,X6)
| X4 != X7
| ~ young(X5)
| ~ man(X5)
| ~ fellow(X5)
| ~ young(X4)
| ~ man(X4)
| ~ fellow(X4)
| X4 = X5
| ~ front(X6)
| ~ furniture(X6)
| ~ seat(X6)
| ~ 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(sK10,sK8) ),
inference(cnf_transformation,[],[f8]) ).
fof(f14,plain,
( ~ sP1
| sK7 = sK10 ),
inference(cnf_transformation,[],[f8]) ).
fof(f15,plain,
( ~ sP1
| in(sK9,sK8) ),
inference(cnf_transformation,[],[f8]) ).
fof(f16,plain,
( ~ sP1
| sK6 = sK9 ),
inference(cnf_transformation,[],[f8]) ).
fof(f17,plain,
( ~ sP1
| young(sK7) ),
inference(cnf_transformation,[],[f8]) ).
fof(f18,plain,
( ~ sP1
| man(sK7) ),
inference(cnf_transformation,[],[f8]) ).
fof(f19,plain,
( ~ sP1
| fellow(sK7) ),
inference(cnf_transformation,[],[f8]) ).
fof(f20,plain,
( ~ sP1
| young(sK6) ),
inference(cnf_transformation,[],[f8]) ).
fof(f21,plain,
( ~ sP1
| man(sK6) ),
inference(cnf_transformation,[],[f8]) ).
fof(f22,plain,
( ~ sP1
| fellow(sK6) ),
inference(cnf_transformation,[],[f8]) ).
fof(f23,plain,
( ~ sP1
| sK6 != sK7 ),
inference(cnf_transformation,[],[f8]) ).
fof(f24,plain,
( ~ sP1
| front(sK8) ),
inference(cnf_transformation,[],[f8]) ).
fof(f25,plain,
( ~ sP1
| furniture(sK8) ),
inference(cnf_transformation,[],[f8]) ).
fof(f26,plain,
( ~ sP1
| seat(sK8) ),
inference(cnf_transformation,[],[f8]) ).
fof(f27,plain,
( ~ sP1
| in(sK3,sK2) ),
inference(cnf_transformation,[],[f8]) ).
fof(f28,plain,
( ~ sP1
| down(sK3,sK4) ),
inference(cnf_transformation,[],[f8]) ).
fof(f29,plain,
( ~ sP1
| barrel(sK3,sK5) ),
inference(cnf_transformation,[],[f8]) ).
fof(f30,plain,
( ~ sP1
| old(sK5) ),
inference(cnf_transformation,[],[f8]) ).
fof(f31,plain,
( ~ sP1
| dirty(sK5) ),
inference(cnf_transformation,[],[f8]) ).
fof(f32,plain,
( ~ sP1
| white(sK5) ),
inference(cnf_transformation,[],[f8]) ).
fof(f33,plain,
( ~ sP1
| car(sK5) ),
inference(cnf_transformation,[],[f8]) ).
fof(f34,plain,
( ~ sP1
| chevy(sK5) ),
inference(cnf_transformation,[],[f8]) ).
fof(f35,plain,
( ~ sP1
| lonely(sK4) ),
inference(cnf_transformation,[],[f8]) ).
fof(f36,plain,
( ~ sP1
| way(sK4) ),
inference(cnf_transformation,[],[f8]) ).
fof(f37,plain,
( ~ sP1
| street(sK4) ),
inference(cnf_transformation,[],[f8]) ).
fof(f38,plain,
( ~ sP1
| event(sK3) ),
inference(cnf_transformation,[],[f8]) ).
fof(f39,plain,
( ~ sP1
| city(sK2) ),
inference(cnf_transformation,[],[f8]) ).
fof(f40,plain,
( ~ sP1
| hollywood(sK2) ),
inference(cnf_transformation,[],[f8]) ).
fof(f69,plain,
( sP0
| sP1 ),
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] :
( ~ in(X17,X15)
| X14 != X17
| ~ in(X16,X15)
| X13 != X16
| ~ young(X14)
| ~ man(X14)
| ~ fellow(X14)
| ~ young(X13)
| ~ man(X13)
| ~ fellow(X13)
| X13 = X14
| ~ front(X15)
| ~ furniture(X15)
| ~ seat(X15)
| ~ in(X10,X9)
| ~ down(X10,X11)
| ~ barrel(X10,X12)
| ~ old(X12)
| ~ dirty(X12)
| ~ white(X12)
| ~ car(X12)
| ~ chevy(X12)
| ~ lonely(X11)
| ~ way(X11)
| ~ street(X11)
| ~ event(X10)
| ~ city(X9)
| ~ hollywood(X9)
| ~ in(X8,X6)
| X5 != X8
| ~ in(X7,X6)
| X4 != X7
| ~ young(X5)
| ~ man(X5)
| ~ fellow(X5)
| ~ young(X4)
| ~ man(X4)
| ~ fellow(X4)
| X4 = X5
| ~ front(X6)
| ~ furniture(X6)
| ~ seat(X6)
| ~ 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]) ).
fof(f73,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X16,X17,X15,X5,X12,X13] :
( ~ in(X17,X15)
| X14 != X17
| ~ in(X16,X15)
| X13 != X16
| ~ young(X14)
| ~ man(X14)
| ~ fellow(X14)
| ~ young(X13)
| ~ man(X13)
| ~ fellow(X13)
| X13 = X14
| ~ front(X15)
| ~ furniture(X15)
| ~ seat(X15)
| ~ in(X10,X9)
| ~ down(X10,X11)
| ~ barrel(X10,X12)
| ~ old(X12)
| ~ dirty(X12)
| ~ white(X12)
| ~ car(X12)
| ~ chevy(X12)
| ~ lonely(X11)
| ~ way(X11)
| ~ street(X11)
| ~ event(X10)
| ~ city(X9)
| ~ hollywood(X9)
| ~ in(X8,X6)
| X5 != X8
| ~ in(X7,X6)
| ~ young(X5)
| ~ man(X5)
| ~ fellow(X5)
| ~ young(X7)
| ~ man(X7)
| ~ fellow(X7)
| X5 = X7
| ~ front(X6)
| ~ furniture(X6)
| ~ seat(X6)
| ~ 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(equality_resolution,[],[f72]) ).
fof(f74,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X16,X17,X15,X12,X13] :
( ~ in(X17,X15)
| X14 != X17
| ~ in(X16,X15)
| X13 != X16
| ~ young(X14)
| ~ man(X14)
| ~ fellow(X14)
| ~ young(X13)
| ~ man(X13)
| ~ fellow(X13)
| X13 = X14
| ~ front(X15)
| ~ furniture(X15)
| ~ seat(X15)
| ~ in(X10,X9)
| ~ down(X10,X11)
| ~ barrel(X10,X12)
| ~ old(X12)
| ~ dirty(X12)
| ~ white(X12)
| ~ car(X12)
| ~ chevy(X12)
| ~ lonely(X11)
| ~ way(X11)
| ~ street(X11)
| ~ event(X10)
| ~ city(X9)
| ~ hollywood(X9)
| ~ in(X8,X6)
| ~ in(X7,X6)
| ~ young(X8)
| ~ man(X8)
| ~ fellow(X8)
| ~ young(X7)
| ~ man(X7)
| ~ fellow(X7)
| X7 = X8
| ~ front(X6)
| ~ furniture(X6)
| ~ seat(X6)
| ~ 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(equality_resolution,[],[f73]) ).
fof(f75,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X16,X17,X15,X12] :
( ~ in(X17,X15)
| X14 != X17
| ~ in(X16,X15)
| ~ young(X14)
| ~ man(X14)
| ~ fellow(X14)
| ~ young(X16)
| ~ man(X16)
| ~ fellow(X16)
| X14 = X16
| ~ front(X15)
| ~ furniture(X15)
| ~ seat(X15)
| ~ in(X10,X9)
| ~ down(X10,X11)
| ~ barrel(X10,X12)
| ~ old(X12)
| ~ dirty(X12)
| ~ white(X12)
| ~ car(X12)
| ~ chevy(X12)
| ~ lonely(X11)
| ~ way(X11)
| ~ street(X11)
| ~ event(X10)
| ~ city(X9)
| ~ hollywood(X9)
| ~ in(X8,X6)
| ~ in(X7,X6)
| ~ young(X8)
| ~ man(X8)
| ~ fellow(X8)
| ~ young(X7)
| ~ man(X7)
| ~ fellow(X7)
| X7 = X8
| ~ front(X6)
| ~ furniture(X6)
| ~ seat(X6)
| ~ 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(equality_resolution,[],[f74]) ).
fof(f76,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X16,X17,X15,X12] :
( ~ in(X17,X15)
| ~ in(X16,X15)
| ~ young(X17)
| ~ man(X17)
| ~ fellow(X17)
| ~ young(X16)
| ~ man(X16)
| ~ fellow(X16)
| X16 = X17
| ~ front(X15)
| ~ furniture(X15)
| ~ seat(X15)
| ~ in(X10,X9)
| ~ down(X10,X11)
| ~ barrel(X10,X12)
| ~ old(X12)
| ~ dirty(X12)
| ~ white(X12)
| ~ car(X12)
| ~ chevy(X12)
| ~ lonely(X11)
| ~ way(X11)
| ~ street(X11)
| ~ event(X10)
| ~ city(X9)
| ~ hollywood(X9)
| ~ in(X8,X6)
| ~ in(X7,X6)
| ~ young(X8)
| ~ man(X8)
| ~ fellow(X8)
| ~ young(X7)
| ~ man(X7)
| ~ fellow(X7)
| X7 = X8
| ~ front(X6)
| ~ furniture(X6)
| ~ seat(X6)
| ~ 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(equality_resolution,[],[f75]) ).
tcf(c_49,plain,
( hollywood(sK2)
| ~ sP1 ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_50,plain,
( city(sK2)
| ~ sP1 ),
inference(cnf_transformation,[],[f39]) ).
tcf(c_51,plain,
( event(sK3)
| ~ sP1 ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_52,plain,
( street(sK4)
| ~ sP1 ),
inference(cnf_transformation,[],[f37]) ).
tcf(c_53,plain,
( way(sK4)
| ~ sP1 ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_54,plain,
( lonely(sK4)
| ~ sP1 ),
inference(cnf_transformation,[],[f35]) ).
tcf(c_55,plain,
( chevy(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_56,plain,
( car(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_57,plain,
( white(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_58,plain,
( dirty(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_59,plain,
( old(sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_60,plain,
( barrel(sK3,sK5)
| ~ sP1 ),
inference(cnf_transformation,[],[f29]) ).
tcf(c_61,plain,
( down(sK3,sK4)
| ~ sP1 ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_62,plain,
( in(sK3,sK2)
| ~ sP1 ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_63,plain,
( seat(sK8)
| ~ sP1 ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_64,plain,
( furniture(sK8)
| ~ sP1 ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_65,plain,
( front(sK8)
| ~ sP1 ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_66,plain,
( ~ sP1
| ( sK6 != sK7 ) ),
inference(cnf_transformation,[],[f23]) ).
tcf(c_67,plain,
( fellow(sK6)
| ~ sP1 ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_68,plain,
( man(sK6)
| ~ sP1 ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_69,plain,
( young(sK6)
| ~ sP1 ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_70,plain,
( fellow(sK7)
| ~ sP1 ),
inference(cnf_transformation,[],[f19]) ).
tcf(c_71,plain,
( man(sK7)
| ~ sP1 ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_72,plain,
( young(sK7)
| ~ sP1 ),
inference(cnf_transformation,[],[f17]) ).
tcf(c_73,plain,
( ( sK6 = sK9 )
| ~ sP1 ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_74,plain,
( in(sK9,sK8)
| ~ sP1 ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_75,plain,
( ( sK7 = sK10 )
| ~ sP1 ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_76,plain,
( in(sK10,sK8)
| ~ sP1 ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_105,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i] :
( ( X11 = X13 )
| ( X7 = X9 )
| ~ young(X13)
| ~ young(X11)
| ~ young(X9)
| ~ young(X7)
| ~ man(X13)
| ~ man(X11)
| ~ man(X9)
| ~ man(X7)
| ~ fellow(X13)
| ~ fellow(X11)
| ~ fellow(X9)
| ~ fellow(X7)
| ~ front(X12)
| ~ front(X8)
| ~ furniture(X12)
| ~ furniture(X8)
| ~ seat(X12)
| ~ seat(X8)
| ~ 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(X10)
| ~ city(X6)
| ~ hollywood(X10)
| ~ hollywood(X6)
| ~ in(X13,X12)
| ~ in(X11,X12)
| ~ in(X9,X8)
| ~ in(X7,X8)
| ~ in(X2,X10)
| ~ in(X0,X6)
| ~ down(X2,X5)
| ~ down(X0,X4)
| ~ barrel(X2,X3)
| ~ barrel(X0,X1) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_108,negated_conjecture,
( sP0
| sP1 ),
inference(cnf_transformation,[],[f69]) ).
tcf(c_4180,negated_conjecture,
! [X0_iProver_down_1: iProver_down_1,X0_iProver_chevy_1: iProver_chevy_1,X0_iProver_street_1: iProver_street_1,X0_iProver_hollywood_1: iProver_hollywood_1,X1_iProver_down_1: iProver_down_1,X1_iProver_chevy_1: iProver_chevy_1,X1_iProver_street_1: iProver_street_1,X1_iProver_hollywood_1: iProver_hollywood_1,X2_iProver_down_1: iProver_down_1,X2_iProver_hollywood_1: iProver_hollywood_1,X3_iProver_down_1: iProver_down_1,X3_iProver_hollywood_1: iProver_hollywood_1,X4_iProver_down_1: iProver_down_1,X5_iProver_down_1: iProver_down_1] :
( ( X4_iProver_down_1 = X5_iProver_down_1 )
| ( X2_iProver_down_1 = X3_iProver_down_1 )
| ~ young(X5_iProver_down_1)
| ~ young(X4_iProver_down_1)
| ~ young(X3_iProver_down_1)
| ~ young(X2_iProver_down_1)
| ~ man(X5_iProver_down_1)
| ~ man(X4_iProver_down_1)
| ~ man(X3_iProver_down_1)
| ~ man(X2_iProver_down_1)
| ~ fellow(X5_iProver_down_1)
| ~ fellow(X4_iProver_down_1)
| ~ fellow(X3_iProver_down_1)
| ~ fellow(X2_iProver_down_1)
| ~ front(X3_iProver_hollywood_1)
| ~ front(X2_iProver_hollywood_1)
| ~ furniture(X3_iProver_hollywood_1)
| ~ furniture(X2_iProver_hollywood_1)
| ~ seat(X3_iProver_hollywood_1)
| ~ seat(X2_iProver_hollywood_1)
| ~ old(X1_iProver_chevy_1)
| ~ old(X0_iProver_chevy_1)
| ~ dirty(X1_iProver_chevy_1)
| ~ dirty(X0_iProver_chevy_1)
| ~ white(X1_iProver_chevy_1)
| ~ white(X0_iProver_chevy_1)
| ~ car(X1_iProver_chevy_1)
| ~ car(X0_iProver_chevy_1)
| ~ chevy(X1_iProver_chevy_1)
| ~ chevy(X0_iProver_chevy_1)
| ~ lonely(X1_iProver_street_1)
| ~ lonely(X0_iProver_street_1)
| ~ way(X1_iProver_street_1)
| ~ way(X0_iProver_street_1)
| ~ street(X1_iProver_street_1)
| ~ street(X0_iProver_street_1)
| ~ event(X1_iProver_down_1)
| ~ event(X0_iProver_down_1)
| ~ city(X1_iProver_hollywood_1)
| ~ city(X0_iProver_hollywood_1)
| ~ hollywood(X1_iProver_hollywood_1)
| ~ hollywood(X0_iProver_hollywood_1)
| ~ in(X5_iProver_down_1,X3_iProver_hollywood_1)
| ~ in(X4_iProver_down_1,X3_iProver_hollywood_1)
| ~ in(X3_iProver_down_1,X2_iProver_hollywood_1)
| ~ in(X2_iProver_down_1,X2_iProver_hollywood_1)
| ~ in(X1_iProver_down_1,X1_iProver_hollywood_1)
| ~ in(X0_iProver_down_1,X0_iProver_hollywood_1)
| ~ down(X1_iProver_down_1,X1_iProver_street_1)
| ~ down(X0_iProver_down_1,X0_iProver_street_1)
| ~ barrel(X1_iProver_down_1,X1_iProver_chevy_1)
| ~ barrel(X0_iProver_down_1,X0_iProver_chevy_1) ),
inference(subtyping,[status(esa)],[c_105]) ).
tcf(c_4210,plain,
( ( sK7 = sK10 )
| ~ sP1 ),
inference(subtyping,[status(esa)],[c_75]) ).
tcf(c_4212,plain,
( ( sK6 = sK9 )
| ~ sP1 ),
inference(subtyping,[status(esa)],[c_73]) ).
tcf(c_4219,plain,
( ~ sP1
| ( sK6 != sK7 ) ),
inference(subtyping,[status(esa)],[c_66]) ).
tcf(c_4237,negated_conjecture,
! [X0_iProver_down_1: iProver_down_1,X0_iProver_hollywood_1: iProver_hollywood_1,X1_iProver_down_1: iProver_down_1] :
( ~ iPr_def_10
| ( X0_iProver_down_1 = X1_iProver_down_1 )
| ~ seat(X0_iProver_hollywood_1)
| ~ furniture(X0_iProver_hollywood_1)
| ~ front(X0_iProver_hollywood_1)
| ~ fellow(X1_iProver_down_1)
| ~ fellow(X0_iProver_down_1)
| ~ man(X1_iProver_down_1)
| ~ man(X0_iProver_down_1)
| ~ young(X1_iProver_down_1)
| ~ young(X0_iProver_down_1)
| ~ in(X1_iProver_down_1,X0_iProver_hollywood_1)
| ~ in(X0_iProver_down_1,X0_iProver_hollywood_1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_4180]) ).
tcf(c_4238,negated_conjecture,
! [X0_iProver_down_1: iProver_down_1,X0_iProver_chevy_1: iProver_chevy_1,X0_iProver_street_1: iProver_street_1,X0_iProver_hollywood_1: iProver_hollywood_1] :
( ~ iPr_def_11
| ~ hollywood(X0_iProver_hollywood_1)
| ~ city(X0_iProver_hollywood_1)
| ~ event(X0_iProver_down_1)
| ~ street(X0_iProver_street_1)
| ~ way(X0_iProver_street_1)
| ~ lonely(X0_iProver_street_1)
| ~ chevy(X0_iProver_chevy_1)
| ~ car(X0_iProver_chevy_1)
| ~ white(X0_iProver_chevy_1)
| ~ dirty(X0_iProver_chevy_1)
| ~ old(X0_iProver_chevy_1)
| ~ barrel(X0_iProver_down_1,X0_iProver_chevy_1)
| ~ down(X0_iProver_down_1,X0_iProver_street_1)
| ~ in(X0_iProver_down_1,X0_iProver_hollywood_1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_4180]) ).
tcf(c_4239,negated_conjecture,
( iPr_def_11
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_4180]) ).
tcf(c_4242,negated_conjecture,
( iPr_def_11
| iPr_def_10 ),
inference(demodulation,[status(thm)],[c_4239]) ).
tcf(c_4251,negated_conjecture,
! [X0_iProver_down_1: iProver_down_1,X0_iProver_chevy_1: iProver_chevy_1,X0_iProver_street_1: iProver_street_1,X0_iProver_hollywood_1: iProver_hollywood_1] :
( ~ iPr_def_11
| ~ old(X0_iProver_chevy_1)
| ~ dirty(X0_iProver_chevy_1)
| ~ white(X0_iProver_chevy_1)
| ~ car(X0_iProver_chevy_1)
| ~ chevy(X0_iProver_chevy_1)
| ~ lonely(X0_iProver_street_1)
| ~ way(X0_iProver_street_1)
| ~ street(X0_iProver_street_1)
| ~ event(X0_iProver_down_1)
| ~ city(X0_iProver_hollywood_1)
| ~ hollywood(X0_iProver_hollywood_1)
| ~ in(X0_iProver_down_1,X0_iProver_hollywood_1)
| ~ down(X0_iProver_down_1,X0_iProver_street_1)
| ~ barrel(X0_iProver_down_1,X0_iProver_chevy_1) ),
inference(demodulation,[status(thm)],[c_4238]) ).
tcf(c_4252,negated_conjecture,
! [X0_iProver_down_1: iProver_down_1,X0_iProver_hollywood_1: iProver_hollywood_1,X1_iProver_down_1: iProver_down_1] :
( ( X0_iProver_down_1 = X1_iProver_down_1 )
| ~ iPr_def_10
| ~ young(X1_iProver_down_1)
| ~ young(X0_iProver_down_1)
| ~ man(X1_iProver_down_1)
| ~ man(X0_iProver_down_1)
| ~ fellow(X1_iProver_down_1)
| ~ fellow(X0_iProver_down_1)
| ~ front(X0_iProver_hollywood_1)
| ~ furniture(X0_iProver_hollywood_1)
| ~ seat(X0_iProver_hollywood_1)
| ~ in(X1_iProver_down_1,X0_iProver_hollywood_1)
| ~ in(X0_iProver_down_1,X0_iProver_hollywood_1) ),
inference(demodulation,[status(thm)],[c_4237]) ).
tcf(c_4260,plain,
! [X0_iProver_down_1: iProver_down_1,X0_iProver_hollywood_1: iProver_hollywood_1,X1_iProver_down_1: iProver_down_1] :
( in(X0_iProver_down_1,X0_iProver_hollywood_1)
| ~ in(X1_iProver_down_1,X0_iProver_hollywood_1)
| ( X0_iProver_down_1 != X1_iProver_down_1 ) ),
theory(equality) ).
tcf(c_4271,plain,
! [X0_iProver_chevy_1: iProver_chevy_1,X0_iProver_street_1: iProver_street_1,X0_iProver_hollywood_1: iProver_hollywood_1] :
( ~ iPr_def_11
| ~ event(sK12)
| ~ old(X0_iProver_chevy_1)
| ~ dirty(X0_iProver_chevy_1)
| ~ white(X0_iProver_chevy_1)
| ~ car(X0_iProver_chevy_1)
| ~ chevy(X0_iProver_chevy_1)
| ~ lonely(X0_iProver_street_1)
| ~ way(X0_iProver_street_1)
| ~ street(X0_iProver_street_1)
| ~ city(X0_iProver_hollywood_1)
| ~ hollywood(X0_iProver_hollywood_1)
| ~ in(sK12,X0_iProver_hollywood_1)
| ~ down(sK12,X0_iProver_street_1)
| ~ barrel(sK12,X0_iProver_chevy_1) ),
inference(instantiation,[status(thm)],[c_4251]) ).
tcf(c_4279,plain,
! [X0_iProver_down_1: iProver_down_1] :
( in(X0_iProver_down_1,sK17)
| ~ in(sK18,sK17)
| ( X0_iProver_down_1 != sK18 ) ),
inference(instantiation,[status(thm)],[c_4260]) ).
tcf(c_4280,plain,
( in(sK15,sK17)
| ~ in(sK18,sK17)
| ( sK15 != sK18 ) ),
inference(instantiation,[status(thm)],[c_4279]) ).
tcf(c_4281,plain,
! [X0_iProver_down_1: iProver_down_1] :
( in(X0_iProver_down_1,sK17)
| ~ in(sK19,sK17)
| ( X0_iProver_down_1 != sK19 ) ),
inference(instantiation,[status(thm)],[c_4260]) ).
tcf(c_4283,plain,
! [X0_iProver_hollywood_1: iProver_hollywood_1] :
( ( sK15 = sK16 )
| ~ iPr_def_10
| ~ young(sK16)
| ~ young(sK15)
| ~ man(sK16)
| ~ man(sK15)
| ~ fellow(sK16)
| ~ fellow(sK15)
| ~ front(X0_iProver_hollywood_1)
| ~ furniture(X0_iProver_hollywood_1)
| ~ seat(X0_iProver_hollywood_1)
| ~ in(sK16,X0_iProver_hollywood_1)
| ~ in(sK15,X0_iProver_hollywood_1) ),
inference(instantiation,[status(thm)],[c_4252]) ).
tcf(c_4284,plain,
( ( sK15 = sK16 )
| ~ iPr_def_10
| ~ young(sK16)
| ~ young(sK15)
| ~ man(sK16)
| ~ man(sK15)
| ~ fellow(sK16)
| ~ fellow(sK15)
| ~ front(sK17)
| ~ furniture(sK17)
| ~ seat(sK17)
| ~ in(sK16,sK17)
| ~ in(sK15,sK17) ),
inference(instantiation,[status(thm)],[c_4283]) ).
tcf(c_4285,plain,
! [X0_iProver_chevy_1: iProver_chevy_1,X0_iProver_street_1: iProver_street_1] :
( ~ iPr_def_11
| ~ event(sK12)
| ~ city(sK11)
| ~ hollywood(sK11)
| ~ old(X0_iProver_chevy_1)
| ~ dirty(X0_iProver_chevy_1)
| ~ white(X0_iProver_chevy_1)
| ~ car(X0_iProver_chevy_1)
| ~ chevy(X0_iProver_chevy_1)
| ~ lonely(X0_iProver_street_1)
| ~ way(X0_iProver_street_1)
| ~ street(X0_iProver_street_1)
| ~ in(sK12,sK11)
| ~ down(sK12,X0_iProver_street_1)
| ~ barrel(sK12,X0_iProver_chevy_1) ),
inference(instantiation,[status(thm)],[c_4271]) ).
tcf(c_4286,plain,
( ~ iPr_def_11
| ~ old(sK13)
| ~ dirty(sK13)
| ~ white(sK13)
| ~ car(sK13)
| ~ chevy(sK13)
| ~ lonely(sK14)
| ~ way(sK14)
| ~ street(sK14)
| ~ event(sK12)
| ~ city(sK11)
| ~ hollywood(sK11)
| ~ in(sK12,sK11)
| ~ down(sK12,sK14)
| ~ barrel(sK12,sK13) ),
inference(instantiation,[status(thm)],[c_4285]) ).
tcf(c_4309,plain,
( in(sK16,sK17)
| ~ in(sK19,sK17)
| ( sK16 != sK19 ) ),
inference(instantiation,[status(thm)],[c_4281]) ).
tcf(c_4336,plain,
! [X0_iProver_chevy_1: iProver_chevy_1,X0_iProver_street_1: iProver_street_1,X0_iProver_hollywood_1: iProver_hollywood_1] :
( ~ iPr_def_11
| ~ event(sK3)
| ~ old(X0_iProver_chevy_1)
| ~ dirty(X0_iProver_chevy_1)
| ~ white(X0_iProver_chevy_1)
| ~ car(X0_iProver_chevy_1)
| ~ chevy(X0_iProver_chevy_1)
| ~ lonely(X0_iProver_street_1)
| ~ way(X0_iProver_street_1)
| ~ street(X0_iProver_street_1)
| ~ city(X0_iProver_hollywood_1)
| ~ hollywood(X0_iProver_hollywood_1)
| ~ in(sK3,X0_iProver_hollywood_1)
| ~ down(sK3,X0_iProver_street_1)
| ~ barrel(sK3,X0_iProver_chevy_1) ),
inference(instantiation,[status(thm)],[c_4251]) ).
tcf(c_4342,plain,
! [X0_iProver_hollywood_1: iProver_hollywood_1] :
( ( sK6 = sK7 )
| ~ iPr_def_10
| ~ young(sK7)
| ~ young(sK6)
| ~ man(sK7)
| ~ man(sK6)
| ~ fellow(sK7)
| ~ fellow(sK6)
| ~ front(X0_iProver_hollywood_1)
| ~ furniture(X0_iProver_hollywood_1)
| ~ seat(X0_iProver_hollywood_1)
| ~ in(sK7,X0_iProver_hollywood_1)
| ~ in(sK6,X0_iProver_hollywood_1) ),
inference(instantiation,[status(thm)],[c_4252]) ).
tcf(c_4344,plain,
! [X0_iProver_chevy_1: iProver_chevy_1,X0_iProver_street_1: iProver_street_1] :
( ~ iPr_def_11
| ~ event(sK3)
| ~ city(sK2)
| ~ hollywood(sK2)
| ~ old(X0_iProver_chevy_1)
| ~ dirty(X0_iProver_chevy_1)
| ~ white(X0_iProver_chevy_1)
| ~ car(X0_iProver_chevy_1)
| ~ chevy(X0_iProver_chevy_1)
| ~ lonely(X0_iProver_street_1)
| ~ way(X0_iProver_street_1)
| ~ street(X0_iProver_street_1)
| ~ in(sK3,sK2)
| ~ down(sK3,X0_iProver_street_1)
| ~ barrel(sK3,X0_iProver_chevy_1) ),
inference(instantiation,[status(thm)],[c_4336]) ).
tcf(c_4362,plain,
! [X0_iProver_down_1: iProver_down_1,X0_iProver_hollywood_1: iProver_hollywood_1] :
( in(sK7,X0_iProver_hollywood_1)
| ~ in(X0_iProver_down_1,X0_iProver_hollywood_1)
| ( sK7 != X0_iProver_down_1 ) ),
inference(instantiation,[status(thm)],[c_4260]) ).
tcf(c_4364,plain,
! [X0_iProver_chevy_1: iProver_chevy_1] :
( ~ iPr_def_11
| ~ lonely(sK4)
| ~ way(sK4)
| ~ street(sK4)
| ~ event(sK3)
| ~ city(sK2)
| ~ hollywood(sK2)
| ~ old(X0_iProver_chevy_1)
| ~ dirty(X0_iProver_chevy_1)
| ~ white(X0_iProver_chevy_1)
| ~ car(X0_iProver_chevy_1)
| ~ chevy(X0_iProver_chevy_1)
| ~ in(sK3,sK2)
| ~ down(sK3,sK4)
| ~ barrel(sK3,X0_iProver_chevy_1) ),
inference(instantiation,[status(thm)],[c_4344]) ).
tcf(c_4381,plain,
! [X0_iProver_hollywood_1: iProver_hollywood_1] :
( in(sK7,X0_iProver_hollywood_1)
| ~ in(sK10,X0_iProver_hollywood_1)
| ( sK7 != sK10 ) ),
inference(instantiation,[status(thm)],[c_4362]) ).
tcf(c_4395,plain,
( ~ iPr_def_11
| ~ 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_4364]) ).
tcf(c_4419,plain,
( in(sK7,sK8)
| ~ in(sK10,sK8)
| ( sK7 != sK10 ) ),
inference(instantiation,[status(thm)],[c_4381]) ).
tcf(c_4462,plain,
( ( sK6 = sK7 )
| ~ iPr_def_10
| ~ young(sK7)
| ~ young(sK6)
| ~ man(sK7)
| ~ man(sK6)
| ~ fellow(sK7)
| ~ fellow(sK6)
| ~ front(sK8)
| ~ furniture(sK8)
| ~ seat(sK8)
| ~ in(sK7,sK8)
| ~ in(sK6,sK8) ),
inference(instantiation,[status(thm)],[c_4342]) ).
tcf(c_4467,plain,
! [X0_iProver_down_1: iProver_down_1,X0_iProver_hollywood_1: iProver_hollywood_1] :
( in(sK6,X0_iProver_hollywood_1)
| ~ in(X0_iProver_down_1,X0_iProver_hollywood_1)
| ( sK6 != X0_iProver_down_1 ) ),
inference(instantiation,[status(thm)],[c_4260]) ).
tcf(c_4473,plain,
! [X0_iProver_hollywood_1: iProver_hollywood_1] :
( in(sK6,X0_iProver_hollywood_1)
| ~ in(sK9,X0_iProver_hollywood_1)
| ( sK6 != sK9 ) ),
inference(instantiation,[status(thm)],[c_4467]) ).
tcf(c_4517,plain,
( in(sK6,sK8)
| ~ in(sK9,sK8)
| ( sK6 != sK9 ) ),
inference(instantiation,[status(thm)],[c_4473]) ).
fof(f4,definition,
( ~ sP0
| ? [X18,X19,X20,X21,X22,X23,X24,X25,X26] :
( in(X26,X24)
& X23 = X26
& in(X25,X24)
& X22 = X25
& young(X23)
& man(X23)
& fellow(X23)
& young(X22)
& man(X22)
& fellow(X22)
& X22 != X23
& front(X24)
& furniture(X24)
& seat(X24)
& in(X19,X18)
& down(X19,X21)
& barrel(X19,X20)
& lonely(X21)
& way(X21)
& street(X21)
& old(X20)
& dirty(X20)
& white(X20)
& car(X20)
& chevy(X20)
& event(X19)
& city(X18)
& hollywood(X18) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f5,definition,
( ~ sP1
| ? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( in(X8,X6)
& X5 = X8
& in(X7,X6)
& X4 = X7
& young(X5)
& man(X5)
& fellow(X5)
& young(X4)
& man(X4)
& fellow(X4)
& X4 != X5
& front(X6)
& furniture(X6)
& seat(X6)
& 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
& ! [X27,X28,X29,X30,X31,X32,X33,X34,X35] :
( ~ in(X35,X33)
| X32 != X35
| ~ in(X34,X33)
| X31 != X34
| ~ young(X32)
| ~ man(X32)
| ~ fellow(X32)
| ~ young(X31)
| ~ man(X31)
| ~ fellow(X31)
| X31 = X32
| ~ front(X33)
| ~ furniture(X33)
| ~ seat(X33)
| ~ in(X28,X27)
| ~ down(X28,X29)
| ~ barrel(X28,X30)
| ~ old(X30)
| ~ dirty(X30)
| ~ white(X30)
| ~ car(X30)
| ~ chevy(X30)
| ~ lonely(X29)
| ~ way(X29)
| ~ street(X29)
| ~ event(X28)
| ~ city(X27)
| ~ hollywood(X27) ) )
| ( sP1
& ! [X9,X10,X11,X12,X13,X14,X15,X16,X17] :
( ~ in(X17,X15)
| X14 != X17
| ~ in(X16,X15)
| X13 != X16
| ~ young(X14)
| ~ man(X14)
| ~ fellow(X14)
| ~ young(X13)
| ~ man(X13)
| ~ fellow(X13)
| X13 = X14
| ~ front(X15)
| ~ furniture(X15)
| ~ seat(X15)
| ~ in(X10,X9)
| ~ down(X10,X12)
| ~ barrel(X10,X11)
| ~ lonely(X12)
| ~ way(X12)
| ~ street(X12)
| ~ old(X11)
| ~ dirty(X11)
| ~ white(X11)
| ~ car(X11)
| ~ chevy(X11)
| ~ event(X10)
| ~ city(X9)
| ~ hollywood(X9) ) ) ),
inference(definition_folding,[],[f3,f5,f4]) ).
fof(f9,plain,
( ~ sP0
| ? [X18,X19,X20,X21,X22,X23,X24,X25,X26] :
( in(X26,X24)
& X23 = X26
& in(X25,X24)
& X22 = X25
& young(X23)
& man(X23)
& fellow(X23)
& young(X22)
& man(X22)
& fellow(X22)
& X22 != X23
& front(X24)
& furniture(X24)
& seat(X24)
& in(X19,X18)
& down(X19,X21)
& barrel(X19,X20)
& lonely(X21)
& way(X21)
& street(X21)
& old(X20)
& dirty(X20)
& white(X20)
& car(X20)
& chevy(X20)
& event(X19)
& city(X18)
& hollywood(X18) ) ),
inference(nnf_transformation,[],[f4]) ).
fof(f10,plain,
( ~ sP0
| ? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( in(X8,X6)
& X5 = X8
& in(X7,X6)
& X4 = X7
& young(X5)
& man(X5)
& fellow(X5)
& young(X4)
& man(X4)
& fellow(X4)
& X4 != X5
& front(X6)
& furniture(X6)
& seat(X6)
& 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(sK19,sK17)
& sK16 = sK19
& in(sK18,sK17)
& sK15 = sK18
& young(sK16)
& man(sK16)
& fellow(sK16)
& young(sK15)
& man(sK15)
& fellow(sK15)
& sK15 != sK16
& front(sK17)
& furniture(sK17)
& seat(sK17)
& in(sK12,sK11)
& down(sK12,sK14)
& barrel(sK12,sK13)
& lonely(sK14)
& way(sK14)
& street(sK14)
& old(sK13)
& dirty(sK13)
& white(sK13)
& car(sK13)
& chevy(sK13)
& event(sK12)
& city(sK11)
& hollywood(sK11) ) ),
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(f41,plain,
( ~ sP0
| in(sK19,sK17) ),
inference(cnf_transformation,[],[f11]) ).
fof(f42,plain,
( ~ sP0
| sK16 = sK19 ),
inference(cnf_transformation,[],[f11]) ).
fof(f43,plain,
( ~ sP0
| in(sK18,sK17) ),
inference(cnf_transformation,[],[f11]) ).
fof(f44,plain,
( ~ sP0
| sK15 = sK18 ),
inference(cnf_transformation,[],[f11]) ).
fof(f45,plain,
( ~ sP0
| young(sK16) ),
inference(cnf_transformation,[],[f11]) ).
fof(f46,plain,
( ~ sP0
| man(sK16) ),
inference(cnf_transformation,[],[f11]) ).
fof(f47,plain,
( ~ sP0
| fellow(sK16) ),
inference(cnf_transformation,[],[f11]) ).
fof(f48,plain,
( ~ sP0
| young(sK15) ),
inference(cnf_transformation,[],[f11]) ).
fof(f49,plain,
( ~ sP0
| man(sK15) ),
inference(cnf_transformation,[],[f11]) ).
fof(f50,plain,
( ~ sP0
| fellow(sK15) ),
inference(cnf_transformation,[],[f11]) ).
fof(f51,plain,
( ~ sP0
| sK15 != sK16 ),
inference(cnf_transformation,[],[f11]) ).
fof(f52,plain,
( ~ sP0
| front(sK17) ),
inference(cnf_transformation,[],[f11]) ).
fof(f53,plain,
( ~ sP0
| furniture(sK17) ),
inference(cnf_transformation,[],[f11]) ).
fof(f54,plain,
( ~ sP0
| seat(sK17) ),
inference(cnf_transformation,[],[f11]) ).
fof(f55,plain,
( ~ sP0
| in(sK12,sK11) ),
inference(cnf_transformation,[],[f11]) ).
fof(f56,plain,
( ~ sP0
| down(sK12,sK14) ),
inference(cnf_transformation,[],[f11]) ).
fof(f57,plain,
( ~ sP0
| barrel(sK12,sK13) ),
inference(cnf_transformation,[],[f11]) ).
fof(f58,plain,
( ~ sP0
| lonely(sK14) ),
inference(cnf_transformation,[],[f11]) ).
fof(f59,plain,
( ~ sP0
| way(sK14) ),
inference(cnf_transformation,[],[f11]) ).
fof(f60,plain,
( ~ sP0
| street(sK14) ),
inference(cnf_transformation,[],[f11]) ).
fof(f61,plain,
( ~ sP0
| old(sK13) ),
inference(cnf_transformation,[],[f11]) ).
fof(f62,plain,
( ~ sP0
| dirty(sK13) ),
inference(cnf_transformation,[],[f11]) ).
fof(f63,plain,
( ~ sP0
| white(sK13) ),
inference(cnf_transformation,[],[f11]) ).
fof(f64,plain,
( ~ sP0
| car(sK13) ),
inference(cnf_transformation,[],[f11]) ).
fof(f65,plain,
( ~ sP0
| chevy(sK13) ),
inference(cnf_transformation,[],[f11]) ).
fof(f66,plain,
( ~ sP0
| event(sK12) ),
inference(cnf_transformation,[],[f11]) ).
fof(f67,plain,
( ~ sP0
| city(sK11) ),
inference(cnf_transformation,[],[f11]) ).
fof(f68,plain,
( ~ sP0
| hollywood(sK11) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_77,plain,
( hollywood(sK11)
| ~ sP0 ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_78,plain,
( city(sK11)
| ~ sP0 ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_79,plain,
( event(sK12)
| ~ sP0 ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_80,plain,
( chevy(sK13)
| ~ sP0 ),
inference(cnf_transformation,[],[f65]) ).
tcf(c_81,plain,
( car(sK13)
| ~ sP0 ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_82,plain,
( white(sK13)
| ~ sP0 ),
inference(cnf_transformation,[],[f63]) ).
tcf(c_83,plain,
( dirty(sK13)
| ~ sP0 ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_84,plain,
( old(sK13)
| ~ sP0 ),
inference(cnf_transformation,[],[f61]) ).
tcf(c_85,plain,
( street(sK14)
| ~ sP0 ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_86,plain,
( way(sK14)
| ~ sP0 ),
inference(cnf_transformation,[],[f59]) ).
tcf(c_87,plain,
( lonely(sK14)
| ~ sP0 ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_88,plain,
( barrel(sK12,sK13)
| ~ sP0 ),
inference(cnf_transformation,[],[f57]) ).
tcf(c_89,plain,
( down(sK12,sK14)
| ~ sP0 ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_90,plain,
( in(sK12,sK11)
| ~ sP0 ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_91,plain,
( seat(sK17)
| ~ sP0 ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_92,plain,
( furniture(sK17)
| ~ sP0 ),
inference(cnf_transformation,[],[f53]) ).
tcf(c_93,plain,
( front(sK17)
| ~ sP0 ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_94,plain,
( ~ sP0
| ( sK15 != sK16 ) ),
inference(cnf_transformation,[],[f51]) ).
tcf(c_95,plain,
( fellow(sK15)
| ~ sP0 ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_96,plain,
( man(sK15)
| ~ sP0 ),
inference(cnf_transformation,[],[f49]) ).
tcf(c_97,plain,
( young(sK15)
| ~ sP0 ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_98,plain,
( fellow(sK16)
| ~ sP0 ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_99,plain,
( man(sK16)
| ~ sP0 ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_100,plain,
( young(sK16)
| ~ sP0 ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_101,plain,
( ( sK15 = sK18 )
| ~ sP0 ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_102,plain,
( in(sK18,sK17)
| ~ sP0 ),
inference(cnf_transformation,[],[f43]) ).
tcf(c_103,plain,
( ( sK16 = sK19 )
| ~ sP0 ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_104,plain,
( in(sK19,sK17)
| ~ sP0 ),
inference(cnf_transformation,[],[f41]) ).
tcf(c_2365,plain,
( sP1
| in(sK19,sK17) ),
inference(resolution,[status(thm)],[c_108,c_104]) ).
tcf(c_2379,plain,
( sP1
| in(sK18,sK17) ),
inference(resolution,[status(thm)],[c_108,c_102]) ).
tcf(c_2393,plain,
( sP1
| young(sK16) ),
inference(resolution,[status(thm)],[c_108,c_100]) ).
tcf(c_2400,plain,
( sP1
| man(sK16) ),
inference(resolution,[status(thm)],[c_108,c_99]) ).
tcf(c_2407,plain,
( sP1
| fellow(sK16) ),
inference(resolution,[status(thm)],[c_108,c_98]) ).
tcf(c_2414,plain,
( sP1
| young(sK15) ),
inference(resolution,[status(thm)],[c_108,c_97]) ).
tcf(c_2421,plain,
( sP1
| man(sK15) ),
inference(resolution,[status(thm)],[c_108,c_96]) ).
tcf(c_2428,plain,
( sP1
| fellow(sK15) ),
inference(resolution,[status(thm)],[c_108,c_95]) ).
tcf(c_2442,plain,
( sP1
| front(sK17) ),
inference(resolution,[status(thm)],[c_108,c_93]) ).
tcf(c_2449,plain,
( sP1
| furniture(sK17) ),
inference(resolution,[status(thm)],[c_108,c_92]) ).
tcf(c_2456,plain,
( sP1
| seat(sK17) ),
inference(resolution,[status(thm)],[c_108,c_91]) ).
tcf(c_2463,plain,
( sP1
| in(sK12,sK11) ),
inference(resolution,[status(thm)],[c_108,c_90]) ).
tcf(c_2470,plain,
( sP1
| down(sK12,sK14) ),
inference(resolution,[status(thm)],[c_108,c_89]) ).
tcf(c_2477,plain,
( sP1
| barrel(sK12,sK13) ),
inference(resolution,[status(thm)],[c_108,c_88]) ).
tcf(c_2484,plain,
( sP1
| lonely(sK14) ),
inference(resolution,[status(thm)],[c_108,c_87]) ).
tcf(c_2491,plain,
( sP1
| way(sK14) ),
inference(resolution,[status(thm)],[c_108,c_86]) ).
tcf(c_2498,plain,
( sP1
| street(sK14) ),
inference(resolution,[status(thm)],[c_108,c_85]) ).
tcf(c_2505,plain,
( sP1
| old(sK13) ),
inference(resolution,[status(thm)],[c_108,c_84]) ).
tcf(c_2512,plain,
( sP1
| dirty(sK13) ),
inference(resolution,[status(thm)],[c_108,c_83]) ).
tcf(c_2519,plain,
( sP1
| white(sK13) ),
inference(resolution,[status(thm)],[c_108,c_82]) ).
tcf(c_2526,plain,
( sP1
| car(sK13) ),
inference(resolution,[status(thm)],[c_108,c_81]) ).
tcf(c_2533,plain,
( sP1
| chevy(sK13) ),
inference(resolution,[status(thm)],[c_108,c_80]) ).
tcf(c_2540,plain,
( sP1
| event(sK12) ),
inference(resolution,[status(thm)],[c_108,c_79]) ).
tcf(c_2547,plain,
( sP1
| city(sK11) ),
inference(resolution,[status(thm)],[c_108,c_78]) ).
tcf(c_2554,plain,
( sP1
| hollywood(sK11) ),
inference(resolution,[status(thm)],[c_108,c_77]) ).
tcf(c_4182,plain,
( ( sK16 = sK19 )
| ~ sP0 ),
inference(subtyping,[status(esa)],[c_103]) ).
tcf(c_4184,plain,
( ( sK15 = sK18 )
| ~ sP0 ),
inference(subtyping,[status(esa)],[c_101]) ).
tcf(c_4191,plain,
( ~ sP0
| ( sK15 != sK16 ) ),
inference(subtyping,[status(esa)],[c_94]) ).
tcf(c_4532,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_4517,c_4462,c_4419,c_4395,c_4309,c_4286,c_4284,c_4280,c_4242,c_4219,c_4212,c_4210,c_4191,c_4184,c_4182,c_2554,c_2547,c_2540,c_2533,c_2526,c_2519,c_2512,c_2505,c_2498,c_2491,c_2484,c_2477,c_2470,c_2463,c_2456,c_2449,c_2442,c_2428,c_2421,c_2414,c_2407,c_2400,c_2393,c_2379,c_2365,c_60,c_61,c_62,c_74,c_76,c_49,c_50,c_51,c_52,c_53,c_54,c_55,c_56,c_57,c_58,c_59,c_63,c_64,c_65,c_67,c_68,c_69,c_70,c_71,c_72,c_108]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : NLP009+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.02 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Thu Sep 24 01:37:52 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.03/0.32 Running first-order theorem proving
% 0.03/0.32 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.07/0.33
% 0.07/0.33 % ======== iProver multi-core TPTP/SMT =========
% 0.07/0.33
% 0.07/0.33 % Detected problem language: tptp
% 0.07/0.33 % Proving...
% 0.54/0.96 % SZS status Started for theBenchmark.p
% 0.54/0.96 % SZS status Theorem for theBenchmark.p
% 0.54/0.96
% 0.54/0.96 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 0.54/0.96
% 0.54/0.96 % ------ iProver source info
% 0.54/0.96
% 0.54/0.96 % git: date: 2026-07-19 20:42:38 +0200
% 0.54/0.96 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 0.54/0.96 % git: non_committed_changes: false
% 0.54/0.96
% 0.54/0.96 % ------ Parsing...
% 0.54/0.96 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Option_epr_non_horn_eq
% 0.54/0.96 %
% 0.54/0.96
% 0.54/0.96 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 0.54/0.96
% 0.54/0.96 % ------ Preprocessing...% ------ preprocesses with Option_epr_non_horn_eq
% 0.54/0.96 gs_s sp: 8 0s gs_e snvd_s sp: 0 0s snvd_e % ------ preprocesses with Option_epr_non_horn_eq
% 0.54/0.96 %
% 0.54/0.96
% 0.54/0.96 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 0.54/0.96 % ------ Proving...
% 0.54/0.96 % ------ Problem Properties
% 0.54/0.96
% 0.54/0.96 %
% 0.54/0.96 % clauses 62
% 0.54/0.96 % conjectures 6
% 0.54/0.96 % EPR 62
% 0.54/0.96 % Horn 58
% 0.54/0.96 % unary 0
% 0.54/0.96 % binary 58
% 0.54/0.96 % lits 150
% 0.54/0.96 % lits eq 7
% 0.54/0.96 % fd_pure 0
% 0.54/0.96 % fd_pseudo 0
% 0.54/0.96 % fd_cond 0
% 0.54/0.96 % fd_pseudo_cond 1
% 0.54/0.96 % AC symbols 0
% 0.54/0.96
% 0.54/0.96 % ------ Schedule EPR non Horn eq is on
% 0.54/0.96
% 0.54/0.96 % ------ Option_epr_non_horn_eq Time Limit: Unbounded
% 0.54/0.96
% 0.54/0.96
% 0.54/0.96 % ------
% 0.54/0.96 % Current options:
% 0.54/0.96 % ------
% 0.54/0.96
% 0.54/0.96
% 0.54/0.96 %
% 0.54/0.96
% 0.54/0.96 % ------ Proving...
% 0.54/0.96 %
% 0.54/0.96
% 0.54/0.96 % SZS status Theorem for theBenchmark.p
% 0.54/0.96
% 0.54/0.96 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 0.54/0.96
% 0.54/0.96
%------------------------------------------------------------------------------