%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU117+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n023.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:34 EDT 2024
% Result : Theorem 7.81s 7.99s
% Output : Refutation 7.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SEU117+1 : TPTP v8.1.2. Released v3.2.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n023.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 11:08:53 EDT 2024
% 0.13/0.35 % CPUTime :
% 7.81/7.99 % Version: 1.5
% 7.81/7.99 % SZS status Theorem
% 7.81/7.99 % SZS output start CNFRefutation
% 7.81/7.99 fof(t32_finsub_1,conjecture,(![A]:(![B]:(element(B,finite_subsets(A))=>element(B,powerset(A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t32_finsub_1)).
% 7.81/7.99 fof(c30,negated_conjecture,(~(![A]:(![B]:(element(B,finite_subsets(A))=>element(B,powerset(A)))))),inference(assume_negation,[status(cth)],[t32_finsub_1])).
% 7.81/7.99 fof(c31,negated_conjecture,(?[A]:(?[B]:(element(B,finite_subsets(A))&~element(B,powerset(A))))),inference(fof_nnf,[status(thm)],[c30])).
% 7.81/7.99 fof(c32,negated_conjecture,(?[X7]:(?[X8]:(element(X8,finite_subsets(X7))&~element(X8,powerset(X7))))),inference(variable_rename,[status(thm)],[c31])).
% 7.81/7.99 fof(c33,negated_conjecture,(element(skolem0003,finite_subsets(skolem0002))&~element(skolem0003,powerset(skolem0002))),inference(skolemize,[status(esa)],[c32])).
% 7.81/7.99 cnf(c35,negated_conjecture,~element(skolem0003,powerset(skolem0002)),inference(split_conjunct,[status(thm)],[c33])).
% 7.81/7.99 fof(t3_subset,axiom,(![A]:(![B]:(element(A,powerset(B))<=>subset(A,B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t3_subset)).
% 7.81/7.99 fof(c42,plain,(![A]:(![B]:((~element(A,powerset(B))|subset(A,B))&(~subset(A,B)|element(A,powerset(B)))))),inference(fof_nnf,[status(thm)],[t3_subset])).
% 7.81/7.99 fof(c43,plain,((![A]:(![B]:(~element(A,powerset(B))|subset(A,B))))&(![A]:(![B]:(~subset(A,B)|element(A,powerset(B)))))),inference(shift_quantors,[status(thm)],[c42])).
% 7.81/7.99 fof(c45,plain,(![X14]:(![X15]:(![X16]:(![X17]:((~element(X14,powerset(X15))|subset(X14,X15))&(~subset(X16,X17)|element(X16,powerset(X17)))))))),inference(shift_quantors,[status(thm)],[fof(c44,plain,((![X14]:(![X15]:(~element(X14,powerset(X15))|subset(X14,X15))))&(![X16]:(![X17]:(~subset(X16,X17)|element(X16,powerset(X17)))))),inference(variable_rename,[status(thm)],[c43])).])).
% 7.81/7.99 cnf(c47,plain,~subset(X228,X227)|element(X228,powerset(X227)),inference(split_conjunct,[status(thm)],[c45])).
% 7.81/7.99 fof(fc2_finsub_1,axiom,(![A]:((((~empty(finite_subsets(A)))&cup_closed(finite_subsets(A)))&diff_closed(finite_subsets(A)))&preboolean(finite_subsets(A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', fc2_finsub_1)).
% 7.81/7.99 fof(c125,plain,(![A]:(((~empty(finite_subsets(A))&cup_closed(finite_subsets(A)))&diff_closed(finite_subsets(A)))&preboolean(finite_subsets(A)))),inference(fof_simplification,[status(thm)],[fc2_finsub_1])).
% 7.81/7.99 fof(c126,plain,((((![A]:~empty(finite_subsets(A)))&(![A]:cup_closed(finite_subsets(A))))&(![A]:diff_closed(finite_subsets(A))))&(![A]:preboolean(finite_subsets(A)))),inference(shift_quantors,[status(thm)],[c125])).
% 7.81/7.99 fof(c128,plain,(![X40]:(![X41]:(![X42]:(![X43]:(((~empty(finite_subsets(X40))&cup_closed(finite_subsets(X41)))&diff_closed(finite_subsets(X42)))&preboolean(finite_subsets(X43))))))),inference(shift_quantors,[status(thm)],[fof(c127,plain,((((![X40]:~empty(finite_subsets(X40)))&(![X41]:cup_closed(finite_subsets(X41))))&(![X42]:diff_closed(finite_subsets(X42))))&(![X43]:preboolean(finite_subsets(X43)))),inference(variable_rename,[status(thm)],[c126])).])).
% 7.81/7.99 cnf(c132,plain,preboolean(finite_subsets(X92)),inference(split_conjunct,[status(thm)],[c128])).
% 7.81/7.99 cnf(reflexivity,axiom,X64=X64,theory(equality)).
% 7.81/7.99 fof(d5_finsub_1,axiom,(![A]:(![B]:(preboolean(B)=>(B=finite_subsets(A)<=>(![C]:(in(C,B)<=>(subset(C,A)&finite(C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', d5_finsub_1)).
% 7.81/7.99 fof(c18,plain,(![A]:(![B]:(~preboolean(B)|((B!=finite_subsets(A)|(![C]:((~in(C,B)|(subset(C,A)&finite(C)))&((~subset(C,A)|~finite(C))|in(C,B)))))&((?[C]:((~in(C,B)|(~subset(C,A)|~finite(C)))&(in(C,B)|(subset(C,A)&finite(C)))))|B=finite_subsets(A)))))),inference(fof_nnf,[status(thm)],[d5_finsub_1])).
% 7.81/7.99 fof(c19,plain,(![A]:(![B]:(~preboolean(B)|((B!=finite_subsets(A)|((![C]:(~in(C,B)|(subset(C,A)&finite(C))))&(![C]:((~subset(C,A)|~finite(C))|in(C,B)))))&((?[C]:((~in(C,B)|(~subset(C,A)|~finite(C)))&(in(C,B)|(subset(C,A)&finite(C)))))|B=finite_subsets(A)))))),inference(shift_quantors,[status(thm)],[c18])).
% 7.81/7.99 fof(c20,plain,(![X2]:(![X3]:(~preboolean(X3)|((X3!=finite_subsets(X2)|((![X4]:(~in(X4,X3)|(subset(X4,X2)&finite(X4))))&(![X5]:((~subset(X5,X2)|~finite(X5))|in(X5,X3)))))&((?[X6]:((~in(X6,X3)|(~subset(X6,X2)|~finite(X6)))&(in(X6,X3)|(subset(X6,X2)&finite(X6)))))|X3=finite_subsets(X2)))))),inference(variable_rename,[status(thm)],[c19])).
% 7.81/7.99 fof(c22,plain,(![X2]:(![X3]:(![X4]:(![X5]:(~preboolean(X3)|((X3!=finite_subsets(X2)|((~in(X4,X3)|(subset(X4,X2)&finite(X4)))&((~subset(X5,X2)|~finite(X5))|in(X5,X3))))&(((~in(skolem0001(X2,X3),X3)|(~subset(skolem0001(X2,X3),X2)|~finite(skolem0001(X2,X3))))&(in(skolem0001(X2,X3),X3)|(subset(skolem0001(X2,X3),X2)&finite(skolem0001(X2,X3)))))|X3=finite_subsets(X2)))))))),inference(shift_quantors,[status(thm)],[fof(c21,plain,(![X2]:(![X3]:(~preboolean(X3)|((X3!=finite_subsets(X2)|((![X4]:(~in(X4,X3)|(subset(X4,X2)&finite(X4))))&(![X5]:((~subset(X5,X2)|~finite(X5))|in(X5,X3)))))&(((~in(skolem0001(X2,X3),X3)|(~subset(skolem0001(X2,X3),X2)|~finite(skolem0001(X2,X3))))&(in(skolem0001(X2,X3),X3)|(subset(skolem0001(X2,X3),X2)&finite(skolem0001(X2,X3)))))|X3=finite_subsets(X2)))))),inference(skolemize,[status(esa)],[c20])).])).
% 7.81/7.99 fof(c23,plain,(![X2]:(![X3]:(![X4]:(![X5]:((((~preboolean(X3)|(X3!=finite_subsets(X2)|(~in(X4,X3)|subset(X4,X2))))&(~preboolean(X3)|(X3!=finite_subsets(X2)|(~in(X4,X3)|finite(X4)))))&(~preboolean(X3)|(X3!=finite_subsets(X2)|((~subset(X5,X2)|~finite(X5))|in(X5,X3)))))&((~preboolean(X3)|((~in(skolem0001(X2,X3),X3)|(~subset(skolem0001(X2,X3),X2)|~finite(skolem0001(X2,X3))))|X3=finite_subsets(X2)))&((~preboolean(X3)|((in(skolem0001(X2,X3),X3)|subset(skolem0001(X2,X3),X2))|X3=finite_subsets(X2)))&(~preboolean(X3)|((in(skolem0001(X2,X3),X3)|finite(skolem0001(X2,X3)))|X3=finite_subsets(X2)))))))))),inference(distribute,[status(thm)],[c22])).
% 7.81/7.99 cnf(c24,plain,~preboolean(X191)|X191!=finite_subsets(X189)|~in(X190,X191)|subset(X190,X189),inference(split_conjunct,[status(thm)],[c23])).
% 7.81/7.99 cnf(c332,plain,~preboolean(finite_subsets(X441))|~in(X442,finite_subsets(X441))|subset(X442,X441),inference(resolution,[status(thm)],[c24, reflexivity])).
% 7.81/7.99 cnf(c129,plain,~empty(finite_subsets(X87)),inference(split_conjunct,[status(thm)],[c128])).
% 7.81/7.99 cnf(c34,negated_conjecture,element(skolem0003,finite_subsets(skolem0002)),inference(split_conjunct,[status(thm)],[c33])).
% 7.81/7.99 fof(t2_subset,axiom,(![A]:(![B]:(element(A,B)=>(empty(B)|in(A,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t2_subset)).
% 7.81/7.99 fof(c162,plain,(![A]:(![B]:(~element(A,B)|(empty(B)|in(A,B))))),inference(fof_nnf,[status(thm)],[t2_subset])).
% 7.81/7.99 fof(c163,plain,(![X60]:(![X61]:(~element(X60,X61)|(empty(X61)|in(X60,X61))))),inference(variable_rename,[status(thm)],[c162])).
% 7.81/7.99 cnf(c164,plain,~element(X266,X267)|empty(X267)|in(X266,X267),inference(split_conjunct,[status(thm)],[c163])).
% 7.81/7.99 cnf(c514,plain,empty(finite_subsets(skolem0002))|in(skolem0003,finite_subsets(skolem0002)),inference(resolution,[status(thm)],[c164, c34])).
% 7.81/7.99 cnf(c3257,plain,in(skolem0003,finite_subsets(skolem0002)),inference(resolution,[status(thm)],[c514, c129])).
% 7.81/7.99 cnf(c3354,plain,~preboolean(finite_subsets(skolem0002))|subset(skolem0003,skolem0002),inference(resolution,[status(thm)],[c3257, c332])).
% 7.81/7.99 cnf(c14808,plain,subset(skolem0003,skolem0002),inference(resolution,[status(thm)],[c3354, c132])).
% 7.81/7.99 cnf(c14810,plain,element(skolem0003,powerset(skolem0002)),inference(resolution,[status(thm)],[c14808, c47])).
% 7.81/7.99 cnf(c14814,plain,$false,inference(resolution,[status(thm)],[c14810, c35])).
% 7.81/7.99 % SZS output end CNFRefutation
% 7.81/7.99
% 7.81/7.99 % Initial clauses : 87
% 7.81/7.99 % Processed clauses : 1127
% 7.81/7.99 % Factors computed : 5
% 7.81/7.99 % Resolvents computed: 14644
% 7.81/7.99 % Tautologies deleted: 29
% 7.81/7.99 % Forward subsumed : 1376
% 7.81/7.99 % Backward subsumed : 127
% 7.81/7.99 % -------- CPU Time ---------
% 7.81/7.99 % User time : 7.588 s
% 7.81/7.99 % System time : 0.040 s
% 7.81/7.99 % Total time : 7.628 s
%------------------------------------------------------------------------------