%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : NLP208+1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n007.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:16:05 EDT 2022
% Result : Theorem 0.18s 0.41s
% Output : CNFRefutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 13
% Syntax : Number of formulae : 76 ( 19 unt; 0 def)
% Number of atoms : 455 ( 16 equ)
% Maximal formula atoms : 48 ( 5 avg)
% Number of connectives : 453 ( 74 ~; 63 |; 288 &)
% ( 0 <=>; 28 =>; 0 <=; 0 <~>)
% Maximal formula depth : 52 ( 7 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 46 ( 43 usr; 1 prp; 0-4 aty)
% Number of functors : 11 ( 11 usr; 11 con; 0-0 aty)
% Number of variables : 205 ( 2 sgn 117 !; 63 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax25,axiom,
! [U,V] :
( human_person(U,V)
=> animate(U,V) ) ).
fof(ax31,axiom,
! [U,V] :
( man(U,V)
=> human_person(U,V) ) ).
fof(ax40,axiom,
! [U,V] :
( object(U,V)
=> nonliving(U,V) ) ).
fof(ax45,axiom,
! [U,V] :
( artifact(U,V)
=> object(U,V) ) ).
fof(ax46,axiom,
! [U,V] :
( instrumentality(U,V)
=> artifact(U,V) ) ).
fof(ax47,axiom,
! [U,V] :
( device(U,V)
=> instrumentality(U,V) ) ).
fof(ax48,axiom,
! [U,V] :
( wheel(U,V)
=> device(U,V) ) ).
fof(ax57,axiom,
! [U,V] :
( animate(U,V)
=> ~ nonliving(U,V) ) ).
fof(ax71,axiom,
! [U,V,W,X] :
( be(U,V,W,X)
=> W = X ) ).
fof(co1,conjecture,
~ ? [U] :
( actual_world(U)
& ? [V,W,X,Y0,Z,X1,X2,X3,X4,X5] :
( of(U,W,V)
& man(U,V)
& jules_forename(U,W)
& forename(U,W)
& frontseat(U,Z)
& chevy(U,X)
& white(U,X)
& dirty(U,X)
& old(U,X)
& of(U,Y0,Z)
& city(U,Z)
& hollywood_placename(U,Y0)
& placename(U,Y0)
& street(U,Z)
& lonely(U,Z)
& event(U,X1)
& agent(U,X1,X)
& present(U,X1)
& barrel(U,X1)
& down(U,X1,Z)
& in(U,X1,Z)
& ! [X6] :
( member(U,X6,X2)
=> ? [X7,X8] :
( state(U,X7)
& be(U,X7,X6,X8)
& in(U,X8,Z) ) )
& two(U,X2)
& group(U,X2)
& ! [X9] :
( member(U,X9,X2)
=> ( fellow(U,X9)
& young(U,X9) ) )
& ! [X10] :
( member(U,X10,X3)
=> ! [X11] :
( member(U,X11,X2)
=> ? [X12] :
( event(U,X12)
& agent(U,X12,X11)
& patient(U,X12,X10)
& present(U,X12)
& nonreflexive(U,X12)
& wear(U,X12) ) ) )
& group(U,X3)
& ! [X13] :
( member(U,X13,X3)
=> ( coat(U,X13)
& black(U,X13)
& cheap(U,X13) ) )
& wheel(U,X5)
& state(U,X4)
& be(U,X4,V,X5)
& behind(U,X5,X5) ) ) ).
fof(subgoal_0,plain,
! [U] :
( actual_world(U)
=> ! [V,W,X,Y0,Z,X1,X2,X3,X4,X5] :
( ( of(U,W,V)
& man(U,V)
& jules_forename(U,W)
& forename(U,W)
& frontseat(U,Z)
& chevy(U,X)
& white(U,X)
& dirty(U,X)
& old(U,X)
& of(U,Y0,Z)
& city(U,Z)
& hollywood_placename(U,Y0)
& placename(U,Y0)
& street(U,Z)
& lonely(U,Z)
& event(U,X1)
& agent(U,X1,X)
& present(U,X1)
& barrel(U,X1)
& down(U,X1,Z)
& in(U,X1,Z)
& ! [X6] :
( member(U,X6,X2)
=> ? [X7,X8] :
( state(U,X7)
& be(U,X7,X6,X8)
& in(U,X8,Z) ) )
& two(U,X2)
& group(U,X2)
& ! [X9] :
( member(U,X9,X2)
=> ( fellow(U,X9)
& young(U,X9) ) )
& ! [X10] :
( member(U,X10,X3)
=> ! [X11] :
( member(U,X11,X2)
=> ? [X12] :
( event(U,X12)
& agent(U,X12,X11)
& patient(U,X12,X10)
& present(U,X12)
& nonreflexive(U,X12)
& wear(U,X12) ) ) )
& group(U,X3)
& ! [X13] :
( member(U,X13,X3)
=> ( coat(U,X13)
& black(U,X13)
& cheap(U,X13) ) )
& wheel(U,X5)
& state(U,X4)
& be(U,X4,V,X5) )
=> ~ behind(U,X5,X5) ) ),
inference(strip,[],[co1]) ).
fof(negate_0_0,plain,
~ ! [U] :
( actual_world(U)
=> ! [V,W,X,Y0,Z,X1,X2,X3,X4,X5] :
( ( of(U,W,V)
& man(U,V)
& jules_forename(U,W)
& forename(U,W)
& frontseat(U,Z)
& chevy(U,X)
& white(U,X)
& dirty(U,X)
& old(U,X)
& of(U,Y0,Z)
& city(U,Z)
& hollywood_placename(U,Y0)
& placename(U,Y0)
& street(U,Z)
& lonely(U,Z)
& event(U,X1)
& agent(U,X1,X)
& present(U,X1)
& barrel(U,X1)
& down(U,X1,Z)
& in(U,X1,Z)
& ! [X6] :
( member(U,X6,X2)
=> ? [X7,X8] :
( state(U,X7)
& be(U,X7,X6,X8)
& in(U,X8,Z) ) )
& two(U,X2)
& group(U,X2)
& ! [X9] :
( member(U,X9,X2)
=> ( fellow(U,X9)
& young(U,X9) ) )
& ! [X10] :
( member(U,X10,X3)
=> ! [X11] :
( member(U,X11,X2)
=> ? [X12] :
( event(U,X12)
& agent(U,X12,X11)
& patient(U,X12,X10)
& present(U,X12)
& nonreflexive(U,X12)
& wear(U,X12) ) ) )
& group(U,X3)
& ! [X13] :
( member(U,X13,X3)
=> ( coat(U,X13)
& black(U,X13)
& cheap(U,X13) ) )
& wheel(U,X5)
& state(U,X4)
& be(U,X4,V,X5) )
=> ~ behind(U,X5,X5) ) ),
inference(negate,[],[subgoal_0]) ).
fof(normalize_0_0,plain,
! [U,V] :
( ~ animate(U,V)
| ~ nonliving(U,V) ),
inference(canonicalize,[],[ax57]) ).
fof(normalize_0_1,plain,
! [U,V] :
( ~ animate(U,V)
| ~ nonliving(U,V) ),
inference(specialize,[],[normalize_0_0]) ).
fof(normalize_0_2,plain,
! [U,V] :
( ~ object(U,V)
| nonliving(U,V) ),
inference(canonicalize,[],[ax40]) ).
fof(normalize_0_3,plain,
! [U,V] :
( ~ object(U,V)
| nonliving(U,V) ),
inference(specialize,[],[normalize_0_2]) ).
fof(normalize_0_4,plain,
! [U,V] :
( ~ artifact(U,V)
| object(U,V) ),
inference(canonicalize,[],[ax45]) ).
fof(normalize_0_5,plain,
! [U,V] :
( ~ artifact(U,V)
| object(U,V) ),
inference(specialize,[],[normalize_0_4]) ).
fof(normalize_0_6,plain,
! [U,V] :
( ~ instrumentality(U,V)
| artifact(U,V) ),
inference(canonicalize,[],[ax46]) ).
fof(normalize_0_7,plain,
! [U,V] :
( ~ instrumentality(U,V)
| artifact(U,V) ),
inference(specialize,[],[normalize_0_6]) ).
fof(normalize_0_8,plain,
! [U,V] :
( ~ device(U,V)
| instrumentality(U,V) ),
inference(canonicalize,[],[ax47]) ).
fof(normalize_0_9,plain,
! [U,V] :
( ~ device(U,V)
| instrumentality(U,V) ),
inference(specialize,[],[normalize_0_8]) ).
fof(normalize_0_10,plain,
? [U] :
( actual_world(U)
& ? [V,W,X,X1,X2,X3,X4,X5,Y0,Z] :
( agent(U,X1,X)
& barrel(U,X1)
& be(U,X4,V,X5)
& behind(U,X5,X5)
& chevy(U,X)
& city(U,Z)
& dirty(U,X)
& down(U,X1,Z)
& event(U,X1)
& forename(U,W)
& frontseat(U,Z)
& group(U,X2)
& group(U,X3)
& hollywood_placename(U,Y0)
& in(U,X1,Z)
& jules_forename(U,W)
& lonely(U,Z)
& man(U,V)
& of(U,W,V)
& of(U,Y0,Z)
& old(U,X)
& placename(U,Y0)
& present(U,X1)
& state(U,X4)
& street(U,Z)
& two(U,X2)
& wheel(U,X5)
& white(U,X)
& ! [X10] :
( ~ member(U,X10,X3)
| ! [X11] :
( ~ member(U,X11,X2)
| ? [X12] :
( agent(U,X12,X11)
& event(U,X12)
& nonreflexive(U,X12)
& patient(U,X12,X10)
& present(U,X12)
& wear(U,X12) ) ) )
& ! [X13] :
( ~ member(U,X13,X3)
| ( black(U,X13)
& cheap(U,X13)
& coat(U,X13) ) )
& ! [X6] :
( ~ member(U,X6,X2)
| ? [X7,X8] :
( be(U,X7,X6,X8)
& in(U,X8,Z)
& state(U,X7) ) )
& ! [X9] :
( ~ member(U,X9,X2)
| ( fellow(U,X9)
& young(U,X9) ) ) ) ),
inference(canonicalize,[],[negate_0_0]) ).
fof(normalize_0_11,plain,
( actual_world(skolemFOFtoCNF_U)
& ? [V,W,X,X1,X2,X3,X4,X5,Y0,Z] :
( agent(skolemFOFtoCNF_U,X1,X)
& barrel(skolemFOFtoCNF_U,X1)
& be(skolemFOFtoCNF_U,X4,V,X5)
& behind(skolemFOFtoCNF_U,X5,X5)
& chevy(skolemFOFtoCNF_U,X)
& city(skolemFOFtoCNF_U,Z)
& dirty(skolemFOFtoCNF_U,X)
& down(skolemFOFtoCNF_U,X1,Z)
& event(skolemFOFtoCNF_U,X1)
& forename(skolemFOFtoCNF_U,W)
& frontseat(skolemFOFtoCNF_U,Z)
& group(skolemFOFtoCNF_U,X2)
& group(skolemFOFtoCNF_U,X3)
& hollywood_placename(skolemFOFtoCNF_U,Y0)
& in(skolemFOFtoCNF_U,X1,Z)
& jules_forename(skolemFOFtoCNF_U,W)
& lonely(skolemFOFtoCNF_U,Z)
& man(skolemFOFtoCNF_U,V)
& of(skolemFOFtoCNF_U,W,V)
& of(skolemFOFtoCNF_U,Y0,Z)
& old(skolemFOFtoCNF_U,X)
& placename(skolemFOFtoCNF_U,Y0)
& present(skolemFOFtoCNF_U,X1)
& state(skolemFOFtoCNF_U,X4)
& street(skolemFOFtoCNF_U,Z)
& two(skolemFOFtoCNF_U,X2)
& wheel(skolemFOFtoCNF_U,X5)
& white(skolemFOFtoCNF_U,X)
& ! [X10] :
( ~ member(skolemFOFtoCNF_U,X10,X3)
| ! [X11] :
( ~ member(skolemFOFtoCNF_U,X11,X2)
| ? [X12] :
( agent(skolemFOFtoCNF_U,X12,X11)
& event(skolemFOFtoCNF_U,X12)
& nonreflexive(skolemFOFtoCNF_U,X12)
& patient(skolemFOFtoCNF_U,X12,X10)
& present(skolemFOFtoCNF_U,X12)
& wear(skolemFOFtoCNF_U,X12) ) ) )
& ! [X13] :
( ~ member(skolemFOFtoCNF_U,X13,X3)
| ( black(skolemFOFtoCNF_U,X13)
& cheap(skolemFOFtoCNF_U,X13)
& coat(skolemFOFtoCNF_U,X13) ) )
& ! [X6] :
( ~ member(skolemFOFtoCNF_U,X6,X2)
| ? [X7,X8] :
( be(skolemFOFtoCNF_U,X7,X6,X8)
& in(skolemFOFtoCNF_U,X8,Z)
& state(skolemFOFtoCNF_U,X7) ) )
& ! [X9] :
( ~ member(skolemFOFtoCNF_U,X9,X2)
| ( fellow(skolemFOFtoCNF_U,X9)
& young(skolemFOFtoCNF_U,X9) ) ) ) ),
inference(skolemize,[],[normalize_0_10]) ).
fof(normalize_0_12,plain,
? [V,W,X,X1,X2,X3,X4,X5,Y0,Z] :
( agent(skolemFOFtoCNF_U,X1,X)
& barrel(skolemFOFtoCNF_U,X1)
& be(skolemFOFtoCNF_U,X4,V,X5)
& behind(skolemFOFtoCNF_U,X5,X5)
& chevy(skolemFOFtoCNF_U,X)
& city(skolemFOFtoCNF_U,Z)
& dirty(skolemFOFtoCNF_U,X)
& down(skolemFOFtoCNF_U,X1,Z)
& event(skolemFOFtoCNF_U,X1)
& forename(skolemFOFtoCNF_U,W)
& frontseat(skolemFOFtoCNF_U,Z)
& group(skolemFOFtoCNF_U,X2)
& group(skolemFOFtoCNF_U,X3)
& hollywood_placename(skolemFOFtoCNF_U,Y0)
& in(skolemFOFtoCNF_U,X1,Z)
& jules_forename(skolemFOFtoCNF_U,W)
& lonely(skolemFOFtoCNF_U,Z)
& man(skolemFOFtoCNF_U,V)
& of(skolemFOFtoCNF_U,W,V)
& of(skolemFOFtoCNF_U,Y0,Z)
& old(skolemFOFtoCNF_U,X)
& placename(skolemFOFtoCNF_U,Y0)
& present(skolemFOFtoCNF_U,X1)
& state(skolemFOFtoCNF_U,X4)
& street(skolemFOFtoCNF_U,Z)
& two(skolemFOFtoCNF_U,X2)
& wheel(skolemFOFtoCNF_U,X5)
& white(skolemFOFtoCNF_U,X)
& ! [X10] :
( ~ member(skolemFOFtoCNF_U,X10,X3)
| ! [X11] :
( ~ member(skolemFOFtoCNF_U,X11,X2)
| ? [X12] :
( agent(skolemFOFtoCNF_U,X12,X11)
& event(skolemFOFtoCNF_U,X12)
& nonreflexive(skolemFOFtoCNF_U,X12)
& patient(skolemFOFtoCNF_U,X12,X10)
& present(skolemFOFtoCNF_U,X12)
& wear(skolemFOFtoCNF_U,X12) ) ) )
& ! [X13] :
( ~ member(skolemFOFtoCNF_U,X13,X3)
| ( black(skolemFOFtoCNF_U,X13)
& cheap(skolemFOFtoCNF_U,X13)
& coat(skolemFOFtoCNF_U,X13) ) )
& ! [X6] :
( ~ member(skolemFOFtoCNF_U,X6,X2)
| ? [X7,X8] :
( be(skolemFOFtoCNF_U,X7,X6,X8)
& in(skolemFOFtoCNF_U,X8,Z)
& state(skolemFOFtoCNF_U,X7) ) )
& ! [X9] :
( ~ member(skolemFOFtoCNF_U,X9,X2)
| ( fellow(skolemFOFtoCNF_U,X9)
& young(skolemFOFtoCNF_U,X9) ) ) ),
inference(conjunct,[],[normalize_0_11]) ).
fof(normalize_0_13,plain,
( agent(skolemFOFtoCNF_U,skolemFOFtoCNF_X1,skolemFOFtoCNF_X_1)
& barrel(skolemFOFtoCNF_U,skolemFOFtoCNF_X1)
& be(skolemFOFtoCNF_U,skolemFOFtoCNF_X4,skolemFOFtoCNF_V,skolemFOFtoCNF_X5)
& behind(skolemFOFtoCNF_U,skolemFOFtoCNF_X5,skolemFOFtoCNF_X5)
& chevy(skolemFOFtoCNF_U,skolemFOFtoCNF_X_1)
& city(skolemFOFtoCNF_U,skolemFOFtoCNF_Z)
& dirty(skolemFOFtoCNF_U,skolemFOFtoCNF_X_1)
& down(skolemFOFtoCNF_U,skolemFOFtoCNF_X1,skolemFOFtoCNF_Z)
& event(skolemFOFtoCNF_U,skolemFOFtoCNF_X1)
& forename(skolemFOFtoCNF_U,skolemFOFtoCNF_W_1)
& frontseat(skolemFOFtoCNF_U,skolemFOFtoCNF_Z)
& group(skolemFOFtoCNF_U,skolemFOFtoCNF_X2)
& group(skolemFOFtoCNF_U,skolemFOFtoCNF_X3)
& hollywood_placename(skolemFOFtoCNF_U,skolemFOFtoCNF_Y_1)
& in(skolemFOFtoCNF_U,skolemFOFtoCNF_X1,skolemFOFtoCNF_Z)
& jules_forename(skolemFOFtoCNF_U,skolemFOFtoCNF_W_1)
& lonely(skolemFOFtoCNF_U,skolemFOFtoCNF_Z)
& man(skolemFOFtoCNF_U,skolemFOFtoCNF_V)
& of(skolemFOFtoCNF_U,skolemFOFtoCNF_W_1,skolemFOFtoCNF_V)
& of(skolemFOFtoCNF_U,skolemFOFtoCNF_Y_1,skolemFOFtoCNF_Z)
& old(skolemFOFtoCNF_U,skolemFOFtoCNF_X_1)
& placename(skolemFOFtoCNF_U,skolemFOFtoCNF_Y_1)
& present(skolemFOFtoCNF_U,skolemFOFtoCNF_X1)
& state(skolemFOFtoCNF_U,skolemFOFtoCNF_X4)
& street(skolemFOFtoCNF_U,skolemFOFtoCNF_Z)
& two(skolemFOFtoCNF_U,skolemFOFtoCNF_X2)
& wheel(skolemFOFtoCNF_U,skolemFOFtoCNF_X5)
& white(skolemFOFtoCNF_U,skolemFOFtoCNF_X_1)
& ! [X10] :
( ~ member(skolemFOFtoCNF_U,X10,skolemFOFtoCNF_X3)
| ! [X11] :
( ~ member(skolemFOFtoCNF_U,X11,skolemFOFtoCNF_X2)
| ? [X12] :
( agent(skolemFOFtoCNF_U,X12,X11)
& event(skolemFOFtoCNF_U,X12)
& nonreflexive(skolemFOFtoCNF_U,X12)
& patient(skolemFOFtoCNF_U,X12,X10)
& present(skolemFOFtoCNF_U,X12)
& wear(skolemFOFtoCNF_U,X12) ) ) )
& ! [X13] :
( ~ member(skolemFOFtoCNF_U,X13,skolemFOFtoCNF_X3)
| ( black(skolemFOFtoCNF_U,X13)
& cheap(skolemFOFtoCNF_U,X13)
& coat(skolemFOFtoCNF_U,X13) ) )
& ! [X6] :
( ~ member(skolemFOFtoCNF_U,X6,skolemFOFtoCNF_X2)
| ? [X7,X8] :
( be(skolemFOFtoCNF_U,X7,X6,X8)
& in(skolemFOFtoCNF_U,X8,skolemFOFtoCNF_Z)
& state(skolemFOFtoCNF_U,X7) ) )
& ! [X9] :
( ~ member(skolemFOFtoCNF_U,X9,skolemFOFtoCNF_X2)
| ( fellow(skolemFOFtoCNF_U,X9)
& young(skolemFOFtoCNF_U,X9) ) ) ),
inference(skolemize,[],[normalize_0_12]) ).
fof(normalize_0_14,plain,
wheel(skolemFOFtoCNF_U,skolemFOFtoCNF_X5),
inference(conjunct,[],[normalize_0_13]) ).
fof(normalize_0_15,plain,
! [U,V] :
( ~ wheel(U,V)
| device(U,V) ),
inference(canonicalize,[],[ax48]) ).
fof(normalize_0_16,plain,
! [U,V] :
( ~ wheel(U,V)
| device(U,V) ),
inference(specialize,[],[normalize_0_15]) ).
fof(normalize_0_17,plain,
be(skolemFOFtoCNF_U,skolemFOFtoCNF_X4,skolemFOFtoCNF_V,skolemFOFtoCNF_X5),
inference(conjunct,[],[normalize_0_13]) ).
fof(normalize_0_18,plain,
! [U,V,W,X] :
( ~ be(U,V,W,X)
| W = X ),
inference(canonicalize,[],[ax71]) ).
fof(normalize_0_19,plain,
! [U,V,W,X] :
( ~ be(U,V,W,X)
| W = X ),
inference(specialize,[],[normalize_0_18]) ).
fof(normalize_0_20,plain,
man(skolemFOFtoCNF_U,skolemFOFtoCNF_V),
inference(conjunct,[],[normalize_0_13]) ).
fof(normalize_0_21,plain,
! [U,V] :
( ~ man(U,V)
| human_person(U,V) ),
inference(canonicalize,[],[ax31]) ).
fof(normalize_0_22,plain,
! [U,V] :
( ~ man(U,V)
| human_person(U,V) ),
inference(specialize,[],[normalize_0_21]) ).
fof(normalize_0_23,plain,
! [U,V] :
( ~ human_person(U,V)
| animate(U,V) ),
inference(canonicalize,[],[ax25]) ).
fof(normalize_0_24,plain,
! [U,V] :
( ~ human_person(U,V)
| animate(U,V) ),
inference(specialize,[],[normalize_0_23]) ).
cnf(refute_0_0,plain,
( ~ animate(U,V)
| ~ nonliving(U,V) ),
inference(canonicalize,[],[normalize_0_1]) ).
cnf(refute_0_1,plain,
( ~ animate(skolemFOFtoCNF_U,skolemFOFtoCNF_X5)
| ~ nonliving(skolemFOFtoCNF_U,skolemFOFtoCNF_X5) ),
inference(subst,[],[refute_0_0:[bind(U,$fot(skolemFOFtoCNF_U)),bind(V,$fot(skolemFOFtoCNF_X5))]]) ).
cnf(refute_0_2,plain,
( ~ object(U,V)
| nonliving(U,V) ),
inference(canonicalize,[],[normalize_0_3]) ).
cnf(refute_0_3,plain,
( ~ object(skolemFOFtoCNF_U,skolemFOFtoCNF_X5)
| nonliving(skolemFOFtoCNF_U,skolemFOFtoCNF_X5) ),
inference(subst,[],[refute_0_2:[bind(U,$fot(skolemFOFtoCNF_U)),bind(V,$fot(skolemFOFtoCNF_X5))]]) ).
cnf(refute_0_4,plain,
( ~ artifact(U,V)
| object(U,V) ),
inference(canonicalize,[],[normalize_0_5]) ).
cnf(refute_0_5,plain,
( ~ artifact(skolemFOFtoCNF_U,skolemFOFtoCNF_X5)
| object(skolemFOFtoCNF_U,skolemFOFtoCNF_X5) ),
inference(subst,[],[refute_0_4:[bind(U,$fot(skolemFOFtoCNF_U)),bind(V,$fot(skolemFOFtoCNF_X5))]]) ).
cnf(refute_0_6,plain,
( ~ instrumentality(U,V)
| artifact(U,V) ),
inference(canonicalize,[],[normalize_0_7]) ).
cnf(refute_0_7,plain,
( ~ instrumentality(skolemFOFtoCNF_U,skolemFOFtoCNF_X5)
| artifact(skolemFOFtoCNF_U,skolemFOFtoCNF_X5) ),
inference(subst,[],[refute_0_6:[bind(U,$fot(skolemFOFtoCNF_U)),bind(V,$fot(skolemFOFtoCNF_X5))]]) ).
cnf(refute_0_8,plain,
( ~ device(U,V)
| instrumentality(U,V) ),
inference(canonicalize,[],[normalize_0_9]) ).
cnf(refute_0_9,plain,
( ~ device(skolemFOFtoCNF_U,skolemFOFtoCNF_X5)
| instrumentality(skolemFOFtoCNF_U,skolemFOFtoCNF_X5) ),
inference(subst,[],[refute_0_8:[bind(U,$fot(skolemFOFtoCNF_U)),bind(V,$fot(skolemFOFtoCNF_X5))]]) ).
cnf(refute_0_10,plain,
wheel(skolemFOFtoCNF_U,skolemFOFtoCNF_X5),
inference(canonicalize,[],[normalize_0_14]) ).
cnf(refute_0_11,plain,
( ~ wheel(U,V)
| device(U,V) ),
inference(canonicalize,[],[normalize_0_16]) ).
cnf(refute_0_12,plain,
( ~ wheel(skolemFOFtoCNF_U,skolemFOFtoCNF_X5)
| device(skolemFOFtoCNF_U,skolemFOFtoCNF_X5) ),
inference(subst,[],[refute_0_11:[bind(U,$fot(skolemFOFtoCNF_U)),bind(V,$fot(skolemFOFtoCNF_X5))]]) ).
cnf(refute_0_13,plain,
device(skolemFOFtoCNF_U,skolemFOFtoCNF_X5),
inference(resolve,[$cnf( wheel(skolemFOFtoCNF_U,skolemFOFtoCNF_X5) )],[refute_0_10,refute_0_12]) ).
cnf(refute_0_14,plain,
instrumentality(skolemFOFtoCNF_U,skolemFOFtoCNF_X5),
inference(resolve,[$cnf( device(skolemFOFtoCNF_U,skolemFOFtoCNF_X5) )],[refute_0_13,refute_0_9]) ).
cnf(refute_0_15,plain,
artifact(skolemFOFtoCNF_U,skolemFOFtoCNF_X5),
inference(resolve,[$cnf( instrumentality(skolemFOFtoCNF_U,skolemFOFtoCNF_X5) )],[refute_0_14,refute_0_7]) ).
cnf(refute_0_16,plain,
object(skolemFOFtoCNF_U,skolemFOFtoCNF_X5),
inference(resolve,[$cnf( artifact(skolemFOFtoCNF_U,skolemFOFtoCNF_X5) )],[refute_0_15,refute_0_5]) ).
cnf(refute_0_17,plain,
nonliving(skolemFOFtoCNF_U,skolemFOFtoCNF_X5),
inference(resolve,[$cnf( object(skolemFOFtoCNF_U,skolemFOFtoCNF_X5) )],[refute_0_16,refute_0_3]) ).
cnf(refute_0_18,plain,
~ animate(skolemFOFtoCNF_U,skolemFOFtoCNF_X5),
inference(resolve,[$cnf( nonliving(skolemFOFtoCNF_U,skolemFOFtoCNF_X5) )],[refute_0_17,refute_0_1]) ).
cnf(refute_0_19,plain,
be(skolemFOFtoCNF_U,skolemFOFtoCNF_X4,skolemFOFtoCNF_V,skolemFOFtoCNF_X5),
inference(canonicalize,[],[normalize_0_17]) ).
cnf(refute_0_20,plain,
( ~ be(U,V,W,X)
| W = X ),
inference(canonicalize,[],[normalize_0_19]) ).
cnf(refute_0_21,plain,
( ~ be(skolemFOFtoCNF_U,skolemFOFtoCNF_X4,skolemFOFtoCNF_V,skolemFOFtoCNF_X5)
| skolemFOFtoCNF_V = skolemFOFtoCNF_X5 ),
inference(subst,[],[refute_0_20:[bind(U,$fot(skolemFOFtoCNF_U)),bind(V,$fot(skolemFOFtoCNF_X4)),bind(W,$fot(skolemFOFtoCNF_V)),bind(X,$fot(skolemFOFtoCNF_X5))]]) ).
cnf(refute_0_22,plain,
skolemFOFtoCNF_V = skolemFOFtoCNF_X5,
inference(resolve,[$cnf( be(skolemFOFtoCNF_U,skolemFOFtoCNF_X4,skolemFOFtoCNF_V,skolemFOFtoCNF_X5) )],[refute_0_19,refute_0_21]) ).
cnf(refute_0_23,plain,
X0 = X0,
introduced(tautology,[refl,[$fot(X0)]]) ).
cnf(refute_0_24,plain,
( X0 != X0
| X0 != Y
| Y = X0 ),
introduced(tautology,[equality,[$cnf( $equal(X0,X0) ),[0],$fot(Y)]]) ).
cnf(refute_0_25,plain,
( X0 != Y
| Y = X0 ),
inference(resolve,[$cnf( $equal(X0,X0) )],[refute_0_23,refute_0_24]) ).
cnf(refute_0_26,plain,
( skolemFOFtoCNF_V != skolemFOFtoCNF_X5
| skolemFOFtoCNF_X5 = skolemFOFtoCNF_V ),
inference(subst,[],[refute_0_25:[bind(X0,$fot(skolemFOFtoCNF_V)),bind(Y,$fot(skolemFOFtoCNF_X5))]]) ).
cnf(refute_0_27,plain,
skolemFOFtoCNF_X5 = skolemFOFtoCNF_V,
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_V,skolemFOFtoCNF_X5) )],[refute_0_22,refute_0_26]) ).
cnf(refute_0_28,plain,
( skolemFOFtoCNF_X5 != skolemFOFtoCNF_V
| ~ animate(skolemFOFtoCNF_U,skolemFOFtoCNF_V)
| animate(skolemFOFtoCNF_U,skolemFOFtoCNF_X5) ),
introduced(tautology,[equality,[$cnf( ~ animate(skolemFOFtoCNF_U,skolemFOFtoCNF_X5) ),[1],$fot(skolemFOFtoCNF_V)]]) ).
cnf(refute_0_29,plain,
( ~ animate(skolemFOFtoCNF_U,skolemFOFtoCNF_V)
| animate(skolemFOFtoCNF_U,skolemFOFtoCNF_X5) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_X5,skolemFOFtoCNF_V) )],[refute_0_27,refute_0_28]) ).
cnf(refute_0_30,plain,
~ animate(skolemFOFtoCNF_U,skolemFOFtoCNF_V),
inference(resolve,[$cnf( animate(skolemFOFtoCNF_U,skolemFOFtoCNF_X5) )],[refute_0_29,refute_0_18]) ).
cnf(refute_0_31,plain,
man(skolemFOFtoCNF_U,skolemFOFtoCNF_V),
inference(canonicalize,[],[normalize_0_20]) ).
cnf(refute_0_32,plain,
( ~ man(U,V)
| human_person(U,V) ),
inference(canonicalize,[],[normalize_0_22]) ).
cnf(refute_0_33,plain,
( ~ man(skolemFOFtoCNF_U,skolemFOFtoCNF_V)
| human_person(skolemFOFtoCNF_U,skolemFOFtoCNF_V) ),
inference(subst,[],[refute_0_32:[bind(U,$fot(skolemFOFtoCNF_U)),bind(V,$fot(skolemFOFtoCNF_V))]]) ).
cnf(refute_0_34,plain,
human_person(skolemFOFtoCNF_U,skolemFOFtoCNF_V),
inference(resolve,[$cnf( man(skolemFOFtoCNF_U,skolemFOFtoCNF_V) )],[refute_0_31,refute_0_33]) ).
cnf(refute_0_35,plain,
( ~ human_person(U,V)
| animate(U,V) ),
inference(canonicalize,[],[normalize_0_24]) ).
cnf(refute_0_36,plain,
( ~ human_person(skolemFOFtoCNF_U,skolemFOFtoCNF_V)
| animate(skolemFOFtoCNF_U,skolemFOFtoCNF_V) ),
inference(subst,[],[refute_0_35:[bind(U,$fot(skolemFOFtoCNF_U)),bind(V,$fot(skolemFOFtoCNF_V))]]) ).
cnf(refute_0_37,plain,
animate(skolemFOFtoCNF_U,skolemFOFtoCNF_V),
inference(resolve,[$cnf( human_person(skolemFOFtoCNF_U,skolemFOFtoCNF_V) )],[refute_0_34,refute_0_36]) ).
cnf(refute_0_38,plain,
$false,
inference(resolve,[$cnf( animate(skolemFOFtoCNF_U,skolemFOFtoCNF_V) )],[refute_0_37,refute_0_30]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.11 % Problem : NLP208+1 : TPTP v8.1.0. Released v2.4.0.
% 0.02/0.12 % Command : metis --show proof --show saturation %s
% 0.12/0.33 % Computer : n007.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 06:17:09 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.12/0.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.18/0.41 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.41
% 0.18/0.41 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 0.18/0.43
%------------------------------------------------------------------------------