%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP022+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n004.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:39 EDT 2024
% Result : CounterSatisfiable 0.59s 0.77s
% Output : Saturation 0.59s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : NLP022+1 : TPTP v8.1.2. Released v2.4.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n004.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 13:31:53 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.59/0.77 % Version: 1.5
% 0.59/0.77 % SZS status CounterSatisfiable
% 0.59/0.77 % SZS output start Saturation
% 0.59/0.77 cnf(reflexivity,axiom,X67=X67,theory(equality)).
% 0.59/0.77 cnf(c35,axiom,X226!=X227|X225!=X228|~in(X226,X225)|in(X227,X228),theory(equality)).
% 0.59/0.77 cnf(symmetry,axiom,X68!=X69|X69=X68,theory(equality)).
% 0.59/0.77 fof(co1,conjecture,(![U]:(![V]:(![W]:(![X]:(![Y]:(![Z]:(![X1]:(![X2]:(![X3]:(((((((((((((((((((((((((((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))&seat(X1))&furniture(X1))&front(X1))&fellow(Y))&man(Y))&young(Y))&fellow(Z))&man(Z))&young(Z))&Y=X2)&in(X2,X1))&Z=X3)&in(X3,X1))=>Y=Z)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', co1)).
% 0.59/0.77 fof(c42,negated_conjecture,(~(![U]:(![V]:(![W]:(![X]:(![Y]:(![Z]:(![X1]:(![X2]:(![X3]:(((((((((((((((((((((((((((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))&seat(X1))&furniture(X1))&front(X1))&fellow(Y))&man(Y))&young(Y))&fellow(Z))&man(Z))&young(Z))&Y=X2)&in(X2,X1))&Z=X3)&in(X3,X1))=>Y=Z))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 0.59/0.77 fof(c43,negated_conjecture,(?[U]:(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(?[X2]:(?[X3]:(((((((((((((((((((((((((((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))&seat(X1))&furniture(X1))&front(X1))&fellow(Y))&man(Y))&young(Y))&fellow(Z))&man(Z))&young(Z))&Y=X2)&in(X2,X1))&Z=X3)&in(X3,X1))&Y!=Z)))))))))),inference(fof_nnf,[status(thm)],[c42])).
% 0.59/0.77 fof(c44,negated_conjecture,(?[U]:(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:((?[X1]:(?[X2]:(?[X3]:((((((((((((((((((((((((((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))&seat(X1))&furniture(X1))&front(X1))&fellow(Y))&man(Y))&young(Y))&fellow(Z))&man(Z))&young(Z))&Y=X2)&in(X2,X1))&Z=X3)&in(X3,X1)))))&Y!=Z))))))),inference(shift_quantors,[status(thm)],[c43])).
% 0.59/0.77 fof(c45,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:((?[X8]:(?[X9]:(?[X10]:((((((((((((((((((((((((((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))&seat(X8))&furniture(X8))&front(X8))&fellow(X6))&man(X6))&young(X6))&fellow(X7))&man(X7))&young(X7))&X6=X9)&in(X9,X8))&X7=X10)&in(X10,X8)))))&X6!=X7))))))),inference(variable_rename,[status(thm)],[c44])).
% 0.59/0.77 fof(c46,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))&seat(skolem0007))&furniture(skolem0007))&front(skolem0007))&fellow(skolem0005))&man(skolem0005))&young(skolem0005))&fellow(skolem0006))&man(skolem0006))&young(skolem0006))&skolem0005=skolem0008)&in(skolem0008,skolem0007))&skolem0006=skolem0009)&in(skolem0009,skolem0007))&skolem0005!=skolem0006),inference(skolemize,[status(esa)],[c45])).
% 0.59/0.77 cnf(c70,negated_conjecture,skolem0005=skolem0008,inference(split_conjunct,[status(thm)],[c46])).
% 0.59/0.77 cnf(c231,plain,skolem0008=skolem0005,inference(resolution,[status(thm)],[c70, symmetry])).
% 0.59/0.77 cnf(c71,negated_conjecture,in(skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c46])).
% 0.59/0.77 cnf(c474,plain,skolem0008!=X282|skolem0007!=X281|in(X282,X281),inference(resolution,[status(thm)],[c35, c71])).
% 0.59/0.77 cnf(c510,plain,skolem0008!=X291|in(X291,skolem0007),inference(resolution,[status(thm)],[c474, reflexivity])).
% 0.59/0.77 cnf(c518,plain,in(skolem0005,skolem0007),inference(resolution,[status(thm)],[c510, c231])).
% 0.59/0.77 cnf(c519,plain,skolem0005!=X298|skolem0007!=X297|in(X298,X297),inference(resolution,[status(thm)],[c518, c35])).
% 0.59/0.77 cnf(c525,plain,skolem0005!=X299|in(X299,skolem0007),inference(resolution,[status(thm)],[c519, reflexivity])).
% 0.59/0.77 cnf(c72,negated_conjecture,skolem0006=skolem0009,inference(split_conjunct,[status(thm)],[c46])).
% 0.59/0.77 cnf(c236,plain,skolem0009=skolem0006,inference(resolution,[status(thm)],[c72, symmetry])).
% 0.59/0.77 cnf(c73,negated_conjecture,in(skolem0009,skolem0007),inference(split_conjunct,[status(thm)],[c46])).
% 0.59/0.77 cnf(c473,plain,skolem0009!=X280|skolem0007!=X279|in(X280,X279),inference(resolution,[status(thm)],[c35, c73])).
% 0.59/0.77 cnf(c509,plain,skolem0009!=X288|in(X288,skolem0007),inference(resolution,[status(thm)],[c473, reflexivity])).
% 0.59/0.77 cnf(c513,plain,in(skolem0006,skolem0007),inference(resolution,[status(thm)],[c509, c236])).
% 0.59/0.77 cnf(c515,plain,skolem0006!=X294|skolem0007!=X293|in(X294,X293),inference(resolution,[status(thm)],[c513, c35])).
% 0.59/0.77 cnf(c521,plain,skolem0006!=X296|in(X296,skolem0007),inference(resolution,[status(thm)],[c515, reflexivity])).
% 0.59/0.77 cnf(c58,negated_conjecture,barrel(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c46])).
% 0.59/0.77 cnf(c38,axiom,X237!=X238|X236!=X239|~barrel(X237,X236)|barrel(X238,X239),theory(equality)).
% 0.59/0.77 cnf(c481,plain,skolem0002!=X290|skolem0003!=X289|barrel(X290,X289),inference(resolution,[status(thm)],[c38, c58])).
% 0.59/0.77 cnf(c516,plain,skolem0002!=X295|barrel(X295,skolem0003),inference(resolution,[status(thm)],[c481, reflexivity])).
% 0.59/0.77 cnf(c59,negated_conjecture,down(skolem0002,skolem0004),inference(split_conjunct,[status(thm)],[c46])).
% 0.59/0.77 cnf(c37,axiom,X233!=X234|X232!=X235|~down(X233,X232)|down(X234,X235),theory(equality)).
% 0.59/0.77 cnf(c480,plain,skolem0002!=X283|skolem0004!=X284|down(X283,X284),inference(resolution,[status(thm)],[c37, c59])).
% 0.59/0.77 cnf(c511,plain,skolem0002!=X292|down(X292,skolem0004),inference(resolution,[status(thm)],[c480, reflexivity])).
% 0.59/0.77 cnf(c60,negated_conjecture,in(skolem0002,skolem0001),inference(split_conjunct,[status(thm)],[c46])).
% 0.59/0.77 cnf(c472,plain,skolem0002!=X278|skolem0001!=X277|in(X278,X277),inference(resolution,[status(thm)],[c35, c60])).
% 0.59/0.77 cnf(c507,plain,skolem0002!=X287|in(X287,skolem0001),inference(resolution,[status(thm)],[c472, reflexivity])).
% 0.59/0.77 cnf(c41,axiom,X246!=X247|~white(X246)|white(X247),theory(equality)).
% 0.59/0.77 cnf(c496,plain,~white(skolem0008)|white(skolem0005),inference(resolution,[status(thm)],[c41, c231])).
% 0.59/0.77 cnf(c495,plain,~white(skolem0005)|white(skolem0008),inference(resolution,[status(thm)],[c41, c70])).
% 0.59/0.77 cnf(c493,plain,~white(skolem0006)|white(skolem0009),inference(resolution,[status(thm)],[c41, c72])).
% 0.59/0.77 cnf(c492,plain,~white(skolem0009)|white(skolem0006),inference(resolution,[status(thm)],[c41, c236])).
% 0.59/0.77 cnf(c40,axiom,X243!=X244|~dirty(X243)|dirty(X244),theory(equality)).
% 0.59/0.77 cnf(c491,plain,~dirty(skolem0008)|dirty(skolem0005),inference(resolution,[status(thm)],[c40, c231])).
% 0.59/0.77 cnf(c490,plain,~dirty(skolem0005)|dirty(skolem0008),inference(resolution,[status(thm)],[c40, c70])).
% 0.59/0.77 cnf(c488,plain,~dirty(skolem0006)|dirty(skolem0009),inference(resolution,[status(thm)],[c40, c72])).
% 0.59/0.77 cnf(c487,plain,~dirty(skolem0009)|dirty(skolem0006),inference(resolution,[status(thm)],[c40, c236])).
% 0.59/0.77 cnf(c39,axiom,X240!=X241|~lonely(X240)|lonely(X241),theory(equality)).
% 0.59/0.77 cnf(c486,plain,~lonely(skolem0008)|lonely(skolem0005),inference(resolution,[status(thm)],[c39, c231])).
% 0.59/0.77 cnf(c485,plain,~lonely(skolem0005)|lonely(skolem0008),inference(resolution,[status(thm)],[c39, c70])).
% 0.59/0.77 cnf(c483,plain,~lonely(skolem0006)|lonely(skolem0009),inference(resolution,[status(thm)],[c39, c72])).
% 0.59/0.77 cnf(c482,plain,~lonely(skolem0009)|lonely(skolem0006),inference(resolution,[status(thm)],[c39, c236])).
% 0.59/0.77 cnf(c66,negated_conjecture,young(skolem0005),inference(split_conjunct,[status(thm)],[c46])).
% 0.59/0.77 cnf(c36,axiom,X229!=X230|~young(X229)|young(X230),theory(equality)).
% 0.59/0.77 cnf(c478,plain,~young(skolem0005)|young(skolem0008),inference(resolution,[status(thm)],[c36, c70])).
% 0.59/0.77 cnf(c508,plain,young(skolem0008),inference(resolution,[status(thm)],[c478, c66])).
% 0.59/0.77 cnf(c69,negated_conjecture,young(skolem0006),inference(split_conjunct,[status(thm)],[c46])).
% 0.59/0.77 cnf(c476,plain,~young(skolem0006)|young(skolem0009),inference(resolution,[status(thm)],[c36, c72])).
% 0.59/0.77 cnf(c506,plain,young(skolem0009),inference(resolution,[status(thm)],[c476, c69])).
% 0.59/0.77 cnf(c32,axiom,X214!=X215|~owner(X214)|owner(X215),theory(equality)).
% 0.59/0.77 cnf(c461,plain,~owner(skolem0008)|owner(skolem0005),inference(resolution,[status(thm)],[c32, c231])).
% 0.59/0.78 cnf(c460,plain,~owner(skolem0005)|owner(skolem0008),inference(resolution,[status(thm)],[c32, c70])).
% 0.59/0.78 cnf(c458,plain,~owner(skolem0006)|owner(skolem0009),inference(resolution,[status(thm)],[c32, c72])).
% 0.59/0.78 cnf(c457,plain,~owner(skolem0009)|owner(skolem0006),inference(resolution,[status(thm)],[c32, c236])).
% 0.59/0.78 cnf(c30,axiom,X205!=X206|~proposition(X205)|proposition(X206),theory(equality)).
% 0.59/0.78 cnf(c451,plain,~proposition(skolem0008)|proposition(skolem0005),inference(resolution,[status(thm)],[c30, c231])).
% 0.59/0.78 cnf(c450,plain,~proposition(skolem0005)|proposition(skolem0008),inference(resolution,[status(thm)],[c30, c70])).
% 0.59/0.78 cnf(c448,plain,~proposition(skolem0006)|proposition(skolem0009),inference(resolution,[status(thm)],[c30, c72])).
% 0.59/0.78 cnf(c447,plain,~proposition(skolem0009)|proposition(skolem0006),inference(resolution,[status(thm)],[c30, c236])).
% 0.59/0.78 cnf(c29,axiom,X202!=X203|~drs(X202)|drs(X203),theory(equality)).
% 0.59/0.78 cnf(c441,plain,~drs(skolem0008)|drs(skolem0005),inference(resolution,[status(thm)],[c29, c231])).
% 0.59/0.78 cnf(c440,plain,~drs(skolem0005)|drs(skolem0008),inference(resolution,[status(thm)],[c29, c70])).
% 0.59/0.78 cnf(c438,plain,~drs(skolem0006)|drs(skolem0009),inference(resolution,[status(thm)],[c29, c72])).
% 0.59/0.78 cnf(c437,plain,~drs(skolem0009)|drs(skolem0006),inference(resolution,[status(thm)],[c29, c236])).
% 0.59/0.78 cnf(c28,axiom,X194!=X195|~woman(X194)|woman(X195),theory(equality)).
% 0.59/0.78 cnf(c436,plain,~woman(skolem0008)|woman(skolem0005),inference(resolution,[status(thm)],[c28, c231])).
% 0.59/0.78 cnf(c435,plain,~woman(skolem0005)|woman(skolem0008),inference(resolution,[status(thm)],[c28, c70])).
% 0.59/0.78 cnf(c433,plain,~woman(skolem0006)|woman(skolem0009),inference(resolution,[status(thm)],[c28, c72])).
% 0.59/0.78 cnf(c432,plain,~woman(skolem0009)|woman(skolem0006),inference(resolution,[status(thm)],[c28, c236])).
% 0.59/0.78 cnf(c27,axiom,X189!=X190|~female(X189)|female(X190),theory(equality)).
% 0.59/0.78 cnf(c431,plain,~female(skolem0008)|female(skolem0005),inference(resolution,[status(thm)],[c27, c231])).
% 0.59/0.78 cnf(c430,plain,~female(skolem0005)|female(skolem0008),inference(resolution,[status(thm)],[c27, c70])).
% 0.59/0.78 cnf(c428,plain,~female(skolem0006)|female(skolem0009),inference(resolution,[status(thm)],[c27, c72])).
% 0.59/0.78 cnf(c427,plain,~female(skolem0009)|female(skolem0006),inference(resolution,[status(thm)],[c27, c236])).
% 0.59/0.78 cnf(c24,axiom,X168!=X169|~new(X168)|new(X169),theory(equality)).
% 0.59/0.78 cnf(c416,plain,~new(skolem0008)|new(skolem0005),inference(resolution,[status(thm)],[c24, c231])).
% 0.59/0.78 cnf(c415,plain,~new(skolem0005)|new(skolem0008),inference(resolution,[status(thm)],[c24, c70])).
% 0.59/0.78 cnf(c413,plain,~new(skolem0006)|new(skolem0009),inference(resolution,[status(thm)],[c24, c72])).
% 0.59/0.78 cnf(c412,plain,~new(skolem0009)|new(skolem0006),inference(resolution,[status(thm)],[c24, c236])).
% 0.59/0.78 cnf(c23,axiom,X161!=X162|~old(X161)|old(X162),theory(equality)).
% 0.59/0.78 cnf(c411,plain,~old(skolem0008)|old(skolem0005),inference(resolution,[status(thm)],[c23, c231])).
% 0.59/0.78 cnf(c410,plain,~old(skolem0005)|old(skolem0008),inference(resolution,[status(thm)],[c23, c70])).
% 0.59/0.78 cnf(c408,plain,~old(skolem0006)|old(skolem0009),inference(resolution,[status(thm)],[c23, c72])).
% 0.59/0.78 cnf(c407,plain,~old(skolem0009)|old(skolem0006),inference(resolution,[status(thm)],[c23, c236])).
% 0.59/0.78 cnf(transitivity,axiom,X70!=X72|X72!=X71|X70=X71,theory(equality)).
% 0.59/0.78 cnf(c391,plain,X276!=skolem0009|X276=skolem0006,inference(resolution,[status(thm)],[c236, transitivity])).
% 0.59/0.78 cnf(c10,axiom,X116!=X117|~instrumentality(X116)|instrumentality(X117),theory(equality)).
% 0.59/0.78 cnf(c406,plain,~instrumentality(skolem0009)|instrumentality(skolem0006),inference(resolution,[status(thm)],[c236, c10])).
% 0.59/0.78 cnf(c11,axiom,X121!=X122|~transport(X121)|transport(X122),theory(equality)).
% 0.59/0.78 cnf(c405,plain,~transport(skolem0009)|transport(skolem0006),inference(resolution,[status(thm)],[c236, c11])).
% 0.59/0.78 cnf(c13,axiom,X127!=X128|~way(X127)|way(X128),theory(equality)).
% 0.59/0.78 cnf(c404,plain,~way(skolem0009)|way(skolem0006),inference(resolution,[status(thm)],[c236, c13])).
% 0.59/0.78 cnf(c366,plain,X275!=skolem0008|X275=skolem0005,inference(resolution,[status(thm)],[c231, transitivity])).
% 0.59/0.78 cnf(c6,axiom,X97!=X98|~front(X97)|front(X98),theory(equality)).
% 0.59/0.78 cnf(c403,plain,~front(skolem0009)|front(skolem0006),inference(resolution,[status(thm)],[c236, c6])).
% 0.59/0.78 cnf(c22,axiom,X156!=X157|~city(X156)|city(X157),theory(equality)).
% 0.59/0.78 cnf(c401,plain,~city(skolem0009)|city(skolem0006),inference(resolution,[status(thm)],[c236, c22])).
% 0.59/0.78 cnf(c239,plain,X274!=skolem0006|X274=skolem0009,inference(resolution,[status(thm)],[c72, transitivity])).
% 0.59/0.78 cnf(c9,axiom,X111!=X112|~furniture(X111)|furniture(X112),theory(equality)).
% 0.59/0.78 cnf(c400,plain,~furniture(skolem0009)|furniture(skolem0006),inference(resolution,[status(thm)],[c236, c9])).
% 0.59/0.78 cnf(c15,axiom,X134!=X135|~chevy(X134)|chevy(X135),theory(equality)).
% 0.59/0.78 cnf(c399,plain,~chevy(skolem0009)|chevy(skolem0006),inference(resolution,[status(thm)],[c236, c15])).
% 0.59/0.78 cnf(c12,axiom,X123!=X124|~street(X123)|street(X124),theory(equality)).
% 0.59/0.78 cnf(c398,plain,~street(skolem0009)|street(skolem0006),inference(resolution,[status(thm)],[c236, c12])).
% 0.59/0.78 cnf(c234,plain,X273!=skolem0005|X273=skolem0008,inference(resolution,[status(thm)],[c70, transitivity])).
% 0.59/0.78 cnf(c19,axiom,X147!=X148|~event(X147)|event(X148),theory(equality)).
% 0.59/0.78 cnf(c397,plain,~event(skolem0009)|event(skolem0006),inference(resolution,[status(thm)],[c236, c19])).
% 0.59/0.78 cnf(c7,axiom,X104!=X105|~nonhuman(X104)|nonhuman(X105),theory(equality)).
% 0.59/0.78 cnf(c396,plain,~nonhuman(skolem0009)|nonhuman(skolem0006),inference(resolution,[status(thm)],[c236, c7])).
% 0.59/0.78 cnf(c21,axiom,X153!=X154|~hollywood(X153)|hollywood(X154),theory(equality)).
% 0.59/0.78 cnf(c395,plain,~hollywood(skolem0009)|hollywood(skolem0006),inference(resolution,[status(thm)],[c236, c21])).
% 0.59/0.78 cnf(c18,axiom,X144!=X145|~location(X144)|location(X145),theory(equality)).
% 0.59/0.78 cnf(c393,plain,~location(skolem0009)|location(skolem0006),inference(resolution,[status(thm)],[c236, c18])).
% 0.59/0.78 fof(ax38,axiom,(![U]:(![V]:(![W]:((have(U,V,W)&human(V))<=>(owner(V)&of(V,W)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax38)).
% 0.59/0.78 fof(c90,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)],[ax38])).
% 0.59/0.78 fof(c91,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)],[c90])).
% 0.59/0.78 fof(c93,plain,(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:(![X28]:(((~have(X23,X24,X25)|~human(X24))|(owner(X24)&of(X24,X25)))&((~owner(X27)|~of(X27,X28))|(have(X26,X27,X28)&human(X27)))))))))),inference(shift_quantors,[status(thm)],[fof(c92,plain,((![X23]:(![X24]:(![X25]:((~have(X23,X24,X25)|~human(X24))|(owner(X24)&of(X24,X25))))))&(![X26]:(![X27]:(![X28]:((~owner(X27)|~of(X27,X28))|(have(X26,X27,X28)&human(X27))))))),inference(variable_rename,[status(thm)],[c91])).])).
% 0.59/0.78 fof(c94,plain,(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:(![X28]:((((~have(X23,X24,X25)|~human(X24))|owner(X24))&((~have(X23,X24,X25)|~human(X24))|of(X24,X25)))&(((~owner(X27)|~of(X27,X28))|have(X26,X27,X28))&((~owner(X27)|~of(X27,X28))|human(X27)))))))))),inference(distribute,[status(thm)],[c93])).
% 0.59/0.78 cnf(c98,plain,~owner(X271)|~of(X271,X272)|human(X271),inference(split_conjunct,[status(thm)],[c94])).
% 0.59/0.78 cnf(c5,axiom,X92!=X93|~object(X92)|object(X93),theory(equality)).
% 0.59/0.78 cnf(c392,plain,~object(skolem0009)|object(skolem0006),inference(resolution,[status(thm)],[c236, c5])).
% 0.59/0.78 cnf(c8,axiom,X107!=X108|~seat(X107)|seat(X108),theory(equality)).
% 0.59/0.78 cnf(c387,plain,~seat(skolem0009)|seat(skolem0006),inference(resolution,[status(thm)],[c236, c8])).
% 0.59/0.78 cnf(c97,plain,~owner(X268)|~of(X268,X269)|have(X270,X268,X269),inference(split_conjunct,[status(thm)],[c94])).
% 0.59/0.78 cnf(c17,axiom,X140!=X141|~vehicle(X140)|vehicle(X141),theory(equality)).
% 0.59/0.78 cnf(c386,plain,~vehicle(skolem0009)|vehicle(skolem0006),inference(resolution,[status(thm)],[c236, c17])).
% 0.59/0.78 cnf(c14,axiom,X130!=X131|~artifact(X130)|artifact(X131),theory(equality)).
% 0.59/0.78 cnf(c385,plain,~artifact(skolem0009)|artifact(skolem0006),inference(resolution,[status(thm)],[c236, c14])).
% 0.59/0.78 cnf(c16,axiom,X137!=X138|~car(X137)|car(X138),theory(equality)).
% 0.59/0.78 cnf(c383,plain,~car(skolem0009)|car(skolem0006),inference(resolution,[status(thm)],[c236, c16])).
% 0.59/0.78 cnf(c381,plain,~instrumentality(skolem0008)|instrumentality(skolem0005),inference(resolution,[status(thm)],[c231, c10])).
% 0.59/0.78 cnf(c96,plain,~have(X266,X265,X267)|~human(X265)|of(X265,X267),inference(split_conjunct,[status(thm)],[c94])).
% 0.59/0.78 cnf(c380,plain,~transport(skolem0008)|transport(skolem0005),inference(resolution,[status(thm)],[c231, c11])).
% 0.59/0.78 cnf(c379,plain,~way(skolem0008)|way(skolem0005),inference(resolution,[status(thm)],[c231, c13])).
% 0.59/0.78 cnf(c378,plain,~front(skolem0008)|front(skolem0005),inference(resolution,[status(thm)],[c231, c6])).
% 0.59/0.78 cnf(c376,plain,~city(skolem0008)|city(skolem0005),inference(resolution,[status(thm)],[c231, c22])).
% 0.59/0.78 cnf(c95,plain,~have(X263,X262,X264)|~human(X262)|owner(X262),inference(split_conjunct,[status(thm)],[c94])).
% 0.59/0.78 cnf(c375,plain,~furniture(skolem0008)|furniture(skolem0005),inference(resolution,[status(thm)],[c231, c9])).
% 0.59/0.78 cnf(c374,plain,~chevy(skolem0008)|chevy(skolem0005),inference(resolution,[status(thm)],[c231, c15])).
% 0.59/0.78 cnf(c373,plain,~street(skolem0008)|street(skolem0005),inference(resolution,[status(thm)],[c231, c12])).
% 0.59/0.78 cnf(c372,plain,~event(skolem0008)|event(skolem0005),inference(resolution,[status(thm)],[c231, c19])).
% 0.59/0.78 cnf(c371,plain,~nonhuman(skolem0008)|nonhuman(skolem0005),inference(resolution,[status(thm)],[c231, c7])).
% 0.59/0.78 fof(ax39,axiom,(![U]:(![V]:(![W]:(((have(U,V,W)&nonhuman(V))&nonhuman(W))=>partof(W,V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax39)).
% 0.59/0.78 fof(c87,plain,(![U]:(![V]:(![W]:(((~have(U,V,W)|~nonhuman(V))|~nonhuman(W))|partof(W,V))))),inference(fof_nnf,[status(thm)],[ax39])).
% 0.59/0.78 fof(c88,plain,(![X20]:(![X21]:(![X22]:(((~have(X20,X21,X22)|~nonhuman(X21))|~nonhuman(X22))|partof(X22,X21))))),inference(variable_rename,[status(thm)],[c87])).
% 0.59/0.78 cnf(c89,plain,~have(X259,X260,X261)|~nonhuman(X260)|~nonhuman(X261)|partof(X261,X260),inference(split_conjunct,[status(thm)],[c88])).
% 0.59/0.78 cnf(c370,plain,~hollywood(skolem0008)|hollywood(skolem0005),inference(resolution,[status(thm)],[c231, c21])).
% 0.59/0.78 cnf(c368,plain,~location(skolem0008)|location(skolem0005),inference(resolution,[status(thm)],[c231, c18])).
% 0.59/0.78 cnf(c367,plain,~object(skolem0008)|object(skolem0005),inference(resolution,[status(thm)],[c231, c5])).
% 0.59/0.78 fof(ax40,axiom,(![U]:(![V]:(![W]:((event(U)&have(U,V,W))=>of(V,W))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax40)).
% 0.59/0.78 fof(c84,plain,(![U]:(![V]:(![W]:((~event(U)|~have(U,V,W))|of(V,W))))),inference(fof_nnf,[status(thm)],[ax40])).
% 0.59/0.78 fof(c85,plain,(![X17]:(![X18]:(![X19]:((~event(X17)|~have(X17,X18,X19))|of(X18,X19))))),inference(variable_rename,[status(thm)],[c84])).
% 0.59/0.78 cnf(c86,plain,~event(X258)|~have(X258,X257,X256)|of(X257,X256),inference(split_conjunct,[status(thm)],[c85])).
% 0.59/0.78 cnf(c362,plain,~seat(skolem0008)|seat(skolem0005),inference(resolution,[status(thm)],[c231, c8])).
% 0.59/0.78 cnf(c361,plain,~vehicle(skolem0008)|vehicle(skolem0005),inference(resolution,[status(thm)],[c231, c17])).
% 0.59/0.78 cnf(c360,plain,~artifact(skolem0008)|artifact(skolem0005),inference(resolution,[status(thm)],[c231, c14])).
% 0.59/0.78 fof(ax41,axiom,(![U]:(![V]:(of(V,U)=>(?[W]:(event(W)&have(W,U,V)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax41)).
% 0.59/0.78 fof(c78,plain,(![U]:(![V]:(~of(V,U)|(?[W]:(event(W)&have(W,U,V)))))),inference(fof_nnf,[status(thm)],[ax41])).
% 0.59/0.78 fof(c79,plain,(![X14]:(![X15]:(~of(X15,X14)|(?[X16]:(event(X16)&have(X16,X14,X15)))))),inference(variable_rename,[status(thm)],[c78])).
% 0.59/0.78 fof(c80,plain,(![X14]:(![X15]:(~of(X15,X14)|(event(skolem0010(X14,X15))&have(skolem0010(X14,X15),X14,X15))))),inference(skolemize,[status(esa)],[c79])).
% 0.59/0.78 fof(c81,plain,(![X14]:(![X15]:((~of(X15,X14)|event(skolem0010(X14,X15)))&(~of(X15,X14)|have(skolem0010(X14,X15),X14,X15))))),inference(distribute,[status(thm)],[c80])).
% 0.59/0.78 cnf(c83,plain,~of(X254,X255)|have(skolem0010(X255,X254),X255,X254),inference(split_conjunct,[status(thm)],[c81])).
% 0.59/0.78 cnf(c358,plain,~car(skolem0008)|car(skolem0005),inference(resolution,[status(thm)],[c231, c16])).
% 0.59/0.78 cnf(c356,plain,~city(skolem0005)|city(skolem0008),inference(resolution,[status(thm)],[c22, c70])).
% 0.59/0.78 cnf(c355,plain,~city(skolem0006)|city(skolem0009),inference(resolution,[status(thm)],[c22, c72])).
% 0.59/0.78 cnf(c351,plain,~hollywood(skolem0005)|hollywood(skolem0008),inference(resolution,[status(thm)],[c21, c70])).
% 0.59/0.78 cnf(c82,plain,~of(X252,X253)|event(skolem0010(X253,X252)),inference(split_conjunct,[status(thm)],[c81])).
% 0.59/0.78 cnf(c350,plain,~hollywood(skolem0006)|hollywood(skolem0009),inference(resolution,[status(thm)],[c21, c72])).
% 0.59/0.78 cnf(c335,plain,~event(skolem0005)|event(skolem0008),inference(resolution,[status(thm)],[c19, c70])).
% 0.59/0.78 cnf(c334,plain,~event(skolem0006)|event(skolem0009),inference(resolution,[status(thm)],[c19, c72])).
% 0.59/0.78 fof(ax42,axiom,(![U]:(![V]:(![W]:((partof(U,V)&partof(U,W))=>V=W)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax42)).
% 0.59/0.78 fof(c75,plain,(![U]:(![V]:(![W]:((~partof(U,V)|~partof(U,W))|V=W)))),inference(fof_nnf,[status(thm)],[ax42])).
% 0.59/0.78 fof(c76,plain,(![X11]:(![X12]:(![X13]:((~partof(X11,X12)|~partof(X11,X13))|X12=X13)))),inference(variable_rename,[status(thm)],[c75])).
% 0.59/0.78 cnf(c77,plain,~partof(X250,X249)|~partof(X250,X251)|X249=X251,inference(split_conjunct,[status(thm)],[c76])).
% 0.59/0.78 cnf(c332,plain,~location(skolem0005)|location(skolem0008),inference(resolution,[status(thm)],[c18, c70])).
% 0.59/0.78 cnf(c331,plain,~location(skolem0006)|location(skolem0009),inference(resolution,[status(thm)],[c18, c72])).
% 0.59/0.78 cnf(c322,plain,~vehicle(skolem0005)|vehicle(skolem0008),inference(resolution,[status(thm)],[c17, c70])).
% 0.59/0.78 cnf(c321,plain,~vehicle(skolem0006)|vehicle(skolem0009),inference(resolution,[status(thm)],[c17, c72])).
% 0.59/0.78 cnf(c316,plain,~car(skolem0005)|car(skolem0008),inference(resolution,[status(thm)],[c16, c70])).
% 0.59/0.78 cnf(c315,plain,~car(skolem0006)|car(skolem0009),inference(resolution,[status(thm)],[c16, c72])).
% 0.59/0.78 cnf(c308,plain,~chevy(skolem0005)|chevy(skolem0008),inference(resolution,[status(thm)],[c15, c70])).
% 0.59/0.78 cnf(c307,plain,~chevy(skolem0006)|chevy(skolem0009),inference(resolution,[status(thm)],[c15, c72])).
% 0.59/0.78 cnf(c303,plain,~artifact(skolem0005)|artifact(skolem0008),inference(resolution,[status(thm)],[c14, c70])).
% 0.59/0.78 cnf(c302,plain,~artifact(skolem0006)|artifact(skolem0009),inference(resolution,[status(thm)],[c14, c72])).
% 0.59/0.78 cnf(c295,plain,~way(skolem0005)|way(skolem0008),inference(resolution,[status(thm)],[c13, c70])).
% 0.59/0.78 cnf(c294,plain,~way(skolem0006)|way(skolem0009),inference(resolution,[status(thm)],[c13, c72])).
% 0.59/0.78 cnf(c290,plain,~street(skolem0005)|street(skolem0008),inference(resolution,[status(thm)],[c12, c70])).
% 0.59/0.78 cnf(c289,plain,~street(skolem0006)|street(skolem0009),inference(resolution,[status(thm)],[c12, c72])).
% 0.59/0.78 cnf(c282,plain,~transport(skolem0005)|transport(skolem0008),inference(resolution,[status(thm)],[c11, c70])).
% 0.59/0.78 cnf(c281,plain,~transport(skolem0006)|transport(skolem0009),inference(resolution,[status(thm)],[c11, c72])).
% 0.59/0.78 cnf(c276,plain,~instrumentality(skolem0005)|instrumentality(skolem0008),inference(resolution,[status(thm)],[c10, c70])).
% 0.59/0.78 cnf(c275,plain,~instrumentality(skolem0006)|instrumentality(skolem0009),inference(resolution,[status(thm)],[c10, c72])).
% 0.59/0.78 cnf(c272,plain,~furniture(skolem0005)|furniture(skolem0008),inference(resolution,[status(thm)],[c9, c70])).
% 0.59/0.78 cnf(c271,plain,~furniture(skolem0006)|furniture(skolem0009),inference(resolution,[status(thm)],[c9, c72])).
% 0.59/0.78 cnf(c266,plain,~seat(skolem0005)|seat(skolem0008),inference(resolution,[status(thm)],[c8, c70])).
% 0.59/0.78 cnf(c265,plain,~seat(skolem0006)|seat(skolem0009),inference(resolution,[status(thm)],[c8, c72])).
% 0.59/0.78 cnf(c258,plain,~nonhuman(skolem0005)|nonhuman(skolem0008),inference(resolution,[status(thm)],[c7, c70])).
% 0.59/0.78 cnf(c257,plain,~nonhuman(skolem0006)|nonhuman(skolem0009),inference(resolution,[status(thm)],[c7, c72])).
% 0.59/0.78 cnf(c255,plain,~front(skolem0005)|front(skolem0008),inference(resolution,[status(thm)],[c6, c70])).
% 0.59/0.78 cnf(c254,plain,~front(skolem0006)|front(skolem0009),inference(resolution,[status(thm)],[c6, c72])).
% 0.59/0.78 cnf(c252,plain,~object(skolem0005)|object(skolem0008),inference(resolution,[status(thm)],[c5, c70])).
% 0.59/0.78 cnf(c251,plain,~object(skolem0006)|object(skolem0009),inference(resolution,[status(thm)],[c5, c72])).
% 0.59/0.78 cnf(c67,negated_conjecture,fellow(skolem0006),inference(split_conjunct,[status(thm)],[c46])).
% 0.59/0.78 cnf(c0,axiom,X73!=X74|~fellow(X73)|fellow(X74),theory(equality)).
% 0.59/0.78 cnf(c237,plain,~fellow(skolem0006)|fellow(skolem0009),inference(resolution,[status(thm)],[c72, c0])).
% 0.59/0.78 cnf(c470,plain,fellow(skolem0009),inference(resolution,[status(thm)],[c237, c67])).
% 0.59/0.78 cnf(c34,axiom,X222!=X223|X221!=X224|~partof(X222,X221)|partof(X223,X224),theory(equality)).
% 0.59/0.78 fof(ax27,axiom,(![U]:(abstraction(U)=>(~entity(U)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax27)).
% 0.59/0.78 fof(c136,plain,(![U]:(abstraction(U)=>~entity(U))),inference(fof_simplification,[status(thm)],[ax27])).
% 0.59/0.78 fof(c137,plain,(![U]:(~abstraction(U)|~entity(U))),inference(fof_nnf,[status(thm)],[c136])).
% 0.59/0.78 fof(c138,plain,(![X40]:(~abstraction(X40)|~entity(X40))),inference(variable_rename,[status(thm)],[c137])).
% 0.59/0.78 cnf(c139,plain,~abstraction(X99)|~entity(X99),inference(split_conjunct,[status(thm)],[c138])).
% 0.59/0.78 fof(ax4,axiom,(![U]:(organism(U)=>entity(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax4)).
% 0.59/0.78 fof(c212,plain,(![U]:(~organism(U)|entity(U))),inference(fof_nnf,[status(thm)],[ax4])).
% 0.59/0.78 fof(c213,plain,(![X63]:(~organism(X63)|entity(X63))),inference(variable_rename,[status(thm)],[c212])).
% 0.59/0.78 cnf(c214,plain,~organism(X146)|entity(X146),inference(split_conjunct,[status(thm)],[c213])).
% 0.59/0.78 fof(ax3,axiom,(![U]:(human(U)=>organism(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax3)).
% 0.59/0.78 fof(c215,plain,(![U]:(~human(U)|organism(U))),inference(fof_nnf,[status(thm)],[ax3])).
% 0.59/0.78 fof(c216,plain,(![X64]:(~human(X64)|organism(X64))),inference(variable_rename,[status(thm)],[c215])).
% 0.59/0.78 cnf(c217,plain,~human(X149)|organism(X149),inference(split_conjunct,[status(thm)],[c216])).
% 0.59/0.78 fof(ax2,axiom,(![U]:(man(U)=>human(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax2)).
% 0.59/0.78 fof(c218,plain,(![U]:(~man(U)|human(U))),inference(fof_nnf,[status(thm)],[ax2])).
% 0.59/0.78 fof(c219,plain,(![X65]:(~man(X65)|human(X65))),inference(variable_rename,[status(thm)],[c218])).
% 0.59/0.78 cnf(c220,plain,~man(X152)|human(X152),inference(split_conjunct,[status(thm)],[c219])).
% 0.59/0.78 cnf(c68,negated_conjecture,man(skolem0006),inference(split_conjunct,[status(thm)],[c46])).
% 0.59/0.78 cnf(c1,axiom,X75!=X76|~man(X75)|man(X76),theory(equality)).
% 0.59/0.78 cnf(c235,plain,~man(skolem0006)|man(skolem0009),inference(resolution,[status(thm)],[c72, c1])).
% 0.59/0.78 cnf(c462,plain,man(skolem0009),inference(resolution,[status(thm)],[c235, c68])).
% 0.59/0.78 cnf(c464,plain,human(skolem0009),inference(resolution,[status(thm)],[c462, c220])).
% 0.59/0.78 cnf(c466,plain,organism(skolem0009),inference(resolution,[status(thm)],[c464, c217])).
% 0.59/0.78 cnf(c467,plain,entity(skolem0009),inference(resolution,[status(thm)],[c466, c214])).
% 0.59/0.78 cnf(c469,plain,~abstraction(skolem0009),inference(resolution,[status(thm)],[c467, c139])).
% 0.59/0.78 fof(ax26,axiom,(![U]:(eventuality(U)=>(~entity(U)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax26)).
% 0.59/0.78 fof(c140,plain,(![U]:(eventuality(U)=>~entity(U))),inference(fof_simplification,[status(thm)],[ax26])).
% 0.59/0.78 fof(c141,plain,(![U]:(~eventuality(U)|~entity(U))),inference(fof_nnf,[status(thm)],[c140])).
% 0.59/0.78 fof(c142,plain,(![X41]:(~eventuality(X41)|~entity(X41))),inference(variable_rename,[status(thm)],[c141])).
% 0.59/0.78 cnf(c143,plain,~eventuality(X100)|~entity(X100),inference(split_conjunct,[status(thm)],[c142])).
% 0.59/0.78 cnf(c468,plain,~eventuality(skolem0009),inference(resolution,[status(thm)],[c467, c143])).
% 0.59/0.78 cnf(c33,axiom,X218!=X219|X217!=X220|~of(X218,X217)|of(X219,X220),theory(equality)).
% 0.59/0.78 fof(ax31,axiom,(![U]:(man(U)=>male(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax31)).
% 0.59/0.78 fof(c121,plain,(![U]:(~man(U)|male(U))),inference(fof_nnf,[status(thm)],[ax31])).
% 0.59/0.78 fof(c122,plain,(![X36]:(~man(X36)|male(X36))),inference(variable_rename,[status(thm)],[c121])).
% 0.59/0.78 cnf(c123,plain,~man(X91)|male(X91),inference(split_conjunct,[status(thm)],[c122])).
% 0.59/0.78 cnf(c463,plain,male(skolem0009),inference(resolution,[status(thm)],[c462, c123])).
% 0.59/0.78 cnf(c64,negated_conjecture,fellow(skolem0005),inference(split_conjunct,[status(thm)],[c46])).
% 0.59/0.78 cnf(c232,plain,~fellow(skolem0005)|fellow(skolem0008),inference(resolution,[status(thm)],[c70, c0])).
% 0.59/0.78 cnf(c455,plain,fellow(skolem0008),inference(resolution,[status(thm)],[c232, c64])).
% 0.59/0.78 cnf(c31,axiom,X212!=X209|X207!=X211|X210!=X208|~have(X212,X207,X210)|have(X209,X211,X208),theory(equality)).
% 0.59/0.78 cnf(c65,negated_conjecture,man(skolem0005),inference(split_conjunct,[status(thm)],[c46])).
% 0.59/0.78 cnf(c230,plain,~man(skolem0005)|man(skolem0008),inference(resolution,[status(thm)],[c70, c1])).
% 0.59/0.78 cnf(c442,plain,man(skolem0008),inference(resolution,[status(thm)],[c230, c65])).
% 0.59/0.78 cnf(c444,plain,human(skolem0008),inference(resolution,[status(thm)],[c442, c220])).
% 0.59/0.78 cnf(c446,plain,organism(skolem0008),inference(resolution,[status(thm)],[c444, c217])).
% 0.59/0.78 cnf(c452,plain,entity(skolem0008),inference(resolution,[status(thm)],[c446, c214])).
% 0.59/0.78 cnf(c454,plain,~abstraction(skolem0008),inference(resolution,[status(thm)],[c452, c139])).
% 0.59/0.78 cnf(c453,plain,~eventuality(skolem0008),inference(resolution,[status(thm)],[c452, c143])).
% 0.59/0.78 cnf(c443,plain,male(skolem0008),inference(resolution,[status(thm)],[c442, c123])).
% 0.59/0.78 cnf(c26,axiom,X182!=X183|~male(X182)|male(X183),theory(equality)).
% 0.59/0.78 cnf(c25,axiom,X175!=X176|~abstraction(X175)|abstraction(X176),theory(equality)).
% 0.59/0.78 fof(ax1,axiom,(![U]:(fellow(U)=>man(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax1)).
% 0.59/0.78 fof(c221,plain,(![U]:(~fellow(U)|man(U))),inference(fof_nnf,[status(thm)],[ax1])).
% 0.59/0.78 fof(c222,plain,(![X66]:(~fellow(X66)|man(X66))),inference(variable_rename,[status(thm)],[c221])).
% 0.59/0.78 cnf(c223,plain,~fellow(X155)|man(X155),inference(split_conjunct,[status(thm)],[c222])).
% 0.59/0.78 fof(ax32,axiom,(![U]:(male(U)=>human(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax32)).
% 0.59/0.78 fof(c118,plain,(![U]:(~male(U)|human(U))),inference(fof_nnf,[status(thm)],[ax32])).
% 0.59/0.78 fof(c119,plain,(![X35]:(~male(X35)|human(X35))),inference(variable_rename,[status(thm)],[c118])).
% 0.59/0.78 cnf(c120,plain,~male(X90)|human(X90),inference(split_conjunct,[status(thm)],[c119])).
% 0.59/0.78 cnf(c247,plain,male(skolem0006),inference(resolution,[status(thm)],[c123, c68])).
% 0.59/0.78 cnf(c249,plain,human(skolem0006),inference(resolution,[status(thm)],[c247, c120])).
% 0.59/0.78 cnf(c337,plain,organism(skolem0006),inference(resolution,[status(thm)],[c217, c249])).
% 0.59/0.78 cnf(c339,plain,entity(skolem0006),inference(resolution,[status(thm)],[c337, c214])).
% 0.59/0.78 cnf(c343,plain,~abstraction(skolem0006),inference(resolution,[status(thm)],[c339, c139])).
% 0.59/0.78 cnf(c342,plain,~eventuality(skolem0006),inference(resolution,[status(thm)],[c339, c143])).
% 0.59/0.78 cnf(c246,plain,male(skolem0005),inference(resolution,[status(thm)],[c123, c65])).
% 0.59/0.78 cnf(c248,plain,human(skolem0005),inference(resolution,[status(thm)],[c246, c120])).
% 0.59/0.78 cnf(c336,plain,organism(skolem0005),inference(resolution,[status(thm)],[c217, c248])).
% 0.59/0.78 cnf(c338,plain,entity(skolem0005),inference(resolution,[status(thm)],[c336, c214])).
% 0.59/0.78 cnf(c341,plain,~abstraction(skolem0005),inference(resolution,[status(thm)],[c338, c139])).
% 0.59/0.78 cnf(c340,plain,~eventuality(skolem0005),inference(resolution,[status(thm)],[c338, c143])).
% 0.59/0.78 cnf(c20,axiom,X150!=X151|~eventuality(X150)|eventuality(X151),theory(equality)).
% 0.59/0.78 fof(ax23,axiom,(![U]:(location(U)=>object(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax23)).
% 0.59/0.78 fof(c151,plain,(![U]:(~location(U)|object(U))),inference(fof_nnf,[status(thm)],[ax23])).
% 0.59/0.78 fof(c152,plain,(![X44]:(~location(X44)|object(X44))),inference(variable_rename,[status(thm)],[c151])).
% 0.59/0.78 cnf(c153,plain,~location(X103)|object(X103),inference(split_conjunct,[status(thm)],[c152])).
% 0.59/0.78 cnf(c48,negated_conjecture,city(skolem0001),inference(split_conjunct,[status(thm)],[c46])).
% 0.59/0.78 fof(ax22,axiom,(![U]:(city(U)=>location(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax22)).
% 0.59/0.78 fof(c154,plain,(![U]:(~city(U)|location(U))),inference(fof_nnf,[status(thm)],[ax22])).
% 0.59/0.78 fof(c155,plain,(![X45]:(~city(X45)|location(X45))),inference(variable_rename,[status(thm)],[c154])).
% 0.59/0.78 cnf(c156,plain,~city(X106)|location(X106),inference(split_conjunct,[status(thm)],[c155])).
% 0.59/0.78 cnf(c259,plain,location(skolem0001),inference(resolution,[status(thm)],[c156, c48])).
% 0.59/0.78 cnf(c260,plain,object(skolem0001),inference(resolution,[status(thm)],[c259, c153])).
% 0.59/0.78 fof(ax5,axiom,(![U]:(organism(U)=>(~object(U)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax5)).
% 0.59/0.78 fof(c208,plain,(![U]:(organism(U)=>~object(U))),inference(fof_simplification,[status(thm)],[ax5])).
% 0.59/0.78 fof(c209,plain,(![U]:(~organism(U)|~object(U))),inference(fof_nnf,[status(thm)],[c208])).
% 0.59/0.78 fof(c210,plain,(![X62]:(~organism(X62)|~object(X62))),inference(variable_rename,[status(thm)],[c209])).
% 0.59/0.78 cnf(c211,plain,~organism(X143)|~object(X143),inference(split_conjunct,[status(thm)],[c210])).
% 0.59/0.78 cnf(c329,plain,~organism(skolem0001),inference(resolution,[status(thm)],[c211, c260])).
% 0.59/0.78 fof(ax18,axiom,(![U]:(artifact(U)=>object(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax18)).
% 0.59/0.78 fof(c167,plain,(![U]:(~artifact(U)|object(U))),inference(fof_nnf,[status(thm)],[ax18])).
% 0.59/0.78 fof(c168,plain,(![X49]:(~artifact(X49)|object(X49))),inference(variable_rename,[status(thm)],[c167])).
% 0.59/0.78 cnf(c169,plain,~artifact(X114)|object(X114),inference(split_conjunct,[status(thm)],[c168])).
% 0.59/0.78 fof(ax17,axiom,(![U]:(instrumentality(U)=>artifact(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax17)).
% 0.59/0.78 fof(c170,plain,(![U]:(~instrumentality(U)|artifact(U))),inference(fof_nnf,[status(thm)],[ax17])).
% 0.59/0.78 fof(c171,plain,(![X50]:(~instrumentality(X50)|artifact(X50))),inference(variable_rename,[status(thm)],[c170])).
% 0.59/0.78 cnf(c172,plain,~instrumentality(X115)|artifact(X115),inference(split_conjunct,[status(thm)],[c171])).
% 0.59/0.78 cnf(c62,negated_conjecture,furniture(skolem0007),inference(split_conjunct,[status(thm)],[c46])).
% 0.59/0.78 fof(ax8,axiom,(![U]:(furniture(U)=>instrumentality(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax8)).
% 0.59/0.78 fof(c199,plain,(![U]:(~furniture(U)|instrumentality(U))),inference(fof_nnf,[status(thm)],[ax8])).
% 0.59/0.78 fof(c200,plain,(![X59]:(~furniture(X59)|instrumentality(X59))),inference(variable_rename,[status(thm)],[c199])).
% 0.59/0.78 cnf(c201,plain,~furniture(X136)|instrumentality(X136),inference(split_conjunct,[status(thm)],[c200])).
% 0.59/0.78 cnf(c309,plain,instrumentality(skolem0007),inference(resolution,[status(thm)],[c201, c62])).
% 0.59/0.78 cnf(c310,plain,artifact(skolem0007),inference(resolution,[status(thm)],[c309, c172])).
% 0.59/0.78 cnf(c312,plain,object(skolem0007),inference(resolution,[status(thm)],[c310, c169])).
% 0.59/0.78 cnf(c328,plain,~organism(skolem0007),inference(resolution,[status(thm)],[c211, c312])).
% 0.59/0.78 fof(ax16,axiom,(![U]:(transport(U)=>instrumentality(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax16)).
% 0.59/0.78 fof(c173,plain,(![U]:(~transport(U)|instrumentality(U))),inference(fof_nnf,[status(thm)],[ax16])).
% 0.59/0.78 fof(c174,plain,(![X51]:(~transport(X51)|instrumentality(X51))),inference(variable_rename,[status(thm)],[c173])).
% 0.59/0.78 cnf(c175,plain,~transport(X118)|instrumentality(X118),inference(split_conjunct,[status(thm)],[c174])).
% 0.59/0.78 fof(ax15,axiom,(![U]:(vehicle(U)=>transport(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax15)).
% 0.59/0.78 fof(c176,plain,(![U]:(~vehicle(U)|transport(U))),inference(fof_nnf,[status(thm)],[ax15])).
% 0.59/0.78 fof(c177,plain,(![X52]:(~vehicle(X52)|transport(X52))),inference(variable_rename,[status(thm)],[c176])).
% 0.59/0.78 cnf(c178,plain,~vehicle(X119)|transport(X119),inference(split_conjunct,[status(thm)],[c177])).
% 0.59/0.78 cnf(c51,negated_conjecture,car(skolem0003),inference(split_conjunct,[status(thm)],[c46])).
% 0.59/0.78 fof(ax14,axiom,(![U]:(car(U)=>vehicle(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax14)).
% 0.59/0.78 fof(c179,plain,(![U]:(~car(U)|vehicle(U))),inference(fof_nnf,[status(thm)],[ax14])).
% 0.59/0.78 fof(c180,plain,(![X53]:(~car(X53)|vehicle(X53))),inference(variable_rename,[status(thm)],[c179])).
% 0.59/0.78 cnf(c181,plain,~car(X120)|vehicle(X120),inference(split_conjunct,[status(thm)],[c180])).
% 0.59/0.78 cnf(c277,plain,vehicle(skolem0003),inference(resolution,[status(thm)],[c181, c51])).
% 0.59/0.78 cnf(c278,plain,transport(skolem0003),inference(resolution,[status(thm)],[c277, c178])).
% 0.59/0.78 cnf(c279,plain,instrumentality(skolem0003),inference(resolution,[status(thm)],[c278, c175])).
% 0.59/0.78 cnf(c283,plain,artifact(skolem0003),inference(resolution,[status(thm)],[c279, c172])).
% 0.59/0.78 cnf(c284,plain,object(skolem0003),inference(resolution,[status(thm)],[c283, c169])).
% 0.59/0.78 cnf(c327,plain,~organism(skolem0003),inference(resolution,[status(thm)],[c211, c284])).
% 0.59/0.78 cnf(c56,negated_conjecture,way(skolem0004),inference(split_conjunct,[status(thm)],[c46])).
% 0.59/0.78 fof(ax11,axiom,(![U]:(way(U)=>artifact(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax11)).
% 0.59/0.78 fof(c189,plain,(![U]:(~way(U)|artifact(U))),inference(fof_nnf,[status(thm)],[ax11])).
% 0.59/0.78 fof(c190,plain,(![X56]:(~way(X56)|artifact(X56))),inference(variable_rename,[status(thm)],[c189])).
% 0.59/0.78 cnf(c191,plain,~way(X129)|artifact(X129),inference(split_conjunct,[status(thm)],[c190])).
% 0.59/0.78 cnf(c296,plain,artifact(skolem0004),inference(resolution,[status(thm)],[c191, c56])).
% 0.59/0.78 cnf(c297,plain,object(skolem0004),inference(resolution,[status(thm)],[c296, c169])).
% 0.59/0.78 cnf(c326,plain,~organism(skolem0004),inference(resolution,[status(thm)],[c211, c297])).
% 0.59/0.78 fof(ax37,axiom,(![U]:(human(U)=>(~nonhuman(U)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax37)).
% 0.59/0.78 fof(c99,plain,(![U]:(human(U)=>~nonhuman(U))),inference(fof_simplification,[status(thm)],[ax37])).
% 0.59/0.78 fof(c100,plain,(![U]:(~human(U)|~nonhuman(U))),inference(fof_nnf,[status(thm)],[c99])).
% 0.59/0.78 fof(c101,plain,(![X29]:(~human(X29)|~nonhuman(X29))),inference(variable_rename,[status(thm)],[c100])).
% 0.59/0.78 cnf(c102,plain,~human(X82)|~nonhuman(X82),inference(split_conjunct,[status(thm)],[c101])).
% 0.59/0.78 cnf(c63,negated_conjecture,front(skolem0007),inference(split_conjunct,[status(thm)],[c46])).
% 0.59/0.78 fof(ax6,axiom,(![U]:(front(U)=>nonhuman(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax6)).
% 0.59/0.78 fof(c205,plain,(![U]:(~front(U)|nonhuman(U))),inference(fof_nnf,[status(thm)],[ax6])).
% 0.59/0.78 fof(c206,plain,(![X61]:(~front(X61)|nonhuman(X61))),inference(variable_rename,[status(thm)],[c205])).
% 0.59/0.78 cnf(c207,plain,~front(X142)|nonhuman(X142),inference(split_conjunct,[status(thm)],[c206])).
% 0.59/0.78 cnf(c323,plain,nonhuman(skolem0007),inference(resolution,[status(thm)],[c207, c63])).
% 0.59/0.78 cnf(c325,plain,~human(skolem0007),inference(resolution,[status(thm)],[c323, c102])).
% 0.59/0.78 fof(ax7,axiom,(![U]:(seat(U)=>furniture(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax7)).
% 0.59/0.78 fof(c202,plain,(![U]:(~seat(U)|furniture(U))),inference(fof_nnf,[status(thm)],[ax7])).
% 0.59/0.78 fof(c203,plain,(![X60]:(~seat(X60)|furniture(X60))),inference(variable_rename,[status(thm)],[c202])).
% 0.59/0.78 cnf(c204,plain,~seat(X139)|furniture(X139),inference(split_conjunct,[status(thm)],[c203])).
% 0.59/0.78 fof(ax24,axiom,(![U]:(object(U)=>entity(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax24)).
% 0.59/0.78 fof(c148,plain,(![U]:(~object(U)|entity(U))),inference(fof_nnf,[status(thm)],[ax24])).
% 0.59/0.78 fof(c149,plain,(![X43]:(~object(X43)|entity(X43))),inference(variable_rename,[status(thm)],[c148])).
% 0.59/0.78 cnf(c150,plain,~object(X102)|entity(X102),inference(split_conjunct,[status(thm)],[c149])).
% 0.59/0.78 cnf(c313,plain,entity(skolem0007),inference(resolution,[status(thm)],[c312, c150])).
% 0.59/0.78 cnf(c318,plain,~abstraction(skolem0007),inference(resolution,[status(thm)],[c313, c139])).
% 0.59/0.78 cnf(c317,plain,~eventuality(skolem0007),inference(resolution,[status(thm)],[c313, c143])).
% 0.59/0.78 fof(ax12,axiom,(![U]:(way(U)=>(~instrumentality(U)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax12)).
% 0.59/0.78 fof(c185,plain,(![U]:(way(U)=>~instrumentality(U))),inference(fof_simplification,[status(thm)],[ax12])).
% 0.59/0.78 fof(c186,plain,(![U]:(~way(U)|~instrumentality(U))),inference(fof_nnf,[status(thm)],[c185])).
% 0.59/0.78 fof(c187,plain,(![X55]:(~way(X55)|~instrumentality(X55))),inference(variable_rename,[status(thm)],[c186])).
% 0.59/0.78 cnf(c188,plain,~way(X126)|~instrumentality(X126),inference(split_conjunct,[status(thm)],[c187])).
% 0.59/0.78 cnf(c311,plain,~way(skolem0007),inference(resolution,[status(thm)],[c309, c188])).
% 0.59/0.78 fof(ax9,axiom,(![U]:(furniture(U)=>(~transport(U)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax9)).
% 0.59/0.78 fof(c195,plain,(![U]:(furniture(U)=>~transport(U))),inference(fof_simplification,[status(thm)],[ax9])).
% 0.59/0.78 fof(c196,plain,(![U]:(~furniture(U)|~transport(U))),inference(fof_nnf,[status(thm)],[c195])).
% 0.59/0.78 fof(c197,plain,(![X58]:(~furniture(X58)|~transport(X58))),inference(variable_rename,[status(thm)],[c196])).
% 0.59/0.78 cnf(c198,plain,~furniture(X133)|~transport(X133),inference(split_conjunct,[status(thm)],[c197])).
% 0.59/0.78 cnf(c305,plain,~furniture(skolem0003),inference(resolution,[status(thm)],[c198, c278])).
% 0.59/0.78 fof(ax10,axiom,(![U]:(street(U)=>way(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax10)).
% 0.59/0.78 fof(c192,plain,(![U]:(~street(U)|way(U))),inference(fof_nnf,[status(thm)],[ax10])).
% 0.59/0.78 fof(c193,plain,(![X57]:(~street(X57)|way(X57))),inference(variable_rename,[status(thm)],[c192])).
% 0.59/0.78 cnf(c194,plain,~street(X132)|way(X132),inference(split_conjunct,[status(thm)],[c193])).
% 0.59/0.78 cnf(c298,plain,entity(skolem0004),inference(resolution,[status(thm)],[c297, c150])).
% 0.59/0.78 cnf(c300,plain,~abstraction(skolem0004),inference(resolution,[status(thm)],[c298, c139])).
% 0.59/0.78 cnf(c299,plain,~eventuality(skolem0004),inference(resolution,[status(thm)],[c298, c143])).
% 0.59/0.78 cnf(c292,plain,~way(skolem0003),inference(resolution,[status(thm)],[c188, c279])).
% 0.59/0.78 fof(ax13,axiom,(![U]:(chevy(U)=>car(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax13)).
% 0.59/0.78 fof(c182,plain,(![U]:(~chevy(U)|car(U))),inference(fof_nnf,[status(thm)],[ax13])).
% 0.59/0.78 fof(c183,plain,(![X54]:(~chevy(X54)|car(X54))),inference(variable_rename,[status(thm)],[c182])).
% 0.59/0.78 cnf(c184,plain,~chevy(X125)|car(X125),inference(split_conjunct,[status(thm)],[c183])).
% 0.59/0.78 cnf(c285,plain,entity(skolem0003),inference(resolution,[status(thm)],[c284, c150])).
% 0.59/0.78 cnf(c287,plain,~abstraction(skolem0003),inference(resolution,[status(thm)],[c285, c139])).
% 0.59/0.78 cnf(c286,plain,~eventuality(skolem0003),inference(resolution,[status(thm)],[c285, c143])).
% 0.59/0.78 fof(ax19,axiom,(![U]:(artifact(U)=>(~location(U)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax19)).
% 0.59/0.78 fof(c163,plain,(![U]:(artifact(U)=>~location(U))),inference(fof_simplification,[status(thm)],[ax19])).
% 0.59/0.78 fof(c164,plain,(![U]:(~artifact(U)|~location(U))),inference(fof_nnf,[status(thm)],[c163])).
% 0.59/0.78 fof(c165,plain,(![X48]:(~artifact(X48)|~location(X48))),inference(variable_rename,[status(thm)],[c164])).
% 0.59/0.78 cnf(c166,plain,~artifact(X113)|~location(X113),inference(split_conjunct,[status(thm)],[c165])).
% 0.59/0.78 cnf(c273,plain,~artifact(skolem0001),inference(resolution,[status(thm)],[c166, c259])).
% 0.59/0.78 fof(ax28,axiom,(![U]:(abstraction(U)=>(~eventuality(U)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax28)).
% 0.59/0.78 fof(c132,plain,(![U]:(abstraction(U)=>~eventuality(U))),inference(fof_simplification,[status(thm)],[ax28])).
% 0.59/0.78 fof(c133,plain,(![U]:(~abstraction(U)|~eventuality(U))),inference(fof_nnf,[status(thm)],[c132])).
% 0.59/0.78 fof(c134,plain,(![X39]:(~abstraction(X39)|~eventuality(X39))),inference(variable_rename,[status(thm)],[c133])).
% 0.59/0.78 cnf(c135,plain,~abstraction(X96)|~eventuality(X96),inference(split_conjunct,[status(thm)],[c134])).
% 0.59/0.78 cnf(c49,negated_conjecture,event(skolem0002),inference(split_conjunct,[status(thm)],[c46])).
% 0.59/0.78 fof(ax20,axiom,(![U]:(event(U)=>eventuality(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax20)).
% 0.59/0.78 fof(c160,plain,(![U]:(~event(U)|eventuality(U))),inference(fof_nnf,[status(thm)],[ax20])).
% 0.59/0.78 fof(c161,plain,(![X47]:(~event(X47)|eventuality(X47))),inference(variable_rename,[status(thm)],[c160])).
% 0.59/0.78 cnf(c162,plain,~event(X110)|eventuality(X110),inference(split_conjunct,[status(thm)],[c161])).
% 0.59/0.78 cnf(c268,plain,eventuality(skolem0002),inference(resolution,[status(thm)],[c162, c49])).
% 0.59/0.78 cnf(c269,plain,~abstraction(skolem0002),inference(resolution,[status(thm)],[c268, c135])).
% 0.59/0.78 fof(ax21,axiom,(![U]:(hollywood(U)=>city(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax21)).
% 0.59/0.78 fof(c157,plain,(![U]:(~hollywood(U)|city(U))),inference(fof_nnf,[status(thm)],[ax21])).
% 0.59/0.78 fof(c158,plain,(![X46]:(~hollywood(X46)|city(X46))),inference(variable_rename,[status(thm)],[c157])).
% 0.59/0.78 cnf(c159,plain,~hollywood(X109)|city(X109),inference(split_conjunct,[status(thm)],[c158])).
% 0.59/0.78 cnf(c261,plain,entity(skolem0001),inference(resolution,[status(thm)],[c260, c150])).
% 0.59/0.78 cnf(c263,plain,~abstraction(skolem0001),inference(resolution,[status(thm)],[c261, c139])).
% 0.59/0.78 cnf(c262,plain,~eventuality(skolem0001),inference(resolution,[status(thm)],[c261, c143])).
% 0.59/0.78 fof(ax25,axiom,(![U]:(old(U)=>(~new(U)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax25)).
% 0.59/0.78 fof(c144,plain,(![U]:(old(U)=>~new(U))),inference(fof_simplification,[status(thm)],[ax25])).
% 0.59/0.78 fof(c145,plain,(![U]:(~old(U)|~new(U))),inference(fof_nnf,[status(thm)],[c144])).
% 0.59/0.78 fof(c146,plain,(![X42]:(~old(X42)|~new(X42))),inference(variable_rename,[status(thm)],[c145])).
% 0.59/0.78 cnf(c147,plain,~old(X101)|~new(X101),inference(split_conjunct,[status(thm)],[c146])).
% 0.59/0.78 fof(ax29,axiom,(![U]:(male(U)=>(~female(U)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax29)).
% 0.59/0.78 fof(c128,plain,(![U]:(male(U)=>~female(U))),inference(fof_simplification,[status(thm)],[ax29])).
% 0.59/0.78 fof(c129,plain,(![U]:(~male(U)|~female(U))),inference(fof_nnf,[status(thm)],[c128])).
% 0.59/0.78 fof(c130,plain,(![X38]:(~male(X38)|~female(X38))),inference(variable_rename,[status(thm)],[c129])).
% 0.59/0.78 cnf(c131,plain,~male(X95)|~female(X95),inference(split_conjunct,[status(thm)],[c130])).
% 0.59/0.78 fof(ax30,axiom,(![U]:(man(U)=>(~woman(U)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax30)).
% 0.59/0.78 fof(c124,plain,(![U]:(man(U)=>~woman(U))),inference(fof_simplification,[status(thm)],[ax30])).
% 0.59/0.78 fof(c125,plain,(![U]:(~man(U)|~woman(U))),inference(fof_nnf,[status(thm)],[c124])).
% 0.59/0.78 fof(c126,plain,(![X37]:(~man(X37)|~woman(X37))),inference(variable_rename,[status(thm)],[c125])).
% 0.59/0.78 cnf(c127,plain,~man(X94)|~woman(X94),inference(split_conjunct,[status(thm)],[c126])).
% 0.59/0.78 fof(ax33,axiom,(![U]:(female(U)=>human(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax33)).
% 0.59/0.78 fof(c115,plain,(![U]:(~female(U)|human(U))),inference(fof_nnf,[status(thm)],[ax33])).
% 0.59/0.78 fof(c116,plain,(![X34]:(~female(X34)|human(X34))),inference(variable_rename,[status(thm)],[c115])).
% 0.59/0.78 cnf(c117,plain,~female(X89)|human(X89),inference(split_conjunct,[status(thm)],[c116])).
% 0.59/0.78 cnf(c4,axiom,X87!=X88|~entity(X87)|entity(X88),theory(equality)).
% 0.59/0.78 fof(ax34,axiom,(![U]:(woman(U)=>female(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax34)).
% 0.59/0.78 fof(c112,plain,(![U]:(~woman(U)|female(U))),inference(fof_nnf,[status(thm)],[ax34])).
% 0.59/0.78 fof(c113,plain,(![X33]:(~woman(X33)|female(X33))),inference(variable_rename,[status(thm)],[c112])).
% 0.59/0.78 cnf(c114,plain,~woman(X86)|female(X86),inference(split_conjunct,[status(thm)],[c113])).
% 0.59/0.78 fof(ax35,axiom,(![U]:(drs(U)<=>proposition(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax35)).
% 0.59/0.78 fof(c106,plain,(![U]:((~drs(U)|proposition(U))&(~proposition(U)|drs(U)))),inference(fof_nnf,[status(thm)],[ax35])).
% 0.59/0.78 fof(c107,plain,((![U]:(~drs(U)|proposition(U)))&(![U]:(~proposition(U)|drs(U)))),inference(shift_quantors,[status(thm)],[c106])).
% 0.59/0.78 fof(c109,plain,(![X31]:(![X32]:((~drs(X31)|proposition(X31))&(~proposition(X32)|drs(X32))))),inference(shift_quantors,[status(thm)],[fof(c108,plain,((![X31]:(~drs(X31)|proposition(X31)))&(![X32]:(~proposition(X32)|drs(X32)))),inference(variable_rename,[status(thm)],[c107])).])).
% 0.59/0.78 cnf(c111,plain,~proposition(X85)|drs(X85),inference(split_conjunct,[status(thm)],[c109])).
% 0.59/0.78 cnf(c110,plain,~drs(X84)|proposition(X84),inference(split_conjunct,[status(thm)],[c109])).
% 0.59/0.78 fof(ax36,axiom,(![U]:(nonhuman(U)=>entity(U))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax36)).
% 0.59/0.78 fof(c103,plain,(![U]:(~nonhuman(U)|entity(U))),inference(fof_nnf,[status(thm)],[ax36])).
% 0.59/0.78 fof(c104,plain,(![X30]:(~nonhuman(X30)|entity(X30))),inference(variable_rename,[status(thm)],[c103])).
% 0.59/0.78 cnf(c105,plain,~nonhuman(X83)|entity(X83),inference(split_conjunct,[status(thm)],[c104])).
% 0.59/0.78 cnf(c3,axiom,X80!=X81|~organism(X80)|organism(X81),theory(equality)).
% 0.59/0.78 cnf(c74,negated_conjecture,skolem0005!=skolem0006,inference(split_conjunct,[status(thm)],[c46])).
% 0.59/0.78 cnf(c2,axiom,X78!=X79|~human(X78)|human(X79),theory(equality)).
% 0.59/0.78 cnf(c61,negated_conjecture,seat(skolem0007),inference(split_conjunct,[status(thm)],[c46])).
% 0.59/0.78 cnf(c57,negated_conjecture,lonely(skolem0004),inference(split_conjunct,[status(thm)],[c46])).
% 0.59/0.78 cnf(c55,negated_conjecture,street(skolem0004),inference(split_conjunct,[status(thm)],[c46])).
% 0.59/0.78 cnf(c54,negated_conjecture,old(skolem0003),inference(split_conjunct,[status(thm)],[c46])).
% 0.59/0.78 cnf(c53,negated_conjecture,dirty(skolem0003),inference(split_conjunct,[status(thm)],[c46])).
% 0.59/0.78 cnf(c52,negated_conjecture,white(skolem0003),inference(split_conjunct,[status(thm)],[c46])).
% 0.59/0.78 cnf(c50,negated_conjecture,chevy(skolem0003),inference(split_conjunct,[status(thm)],[c46])).
% 0.59/0.78 cnf(c47,negated_conjecture,hollywood(skolem0001),inference(split_conjunct,[status(thm)],[c46])).
% 0.59/0.78 % SZS output end Saturation
% 0.59/0.78
% 0.59/0.78 % Initial clauses : 120
% 0.59/0.78 % Processed clauses : 322
% 0.59/0.78 % Factors computed : 2
% 0.59/0.78 % Resolvents computed: 302
% 0.59/0.78 % Tautologies deleted: 38
% 0.59/0.78 % Forward subsumed : 64
% 0.59/0.78 % Backward subsumed : 6
% 0.59/0.78 % -------- CPU Time ---------
% 0.59/0.78 % User time : 0.414 s
% 0.59/0.78 % System time : 0.018 s
% 0.59/0.78 % Total time : 0.432 s
%------------------------------------------------------------------------------