%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU148+3 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n029.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:40 EDT 2024
% Result : Theorem 0.48s 0.65s
% Output : Refutation 0.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU148+3 : TPTP v8.1.2. Released v3.2.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n029.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:21:38 EDT 2024
% 0.14/0.34 % CPUTime :
% 0.48/0.65 % Version: 1.5
% 0.48/0.65 % SZS status Theorem
% 0.48/0.65 % SZS output start CNFRefutation
% 0.48/0.65 fof(t6_zfmisc_1,conjecture,(![A]:(![B]:(subset(singleton(A),singleton(B))=>A=B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t6_zfmisc_1)).
% 0.48/0.65 fof(c4,negated_conjecture,(~(![A]:(![B]:(subset(singleton(A),singleton(B))=>A=B)))),inference(assume_negation,[status(cth)],[t6_zfmisc_1])).
% 0.48/0.65 fof(c5,negated_conjecture,(?[A]:(?[B]:(subset(singleton(A),singleton(B))&A!=B))),inference(fof_nnf,[status(thm)],[c4])).
% 0.48/0.65 fof(c6,negated_conjecture,(?[X2]:(?[X3]:(subset(singleton(X2),singleton(X3))&X2!=X3))),inference(variable_rename,[status(thm)],[c5])).
% 0.48/0.65 fof(c7,negated_conjecture,(subset(singleton(skolem0001),singleton(skolem0002))&skolem0001!=skolem0002),inference(skolemize,[status(esa)],[c6])).
% 0.48/0.65 cnf(c9,negated_conjecture,skolem0001!=skolem0002,inference(split_conjunct,[status(thm)],[c7])).
% 0.48/0.65 cnf(reflexivity,axiom,X21=X21,theory(equality)).
% 0.48/0.65 fof(d1_tarski,axiom,(![A]:(![B]:(B=singleton(A)<=>(![C]:(in(C,B)<=>C=A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', d1_tarski)).
% 0.48/0.65 fof(c31,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.65 fof(c32,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)],[c31])).
% 0.48/0.65 fof(c33,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)],[c32])).
% 0.48/0.65 fof(c35,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(c34,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)],[c33])).])).
% 0.48/0.65 fof(c36,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)],[c35])).
% 0.48/0.65 cnf(c37,plain,X54!=singleton(X52)|~in(X53,X54)|X53=X52,inference(split_conjunct,[status(thm)],[c36])).
% 0.48/0.65 cnf(c53,plain,~in(X55,singleton(X56))|X55=X56,inference(resolution,[status(thm)],[c37, reflexivity])).
% 0.48/0.65 cnf(c1,axiom,X51!=X48|X50!=X49|~in(X51,X50)|in(X48,X49),theory(equality)).
% 0.48/0.65 cnf(c38,plain,X59!=singleton(X57)|X58!=X57|in(X58,X59),inference(split_conjunct,[status(thm)],[c36])).
% 0.48/0.65 cnf(c54,plain,X61!=X60|in(X61,singleton(X60)),inference(resolution,[status(thm)],[c38, reflexivity])).
% 0.48/0.65 cnf(c55,plain,in(X62,singleton(X62)),inference(resolution,[status(thm)],[c54, reflexivity])).
% 0.48/0.65 cnf(c56,plain,X82!=X81|singleton(X82)!=X80|in(X81,X80),inference(resolution,[status(thm)],[c55, c1])).
% 0.48/0.65 fof(l1_zfmisc_1,axiom,(![A]:singleton(A)!=empty_set),file('/export/starexec/sandbox/benchmark/theBenchmark.p', l1_zfmisc_1)).
% 0.48/0.65 fof(c28,plain,(![X11]:singleton(X11)!=empty_set),inference(variable_rename,[status(thm)],[l1_zfmisc_1])).
% 0.48/0.65 cnf(c29,plain,singleton(X26)!=empty_set,inference(split_conjunct,[status(thm)],[c28])).
% 0.48/0.65 cnf(c8,negated_conjecture,subset(singleton(skolem0001),singleton(skolem0002)),inference(split_conjunct,[status(thm)],[c7])).
% 0.48/0.65 fof(l4_zfmisc_1,axiom,(![A]:(![B]:(subset(A,singleton(B))<=>(A=empty_set|A=singleton(B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', l4_zfmisc_1)).
% 0.48/0.65 fof(c20,plain,(![A]:(![B]:((~subset(A,singleton(B))|(A=empty_set|A=singleton(B)))&((A!=empty_set&A!=singleton(B))|subset(A,singleton(B)))))),inference(fof_nnf,[status(thm)],[l4_zfmisc_1])).
% 0.48/0.65 fof(c21,plain,((![A]:(![B]:(~subset(A,singleton(B))|(A=empty_set|A=singleton(B)))))&(![A]:(![B]:((A!=empty_set&A!=singleton(B))|subset(A,singleton(B)))))),inference(shift_quantors,[status(thm)],[c20])).
% 0.48/0.65 fof(c23,plain,(![X7]:(![X8]:(![X9]:(![X10]:((~subset(X7,singleton(X8))|(X7=empty_set|X7=singleton(X8)))&((X9!=empty_set&X9!=singleton(X10))|subset(X9,singleton(X10)))))))),inference(shift_quantors,[status(thm)],[fof(c22,plain,((![X7]:(![X8]:(~subset(X7,singleton(X8))|(X7=empty_set|X7=singleton(X8)))))&(![X9]:(![X10]:((X9!=empty_set&X9!=singleton(X10))|subset(X9,singleton(X10)))))),inference(variable_rename,[status(thm)],[c21])).])).
% 0.48/0.65 fof(c24,plain,(![X7]:(![X8]:(![X9]:(![X10]:((~subset(X7,singleton(X8))|(X7=empty_set|X7=singleton(X8)))&((X9!=empty_set|subset(X9,singleton(X10)))&(X9!=singleton(X10)|subset(X9,singleton(X10))))))))),inference(distribute,[status(thm)],[c23])).
% 0.48/0.65 cnf(c25,plain,~subset(X77,singleton(X76))|X77=empty_set|X77=singleton(X76),inference(split_conjunct,[status(thm)],[c24])).
% 0.48/0.65 cnf(c65,plain,singleton(skolem0001)=empty_set|singleton(skolem0001)=singleton(skolem0002),inference(resolution,[status(thm)],[c25, c8])).
% 0.48/0.65 cnf(c113,plain,singleton(skolem0001)=singleton(skolem0002),inference(resolution,[status(thm)],[c65, c29])).
% 0.48/0.65 cnf(c140,plain,skolem0001!=X109|in(X109,singleton(skolem0002)),inference(resolution,[status(thm)],[c113, c56])).
% 0.48/0.65 cnf(c214,plain,in(skolem0001,singleton(skolem0002)),inference(resolution,[status(thm)],[c140, reflexivity])).
% 0.48/0.65 cnf(c217,plain,skolem0001=skolem0002,inference(resolution,[status(thm)],[c214, c53])).
% 0.48/0.65 cnf(c221,plain,$false,inference(resolution,[status(thm)],[c217, c9])).
% 0.48/0.65 % SZS output end CNFRefutation
% 0.48/0.65
% 0.48/0.65 % Initial clauses : 22
% 0.48/0.65 % Processed clauses : 48
% 0.48/0.65 % Factors computed : 4
% 0.48/0.65 % Resolvents computed: 180
% 0.48/0.65 % Tautologies deleted: 3
% 0.48/0.65 % Forward subsumed : 18
% 0.48/0.65 % Backward subsumed : 1
% 0.48/0.65 % -------- CPU Time ---------
% 0.48/0.65 % User time : 0.264 s
% 0.48/0.65 % System time : 0.018 s
% 0.48/0.65 % Total time : 0.282 s
%------------------------------------------------------------------------------