%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU147+3 : TPTP v8.1.2. Bugfixed v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n015.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 234.47s 234.94s
% Output : Refutation 234.47s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SEU147+3 : TPTP v8.1.2. Bugfixed v4.0.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n015.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed May 8 10:52:38 EDT 2024
% 0.12/0.34 % CPUTime :
% 234.47/234.94 % Version: 1.5
% 234.47/234.94 % SZS status Theorem
% 234.47/234.94 % SZS output start CNFRefutation
% 234.47/234.94 fof(t1_zfmisc_1,conjecture,powerset(empty_set)=singleton(empty_set),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t1_zfmisc_1)).
% 234.47/234.94 fof(c14,negated_conjecture,(~powerset(empty_set)=singleton(empty_set)),inference(assume_negation,[status(cth)],[t1_zfmisc_1])).
% 234.47/234.94 fof(c15,negated_conjecture,powerset(empty_set)!=singleton(empty_set),inference(fof_simplification,[status(thm)],[c14])).
% 234.47/234.94 cnf(c16,negated_conjecture,powerset(empty_set)!=singleton(empty_set),inference(split_conjunct,[status(thm)],[c15])).
% 234.47/234.94 cnf(reflexivity,axiom,X25=X25,theory(equality)).
% 234.47/234.94 cnf(c2,axiom,X54!=X55|X56!=X57|~in(X54,X56)|in(X55,X57),theory(equality)).
% 234.47/234.94 fof(reflexivity_r1_tarski,axiom,(![A]:(![B]:subset(A,A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', reflexivity_r1_tarski)).
% 234.47/234.94 fof(c17,plain,(![A]:subset(A,A)),inference(fof_simplification,[status(thm)],[reflexivity_r1_tarski])).
% 234.47/234.94 fof(c18,plain,(![X6]:subset(X6,X6)),inference(variable_rename,[status(thm)],[c17])).
% 234.47/234.94 cnf(c19,plain,subset(X26,X26),inference(split_conjunct,[status(thm)],[c18])).
% 234.47/234.94 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)).
% 234.47/234.94 fof(c28,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])).
% 234.47/234.94 fof(c29,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)],[c28])).
% 234.47/234.94 fof(c30,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)],[c29])).
% 234.47/234.94 fof(c32,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(c31,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)],[c30])).])).
% 234.47/234.94 fof(c33,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)],[c32])).
% 234.47/234.94 cnf(c35,plain,X60!=powerset(X59)|~subset(X58,X59)|in(X58,X60),inference(split_conjunct,[status(thm)],[c33])).
% 234.47/234.94 cnf(c61,plain,~subset(X61,X62)|in(X61,powerset(X62)),inference(resolution,[status(thm)],[c35, reflexivity])).
% 234.47/234.94 cnf(c62,plain,in(X63,powerset(X63)),inference(resolution,[status(thm)],[c61, c19])).
% 234.47/234.94 cnf(c65,plain,X97!=X99|powerset(X97)!=X98|in(X99,X98),inference(resolution,[status(thm)],[c62, c2])).
% 234.47/234.94 cnf(c101,plain,X101!=X100|in(X100,powerset(X101)),inference(resolution,[status(thm)],[c65, reflexivity])).
% 234.47/234.94 cnf(symmetry,axiom,X27!=X28|X28=X27,theory(equality)).
% 234.47/234.94 fof(d1_tarski,axiom,(![A]:(![B]:(B=singleton(A)<=>(![C]:(in(C,B)<=>C=A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_tarski)).
% 234.47/234.94 fof(c38,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])).
% 234.47/234.94 fof(c39,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)],[c38])).
% 234.47/234.94 fof(c40,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)],[c39])).
% 234.47/234.94 fof(c42,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(c41,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)],[c40])).])).
% 234.47/234.94 fof(c43,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)],[c42])).
% 234.47/234.94 cnf(c47,plain,in(skolem0005(X134,X133),X133)|skolem0005(X134,X133)=X134|X133=singleton(X134),inference(split_conjunct,[status(thm)],[c43])).
% 234.47/234.94 cnf(c186,plain,in(skolem0005(X202,X203),X203)|X203=singleton(X202)|X202=skolem0005(X202,X203),inference(resolution,[status(thm)],[c47, symmetry])).
% 234.47/234.94 cnf(c455,plain,in(skolem0005(X1236,X1235),X1235)|X1235=singleton(X1236)|in(skolem0005(X1236,X1235),powerset(X1236)),inference(resolution,[status(thm)],[c186, c101])).
% 234.47/234.94 cnf(c16525,plain,in(skolem0005(X1304,powerset(X1304)),powerset(X1304))|powerset(X1304)=singleton(X1304),inference(factor,[status(thm)],[c455])).
% 234.47/234.94 cnf(c46,plain,~in(skolem0005(X124,X123),X123)|skolem0005(X124,X123)!=X124|X123=singleton(X124),inference(split_conjunct,[status(thm)],[c43])).
% 234.47/234.94 fof(t3_xboole_1,axiom,(![A]:(subset(A,empty_set)=>A=empty_set)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t3_xboole_1)).
% 234.47/234.94 fof(c5,plain,(![A]:(~subset(A,empty_set)|A=empty_set)),inference(fof_nnf,[status(thm)],[t3_xboole_1])).
% 234.47/234.94 fof(c6,plain,(![X2]:(~subset(X2,empty_set)|X2=empty_set)),inference(variable_rename,[status(thm)],[c5])).
% 234.47/234.94 cnf(c7,plain,~subset(X42,empty_set)|X42=empty_set,inference(split_conjunct,[status(thm)],[c6])).
% 234.47/234.94 cnf(c34,plain,X50!=powerset(X49)|~in(X51,X50)|subset(X51,X49),inference(split_conjunct,[status(thm)],[c33])).
% 234.47/234.94 cnf(c60,plain,~in(X53,powerset(X52))|subset(X53,X52),inference(resolution,[status(thm)],[c34, reflexivity])).
% 234.47/234.94 cnf(c16622,plain,in(skolem0005(empty_set,powerset(empty_set)),powerset(empty_set)),inference(resolution,[status(thm)],[c455, c16])).
% 234.47/234.94 cnf(c16673,plain,subset(skolem0005(empty_set,powerset(empty_set)),empty_set),inference(resolution,[status(thm)],[c16622, c60])).
% 234.47/234.94 cnf(c16684,plain,skolem0005(empty_set,powerset(empty_set))=empty_set,inference(resolution,[status(thm)],[c16673, c7])).
% 234.47/234.94 cnf(c16736,plain,~in(skolem0005(empty_set,powerset(empty_set)),powerset(empty_set))|powerset(empty_set)=singleton(empty_set),inference(resolution,[status(thm)],[c16684, c46])).
% 234.47/234.94 cnf(c342782,plain,powerset(empty_set)=singleton(empty_set),inference(resolution,[status(thm)],[c16736, c16525])).
% 234.47/234.94 cnf(c343129,plain,$false,inference(resolution,[status(thm)],[c342782, c16])).
% 234.47/234.94 % SZS output end CNFRefutation
% 234.47/234.94
% 234.47/234.94 % Initial clauses : 25
% 234.47/234.94 % Processed clauses : 1939
% 234.47/234.94 % Factors computed : 495
% 234.47/234.94 % Resolvents computed: 342635
% 234.47/234.94 % Tautologies deleted: 44
% 234.47/234.94 % Forward subsumed : 1867
% 234.47/234.94 % Backward subsumed : 4
% 234.47/234.94 % -------- CPU Time ---------
% 234.47/234.94 % User time : 233.360 s
% 234.47/234.94 % System time : 0.951 s
% 234.47/234.94 % Total time : 234.311 s
%------------------------------------------------------------------------------