%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET882+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n027.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:18 EDT 2024
% Result : Theorem 0.48s 0.71s
% Output : Refutation 0.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SET882+1 : TPTP v8.1.2. Released v3.2.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n027.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 19:39:53 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.48/0.71 % Version: 1.5
% 0.48/0.71 % SZS status Theorem
% 0.48/0.71 % SZS output start CNFRefutation
% 0.48/0.71 fof(t23_zfmisc_1,conjecture,(![A]:(![B]:(A!=B=>set_difference(unordered_pair(A,B),singleton(B))=singleton(A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t23_zfmisc_1)).
% 0.48/0.71 fof(c5,negated_conjecture,(~(![A]:(![B]:(A!=B=>set_difference(unordered_pair(A,B),singleton(B))=singleton(A))))),inference(assume_negation,[status(cth)],[t23_zfmisc_1])).
% 0.48/0.71 fof(c6,negated_conjecture,(?[A]:(?[B]:(A!=B&set_difference(unordered_pair(A,B),singleton(B))!=singleton(A)))),inference(fof_nnf,[status(thm)],[c5])).
% 0.48/0.71 fof(c7,negated_conjecture,(?[X2]:(?[X3]:(X2!=X3&set_difference(unordered_pair(X2,X3),singleton(X3))!=singleton(X2)))),inference(variable_rename,[status(thm)],[c6])).
% 0.48/0.71 fof(c8,negated_conjecture,(skolem0001!=skolem0002&set_difference(unordered_pair(skolem0001,skolem0002),singleton(skolem0002))!=singleton(skolem0001)),inference(skolemize,[status(esa)],[c7])).
% 0.48/0.71 cnf(c9,negated_conjecture,skolem0001!=skolem0002,inference(split_conjunct,[status(thm)],[c8])).
% 0.48/0.71 cnf(reflexivity,axiom,X23=X23,theory(equality)).
% 0.48/0.71 fof(d1_tarski,axiom,(![A]:(![B]:(B=singleton(A)<=>(![C]:(in(C,B)<=>C=A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_tarski)).
% 0.48/0.71 fof(c28,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])).
% 0.48/0.71 fof(c29,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)],[c28])).
% 0.48/0.71 fof(c30,plain,((![X12]:(![X13]:(X13!=singleton(X12)|((![X14]:(~in(X14,X13)|X14=X12))&(![X15]:(X15!=X12|in(X15,X13)))))))&(![X16]:(![X17]:((?[X18]:((~in(X18,X17)|X18!=X16)&(in(X18,X17)|X18=X16)))|X17=singleton(X16))))),inference(variable_rename,[status(thm)],[c29])).
% 0.48/0.71 fof(c32,plain,(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:((X13!=singleton(X12)|((~in(X14,X13)|X14=X12)&(X15!=X12|in(X15,X13))))&(((~in(skolem0005(X16,X17),X17)|skolem0005(X16,X17)!=X16)&(in(skolem0005(X16,X17),X17)|skolem0005(X16,X17)=X16))|X17=singleton(X16))))))))),inference(shift_quantors,[status(thm)],[fof(c31,plain,((![X12]:(![X13]:(X13!=singleton(X12)|((![X14]:(~in(X14,X13)|X14=X12))&(![X15]:(X15!=X12|in(X15,X13)))))))&(![X16]:(![X17]:(((~in(skolem0005(X16,X17),X17)|skolem0005(X16,X17)!=X16)&(in(skolem0005(X16,X17),X17)|skolem0005(X16,X17)=X16))|X17=singleton(X16))))),inference(skolemize,[status(esa)],[c30])).])).
% 0.48/0.71 fof(c33,plain,(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(((X13!=singleton(X12)|(~in(X14,X13)|X14=X12))&(X13!=singleton(X12)|(X15!=X12|in(X15,X13))))&(((~in(skolem0005(X16,X17),X17)|skolem0005(X16,X17)!=X16)|X17=singleton(X16))&((in(skolem0005(X16,X17),X17)|skolem0005(X16,X17)=X16)|X17=singleton(X16)))))))))),inference(distribute,[status(thm)],[c32])).
% 0.48/0.71 cnf(c34,plain,X56!=singleton(X58)|~in(X57,X56)|X57=X58,inference(split_conjunct,[status(thm)],[c33])).
% 0.48/0.71 cnf(c60,plain,~in(X60,singleton(X59))|X60=X59,inference(resolution,[status(thm)],[c34, reflexivity])).
% 0.48/0.71 cnf(c10,negated_conjecture,set_difference(unordered_pair(skolem0001,skolem0002),singleton(skolem0002))!=singleton(skolem0001),inference(split_conjunct,[status(thm)],[c8])).
% 0.48/0.71 cnf(c35,plain,X62!=singleton(X63)|X61!=X63|in(X61,X62),inference(split_conjunct,[status(thm)],[c33])).
% 0.48/0.71 cnf(c61,plain,X69!=X68|in(X69,singleton(X68)),inference(resolution,[status(thm)],[c35, reflexivity])).
% 0.48/0.71 cnf(c62,plain,in(X70,singleton(X70)),inference(resolution,[status(thm)],[c61, reflexivity])).
% 0.48/0.71 fof(l39_zfmisc_1,axiom,(![A]:(![B]:(![C]:(set_difference(unordered_pair(A,B),C)=singleton(A)<=>((~in(A,C))&(in(B,C)|A=B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l39_zfmisc_1)).
% 0.48/0.71 fof(c18,plain,(![A]:(![B]:(![C]:(set_difference(unordered_pair(A,B),C)=singleton(A)<=>(~in(A,C)&(in(B,C)|A=B)))))),inference(fof_simplification,[status(thm)],[l39_zfmisc_1])).
% 0.48/0.71 fof(c19,plain,(![A]:(![B]:(![C]:((set_difference(unordered_pair(A,B),C)!=singleton(A)|(~in(A,C)&(in(B,C)|A=B)))&((in(A,C)|(~in(B,C)&A!=B))|set_difference(unordered_pair(A,B),C)=singleton(A)))))),inference(fof_nnf,[status(thm)],[c18])).
% 0.48/0.71 fof(c20,plain,((![A]:(![B]:(![C]:(set_difference(unordered_pair(A,B),C)!=singleton(A)|(~in(A,C)&(in(B,C)|A=B))))))&(![A]:(![B]:(![C]:((in(A,C)|(~in(B,C)&A!=B))|set_difference(unordered_pair(A,B),C)=singleton(A)))))),inference(shift_quantors,[status(thm)],[c19])).
% 0.48/0.71 fof(c22,plain,(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:((set_difference(unordered_pair(X6,X7),X8)!=singleton(X6)|(~in(X6,X8)&(in(X7,X8)|X6=X7)))&((in(X9,X11)|(~in(X10,X11)&X9!=X10))|set_difference(unordered_pair(X9,X10),X11)=singleton(X9))))))))),inference(shift_quantors,[status(thm)],[fof(c21,plain,((![X6]:(![X7]:(![X8]:(set_difference(unordered_pair(X6,X7),X8)!=singleton(X6)|(~in(X6,X8)&(in(X7,X8)|X6=X7))))))&(![X9]:(![X10]:(![X11]:((in(X9,X11)|(~in(X10,X11)&X9!=X10))|set_difference(unordered_pair(X9,X10),X11)=singleton(X9)))))),inference(variable_rename,[status(thm)],[c20])).])).
% 0.48/0.71 fof(c23,plain,(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(((set_difference(unordered_pair(X6,X7),X8)!=singleton(X6)|~in(X6,X8))&(set_difference(unordered_pair(X6,X7),X8)!=singleton(X6)|(in(X7,X8)|X6=X7)))&(((in(X9,X11)|~in(X10,X11))|set_difference(unordered_pair(X9,X10),X11)=singleton(X9))&((in(X9,X11)|X9!=X10)|set_difference(unordered_pair(X9,X10),X11)=singleton(X9)))))))))),inference(distribute,[status(thm)],[c22])).
% 0.48/0.71 cnf(c26,plain,in(X113,X115)|~in(X114,X115)|set_difference(unordered_pair(X113,X114),X115)=singleton(X113),inference(split_conjunct,[status(thm)],[c23])).
% 0.48/0.71 cnf(c96,plain,in(X346,singleton(X345))|set_difference(unordered_pair(X346,X345),singleton(X345))=singleton(X346),inference(resolution,[status(thm)],[c26, c62])).
% 0.48/0.71 cnf(c743,plain,in(skolem0001,singleton(skolem0002)),inference(resolution,[status(thm)],[c96, c10])).
% 0.48/0.71 cnf(c771,plain,skolem0001=skolem0002,inference(resolution,[status(thm)],[c743, c60])).
% 0.48/0.71 cnf(c774,plain,$false,inference(resolution,[status(thm)],[c771, c9])).
% 0.48/0.71 % SZS output end CNFRefutation
% 0.48/0.71
% 0.48/0.71 % Initial clauses : 22
% 0.48/0.71 % Processed clauses : 93
% 0.48/0.71 % Factors computed : 4
% 0.48/0.71 % Resolvents computed: 744
% 0.48/0.71 % Tautologies deleted: 4
% 0.48/0.71 % Forward subsumed : 61
% 0.48/0.71 % Backward subsumed : 0
% 0.48/0.71 % -------- CPU Time ---------
% 0.48/0.71 % User time : 0.349 s
% 0.48/0.71 % System time : 0.021 s
% 0.48/0.71 % Total time : 0.370 s
%------------------------------------------------------------------------------