%------------------------------------------------------------------------------
% File : Toma---0.7
% Problem : ANA133-1 : TPTP v9.0.0. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_Leo-III %s %d THM
% Computer : n016.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:11:32 AM UTC 2025
% Result : Unsatisfiable 91.86s 91.98s
% Output : CNFRefutation 91.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 12
% Syntax : Number of formulae : 34 ( 33 unt; 0 def)
% Number of atoms : 36 ( 35 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 5 ( 3 ~; 0 |; 2 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-2 aty)
% Number of variables : 40 ( 2 sgn 1 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(g0,negated_conjecture,
d(T) != times(x,cos(x)),
file('theBenchmark.p',goal) ).
fof(e,plain,
! [T] :
( true != false
& eq(T,T) = true
& eq(d(T),times(x,cos(x))) = false ),
inference(encode_existential,[status(esa)],[g0]) ).
cnf(g1,plain,
true != false,
inference(split_conjunct,[status(thm)],[e]) ).
cnf(c3,axiom,
d(x) = one,
file('theBenchmark.p',derivative_of_x) ).
cnf(c4,plain,
eq(X,X) = true,
inference(split_conjunct,[status(thm)],[e]) ).
cnf(c5,axiom,
times(one,X) = X,
file('theBenchmark.p',times_one) ).
cnf(c6,axiom,
'+'(zero,X) = X,
file('theBenchmark.p',plus_zero) ).
cnf(c8,axiom,
times(X,Y) = times(Y,X),
file('theBenchmark.p',commutativity_of_times) ).
cnf(c9,axiom,
'+'(X,Y) = '+'(Y,X),
file('theBenchmark.p',commutativity_of_plus) ).
cnf(c11,plain,
times(X,one) = X,
inference(equational,[status(thm)],[c5,c8]) ).
cnf(c13,axiom,
'+'(X,minus(X)) = zero,
file('theBenchmark.p',minus) ).
cnf(c15,axiom,
d(sin(X)) = times(cos(X),d(X)),
file('theBenchmark.p',derivative_of_sin) ).
cnf(c16,plain,
times(cos(X),d(X)) = d(sin(X)),
inference(equational,[status(thm)],[c15]) ).
cnf(c19,plain,
d(sin(x)) = cos(x),
inference(equational,[status(thm)],[c3,c11,c16]) ).
cnf(c22,axiom,
d('+'(X,Y)) = '+'(d(X),d(Y)),
file('theBenchmark.p',derivative_of_plus) ).
cnf(c23,plain,
'+'(d(X),d(Y)) = d('+'(X,Y)),
inference(equational,[status(thm)],[c22]) ).
cnf(c31,axiom,
'+'(X,'+'(Y,Z)) = '+'('+'(X,Y),Z),
file('theBenchmark.p',associtivity_of_plus) ).
cnf(c32,plain,
'+'('+'(X,Y),Z) = '+'(X,'+'(Y,Z)),
inference(equational,[status(thm)],[c31]) ).
cnf(c34,plain,
'+'(X,'+'(Y,Z)) = '+'(Y,'+'(X,Z)),
inference(equational,[status(thm)],[c9,c32]) ).
cnf(c36,plain,
'+'(X,'+'(minus(X),Y)) = Y,
inference(equational,[status(thm)],[c6,c13,c32]) ).
cnf(c40,axiom,
d(cos(X)) = minus(times(sin(X),d(X))),
file('theBenchmark.p',derivative_of_cos) ).
cnf(c41,plain,
minus(times(sin(X),d(X))) = d(cos(X)),
inference(equational,[status(thm)],[c40]) ).
cnf(c44,plain,
d(cos(x)) = minus(sin(x)),
inference(equational,[status(thm)],[c3,c11,c41]) ).
cnf(c83,plain,
eq(d(X),times(x,cos(x))) = false,
inference(split_conjunct,[status(thm)],[e]) ).
cnf(c161,plain,
'+'(minus(sin(x)),d(X)) = d('+'(cos(x),X)),
inference(equational,[status(thm)],[c23,c44]) ).
cnf(c305,axiom,
d(times(X,Y)) = '+'(times(X,d(Y)),times(Y,d(X))),
file('theBenchmark.p',derivative_of_times) ).
cnf(c306,plain,
'+'(times(X,d(Y)),times(Y,d(X))) = d(times(X,Y)),
inference(equational,[status(thm)],[c305]) ).
cnf(c317,plain,
'+'(X,times(x,d(X))) = d(times(x,X)),
inference(equational,[status(thm)],[c3,c9,c11,c306]) ).
cnf(c733,plain,
'+'(X,'+'(Y,times(x,d(X)))) = '+'(Y,d(times(x,X))),
inference(equational,[status(thm)],[c34,c317]) ).
cnf(c734,plain,
'+'(minus(X),d(times(x,X))) = times(x,d(X)),
inference(equational,[status(thm)],[c36,c733]) ).
cnf(c2313,plain,
d('+'(cos(x),times(x,sin(x)))) = times(x,cos(x)),
inference(equational,[status(thm)],[c19,c161,c734]) ).
cnf(c2314,plain,
true = false,
inference(equational,[status(thm)],[c4,c83,c2313]) ).
cnf(g2,plain,
true = false,
inference(equational,[status(thm)],[c2314]) ).
cnf(g3,plain,
$false,
inference(resolution,[status(thm)],[g1,g2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : ANA133-1 : TPTP v9.0.0. Released v8.1.0.
% 0.08/0.13 % Command : run_Leo-III %s %d THM
% 0.12/0.34 % Computer : n016.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Mon Jul 14 04:04:19 EDT 2025
% 0.12/0.34 % CPUTime :
% 91.86/91.98 % SZS status Unsatisfiable
% 91.86/91.98 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------