%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : NLP009+1 : TPTP v5.0.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art01.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Sat Dec 25 21:11:14 EST 2010
% Result : Theorem 0.22s
% Output : CNFRefutation 0.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 72
% Number of leaves : 3
% Syntax : Number of formulae : 173 ( 35 unt; 0 def)
% Number of atoms : 2112 ( 173 equ)
% Maximal formula atoms : 112 ( 12 avg)
% Number of connectives : 3082 (1143 ~;1324 |; 607 &)
% ( 0 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 67 ( 11 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 24 ( 22 usr; 3 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 18 con; 0-0 aty)
% Number of variables : 425 ( 0 sgn 90 !; 144 ?)
% Comments :
%------------------------------------------------------------------------------
fof(1,conjecture,
( ( ? [X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( hollywood(X1)
& city(X1)
& event(X2)
& street(X3)
& way(X3)
& lonely(X3)
& chevy(X4)
& car(X4)
& white(X4)
& dirty(X4)
& old(X4)
& barrel(X2,X4)
& down(X2,X3)
& in(X2,X1)
& seat(X7)
& furniture(X7)
& front(X7)
& X5 != X6
& fellow(X5)
& man(X5)
& young(X5)
& fellow(X6)
& man(X6)
& young(X6)
& X5 = X8
& in(X8,X7)
& X6 = X9
& in(X9,X7) )
=> ? [X10,X11,X12,X13,X14,X15,X16,X17,X18] :
( hollywood(X10)
& city(X10)
& event(X11)
& chevy(X12)
& car(X12)
& white(X12)
& dirty(X12)
& old(X12)
& street(X13)
& way(X13)
& lonely(X13)
& barrel(X11,X12)
& down(X11,X13)
& in(X11,X10)
& seat(X16)
& furniture(X16)
& front(X16)
& X14 != X15
& fellow(X14)
& man(X14)
& young(X14)
& fellow(X15)
& man(X15)
& young(X15)
& X14 = X17
& in(X17,X16)
& X15 = X18
& in(X18,X16) ) )
& ( ? [X19,X20,X21,X22,X23,X24,X25,X26,X27] :
( hollywood(X19)
& city(X19)
& event(X20)
& chevy(X21)
& car(X21)
& white(X21)
& dirty(X21)
& old(X21)
& street(X22)
& way(X22)
& lonely(X22)
& barrel(X20,X21)
& down(X20,X22)
& in(X20,X19)
& seat(X25)
& furniture(X25)
& front(X25)
& X23 != X24
& fellow(X23)
& man(X23)
& young(X23)
& fellow(X24)
& man(X24)
& young(X24)
& X23 = X26
& in(X26,X25)
& X24 = X27
& in(X27,X25) )
=> ? [X28,X29,X30,X31,X32,X33,X34,X35,X36] :
( hollywood(X28)
& city(X28)
& event(X29)
& street(X30)
& way(X30)
& lonely(X30)
& chevy(X31)
& car(X31)
& white(X31)
& dirty(X31)
& old(X31)
& barrel(X29,X31)
& down(X29,X30)
& in(X29,X28)
& seat(X34)
& furniture(X34)
& front(X34)
& X32 != X33
& fellow(X32)
& man(X32)
& young(X32)
& fellow(X33)
& man(X33)
& young(X33)
& X32 = X35
& in(X35,X34)
& X33 = X36
& in(X36,X34) ) ) ),
file('/tmp/tmpmIEcTk/sel_NLP009+1.p_1',co1) ).
fof(2,negated_conjecture,
~ ( ( ? [X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( hollywood(X1)
& city(X1)
& event(X2)
& street(X3)
& way(X3)
& lonely(X3)
& chevy(X4)
& car(X4)
& white(X4)
& dirty(X4)
& old(X4)
& barrel(X2,X4)
& down(X2,X3)
& in(X2,X1)
& seat(X7)
& furniture(X7)
& front(X7)
& X5 != X6
& fellow(X5)
& man(X5)
& young(X5)
& fellow(X6)
& man(X6)
& young(X6)
& X5 = X8
& in(X8,X7)
& X6 = X9
& in(X9,X7) )
=> ? [X10,X11,X12,X13,X14,X15,X16,X17,X18] :
( hollywood(X10)
& city(X10)
& event(X11)
& chevy(X12)
& car(X12)
& white(X12)
& dirty(X12)
& old(X12)
& street(X13)
& way(X13)
& lonely(X13)
& barrel(X11,X12)
& down(X11,X13)
& in(X11,X10)
& seat(X16)
& furniture(X16)
& front(X16)
& X14 != X15
& fellow(X14)
& man(X14)
& young(X14)
& fellow(X15)
& man(X15)
& young(X15)
& X14 = X17
& in(X17,X16)
& X15 = X18
& in(X18,X16) ) )
& ( ? [X19,X20,X21,X22,X23,X24,X25,X26,X27] :
( hollywood(X19)
& city(X19)
& event(X20)
& chevy(X21)
& car(X21)
& white(X21)
& dirty(X21)
& old(X21)
& street(X22)
& way(X22)
& lonely(X22)
& barrel(X20,X21)
& down(X20,X22)
& in(X20,X19)
& seat(X25)
& furniture(X25)
& front(X25)
& X23 != X24
& fellow(X23)
& man(X23)
& young(X23)
& fellow(X24)
& man(X24)
& young(X24)
& X23 = X26
& in(X26,X25)
& X24 = X27
& in(X27,X25) )
=> ? [X28,X29,X30,X31,X32,X33,X34,X35,X36] :
( hollywood(X28)
& city(X28)
& event(X29)
& street(X30)
& way(X30)
& lonely(X30)
& chevy(X31)
& car(X31)
& white(X31)
& dirty(X31)
& old(X31)
& barrel(X29,X31)
& down(X29,X30)
& in(X29,X28)
& seat(X34)
& furniture(X34)
& front(X34)
& X32 != X33
& fellow(X32)
& man(X32)
& young(X32)
& fellow(X33)
& man(X33)
& young(X33)
& X32 = X35
& in(X35,X34)
& X33 = X36
& in(X36,X34) ) ) ),
inference(assume_negation,[status(cth)],[1]) ).
fof(3,plain,
( ( ? [X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( hollywood(X1)
& city(X1)
& event(X2)
& street(X3)
& way(X3)
& lonely(X3)
& chevy(X4)
& car(X4)
& white(X4)
& dirty(X4)
& old(X4)
& barrel(X2,X4)
& down(X2,X3)
& in(X2,X1)
& seat(X7)
& furniture(X7)
& front(X7)
& X5 != X6
& fellow(X5)
& man(X5)
& young(X5)
& fellow(X6)
& man(X6)
& young(X6)
& X5 = X8
& in(X8,X7)
& X6 = X9
& in(X9,X7) )
=> ? [X10,X11,X12,X13,X14,X15,X16,X17,X18] :
( hollywood(X10)
& city(X10)
& event(X11)
& chevy(X12)
& car(X12)
& white(X12)
& dirty(X12)
& old(X12)
& street(X13)
& way(X13)
& lonely(X13)
& barrel(X11,X12)
& down(X11,X13)
& in(X11,X10)
& seat(X16)
& furniture(X16)
& front(X16)
& X14 != X15
& fellow(X14)
& man(X14)
& young(X14)
& fellow(X15)
& man(X15)
& young(X15)
& X14 = X17
& in(X17,X16)
& X15 = X18
& in(X18,X16) ) )
=> epred1_0 ),
introduced(definition) ).
fof(4,plain,
( ( ? [X19,X20,X21,X22,X23,X24,X25,X26,X27] :
( hollywood(X19)
& city(X19)
& event(X20)
& chevy(X21)
& car(X21)
& white(X21)
& dirty(X21)
& old(X21)
& street(X22)
& way(X22)
& lonely(X22)
& barrel(X20,X21)
& down(X20,X22)
& in(X20,X19)
& seat(X25)
& furniture(X25)
& front(X25)
& X23 != X24
& fellow(X23)
& man(X23)
& young(X23)
& fellow(X24)
& man(X24)
& young(X24)
& X23 = X26
& in(X26,X25)
& X24 = X27
& in(X27,X25) )
=> ? [X28,X29,X30,X31,X32,X33,X34,X35,X36] :
( hollywood(X28)
& city(X28)
& event(X29)
& street(X30)
& way(X30)
& lonely(X30)
& chevy(X31)
& car(X31)
& white(X31)
& dirty(X31)
& old(X31)
& barrel(X29,X31)
& down(X29,X30)
& in(X29,X28)
& seat(X34)
& furniture(X34)
& front(X34)
& X32 != X33
& fellow(X32)
& man(X32)
& young(X32)
& fellow(X33)
& man(X33)
& young(X33)
& X32 = X35
& in(X35,X34)
& X33 = X36
& in(X36,X34) ) )
=> epred2_0 ),
introduced(definition) ).
fof(5,negated_conjecture,
~ ( epred1_0
& epred2_0 ),
inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[2,3,theory(equality)]),4,theory(equality)]) ).
fof(6,negated_conjecture,
( ~ epred1_0
| ~ epred2_0 ),
inference(fof_nnf,[status(thm)],[5]) ).
cnf(7,negated_conjecture,
( ~ epred2_0
| ~ epred1_0 ),
inference(split_conjunct,[status(thm)],[6]) ).
fof(8,plain,
( ( ? [X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( hollywood(X1)
& city(X1)
& event(X2)
& street(X3)
& way(X3)
& lonely(X3)
& chevy(X4)
& car(X4)
& white(X4)
& dirty(X4)
& old(X4)
& barrel(X2,X4)
& down(X2,X3)
& in(X2,X1)
& seat(X7)
& furniture(X7)
& front(X7)
& X5 != X6
& fellow(X5)
& man(X5)
& young(X5)
& fellow(X6)
& man(X6)
& young(X6)
& X5 = X8
& in(X8,X7)
& X6 = X9
& in(X9,X7) )
& ! [X10,X11,X12,X13,X14,X15,X16,X17,X18] :
( ~ hollywood(X10)
| ~ city(X10)
| ~ event(X11)
| ~ chevy(X12)
| ~ car(X12)
| ~ white(X12)
| ~ dirty(X12)
| ~ old(X12)
| ~ street(X13)
| ~ way(X13)
| ~ lonely(X13)
| ~ barrel(X11,X12)
| ~ down(X11,X13)
| ~ in(X11,X10)
| ~ seat(X16)
| ~ furniture(X16)
| ~ front(X16)
| X14 = X15
| ~ fellow(X14)
| ~ man(X14)
| ~ young(X14)
| ~ fellow(X15)
| ~ man(X15)
| ~ young(X15)
| X14 != X17
| ~ in(X17,X16)
| X15 != X18
| ~ in(X18,X16) ) )
| epred1_0 ),
inference(fof_nnf,[status(thm)],[3]) ).
fof(9,plain,
( ( ? [X19,X20,X21,X22,X23,X24,X25,X26,X27] :
( hollywood(X19)
& city(X19)
& event(X20)
& street(X21)
& way(X21)
& lonely(X21)
& chevy(X22)
& car(X22)
& white(X22)
& dirty(X22)
& old(X22)
& barrel(X20,X22)
& down(X20,X21)
& in(X20,X19)
& seat(X25)
& furniture(X25)
& front(X25)
& X23 != X24
& fellow(X23)
& man(X23)
& young(X23)
& fellow(X24)
& man(X24)
& young(X24)
& X23 = X26
& in(X26,X25)
& X24 = X27
& in(X27,X25) )
& ! [X28,X29,X30,X31,X32,X33,X34,X35,X36] :
( ~ hollywood(X28)
| ~ city(X28)
| ~ event(X29)
| ~ chevy(X30)
| ~ car(X30)
| ~ white(X30)
| ~ dirty(X30)
| ~ old(X30)
| ~ street(X31)
| ~ way(X31)
| ~ lonely(X31)
| ~ barrel(X29,X30)
| ~ down(X29,X31)
| ~ in(X29,X28)
| ~ seat(X34)
| ~ furniture(X34)
| ~ front(X34)
| X32 = X33
| ~ fellow(X32)
| ~ man(X32)
| ~ young(X32)
| ~ fellow(X33)
| ~ man(X33)
| ~ young(X33)
| X32 != X35
| ~ in(X35,X34)
| X33 != X36
| ~ in(X36,X34) ) )
| epred1_0 ),
inference(variable_rename,[status(thm)],[8]) ).
fof(10,plain,
( ( hollywood(esk1_0)
& city(esk1_0)
& event(esk2_0)
& street(esk3_0)
& way(esk3_0)
& lonely(esk3_0)
& chevy(esk4_0)
& car(esk4_0)
& white(esk4_0)
& dirty(esk4_0)
& old(esk4_0)
& barrel(esk2_0,esk4_0)
& down(esk2_0,esk3_0)
& in(esk2_0,esk1_0)
& seat(esk7_0)
& furniture(esk7_0)
& front(esk7_0)
& esk5_0 != esk6_0
& fellow(esk5_0)
& man(esk5_0)
& young(esk5_0)
& fellow(esk6_0)
& man(esk6_0)
& young(esk6_0)
& esk5_0 = esk8_0
& in(esk8_0,esk7_0)
& esk6_0 = esk9_0
& in(esk9_0,esk7_0)
& ! [X28,X29,X30,X31,X32,X33,X34,X35,X36] :
( ~ hollywood(X28)
| ~ city(X28)
| ~ event(X29)
| ~ chevy(X30)
| ~ car(X30)
| ~ white(X30)
| ~ dirty(X30)
| ~ old(X30)
| ~ street(X31)
| ~ way(X31)
| ~ lonely(X31)
| ~ barrel(X29,X30)
| ~ down(X29,X31)
| ~ in(X29,X28)
| ~ seat(X34)
| ~ furniture(X34)
| ~ front(X34)
| X32 = X33
| ~ fellow(X32)
| ~ man(X32)
| ~ young(X32)
| ~ fellow(X33)
| ~ man(X33)
| ~ young(X33)
| X32 != X35
| ~ in(X35,X34)
| X33 != X36
| ~ in(X36,X34) ) )
| epred1_0 ),
inference(skolemize,[status(esa)],[9]) ).
fof(11,plain,
! [X28,X29,X30,X31,X32,X33,X34,X35,X36] :
( ( ( ~ hollywood(X28)
| ~ city(X28)
| ~ event(X29)
| ~ chevy(X30)
| ~ car(X30)
| ~ white(X30)
| ~ dirty(X30)
| ~ old(X30)
| ~ street(X31)
| ~ way(X31)
| ~ lonely(X31)
| ~ barrel(X29,X30)
| ~ down(X29,X31)
| ~ in(X29,X28)
| ~ seat(X34)
| ~ furniture(X34)
| ~ front(X34)
| X32 = X33
| ~ fellow(X32)
| ~ man(X32)
| ~ young(X32)
| ~ fellow(X33)
| ~ man(X33)
| ~ young(X33)
| X32 != X35
| ~ in(X35,X34)
| X33 != X36
| ~ in(X36,X34) )
& hollywood(esk1_0)
& city(esk1_0)
& event(esk2_0)
& street(esk3_0)
& way(esk3_0)
& lonely(esk3_0)
& chevy(esk4_0)
& car(esk4_0)
& white(esk4_0)
& dirty(esk4_0)
& old(esk4_0)
& barrel(esk2_0,esk4_0)
& down(esk2_0,esk3_0)
& in(esk2_0,esk1_0)
& seat(esk7_0)
& furniture(esk7_0)
& front(esk7_0)
& esk5_0 != esk6_0
& fellow(esk5_0)
& man(esk5_0)
& young(esk5_0)
& fellow(esk6_0)
& man(esk6_0)
& young(esk6_0)
& esk5_0 = esk8_0
& in(esk8_0,esk7_0)
& esk6_0 = esk9_0
& in(esk9_0,esk7_0) )
| epred1_0 ),
inference(shift_quantors,[status(thm)],[10]) ).
fof(12,plain,
! [X28,X29,X30,X31,X32,X33,X34,X35,X36] :
( ( ~ hollywood(X28)
| ~ city(X28)
| ~ event(X29)
| ~ chevy(X30)
| ~ car(X30)
| ~ white(X30)
| ~ dirty(X30)
| ~ old(X30)
| ~ street(X31)
| ~ way(X31)
| ~ lonely(X31)
| ~ barrel(X29,X30)
| ~ down(X29,X31)
| ~ in(X29,X28)
| ~ seat(X34)
| ~ furniture(X34)
| ~ front(X34)
| X32 = X33
| ~ fellow(X32)
| ~ man(X32)
| ~ young(X32)
| ~ fellow(X33)
| ~ man(X33)
| ~ young(X33)
| X32 != X35
| ~ in(X35,X34)
| X33 != X36
| ~ in(X36,X34)
| epred1_0 )
& ( hollywood(esk1_0)
| epred1_0 )
& ( city(esk1_0)
| epred1_0 )
& ( event(esk2_0)
| epred1_0 )
& ( street(esk3_0)
| epred1_0 )
& ( way(esk3_0)
| epred1_0 )
& ( lonely(esk3_0)
| epred1_0 )
& ( chevy(esk4_0)
| epred1_0 )
& ( car(esk4_0)
| epred1_0 )
& ( white(esk4_0)
| epred1_0 )
& ( dirty(esk4_0)
| epred1_0 )
& ( old(esk4_0)
| epred1_0 )
& ( barrel(esk2_0,esk4_0)
| epred1_0 )
& ( down(esk2_0,esk3_0)
| epred1_0 )
& ( in(esk2_0,esk1_0)
| epred1_0 )
& ( seat(esk7_0)
| epred1_0 )
& ( furniture(esk7_0)
| epred1_0 )
& ( front(esk7_0)
| epred1_0 )
& ( esk5_0 != esk6_0
| epred1_0 )
& ( fellow(esk5_0)
| epred1_0 )
& ( man(esk5_0)
| epred1_0 )
& ( young(esk5_0)
| epred1_0 )
& ( fellow(esk6_0)
| epred1_0 )
& ( man(esk6_0)
| epred1_0 )
& ( young(esk6_0)
| epred1_0 )
& ( esk5_0 = esk8_0
| epred1_0 )
& ( in(esk8_0,esk7_0)
| epred1_0 )
& ( esk6_0 = esk9_0
| epred1_0 )
& ( in(esk9_0,esk7_0)
| epred1_0 ) ),
inference(distribute,[status(thm)],[11]) ).
cnf(13,plain,
( epred1_0
| in(esk9_0,esk7_0) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(14,plain,
( epred1_0
| esk6_0 = esk9_0 ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(15,plain,
( epred1_0
| in(esk8_0,esk7_0) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(16,plain,
( epred1_0
| esk5_0 = esk8_0 ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(17,plain,
( epred1_0
| young(esk6_0) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(18,plain,
( epred1_0
| man(esk6_0) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(19,plain,
( epred1_0
| fellow(esk6_0) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(20,plain,
( epred1_0
| young(esk5_0) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(21,plain,
( epred1_0
| man(esk5_0) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(22,plain,
( epred1_0
| fellow(esk5_0) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(23,plain,
( epred1_0
| esk5_0 != esk6_0 ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(24,plain,
( epred1_0
| front(esk7_0) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(25,plain,
( epred1_0
| furniture(esk7_0) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(26,plain,
( epred1_0
| seat(esk7_0) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(27,plain,
( epred1_0
| in(esk2_0,esk1_0) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(28,plain,
( epred1_0
| down(esk2_0,esk3_0) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(29,plain,
( epred1_0
| barrel(esk2_0,esk4_0) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(30,plain,
( epred1_0
| old(esk4_0) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(31,plain,
( epred1_0
| dirty(esk4_0) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(32,plain,
( epred1_0
| white(esk4_0) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(33,plain,
( epred1_0
| car(esk4_0) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(34,plain,
( epred1_0
| chevy(esk4_0) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(35,plain,
( epred1_0
| lonely(esk3_0) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(36,plain,
( epred1_0
| way(esk3_0) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(37,plain,
( epred1_0
| street(esk3_0) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(38,plain,
( epred1_0
| event(esk2_0) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(39,plain,
( epred1_0
| city(esk1_0) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(40,plain,
( epred1_0
| hollywood(esk1_0) ),
inference(split_conjunct,[status(thm)],[12]) ).
cnf(41,plain,
( epred1_0
| X5 = X3
| ~ in(X1,X2)
| X3 != X1
| ~ in(X4,X2)
| X5 != X4
| ~ young(X3)
| ~ man(X3)
| ~ fellow(X3)
| ~ young(X5)
| ~ man(X5)
| ~ fellow(X5)
| ~ front(X2)
| ~ furniture(X2)
| ~ seat(X2)
| ~ in(X6,X7)
| ~ down(X6,X8)
| ~ barrel(X6,X9)
| ~ lonely(X8)
| ~ way(X8)
| ~ street(X8)
| ~ old(X9)
| ~ dirty(X9)
| ~ white(X9)
| ~ car(X9)
| ~ chevy(X9)
| ~ event(X6)
| ~ city(X7)
| ~ hollywood(X7) ),
inference(split_conjunct,[status(thm)],[12]) ).
fof(42,plain,
( ( ? [X19,X20,X21,X22,X23,X24,X25,X26,X27] :
( hollywood(X19)
& city(X19)
& event(X20)
& chevy(X21)
& car(X21)
& white(X21)
& dirty(X21)
& old(X21)
& street(X22)
& way(X22)
& lonely(X22)
& barrel(X20,X21)
& down(X20,X22)
& in(X20,X19)
& seat(X25)
& furniture(X25)
& front(X25)
& X23 != X24
& fellow(X23)
& man(X23)
& young(X23)
& fellow(X24)
& man(X24)
& young(X24)
& X23 = X26
& in(X26,X25)
& X24 = X27
& in(X27,X25) )
& ! [X28,X29,X30,X31,X32,X33,X34,X35,X36] :
( ~ hollywood(X28)
| ~ city(X28)
| ~ event(X29)
| ~ street(X30)
| ~ way(X30)
| ~ lonely(X30)
| ~ chevy(X31)
| ~ car(X31)
| ~ white(X31)
| ~ dirty(X31)
| ~ old(X31)
| ~ barrel(X29,X31)
| ~ down(X29,X30)
| ~ in(X29,X28)
| ~ seat(X34)
| ~ furniture(X34)
| ~ front(X34)
| X32 = X33
| ~ fellow(X32)
| ~ man(X32)
| ~ young(X32)
| ~ fellow(X33)
| ~ man(X33)
| ~ young(X33)
| X32 != X35
| ~ in(X35,X34)
| X33 != X36
| ~ in(X36,X34) ) )
| epred2_0 ),
inference(fof_nnf,[status(thm)],[4]) ).
fof(43,plain,
( ( ? [X37,X38,X39,X40,X41,X42,X43,X44,X45] :
( hollywood(X37)
& city(X37)
& event(X38)
& chevy(X39)
& car(X39)
& white(X39)
& dirty(X39)
& old(X39)
& street(X40)
& way(X40)
& lonely(X40)
& barrel(X38,X39)
& down(X38,X40)
& in(X38,X37)
& seat(X43)
& furniture(X43)
& front(X43)
& X41 != X42
& fellow(X41)
& man(X41)
& young(X41)
& fellow(X42)
& man(X42)
& young(X42)
& X41 = X44
& in(X44,X43)
& X42 = X45
& in(X45,X43) )
& ! [X46,X47,X48,X49,X50,X51,X52,X53,X54] :
( ~ hollywood(X46)
| ~ city(X46)
| ~ event(X47)
| ~ street(X48)
| ~ way(X48)
| ~ lonely(X48)
| ~ chevy(X49)
| ~ car(X49)
| ~ white(X49)
| ~ dirty(X49)
| ~ old(X49)
| ~ barrel(X47,X49)
| ~ down(X47,X48)
| ~ in(X47,X46)
| ~ seat(X52)
| ~ furniture(X52)
| ~ front(X52)
| X50 = X51
| ~ fellow(X50)
| ~ man(X50)
| ~ young(X50)
| ~ fellow(X51)
| ~ man(X51)
| ~ young(X51)
| X50 != X53
| ~ in(X53,X52)
| X51 != X54
| ~ in(X54,X52) ) )
| epred2_0 ),
inference(variable_rename,[status(thm)],[42]) ).
fof(44,plain,
( ( hollywood(esk10_0)
& city(esk10_0)
& event(esk11_0)
& chevy(esk12_0)
& car(esk12_0)
& white(esk12_0)
& dirty(esk12_0)
& old(esk12_0)
& street(esk13_0)
& way(esk13_0)
& lonely(esk13_0)
& barrel(esk11_0,esk12_0)
& down(esk11_0,esk13_0)
& in(esk11_0,esk10_0)
& seat(esk16_0)
& furniture(esk16_0)
& front(esk16_0)
& esk14_0 != esk15_0
& fellow(esk14_0)
& man(esk14_0)
& young(esk14_0)
& fellow(esk15_0)
& man(esk15_0)
& young(esk15_0)
& esk14_0 = esk17_0
& in(esk17_0,esk16_0)
& esk15_0 = esk18_0
& in(esk18_0,esk16_0)
& ! [X46,X47,X48,X49,X50,X51,X52,X53,X54] :
( ~ hollywood(X46)
| ~ city(X46)
| ~ event(X47)
| ~ street(X48)
| ~ way(X48)
| ~ lonely(X48)
| ~ chevy(X49)
| ~ car(X49)
| ~ white(X49)
| ~ dirty(X49)
| ~ old(X49)
| ~ barrel(X47,X49)
| ~ down(X47,X48)
| ~ in(X47,X46)
| ~ seat(X52)
| ~ furniture(X52)
| ~ front(X52)
| X50 = X51
| ~ fellow(X50)
| ~ man(X50)
| ~ young(X50)
| ~ fellow(X51)
| ~ man(X51)
| ~ young(X51)
| X50 != X53
| ~ in(X53,X52)
| X51 != X54
| ~ in(X54,X52) ) )
| epred2_0 ),
inference(skolemize,[status(esa)],[43]) ).
fof(45,plain,
! [X46,X47,X48,X49,X50,X51,X52,X53,X54] :
( ( ( ~ hollywood(X46)
| ~ city(X46)
| ~ event(X47)
| ~ street(X48)
| ~ way(X48)
| ~ lonely(X48)
| ~ chevy(X49)
| ~ car(X49)
| ~ white(X49)
| ~ dirty(X49)
| ~ old(X49)
| ~ barrel(X47,X49)
| ~ down(X47,X48)
| ~ in(X47,X46)
| ~ seat(X52)
| ~ furniture(X52)
| ~ front(X52)
| X50 = X51
| ~ fellow(X50)
| ~ man(X50)
| ~ young(X50)
| ~ fellow(X51)
| ~ man(X51)
| ~ young(X51)
| X50 != X53
| ~ in(X53,X52)
| X51 != X54
| ~ in(X54,X52) )
& hollywood(esk10_0)
& city(esk10_0)
& event(esk11_0)
& chevy(esk12_0)
& car(esk12_0)
& white(esk12_0)
& dirty(esk12_0)
& old(esk12_0)
& street(esk13_0)
& way(esk13_0)
& lonely(esk13_0)
& barrel(esk11_0,esk12_0)
& down(esk11_0,esk13_0)
& in(esk11_0,esk10_0)
& seat(esk16_0)
& furniture(esk16_0)
& front(esk16_0)
& esk14_0 != esk15_0
& fellow(esk14_0)
& man(esk14_0)
& young(esk14_0)
& fellow(esk15_0)
& man(esk15_0)
& young(esk15_0)
& esk14_0 = esk17_0
& in(esk17_0,esk16_0)
& esk15_0 = esk18_0
& in(esk18_0,esk16_0) )
| epred2_0 ),
inference(shift_quantors,[status(thm)],[44]) ).
fof(46,plain,
! [X46,X47,X48,X49,X50,X51,X52,X53,X54] :
( ( ~ hollywood(X46)
| ~ city(X46)
| ~ event(X47)
| ~ street(X48)
| ~ way(X48)
| ~ lonely(X48)
| ~ chevy(X49)
| ~ car(X49)
| ~ white(X49)
| ~ dirty(X49)
| ~ old(X49)
| ~ barrel(X47,X49)
| ~ down(X47,X48)
| ~ in(X47,X46)
| ~ seat(X52)
| ~ furniture(X52)
| ~ front(X52)
| X50 = X51
| ~ fellow(X50)
| ~ man(X50)
| ~ young(X50)
| ~ fellow(X51)
| ~ man(X51)
| ~ young(X51)
| X50 != X53
| ~ in(X53,X52)
| X51 != X54
| ~ in(X54,X52)
| epred2_0 )
& ( hollywood(esk10_0)
| epred2_0 )
& ( city(esk10_0)
| epred2_0 )
& ( event(esk11_0)
| epred2_0 )
& ( chevy(esk12_0)
| epred2_0 )
& ( car(esk12_0)
| epred2_0 )
& ( white(esk12_0)
| epred2_0 )
& ( dirty(esk12_0)
| epred2_0 )
& ( old(esk12_0)
| epred2_0 )
& ( street(esk13_0)
| epred2_0 )
& ( way(esk13_0)
| epred2_0 )
& ( lonely(esk13_0)
| epred2_0 )
& ( barrel(esk11_0,esk12_0)
| epred2_0 )
& ( down(esk11_0,esk13_0)
| epred2_0 )
& ( in(esk11_0,esk10_0)
| epred2_0 )
& ( seat(esk16_0)
| epred2_0 )
& ( furniture(esk16_0)
| epred2_0 )
& ( front(esk16_0)
| epred2_0 )
& ( esk14_0 != esk15_0
| epred2_0 )
& ( fellow(esk14_0)
| epred2_0 )
& ( man(esk14_0)
| epred2_0 )
& ( young(esk14_0)
| epred2_0 )
& ( fellow(esk15_0)
| epred2_0 )
& ( man(esk15_0)
| epred2_0 )
& ( young(esk15_0)
| epred2_0 )
& ( esk14_0 = esk17_0
| epred2_0 )
& ( in(esk17_0,esk16_0)
| epred2_0 )
& ( esk15_0 = esk18_0
| epred2_0 )
& ( in(esk18_0,esk16_0)
| epred2_0 ) ),
inference(distribute,[status(thm)],[45]) ).
cnf(47,plain,
( epred2_0
| in(esk18_0,esk16_0) ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(48,plain,
( epred2_0
| esk15_0 = esk18_0 ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(49,plain,
( epred2_0
| in(esk17_0,esk16_0) ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(50,plain,
( epred2_0
| esk14_0 = esk17_0 ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(51,plain,
( epred2_0
| young(esk15_0) ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(52,plain,
( epred2_0
| man(esk15_0) ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(53,plain,
( epred2_0
| fellow(esk15_0) ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(54,plain,
( epred2_0
| young(esk14_0) ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(55,plain,
( epred2_0
| man(esk14_0) ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(56,plain,
( epred2_0
| fellow(esk14_0) ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(57,plain,
( epred2_0
| esk14_0 != esk15_0 ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(58,plain,
( epred2_0
| front(esk16_0) ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(59,plain,
( epred2_0
| furniture(esk16_0) ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(60,plain,
( epred2_0
| seat(esk16_0) ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(61,plain,
( epred2_0
| in(esk11_0,esk10_0) ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(62,plain,
( epred2_0
| down(esk11_0,esk13_0) ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(63,plain,
( epred2_0
| barrel(esk11_0,esk12_0) ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(64,plain,
( epred2_0
| lonely(esk13_0) ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(65,plain,
( epred2_0
| way(esk13_0) ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(66,plain,
( epred2_0
| street(esk13_0) ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(67,plain,
( epred2_0
| old(esk12_0) ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(68,plain,
( epred2_0
| dirty(esk12_0) ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(69,plain,
( epred2_0
| white(esk12_0) ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(70,plain,
( epred2_0
| car(esk12_0) ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(71,plain,
( epred2_0
| chevy(esk12_0) ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(72,plain,
( epred2_0
| event(esk11_0) ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(73,plain,
( epred2_0
| city(esk10_0) ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(74,plain,
( epred2_0
| hollywood(esk10_0) ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(75,plain,
( epred2_0
| X5 = X3
| ~ in(X1,X2)
| X3 != X1
| ~ in(X4,X2)
| X5 != X4
| ~ young(X3)
| ~ man(X3)
| ~ fellow(X3)
| ~ young(X5)
| ~ man(X5)
| ~ fellow(X5)
| ~ front(X2)
| ~ furniture(X2)
| ~ seat(X2)
| ~ in(X6,X7)
| ~ down(X6,X8)
| ~ barrel(X6,X9)
| ~ old(X9)
| ~ dirty(X9)
| ~ white(X9)
| ~ car(X9)
| ~ chevy(X9)
| ~ lonely(X8)
| ~ way(X8)
| ~ street(X8)
| ~ event(X6)
| ~ city(X7)
| ~ hollywood(X7) ),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(77,plain,
( epred1_0
| in(esk6_0,esk7_0) ),
inference(spm,[status(thm)],[13,14,theory(equality)]) ).
cnf(80,plain,
( X1 = X2
| epred1_0
| X3 != X1
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X4)
| ~ furniture(X4)
| ~ seat(X4)
| ~ in(X5,X6)
| ~ in(X2,X4)
| ~ in(X3,X4)
| ~ down(X5,X7)
| ~ barrel(X5,X8)
| ~ old(X8)
| ~ dirty(X8)
| ~ white(X8)
| ~ car(X8)
| ~ chevy(X8)
| ~ lonely(X7)
| ~ way(X7)
| ~ street(X7)
| ~ event(X5)
| ~ city(X6)
| ~ hollywood(X6) ),
inference(er,[status(thm)],[41,theory(equality)]) ).
cnf(81,plain,
( X1 = X2
| epred1_0
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X4,X5)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ down(X4,X6)
| ~ barrel(X4,X7)
| ~ old(X7)
| ~ dirty(X7)
| ~ white(X7)
| ~ car(X7)
| ~ chevy(X7)
| ~ lonely(X6)
| ~ way(X6)
| ~ street(X6)
| ~ event(X4)
| ~ city(X5)
| ~ hollywood(X5) ),
inference(er,[status(thm)],[80,theory(equality)]) ).
cnf(82,plain,
( X1 = X2
| epred2_0
| X3 != X1
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X4)
| ~ furniture(X4)
| ~ seat(X4)
| ~ in(X5,X6)
| ~ in(X2,X4)
| ~ in(X3,X4)
| ~ down(X5,X7)
| ~ barrel(X5,X8)
| ~ old(X8)
| ~ dirty(X8)
| ~ white(X8)
| ~ car(X8)
| ~ chevy(X8)
| ~ lonely(X7)
| ~ way(X7)
| ~ street(X7)
| ~ event(X5)
| ~ city(X6)
| ~ hollywood(X6) ),
inference(er,[status(thm)],[75,theory(equality)]) ).
cnf(83,plain,
( X1 = X2
| epred2_0
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X4,X5)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ down(X4,X6)
| ~ barrel(X4,X7)
| ~ old(X7)
| ~ dirty(X7)
| ~ white(X7)
| ~ car(X7)
| ~ chevy(X7)
| ~ lonely(X6)
| ~ way(X6)
| ~ street(X6)
| ~ event(X4)
| ~ city(X5)
| ~ hollywood(X5) ),
inference(er,[status(thm)],[82,theory(equality)]) ).
cnf(84,plain,
( X1 = X2
| epred1_0
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ down(esk2_0,X4)
| ~ barrel(esk2_0,X5)
| ~ old(X5)
| ~ dirty(X5)
| ~ white(X5)
| ~ car(X5)
| ~ chevy(X5)
| ~ lonely(X4)
| ~ way(X4)
| ~ street(X4)
| ~ event(esk2_0)
| ~ city(esk1_0)
| ~ hollywood(esk1_0) ),
inference(spm,[status(thm)],[81,27,theory(equality)]) ).
cnf(94,plain,
( X1 = X2
| epred1_0
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ down(esk2_0,X4)
| ~ barrel(esk2_0,X5)
| ~ old(X5)
| ~ dirty(X5)
| ~ white(X5)
| ~ car(X5)
| ~ chevy(X5)
| ~ lonely(X4)
| ~ way(X4)
| ~ street(X4)
| ~ event(esk2_0)
| ~ city(esk1_0) ),
inference(csr,[status(thm)],[84,40]) ).
cnf(95,plain,
( X1 = X2
| epred1_0
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ down(esk2_0,X4)
| ~ barrel(esk2_0,X5)
| ~ old(X5)
| ~ dirty(X5)
| ~ white(X5)
| ~ car(X5)
| ~ chevy(X5)
| ~ lonely(X4)
| ~ way(X4)
| ~ street(X4)
| ~ event(esk2_0) ),
inference(csr,[status(thm)],[94,39]) ).
cnf(96,plain,
( X1 = X2
| epred1_0
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ down(esk2_0,X4)
| ~ barrel(esk2_0,X5)
| ~ old(X5)
| ~ dirty(X5)
| ~ white(X5)
| ~ car(X5)
| ~ chevy(X5)
| ~ lonely(X4)
| ~ way(X4)
| ~ street(X4) ),
inference(csr,[status(thm)],[95,38]) ).
cnf(97,plain,
( X1 = X2
| epred1_0
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ barrel(esk2_0,X4)
| ~ old(X4)
| ~ dirty(X4)
| ~ white(X4)
| ~ car(X4)
| ~ chevy(X4)
| ~ lonely(esk3_0)
| ~ way(esk3_0)
| ~ street(esk3_0) ),
inference(spm,[status(thm)],[96,28,theory(equality)]) ).
cnf(98,plain,
( X1 = X2
| epred1_0
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ barrel(esk2_0,X4)
| ~ old(X4)
| ~ dirty(X4)
| ~ white(X4)
| ~ car(X4)
| ~ chevy(X4)
| ~ lonely(esk3_0)
| ~ way(esk3_0) ),
inference(csr,[status(thm)],[97,37]) ).
cnf(99,plain,
( X1 = X2
| epred1_0
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ barrel(esk2_0,X4)
| ~ old(X4)
| ~ dirty(X4)
| ~ white(X4)
| ~ car(X4)
| ~ chevy(X4)
| ~ lonely(esk3_0) ),
inference(csr,[status(thm)],[98,36]) ).
cnf(100,plain,
( X1 = X2
| epred1_0
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ barrel(esk2_0,X4)
| ~ old(X4)
| ~ dirty(X4)
| ~ white(X4)
| ~ car(X4)
| ~ chevy(X4) ),
inference(csr,[status(thm)],[99,35]) ).
cnf(101,plain,
( X1 = X2
| epred1_0
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ old(esk4_0)
| ~ dirty(esk4_0)
| ~ white(esk4_0)
| ~ car(esk4_0)
| ~ chevy(esk4_0) ),
inference(spm,[status(thm)],[100,29,theory(equality)]) ).
cnf(102,plain,
( X1 = X2
| epred1_0
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ old(esk4_0)
| ~ dirty(esk4_0)
| ~ white(esk4_0)
| ~ car(esk4_0) ),
inference(csr,[status(thm)],[101,34]) ).
cnf(103,plain,
( X1 = X2
| epred1_0
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ old(esk4_0)
| ~ dirty(esk4_0)
| ~ white(esk4_0) ),
inference(csr,[status(thm)],[102,33]) ).
cnf(104,plain,
( X1 = X2
| epred1_0
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ old(esk4_0)
| ~ dirty(esk4_0) ),
inference(csr,[status(thm)],[103,32]) ).
cnf(105,plain,
( X1 = X2
| epred1_0
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ old(esk4_0) ),
inference(csr,[status(thm)],[104,31]) ).
cnf(106,plain,
( X1 = X2
| epred1_0
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3) ),
inference(csr,[status(thm)],[105,30]) ).
cnf(108,plain,
( X1 = esk8_0
| epred1_0
| ~ young(esk8_0)
| ~ young(X1)
| ~ man(esk8_0)
| ~ man(X1)
| ~ fellow(esk8_0)
| ~ fellow(X1)
| ~ front(esk7_0)
| ~ furniture(esk7_0)
| ~ seat(esk7_0)
| ~ in(X1,esk7_0) ),
inference(spm,[status(thm)],[106,15,theory(equality)]) ).
cnf(117,plain,
( X1 = esk8_0
| epred1_0
| ~ young(esk8_0)
| ~ young(X1)
| ~ man(esk8_0)
| ~ man(X1)
| ~ fellow(esk8_0)
| ~ fellow(X1)
| ~ front(esk7_0)
| ~ furniture(esk7_0)
| ~ in(X1,esk7_0) ),
inference(csr,[status(thm)],[108,26]) ).
cnf(118,plain,
( X1 = esk8_0
| epred1_0
| ~ young(esk8_0)
| ~ young(X1)
| ~ man(esk8_0)
| ~ man(X1)
| ~ fellow(esk8_0)
| ~ fellow(X1)
| ~ front(esk7_0)
| ~ in(X1,esk7_0) ),
inference(csr,[status(thm)],[117,25]) ).
cnf(119,plain,
( X1 = esk8_0
| epred1_0
| ~ young(esk8_0)
| ~ young(X1)
| ~ man(esk8_0)
| ~ man(X1)
| ~ fellow(esk8_0)
| ~ fellow(X1)
| ~ in(X1,esk7_0) ),
inference(csr,[status(thm)],[118,24]) ).
cnf(120,plain,
( X1 = esk5_0
| epred1_0
| ~ young(esk5_0)
| ~ young(X1)
| ~ man(esk5_0)
| ~ man(X1)
| ~ fellow(esk5_0)
| ~ fellow(X1)
| ~ in(X1,esk7_0) ),
inference(spm,[status(thm)],[119,16,theory(equality)]) ).
cnf(121,plain,
( X1 = esk5_0
| epred1_0
| ~ young(esk5_0)
| ~ young(X1)
| ~ man(esk5_0)
| ~ man(X1)
| ~ fellow(X1)
| ~ in(X1,esk7_0) ),
inference(csr,[status(thm)],[120,22]) ).
cnf(122,plain,
( X1 = esk5_0
| epred1_0
| ~ young(esk5_0)
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ in(X1,esk7_0) ),
inference(csr,[status(thm)],[121,21]) ).
cnf(123,plain,
( X1 = esk5_0
| epred1_0
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ in(X1,esk7_0) ),
inference(csr,[status(thm)],[122,20]) ).
cnf(124,plain,
( esk6_0 = esk5_0
| epred1_0
| ~ man(esk6_0)
| ~ fellow(esk6_0)
| ~ in(esk6_0,esk7_0) ),
inference(spm,[status(thm)],[123,17,theory(equality)]) ).
cnf(127,plain,
( esk6_0 = esk5_0
| epred1_0
| ~ man(esk6_0)
| ~ fellow(esk6_0) ),
inference(csr,[status(thm)],[124,77]) ).
cnf(128,plain,
( esk6_0 = esk5_0
| epred1_0
| ~ man(esk6_0) ),
inference(csr,[status(thm)],[127,19]) ).
cnf(129,plain,
( esk6_0 = esk5_0
| epred1_0 ),
inference(csr,[status(thm)],[128,18]) ).
cnf(130,plain,
epred1_0,
inference(csr,[status(thm)],[129,23]) ).
cnf(165,negated_conjecture,
( ~ epred2_0
| $false ),
inference(rw,[status(thm)],[7,130,theory(equality)]) ).
cnf(166,negated_conjecture,
~ epred2_0,
inference(cn,[status(thm)],[165,theory(equality)]) ).
cnf(167,plain,
esk17_0 = esk14_0,
inference(sr,[status(thm)],[50,166,theory(equality)]) ).
cnf(168,plain,
esk18_0 = esk15_0,
inference(sr,[status(thm)],[48,166,theory(equality)]) ).
cnf(169,plain,
hollywood(esk10_0),
inference(sr,[status(thm)],[74,166,theory(equality)]) ).
cnf(170,plain,
city(esk10_0),
inference(sr,[status(thm)],[73,166,theory(equality)]) ).
cnf(171,plain,
event(esk11_0),
inference(sr,[status(thm)],[72,166,theory(equality)]) ).
cnf(172,plain,
street(esk13_0),
inference(sr,[status(thm)],[66,166,theory(equality)]) ).
cnf(173,plain,
way(esk13_0),
inference(sr,[status(thm)],[65,166,theory(equality)]) ).
cnf(174,plain,
lonely(esk13_0),
inference(sr,[status(thm)],[64,166,theory(equality)]) ).
cnf(175,plain,
chevy(esk12_0),
inference(sr,[status(thm)],[71,166,theory(equality)]) ).
cnf(176,plain,
car(esk12_0),
inference(sr,[status(thm)],[70,166,theory(equality)]) ).
cnf(177,plain,
white(esk12_0),
inference(sr,[status(thm)],[69,166,theory(equality)]) ).
cnf(178,plain,
dirty(esk12_0),
inference(sr,[status(thm)],[68,166,theory(equality)]) ).
cnf(179,plain,
old(esk12_0),
inference(sr,[status(thm)],[67,166,theory(equality)]) ).
cnf(180,plain,
seat(esk16_0),
inference(sr,[status(thm)],[60,166,theory(equality)]) ).
cnf(181,plain,
furniture(esk16_0),
inference(sr,[status(thm)],[59,166,theory(equality)]) ).
cnf(182,plain,
front(esk16_0),
inference(sr,[status(thm)],[58,166,theory(equality)]) ).
cnf(183,plain,
fellow(esk14_0),
inference(sr,[status(thm)],[56,166,theory(equality)]) ).
cnf(184,plain,
fellow(esk15_0),
inference(sr,[status(thm)],[53,166,theory(equality)]) ).
cnf(185,plain,
man(esk14_0),
inference(sr,[status(thm)],[55,166,theory(equality)]) ).
cnf(186,plain,
man(esk15_0),
inference(sr,[status(thm)],[52,166,theory(equality)]) ).
cnf(187,plain,
young(esk14_0),
inference(sr,[status(thm)],[54,166,theory(equality)]) ).
cnf(188,plain,
young(esk15_0),
inference(sr,[status(thm)],[51,166,theory(equality)]) ).
cnf(189,plain,
barrel(esk11_0,esk12_0),
inference(sr,[status(thm)],[63,166,theory(equality)]) ).
cnf(190,plain,
down(esk11_0,esk13_0),
inference(sr,[status(thm)],[62,166,theory(equality)]) ).
cnf(191,plain,
in(esk11_0,esk10_0),
inference(sr,[status(thm)],[61,166,theory(equality)]) ).
cnf(192,plain,
in(esk17_0,esk16_0),
inference(sr,[status(thm)],[49,166,theory(equality)]) ).
cnf(193,plain,
in(esk18_0,esk16_0),
inference(sr,[status(thm)],[47,166,theory(equality)]) ).
cnf(196,plain,
in(esk14_0,esk16_0),
inference(rw,[status(thm)],[192,167,theory(equality)]) ).
cnf(197,plain,
in(esk15_0,esk16_0),
inference(rw,[status(thm)],[193,168,theory(equality)]) ).
cnf(200,plain,
( X1 = X2
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X4,X5)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ down(X4,X6)
| ~ barrel(X4,X7)
| ~ old(X7)
| ~ dirty(X7)
| ~ white(X7)
| ~ car(X7)
| ~ chevy(X7)
| ~ lonely(X6)
| ~ way(X6)
| ~ street(X6)
| ~ event(X4)
| ~ city(X5)
| ~ hollywood(X5) ),
inference(sr,[status(thm)],[83,166,theory(equality)]) ).
cnf(201,plain,
( X1 = X2
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ down(esk11_0,X4)
| ~ barrel(esk11_0,X5)
| ~ old(X5)
| ~ dirty(X5)
| ~ white(X5)
| ~ car(X5)
| ~ chevy(X5)
| ~ lonely(X4)
| ~ way(X4)
| ~ street(X4)
| ~ event(esk11_0)
| ~ city(esk10_0)
| ~ hollywood(esk10_0) ),
inference(spm,[status(thm)],[200,191,theory(equality)]) ).
cnf(204,plain,
( X1 = X2
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ down(esk11_0,X4)
| ~ barrel(esk11_0,X5)
| ~ old(X5)
| ~ dirty(X5)
| ~ white(X5)
| ~ car(X5)
| ~ chevy(X5)
| ~ lonely(X4)
| ~ way(X4)
| ~ street(X4)
| $false
| ~ city(esk10_0)
| ~ hollywood(esk10_0) ),
inference(rw,[status(thm)],[201,171,theory(equality)]) ).
cnf(205,plain,
( X1 = X2
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ down(esk11_0,X4)
| ~ barrel(esk11_0,X5)
| ~ old(X5)
| ~ dirty(X5)
| ~ white(X5)
| ~ car(X5)
| ~ chevy(X5)
| ~ lonely(X4)
| ~ way(X4)
| ~ street(X4)
| $false
| $false
| ~ hollywood(esk10_0) ),
inference(rw,[status(thm)],[204,170,theory(equality)]) ).
cnf(206,plain,
( X1 = X2
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ down(esk11_0,X4)
| ~ barrel(esk11_0,X5)
| ~ old(X5)
| ~ dirty(X5)
| ~ white(X5)
| ~ car(X5)
| ~ chevy(X5)
| ~ lonely(X4)
| ~ way(X4)
| ~ street(X4)
| $false
| $false
| $false ),
inference(rw,[status(thm)],[205,169,theory(equality)]) ).
cnf(207,plain,
( X1 = X2
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ down(esk11_0,X4)
| ~ barrel(esk11_0,X5)
| ~ old(X5)
| ~ dirty(X5)
| ~ white(X5)
| ~ car(X5)
| ~ chevy(X5)
| ~ lonely(X4)
| ~ way(X4)
| ~ street(X4) ),
inference(cn,[status(thm)],[206,theory(equality)]) ).
cnf(208,plain,
( X1 = X2
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ barrel(esk11_0,X4)
| ~ old(X4)
| ~ dirty(X4)
| ~ white(X4)
| ~ car(X4)
| ~ chevy(X4)
| ~ lonely(esk13_0)
| ~ way(esk13_0)
| ~ street(esk13_0) ),
inference(spm,[status(thm)],[207,190,theory(equality)]) ).
cnf(209,plain,
( X1 = X2
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ barrel(esk11_0,X4)
| ~ old(X4)
| ~ dirty(X4)
| ~ white(X4)
| ~ car(X4)
| ~ chevy(X4)
| $false
| ~ way(esk13_0)
| ~ street(esk13_0) ),
inference(rw,[status(thm)],[208,174,theory(equality)]) ).
cnf(210,plain,
( X1 = X2
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ barrel(esk11_0,X4)
| ~ old(X4)
| ~ dirty(X4)
| ~ white(X4)
| ~ car(X4)
| ~ chevy(X4)
| $false
| $false
| ~ street(esk13_0) ),
inference(rw,[status(thm)],[209,173,theory(equality)]) ).
cnf(211,plain,
( X1 = X2
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ barrel(esk11_0,X4)
| ~ old(X4)
| ~ dirty(X4)
| ~ white(X4)
| ~ car(X4)
| ~ chevy(X4)
| $false
| $false
| $false ),
inference(rw,[status(thm)],[210,172,theory(equality)]) ).
cnf(212,plain,
( X1 = X2
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ barrel(esk11_0,X4)
| ~ old(X4)
| ~ dirty(X4)
| ~ white(X4)
| ~ car(X4)
| ~ chevy(X4) ),
inference(cn,[status(thm)],[211,theory(equality)]) ).
cnf(213,plain,
( X1 = X2
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| ~ old(esk12_0)
| ~ dirty(esk12_0)
| ~ white(esk12_0)
| ~ car(esk12_0)
| ~ chevy(esk12_0) ),
inference(spm,[status(thm)],[212,189,theory(equality)]) ).
cnf(214,plain,
( X1 = X2
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| $false
| ~ dirty(esk12_0)
| ~ white(esk12_0)
| ~ car(esk12_0)
| ~ chevy(esk12_0) ),
inference(rw,[status(thm)],[213,179,theory(equality)]) ).
cnf(215,plain,
( X1 = X2
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| $false
| $false
| ~ white(esk12_0)
| ~ car(esk12_0)
| ~ chevy(esk12_0) ),
inference(rw,[status(thm)],[214,178,theory(equality)]) ).
cnf(216,plain,
( X1 = X2
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| $false
| $false
| $false
| ~ car(esk12_0)
| ~ chevy(esk12_0) ),
inference(rw,[status(thm)],[215,177,theory(equality)]) ).
cnf(217,plain,
( X1 = X2
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| $false
| $false
| $false
| $false
| ~ chevy(esk12_0) ),
inference(rw,[status(thm)],[216,176,theory(equality)]) ).
cnf(218,plain,
( X1 = X2
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3)
| $false
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[217,175,theory(equality)]) ).
cnf(219,plain,
( X1 = X2
| ~ young(X2)
| ~ young(X1)
| ~ man(X2)
| ~ man(X1)
| ~ fellow(X2)
| ~ fellow(X1)
| ~ front(X3)
| ~ furniture(X3)
| ~ seat(X3)
| ~ in(X2,X3)
| ~ in(X1,X3) ),
inference(cn,[status(thm)],[218,theory(equality)]) ).
cnf(221,plain,
( X1 = esk14_0
| ~ young(esk14_0)
| ~ young(X1)
| ~ man(esk14_0)
| ~ man(X1)
| ~ fellow(esk14_0)
| ~ fellow(X1)
| ~ front(esk16_0)
| ~ furniture(esk16_0)
| ~ seat(esk16_0)
| ~ in(X1,esk16_0) ),
inference(spm,[status(thm)],[219,196,theory(equality)]) ).
cnf(223,plain,
( X1 = esk14_0
| $false
| ~ young(X1)
| ~ man(esk14_0)
| ~ man(X1)
| ~ fellow(esk14_0)
| ~ fellow(X1)
| ~ front(esk16_0)
| ~ furniture(esk16_0)
| ~ seat(esk16_0)
| ~ in(X1,esk16_0) ),
inference(rw,[status(thm)],[221,187,theory(equality)]) ).
cnf(224,plain,
( X1 = esk14_0
| $false
| ~ young(X1)
| $false
| ~ man(X1)
| ~ fellow(esk14_0)
| ~ fellow(X1)
| ~ front(esk16_0)
| ~ furniture(esk16_0)
| ~ seat(esk16_0)
| ~ in(X1,esk16_0) ),
inference(rw,[status(thm)],[223,185,theory(equality)]) ).
cnf(225,plain,
( X1 = esk14_0
| $false
| ~ young(X1)
| $false
| ~ man(X1)
| $false
| ~ fellow(X1)
| ~ front(esk16_0)
| ~ furniture(esk16_0)
| ~ seat(esk16_0)
| ~ in(X1,esk16_0) ),
inference(rw,[status(thm)],[224,183,theory(equality)]) ).
cnf(226,plain,
( X1 = esk14_0
| $false
| ~ young(X1)
| $false
| ~ man(X1)
| $false
| ~ fellow(X1)
| $false
| ~ furniture(esk16_0)
| ~ seat(esk16_0)
| ~ in(X1,esk16_0) ),
inference(rw,[status(thm)],[225,182,theory(equality)]) ).
cnf(227,plain,
( X1 = esk14_0
| $false
| ~ young(X1)
| $false
| ~ man(X1)
| $false
| ~ fellow(X1)
| $false
| $false
| ~ seat(esk16_0)
| ~ in(X1,esk16_0) ),
inference(rw,[status(thm)],[226,181,theory(equality)]) ).
cnf(228,plain,
( X1 = esk14_0
| $false
| ~ young(X1)
| $false
| ~ man(X1)
| $false
| ~ fellow(X1)
| $false
| $false
| $false
| ~ in(X1,esk16_0) ),
inference(rw,[status(thm)],[227,180,theory(equality)]) ).
cnf(229,plain,
( X1 = esk14_0
| ~ young(X1)
| ~ man(X1)
| ~ fellow(X1)
| ~ in(X1,esk16_0) ),
inference(cn,[status(thm)],[228,theory(equality)]) ).
cnf(237,plain,
( esk15_0 = esk14_0
| ~ man(esk15_0)
| ~ fellow(esk15_0)
| ~ in(esk15_0,esk16_0) ),
inference(spm,[status(thm)],[229,188,theory(equality)]) ).
cnf(238,plain,
( esk15_0 = esk14_0
| $false
| ~ fellow(esk15_0)
| ~ in(esk15_0,esk16_0) ),
inference(rw,[status(thm)],[237,186,theory(equality)]) ).
cnf(239,plain,
( esk15_0 = esk14_0
| $false
| $false
| ~ in(esk15_0,esk16_0) ),
inference(rw,[status(thm)],[238,184,theory(equality)]) ).
cnf(240,plain,
( esk15_0 = esk14_0
| $false
| $false
| $false ),
inference(rw,[status(thm)],[239,197,theory(equality)]) ).
cnf(241,plain,
esk15_0 = esk14_0,
inference(cn,[status(thm)],[240,theory(equality)]) ).
cnf(252,plain,
( epred2_0
| $false ),
inference(rw,[status(thm)],[57,241,theory(equality)]) ).
cnf(253,plain,
epred2_0,
inference(cn,[status(thm)],[252,theory(equality)]) ).
cnf(254,plain,
$false,
inference(sr,[status(thm)],[253,166,theory(equality)]) ).
cnf(255,plain,
$false,
254,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/NLP/NLP009+1.p
% --creating new selector for []
% -running prover on /tmp/tmpmIEcTk/sel_NLP009+1.p_1 with time limit 29
% -prover status Theorem
% Problem NLP009+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/NLP/NLP009+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/NLP/NLP009+1.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% See solution above
% # SZS output end CNFRefutation
%
%------------------------------------------------------------------------------