%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : KLE147-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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 : Sun Sep 27 07:44:24 AM UTC 2026
% Result : Unsatisfiable 103.69s 14.41s
% Output : CNFRefutation 103.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 57
% Number of leaves : 22
% Syntax : Number of formulae : 340 ( 340 unt; 0 def)
% Number of atoms : 340 ( 339 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 7 con; 0-4 aty)
% Number of variables : 614 ( 19 sgn 42 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ifeq_axiom,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq3(VAR_0,VAR_0,VAR_1,VAR_2) = VAR_1,
file('theBenchmark.p',ifeq_axiom) ).
cnf(c_1,plain,
ifeq3(A,A,B,C) = B,
inference(clausify,[status(thm)],[ifeq_axiom]) ).
fof(ifeq_axiom_001,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq2(VAR_0,VAR_0,VAR_1,VAR_2) = VAR_1,
file('theBenchmark.p',ifeq_axiom_001) ).
cnf(c_2,plain,
ifeq2(A,A,B,C) = B,
inference(clausify,[status(thm)],[ifeq_axiom_001]) ).
fof(ifeq_axiom_002,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq(VAR_0,VAR_0,VAR_1,VAR_2) = VAR_1,
file('theBenchmark.p',ifeq_axiom_002) ).
cnf(c_3,plain,
ifeq(A,A,B,C) = B,
inference(clausify,[status(thm)],[ifeq_axiom_002]) ).
fof(additive_commutativity,axiom,
! [VAR_0,VAR_1] : addition(VAR_0,VAR_1) = addition(VAR_1,VAR_0),
file('theBenchmark.p',additive_commutativity) ).
cnf(c_4,plain,
addition(A,B) = addition(B,A),
inference(clausify,[status(thm)],[additive_commutativity]) ).
fof(additive_associativity,axiom,
! [VAR_0,VAR_1,VAR_2] : addition(VAR_0,addition(VAR_1,VAR_2)) = addition(addition(VAR_0,VAR_1),VAR_2),
file('theBenchmark.p',additive_associativity) ).
cnf(c_5,plain,
addition(A,addition(B,C)) = addition(addition(A,B),C),
inference(clausify,[status(thm)],[additive_associativity]) ).
cnf(c_6,plain,
addition(addition(A,B),C) = addition(A,addition(B,C)),
inference(copy,[status(thm)],[c_5]) ).
fof(additive_identity,axiom,
! [VAR_0] : addition(VAR_0,zero) = VAR_0,
file('theBenchmark.p',additive_identity) ).
cnf(c_7,plain,
addition(A,zero) = A,
inference(clausify,[status(thm)],[additive_identity]) ).
fof(idempotence,axiom,
! [VAR_0] : addition(VAR_0,VAR_0) = VAR_0,
file('theBenchmark.p',idempotence) ).
cnf(c_8,plain,
addition(A,A) = A,
inference(clausify,[status(thm)],[idempotence]) ).
fof(multiplicative_associativity,axiom,
! [VAR_0,VAR_1,VAR_2] : multiplication(VAR_0,multiplication(VAR_1,VAR_2)) = multiplication(multiplication(VAR_0,VAR_1),VAR_2),
file('theBenchmark.p',multiplicative_associativity) ).
cnf(c_9,plain,
multiplication(A,multiplication(B,C)) = multiplication(multiplication(A,B),C),
inference(clausify,[status(thm)],[multiplicative_associativity]) ).
cnf(c_10,plain,
multiplication(multiplication(A,B),C) = multiplication(A,multiplication(B,C)),
inference(copy,[status(thm)],[c_9]) ).
fof(multiplicative_right_identity,axiom,
! [VAR_0] : multiplication(VAR_0,one) = VAR_0,
file('theBenchmark.p',multiplicative_right_identity) ).
cnf(c_11,plain,
multiplication(A,one) = A,
inference(clausify,[status(thm)],[multiplicative_right_identity]) ).
fof(multiplicative_left_identity,axiom,
! [VAR_0] : multiplication(one,VAR_0) = VAR_0,
file('theBenchmark.p',multiplicative_left_identity) ).
cnf(c_12,plain,
multiplication(one,A) = A,
inference(clausify,[status(thm)],[multiplicative_left_identity]) ).
fof(distributivity1,axiom,
! [VAR_0,VAR_1,VAR_2] : multiplication(VAR_0,addition(VAR_1,VAR_2)) = addition(multiplication(VAR_0,VAR_1),multiplication(VAR_0,VAR_2)),
file('theBenchmark.p',distributivity1) ).
cnf(c_13,plain,
multiplication(A,addition(B,C)) = addition(multiplication(A,B),multiplication(A,C)),
inference(clausify,[status(thm)],[distributivity1]) ).
cnf(c_14,plain,
addition(multiplication(A,B),multiplication(A,C)) = multiplication(A,addition(B,C)),
inference(copy,[status(thm)],[c_13]) ).
fof(distributivity2,axiom,
! [VAR_0,VAR_1,VAR_2] : multiplication(addition(VAR_0,VAR_1),VAR_2) = addition(multiplication(VAR_0,VAR_2),multiplication(VAR_1,VAR_2)),
file('theBenchmark.p',distributivity2) ).
cnf(c_15,plain,
multiplication(addition(A,B),C) = addition(multiplication(A,C),multiplication(B,C)),
inference(clausify,[status(thm)],[distributivity2]) ).
cnf(c_16,plain,
addition(multiplication(A,B),multiplication(C,B)) = multiplication(addition(A,C),B),
inference(copy,[status(thm)],[c_15]) ).
fof(left_annihilation,axiom,
! [VAR_0] : multiplication(zero,VAR_0) = zero,
file('theBenchmark.p',left_annihilation) ).
cnf(c_17,plain,
multiplication(zero,A) = zero,
inference(clausify,[status(thm)],[left_annihilation]) ).
fof(star_unfold1,axiom,
! [VAR_0] : addition(one,multiplication(VAR_0,star(VAR_0))) = star(VAR_0),
file('theBenchmark.p',star_unfold1) ).
cnf(c_18,plain,
addition(one,multiplication(A,star(A))) = star(A),
inference(clausify,[status(thm)],[star_unfold1]) ).
fof(star_unfold2,axiom,
! [VAR_0] : addition(one,multiplication(star(VAR_0),VAR_0)) = star(VAR_0),
file('theBenchmark.p',star_unfold2) ).
cnf(c_19,plain,
addition(one,multiplication(star(A),A)) = star(A),
inference(clausify,[status(thm)],[star_unfold2]) ).
fof(star_induction1,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq(leq(addition(multiplication(VAR_0,VAR_1),VAR_2),VAR_1),true,leq(multiplication(star(VAR_0),VAR_2),VAR_1),true) = true,
file('theBenchmark.p',star_induction1) ).
cnf(c_20,plain,
ifeq(leq(addition(multiplication(A,B),C),B),true,leq(multiplication(star(A),C),B),true) = true,
inference(clausify,[status(thm)],[star_induction1]) ).
fof(star_induction2,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq(leq(addition(multiplication(VAR_0,VAR_1),VAR_2),VAR_0),true,leq(multiplication(VAR_2,star(VAR_1)),VAR_0),true) = true,
file('theBenchmark.p',star_induction2) ).
cnf(c_21,plain,
ifeq(leq(addition(multiplication(A,B),C),A),true,leq(multiplication(C,star(B)),A),true) = true,
inference(clausify,[status(thm)],[star_induction2]) ).
fof(infty_unfold1,axiom,
! [VAR_0] : strong_iteration(VAR_0) = addition(multiplication(VAR_0,strong_iteration(VAR_0)),one),
file('theBenchmark.p',infty_unfold1) ).
cnf(c_22,plain,
strong_iteration(A) = addition(multiplication(A,strong_iteration(A)),one),
inference(clausify,[status(thm)],[infty_unfold1]) ).
cnf(c_26028,plain,
strong_iteration(A) = addition(one,multiplication(A,strong_iteration(A))),
inference(paramod,[status(thm)],[c_4,c_22]) ).
cnf(c_23,plain,
addition(one,multiplication(A,strong_iteration(A))) = strong_iteration(A),
inference(copy,[status(thm)],[c_26028]) ).
fof(isolation,axiom,
! [VAR_0] : strong_iteration(VAR_0) = addition(star(VAR_0),multiplication(strong_iteration(VAR_0),zero)),
file('theBenchmark.p',isolation) ).
cnf(c_25,plain,
strong_iteration(A) = addition(star(A),multiplication(strong_iteration(A),zero)),
inference(clausify,[status(thm)],[isolation]) ).
cnf(c_26,plain,
addition(star(A),multiplication(strong_iteration(A),zero)) = strong_iteration(A),
inference(copy,[status(thm)],[c_25]) ).
fof(order_1,axiom,
! [VAR_0,VAR_1] : ifeq2(leq(VAR_0,VAR_1),true,addition(VAR_0,VAR_1),VAR_1) = VAR_1,
file('theBenchmark.p',order_1) ).
cnf(c_27,plain,
ifeq2(leq(A,B),true,addition(A,B),B) = B,
inference(clausify,[status(thm)],[order_1]) ).
fof(order,axiom,
! [VAR_0,VAR_1] : ifeq3(addition(VAR_0,VAR_1),VAR_1,leq(VAR_0,VAR_1),true) = true,
file('theBenchmark.p',order) ).
cnf(c_28,plain,
ifeq3(addition(A,B),B,leq(A,B),true) = true,
inference(clausify,[status(thm)],[order]) ).
fof(goals,axiom,
tuple(leq(multiplication(star(sK1_goals_X1),strong_iteration(multiplication(star(sK2_goals_X0),sK1_goals_X1))),strong_iteration(multiplication(star(sK2_goals_X0),sK1_goals_X1))),leq(strong_iteration(multiplication(star(sK4_goals_X0),sK3_goals_X1)),multiplication(star(sK3_goals_X1),strong_iteration(multiplication(star(sK4_goals_X0),sK3_goals_X1))))) != tuple(true,true),
file('theBenchmark.p',goals) ).
cnf(c_29,plain,
tuple(leq(multiplication(star(sK1_goals_X1),strong_iteration(multiplication(star(sK2_goals_X0),sK1_goals_X1))),strong_iteration(multiplication(star(sK2_goals_X0),sK1_goals_X1))),leq(strong_iteration(multiplication(star(sK4_goals_X0),sK3_goals_X1)),multiplication(star(sK3_goals_X1),strong_iteration(multiplication(star(sK4_goals_X0),sK3_goals_X1))))) != tuple(true,true),
inference(clausify,[status(thm)],[goals]) ).
cnf(c_26029,plain,
addition(addition(A,B),C) = addition(B,addition(A,C)),
inference(paramod,[status(thm)],[c_4,c_6]) ).
cnf(c_31,plain,
addition(A,addition(B,C)) = addition(B,addition(A,C)),
inference(paramod,[status(thm)],[c_6,c_26029]) ).
cnf(c_26030,plain,
A = addition(zero,A),
inference(paramod,[status(thm)],[c_7,c_4]) ).
cnf(c_32,plain,
addition(zero,A) = A,
inference(copy,[status(thm)],[c_26030]) ).
cnf(c_26031,plain,
addition(A,B) = addition(A,addition(A,B)),
inference(paramod,[status(thm)],[c_8,c_6]) ).
cnf(c_33,plain,
addition(A,addition(A,B)) = addition(A,B),
inference(copy,[status(thm)],[c_26031]) ).
cnf(c_26032,plain,
addition(addition(A,B),B) = addition(A,B),
inference(paramod,[status(thm)],[c_8,c_6]) ).
cnf(c_35,plain,
addition(A,addition(B,A)) = addition(B,A),
inference(paramod,[status(thm)],[c_4,c_26032]) ).
cnf(c_36,plain,
addition(multiplication(A,addition(B,C)),D) = addition(multiplication(A,B),addition(multiplication(A,C),D)),
inference(paramod,[status(thm)],[c_14,c_6]) ).
cnf(c_26033,plain,
addition(A,multiplication(A,B)) = multiplication(A,addition(one,B)),
inference(paramod,[status(thm)],[c_11,c_14]) ).
cnf(c_37,plain,
multiplication(A,addition(one,B)) = addition(A,multiplication(A,B)),
inference(copy,[status(thm)],[c_26033]) ).
cnf(c_39,plain,
addition(multiplication(addition(A,B),C),D) = addition(multiplication(A,C),addition(multiplication(B,C),D)),
inference(paramod,[status(thm)],[c_16,c_6]) ).
cnf(c_41,plain,
addition(multiplication(A,B),multiplication(C,multiplication(D,B))) = multiplication(addition(A,multiplication(C,D)),B),
inference(paramod,[status(thm)],[c_10,c_16]) ).
cnf(c_26034,plain,
addition(A,multiplication(B,A)) = multiplication(addition(one,B),A),
inference(paramod,[status(thm)],[c_12,c_16]) ).
cnf(c_42,plain,
multiplication(addition(one,A),B) = addition(B,multiplication(A,B)),
inference(copy,[status(thm)],[c_26034]) ).
cnf(c_26035,plain,
addition(star(A),B) = addition(one,addition(multiplication(A,star(A)),B)),
inference(paramod,[status(thm)],[c_18,c_6]) ).
cnf(c_44,plain,
addition(one,addition(multiplication(A,star(A)),B)) = addition(star(A),B),
inference(copy,[status(thm)],[c_26035]) ).
cnf(c_45,plain,
addition(one,multiplication(A,multiplication(B,star(multiplication(A,B))))) = star(multiplication(A,B)),
inference(paramod,[status(thm)],[c_10,c_18]) ).
cnf(c_26036,plain,
addition(multiplication(A,one),multiplication(A,multiplication(B,star(B)))) = multiplication(A,star(B)),
inference(paramod,[status(thm)],[c_18,c_14]) ).
cnf(c_47,plain,
addition(A,multiplication(A,multiplication(B,star(B)))) = multiplication(A,star(B)),
inference(paramod,[status(thm)],[c_11,c_26036]) ).
cnf(c_26037,plain,
addition(multiplication(one,A),multiplication(multiplication(B,star(B)),A)) = multiplication(star(B),A),
inference(paramod,[status(thm)],[c_18,c_16]) ).
cnf(c_26038,plain,
addition(A,multiplication(multiplication(B,star(B)),A)) = multiplication(star(B),A),
inference(paramod,[status(thm)],[c_12,c_26037]) ).
cnf(c_48,plain,
addition(A,multiplication(B,multiplication(star(B),A))) = multiplication(star(B),A),
inference(paramod,[status(thm)],[c_10,c_26038]) ).
cnf(c_26039,plain,
ifeq(leq(addition(multiplication(A,B),one),B),true,leq(star(A),B),true) = true,
inference(paramod,[status(thm)],[c_11,c_20]) ).
cnf(c_58,plain,
ifeq(leq(addition(one,multiplication(A,B)),B),true,leq(star(A),B),true) = true,
inference(paramod,[status(thm)],[c_4,c_26039]) ).
cnf(c_61,plain,
ifeq(leq(multiplication(addition(A,B),C),C),true,leq(multiplication(star(A),multiplication(B,C)),C),true) = true,
inference(paramod,[status(thm)],[c_16,c_20]) ).
cnf(c_26040,plain,
ifeq(leq(addition(multiplication(A,B),one),A),true,leq(star(B),A),true) = true,
inference(paramod,[status(thm)],[c_12,c_21]) ).
cnf(c_70,plain,
ifeq(leq(addition(one,multiplication(A,B)),A),true,leq(star(B),A),true) = true,
inference(paramod,[status(thm)],[c_4,c_26040]) ).
cnf(c_91,plain,
ifeq2(leq(A,B),true,addition(B,A),B) = B,
inference(paramod,[status(thm)],[c_4,c_27]) ).
cnf(c_26041,plain,
ifeq3(A,A,leq(A,A),true) = true,
inference(paramod,[status(thm)],[c_8,c_28]) ).
cnf(c_104,plain,
leq(A,A) = true,
inference(paramod,[status(thm)],[c_1,c_26041]) ).
cnf(c_26042,plain,
addition(A,multiplication(B,addition(C,D))) = addition(multiplication(B,C),addition(A,multiplication(B,D))),
inference(paramod,[status(thm)],[c_14,c_31]) ).
cnf(c_111,plain,
addition(multiplication(A,B),addition(C,multiplication(A,D))) = addition(C,multiplication(A,addition(B,D))),
inference(copy,[status(thm)],[c_26042]) ).
cnf(c_26043,plain,
addition(A,star(B)) = addition(one,addition(A,multiplication(B,star(B)))),
inference(paramod,[status(thm)],[c_18,c_31]) ).
cnf(c_113,plain,
addition(one,addition(A,multiplication(B,star(B)))) = addition(A,star(B)),
inference(copy,[status(thm)],[c_26043]) ).
cnf(c_26044,plain,
addition(A,strong_iteration(B)) = addition(one,addition(A,multiplication(B,strong_iteration(B)))),
inference(paramod,[status(thm)],[c_23,c_31]) ).
cnf(c_117,plain,
addition(one,addition(A,multiplication(B,strong_iteration(B)))) = addition(A,strong_iteration(B)),
inference(copy,[status(thm)],[c_26044]) ).
cnf(c_120,plain,
ifeq2(leq(A,addition(B,C)),true,addition(B,addition(A,C)),addition(B,C)) = addition(B,C),
inference(paramod,[status(thm)],[c_31,c_27]) ).
cnf(c_121,plain,
ifeq3(addition(A,addition(B,C)),addition(A,C),leq(B,addition(A,C)),true) = true,
inference(paramod,[status(thm)],[c_31,c_28]) ).
cnf(c_26045,plain,
addition(addition(A,B),addition(B,C)) = addition(A,addition(B,C)),
inference(paramod,[status(thm)],[c_33,c_6]) ).
cnf(c_26046,plain,
addition(B,addition(addition(A,B),C)) = addition(A,addition(B,C)),
inference(paramod,[status(thm)],[c_31,c_26045]) ).
cnf(c_133,plain,
addition(A,addition(B,addition(A,C))) = addition(B,addition(A,C)),
inference(paramod,[status(thm)],[c_6,c_26046]) ).
cnf(c_26047,plain,
addition(one,star(A)) = addition(one,multiplication(A,star(A))),
inference(paramod,[status(thm)],[c_18,c_33]) ).
cnf(c_134,plain,
addition(one,star(A)) = star(A),
inference(paramod,[status(thm)],[c_18,c_26047]) ).
cnf(c_26048,plain,
addition(one,strong_iteration(A)) = addition(one,multiplication(A,strong_iteration(A))),
inference(paramod,[status(thm)],[c_23,c_33]) ).
cnf(c_137,plain,
addition(one,strong_iteration(A)) = strong_iteration(A),
inference(paramod,[status(thm)],[c_23,c_26048]) ).
cnf(c_26049,plain,
ifeq3(addition(A,B),addition(A,B),leq(A,addition(A,B)),true) = true,
inference(paramod,[status(thm)],[c_33,c_28]) ).
cnf(c_141,plain,
leq(A,addition(A,B)) = true,
inference(paramod,[status(thm)],[c_1,c_26049]) ).
cnf(c_26050,plain,
addition(star(A),B) = addition(one,addition(star(A),B)),
inference(paramod,[status(thm)],[c_134,c_6]) ).
cnf(c_143,plain,
addition(one,addition(star(A),B)) = addition(star(A),B),
inference(copy,[status(thm)],[c_26050]) ).
cnf(c_26051,plain,
addition(multiplication(A,one),multiplication(A,star(B))) = multiplication(A,star(B)),
inference(paramod,[status(thm)],[c_134,c_14]) ).
cnf(c_144,plain,
addition(A,multiplication(A,star(B))) = multiplication(A,star(B)),
inference(paramod,[status(thm)],[c_11,c_26051]) ).
cnf(c_26052,plain,
addition(multiplication(one,A),multiplication(star(B),A)) = multiplication(star(B),A),
inference(paramod,[status(thm)],[c_134,c_16]) ).
cnf(c_145,plain,
addition(A,multiplication(star(B),A)) = multiplication(star(B),A),
inference(paramod,[status(thm)],[c_12,c_26052]) ).
cnf(c_26053,plain,
addition(A,star(B)) = addition(one,addition(A,star(B))),
inference(paramod,[status(thm)],[c_134,c_31]) ).
cnf(c_148,plain,
addition(one,addition(A,star(B))) = addition(A,star(B)),
inference(copy,[status(thm)],[c_26053]) ).
cnf(c_26054,plain,
addition(A,strong_iteration(B)) = addition(one,addition(A,strong_iteration(B))),
inference(paramod,[status(thm)],[c_137,c_31]) ).
cnf(c_154,plain,
addition(one,addition(A,strong_iteration(B))) = addition(A,strong_iteration(B)),
inference(copy,[status(thm)],[c_26054]) ).
cnf(c_156,plain,
leq(addition(A,B),addition(A,addition(B,C))) = true,
inference(paramod,[status(thm)],[c_6,c_141]) ).
cnf(c_26055,plain,
addition(multiplication(A,star(A)),star(A)) = addition(one,multiplication(A,star(A))),
inference(paramod,[status(thm)],[c_18,c_35]) ).
cnf(c_26056,plain,
addition(star(A),multiplication(A,star(A))) = addition(one,multiplication(A,star(A))),
inference(paramod,[status(thm)],[c_4,c_26055]) ).
cnf(c_26057,plain,
multiplication(addition(one,A),star(A)) = addition(one,multiplication(A,star(A))),
inference(paramod,[status(thm)],[c_42,c_26056]) ).
cnf(c_165,plain,
multiplication(addition(one,A),star(A)) = star(A),
inference(paramod,[status(thm)],[c_18,c_26057]) ).
cnf(c_26058,plain,
addition(multiplication(star(A),A),star(A)) = addition(one,multiplication(star(A),A)),
inference(paramod,[status(thm)],[c_19,c_35]) ).
cnf(c_26059,plain,
addition(star(A),multiplication(star(A),A)) = addition(one,multiplication(star(A),A)),
inference(paramod,[status(thm)],[c_4,c_26058]) ).
cnf(c_26060,plain,
multiplication(star(A),addition(one,A)) = addition(one,multiplication(star(A),A)),
inference(paramod,[status(thm)],[c_37,c_26059]) ).
cnf(c_166,plain,
multiplication(star(A),addition(one,A)) = star(A),
inference(paramod,[status(thm)],[c_19,c_26060]) ).
cnf(c_26061,plain,
addition(multiplication(A,strong_iteration(A)),strong_iteration(A)) = addition(one,multiplication(A,strong_iteration(A))),
inference(paramod,[status(thm)],[c_23,c_35]) ).
cnf(c_26062,plain,
addition(strong_iteration(A),multiplication(A,strong_iteration(A))) = addition(one,multiplication(A,strong_iteration(A))),
inference(paramod,[status(thm)],[c_4,c_26061]) ).
cnf(c_26063,plain,
multiplication(addition(one,A),strong_iteration(A)) = addition(one,multiplication(A,strong_iteration(A))),
inference(paramod,[status(thm)],[c_42,c_26062]) ).
cnf(c_169,plain,
multiplication(addition(one,A),strong_iteration(A)) = strong_iteration(A),
inference(paramod,[status(thm)],[c_23,c_26063]) ).
cnf(c_184,plain,
multiplication(addition(A,one),star(A)) = star(A),
inference(paramod,[status(thm)],[c_4,c_165]) ).
cnf(c_26064,plain,
addition(star(A),multiplication(B,star(A))) = multiplication(addition(addition(one,A),B),star(A)),
inference(paramod,[status(thm)],[c_165,c_16]) ).
cnf(c_26065,plain,
multiplication(addition(one,B),star(A)) = multiplication(addition(addition(one,A),B),star(A)),
inference(paramod,[status(thm)],[c_42,c_26064]) ).
cnf(c_26066,plain,
multiplication(addition(one,B),star(A)) = multiplication(addition(one,addition(A,B)),star(A)),
inference(paramod,[status(thm)],[c_6,c_26065]) ).
cnf(c_188,plain,
multiplication(addition(one,addition(A,B)),star(A)) = multiplication(addition(one,B),star(A)),
inference(copy,[status(thm)],[c_26066]) ).
cnf(c_198,plain,
multiplication(addition(one,A),star(addition(one,A))) = star(addition(one,A)),
inference(paramod,[status(thm)],[c_33,c_165]) ).
cnf(c_206,plain,
addition(multiplication(A,multiplication(addition(B,C),D)),E) = addition(multiplication(A,multiplication(B,D)),addition(multiplication(A,multiplication(C,D)),E)),
inference(paramod,[status(thm)],[c_16,c_36]) ).
cnf(c_26067,plain,
addition(multiplication(A,strong_iteration(B)),C) = addition(multiplication(A,star(B)),addition(multiplication(A,multiplication(strong_iteration(B),zero)),C)),
inference(paramod,[status(thm)],[c_26,c_36]) ).
cnf(c_213,plain,
addition(multiplication(A,star(B)),addition(multiplication(A,multiplication(strong_iteration(B),zero)),C)) = addition(multiplication(A,strong_iteration(B)),C),
inference(copy,[status(thm)],[c_26067]) ).
cnf(c_26068,plain,
addition(multiplication(star(A),B),star(A)) = multiplication(star(A),addition(B,addition(one,A))),
inference(paramod,[status(thm)],[c_166,c_14]) ).
cnf(c_26069,plain,
addition(star(A),multiplication(star(A),B)) = multiplication(star(A),addition(B,addition(one,A))),
inference(paramod,[status(thm)],[c_4,c_26068]) ).
cnf(c_225,plain,
multiplication(star(A),addition(one,B)) = multiplication(star(A),addition(B,addition(one,A))),
inference(paramod,[status(thm)],[c_37,c_26069]) ).
cnf(c_241,plain,
multiplication(addition(A,one),strong_iteration(A)) = strong_iteration(A),
inference(paramod,[status(thm)],[c_4,c_169]) ).
cnf(c_26070,plain,
multiplication(addition(one,A),addition(one,star(A))) = addition(addition(one,A),star(A)),
inference(paramod,[status(thm)],[c_165,c_37]) ).
cnf(c_26071,plain,
multiplication(addition(one,A),star(A)) = addition(addition(one,A),star(A)),
inference(paramod,[status(thm)],[c_134,c_26070]) ).
cnf(c_26072,plain,
star(A) = addition(addition(one,A),star(A)),
inference(paramod,[status(thm)],[c_165,c_26071]) ).
cnf(c_26073,plain,
star(A) = addition(one,addition(A,star(A))),
inference(paramod,[status(thm)],[c_6,c_26072]) ).
cnf(c_26074,plain,
star(A) = addition(A,star(A)),
inference(paramod,[status(thm)],[c_148,c_26073]) ).
cnf(c_306,plain,
addition(A,star(A)) = star(A),
inference(copy,[status(thm)],[c_26074]) ).
cnf(c_26075,plain,
multiplication(addition(one,A),addition(one,strong_iteration(A))) = addition(addition(one,A),strong_iteration(A)),
inference(paramod,[status(thm)],[c_169,c_37]) ).
cnf(c_26076,plain,
multiplication(addition(one,A),strong_iteration(A)) = addition(addition(one,A),strong_iteration(A)),
inference(paramod,[status(thm)],[c_137,c_26075]) ).
cnf(c_26077,plain,
strong_iteration(A) = addition(addition(one,A),strong_iteration(A)),
inference(paramod,[status(thm)],[c_169,c_26076]) ).
cnf(c_26078,plain,
strong_iteration(A) = addition(one,addition(A,strong_iteration(A))),
inference(paramod,[status(thm)],[c_6,c_26077]) ).
cnf(c_26079,plain,
strong_iteration(A) = addition(A,strong_iteration(A)),
inference(paramod,[status(thm)],[c_154,c_26078]) ).
cnf(c_309,plain,
addition(A,strong_iteration(A)) = strong_iteration(A),
inference(copy,[status(thm)],[c_26079]) ).
cnf(c_415,plain,
multiplication(addition(one,A),zero) = multiplication(A,zero),
inference(paramod,[status(thm)],[c_42,c_32]) ).
cnf(c_26080,plain,
multiplication(strong_iteration(A),zero) = multiplication(multiplication(A,strong_iteration(A)),zero),
inference(paramod,[status(thm)],[c_23,c_415]) ).
cnf(c_26081,plain,
multiplication(strong_iteration(A),zero) = multiplication(A,multiplication(strong_iteration(A),zero)),
inference(paramod,[status(thm)],[c_10,c_26080]) ).
cnf(c_434,plain,
multiplication(A,multiplication(strong_iteration(A),zero)) = multiplication(strong_iteration(A),zero),
inference(copy,[status(thm)],[c_26081]) ).
cnf(c_557,plain,
addition(multiplication(A,B),multiplication(C,zero)) = multiplication(addition(A,multiplication(C,zero)),B),
inference(paramod,[status(thm)],[c_17,c_41]) ).
cnf(c_26082,plain,
addition(star(A),multiplication(B,multiplication(C,star(A)))) = multiplication(addition(addition(one,A),multiplication(B,C)),star(A)),
inference(paramod,[status(thm)],[c_165,c_41]) ).
cnf(c_26083,plain,
addition(star(A),multiplication(B,multiplication(C,star(A)))) = multiplication(addition(one,addition(A,multiplication(B,C))),star(A)),
inference(paramod,[status(thm)],[c_6,c_26082]) ).
cnf(c_565,plain,
addition(star(A),multiplication(B,multiplication(C,star(A)))) = multiplication(addition(one,multiplication(B,C)),star(A)),
inference(paramod,[status(thm)],[c_188,c_26083]) ).
cnf(c_26084,plain,
addition(one,multiplication(addition(A,B),star(A))) = addition(star(A),multiplication(B,star(A))),
inference(paramod,[status(thm)],[c_16,c_44]) ).
cnf(c_621,plain,
addition(one,multiplication(addition(A,B),star(A))) = multiplication(addition(one,B),star(A)),
inference(paramod,[status(thm)],[c_42,c_26084]) ).
cnf(c_26085,plain,
addition(one,addition(multiplication(A,star(A)),multiplication(strong_iteration(A),zero))) = strong_iteration(A),
inference(paramod,[status(thm)],[c_26,c_44]) ).
cnf(c_26086,plain,
addition(one,multiplication(addition(A,multiplication(strong_iteration(A),zero)),star(A))) = strong_iteration(A),
inference(paramod,[status(thm)],[c_557,c_26085]) ).
cnf(c_622,plain,
multiplication(addition(one,multiplication(strong_iteration(A),zero)),star(A)) = strong_iteration(A),
inference(paramod,[status(thm)],[c_621,c_26086]) ).
cnf(c_626,plain,
leq(one,addition(star(A),B)) = true,
inference(paramod,[status(thm)],[c_44,c_141]) ).
cnf(c_26087,plain,
addition(one,multiplication(addition(one,A),multiplication(B,star(B)))) = addition(star(B),multiplication(A,multiplication(B,star(B)))),
inference(paramod,[status(thm)],[c_42,c_44]) ).
cnf(c_639,plain,
addition(one,multiplication(addition(one,A),multiplication(B,star(B)))) = multiplication(addition(one,multiplication(A,B)),star(B)),
inference(paramod,[status(thm)],[c_565,c_26087]) ).
cnf(c_26088,plain,
addition(one,multiplication(A,zero)) = star(multiplication(A,zero)),
inference(paramod,[status(thm)],[c_17,c_45]) ).
cnf(c_686,plain,
star(multiplication(A,zero)) = addition(one,multiplication(A,zero)),
inference(copy,[status(thm)],[c_26088]) ).
cnf(c_756,plain,
leq(one,multiplication(star(A),star(B))) = true,
inference(paramod,[status(thm)],[c_47,c_626]) ).
cnf(c_787,plain,
leq(A,multiplication(star(B),A)) = true,
inference(paramod,[status(thm)],[c_48,c_141]) ).
cnf(c_26089,plain,
multiplication(A,addition(one,multiplication(star(A),A))) = multiplication(star(A),A),
inference(paramod,[status(thm)],[c_48,c_37]) ).
cnf(c_26090,plain,
multiplication(A,star(A)) = multiplication(star(A),A),
inference(paramod,[status(thm)],[c_19,c_26089]) ).
cnf(c_790,plain,
multiplication(star(A),A) = multiplication(A,star(A)),
inference(copy,[status(thm)],[c_26090]) ).
cnf(c_26091,plain,
addition(A,multiplication(multiplication(B,zero),multiplication(addition(one,multiplication(B,zero)),A))) = multiplication(star(multiplication(B,zero)),A),
inference(paramod,[status(thm)],[c_686,c_48]) ).
cnf(c_26092,plain,
addition(A,multiplication(B,multiplication(zero,multiplication(addition(one,multiplication(B,zero)),A)))) = multiplication(star(multiplication(B,zero)),A),
inference(paramod,[status(thm)],[c_10,c_26091]) ).
cnf(c_26093,plain,
addition(A,multiplication(B,zero)) = multiplication(star(multiplication(B,zero)),A),
inference(paramod,[status(thm)],[c_17,c_26092]) ).
cnf(c_26094,plain,
addition(A,multiplication(B,zero)) = multiplication(addition(one,multiplication(B,zero)),A),
inference(paramod,[status(thm)],[c_686,c_26093]) ).
cnf(c_796,plain,
multiplication(addition(one,multiplication(A,zero)),B) = addition(B,multiplication(A,zero)),
inference(copy,[status(thm)],[c_26094]) ).
cnf(c_803,plain,
tuple(leq(multiplication(star(sK1_goals_X1),strong_iteration(multiplication(star(sK2_goals_X0),sK1_goals_X1))),strong_iteration(multiplication(star(sK2_goals_X0),sK1_goals_X1))),true) != tuple(true,true),
inference(paramod,[status(thm)],[c_787,c_29]) ).
cnf(c_809,plain,
addition(multiplication(A,star(A)),multiplication(star(A),B)) = multiplication(star(A),addition(A,B)),
inference(paramod,[status(thm)],[c_790,c_14]) ).
cnf(c_26095,plain,
ifeq2(true,true,addition(one,multiplication(star(A),star(B))),multiplication(star(A),star(B))) = multiplication(star(A),star(B)),
inference(paramod,[status(thm)],[c_756,c_27]) ).
cnf(c_905,plain,
addition(one,multiplication(star(A),star(B))) = multiplication(star(A),star(B)),
inference(paramod,[status(thm)],[c_2,c_26095]) ).
cnf(c_26096,plain,
ifeq(leq(addition(one,star(A)),star(A)),true,leq(star(addition(one,A)),star(A)),true) = true,
inference(paramod,[status(thm)],[c_165,c_58]) ).
cnf(c_26097,plain,
ifeq(leq(star(A),star(A)),true,leq(star(addition(one,A)),star(A)),true) = true,
inference(paramod,[status(thm)],[c_134,c_26096]) ).
cnf(c_26098,plain,
ifeq(true,true,leq(star(addition(one,A)),star(A)),true) = true,
inference(paramod,[status(thm)],[c_104,c_26097]) ).
cnf(c_1135,plain,
leq(star(addition(one,A)),star(A)) = true,
inference(paramod,[status(thm)],[c_3,c_26098]) ).
cnf(c_26099,plain,
ifeq2(true,true,addition(star(addition(one,A)),star(A)),star(A)) = star(A),
inference(paramod,[status(thm)],[c_1135,c_27]) ).
cnf(c_26100,plain,
ifeq2(true,true,addition(star(A),star(addition(one,A))),star(A)) = star(A),
inference(paramod,[status(thm)],[c_4,c_26099]) ).
cnf(c_1166,plain,
addition(star(A),star(addition(one,A))) = star(A),
inference(paramod,[status(thm)],[c_2,c_26100]) ).
cnf(c_26101,plain,
ifeq(leq(star(A),star(A)),true,leq(multiplication(star(A),multiplication(one,star(A))),star(A)),true) = true,
inference(paramod,[status(thm)],[c_184,c_61]) ).
cnf(c_26102,plain,
ifeq(true,true,leq(multiplication(star(A),multiplication(one,star(A))),star(A)),true) = true,
inference(paramod,[status(thm)],[c_104,c_26101]) ).
cnf(c_26103,plain,
ifeq(true,true,leq(multiplication(star(A),star(A)),star(A)),true) = true,
inference(paramod,[status(thm)],[c_12,c_26102]) ).
cnf(c_1211,plain,
leq(multiplication(star(A),star(A)),star(A)) = true,
inference(paramod,[status(thm)],[c_3,c_26103]) ).
cnf(c_26104,plain,
ifeq(leq(strong_iteration(A),strong_iteration(A)),true,leq(multiplication(star(A),multiplication(one,strong_iteration(A))),strong_iteration(A)),true) = true,
inference(paramod,[status(thm)],[c_241,c_61]) ).
cnf(c_26105,plain,
ifeq(true,true,leq(multiplication(star(A),multiplication(one,strong_iteration(A))),strong_iteration(A)),true) = true,
inference(paramod,[status(thm)],[c_104,c_26104]) ).
cnf(c_26106,plain,
ifeq(true,true,leq(multiplication(star(A),strong_iteration(A)),strong_iteration(A)),true) = true,
inference(paramod,[status(thm)],[c_12,c_26105]) ).
cnf(c_1214,plain,
leq(multiplication(star(A),strong_iteration(A)),strong_iteration(A)) = true,
inference(paramod,[status(thm)],[c_3,c_26106]) ).
cnf(c_1312,plain,
ifeq2(leq(star(A),star(addition(one,A))),true,star(A),star(addition(one,A))) = star(addition(one,A)),
inference(paramod,[status(thm)],[c_1166,c_27]) ).
cnf(c_26107,plain,
ifeq2(true,true,addition(multiplication(star(A),star(A)),star(A)),star(A)) = star(A),
inference(paramod,[status(thm)],[c_1211,c_27]) ).
cnf(c_26108,plain,
ifeq2(true,true,addition(star(A),multiplication(star(A),star(A))),star(A)) = star(A),
inference(paramod,[status(thm)],[c_4,c_26107]) ).
cnf(c_26109,plain,
ifeq2(true,true,multiplication(star(A),addition(one,star(A))),star(A)) = star(A),
inference(paramod,[status(thm)],[c_37,c_26108]) ).
cnf(c_26110,plain,
ifeq2(true,true,multiplication(star(A),star(A)),star(A)) = star(A),
inference(paramod,[status(thm)],[c_134,c_26109]) ).
cnf(c_1337,plain,
multiplication(star(A),star(A)) = star(A),
inference(paramod,[status(thm)],[c_2,c_26110]) ).
cnf(c_26111,plain,
ifeq(leq(addition(one,star(A)),star(A)),true,leq(star(star(A)),star(A)),true) = true,
inference(paramod,[status(thm)],[c_1337,c_58]) ).
cnf(c_26112,plain,
ifeq(leq(star(A),star(A)),true,leq(star(star(A)),star(A)),true) = true,
inference(paramod,[status(thm)],[c_134,c_26111]) ).
cnf(c_26113,plain,
ifeq(true,true,leq(star(star(A)),star(A)),true) = true,
inference(paramod,[status(thm)],[c_104,c_26112]) ).
cnf(c_1357,plain,
leq(star(star(A)),star(A)) = true,
inference(paramod,[status(thm)],[c_3,c_26113]) ).
cnf(c_26114,plain,
ifeq2(true,true,addition(multiplication(star(A),strong_iteration(A)),strong_iteration(A)),strong_iteration(A)) = strong_iteration(A),
inference(paramod,[status(thm)],[c_1214,c_27]) ).
cnf(c_26115,plain,
ifeq2(true,true,addition(strong_iteration(A),multiplication(star(A),strong_iteration(A))),strong_iteration(A)) = strong_iteration(A),
inference(paramod,[status(thm)],[c_4,c_26114]) ).
cnf(c_26116,plain,
ifeq2(true,true,multiplication(star(A),strong_iteration(A)),strong_iteration(A)) = strong_iteration(A),
inference(paramod,[status(thm)],[c_145,c_26115]) ).
cnf(c_1361,plain,
multiplication(star(A),strong_iteration(A)) = strong_iteration(A),
inference(paramod,[status(thm)],[c_2,c_26116]) ).
cnf(c_26117,plain,
addition(strong_iteration(A),multiplication(B,strong_iteration(A))) = multiplication(addition(star(A),B),strong_iteration(A)),
inference(paramod,[status(thm)],[c_1361,c_16]) ).
cnf(c_26118,plain,
multiplication(addition(one,B),strong_iteration(A)) = multiplication(addition(star(A),B),strong_iteration(A)),
inference(paramod,[status(thm)],[c_42,c_26117]) ).
cnf(c_1366,plain,
multiplication(addition(star(A),B),strong_iteration(A)) = multiplication(addition(one,B),strong_iteration(A)),
inference(copy,[status(thm)],[c_26118]) ).
cnf(c_26119,plain,
addition(one,addition(multiplication(A,star(A)),multiplication(star(A),star(B)))) = multiplication(star(A),star(B)),
inference(paramod,[status(thm)],[c_144,c_44]) ).
cnf(c_1557,plain,
addition(one,multiplication(star(A),addition(A,star(B)))) = multiplication(star(A),star(B)),
inference(paramod,[status(thm)],[c_809,c_26119]) ).
cnf(c_4028,plain,
multiplication(addition(A,one),star(addition(one,A))) = star(addition(one,A)),
inference(paramod,[status(thm)],[c_4,c_198]) ).
cnf(c_26120,plain,
multiplication(addition(one,multiplication(A,zero)),B) = addition(multiplication(A,zero),B),
inference(paramod,[status(thm)],[c_796,c_4]) ).
cnf(c_5002,plain,
addition(multiplication(A,zero),B) = multiplication(addition(one,multiplication(A,zero)),B),
inference(copy,[status(thm)],[c_26120]) ).
cnf(c_26121,plain,
multiplication(A,addition(one,zero)) = multiplication(addition(one,multiplication(A,zero)),A),
inference(paramod,[status(thm)],[c_796,c_37]) ).
cnf(c_26122,plain,
multiplication(A,one) = multiplication(addition(one,multiplication(A,zero)),A),
inference(paramod,[status(thm)],[c_7,c_26121]) ).
cnf(c_26123,plain,
A = multiplication(addition(one,multiplication(A,zero)),A),
inference(paramod,[status(thm)],[c_11,c_26122]) ).
cnf(c_5024,plain,
multiplication(addition(one,multiplication(A,zero)),A) = A,
inference(copy,[status(thm)],[c_26123]) ).
cnf(c_26124,plain,
addition(one,multiplication(addition(one,multiplication(A,zero)),multiplication(B,star(B)))) = addition(star(B),multiplication(A,zero)),
inference(paramod,[status(thm)],[c_796,c_44]) ).
cnf(c_26125,plain,
multiplication(addition(one,multiplication(multiplication(A,zero),B)),star(B)) = addition(star(B),multiplication(A,zero)),
inference(paramod,[status(thm)],[c_639,c_26124]) ).
cnf(c_26126,plain,
multiplication(addition(one,multiplication(A,multiplication(zero,B))),star(B)) = addition(star(B),multiplication(A,zero)),
inference(paramod,[status(thm)],[c_10,c_26125]) ).
cnf(c_26127,plain,
multiplication(addition(one,multiplication(A,zero)),star(B)) = addition(star(B),multiplication(A,zero)),
inference(paramod,[status(thm)],[c_17,c_26126]) ).
cnf(c_5035,plain,
addition(star(A),multiplication(B,zero)) = multiplication(addition(one,multiplication(B,zero)),star(A)),
inference(copy,[status(thm)],[c_26127]) ).
cnf(c_26128,plain,
addition(multiplication(star(A),B),multiplication(star(A),star(C))) = addition(one,multiplication(star(A),addition(B,star(C)))),
inference(paramod,[status(thm)],[c_905,c_111]) ).
cnf(c_26129,plain,
multiplication(star(A),addition(B,star(C))) = addition(one,multiplication(star(A),addition(B,star(C)))),
inference(paramod,[status(thm)],[c_14,c_26128]) ).
cnf(c_6109,plain,
addition(one,multiplication(star(A),addition(B,star(C)))) = multiplication(star(A),addition(B,star(C))),
inference(copy,[status(thm)],[c_26129]) ).
cnf(c_6115,plain,
multiplication(star(A),addition(A,star(B))) = multiplication(star(A),star(B)),
inference(paramod,[status(thm)],[c_6109,c_1557]) ).
cnf(c_26130,plain,
ifeq2(true,true,addition(star(star(A)),star(A)),star(A)) = star(A),
inference(paramod,[status(thm)],[c_1357,c_27]) ).
cnf(c_26131,plain,
ifeq2(true,true,addition(star(A),star(star(A))),star(A)) = star(A),
inference(paramod,[status(thm)],[c_4,c_26130]) ).
cnf(c_26132,plain,
ifeq2(true,true,star(star(A)),star(A)) = star(A),
inference(paramod,[status(thm)],[c_306,c_26131]) ).
cnf(c_6345,plain,
star(star(A)) = star(A),
inference(paramod,[status(thm)],[c_2,c_26132]) ).
cnf(c_26133,plain,
ifeq3(addition(A,star(B)),addition(A,star(B)),leq(B,addition(A,star(B))),true) = true,
inference(paramod,[status(thm)],[c_306,c_121]) ).
cnf(c_8191,plain,
leq(A,addition(B,star(A))) = true,
inference(paramod,[status(thm)],[c_1,c_26133]) ).
cnf(c_8258,plain,
leq(A,addition(star(A),B)) = true,
inference(paramod,[status(thm)],[c_4,c_8191]) ).
cnf(c_8301,plain,
leq(A,multiplication(star(B),star(A))) = true,
inference(paramod,[status(thm)],[c_48,c_8258]) ).
cnf(c_26134,plain,
ifeq(leq(star(addition(one,A)),star(addition(one,A))),true,leq(multiplication(star(A),multiplication(one,star(addition(one,A)))),star(addition(one,A))),true) = true,
inference(paramod,[status(thm)],[c_4028,c_61]) ).
cnf(c_26135,plain,
ifeq(true,true,leq(multiplication(star(A),multiplication(one,star(addition(one,A)))),star(addition(one,A))),true) = true,
inference(paramod,[status(thm)],[c_104,c_26134]) ).
cnf(c_26136,plain,
ifeq(true,true,leq(multiplication(star(A),star(addition(one,A))),star(addition(one,A))),true) = true,
inference(paramod,[status(thm)],[c_12,c_26135]) ).
cnf(c_8594,plain,
leq(multiplication(star(A),star(addition(one,A))),star(addition(one,A))) = true,
inference(paramod,[status(thm)],[c_3,c_26136]) ).
cnf(c_26137,plain,
addition(multiplication(addition(one,multiplication(A,zero)),B),C) = addition(multiplication(A,zero),addition(B,C)),
inference(paramod,[status(thm)],[c_5002,c_6]) ).
cnf(c_26138,plain,
addition(multiplication(one,B),addition(multiplication(multiplication(A,zero),B),C)) = addition(multiplication(A,zero),addition(B,C)),
inference(paramod,[status(thm)],[c_39,c_26137]) ).
cnf(c_26139,plain,
addition(B,addition(multiplication(multiplication(A,zero),B),C)) = addition(multiplication(A,zero),addition(B,C)),
inference(paramod,[status(thm)],[c_12,c_26138]) ).
cnf(c_26140,plain,
addition(B,addition(multiplication(A,multiplication(zero,B)),C)) = addition(multiplication(A,zero),addition(B,C)),
inference(paramod,[status(thm)],[c_10,c_26139]) ).
cnf(c_26141,plain,
addition(B,addition(multiplication(A,zero),C)) = addition(multiplication(A,zero),addition(B,C)),
inference(paramod,[status(thm)],[c_17,c_26140]) ).
cnf(c_26142,plain,
addition(B,multiplication(addition(one,multiplication(A,zero)),C)) = addition(multiplication(A,zero),addition(B,C)),
inference(paramod,[status(thm)],[c_5002,c_26141]) ).
cnf(c_8730,plain,
addition(A,multiplication(addition(one,multiplication(B,zero)),C)) = multiplication(addition(one,multiplication(B,zero)),addition(A,C)),
inference(paramod,[status(thm)],[c_5002,c_26142]) ).
cnf(c_26143,plain,
addition(multiplication(A,multiplication(B,zero)),C) = multiplication(addition(one,multiplication(multiplication(A,B),zero)),C),
inference(paramod,[status(thm)],[c_10,c_5002]) ).
cnf(c_8731,plain,
addition(multiplication(A,multiplication(B,zero)),C) = multiplication(addition(one,multiplication(A,multiplication(B,zero))),C),
inference(paramod,[status(thm)],[c_10,c_26143]) ).
cnf(c_26144,plain,
addition(multiplication(A,multiplication(addition(one,multiplication(B,zero)),C)),D) = addition(multiplication(A,multiplication(B,zero)),addition(multiplication(A,C),D)),
inference(paramod,[status(thm)],[c_5002,c_36]) ).
cnf(c_26145,plain,
addition(multiplication(A,multiplication(one,C)),addition(multiplication(A,multiplication(multiplication(B,zero),C)),D)) = addition(multiplication(A,multiplication(B,zero)),addition(multiplication(A,C),D)),
inference(paramod,[status(thm)],[c_206,c_26144]) ).
cnf(c_26146,plain,
addition(multiplication(A,C),addition(multiplication(A,multiplication(multiplication(B,zero),C)),D)) = addition(multiplication(A,multiplication(B,zero)),addition(multiplication(A,C),D)),
inference(paramod,[status(thm)],[c_12,c_26145]) ).
cnf(c_26147,plain,
addition(multiplication(A,C),addition(multiplication(A,multiplication(B,multiplication(zero,C))),D)) = addition(multiplication(A,multiplication(B,zero)),addition(multiplication(A,C),D)),
inference(paramod,[status(thm)],[c_10,c_26146]) ).
cnf(c_26148,plain,
addition(multiplication(A,C),addition(multiplication(A,multiplication(B,zero)),D)) = addition(multiplication(A,multiplication(B,zero)),addition(multiplication(A,C),D)),
inference(paramod,[status(thm)],[c_17,c_26147]) ).
cnf(c_26149,plain,
addition(multiplication(A,C),multiplication(addition(one,multiplication(A,multiplication(B,zero))),D)) = addition(multiplication(A,multiplication(B,zero)),addition(multiplication(A,C),D)),
inference(paramod,[status(thm)],[c_8731,c_26148]) ).
cnf(c_8734,plain,
addition(multiplication(A,B),multiplication(addition(one,multiplication(A,multiplication(C,zero))),D)) = multiplication(addition(one,multiplication(A,multiplication(C,zero))),addition(multiplication(A,B),D)),
inference(paramod,[status(thm)],[c_8731,c_26149]) ).
cnf(c_26150,plain,
addition(multiplication(A,star(B)),multiplication(addition(one,multiplication(A,multiplication(strong_iteration(B),zero))),C)) = addition(multiplication(A,strong_iteration(B)),C),
inference(paramod,[status(thm)],[c_8731,c_213]) ).
cnf(c_26151,plain,
multiplication(addition(one,multiplication(A,multiplication(strong_iteration(B),zero))),addition(multiplication(A,star(B)),C)) = addition(multiplication(A,strong_iteration(B)),C),
inference(paramod,[status(thm)],[c_8734,c_26150]) ).
cnf(c_9006,plain,
addition(multiplication(A,strong_iteration(B)),C) = multiplication(addition(one,multiplication(A,multiplication(strong_iteration(B),zero))),addition(multiplication(A,star(B)),C)),
inference(copy,[status(thm)],[c_26151]) ).
cnf(c_26152,plain,
multiplication(star(star(A)),star(A)) = multiplication(star(star(A)),star(addition(one,A))),
inference(paramod,[status(thm)],[c_1166,c_6115]) ).
cnf(c_26153,plain,
multiplication(star(A),star(A)) = multiplication(star(star(A)),star(addition(one,A))),
inference(paramod,[status(thm)],[c_6345,c_26152]) ).
cnf(c_26154,plain,
star(A) = multiplication(star(star(A)),star(addition(one,A))),
inference(paramod,[status(thm)],[c_1337,c_26153]) ).
cnf(c_26155,plain,
star(A) = multiplication(star(A),star(addition(one,A))),
inference(paramod,[status(thm)],[c_6345,c_26154]) ).
cnf(c_9299,plain,
multiplication(star(A),star(addition(one,A))) = star(A),
inference(copy,[status(thm)],[c_26155]) ).
cnf(c_9333,plain,
leq(star(A),star(addition(one,A))) = true,
inference(paramod,[status(thm)],[c_9299,c_8594]) ).
cnf(c_26156,plain,
ifeq2(true,true,star(A),star(addition(one,A))) = star(addition(one,A)),
inference(paramod,[status(thm)],[c_9333,c_1312]) ).
cnf(c_26157,plain,
star(A) = star(addition(one,A)),
inference(paramod,[status(thm)],[c_2,c_26156]) ).
cnf(c_9339,plain,
star(addition(one,A)) = star(A),
inference(copy,[status(thm)],[c_26157]) ).
cnf(c_26158,plain,
star(star(A)) = star(multiplication(A,star(A))),
inference(paramod,[status(thm)],[c_18,c_9339]) ).
cnf(c_26159,plain,
star(A) = star(multiplication(A,star(A))),
inference(paramod,[status(thm)],[c_6345,c_26158]) ).
cnf(c_9469,plain,
star(multiplication(A,star(A))) = star(A),
inference(copy,[status(thm)],[c_26159]) ).
cnf(c_9582,plain,
leq(multiplication(A,star(A)),multiplication(star(B),star(A))) = true,
inference(paramod,[status(thm)],[c_9469,c_8301]) ).
cnf(c_9713,plain,
addition(star(A),multiplication(B,star(B))) = addition(star(A),star(B)),
inference(paramod,[status(thm)],[c_143,c_113]) ).
cnf(c_9714,plain,
addition(star(A),multiplication(B,strong_iteration(B))) = addition(star(A),strong_iteration(B)),
inference(paramod,[status(thm)],[c_143,c_117]) ).
cnf(c_9963,plain,
leq(addition(A,B),addition(A,star(B))) = true,
inference(paramod,[status(thm)],[c_306,c_156]) ).
cnf(c_9964,plain,
leq(addition(A,B),addition(A,strong_iteration(B))) = true,
inference(paramod,[status(thm)],[c_309,c_156]) ).
cnf(c_10047,plain,
leq(addition(A,B),addition(star(B),A)) = true,
inference(paramod,[status(thm)],[c_4,c_9963]) ).
cnf(c_26160,plain,
ifeq2(true,true,addition(star(A),addition(addition(B,A),B)),addition(star(A),B)) = addition(star(A),B),
inference(paramod,[status(thm)],[c_10047,c_120]) ).
cnf(c_26161,plain,
ifeq2(true,true,addition(star(A),addition(B,addition(B,A))),addition(star(A),B)) = addition(star(A),B),
inference(paramod,[status(thm)],[c_4,c_26160]) ).
cnf(c_26162,plain,
ifeq2(true,true,addition(star(A),addition(B,A)),addition(star(A),B)) = addition(star(A),B),
inference(paramod,[status(thm)],[c_33,c_26161]) ).
cnf(c_10249,plain,
addition(star(A),addition(B,A)) = addition(star(A),B),
inference(paramod,[status(thm)],[c_2,c_26162]) ).
cnf(c_10709,plain,
leq(addition(star(A),B),addition(star(A),strong_iteration(addition(B,A)))) = true,
inference(paramod,[status(thm)],[c_10249,c_9964]) ).
cnf(c_26163,plain,
ifeq2(true,true,addition(multiplication(star(A),star(B)),multiplication(B,star(B))),multiplication(star(A),star(B))) = multiplication(star(A),star(B)),
inference(paramod,[status(thm)],[c_9582,c_91]) ).
cnf(c_26164,plain,
ifeq2(true,true,multiplication(addition(star(A),B),star(B)),multiplication(star(A),star(B))) = multiplication(star(A),star(B)),
inference(paramod,[status(thm)],[c_16,c_26163]) ).
cnf(c_11431,plain,
multiplication(addition(star(A),B),star(B)) = multiplication(star(A),star(B)),
inference(paramod,[status(thm)],[c_2,c_26164]) ).
cnf(c_26165,plain,
addition(star(A),addition(multiplication(B,strong_iteration(B)),A)) = addition(star(A),strong_iteration(B)),
inference(paramod,[status(thm)],[c_9714,c_10249]) ).
cnf(c_26166,plain,
addition(star(A),multiplication(addition(one,multiplication(B,multiplication(strong_iteration(B),zero))),addition(multiplication(B,star(B)),A))) = addition(star(A),strong_iteration(B)),
inference(paramod,[status(thm)],[c_9006,c_26165]) ).
cnf(c_26167,plain,
addition(star(A),multiplication(addition(one,multiplication(strong_iteration(B),zero)),addition(multiplication(B,star(B)),A))) = addition(star(A),strong_iteration(B)),
inference(paramod,[status(thm)],[c_434,c_26166]) ).
cnf(c_26168,plain,
multiplication(addition(one,multiplication(strong_iteration(B),zero)),addition(star(A),addition(multiplication(B,star(B)),A))) = addition(star(A),strong_iteration(B)),
inference(paramod,[status(thm)],[c_8730,c_26167]) ).
cnf(c_26169,plain,
multiplication(addition(one,multiplication(strong_iteration(B),zero)),addition(star(A),multiplication(B,star(B)))) = addition(star(A),strong_iteration(B)),
inference(paramod,[status(thm)],[c_10249,c_26168]) ).
cnf(c_26170,plain,
multiplication(addition(one,multiplication(strong_iteration(B),zero)),addition(star(A),star(B))) = addition(star(A),strong_iteration(B)),
inference(paramod,[status(thm)],[c_9713,c_26169]) ).
cnf(c_13097,plain,
addition(star(A),strong_iteration(B)) = multiplication(addition(one,multiplication(strong_iteration(B),zero)),addition(star(A),star(B))),
inference(copy,[status(thm)],[c_26170]) ).
cnf(c_13185,plain,
leq(addition(star(A),B),multiplication(addition(one,multiplication(strong_iteration(addition(B,A)),zero)),addition(star(A),star(addition(B,A))))) = true,
inference(paramod,[status(thm)],[c_13097,c_10709]) ).
cnf(c_26171,plain,
multiplication(star(addition(A,B)),addition(one,A)) = multiplication(star(addition(A,B)),addition(one,addition(A,B))),
inference(paramod,[status(thm)],[c_133,c_225]) ).
cnf(c_18553,plain,
multiplication(star(addition(A,B)),addition(one,A)) = star(addition(A,B)),
inference(paramod,[status(thm)],[c_166,c_26171]) ).
cnf(c_26172,plain,
ifeq(leq(addition(one,star(addition(A,B))),star(addition(A,B))),true,leq(star(addition(one,A)),star(addition(A,B))),true) = true,
inference(paramod,[status(thm)],[c_18553,c_70]) ).
cnf(c_26173,plain,
ifeq(leq(star(addition(A,B)),star(addition(A,B))),true,leq(star(addition(one,A)),star(addition(A,B))),true) = true,
inference(paramod,[status(thm)],[c_134,c_26172]) ).
cnf(c_26174,plain,
ifeq(true,true,leq(star(addition(one,A)),star(addition(A,B))),true) = true,
inference(paramod,[status(thm)],[c_104,c_26173]) ).
cnf(c_26175,plain,
ifeq(true,true,leq(star(A),star(addition(A,B))),true) = true,
inference(paramod,[status(thm)],[c_9339,c_26174]) ).
cnf(c_19749,plain,
leq(star(A),star(addition(A,B))) = true,
inference(paramod,[status(thm)],[c_3,c_26175]) ).
cnf(c_19846,plain,
leq(star(A),star(addition(B,A))) = true,
inference(paramod,[status(thm)],[c_4,c_19749]) ).
cnf(c_26176,plain,
ifeq2(true,true,addition(star(A),star(addition(A,B))),star(addition(A,B))) = star(addition(A,B)),
inference(paramod,[status(thm)],[c_19749,c_27]) ).
cnf(c_19850,plain,
addition(star(A),star(addition(A,B))) = star(addition(A,B)),
inference(paramod,[status(thm)],[c_2,c_26176]) ).
cnf(c_26177,plain,
ifeq2(true,true,addition(star(A),star(addition(B,A))),star(addition(B,A))) = star(addition(B,A)),
inference(paramod,[status(thm)],[c_19846,c_27]) ).
cnf(c_19887,plain,
addition(star(A),star(addition(B,A))) = star(addition(B,A)),
inference(paramod,[status(thm)],[c_2,c_26177]) ).
cnf(c_26178,plain,
leq(addition(star(A),B),multiplication(addition(one,multiplication(strong_iteration(addition(B,A)),zero)),star(addition(B,A)))) = true,
inference(paramod,[status(thm)],[c_19887,c_13185]) ).
cnf(c_19915,plain,
leq(addition(star(A),B),strong_iteration(addition(B,A))) = true,
inference(paramod,[status(thm)],[c_622,c_26178]) ).
cnf(c_19973,plain,
leq(addition(A,star(B)),strong_iteration(addition(A,B))) = true,
inference(paramod,[status(thm)],[c_4,c_19915]) ).
cnf(c_26179,plain,
ifeq2(true,true,addition(addition(A,star(B)),strong_iteration(addition(A,B))),strong_iteration(addition(A,B))) = strong_iteration(addition(A,B)),
inference(paramod,[status(thm)],[c_19973,c_27]) ).
cnf(c_26180,plain,
ifeq2(true,true,addition(A,addition(star(B),strong_iteration(addition(A,B)))),strong_iteration(addition(A,B))) = strong_iteration(addition(A,B)),
inference(paramod,[status(thm)],[c_6,c_26179]) ).
cnf(c_26181,plain,
ifeq2(true,true,addition(A,multiplication(addition(one,multiplication(strong_iteration(addition(A,B)),zero)),addition(star(B),star(addition(A,B))))),strong_iteration(addition(A,B))) = strong_iteration(addition(A,B)),
inference(paramod,[status(thm)],[c_13097,c_26180]) ).
cnf(c_26182,plain,
ifeq2(true,true,addition(A,multiplication(addition(one,multiplication(strong_iteration(addition(A,B)),zero)),star(addition(A,B)))),strong_iteration(addition(A,B))) = strong_iteration(addition(A,B)),
inference(paramod,[status(thm)],[c_19887,c_26181]) ).
cnf(c_26183,plain,
ifeq2(true,true,addition(A,strong_iteration(addition(A,B))),strong_iteration(addition(A,B))) = strong_iteration(addition(A,B)),
inference(paramod,[status(thm)],[c_622,c_26182]) ).
cnf(c_20090,plain,
addition(A,strong_iteration(addition(A,B))) = strong_iteration(addition(A,B)),
inference(paramod,[status(thm)],[c_2,c_26183]) ).
cnf(c_26184,plain,
multiplication(star(addition(A,B)),star(star(addition(A,B)))) = multiplication(star(A),star(star(addition(A,B)))),
inference(paramod,[status(thm)],[c_19850,c_11431]) ).
cnf(c_26185,plain,
multiplication(star(addition(A,B)),star(addition(A,B))) = multiplication(star(A),star(star(addition(A,B)))),
inference(paramod,[status(thm)],[c_6345,c_26184]) ).
cnf(c_26186,plain,
star(addition(A,B)) = multiplication(star(A),star(star(addition(A,B)))),
inference(paramod,[status(thm)],[c_1337,c_26185]) ).
cnf(c_26187,plain,
star(addition(A,B)) = multiplication(star(A),star(addition(A,B))),
inference(paramod,[status(thm)],[c_6345,c_26186]) ).
cnf(c_20635,plain,
multiplication(star(A),star(addition(A,B))) = star(addition(A,B)),
inference(copy,[status(thm)],[c_26187]) ).
cnf(c_26188,plain,
multiplication(star(A),star(strong_iteration(addition(A,B)))) = star(addition(A,strong_iteration(addition(A,B)))),
inference(paramod,[status(thm)],[c_20090,c_20635]) ).
cnf(c_21462,plain,
multiplication(star(A),star(strong_iteration(addition(A,B)))) = star(strong_iteration(addition(A,B))),
inference(paramod,[status(thm)],[c_20090,c_26188]) ).
cnf(c_26189,plain,
multiplication(addition(star(A),multiplication(strong_iteration(A),zero)),strong_iteration(A)) = strong_iteration(A),
inference(paramod,[status(thm)],[c_5024,c_1366]) ).
cnf(c_26190,plain,
multiplication(multiplication(addition(one,multiplication(strong_iteration(A),zero)),star(A)),strong_iteration(A)) = strong_iteration(A),
inference(paramod,[status(thm)],[c_5035,c_26189]) ).
cnf(c_25134,plain,
multiplication(strong_iteration(A),strong_iteration(A)) = strong_iteration(A),
inference(paramod,[status(thm)],[c_622,c_26190]) ).
cnf(c_26191,plain,
ifeq(leq(addition(one,strong_iteration(A)),strong_iteration(A)),true,leq(star(strong_iteration(A)),strong_iteration(A)),true) = true,
inference(paramod,[status(thm)],[c_25134,c_58]) ).
cnf(c_26192,plain,
ifeq(leq(strong_iteration(A),strong_iteration(A)),true,leq(star(strong_iteration(A)),strong_iteration(A)),true) = true,
inference(paramod,[status(thm)],[c_137,c_26191]) ).
cnf(c_26193,plain,
ifeq(true,true,leq(star(strong_iteration(A)),strong_iteration(A)),true) = true,
inference(paramod,[status(thm)],[c_104,c_26192]) ).
cnf(c_25167,plain,
leq(star(strong_iteration(A)),strong_iteration(A)) = true,
inference(paramod,[status(thm)],[c_3,c_26193]) ).
cnf(c_26194,plain,
ifeq2(true,true,addition(star(strong_iteration(A)),strong_iteration(A)),strong_iteration(A)) = strong_iteration(A),
inference(paramod,[status(thm)],[c_25167,c_27]) ).
cnf(c_26195,plain,
ifeq2(true,true,addition(strong_iteration(A),star(strong_iteration(A))),strong_iteration(A)) = strong_iteration(A),
inference(paramod,[status(thm)],[c_4,c_26194]) ).
cnf(c_26196,plain,
ifeq2(true,true,star(strong_iteration(A)),strong_iteration(A)) = strong_iteration(A),
inference(paramod,[status(thm)],[c_306,c_26195]) ).
cnf(c_25205,plain,
star(strong_iteration(A)) = strong_iteration(A),
inference(paramod,[status(thm)],[c_2,c_26196]) ).
cnf(c_26197,plain,
multiplication(star(A),strong_iteration(addition(A,B))) = star(strong_iteration(addition(A,B))),
inference(paramod,[status(thm)],[c_25205,c_21462]) ).
cnf(c_25338,plain,
multiplication(star(A),strong_iteration(addition(A,B))) = strong_iteration(addition(A,B)),
inference(paramod,[status(thm)],[c_25205,c_26197]) ).
cnf(c_26198,plain,
multiplication(star(A),strong_iteration(multiplication(star(B),A))) = strong_iteration(addition(A,multiplication(B,multiplication(star(B),A)))),
inference(paramod,[status(thm)],[c_48,c_25338]) ).
cnf(c_26010,plain,
multiplication(star(A),strong_iteration(multiplication(star(B),A))) = strong_iteration(multiplication(star(B),A)),
inference(paramod,[status(thm)],[c_48,c_26198]) ).
cnf(c_26199,plain,
tuple(leq(strong_iteration(multiplication(star(sK2_goals_X0),sK1_goals_X1)),strong_iteration(multiplication(star(sK2_goals_X0),sK1_goals_X1))),true) != tuple(true,true),
inference(paramod,[status(thm)],[c_26010,c_803]) ).
cnf(c_26200,plain,
tuple(true,true) != tuple(true,true),
inference(paramod,[status(thm)],[c_104,c_26199]) ).
cnf(c_26027,plain,
$false,
inference(copy,[status(thm)],[c_26200]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KLE147-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n012.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Fri Sep 25 19:26:50 UTC 2026
% 0.12/0.35 % CPUTime :
% 0.12/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.12/0.36 % Process 2774557 was started by sandbox2 on n012,
% 0.12/0.36 % Fri Sep 25 19:26:50 2026
% 0.12/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.12/0.36
% 0.12/0.36 % From the command line: assign(max_seconds, 300).
% 103.69/14.41
% 103.69/14.41 % given #500 (W,wt=31): 9495 leq(addition(one,A),multiplication(star(A),strong_iteration(B))) = true. [para(9339(a,1),8304(a,1,2,1))].
% 103.69/14.41
% 103.69/14.41 % SZS status Unsatisfiable for theBenchmark
% 103.69/14.41
% 103.69/14.41 % Proof 1 at 4.80 (+ 1.19) seconds.
% 103.69/14.41 % Length of proof is 145.
% 103.69/14.41 % Level of proof is 21.
% 103.69/14.41 % Maximum clause weight is 68.000.
% 103.69/14.41 % Given clauses 983.
% 103.69/14.41
% 103.69/14.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------