%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU146+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n018.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 4.28s 4.54s
% Output : Refutation 4.28s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SEU146+1 : TPTP v8.1.2. Released v3.3.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n018.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 10:52:38 EDT 2024
% 0.13/0.34 % CPUTime :
% 4.28/4.54 % Version: 1.5
% 4.28/4.54 % SZS status Theorem
% 4.28/4.54 % SZS output start CNFRefutation
% 4.28/4.54 cnf(reflexivity,axiom,X26=X26,theory(equality)).
% 4.28/4.54 fof(t2_xboole_1,axiom,(![A]:subset(empty_set,A)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t2_xboole_1)).
% 4.28/4.54 fof(c14,plain,(![X7]:subset(empty_set,X7)),inference(variable_rename,[status(thm)],[t2_xboole_1])).
% 4.28/4.54 cnf(c15,plain,subset(empty_set,X31),inference(split_conjunct,[status(thm)],[c14])).
% 4.28/4.54 cnf(c3,axiom,X71!=X72|X74!=X73|~subset(X71,X74)|subset(X72,X73),theory(equality)).
% 4.28/4.54 cnf(c77,plain,empty_set!=X142|X143!=X144|subset(X142,X144),inference(resolution,[status(thm)],[c3, c15])).
% 4.28/4.54 cnf(c216,plain,empty_set!=X146|subset(X146,X147),inference(resolution,[status(thm)],[c77, reflexivity])).
% 4.28/4.54 fof(d10_xboole_0,axiom,(![A]:(![B]:(A=B<=>(subset(A,B)&subset(B,A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d10_xboole_0)).
% 4.28/4.54 fof(c49,plain,(![A]:(![B]:((A!=B|(subset(A,B)&subset(B,A)))&((~subset(A,B)|~subset(B,A))|A=B)))),inference(fof_nnf,[status(thm)],[d10_xboole_0])).
% 4.28/4.54 fof(c50,plain,((![A]:(![B]:(A!=B|(subset(A,B)&subset(B,A)))))&(![A]:(![B]:((~subset(A,B)|~subset(B,A))|A=B)))),inference(shift_quantors,[status(thm)],[c49])).
% 4.28/4.54 fof(c52,plain,(![X20]:(![X21]:(![X22]:(![X23]:((X20!=X21|(subset(X20,X21)&subset(X21,X20)))&((~subset(X22,X23)|~subset(X23,X22))|X22=X23)))))),inference(shift_quantors,[status(thm)],[fof(c51,plain,((![X20]:(![X21]:(X20!=X21|(subset(X20,X21)&subset(X21,X20)))))&(![X22]:(![X23]:((~subset(X22,X23)|~subset(X23,X22))|X22=X23)))),inference(variable_rename,[status(thm)],[c50])).])).
% 4.28/4.54 fof(c53,plain,(![X20]:(![X21]:(![X22]:(![X23]:(((X20!=X21|subset(X20,X21))&(X20!=X21|subset(X21,X20)))&((~subset(X22,X23)|~subset(X23,X22))|X22=X23)))))),inference(distribute,[status(thm)],[c52])).
% 4.28/4.54 cnf(c54,plain,X35!=X36|subset(X35,X36),inference(split_conjunct,[status(thm)],[c53])).
% 4.28/4.54 cnf(symmetry,axiom,X28!=X29|X29=X28,theory(equality)).
% 4.28/4.54 fof(l4_zfmisc_1,conjecture,(![A]:(![B]:(subset(A,singleton(B))<=>(A=empty_set|A=singleton(B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l4_zfmisc_1)).
% 4.28/4.54 fof(c26,negated_conjecture,(~(![A]:(![B]:(subset(A,singleton(B))<=>(A=empty_set|A=singleton(B)))))),inference(assume_negation,[status(cth)],[l4_zfmisc_1])).
% 4.28/4.54 fof(c27,negated_conjecture,(?[A]:(?[B]:((~subset(A,singleton(B))|(A!=empty_set&A!=singleton(B)))&(subset(A,singleton(B))|(A=empty_set|A=singleton(B)))))),inference(fof_nnf,[status(thm)],[c26])).
% 4.28/4.54 fof(c28,negated_conjecture,(?[X11]:(?[X12]:((~subset(X11,singleton(X12))|(X11!=empty_set&X11!=singleton(X12)))&(subset(X11,singleton(X12))|(X11=empty_set|X11=singleton(X12)))))),inference(variable_rename,[status(thm)],[c27])).
% 4.28/4.54 fof(c29,negated_conjecture,((~subset(skolem0003,singleton(skolem0004))|(skolem0003!=empty_set&skolem0003!=singleton(skolem0004)))&(subset(skolem0003,singleton(skolem0004))|(skolem0003=empty_set|skolem0003=singleton(skolem0004)))),inference(skolemize,[status(esa)],[c28])).
% 4.28/4.54 fof(c30,negated_conjecture,(((~subset(skolem0003,singleton(skolem0004))|skolem0003!=empty_set)&(~subset(skolem0003,singleton(skolem0004))|skolem0003!=singleton(skolem0004)))&(subset(skolem0003,singleton(skolem0004))|(skolem0003=empty_set|skolem0003=singleton(skolem0004)))),inference(distribute,[status(thm)],[c29])).
% 4.28/4.54 cnf(c33,negated_conjecture,subset(skolem0003,singleton(skolem0004))|skolem0003=empty_set|skolem0003=singleton(skolem0004),inference(split_conjunct,[status(thm)],[c30])).
% 4.28/4.54 cnf(c120,plain,subset(skolem0003,singleton(skolem0004))|skolem0003=singleton(skolem0004)|empty_set=skolem0003,inference(resolution,[status(thm)],[c33, symmetry])).
% 4.28/4.54 cnf(c553,plain,subset(skolem0003,singleton(skolem0004))|empty_set=skolem0003,inference(resolution,[status(thm)],[c120, c54])).
% 4.28/4.54 cnf(c1563,plain,subset(skolem0003,singleton(skolem0004))|subset(skolem0003,X640),inference(resolution,[status(thm)],[c553, c216])).
% 4.28/4.54 cnf(c1580,plain,subset(skolem0003,singleton(skolem0004)),inference(factor,[status(thm)],[c1563])).
% 4.28/4.54 cnf(c32,negated_conjecture,~subset(skolem0003,singleton(skolem0004))|skolem0003!=singleton(skolem0004),inference(split_conjunct,[status(thm)],[c30])).
% 4.28/4.54 cnf(c56,plain,~subset(X105,X104)|~subset(X104,X105)|X105=X104,inference(split_conjunct,[status(thm)],[c53])).
% 4.28/4.54 cnf(c1597,plain,~subset(singleton(skolem0004),skolem0003)|singleton(skolem0004)=skolem0003,inference(resolution,[status(thm)],[c1580, c56])).
% 4.28/4.54 fof(l2_zfmisc_1,axiom,(![A]:(![B]:(subset(singleton(A),B)<=>in(A,B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l2_zfmisc_1)).
% 4.28/4.54 fof(c39,plain,(![A]:(![B]:((~subset(singleton(A),B)|in(A,B))&(~in(A,B)|subset(singleton(A),B))))),inference(fof_nnf,[status(thm)],[l2_zfmisc_1])).
% 4.28/4.54 fof(c40,plain,((![A]:(![B]:(~subset(singleton(A),B)|in(A,B))))&(![A]:(![B]:(~in(A,B)|subset(singleton(A),B))))),inference(shift_quantors,[status(thm)],[c39])).
% 4.28/4.54 fof(c42,plain,(![X16]:(![X17]:(![X18]:(![X19]:((~subset(singleton(X16),X17)|in(X16,X17))&(~in(X18,X19)|subset(singleton(X18),X19))))))),inference(shift_quantors,[status(thm)],[fof(c41,plain,((![X16]:(![X17]:(~subset(singleton(X16),X17)|in(X16,X17))))&(![X18]:(![X19]:(~in(X18,X19)|subset(singleton(X18),X19))))),inference(variable_rename,[status(thm)],[c40])).])).
% 4.28/4.54 cnf(c44,plain,~in(X67,X66)|subset(singleton(X67),X66),inference(split_conjunct,[status(thm)],[c42])).
% 4.28/4.54 cnf(c31,negated_conjecture,~subset(skolem0003,singleton(skolem0004))|skolem0003!=empty_set,inference(split_conjunct,[status(thm)],[c30])).
% 4.28/4.54 cnf(c1594,plain,skolem0003!=empty_set,inference(resolution,[status(thm)],[c1580, c31])).
% 4.28/4.54 fof(t3_xboole_1,axiom,(![A]:(subset(A,empty_set)=>A=empty_set)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t3_xboole_1)).
% 4.28/4.54 fof(c5,plain,(![A]:(~subset(A,empty_set)|A=empty_set)),inference(fof_nnf,[status(thm)],[t3_xboole_1])).
% 4.28/4.54 fof(c6,plain,(![X2]:(~subset(X2,empty_set)|X2=empty_set)),inference(variable_rename,[status(thm)],[c5])).
% 4.28/4.54 cnf(c7,plain,~subset(X57,empty_set)|X57=empty_set,inference(split_conjunct,[status(thm)],[c6])).
% 4.28/4.54 fof(t37_xboole_1,axiom,(![A]:(![B]:(set_difference(A,B)=empty_set<=>subset(A,B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t37_xboole_1)).
% 4.28/4.54 fof(c8,plain,(![A]:(![B]:((set_difference(A,B)!=empty_set|subset(A,B))&(~subset(A,B)|set_difference(A,B)=empty_set)))),inference(fof_nnf,[status(thm)],[t37_xboole_1])).
% 4.28/4.54 fof(c9,plain,((![A]:(![B]:(set_difference(A,B)!=empty_set|subset(A,B))))&(![A]:(![B]:(~subset(A,B)|set_difference(A,B)=empty_set)))),inference(shift_quantors,[status(thm)],[c8])).
% 4.28/4.54 fof(c11,plain,(![X3]:(![X4]:(![X5]:(![X6]:((set_difference(X3,X4)!=empty_set|subset(X3,X4))&(~subset(X5,X6)|set_difference(X5,X6)=empty_set)))))),inference(shift_quantors,[status(thm)],[fof(c10,plain,((![X3]:(![X4]:(set_difference(X3,X4)!=empty_set|subset(X3,X4))))&(![X5]:(![X6]:(~subset(X5,X6)|set_difference(X5,X6)=empty_set)))),inference(variable_rename,[status(thm)],[c9])).])).
% 4.28/4.54 cnf(c13,plain,~subset(X76,X75)|set_difference(X76,X75)=empty_set,inference(split_conjunct,[status(thm)],[c11])).
% 4.28/4.54 cnf(c1595,plain,set_difference(skolem0003,singleton(skolem0004))=empty_set,inference(resolution,[status(thm)],[c1580, c13])).
% 4.28/4.54 fof(reflexivity_r1_tarski,axiom,(![A]:(![B]:subset(A,A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', reflexivity_r1_tarski)).
% 4.28/4.54 fof(c16,plain,(![A]:subset(A,A)),inference(fof_simplification,[status(thm)],[reflexivity_r1_tarski])).
% 4.28/4.54 fof(c17,plain,(![X8]:subset(X8,X8)),inference(variable_rename,[status(thm)],[c16])).
% 4.28/4.54 cnf(c18,plain,subset(X27,X27),inference(split_conjunct,[status(thm)],[c17])).
% 4.28/4.54 fof(l3_zfmisc_1,axiom,(![A]:(![B]:(![C]:(subset(A,B)=>(in(C,A)|subset(A,set_difference(B,singleton(C)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l3_zfmisc_1)).
% 4.28/4.54 fof(c34,plain,(![A]:(![B]:(![C]:(~subset(A,B)|(in(C,A)|subset(A,set_difference(B,singleton(C)))))))),inference(fof_nnf,[status(thm)],[l3_zfmisc_1])).
% 4.28/4.54 fof(c35,plain,(![A]:(![B]:(~subset(A,B)|(![C]:(in(C,A)|subset(A,set_difference(B,singleton(C)))))))),inference(shift_quantors,[status(thm)],[c34])).
% 4.28/4.54 fof(c37,plain,(![X13]:(![X14]:(![X15]:(~subset(X13,X14)|(in(X15,X13)|subset(X13,set_difference(X14,singleton(X15)))))))),inference(shift_quantors,[status(thm)],[fof(c36,plain,(![X13]:(![X14]:(~subset(X13,X14)|(![X15]:(in(X15,X13)|subset(X13,set_difference(X14,singleton(X15)))))))),inference(variable_rename,[status(thm)],[c35])).])).
% 4.28/4.54 cnf(c38,plain,~subset(X98,X96)|in(X97,X98)|subset(X98,set_difference(X96,singleton(X97))),inference(split_conjunct,[status(thm)],[c37])).
% 4.28/4.54 cnf(c138,plain,in(X326,X325)|subset(X325,set_difference(X325,singleton(X326))),inference(resolution,[status(thm)],[c38, c18])).
% 4.28/4.54 cnf(c636,plain,in(X3400,X3402)|X3402!=X3399|set_difference(X3402,singleton(X3400))!=X3401|subset(X3399,X3401),inference(resolution,[status(thm)],[c138, c3])).
% 4.28/4.54 cnf(c7746,plain,in(skolem0004,skolem0003)|skolem0003!=X3725|subset(X3725,empty_set),inference(resolution,[status(thm)],[c636, c1595])).
% 4.28/4.54 cnf(c8667,plain,in(skolem0004,skolem0003)|subset(skolem0003,empty_set),inference(resolution,[status(thm)],[c7746, reflexivity])).
% 4.28/4.54 cnf(c8681,plain,in(skolem0004,skolem0003)|skolem0003=empty_set,inference(resolution,[status(thm)],[c8667, c7])).
% 4.28/4.54 cnf(c8720,plain,in(skolem0004,skolem0003),inference(resolution,[status(thm)],[c8681, c1594])).
% 4.28/4.54 cnf(c8734,plain,subset(singleton(skolem0004),skolem0003),inference(resolution,[status(thm)],[c8720, c44])).
% 4.28/4.54 cnf(c8742,plain,singleton(skolem0004)=skolem0003,inference(resolution,[status(thm)],[c8734, c1597])).
% 4.28/4.54 cnf(c8753,plain,skolem0003=singleton(skolem0004),inference(resolution,[status(thm)],[c8742, symmetry])).
% 4.28/4.54 cnf(c8793,plain,~subset(skolem0003,singleton(skolem0004)),inference(resolution,[status(thm)],[c8753, c32])).
% 4.28/4.54 cnf(c8811,plain,$false,inference(resolution,[status(thm)],[c8793, c1580])).
% 4.28/4.54 % SZS output end CNFRefutation
% 4.28/4.54
% 4.28/4.54 % Initial clauses : 29
% 4.28/4.54 % Processed clauses : 473
% 4.28/4.54 % Factors computed : 13
% 4.28/4.54 % Resolvents computed: 8738
% 4.28/4.54 % Tautologies deleted: 8
% 4.28/4.54 % Forward subsumed : 1778
% 4.28/4.54 % Backward subsumed : 97
% 4.28/4.54 % -------- CPU Time ---------
% 4.28/4.54 % User time : 4.068 s
% 4.28/4.54 % System time : 0.030 s
% 4.28/4.54 % Total time : 4.098 s
%------------------------------------------------------------------------------