%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : NLP009+1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n023.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Mon Jul 18 03:13:44 EDT 2022
% Result : Theorem 0.19s 0.41s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 19
% Syntax : Number of formulae : 245 ( 135 unt; 0 def)
% Number of atoms : 2063 ( 205 equ)
% Maximal formula atoms : 112 ( 8 avg)
% Number of connectives : 3056 (1238 ~;1183 |; 627 &)
% ( 0 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 41 ( 8 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 23 ( 20 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 18 con; 0-0 aty)
% Number of variables : 470 ( 0 sgn 63 !; 189 ?)
% Comments :
%------------------------------------------------------------------------------
fof(co1,conjecture,
( ( ? [U,V,W,X0,Y0,Z,X1,X2,X3] :
( hollywood(U)
& city(U)
& event(V)
& street(W)
& way(W)
& lonely(W)
& chevy(X0)
& car(X0)
& white(X0)
& dirty(X0)
& old(X0)
& barrel(V,X0)
& down(V,W)
& in(V,U)
& seat(X1)
& furniture(X1)
& front(X1)
& Y0 != Z
& fellow(Y0)
& man(Y0)
& young(Y0)
& fellow(Z)
& man(Z)
& young(Z)
& Y0 = X2
& in(X2,X1)
& Z = X3
& in(X3,X1) )
=> ? [X4,X5,X6,X7,X8,X9,X10,X11,X12] :
( hollywood(X4)
& city(X4)
& event(X5)
& chevy(X6)
& car(X6)
& white(X6)
& dirty(X6)
& old(X6)
& street(X7)
& way(X7)
& lonely(X7)
& barrel(X5,X6)
& down(X5,X7)
& in(X5,X4)
& seat(X10)
& furniture(X10)
& front(X10)
& X8 != X9
& fellow(X8)
& man(X8)
& young(X8)
& fellow(X9)
& man(X9)
& young(X9)
& X8 = X11
& in(X11,X10)
& X9 = X12
& in(X12,X10) ) )
& ( ? [X13,X14,X15,X16,X17,X18,X19,X20,X21] :
( hollywood(X13)
& city(X13)
& event(X14)
& chevy(X15)
& car(X15)
& white(X15)
& dirty(X15)
& old(X15)
& street(X16)
& way(X16)
& lonely(X16)
& barrel(X14,X15)
& down(X14,X16)
& in(X14,X13)
& seat(X19)
& furniture(X19)
& front(X19)
& X17 != X18
& fellow(X17)
& man(X17)
& young(X17)
& fellow(X18)
& man(X18)
& young(X18)
& X17 = X20
& in(X20,X19)
& X18 = X21
& in(X21,X19) )
=> ? [X22,X23,X24,X25,X26,X27,X28,X29,X30] :
( hollywood(X22)
& city(X22)
& event(X23)
& street(X24)
& way(X24)
& lonely(X24)
& chevy(X25)
& car(X25)
& white(X25)
& dirty(X25)
& old(X25)
& barrel(X23,X25)
& down(X23,X24)
& in(X23,X22)
& seat(X28)
& furniture(X28)
& front(X28)
& X26 != X27
& fellow(X26)
& man(X26)
& young(X26)
& fellow(X27)
& man(X27)
& young(X27)
& X26 = X29
& in(X29,X28)
& X27 = X30
& in(X30,X28) ) ) ) ).
fof(subgoal_0,plain,
( ? [U,V,W,X0,Y0,Z,X1,X2,X3] :
( hollywood(U)
& city(U)
& event(V)
& street(W)
& way(W)
& lonely(W)
& chevy(X0)
& car(X0)
& white(X0)
& dirty(X0)
& old(X0)
& barrel(V,X0)
& down(V,W)
& in(V,U)
& seat(X1)
& furniture(X1)
& front(X1)
& Y0 != Z
& fellow(Y0)
& man(Y0)
& young(Y0)
& fellow(Z)
& man(Z)
& young(Z)
& Y0 = X2
& in(X2,X1)
& Z = X3
& in(X3,X1) )
=> ? [X4,X5,X6,X7,X8,X9,X10,X11,X12] :
( hollywood(X4)
& city(X4)
& event(X5)
& chevy(X6)
& car(X6)
& white(X6)
& dirty(X6)
& old(X6)
& street(X7)
& way(X7)
& lonely(X7)
& barrel(X5,X6)
& down(X5,X7)
& in(X5,X4)
& seat(X10)
& furniture(X10)
& front(X10)
& X8 != X9
& fellow(X8)
& man(X8)
& young(X8)
& fellow(X9)
& man(X9)
& young(X9)
& X8 = X11
& in(X11,X10)
& X9 = X12
& in(X12,X10) ) ),
inference(strip,[],[co1]) ).
fof(subgoal_1,plain,
( ( ( ? [U,V,W,X0,Y0,Z,X1,X2,X3] :
( hollywood(U)
& city(U)
& event(V)
& street(W)
& way(W)
& lonely(W)
& chevy(X0)
& car(X0)
& white(X0)
& dirty(X0)
& old(X0)
& barrel(V,X0)
& down(V,W)
& in(V,U)
& seat(X1)
& furniture(X1)
& front(X1)
& Y0 != Z
& fellow(Y0)
& man(Y0)
& young(Y0)
& fellow(Z)
& man(Z)
& young(Z)
& Y0 = X2
& in(X2,X1)
& Z = X3
& in(X3,X1) )
=> ? [X4,X5,X6,X7,X8,X9,X10,X11,X12] :
( hollywood(X4)
& city(X4)
& event(X5)
& chevy(X6)
& car(X6)
& white(X6)
& dirty(X6)
& old(X6)
& street(X7)
& way(X7)
& lonely(X7)
& barrel(X5,X6)
& down(X5,X7)
& in(X5,X4)
& seat(X10)
& furniture(X10)
& front(X10)
& X8 != X9
& fellow(X8)
& man(X8)
& young(X8)
& fellow(X9)
& man(X9)
& young(X9)
& X8 = X11
& in(X11,X10)
& X9 = X12
& in(X12,X10) ) )
& ? [X13,X14,X15,X16,X17,X18,X19,X20,X21] :
( hollywood(X13)
& city(X13)
& event(X14)
& chevy(X15)
& car(X15)
& white(X15)
& dirty(X15)
& old(X15)
& street(X16)
& way(X16)
& lonely(X16)
& barrel(X14,X15)
& down(X14,X16)
& in(X14,X13)
& seat(X19)
& furniture(X19)
& front(X19)
& X17 != X18
& fellow(X17)
& man(X17)
& young(X17)
& fellow(X18)
& man(X18)
& young(X18)
& X17 = X20
& in(X20,X19)
& X18 = X21
& in(X21,X19) ) )
=> ? [X22,X23,X24,X25,X26,X27,X28,X29,X30] :
( hollywood(X22)
& city(X22)
& event(X23)
& street(X24)
& way(X24)
& lonely(X24)
& chevy(X25)
& car(X25)
& white(X25)
& dirty(X25)
& old(X25)
& barrel(X23,X25)
& down(X23,X24)
& in(X23,X22)
& seat(X28)
& furniture(X28)
& front(X28)
& X26 != X27
& fellow(X26)
& man(X26)
& young(X26)
& fellow(X27)
& man(X27)
& young(X27)
& X26 = X29
& in(X29,X28)
& X27 = X30
& in(X30,X28) ) ),
inference(strip,[],[co1]) ).
fof(negate_0_0,plain,
~ ( ? [U,V,W,X0,Y0,Z,X1,X2,X3] :
( hollywood(U)
& city(U)
& event(V)
& street(W)
& way(W)
& lonely(W)
& chevy(X0)
& car(X0)
& white(X0)
& dirty(X0)
& old(X0)
& barrel(V,X0)
& down(V,W)
& in(V,U)
& seat(X1)
& furniture(X1)
& front(X1)
& Y0 != Z
& fellow(Y0)
& man(Y0)
& young(Y0)
& fellow(Z)
& man(Z)
& young(Z)
& Y0 = X2
& in(X2,X1)
& Z = X3
& in(X3,X1) )
=> ? [X4,X5,X6,X7,X8,X9,X10,X11,X12] :
( hollywood(X4)
& city(X4)
& event(X5)
& chevy(X6)
& car(X6)
& white(X6)
& dirty(X6)
& old(X6)
& street(X7)
& way(X7)
& lonely(X7)
& barrel(X5,X6)
& down(X5,X7)
& in(X5,X4)
& seat(X10)
& furniture(X10)
& front(X10)
& X8 != X9
& fellow(X8)
& man(X8)
& young(X8)
& fellow(X9)
& man(X9)
& young(X9)
& X8 = X11
& in(X11,X10)
& X9 = X12
& in(X12,X10) ) ),
inference(negate,[],[subgoal_0]) ).
fof(normalize_0_0,plain,
( ? [U,V,W,X0,X1,X2,X3,Y0,Z] :
( Y0 != Z
& Y0 = X2
& Z = X3
& barrel(V,X0)
& car(X0)
& chevy(X0)
& city(U)
& dirty(X0)
& down(V,W)
& event(V)
& fellow(Y0)
& fellow(Z)
& front(X1)
& furniture(X1)
& hollywood(U)
& in(V,U)
& in(X2,X1)
& in(X3,X1)
& lonely(W)
& man(Y0)
& man(Z)
& old(X0)
& seat(X1)
& street(W)
& way(W)
& white(X0)
& young(Y0)
& young(Z) )
& ! [X10,X11,X12,X4,X5,X6,X7,X8,X9] :
( X8 != X11
| X9 != X12
| ~ barrel(X5,X6)
| ~ car(X6)
| ~ chevy(X6)
| ~ city(X4)
| ~ dirty(X6)
| ~ down(X5,X7)
| ~ event(X5)
| ~ fellow(X8)
| ~ fellow(X9)
| ~ front(X10)
| ~ furniture(X10)
| ~ hollywood(X4)
| ~ in(X11,X10)
| ~ in(X12,X10)
| ~ in(X5,X4)
| ~ lonely(X7)
| ~ man(X8)
| ~ man(X9)
| ~ old(X6)
| ~ seat(X10)
| ~ street(X7)
| ~ way(X7)
| ~ white(X6)
| ~ young(X8)
| ~ young(X9)
| X8 = X9 ) ),
inference(canonicalize,[],[negate_0_0]) ).
fof(normalize_0_1,plain,
? [U,V,W,X0,X1,X2,X3,Y0,Z] :
( Y0 != Z
& Y0 = X2
& Z = X3
& barrel(V,X0)
& car(X0)
& chevy(X0)
& city(U)
& dirty(X0)
& down(V,W)
& event(V)
& fellow(Y0)
& fellow(Z)
& front(X1)
& furniture(X1)
& hollywood(U)
& in(V,U)
& in(X2,X1)
& in(X3,X1)
& lonely(W)
& man(Y0)
& man(Z)
& old(X0)
& seat(X1)
& street(W)
& way(W)
& white(X0)
& young(Y0)
& young(Z) ),
inference(conjunct,[],[normalize_0_0]) ).
fof(normalize_0_2,plain,
( skolemFOFtoCNF_Y != skolemFOFtoCNF_Z
& skolemFOFtoCNF_Y = skolemFOFtoCNF_X2
& skolemFOFtoCNF_Z = skolemFOFtoCNF_X3
& barrel(skolemFOFtoCNF_V,skolemFOFtoCNF_X)
& car(skolemFOFtoCNF_X)
& chevy(skolemFOFtoCNF_X)
& city(skolemFOFtoCNF_U)
& dirty(skolemFOFtoCNF_X)
& down(skolemFOFtoCNF_V,skolemFOFtoCNF_W)
& event(skolemFOFtoCNF_V)
& fellow(skolemFOFtoCNF_Y)
& fellow(skolemFOFtoCNF_Z)
& front(skolemFOFtoCNF_X1)
& furniture(skolemFOFtoCNF_X1)
& hollywood(skolemFOFtoCNF_U)
& in(skolemFOFtoCNF_V,skolemFOFtoCNF_U)
& in(skolemFOFtoCNF_X2,skolemFOFtoCNF_X1)
& in(skolemFOFtoCNF_X3,skolemFOFtoCNF_X1)
& lonely(skolemFOFtoCNF_W)
& man(skolemFOFtoCNF_Y)
& man(skolemFOFtoCNF_Z)
& old(skolemFOFtoCNF_X)
& seat(skolemFOFtoCNF_X1)
& street(skolemFOFtoCNF_W)
& way(skolemFOFtoCNF_W)
& white(skolemFOFtoCNF_X)
& young(skolemFOFtoCNF_Y)
& young(skolemFOFtoCNF_Z) ),
inference(skolemize,[],[normalize_0_1]) ).
fof(normalize_0_3,plain,
barrel(skolemFOFtoCNF_V,skolemFOFtoCNF_X),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_4,plain,
down(skolemFOFtoCNF_V,skolemFOFtoCNF_W),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_5,plain,
in(skolemFOFtoCNF_X2,skolemFOFtoCNF_X1),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_6,plain,
in(skolemFOFtoCNF_V,skolemFOFtoCNF_U),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_7,plain,
in(skolemFOFtoCNF_X3,skolemFOFtoCNF_X1),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_8,plain,
! [X10,X11,X12,X4,X5,X6,X7,X8,X9] :
( X8 != X11
| X9 != X12
| ~ barrel(X5,X6)
| ~ car(X6)
| ~ chevy(X6)
| ~ city(X4)
| ~ dirty(X6)
| ~ down(X5,X7)
| ~ event(X5)
| ~ fellow(X8)
| ~ fellow(X9)
| ~ front(X10)
| ~ furniture(X10)
| ~ hollywood(X4)
| ~ in(X11,X10)
| ~ in(X12,X10)
| ~ in(X5,X4)
| ~ lonely(X7)
| ~ man(X8)
| ~ man(X9)
| ~ old(X6)
| ~ seat(X10)
| ~ street(X7)
| ~ way(X7)
| ~ white(X6)
| ~ young(X8)
| ~ young(X9)
| X8 = X9 ),
inference(conjunct,[],[normalize_0_0]) ).
fof(normalize_0_9,plain,
! [X10,X11,X12,X4,X5,X6,X7,X8,X9] :
( X8 != X11
| X9 != X12
| ~ barrel(X5,X6)
| ~ car(X6)
| ~ chevy(X6)
| ~ city(X4)
| ~ dirty(X6)
| ~ down(X5,X7)
| ~ event(X5)
| ~ fellow(X8)
| ~ fellow(X9)
| ~ front(X10)
| ~ furniture(X10)
| ~ hollywood(X4)
| ~ in(X11,X10)
| ~ in(X12,X10)
| ~ in(X5,X4)
| ~ lonely(X7)
| ~ man(X8)
| ~ man(X9)
| ~ old(X6)
| ~ seat(X10)
| ~ street(X7)
| ~ way(X7)
| ~ white(X6)
| ~ young(X8)
| ~ young(X9)
| X8 = X9 ),
inference(specialize,[],[normalize_0_8]) ).
fof(normalize_0_10,plain,
fellow(skolemFOFtoCNF_Z),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_11,plain,
skolemFOFtoCNF_Z = skolemFOFtoCNF_X3,
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_12,plain,
front(skolemFOFtoCNF_X1),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_13,plain,
furniture(skolemFOFtoCNF_X1),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_14,plain,
man(skolemFOFtoCNF_Z),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_15,plain,
seat(skolemFOFtoCNF_X1),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_16,plain,
young(skolemFOFtoCNF_Z),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_17,plain,
city(skolemFOFtoCNF_U),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_18,plain,
event(skolemFOFtoCNF_V),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_19,plain,
hollywood(skolemFOFtoCNF_U),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_20,plain,
fellow(skolemFOFtoCNF_Y),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_21,plain,
skolemFOFtoCNF_Y = skolemFOFtoCNF_X2,
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_22,plain,
man(skolemFOFtoCNF_Y),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_23,plain,
young(skolemFOFtoCNF_Y),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_24,plain,
skolemFOFtoCNF_Y != skolemFOFtoCNF_Z,
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_25,plain,
lonely(skolemFOFtoCNF_W),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_26,plain,
street(skolemFOFtoCNF_W),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_27,plain,
way(skolemFOFtoCNF_W),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_28,plain,
car(skolemFOFtoCNF_X),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_29,plain,
chevy(skolemFOFtoCNF_X),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_30,plain,
dirty(skolemFOFtoCNF_X),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_31,plain,
old(skolemFOFtoCNF_X),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_32,plain,
white(skolemFOFtoCNF_X),
inference(conjunct,[],[normalize_0_2]) ).
cnf(refute_0_0,plain,
barrel(skolemFOFtoCNF_V,skolemFOFtoCNF_X),
inference(canonicalize,[],[normalize_0_3]) ).
cnf(refute_0_1,plain,
down(skolemFOFtoCNF_V,skolemFOFtoCNF_W),
inference(canonicalize,[],[normalize_0_4]) ).
cnf(refute_0_2,plain,
in(skolemFOFtoCNF_X2,skolemFOFtoCNF_X1),
inference(canonicalize,[],[normalize_0_5]) ).
cnf(refute_0_3,plain,
in(skolemFOFtoCNF_V,skolemFOFtoCNF_U),
inference(canonicalize,[],[normalize_0_6]) ).
cnf(refute_0_4,plain,
in(skolemFOFtoCNF_X3,skolemFOFtoCNF_X1),
inference(canonicalize,[],[normalize_0_7]) ).
cnf(refute_0_5,plain,
( X8 != X11
| X9 != X12
| ~ barrel(X5,X6)
| ~ car(X6)
| ~ chevy(X6)
| ~ city(X4)
| ~ dirty(X6)
| ~ down(X5,X7)
| ~ event(X5)
| ~ fellow(X8)
| ~ fellow(X9)
| ~ front(X10)
| ~ furniture(X10)
| ~ hollywood(X4)
| ~ in(X11,X10)
| ~ in(X12,X10)
| ~ in(X5,X4)
| ~ lonely(X7)
| ~ man(X8)
| ~ man(X9)
| ~ old(X6)
| ~ seat(X10)
| ~ street(X7)
| ~ way(X7)
| ~ white(X6)
| ~ young(X8)
| ~ young(X9)
| X8 = X9 ),
inference(canonicalize,[],[normalize_0_9]) ).
cnf(refute_0_6,plain,
( X11 != X11
| X12 != X12
| ~ barrel(X5,X6)
| ~ car(X6)
| ~ chevy(X6)
| ~ city(X4)
| ~ dirty(X6)
| ~ down(X5,X7)
| ~ event(X5)
| ~ fellow(X11)
| ~ fellow(X12)
| ~ front(X10)
| ~ furniture(X10)
| ~ hollywood(X4)
| ~ in(X11,X10)
| ~ in(X12,X10)
| ~ in(X5,X4)
| ~ lonely(X7)
| ~ man(X11)
| ~ man(X12)
| ~ old(X6)
| ~ seat(X10)
| ~ street(X7)
| ~ way(X7)
| ~ white(X6)
| ~ young(X11)
| ~ young(X12)
| X11 = X12 ),
inference(subst,[],[refute_0_5:[bind(X8,$fot(X11)),bind(X9,$fot(X12))]]) ).
cnf(refute_0_7,plain,
X11 = X11,
introduced(tautology,[refl,[$fot(X11)]]) ).
cnf(refute_0_8,plain,
( X12 != X12
| ~ barrel(X5,X6)
| ~ car(X6)
| ~ chevy(X6)
| ~ city(X4)
| ~ dirty(X6)
| ~ down(X5,X7)
| ~ event(X5)
| ~ fellow(X11)
| ~ fellow(X12)
| ~ front(X10)
| ~ furniture(X10)
| ~ hollywood(X4)
| ~ in(X11,X10)
| ~ in(X12,X10)
| ~ in(X5,X4)
| ~ lonely(X7)
| ~ man(X11)
| ~ man(X12)
| ~ old(X6)
| ~ seat(X10)
| ~ street(X7)
| ~ way(X7)
| ~ white(X6)
| ~ young(X11)
| ~ young(X12)
| X11 = X12 ),
inference(resolve,[$cnf( $equal(X11,X11) )],[refute_0_7,refute_0_6]) ).
cnf(refute_0_9,plain,
X12 = X12,
introduced(tautology,[refl,[$fot(X12)]]) ).
cnf(refute_0_10,plain,
( ~ barrel(X5,X6)
| ~ car(X6)
| ~ chevy(X6)
| ~ city(X4)
| ~ dirty(X6)
| ~ down(X5,X7)
| ~ event(X5)
| ~ fellow(X11)
| ~ fellow(X12)
| ~ front(X10)
| ~ furniture(X10)
| ~ hollywood(X4)
| ~ in(X11,X10)
| ~ in(X12,X10)
| ~ in(X5,X4)
| ~ lonely(X7)
| ~ man(X11)
| ~ man(X12)
| ~ old(X6)
| ~ seat(X10)
| ~ street(X7)
| ~ way(X7)
| ~ white(X6)
| ~ young(X11)
| ~ young(X12)
| X11 = X12 ),
inference(resolve,[$cnf( $equal(X12,X12) )],[refute_0_9,refute_0_8]) ).
cnf(refute_0_11,plain,
( ~ barrel(X_28,X_29)
| ~ car(X_29)
| ~ chevy(X_29)
| ~ city(X_27)
| ~ dirty(X_29)
| ~ down(X_28,X_30)
| ~ event(X_28)
| ~ fellow(X_26)
| ~ fellow(skolemFOFtoCNF_X3)
| ~ front(skolemFOFtoCNF_X1)
| ~ furniture(skolemFOFtoCNF_X1)
| ~ hollywood(X_27)
| ~ in(X_26,skolemFOFtoCNF_X1)
| ~ in(X_28,X_27)
| ~ in(skolemFOFtoCNF_X3,skolemFOFtoCNF_X1)
| ~ lonely(X_30)
| ~ man(X_26)
| ~ man(skolemFOFtoCNF_X3)
| ~ old(X_29)
| ~ seat(skolemFOFtoCNF_X1)
| ~ street(X_30)
| ~ way(X_30)
| ~ white(X_29)
| ~ young(X_26)
| ~ young(skolemFOFtoCNF_X3)
| skolemFOFtoCNF_X3 = X_26 ),
inference(subst,[],[refute_0_10:[bind(X10,$fot(skolemFOFtoCNF_X1)),bind(X11,$fot(skolemFOFtoCNF_X3)),bind(X12,$fot(X_26)),bind(X4,$fot(X_27)),bind(X5,$fot(X_28)),bind(X6,$fot(X_29)),bind(X7,$fot(X_30))]]) ).
cnf(refute_0_12,plain,
( ~ barrel(X_28,X_29)
| ~ car(X_29)
| ~ chevy(X_29)
| ~ city(X_27)
| ~ dirty(X_29)
| ~ down(X_28,X_30)
| ~ event(X_28)
| ~ fellow(X_26)
| ~ fellow(skolemFOFtoCNF_X3)
| ~ front(skolemFOFtoCNF_X1)
| ~ furniture(skolemFOFtoCNF_X1)
| ~ hollywood(X_27)
| ~ in(X_26,skolemFOFtoCNF_X1)
| ~ in(X_28,X_27)
| ~ lonely(X_30)
| ~ man(X_26)
| ~ man(skolemFOFtoCNF_X3)
| ~ old(X_29)
| ~ seat(skolemFOFtoCNF_X1)
| ~ street(X_30)
| ~ way(X_30)
| ~ white(X_29)
| ~ young(X_26)
| ~ young(skolemFOFtoCNF_X3)
| skolemFOFtoCNF_X3 = X_26 ),
inference(resolve,[$cnf( in(skolemFOFtoCNF_X3,skolemFOFtoCNF_X1) )],[refute_0_4,refute_0_11]) ).
cnf(refute_0_13,plain,
fellow(skolemFOFtoCNF_Z),
inference(canonicalize,[],[normalize_0_10]) ).
cnf(refute_0_14,plain,
skolemFOFtoCNF_Z = skolemFOFtoCNF_X3,
inference(canonicalize,[],[normalize_0_11]) ).
cnf(refute_0_15,plain,
( skolemFOFtoCNF_Z != skolemFOFtoCNF_X3
| ~ fellow(skolemFOFtoCNF_Z)
| fellow(skolemFOFtoCNF_X3) ),
introduced(tautology,[equality,[$cnf( fellow(skolemFOFtoCNF_Z) ),[0],$fot(skolemFOFtoCNF_X3)]]) ).
cnf(refute_0_16,plain,
( ~ fellow(skolemFOFtoCNF_Z)
| fellow(skolemFOFtoCNF_X3) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_Z,skolemFOFtoCNF_X3) )],[refute_0_14,refute_0_15]) ).
cnf(refute_0_17,plain,
fellow(skolemFOFtoCNF_X3),
inference(resolve,[$cnf( fellow(skolemFOFtoCNF_Z) )],[refute_0_13,refute_0_16]) ).
cnf(refute_0_18,plain,
( ~ barrel(X_28,X_29)
| ~ car(X_29)
| ~ chevy(X_29)
| ~ city(X_27)
| ~ dirty(X_29)
| ~ down(X_28,X_30)
| ~ event(X_28)
| ~ fellow(X_26)
| ~ front(skolemFOFtoCNF_X1)
| ~ furniture(skolemFOFtoCNF_X1)
| ~ hollywood(X_27)
| ~ in(X_26,skolemFOFtoCNF_X1)
| ~ in(X_28,X_27)
| ~ lonely(X_30)
| ~ man(X_26)
| ~ man(skolemFOFtoCNF_X3)
| ~ old(X_29)
| ~ seat(skolemFOFtoCNF_X1)
| ~ street(X_30)
| ~ way(X_30)
| ~ white(X_29)
| ~ young(X_26)
| ~ young(skolemFOFtoCNF_X3)
| skolemFOFtoCNF_X3 = X_26 ),
inference(resolve,[$cnf( fellow(skolemFOFtoCNF_X3) )],[refute_0_17,refute_0_12]) ).
cnf(refute_0_19,plain,
front(skolemFOFtoCNF_X1),
inference(canonicalize,[],[normalize_0_12]) ).
cnf(refute_0_20,plain,
( ~ barrel(X_28,X_29)
| ~ car(X_29)
| ~ chevy(X_29)
| ~ city(X_27)
| ~ dirty(X_29)
| ~ down(X_28,X_30)
| ~ event(X_28)
| ~ fellow(X_26)
| ~ furniture(skolemFOFtoCNF_X1)
| ~ hollywood(X_27)
| ~ in(X_26,skolemFOFtoCNF_X1)
| ~ in(X_28,X_27)
| ~ lonely(X_30)
| ~ man(X_26)
| ~ man(skolemFOFtoCNF_X3)
| ~ old(X_29)
| ~ seat(skolemFOFtoCNF_X1)
| ~ street(X_30)
| ~ way(X_30)
| ~ white(X_29)
| ~ young(X_26)
| ~ young(skolemFOFtoCNF_X3)
| skolemFOFtoCNF_X3 = X_26 ),
inference(resolve,[$cnf( front(skolemFOFtoCNF_X1) )],[refute_0_19,refute_0_18]) ).
cnf(refute_0_21,plain,
furniture(skolemFOFtoCNF_X1),
inference(canonicalize,[],[normalize_0_13]) ).
cnf(refute_0_22,plain,
( ~ barrel(X_28,X_29)
| ~ car(X_29)
| ~ chevy(X_29)
| ~ city(X_27)
| ~ dirty(X_29)
| ~ down(X_28,X_30)
| ~ event(X_28)
| ~ fellow(X_26)
| ~ hollywood(X_27)
| ~ in(X_26,skolemFOFtoCNF_X1)
| ~ in(X_28,X_27)
| ~ lonely(X_30)
| ~ man(X_26)
| ~ man(skolemFOFtoCNF_X3)
| ~ old(X_29)
| ~ seat(skolemFOFtoCNF_X1)
| ~ street(X_30)
| ~ way(X_30)
| ~ white(X_29)
| ~ young(X_26)
| ~ young(skolemFOFtoCNF_X3)
| skolemFOFtoCNF_X3 = X_26 ),
inference(resolve,[$cnf( furniture(skolemFOFtoCNF_X1) )],[refute_0_21,refute_0_20]) ).
cnf(refute_0_23,plain,
man(skolemFOFtoCNF_Z),
inference(canonicalize,[],[normalize_0_14]) ).
cnf(refute_0_24,plain,
( skolemFOFtoCNF_Z != skolemFOFtoCNF_X3
| ~ man(skolemFOFtoCNF_Z)
| man(skolemFOFtoCNF_X3) ),
introduced(tautology,[equality,[$cnf( man(skolemFOFtoCNF_Z) ),[0],$fot(skolemFOFtoCNF_X3)]]) ).
cnf(refute_0_25,plain,
( ~ man(skolemFOFtoCNF_Z)
| man(skolemFOFtoCNF_X3) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_Z,skolemFOFtoCNF_X3) )],[refute_0_14,refute_0_24]) ).
cnf(refute_0_26,plain,
man(skolemFOFtoCNF_X3),
inference(resolve,[$cnf( man(skolemFOFtoCNF_Z) )],[refute_0_23,refute_0_25]) ).
cnf(refute_0_27,plain,
( ~ barrel(X_28,X_29)
| ~ car(X_29)
| ~ chevy(X_29)
| ~ city(X_27)
| ~ dirty(X_29)
| ~ down(X_28,X_30)
| ~ event(X_28)
| ~ fellow(X_26)
| ~ hollywood(X_27)
| ~ in(X_26,skolemFOFtoCNF_X1)
| ~ in(X_28,X_27)
| ~ lonely(X_30)
| ~ man(X_26)
| ~ old(X_29)
| ~ seat(skolemFOFtoCNF_X1)
| ~ street(X_30)
| ~ way(X_30)
| ~ white(X_29)
| ~ young(X_26)
| ~ young(skolemFOFtoCNF_X3)
| skolemFOFtoCNF_X3 = X_26 ),
inference(resolve,[$cnf( man(skolemFOFtoCNF_X3) )],[refute_0_26,refute_0_22]) ).
cnf(refute_0_28,plain,
seat(skolemFOFtoCNF_X1),
inference(canonicalize,[],[normalize_0_15]) ).
cnf(refute_0_29,plain,
( ~ barrel(X_28,X_29)
| ~ car(X_29)
| ~ chevy(X_29)
| ~ city(X_27)
| ~ dirty(X_29)
| ~ down(X_28,X_30)
| ~ event(X_28)
| ~ fellow(X_26)
| ~ hollywood(X_27)
| ~ in(X_26,skolemFOFtoCNF_X1)
| ~ in(X_28,X_27)
| ~ lonely(X_30)
| ~ man(X_26)
| ~ old(X_29)
| ~ street(X_30)
| ~ way(X_30)
| ~ white(X_29)
| ~ young(X_26)
| ~ young(skolemFOFtoCNF_X3)
| skolemFOFtoCNF_X3 = X_26 ),
inference(resolve,[$cnf( seat(skolemFOFtoCNF_X1) )],[refute_0_28,refute_0_27]) ).
cnf(refute_0_30,plain,
young(skolemFOFtoCNF_Z),
inference(canonicalize,[],[normalize_0_16]) ).
cnf(refute_0_31,plain,
( skolemFOFtoCNF_Z != skolemFOFtoCNF_X3
| ~ young(skolemFOFtoCNF_Z)
| young(skolemFOFtoCNF_X3) ),
introduced(tautology,[equality,[$cnf( young(skolemFOFtoCNF_Z) ),[0],$fot(skolemFOFtoCNF_X3)]]) ).
cnf(refute_0_32,plain,
( ~ young(skolemFOFtoCNF_Z)
| young(skolemFOFtoCNF_X3) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_Z,skolemFOFtoCNF_X3) )],[refute_0_14,refute_0_31]) ).
cnf(refute_0_33,plain,
young(skolemFOFtoCNF_X3),
inference(resolve,[$cnf( young(skolemFOFtoCNF_Z) )],[refute_0_30,refute_0_32]) ).
cnf(refute_0_34,plain,
( ~ barrel(X_28,X_29)
| ~ car(X_29)
| ~ chevy(X_29)
| ~ city(X_27)
| ~ dirty(X_29)
| ~ down(X_28,X_30)
| ~ event(X_28)
| ~ fellow(X_26)
| ~ hollywood(X_27)
| ~ in(X_26,skolemFOFtoCNF_X1)
| ~ in(X_28,X_27)
| ~ lonely(X_30)
| ~ man(X_26)
| ~ old(X_29)
| ~ street(X_30)
| ~ way(X_30)
| ~ white(X_29)
| ~ young(X_26)
| skolemFOFtoCNF_X3 = X_26 ),
inference(resolve,[$cnf( young(skolemFOFtoCNF_X3) )],[refute_0_33,refute_0_29]) ).
cnf(refute_0_35,plain,
( ~ barrel(skolemFOFtoCNF_V,X_34)
| ~ car(X_34)
| ~ chevy(X_34)
| ~ city(skolemFOFtoCNF_U)
| ~ dirty(X_34)
| ~ down(skolemFOFtoCNF_V,X_35)
| ~ event(skolemFOFtoCNF_V)
| ~ fellow(X_31)
| ~ hollywood(skolemFOFtoCNF_U)
| ~ in(X_31,skolemFOFtoCNF_X1)
| ~ in(skolemFOFtoCNF_V,skolemFOFtoCNF_U)
| ~ lonely(X_35)
| ~ man(X_31)
| ~ old(X_34)
| ~ street(X_35)
| ~ way(X_35)
| ~ white(X_34)
| ~ young(X_31)
| skolemFOFtoCNF_X3 = X_31 ),
inference(subst,[],[refute_0_34:[bind(X_26,$fot(X_31)),bind(X_27,$fot(skolemFOFtoCNF_U)),bind(X_28,$fot(skolemFOFtoCNF_V)),bind(X_29,$fot(X_34)),bind(X_30,$fot(X_35))]]) ).
cnf(refute_0_36,plain,
( ~ barrel(skolemFOFtoCNF_V,X_34)
| ~ car(X_34)
| ~ chevy(X_34)
| ~ city(skolemFOFtoCNF_U)
| ~ dirty(X_34)
| ~ down(skolemFOFtoCNF_V,X_35)
| ~ event(skolemFOFtoCNF_V)
| ~ fellow(X_31)
| ~ hollywood(skolemFOFtoCNF_U)
| ~ in(X_31,skolemFOFtoCNF_X1)
| ~ lonely(X_35)
| ~ man(X_31)
| ~ old(X_34)
| ~ street(X_35)
| ~ way(X_35)
| ~ white(X_34)
| ~ young(X_31)
| skolemFOFtoCNF_X3 = X_31 ),
inference(resolve,[$cnf( in(skolemFOFtoCNF_V,skolemFOFtoCNF_U) )],[refute_0_3,refute_0_35]) ).
cnf(refute_0_37,plain,
city(skolemFOFtoCNF_U),
inference(canonicalize,[],[normalize_0_17]) ).
cnf(refute_0_38,plain,
( ~ barrel(skolemFOFtoCNF_V,X_34)
| ~ car(X_34)
| ~ chevy(X_34)
| ~ dirty(X_34)
| ~ down(skolemFOFtoCNF_V,X_35)
| ~ event(skolemFOFtoCNF_V)
| ~ fellow(X_31)
| ~ hollywood(skolemFOFtoCNF_U)
| ~ in(X_31,skolemFOFtoCNF_X1)
| ~ lonely(X_35)
| ~ man(X_31)
| ~ old(X_34)
| ~ street(X_35)
| ~ way(X_35)
| ~ white(X_34)
| ~ young(X_31)
| skolemFOFtoCNF_X3 = X_31 ),
inference(resolve,[$cnf( city(skolemFOFtoCNF_U) )],[refute_0_37,refute_0_36]) ).
cnf(refute_0_39,plain,
event(skolemFOFtoCNF_V),
inference(canonicalize,[],[normalize_0_18]) ).
cnf(refute_0_40,plain,
( ~ barrel(skolemFOFtoCNF_V,X_34)
| ~ car(X_34)
| ~ chevy(X_34)
| ~ dirty(X_34)
| ~ down(skolemFOFtoCNF_V,X_35)
| ~ fellow(X_31)
| ~ hollywood(skolemFOFtoCNF_U)
| ~ in(X_31,skolemFOFtoCNF_X1)
| ~ lonely(X_35)
| ~ man(X_31)
| ~ old(X_34)
| ~ street(X_35)
| ~ way(X_35)
| ~ white(X_34)
| ~ young(X_31)
| skolemFOFtoCNF_X3 = X_31 ),
inference(resolve,[$cnf( event(skolemFOFtoCNF_V) )],[refute_0_39,refute_0_38]) ).
cnf(refute_0_41,plain,
hollywood(skolemFOFtoCNF_U),
inference(canonicalize,[],[normalize_0_19]) ).
cnf(refute_0_42,plain,
( ~ barrel(skolemFOFtoCNF_V,X_34)
| ~ car(X_34)
| ~ chevy(X_34)
| ~ dirty(X_34)
| ~ down(skolemFOFtoCNF_V,X_35)
| ~ fellow(X_31)
| ~ in(X_31,skolemFOFtoCNF_X1)
| ~ lonely(X_35)
| ~ man(X_31)
| ~ old(X_34)
| ~ street(X_35)
| ~ way(X_35)
| ~ white(X_34)
| ~ young(X_31)
| skolemFOFtoCNF_X3 = X_31 ),
inference(resolve,[$cnf( hollywood(skolemFOFtoCNF_U) )],[refute_0_41,refute_0_40]) ).
cnf(refute_0_43,plain,
( ~ barrel(skolemFOFtoCNF_V,X_37)
| ~ car(X_37)
| ~ chevy(X_37)
| ~ dirty(X_37)
| ~ down(skolemFOFtoCNF_V,X_38)
| ~ fellow(skolemFOFtoCNF_X2)
| ~ in(skolemFOFtoCNF_X2,skolemFOFtoCNF_X1)
| ~ lonely(X_38)
| ~ man(skolemFOFtoCNF_X2)
| ~ old(X_37)
| ~ street(X_38)
| ~ way(X_38)
| ~ white(X_37)
| ~ young(skolemFOFtoCNF_X2)
| skolemFOFtoCNF_X3 = skolemFOFtoCNF_X2 ),
inference(subst,[],[refute_0_42:[bind(X_31,$fot(skolemFOFtoCNF_X2)),bind(X_34,$fot(X_37)),bind(X_35,$fot(X_38))]]) ).
cnf(refute_0_44,plain,
( ~ barrel(skolemFOFtoCNF_V,X_37)
| ~ car(X_37)
| ~ chevy(X_37)
| ~ dirty(X_37)
| ~ down(skolemFOFtoCNF_V,X_38)
| ~ fellow(skolemFOFtoCNF_X2)
| ~ lonely(X_38)
| ~ man(skolemFOFtoCNF_X2)
| ~ old(X_37)
| ~ street(X_38)
| ~ way(X_38)
| ~ white(X_37)
| ~ young(skolemFOFtoCNF_X2)
| skolemFOFtoCNF_X3 = skolemFOFtoCNF_X2 ),
inference(resolve,[$cnf( in(skolemFOFtoCNF_X2,skolemFOFtoCNF_X1) )],[refute_0_2,refute_0_43]) ).
cnf(refute_0_45,plain,
fellow(skolemFOFtoCNF_Y),
inference(canonicalize,[],[normalize_0_20]) ).
cnf(refute_0_46,plain,
skolemFOFtoCNF_Y = skolemFOFtoCNF_X2,
inference(canonicalize,[],[normalize_0_21]) ).
cnf(refute_0_47,plain,
( skolemFOFtoCNF_Y != skolemFOFtoCNF_X2
| ~ fellow(skolemFOFtoCNF_Y)
| fellow(skolemFOFtoCNF_X2) ),
introduced(tautology,[equality,[$cnf( fellow(skolemFOFtoCNF_Y) ),[0],$fot(skolemFOFtoCNF_X2)]]) ).
cnf(refute_0_48,plain,
( ~ fellow(skolemFOFtoCNF_Y)
| fellow(skolemFOFtoCNF_X2) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_Y,skolemFOFtoCNF_X2) )],[refute_0_46,refute_0_47]) ).
cnf(refute_0_49,plain,
fellow(skolemFOFtoCNF_X2),
inference(resolve,[$cnf( fellow(skolemFOFtoCNF_Y) )],[refute_0_45,refute_0_48]) ).
cnf(refute_0_50,plain,
( ~ barrel(skolemFOFtoCNF_V,X_37)
| ~ car(X_37)
| ~ chevy(X_37)
| ~ dirty(X_37)
| ~ down(skolemFOFtoCNF_V,X_38)
| ~ lonely(X_38)
| ~ man(skolemFOFtoCNF_X2)
| ~ old(X_37)
| ~ street(X_38)
| ~ way(X_38)
| ~ white(X_37)
| ~ young(skolemFOFtoCNF_X2)
| skolemFOFtoCNF_X3 = skolemFOFtoCNF_X2 ),
inference(resolve,[$cnf( fellow(skolemFOFtoCNF_X2) )],[refute_0_49,refute_0_44]) ).
cnf(refute_0_51,plain,
man(skolemFOFtoCNF_Y),
inference(canonicalize,[],[normalize_0_22]) ).
cnf(refute_0_52,plain,
( skolemFOFtoCNF_Y != skolemFOFtoCNF_X2
| ~ man(skolemFOFtoCNF_Y)
| man(skolemFOFtoCNF_X2) ),
introduced(tautology,[equality,[$cnf( man(skolemFOFtoCNF_Y) ),[0],$fot(skolemFOFtoCNF_X2)]]) ).
cnf(refute_0_53,plain,
( ~ man(skolemFOFtoCNF_Y)
| man(skolemFOFtoCNF_X2) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_Y,skolemFOFtoCNF_X2) )],[refute_0_46,refute_0_52]) ).
cnf(refute_0_54,plain,
man(skolemFOFtoCNF_X2),
inference(resolve,[$cnf( man(skolemFOFtoCNF_Y) )],[refute_0_51,refute_0_53]) ).
cnf(refute_0_55,plain,
( ~ barrel(skolemFOFtoCNF_V,X_37)
| ~ car(X_37)
| ~ chevy(X_37)
| ~ dirty(X_37)
| ~ down(skolemFOFtoCNF_V,X_38)
| ~ lonely(X_38)
| ~ old(X_37)
| ~ street(X_38)
| ~ way(X_38)
| ~ white(X_37)
| ~ young(skolemFOFtoCNF_X2)
| skolemFOFtoCNF_X3 = skolemFOFtoCNF_X2 ),
inference(resolve,[$cnf( man(skolemFOFtoCNF_X2) )],[refute_0_54,refute_0_50]) ).
cnf(refute_0_56,plain,
young(skolemFOFtoCNF_Y),
inference(canonicalize,[],[normalize_0_23]) ).
cnf(refute_0_57,plain,
( skolemFOFtoCNF_Y != skolemFOFtoCNF_X2
| ~ young(skolemFOFtoCNF_Y)
| young(skolemFOFtoCNF_X2) ),
introduced(tautology,[equality,[$cnf( young(skolemFOFtoCNF_Y) ),[0],$fot(skolemFOFtoCNF_X2)]]) ).
cnf(refute_0_58,plain,
( ~ young(skolemFOFtoCNF_Y)
| young(skolemFOFtoCNF_X2) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_Y,skolemFOFtoCNF_X2) )],[refute_0_46,refute_0_57]) ).
cnf(refute_0_59,plain,
young(skolemFOFtoCNF_X2),
inference(resolve,[$cnf( young(skolemFOFtoCNF_Y) )],[refute_0_56,refute_0_58]) ).
cnf(refute_0_60,plain,
( ~ barrel(skolemFOFtoCNF_V,X_37)
| ~ car(X_37)
| ~ chevy(X_37)
| ~ dirty(X_37)
| ~ down(skolemFOFtoCNF_V,X_38)
| ~ lonely(X_38)
| ~ old(X_37)
| ~ street(X_38)
| ~ way(X_38)
| ~ white(X_37)
| skolemFOFtoCNF_X3 = skolemFOFtoCNF_X2 ),
inference(resolve,[$cnf( young(skolemFOFtoCNF_X2) )],[refute_0_59,refute_0_55]) ).
cnf(refute_0_61,plain,
skolemFOFtoCNF_Y != skolemFOFtoCNF_Z,
inference(canonicalize,[],[normalize_0_24]) ).
cnf(refute_0_62,plain,
( skolemFOFtoCNF_X2 != skolemFOFtoCNF_Z
| skolemFOFtoCNF_Y != skolemFOFtoCNF_X2
| skolemFOFtoCNF_Y = skolemFOFtoCNF_Z ),
introduced(tautology,[equality,[$cnf( $equal(skolemFOFtoCNF_Y,skolemFOFtoCNF_X2) ),[1],$fot(skolemFOFtoCNF_Z)]]) ).
cnf(refute_0_63,plain,
( skolemFOFtoCNF_X2 != skolemFOFtoCNF_Z
| skolemFOFtoCNF_Y = skolemFOFtoCNF_Z ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_Y,skolemFOFtoCNF_X2) )],[refute_0_46,refute_0_62]) ).
cnf(refute_0_64,plain,
( skolemFOFtoCNF_X2 != skolemFOFtoCNF_X3
| skolemFOFtoCNF_Z != skolemFOFtoCNF_X3
| skolemFOFtoCNF_X2 = skolemFOFtoCNF_Z ),
introduced(tautology,[equality,[$cnf( ~ $equal(skolemFOFtoCNF_X2,skolemFOFtoCNF_Z) ),[1],$fot(skolemFOFtoCNF_X3)]]) ).
cnf(refute_0_65,plain,
( skolemFOFtoCNF_X2 != skolemFOFtoCNF_X3
| skolemFOFtoCNF_X2 = skolemFOFtoCNF_Z ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_Z,skolemFOFtoCNF_X3) )],[refute_0_14,refute_0_64]) ).
cnf(refute_0_66,plain,
( skolemFOFtoCNF_X2 != skolemFOFtoCNF_X3
| skolemFOFtoCNF_Y = skolemFOFtoCNF_Z ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_X2,skolemFOFtoCNF_Z) )],[refute_0_65,refute_0_63]) ).
cnf(refute_0_67,plain,
skolemFOFtoCNF_X2 != skolemFOFtoCNF_X3,
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_Y,skolemFOFtoCNF_Z) )],[refute_0_66,refute_0_61]) ).
cnf(refute_0_68,plain,
X = X,
introduced(tautology,[refl,[$fot(X)]]) ).
cnf(refute_0_69,plain,
( X != X
| X != Y
| Y = X ),
introduced(tautology,[equality,[$cnf( $equal(X,X) ),[0],$fot(Y)]]) ).
cnf(refute_0_70,plain,
( X != Y
| Y = X ),
inference(resolve,[$cnf( $equal(X,X) )],[refute_0_68,refute_0_69]) ).
cnf(refute_0_71,plain,
( skolemFOFtoCNF_X3 != skolemFOFtoCNF_X2
| skolemFOFtoCNF_X2 = skolemFOFtoCNF_X3 ),
inference(subst,[],[refute_0_70:[bind(X,$fot(skolemFOFtoCNF_X3)),bind(Y,$fot(skolemFOFtoCNF_X2))]]) ).
cnf(refute_0_72,plain,
skolemFOFtoCNF_X3 != skolemFOFtoCNF_X2,
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_X2,skolemFOFtoCNF_X3) )],[refute_0_71,refute_0_67]) ).
cnf(refute_0_73,plain,
( ~ barrel(skolemFOFtoCNF_V,X_37)
| ~ car(X_37)
| ~ chevy(X_37)
| ~ dirty(X_37)
| ~ down(skolemFOFtoCNF_V,X_38)
| ~ lonely(X_38)
| ~ old(X_37)
| ~ street(X_38)
| ~ way(X_38)
| ~ white(X_37) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_X3,skolemFOFtoCNF_X2) )],[refute_0_60,refute_0_72]) ).
cnf(refute_0_74,plain,
( ~ barrel(skolemFOFtoCNF_V,X_39)
| ~ car(X_39)
| ~ chevy(X_39)
| ~ dirty(X_39)
| ~ down(skolemFOFtoCNF_V,skolemFOFtoCNF_W)
| ~ lonely(skolemFOFtoCNF_W)
| ~ old(X_39)
| ~ street(skolemFOFtoCNF_W)
| ~ way(skolemFOFtoCNF_W)
| ~ white(X_39) ),
inference(subst,[],[refute_0_73:[bind(X_37,$fot(X_39)),bind(X_38,$fot(skolemFOFtoCNF_W))]]) ).
cnf(refute_0_75,plain,
( ~ barrel(skolemFOFtoCNF_V,X_39)
| ~ car(X_39)
| ~ chevy(X_39)
| ~ dirty(X_39)
| ~ lonely(skolemFOFtoCNF_W)
| ~ old(X_39)
| ~ street(skolemFOFtoCNF_W)
| ~ way(skolemFOFtoCNF_W)
| ~ white(X_39) ),
inference(resolve,[$cnf( down(skolemFOFtoCNF_V,skolemFOFtoCNF_W) )],[refute_0_1,refute_0_74]) ).
cnf(refute_0_76,plain,
lonely(skolemFOFtoCNF_W),
inference(canonicalize,[],[normalize_0_25]) ).
cnf(refute_0_77,plain,
( ~ barrel(skolemFOFtoCNF_V,X_39)
| ~ car(X_39)
| ~ chevy(X_39)
| ~ dirty(X_39)
| ~ old(X_39)
| ~ street(skolemFOFtoCNF_W)
| ~ way(skolemFOFtoCNF_W)
| ~ white(X_39) ),
inference(resolve,[$cnf( lonely(skolemFOFtoCNF_W) )],[refute_0_76,refute_0_75]) ).
cnf(refute_0_78,plain,
street(skolemFOFtoCNF_W),
inference(canonicalize,[],[normalize_0_26]) ).
cnf(refute_0_79,plain,
( ~ barrel(skolemFOFtoCNF_V,X_39)
| ~ car(X_39)
| ~ chevy(X_39)
| ~ dirty(X_39)
| ~ old(X_39)
| ~ way(skolemFOFtoCNF_W)
| ~ white(X_39) ),
inference(resolve,[$cnf( street(skolemFOFtoCNF_W) )],[refute_0_78,refute_0_77]) ).
cnf(refute_0_80,plain,
way(skolemFOFtoCNF_W),
inference(canonicalize,[],[normalize_0_27]) ).
cnf(refute_0_81,plain,
( ~ barrel(skolemFOFtoCNF_V,X_39)
| ~ car(X_39)
| ~ chevy(X_39)
| ~ dirty(X_39)
| ~ old(X_39)
| ~ white(X_39) ),
inference(resolve,[$cnf( way(skolemFOFtoCNF_W) )],[refute_0_80,refute_0_79]) ).
cnf(refute_0_82,plain,
( ~ barrel(skolemFOFtoCNF_V,skolemFOFtoCNF_X)
| ~ car(skolemFOFtoCNF_X)
| ~ chevy(skolemFOFtoCNF_X)
| ~ dirty(skolemFOFtoCNF_X)
| ~ old(skolemFOFtoCNF_X)
| ~ white(skolemFOFtoCNF_X) ),
inference(subst,[],[refute_0_81:[bind(X_39,$fot(skolemFOFtoCNF_X))]]) ).
cnf(refute_0_83,plain,
( ~ car(skolemFOFtoCNF_X)
| ~ chevy(skolemFOFtoCNF_X)
| ~ dirty(skolemFOFtoCNF_X)
| ~ old(skolemFOFtoCNF_X)
| ~ white(skolemFOFtoCNF_X) ),
inference(resolve,[$cnf( barrel(skolemFOFtoCNF_V,skolemFOFtoCNF_X) )],[refute_0_0,refute_0_82]) ).
cnf(refute_0_84,plain,
car(skolemFOFtoCNF_X),
inference(canonicalize,[],[normalize_0_28]) ).
cnf(refute_0_85,plain,
( ~ chevy(skolemFOFtoCNF_X)
| ~ dirty(skolemFOFtoCNF_X)
| ~ old(skolemFOFtoCNF_X)
| ~ white(skolemFOFtoCNF_X) ),
inference(resolve,[$cnf( car(skolemFOFtoCNF_X) )],[refute_0_84,refute_0_83]) ).
cnf(refute_0_86,plain,
chevy(skolemFOFtoCNF_X),
inference(canonicalize,[],[normalize_0_29]) ).
cnf(refute_0_87,plain,
( ~ dirty(skolemFOFtoCNF_X)
| ~ old(skolemFOFtoCNF_X)
| ~ white(skolemFOFtoCNF_X) ),
inference(resolve,[$cnf( chevy(skolemFOFtoCNF_X) )],[refute_0_86,refute_0_85]) ).
cnf(refute_0_88,plain,
dirty(skolemFOFtoCNF_X),
inference(canonicalize,[],[normalize_0_30]) ).
cnf(refute_0_89,plain,
( ~ old(skolemFOFtoCNF_X)
| ~ white(skolemFOFtoCNF_X) ),
inference(resolve,[$cnf( dirty(skolemFOFtoCNF_X) )],[refute_0_88,refute_0_87]) ).
cnf(refute_0_90,plain,
old(skolemFOFtoCNF_X),
inference(canonicalize,[],[normalize_0_31]) ).
cnf(refute_0_91,plain,
~ white(skolemFOFtoCNF_X),
inference(resolve,[$cnf( old(skolemFOFtoCNF_X) )],[refute_0_90,refute_0_89]) ).
cnf(refute_0_92,plain,
white(skolemFOFtoCNF_X),
inference(canonicalize,[],[normalize_0_32]) ).
cnf(refute_0_93,plain,
$false,
inference(resolve,[$cnf( white(skolemFOFtoCNF_X) )],[refute_0_92,refute_0_91]) ).
fof(negate_1_0,plain,
~ ( ( ( ? [U,V,W,X0,Y0,Z,X1,X2,X3] :
( hollywood(U)
& city(U)
& event(V)
& street(W)
& way(W)
& lonely(W)
& chevy(X0)
& car(X0)
& white(X0)
& dirty(X0)
& old(X0)
& barrel(V,X0)
& down(V,W)
& in(V,U)
& seat(X1)
& furniture(X1)
& front(X1)
& Y0 != Z
& fellow(Y0)
& man(Y0)
& young(Y0)
& fellow(Z)
& man(Z)
& young(Z)
& Y0 = X2
& in(X2,X1)
& Z = X3
& in(X3,X1) )
=> ? [X4,X5,X6,X7,X8,X9,X10,X11,X12] :
( hollywood(X4)
& city(X4)
& event(X5)
& chevy(X6)
& car(X6)
& white(X6)
& dirty(X6)
& old(X6)
& street(X7)
& way(X7)
& lonely(X7)
& barrel(X5,X6)
& down(X5,X7)
& in(X5,X4)
& seat(X10)
& furniture(X10)
& front(X10)
& X8 != X9
& fellow(X8)
& man(X8)
& young(X8)
& fellow(X9)
& man(X9)
& young(X9)
& X8 = X11
& in(X11,X10)
& X9 = X12
& in(X12,X10) ) )
& ? [X13,X14,X15,X16,X17,X18,X19,X20,X21] :
( hollywood(X13)
& city(X13)
& event(X14)
& chevy(X15)
& car(X15)
& white(X15)
& dirty(X15)
& old(X15)
& street(X16)
& way(X16)
& lonely(X16)
& barrel(X14,X15)
& down(X14,X16)
& in(X14,X13)
& seat(X19)
& furniture(X19)
& front(X19)
& X17 != X18
& fellow(X17)
& man(X17)
& young(X17)
& fellow(X18)
& man(X18)
& young(X18)
& X17 = X20
& in(X20,X19)
& X18 = X21
& in(X21,X19) ) )
=> ? [X22,X23,X24,X25,X26,X27,X28,X29,X30] :
( hollywood(X22)
& city(X22)
& event(X23)
& street(X24)
& way(X24)
& lonely(X24)
& chevy(X25)
& car(X25)
& white(X25)
& dirty(X25)
& old(X25)
& barrel(X23,X25)
& down(X23,X24)
& in(X23,X22)
& seat(X28)
& furniture(X28)
& front(X28)
& X26 != X27
& fellow(X26)
& man(X26)
& young(X26)
& fellow(X27)
& man(X27)
& young(X27)
& X26 = X29
& in(X29,X28)
& X27 = X30
& in(X30,X28) ) ),
inference(negate,[],[subgoal_1]) ).
fof(normalize_1_0,plain,
( ( ? [X10,X11,X12,X4,X5,X6,X7,X8,X9] :
( X8 != X9
& X8 = X11
& X9 = X12
& barrel(X5,X6)
& car(X6)
& chevy(X6)
& city(X4)
& dirty(X6)
& down(X5,X7)
& event(X5)
& fellow(X8)
& fellow(X9)
& front(X10)
& furniture(X10)
& hollywood(X4)
& in(X11,X10)
& in(X12,X10)
& in(X5,X4)
& lonely(X7)
& man(X8)
& man(X9)
& old(X6)
& seat(X10)
& street(X7)
& way(X7)
& white(X6)
& young(X8)
& young(X9) )
| ! [U,V,W,X0,X1,X2,X3,Y0,Z] :
( Y0 != X2
| Z != X3
| ~ barrel(V,X0)
| ~ car(X0)
| ~ chevy(X0)
| ~ city(U)
| ~ dirty(X0)
| ~ down(V,W)
| ~ event(V)
| ~ fellow(Y0)
| ~ fellow(Z)
| ~ front(X1)
| ~ furniture(X1)
| ~ hollywood(U)
| ~ in(V,U)
| ~ in(X2,X1)
| ~ in(X3,X1)
| ~ lonely(W)
| ~ man(Y0)
| ~ man(Z)
| ~ old(X0)
| ~ seat(X1)
| ~ street(W)
| ~ way(W)
| ~ white(X0)
| ~ young(Y0)
| ~ young(Z)
| Y0 = Z ) )
& ? [X13,X14,X15,X16,X17,X18,X19,X20,X21] :
( X17 != X18
& X17 = X20
& X18 = X21
& barrel(X14,X15)
& car(X15)
& chevy(X15)
& city(X13)
& dirty(X15)
& down(X14,X16)
& event(X14)
& fellow(X17)
& fellow(X18)
& front(X19)
& furniture(X19)
& hollywood(X13)
& in(X14,X13)
& in(X20,X19)
& in(X21,X19)
& lonely(X16)
& man(X17)
& man(X18)
& old(X15)
& seat(X19)
& street(X16)
& way(X16)
& white(X15)
& young(X17)
& young(X18) )
& ! [X22,X23,X24,X25,X26,X27,X28,X29,X30] :
( X26 != X29
| X27 != X30
| ~ barrel(X23,X25)
| ~ car(X25)
| ~ chevy(X25)
| ~ city(X22)
| ~ dirty(X25)
| ~ down(X23,X24)
| ~ event(X23)
| ~ fellow(X26)
| ~ fellow(X27)
| ~ front(X28)
| ~ furniture(X28)
| ~ hollywood(X22)
| ~ in(X23,X22)
| ~ in(X29,X28)
| ~ in(X30,X28)
| ~ lonely(X24)
| ~ man(X26)
| ~ man(X27)
| ~ old(X25)
| ~ seat(X28)
| ~ street(X24)
| ~ way(X24)
| ~ white(X25)
| ~ young(X26)
| ~ young(X27)
| X26 = X27 ) ),
inference(canonicalize,[],[negate_1_0]) ).
fof(normalize_1_1,plain,
? [X13,X14,X15,X16,X17,X18,X19,X20,X21] :
( X17 != X18
& X17 = X20
& X18 = X21
& barrel(X14,X15)
& car(X15)
& chevy(X15)
& city(X13)
& dirty(X15)
& down(X14,X16)
& event(X14)
& fellow(X17)
& fellow(X18)
& front(X19)
& furniture(X19)
& hollywood(X13)
& in(X14,X13)
& in(X20,X19)
& in(X21,X19)
& lonely(X16)
& man(X17)
& man(X18)
& old(X15)
& seat(X19)
& street(X16)
& way(X16)
& white(X15)
& young(X17)
& young(X18) ),
inference(conjunct,[],[normalize_1_0]) ).
fof(normalize_1_2,plain,
( skolemFOFtoCNF_X17 != skolemFOFtoCNF_X18
& skolemFOFtoCNF_X17 = skolemFOFtoCNF_X20
& skolemFOFtoCNF_X18 = skolemFOFtoCNF_X21
& barrel(skolemFOFtoCNF_X14,skolemFOFtoCNF_X15)
& car(skolemFOFtoCNF_X15)
& chevy(skolemFOFtoCNF_X15)
& city(skolemFOFtoCNF_X13)
& dirty(skolemFOFtoCNF_X15)
& down(skolemFOFtoCNF_X14,skolemFOFtoCNF_X16)
& event(skolemFOFtoCNF_X14)
& fellow(skolemFOFtoCNF_X17)
& fellow(skolemFOFtoCNF_X18)
& front(skolemFOFtoCNF_X19)
& furniture(skolemFOFtoCNF_X19)
& hollywood(skolemFOFtoCNF_X13)
& in(skolemFOFtoCNF_X14,skolemFOFtoCNF_X13)
& in(skolemFOFtoCNF_X20,skolemFOFtoCNF_X19)
& in(skolemFOFtoCNF_X21,skolemFOFtoCNF_X19)
& lonely(skolemFOFtoCNF_X16)
& man(skolemFOFtoCNF_X17)
& man(skolemFOFtoCNF_X18)
& old(skolemFOFtoCNF_X15)
& seat(skolemFOFtoCNF_X19)
& street(skolemFOFtoCNF_X16)
& way(skolemFOFtoCNF_X16)
& white(skolemFOFtoCNF_X15)
& young(skolemFOFtoCNF_X17)
& young(skolemFOFtoCNF_X18) ),
inference(skolemize,[],[normalize_1_1]) ).
fof(normalize_1_3,plain,
barrel(skolemFOFtoCNF_X14,skolemFOFtoCNF_X15),
inference(conjunct,[],[normalize_1_2]) ).
fof(normalize_1_4,plain,
down(skolemFOFtoCNF_X14,skolemFOFtoCNF_X16),
inference(conjunct,[],[normalize_1_2]) ).
fof(normalize_1_5,plain,
in(skolemFOFtoCNF_X20,skolemFOFtoCNF_X19),
inference(conjunct,[],[normalize_1_2]) ).
fof(normalize_1_6,plain,
skolemFOFtoCNF_X17 = skolemFOFtoCNF_X20,
inference(conjunct,[],[normalize_1_2]) ).
fof(normalize_1_7,plain,
in(skolemFOFtoCNF_X14,skolemFOFtoCNF_X13),
inference(conjunct,[],[normalize_1_2]) ).
fof(normalize_1_8,plain,
in(skolemFOFtoCNF_X21,skolemFOFtoCNF_X19),
inference(conjunct,[],[normalize_1_2]) ).
fof(normalize_1_9,plain,
skolemFOFtoCNF_X18 = skolemFOFtoCNF_X21,
inference(conjunct,[],[normalize_1_2]) ).
fof(normalize_1_10,plain,
! [X22,X23,X24,X25,X26,X27,X28,X29,X30] :
( X26 != X29
| X27 != X30
| ~ barrel(X23,X25)
| ~ car(X25)
| ~ chevy(X25)
| ~ city(X22)
| ~ dirty(X25)
| ~ down(X23,X24)
| ~ event(X23)
| ~ fellow(X26)
| ~ fellow(X27)
| ~ front(X28)
| ~ furniture(X28)
| ~ hollywood(X22)
| ~ in(X23,X22)
| ~ in(X29,X28)
| ~ in(X30,X28)
| ~ lonely(X24)
| ~ man(X26)
| ~ man(X27)
| ~ old(X25)
| ~ seat(X28)
| ~ street(X24)
| ~ way(X24)
| ~ white(X25)
| ~ young(X26)
| ~ young(X27)
| X26 = X27 ),
inference(conjunct,[],[normalize_1_0]) ).
fof(normalize_1_11,plain,
! [X22,X23,X24,X25,X26,X27,X28,X29,X30] :
( X26 != X29
| X27 != X30
| ~ barrel(X23,X25)
| ~ car(X25)
| ~ chevy(X25)
| ~ city(X22)
| ~ dirty(X25)
| ~ down(X23,X24)
| ~ event(X23)
| ~ fellow(X26)
| ~ fellow(X27)
| ~ front(X28)
| ~ furniture(X28)
| ~ hollywood(X22)
| ~ in(X23,X22)
| ~ in(X29,X28)
| ~ in(X30,X28)
| ~ lonely(X24)
| ~ man(X26)
| ~ man(X27)
| ~ old(X25)
| ~ seat(X28)
| ~ street(X24)
| ~ way(X24)
| ~ white(X25)
| ~ young(X26)
| ~ young(X27)
| X26 = X27 ),
inference(specialize,[],[normalize_1_10]) ).
fof(normalize_1_12,plain,
fellow(skolemFOFtoCNF_X18),
inference(conjunct,[],[normalize_1_2]) ).
fof(normalize_1_13,plain,
front(skolemFOFtoCNF_X19),
inference(conjunct,[],[normalize_1_2]) ).
fof(normalize_1_14,plain,
furniture(skolemFOFtoCNF_X19),
inference(conjunct,[],[normalize_1_2]) ).
fof(normalize_1_15,plain,
man(skolemFOFtoCNF_X18),
inference(conjunct,[],[normalize_1_2]) ).
fof(normalize_1_16,plain,
seat(skolemFOFtoCNF_X19),
inference(conjunct,[],[normalize_1_2]) ).
fof(normalize_1_17,plain,
young(skolemFOFtoCNF_X18),
inference(conjunct,[],[normalize_1_2]) ).
fof(normalize_1_18,plain,
city(skolemFOFtoCNF_X13),
inference(conjunct,[],[normalize_1_2]) ).
fof(normalize_1_19,plain,
event(skolemFOFtoCNF_X14),
inference(conjunct,[],[normalize_1_2]) ).
fof(normalize_1_20,plain,
hollywood(skolemFOFtoCNF_X13),
inference(conjunct,[],[normalize_1_2]) ).
fof(normalize_1_21,plain,
fellow(skolemFOFtoCNF_X17),
inference(conjunct,[],[normalize_1_2]) ).
fof(normalize_1_22,plain,
man(skolemFOFtoCNF_X17),
inference(conjunct,[],[normalize_1_2]) ).
fof(normalize_1_23,plain,
young(skolemFOFtoCNF_X17),
inference(conjunct,[],[normalize_1_2]) ).
fof(normalize_1_24,plain,
skolemFOFtoCNF_X17 != skolemFOFtoCNF_X18,
inference(conjunct,[],[normalize_1_2]) ).
fof(normalize_1_25,plain,
lonely(skolemFOFtoCNF_X16),
inference(conjunct,[],[normalize_1_2]) ).
fof(normalize_1_26,plain,
street(skolemFOFtoCNF_X16),
inference(conjunct,[],[normalize_1_2]) ).
fof(normalize_1_27,plain,
way(skolemFOFtoCNF_X16),
inference(conjunct,[],[normalize_1_2]) ).
fof(normalize_1_28,plain,
car(skolemFOFtoCNF_X15),
inference(conjunct,[],[normalize_1_2]) ).
fof(normalize_1_29,plain,
chevy(skolemFOFtoCNF_X15),
inference(conjunct,[],[normalize_1_2]) ).
fof(normalize_1_30,plain,
dirty(skolemFOFtoCNF_X15),
inference(conjunct,[],[normalize_1_2]) ).
fof(normalize_1_31,plain,
old(skolemFOFtoCNF_X15),
inference(conjunct,[],[normalize_1_2]) ).
fof(normalize_1_32,plain,
white(skolemFOFtoCNF_X15),
inference(conjunct,[],[normalize_1_2]) ).
cnf(refute_1_0,plain,
barrel(skolemFOFtoCNF_X14,skolemFOFtoCNF_X15),
inference(canonicalize,[],[normalize_1_3]) ).
cnf(refute_1_1,plain,
down(skolemFOFtoCNF_X14,skolemFOFtoCNF_X16),
inference(canonicalize,[],[normalize_1_4]) ).
cnf(refute_1_2,plain,
in(skolemFOFtoCNF_X20,skolemFOFtoCNF_X19),
inference(canonicalize,[],[normalize_1_5]) ).
cnf(refute_1_3,plain,
skolemFOFtoCNF_X17 = skolemFOFtoCNF_X20,
inference(canonicalize,[],[normalize_1_6]) ).
cnf(refute_1_4,plain,
X = X,
introduced(tautology,[refl,[$fot(X)]]) ).
cnf(refute_1_5,plain,
( X != X
| X != Y
| Y = X ),
introduced(tautology,[equality,[$cnf( $equal(X,X) ),[0],$fot(Y)]]) ).
cnf(refute_1_6,plain,
( X != Y
| Y = X ),
inference(resolve,[$cnf( $equal(X,X) )],[refute_1_4,refute_1_5]) ).
cnf(refute_1_7,plain,
( skolemFOFtoCNF_X17 != skolemFOFtoCNF_X20
| skolemFOFtoCNF_X20 = skolemFOFtoCNF_X17 ),
inference(subst,[],[refute_1_6:[bind(X,$fot(skolemFOFtoCNF_X17)),bind(Y,$fot(skolemFOFtoCNF_X20))]]) ).
cnf(refute_1_8,plain,
skolemFOFtoCNF_X20 = skolemFOFtoCNF_X17,
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_X17,skolemFOFtoCNF_X20) )],[refute_1_3,refute_1_7]) ).
cnf(refute_1_9,plain,
( skolemFOFtoCNF_X20 != skolemFOFtoCNF_X17
| ~ in(skolemFOFtoCNF_X20,skolemFOFtoCNF_X19)
| in(skolemFOFtoCNF_X17,skolemFOFtoCNF_X19) ),
introduced(tautology,[equality,[$cnf( in(skolemFOFtoCNF_X20,skolemFOFtoCNF_X19) ),[0],$fot(skolemFOFtoCNF_X17)]]) ).
cnf(refute_1_10,plain,
( ~ in(skolemFOFtoCNF_X20,skolemFOFtoCNF_X19)
| in(skolemFOFtoCNF_X17,skolemFOFtoCNF_X19) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_X20,skolemFOFtoCNF_X17) )],[refute_1_8,refute_1_9]) ).
cnf(refute_1_11,plain,
in(skolemFOFtoCNF_X17,skolemFOFtoCNF_X19),
inference(resolve,[$cnf( in(skolemFOFtoCNF_X20,skolemFOFtoCNF_X19) )],[refute_1_2,refute_1_10]) ).
cnf(refute_1_12,plain,
in(skolemFOFtoCNF_X14,skolemFOFtoCNF_X13),
inference(canonicalize,[],[normalize_1_7]) ).
cnf(refute_1_13,plain,
in(skolemFOFtoCNF_X21,skolemFOFtoCNF_X19),
inference(canonicalize,[],[normalize_1_8]) ).
cnf(refute_1_14,plain,
skolemFOFtoCNF_X18 = skolemFOFtoCNF_X21,
inference(canonicalize,[],[normalize_1_9]) ).
cnf(refute_1_15,plain,
( skolemFOFtoCNF_X18 != skolemFOFtoCNF_X21
| skolemFOFtoCNF_X21 = skolemFOFtoCNF_X18 ),
inference(subst,[],[refute_1_6:[bind(X,$fot(skolemFOFtoCNF_X18)),bind(Y,$fot(skolemFOFtoCNF_X21))]]) ).
cnf(refute_1_16,plain,
skolemFOFtoCNF_X21 = skolemFOFtoCNF_X18,
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_X18,skolemFOFtoCNF_X21) )],[refute_1_14,refute_1_15]) ).
cnf(refute_1_17,plain,
( skolemFOFtoCNF_X21 != skolemFOFtoCNF_X18
| ~ in(skolemFOFtoCNF_X21,skolemFOFtoCNF_X19)
| in(skolemFOFtoCNF_X18,skolemFOFtoCNF_X19) ),
introduced(tautology,[equality,[$cnf( in(skolemFOFtoCNF_X21,skolemFOFtoCNF_X19) ),[0],$fot(skolemFOFtoCNF_X18)]]) ).
cnf(refute_1_18,plain,
( ~ in(skolemFOFtoCNF_X21,skolemFOFtoCNF_X19)
| in(skolemFOFtoCNF_X18,skolemFOFtoCNF_X19) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_X21,skolemFOFtoCNF_X18) )],[refute_1_16,refute_1_17]) ).
cnf(refute_1_19,plain,
in(skolemFOFtoCNF_X18,skolemFOFtoCNF_X19),
inference(resolve,[$cnf( in(skolemFOFtoCNF_X21,skolemFOFtoCNF_X19) )],[refute_1_13,refute_1_18]) ).
cnf(refute_1_20,plain,
( X26 != X29
| X27 != X30
| ~ barrel(X23,X25)
| ~ car(X25)
| ~ chevy(X25)
| ~ city(X22)
| ~ dirty(X25)
| ~ down(X23,X24)
| ~ event(X23)
| ~ fellow(X26)
| ~ fellow(X27)
| ~ front(X28)
| ~ furniture(X28)
| ~ hollywood(X22)
| ~ in(X23,X22)
| ~ in(X29,X28)
| ~ in(X30,X28)
| ~ lonely(X24)
| ~ man(X26)
| ~ man(X27)
| ~ old(X25)
| ~ seat(X28)
| ~ street(X24)
| ~ way(X24)
| ~ white(X25)
| ~ young(X26)
| ~ young(X27)
| X26 = X27 ),
inference(canonicalize,[],[normalize_1_11]) ).
cnf(refute_1_21,plain,
( X29 != X29
| X30 != X30
| ~ barrel(X23,X25)
| ~ car(X25)
| ~ chevy(X25)
| ~ city(X22)
| ~ dirty(X25)
| ~ down(X23,X24)
| ~ event(X23)
| ~ fellow(X29)
| ~ fellow(X30)
| ~ front(X28)
| ~ furniture(X28)
| ~ hollywood(X22)
| ~ in(X23,X22)
| ~ in(X29,X28)
| ~ in(X30,X28)
| ~ lonely(X24)
| ~ man(X29)
| ~ man(X30)
| ~ old(X25)
| ~ seat(X28)
| ~ street(X24)
| ~ way(X24)
| ~ white(X25)
| ~ young(X29)
| ~ young(X30)
| X29 = X30 ),
inference(subst,[],[refute_1_20:[bind(X26,$fot(X29)),bind(X27,$fot(X30))]]) ).
cnf(refute_1_22,plain,
X29 = X29,
introduced(tautology,[refl,[$fot(X29)]]) ).
cnf(refute_1_23,plain,
( X30 != X30
| ~ barrel(X23,X25)
| ~ car(X25)
| ~ chevy(X25)
| ~ city(X22)
| ~ dirty(X25)
| ~ down(X23,X24)
| ~ event(X23)
| ~ fellow(X29)
| ~ fellow(X30)
| ~ front(X28)
| ~ furniture(X28)
| ~ hollywood(X22)
| ~ in(X23,X22)
| ~ in(X29,X28)
| ~ in(X30,X28)
| ~ lonely(X24)
| ~ man(X29)
| ~ man(X30)
| ~ old(X25)
| ~ seat(X28)
| ~ street(X24)
| ~ way(X24)
| ~ white(X25)
| ~ young(X29)
| ~ young(X30)
| X29 = X30 ),
inference(resolve,[$cnf( $equal(X29,X29) )],[refute_1_22,refute_1_21]) ).
cnf(refute_1_24,plain,
X30 = X30,
introduced(tautology,[refl,[$fot(X30)]]) ).
cnf(refute_1_25,plain,
( ~ barrel(X23,X25)
| ~ car(X25)
| ~ chevy(X25)
| ~ city(X22)
| ~ dirty(X25)
| ~ down(X23,X24)
| ~ event(X23)
| ~ fellow(X29)
| ~ fellow(X30)
| ~ front(X28)
| ~ furniture(X28)
| ~ hollywood(X22)
| ~ in(X23,X22)
| ~ in(X29,X28)
| ~ in(X30,X28)
| ~ lonely(X24)
| ~ man(X29)
| ~ man(X30)
| ~ old(X25)
| ~ seat(X28)
| ~ street(X24)
| ~ way(X24)
| ~ white(X25)
| ~ young(X29)
| ~ young(X30)
| X29 = X30 ),
inference(resolve,[$cnf( $equal(X30,X30) )],[refute_1_24,refute_1_23]) ).
cnf(refute_1_26,plain,
( ~ barrel(X_70,X_72)
| ~ car(X_72)
| ~ chevy(X_72)
| ~ city(X_69)
| ~ dirty(X_72)
| ~ down(X_70,X_71)
| ~ event(X_70)
| ~ fellow(X_75)
| ~ fellow(skolemFOFtoCNF_X18)
| ~ front(skolemFOFtoCNF_X19)
| ~ furniture(skolemFOFtoCNF_X19)
| ~ hollywood(X_69)
| ~ in(X_70,X_69)
| ~ in(X_75,skolemFOFtoCNF_X19)
| ~ in(skolemFOFtoCNF_X18,skolemFOFtoCNF_X19)
| ~ lonely(X_71)
| ~ man(X_75)
| ~ man(skolemFOFtoCNF_X18)
| ~ old(X_72)
| ~ seat(skolemFOFtoCNF_X19)
| ~ street(X_71)
| ~ way(X_71)
| ~ white(X_72)
| ~ young(X_75)
| ~ young(skolemFOFtoCNF_X18)
| skolemFOFtoCNF_X18 = X_75 ),
inference(subst,[],[refute_1_25:[bind(X22,$fot(X_69)),bind(X23,$fot(X_70)),bind(X24,$fot(X_71)),bind(X25,$fot(X_72)),bind(X28,$fot(skolemFOFtoCNF_X19)),bind(X29,$fot(skolemFOFtoCNF_X18)),bind(X30,$fot(X_75))]]) ).
cnf(refute_1_27,plain,
( ~ barrel(X_70,X_72)
| ~ car(X_72)
| ~ chevy(X_72)
| ~ city(X_69)
| ~ dirty(X_72)
| ~ down(X_70,X_71)
| ~ event(X_70)
| ~ fellow(X_75)
| ~ fellow(skolemFOFtoCNF_X18)
| ~ front(skolemFOFtoCNF_X19)
| ~ furniture(skolemFOFtoCNF_X19)
| ~ hollywood(X_69)
| ~ in(X_70,X_69)
| ~ in(X_75,skolemFOFtoCNF_X19)
| ~ lonely(X_71)
| ~ man(X_75)
| ~ man(skolemFOFtoCNF_X18)
| ~ old(X_72)
| ~ seat(skolemFOFtoCNF_X19)
| ~ street(X_71)
| ~ way(X_71)
| ~ white(X_72)
| ~ young(X_75)
| ~ young(skolemFOFtoCNF_X18)
| skolemFOFtoCNF_X18 = X_75 ),
inference(resolve,[$cnf( in(skolemFOFtoCNF_X18,skolemFOFtoCNF_X19) )],[refute_1_19,refute_1_26]) ).
cnf(refute_1_28,plain,
fellow(skolemFOFtoCNF_X18),
inference(canonicalize,[],[normalize_1_12]) ).
cnf(refute_1_29,plain,
( ~ barrel(X_70,X_72)
| ~ car(X_72)
| ~ chevy(X_72)
| ~ city(X_69)
| ~ dirty(X_72)
| ~ down(X_70,X_71)
| ~ event(X_70)
| ~ fellow(X_75)
| ~ front(skolemFOFtoCNF_X19)
| ~ furniture(skolemFOFtoCNF_X19)
| ~ hollywood(X_69)
| ~ in(X_70,X_69)
| ~ in(X_75,skolemFOFtoCNF_X19)
| ~ lonely(X_71)
| ~ man(X_75)
| ~ man(skolemFOFtoCNF_X18)
| ~ old(X_72)
| ~ seat(skolemFOFtoCNF_X19)
| ~ street(X_71)
| ~ way(X_71)
| ~ white(X_72)
| ~ young(X_75)
| ~ young(skolemFOFtoCNF_X18)
| skolemFOFtoCNF_X18 = X_75 ),
inference(resolve,[$cnf( fellow(skolemFOFtoCNF_X18) )],[refute_1_28,refute_1_27]) ).
cnf(refute_1_30,plain,
front(skolemFOFtoCNF_X19),
inference(canonicalize,[],[normalize_1_13]) ).
cnf(refute_1_31,plain,
( ~ barrel(X_70,X_72)
| ~ car(X_72)
| ~ chevy(X_72)
| ~ city(X_69)
| ~ dirty(X_72)
| ~ down(X_70,X_71)
| ~ event(X_70)
| ~ fellow(X_75)
| ~ furniture(skolemFOFtoCNF_X19)
| ~ hollywood(X_69)
| ~ in(X_70,X_69)
| ~ in(X_75,skolemFOFtoCNF_X19)
| ~ lonely(X_71)
| ~ man(X_75)
| ~ man(skolemFOFtoCNF_X18)
| ~ old(X_72)
| ~ seat(skolemFOFtoCNF_X19)
| ~ street(X_71)
| ~ way(X_71)
| ~ white(X_72)
| ~ young(X_75)
| ~ young(skolemFOFtoCNF_X18)
| skolemFOFtoCNF_X18 = X_75 ),
inference(resolve,[$cnf( front(skolemFOFtoCNF_X19) )],[refute_1_30,refute_1_29]) ).
cnf(refute_1_32,plain,
furniture(skolemFOFtoCNF_X19),
inference(canonicalize,[],[normalize_1_14]) ).
cnf(refute_1_33,plain,
( ~ barrel(X_70,X_72)
| ~ car(X_72)
| ~ chevy(X_72)
| ~ city(X_69)
| ~ dirty(X_72)
| ~ down(X_70,X_71)
| ~ event(X_70)
| ~ fellow(X_75)
| ~ hollywood(X_69)
| ~ in(X_70,X_69)
| ~ in(X_75,skolemFOFtoCNF_X19)
| ~ lonely(X_71)
| ~ man(X_75)
| ~ man(skolemFOFtoCNF_X18)
| ~ old(X_72)
| ~ seat(skolemFOFtoCNF_X19)
| ~ street(X_71)
| ~ way(X_71)
| ~ white(X_72)
| ~ young(X_75)
| ~ young(skolemFOFtoCNF_X18)
| skolemFOFtoCNF_X18 = X_75 ),
inference(resolve,[$cnf( furniture(skolemFOFtoCNF_X19) )],[refute_1_32,refute_1_31]) ).
cnf(refute_1_34,plain,
man(skolemFOFtoCNF_X18),
inference(canonicalize,[],[normalize_1_15]) ).
cnf(refute_1_35,plain,
( ~ barrel(X_70,X_72)
| ~ car(X_72)
| ~ chevy(X_72)
| ~ city(X_69)
| ~ dirty(X_72)
| ~ down(X_70,X_71)
| ~ event(X_70)
| ~ fellow(X_75)
| ~ hollywood(X_69)
| ~ in(X_70,X_69)
| ~ in(X_75,skolemFOFtoCNF_X19)
| ~ lonely(X_71)
| ~ man(X_75)
| ~ old(X_72)
| ~ seat(skolemFOFtoCNF_X19)
| ~ street(X_71)
| ~ way(X_71)
| ~ white(X_72)
| ~ young(X_75)
| ~ young(skolemFOFtoCNF_X18)
| skolemFOFtoCNF_X18 = X_75 ),
inference(resolve,[$cnf( man(skolemFOFtoCNF_X18) )],[refute_1_34,refute_1_33]) ).
cnf(refute_1_36,plain,
seat(skolemFOFtoCNF_X19),
inference(canonicalize,[],[normalize_1_16]) ).
cnf(refute_1_37,plain,
( ~ barrel(X_70,X_72)
| ~ car(X_72)
| ~ chevy(X_72)
| ~ city(X_69)
| ~ dirty(X_72)
| ~ down(X_70,X_71)
| ~ event(X_70)
| ~ fellow(X_75)
| ~ hollywood(X_69)
| ~ in(X_70,X_69)
| ~ in(X_75,skolemFOFtoCNF_X19)
| ~ lonely(X_71)
| ~ man(X_75)
| ~ old(X_72)
| ~ street(X_71)
| ~ way(X_71)
| ~ white(X_72)
| ~ young(X_75)
| ~ young(skolemFOFtoCNF_X18)
| skolemFOFtoCNF_X18 = X_75 ),
inference(resolve,[$cnf( seat(skolemFOFtoCNF_X19) )],[refute_1_36,refute_1_35]) ).
cnf(refute_1_38,plain,
young(skolemFOFtoCNF_X18),
inference(canonicalize,[],[normalize_1_17]) ).
cnf(refute_1_39,plain,
( ~ barrel(X_70,X_72)
| ~ car(X_72)
| ~ chevy(X_72)
| ~ city(X_69)
| ~ dirty(X_72)
| ~ down(X_70,X_71)
| ~ event(X_70)
| ~ fellow(X_75)
| ~ hollywood(X_69)
| ~ in(X_70,X_69)
| ~ in(X_75,skolemFOFtoCNF_X19)
| ~ lonely(X_71)
| ~ man(X_75)
| ~ old(X_72)
| ~ street(X_71)
| ~ way(X_71)
| ~ white(X_72)
| ~ young(X_75)
| skolemFOFtoCNF_X18 = X_75 ),
inference(resolve,[$cnf( young(skolemFOFtoCNF_X18) )],[refute_1_38,refute_1_37]) ).
cnf(refute_1_40,plain,
( ~ barrel(skolemFOFtoCNF_X14,X_79)
| ~ car(X_79)
| ~ chevy(X_79)
| ~ city(skolemFOFtoCNF_X13)
| ~ dirty(X_79)
| ~ down(skolemFOFtoCNF_X14,X_78)
| ~ event(skolemFOFtoCNF_X14)
| ~ fellow(X_80)
| ~ hollywood(skolemFOFtoCNF_X13)
| ~ in(X_80,skolemFOFtoCNF_X19)
| ~ in(skolemFOFtoCNF_X14,skolemFOFtoCNF_X13)
| ~ lonely(X_78)
| ~ man(X_80)
| ~ old(X_79)
| ~ street(X_78)
| ~ way(X_78)
| ~ white(X_79)
| ~ young(X_80)
| skolemFOFtoCNF_X18 = X_80 ),
inference(subst,[],[refute_1_39:[bind(X_69,$fot(skolemFOFtoCNF_X13)),bind(X_70,$fot(skolemFOFtoCNF_X14)),bind(X_71,$fot(X_78)),bind(X_72,$fot(X_79)),bind(X_75,$fot(X_80))]]) ).
cnf(refute_1_41,plain,
( ~ barrel(skolemFOFtoCNF_X14,X_79)
| ~ car(X_79)
| ~ chevy(X_79)
| ~ city(skolemFOFtoCNF_X13)
| ~ dirty(X_79)
| ~ down(skolemFOFtoCNF_X14,X_78)
| ~ event(skolemFOFtoCNF_X14)
| ~ fellow(X_80)
| ~ hollywood(skolemFOFtoCNF_X13)
| ~ in(X_80,skolemFOFtoCNF_X19)
| ~ lonely(X_78)
| ~ man(X_80)
| ~ old(X_79)
| ~ street(X_78)
| ~ way(X_78)
| ~ white(X_79)
| ~ young(X_80)
| skolemFOFtoCNF_X18 = X_80 ),
inference(resolve,[$cnf( in(skolemFOFtoCNF_X14,skolemFOFtoCNF_X13) )],[refute_1_12,refute_1_40]) ).
cnf(refute_1_42,plain,
city(skolemFOFtoCNF_X13),
inference(canonicalize,[],[normalize_1_18]) ).
cnf(refute_1_43,plain,
( ~ barrel(skolemFOFtoCNF_X14,X_79)
| ~ car(X_79)
| ~ chevy(X_79)
| ~ dirty(X_79)
| ~ down(skolemFOFtoCNF_X14,X_78)
| ~ event(skolemFOFtoCNF_X14)
| ~ fellow(X_80)
| ~ hollywood(skolemFOFtoCNF_X13)
| ~ in(X_80,skolemFOFtoCNF_X19)
| ~ lonely(X_78)
| ~ man(X_80)
| ~ old(X_79)
| ~ street(X_78)
| ~ way(X_78)
| ~ white(X_79)
| ~ young(X_80)
| skolemFOFtoCNF_X18 = X_80 ),
inference(resolve,[$cnf( city(skolemFOFtoCNF_X13) )],[refute_1_42,refute_1_41]) ).
cnf(refute_1_44,plain,
event(skolemFOFtoCNF_X14),
inference(canonicalize,[],[normalize_1_19]) ).
cnf(refute_1_45,plain,
( ~ barrel(skolemFOFtoCNF_X14,X_79)
| ~ car(X_79)
| ~ chevy(X_79)
| ~ dirty(X_79)
| ~ down(skolemFOFtoCNF_X14,X_78)
| ~ fellow(X_80)
| ~ hollywood(skolemFOFtoCNF_X13)
| ~ in(X_80,skolemFOFtoCNF_X19)
| ~ lonely(X_78)
| ~ man(X_80)
| ~ old(X_79)
| ~ street(X_78)
| ~ way(X_78)
| ~ white(X_79)
| ~ young(X_80)
| skolemFOFtoCNF_X18 = X_80 ),
inference(resolve,[$cnf( event(skolemFOFtoCNF_X14) )],[refute_1_44,refute_1_43]) ).
cnf(refute_1_46,plain,
hollywood(skolemFOFtoCNF_X13),
inference(canonicalize,[],[normalize_1_20]) ).
cnf(refute_1_47,plain,
( ~ barrel(skolemFOFtoCNF_X14,X_79)
| ~ car(X_79)
| ~ chevy(X_79)
| ~ dirty(X_79)
| ~ down(skolemFOFtoCNF_X14,X_78)
| ~ fellow(X_80)
| ~ in(X_80,skolemFOFtoCNF_X19)
| ~ lonely(X_78)
| ~ man(X_80)
| ~ old(X_79)
| ~ street(X_78)
| ~ way(X_78)
| ~ white(X_79)
| ~ young(X_80)
| skolemFOFtoCNF_X18 = X_80 ),
inference(resolve,[$cnf( hollywood(skolemFOFtoCNF_X13) )],[refute_1_46,refute_1_45]) ).
cnf(refute_1_48,plain,
( ~ barrel(skolemFOFtoCNF_X14,X_82)
| ~ car(X_82)
| ~ chevy(X_82)
| ~ dirty(X_82)
| ~ down(skolemFOFtoCNF_X14,X_81)
| ~ fellow(skolemFOFtoCNF_X17)
| ~ in(skolemFOFtoCNF_X17,skolemFOFtoCNF_X19)
| ~ lonely(X_81)
| ~ man(skolemFOFtoCNF_X17)
| ~ old(X_82)
| ~ street(X_81)
| ~ way(X_81)
| ~ white(X_82)
| ~ young(skolemFOFtoCNF_X17)
| skolemFOFtoCNF_X18 = skolemFOFtoCNF_X17 ),
inference(subst,[],[refute_1_47:[bind(X_78,$fot(X_81)),bind(X_79,$fot(X_82)),bind(X_80,$fot(skolemFOFtoCNF_X17))]]) ).
cnf(refute_1_49,plain,
( ~ barrel(skolemFOFtoCNF_X14,X_82)
| ~ car(X_82)
| ~ chevy(X_82)
| ~ dirty(X_82)
| ~ down(skolemFOFtoCNF_X14,X_81)
| ~ fellow(skolemFOFtoCNF_X17)
| ~ lonely(X_81)
| ~ man(skolemFOFtoCNF_X17)
| ~ old(X_82)
| ~ street(X_81)
| ~ way(X_81)
| ~ white(X_82)
| ~ young(skolemFOFtoCNF_X17)
| skolemFOFtoCNF_X18 = skolemFOFtoCNF_X17 ),
inference(resolve,[$cnf( in(skolemFOFtoCNF_X17,skolemFOFtoCNF_X19) )],[refute_1_11,refute_1_48]) ).
cnf(refute_1_50,plain,
fellow(skolemFOFtoCNF_X17),
inference(canonicalize,[],[normalize_1_21]) ).
cnf(refute_1_51,plain,
( ~ barrel(skolemFOFtoCNF_X14,X_82)
| ~ car(X_82)
| ~ chevy(X_82)
| ~ dirty(X_82)
| ~ down(skolemFOFtoCNF_X14,X_81)
| ~ lonely(X_81)
| ~ man(skolemFOFtoCNF_X17)
| ~ old(X_82)
| ~ street(X_81)
| ~ way(X_81)
| ~ white(X_82)
| ~ young(skolemFOFtoCNF_X17)
| skolemFOFtoCNF_X18 = skolemFOFtoCNF_X17 ),
inference(resolve,[$cnf( fellow(skolemFOFtoCNF_X17) )],[refute_1_50,refute_1_49]) ).
cnf(refute_1_52,plain,
man(skolemFOFtoCNF_X17),
inference(canonicalize,[],[normalize_1_22]) ).
cnf(refute_1_53,plain,
( ~ barrel(skolemFOFtoCNF_X14,X_82)
| ~ car(X_82)
| ~ chevy(X_82)
| ~ dirty(X_82)
| ~ down(skolemFOFtoCNF_X14,X_81)
| ~ lonely(X_81)
| ~ old(X_82)
| ~ street(X_81)
| ~ way(X_81)
| ~ white(X_82)
| ~ young(skolemFOFtoCNF_X17)
| skolemFOFtoCNF_X18 = skolemFOFtoCNF_X17 ),
inference(resolve,[$cnf( man(skolemFOFtoCNF_X17) )],[refute_1_52,refute_1_51]) ).
cnf(refute_1_54,plain,
young(skolemFOFtoCNF_X17),
inference(canonicalize,[],[normalize_1_23]) ).
cnf(refute_1_55,plain,
( ~ barrel(skolemFOFtoCNF_X14,X_82)
| ~ car(X_82)
| ~ chevy(X_82)
| ~ dirty(X_82)
| ~ down(skolemFOFtoCNF_X14,X_81)
| ~ lonely(X_81)
| ~ old(X_82)
| ~ street(X_81)
| ~ way(X_81)
| ~ white(X_82)
| skolemFOFtoCNF_X18 = skolemFOFtoCNF_X17 ),
inference(resolve,[$cnf( young(skolemFOFtoCNF_X17) )],[refute_1_54,refute_1_53]) ).
cnf(refute_1_56,plain,
skolemFOFtoCNF_X17 != skolemFOFtoCNF_X18,
inference(canonicalize,[],[normalize_1_24]) ).
cnf(refute_1_57,plain,
( skolemFOFtoCNF_X18 != skolemFOFtoCNF_X17
| skolemFOFtoCNF_X17 = skolemFOFtoCNF_X18 ),
inference(subst,[],[refute_1_6:[bind(X,$fot(skolemFOFtoCNF_X18)),bind(Y,$fot(skolemFOFtoCNF_X17))]]) ).
cnf(refute_1_58,plain,
skolemFOFtoCNF_X18 != skolemFOFtoCNF_X17,
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_X17,skolemFOFtoCNF_X18) )],[refute_1_57,refute_1_56]) ).
cnf(refute_1_59,plain,
( ~ barrel(skolemFOFtoCNF_X14,X_82)
| ~ car(X_82)
| ~ chevy(X_82)
| ~ dirty(X_82)
| ~ down(skolemFOFtoCNF_X14,X_81)
| ~ lonely(X_81)
| ~ old(X_82)
| ~ street(X_81)
| ~ way(X_81)
| ~ white(X_82) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_X18,skolemFOFtoCNF_X17) )],[refute_1_55,refute_1_58]) ).
cnf(refute_1_60,plain,
( ~ barrel(skolemFOFtoCNF_X14,X_85)
| ~ car(X_85)
| ~ chevy(X_85)
| ~ dirty(X_85)
| ~ down(skolemFOFtoCNF_X14,skolemFOFtoCNF_X16)
| ~ lonely(skolemFOFtoCNF_X16)
| ~ old(X_85)
| ~ street(skolemFOFtoCNF_X16)
| ~ way(skolemFOFtoCNF_X16)
| ~ white(X_85) ),
inference(subst,[],[refute_1_59:[bind(X_81,$fot(skolemFOFtoCNF_X16)),bind(X_82,$fot(X_85))]]) ).
cnf(refute_1_61,plain,
( ~ barrel(skolemFOFtoCNF_X14,X_85)
| ~ car(X_85)
| ~ chevy(X_85)
| ~ dirty(X_85)
| ~ lonely(skolemFOFtoCNF_X16)
| ~ old(X_85)
| ~ street(skolemFOFtoCNF_X16)
| ~ way(skolemFOFtoCNF_X16)
| ~ white(X_85) ),
inference(resolve,[$cnf( down(skolemFOFtoCNF_X14,skolemFOFtoCNF_X16) )],[refute_1_1,refute_1_60]) ).
cnf(refute_1_62,plain,
lonely(skolemFOFtoCNF_X16),
inference(canonicalize,[],[normalize_1_25]) ).
cnf(refute_1_63,plain,
( ~ barrel(skolemFOFtoCNF_X14,X_85)
| ~ car(X_85)
| ~ chevy(X_85)
| ~ dirty(X_85)
| ~ old(X_85)
| ~ street(skolemFOFtoCNF_X16)
| ~ way(skolemFOFtoCNF_X16)
| ~ white(X_85) ),
inference(resolve,[$cnf( lonely(skolemFOFtoCNF_X16) )],[refute_1_62,refute_1_61]) ).
cnf(refute_1_64,plain,
street(skolemFOFtoCNF_X16),
inference(canonicalize,[],[normalize_1_26]) ).
cnf(refute_1_65,plain,
( ~ barrel(skolemFOFtoCNF_X14,X_85)
| ~ car(X_85)
| ~ chevy(X_85)
| ~ dirty(X_85)
| ~ old(X_85)
| ~ way(skolemFOFtoCNF_X16)
| ~ white(X_85) ),
inference(resolve,[$cnf( street(skolemFOFtoCNF_X16) )],[refute_1_64,refute_1_63]) ).
cnf(refute_1_66,plain,
way(skolemFOFtoCNF_X16),
inference(canonicalize,[],[normalize_1_27]) ).
cnf(refute_1_67,plain,
( ~ barrel(skolemFOFtoCNF_X14,X_85)
| ~ car(X_85)
| ~ chevy(X_85)
| ~ dirty(X_85)
| ~ old(X_85)
| ~ white(X_85) ),
inference(resolve,[$cnf( way(skolemFOFtoCNF_X16) )],[refute_1_66,refute_1_65]) ).
cnf(refute_1_68,plain,
( ~ barrel(skolemFOFtoCNF_X14,skolemFOFtoCNF_X15)
| ~ car(skolemFOFtoCNF_X15)
| ~ chevy(skolemFOFtoCNF_X15)
| ~ dirty(skolemFOFtoCNF_X15)
| ~ old(skolemFOFtoCNF_X15)
| ~ white(skolemFOFtoCNF_X15) ),
inference(subst,[],[refute_1_67:[bind(X_85,$fot(skolemFOFtoCNF_X15))]]) ).
cnf(refute_1_69,plain,
( ~ car(skolemFOFtoCNF_X15)
| ~ chevy(skolemFOFtoCNF_X15)
| ~ dirty(skolemFOFtoCNF_X15)
| ~ old(skolemFOFtoCNF_X15)
| ~ white(skolemFOFtoCNF_X15) ),
inference(resolve,[$cnf( barrel(skolemFOFtoCNF_X14,skolemFOFtoCNF_X15) )],[refute_1_0,refute_1_68]) ).
cnf(refute_1_70,plain,
car(skolemFOFtoCNF_X15),
inference(canonicalize,[],[normalize_1_28]) ).
cnf(refute_1_71,plain,
( ~ chevy(skolemFOFtoCNF_X15)
| ~ dirty(skolemFOFtoCNF_X15)
| ~ old(skolemFOFtoCNF_X15)
| ~ white(skolemFOFtoCNF_X15) ),
inference(resolve,[$cnf( car(skolemFOFtoCNF_X15) )],[refute_1_70,refute_1_69]) ).
cnf(refute_1_72,plain,
chevy(skolemFOFtoCNF_X15),
inference(canonicalize,[],[normalize_1_29]) ).
cnf(refute_1_73,plain,
( ~ dirty(skolemFOFtoCNF_X15)
| ~ old(skolemFOFtoCNF_X15)
| ~ white(skolemFOFtoCNF_X15) ),
inference(resolve,[$cnf( chevy(skolemFOFtoCNF_X15) )],[refute_1_72,refute_1_71]) ).
cnf(refute_1_74,plain,
dirty(skolemFOFtoCNF_X15),
inference(canonicalize,[],[normalize_1_30]) ).
cnf(refute_1_75,plain,
( ~ old(skolemFOFtoCNF_X15)
| ~ white(skolemFOFtoCNF_X15) ),
inference(resolve,[$cnf( dirty(skolemFOFtoCNF_X15) )],[refute_1_74,refute_1_73]) ).
cnf(refute_1_76,plain,
old(skolemFOFtoCNF_X15),
inference(canonicalize,[],[normalize_1_31]) ).
cnf(refute_1_77,plain,
~ white(skolemFOFtoCNF_X15),
inference(resolve,[$cnf( old(skolemFOFtoCNF_X15) )],[refute_1_76,refute_1_75]) ).
cnf(refute_1_78,plain,
white(skolemFOFtoCNF_X15),
inference(canonicalize,[],[normalize_1_32]) ).
cnf(refute_1_79,plain,
$false,
inference(resolve,[$cnf( white(skolemFOFtoCNF_X15) )],[refute_1_78,refute_1_77]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : NLP009+1 : TPTP v8.1.0. Released v2.4.0.
% 0.12/0.12 % Command : metis --show proof --show saturation %s
% 0.12/0.33 % Computer : n023.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Fri Jul 1 01:01:59 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.19/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.19/0.41 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.41
% 0.19/0.41 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 0.19/0.45
%------------------------------------------------------------------------------