%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU165+3 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n015.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.43s 0.62s
% Output : Refutation 0.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SEU165+3 : TPTP v8.1.2. Released v3.2.0.
% 0.13/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.35 % Computer : n015.cluster.edu
% 0.15/0.35 % Model : x86_64 x86_64
% 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.35 % Memory : 8042.1875MB
% 0.15/0.35 % 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 11:58:38 EDT 2024
% 0.15/0.36 % CPUTime :
% 0.43/0.62 % Version: 1.5
% 0.43/0.62 % SZS status Theorem
% 0.43/0.62 % SZS output start CNFRefutation
% 0.43/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.43/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.43/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.43/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.43/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.43/0.62 cnf(c11,plain,~in(ordered_pair(X60,X59),cartesian_product2(X61,X62))|in(X60,X61),inference(split_conjunct,[status(thm)],[c10])).
% 0.43/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.43/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.43/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.43/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.43/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.43/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.43/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.43/0.62 cnf(c130,plain,in(skolem0001,skolem0003),inference(resolution,[status(thm)],[c20, c11])).
% 0.43/0.62 cnf(c12,plain,~in(ordered_pair(X64,X63),cartesian_product2(X65,X66))|in(X63,X66),inference(split_conjunct,[status(thm)],[c10])).
% 0.43/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.43/0.62 cnf(c151,plain,in(skolem0002,skolem0004),inference(resolution,[status(thm)],[c21, c12])).
% 0.43/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.43/0.62 cnf(c13,plain,~in(X101,X98)|~in(X99,X100)|in(ordered_pair(X101,X99),cartesian_product2(X98,X100)),inference(split_conjunct,[status(thm)],[c10])).
% 0.43/0.62 cnf(c158,plain,~in(X166,X165)|in(ordered_pair(X166,skolem0002),cartesian_product2(X165,skolem0004)),inference(resolution,[status(thm)],[c151, c13])).
% 0.43/0.62 cnf(c303,plain,in(ordered_pair(skolem0001,skolem0002),cartesian_product2(skolem0003,skolem0004)),inference(resolution,[status(thm)],[c158, c130])).
% 0.43/0.62 cnf(c328,plain,~in(skolem0001,skolem0003)|~in(skolem0002,skolem0004),inference(resolution,[status(thm)],[c303, c19])).
% 0.43/0.62 cnf(c333,plain,~in(skolem0001,skolem0003),inference(resolution,[status(thm)],[c328, c151])).
% 0.43/0.62 cnf(c336,plain,$false,inference(resolution,[status(thm)],[c333, c130])).
% 0.43/0.62 % SZS output end CNFRefutation
% 0.43/0.62
% 0.43/0.62 % Initial clauses : 21
% 0.43/0.62 % Processed clauses : 65
% 0.43/0.62 % Factors computed : 6
% 0.43/0.62 % Resolvents computed: 291
% 0.43/0.62 % Tautologies deleted: 3
% 0.43/0.62 % Forward subsumed : 29
% 0.43/0.62 % Backward subsumed : 4
% 0.43/0.62 % -------- CPU Time ---------
% 0.43/0.62 % User time : 0.246 s
% 0.43/0.62 % System time : 0.017 s
% 0.43/0.62 % Total time : 0.263 s
%------------------------------------------------------------------------------