%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUM001-1 : TPTP v8.1.2. Released v1.0.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:34:59 EDT 2024
% Result : Unsatisfiable 68.04s 68.21s
% Output : Refutation 68.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 8
% Syntax : Number of clauses : 15 ( 9 unt; 0 nHn; 7 RR)
% Number of literals : 24 ( 0 equ; 10 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 38 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_equation,negated_conjecture,
~ equalish(add(add(a,b),c),add(a,add(b,c))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_equation) ).
cnf(addition_inverts_subtraction1,axiom,
equalish(subtract(add(X6,X5),X5),X6),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM002-0.ax',addition_inverts_subtraction1) ).
cnf(transitivity,axiom,
( ~ equalish(X11,X9)
| ~ equalish(X9,X10)
| equalish(X11,X10) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM002-0.ax',transitivity) ).
cnf(c4,plain,
( ~ equalish(X33,subtract(add(X34,X35),X35))
| equalish(X33,X34) ),
inference(resolution,[status(thm)],[transitivity,addition_inverts_subtraction1]) ).
cnf(associativity_of_addition,axiom,
equalish(add(X14,add(X12,X13)),add(add(X14,X12),X13)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM002-0.ax',associativity_of_addition) ).
cnf(commutativity_of_addition,axiom,
equalish(add(X4,X3),add(X3,X4)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM002-0.ax',commutativity_of_addition) ).
cnf(addition_inverts_subtraction2,axiom,
equalish(X8,subtract(add(X8,X7),X7)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM002-0.ax',addition_inverts_subtraction2) ).
cnf(subtract_substitution1,axiom,
( ~ equalish(X88,X86)
| ~ equalish(X87,subtract(X88,X89))
| equalish(X87,subtract(X86,X89)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM002-0.ax',subtract_substitution1) ).
cnf(c98,plain,
( ~ equalish(add(X93,X94),X92)
| equalish(X93,subtract(X92,X94)) ),
inference(resolution,[status(thm)],[subtract_substitution1,addition_inverts_subtraction2]) ).
cnf(c105,plain,
equalish(X96,subtract(add(X95,X96),X95)),
inference(resolution,[status(thm)],[c98,commutativity_of_addition]) ).
cnf(subtract_substitution2,axiom,
( ~ equalish(X102,X100)
| ~ equalish(X101,subtract(X103,X102))
| equalish(X101,subtract(X103,X100)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM002-0.ax',subtract_substitution2) ).
cnf(c121,plain,
( ~ equalish(X135,X133)
| equalish(X134,subtract(add(X135,X134),X133)) ),
inference(resolution,[status(thm)],[subtract_substitution2,c105]) ).
cnf(c183,plain,
equalish(X1099,subtract(add(add(X1102,add(X1100,X1101)),X1099),add(add(X1102,X1100),X1101))),
inference(resolution,[status(thm)],[c121,associativity_of_addition]) ).
cnf(c8222,plain,
equalish(add(add(X7103,X7102),X7101),add(X7103,add(X7102,X7101))),
inference(resolution,[status(thm)],[c183,c4]) ).
cnf(c108871,plain,
$false,
inference(resolution,[status(thm)],[c8222,prove_equation]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.14 % Problem : NUM001-1 : TPTP v8.1.2. Released v1.0.0.
% 0.13/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.37 % Computer : n022.cluster.edu
% 0.14/0.37 % Model : x86_64 x86_64
% 0.14/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.37 % Memory : 8042.1875MB
% 0.14/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.37 % CPULimit : 300
% 0.14/0.37 % WCLimit : 300
% 0.14/0.37 % DateTime : Wed May 8 16:16:08 EDT 2024
% 0.14/0.37 % CPUTime :
% 68.04/68.21 % Version: 1.5
% 68.04/68.21 % SZS status Unsatisfiable
% 68.04/68.21 % SZS output start CNFRefutation
% See solution above
% 68.04/68.21
% 68.04/68.21 % Initial clauses : 13
% 68.04/68.21 % Processed clauses : 1141
% 68.04/68.21 % Factors computed : 5
% 68.04/68.21 % Resolvents computed: 108999
% 68.04/68.21 % Tautologies deleted: 2
% 68.04/68.21 % Forward subsumed : 1455
% 68.04/68.21 % Backward subsumed : 1
% 68.04/68.21 % -------- CPU Time ---------
% 68.04/68.21 % User time : 67.612 s
% 68.04/68.21 % System time : 0.219 s
% 68.04/68.21 % Total time : 67.831 s
%------------------------------------------------------------------------------