%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : KLE044-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n008.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:28 PM UTC 2026
% Result : Unsatisfiable 62.00s 14.42s
% Output : CNFRefutation 62.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 58
% Number of leaves : 21
% Syntax : Number of clauses : 240 ( 240 unt; 0 nHn; 6 RR)
% Number of literals : 240 ( 239 equ; 5 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 4 con; 0-4 aty)
% Number of variables : 400 ( 23 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t9,axiom,
addition(X1,X2) = addition(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t35,plain,
addition(X1,X2) = addition(X2,X1),
inference(orient,[status(thm)],[t9]) ).
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(t83130,plain,
ifeq(leq(addition(X3,multiplication(X1,X2)),X2),true,leq(multiplication(star(X1),X3),X2),true) = true,
inference(step,[status(thm)],[t24,t35]) ).
cnf(t101,plain,
ifeq(leq(addition(X1,multiplication(X2,X3)),X3),true,leq(multiplication(star(X2),X1),X3),true) = true,
inference(orient,[status(thm)],[t83130]) ).
cnf(hi11,axiom,
ifeq2(leq(A,B),true,addition(A,B),B) = B,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(hi13,axiom,
leq(addition(one,multiplication(A,star(A))),star(A)) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t19,plain,
addition(addition(one,multiplication(X1,star(X1))),star(X1)) = star(X1),
inference(hyper_resolution,[status(thm)],[hi11,hi13]) ).
cnf(t83124,plain,
addition(star(X1),addition(one,multiplication(X1,star(X1)))) = star(X1),
inference(step,[status(thm)],[t19,t35]) ).
cnf(t13,axiom,
addition(addition(X1,X2),X3) = addition(X1,addition(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t83123,plain,
addition(X3,addition(X1,X2)) = addition(X1,addition(X2,X3)),
inference(step,[status(thm)],[t13,t35]) ).
cnf(t38,plain,
addition(X1,addition(X2,X3)) = addition(X2,addition(X3,X1)),
inference(orient,[status(thm)],[t83123]) ).
cnf(t83125,plain,
addition(one,addition(multiplication(X1,star(X1)),star(X1))) = star(X1),
inference(step,[status(thm)],[t83124,t38]) ).
cnf(t83126,plain,
addition(one,addition(star(X1),multiplication(X1,star(X1)))) = star(X1),
inference(step,[status(thm)],[t83125,t35]) ).
cnf(t56,plain,
addition(one,addition(star(X1),multiplication(X1,star(X1)))) = star(X1),
inference(orient,[status(thm)],[t83126]) ).
cnf(t22,axiom,
addition(multiplication(X1,X2),multiplication(X3,X2)) = multiplication(addition(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t66,plain,
addition(multiplication(X1,X2),multiplication(X3,X2)) = multiplication(addition(X1,X3),X2),
inference(orient,[status(thm)],[t22]) ).
cnf(t7,axiom,
multiplication(one,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t28,plain,
multiplication(one,X1) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t68,plain,
multiplication(addition(one,X1),X2) = addition(X2,multiplication(X1,X2)),
inference(cp,[status(thm)],[t66,t28]) ).
cnf(t83141,plain,
multiplication(addition(X1,one),X2) = addition(X2,multiplication(X1,X2)),
inference(step,[status(thm)],[t68,t35]) ).
cnf(t177,plain,
addition(X1,multiplication(X2,X1)) = multiplication(addition(X2,one),X1),
inference(orient,[status(thm)],[t83141]) ).
cnf(t83142,plain,
addition(one,multiplication(addition(X1,one),star(X1))) = star(X1),
inference(step,[status(thm)],[t56,t177]) ).
cnf(t191,plain,
addition(one,multiplication(addition(X1,one),star(X1))) = star(X1),
inference(rw,[status(thm)],[t83142]) ).
cnf(t268,plain,
addition(one,multiplication(addition(X1,one),star(X1))) = star(X1),
inference(orient,[status(thm)],[t191]) ).
cnf(t275,plain,
true = ifeq(leq(star(X1),star(X1)),true,leq(multiplication(star(addition(X1,one)),one),star(X1)),true),
inference(cp,[status(thm)],[t101,t268]) ).
cnf(hi12,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)],[hi12,hi3]) ).
cnf(t91,plain,
leq(X1,X1) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(t83148,plain,
true = ifeq(true,true,leq(multiplication(star(addition(X1,one)),one),star(X1)),true),
inference(step,[status(thm)],[t275,t91]) ).
cnf(t10,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)],[t10]) ).
cnf(t83149,plain,
true = leq(multiplication(star(addition(X1,one)),one),star(X1)),
inference(step,[status(thm)],[t83148,t29]) ).
cnf(t5,axiom,
multiplication(X1,one) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t27,plain,
multiplication(X1,one) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t83150,plain,
true = leq(star(addition(X1,one)),star(X1)),
inference(step,[status(thm)],[t83149,t27]) ).
cnf(t278,plain,
leq(star(addition(X1,one)),star(X1)) = true,
inference(orient,[status(thm)],[t83150]) ).
cnf(t187,plain,
true = ifeq(leq(multiplication(addition(X1,one),X2),X2),true,leq(multiplication(star(X1),X2),X2),true),
inference(cp,[status(thm)],[t101,t177]) ).
cnf(t82986,plain,
ifeq(leq(multiplication(addition(X1,one),X2),X2),true,leq(multiplication(star(X1),X2),X2),true) = true,
inference(orient,[status(thm)],[t187]) ).
cnf(t15,axiom,
ifeq3(addition(X1,X2),X2,leq(X1,X2),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t128,plain,
ifeq3(addition(X1,X2),X2,leq(X1,X2),true) = true,
inference(orient,[status(thm)],[t15]) ).
cnf(t0,axiom,
addition(X1,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t25,plain,
addition(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t41,plain,
addition(X1,addition(X2,X1)) = addition(X2,X1),
inference(cp,[status(thm)],[t38,t25]) ).
cnf(t83136,plain,
addition(X1,addition(X1,X2)) = addition(X2,X1),
inference(step,[status(thm)],[t41,t38]) ).
cnf(t83137,plain,
addition(X1,addition(X1,X2)) = addition(X1,X2),
inference(step,[status(thm)],[t83136,t35]) ).
cnf(t151,plain,
addition(X1,addition(X1,X2)) = addition(X1,X2),
inference(orient,[status(thm)],[t83137]) ).
cnf(t160,plain,
true = ifeq3(addition(X1,X2),addition(X1,X2),leq(X1,addition(X1,X2)),true),
inference(cp,[status(thm)],[t128,t151]) ).
cnf(t12,axiom,
ifeq3(X1,X1,X2,X3) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t30,plain,
ifeq3(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t12]) ).
cnf(t83140,plain,
true = leq(X1,addition(X1,X2)),
inference(step,[status(thm)],[t160,t30]) ).
cnf(t169,plain,
leq(X1,addition(X1,X2)) = true,
inference(orient,[status(thm)],[t83140]) ).
cnf(t170,plain,
true = leq(multiplication(X1,X2),multiplication(addition(X1,X3),X2)),
inference(cp,[status(thm)],[t169,t66]) ).
cnf(t342,plain,
leq(multiplication(X1,X2),multiplication(addition(X1,X3),X2)) = true,
inference(orient,[status(thm)],[t170]) ).
cnf(t21,axiom,
addition(multiplication(X1,X2),multiplication(X1,X3)) = multiplication(X1,addition(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t73,plain,
addition(multiplication(X1,X2),multiplication(X1,X3)) = multiplication(X1,addition(X2,X3)),
inference(orient,[status(thm)],[t21]) ).
cnf(t348,plain,
true = leq(multiplication(multiplication(X1,X2),X3),multiplication(multiplication(X1,addition(X2,Y3)),X3)),
inference(cp,[status(thm)],[t342,t73]) ).
cnf(t18,axiom,
multiplication(multiplication(X1,X2),X3) = multiplication(X1,multiplication(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t80,plain,
multiplication(multiplication(X1,X2),X3) = multiplication(X1,multiplication(X2,X3)),
inference(orient,[status(thm)],[t18]) ).
cnf(t83300,plain,
true = leq(multiplication(X1,multiplication(X2,X3)),multiplication(multiplication(X1,addition(X2,Y3)),X3)),
inference(step,[status(thm)],[t348,t80]) ).
cnf(t83301,plain,
true = leq(multiplication(X1,multiplication(X2,X3)),multiplication(X1,multiplication(addition(X2,Y3),X3))),
inference(step,[status(thm)],[t83300,t80]) ).
cnf(t3602,plain,
leq(multiplication(X1,multiplication(X2,X3)),multiplication(X1,multiplication(addition(X2,Y3),X3))) = true,
inference(orient,[status(thm)],[t83301]) ).
cnf(t14,axiom,
ifeq2(leq(X1,X2),true,addition(X1,X2),X2) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t32,plain,
ifeq2(leq(X1,X2),true,addition(X1,X2),X2) = X2,
inference(orient,[status(thm)],[t14]) ).
cnf(t154,plain,
addition(one,addition(star(X1),multiplication(X1,star(X1)))) = addition(one,star(X1)),
inference(cp,[status(thm)],[t151,t56]) ).
cnf(t83138,plain,
star(X1) = addition(one,star(X1)),
inference(step,[status(thm)],[t154,t56]) ).
cnf(t163,plain,
addition(one,star(X1)) = star(X1),
inference(orient,[status(thm)],[t83138]) ).
cnf(t349,plain,
true = leq(multiplication(one,X1),multiplication(star(X2),X1)),
inference(cp,[status(thm)],[t342,t163]) ).
cnf(t83155,plain,
true = leq(X1,multiplication(star(X2),X1)),
inference(step,[status(thm)],[t349,t28]) ).
cnf(t359,plain,
leq(X1,multiplication(star(X2),X1)) = true,
inference(orient,[status(thm)],[t83155]) ).
cnf(t37,plain,
X1 = ifeq2(leq(X2,X1),true,addition(X1,X2),X1),
inference(cp,[status(thm)],[t32,t35]) ).
cnf(t306,plain,
ifeq2(leq(X1,X2),true,addition(X2,X1),X2) = X2,
inference(orient,[status(thm)],[t37]) ).
cnf(t344,plain,
true = leq(multiplication(X1,multiplication(X2,X3)),multiplication(addition(multiplication(X1,X2),Y3),X3)),
inference(cp,[status(thm)],[t342,t80]) ).
cnf(t83205,plain,
true = leq(multiplication(X1,multiplication(X2,X3)),multiplication(addition(Y3,multiplication(X1,X2)),X3)),
inference(step,[status(thm)],[t344,t35]) ).
cnf(t1181,plain,
leq(multiplication(X1,multiplication(X2,X3)),multiplication(addition(Y3,multiplication(X1,X2)),X3)) = true,
inference(orient,[status(thm)],[t83205]) ).
cnf(t1186,plain,
true = leq(multiplication(X1,X2),multiplication(addition(X3,multiplication(X1,X2)),one)),
inference(cp,[status(thm)],[t1181,t27]) ).
cnf(t83206,plain,
true = leq(multiplication(X1,X2),addition(X3,multiplication(X1,X2))),
inference(step,[status(thm)],[t1186,t27]) ).
cnf(t1217,plain,
leq(multiplication(X1,X2),addition(X3,multiplication(X1,X2))) = true,
inference(orient,[status(thm)],[t83206]) ).
cnf(hi14,axiom,
leq(addition(one,multiplication(star(A),A)),star(A)) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t20,plain,
addition(addition(one,multiplication(star(X1),X1)),star(X1)) = star(X1),
inference(hyper_resolution,[status(thm)],[hi11,hi14]) ).
cnf(t83127,plain,
addition(star(X1),addition(one,multiplication(star(X1),X1))) = star(X1),
inference(step,[status(thm)],[t20,t35]) ).
cnf(t83128,plain,
addition(one,addition(multiplication(star(X1),X1),star(X1))) = star(X1),
inference(step,[status(thm)],[t83127,t38]) ).
cnf(t83129,plain,
addition(one,addition(star(X1),multiplication(star(X1),X1))) = star(X1),
inference(step,[status(thm)],[t83128,t35]) ).
cnf(t61,plain,
addition(one,addition(star(X1),multiplication(star(X1),X1))) = star(X1),
inference(orient,[status(thm)],[t83129]) ).
cnf(t75,plain,
multiplication(X1,addition(one,X2)) = addition(X1,multiplication(X1,X2)),
inference(cp,[status(thm)],[t73,t27]) ).
cnf(t83144,plain,
multiplication(X1,addition(X2,one)) = addition(X1,multiplication(X1,X2)),
inference(step,[status(thm)],[t75,t35]) ).
cnf(t207,plain,
addition(X1,multiplication(X1,X2)) = multiplication(X1,addition(X2,one)),
inference(orient,[status(thm)],[t83144]) ).
cnf(t83145,plain,
addition(one,multiplication(star(X1),addition(X1,one))) = star(X1),
inference(step,[status(thm)],[t61,t207]) ).
cnf(t220,plain,
addition(one,multiplication(star(X1),addition(X1,one))) = star(X1),
inference(rw,[status(thm)],[t83145]) ).
cnf(t297,plain,
addition(one,multiplication(star(X1),addition(X1,one))) = star(X1),
inference(orient,[status(thm)],[t220]) ).
cnf(t1224,plain,
true = leq(multiplication(star(X1),addition(X1,one)),star(X1)),
inference(cp,[status(thm)],[t1217,t297]) ).
cnf(t1233,plain,
leq(multiplication(star(X1),addition(X1,one)),star(X1)) = true,
inference(orient,[status(thm)],[t1224]) ).
cnf(t1237,plain,
star(X1) = ifeq2(true,true,addition(star(X1),multiplication(star(X1),addition(X1,one))),star(X1)),
inference(cp,[status(thm)],[t306,t1233]) ).
cnf(t11,axiom,
ifeq2(X1,X1,X2,X3) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t31,plain,
ifeq2(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t11]) ).
cnf(t83207,plain,
star(X1) = addition(star(X1),multiplication(star(X1),addition(X1,one))),
inference(step,[status(thm)],[t1237,t31]) ).
cnf(t83208,plain,
star(X1) = multiplication(star(X1),addition(addition(X1,one),one)),
inference(step,[status(thm)],[t83207,t207]) ).
cnf(t83209,plain,
star(X1) = multiplication(star(X1),addition(one,addition(X1,one))),
inference(step,[status(thm)],[t83208,t35]) ).
cnf(t83210,plain,
star(X1) = multiplication(star(X1),addition(X1,addition(one,one))),
inference(step,[status(thm)],[t83209,t38]) ).
cnf(t83211,plain,
star(X1) = multiplication(star(X1),addition(X1,one)),
inference(step,[status(thm)],[t83210,t25]) ).
cnf(t1242,plain,
multiplication(star(X1),addition(X1,one)) = star(X1),
inference(orient,[status(thm)],[t83211]) ).
cnf(t1272,plain,
true = leq(addition(X1,one),star(X1)),
inference(cp,[status(thm)],[t359,t1242]) ).
cnf(t1295,plain,
leq(addition(X1,one),star(X1)) = true,
inference(orient,[status(thm)],[t1272]) ).
cnf(t1297,plain,
star(X1) = ifeq2(true,true,addition(addition(X1,one),star(X1)),star(X1)),
inference(cp,[status(thm)],[t32,t1295]) ).
cnf(t83216,plain,
star(X1) = addition(addition(X1,one),star(X1)),
inference(step,[status(thm)],[t1297,t31]) ).
cnf(t83217,plain,
star(X1) = addition(star(X1),addition(X1,one)),
inference(step,[status(thm)],[t83216,t35]) ).
cnf(t83218,plain,
star(X1) = addition(one,addition(star(X1),X1)),
inference(step,[status(thm)],[t83217,t38]) ).
cnf(t83219,plain,
star(X1) = addition(X1,addition(one,star(X1))),
inference(step,[status(thm)],[t83218,t38]) ).
cnf(t83220,plain,
star(X1) = addition(X1,star(X1)),
inference(step,[status(thm)],[t83219,t163]) ).
cnf(t1303,plain,
addition(X1,star(X1)) = star(X1),
inference(orient,[status(thm)],[t83220]) ).
cnf(t3668,plain,
true = leq(multiplication(X1,multiplication(X2,X3)),multiplication(X1,multiplication(star(X2),X3))),
inference(cp,[status(thm)],[t3602,t1303]) ).
cnf(t3791,plain,
leq(multiplication(X1,multiplication(X2,X3)),multiplication(X1,multiplication(star(X2),X3))) = true,
inference(orient,[status(thm)],[t3668]) ).
cnf(t181,plain,
multiplication(addition(multiplication(X1,X2),one),X3) = addition(X3,multiplication(X1,multiplication(X2,X3))),
inference(cp,[status(thm)],[t177,t80]) ).
cnf(t83158,plain,
multiplication(addition(one,multiplication(X1,X2)),X3) = addition(X3,multiplication(X1,multiplication(X2,X3))),
inference(step,[status(thm)],[t181,t35]) ).
cnf(t413,plain,
addition(X1,multiplication(X2,multiplication(X3,X1))) = multiplication(addition(one,multiplication(X2,X3)),X1),
inference(orient,[status(thm)],[t83158]) ).
cnf(t414,plain,
multiplication(addition(one,multiplication(X1,X2)),X1) = multiplication(X1,addition(multiplication(X2,X1),one)),
inference(cp,[status(thm)],[t413,t207]) ).
cnf(t83159,plain,
multiplication(addition(one,multiplication(X1,X2)),X1) = multiplication(X1,addition(one,multiplication(X2,X1))),
inference(step,[status(thm)],[t414,t35]) ).
cnf(t442,plain,
multiplication(addition(one,multiplication(X1,X2)),X1) = multiplication(X1,addition(one,multiplication(X2,X1))),
inference(orient,[status(thm)],[t83159]) ).
cnf(t443,plain,
multiplication(addition(X1,one),addition(one,multiplication(star(X1),addition(X1,one)))) = multiplication(star(X1),addition(X1,one)),
inference(cp,[status(thm)],[t442,t268]) ).
cnf(t83160,plain,
multiplication(addition(X1,one),star(X1)) = multiplication(star(X1),addition(X1,one)),
inference(step,[status(thm)],[t443,t297]) ).
cnf(t470,plain,
multiplication(addition(X1,one),star(X1)) = multiplication(star(X1),addition(X1,one)),
inference(orient,[status(thm)],[t83160]) ).
cnf(t483,plain,
true = leq(multiplication(X1,star(X1)),multiplication(star(X1),addition(X1,one))),
inference(cp,[status(thm)],[t342,t470]) ).
cnf(t622,plain,
leq(multiplication(X1,star(X1)),multiplication(star(X1),addition(X1,one))) = true,
inference(orient,[status(thm)],[t483]) ).
cnf(t83214,plain,
leq(multiplication(X1,star(X1)),star(X1)) = true,
inference(step,[status(thm)],[t622,t1242]) ).
cnf(t1287,plain,
leq(multiplication(X1,star(X1)),star(X1)) = true,
inference(rw,[status(thm)],[t83214]) ).
cnf(t1338,plain,
leq(multiplication(X1,star(X1)),star(X1)) = true,
inference(orient,[status(thm)],[t1287]) ).
cnf(t1339,plain,
true = leq(multiplication(X1,multiplication(X2,star(multiplication(X1,X2)))),star(multiplication(X1,X2))),
inference(cp,[status(thm)],[t1338,t80]) ).
cnf(t4192,plain,
leq(multiplication(X1,multiplication(X2,star(multiplication(X1,X2)))),star(multiplication(X1,X2))) = true,
inference(orient,[status(thm)],[t1339]) ).
cnf(t4227,plain,
star(multiplication(X1,X2)) = ifeq2(true,true,addition(star(multiplication(X1,X2)),multiplication(X1,multiplication(X2,star(multiplication(X1,X2))))),star(multiplication(X1,X2))),
inference(cp,[status(thm)],[t306,t4192]) ).
cnf(t83305,plain,
star(multiplication(X1,X2)) = addition(star(multiplication(X1,X2)),multiplication(X1,multiplication(X2,star(multiplication(X1,X2))))),
inference(step,[status(thm)],[t4227,t31]) ).
cnf(t83306,plain,
star(multiplication(X1,X2)) = multiplication(addition(one,multiplication(X1,X2)),star(multiplication(X1,X2))),
inference(step,[status(thm)],[t83305,t413]) ).
cnf(t4229,plain,
multiplication(addition(one,multiplication(X1,X2)),star(multiplication(X1,X2))) = star(multiplication(X1,X2)),
inference(orient,[status(thm)],[t83306]) ).
cnf(t4234,plain,
star(multiplication(star(X1),addition(X1,one))) = multiplication(addition(one,star(X1)),star(multiplication(star(X1),addition(X1,one)))),
inference(cp,[status(thm)],[t4229,t1242]) ).
cnf(t83307,plain,
star(star(X1)) = multiplication(addition(one,star(X1)),star(multiplication(star(X1),addition(X1,one)))),
inference(step,[status(thm)],[t4234,t1242]) ).
cnf(t83308,plain,
star(star(X1)) = multiplication(star(X1),star(multiplication(star(X1),addition(X1,one)))),
inference(step,[status(thm)],[t83307,t163]) ).
cnf(t83309,plain,
star(star(X1)) = multiplication(star(X1),star(star(X1))),
inference(step,[status(thm)],[t83308,t1242]) ).
cnf(t4307,plain,
multiplication(star(X1),star(star(X1))) = star(star(X1)),
inference(orient,[status(thm)],[t83309]) ).
cnf(t4345,plain,
true = leq(multiplication(X1,multiplication(X2,star(star(X2)))),multiplication(X1,star(star(X2)))),
inference(cp,[status(thm)],[t3791,t4307]) ).
cnf(t13962,plain,
leq(multiplication(X1,multiplication(X2,star(star(X2)))),multiplication(X1,star(star(X2)))) = true,
inference(orient,[status(thm)],[t4345]) ).
cnf(t82988,plain,
true = ifeq(true,true,leq(multiplication(star(X1),multiplication(addition(X1,one),star(star(addition(X1,one))))),multiplication(addition(X1,one),star(star(addition(X1,one))))),true),
inference(cp,[status(thm)],[t82986,t13962]) ).
cnf(t84559,plain,
true = leq(multiplication(star(X1),multiplication(addition(X1,one),star(star(addition(X1,one))))),multiplication(addition(X1,one),star(star(addition(X1,one))))),
inference(step,[status(thm)],[t82988,t29]) ).
cnf(t1250,plain,
multiplication(star(X1),multiplication(addition(X1,one),X2)) = multiplication(star(X1),X2),
inference(cp,[status(thm)],[t80,t1242]) ).
cnf(t1435,plain,
multiplication(star(X1),multiplication(addition(X1,one),X2)) = multiplication(star(X1),X2),
inference(orient,[status(thm)],[t1250]) ).
cnf(t84560,plain,
true = leq(multiplication(star(X1),star(star(addition(X1,one)))),multiplication(addition(X1,one),star(star(addition(X1,one))))),
inference(step,[status(thm)],[t84559,t1435]) ).
cnf(t77,plain,
multiplication(X1,X2) = ifeq2(leq(multiplication(X1,X3),multiplication(X1,X2)),true,multiplication(X1,addition(X3,X2)),multiplication(X1,X2)),
inference(cp,[status(thm)],[t32,t73]) ).
cnf(t83297,plain,
multiplication(X1,X2) = ifeq2(leq(multiplication(X1,X3),multiplication(X1,X2)),true,multiplication(X1,addition(X2,X3)),multiplication(X1,X2)),
inference(step,[status(thm)],[t77,t35]) ).
cnf(t3442,plain,
ifeq2(leq(multiplication(X1,X2),multiplication(X1,X3)),true,multiplication(X1,addition(X3,X2)),multiplication(X1,X3)) = multiplication(X1,X3),
inference(orient,[status(thm)],[t83297]) ).
cnf(t3542,plain,
multiplication(X1,one) = ifeq2(leq(multiplication(X1,star(X2)),multiplication(X1,one)),true,multiplication(X1,star(X2)),multiplication(X1,one)),
inference(cp,[status(thm)],[t3442,t163]) ).
cnf(t83539,plain,
X1 = ifeq2(leq(multiplication(X1,star(X2)),multiplication(X1,one)),true,multiplication(X1,star(X2)),multiplication(X1,one)),
inference(step,[status(thm)],[t3542,t27]) ).
cnf(t83540,plain,
X1 = ifeq2(leq(multiplication(X1,star(X2)),X1),true,multiplication(X1,star(X2)),multiplication(X1,one)),
inference(step,[status(thm)],[t83539,t27]) ).
cnf(t83541,plain,
X1 = ifeq2(leq(multiplication(X1,star(X2)),X1),true,multiplication(X1,star(X2)),X1),
inference(step,[status(thm)],[t83540,t27]) ).
cnf(t13727,plain,
ifeq2(leq(multiplication(X1,star(X2)),X1),true,multiplication(X1,star(X2)),X1) = X1,
inference(orient,[status(thm)],[t83541]) ).
cnf(t23,axiom,
ifeq(leq(addition(multiplication(X1,X2),X3),X1),true,leq(multiplication(X3,star(X2)),X1),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t83131,plain,
ifeq(leq(addition(X3,multiplication(X1,X2)),X1),true,leq(multiplication(X3,star(X2)),X1),true) = true,
inference(step,[status(thm)],[t23,t35]) ).
cnf(t114,plain,
ifeq(leq(addition(X1,multiplication(X2,X3)),X2),true,leq(multiplication(X1,star(X3)),X2),true) = true,
inference(orient,[status(thm)],[t83131]) ).
cnf(t115,plain,
true = ifeq(leq(multiplication(X1,X2),X1),true,leq(multiplication(multiplication(X1,X2),star(X2)),X1),true),
inference(cp,[status(thm)],[t114,t25]) ).
cnf(t83678,plain,
true = ifeq(leq(multiplication(X1,X2),X1),true,leq(multiplication(X1,multiplication(X2,star(X2))),X1),true),
inference(step,[status(thm)],[t115,t80]) ).
cnf(t21358,plain,
ifeq(leq(multiplication(X1,X2),X1),true,leq(multiplication(X1,multiplication(X2,star(X2))),X1),true) = true,
inference(orient,[status(thm)],[t83678]) ).
cnf(t21415,plain,
true = ifeq(leq(star(X1),star(X1)),true,leq(multiplication(star(X1),multiplication(addition(X1,one),star(addition(X1,one)))),star(X1)),true),
inference(cp,[status(thm)],[t21358,t1242]) ).
cnf(t83679,plain,
true = ifeq(true,true,leq(multiplication(star(X1),multiplication(addition(X1,one),star(addition(X1,one)))),star(X1)),true),
inference(step,[status(thm)],[t21415,t91]) ).
cnf(t83680,plain,
true = leq(multiplication(star(X1),multiplication(addition(X1,one),star(addition(X1,one)))),star(X1)),
inference(step,[status(thm)],[t83679,t29]) ).
cnf(t83681,plain,
true = leq(multiplication(star(X1),star(addition(X1,one))),star(X1)),
inference(step,[status(thm)],[t83680,t1435]) ).
cnf(t21455,plain,
leq(multiplication(star(X1),star(addition(X1,one))),star(X1)) = true,
inference(orient,[status(thm)],[t83681]) ).
cnf(t21466,plain,
star(X1) = ifeq2(true,true,multiplication(star(X1),star(addition(X1,one))),star(X1)),
inference(cp,[status(thm)],[t13727,t21455]) ).
cnf(t83682,plain,
star(X1) = multiplication(star(X1),star(addition(X1,one))),
inference(step,[status(thm)],[t21466,t31]) ).
cnf(t21470,plain,
multiplication(star(X1),star(addition(X1,one))) = star(X1),
inference(orient,[status(thm)],[t83682]) ).
cnf(t21556,plain,
true = ifeq(leq(star(X1),star(X1)),true,leq(multiplication(star(X1),multiplication(star(addition(X1,one)),star(star(addition(X1,one))))),star(X1)),true),
inference(cp,[status(thm)],[t21358,t21470]) ).
cnf(t83685,plain,
true = ifeq(true,true,leq(multiplication(star(X1),multiplication(star(addition(X1,one)),star(star(addition(X1,one))))),star(X1)),true),
inference(step,[status(thm)],[t21556,t91]) ).
cnf(t83686,plain,
true = leq(multiplication(star(X1),multiplication(star(addition(X1,one)),star(star(addition(X1,one))))),star(X1)),
inference(step,[status(thm)],[t83685,t29]) ).
cnf(t21476,plain,
multiplication(star(X1),multiplication(star(addition(X1,one)),X2)) = multiplication(star(X1),X2),
inference(cp,[status(thm)],[t80,t21470]) ).
cnf(t21624,plain,
multiplication(star(X1),multiplication(star(addition(X1,one)),X2)) = multiplication(star(X1),X2),
inference(orient,[status(thm)],[t21476]) ).
cnf(t83687,plain,
true = leq(multiplication(star(X1),star(star(addition(X1,one)))),star(X1)),
inference(step,[status(thm)],[t83686,t21624]) ).
cnf(t21752,plain,
leq(multiplication(star(X1),star(star(addition(X1,one)))),star(X1)) = true,
inference(orient,[status(thm)],[t83687]) ).
cnf(t21763,plain,
star(X1) = ifeq2(true,true,multiplication(star(X1),star(star(addition(X1,one)))),star(X1)),
inference(cp,[status(thm)],[t13727,t21752]) ).
cnf(t83688,plain,
star(X1) = multiplication(star(X1),star(star(addition(X1,one)))),
inference(step,[status(thm)],[t21763,t31]) ).
cnf(t21766,plain,
multiplication(star(X1),star(star(addition(X1,one)))) = star(X1),
inference(orient,[status(thm)],[t83688]) ).
cnf(t84561,plain,
true = leq(star(X1),multiplication(addition(X1,one),star(star(addition(X1,one))))),
inference(step,[status(thm)],[t84560,t21766]) ).
cnf(t189,plain,
addition(X1,addition(multiplication(X2,X1),X3)) = addition(X3,multiplication(addition(X2,one),X1)),
inference(cp,[status(thm)],[t38,t177]) ).
cnf(t83897,plain,
addition(X1,addition(X3,multiplication(X2,X1))) = addition(X3,multiplication(addition(X2,one),X1)),
inference(step,[status(thm)],[t189,t35]) ).
cnf(t34420,plain,
addition(X1,addition(X2,multiplication(X3,X1))) = addition(X2,multiplication(addition(X3,one),X1)),
inference(orient,[status(thm)],[t83897]) ).
cnf(t34671,plain,
addition(X1,addition(addition(X2,one),multiplication(X2,X1))) = multiplication(addition(X2,one),addition(X1,one)),
inference(cp,[status(thm)],[t34420,t207]) ).
cnf(t83898,plain,
addition(X1,addition(multiplication(X2,X1),addition(X2,one))) = multiplication(addition(X2,one),addition(X1,one)),
inference(step,[status(thm)],[t34671,t35]) ).
cnf(t83899,plain,
addition(X1,addition(one,addition(multiplication(X2,X1),X2))) = multiplication(addition(X2,one),addition(X1,one)),
inference(step,[status(thm)],[t83898,t38]) ).
cnf(t83900,plain,
addition(X1,addition(X2,addition(one,multiplication(X2,X1)))) = multiplication(addition(X2,one),addition(X1,one)),
inference(step,[status(thm)],[t83899,t38]) ).
cnf(t35173,plain,
addition(X1,addition(X2,addition(one,multiplication(X2,X1)))) = multiplication(addition(X2,one),addition(X1,one)),
inference(orient,[status(thm)],[t83900]) ).
cnf(t35336,plain,
addition(X1,addition(X2,addition(one,multiplication(X2,X1)))) = addition(X1,multiplication(addition(X2,one),addition(X1,one))),
inference(cp,[status(thm)],[t151,t35173]) ).
cnf(t84012,plain,
multiplication(addition(X2,one),addition(X1,one)) = addition(X1,multiplication(addition(X2,one),addition(X1,one))),
inference(step,[status(thm)],[t35336,t35173]) ).
cnf(t43346,plain,
addition(X1,multiplication(addition(X2,one),addition(X1,one))) = multiplication(addition(X2,one),addition(X1,one)),
inference(orient,[status(thm)],[t84012]) ).
cnf(t43356,plain,
star(multiplication(addition(X1,one),addition(one,one))) = multiplication(multiplication(addition(X1,one),addition(one,one)),star(multiplication(addition(X1,one),addition(one,one)))),
inference(cp,[status(thm)],[t4229,t43346]) ).
cnf(t84013,plain,
star(multiplication(addition(X1,one),one)) = multiplication(multiplication(addition(X1,one),addition(one,one)),star(multiplication(addition(X1,one),addition(one,one)))),
inference(step,[status(thm)],[t43356,t25]) ).
cnf(t84014,plain,
star(addition(X1,one)) = multiplication(multiplication(addition(X1,one),addition(one,one)),star(multiplication(addition(X1,one),addition(one,one)))),
inference(step,[status(thm)],[t84013,t27]) ).
cnf(t84015,plain,
star(addition(X1,one)) = multiplication(addition(X1,one),multiplication(addition(one,one),star(multiplication(addition(X1,one),addition(one,one))))),
inference(step,[status(thm)],[t84014,t80]) ).
cnf(t84016,plain,
star(addition(X1,one)) = multiplication(addition(X1,one),multiplication(one,star(multiplication(addition(X1,one),addition(one,one))))),
inference(step,[status(thm)],[t84015,t25]) ).
cnf(t84017,plain,
star(addition(X1,one)) = multiplication(addition(X1,one),star(multiplication(addition(X1,one),addition(one,one)))),
inference(step,[status(thm)],[t84016,t28]) ).
cnf(t84018,plain,
star(addition(X1,one)) = multiplication(addition(X1,one),star(multiplication(addition(X1,one),one))),
inference(step,[status(thm)],[t84017,t25]) ).
cnf(t84019,plain,
star(addition(X1,one)) = multiplication(addition(X1,one),star(addition(X1,one))),
inference(step,[status(thm)],[t84018,t27]) ).
cnf(t43389,plain,
multiplication(addition(X1,one),star(addition(X1,one))) = star(addition(X1,one)),
inference(orient,[status(thm)],[t84019]) ).
cnf(t43402,plain,
star(multiplication(addition(X1,one),star(addition(X1,one)))) = multiplication(addition(one,star(addition(X1,one))),star(multiplication(addition(X1,one),star(addition(X1,one))))),
inference(cp,[status(thm)],[t4229,t43389]) ).
cnf(t84020,plain,
star(star(addition(X1,one))) = multiplication(addition(one,star(addition(X1,one))),star(multiplication(addition(X1,one),star(addition(X1,one))))),
inference(step,[status(thm)],[t43402,t43389]) ).
cnf(t84021,plain,
star(star(addition(X1,one))) = multiplication(star(addition(X1,one)),star(multiplication(addition(X1,one),star(addition(X1,one))))),
inference(step,[status(thm)],[t84020,t163]) ).
cnf(t117,plain,
true = ifeq(leq(multiplication(X1,addition(X2,X3)),X1),true,leq(multiplication(multiplication(X1,X2),star(X3)),X1),true),
inference(cp,[status(thm)],[t114,t73]) ).
cnf(t83751,plain,
true = ifeq(leq(multiplication(X1,addition(X2,X3)),X1),true,leq(multiplication(X1,multiplication(X2,star(X3))),X1),true),
inference(step,[status(thm)],[t117,t80]) ).
cnf(t25756,plain,
ifeq(leq(multiplication(X1,addition(X2,X3)),X1),true,leq(multiplication(X1,multiplication(X2,star(X3))),X1),true) = true,
inference(orient,[status(thm)],[t83751]) ).
cnf(t102,plain,
true = ifeq(leq(multiplication(X1,X2),X2),true,leq(multiplication(star(X1),multiplication(X1,X2)),X2),true),
inference(cp,[status(thm)],[t101,t25]) ).
cnf(t6534,plain,
ifeq(leq(multiplication(X1,X2),X2),true,leq(multiplication(star(X1),multiplication(X1,X2)),X2),true) = true,
inference(orient,[status(thm)],[t102]) ).
cnf(t6536,plain,
true = ifeq(true,true,leq(multiplication(star(X1),multiplication(X1,star(X1))),star(X1)),true),
inference(cp,[status(thm)],[t6534,t1338]) ).
cnf(t83371,plain,
true = leq(multiplication(star(X1),multiplication(X1,star(X1))),star(X1)),
inference(step,[status(thm)],[t6536,t29]) ).
cnf(t6615,plain,
leq(multiplication(star(X1),multiplication(X1,star(X1))),star(X1)) = true,
inference(orient,[status(thm)],[t83371]) ).
cnf(t6620,plain,
star(X1) = ifeq2(true,true,addition(star(X1),multiplication(star(X1),multiplication(X1,star(X1)))),star(X1)),
inference(cp,[status(thm)],[t306,t6615]) ).
cnf(t83372,plain,
star(X1) = addition(star(X1),multiplication(star(X1),multiplication(X1,star(X1)))),
inference(step,[status(thm)],[t6620,t31]) ).
cnf(t83373,plain,
star(X1) = multiplication(addition(one,multiplication(star(X1),X1)),star(X1)),
inference(step,[status(thm)],[t83372,t413]) ).
cnf(t83374,plain,
star(X1) = multiplication(star(X1),addition(one,multiplication(X1,star(X1)))),
inference(step,[status(thm)],[t83373,t442]) ).
cnf(t6624,plain,
multiplication(star(X1),addition(one,multiplication(X1,star(X1)))) = star(X1),
inference(orient,[status(thm)],[t83374]) ).
cnf(t6630,plain,
multiplication(star(X1),multiplication(addition(one,multiplication(X1,star(X1))),X2)) = multiplication(star(X1),X2),
inference(cp,[status(thm)],[t80,t6624]) ).
cnf(t11511,plain,
multiplication(star(X1),multiplication(addition(one,multiplication(X1,star(X1))),X2)) = multiplication(star(X1),X2),
inference(orient,[status(thm)],[t6630]) ).
cnf(t1269,plain,
multiplication(addition(one,multiplication(X1,star(X2))),addition(X2,one)) = addition(addition(X2,one),multiplication(X1,star(X2))),
inference(cp,[status(thm)],[t413,t1242]) ).
cnf(t2802,plain,
multiplication(addition(one,multiplication(X1,star(X2))),addition(X2,one)) = addition(addition(X2,one),multiplication(X1,star(X2))),
inference(orient,[status(thm)],[t1269]) ).
cnf(t11512,plain,
multiplication(star(X1),addition(X1,one)) = multiplication(star(X1),addition(addition(X1,one),multiplication(X1,star(X1)))),
inference(cp,[status(thm)],[t11511,t2802]) ).
cnf(t83499,plain,
star(X1) = multiplication(star(X1),addition(addition(X1,one),multiplication(X1,star(X1)))),
inference(step,[status(thm)],[t11512,t1242]) ).
cnf(t11602,plain,
multiplication(star(X1),addition(addition(X1,one),multiplication(X1,star(X1)))) = star(X1),
inference(orient,[status(thm)],[t83499]) ).
cnf(t25778,plain,
true = ifeq(leq(star(X1),star(X1)),true,leq(multiplication(star(X1),multiplication(addition(X1,one),star(multiplication(X1,star(X1))))),star(X1)),true),
inference(cp,[status(thm)],[t25756,t11602]) ).
cnf(t83752,plain,
true = ifeq(true,true,leq(multiplication(star(X1),multiplication(addition(X1,one),star(multiplication(X1,star(X1))))),star(X1)),true),
inference(step,[status(thm)],[t25778,t91]) ).
cnf(t83753,plain,
true = leq(multiplication(star(X1),multiplication(addition(X1,one),star(multiplication(X1,star(X1))))),star(X1)),
inference(step,[status(thm)],[t83752,t29]) ).
cnf(t83754,plain,
true = leq(multiplication(star(X1),star(multiplication(X1,star(X1)))),star(X1)),
inference(step,[status(thm)],[t83753,t1435]) ).
cnf(t25943,plain,
leq(multiplication(star(X1),star(multiplication(X1,star(X1)))),star(X1)) = true,
inference(orient,[status(thm)],[t83754]) ).
cnf(t25952,plain,
star(X1) = ifeq2(true,true,multiplication(star(X1),star(multiplication(X1,star(X1)))),star(X1)),
inference(cp,[status(thm)],[t13727,t25943]) ).
cnf(t83755,plain,
star(X1) = multiplication(star(X1),star(multiplication(X1,star(X1)))),
inference(step,[status(thm)],[t25952,t31]) ).
cnf(t25956,plain,
multiplication(star(X1),star(multiplication(X1,star(X1)))) = star(X1),
inference(orient,[status(thm)],[t83755]) ).
cnf(t84022,plain,
star(star(addition(X1,one))) = star(addition(X1,one)),
inference(step,[status(thm)],[t84021,t25956]) ).
cnf(t43586,plain,
star(star(addition(X1,one))) = star(addition(X1,one)),
inference(orient,[status(thm)],[t84022]) ).
cnf(t84562,plain,
true = leq(star(X1),multiplication(addition(X1,one),star(addition(X1,one)))),
inference(step,[status(thm)],[t84561,t43586]) ).
cnf(t84563,plain,
true = leq(star(X1),star(addition(X1,one))),
inference(step,[status(thm)],[t84562,t43389]) ).
cnf(t83114,plain,
leq(star(X1),star(addition(X1,one))) = true,
inference(orient,[status(thm)],[t84563]) ).
cnf(goal_0,negated_conjecture,
tuple(leq(star(addition(one,sK2_goals_X0)),star(sK2_goals_X0)),leq(star(sK1_goals_X0),star(addition(one,sK1_goals_X0)))) != tuple(true,true),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
tuple(leq(star(addition(sK2_goals_X0,one)),star(sK2_goals_X0)),leq(star(sK1_goals_X0),star(addition(one,sK1_goals_X0)))) != tuple(true,true),
inference(rw,[status(thm)],[goal_0,t35]) ).
cnf(g0_1,plain,
tuple(true,leq(star(sK1_goals_X0),star(addition(one,sK1_goals_X0)))) != tuple(true,true),
inference(rw,[status(thm)],[g0_0,t278]) ).
cnf(g0_2,plain,
tuple(true,leq(star(sK1_goals_X0),star(addition(sK1_goals_X0,one)))) != tuple(true,true),
inference(rw,[status(thm)],[g0_1,t35]) ).
cnf(g0_3,plain,
tuple(true,true) != tuple(true,true),
inference(rw,[status(thm)],[g0_2,t83114]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KLE044-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/5.38 % Computer : n008.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.39 % CPULimit : 300
% 0.10/5.39 % WCLimit : 300
% 0.10/5.39 % DateTime : Wed Sep 23 18:46:17 UTC 2026
% 0.10/5.39 % CPUTime :
% 0.10/5.39 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 62.00/14.42 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 62.00/14.42 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------