%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU155+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n022.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:41 EDT 2024
% Result : Theorem 0.23s 0.57s
% Output : Refutation 0.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.14 % Problem : SEU155+1 : TPTP v8.1.2. Released v3.3.0.
% 0.10/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.37 % Computer : n022.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 12:06:38 EDT 2024
% 0.15/0.37 % CPUTime :
% 0.23/0.57 % Version: 1.5
% 0.23/0.57 % SZS status Theorem
% 0.23/0.57 % SZS output start CNFRefutation
% 0.23/0.57 fof(l50_zfmisc_1,conjecture,(![A]:(![B]:(in(A,B)=>subset(A,union(B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l50_zfmisc_1)).
% 0.23/0.57 fof(c6,negated_conjecture,(~(![A]:(![B]:(in(A,B)=>subset(A,union(B)))))),inference(assume_negation,[status(cth)],[l50_zfmisc_1])).
% 0.23/0.57 fof(c7,negated_conjecture,(?[A]:(?[B]:(in(A,B)&~subset(A,union(B))))),inference(fof_nnf,[status(thm)],[c6])).
% 0.23/0.57 fof(c8,negated_conjecture,(?[X3]:(?[X4]:(in(X3,X4)&~subset(X3,union(X4))))),inference(variable_rename,[status(thm)],[c7])).
% 0.23/0.57 fof(c9,negated_conjecture,(in(skolem0001,skolem0002)&~subset(skolem0001,union(skolem0002))),inference(skolemize,[status(esa)],[c8])).
% 0.23/0.57 cnf(c11,negated_conjecture,~subset(skolem0001,union(skolem0002)),inference(split_conjunct,[status(thm)],[c9])).
% 0.23/0.57 fof(d3_tarski,axiom,(![A]:(![B]:(subset(A,B)<=>(![C]:(in(C,A)=>in(C,B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d3_tarski)).
% 0.23/0.57 fof(c25,plain,(![A]:(![B]:((~subset(A,B)|(![C]:(~in(C,A)|in(C,B))))&((?[C]:(in(C,A)&~in(C,B)))|subset(A,B))))),inference(fof_nnf,[status(thm)],[d3_tarski])).
% 0.23/0.57 fof(c26,plain,((![A]:(![B]:(~subset(A,B)|(![C]:(~in(C,A)|in(C,B))))))&(![A]:(![B]:((?[C]:(in(C,A)&~in(C,B)))|subset(A,B))))),inference(shift_quantors,[status(thm)],[c25])).
% 0.23/0.57 fof(c27,plain,((![X16]:(![X17]:(~subset(X16,X17)|(![X18]:(~in(X18,X16)|in(X18,X17))))))&(![X19]:(![X20]:((?[X21]:(in(X21,X19)&~in(X21,X20)))|subset(X19,X20))))),inference(variable_rename,[status(thm)],[c26])).
% 0.23/0.57 fof(c29,plain,(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:((~subset(X16,X17)|(~in(X18,X16)|in(X18,X17)))&((in(skolem0006(X19,X20),X19)&~in(skolem0006(X19,X20),X20))|subset(X19,X20)))))))),inference(shift_quantors,[status(thm)],[fof(c28,plain,((![X16]:(![X17]:(~subset(X16,X17)|(![X18]:(~in(X18,X16)|in(X18,X17))))))&(![X19]:(![X20]:((in(skolem0006(X19,X20),X19)&~in(skolem0006(X19,X20),X20))|subset(X19,X20))))),inference(skolemize,[status(esa)],[c27])).])).
% 0.23/0.57 fof(c30,plain,(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:((~subset(X16,X17)|(~in(X18,X16)|in(X18,X17)))&((in(skolem0006(X19,X20),X19)|subset(X19,X20))&(~in(skolem0006(X19,X20),X20)|subset(X19,X20))))))))),inference(distribute,[status(thm)],[c29])).
% 0.23/0.57 cnf(c33,plain,~in(skolem0006(X44,X43),X43)|subset(X44,X43),inference(split_conjunct,[status(thm)],[c30])).
% 0.23/0.57 cnf(c32,plain,in(skolem0006(X42,X41),X42)|subset(X42,X41),inference(split_conjunct,[status(thm)],[c30])).
% 0.23/0.57 cnf(c45,plain,in(skolem0006(skolem0001,union(skolem0002)),skolem0001),inference(resolution,[status(thm)],[c32, c11])).
% 0.23/0.57 cnf(c10,negated_conjecture,in(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c9])).
% 0.23/0.57 cnf(reflexivity,axiom,X24=X24,theory(equality)).
% 0.23/0.57 fof(d4_tarski,axiom,(![A]:(![B]:(B=union(A)<=>(![C]:(in(C,B)<=>(?[D]:(in(C,D)&in(D,A)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d4_tarski)).
% 0.23/0.57 fof(c13,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.23/0.57 fof(c14,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)],[c13])).
% 0.23/0.57 fof(c15,plain,((![X5]:(![X6]:(X6!=union(X5)|((![X7]:(~in(X7,X6)|(?[X8]:(in(X7,X8)&in(X8,X5)))))&(![X9]:((![X10]:(~in(X9,X10)|~in(X10,X5)))|in(X9,X6)))))))&(![X11]:(![X12]:((?[X13]:((~in(X13,X12)|(![X14]:(~in(X13,X14)|~in(X14,X11))))&(in(X13,X12)|(?[X15]:(in(X13,X15)&in(X15,X11))))))|X12=union(X11))))),inference(variable_rename,[status(thm)],[c14])).
% 0.23/0.57 fof(c17,plain,(![X5]:(![X6]:(![X7]:(![X9]:(![X10]:(![X11]:(![X12]:(![X14]:((X6!=union(X5)|((~in(X7,X6)|(in(X7,skolem0003(X5,X6,X7))&in(skolem0003(X5,X6,X7),X5)))&((~in(X9,X10)|~in(X10,X5))|in(X9,X6))))&(((~in(skolem0004(X11,X12),X12)|(~in(skolem0004(X11,X12),X14)|~in(X14,X11)))&(in(skolem0004(X11,X12),X12)|(in(skolem0004(X11,X12),skolem0005(X11,X12))&in(skolem0005(X11,X12),X11))))|X12=union(X11))))))))))),inference(shift_quantors,[status(thm)],[fof(c16,plain,((![X5]:(![X6]:(X6!=union(X5)|((![X7]:(~in(X7,X6)|(in(X7,skolem0003(X5,X6,X7))&in(skolem0003(X5,X6,X7),X5))))&(![X9]:((![X10]:(~in(X9,X10)|~in(X10,X5)))|in(X9,X6)))))))&(![X11]:(![X12]:(((~in(skolem0004(X11,X12),X12)|(![X14]:(~in(skolem0004(X11,X12),X14)|~in(X14,X11))))&(in(skolem0004(X11,X12),X12)|(in(skolem0004(X11,X12),skolem0005(X11,X12))&in(skolem0005(X11,X12),X11))))|X12=union(X11))))),inference(skolemize,[status(esa)],[c15])).])).
% 0.23/0.57 fof(c18,plain,(![X5]:(![X6]:(![X7]:(![X9]:(![X10]:(![X11]:(![X12]:(![X14]:((((X6!=union(X5)|(~in(X7,X6)|in(X7,skolem0003(X5,X6,X7))))&(X6!=union(X5)|(~in(X7,X6)|in(skolem0003(X5,X6,X7),X5))))&(X6!=union(X5)|((~in(X9,X10)|~in(X10,X5))|in(X9,X6))))&(((~in(skolem0004(X11,X12),X12)|(~in(skolem0004(X11,X12),X14)|~in(X14,X11)))|X12=union(X11))&(((in(skolem0004(X11,X12),X12)|in(skolem0004(X11,X12),skolem0005(X11,X12)))|X12=union(X11))&((in(skolem0004(X11,X12),X12)|in(skolem0005(X11,X12),X11))|X12=union(X11))))))))))))),inference(distribute,[status(thm)],[c17])).
% 0.23/0.57 cnf(c21,plain,X81!=union(X82)|~in(X80,X79)|~in(X79,X82)|in(X80,X81),inference(split_conjunct,[status(thm)],[c18])).
% 0.23/0.57 cnf(c81,plain,~in(X87,X85)|~in(X85,X86)|in(X87,union(X86)),inference(resolution,[status(thm)],[c21, reflexivity])).
% 0.23/0.57 cnf(c86,plain,~in(X92,skolem0001)|in(X92,union(skolem0002)),inference(resolution,[status(thm)],[c81, c10])).
% 0.23/0.57 cnf(c93,plain,in(skolem0006(skolem0001,union(skolem0002)),union(skolem0002)),inference(resolution,[status(thm)],[c86, c45])).
% 0.23/0.57 cnf(c99,plain,subset(skolem0001,union(skolem0002)),inference(resolution,[status(thm)],[c93, c33])).
% 0.23/0.57 cnf(c100,plain,$false,inference(resolution,[status(thm)],[c99, c11])).
% 0.23/0.57 % SZS output end CNFRefutation
% 0.23/0.57
% 0.23/0.57 % Initial clauses : 20
% 0.23/0.57 % Processed clauses : 38
% 0.23/0.57 % Factors computed : 5
% 0.23/0.57 % Resolvents computed: 59
% 0.23/0.57 % Tautologies deleted: 2
% 0.23/0.57 % Forward subsumed : 11
% 0.23/0.57 % Backward subsumed : 0
% 0.23/0.57 % -------- CPU Time ---------
% 0.23/0.57 % User time : 0.181 s
% 0.23/0.57 % System time : 0.016 s
% 0.23/0.57 % Total time : 0.197 s
%------------------------------------------------------------------------------