%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU151+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n019.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:40 EDT 2024
% Result : Theorem 0.48s 0.67s
% Output : Refutation 0.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SEU151+1 : TPTP v8.1.2. Released v3.3.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n019.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 10:52:53 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.48/0.67 % Version: 1.5
% 0.48/0.67 % SZS status Theorem
% 0.48/0.67 % SZS output start CNFRefutation
% 0.48/0.67 fof(t10_zfmisc_1,conjecture,(![A]:(![B]:(![C]:(![D]:(~((unordered_pair(A,B)=unordered_pair(C,D)&A!=C)&A!=D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t10_zfmisc_1)).
% 0.48/0.67 fof(c2,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(~((unordered_pair(A,B)=unordered_pair(C,D)&A!=C)&A!=D))))))),inference(assume_negation,[status(cth)],[t10_zfmisc_1])).
% 0.48/0.67 fof(c3,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:((unordered_pair(A,B)=unordered_pair(C,D)&A!=C)&A!=D))))),inference(fof_nnf,[status(thm)],[c2])).
% 0.48/0.67 fof(c4,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:((unordered_pair(X2,X3)=unordered_pair(X4,X5)&X2!=X4)&X2!=X5))))),inference(variable_rename,[status(thm)],[c3])).
% 0.48/0.67 fof(c5,negated_conjecture,((unordered_pair(skolem0001,skolem0002)=unordered_pair(skolem0003,skolem0004)&skolem0001!=skolem0003)&skolem0001!=skolem0004),inference(skolemize,[status(esa)],[c4])).
% 0.48/0.67 cnf(c7,negated_conjecture,skolem0001!=skolem0003,inference(split_conjunct,[status(thm)],[c5])).
% 0.48/0.67 cnf(c8,negated_conjecture,skolem0001!=skolem0004,inference(split_conjunct,[status(thm)],[c5])).
% 0.48/0.67 cnf(reflexivity,axiom,X19=X19,theory(equality)).
% 0.48/0.67 cnf(symmetry,axiom,X20!=X21|X21=X20,theory(equality)).
% 0.48/0.67 cnf(c6,negated_conjecture,unordered_pair(skolem0001,skolem0002)=unordered_pair(skolem0003,skolem0004),inference(split_conjunct,[status(thm)],[c5])).
% 0.48/0.67 cnf(transitivity,axiom,X22!=X23|X23!=X24|X22=X24,theory(equality)).
% 0.48/0.67 fof(commutativity_k2_tarski,axiom,(![A]:(![B]:unordered_pair(A,B)=unordered_pair(B,A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', commutativity_k2_tarski)).
% 0.48/0.67 fof(c22,plain,(![X15]:(![X16]:unordered_pair(X15,X16)=unordered_pair(X16,X15))),inference(variable_rename,[status(thm)],[commutativity_k2_tarski])).
% 0.48/0.67 cnf(c23,plain,unordered_pair(X36,X37)=unordered_pair(X37,X36),inference(split_conjunct,[status(thm)],[c22])).
% 0.48/0.67 cnf(c36,plain,X52!=unordered_pair(X53,X54)|X52=unordered_pair(X54,X53),inference(resolution,[status(thm)],[c23, transitivity])).
% 0.48/0.67 cnf(c47,plain,unordered_pair(skolem0001,skolem0002)=unordered_pair(skolem0004,skolem0003),inference(resolution,[status(thm)],[c36, c6])).
% 0.48/0.67 cnf(c61,plain,unordered_pair(skolem0004,skolem0003)=unordered_pair(skolem0001,skolem0002),inference(resolution,[status(thm)],[c47, symmetry])).
% 0.48/0.67 fof(d2_tarski,axiom,(![A]:(![B]:(![C]:(C=unordered_pair(A,B)<=>(![D]:(in(D,C)<=>(D=A|D=B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d2_tarski)).
% 0.48/0.67 fof(c10,plain,(![A]:(![B]:(![C]:((C!=unordered_pair(A,B)|(![D]:((~in(D,C)|(D=A|D=B))&((D!=A&D!=B)|in(D,C)))))&((?[D]:((~in(D,C)|(D!=A&D!=B))&(in(D,C)|(D=A|D=B))))|C=unordered_pair(A,B)))))),inference(fof_nnf,[status(thm)],[d2_tarski])).
% 0.48/0.67 fof(c11,plain,((![A]:(![B]:(![C]:(C!=unordered_pair(A,B)|((![D]:(~in(D,C)|(D=A|D=B)))&(![D]:((D!=A&D!=B)|in(D,C))))))))&(![A]:(![B]:(![C]:((?[D]:((~in(D,C)|(D!=A&D!=B))&(in(D,C)|(D=A|D=B))))|C=unordered_pair(A,B)))))),inference(shift_quantors,[status(thm)],[c10])).
% 0.48/0.67 fof(c12,plain,((![X6]:(![X7]:(![X8]:(X8!=unordered_pair(X6,X7)|((![X9]:(~in(X9,X8)|(X9=X6|X9=X7)))&(![X10]:((X10!=X6&X10!=X7)|in(X10,X8))))))))&(![X11]:(![X12]:(![X13]:((?[X14]:((~in(X14,X13)|(X14!=X11&X14!=X12))&(in(X14,X13)|(X14=X11|X14=X12))))|X13=unordered_pair(X11,X12)))))),inference(variable_rename,[status(thm)],[c11])).
% 0.48/0.67 fof(c14,plain,(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:((X8!=unordered_pair(X6,X7)|((~in(X9,X8)|(X9=X6|X9=X7))&((X10!=X6&X10!=X7)|in(X10,X8))))&(((~in(skolem0005(X11,X12,X13),X13)|(skolem0005(X11,X12,X13)!=X11&skolem0005(X11,X12,X13)!=X12))&(in(skolem0005(X11,X12,X13),X13)|(skolem0005(X11,X12,X13)=X11|skolem0005(X11,X12,X13)=X12)))|X13=unordered_pair(X11,X12))))))))))),inference(shift_quantors,[status(thm)],[fof(c13,plain,((![X6]:(![X7]:(![X8]:(X8!=unordered_pair(X6,X7)|((![X9]:(~in(X9,X8)|(X9=X6|X9=X7)))&(![X10]:((X10!=X6&X10!=X7)|in(X10,X8))))))))&(![X11]:(![X12]:(![X13]:(((~in(skolem0005(X11,X12,X13),X13)|(skolem0005(X11,X12,X13)!=X11&skolem0005(X11,X12,X13)!=X12))&(in(skolem0005(X11,X12,X13),X13)|(skolem0005(X11,X12,X13)=X11|skolem0005(X11,X12,X13)=X12)))|X13=unordered_pair(X11,X12)))))),inference(skolemize,[status(esa)],[c12])).])).
% 0.48/0.67 fof(c15,plain,(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(((X8!=unordered_pair(X6,X7)|(~in(X9,X8)|(X9=X6|X9=X7)))&((X8!=unordered_pair(X6,X7)|(X10!=X6|in(X10,X8)))&(X8!=unordered_pair(X6,X7)|(X10!=X7|in(X10,X8)))))&((((~in(skolem0005(X11,X12,X13),X13)|skolem0005(X11,X12,X13)!=X11)|X13=unordered_pair(X11,X12))&((~in(skolem0005(X11,X12,X13),X13)|skolem0005(X11,X12,X13)!=X12)|X13=unordered_pair(X11,X12)))&((in(skolem0005(X11,X12,X13),X13)|(skolem0005(X11,X12,X13)=X11|skolem0005(X11,X12,X13)=X12))|X13=unordered_pair(X11,X12)))))))))))),inference(distribute,[status(thm)],[c14])).
% 0.48/0.67 cnf(c17,plain,X64!=unordered_pair(X65,X63)|X66!=X65|in(X66,X64),inference(split_conjunct,[status(thm)],[c15])).
% 0.48/0.67 cnf(c82,plain,X114!=skolem0001|in(X114,unordered_pair(skolem0004,skolem0003)),inference(resolution,[status(thm)],[c17, c61])).
% 0.48/0.67 cnf(c192,plain,in(skolem0001,unordered_pair(skolem0004,skolem0003)),inference(resolution,[status(thm)],[c82, reflexivity])).
% 0.48/0.67 cnf(c16,plain,X61!=unordered_pair(X62,X60)|~in(X59,X61)|X59=X62|X59=X60,inference(split_conjunct,[status(thm)],[c15])).
% 0.48/0.67 cnf(c49,plain,~in(X146,unordered_pair(X147,X145))|X146=X147|X146=X145,inference(resolution,[status(thm)],[c16, reflexivity])).
% 0.48/0.67 cnf(c324,plain,skolem0001=skolem0004|skolem0001=skolem0003,inference(resolution,[status(thm)],[c49, c192])).
% 0.48/0.67 cnf(c402,plain,skolem0001=skolem0003,inference(resolution,[status(thm)],[c324, c8])).
% 0.48/0.67 cnf(c429,plain,$false,inference(resolution,[status(thm)],[c402, c7])).
% 0.48/0.67 % SZS output end CNFRefutation
% 0.48/0.67
% 0.48/0.67 % Initial clauses : 17
% 0.48/0.67 % Processed clauses : 76
% 0.48/0.67 % Factors computed : 4
% 0.48/0.67 % Resolvents computed: 404
% 0.48/0.67 % Tautologies deleted: 2
% 0.48/0.67 % Forward subsumed : 33
% 0.48/0.67 % Backward subsumed : 1
% 0.48/0.67 % -------- CPU Time ---------
% 0.48/0.67 % User time : 0.297 s
% 0.48/0.67 % System time : 0.014 s
% 0.48/0.67 % Total time : 0.311 s
%------------------------------------------------------------------------------