%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP037+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n028.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.53s 0.74s
% Output : Saturation 0.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : NLP037+1 : TPTP v8.1.2. Released v2.4.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n028.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed May 8 13:47:23 EDT 2024
% 0.14/0.36 % CPUTime :
% 0.53/0.74 % Version: 1.5
% 0.53/0.74 % SZS status CounterSatisfiable
% 0.53/0.74 % SZS output start Saturation
% 0.53/0.74 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.53/0.74 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.53/0.74 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.53/0.74 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.53/0.74 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.53/0.74 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.53/0.74 cnf(c77,plain,~member(X467,X466,X468)|~member(X467,X465,X468)|X465=X466|~member(X467,X469,X468)|X469=X465|X469=X466|member(X467,skolem0009(X467,X468,X466,X465,X469),X468)|three(X467,X468),inference(split_conjunct,[status(thm)],[c69])).
% 0.53/0.74 cnf(c80,plain,~member(X462,X461,X463)|~member(X462,X460,X463)|X460=X461|~member(X462,X464,X463)|X464=X460|X464=X461|skolem0009(X462,X463,X461,X460,X464)!=X461|three(X462,X463),inference(split_conjunct,[status(thm)],[c69])).
% 0.53/0.74 cnf(c79,plain,~member(X457,X456,X458)|~member(X457,X455,X458)|X455=X456|~member(X457,X459,X458)|X459=X455|X459=X456|skolem0009(X457,X458,X456,X455,X459)!=X455|three(X457,X458),inference(split_conjunct,[status(thm)],[c69])).
% 0.53/0.74 cnf(c78,plain,~member(X452,X451,X453)|~member(X452,X450,X453)|X450=X451|~member(X452,X454,X453)|X454=X450|X454=X451|skolem0009(X452,X453,X451,X450,X454)!=X454|three(X452,X453),inference(split_conjunct,[status(thm)],[c69])).
% 0.53/0.74 cnf(c76,plain,~three(X448,X449)|~member(X448,X447,X449)|X447=skolem0008(X448,X449)|X447=skolem0007(X448,X449)|X447=skolem0006(X448,X449),inference(split_conjunct,[status(thm)],[c69])).
% 0.53/0.74 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,Z))&present(U,X1))&sit(U,X1))&at(U,X1,V))&with(U,X1,X)))))&three(U,Y))&group(U,Y))&(![X2]:(member(U,X2,Y)=>(guy(U,X2)&young(U,X2)))))))))&group(U,W))&(![X3]:(member(U,X3,W)=>hamburger(U,X3))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1)).
% 0.53/0.74 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,Z))&present(U,X1))&sit(U,X1))&at(U,X1,V))&with(U,X1,X)))))&three(U,Y))&group(U,Y))&(![X2]:(member(U,X2,Y)=>(guy(U,X2)&young(U,X2)))))))))&group(U,W))&(![X3]:(member(U,X3,W)=>hamburger(U,X3)))))))))),inference(assume_negation,[status(cth)],[co1])).
% 0.53/0.74 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,Z))&present(U,X1))&sit(U,X1))&at(U,X1,V))&with(U,X1,X)))))&three(U,Y))&group(U,Y))&(![X2]:(~member(U,X2,Y)|(guy(U,X2)&young(U,X2)))))))))&group(U,W))&(![X3]:(~member(U,X3,W)|hamburger(U,X3)))))))),inference(fof_nnf,[status(thm)],[c41])).
% 0.53/0.74 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,X7))&present(X2,X8))&sit(X2,X8))&at(X2,X8,X3))&with(X2,X8,X5)))))&three(X2,X6))&group(X2,X6))&(![X9]:(~member(X2,X9,X6)|(guy(X2,X9)&young(X2,X9)))))))))&group(X2,X4))&(![X10]:(~member(X2,X10,X4)|hamburger(X2,X10)))))))),inference(variable_rename,[status(thm)],[c42])).
% 0.53/0.74 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),X7))&present(skolem0001,skolem0005(X5,X7)))&sit(skolem0001,skolem0005(X5,X7)))&at(skolem0001,skolem0005(X5,X7),skolem0002))&with(skolem0001,skolem0005(X5,X7),X5)))&three(skolem0001,skolem0004(X5)))&group(skolem0001,skolem0004(X5)))&(~member(skolem0001,X9,skolem0004(X5))|(guy(skolem0001,X9)&young(skolem0001,X9))))))&group(skolem0001,skolem0003))&(~member(skolem0001,X10,skolem0003)|hamburger(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),X7))&present(skolem0001,skolem0005(X5,X7)))&sit(skolem0001,skolem0005(X5,X7)))&at(skolem0001,skolem0005(X5,X7),skolem0002))&with(skolem0001,skolem0005(X5,X7),X5))))&three(skolem0001,skolem0004(X5)))&group(skolem0001,skolem0004(X5)))&(![X9]:(~member(skolem0001,X9,skolem0004(X5))|(guy(skolem0001,X9)&young(skolem0001,X9))))))))&group(skolem0001,skolem0003))&(![X10]:(~member(skolem0001,X10,skolem0003)|hamburger(skolem0001,X10))))),inference(skolemize,[status(esa)],[c43])).])).
% 0.53/0.74 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),X7))))&(~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),X5))))&(~member(skolem0001,X5,skolem0003)|three(skolem0001,skolem0004(X5))))&(~member(skolem0001,X5,skolem0003)|group(skolem0001,skolem0004(X5))))&((~member(skolem0001,X5,skolem0003)|(~member(skolem0001,X9,skolem0004(X5))|guy(skolem0001,X9)))&(~member(skolem0001,X5,skolem0003)|(~member(skolem0001,X9,skolem0004(X5))|young(skolem0001,X9))))))&group(skolem0001,skolem0003))&(~member(skolem0001,X10,skolem0003)|hamburger(skolem0001,X10)))))))),inference(distribute,[status(thm)],[c45])).
% 0.53/0.74 cnf(c53,negated_conjecture,~member(skolem0001,X445,skolem0003)|~member(skolem0001,X446,skolem0004(X445))|at(skolem0001,skolem0005(X445,X446),skolem0002),inference(split_conjunct,[status(thm)],[c46])).
% 0.53/0.74 cnf(c54,negated_conjecture,~member(skolem0001,X443,skolem0003)|~member(skolem0001,X444,skolem0004(X443))|with(skolem0001,skolem0005(X443,X444),X443),inference(split_conjunct,[status(thm)],[c46])).
% 0.53/0.74 cnf(c50,negated_conjecture,~member(skolem0001,X441,skolem0003)|~member(skolem0001,X442,skolem0004(X441))|agent(skolem0001,skolem0005(X441,X442),X442),inference(split_conjunct,[status(thm)],[c46])).
% 0.53/0.74 cnf(c52,negated_conjecture,~member(skolem0001,X439,skolem0003)|~member(skolem0001,X440,skolem0004(X439))|sit(skolem0001,skolem0005(X439,X440)),inference(split_conjunct,[status(thm)],[c46])).
% 0.53/0.74 cnf(c51,negated_conjecture,~member(skolem0001,X437,skolem0003)|~member(skolem0001,X438,skolem0004(X437))|present(skolem0001,skolem0005(X437,X438)),inference(split_conjunct,[status(thm)],[c46])).
% 0.53/0.74 cnf(c49,negated_conjecture,~member(skolem0001,X435,skolem0003)|~member(skolem0001,X436,skolem0004(X435))|event(skolem0001,skolem0005(X435,X436)),inference(split_conjunct,[status(thm)],[c46])).
% 0.53/0.74 cnf(c40,axiom,X434!=X429|X432!=X430|X433!=X431|~agent(X434,X432,X433)|agent(X429,X430,X431),theory(equality)).
% 0.53/0.74 cnf(c38,axiom,X428!=X423|X426!=X424|X427!=X425|~at(X428,X426,X427)|at(X423,X424,X425),theory(equality)).
% 0.53/0.74 cnf(c37,axiom,X422!=X417|X420!=X418|X421!=X419|~with(X422,X420,X421)|with(X417,X418,X419),theory(equality)).
% 0.53/0.74 cnf(c58,negated_conjecture,~member(skolem0001,X415,skolem0003)|~member(skolem0001,X416,skolem0004(X415))|young(skolem0001,X416),inference(split_conjunct,[status(thm)],[c46])).
% 0.53/0.74 cnf(c57,negated_conjecture,~member(skolem0001,X413,skolem0003)|~member(skolem0001,X414,skolem0004(X413))|guy(skolem0001,X414),inference(split_conjunct,[status(thm)],[c46])).
% 0.53/0.74 cnf(c34,axiom,X412!=X407|X410!=X408|X411!=X409|~member(X412,X410,X411)|member(X407,X408,X409),theory(equality)).
% 0.53/0.74 cnf(c39,axiom,X405!=X403|X404!=X406|~present(X405,X404)|present(X403,X406),theory(equality)).
% 0.53/0.74 cnf(c36,axiom,X401!=X399|X400!=X402|~young(X401,X400)|young(X399,X402),theory(equality)).
% 0.53/0.74 cnf(reflexivity,axiom,X105=X105,theory(equality)).
% 0.53/0.74 fof(ax30,axiom,(![U]:(![V]:(thing(U,V)=>singleton(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax30)).
% 0.53/0.74 fof(c116,plain,(![U]:(![V]:(~thing(U,V)|singleton(U,V)))),inference(fof_nnf,[status(thm)],[ax30])).
% 0.53/0.74 fof(c117,plain,(![X45]:(![X46]:(~thing(X45,X46)|singleton(X45,X46)))),inference(variable_rename,[status(thm)],[c116])).
% 0.53/0.74 cnf(c118,plain,~thing(X139,X138)|singleton(X139,X138),inference(split_conjunct,[status(thm)],[c117])).
% 0.53/0.74 fof(ax31,axiom,(![U]:(![V]:(entity(U,V)=>thing(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax31)).
% 0.53/0.74 fof(c113,plain,(![U]:(![V]:(~entity(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax31])).
% 0.53/0.74 fof(c114,plain,(![X43]:(![X44]:(~entity(X43,X44)|thing(X43,X44)))),inference(variable_rename,[status(thm)],[c113])).
% 0.53/0.74 cnf(c115,plain,~entity(X136,X137)|thing(X136,X137),inference(split_conjunct,[status(thm)],[c114])).
% 0.53/0.74 fof(ax14,axiom,(![U]:(![V]:(object(U,V)=>entity(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax14)).
% 0.53/0.74 fof(c164,plain,(![U]:(![V]:(~object(U,V)|entity(U,V)))),inference(fof_nnf,[status(thm)],[ax14])).
% 0.53/0.74 fof(c165,plain,(![X77]:(![X78]:(~object(X77,X78)|entity(X77,X78)))),inference(variable_rename,[status(thm)],[c164])).
% 0.53/0.74 cnf(c166,plain,~object(X186,X187)|entity(X186,X187),inference(split_conjunct,[status(thm)],[c165])).
% 0.53/0.74 cnf(c48,negated_conjecture,table(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c46])).
% 0.53/0.74 fof(ax4,axiom,(![U]:(![V]:(table(U,V)=>furniture(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax4)).
% 0.53/0.74 fof(c194,plain,(![U]:(![V]:(~table(U,V)|furniture(U,V)))),inference(fof_nnf,[status(thm)],[ax4])).
% 0.53/0.74 fof(c195,plain,(![X97]:(![X98]:(~table(X97,X98)|furniture(X97,X98)))),inference(variable_rename,[status(thm)],[c194])).
% 0.53/0.74 cnf(c196,plain,~table(X214,X215)|furniture(X214,X215),inference(split_conjunct,[status(thm)],[c195])).
% 0.53/0.74 cnf(c213,plain,furniture(skolem0001,skolem0002),inference(resolution,[status(thm)],[c196, c48])).
% 0.53/0.74 fof(ax3,axiom,(![U]:(![V]:(furniture(U,V)=>instrumentality(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax3)).
% 0.53/0.74 fof(c197,plain,(![U]:(![V]:(~furniture(U,V)|instrumentality(U,V)))),inference(fof_nnf,[status(thm)],[ax3])).
% 0.53/0.74 fof(c198,plain,(![X99]:(![X100]:(~furniture(X99,X100)|instrumentality(X99,X100)))),inference(variable_rename,[status(thm)],[c197])).
% 0.53/0.74 cnf(c199,plain,~furniture(X217,X216)|instrumentality(X217,X216),inference(split_conjunct,[status(thm)],[c198])).
% 0.53/0.74 cnf(c215,plain,instrumentality(skolem0001,skolem0002),inference(resolution,[status(thm)],[c199, c213])).
% 0.53/0.74 fof(ax2,axiom,(![U]:(![V]:(instrumentality(U,V)=>artifact(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax2)).
% 0.53/0.74 fof(c200,plain,(![U]:(![V]:(~instrumentality(U,V)|artifact(U,V)))),inference(fof_nnf,[status(thm)],[ax2])).
% 0.53/0.74 fof(c201,plain,(![X101]:(![X102]:(~instrumentality(X101,X102)|artifact(X101,X102)))),inference(variable_rename,[status(thm)],[c200])).
% 0.53/0.74 cnf(c202,plain,~instrumentality(X218,X219)|artifact(X218,X219),inference(split_conjunct,[status(thm)],[c201])).
% 0.53/0.74 cnf(c217,plain,artifact(skolem0001,skolem0002),inference(resolution,[status(thm)],[c202, c215])).
% 0.53/0.74 fof(ax1,axiom,(![U]:(![V]:(artifact(U,V)=>object(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax1)).
% 0.53/0.74 fof(c203,plain,(![U]:(![V]:(~artifact(U,V)|object(U,V)))),inference(fof_nnf,[status(thm)],[ax1])).
% 0.53/0.74 fof(c204,plain,(![X103]:(![X104]:(~artifact(X103,X104)|object(X103,X104)))),inference(variable_rename,[status(thm)],[c203])).
% 0.53/0.74 cnf(c205,plain,~artifact(X225,X224)|object(X225,X224),inference(split_conjunct,[status(thm)],[c204])).
% 0.53/0.74 cnf(c219,plain,object(skolem0001,skolem0002),inference(resolution,[status(thm)],[c205, c217])).
% 0.53/0.74 cnf(c222,plain,entity(skolem0001,skolem0002),inference(resolution,[status(thm)],[c219, c166])).
% 0.53/0.74 cnf(c226,plain,thing(skolem0001,skolem0002),inference(resolution,[status(thm)],[c222, c115])).
% 0.53/0.74 cnf(c230,plain,singleton(skolem0001,skolem0002),inference(resolution,[status(thm)],[c226, c118])).
% 0.53/0.74 cnf(c32,axiom,X390!=X388|X389!=X391|~singleton(X390,X389)|singleton(X388,X391),theory(equality)).
% 0.53/0.74 cnf(c271,plain,skolem0001!=X397|skolem0002!=X396|singleton(X397,X396),inference(resolution,[status(thm)],[c32, c230])).
% 0.53/0.74 cnf(c272,plain,skolem0001!=X398|singleton(X398,skolem0002),inference(resolution,[status(thm)],[c271, reflexivity])).
% 0.53/0.74 cnf(c33,axiom,X394!=X392|X393!=X395|~guy(X394,X393)|guy(X392,X395),theory(equality)).
% 0.53/0.74 fof(ax28,axiom,(![U]:(![V]:(entity(U,V)=>existent(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax28)).
% 0.53/0.74 fof(c122,plain,(![U]:(![V]:(~entity(U,V)|existent(U,V)))),inference(fof_nnf,[status(thm)],[ax28])).
% 0.53/0.74 fof(c123,plain,(![X49]:(![X50]:(~entity(X49,X50)|existent(X49,X50)))),inference(variable_rename,[status(thm)],[c122])).
% 0.53/0.74 cnf(c124,plain,~entity(X142,X143)|existent(X142,X143),inference(split_conjunct,[status(thm)],[c123])).
% 0.53/0.74 cnf(c227,plain,existent(skolem0001,skolem0002),inference(resolution,[status(thm)],[c222, c124])).
% 0.53/0.74 cnf(c31,axiom,X383!=X381|X382!=X384|~existent(X383,X382)|existent(X381,X384),theory(equality)).
% 0.53/0.74 cnf(c268,plain,skolem0001!=X386|skolem0002!=X385|existent(X386,X385),inference(resolution,[status(thm)],[c31, c227])).
% 0.53/0.74 cnf(c269,plain,skolem0001!=X387|existent(X387,skolem0002),inference(resolution,[status(thm)],[c268, reflexivity])).
% 0.53/0.74 cnf(c30,axiom,X379!=X377|X378!=X380|~living(X379,X378)|living(X377,X380),theory(equality)).
% 0.53/0.74 cnf(c29,axiom,X375!=X373|X374!=X376|~organism(X375,X374)|organism(X373,X376),theory(equality)).
% 0.53/0.74 cnf(c28,axiom,X371!=X369|X370!=X372|~human(X371,X370)|human(X369,X372),theory(equality)).
% 0.53/0.74 cnf(c27,axiom,X367!=X365|X366!=X368|~animate(X367,X366)|animate(X365,X368),theory(equality)).
% 0.53/0.74 cnf(c26,axiom,X363!=X361|X362!=X364|~human_person(X363,X362)|human_person(X361,X364),theory(equality)).
% 0.53/0.74 cnf(c25,axiom,X359!=X357|X358!=X360|~male(X359,X358)|male(X357,X360),theory(equality)).
% 0.53/0.74 cnf(c24,axiom,X355!=X353|X354!=X356|~man(X355,X354)|man(X353,X356),theory(equality)).
% 0.53/0.74 cnf(c59,negated_conjecture,group(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c46])).
% 0.53/0.74 fof(ax22,axiom,(![U]:(![V]:(group(U,V)=>set(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax22)).
% 0.53/0.74 fof(c140,plain,(![U]:(![V]:(~group(U,V)|set(U,V)))),inference(fof_nnf,[status(thm)],[ax22])).
% 0.53/0.74 fof(c141,plain,(![X61]:(![X62]:(~group(X61,X62)|set(X61,X62)))),inference(variable_rename,[status(thm)],[c140])).
% 0.53/0.74 cnf(c142,plain,~group(X158,X159)|set(X158,X159),inference(split_conjunct,[status(thm)],[c141])).
% 0.53/0.74 cnf(c209,plain,set(skolem0001,skolem0003),inference(resolution,[status(thm)],[c142, c59])).
% 0.53/0.74 fof(ax21,axiom,(![U]:(![V]:(set(U,V)=>multiple(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax21)).
% 0.53/0.74 fof(c143,plain,(![U]:(![V]:(~set(U,V)|multiple(U,V)))),inference(fof_nnf,[status(thm)],[ax21])).
% 0.53/0.74 fof(c144,plain,(![X63]:(![X64]:(~set(X63,X64)|multiple(X63,X64)))),inference(variable_rename,[status(thm)],[c143])).
% 0.53/0.74 cnf(c145,plain,~set(X164,X165)|multiple(X164,X165),inference(split_conjunct,[status(thm)],[c144])).
% 0.53/0.74 cnf(c210,plain,multiple(skolem0001,skolem0003),inference(resolution,[status(thm)],[c145, c209])).
% 0.53/0.74 cnf(c23,axiom,X347!=X345|X346!=X348|~multiple(X347,X346)|multiple(X345,X348),theory(equality)).
% 0.53/0.74 cnf(c264,plain,skolem0001!=X350|skolem0003!=X351|multiple(X350,X351),inference(resolution,[status(thm)],[c23, c210])).
% 0.53/0.74 cnf(c266,plain,skolem0001!=X352|multiple(X352,skolem0003),inference(resolution,[status(thm)],[c264, reflexivity])).
% 0.53/0.74 cnf(c22,axiom,X341!=X339|X340!=X342|~set(X341,X340)|set(X339,X342),theory(equality)).
% 0.53/0.74 cnf(c262,plain,skolem0001!=X344|skolem0003!=X343|set(X344,X343),inference(resolution,[status(thm)],[c22, c209])).
% 0.53/0.74 cnf(c263,plain,skolem0001!=X349|set(X349,skolem0003),inference(resolution,[status(thm)],[c262, reflexivity])).
% 0.53/0.74 cnf(c21,axiom,X334!=X332|X333!=X335|~group(X334,X333)|group(X332,X335),theory(equality)).
% 0.53/0.74 cnf(c259,plain,skolem0001!=X336|skolem0003!=X337|group(X336,X337),inference(resolution,[status(thm)],[c21, c59])).
% 0.53/0.74 cnf(c260,plain,skolem0001!=X338|group(X338,skolem0003),inference(resolution,[status(thm)],[c259, reflexivity])).
% 0.53/0.74 cnf(c20,axiom,X330!=X328|X329!=X331|~three(X330,X329)|three(X328,X331),theory(equality)).
% 0.53/0.74 cnf(c19,axiom,X326!=X324|X325!=X327|~hamburger(X326,X325)|hamburger(X324,X327),theory(equality)).
% 0.53/0.74 cnf(c14,axiom,X284!=X282|X283!=X285|~entity(X284,X283)|entity(X282,X285),theory(equality)).
% 0.53/0.74 cnf(c243,plain,skolem0001!=X322|skolem0002!=X321|entity(X322,X321),inference(resolution,[status(thm)],[c14, c222])).
% 0.53/0.74 cnf(c257,plain,skolem0001!=X323|entity(X323,skolem0002),inference(resolution,[status(thm)],[c243, reflexivity])).
% 0.53/0.74 cnf(c18,axiom,X319!=X317|X318!=X320|~burger(X319,X318)|burger(X317,X320),theory(equality)).
% 0.53/0.74 fof(ax13,axiom,(![U]:(![V]:(object(U,V)=>nonliving(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax13)).
% 0.53/0.74 fof(c167,plain,(![U]:(![V]:(~object(U,V)|nonliving(U,V)))),inference(fof_nnf,[status(thm)],[ax13])).
% 0.53/0.74 fof(c168,plain,(![X79]:(![X80]:(~object(X79,X80)|nonliving(X79,X80)))),inference(variable_rename,[status(thm)],[c167])).
% 0.53/0.74 cnf(c169,plain,~object(X188,X189)|nonliving(X188,X189),inference(split_conjunct,[status(thm)],[c168])).
% 0.53/0.74 cnf(c223,plain,nonliving(skolem0001,skolem0002),inference(resolution,[status(thm)],[c219, c169])).
% 0.53/0.74 cnf(c13,axiom,X275!=X273|X274!=X276|~nonliving(X275,X274)|nonliving(X273,X276),theory(equality)).
% 0.53/0.74 cnf(c239,plain,skolem0001!=X314|skolem0002!=X315|nonliving(X314,X315),inference(resolution,[status(thm)],[c13, c223])).
% 0.53/0.74 cnf(c255,plain,skolem0001!=X316|nonliving(X316,skolem0002),inference(resolution,[status(thm)],[c239, reflexivity])).
% 0.53/0.74 fof(ax12,axiom,(![U]:(![V]:(object(U,V)=>impartial(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax12)).
% 0.53/0.74 fof(c170,plain,(![U]:(![V]:(~object(U,V)|impartial(U,V)))),inference(fof_nnf,[status(thm)],[ax12])).
% 0.53/0.74 fof(c171,plain,(![X81]:(![X82]:(~object(X81,X82)|impartial(X81,X82)))),inference(variable_rename,[status(thm)],[c170])).
% 0.53/0.74 cnf(c172,plain,~object(X190,X191)|impartial(X190,X191),inference(split_conjunct,[status(thm)],[c171])).
% 0.53/0.74 cnf(c220,plain,impartial(skolem0001,skolem0002),inference(resolution,[status(thm)],[c219, c172])).
% 0.53/0.74 cnf(c12,axiom,X265!=X263|X264!=X266|~impartial(X265,X264)|impartial(X263,X266),theory(equality)).
% 0.53/0.74 cnf(c234,plain,skolem0001!=X308|skolem0002!=X307|impartial(X308,X307),inference(resolution,[status(thm)],[c12, c220])).
% 0.53/0.74 cnf(c253,plain,skolem0001!=X313|impartial(X313,skolem0002),inference(resolution,[status(thm)],[c234, reflexivity])).
% 0.53/0.74 cnf(c17,axiom,X311!=X309|X310!=X312|~meat(X311,X310)|meat(X309,X312),theory(equality)).
% 0.53/0.74 cnf(c9,axiom,X232!=X230|X231!=X233|~thing(X232,X231)|thing(X230,X233),theory(equality)).
% 0.53/0.74 cnf(c232,plain,skolem0001!=X304|skolem0002!=X305|thing(X304,X305),inference(resolution,[status(thm)],[c9, c226])).
% 0.53/0.74 cnf(c251,plain,skolem0001!=X306|thing(X306,skolem0002),inference(resolution,[status(thm)],[c232, reflexivity])).
% 0.53/0.74 cnf(c16,axiom,X302!=X300|X301!=X303|~food(X302,X301)|food(X300,X303),theory(equality)).
% 0.53/0.74 cnf(c8,axiom,X228!=X226|X227!=X229|~specific(X228,X227)|specific(X226,X229),theory(equality)).
% 0.53/0.74 fof(ax29,axiom,(![U]:(![V]:(entity(U,V)=>specific(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax29)).
% 0.53/0.74 fof(c119,plain,(![U]:(![V]:(~entity(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax29])).
% 0.53/0.74 fof(c120,plain,(![X47]:(![X48]:(~entity(X47,X48)|specific(X47,X48)))),inference(variable_rename,[status(thm)],[c119])).
% 0.53/0.74 cnf(c121,plain,~entity(X141,X140)|specific(X141,X140),inference(split_conjunct,[status(thm)],[c120])).
% 0.53/0.74 cnf(c228,plain,specific(skolem0001,skolem0002),inference(resolution,[status(thm)],[c222, c121])).
% 0.53/0.74 cnf(c231,plain,skolem0001!=X297|skolem0002!=X298|specific(X297,X298),inference(resolution,[status(thm)],[c228, c8])).
% 0.53/0.74 cnf(c249,plain,skolem0001!=X299|specific(X299,skolem0002),inference(resolution,[status(thm)],[c231, reflexivity])).
% 0.53/0.74 cnf(c6,axiom,X212!=X210|X211!=X213|~unisex(X212,X211)|unisex(X210,X213),theory(equality)).
% 0.53/0.74 fof(ax11,axiom,(![U]:(![V]:(object(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax11)).
% 0.53/0.74 fof(c173,plain,(![U]:(![V]:(~object(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax11])).
% 0.53/0.74 fof(c174,plain,(![X83]:(![X84]:(~object(X83,X84)|unisex(X83,X84)))),inference(variable_rename,[status(thm)],[c173])).
% 0.53/0.74 cnf(c175,plain,~object(X193,X192)|unisex(X193,X192),inference(split_conjunct,[status(thm)],[c174])).
% 0.53/0.74 cnf(c221,plain,unisex(skolem0001,skolem0002),inference(resolution,[status(thm)],[c219, c175])).
% 0.53/0.74 cnf(c225,plain,skolem0001!=X295|skolem0002!=X294|unisex(X295,X294),inference(resolution,[status(thm)],[c221, c6])).
% 0.53/0.74 cnf(c247,plain,skolem0001!=X296|unisex(X296,skolem0002),inference(resolution,[status(thm)],[c225, reflexivity])).
% 0.53/0.74 cnf(c15,axiom,X292!=X290|X291!=X293|~substance_matter(X292,X291)|substance_matter(X290,X293),theory(equality)).
% 0.53/0.74 cnf(c1,axiom,X148!=X146|X147!=X149|~object(X148,X147)|object(X146,X149),theory(equality)).
% 0.53/0.74 cnf(c224,plain,skolem0001!=X288|skolem0002!=X287|object(X288,X287),inference(resolution,[status(thm)],[c219, c1])).
% 0.53/0.75 cnf(c245,plain,skolem0001!=X289|object(X289,skolem0002),inference(resolution,[status(thm)],[c224, reflexivity])).
% 0.53/0.75 cnf(c0,axiom,X134!=X132|X133!=X135|~artifact(X134,X133)|artifact(X132,X135),theory(equality)).
% 0.53/0.75 cnf(c218,plain,skolem0001!=X281|skolem0002!=X280|artifact(X281,X280),inference(resolution,[status(thm)],[c217, c0])).
% 0.53/0.75 cnf(c242,plain,skolem0001!=X286|artifact(X286,skolem0002),inference(resolution,[status(thm)],[c218, reflexivity])).
% 0.53/0.75 cnf(c2,axiom,X162!=X160|X161!=X163|~instrumentality(X162,X161)|instrumentality(X160,X163),theory(equality)).
% 0.53/0.75 cnf(c216,plain,skolem0001!=X277|skolem0002!=X278|instrumentality(X277,X278),inference(resolution,[status(thm)],[c215, c2])).
% 0.53/0.75 cnf(c240,plain,skolem0001!=X279|instrumentality(X279,skolem0002),inference(resolution,[status(thm)],[c216, reflexivity])).
% 0.53/0.75 cnf(c3,axiom,X170!=X168|X169!=X171|~furniture(X170,X169)|furniture(X168,X171),theory(equality)).
% 0.53/0.75 cnf(c214,plain,skolem0001!=X271|skolem0002!=X270|furniture(X271,X270),inference(resolution,[status(thm)],[c213, c3])).
% 0.53/0.75 cnf(c237,plain,skolem0001!=X272|furniture(X272,skolem0002),inference(resolution,[status(thm)],[c214, reflexivity])).
% 0.53/0.75 cnf(c4,axiom,X184!=X182|X183!=X185|~table(X184,X183)|table(X182,X185),theory(equality)).
% 0.53/0.75 cnf(c212,plain,skolem0001!=X268|skolem0002!=X267|table(X268,X267),inference(resolution,[status(thm)],[c4, c48])).
% 0.53/0.75 cnf(c235,plain,skolem0001!=X269|table(X269,skolem0002),inference(resolution,[status(thm)],[c212, reflexivity])).
% 0.53/0.75 cnf(c75,plain,~three(X261,X262)|skolem0008(X261,X262)!=skolem0006(X261,X262),inference(split_conjunct,[status(thm)],[c69])).
% 0.53/0.75 cnf(c74,plain,~three(X259,X260)|skolem0008(X259,X260)!=skolem0007(X259,X260),inference(split_conjunct,[status(thm)],[c69])).
% 0.53/0.75 cnf(c72,plain,~three(X257,X258)|skolem0007(X257,X258)!=skolem0006(X257,X258),inference(split_conjunct,[status(thm)],[c69])).
% 0.53/0.75 cnf(c56,negated_conjecture,~member(skolem0001,X256,skolem0003)|group(skolem0001,skolem0004(X256)),inference(split_conjunct,[status(thm)],[c46])).
% 0.53/0.75 cnf(c55,negated_conjecture,~member(skolem0001,X255,skolem0003)|three(skolem0001,skolem0004(X255)),inference(split_conjunct,[status(thm)],[c46])).
% 0.53/0.75 cnf(c11,axiom,X253!=X251|X252!=X254|~sit(X253,X252)|sit(X251,X254),theory(equality)).
% 0.53/0.75 cnf(c73,plain,~three(X249,X250)|member(X249,skolem0008(X249,X250),X250),inference(split_conjunct,[status(thm)],[c69])).
% 0.53/0.75 cnf(c71,plain,~three(X247,X248)|member(X247,skolem0007(X247,X248),X248),inference(split_conjunct,[status(thm)],[c69])).
% 0.53/0.75 cnf(c70,plain,~three(X245,X246)|member(X245,skolem0006(X245,X246),X246),inference(split_conjunct,[status(thm)],[c69])).
% 0.53/0.75 cnf(c60,negated_conjecture,~member(skolem0001,X244,skolem0003)|hamburger(skolem0001,X244),inference(split_conjunct,[status(thm)],[c46])).
% 0.53/0.75 cnf(c10,axiom,X241!=X239|X240!=X242|~event(X241,X240)|event(X239,X242),theory(equality)).
% 0.53/0.75 cnf(c35,axiom,X238!=X237|~actual_world(X238)|actual_world(X237),theory(equality)).
% 0.53/0.75 fof(ax36,axiom,(![U]:(![V]:(animate(U,V)=>(~nonliving(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax36)).
% 0.53/0.75 fof(c97,plain,(![U]:(![V]:(animate(U,V)=>~nonliving(U,V)))),inference(fof_simplification,[status(thm)],[ax36])).
% 0.53/0.75 fof(c98,plain,(![U]:(![V]:(~animate(U,V)|~nonliving(U,V)))),inference(fof_nnf,[status(thm)],[c97])).
% 0.53/0.75 fof(c99,plain,(![X33]:(![X34]:(~animate(X33,X34)|~nonliving(X33,X34)))),inference(variable_rename,[status(thm)],[c98])).
% 0.53/0.75 cnf(c100,plain,~animate(X123,X122)|~nonliving(X123,X122),inference(split_conjunct,[status(thm)],[c99])).
% 0.53/0.75 cnf(c229,plain,~animate(skolem0001,skolem0002),inference(resolution,[status(thm)],[c223, c100])).
% 0.53/0.75 cnf(c7,axiom,X222!=X220|X221!=X223|~nonexistent(X222,X221)|nonexistent(X220,X223),theory(equality)).
% 0.53/0.75 fof(ax5,axiom,(![U]:(![V]:(eventuality(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax5)).
% 0.53/0.75 fof(c191,plain,(![U]:(![V]:(~eventuality(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax5])).
% 0.53/0.75 fof(c192,plain,(![X95]:(![X96]:(~eventuality(X95,X96)|unisex(X95,X96)))),inference(variable_rename,[status(thm)],[c191])).
% 0.53/0.75 cnf(c193,plain,~eventuality(X209,X208)|unisex(X209,X208),inference(split_conjunct,[status(thm)],[c192])).
% 0.53/0.75 fof(ax6,axiom,(![U]:(![V]:(eventuality(U,V)=>nonexistent(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax6)).
% 0.53/0.75 fof(c188,plain,(![U]:(![V]:(~eventuality(U,V)|nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[ax6])).
% 0.53/0.75 fof(c189,plain,(![X93]:(![X94]:(~eventuality(X93,X94)|nonexistent(X93,X94)))),inference(variable_rename,[status(thm)],[c188])).
% 0.53/0.75 cnf(c190,plain,~eventuality(X207,X206)|nonexistent(X207,X206),inference(split_conjunct,[status(thm)],[c189])).
% 0.53/0.75 fof(ax7,axiom,(![U]:(![V]:(eventuality(U,V)=>specific(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax7)).
% 0.53/0.75 fof(c185,plain,(![U]:(![V]:(~eventuality(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax7])).
% 0.53/0.75 fof(c186,plain,(![X91]:(![X92]:(~eventuality(X91,X92)|specific(X91,X92)))),inference(variable_rename,[status(thm)],[c185])).
% 0.53/0.75 cnf(c187,plain,~eventuality(X205,X204)|specific(X205,X204),inference(split_conjunct,[status(thm)],[c186])).
% 0.53/0.75 fof(ax8,axiom,(![U]:(![V]:(eventuality(U,V)=>thing(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax8)).
% 0.53/0.75 fof(c182,plain,(![U]:(![V]:(~eventuality(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax8])).
% 0.53/0.75 fof(c183,plain,(![X89]:(![X90]:(~eventuality(X89,X90)|thing(X89,X90)))),inference(variable_rename,[status(thm)],[c182])).
% 0.53/0.75 cnf(c184,plain,~eventuality(X202,X203)|thing(X202,X203),inference(split_conjunct,[status(thm)],[c183])).
% 0.53/0.75 fof(ax9,axiom,(![U]:(![V]:(event(U,V)=>eventuality(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax9)).
% 0.53/0.75 fof(c179,plain,(![U]:(![V]:(~event(U,V)|eventuality(U,V)))),inference(fof_nnf,[status(thm)],[ax9])).
% 0.53/0.75 fof(c180,plain,(![X87]:(![X88]:(~event(X87,X88)|eventuality(X87,X88)))),inference(variable_rename,[status(thm)],[c179])).
% 0.53/0.75 cnf(c181,plain,~event(X201,X200)|eventuality(X201,X200),inference(split_conjunct,[status(thm)],[c180])).
% 0.53/0.75 cnf(c5,axiom,X198!=X196|X197!=X199|~eventuality(X198,X197)|eventuality(X196,X199),theory(equality)).
% 0.53/0.75 fof(ax10,axiom,(![U]:(![V]:(sit(U,V)=>event(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax10)).
% 0.53/0.75 fof(c176,plain,(![U]:(![V]:(~sit(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax10])).
% 0.53/0.75 fof(c177,plain,(![X85]:(![X86]:(~sit(X85,X86)|event(X85,X86)))),inference(variable_rename,[status(thm)],[c176])).
% 0.53/0.75 cnf(c178,plain,~sit(X195,X194)|event(X195,X194),inference(split_conjunct,[status(thm)],[c177])).
% 0.53/0.75 fof(ax15,axiom,(![U]:(![V]:(substance_matter(U,V)=>object(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax15)).
% 0.53/0.75 fof(c161,plain,(![U]:(![V]:(~substance_matter(U,V)|object(U,V)))),inference(fof_nnf,[status(thm)],[ax15])).
% 0.53/0.75 fof(c162,plain,(![X75]:(![X76]:(~substance_matter(X75,X76)|object(X75,X76)))),inference(variable_rename,[status(thm)],[c161])).
% 0.53/0.75 cnf(c163,plain,~substance_matter(X181,X180)|object(X181,X180),inference(split_conjunct,[status(thm)],[c162])).
% 0.53/0.75 fof(ax16,axiom,(![U]:(![V]:(food(U,V)=>substance_matter(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax16)).
% 0.53/0.75 fof(c158,plain,(![U]:(![V]:(~food(U,V)|substance_matter(U,V)))),inference(fof_nnf,[status(thm)],[ax16])).
% 0.53/0.75 fof(c159,plain,(![X73]:(![X74]:(~food(X73,X74)|substance_matter(X73,X74)))),inference(variable_rename,[status(thm)],[c158])).
% 0.53/0.75 cnf(c160,plain,~food(X179,X178)|substance_matter(X179,X178),inference(split_conjunct,[status(thm)],[c159])).
% 0.53/0.75 fof(ax17,axiom,(![U]:(![V]:(meat(U,V)=>food(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax17)).
% 0.53/0.75 fof(c155,plain,(![U]:(![V]:(~meat(U,V)|food(U,V)))),inference(fof_nnf,[status(thm)],[ax17])).
% 0.53/0.75 fof(c156,plain,(![X71]:(![X72]:(~meat(X71,X72)|food(X71,X72)))),inference(variable_rename,[status(thm)],[c155])).
% 0.53/0.75 cnf(c157,plain,~meat(X176,X177)|food(X176,X177),inference(split_conjunct,[status(thm)],[c156])).
% 0.53/0.75 fof(ax18,axiom,(![U]:(![V]:(burger(U,V)=>meat(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax18)).
% 0.53/0.75 fof(c152,plain,(![U]:(![V]:(~burger(U,V)|meat(U,V)))),inference(fof_nnf,[status(thm)],[ax18])).
% 0.53/0.75 fof(c153,plain,(![X69]:(![X70]:(~burger(X69,X70)|meat(X69,X70)))),inference(variable_rename,[status(thm)],[c152])).
% 0.53/0.75 cnf(c154,plain,~burger(X175,X174)|meat(X175,X174),inference(split_conjunct,[status(thm)],[c153])).
% 0.53/0.75 fof(ax19,axiom,(![U]:(![V]:(hamburger(U,V)=>burger(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax19)).
% 0.53/0.75 fof(c149,plain,(![U]:(![V]:(~hamburger(U,V)|burger(U,V)))),inference(fof_nnf,[status(thm)],[ax19])).
% 0.53/0.75 fof(c150,plain,(![X67]:(![X68]:(~hamburger(X67,X68)|burger(X67,X68)))),inference(variable_rename,[status(thm)],[c149])).
% 0.53/0.75 cnf(c151,plain,~hamburger(X173,X172)|burger(X173,X172),inference(split_conjunct,[status(thm)],[c150])).
% 0.53/0.75 fof(ax20,axiom,(![U]:(![V]:(three(U,V)=>group(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax20)).
% 0.53/0.75 fof(c146,plain,(![U]:(![V]:(~three(U,V)|group(U,V)))),inference(fof_nnf,[status(thm)],[ax20])).
% 0.53/0.75 fof(c147,plain,(![X65]:(![X66]:(~three(X65,X66)|group(X65,X66)))),inference(variable_rename,[status(thm)],[c146])).
% 0.53/0.75 cnf(c148,plain,~three(X166,X167)|group(X166,X167),inference(split_conjunct,[status(thm)],[c147])).
% 0.53/0.75 fof(ax39,axiom,(![U]:(![V]:(singleton(U,V)=>(~multiple(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax39)).
% 0.53/0.75 fof(c85,plain,(![U]:(![V]:(singleton(U,V)=>~multiple(U,V)))),inference(fof_simplification,[status(thm)],[ax39])).
% 0.53/0.75 fof(c86,plain,(![U]:(![V]:(~singleton(U,V)|~multiple(U,V)))),inference(fof_nnf,[status(thm)],[c85])).
% 0.53/0.75 fof(c87,plain,(![X27]:(![X28]:(~singleton(X27,X28)|~multiple(X27,X28)))),inference(variable_rename,[status(thm)],[c86])).
% 0.53/0.75 cnf(c88,plain,~singleton(X114,X113)|~multiple(X114,X113),inference(split_conjunct,[status(thm)],[c87])).
% 0.53/0.75 cnf(c211,plain,~singleton(skolem0001,skolem0003),inference(resolution,[status(thm)],[c210, c88])).
% 0.53/0.75 fof(ax23,axiom,(![U]:(![V]:(man(U,V)=>male(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax23)).
% 0.53/0.75 fof(c137,plain,(![U]:(![V]:(~man(U,V)|male(U,V)))),inference(fof_nnf,[status(thm)],[ax23])).
% 0.53/0.75 fof(c138,plain,(![X59]:(![X60]:(~man(X59,X60)|male(X59,X60)))),inference(variable_rename,[status(thm)],[c137])).
% 0.53/0.75 cnf(c139,plain,~man(X157,X156)|male(X157,X156),inference(split_conjunct,[status(thm)],[c138])).
% 0.53/0.75 fof(ax24,axiom,(![U]:(![V]:(human_person(U,V)=>animate(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax24)).
% 0.53/0.75 fof(c134,plain,(![U]:(![V]:(~human_person(U,V)|animate(U,V)))),inference(fof_nnf,[status(thm)],[ax24])).
% 0.53/0.75 fof(c135,plain,(![X57]:(![X58]:(~human_person(X57,X58)|animate(X57,X58)))),inference(variable_rename,[status(thm)],[c134])).
% 0.53/0.75 cnf(c136,plain,~human_person(X154,X155)|animate(X154,X155),inference(split_conjunct,[status(thm)],[c135])).
% 0.53/0.75 fof(ax25,axiom,(![U]:(![V]:(human_person(U,V)=>human(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax25)).
% 0.53/0.75 fof(c131,plain,(![U]:(![V]:(~human_person(U,V)|human(U,V)))),inference(fof_nnf,[status(thm)],[ax25])).
% 0.53/0.75 fof(c132,plain,(![X55]:(![X56]:(~human_person(X55,X56)|human(X55,X56)))),inference(variable_rename,[status(thm)],[c131])).
% 0.53/0.75 cnf(c133,plain,~human_person(X152,X153)|human(X152,X153),inference(split_conjunct,[status(thm)],[c132])).
% 0.53/0.75 fof(ax26,axiom,(![U]:(![V]:(organism(U,V)=>living(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax26)).
% 0.53/0.75 fof(c128,plain,(![U]:(![V]:(~organism(U,V)|living(U,V)))),inference(fof_nnf,[status(thm)],[ax26])).
% 0.53/0.75 fof(c129,plain,(![X53]:(![X54]:(~organism(X53,X54)|living(X53,X54)))),inference(variable_rename,[status(thm)],[c128])).
% 0.53/0.75 cnf(c130,plain,~organism(X151,X150)|living(X151,X150),inference(split_conjunct,[status(thm)],[c129])).
% 0.53/0.75 fof(ax27,axiom,(![U]:(![V]:(organism(U,V)=>impartial(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax27)).
% 0.53/0.75 fof(c125,plain,(![U]:(![V]:(~organism(U,V)|impartial(U,V)))),inference(fof_nnf,[status(thm)],[ax27])).
% 0.53/0.75 fof(c126,plain,(![X51]:(![X52]:(~organism(X51,X52)|impartial(X51,X52)))),inference(variable_rename,[status(thm)],[c125])).
% 0.53/0.75 cnf(c127,plain,~organism(X144,X145)|impartial(X144,X145),inference(split_conjunct,[status(thm)],[c126])).
% 0.53/0.75 fof(ax32,axiom,(![U]:(![V]:(organism(U,V)=>entity(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax32)).
% 0.53/0.75 fof(c110,plain,(![U]:(![V]:(~organism(U,V)|entity(U,V)))),inference(fof_nnf,[status(thm)],[ax32])).
% 0.53/0.75 fof(c111,plain,(![X41]:(![X42]:(~organism(X41,X42)|entity(X41,X42)))),inference(variable_rename,[status(thm)],[c110])).
% 0.53/0.75 cnf(c112,plain,~organism(X130,X131)|entity(X130,X131),inference(split_conjunct,[status(thm)],[c111])).
% 0.53/0.75 fof(ax33,axiom,(![U]:(![V]:(human_person(U,V)=>organism(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax33)).
% 0.53/0.75 fof(c107,plain,(![U]:(![V]:(~human_person(U,V)|organism(U,V)))),inference(fof_nnf,[status(thm)],[ax33])).
% 0.53/0.75 fof(c108,plain,(![X39]:(![X40]:(~human_person(X39,X40)|organism(X39,X40)))),inference(variable_rename,[status(thm)],[c107])).
% 0.53/0.75 cnf(c109,plain,~human_person(X129,X128)|organism(X129,X128),inference(split_conjunct,[status(thm)],[c108])).
% 0.53/0.75 fof(ax34,axiom,(![U]:(![V]:(man(U,V)=>human_person(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax34)).
% 0.53/0.75 fof(c104,plain,(![U]:(![V]:(~man(U,V)|human_person(U,V)))),inference(fof_nnf,[status(thm)],[ax34])).
% 0.53/0.75 fof(c105,plain,(![X37]:(![X38]:(~man(X37,X38)|human_person(X37,X38)))),inference(variable_rename,[status(thm)],[c104])).
% 0.53/0.75 cnf(c106,plain,~man(X126,X127)|human_person(X126,X127),inference(split_conjunct,[status(thm)],[c105])).
% 0.53/0.75 fof(ax35,axiom,(![U]:(![V]:(guy(U,V)=>man(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax35)).
% 0.53/0.75 fof(c101,plain,(![U]:(![V]:(~guy(U,V)|man(U,V)))),inference(fof_nnf,[status(thm)],[ax35])).
% 0.53/0.75 fof(c102,plain,(![X35]:(![X36]:(~guy(X35,X36)|man(X35,X36)))),inference(variable_rename,[status(thm)],[c101])).
% 0.53/0.75 cnf(c103,plain,~guy(X125,X124)|man(X125,X124),inference(split_conjunct,[status(thm)],[c102])).
% 0.53/0.75 cnf(transitivity,axiom,X119!=X120|X120!=X121|X119=X121,theory(equality)).
% 0.53/0.75 fof(ax37,axiom,(![U]:(![V]:(existent(U,V)=>(~nonexistent(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax37)).
% 0.53/0.75 fof(c93,plain,(![U]:(![V]:(existent(U,V)=>~nonexistent(U,V)))),inference(fof_simplification,[status(thm)],[ax37])).
% 0.53/0.75 fof(c94,plain,(![U]:(![V]:(~existent(U,V)|~nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[c93])).
% 0.53/0.75 fof(c95,plain,(![X31]:(![X32]:(~existent(X31,X32)|~nonexistent(X31,X32)))),inference(variable_rename,[status(thm)],[c94])).
% 0.53/0.75 cnf(c96,plain,~existent(X118,X117)|~nonexistent(X118,X117),inference(split_conjunct,[status(thm)],[c95])).
% 0.53/0.75 fof(ax38,axiom,(![U]:(![V]:(nonliving(U,V)=>(~living(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax38)).
% 0.53/0.75 fof(c89,plain,(![U]:(![V]:(nonliving(U,V)=>~living(U,V)))),inference(fof_simplification,[status(thm)],[ax38])).
% 0.53/0.75 fof(c90,plain,(![U]:(![V]:(~nonliving(U,V)|~living(U,V)))),inference(fof_nnf,[status(thm)],[c89])).
% 0.53/0.75 fof(c91,plain,(![X29]:(![X30]:(~nonliving(X29,X30)|~living(X29,X30)))),inference(variable_rename,[status(thm)],[c90])).
% 0.53/0.75 cnf(c92,plain,~nonliving(X116,X115)|~living(X116,X115),inference(split_conjunct,[status(thm)],[c91])).
% 0.53/0.75 fof(ax40,axiom,(![U]:(![V]:(unisex(U,V)=>(~male(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax40)).
% 0.53/0.75 fof(c81,plain,(![U]:(![V]:(unisex(U,V)=>~male(U,V)))),inference(fof_simplification,[status(thm)],[ax40])).
% 0.53/0.75 fof(c82,plain,(![U]:(![V]:(~unisex(U,V)|~male(U,V)))),inference(fof_nnf,[status(thm)],[c81])).
% 0.53/0.75 fof(c83,plain,(![X25]:(![X26]:(~unisex(X25,X26)|~male(X25,X26)))),inference(variable_rename,[status(thm)],[c82])).
% 0.53/0.75 cnf(c84,plain,~unisex(X111,X112)|~male(X111,X112),inference(split_conjunct,[status(thm)],[c83])).
% 0.53/0.75 cnf(symmetry,axiom,X108!=X109|X109=X108,theory(equality)).
% 0.53/0.75 fof(ax42,axiom,(![U]:(~(?[V]:member(U,V,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax42)).
% 0.53/0.75 fof(c61,plain,(![U]:(![V]:~member(U,V,V))),inference(fof_nnf,[status(thm)],[ax42])).
% 0.53/0.75 fof(c62,plain,(![X11]:(![X12]:~member(X11,X12,X12))),inference(variable_rename,[status(thm)],[c61])).
% 0.53/0.75 cnf(c63,plain,~member(X107,X106,X106),inference(split_conjunct,[status(thm)],[c62])).
% 0.53/0.75 cnf(c47,negated_conjecture,actual_world(skolem0001),inference(split_conjunct,[status(thm)],[c46])).
% 0.53/0.75 % SZS output end Saturation
% 0.53/0.75
% 0.53/0.75 % Initial clauses : 110
% 0.53/0.75 % Processed clauses : 158
% 0.53/0.75 % Factors computed : 3
% 0.53/0.75 % Resolvents computed: 67
% 0.53/0.75 % Tautologies deleted: 3
% 0.53/0.75 % Forward subsumed : 19
% 0.53/0.75 % Backward subsumed : 0
% 0.53/0.75 % -------- CPU Time ---------
% 0.53/0.75 % User time : 0.363 s
% 0.53/0.75 % System time : 0.015 s
% 0.53/0.75 % Total time : 0.378 s
%------------------------------------------------------------------------------