%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU165+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n005.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:44 EDT 2024
% Result : Theorem 0.38s 0.62s
% Output : Refutation 0.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : SEU165+1 : TPTP v8.1.2. Released v3.3.0.
% 0.04/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n005.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Wed May 8 12:00:38 EDT 2024
% 0.15/0.36 % CPUTime :
% 0.38/0.62 % Version: 1.5
% 0.38/0.62 % SZS status Theorem
% 0.38/0.62 % SZS output start CNFRefutation
% 0.38/0.62 fof(l55_zfmisc_1,axiom,(![A]:(![B]:(![C]:(![D]:(in(ordered_pair(A,B),cartesian_product2(C,D))<=>(in(A,C)&in(B,D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l55_zfmisc_1)).
% 0.38/0.62 fof(c6,plain,(![A]:(![B]:(![C]:(![D]:((~in(ordered_pair(A,B),cartesian_product2(C,D))|(in(A,C)&in(B,D)))&((~in(A,C)|~in(B,D))|in(ordered_pair(A,B),cartesian_product2(C,D)))))))),inference(fof_nnf,[status(thm)],[l55_zfmisc_1])).
% 0.38/0.62 fof(c7,plain,((![A]:(![B]:(![C]:(![D]:(~in(ordered_pair(A,B),cartesian_product2(C,D))|(in(A,C)&in(B,D)))))))&(![A]:(![B]:(![C]:(![D]:((~in(A,C)|~in(B,D))|in(ordered_pair(A,B),cartesian_product2(C,D)))))))),inference(shift_quantors,[status(thm)],[c6])).
% 0.38/0.62 fof(c9,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:((~in(ordered_pair(X2,X3),cartesian_product2(X4,X5))|(in(X2,X4)&in(X3,X5)))&((~in(X6,X8)|~in(X7,X9))|in(ordered_pair(X6,X7),cartesian_product2(X8,X9)))))))))))),inference(shift_quantors,[status(thm)],[fof(c8,plain,((![X2]:(![X3]:(![X4]:(![X5]:(~in(ordered_pair(X2,X3),cartesian_product2(X4,X5))|(in(X2,X4)&in(X3,X5)))))))&(![X6]:(![X7]:(![X8]:(![X9]:((~in(X6,X8)|~in(X7,X9))|in(ordered_pair(X6,X7),cartesian_product2(X8,X9)))))))),inference(variable_rename,[status(thm)],[c7])).])).
% 0.38/0.62 fof(c10,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:(((~in(ordered_pair(X2,X3),cartesian_product2(X4,X5))|in(X2,X4))&(~in(ordered_pair(X2,X3),cartesian_product2(X4,X5))|in(X3,X5)))&((~in(X6,X8)|~in(X7,X9))|in(ordered_pair(X6,X7),cartesian_product2(X8,X9)))))))))))),inference(distribute,[status(thm)],[c9])).
% 0.38/0.62 cnf(c11,plain,~in(ordered_pair(X59,X62),cartesian_product2(X60,X61))|in(X59,X60),inference(split_conjunct,[status(thm)],[c10])).
% 0.38/0.62 fof(t106_zfmisc_1,conjecture,(![A]:(![B]:(![C]:(![D]:(in(ordered_pair(A,B),cartesian_product2(C,D))<=>(in(A,C)&in(B,D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t106_zfmisc_1)).
% 0.38/0.62 fof(c14,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(in(ordered_pair(A,B),cartesian_product2(C,D))<=>(in(A,C)&in(B,D)))))))),inference(assume_negation,[status(cth)],[t106_zfmisc_1])).
% 0.38/0.62 fof(c15,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:((~in(ordered_pair(A,B),cartesian_product2(C,D))|(~in(A,C)|~in(B,D)))&(in(ordered_pair(A,B),cartesian_product2(C,D))|(in(A,C)&in(B,D)))))))),inference(fof_nnf,[status(thm)],[c14])).
% 0.38/0.62 fof(c16,negated_conjecture,(?[X10]:(?[X11]:(?[X12]:(?[X13]:((~in(ordered_pair(X10,X11),cartesian_product2(X12,X13))|(~in(X10,X12)|~in(X11,X13)))&(in(ordered_pair(X10,X11),cartesian_product2(X12,X13))|(in(X10,X12)&in(X11,X13)))))))),inference(variable_rename,[status(thm)],[c15])).
% 0.38/0.62 fof(c17,negated_conjecture,((~in(ordered_pair(skolem0001,skolem0002),cartesian_product2(skolem0003,skolem0004))|(~in(skolem0001,skolem0003)|~in(skolem0002,skolem0004)))&(in(ordered_pair(skolem0001,skolem0002),cartesian_product2(skolem0003,skolem0004))|(in(skolem0001,skolem0003)&in(skolem0002,skolem0004)))),inference(skolemize,[status(esa)],[c16])).
% 0.38/0.62 fof(c18,negated_conjecture,((~in(ordered_pair(skolem0001,skolem0002),cartesian_product2(skolem0003,skolem0004))|(~in(skolem0001,skolem0003)|~in(skolem0002,skolem0004)))&((in(ordered_pair(skolem0001,skolem0002),cartesian_product2(skolem0003,skolem0004))|in(skolem0001,skolem0003))&(in(ordered_pair(skolem0001,skolem0002),cartesian_product2(skolem0003,skolem0004))|in(skolem0002,skolem0004)))),inference(distribute,[status(thm)],[c17])).
% 0.38/0.62 cnf(c20,negated_conjecture,in(ordered_pair(skolem0001,skolem0002),cartesian_product2(skolem0003,skolem0004))|in(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c18])).
% 0.38/0.62 cnf(c150,plain,in(skolem0001,skolem0003),inference(resolution,[status(thm)],[c20, c11])).
% 0.38/0.62 cnf(c12,plain,~in(ordered_pair(X63,X66),cartesian_product2(X64,X65))|in(X66,X65),inference(split_conjunct,[status(thm)],[c10])).
% 0.38/0.62 cnf(c21,negated_conjecture,in(ordered_pair(skolem0001,skolem0002),cartesian_product2(skolem0003,skolem0004))|in(skolem0002,skolem0004),inference(split_conjunct,[status(thm)],[c18])).
% 0.38/0.62 cnf(c168,plain,in(skolem0002,skolem0004),inference(resolution,[status(thm)],[c21, c12])).
% 0.38/0.62 cnf(c19,negated_conjecture,~in(ordered_pair(skolem0001,skolem0002),cartesian_product2(skolem0003,skolem0004))|~in(skolem0001,skolem0003)|~in(skolem0002,skolem0004),inference(split_conjunct,[status(thm)],[c18])).
% 0.38/0.62 cnf(c13,plain,~in(X103,X104)|~in(X102,X105)|in(ordered_pair(X103,X102),cartesian_product2(X104,X105)),inference(split_conjunct,[status(thm)],[c10])).
% 0.38/0.62 cnf(c173,plain,~in(X168,X167)|in(ordered_pair(X168,skolem0002),cartesian_product2(X167,skolem0004)),inference(resolution,[status(thm)],[c168, c13])).
% 0.38/0.62 cnf(c302,plain,in(ordered_pair(skolem0001,skolem0002),cartesian_product2(skolem0003,skolem0004)),inference(resolution,[status(thm)],[c173, c150])).
% 0.38/0.62 cnf(c306,plain,~in(skolem0001,skolem0003)|~in(skolem0002,skolem0004),inference(resolution,[status(thm)],[c302, c19])).
% 0.38/0.62 cnf(c325,plain,~in(skolem0001,skolem0003),inference(resolution,[status(thm)],[c306, c168])).
% 0.38/0.62 cnf(c326,plain,$false,inference(resolution,[status(thm)],[c325, c150])).
% 0.38/0.62 % SZS output end CNFRefutation
% 0.38/0.62
% 0.38/0.62 % Initial clauses : 25
% 0.38/0.62 % Processed clauses : 65
% 0.38/0.62 % Factors computed : 6
% 0.38/0.62 % Resolvents computed: 277
% 0.38/0.62 % Tautologies deleted: 3
% 0.38/0.62 % Forward subsumed : 31
% 0.38/0.62 % Backward subsumed : 4
% 0.38/0.62 % -------- CPU Time ---------
% 0.38/0.62 % User time : 0.241 s
% 0.38/0.62 % System time : 0.015 s
% 0.38/0.62 % Total time : 0.256 s
%------------------------------------------------------------------------------