%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : KLE145+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:58:03 PM UTC 2026
% Result : Theorem 57.76s 7.78s
% Output : CNFRefutation 41.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 18
% Syntax : Number of formulae : 149 ( 97 unt; 0 def)
% Number of atoms : 205 ( 164 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 118 ( 62 ~; 51 |; 2 &)
% ( 1 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 229 ( 228 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] : addition(A,B) = addition(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [C,B,A] : addition(A,addition(B,C)) = addition(addition(A,B),C),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A] : addition(A,zero) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A] : addition(A,A) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A,B,C] : multiplication(A,multiplication(B,C)) = multiplication(multiplication(A,B),C),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A] : multiplication(A,one) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A] : multiplication(one,A) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A,B,C] : multiplication(A,addition(B,C)) = addition(multiplication(A,B),multiplication(A,C)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A,B,C] : multiplication(addition(A,B),C) = addition(multiplication(A,C),multiplication(B,C)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [A] : multiplication(zero,A) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [A] : addition(one,multiplication(A,star(A))) = star(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [A] : addition(one,multiplication(star(A),A)) = star(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A,B,C] :
( leq(addition(multiplication(A,C),B),C)
=> leq(multiplication(star(A),B),C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [A,B,C] :
( leq(addition(multiplication(C,A),B),C)
=> leq(multiplication(B,star(A)),C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A] : strong_iteration(A) = addition(multiplication(A,strong_iteration(A)),one),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [A] : strong_iteration(A) = addition(star(A),multiplication(strong_iteration(A),zero)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [A,B] :
( leq(A,B)
<=> addition(A,B) = B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,conjecture,
! [X0] : star(strong_iteration(X0)) = strong_iteration(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,negated_conjecture,
~ ! [X0] : star(strong_iteration(X0)) = strong_iteration(X0),
inference(negated_conjecture,[status(cth)],[f19]) ).
fof(f21,plain,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f22,plain,
! [X0,X1,X2] : addition(X0,addition(X1,X2)) = addition(addition(X0,X1),X2),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f23,plain,
! [X0] : addition(X0,zero) = X0,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f24,plain,
! [X0] : addition(X0,X0) = X0,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f25,plain,
! [X0,X1,X2] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f26,plain,
! [X0] : multiplication(X0,one) = X0,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f27,plain,
! [X0] : multiplication(one,X0) = X0,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f28,plain,
! [X0,X1,X2] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f29,plain,
! [X0,X1,X2] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f30,plain,
! [X0] : multiplication(zero,X0) = zero,
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f31,plain,
! [X0] : addition(one,multiplication(X0,star(X0))) = star(X0),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f32,plain,
! [X0] : addition(one,multiplication(star(X0),X0)) = star(X0),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f33,plain,
! [A,B,C] :
( leq(multiplication(star(A),B),C)
| ~ leq(addition(multiplication(A,C),B),C) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f34,plain,
! [X0,X1,X2] :
( leq(multiplication(star(X0),X2),X1)
| ~ leq(addition(multiplication(X0,X1),X2),X1) ),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f35,plain,
! [A,B,C] :
( leq(multiplication(B,star(A)),C)
| ~ leq(addition(multiplication(C,A),B),C) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f36,plain,
! [X0,X1,X2] :
( leq(multiplication(X2,star(X1)),X0)
| ~ leq(addition(multiplication(X0,X1),X2),X0) ),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f37,plain,
! [X0] : strong_iteration(X0) = addition(multiplication(X0,strong_iteration(X0)),one),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f40,plain,
! [X0] : strong_iteration(X0) = addition(star(X0),multiplication(strong_iteration(X0),zero)),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f41,plain,
! [A,B] :
( ( addition(A,B) != B
| leq(A,B) )
& ( addition(A,B) = B
| ~ leq(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f18]) ).
fof(f42,plain,
( ! [A,B] :
( addition(A,B) != B
| leq(A,B) )
& ! [A,B] :
( addition(A,B) = B
| ~ leq(A,B) ) ),
inference(miniscoping,[status(thm)],[f41]) ).
fof(f43,plain,
! [X0,X1] :
( addition(X0,X1) = X1
| ~ leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f44,plain,
! [X0,X1] :
( addition(X0,X1) != X1
| leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f45,plain,
? [X0] : star(strong_iteration(X0)) != strong_iteration(X0),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f46,plain,
star(strong_iteration(sK0_skl)) != strong_iteration(sK0_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X0,sK0_skl)],[f45]) ).
fof(f47,plain,
star(strong_iteration(sK0_skl)) != strong_iteration(sK0_skl),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f48,plain,
! [X0] : strong_iteration(X0) = addition(one,multiplication(X0,strong_iteration(X0))),
inference(forward_demodulation,[status(thm)],[f21,f37]) ).
fof(f50,plain,
! [X0,X1] :
( leq(multiplication(star(X0),multiplication(X0,X1)),X1)
| ~ leq(multiplication(X0,X1),X1) ),
inference(paramodulation,[status(thm)],[f24,f34]) ).
fof(f74,plain,
! [X0,X1,X2] :
( leq(multiplication(star(X1),X0),X2)
| ~ leq(addition(X0,multiplication(X1,X2)),X2) ),
inference(paramodulation,[status(thm)],[f21,f34]) ).
fof(f146,plain,
! [X0,X1] :
( ~ leq(multiplication(X0,X1),X1)
| addition(multiplication(star(X0),multiplication(X0,X1)),X1) = X1 ),
inference(resolution,[status(thm)],[f43,f50]) ).
fof(f153,plain,
! [X0,X1] :
( ~ leq(multiplication(X1,X0),X0)
| addition(X0,multiplication(star(X1),multiplication(X1,X0))) = X0 ),
inference(forward_demodulation,[status(thm)],[f21,f146]) ).
fof(f155,plain,
! [X0,X1,X2] :
( leq(multiplication(X2,star(X1)),X0)
| addition(addition(multiplication(X0,X1),X2),X0) != X0 ),
inference(resolution,[status(thm)],[f44,f36]) ).
fof(f159,plain,
! [X0,X1,X2] :
( leq(multiplication(X2,star(X1)),X0)
| addition(X0,addition(multiplication(X0,X1),X2)) != X0 ),
inference(forward_demodulation,[status(thm)],[f21,f155]) ).
fof(f229,plain,
! [X0,X1,X2] : addition(X0,addition(X1,X2)) = addition(X2,addition(X0,X1)),
inference(paramodulation,[status(thm)],[f21,f22]) ).
fof(f238,plain,
! [X0,X1,X2] : addition(X0,addition(X1,X2)) = addition(addition(X1,X0),X2),
inference(paramodulation,[status(thm)],[f21,f22]) ).
fof(f240,plain,
! [X0,X1] : addition(X0,addition(X0,X1)) = addition(X0,X1),
inference(paramodulation,[status(thm)],[f24,f22]) ).
fof(f247,plain,
! [X0,X1,X2] : addition(X0,addition(X1,X2)) = addition(X1,addition(X0,X2)),
inference(forward_demodulation,[status(thm)],[f22,f238]) ).
fof(f252,plain,
! [X0] : addition(one,star(X0)) = addition(one,multiplication(star(X0),X0)),
inference(paramodulation,[status(thm)],[f32,f240]) ).
fof(f253,plain,
! [X0] : addition(one,strong_iteration(X0)) = addition(one,multiplication(X0,strong_iteration(X0))),
inference(paramodulation,[status(thm)],[f48,f240]) ).
fof(f258,plain,
! [X0,X1] : addition(X0,addition(X1,X0)) = addition(X0,X1),
inference(paramodulation,[status(thm)],[f21,f240]) ).
fof(f272,plain,
! [X0] : addition(one,star(X0)) = star(X0),
inference(forward_demodulation,[status(thm)],[f32,f252]) ).
fof(f274,plain,
! [X0] : addition(one,strong_iteration(X0)) = strong_iteration(X0),
inference(forward_demodulation,[status(thm)],[f48,f253]) ).
fof(f288,plain,
! [X0,X1] : addition(one,addition(strong_iteration(X0),X1)) = addition(strong_iteration(X0),X1),
inference(paramodulation,[status(thm)],[f274,f22]) ).
fof(f319,plain,
! [X0,X1] : multiplication(X0,addition(one,X1)) = addition(X0,multiplication(X0,X1)),
inference(paramodulation,[status(thm)],[f26,f28]) ).
fof(f361,plain,
! [X0,X1] : multiplication(addition(one,X0),X1) = addition(X1,multiplication(X0,X1)),
inference(paramodulation,[status(thm)],[f27,f29]) ).
fof(f486,plain,
! [X0,X1] :
( ~ leq(addition(X0,multiplication(X1,X0)),X0)
| addition(X0,multiplication(star(star(X1)),multiplication(star(X1),X0))) = X0 ),
inference(resolution,[status(thm)],[f153,f74]) ).
fof(f492,plain,
! [X0,X1] :
( addition(multiplication(X1,X0),X0) != X0
| addition(X0,multiplication(star(X1),multiplication(X1,X0))) = X0 ),
inference(resolution,[status(thm)],[f153,f44]) ).
fof(f506,plain,
! [X0,X1] :
( ~ leq(multiplication(addition(one,X1),X0),X0)
| addition(X0,multiplication(star(star(X1)),multiplication(star(X1),X0))) = X0 ),
inference(forward_demodulation,[status(thm)],[f361,f486]) ).
fof(f510,plain,
! [X0,X1] :
( addition(X0,multiplication(X1,X0)) != X0
| addition(X0,multiplication(star(X1),multiplication(X1,X0))) = X0 ),
inference(forward_demodulation,[status(thm)],[f21,f492]) ).
fof(f511,plain,
! [X0,X1] :
( multiplication(addition(one,X1),X0) != X0
| addition(X0,multiplication(star(X1),multiplication(X1,X0))) = X0 ),
inference(forward_demodulation,[status(thm)],[f361,f510]) ).
fof(f547,plain,
! [X0] :
( multiplication(addition(one,one),X0) != X0
| addition(X0,multiplication(star(one),X0)) = X0 ),
inference(paramodulation,[status(thm)],[f27,f511]) ).
fof(f552,plain,
! [X0] :
( multiplication(addition(one,one),X0) != X0
| multiplication(addition(one,star(one)),X0) = X0 ),
inference(forward_demodulation,[status(thm)],[f361,f547]) ).
fof(f553,plain,
! [X0] :
( multiplication(addition(one,one),X0) != X0
| multiplication(star(one),X0) = X0 ),
inference(forward_demodulation,[status(thm)],[f272,f552]) ).
fof(f554,plain,
! [X0] :
( multiplication(one,X0) != X0
| multiplication(star(one),X0) = X0 ),
inference(forward_demodulation,[status(thm)],[f24,f553]) ).
fof(f555,plain,
! [X0] :
( X0 != X0
| multiplication(star(one),X0) = X0 ),
inference(forward_demodulation,[status(thm)],[f27,f554]) ).
fof(f560,plain,
! [X0] : multiplication(star(one),X0) = X0,
inference(trivial_equality_resolution,[status(thm)],[f555]) ).
fof(f563,plain,
star(one) = one,
inference(paramodulation,[status(thm)],[f26,f560]) ).
fof(f811,plain,
! [X0] : addition(multiplication(star(X0),X0),star(X0)) = addition(multiplication(star(X0),X0),one),
inference(paramodulation,[status(thm)],[f32,f258]) ).
fof(f812,plain,
! [X0] : addition(multiplication(X0,strong_iteration(X0)),strong_iteration(X0)) = addition(multiplication(X0,strong_iteration(X0)),one),
inference(paramodulation,[status(thm)],[f48,f258]) ).
fof(f813,plain,
! [X0] : addition(multiplication(X0,star(X0)),star(X0)) = addition(multiplication(X0,star(X0)),one),
inference(paramodulation,[status(thm)],[f31,f258]) ).
fof(f831,plain,
! [X0,X1,X2] : addition(X0,addition(addition(X1,X0),X2)) = addition(addition(X0,X1),X2),
inference(paramodulation,[status(thm)],[f258,f22]) ).
fof(f843,plain,
! [X0] : addition(star(X0),multiplication(star(X0),X0)) = addition(multiplication(star(X0),X0),one),
inference(forward_demodulation,[status(thm)],[f21,f811]) ).
fof(f844,plain,
! [X0] : multiplication(star(X0),addition(one,X0)) = addition(multiplication(star(X0),X0),one),
inference(forward_demodulation,[status(thm)],[f319,f843]) ).
fof(f845,plain,
! [X0] : multiplication(star(X0),addition(one,X0)) = addition(one,multiplication(star(X0),X0)),
inference(forward_demodulation,[status(thm)],[f21,f844]) ).
fof(f846,plain,
! [X0] : multiplication(star(X0),addition(one,X0)) = star(X0),
inference(forward_demodulation,[status(thm)],[f32,f845]) ).
fof(f847,plain,
! [X0] : addition(strong_iteration(X0),multiplication(X0,strong_iteration(X0))) = addition(multiplication(X0,strong_iteration(X0)),one),
inference(forward_demodulation,[status(thm)],[f21,f812]) ).
fof(f848,plain,
! [X0] : multiplication(addition(one,X0),strong_iteration(X0)) = addition(multiplication(X0,strong_iteration(X0)),one),
inference(forward_demodulation,[status(thm)],[f361,f847]) ).
fof(f849,plain,
! [X0] : multiplication(addition(one,X0),strong_iteration(X0)) = addition(one,multiplication(X0,strong_iteration(X0))),
inference(forward_demodulation,[status(thm)],[f21,f848]) ).
fof(f850,plain,
! [X0] : multiplication(addition(one,X0),strong_iteration(X0)) = strong_iteration(X0),
inference(forward_demodulation,[status(thm)],[f48,f849]) ).
fof(f851,plain,
! [X0] : addition(star(X0),multiplication(X0,star(X0))) = addition(multiplication(X0,star(X0)),one),
inference(forward_demodulation,[status(thm)],[f21,f813]) ).
fof(f852,plain,
! [X0] : multiplication(addition(one,X0),star(X0)) = addition(multiplication(X0,star(X0)),one),
inference(forward_demodulation,[status(thm)],[f361,f851]) ).
fof(f853,plain,
! [X0] : multiplication(addition(one,X0),star(X0)) = addition(one,multiplication(X0,star(X0))),
inference(forward_demodulation,[status(thm)],[f21,f852]) ).
fof(f854,plain,
! [X0] : multiplication(addition(one,X0),star(X0)) = star(X0),
inference(forward_demodulation,[status(thm)],[f31,f853]) ).
fof(f872,plain,
! [X0,X1,X2] : addition(X0,addition(X1,addition(X0,X2))) = addition(addition(X0,X1),X2),
inference(forward_demodulation,[status(thm)],[f22,f831]) ).
fof(f874,plain,
! [X0,X1,X2] : addition(X0,addition(X1,addition(X0,X2))) = addition(X0,addition(X1,X2)),
inference(forward_demodulation,[status(thm)],[f22,f872]) ).
fof(f1021,plain,
! [X0] : multiplication(star(star(X0)),star(X0)) = star(star(X0)),
inference(paramodulation,[status(thm)],[f272,f846]) ).
fof(f1399,plain,
! [X0,X1,X2] : addition(X0,addition(X1,addition(X0,X2))) = addition(X0,addition(X2,X1)),
inference(paramodulation,[status(thm)],[f229,f240]) ).
fof(f1482,plain,
! [X0,X1,X2] : addition(X0,addition(X1,X2)) = addition(X0,addition(X2,X1)),
inference(forward_demodulation,[status(thm)],[f874,f1399]) ).
fof(f1515,plain,
! [X0,X1] : addition(X0,star(X1)) = addition(one,addition(X0,star(X1))),
inference(paramodulation,[status(thm)],[f272,f247]) ).
fof(f2279,plain,
! [X0,X1] :
( leq(star(X1),X0)
| addition(X0,addition(multiplication(X0,X1),one)) != X0 ),
inference(paramodulation,[status(thm)],[f27,f159]) ).
fof(f2280,plain,
! [X0,X1] :
( leq(multiplication(X1,one),X0)
| addition(X0,addition(multiplication(X0,one),X1)) != X0 ),
inference(paramodulation,[status(thm)],[f563,f159]) ).
fof(f2302,plain,
! [X0,X1] :
( leq(star(X1),X0)
| addition(X0,addition(one,multiplication(X0,X1))) != X0 ),
inference(forward_demodulation,[status(thm)],[f1482,f2279]) ).
fof(f2303,plain,
! [X0,X1] :
( leq(multiplication(X1,one),X0)
| addition(X0,addition(X0,X1)) != X0 ),
inference(forward_demodulation,[status(thm)],[f26,f2280]) ).
fof(f2304,plain,
! [X0,X1] :
( leq(multiplication(X1,one),X0)
| addition(X0,X1) != X0 ),
inference(forward_demodulation,[status(thm)],[f240,f2303]) ).
fof(f2305,plain,
! [X0,X1] :
( leq(X1,X0)
| addition(X0,X1) != X0 ),
inference(forward_demodulation,[status(thm)],[f26,f2304]) ).
fof(f3524,plain,
! [X0] : multiplication(addition(one,X0),addition(one,star(X0))) = addition(addition(one,X0),star(X0)),
inference(paramodulation,[status(thm)],[f854,f319]) ).
fof(f3550,plain,
! [X0] :
( multiplication(addition(one,X0),star(X0)) != star(X0)
| multiplication(star(X0),addition(one,multiplication(X0,star(X0)))) = star(X0) ),
inference(paramodulation,[status(thm)],[f319,f511]) ).
fof(f3586,plain,
! [X0] : multiplication(addition(one,X0),star(X0)) = addition(addition(one,X0),star(X0)),
inference(forward_demodulation,[status(thm)],[f272,f3524]) ).
fof(f3587,plain,
! [X0] : star(X0) = addition(addition(one,X0),star(X0)),
inference(forward_demodulation,[status(thm)],[f854,f3586]) ).
fof(f3588,plain,
! [X0] : star(X0) = addition(one,addition(X0,star(X0))),
inference(forward_demodulation,[status(thm)],[f22,f3587]) ).
fof(f3589,plain,
! [X0] : star(X0) = addition(X0,star(X0)),
inference(forward_demodulation,[status(thm)],[f1515,f3588]) ).
fof(f3645,plain,
! [X0] :
( multiplication(addition(one,X0),star(X0)) != star(X0)
| multiplication(star(X0),star(X0)) = star(X0) ),
inference(forward_demodulation,[status(thm)],[f31,f3550]) ).
fof(f3646,plain,
! [X0] :
( star(X0) != star(X0)
| multiplication(star(X0),star(X0)) = star(X0) ),
inference(forward_demodulation,[status(thm)],[f854,f3645]) ).
fof(f3647,plain,
! [X0] : multiplication(star(X0),star(X0)) = star(X0),
inference(trivial_equality_resolution,[status(thm)],[f3646]) ).
fof(f3822,plain,
! [X0] :
( multiplication(addition(one,star(X0)),star(X0)) != star(X0)
| addition(star(X0),multiplication(star(star(X0)),star(X0))) = star(X0) ),
inference(paramodulation,[status(thm)],[f3647,f511]) ).
fof(f3830,plain,
! [X0,X1] : multiplication(star(X0),multiplication(star(X0),X1)) = multiplication(star(X0),X1),
inference(paramodulation,[status(thm)],[f3647,f25]) ).
fof(f3842,plain,
! [X0] :
( multiplication(addition(one,star(X0)),star(X0)) != star(X0)
| multiplication(addition(one,star(star(X0))),star(X0)) = star(X0) ),
inference(forward_demodulation,[status(thm)],[f361,f3822]) ).
fof(f3843,plain,
! [X0] :
( multiplication(addition(one,star(X0)),star(X0)) != star(X0)
| multiplication(star(star(X0)),star(X0)) = star(X0) ),
inference(forward_demodulation,[status(thm)],[f272,f3842]) ).
fof(f3844,plain,
! [X0] :
( multiplication(addition(one,star(X0)),star(X0)) != star(X0)
| star(star(X0)) = star(X0) ),
inference(forward_demodulation,[status(thm)],[f1021,f3843]) ).
fof(f3845,plain,
! [X0] :
( multiplication(star(X0),star(X0)) != star(X0)
| star(star(X0)) = star(X0) ),
inference(forward_demodulation,[status(thm)],[f272,f3844]) ).
fof(f3846,plain,
! [X0] :
( star(X0) != star(X0)
| star(star(X0)) = star(X0) ),
inference(forward_demodulation,[status(thm)],[f3647,f3845]) ).
fof(f3868,plain,
! [X0,X1] :
( ~ leq(multiplication(addition(one,X1),X0),X0)
| addition(X0,multiplication(star(X1),multiplication(star(X1),X0))) = X0 ),
inference(backward_demodulation,[status(thm)],[f3875,f506]) ).
fof(f3875,plain,
! [X0] : star(star(X0)) = star(X0),
inference(trivial_equality_resolution,[status(thm)],[f3846]) ).
fof(f3905,plain,
! [X0,X1] :
( ~ leq(multiplication(addition(one,X1),X0),X0)
| addition(X0,multiplication(star(X1),X0)) = X0 ),
inference(forward_demodulation,[status(thm)],[f3830,f3868]) ).
fof(f3906,plain,
! [X0,X1] :
( ~ leq(multiplication(addition(one,X0),X1),X1)
| multiplication(addition(one,star(X0)),X1) = X1 ),
inference(forward_demodulation,[status(thm)],[f361,f3905]) ).
fof(f3907,plain,
! [X0,X1] :
( ~ leq(multiplication(addition(one,X0),X1),X1)
| multiplication(star(X0),X1) = X1 ),
inference(forward_demodulation,[status(thm)],[f272,f3906]) ).
fof(f3981,plain,
! [X0] : multiplication(addition(one,X0),X0) = multiplication(X0,addition(one,X0)),
inference(paramodulation,[status(thm)],[f319,f361]) ).
fof(f3991,plain,
! [X0,X1,X2] : multiplication(addition(one,multiplication(X0,X1)),X2) = addition(X2,multiplication(X0,multiplication(X1,X2))),
inference(paramodulation,[status(thm)],[f25,f361]) ).
fof(f7412,plain,
! [X0,X1] :
( addition(star(X1),X0) = X0
| addition(X0,addition(one,multiplication(X0,X1))) != X0 ),
inference(resolution,[status(thm)],[f2302,f43]) ).
fof(f11067,plain,
! [X0] :
( ~ leq(strong_iteration(X0),strong_iteration(X0))
| multiplication(star(X0),strong_iteration(X0)) = strong_iteration(X0) ),
inference(paramodulation,[status(thm)],[f850,f3907]) ).
fof(f13146,plain,
! [X0,X1] :
( addition(X0,star(X1)) = X0
| addition(X0,addition(one,multiplication(X0,X1))) != X0 ),
inference(paramodulation,[status(thm)],[f21,f7412]) ).
fof(f13319,plain,
! [X0] :
( addition(strong_iteration(X0),strong_iteration(X0)) != strong_iteration(X0)
| multiplication(star(X0),strong_iteration(X0)) = strong_iteration(X0) ),
inference(resolution,[status(thm)],[f11067,f2305]) ).
fof(f13325,plain,
! [X0] :
( strong_iteration(X0) != strong_iteration(X0)
| multiplication(star(X0),strong_iteration(X0)) = strong_iteration(X0) ),
inference(forward_demodulation,[status(thm)],[f24,f13319]) ).
fof(f13327,plain,
! [X0] : multiplication(star(X0),strong_iteration(X0)) = strong_iteration(X0),
inference(trivial_equality_resolution,[status(thm)],[f13325]) ).
fof(f13353,plain,
! [X0,X1] : multiplication(addition(star(X0),X1),strong_iteration(X0)) = addition(strong_iteration(X0),multiplication(X1,strong_iteration(X0))),
inference(paramodulation,[status(thm)],[f13327,f29]) ).
fof(f13382,plain,
! [X0,X1] : multiplication(addition(star(X0),X1),strong_iteration(X0)) = multiplication(addition(one,X1),strong_iteration(X0)),
inference(forward_demodulation,[status(thm)],[f361,f13353]) ).
fof(f13476,plain,
! [X0] :
( star(X0) = X0
| addition(X0,addition(one,multiplication(X0,X0))) != X0 ),
inference(paramodulation,[status(thm)],[f3589,f13146]) ).
fof(f13601,plain,
addition(strong_iteration(sK0_skl),addition(one,multiplication(strong_iteration(sK0_skl),strong_iteration(sK0_skl)))) != strong_iteration(sK0_skl),
inference(resolution,[status(thm)],[f13476,f47]) ).
fof(f13605,plain,
addition(one,addition(strong_iteration(sK0_skl),multiplication(strong_iteration(sK0_skl),strong_iteration(sK0_skl)))) != strong_iteration(sK0_skl),
inference(forward_demodulation,[status(thm)],[f247,f13601]) ).
fof(f13606,plain,
addition(strong_iteration(sK0_skl),multiplication(strong_iteration(sK0_skl),strong_iteration(sK0_skl))) != strong_iteration(sK0_skl),
inference(forward_demodulation,[status(thm)],[f288,f13605]) ).
fof(f13607,plain,
multiplication(addition(one,strong_iteration(sK0_skl)),strong_iteration(sK0_skl)) != strong_iteration(sK0_skl),
inference(forward_demodulation,[status(thm)],[f361,f13606]) ).
fof(f13608,plain,
multiplication(strong_iteration(sK0_skl),addition(one,strong_iteration(sK0_skl))) != strong_iteration(sK0_skl),
inference(forward_demodulation,[status(thm)],[f3981,f13607]) ).
fof(f13609,plain,
multiplication(strong_iteration(sK0_skl),strong_iteration(sK0_skl)) != strong_iteration(sK0_skl),
inference(forward_demodulation,[status(thm)],[f274,f13608]) ).
fof(f18701,plain,
! [X0,X1] : multiplication(addition(one,multiplication(X0,zero)),X1) = addition(X1,multiplication(X0,zero)),
inference(paramodulation,[status(thm)],[f30,f3991]) ).
fof(f20265,plain,
! [X0] : multiplication(strong_iteration(X0),strong_iteration(X0)) = multiplication(addition(one,multiplication(strong_iteration(X0),zero)),strong_iteration(X0)),
inference(paramodulation,[status(thm)],[f40,f13382]) ).
fof(f20336,plain,
! [X0] : multiplication(strong_iteration(X0),strong_iteration(X0)) = addition(strong_iteration(X0),multiplication(strong_iteration(X0),zero)),
inference(forward_demodulation,[status(thm)],[f18701,f20265]) ).
fof(f20337,plain,
! [X0] : multiplication(strong_iteration(X0),strong_iteration(X0)) = multiplication(strong_iteration(X0),addition(one,zero)),
inference(forward_demodulation,[status(thm)],[f319,f20336]) ).
fof(f20338,plain,
! [X0] : multiplication(strong_iteration(X0),strong_iteration(X0)) = multiplication(strong_iteration(X0),one),
inference(forward_demodulation,[status(thm)],[f23,f20337]) ).
fof(f20339,plain,
strong_iteration(sK0_skl) != strong_iteration(sK0_skl),
inference(backward_demodulation,[status(thm)],[f20341,f13609]) ).
fof(f20341,plain,
! [X0] : multiplication(strong_iteration(X0),strong_iteration(X0)) = strong_iteration(X0),
inference(forward_demodulation,[status(thm)],[f26,f20338]) ).
fof(f20429,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f20339]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KLE145+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n020.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 20 22:47:17 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.38 % Drodi V4.1.1
% 57.76/7.78 % Refutation found
% 57.76/7.78 % SZS status Theorem for theBenchmark: Theorem is valid
% 57.76/7.78 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.69/8.07 % Elapsed time: 7.686823 seconds
% 3.69/8.07 % CPU time: 59.209323 seconds
% 3.69/8.07 % Total memory used: 435.583 MB
% 3.69/8.07 % Net memory used: 407.310 MB
%------------------------------------------------------------------------------