%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP038+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:33:44 EDT 2024
% Result : CounterSatisfiable 0.61s 0.82s
% Output : Saturation 0.61s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : NLP038+1 : TPTP v8.1.2. Released v2.4.0.
% 0.06/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n013.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:34:38 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.61/0.82 % Version: 1.5
% 0.61/0.82 % SZS status CounterSatisfiable
% 0.61/0.82 % SZS output start Saturation
% 0.61/0.82 cnf(reflexivity,axiom,X105=X105,theory(equality)).
% 0.61/0.82 fof(co1,conjecture,(~(?[U]:(actual_world(U)&(?[V]:(?[W]:((((table(U,V)&(![X]:(member(U,X,W)=>(?[Y]:(((![Z]:(member(U,Z,Y)=>(?[X1]:(((((event(U,X1)&agent(U,X1,X))&present(U,X1))&sit(U,X1))&at(U,X1,V))&with(U,X1,Z)))))&group(U,Y))&(![X2]:(member(U,X2,Y)=>hamburger(U,X2))))))))&three(U,W))&group(U,W))&(![X3]:(member(U,X3,W)=>(guy(U,X3)&young(U,X3)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1)).
% 0.61/0.82 fof(c41,negated_conjecture,(~(~(?[U]:(actual_world(U)&(?[V]:(?[W]:((((table(U,V)&(![X]:(member(U,X,W)=>(?[Y]:(((![Z]:(member(U,Z,Y)=>(?[X1]:(((((event(U,X1)&agent(U,X1,X))&present(U,X1))&sit(U,X1))&at(U,X1,V))&with(U,X1,Z)))))&group(U,Y))&(![X2]:(member(U,X2,Y)=>hamburger(U,X2))))))))&three(U,W))&group(U,W))&(![X3]:(member(U,X3,W)=>(guy(U,X3)&young(U,X3))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 0.61/0.82 fof(c42,negated_conjecture,(?[U]:(actual_world(U)&(?[V]:(?[W]:((((table(U,V)&(![X]:(~member(U,X,W)|(?[Y]:(((![Z]:(~member(U,Z,Y)|(?[X1]:(((((event(U,X1)&agent(U,X1,X))&present(U,X1))&sit(U,X1))&at(U,X1,V))&with(U,X1,Z)))))&group(U,Y))&(![X2]:(~member(U,X2,Y)|hamburger(U,X2))))))))&three(U,W))&group(U,W))&(![X3]:(~member(U,X3,W)|(guy(U,X3)&young(U,X3))))))))),inference(fof_nnf,[status(thm)],[c41])).
% 0.61/0.82 fof(c43,negated_conjecture,(?[X2]:(actual_world(X2)&(?[X3]:(?[X4]:((((table(X2,X3)&(![X5]:(~member(X2,X5,X4)|(?[X6]:(((![X7]:(~member(X2,X7,X6)|(?[X8]:(((((event(X2,X8)&agent(X2,X8,X5))&present(X2,X8))&sit(X2,X8))&at(X2,X8,X3))&with(X2,X8,X7)))))&group(X2,X6))&(![X9]:(~member(X2,X9,X6)|hamburger(X2,X9))))))))&three(X2,X4))&group(X2,X4))&(![X10]:(~member(X2,X10,X4)|(guy(X2,X10)&young(X2,X10))))))))),inference(variable_rename,[status(thm)],[c42])).
% 0.61/0.82 fof(c45,negated_conjecture,(![X5]:(![X7]:(![X9]:(![X10]:(actual_world(skolem0001)&((((table(skolem0001,skolem0002)&(~member(skolem0001,X5,skolem0003)|(((~member(skolem0001,X7,skolem0004(X5))|(((((event(skolem0001,skolem0005(X5,X7))&agent(skolem0001,skolem0005(X5,X7),X5))&present(skolem0001,skolem0005(X5,X7)))&sit(skolem0001,skolem0005(X5,X7)))&at(skolem0001,skolem0005(X5,X7),skolem0002))&with(skolem0001,skolem0005(X5,X7),X7)))&group(skolem0001,skolem0004(X5)))&(~member(skolem0001,X9,skolem0004(X5))|hamburger(skolem0001,X9)))))&three(skolem0001,skolem0003))&group(skolem0001,skolem0003))&(~member(skolem0001,X10,skolem0003)|(guy(skolem0001,X10)&young(skolem0001,X10))))))))),inference(shift_quantors,[status(thm)],[fof(c44,negated_conjecture,(actual_world(skolem0001)&((((table(skolem0001,skolem0002)&(![X5]:(~member(skolem0001,X5,skolem0003)|(((![X7]:(~member(skolem0001,X7,skolem0004(X5))|(((((event(skolem0001,skolem0005(X5,X7))&agent(skolem0001,skolem0005(X5,X7),X5))&present(skolem0001,skolem0005(X5,X7)))&sit(skolem0001,skolem0005(X5,X7)))&at(skolem0001,skolem0005(X5,X7),skolem0002))&with(skolem0001,skolem0005(X5,X7),X7))))&group(skolem0001,skolem0004(X5)))&(![X9]:(~member(skolem0001,X9,skolem0004(X5))|hamburger(skolem0001,X9)))))))&three(skolem0001,skolem0003))&group(skolem0001,skolem0003))&(![X10]:(~member(skolem0001,X10,skolem0003)|(guy(skolem0001,X10)&young(skolem0001,X10)))))),inference(skolemize,[status(esa)],[c43])).])).
% 0.61/0.82 fof(c46,negated_conjecture,(![X5]:(![X7]:(![X9]:(![X10]:(actual_world(skolem0001)&((((table(skolem0001,skolem0002)&((((((((~member(skolem0001,X5,skolem0003)|(~member(skolem0001,X7,skolem0004(X5))|event(skolem0001,skolem0005(X5,X7))))&(~member(skolem0001,X5,skolem0003)|(~member(skolem0001,X7,skolem0004(X5))|agent(skolem0001,skolem0005(X5,X7),X5))))&(~member(skolem0001,X5,skolem0003)|(~member(skolem0001,X7,skolem0004(X5))|present(skolem0001,skolem0005(X5,X7)))))&(~member(skolem0001,X5,skolem0003)|(~member(skolem0001,X7,skolem0004(X5))|sit(skolem0001,skolem0005(X5,X7)))))&(~member(skolem0001,X5,skolem0003)|(~member(skolem0001,X7,skolem0004(X5))|at(skolem0001,skolem0005(X5,X7),skolem0002))))&(~member(skolem0001,X5,skolem0003)|(~member(skolem0001,X7,skolem0004(X5))|with(skolem0001,skolem0005(X5,X7),X7))))&(~member(skolem0001,X5,skolem0003)|group(skolem0001,skolem0004(X5))))&(~member(skolem0001,X5,skolem0003)|(~member(skolem0001,X9,skolem0004(X5))|hamburger(skolem0001,X9)))))&three(skolem0001,skolem0003))&group(skolem0001,skolem0003))&((~member(skolem0001,X10,skolem0003)|guy(skolem0001,X10))&(~member(skolem0001,X10,skolem0003)|young(skolem0001,X10))))))))),inference(distribute,[status(thm)],[c45])).
% 0.61/0.82 cnf(c57,negated_conjecture,three(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c46])).
% 0.61/0.82 fof(ax41,axiom,(![U]:(![V]:(three(U,V)<=>(?[W]:(member(U,W,V)&(?[X]:((member(U,X,V)&X!=W)&(?[Y]:(((member(U,Y,V)&Y!=X)&Y!=W)&(![Z]:(member(U,Z,V)=>((Z=Y|Z=X)|Z=W)))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax41)).
% 0.61/0.82 fof(c64,plain,(![U]:(![V]:((~three(U,V)|(?[W]:(member(U,W,V)&(?[X]:((member(U,X,V)&X!=W)&(?[Y]:(((member(U,Y,V)&Y!=X)&Y!=W)&(![Z]:(~member(U,Z,V)|((Z=Y|Z=X)|Z=W))))))))))&((![W]:(~member(U,W,V)|(![X]:((~member(U,X,V)|X=W)|(![Y]:(((~member(U,Y,V)|Y=X)|Y=W)|(?[Z]:(member(U,Z,V)&((Z!=Y&Z!=X)&Z!=W)))))))))|three(U,V))))),inference(fof_nnf,[status(thm)],[ax41])).
% 0.61/0.82 fof(c65,plain,((![U]:(![V]:(~three(U,V)|(?[W]:(member(U,W,V)&(?[X]:((member(U,X,V)&X!=W)&(?[Y]:(((member(U,Y,V)&Y!=X)&Y!=W)&(![Z]:(~member(U,Z,V)|((Z=Y|Z=X)|Z=W))))))))))))&(![U]:(![V]:((![W]:(~member(U,W,V)|(![X]:((~member(U,X,V)|X=W)|(![Y]:(((~member(U,Y,V)|Y=X)|Y=W)|(?[Z]:(member(U,Z,V)&((Z!=Y&Z!=X)&Z!=W)))))))))|three(U,V))))),inference(shift_quantors,[status(thm)],[c64])).
% 0.61/0.82 fof(c66,plain,((![X13]:(![X14]:(~three(X13,X14)|(?[X15]:(member(X13,X15,X14)&(?[X16]:((member(X13,X16,X14)&X16!=X15)&(?[X17]:(((member(X13,X17,X14)&X17!=X16)&X17!=X15)&(![X18]:(~member(X13,X18,X14)|((X18=X17|X18=X16)|X18=X15))))))))))))&(![X19]:(![X20]:((![X21]:(~member(X19,X21,X20)|(![X22]:((~member(X19,X22,X20)|X22=X21)|(![X23]:(((~member(X19,X23,X20)|X23=X22)|X23=X21)|(?[X24]:(member(X19,X24,X20)&((X24!=X23&X24!=X22)&X24!=X21)))))))))|three(X19,X20))))),inference(variable_rename,[status(thm)],[c65])).
% 0.61/0.82 fof(c68,plain,(![X13]:(![X14]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:((~three(X13,X14)|(member(X13,skolem0006(X13,X14),X14)&((member(X13,skolem0007(X13,X14),X14)&skolem0007(X13,X14)!=skolem0006(X13,X14))&(((member(X13,skolem0008(X13,X14),X14)&skolem0008(X13,X14)!=skolem0007(X13,X14))&skolem0008(X13,X14)!=skolem0006(X13,X14))&(~member(X13,X18,X14)|((X18=skolem0008(X13,X14)|X18=skolem0007(X13,X14))|X18=skolem0006(X13,X14)))))))&((~member(X19,X21,X20)|((~member(X19,X22,X20)|X22=X21)|(((~member(X19,X23,X20)|X23=X22)|X23=X21)|(member(X19,skolem0009(X19,X20,X21,X22,X23),X20)&((skolem0009(X19,X20,X21,X22,X23)!=X23&skolem0009(X19,X20,X21,X22,X23)!=X22)&skolem0009(X19,X20,X21,X22,X23)!=X21)))))|three(X19,X20))))))))))),inference(shift_quantors,[status(thm)],[fof(c67,plain,((![X13]:(![X14]:(~three(X13,X14)|(member(X13,skolem0006(X13,X14),X14)&((member(X13,skolem0007(X13,X14),X14)&skolem0007(X13,X14)!=skolem0006(X13,X14))&(((member(X13,skolem0008(X13,X14),X14)&skolem0008(X13,X14)!=skolem0007(X13,X14))&skolem0008(X13,X14)!=skolem0006(X13,X14))&(![X18]:(~member(X13,X18,X14)|((X18=skolem0008(X13,X14)|X18=skolem0007(X13,X14))|X18=skolem0006(X13,X14))))))))))&(![X19]:(![X20]:((![X21]:(~member(X19,X21,X20)|(![X22]:((~member(X19,X22,X20)|X22=X21)|(![X23]:(((~member(X19,X23,X20)|X23=X22)|X23=X21)|(member(X19,skolem0009(X19,X20,X21,X22,X23),X20)&((skolem0009(X19,X20,X21,X22,X23)!=X23&skolem0009(X19,X20,X21,X22,X23)!=X22)&skolem0009(X19,X20,X21,X22,X23)!=X21))))))))|three(X19,X20))))),inference(skolemize,[status(esa)],[c66])).])).
% 0.61/0.82 fof(c69,plain,(![X13]:(![X14]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(((~three(X13,X14)|member(X13,skolem0006(X13,X14),X14))&(((~three(X13,X14)|member(X13,skolem0007(X13,X14),X14))&(~three(X13,X14)|skolem0007(X13,X14)!=skolem0006(X13,X14)))&((((~three(X13,X14)|member(X13,skolem0008(X13,X14),X14))&(~three(X13,X14)|skolem0008(X13,X14)!=skolem0007(X13,X14)))&(~three(X13,X14)|skolem0008(X13,X14)!=skolem0006(X13,X14)))&(~three(X13,X14)|(~member(X13,X18,X14)|((X18=skolem0008(X13,X14)|X18=skolem0007(X13,X14))|X18=skolem0006(X13,X14)))))))&(((~member(X19,X21,X20)|((~member(X19,X22,X20)|X22=X21)|(((~member(X19,X23,X20)|X23=X22)|X23=X21)|member(X19,skolem0009(X19,X20,X21,X22,X23),X20))))|three(X19,X20))&((((~member(X19,X21,X20)|((~member(X19,X22,X20)|X22=X21)|(((~member(X19,X23,X20)|X23=X22)|X23=X21)|skolem0009(X19,X20,X21,X22,X23)!=X23)))|three(X19,X20))&((~member(X19,X21,X20)|((~member(X19,X22,X20)|X22=X21)|(((~member(X19,X23,X20)|X23=X22)|X23=X21)|skolem0009(X19,X20,X21,X22,X23)!=X22)))|three(X19,X20)))&((~member(X19,X21,X20)|((~member(X19,X22,X20)|X22=X21)|(((~member(X19,X23,X20)|X23=X22)|X23=X21)|skolem0009(X19,X20,X21,X22,X23)!=X21)))|three(X19,X20))))))))))))),inference(distribute,[status(thm)],[c68])).
% 0.61/0.82 cnf(c73,plain,~three(X254,X255)|member(X254,skolem0008(X254,X255),X255),inference(split_conjunct,[status(thm)],[c69])).
% 0.61/0.82 cnf(c237,plain,member(skolem0001,skolem0008(skolem0001,skolem0003),skolem0003),inference(resolution,[status(thm)],[c73, c57])).
% 0.61/0.82 cnf(c34,axiom,X398!=X396|X395!=X397|X394!=X393|~member(X398,X395,X394)|member(X396,X397,X393),theory(equality)).
% 0.61/0.82 cnf(c391,plain,skolem0001!=X643|skolem0008(skolem0001,skolem0003)!=X642|skolem0003!=X641|member(X643,X642,X641),inference(resolution,[status(thm)],[c34, c237])).
% 0.61/0.82 cnf(c520,plain,skolem0001!=X648|skolem0003!=X649|member(X648,skolem0008(skolem0001,skolem0003),X649),inference(resolution,[status(thm)],[c391, reflexivity])).
% 0.61/0.82 cnf(c524,plain,skolem0001!=X650|member(X650,skolem0008(skolem0001,skolem0003),skolem0003),inference(resolution,[status(thm)],[c520, reflexivity])).
% 0.61/0.82 cnf(c71,plain,~three(X252,X253)|member(X252,skolem0007(X252,X253),X253),inference(split_conjunct,[status(thm)],[c69])).
% 0.61/0.82 cnf(c236,plain,member(skolem0001,skolem0007(skolem0001,skolem0003),skolem0003),inference(resolution,[status(thm)],[c71, c57])).
% 0.61/0.82 cnf(c390,plain,skolem0001!=X635|skolem0007(skolem0001,skolem0003)!=X634|skolem0003!=X633|member(X635,X634,X633),inference(resolution,[status(thm)],[c34, c236])).
% 0.61/0.82 cnf(c516,plain,skolem0001!=X645|skolem0003!=X646|member(X645,skolem0007(skolem0001,skolem0003),X646),inference(resolution,[status(thm)],[c390, reflexivity])).
% 0.61/0.82 cnf(c522,plain,skolem0001!=X647|member(X647,skolem0007(skolem0001,skolem0003),skolem0003),inference(resolution,[status(thm)],[c516, reflexivity])).
% 0.61/0.82 cnf(c70,plain,~three(X250,X251)|member(X250,skolem0006(X250,X251),X251),inference(split_conjunct,[status(thm)],[c69])).
% 0.61/0.82 cnf(c235,plain,member(skolem0001,skolem0006(skolem0001,skolem0003),skolem0003),inference(resolution,[status(thm)],[c70, c57])).
% 0.61/0.82 cnf(c389,plain,skolem0001!=X626|skolem0006(skolem0001,skolem0003)!=X625|skolem0003!=X624|member(X626,X625,X624),inference(resolution,[status(thm)],[c34, c235])).
% 0.61/0.82 cnf(c511,plain,skolem0001!=X640|skolem0003!=X639|member(X640,skolem0006(skolem0001,skolem0003),X639),inference(resolution,[status(thm)],[c389, reflexivity])).
% 0.61/0.82 cnf(c519,plain,skolem0001!=X644|member(X644,skolem0006(skolem0001,skolem0003),skolem0003),inference(resolution,[status(thm)],[c511, reflexivity])).
% 0.61/0.82 cnf(c60,negated_conjecture,~member(skolem0001,X245,skolem0003)|young(skolem0001,X245),inference(split_conjunct,[status(thm)],[c46])).
% 0.61/0.82 cnf(c263,plain,young(skolem0001,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c236, c60])).
% 0.61/0.82 cnf(c36,axiom,X407!=X406|X408!=X405|~young(X407,X408)|young(X406,X405),theory(equality)).
% 0.61/0.82 cnf(c398,plain,skolem0001!=X636|skolem0007(skolem0001,skolem0003)!=X637|young(X636,X637),inference(resolution,[status(thm)],[c36, c263])).
% 0.61/0.82 cnf(c517,plain,skolem0001!=X638|young(X638,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c398, reflexivity])).
% 0.61/0.82 cnf(c284,plain,young(skolem0001,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c237, c60])).
% 0.61/0.82 cnf(c397,plain,skolem0001!=X630|skolem0008(skolem0001,skolem0003)!=X631|young(X630,X631),inference(resolution,[status(thm)],[c36, c284])).
% 0.61/0.82 cnf(c514,plain,skolem0001!=X632|young(X632,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c397, reflexivity])).
% 0.61/0.82 cnf(c239,plain,young(skolem0001,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c235, c60])).
% 0.61/0.82 cnf(c396,plain,skolem0001!=X627|skolem0006(skolem0001,skolem0003)!=X628|young(X627,X628),inference(resolution,[status(thm)],[c36, c239])).
% 0.61/0.82 cnf(c512,plain,skolem0001!=X629|young(X629,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c396, reflexivity])).
% 0.61/0.82 cnf(c59,negated_conjecture,~member(skolem0001,X244,skolem0003)|guy(skolem0001,X244),inference(split_conjunct,[status(thm)],[c46])).
% 0.61/0.82 cnf(c262,plain,guy(skolem0001,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c236, c59])).
% 0.61/0.82 cnf(c33,axiom,X387!=X386|X388!=X385|~guy(X387,X388)|guy(X386,X385),theory(equality)).
% 0.61/0.82 cnf(c385,plain,skolem0001!=X621|skolem0007(skolem0001,skolem0003)!=X622|guy(X621,X622),inference(resolution,[status(thm)],[c33, c262])).
% 0.61/0.82 cnf(c509,plain,skolem0001!=X623|guy(X623,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c385, reflexivity])).
% 0.61/0.82 cnf(c283,plain,guy(skolem0001,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c237, c59])).
% 0.61/0.82 cnf(c384,plain,skolem0001!=X618|skolem0008(skolem0001,skolem0003)!=X619|guy(X618,X619),inference(resolution,[status(thm)],[c33, c283])).
% 0.61/0.82 cnf(c507,plain,skolem0001!=X620|guy(X620,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c384, reflexivity])).
% 0.61/0.82 cnf(c238,plain,guy(skolem0001,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c235, c59])).
% 0.61/0.82 cnf(c383,plain,skolem0001!=X615|skolem0006(skolem0001,skolem0003)!=X616|guy(X615,X616),inference(resolution,[status(thm)],[c33, c238])).
% 0.61/0.82 cnf(c505,plain,skolem0001!=X617|guy(X617,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c383, reflexivity])).
% 0.61/0.82 fof(ax30,axiom,(![U]:(![V]:(thing(U,V)=>singleton(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax30)).
% 0.61/0.82 fof(c116,plain,(![U]:(![V]:(~thing(U,V)|singleton(U,V)))),inference(fof_nnf,[status(thm)],[ax30])).
% 0.61/0.82 fof(c117,plain,(![X45]:(![X46]:(~thing(X45,X46)|singleton(X45,X46)))),inference(variable_rename,[status(thm)],[c116])).
% 0.61/0.82 cnf(c118,plain,~thing(X138,X139)|singleton(X138,X139),inference(split_conjunct,[status(thm)],[c117])).
% 0.61/0.82 fof(ax31,axiom,(![U]:(![V]:(entity(U,V)=>thing(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax31)).
% 0.61/0.82 fof(c113,plain,(![U]:(![V]:(~entity(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax31])).
% 0.61/0.82 fof(c114,plain,(![X43]:(![X44]:(~entity(X43,X44)|thing(X43,X44)))),inference(variable_rename,[status(thm)],[c113])).
% 0.61/0.82 cnf(c115,plain,~entity(X136,X137)|thing(X136,X137),inference(split_conjunct,[status(thm)],[c114])).
% 0.61/0.82 fof(ax32,axiom,(![U]:(![V]:(organism(U,V)=>entity(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax32)).
% 0.61/0.82 fof(c110,plain,(![U]:(![V]:(~organism(U,V)|entity(U,V)))),inference(fof_nnf,[status(thm)],[ax32])).
% 0.61/0.82 fof(c111,plain,(![X41]:(![X42]:(~organism(X41,X42)|entity(X41,X42)))),inference(variable_rename,[status(thm)],[c110])).
% 0.61/0.82 cnf(c112,plain,~organism(X134,X135)|entity(X134,X135),inference(split_conjunct,[status(thm)],[c111])).
% 0.61/0.82 fof(ax33,axiom,(![U]:(![V]:(human_person(U,V)=>organism(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax33)).
% 0.61/0.82 fof(c107,plain,(![U]:(![V]:(~human_person(U,V)|organism(U,V)))),inference(fof_nnf,[status(thm)],[ax33])).
% 0.61/0.82 fof(c108,plain,(![X39]:(![X40]:(~human_person(X39,X40)|organism(X39,X40)))),inference(variable_rename,[status(thm)],[c107])).
% 0.61/0.82 cnf(c109,plain,~human_person(X128,X129)|organism(X128,X129),inference(split_conjunct,[status(thm)],[c108])).
% 0.61/0.82 fof(ax34,axiom,(![U]:(![V]:(man(U,V)=>human_person(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax34)).
% 0.61/0.82 fof(c104,plain,(![U]:(![V]:(~man(U,V)|human_person(U,V)))),inference(fof_nnf,[status(thm)],[ax34])).
% 0.61/0.82 fof(c105,plain,(![X37]:(![X38]:(~man(X37,X38)|human_person(X37,X38)))),inference(variable_rename,[status(thm)],[c104])).
% 0.61/0.82 cnf(c106,plain,~man(X126,X127)|human_person(X126,X127),inference(split_conjunct,[status(thm)],[c105])).
% 0.61/0.82 fof(ax35,axiom,(![U]:(![V]:(guy(U,V)=>man(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax35)).
% 0.61/0.82 fof(c101,plain,(![U]:(![V]:(~guy(U,V)|man(U,V)))),inference(fof_nnf,[status(thm)],[ax35])).
% 0.61/0.82 fof(c102,plain,(![X35]:(![X36]:(~guy(X35,X36)|man(X35,X36)))),inference(variable_rename,[status(thm)],[c101])).
% 0.61/0.82 cnf(c103,plain,~guy(X125,X124)|man(X125,X124),inference(split_conjunct,[status(thm)],[c102])).
% 0.61/0.82 cnf(c240,plain,man(skolem0001,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c238, c103])).
% 0.61/0.82 cnf(c242,plain,human_person(skolem0001,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c240, c106])).
% 0.61/0.82 cnf(c245,plain,organism(skolem0001,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c242, c109])).
% 0.61/0.82 cnf(c251,plain,entity(skolem0001,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c245, c112])).
% 0.61/0.82 cnf(c255,plain,thing(skolem0001,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c251, c115])).
% 0.61/0.82 cnf(c260,plain,singleton(skolem0001,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c255, c118])).
% 0.61/0.82 cnf(c32,axiom,X378!=X377|X379!=X376|~singleton(X378,X379)|singleton(X377,X376),theory(equality)).
% 0.61/0.82 cnf(c379,plain,skolem0001!=X612|skolem0006(skolem0001,skolem0003)!=X613|singleton(X612,X613),inference(resolution,[status(thm)],[c32, c260])).
% 0.61/0.82 cnf(c503,plain,skolem0001!=X614|singleton(X614,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c379, reflexivity])).
% 0.61/0.82 cnf(c285,plain,man(skolem0001,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c283, c103])).
% 0.61/0.82 cnf(c286,plain,human_person(skolem0001,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c285, c106])).
% 0.61/0.82 cnf(c289,plain,organism(skolem0001,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c286, c109])).
% 0.61/0.82 cnf(c295,plain,entity(skolem0001,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c289, c112])).
% 0.61/0.82 cnf(c299,plain,thing(skolem0001,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c295, c115])).
% 0.61/0.82 cnf(c304,plain,singleton(skolem0001,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c299, c118])).
% 0.61/0.82 cnf(c377,plain,skolem0001!=X609|skolem0008(skolem0001,skolem0003)!=X610|singleton(X609,X610),inference(resolution,[status(thm)],[c32, c304])).
% 0.61/0.82 cnf(c501,plain,skolem0001!=X611|singleton(X611,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c377, reflexivity])).
% 0.61/0.82 cnf(c264,plain,man(skolem0001,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c262, c103])).
% 0.61/0.82 cnf(c265,plain,human_person(skolem0001,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c264, c106])).
% 0.61/0.82 cnf(c268,plain,organism(skolem0001,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c265, c109])).
% 0.61/0.82 cnf(c273,plain,entity(skolem0001,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c268, c112])).
% 0.61/0.82 cnf(c276,plain,thing(skolem0001,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c273, c115])).
% 0.61/0.82 cnf(c281,plain,singleton(skolem0001,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c276, c118])).
% 0.61/0.82 cnf(c376,plain,skolem0001!=X606|skolem0007(skolem0001,skolem0003)!=X607|singleton(X606,X607),inference(resolution,[status(thm)],[c32, c281])).
% 0.61/0.82 cnf(c499,plain,skolem0001!=X608|singleton(X608,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c376, reflexivity])).
% 0.61/0.82 fof(ax28,axiom,(![U]:(![V]:(entity(U,V)=>existent(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax28)).
% 0.61/0.82 fof(c122,plain,(![U]:(![V]:(~entity(U,V)|existent(U,V)))),inference(fof_nnf,[status(thm)],[ax28])).
% 0.61/0.82 fof(c123,plain,(![X49]:(![X50]:(~entity(X49,X50)|existent(X49,X50)))),inference(variable_rename,[status(thm)],[c122])).
% 0.61/0.82 cnf(c124,plain,~entity(X143,X142)|existent(X143,X142),inference(split_conjunct,[status(thm)],[c123])).
% 0.61/0.82 cnf(c301,plain,existent(skolem0001,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c295, c124])).
% 0.61/0.82 cnf(c31,axiom,X368!=X367|X369!=X366|~existent(X368,X369)|existent(X367,X366),theory(equality)).
% 0.61/0.82 cnf(c370,plain,skolem0001!=X604|skolem0008(skolem0001,skolem0003)!=X603|existent(X604,X603),inference(resolution,[status(thm)],[c31, c301])).
% 0.61/0.82 cnf(c497,plain,skolem0001!=X605|existent(X605,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c370, reflexivity])).
% 0.61/0.82 cnf(c257,plain,existent(skolem0001,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c251, c124])).
% 0.61/0.82 cnf(c369,plain,skolem0001!=X601|skolem0006(skolem0001,skolem0003)!=X600|existent(X601,X600),inference(resolution,[status(thm)],[c31, c257])).
% 0.61/0.82 cnf(c495,plain,skolem0001!=X602|existent(X602,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c369, reflexivity])).
% 0.61/0.82 cnf(c278,plain,existent(skolem0001,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c273, c124])).
% 0.61/0.82 cnf(c368,plain,skolem0001!=X598|skolem0007(skolem0001,skolem0003)!=X597|existent(X598,X597),inference(resolution,[status(thm)],[c31, c278])).
% 0.61/0.82 cnf(c493,plain,skolem0001!=X599|existent(X599,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c368, reflexivity])).
% 0.61/0.82 cnf(c23,axiom,X303!=X302|X304!=X301|~multiple(X303,X304)|multiple(X302,X301),theory(equality)).
% 0.61/0.82 fof(ax21,axiom,(![U]:(![V]:(set(U,V)=>multiple(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax21)).
% 0.61/0.82 fof(c143,plain,(![U]:(![V]:(~set(U,V)|multiple(U,V)))),inference(fof_nnf,[status(thm)],[ax21])).
% 0.61/0.82 fof(c144,plain,(![X63]:(![X64]:(~set(X63,X64)|multiple(X63,X64)))),inference(variable_rename,[status(thm)],[c143])).
% 0.61/0.82 cnf(c145,plain,~set(X164,X165)|multiple(X164,X165),inference(split_conjunct,[status(thm)],[c144])).
% 0.61/0.82 fof(ax22,axiom,(![U]:(![V]:(group(U,V)=>set(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax22)).
% 0.61/0.82 fof(c140,plain,(![U]:(![V]:(~group(U,V)|set(U,V)))),inference(fof_nnf,[status(thm)],[ax22])).
% 0.61/0.82 fof(c141,plain,(![X61]:(![X62]:(~group(X61,X62)|set(X61,X62)))),inference(variable_rename,[status(thm)],[c140])).
% 0.61/0.82 cnf(c142,plain,~group(X162,X163)|set(X162,X163),inference(split_conjunct,[status(thm)],[c141])).
% 0.61/0.82 cnf(c55,negated_conjecture,~member(skolem0001,X300,skolem0003)|group(skolem0001,skolem0004(X300)),inference(split_conjunct,[status(thm)],[c46])).
% 0.61/0.82 cnf(c309,plain,group(skolem0001,skolem0004(skolem0008(skolem0001,skolem0003))),inference(resolution,[status(thm)],[c55, c237])).
% 0.61/0.82 cnf(c315,plain,set(skolem0001,skolem0004(skolem0008(skolem0001,skolem0003))),inference(resolution,[status(thm)],[c309, c142])).
% 0.61/0.82 cnf(c322,plain,multiple(skolem0001,skolem0004(skolem0008(skolem0001,skolem0003))),inference(resolution,[status(thm)],[c315, c145])).
% 0.61/0.82 cnf(c330,plain,skolem0001!=X595|skolem0004(skolem0008(skolem0001,skolem0003))!=X594|multiple(X595,X594),inference(resolution,[status(thm)],[c322, c23])).
% 0.61/0.82 cnf(c491,plain,skolem0001!=X596|multiple(X596,skolem0004(skolem0008(skolem0001,skolem0003))),inference(resolution,[status(thm)],[c330, reflexivity])).
% 0.61/0.82 fof(ax26,axiom,(![U]:(![V]:(organism(U,V)=>living(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax26)).
% 0.61/0.82 fof(c128,plain,(![U]:(![V]:(~organism(U,V)|living(U,V)))),inference(fof_nnf,[status(thm)],[ax26])).
% 0.61/0.82 fof(c129,plain,(![X53]:(![X54]:(~organism(X53,X54)|living(X53,X54)))),inference(variable_rename,[status(thm)],[c128])).
% 0.61/0.82 cnf(c130,plain,~organism(X151,X150)|living(X151,X150),inference(split_conjunct,[status(thm)],[c129])).
% 0.61/0.82 cnf(c271,plain,living(skolem0001,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c268, c130])).
% 0.61/0.82 cnf(c30,axiom,X360!=X359|X361!=X358|~living(X360,X361)|living(X359,X358),theory(equality)).
% 0.61/0.82 cnf(c364,plain,skolem0001!=X592|skolem0007(skolem0001,skolem0003)!=X591|living(X592,X591),inference(resolution,[status(thm)],[c30, c271])).
% 0.61/0.82 cnf(c489,plain,skolem0001!=X593|living(X593,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c364, reflexivity])).
% 0.61/0.82 cnf(c308,plain,group(skolem0001,skolem0004(skolem0007(skolem0001,skolem0003))),inference(resolution,[status(thm)],[c55, c236])).
% 0.61/0.82 cnf(c312,plain,set(skolem0001,skolem0004(skolem0007(skolem0001,skolem0003))),inference(resolution,[status(thm)],[c308, c142])).
% 0.61/0.82 cnf(c320,plain,multiple(skolem0001,skolem0004(skolem0007(skolem0001,skolem0003))),inference(resolution,[status(thm)],[c312, c145])).
% 0.61/0.82 cnf(c328,plain,skolem0001!=X589|skolem0004(skolem0007(skolem0001,skolem0003))!=X588|multiple(X589,X588),inference(resolution,[status(thm)],[c320, c23])).
% 0.61/0.82 cnf(c487,plain,skolem0001!=X590|multiple(X590,skolem0004(skolem0007(skolem0001,skolem0003))),inference(resolution,[status(thm)],[c328, reflexivity])).
% 0.61/0.82 cnf(c249,plain,living(skolem0001,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c245, c130])).
% 0.61/0.82 cnf(c363,plain,skolem0001!=X586|skolem0006(skolem0001,skolem0003)!=X585|living(X586,X585),inference(resolution,[status(thm)],[c30, c249])).
% 0.61/0.82 cnf(c485,plain,skolem0001!=X587|living(X587,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c363, reflexivity])).
% 0.61/0.83 cnf(c307,plain,group(skolem0001,skolem0004(skolem0006(skolem0001,skolem0003))),inference(resolution,[status(thm)],[c55, c235])).
% 0.61/0.83 cnf(c310,plain,set(skolem0001,skolem0004(skolem0006(skolem0001,skolem0003))),inference(resolution,[status(thm)],[c307, c142])).
% 0.61/0.83 cnf(c318,plain,multiple(skolem0001,skolem0004(skolem0006(skolem0001,skolem0003))),inference(resolution,[status(thm)],[c310, c145])).
% 0.61/0.83 cnf(c323,plain,skolem0001!=X583|skolem0004(skolem0006(skolem0001,skolem0003))!=X582|multiple(X583,X582),inference(resolution,[status(thm)],[c318, c23])).
% 0.61/0.83 cnf(c483,plain,skolem0001!=X584|multiple(X584,skolem0004(skolem0006(skolem0001,skolem0003))),inference(resolution,[status(thm)],[c323, reflexivity])).
% 0.61/0.83 cnf(c293,plain,living(skolem0001,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c289, c130])).
% 0.61/0.83 cnf(c362,plain,skolem0001!=X580|skolem0008(skolem0001,skolem0003)!=X579|living(X580,X579),inference(resolution,[status(thm)],[c30, c293])).
% 0.61/0.83 cnf(c481,plain,skolem0001!=X581|living(X581,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c362, reflexivity])).
% 0.61/0.83 cnf(c22,axiom,X298!=X297|X299!=X296|~set(X298,X299)|set(X297,X296),theory(equality)).
% 0.61/0.83 cnf(c321,plain,skolem0001!=X577|skolem0004(skolem0008(skolem0001,skolem0003))!=X576|set(X577,X576),inference(resolution,[status(thm)],[c315, c22])).
% 0.61/0.83 cnf(c479,plain,skolem0001!=X578|set(X578,skolem0004(skolem0008(skolem0001,skolem0003))),inference(resolution,[status(thm)],[c321, reflexivity])).
% 0.61/0.83 cnf(c29,axiom,X351!=X350|X352!=X349|~organism(X351,X352)|organism(X350,X349),theory(equality)).
% 0.61/0.83 cnf(c358,plain,skolem0001!=X574|skolem0008(skolem0001,skolem0003)!=X573|organism(X574,X573),inference(resolution,[status(thm)],[c29, c289])).
% 0.61/0.83 cnf(c477,plain,skolem0001!=X575|organism(X575,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c358, reflexivity])).
% 0.61/0.83 cnf(c319,plain,skolem0001!=X571|skolem0004(skolem0007(skolem0001,skolem0003))!=X570|set(X571,X570),inference(resolution,[status(thm)],[c312, c22])).
% 0.61/0.83 cnf(c475,plain,skolem0001!=X572|set(X572,skolem0004(skolem0007(skolem0001,skolem0003))),inference(resolution,[status(thm)],[c319, reflexivity])).
% 0.61/0.83 cnf(c357,plain,skolem0001!=X568|skolem0007(skolem0001,skolem0003)!=X567|organism(X568,X567),inference(resolution,[status(thm)],[c29, c268])).
% 0.61/0.83 cnf(c473,plain,skolem0001!=X569|organism(X569,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c357, reflexivity])).
% 0.61/0.83 cnf(c317,plain,skolem0001!=X565|skolem0004(skolem0006(skolem0001,skolem0003))!=X564|set(X565,X564),inference(resolution,[status(thm)],[c310, c22])).
% 0.61/0.83 cnf(c471,plain,skolem0001!=X566|set(X566,skolem0004(skolem0006(skolem0001,skolem0003))),inference(resolution,[status(thm)],[c317, reflexivity])).
% 0.61/0.83 cnf(c356,plain,skolem0001!=X562|skolem0006(skolem0001,skolem0003)!=X561|organism(X562,X561),inference(resolution,[status(thm)],[c29, c245])).
% 0.61/0.83 cnf(c469,plain,skolem0001!=X563|organism(X563,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c356, reflexivity])).
% 0.61/0.83 cnf(c21,axiom,X294!=X293|X295!=X292|~group(X294,X295)|group(X293,X292),theory(equality)).
% 0.61/0.83 cnf(c316,plain,skolem0001!=X558|skolem0004(skolem0008(skolem0001,skolem0003))!=X559|group(X558,X559),inference(resolution,[status(thm)],[c309, c21])).
% 0.61/0.83 cnf(c467,plain,skolem0001!=X560|group(X560,skolem0004(skolem0008(skolem0001,skolem0003))),inference(resolution,[status(thm)],[c316, reflexivity])).
% 0.61/0.83 fof(ax25,axiom,(![U]:(![V]:(human_person(U,V)=>human(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax25)).
% 0.61/0.83 fof(c131,plain,(![U]:(![V]:(~human_person(U,V)|human(U,V)))),inference(fof_nnf,[status(thm)],[ax25])).
% 0.61/0.83 fof(c132,plain,(![X55]:(![X56]:(~human_person(X55,X56)|human(X55,X56)))),inference(variable_rename,[status(thm)],[c131])).
% 0.61/0.83 cnf(c133,plain,~human_person(X152,X153)|human(X152,X153),inference(split_conjunct,[status(thm)],[c132])).
% 0.61/0.83 cnf(c290,plain,human(skolem0001,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c286, c133])).
% 0.61/0.83 cnf(c28,axiom,X341!=X340|X342!=X339|~human(X341,X342)|human(X340,X339),theory(equality)).
% 0.61/0.83 cnf(c351,plain,skolem0001!=X556|skolem0008(skolem0001,skolem0003)!=X555|human(X556,X555),inference(resolution,[status(thm)],[c28, c290])).
% 0.61/0.83 cnf(c465,plain,skolem0001!=X557|human(X557,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c351, reflexivity])).
% 0.61/0.83 cnf(c313,plain,skolem0001!=X552|skolem0004(skolem0007(skolem0001,skolem0003))!=X553|group(X552,X553),inference(resolution,[status(thm)],[c308, c21])).
% 0.61/0.83 cnf(c463,plain,skolem0001!=X554|group(X554,skolem0004(skolem0007(skolem0001,skolem0003))),inference(resolution,[status(thm)],[c313, reflexivity])).
% 0.61/0.83 cnf(c269,plain,human(skolem0001,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c265, c133])).
% 0.61/0.83 cnf(c350,plain,skolem0001!=X550|skolem0007(skolem0001,skolem0003)!=X549|human(X550,X549),inference(resolution,[status(thm)],[c28, c269])).
% 0.61/0.83 cnf(c461,plain,skolem0001!=X551|human(X551,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c350, reflexivity])).
% 0.61/0.83 cnf(c311,plain,skolem0001!=X546|skolem0004(skolem0006(skolem0001,skolem0003))!=X547|group(X546,X547),inference(resolution,[status(thm)],[c307, c21])).
% 0.61/0.83 cnf(c459,plain,skolem0001!=X548|group(X548,skolem0004(skolem0006(skolem0001,skolem0003))),inference(resolution,[status(thm)],[c311, reflexivity])).
% 0.61/0.83 cnf(c246,plain,human(skolem0001,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c242, c133])).
% 0.61/0.83 cnf(c349,plain,skolem0001!=X544|skolem0006(skolem0001,skolem0003)!=X543|human(X544,X543),inference(resolution,[status(thm)],[c28, c246])).
% 0.61/0.83 cnf(c457,plain,skolem0001!=X545|human(X545,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c349, reflexivity])).
% 0.61/0.83 fof(ax24,axiom,(![U]:(![V]:(human_person(U,V)=>animate(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax24)).
% 0.61/0.83 fof(c134,plain,(![U]:(![V]:(~human_person(U,V)|animate(U,V)))),inference(fof_nnf,[status(thm)],[ax24])).
% 0.61/0.83 fof(c135,plain,(![X57]:(![X58]:(~human_person(X57,X58)|animate(X57,X58)))),inference(variable_rename,[status(thm)],[c134])).
% 0.61/0.83 cnf(c136,plain,~human_person(X155,X154)|animate(X155,X154),inference(split_conjunct,[status(thm)],[c135])).
% 0.61/0.83 cnf(c244,plain,animate(skolem0001,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c242, c136])).
% 0.61/0.83 cnf(c27,axiom,X333!=X332|X334!=X331|~animate(X333,X334)|animate(X332,X331),theory(equality)).
% 0.61/0.83 cnf(c345,plain,skolem0001!=X536|skolem0006(skolem0001,skolem0003)!=X535|animate(X536,X535),inference(resolution,[status(thm)],[c27, c244])).
% 0.61/0.83 cnf(c455,plain,skolem0001!=X542|animate(X542,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c345, reflexivity])).
% 0.61/0.83 cnf(c80,plain,~member(X537,X539,X540)|~member(X537,X541,X540)|X541=X539|~member(X537,X538,X540)|X538=X541|X538=X539|skolem0009(X537,X540,X539,X541,X538)!=X539|three(X537,X540),inference(split_conjunct,[status(thm)],[c69])).
% 0.61/0.83 cnf(c267,plain,animate(skolem0001,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c265, c136])).
% 0.61/0.83 cnf(c344,plain,skolem0001!=X533|skolem0007(skolem0001,skolem0003)!=X532|animate(X533,X532),inference(resolution,[status(thm)],[c27, c267])).
% 0.61/0.83 cnf(c453,plain,skolem0001!=X534|animate(X534,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c344, reflexivity])).
% 0.61/0.83 cnf(c79,plain,~member(X527,X529,X530)|~member(X527,X531,X530)|X531=X529|~member(X527,X528,X530)|X528=X531|X528=X529|skolem0009(X527,X530,X529,X531,X528)!=X531|three(X527,X530),inference(split_conjunct,[status(thm)],[c69])).
% 0.61/0.83 cnf(c288,plain,animate(skolem0001,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c286, c136])).
% 0.61/0.83 cnf(c343,plain,skolem0001!=X525|skolem0008(skolem0001,skolem0003)!=X524|animate(X525,X524),inference(resolution,[status(thm)],[c27, c288])).
% 0.61/0.83 cnf(c451,plain,skolem0001!=X526|animate(X526,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c343, reflexivity])).
% 0.61/0.83 cnf(c26,axiom,X324!=X323|X325!=X322|~human_person(X324,X325)|human_person(X323,X322),theory(equality)).
% 0.61/0.83 cnf(c339,plain,skolem0001!=X521|skolem0007(skolem0001,skolem0003)!=X522|human_person(X521,X522),inference(resolution,[status(thm)],[c26, c265])).
% 0.61/0.83 cnf(c449,plain,skolem0001!=X523|human_person(X523,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c339, reflexivity])).
% 0.61/0.83 cnf(c78,plain,~member(X516,X518,X519)|~member(X516,X520,X519)|X520=X518|~member(X516,X517,X519)|X517=X520|X517=X518|skolem0009(X516,X519,X518,X520,X517)!=X517|three(X516,X519),inference(split_conjunct,[status(thm)],[c69])).
% 0.61/0.83 cnf(c338,plain,skolem0001!=X513|skolem0006(skolem0001,skolem0003)!=X514|human_person(X513,X514),inference(resolution,[status(thm)],[c26, c242])).
% 0.61/0.83 cnf(c447,plain,skolem0001!=X515|human_person(X515,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c338, reflexivity])).
% 0.61/0.83 cnf(c337,plain,skolem0001!=X505|skolem0008(skolem0001,skolem0003)!=X506|human_person(X505,X506),inference(resolution,[status(thm)],[c26, c286])).
% 0.61/0.83 cnf(c440,plain,skolem0001!=X512|human_person(X512,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c337, reflexivity])).
% 0.61/0.83 cnf(c77,plain,~member(X507,X509,X510)|~member(X507,X511,X510)|X511=X509|~member(X507,X508,X510)|X508=X511|X508=X509|member(X507,skolem0009(X507,X510,X509,X511,X508),X510)|three(X507,X510),inference(split_conjunct,[status(thm)],[c69])).
% 0.61/0.83 fof(ax23,axiom,(![U]:(![V]:(man(U,V)=>male(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax23)).
% 0.61/0.83 fof(c137,plain,(![U]:(![V]:(~man(U,V)|male(U,V)))),inference(fof_nnf,[status(thm)],[ax23])).
% 0.61/0.83 fof(c138,plain,(![X59]:(![X60]:(~man(X59,X60)|male(X59,X60)))),inference(variable_rename,[status(thm)],[c137])).
% 0.61/0.83 cnf(c139,plain,~man(X156,X157)|male(X156,X157),inference(split_conjunct,[status(thm)],[c138])).
% 0.61/0.83 cnf(c243,plain,male(skolem0001,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c240, c139])).
% 0.61/0.83 cnf(c25,axiom,X311!=X310|X312!=X309|~male(X311,X312)|male(X310,X309),theory(equality)).
% 0.61/0.83 cnf(c334,plain,skolem0001!=X502|skolem0006(skolem0001,skolem0003)!=X503|male(X502,X503),inference(resolution,[status(thm)],[c25, c243])).
% 0.61/0.83 cnf(c438,plain,skolem0001!=X504|male(X504,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c334, reflexivity])).
% 0.61/0.83 cnf(c76,plain,~three(X500,X501)|~member(X500,X499,X501)|X499=skolem0008(X500,X501)|X499=skolem0007(X500,X501)|X499=skolem0006(X500,X501),inference(split_conjunct,[status(thm)],[c69])).
% 0.61/0.83 cnf(c287,plain,male(skolem0001,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c285, c139])).
% 0.61/0.83 cnf(c333,plain,skolem0001!=X496|skolem0008(skolem0001,skolem0003)!=X497|male(X496,X497),inference(resolution,[status(thm)],[c25, c287])).
% 0.61/0.83 cnf(c433,plain,skolem0001!=X498|male(X498,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c333, reflexivity])).
% 0.61/0.83 cnf(c266,plain,male(skolem0001,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c264, c139])).
% 0.61/0.83 cnf(c332,plain,skolem0001!=X493|skolem0007(skolem0001,skolem0003)!=X494|male(X493,X494),inference(resolution,[status(thm)],[c25, c266])).
% 0.61/0.83 cnf(c431,plain,skolem0001!=X495|male(X495,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c332, reflexivity])).
% 0.61/0.83 cnf(c56,negated_conjecture,~member(skolem0001,X491,skolem0003)|~member(skolem0001,X492,skolem0004(X491))|hamburger(skolem0001,X492),inference(split_conjunct,[status(thm)],[c46])).
% 0.61/0.83 cnf(c24,axiom,X307!=X306|X308!=X305|~man(X307,X308)|man(X306,X305),theory(equality)).
% 0.61/0.83 cnf(c327,plain,skolem0001!=X488|skolem0008(skolem0001,skolem0003)!=X489|man(X488,X489),inference(resolution,[status(thm)],[c24, c285])).
% 0.61/0.83 cnf(c429,plain,skolem0001!=X490|man(X490,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c327, reflexivity])).
% 0.61/0.83 cnf(c326,plain,skolem0001!=X483|skolem0007(skolem0001,skolem0003)!=X484|man(X483,X484),inference(resolution,[status(thm)],[c24, c264])).
% 0.61/0.83 cnf(c427,plain,skolem0001!=X487|man(X487,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c326, reflexivity])).
% 0.61/0.83 cnf(c54,negated_conjecture,~member(skolem0001,X485,skolem0003)|~member(skolem0001,X486,skolem0004(X485))|with(skolem0001,skolem0005(X485,X486),X486),inference(split_conjunct,[status(thm)],[c46])).
% 0.61/0.83 cnf(c325,plain,skolem0001!=X480|skolem0006(skolem0001,skolem0003)!=X481|man(X480,X481),inference(resolution,[status(thm)],[c24, c240])).
% 0.61/0.83 cnf(c425,plain,skolem0001!=X482|man(X482,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c325, reflexivity])).
% 0.61/0.83 cnf(c53,negated_conjecture,~member(skolem0001,X478,skolem0003)|~member(skolem0001,X479,skolem0004(X478))|at(skolem0001,skolem0005(X478,X479),skolem0002),inference(split_conjunct,[status(thm)],[c46])).
% 0.61/0.83 cnf(c8,axiom,X228!=X227|X229!=X226|~specific(X228,X229)|specific(X227,X226),theory(equality)).
% 0.61/0.83 fof(ax29,axiom,(![U]:(![V]:(entity(U,V)=>specific(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax29)).
% 0.61/0.83 fof(c119,plain,(![U]:(![V]:(~entity(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax29])).
% 0.61/0.83 fof(c120,plain,(![X47]:(![X48]:(~entity(X47,X48)|specific(X47,X48)))),inference(variable_rename,[status(thm)],[c119])).
% 0.61/0.83 cnf(c121,plain,~entity(X140,X141)|specific(X140,X141),inference(split_conjunct,[status(thm)],[c120])).
% 0.61/0.83 cnf(c302,plain,specific(skolem0001,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c295, c121])).
% 0.61/0.83 cnf(c306,plain,skolem0001!=X476|skolem0008(skolem0001,skolem0003)!=X475|specific(X476,X475),inference(resolution,[status(thm)],[c302, c8])).
% 0.61/0.83 cnf(c423,plain,skolem0001!=X477|specific(X477,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c306, reflexivity])).
% 0.61/0.83 cnf(c9,axiom,X232!=X231|X233!=X230|~thing(X232,X233)|thing(X231,X230),theory(equality)).
% 0.61/0.83 cnf(c303,plain,skolem0001!=X473|skolem0008(skolem0001,skolem0003)!=X472|thing(X473,X472),inference(resolution,[status(thm)],[c299, c9])).
% 0.61/0.83 cnf(c421,plain,skolem0001!=X474|thing(X474,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c303, reflexivity])).
% 0.61/0.83 cnf(c52,negated_conjecture,~member(skolem0001,X470,skolem0003)|~member(skolem0001,X471,skolem0004(X470))|sit(skolem0001,skolem0005(X470,X471)),inference(split_conjunct,[status(thm)],[c46])).
% 0.61/0.83 cnf(c14,axiom,X266!=X265|X267!=X264|~entity(X266,X267)|entity(X265,X264),theory(equality)).
% 0.61/0.83 cnf(c300,plain,skolem0001!=X468|skolem0008(skolem0001,skolem0003)!=X467|entity(X468,X467),inference(resolution,[status(thm)],[c295, c14])).
% 0.61/0.83 cnf(c419,plain,skolem0001!=X469|entity(X469,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c300, reflexivity])).
% 0.61/0.83 cnf(c12,axiom,X258!=X257|X259!=X256|~impartial(X258,X259)|impartial(X257,X256),theory(equality)).
% 0.61/0.83 fof(ax27,axiom,(![U]:(![V]:(organism(U,V)=>impartial(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax27)).
% 0.61/0.83 fof(c125,plain,(![U]:(![V]:(~organism(U,V)|impartial(U,V)))),inference(fof_nnf,[status(thm)],[ax27])).
% 0.61/0.83 fof(c126,plain,(![X51]:(![X52]:(~organism(X51,X52)|impartial(X51,X52)))),inference(variable_rename,[status(thm)],[c125])).
% 0.61/0.83 cnf(c127,plain,~organism(X149,X148)|impartial(X149,X148),inference(split_conjunct,[status(thm)],[c126])).
% 0.61/0.83 cnf(c294,plain,impartial(skolem0001,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c289, c127])).
% 0.61/0.83 cnf(c298,plain,skolem0001!=X463|skolem0008(skolem0001,skolem0003)!=X462|impartial(X463,X462),inference(resolution,[status(thm)],[c294, c12])).
% 0.61/0.83 cnf(c417,plain,skolem0001!=X466|impartial(X466,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c298, reflexivity])).
% 0.61/0.83 cnf(c51,negated_conjecture,~member(skolem0001,X464,skolem0003)|~member(skolem0001,X465,skolem0004(X464))|present(skolem0001,skolem0005(X464,X465)),inference(split_conjunct,[status(thm)],[c46])).
% 0.61/0.83 cnf(c279,plain,specific(skolem0001,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c273, c121])).
% 0.61/0.83 cnf(c282,plain,skolem0001!=X460|skolem0007(skolem0001,skolem0003)!=X459|specific(X460,X459),inference(resolution,[status(thm)],[c279, c8])).
% 0.61/0.83 cnf(c415,plain,skolem0001!=X461|specific(X461,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c282, reflexivity])).
% 0.61/0.83 cnf(c50,negated_conjecture,~member(skolem0001,X457,skolem0003)|~member(skolem0001,X458,skolem0004(X457))|agent(skolem0001,skolem0005(X457,X458),X457),inference(split_conjunct,[status(thm)],[c46])).
% 0.61/0.83 cnf(c280,plain,skolem0001!=X455|skolem0007(skolem0001,skolem0003)!=X454|thing(X455,X454),inference(resolution,[status(thm)],[c276, c9])).
% 0.61/0.83 cnf(c413,plain,skolem0001!=X456|thing(X456,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c280, reflexivity])).
% 0.61/0.83 cnf(c277,plain,skolem0001!=X452|skolem0007(skolem0001,skolem0003)!=X451|entity(X452,X451),inference(resolution,[status(thm)],[c273, c14])).
% 0.61/0.83 cnf(c411,plain,skolem0001!=X453|entity(X453,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c277, reflexivity])).
% 0.61/0.83 cnf(c49,negated_conjecture,~member(skolem0001,X449,skolem0003)|~member(skolem0001,X450,skolem0004(X449))|event(skolem0001,skolem0005(X449,X450)),inference(split_conjunct,[status(thm)],[c46])).
% 0.61/0.83 cnf(c272,plain,impartial(skolem0001,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c268, c127])).
% 0.61/0.83 cnf(c275,plain,skolem0001!=X447|skolem0007(skolem0001,skolem0003)!=X446|impartial(X447,X446),inference(resolution,[status(thm)],[c272, c12])).
% 0.61/0.83 cnf(c409,plain,skolem0001!=X448|impartial(X448,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c275, reflexivity])).
% 0.61/0.83 cnf(c258,plain,specific(skolem0001,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c251, c121])).
% 0.61/0.83 cnf(c261,plain,skolem0001!=X438|skolem0006(skolem0001,skolem0003)!=X437|specific(X438,X437),inference(resolution,[status(thm)],[c258, c8])).
% 0.61/0.83 cnf(c407,plain,skolem0001!=X445|specific(X445,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c261, reflexivity])).
% 0.61/0.83 cnf(c40,axiom,X444!=X442|X441!=X443|X440!=X439|~agent(X444,X441,X440)|agent(X442,X443,X439),theory(equality)).
% 0.61/0.83 cnf(c259,plain,skolem0001!=X435|skolem0006(skolem0001,skolem0003)!=X434|thing(X435,X434),inference(resolution,[status(thm)],[c255, c9])).
% 0.61/0.83 cnf(c405,plain,skolem0001!=X436|thing(X436,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c259, reflexivity])).
% 0.61/0.83 cnf(c38,axiom,X433!=X431|X430!=X432|X429!=X428|~at(X433,X430,X429)|at(X431,X432,X428),theory(equality)).
% 0.61/0.83 cnf(c256,plain,skolem0001!=X426|skolem0006(skolem0001,skolem0003)!=X425|entity(X426,X425),inference(resolution,[status(thm)],[c251, c14])).
% 0.61/0.83 cnf(c403,plain,skolem0001!=X427|entity(X427,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c256, reflexivity])).
% 0.61/0.83 cnf(c250,plain,impartial(skolem0001,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c245, c127])).
% 0.61/0.83 cnf(c253,plain,skolem0001!=X423|skolem0006(skolem0001,skolem0003)!=X422|impartial(X423,X422),inference(resolution,[status(thm)],[c250, c12])).
% 0.61/0.83 cnf(c401,plain,skolem0001!=X424|impartial(X424,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c253, reflexivity])).
% 0.61/0.83 cnf(c37,axiom,X421!=X419|X418!=X420|X417!=X416|~with(X421,X418,X417)|with(X419,X420,X416),theory(equality)).
% 0.61/0.83 cnf(c39,axiom,X414!=X413|X415!=X412|~present(X414,X415)|present(X413,X412),theory(equality)).
% 0.61/0.83 fof(ax14,axiom,(![U]:(![V]:(object(U,V)=>entity(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax14)).
% 0.61/0.83 fof(c164,plain,(![U]:(![V]:(~object(U,V)|entity(U,V)))),inference(fof_nnf,[status(thm)],[ax14])).
% 0.61/0.83 fof(c165,plain,(![X77]:(![X78]:(~object(X77,X78)|entity(X77,X78)))),inference(variable_rename,[status(thm)],[c164])).
% 0.61/0.83 cnf(c166,plain,~object(X186,X187)|entity(X186,X187),inference(split_conjunct,[status(thm)],[c165])).
% 0.61/0.83 cnf(c48,negated_conjecture,table(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c46])).
% 0.61/0.83 fof(ax4,axiom,(![U]:(![V]:(table(U,V)=>furniture(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax4)).
% 0.61/0.83 fof(c194,plain,(![U]:(![V]:(~table(U,V)|furniture(U,V)))),inference(fof_nnf,[status(thm)],[ax4])).
% 0.61/0.83 fof(c195,plain,(![X97]:(![X98]:(~table(X97,X98)|furniture(X97,X98)))),inference(variable_rename,[status(thm)],[c194])).
% 0.61/0.83 cnf(c196,plain,~table(X214,X215)|furniture(X214,X215),inference(split_conjunct,[status(thm)],[c195])).
% 0.61/0.83 cnf(c214,plain,furniture(skolem0001,skolem0002),inference(resolution,[status(thm)],[c196, c48])).
% 0.61/0.83 fof(ax3,axiom,(![U]:(![V]:(furniture(U,V)=>instrumentality(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax3)).
% 0.61/0.83 fof(c197,plain,(![U]:(![V]:(~furniture(U,V)|instrumentality(U,V)))),inference(fof_nnf,[status(thm)],[ax3])).
% 0.61/0.83 fof(c198,plain,(![X99]:(![X100]:(~furniture(X99,X100)|instrumentality(X99,X100)))),inference(variable_rename,[status(thm)],[c197])).
% 0.61/0.83 cnf(c199,plain,~furniture(X216,X217)|instrumentality(X216,X217),inference(split_conjunct,[status(thm)],[c198])).
% 0.61/0.83 cnf(c216,plain,instrumentality(skolem0001,skolem0002),inference(resolution,[status(thm)],[c199, c214])).
% 0.61/0.83 fof(ax2,axiom,(![U]:(![V]:(instrumentality(U,V)=>artifact(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax2)).
% 0.61/0.83 fof(c200,plain,(![U]:(![V]:(~instrumentality(U,V)|artifact(U,V)))),inference(fof_nnf,[status(thm)],[ax2])).
% 0.61/0.83 fof(c201,plain,(![X101]:(![X102]:(~instrumentality(X101,X102)|artifact(X101,X102)))),inference(variable_rename,[status(thm)],[c200])).
% 0.61/0.83 cnf(c202,plain,~instrumentality(X223,X222)|artifact(X223,X222),inference(split_conjunct,[status(thm)],[c201])).
% 0.61/0.83 cnf(c218,plain,artifact(skolem0001,skolem0002),inference(resolution,[status(thm)],[c202, c216])).
% 0.61/0.83 fof(ax1,axiom,(![U]:(![V]:(artifact(U,V)=>object(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax1)).
% 0.61/0.83 fof(c203,plain,(![U]:(![V]:(~artifact(U,V)|object(U,V)))),inference(fof_nnf,[status(thm)],[ax1])).
% 0.61/0.83 fof(c204,plain,(![X103]:(![X104]:(~artifact(X103,X104)|object(X103,X104)))),inference(variable_rename,[status(thm)],[c203])).
% 0.61/0.83 cnf(c205,plain,~artifact(X225,X224)|object(X225,X224),inference(split_conjunct,[status(thm)],[c204])).
% 0.61/0.83 cnf(c220,plain,object(skolem0001,skolem0002),inference(resolution,[status(thm)],[c205, c218])).
% 0.61/0.83 cnf(c225,plain,entity(skolem0001,skolem0002),inference(resolution,[status(thm)],[c220, c166])).
% 0.61/0.83 cnf(c228,plain,thing(skolem0001,skolem0002),inference(resolution,[status(thm)],[c225, c115])).
% 0.61/0.83 cnf(c232,plain,singleton(skolem0001,skolem0002),inference(resolution,[status(thm)],[c228, c118])).
% 0.61/0.83 cnf(c378,plain,skolem0001!=X409|skolem0002!=X410|singleton(X409,X410),inference(resolution,[status(thm)],[c32, c232])).
% 0.61/0.83 cnf(c399,plain,skolem0001!=X411|singleton(X411,skolem0002),inference(resolution,[status(thm)],[c378, reflexivity])).
% 0.61/0.83 cnf(c229,plain,existent(skolem0001,skolem0002),inference(resolution,[status(thm)],[c225, c124])).
% 0.61/0.83 cnf(c371,plain,skolem0001!=X403|skolem0002!=X402|existent(X403,X402),inference(resolution,[status(thm)],[c31, c229])).
% 0.61/0.83 cnf(c394,plain,skolem0001!=X404|existent(X404,skolem0002),inference(resolution,[status(thm)],[c371, reflexivity])).
% 0.61/0.83 cnf(c58,negated_conjecture,group(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c46])).
% 0.61/0.83 cnf(c209,plain,set(skolem0001,skolem0003),inference(resolution,[status(thm)],[c142, c58])).
% 0.61/0.83 cnf(c210,plain,multiple(skolem0001,skolem0003),inference(resolution,[status(thm)],[c145, c209])).
% 0.61/0.83 cnf(c314,plain,skolem0001!=X400|skolem0003!=X399|multiple(X400,X399),inference(resolution,[status(thm)],[c23, c210])).
% 0.61/0.83 cnf(c392,plain,skolem0001!=X401|multiple(X401,skolem0003),inference(resolution,[status(thm)],[c314, reflexivity])).
% 0.61/0.83 cnf(c305,plain,skolem0001!=X391|skolem0003!=X390|set(X391,X390),inference(resolution,[status(thm)],[c22, c209])).
% 0.61/0.83 cnf(c387,plain,skolem0001!=X392|set(X392,skolem0003),inference(resolution,[status(thm)],[c305, reflexivity])).
% 0.61/0.83 cnf(c297,plain,skolem0001!=X383|skolem0003!=X384|group(X383,X384),inference(resolution,[status(thm)],[c21, c58])).
% 0.61/0.83 cnf(c382,plain,skolem0001!=X389|group(X389,skolem0003),inference(resolution,[status(thm)],[c297, reflexivity])).
% 0.61/0.83 cnf(c20,axiom,X290!=X289|X291!=X288|~three(X290,X291)|three(X289,X288),theory(equality)).
% 0.61/0.83 cnf(c292,plain,skolem0001!=X380|skolem0003!=X381|three(X380,X381),inference(resolution,[status(thm)],[c20, c57])).
% 0.61/0.83 cnf(c380,plain,skolem0001!=X382|three(X382,skolem0003),inference(resolution,[status(thm)],[c292, reflexivity])).
% 0.61/0.83 cnf(c254,plain,skolem0001!=X374|skolem0002!=X373|entity(X374,X373),inference(resolution,[status(thm)],[c14, c225])).
% 0.61/0.83 cnf(c374,plain,skolem0001!=X375|entity(X375,skolem0002),inference(resolution,[status(thm)],[c254, reflexivity])).
% 0.61/0.83 fof(ax13,axiom,(![U]:(![V]:(object(U,V)=>nonliving(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax13)).
% 0.61/0.83 fof(c167,plain,(![U]:(![V]:(~object(U,V)|nonliving(U,V)))),inference(fof_nnf,[status(thm)],[ax13])).
% 0.61/0.83 fof(c168,plain,(![X79]:(![X80]:(~object(X79,X80)|nonliving(X79,X80)))),inference(variable_rename,[status(thm)],[c167])).
% 0.61/0.83 cnf(c169,plain,~object(X188,X189)|nonliving(X188,X189),inference(split_conjunct,[status(thm)],[c168])).
% 0.61/0.83 cnf(c222,plain,nonliving(skolem0001,skolem0002),inference(resolution,[status(thm)],[c220, c169])).
% 0.61/0.83 cnf(c13,axiom,X262!=X261|X263!=X260|~nonliving(X262,X263)|nonliving(X261,X260),theory(equality)).
% 0.61/0.83 cnf(c248,plain,skolem0001!=X370|skolem0002!=X371|nonliving(X370,X371),inference(resolution,[status(thm)],[c13, c222])).
% 0.61/0.83 cnf(c372,plain,skolem0001!=X372|nonliving(X372,skolem0002),inference(resolution,[status(thm)],[c248, reflexivity])).
% 0.61/0.83 fof(ax12,axiom,(![U]:(![V]:(object(U,V)=>impartial(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax12)).
% 0.61/0.83 fof(c170,plain,(![U]:(![V]:(~object(U,V)|impartial(U,V)))),inference(fof_nnf,[status(thm)],[ax12])).
% 0.61/0.83 fof(c171,plain,(![X81]:(![X82]:(~object(X81,X82)|impartial(X81,X82)))),inference(variable_rename,[status(thm)],[c170])).
% 0.61/0.83 cnf(c172,plain,~object(X191,X190)|impartial(X191,X190),inference(split_conjunct,[status(thm)],[c171])).
% 0.61/0.83 cnf(c221,plain,impartial(skolem0001,skolem0002),inference(resolution,[status(thm)],[c220, c172])).
% 0.61/0.83 cnf(c241,plain,skolem0001!=X364|skolem0002!=X363|impartial(X364,X363),inference(resolution,[status(thm)],[c12, c221])).
% 0.61/0.83 cnf(c366,plain,skolem0001!=X365|impartial(X365,skolem0002),inference(resolution,[status(thm)],[c241, reflexivity])).
% 0.61/0.83 cnf(c230,plain,specific(skolem0001,skolem0002),inference(resolution,[status(thm)],[c225, c121])).
% 0.61/0.83 cnf(c233,plain,skolem0001!=X357|skolem0002!=X356|specific(X357,X356),inference(resolution,[status(thm)],[c230, c8])).
% 0.61/0.83 cnf(c361,plain,skolem0001!=X362|specific(X362,skolem0002),inference(resolution,[status(thm)],[c233, reflexivity])).
% 0.61/0.83 cnf(c231,plain,skolem0001!=X354|skolem0002!=X353|thing(X354,X353),inference(resolution,[status(thm)],[c228, c9])).
% 0.61/0.83 cnf(c359,plain,skolem0001!=X355|thing(X355,skolem0002),inference(resolution,[status(thm)],[c231, reflexivity])).
% 0.61/0.83 cnf(c6,axiom,X208!=X207|X209!=X206|~unisex(X208,X209)|unisex(X207,X206),theory(equality)).
% 0.61/0.83 fof(ax11,axiom,(![U]:(![V]:(object(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax11)).
% 0.61/0.83 fof(c173,plain,(![U]:(![V]:(~object(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax11])).
% 0.61/0.83 fof(c174,plain,(![X83]:(![X84]:(~object(X83,X84)|unisex(X83,X84)))),inference(variable_rename,[status(thm)],[c173])).
% 0.61/0.83 cnf(c175,plain,~object(X196,X197)|unisex(X196,X197),inference(split_conjunct,[status(thm)],[c174])).
% 0.61/0.83 cnf(c224,plain,unisex(skolem0001,skolem0002),inference(resolution,[status(thm)],[c220, c175])).
% 0.61/0.83 cnf(c227,plain,skolem0001!=X346|skolem0002!=X347|unisex(X346,X347),inference(resolution,[status(thm)],[c224, c6])).
% 0.61/0.83 cnf(c354,plain,skolem0001!=X348|unisex(X348,skolem0002),inference(resolution,[status(thm)],[c227, reflexivity])).
% 0.61/0.83 cnf(c1,axiom,X146!=X145|X147!=X144|~object(X146,X147)|object(X145,X144),theory(equality)).
% 0.61/0.83 cnf(c223,plain,skolem0001!=X343|skolem0002!=X344|object(X343,X344),inference(resolution,[status(thm)],[c220, c1])).
% 0.61/0.83 cnf(c352,plain,skolem0001!=X345|object(X345,skolem0002),inference(resolution,[status(thm)],[c223, reflexivity])).
% 0.61/0.83 cnf(c0,axiom,X132!=X131|X133!=X130|~artifact(X132,X133)|artifact(X131,X130),theory(equality)).
% 0.61/0.83 cnf(c219,plain,skolem0001!=X336|skolem0002!=X337|artifact(X336,X337),inference(resolution,[status(thm)],[c218, c0])).
% 0.61/0.83 cnf(c347,plain,skolem0001!=X338|artifact(X338,skolem0002),inference(resolution,[status(thm)],[c219, reflexivity])).
% 0.61/0.83 cnf(c2,axiom,X160!=X159|X161!=X158|~instrumentality(X160,X161)|instrumentality(X159,X158),theory(equality)).
% 0.61/0.83 cnf(c217,plain,skolem0001!=X329|skolem0002!=X330|instrumentality(X329,X330),inference(resolution,[status(thm)],[c216, c2])).
% 0.61/0.83 cnf(c342,plain,skolem0001!=X335|instrumentality(X335,skolem0002),inference(resolution,[status(thm)],[c217, reflexivity])).
% 0.61/0.83 cnf(c3,axiom,X168!=X167|X169!=X166|~furniture(X168,X169)|furniture(X167,X166),theory(equality)).
% 0.61/0.83 cnf(c215,plain,skolem0001!=X326|skolem0002!=X327|furniture(X326,X327),inference(resolution,[status(thm)],[c214, c3])).
% 0.61/0.83 cnf(c340,plain,skolem0001!=X328|furniture(X328,skolem0002),inference(resolution,[status(thm)],[c215, reflexivity])).
% 0.61/0.83 cnf(c4,axiom,X180!=X179|X181!=X178|~table(X180,X181)|table(X179,X178),theory(equality)).
% 0.61/0.83 cnf(c213,plain,skolem0001!=X320|skolem0002!=X319|table(X320,X319),inference(resolution,[status(thm)],[c4, c48])).
% 0.61/0.83 cnf(c335,plain,skolem0001!=X321|table(X321,skolem0002),inference(resolution,[status(thm)],[c213, reflexivity])).
% 0.61/0.83 cnf(c75,plain,~three(X317,X318)|skolem0008(X317,X318)!=skolem0006(X317,X318),inference(split_conjunct,[status(thm)],[c69])).
% 0.61/0.83 cnf(c74,plain,~three(X315,X316)|skolem0008(X315,X316)!=skolem0007(X315,X316),inference(split_conjunct,[status(thm)],[c69])).
% 0.61/0.83 cnf(c72,plain,~three(X313,X314)|skolem0007(X313,X314)!=skolem0006(X313,X314),inference(split_conjunct,[status(thm)],[c69])).
% 0.61/0.83 fof(ax39,axiom,(![U]:(![V]:(singleton(U,V)=>(~multiple(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax39)).
% 0.61/0.83 fof(c85,plain,(![U]:(![V]:(singleton(U,V)=>~multiple(U,V)))),inference(fof_simplification,[status(thm)],[ax39])).
% 0.61/0.83 fof(c86,plain,(![U]:(![V]:(~singleton(U,V)|~multiple(U,V)))),inference(fof_nnf,[status(thm)],[c85])).
% 0.61/0.83 fof(c87,plain,(![X27]:(![X28]:(~singleton(X27,X28)|~multiple(X27,X28)))),inference(variable_rename,[status(thm)],[c86])).
% 0.61/0.83 cnf(c88,plain,~singleton(X114,X113)|~multiple(X114,X113),inference(split_conjunct,[status(thm)],[c87])).
% 0.61/0.83 cnf(c331,plain,~singleton(skolem0001,skolem0004(skolem0008(skolem0001,skolem0003))),inference(resolution,[status(thm)],[c322, c88])).
% 0.61/0.83 cnf(c329,plain,~singleton(skolem0001,skolem0004(skolem0007(skolem0001,skolem0003))),inference(resolution,[status(thm)],[c320, c88])).
% 0.61/0.83 cnf(c324,plain,~singleton(skolem0001,skolem0004(skolem0006(skolem0001,skolem0003))),inference(resolution,[status(thm)],[c318, c88])).
% 0.61/0.83 fof(ax38,axiom,(![U]:(![V]:(nonliving(U,V)=>(~living(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax38)).
% 0.61/0.83 fof(c89,plain,(![U]:(![V]:(nonliving(U,V)=>~living(U,V)))),inference(fof_simplification,[status(thm)],[ax38])).
% 0.61/0.83 fof(c90,plain,(![U]:(![V]:(~nonliving(U,V)|~living(U,V)))),inference(fof_nnf,[status(thm)],[c89])).
% 0.61/0.83 fof(c91,plain,(![X29]:(![X30]:(~nonliving(X29,X30)|~living(X29,X30)))),inference(variable_rename,[status(thm)],[c90])).
% 0.61/0.83 cnf(c92,plain,~nonliving(X115,X116)|~living(X115,X116),inference(split_conjunct,[status(thm)],[c91])).
% 0.61/0.83 cnf(c296,plain,~nonliving(skolem0001,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c293, c92])).
% 0.61/0.83 fof(ax40,axiom,(![U]:(![V]:(unisex(U,V)=>(~male(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax40)).
% 0.61/0.83 fof(c81,plain,(![U]:(![V]:(unisex(U,V)=>~male(U,V)))),inference(fof_simplification,[status(thm)],[ax40])).
% 0.61/0.83 fof(c82,plain,(![U]:(![V]:(~unisex(U,V)|~male(U,V)))),inference(fof_nnf,[status(thm)],[c81])).
% 0.61/0.83 fof(c83,plain,(![X25]:(![X26]:(~unisex(X25,X26)|~male(X25,X26)))),inference(variable_rename,[status(thm)],[c82])).
% 0.61/0.83 cnf(c84,plain,~unisex(X111,X112)|~male(X111,X112),inference(split_conjunct,[status(thm)],[c83])).
% 0.61/0.83 cnf(c291,plain,~unisex(skolem0001,skolem0008(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c287, c84])).
% 0.61/0.83 cnf(c19,axiom,X286!=X285|X287!=X284|~hamburger(X286,X287)|hamburger(X285,X284),theory(equality)).
% 0.61/0.83 cnf(c18,axiom,X282!=X281|X283!=X280|~burger(X282,X283)|burger(X281,X280),theory(equality)).
% 0.61/0.83 cnf(c274,plain,~nonliving(skolem0001,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c271, c92])).
% 0.61/0.83 cnf(c270,plain,~unisex(skolem0001,skolem0007(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c266, c84])).
% 0.61/0.83 cnf(c17,axiom,X278!=X277|X279!=X276|~meat(X278,X279)|meat(X277,X276),theory(equality)).
% 0.61/0.83 cnf(c16,axiom,X274!=X273|X275!=X272|~food(X274,X275)|food(X273,X272),theory(equality)).
% 0.61/0.83 cnf(c15,axiom,X270!=X269|X271!=X268|~substance_matter(X270,X271)|substance_matter(X269,X268),theory(equality)).
% 0.61/0.83 cnf(c252,plain,~nonliving(skolem0001,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c249, c92])).
% 0.61/0.83 cnf(c247,plain,~unisex(skolem0001,skolem0006(skolem0001,skolem0003)),inference(resolution,[status(thm)],[c243, c84])).
% 0.61/0.83 cnf(c11,axiom,X248!=X247|X249!=X246|~sit(X248,X249)|sit(X247,X246),theory(equality)).
% 0.61/0.83 cnf(c35,axiom,X242!=X241|~actual_world(X242)|actual_world(X241),theory(equality)).
% 0.61/0.83 cnf(c10,axiom,X237!=X236|X238!=X235|~event(X237,X238)|event(X236,X235),theory(equality)).
% 0.61/0.83 fof(ax36,axiom,(![U]:(![V]:(animate(U,V)=>(~nonliving(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax36)).
% 0.61/0.83 fof(c97,plain,(![U]:(![V]:(animate(U,V)=>~nonliving(U,V)))),inference(fof_simplification,[status(thm)],[ax36])).
% 0.61/0.83 fof(c98,plain,(![U]:(![V]:(~animate(U,V)|~nonliving(U,V)))),inference(fof_nnf,[status(thm)],[c97])).
% 0.61/0.83 fof(c99,plain,(![X33]:(![X34]:(~animate(X33,X34)|~nonliving(X33,X34)))),inference(variable_rename,[status(thm)],[c98])).
% 0.61/0.83 cnf(c100,plain,~animate(X122,X123)|~nonliving(X122,X123),inference(split_conjunct,[status(thm)],[c99])).
% 0.61/0.83 cnf(c226,plain,~animate(skolem0001,skolem0002),inference(resolution,[status(thm)],[c222, c100])).
% 0.61/0.83 cnf(c7,axiom,X220!=X219|X221!=X218|~nonexistent(X220,X221)|nonexistent(X219,X218),theory(equality)).
% 0.61/0.83 fof(ax5,axiom,(![U]:(![V]:(eventuality(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax5)).
% 0.61/0.83 fof(c191,plain,(![U]:(![V]:(~eventuality(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax5])).
% 0.61/0.83 fof(c192,plain,(![X95]:(![X96]:(~eventuality(X95,X96)|unisex(X95,X96)))),inference(variable_rename,[status(thm)],[c191])).
% 0.61/0.83 cnf(c193,plain,~eventuality(X212,X213)|unisex(X212,X213),inference(split_conjunct,[status(thm)],[c192])).
% 0.61/0.83 fof(ax6,axiom,(![U]:(![V]:(eventuality(U,V)=>nonexistent(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax6)).
% 0.61/0.83 fof(c188,plain,(![U]:(![V]:(~eventuality(U,V)|nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[ax6])).
% 0.61/0.83 fof(c189,plain,(![X93]:(![X94]:(~eventuality(X93,X94)|nonexistent(X93,X94)))),inference(variable_rename,[status(thm)],[c188])).
% 0.61/0.83 cnf(c190,plain,~eventuality(X210,X211)|nonexistent(X210,X211),inference(split_conjunct,[status(thm)],[c189])).
% 0.61/0.83 fof(ax7,axiom,(![U]:(![V]:(eventuality(U,V)=>specific(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax7)).
% 0.61/0.83 fof(c185,plain,(![U]:(![V]:(~eventuality(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax7])).
% 0.61/0.83 fof(c186,plain,(![X91]:(![X92]:(~eventuality(X91,X92)|specific(X91,X92)))),inference(variable_rename,[status(thm)],[c185])).
% 0.61/0.83 cnf(c187,plain,~eventuality(X205,X204)|specific(X205,X204),inference(split_conjunct,[status(thm)],[c186])).
% 0.61/0.83 fof(ax8,axiom,(![U]:(![V]:(eventuality(U,V)=>thing(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax8)).
% 0.61/0.83 fof(c182,plain,(![U]:(![V]:(~eventuality(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax8])).
% 0.61/0.83 fof(c183,plain,(![X89]:(![X90]:(~eventuality(X89,X90)|thing(X89,X90)))),inference(variable_rename,[status(thm)],[c182])).
% 0.61/0.83 cnf(c184,plain,~eventuality(X202,X203)|thing(X202,X203),inference(split_conjunct,[status(thm)],[c183])).
% 0.61/0.83 fof(ax9,axiom,(![U]:(![V]:(event(U,V)=>eventuality(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax9)).
% 0.61/0.83 fof(c179,plain,(![U]:(![V]:(~event(U,V)|eventuality(U,V)))),inference(fof_nnf,[status(thm)],[ax9])).
% 0.61/0.83 fof(c180,plain,(![X87]:(![X88]:(~event(X87,X88)|eventuality(X87,X88)))),inference(variable_rename,[status(thm)],[c179])).
% 0.61/0.83 cnf(c181,plain,~event(X200,X201)|eventuality(X200,X201),inference(split_conjunct,[status(thm)],[c180])).
% 0.61/0.83 fof(ax10,axiom,(![U]:(![V]:(sit(U,V)=>event(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax10)).
% 0.61/0.83 fof(c176,plain,(![U]:(![V]:(~sit(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax10])).
% 0.61/0.83 fof(c177,plain,(![X85]:(![X86]:(~sit(X85,X86)|event(X85,X86)))),inference(variable_rename,[status(thm)],[c176])).
% 0.61/0.83 cnf(c178,plain,~sit(X198,X199)|event(X198,X199),inference(split_conjunct,[status(thm)],[c177])).
% 0.61/0.83 cnf(c5,axiom,X194!=X193|X195!=X192|~eventuality(X194,X195)|eventuality(X193,X192),theory(equality)).
% 0.61/0.83 fof(ax15,axiom,(![U]:(![V]:(substance_matter(U,V)=>object(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax15)).
% 0.61/0.83 fof(c161,plain,(![U]:(![V]:(~substance_matter(U,V)|object(U,V)))),inference(fof_nnf,[status(thm)],[ax15])).
% 0.61/0.83 fof(c162,plain,(![X75]:(![X76]:(~substance_matter(X75,X76)|object(X75,X76)))),inference(variable_rename,[status(thm)],[c161])).
% 0.61/0.83 cnf(c163,plain,~substance_matter(X184,X185)|object(X184,X185),inference(split_conjunct,[status(thm)],[c162])).
% 0.61/0.83 fof(ax16,axiom,(![U]:(![V]:(food(U,V)=>substance_matter(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax16)).
% 0.61/0.83 fof(c158,plain,(![U]:(![V]:(~food(U,V)|substance_matter(U,V)))),inference(fof_nnf,[status(thm)],[ax16])).
% 0.61/0.83 fof(c159,plain,(![X73]:(![X74]:(~food(X73,X74)|substance_matter(X73,X74)))),inference(variable_rename,[status(thm)],[c158])).
% 0.61/0.83 cnf(c160,plain,~food(X182,X183)|substance_matter(X182,X183),inference(split_conjunct,[status(thm)],[c159])).
% 0.61/0.83 fof(ax17,axiom,(![U]:(![V]:(meat(U,V)=>food(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax17)).
% 0.61/0.83 fof(c155,plain,(![U]:(![V]:(~meat(U,V)|food(U,V)))),inference(fof_nnf,[status(thm)],[ax17])).
% 0.61/0.83 fof(c156,plain,(![X71]:(![X72]:(~meat(X71,X72)|food(X71,X72)))),inference(variable_rename,[status(thm)],[c155])).
% 0.61/0.83 cnf(c157,plain,~meat(X177,X176)|food(X177,X176),inference(split_conjunct,[status(thm)],[c156])).
% 0.61/0.83 fof(ax18,axiom,(![U]:(![V]:(burger(U,V)=>meat(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax18)).
% 0.61/0.83 fof(c152,plain,(![U]:(![V]:(~burger(U,V)|meat(U,V)))),inference(fof_nnf,[status(thm)],[ax18])).
% 0.61/0.83 fof(c153,plain,(![X69]:(![X70]:(~burger(X69,X70)|meat(X69,X70)))),inference(variable_rename,[status(thm)],[c152])).
% 0.61/0.83 cnf(c154,plain,~burger(X175,X174)|meat(X175,X174),inference(split_conjunct,[status(thm)],[c153])).
% 0.61/0.83 fof(ax19,axiom,(![U]:(![V]:(hamburger(U,V)=>burger(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax19)).
% 0.61/0.83 fof(c149,plain,(![U]:(![V]:(~hamburger(U,V)|burger(U,V)))),inference(fof_nnf,[status(thm)],[ax19])).
% 0.61/0.83 fof(c150,plain,(![X67]:(![X68]:(~hamburger(X67,X68)|burger(X67,X68)))),inference(variable_rename,[status(thm)],[c149])).
% 0.61/0.83 cnf(c151,plain,~hamburger(X172,X173)|burger(X172,X173),inference(split_conjunct,[status(thm)],[c150])).
% 0.61/0.83 fof(ax20,axiom,(![U]:(![V]:(three(U,V)=>group(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax20)).
% 0.61/0.83 fof(c146,plain,(![U]:(![V]:(~three(U,V)|group(U,V)))),inference(fof_nnf,[status(thm)],[ax20])).
% 0.61/0.83 fof(c147,plain,(![X65]:(![X66]:(~three(X65,X66)|group(X65,X66)))),inference(variable_rename,[status(thm)],[c146])).
% 0.61/0.83 cnf(c148,plain,~three(X170,X171)|group(X170,X171),inference(split_conjunct,[status(thm)],[c147])).
% 0.61/0.83 cnf(c211,plain,~singleton(skolem0001,skolem0003),inference(resolution,[status(thm)],[c210, c88])).
% 0.61/0.83 fof(ax37,axiom,(![U]:(![V]:(existent(U,V)=>(~nonexistent(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax37)).
% 0.61/0.83 fof(c93,plain,(![U]:(![V]:(existent(U,V)=>~nonexistent(U,V)))),inference(fof_simplification,[status(thm)],[ax37])).
% 0.61/0.83 fof(c94,plain,(![U]:(![V]:(~existent(U,V)|~nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[c93])).
% 0.61/0.83 fof(c95,plain,(![X31]:(![X32]:(~existent(X31,X32)|~nonexistent(X31,X32)))),inference(variable_rename,[status(thm)],[c94])).
% 0.61/0.83 cnf(c96,plain,~existent(X121,X120)|~nonexistent(X121,X120),inference(split_conjunct,[status(thm)],[c95])).
% 0.61/0.83 cnf(transitivity,axiom,X118!=X117|X117!=X119|X118=X119,theory(equality)).
% 0.61/0.83 cnf(symmetry,axiom,X109!=X108|X108=X109,theory(equality)).
% 0.61/0.83 fof(ax42,axiom,(![U]:(~(?[V]:member(U,V,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax42)).
% 0.61/0.83 fof(c61,plain,(![U]:(![V]:~member(U,V,V))),inference(fof_nnf,[status(thm)],[ax42])).
% 0.61/0.83 fof(c62,plain,(![X11]:(![X12]:~member(X11,X12,X12))),inference(variable_rename,[status(thm)],[c61])).
% 0.61/0.83 cnf(c63,plain,~member(X106,X107,X107),inference(split_conjunct,[status(thm)],[c62])).
% 0.61/0.83 cnf(c47,negated_conjecture,actual_world(skolem0001),inference(split_conjunct,[status(thm)],[c46])).
% 0.61/0.83 % SZS output end Saturation
% 0.61/0.83
% 0.61/0.83 % Initial clauses : 110
% 0.61/0.83 % Processed clauses : 343
% 0.61/0.83 % Factors computed : 3
% 0.61/0.83 % Resolvents computed: 317
% 0.61/0.83 % Tautologies deleted: 3
% 0.61/0.83 % Forward subsumed : 84
% 0.61/0.83 % Backward subsumed : 0
% 0.61/0.83 % -------- CPU Time ---------
% 0.61/0.83 % User time : 0.467 s
% 0.61/0.83 % System time : 0.009 s
% 0.61/0.83 % Total time : 0.476 s
%------------------------------------------------------------------------------