%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET809+4 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n016.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:40:07 EDT 2024
% Result : Theorem 3.86s 4.06s
% Output : Refutation 3.86s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SET809+4 : TPTP v8.1.2. Released v3.2.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n016.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.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 19:16:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 3.86/4.06 % Version: 1.5
% 3.86/4.06 % SZS status Theorem
% 3.86/4.06 % SZS output start CNFRefutation
% 3.86/4.06 fof(strict_well_order,axiom,(![R]:(![E]:(strict_well_order(R,E)<=>(strict_order(R,E)&(![A]:((subset(A,E)&(?[X]:member(X,A)))=>(?[Y]:least(Y,R,A)))))))),file('/export/starexec/sandbox/benchmark/Axioms/SET006+4.ax', strict_well_order)).
% 3.86/4.06 fof(c92,plain,(![R]:(![E]:((~strict_well_order(R,E)|(strict_order(R,E)&(![A]:((~subset(A,E)|(![X]:~member(X,A)))|(?[Y]:least(Y,R,A))))))&((~strict_order(R,E)|(?[A]:((subset(A,E)&(?[X]:member(X,A)))&(![Y]:~least(Y,R,A)))))|strict_well_order(R,E))))),inference(fof_nnf,[status(thm)],[strict_well_order])).
% 3.86/4.06 fof(c93,plain,((![R]:(![E]:(~strict_well_order(R,E)|(strict_order(R,E)&(![A]:((~subset(A,E)|(![X]:~member(X,A)))|(?[Y]:least(Y,R,A))))))))&(![R]:(![E]:((~strict_order(R,E)|(?[A]:((subset(A,E)&(?[X]:member(X,A)))&(![Y]:~least(Y,R,A)))))|strict_well_order(R,E))))),inference(shift_quantors,[status(thm)],[c92])).
% 3.86/4.06 fof(c94,plain,((![X43]:(![X44]:(~strict_well_order(X43,X44)|(strict_order(X43,X44)&(![X45]:((~subset(X45,X44)|(![X46]:~member(X46,X45)))|(?[X47]:least(X47,X43,X45))))))))&(![X48]:(![X49]:((~strict_order(X48,X49)|(?[X50]:((subset(X50,X49)&(?[X51]:member(X51,X50)))&(![X52]:~least(X52,X48,X50)))))|strict_well_order(X48,X49))))),inference(variable_rename,[status(thm)],[c93])).
% 3.86/4.06 fof(c96,plain,(![X43]:(![X44]:(![X45]:(![X46]:(![X48]:(![X49]:(![X52]:((~strict_well_order(X43,X44)|(strict_order(X43,X44)&((~subset(X45,X44)|~member(X46,X45))|least(skolem0008(X43,X44,X45),X43,X45))))&((~strict_order(X48,X49)|((subset(skolem0009(X48,X49),X49)&member(skolem0010(X48,X49),skolem0009(X48,X49)))&~least(X52,X48,skolem0009(X48,X49))))|strict_well_order(X48,X49)))))))))),inference(shift_quantors,[status(thm)],[fof(c95,plain,((![X43]:(![X44]:(~strict_well_order(X43,X44)|(strict_order(X43,X44)&(![X45]:((~subset(X45,X44)|(![X46]:~member(X46,X45)))|least(skolem0008(X43,X44,X45),X43,X45)))))))&(![X48]:(![X49]:((~strict_order(X48,X49)|((subset(skolem0009(X48,X49),X49)&member(skolem0010(X48,X49),skolem0009(X48,X49)))&(![X52]:~least(X52,X48,skolem0009(X48,X49)))))|strict_well_order(X48,X49))))),inference(skolemize,[status(esa)],[c94])).])).
% 3.86/4.06 fof(c97,plain,(![X43]:(![X44]:(![X45]:(![X46]:(![X48]:(![X49]:(![X52]:(((~strict_well_order(X43,X44)|strict_order(X43,X44))&(~strict_well_order(X43,X44)|((~subset(X45,X44)|~member(X46,X45))|least(skolem0008(X43,X44,X45),X43,X45))))&((((~strict_order(X48,X49)|subset(skolem0009(X48,X49),X49))|strict_well_order(X48,X49))&((~strict_order(X48,X49)|member(skolem0010(X48,X49),skolem0009(X48,X49)))|strict_well_order(X48,X49)))&((~strict_order(X48,X49)|~least(X52,X48,skolem0009(X48,X49)))|strict_well_order(X48,X49))))))))))),inference(distribute,[status(thm)],[c96])).
% 3.86/4.06 cnf(c98,plain,~strict_well_order(X120,X121)|strict_order(X120,X121),inference(split_conjunct,[status(thm)],[c97])).
% 3.86/4.06 fof(thV2,conjecture,(![A]:(member(A,on)=>(~member(A,A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', thV2)).
% 3.86/4.06 fof(c18,negated_conjecture,(~(![A]:(member(A,on)=>(~member(A,A))))),inference(assume_negation,[status(cth)],[thV2])).
% 3.86/4.06 fof(c19,negated_conjecture,(~(![A]:(member(A,on)=>~member(A,A)))),inference(fof_simplification,[status(thm)],[c18])).
% 3.86/4.06 fof(c20,negated_conjecture,(?[A]:(member(A,on)&member(A,A))),inference(fof_nnf,[status(thm)],[c19])).
% 3.86/4.06 fof(c21,negated_conjecture,(?[X2]:(member(X2,on)&member(X2,X2))),inference(variable_rename,[status(thm)],[c20])).
% 3.86/4.06 fof(c22,negated_conjecture,(member(skolem0001,on)&member(skolem0001,skolem0001)),inference(skolemize,[status(esa)],[c21])).
% 3.86/4.06 cnf(c23,negated_conjecture,member(skolem0001,on),inference(split_conjunct,[status(thm)],[c22])).
% 3.86/4.06 fof(ordinal_number,axiom,(![A]:(member(A,on)<=>((set(A)&strict_well_order(member_predicate,A))&(![X]:(member(X,A)=>subset(X,A)))))),file('/export/starexec/sandbox/benchmark/Axioms/SET006+4.ax', ordinal_number)).
% 3.86/4.06 fof(c103,plain,(![A]:((~member(A,on)|((set(A)&strict_well_order(member_predicate,A))&(![X]:(~member(X,A)|subset(X,A)))))&(((~set(A)|~strict_well_order(member_predicate,A))|(?[X]:(member(X,A)&~subset(X,A))))|member(A,on)))),inference(fof_nnf,[status(thm)],[ordinal_number])).
% 3.86/4.06 fof(c104,plain,((![A]:(~member(A,on)|((set(A)&strict_well_order(member_predicate,A))&(![X]:(~member(X,A)|subset(X,A))))))&(![A]:(((~set(A)|~strict_well_order(member_predicate,A))|(?[X]:(member(X,A)&~subset(X,A))))|member(A,on)))),inference(shift_quantors,[status(thm)],[c103])).
% 3.86/4.06 fof(c105,plain,((![X53]:(~member(X53,on)|((set(X53)&strict_well_order(member_predicate,X53))&(![X54]:(~member(X54,X53)|subset(X54,X53))))))&(![X55]:(((~set(X55)|~strict_well_order(member_predicate,X55))|(?[X56]:(member(X56,X55)&~subset(X56,X55))))|member(X55,on)))),inference(variable_rename,[status(thm)],[c104])).
% 3.86/4.06 fof(c107,plain,(![X53]:(![X54]:(![X55]:((~member(X53,on)|((set(X53)&strict_well_order(member_predicate,X53))&(~member(X54,X53)|subset(X54,X53))))&(((~set(X55)|~strict_well_order(member_predicate,X55))|(member(skolem0011(X55),X55)&~subset(skolem0011(X55),X55)))|member(X55,on)))))),inference(shift_quantors,[status(thm)],[fof(c106,plain,((![X53]:(~member(X53,on)|((set(X53)&strict_well_order(member_predicate,X53))&(![X54]:(~member(X54,X53)|subset(X54,X53))))))&(![X55]:(((~set(X55)|~strict_well_order(member_predicate,X55))|(member(skolem0011(X55),X55)&~subset(skolem0011(X55),X55)))|member(X55,on)))),inference(skolemize,[status(esa)],[c105])).])).
% 3.86/4.06 fof(c108,plain,(![X53]:(![X54]:(![X55]:((((~member(X53,on)|set(X53))&(~member(X53,on)|strict_well_order(member_predicate,X53)))&(~member(X53,on)|(~member(X54,X53)|subset(X54,X53))))&((((~set(X55)|~strict_well_order(member_predicate,X55))|member(skolem0011(X55),X55))|member(X55,on))&(((~set(X55)|~strict_well_order(member_predicate,X55))|~subset(skolem0011(X55),X55))|member(X55,on))))))),inference(distribute,[status(thm)],[c107])).
% 3.86/4.06 cnf(c110,plain,~member(X157,on)|strict_well_order(member_predicate,X157),inference(split_conjunct,[status(thm)],[c108])).
% 3.86/4.06 cnf(c215,plain,strict_well_order(member_predicate,skolem0001),inference(resolution,[status(thm)],[c110, c23])).
% 3.86/4.06 cnf(c216,plain,strict_order(member_predicate,skolem0001),inference(resolution,[status(thm)],[c215, c98])).
% 3.86/4.06 cnf(c24,negated_conjecture,member(skolem0001,skolem0001),inference(split_conjunct,[status(thm)],[c22])).
% 3.86/4.06 fof(rel_member,axiom,(![X]:(![Y]:(apply(member_predicate,X,Y)<=>member(X,Y)))),file('/export/starexec/sandbox/benchmark/Axioms/SET006+4.ax', rel_member)).
% 3.86/4.06 fof(c75,plain,(![X]:(![Y]:((~apply(member_predicate,X,Y)|member(X,Y))&(~member(X,Y)|apply(member_predicate,X,Y))))),inference(fof_nnf,[status(thm)],[rel_member])).
% 3.86/4.06 fof(c76,plain,((![X]:(![Y]:(~apply(member_predicate,X,Y)|member(X,Y))))&(![X]:(![Y]:(~member(X,Y)|apply(member_predicate,X,Y))))),inference(shift_quantors,[status(thm)],[c75])).
% 3.86/4.06 fof(c78,plain,(![X31]:(![X32]:(![X33]:(![X34]:((~apply(member_predicate,X31,X32)|member(X31,X32))&(~member(X33,X34)|apply(member_predicate,X33,X34))))))),inference(shift_quantors,[status(thm)],[fof(c77,plain,((![X31]:(![X32]:(~apply(member_predicate,X31,X32)|member(X31,X32))))&(![X33]:(![X34]:(~member(X33,X34)|apply(member_predicate,X33,X34))))),inference(variable_rename,[status(thm)],[c76])).])).
% 3.86/4.06 cnf(c80,plain,~member(X151,X152)|apply(member_predicate,X151,X152),inference(split_conjunct,[status(thm)],[c78])).
% 3.86/4.06 cnf(c209,plain,apply(member_predicate,skolem0001,skolem0001),inference(resolution,[status(thm)],[c80, c24])).
% 3.86/4.06 fof(strict_order,axiom,(![R]:(![E]:(strict_order(R,E)<=>((![X]:(![Y]:((member(X,E)&member(Y,E))=>(~(apply(R,X,Y)&apply(R,Y,X))))))&(![X]:(![Y]:(![Z]:(((member(X,E)&member(Y,E))&member(Z,E))=>((apply(R,X,Y)&apply(R,Y,Z))=>apply(R,X,Z)))))))))),file('/export/starexec/sandbox/benchmark/Axioms/SET006+4.ax', strict_order)).
% 3.86/4.06 fof(c43,plain,(![R]:(![E]:((~strict_order(R,E)|((![X]:(![Y]:((~member(X,E)|~member(Y,E))|(~apply(R,X,Y)|~apply(R,Y,X)))))&(![X]:(![Y]:(![Z]:(((~member(X,E)|~member(Y,E))|~member(Z,E))|((~apply(R,X,Y)|~apply(R,Y,Z))|apply(R,X,Z))))))))&(((?[X]:(?[Y]:((member(X,E)&member(Y,E))&(apply(R,X,Y)&apply(R,Y,X)))))|(?[X]:(?[Y]:(?[Z]:(((member(X,E)&member(Y,E))&member(Z,E))&((apply(R,X,Y)&apply(R,Y,Z))&~apply(R,X,Z)))))))|strict_order(R,E))))),inference(fof_nnf,[status(thm)],[strict_order])).
% 3.86/4.06 fof(c44,plain,((![R]:(![E]:(~strict_order(R,E)|((![X]:(![Y]:((~member(X,E)|~member(Y,E))|(~apply(R,X,Y)|~apply(R,Y,X)))))&(![X]:(![Y]:(![Z]:(((~member(X,E)|~member(Y,E))|~member(Z,E))|((~apply(R,X,Y)|~apply(R,Y,Z))|apply(R,X,Z))))))))))&(![R]:(![E]:(((?[X]:(?[Y]:((member(X,E)&member(Y,E))&(apply(R,X,Y)&apply(R,Y,X)))))|(?[X]:(?[Y]:(?[Z]:(((member(X,E)&member(Y,E))&member(Z,E))&((apply(R,X,Y)&apply(R,Y,Z))&~apply(R,X,Z)))))))|strict_order(R,E))))),inference(shift_quantors,[status(thm)],[c43])).
% 3.86/4.06 fof(c45,plain,((![X17]:(![X18]:(~strict_order(X17,X18)|((![X19]:(![X20]:((~member(X19,X18)|~member(X20,X18))|(~apply(X17,X19,X20)|~apply(X17,X20,X19)))))&(![X21]:(![X22]:(![X23]:(((~member(X21,X18)|~member(X22,X18))|~member(X23,X18))|((~apply(X17,X21,X22)|~apply(X17,X22,X23))|apply(X17,X21,X23))))))))))&(![X24]:(![X25]:(((?[X26]:(?[X27]:((member(X26,X25)&member(X27,X25))&(apply(X24,X26,X27)&apply(X24,X27,X26)))))|(?[X28]:(?[X29]:(?[X30]:(((member(X28,X25)&member(X29,X25))&member(X30,X25))&((apply(X24,X28,X29)&apply(X24,X29,X30))&~apply(X24,X28,X30)))))))|strict_order(X24,X25))))),inference(variable_rename,[status(thm)],[c44])).
% 3.86/4.06 fof(c47,plain,(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:((~strict_order(X17,X18)|(((~member(X19,X18)|~member(X20,X18))|(~apply(X17,X19,X20)|~apply(X17,X20,X19)))&(((~member(X21,X18)|~member(X22,X18))|~member(X23,X18))|((~apply(X17,X21,X22)|~apply(X17,X22,X23))|apply(X17,X21,X23)))))&((((member(skolem0002(X24,X25),X25)&member(skolem0003(X24,X25),X25))&(apply(X24,skolem0002(X24,X25),skolem0003(X24,X25))&apply(X24,skolem0003(X24,X25),skolem0002(X24,X25))))|(((member(skolem0004(X24,X25),X25)&member(skolem0005(X24,X25),X25))&member(skolem0006(X24,X25),X25))&((apply(X24,skolem0004(X24,X25),skolem0005(X24,X25))&apply(X24,skolem0005(X24,X25),skolem0006(X24,X25)))&~apply(X24,skolem0004(X24,X25),skolem0006(X24,X25)))))|strict_order(X24,X25)))))))))))),inference(shift_quantors,[status(thm)],[fof(c46,plain,((![X17]:(![X18]:(~strict_order(X17,X18)|((![X19]:(![X20]:((~member(X19,X18)|~member(X20,X18))|(~apply(X17,X19,X20)|~apply(X17,X20,X19)))))&(![X21]:(![X22]:(![X23]:(((~member(X21,X18)|~member(X22,X18))|~member(X23,X18))|((~apply(X17,X21,X22)|~apply(X17,X22,X23))|apply(X17,X21,X23))))))))))&(![X24]:(![X25]:((((member(skolem0002(X24,X25),X25)&member(skolem0003(X24,X25),X25))&(apply(X24,skolem0002(X24,X25),skolem0003(X24,X25))&apply(X24,skolem0003(X24,X25),skolem0002(X24,X25))))|(((member(skolem0004(X24,X25),X25)&member(skolem0005(X24,X25),X25))&member(skolem0006(X24,X25),X25))&((apply(X24,skolem0004(X24,X25),skolem0005(X24,X25))&apply(X24,skolem0005(X24,X25),skolem0006(X24,X25)))&~apply(X24,skolem0004(X24,X25),skolem0006(X24,X25)))))|strict_order(X24,X25))))),inference(skolemize,[status(esa)],[c45])).])).
% 3.86/4.06 fof(c48,plain,(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:(((~strict_order(X17,X18)|((~member(X19,X18)|~member(X20,X18))|(~apply(X17,X19,X20)|~apply(X17,X20,X19))))&(~strict_order(X17,X18)|(((~member(X21,X18)|~member(X22,X18))|~member(X23,X18))|((~apply(X17,X21,X22)|~apply(X17,X22,X23))|apply(X17,X21,X23)))))&(((((((member(skolem0002(X24,X25),X25)|member(skolem0004(X24,X25),X25))|strict_order(X24,X25))&((member(skolem0002(X24,X25),X25)|member(skolem0005(X24,X25),X25))|strict_order(X24,X25)))&((member(skolem0002(X24,X25),X25)|member(skolem0006(X24,X25),X25))|strict_order(X24,X25)))&((((member(skolem0002(X24,X25),X25)|apply(X24,skolem0004(X24,X25),skolem0005(X24,X25)))|strict_order(X24,X25))&((member(skolem0002(X24,X25),X25)|apply(X24,skolem0005(X24,X25),skolem0006(X24,X25)))|strict_order(X24,X25)))&((member(skolem0002(X24,X25),X25)|~apply(X24,skolem0004(X24,X25),skolem0006(X24,X25)))|strict_order(X24,X25))))&(((((member(skolem0003(X24,X25),X25)|member(skolem0004(X24,X25),X25))|strict_order(X24,X25))&((member(skolem0003(X24,X25),X25)|member(skolem0005(X24,X25),X25))|strict_order(X24,X25)))&((member(skolem0003(X24,X25),X25)|member(skolem0006(X24,X25),X25))|strict_order(X24,X25)))&((((member(skolem0003(X24,X25),X25)|apply(X24,skolem0004(X24,X25),skolem0005(X24,X25)))|strict_order(X24,X25))&((member(skolem0003(X24,X25),X25)|apply(X24,skolem0005(X24,X25),skolem0006(X24,X25)))|strict_order(X24,X25)))&((member(skolem0003(X24,X25),X25)|~apply(X24,skolem0004(X24,X25),skolem0006(X24,X25)))|strict_order(X24,X25)))))&((((((apply(X24,skolem0002(X24,X25),skolem0003(X24,X25))|member(skolem0004(X24,X25),X25))|strict_order(X24,X25))&((apply(X24,skolem0002(X24,X25),skolem0003(X24,X25))|member(skolem0005(X24,X25),X25))|strict_order(X24,X25)))&((apply(X24,skolem0002(X24,X25),skolem0003(X24,X25))|member(skolem0006(X24,X25),X25))|strict_order(X24,X25)))&((((apply(X24,skolem0002(X24,X25),skolem0003(X24,X25))|apply(X24,skolem0004(X24,X25),skolem0005(X24,X25)))|strict_order(X24,X25))&((apply(X24,skolem0002(X24,X25),skolem0003(X24,X25))|apply(X24,skolem0005(X24,X25),skolem0006(X24,X25)))|strict_order(X24,X25)))&((apply(X24,skolem0002(X24,X25),skolem0003(X24,X25))|~apply(X24,skolem0004(X24,X25),skolem0006(X24,X25)))|strict_order(X24,X25))))&(((((apply(X24,skolem0003(X24,X25),skolem0002(X24,X25))|member(skolem0004(X24,X25),X25))|strict_order(X24,X25))&((apply(X24,skolem0003(X24,X25),skolem0002(X24,X25))|member(skolem0005(X24,X25),X25))|strict_order(X24,X25)))&((apply(X24,skolem0003(X24,X25),skolem0002(X24,X25))|member(skolem0006(X24,X25),X25))|strict_order(X24,X25)))&((((apply(X24,skolem0003(X24,X25),skolem0002(X24,X25))|apply(X24,skolem0004(X24,X25),skolem0005(X24,X25)))|strict_order(X24,X25))&((apply(X24,skolem0003(X24,X25),skolem0002(X24,X25))|apply(X24,skolem0005(X24,X25),skolem0006(X24,X25)))|strict_order(X24,X25)))&((apply(X24,skolem0003(X24,X25),skolem0002(X24,X25))|~apply(X24,skolem0004(X24,X25),skolem0006(X24,X25)))|strict_order(X24,X25)))))))))))))))),inference(distribute,[status(thm)],[c47])).
% 3.86/4.06 cnf(c49,plain,~strict_order(X370,X368)|~member(X367,X368)|~member(X369,X368)|~apply(X370,X367,X369)|~apply(X370,X369,X367),inference(split_conjunct,[status(thm)],[c48])).
% 3.86/4.06 cnf(c467,plain,~strict_order(X1833,X1832)|~member(X1831,X1832)|~apply(X1833,X1831,X1831),inference(factor,[status(thm)],[c49])).
% 3.86/4.06 cnf(c9598,plain,~strict_order(member_predicate,X1834)|~member(skolem0001,X1834),inference(resolution,[status(thm)],[c467, c209])).
% 3.86/4.06 cnf(c9714,plain,~strict_order(member_predicate,skolem0001),inference(resolution,[status(thm)],[c9598, c24])).
% 3.86/4.06 cnf(c9820,plain,$false,inference(resolution,[status(thm)],[c9714, c216])).
% 3.86/4.06 % SZS output end CNFRefutation
% 3.86/4.06
% 3.86/4.06 % Initial clauses : 101
% 3.86/4.06 % Processed clauses : 618
% 3.86/4.06 % Factors computed : 22
% 3.86/4.06 % Resolvents computed: 9608
% 3.86/4.06 % Tautologies deleted: 4
% 3.86/4.06 % Forward subsumed : 449
% 3.86/4.06 % Backward subsumed : 3
% 3.86/4.06 % -------- CPU Time ---------
% 3.86/4.06 % User time : 3.673 s
% 3.86/4.06 % System time : 0.032 s
% 3.86/4.06 % Total time : 3.705 s
%------------------------------------------------------------------------------