%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU147+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n026.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:39 EDT 2024
% Result : Theorem 225.65s 225.86s
% Output : Refutation 225.65s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SEU147+1 : TPTP v8.1.2. Released v3.3.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n026.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed May 8 11:47:38 EDT 2024
% 0.14/0.34 % CPUTime :
% 225.65/225.86 % Version: 1.5
% 225.65/225.86 % SZS status Theorem
% 225.65/225.86 % SZS output start CNFRefutation
% 225.65/225.86 fof(t1_zfmisc_1,conjecture,powerset(empty_set)=singleton(empty_set),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t1_zfmisc_1)).
% 225.65/225.86 fof(c14,negated_conjecture,(~powerset(empty_set)=singleton(empty_set)),inference(assume_negation,[status(cth)],[t1_zfmisc_1])).
% 225.65/225.86 fof(c15,negated_conjecture,powerset(empty_set)!=singleton(empty_set),inference(fof_simplification,[status(thm)],[c14])).
% 225.65/225.86 cnf(c16,negated_conjecture,powerset(empty_set)!=singleton(empty_set),inference(split_conjunct,[status(thm)],[c15])).
% 225.65/225.86 cnf(reflexivity,axiom,X25=X25,theory(equality)).
% 225.65/225.86 cnf(c2,axiom,X50!=X49|X48!=X51|~in(X50,X48)|in(X49,X51),theory(equality)).
% 225.65/225.86 fof(reflexivity_r1_tarski,axiom,(![A]:(![B]:subset(A,A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', reflexivity_r1_tarski)).
% 225.65/225.86 fof(c17,plain,(![A]:subset(A,A)),inference(fof_simplification,[status(thm)],[reflexivity_r1_tarski])).
% 225.65/225.86 fof(c18,plain,(![X6]:subset(X6,X6)),inference(variable_rename,[status(thm)],[c17])).
% 225.65/225.86 cnf(c19,plain,subset(X26,X26),inference(split_conjunct,[status(thm)],[c18])).
% 225.65/225.86 fof(d1_zfmisc_1,axiom,(![A]:(![B]:(B=powerset(A)<=>(![C]:(in(C,B)<=>subset(C,A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_zfmisc_1)).
% 225.65/225.86 fof(c31,plain,(![A]:(![B]:((B!=powerset(A)|(![C]:((~in(C,B)|subset(C,A))&(~subset(C,A)|in(C,B)))))&((?[C]:((~in(C,B)|~subset(C,A))&(in(C,B)|subset(C,A))))|B=powerset(A))))),inference(fof_nnf,[status(thm)],[d1_zfmisc_1])).
% 225.65/225.86 fof(c32,plain,((![A]:(![B]:(B!=powerset(A)|((![C]:(~in(C,B)|subset(C,A)))&(![C]:(~subset(C,A)|in(C,B)))))))&(![A]:(![B]:((?[C]:((~in(C,B)|~subset(C,A))&(in(C,B)|subset(C,A))))|B=powerset(A))))),inference(shift_quantors,[status(thm)],[c31])).
% 225.65/225.86 fof(c33,plain,((![X9]:(![X10]:(X10!=powerset(X9)|((![X11]:(~in(X11,X10)|subset(X11,X9)))&(![X12]:(~subset(X12,X9)|in(X12,X10)))))))&(![X13]:(![X14]:((?[X15]:((~in(X15,X14)|~subset(X15,X13))&(in(X15,X14)|subset(X15,X13))))|X14=powerset(X13))))),inference(variable_rename,[status(thm)],[c32])).
% 225.65/225.86 fof(c35,plain,(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:((X10!=powerset(X9)|((~in(X11,X10)|subset(X11,X9))&(~subset(X12,X9)|in(X12,X10))))&(((~in(skolem0004(X13,X14),X14)|~subset(skolem0004(X13,X14),X13))&(in(skolem0004(X13,X14),X14)|subset(skolem0004(X13,X14),X13)))|X14=powerset(X13))))))))),inference(shift_quantors,[status(thm)],[fof(c34,plain,((![X9]:(![X10]:(X10!=powerset(X9)|((![X11]:(~in(X11,X10)|subset(X11,X9)))&(![X12]:(~subset(X12,X9)|in(X12,X10)))))))&(![X13]:(![X14]:(((~in(skolem0004(X13,X14),X14)|~subset(skolem0004(X13,X14),X13))&(in(skolem0004(X13,X14),X14)|subset(skolem0004(X13,X14),X13)))|X14=powerset(X13))))),inference(skolemize,[status(esa)],[c33])).])).
% 225.65/225.86 fof(c36,plain,(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(((X10!=powerset(X9)|(~in(X11,X10)|subset(X11,X9)))&(X10!=powerset(X9)|(~subset(X12,X9)|in(X12,X10))))&(((~in(skolem0004(X13,X14),X14)|~subset(skolem0004(X13,X14),X13))|X14=powerset(X13))&((in(skolem0004(X13,X14),X14)|subset(skolem0004(X13,X14),X13))|X14=powerset(X13)))))))))),inference(distribute,[status(thm)],[c35])).
% 225.65/225.86 cnf(c38,plain,X59!=powerset(X58)|~subset(X60,X58)|in(X60,X59),inference(split_conjunct,[status(thm)],[c36])).
% 225.65/225.86 cnf(c64,plain,~subset(X61,X62)|in(X61,powerset(X62)),inference(resolution,[status(thm)],[c38, reflexivity])).
% 225.65/225.86 cnf(c65,plain,in(X67,powerset(X67)),inference(resolution,[status(thm)],[c64, c19])).
% 225.65/225.86 cnf(c69,plain,X101!=X99|powerset(X101)!=X100|in(X99,X100),inference(resolution,[status(thm)],[c65, c2])).
% 225.65/225.86 cnf(c105,plain,X102!=X103|in(X103,powerset(X102)),inference(resolution,[status(thm)],[c69, reflexivity])).
% 225.65/225.86 cnf(symmetry,axiom,X27!=X28|X28=X27,theory(equality)).
% 225.65/225.86 fof(d1_tarski,axiom,(![A]:(![B]:(B=singleton(A)<=>(![C]:(in(C,B)<=>C=A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_tarski)).
% 225.65/225.86 fof(c41,plain,(![A]:(![B]:((B!=singleton(A)|(![C]:((~in(C,B)|C=A)&(C!=A|in(C,B)))))&((?[C]:((~in(C,B)|C!=A)&(in(C,B)|C=A)))|B=singleton(A))))),inference(fof_nnf,[status(thm)],[d1_tarski])).
% 225.65/225.86 fof(c42,plain,((![A]:(![B]:(B!=singleton(A)|((![C]:(~in(C,B)|C=A))&(![C]:(C!=A|in(C,B)))))))&(![A]:(![B]:((?[C]:((~in(C,B)|C!=A)&(in(C,B)|C=A)))|B=singleton(A))))),inference(shift_quantors,[status(thm)],[c41])).
% 225.65/225.86 fof(c43,plain,((![X16]:(![X17]:(X17!=singleton(X16)|((![X18]:(~in(X18,X17)|X18=X16))&(![X19]:(X19!=X16|in(X19,X17)))))))&(![X20]:(![X21]:((?[X22]:((~in(X22,X21)|X22!=X20)&(in(X22,X21)|X22=X20)))|X21=singleton(X20))))),inference(variable_rename,[status(thm)],[c42])).
% 225.65/225.86 fof(c45,plain,(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:((X17!=singleton(X16)|((~in(X18,X17)|X18=X16)&(X19!=X16|in(X19,X17))))&(((~in(skolem0005(X20,X21),X21)|skolem0005(X20,X21)!=X20)&(in(skolem0005(X20,X21),X21)|skolem0005(X20,X21)=X20))|X21=singleton(X20))))))))),inference(shift_quantors,[status(thm)],[fof(c44,plain,((![X16]:(![X17]:(X17!=singleton(X16)|((![X18]:(~in(X18,X17)|X18=X16))&(![X19]:(X19!=X16|in(X19,X17)))))))&(![X20]:(![X21]:(((~in(skolem0005(X20,X21),X21)|skolem0005(X20,X21)!=X20)&(in(skolem0005(X20,X21),X21)|skolem0005(X20,X21)=X20))|X21=singleton(X20))))),inference(skolemize,[status(esa)],[c43])).])).
% 225.65/225.86 fof(c46,plain,(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(((X17!=singleton(X16)|(~in(X18,X17)|X18=X16))&(X17!=singleton(X16)|(X19!=X16|in(X19,X17))))&(((~in(skolem0005(X20,X21),X21)|skolem0005(X20,X21)!=X20)|X21=singleton(X20))&((in(skolem0005(X20,X21),X21)|skolem0005(X20,X21)=X20)|X21=singleton(X20)))))))))),inference(distribute,[status(thm)],[c45])).
% 225.65/225.86 cnf(c50,plain,in(skolem0005(X128,X129),X129)|skolem0005(X128,X129)=X128|X129=singleton(X128),inference(split_conjunct,[status(thm)],[c46])).
% 225.65/225.86 cnf(c198,plain,in(skolem0005(X209,X208),X208)|X208=singleton(X209)|X209=skolem0005(X209,X208),inference(resolution,[status(thm)],[c50, symmetry])).
% 225.65/225.86 cnf(c528,plain,in(skolem0005(X1282,X1281),X1281)|X1281=singleton(X1282)|in(skolem0005(X1282,X1281),powerset(X1282)),inference(resolution,[status(thm)],[c198, c105])).
% 225.65/225.86 cnf(c17922,plain,in(skolem0005(empty_set,powerset(empty_set)),powerset(empty_set)),inference(resolution,[status(thm)],[c528, c16])).
% 225.65/225.86 cnf(c49,plain,~in(skolem0005(X118,X119),X119)|skolem0005(X118,X119)!=X118|X119=singleton(X118),inference(split_conjunct,[status(thm)],[c46])).
% 225.65/225.86 fof(t3_xboole_1,axiom,(![A]:(subset(A,empty_set)=>A=empty_set)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t3_xboole_1)).
% 225.65/225.86 fof(c5,plain,(![A]:(~subset(A,empty_set)|A=empty_set)),inference(fof_nnf,[status(thm)],[t3_xboole_1])).
% 225.65/225.86 fof(c6,plain,(![X2]:(~subset(X2,empty_set)|X2=empty_set)),inference(variable_rename,[status(thm)],[c5])).
% 225.65/225.86 cnf(c7,plain,~subset(X45,empty_set)|X45=empty_set,inference(split_conjunct,[status(thm)],[c6])).
% 225.65/225.86 cnf(c37,plain,X54!=powerset(X53)|~in(X55,X54)|subset(X55,X53),inference(split_conjunct,[status(thm)],[c36])).
% 225.65/225.86 cnf(c63,plain,~in(X57,powerset(X56))|subset(X57,X56),inference(resolution,[status(thm)],[c37, reflexivity])).
% 225.65/225.86 cnf(c17987,plain,subset(skolem0005(empty_set,powerset(empty_set)),empty_set),inference(resolution,[status(thm)],[c17922, c63])).
% 225.65/225.86 cnf(c17996,plain,skolem0005(empty_set,powerset(empty_set))=empty_set,inference(resolution,[status(thm)],[c17987, c7])).
% 225.65/225.86 cnf(c18003,plain,~in(skolem0005(empty_set,powerset(empty_set)),powerset(empty_set))|powerset(empty_set)=singleton(empty_set),inference(resolution,[status(thm)],[c17996, c49])).
% 225.65/225.86 cnf(c341408,plain,powerset(empty_set)=singleton(empty_set),inference(resolution,[status(thm)],[c18003, c17922])).
% 225.65/225.86 cnf(c341502,plain,$false,inference(resolution,[status(thm)],[c341408, c16])).
% 225.65/225.86 % SZS output end CNFRefutation
% 225.65/225.86
% 225.65/225.86 % Initial clauses : 28
% 225.65/225.86 % Processed clauses : 1942
% 225.65/225.86 % Factors computed : 497
% 225.65/225.86 % Resolvents computed: 341125
% 225.65/225.86 % Tautologies deleted: 46
% 225.65/225.86 % Forward subsumed : 1872
% 225.65/225.86 % Backward subsumed : 4
% 225.65/225.86 % -------- CPU Time ---------
% 225.65/225.86 % User time : 224.569 s
% 225.65/225.86 % System time : 0.915 s
% 225.65/225.86 % Total time : 225.484 s
%------------------------------------------------------------------------------