PyRes---1.5.CSA-Sat.s

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

% Computer : n011.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:27 EDT 2024

% Result   : CounterSatisfiable 0.69s 0.87s
% Output   : Saturation 0.69s
% Verified : 
% SZS Type : -

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