%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : KLE041+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/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:57:50 PM UTC 2026
% Result : Theorem 3.02s 0.89s
% Output : CNFRefutation 3.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 15
% Syntax : Number of formulae : 146 ( 108 unt; 0 def)
% Number of atoms : 188 ( 115 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 92 ( 50 ~; 33 |; 4 &)
% ( 1 <=>; 4 =>; 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; 4 con; 0-2 aty)
% Number of variables : 206 ( 204 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] : addition(A,B) = addition(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [C,B,A] : addition(A,addition(B,C)) = addition(addition(A,B),C),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A] : addition(A,zero) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A] : addition(A,A) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A] : multiplication(A,one) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [A] : multiplication(one,A) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A,B,C] : multiplication(A,addition(B,C)) = addition(multiplication(A,B),multiplication(A,C)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A,B,C] : multiplication(addition(A,B),C) = addition(multiplication(A,C),multiplication(B,C)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [A] : multiplication(A,zero) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [A] : multiplication(zero,A) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [A,B] :
( leq(A,B)
<=> addition(A,B) = B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A] : leq(addition(one,multiplication(A,star(A))),star(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A,B,C] :
( leq(addition(multiplication(A,B),C),B)
=> leq(multiplication(star(A),C),B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [A,B,C] :
( leq(addition(multiplication(A,B),C),A)
=> leq(multiplication(C,star(B)),A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,conjecture,
! [X0,X1] :
( leq(X0,X1)
=> leq(star(X0),star(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,negated_conjecture,
~ ! [X0,X1] :
( leq(X0,X1)
=> leq(star(X0),star(X1)) ),
inference(negated_conjecture,[status(cth)],[f17]) ).
fof(f19,plain,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f20,plain,
! [X0,X1,X2] : addition(X0,addition(X1,X2)) = addition(addition(X0,X1),X2),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f21,plain,
! [X0] : addition(X0,zero) = X0,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f22,plain,
! [X0] : addition(X0,X0) = X0,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f24,plain,
! [X0] : multiplication(X0,one) = X0,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f25,plain,
! [X0] : multiplication(one,X0) = X0,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f26,plain,
! [X0,X1,X2] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f27,plain,
! [X0,X1,X2] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f28,plain,
! [X0] : multiplication(X0,zero) = zero,
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f29,plain,
! [X0] : multiplication(zero,X0) = zero,
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f30,plain,
! [A,B] :
( ( addition(A,B) != B
| leq(A,B) )
& ( addition(A,B) = B
| ~ leq(A,B) ) ),
inference(NNF_transformation,[status(thm)],[f12]) ).
fof(f31,plain,
( ! [A,B] :
( addition(A,B) != B
| leq(A,B) )
& ! [A,B] :
( addition(A,B) = B
| ~ leq(A,B) ) ),
inference(miniscoping,[status(thm)],[f30]) ).
fof(f32,plain,
! [X0,X1] :
( addition(X0,X1) = X1
| ~ leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f33,plain,
! [X0,X1] :
( addition(X0,X1) != X1
| leq(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f34,plain,
! [X0] : leq(addition(one,multiplication(X0,star(X0))),star(X0)),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f36,plain,
! [A,B,C] :
( leq(multiplication(star(A),C),B)
| ~ leq(addition(multiplication(A,B),C),B) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f37,plain,
! [X0,X1,X2] :
( leq(multiplication(star(X0),X2),X1)
| ~ leq(addition(multiplication(X0,X1),X2),X1) ),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f38,plain,
! [A,B,C] :
( leq(multiplication(C,star(B)),A)
| ~ leq(addition(multiplication(A,B),C),A) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f39,plain,
! [X0,X1,X2] :
( leq(multiplication(X2,star(X1)),X0)
| ~ leq(addition(multiplication(X0,X1),X2),X0) ),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f40,plain,
? [X0,X1] :
( ~ leq(star(X0),star(X1))
& leq(X0,X1) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f41,plain,
( ~ leq(star(sK0_skl),star(sK1_skl))
& leq(sK0_skl,sK1_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(X0,sK0_skl),skolemize(X1,sK1_skl)],[f40]) ).
fof(f42,plain,
leq(sK0_skl,sK1_skl),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f43,plain,
~ leq(star(sK0_skl),star(sK1_skl)),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f44,plain,
addition(sK0_skl,sK1_skl) = sK1_skl,
inference(resolution,[status(thm)],[f32,f42]) ).
fof(f45,plain,
! [X0,X1,X2] :
( leq(multiplication(star(X0),X2),X1)
| addition(addition(multiplication(X0,X1),X2),X1) != X1 ),
inference(resolution,[status(thm)],[f33,f37]) ).
fof(f48,plain,
! [X0,X1,X2] :
( leq(multiplication(star(X0),X2),X1)
| addition(multiplication(X0,X1),addition(X2,X1)) != X1 ),
inference(forward_demodulation,[status(thm)],[f20,f45]) ).
fof(f49,plain,
! [X0,X1,X2] :
( addition(multiplication(X2,star(X1)),X0) = X0
| ~ leq(addition(multiplication(X0,X1),X2),X0) ),
inference(resolution,[status(thm)],[f39,f32]) ).
fof(f50,plain,
! [X0,X1] :
( leq(multiplication(star(X0),multiplication(X0,X1)),X1)
| ~ leq(multiplication(X0,X1),X1) ),
inference(paramodulation,[status(thm)],[f22,f37]) ).
fof(f56,plain,
! [X0] : X0 = addition(zero,X0),
inference(paramodulation,[status(thm)],[f21,f19]) ).
fof(f67,plain,
! [X0,X1,X2] : addition(X0,addition(X1,X2)) = addition(X2,addition(X0,X1)),
inference(paramodulation,[status(thm)],[f19,f20]) ).
fof(f72,plain,
! [X0,X1,X2] : addition(X0,addition(X1,X2)) = addition(addition(X1,X0),X2),
inference(paramodulation,[status(thm)],[f19,f20]) ).
fof(f74,plain,
! [X0,X1] : addition(X0,addition(X0,X1)) = addition(X0,X1),
inference(paramodulation,[status(thm)],[f22,f20]) ).
fof(f79,plain,
! [X0,X1,X2] :
( leq(multiplication(star(X1),X2),X0)
| addition(X0,addition(multiplication(X1,X0),X2)) != X0 ),
inference(backward_demodulation,[status(thm)],[f67,f48]) ).
fof(f82,plain,
! [X0,X1,X2] : addition(X0,addition(X1,X2)) = addition(X1,addition(X0,X2)),
inference(forward_demodulation,[status(thm)],[f20,f72]) ).
fof(f92,plain,
! [X0] : addition(sK0_skl,addition(sK1_skl,X0)) = addition(sK1_skl,X0),
inference(paramodulation,[status(thm)],[f44,f20]) ).
fof(f116,plain,
! [X0,X1] :
( leq(star(X1),X0)
| ~ leq(addition(multiplication(X0,X1),one),X0) ),
inference(paramodulation,[status(thm)],[f25,f39]) ).
fof(f117,plain,
! [X0] :
( leq(multiplication(star(one),X0),X0)
| ~ leq(multiplication(one,X0),X0) ),
inference(paramodulation,[status(thm)],[f25,f50]) ).
fof(f120,plain,
! [X0,X1] :
( leq(multiplication(star(one),X1),X0)
| ~ leq(addition(X0,X1),X0) ),
inference(paramodulation,[status(thm)],[f25,f37]) ).
fof(f121,plain,
! [X0,X1] :
( leq(star(X1),X0)
| ~ leq(addition(one,multiplication(X0,X1)),X0) ),
inference(forward_demodulation,[status(thm)],[f19,f116]) ).
fof(f122,plain,
! [X0] :
( leq(multiplication(star(one),X0),X0)
| ~ leq(X0,X0) ),
inference(forward_demodulation,[status(thm)],[f25,f117]) ).
fof(f139,plain,
! [X0,X1] :
( addition(multiplication(X0,star(zero)),X1) = X1
| ~ leq(addition(zero,X0),X1) ),
inference(paramodulation,[status(thm)],[f28,f49]) ).
fof(f146,plain,
! [X0,X1] :
( addition(multiplication(X0,star(zero)),X1) = X1
| ~ leq(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f56,f139]) ).
fof(f150,plain,
! [X0,X1,X2] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X2),multiplication(X0,X1)),
inference(paramodulation,[status(thm)],[f19,f26]) ).
fof(f160,plain,
! [X0,X1] : multiplication(X0,addition(X1,one)) = addition(multiplication(X0,X1),X0),
inference(paramodulation,[status(thm)],[f24,f26]) ).
fof(f167,plain,
! [X0,X1,X2] : multiplication(X0,addition(X1,X2)) = multiplication(X0,addition(X2,X1)),
inference(forward_demodulation,[status(thm)],[f26,f150]) ).
fof(f179,plain,
! [X0,X1] : multiplication(X0,addition(X1,one)) = addition(X0,multiplication(X0,X1)),
inference(forward_demodulation,[status(thm)],[f19,f160]) ).
fof(f185,plain,
! [X0,X1,X2] : multiplication(addition(X0,X1),X2) = addition(multiplication(X1,X2),multiplication(X0,X2)),
inference(paramodulation,[status(thm)],[f19,f27]) ).
fof(f188,plain,
! [X0,X1] : multiplication(addition(one,X0),X1) = addition(X1,multiplication(X0,X1)),
inference(paramodulation,[status(thm)],[f25,f27]) ).
fof(f192,plain,
! [X0,X1] : multiplication(addition(X0,one),X1) = addition(multiplication(X0,X1),X1),
inference(paramodulation,[status(thm)],[f25,f27]) ).
fof(f204,plain,
! [X0,X1,X2] : multiplication(addition(X0,X1),X2) = multiplication(addition(X1,X0),X2),
inference(forward_demodulation,[status(thm)],[f27,f185]) ).
fof(f209,plain,
! [X0,X1] : multiplication(addition(X0,one),X1) = addition(X1,multiplication(X0,X1)),
inference(forward_demodulation,[status(thm)],[f19,f192]) ).
fof(f229,plain,
! [X0,X1] :
( leq(multiplication(star(zero),X0),X1)
| ~ leq(addition(zero,X0),X1) ),
inference(paramodulation,[status(thm)],[f29,f37]) ).
fof(f241,plain,
! [X0,X1] :
( leq(multiplication(star(zero),X0),X1)
| ~ leq(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f56,f229]) ).
fof(f243,plain,
! [X0] : addition(sK0_skl,addition(X0,sK1_skl)) = addition(sK1_skl,X0),
inference(paramodulation,[status(thm)],[f19,f92]) ).
fof(f259,plain,
! [X0,X1] : addition(sK0_skl,addition(addition(X0,sK1_skl),X1)) = addition(addition(sK1_skl,X0),X1),
inference(paramodulation,[status(thm)],[f243,f20]) ).
fof(f264,plain,
! [X0,X1] : addition(sK0_skl,addition(X0,addition(sK1_skl,X1))) = addition(addition(sK1_skl,X0),X1),
inference(forward_demodulation,[status(thm)],[f20,f259]) ).
fof(f265,plain,
! [X0,X1] : addition(sK0_skl,addition(X0,addition(sK1_skl,X1))) = addition(sK1_skl,addition(X0,X1)),
inference(forward_demodulation,[status(thm)],[f20,f264]) ).
fof(f267,plain,
! [X0] :
( addition(multiplication(star(one),X0),X0) = X0
| ~ leq(X0,X0) ),
inference(resolution,[status(thm)],[f122,f32]) ).
fof(f270,plain,
! [X0] :
( addition(X0,multiplication(star(one),X0)) = X0
| ~ leq(X0,X0) ),
inference(forward_demodulation,[status(thm)],[f19,f267]) ).
fof(f311,plain,
! [X0,X1] : addition(X0,addition(X1,X0)) = addition(X0,X1),
inference(paramodulation,[status(thm)],[f19,f74]) ).
fof(f365,plain,
! [X0,X1,X2] : addition(X0,addition(addition(X1,X0),X2)) = addition(addition(X0,X1),X2),
inference(paramodulation,[status(thm)],[f311,f20]) ).
fof(f401,plain,
! [X0,X1,X2] : addition(X0,addition(X1,addition(X0,X2))) = addition(addition(X0,X1),X2),
inference(forward_demodulation,[status(thm)],[f20,f365]) ).
fof(f403,plain,
! [X0,X1,X2] : addition(X0,addition(X1,addition(X0,X2))) = addition(X0,addition(X1,X2)),
inference(forward_demodulation,[status(thm)],[f20,f401]) ).
fof(f405,plain,
! [X0] : addition(addition(one,multiplication(X0,star(X0))),star(X0)) = star(X0),
inference(resolution,[status(thm)],[f34,f32]) ).
fof(f406,plain,
leq(addition(one,zero),star(zero)),
inference(paramodulation,[status(thm)],[f29,f34]) ).
fof(f407,plain,
leq(addition(one,star(one)),star(one)),
inference(paramodulation,[status(thm)],[f25,f34]) ).
fof(f409,plain,
! [X0] : addition(one,addition(multiplication(X0,star(X0)),star(X0))) = star(X0),
inference(forward_demodulation,[status(thm)],[f20,f405]) ).
fof(f410,plain,
! [X0] : addition(one,addition(star(X0),multiplication(X0,star(X0)))) = star(X0),
inference(forward_demodulation,[status(thm)],[f19,f409]) ).
fof(f411,plain,
! [X0] : addition(one,multiplication(addition(X0,one),star(X0))) = star(X0),
inference(forward_demodulation,[status(thm)],[f209,f410]) ).
fof(f412,plain,
leq(one,star(zero)),
inference(forward_demodulation,[status(thm)],[f21,f406]) ).
fof(f479,plain,
! [X0,X1,X2] : addition(X0,addition(X1,addition(X0,X2))) = addition(X0,addition(X2,X1)),
inference(paramodulation,[status(thm)],[f67,f74]) ).
fof(f552,plain,
! [X0,X1,X2] : addition(X0,addition(X1,X2)) = addition(X0,addition(X2,X1)),
inference(forward_demodulation,[status(thm)],[f403,f479]) ).
fof(f745,plain,
! [X0] :
( leq(star(zero),X0)
| ~ leq(one,X0) ),
inference(paramodulation,[status(thm)],[f24,f241]) ).
fof(f780,plain,
leq(star(zero),star(zero)),
inference(resolution,[status(thm)],[f412,f745]) ).
fof(f781,plain,
addition(one,star(zero)) = star(zero),
inference(resolution,[status(thm)],[f412,f32]) ).
fof(f982,plain,
~ leq(addition(one,multiplication(star(sK1_skl),sK0_skl)),star(sK1_skl)),
inference(resolution,[status(thm)],[f121,f43]) ).
fof(f1279,plain,
addition(multiplication(addition(one,star(one)),star(zero)),star(one)) = star(one),
inference(resolution,[status(thm)],[f407,f146]) ).
fof(f1280,plain,
addition(addition(one,star(one)),star(one)) = star(one),
inference(resolution,[status(thm)],[f407,f32]) ).
fof(f1281,plain,
addition(star(one),multiplication(addition(one,star(one)),star(zero))) = star(one),
inference(forward_demodulation,[status(thm)],[f19,f1279]) ).
fof(f1282,plain,
addition(one,addition(star(one),star(one))) = star(one),
inference(forward_demodulation,[status(thm)],[f20,f1280]) ).
fof(f1284,plain,
addition(star(one),multiplication(star(one),star(zero))) = star(one),
inference(backward_demodulation,[status(thm)],[f1285,f1281]) ).
fof(f1285,plain,
addition(one,star(one)) = star(one),
inference(forward_demodulation,[status(thm)],[f22,f1282]) ).
fof(f1286,plain,
multiplication(star(one),addition(star(zero),one)) = star(one),
inference(forward_demodulation,[status(thm)],[f179,f1284]) ).
fof(f1287,plain,
multiplication(star(one),addition(one,star(zero))) = star(one),
inference(forward_demodulation,[status(thm)],[f167,f1286]) ).
fof(f1288,plain,
multiplication(star(one),star(zero)) = star(one),
inference(forward_demodulation,[status(thm)],[f781,f1287]) ).
fof(f1827,plain,
! [X0] : addition(multiplication(addition(X0,one),star(X0)),star(X0)) = addition(multiplication(addition(X0,one),star(X0)),one),
inference(paramodulation,[status(thm)],[f411,f311]) ).
fof(f1828,plain,
! [X0] : addition(one,star(X0)) = addition(one,multiplication(addition(X0,one),star(X0))),
inference(paramodulation,[status(thm)],[f411,f74]) ).
fof(f1833,plain,
! [X0] : addition(star(X0),multiplication(addition(X0,one),star(X0))) = addition(multiplication(addition(X0,one),star(X0)),one),
inference(forward_demodulation,[status(thm)],[f19,f1827]) ).
fof(f1834,plain,
! [X0] : multiplication(addition(addition(X0,one),one),star(X0)) = addition(multiplication(addition(X0,one),star(X0)),one),
inference(forward_demodulation,[status(thm)],[f209,f1833]) ).
fof(f1835,plain,
! [X0] : multiplication(addition(one,addition(X0,one)),star(X0)) = addition(multiplication(addition(X0,one),star(X0)),one),
inference(forward_demodulation,[status(thm)],[f204,f1834]) ).
fof(f1836,plain,
! [X0] : multiplication(addition(one,X0),star(X0)) = addition(multiplication(addition(X0,one),star(X0)),one),
inference(forward_demodulation,[status(thm)],[f311,f1835]) ).
fof(f1837,plain,
! [X0] : multiplication(addition(one,X0),star(X0)) = addition(one,multiplication(addition(X0,one),star(X0))),
inference(forward_demodulation,[status(thm)],[f19,f1836]) ).
fof(f1839,plain,
! [X0] : multiplication(addition(one,X0),star(X0)) = star(X0),
inference(forward_demodulation,[status(thm)],[f411,f1837]) ).
fof(f1842,plain,
! [X0] : addition(one,star(X0)) = star(X0),
inference(forward_demodulation,[status(thm)],[f411,f1828]) ).
fof(f1845,plain,
! [X0,X1] : addition(one,addition(X0,star(X1))) = addition(X0,star(X1)),
inference(paramodulation,[status(thm)],[f1842,f82]) ).
fof(f1847,plain,
! [X0,X1] : addition(one,addition(star(X0),X1)) = addition(X1,star(X0)),
inference(paramodulation,[status(thm)],[f1842,f67]) ).
fof(f1862,plain,
! [X0] : multiplication(addition(X0,one),star(X0)) = star(X0),
inference(paramodulation,[status(thm)],[f204,f1839]) ).
fof(f1884,plain,
! [X0] : multiplication(addition(one,X0),addition(star(X0),one)) = addition(addition(one,X0),star(X0)),
inference(paramodulation,[status(thm)],[f1839,f179]) ).
fof(f1906,plain,
! [X0] : multiplication(addition(one,X0),addition(one,star(X0))) = addition(addition(one,X0),star(X0)),
inference(forward_demodulation,[status(thm)],[f167,f1884]) ).
fof(f1907,plain,
! [X0] : multiplication(addition(one,X0),star(X0)) = addition(addition(one,X0),star(X0)),
inference(forward_demodulation,[status(thm)],[f1842,f1906]) ).
fof(f1908,plain,
! [X0] : star(X0) = addition(addition(one,X0),star(X0)),
inference(forward_demodulation,[status(thm)],[f1839,f1907]) ).
fof(f1909,plain,
! [X0] : star(X0) = addition(one,addition(X0,star(X0))),
inference(forward_demodulation,[status(thm)],[f20,f1908]) ).
fof(f1910,plain,
! [X0] : star(X0) = addition(X0,star(X0)),
inference(forward_demodulation,[status(thm)],[f1845,f1909]) ).
fof(f1934,plain,
! [X0] : addition(sK0_skl,addition(X0,star(sK1_skl))) = addition(sK1_skl,addition(X0,star(sK1_skl))),
inference(paramodulation,[status(thm)],[f1910,f265]) ).
fof(f1942,plain,
! [X0,X1] : addition(X0,addition(X1,star(X0))) = addition(X1,star(X0)),
inference(paramodulation,[status(thm)],[f1910,f82]) ).
fof(f1952,plain,
! [X0] : addition(sK0_skl,addition(X0,star(sK1_skl))) = addition(X0,star(sK1_skl)),
inference(backward_demodulation,[status(thm)],[f1942,f1934]) ).
fof(f1962,plain,
! [X0,X1] : multiplication(star(X0),X1) = addition(X1,multiplication(star(X0),X1)),
inference(paramodulation,[status(thm)],[f1842,f188]) ).
fof(f2025,plain,
! [X0] :
( multiplication(star(one),X0) = X0
| ~ leq(X0,X0) ),
inference(backward_demodulation,[status(thm)],[f1962,f270]) ).
fof(f2275,plain,
! [X0,X1,X2] : addition(X0,addition(multiplication(X1,X0),X2)) = addition(multiplication(addition(X1,one),X0),X2),
inference(paramodulation,[status(thm)],[f209,f20]) ).
fof(f2532,plain,
multiplication(star(one),star(zero)) = star(zero),
inference(resolution,[status(thm)],[f2025,f780]) ).
fof(f2546,plain,
! [X0] :
( addition(X0,X0) != X0
| multiplication(star(one),X0) = X0 ),
inference(resolution,[status(thm)],[f2025,f33]) ).
fof(f2549,plain,
! [X0,X1] :
( leq(multiplication(star(zero),X1),X0)
| ~ leq(addition(X0,X1),X0) ),
inference(backward_demodulation,[status(thm)],[f2560,f120]) ).
fof(f2560,plain,
star(one) = star(zero),
inference(forward_demodulation,[status(thm)],[f1288,f2532]) ).
fof(f2604,plain,
! [X0] :
( addition(X0,X0) != X0
| multiplication(star(zero),X0) = X0 ),
inference(forward_demodulation,[status(thm)],[f2560,f2546]) ).
fof(f2605,plain,
! [X0] :
( X0 != X0
| multiplication(star(zero),X0) = X0 ),
inference(forward_demodulation,[status(thm)],[f22,f2604]) ).
fof(f2621,plain,
! [X0] : multiplication(star(zero),X0) = X0,
inference(trivial_equality_resolution,[status(thm)],[f2605]) ).
fof(f2623,plain,
! [X0,X1] :
( leq(X1,X0)
| ~ leq(addition(X0,X1),X0) ),
inference(forward_demodulation,[status(thm)],[f2621,f2549]) ).
fof(f2877,plain,
~ leq(addition(star(sK1_skl),addition(one,multiplication(star(sK1_skl),sK0_skl))),star(sK1_skl)),
inference(resolution,[status(thm)],[f2623,f982]) ).
fof(f2882,plain,
~ leq(addition(one,addition(star(sK1_skl),multiplication(star(sK1_skl),sK0_skl))),star(sK1_skl)),
inference(forward_demodulation,[status(thm)],[f82,f2877]) ).
fof(f2883,plain,
~ leq(addition(multiplication(star(sK1_skl),sK0_skl),star(sK1_skl)),star(sK1_skl)),
inference(forward_demodulation,[status(thm)],[f1847,f2882]) ).
fof(f2884,plain,
~ leq(addition(star(sK1_skl),multiplication(star(sK1_skl),sK0_skl)),star(sK1_skl)),
inference(forward_demodulation,[status(thm)],[f19,f2883]) ).
fof(f2885,plain,
~ leq(multiplication(star(sK1_skl),addition(sK0_skl,one)),star(sK1_skl)),
inference(forward_demodulation,[status(thm)],[f179,f2884]) ).
fof(f3471,plain,
addition(star(sK1_skl),addition(multiplication(sK1_skl,star(sK1_skl)),addition(sK0_skl,one))) != star(sK1_skl),
inference(resolution,[status(thm)],[f2885,f79]) ).
fof(f3476,plain,
addition(multiplication(addition(sK1_skl,one),star(sK1_skl)),addition(sK0_skl,one)) != star(sK1_skl),
inference(forward_demodulation,[status(thm)],[f2275,f3471]) ).
fof(f3477,plain,
addition(sK0_skl,addition(multiplication(addition(sK1_skl,one),star(sK1_skl)),one)) != star(sK1_skl),
inference(forward_demodulation,[status(thm)],[f82,f3476]) ).
fof(f3478,plain,
addition(sK0_skl,addition(one,multiplication(addition(sK1_skl,one),star(sK1_skl)))) != star(sK1_skl),
inference(forward_demodulation,[status(thm)],[f552,f3477]) ).
fof(f3479,plain,
addition(sK0_skl,addition(one,star(sK1_skl))) != star(sK1_skl),
inference(forward_demodulation,[status(thm)],[f1862,f3478]) ).
fof(f3480,plain,
addition(one,star(sK1_skl)) != star(sK1_skl),
inference(forward_demodulation,[status(thm)],[f1952,f3479]) ).
fof(f3481,plain,
star(sK1_skl) != star(sK1_skl),
inference(forward_demodulation,[status(thm)],[f1842,f3480]) ).
fof(f3482,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f3481]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KLE041+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n020.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 20 22:41:03 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.39 % Drodi V4.1.1
% 3.02/0.89 % Refutation found
% 3.02/0.89 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.02/0.89 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.08/0.94 % Elapsed time: 0.544879 seconds
% 2.08/0.94 % CPU time: 3.764147 seconds
% 2.08/0.94 % Total memory used: 106.951 MB
% 2.08/0.94 % Net memory used: 105.306 MB
%------------------------------------------------------------------------------