%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET873+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n017.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:17 EDT 2024
% Result : Theorem 3.35s 3.55s
% Output : Refutation 3.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : SET873+1 : TPTP v8.1.2. Released v3.2.0.
% 0.12/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n017.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 18:24:23 EDT 2024
% 0.14/0.35 % CPUTime :
% 3.35/3.55 % Version: 1.5
% 3.35/3.55 % SZS status Theorem
% 3.35/3.55 % SZS output start CNFRefutation
% 3.35/3.55 fof(t13_zfmisc_1,conjecture,(![A]:(![B]:(set_union2(singleton(A),singleton(B))=singleton(A)=>A=B))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t13_zfmisc_1)).
% 3.35/3.55 fof(c5,negated_conjecture,(~(![A]:(![B]:(set_union2(singleton(A),singleton(B))=singleton(A)=>A=B)))),inference(assume_negation,[status(cth)],[t13_zfmisc_1])).
% 3.35/3.55 fof(c6,negated_conjecture,(?[A]:(?[B]:(set_union2(singleton(A),singleton(B))=singleton(A)&A!=B))),inference(fof_nnf,[status(thm)],[c5])).
% 3.35/3.55 fof(c7,negated_conjecture,(?[X2]:(?[X3]:(set_union2(singleton(X2),singleton(X3))=singleton(X2)&X2!=X3))),inference(variable_rename,[status(thm)],[c6])).
% 3.35/3.55 fof(c8,negated_conjecture,(set_union2(singleton(skolem0001),singleton(skolem0002))=singleton(skolem0001)&skolem0001!=skolem0002),inference(skolemize,[status(esa)],[c7])).
% 3.35/3.55 cnf(c10,negated_conjecture,skolem0001!=skolem0002,inference(split_conjunct,[status(thm)],[c8])).
% 3.35/3.55 cnf(symmetry,axiom,X28!=X27|X27=X28,theory(equality)).
% 3.35/3.55 cnf(reflexivity,axiom,X25=X25,theory(equality)).
% 3.35/3.55 fof(d1_tarski,axiom,(![A]:(![B]:(B=singleton(A)<=>(![C]:(in(C,B)<=>C=A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_tarski)).
% 3.35/3.55 fof(c39,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])).
% 3.35/3.55 fof(c40,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)],[c39])).
% 3.35/3.55 fof(c41,plain,((![X14]:(![X15]:(X15!=singleton(X14)|((![X16]:(~in(X16,X15)|X16=X14))&(![X17]:(X17!=X14|in(X17,X15)))))))&(![X18]:(![X19]:((?[X20]:((~in(X20,X19)|X20!=X18)&(in(X20,X19)|X20=X18)))|X19=singleton(X18))))),inference(variable_rename,[status(thm)],[c40])).
% 3.35/3.55 fof(c43,plain,(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:((X15!=singleton(X14)|((~in(X16,X15)|X16=X14)&(X17!=X14|in(X17,X15))))&(((~in(skolem0005(X18,X19),X19)|skolem0005(X18,X19)!=X18)&(in(skolem0005(X18,X19),X19)|skolem0005(X18,X19)=X18))|X19=singleton(X18))))))))),inference(shift_quantors,[status(thm)],[fof(c42,plain,((![X14]:(![X15]:(X15!=singleton(X14)|((![X16]:(~in(X16,X15)|X16=X14))&(![X17]:(X17!=X14|in(X17,X15)))))))&(![X18]:(![X19]:(((~in(skolem0005(X18,X19),X19)|skolem0005(X18,X19)!=X18)&(in(skolem0005(X18,X19),X19)|skolem0005(X18,X19)=X18))|X19=singleton(X18))))),inference(skolemize,[status(esa)],[c41])).])).
% 3.35/3.55 fof(c44,plain,(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(((X15!=singleton(X14)|(~in(X16,X15)|X16=X14))&(X15!=singleton(X14)|(X17!=X14|in(X17,X15))))&(((~in(skolem0005(X18,X19),X19)|skolem0005(X18,X19)!=X18)|X19=singleton(X18))&((in(skolem0005(X18,X19),X19)|skolem0005(X18,X19)=X18)|X19=singleton(X18)))))))))),inference(distribute,[status(thm)],[c43])).
% 3.35/3.55 cnf(c45,plain,X100!=singleton(X99)|~in(X98,X100)|X98=X99,inference(split_conjunct,[status(thm)],[c44])).
% 3.35/3.55 cnf(c134,plain,~in(X104,singleton(X105))|X104=X105,inference(resolution,[status(thm)],[c45, reflexivity])).
% 3.35/3.55 fof(l21_zfmisc_1,axiom,(![A]:(![B]:(subset(set_union2(singleton(A),B),B)=>in(A,B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l21_zfmisc_1)).
% 3.35/3.55 fof(c21,plain,(![A]:(![B]:(~subset(set_union2(singleton(A),B),B)|in(A,B)))),inference(fof_nnf,[status(thm)],[l21_zfmisc_1])).
% 3.35/3.55 fof(c22,plain,(![X7]:(![X8]:(~subset(set_union2(singleton(X7),X8),X8)|in(X7,X8)))),inference(variable_rename,[status(thm)],[c21])).
% 3.35/3.55 cnf(c23,plain,~subset(set_union2(singleton(X90),X91),X91)|in(X90,X91),inference(split_conjunct,[status(thm)],[c22])).
% 3.35/3.55 fof(commutativity_k2_xboole_0,axiom,(![A]:(![B]:set_union2(A,B)=set_union2(B,A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', commutativity_k2_xboole_0)).
% 3.35/3.55 fof(c49,plain,(![X21]:(![X22]:set_union2(X21,X22)=set_union2(X22,X21))),inference(variable_rename,[status(thm)],[commutativity_k2_xboole_0])).
% 3.35/3.55 cnf(c50,plain,set_union2(X58,X59)=set_union2(X59,X58),inference(split_conjunct,[status(thm)],[c49])).
% 3.35/3.55 cnf(c9,negated_conjecture,set_union2(singleton(skolem0001),singleton(skolem0002))=singleton(skolem0001),inference(split_conjunct,[status(thm)],[c8])).
% 3.35/3.55 fof(reflexivity_r1_tarski,axiom,(![A]:(![B]:subset(A,A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', reflexivity_r1_tarski)).
% 3.35/3.55 fof(c11,plain,(![A]:subset(A,A)),inference(fof_simplification,[status(thm)],[reflexivity_r1_tarski])).
% 3.35/3.55 fof(c12,plain,(![X4]:subset(X4,X4)),inference(variable_rename,[status(thm)],[c11])).
% 3.35/3.55 cnf(c13,plain,subset(X26,X26),inference(split_conjunct,[status(thm)],[c12])).
% 3.35/3.55 cnf(c4,axiom,X75!=X74|X73!=X76|~subset(X75,X73)|subset(X74,X76),theory(equality)).
% 3.35/3.55 cnf(c90,plain,X86!=X85|X86!=X87|subset(X85,X87),inference(resolution,[status(thm)],[c4, c13])).
% 3.35/3.55 cnf(c116,plain,set_union2(singleton(skolem0001),singleton(skolem0002))!=X322|subset(X322,singleton(skolem0001)),inference(resolution,[status(thm)],[c90, c9])).
% 3.35/3.55 cnf(c914,plain,subset(set_union2(singleton(skolem0002),singleton(skolem0001)),singleton(skolem0001)),inference(resolution,[status(thm)],[c116, c50])).
% 3.35/3.55 cnf(c9802,plain,in(skolem0002,singleton(skolem0001)),inference(resolution,[status(thm)],[c914, c23])).
% 3.35/3.55 cnf(c9855,plain,skolem0002=skolem0001,inference(resolution,[status(thm)],[c9802, c134])).
% 3.35/3.55 cnf(c9876,plain,skolem0001=skolem0002,inference(resolution,[status(thm)],[c9855, symmetry])).
% 3.35/3.55 cnf(c9945,plain,$false,inference(resolution,[status(thm)],[c9876, c10])).
% 3.35/3.55 % SZS output end CNFRefutation
% 3.35/3.55
% 3.35/3.55 % Initial clauses : 23
% 3.35/3.55 % Processed clauses : 385
% 3.35/3.55 % Factors computed : 11
% 3.35/3.55 % Resolvents computed: 9881
% 3.35/3.55 % Tautologies deleted: 4
% 3.35/3.55 % Forward subsumed : 623
% 3.35/3.55 % Backward subsumed : 3
% 3.35/3.55 % -------- CPU Time ---------
% 3.35/3.55 % User time : 3.136 s
% 3.35/3.55 % System time : 0.033 s
% 3.35/3.55 % Total time : 3.169 s
%------------------------------------------------------------------------------