%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUM383+1 : TPTP v8.1.2. Released v3.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:35:41 EDT 2024
% Result : Theorem 0.81s 1.01s
% Output : Refutation 0.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : NUM383+1 : TPTP v8.1.2. Released v3.2.0.
% 0.04/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.35 % Computer : n004.cluster.edu
% 0.15/0.35 % Model : x86_64 x86_64
% 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.35 % Memory : 8042.1875MB
% 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.35 % CPULimit : 300
% 0.15/0.35 % WCLimit : 300
% 0.15/0.35 % DateTime : Wed May 8 16:44:08 EDT 2024
% 0.15/0.35 % CPUTime :
% 0.81/1.01 % Version: 1.5
% 0.81/1.01 % SZS status Theorem
% 0.81/1.01 % SZS output start CNFRefutation
% 0.81/1.01 fof(t7_ordinal1,conjecture,(![A]:(![B]:(~(in(A,B)&subset(B,A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t7_ordinal1)).
% 0.81/1.01 fof(c13,negated_conjecture,(~(![A]:(![B]:(~(in(A,B)&subset(B,A)))))),inference(assume_negation,[status(cth)],[t7_ordinal1])).
% 0.81/1.01 fof(c14,negated_conjecture,(?[A]:(?[B]:(in(A,B)&subset(B,A)))),inference(fof_nnf,[status(thm)],[c13])).
% 0.81/1.01 fof(c15,negated_conjecture,(?[X4]:(?[X5]:(in(X4,X5)&subset(X5,X4)))),inference(variable_rename,[status(thm)],[c14])).
% 0.81/1.01 fof(c16,negated_conjecture,(in(skolem0001,skolem0002)&subset(skolem0002,skolem0001)),inference(skolemize,[status(esa)],[c15])).
% 0.81/1.01 cnf(c17,negated_conjecture,in(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c16])).
% 0.81/1.01 fof(t7_boole,axiom,(![A]:(![B]:(~(in(A,B)&empty(B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t7_boole)).
% 0.81/1.01 fof(c19,plain,(![A]:(![B]:(~in(A,B)|~empty(B)))),inference(fof_nnf,[status(thm)],[t7_boole])).
% 0.81/1.01 fof(c20,plain,(![X6]:(![X7]:(~in(X6,X7)|~empty(X7)))),inference(variable_rename,[status(thm)],[c19])).
% 0.81/1.01 cnf(c21,plain,~in(X74,X75)|~empty(X75),inference(split_conjunct,[status(thm)],[c20])).
% 0.81/1.01 cnf(c133,plain,~empty(skolem0002),inference(resolution,[status(thm)],[c21, c17])).
% 0.81/1.01 fof(existence_m1_subset_1,axiom,(![A]:(?[B]:element(B,A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', existence_m1_subset_1)).
% 0.81/1.01 fof(c96,plain,(![X34]:(?[X35]:element(X35,X34))),inference(variable_rename,[status(thm)],[existence_m1_subset_1])).
% 0.81/1.01 fof(c97,plain,(![X34]:element(skolem0013(X34),X34)),inference(skolemize,[status(esa)],[c96])).
% 0.81/1.01 cnf(c98,plain,element(skolem0013(X59),X59),inference(split_conjunct,[status(thm)],[c97])).
% 0.81/1.01 fof(t2_subset,axiom,(![A]:(![B]:(element(A,B)=>(empty(B)|in(A,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t2_subset)).
% 0.81/1.01 fof(c37,plain,(![A]:(![B]:(~element(A,B)|(empty(B)|in(A,B))))),inference(fof_nnf,[status(thm)],[t2_subset])).
% 0.81/1.01 fof(c38,plain,(![X19]:(![X20]:(~element(X19,X20)|(empty(X20)|in(X19,X20))))),inference(variable_rename,[status(thm)],[c37])).
% 0.81/1.01 cnf(c39,plain,~element(X114,X113)|empty(X113)|in(X114,X113),inference(split_conjunct,[status(thm)],[c38])).
% 0.81/1.01 cnf(c216,plain,empty(X156)|in(skolem0013(X156),X156),inference(resolution,[status(thm)],[c39, c98])).
% 0.81/1.01 cnf(c479,plain,in(skolem0013(skolem0002),skolem0002),inference(resolution,[status(thm)],[c216, c133])).
% 0.81/1.01 fof(t5_subset,axiom,(![A]:(![B]:(![C]:(~((in(A,B)&element(B,powerset(C)))&empty(C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t5_subset)).
% 0.81/1.01 fof(c25,plain,(![A]:(![B]:(![C]:((~in(A,B)|~element(B,powerset(C)))|~empty(C))))),inference(fof_nnf,[status(thm)],[t5_subset])).
% 0.81/1.01 fof(c26,plain,(![X9]:(![X10]:(![X11]:((~in(X9,X10)|~element(X10,powerset(X11)))|~empty(X11))))),inference(variable_rename,[status(thm)],[c25])).
% 0.81/1.01 cnf(c27,plain,~in(X97,X98)|~element(X98,powerset(X96))|~empty(X96),inference(split_conjunct,[status(thm)],[c26])).
% 0.81/1.01 cnf(c18,negated_conjecture,subset(skolem0002,skolem0001),inference(split_conjunct,[status(thm)],[c16])).
% 0.81/1.01 fof(t3_subset,axiom,(![A]:(![B]:(element(A,powerset(B))<=>subset(A,B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t3_subset)).
% 0.81/1.01 fof(c31,plain,(![A]:(![B]:((~element(A,powerset(B))|subset(A,B))&(~subset(A,B)|element(A,powerset(B)))))),inference(fof_nnf,[status(thm)],[t3_subset])).
% 0.81/1.01 fof(c32,plain,((![A]:(![B]:(~element(A,powerset(B))|subset(A,B))))&(![A]:(![B]:(~subset(A,B)|element(A,powerset(B)))))),inference(shift_quantors,[status(thm)],[c31])).
% 0.81/1.01 fof(c34,plain,(![X15]:(![X16]:(![X17]:(![X18]:((~element(X15,powerset(X16))|subset(X15,X16))&(~subset(X17,X18)|element(X17,powerset(X18)))))))),inference(shift_quantors,[status(thm)],[fof(c33,plain,((![X15]:(![X16]:(~element(X15,powerset(X16))|subset(X15,X16))))&(![X17]:(![X18]:(~subset(X17,X18)|element(X17,powerset(X18)))))),inference(variable_rename,[status(thm)],[c32])).])).
% 0.81/1.01 cnf(c36,plain,~subset(X107,X108)|element(X107,powerset(X108)),inference(split_conjunct,[status(thm)],[c34])).
% 0.81/1.01 cnf(c208,plain,element(skolem0002,powerset(skolem0001)),inference(resolution,[status(thm)],[c36, c18])).
% 0.81/1.01 cnf(c338,plain,~in(X158,skolem0002)|~empty(skolem0001),inference(resolution,[status(thm)],[c208, c27])).
% 0.81/1.01 cnf(c566,plain,~empty(skolem0001),inference(resolution,[status(thm)],[c338, c479])).
% 0.81/1.01 fof(antisymmetry_r2_hidden,axiom,(![A]:(![B]:(in(A,B)=>(~in(B,A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', antisymmetry_r2_hidden)).
% 0.81/1.01 fof(c111,plain,(![A]:(![B]:(in(A,B)=>~in(B,A)))),inference(fof_simplification,[status(thm)],[antisymmetry_r2_hidden])).
% 0.81/1.01 fof(c112,plain,(![A]:(![B]:(~in(A,B)|~in(B,A)))),inference(fof_nnf,[status(thm)],[c111])).
% 0.81/1.01 fof(c113,plain,(![X39]:(![X40]:(~in(X39,X40)|~in(X40,X39)))),inference(variable_rename,[status(thm)],[c112])).
% 0.81/1.01 cnf(c114,plain,~in(X93,X92)|~in(X92,X93),inference(split_conjunct,[status(thm)],[c113])).
% 0.81/1.01 cnf(c203,plain,~in(X94,X94),inference(factor,[status(thm)],[c114])).
% 0.81/1.01 fof(t4_subset,axiom,(![A]:(![B]:(![C]:((in(A,B)&element(B,powerset(C)))=>element(A,C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t4_subset)).
% 0.81/1.01 fof(c28,plain,(![A]:(![B]:(![C]:((~in(A,B)|~element(B,powerset(C)))|element(A,C))))),inference(fof_nnf,[status(thm)],[t4_subset])).
% 0.81/1.01 fof(c29,plain,(![X12]:(![X13]:(![X14]:((~in(X12,X13)|~element(X13,powerset(X14)))|element(X12,X14))))),inference(variable_rename,[status(thm)],[c28])).
% 0.81/1.01 cnf(c30,plain,~in(X102,X104)|~element(X104,powerset(X103))|element(X102,X103),inference(split_conjunct,[status(thm)],[c29])).
% 0.81/1.01 cnf(c340,plain,~in(X194,skolem0002)|element(X194,skolem0001),inference(resolution,[status(thm)],[c208, c30])).
% 0.81/1.01 cnf(c796,plain,element(skolem0001,skolem0001),inference(resolution,[status(thm)],[c340, c17])).
% 0.81/1.01 cnf(c800,plain,empty(skolem0001)|in(skolem0001,skolem0001),inference(resolution,[status(thm)],[c796, c39])).
% 0.81/1.01 cnf(c1098,plain,empty(skolem0001),inference(resolution,[status(thm)],[c800, c203])).
% 0.81/1.01 cnf(c1104,plain,$false,inference(resolution,[status(thm)],[c1098, c566])).
% 0.81/1.01 % SZS output end CNFRefutation
% 0.81/1.01
% 0.81/1.01 % Initial clauses : 60
% 0.81/1.01 % Processed clauses : 319
% 0.81/1.01 % Factors computed : 4
% 0.81/1.01 % Resolvents computed: 994
% 0.81/1.01 % Tautologies deleted: 12
% 0.81/1.01 % Forward subsumed : 291
% 0.81/1.01 % Backward subsumed : 20
% 0.81/1.01 % -------- CPU Time ---------
% 0.81/1.01 % User time : 0.633 s
% 0.81/1.01 % System time : 0.019 s
% 0.81/1.01 % Total time : 0.652 s
%------------------------------------------------------------------------------