PyRes---1.5.CSA-Sat.s

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

% Computer : n019.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Thu May  9 17:34:26 EDT 2024

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

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12  % Problem  : NLP154+1 : TPTP v8.1.2. Released v2.4.0.
% 0.03/0.13  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34  % Computer : n019.cluster.edu
% 0.14/0.34  % Model    : x86_64 x86_64
% 0.14/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34  % Memory   : 8042.1875MB
% 0.14/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34  % CPULimit : 300
% 0.14/0.34  % WCLimit  : 300
% 0.14/0.34  % DateTime : Wed May  8 13:23:07 EDT 2024
% 0.14/0.34  % CPUTime  : 
% 0.80/0.97  % Version:  1.5
% 0.80/0.97  % SZS status CounterSatisfiable
% 0.80/0.97  % SZS output start Saturation
% 0.80/0.97  fof(co1,conjecture,(~((?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(((((((((((((((of(U,W,V)&city(U,V))&hollywood_placename(U,W))&placename(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&street(U,Y))&lonely(U,Y))&event(U,Z))&agent(U,Z,X))&present(U,Z))&barrel(U,Z))&down(U,Z,Y))&in(U,Z,V)))))))))&(~(?[X1]:(actual_world(X1)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X2]:(((((((((((((((((((of(X1,W,V)&city(X1,V))&hollywood_placename(X1,W))&placename(X1,W))&chevy(X1,X))&white(X1,X))&dirty(X1,X))&old(X1,X))&street(X1,Y))&lonely(X1,Y))&event(X1,Z))&agent(X1,Z,X))&present(X1,Z))&barrel(X1,Z))&down(X1,Z,Y))&in(X1,Z,V))&(![X3]:((frontseat(X1,X3)&member(X1,X3,X2))=>(?[X4]:(?[X5]:((state(X1,X4)&be(X1,X4,X3,X5))&in(X1,X5,X3)))))))&two(X1,X2))&group(X1,X2))&(![X6]:(member(X1,X6,X2)=>(fellow(X1,X6)&young(X1,X6)))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', co1)).
% 0.80/0.97  fof(c59,negated_conjecture,(~(~((?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(((((((((((((((of(U,W,V)&city(U,V))&hollywood_placename(U,W))&placename(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&street(U,Y))&lonely(U,Y))&event(U,Z))&agent(U,Z,X))&present(U,Z))&barrel(U,Z))&down(U,Z,Y))&in(U,Z,V)))))))))&(~(?[X1]:(actual_world(X1)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X2]:(((((((((((((((((((of(X1,W,V)&city(X1,V))&hollywood_placename(X1,W))&placename(X1,W))&chevy(X1,X))&white(X1,X))&dirty(X1,X))&old(X1,X))&street(X1,Y))&lonely(X1,Y))&event(X1,Z))&agent(X1,Z,X))&present(X1,Z))&barrel(X1,Z))&down(X1,Z,Y))&in(X1,Z,V))&(![X3]:((frontseat(X1,X3)&member(X1,X3,X2))=>(?[X4]:(?[X5]:((state(X1,X4)&be(X1,X4,X3,X5))&in(X1,X5,X3)))))))&two(X1,X2))&group(X1,X2))&(![X6]:(member(X1,X6,X2)=>(fellow(X1,X6)&young(X1,X6))))))))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 0.80/0.97  fof(c60,negated_conjecture,((?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(((((((((((((((of(U,W,V)&city(U,V))&hollywood_placename(U,W))&placename(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&street(U,Y))&lonely(U,Y))&event(U,Z))&agent(U,Z,X))&present(U,Z))&barrel(U,Z))&down(U,Z,Y))&in(U,Z,V)))))))))&(![X1]:(~actual_world(X1)|(![V]:(![W]:(![X]:(![Y]:(![Z]:(![X2]:(((((((((((((((((((~of(X1,W,V)|~city(X1,V))|~hollywood_placename(X1,W))|~placename(X1,W))|~chevy(X1,X))|~white(X1,X))|~dirty(X1,X))|~old(X1,X))|~street(X1,Y))|~lonely(X1,Y))|~event(X1,Z))|~agent(X1,Z,X))|~present(X1,Z))|~barrel(X1,Z))|~down(X1,Z,Y))|~in(X1,Z,V))|(?[X3]:((frontseat(X1,X3)&member(X1,X3,X2))&(![X4]:(![X5]:((~state(X1,X4)|~be(X1,X4,X3,X5))|~in(X1,X5,X3)))))))|~two(X1,X2))|~group(X1,X2))|(?[X6]:(member(X1,X6,X2)&(~fellow(X1,X6)|~young(X1,X6)))))))))))))),inference(fof_nnf,[status(thm)],[c59])).
% 0.80/0.97  fof(c61,negated_conjecture,((?[X2]:(actual_world(X2)&(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(((((((((((((((of(X2,X4,X3)&city(X2,X3))&hollywood_placename(X2,X4))&placename(X2,X4))&chevy(X2,X5))&white(X2,X5))&dirty(X2,X5))&old(X2,X5))&street(X2,X6))&lonely(X2,X6))&event(X2,X7))&agent(X2,X7,X5))&present(X2,X7))&barrel(X2,X7))&down(X2,X7,X6))&in(X2,X7,X3)))))))))&(![X8]:(~actual_world(X8)|(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(((((((((((((((((((~of(X8,X10,X9)|~city(X8,X9))|~hollywood_placename(X8,X10))|~placename(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~street(X8,X12))|~lonely(X8,X12))|~event(X8,X13))|~agent(X8,X13,X11))|~present(X8,X13))|~barrel(X8,X13))|~down(X8,X13,X12))|~in(X8,X13,X9))|(?[X15]:((frontseat(X8,X15)&member(X8,X15,X14))&(![X16]:(![X17]:((~state(X8,X16)|~be(X8,X16,X15,X17))|~in(X8,X17,X15)))))))|~two(X8,X14))|~group(X8,X14))|(?[X18]:(member(X8,X18,X14)&(~fellow(X8,X18)|~young(X8,X18)))))))))))))),inference(variable_rename,[status(thm)],[c60])).
% 0.80/0.97  fof(c63,negated_conjecture,(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X16]:(![X17]:((actual_world(skolem0001)&(((((((((((((((of(skolem0001,skolem0003,skolem0002)&city(skolem0001,skolem0002))&hollywood_placename(skolem0001,skolem0003))&placename(skolem0001,skolem0003))&chevy(skolem0001,skolem0004))&white(skolem0001,skolem0004))&dirty(skolem0001,skolem0004))&old(skolem0001,skolem0004))&street(skolem0001,skolem0005))&lonely(skolem0001,skolem0005))&event(skolem0001,skolem0006))&agent(skolem0001,skolem0006,skolem0004))&present(skolem0001,skolem0006))&barrel(skolem0001,skolem0006))&down(skolem0001,skolem0006,skolem0005))&in(skolem0001,skolem0006,skolem0002)))&(~actual_world(X8)|(((((((((((((((((((~of(X8,X10,X9)|~city(X8,X9))|~hollywood_placename(X8,X10))|~placename(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~street(X8,X12))|~lonely(X8,X12))|~event(X8,X13))|~agent(X8,X13,X11))|~present(X8,X13))|~barrel(X8,X13))|~down(X8,X13,X12))|~in(X8,X13,X9))|((frontseat(X8,skolem0007(X8,X9,X10,X11,X12,X13,X14))&member(X8,skolem0007(X8,X9,X10,X11,X12,X13,X14),X14))&((~state(X8,X16)|~be(X8,X16,skolem0007(X8,X9,X10,X11,X12,X13,X14),X17))|~in(X8,X17,skolem0007(X8,X9,X10,X11,X12,X13,X14)))))|~two(X8,X14))|~group(X8,X14))|(member(X8,skolem0008(X8,X9,X10,X11,X12,X13,X14),X14)&(~fellow(X8,skolem0008(X8,X9,X10,X11,X12,X13,X14))|~young(X8,skolem0008(X8,X9,X10,X11,X12,X13,X14)))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c62,negated_conjecture,((actual_world(skolem0001)&(((((((((((((((of(skolem0001,skolem0003,skolem0002)&city(skolem0001,skolem0002))&hollywood_placename(skolem0001,skolem0003))&placename(skolem0001,skolem0003))&chevy(skolem0001,skolem0004))&white(skolem0001,skolem0004))&dirty(skolem0001,skolem0004))&old(skolem0001,skolem0004))&street(skolem0001,skolem0005))&lonely(skolem0001,skolem0005))&event(skolem0001,skolem0006))&agent(skolem0001,skolem0006,skolem0004))&present(skolem0001,skolem0006))&barrel(skolem0001,skolem0006))&down(skolem0001,skolem0006,skolem0005))&in(skolem0001,skolem0006,skolem0002)))&(![X8]:(~actual_world(X8)|(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(((((((((((((((((((~of(X8,X10,X9)|~city(X8,X9))|~hollywood_placename(X8,X10))|~placename(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~street(X8,X12))|~lonely(X8,X12))|~event(X8,X13))|~agent(X8,X13,X11))|~present(X8,X13))|~barrel(X8,X13))|~down(X8,X13,X12))|~in(X8,X13,X9))|((frontseat(X8,skolem0007(X8,X9,X10,X11,X12,X13,X14))&member(X8,skolem0007(X8,X9,X10,X11,X12,X13,X14),X14))&(![X16]:(![X17]:((~state(X8,X16)|~be(X8,X16,skolem0007(X8,X9,X10,X11,X12,X13,X14),X17))|~in(X8,X17,skolem0007(X8,X9,X10,X11,X12,X13,X14)))))))|~two(X8,X14))|~group(X8,X14))|(member(X8,skolem0008(X8,X9,X10,X11,X12,X13,X14),X14)&(~fellow(X8,skolem0008(X8,X9,X10,X11,X12,X13,X14))|~young(X8,skolem0008(X8,X9,X10,X11,X12,X13,X14)))))))))))))),inference(skolemize,[status(esa)],[c61])).])).
% 0.80/0.97  fof(c64,negated_conjecture,(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X16]:(![X17]:((actual_world(skolem0001)&(((((((((((((((of(skolem0001,skolem0003,skolem0002)&city(skolem0001,skolem0002))&hollywood_placename(skolem0001,skolem0003))&placename(skolem0001,skolem0003))&chevy(skolem0001,skolem0004))&white(skolem0001,skolem0004))&dirty(skolem0001,skolem0004))&old(skolem0001,skolem0004))&street(skolem0001,skolem0005))&lonely(skolem0001,skolem0005))&event(skolem0001,skolem0006))&agent(skolem0001,skolem0006,skolem0004))&present(skolem0001,skolem0006))&barrel(skolem0001,skolem0006))&down(skolem0001,skolem0006,skolem0005))&in(skolem0001,skolem0006,skolem0002)))&((((~actual_world(X8)|(((((((((((((((((((~of(X8,X10,X9)|~city(X8,X9))|~hollywood_placename(X8,X10))|~placename(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~street(X8,X12))|~lonely(X8,X12))|~event(X8,X13))|~agent(X8,X13,X11))|~present(X8,X13))|~barrel(X8,X13))|~down(X8,X13,X12))|~in(X8,X13,X9))|frontseat(X8,skolem0007(X8,X9,X10,X11,X12,X13,X14)))|~two(X8,X14))|~group(X8,X14))|member(X8,skolem0008(X8,X9,X10,X11,X12,X13,X14),X14)))&(~actual_world(X8)|(((((((((((((((((((~of(X8,X10,X9)|~city(X8,X9))|~hollywood_placename(X8,X10))|~placename(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~street(X8,X12))|~lonely(X8,X12))|~event(X8,X13))|~agent(X8,X13,X11))|~present(X8,X13))|~barrel(X8,X13))|~down(X8,X13,X12))|~in(X8,X13,X9))|frontseat(X8,skolem0007(X8,X9,X10,X11,X12,X13,X14)))|~two(X8,X14))|~group(X8,X14))|(~fellow(X8,skolem0008(X8,X9,X10,X11,X12,X13,X14))|~young(X8,skolem0008(X8,X9,X10,X11,X12,X13,X14))))))&((~actual_world(X8)|(((((((((((((((((((~of(X8,X10,X9)|~city(X8,X9))|~hollywood_placename(X8,X10))|~placename(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~street(X8,X12))|~lonely(X8,X12))|~event(X8,X13))|~agent(X8,X13,X11))|~present(X8,X13))|~barrel(X8,X13))|~down(X8,X13,X12))|~in(X8,X13,X9))|member(X8,skolem0007(X8,X9,X10,X11,X12,X13,X14),X14))|~two(X8,X14))|~group(X8,X14))|member(X8,skolem0008(X8,X9,X10,X11,X12,X13,X14),X14)))&(~actual_world(X8)|(((((((((((((((((((~of(X8,X10,X9)|~city(X8,X9))|~hollywood_placename(X8,X10))|~placename(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~street(X8,X12))|~lonely(X8,X12))|~event(X8,X13))|~agent(X8,X13,X11))|~present(X8,X13))|~barrel(X8,X13))|~down(X8,X13,X12))|~in(X8,X13,X9))|member(X8,skolem0007(X8,X9,X10,X11,X12,X13,X14),X14))|~two(X8,X14))|~group(X8,X14))|(~fellow(X8,skolem0008(X8,X9,X10,X11,X12,X13,X14))|~young(X8,skolem0008(X8,X9,X10,X11,X12,X13,X14)))))))&((~actual_world(X8)|(((((((((((((((((((~of(X8,X10,X9)|~city(X8,X9))|~hollywood_placename(X8,X10))|~placename(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~street(X8,X12))|~lonely(X8,X12))|~event(X8,X13))|~agent(X8,X13,X11))|~present(X8,X13))|~barrel(X8,X13))|~down(X8,X13,X12))|~in(X8,X13,X9))|((~state(X8,X16)|~be(X8,X16,skolem0007(X8,X9,X10,X11,X12,X13,X14),X17))|~in(X8,X17,skolem0007(X8,X9,X10,X11,X12,X13,X14))))|~two(X8,X14))|~group(X8,X14))|member(X8,skolem0008(X8,X9,X10,X11,X12,X13,X14),X14)))&(~actual_world(X8)|(((((((((((((((((((~of(X8,X10,X9)|~city(X8,X9))|~hollywood_placename(X8,X10))|~placename(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~street(X8,X12))|~lonely(X8,X12))|~event(X8,X13))|~agent(X8,X13,X11))|~present(X8,X13))|~barrel(X8,X13))|~down(X8,X13,X12))|~in(X8,X13,X9))|((~state(X8,X16)|~be(X8,X16,skolem0007(X8,X9,X10,X11,X12,X13,X14),X17))|~in(X8,X17,skolem0007(X8,X9,X10,X11,X12,X13,X14))))|~two(X8,X14))|~group(X8,X14))|(~fellow(X8,skolem0008(X8,X9,X10,X11,X12,X13,X14))|~young(X8,skolem0008(X8,X9,X10,X11,X12,X13,X14))))))))))))))))),inference(distribute,[status(thm)],[c63])).
% 0.80/0.97  cnf(c66,negated_conjecture,of(skolem0001,skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c64])).
% 0.80/0.97  cnf(c77,negated_conjecture,agent(skolem0001,skolem0006,skolem0004),inference(split_conjunct,[status(thm)],[c64])).
% 0.80/0.97  cnf(c80,negated_conjecture,down(skolem0001,skolem0006,skolem0005),inference(split_conjunct,[status(thm)],[c64])).
% 0.80/0.97  cnf(c81,negated_conjecture,in(skolem0001,skolem0006,skolem0002),inference(split_conjunct,[status(thm)],[c64])).
% 0.80/0.97  cnf(c84,negated_conjecture,~actual_world(X729)|~of(X729,X730,X731)|~city(X729,X731)|~hollywood_placename(X729,X730)|~placename(X729,X730)|~chevy(X729,X728)|~white(X729,X728)|~dirty(X729,X728)|~old(X729,X728)|~street(X729,X732)|~lonely(X729,X732)|~event(X729,X726)|~agent(X729,X726,X728)|~present(X729,X726)|~barrel(X729,X726)|~down(X729,X726,X732)|~in(X729,X726,X731)|member(X729,skolem0007(X729,X731,X730,X728,X732,X726,X727),X727)|~two(X729,X727)|~group(X729,X727)|member(X729,skolem0008(X729,X731,X730,X728,X732,X726,X727),X727),inference(split_conjunct,[status(thm)],[c64])).
% 0.80/0.97  cnf(c533,plain,~actual_world(skolem0001)|~of(skolem0001,X826,skolem0002)|~city(skolem0001,skolem0002)|~hollywood_placename(skolem0001,X826)|~placename(skolem0001,X826)|~chevy(skolem0001,X827)|~white(skolem0001,X827)|~dirty(skolem0001,X827)|~old(skolem0001,X827)|~street(skolem0001,X829)|~lonely(skolem0001,X829)|~event(skolem0001,skolem0006)|~agent(skolem0001,skolem0006,X827)|~present(skolem0001,skolem0006)|~barrel(skolem0001,skolem0006)|~down(skolem0001,skolem0006,X829)|member(skolem0001,skolem0007(skolem0001,skolem0002,X826,X827,X829,skolem0006,X828),X828)|~two(skolem0001,X828)|~group(skolem0001,X828)|member(skolem0001,skolem0008(skolem0001,skolem0002,X826,X827,X829,skolem0006,X828),X828),inference(resolution,[status(thm)],[c84, c81])).
% 0.80/0.97  cnf(c559,plain,~actual_world(skolem0001)|~of(skolem0001,X833,skolem0002)|~city(skolem0001,skolem0002)|~hollywood_placename(skolem0001,X833)|~placename(skolem0001,X833)|~chevy(skolem0001,X831)|~white(skolem0001,X831)|~dirty(skolem0001,X831)|~old(skolem0001,X831)|~street(skolem0001,skolem0005)|~lonely(skolem0001,skolem0005)|~event(skolem0001,skolem0006)|~agent(skolem0001,skolem0006,X831)|~present(skolem0001,skolem0006)|~barrel(skolem0001,skolem0006)|member(skolem0001,skolem0007(skolem0001,skolem0002,X833,X831,skolem0005,skolem0006,X832),X832)|~two(skolem0001,X832)|~group(skolem0001,X832)|member(skolem0001,skolem0008(skolem0001,skolem0002,X833,X831,skolem0005,skolem0006,X832),X832),inference(resolution,[status(thm)],[c533, c80])).
% 0.80/0.97  cnf(c560,plain,~actual_world(skolem0001)|~of(skolem0001,X834,skolem0002)|~city(skolem0001,skolem0002)|~hollywood_placename(skolem0001,X834)|~placename(skolem0001,X834)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~street(skolem0001,skolem0005)|~lonely(skolem0001,skolem0005)|~event(skolem0001,skolem0006)|~present(skolem0001,skolem0006)|~barrel(skolem0001,skolem0006)|member(skolem0001,skolem0007(skolem0001,skolem0002,X834,skolem0004,skolem0005,skolem0006,X835),X835)|~two(skolem0001,X835)|~group(skolem0001,X835)|member(skolem0001,skolem0008(skolem0001,skolem0002,X834,skolem0004,skolem0005,skolem0006,X835),X835),inference(resolution,[status(thm)],[c559, c77])).
% 0.80/0.97  cnf(c561,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0002)|~hollywood_placename(skolem0001,skolem0003)|~placename(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~street(skolem0001,skolem0005)|~lonely(skolem0001,skolem0005)|~event(skolem0001,skolem0006)|~present(skolem0001,skolem0006)|~barrel(skolem0001,skolem0006)|member(skolem0001,skolem0007(skolem0001,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,X836),X836)|~two(skolem0001,X836)|~group(skolem0001,X836)|member(skolem0001,skolem0008(skolem0001,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,X836),X836),inference(resolution,[status(thm)],[c560, c66])).
% 0.80/0.97  cnf(c82,negated_conjecture,~actual_world(X705)|~of(X705,X706,X707)|~city(X705,X707)|~hollywood_placename(X705,X706)|~placename(X705,X706)|~chevy(X705,X704)|~white(X705,X704)|~dirty(X705,X704)|~old(X705,X704)|~street(X705,X708)|~lonely(X705,X708)|~event(X705,X702)|~agent(X705,X702,X704)|~present(X705,X702)|~barrel(X705,X702)|~down(X705,X702,X708)|~in(X705,X702,X707)|frontseat(X705,skolem0007(X705,X707,X706,X704,X708,X702,X703))|~two(X705,X703)|~group(X705,X703)|member(X705,skolem0008(X705,X707,X706,X704,X708,X702,X703),X703),inference(split_conjunct,[status(thm)],[c64])).
% 0.80/0.97  cnf(c525,plain,~actual_world(skolem0001)|~of(skolem0001,X817,skolem0002)|~city(skolem0001,skolem0002)|~hollywood_placename(skolem0001,X817)|~placename(skolem0001,X817)|~chevy(skolem0001,X820)|~white(skolem0001,X820)|~dirty(skolem0001,X820)|~old(skolem0001,X820)|~street(skolem0001,X818)|~lonely(skolem0001,X818)|~event(skolem0001,skolem0006)|~agent(skolem0001,skolem0006,X820)|~present(skolem0001,skolem0006)|~barrel(skolem0001,skolem0006)|~down(skolem0001,skolem0006,X818)|frontseat(skolem0001,skolem0007(skolem0001,skolem0002,X817,X820,X818,skolem0006,X819))|~two(skolem0001,X819)|~group(skolem0001,X819)|member(skolem0001,skolem0008(skolem0001,skolem0002,X817,X820,X818,skolem0006,X819),X819),inference(resolution,[status(thm)],[c82, c81])).
% 0.80/0.97  cnf(c556,plain,~actual_world(skolem0001)|~of(skolem0001,X821,skolem0002)|~city(skolem0001,skolem0002)|~hollywood_placename(skolem0001,X821)|~placename(skolem0001,X821)|~chevy(skolem0001,X823)|~white(skolem0001,X823)|~dirty(skolem0001,X823)|~old(skolem0001,X823)|~street(skolem0001,skolem0005)|~lonely(skolem0001,skolem0005)|~event(skolem0001,skolem0006)|~agent(skolem0001,skolem0006,X823)|~present(skolem0001,skolem0006)|~barrel(skolem0001,skolem0006)|frontseat(skolem0001,skolem0007(skolem0001,skolem0002,X821,X823,skolem0005,skolem0006,X822))|~two(skolem0001,X822)|~group(skolem0001,X822)|member(skolem0001,skolem0008(skolem0001,skolem0002,X821,X823,skolem0005,skolem0006,X822),X822),inference(resolution,[status(thm)],[c525, c80])).
% 0.80/0.97  cnf(c557,plain,~actual_world(skolem0001)|~of(skolem0001,X825,skolem0002)|~city(skolem0001,skolem0002)|~hollywood_placename(skolem0001,X825)|~placename(skolem0001,X825)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~street(skolem0001,skolem0005)|~lonely(skolem0001,skolem0005)|~event(skolem0001,skolem0006)|~present(skolem0001,skolem0006)|~barrel(skolem0001,skolem0006)|frontseat(skolem0001,skolem0007(skolem0001,skolem0002,X825,skolem0004,skolem0005,skolem0006,X824))|~two(skolem0001,X824)|~group(skolem0001,X824)|member(skolem0001,skolem0008(skolem0001,skolem0002,X825,skolem0004,skolem0005,skolem0006,X824),X824),inference(resolution,[status(thm)],[c556, c77])).
% 0.80/0.97  cnf(c558,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0002)|~hollywood_placename(skolem0001,skolem0003)|~placename(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~street(skolem0001,skolem0005)|~lonely(skolem0001,skolem0005)|~event(skolem0001,skolem0006)|~present(skolem0001,skolem0006)|~barrel(skolem0001,skolem0006)|frontseat(skolem0001,skolem0007(skolem0001,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,X830))|~two(skolem0001,X830)|~group(skolem0001,X830)|member(skolem0001,skolem0008(skolem0001,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,X830),X830),inference(resolution,[status(thm)],[c557, c66])).
% 0.80/0.97  fof(ax58,axiom,(![U]:(![V]:(![W]:(((entity(U,V)&placename(U,W))&of(U,W,V))=>(~(?[X]:((placename(U,X)&X!=W)&of(U,X,V)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax58)).
% 0.80/0.97  fof(c107,plain,(![U]:(![V]:(![W]:(((~entity(U,V)|~placename(U,W))|~of(U,W,V))|(![X]:((~placename(U,X)|X=W)|~of(U,X,V))))))),inference(fof_nnf,[status(thm)],[ax58])).
% 0.80/0.97  fof(c109,plain,(![X35]:(![X36]:(![X37]:(![X38]:(((~entity(X35,X36)|~placename(X35,X37))|~of(X35,X37,X36))|((~placename(X35,X38)|X38=X37)|~of(X35,X38,X36))))))),inference(shift_quantors,[status(thm)],[fof(c108,plain,(![X35]:(![X36]:(![X37]:(((~entity(X35,X36)|~placename(X35,X37))|~of(X35,X37,X36))|(![X38]:((~placename(X35,X38)|X38=X37)|~of(X35,X38,X36))))))),inference(variable_rename,[status(thm)],[c107])).])).
% 0.80/0.97  cnf(c110,plain,~entity(X802,X804)|~placename(X802,X801)|~of(X802,X801,X804)|~placename(X802,X803)|X803=X801|~of(X802,X803,X804),inference(split_conjunct,[status(thm)],[c109])).
% 0.80/0.97  cnf(c554,plain,~entity(skolem0001,skolem0002)|~placename(skolem0001,X816)|~of(skolem0001,X816,skolem0002)|~placename(skolem0001,skolem0003)|skolem0003=X816,inference(resolution,[status(thm)],[c110, c66])).
% 0.80/0.97  fof(ax60,axiom,(![U]:(![V]:(two(U,V)<=>(?[W]:(member(U,W,V)&(?[X]:((member(U,X,V)&X!=W)&(![Y]:(member(U,Y,V)=>(Y=X|Y=W)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax60)).
% 0.80/0.97  fof(c91,plain,(![U]:(![V]:((~two(U,V)|(?[W]:(member(U,W,V)&(?[X]:((member(U,X,V)&X!=W)&(![Y]:(~member(U,Y,V)|(Y=X|Y=W))))))))&((![W]:(~member(U,W,V)|(![X]:((~member(U,X,V)|X=W)|(?[Y]:(member(U,Y,V)&(Y!=X&Y!=W)))))))|two(U,V))))),inference(fof_nnf,[status(thm)],[ax60])).
% 0.80/0.97  fof(c92,plain,((![U]:(![V]:(~two(U,V)|(?[W]:(member(U,W,V)&(?[X]:((member(U,X,V)&X!=W)&(![Y]:(~member(U,Y,V)|(Y=X|Y=W))))))))))&(![U]:(![V]:((![W]:(~member(U,W,V)|(![X]:((~member(U,X,V)|X=W)|(?[Y]:(member(U,Y,V)&(Y!=X&Y!=W)))))))|two(U,V))))),inference(shift_quantors,[status(thm)],[c91])).
% 0.80/0.97  fof(c93,plain,((![X21]:(![X22]:(~two(X21,X22)|(?[X23]:(member(X21,X23,X22)&(?[X24]:((member(X21,X24,X22)&X24!=X23)&(![X25]:(~member(X21,X25,X22)|(X25=X24|X25=X23))))))))))&(![X26]:(![X27]:((![X28]:(~member(X26,X28,X27)|(![X29]:((~member(X26,X29,X27)|X29=X28)|(?[X30]:(member(X26,X30,X27)&(X30!=X29&X30!=X28)))))))|two(X26,X27))))),inference(variable_rename,[status(thm)],[c92])).
% 0.80/0.97  fof(c95,plain,(![X21]:(![X22]:(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:((~two(X21,X22)|(member(X21,skolem0009(X21,X22),X22)&((member(X21,skolem0010(X21,X22),X22)&skolem0010(X21,X22)!=skolem0009(X21,X22))&(~member(X21,X25,X22)|(X25=skolem0010(X21,X22)|X25=skolem0009(X21,X22))))))&((~member(X26,X28,X27)|((~member(X26,X29,X27)|X29=X28)|(member(X26,skolem0011(X26,X27,X28,X29),X27)&(skolem0011(X26,X27,X28,X29)!=X29&skolem0011(X26,X27,X28,X29)!=X28))))|two(X26,X27)))))))))),inference(shift_quantors,[status(thm)],[fof(c94,plain,((![X21]:(![X22]:(~two(X21,X22)|(member(X21,skolem0009(X21,X22),X22)&((member(X21,skolem0010(X21,X22),X22)&skolem0010(X21,X22)!=skolem0009(X21,X22))&(![X25]:(~member(X21,X25,X22)|(X25=skolem0010(X21,X22)|X25=skolem0009(X21,X22)))))))))&(![X26]:(![X27]:((![X28]:(~member(X26,X28,X27)|(![X29]:((~member(X26,X29,X27)|X29=X28)|(member(X26,skolem0011(X26,X27,X28,X29),X27)&(skolem0011(X26,X27,X28,X29)!=X29&skolem0011(X26,X27,X28,X29)!=X28))))))|two(X26,X27))))),inference(skolemize,[status(esa)],[c93])).])).
% 0.80/0.97  fof(c96,plain,(![X21]:(![X22]:(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:(((~two(X21,X22)|member(X21,skolem0009(X21,X22),X22))&(((~two(X21,X22)|member(X21,skolem0010(X21,X22),X22))&(~two(X21,X22)|skolem0010(X21,X22)!=skolem0009(X21,X22)))&(~two(X21,X22)|(~member(X21,X25,X22)|(X25=skolem0010(X21,X22)|X25=skolem0009(X21,X22))))))&(((~member(X26,X28,X27)|((~member(X26,X29,X27)|X29=X28)|member(X26,skolem0011(X26,X27,X28,X29),X27)))|two(X26,X27))&(((~member(X26,X28,X27)|((~member(X26,X29,X27)|X29=X28)|skolem0011(X26,X27,X28,X29)!=X29))|two(X26,X27))&((~member(X26,X28,X27)|((~member(X26,X29,X27)|X29=X28)|skolem0011(X26,X27,X28,X29)!=X28))|two(X26,X27)))))))))))),inference(distribute,[status(thm)],[c95])).
% 0.80/0.97  cnf(c103,plain,~member(X815,X813,X814)|~member(X815,X812,X814)|X812=X813|skolem0011(X815,X814,X813,X812)!=X813|two(X815,X814),inference(split_conjunct,[status(thm)],[c96])).
% 0.80/0.97  cnf(c102,plain,~member(X811,X809,X810)|~member(X811,X808,X810)|X808=X809|skolem0011(X811,X810,X809,X808)!=X808|two(X811,X810),inference(split_conjunct,[status(thm)],[c96])).
% 0.80/0.97  cnf(c101,plain,~member(X797,X795,X796)|~member(X797,X794,X796)|X794=X795|member(X797,skolem0011(X797,X796,X795,X794),X796)|two(X797,X796),inference(split_conjunct,[status(thm)],[c96])).
% 0.80/0.97  cnf(reflexivity,axiom,X153=X153,theory(equality)).
% 0.80/0.97  cnf(c55,axiom,X669!=X667|X668!=X666|X665!=X664|~agent(X669,X668,X665)|agent(X667,X666,X664),theory(equality)).
% 0.80/0.97  cnf(c508,plain,skolem0001!=X790|skolem0006!=X788|skolem0004!=X789|agent(X790,X788,X789),inference(resolution,[status(thm)],[c55, c77])).
% 0.80/0.97  cnf(c549,plain,skolem0001!=X791|skolem0006!=X792|agent(X791,X792,skolem0004),inference(resolution,[status(thm)],[c508, reflexivity])).
% 0.80/0.97  cnf(c550,plain,skolem0001!=X793|agent(X793,skolem0006,skolem0004),inference(resolution,[status(thm)],[c549, reflexivity])).
% 0.80/0.97  cnf(c53,axiom,X649!=X647|X648!=X646|X645!=X644|~down(X649,X648,X645)|down(X647,X646,X644),theory(equality)).
% 0.80/0.97  cnf(c499,plain,skolem0001!=X779|skolem0006!=X780|skolem0005!=X781|down(X779,X780,X781),inference(resolution,[status(thm)],[c53, c80])).
% 0.80/0.97  cnf(c546,plain,skolem0001!=X783|skolem0006!=X782|down(X783,X782,skolem0005),inference(resolution,[status(thm)],[c499, reflexivity])).
% 0.80/0.97  cnf(c547,plain,skolem0001!=X787|down(X787,skolem0006,skolem0005),inference(resolution,[status(thm)],[c546, reflexivity])).
% 0.80/0.97  cnf(c100,plain,~two(X786,X785)|~member(X786,X784,X785)|X784=skolem0010(X786,X785)|X784=skolem0009(X786,X785),inference(split_conjunct,[status(thm)],[c96])).
% 0.80/0.97  cnf(c52,axiom,X638!=X636|X637!=X635|X634!=X633|~in(X638,X637,X634)|in(X636,X635,X633),theory(equality)).
% 0.80/0.97  cnf(c495,plain,skolem0001!=X764|skolem0006!=X765|skolem0002!=X766|in(X764,X765,X766),inference(resolution,[status(thm)],[c52, c81])).
% 0.80/0.97  cnf(c543,plain,skolem0001!=X776|skolem0006!=X777|in(X776,X777,skolem0002),inference(resolution,[status(thm)],[c495, reflexivity])).
% 0.80/0.97  cnf(c544,plain,skolem0001!=X778|in(X778,skolem0006,skolem0002),inference(resolution,[status(thm)],[c543, reflexivity])).
% 0.80/0.97  cnf(c87,negated_conjecture,~actual_world(X771)|~of(X771,X772,X774)|~city(X771,X774)|~hollywood_placename(X771,X772)|~placename(X771,X772)|~chevy(X771,X770)|~white(X771,X770)|~dirty(X771,X770)|~old(X771,X770)|~street(X771,X775)|~lonely(X771,X775)|~event(X771,X767)|~agent(X771,X767,X770)|~present(X771,X767)|~barrel(X771,X767)|~down(X771,X767,X775)|~in(X771,X767,X774)|~state(X771,X769)|~be(X771,X769,skolem0007(X771,X774,X772,X770,X775,X767,X768),X773)|~in(X771,X773,skolem0007(X771,X774,X772,X770,X775,X767,X768))|~two(X771,X768)|~group(X771,X768)|~fellow(X771,skolem0008(X771,X774,X772,X770,X775,X767,X768))|~young(X771,skolem0008(X771,X774,X772,X770,X775,X767,X768)),inference(split_conjunct,[status(thm)],[c64])).
% 0.80/0.97  cnf(c48,axiom,X603!=X601|X602!=X600|X599!=X598|~of(X603,X602,X599)|of(X601,X600,X598),theory(equality)).
% 0.80/0.97  cnf(c484,plain,skolem0001!=X758|skolem0003!=X760|skolem0002!=X759|of(X758,X760,X759),inference(resolution,[status(thm)],[c48, c66])).
% 0.80/0.97  cnf(c540,plain,skolem0001!=X761|skolem0003!=X762|of(X761,X762,skolem0002),inference(resolution,[status(thm)],[c484, reflexivity])).
% 0.80/0.97  cnf(c541,plain,skolem0001!=X763|of(X763,skolem0003,skolem0002),inference(resolution,[status(thm)],[c540, reflexivity])).
% 0.80/0.97  cnf(c86,negated_conjecture,~actual_world(X753)|~of(X753,X754,X756)|~city(X753,X756)|~hollywood_placename(X753,X754)|~placename(X753,X754)|~chevy(X753,X752)|~white(X753,X752)|~dirty(X753,X752)|~old(X753,X752)|~street(X753,X757)|~lonely(X753,X757)|~event(X753,X749)|~agent(X753,X749,X752)|~present(X753,X749)|~barrel(X753,X749)|~down(X753,X749,X757)|~in(X753,X749,X756)|~state(X753,X751)|~be(X753,X751,skolem0007(X753,X756,X754,X752,X757,X749,X750),X755)|~in(X753,X755,skolem0007(X753,X756,X754,X752,X757,X749,X750))|~two(X753,X750)|~group(X753,X750)|member(X753,skolem0008(X753,X756,X754,X752,X757,X749,X750),X750),inference(split_conjunct,[status(thm)],[c64])).
% 0.80/0.97  cnf(c71,negated_conjecture,white(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c64])).
% 0.80/0.97  cnf(c58,axiom,X696!=X695|X694!=X693|~white(X696,X694)|white(X695,X693),theory(equality)).
% 0.80/0.97  cnf(c521,plain,skolem0001!=X747|skolem0004!=X746|white(X747,X746),inference(resolution,[status(thm)],[c58, c71])).
% 0.80/0.97  cnf(c538,plain,skolem0001!=X748|white(X748,skolem0004),inference(resolution,[status(thm)],[c521, reflexivity])).
% 0.80/0.97  cnf(c72,negated_conjecture,dirty(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c64])).
% 0.80/0.97  cnf(c57,axiom,X686!=X685|X684!=X683|~dirty(X686,X684)|dirty(X685,X683),theory(equality)).
% 0.80/0.97  cnf(c516,plain,skolem0001!=X736|skolem0004!=X737|dirty(X736,X737),inference(resolution,[status(thm)],[c57, c72])).
% 0.80/0.97  cnf(c536,plain,skolem0001!=X745|dirty(X745,skolem0004),inference(resolution,[status(thm)],[c516, reflexivity])).
% 0.80/0.97  cnf(c85,negated_conjecture,~actual_world(X741)|~of(X741,X742,X743)|~city(X741,X743)|~hollywood_placename(X741,X742)|~placename(X741,X742)|~chevy(X741,X740)|~white(X741,X740)|~dirty(X741,X740)|~old(X741,X740)|~street(X741,X744)|~lonely(X741,X744)|~event(X741,X738)|~agent(X741,X738,X740)|~present(X741,X738)|~barrel(X741,X738)|~down(X741,X738,X744)|~in(X741,X738,X743)|member(X741,skolem0007(X741,X743,X742,X740,X744,X738,X739),X739)|~two(X741,X739)|~group(X741,X739)|~fellow(X741,skolem0008(X741,X743,X742,X740,X744,X738,X739))|~young(X741,skolem0008(X741,X743,X742,X740,X744,X738,X739)),inference(split_conjunct,[status(thm)],[c64])).
% 0.80/0.97  cnf(c75,negated_conjecture,lonely(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c64])).
% 0.80/0.97  cnf(c56,axiom,X678!=X677|X676!=X675|~lonely(X678,X676)|lonely(X677,X675),theory(equality)).
% 0.80/0.97  cnf(c512,plain,skolem0001!=X734|skolem0005!=X733|lonely(X734,X733),inference(resolution,[status(thm)],[c56, c75])).
% 0.80/0.97  cnf(c534,plain,skolem0001!=X735|lonely(X735,skolem0005),inference(resolution,[status(thm)],[c512, reflexivity])).
% 0.80/0.97  cnf(c78,negated_conjecture,present(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c64])).
% 0.80/0.97  cnf(c54,axiom,X657!=X656|X655!=X654|~present(X657,X655)|present(X656,X654),theory(equality)).
% 0.80/0.97  cnf(c503,plain,skolem0001!=X724|skolem0006!=X723|present(X724,X723),inference(resolution,[status(thm)],[c54, c78])).
% 0.80/0.97  cnf(c531,plain,skolem0001!=X725|present(X725,skolem0006),inference(resolution,[status(thm)],[c503, reflexivity])).
% 0.80/0.97  cnf(c73,negated_conjecture,old(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c64])).
% 0.80/0.97  cnf(c47,axiom,X591!=X590|X589!=X588|~old(X591,X589)|old(X590,X588),theory(equality)).
% 0.80/0.97  cnf(c479,plain,skolem0001!=X721|skolem0004!=X720|old(X721,X720),inference(resolution,[status(thm)],[c47, c73])).
% 0.80/0.97  cnf(c529,plain,skolem0001!=X722|old(X722,skolem0004),inference(resolution,[status(thm)],[c479, reflexivity])).
% 0.80/0.97  cnf(c83,negated_conjecture,~actual_world(X716)|~of(X716,X717,X718)|~city(X716,X718)|~hollywood_placename(X716,X717)|~placename(X716,X717)|~chevy(X716,X715)|~white(X716,X715)|~dirty(X716,X715)|~old(X716,X715)|~street(X716,X719)|~lonely(X716,X719)|~event(X716,X713)|~agent(X716,X713,X715)|~present(X716,X713)|~barrel(X716,X713)|~down(X716,X713,X719)|~in(X716,X713,X718)|frontseat(X716,skolem0007(X716,X718,X717,X715,X719,X713,X714))|~two(X716,X714)|~group(X716,X714)|~fellow(X716,skolem0008(X716,X718,X717,X715,X719,X713,X714))|~young(X716,skolem0008(X716,X718,X717,X715,X719,X713,X714)),inference(split_conjunct,[status(thm)],[c64])).
% 0.80/0.97  fof(ax44,axiom,(![U]:(![V]:(thing(U,V)=>singleton(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax44)).
% 0.80/0.97  fof(c158,plain,(![U]:(![V]:(~thing(U,V)|singleton(U,V)))),inference(fof_nnf,[status(thm)],[ax44])).
% 0.80/0.97  fof(c159,plain,(![X65]:(![X66]:(~thing(X65,X66)|singleton(X65,X66)))),inference(variable_rename,[status(thm)],[c158])).
% 0.80/0.97  cnf(c160,plain,~thing(X205,X204)|singleton(X205,X204),inference(split_conjunct,[status(thm)],[c159])).
% 0.80/0.97  fof(ax45,axiom,(![U]:(![V]:(entity(U,V)=>thing(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax45)).
% 0.80/0.97  fof(c155,plain,(![U]:(![V]:(~entity(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax45])).
% 0.80/0.97  fof(c156,plain,(![X63]:(![X64]:(~entity(X63,X64)|thing(X63,X64)))),inference(variable_rename,[status(thm)],[c155])).
% 0.80/0.97  cnf(c157,plain,~entity(X203,X202)|thing(X203,X202),inference(split_conjunct,[status(thm)],[c156])).
% 0.80/0.97  fof(ax19,axiom,(![U]:(![V]:(object(U,V)=>entity(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax19)).
% 0.80/0.97  fof(c233,plain,(![U]:(![V]:(~object(U,V)|entity(U,V)))),inference(fof_nnf,[status(thm)],[ax19])).
% 0.80/0.97  fof(c234,plain,(![X115]:(![X116]:(~object(X115,X116)|entity(X115,X116)))),inference(variable_rename,[status(thm)],[c233])).
% 0.80/0.97  cnf(c235,plain,~object(X286,X287)|entity(X286,X287),inference(split_conjunct,[status(thm)],[c234])).
% 0.80/0.97  cnf(c67,negated_conjecture,city(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c64])).
% 0.80/0.97  fof(ax5,axiom,(![U]:(![V]:(city(U,V)=>location(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax5)).
% 0.80/0.97  fof(c275,plain,(![U]:(![V]:(~city(U,V)|location(U,V)))),inference(fof_nnf,[status(thm)],[ax5])).
% 0.80/0.97  fof(c276,plain,(![X143]:(![X144]:(~city(X143,X144)|location(X143,X144)))),inference(variable_rename,[status(thm)],[c275])).
% 0.80/0.97  cnf(c277,plain,~city(X350,X351)|location(X350,X351),inference(split_conjunct,[status(thm)],[c276])).
% 0.80/0.97  cnf(c366,plain,location(skolem0001,skolem0002),inference(resolution,[status(thm)],[c277, c67])).
% 0.80/0.97  fof(ax4,axiom,(![U]:(![V]:(location(U,V)=>object(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax4)).
% 0.80/0.97  fof(c278,plain,(![U]:(![V]:(~location(U,V)|object(U,V)))),inference(fof_nnf,[status(thm)],[ax4])).
% 0.80/0.97  fof(c279,plain,(![X145]:(![X146]:(~location(X145,X146)|object(X145,X146)))),inference(variable_rename,[status(thm)],[c278])).
% 0.80/0.97  cnf(c280,plain,~location(X357,X356)|object(X357,X356),inference(split_conjunct,[status(thm)],[c279])).
% 0.80/0.97  cnf(c370,plain,object(skolem0001,skolem0002),inference(resolution,[status(thm)],[c280, c366])).
% 0.80/0.97  cnf(c374,plain,entity(skolem0001,skolem0002),inference(resolution,[status(thm)],[c370, c235])).
% 0.80/0.97  cnf(c381,plain,thing(skolem0001,skolem0002),inference(resolution,[status(thm)],[c374, c157])).
% 0.80/0.97  cnf(c385,plain,singleton(skolem0001,skolem0002),inference(resolution,[status(thm)],[c381, c160])).
% 0.80/0.97  cnf(c44,axiom,X564!=X563|X562!=X561|~singleton(X564,X562)|singleton(X563,X561),theory(equality)).
% 0.80/0.97  cnf(c468,plain,skolem0001!=X710|skolem0002!=X711|singleton(X710,X711),inference(resolution,[status(thm)],[c44, c385])).
% 0.80/0.97  cnf(c527,plain,skolem0001!=X712|singleton(X712,skolem0002),inference(resolution,[status(thm)],[c468, reflexivity])).
% 0.80/0.97  cnf(c69,negated_conjecture,placename(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c64])).
% 0.80/0.97  fof(ax13,axiom,(![U]:(![V]:(placename(U,V)=>relname(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax13)).
% 0.80/0.97  fof(c251,plain,(![U]:(![V]:(~placename(U,V)|relname(U,V)))),inference(fof_nnf,[status(thm)],[ax13])).
% 0.80/0.97  fof(c252,plain,(![X127]:(![X128]:(~placename(X127,X128)|relname(X127,X128)))),inference(variable_rename,[status(thm)],[c251])).
% 0.80/0.97  cnf(c253,plain,~placename(X323,X322)|relname(X323,X322),inference(split_conjunct,[status(thm)],[c252])).
% 0.80/0.97  cnf(c344,plain,relname(skolem0001,skolem0003),inference(resolution,[status(thm)],[c253, c69])).
% 0.80/0.97  fof(ax12,axiom,(![U]:(![V]:(relname(U,V)=>relation(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax12)).
% 0.80/0.97  fof(c254,plain,(![U]:(![V]:(~relname(U,V)|relation(U,V)))),inference(fof_nnf,[status(thm)],[ax12])).
% 0.80/0.97  fof(c255,plain,(![X129]:(![X130]:(~relname(X129,X130)|relation(X129,X130)))),inference(variable_rename,[status(thm)],[c254])).
% 0.80/0.97  cnf(c256,plain,~relname(X324,X325)|relation(X324,X325),inference(split_conjunct,[status(thm)],[c255])).
% 0.80/0.97  cnf(c346,plain,relation(skolem0001,skolem0003),inference(resolution,[status(thm)],[c256, c344])).
% 0.80/0.97  fof(ax11,axiom,(![U]:(![V]:(relation(U,V)=>abstraction(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax11)).
% 0.80/0.97  fof(c257,plain,(![U]:(![V]:(~relation(U,V)|abstraction(U,V)))),inference(fof_nnf,[status(thm)],[ax11])).
% 0.80/0.97  fof(c258,plain,(![X131]:(![X132]:(~relation(X131,X132)|abstraction(X131,X132)))),inference(variable_rename,[status(thm)],[c257])).
% 0.80/0.97  cnf(c259,plain,~relation(X327,X326)|abstraction(X327,X326),inference(split_conjunct,[status(thm)],[c258])).
% 0.80/0.97  cnf(c348,plain,abstraction(skolem0001,skolem0003),inference(resolution,[status(thm)],[c259, c346])).
% 0.80/0.97  fof(ax10,axiom,(![U]:(![V]:(abstraction(U,V)=>thing(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax10)).
% 0.80/0.97  fof(c260,plain,(![U]:(![V]:(~abstraction(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax10])).
% 0.80/0.97  fof(c261,plain,(![X133]:(![X134]:(~abstraction(X133,X134)|thing(X133,X134)))),inference(variable_rename,[status(thm)],[c260])).
% 0.80/0.97  cnf(c262,plain,~abstraction(X333,X332)|thing(X333,X332),inference(split_conjunct,[status(thm)],[c261])).
% 0.80/0.97  cnf(c351,plain,thing(skolem0001,skolem0003),inference(resolution,[status(thm)],[c262, c348])).
% 0.80/0.97  cnf(c352,plain,singleton(skolem0001,skolem0003),inference(resolution,[status(thm)],[c351, c160])).
% 0.80/0.97  cnf(c467,plain,skolem0001!=X700|skolem0003!=X701|singleton(X700,X701),inference(resolution,[status(thm)],[c44, c352])).
% 0.80/0.97  cnf(c524,plain,skolem0001!=X709|singleton(X709,skolem0003),inference(resolution,[status(thm)],[c467, reflexivity])).
% 0.80/0.97  cnf(c70,negated_conjecture,chevy(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c64])).
% 0.80/0.97  fof(ax25,axiom,(![U]:(![V]:(chevy(U,V)=>car(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax25)).
% 0.80/0.97  fof(c215,plain,(![U]:(![V]:(~chevy(U,V)|car(U,V)))),inference(fof_nnf,[status(thm)],[ax25])).
% 0.80/0.97  fof(c216,plain,(![X103]:(![X104]:(~chevy(X103,X104)|car(X103,X104)))),inference(variable_rename,[status(thm)],[c215])).
% 0.80/0.97  cnf(c217,plain,~chevy(X266,X267)|car(X266,X267),inference(split_conjunct,[status(thm)],[c216])).
% 0.80/0.97  cnf(c305,plain,car(skolem0001,skolem0004),inference(resolution,[status(thm)],[c217, c70])).
% 0.80/0.97  fof(ax24,axiom,(![U]:(![V]:(car(U,V)=>vehicle(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax24)).
% 0.80/0.97  fof(c218,plain,(![U]:(![V]:(~car(U,V)|vehicle(U,V)))),inference(fof_nnf,[status(thm)],[ax24])).
% 0.80/0.97  fof(c219,plain,(![X105]:(![X106]:(~car(X105,X106)|vehicle(X105,X106)))),inference(variable_rename,[status(thm)],[c218])).
% 0.80/0.97  cnf(c220,plain,~car(X268,X269)|vehicle(X268,X269),inference(split_conjunct,[status(thm)],[c219])).
% 0.80/0.97  cnf(c306,plain,vehicle(skolem0001,skolem0004),inference(resolution,[status(thm)],[c220, c305])).
% 0.80/0.97  fof(ax23,axiom,(![U]:(![V]:(vehicle(U,V)=>transport(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax23)).
% 0.80/0.97  fof(c221,plain,(![U]:(![V]:(~vehicle(U,V)|transport(U,V)))),inference(fof_nnf,[status(thm)],[ax23])).
% 0.80/0.97  fof(c222,plain,(![X107]:(![X108]:(~vehicle(X107,X108)|transport(X107,X108)))),inference(variable_rename,[status(thm)],[c221])).
% 0.80/0.97  cnf(c223,plain,~vehicle(X275,X274)|transport(X275,X274),inference(split_conjunct,[status(thm)],[c222])).
% 0.80/0.97  cnf(c308,plain,transport(skolem0001,skolem0004),inference(resolution,[status(thm)],[c223, c306])).
% 0.80/0.97  fof(ax22,axiom,(![U]:(![V]:(transport(U,V)=>instrumentality(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax22)).
% 0.80/0.97  fof(c224,plain,(![U]:(![V]:(~transport(U,V)|instrumentality(U,V)))),inference(fof_nnf,[status(thm)],[ax22])).
% 0.80/0.97  fof(c225,plain,(![X109]:(![X110]:(~transport(X109,X110)|instrumentality(X109,X110)))),inference(variable_rename,[status(thm)],[c224])).
% 0.80/0.97  cnf(c226,plain,~transport(X277,X276)|instrumentality(X277,X276),inference(split_conjunct,[status(thm)],[c225])).
% 0.80/0.97  cnf(c309,plain,instrumentality(skolem0001,skolem0004),inference(resolution,[status(thm)],[c226, c308])).
% 0.80/0.97  fof(ax21,axiom,(![U]:(![V]:(instrumentality(U,V)=>artifact(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax21)).
% 0.80/0.97  fof(c227,plain,(![U]:(![V]:(~instrumentality(U,V)|artifact(U,V)))),inference(fof_nnf,[status(thm)],[ax21])).
% 0.80/0.97  fof(c228,plain,(![X111]:(![X112]:(~instrumentality(X111,X112)|artifact(X111,X112)))),inference(variable_rename,[status(thm)],[c227])).
% 0.80/0.97  cnf(c229,plain,~instrumentality(X279,X278)|artifact(X279,X278),inference(split_conjunct,[status(thm)],[c228])).
% 0.80/0.97  cnf(c311,plain,artifact(skolem0001,skolem0004),inference(resolution,[status(thm)],[c229, c309])).
% 0.80/0.97  fof(ax20,axiom,(![U]:(![V]:(artifact(U,V)=>object(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax20)).
% 0.80/0.97  fof(c230,plain,(![U]:(![V]:(~artifact(U,V)|object(U,V)))),inference(fof_nnf,[status(thm)],[ax20])).
% 0.80/0.97  fof(c231,plain,(![X113]:(![X114]:(~artifact(X113,X114)|object(X113,X114)))),inference(variable_rename,[status(thm)],[c230])).
% 0.80/0.97  cnf(c232,plain,~artifact(X284,X285)|object(X284,X285),inference(split_conjunct,[status(thm)],[c231])).
% 0.80/0.97  cnf(c312,plain,object(skolem0001,skolem0004),inference(resolution,[status(thm)],[c232, c311])).
% 0.80/0.97  cnf(c314,plain,entity(skolem0001,skolem0004),inference(resolution,[status(thm)],[c235, c312])).
% 0.80/0.97  cnf(c315,plain,thing(skolem0001,skolem0004),inference(resolution,[status(thm)],[c314, c157])).
% 0.80/0.97  cnf(c318,plain,singleton(skolem0001,skolem0004),inference(resolution,[status(thm)],[c315, c160])).
% 0.80/0.97  cnf(c466,plain,skolem0001!=X697|skolem0004!=X698|singleton(X697,X698),inference(resolution,[status(thm)],[c44, c318])).
% 0.80/0.97  cnf(c522,plain,skolem0001!=X699|singleton(X699,skolem0004),inference(resolution,[status(thm)],[c466, reflexivity])).
% 0.80/0.97  cnf(c74,negated_conjecture,street(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c64])).
% 0.80/0.97  fof(ax15,axiom,(![U]:(![V]:(street(U,V)=>way(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax15)).
% 0.80/0.97  fof(c245,plain,(![U]:(![V]:(~street(U,V)|way(U,V)))),inference(fof_nnf,[status(thm)],[ax15])).
% 0.80/0.97  fof(c246,plain,(![X123]:(![X124]:(~street(X123,X124)|way(X123,X124)))),inference(variable_rename,[status(thm)],[c245])).
% 0.80/0.97  cnf(c247,plain,~street(X306,X307)|way(X306,X307),inference(split_conjunct,[status(thm)],[c246])).
% 0.80/0.97  cnf(c326,plain,way(skolem0001,skolem0005),inference(resolution,[status(thm)],[c247, c74])).
% 0.80/0.97  fof(ax14,axiom,(![U]:(![V]:(way(U,V)=>artifact(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax14)).
% 0.80/0.97  fof(c248,plain,(![U]:(![V]:(~way(U,V)|artifact(U,V)))),inference(fof_nnf,[status(thm)],[ax14])).
% 0.80/0.97  fof(c249,plain,(![X125]:(![X126]:(~way(X125,X126)|artifact(X125,X126)))),inference(variable_rename,[status(thm)],[c248])).
% 0.80/0.97  cnf(c250,plain,~way(X308,X309)|artifact(X308,X309),inference(split_conjunct,[status(thm)],[c249])).
% 0.80/0.97  cnf(c327,plain,artifact(skolem0001,skolem0005),inference(resolution,[status(thm)],[c250, c326])).
% 0.80/0.97  cnf(c328,plain,object(skolem0001,skolem0005),inference(resolution,[status(thm)],[c327, c232])).
% 0.80/0.97  cnf(c332,plain,entity(skolem0001,skolem0005),inference(resolution,[status(thm)],[c328, c235])).
% 0.80/0.97  cnf(c336,plain,thing(skolem0001,skolem0005),inference(resolution,[status(thm)],[c332, c157])).
% 0.80/0.97  cnf(c340,plain,singleton(skolem0001,skolem0005),inference(resolution,[status(thm)],[c336, c160])).
% 0.80/0.97  cnf(c465,plain,skolem0001!=X690|skolem0005!=X691|singleton(X690,X691),inference(resolution,[status(thm)],[c44, c340])).
% 0.80/0.97  cnf(c519,plain,skolem0001!=X692|singleton(X692,skolem0005),inference(resolution,[status(thm)],[c465, reflexivity])).
% 0.80/0.97  fof(ax32,axiom,(![U]:(![V]:(eventuality(U,V)=>thing(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax32)).
% 0.80/0.97  fof(c194,plain,(![U]:(![V]:(~eventuality(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax32])).
% 0.80/0.97  fof(c195,plain,(![X89]:(![X90]:(~eventuality(X89,X90)|thing(X89,X90)))),inference(variable_rename,[status(thm)],[c194])).
% 0.80/0.97  cnf(c196,plain,~eventuality(X240,X241)|thing(X240,X241),inference(split_conjunct,[status(thm)],[c195])).
% 0.80/0.97  cnf(c76,negated_conjecture,event(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c64])).
% 0.80/0.97  fof(ax27,axiom,(![U]:(![V]:(event(U,V)=>eventuality(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax27)).
% 0.80/0.97  fof(c209,plain,(![U]:(![V]:(~event(U,V)|eventuality(U,V)))),inference(fof_nnf,[status(thm)],[ax27])).
% 0.80/0.97  fof(c210,plain,(![X99]:(![X100]:(~event(X99,X100)|eventuality(X99,X100)))),inference(variable_rename,[status(thm)],[c209])).
% 0.80/0.97  cnf(c211,plain,~event(X255,X254)|eventuality(X255,X254),inference(split_conjunct,[status(thm)],[c210])).
% 0.80/0.97  cnf(c296,plain,eventuality(skolem0001,skolem0006),inference(resolution,[status(thm)],[c211, c76])).
% 0.80/0.97  cnf(c299,plain,thing(skolem0001,skolem0006),inference(resolution,[status(thm)],[c296, c196])).
% 0.80/0.97  cnf(c303,plain,singleton(skolem0001,skolem0006),inference(resolution,[status(thm)],[c299, c160])).
% 0.80/0.97  cnf(c464,plain,skolem0001!=X687|skolem0006!=X688|singleton(X687,X688),inference(resolution,[status(thm)],[c44, c303])).
% 0.80/0.97  cnf(c517,plain,skolem0001!=X689|singleton(X689,skolem0006),inference(resolution,[status(thm)],[c464, reflexivity])).
% 0.80/0.97  fof(ax42,axiom,(![U]:(![V]:(entity(U,V)=>existent(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax42)).
% 0.80/0.97  fof(c164,plain,(![U]:(![V]:(~entity(U,V)|existent(U,V)))),inference(fof_nnf,[status(thm)],[ax42])).
% 0.80/0.97  fof(c165,plain,(![X69]:(![X70]:(~entity(X69,X70)|existent(X69,X70)))),inference(variable_rename,[status(thm)],[c164])).
% 0.80/0.97  cnf(c166,plain,~entity(X212,X213)|existent(X212,X213),inference(split_conjunct,[status(thm)],[c165])).
% 0.80/0.97  cnf(c316,plain,existent(skolem0001,skolem0004),inference(resolution,[status(thm)],[c314, c166])).
% 0.80/0.97  cnf(c43,axiom,X556!=X555|X554!=X553|~existent(X556,X554)|existent(X555,X553),theory(equality)).
% 0.80/0.97  cnf(c460,plain,skolem0001!=X680|skolem0004!=X681|existent(X680,X681),inference(resolution,[status(thm)],[c43, c316])).
% 0.80/0.98  cnf(c514,plain,skolem0001!=X682|existent(X682,skolem0004),inference(resolution,[status(thm)],[c460, reflexivity])).
% 0.80/0.98  cnf(c337,plain,existent(skolem0001,skolem0005),inference(resolution,[status(thm)],[c332, c166])).
% 0.80/0.98  cnf(c459,plain,skolem0001!=X673|skolem0005!=X674|existent(X673,X674),inference(resolution,[status(thm)],[c43, c337])).
% 0.80/0.98  cnf(c511,plain,skolem0001!=X679|existent(X679,skolem0005),inference(resolution,[status(thm)],[c459, reflexivity])).
% 0.80/0.98  cnf(c383,plain,existent(skolem0001,skolem0002),inference(resolution,[status(thm)],[c374, c166])).
% 0.80/0.98  cnf(c458,plain,skolem0001!=X670|skolem0002!=X671|existent(X670,X671),inference(resolution,[status(thm)],[c43, c383])).
% 0.80/0.98  cnf(c509,plain,skolem0001!=X672|existent(X672,skolem0002),inference(resolution,[status(thm)],[c458, reflexivity])).
% 0.80/0.98  fof(ax31,axiom,(![U]:(![V]:(eventuality(U,V)=>specific(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax31)).
% 0.80/0.98  fof(c197,plain,(![U]:(![V]:(~eventuality(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax31])).
% 0.80/0.98  fof(c198,plain,(![X91]:(![X92]:(~eventuality(X91,X92)|specific(X91,X92)))),inference(variable_rename,[status(thm)],[c197])).
% 0.80/0.98  cnf(c199,plain,~eventuality(X242,X243)|specific(X242,X243),inference(split_conjunct,[status(thm)],[c198])).
% 0.80/0.98  cnf(c298,plain,specific(skolem0001,skolem0006),inference(resolution,[status(thm)],[c296, c199])).
% 0.80/0.98  cnf(c31,axiom,X448!=X447|X446!=X445|~specific(X448,X446)|specific(X447,X445),theory(equality)).
% 0.80/0.98  cnf(c417,plain,skolem0001!=X662|skolem0006!=X661|specific(X662,X661),inference(resolution,[status(thm)],[c31, c298])).
% 0.80/0.98  cnf(c506,plain,skolem0001!=X663|specific(X663,skolem0006),inference(resolution,[status(thm)],[c417, reflexivity])).
% 0.80/0.98  fof(ax43,axiom,(![U]:(![V]:(entity(U,V)=>specific(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax43)).
% 0.80/0.98  fof(c161,plain,(![U]:(![V]:(~entity(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax43])).
% 0.80/0.98  fof(c162,plain,(![X67]:(![X68]:(~entity(X67,X68)|specific(X67,X68)))),inference(variable_rename,[status(thm)],[c161])).
% 0.80/0.98  cnf(c163,plain,~entity(X211,X210)|specific(X211,X210),inference(split_conjunct,[status(thm)],[c162])).
% 0.80/0.98  cnf(c338,plain,specific(skolem0001,skolem0005),inference(resolution,[status(thm)],[c332, c163])).
% 0.80/0.98  cnf(c416,plain,skolem0001!=X659|skolem0005!=X658|specific(X659,X658),inference(resolution,[status(thm)],[c31, c338])).
% 0.80/0.98  cnf(c504,plain,skolem0001!=X660|specific(X660,skolem0005),inference(resolution,[status(thm)],[c416, reflexivity])).
% 0.80/0.98  cnf(c384,plain,specific(skolem0001,skolem0002),inference(resolution,[status(thm)],[c374, c163])).
% 0.80/0.98  cnf(c415,plain,skolem0001!=X652|skolem0002!=X651|specific(X652,X651),inference(resolution,[status(thm)],[c31, c384])).
% 0.80/0.98  cnf(c501,plain,skolem0001!=X653|specific(X653,skolem0002),inference(resolution,[status(thm)],[c415, reflexivity])).
% 0.80/0.98  cnf(c317,plain,specific(skolem0001,skolem0004),inference(resolution,[status(thm)],[c314, c163])).
% 0.80/0.98  cnf(c414,plain,skolem0001!=X643|skolem0004!=X642|specific(X643,X642),inference(resolution,[status(thm)],[c31, c317])).
% 0.80/0.98  cnf(c498,plain,skolem0001!=X650|specific(X650,skolem0004),inference(resolution,[status(thm)],[c414, reflexivity])).
% 0.80/0.98  fof(ax30,axiom,(![U]:(![V]:(eventuality(U,V)=>nonexistent(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax30)).
% 0.80/0.98  fof(c200,plain,(![U]:(![V]:(~eventuality(U,V)|nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[ax30])).
% 0.80/0.98  fof(c201,plain,(![X93]:(![X94]:(~eventuality(X93,X94)|nonexistent(X93,X94)))),inference(variable_rename,[status(thm)],[c200])).
% 0.80/0.98  cnf(c202,plain,~eventuality(X244,X245)|nonexistent(X244,X245),inference(split_conjunct,[status(thm)],[c201])).
% 0.80/0.98  cnf(c297,plain,nonexistent(skolem0001,skolem0006),inference(resolution,[status(thm)],[c296, c202])).
% 0.80/0.98  cnf(c30,axiom,X439!=X438|X437!=X436|~nonexistent(X439,X437)|nonexistent(X438,X436),theory(equality)).
% 0.80/0.98  cnf(c410,plain,skolem0001!=X639|skolem0006!=X640|nonexistent(X639,X640),inference(resolution,[status(thm)],[c30, c297])).
% 0.80/0.98  cnf(c496,plain,skolem0001!=X641|nonexistent(X641,skolem0006),inference(resolution,[status(thm)],[c410, reflexivity])).
% 0.80/0.98  cnf(c28,axiom,X421!=X420|X419!=X418|~eventuality(X421,X419)|eventuality(X420,X418),theory(equality)).
% 0.80/0.98  cnf(c402,plain,skolem0001!=X631|skolem0006!=X630|eventuality(X631,X630),inference(resolution,[status(thm)],[c28, c296])).
% 0.80/0.98  cnf(c493,plain,skolem0001!=X632|eventuality(X632,skolem0006),inference(resolution,[status(thm)],[c402, reflexivity])).
% 0.80/0.98  cnf(c27,axiom,X412!=X411|X410!=X409|~event(X412,X410)|event(X411,X409),theory(equality)).
% 0.80/0.98  cnf(c398,plain,skolem0001!=X627|skolem0006!=X628|event(X627,X628),inference(resolution,[status(thm)],[c27, c76])).
% 0.80/0.98  cnf(c491,plain,skolem0001!=X629|event(X629,skolem0006),inference(resolution,[status(thm)],[c398, reflexivity])).
% 0.80/0.98  cnf(c50,axiom,X626!=X624|X625!=X623|X622!=X621|~member(X626,X625,X622)|member(X624,X623,X621),theory(equality)).
% 0.80/0.98  cnf(c79,negated_conjecture,barrel(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c64])).
% 0.80/0.98  cnf(c26,axiom,X402!=X401|X400!=X399|~barrel(X402,X400)|barrel(X401,X399),theory(equality)).
% 0.80/0.98  cnf(c393,plain,skolem0001!=X618|skolem0006!=X619|barrel(X618,X619),inference(resolution,[status(thm)],[c26, c79])).
% 0.80/0.98  cnf(c489,plain,skolem0001!=X620|barrel(X620,skolem0006),inference(resolution,[status(thm)],[c393, reflexivity])).
% 0.80/0.98  cnf(c25,axiom,X391!=X390|X389!=X388|~chevy(X391,X389)|chevy(X390,X388),theory(equality)).
% 0.80/0.98  cnf(c390,plain,skolem0001!=X607|skolem0004!=X608|chevy(X607,X608),inference(resolution,[status(thm)],[c25, c70])).
% 0.80/0.98  cnf(c487,plain,skolem0001!=X617|chevy(X617,skolem0004),inference(resolution,[status(thm)],[c390, reflexivity])).
% 0.80/0.98  cnf(c49,axiom,X616!=X614|X615!=X611|X610!=X609|X612!=X613|~be(X616,X615,X610,X612)|be(X614,X611,X609,X613),theory(equality)).
% 0.80/0.98  cnf(c24,axiom,X376!=X375|X374!=X373|~car(X376,X374)|car(X375,X373),theory(equality)).
% 0.80/0.98  cnf(c388,plain,skolem0001!=X605|skolem0004!=X604|car(X605,X604),inference(resolution,[status(thm)],[c24, c305])).
% 0.80/0.98  cnf(c485,plain,skolem0001!=X606|car(X606,skolem0004),inference(resolution,[status(thm)],[c388, reflexivity])).
% 0.80/0.98  cnf(c23,axiom,X365!=X364|X363!=X362|~vehicle(X365,X363)|vehicle(X364,X362),theory(equality)).
% 0.80/0.98  cnf(c387,plain,skolem0001!=X595|skolem0004!=X596|vehicle(X595,X596),inference(resolution,[status(thm)],[c23, c306])).
% 0.80/0.98  cnf(c482,plain,skolem0001!=X597|vehicle(X597,skolem0004),inference(resolution,[status(thm)],[c387, reflexivity])).
% 0.80/0.98  cnf(c13,axiom,X297!=X296|X295!=X294|~thing(X297,X295)|thing(X296,X294),theory(equality)).
% 0.80/0.98  cnf(c386,plain,skolem0001!=X593|skolem0002!=X592|thing(X593,X592),inference(resolution,[status(thm)],[c381, c13])).
% 0.80/0.98  cnf(c480,plain,skolem0001!=X594|thing(X594,skolem0002),inference(resolution,[status(thm)],[c386, reflexivity])).
% 0.80/0.98  cnf(c21,axiom,X355!=X354|X353!=X352|~entity(X355,X353)|entity(X354,X352),theory(equality)).
% 0.80/0.98  cnf(c382,plain,skolem0001!=X586|skolem0002!=X585|entity(X586,X585),inference(resolution,[status(thm)],[c374, c21])).
% 0.80/0.98  cnf(c477,plain,skolem0001!=X587|entity(X587,skolem0002),inference(resolution,[status(thm)],[c382, reflexivity])).
% 0.80/0.98  cnf(c22,axiom,X361!=X360|X359!=X358|~transport(X361,X359)|transport(X360,X358),theory(equality)).
% 0.80/0.98  cnf(c380,plain,skolem0001!=X579|skolem0004!=X578|transport(X579,X578),inference(resolution,[status(thm)],[c22, c308])).
% 0.80/0.98  cnf(c475,plain,skolem0001!=X584|transport(X584,skolem0004),inference(resolution,[status(thm)],[c380, reflexivity])).
% 0.80/0.98  cnf(c46,axiom,X583!=X582|X581!=X580|~young(X583,X581)|young(X582,X580),theory(equality)).
% 0.80/0.98  cnf(c20,axiom,X347!=X346|X345!=X344|~nonliving(X347,X345)|nonliving(X346,X344),theory(equality)).
% 0.80/0.98  fof(ax18,axiom,(![U]:(![V]:(object(U,V)=>nonliving(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax18)).
% 0.80/0.98  fof(c236,plain,(![U]:(![V]:(~object(U,V)|nonliving(U,V)))),inference(fof_nnf,[status(thm)],[ax18])).
% 0.80/0.98  fof(c237,plain,(![X117]:(![X118]:(~object(X117,X118)|nonliving(X117,X118)))),inference(variable_rename,[status(thm)],[c236])).
% 0.80/0.98  cnf(c238,plain,~object(X292,X293)|nonliving(X292,X293),inference(split_conjunct,[status(thm)],[c237])).
% 0.80/0.98  cnf(c373,plain,nonliving(skolem0001,skolem0002),inference(resolution,[status(thm)],[c370, c238])).
% 0.80/0.98  cnf(c379,plain,skolem0001!=X575|skolem0002!=X576|nonliving(X575,X576),inference(resolution,[status(thm)],[c373, c20])).
% 0.80/0.98  cnf(c473,plain,skolem0001!=X577|nonliving(X577,skolem0002),inference(resolution,[status(thm)],[c379, reflexivity])).
% 0.80/0.98  cnf(c45,axiom,X574!=X573|X572!=X571|~fellow(X574,X572)|fellow(X573,X571),theory(equality)).
% 0.80/0.98  cnf(c10,axiom,X273!=X272|X271!=X270|~unisex(X273,X271)|unisex(X272,X270),theory(equality)).
% 0.80/0.98  fof(ax16,axiom,(![U]:(![V]:(object(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax16)).
% 0.80/0.98  fof(c242,plain,(![U]:(![V]:(~object(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax16])).
% 0.80/0.98  fof(c243,plain,(![X121]:(![X122]:(~object(X121,X122)|unisex(X121,X122)))),inference(variable_rename,[status(thm)],[c242])).
% 0.80/0.98  cnf(c244,plain,~object(X301,X300)|unisex(X301,X300),inference(split_conjunct,[status(thm)],[c243])).
% 0.80/0.98  cnf(c372,plain,unisex(skolem0001,skolem0002),inference(resolution,[status(thm)],[c370, c244])).
% 0.80/0.98  cnf(c377,plain,skolem0001!=X568|skolem0002!=X569|unisex(X568,X569),inference(resolution,[status(thm)],[c372, c10])).
% 0.80/0.98  cnf(c471,plain,skolem0001!=X570|unisex(X570,skolem0002),inference(resolution,[status(thm)],[c377, reflexivity])).
% 0.80/0.98  cnf(c19,axiom,X339!=X338|X337!=X336|~impartial(X339,X337)|impartial(X338,X336),theory(equality)).
% 0.80/0.98  fof(ax17,axiom,(![U]:(![V]:(object(U,V)=>impartial(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax17)).
% 0.80/0.98  fof(c239,plain,(![U]:(![V]:(~object(U,V)|impartial(U,V)))),inference(fof_nnf,[status(thm)],[ax17])).
% 0.80/0.98  fof(c240,plain,(![X119]:(![X120]:(~object(X119,X120)|impartial(X119,X120)))),inference(variable_rename,[status(thm)],[c239])).
% 0.80/0.98  cnf(c241,plain,~object(X298,X299)|impartial(X298,X299),inference(split_conjunct,[status(thm)],[c240])).
% 0.80/0.98  cnf(c371,plain,impartial(skolem0001,skolem0002),inference(resolution,[status(thm)],[c370, c241])).
% 0.80/0.98  cnf(c376,plain,skolem0001!=X565|skolem0002!=X566|impartial(X565,X566),inference(resolution,[status(thm)],[c371, c19])).
% 0.80/0.98  cnf(c469,plain,skolem0001!=X567|impartial(X567,skolem0002),inference(resolution,[status(thm)],[c376, reflexivity])).
% 0.80/0.98  cnf(c5,axiom,X223!=X222|X221!=X220|~object(X223,X221)|object(X222,X220),theory(equality)).
% 0.80/0.98  cnf(c375,plain,skolem0001!=X559|skolem0002!=X558|object(X559,X558),inference(resolution,[status(thm)],[c370, c5])).
% 0.80/0.98  cnf(c462,plain,skolem0001!=X560|object(X560,skolem0002),inference(resolution,[status(thm)],[c375, reflexivity])).
% 0.80/0.98  cnf(c369,plain,skolem0001!=X552|skolem0005!=X551|entity(X552,X551),inference(resolution,[status(thm)],[c21, c332])).
% 0.80/0.98  cnf(c457,plain,skolem0001!=X557|entity(X557,skolem0005),inference(resolution,[status(thm)],[c369, reflexivity])).
% 0.80/0.98  cnf(c368,plain,skolem0001!=X549|skolem0004!=X548|entity(X549,X548),inference(resolution,[status(thm)],[c21, c314])).
% 0.80/0.98  cnf(c455,plain,skolem0001!=X550|entity(X550,skolem0004),inference(resolution,[status(thm)],[c368, reflexivity])).
% 0.80/0.98  cnf(c42,axiom,X547!=X546|X545!=X544|~living(X547,X545)|living(X546,X544),theory(equality)).
% 0.80/0.98  cnf(c4,axiom,X209!=X208|X207!=X206|~location(X209,X207)|location(X208,X206),theory(equality)).
% 0.80/0.98  cnf(c367,plain,skolem0001!=X542|skolem0002!=X541|location(X542,X541),inference(resolution,[status(thm)],[c366, c4])).
% 0.80/0.98  cnf(c453,plain,skolem0001!=X543|location(X543,skolem0002),inference(resolution,[status(thm)],[c367, reflexivity])).
% 0.80/0.98  fof(ax7,axiom,(![U]:(![V]:(abstraction(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax7)).
% 0.80/0.98  fof(c269,plain,(![U]:(![V]:(~abstraction(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax7])).
% 0.80/0.98  fof(c270,plain,(![X139]:(![X140]:(~abstraction(X139,X140)|unisex(X139,X140)))),inference(variable_rename,[status(thm)],[c269])).
% 0.80/0.98  cnf(c271,plain,~abstraction(X343,X342)|unisex(X343,X342),inference(split_conjunct,[status(thm)],[c270])).
% 0.80/0.98  cnf(c361,plain,unisex(skolem0001,skolem0003),inference(resolution,[status(thm)],[c271, c348])).
% 0.80/0.98  cnf(c364,plain,skolem0001!=X538|skolem0003!=X539|unisex(X538,X539),inference(resolution,[status(thm)],[c361, c10])).
% 0.80/0.98  cnf(c451,plain,skolem0001!=X540|unisex(X540,skolem0003),inference(resolution,[status(thm)],[c364, reflexivity])).
% 0.80/0.98  cnf(c41,axiom,X537!=X536|X535!=X534|~organism(X537,X535)|organism(X536,X534),theory(equality)).
% 0.80/0.98  cnf(c319,plain,nonliving(skolem0001,skolem0004),inference(resolution,[status(thm)],[c238, c312])).
% 0.80/0.98  cnf(c363,plain,skolem0001!=X531|skolem0004!=X532|nonliving(X531,X532),inference(resolution,[status(thm)],[c20, c319])).
% 0.80/0.98  cnf(c449,plain,skolem0001!=X533|nonliving(X533,skolem0004),inference(resolution,[status(thm)],[c363, reflexivity])).
% 0.80/0.98  cnf(c331,plain,nonliving(skolem0001,skolem0005),inference(resolution,[status(thm)],[c328, c238])).
% 0.80/0.98  cnf(c362,plain,skolem0001!=X524|skolem0005!=X525|nonliving(X524,X525),inference(resolution,[status(thm)],[c20, c331])).
% 0.80/0.98  cnf(c447,plain,skolem0001!=X530|nonliving(X530,skolem0005),inference(resolution,[status(thm)],[c362, reflexivity])).
% 0.80/0.98  cnf(c40,axiom,X529!=X528|X527!=X526|~human(X529,X527)|human(X528,X526),theory(equality)).
% 0.80/0.98  cnf(c11,axiom,X283!=X282|X281!=X280|~general(X283,X281)|general(X282,X280),theory(equality)).
% 0.80/0.98  fof(ax8,axiom,(![U]:(![V]:(abstraction(U,V)=>general(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax8)).
% 0.80/0.98  fof(c266,plain,(![U]:(![V]:(~abstraction(U,V)|general(U,V)))),inference(fof_nnf,[status(thm)],[ax8])).
% 0.80/0.98  fof(c267,plain,(![X137]:(![X138]:(~abstraction(X137,X138)|general(X137,X138)))),inference(variable_rename,[status(thm)],[c266])).
% 0.80/0.98  cnf(c268,plain,~abstraction(X340,X341)|general(X340,X341),inference(split_conjunct,[status(thm)],[c267])).
% 0.80/0.98  cnf(c358,plain,general(skolem0001,skolem0003),inference(resolution,[status(thm)],[c268, c348])).
% 0.80/0.98  cnf(c360,plain,skolem0001!=X521|skolem0003!=X522|general(X521,X522),inference(resolution,[status(thm)],[c358, c11])).
% 0.80/0.98  cnf(c445,plain,skolem0001!=X523|general(X523,skolem0003),inference(resolution,[status(thm)],[c360, reflexivity])).
% 0.80/0.98  cnf(c39,axiom,X520!=X519|X518!=X517|~animate(X520,X518)|animate(X519,X517),theory(equality)).
% 0.80/0.98  cnf(c12,axiom,X291!=X290|X289!=X288|~nonhuman(X291,X289)|nonhuman(X290,X288),theory(equality)).
% 0.80/0.98  fof(ax9,axiom,(![U]:(![V]:(abstraction(U,V)=>nonhuman(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax9)).
% 0.80/0.98  fof(c263,plain,(![U]:(![V]:(~abstraction(U,V)|nonhuman(U,V)))),inference(fof_nnf,[status(thm)],[ax9])).
% 0.80/0.98  fof(c264,plain,(![X135]:(![X136]:(~abstraction(X135,X136)|nonhuman(X135,X136)))),inference(variable_rename,[status(thm)],[c263])).
% 0.80/0.98  cnf(c265,plain,~abstraction(X334,X335)|nonhuman(X334,X335),inference(split_conjunct,[status(thm)],[c264])).
% 0.80/0.98  cnf(c354,plain,nonhuman(skolem0001,skolem0003),inference(resolution,[status(thm)],[c265, c348])).
% 0.80/0.98  cnf(c357,plain,skolem0001!=X514|skolem0003!=X515|nonhuman(X514,X515),inference(resolution,[status(thm)],[c354, c12])).
% 0.80/0.98  cnf(c443,plain,skolem0001!=X516|nonhuman(X516,skolem0003),inference(resolution,[status(thm)],[c357, reflexivity])).
% 0.80/0.98  cnf(c329,plain,impartial(skolem0001,skolem0005),inference(resolution,[status(thm)],[c328, c241])).
% 0.80/0.98  cnf(c356,plain,skolem0001!=X511|skolem0005!=X512|impartial(X511,X512),inference(resolution,[status(thm)],[c19, c329])).
% 0.80/0.98  cnf(c441,plain,skolem0001!=X513|impartial(X513,skolem0005),inference(resolution,[status(thm)],[c356, reflexivity])).
% 0.80/0.98  cnf(c38,axiom,X510!=X509|X508!=X507|~human_person(X510,X508)|human_person(X509,X507),theory(equality)).
% 0.80/0.98  cnf(c323,plain,impartial(skolem0001,skolem0004),inference(resolution,[status(thm)],[c241, c312])).
% 0.80/0.98  cnf(c355,plain,skolem0001!=X504|skolem0004!=X505|impartial(X504,X505),inference(resolution,[status(thm)],[c19, c323])).
% 0.80/0.98  cnf(c439,plain,skolem0001!=X506|impartial(X506,skolem0004),inference(resolution,[status(thm)],[c355, reflexivity])).
% 0.80/0.98  cnf(c353,plain,skolem0001!=X498|skolem0003!=X497|thing(X498,X497),inference(resolution,[status(thm)],[c351, c13])).
% 0.80/0.98  cnf(c437,plain,skolem0001!=X503|thing(X503,skolem0003),inference(resolution,[status(thm)],[c353, reflexivity])).
% 0.80/0.98  cnf(c37,axiom,X502!=X501|X500!=X499|~male(X502,X500)|male(X501,X499),theory(equality)).
% 0.80/0.98  cnf(c9,axiom,X265!=X264|X263!=X262|~abstraction(X265,X263)|abstraction(X264,X262),theory(equality)).
% 0.80/0.98  cnf(c350,plain,skolem0001!=X494|skolem0003!=X495|abstraction(X494,X495),inference(resolution,[status(thm)],[c348, c9])).
% 0.80/0.98  cnf(c435,plain,skolem0001!=X496|abstraction(X496,skolem0003),inference(resolution,[status(thm)],[c350, reflexivity])).
% 0.80/0.98  cnf(c36,axiom,X493!=X492|X491!=X490|~man(X493,X491)|man(X492,X490),theory(equality)).
% 0.80/0.98  cnf(c18,axiom,X331!=X330|X329!=X328|~street(X331,X329)|street(X330,X328),theory(equality)).
% 0.80/0.98  cnf(c349,plain,skolem0001!=X487|skolem0005!=X488|street(X487,X488),inference(resolution,[status(thm)],[c18, c74])).
% 0.80/0.98  cnf(c433,plain,skolem0001!=X489|street(X489,skolem0005),inference(resolution,[status(thm)],[c349, reflexivity])).
% 0.80/0.98  cnf(c14,axiom,X305!=X304|X303!=X302|~relation(X305,X303)|relation(X304,X302),theory(equality)).
% 0.80/0.98  cnf(c347,plain,skolem0001!=X484|skolem0003!=X485|relation(X484,X485),inference(resolution,[status(thm)],[c346, c14])).
% 0.80/0.98  cnf(c431,plain,skolem0001!=X486|relation(X486,skolem0003),inference(resolution,[status(thm)],[c347, reflexivity])).
% 0.80/0.98  cnf(c35,axiom,X483!=X482|X481!=X480|~multiple(X483,X481)|multiple(X482,X480),theory(equality)).
% 0.80/0.98  cnf(c15,axiom,X313!=X312|X311!=X310|~relname(X313,X311)|relname(X312,X310),theory(equality)).
% 0.80/0.98  cnf(c345,plain,skolem0001!=X478|skolem0003!=X477|relname(X478,X477),inference(resolution,[status(thm)],[c344, c15])).
% 0.80/0.98  cnf(c429,plain,skolem0001!=X479|relname(X479,skolem0003),inference(resolution,[status(thm)],[c345, reflexivity])).
% 0.80/0.98  cnf(c17,axiom,X321!=X320|X319!=X318|~artifact(X321,X319)|artifact(X320,X318),theory(equality)).
% 0.80/0.98  cnf(c343,plain,skolem0001!=X471|skolem0004!=X470|artifact(X471,X470),inference(resolution,[status(thm)],[c17, c311])).
% 0.80/0.98  cnf(c427,plain,skolem0001!=X476|artifact(X476,skolem0004),inference(resolution,[status(thm)],[c343, reflexivity])).
% 0.80/0.98  cnf(c34,axiom,X475!=X474|X473!=X472|~set(X475,X473)|set(X474,X472),theory(equality)).
% 0.80/0.98  cnf(c342,plain,skolem0001!=X468|skolem0005!=X467|artifact(X468,X467),inference(resolution,[status(thm)],[c17, c327])).
% 0.80/0.98  cnf(c425,plain,skolem0001!=X469|artifact(X469,skolem0005),inference(resolution,[status(thm)],[c342, reflexivity])).
% 0.80/0.98  cnf(c33,axiom,X466!=X465|X464!=X463|~group(X466,X464)|group(X465,X463),theory(equality)).
% 0.80/0.98  cnf(c341,plain,skolem0001!=X461|skolem0005!=X460|thing(X461,X460),inference(resolution,[status(thm)],[c336, c13])).
% 0.80/0.98  cnf(c423,plain,skolem0001!=X462|thing(X462,skolem0005),inference(resolution,[status(thm)],[c341, reflexivity])).
% 0.80/0.98  cnf(c16,axiom,X317!=X316|X315!=X314|~way(X317,X315)|way(X316,X314),theory(equality)).
% 0.80/0.98  cnf(c339,plain,skolem0001!=X458|skolem0005!=X457|way(X458,X457),inference(resolution,[status(thm)],[c16, c326])).
% 0.80/0.98  cnf(c421,plain,skolem0001!=X459|way(X459,skolem0005),inference(resolution,[status(thm)],[c339, reflexivity])).
% 0.80/0.98  cnf(c32,axiom,X456!=X455|X454!=X453|~two(X456,X454)|two(X455,X453),theory(equality)).
% 0.80/0.98  cnf(c330,plain,unisex(skolem0001,skolem0005),inference(resolution,[status(thm)],[c328, c244])).
% 0.80/0.98  cnf(c334,plain,skolem0001!=X450|skolem0005!=X451|unisex(X450,X451),inference(resolution,[status(thm)],[c330, c10])).
% 0.80/0.98  cnf(c419,plain,skolem0001!=X452|unisex(X452,skolem0005),inference(resolution,[status(thm)],[c334, reflexivity])).
% 0.80/0.98  cnf(c333,plain,skolem0001!=X444|skolem0005!=X443|object(X444,X443),inference(resolution,[status(thm)],[c328, c5])).
% 0.80/0.98  cnf(c413,plain,skolem0001!=X449|object(X449,skolem0005),inference(resolution,[status(thm)],[c333, reflexivity])).
% 0.80/0.98  cnf(c324,plain,unisex(skolem0001,skolem0004),inference(resolution,[status(thm)],[c244, c312])).
% 0.80/0.98  cnf(c325,plain,skolem0001!=X440|skolem0004!=X441|unisex(X440,X441),inference(resolution,[status(thm)],[c324, c10])).
% 0.80/0.98  cnf(c411,plain,skolem0001!=X442|unisex(X442,skolem0004),inference(resolution,[status(thm)],[c325, reflexivity])).
% 0.80/0.98  cnf(c321,plain,skolem0001!=X434|skolem0006!=X433|thing(X434,X433),inference(resolution,[status(thm)],[c13, c299])).
% 0.80/0.98  cnf(c408,plain,skolem0001!=X435|thing(X435,skolem0006),inference(resolution,[status(thm)],[c321, reflexivity])).
% 0.80/0.98  cnf(c320,plain,skolem0001!=X431|skolem0004!=X430|thing(X431,X430),inference(resolution,[status(thm)],[c13, c315])).
% 0.80/0.98  cnf(c406,plain,skolem0001!=X432|thing(X432,skolem0004),inference(resolution,[status(thm)],[c320, reflexivity])).
% 0.80/0.98  cnf(c29,axiom,X429!=X428|X427!=X426|~state(X429,X427)|state(X428,X426),theory(equality)).
% 0.80/0.98  cnf(c313,plain,skolem0001!=X424|skolem0004!=X423|object(X424,X423),inference(resolution,[status(thm)],[c312, c5])).
% 0.80/0.98  cnf(c404,plain,skolem0001!=X425|object(X425,skolem0004),inference(resolution,[status(thm)],[c313, reflexivity])).
% 0.80/0.98  cnf(c1,axiom,X169!=X168|X167!=X166|~instrumentality(X169,X167)|instrumentality(X168,X166),theory(equality)).
% 0.80/0.98  cnf(c310,plain,skolem0001!=X417|skolem0004!=X416|instrumentality(X417,X416),inference(resolution,[status(thm)],[c309, c1])).
% 0.80/0.98  cnf(c401,plain,skolem0001!=X422|instrumentality(X422,skolem0004),inference(resolution,[status(thm)],[c310, reflexivity])).
% 0.80/0.98  fof(ax29,axiom,(![U]:(![V]:(eventuality(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax29)).
% 0.80/0.98  fof(c203,plain,(![U]:(![V]:(~eventuality(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax29])).
% 0.80/0.98  fof(c204,plain,(![X95]:(![X96]:(~eventuality(X95,X96)|unisex(X95,X96)))),inference(variable_rename,[status(thm)],[c203])).
% 0.80/0.98  cnf(c205,plain,~eventuality(X246,X247)|unisex(X246,X247),inference(split_conjunct,[status(thm)],[c204])).
% 0.80/0.98  cnf(c300,plain,unisex(skolem0001,skolem0006),inference(resolution,[status(thm)],[c296, c205])).
% 0.80/0.98  cnf(c307,plain,skolem0001!=X413|skolem0006!=X414|unisex(X413,X414),inference(resolution,[status(thm)],[c10, c300])).
% 0.80/0.98  cnf(c399,plain,skolem0001!=X415|unisex(X415,skolem0006),inference(resolution,[status(thm)],[c307, reflexivity])).
% 0.80/0.98  cnf(c8,axiom,X259!=X258|X257!=X256|~placename(X259,X257)|placename(X258,X256),theory(equality)).
% 0.80/0.98  cnf(c302,plain,skolem0001!=X406|skolem0003!=X407|placename(X406,X407),inference(resolution,[status(thm)],[c8, c69])).
% 0.80/0.98  cnf(c396,plain,skolem0001!=X408|placename(X408,skolem0003),inference(resolution,[status(thm)],[c302, reflexivity])).
% 0.80/0.98  cnf(c68,negated_conjecture,hollywood_placename(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c64])).
% 0.80/0.98  cnf(c7,axiom,X251!=X250|X249!=X248|~hollywood_placename(X251,X249)|hollywood_placename(X250,X248),theory(equality)).
% 0.80/0.98  cnf(c295,plain,skolem0001!=X404|skolem0003!=X403|hollywood_placename(X404,X403),inference(resolution,[status(thm)],[c7, c68])).
% 0.80/0.98  cnf(c394,plain,skolem0001!=X405|hollywood_placename(X405,skolem0003),inference(resolution,[status(thm)],[c295, reflexivity])).
% 0.80/0.98  cnf(c6,axiom,X237!=X236|X235!=X234|~city(X237,X235)|city(X236,X234),theory(equality)).
% 0.80/0.98  cnf(c294,plain,skolem0001!=X396|skolem0002!=X397|city(X396,X397),inference(resolution,[status(thm)],[c6, c67])).
% 0.80/0.98  cnf(c391,plain,skolem0001!=X398|city(X398,skolem0002),inference(resolution,[status(thm)],[c294, reflexivity])).
% 0.80/0.98  cnf(c99,plain,~two(X395,X394)|skolem0010(X395,X394)!=skolem0009(X395,X394),inference(split_conjunct,[status(thm)],[c96])).
% 0.80/0.98  cnf(c98,plain,~two(X393,X392)|member(X393,skolem0010(X393,X392),X392),inference(split_conjunct,[status(thm)],[c96])).
% 0.80/0.98  cnf(c97,plain,~two(X387,X386)|member(X387,skolem0009(X387,X386),X386),inference(split_conjunct,[status(thm)],[c96])).
% 0.80/0.98  fof(ax59,axiom,(![U]:(![V]:(![W]:(![X]:(be(U,V,W,X)=>W=X))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax59)).
% 0.80/0.98  fof(c104,plain,(![U]:(![V]:(![W]:(![X]:(~be(U,V,W,X)|W=X))))),inference(fof_nnf,[status(thm)],[ax59])).
% 0.80/0.98  fof(c105,plain,(![X31]:(![X32]:(![X33]:(![X34]:(~be(X31,X32,X33,X34)|X33=X34))))),inference(variable_rename,[status(thm)],[c104])).
% 0.80/0.98  cnf(c106,plain,~be(X384,X382,X385,X383)|X385=X383,inference(split_conjunct,[status(thm)],[c105])).
% 0.80/0.98  cnf(c51,axiom,X380!=X379|~actual_world(X380)|actual_world(X379),theory(equality)).
% 0.80/0.98  fof(ax1,axiom,(![U]:(![V]:(furniture(U,V)=>instrumentality(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax1)).
% 0.80/0.98  fof(c287,plain,(![U]:(![V]:(~furniture(U,V)|instrumentality(U,V)))),inference(fof_nnf,[status(thm)],[ax1])).
% 0.80/0.98  fof(c288,plain,(![X151]:(![X152]:(~furniture(X151,X152)|instrumentality(X151,X152)))),inference(variable_rename,[status(thm)],[c287])).
% 0.80/0.98  cnf(c289,plain,~furniture(X370,X371)|instrumentality(X370,X371),inference(split_conjunct,[status(thm)],[c288])).
% 0.80/0.98  fof(ax2,axiom,(![U]:(![V]:(seat(U,V)=>furniture(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax2)).
% 0.80/0.98  fof(c284,plain,(![U]:(![V]:(~seat(U,V)|furniture(U,V)))),inference(fof_nnf,[status(thm)],[ax2])).
% 0.80/0.98  fof(c285,plain,(![X149]:(![X150]:(~seat(X149,X150)|furniture(X149,X150)))),inference(variable_rename,[status(thm)],[c284])).
% 0.80/0.98  cnf(c286,plain,~seat(X368,X369)|furniture(X368,X369),inference(split_conjunct,[status(thm)],[c285])).
% 0.80/0.98  fof(ax3,axiom,(![U]:(![V]:(frontseat(U,V)=>seat(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax3)).
% 0.80/0.98  fof(c281,plain,(![U]:(![V]:(~frontseat(U,V)|seat(U,V)))),inference(fof_nnf,[status(thm)],[ax3])).
% 0.80/0.98  fof(c282,plain,(![X147]:(![X148]:(~frontseat(X147,X148)|seat(X147,X148)))),inference(variable_rename,[status(thm)],[c281])).
% 0.80/0.98  cnf(c283,plain,~frontseat(X367,X366)|seat(X367,X366),inference(split_conjunct,[status(thm)],[c282])).
% 0.80/0.98  fof(ax50,axiom,(![U]:(![V]:(animate(U,V)=>(~nonliving(U,V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax50)).
% 0.80/0.98  fof(c139,plain,(![U]:(![V]:(animate(U,V)=>~nonliving(U,V)))),inference(fof_simplification,[status(thm)],[ax50])).
% 0.80/0.98  fof(c140,plain,(![U]:(![V]:(~animate(U,V)|~nonliving(U,V)))),inference(fof_nnf,[status(thm)],[c139])).
% 0.80/0.98  fof(c141,plain,(![X53]:(![X54]:(~animate(X53,X54)|~nonliving(X53,X54)))),inference(variable_rename,[status(thm)],[c140])).
% 0.80/0.98  cnf(c142,plain,~animate(X189,X188)|~nonliving(X189,X188),inference(split_conjunct,[status(thm)],[c141])).
% 0.80/0.98  cnf(c378,plain,~animate(skolem0001,skolem0002),inference(resolution,[status(thm)],[c373, c142])).
% 0.80/0.98  fof(ax6,axiom,(![U]:(![V]:(hollywood_placename(U,V)=>placename(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax6)).
% 0.80/0.98  fof(c272,plain,(![U]:(![V]:(~hollywood_placename(U,V)|placename(U,V)))),inference(fof_nnf,[status(thm)],[ax6])).
% 0.80/0.98  fof(c273,plain,(![X141]:(![X142]:(~hollywood_placename(X141,X142)|placename(X141,X142)))),inference(variable_rename,[status(thm)],[c272])).
% 0.80/0.98  cnf(c274,plain,~hollywood_placename(X349,X348)|placename(X349,X348),inference(split_conjunct,[status(thm)],[c273])).
% 0.80/0.98  fof(ax55,axiom,(![U]:(![V]:(specific(U,V)=>(~general(U,V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax55)).
% 0.80/0.98  fof(c119,plain,(![U]:(![V]:(specific(U,V)=>~general(U,V)))),inference(fof_simplification,[status(thm)],[ax55])).
% 0.80/0.98  fof(c120,plain,(![U]:(![V]:(~specific(U,V)|~general(U,V)))),inference(fof_nnf,[status(thm)],[c119])).
% 0.80/0.98  fof(c121,plain,(![X43]:(![X44]:(~specific(X43,X44)|~general(X43,X44)))),inference(variable_rename,[status(thm)],[c120])).
% 0.80/0.98  cnf(c122,plain,~specific(X175,X174)|~general(X175,X174),inference(split_conjunct,[status(thm)],[c121])).
% 0.80/0.98  cnf(c359,plain,~specific(skolem0001,skolem0003),inference(resolution,[status(thm)],[c358, c122])).
% 0.80/0.98  cnf(c335,plain,~animate(skolem0001,skolem0005),inference(resolution,[status(thm)],[c331, c142])).
% 0.80/0.98  cnf(c322,plain,~animate(skolem0001,skolem0004),inference(resolution,[status(thm)],[c319, c142])).
% 0.80/0.98  fof(ax26,axiom,(![U]:(![V]:(barrel(U,V)=>event(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax26)).
% 0.80/0.98  fof(c212,plain,(![U]:(![V]:(~barrel(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax26])).
% 0.80/0.98  fof(c213,plain,(![X101]:(![X102]:(~barrel(X101,X102)|event(X101,X102)))),inference(variable_rename,[status(thm)],[c212])).
% 0.80/0.98  cnf(c214,plain,~barrel(X261,X260)|event(X261,X260),inference(split_conjunct,[status(thm)],[c213])).
% 0.80/0.98  fof(ax51,axiom,(![U]:(![V]:(existent(U,V)=>(~nonexistent(U,V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax51)).
% 0.80/0.98  fof(c135,plain,(![U]:(![V]:(existent(U,V)=>~nonexistent(U,V)))),inference(fof_simplification,[status(thm)],[ax51])).
% 0.80/0.98  fof(c136,plain,(![U]:(![V]:(~existent(U,V)|~nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[c135])).
% 0.80/0.98  fof(c137,plain,(![X51]:(![X52]:(~existent(X51,X52)|~nonexistent(X51,X52)))),inference(variable_rename,[status(thm)],[c136])).
% 0.80/0.98  cnf(c138,plain,~existent(X186,X187)|~nonexistent(X186,X187),inference(split_conjunct,[status(thm)],[c137])).
% 0.80/0.98  cnf(c301,plain,~existent(skolem0001,skolem0006),inference(resolution,[status(thm)],[c297, c138])).
% 0.80/0.98  fof(ax28,axiom,(![U]:(![V]:(state(U,V)=>event(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax28)).
% 0.80/0.98  fof(c206,plain,(![U]:(![V]:(~state(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax28])).
% 0.80/0.98  fof(c207,plain,(![X97]:(![X98]:(~state(X97,X98)|event(X97,X98)))),inference(variable_rename,[status(thm)],[c206])).
% 0.80/0.98  cnf(c208,plain,~state(X252,X253)|event(X252,X253),inference(split_conjunct,[status(thm)],[c207])).
% 0.80/0.98  fof(ax33,axiom,(![U]:(![V]:(state(U,V)=>eventuality(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax33)).
% 0.80/0.98  fof(c191,plain,(![U]:(![V]:(~state(U,V)|eventuality(U,V)))),inference(fof_nnf,[status(thm)],[ax33])).
% 0.80/0.98  fof(c192,plain,(![X87]:(![X88]:(~state(X87,X88)|eventuality(X87,X88)))),inference(variable_rename,[status(thm)],[c191])).
% 0.80/0.98  cnf(c193,plain,~state(X238,X239)|eventuality(X238,X239),inference(split_conjunct,[status(thm)],[c192])).
% 0.80/0.98  fof(ax34,axiom,(![U]:(![V]:(two(U,V)=>group(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax34)).
% 0.80/0.98  fof(c188,plain,(![U]:(![V]:(~two(U,V)|group(U,V)))),inference(fof_nnf,[status(thm)],[ax34])).
% 0.80/0.98  fof(c189,plain,(![X85]:(![X86]:(~two(X85,X86)|group(X85,X86)))),inference(variable_rename,[status(thm)],[c188])).
% 0.80/0.98  cnf(c190,plain,~two(X233,X232)|group(X233,X232),inference(split_conjunct,[status(thm)],[c189])).
% 0.80/0.98  fof(ax35,axiom,(![U]:(![V]:(set(U,V)=>multiple(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax35)).
% 0.80/0.98  fof(c185,plain,(![U]:(![V]:(~set(U,V)|multiple(U,V)))),inference(fof_nnf,[status(thm)],[ax35])).
% 0.80/0.98  fof(c186,plain,(![X83]:(![X84]:(~set(X83,X84)|multiple(X83,X84)))),inference(variable_rename,[status(thm)],[c185])).
% 0.80/0.98  cnf(c187,plain,~set(X231,X230)|multiple(X231,X230),inference(split_conjunct,[status(thm)],[c186])).
% 0.80/0.98  fof(ax36,axiom,(![U]:(![V]:(group(U,V)=>set(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax36)).
% 0.80/0.98  fof(c182,plain,(![U]:(![V]:(~group(U,V)|set(U,V)))),inference(fof_nnf,[status(thm)],[ax36])).
% 0.80/0.98  fof(c183,plain,(![X81]:(![X82]:(~group(X81,X82)|set(X81,X82)))),inference(variable_rename,[status(thm)],[c182])).
% 0.80/0.98  cnf(c184,plain,~group(X229,X228)|set(X229,X228),inference(split_conjunct,[status(thm)],[c183])).
% 0.80/0.98  fof(ax37,axiom,(![U]:(![V]:(man(U,V)=>male(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax37)).
% 0.80/0.98  fof(c179,plain,(![U]:(![V]:(~man(U,V)|male(U,V)))),inference(fof_nnf,[status(thm)],[ax37])).
% 0.80/0.98  fof(c180,plain,(![X79]:(![X80]:(~man(X79,X80)|male(X79,X80)))),inference(variable_rename,[status(thm)],[c179])).
% 0.80/0.98  cnf(c181,plain,~man(X226,X227)|male(X226,X227),inference(split_conjunct,[status(thm)],[c180])).
% 0.80/0.98  fof(ax38,axiom,(![U]:(![V]:(human_person(U,V)=>animate(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax38)).
% 0.80/0.98  fof(c176,plain,(![U]:(![V]:(~human_person(U,V)|animate(U,V)))),inference(fof_nnf,[status(thm)],[ax38])).
% 0.80/0.98  fof(c177,plain,(![X77]:(![X78]:(~human_person(X77,X78)|animate(X77,X78)))),inference(variable_rename,[status(thm)],[c176])).
% 0.80/0.98  cnf(c178,plain,~human_person(X224,X225)|animate(X224,X225),inference(split_conjunct,[status(thm)],[c177])).
% 0.80/0.98  fof(ax39,axiom,(![U]:(![V]:(human_person(U,V)=>human(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax39)).
% 0.80/0.98  fof(c173,plain,(![U]:(![V]:(~human_person(U,V)|human(U,V)))),inference(fof_nnf,[status(thm)],[ax39])).
% 0.80/0.98  fof(c174,plain,(![X75]:(![X76]:(~human_person(X75,X76)|human(X75,X76)))),inference(variable_rename,[status(thm)],[c173])).
% 0.80/0.98  cnf(c175,plain,~human_person(X218,X219)|human(X218,X219),inference(split_conjunct,[status(thm)],[c174])).
% 0.80/0.98  fof(ax40,axiom,(![U]:(![V]:(organism(U,V)=>living(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax40)).
% 0.80/0.98  fof(c170,plain,(![U]:(![V]:(~organism(U,V)|living(U,V)))),inference(fof_nnf,[status(thm)],[ax40])).
% 0.80/0.98  fof(c171,plain,(![X73]:(![X74]:(~organism(X73,X74)|living(X73,X74)))),inference(variable_rename,[status(thm)],[c170])).
% 0.80/0.98  cnf(c172,plain,~organism(X216,X217)|living(X216,X217),inference(split_conjunct,[status(thm)],[c171])).
% 0.80/0.98  fof(ax41,axiom,(![U]:(![V]:(organism(U,V)=>impartial(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax41)).
% 0.80/0.98  fof(c167,plain,(![U]:(![V]:(~organism(U,V)|impartial(U,V)))),inference(fof_nnf,[status(thm)],[ax41])).
% 0.80/0.98  fof(c168,plain,(![X71]:(![X72]:(~organism(X71,X72)|impartial(X71,X72)))),inference(variable_rename,[status(thm)],[c167])).
% 0.80/0.98  cnf(c169,plain,~organism(X214,X215)|impartial(X214,X215),inference(split_conjunct,[status(thm)],[c168])).
% 0.80/0.98  fof(ax46,axiom,(![U]:(![V]:(organism(U,V)=>entity(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax46)).
% 0.80/0.98  fof(c152,plain,(![U]:(![V]:(~organism(U,V)|entity(U,V)))),inference(fof_nnf,[status(thm)],[ax46])).
% 0.80/0.98  fof(c153,plain,(![X61]:(![X62]:(~organism(X61,X62)|entity(X61,X62)))),inference(variable_rename,[status(thm)],[c152])).
% 0.80/0.98  cnf(c154,plain,~organism(X200,X201)|entity(X200,X201),inference(split_conjunct,[status(thm)],[c153])).
% 0.80/0.98  fof(ax47,axiom,(![U]:(![V]:(human_person(U,V)=>organism(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax47)).
% 0.80/0.98  fof(c149,plain,(![U]:(![V]:(~human_person(U,V)|organism(U,V)))),inference(fof_nnf,[status(thm)],[ax47])).
% 0.80/0.98  fof(c150,plain,(![X59]:(![X60]:(~human_person(X59,X60)|organism(X59,X60)))),inference(variable_rename,[status(thm)],[c149])).
% 0.80/0.98  cnf(c151,plain,~human_person(X198,X199)|organism(X198,X199),inference(split_conjunct,[status(thm)],[c150])).
% 0.80/0.98  fof(ax48,axiom,(![U]:(![V]:(man(U,V)=>human_person(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax48)).
% 0.80/0.98  fof(c146,plain,(![U]:(![V]:(~man(U,V)|human_person(U,V)))),inference(fof_nnf,[status(thm)],[ax48])).
% 0.80/0.98  fof(c147,plain,(![X57]:(![X58]:(~man(X57,X58)|human_person(X57,X58)))),inference(variable_rename,[status(thm)],[c146])).
% 0.80/0.98  cnf(c148,plain,~man(X196,X197)|human_person(X196,X197),inference(split_conjunct,[status(thm)],[c147])).
% 0.80/0.98  cnf(c3,axiom,X195!=X194|X193!=X192|~frontseat(X195,X193)|frontseat(X194,X192),theory(equality)).
% 0.80/0.98  fof(ax49,axiom,(![U]:(![V]:(fellow(U,V)=>man(U,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax49)).
% 0.80/0.98  fof(c143,plain,(![U]:(![V]:(~fellow(U,V)|man(U,V)))),inference(fof_nnf,[status(thm)],[ax49])).
% 0.80/0.98  fof(c144,plain,(![X55]:(![X56]:(~fellow(X55,X56)|man(X55,X56)))),inference(variable_rename,[status(thm)],[c143])).
% 0.80/0.98  cnf(c145,plain,~fellow(X191,X190)|man(X191,X190),inference(split_conjunct,[status(thm)],[c144])).
% 0.80/0.98  fof(ax52,axiom,(![U]:(![V]:(nonhuman(U,V)=>(~human(U,V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax52)).
% 0.80/0.98  fof(c131,plain,(![U]:(![V]:(nonhuman(U,V)=>~human(U,V)))),inference(fof_simplification,[status(thm)],[ax52])).
% 0.80/0.98  fof(c132,plain,(![U]:(![V]:(~nonhuman(U,V)|~human(U,V)))),inference(fof_nnf,[status(thm)],[c131])).
% 0.80/0.98  fof(c133,plain,(![X49]:(![X50]:(~nonhuman(X49,X50)|~human(X49,X50)))),inference(variable_rename,[status(thm)],[c132])).
% 0.80/0.98  cnf(c134,plain,~nonhuman(X185,X184)|~human(X185,X184),inference(split_conjunct,[status(thm)],[c133])).
% 0.80/0.98  fof(ax53,axiom,(![U]:(![V]:(nonliving(U,V)=>(~living(U,V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax53)).
% 0.80/0.98  fof(c127,plain,(![U]:(![V]:(nonliving(U,V)=>~living(U,V)))),inference(fof_simplification,[status(thm)],[ax53])).
% 0.80/0.98  fof(c128,plain,(![U]:(![V]:(~nonliving(U,V)|~living(U,V)))),inference(fof_nnf,[status(thm)],[c127])).
% 0.80/0.98  fof(c129,plain,(![X47]:(![X48]:(~nonliving(X47,X48)|~living(X47,X48)))),inference(variable_rename,[status(thm)],[c128])).
% 0.80/0.98  cnf(c130,plain,~nonliving(X183,X182)|~living(X183,X182),inference(split_conjunct,[status(thm)],[c129])).
% 0.80/0.98  cnf(c2,axiom,X181!=X180|X179!=X178|~seat(X181,X179)|seat(X180,X178),theory(equality)).
% 0.80/0.98  fof(ax54,axiom,(![U]:(![V]:(singleton(U,V)=>(~multiple(U,V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax54)).
% 0.80/0.98  fof(c123,plain,(![U]:(![V]:(singleton(U,V)=>~multiple(U,V)))),inference(fof_simplification,[status(thm)],[ax54])).
% 0.80/0.98  fof(c124,plain,(![U]:(![V]:(~singleton(U,V)|~multiple(U,V)))),inference(fof_nnf,[status(thm)],[c123])).
% 0.80/0.98  fof(c125,plain,(![X45]:(![X46]:(~singleton(X45,X46)|~multiple(X45,X46)))),inference(variable_rename,[status(thm)],[c124])).
% 0.80/0.98  cnf(c126,plain,~singleton(X176,X177)|~multiple(X176,X177),inference(split_conjunct,[status(thm)],[c125])).
% 0.80/0.98  fof(ax56,axiom,(![U]:(![V]:(unisex(U,V)=>(~male(U,V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax56)).
% 0.80/0.98  fof(c115,plain,(![U]:(![V]:(unisex(U,V)=>~male(U,V)))),inference(fof_simplification,[status(thm)],[ax56])).
% 0.80/0.98  fof(c116,plain,(![U]:(![V]:(~unisex(U,V)|~male(U,V)))),inference(fof_nnf,[status(thm)],[c115])).
% 0.80/0.98  fof(c117,plain,(![X41]:(![X42]:(~unisex(X41,X42)|~male(X41,X42)))),inference(variable_rename,[status(thm)],[c116])).
% 0.80/0.98  cnf(c118,plain,~unisex(X172,X173)|~male(X172,X173),inference(split_conjunct,[status(thm)],[c117])).
% 0.80/0.98  fof(ax57,axiom,(![U]:(![V]:(young(U,V)=>(~old(U,V))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax57)).
% 0.80/0.98  fof(c111,plain,(![U]:(![V]:(young(U,V)=>~old(U,V)))),inference(fof_simplification,[status(thm)],[ax57])).
% 0.80/0.98  fof(c112,plain,(![U]:(![V]:(~young(U,V)|~old(U,V)))),inference(fof_nnf,[status(thm)],[c111])).
% 0.80/0.98  fof(c113,plain,(![X39]:(![X40]:(~young(X39,X40)|~old(X39,X40)))),inference(variable_rename,[status(thm)],[c112])).
% 0.80/0.98  cnf(c114,plain,~young(X170,X171)|~old(X170,X171),inference(split_conjunct,[status(thm)],[c113])).
% 0.80/0.98  cnf(c293,plain,~young(skolem0001,skolem0004),inference(resolution,[status(thm)],[c114, c73])).
% 0.80/0.98  cnf(c0,axiom,X165!=X164|X163!=X162|~furniture(X165,X163)|furniture(X164,X162),theory(equality)).
% 0.80/0.98  cnf(transitivity,axiom,X161!=X159|X159!=X160|X161=X160,theory(equality)).
% 0.80/0.98  cnf(symmetry,axiom,X157!=X156|X156=X157,theory(equality)).
% 0.80/0.98  fof(ax61,axiom,(![U]:(~(?[V]:member(U,V,V)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax61)).
% 0.80/0.98  fof(c88,plain,(![U]:(![V]:~member(U,V,V))),inference(fof_nnf,[status(thm)],[ax61])).
% 0.80/0.98  fof(c89,plain,(![X19]:(![X20]:~member(X19,X20,X20))),inference(variable_rename,[status(thm)],[c88])).
% 0.80/0.98  cnf(c90,plain,~member(X154,X155,X155),inference(split_conjunct,[status(thm)],[c89])).
% 0.80/0.98  cnf(c65,negated_conjecture,actual_world(skolem0001),inference(split_conjunct,[status(thm)],[c64])).
% 0.80/0.98  % SZS output end Saturation
% 0.80/0.98  
% 0.80/0.98  % Initial clauses    : 152
% 0.80/0.98  % Processed clauses  : 350
% 0.80/0.98  % Factors computed   : 3
% 0.80/0.98  % Resolvents computed: 269
% 0.80/0.98  % Tautologies deleted: 3
% 0.80/0.98  % Forward subsumed   : 71
% 0.80/0.98  % Backward subsumed  : 0
% 0.80/0.98  % -------- CPU Time ---------
% 0.80/0.98  % User time          : 0.609 s
% 0.80/0.98  % System time        : 0.024 s
% 0.80/0.98  % Total time         : 0.633 s
%------------------------------------------------------------------------------