%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUM405+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n025.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:35:43 EDT 2024
% Result : Theorem 4.39s 4.57s
% Output : Refutation 4.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NUM405+1 : 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 : n025.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 16:28:23 EDT 2024
% 0.13/0.34 % CPUTime :
% 4.39/4.57 % Version: 1.5
% 4.39/4.57 % SZS status Theorem
% 4.39/4.57 % SZS output start CNFRefutation
% 4.39/4.57 fof(t37_ordinal1,axiom,(![A]:(~(![B]:(in(B,A)<=>ordinal(B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t37_ordinal1)).
% 4.39/4.57 fof(c25,plain,(![A]:(?[B]:((~in(B,A)|~ordinal(B))&(in(B,A)|ordinal(B))))),inference(fof_nnf,[status(thm)],[t37_ordinal1])).
% 4.39/4.57 fof(c26,plain,(![X9]:(?[X10]:((~in(X10,X9)|~ordinal(X10))&(in(X10,X9)|ordinal(X10))))),inference(variable_rename,[status(thm)],[c25])).
% 4.39/4.57 fof(c27,plain,(![X9]:((~in(skolem0002(X9),X9)|~ordinal(skolem0002(X9)))&(in(skolem0002(X9),X9)|ordinal(skolem0002(X9))))),inference(skolemize,[status(esa)],[c26])).
% 4.39/4.57 cnf(c29,plain,in(skolem0002(X90),X90)|ordinal(skolem0002(X90)),inference(split_conjunct,[status(thm)],[c27])).
% 4.39/4.57 fof(s1_xboole_0__e2_43__ordinal1,axiom,(![A]:(?[B]:(![C]:(in(C,B)<=>(in(C,A)&ordinal(C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', s1_xboole_0__e2_43__ordinal1)).
% 4.39/4.57 fof(c36,plain,(![A]:(?[B]:(![C]:((~in(C,B)|(in(C,A)&ordinal(C)))&((~in(C,A)|~ordinal(C))|in(C,B)))))),inference(fof_nnf,[status(thm)],[s1_xboole_0__e2_43__ordinal1])).
% 4.39/4.57 fof(c37,plain,(![A]:(?[B]:((![C]:(~in(C,B)|(in(C,A)&ordinal(C))))&(![C]:((~in(C,A)|~ordinal(C))|in(C,B)))))),inference(shift_quantors,[status(thm)],[c36])).
% 4.39/4.57 fof(c38,plain,(![X15]:(?[X16]:((![X17]:(~in(X17,X16)|(in(X17,X15)&ordinal(X17))))&(![X18]:((~in(X18,X15)|~ordinal(X18))|in(X18,X16)))))),inference(variable_rename,[status(thm)],[c37])).
% 4.39/4.57 fof(c40,plain,(![X15]:(![X17]:(![X18]:((~in(X17,skolem0003(X15))|(in(X17,X15)&ordinal(X17)))&((~in(X18,X15)|~ordinal(X18))|in(X18,skolem0003(X15))))))),inference(shift_quantors,[status(thm)],[fof(c39,plain,(![X15]:((![X17]:(~in(X17,skolem0003(X15))|(in(X17,X15)&ordinal(X17))))&(![X18]:((~in(X18,X15)|~ordinal(X18))|in(X18,skolem0003(X15)))))),inference(skolemize,[status(esa)],[c38])).])).
% 4.39/4.57 fof(c41,plain,(![X15]:(![X17]:(![X18]:(((~in(X17,skolem0003(X15))|in(X17,X15))&(~in(X17,skolem0003(X15))|ordinal(X17)))&((~in(X18,X15)|~ordinal(X18))|in(X18,skolem0003(X15))))))),inference(distribute,[status(thm)],[c40])).
% 4.39/4.57 cnf(c43,plain,~in(X106,skolem0003(X107))|ordinal(X106),inference(split_conjunct,[status(thm)],[c41])).
% 4.39/4.57 cnf(c283,plain,ordinal(skolem0002(skolem0003(X115))),inference(resolution,[status(thm)],[c43, c29])).
% 4.39/4.57 cnf(c28,plain,~in(skolem0002(X88),X88)|~ordinal(skolem0002(X88)),inference(split_conjunct,[status(thm)],[c27])).
% 4.39/4.57 cnf(c44,plain,~in(X109,X108)|~ordinal(X109)|in(X109,skolem0003(X108)),inference(split_conjunct,[status(thm)],[c41])).
% 4.39/4.57 fof(t38_ordinal1,conjecture,(![A]:(~(![B]:(ordinal(B)=>in(B,A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t38_ordinal1)).
% 4.39/4.57 fof(c20,negated_conjecture,(~(![A]:(~(![B]:(ordinal(B)=>in(B,A)))))),inference(assume_negation,[status(cth)],[t38_ordinal1])).
% 4.39/4.57 fof(c21,negated_conjecture,(?[A]:(![B]:(~ordinal(B)|in(B,A)))),inference(fof_nnf,[status(thm)],[c20])).
% 4.39/4.57 fof(c22,negated_conjecture,(?[X7]:(![X8]:(~ordinal(X8)|in(X8,X7)))),inference(variable_rename,[status(thm)],[c21])).
% 4.39/4.57 fof(c23,negated_conjecture,(![X8]:(~ordinal(X8)|in(X8,skolem0001))),inference(skolemize,[status(esa)],[c22])).
% 4.39/4.57 cnf(c24,negated_conjecture,~ordinal(X86)|in(X86,skolem0001),inference(split_conjunct,[status(thm)],[c23])).
% 4.39/4.57 cnf(c384,plain,in(skolem0002(skolem0003(X183)),skolem0001),inference(resolution,[status(thm)],[c283, c24])).
% 4.39/4.57 cnf(c779,plain,~ordinal(skolem0002(skolem0003(X338)))|in(skolem0002(skolem0003(X338)),skolem0003(skolem0001)),inference(resolution,[status(thm)],[c384, c44])).
% 4.39/4.57 cnf(c2430,plain,in(skolem0002(skolem0003(X694)),skolem0003(skolem0001)),inference(resolution,[status(thm)],[c779, c283])).
% 4.39/4.57 cnf(c7065,plain,~ordinal(skolem0002(skolem0003(skolem0001))),inference(resolution,[status(thm)],[c2430, c28])).
% 4.39/4.57 cnf(c7075,plain,$false,inference(resolution,[status(thm)],[c7065, c283])).
% 4.39/4.57 % SZS output end CNFRefutation
% 4.39/4.57
% 4.39/4.57 % Initial clauses : 88
% 4.39/4.57 % Processed clauses : 961
% 4.39/4.57 % Factors computed : 6
% 4.39/4.57 % Resolvents computed: 6914
% 4.39/4.57 % Tautologies deleted: 16
% 4.39/4.57 % Forward subsumed : 1868
% 4.39/4.57 % Backward subsumed : 38
% 4.39/4.57 % -------- CPU Time ---------
% 4.39/4.57 % User time : 4.196 s
% 4.39/4.57 % System time : 0.029 s
% 4.39/4.57 % Total time : 4.225 s
%------------------------------------------------------------------------------