%------------------------------------------------------------------------------
% File : Toma---0.7
% Problem : BOO026-1 : TPTP v9.0.0. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_Leo-III %s %d THM
% 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 : Tue Jul 15 06:14:48 AM UTC 2025
% Result : Unsatisfiable 60.61s 60.85s
% Output : CNFRefutation 60.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 10
% Syntax : Number of clauses : 107 ( 107 unt; 0 nHn; 24 RR)
% Number of literals : 107 ( 106 equ; 1 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 127 ( 4 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(g0,negated_conjecture,
multiply(add(a,b),b) != b,
file('theBenchmark.p',prove_multiply_add) ).
cnf(c1,axiom,
add(X,inverse(X)) = n1,
file('theBenchmark.p',additive_inverse) ).
cnf(c2,axiom,
multiply(X,inverse(X)) = n0,
file('theBenchmark.p',multiplicative_inverse) ).
cnf(c3,axiom,
multiply(X,add(Y,Z)) = add(multiply(Y,X),multiply(Z,X)),
file('theBenchmark.p',multiply_add_property) ).
cnf(c4,plain,
add(multiply(X,Y),multiply(Z,Y)) = multiply(Y,add(X,Z)),
inference(equational,[status(thm)],[c3]) ).
cnf(c5,axiom,
add(X,multiply(Y,Z)) = multiply(add(Y,X),add(Z,X)),
file('theBenchmark.p',add_multiply_property) ).
cnf(c6,plain,
multiply(add(X,Y),add(Z,Y)) = add(Y,multiply(X,Z)),
inference(equational,[status(thm)],[c5]) ).
cnf(c7,plain,
multiply(n1,add(X,inverse(Y))) = add(inverse(Y),multiply(Y,X)),
inference(equational,[status(thm)],[c1,c6]) ).
cnf(c8,plain,
add(inverse(X),multiply(X,X)) = multiply(n1,n1),
inference(equational,[status(thm)],[c1,c7]) ).
cnf(c9,plain,
multiply(add(X,inverse(Y)),n1) = add(inverse(Y),multiply(X,Y)),
inference(equational,[status(thm)],[c1,c6]) ).
cnf(c10,plain,
multiply(inverse(X),add(Y,X)) = add(multiply(Y,inverse(X)),n0),
inference(equational,[status(thm)],[c2,c4]) ).
cnf(c11,plain,
multiply(inverse(X),add(X,Y)) = add(n0,multiply(Y,inverse(X))),
inference(equational,[status(thm)],[c2,c4]) ).
cnf(c14,plain,
add(multiply(X,inverse(inverse(X))),n0) = multiply(inverse(inverse(X)),n1),
inference(equational,[status(thm)],[c1,c10]) ).
cnf(c16,plain,
add(inverse(add(X,Y)),add(Y,multiply(X,X))) = multiply(n1,n1),
inference(equational,[status(thm)],[c6,c8]) ).
cnf(c17,plain,
add(n0,multiply(multiply(X,X),inverse(inverse(X)))) = multiply(inverse(inverse(X)),multiply(n1,n1)),
inference(equational,[status(thm)],[c8,c11]) ).
cnf(c18,plain,
multiply(multiply(n1,n1),add(X,multiply(Y,Y))) = add(multiply(Y,Y),multiply(inverse(Y),X)),
inference(equational,[status(thm)],[c6,c8]) ).
cnf(c19,plain,
multiply(multiply(n1,n1),add(X,multiply(X,X))) = multiply(X,n1),
inference(equational,[status(thm)],[c1,c4,c18]) ).
cnf(c20,plain,
multiply(add(X,multiply(Y,Y)),multiply(n1,n1)) = add(multiply(Y,Y),multiply(X,inverse(Y))),
inference(equational,[status(thm)],[c6,c8]) ).
cnf(c23,axiom,
add(multiply(X,inverse(X)),add(multiply(X,Y),multiply(inverse(X),Y))) = Y,
file('theBenchmark.p',pixley1) ).
cnf(c24,plain,
add(n0,multiply(X,n1)) = X,
inference(equational,[status(thm)],[c1,c2,c4,c23]) ).
cnf(c25,plain,
multiply(X,add(Y,multiply(X,n1))) = add(multiply(X,n1),multiply(n0,Y)),
inference(equational,[status(thm)],[c6,c24]) ).
cnf(c26,plain,
multiply(X,X) = add(multiply(X,n1),multiply(n0,n0)),
inference(equational,[status(thm)],[c24,c25]) ).
cnf(c27,plain,
multiply(add(X,multiply(Y,n1)),Y) = add(multiply(Y,n1),multiply(X,n0)),
inference(equational,[status(thm)],[c6,c24]) ).
cnf(c28,plain,
add(inverse(add(n1,n0)),n1) = multiply(n1,n1),
inference(equational,[status(thm)],[c16,c24]) ).
cnf(c29,plain,
add(n0,add(inverse(X),multiply(Y,X))) = add(Y,inverse(X)),
inference(equational,[status(thm)],[c9,c24]) ).
cnf(c30,plain,
add(n0,add(inverse(inverse(X)),n0)) = add(X,inverse(inverse(X))),
inference(equational,[status(thm)],[c2,c29]) ).
cnf(c31,plain,
add(n0,multiply(multiply(X,n1),inverse(n0))) = multiply(inverse(n0),X),
inference(equational,[status(thm)],[c11,c24]) ).
cnf(c43,axiom,
add(multiply(X,inverse(Y)),add(multiply(X,Y),multiply(inverse(Y),Y))) = X,
file('theBenchmark.p',pixley2) ).
cnf(c44,plain,
add(multiply(X,inverse(Y)),multiply(Y,add(X,inverse(Y)))) = X,
inference(equational,[status(thm)],[c4,c43]) ).
cnf(c47,axiom,
add(multiply(X,inverse(Y)),add(multiply(X,X),multiply(inverse(Y),X))) = X,
file('theBenchmark.p',pixley3) ).
cnf(c48,plain,
add(multiply(X,inverse(Y)),multiply(X,add(X,inverse(Y)))) = X,
inference(equational,[status(thm)],[c4,c47]) ).
cnf(c50,axiom,
multiply(add(X,inverse(X)),multiply(add(X,Y),add(inverse(X),Y))) = Y,
file('theBenchmark.p',pixley1_dual) ).
cnf(c51,plain,
multiply(n1,add(X,n0)) = X,
inference(equational,[status(thm)],[c1,c2,c6,c50]) ).
cnf(c52,plain,
add(X,multiply(Y,add(X,n0))) = multiply(add(X,n0),add(n1,Y)),
inference(equational,[status(thm)],[c4,c51]) ).
cnf(c53,plain,
add(X,multiply(n0,add(X,n0))) = X,
inference(equational,[status(thm)],[c6,c24,c52]) ).
cnf(c54,plain,
add(X,X) = multiply(add(X,n0),add(n1,n1)),
inference(equational,[status(thm)],[c51,c52]) ).
cnf(c55,plain,
add(multiply(X,add(Y,n0)),Y) = multiply(add(Y,n0),add(X,n1)),
inference(equational,[status(thm)],[c4,c51]) ).
cnf(c58,plain,
add(inverse(add(X,n0)),X) = multiply(add(n1,inverse(add(X,n0))),n1),
inference(equational,[status(thm)],[c9,c51]) ).
cnf(c61,plain,
add(n0,add(inverse(add(X,n0)),X)) = add(n1,inverse(add(X,n0))),
inference(equational,[status(thm)],[c24,c58]) ).
cnf(c62,plain,
add(n1,inverse(add(n1,n0))) = n1,
inference(equational,[status(thm)],[c24,c28,c61]) ).
cnf(c67,plain,
add(add(n0,multiply(X,Y)),Y) = multiply(add(Y,n0),add(add(X,n0),n1)),
inference(equational,[status(thm)],[c6,c55]) ).
cnf(c69,plain,
multiply(add(multiply(X,Y),n0),add(n1,n1)) = multiply(Y,add(X,X)),
inference(equational,[status(thm)],[c4,c54]) ).
cnf(c71,plain,
multiply(inverse(X),multiply(add(X,n0),add(n1,n1))) = add(n0,n0),
inference(equational,[status(thm)],[c2,c10,c54]) ).
cnf(c73,plain,
multiply(inverse(multiply(X,Y)),multiply(Y,add(X,X))) = add(n0,n0),
inference(equational,[status(thm)],[c69,c71]) ).
cnf(c79,axiom,
multiply(add(X,inverse(Y)),multiply(add(X,X),add(inverse(Y),X))) = X,
file('theBenchmark.p',pixley3_dual) ).
cnf(c80,plain,
multiply(add(X,inverse(Y)),add(X,multiply(X,inverse(Y)))) = X,
inference(equational,[status(thm)],[c6,c79]) ).
cnf(c82,plain,
add(n0,multiply(multiply(n0,add(X,n0)),inverse(X))) = multiply(inverse(X),X),
inference(equational,[status(thm)],[c11,c53]) ).
cnf(c87,plain,
add(X,multiply(multiply(add(X,n0),n1),add(X,n0))) = add(X,n0),
inference(equational,[status(thm)],[c4,c25,c51,c52]) ).
cnf(c98,plain,
multiply(add(X,multiply(n0,n0)),multiply(Y,Y)) = add(multiply(n0,n0),multiply(X,multiply(Y,n1))),
inference(equational,[status(thm)],[c6,c26]) ).
cnf(c110,plain,
multiply(multiply(X,add(Y,Z)),add(W,multiply(Z,X))) = add(multiply(Z,X),multiply(multiply(Y,X),W)),
inference(equational,[status(thm)],[c4,c6]) ).
cnf(c111,plain,
add(multiply(n0,n1),multiply(multiply(X,n1),Y)) = multiply(X,add(Y,multiply(n0,n1))),
inference(equational,[status(thm)],[c51,c110]) ).
cnf(c112,plain,
multiply(X,add(n1,multiply(n0,n1))) = multiply(n1,X),
inference(equational,[status(thm)],[c4,c24,c111]) ).
cnf(c113,plain,
multiply(n1,n0) = n0,
inference(equational,[status(thm)],[c4,c25,c51,c112]) ).
cnf(c114,plain,
multiply(n0,add(n1,X)) = add(n0,multiply(X,n0)),
inference(equational,[status(thm)],[c4,c113]) ).
cnf(c115,plain,
multiply(n0,add(X,n1)) = add(multiply(X,n0),n0),
inference(equational,[status(thm)],[c4,c113]) ).
cnf(c118,plain,
multiply(n1,add(X,multiply(n0,n1))) = multiply(n1,add(n0,X)),
inference(equational,[status(thm)],[c4,c6,c112]) ).
cnf(c119,plain,
multiply(n1,add(n0,n1)) = multiply(n1,n1),
inference(equational,[status(thm)],[c112,c118]) ).
cnf(c120,plain,
multiply(n1,inverse(multiply(n1,n1))) = add(n0,n0),
inference(equational,[status(thm)],[c6,c73,c112,c119]) ).
cnf(c122,plain,
add(n0,multiply(multiply(n0,n1),n0)) = n0,
inference(equational,[status(thm)],[c112,c113,c114]) ).
cnf(c123,plain,
add(n1,add(n0,multiply(n0,n0))) = n1,
inference(equational,[status(thm)],[c53,c114]) ).
cnf(c125,plain,
multiply(multiply(n1,n1),multiply(n0,n0)) = multiply(multiply(n0,n1),n1),
inference(equational,[status(thm)],[c4,c19,c51,c111]) ).
cnf(c126,plain,
multiply(n1,add(n0,multiply(n0,n0))) = n0,
inference(equational,[status(thm)],[c111,c114,c118,c122,c125]) ).
cnf(c134,plain,
multiply(X,add(inverse(multiply(X,n1)),multiply(n0,n1))) = add(multiply(n0,n1),n0),
inference(equational,[status(thm)],[c2,c111]) ).
cnf(c136,plain,
multiply(add(n1,multiply(n0,n1)),add(X,Y)) = add(multiply(n1,X),multiply(n1,Y)),
inference(equational,[status(thm)],[c4,c112]) ).
cnf(c137,plain,
multiply(add(n1,multiply(n0,n1)),X) = add(n0,multiply(n1,multiply(X,n1))),
inference(equational,[status(thm)],[c24,c113,c136]) ).
cnf(c140,plain,
add(n0,multiply(n1,multiply(n1,n1))) = add(multiply(n1,n1),n0),
inference(equational,[status(thm)],[c123,c126,c136,c137]) ).
cnf(c141,plain,
add(multiply(n1,X),multiply(n1,inverse(X))) = add(multiply(n1,n1),n0),
inference(equational,[status(thm)],[c1,c136,c137,c140]) ).
cnf(c142,plain,
add(n0,multiply(n1,inverse(n0))) = add(multiply(n1,n1),n0),
inference(equational,[status(thm)],[c113,c141]) ).
cnf(c144,plain,
add(X,multiply(n1,inverse(add(X,n0)))) = add(multiply(n1,n1),n0),
inference(equational,[status(thm)],[c51,c141]) ).
cnf(c145,plain,
multiply(n1,n1) = n1,
inference(equational,[status(thm)],[c51,c62,c80,c144]) ).
cnf(c146,plain,
add(n0,n0) = n0,
inference(equational,[status(thm)],[c2,c120,c145]) ).
cnf(c147,plain,
add(n0,n1) = n1,
inference(equational,[status(thm)],[c24,c145]) ).
cnf(c148,plain,
add(n1,n0) = n1,
inference(equational,[status(thm)],[c140,c145,c147]) ).
cnf(c149,plain,
add(n1,n1) = n1,
inference(equational,[status(thm)],[c87,c145,c148]) ).
cnf(c151,plain,
multiply(n0,n1) = n0,
inference(equational,[status(thm)],[c113,c115,c146,c149]) ).
cnf(c152,plain,
multiply(inverse(n0),n1) = n1,
inference(equational,[status(thm)],[c31,c142,c145,c148]) ).
cnf(c153,plain,
inverse(n0) = n1,
inference(equational,[status(thm)],[c24,c147,c152]) ).
cnf(c154,plain,
multiply(n0,n0) = n0,
inference(equational,[status(thm)],[c24,c82,c113,c146,c153]) ).
cnf(c155,plain,
multiply(X,n1) = multiply(n1,X),
inference(equational,[status(thm)],[c24,c31,c153]) ).
cnf(c156,plain,
inverse(n1) = n0,
inference(equational,[status(thm)],[c51,c134,c145,c146,c151,c155]) ).
cnf(c157,plain,
add(n0,multiply(n1,X)) = X,
inference(equational,[status(thm)],[c6,c51,c148]) ).
cnf(c158,plain,
add(n0,X) = add(X,n0),
inference(equational,[status(thm)],[c118,c151,c157]) ).
cnf(c159,plain,
multiply(n1,add(X,n1)) = add(multiply(X,n1),n1),
inference(equational,[status(thm)],[c4,c145]) ).
cnf(c162,plain,
add(multiply(X,n1),n1) = add(n1,multiply(n0,X)),
inference(equational,[status(thm)],[c25,c145,c159]) ).
cnf(c165,plain,
add(n1,multiply(n0,X)) = add(n1,multiply(X,n0)),
inference(equational,[status(thm)],[c27,c145,c155,c159,c162]) ).
cnf(c166,plain,
multiply(n1,multiply(X,X)) = multiply(X,n1),
inference(equational,[status(thm)],[c98,c148,c154,c157,c165]) ).
cnf(c167,plain,
multiply(X,X) = X,
inference(equational,[status(thm)],[c24,c157,c166]) ).
cnf(c168,plain,
add(X,Y) = add(Y,X),
inference(equational,[status(thm)],[c6,c167]) ).
cnf(c173,plain,
add(X,X) = X,
inference(equational,[status(thm)],[c51,c54,c149,c155]) ).
cnf(c174,plain,
multiply(X,Y) = multiply(Y,X),
inference(equational,[status(thm)],[c4,c173]) ).
cnf(c175,plain,
multiply(X,n1) = add(X,n0),
inference(equational,[status(thm)],[c2,c20,c145,c167,c173]) ).
cnf(c177,plain,
add(n0,inverse(X)) = inverse(X),
inference(equational,[status(thm)],[c2,c44,c158,c167,c173]) ).
cnf(c178,plain,
multiply(n0,inverse(X)) = n0,
inference(equational,[status(thm)],[c4,c48,c146,c174,c177]) ).
cnf(c179,plain,
add(n0,add(X,n0)) = X,
inference(equational,[status(thm)],[c67,c148,c149,c157,c158,c173,c175]) ).
cnf(c182,plain,
add(n1,multiply(X,n0)) = add(n0,add(X,n1)),
inference(equational,[status(thm)],[c20,c145,c156,c158,c175]) ).
cnf(c186,plain,
multiply(X,inverse(inverse(X))) = inverse(inverse(X)),
inference(equational,[status(thm)],[c14,c175,c179]) ).
cnf(c187,plain,
add(X,inverse(inverse(X))) = inverse(inverse(X)),
inference(equational,[status(thm)],[c30,c179]) ).
cnf(c188,plain,
inverse(inverse(X)) = X,
inference(equational,[status(thm)],[c80,c167,c186,c187]) ).
cnf(c189,plain,
add(n0,X) = X,
inference(equational,[status(thm)],[c177,c188]) ).
cnf(c190,plain,
multiply(n0,X) = n0,
inference(equational,[status(thm)],[c178,c188]) ).
cnf(c191,plain,
add(X,n0) = X,
inference(equational,[status(thm)],[c17,c145,c167,c175,c188,c189]) ).
cnf(c193,plain,
add(X,n1) = n1,
inference(equational,[status(thm)],[c148,c165,c182,c189,c190]) ).
cnf(c196,plain,
multiply(X,add(Y,X)) = add(X,multiply(Y,X)),
inference(equational,[status(thm)],[c4,c167,c168]) ).
cnf(c197,plain,
add(add(X,multiply(Y,Z)),multiply(W,add(Z,X))) = multiply(add(Z,X),add(add(Y,X),W)),
inference(equational,[status(thm)],[c4,c6]) ).
cnf(c198,plain,
add(X,multiply(Y,X)) = X,
inference(equational,[status(thm)],[c51,c168,c175,c189,c191,c193,c197]) ).
cnf(g1,plain,
multiply(add(a,b),b) = b,
inference(equational,[status(thm)],[c174,c196,c198]) ).
cnf(g2,plain,
$false,
inference(resolution,[status(thm)],[g0,g1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : BOO026-1 : TPTP v9.0.0. Released v2.2.0.
% 0.08/0.14 % Command : run_Leo-III %s %d THM
% 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.35 % CPULimit : 300
% 0.15/0.35 % WCLimit : 300
% 0.15/0.35 % DateTime : Mon Jul 14 04:24:04 EDT 2025
% 0.15/0.35 % CPUTime :
% 60.61/60.85 % SZS status Unsatisfiable
% 60.61/60.85 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------