%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET766+4 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n004.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:03 EDT 2024
% Result : Theorem 104.94s 105.18s
% Output : Refutation 104.94s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : SET766+4 : TPTP v8.1.2. Released v2.2.0.
% 0.04/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n004.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Wed May 8 18:46:38 EDT 2024
% 0.15/0.36 % CPUTime :
% 104.94/105.18 % Version: 1.5
% 104.94/105.18 % SZS status Theorem
% 104.94/105.18 % SZS output start CNFRefutation
% 104.94/105.18 fof(thIII02,conjecture,(![E]:(![R]:(![A]:((equivalence(R,E)&member(A,E))=>member(A,equivalence_class(A,E,R)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', thIII02)).
% 104.94/105.18 fof(c17,negated_conjecture,(~(![E]:(![R]:(![A]:((equivalence(R,E)&member(A,E))=>member(A,equivalence_class(A,E,R))))))),inference(assume_negation,[status(cth)],[thIII02])).
% 104.94/105.18 fof(c18,negated_conjecture,(?[E]:(?[R]:(?[A]:((equivalence(R,E)&member(A,E))&~member(A,equivalence_class(A,E,R)))))),inference(fof_nnf,[status(thm)],[c17])).
% 104.94/105.18 fof(c19,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:((equivalence(X3,X2)&member(X4,X2))&~member(X4,equivalence_class(X4,X2,X3)))))),inference(variable_rename,[status(thm)],[c18])).
% 104.94/105.18 fof(c20,negated_conjecture,((equivalence(skolem0002,skolem0001)&member(skolem0003,skolem0001))&~member(skolem0003,equivalence_class(skolem0003,skolem0001,skolem0002))),inference(skolemize,[status(esa)],[c19])).
% 104.94/105.18 cnf(c23,negated_conjecture,~member(skolem0003,equivalence_class(skolem0003,skolem0001,skolem0002)),inference(split_conjunct,[status(thm)],[c20])).
% 104.94/105.18 cnf(c22,negated_conjecture,member(skolem0003,skolem0001),inference(split_conjunct,[status(thm)],[c20])).
% 104.94/105.18 fof(equivalence_class,axiom,(![R]:(![E]:(![A]:(![X]:(member(X,equivalence_class(A,E,R))<=>(member(X,E)&apply(R,A,X))))))),file('/export/starexec/sandbox2/benchmark/Axioms/SET006+2.ax', equivalence_class)).
% 104.94/105.18 fof(c44,plain,(![R]:(![E]:(![A]:(![X]:((~member(X,equivalence_class(A,E,R))|(member(X,E)&apply(R,A,X)))&((~member(X,E)|~apply(R,A,X))|member(X,equivalence_class(A,E,R)))))))),inference(fof_nnf,[status(thm)],[equivalence_class])).
% 104.94/105.18 fof(c45,plain,((![R]:(![E]:(![A]:(![X]:(~member(X,equivalence_class(A,E,R))|(member(X,E)&apply(R,A,X)))))))&(![R]:(![E]:(![A]:(![X]:((~member(X,E)|~apply(R,A,X))|member(X,equivalence_class(A,E,R)))))))),inference(shift_quantors,[status(thm)],[c44])).
% 104.94/105.18 fof(c47,plain,(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:((~member(X20,equivalence_class(X19,X18,X17))|(member(X20,X18)&apply(X17,X19,X20)))&((~member(X24,X22)|~apply(X21,X23,X24))|member(X24,equivalence_class(X23,X22,X21)))))))))))),inference(shift_quantors,[status(thm)],[fof(c46,plain,((![X17]:(![X18]:(![X19]:(![X20]:(~member(X20,equivalence_class(X19,X18,X17))|(member(X20,X18)&apply(X17,X19,X20)))))))&(![X21]:(![X22]:(![X23]:(![X24]:((~member(X24,X22)|~apply(X21,X23,X24))|member(X24,equivalence_class(X23,X22,X21)))))))),inference(variable_rename,[status(thm)],[c45])).])).
% 104.94/105.18 fof(c48,plain,(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(((~member(X20,equivalence_class(X19,X18,X17))|member(X20,X18))&(~member(X20,equivalence_class(X19,X18,X17))|apply(X17,X19,X20)))&((~member(X24,X22)|~apply(X21,X23,X24))|member(X24,equivalence_class(X23,X22,X21)))))))))))),inference(distribute,[status(thm)],[c47])).
% 104.94/105.18 cnf(c51,plain,~member(X470,X468)|~apply(X471,X469,X470)|member(X470,equivalence_class(X469,X468,X471)),inference(split_conjunct,[status(thm)],[c48])).
% 104.94/105.18 cnf(c21,negated_conjecture,equivalence(skolem0002,skolem0001),inference(split_conjunct,[status(thm)],[c20])).
% 104.94/105.18 fof(equivalence,axiom,(![A]:(![R]:(equivalence(R,A)<=>(((![X]:(member(X,A)=>apply(R,X,X)))&(![X]:(![Y]:((member(X,A)&member(Y,A))=>(apply(R,X,Y)=>apply(R,Y,X))))))&(![X]:(![Y]:(![Z]:(((member(X,A)&member(Y,A))&member(Z,A))=>((apply(R,X,Y)&apply(R,Y,Z))=>apply(R,X,Z)))))))))),file('/export/starexec/sandbox2/benchmark/Axioms/SET006+2.ax', equivalence)).
% 104.94/105.18 fof(c52,plain,(![A]:(![R]:((~equivalence(R,A)|(((![X]:(~member(X,A)|apply(R,X,X)))&(![X]:(![Y]:((~member(X,A)|~member(Y,A))|(~apply(R,X,Y)|apply(R,Y,X))))))&(![X]:(![Y]:(![Z]:(((~member(X,A)|~member(Y,A))|~member(Z,A))|((~apply(R,X,Y)|~apply(R,Y,Z))|apply(R,X,Z))))))))&((((?[X]:(member(X,A)&~apply(R,X,X)))|(?[X]:(?[Y]:((member(X,A)&member(Y,A))&(apply(R,X,Y)&~apply(R,Y,X))))))|(?[X]:(?[Y]:(?[Z]:(((member(X,A)&member(Y,A))&member(Z,A))&((apply(R,X,Y)&apply(R,Y,Z))&~apply(R,X,Z)))))))|equivalence(R,A))))),inference(fof_nnf,[status(thm)],[equivalence])).
% 104.94/105.18 fof(c53,plain,((![A]:(![R]:(~equivalence(R,A)|(((![X]:(~member(X,A)|apply(R,X,X)))&(![X]:(![Y]:((~member(X,A)|~member(Y,A))|(~apply(R,X,Y)|apply(R,Y,X))))))&(![X]:(![Y]:(![Z]:(((~member(X,A)|~member(Y,A))|~member(Z,A))|((~apply(R,X,Y)|~apply(R,Y,Z))|apply(R,X,Z))))))))))&(![A]:(![R]:((((?[X]:(member(X,A)&~apply(R,X,X)))|(?[X]:(?[Y]:((member(X,A)&member(Y,A))&(apply(R,X,Y)&~apply(R,Y,X))))))|(?[X]:(?[Y]:(?[Z]:(((member(X,A)&member(Y,A))&member(Z,A))&((apply(R,X,Y)&apply(R,Y,Z))&~apply(R,X,Z)))))))|equivalence(R,A))))),inference(shift_quantors,[status(thm)],[c52])).
% 104.94/105.18 fof(c54,plain,((![X25]:(![X26]:(~equivalence(X26,X25)|(((![X27]:(~member(X27,X25)|apply(X26,X27,X27)))&(![X28]:(![X29]:((~member(X28,X25)|~member(X29,X25))|(~apply(X26,X28,X29)|apply(X26,X29,X28))))))&(![X30]:(![X31]:(![X32]:(((~member(X30,X25)|~member(X31,X25))|~member(X32,X25))|((~apply(X26,X30,X31)|~apply(X26,X31,X32))|apply(X26,X30,X32))))))))))&(![X33]:(![X34]:((((?[X35]:(member(X35,X33)&~apply(X34,X35,X35)))|(?[X36]:(?[X37]:((member(X36,X33)&member(X37,X33))&(apply(X34,X36,X37)&~apply(X34,X37,X36))))))|(?[X38]:(?[X39]:(?[X40]:(((member(X38,X33)&member(X39,X33))&member(X40,X33))&((apply(X34,X38,X39)&apply(X34,X39,X40))&~apply(X34,X38,X40)))))))|equivalence(X34,X33))))),inference(variable_rename,[status(thm)],[c53])).
% 104.94/105.18 fof(c56,plain,(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:(![X34]:((~equivalence(X26,X25)|(((~member(X27,X25)|apply(X26,X27,X27))&((~member(X28,X25)|~member(X29,X25))|(~apply(X26,X28,X29)|apply(X26,X29,X28))))&(((~member(X30,X25)|~member(X31,X25))|~member(X32,X25))|((~apply(X26,X30,X31)|~apply(X26,X31,X32))|apply(X26,X30,X32)))))&((((member(skolem0008(X33,X34),X33)&~apply(X34,skolem0008(X33,X34),skolem0008(X33,X34)))|((member(skolem0009(X33,X34),X33)&member(skolem0010(X33,X34),X33))&(apply(X34,skolem0009(X33,X34),skolem0010(X33,X34))&~apply(X34,skolem0010(X33,X34),skolem0009(X33,X34)))))|(((member(skolem0011(X33,X34),X33)&member(skolem0012(X33,X34),X33))&member(skolem0013(X33,X34),X33))&((apply(X34,skolem0011(X33,X34),skolem0012(X33,X34))&apply(X34,skolem0012(X33,X34),skolem0013(X33,X34)))&~apply(X34,skolem0011(X33,X34),skolem0013(X33,X34)))))|equivalence(X34,X33))))))))))))),inference(shift_quantors,[status(thm)],[fof(c55,plain,((![X25]:(![X26]:(~equivalence(X26,X25)|(((![X27]:(~member(X27,X25)|apply(X26,X27,X27)))&(![X28]:(![X29]:((~member(X28,X25)|~member(X29,X25))|(~apply(X26,X28,X29)|apply(X26,X29,X28))))))&(![X30]:(![X31]:(![X32]:(((~member(X30,X25)|~member(X31,X25))|~member(X32,X25))|((~apply(X26,X30,X31)|~apply(X26,X31,X32))|apply(X26,X30,X32))))))))))&(![X33]:(![X34]:((((member(skolem0008(X33,X34),X33)&~apply(X34,skolem0008(X33,X34),skolem0008(X33,X34)))|((member(skolem0009(X33,X34),X33)&member(skolem0010(X33,X34),X33))&(apply(X34,skolem0009(X33,X34),skolem0010(X33,X34))&~apply(X34,skolem0010(X33,X34),skolem0009(X33,X34)))))|(((member(skolem0011(X33,X34),X33)&member(skolem0012(X33,X34),X33))&member(skolem0013(X33,X34),X33))&((apply(X34,skolem0011(X33,X34),skolem0012(X33,X34))&apply(X34,skolem0012(X33,X34),skolem0013(X33,X34)))&~apply(X34,skolem0011(X33,X34),skolem0013(X33,X34)))))|equivalence(X34,X33))))),inference(skolemize,[status(esa)],[c54])).])).
% 104.94/105.18 fof(c57,plain,(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:(![X34]:((((~equivalence(X26,X25)|(~member(X27,X25)|apply(X26,X27,X27)))&(~equivalence(X26,X25)|((~member(X28,X25)|~member(X29,X25))|(~apply(X26,X28,X29)|apply(X26,X29,X28)))))&(~equivalence(X26,X25)|(((~member(X30,X25)|~member(X31,X25))|~member(X32,X25))|((~apply(X26,X30,X31)|~apply(X26,X31,X32))|apply(X26,X30,X32)))))&(((((((((member(skolem0008(X33,X34),X33)|member(skolem0009(X33,X34),X33))|member(skolem0011(X33,X34),X33))|equivalence(X34,X33))&(((member(skolem0008(X33,X34),X33)|member(skolem0009(X33,X34),X33))|member(skolem0012(X33,X34),X33))|equivalence(X34,X33)))&(((member(skolem0008(X33,X34),X33)|member(skolem0009(X33,X34),X33))|member(skolem0013(X33,X34),X33))|equivalence(X34,X33)))&(((((member(skolem0008(X33,X34),X33)|member(skolem0009(X33,X34),X33))|apply(X34,skolem0011(X33,X34),skolem0012(X33,X34)))|equivalence(X34,X33))&(((member(skolem0008(X33,X34),X33)|member(skolem0009(X33,X34),X33))|apply(X34,skolem0012(X33,X34),skolem0013(X33,X34)))|equivalence(X34,X33)))&(((member(skolem0008(X33,X34),X33)|member(skolem0009(X33,X34),X33))|~apply(X34,skolem0011(X33,X34),skolem0013(X33,X34)))|equivalence(X34,X33))))&((((((member(skolem0008(X33,X34),X33)|member(skolem0010(X33,X34),X33))|member(skolem0011(X33,X34),X33))|equivalence(X34,X33))&(((member(skolem0008(X33,X34),X33)|member(skolem0010(X33,X34),X33))|member(skolem0012(X33,X34),X33))|equivalence(X34,X33)))&(((member(skolem0008(X33,X34),X33)|member(skolem0010(X33,X34),X33))|member(skolem0013(X33,X34),X33))|equivalence(X34,X33)))&(((((member(skolem0008(X33,X34),X33)|member(skolem0010(X33,X34),X33))|apply(X34,skolem0011(X33,X34),skolem0012(X33,X34)))|equivalence(X34,X33))&(((member(skolem0008(X33,X34),X33)|member(skolem0010(X33,X34),X33))|apply(X34,skolem0012(X33,X34),skolem0013(X33,X34)))|equivalence(X34,X33)))&(((member(skolem0008(X33,X34),X33)|member(skolem0010(X33,X34),X33))|~apply(X34,skolem0011(X33,X34),skolem0013(X33,X34)))|equivalence(X34,X33)))))&(((((((member(skolem0008(X33,X34),X33)|apply(X34,skolem0009(X33,X34),skolem0010(X33,X34)))|member(skolem0011(X33,X34),X33))|equivalence(X34,X33))&(((member(skolem0008(X33,X34),X33)|apply(X34,skolem0009(X33,X34),skolem0010(X33,X34)))|member(skolem0012(X33,X34),X33))|equivalence(X34,X33)))&(((member(skolem0008(X33,X34),X33)|apply(X34,skolem0009(X33,X34),skolem0010(X33,X34)))|member(skolem0013(X33,X34),X33))|equivalence(X34,X33)))&(((((member(skolem0008(X33,X34),X33)|apply(X34,skolem0009(X33,X34),skolem0010(X33,X34)))|apply(X34,skolem0011(X33,X34),skolem0012(X33,X34)))|equivalence(X34,X33))&(((member(skolem0008(X33,X34),X33)|apply(X34,skolem0009(X33,X34),skolem0010(X33,X34)))|apply(X34,skolem0012(X33,X34),skolem0013(X33,X34)))|equivalence(X34,X33)))&(((member(skolem0008(X33,X34),X33)|apply(X34,skolem0009(X33,X34),skolem0010(X33,X34)))|~apply(X34,skolem0011(X33,X34),skolem0013(X33,X34)))|equivalence(X34,X33))))&((((((member(skolem0008(X33,X34),X33)|~apply(X34,skolem0010(X33,X34),skolem0009(X33,X34)))|member(skolem0011(X33,X34),X33))|equivalence(X34,X33))&(((member(skolem0008(X33,X34),X33)|~apply(X34,skolem0010(X33,X34),skolem0009(X33,X34)))|member(skolem0012(X33,X34),X33))|equivalence(X34,X33)))&(((member(skolem0008(X33,X34),X33)|~apply(X34,skolem0010(X33,X34),skolem0009(X33,X34)))|member(skolem0013(X33,X34),X33))|equivalence(X34,X33)))&(((((member(skolem0008(X33,X34),X33)|~apply(X34,skolem0010(X33,X34),skolem0009(X33,X34)))|apply(X34,skolem0011(X33,X34),skolem0012(X33,X34)))|equivalence(X34,X33))&(((member(skolem0008(X33,X34),X33)|~apply(X34,skolem0010(X33,X34),skolem0009(X33,X34)))|apply(X34,skolem0012(X33,X34),skolem0013(X33,X34)))|equivalence(X34,X33)))&(((member(skolem0008(X33,X34),X33)|~apply(X34,skolem0010(X33,X34),skolem0009(X33,X34)))|~apply(X34,skolem0011(X33,X34),skolem0013(X33,X34)))|equivalence(X34,X33))))))&((((((((~apply(X34,skolem0008(X33,X34),skolem0008(X33,X34))|member(skolem0009(X33,X34),X33))|member(skolem0011(X33,X34),X33))|equivalence(X34,X33))&(((~apply(X34,skolem0008(X33,X34),skolem0008(X33,X34))|member(skolem0009(X33,X34),X33))|member(skolem0012(X33,X34),X33))|equivalence(X34,X33)))&(((~apply(X34,skolem0008(X33,X34),skolem0008(X33,X34))|member(skolem0009(X33,X34),X33))|member(skolem0013(X33,X34),X33))|equivalence(X34,X33)))&(((((~apply(X34,skolem0008(X33,X34),skolem0008(X33,X34))|member(skolem0009(X33,X34),X33))|apply(X34,skolem0011(X33,X34),skolem0012(X33,X34)))|equivalence(X34,X33))&(((~apply(X34,skolem0008(X33,X34),skolem0008(X33,X34))|member(skolem0009(X33,X34),X33))|apply(X34,skolem0012(X33,X34),skolem0013(X33,X34)))|equivalence(X34,X33)))&(((~apply(X34,skolem0008(X33,X34),skolem0008(X33,X34))|member(skolem0009(X33,X34),X33))|~apply(X34,skolem0011(X33,X34),skolem0013(X33,X34)))|equivalence(X34,X33))))&((((((~apply(X34,skolem0008(X33,X34),skolem0008(X33,X34))|member(skolem0010(X33,X34),X33))|member(skolem0011(X33,X34),X33))|equivalence(X34,X33))&(((~apply(X34,skolem0008(X33,X34),skolem0008(X33,X34))|member(skolem0010(X33,X34),X33))|member(skolem0012(X33,X34),X33))|equivalence(X34,X33)))&(((~apply(X34,skolem0008(X33,X34),skolem0008(X33,X34))|member(skolem0010(X33,X34),X33))|member(skolem0013(X33,X34),X33))|equivalence(X34,X33)))&(((((~apply(X34,skolem0008(X33,X34),skolem0008(X33,X34))|member(skolem0010(X33,X34),X33))|apply(X34,skolem0011(X33,X34),skolem0012(X33,X34)))|equivalence(X34,X33))&(((~apply(X34,skolem0008(X33,X34),skolem0008(X33,X34))|member(skolem0010(X33,X34),X33))|apply(X34,skolem0012(X33,X34),skolem0013(X33,X34)))|equivalence(X34,X33)))&(((~apply(X34,skolem0008(X33,X34),skolem0008(X33,X34))|member(skolem0010(X33,X34),X33))|~apply(X34,skolem0011(X33,X34),skolem0013(X33,X34)))|equivalence(X34,X33)))))&(((((((~apply(X34,skolem0008(X33,X34),skolem0008(X33,X34))|apply(X34,skolem0009(X33,X34),skolem0010(X33,X34)))|member(skolem0011(X33,X34),X33))|equivalence(X34,X33))&(((~apply(X34,skolem0008(X33,X34),skolem0008(X33,X34))|apply(X34,skolem0009(X33,X34),skolem0010(X33,X34)))|member(skolem0012(X33,X34),X33))|equivalence(X34,X33)))&(((~apply(X34,skolem0008(X33,X34),skolem0008(X33,X34))|apply(X34,skolem0009(X33,X34),skolem0010(X33,X34)))|member(skolem0013(X33,X34),X33))|equivalence(X34,X33)))&(((((~apply(X34,skolem0008(X33,X34),skolem0008(X33,X34))|apply(X34,skolem0009(X33,X34),skolem0010(X33,X34)))|apply(X34,skolem0011(X33,X34),skolem0012(X33,X34)))|equivalence(X34,X33))&(((~apply(X34,skolem0008(X33,X34),skolem0008(X33,X34))|apply(X34,skolem0009(X33,X34),skolem0010(X33,X34)))|apply(X34,skolem0012(X33,X34),skolem0013(X33,X34)))|equivalence(X34,X33)))&(((~apply(X34,skolem0008(X33,X34),skolem0008(X33,X34))|apply(X34,skolem0009(X33,X34),skolem0010(X33,X34)))|~apply(X34,skolem0011(X33,X34),skolem0013(X33,X34)))|equivalence(X34,X33))))&((((((~apply(X34,skolem0008(X33,X34),skolem0008(X33,X34))|~apply(X34,skolem0010(X33,X34),skolem0009(X33,X34)))|member(skolem0011(X33,X34),X33))|equivalence(X34,X33))&(((~apply(X34,skolem0008(X33,X34),skolem0008(X33,X34))|~apply(X34,skolem0010(X33,X34),skolem0009(X33,X34)))|member(skolem0012(X33,X34),X33))|equivalence(X34,X33)))&(((~apply(X34,skolem0008(X33,X34),skolem0008(X33,X34))|~apply(X34,skolem0010(X33,X34),skolem0009(X33,X34)))|member(skolem0013(X33,X34),X33))|equivalence(X34,X33)))&(((((~apply(X34,skolem0008(X33,X34),skolem0008(X33,X34))|~apply(X34,skolem0010(X33,X34),skolem0009(X33,X34)))|apply(X34,skolem0011(X33,X34),skolem0012(X33,X34)))|equivalence(X34,X33))&(((~apply(X34,skolem0008(X33,X34),skolem0008(X33,X34))|~apply(X34,skolem0010(X33,X34),skolem0009(X33,X34)))|apply(X34,skolem0012(X33,X34),skolem0013(X33,X34)))|equivalence(X34,X33)))&(((~apply(X34,skolem0008(X33,X34),skolem0008(X33,X34))|~apply(X34,skolem0010(X33,X34),skolem0009(X33,X34)))|~apply(X34,skolem0011(X33,X34),skolem0013(X33,X34)))|equivalence(X34,X33)))))))))))))))))),inference(distribute,[status(thm)],[c56])).
% 104.94/105.18 cnf(c58,plain,~equivalence(X484,X485)|~member(X483,X485)|apply(X484,X483,X483),inference(split_conjunct,[status(thm)],[c57])).
% 104.94/105.18 cnf(c902,plain,~equivalence(X584,skolem0001)|apply(X584,skolem0003,skolem0003),inference(resolution,[status(thm)],[c58, c22])).
% 104.94/105.18 cnf(c1475,plain,apply(skolem0002,skolem0003,skolem0003),inference(resolution,[status(thm)],[c902, c21])).
% 104.94/105.18 cnf(c1482,plain,~member(skolem0003,X15017)|member(skolem0003,equivalence_class(skolem0003,X15017,skolem0002)),inference(resolution,[status(thm)],[c1475, c51])).
% 104.94/105.18 cnf(c101519,plain,member(skolem0003,equivalence_class(skolem0003,skolem0001,skolem0002)),inference(resolution,[status(thm)],[c1482, c22])).
% 104.94/105.18 cnf(c101674,plain,$false,inference(resolution,[status(thm)],[c101519, c23])).
% 104.94/105.18 % SZS output end CNFRefutation
% 104.94/105.18
% 104.94/105.18 % Initial clauses : 147
% 104.94/105.18 % Processed clauses : 1893
% 104.94/105.18 % Factors computed : 43
% 104.94/105.18 % Resolvents computed: 101424
% 104.94/105.18 % Tautologies deleted: 36
% 104.94/105.18 % Forward subsumed : 4687
% 104.94/105.18 % Backward subsumed : 19
% 104.94/105.18 % -------- CPU Time ---------
% 104.94/105.18 % User time : 104.578 s
% 104.94/105.18 % System time : 0.223 s
% 104.94/105.18 % Total time : 104.801 s
%------------------------------------------------------------------------------