%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET902+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n015.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:19 EDT 2024
% Result : Theorem 5.01s 5.21s
% Output : Refutation 5.01s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SET902+1 : TPTP v8.1.2. Released v3.2.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n015.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 18:35:08 EDT 2024
% 0.13/0.34 % CPUTime :
% 5.01/5.21 % Version: 1.5
% 5.01/5.21 % SZS status Theorem
% 5.01/5.21 % SZS output start CNFRefutation
% 5.01/5.21 fof(t43_zfmisc_1,conjecture,(![A]:(![B]:(![C]:(~(((singleton(A)=set_union2(B,C)&(~(B=singleton(A)&C=singleton(A))))&(~(B=empty_set&C=singleton(A))))&(~(B=singleton(A)&C=empty_set))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t43_zfmisc_1)).
% 5.01/5.21 fof(c6,negated_conjecture,(~(![A]:(![B]:(![C]:(~(((singleton(A)=set_union2(B,C)&(~(B=singleton(A)&C=singleton(A))))&(~(B=empty_set&C=singleton(A))))&(~(B=singleton(A)&C=empty_set)))))))),inference(assume_negation,[status(cth)],[t43_zfmisc_1])).
% 5.01/5.21 fof(c7,negated_conjecture,(?[A]:(?[B]:(?[C]:(((singleton(A)=set_union2(B,C)&(B!=singleton(A)|C!=singleton(A)))&(B!=empty_set|C!=singleton(A)))&(B!=singleton(A)|C!=empty_set))))),inference(fof_nnf,[status(thm)],[c6])).
% 5.01/5.21 fof(c8,negated_conjecture,(?[X4]:(?[X5]:(?[X6]:(((singleton(X4)=set_union2(X5,X6)&(X5!=singleton(X4)|X6!=singleton(X4)))&(X5!=empty_set|X6!=singleton(X4)))&(X5!=singleton(X4)|X6!=empty_set))))),inference(variable_rename,[status(thm)],[c7])).
% 5.01/5.21 fof(c9,negated_conjecture,(((singleton(skolem0001)=set_union2(skolem0002,skolem0003)&(skolem0002!=singleton(skolem0001)|skolem0003!=singleton(skolem0001)))&(skolem0002!=empty_set|skolem0003!=singleton(skolem0001)))&(skolem0002!=singleton(skolem0001)|skolem0003!=empty_set)),inference(skolemize,[status(esa)],[c8])).
% 5.01/5.21 cnf(c12,negated_conjecture,skolem0002!=empty_set|skolem0003!=singleton(skolem0001),inference(split_conjunct,[status(thm)],[c9])).
% 5.01/5.21 fof(l4_zfmisc_1,axiom,(![A]:(![B]:(subset(A,singleton(B))<=>(A=empty_set|A=singleton(B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l4_zfmisc_1)).
% 5.01/5.21 fof(c24,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])).
% 5.01/5.21 fof(c25,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)],[c24])).
% 5.01/5.21 fof(c27,plain,(![X10]:(![X11]:(![X12]:(![X13]:((~subset(X10,singleton(X11))|(X10=empty_set|X10=singleton(X11)))&((X12!=empty_set&X12!=singleton(X13))|subset(X12,singleton(X13)))))))),inference(shift_quantors,[status(thm)],[fof(c26,plain,((![X10]:(![X11]:(~subset(X10,singleton(X11))|(X10=empty_set|X10=singleton(X11)))))&(![X12]:(![X13]:((X12!=empty_set&X12!=singleton(X13))|subset(X12,singleton(X13)))))),inference(variable_rename,[status(thm)],[c25])).])).
% 5.01/5.21 fof(c28,plain,(![X10]:(![X11]:(![X12]:(![X13]:((~subset(X10,singleton(X11))|(X10=empty_set|X10=singleton(X11)))&((X12!=empty_set|subset(X12,singleton(X13)))&(X12!=singleton(X13)|subset(X12,singleton(X13))))))))),inference(distribute,[status(thm)],[c27])).
% 5.01/5.21 cnf(c29,plain,~subset(X93,singleton(X94))|X93=empty_set|X93=singleton(X94),inference(split_conjunct,[status(thm)],[c28])).
% 5.01/5.21 cnf(reflexivity,axiom,X22=X22,theory(equality)).
% 5.01/5.21 fof(t7_xboole_1,axiom,(![A]:(![B]:subset(A,set_union2(A,B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t7_xboole_1)).
% 5.01/5.21 fof(c4,plain,(![X2]:(![X3]:subset(X2,set_union2(X2,X3)))),inference(variable_rename,[status(thm)],[t7_xboole_1])).
% 5.01/5.21 cnf(c5,plain,subset(X27,set_union2(X27,X28)),inference(split_conjunct,[status(thm)],[c4])).
% 5.01/5.21 cnf(c3,axiom,X57!=X55|X54!=X56|~subset(X57,X54)|subset(X55,X56),theory(equality)).
% 5.01/5.21 cnf(c78,plain,X136!=X138|set_union2(X136,X137)!=X135|subset(X138,X135),inference(resolution,[status(thm)],[c3, c5])).
% 5.01/5.21 cnf(symmetry,axiom,X25!=X24|X24=X25,theory(equality)).
% 5.01/5.21 cnf(c10,negated_conjecture,singleton(skolem0001)=set_union2(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c9])).
% 5.01/5.21 cnf(transitivity,axiom,X33!=X32|X32!=X34|X33=X34,theory(equality)).
% 5.01/5.21 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)).
% 5.01/5.21 fof(c50,plain,(![X20]:(![X21]:set_union2(X20,X21)=set_union2(X21,X20))),inference(variable_rename,[status(thm)],[commutativity_k2_xboole_0])).
% 5.01/5.21 cnf(c51,plain,set_union2(X59,X60)=set_union2(X60,X59),inference(split_conjunct,[status(thm)],[c50])).
% 5.01/5.21 cnf(c82,plain,X173!=set_union2(X171,X172)|X173=set_union2(X172,X171),inference(resolution,[status(thm)],[c51, transitivity])).
% 5.01/5.21 cnf(c327,plain,singleton(skolem0001)=set_union2(skolem0003,skolem0002),inference(resolution,[status(thm)],[c82, c10])).
% 5.01/5.21 cnf(c472,plain,set_union2(skolem0003,skolem0002)=singleton(skolem0001),inference(resolution,[status(thm)],[c327, symmetry])).
% 5.01/5.21 cnf(c511,plain,skolem0003!=X222|subset(X222,singleton(skolem0001)),inference(resolution,[status(thm)],[c472, c78])).
% 5.01/5.21 cnf(c630,plain,subset(skolem0003,singleton(skolem0001)),inference(resolution,[status(thm)],[c511, reflexivity])).
% 5.01/5.21 cnf(c634,plain,skolem0003=empty_set|skolem0003=singleton(skolem0001),inference(resolution,[status(thm)],[c630, c29])).
% 5.01/5.21 cnf(c2261,plain,skolem0003=empty_set|skolem0002!=empty_set,inference(resolution,[status(thm)],[c634, c12])).
% 5.01/5.21 cnf(c88,plain,set_union2(skolem0002,skolem0003)=singleton(skolem0001),inference(resolution,[status(thm)],[c10, symmetry])).
% 5.01/5.21 cnf(c247,plain,skolem0002!=X167|subset(X167,singleton(skolem0001)),inference(resolution,[status(thm)],[c78, c88])).
% 5.01/5.21 cnf(c302,plain,subset(skolem0002,singleton(skolem0001)),inference(resolution,[status(thm)],[c247, reflexivity])).
% 5.01/5.21 cnf(c304,plain,skolem0002=empty_set|skolem0002=singleton(skolem0001),inference(resolution,[status(thm)],[c302, c29])).
% 5.01/5.21 cnf(c11,negated_conjecture,skolem0002!=singleton(skolem0001)|skolem0003!=singleton(skolem0001),inference(split_conjunct,[status(thm)],[c9])).
% 5.01/5.21 cnf(c2265,plain,skolem0003=empty_set|skolem0002!=singleton(skolem0001),inference(resolution,[status(thm)],[c634, c11])).
% 5.01/5.21 cnf(c4067,plain,skolem0003=empty_set|skolem0002=empty_set,inference(resolution,[status(thm)],[c2265, c304])).
% 5.01/5.21 cnf(c4136,plain,skolem0003=empty_set,inference(resolution,[status(thm)],[c4067, c2261])).
% 5.01/5.21 cnf(c13,negated_conjecture,skolem0002!=singleton(skolem0001)|skolem0003!=empty_set,inference(split_conjunct,[status(thm)],[c9])).
% 5.01/5.21 cnf(c187,plain,X616!=set_union2(skolem0002,skolem0003)|X616=singleton(skolem0001),inference(resolution,[status(thm)],[c88, transitivity])).
% 5.01/5.21 fof(idempotence_k2_xboole_0,axiom,(![A]:(![B]:set_union2(A,A)=A)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', idempotence_k2_xboole_0)).
% 5.01/5.21 fof(c34,plain,(![A]:set_union2(A,A)=A),inference(fof_simplification,[status(thm)],[idempotence_k2_xboole_0])).
% 5.01/5.21 fof(c35,plain,(![X15]:set_union2(X15,X15)=X15),inference(variable_rename,[status(thm)],[c34])).
% 5.01/5.21 cnf(c36,plain,set_union2(X30,X30)=X30,inference(split_conjunct,[status(thm)],[c35])).
% 5.01/5.21 cnf(c56,plain,X67!=set_union2(X66,X66)|X67=X66,inference(resolution,[status(thm)],[transitivity, c36])).
% 5.01/5.21 cnf(c0,axiom,X46!=X44|X43!=X45|set_union2(X46,X43)=set_union2(X44,X45),theory(equality)).
% 5.01/5.21 cnf(c62,plain,X122!=X123|set_union2(X122,X121)=set_union2(X123,X121),inference(resolution,[status(thm)],[c0, reflexivity])).
% 5.01/5.21 cnf(c1480,plain,skolem0002=empty_set|skolem0003!=empty_set,inference(resolution,[status(thm)],[c304, c13])).
% 5.01/5.21 cnf(c4087,plain,skolem0002=empty_set,inference(resolution,[status(thm)],[c4067, c1480])).
% 5.01/5.21 cnf(c4141,plain,empty_set=skolem0002,inference(resolution,[status(thm)],[c4087, symmetry])).
% 5.01/5.21 cnf(c4234,plain,X877!=empty_set|X877=skolem0002,inference(resolution,[status(thm)],[c4141, transitivity])).
% 5.01/5.21 cnf(c5015,plain,skolem0003=skolem0002,inference(resolution,[status(thm)],[c4234, c4136])).
% 5.01/5.21 cnf(c5084,plain,set_union2(skolem0003,X1404)=set_union2(skolem0002,X1404),inference(resolution,[status(thm)],[c5015, c62])).
% 5.01/5.21 cnf(c12753,plain,set_union2(skolem0003,skolem0002)=skolem0002,inference(resolution,[status(thm)],[c5084, c56])).
% 5.01/5.21 cnf(c12787,plain,skolem0002=set_union2(skolem0003,skolem0002),inference(resolution,[status(thm)],[c12753, symmetry])).
% 5.01/5.21 cnf(c12876,plain,skolem0002=set_union2(skolem0002,skolem0003),inference(resolution,[status(thm)],[c12787, c82])).
% 5.01/5.21 cnf(c13116,plain,skolem0002=singleton(skolem0001),inference(resolution,[status(thm)],[c12876, c187])).
% 5.01/5.21 cnf(c13166,plain,skolem0003!=empty_set,inference(resolution,[status(thm)],[c13116, c13])).
% 5.01/5.21 cnf(c13382,plain,$false,inference(resolution,[status(thm)],[c13166, c4136])).
% 5.01/5.21 % SZS output end CNFRefutation
% 5.01/5.21
% 5.01/5.21 % Initial clauses : 24
% 5.01/5.21 % Processed clauses : 541
% 5.01/5.21 % Factors computed : 6
% 5.01/5.21 % Resolvents computed: 13325
% 5.01/5.21 % Tautologies deleted: 4
% 5.01/5.21 % Forward subsumed : 1004
% 5.01/5.21 % Backward subsumed : 46
% 5.01/5.21 % -------- CPU Time ---------
% 5.01/5.21 % User time : 4.824 s
% 5.01/5.21 % System time : 0.036 s
% 5.01/5.21 % Total time : 4.860 s
%------------------------------------------------------------------------------