%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU148+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n024.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 0.47s 0.63s
% Output : Refutation 0.47s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU148+1 : TPTP v8.1.2. Released v3.3.0.
% 0.07/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n024.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed May 8 11:25:23 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.47/0.63 % Version: 1.5
% 0.47/0.63 % SZS status Theorem
% 0.47/0.63 % SZS output start CNFRefutation
% 0.47/0.63 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.47/0.63 fof(c4,negated_conjecture,(~(![A]:(![B]:(subset(singleton(A),singleton(B))=>A=B)))),inference(assume_negation,[status(cth)],[t6_zfmisc_1])).
% 0.47/0.63 fof(c5,negated_conjecture,(?[A]:(?[B]:(subset(singleton(A),singleton(B))&A!=B))),inference(fof_nnf,[status(thm)],[c4])).
% 0.47/0.63 fof(c6,negated_conjecture,(?[X2]:(?[X3]:(subset(singleton(X2),singleton(X3))&X2!=X3))),inference(variable_rename,[status(thm)],[c5])).
% 0.47/0.63 fof(c7,negated_conjecture,(subset(singleton(skolem0001),singleton(skolem0002))&skolem0001!=skolem0002),inference(skolemize,[status(esa)],[c6])).
% 0.47/0.63 cnf(c9,negated_conjecture,skolem0001!=skolem0002,inference(split_conjunct,[status(thm)],[c7])).
% 0.47/0.63 cnf(reflexivity,axiom,X21=X21,theory(equality)).
% 0.47/0.63 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.47/0.63 fof(c33,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.47/0.63 fof(c34,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)],[c33])).
% 0.47/0.63 fof(c35,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)],[c34])).
% 0.47/0.63 fof(c37,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(c36,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)],[c35])).])).
% 0.47/0.63 fof(c38,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)],[c37])).
% 0.47/0.63 cnf(c39,plain,X53!=singleton(X52)|~in(X54,X53)|X54=X52,inference(split_conjunct,[status(thm)],[c38])).
% 0.47/0.63 cnf(c55,plain,~in(X55,singleton(X56))|X55=X56,inference(resolution,[status(thm)],[c39, reflexivity])).
% 0.47/0.63 cnf(c1,axiom,X46!=X45|X48!=X47|~in(X46,X48)|in(X45,X47),theory(equality)).
% 0.47/0.63 cnf(c40,plain,X58!=singleton(X57)|X59!=X57|in(X59,X58),inference(split_conjunct,[status(thm)],[c38])).
% 0.47/0.63 cnf(c56,plain,X64!=X65|in(X64,singleton(X65)),inference(resolution,[status(thm)],[c40, reflexivity])).
% 0.47/0.63 cnf(c60,plain,in(X66,singleton(X66)),inference(resolution,[status(thm)],[c56, reflexivity])).
% 0.47/0.63 cnf(c63,plain,X80!=X82|singleton(X80)!=X81|in(X82,X81),inference(resolution,[status(thm)],[c60, c1])).
% 0.47/0.63 fof(l1_zfmisc_1,axiom,(![A]:singleton(A)!=empty_set),file('/export/starexec/sandbox/benchmark/theBenchmark.p', l1_zfmisc_1)).
% 0.47/0.63 fof(c28,plain,(![X11]:singleton(X11)!=empty_set),inference(variable_rename,[status(thm)],[l1_zfmisc_1])).
% 0.47/0.63 cnf(c29,plain,singleton(X26)!=empty_set,inference(split_conjunct,[status(thm)],[c28])).
% 0.47/0.63 cnf(c8,negated_conjecture,subset(singleton(skolem0001),singleton(skolem0002)),inference(split_conjunct,[status(thm)],[c7])).
% 0.47/0.63 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.47/0.63 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.47/0.63 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.47/0.63 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.47/0.63 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.47/0.63 cnf(c25,plain,~subset(X73,singleton(X72))|X73=empty_set|X73=singleton(X72),inference(split_conjunct,[status(thm)],[c24])).
% 0.47/0.63 cnf(c66,plain,singleton(skolem0001)=empty_set|singleton(skolem0001)=singleton(skolem0002),inference(resolution,[status(thm)],[c25, c8])).
% 0.47/0.63 cnf(c112,plain,singleton(skolem0001)=singleton(skolem0002),inference(resolution,[status(thm)],[c66, c29])).
% 0.47/0.63 cnf(c138,plain,skolem0001!=X106|in(X106,singleton(skolem0002)),inference(resolution,[status(thm)],[c112, c63])).
% 0.47/0.63 cnf(c170,plain,in(skolem0001,singleton(skolem0002)),inference(resolution,[status(thm)],[c138, reflexivity])).
% 0.47/0.63 cnf(c173,plain,skolem0001=skolem0002,inference(resolution,[status(thm)],[c170, c55])).
% 0.47/0.63 cnf(c218,plain,$false,inference(resolution,[status(thm)],[c173, c9])).
% 0.47/0.63 % SZS output end CNFRefutation
% 0.47/0.63
% 0.47/0.63 % Initial clauses : 24
% 0.47/0.63 % Processed clauses : 47
% 0.47/0.63 % Factors computed : 4
% 0.47/0.63 % Resolvents computed: 177
% 0.47/0.63 % Tautologies deleted: 3
% 0.47/0.63 % Forward subsumed : 17
% 0.47/0.63 % Backward subsumed : 1
% 0.47/0.63 % -------- CPU Time ---------
% 0.47/0.63 % User time : 0.274 s
% 0.47/0.63 % System time : 0.019 s
% 0.47/0.63 % Total time : 0.293 s
%------------------------------------------------------------------------------