%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET867+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n021.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:16 EDT 2024
% Result : Theorem 0.60s 0.77s
% Output : Refutation 0.60s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : SET867+1 : TPTP v8.1.2. Released v3.2.0.
% 0.04/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.37 % Computer : n021.cluster.edu
% 0.15/0.37 % Model : x86_64 x86_64
% 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.37 % Memory : 8042.1875MB
% 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.37 % CPULimit : 300
% 0.15/0.37 % WCLimit : 300
% 0.15/0.37 % DateTime : Wed May 8 19:25:23 EDT 2024
% 0.15/0.37 % CPUTime :
% 0.60/0.77 % Version: 1.5
% 0.60/0.77 % SZS status Theorem
% 0.60/0.77 % SZS output start CNFRefutation
% 0.60/0.77 fof(t2_zfmisc_1,conjecture,union(empty_set)=empty_set,file('/export/starexec/sandbox/benchmark/theBenchmark.p', t2_zfmisc_1)).
% 0.60/0.77 fof(c3,negated_conjecture,(~union(empty_set)=empty_set),inference(assume_negation,[status(cth)],[t2_zfmisc_1])).
% 0.60/0.77 fof(c4,negated_conjecture,union(empty_set)!=empty_set,inference(fof_simplification,[status(thm)],[c3])).
% 0.60/0.77 cnf(c5,negated_conjecture,union(empty_set)!=empty_set,inference(split_conjunct,[status(thm)],[c4])).
% 0.60/0.77 cnf(symmetry,axiom,X23!=X22|X22=X23,theory(equality)).
% 0.60/0.77 cnf(reflexivity,axiom,X21=X21,theory(equality)).
% 0.60/0.77 fof(d1_xboole_0,axiom,(![A]:(A=empty_set<=>(![B]:(~in(B,A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', d1_xboole_0)).
% 0.60/0.77 fof(c26,plain,(![A]:(A=empty_set<=>(![B]:~in(B,A)))),inference(fof_simplification,[status(thm)],[d1_xboole_0])).
% 0.60/0.77 fof(c27,plain,(![A]:((A!=empty_set|(![B]:~in(B,A)))&((?[B]:in(B,A))|A=empty_set))),inference(fof_nnf,[status(thm)],[c26])).
% 0.60/0.77 fof(c28,plain,((![A]:(A!=empty_set|(![B]:~in(B,A))))&(![A]:((?[B]:in(B,A))|A=empty_set))),inference(shift_quantors,[status(thm)],[c27])).
% 0.60/0.77 fof(c29,plain,((![X15]:(X15!=empty_set|(![X16]:~in(X16,X15))))&(![X17]:((?[X18]:in(X18,X17))|X17=empty_set))),inference(variable_rename,[status(thm)],[c28])).
% 0.60/0.77 fof(c31,plain,(![X15]:(![X16]:(![X17]:((X15!=empty_set|~in(X16,X15))&(in(skolem0006(X17),X17)|X17=empty_set))))),inference(shift_quantors,[status(thm)],[fof(c30,plain,((![X15]:(X15!=empty_set|(![X16]:~in(X16,X15))))&(![X17]:(in(skolem0006(X17),X17)|X17=empty_set))),inference(skolemize,[status(esa)],[c29])).])).
% 0.60/0.77 cnf(c32,plain,X38!=empty_set|~in(X37,X38),inference(split_conjunct,[status(thm)],[c31])).
% 0.60/0.77 fof(d4_tarski,axiom,(![A]:(![B]:(B=union(A)<=>(![C]:(in(C,B)<=>(?[D]:(in(C,D)&in(D,A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', d4_tarski)).
% 0.60/0.77 fof(c14,plain,(![A]:(![B]:((B!=union(A)|(![C]:((~in(C,B)|(?[D]:(in(C,D)&in(D,A))))&((![D]:(~in(C,D)|~in(D,A)))|in(C,B)))))&((?[C]:((~in(C,B)|(![D]:(~in(C,D)|~in(D,A))))&(in(C,B)|(?[D]:(in(C,D)&in(D,A))))))|B=union(A))))),inference(fof_nnf,[status(thm)],[d4_tarski])).
% 0.60/0.77 fof(c15,plain,((![A]:(![B]:(B!=union(A)|((![C]:(~in(C,B)|(?[D]:(in(C,D)&in(D,A)))))&(![C]:((![D]:(~in(C,D)|~in(D,A)))|in(C,B)))))))&(![A]:(![B]:((?[C]:((~in(C,B)|(![D]:(~in(C,D)|~in(D,A))))&(in(C,B)|(?[D]:(in(C,D)&in(D,A))))))|B=union(A))))),inference(shift_quantors,[status(thm)],[c14])).
% 0.60/0.77 fof(c16,plain,((![X4]:(![X5]:(X5!=union(X4)|((![X6]:(~in(X6,X5)|(?[X7]:(in(X6,X7)&in(X7,X4)))))&(![X8]:((![X9]:(~in(X8,X9)|~in(X9,X4)))|in(X8,X5)))))))&(![X10]:(![X11]:((?[X12]:((~in(X12,X11)|(![X13]:(~in(X12,X13)|~in(X13,X10))))&(in(X12,X11)|(?[X14]:(in(X12,X14)&in(X14,X10))))))|X11=union(X10))))),inference(variable_rename,[status(thm)],[c15])).
% 0.60/0.77 fof(c18,plain,(![X4]:(![X5]:(![X6]:(![X8]:(![X9]:(![X10]:(![X11]:(![X13]:((X5!=union(X4)|((~in(X6,X5)|(in(X6,skolem0003(X4,X5,X6))&in(skolem0003(X4,X5,X6),X4)))&((~in(X8,X9)|~in(X9,X4))|in(X8,X5))))&(((~in(skolem0004(X10,X11),X11)|(~in(skolem0004(X10,X11),X13)|~in(X13,X10)))&(in(skolem0004(X10,X11),X11)|(in(skolem0004(X10,X11),skolem0005(X10,X11))&in(skolem0005(X10,X11),X10))))|X11=union(X10))))))))))),inference(shift_quantors,[status(thm)],[fof(c17,plain,((![X4]:(![X5]:(X5!=union(X4)|((![X6]:(~in(X6,X5)|(in(X6,skolem0003(X4,X5,X6))&in(skolem0003(X4,X5,X6),X4))))&(![X8]:((![X9]:(~in(X8,X9)|~in(X9,X4)))|in(X8,X5)))))))&(![X10]:(![X11]:(((~in(skolem0004(X10,X11),X11)|(![X13]:(~in(skolem0004(X10,X11),X13)|~in(X13,X10))))&(in(skolem0004(X10,X11),X11)|(in(skolem0004(X10,X11),skolem0005(X10,X11))&in(skolem0005(X10,X11),X10))))|X11=union(X10))))),inference(skolemize,[status(esa)],[c16])).])).
% 0.60/0.77 fof(c19,plain,(![X4]:(![X5]:(![X6]:(![X8]:(![X9]:(![X10]:(![X11]:(![X13]:((((X5!=union(X4)|(~in(X6,X5)|in(X6,skolem0003(X4,X5,X6))))&(X5!=union(X4)|(~in(X6,X5)|in(skolem0003(X4,X5,X6),X4))))&(X5!=union(X4)|((~in(X8,X9)|~in(X9,X4))|in(X8,X5))))&(((~in(skolem0004(X10,X11),X11)|(~in(skolem0004(X10,X11),X13)|~in(X13,X10)))|X11=union(X10))&(((in(skolem0004(X10,X11),X11)|in(skolem0004(X10,X11),skolem0005(X10,X11)))|X11=union(X10))&((in(skolem0004(X10,X11),X11)|in(skolem0005(X10,X11),X10))|X11=union(X10))))))))))))),inference(distribute,[status(thm)],[c18])).
% 0.60/0.77 cnf(c25,plain,in(skolem0004(X86,X85),X85)|in(skolem0005(X86,X85),X86)|X85=union(X86),inference(split_conjunct,[status(thm)],[c19])).
% 0.60/0.77 cnf(c128,plain,in(skolem0005(X181,X182),X181)|X182=union(X181)|X182!=empty_set,inference(resolution,[status(thm)],[c25, c32])).
% 0.60/0.77 cnf(c491,plain,in(skolem0005(X183,empty_set),X183)|empty_set=union(X183),inference(resolution,[status(thm)],[c128, reflexivity])).
% 0.60/0.77 cnf(c507,plain,empty_set=union(X184)|X184!=empty_set,inference(resolution,[status(thm)],[c491, c32])).
% 0.60/0.77 cnf(c523,plain,empty_set=union(empty_set),inference(resolution,[status(thm)],[c507, reflexivity])).
% 0.60/0.77 cnf(c566,plain,union(empty_set)=empty_set,inference(resolution,[status(thm)],[c523, symmetry])).
% 0.60/0.77 cnf(c576,plain,$false,inference(resolution,[status(thm)],[c566, c5])).
% 0.60/0.77 % SZS output end CNFRefutation
% 0.60/0.77
% 0.60/0.77 % Initial clauses : 19
% 0.60/0.77 % Processed clauses : 90
% 0.60/0.77 % Factors computed : 6
% 0.60/0.77 % Resolvents computed: 543
% 0.60/0.77 % Tautologies deleted: 4
% 0.60/0.77 % Forward subsumed : 40
% 0.60/0.77 % Backward subsumed : 1
% 0.60/0.77 % -------- CPU Time ---------
% 0.60/0.77 % User time : 0.380 s
% 0.60/0.77 % System time : 0.016 s
% 0.60/0.77 % Total time : 0.395 s
%------------------------------------------------------------------------------