%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : NLP204+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 08:51:27 AM UTC 2026
% Result : Theorem 233.70s 248.82s
% Output : Proof 233.96s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(ax1,axiom,
! [U,V] :
( jules_forename(U,V)
=> forename(U,V) ),
file('theBenchmark.p',ax1) ).
fof(ax2,axiom,
! [U,V] :
( forename(U,V)
=> relname(U,V) ),
file('theBenchmark.p',ax2) ).
fof(ax3,axiom,
! [U,V] :
( furniture(U,V)
=> instrumentality(U,V) ),
file('theBenchmark.p',ax3) ).
fof(ax4,axiom,
! [U,V] :
( seat(U,V)
=> furniture(U,V) ),
file('theBenchmark.p',ax4) ).
fof(ax5,axiom,
! [U,V] :
( frontseat(U,V)
=> seat(U,V) ),
file('theBenchmark.p',ax5) ).
fof(ax6,axiom,
! [U,V] :
( location(U,V)
=> object(U,V) ),
file('theBenchmark.p',ax6) ).
fof(ax7,axiom,
! [U,V] :
( city(U,V)
=> location(U,V) ),
file('theBenchmark.p',ax7) ).
fof(ax8,axiom,
! [U,V] :
( hollywood_placename(U,V)
=> placename(U,V) ),
file('theBenchmark.p',ax8) ).
fof(ax9,axiom,
! [U,V] :
( abstraction(U,V)
=> unisex(U,V) ),
file('theBenchmark.p',ax9) ).
fof(ax10,axiom,
! [U,V] :
( abstraction(U,V)
=> general(U,V) ),
file('theBenchmark.p',ax10) ).
fof(ax11,axiom,
! [U,V] :
( abstraction(U,V)
=> nonhuman(U,V) ),
file('theBenchmark.p',ax11) ).
fof(ax12,axiom,
! [U,V] :
( abstraction(U,V)
=> thing(U,V) ),
file('theBenchmark.p',ax12) ).
fof(ax13,axiom,
! [U,V] :
( relation(U,V)
=> abstraction(U,V) ),
file('theBenchmark.p',ax13) ).
fof(ax14,axiom,
! [U,V] :
( relname(U,V)
=> relation(U,V) ),
file('theBenchmark.p',ax14) ).
fof(ax15,axiom,
! [U,V] :
( placename(U,V)
=> relname(U,V) ),
file('theBenchmark.p',ax15) ).
fof(ax16,axiom,
! [U,V] :
( transport(U,V)
=> instrumentality(U,V) ),
file('theBenchmark.p',ax16) ).
fof(ax17,axiom,
! [U,V] :
( vehicle(U,V)
=> transport(U,V) ),
file('theBenchmark.p',ax17) ).
fof(ax18,axiom,
! [U,V] :
( car(U,V)
=> vehicle(U,V) ),
file('theBenchmark.p',ax18) ).
fof(ax19,axiom,
! [U,V] :
( chevy(U,V)
=> car(U,V) ),
file('theBenchmark.p',ax19) ).
fof(ax20,axiom,
! [U,V] :
( way(U,V)
=> artifact(U,V) ),
file('theBenchmark.p',ax20) ).
fof(ax21,axiom,
! [U,V] :
( street(U,V)
=> way(U,V) ),
file('theBenchmark.p',ax21) ).
fof(ax22,axiom,
! [U,V] :
( barrel(U,V)
=> event(U,V) ),
file('theBenchmark.p',ax22) ).
fof(ax23,axiom,
! [U,V] :
( two(U,V)
=> group(U,V) ),
file('theBenchmark.p',ax23) ).
fof(ax24,axiom,
! [U,V] :
( man(U,V)
=> male(U,V) ),
file('theBenchmark.p',ax24) ).
fof(ax25,axiom,
! [U,V] :
( human_person(U,V)
=> animate(U,V) ),
file('theBenchmark.p',ax25) ).
fof(ax26,axiom,
! [U,V] :
( human_person(U,V)
=> human(U,V) ),
file('theBenchmark.p',ax26) ).
fof(ax27,axiom,
! [U,V] :
( organism(U,V)
=> living(U,V) ),
file('theBenchmark.p',ax27) ).
fof(ax28,axiom,
! [U,V] :
( organism(U,V)
=> impartial(U,V) ),
file('theBenchmark.p',ax28) ).
fof(ax29,axiom,
! [U,V] :
( organism(U,V)
=> entity(U,V) ),
file('theBenchmark.p',ax29) ).
fof(ax30,axiom,
! [U,V] :
( human_person(U,V)
=> organism(U,V) ),
file('theBenchmark.p',ax30) ).
fof(ax31,axiom,
! [U,V] :
( man(U,V)
=> human_person(U,V) ),
file('theBenchmark.p',ax31) ).
fof(ax32,axiom,
! [U,V] :
( fellow(U,V)
=> man(U,V) ),
file('theBenchmark.p',ax32) ).
fof(ax33,axiom,
! [U,V] :
( wear(U,V)
=> event(U,V) ),
file('theBenchmark.p',ax33) ).
fof(ax34,axiom,
! [U,V] :
( set(U,V)
=> multiple(U,V) ),
file('theBenchmark.p',ax34) ).
fof(ax35,axiom,
! [U,V] :
( group(U,V)
=> set(U,V) ),
file('theBenchmark.p',ax35) ).
fof(ax36,axiom,
! [U,V] :
( clothes(U,V)
=> artifact(U,V) ),
file('theBenchmark.p',ax36) ).
fof(ax37,axiom,
! [U,V] :
( coat(U,V)
=> clothes(U,V) ),
file('theBenchmark.p',ax37) ).
fof(ax38,axiom,
! [U,V] :
( object(U,V)
=> unisex(U,V) ),
file('theBenchmark.p',ax38) ).
fof(ax39,axiom,
! [U,V] :
( object(U,V)
=> impartial(U,V) ),
file('theBenchmark.p',ax39) ).
fof(ax40,axiom,
! [U,V] :
( object(U,V)
=> nonliving(U,V) ),
file('theBenchmark.p',ax40) ).
fof(ax41,axiom,
! [U,V] :
( entity(U,V)
=> existent(U,V) ),
file('theBenchmark.p',ax41) ).
fof(ax42,axiom,
! [U,V] :
( entity(U,V)
=> specific(U,V) ),
file('theBenchmark.p',ax42) ).
fof(ax43,axiom,
! [U,V] :
( entity(U,V)
=> thing(U,V) ),
file('theBenchmark.p',ax43) ).
fof(ax44,axiom,
! [U,V] :
( object(U,V)
=> entity(U,V) ),
file('theBenchmark.p',ax44) ).
fof(ax45,axiom,
! [U,V] :
( artifact(U,V)
=> object(U,V) ),
file('theBenchmark.p',ax45) ).
fof(ax46,axiom,
! [U,V] :
( instrumentality(U,V)
=> artifact(U,V) ),
file('theBenchmark.p',ax46) ).
fof(ax47,axiom,
! [U,V] :
( device(U,V)
=> instrumentality(U,V) ),
file('theBenchmark.p',ax47) ).
fof(ax48,axiom,
! [U,V] :
( wheel(U,V)
=> device(U,V) ),
file('theBenchmark.p',ax48) ).
fof(ax49,axiom,
! [U,V] :
( event(U,V)
=> eventuality(U,V) ),
file('theBenchmark.p',ax49) ).
fof(ax50,axiom,
! [U,V] :
( state(U,V)
=> event(U,V) ),
file('theBenchmark.p',ax50) ).
fof(ax51,axiom,
! [U,V] :
( eventuality(U,V)
=> unisex(U,V) ),
file('theBenchmark.p',ax51) ).
fof(ax52,axiom,
! [U,V] :
( eventuality(U,V)
=> nonexistent(U,V) ),
file('theBenchmark.p',ax52) ).
fof(ax53,axiom,
! [U,V] :
( eventuality(U,V)
=> specific(U,V) ),
file('theBenchmark.p',ax53) ).
fof(ax54,axiom,
! [U,V] :
( thing(U,V)
=> singleton(U,V) ),
file('theBenchmark.p',ax54) ).
fof(ax55,axiom,
! [U,V] :
( eventuality(U,V)
=> thing(U,V) ),
file('theBenchmark.p',ax55) ).
fof(ax56,axiom,
! [U,V] :
( state(U,V)
=> eventuality(U,V) ),
file('theBenchmark.p',ax56) ).
fof(ax57,axiom,
! [U,V] :
( animate(U,V)
=> ~ nonliving(U,V) ),
file('theBenchmark.p',ax57) ).
fof(ax58,axiom,
! [U,V] :
( existent(U,V)
=> ~ nonexistent(U,V) ),
file('theBenchmark.p',ax58) ).
fof(ax59,axiom,
! [U,V] :
( nonhuman(U,V)
=> ~ human(U,V) ),
file('theBenchmark.p',ax59) ).
fof(ax60,axiom,
! [U,V] :
( nonliving(U,V)
=> ~ living(U,V) ),
file('theBenchmark.p',ax60) ).
fof(ax61,axiom,
! [U,V] :
( singleton(U,V)
=> ~ multiple(U,V) ),
file('theBenchmark.p',ax61) ).
fof(ax62,axiom,
! [U,V] :
( specific(U,V)
=> ~ general(U,V) ),
file('theBenchmark.p',ax62) ).
fof(ax63,axiom,
! [U,V] :
( unisex(U,V)
=> ~ male(U,V) ),
file('theBenchmark.p',ax63) ).
fof(ax64,axiom,
! [U,V] :
( white(U,V)
=> ~ black(U,V) ),
file('theBenchmark.p',ax64) ).
fof(ax65,axiom,
! [U,V] :
( young(U,V)
=> ~ old(U,V) ),
file('theBenchmark.p',ax65) ).
fof(ax66,axiom,
! [U,V,W] :
( ( of(U,W,V)
& forename(U,W)
& entity(U,V) )
=> ~ ? [X] :
( of(U,X,V)
& X != W
& forename(U,X) ) ),
file('theBenchmark.p',ax66) ).
fof(ax67,axiom,
! [U,V,W] :
( ( of(U,W,V)
& placename(U,W)
& entity(U,V) )
=> ~ ? [X] :
( of(U,X,V)
& X != W
& placename(U,X) ) ),
file('theBenchmark.p',ax67) ).
fof(ax68,axiom,
! [U,V] :
( two(U,V)
<=> ? [W] :
( ? [X] :
( ! [Y] :
( member(U,Y,V)
=> ( Y = W
| Y = X ) )
& X != W
& member(U,X,V) )
& member(U,W,V) ) ),
file('theBenchmark.p',ax68) ).
fof(ax69,axiom,
! [U,V,W,X] :
( ( patient(U,V,X)
& agent(U,V,W)
& nonreflexive(U,V) )
=> W != X ),
file('theBenchmark.p',ax69) ).
fof(ax70,axiom,
! [U] :
~ ? [V] : member(U,V,V),
file('theBenchmark.p',ax70) ).
fof(ax71,axiom,
! [U,V,W,X] :
( be(U,V,W,X)
=> W = X ),
file('theBenchmark.p',ax71) ).
fof(co1,conjecture,
~ ? [U] :
( ? [V,W,X,Y,Z,X1,X2,X3,X4,X5,X6] :
( behind(U,X6,X6)
& be(U,X5,V,X6)
& state(U,X5)
& wheel(U,X6)
& ! [X14] :
( member(U,X14,X4)
=> ( cheap(U,X14)
& black(U,X14)
& coat(U,X14) ) )
& group(U,X4)
& ! [X11] :
( member(U,X11,X4)
=> ! [X12] :
( member(U,X12,X3)
=> ? [X13] :
( wear(U,X13)
& nonreflexive(U,X13)
& present(U,X13)
& patient(U,X13,X11)
& agent(U,X13,X12)
& event(U,X13) ) ) )
& ! [X10] :
( member(U,X10,X3)
=> ( young(U,X10)
& fellow(U,X10) ) )
& group(U,X3)
& two(U,X3)
& ! [X7] :
( member(U,X7,X3)
=> ? [X8,X9] :
( in(U,X9,X)
& be(U,X8,X7,X9)
& state(U,X8) ) )
& in(U,X2,X1)
& down(U,X2,X1)
& barrel(U,X2)
& present(U,X2)
& agent(U,X2,Y)
& event(U,X2)
& lonely(U,X1)
& street(U,X1)
& placename(U,Z)
& hollywood_placename(U,Z)
& city(U,X1)
& of(U,Z,X1)
& old(U,Y)
& dirty(U,Y)
& white(U,Y)
& chevy(U,Y)
& frontseat(U,X)
& forename(U,W)
& jules_forename(U,W)
& man(U,V)
& of(U,W,V) )
& actual_world(U) ),
file('theBenchmark.p',co1) ).
fof(f_1_1,plain,
! [U,V] :
( forename(U,V)
| ~ jules_forename(U,V) ),
inference(fof_nnf,[status(thm)],[ax1]) ).
fof(f_1_2,plain,
! [U_1,U_0] :
( forename(U_1,U_0)
| ~ jules_forename(U_1,U_0) ),
inference(variable_rename,[status(thm)],[f_1_1]) ).
cnf(f_1_3,plain,
( forename(U_1,U_0)
| ~ jules_forename(U_1,U_0) ),
inference(clausify,[status(thm)],[f_1_2]) ).
fof(f_2_1,plain,
! [U,V] :
( relname(U,V)
| ~ forename(U,V) ),
inference(fof_nnf,[status(thm)],[ax2]) ).
fof(f_2_2,plain,
! [U_3,U_2] :
( relname(U_3,U_2)
| ~ forename(U_3,U_2) ),
inference(variable_rename,[status(thm)],[f_2_1]) ).
cnf(f_2_3,plain,
( relname(U_3,U_2)
| ~ forename(U_3,U_2) ),
inference(clausify,[status(thm)],[f_2_2]) ).
fof(f_3_1,plain,
! [U,V] :
( instrumentality(U,V)
| ~ furniture(U,V) ),
inference(fof_nnf,[status(thm)],[ax3]) ).
fof(f_3_2,plain,
! [U_5,U_4] :
( instrumentality(U_5,U_4)
| ~ furniture(U_5,U_4) ),
inference(variable_rename,[status(thm)],[f_3_1]) ).
cnf(f_3_3,plain,
( instrumentality(U_5,U_4)
| ~ furniture(U_5,U_4) ),
inference(clausify,[status(thm)],[f_3_2]) ).
fof(f_4_1,plain,
! [U,V] :
( furniture(U,V)
| ~ seat(U,V) ),
inference(fof_nnf,[status(thm)],[ax4]) ).
fof(f_4_2,plain,
! [U_7,U_6] :
( furniture(U_7,U_6)
| ~ seat(U_7,U_6) ),
inference(variable_rename,[status(thm)],[f_4_1]) ).
cnf(f_4_3,plain,
( furniture(U_7,U_6)
| ~ seat(U_7,U_6) ),
inference(clausify,[status(thm)],[f_4_2]) ).
fof(f_5_1,plain,
! [U,V] :
( seat(U,V)
| ~ frontseat(U,V) ),
inference(fof_nnf,[status(thm)],[ax5]) ).
fof(f_5_2,plain,
! [U_9,U_8] :
( seat(U_9,U_8)
| ~ frontseat(U_9,U_8) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
cnf(f_5_3,plain,
( seat(U_9,U_8)
| ~ frontseat(U_9,U_8) ),
inference(clausify,[status(thm)],[f_5_2]) ).
fof(f_6_1,plain,
! [U,V] :
( object(U,V)
| ~ location(U,V) ),
inference(fof_nnf,[status(thm)],[ax6]) ).
fof(f_6_2,plain,
! [U_11,U_10] :
( object(U_11,U_10)
| ~ location(U_11,U_10) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
cnf(f_6_3,plain,
( object(U_11,U_10)
| ~ location(U_11,U_10) ),
inference(clausify,[status(thm)],[f_6_2]) ).
fof(f_7_1,plain,
! [U,V] :
( location(U,V)
| ~ city(U,V) ),
inference(fof_nnf,[status(thm)],[ax7]) ).
fof(f_7_2,plain,
! [U_13,U_12] :
( location(U_13,U_12)
| ~ city(U_13,U_12) ),
inference(variable_rename,[status(thm)],[f_7_1]) ).
cnf(f_7_3,plain,
( location(U_13,U_12)
| ~ city(U_13,U_12) ),
inference(clausify,[status(thm)],[f_7_2]) ).
fof(f_8_1,plain,
! [U,V] :
( placename(U,V)
| ~ hollywood_placename(U,V) ),
inference(fof_nnf,[status(thm)],[ax8]) ).
fof(f_8_2,plain,
! [U_15,U_14] :
( placename(U_15,U_14)
| ~ hollywood_placename(U_15,U_14) ),
inference(variable_rename,[status(thm)],[f_8_1]) ).
cnf(f_8_3,plain,
( placename(U_15,U_14)
| ~ hollywood_placename(U_15,U_14) ),
inference(clausify,[status(thm)],[f_8_2]) ).
fof(f_9_1,plain,
! [U,V] :
( unisex(U,V)
| ~ abstraction(U,V) ),
inference(fof_nnf,[status(thm)],[ax9]) ).
fof(f_9_2,plain,
! [U_17,U_16] :
( unisex(U_17,U_16)
| ~ abstraction(U_17,U_16) ),
inference(variable_rename,[status(thm)],[f_9_1]) ).
cnf(f_9_3,plain,
( unisex(U_17,U_16)
| ~ abstraction(U_17,U_16) ),
inference(clausify,[status(thm)],[f_9_2]) ).
fof(f_10_1,plain,
! [U,V] :
( general(U,V)
| ~ abstraction(U,V) ),
inference(fof_nnf,[status(thm)],[ax10]) ).
fof(f_10_2,plain,
! [U_19,U_18] :
( general(U_19,U_18)
| ~ abstraction(U_19,U_18) ),
inference(variable_rename,[status(thm)],[f_10_1]) ).
cnf(f_10_3,plain,
( general(U_19,U_18)
| ~ abstraction(U_19,U_18) ),
inference(clausify,[status(thm)],[f_10_2]) ).
fof(f_11_1,plain,
! [U,V] :
( nonhuman(U,V)
| ~ abstraction(U,V) ),
inference(fof_nnf,[status(thm)],[ax11]) ).
fof(f_11_2,plain,
! [U_21,U_20] :
( nonhuman(U_21,U_20)
| ~ abstraction(U_21,U_20) ),
inference(variable_rename,[status(thm)],[f_11_1]) ).
cnf(f_11_3,plain,
( nonhuman(U_21,U_20)
| ~ abstraction(U_21,U_20) ),
inference(clausify,[status(thm)],[f_11_2]) ).
fof(f_12_1,plain,
! [U,V] :
( thing(U,V)
| ~ abstraction(U,V) ),
inference(fof_nnf,[status(thm)],[ax12]) ).
fof(f_12_2,plain,
! [U_23,U_22] :
( thing(U_23,U_22)
| ~ abstraction(U_23,U_22) ),
inference(variable_rename,[status(thm)],[f_12_1]) ).
cnf(f_12_3,plain,
( thing(U_23,U_22)
| ~ abstraction(U_23,U_22) ),
inference(clausify,[status(thm)],[f_12_2]) ).
fof(f_13_1,plain,
! [U,V] :
( abstraction(U,V)
| ~ relation(U,V) ),
inference(fof_nnf,[status(thm)],[ax13]) ).
fof(f_13_2,plain,
! [U_25,U_24] :
( abstraction(U_25,U_24)
| ~ relation(U_25,U_24) ),
inference(variable_rename,[status(thm)],[f_13_1]) ).
cnf(f_13_3,plain,
( abstraction(U_25,U_24)
| ~ relation(U_25,U_24) ),
inference(clausify,[status(thm)],[f_13_2]) ).
fof(f_14_1,plain,
! [U,V] :
( relation(U,V)
| ~ relname(U,V) ),
inference(fof_nnf,[status(thm)],[ax14]) ).
fof(f_14_2,plain,
! [U_27,U_26] :
( relation(U_27,U_26)
| ~ relname(U_27,U_26) ),
inference(variable_rename,[status(thm)],[f_14_1]) ).
cnf(f_14_3,plain,
( relation(U_27,U_26)
| ~ relname(U_27,U_26) ),
inference(clausify,[status(thm)],[f_14_2]) ).
fof(f_15_1,plain,
! [U,V] :
( relname(U,V)
| ~ placename(U,V) ),
inference(fof_nnf,[status(thm)],[ax15]) ).
fof(f_15_2,plain,
! [U_29,U_28] :
( relname(U_29,U_28)
| ~ placename(U_29,U_28) ),
inference(variable_rename,[status(thm)],[f_15_1]) ).
cnf(f_15_3,plain,
( relname(U_29,U_28)
| ~ placename(U_29,U_28) ),
inference(clausify,[status(thm)],[f_15_2]) ).
fof(f_16_1,plain,
! [U,V] :
( instrumentality(U,V)
| ~ transport(U,V) ),
inference(fof_nnf,[status(thm)],[ax16]) ).
fof(f_16_2,plain,
! [U_31,U_30] :
( instrumentality(U_31,U_30)
| ~ transport(U_31,U_30) ),
inference(variable_rename,[status(thm)],[f_16_1]) ).
cnf(f_16_3,plain,
( instrumentality(U_31,U_30)
| ~ transport(U_31,U_30) ),
inference(clausify,[status(thm)],[f_16_2]) ).
fof(f_17_1,plain,
! [U,V] :
( transport(U,V)
| ~ vehicle(U,V) ),
inference(fof_nnf,[status(thm)],[ax17]) ).
fof(f_17_2,plain,
! [U_33,U_32] :
( transport(U_33,U_32)
| ~ vehicle(U_33,U_32) ),
inference(variable_rename,[status(thm)],[f_17_1]) ).
cnf(f_17_3,plain,
( transport(U_33,U_32)
| ~ vehicle(U_33,U_32) ),
inference(clausify,[status(thm)],[f_17_2]) ).
fof(f_18_1,plain,
! [U,V] :
( vehicle(U,V)
| ~ car(U,V) ),
inference(fof_nnf,[status(thm)],[ax18]) ).
fof(f_18_2,plain,
! [U_35,U_34] :
( vehicle(U_35,U_34)
| ~ car(U_35,U_34) ),
inference(variable_rename,[status(thm)],[f_18_1]) ).
cnf(f_18_3,plain,
( vehicle(U_35,U_34)
| ~ car(U_35,U_34) ),
inference(clausify,[status(thm)],[f_18_2]) ).
fof(f_19_1,plain,
! [U,V] :
( car(U,V)
| ~ chevy(U,V) ),
inference(fof_nnf,[status(thm)],[ax19]) ).
fof(f_19_2,plain,
! [U_37,U_36] :
( car(U_37,U_36)
| ~ chevy(U_37,U_36) ),
inference(variable_rename,[status(thm)],[f_19_1]) ).
cnf(f_19_3,plain,
( car(U_37,U_36)
| ~ chevy(U_37,U_36) ),
inference(clausify,[status(thm)],[f_19_2]) ).
fof(f_20_1,plain,
! [U,V] :
( artifact(U,V)
| ~ way(U,V) ),
inference(fof_nnf,[status(thm)],[ax20]) ).
fof(f_20_2,plain,
! [U_39,U_38] :
( artifact(U_39,U_38)
| ~ way(U_39,U_38) ),
inference(variable_rename,[status(thm)],[f_20_1]) ).
cnf(f_20_3,plain,
( artifact(U_39,U_38)
| ~ way(U_39,U_38) ),
inference(clausify,[status(thm)],[f_20_2]) ).
fof(f_21_1,plain,
! [U,V] :
( way(U,V)
| ~ street(U,V) ),
inference(fof_nnf,[status(thm)],[ax21]) ).
fof(f_21_2,plain,
! [U_41,U_40] :
( way(U_41,U_40)
| ~ street(U_41,U_40) ),
inference(variable_rename,[status(thm)],[f_21_1]) ).
cnf(f_21_3,plain,
( way(U_41,U_40)
| ~ street(U_41,U_40) ),
inference(clausify,[status(thm)],[f_21_2]) ).
fof(f_22_1,plain,
! [U,V] :
( event(U,V)
| ~ barrel(U,V) ),
inference(fof_nnf,[status(thm)],[ax22]) ).
fof(f_22_2,plain,
! [U_43,U_42] :
( event(U_43,U_42)
| ~ barrel(U_43,U_42) ),
inference(variable_rename,[status(thm)],[f_22_1]) ).
cnf(f_22_3,plain,
( event(U_43,U_42)
| ~ barrel(U_43,U_42) ),
inference(clausify,[status(thm)],[f_22_2]) ).
fof(f_23_1,plain,
! [U,V] :
( group(U,V)
| ~ two(U,V) ),
inference(fof_nnf,[status(thm)],[ax23]) ).
fof(f_23_2,plain,
! [U_45,U_44] :
( group(U_45,U_44)
| ~ two(U_45,U_44) ),
inference(variable_rename,[status(thm)],[f_23_1]) ).
cnf(f_23_3,plain,
( group(U_45,U_44)
| ~ two(U_45,U_44) ),
inference(clausify,[status(thm)],[f_23_2]) ).
fof(f_24_1,plain,
! [U,V] :
( male(U,V)
| ~ man(U,V) ),
inference(fof_nnf,[status(thm)],[ax24]) ).
fof(f_24_2,plain,
! [U_47,U_46] :
( male(U_47,U_46)
| ~ man(U_47,U_46) ),
inference(variable_rename,[status(thm)],[f_24_1]) ).
cnf(f_24_3,plain,
( male(U_47,U_46)
| ~ man(U_47,U_46) ),
inference(clausify,[status(thm)],[f_24_2]) ).
fof(f_25_1,plain,
! [U,V] :
( animate(U,V)
| ~ human_person(U,V) ),
inference(fof_nnf,[status(thm)],[ax25]) ).
fof(f_25_2,plain,
! [U_49,U_48] :
( animate(U_49,U_48)
| ~ human_person(U_49,U_48) ),
inference(variable_rename,[status(thm)],[f_25_1]) ).
cnf(f_25_3,plain,
( animate(U_49,U_48)
| ~ human_person(U_49,U_48) ),
inference(clausify,[status(thm)],[f_25_2]) ).
fof(f_26_1,plain,
! [U,V] :
( human(U,V)
| ~ human_person(U,V) ),
inference(fof_nnf,[status(thm)],[ax26]) ).
fof(f_26_2,plain,
! [U_51,U_50] :
( human(U_51,U_50)
| ~ human_person(U_51,U_50) ),
inference(variable_rename,[status(thm)],[f_26_1]) ).
cnf(f_26_3,plain,
( human(U_51,U_50)
| ~ human_person(U_51,U_50) ),
inference(clausify,[status(thm)],[f_26_2]) ).
fof(f_27_1,plain,
! [U,V] :
( living(U,V)
| ~ organism(U,V) ),
inference(fof_nnf,[status(thm)],[ax27]) ).
fof(f_27_2,plain,
! [U_53,U_52] :
( living(U_53,U_52)
| ~ organism(U_53,U_52) ),
inference(variable_rename,[status(thm)],[f_27_1]) ).
cnf(f_27_3,plain,
( living(U_53,U_52)
| ~ organism(U_53,U_52) ),
inference(clausify,[status(thm)],[f_27_2]) ).
fof(f_28_1,plain,
! [U,V] :
( impartial(U,V)
| ~ organism(U,V) ),
inference(fof_nnf,[status(thm)],[ax28]) ).
fof(f_28_2,plain,
! [U_55,U_54] :
( impartial(U_55,U_54)
| ~ organism(U_55,U_54) ),
inference(variable_rename,[status(thm)],[f_28_1]) ).
cnf(f_28_3,plain,
( impartial(U_55,U_54)
| ~ organism(U_55,U_54) ),
inference(clausify,[status(thm)],[f_28_2]) ).
fof(f_29_1,plain,
! [U,V] :
( entity(U,V)
| ~ organism(U,V) ),
inference(fof_nnf,[status(thm)],[ax29]) ).
fof(f_29_2,plain,
! [U_57,U_56] :
( entity(U_57,U_56)
| ~ organism(U_57,U_56) ),
inference(variable_rename,[status(thm)],[f_29_1]) ).
cnf(f_29_3,plain,
( entity(U_57,U_56)
| ~ organism(U_57,U_56) ),
inference(clausify,[status(thm)],[f_29_2]) ).
fof(f_30_1,plain,
! [U,V] :
( organism(U,V)
| ~ human_person(U,V) ),
inference(fof_nnf,[status(thm)],[ax30]) ).
fof(f_30_2,plain,
! [U_59,U_58] :
( organism(U_59,U_58)
| ~ human_person(U_59,U_58) ),
inference(variable_rename,[status(thm)],[f_30_1]) ).
cnf(f_30_3,plain,
( organism(U_59,U_58)
| ~ human_person(U_59,U_58) ),
inference(clausify,[status(thm)],[f_30_2]) ).
fof(f_31_1,plain,
! [U,V] :
( human_person(U,V)
| ~ man(U,V) ),
inference(fof_nnf,[status(thm)],[ax31]) ).
fof(f_31_2,plain,
! [U_61,U_60] :
( human_person(U_61,U_60)
| ~ man(U_61,U_60) ),
inference(variable_rename,[status(thm)],[f_31_1]) ).
cnf(f_31_3,plain,
( human_person(U_61,U_60)
| ~ man(U_61,U_60) ),
inference(clausify,[status(thm)],[f_31_2]) ).
fof(f_32_1,plain,
! [U,V] :
( man(U,V)
| ~ fellow(U,V) ),
inference(fof_nnf,[status(thm)],[ax32]) ).
fof(f_32_2,plain,
! [U_63,U_62] :
( man(U_63,U_62)
| ~ fellow(U_63,U_62) ),
inference(variable_rename,[status(thm)],[f_32_1]) ).
cnf(f_32_3,plain,
( man(U_63,U_62)
| ~ fellow(U_63,U_62) ),
inference(clausify,[status(thm)],[f_32_2]) ).
fof(f_33_1,plain,
! [U,V] :
( event(U,V)
| ~ wear(U,V) ),
inference(fof_nnf,[status(thm)],[ax33]) ).
fof(f_33_2,plain,
! [U_65,U_64] :
( event(U_65,U_64)
| ~ wear(U_65,U_64) ),
inference(variable_rename,[status(thm)],[f_33_1]) ).
cnf(f_33_3,plain,
( event(U_65,U_64)
| ~ wear(U_65,U_64) ),
inference(clausify,[status(thm)],[f_33_2]) ).
fof(f_34_1,plain,
! [U,V] :
( multiple(U,V)
| ~ set(U,V) ),
inference(fof_nnf,[status(thm)],[ax34]) ).
fof(f_34_2,plain,
! [U_67,U_66] :
( multiple(U_67,U_66)
| ~ set(U_67,U_66) ),
inference(variable_rename,[status(thm)],[f_34_1]) ).
cnf(f_34_3,plain,
( multiple(U_67,U_66)
| ~ set(U_67,U_66) ),
inference(clausify,[status(thm)],[f_34_2]) ).
fof(f_35_1,plain,
! [U,V] :
( set(U,V)
| ~ group(U,V) ),
inference(fof_nnf,[status(thm)],[ax35]) ).
fof(f_35_2,plain,
! [U_69,U_68] :
( set(U_69,U_68)
| ~ group(U_69,U_68) ),
inference(variable_rename,[status(thm)],[f_35_1]) ).
cnf(f_35_3,plain,
( set(U_69,U_68)
| ~ group(U_69,U_68) ),
inference(clausify,[status(thm)],[f_35_2]) ).
fof(f_36_1,plain,
! [U,V] :
( artifact(U,V)
| ~ clothes(U,V) ),
inference(fof_nnf,[status(thm)],[ax36]) ).
fof(f_36_2,plain,
! [U_71,U_70] :
( artifact(U_71,U_70)
| ~ clothes(U_71,U_70) ),
inference(variable_rename,[status(thm)],[f_36_1]) ).
cnf(f_36_3,plain,
( artifact(U_71,U_70)
| ~ clothes(U_71,U_70) ),
inference(clausify,[status(thm)],[f_36_2]) ).
fof(f_37_1,plain,
! [U,V] :
( clothes(U,V)
| ~ coat(U,V) ),
inference(fof_nnf,[status(thm)],[ax37]) ).
fof(f_37_2,plain,
! [U_73,U_72] :
( clothes(U_73,U_72)
| ~ coat(U_73,U_72) ),
inference(variable_rename,[status(thm)],[f_37_1]) ).
cnf(f_37_3,plain,
( clothes(U_73,U_72)
| ~ coat(U_73,U_72) ),
inference(clausify,[status(thm)],[f_37_2]) ).
fof(f_38_1,plain,
! [U,V] :
( unisex(U,V)
| ~ object(U,V) ),
inference(fof_nnf,[status(thm)],[ax38]) ).
fof(f_38_2,plain,
! [U_75,U_74] :
( unisex(U_75,U_74)
| ~ object(U_75,U_74) ),
inference(variable_rename,[status(thm)],[f_38_1]) ).
cnf(f_38_3,plain,
( unisex(U_75,U_74)
| ~ object(U_75,U_74) ),
inference(clausify,[status(thm)],[f_38_2]) ).
fof(f_39_1,plain,
! [U,V] :
( impartial(U,V)
| ~ object(U,V) ),
inference(fof_nnf,[status(thm)],[ax39]) ).
fof(f_39_2,plain,
! [U_77,U_76] :
( impartial(U_77,U_76)
| ~ object(U_77,U_76) ),
inference(variable_rename,[status(thm)],[f_39_1]) ).
cnf(f_39_3,plain,
( impartial(U_77,U_76)
| ~ object(U_77,U_76) ),
inference(clausify,[status(thm)],[f_39_2]) ).
fof(f_40_1,plain,
! [U,V] :
( nonliving(U,V)
| ~ object(U,V) ),
inference(fof_nnf,[status(thm)],[ax40]) ).
fof(f_40_2,plain,
! [U_79,U_78] :
( nonliving(U_79,U_78)
| ~ object(U_79,U_78) ),
inference(variable_rename,[status(thm)],[f_40_1]) ).
cnf(f_40_3,plain,
( nonliving(U_79,U_78)
| ~ object(U_79,U_78) ),
inference(clausify,[status(thm)],[f_40_2]) ).
fof(f_41_1,plain,
! [U,V] :
( existent(U,V)
| ~ entity(U,V) ),
inference(fof_nnf,[status(thm)],[ax41]) ).
fof(f_41_2,plain,
! [U_81,U_80] :
( existent(U_81,U_80)
| ~ entity(U_81,U_80) ),
inference(variable_rename,[status(thm)],[f_41_1]) ).
cnf(f_41_3,plain,
( existent(U_81,U_80)
| ~ entity(U_81,U_80) ),
inference(clausify,[status(thm)],[f_41_2]) ).
fof(f_42_1,plain,
! [U,V] :
( specific(U,V)
| ~ entity(U,V) ),
inference(fof_nnf,[status(thm)],[ax42]) ).
fof(f_42_2,plain,
! [U_83,U_82] :
( specific(U_83,U_82)
| ~ entity(U_83,U_82) ),
inference(variable_rename,[status(thm)],[f_42_1]) ).
cnf(f_42_3,plain,
( specific(U_83,U_82)
| ~ entity(U_83,U_82) ),
inference(clausify,[status(thm)],[f_42_2]) ).
fof(f_43_1,plain,
! [U,V] :
( thing(U,V)
| ~ entity(U,V) ),
inference(fof_nnf,[status(thm)],[ax43]) ).
fof(f_43_2,plain,
! [U_85,U_84] :
( thing(U_85,U_84)
| ~ entity(U_85,U_84) ),
inference(variable_rename,[status(thm)],[f_43_1]) ).
cnf(f_43_3,plain,
( thing(U_85,U_84)
| ~ entity(U_85,U_84) ),
inference(clausify,[status(thm)],[f_43_2]) ).
fof(f_44_1,plain,
! [U,V] :
( entity(U,V)
| ~ object(U,V) ),
inference(fof_nnf,[status(thm)],[ax44]) ).
fof(f_44_2,plain,
! [U_87,U_86] :
( entity(U_87,U_86)
| ~ object(U_87,U_86) ),
inference(variable_rename,[status(thm)],[f_44_1]) ).
cnf(f_44_3,plain,
( entity(U_87,U_86)
| ~ object(U_87,U_86) ),
inference(clausify,[status(thm)],[f_44_2]) ).
fof(f_45_1,plain,
! [U,V] :
( object(U,V)
| ~ artifact(U,V) ),
inference(fof_nnf,[status(thm)],[ax45]) ).
fof(f_45_2,plain,
! [U_89,U_88] :
( object(U_89,U_88)
| ~ artifact(U_89,U_88) ),
inference(variable_rename,[status(thm)],[f_45_1]) ).
cnf(f_45_3,plain,
( object(U_89,U_88)
| ~ artifact(U_89,U_88) ),
inference(clausify,[status(thm)],[f_45_2]) ).
fof(f_46_1,plain,
! [U,V] :
( artifact(U,V)
| ~ instrumentality(U,V) ),
inference(fof_nnf,[status(thm)],[ax46]) ).
fof(f_46_2,plain,
! [U_91,U_90] :
( artifact(U_91,U_90)
| ~ instrumentality(U_91,U_90) ),
inference(variable_rename,[status(thm)],[f_46_1]) ).
cnf(f_46_3,plain,
( artifact(U_91,U_90)
| ~ instrumentality(U_91,U_90) ),
inference(clausify,[status(thm)],[f_46_2]) ).
fof(f_47_1,plain,
! [U,V] :
( instrumentality(U,V)
| ~ device(U,V) ),
inference(fof_nnf,[status(thm)],[ax47]) ).
fof(f_47_2,plain,
! [U_93,U_92] :
( instrumentality(U_93,U_92)
| ~ device(U_93,U_92) ),
inference(variable_rename,[status(thm)],[f_47_1]) ).
cnf(f_47_3,plain,
( instrumentality(U_93,U_92)
| ~ device(U_93,U_92) ),
inference(clausify,[status(thm)],[f_47_2]) ).
fof(f_48_1,plain,
! [U,V] :
( device(U,V)
| ~ wheel(U,V) ),
inference(fof_nnf,[status(thm)],[ax48]) ).
fof(f_48_2,plain,
! [U_95,U_94] :
( device(U_95,U_94)
| ~ wheel(U_95,U_94) ),
inference(variable_rename,[status(thm)],[f_48_1]) ).
cnf(f_48_3,plain,
( device(U_95,U_94)
| ~ wheel(U_95,U_94) ),
inference(clausify,[status(thm)],[f_48_2]) ).
fof(f_49_1,plain,
! [U,V] :
( eventuality(U,V)
| ~ event(U,V) ),
inference(fof_nnf,[status(thm)],[ax49]) ).
fof(f_49_2,plain,
! [U_97,U_96] :
( eventuality(U_97,U_96)
| ~ event(U_97,U_96) ),
inference(variable_rename,[status(thm)],[f_49_1]) ).
cnf(f_49_3,plain,
( eventuality(U_97,U_96)
| ~ event(U_97,U_96) ),
inference(clausify,[status(thm)],[f_49_2]) ).
fof(f_50_1,plain,
! [U,V] :
( event(U,V)
| ~ state(U,V) ),
inference(fof_nnf,[status(thm)],[ax50]) ).
fof(f_50_2,plain,
! [U_99,U_98] :
( event(U_99,U_98)
| ~ state(U_99,U_98) ),
inference(variable_rename,[status(thm)],[f_50_1]) ).
cnf(f_50_3,plain,
( event(U_99,U_98)
| ~ state(U_99,U_98) ),
inference(clausify,[status(thm)],[f_50_2]) ).
fof(f_51_1,plain,
! [U,V] :
( unisex(U,V)
| ~ eventuality(U,V) ),
inference(fof_nnf,[status(thm)],[ax51]) ).
fof(f_51_2,plain,
! [U_101,U_100] :
( unisex(U_101,U_100)
| ~ eventuality(U_101,U_100) ),
inference(variable_rename,[status(thm)],[f_51_1]) ).
cnf(f_51_3,plain,
( unisex(U_101,U_100)
| ~ eventuality(U_101,U_100) ),
inference(clausify,[status(thm)],[f_51_2]) ).
fof(f_52_1,plain,
! [U,V] :
( nonexistent(U,V)
| ~ eventuality(U,V) ),
inference(fof_nnf,[status(thm)],[ax52]) ).
fof(f_52_2,plain,
! [U_103,U_102] :
( nonexistent(U_103,U_102)
| ~ eventuality(U_103,U_102) ),
inference(variable_rename,[status(thm)],[f_52_1]) ).
cnf(f_52_3,plain,
( nonexistent(U_103,U_102)
| ~ eventuality(U_103,U_102) ),
inference(clausify,[status(thm)],[f_52_2]) ).
fof(f_53_1,plain,
! [U,V] :
( specific(U,V)
| ~ eventuality(U,V) ),
inference(fof_nnf,[status(thm)],[ax53]) ).
fof(f_53_2,plain,
! [U_105,U_104] :
( specific(U_105,U_104)
| ~ eventuality(U_105,U_104) ),
inference(variable_rename,[status(thm)],[f_53_1]) ).
cnf(f_53_3,plain,
( specific(U_105,U_104)
| ~ eventuality(U_105,U_104) ),
inference(clausify,[status(thm)],[f_53_2]) ).
fof(f_54_1,plain,
! [U,V] :
( singleton(U,V)
| ~ thing(U,V) ),
inference(fof_nnf,[status(thm)],[ax54]) ).
fof(f_54_2,plain,
! [U_107,U_106] :
( singleton(U_107,U_106)
| ~ thing(U_107,U_106) ),
inference(variable_rename,[status(thm)],[f_54_1]) ).
cnf(f_54_3,plain,
( singleton(U_107,U_106)
| ~ thing(U_107,U_106) ),
inference(clausify,[status(thm)],[f_54_2]) ).
fof(f_55_1,plain,
! [U,V] :
( thing(U,V)
| ~ eventuality(U,V) ),
inference(fof_nnf,[status(thm)],[ax55]) ).
fof(f_55_2,plain,
! [U_109,U_108] :
( thing(U_109,U_108)
| ~ eventuality(U_109,U_108) ),
inference(variable_rename,[status(thm)],[f_55_1]) ).
cnf(f_55_3,plain,
( thing(U_109,U_108)
| ~ eventuality(U_109,U_108) ),
inference(clausify,[status(thm)],[f_55_2]) ).
fof(f_56_1,plain,
! [U,V] :
( eventuality(U,V)
| ~ state(U,V) ),
inference(fof_nnf,[status(thm)],[ax56]) ).
fof(f_56_2,plain,
! [U_111,U_110] :
( eventuality(U_111,U_110)
| ~ state(U_111,U_110) ),
inference(variable_rename,[status(thm)],[f_56_1]) ).
cnf(f_56_3,plain,
( eventuality(U_111,U_110)
| ~ state(U_111,U_110) ),
inference(clausify,[status(thm)],[f_56_2]) ).
fof(f_57_1,plain,
! [U,V] :
( ~ nonliving(U,V)
| ~ animate(U,V) ),
inference(fof_nnf,[status(thm)],[ax57]) ).
fof(f_57_2,plain,
! [U_113,U_112] :
( ~ nonliving(U_113,U_112)
| ~ animate(U_113,U_112) ),
inference(variable_rename,[status(thm)],[f_57_1]) ).
cnf(f_57_3,plain,
( ~ nonliving(U_113,U_112)
| ~ animate(U_113,U_112) ),
inference(clausify,[status(thm)],[f_57_2]) ).
fof(f_58_1,plain,
! [U,V] :
( ~ nonexistent(U,V)
| ~ existent(U,V) ),
inference(fof_nnf,[status(thm)],[ax58]) ).
fof(f_58_2,plain,
! [U_115,U_114] :
( ~ nonexistent(U_115,U_114)
| ~ existent(U_115,U_114) ),
inference(variable_rename,[status(thm)],[f_58_1]) ).
cnf(f_58_3,plain,
( ~ nonexistent(U_115,U_114)
| ~ existent(U_115,U_114) ),
inference(clausify,[status(thm)],[f_58_2]) ).
fof(f_59_1,plain,
! [U,V] :
( ~ human(U,V)
| ~ nonhuman(U,V) ),
inference(fof_nnf,[status(thm)],[ax59]) ).
fof(f_59_2,plain,
! [U_117,U_116] :
( ~ human(U_117,U_116)
| ~ nonhuman(U_117,U_116) ),
inference(variable_rename,[status(thm)],[f_59_1]) ).
cnf(f_59_3,plain,
( ~ human(U_117,U_116)
| ~ nonhuman(U_117,U_116) ),
inference(clausify,[status(thm)],[f_59_2]) ).
fof(f_60_1,plain,
! [U,V] :
( ~ living(U,V)
| ~ nonliving(U,V) ),
inference(fof_nnf,[status(thm)],[ax60]) ).
fof(f_60_2,plain,
! [U_119,U_118] :
( ~ living(U_119,U_118)
| ~ nonliving(U_119,U_118) ),
inference(variable_rename,[status(thm)],[f_60_1]) ).
cnf(f_60_3,plain,
( ~ living(U_119,U_118)
| ~ nonliving(U_119,U_118) ),
inference(clausify,[status(thm)],[f_60_2]) ).
fof(f_61_1,plain,
! [U,V] :
( ~ multiple(U,V)
| ~ singleton(U,V) ),
inference(fof_nnf,[status(thm)],[ax61]) ).
fof(f_61_2,plain,
! [U_121,U_120] :
( ~ multiple(U_121,U_120)
| ~ singleton(U_121,U_120) ),
inference(variable_rename,[status(thm)],[f_61_1]) ).
cnf(f_61_3,plain,
( ~ multiple(U_121,U_120)
| ~ singleton(U_121,U_120) ),
inference(clausify,[status(thm)],[f_61_2]) ).
fof(f_62_1,plain,
! [U,V] :
( ~ general(U,V)
| ~ specific(U,V) ),
inference(fof_nnf,[status(thm)],[ax62]) ).
fof(f_62_2,plain,
! [U_123,U_122] :
( ~ general(U_123,U_122)
| ~ specific(U_123,U_122) ),
inference(variable_rename,[status(thm)],[f_62_1]) ).
cnf(f_62_3,plain,
( ~ general(U_123,U_122)
| ~ specific(U_123,U_122) ),
inference(clausify,[status(thm)],[f_62_2]) ).
fof(f_63_1,plain,
! [U,V] :
( ~ male(U,V)
| ~ unisex(U,V) ),
inference(fof_nnf,[status(thm)],[ax63]) ).
fof(f_63_2,plain,
! [U_125,U_124] :
( ~ male(U_125,U_124)
| ~ unisex(U_125,U_124) ),
inference(variable_rename,[status(thm)],[f_63_1]) ).
cnf(f_63_3,plain,
( ~ male(U_125,U_124)
| ~ unisex(U_125,U_124) ),
inference(clausify,[status(thm)],[f_63_2]) ).
fof(f_64_1,plain,
! [U,V] :
( ~ black(U,V)
| ~ white(U,V) ),
inference(fof_nnf,[status(thm)],[ax64]) ).
fof(f_64_2,plain,
! [U_127,U_126] :
( ~ black(U_127,U_126)
| ~ white(U_127,U_126) ),
inference(variable_rename,[status(thm)],[f_64_1]) ).
cnf(f_64_3,plain,
( ~ black(U_127,U_126)
| ~ white(U_127,U_126) ),
inference(clausify,[status(thm)],[f_64_2]) ).
fof(f_65_1,plain,
! [U,V] :
( ~ old(U,V)
| ~ young(U,V) ),
inference(fof_nnf,[status(thm)],[ax65]) ).
fof(f_65_2,plain,
! [U_129,U_128] :
( ~ old(U_129,U_128)
| ~ young(U_129,U_128) ),
inference(variable_rename,[status(thm)],[f_65_1]) ).
cnf(f_65_3,plain,
( ~ old(U_129,U_128)
| ~ young(U_129,U_128) ),
inference(clausify,[status(thm)],[f_65_2]) ).
fof(f_66_1,plain,
! [U,V,W] :
( ! [X] :
( ~ of(U,X,V)
| X = W
| ~ forename(U,X) )
| ~ of(U,W,V)
| ~ forename(U,W)
| ~ entity(U,V) ),
inference(fof_nnf,[status(thm)],[ax66]) ).
fof(f_66_2,plain,
! [U_133,U_132,U_131] :
( ! [U_130] :
( ~ of(U_133,U_130,U_132)
| U_130 = U_131
| ~ forename(U_133,U_130) )
| ~ of(U_133,U_131,U_132)
| ~ forename(U_133,U_131)
| ~ entity(U_133,U_132) ),
inference(variable_rename,[status(thm)],[f_66_1]) ).
cnf(f_66_3,plain,
( ~ of(U_133,U_130,U_132)
| U_130 = U_131
| ~ forename(U_133,U_130)
| ~ of(U_133,U_131,U_132)
| ~ forename(U_133,U_131)
| ~ entity(U_133,U_132) ),
inference(clausify,[status(thm)],[f_66_2]) ).
fof(f_67_1,plain,
! [U,V,W] :
( ! [X] :
( ~ of(U,X,V)
| X = W
| ~ placename(U,X) )
| ~ of(U,W,V)
| ~ placename(U,W)
| ~ entity(U,V) ),
inference(fof_nnf,[status(thm)],[ax67]) ).
fof(f_67_2,plain,
! [U_137,U_136,U_135] :
( ! [U_134] :
( ~ of(U_137,U_134,U_136)
| U_134 = U_135
| ~ placename(U_137,U_134) )
| ~ of(U_137,U_135,U_136)
| ~ placename(U_137,U_135)
| ~ entity(U_137,U_136) ),
inference(variable_rename,[status(thm)],[f_67_1]) ).
cnf(f_67_3,plain,
( ~ of(U_137,U_134,U_136)
| U_134 = U_135
| ~ placename(U_137,U_134)
| ~ of(U_137,U_135,U_136)
| ~ placename(U_137,U_135)
| ~ entity(U_137,U_136) ),
inference(clausify,[status(thm)],[f_67_2]) ).
fof(f_68_1,plain,
! [U,V] :
( ( two(U,V)
| ! [W] :
( ! [X] :
( ? [Y] :
( Y != W
& Y != X
& member(U,Y,V) )
| X = W
| ~ member(U,X,V) )
| ~ member(U,W,V) ) )
& ( ? [W] :
( ? [X] :
( ! [Y] :
( Y = W
| Y = X
| ~ member(U,Y,V) )
& X != W
& member(U,X,V) )
& member(U,W,V) )
| ~ two(U,V) ) ),
inference(fof_nnf,[status(thm)],[ax68]) ).
fof(f_68_2,plain,
! [U_145,U_144] :
( ( two(U_145,U_144)
| ! [U_143] :
( ! [U_142] :
( ? [U_141] :
( U_141 != U_143
& U_141 != U_142
& member(U_145,U_141,U_144) )
| U_142 = U_143
| ~ member(U_145,U_142,U_144) )
| ~ member(U_145,U_143,U_144) ) )
& ( ? [U_140] :
( ? [U_139] :
( ! [U_138] :
( U_138 = U_140
| U_138 = U_139
| ~ member(U_145,U_138,U_144) )
& U_139 != U_140
& member(U_145,U_139,U_144) )
& member(U_145,U_140,U_144) )
| ~ two(U_145,U_144) ) ),
inference(variable_rename,[status(thm)],[f_68_1]) ).
fof(f_68_3,plain,
( ! [U_149,U_147] :
( two(U_149,U_147)
| ! [U_143] :
( ! [U_142] :
( ? [U_141] :
( U_141 != U_143
& U_141 != U_142
& member(U_149,U_141,U_147) )
| U_142 = U_143
| ~ member(U_149,U_142,U_147) )
| ~ member(U_149,U_143,U_147) ) )
& ! [U_148,U_146] :
( ? [U_140] :
( ? [U_139] :
( ! [U_138] :
( U_138 = U_140
| U_138 = U_139
| ~ member(U_148,U_138,U_146) )
& U_139 != U_140
& member(U_148,U_139,U_146) )
& member(U_148,U_140,U_146) )
| ~ two(U_148,U_146) ) ),
inference(miniscope,[status(thm)],[f_68_2]) ).
fof(f_68_4,plain,
( ! [U_149,U_147] :
( two(U_149,U_147)
| ! [U_143] :
( ! [U_142] :
( ? [U_141] :
( U_141 != U_143
& U_141 != U_142
& member(U_149,U_141,U_147) )
| U_142 = U_143
| ~ member(U_149,U_142,U_147) )
| ~ member(U_149,U_143,U_147) ) )
& ! [U_148,U_146] :
( ( ? [U_139] :
( ! [U_138] :
( U_138 = sK1(U_148,U_146)
| U_138 = U_139
| ~ member(U_148,U_138,U_146) )
& U_139 != sK1(U_148,U_146)
& member(U_148,U_139,U_146) )
& member(U_148,sK1(U_148,U_146),U_146) )
| ~ two(U_148,U_146) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_140,sK1(U_148,U_146))],[f_68_3]) ).
fof(f_68_5,plain,
( ! [U_149,U_147] :
( two(U_149,U_147)
| ! [U_143] :
( ! [U_142] :
( ? [U_141] :
( U_141 != U_143
& U_141 != U_142
& member(U_149,U_141,U_147) )
| U_142 = U_143
| ~ member(U_149,U_142,U_147) )
| ~ member(U_149,U_143,U_147) ) )
& ! [U_148,U_146] :
( ( ! [U_138] :
( U_138 = sK1(U_148,U_146)
| U_138 = sK2(U_148,U_146)
| ~ member(U_148,U_138,U_146) )
& sK2(U_148,U_146) != sK1(U_148,U_146)
& member(U_148,sK2(U_148,U_146),U_146)
& member(U_148,sK1(U_148,U_146),U_146) )
| ~ two(U_148,U_146) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_139,sK2(U_148,U_146))],[f_68_4]) ).
fof(f_68_6,plain,
( ! [U_149,U_147] :
( two(U_149,U_147)
| ! [U_143] :
( ! [U_142] :
( ( sK3(U_149,U_147,U_143,U_142) != U_143
& sK3(U_149,U_147,U_143,U_142) != U_142
& member(U_149,sK3(U_149,U_147,U_143,U_142),U_147) )
| U_142 = U_143
| ~ member(U_149,U_142,U_147) )
| ~ member(U_149,U_143,U_147) ) )
& ! [U_148,U_146] :
( ( ! [U_138] :
( U_138 = sK1(U_148,U_146)
| U_138 = sK2(U_148,U_146)
| ~ member(U_148,U_138,U_146) )
& sK2(U_148,U_146) != sK1(U_148,U_146)
& member(U_148,sK2(U_148,U_146),U_146)
& member(U_148,sK1(U_148,U_146),U_146) )
| ~ two(U_148,U_146) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_141,sK3(U_149,U_147,U_143,U_142))],[f_68_5]) ).
cnf(f_68_7,plain,
( member(U_148,sK1(U_148,U_146),U_146)
| ~ two(U_148,U_146) ),
inference(clausify,[status(thm)],[f_68_6]) ).
cnf(f_68_8,plain,
( member(U_148,sK2(U_148,U_146),U_146)
| ~ two(U_148,U_146) ),
inference(clausify,[status(thm)],[f_68_6]) ).
cnf(f_68_9,plain,
( sK2(U_148,U_146) != sK1(U_148,U_146)
| ~ two(U_148,U_146) ),
inference(clausify,[status(thm)],[f_68_6]) ).
cnf(f_68_10,plain,
( U_138 = sK1(U_148,U_146)
| U_138 = sK2(U_148,U_146)
| ~ member(U_148,U_138,U_146)
| ~ two(U_148,U_146) ),
inference(clausify,[status(thm)],[f_68_6]) ).
cnf(f_68_11,plain,
( member(U_149,sK3(U_149,U_147,U_143,U_142),U_147)
| U_142 = U_143
| ~ member(U_149,U_142,U_147)
| ~ member(U_149,U_143,U_147)
| two(U_149,U_147) ),
inference(clausify,[status(thm)],[f_68_6]) ).
cnf(f_68_12,plain,
( sK3(U_149,U_147,U_143,U_142) != U_142
| U_142 = U_143
| ~ member(U_149,U_142,U_147)
| ~ member(U_149,U_143,U_147)
| two(U_149,U_147) ),
inference(clausify,[status(thm)],[f_68_6]) ).
cnf(f_68_13,plain,
( sK3(U_149,U_147,U_143,U_142) != U_143
| U_142 = U_143
| ~ member(U_149,U_142,U_147)
| ~ member(U_149,U_143,U_147)
| two(U_149,U_147) ),
inference(clausify,[status(thm)],[f_68_6]) ).
fof(f_69_1,plain,
! [U,V,W,X] :
( W != X
| ~ patient(U,V,X)
| ~ agent(U,V,W)
| ~ nonreflexive(U,V) ),
inference(fof_nnf,[status(thm)],[ax69]) ).
fof(f_69_2,plain,
! [U_153,U_152,U_151,U_150] :
( U_151 != U_150
| ~ patient(U_153,U_152,U_150)
| ~ agent(U_153,U_152,U_151)
| ~ nonreflexive(U_153,U_152) ),
inference(variable_rename,[status(thm)],[f_69_1]) ).
cnf(f_69_3,plain,
( U_151 != U_150
| ~ patient(U_153,U_152,U_150)
| ~ agent(U_153,U_152,U_151)
| ~ nonreflexive(U_153,U_152) ),
inference(clausify,[status(thm)],[f_69_2]) ).
fof(f_70_1,plain,
! [U,V] : ~ member(U,V,V),
inference(fof_nnf,[status(thm)],[ax70]) ).
fof(f_70_2,plain,
! [U_155,U_154] : ~ member(U_155,U_154,U_154),
inference(variable_rename,[status(thm)],[f_70_1]) ).
cnf(f_70_3,plain,
~ member(U_155,U_154,U_154),
inference(clausify,[status(thm)],[f_70_2]) ).
fof(f_71_1,plain,
! [U,V,W,X] :
( W = X
| ~ be(U,V,W,X) ),
inference(fof_nnf,[status(thm)],[ax71]) ).
fof(f_71_2,plain,
! [U_159,U_158,U_157,U_156] :
( U_157 = U_156
| ~ be(U_159,U_158,U_157,U_156) ),
inference(variable_rename,[status(thm)],[f_71_1]) ).
cnf(f_71_3,plain,
( U_157 = U_156
| ~ be(U_159,U_158,U_157,U_156) ),
inference(clausify,[status(thm)],[f_71_2]) ).
fof(f_72_1,negated_conjecture,
? [U] :
( ? [V,W,X,Y,Z,X1,X2,X3,X4,X5,X6] :
( behind(U,X6,X6)
& be(U,X5,V,X6)
& state(U,X5)
& wheel(U,X6)
& ! [X14] :
( member(U,X14,X4)
=> ( cheap(U,X14)
& black(U,X14)
& coat(U,X14) ) )
& group(U,X4)
& ! [X11] :
( member(U,X11,X4)
=> ! [X12] :
( member(U,X12,X3)
=> ? [X13] :
( wear(U,X13)
& nonreflexive(U,X13)
& present(U,X13)
& patient(U,X13,X11)
& agent(U,X13,X12)
& event(U,X13) ) ) )
& ! [X10] :
( member(U,X10,X3)
=> ( young(U,X10)
& fellow(U,X10) ) )
& group(U,X3)
& two(U,X3)
& ! [X7] :
( member(U,X7,X3)
=> ? [X8,X9] :
( in(U,X9,X)
& be(U,X8,X7,X9)
& state(U,X8) ) )
& in(U,X2,X1)
& down(U,X2,X1)
& barrel(U,X2)
& present(U,X2)
& agent(U,X2,Y)
& event(U,X2)
& lonely(U,X1)
& street(U,X1)
& placename(U,Z)
& hollywood_placename(U,Z)
& city(U,X1)
& of(U,Z,X1)
& old(U,Y)
& dirty(U,Y)
& white(U,Y)
& chevy(U,Y)
& frontseat(U,X)
& forename(U,W)
& jules_forename(U,W)
& man(U,V)
& of(U,W,V) )
& actual_world(U) ),
inference(negate,[status(cth)],[co1]) ).
fof(f_72_2,negated_conjecture,
? [U] :
( ? [V,W,X,Y,Z,X1,X2,X3,X4,X5,X6] :
( behind(U,X6,X6)
& be(U,X5,V,X6)
& state(U,X5)
& wheel(U,X6)
& ! [X14] :
( ( cheap(U,X14)
& black(U,X14)
& coat(U,X14) )
| ~ member(U,X14,X4) )
& group(U,X4)
& ! [X11] :
( ! [X12] :
( ? [X13] :
( wear(U,X13)
& nonreflexive(U,X13)
& present(U,X13)
& patient(U,X13,X11)
& agent(U,X13,X12)
& event(U,X13) )
| ~ member(U,X12,X3) )
| ~ member(U,X11,X4) )
& ! [X10] :
( ( young(U,X10)
& fellow(U,X10) )
| ~ member(U,X10,X3) )
& group(U,X3)
& two(U,X3)
& ! [X7] :
( ? [X8,X9] :
( in(U,X9,X)
& be(U,X8,X7,X9)
& state(U,X8) )
| ~ member(U,X7,X3) )
& in(U,X2,X1)
& down(U,X2,X1)
& barrel(U,X2)
& present(U,X2)
& agent(U,X2,Y)
& event(U,X2)
& lonely(U,X1)
& street(U,X1)
& placename(U,Z)
& hollywood_placename(U,Z)
& city(U,X1)
& of(U,Z,X1)
& old(U,Y)
& dirty(U,Y)
& white(U,Y)
& chevy(U,Y)
& frontseat(U,X)
& forename(U,W)
& jules_forename(U,W)
& man(U,V)
& of(U,W,V) )
& actual_world(U) ),
inference(fof_nnf,[status(thm)],[f_72_1]) ).
fof(f_72_3,negated_conjecture,
? [U_179] :
( ? [U_178,U_177,U_176,U_175,U_174,U_173,U_172,U_171,U_170,U_169,U_168] :
( behind(U_179,U_168,U_168)
& be(U_179,U_169,U_178,U_168)
& state(U_179,U_169)
& wheel(U_179,U_168)
& ! [U_167] :
( ( cheap(U_179,U_167)
& black(U_179,U_167)
& coat(U_179,U_167) )
| ~ member(U_179,U_167,U_170) )
& group(U_179,U_170)
& ! [U_166] :
( ! [U_165] :
( ? [U_164] :
( wear(U_179,U_164)
& nonreflexive(U_179,U_164)
& present(U_179,U_164)
& patient(U_179,U_164,U_166)
& agent(U_179,U_164,U_165)
& event(U_179,U_164) )
| ~ member(U_179,U_165,U_171) )
| ~ member(U_179,U_166,U_170) )
& ! [U_163] :
( ( young(U_179,U_163)
& fellow(U_179,U_163) )
| ~ member(U_179,U_163,U_171) )
& group(U_179,U_171)
& two(U_179,U_171)
& ! [U_162] :
( ? [U_161,U_160] :
( in(U_179,U_160,U_176)
& be(U_179,U_161,U_162,U_160)
& state(U_179,U_161) )
| ~ member(U_179,U_162,U_171) )
& in(U_179,U_172,U_173)
& down(U_179,U_172,U_173)
& barrel(U_179,U_172)
& present(U_179,U_172)
& agent(U_179,U_172,U_175)
& event(U_179,U_172)
& lonely(U_179,U_173)
& street(U_179,U_173)
& placename(U_179,U_174)
& hollywood_placename(U_179,U_174)
& city(U_179,U_173)
& of(U_179,U_174,U_173)
& old(U_179,U_175)
& dirty(U_179,U_175)
& white(U_179,U_175)
& chevy(U_179,U_175)
& frontseat(U_179,U_176)
& forename(U_179,U_177)
& jules_forename(U_179,U_177)
& man(U_179,U_178)
& of(U_179,U_177,U_178) )
& actual_world(U_179) ),
inference(variable_rename,[status(thm)],[f_72_2]) ).
fof(f_72_4,negated_conjecture,
? [U_179] :
( ? [U_178] :
( ? [U_177] :
( forename(U_179,U_177)
& jules_forename(U_179,U_177)
& of(U_179,U_177,U_178) )
& ? [U_169] :
( ? [U_168] :
( behind(U_179,U_168,U_168)
& be(U_179,U_169,U_178,U_168)
& wheel(U_179,U_168) )
& state(U_179,U_169) )
& man(U_179,U_178) )
& ? [U_176] :
( ? [U_171] :
( ? [U_170] :
( ! [U_167] :
( ( cheap(U_179,U_167)
& black(U_179,U_167)
& coat(U_179,U_167) )
| ~ member(U_179,U_167,U_170) )
& group(U_179,U_170)
& ! [U_166] :
( ! [U_165] :
( ? [U_164] :
( wear(U_179,U_164)
& nonreflexive(U_179,U_164)
& present(U_179,U_164)
& patient(U_179,U_164,U_166)
& agent(U_179,U_164,U_165)
& event(U_179,U_164) )
| ~ member(U_179,U_165,U_171) )
| ~ member(U_179,U_166,U_170) ) )
& ! [U_163] :
( ( young(U_179,U_163)
& fellow(U_179,U_163) )
| ~ member(U_179,U_163,U_171) )
& group(U_179,U_171)
& two(U_179,U_171)
& ! [U_162] :
( ? [U_161] :
( ? [U_160] :
( in(U_179,U_160,U_176)
& be(U_179,U_161,U_162,U_160) )
& state(U_179,U_161) )
| ~ member(U_179,U_162,U_171) ) )
& frontseat(U_179,U_176) )
& ? [U_175] :
( ? [U_174] :
( ? [U_173] :
( ? [U_172] :
( in(U_179,U_172,U_173)
& down(U_179,U_172,U_173)
& barrel(U_179,U_172)
& present(U_179,U_172)
& agent(U_179,U_172,U_175)
& event(U_179,U_172) )
& lonely(U_179,U_173)
& street(U_179,U_173)
& city(U_179,U_173)
& of(U_179,U_174,U_173) )
& placename(U_179,U_174)
& hollywood_placename(U_179,U_174) )
& old(U_179,U_175)
& dirty(U_179,U_175)
& white(U_179,U_175)
& chevy(U_179,U_175) )
& actual_world(U_179) ),
inference(miniscope,[status(thm)],[f_72_3]) ).
fof(f_72_5,negated_conjecture,
( ? [U_178] :
( ? [U_177] :
( forename(sK4,U_177)
& jules_forename(sK4,U_177)
& of(sK4,U_177,U_178) )
& ? [U_169] :
( ? [U_168] :
( behind(sK4,U_168,U_168)
& be(sK4,U_169,U_178,U_168)
& wheel(sK4,U_168) )
& state(sK4,U_169) )
& man(sK4,U_178) )
& ? [U_176] :
( ? [U_171] :
( ? [U_170] :
( ! [U_167] :
( ( cheap(sK4,U_167)
& black(sK4,U_167)
& coat(sK4,U_167) )
| ~ member(sK4,U_167,U_170) )
& group(sK4,U_170)
& ! [U_166] :
( ! [U_165] :
( ? [U_164] :
( wear(sK4,U_164)
& nonreflexive(sK4,U_164)
& present(sK4,U_164)
& patient(sK4,U_164,U_166)
& agent(sK4,U_164,U_165)
& event(sK4,U_164) )
| ~ member(sK4,U_165,U_171) )
| ~ member(sK4,U_166,U_170) ) )
& ! [U_163] :
( ( young(sK4,U_163)
& fellow(sK4,U_163) )
| ~ member(sK4,U_163,U_171) )
& group(sK4,U_171)
& two(sK4,U_171)
& ! [U_162] :
( ? [U_161] :
( ? [U_160] :
( in(sK4,U_160,U_176)
& be(sK4,U_161,U_162,U_160) )
& state(sK4,U_161) )
| ~ member(sK4,U_162,U_171) ) )
& frontseat(sK4,U_176) )
& ? [U_175] :
( ? [U_174] :
( ? [U_173] :
( ? [U_172] :
( in(sK4,U_172,U_173)
& down(sK4,U_172,U_173)
& barrel(sK4,U_172)
& present(sK4,U_172)
& agent(sK4,U_172,U_175)
& event(sK4,U_172) )
& lonely(sK4,U_173)
& street(sK4,U_173)
& city(sK4,U_173)
& of(sK4,U_174,U_173) )
& placename(sK4,U_174)
& hollywood_placename(sK4,U_174) )
& old(sK4,U_175)
& dirty(sK4,U_175)
& white(sK4,U_175)
& chevy(sK4,U_175) )
& actual_world(sK4) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_179,sK4)],[f_72_4]) ).
fof(f_72_6,negated_conjecture,
( ? [U_178] :
( ? [U_177] :
( forename(sK4,U_177)
& jules_forename(sK4,U_177)
& of(sK4,U_177,U_178) )
& ? [U_169] :
( ? [U_168] :
( behind(sK4,U_168,U_168)
& be(sK4,U_169,U_178,U_168)
& wheel(sK4,U_168) )
& state(sK4,U_169) )
& man(sK4,U_178) )
& ? [U_176] :
( ? [U_171] :
( ? [U_170] :
( ! [U_167] :
( ( cheap(sK4,U_167)
& black(sK4,U_167)
& coat(sK4,U_167) )
| ~ member(sK4,U_167,U_170) )
& group(sK4,U_170)
& ! [U_166] :
( ! [U_165] :
( ? [U_164] :
( wear(sK4,U_164)
& nonreflexive(sK4,U_164)
& present(sK4,U_164)
& patient(sK4,U_164,U_166)
& agent(sK4,U_164,U_165)
& event(sK4,U_164) )
| ~ member(sK4,U_165,U_171) )
| ~ member(sK4,U_166,U_170) ) )
& ! [U_163] :
( ( young(sK4,U_163)
& fellow(sK4,U_163) )
| ~ member(sK4,U_163,U_171) )
& group(sK4,U_171)
& two(sK4,U_171)
& ! [U_162] :
( ? [U_161] :
( ? [U_160] :
( in(sK4,U_160,U_176)
& be(sK4,U_161,U_162,U_160) )
& state(sK4,U_161) )
| ~ member(sK4,U_162,U_171) ) )
& frontseat(sK4,U_176) )
& ? [U_174] :
( ? [U_173] :
( ? [U_172] :
( in(sK4,U_172,U_173)
& down(sK4,U_172,U_173)
& barrel(sK4,U_172)
& present(sK4,U_172)
& agent(sK4,U_172,sK5)
& event(sK4,U_172) )
& lonely(sK4,U_173)
& street(sK4,U_173)
& city(sK4,U_173)
& of(sK4,U_174,U_173) )
& placename(sK4,U_174)
& hollywood_placename(sK4,U_174) )
& old(sK4,sK5)
& dirty(sK4,sK5)
& white(sK4,sK5)
& chevy(sK4,sK5)
& actual_world(sK4) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_175,sK5)],[f_72_5]) ).
fof(f_72_7,negated_conjecture,
( ? [U_178] :
( ? [U_177] :
( forename(sK4,U_177)
& jules_forename(sK4,U_177)
& of(sK4,U_177,U_178) )
& ? [U_169] :
( ? [U_168] :
( behind(sK4,U_168,U_168)
& be(sK4,U_169,U_178,U_168)
& wheel(sK4,U_168) )
& state(sK4,U_169) )
& man(sK4,U_178) )
& ? [U_176] :
( ? [U_171] :
( ? [U_170] :
( ! [U_167] :
( ( cheap(sK4,U_167)
& black(sK4,U_167)
& coat(sK4,U_167) )
| ~ member(sK4,U_167,U_170) )
& group(sK4,U_170)
& ! [U_166] :
( ! [U_165] :
( ? [U_164] :
( wear(sK4,U_164)
& nonreflexive(sK4,U_164)
& present(sK4,U_164)
& patient(sK4,U_164,U_166)
& agent(sK4,U_164,U_165)
& event(sK4,U_164) )
| ~ member(sK4,U_165,U_171) )
| ~ member(sK4,U_166,U_170) ) )
& ! [U_163] :
( ( young(sK4,U_163)
& fellow(sK4,U_163) )
| ~ member(sK4,U_163,U_171) )
& group(sK4,U_171)
& two(sK4,U_171)
& ! [U_162] :
( ? [U_161] :
( ? [U_160] :
( in(sK4,U_160,U_176)
& be(sK4,U_161,U_162,U_160) )
& state(sK4,U_161) )
| ~ member(sK4,U_162,U_171) ) )
& frontseat(sK4,U_176) )
& ? [U_173] :
( ? [U_172] :
( in(sK4,U_172,U_173)
& down(sK4,U_172,U_173)
& barrel(sK4,U_172)
& present(sK4,U_172)
& agent(sK4,U_172,sK5)
& event(sK4,U_172) )
& lonely(sK4,U_173)
& street(sK4,U_173)
& city(sK4,U_173)
& of(sK4,sK6,U_173) )
& placename(sK4,sK6)
& hollywood_placename(sK4,sK6)
& old(sK4,sK5)
& dirty(sK4,sK5)
& white(sK4,sK5)
& chevy(sK4,sK5)
& actual_world(sK4) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_174,sK6)],[f_72_6]) ).
fof(f_72_8,negated_conjecture,
( ? [U_178] :
( ? [U_177] :
( forename(sK4,U_177)
& jules_forename(sK4,U_177)
& of(sK4,U_177,U_178) )
& ? [U_169] :
( ? [U_168] :
( behind(sK4,U_168,U_168)
& be(sK4,U_169,U_178,U_168)
& wheel(sK4,U_168) )
& state(sK4,U_169) )
& man(sK4,U_178) )
& ? [U_176] :
( ? [U_171] :
( ? [U_170] :
( ! [U_167] :
( ( cheap(sK4,U_167)
& black(sK4,U_167)
& coat(sK4,U_167) )
| ~ member(sK4,U_167,U_170) )
& group(sK4,U_170)
& ! [U_166] :
( ! [U_165] :
( ? [U_164] :
( wear(sK4,U_164)
& nonreflexive(sK4,U_164)
& present(sK4,U_164)
& patient(sK4,U_164,U_166)
& agent(sK4,U_164,U_165)
& event(sK4,U_164) )
| ~ member(sK4,U_165,U_171) )
| ~ member(sK4,U_166,U_170) ) )
& ! [U_163] :
( ( young(sK4,U_163)
& fellow(sK4,U_163) )
| ~ member(sK4,U_163,U_171) )
& group(sK4,U_171)
& two(sK4,U_171)
& ! [U_162] :
( ? [U_161] :
( ? [U_160] :
( in(sK4,U_160,U_176)
& be(sK4,U_161,U_162,U_160) )
& state(sK4,U_161) )
| ~ member(sK4,U_162,U_171) ) )
& frontseat(sK4,U_176) )
& ? [U_172] :
( in(sK4,U_172,sK7)
& down(sK4,U_172,sK7)
& barrel(sK4,U_172)
& present(sK4,U_172)
& agent(sK4,U_172,sK5)
& event(sK4,U_172) )
& lonely(sK4,sK7)
& street(sK4,sK7)
& city(sK4,sK7)
& of(sK4,sK6,sK7)
& placename(sK4,sK6)
& hollywood_placename(sK4,sK6)
& old(sK4,sK5)
& dirty(sK4,sK5)
& white(sK4,sK5)
& chevy(sK4,sK5)
& actual_world(sK4) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_173,sK7)],[f_72_7]) ).
fof(f_72_9,negated_conjecture,
( ? [U_178] :
( ? [U_177] :
( forename(sK4,U_177)
& jules_forename(sK4,U_177)
& of(sK4,U_177,U_178) )
& ? [U_169] :
( ? [U_168] :
( behind(sK4,U_168,U_168)
& be(sK4,U_169,U_178,U_168)
& wheel(sK4,U_168) )
& state(sK4,U_169) )
& man(sK4,U_178) )
& ? [U_176] :
( ? [U_171] :
( ? [U_170] :
( ! [U_167] :
( ( cheap(sK4,U_167)
& black(sK4,U_167)
& coat(sK4,U_167) )
| ~ member(sK4,U_167,U_170) )
& group(sK4,U_170)
& ! [U_166] :
( ! [U_165] :
( ? [U_164] :
( wear(sK4,U_164)
& nonreflexive(sK4,U_164)
& present(sK4,U_164)
& patient(sK4,U_164,U_166)
& agent(sK4,U_164,U_165)
& event(sK4,U_164) )
| ~ member(sK4,U_165,U_171) )
| ~ member(sK4,U_166,U_170) ) )
& ! [U_163] :
( ( young(sK4,U_163)
& fellow(sK4,U_163) )
| ~ member(sK4,U_163,U_171) )
& group(sK4,U_171)
& two(sK4,U_171)
& ! [U_162] :
( ? [U_161] :
( ? [U_160] :
( in(sK4,U_160,U_176)
& be(sK4,U_161,U_162,U_160) )
& state(sK4,U_161) )
| ~ member(sK4,U_162,U_171) ) )
& frontseat(sK4,U_176) )
& in(sK4,sK8,sK7)
& down(sK4,sK8,sK7)
& barrel(sK4,sK8)
& present(sK4,sK8)
& agent(sK4,sK8,sK5)
& event(sK4,sK8)
& lonely(sK4,sK7)
& street(sK4,sK7)
& city(sK4,sK7)
& of(sK4,sK6,sK7)
& placename(sK4,sK6)
& hollywood_placename(sK4,sK6)
& old(sK4,sK5)
& dirty(sK4,sK5)
& white(sK4,sK5)
& chevy(sK4,sK5)
& actual_world(sK4) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_172,sK8)],[f_72_8]) ).
fof(f_72_10,negated_conjecture,
( ? [U_178] :
( ? [U_177] :
( forename(sK4,U_177)
& jules_forename(sK4,U_177)
& of(sK4,U_177,U_178) )
& ? [U_169] :
( ? [U_168] :
( behind(sK4,U_168,U_168)
& be(sK4,U_169,U_178,U_168)
& wheel(sK4,U_168) )
& state(sK4,U_169) )
& man(sK4,U_178) )
& ? [U_171] :
( ? [U_170] :
( ! [U_167] :
( ( cheap(sK4,U_167)
& black(sK4,U_167)
& coat(sK4,U_167) )
| ~ member(sK4,U_167,U_170) )
& group(sK4,U_170)
& ! [U_166] :
( ! [U_165] :
( ? [U_164] :
( wear(sK4,U_164)
& nonreflexive(sK4,U_164)
& present(sK4,U_164)
& patient(sK4,U_164,U_166)
& agent(sK4,U_164,U_165)
& event(sK4,U_164) )
| ~ member(sK4,U_165,U_171) )
| ~ member(sK4,U_166,U_170) ) )
& ! [U_163] :
( ( young(sK4,U_163)
& fellow(sK4,U_163) )
| ~ member(sK4,U_163,U_171) )
& group(sK4,U_171)
& two(sK4,U_171)
& ! [U_162] :
( ? [U_161] :
( ? [U_160] :
( in(sK4,U_160,sK9)
& be(sK4,U_161,U_162,U_160) )
& state(sK4,U_161) )
| ~ member(sK4,U_162,U_171) ) )
& frontseat(sK4,sK9)
& in(sK4,sK8,sK7)
& down(sK4,sK8,sK7)
& barrel(sK4,sK8)
& present(sK4,sK8)
& agent(sK4,sK8,sK5)
& event(sK4,sK8)
& lonely(sK4,sK7)
& street(sK4,sK7)
& city(sK4,sK7)
& of(sK4,sK6,sK7)
& placename(sK4,sK6)
& hollywood_placename(sK4,sK6)
& old(sK4,sK5)
& dirty(sK4,sK5)
& white(sK4,sK5)
& chevy(sK4,sK5)
& actual_world(sK4) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_176,sK9)],[f_72_9]) ).
fof(f_72_11,negated_conjecture,
( ? [U_178] :
( ? [U_177] :
( forename(sK4,U_177)
& jules_forename(sK4,U_177)
& of(sK4,U_177,U_178) )
& ? [U_169] :
( ? [U_168] :
( behind(sK4,U_168,U_168)
& be(sK4,U_169,U_178,U_168)
& wheel(sK4,U_168) )
& state(sK4,U_169) )
& man(sK4,U_178) )
& ? [U_170] :
( ! [U_167] :
( ( cheap(sK4,U_167)
& black(sK4,U_167)
& coat(sK4,U_167) )
| ~ member(sK4,U_167,U_170) )
& group(sK4,U_170)
& ! [U_166] :
( ! [U_165] :
( ? [U_164] :
( wear(sK4,U_164)
& nonreflexive(sK4,U_164)
& present(sK4,U_164)
& patient(sK4,U_164,U_166)
& agent(sK4,U_164,U_165)
& event(sK4,U_164) )
| ~ member(sK4,U_165,sK10) )
| ~ member(sK4,U_166,U_170) ) )
& ! [U_163] :
( ( young(sK4,U_163)
& fellow(sK4,U_163) )
| ~ member(sK4,U_163,sK10) )
& group(sK4,sK10)
& two(sK4,sK10)
& ! [U_162] :
( ? [U_161] :
( ? [U_160] :
( in(sK4,U_160,sK9)
& be(sK4,U_161,U_162,U_160) )
& state(sK4,U_161) )
| ~ member(sK4,U_162,sK10) )
& frontseat(sK4,sK9)
& in(sK4,sK8,sK7)
& down(sK4,sK8,sK7)
& barrel(sK4,sK8)
& present(sK4,sK8)
& agent(sK4,sK8,sK5)
& event(sK4,sK8)
& lonely(sK4,sK7)
& street(sK4,sK7)
& city(sK4,sK7)
& of(sK4,sK6,sK7)
& placename(sK4,sK6)
& hollywood_placename(sK4,sK6)
& old(sK4,sK5)
& dirty(sK4,sK5)
& white(sK4,sK5)
& chevy(sK4,sK5)
& actual_world(sK4) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(U_171,sK10)],[f_72_10]) ).
fof(f_72_12,negated_conjecture,
( ? [U_178] :
( ? [U_177] :
( forename(sK4,U_177)
& jules_forename(sK4,U_177)
& of(sK4,U_177,U_178) )
& ? [U_169] :
( ? [U_168] :
( behind(sK4,U_168,U_168)
& be(sK4,U_169,U_178,U_168)
& wheel(sK4,U_168) )
& state(sK4,U_169) )
& man(sK4,U_178) )
& ? [U_170] :
( ! [U_167] :
( ( cheap(sK4,U_167)
& black(sK4,U_167)
& coat(sK4,U_167) )
| ~ member(sK4,U_167,U_170) )
& group(sK4,U_170)
& ! [U_166] :
( ! [U_165] :
( ? [U_164] :
( wear(sK4,U_164)
& nonreflexive(sK4,U_164)
& present(sK4,U_164)
& patient(sK4,U_164,U_166)
& agent(sK4,U_164,U_165)
& event(sK4,U_164) )
| ~ member(sK4,U_165,sK10) )
| ~ member(sK4,U_166,U_170) ) )
& ! [U_163] :
( ( young(sK4,U_163)
& fellow(sK4,U_163) )
| ~ member(sK4,U_163,sK10) )
& group(sK4,sK10)
& two(sK4,sK10)
& ! [U_162] :
( ( ? [U_160] :
( in(sK4,U_160,sK9)
& be(sK4,sK11(U_162),U_162,U_160) )
& state(sK4,sK11(U_162)) )
| ~ member(sK4,U_162,sK10) )
& frontseat(sK4,sK9)
& in(sK4,sK8,sK7)
& down(sK4,sK8,sK7)
& barrel(sK4,sK8)
& present(sK4,sK8)
& agent(sK4,sK8,sK5)
& event(sK4,sK8)
& lonely(sK4,sK7)
& street(sK4,sK7)
& city(sK4,sK7)
& of(sK4,sK6,sK7)
& placename(sK4,sK6)
& hollywood_placename(sK4,sK6)
& old(sK4,sK5)
& dirty(sK4,sK5)
& white(sK4,sK5)
& chevy(sK4,sK5)
& actual_world(sK4) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(U_161,sK11(U_162))],[f_72_11]) ).
fof(f_72_13,negated_conjecture,
( ? [U_178] :
( ? [U_177] :
( forename(sK4,U_177)
& jules_forename(sK4,U_177)
& of(sK4,U_177,U_178) )
& ? [U_169] :
( ? [U_168] :
( behind(sK4,U_168,U_168)
& be(sK4,U_169,U_178,U_168)
& wheel(sK4,U_168) )
& state(sK4,U_169) )
& man(sK4,U_178) )
& ? [U_170] :
( ! [U_167] :
( ( cheap(sK4,U_167)
& black(sK4,U_167)
& coat(sK4,U_167) )
| ~ member(sK4,U_167,U_170) )
& group(sK4,U_170)
& ! [U_166] :
( ! [U_165] :
( ? [U_164] :
( wear(sK4,U_164)
& nonreflexive(sK4,U_164)
& present(sK4,U_164)
& patient(sK4,U_164,U_166)
& agent(sK4,U_164,U_165)
& event(sK4,U_164) )
| ~ member(sK4,U_165,sK10) )
| ~ member(sK4,U_166,U_170) ) )
& ! [U_163] :
( ( young(sK4,U_163)
& fellow(sK4,U_163) )
| ~ member(sK4,U_163,sK10) )
& group(sK4,sK10)
& two(sK4,sK10)
& ! [U_162] :
( ( in(sK4,sK12(U_162),sK9)
& be(sK4,sK11(U_162),U_162,sK12(U_162))
& state(sK4,sK11(U_162)) )
| ~ member(sK4,U_162,sK10) )
& frontseat(sK4,sK9)
& in(sK4,sK8,sK7)
& down(sK4,sK8,sK7)
& barrel(sK4,sK8)
& present(sK4,sK8)
& agent(sK4,sK8,sK5)
& event(sK4,sK8)
& lonely(sK4,sK7)
& street(sK4,sK7)
& city(sK4,sK7)
& of(sK4,sK6,sK7)
& placename(sK4,sK6)
& hollywood_placename(sK4,sK6)
& old(sK4,sK5)
& dirty(sK4,sK5)
& white(sK4,sK5)
& chevy(sK4,sK5)
& actual_world(sK4) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(U_160,sK12(U_162))],[f_72_12]) ).
fof(f_72_14,negated_conjecture,
( ? [U_178] :
( ? [U_177] :
( forename(sK4,U_177)
& jules_forename(sK4,U_177)
& of(sK4,U_177,U_178) )
& ? [U_169] :
( ? [U_168] :
( behind(sK4,U_168,U_168)
& be(sK4,U_169,U_178,U_168)
& wheel(sK4,U_168) )
& state(sK4,U_169) )
& man(sK4,U_178) )
& ! [U_167] :
( ( cheap(sK4,U_167)
& black(sK4,U_167)
& coat(sK4,U_167) )
| ~ member(sK4,U_167,sK13) )
& group(sK4,sK13)
& ! [U_166] :
( ! [U_165] :
( ? [U_164] :
( wear(sK4,U_164)
& nonreflexive(sK4,U_164)
& present(sK4,U_164)
& patient(sK4,U_164,U_166)
& agent(sK4,U_164,U_165)
& event(sK4,U_164) )
| ~ member(sK4,U_165,sK10) )
| ~ member(sK4,U_166,sK13) )
& ! [U_163] :
( ( young(sK4,U_163)
& fellow(sK4,U_163) )
| ~ member(sK4,U_163,sK10) )
& group(sK4,sK10)
& two(sK4,sK10)
& ! [U_162] :
( ( in(sK4,sK12(U_162),sK9)
& be(sK4,sK11(U_162),U_162,sK12(U_162))
& state(sK4,sK11(U_162)) )
| ~ member(sK4,U_162,sK10) )
& frontseat(sK4,sK9)
& in(sK4,sK8,sK7)
& down(sK4,sK8,sK7)
& barrel(sK4,sK8)
& present(sK4,sK8)
& agent(sK4,sK8,sK5)
& event(sK4,sK8)
& lonely(sK4,sK7)
& street(sK4,sK7)
& city(sK4,sK7)
& of(sK4,sK6,sK7)
& placename(sK4,sK6)
& hollywood_placename(sK4,sK6)
& old(sK4,sK5)
& dirty(sK4,sK5)
& white(sK4,sK5)
& chevy(sK4,sK5)
& actual_world(sK4) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(U_170,sK13)],[f_72_13]) ).
fof(f_72_15,negated_conjecture,
( ? [U_178] :
( ? [U_177] :
( forename(sK4,U_177)
& jules_forename(sK4,U_177)
& of(sK4,U_177,U_178) )
& ? [U_169] :
( ? [U_168] :
( behind(sK4,U_168,U_168)
& be(sK4,U_169,U_178,U_168)
& wheel(sK4,U_168) )
& state(sK4,U_169) )
& man(sK4,U_178) )
& ! [U_167] :
( ( cheap(sK4,U_167)
& black(sK4,U_167)
& coat(sK4,U_167) )
| ~ member(sK4,U_167,sK13) )
& group(sK4,sK13)
& ! [U_166] :
( ! [U_165] :
( ( wear(sK4,sK14(U_166,U_165))
& nonreflexive(sK4,sK14(U_166,U_165))
& present(sK4,sK14(U_166,U_165))
& patient(sK4,sK14(U_166,U_165),U_166)
& agent(sK4,sK14(U_166,U_165),U_165)
& event(sK4,sK14(U_166,U_165)) )
| ~ member(sK4,U_165,sK10) )
| ~ member(sK4,U_166,sK13) )
& ! [U_163] :
( ( young(sK4,U_163)
& fellow(sK4,U_163) )
| ~ member(sK4,U_163,sK10) )
& group(sK4,sK10)
& two(sK4,sK10)
& ! [U_162] :
( ( in(sK4,sK12(U_162),sK9)
& be(sK4,sK11(U_162),U_162,sK12(U_162))
& state(sK4,sK11(U_162)) )
| ~ member(sK4,U_162,sK10) )
& frontseat(sK4,sK9)
& in(sK4,sK8,sK7)
& down(sK4,sK8,sK7)
& barrel(sK4,sK8)
& present(sK4,sK8)
& agent(sK4,sK8,sK5)
& event(sK4,sK8)
& lonely(sK4,sK7)
& street(sK4,sK7)
& city(sK4,sK7)
& of(sK4,sK6,sK7)
& placename(sK4,sK6)
& hollywood_placename(sK4,sK6)
& old(sK4,sK5)
& dirty(sK4,sK5)
& white(sK4,sK5)
& chevy(sK4,sK5)
& actual_world(sK4) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(U_164,sK14(U_166,U_165))],[f_72_14]) ).
fof(f_72_16,negated_conjecture,
( ? [U_177] :
( forename(sK4,U_177)
& jules_forename(sK4,U_177)
& of(sK4,U_177,sK15) )
& ? [U_169] :
( ? [U_168] :
( behind(sK4,U_168,U_168)
& be(sK4,U_169,sK15,U_168)
& wheel(sK4,U_168) )
& state(sK4,U_169) )
& man(sK4,sK15)
& ! [U_167] :
( ( cheap(sK4,U_167)
& black(sK4,U_167)
& coat(sK4,U_167) )
| ~ member(sK4,U_167,sK13) )
& group(sK4,sK13)
& ! [U_166] :
( ! [U_165] :
( ( wear(sK4,sK14(U_166,U_165))
& nonreflexive(sK4,sK14(U_166,U_165))
& present(sK4,sK14(U_166,U_165))
& patient(sK4,sK14(U_166,U_165),U_166)
& agent(sK4,sK14(U_166,U_165),U_165)
& event(sK4,sK14(U_166,U_165)) )
| ~ member(sK4,U_165,sK10) )
| ~ member(sK4,U_166,sK13) )
& ! [U_163] :
( ( young(sK4,U_163)
& fellow(sK4,U_163) )
| ~ member(sK4,U_163,sK10) )
& group(sK4,sK10)
& two(sK4,sK10)
& ! [U_162] :
( ( in(sK4,sK12(U_162),sK9)
& be(sK4,sK11(U_162),U_162,sK12(U_162))
& state(sK4,sK11(U_162)) )
| ~ member(sK4,U_162,sK10) )
& frontseat(sK4,sK9)
& in(sK4,sK8,sK7)
& down(sK4,sK8,sK7)
& barrel(sK4,sK8)
& present(sK4,sK8)
& agent(sK4,sK8,sK5)
& event(sK4,sK8)
& lonely(sK4,sK7)
& street(sK4,sK7)
& city(sK4,sK7)
& of(sK4,sK6,sK7)
& placename(sK4,sK6)
& hollywood_placename(sK4,sK6)
& old(sK4,sK5)
& dirty(sK4,sK5)
& white(sK4,sK5)
& chevy(sK4,sK5)
& actual_world(sK4) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(U_178,sK15)],[f_72_15]) ).
fof(f_72_17,negated_conjecture,
( ? [U_177] :
( forename(sK4,U_177)
& jules_forename(sK4,U_177)
& of(sK4,U_177,sK15) )
& ? [U_168] :
( behind(sK4,U_168,U_168)
& be(sK4,sK16,sK15,U_168)
& wheel(sK4,U_168) )
& state(sK4,sK16)
& man(sK4,sK15)
& ! [U_167] :
( ( cheap(sK4,U_167)
& black(sK4,U_167)
& coat(sK4,U_167) )
| ~ member(sK4,U_167,sK13) )
& group(sK4,sK13)
& ! [U_166] :
( ! [U_165] :
( ( wear(sK4,sK14(U_166,U_165))
& nonreflexive(sK4,sK14(U_166,U_165))
& present(sK4,sK14(U_166,U_165))
& patient(sK4,sK14(U_166,U_165),U_166)
& agent(sK4,sK14(U_166,U_165),U_165)
& event(sK4,sK14(U_166,U_165)) )
| ~ member(sK4,U_165,sK10) )
| ~ member(sK4,U_166,sK13) )
& ! [U_163] :
( ( young(sK4,U_163)
& fellow(sK4,U_163) )
| ~ member(sK4,U_163,sK10) )
& group(sK4,sK10)
& two(sK4,sK10)
& ! [U_162] :
( ( in(sK4,sK12(U_162),sK9)
& be(sK4,sK11(U_162),U_162,sK12(U_162))
& state(sK4,sK11(U_162)) )
| ~ member(sK4,U_162,sK10) )
& frontseat(sK4,sK9)
& in(sK4,sK8,sK7)
& down(sK4,sK8,sK7)
& barrel(sK4,sK8)
& present(sK4,sK8)
& agent(sK4,sK8,sK5)
& event(sK4,sK8)
& lonely(sK4,sK7)
& street(sK4,sK7)
& city(sK4,sK7)
& of(sK4,sK6,sK7)
& placename(sK4,sK6)
& hollywood_placename(sK4,sK6)
& old(sK4,sK5)
& dirty(sK4,sK5)
& white(sK4,sK5)
& chevy(sK4,sK5)
& actual_world(sK4) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(U_169,sK16)],[f_72_16]) ).
fof(f_72_18,negated_conjecture,
( ? [U_177] :
( forename(sK4,U_177)
& jules_forename(sK4,U_177)
& of(sK4,U_177,sK15) )
& behind(sK4,sK17,sK17)
& be(sK4,sK16,sK15,sK17)
& wheel(sK4,sK17)
& state(sK4,sK16)
& man(sK4,sK15)
& ! [U_167] :
( ( cheap(sK4,U_167)
& black(sK4,U_167)
& coat(sK4,U_167) )
| ~ member(sK4,U_167,sK13) )
& group(sK4,sK13)
& ! [U_166] :
( ! [U_165] :
( ( wear(sK4,sK14(U_166,U_165))
& nonreflexive(sK4,sK14(U_166,U_165))
& present(sK4,sK14(U_166,U_165))
& patient(sK4,sK14(U_166,U_165),U_166)
& agent(sK4,sK14(U_166,U_165),U_165)
& event(sK4,sK14(U_166,U_165)) )
| ~ member(sK4,U_165,sK10) )
| ~ member(sK4,U_166,sK13) )
& ! [U_163] :
( ( young(sK4,U_163)
& fellow(sK4,U_163) )
| ~ member(sK4,U_163,sK10) )
& group(sK4,sK10)
& two(sK4,sK10)
& ! [U_162] :
( ( in(sK4,sK12(U_162),sK9)
& be(sK4,sK11(U_162),U_162,sK12(U_162))
& state(sK4,sK11(U_162)) )
| ~ member(sK4,U_162,sK10) )
& frontseat(sK4,sK9)
& in(sK4,sK8,sK7)
& down(sK4,sK8,sK7)
& barrel(sK4,sK8)
& present(sK4,sK8)
& agent(sK4,sK8,sK5)
& event(sK4,sK8)
& lonely(sK4,sK7)
& street(sK4,sK7)
& city(sK4,sK7)
& of(sK4,sK6,sK7)
& placename(sK4,sK6)
& hollywood_placename(sK4,sK6)
& old(sK4,sK5)
& dirty(sK4,sK5)
& white(sK4,sK5)
& chevy(sK4,sK5)
& actual_world(sK4) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17]),skolemize(U_168,sK17)],[f_72_17]) ).
fof(f_72_19,negated_conjecture,
( forename(sK4,sK18)
& jules_forename(sK4,sK18)
& of(sK4,sK18,sK15)
& behind(sK4,sK17,sK17)
& be(sK4,sK16,sK15,sK17)
& wheel(sK4,sK17)
& state(sK4,sK16)
& man(sK4,sK15)
& ! [U_167] :
( ( cheap(sK4,U_167)
& black(sK4,U_167)
& coat(sK4,U_167) )
| ~ member(sK4,U_167,sK13) )
& group(sK4,sK13)
& ! [U_166] :
( ! [U_165] :
( ( wear(sK4,sK14(U_166,U_165))
& nonreflexive(sK4,sK14(U_166,U_165))
& present(sK4,sK14(U_166,U_165))
& patient(sK4,sK14(U_166,U_165),U_166)
& agent(sK4,sK14(U_166,U_165),U_165)
& event(sK4,sK14(U_166,U_165)) )
| ~ member(sK4,U_165,sK10) )
| ~ member(sK4,U_166,sK13) )
& ! [U_163] :
( ( young(sK4,U_163)
& fellow(sK4,U_163) )
| ~ member(sK4,U_163,sK10) )
& group(sK4,sK10)
& two(sK4,sK10)
& ! [U_162] :
( ( in(sK4,sK12(U_162),sK9)
& be(sK4,sK11(U_162),U_162,sK12(U_162))
& state(sK4,sK11(U_162)) )
| ~ member(sK4,U_162,sK10) )
& frontseat(sK4,sK9)
& in(sK4,sK8,sK7)
& down(sK4,sK8,sK7)
& barrel(sK4,sK8)
& present(sK4,sK8)
& agent(sK4,sK8,sK5)
& event(sK4,sK8)
& lonely(sK4,sK7)
& street(sK4,sK7)
& city(sK4,sK7)
& of(sK4,sK6,sK7)
& placename(sK4,sK6)
& hollywood_placename(sK4,sK6)
& old(sK4,sK5)
& dirty(sK4,sK5)
& white(sK4,sK5)
& chevy(sK4,sK5)
& actual_world(sK4) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(U_177,sK18)],[f_72_18]) ).
cnf(f_72_20,negated_conjecture,
actual_world(sK4),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_21,negated_conjecture,
chevy(sK4,sK5),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_22,negated_conjecture,
white(sK4,sK5),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_23,negated_conjecture,
dirty(sK4,sK5),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_24,negated_conjecture,
old(sK4,sK5),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_25,negated_conjecture,
hollywood_placename(sK4,sK6),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_26,negated_conjecture,
placename(sK4,sK6),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_27,negated_conjecture,
of(sK4,sK6,sK7),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_28,negated_conjecture,
city(sK4,sK7),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_29,negated_conjecture,
street(sK4,sK7),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_30,negated_conjecture,
lonely(sK4,sK7),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_31,negated_conjecture,
event(sK4,sK8),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_32,negated_conjecture,
agent(sK4,sK8,sK5),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_33,negated_conjecture,
present(sK4,sK8),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_34,negated_conjecture,
barrel(sK4,sK8),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_35,negated_conjecture,
down(sK4,sK8,sK7),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_36,negated_conjecture,
in(sK4,sK8,sK7),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_37,negated_conjecture,
frontseat(sK4,sK9),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_38,negated_conjecture,
( state(sK4,sK11(U_162))
| ~ member(sK4,U_162,sK10) ),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_39,negated_conjecture,
( be(sK4,sK11(U_162),U_162,sK12(U_162))
| ~ member(sK4,U_162,sK10) ),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_40,negated_conjecture,
( in(sK4,sK12(U_162),sK9)
| ~ member(sK4,U_162,sK10) ),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_41,negated_conjecture,
two(sK4,sK10),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_42,negated_conjecture,
group(sK4,sK10),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_43,negated_conjecture,
( fellow(sK4,U_163)
| ~ member(sK4,U_163,sK10) ),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_44,negated_conjecture,
( young(sK4,U_163)
| ~ member(sK4,U_163,sK10) ),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_45,negated_conjecture,
( event(sK4,sK14(U_166,U_165))
| ~ member(sK4,U_165,sK10)
| ~ member(sK4,U_166,sK13) ),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_46,negated_conjecture,
( agent(sK4,sK14(U_166,U_165),U_165)
| ~ member(sK4,U_165,sK10)
| ~ member(sK4,U_166,sK13) ),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_47,negated_conjecture,
( patient(sK4,sK14(U_166,U_165),U_166)
| ~ member(sK4,U_165,sK10)
| ~ member(sK4,U_166,sK13) ),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_48,negated_conjecture,
( present(sK4,sK14(U_166,U_165))
| ~ member(sK4,U_165,sK10)
| ~ member(sK4,U_166,sK13) ),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_49,negated_conjecture,
( nonreflexive(sK4,sK14(U_166,U_165))
| ~ member(sK4,U_165,sK10)
| ~ member(sK4,U_166,sK13) ),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_50,negated_conjecture,
( wear(sK4,sK14(U_166,U_165))
| ~ member(sK4,U_165,sK10)
| ~ member(sK4,U_166,sK13) ),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_51,negated_conjecture,
group(sK4,sK13),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_52,negated_conjecture,
( coat(sK4,U_167)
| ~ member(sK4,U_167,sK13) ),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_53,negated_conjecture,
( black(sK4,U_167)
| ~ member(sK4,U_167,sK13) ),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_54,negated_conjecture,
( cheap(sK4,U_167)
| ~ member(sK4,U_167,sK13) ),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_55,negated_conjecture,
man(sK4,sK15),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_56,negated_conjecture,
state(sK4,sK16),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_57,negated_conjecture,
wheel(sK4,sK17),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_58,negated_conjecture,
be(sK4,sK16,sK15,sK17),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_59,negated_conjecture,
behind(sK4,sK17,sK17),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_60,negated_conjecture,
of(sK4,sK18,sK15),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_61,negated_conjecture,
jules_forename(sK4,sK18),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(f_72_62,negated_conjecture,
forename(sK4,sK18),
inference(clausify,[status(thm)],[f_72_19]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( sK1(Eq_x_0,Eq_x_1) = sK1(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( sK2(Eq_x_0,Eq_x_1) = sK2(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( sK3(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = sK3(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( sK11(Eq_x_0) = sK11(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( sK12(Eq_x_0) = sK12(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_9,axiom,
( sK14(Eq_x_0,Eq_x_1) = sK14(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_10,axiom,
( jules_forename(Eq_y_0,Eq_y_1)
| ~ jules_forename(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_11,axiom,
( forename(Eq_y_0,Eq_y_1)
| ~ forename(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_12,axiom,
( relname(Eq_y_0,Eq_y_1)
| ~ relname(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_13,axiom,
( furniture(Eq_y_0,Eq_y_1)
| ~ furniture(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_14,axiom,
( instrumentality(Eq_y_0,Eq_y_1)
| ~ instrumentality(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_15,axiom,
( seat(Eq_y_0,Eq_y_1)
| ~ seat(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_16,axiom,
( frontseat(Eq_y_0,Eq_y_1)
| ~ frontseat(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_17,axiom,
( location(Eq_y_0,Eq_y_1)
| ~ location(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_18,axiom,
( object(Eq_y_0,Eq_y_1)
| ~ object(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_19,axiom,
( city(Eq_y_0,Eq_y_1)
| ~ city(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_20,axiom,
( hollywood_placename(Eq_y_0,Eq_y_1)
| ~ hollywood_placename(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_21,axiom,
( placename(Eq_y_0,Eq_y_1)
| ~ placename(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_22,axiom,
( abstraction(Eq_y_0,Eq_y_1)
| ~ abstraction(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_23,axiom,
( unisex(Eq_y_0,Eq_y_1)
| ~ unisex(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_24,axiom,
( general(Eq_y_0,Eq_y_1)
| ~ general(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_25,axiom,
( nonhuman(Eq_y_0,Eq_y_1)
| ~ nonhuman(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_26,axiom,
( thing(Eq_y_0,Eq_y_1)
| ~ thing(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_27,axiom,
( relation(Eq_y_0,Eq_y_1)
| ~ relation(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_28,axiom,
( transport(Eq_y_0,Eq_y_1)
| ~ transport(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_29,axiom,
( vehicle(Eq_y_0,Eq_y_1)
| ~ vehicle(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_30,axiom,
( car(Eq_y_0,Eq_y_1)
| ~ car(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_31,axiom,
( chevy(Eq_y_0,Eq_y_1)
| ~ chevy(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_32,axiom,
( way(Eq_y_0,Eq_y_1)
| ~ way(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_33,axiom,
( artifact(Eq_y_0,Eq_y_1)
| ~ artifact(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_34,axiom,
( street(Eq_y_0,Eq_y_1)
| ~ street(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_35,axiom,
( barrel(Eq_y_0,Eq_y_1)
| ~ barrel(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_36,axiom,
( event(Eq_y_0,Eq_y_1)
| ~ event(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_37,axiom,
( two(Eq_y_0,Eq_y_1)
| ~ two(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_38,axiom,
( group(Eq_y_0,Eq_y_1)
| ~ group(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_39,axiom,
( man(Eq_y_0,Eq_y_1)
| ~ man(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_40,axiom,
( male(Eq_y_0,Eq_y_1)
| ~ male(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_41,axiom,
( human_person(Eq_y_0,Eq_y_1)
| ~ human_person(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_42,axiom,
( animate(Eq_y_0,Eq_y_1)
| ~ animate(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_43,axiom,
( human(Eq_y_0,Eq_y_1)
| ~ human(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_44,axiom,
( organism(Eq_y_0,Eq_y_1)
| ~ organism(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_45,axiom,
( living(Eq_y_0,Eq_y_1)
| ~ living(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_46,axiom,
( impartial(Eq_y_0,Eq_y_1)
| ~ impartial(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_47,axiom,
( entity(Eq_y_0,Eq_y_1)
| ~ entity(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_48,axiom,
( fellow(Eq_y_0,Eq_y_1)
| ~ fellow(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_49,axiom,
( wear(Eq_y_0,Eq_y_1)
| ~ wear(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_50,axiom,
( set(Eq_y_0,Eq_y_1)
| ~ set(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_51,axiom,
( multiple(Eq_y_0,Eq_y_1)
| ~ multiple(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_52,axiom,
( clothes(Eq_y_0,Eq_y_1)
| ~ clothes(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_53,axiom,
( coat(Eq_y_0,Eq_y_1)
| ~ coat(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_54,axiom,
( nonliving(Eq_y_0,Eq_y_1)
| ~ nonliving(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_55,axiom,
( existent(Eq_y_0,Eq_y_1)
| ~ existent(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_56,axiom,
( specific(Eq_y_0,Eq_y_1)
| ~ specific(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_57,axiom,
( device(Eq_y_0,Eq_y_1)
| ~ device(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_58,axiom,
( wheel(Eq_y_0,Eq_y_1)
| ~ wheel(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_59,axiom,
( eventuality(Eq_y_0,Eq_y_1)
| ~ eventuality(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_60,axiom,
( state(Eq_y_0,Eq_y_1)
| ~ state(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_61,axiom,
( nonexistent(Eq_y_0,Eq_y_1)
| ~ nonexistent(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_62,axiom,
( singleton(Eq_y_0,Eq_y_1)
| ~ singleton(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_63,axiom,
( white(Eq_y_0,Eq_y_1)
| ~ white(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_64,axiom,
( black(Eq_y_0,Eq_y_1)
| ~ black(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_65,axiom,
( young(Eq_y_0,Eq_y_1)
| ~ young(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_66,axiom,
( old(Eq_y_0,Eq_y_1)
| ~ old(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_67,axiom,
( of(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ of(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_68,axiom,
( member(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ member(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_69,axiom,
( nonreflexive(Eq_y_0,Eq_y_1)
| ~ nonreflexive(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_70,axiom,
( agent(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ agent(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_71,axiom,
( patient(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ patient(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_72,axiom,
( be(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ be(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_73,axiom,
( actual_world(Eq_y_0)
| ~ actual_world(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_74,axiom,
( dirty(Eq_y_0,Eq_y_1)
| ~ dirty(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_75,axiom,
( lonely(Eq_y_0,Eq_y_1)
| ~ lonely(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_76,axiom,
( present(Eq_y_0,Eq_y_1)
| ~ present(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_77,axiom,
( down(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ down(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_78,axiom,
( in(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ in(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_79,axiom,
( cheap(Eq_y_0,Eq_y_1)
| ~ cheap(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_80,axiom,
( behind(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ behind(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP204+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.10/15.44 % CPULimit : 300
% 0.10/15.44 % WCLimit : 300
% 0.10/15.44 % DateTime : Sat Sep 19 17:21:21 UTC 2026
% 0.10/15.45 % CPUTime :
% 233.70/248.82 % SZS status Theorem for theBenchmark
% 233.70/248.82 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------