%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU295+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n003.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:41:02 EDT 2024
% Result : Theorem 83.87s 84.13s
% Output : Refutation 83.87s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SEU295+2 : TPTP v8.1.2. Released v3.3.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n003.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed May 8 11:08:37 EDT 2024
% 0.12/0.34 % CPUTime :
% 83.87/84.13 % Version: 1.5
% 83.87/84.13 % SZS status Theorem
% 83.87/84.13 % SZS output start CNFRefutation
% 83.87/84.13 fof(t15_finset_1,conjecture,(![A]:(![B]:(finite(A)=>finite(set_intersection2(A,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t15_finset_1)).
% 83.87/84.13 fof(c691,negated_conjecture,(~(![A]:(![B]:(finite(A)=>finite(set_intersection2(A,B)))))),inference(assume_negation,[status(cth)],[t15_finset_1])).
% 83.87/84.13 fof(c692,negated_conjecture,(?[A]:(?[B]:(finite(A)&~finite(set_intersection2(A,B))))),inference(fof_nnf,[status(thm)],[c691])).
% 83.87/84.13 fof(c693,negated_conjecture,(?[A]:(finite(A)&(?[B]:~finite(set_intersection2(A,B))))),inference(shift_quantors,[status(thm)],[c692])).
% 83.87/84.13 fof(c694,negated_conjecture,(?[X364]:(finite(X364)&(?[X365]:~finite(set_intersection2(X364,X365))))),inference(variable_rename,[status(thm)],[c693])).
% 83.87/84.13 fof(c695,negated_conjecture,(finite(skolem0027)&~finite(set_intersection2(skolem0027,skolem0028))),inference(skolemize,[status(esa)],[c694])).
% 83.87/84.13 cnf(c697,negated_conjecture,~finite(set_intersection2(skolem0027,skolem0028)),inference(split_conjunct,[status(thm)],[c695])).
% 83.87/84.13 cnf(c696,negated_conjecture,finite(skolem0027),inference(split_conjunct,[status(thm)],[c695])).
% 83.87/84.13 fof(fc11_finset_1,axiom,(![A]:(![B]:(finite(A)=>finite(set_intersection2(A,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', fc11_finset_1)).
% 83.87/84.13 fof(c1999,plain,(![A]:(![B]:(~finite(A)|finite(set_intersection2(A,B))))),inference(fof_nnf,[status(thm)],[fc11_finset_1])).
% 83.87/84.13 fof(c2000,plain,(![A]:(~finite(A)|(![B]:finite(set_intersection2(A,B))))),inference(shift_quantors,[status(thm)],[c1999])).
% 83.87/84.13 fof(c2002,plain,(![X836]:(![X837]:(~finite(X836)|finite(set_intersection2(X836,X837))))),inference(shift_quantors,[status(thm)],[fof(c2001,plain,(![X836]:(~finite(X836)|(![X837]:finite(set_intersection2(X836,X837))))),inference(variable_rename,[status(thm)],[c2000])).])).
% 83.87/84.13 cnf(c2003,plain,~finite(X6222)|finite(set_intersection2(X6222,X6221)),inference(split_conjunct,[status(thm)],[c2002])).
% 83.87/84.13 cnf(c68558,plain,finite(set_intersection2(skolem0027,X6322)),inference(resolution,[status(thm)],[c2003, c696])).
% 83.87/84.13 cnf(c70376,plain,$false,inference(resolution,[status(thm)],[c68558, c697])).
% 83.87/84.13 % SZS output end CNFRefutation
% 83.87/84.13
% 83.87/84.13 % Initial clauses : 1562
% 83.87/84.13 % Processed clauses : 3968
% 83.87/84.13 % Factors computed : 164
% 83.87/84.13 % Resolvents computed: 67422
% 83.87/84.13 % Tautologies deleted: 26
% 83.87/84.13 % Forward subsumed : 2417
% 83.87/84.13 % Backward subsumed : 126
% 83.87/84.13 % -------- CPU Time ---------
% 83.87/84.13 % User time : 83.586 s
% 83.87/84.13 % System time : 0.152 s
% 83.87/84.13 % Total time : 83.738 s
%------------------------------------------------------------------------------