%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : RNG039-1 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n027.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:38:16 EDT 2024
% Result : Unsatisfiable 35.73s 35.93s
% Output : Refutation 35.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 10
% Syntax : Number of clauses : 25 ( 14 unt; 0 nHn; 11 RR)
% Number of literals : 43 ( 22 equ; 19 neg)
% Maximal clause size : 5 ( 1 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% Number of variables : 53 ( 13 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_c_equals_d,negated_conjecture,
c != d,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_c_equals_d) ).
cnf(symmetry,axiom,
( X40 != X41
| X41 = X40 ),
theory(equality) ).
cnf(transitivity,axiom,
( X150 != X151
| X151 != X152
| X150 = X152 ),
theory(equality) ).
cnf(clause35,axiom,
multiply(X9,X9) = X9,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause35) ).
cnf(c270,plain,
( X161 != multiply(X160,X160)
| X161 = X160 ),
inference(resolution,[status(thm)],[transitivity,clause35]) ).
cnf(clause44,axiom,
product(a,multiply(b,X126),multiply(X125,X126)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause44) ).
cnf(multiplication_is_well_defined,axiom,
( ~ product(X118,X119,X120)
| ~ product(X118,X119,X117)
| X120 = X117 ),
file('/export/starexec/sandbox2/benchmark/Axioms/RNG001-0.ax',multiplication_is_well_defined) ).
cnf(c194,plain,
( ~ product(a,multiply(b,X1607),X1606)
| X1606 = multiply(X1608,X1607) ),
inference(resolution,[status(thm)],[clause44,multiplication_is_well_defined]) ).
cnf(c4751,plain,
multiply(X2000,X2001) = multiply(X1999,X2001),
inference(resolution,[status(thm)],[c194,clause44]) ).
cnf(c7139,plain,
multiply(X2003,X2002) = X2002,
inference(resolution,[status(thm)],[c4751,c270]) ).
cnf(c7149,plain,
( X2651 != multiply(X2650,X2649)
| X2651 = X2649 ),
inference(resolution,[status(thm)],[c7139,transitivity]) ).
cnf(closure_of_multiplication,axiom,
product(X7,X8,multiply(X7,X8)),
file('/export/starexec/sandbox2/benchmark/Axioms/RNG001-0.ax',closure_of_multiplication) ).
cnf(c181,plain,
( ~ product(X1169,X1168,X1167)
| X1167 = multiply(X1169,X1168) ),
inference(resolution,[status(thm)],[multiplication_is_well_defined,closure_of_multiplication]) ).
cnf(clause71,axiom,
product(X3,X3,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause71) ).
cnf(clause32,axiom,
sum(X6,X6,additive_identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause32) ).
cnf(distributivity4,axiom,
( ~ product(X101,X105,X102)
| ~ product(X103,X105,X104)
| ~ sum(X101,X103,X106)
| ~ sum(X102,X104,X100)
| product(X106,X105,X100) ),
file('/export/starexec/sandbox2/benchmark/Axioms/RNG001-0.ax',distributivity4) ).
cnf(c121,plain,
( ~ product(X1242,X1243,X1242)
| ~ product(X1241,X1243,X1241)
| ~ sum(X1242,X1241,X1244)
| product(X1244,X1243,X1244) ),
inference(factor,[status(thm)],[distributivity4]) ).
cnf(c2943,plain,
( ~ product(X5414,X5413,X5414)
| product(additive_identity,X5413,additive_identity) ),
inference(resolution,[status(thm)],[c121,clause32]) ).
cnf(c52534,plain,
product(additive_identity,X5415,additive_identity),
inference(resolution,[status(thm)],[c2943,clause71]) ).
cnf(c52553,plain,
additive_identity = multiply(additive_identity,X5455),
inference(resolution,[status(thm)],[c52534,c181]) ).
cnf(c52966,plain,
additive_identity = X5456,
inference(resolution,[status(thm)],[c52553,c7149]) ).
cnf(c53015,plain,
X5465 = additive_identity,
inference(resolution,[status(thm)],[c52966,symmetry]) ).
cnf(c53041,plain,
( X5676 != additive_identity
| X5676 = X5675 ),
inference(resolution,[status(thm)],[c52966,transitivity]) ).
cnf(c56597,plain,
X5678 = X5677,
inference(resolution,[status(thm)],[c53041,c53015]) ).
cnf(c56653,plain,
$false,
inference(resolution,[status(thm)],[c56597,prove_c_equals_d]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : RNG039-1 : TPTP v8.1.2. Released v1.0.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n027.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 21:20:23 EDT 2024
% 0.13/0.34 % CPUTime :
% 35.73/35.93 % Version: 1.5
% 35.73/35.93 % SZS status Unsatisfiable
% 35.73/35.93 % SZS output start CNFRefutation
% See solution above
% 35.73/35.93
% 35.73/35.93 % Initial clauses : 68
% 35.73/35.93 % Processed clauses : 1062
% 35.73/35.93 % Factors computed : 174
% 35.73/35.93 % Resolvents computed: 56573
% 35.73/35.93 % Tautologies deleted: 41
% 35.73/35.93 % Forward subsumed : 2761
% 35.73/35.93 % Backward subsumed : 568
% 35.73/35.93 % -------- CPU Time ---------
% 35.73/35.93 % User time : 35.478 s
% 35.73/35.93 % System time : 0.100 s
% 35.73/35.93 % Total time : 35.578 s
%------------------------------------------------------------------------------