%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP125+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n014.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 : 300s
% DateTime : Thu May 9 17:34:14 EDT 2024
% Result : CounterSatisfiable 0.53s 0.74s
% Output : Saturation 0.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : NLP125+1 : TPTP v8.1.2. Released v2.4.0.
% 0.08/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n014.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Wed May 8 13:42:38 EDT 2024
% 0.15/0.36 % CPUTime :
% 0.53/0.74 % Version: 1.5
% 0.53/0.74 % SZS status CounterSatisfiable
% 0.53/0.74 % SZS output start Saturation
% 0.53/0.74 fof(co1,conjecture,(~(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(((((((((((((((of(U,V,W)&city(U,W))&hollywood_placename(U,V))&placename(U,V))&street(U,W))&lonely(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&event(U,Y))&agent(U,Y,X))&present(U,Y))&barrel(U,Y))&down(U,Y,W))&in(U,Y,W))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1)).
% 0.53/0.74 fof(c40,negated_conjecture,(~(~(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(((((((((((((((of(U,V,W)&city(U,W))&hollywood_placename(U,V))&placename(U,V))&street(U,W))&lonely(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&event(U,Y))&agent(U,Y,X))&present(U,Y))&barrel(U,Y))&down(U,Y,W))&in(U,Y,W)))))))))),inference(assume_negation,[status(cth)],[co1])).
% 0.53/0.74 fof(c41,negated_conjecture,(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(((((((((((((((of(U,V,W)&city(U,W))&hollywood_placename(U,V))&placename(U,V))&street(U,W))&lonely(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&event(U,Y))&agent(U,Y,X))&present(U,Y))&barrel(U,Y))&down(U,Y,W))&in(U,Y,W)))))))),inference(fof_nnf,[status(thm)],[c40])).
% 0.53/0.74 fof(c42,negated_conjecture,(?[X2]:(actual_world(X2)&(?[X3]:(?[X4]:(?[X5]:(?[X6]:(((((((((((((((of(X2,X3,X4)&city(X2,X4))&hollywood_placename(X2,X3))&placename(X2,X3))&street(X2,X4))&lonely(X2,X4))&chevy(X2,X5))&white(X2,X5))&dirty(X2,X5))&old(X2,X5))&event(X2,X6))&agent(X2,X6,X5))&present(X2,X6))&barrel(X2,X6))&down(X2,X6,X4))&in(X2,X6,X4)))))))),inference(variable_rename,[status(thm)],[c41])).
% 0.53/0.74 fof(c43,negated_conjecture,(actual_world(skolem0001)&(((((((((((((((of(skolem0001,skolem0002,skolem0003)&city(skolem0001,skolem0003))&hollywood_placename(skolem0001,skolem0002))&placename(skolem0001,skolem0002))&street(skolem0001,skolem0003))&lonely(skolem0001,skolem0003))&chevy(skolem0001,skolem0004))&white(skolem0001,skolem0004))&dirty(skolem0001,skolem0004))&old(skolem0001,skolem0004))&event(skolem0001,skolem0005))&agent(skolem0001,skolem0005,skolem0004))&present(skolem0001,skolem0005))&barrel(skolem0001,skolem0005))&down(skolem0001,skolem0005,skolem0003))&in(skolem0001,skolem0005,skolem0003))),inference(skolemize,[status(esa)],[c42])).
% 0.53/0.74 cnf(c45,negated_conjecture,of(skolem0001,skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c43])).
% 0.53/0.74 fof(ax35,axiom,(![U]:(![V]:(![W]:(((entity(U,V)&placename(U,W))&of(U,W,V))=>(~(?[X]:((placename(U,X)&X!=W)&of(U,X,V)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax35)).
% 0.53/0.74 fof(c61,plain,(![U]:(![V]:(![W]:(((~entity(U,V)|~placename(U,W))|~of(U,W,V))|(![X]:((~placename(U,X)|X=W)|~of(U,X,V))))))),inference(fof_nnf,[status(thm)],[ax35])).
% 0.53/0.74 fof(c63,plain,(![X7]:(![X8]:(![X9]:(![X10]:(((~entity(X7,X8)|~placename(X7,X9))|~of(X7,X9,X8))|((~placename(X7,X10)|X10=X9)|~of(X7,X10,X8))))))),inference(shift_quantors,[status(thm)],[fof(c62,plain,(![X7]:(![X8]:(![X9]:(((~entity(X7,X8)|~placename(X7,X9))|~of(X7,X9,X8))|(![X10]:((~placename(X7,X10)|X10=X9)|~of(X7,X10,X8))))))),inference(variable_rename,[status(thm)],[c61])).])).
% 0.53/0.74 cnf(c64,plain,~entity(X433,X435)|~placename(X433,X434)|~of(X433,X434,X435)|~placename(X433,X432)|X432=X434|~of(X433,X432,X435),inference(split_conjunct,[status(thm)],[c63])).
% 0.53/0.74 cnf(c347,plain,~entity(skolem0001,skolem0003)|~placename(skolem0001,X511)|~of(skolem0001,X511,skolem0003)|~placename(skolem0001,skolem0002)|skolem0002=X511,inference(resolution,[status(thm)],[c64, c45])).
% 0.53/0.74 cnf(reflexivity,axiom,X79=X79,theory(equality)).
% 0.53/0.74 cnf(c56,negated_conjecture,agent(skolem0001,skolem0005,skolem0004),inference(split_conjunct,[status(thm)],[c43])).
% 0.53/0.74 cnf(c35,axiom,X386!=X388|X387!=X389|X390!=X391|~agent(X386,X387,X390)|agent(X388,X389,X391),theory(equality)).
% 0.53/0.74 cnf(c325,plain,skolem0001!=X497|skolem0005!=X498|skolem0004!=X496|agent(X497,X498,X496),inference(resolution,[status(thm)],[c35, c56])).
% 0.53/0.74 cnf(c385,plain,skolem0001!=X508|skolem0005!=X509|agent(X508,X509,skolem0004),inference(resolution,[status(thm)],[c325, reflexivity])).
% 0.53/0.74 cnf(c390,plain,skolem0001!=X510|agent(X510,skolem0005,skolem0004),inference(resolution,[status(thm)],[c385, reflexivity])).
% 0.53/0.74 cnf(c59,negated_conjecture,down(skolem0001,skolem0005,skolem0003),inference(split_conjunct,[status(thm)],[c43])).
% 0.53/0.74 cnf(c33,axiom,X366!=X368|X367!=X369|X370!=X371|~down(X366,X367,X370)|down(X368,X369,X371),theory(equality)).
% 0.53/0.74 cnf(c316,plain,skolem0001!=X488|skolem0005!=X487|skolem0003!=X489|down(X488,X487,X489),inference(resolution,[status(thm)],[c33, c59])).
% 0.53/0.74 cnf(c380,plain,skolem0001!=X503|skolem0005!=X502|down(X503,X502,skolem0003),inference(resolution,[status(thm)],[c316, reflexivity])).
% 0.53/0.74 cnf(c388,plain,skolem0001!=X507|down(X507,skolem0005,skolem0003),inference(resolution,[status(thm)],[c380, reflexivity])).
% 0.53/0.74 cnf(c60,negated_conjecture,in(skolem0001,skolem0005,skolem0003),inference(split_conjunct,[status(thm)],[c43])).
% 0.53/0.74 cnf(c32,axiom,X355!=X357|X356!=X358|X359!=X360|~in(X355,X356,X359)|in(X357,X358,X360),theory(equality)).
% 0.53/0.74 cnf(c312,plain,skolem0001!=X480|skolem0005!=X482|skolem0003!=X481|in(X480,X482,X481),inference(resolution,[status(thm)],[c32, c60])).
% 0.53/0.74 cnf(c376,plain,skolem0001!=X499|skolem0005!=X500|in(X499,X500,skolem0003),inference(resolution,[status(thm)],[c312, reflexivity])).
% 0.53/0.74 cnf(c386,plain,skolem0001!=X501|in(X501,skolem0005,skolem0003),inference(resolution,[status(thm)],[c376, reflexivity])).
% 0.53/0.74 cnf(c30,axiom,X343!=X345|X344!=X346|X347!=X348|~of(X343,X344,X347)|of(X345,X346,X348),theory(equality)).
% 0.53/0.74 cnf(c307,plain,skolem0001!=X474|skolem0002!=X472|skolem0003!=X473|of(X474,X472,X473),inference(resolution,[status(thm)],[c30, c45])).
% 0.53/0.74 cnf(c372,plain,skolem0001!=X494|skolem0002!=X493|of(X494,X493,skolem0003),inference(resolution,[status(thm)],[c307, reflexivity])).
% 0.53/0.74 cnf(c383,plain,skolem0001!=X495|of(X495,skolem0002,skolem0003),inference(resolution,[status(thm)],[c372, reflexivity])).
% 0.53/0.74 cnf(c50,negated_conjecture,lonely(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c43])).
% 0.53/0.74 cnf(c39,axiom,X424!=X426|X425!=X427|~lonely(X424,X425)|lonely(X426,X427),theory(equality)).
% 0.53/0.74 cnf(c342,plain,skolem0001!=X490|skolem0003!=X491|lonely(X490,X491),inference(resolution,[status(thm)],[c39, c50])).
% 0.53/0.74 cnf(c381,plain,skolem0001!=X492|lonely(X492,skolem0003),inference(resolution,[status(thm)],[c342, reflexivity])).
% 0.53/0.74 cnf(c52,negated_conjecture,white(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c43])).
% 0.53/0.74 cnf(c38,axiom,X415!=X417|X416!=X418|~white(X415,X416)|white(X417,X418),theory(equality)).
% 0.53/0.74 cnf(c338,plain,skolem0001!=X485|skolem0004!=X484|white(X485,X484),inference(resolution,[status(thm)],[c38, c52])).
% 0.53/0.74 cnf(c378,plain,skolem0001!=X486|white(X486,skolem0004),inference(resolution,[status(thm)],[c338, reflexivity])).
% 0.53/0.74 cnf(c53,negated_conjecture,dirty(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c43])).
% 0.53/0.74 cnf(c37,axiom,X405!=X407|X406!=X408|~dirty(X405,X406)|dirty(X407,X408),theory(equality)).
% 0.53/0.74 cnf(c333,plain,skolem0001!=X479|skolem0004!=X478|dirty(X479,X478),inference(resolution,[status(thm)],[c37, c53])).
% 0.53/0.74 cnf(c375,plain,skolem0001!=X483|dirty(X483,skolem0004),inference(resolution,[status(thm)],[c333, reflexivity])).
% 0.53/0.74 cnf(c54,negated_conjecture,old(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c43])).
% 0.53/0.74 cnf(c36,axiom,X397!=X399|X398!=X400|~old(X397,X398)|old(X399,X400),theory(equality)).
% 0.53/0.74 cnf(c329,plain,skolem0001!=X476|skolem0004!=X475|old(X476,X475),inference(resolution,[status(thm)],[c36, c54])).
% 0.53/0.74 cnf(c373,plain,skolem0001!=X477|old(X477,skolem0004),inference(resolution,[status(thm)],[c329, reflexivity])).
% 0.53/0.74 cnf(c57,negated_conjecture,present(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c43])).
% 0.53/0.74 cnf(c34,axiom,X376!=X378|X377!=X379|~present(X376,X377)|present(X378,X379),theory(equality)).
% 0.53/0.74 cnf(c320,plain,skolem0001!=X469|skolem0005!=X470|present(X469,X470),inference(resolution,[status(thm)],[c34, c57])).
% 0.53/0.74 cnf(c370,plain,skolem0001!=X471|present(X471,skolem0005),inference(resolution,[status(thm)],[c320, reflexivity])).
% 0.53/0.74 cnf(c58,negated_conjecture,barrel(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c43])).
% 0.53/0.74 cnf(c29,axiom,X335!=X337|X336!=X338|~barrel(X335,X336)|barrel(X337,X338),theory(equality)).
% 0.53/0.74 cnf(c303,plain,skolem0001!=X467|skolem0005!=X466|barrel(X467,X466),inference(resolution,[status(thm)],[c29, c58])).
% 0.53/0.74 cnf(c368,plain,skolem0001!=X468|barrel(X468,skolem0005),inference(resolution,[status(thm)],[c303, reflexivity])).
% 0.53/0.74 cnf(c55,negated_conjecture,event(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c43])).
% 0.53/0.74 cnf(c28,axiom,X326!=X328|X327!=X329|~event(X326,X327)|event(X328,X329),theory(equality)).
% 0.53/0.74 cnf(c299,plain,skolem0001!=X464|skolem0005!=X463|event(X464,X463),inference(resolution,[status(thm)],[c28, c55])).
% 0.53/0.74 cnf(c366,plain,skolem0001!=X465|event(X465,skolem0005),inference(resolution,[status(thm)],[c299, reflexivity])).
% 0.53/0.74 fof(ax31,axiom,(![U]:(![V]:(event(U,V)=>eventuality(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax31)).
% 0.53/0.74 fof(c76,plain,(![U]:(![V]:(~event(U,V)|eventuality(U,V)))),inference(fof_nnf,[status(thm)],[ax31])).
% 0.53/0.74 fof(c77,plain,(![X17]:(![X18]:(~event(X17,X18)|eventuality(X17,X18)))),inference(variable_rename,[status(thm)],[c76])).
% 0.53/0.74 cnf(c78,plain,~event(X101,X100)|eventuality(X101,X100),inference(split_conjunct,[status(thm)],[c77])).
% 0.53/0.74 cnf(c173,plain,eventuality(skolem0001,skolem0005),inference(resolution,[status(thm)],[c78, c55])).
% 0.53/0.74 fof(ax30,axiom,(![U]:(![V]:(eventuality(U,V)=>thing(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax30)).
% 0.53/0.74 fof(c79,plain,(![U]:(![V]:(~eventuality(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax30])).
% 0.53/0.74 fof(c80,plain,(![X19]:(![X20]:(~eventuality(X19,X20)|thing(X19,X20)))),inference(variable_rename,[status(thm)],[c79])).
% 0.53/0.74 cnf(c81,plain,~eventuality(X107,X106)|thing(X107,X106),inference(split_conjunct,[status(thm)],[c80])).
% 0.53/0.74 cnf(c174,plain,thing(skolem0001,skolem0005),inference(resolution,[status(thm)],[c81, c173])).
% 0.53/0.74 fof(ax29,axiom,(![U]:(![V]:(thing(U,V)=>singleton(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax29)).
% 0.53/0.74 fof(c82,plain,(![U]:(![V]:(~thing(U,V)|singleton(U,V)))),inference(fof_nnf,[status(thm)],[ax29])).
% 0.53/0.74 fof(c83,plain,(![X21]:(![X22]:(~thing(X21,X22)|singleton(X21,X22)))),inference(variable_rename,[status(thm)],[c82])).
% 0.53/0.74 cnf(c84,plain,~thing(X109,X108)|singleton(X109,X108),inference(split_conjunct,[status(thm)],[c83])).
% 0.53/0.74 cnf(c175,plain,singleton(skolem0001,skolem0005),inference(resolution,[status(thm)],[c84, c174])).
% 0.53/0.74 cnf(c27,axiom,X316!=X318|X317!=X319|~singleton(X316,X317)|singleton(X318,X319),theory(equality)).
% 0.53/0.74 cnf(c294,plain,skolem0001!=X461|skolem0005!=X460|singleton(X461,X460),inference(resolution,[status(thm)],[c27, c175])).
% 0.53/0.74 cnf(c364,plain,skolem0001!=X462|singleton(X462,skolem0005),inference(resolution,[status(thm)],[c294, reflexivity])).
% 0.53/0.74 cnf(c49,negated_conjecture,street(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c43])).
% 0.53/0.74 fof(ax25,axiom,(![U]:(![V]:(street(U,V)=>way(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax25)).
% 0.53/0.74 fof(c94,plain,(![U]:(![V]:(~street(U,V)|way(U,V)))),inference(fof_nnf,[status(thm)],[ax25])).
% 0.53/0.74 fof(c95,plain,(![X29]:(![X30]:(~street(X29,X30)|way(X29,X30)))),inference(variable_rename,[status(thm)],[c94])).
% 0.53/0.74 cnf(c96,plain,~street(X124,X125)|way(X124,X125),inference(split_conjunct,[status(thm)],[c95])).
% 0.53/0.74 cnf(c180,plain,way(skolem0001,skolem0003),inference(resolution,[status(thm)],[c96, c49])).
% 0.53/0.74 fof(ax24,axiom,(![U]:(![V]:(way(U,V)=>artifact(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax24)).
% 0.53/0.74 fof(c97,plain,(![U]:(![V]:(~way(U,V)|artifact(U,V)))),inference(fof_nnf,[status(thm)],[ax24])).
% 0.53/0.74 fof(c98,plain,(![X31]:(![X32]:(~way(X31,X32)|artifact(X31,X32)))),inference(variable_rename,[status(thm)],[c97])).
% 0.53/0.74 cnf(c99,plain,~way(X126,X127)|artifact(X126,X127),inference(split_conjunct,[status(thm)],[c98])).
% 0.53/0.74 cnf(c181,plain,artifact(skolem0001,skolem0003),inference(resolution,[status(thm)],[c99, c180])).
% 0.53/0.74 fof(ax23,axiom,(![U]:(![V]:(artifact(U,V)=>object(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax23)).
% 0.53/0.74 fof(c100,plain,(![U]:(![V]:(~artifact(U,V)|object(U,V)))),inference(fof_nnf,[status(thm)],[ax23])).
% 0.53/0.74 fof(c101,plain,(![X33]:(![X34]:(~artifact(X33,X34)|object(X33,X34)))),inference(variable_rename,[status(thm)],[c100])).
% 0.53/0.74 cnf(c102,plain,~artifact(X133,X132)|object(X133,X132),inference(split_conjunct,[status(thm)],[c101])).
% 0.53/0.74 cnf(c184,plain,object(skolem0001,skolem0003),inference(resolution,[status(thm)],[c102, c181])).
% 0.53/0.74 fof(ax22,axiom,(![U]:(![V]:(object(U,V)=>entity(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax22)).
% 0.53/0.74 fof(c103,plain,(![U]:(![V]:(~object(U,V)|entity(U,V)))),inference(fof_nnf,[status(thm)],[ax22])).
% 0.53/0.74 fof(c104,plain,(![X35]:(![X36]:(~object(X35,X36)|entity(X35,X36)))),inference(variable_rename,[status(thm)],[c103])).
% 0.53/0.74 cnf(c105,plain,~object(X134,X135)|entity(X134,X135),inference(split_conjunct,[status(thm)],[c104])).
% 0.53/0.74 cnf(c185,plain,entity(skolem0001,skolem0003),inference(resolution,[status(thm)],[c105, c184])).
% 0.53/0.74 fof(ax21,axiom,(![U]:(![V]:(entity(U,V)=>thing(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax21)).
% 0.53/0.74 fof(c106,plain,(![U]:(![V]:(~entity(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax21])).
% 0.53/0.74 fof(c107,plain,(![X37]:(![X38]:(~entity(X37,X38)|thing(X37,X38)))),inference(variable_rename,[status(thm)],[c106])).
% 0.53/0.74 cnf(c108,plain,~entity(X136,X137)|thing(X136,X137),inference(split_conjunct,[status(thm)],[c107])).
% 0.53/0.74 cnf(c186,plain,thing(skolem0001,skolem0003),inference(resolution,[status(thm)],[c108, c185])).
% 0.53/0.74 cnf(c187,plain,singleton(skolem0001,skolem0003),inference(resolution,[status(thm)],[c186, c84])).
% 0.53/0.74 cnf(c293,plain,skolem0001!=X458|skolem0003!=X457|singleton(X458,X457),inference(resolution,[status(thm)],[c27, c187])).
% 0.53/0.74 cnf(c362,plain,skolem0001!=X459|singleton(X459,skolem0003),inference(resolution,[status(thm)],[c293, reflexivity])).
% 0.53/0.74 cnf(c51,negated_conjecture,chevy(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c43])).
% 0.53/0.74 fof(ax5,axiom,(![U]:(![V]:(chevy(U,V)=>car(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax5)).
% 0.53/0.74 fof(c154,plain,(![U]:(![V]:(~chevy(U,V)|car(U,V)))),inference(fof_nnf,[status(thm)],[ax5])).
% 0.53/0.74 fof(c155,plain,(![X69]:(![X70]:(~chevy(X69,X70)|car(X69,X70)))),inference(variable_rename,[status(thm)],[c154])).
% 0.53/0.74 cnf(c156,plain,~chevy(X197,X196)|car(X197,X196),inference(split_conjunct,[status(thm)],[c155])).
% 0.53/0.74 cnf(c214,plain,car(skolem0001,skolem0004),inference(resolution,[status(thm)],[c156, c51])).
% 0.53/0.74 fof(ax4,axiom,(![U]:(![V]:(car(U,V)=>vehicle(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax4)).
% 0.53/0.74 fof(c157,plain,(![U]:(![V]:(~car(U,V)|vehicle(U,V)))),inference(fof_nnf,[status(thm)],[ax4])).
% 0.53/0.74 fof(c158,plain,(![X71]:(![X72]:(~car(X71,X72)|vehicle(X71,X72)))),inference(variable_rename,[status(thm)],[c157])).
% 0.53/0.74 cnf(c159,plain,~car(X202,X203)|vehicle(X202,X203),inference(split_conjunct,[status(thm)],[c158])).
% 0.53/0.74 cnf(c217,plain,vehicle(skolem0001,skolem0004),inference(resolution,[status(thm)],[c159, c214])).
% 0.53/0.74 fof(ax3,axiom,(![U]:(![V]:(vehicle(U,V)=>transport(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax3)).
% 0.53/0.74 fof(c160,plain,(![U]:(![V]:(~vehicle(U,V)|transport(U,V)))),inference(fof_nnf,[status(thm)],[ax3])).
% 0.53/0.74 fof(c161,plain,(![X73]:(![X74]:(~vehicle(X73,X74)|transport(X73,X74)))),inference(variable_rename,[status(thm)],[c160])).
% 0.53/0.74 cnf(c162,plain,~vehicle(X205,X204)|transport(X205,X204),inference(split_conjunct,[status(thm)],[c161])).
% 0.53/0.74 cnf(c219,plain,transport(skolem0001,skolem0004),inference(resolution,[status(thm)],[c162, c217])).
% 0.53/0.74 fof(ax2,axiom,(![U]:(![V]:(transport(U,V)=>instrumentality(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax2)).
% 0.53/0.74 fof(c163,plain,(![U]:(![V]:(~transport(U,V)|instrumentality(U,V)))),inference(fof_nnf,[status(thm)],[ax2])).
% 0.53/0.74 fof(c164,plain,(![X75]:(![X76]:(~transport(X75,X76)|instrumentality(X75,X76)))),inference(variable_rename,[status(thm)],[c163])).
% 0.53/0.74 cnf(c165,plain,~transport(X211,X210)|instrumentality(X211,X210),inference(split_conjunct,[status(thm)],[c164])).
% 0.53/0.74 cnf(c222,plain,instrumentality(skolem0001,skolem0004),inference(resolution,[status(thm)],[c165, c219])).
% 0.53/0.74 fof(ax1,axiom,(![U]:(![V]:(instrumentality(U,V)=>artifact(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax1)).
% 0.53/0.74 fof(c166,plain,(![U]:(![V]:(~instrumentality(U,V)|artifact(U,V)))),inference(fof_nnf,[status(thm)],[ax1])).
% 0.53/0.74 fof(c167,plain,(![X77]:(![X78]:(~instrumentality(X77,X78)|artifact(X77,X78)))),inference(variable_rename,[status(thm)],[c166])).
% 0.53/0.75 cnf(c168,plain,~instrumentality(X213,X212)|artifact(X213,X212),inference(split_conjunct,[status(thm)],[c167])).
% 0.53/0.75 cnf(c224,plain,artifact(skolem0001,skolem0004),inference(resolution,[status(thm)],[c168, c222])).
% 0.53/0.75 cnf(c226,plain,object(skolem0001,skolem0004),inference(resolution,[status(thm)],[c224, c102])).
% 0.53/0.75 cnf(c227,plain,entity(skolem0001,skolem0004),inference(resolution,[status(thm)],[c226, c105])).
% 0.53/0.75 cnf(c235,plain,thing(skolem0001,skolem0004),inference(resolution,[status(thm)],[c227, c108])).
% 0.53/0.75 cnf(c239,plain,singleton(skolem0001,skolem0004),inference(resolution,[status(thm)],[c235, c84])).
% 0.53/0.75 cnf(c292,plain,skolem0001!=X455|skolem0004!=X454|singleton(X455,X454),inference(resolution,[status(thm)],[c27, c239])).
% 0.53/0.75 cnf(c360,plain,skolem0001!=X456|singleton(X456,skolem0004),inference(resolution,[status(thm)],[c292, reflexivity])).
% 0.53/0.75 cnf(c48,negated_conjecture,placename(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c43])).
% 0.53/0.75 fof(ax15,axiom,(![U]:(![V]:(placename(U,V)=>relname(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax15)).
% 0.53/0.75 fof(c124,plain,(![U]:(![V]:(~placename(U,V)|relname(U,V)))),inference(fof_nnf,[status(thm)],[ax15])).
% 0.53/0.75 fof(c125,plain,(![X49]:(![X50]:(~placename(X49,X50)|relname(X49,X50)))),inference(variable_rename,[status(thm)],[c124])).
% 0.53/0.75 cnf(c126,plain,~placename(X161,X160)|relname(X161,X160),inference(split_conjunct,[status(thm)],[c125])).
% 0.53/0.75 cnf(c195,plain,relname(skolem0001,skolem0002),inference(resolution,[status(thm)],[c126, c48])).
% 0.53/0.75 fof(ax14,axiom,(![U]:(![V]:(relname(U,V)=>relation(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax14)).
% 0.53/0.75 fof(c127,plain,(![U]:(![V]:(~relname(U,V)|relation(U,V)))),inference(fof_nnf,[status(thm)],[ax14])).
% 0.53/0.75 fof(c128,plain,(![X51]:(![X52]:(~relname(X51,X52)|relation(X51,X52)))),inference(variable_rename,[status(thm)],[c127])).
% 0.53/0.75 cnf(c129,plain,~relname(X162,X163)|relation(X162,X163),inference(split_conjunct,[status(thm)],[c128])).
% 0.53/0.75 cnf(c196,plain,relation(skolem0001,skolem0002),inference(resolution,[status(thm)],[c129, c195])).
% 0.53/0.75 fof(ax13,axiom,(![U]:(![V]:(relation(U,V)=>abstraction(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax13)).
% 0.53/0.75 fof(c130,plain,(![U]:(![V]:(~relation(U,V)|abstraction(U,V)))),inference(fof_nnf,[status(thm)],[ax13])).
% 0.53/0.75 fof(c131,plain,(![X53]:(![X54]:(~relation(X53,X54)|abstraction(X53,X54)))),inference(variable_rename,[status(thm)],[c130])).
% 0.53/0.75 cnf(c132,plain,~relation(X168,X169)|abstraction(X168,X169),inference(split_conjunct,[status(thm)],[c131])).
% 0.53/0.75 cnf(c198,plain,abstraction(skolem0001,skolem0002),inference(resolution,[status(thm)],[c132, c196])).
% 0.53/0.75 fof(ax12,axiom,(![U]:(![V]:(abstraction(U,V)=>thing(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax12)).
% 0.53/0.75 fof(c133,plain,(![U]:(![V]:(~abstraction(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax12])).
% 0.53/0.75 fof(c134,plain,(![X55]:(![X56]:(~abstraction(X55,X56)|thing(X55,X56)))),inference(variable_rename,[status(thm)],[c133])).
% 0.53/0.75 cnf(c135,plain,~abstraction(X171,X170)|thing(X171,X170),inference(split_conjunct,[status(thm)],[c134])).
% 0.53/0.75 cnf(c199,plain,thing(skolem0001,skolem0002),inference(resolution,[status(thm)],[c135, c198])).
% 0.53/0.75 cnf(c200,plain,singleton(skolem0001,skolem0002),inference(resolution,[status(thm)],[c199, c84])).
% 0.53/0.75 cnf(c291,plain,skolem0001!=X452|skolem0002!=X451|singleton(X452,X451),inference(resolution,[status(thm)],[c27, c200])).
% 0.53/0.75 cnf(c358,plain,skolem0001!=X453|singleton(X453,skolem0002),inference(resolution,[status(thm)],[c291, reflexivity])).
% 0.53/0.75 fof(ax27,axiom,(![U]:(![V]:(eventuality(U,V)=>nonexistent(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax27)).
% 0.53/0.75 fof(c88,plain,(![U]:(![V]:(~eventuality(U,V)|nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[ax27])).
% 0.53/0.75 fof(c89,plain,(![X25]:(![X26]:(~eventuality(X25,X26)|nonexistent(X25,X26)))),inference(variable_rename,[status(thm)],[c88])).
% 0.53/0.75 cnf(c90,plain,~eventuality(X117,X116)|nonexistent(X117,X116),inference(split_conjunct,[status(thm)],[c89])).
% 0.53/0.75 cnf(c177,plain,nonexistent(skolem0001,skolem0005),inference(resolution,[status(thm)],[c90, c173])).
% 0.53/0.75 cnf(c26,axiom,X308!=X310|X309!=X311|~nonexistent(X308,X309)|nonexistent(X310,X311),theory(equality)).
% 0.53/0.75 cnf(c287,plain,skolem0001!=X449|skolem0005!=X448|nonexistent(X449,X448),inference(resolution,[status(thm)],[c26, c177])).
% 0.53/0.75 cnf(c356,plain,skolem0001!=X450|nonexistent(X450,skolem0005),inference(resolution,[status(thm)],[c287, reflexivity])).
% 0.53/0.75 cnf(c25,axiom,X299!=X301|X300!=X302|~eventuality(X299,X300)|eventuality(X301,X302),theory(equality)).
% 0.53/0.75 cnf(c283,plain,skolem0001!=X446|skolem0005!=X445|eventuality(X446,X445),inference(resolution,[status(thm)],[c25, c173])).
% 0.53/0.75 cnf(c354,plain,skolem0001!=X447|eventuality(X447,skolem0005),inference(resolution,[status(thm)],[c283, reflexivity])).
% 0.53/0.75 cnf(c24,axiom,X289!=X291|X290!=X292|~street(X289,X290)|street(X291,X292),theory(equality)).
% 0.53/0.75 cnf(c278,plain,skolem0001!=X442|skolem0003!=X443|street(X442,X443),inference(resolution,[status(thm)],[c24, c49])).
% 0.53/0.75 cnf(c352,plain,skolem0001!=X444|street(X444,skolem0003),inference(resolution,[status(thm)],[c278, reflexivity])).
% 0.53/0.75 cnf(c23,axiom,X281!=X283|X282!=X284|~way(X281,X282)|way(X283,X284),theory(equality)).
% 0.53/0.75 cnf(c274,plain,skolem0001!=X440|skolem0003!=X439|way(X440,X439),inference(resolution,[status(thm)],[c23, c180])).
% 0.53/0.75 cnf(c350,plain,skolem0001!=X441|way(X441,skolem0003),inference(resolution,[status(thm)],[c274, reflexivity])).
% 0.53/0.75 fof(ax20,axiom,(![U]:(![V]:(entity(U,V)=>specific(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax20)).
% 0.53/0.75 fof(c109,plain,(![U]:(![V]:(~entity(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax20])).
% 0.53/0.75 fof(c110,plain,(![X39]:(![X40]:(~entity(X39,X40)|specific(X39,X40)))),inference(variable_rename,[status(thm)],[c109])).
% 0.53/0.75 cnf(c111,plain,~entity(X142,X143)|specific(X142,X143),inference(split_conjunct,[status(thm)],[c110])).
% 0.53/0.75 cnf(c236,plain,specific(skolem0001,skolem0004),inference(resolution,[status(thm)],[c227, c111])).
% 0.53/0.75 cnf(c22,axiom,X272!=X274|X273!=X275|~specific(X272,X273)|specific(X274,X275),theory(equality)).
% 0.53/0.75 cnf(c270,plain,skolem0001!=X437|skolem0004!=X436|specific(X437,X436),inference(resolution,[status(thm)],[c22, c236])).
% 0.53/0.75 cnf(c348,plain,skolem0001!=X438|specific(X438,skolem0004),inference(resolution,[status(thm)],[c270, reflexivity])).
% 0.53/0.75 cnf(c188,plain,specific(skolem0001,skolem0003),inference(resolution,[status(thm)],[c111, c185])).
% 0.53/0.75 cnf(c269,plain,skolem0001!=X430|skolem0003!=X429|specific(X430,X429),inference(resolution,[status(thm)],[c22, c188])).
% 0.53/0.75 cnf(c344,plain,skolem0001!=X431|specific(X431,skolem0003),inference(resolution,[status(thm)],[c269, reflexivity])).
% 0.53/0.75 fof(ax28,axiom,(![U]:(![V]:(eventuality(U,V)=>specific(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax28)).
% 0.53/0.75 fof(c85,plain,(![U]:(![V]:(~eventuality(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax28])).
% 0.53/0.75 fof(c86,plain,(![X23]:(![X24]:(~eventuality(X23,X24)|specific(X23,X24)))),inference(variable_rename,[status(thm)],[c85])).
% 0.53/0.75 cnf(c87,plain,~eventuality(X111,X110)|specific(X111,X110),inference(split_conjunct,[status(thm)],[c86])).
% 0.53/0.75 cnf(c176,plain,specific(skolem0001,skolem0005),inference(resolution,[status(thm)],[c87, c173])).
% 0.53/0.75 cnf(c268,plain,skolem0001!=X423|skolem0005!=X422|specific(X423,X422),inference(resolution,[status(thm)],[c22, c176])).
% 0.53/0.75 cnf(c341,plain,skolem0001!=X428|specific(X428,skolem0005),inference(resolution,[status(thm)],[c268, reflexivity])).
% 0.53/0.75 fof(ax19,axiom,(![U]:(![V]:(entity(U,V)=>existent(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax19)).
% 0.53/0.75 fof(c112,plain,(![U]:(![V]:(~entity(U,V)|existent(U,V)))),inference(fof_nnf,[status(thm)],[ax19])).
% 0.53/0.75 fof(c113,plain,(![X41]:(![X42]:(~entity(X41,X42)|existent(X41,X42)))),inference(variable_rename,[status(thm)],[c112])).
% 0.53/0.75 cnf(c114,plain,~entity(X144,X145)|existent(X144,X145),inference(split_conjunct,[status(thm)],[c113])).
% 0.53/0.75 cnf(c237,plain,existent(skolem0001,skolem0004),inference(resolution,[status(thm)],[c227, c114])).
% 0.53/0.75 cnf(c21,axiom,X262!=X264|X263!=X265|~existent(X262,X263)|existent(X264,X265),theory(equality)).
% 0.53/0.75 cnf(c263,plain,skolem0001!=X419|skolem0004!=X420|existent(X419,X420),inference(resolution,[status(thm)],[c21, c237])).
% 0.53/0.75 cnf(c339,plain,skolem0001!=X421|existent(X421,skolem0004),inference(resolution,[status(thm)],[c263, reflexivity])).
% 0.53/0.75 cnf(c189,plain,existent(skolem0001,skolem0003),inference(resolution,[status(thm)],[c114, c185])).
% 0.53/0.75 cnf(c262,plain,skolem0001!=X412|skolem0003!=X413|existent(X412,X413),inference(resolution,[status(thm)],[c21, c189])).
% 0.53/0.75 cnf(c336,plain,skolem0001!=X414|existent(X414,skolem0003),inference(resolution,[status(thm)],[c262, reflexivity])).
% 0.53/0.75 cnf(c20,axiom,X254!=X256|X255!=X257|~entity(X254,X255)|entity(X256,X257),theory(equality)).
% 0.53/0.75 cnf(c258,plain,skolem0001!=X410|skolem0004!=X409|entity(X410,X409),inference(resolution,[status(thm)],[c20, c227])).
% 0.53/0.75 cnf(c334,plain,skolem0001!=X411|entity(X411,skolem0004),inference(resolution,[status(thm)],[c258, reflexivity])).
% 0.53/0.75 cnf(c257,plain,skolem0001!=X403|skolem0003!=X402|entity(X403,X402),inference(resolution,[status(thm)],[c20, c185])).
% 0.53/0.75 cnf(c331,plain,skolem0001!=X404|entity(X404,skolem0003),inference(resolution,[status(thm)],[c257, reflexivity])).
% 0.53/0.75 fof(ax18,axiom,(![U]:(![V]:(object(U,V)=>nonliving(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax18)).
% 0.53/0.75 fof(c115,plain,(![U]:(![V]:(~object(U,V)|nonliving(U,V)))),inference(fof_nnf,[status(thm)],[ax18])).
% 0.53/0.75 fof(c116,plain,(![X43]:(![X44]:(~object(X43,X44)|nonliving(X43,X44)))),inference(variable_rename,[status(thm)],[c115])).
% 0.53/0.75 cnf(c117,plain,~object(X151,X150)|nonliving(X151,X150),inference(split_conjunct,[status(thm)],[c116])).
% 0.53/0.75 cnf(c191,plain,nonliving(skolem0001,skolem0003),inference(resolution,[status(thm)],[c117, c184])).
% 0.53/0.75 cnf(c19,axiom,X245!=X247|X246!=X248|~nonliving(X245,X246)|nonliving(X247,X248),theory(equality)).
% 0.53/0.75 cnf(c253,plain,skolem0001!=X395|skolem0003!=X396|nonliving(X395,X396),inference(resolution,[status(thm)],[c19, c191])).
% 0.53/0.75 cnf(c328,plain,skolem0001!=X401|nonliving(X401,skolem0003),inference(resolution,[status(thm)],[c253, reflexivity])).
% 0.53/0.75 cnf(c230,plain,nonliving(skolem0001,skolem0004),inference(resolution,[status(thm)],[c226, c117])).
% 0.53/0.75 cnf(c252,plain,skolem0001!=X392|skolem0004!=X393|nonliving(X392,X393),inference(resolution,[status(thm)],[c19, c230])).
% 0.53/0.75 cnf(c326,plain,skolem0001!=X394|nonliving(X394,skolem0004),inference(resolution,[status(thm)],[c252, reflexivity])).
% 0.53/0.75 fof(ax17,axiom,(![U]:(![V]:(object(U,V)=>impartial(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax17)).
% 0.53/0.75 fof(c118,plain,(![U]:(![V]:(~object(U,V)|impartial(U,V)))),inference(fof_nnf,[status(thm)],[ax17])).
% 0.53/0.75 fof(c119,plain,(![X45]:(![X46]:(~object(X45,X46)|impartial(X45,X46)))),inference(variable_rename,[status(thm)],[c118])).
% 0.53/0.75 cnf(c120,plain,~object(X152,X153)|impartial(X152,X153),inference(split_conjunct,[status(thm)],[c119])).
% 0.53/0.75 cnf(c192,plain,impartial(skolem0001,skolem0003),inference(resolution,[status(thm)],[c120, c184])).
% 0.53/0.75 cnf(c18,axiom,X235!=X237|X236!=X238|~impartial(X235,X236)|impartial(X237,X238),theory(equality)).
% 0.53/0.75 cnf(c247,plain,skolem0001!=X384|skolem0003!=X383|impartial(X384,X383),inference(resolution,[status(thm)],[c18, c192])).
% 0.53/0.75 cnf(c323,plain,skolem0001!=X385|impartial(X385,skolem0003),inference(resolution,[status(thm)],[c247, reflexivity])).
% 0.53/0.75 cnf(c228,plain,impartial(skolem0001,skolem0004),inference(resolution,[status(thm)],[c226, c120])).
% 0.53/0.75 cnf(c246,plain,skolem0001!=X381|skolem0004!=X380|impartial(X381,X380),inference(resolution,[status(thm)],[c18, c228])).
% 0.53/0.75 cnf(c321,plain,skolem0001!=X382|impartial(X382,skolem0004),inference(resolution,[status(thm)],[c246, reflexivity])).
% 0.53/0.75 cnf(c17,axiom,X225!=X227|X226!=X228|~relname(X225,X226)|relname(X227,X228),theory(equality)).
% 0.53/0.75 cnf(c242,plain,skolem0001!=X373|skolem0002!=X374|relname(X373,X374),inference(resolution,[status(thm)],[c17, c195])).
% 0.53/0.75 cnf(c318,plain,skolem0001!=X375|relname(X375,skolem0002),inference(resolution,[status(thm)],[c242, reflexivity])).
% 0.53/0.75 cnf(c16,axiom,X218!=X220|X219!=X221|~relation(X218,X219)|relation(X220,X221),theory(equality)).
% 0.53/0.75 cnf(c241,plain,skolem0001!=X364|skolem0002!=X365|relation(X364,X365),inference(resolution,[status(thm)],[c16, c196])).
% 0.53/0.75 cnf(c315,plain,skolem0001!=X372|relation(X372,skolem0002),inference(resolution,[status(thm)],[c241, reflexivity])).
% 0.53/0.75 cnf(c15,axiom,X214!=X216|X215!=X217|~thing(X214,X215)|thing(X216,X217),theory(equality)).
% 0.53/0.75 cnf(c240,plain,skolem0001!=X362|skolem0004!=X361|thing(X362,X361),inference(resolution,[status(thm)],[c235, c15])).
% 0.53/0.75 cnf(c313,plain,skolem0001!=X363|thing(X363,skolem0004),inference(resolution,[status(thm)],[c240, reflexivity])).
% 0.53/0.75 cnf(c12,axiom,X188!=X190|X189!=X191|~unisex(X188,X189)|unisex(X190,X191),theory(equality)).
% 0.53/0.75 fof(ax16,axiom,(![U]:(![V]:(object(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax16)).
% 0.53/0.75 fof(c121,plain,(![U]:(![V]:(~object(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax16])).
% 0.53/0.75 fof(c122,plain,(![X47]:(![X48]:(~object(X47,X48)|unisex(X47,X48)))),inference(variable_rename,[status(thm)],[c121])).
% 0.53/0.75 cnf(c123,plain,~object(X158,X159)|unisex(X158,X159),inference(split_conjunct,[status(thm)],[c122])).
% 0.53/0.75 cnf(c229,plain,unisex(skolem0001,skolem0004),inference(resolution,[status(thm)],[c226, c123])).
% 0.53/0.75 cnf(c238,plain,skolem0001!=X353|skolem0004!=X352|unisex(X353,X352),inference(resolution,[status(thm)],[c229, c12])).
% 0.53/0.75 cnf(c310,plain,skolem0001!=X354|unisex(X354,skolem0004),inference(resolution,[status(thm)],[c238, reflexivity])).
% 0.53/0.75 cnf(c234,plain,skolem0001!=X350|skolem0003!=X349|thing(X350,X349),inference(resolution,[status(thm)],[c15, c186])).
% 0.53/0.75 cnf(c308,plain,skolem0001!=X351|thing(X351,skolem0003),inference(resolution,[status(thm)],[c234, reflexivity])).
% 0.53/0.75 cnf(c233,plain,skolem0001!=X341|skolem0002!=X340|thing(X341,X340),inference(resolution,[status(thm)],[c15, c199])).
% 0.53/0.75 cnf(c305,plain,skolem0001!=X342|thing(X342,skolem0002),inference(resolution,[status(thm)],[c233, reflexivity])).
% 0.53/0.75 cnf(c232,plain,skolem0001!=X334|skolem0005!=X333|thing(X334,X333),inference(resolution,[status(thm)],[c15, c174])).
% 0.53/0.75 cnf(c302,plain,skolem0001!=X339|thing(X339,skolem0005),inference(resolution,[status(thm)],[c232, reflexivity])).
% 0.53/0.75 cnf(c7,axiom,X146!=X148|X147!=X149|~object(X146,X147)|object(X148,X149),theory(equality)).
% 0.53/0.75 cnf(c231,plain,skolem0001!=X330|skolem0004!=X331|object(X330,X331),inference(resolution,[status(thm)],[c226, c7])).
% 0.53/0.75 cnf(c300,plain,skolem0001!=X332|object(X332,skolem0004),inference(resolution,[status(thm)],[c231, reflexivity])).
% 0.53/0.75 cnf(c1,axiom,X92!=X94|X93!=X95|~artifact(X92,X93)|artifact(X94,X95),theory(equality)).
% 0.53/0.75 cnf(c225,plain,skolem0001!=X324|skolem0004!=X323|artifact(X324,X323),inference(resolution,[status(thm)],[c224, c1])).
% 0.53/0.75 cnf(c297,plain,skolem0001!=X325|artifact(X325,skolem0004),inference(resolution,[status(thm)],[c225, reflexivity])).
% 0.53/0.75 cnf(c0,axiom,X86!=X88|X87!=X89|~instrumentality(X86,X87)|instrumentality(X88,X89),theory(equality)).
% 0.53/0.75 cnf(c223,plain,skolem0001!=X321|skolem0004!=X320|instrumentality(X321,X320),inference(resolution,[status(thm)],[c222, c0])).
% 0.53/0.75 cnf(c295,plain,skolem0001!=X322|instrumentality(X322,skolem0004),inference(resolution,[status(thm)],[c223, reflexivity])).
% 0.53/0.75 fof(ax11,axiom,(![U]:(![V]:(abstraction(U,V)=>nonhuman(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax11)).
% 0.53/0.75 fof(c136,plain,(![U]:(![V]:(~abstraction(U,V)|nonhuman(U,V)))),inference(fof_nnf,[status(thm)],[ax11])).
% 0.53/0.75 fof(c137,plain,(![X57]:(![X58]:(~abstraction(X57,X58)|nonhuman(X57,X58)))),inference(variable_rename,[status(thm)],[c136])).
% 0.53/0.75 cnf(c138,plain,~abstraction(X176,X177)|nonhuman(X176,X177),inference(split_conjunct,[status(thm)],[c137])).
% 0.53/0.75 cnf(c202,plain,nonhuman(skolem0001,skolem0002),inference(resolution,[status(thm)],[c138, c198])).
% 0.53/0.75 cnf(c14,axiom,X206!=X208|X207!=X209|~nonhuman(X206,X207)|nonhuman(X208,X209),theory(equality)).
% 0.53/0.75 cnf(c221,plain,skolem0001!=X314|skolem0002!=X313|nonhuman(X314,X313),inference(resolution,[status(thm)],[c14, c202])).
% 0.53/0.75 cnf(c289,plain,skolem0001!=X315|nonhuman(X315,skolem0002),inference(resolution,[status(thm)],[c221, reflexivity])).
% 0.53/0.75 cnf(c2,axiom,X102!=X104|X103!=X105|~transport(X102,X103)|transport(X104,X105),theory(equality)).
% 0.53/0.75 cnf(c220,plain,skolem0001!=X306|skolem0004!=X307|transport(X306,X307),inference(resolution,[status(thm)],[c219, c2])).
% 0.53/0.75 cnf(c286,plain,skolem0001!=X312|transport(X312,skolem0004),inference(resolution,[status(thm)],[c220, reflexivity])).
% 0.53/0.75 cnf(c3,axiom,X112!=X114|X113!=X115|~vehicle(X112,X113)|vehicle(X114,X115),theory(equality)).
% 0.53/0.75 cnf(c218,plain,skolem0001!=X304|skolem0004!=X303|vehicle(X304,X303),inference(resolution,[status(thm)],[c217, c3])).
% 0.53/0.75 cnf(c284,plain,skolem0001!=X305|vehicle(X305,skolem0004),inference(resolution,[status(thm)],[c218, reflexivity])).
% 0.53/0.75 cnf(c4,axiom,X120!=X122|X121!=X123|~car(X120,X121)|car(X122,X123),theory(equality)).
% 0.53/0.75 cnf(c216,plain,skolem0001!=X297|skolem0004!=X296|car(X297,X296),inference(resolution,[status(thm)],[c214, c4])).
% 0.53/0.75 cnf(c281,plain,skolem0001!=X298|car(X298,skolem0004),inference(resolution,[status(thm)],[c216, reflexivity])).
% 0.53/0.75 fof(ax10,axiom,(![U]:(![V]:(abstraction(U,V)=>general(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax10)).
% 0.53/0.75 fof(c139,plain,(![U]:(![V]:(~abstraction(U,V)|general(U,V)))),inference(fof_nnf,[status(thm)],[ax10])).
% 0.53/0.75 fof(c140,plain,(![X59]:(![X60]:(~abstraction(X59,X60)|general(X59,X60)))),inference(variable_rename,[status(thm)],[c139])).
% 0.53/0.75 cnf(c141,plain,~abstraction(X179,X178)|general(X179,X178),inference(split_conjunct,[status(thm)],[c140])).
% 0.53/0.75 cnf(c203,plain,general(skolem0001,skolem0002),inference(resolution,[status(thm)],[c141, c198])).
% 0.53/0.75 cnf(c13,axiom,X198!=X200|X199!=X201|~general(X198,X199)|general(X200,X201),theory(equality)).
% 0.53/0.75 cnf(c215,plain,skolem0001!=X294|skolem0002!=X293|general(X294,X293),inference(resolution,[status(thm)],[c13, c203])).
% 0.53/0.75 cnf(c279,plain,skolem0001!=X295|general(X295,skolem0002),inference(resolution,[status(thm)],[c215, reflexivity])).
% 0.53/0.75 cnf(c6,axiom,X138!=X140|X139!=X141|~location(X138,X139)|location(X140,X141),theory(equality)).
% 0.53/0.75 cnf(c46,negated_conjecture,city(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c43])).
% 0.53/0.75 fof(ax7,axiom,(![U]:(![V]:(city(U,V)=>location(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax7)).
% 0.53/0.75 fof(c148,plain,(![U]:(![V]:(~city(U,V)|location(U,V)))),inference(fof_nnf,[status(thm)],[ax7])).
% 0.53/0.75 fof(c149,plain,(![X65]:(![X66]:(~city(X65,X66)|location(X65,X66)))),inference(variable_rename,[status(thm)],[c148])).
% 0.53/0.75 cnf(c150,plain,~city(X193,X192)|location(X193,X192),inference(split_conjunct,[status(thm)],[c149])).
% 0.53/0.75 cnf(c211,plain,location(skolem0001,skolem0003),inference(resolution,[status(thm)],[c150, c46])).
% 0.53/0.75 cnf(c212,plain,skolem0001!=X287|skolem0003!=X286|location(X287,X286),inference(resolution,[status(thm)],[c211, c6])).
% 0.53/0.75 cnf(c276,plain,skolem0001!=X288|location(X288,skolem0003),inference(resolution,[status(thm)],[c212, reflexivity])).
% 0.53/0.75 fof(ax9,axiom,(![U]:(![V]:(abstraction(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax9)).
% 0.53/0.75 fof(c142,plain,(![U]:(![V]:(~abstraction(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax9])).
% 0.53/0.75 fof(c143,plain,(![X61]:(![X62]:(~abstraction(X61,X62)|unisex(X61,X62)))),inference(variable_rename,[status(thm)],[c142])).
% 0.53/0.75 cnf(c144,plain,~abstraction(X185,X184)|unisex(X185,X184),inference(split_conjunct,[status(thm)],[c143])).
% 0.53/0.75 cnf(c206,plain,unisex(skolem0001,skolem0002),inference(resolution,[status(thm)],[c144, c198])).
% 0.53/0.75 cnf(c210,plain,skolem0001!=X280|skolem0002!=X279|unisex(X280,X279),inference(resolution,[status(thm)],[c12, c206])).
% 0.53/0.75 cnf(c273,plain,skolem0001!=X285|unisex(X285,skolem0002),inference(resolution,[status(thm)],[c210, reflexivity])).
% 0.53/0.75 cnf(c194,plain,unisex(skolem0001,skolem0003),inference(resolution,[status(thm)],[c123, c184])).
% 0.53/0.75 cnf(c209,plain,skolem0001!=X277|skolem0003!=X276|unisex(X277,X276),inference(resolution,[status(thm)],[c12, c194])).
% 0.53/0.75 cnf(c271,plain,skolem0001!=X278|unisex(X278,skolem0003),inference(resolution,[status(thm)],[c209, reflexivity])).
% 0.53/0.75 fof(ax26,axiom,(![U]:(![V]:(eventuality(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax26)).
% 0.53/0.75 fof(c91,plain,(![U]:(![V]:(~eventuality(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax26])).
% 0.53/0.75 fof(c92,plain,(![X27]:(![X28]:(~eventuality(X27,X28)|unisex(X27,X28)))),inference(variable_rename,[status(thm)],[c91])).
% 0.53/0.75 cnf(c93,plain,~eventuality(X119,X118)|unisex(X119,X118),inference(split_conjunct,[status(thm)],[c92])).
% 0.53/0.75 cnf(c179,plain,unisex(skolem0001,skolem0005),inference(resolution,[status(thm)],[c93, c173])).
% 0.53/0.75 cnf(c208,plain,skolem0001!=X270|skolem0005!=X269|unisex(X270,X269),inference(resolution,[status(thm)],[c12, c179])).
% 0.53/0.75 cnf(c266,plain,skolem0001!=X271|unisex(X271,skolem0005),inference(resolution,[status(thm)],[c208, reflexivity])).
% 0.53/0.75 cnf(c11,axiom,X180!=X182|X181!=X183|~abstraction(X180,X181)|abstraction(X182,X183),theory(equality)).
% 0.53/0.75 cnf(c205,plain,skolem0001!=X267|skolem0002!=X266|abstraction(X267,X266),inference(resolution,[status(thm)],[c11, c198])).
% 0.53/0.75 cnf(c264,plain,skolem0001!=X268|abstraction(X268,skolem0002),inference(resolution,[status(thm)],[c205, reflexivity])).
% 0.53/0.75 cnf(c10,axiom,X172!=X174|X173!=X175|~placename(X172,X173)|placename(X174,X175),theory(equality)).
% 0.53/0.75 cnf(c201,plain,skolem0001!=X260|skolem0002!=X259|placename(X260,X259),inference(resolution,[status(thm)],[c10, c48])).
% 0.53/0.75 cnf(c260,plain,skolem0001!=X261|placename(X261,skolem0002),inference(resolution,[status(thm)],[c201, reflexivity])).
% 0.53/0.75 cnf(c47,negated_conjecture,hollywood_placename(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c43])).
% 0.53/0.75 cnf(c9,axiom,X164!=X166|X165!=X167|~hollywood_placename(X164,X165)|hollywood_placename(X166,X167),theory(equality)).
% 0.53/0.75 cnf(c197,plain,skolem0001!=X253|skolem0002!=X252|hollywood_placename(X253,X252),inference(resolution,[status(thm)],[c9, c47])).
% 0.53/0.75 cnf(c256,plain,skolem0001!=X258|hollywood_placename(X258,skolem0002),inference(resolution,[status(thm)],[c197, reflexivity])).
% 0.53/0.75 cnf(c8,axiom,X154!=X156|X155!=X157|~city(X154,X155)|city(X156,X157),theory(equality)).
% 0.53/0.75 cnf(c193,plain,skolem0001!=X250|skolem0003!=X249|city(X250,X249),inference(resolution,[status(thm)],[c8, c46])).
% 0.53/0.75 cnf(c254,plain,skolem0001!=X251|city(X251,skolem0003),inference(resolution,[status(thm)],[c193, reflexivity])).
% 0.53/0.75 cnf(c190,plain,skolem0001!=X242|skolem0003!=X243|object(X242,X243),inference(resolution,[status(thm)],[c7, c184])).
% 0.53/0.75 cnf(c250,plain,skolem0001!=X244|object(X244,skolem0003),inference(resolution,[status(thm)],[c190, reflexivity])).
% 0.53/0.75 cnf(c5,axiom,X128!=X130|X129!=X131|~chevy(X128,X129)|chevy(X130,X131),theory(equality)).
% 0.53/0.75 cnf(c183,plain,skolem0001!=X240|skolem0004!=X239|chevy(X240,X239),inference(resolution,[status(thm)],[c5, c51])).
% 0.53/0.75 cnf(c248,plain,skolem0001!=X241|chevy(X241,skolem0004),inference(resolution,[status(thm)],[c183, reflexivity])).
% 0.53/0.75 cnf(c182,plain,skolem0001!=X233|skolem0003!=X232|artifact(X233,X232),inference(resolution,[status(thm)],[c181, c1])).
% 0.53/0.75 cnf(c244,plain,skolem0001!=X234|artifact(X234,skolem0003),inference(resolution,[status(thm)],[c182, reflexivity])).
% 0.53/0.75 cnf(c31,axiom,X229!=X230|~actual_world(X229)|actual_world(X230),theory(equality)).
% 0.53/0.75 fof(ax6,axiom,(![U]:(![V]:(location(U,V)=>object(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax6)).
% 0.53/0.75 fof(c151,plain,(![U]:(![V]:(~location(U,V)|object(U,V)))),inference(fof_nnf,[status(thm)],[ax6])).
% 0.53/0.75 fof(c152,plain,(![X67]:(![X68]:(~location(X67,X68)|object(X67,X68)))),inference(variable_rename,[status(thm)],[c151])).
% 0.53/0.75 cnf(c153,plain,~location(X194,X195)|object(X194,X195),inference(split_conjunct,[status(thm)],[c152])).
% 0.53/0.75 fof(ax8,axiom,(![U]:(![V]:(hollywood_placename(U,V)=>placename(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax8)).
% 0.53/0.75 fof(c145,plain,(![U]:(![V]:(~hollywood_placename(U,V)|placename(U,V)))),inference(fof_nnf,[status(thm)],[ax8])).
% 0.53/0.75 fof(c146,plain,(![X63]:(![X64]:(~hollywood_placename(X63,X64)|placename(X63,X64)))),inference(variable_rename,[status(thm)],[c145])).
% 0.53/0.75 cnf(c147,plain,~hollywood_placename(X186,X187)|placename(X186,X187),inference(split_conjunct,[status(thm)],[c146])).
% 0.53/0.75 fof(ax34,axiom,(![U]:(![V]:(specific(U,V)=>(~general(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax34)).
% 0.53/0.75 fof(c65,plain,(![U]:(![V]:(specific(U,V)=>~general(U,V)))),inference(fof_simplification,[status(thm)],[ax34])).
% 0.53/0.75 fof(c66,plain,(![U]:(![V]:(~specific(U,V)|~general(U,V)))),inference(fof_nnf,[status(thm)],[c65])).
% 0.53/0.75 fof(c67,plain,(![X11]:(![X12]:(~specific(X11,X12)|~general(X11,X12)))),inference(variable_rename,[status(thm)],[c66])).
% 0.53/0.75 cnf(c68,plain,~specific(X91,X90)|~general(X91,X90),inference(split_conjunct,[status(thm)],[c67])).
% 0.53/0.75 cnf(c204,plain,~specific(skolem0001,skolem0002),inference(resolution,[status(thm)],[c203, c68])).
% 0.53/0.75 fof(ax33,axiom,(![U]:(![V]:(existent(U,V)=>(~nonexistent(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax33)).
% 0.53/0.75 fof(c69,plain,(![U]:(![V]:(existent(U,V)=>~nonexistent(U,V)))),inference(fof_simplification,[status(thm)],[ax33])).
% 0.53/0.75 fof(c70,plain,(![U]:(![V]:(~existent(U,V)|~nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[c69])).
% 0.53/0.75 fof(c71,plain,(![X13]:(![X14]:(~existent(X13,X14)|~nonexistent(X13,X14)))),inference(variable_rename,[status(thm)],[c70])).
% 0.53/0.75 cnf(c72,plain,~existent(X96,X97)|~nonexistent(X96,X97),inference(split_conjunct,[status(thm)],[c71])).
% 0.53/0.75 cnf(c178,plain,~existent(skolem0001,skolem0005),inference(resolution,[status(thm)],[c177, c72])).
% 0.53/0.75 fof(ax32,axiom,(![U]:(![V]:(barrel(U,V)=>event(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax32)).
% 0.53/0.75 fof(c73,plain,(![U]:(![V]:(~barrel(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax32])).
% 0.53/0.75 fof(c74,plain,(![X15]:(![X16]:(~barrel(X15,X16)|event(X15,X16)))),inference(variable_rename,[status(thm)],[c73])).
% 0.53/0.75 cnf(c75,plain,~barrel(X98,X99)|event(X98,X99),inference(split_conjunct,[status(thm)],[c74])).
% 0.53/0.75 cnf(transitivity,axiom,X83!=X85|X85!=X84|X83=X84,theory(equality)).
% 0.53/0.75 cnf(symmetry,axiom,X80!=X81|X81=X80,theory(equality)).
% 0.53/0.75 cnf(c44,negated_conjecture,actual_world(skolem0001),inference(split_conjunct,[status(thm)],[c43])).
% 0.53/0.75 % SZS output end Saturation
% 0.53/0.75
% 0.53/0.75 % Initial clauses : 95
% 0.53/0.75 % Processed clauses : 254
% 0.53/0.75 % Factors computed : 2
% 0.53/0.75 % Resolvents computed: 222
% 0.53/0.75 % Tautologies deleted: 3
% 0.53/0.75 % Forward subsumed : 62
% 0.53/0.75 % Backward subsumed : 0
% 0.53/0.75 % -------- CPU Time ---------
% 0.53/0.75 % User time : 0.366 s
% 0.53/0.75 % System time : 0.018 s
% 0.53/0.75 % Total time : 0.384 s
%------------------------------------------------------------------------------