PyRes---1.5.CSA-Sat.s

%------------------------------------------------------------------------------
% File     : PyRes---1.5
% Problem  : NLP020+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s

% Computer : n007.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:38 EDT 2024

% Result   : CounterSatisfiable 0.78s 0.97s
% Output   : Saturation 0.83s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13  % Problem  : NLP020+1 : TPTP v8.1.2. Released v2.4.0.
% 0.03/0.14  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35  % Computer : n007.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:36:53 EDT 2024
% 0.13/0.35  % CPUTime  : 
% 0.78/0.97  % Version:  1.5
% 0.78/0.97  % SZS status CounterSatisfiable
% 0.78/0.97  % SZS output start Saturation
% 0.78/0.97  cnf(reflexivity,axiom,X67=X67,theory(equality)).
% 0.78/0.97  cnf(c35,axiom,X226!=X227|X225!=X228|~in(X226,X225)|in(X227,X228),theory(equality)).
% 0.78/0.97  cnf(symmetry,axiom,X69!=X68|X68=X69,theory(equality)).
% 0.78/0.97  fof(co1,conjecture,(![U]:(![V]:(![W]:(![X]:(![Y]:(![Z]:(![X1]:(![X3]:(![X4]:(((((((((((((((((((((((((((seat(U)&furniture(U))&front(U))&hollywood(V))&city(V))&event(W))&street(X))&way(X))&lonely(X))&chevy(Y))&car(Y))&white(Y))&dirty(Y))&old(Y))&barrel(W,Y))&down(W,X))&in(W,V))&fellow(Z))&man(Z))&young(Z))&fellow(X1))&man(X1))&young(X1))&Z=X3)&in(X3,U))&X1=X4)&in(X4,U))=>Z!=X1)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1)).
% 0.78/0.97  fof(c42,negated_conjecture,(~(![U]:(![V]:(![W]:(![X]:(![Y]:(![Z]:(![X1]:(![X3]:(![X4]:(((((((((((((((((((((((((((seat(U)&furniture(U))&front(U))&hollywood(V))&city(V))&event(W))&street(X))&way(X))&lonely(X))&chevy(Y))&car(Y))&white(Y))&dirty(Y))&old(Y))&barrel(W,Y))&down(W,X))&in(W,V))&fellow(Z))&man(Z))&young(Z))&fellow(X1))&man(X1))&young(X1))&Z=X3)&in(X3,U))&X1=X4)&in(X4,U))=>Z!=X1))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 0.78/0.97  fof(c43,negated_conjecture,(?[U]:(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:(?[X3]:(?[X4]:(((((((((((((((((((((((((((seat(U)&furniture(U))&front(U))&hollywood(V))&city(V))&event(W))&street(X))&way(X))&lonely(X))&chevy(Y))&car(Y))&white(Y))&dirty(Y))&old(Y))&barrel(W,Y))&down(W,X))&in(W,V))&fellow(Z))&man(Z))&young(Z))&fellow(X1))&man(X1))&young(X1))&Z=X3)&in(X3,U))&X1=X4)&in(X4,U))&Z=X1)))))))))),inference(fof_nnf,[status(thm)],[c42])).
% 0.78/0.97  fof(c44,negated_conjecture,(?[U]:(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X1]:((?[X3]:(?[X4]:((((((((((((((((((((((((((seat(U)&furniture(U))&front(U))&hollywood(V))&city(V))&event(W))&street(X))&way(X))&lonely(X))&chevy(Y))&car(Y))&white(Y))&dirty(Y))&old(Y))&barrel(W,Y))&down(W,X))&in(W,V))&fellow(Z))&man(Z))&young(Z))&fellow(X1))&man(X1))&young(X1))&Z=X3)&in(X3,U))&X1=X4)&in(X4,U))))&Z=X1)))))))),inference(shift_quantors,[status(thm)],[c43])).
% 0.78/0.97  fof(c45,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:((?[X9]:(?[X10]:((((((((((((((((((((((((((seat(X2)&furniture(X2))&front(X2))&hollywood(X3))&city(X3))&event(X4))&street(X5))&way(X5))&lonely(X5))&chevy(X6))&car(X6))&white(X6))&dirty(X6))&old(X6))&barrel(X4,X6))&down(X4,X5))&in(X4,X3))&fellow(X7))&man(X7))&young(X7))&fellow(X8))&man(X8))&young(X8))&X7=X9)&in(X9,X2))&X8=X10)&in(X10,X2))))&X7=X8)))))))),inference(variable_rename,[status(thm)],[c44])).
% 0.78/0.97  fof(c46,negated_conjecture,(((((((((((((((((((((((((((seat(skolem0001)&furniture(skolem0001))&front(skolem0001))&hollywood(skolem0002))&city(skolem0002))&event(skolem0003))&street(skolem0004))&way(skolem0004))&lonely(skolem0004))&chevy(skolem0005))&car(skolem0005))&white(skolem0005))&dirty(skolem0005))&old(skolem0005))&barrel(skolem0003,skolem0005))&down(skolem0003,skolem0004))&in(skolem0003,skolem0002))&fellow(skolem0006))&man(skolem0006))&young(skolem0006))&fellow(skolem0007))&man(skolem0007))&young(skolem0007))&skolem0006=skolem0008)&in(skolem0008,skolem0001))&skolem0007=skolem0009)&in(skolem0009,skolem0001))&skolem0006=skolem0007),inference(skolemize,[status(esa)],[c45])).
% 0.78/0.97  cnf(c74,negated_conjecture,skolem0006=skolem0007,inference(split_conjunct,[status(thm)],[c46])).
% 0.78/0.97  cnf(c244,plain,skolem0007=skolem0006,inference(resolution,[status(thm)],[c74, symmetry])).
% 0.78/0.97  cnf(transitivity,axiom,X72!=X71|X71!=X70|X72=X70,theory(equality)).
% 0.78/0.97  cnf(c70,negated_conjecture,skolem0006=skolem0008,inference(split_conjunct,[status(thm)],[c46])).
% 0.78/0.97  cnf(c231,plain,X273!=skolem0006|X273=skolem0008,inference(resolution,[status(thm)],[c70, transitivity])).
% 0.78/0.97  cnf(c573,plain,skolem0007=skolem0008,inference(resolution,[status(thm)],[c231, c244])).
% 0.78/0.97  cnf(c583,plain,skolem0008=skolem0007,inference(resolution,[status(thm)],[c573, symmetry])).
% 0.78/0.97  cnf(c71,negated_conjecture,in(skolem0008,skolem0001),inference(split_conjunct,[status(thm)],[c46])).
% 0.78/0.97  cnf(c538,plain,skolem0008!=X279|skolem0001!=X280|in(X279,X280),inference(resolution,[status(thm)],[c35, c71])).
% 0.78/0.97  cnf(c825,plain,skolem0008!=X297|in(X297,skolem0001),inference(resolution,[status(thm)],[c538, reflexivity])).
% 0.78/0.97  cnf(c858,plain,in(skolem0007,skolem0001),inference(resolution,[status(thm)],[c825, c583])).
% 0.78/0.97  cnf(c861,plain,skolem0007!=X305|skolem0001!=X306|in(X305,X306),inference(resolution,[status(thm)],[c858, c35])).
% 0.78/0.97  cnf(c873,plain,skolem0007!=X307|in(X307,skolem0001),inference(resolution,[status(thm)],[c861, reflexivity])).
% 0.78/0.97  cnf(c234,plain,skolem0008=skolem0006,inference(resolution,[status(thm)],[c70, symmetry])).
% 0.78/0.97  cnf(c857,plain,in(skolem0006,skolem0001),inference(resolution,[status(thm)],[c825, c234])).
% 0.78/0.97  cnf(c860,plain,skolem0006!=X302|skolem0001!=X303|in(X302,X303),inference(resolution,[status(thm)],[c857, c35])).
% 0.78/0.97  cnf(c868,plain,skolem0006!=X304|in(X304,skolem0001),inference(resolution,[status(thm)],[c860, reflexivity])).
% 0.78/0.97  cnf(c61,negated_conjecture,barrel(skolem0003,skolem0005),inference(split_conjunct,[status(thm)],[c46])).
% 0.78/0.97  cnf(c38,axiom,X237!=X238|X236!=X239|~barrel(X237,X236)|barrel(X238,X239),theory(equality)).
% 0.78/0.97  cnf(c549,plain,skolem0003!=X287|skolem0005!=X288|barrel(X287,X288),inference(resolution,[status(thm)],[c38, c61])).
% 0.78/0.97  cnf(c830,plain,skolem0003!=X301|barrel(X301,skolem0005),inference(resolution,[status(thm)],[c549, reflexivity])).
% 0.78/0.97  cnf(c62,negated_conjecture,down(skolem0003,skolem0004),inference(split_conjunct,[status(thm)],[c46])).
% 0.78/0.97  cnf(c37,axiom,X233!=X234|X232!=X235|~down(X233,X232)|down(X234,X235),theory(equality)).
% 0.78/0.97  cnf(c548,plain,skolem0003!=X286|skolem0004!=X285|down(X286,X285),inference(resolution,[status(thm)],[c37, c62])).
% 0.78/0.97  cnf(c829,plain,skolem0003!=X300|down(X300,skolem0004),inference(resolution,[status(thm)],[c548, reflexivity])).
% 0.78/0.97  cnf(c73,negated_conjecture,in(skolem0009,skolem0001),inference(split_conjunct,[status(thm)],[c46])).
% 0.78/0.97  cnf(c540,plain,skolem0009!=X283|skolem0001!=X284|in(X283,X284),inference(resolution,[status(thm)],[c35, c73])).
% 0.78/0.97  cnf(c828,plain,skolem0009!=X299|in(X299,skolem0001),inference(resolution,[status(thm)],[c540, reflexivity])).
% 0.78/0.97  cnf(c63,negated_conjecture,in(skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c46])).
% 0.78/0.97  cnf(c539,plain,skolem0003!=X281|skolem0002!=X282|in(X281,X282),inference(resolution,[status(thm)],[c35, c63])).
% 0.78/0.97  cnf(c827,plain,skolem0003!=X298|in(X298,skolem0002),inference(resolution,[status(thm)],[c539, reflexivity])).
% 0.78/0.97  cnf(c16,axiom,X137!=X138|~car(X137)|car(X138),theory(equality)).
% 0.78/0.97  cnf(c72,negated_conjecture,skolem0007=skolem0009,inference(split_conjunct,[status(thm)],[c46])).
% 0.78/0.97  cnf(c236,plain,X274!=skolem0007|X274=skolem0009,inference(resolution,[status(thm)],[c72, transitivity])).
% 0.78/0.97  cnf(c654,plain,skolem0008=skolem0009,inference(resolution,[status(thm)],[c236, c583])).
% 0.78/0.97  cnf(c701,plain,skolem0009=skolem0008,inference(resolution,[status(thm)],[c654, symmetry])).
% 0.78/0.97  cnf(c810,plain,~car(skolem0009)|car(skolem0008),inference(resolution,[status(thm)],[c701, c16])).
% 0.78/0.97  cnf(c5,axiom,X92!=X93|~object(X92)|object(X93),theory(equality)).
% 0.78/0.97  cnf(c809,plain,~object(skolem0009)|object(skolem0008),inference(resolution,[status(thm)],[c701, c5])).
% 0.78/0.97  cnf(c11,axiom,X121!=X122|~transport(X121)|transport(X122),theory(equality)).
% 0.78/0.97  cnf(c808,plain,~transport(skolem0009)|transport(skolem0008),inference(resolution,[status(thm)],[c701, c11])).
% 0.78/0.97  cnf(c8,axiom,X107!=X108|~seat(X107)|seat(X108),theory(equality)).
% 0.78/0.97  cnf(c807,plain,~seat(skolem0009)|seat(skolem0008),inference(resolution,[status(thm)],[c701, c8])).
% 0.78/0.97  cnf(c15,axiom,X134!=X135|~chevy(X134)|chevy(X135),theory(equality)).
% 0.78/0.97  cnf(c806,plain,~chevy(skolem0009)|chevy(skolem0008),inference(resolution,[status(thm)],[c701, c15])).
% 0.78/0.97  cnf(c32,axiom,X214!=X215|~owner(X214)|owner(X215),theory(equality)).
% 0.78/0.97  cnf(c805,plain,~owner(skolem0009)|owner(skolem0008),inference(resolution,[status(thm)],[c701, c32])).
% 0.78/0.97  cnf(c19,axiom,X147!=X148|~event(X147)|event(X148),theory(equality)).
% 0.78/0.97  cnf(c804,plain,~event(skolem0009)|event(skolem0008),inference(resolution,[status(thm)],[c701, c19])).
% 0.78/0.97  cnf(c29,axiom,X199!=X200|~drs(X199)|drs(X200),theory(equality)).
% 0.78/0.97  cnf(c803,plain,~drs(skolem0009)|drs(skolem0008),inference(resolution,[status(thm)],[c701, c29])).
% 0.78/0.97  cnf(c6,axiom,X97!=X98|~front(X97)|front(X98),theory(equality)).
% 0.78/0.97  cnf(c802,plain,~front(skolem0009)|front(skolem0008),inference(resolution,[status(thm)],[c701, c6])).
% 0.78/0.97  cnf(c796,plain,X296!=skolem0009|X296=skolem0008,inference(resolution,[status(thm)],[c701, transitivity])).
% 0.78/0.97  cnf(c17,axiom,X140!=X141|~vehicle(X140)|vehicle(X141),theory(equality)).
% 0.78/0.97  cnf(c800,plain,~vehicle(skolem0009)|vehicle(skolem0008),inference(resolution,[status(thm)],[c701, c17])).
% 0.78/0.97  cnf(c12,axiom,X123!=X124|~street(X123)|street(X124),theory(equality)).
% 0.78/0.97  cnf(c799,plain,~street(skolem0009)|street(skolem0008),inference(resolution,[status(thm)],[c701, c12])).
% 0.78/0.97  cnf(c27,axiom,X188!=X189|~female(X188)|female(X189),theory(equality)).
% 0.78/0.97  cnf(c797,plain,~female(skolem0009)|female(skolem0008),inference(resolution,[status(thm)],[c701, c27])).
% 0.78/0.97  cnf(c39,axiom,X240!=X241|~dirty(X240)|dirty(X241),theory(equality)).
% 0.78/0.97  cnf(c795,plain,~dirty(skolem0009)|dirty(skolem0008),inference(resolution,[status(thm)],[c701, c39])).
% 0.78/0.97  cnf(c40,axiom,X243!=X244|~white(X243)|white(X244),theory(equality)).
% 0.78/0.97  cnf(c794,plain,~white(skolem0009)|white(skolem0008),inference(resolution,[status(thm)],[c701, c40])).
% 0.78/0.97  cnf(c41,axiom,X246!=X247|~lonely(X246)|lonely(X247),theory(equality)).
% 0.78/0.97  cnf(c793,plain,~lonely(skolem0009)|lonely(skolem0008),inference(resolution,[status(thm)],[c701, c41])).
% 0.78/0.97  cnf(c24,axiom,X167!=X168|~new(X167)|new(X168),theory(equality)).
% 0.78/0.97  cnf(c792,plain,~new(skolem0009)|new(skolem0008),inference(resolution,[status(thm)],[c701, c24])).
% 0.78/0.97  cnf(c7,axiom,X104!=X105|~nonhuman(X104)|nonhuman(X105),theory(equality)).
% 0.78/0.97  cnf(c791,plain,~nonhuman(skolem0009)|nonhuman(skolem0008),inference(resolution,[status(thm)],[c701, c7])).
% 0.78/0.97  cnf(c18,axiom,X144!=X145|~location(X144)|location(X145),theory(equality)).
% 0.78/0.97  cnf(c790,plain,~location(skolem0009)|location(skolem0008),inference(resolution,[status(thm)],[c701, c18])).
% 0.78/0.97  cnf(c23,axiom,X161!=X162|~old(X161)|old(X162),theory(equality)).
% 0.78/0.97  cnf(c788,plain,~old(skolem0009)|old(skolem0008),inference(resolution,[status(thm)],[c701, c23])).
% 0.78/0.97  cnf(c30,axiom,X205!=X206|~proposition(X205)|proposition(X206),theory(equality)).
% 0.78/0.97  cnf(c786,plain,~proposition(skolem0009)|proposition(skolem0008),inference(resolution,[status(thm)],[c701, c30])).
% 0.78/0.97  cnf(c13,axiom,X127!=X128|~way(X127)|way(X128),theory(equality)).
% 0.78/0.97  cnf(c784,plain,~way(skolem0009)|way(skolem0008),inference(resolution,[status(thm)],[c701, c13])).
% 0.78/0.97  cnf(c28,axiom,X192!=X193|~woman(X192)|woman(X193),theory(equality)).
% 0.78/0.97  cnf(c781,plain,~woman(skolem0009)|woman(skolem0008),inference(resolution,[status(thm)],[c701, c28])).
% 0.78/0.97  cnf(c9,axiom,X111!=X112|~furniture(X111)|furniture(X112),theory(equality)).
% 0.78/0.97  cnf(c780,plain,~furniture(skolem0009)|furniture(skolem0008),inference(resolution,[status(thm)],[c701, c9])).
% 0.78/0.97  cnf(c21,axiom,X153!=X154|~hollywood(X153)|hollywood(X154),theory(equality)).
% 0.78/0.97  cnf(c779,plain,~hollywood(skolem0009)|hollywood(skolem0008),inference(resolution,[status(thm)],[c701, c21])).
% 0.78/0.97  cnf(c22,axiom,X156!=X157|~city(X156)|city(X157),theory(equality)).
% 0.78/0.97  cnf(c778,plain,~city(skolem0009)|city(skolem0008),inference(resolution,[status(thm)],[c701, c22])).
% 0.78/0.97  cnf(c10,axiom,X116!=X117|~instrumentality(X116)|instrumentality(X117),theory(equality)).
% 0.78/0.97  cnf(c777,plain,~instrumentality(skolem0009)|instrumentality(skolem0008),inference(resolution,[status(thm)],[c701, c10])).
% 0.78/0.97  cnf(c14,axiom,X130!=X131|~artifact(X130)|artifact(X131),theory(equality)).
% 0.78/0.97  cnf(c774,plain,~artifact(skolem0009)|artifact(skolem0008),inference(resolution,[status(thm)],[c701, c14])).
% 0.78/0.97  cnf(c652,plain,skolem0006=skolem0009,inference(resolution,[status(thm)],[c236, c74])).
% 0.78/0.97  cnf(c663,plain,skolem0009=skolem0006,inference(resolution,[status(thm)],[c652, symmetry])).
% 0.78/0.97  cnf(c768,plain,~car(skolem0009)|car(skolem0006),inference(resolution,[status(thm)],[c663, c16])).
% 0.78/0.97  cnf(c767,plain,~object(skolem0009)|object(skolem0006),inference(resolution,[status(thm)],[c663, c5])).
% 0.78/0.97  cnf(c766,plain,~transport(skolem0009)|transport(skolem0006),inference(resolution,[status(thm)],[c663, c11])).
% 0.78/0.97  cnf(c765,plain,~seat(skolem0009)|seat(skolem0006),inference(resolution,[status(thm)],[c663, c8])).
% 0.78/0.97  cnf(c763,plain,~chevy(skolem0009)|chevy(skolem0006),inference(resolution,[status(thm)],[c663, c15])).
% 0.78/0.97  cnf(c762,plain,~owner(skolem0009)|owner(skolem0006),inference(resolution,[status(thm)],[c663, c32])).
% 0.78/0.97  cnf(c761,plain,~event(skolem0009)|event(skolem0006),inference(resolution,[status(thm)],[c663, c19])).
% 0.78/0.97  cnf(c760,plain,~drs(skolem0009)|drs(skolem0006),inference(resolution,[status(thm)],[c663, c29])).
% 0.78/0.97  cnf(c759,plain,~front(skolem0009)|front(skolem0006),inference(resolution,[status(thm)],[c663, c6])).
% 0.78/0.97  cnf(c753,plain,X295!=skolem0009|X295=skolem0006,inference(resolution,[status(thm)],[c663, transitivity])).
% 0.78/0.97  cnf(c757,plain,~vehicle(skolem0009)|vehicle(skolem0006),inference(resolution,[status(thm)],[c663, c17])).
% 0.78/0.97  cnf(c756,plain,~street(skolem0009)|street(skolem0006),inference(resolution,[status(thm)],[c663, c12])).
% 0.78/0.97  cnf(c754,plain,~female(skolem0009)|female(skolem0006),inference(resolution,[status(thm)],[c663, c27])).
% 0.78/0.97  cnf(c752,plain,~dirty(skolem0009)|dirty(skolem0006),inference(resolution,[status(thm)],[c663, c39])).
% 0.78/0.97  cnf(c751,plain,~white(skolem0009)|white(skolem0006),inference(resolution,[status(thm)],[c663, c40])).
% 0.78/0.97  cnf(c750,plain,~lonely(skolem0009)|lonely(skolem0006),inference(resolution,[status(thm)],[c663, c41])).
% 0.78/0.97  cnf(c749,plain,~new(skolem0009)|new(skolem0006),inference(resolution,[status(thm)],[c663, c24])).
% 0.78/0.97  cnf(c748,plain,~nonhuman(skolem0009)|nonhuman(skolem0006),inference(resolution,[status(thm)],[c663, c7])).
% 0.78/0.97  cnf(c747,plain,~location(skolem0009)|location(skolem0006),inference(resolution,[status(thm)],[c663, c18])).
% 0.78/0.97  cnf(c745,plain,~old(skolem0009)|old(skolem0006),inference(resolution,[status(thm)],[c663, c23])).
% 0.78/0.97  cnf(c743,plain,~proposition(skolem0009)|proposition(skolem0006),inference(resolution,[status(thm)],[c663, c30])).
% 0.78/0.97  cnf(c741,plain,~way(skolem0009)|way(skolem0006),inference(resolution,[status(thm)],[c663, c13])).
% 0.78/0.97  cnf(c738,plain,~woman(skolem0009)|woman(skolem0006),inference(resolution,[status(thm)],[c663, c28])).
% 0.78/0.97  cnf(c737,plain,~furniture(skolem0009)|furniture(skolem0006),inference(resolution,[status(thm)],[c663, c9])).
% 0.78/0.97  cnf(c736,plain,~hollywood(skolem0009)|hollywood(skolem0006),inference(resolution,[status(thm)],[c663, c21])).
% 0.78/0.97  cnf(c735,plain,~city(skolem0009)|city(skolem0006),inference(resolution,[status(thm)],[c663, c22])).
% 0.78/0.97  cnf(c734,plain,~instrumentality(skolem0009)|instrumentality(skolem0006),inference(resolution,[status(thm)],[c663, c10])).
% 0.78/0.97  cnf(c731,plain,~artifact(skolem0009)|artifact(skolem0006),inference(resolution,[status(thm)],[c663, c14])).
% 0.78/0.97  cnf(c729,plain,~car(skolem0008)|car(skolem0009),inference(resolution,[status(thm)],[c654, c16])).
% 0.78/0.97  cnf(c728,plain,~object(skolem0008)|object(skolem0009),inference(resolution,[status(thm)],[c654, c5])).
% 0.78/0.97  cnf(c727,plain,~transport(skolem0008)|transport(skolem0009),inference(resolution,[status(thm)],[c654, c11])).
% 0.78/0.97  cnf(c726,plain,~seat(skolem0008)|seat(skolem0009),inference(resolution,[status(thm)],[c654, c8])).
% 0.78/0.97  cnf(c725,plain,~chevy(skolem0008)|chevy(skolem0009),inference(resolution,[status(thm)],[c654, c15])).
% 0.78/0.97  cnf(c724,plain,~owner(skolem0008)|owner(skolem0009),inference(resolution,[status(thm)],[c654, c32])).
% 0.78/0.97  cnf(c723,plain,~event(skolem0008)|event(skolem0009),inference(resolution,[status(thm)],[c654, c19])).
% 0.78/0.97  cnf(c722,plain,~drs(skolem0008)|drs(skolem0009),inference(resolution,[status(thm)],[c654, c29])).
% 0.78/0.97  cnf(c721,plain,~front(skolem0008)|front(skolem0009),inference(resolution,[status(thm)],[c654, c6])).
% 0.78/0.97  cnf(c719,plain,~vehicle(skolem0008)|vehicle(skolem0009),inference(resolution,[status(thm)],[c654, c17])).
% 0.78/0.97  cnf(c715,plain,X294!=skolem0008|X294=skolem0009,inference(resolution,[status(thm)],[c654, transitivity])).
% 0.78/0.97  cnf(c718,plain,~street(skolem0008)|street(skolem0009),inference(resolution,[status(thm)],[c654, c12])).
% 0.78/0.97  cnf(c716,plain,~female(skolem0008)|female(skolem0009),inference(resolution,[status(thm)],[c654, c27])).
% 0.78/0.97  cnf(c714,plain,~dirty(skolem0008)|dirty(skolem0009),inference(resolution,[status(thm)],[c654, c39])).
% 0.78/0.97  cnf(c713,plain,~white(skolem0008)|white(skolem0009),inference(resolution,[status(thm)],[c654, c40])).
% 0.78/0.97  cnf(c712,plain,~lonely(skolem0008)|lonely(skolem0009),inference(resolution,[status(thm)],[c654, c41])).
% 0.78/0.97  cnf(c711,plain,~new(skolem0008)|new(skolem0009),inference(resolution,[status(thm)],[c654, c24])).
% 0.78/0.97  cnf(c710,plain,~nonhuman(skolem0008)|nonhuman(skolem0009),inference(resolution,[status(thm)],[c654, c7])).
% 0.78/0.97  cnf(c709,plain,~location(skolem0008)|location(skolem0009),inference(resolution,[status(thm)],[c654, c18])).
% 0.78/0.97  cnf(c707,plain,~old(skolem0008)|old(skolem0009),inference(resolution,[status(thm)],[c654, c23])).
% 0.78/0.97  cnf(c705,plain,~proposition(skolem0008)|proposition(skolem0009),inference(resolution,[status(thm)],[c654, c30])).
% 0.78/0.97  cnf(c703,plain,~way(skolem0008)|way(skolem0009),inference(resolution,[status(thm)],[c654, c13])).
% 0.78/0.97  cnf(c700,plain,~woman(skolem0008)|woman(skolem0009),inference(resolution,[status(thm)],[c654, c28])).
% 0.78/0.97  cnf(c699,plain,~furniture(skolem0008)|furniture(skolem0009),inference(resolution,[status(thm)],[c654, c9])).
% 0.78/0.97  cnf(c698,plain,~hollywood(skolem0008)|hollywood(skolem0009),inference(resolution,[status(thm)],[c654, c21])).
% 0.78/0.97  cnf(c697,plain,~city(skolem0008)|city(skolem0009),inference(resolution,[status(thm)],[c654, c22])).
% 0.78/0.97  cnf(c696,plain,~instrumentality(skolem0008)|instrumentality(skolem0009),inference(resolution,[status(thm)],[c654, c10])).
% 0.78/0.97  cnf(c693,plain,~artifact(skolem0008)|artifact(skolem0009),inference(resolution,[status(thm)],[c654, c14])).
% 0.78/0.97  cnf(c691,plain,~car(skolem0006)|car(skolem0009),inference(resolution,[status(thm)],[c652, c16])).
% 0.78/0.97  cnf(c690,plain,~object(skolem0006)|object(skolem0009),inference(resolution,[status(thm)],[c652, c5])).
% 0.78/0.97  cnf(c689,plain,~transport(skolem0006)|transport(skolem0009),inference(resolution,[status(thm)],[c652, c11])).
% 0.78/0.97  cnf(c688,plain,~seat(skolem0006)|seat(skolem0009),inference(resolution,[status(thm)],[c652, c8])).
% 0.78/0.97  cnf(c687,plain,~chevy(skolem0006)|chevy(skolem0009),inference(resolution,[status(thm)],[c652, c15])).
% 0.78/0.97  cnf(c686,plain,~owner(skolem0006)|owner(skolem0009),inference(resolution,[status(thm)],[c652, c32])).
% 0.78/0.97  cnf(c685,plain,~event(skolem0006)|event(skolem0009),inference(resolution,[status(thm)],[c652, c19])).
% 0.78/0.97  cnf(c684,plain,~drs(skolem0006)|drs(skolem0009),inference(resolution,[status(thm)],[c652, c29])).
% 0.78/0.97  cnf(c683,plain,~front(skolem0006)|front(skolem0009),inference(resolution,[status(thm)],[c652, c6])).
% 0.78/0.97  cnf(c681,plain,~vehicle(skolem0006)|vehicle(skolem0009),inference(resolution,[status(thm)],[c652, c17])).
% 0.78/0.97  cnf(c680,plain,~street(skolem0006)|street(skolem0009),inference(resolution,[status(thm)],[c652, c12])).
% 0.78/0.97  cnf(c677,plain,X293!=skolem0006|X293=skolem0009,inference(resolution,[status(thm)],[c652, transitivity])).
% 0.78/0.97  cnf(c678,plain,~female(skolem0006)|female(skolem0009),inference(resolution,[status(thm)],[c652, c27])).
% 0.78/0.97  cnf(c676,plain,~dirty(skolem0006)|dirty(skolem0009),inference(resolution,[status(thm)],[c652, c39])).
% 0.78/0.97  cnf(c675,plain,~white(skolem0006)|white(skolem0009),inference(resolution,[status(thm)],[c652, c40])).
% 0.78/0.97  cnf(c674,plain,~lonely(skolem0006)|lonely(skolem0009),inference(resolution,[status(thm)],[c652, c41])).
% 0.78/0.97  cnf(c673,plain,~new(skolem0006)|new(skolem0009),inference(resolution,[status(thm)],[c652, c24])).
% 0.78/0.97  cnf(c672,plain,~nonhuman(skolem0006)|nonhuman(skolem0009),inference(resolution,[status(thm)],[c652, c7])).
% 0.78/0.97  cnf(c671,plain,~location(skolem0006)|location(skolem0009),inference(resolution,[status(thm)],[c652, c18])).
% 0.78/0.97  cnf(c669,plain,~old(skolem0006)|old(skolem0009),inference(resolution,[status(thm)],[c652, c23])).
% 0.78/0.97  cnf(c667,plain,~proposition(skolem0006)|proposition(skolem0009),inference(resolution,[status(thm)],[c652, c30])).
% 0.78/0.97  cnf(c665,plain,~way(skolem0006)|way(skolem0009),inference(resolution,[status(thm)],[c652, c13])).
% 0.78/0.97  cnf(c662,plain,~woman(skolem0006)|woman(skolem0009),inference(resolution,[status(thm)],[c652, c28])).
% 0.78/0.97  cnf(c661,plain,~furniture(skolem0006)|furniture(skolem0009),inference(resolution,[status(thm)],[c652, c9])).
% 0.78/0.97  cnf(c660,plain,~hollywood(skolem0006)|hollywood(skolem0009),inference(resolution,[status(thm)],[c652, c21])).
% 0.78/0.97  cnf(c659,plain,~city(skolem0006)|city(skolem0009),inference(resolution,[status(thm)],[c652, c22])).
% 0.78/0.97  cnf(c658,plain,~instrumentality(skolem0006)|instrumentality(skolem0009),inference(resolution,[status(thm)],[c652, c10])).
% 0.78/0.97  cnf(c655,plain,~artifact(skolem0006)|artifact(skolem0009),inference(resolution,[status(thm)],[c652, c14])).
% 0.78/0.97  cnf(c649,plain,~car(skolem0008)|car(skolem0007),inference(resolution,[status(thm)],[c583, c16])).
% 0.78/0.97  cnf(c648,plain,~object(skolem0008)|object(skolem0007),inference(resolution,[status(thm)],[c583, c5])).
% 0.78/0.97  cnf(c647,plain,~transport(skolem0008)|transport(skolem0007),inference(resolution,[status(thm)],[c583, c11])).
% 0.78/0.97  cnf(c646,plain,~seat(skolem0008)|seat(skolem0007),inference(resolution,[status(thm)],[c583, c8])).
% 0.78/0.97  cnf(c645,plain,~chevy(skolem0008)|chevy(skolem0007),inference(resolution,[status(thm)],[c583, c15])).
% 0.78/0.97  cnf(c644,plain,~owner(skolem0008)|owner(skolem0007),inference(resolution,[status(thm)],[c583, c32])).
% 0.78/0.97  cnf(c643,plain,~event(skolem0008)|event(skolem0007),inference(resolution,[status(thm)],[c583, c19])).
% 0.78/0.97  cnf(c642,plain,~drs(skolem0008)|drs(skolem0007),inference(resolution,[status(thm)],[c583, c29])).
% 0.78/0.97  cnf(c641,plain,~front(skolem0008)|front(skolem0007),inference(resolution,[status(thm)],[c583, c6])).
% 0.78/0.97  cnf(c639,plain,~vehicle(skolem0008)|vehicle(skolem0007),inference(resolution,[status(thm)],[c583, c17])).
% 0.78/0.97  cnf(c638,plain,~street(skolem0008)|street(skolem0007),inference(resolution,[status(thm)],[c583, c12])).
% 0.78/0.97  cnf(c635,plain,X292!=skolem0008|X292=skolem0007,inference(resolution,[status(thm)],[c583, transitivity])).
% 0.78/0.97  cnf(c636,plain,~female(skolem0008)|female(skolem0007),inference(resolution,[status(thm)],[c583, c27])).
% 0.78/0.97  cnf(c634,plain,~dirty(skolem0008)|dirty(skolem0007),inference(resolution,[status(thm)],[c583, c39])).
% 0.78/0.97  cnf(c633,plain,~white(skolem0008)|white(skolem0007),inference(resolution,[status(thm)],[c583, c40])).
% 0.78/0.97  cnf(c632,plain,~lonely(skolem0008)|lonely(skolem0007),inference(resolution,[status(thm)],[c583, c41])).
% 0.78/0.97  cnf(c631,plain,~new(skolem0008)|new(skolem0007),inference(resolution,[status(thm)],[c583, c24])).
% 0.78/0.97  cnf(c630,plain,~nonhuman(skolem0008)|nonhuman(skolem0007),inference(resolution,[status(thm)],[c583, c7])).
% 0.78/0.97  cnf(c629,plain,~location(skolem0008)|location(skolem0007),inference(resolution,[status(thm)],[c583, c18])).
% 0.78/0.97  cnf(c627,plain,~old(skolem0008)|old(skolem0007),inference(resolution,[status(thm)],[c583, c23])).
% 0.78/0.97  cnf(c625,plain,~proposition(skolem0008)|proposition(skolem0007),inference(resolution,[status(thm)],[c583, c30])).
% 0.78/0.97  cnf(c623,plain,~way(skolem0008)|way(skolem0007),inference(resolution,[status(thm)],[c583, c13])).
% 0.78/0.97  cnf(c620,plain,~woman(skolem0008)|woman(skolem0007),inference(resolution,[status(thm)],[c583, c28])).
% 0.78/0.97  cnf(c619,plain,~furniture(skolem0008)|furniture(skolem0007),inference(resolution,[status(thm)],[c583, c9])).
% 0.78/0.97  cnf(c618,plain,~hollywood(skolem0008)|hollywood(skolem0007),inference(resolution,[status(thm)],[c583, c21])).
% 0.78/0.97  cnf(c617,plain,~city(skolem0008)|city(skolem0007),inference(resolution,[status(thm)],[c583, c22])).
% 0.78/0.97  cnf(c616,plain,~instrumentality(skolem0008)|instrumentality(skolem0007),inference(resolution,[status(thm)],[c583, c10])).
% 0.78/0.97  cnf(c613,plain,~artifact(skolem0008)|artifact(skolem0007),inference(resolution,[status(thm)],[c583, c14])).
% 0.78/0.97  cnf(c611,plain,~car(skolem0007)|car(skolem0008),inference(resolution,[status(thm)],[c573, c16])).
% 0.78/0.97  cnf(c610,plain,~object(skolem0007)|object(skolem0008),inference(resolution,[status(thm)],[c573, c5])).
% 0.78/0.97  cnf(c609,plain,~transport(skolem0007)|transport(skolem0008),inference(resolution,[status(thm)],[c573, c11])).
% 0.78/0.97  cnf(c608,plain,~seat(skolem0007)|seat(skolem0008),inference(resolution,[status(thm)],[c573, c8])).
% 0.78/0.97  cnf(c607,plain,~chevy(skolem0007)|chevy(skolem0008),inference(resolution,[status(thm)],[c573, c15])).
% 0.78/0.97  cnf(c606,plain,~owner(skolem0007)|owner(skolem0008),inference(resolution,[status(thm)],[c573, c32])).
% 0.78/0.97  cnf(c605,plain,~event(skolem0007)|event(skolem0008),inference(resolution,[status(thm)],[c573, c19])).
% 0.78/0.97  cnf(c604,plain,~drs(skolem0007)|drs(skolem0008),inference(resolution,[status(thm)],[c573, c29])).
% 0.78/0.97  cnf(c603,plain,~front(skolem0007)|front(skolem0008),inference(resolution,[status(thm)],[c573, c6])).
% 0.78/0.97  cnf(c601,plain,~vehicle(skolem0007)|vehicle(skolem0008),inference(resolution,[status(thm)],[c573, c17])).
% 0.78/0.97  cnf(c600,plain,~street(skolem0007)|street(skolem0008),inference(resolution,[status(thm)],[c573, c12])).
% 0.78/0.97  cnf(c598,plain,~female(skolem0007)|female(skolem0008),inference(resolution,[status(thm)],[c573, c27])).
% 0.78/0.97  cnf(c597,plain,X291!=skolem0007|X291=skolem0008,inference(resolution,[status(thm)],[c573, transitivity])).
% 0.78/0.98  cnf(c596,plain,~dirty(skolem0007)|dirty(skolem0008),inference(resolution,[status(thm)],[c573, c39])).
% 0.78/0.98  cnf(c595,plain,~white(skolem0007)|white(skolem0008),inference(resolution,[status(thm)],[c573, c40])).
% 0.78/0.98  cnf(c594,plain,~lonely(skolem0007)|lonely(skolem0008),inference(resolution,[status(thm)],[c573, c41])).
% 0.78/0.98  cnf(c593,plain,~new(skolem0007)|new(skolem0008),inference(resolution,[status(thm)],[c573, c24])).
% 0.78/0.98  cnf(c592,plain,~nonhuman(skolem0007)|nonhuman(skolem0008),inference(resolution,[status(thm)],[c573, c7])).
% 0.78/0.98  cnf(c591,plain,~location(skolem0007)|location(skolem0008),inference(resolution,[status(thm)],[c573, c18])).
% 0.78/0.98  cnf(c589,plain,~old(skolem0007)|old(skolem0008),inference(resolution,[status(thm)],[c573, c23])).
% 0.78/0.98  cnf(c587,plain,~proposition(skolem0007)|proposition(skolem0008),inference(resolution,[status(thm)],[c573, c30])).
% 0.78/0.98  cnf(c585,plain,~way(skolem0007)|way(skolem0008),inference(resolution,[status(thm)],[c573, c13])).
% 0.78/0.98  cnf(c582,plain,~woman(skolem0007)|woman(skolem0008),inference(resolution,[status(thm)],[c573, c28])).
% 0.78/0.98  cnf(c581,plain,~furniture(skolem0007)|furniture(skolem0008),inference(resolution,[status(thm)],[c573, c9])).
% 0.78/0.98  cnf(c580,plain,~hollywood(skolem0007)|hollywood(skolem0008),inference(resolution,[status(thm)],[c573, c21])).
% 0.78/0.98  cnf(c579,plain,~city(skolem0007)|city(skolem0008),inference(resolution,[status(thm)],[c573, c22])).
% 0.78/0.98  cnf(c578,plain,~instrumentality(skolem0007)|instrumentality(skolem0008),inference(resolution,[status(thm)],[c573, c10])).
% 0.78/0.98  cnf(c575,plain,~artifact(skolem0007)|artifact(skolem0008),inference(resolution,[status(thm)],[c573, c14])).
% 0.78/0.98  cnf(c570,plain,~lonely(skolem0006)|lonely(skolem0008),inference(resolution,[status(thm)],[c41, c70])).
% 0.78/0.98  cnf(c239,plain,skolem0009=skolem0007,inference(resolution,[status(thm)],[c72, symmetry])).
% 0.78/0.98  cnf(c569,plain,~lonely(skolem0009)|lonely(skolem0007),inference(resolution,[status(thm)],[c41, c239])).
% 0.78/0.98  cnf(c568,plain,~lonely(skolem0008)|lonely(skolem0006),inference(resolution,[status(thm)],[c41, c234])).
% 0.78/0.98  cnf(c567,plain,~lonely(skolem0007)|lonely(skolem0009),inference(resolution,[status(thm)],[c41, c72])).
% 0.78/0.98  cnf(c566,plain,~lonely(skolem0006)|lonely(skolem0007),inference(resolution,[status(thm)],[c41, c74])).
% 0.78/0.98  cnf(c565,plain,~lonely(skolem0007)|lonely(skolem0006),inference(resolution,[status(thm)],[c41, c244])).
% 0.78/0.98  cnf(c563,plain,~white(skolem0006)|white(skolem0008),inference(resolution,[status(thm)],[c40, c70])).
% 0.78/0.98  cnf(c562,plain,~white(skolem0009)|white(skolem0007),inference(resolution,[status(thm)],[c40, c239])).
% 0.78/0.98  cnf(c561,plain,~white(skolem0008)|white(skolem0006),inference(resolution,[status(thm)],[c40, c234])).
% 0.78/0.98  cnf(c560,plain,~white(skolem0007)|white(skolem0009),inference(resolution,[status(thm)],[c40, c72])).
% 0.78/0.98  cnf(c559,plain,~white(skolem0006)|white(skolem0007),inference(resolution,[status(thm)],[c40, c74])).
% 0.78/0.98  cnf(c558,plain,~white(skolem0007)|white(skolem0006),inference(resolution,[status(thm)],[c40, c244])).
% 0.78/0.98  cnf(c556,plain,~dirty(skolem0006)|dirty(skolem0008),inference(resolution,[status(thm)],[c39, c70])).
% 0.78/0.98  cnf(c555,plain,~dirty(skolem0009)|dirty(skolem0007),inference(resolution,[status(thm)],[c39, c239])).
% 0.78/0.98  cnf(c554,plain,~dirty(skolem0008)|dirty(skolem0006),inference(resolution,[status(thm)],[c39, c234])).
% 0.78/0.98  cnf(c553,plain,~dirty(skolem0007)|dirty(skolem0009),inference(resolution,[status(thm)],[c39, c72])).
% 0.78/0.98  cnf(c552,plain,~dirty(skolem0006)|dirty(skolem0007),inference(resolution,[status(thm)],[c39, c74])).
% 0.78/0.98  cnf(c551,plain,~dirty(skolem0007)|dirty(skolem0006),inference(resolution,[status(thm)],[c39, c244])).
% 0.78/0.98  cnf(c66,negated_conjecture,young(skolem0006),inference(split_conjunct,[status(thm)],[c46])).
% 0.78/0.98  cnf(c36,axiom,X229!=X230|~young(X229)|young(X230),theory(equality)).
% 0.78/0.98  cnf(c547,plain,~young(skolem0006)|young(skolem0008),inference(resolution,[status(thm)],[c36, c70])).
% 0.78/0.98  cnf(c826,plain,young(skolem0008),inference(resolution,[status(thm)],[c547, c66])).
% 0.78/0.98  cnf(c69,negated_conjecture,young(skolem0007),inference(split_conjunct,[status(thm)],[c46])).
% 0.78/0.98  cnf(c544,plain,~young(skolem0007)|young(skolem0009),inference(resolution,[status(thm)],[c36, c72])).
% 0.78/0.98  cnf(c824,plain,young(skolem0009),inference(resolution,[status(thm)],[c544, c69])).
% 0.78/0.98  cnf(c528,plain,~owner(skolem0006)|owner(skolem0008),inference(resolution,[status(thm)],[c32, c70])).
% 0.78/0.98  cnf(c527,plain,~owner(skolem0009)|owner(skolem0007),inference(resolution,[status(thm)],[c32, c239])).
% 0.78/0.98  cnf(c526,plain,~owner(skolem0008)|owner(skolem0006),inference(resolution,[status(thm)],[c32, c234])).
% 0.78/0.98  cnf(c525,plain,~owner(skolem0007)|owner(skolem0009),inference(resolution,[status(thm)],[c32, c72])).
% 0.78/0.98  cnf(c524,plain,~owner(skolem0006)|owner(skolem0007),inference(resolution,[status(thm)],[c32, c74])).
% 0.78/0.98  cnf(c523,plain,~owner(skolem0007)|owner(skolem0006),inference(resolution,[status(thm)],[c32, c244])).
% 0.78/0.98  cnf(c514,plain,~proposition(skolem0006)|proposition(skolem0008),inference(resolution,[status(thm)],[c30, c70])).
% 0.78/0.98  cnf(c513,plain,~proposition(skolem0009)|proposition(skolem0007),inference(resolution,[status(thm)],[c30, c239])).
% 0.78/0.98  cnf(c512,plain,~proposition(skolem0008)|proposition(skolem0006),inference(resolution,[status(thm)],[c30, c234])).
% 0.78/0.98  cnf(c511,plain,~proposition(skolem0007)|proposition(skolem0009),inference(resolution,[status(thm)],[c30, c72])).
% 0.78/0.98  cnf(c510,plain,~proposition(skolem0006)|proposition(skolem0007),inference(resolution,[status(thm)],[c30, c74])).
% 0.78/0.98  cnf(c509,plain,~proposition(skolem0007)|proposition(skolem0006),inference(resolution,[status(thm)],[c30, c244])).
% 0.78/0.98  cnf(c505,plain,~drs(skolem0006)|drs(skolem0008),inference(resolution,[status(thm)],[c29, c70])).
% 0.78/0.98  cnf(c504,plain,~drs(skolem0009)|drs(skolem0007),inference(resolution,[status(thm)],[c29, c239])).
% 0.78/0.98  cnf(c503,plain,~drs(skolem0008)|drs(skolem0006),inference(resolution,[status(thm)],[c29, c234])).
% 0.78/0.98  cnf(c502,plain,~drs(skolem0007)|drs(skolem0009),inference(resolution,[status(thm)],[c29, c72])).
% 0.78/0.98  cnf(c501,plain,~drs(skolem0006)|drs(skolem0007),inference(resolution,[status(thm)],[c29, c74])).
% 0.78/0.98  cnf(c500,plain,~drs(skolem0007)|drs(skolem0006),inference(resolution,[status(thm)],[c29, c244])).
% 0.78/0.98  cnf(c498,plain,~woman(skolem0006)|woman(skolem0008),inference(resolution,[status(thm)],[c28, c70])).
% 0.78/0.98  cnf(c497,plain,~woman(skolem0009)|woman(skolem0007),inference(resolution,[status(thm)],[c28, c239])).
% 0.78/0.98  cnf(c496,plain,~woman(skolem0008)|woman(skolem0006),inference(resolution,[status(thm)],[c28, c234])).
% 0.78/0.98  cnf(c495,plain,~woman(skolem0007)|woman(skolem0009),inference(resolution,[status(thm)],[c28, c72])).
% 0.78/0.98  cnf(c494,plain,~woman(skolem0006)|woman(skolem0007),inference(resolution,[status(thm)],[c28, c74])).
% 0.78/0.98  cnf(c493,plain,~woman(skolem0007)|woman(skolem0006),inference(resolution,[status(thm)],[c28, c244])).
% 0.78/0.98  cnf(c491,plain,~female(skolem0006)|female(skolem0008),inference(resolution,[status(thm)],[c27, c70])).
% 0.78/0.98  cnf(c490,plain,~female(skolem0009)|female(skolem0007),inference(resolution,[status(thm)],[c27, c239])).
% 0.78/0.98  cnf(c489,plain,~female(skolem0008)|female(skolem0006),inference(resolution,[status(thm)],[c27, c234])).
% 0.78/0.98  cnf(c488,plain,~female(skolem0007)|female(skolem0009),inference(resolution,[status(thm)],[c27, c72])).
% 0.78/0.98  cnf(c487,plain,~female(skolem0006)|female(skolem0007),inference(resolution,[status(thm)],[c27, c74])).
% 0.78/0.98  cnf(c486,plain,~female(skolem0007)|female(skolem0006),inference(resolution,[status(thm)],[c27, c244])).
% 0.78/0.98  cnf(c470,plain,~new(skolem0006)|new(skolem0008),inference(resolution,[status(thm)],[c24, c70])).
% 0.78/0.98  cnf(c469,plain,~new(skolem0009)|new(skolem0007),inference(resolution,[status(thm)],[c24, c239])).
% 0.78/0.98  cnf(c468,plain,~new(skolem0008)|new(skolem0006),inference(resolution,[status(thm)],[c24, c234])).
% 0.78/0.98  cnf(c467,plain,~new(skolem0007)|new(skolem0009),inference(resolution,[status(thm)],[c24, c72])).
% 0.78/0.98  cnf(c466,plain,~new(skolem0006)|new(skolem0007),inference(resolution,[status(thm)],[c24, c74])).
% 0.78/0.98  cnf(c465,plain,~new(skolem0007)|new(skolem0006),inference(resolution,[status(thm)],[c24, c244])).
% 0.78/0.98  cnf(c462,plain,~car(skolem0007)|car(skolem0006),inference(resolution,[status(thm)],[c244, c16])).
% 0.78/0.98  cnf(c461,plain,~object(skolem0007)|object(skolem0006),inference(resolution,[status(thm)],[c244, c5])).
% 0.78/0.98  cnf(c460,plain,~transport(skolem0007)|transport(skolem0006),inference(resolution,[status(thm)],[c244, c11])).
% 0.78/0.98  cnf(c459,plain,~seat(skolem0007)|seat(skolem0006),inference(resolution,[status(thm)],[c244, c8])).
% 0.78/0.98  cnf(c458,plain,~chevy(skolem0007)|chevy(skolem0006),inference(resolution,[status(thm)],[c244, c15])).
% 0.78/0.98  cnf(c457,plain,~event(skolem0007)|event(skolem0006),inference(resolution,[status(thm)],[c244, c19])).
% 0.78/0.98  cnf(c456,plain,~front(skolem0007)|front(skolem0006),inference(resolution,[status(thm)],[c244, c6])).
% 0.78/0.98  cnf(c451,plain,X278!=skolem0007|X278=skolem0006,inference(resolution,[status(thm)],[c244, transitivity])).
% 0.78/0.98  cnf(c454,plain,~vehicle(skolem0007)|vehicle(skolem0006),inference(resolution,[status(thm)],[c244, c17])).
% 0.78/0.98  cnf(c453,plain,~street(skolem0007)|street(skolem0006),inference(resolution,[status(thm)],[c244, c12])).
% 0.78/0.98  cnf(c450,plain,~nonhuman(skolem0007)|nonhuman(skolem0006),inference(resolution,[status(thm)],[c244, c7])).
% 0.78/0.98  cnf(c449,plain,~location(skolem0007)|location(skolem0006),inference(resolution,[status(thm)],[c244, c18])).
% 0.78/0.98  cnf(c448,plain,~old(skolem0007)|old(skolem0006),inference(resolution,[status(thm)],[c244, c23])).
% 0.78/0.98  cnf(c446,plain,~way(skolem0007)|way(skolem0006),inference(resolution,[status(thm)],[c244, c13])).
% 0.78/0.98  cnf(c444,plain,~furniture(skolem0007)|furniture(skolem0006),inference(resolution,[status(thm)],[c244, c9])).
% 0.78/0.98  cnf(c443,plain,~hollywood(skolem0007)|hollywood(skolem0006),inference(resolution,[status(thm)],[c244, c21])).
% 0.78/0.98  cnf(c442,plain,~city(skolem0007)|city(skolem0006),inference(resolution,[status(thm)],[c244, c22])).
% 0.78/0.98  cnf(c441,plain,~instrumentality(skolem0007)|instrumentality(skolem0006),inference(resolution,[status(thm)],[c244, c10])).
% 0.78/0.98  cnf(c438,plain,~artifact(skolem0007)|artifact(skolem0006),inference(resolution,[status(thm)],[c244, c14])).
% 0.78/0.98  cnf(c437,plain,~old(skolem0006)|old(skolem0008),inference(resolution,[status(thm)],[c23, c70])).
% 0.78/0.98  cnf(c436,plain,~old(skolem0009)|old(skolem0007),inference(resolution,[status(thm)],[c23, c239])).
% 0.78/0.98  cnf(c435,plain,~old(skolem0008)|old(skolem0006),inference(resolution,[status(thm)],[c23, c234])).
% 0.78/0.98  cnf(c434,plain,~old(skolem0007)|old(skolem0009),inference(resolution,[status(thm)],[c23, c72])).
% 0.78/0.98  cnf(c433,plain,~old(skolem0006)|old(skolem0007),inference(resolution,[status(thm)],[c23, c74])).
% 0.78/0.98  cnf(c430,plain,~car(skolem0009)|car(skolem0007),inference(resolution,[status(thm)],[c239, c16])).
% 0.78/0.98  cnf(c429,plain,~object(skolem0009)|object(skolem0007),inference(resolution,[status(thm)],[c239, c5])).
% 0.78/0.98  cnf(c428,plain,~transport(skolem0009)|transport(skolem0007),inference(resolution,[status(thm)],[c239, c11])).
% 0.78/0.98  cnf(c427,plain,~seat(skolem0009)|seat(skolem0007),inference(resolution,[status(thm)],[c239, c8])).
% 0.78/0.98  cnf(c426,plain,~chevy(skolem0009)|chevy(skolem0007),inference(resolution,[status(thm)],[c239, c15])).
% 0.78/0.98  cnf(c425,plain,~event(skolem0009)|event(skolem0007),inference(resolution,[status(thm)],[c239, c19])).
% 0.78/0.98  cnf(c424,plain,~front(skolem0009)|front(skolem0007),inference(resolution,[status(thm)],[c239, c6])).
% 0.78/0.98  cnf(c422,plain,~vehicle(skolem0009)|vehicle(skolem0007),inference(resolution,[status(thm)],[c239, c17])).
% 0.78/0.98  cnf(c419,plain,X277!=skolem0009|X277=skolem0007,inference(resolution,[status(thm)],[c239, transitivity])).
% 0.78/0.98  cnf(c421,plain,~street(skolem0009)|street(skolem0007),inference(resolution,[status(thm)],[c239, c12])).
% 0.78/0.98  cnf(c418,plain,~nonhuman(skolem0009)|nonhuman(skolem0007),inference(resolution,[status(thm)],[c239, c7])).
% 0.78/0.98  cnf(c417,plain,~location(skolem0009)|location(skolem0007),inference(resolution,[status(thm)],[c239, c18])).
% 0.78/0.98  cnf(c415,plain,~way(skolem0009)|way(skolem0007),inference(resolution,[status(thm)],[c239, c13])).
% 0.78/0.98  cnf(c413,plain,~furniture(skolem0009)|furniture(skolem0007),inference(resolution,[status(thm)],[c239, c9])).
% 0.78/0.98  cnf(c412,plain,~hollywood(skolem0009)|hollywood(skolem0007),inference(resolution,[status(thm)],[c239, c21])).
% 0.78/0.98  cnf(c411,plain,~city(skolem0009)|city(skolem0007),inference(resolution,[status(thm)],[c239, c22])).
% 0.78/0.98  cnf(c410,plain,~instrumentality(skolem0009)|instrumentality(skolem0007),inference(resolution,[status(thm)],[c239, c10])).
% 0.78/0.98  cnf(c407,plain,~artifact(skolem0009)|artifact(skolem0007),inference(resolution,[status(thm)],[c239, c14])).
% 0.78/0.98  cnf(c405,plain,~car(skolem0008)|car(skolem0006),inference(resolution,[status(thm)],[c234, c16])).
% 0.78/0.98  cnf(c404,plain,~object(skolem0008)|object(skolem0006),inference(resolution,[status(thm)],[c234, c5])).
% 0.78/0.98  cnf(c403,plain,~transport(skolem0008)|transport(skolem0006),inference(resolution,[status(thm)],[c234, c11])).
% 0.78/0.98  cnf(c402,plain,~seat(skolem0008)|seat(skolem0006),inference(resolution,[status(thm)],[c234, c8])).
% 0.78/0.98  cnf(c401,plain,~chevy(skolem0008)|chevy(skolem0006),inference(resolution,[status(thm)],[c234, c15])).
% 0.78/0.98  cnf(c400,plain,~event(skolem0008)|event(skolem0006),inference(resolution,[status(thm)],[c234, c19])).
% 0.78/0.98  cnf(c399,plain,~front(skolem0008)|front(skolem0006),inference(resolution,[status(thm)],[c234, c6])).
% 0.78/0.98  cnf(c394,plain,X276!=skolem0008|X276=skolem0006,inference(resolution,[status(thm)],[c234, transitivity])).
% 0.78/0.98  cnf(c241,plain,X275!=skolem0006|X275=skolem0007,inference(resolution,[status(thm)],[c74, transitivity])).
% 0.78/0.98  cnf(c397,plain,~vehicle(skolem0008)|vehicle(skolem0006),inference(resolution,[status(thm)],[c234, c17])).
% 0.78/0.98  cnf(c396,plain,~street(skolem0008)|street(skolem0006),inference(resolution,[status(thm)],[c234, c12])).
% 0.78/0.98  cnf(c393,plain,~nonhuman(skolem0008)|nonhuman(skolem0006),inference(resolution,[status(thm)],[c234, c7])).
% 0.78/0.98  cnf(c392,plain,~location(skolem0008)|location(skolem0006),inference(resolution,[status(thm)],[c234, c18])).
% 0.78/0.98  fof(ax38,axiom,(![U]:(![V]:(![W]:((have(U,V,W)&human(V))<=>(owner(V)&of(V,W)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax38)).
% 0.78/0.98  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.78/0.98  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.78/0.98  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.78/0.98  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.78/0.98  cnf(c98,plain,~owner(X271)|~of(X271,X272)|human(X271),inference(split_conjunct,[status(thm)],[c94])).
% 0.78/0.98  cnf(c390,plain,~way(skolem0008)|way(skolem0006),inference(resolution,[status(thm)],[c234, c13])).
% 0.78/0.98  cnf(c388,plain,~furniture(skolem0008)|furniture(skolem0006),inference(resolution,[status(thm)],[c234, c9])).
% 0.78/0.98  cnf(c387,plain,~hollywood(skolem0008)|hollywood(skolem0006),inference(resolution,[status(thm)],[c234, c21])).
% 0.78/0.98  cnf(c386,plain,~city(skolem0008)|city(skolem0006),inference(resolution,[status(thm)],[c234, c22])).
% 0.78/0.98  cnf(c97,plain,~owner(X268)|~of(X268,X269)|have(X270,X268,X269),inference(split_conjunct,[status(thm)],[c94])).
% 0.78/0.98  cnf(c385,plain,~instrumentality(skolem0008)|instrumentality(skolem0006),inference(resolution,[status(thm)],[c234, c10])).
% 0.78/0.98  cnf(c382,plain,~artifact(skolem0008)|artifact(skolem0006),inference(resolution,[status(thm)],[c234, c14])).
% 0.78/0.98  cnf(c380,plain,~city(skolem0006)|city(skolem0008),inference(resolution,[status(thm)],[c22, c70])).
% 0.78/0.98  cnf(c96,plain,~have(X267,X265,X266)|~human(X265)|of(X265,X266),inference(split_conjunct,[status(thm)],[c94])).
% 0.78/0.98  cnf(c379,plain,~city(skolem0007)|city(skolem0009),inference(resolution,[status(thm)],[c22, c72])).
% 0.78/0.98  cnf(c378,plain,~city(skolem0006)|city(skolem0007),inference(resolution,[status(thm)],[c22, c74])).
% 0.78/0.98  cnf(c374,plain,~hollywood(skolem0006)|hollywood(skolem0008),inference(resolution,[status(thm)],[c21, c70])).
% 0.78/0.98  cnf(c373,plain,~hollywood(skolem0007)|hollywood(skolem0009),inference(resolution,[status(thm)],[c21, c72])).
% 0.78/0.98  cnf(c372,plain,~hollywood(skolem0006)|hollywood(skolem0007),inference(resolution,[status(thm)],[c21, c74])).
% 0.78/0.98  cnf(c95,plain,~have(X264,X262,X263)|~human(X262)|owner(X262),inference(split_conjunct,[status(thm)],[c94])).
% 0.78/0.98  cnf(c356,plain,~event(skolem0006)|event(skolem0008),inference(resolution,[status(thm)],[c19, c70])).
% 0.78/0.98  cnf(c355,plain,~event(skolem0007)|event(skolem0009),inference(resolution,[status(thm)],[c19, c72])).
% 0.78/0.98  fof(ax39,axiom,(![U]:(![V]:(![W]:(((have(U,V,W)&nonhuman(V))&nonhuman(W))=>partof(W,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax39)).
% 0.78/0.98  fof(c87,plain,(![U]:(![V]:(![W]:(((~have(U,V,W)|~nonhuman(V))|~nonhuman(W))|partof(W,V))))),inference(fof_nnf,[status(thm)],[ax39])).
% 0.78/0.98  fof(c88,plain,(![X20]:(![X21]:(![X22]:(((~have(X20,X21,X22)|~nonhuman(X21))|~nonhuman(X22))|partof(X22,X21))))),inference(variable_rename,[status(thm)],[c87])).
% 0.78/0.98  cnf(c89,plain,~have(X260,X261,X259)|~nonhuman(X261)|~nonhuman(X259)|partof(X259,X261),inference(split_conjunct,[status(thm)],[c88])).
% 0.78/0.98  cnf(c354,plain,~event(skolem0006)|event(skolem0007),inference(resolution,[status(thm)],[c19, c74])).
% 0.78/0.98  cnf(c352,plain,~location(skolem0006)|location(skolem0008),inference(resolution,[status(thm)],[c18, c70])).
% 0.78/0.98  cnf(c351,plain,~location(skolem0007)|location(skolem0009),inference(resolution,[status(thm)],[c18, c72])).
% 0.78/0.98  cnf(c350,plain,~location(skolem0006)|location(skolem0007),inference(resolution,[status(thm)],[c18, c74])).
% 0.78/0.98  cnf(c341,plain,~vehicle(skolem0006)|vehicle(skolem0008),inference(resolution,[status(thm)],[c17, c70])).
% 0.78/0.98  fof(ax40,axiom,(![U]:(![V]:(![W]:((event(U)&have(U,V,W))=>of(V,W))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax40)).
% 0.78/0.98  fof(c84,plain,(![U]:(![V]:(![W]:((~event(U)|~have(U,V,W))|of(V,W))))),inference(fof_nnf,[status(thm)],[ax40])).
% 0.78/0.98  fof(c85,plain,(![X17]:(![X18]:(![X19]:((~event(X17)|~have(X17,X18,X19))|of(X18,X19))))),inference(variable_rename,[status(thm)],[c84])).
% 0.78/0.98  cnf(c86,plain,~event(X256)|~have(X256,X257,X258)|of(X257,X258),inference(split_conjunct,[status(thm)],[c85])).
% 0.78/0.98  cnf(c340,plain,~vehicle(skolem0007)|vehicle(skolem0009),inference(resolution,[status(thm)],[c17, c72])).
% 0.78/0.98  cnf(c339,plain,~vehicle(skolem0006)|vehicle(skolem0007),inference(resolution,[status(thm)],[c17, c74])).
% 0.78/0.98  cnf(c334,plain,~car(skolem0006)|car(skolem0008),inference(resolution,[status(thm)],[c16, c70])).
% 0.78/0.98  cnf(c333,plain,~car(skolem0007)|car(skolem0009),inference(resolution,[status(thm)],[c16, c72])).
% 0.78/0.98  cnf(c332,plain,~car(skolem0006)|car(skolem0007),inference(resolution,[status(thm)],[c16, c74])).
% 0.78/0.98  fof(ax41,axiom,(![U]:(![V]:(of(V,U)=>(?[W]:(event(W)&have(W,U,V)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax41)).
% 0.78/0.98  fof(c78,plain,(![U]:(![V]:(~of(V,U)|(?[W]:(event(W)&have(W,U,V)))))),inference(fof_nnf,[status(thm)],[ax41])).
% 0.78/0.98  fof(c79,plain,(![X14]:(![X15]:(~of(X15,X14)|(?[X16]:(event(X16)&have(X16,X14,X15)))))),inference(variable_rename,[status(thm)],[c78])).
% 0.78/0.98  fof(c80,plain,(![X14]:(![X15]:(~of(X15,X14)|(event(skolem0010(X14,X15))&have(skolem0010(X14,X15),X14,X15))))),inference(skolemize,[status(esa)],[c79])).
% 0.78/0.98  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.78/0.98  cnf(c83,plain,~of(X255,X254)|have(skolem0010(X254,X255),X254,X255),inference(split_conjunct,[status(thm)],[c81])).
% 0.78/0.98  cnf(c325,plain,~chevy(skolem0006)|chevy(skolem0008),inference(resolution,[status(thm)],[c15, c70])).
% 0.78/0.98  cnf(c324,plain,~chevy(skolem0007)|chevy(skolem0009),inference(resolution,[status(thm)],[c15, c72])).
% 0.78/0.98  cnf(c323,plain,~chevy(skolem0006)|chevy(skolem0007),inference(resolution,[status(thm)],[c15, c74])).
% 0.78/0.98  cnf(c319,plain,~artifact(skolem0006)|artifact(skolem0008),inference(resolution,[status(thm)],[c14, c70])).
% 0.78/0.98  cnf(c318,plain,~artifact(skolem0007)|artifact(skolem0009),inference(resolution,[status(thm)],[c14, c72])).
% 0.78/0.98  cnf(c82,plain,~of(X253,X252)|event(skolem0010(X252,X253)),inference(split_conjunct,[status(thm)],[c81])).
% 0.78/0.98  cnf(c317,plain,~artifact(skolem0006)|artifact(skolem0007),inference(resolution,[status(thm)],[c14, c74])).
% 0.78/0.98  cnf(c310,plain,~way(skolem0006)|way(skolem0008),inference(resolution,[status(thm)],[c13, c70])).
% 0.78/0.98  cnf(c309,plain,~way(skolem0007)|way(skolem0009),inference(resolution,[status(thm)],[c13, c72])).
% 0.78/0.98  cnf(c308,plain,~way(skolem0006)|way(skolem0007),inference(resolution,[status(thm)],[c13, c74])).
% 0.78/0.98  cnf(c304,plain,~street(skolem0006)|street(skolem0008),inference(resolution,[status(thm)],[c12, c70])).
% 0.78/0.98  fof(ax42,axiom,(![U]:(![V]:(![W]:((partof(U,V)&partof(U,W))=>V=W)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax42)).
% 0.78/0.98  fof(c75,plain,(![U]:(![V]:(![W]:((~partof(U,V)|~partof(U,W))|V=W)))),inference(fof_nnf,[status(thm)],[ax42])).
% 0.78/0.98  fof(c76,plain,(![X11]:(![X12]:(![X13]:((~partof(X11,X12)|~partof(X11,X13))|X12=X13)))),inference(variable_rename,[status(thm)],[c75])).
% 0.78/0.98  cnf(c77,plain,~partof(X249,X250)|~partof(X249,X251)|X250=X251,inference(split_conjunct,[status(thm)],[c76])).
% 0.78/0.98  cnf(c303,plain,~street(skolem0007)|street(skolem0009),inference(resolution,[status(thm)],[c12, c72])).
% 0.78/0.98  cnf(c302,plain,~street(skolem0006)|street(skolem0007),inference(resolution,[status(thm)],[c12, c74])).
% 0.78/0.98  cnf(c295,plain,~transport(skolem0006)|transport(skolem0008),inference(resolution,[status(thm)],[c11, c70])).
% 0.78/0.98  cnf(c294,plain,~transport(skolem0007)|transport(skolem0009),inference(resolution,[status(thm)],[c11, c72])).
% 0.78/0.98  cnf(c293,plain,~transport(skolem0006)|transport(skolem0007),inference(resolution,[status(thm)],[c11, c74])).
% 0.78/0.98  cnf(c288,plain,~instrumentality(skolem0006)|instrumentality(skolem0008),inference(resolution,[status(thm)],[c10, c70])).
% 0.78/0.98  cnf(c287,plain,~instrumentality(skolem0007)|instrumentality(skolem0009),inference(resolution,[status(thm)],[c10, c72])).
% 0.78/0.98  cnf(c286,plain,~instrumentality(skolem0006)|instrumentality(skolem0007),inference(resolution,[status(thm)],[c10, c74])).
% 0.78/0.98  cnf(c283,plain,~furniture(skolem0006)|furniture(skolem0008),inference(resolution,[status(thm)],[c9, c70])).
% 0.78/0.98  cnf(c282,plain,~furniture(skolem0007)|furniture(skolem0009),inference(resolution,[status(thm)],[c9, c72])).
% 0.78/0.98  cnf(c281,plain,~furniture(skolem0006)|furniture(skolem0007),inference(resolution,[status(thm)],[c9, c74])).
% 0.78/0.98  cnf(c276,plain,~seat(skolem0006)|seat(skolem0008),inference(resolution,[status(thm)],[c8, c70])).
% 0.78/0.98  cnf(c275,plain,~seat(skolem0007)|seat(skolem0009),inference(resolution,[status(thm)],[c8, c72])).
% 0.78/0.98  cnf(c274,plain,~seat(skolem0006)|seat(skolem0007),inference(resolution,[status(thm)],[c8, c74])).
% 0.78/0.98  cnf(c267,plain,~nonhuman(skolem0006)|nonhuman(skolem0008),inference(resolution,[status(thm)],[c7, c70])).
% 0.78/0.98  cnf(c266,plain,~nonhuman(skolem0007)|nonhuman(skolem0009),inference(resolution,[status(thm)],[c7, c72])).
% 0.78/0.98  cnf(c265,plain,~nonhuman(skolem0006)|nonhuman(skolem0007),inference(resolution,[status(thm)],[c7, c74])).
% 0.78/0.98  cnf(c263,plain,~front(skolem0006)|front(skolem0008),inference(resolution,[status(thm)],[c6, c70])).
% 0.78/0.98  cnf(c262,plain,~front(skolem0007)|front(skolem0009),inference(resolution,[status(thm)],[c6, c72])).
% 0.78/0.98  cnf(c261,plain,~front(skolem0006)|front(skolem0007),inference(resolution,[status(thm)],[c6, c74])).
% 0.78/0.98  cnf(c259,plain,~object(skolem0006)|object(skolem0008),inference(resolution,[status(thm)],[c5, c70])).
% 0.78/0.98  cnf(c258,plain,~object(skolem0007)|object(skolem0009),inference(resolution,[status(thm)],[c5, c72])).
% 0.78/0.98  cnf(c257,plain,~object(skolem0006)|object(skolem0007),inference(resolution,[status(thm)],[c5, c74])).
% 0.78/0.98  fof(ax27,axiom,(![U]:(abstraction(U)=>(~entity(U)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax27)).
% 0.78/0.98  fof(c136,plain,(![U]:(abstraction(U)=>~entity(U))),inference(fof_simplification,[status(thm)],[ax27])).
% 0.78/0.98  fof(c137,plain,(![U]:(~abstraction(U)|~entity(U))),inference(fof_nnf,[status(thm)],[c136])).
% 0.78/0.98  fof(c138,plain,(![X40]:(~abstraction(X40)|~entity(X40))),inference(variable_rename,[status(thm)],[c137])).
% 0.78/0.98  cnf(c139,plain,~abstraction(X99)|~entity(X99),inference(split_conjunct,[status(thm)],[c138])).
% 0.78/0.98  fof(ax4,axiom,(![U]:(organism(U)=>entity(U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax4)).
% 0.78/0.98  fof(c212,plain,(![U]:(~organism(U)|entity(U))),inference(fof_nnf,[status(thm)],[ax4])).
% 0.78/0.98  fof(c213,plain,(![X63]:(~organism(X63)|entity(X63))),inference(variable_rename,[status(thm)],[c212])).
% 0.78/0.98  cnf(c214,plain,~organism(X146)|entity(X146),inference(split_conjunct,[status(thm)],[c213])).
% 0.83/0.98  fof(ax3,axiom,(![U]:(human(U)=>organism(U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax3)).
% 0.83/0.98  fof(c215,plain,(![U]:(~human(U)|organism(U))),inference(fof_nnf,[status(thm)],[ax3])).
% 0.83/0.98  fof(c216,plain,(![X64]:(~human(X64)|organism(X64))),inference(variable_rename,[status(thm)],[c215])).
% 0.83/0.98  cnf(c217,plain,~human(X149)|organism(X149),inference(split_conjunct,[status(thm)],[c216])).
% 0.83/0.98  fof(ax2,axiom,(![U]:(man(U)=>human(U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax2)).
% 0.83/0.98  fof(c218,plain,(![U]:(~man(U)|human(U))),inference(fof_nnf,[status(thm)],[ax2])).
% 0.83/0.98  fof(c219,plain,(![X65]:(~man(X65)|human(X65))),inference(variable_rename,[status(thm)],[c218])).
% 0.83/0.98  cnf(c220,plain,~man(X152)|human(X152),inference(split_conjunct,[status(thm)],[c219])).
% 0.83/0.98  fof(ax1,axiom,(![U]:(fellow(U)=>man(U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax1)).
% 0.83/0.98  fof(c221,plain,(![U]:(~fellow(U)|man(U))),inference(fof_nnf,[status(thm)],[ax1])).
% 0.83/0.98  fof(c222,plain,(![X66]:(~fellow(X66)|man(X66))),inference(variable_rename,[status(thm)],[c221])).
% 0.83/0.98  cnf(c223,plain,~fellow(X155)|man(X155),inference(split_conjunct,[status(thm)],[c222])).
% 0.83/0.98  cnf(c67,negated_conjecture,fellow(skolem0007),inference(split_conjunct,[status(thm)],[c46])).
% 0.83/0.98  cnf(c0,axiom,X73!=X74|~fellow(X73)|fellow(X74),theory(equality)).
% 0.83/0.98  cnf(c235,plain,~fellow(skolem0007)|fellow(skolem0009),inference(resolution,[status(thm)],[c72, c0])).
% 0.83/0.98  cnf(c529,plain,fellow(skolem0009),inference(resolution,[status(thm)],[c235, c67])).
% 0.83/0.98  cnf(c530,plain,man(skolem0009),inference(resolution,[status(thm)],[c529, c223])).
% 0.83/0.98  cnf(c531,plain,human(skolem0009),inference(resolution,[status(thm)],[c530, c220])).
% 0.83/0.98  cnf(c533,plain,organism(skolem0009),inference(resolution,[status(thm)],[c531, c217])).
% 0.83/0.98  cnf(c535,plain,entity(skolem0009),inference(resolution,[status(thm)],[c533, c214])).
% 0.83/0.98  cnf(c537,plain,~abstraction(skolem0009),inference(resolution,[status(thm)],[c535, c139])).
% 0.83/0.98  fof(ax26,axiom,(![U]:(eventuality(U)=>(~entity(U)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax26)).
% 0.83/0.98  fof(c140,plain,(![U]:(eventuality(U)=>~entity(U))),inference(fof_simplification,[status(thm)],[ax26])).
% 0.83/0.98  fof(c141,plain,(![U]:(~eventuality(U)|~entity(U))),inference(fof_nnf,[status(thm)],[c140])).
% 0.83/0.98  fof(c142,plain,(![X41]:(~eventuality(X41)|~entity(X41))),inference(variable_rename,[status(thm)],[c141])).
% 0.83/0.98  cnf(c143,plain,~eventuality(X100)|~entity(X100),inference(split_conjunct,[status(thm)],[c142])).
% 0.83/0.98  cnf(c536,plain,~eventuality(skolem0009),inference(resolution,[status(thm)],[c535, c143])).
% 0.83/0.98  cnf(c34,axiom,X222!=X223|X221!=X224|~partof(X222,X221)|partof(X223,X224),theory(equality)).
% 0.83/0.98  fof(ax31,axiom,(![U]:(man(U)=>male(U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax31)).
% 0.83/0.98  fof(c121,plain,(![U]:(~man(U)|male(U))),inference(fof_nnf,[status(thm)],[ax31])).
% 0.83/0.98  fof(c122,plain,(![X36]:(~man(X36)|male(X36))),inference(variable_rename,[status(thm)],[c121])).
% 0.83/0.98  cnf(c123,plain,~man(X91)|male(X91),inference(split_conjunct,[status(thm)],[c122])).
% 0.83/0.98  cnf(c532,plain,male(skolem0009),inference(resolution,[status(thm)],[c530, c123])).
% 0.83/0.98  cnf(c33,axiom,X218!=X219|X217!=X220|~of(X218,X217)|of(X219,X220),theory(equality)).
% 0.83/0.98  cnf(c64,negated_conjecture,fellow(skolem0006),inference(split_conjunct,[status(thm)],[c46])).
% 0.83/0.98  cnf(c230,plain,~fellow(skolem0006)|fellow(skolem0008),inference(resolution,[status(thm)],[c70, c0])).
% 0.83/0.98  cnf(c506,plain,fellow(skolem0008),inference(resolution,[status(thm)],[c230, c64])).
% 0.83/0.98  cnf(c507,plain,man(skolem0008),inference(resolution,[status(thm)],[c506, c223])).
% 0.83/0.98  cnf(c515,plain,human(skolem0008),inference(resolution,[status(thm)],[c507, c220])).
% 0.83/0.98  cnf(c517,plain,organism(skolem0008),inference(resolution,[status(thm)],[c515, c217])).
% 0.83/0.98  cnf(c519,plain,entity(skolem0008),inference(resolution,[status(thm)],[c517, c214])).
% 0.83/0.98  cnf(c521,plain,~abstraction(skolem0008),inference(resolution,[status(thm)],[c519, c139])).
% 0.83/0.98  cnf(c520,plain,~eventuality(skolem0008),inference(resolution,[status(thm)],[c519, c143])).
% 0.83/0.98  cnf(c31,axiom,X207!=X211|X212!=X208|X210!=X209|~have(X207,X212,X210)|have(X211,X208,X209),theory(equality)).
% 0.83/0.98  cnf(c516,plain,male(skolem0008),inference(resolution,[status(thm)],[c507, c123])).
% 0.83/0.98  cnf(c26,axiom,X181!=X182|~male(X181)|male(X182),theory(equality)).
% 0.83/0.98  cnf(c25,axiom,X174!=X175|~abstraction(X174)|abstraction(X175),theory(equality)).
% 0.83/0.98  fof(ax32,axiom,(![U]:(male(U)=>human(U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax32)).
% 0.83/0.98  fof(c118,plain,(![U]:(~male(U)|human(U))),inference(fof_nnf,[status(thm)],[ax32])).
% 0.83/0.98  fof(c119,plain,(![X35]:(~male(X35)|human(X35))),inference(variable_rename,[status(thm)],[c118])).
% 0.83/0.98  cnf(c120,plain,~male(X90)|human(X90),inference(split_conjunct,[status(thm)],[c119])).
% 0.83/0.98  cnf(c65,negated_conjecture,man(skolem0006),inference(split_conjunct,[status(thm)],[c46])).
% 0.83/0.98  cnf(c254,plain,male(skolem0006),inference(resolution,[status(thm)],[c123, c65])).
% 0.83/0.98  cnf(c256,plain,human(skolem0006),inference(resolution,[status(thm)],[c254, c120])).
% 0.83/0.98  cnf(c359,plain,organism(skolem0006),inference(resolution,[status(thm)],[c217, c256])).
% 0.83/0.98  cnf(c361,plain,entity(skolem0006),inference(resolution,[status(thm)],[c359, c214])).
% 0.83/0.98  cnf(c365,plain,~abstraction(skolem0006),inference(resolution,[status(thm)],[c361, c139])).
% 0.83/0.98  cnf(c364,plain,~eventuality(skolem0006),inference(resolution,[status(thm)],[c361, c143])).
% 0.83/0.98  cnf(c68,negated_conjecture,man(skolem0007),inference(split_conjunct,[status(thm)],[c46])).
% 0.83/0.98  cnf(c253,plain,male(skolem0007),inference(resolution,[status(thm)],[c123, c68])).
% 0.83/0.98  cnf(c255,plain,human(skolem0007),inference(resolution,[status(thm)],[c253, c120])).
% 0.83/0.98  cnf(c358,plain,organism(skolem0007),inference(resolution,[status(thm)],[c217, c255])).
% 0.83/0.98  cnf(c360,plain,entity(skolem0007),inference(resolution,[status(thm)],[c358, c214])).
% 0.83/0.98  cnf(c363,plain,~abstraction(skolem0007),inference(resolution,[status(thm)],[c360, c139])).
% 0.83/0.98  cnf(c362,plain,~eventuality(skolem0007),inference(resolution,[status(thm)],[c360, c143])).
% 0.83/0.98  cnf(c20,axiom,X150!=X151|~eventuality(X150)|eventuality(X151),theory(equality)).
% 0.83/0.98  fof(ax18,axiom,(![U]:(artifact(U)=>object(U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax18)).
% 0.83/0.98  fof(c167,plain,(![U]:(~artifact(U)|object(U))),inference(fof_nnf,[status(thm)],[ax18])).
% 0.83/0.98  fof(c168,plain,(![X49]:(~artifact(X49)|object(X49))),inference(variable_rename,[status(thm)],[c167])).
% 0.83/0.98  cnf(c169,plain,~artifact(X114)|object(X114),inference(split_conjunct,[status(thm)],[c168])).
% 0.83/0.98  fof(ax17,axiom,(![U]:(instrumentality(U)=>artifact(U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax17)).
% 0.83/0.98  fof(c170,plain,(![U]:(~instrumentality(U)|artifact(U))),inference(fof_nnf,[status(thm)],[ax17])).
% 0.83/0.98  fof(c171,plain,(![X50]:(~instrumentality(X50)|artifact(X50))),inference(variable_rename,[status(thm)],[c170])).
% 0.83/0.98  cnf(c172,plain,~instrumentality(X115)|artifact(X115),inference(split_conjunct,[status(thm)],[c171])).
% 0.83/0.98  fof(ax16,axiom,(![U]:(transport(U)=>instrumentality(U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax16)).
% 0.83/0.98  fof(c173,plain,(![U]:(~transport(U)|instrumentality(U))),inference(fof_nnf,[status(thm)],[ax16])).
% 0.83/0.98  fof(c174,plain,(![X51]:(~transport(X51)|instrumentality(X51))),inference(variable_rename,[status(thm)],[c173])).
% 0.83/0.98  cnf(c175,plain,~transport(X118)|instrumentality(X118),inference(split_conjunct,[status(thm)],[c174])).
% 0.83/0.98  fof(ax15,axiom,(![U]:(vehicle(U)=>transport(U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax15)).
% 0.83/0.98  fof(c176,plain,(![U]:(~vehicle(U)|transport(U))),inference(fof_nnf,[status(thm)],[ax15])).
% 0.83/0.98  fof(c177,plain,(![X52]:(~vehicle(X52)|transport(X52))),inference(variable_rename,[status(thm)],[c176])).
% 0.83/0.98  cnf(c178,plain,~vehicle(X119)|transport(X119),inference(split_conjunct,[status(thm)],[c177])).
% 0.83/0.98  cnf(c57,negated_conjecture,car(skolem0005),inference(split_conjunct,[status(thm)],[c46])).
% 0.83/0.98  fof(ax14,axiom,(![U]:(car(U)=>vehicle(U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax14)).
% 0.83/0.98  fof(c179,plain,(![U]:(~car(U)|vehicle(U))),inference(fof_nnf,[status(thm)],[ax14])).
% 0.83/0.98  fof(c180,plain,(![X53]:(~car(X53)|vehicle(X53))),inference(variable_rename,[status(thm)],[c179])).
% 0.83/0.98  cnf(c181,plain,~car(X120)|vehicle(X120),inference(split_conjunct,[status(thm)],[c180])).
% 0.83/0.98  cnf(c290,plain,vehicle(skolem0005),inference(resolution,[status(thm)],[c181, c57])).
% 0.83/0.98  cnf(c291,plain,transport(skolem0005),inference(resolution,[status(thm)],[c290, c178])).
% 0.83/0.98  cnf(c292,plain,instrumentality(skolem0005),inference(resolution,[status(thm)],[c291, c175])).
% 0.83/0.98  cnf(c297,plain,artifact(skolem0005),inference(resolution,[status(thm)],[c292, c172])).
% 0.83/0.98  cnf(c298,plain,object(skolem0005),inference(resolution,[status(thm)],[c297, c169])).
% 0.83/0.98  fof(ax5,axiom,(![U]:(organism(U)=>(~object(U)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax5)).
% 0.83/0.98  fof(c208,plain,(![U]:(organism(U)=>~object(U))),inference(fof_simplification,[status(thm)],[ax5])).
% 0.83/0.98  fof(c209,plain,(![U]:(~organism(U)|~object(U))),inference(fof_nnf,[status(thm)],[c208])).
% 0.83/0.98  fof(c210,plain,(![X62]:(~organism(X62)|~object(X62))),inference(variable_rename,[status(thm)],[c209])).
% 0.83/0.98  cnf(c211,plain,~organism(X143)|~object(X143),inference(split_conjunct,[status(thm)],[c210])).
% 0.83/0.98  cnf(c349,plain,~organism(skolem0005),inference(resolution,[status(thm)],[c211, c298])).
% 0.83/0.98  cnf(c54,negated_conjecture,way(skolem0004),inference(split_conjunct,[status(thm)],[c46])).
% 0.83/0.98  fof(ax11,axiom,(![U]:(way(U)=>artifact(U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax11)).
% 0.83/0.98  fof(c189,plain,(![U]:(~way(U)|artifact(U))),inference(fof_nnf,[status(thm)],[ax11])).
% 0.83/0.98  fof(c190,plain,(![X56]:(~way(X56)|artifact(X56))),inference(variable_rename,[status(thm)],[c189])).
% 0.83/0.98  cnf(c191,plain,~way(X129)|artifact(X129),inference(split_conjunct,[status(thm)],[c190])).
% 0.83/0.98  cnf(c312,plain,artifact(skolem0004),inference(resolution,[status(thm)],[c191, c54])).
% 0.83/0.98  cnf(c313,plain,object(skolem0004),inference(resolution,[status(thm)],[c312, c169])).
% 0.83/0.98  cnf(c348,plain,~organism(skolem0004),inference(resolution,[status(thm)],[c211, c313])).
% 0.83/0.98  cnf(c48,negated_conjecture,furniture(skolem0001),inference(split_conjunct,[status(thm)],[c46])).
% 0.83/0.98  fof(ax8,axiom,(![U]:(furniture(U)=>instrumentality(U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax8)).
% 0.83/0.98  fof(c199,plain,(![U]:(~furniture(U)|instrumentality(U))),inference(fof_nnf,[status(thm)],[ax8])).
% 0.83/0.98  fof(c200,plain,(![X59]:(~furniture(X59)|instrumentality(X59))),inference(variable_rename,[status(thm)],[c199])).
% 0.83/0.98  cnf(c201,plain,~furniture(X136)|instrumentality(X136),inference(split_conjunct,[status(thm)],[c200])).
% 0.83/0.98  cnf(c327,plain,instrumentality(skolem0001),inference(resolution,[status(thm)],[c201, c48])).
% 0.83/0.98  cnf(c328,plain,artifact(skolem0001),inference(resolution,[status(thm)],[c327, c172])).
% 0.83/0.98  cnf(c330,plain,object(skolem0001),inference(resolution,[status(thm)],[c328, c169])).
% 0.83/0.98  cnf(c347,plain,~organism(skolem0001),inference(resolution,[status(thm)],[c211, c330])).
% 0.83/0.98  fof(ax23,axiom,(![U]:(location(U)=>object(U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax23)).
% 0.83/0.98  fof(c151,plain,(![U]:(~location(U)|object(U))),inference(fof_nnf,[status(thm)],[ax23])).
% 0.83/0.98  fof(c152,plain,(![X44]:(~location(X44)|object(X44))),inference(variable_rename,[status(thm)],[c151])).
% 0.83/0.98  cnf(c153,plain,~location(X103)|object(X103),inference(split_conjunct,[status(thm)],[c152])).
% 0.83/0.98  cnf(c51,negated_conjecture,city(skolem0002),inference(split_conjunct,[status(thm)],[c46])).
% 0.83/0.98  fof(ax22,axiom,(![U]:(city(U)=>location(U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax22)).
% 0.83/0.98  fof(c154,plain,(![U]:(~city(U)|location(U))),inference(fof_nnf,[status(thm)],[ax22])).
% 0.83/0.98  fof(c155,plain,(![X45]:(~city(X45)|location(X45))),inference(variable_rename,[status(thm)],[c154])).
% 0.83/0.98  cnf(c156,plain,~city(X106)|location(X106),inference(split_conjunct,[status(thm)],[c155])).
% 0.83/0.98  cnf(c269,plain,location(skolem0002),inference(resolution,[status(thm)],[c156, c51])).
% 0.83/0.98  cnf(c270,plain,object(skolem0002),inference(resolution,[status(thm)],[c269, c153])).
% 0.83/0.98  cnf(c346,plain,~organism(skolem0002),inference(resolution,[status(thm)],[c211, c270])).
% 0.83/0.98  fof(ax37,axiom,(![U]:(human(U)=>(~nonhuman(U)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax37)).
% 0.83/0.98  fof(c99,plain,(![U]:(human(U)=>~nonhuman(U))),inference(fof_simplification,[status(thm)],[ax37])).
% 0.83/0.98  fof(c100,plain,(![U]:(~human(U)|~nonhuman(U))),inference(fof_nnf,[status(thm)],[c99])).
% 0.83/0.98  fof(c101,plain,(![X29]:(~human(X29)|~nonhuman(X29))),inference(variable_rename,[status(thm)],[c100])).
% 0.83/0.98  cnf(c102,plain,~human(X82)|~nonhuman(X82),inference(split_conjunct,[status(thm)],[c101])).
% 0.83/0.98  cnf(c49,negated_conjecture,front(skolem0001),inference(split_conjunct,[status(thm)],[c46])).
% 0.83/0.98  fof(ax6,axiom,(![U]:(front(U)=>nonhuman(U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax6)).
% 0.83/0.98  fof(c205,plain,(![U]:(~front(U)|nonhuman(U))),inference(fof_nnf,[status(thm)],[ax6])).
% 0.83/0.98  fof(c206,plain,(![X61]:(~front(X61)|nonhuman(X61))),inference(variable_rename,[status(thm)],[c205])).
% 0.83/0.98  cnf(c207,plain,~front(X142)|nonhuman(X142),inference(split_conjunct,[status(thm)],[c206])).
% 0.83/0.98  cnf(c343,plain,nonhuman(skolem0001),inference(resolution,[status(thm)],[c207, c49])).
% 0.83/0.98  cnf(c344,plain,~human(skolem0001),inference(resolution,[status(thm)],[c343, c102])).
% 0.83/0.98  fof(ax7,axiom,(![U]:(seat(U)=>furniture(U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax7)).
% 0.83/0.98  fof(c202,plain,(![U]:(~seat(U)|furniture(U))),inference(fof_nnf,[status(thm)],[ax7])).
% 0.83/0.98  fof(c203,plain,(![X60]:(~seat(X60)|furniture(X60))),inference(variable_rename,[status(thm)],[c202])).
% 0.83/0.98  cnf(c204,plain,~seat(X139)|furniture(X139),inference(split_conjunct,[status(thm)],[c203])).
% 0.83/0.98  fof(ax24,axiom,(![U]:(object(U)=>entity(U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax24)).
% 0.83/0.98  fof(c148,plain,(![U]:(~object(U)|entity(U))),inference(fof_nnf,[status(thm)],[ax24])).
% 0.83/0.98  fof(c149,plain,(![X43]:(~object(X43)|entity(X43))),inference(variable_rename,[status(thm)],[c148])).
% 0.83/0.98  cnf(c150,plain,~object(X102)|entity(X102),inference(split_conjunct,[status(thm)],[c149])).
% 0.83/0.98  cnf(c331,plain,entity(skolem0001),inference(resolution,[status(thm)],[c330, c150])).
% 0.83/0.98  cnf(c337,plain,~abstraction(skolem0001),inference(resolution,[status(thm)],[c331, c139])).
% 0.83/0.98  cnf(c336,plain,~eventuality(skolem0001),inference(resolution,[status(thm)],[c331, c143])).
% 0.83/0.98  fof(ax12,axiom,(![U]:(way(U)=>(~instrumentality(U)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax12)).
% 0.83/0.98  fof(c185,plain,(![U]:(way(U)=>~instrumentality(U))),inference(fof_simplification,[status(thm)],[ax12])).
% 0.83/0.98  fof(c186,plain,(![U]:(~way(U)|~instrumentality(U))),inference(fof_nnf,[status(thm)],[c185])).
% 0.83/0.98  fof(c187,plain,(![X55]:(~way(X55)|~instrumentality(X55))),inference(variable_rename,[status(thm)],[c186])).
% 0.83/0.98  cnf(c188,plain,~way(X126)|~instrumentality(X126),inference(split_conjunct,[status(thm)],[c187])).
% 0.83/0.98  cnf(c329,plain,~way(skolem0001),inference(resolution,[status(thm)],[c327, c188])).
% 0.83/0.98  fof(ax9,axiom,(![U]:(furniture(U)=>(~transport(U)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax9)).
% 0.83/0.98  fof(c195,plain,(![U]:(furniture(U)=>~transport(U))),inference(fof_simplification,[status(thm)],[ax9])).
% 0.83/0.98  fof(c196,plain,(![U]:(~furniture(U)|~transport(U))),inference(fof_nnf,[status(thm)],[c195])).
% 0.83/0.98  fof(c197,plain,(![X58]:(~furniture(X58)|~transport(X58))),inference(variable_rename,[status(thm)],[c196])).
% 0.83/0.98  cnf(c198,plain,~furniture(X133)|~transport(X133),inference(split_conjunct,[status(thm)],[c197])).
% 0.83/0.98  cnf(c322,plain,~furniture(skolem0005),inference(resolution,[status(thm)],[c198, c291])).
% 0.83/0.98  fof(ax10,axiom,(![U]:(street(U)=>way(U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax10)).
% 0.83/0.98  fof(c192,plain,(![U]:(~street(U)|way(U))),inference(fof_nnf,[status(thm)],[ax10])).
% 0.83/0.98  fof(c193,plain,(![X57]:(~street(X57)|way(X57))),inference(variable_rename,[status(thm)],[c192])).
% 0.83/0.98  cnf(c194,plain,~street(X132)|way(X132),inference(split_conjunct,[status(thm)],[c193])).
% 0.83/0.98  cnf(c314,plain,entity(skolem0004),inference(resolution,[status(thm)],[c313, c150])).
% 0.83/0.98  cnf(c316,plain,~abstraction(skolem0004),inference(resolution,[status(thm)],[c314, c139])).
% 0.83/0.98  cnf(c315,plain,~eventuality(skolem0004),inference(resolution,[status(thm)],[c314, c143])).
% 0.83/0.98  cnf(c307,plain,~way(skolem0005),inference(resolution,[status(thm)],[c188, c292])).
% 0.83/0.98  fof(ax13,axiom,(![U]:(chevy(U)=>car(U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax13)).
% 0.83/0.98  fof(c182,plain,(![U]:(~chevy(U)|car(U))),inference(fof_nnf,[status(thm)],[ax13])).
% 0.83/0.98  fof(c183,plain,(![X54]:(~chevy(X54)|car(X54))),inference(variable_rename,[status(thm)],[c182])).
% 0.83/0.98  cnf(c184,plain,~chevy(X125)|car(X125),inference(split_conjunct,[status(thm)],[c183])).
% 0.83/0.98  cnf(c299,plain,entity(skolem0005),inference(resolution,[status(thm)],[c298, c150])).
% 0.83/0.98  cnf(c301,plain,~abstraction(skolem0005),inference(resolution,[status(thm)],[c299, c139])).
% 0.83/0.98  cnf(c300,plain,~eventuality(skolem0005),inference(resolution,[status(thm)],[c299, c143])).
% 0.83/0.98  fof(ax19,axiom,(![U]:(artifact(U)=>(~location(U)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax19)).
% 0.83/0.98  fof(c163,plain,(![U]:(artifact(U)=>~location(U))),inference(fof_simplification,[status(thm)],[ax19])).
% 0.83/0.98  fof(c164,plain,(![U]:(~artifact(U)|~location(U))),inference(fof_nnf,[status(thm)],[c163])).
% 0.83/0.98  fof(c165,plain,(![X48]:(~artifact(X48)|~location(X48))),inference(variable_rename,[status(thm)],[c164])).
% 0.83/0.98  cnf(c166,plain,~artifact(X113)|~location(X113),inference(split_conjunct,[status(thm)],[c165])).
% 0.83/0.98  cnf(c285,plain,~artifact(skolem0002),inference(resolution,[status(thm)],[c166, c269])).
% 0.83/0.98  fof(ax28,axiom,(![U]:(abstraction(U)=>(~eventuality(U)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax28)).
% 0.83/0.98  fof(c132,plain,(![U]:(abstraction(U)=>~eventuality(U))),inference(fof_simplification,[status(thm)],[ax28])).
% 0.83/0.98  fof(c133,plain,(![U]:(~abstraction(U)|~eventuality(U))),inference(fof_nnf,[status(thm)],[c132])).
% 0.83/0.98  fof(c134,plain,(![X39]:(~abstraction(X39)|~eventuality(X39))),inference(variable_rename,[status(thm)],[c133])).
% 0.83/0.98  cnf(c135,plain,~abstraction(X96)|~eventuality(X96),inference(split_conjunct,[status(thm)],[c134])).
% 0.83/0.98  cnf(c52,negated_conjecture,event(skolem0003),inference(split_conjunct,[status(thm)],[c46])).
% 0.83/0.98  fof(ax20,axiom,(![U]:(event(U)=>eventuality(U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax20)).
% 0.83/0.98  fof(c160,plain,(![U]:(~event(U)|eventuality(U))),inference(fof_nnf,[status(thm)],[ax20])).
% 0.83/0.98  fof(c161,plain,(![X47]:(~event(X47)|eventuality(X47))),inference(variable_rename,[status(thm)],[c160])).
% 0.83/0.98  cnf(c162,plain,~event(X110)|eventuality(X110),inference(split_conjunct,[status(thm)],[c161])).
% 0.83/0.98  cnf(c279,plain,eventuality(skolem0003),inference(resolution,[status(thm)],[c162, c52])).
% 0.83/0.98  cnf(c280,plain,~abstraction(skolem0003),inference(resolution,[status(thm)],[c279, c135])).
% 0.83/0.98  fof(ax21,axiom,(![U]:(hollywood(U)=>city(U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax21)).
% 0.83/0.98  fof(c157,plain,(![U]:(~hollywood(U)|city(U))),inference(fof_nnf,[status(thm)],[ax21])).
% 0.83/0.98  fof(c158,plain,(![X46]:(~hollywood(X46)|city(X46))),inference(variable_rename,[status(thm)],[c157])).
% 0.83/0.98  cnf(c159,plain,~hollywood(X109)|city(X109),inference(split_conjunct,[status(thm)],[c158])).
% 0.83/0.98  cnf(c271,plain,entity(skolem0002),inference(resolution,[status(thm)],[c270, c150])).
% 0.83/0.98  cnf(c273,plain,~abstraction(skolem0002),inference(resolution,[status(thm)],[c271, c139])).
% 0.83/0.98  cnf(c272,plain,~eventuality(skolem0002),inference(resolution,[status(thm)],[c271, c143])).
% 0.83/0.98  fof(ax25,axiom,(![U]:(old(U)=>(~new(U)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax25)).
% 0.83/0.98  fof(c144,plain,(![U]:(old(U)=>~new(U))),inference(fof_simplification,[status(thm)],[ax25])).
% 0.83/0.98  fof(c145,plain,(![U]:(~old(U)|~new(U))),inference(fof_nnf,[status(thm)],[c144])).
% 0.83/0.98  fof(c146,plain,(![X42]:(~old(X42)|~new(X42))),inference(variable_rename,[status(thm)],[c145])).
% 0.83/0.98  cnf(c147,plain,~old(X101)|~new(X101),inference(split_conjunct,[status(thm)],[c146])).
% 0.83/0.98  fof(ax29,axiom,(![U]:(male(U)=>(~female(U)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax29)).
% 0.83/0.98  fof(c128,plain,(![U]:(male(U)=>~female(U))),inference(fof_simplification,[status(thm)],[ax29])).
% 0.83/0.98  fof(c129,plain,(![U]:(~male(U)|~female(U))),inference(fof_nnf,[status(thm)],[c128])).
% 0.83/0.98  fof(c130,plain,(![X38]:(~male(X38)|~female(X38))),inference(variable_rename,[status(thm)],[c129])).
% 0.83/0.98  cnf(c131,plain,~male(X95)|~female(X95),inference(split_conjunct,[status(thm)],[c130])).
% 0.83/0.98  fof(ax30,axiom,(![U]:(man(U)=>(~woman(U)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax30)).
% 0.83/0.98  fof(c124,plain,(![U]:(man(U)=>~woman(U))),inference(fof_simplification,[status(thm)],[ax30])).
% 0.83/0.98  fof(c125,plain,(![U]:(~man(U)|~woman(U))),inference(fof_nnf,[status(thm)],[c124])).
% 0.83/0.98  fof(c126,plain,(![X37]:(~man(X37)|~woman(X37))),inference(variable_rename,[status(thm)],[c125])).
% 0.83/0.98  cnf(c127,plain,~man(X94)|~woman(X94),inference(split_conjunct,[status(thm)],[c126])).
% 0.83/0.98  fof(ax33,axiom,(![U]:(female(U)=>human(U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax33)).
% 0.83/0.98  fof(c115,plain,(![U]:(~female(U)|human(U))),inference(fof_nnf,[status(thm)],[ax33])).
% 0.83/0.98  fof(c116,plain,(![X34]:(~female(X34)|human(X34))),inference(variable_rename,[status(thm)],[c115])).
% 0.83/0.98  cnf(c117,plain,~female(X89)|human(X89),inference(split_conjunct,[status(thm)],[c116])).
% 0.83/0.98  cnf(c4,axiom,X87!=X88|~entity(X87)|entity(X88),theory(equality)).
% 0.83/0.98  fof(ax34,axiom,(![U]:(woman(U)=>female(U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax34)).
% 0.83/0.98  fof(c112,plain,(![U]:(~woman(U)|female(U))),inference(fof_nnf,[status(thm)],[ax34])).
% 0.83/0.98  fof(c113,plain,(![X33]:(~woman(X33)|female(X33))),inference(variable_rename,[status(thm)],[c112])).
% 0.83/0.98  cnf(c114,plain,~woman(X86)|female(X86),inference(split_conjunct,[status(thm)],[c113])).
% 0.83/0.98  fof(ax35,axiom,(![U]:(drs(U)<=>proposition(U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax35)).
% 0.83/0.98  fof(c106,plain,(![U]:((~drs(U)|proposition(U))&(~proposition(U)|drs(U)))),inference(fof_nnf,[status(thm)],[ax35])).
% 0.83/0.98  fof(c107,plain,((![U]:(~drs(U)|proposition(U)))&(![U]:(~proposition(U)|drs(U)))),inference(shift_quantors,[status(thm)],[c106])).
% 0.83/0.98  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.83/0.98  cnf(c111,plain,~proposition(X85)|drs(X85),inference(split_conjunct,[status(thm)],[c109])).
% 0.83/0.98  cnf(c110,plain,~drs(X84)|proposition(X84),inference(split_conjunct,[status(thm)],[c109])).
% 0.83/0.98  fof(ax36,axiom,(![U]:(nonhuman(U)=>entity(U))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax36)).
% 0.83/0.98  fof(c103,plain,(![U]:(~nonhuman(U)|entity(U))),inference(fof_nnf,[status(thm)],[ax36])).
% 0.83/0.98  fof(c104,plain,(![X30]:(~nonhuman(X30)|entity(X30))),inference(variable_rename,[status(thm)],[c103])).
% 0.83/0.98  cnf(c105,plain,~nonhuman(X83)|entity(X83),inference(split_conjunct,[status(thm)],[c104])).
% 0.83/0.98  cnf(c3,axiom,X80!=X81|~organism(X80)|organism(X81),theory(equality)).
% 0.83/0.98  cnf(c2,axiom,X78!=X79|~human(X78)|human(X79),theory(equality)).
% 0.83/0.98  cnf(c1,axiom,X75!=X76|~man(X75)|man(X76),theory(equality)).
% 0.83/0.98  cnf(c60,negated_conjecture,old(skolem0005),inference(split_conjunct,[status(thm)],[c46])).
% 0.83/0.98  cnf(c59,negated_conjecture,dirty(skolem0005),inference(split_conjunct,[status(thm)],[c46])).
% 0.83/0.98  cnf(c58,negated_conjecture,white(skolem0005),inference(split_conjunct,[status(thm)],[c46])).
% 0.83/0.98  cnf(c56,negated_conjecture,chevy(skolem0005),inference(split_conjunct,[status(thm)],[c46])).
% 0.83/0.98  cnf(c55,negated_conjecture,lonely(skolem0004),inference(split_conjunct,[status(thm)],[c46])).
% 0.83/0.98  cnf(c53,negated_conjecture,street(skolem0004),inference(split_conjunct,[status(thm)],[c46])).
% 0.83/0.98  cnf(c50,negated_conjecture,hollywood(skolem0002),inference(split_conjunct,[status(thm)],[c46])).
% 0.83/0.98  cnf(c47,negated_conjecture,seat(skolem0001),inference(split_conjunct,[status(thm)],[c46])).
% 0.83/0.98  % SZS output end Saturation
% 0.83/0.98  
% 0.83/0.98  % Initial clauses    : 120
% 0.83/0.98  % Processed clauses  : 551
% 0.83/0.98  % Factors computed   : 2
% 0.83/0.98  % Resolvents computed: 652
% 0.83/0.98  % Tautologies deleted: 38
% 0.83/0.98  % Forward subsumed   : 185
% 0.83/0.98  % Backward subsumed  : 4
% 0.83/0.98  % -------- CPU Time ---------
% 0.83/0.98  % User time          : 0.616 s
% 0.83/0.98  % System time        : 0.016 s
% 0.83/0.98  % Total time         : 0.632 s
%------------------------------------------------------------------------------