%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MSC012+1 : TPTP v8.1.2. Released v3.2.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:33:23 EDT 2024
% Result : Theorem 0.58s 0.80s
% Output : Refutation 0.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : MSC012+1 : TPTP v8.1.2. Released v3.2.0.
% 0.08/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n022.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 13:58:08 EDT 2024
% 0.15/0.37 % CPUTime :
% 0.58/0.80 % Version: 1.5
% 0.58/0.80 % SZS status Theorem
% 0.58/0.80 % SZS output start CNFRefutation
% 0.58/0.80 fof(goal_to_be_proved,conjecture,goal,file('/export/starexec/sandbox/benchmark/theBenchmark.p', goal_to_be_proved)).
% 0.58/0.80 fof(c0,negated_conjecture,(~goal),inference(assume_negation,[status(cth)],[goal_to_be_proved])).
% 0.58/0.80 fof(c1,negated_conjecture,~goal,inference(fof_simplification,[status(thm)],[c0])).
% 0.58/0.80 cnf(c2,negated_conjecture,~goal,inference(split_conjunct,[status(thm)],[c1])).
% 0.58/0.80 fof(right_to_left,axiom,(![A]:(p(A)|(?[B]:(less(A,B)&p(B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', right_to_left)).
% 0.58/0.80 fof(c9,plain,(![X7]:(p(X7)|(?[X8]:(less(X7,X8)&p(X8))))),inference(variable_rename,[status(thm)],[right_to_left])).
% 0.58/0.80 fof(c10,plain,(![X7]:(p(X7)|(less(X7,skolem0002(X7))&p(skolem0002(X7))))),inference(skolemize,[status(esa)],[c9])).
% 0.58/0.80 fof(c11,plain,(![X7]:((p(X7)|less(X7,skolem0002(X7)))&(p(X7)|p(skolem0002(X7))))),inference(distribute,[status(thm)],[c10])).
% 0.58/0.80 cnf(c13,plain,p(X12)|p(skolem0002(X12)),inference(split_conjunct,[status(thm)],[c11])).
% 0.58/0.80 fof(serial_less,axiom,(![A]:(?[B]:less(A,B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', serial_less)).
% 0.58/0.80 fof(c3,plain,(![X2]:(?[X3]:less(X2,X3))),inference(variable_rename,[status(thm)],[serial_less])).
% 0.58/0.80 fof(c4,plain,(![X2]:less(X2,skolem0001(X2))),inference(skolemize,[status(esa)],[c3])).
% 0.58/0.80 cnf(c5,plain,less(X11,skolem0001(X11)),inference(split_conjunct,[status(thm)],[c4])).
% 0.58/0.80 fof(left_to_right,axiom,(![A]:(![B]:(((p(A)&less(A,B))&p(B))=>goal))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', left_to_right)).
% 0.58/0.80 fof(c14,plain,(![A]:(![B]:(((~p(A)|~less(A,B))|~p(B))|goal))),inference(fof_nnf,[status(thm)],[left_to_right])).
% 0.58/0.80 fof(c15,plain,((![A]:(![B]:((~p(A)|~less(A,B))|~p(B))))|goal),inference(shift_quantors,[status(thm)],[c14])).
% 0.58/0.80 fof(c17,plain,(![X9]:(![X10]:(((~p(X9)|~less(X9,X10))|~p(X10))|goal))),inference(shift_quantors,[status(thm)],[fof(c16,plain,((![X9]:(![X10]:((~p(X9)|~less(X9,X10))|~p(X10))))|goal),inference(variable_rename,[status(thm)],[c15])).])).
% 0.58/0.80 cnf(c18,plain,~p(X17)|~less(X17,X18)|~p(X18)|goal,inference(split_conjunct,[status(thm)],[c17])).
% 0.58/0.80 cnf(c23,plain,~p(X23)|~p(skolem0001(X23))|goal,inference(resolution,[status(thm)],[c18, c5])).
% 0.58/0.80 cnf(c12,plain,p(X13)|less(X13,skolem0002(X13)),inference(split_conjunct,[status(thm)],[c11])).
% 0.58/0.80 fof(transitive_less,axiom,(![A]:(![B]:(![C]:((less(A,B)&less(B,C))=>less(A,C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', transitive_less)).
% 0.58/0.80 fof(c6,plain,(![A]:(![B]:(![C]:((~less(A,B)|~less(B,C))|less(A,C))))),inference(fof_nnf,[status(thm)],[transitive_less])).
% 0.58/0.80 fof(c7,plain,(![X4]:(![X5]:(![X6]:((~less(X4,X5)|~less(X5,X6))|less(X4,X6))))),inference(variable_rename,[status(thm)],[c6])).
% 0.58/0.80 cnf(c8,plain,~less(X15,X16)|~less(X16,X14)|less(X15,X14),inference(split_conjunct,[status(thm)],[c7])).
% 0.58/0.80 cnf(c20,plain,~less(X25,X26)|less(X25,skolem0002(X26))|p(X26),inference(resolution,[status(thm)],[c8, c12])).
% 0.58/0.80 cnf(c37,plain,less(X36,skolem0002(skolem0001(X36)))|p(skolem0001(X36)),inference(resolution,[status(thm)],[c20, c5])).
% 0.58/0.80 cnf(c62,plain,p(skolem0001(X99))|~p(X99)|~p(skolem0002(skolem0001(X99)))|goal,inference(resolution,[status(thm)],[c37, c18])).
% 0.58/0.80 cnf(c701,plain,p(skolem0001(X100))|~p(X100)|goal,inference(resolution,[status(thm)],[c62, c13])).
% 0.58/0.80 cnf(c716,plain,p(skolem0001(X101))|goal|p(skolem0002(X101)),inference(resolution,[status(thm)],[c701, c13])).
% 0.58/0.80 cnf(c740,plain,goal|p(skolem0002(X102))|~p(X102),inference(resolution,[status(thm)],[c716, c23])).
% 0.58/0.80 cnf(c770,plain,goal|p(skolem0002(X104)),inference(resolution,[status(thm)],[c740, c13])).
% 0.58/0.80 cnf(c816,plain,p(skolem0002(X105)),inference(resolution,[status(thm)],[c770, c2])).
% 0.58/0.80 cnf(c820,plain,goal|p(skolem0001(skolem0002(X106))),inference(resolution,[status(thm)],[c770, c701])).
% 0.58/0.80 cnf(c838,plain,goal|~p(skolem0002(X108)),inference(resolution,[status(thm)],[c820, c23])).
% 0.58/0.80 cnf(c853,plain,goal,inference(resolution,[status(thm)],[c838, c816])).
% 0.58/0.80 cnf(c857,plain,$false,inference(resolution,[status(thm)],[c853, c2])).
% 0.58/0.80 % SZS output end CNFRefutation
% 0.58/0.80
% 0.58/0.80 % Initial clauses : 6
% 0.58/0.80 % Processed clauses : 71
% 0.58/0.80 % Factors computed : 1
% 0.58/0.80 % Resolvents computed: 838
% 0.58/0.80 % Tautologies deleted: 3
% 0.58/0.80 % Forward subsumed : 17
% 0.58/0.80 % Backward subsumed : 40
% 0.58/0.80 % -------- CPU Time ---------
% 0.58/0.80 % User time : 0.401 s
% 0.58/0.80 % System time : 0.015 s
% 0.58/0.80 % Total time : 0.416 s
%------------------------------------------------------------------------------