%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP003+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n023.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:33:31 EDT 2024
% Result : CounterSatisfiable 0.45s 0.63s
% Output : Saturation 0.45s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NLP003+1 : TPTP v8.1.2. Released v2.4.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n023.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 13:43:38 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.45/0.63 % Version: 1.5
% 0.45/0.63 % SZS status CounterSatisfiable
% 0.45/0.63 % SZS output start Saturation
% 0.45/0.63 cnf(reflexivity,axiom,X53=X53,theory(equality)).
% 0.45/0.63 fof(co1,conjecture,(~(?[U]:(?[V]:(?[W]:(?[X]:(((((((((((((hollywood(U)&city(U))&event(V))&chevy(W))&car(W))&white(W))&dirty(W))&old(W))&street(X))&way(X))&lonely(X))&barrel(V,W))&down(V,X))&in(V,U))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', co1)).
% 0.45/0.63 fof(c36,negated_conjecture,(~(~(?[U]:(?[V]:(?[W]:(?[X]:(((((((((((((hollywood(U)&city(U))&event(V))&chevy(W))&car(W))&white(W))&dirty(W))&old(W))&street(X))&way(X))&lonely(X))&barrel(V,W))&down(V,X))&in(V,U)))))))),inference(assume_negation,[status(cth)],[co1])).
% 0.45/0.63 fof(c37,negated_conjecture,(?[U]:(?[V]:(?[W]:(?[X]:(((((((((((((hollywood(U)&city(U))&event(V))&chevy(W))&car(W))&white(W))&dirty(W))&old(W))&street(X))&way(X))&lonely(X))&barrel(V,W))&down(V,X))&in(V,U)))))),inference(fof_nnf,[status(thm)],[c36])).
% 0.45/0.63 fof(c38,negated_conjecture,(?[U]:(?[V]:((?[W]:(?[X]:((((((((((((hollywood(U)&city(U))&event(V))&chevy(W))&car(W))&white(W))&dirty(W))&old(W))&street(X))&way(X))&lonely(X))&barrel(V,W))&down(V,X))))&in(V,U)))),inference(shift_quantors,[status(thm)],[c37])).
% 0.45/0.63 fof(c39,negated_conjecture,(?[X2]:(?[X3]:((?[X4]:(?[X5]:((((((((((((hollywood(X2)&city(X2))&event(X3))&chevy(X4))&car(X4))&white(X4))&dirty(X4))&old(X4))&street(X5))&way(X5))&lonely(X5))&barrel(X3,X4))&down(X3,X5))))&in(X3,X2)))),inference(variable_rename,[status(thm)],[c38])).
% 0.45/0.63 fof(c40,negated_conjecture,(((((((((((((hollywood(skolem0001)&city(skolem0001))&event(skolem0002))&chevy(skolem0003))&car(skolem0003))&white(skolem0003))&dirty(skolem0003))&old(skolem0003))&street(skolem0004))&way(skolem0004))&lonely(skolem0004))&barrel(skolem0002,skolem0003))&down(skolem0002,skolem0004))&in(skolem0002,skolem0001)),inference(skolemize,[status(esa)],[c39])).
% 0.45/0.63 cnf(c52,negated_conjecture,barrel(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c40])).
% 0.45/0.63 cnf(c32,axiom,X239!=X238|X237!=X236|~barrel(X239,X237)|barrel(X238,X236),theory(equality)).
% 0.45/0.63 cnf(c240,plain,skolem0002!=X241|skolem0003!=X240|barrel(X241,X240),inference(resolution,[status(thm)],[c32, c52])).
% 0.45/0.63 cnf(c241,plain,skolem0002!=X242|barrel(X242,skolem0003),inference(resolution,[status(thm)],[c240, reflexivity])).
% 0.45/0.63 fof(ax30,axiom,(![U]:(![V]:(![W]:(((have(U,V,W)&nonhuman(V))&nonhuman(W))=>partof(W,V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax30)).
% 0.45/0.63 fof(c67,plain,(![U]:(![V]:(![W]:(((~have(U,V,W)|~nonhuman(V))|~nonhuman(W))|partof(W,V))))),inference(fof_nnf,[status(thm)],[ax30])).
% 0.45/0.63 fof(c68,plain,(![X15]:(![X16]:(![X17]:(((~have(X15,X16,X17)|~nonhuman(X16))|~nonhuman(X17))|partof(X17,X16))))),inference(variable_rename,[status(thm)],[c67])).
% 0.45/0.63 cnf(c69,plain,~have(X234,X233,X235)|~nonhuman(X233)|~nonhuman(X235)|partof(X235,X233),inference(split_conjunct,[status(thm)],[c68])).
% 0.45/0.63 cnf(c53,negated_conjecture,down(skolem0002,skolem0004),inference(split_conjunct,[status(thm)],[c40])).
% 0.45/0.63 cnf(c31,axiom,X229!=X228|X227!=X226|~down(X229,X227)|down(X228,X226),theory(equality)).
% 0.45/0.63 cnf(c237,plain,skolem0002!=X230|skolem0004!=X231|down(X230,X231),inference(resolution,[status(thm)],[c31, c53])).
% 0.45/0.63 cnf(c238,plain,skolem0002!=X232|down(X232,skolem0004),inference(resolution,[status(thm)],[c237, reflexivity])).
% 0.45/0.63 cnf(c54,negated_conjecture,in(skolem0002,skolem0001),inference(split_conjunct,[status(thm)],[c40])).
% 0.45/0.63 cnf(c30,axiom,X213!=X212|X211!=X210|~in(X213,X211)|in(X212,X210),theory(equality)).
% 0.45/0.63 cnf(c234,plain,skolem0002!=X224|skolem0001!=X223|in(X224,X223),inference(resolution,[status(thm)],[c30, c54])).
% 0.45/0.63 cnf(c235,plain,skolem0002!=X225|in(X225,skolem0001),inference(resolution,[status(thm)],[c234, reflexivity])).
% 0.45/0.63 fof(ax29,axiom,(![U]:(![V]:(![W]:((have(U,V,W)&human(V))<=>(owner(V)&of(V,W)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax29)).
% 0.45/0.63 fof(c70,plain,(![U]:(![V]:(![W]:(((~have(U,V,W)|~human(V))|(owner(V)&of(V,W)))&((~owner(V)|~of(V,W))|(have(U,V,W)&human(V))))))),inference(fof_nnf,[status(thm)],[ax29])).
% 0.45/0.63 fof(c71,plain,((![U]:(![V]:(![W]:((~have(U,V,W)|~human(V))|(owner(V)&of(V,W))))))&(![U]:(![V]:(![W]:((~owner(V)|~of(V,W))|(have(U,V,W)&human(V))))))),inference(shift_quantors,[status(thm)],[c70])).
% 0.45/0.63 fof(c73,plain,(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(((~have(X18,X19,X20)|~human(X19))|(owner(X19)&of(X19,X20)))&((~owner(X22)|~of(X22,X23))|(have(X21,X22,X23)&human(X22)))))))))),inference(shift_quantors,[status(thm)],[fof(c72,plain,((![X18]:(![X19]:(![X20]:((~have(X18,X19,X20)|~human(X19))|(owner(X19)&of(X19,X20))))))&(![X21]:(![X22]:(![X23]:((~owner(X22)|~of(X22,X23))|(have(X21,X22,X23)&human(X22))))))),inference(variable_rename,[status(thm)],[c71])).])).
% 0.45/0.63 fof(c74,plain,(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:((((~have(X18,X19,X20)|~human(X19))|owner(X19))&((~have(X18,X19,X20)|~human(X19))|of(X19,X20)))&(((~owner(X22)|~of(X22,X23))|have(X21,X22,X23))&((~owner(X22)|~of(X22,X23))|human(X22)))))))))),inference(distribute,[status(thm)],[c73])).
% 0.45/0.63 cnf(c77,plain,~owner(X221)|~of(X221,X222)|have(X220,X221,X222),inference(split_conjunct,[status(thm)],[c74])).
% 0.45/0.63 cnf(c76,plain,~have(X219,X218,X217)|~human(X218)|of(X218,X217),inference(split_conjunct,[status(thm)],[c74])).
% 0.45/0.63 fof(ax31,axiom,(![U]:(![V]:(![W]:((event(U)&have(U,V,W))=>of(V,W))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax31)).
% 0.45/0.63 fof(c64,plain,(![U]:(![V]:(![W]:((~event(U)|~have(U,V,W))|of(V,W))))),inference(fof_nnf,[status(thm)],[ax31])).
% 0.45/0.63 fof(c65,plain,(![X12]:(![X13]:(![X14]:((~event(X12)|~have(X12,X13,X14))|of(X13,X14))))),inference(variable_rename,[status(thm)],[c64])).
% 0.45/0.63 cnf(c66,plain,~event(X214)|~have(X214,X215,X216)|of(X215,X216),inference(split_conjunct,[status(thm)],[c65])).
% 0.45/0.63 fof(ax32,axiom,(![U]:(![V]:(of(V,U)=>(?[W]:(event(W)&have(W,U,V)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax32)).
% 0.45/0.63 fof(c58,plain,(![U]:(![V]:(~of(V,U)|(?[W]:(event(W)&have(W,U,V)))))),inference(fof_nnf,[status(thm)],[ax32])).
% 0.45/0.63 fof(c59,plain,(![X9]:(![X10]:(~of(X10,X9)|(?[X11]:(event(X11)&have(X11,X9,X10)))))),inference(variable_rename,[status(thm)],[c58])).
% 0.45/0.63 fof(c60,plain,(![X9]:(![X10]:(~of(X10,X9)|(event(skolem0005(X9,X10))&have(skolem0005(X9,X10),X9,X10))))),inference(skolemize,[status(esa)],[c59])).
% 0.45/0.63 fof(c61,plain,(![X9]:(![X10]:((~of(X10,X9)|event(skolem0005(X9,X10)))&(~of(X10,X9)|have(skolem0005(X9,X10),X9,X10))))),inference(distribute,[status(thm)],[c60])).
% 0.45/0.63 cnf(c63,plain,~of(X208,X209)|have(skolem0005(X209,X208),X209,X208),inference(split_conjunct,[status(thm)],[c61])).
% 0.45/0.63 fof(ax33,axiom,(![U]:(![V]:(![W]:((partof(U,V)&partof(U,W))=>V=W)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax33)).
% 0.45/0.63 fof(c55,plain,(![U]:(![V]:(![W]:((~partof(U,V)|~partof(U,W))|V=W)))),inference(fof_nnf,[status(thm)],[ax33])).
% 0.45/0.63 fof(c56,plain,(![X6]:(![X7]:(![X8]:((~partof(X6,X7)|~partof(X6,X8))|X7=X8)))),inference(variable_rename,[status(thm)],[c55])).
% 0.45/0.63 cnf(c57,plain,~partof(X203,X204)|~partof(X203,X205)|X204=X205,inference(split_conjunct,[status(thm)],[c56])).
% 0.45/0.63 cnf(c75,plain,~have(X202,X201,X200)|~human(X201)|owner(X201),inference(split_conjunct,[status(thm)],[c74])).
% 0.45/0.63 cnf(c78,plain,~owner(X198)|~of(X198,X199)|human(X198),inference(split_conjunct,[status(thm)],[c74])).
% 0.45/0.63 cnf(c29,axiom,X197!=X196|X195!=X194|~partof(X197,X195)|partof(X196,X194),theory(equality)).
% 0.45/0.63 cnf(c62,plain,~of(X192,X193)|event(skolem0005(X193,X192)),inference(split_conjunct,[status(thm)],[c61])).
% 0.45/0.63 cnf(c35,axiom,X190!=X189|~white(X190)|white(X189),theory(equality)).
% 0.45/0.63 cnf(c34,axiom,X187!=X186|~dirty(X187)|dirty(X186),theory(equality)).
% 0.45/0.63 cnf(c28,axiom,X185!=X184|X183!=X182|~of(X185,X183)|of(X184,X182),theory(equality)).
% 0.45/0.63 cnf(c33,axiom,X180!=X179|~lonely(X180)|lonely(X179),theory(equality)).
% 0.45/0.63 cnf(c27,axiom,X177!=X176|~owner(X177)|owner(X176),theory(equality)).
% 0.45/0.63 cnf(c26,axiom,X170!=X169|X172!=X174|X173!=X171|~have(X170,X172,X173)|have(X169,X174,X171),theory(equality)).
% 0.45/0.63 cnf(c25,axiom,X168!=X167|~nonhuman(X168)|nonhuman(X167),theory(equality)).
% 0.45/0.63 cnf(c24,axiom,X165!=X164|~proposition(X165)|proposition(X164),theory(equality)).
% 0.45/0.63 cnf(c23,axiom,X161!=X160|~drs(X161)|drs(X160),theory(equality)).
% 0.45/0.63 cnf(c22,axiom,X159!=X158|~human(X159)|human(X158),theory(equality)).
% 0.45/0.63 cnf(c21,axiom,X156!=X155|~woman(X156)|woman(X155),theory(equality)).
% 0.45/0.63 cnf(c20,axiom,X152!=X151|~man(X152)|man(X151),theory(equality)).
% 0.45/0.63 cnf(c19,axiom,X150!=X149|~female(X150)|female(X149),theory(equality)).
% 0.45/0.63 cnf(c18,axiom,X147!=X146|~male(X147)|male(X146),theory(equality)).
% 0.45/0.63 cnf(c17,axiom,X143!=X142|~abstraction(X143)|abstraction(X142),theory(equality)).
% 0.45/0.63 cnf(c16,axiom,X141!=X140|~new(X141)|new(X140),theory(equality)).
% 0.45/0.63 cnf(c15,axiom,X138!=X137|~old(X138)|old(X137),theory(equality)).
% 0.45/0.63 cnf(c14,axiom,X133!=X132|~entity(X133)|entity(X132),theory(equality)).
% 0.45/0.63 cnf(c13,axiom,X126!=X125|~city(X126)|city(X125),theory(equality)).
% 0.45/0.63 cnf(c12,axiom,X119!=X118|~hollywood(X119)|hollywood(X118),theory(equality)).
% 0.45/0.63 cnf(c11,axiom,X112!=X111|~eventuality(X112)|eventuality(X111),theory(equality)).
% 0.45/0.63 fof(ax1,axiom,(![U]:(chevy(U)=>car(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax1)).
% 0.45/0.63 fof(c172,plain,(![U]:(~chevy(U)|car(U))),inference(fof_nnf,[status(thm)],[ax1])).
% 0.45/0.63 fof(c173,plain,(![X52]:(~chevy(X52)|car(X52))),inference(variable_rename,[status(thm)],[c172])).
% 0.45/0.63 cnf(c174,plain,~chevy(X110)|car(X110),inference(split_conjunct,[status(thm)],[c173])).
% 0.45/0.63 fof(ax17,axiom,(![U]:(eventuality(U)=>(~entity(U)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax17)).
% 0.45/0.63 fof(c120,plain,(![U]:(eventuality(U)=>~entity(U))),inference(fof_simplification,[status(thm)],[ax17])).
% 0.45/0.63 fof(c121,plain,(![U]:(~eventuality(U)|~entity(U))),inference(fof_nnf,[status(thm)],[c120])).
% 0.45/0.63 fof(c122,plain,(![X36]:(~eventuality(X36)|~entity(X36))),inference(variable_rename,[status(thm)],[c121])).
% 0.45/0.63 cnf(c123,plain,~eventuality(X78)|~entity(X78),inference(split_conjunct,[status(thm)],[c122])).
% 0.45/0.63 fof(ax15,axiom,(![U]:(object(U)=>entity(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax15)).
% 0.45/0.63 fof(c128,plain,(![U]:(~object(U)|entity(U))),inference(fof_nnf,[status(thm)],[ax15])).
% 0.45/0.63 fof(c129,plain,(![X38]:(~object(X38)|entity(X38))),inference(variable_rename,[status(thm)],[c128])).
% 0.45/0.63 cnf(c130,plain,~object(X82)|entity(X82),inference(split_conjunct,[status(thm)],[c129])).
% 0.45/0.63 fof(ax9,axiom,(![U]:(artifact(U)=>object(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax9)).
% 0.45/0.63 fof(c147,plain,(![U]:(~artifact(U)|object(U))),inference(fof_nnf,[status(thm)],[ax9])).
% 0.45/0.63 fof(c148,plain,(![X44]:(~artifact(X44)|object(X44))),inference(variable_rename,[status(thm)],[c147])).
% 0.45/0.63 cnf(c149,plain,~artifact(X94)|object(X94),inference(split_conjunct,[status(thm)],[c148])).
% 0.45/0.63 fof(ax5,axiom,(![U]:(instrumentality(U)=>artifact(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax5)).
% 0.45/0.63 fof(c160,plain,(![U]:(~instrumentality(U)|artifact(U))),inference(fof_nnf,[status(thm)],[ax5])).
% 0.45/0.63 fof(c161,plain,(![X48]:(~instrumentality(X48)|artifact(X48))),inference(variable_rename,[status(thm)],[c160])).
% 0.45/0.63 cnf(c162,plain,~instrumentality(X102)|artifact(X102),inference(split_conjunct,[status(thm)],[c161])).
% 0.45/0.63 fof(ax4,axiom,(![U]:(transport(U)=>instrumentality(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax4)).
% 0.45/0.63 fof(c163,plain,(![U]:(~transport(U)|instrumentality(U))),inference(fof_nnf,[status(thm)],[ax4])).
% 0.45/0.63 fof(c164,plain,(![X49]:(~transport(X49)|instrumentality(X49))),inference(variable_rename,[status(thm)],[c163])).
% 0.45/0.63 cnf(c165,plain,~transport(X103)|instrumentality(X103),inference(split_conjunct,[status(thm)],[c164])).
% 0.45/0.63 fof(ax3,axiom,(![U]:(vehicle(U)=>transport(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax3)).
% 0.45/0.63 fof(c166,plain,(![U]:(~vehicle(U)|transport(U))),inference(fof_nnf,[status(thm)],[ax3])).
% 0.45/0.63 fof(c167,plain,(![X50]:(~vehicle(X50)|transport(X50))),inference(variable_rename,[status(thm)],[c166])).
% 0.45/0.63 cnf(c168,plain,~vehicle(X104)|transport(X104),inference(split_conjunct,[status(thm)],[c167])).
% 0.45/0.63 cnf(c45,negated_conjecture,car(skolem0003),inference(split_conjunct,[status(thm)],[c40])).
% 0.45/0.63 fof(ax2,axiom,(![U]:(car(U)=>vehicle(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax2)).
% 0.45/0.63 fof(c169,plain,(![U]:(~car(U)|vehicle(U))),inference(fof_nnf,[status(thm)],[ax2])).
% 0.45/0.63 fof(c170,plain,(![X51]:(~car(X51)|vehicle(X51))),inference(variable_rename,[status(thm)],[c169])).
% 0.45/0.63 cnf(c171,plain,~car(X105)|vehicle(X105),inference(split_conjunct,[status(thm)],[c170])).
% 0.45/0.63 cnf(c203,plain,vehicle(skolem0003),inference(resolution,[status(thm)],[c171, c45])).
% 0.45/0.63 cnf(c205,plain,transport(skolem0003),inference(resolution,[status(thm)],[c203, c168])).
% 0.45/0.63 cnf(c206,plain,instrumentality(skolem0003),inference(resolution,[status(thm)],[c205, c165])).
% 0.45/0.63 cnf(c207,plain,artifact(skolem0003),inference(resolution,[status(thm)],[c206, c162])).
% 0.45/0.63 cnf(c208,plain,object(skolem0003),inference(resolution,[status(thm)],[c207, c149])).
% 0.45/0.63 cnf(c209,plain,entity(skolem0003),inference(resolution,[status(thm)],[c208, c130])).
% 0.45/0.63 cnf(c212,plain,~eventuality(skolem0003),inference(resolution,[status(thm)],[c209, c123])).
% 0.45/0.63 fof(ax18,axiom,(![U]:(abstraction(U)=>(~entity(U)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax18)).
% 0.45/0.63 fof(c116,plain,(![U]:(abstraction(U)=>~entity(U))),inference(fof_simplification,[status(thm)],[ax18])).
% 0.45/0.63 fof(c117,plain,(![U]:(~abstraction(U)|~entity(U))),inference(fof_nnf,[status(thm)],[c116])).
% 0.45/0.63 fof(c118,plain,(![X35]:(~abstraction(X35)|~entity(X35))),inference(variable_rename,[status(thm)],[c117])).
% 0.45/0.63 cnf(c119,plain,~abstraction(X77)|~entity(X77),inference(split_conjunct,[status(thm)],[c118])).
% 0.45/0.63 cnf(c211,plain,~abstraction(skolem0003),inference(resolution,[status(thm)],[c209, c119])).
% 0.45/0.63 cnf(c10,axiom,X109!=X108|~event(X109)|event(X108),theory(equality)).
% 0.45/0.63 cnf(c9,axiom,X107!=X106|~location(X107)|location(X106),theory(equality)).
% 0.45/0.63 cnf(c50,negated_conjecture,way(skolem0004),inference(split_conjunct,[status(thm)],[c40])).
% 0.45/0.63 fof(ax6,axiom,(![U]:(instrumentality(U)=>(~way(U)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax6)).
% 0.45/0.63 fof(c156,plain,(![U]:(instrumentality(U)=>~way(U))),inference(fof_simplification,[status(thm)],[ax6])).
% 0.45/0.63 fof(c157,plain,(![U]:(~instrumentality(U)|~way(U))),inference(fof_nnf,[status(thm)],[c156])).
% 0.45/0.63 fof(c158,plain,(![X47]:(~instrumentality(X47)|~way(X47))),inference(variable_rename,[status(thm)],[c157])).
% 0.45/0.63 cnf(c159,plain,~instrumentality(X99)|~way(X99),inference(split_conjunct,[status(thm)],[c158])).
% 0.45/0.63 cnf(c201,plain,~instrumentality(skolem0004),inference(resolution,[status(thm)],[c159, c50])).
% 0.45/0.63 cnf(c8,axiom,X101!=X100|~object(X101)|object(X100),theory(equality)).
% 0.45/0.63 fof(ax7,axiom,(![U]:(street(U)=>way(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax7)).
% 0.45/0.63 fof(c153,plain,(![U]:(~street(U)|way(U))),inference(fof_nnf,[status(thm)],[ax7])).
% 0.45/0.63 fof(c154,plain,(![X46]:(~street(X46)|way(X46))),inference(variable_rename,[status(thm)],[c153])).
% 0.45/0.63 cnf(c155,plain,~street(X98)|way(X98),inference(split_conjunct,[status(thm)],[c154])).
% 0.45/0.63 fof(ax8,axiom,(![U]:(way(U)=>artifact(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax8)).
% 0.45/0.63 fof(c150,plain,(![U]:(~way(U)|artifact(U))),inference(fof_nnf,[status(thm)],[ax8])).
% 0.45/0.63 fof(c151,plain,(![X45]:(~way(X45)|artifact(X45))),inference(variable_rename,[status(thm)],[c150])).
% 0.45/0.63 cnf(c152,plain,~way(X95)|artifact(X95),inference(split_conjunct,[status(thm)],[c151])).
% 0.45/0.63 cnf(c194,plain,artifact(skolem0004),inference(resolution,[status(thm)],[c152, c50])).
% 0.45/0.63 cnf(c195,plain,object(skolem0004),inference(resolution,[status(thm)],[c194, c149])).
% 0.45/0.63 cnf(c196,plain,entity(skolem0004),inference(resolution,[status(thm)],[c195, c130])).
% 0.45/0.63 cnf(c198,plain,~eventuality(skolem0004),inference(resolution,[status(thm)],[c196, c123])).
% 0.45/0.63 cnf(c197,plain,~abstraction(skolem0004),inference(resolution,[status(thm)],[c196, c119])).
% 0.45/0.63 cnf(c7,axiom,X97!=X96|~street(X97)|street(X96),theory(equality)).
% 0.45/0.63 cnf(c6,axiom,X93!=X92|~way(X93)|way(X92),theory(equality)).
% 0.45/0.63 cnf(c42,negated_conjecture,city(skolem0001),inference(split_conjunct,[status(thm)],[c40])).
% 0.45/0.63 fof(ax13,axiom,(![U]:(city(U)=>location(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax13)).
% 0.45/0.63 fof(c134,plain,(![U]:(~city(U)|location(U))),inference(fof_nnf,[status(thm)],[ax13])).
% 0.45/0.63 fof(c135,plain,(![X40]:(~city(X40)|location(X40))),inference(variable_rename,[status(thm)],[c134])).
% 0.45/0.63 cnf(c136,plain,~city(X84)|location(X84),inference(split_conjunct,[status(thm)],[c135])).
% 0.45/0.63 cnf(c182,plain,location(skolem0001),inference(resolution,[status(thm)],[c136, c42])).
% 0.45/0.63 fof(ax10,axiom,(![U]:(artifact(U)=>(~location(U)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax10)).
% 0.45/0.63 fof(c143,plain,(![U]:(artifact(U)=>~location(U))),inference(fof_simplification,[status(thm)],[ax10])).
% 0.45/0.63 fof(c144,plain,(![U]:(~artifact(U)|~location(U))),inference(fof_nnf,[status(thm)],[c143])).
% 0.45/0.63 fof(c145,plain,(![X43]:(~artifact(X43)|~location(X43))),inference(variable_rename,[status(thm)],[c144])).
% 0.45/0.63 cnf(c146,plain,~artifact(X91)|~location(X91),inference(split_conjunct,[status(thm)],[c145])).
% 0.45/0.63 cnf(c192,plain,~artifact(skolem0001),inference(resolution,[status(thm)],[c146, c182])).
% 0.45/0.63 fof(ax19,axiom,(![U]:(abstraction(U)=>(~eventuality(U)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax19)).
% 0.45/0.63 fof(c112,plain,(![U]:(abstraction(U)=>~eventuality(U))),inference(fof_simplification,[status(thm)],[ax19])).
% 0.45/0.63 fof(c113,plain,(![U]:(~abstraction(U)|~eventuality(U))),inference(fof_nnf,[status(thm)],[c112])).
% 0.45/0.63 fof(c114,plain,(![X34]:(~abstraction(X34)|~eventuality(X34))),inference(variable_rename,[status(thm)],[c113])).
% 0.45/0.63 cnf(c115,plain,~abstraction(X76)|~eventuality(X76),inference(split_conjunct,[status(thm)],[c114])).
% 0.45/0.63 cnf(c43,negated_conjecture,event(skolem0002),inference(split_conjunct,[status(thm)],[c40])).
% 0.45/0.63 fof(ax11,axiom,(![U]:(event(U)=>eventuality(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax11)).
% 0.45/0.63 fof(c140,plain,(![U]:(~event(U)|eventuality(U))),inference(fof_nnf,[status(thm)],[ax11])).
% 0.45/0.63 fof(c141,plain,(![X42]:(~event(X42)|eventuality(X42))),inference(variable_rename,[status(thm)],[c140])).
% 0.45/0.63 cnf(c142,plain,~event(X90)|eventuality(X90),inference(split_conjunct,[status(thm)],[c141])).
% 0.45/0.63 cnf(c190,plain,eventuality(skolem0002),inference(resolution,[status(thm)],[c142, c43])).
% 0.45/0.63 cnf(c191,plain,~abstraction(skolem0002),inference(resolution,[status(thm)],[c190, c115])).
% 0.45/0.63 cnf(c5,axiom,X89!=X88|~artifact(X89)|artifact(X88),theory(equality)).
% 0.45/0.63 fof(ax12,axiom,(![U]:(hollywood(U)=>city(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax12)).
% 0.45/0.63 fof(c137,plain,(![U]:(~hollywood(U)|city(U))),inference(fof_nnf,[status(thm)],[ax12])).
% 0.45/0.63 fof(c138,plain,(![X41]:(~hollywood(X41)|city(X41))),inference(variable_rename,[status(thm)],[c137])).
% 0.45/0.63 cnf(c139,plain,~hollywood(X87)|city(X87),inference(split_conjunct,[status(thm)],[c138])).
% 0.45/0.63 fof(ax14,axiom,(![U]:(location(U)=>object(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax14)).
% 0.45/0.63 fof(c131,plain,(![U]:(~location(U)|object(U))),inference(fof_nnf,[status(thm)],[ax14])).
% 0.45/0.63 fof(c132,plain,(![X39]:(~location(X39)|object(X39))),inference(variable_rename,[status(thm)],[c131])).
% 0.45/0.63 cnf(c133,plain,~location(X83)|object(X83),inference(split_conjunct,[status(thm)],[c132])).
% 0.45/0.63 cnf(c183,plain,object(skolem0001),inference(resolution,[status(thm)],[c182, c133])).
% 0.45/0.63 cnf(c184,plain,entity(skolem0001),inference(resolution,[status(thm)],[c183, c130])).
% 0.45/0.63 cnf(c187,plain,~eventuality(skolem0001),inference(resolution,[status(thm)],[c184, c123])).
% 0.45/0.63 cnf(c186,plain,~abstraction(skolem0001),inference(resolution,[status(thm)],[c184, c119])).
% 0.45/0.63 cnf(c4,axiom,X86!=X85|~instrumentality(X86)|instrumentality(X85),theory(equality)).
% 0.45/0.63 cnf(c3,axiom,X81!=X80|~transport(X81)|transport(X80),theory(equality)).
% 0.45/0.63 fof(ax16,axiom,(![U]:(old(U)=>(~new(U)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax16)).
% 0.45/0.63 fof(c124,plain,(![U]:(old(U)=>~new(U))),inference(fof_simplification,[status(thm)],[ax16])).
% 0.45/0.63 fof(c125,plain,(![U]:(~old(U)|~new(U))),inference(fof_nnf,[status(thm)],[c124])).
% 0.45/0.63 fof(c126,plain,(![X37]:(~old(X37)|~new(X37))),inference(variable_rename,[status(thm)],[c125])).
% 0.45/0.63 cnf(c127,plain,~old(X79)|~new(X79),inference(split_conjunct,[status(thm)],[c126])).
% 0.45/0.63 fof(ax20,axiom,(![U]:(male(U)=>(~female(U)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax20)).
% 0.45/0.63 fof(c108,plain,(![U]:(male(U)=>~female(U))),inference(fof_simplification,[status(thm)],[ax20])).
% 0.45/0.63 fof(c109,plain,(![U]:(~male(U)|~female(U))),inference(fof_nnf,[status(thm)],[c108])).
% 0.45/0.63 fof(c110,plain,(![X33]:(~male(X33)|~female(X33))),inference(variable_rename,[status(thm)],[c109])).
% 0.45/0.63 cnf(c111,plain,~male(X75)|~female(X75),inference(split_conjunct,[status(thm)],[c110])).
% 0.45/0.63 cnf(c2,axiom,X74!=X73|~vehicle(X74)|vehicle(X73),theory(equality)).
% 0.45/0.63 fof(ax21,axiom,(![U]:(man(U)=>(~woman(U)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax21)).
% 0.45/0.63 fof(c104,plain,(![U]:(man(U)=>~woman(U))),inference(fof_simplification,[status(thm)],[ax21])).
% 0.45/0.63 fof(c105,plain,(![U]:(~man(U)|~woman(U))),inference(fof_nnf,[status(thm)],[c104])).
% 0.45/0.63 fof(c106,plain,(![X32]:(~man(X32)|~woman(X32))),inference(variable_rename,[status(thm)],[c105])).
% 0.45/0.63 cnf(c107,plain,~man(X72)|~woman(X72),inference(split_conjunct,[status(thm)],[c106])).
% 0.45/0.63 fof(ax22,axiom,(![U]:(man(U)=>male(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax22)).
% 0.45/0.63 fof(c101,plain,(![U]:(~man(U)|male(U))),inference(fof_nnf,[status(thm)],[ax22])).
% 0.45/0.63 fof(c102,plain,(![X31]:(~man(X31)|male(X31))),inference(variable_rename,[status(thm)],[c101])).
% 0.45/0.63 cnf(c103,plain,~man(X71)|male(X71),inference(split_conjunct,[status(thm)],[c102])).
% 0.45/0.63 fof(ax23,axiom,(![U]:(male(U)=>human(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax23)).
% 0.45/0.63 fof(c98,plain,(![U]:(~male(U)|human(U))),inference(fof_nnf,[status(thm)],[ax23])).
% 0.45/0.63 fof(c99,plain,(![X30]:(~male(X30)|human(X30))),inference(variable_rename,[status(thm)],[c98])).
% 0.45/0.63 cnf(c100,plain,~male(X70)|human(X70),inference(split_conjunct,[status(thm)],[c99])).
% 0.45/0.63 fof(ax24,axiom,(![U]:(female(U)=>human(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax24)).
% 0.45/0.63 fof(c95,plain,(![U]:(~female(U)|human(U))),inference(fof_nnf,[status(thm)],[ax24])).
% 0.45/0.63 fof(c96,plain,(![X29]:(~female(X29)|human(X29))),inference(variable_rename,[status(thm)],[c95])).
% 0.45/0.63 cnf(c97,plain,~female(X69)|human(X69),inference(split_conjunct,[status(thm)],[c96])).
% 0.45/0.63 fof(ax25,axiom,(![U]:(woman(U)=>female(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax25)).
% 0.45/0.63 fof(c92,plain,(![U]:(~woman(U)|female(U))),inference(fof_nnf,[status(thm)],[ax25])).
% 0.45/0.63 fof(c93,plain,(![X28]:(~woman(X28)|female(X28))),inference(variable_rename,[status(thm)],[c92])).
% 0.45/0.63 cnf(c94,plain,~woman(X68)|female(X68),inference(split_conjunct,[status(thm)],[c93])).
% 0.45/0.63 cnf(c1,axiom,X67!=X66|~car(X67)|car(X66),theory(equality)).
% 0.45/0.63 fof(ax26,axiom,(![U]:(drs(U)<=>proposition(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax26)).
% 0.45/0.63 fof(c86,plain,(![U]:((~drs(U)|proposition(U))&(~proposition(U)|drs(U)))),inference(fof_nnf,[status(thm)],[ax26])).
% 0.45/0.63 fof(c87,plain,((![U]:(~drs(U)|proposition(U)))&(![U]:(~proposition(U)|drs(U)))),inference(shift_quantors,[status(thm)],[c86])).
% 0.45/0.63 fof(c89,plain,(![X26]:(![X27]:((~drs(X26)|proposition(X26))&(~proposition(X27)|drs(X27))))),inference(shift_quantors,[status(thm)],[fof(c88,plain,((![X26]:(~drs(X26)|proposition(X26)))&(![X27]:(~proposition(X27)|drs(X27)))),inference(variable_rename,[status(thm)],[c87])).])).
% 0.45/0.63 cnf(c91,plain,~proposition(X65)|drs(X65),inference(split_conjunct,[status(thm)],[c89])).
% 0.45/0.63 cnf(c90,plain,~drs(X64)|proposition(X64),inference(split_conjunct,[status(thm)],[c89])).
% 0.45/0.63 fof(ax27,axiom,(![U]:(nonhuman(U)=>entity(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax27)).
% 0.45/0.63 fof(c83,plain,(![U]:(~nonhuman(U)|entity(U))),inference(fof_nnf,[status(thm)],[ax27])).
% 0.45/0.63 fof(c84,plain,(![X25]:(~nonhuman(X25)|entity(X25))),inference(variable_rename,[status(thm)],[c83])).
% 0.45/0.63 cnf(c85,plain,~nonhuman(X63)|entity(X63),inference(split_conjunct,[status(thm)],[c84])).
% 0.45/0.63 fof(ax28,axiom,(![U]:(human(U)=>(~nonhuman(U)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax28)).
% 0.45/0.63 fof(c79,plain,(![U]:(human(U)=>~nonhuman(U))),inference(fof_simplification,[status(thm)],[ax28])).
% 0.45/0.63 fof(c80,plain,(![U]:(~human(U)|~nonhuman(U))),inference(fof_nnf,[status(thm)],[c79])).
% 0.45/0.63 fof(c81,plain,(![X24]:(~human(X24)|~nonhuman(X24))),inference(variable_rename,[status(thm)],[c80])).
% 0.45/0.63 cnf(c82,plain,~human(X62)|~nonhuman(X62),inference(split_conjunct,[status(thm)],[c81])).
% 0.45/0.63 cnf(c0,axiom,X61!=X60|~chevy(X61)|chevy(X60),theory(equality)).
% 0.45/0.63 cnf(c51,negated_conjecture,lonely(skolem0004),inference(split_conjunct,[status(thm)],[c40])).
% 0.45/0.63 cnf(transitivity,axiom,X56!=X58|X58!=X57|X56=X57,theory(equality)).
% 0.45/0.63 cnf(c49,negated_conjecture,street(skolem0004),inference(split_conjunct,[status(thm)],[c40])).
% 0.45/0.63 cnf(c48,negated_conjecture,old(skolem0003),inference(split_conjunct,[status(thm)],[c40])).
% 0.45/0.63 cnf(c47,negated_conjecture,dirty(skolem0003),inference(split_conjunct,[status(thm)],[c40])).
% 0.45/0.63 cnf(c46,negated_conjecture,white(skolem0003),inference(split_conjunct,[status(thm)],[c40])).
% 0.45/0.63 cnf(symmetry,axiom,X54!=X55|X55=X54,theory(equality)).
% 0.45/0.63 cnf(c44,negated_conjecture,chevy(skolem0003),inference(split_conjunct,[status(thm)],[c40])).
% 0.45/0.63 cnf(c41,negated_conjecture,hollywood(skolem0001),inference(split_conjunct,[status(thm)],[c40])).
% 0.45/0.63 % SZS output end Saturation
% 0.45/0.63
% 0.45/0.63 % Initial clauses : 91
% 0.45/0.63 % Processed clauses : 119
% 0.45/0.63 % Factors computed : 2
% 0.45/0.63 % Resolvents computed: 66
% 0.45/0.63 % Tautologies deleted: 32
% 0.45/0.63 % Forward subsumed : 8
% 0.45/0.63 % Backward subsumed : 0
% 0.45/0.63 % -------- CPU Time ---------
% 0.45/0.63 % User time : 0.257 s
% 0.45/0.63 % System time : 0.018 s
% 0.45/0.63 % Total time : 0.275 s
%------------------------------------------------------------------------------