%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET810+4 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n021.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 4.29s 4.49s
% Output : Refutation 4.29s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : SET810+4 : TPTP v8.1.2. Released v3.2.0.
% 0.08/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.37 % Computer : n021.cluster.edu
% 0.15/0.37 % Model : x86_64 x86_64
% 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.37 % Memory : 8042.1875MB
% 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.37 % CPULimit : 300
% 0.15/0.37 % WCLimit : 300
% 0.15/0.37 % DateTime : Wed May 8 18:45:23 EDT 2024
% 0.15/0.37 % CPUTime :
% 4.29/4.49 % Version: 1.5
% 4.29/4.49 % SZS status Theorem
% 4.29/4.49 % SZS output start CNFRefutation
% 4.29/4.49 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/sandbox2/benchmark/Axioms/SET006+4.ax', strict_well_order)).
% 4.29/4.49 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))))))&((~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])).
% 4.29/4.49 fof(c94,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)],[c93])).
% 4.29/4.49 fof(c95,plain,((![X44]:(![X45]:(~strict_well_order(X44,X45)|(strict_order(X44,X45)&(![X46]:((~subset(X46,X45)|(![X47]:~member(X47,X46)))|(?[X48]:least(X48,X44,X46))))))))&(![X49]:(![X50]:((~strict_order(X49,X50)|(?[X51]:((subset(X51,X50)&(?[X52]:member(X52,X51)))&(![X53]:~least(X53,X49,X51)))))|strict_well_order(X49,X50))))),inference(variable_rename,[status(thm)],[c94])).
% 4.29/4.49 fof(c97,plain,(![X44]:(![X45]:(![X46]:(![X47]:(![X49]:(![X50]:(![X53]:((~strict_well_order(X44,X45)|(strict_order(X44,X45)&((~subset(X46,X45)|~member(X47,X46))|least(skolem0009(X44,X45,X46),X44,X46))))&((~strict_order(X49,X50)|((subset(skolem0010(X49,X50),X50)&member(skolem0011(X49,X50),skolem0010(X49,X50)))&~least(X53,X49,skolem0010(X49,X50))))|strict_well_order(X49,X50)))))))))),inference(shift_quantors,[status(thm)],[fof(c96,plain,((![X44]:(![X45]:(~strict_well_order(X44,X45)|(strict_order(X44,X45)&(![X46]:((~subset(X46,X45)|(![X47]:~member(X47,X46)))|least(skolem0009(X44,X45,X46),X44,X46)))))))&(![X49]:(![X50]:((~strict_order(X49,X50)|((subset(skolem0010(X49,X50),X50)&member(skolem0011(X49,X50),skolem0010(X49,X50)))&(![X53]:~least(X53,X49,skolem0010(X49,X50)))))|strict_well_order(X49,X50))))),inference(skolemize,[status(esa)],[c95])).])).
% 4.29/4.49 fof(c98,plain,(![X44]:(![X45]:(![X46]:(![X47]:(![X49]:(![X50]:(![X53]:(((~strict_well_order(X44,X45)|strict_order(X44,X45))&(~strict_well_order(X44,X45)|((~subset(X46,X45)|~member(X47,X46))|least(skolem0009(X44,X45,X46),X44,X46))))&((((~strict_order(X49,X50)|subset(skolem0010(X49,X50),X50))|strict_well_order(X49,X50))&((~strict_order(X49,X50)|member(skolem0011(X49,X50),skolem0010(X49,X50)))|strict_well_order(X49,X50)))&((~strict_order(X49,X50)|~least(X53,X49,skolem0010(X49,X50)))|strict_well_order(X49,X50))))))))))),inference(distribute,[status(thm)],[c97])).
% 4.29/4.49 cnf(c99,plain,~strict_well_order(X118,X119)|strict_order(X118,X119),inference(split_conjunct,[status(thm)],[c98])).
% 4.29/4.49 fof(thV3,conjecture,(![A]:(![B]:((member(A,on)&member(B,on))=>(~(member(A,B)&member(B,A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', thV3)).
% 4.29/4.49 fof(c18,negated_conjecture,(~(![A]:(![B]:((member(A,on)&member(B,on))=>(~(member(A,B)&member(B,A))))))),inference(assume_negation,[status(cth)],[thV3])).
% 4.29/4.49 fof(c19,negated_conjecture,(?[A]:(?[B]:((member(A,on)&member(B,on))&(member(A,B)&member(B,A))))),inference(fof_nnf,[status(thm)],[c18])).
% 4.29/4.49 fof(c20,negated_conjecture,(?[X2]:(?[X3]:((member(X2,on)&member(X3,on))&(member(X2,X3)&member(X3,X2))))),inference(variable_rename,[status(thm)],[c19])).
% 4.29/4.49 fof(c21,negated_conjecture,((member(skolem0001,on)&member(skolem0002,on))&(member(skolem0001,skolem0002)&member(skolem0002,skolem0001))),inference(skolemize,[status(esa)],[c20])).
% 4.29/4.49 cnf(c22,negated_conjecture,member(skolem0001,on),inference(split_conjunct,[status(thm)],[c21])).
% 4.29/4.49 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/sandbox2/benchmark/Axioms/SET006+4.ax', ordinal_number)).
% 4.29/4.49 fof(c104,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])).
% 4.29/4.49 fof(c105,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)],[c104])).
% 4.29/4.49 fof(c106,plain,((![X54]:(~member(X54,on)|((set(X54)&strict_well_order(member_predicate,X54))&(![X55]:(~member(X55,X54)|subset(X55,X54))))))&(![X56]:(((~set(X56)|~strict_well_order(member_predicate,X56))|(?[X57]:(member(X57,X56)&~subset(X57,X56))))|member(X56,on)))),inference(variable_rename,[status(thm)],[c105])).
% 4.29/4.49 fof(c108,plain,(![X54]:(![X55]:(![X56]:((~member(X54,on)|((set(X54)&strict_well_order(member_predicate,X54))&(~member(X55,X54)|subset(X55,X54))))&(((~set(X56)|~strict_well_order(member_predicate,X56))|(member(skolem0012(X56),X56)&~subset(skolem0012(X56),X56)))|member(X56,on)))))),inference(shift_quantors,[status(thm)],[fof(c107,plain,((![X54]:(~member(X54,on)|((set(X54)&strict_well_order(member_predicate,X54))&(![X55]:(~member(X55,X54)|subset(X55,X54))))))&(![X56]:(((~set(X56)|~strict_well_order(member_predicate,X56))|(member(skolem0012(X56),X56)&~subset(skolem0012(X56),X56)))|member(X56,on)))),inference(skolemize,[status(esa)],[c106])).])).
% 4.29/4.49 fof(c109,plain,(![X54]:(![X55]:(![X56]:((((~member(X54,on)|set(X54))&(~member(X54,on)|strict_well_order(member_predicate,X54)))&(~member(X54,on)|(~member(X55,X54)|subset(X55,X54))))&((((~set(X56)|~strict_well_order(member_predicate,X56))|member(skolem0012(X56),X56))|member(X56,on))&(((~set(X56)|~strict_well_order(member_predicate,X56))|~subset(skolem0012(X56),X56))|member(X56,on))))))),inference(distribute,[status(thm)],[c108])).
% 4.29/4.49 cnf(c111,plain,~member(X158,on)|strict_well_order(member_predicate,X158),inference(split_conjunct,[status(thm)],[c109])).
% 4.29/4.49 cnf(c223,plain,strict_well_order(member_predicate,skolem0001),inference(resolution,[status(thm)],[c111, c22])).
% 4.29/4.49 cnf(c226,plain,strict_order(member_predicate,skolem0001),inference(resolution,[status(thm)],[c223, c99])).
% 4.29/4.49 cnf(c25,negated_conjecture,member(skolem0002,skolem0001),inference(split_conjunct,[status(thm)],[c21])).
% 4.29/4.49 fof(rel_member,axiom,(![X]:(![Y]:(apply(member_predicate,X,Y)<=>member(X,Y)))),file('/export/starexec/sandbox2/benchmark/Axioms/SET006+4.ax', rel_member)).
% 4.29/4.49 fof(c76,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])).
% 4.29/4.49 fof(c77,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)],[c76])).
% 4.29/4.49 fof(c79,plain,(![X32]:(![X33]:(![X34]:(![X35]:((~apply(member_predicate,X32,X33)|member(X32,X33))&(~member(X34,X35)|apply(member_predicate,X34,X35))))))),inference(shift_quantors,[status(thm)],[fof(c78,plain,((![X32]:(![X33]:(~apply(member_predicate,X32,X33)|member(X32,X33))))&(![X34]:(![X35]:(~member(X34,X35)|apply(member_predicate,X34,X35))))),inference(variable_rename,[status(thm)],[c77])).])).
% 4.29/4.49 cnf(c81,plain,~member(X153,X152)|apply(member_predicate,X153,X152),inference(split_conjunct,[status(thm)],[c79])).
% 4.29/4.49 fof(subset,axiom,(![A]:(![B]:(subset(A,B)<=>(![X]:(member(X,A)=>member(X,B)))))),file('/export/starexec/sandbox2/benchmark/Axioms/SET006+0.ax', subset)).
% 4.29/4.49 fof(c189,plain,(![A]:(![B]:((~subset(A,B)|(![X]:(~member(X,A)|member(X,B))))&((?[X]:(member(X,A)&~member(X,B)))|subset(A,B))))),inference(fof_nnf,[status(thm)],[subset])).
% 4.29/4.49 fof(c190,plain,((![A]:(![B]:(~subset(A,B)|(![X]:(~member(X,A)|member(X,B))))))&(![A]:(![B]:((?[X]:(member(X,A)&~member(X,B)))|subset(A,B))))),inference(shift_quantors,[status(thm)],[c189])).
% 4.29/4.49 fof(c191,plain,((![X107]:(![X108]:(~subset(X107,X108)|(![X109]:(~member(X109,X107)|member(X109,X108))))))&(![X110]:(![X111]:((?[X112]:(member(X112,X110)&~member(X112,X111)))|subset(X110,X111))))),inference(variable_rename,[status(thm)],[c190])).
% 4.29/4.49 fof(c193,plain,(![X107]:(![X108]:(![X109]:(![X110]:(![X111]:((~subset(X107,X108)|(~member(X109,X107)|member(X109,X108)))&((member(skolem0015(X110,X111),X110)&~member(skolem0015(X110,X111),X111))|subset(X110,X111)))))))),inference(shift_quantors,[status(thm)],[fof(c192,plain,((![X107]:(![X108]:(~subset(X107,X108)|(![X109]:(~member(X109,X107)|member(X109,X108))))))&(![X110]:(![X111]:((member(skolem0015(X110,X111),X110)&~member(skolem0015(X110,X111),X111))|subset(X110,X111))))),inference(skolemize,[status(esa)],[c191])).])).
% 4.29/4.49 fof(c194,plain,(![X107]:(![X108]:(![X109]:(![X110]:(![X111]:((~subset(X107,X108)|(~member(X109,X107)|member(X109,X108)))&((member(skolem0015(X110,X111),X110)|subset(X110,X111))&(~member(skolem0015(X110,X111),X111)|subset(X110,X111))))))))),inference(distribute,[status(thm)],[c193])).
% 4.29/4.49 cnf(c195,plain,~subset(X508,X509)|~member(X510,X508)|member(X510,X509),inference(split_conjunct,[status(thm)],[c194])).
% 4.29/4.49 cnf(c1271,plain,~subset(skolem0001,X524)|member(skolem0002,X524),inference(resolution,[status(thm)],[c195, c25])).
% 4.29/4.49 cnf(c23,negated_conjecture,member(skolem0002,on),inference(split_conjunct,[status(thm)],[c21])).
% 4.29/4.49 cnf(c24,negated_conjecture,member(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c21])).
% 4.29/4.49 cnf(c112,plain,~member(X687,on)|~member(X686,X687)|subset(X686,X687),inference(split_conjunct,[status(thm)],[c109])).
% 4.29/4.49 cnf(c1968,plain,~member(skolem0002,on)|subset(skolem0001,skolem0002),inference(resolution,[status(thm)],[c112, c24])).
% 4.29/4.49 cnf(c4583,plain,subset(skolem0001,skolem0002),inference(resolution,[status(thm)],[c1968, c23])).
% 4.29/4.49 cnf(c4585,plain,member(skolem0002,skolem0002),inference(resolution,[status(thm)],[c4583, c1271])).
% 4.29/4.49 cnf(c4598,plain,apply(member_predicate,skolem0002,skolem0002),inference(resolution,[status(thm)],[c4585, c81])).
% 4.29/4.49 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/sandbox2/benchmark/Axioms/SET006+4.ax', strict_order)).
% 4.29/4.49 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))))))))&(((?[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])).
% 4.29/4.49 fof(c45,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)],[c44])).
% 4.29/4.49 fof(c46,plain,((![X18]:(![X19]:(~strict_order(X18,X19)|((![X20]:(![X21]:((~member(X20,X19)|~member(X21,X19))|(~apply(X18,X20,X21)|~apply(X18,X21,X20)))))&(![X22]:(![X23]:(![X24]:(((~member(X22,X19)|~member(X23,X19))|~member(X24,X19))|((~apply(X18,X22,X23)|~apply(X18,X23,X24))|apply(X18,X22,X24))))))))))&(![X25]:(![X26]:(((?[X27]:(?[X28]:((member(X27,X26)&member(X28,X26))&(apply(X25,X27,X28)&apply(X25,X28,X27)))))|(?[X29]:(?[X30]:(?[X31]:(((member(X29,X26)&member(X30,X26))&member(X31,X26))&((apply(X25,X29,X30)&apply(X25,X30,X31))&~apply(X25,X29,X31)))))))|strict_order(X25,X26))))),inference(variable_rename,[status(thm)],[c45])).
% 4.29/4.49 fof(c48,plain,(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:(![X26]:((~strict_order(X18,X19)|(((~member(X20,X19)|~member(X21,X19))|(~apply(X18,X20,X21)|~apply(X18,X21,X20)))&(((~member(X22,X19)|~member(X23,X19))|~member(X24,X19))|((~apply(X18,X22,X23)|~apply(X18,X23,X24))|apply(X18,X22,X24)))))&((((member(skolem0003(X25,X26),X26)&member(skolem0004(X25,X26),X26))&(apply(X25,skolem0003(X25,X26),skolem0004(X25,X26))&apply(X25,skolem0004(X25,X26),skolem0003(X25,X26))))|(((member(skolem0005(X25,X26),X26)&member(skolem0006(X25,X26),X26))&member(skolem0007(X25,X26),X26))&((apply(X25,skolem0005(X25,X26),skolem0006(X25,X26))&apply(X25,skolem0006(X25,X26),skolem0007(X25,X26)))&~apply(X25,skolem0005(X25,X26),skolem0007(X25,X26)))))|strict_order(X25,X26)))))))))))),inference(shift_quantors,[status(thm)],[fof(c47,plain,((![X18]:(![X19]:(~strict_order(X18,X19)|((![X20]:(![X21]:((~member(X20,X19)|~member(X21,X19))|(~apply(X18,X20,X21)|~apply(X18,X21,X20)))))&(![X22]:(![X23]:(![X24]:(((~member(X22,X19)|~member(X23,X19))|~member(X24,X19))|((~apply(X18,X22,X23)|~apply(X18,X23,X24))|apply(X18,X22,X24))))))))))&(![X25]:(![X26]:((((member(skolem0003(X25,X26),X26)&member(skolem0004(X25,X26),X26))&(apply(X25,skolem0003(X25,X26),skolem0004(X25,X26))&apply(X25,skolem0004(X25,X26),skolem0003(X25,X26))))|(((member(skolem0005(X25,X26),X26)&member(skolem0006(X25,X26),X26))&member(skolem0007(X25,X26),X26))&((apply(X25,skolem0005(X25,X26),skolem0006(X25,X26))&apply(X25,skolem0006(X25,X26),skolem0007(X25,X26)))&~apply(X25,skolem0005(X25,X26),skolem0007(X25,X26)))))|strict_order(X25,X26))))),inference(skolemize,[status(esa)],[c46])).])).
% 4.29/4.49 fof(c49,plain,(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:(![X26]:(((~strict_order(X18,X19)|((~member(X20,X19)|~member(X21,X19))|(~apply(X18,X20,X21)|~apply(X18,X21,X20))))&(~strict_order(X18,X19)|(((~member(X22,X19)|~member(X23,X19))|~member(X24,X19))|((~apply(X18,X22,X23)|~apply(X18,X23,X24))|apply(X18,X22,X24)))))&(((((((member(skolem0003(X25,X26),X26)|member(skolem0005(X25,X26),X26))|strict_order(X25,X26))&((member(skolem0003(X25,X26),X26)|member(skolem0006(X25,X26),X26))|strict_order(X25,X26)))&((member(skolem0003(X25,X26),X26)|member(skolem0007(X25,X26),X26))|strict_order(X25,X26)))&((((member(skolem0003(X25,X26),X26)|apply(X25,skolem0005(X25,X26),skolem0006(X25,X26)))|strict_order(X25,X26))&((member(skolem0003(X25,X26),X26)|apply(X25,skolem0006(X25,X26),skolem0007(X25,X26)))|strict_order(X25,X26)))&((member(skolem0003(X25,X26),X26)|~apply(X25,skolem0005(X25,X26),skolem0007(X25,X26)))|strict_order(X25,X26))))&(((((member(skolem0004(X25,X26),X26)|member(skolem0005(X25,X26),X26))|strict_order(X25,X26))&((member(skolem0004(X25,X26),X26)|member(skolem0006(X25,X26),X26))|strict_order(X25,X26)))&((member(skolem0004(X25,X26),X26)|member(skolem0007(X25,X26),X26))|strict_order(X25,X26)))&((((member(skolem0004(X25,X26),X26)|apply(X25,skolem0005(X25,X26),skolem0006(X25,X26)))|strict_order(X25,X26))&((member(skolem0004(X25,X26),X26)|apply(X25,skolem0006(X25,X26),skolem0007(X25,X26)))|strict_order(X25,X26)))&((member(skolem0004(X25,X26),X26)|~apply(X25,skolem0005(X25,X26),skolem0007(X25,X26)))|strict_order(X25,X26)))))&((((((apply(X25,skolem0003(X25,X26),skolem0004(X25,X26))|member(skolem0005(X25,X26),X26))|strict_order(X25,X26))&((apply(X25,skolem0003(X25,X26),skolem0004(X25,X26))|member(skolem0006(X25,X26),X26))|strict_order(X25,X26)))&((apply(X25,skolem0003(X25,X26),skolem0004(X25,X26))|member(skolem0007(X25,X26),X26))|strict_order(X25,X26)))&((((apply(X25,skolem0003(X25,X26),skolem0004(X25,X26))|apply(X25,skolem0005(X25,X26),skolem0006(X25,X26)))|strict_order(X25,X26))&((apply(X25,skolem0003(X25,X26),skolem0004(X25,X26))|apply(X25,skolem0006(X25,X26),skolem0007(X25,X26)))|strict_order(X25,X26)))&((apply(X25,skolem0003(X25,X26),skolem0004(X25,X26))|~apply(X25,skolem0005(X25,X26),skolem0007(X25,X26)))|strict_order(X25,X26))))&(((((apply(X25,skolem0004(X25,X26),skolem0003(X25,X26))|member(skolem0005(X25,X26),X26))|strict_order(X25,X26))&((apply(X25,skolem0004(X25,X26),skolem0003(X25,X26))|member(skolem0006(X25,X26),X26))|strict_order(X25,X26)))&((apply(X25,skolem0004(X25,X26),skolem0003(X25,X26))|member(skolem0007(X25,X26),X26))|strict_order(X25,X26)))&((((apply(X25,skolem0004(X25,X26),skolem0003(X25,X26))|apply(X25,skolem0005(X25,X26),skolem0006(X25,X26)))|strict_order(X25,X26))&((apply(X25,skolem0004(X25,X26),skolem0003(X25,X26))|apply(X25,skolem0006(X25,X26),skolem0007(X25,X26)))|strict_order(X25,X26)))&((apply(X25,skolem0004(X25,X26),skolem0003(X25,X26))|~apply(X25,skolem0005(X25,X26),skolem0007(X25,X26)))|strict_order(X25,X26)))))))))))))))),inference(distribute,[status(thm)],[c48])).
% 4.29/4.49 cnf(c50,plain,~strict_order(X359,X357)|~member(X360,X357)|~member(X358,X357)|~apply(X359,X360,X358)|~apply(X359,X358,X360),inference(split_conjunct,[status(thm)],[c49])).
% 4.29/4.49 cnf(c520,plain,~strict_order(X1738,X1737)|~member(X1736,X1737)|~apply(X1738,X1736,X1736),inference(factor,[status(thm)],[c50])).
% 4.29/4.49 cnf(c9406,plain,~strict_order(member_predicate,X1747)|~member(skolem0002,X1747),inference(resolution,[status(thm)],[c520, c4598])).
% 4.29/4.49 cnf(c9751,plain,~strict_order(member_predicate,skolem0001),inference(resolution,[status(thm)],[c9406, c25])).
% 4.29/4.49 cnf(c9902,plain,$false,inference(resolution,[status(thm)],[c9751, c226])).
% 4.29/4.49 % SZS output end CNFRefutation
% 4.29/4.49
% 4.29/4.49 % Initial clauses : 103
% 4.29/4.49 % Processed clauses : 666
% 4.29/4.49 % Factors computed : 20
% 4.29/4.49 % Resolvents computed: 9689
% 4.29/4.49 % Tautologies deleted: 5
% 4.29/4.49 % Forward subsumed : 496
% 4.29/4.49 % Backward subsumed : 7
% 4.29/4.49 % -------- CPU Time ---------
% 4.29/4.49 % User time : 4.094 s
% 4.29/4.49 % System time : 0.024 s
% 4.29/4.49 % Total time : 4.118 s
%------------------------------------------------------------------------------