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