%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : KLE147-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n010.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 : Fri Sep 25 01:51:43 PM UTC 2026
% Result : Unsatisfiable 194.27s 25.14s
% Output : CNFRefutation 194.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 60
% Number of leaves : 24
% Syntax : Number of clauses : 283 ( 283 unt; 0 nHn; 5 RR)
% Number of literals : 283 ( 282 equ; 4 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 7 ( 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 : 474 ( 43 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t21,axiom,
addition(multiplication(X1,X2),multiplication(X3,X2)) = multiplication(addition(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t40,plain,
addition(multiplication(X1,X2),multiplication(X3,X2)) = multiplication(addition(X1,X3),X2),
inference(orient,[status(thm)],[t21]) ).
cnf(t17,axiom,
ifeq2(leq(X1,X2),true,addition(X1,X2),X2) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t31,plain,
ifeq2(leq(X1,X2),true,addition(X1,X2),X2) = X2,
inference(orient,[status(thm)],[t17]) ).
cnf(t8,axiom,
addition(X1,X2) = addition(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t48,plain,
addition(X1,X2) = addition(X2,X1),
inference(orient,[status(thm)],[t8]) ).
cnf(t52,plain,
X1 = ifeq2(leq(X2,X1),true,addition(X1,X2),X1),
inference(cp,[status(thm)],[t31,t48]) ).
cnf(t3130,plain,
ifeq2(leq(X1,X2),true,addition(X2,X1),X2) = X2,
inference(orient,[status(thm)],[t52]) ).
cnf(t24,axiom,
ifeq(leq(addition(multiplication(X1,X2),X3),X2),true,leq(multiplication(star(X1),X3),X2),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t94,plain,
ifeq(leq(addition(multiplication(X1,X2),X3),X2),true,leq(multiplication(star(X1),X3),X2),true) = true,
inference(orient,[status(thm)],[t24]) ).
cnf(t96,plain,
true = ifeq(leq(multiplication(addition(X1,X2),X3),X3),true,leq(multiplication(star(X1),multiplication(X2,X3)),X3),true),
inference(cp,[status(thm)],[t94,t40]) ).
cnf(t47872,plain,
ifeq(leq(multiplication(addition(X1,X2),X3),X3),true,leq(multiplication(star(X1),multiplication(X2,X3)),X3),true) = true,
inference(orient,[status(thm)],[t96]) ).
cnf(t18,axiom,
ifeq3(addition(X1,X2),X2,leq(X1,X2),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t120,plain,
ifeq3(addition(X1,X2),X2,leq(X1,X2),true) = true,
inference(orient,[status(thm)],[t18]) ).
cnf(t16,axiom,
addition(addition(X1,X2),X3) = addition(X1,addition(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t53,plain,
addition(addition(X1,X2),X3) = addition(X1,addition(X2,X3)),
inference(orient,[status(thm)],[t16]) ).
cnf(t0,axiom,
addition(X1,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t27,plain,
addition(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t56,plain,
addition(X1,addition(X1,X2)) = addition(X1,X2),
inference(cp,[status(thm)],[t53,t27]) ).
cnf(t150,plain,
addition(X1,addition(X1,X2)) = addition(X1,X2),
inference(orient,[status(thm)],[t56]) ).
cnf(t159,plain,
true = ifeq3(addition(X1,X2),addition(X1,X2),leq(X1,addition(X1,X2)),true),
inference(cp,[status(thm)],[t120,t150]) ).
cnf(t11,axiom,
ifeq3(X1,X1,X2,X3) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t34,plain,
ifeq3(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t11]) ).
cnf(t194796,plain,
true = leq(X1,addition(X1,X2)),
inference(step,[status(thm)],[t159,t34]) ).
cnf(t173,plain,
leq(X1,addition(X1,X2)) = true,
inference(orient,[status(thm)],[t194796]) ).
cnf(t178,plain,
true = leq(X1,addition(X2,X1)),
inference(cp,[status(thm)],[t173,t48]) ).
cnf(t184,plain,
leq(X1,addition(X2,X1)) = true,
inference(orient,[status(thm)],[t178]) ).
cnf(t13,axiom,
addition(one,multiplication(X1,star(X1))) = star(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t71,plain,
addition(one,multiplication(X1,star(X1))) = star(X1),
inference(orient,[status(thm)],[t13]) ).
cnf(t188,plain,
true = leq(multiplication(X1,star(X1)),star(X1)),
inference(cp,[status(thm)],[t184,t71]) ).
cnf(t350,plain,
leq(multiplication(X1,star(X1)),star(X1)) = true,
inference(orient,[status(thm)],[t188]) ).
cnf(t352,plain,
star(X1) = ifeq2(true,true,addition(multiplication(X1,star(X1)),star(X1)),star(X1)),
inference(cp,[status(thm)],[t31,t350]) ).
cnf(t10,axiom,
ifeq2(X1,X1,X2,X3) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t30,plain,
ifeq2(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t10]) ).
cnf(t194857,plain,
star(X1) = addition(multiplication(X1,star(X1)),star(X1)),
inference(step,[status(thm)],[t352,t30]) ).
cnf(t194858,plain,
star(X1) = addition(star(X1),multiplication(X1,star(X1))),
inference(step,[status(thm)],[t194857,t48]) ).
cnf(t6,axiom,
multiplication(one,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t26,plain,
multiplication(one,X1) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t42,plain,
multiplication(addition(one,X1),X2) = addition(X2,multiplication(X1,X2)),
inference(cp,[status(thm)],[t40,t26]) ).
cnf(t234,plain,
addition(X1,multiplication(X2,X1)) = multiplication(addition(one,X2),X1),
inference(orient,[status(thm)],[t42]) ).
cnf(t194859,plain,
star(X1) = multiplication(addition(one,X1),star(X1)),
inference(step,[status(thm)],[t194858,t234]) ).
cnf(t1731,plain,
multiplication(addition(one,X1),star(X1)) = star(X1),
inference(orient,[status(thm)],[t194859]) ).
cnf(t1761,plain,
star(X1) = multiplication(addition(X1,one),star(X1)),
inference(cp,[status(thm)],[t1731,t48]) ).
cnf(t1778,plain,
multiplication(addition(X1,one),star(X1)) = star(X1),
inference(orient,[status(thm)],[t1761]) ).
cnf(t47885,plain,
true = ifeq(leq(star(X1),star(X1)),true,leq(multiplication(star(X1),multiplication(one,star(X1))),star(X1)),true),
inference(cp,[status(thm)],[t47872,t1778]) ).
cnf(hi18,axiom,
ifeq3(addition(A,B),B,leq(A,B),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(hi3,axiom,
addition(A,A) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t3,plain,
leq(X1,X1) = true,
inference(hyper_resolution,[status(thm)],[hi18,hi3]) ).
cnf(t81,plain,
leq(X1,X1) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(t195324,plain,
true = ifeq(true,true,leq(multiplication(star(X1),multiplication(one,star(X1))),star(X1)),true),
inference(step,[status(thm)],[t47885,t81]) ).
cnf(t9,axiom,
ifeq(X1,X1,X2,X3) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t29,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t9]) ).
cnf(t195325,plain,
true = leq(multiplication(star(X1),multiplication(one,star(X1))),star(X1)),
inference(step,[status(thm)],[t195324,t29]) ).
cnf(t195326,plain,
true = leq(multiplication(star(X1),star(X1)),star(X1)),
inference(step,[status(thm)],[t195325,t26]) ).
cnf(t48137,plain,
leq(multiplication(star(X1),star(X1)),star(X1)) = true,
inference(orient,[status(thm)],[t195326]) ).
cnf(t48149,plain,
star(X1) = ifeq2(true,true,addition(star(X1),multiplication(star(X1),star(X1))),star(X1)),
inference(cp,[status(thm)],[t3130,t48137]) ).
cnf(t195327,plain,
star(X1) = addition(star(X1),multiplication(star(X1),star(X1))),
inference(step,[status(thm)],[t48149,t30]) ).
cnf(t195328,plain,
star(X1) = multiplication(addition(one,star(X1)),star(X1)),
inference(step,[status(thm)],[t195327,t234]) ).
cnf(t20,axiom,
addition(multiplication(X1,X2),multiplication(X1,X3)) = multiplication(X1,addition(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t36,plain,
addition(multiplication(X1,X2),multiplication(X1,X3)) = multiplication(X1,addition(X2,X3)),
inference(orient,[status(thm)],[t20]) ).
cnf(t5,axiom,
multiplication(X1,one) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t25,plain,
multiplication(X1,one) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t37,plain,
multiplication(X1,addition(one,X2)) = addition(X1,multiplication(X1,X2)),
inference(cp,[status(thm)],[t36,t25]) ).
cnf(t222,plain,
addition(X1,multiplication(X1,X2)) = multiplication(X1,addition(one,X2)),
inference(orient,[status(thm)],[t37]) ).
cnf(t235,plain,
multiplication(addition(one,X1),X1) = multiplication(X1,addition(one,X1)),
inference(cp,[status(thm)],[t234,t222]) ).
cnf(t269,plain,
multiplication(addition(one,X1),X1) = multiplication(X1,addition(one,X1)),
inference(orient,[status(thm)],[t235]) ).
cnf(t195329,plain,
star(X1) = multiplication(star(X1),addition(one,star(X1))),
inference(step,[status(thm)],[t195328,t269]) ).
cnf(t14,axiom,
addition(one,multiplication(star(X1),X1)) = star(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t77,plain,
addition(one,multiplication(star(X1),X1)) = star(X1),
inference(orient,[status(thm)],[t14]) ).
cnf(t153,plain,
addition(one,multiplication(star(X1),X1)) = addition(one,star(X1)),
inference(cp,[status(thm)],[t150,t77]) ).
cnf(t194792,plain,
star(X1) = addition(one,star(X1)),
inference(step,[status(thm)],[t153,t77]) ).
cnf(t163,plain,
addition(one,star(X1)) = star(X1),
inference(orient,[status(thm)],[t194792]) ).
cnf(t195330,plain,
star(X1) = multiplication(star(X1),star(X1)),
inference(step,[status(thm)],[t195329,t163]) ).
cnf(t48151,plain,
multiplication(star(X1),star(X1)) = star(X1),
inference(orient,[status(thm)],[t195330]) ).
cnf(t48162,plain,
multiplication(addition(star(X1),X2),star(X1)) = addition(star(X1),multiplication(X2,star(X1))),
inference(cp,[status(thm)],[t40,t48151]) ).
cnf(t195354,plain,
multiplication(addition(star(X1),X2),star(X1)) = multiplication(addition(one,X2),star(X1)),
inference(step,[status(thm)],[t48162,t234]) ).
cnf(t48613,plain,
multiplication(addition(star(X1),X2),star(X1)) = multiplication(addition(one,X2),star(X1)),
inference(orient,[status(thm)],[t195354]) ).
cnf(t157,plain,
addition(X1,X2) = addition(X1,addition(X2,X1)),
inference(cp,[status(thm)],[t150,t48]) ).
cnf(t201,plain,
addition(X1,addition(X2,X1)) = addition(X1,X2),
inference(orient,[status(thm)],[t157]) ).
cnf(t48634,plain,
multiplication(addition(one,addition(X1,star(X2))),star(X2)) = multiplication(addition(star(X2),X1),star(X2)),
inference(cp,[status(thm)],[t48613,t201]) ).
cnf(t189,plain,
true = leq(X1,addition(X2,addition(X3,X1))),
inference(cp,[status(thm)],[t184,t53]) ).
cnf(t356,plain,
leq(X1,addition(X2,addition(X3,X1))) = true,
inference(orient,[status(thm)],[t189]) ).
cnf(t358,plain,
true = leq(X1,addition(addition(X2,X1),X3)),
inference(cp,[status(thm)],[t356,t48]) ).
cnf(t194801,plain,
true = leq(X1,addition(X2,addition(X1,X3))),
inference(step,[status(thm)],[t358,t53]) ).
cnf(t433,plain,
leq(X1,addition(X2,addition(X1,X3))) = true,
inference(orient,[status(thm)],[t194801]) ).
cnf(t439,plain,
true = leq(one,addition(X1,star(X2))),
inference(cp,[status(thm)],[t433,t163]) ).
cnf(t457,plain,
leq(one,addition(X1,star(X2))) = true,
inference(orient,[status(thm)],[t439]) ).
cnf(t460,plain,
addition(X1,star(X2)) = ifeq2(true,true,addition(one,addition(X1,star(X2))),addition(X1,star(X2))),
inference(cp,[status(thm)],[t31,t457]) ).
cnf(t194808,plain,
addition(X1,star(X2)) = addition(one,addition(X1,star(X2))),
inference(step,[status(thm)],[t460,t30]) ).
cnf(t589,plain,
addition(one,addition(X1,star(X2))) = addition(X1,star(X2)),
inference(orient,[status(thm)],[t194808]) ).
cnf(t195361,plain,
multiplication(addition(X1,star(X2)),star(X2)) = multiplication(addition(star(X2),X1),star(X2)),
inference(step,[status(thm)],[t48634,t589]) ).
cnf(t195362,plain,
multiplication(addition(X1,star(X2)),star(X2)) = multiplication(addition(one,X1),star(X2)),
inference(step,[status(thm)],[t195361,t48613]) ).
cnf(t48940,plain,
multiplication(addition(X1,star(X2)),star(X2)) = multiplication(addition(one,X1),star(X2)),
inference(orient,[status(thm)],[t195362]) ).
cnf(t186,plain,
true = leq(multiplication(star(X1),X1),star(X1)),
inference(cp,[status(thm)],[t184,t77]) ).
cnf(t340,plain,
leq(multiplication(star(X1),X1),star(X1)) = true,
inference(orient,[status(thm)],[t186]) ).
cnf(t341,plain,
star(X1) = ifeq2(true,true,addition(multiplication(star(X1),X1),star(X1)),star(X1)),
inference(cp,[status(thm)],[t31,t340]) ).
cnf(t194820,plain,
star(X1) = addition(multiplication(star(X1),X1),star(X1)),
inference(step,[status(thm)],[t341,t30]) ).
cnf(t194821,plain,
star(X1) = addition(star(X1),multiplication(star(X1),X1)),
inference(step,[status(thm)],[t194820,t48]) ).
cnf(t194822,plain,
star(X1) = multiplication(star(X1),addition(one,X1)),
inference(step,[status(thm)],[t194821,t222]) ).
cnf(t660,plain,
multiplication(star(X1),addition(one,X1)) = star(X1),
inference(orient,[status(thm)],[t194822]) ).
cnf(t673,plain,
multiplication(addition(one,star(X1)),addition(one,X1)) = addition(addition(one,X1),star(X1)),
inference(cp,[status(thm)],[t234,t660]) ).
cnf(t194823,plain,
multiplication(star(X1),addition(one,X1)) = addition(addition(one,X1),star(X1)),
inference(step,[status(thm)],[t673,t163]) ).
cnf(t194824,plain,
star(X1) = addition(addition(one,X1),star(X1)),
inference(step,[status(thm)],[t194823,t660]) ).
cnf(t194825,plain,
star(X1) = addition(one,addition(X1,star(X1))),
inference(step,[status(thm)],[t194824,t53]) ).
cnf(t194826,plain,
star(X1) = addition(X1,star(X1)),
inference(step,[status(thm)],[t194825,t589]) ).
cnf(t688,plain,
addition(X1,star(X1)) = star(X1),
inference(orient,[status(thm)],[t194826]) ).
cnf(t689,plain,
star(addition(X1,X2)) = addition(X1,addition(X2,star(addition(X1,X2)))),
inference(cp,[status(thm)],[t688,t53]) ).
cnf(t30510,plain,
addition(X1,addition(X2,star(addition(X1,X2)))) = star(addition(X1,X2)),
inference(orient,[status(thm)],[t689]) ).
cnf(t30556,plain,
star(addition(X1,addition(X1,X2))) = addition(X1,addition(addition(X1,X2),star(addition(X1,X2)))),
inference(cp,[status(thm)],[t30510,t150]) ).
cnf(t195222,plain,
star(addition(X1,X2)) = addition(X1,addition(addition(X1,X2),star(addition(X1,X2)))),
inference(step,[status(thm)],[t30556,t150]) ).
cnf(t195223,plain,
star(addition(X1,X2)) = addition(X1,addition(X1,addition(X2,star(addition(X1,X2))))),
inference(step,[status(thm)],[t195222,t53]) ).
cnf(t195224,plain,
star(addition(X1,X2)) = addition(X1,star(addition(X1,X2))),
inference(step,[status(thm)],[t195223,t30510]) ).
cnf(t31091,plain,
addition(X1,star(addition(X1,X2))) = star(addition(X1,X2)),
inference(orient,[status(thm)],[t195224]) ).
cnf(t48951,plain,
multiplication(addition(one,X1),star(addition(X1,X2))) = multiplication(star(addition(X1,X2)),star(addition(X1,X2))),
inference(cp,[status(thm)],[t48940,t31091]) ).
cnf(t195370,plain,
multiplication(addition(one,X1),star(addition(X1,X2))) = star(addition(X1,X2)),
inference(step,[status(thm)],[t48951,t48151]) ).
cnf(t49296,plain,
multiplication(addition(one,X1),star(addition(X1,X2))) = star(addition(X1,X2)),
inference(orient,[status(thm)],[t195370]) ).
cnf(t15,axiom,
addition(star(X1),multiplication(strong_iteration(X1),zero)) = strong_iteration(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t68,plain,
addition(star(X1),multiplication(strong_iteration(X1),zero)) = strong_iteration(X1),
inference(orient,[status(thm)],[t15]) ).
cnf(t70,plain,
addition(star(X1),addition(multiplication(strong_iteration(X1),zero),X2)) = addition(strong_iteration(X1),X2),
inference(cp,[status(thm)],[t53,t68]) ).
cnf(t17327,plain,
addition(star(X1),addition(multiplication(strong_iteration(X1),zero),X2)) = addition(strong_iteration(X1),X2),
inference(orient,[status(thm)],[t70]) ).
cnf(t49417,plain,
star(addition(star(X1),addition(multiplication(strong_iteration(X1),zero),X2))) = multiplication(addition(one,star(X1)),star(addition(strong_iteration(X1),X2))),
inference(cp,[status(thm)],[t49296,t17327]) ).
cnf(t195509,plain,
star(addition(strong_iteration(X1),X2)) = multiplication(addition(one,star(X1)),star(addition(strong_iteration(X1),X2))),
inference(step,[status(thm)],[t49417,t17327]) ).
cnf(t195510,plain,
star(addition(strong_iteration(X1),X2)) = multiplication(star(X1),star(addition(strong_iteration(X1),X2))),
inference(step,[status(thm)],[t195509,t163]) ).
cnf(t62866,plain,
multiplication(star(X1),star(addition(strong_iteration(X1),X2))) = star(addition(strong_iteration(X1),X2)),
inference(orient,[status(thm)],[t195510]) ).
cnf(t22,axiom,
ifeq(leq(X1,addition(multiplication(X2,X1),X3)),true,leq(X1,multiplication(strong_iteration(X2),X3)),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t82,plain,
ifeq(leq(X1,addition(multiplication(X2,X1),X3)),true,leq(X1,multiplication(strong_iteration(X2),X3)),true) = true,
inference(orient,[status(thm)],[t22]) ).
cnf(t93,plain,
true = ifeq(leq(X1,addition(multiplication(X2,X1),one)),true,leq(X1,strong_iteration(X2)),true),
inference(cp,[status(thm)],[t82,t25]) ).
cnf(t195244,plain,
true = ifeq(leq(X1,addition(one,multiplication(X2,X1))),true,leq(X1,strong_iteration(X2)),true),
inference(step,[status(thm)],[t93,t48]) ).
cnf(t39423,plain,
ifeq(leq(X1,addition(one,multiplication(X2,X1))),true,leq(X1,strong_iteration(X2)),true) = true,
inference(orient,[status(thm)],[t195244]) ).
cnf(t12,axiom,
addition(multiplication(X1,strong_iteration(X1)),one) = strong_iteration(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t194786,plain,
addition(one,multiplication(X1,strong_iteration(X1))) = strong_iteration(X1),
inference(step,[status(thm)],[t12,t48]) ).
cnf(t62,plain,
addition(one,multiplication(X1,strong_iteration(X1))) = strong_iteration(X1),
inference(orient,[status(thm)],[t194786]) ).
cnf(t67,plain,
addition(one,addition(multiplication(X1,strong_iteration(X1)),X2)) = addition(strong_iteration(X1),X2),
inference(cp,[status(thm)],[t53,t62]) ).
cnf(t14429,plain,
addition(one,addition(multiplication(X1,strong_iteration(X1)),X2)) = addition(strong_iteration(X1),X2),
inference(orient,[status(thm)],[t67]) ).
cnf(t14442,plain,
addition(strong_iteration(X1),multiplication(X2,strong_iteration(X1))) = addition(one,multiplication(addition(X1,X2),strong_iteration(X1))),
inference(cp,[status(thm)],[t14429,t40]) ).
cnf(t196128,plain,
multiplication(addition(one,X2),strong_iteration(X1)) = addition(one,multiplication(addition(X1,X2),strong_iteration(X1))),
inference(step,[status(thm)],[t14442,t234]) ).
cnf(t179951,plain,
addition(one,multiplication(addition(X1,X2),strong_iteration(X1))) = multiplication(addition(one,X2),strong_iteration(X1)),
inference(orient,[status(thm)],[t196128]) ).
cnf(t180723,plain,
true = ifeq(leq(strong_iteration(X1),multiplication(addition(one,X2),strong_iteration(X1))),true,leq(strong_iteration(X1),strong_iteration(addition(X1,X2))),true),
inference(cp,[status(thm)],[t39423,t179951]) ).
cnf(t243,plain,
true = leq(X1,multiplication(addition(one,X2),X1)),
inference(cp,[status(thm)],[t173,t234]) ).
cnf(t423,plain,
leq(X1,multiplication(addition(one,X2),X1)) = true,
inference(orient,[status(thm)],[t243]) ).
cnf(t196129,plain,
true = ifeq(true,true,leq(strong_iteration(X1),strong_iteration(addition(X1,X2))),true),
inference(step,[status(thm)],[t180723,t423]) ).
cnf(t196130,plain,
true = leq(strong_iteration(X1),strong_iteration(addition(X1,X2))),
inference(step,[status(thm)],[t196129,t29]) ).
cnf(t180804,plain,
leq(strong_iteration(X1),strong_iteration(addition(X1,X2))) = true,
inference(orient,[status(thm)],[t196130]) ).
cnf(t180882,plain,
true = leq(strong_iteration(X1),strong_iteration(multiplication(addition(one,X2),X1))),
inference(cp,[status(thm)],[t180804,t234]) ).
cnf(t184219,plain,
leq(strong_iteration(X1),strong_iteration(multiplication(addition(one,X2),X1))) = true,
inference(orient,[status(thm)],[t180882]) ).
cnf(t184348,plain,
true = leq(strong_iteration(X1),strong_iteration(multiplication(star(X2),X1))),
inference(cp,[status(thm)],[t184219,t163]) ).
cnf(t184498,plain,
leq(strong_iteration(X1),strong_iteration(multiplication(star(X2),X1))) = true,
inference(orient,[status(thm)],[t184348]) ).
cnf(t184598,plain,
strong_iteration(multiplication(star(X1),X2)) = ifeq2(true,true,addition(strong_iteration(X2),strong_iteration(multiplication(star(X1),X2))),strong_iteration(multiplication(star(X1),X2))),
inference(cp,[status(thm)],[t31,t184498]) ).
cnf(t196196,plain,
strong_iteration(multiplication(star(X1),X2)) = addition(strong_iteration(X2),strong_iteration(multiplication(star(X1),X2))),
inference(step,[status(thm)],[t184598,t30]) ).
cnf(t189883,plain,
addition(strong_iteration(X1),strong_iteration(multiplication(star(X2),X1))) = strong_iteration(multiplication(star(X2),X1)),
inference(orient,[status(thm)],[t196196]) ).
cnf(t190235,plain,
star(addition(strong_iteration(X1),strong_iteration(multiplication(star(X2),X1)))) = multiplication(star(X1),star(strong_iteration(multiplication(star(X2),X1)))),
inference(cp,[status(thm)],[t62866,t189883]) ).
cnf(t196246,plain,
star(strong_iteration(multiplication(star(X2),X1))) = multiplication(star(X1),star(strong_iteration(multiplication(star(X2),X1)))),
inference(step,[status(thm)],[t190235,t189883]) ).
cnf(t97,plain,
true = ifeq(leq(multiplication(X1,X2),X2),true,leq(multiplication(star(X1),multiplication(X1,X2)),X2),true),
inference(cp,[status(thm)],[t94,t27]) ).
cnf(t19,axiom,
multiplication(multiplication(X1,X2),X3) = multiplication(X1,multiplication(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t35,plain,
multiplication(multiplication(X1,X2),X3) = multiplication(X1,multiplication(X2,X3)),
inference(orient,[status(thm)],[t19]) ).
cnf(t270,plain,
multiplication(multiplication(star(X1),X1),addition(one,multiplication(star(X1),X1))) = multiplication(star(X1),multiplication(star(X1),X1)),
inference(cp,[status(thm)],[t269,t77]) ).
cnf(t195313,plain,
multiplication(star(X1),multiplication(X1,addition(one,multiplication(star(X1),X1)))) = multiplication(star(X1),multiplication(star(X1),X1)),
inference(step,[status(thm)],[t270,t35]) ).
cnf(t195314,plain,
multiplication(star(X1),multiplication(X1,star(X1))) = multiplication(star(X1),multiplication(star(X1),X1)),
inference(step,[status(thm)],[t195313,t77]) ).
cnf(t47099,plain,
multiplication(star(X1),multiplication(star(X1),X1)) = multiplication(star(X1),multiplication(X1,star(X1))),
inference(orient,[status(thm)],[t195314]) ).
cnf(t272,plain,
multiplication(multiplication(X1,star(X1)),addition(one,multiplication(X1,star(X1)))) = multiplication(star(X1),multiplication(X1,star(X1))),
inference(cp,[status(thm)],[t269,t71]) ).
cnf(t195317,plain,
multiplication(X1,multiplication(star(X1),addition(one,multiplication(X1,star(X1))))) = multiplication(star(X1),multiplication(X1,star(X1))),
inference(step,[status(thm)],[t272,t35]) ).
cnf(t195318,plain,
multiplication(X1,multiplication(star(X1),star(X1))) = multiplication(star(X1),multiplication(X1,star(X1))),
inference(step,[status(thm)],[t195317,t71]) ).
cnf(t47313,plain,
multiplication(star(X1),multiplication(X1,star(X1))) = multiplication(X1,multiplication(star(X1),star(X1))),
inference(orient,[status(thm)],[t195318]) ).
cnf(t195319,plain,
multiplication(star(X1),multiplication(star(X1),X1)) = multiplication(X1,multiplication(star(X1),star(X1))),
inference(step,[status(thm)],[t47099,t47313]) ).
cnf(t47314,plain,
multiplication(star(X1),multiplication(star(X1),X1)) = multiplication(X1,multiplication(star(X1),star(X1))),
inference(orient,[status(thm)],[t195319]) ).
cnf(t195331,plain,
multiplication(star(X1),multiplication(star(X1),X1)) = multiplication(X1,star(X1)),
inference(step,[status(thm)],[t47314,t48151]) ).
cnf(t48152,plain,
multiplication(star(X1),multiplication(star(X1),X1)) = multiplication(X1,star(X1)),
inference(orient,[status(thm)],[t195331]) ).
cnf(t48166,plain,
multiplication(star(X1),multiplication(star(X1),X2)) = multiplication(star(X1),X2),
inference(cp,[status(thm)],[t35,t48151]) ).
cnf(t48272,plain,
multiplication(star(X1),multiplication(star(X1),X2)) = multiplication(star(X1),X2),
inference(orient,[status(thm)],[t48166]) ).
cnf(t195344,plain,
multiplication(star(X1),X1) = multiplication(X1,star(X1)),
inference(step,[status(thm)],[t48152,t48272]) ).
cnf(t48304,plain,
multiplication(star(X1),X1) = multiplication(X1,star(X1)),
inference(rw,[status(thm)],[t195344]) ).
cnf(t48305,plain,
multiplication(star(X1),X1) = multiplication(X1,star(X1)),
inference(orient,[status(thm)],[t48304]) ).
cnf(t48315,plain,
multiplication(star(X1),multiplication(X1,X2)) = multiplication(multiplication(X1,star(X1)),X2),
inference(cp,[status(thm)],[t35,t48305]) ).
cnf(t195349,plain,
multiplication(star(X1),multiplication(X1,X2)) = multiplication(X1,multiplication(star(X1),X2)),
inference(step,[status(thm)],[t48315,t35]) ).
cnf(t48366,plain,
multiplication(star(X1),multiplication(X1,X2)) = multiplication(X1,multiplication(star(X1),X2)),
inference(orient,[status(thm)],[t195349]) ).
cnf(t195390,plain,
true = ifeq(leq(multiplication(X1,X2),X2),true,leq(multiplication(X1,multiplication(star(X1),X2)),X2),true),
inference(step,[status(thm)],[t97,t48366]) ).
cnf(t52797,plain,
ifeq(leq(multiplication(X1,X2),X2),true,leq(multiplication(X1,multiplication(star(X1),X2)),X2),true) = true,
inference(orient,[status(thm)],[t195390]) ).
cnf(t41,plain,
multiplication(addition(multiplication(X1,X2),X3),Y3) = addition(multiplication(X1,multiplication(X2,Y3)),multiplication(X3,Y3)),
inference(cp,[status(thm)],[t40,t35]) ).
cnf(t804,plain,
addition(multiplication(X1,multiplication(X2,X3)),multiplication(Y3,X3)) = multiplication(addition(multiplication(X1,X2),Y3),X3),
inference(orient,[status(thm)],[t41]) ).
cnf(t7,axiom,
multiplication(zero,X1) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t46,plain,
multiplication(zero,X1) = zero,
inference(orient,[status(thm)],[t7]) ).
cnf(t821,plain,
multiplication(addition(multiplication(X1,zero),X2),X3) = addition(multiplication(X1,zero),multiplication(X2,X3)),
inference(cp,[status(thm)],[t804,t46]) ).
cnf(t51045,plain,
addition(multiplication(X1,zero),multiplication(X2,X3)) = multiplication(addition(multiplication(X1,zero),X2),X3),
inference(orient,[status(thm)],[t821]) ).
cnf(t51046,plain,
multiplication(addition(multiplication(X1,zero),X2),zero) = multiplication(addition(X1,X2),zero),
inference(cp,[status(thm)],[t51045,t40]) ).
cnf(t51381,plain,
multiplication(addition(multiplication(X1,zero),X2),zero) = multiplication(addition(X1,X2),zero),
inference(orient,[status(thm)],[t51046]) ).
cnf(t51385,plain,
multiplication(addition(X1,multiplication(X2,zero)),zero) = multiplication(multiplication(addition(X1,X2),zero),zero),
inference(cp,[status(thm)],[t51381,t40]) ).
cnf(t195381,plain,
multiplication(addition(X1,multiplication(X2,zero)),zero) = multiplication(addition(X1,X2),multiplication(zero,zero)),
inference(step,[status(thm)],[t51385,t35]) ).
cnf(t195382,plain,
multiplication(addition(X1,multiplication(X2,zero)),zero) = multiplication(addition(X1,X2),zero),
inference(step,[status(thm)],[t195381,t46]) ).
cnf(t51595,plain,
multiplication(addition(X1,multiplication(X2,zero)),zero) = multiplication(addition(X1,X2),zero),
inference(orient,[status(thm)],[t195382]) ).
cnf(t51623,plain,
multiplication(addition(X1,multiplication(X2,zero)),addition(one,zero)) = addition(addition(X1,multiplication(X2,zero)),multiplication(addition(X1,X2),zero)),
inference(cp,[status(thm)],[t222,t51595]) ).
cnf(t1,axiom,
addition(X1,zero) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t28,plain,
addition(X1,zero) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t195383,plain,
multiplication(addition(X1,multiplication(X2,zero)),one) = addition(addition(X1,multiplication(X2,zero)),multiplication(addition(X1,X2),zero)),
inference(step,[status(thm)],[t51623,t28]) ).
cnf(t195384,plain,
addition(X1,multiplication(X2,zero)) = addition(addition(X1,multiplication(X2,zero)),multiplication(addition(X1,X2),zero)),
inference(step,[status(thm)],[t195383,t25]) ).
cnf(t195385,plain,
addition(X1,multiplication(X2,zero)) = addition(X1,addition(multiplication(X2,zero),multiplication(addition(X1,X2),zero))),
inference(step,[status(thm)],[t195384,t53]) ).
cnf(t195386,plain,
addition(X1,multiplication(X2,zero)) = addition(X1,multiplication(addition(multiplication(X2,zero),addition(X1,X2)),zero)),
inference(step,[status(thm)],[t195385,t51045]) ).
cnf(t195387,plain,
addition(X1,multiplication(X2,zero)) = addition(X1,multiplication(addition(X2,addition(X1,X2)),zero)),
inference(step,[status(thm)],[t195386,t51381]) ).
cnf(t195388,plain,
addition(X1,multiplication(X2,zero)) = addition(X1,multiplication(addition(X2,X1),zero)),
inference(step,[status(thm)],[t195387,t201]) ).
cnf(t51769,plain,
addition(X1,multiplication(addition(X2,X1),zero)) = addition(X1,multiplication(X2,zero)),
inference(orient,[status(thm)],[t195388]) ).
cnf(t51819,plain,
addition(addition(X1,X2),multiplication(X2,zero)) = addition(addition(X1,X2),multiplication(addition(X2,X1),zero)),
inference(cp,[status(thm)],[t51769,t201]) ).
cnf(t195546,plain,
addition(X1,addition(X2,multiplication(X2,zero))) = addition(addition(X1,X2),multiplication(addition(X2,X1),zero)),
inference(step,[status(thm)],[t51819,t53]) ).
cnf(t195547,plain,
addition(X1,multiplication(X2,addition(one,zero))) = addition(addition(X1,X2),multiplication(addition(X2,X1),zero)),
inference(step,[status(thm)],[t195546,t222]) ).
cnf(t195548,plain,
addition(X1,multiplication(X2,one)) = addition(addition(X1,X2),multiplication(addition(X2,X1),zero)),
inference(step,[status(thm)],[t195547,t28]) ).
cnf(t195549,plain,
addition(X1,X2) = addition(addition(X1,X2),multiplication(addition(X2,X1),zero)),
inference(step,[status(thm)],[t195548,t25]) ).
cnf(t195550,plain,
addition(X1,X2) = addition(X1,addition(X2,multiplication(addition(X2,X1),zero))),
inference(step,[status(thm)],[t195549,t53]) ).
cnf(t51863,plain,
addition(X1,multiplication(X2,zero)) = addition(X1,multiplication(addition(X1,X2),zero)),
inference(cp,[status(thm)],[t51769,t48]) ).
cnf(t52076,plain,
addition(X1,multiplication(addition(X1,X2),zero)) = addition(X1,multiplication(X2,zero)),
inference(orient,[status(thm)],[t51863]) ).
cnf(t195551,plain,
addition(X1,X2) = addition(X1,addition(X2,multiplication(X1,zero))),
inference(step,[status(thm)],[t195550,t52076]) ).
cnf(t65114,plain,
addition(X1,addition(X2,multiplication(X1,zero))) = addition(X1,X2),
inference(orient,[status(thm)],[t195551]) ).
cnf(t65226,plain,
true = leq(multiplication(X1,zero),addition(X1,X2)),
inference(cp,[status(thm)],[t356,t65114]) ).
cnf(t65284,plain,
leq(multiplication(X1,zero),addition(X1,X2)) = true,
inference(orient,[status(thm)],[t65226]) ).
cnf(t65292,plain,
true = leq(multiplication(X1,zero),multiplication(addition(one,X2),X1)),
inference(cp,[status(thm)],[t65284,t234]) ).
cnf(t65947,plain,
leq(multiplication(X1,zero),multiplication(addition(one,X2),X1)) = true,
inference(orient,[status(thm)],[t65292]) ).
cnf(t65975,plain,
true = leq(multiplication(X1,zero),multiplication(star(X2),X1)),
inference(cp,[status(thm)],[t65947,t163]) ).
cnf(t66001,plain,
leq(multiplication(X1,zero),multiplication(star(X2),X1)) = true,
inference(orient,[status(thm)],[t65975]) ).
cnf(t66028,plain,
multiplication(star(X1),X2) = ifeq2(true,true,addition(multiplication(star(X1),X2),multiplication(X2,zero)),multiplication(star(X1),X2)),
inference(cp,[status(thm)],[t3130,t66001]) ).
cnf(t195563,plain,
multiplication(star(X1),X2) = addition(multiplication(star(X1),X2),multiplication(X2,zero)),
inference(step,[status(thm)],[t66028,t30]) ).
cnf(t43,plain,
multiplication(addition(X1,multiplication(X2,X3)),Y3) = addition(multiplication(X1,Y3),multiplication(X2,multiplication(X3,Y3))),
inference(cp,[status(thm)],[t40,t35]) ).
cnf(t1250,plain,
addition(multiplication(X1,X2),multiplication(X3,multiplication(Y3,X2))) = multiplication(addition(X1,multiplication(X3,Y3)),X2),
inference(orient,[status(thm)],[t43]) ).
cnf(t1282,plain,
multiplication(addition(X1,multiplication(X2,zero)),X3) = addition(multiplication(X1,X3),multiplication(X2,zero)),
inference(cp,[status(thm)],[t1250,t46]) ).
cnf(t52328,plain,
addition(multiplication(X1,X2),multiplication(X3,zero)) = multiplication(addition(X1,multiplication(X3,zero)),X2),
inference(orient,[status(thm)],[t1282]) ).
cnf(t195564,plain,
multiplication(star(X1),X2) = multiplication(addition(star(X1),multiplication(X2,zero)),X2),
inference(step,[status(thm)],[t195563,t52328]) ).
cnf(t67031,plain,
multiplication(addition(star(X1),multiplication(X2,zero)),X2) = multiplication(star(X1),X2),
inference(orient,[status(thm)],[t195564]) ).
cnf(t17333,plain,
addition(strong_iteration(X1),multiplication(strong_iteration(X1),X2)) = addition(star(X1),multiplication(strong_iteration(X1),addition(zero,X2))),
inference(cp,[status(thm)],[t17327,t36]) ).
cnf(t195201,plain,
multiplication(strong_iteration(X1),addition(one,X2)) = addition(star(X1),multiplication(strong_iteration(X1),addition(zero,X2))),
inference(step,[status(thm)],[t17333,t222]) ).
cnf(t49,plain,
addition(zero,X1) = X1,
inference(cp,[status(thm)],[t48,t28]) ).
cnf(t136,plain,
addition(zero,X1) = X1,
inference(orient,[status(thm)],[t49]) ).
cnf(t195202,plain,
multiplication(strong_iteration(X1),addition(one,X2)) = addition(star(X1),multiplication(strong_iteration(X1),X2)),
inference(step,[status(thm)],[t195201,t136]) ).
cnf(t29557,plain,
addition(star(X1),multiplication(strong_iteration(X1),X2)) = multiplication(strong_iteration(X1),addition(one,X2)),
inference(orient,[status(thm)],[t195202]) ).
cnf(t67032,plain,
multiplication(star(X1),strong_iteration(X1)) = multiplication(multiplication(strong_iteration(X1),addition(one,zero)),strong_iteration(X1)),
inference(cp,[status(thm)],[t67031,t29557]) ).
cnf(t187,plain,
true = leq(multiplication(X1,strong_iteration(X1)),strong_iteration(X1)),
inference(cp,[status(thm)],[t184,t62]) ).
cnf(t345,plain,
leq(multiplication(X1,strong_iteration(X1)),strong_iteration(X1)) = true,
inference(orient,[status(thm)],[t187]) ).
cnf(t347,plain,
strong_iteration(X1) = ifeq2(true,true,addition(multiplication(X1,strong_iteration(X1)),strong_iteration(X1)),strong_iteration(X1)),
inference(cp,[status(thm)],[t31,t345]) ).
cnf(t194854,plain,
strong_iteration(X1) = addition(multiplication(X1,strong_iteration(X1)),strong_iteration(X1)),
inference(step,[status(thm)],[t347,t30]) ).
cnf(t194855,plain,
strong_iteration(X1) = addition(strong_iteration(X1),multiplication(X1,strong_iteration(X1))),
inference(step,[status(thm)],[t194854,t48]) ).
cnf(t194856,plain,
strong_iteration(X1) = multiplication(addition(one,X1),strong_iteration(X1)),
inference(step,[status(thm)],[t194855,t234]) ).
cnf(t1625,plain,
multiplication(addition(one,X1),strong_iteration(X1)) = strong_iteration(X1),
inference(orient,[status(thm)],[t194856]) ).
cnf(t1655,plain,
strong_iteration(X1) = multiplication(addition(X1,one),strong_iteration(X1)),
inference(cp,[status(thm)],[t1625,t48]) ).
cnf(t1680,plain,
multiplication(addition(X1,one),strong_iteration(X1)) = strong_iteration(X1),
inference(orient,[status(thm)],[t1655]) ).
cnf(t47887,plain,
true = ifeq(leq(strong_iteration(X1),strong_iteration(X1)),true,leq(multiplication(star(X1),multiplication(one,strong_iteration(X1))),strong_iteration(X1)),true),
inference(cp,[status(thm)],[t47872,t1680]) ).
cnf(t195335,plain,
true = ifeq(true,true,leq(multiplication(star(X1),multiplication(one,strong_iteration(X1))),strong_iteration(X1)),true),
inference(step,[status(thm)],[t47887,t81]) ).
cnf(t195336,plain,
true = leq(multiplication(star(X1),multiplication(one,strong_iteration(X1))),strong_iteration(X1)),
inference(step,[status(thm)],[t195335,t29]) ).
cnf(t195337,plain,
true = leq(multiplication(star(X1),strong_iteration(X1)),strong_iteration(X1)),
inference(step,[status(thm)],[t195336,t26]) ).
cnf(t48193,plain,
leq(multiplication(star(X1),strong_iteration(X1)),strong_iteration(X1)) = true,
inference(orient,[status(thm)],[t195337]) ).
cnf(t48199,plain,
strong_iteration(X1) = ifeq2(true,true,addition(strong_iteration(X1),multiplication(star(X1),strong_iteration(X1))),strong_iteration(X1)),
inference(cp,[status(thm)],[t3130,t48193]) ).
cnf(t195338,plain,
strong_iteration(X1) = addition(strong_iteration(X1),multiplication(star(X1),strong_iteration(X1))),
inference(step,[status(thm)],[t48199,t30]) ).
cnf(t195339,plain,
strong_iteration(X1) = multiplication(addition(one,star(X1)),strong_iteration(X1)),
inference(step,[status(thm)],[t195338,t234]) ).
cnf(t195340,plain,
strong_iteration(X1) = multiplication(star(X1),strong_iteration(X1)),
inference(step,[status(thm)],[t195339,t163]) ).
cnf(t48202,plain,
multiplication(star(X1),strong_iteration(X1)) = strong_iteration(X1),
inference(orient,[status(thm)],[t195340]) ).
cnf(t195565,plain,
strong_iteration(X1) = multiplication(multiplication(strong_iteration(X1),addition(one,zero)),strong_iteration(X1)),
inference(step,[status(thm)],[t67032,t48202]) ).
cnf(t195566,plain,
strong_iteration(X1) = multiplication(strong_iteration(X1),multiplication(addition(one,zero),strong_iteration(X1))),
inference(step,[status(thm)],[t195565,t35]) ).
cnf(t195567,plain,
strong_iteration(X1) = multiplication(strong_iteration(X1),multiplication(one,strong_iteration(X1))),
inference(step,[status(thm)],[t195566,t28]) ).
cnf(t195568,plain,
strong_iteration(X1) = multiplication(strong_iteration(X1),strong_iteration(X1)),
inference(step,[status(thm)],[t195567,t26]) ).
cnf(t67170,plain,
multiplication(strong_iteration(X1),strong_iteration(X1)) = strong_iteration(X1),
inference(orient,[status(thm)],[t195568]) ).
cnf(t67210,plain,
true = ifeq(leq(strong_iteration(X1),strong_iteration(X1)),true,leq(multiplication(strong_iteration(X1),multiplication(star(strong_iteration(X1)),strong_iteration(X1))),strong_iteration(X1)),true),
inference(cp,[status(thm)],[t52797,t67170]) ).
cnf(t195572,plain,
true = ifeq(true,true,leq(multiplication(strong_iteration(X1),multiplication(star(strong_iteration(X1)),strong_iteration(X1))),strong_iteration(X1)),true),
inference(step,[status(thm)],[t67210,t81]) ).
cnf(t195573,plain,
true = leq(multiplication(strong_iteration(X1),multiplication(star(strong_iteration(X1)),strong_iteration(X1))),strong_iteration(X1)),
inference(step,[status(thm)],[t195572,t29]) ).
cnf(t154,plain,
addition(one,multiplication(X1,strong_iteration(X1))) = addition(one,strong_iteration(X1)),
inference(cp,[status(thm)],[t150,t62]) ).
cnf(t194794,plain,
strong_iteration(X1) = addition(one,strong_iteration(X1)),
inference(step,[status(thm)],[t154,t62]) ).
cnf(t168,plain,
addition(one,strong_iteration(X1)) = strong_iteration(X1),
inference(orient,[status(thm)],[t194794]) ).
cnf(t1736,plain,
star(strong_iteration(X1)) = multiplication(strong_iteration(X1),star(strong_iteration(X1))),
inference(cp,[status(thm)],[t1731,t168]) ).
cnf(t1796,plain,
multiplication(strong_iteration(X1),star(strong_iteration(X1))) = star(strong_iteration(X1)),
inference(orient,[status(thm)],[t1736]) ).
cnf(t1801,plain,
multiplication(strong_iteration(X1),multiplication(star(strong_iteration(X1)),X2)) = multiplication(star(strong_iteration(X1)),X2),
inference(cp,[status(thm)],[t35,t1796]) ).
cnf(t60397,plain,
multiplication(strong_iteration(X1),multiplication(star(strong_iteration(X1)),X2)) = multiplication(star(strong_iteration(X1)),X2),
inference(orient,[status(thm)],[t1801]) ).
cnf(t195574,plain,
true = leq(multiplication(star(strong_iteration(X1)),strong_iteration(X1)),strong_iteration(X1)),
inference(step,[status(thm)],[t195573,t60397]) ).
cnf(t665,plain,
star(strong_iteration(X1)) = multiplication(star(strong_iteration(X1)),strong_iteration(X1)),
inference(cp,[status(thm)],[t660,t168]) ).
cnf(t947,plain,
multiplication(star(strong_iteration(X1)),strong_iteration(X1)) = star(strong_iteration(X1)),
inference(orient,[status(thm)],[t665]) ).
cnf(t195575,plain,
true = leq(star(strong_iteration(X1)),strong_iteration(X1)),
inference(step,[status(thm)],[t195574,t947]) ).
cnf(t67215,plain,
leq(star(strong_iteration(X1)),strong_iteration(X1)) = true,
inference(orient,[status(thm)],[t195575]) ).
cnf(t67218,plain,
strong_iteration(X1) = ifeq2(true,true,addition(strong_iteration(X1),star(strong_iteration(X1))),strong_iteration(X1)),
inference(cp,[status(thm)],[t3130,t67215]) ).
cnf(t195576,plain,
strong_iteration(X1) = addition(strong_iteration(X1),star(strong_iteration(X1))),
inference(step,[status(thm)],[t67218,t30]) ).
cnf(t195577,plain,
strong_iteration(X1) = star(strong_iteration(X1)),
inference(step,[status(thm)],[t195576,t688]) ).
cnf(t67223,plain,
star(strong_iteration(X1)) = strong_iteration(X1),
inference(orient,[status(thm)],[t195577]) ).
cnf(t196247,plain,
strong_iteration(multiplication(star(X2),X1)) = multiplication(star(X1),star(strong_iteration(multiplication(star(X2),X1)))),
inference(step,[status(thm)],[t196246,t67223]) ).
cnf(t196248,plain,
strong_iteration(multiplication(star(X2),X1)) = multiplication(star(X1),strong_iteration(multiplication(star(X2),X1))),
inference(step,[status(thm)],[t196247,t67223]) ).
cnf(t194644,plain,
multiplication(star(X1),strong_iteration(multiplication(star(X2),X1))) = strong_iteration(multiplication(star(X2),X1)),
inference(orient,[status(thm)],[t196248]) ).
cnf(t424,plain,
true = leq(X1,multiplication(star(X2),X1)),
inference(cp,[status(thm)],[t423,t163]) ).
cnf(t430,plain,
leq(X1,multiplication(star(X2),X1)) = true,
inference(orient,[status(thm)],[t424]) ).
cnf(goal_0,negated_conjecture,
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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
tuple(leq(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(rw,[status(thm)],[goal_0,t194644]) ).
cnf(g0_1,plain,
tuple(true,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(rw,[status(thm)],[g0_0,t81]) ).
cnf(g0_2,plain,
tuple(true,true) != tuple(true,true),
inference(rw,[status(thm)],[g0_1,t430]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KLE147-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.58 % Computer : n010.cluster.edu
% 0.10/0.58 % Model : x86_64 x86_64
% 0.10/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.58 % Memory : 8046.5625MB
% 0.10/0.58 % OS : Linux 6.8.0-71-generic
% 0.10/0.58 % CPULimit : 300
% 0.10/0.58 % WCLimit : 300
% 0.10/0.58 % DateTime : Wed Sep 23 19:05:48 UTC 2026
% 0.10/0.58 % CPUTime :
% 0.10/0.58 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 194.27/25.14 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 194.27/25.14 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------