%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU140+2 : TPTP v8.1.2. Released v3.3.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:38 EDT 2024
% Result : Theorem 26.82s 27.01s
% Output : Refutation 26.82s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.14/0.14 % Problem : SEU140+2 : TPTP v8.1.2. Released v3.3.0.
% 0.14/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.16/0.37 % Computer : n029.cluster.edu
% 0.16/0.37 % Model : x86_64 x86_64
% 0.16/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.37 % Memory : 8042.1875MB
% 0.16/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.37 % CPULimit : 300
% 0.16/0.37 % WCLimit : 300
% 0.16/0.37 % DateTime : Wed May 8 12:03:23 EDT 2024
% 0.16/0.37 % CPUTime :
% 26.82/27.01 % Version: 1.5
% 26.82/27.01 % SZS status Theorem
% 26.82/27.01 % SZS output start CNFRefutation
% 26.82/27.01 fof(t63_xboole_1,conjecture,(![A]:(![B]:(![C]:((subset(A,B)&disjoint(B,C))=>disjoint(A,C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t63_xboole_1)).
% 26.82/27.01 fof(c22,negated_conjecture,(~(![A]:(![B]:(![C]:((subset(A,B)&disjoint(B,C))=>disjoint(A,C)))))),inference(assume_negation,[status(cth)],[t63_xboole_1])).
% 26.82/27.01 fof(c23,negated_conjecture,(?[A]:(?[B]:(?[C]:((subset(A,B)&disjoint(B,C))&~disjoint(A,C))))),inference(fof_nnf,[status(thm)],[c22])).
% 26.82/27.01 fof(c24,negated_conjecture,(?[X12]:(?[X13]:(?[X14]:((subset(X12,X13)&disjoint(X13,X14))&~disjoint(X12,X14))))),inference(variable_rename,[status(thm)],[c23])).
% 26.82/27.01 fof(c25,negated_conjecture,((subset(skolem0001,skolem0002)&disjoint(skolem0002,skolem0003))&~disjoint(skolem0001,skolem0003)),inference(skolemize,[status(esa)],[c24])).
% 26.82/27.01 cnf(c28,negated_conjecture,~disjoint(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c25])).
% 26.82/27.01 fof(t3_xboole_0,plain,(![A]:(![B]:((~((~disjoint(A,B))&(![C]:(~(in(C,A)&in(C,B))))))&(~((?[C]:(in(C,A)&in(C,B)))&disjoint(A,B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t3_xboole_0)).
% 26.82/27.01 fof(c52,plain,(![A]:(![B]:((~(~disjoint(A,B)&(![C]:(~(in(C,A)&in(C,B))))))&(~((?[C]:(in(C,A)&in(C,B)))&disjoint(A,B)))))),inference(fof_simplification,[status(thm)],[t3_xboole_0])).
% 26.82/27.01 fof(c53,plain,(![A]:(![B]:((disjoint(A,B)|(?[C]:(in(C,A)&in(C,B))))&((![C]:(~in(C,A)|~in(C,B)))|~disjoint(A,B))))),inference(fof_nnf,[status(thm)],[c52])).
% 26.82/27.01 fof(c54,plain,((![A]:(![B]:(disjoint(A,B)|(?[C]:(in(C,A)&in(C,B))))))&(![A]:(![B]:((![C]:(~in(C,A)|~in(C,B)))|~disjoint(A,B))))),inference(shift_quantors,[status(thm)],[c53])).
% 26.82/27.01 fof(c55,plain,((![X31]:(![X32]:(disjoint(X31,X32)|(?[X33]:(in(X33,X31)&in(X33,X32))))))&(![X34]:(![X35]:((![X36]:(~in(X36,X34)|~in(X36,X35)))|~disjoint(X34,X35))))),inference(variable_rename,[status(thm)],[c54])).
% 26.82/27.01 fof(c57,plain,(![X31]:(![X32]:(![X34]:(![X35]:(![X36]:((disjoint(X31,X32)|(in(skolem0005(X31,X32),X31)&in(skolem0005(X31,X32),X32)))&((~in(X36,X34)|~in(X36,X35))|~disjoint(X34,X35)))))))),inference(shift_quantors,[status(thm)],[fof(c56,plain,((![X31]:(![X32]:(disjoint(X31,X32)|(in(skolem0005(X31,X32),X31)&in(skolem0005(X31,X32),X32)))))&(![X34]:(![X35]:((![X36]:(~in(X36,X34)|~in(X36,X35)))|~disjoint(X34,X35))))),inference(skolemize,[status(esa)],[c55])).])).
% 26.82/27.01 fof(c58,plain,(![X31]:(![X32]:(![X34]:(![X35]:(![X36]:(((disjoint(X31,X32)|in(skolem0005(X31,X32),X31))&(disjoint(X31,X32)|in(skolem0005(X31,X32),X32)))&((~in(X36,X34)|~in(X36,X35))|~disjoint(X34,X35)))))))),inference(distribute,[status(thm)],[c57])).
% 26.82/27.01 cnf(c60,plain,disjoint(X293,X292)|in(skolem0005(X293,X292),X292),inference(split_conjunct,[status(thm)],[c58])).
% 26.82/27.01 cnf(c464,plain,in(skolem0005(skolem0001,skolem0003),skolem0003),inference(resolution,[status(thm)],[c60, c28])).
% 26.82/27.01 cnf(c27,negated_conjecture,disjoint(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c25])).
% 26.82/27.01 cnf(c61,plain,~in(X300,X302)|~in(X300,X301)|~disjoint(X302,X301),inference(split_conjunct,[status(thm)],[c58])).
% 26.82/27.01 cnf(c474,plain,~in(X1157,skolem0002)|~in(X1157,skolem0003),inference(resolution,[status(thm)],[c61, c27])).
% 26.82/27.01 cnf(c4355,plain,~in(skolem0005(skolem0001,skolem0003),skolem0002),inference(resolution,[status(thm)],[c474, c464])).
% 26.82/27.01 cnf(c59,plain,disjoint(X285,X284)|in(skolem0005(X285,X284),X285),inference(split_conjunct,[status(thm)],[c58])).
% 26.82/27.01 cnf(c446,plain,in(skolem0005(skolem0001,skolem0003),skolem0001),inference(resolution,[status(thm)],[c59, c28])).
% 26.82/27.01 fof(d2_xboole_0,axiom,(![A]:(![B]:(![C]:(C=set_union2(A,B)<=>(![D]:(in(D,C)<=>(in(D,A)|in(D,B)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d2_xboole_0)).
% 26.82/27.01 fof(c203,plain,(![A]:(![B]:(![C]:((C!=set_union2(A,B)|(![D]:((~in(D,C)|(in(D,A)|in(D,B)))&((~in(D,A)&~in(D,B))|in(D,C)))))&((?[D]:((~in(D,C)|(~in(D,A)&~in(D,B)))&(in(D,C)|(in(D,A)|in(D,B)))))|C=set_union2(A,B)))))),inference(fof_nnf,[status(thm)],[d2_xboole_0])).
% 26.82/27.01 fof(c204,plain,((![A]:(![B]:(![C]:(C!=set_union2(A,B)|((![D]:(~in(D,C)|(in(D,A)|in(D,B))))&(![D]:((~in(D,A)&~in(D,B))|in(D,C))))))))&(![A]:(![B]:(![C]:((?[D]:((~in(D,C)|(~in(D,A)&~in(D,B)))&(in(D,C)|(in(D,A)|in(D,B)))))|C=set_union2(A,B)))))),inference(shift_quantors,[status(thm)],[c203])).
% 26.82/27.01 fof(c205,plain,((![X118]:(![X119]:(![X120]:(X120!=set_union2(X118,X119)|((![X121]:(~in(X121,X120)|(in(X121,X118)|in(X121,X119))))&(![X122]:((~in(X122,X118)&~in(X122,X119))|in(X122,X120))))))))&(![X123]:(![X124]:(![X125]:((?[X126]:((~in(X126,X125)|(~in(X126,X123)&~in(X126,X124)))&(in(X126,X125)|(in(X126,X123)|in(X126,X124)))))|X125=set_union2(X123,X124)))))),inference(variable_rename,[status(thm)],[c204])).
% 26.82/27.01 fof(c207,plain,(![X118]:(![X119]:(![X120]:(![X121]:(![X122]:(![X123]:(![X124]:(![X125]:((X120!=set_union2(X118,X119)|((~in(X121,X120)|(in(X121,X118)|in(X121,X119)))&((~in(X122,X118)&~in(X122,X119))|in(X122,X120))))&(((~in(skolem0012(X123,X124,X125),X125)|(~in(skolem0012(X123,X124,X125),X123)&~in(skolem0012(X123,X124,X125),X124)))&(in(skolem0012(X123,X124,X125),X125)|(in(skolem0012(X123,X124,X125),X123)|in(skolem0012(X123,X124,X125),X124))))|X125=set_union2(X123,X124))))))))))),inference(shift_quantors,[status(thm)],[fof(c206,plain,((![X118]:(![X119]:(![X120]:(X120!=set_union2(X118,X119)|((![X121]:(~in(X121,X120)|(in(X121,X118)|in(X121,X119))))&(![X122]:((~in(X122,X118)&~in(X122,X119))|in(X122,X120))))))))&(![X123]:(![X124]:(![X125]:(((~in(skolem0012(X123,X124,X125),X125)|(~in(skolem0012(X123,X124,X125),X123)&~in(skolem0012(X123,X124,X125),X124)))&(in(skolem0012(X123,X124,X125),X125)|(in(skolem0012(X123,X124,X125),X123)|in(skolem0012(X123,X124,X125),X124))))|X125=set_union2(X123,X124)))))),inference(skolemize,[status(esa)],[c205])).])).
% 26.82/27.01 fof(c208,plain,(![X118]:(![X119]:(![X120]:(![X121]:(![X122]:(![X123]:(![X124]:(![X125]:(((X120!=set_union2(X118,X119)|(~in(X121,X120)|(in(X121,X118)|in(X121,X119))))&((X120!=set_union2(X118,X119)|(~in(X122,X118)|in(X122,X120)))&(X120!=set_union2(X118,X119)|(~in(X122,X119)|in(X122,X120)))))&((((~in(skolem0012(X123,X124,X125),X125)|~in(skolem0012(X123,X124,X125),X123))|X125=set_union2(X123,X124))&((~in(skolem0012(X123,X124,X125),X125)|~in(skolem0012(X123,X124,X125),X124))|X125=set_union2(X123,X124)))&((in(skolem0012(X123,X124,X125),X125)|(in(skolem0012(X123,X124,X125),X123)|in(skolem0012(X123,X124,X125),X124)))|X125=set_union2(X123,X124)))))))))))),inference(distribute,[status(thm)],[c207])).
% 26.82/27.01 cnf(c210,plain,X588!=set_union2(X591,X589)|~in(X590,X591)|in(X590,X588),inference(split_conjunct,[status(thm)],[c208])).
% 26.82/27.01 cnf(c26,negated_conjecture,subset(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c25])).
% 26.82/27.01 fof(t45_xboole_1,plain,(![A]:(![B]:(subset(A,B)=>B=set_union2(A,set_difference(B,A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t45_xboole_1)).
% 26.82/27.01 fof(c44,plain,(![A]:(![B]:(~subset(A,B)|B=set_union2(A,set_difference(B,A))))),inference(fof_nnf,[status(thm)],[t45_xboole_1])).
% 26.82/27.01 fof(c45,plain,(![X26]:(![X27]:(~subset(X26,X27)|X27=set_union2(X26,set_difference(X27,X26))))),inference(variable_rename,[status(thm)],[c44])).
% 26.82/27.01 cnf(c46,plain,~subset(X264,X263)|X263=set_union2(X264,set_difference(X263,X264)),inference(split_conjunct,[status(thm)],[c45])).
% 26.82/27.01 cnf(c412,plain,skolem0002=set_union2(skolem0001,set_difference(skolem0002,skolem0001)),inference(resolution,[status(thm)],[c46, c26])).
% 26.82/27.01 cnf(c7006,plain,~in(X3213,skolem0001)|in(X3213,skolem0002),inference(resolution,[status(thm)],[c412, c210])).
% 26.82/27.01 cnf(c22825,plain,in(skolem0005(skolem0001,skolem0003),skolem0002),inference(resolution,[status(thm)],[c7006, c446])).
% 26.82/27.01 cnf(c45175,plain,$false,inference(resolution,[status(thm)],[c22825, c4355])).
% 26.82/27.01 % SZS output end CNFRefutation
% 26.82/27.01
% 26.82/27.01 % Initial clauses : 98
% 26.82/27.01 % Processed clauses : 1069
% 26.82/27.01 % Factors computed : 84
% 26.82/27.01 % Resolvents computed: 44878
% 26.82/27.01 % Tautologies deleted: 46
% 26.82/27.01 % Forward subsumed : 2576
% 26.82/27.01 % Backward subsumed : 62
% 26.82/27.01 % -------- CPU Time ---------
% 26.82/27.01 % User time : 26.545 s
% 26.82/27.01 % System time : 0.095 s
% 26.82/27.01 % Total time : 26.640 s
%------------------------------------------------------------------------------