%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : NLP204+1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n006.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:02 EDT 2022
% Result : Theorem 0.10s 0.40s
% Output : CNFRefutation 0.17s
% 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 : 54 ( 8 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 46 ( 43 usr; 1 prp; 0-4 aty)
% Number of functors : 12 ( 12 usr; 12 con; 0-0 aty)
% Number of variables : 211 ( 2 sgn 119 !; 67 ?)
% 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,X6] :
( of(U,W,V)
& man(U,V)
& jules_forename(U,W)
& forename(U,W)
& frontseat(U,X)
& chevy(U,Y0)
& white(U,Y0)
& dirty(U,Y0)
& old(U,Y0)
& of(U,Z,X1)
& city(U,X1)
& hollywood_placename(U,Z)
& placename(U,Z)
& street(U,X1)
& lonely(U,X1)
& event(U,X2)
& agent(U,X2,Y0)
& present(U,X2)
& barrel(U,X2)
& down(U,X2,X1)
& in(U,X2,X1)
& ! [X7] :
( member(U,X7,X3)
=> ? [X8,X9] :
( state(U,X8)
& be(U,X8,X7,X9)
& in(U,X9,X) ) )
& two(U,X3)
& group(U,X3)
& ! [X10] :
( member(U,X10,X3)
=> ( fellow(U,X10)
& young(U,X10) ) )
& ! [X11] :
( member(U,X11,X4)
=> ! [X12] :
( member(U,X12,X3)
=> ? [X13] :
( event(U,X13)
& agent(U,X13,X12)
& patient(U,X13,X11)
& present(U,X13)
& nonreflexive(U,X13)
& wear(U,X13) ) ) )
& group(U,X4)
& ! [X14] :
( member(U,X14,X4)
=> ( coat(U,X14)
& black(U,X14)
& cheap(U,X14) ) )
& wheel(U,X6)
& state(U,X5)
& be(U,X5,V,X6)
& behind(U,X6,X6) ) ) ).
fof(subgoal_0,plain,
! [U] :
( actual_world(U)
=> ! [V,W,X,Y0,Z,X1,X2,X3,X4,X5,X6] :
( ( of(U,W,V)
& man(U,V)
& jules_forename(U,W)
& forename(U,W)
& frontseat(U,X)
& chevy(U,Y0)
& white(U,Y0)
& dirty(U,Y0)
& old(U,Y0)
& of(U,Z,X1)
& city(U,X1)
& hollywood_placename(U,Z)
& placename(U,Z)
& street(U,X1)
& lonely(U,X1)
& event(U,X2)
& agent(U,X2,Y0)
& present(U,X2)
& barrel(U,X2)
& down(U,X2,X1)
& in(U,X2,X1)
& ! [X7] :
( member(U,X7,X3)
=> ? [X8,X9] :
( state(U,X8)
& be(U,X8,X7,X9)
& in(U,X9,X) ) )
& two(U,X3)
& group(U,X3)
& ! [X10] :
( member(U,X10,X3)
=> ( fellow(U,X10)
& young(U,X10) ) )
& ! [X11] :
( member(U,X11,X4)
=> ! [X12] :
( member(U,X12,X3)
=> ? [X13] :
( event(U,X13)
& agent(U,X13,X12)
& patient(U,X13,X11)
& present(U,X13)
& nonreflexive(U,X13)
& wear(U,X13) ) ) )
& group(U,X4)
& ! [X14] :
( member(U,X14,X4)
=> ( coat(U,X14)
& black(U,X14)
& cheap(U,X14) ) )
& wheel(U,X6)
& state(U,X5)
& be(U,X5,V,X6) )
=> ~ behind(U,X6,X6) ) ),
inference(strip,[],[co1]) ).
fof(negate_0_0,plain,
~ ! [U] :
( actual_world(U)
=> ! [V,W,X,Y0,Z,X1,X2,X3,X4,X5,X6] :
( ( of(U,W,V)
& man(U,V)
& jules_forename(U,W)
& forename(U,W)
& frontseat(U,X)
& chevy(U,Y0)
& white(U,Y0)
& dirty(U,Y0)
& old(U,Y0)
& of(U,Z,X1)
& city(U,X1)
& hollywood_placename(U,Z)
& placename(U,Z)
& street(U,X1)
& lonely(U,X1)
& event(U,X2)
& agent(U,X2,Y0)
& present(U,X2)
& barrel(U,X2)
& down(U,X2,X1)
& in(U,X2,X1)
& ! [X7] :
( member(U,X7,X3)
=> ? [X8,X9] :
( state(U,X8)
& be(U,X8,X7,X9)
& in(U,X9,X) ) )
& two(U,X3)
& group(U,X3)
& ! [X10] :
( member(U,X10,X3)
=> ( fellow(U,X10)
& young(U,X10) ) )
& ! [X11] :
( member(U,X11,X4)
=> ! [X12] :
( member(U,X12,X3)
=> ? [X13] :
( event(U,X13)
& agent(U,X13,X12)
& patient(U,X13,X11)
& present(U,X13)
& nonreflexive(U,X13)
& wear(U,X13) ) ) )
& group(U,X4)
& ! [X14] :
( member(U,X14,X4)
=> ( coat(U,X14)
& black(U,X14)
& cheap(U,X14) ) )
& wheel(U,X6)
& state(U,X5)
& be(U,X5,V,X6) )
=> ~ behind(U,X6,X6) ) ),
inference(negate,[],[subgoal_0]) ).
fof(normalize_0_0,plain,
! [U,V] :
( ~ object(U,V)
| nonliving(U,V) ),
inference(canonicalize,[],[ax40]) ).
fof(normalize_0_1,plain,
! [U,V] :
( ~ object(U,V)
| nonliving(U,V) ),
inference(specialize,[],[normalize_0_0]) ).
fof(normalize_0_2,plain,
! [U,V] :
( ~ artifact(U,V)
| object(U,V) ),
inference(canonicalize,[],[ax45]) ).
fof(normalize_0_3,plain,
! [U,V] :
( ~ artifact(U,V)
| object(U,V) ),
inference(specialize,[],[normalize_0_2]) ).
fof(normalize_0_4,plain,
! [U,V] :
( ~ instrumentality(U,V)
| artifact(U,V) ),
inference(canonicalize,[],[ax46]) ).
fof(normalize_0_5,plain,
! [U,V] :
( ~ instrumentality(U,V)
| artifact(U,V) ),
inference(specialize,[],[normalize_0_4]) ).
fof(normalize_0_6,plain,
! [U,V] :
( ~ device(U,V)
| instrumentality(U,V) ),
inference(canonicalize,[],[ax47]) ).
fof(normalize_0_7,plain,
! [U,V] :
( ~ device(U,V)
| instrumentality(U,V) ),
inference(specialize,[],[normalize_0_6]) ).
fof(normalize_0_8,plain,
? [U] :
( actual_world(U)
& ? [V,W,X,X1,X2,X3,X4,X5,X6,Y0,Z] :
( agent(U,X2,Y0)
& barrel(U,X2)
& be(U,X5,V,X6)
& behind(U,X6,X6)
& chevy(U,Y0)
& city(U,X1)
& dirty(U,Y0)
& down(U,X2,X1)
& event(U,X2)
& forename(U,W)
& frontseat(U,X)
& group(U,X3)
& group(U,X4)
& hollywood_placename(U,Z)
& in(U,X2,X1)
& jules_forename(U,W)
& lonely(U,X1)
& man(U,V)
& of(U,W,V)
& of(U,Z,X1)
& old(U,Y0)
& placename(U,Z)
& present(U,X2)
& state(U,X5)
& street(U,X1)
& two(U,X3)
& wheel(U,X6)
& white(U,Y0)
& ! [X10] :
( ~ member(U,X10,X3)
| ( fellow(U,X10)
& young(U,X10) ) )
& ! [X11] :
( ~ member(U,X11,X4)
| ! [X12] :
( ~ member(U,X12,X3)
| ? [X13] :
( agent(U,X13,X12)
& event(U,X13)
& nonreflexive(U,X13)
& patient(U,X13,X11)
& present(U,X13)
& wear(U,X13) ) ) )
& ! [X14] :
( ~ member(U,X14,X4)
| ( black(U,X14)
& cheap(U,X14)
& coat(U,X14) ) )
& ! [X7] :
( ~ member(U,X7,X3)
| ? [X8,X9] :
( be(U,X8,X7,X9)
& in(U,X9,X)
& state(U,X8) ) ) ) ),
inference(canonicalize,[],[negate_0_0]) ).
fof(normalize_0_9,plain,
( actual_world(skolemFOFtoCNF_U)
& ? [V,W,X,X1,X2,X3,X4,X5,X6,Y0,Z] :
( agent(skolemFOFtoCNF_U,X2,Y0)
& barrel(skolemFOFtoCNF_U,X2)
& be(skolemFOFtoCNF_U,X5,V,X6)
& behind(skolemFOFtoCNF_U,X6,X6)
& chevy(skolemFOFtoCNF_U,Y0)
& city(skolemFOFtoCNF_U,X1)
& dirty(skolemFOFtoCNF_U,Y0)
& down(skolemFOFtoCNF_U,X2,X1)
& event(skolemFOFtoCNF_U,X2)
& forename(skolemFOFtoCNF_U,W)
& frontseat(skolemFOFtoCNF_U,X)
& group(skolemFOFtoCNF_U,X3)
& group(skolemFOFtoCNF_U,X4)
& hollywood_placename(skolemFOFtoCNF_U,Z)
& in(skolemFOFtoCNF_U,X2,X1)
& jules_forename(skolemFOFtoCNF_U,W)
& lonely(skolemFOFtoCNF_U,X1)
& man(skolemFOFtoCNF_U,V)
& of(skolemFOFtoCNF_U,W,V)
& of(skolemFOFtoCNF_U,Z,X1)
& old(skolemFOFtoCNF_U,Y0)
& placename(skolemFOFtoCNF_U,Z)
& present(skolemFOFtoCNF_U,X2)
& state(skolemFOFtoCNF_U,X5)
& street(skolemFOFtoCNF_U,X1)
& two(skolemFOFtoCNF_U,X3)
& wheel(skolemFOFtoCNF_U,X6)
& white(skolemFOFtoCNF_U,Y0)
& ! [X10] :
( ~ member(skolemFOFtoCNF_U,X10,X3)
| ( fellow(skolemFOFtoCNF_U,X10)
& young(skolemFOFtoCNF_U,X10) ) )
& ! [X11] :
( ~ member(skolemFOFtoCNF_U,X11,X4)
| ! [X12] :
( ~ member(skolemFOFtoCNF_U,X12,X3)
| ? [X13] :
( agent(skolemFOFtoCNF_U,X13,X12)
& event(skolemFOFtoCNF_U,X13)
& nonreflexive(skolemFOFtoCNF_U,X13)
& patient(skolemFOFtoCNF_U,X13,X11)
& present(skolemFOFtoCNF_U,X13)
& wear(skolemFOFtoCNF_U,X13) ) ) )
& ! [X14] :
( ~ member(skolemFOFtoCNF_U,X14,X4)
| ( black(skolemFOFtoCNF_U,X14)
& cheap(skolemFOFtoCNF_U,X14)
& coat(skolemFOFtoCNF_U,X14) ) )
& ! [X7] :
( ~ member(skolemFOFtoCNF_U,X7,X3)
| ? [X8,X9] :
( be(skolemFOFtoCNF_U,X8,X7,X9)
& in(skolemFOFtoCNF_U,X9,X)
& state(skolemFOFtoCNF_U,X8) ) ) ) ),
inference(skolemize,[],[normalize_0_8]) ).
fof(normalize_0_10,plain,
? [V,W,X,X1,X2,X3,X4,X5,X6,Y0,Z] :
( agent(skolemFOFtoCNF_U,X2,Y0)
& barrel(skolemFOFtoCNF_U,X2)
& be(skolemFOFtoCNF_U,X5,V,X6)
& behind(skolemFOFtoCNF_U,X6,X6)
& chevy(skolemFOFtoCNF_U,Y0)
& city(skolemFOFtoCNF_U,X1)
& dirty(skolemFOFtoCNF_U,Y0)
& down(skolemFOFtoCNF_U,X2,X1)
& event(skolemFOFtoCNF_U,X2)
& forename(skolemFOFtoCNF_U,W)
& frontseat(skolemFOFtoCNF_U,X)
& group(skolemFOFtoCNF_U,X3)
& group(skolemFOFtoCNF_U,X4)
& hollywood_placename(skolemFOFtoCNF_U,Z)
& in(skolemFOFtoCNF_U,X2,X1)
& jules_forename(skolemFOFtoCNF_U,W)
& lonely(skolemFOFtoCNF_U,X1)
& man(skolemFOFtoCNF_U,V)
& of(skolemFOFtoCNF_U,W,V)
& of(skolemFOFtoCNF_U,Z,X1)
& old(skolemFOFtoCNF_U,Y0)
& placename(skolemFOFtoCNF_U,Z)
& present(skolemFOFtoCNF_U,X2)
& state(skolemFOFtoCNF_U,X5)
& street(skolemFOFtoCNF_U,X1)
& two(skolemFOFtoCNF_U,X3)
& wheel(skolemFOFtoCNF_U,X6)
& white(skolemFOFtoCNF_U,Y0)
& ! [X10] :
( ~ member(skolemFOFtoCNF_U,X10,X3)
| ( fellow(skolemFOFtoCNF_U,X10)
& young(skolemFOFtoCNF_U,X10) ) )
& ! [X11] :
( ~ member(skolemFOFtoCNF_U,X11,X4)
| ! [X12] :
( ~ member(skolemFOFtoCNF_U,X12,X3)
| ? [X13] :
( agent(skolemFOFtoCNF_U,X13,X12)
& event(skolemFOFtoCNF_U,X13)
& nonreflexive(skolemFOFtoCNF_U,X13)
& patient(skolemFOFtoCNF_U,X13,X11)
& present(skolemFOFtoCNF_U,X13)
& wear(skolemFOFtoCNF_U,X13) ) ) )
& ! [X14] :
( ~ member(skolemFOFtoCNF_U,X14,X4)
| ( black(skolemFOFtoCNF_U,X14)
& cheap(skolemFOFtoCNF_U,X14)
& coat(skolemFOFtoCNF_U,X14) ) )
& ! [X7] :
( ~ member(skolemFOFtoCNF_U,X7,X3)
| ? [X8,X9] :
( be(skolemFOFtoCNF_U,X8,X7,X9)
& in(skolemFOFtoCNF_U,X9,X)
& state(skolemFOFtoCNF_U,X8) ) ) ),
inference(conjunct,[],[normalize_0_9]) ).
fof(normalize_0_11,plain,
( agent(skolemFOFtoCNF_U,skolemFOFtoCNF_X2,skolemFOFtoCNF_Y_1)
& barrel(skolemFOFtoCNF_U,skolemFOFtoCNF_X2)
& be(skolemFOFtoCNF_U,skolemFOFtoCNF_X5,skolemFOFtoCNF_V,skolemFOFtoCNF_X6)
& behind(skolemFOFtoCNF_U,skolemFOFtoCNF_X6,skolemFOFtoCNF_X6)
& chevy(skolemFOFtoCNF_U,skolemFOFtoCNF_Y_1)
& city(skolemFOFtoCNF_U,skolemFOFtoCNF_X1)
& dirty(skolemFOFtoCNF_U,skolemFOFtoCNF_Y_1)
& down(skolemFOFtoCNF_U,skolemFOFtoCNF_X2,skolemFOFtoCNF_X1)
& event(skolemFOFtoCNF_U,skolemFOFtoCNF_X2)
& forename(skolemFOFtoCNF_U,skolemFOFtoCNF_W_1)
& frontseat(skolemFOFtoCNF_U,skolemFOFtoCNF_X_1)
& group(skolemFOFtoCNF_U,skolemFOFtoCNF_X3)
& group(skolemFOFtoCNF_U,skolemFOFtoCNF_X4)
& hollywood_placename(skolemFOFtoCNF_U,skolemFOFtoCNF_Z)
& in(skolemFOFtoCNF_U,skolemFOFtoCNF_X2,skolemFOFtoCNF_X1)
& jules_forename(skolemFOFtoCNF_U,skolemFOFtoCNF_W_1)
& lonely(skolemFOFtoCNF_U,skolemFOFtoCNF_X1)
& man(skolemFOFtoCNF_U,skolemFOFtoCNF_V)
& of(skolemFOFtoCNF_U,skolemFOFtoCNF_W_1,skolemFOFtoCNF_V)
& of(skolemFOFtoCNF_U,skolemFOFtoCNF_Z,skolemFOFtoCNF_X1)
& old(skolemFOFtoCNF_U,skolemFOFtoCNF_Y_1)
& placename(skolemFOFtoCNF_U,skolemFOFtoCNF_Z)
& present(skolemFOFtoCNF_U,skolemFOFtoCNF_X2)
& state(skolemFOFtoCNF_U,skolemFOFtoCNF_X5)
& street(skolemFOFtoCNF_U,skolemFOFtoCNF_X1)
& two(skolemFOFtoCNF_U,skolemFOFtoCNF_X3)
& wheel(skolemFOFtoCNF_U,skolemFOFtoCNF_X6)
& white(skolemFOFtoCNF_U,skolemFOFtoCNF_Y_1)
& ! [X10] :
( ~ member(skolemFOFtoCNF_U,X10,skolemFOFtoCNF_X3)
| ( fellow(skolemFOFtoCNF_U,X10)
& young(skolemFOFtoCNF_U,X10) ) )
& ! [X11] :
( ~ member(skolemFOFtoCNF_U,X11,skolemFOFtoCNF_X4)
| ! [X12] :
( ~ member(skolemFOFtoCNF_U,X12,skolemFOFtoCNF_X3)
| ? [X13] :
( agent(skolemFOFtoCNF_U,X13,X12)
& event(skolemFOFtoCNF_U,X13)
& nonreflexive(skolemFOFtoCNF_U,X13)
& patient(skolemFOFtoCNF_U,X13,X11)
& present(skolemFOFtoCNF_U,X13)
& wear(skolemFOFtoCNF_U,X13) ) ) )
& ! [X14] :
( ~ member(skolemFOFtoCNF_U,X14,skolemFOFtoCNF_X4)
| ( black(skolemFOFtoCNF_U,X14)
& cheap(skolemFOFtoCNF_U,X14)
& coat(skolemFOFtoCNF_U,X14) ) )
& ! [X7] :
( ~ member(skolemFOFtoCNF_U,X7,skolemFOFtoCNF_X3)
| ? [X8,X9] :
( be(skolemFOFtoCNF_U,X8,X7,X9)
& in(skolemFOFtoCNF_U,X9,skolemFOFtoCNF_X_1)
& state(skolemFOFtoCNF_U,X8) ) ) ),
inference(skolemize,[],[normalize_0_10]) ).
fof(normalize_0_12,plain,
wheel(skolemFOFtoCNF_U,skolemFOFtoCNF_X6),
inference(conjunct,[],[normalize_0_11]) ).
fof(normalize_0_13,plain,
! [U,V] :
( ~ wheel(U,V)
| device(U,V) ),
inference(canonicalize,[],[ax48]) ).
fof(normalize_0_14,plain,
! [U,V] :
( ~ wheel(U,V)
| device(U,V) ),
inference(specialize,[],[normalize_0_13]) ).
fof(normalize_0_15,plain,
! [U,V] :
( ~ animate(U,V)
| ~ nonliving(U,V) ),
inference(canonicalize,[],[ax57]) ).
fof(normalize_0_16,plain,
! [U,V] :
( ~ animate(U,V)
| ~ nonliving(U,V) ),
inference(specialize,[],[normalize_0_15]) ).
fof(normalize_0_17,plain,
be(skolemFOFtoCNF_U,skolemFOFtoCNF_X5,skolemFOFtoCNF_V,skolemFOFtoCNF_X6),
inference(conjunct,[],[normalize_0_11]) ).
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,
! [U,V] :
( ~ human_person(U,V)
| animate(U,V) ),
inference(canonicalize,[],[ax25]) ).
fof(normalize_0_21,plain,
! [U,V] :
( ~ human_person(U,V)
| animate(U,V) ),
inference(specialize,[],[normalize_0_20]) ).
fof(normalize_0_22,plain,
man(skolemFOFtoCNF_U,skolemFOFtoCNF_V),
inference(conjunct,[],[normalize_0_11]) ).
fof(normalize_0_23,plain,
! [U,V] :
( ~ man(U,V)
| human_person(U,V) ),
inference(canonicalize,[],[ax31]) ).
fof(normalize_0_24,plain,
! [U,V] :
( ~ man(U,V)
| human_person(U,V) ),
inference(specialize,[],[normalize_0_23]) ).
cnf(refute_0_0,plain,
( ~ object(U,V)
| nonliving(U,V) ),
inference(canonicalize,[],[normalize_0_1]) ).
cnf(refute_0_1,plain,
( ~ object(skolemFOFtoCNF_U,skolemFOFtoCNF_X6)
| nonliving(skolemFOFtoCNF_U,skolemFOFtoCNF_X6) ),
inference(subst,[],[refute_0_0:[bind(U,$fot(skolemFOFtoCNF_U)),bind(V,$fot(skolemFOFtoCNF_X6))]]) ).
cnf(refute_0_2,plain,
( ~ artifact(U,V)
| object(U,V) ),
inference(canonicalize,[],[normalize_0_3]) ).
cnf(refute_0_3,plain,
( ~ artifact(skolemFOFtoCNF_U,skolemFOFtoCNF_X6)
| object(skolemFOFtoCNF_U,skolemFOFtoCNF_X6) ),
inference(subst,[],[refute_0_2:[bind(U,$fot(skolemFOFtoCNF_U)),bind(V,$fot(skolemFOFtoCNF_X6))]]) ).
cnf(refute_0_4,plain,
( ~ instrumentality(U,V)
| artifact(U,V) ),
inference(canonicalize,[],[normalize_0_5]) ).
cnf(refute_0_5,plain,
( ~ instrumentality(skolemFOFtoCNF_U,skolemFOFtoCNF_X6)
| artifact(skolemFOFtoCNF_U,skolemFOFtoCNF_X6) ),
inference(subst,[],[refute_0_4:[bind(U,$fot(skolemFOFtoCNF_U)),bind(V,$fot(skolemFOFtoCNF_X6))]]) ).
cnf(refute_0_6,plain,
( ~ device(U,V)
| instrumentality(U,V) ),
inference(canonicalize,[],[normalize_0_7]) ).
cnf(refute_0_7,plain,
( ~ device(skolemFOFtoCNF_U,skolemFOFtoCNF_X6)
| instrumentality(skolemFOFtoCNF_U,skolemFOFtoCNF_X6) ),
inference(subst,[],[refute_0_6:[bind(U,$fot(skolemFOFtoCNF_U)),bind(V,$fot(skolemFOFtoCNF_X6))]]) ).
cnf(refute_0_8,plain,
wheel(skolemFOFtoCNF_U,skolemFOFtoCNF_X6),
inference(canonicalize,[],[normalize_0_12]) ).
cnf(refute_0_9,plain,
( ~ wheel(U,V)
| device(U,V) ),
inference(canonicalize,[],[normalize_0_14]) ).
cnf(refute_0_10,plain,
( ~ wheel(skolemFOFtoCNF_U,skolemFOFtoCNF_X6)
| device(skolemFOFtoCNF_U,skolemFOFtoCNF_X6) ),
inference(subst,[],[refute_0_9:[bind(U,$fot(skolemFOFtoCNF_U)),bind(V,$fot(skolemFOFtoCNF_X6))]]) ).
cnf(refute_0_11,plain,
device(skolemFOFtoCNF_U,skolemFOFtoCNF_X6),
inference(resolve,[$cnf( wheel(skolemFOFtoCNF_U,skolemFOFtoCNF_X6) )],[refute_0_8,refute_0_10]) ).
cnf(refute_0_12,plain,
instrumentality(skolemFOFtoCNF_U,skolemFOFtoCNF_X6),
inference(resolve,[$cnf( device(skolemFOFtoCNF_U,skolemFOFtoCNF_X6) )],[refute_0_11,refute_0_7]) ).
cnf(refute_0_13,plain,
artifact(skolemFOFtoCNF_U,skolemFOFtoCNF_X6),
inference(resolve,[$cnf( instrumentality(skolemFOFtoCNF_U,skolemFOFtoCNF_X6) )],[refute_0_12,refute_0_5]) ).
cnf(refute_0_14,plain,
object(skolemFOFtoCNF_U,skolemFOFtoCNF_X6),
inference(resolve,[$cnf( artifact(skolemFOFtoCNF_U,skolemFOFtoCNF_X6) )],[refute_0_13,refute_0_3]) ).
cnf(refute_0_15,plain,
nonliving(skolemFOFtoCNF_U,skolemFOFtoCNF_X6),
inference(resolve,[$cnf( object(skolemFOFtoCNF_U,skolemFOFtoCNF_X6) )],[refute_0_14,refute_0_1]) ).
cnf(refute_0_16,plain,
( ~ animate(U,V)
| ~ nonliving(U,V) ),
inference(canonicalize,[],[normalize_0_16]) ).
cnf(refute_0_17,plain,
( ~ animate(skolemFOFtoCNF_U,skolemFOFtoCNF_X6)
| ~ nonliving(skolemFOFtoCNF_U,skolemFOFtoCNF_X6) ),
inference(subst,[],[refute_0_16:[bind(U,$fot(skolemFOFtoCNF_U)),bind(V,$fot(skolemFOFtoCNF_X6))]]) ).
cnf(refute_0_18,plain,
~ animate(skolemFOFtoCNF_U,skolemFOFtoCNF_X6),
inference(resolve,[$cnf( nonliving(skolemFOFtoCNF_U,skolemFOFtoCNF_X6) )],[refute_0_15,refute_0_17]) ).
cnf(refute_0_19,plain,
be(skolemFOFtoCNF_U,skolemFOFtoCNF_X5,skolemFOFtoCNF_V,skolemFOFtoCNF_X6),
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_X5,skolemFOFtoCNF_V,skolemFOFtoCNF_X6)
| skolemFOFtoCNF_V = skolemFOFtoCNF_X6 ),
inference(subst,[],[refute_0_20:[bind(U,$fot(skolemFOFtoCNF_U)),bind(V,$fot(skolemFOFtoCNF_X5)),bind(W,$fot(skolemFOFtoCNF_V)),bind(X,$fot(skolemFOFtoCNF_X6))]]) ).
cnf(refute_0_22,plain,
skolemFOFtoCNF_V = skolemFOFtoCNF_X6,
inference(resolve,[$cnf( be(skolemFOFtoCNF_U,skolemFOFtoCNF_X5,skolemFOFtoCNF_V,skolemFOFtoCNF_X6) )],[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_X6
| skolemFOFtoCNF_X6 = skolemFOFtoCNF_V ),
inference(subst,[],[refute_0_25:[bind(X0,$fot(skolemFOFtoCNF_V)),bind(Y,$fot(skolemFOFtoCNF_X6))]]) ).
cnf(refute_0_27,plain,
skolemFOFtoCNF_X6 = skolemFOFtoCNF_V,
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_V,skolemFOFtoCNF_X6) )],[refute_0_22,refute_0_26]) ).
cnf(refute_0_28,plain,
( skolemFOFtoCNF_X6 != skolemFOFtoCNF_V
| ~ animate(skolemFOFtoCNF_U,skolemFOFtoCNF_V)
| animate(skolemFOFtoCNF_U,skolemFOFtoCNF_X6) ),
introduced(tautology,[equality,[$cnf( ~ animate(skolemFOFtoCNF_U,skolemFOFtoCNF_X6) ),[1],$fot(skolemFOFtoCNF_V)]]) ).
cnf(refute_0_29,plain,
( ~ animate(skolemFOFtoCNF_U,skolemFOFtoCNF_V)
| animate(skolemFOFtoCNF_U,skolemFOFtoCNF_X6) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_X6,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_X6) )],[refute_0_29,refute_0_18]) ).
cnf(refute_0_31,plain,
( ~ human_person(U,V)
| animate(U,V) ),
inference(canonicalize,[],[normalize_0_21]) ).
cnf(refute_0_32,plain,
( ~ human_person(skolemFOFtoCNF_U,skolemFOFtoCNF_V)
| animate(skolemFOFtoCNF_U,skolemFOFtoCNF_V) ),
inference(subst,[],[refute_0_31:[bind(U,$fot(skolemFOFtoCNF_U)),bind(V,$fot(skolemFOFtoCNF_V))]]) ).
cnf(refute_0_33,plain,
man(skolemFOFtoCNF_U,skolemFOFtoCNF_V),
inference(canonicalize,[],[normalize_0_22]) ).
cnf(refute_0_34,plain,
( ~ man(U,V)
| human_person(U,V) ),
inference(canonicalize,[],[normalize_0_24]) ).
cnf(refute_0_35,plain,
( ~ man(skolemFOFtoCNF_U,skolemFOFtoCNF_V)
| human_person(skolemFOFtoCNF_U,skolemFOFtoCNF_V) ),
inference(subst,[],[refute_0_34:[bind(U,$fot(skolemFOFtoCNF_U)),bind(V,$fot(skolemFOFtoCNF_V))]]) ).
cnf(refute_0_36,plain,
human_person(skolemFOFtoCNF_U,skolemFOFtoCNF_V),
inference(resolve,[$cnf( man(skolemFOFtoCNF_U,skolemFOFtoCNF_V) )],[refute_0_33,refute_0_35]) ).
cnf(refute_0_37,plain,
animate(skolemFOFtoCNF_U,skolemFOFtoCNF_V),
inference(resolve,[$cnf( human_person(skolemFOFtoCNF_U,skolemFOFtoCNF_V) )],[refute_0_36,refute_0_32]) ).
cnf(refute_0_38,plain,
$false,
inference(resolve,[$cnf( animate(skolemFOFtoCNF_U,skolemFOFtoCNF_V) )],[refute_0_37,refute_0_30]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.10 % Problem : NLP204+1 : TPTP v8.1.0. Released v2.4.0.
% 0.10/0.11 % Command : metis --show proof --show saturation %s
% 0.10/0.31 % Computer : n006.cluster.edu
% 0.10/0.31 % Model : x86_64 x86_64
% 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.31 % Memory : 8042.1875MB
% 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.31 % CPULimit : 300
% 0.10/0.31 % WCLimit : 600
% 0.10/0.31 % DateTime : Fri Jul 1 08:33:23 EDT 2022
% 0.10/0.32 % CPUTime :
% 0.10/0.32 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.10/0.40 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.40
% 0.10/0.40 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 0.17/0.42
%------------------------------------------------------------------------------