%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : KLE145-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 : 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 84.43s 12.63s
% Output : CNFRefutation 84.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 55
% Number of leaves : 23
% Syntax : Number of clauses : 230 ( 230 unt; 0 nHn; 3 RR)
% Number of literals : 230 ( 229 equ; 2 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 : 12 ( 12 usr; 4 con; 0-4 aty)
% Number of variables : 370 ( 32 sgn)
% Comments :
%------------------------------------------------------------------------------
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(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(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(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(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(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(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(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(t67818,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(t67819,plain,
multiplication(star(X1),multiplication(X1,star(X1))) = multiplication(star(X1),multiplication(star(X1),X1)),
inference(step,[status(thm)],[t67818,t77]) ).
cnf(t47099,plain,
multiplication(star(X1),multiplication(star(X1),X1)) = multiplication(star(X1),multiplication(X1,star(X1))),
inference(orient,[status(thm)],[t67819]) ).
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(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(t67822,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(t67823,plain,
multiplication(X1,multiplication(star(X1),star(X1))) = multiplication(star(X1),multiplication(X1,star(X1))),
inference(step,[status(thm)],[t67822,t71]) ).
cnf(t47313,plain,
multiplication(star(X1),multiplication(X1,star(X1))) = multiplication(X1,multiplication(star(X1),star(X1))),
inference(orient,[status(thm)],[t67823]) ).
cnf(t67824,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)],[t67824]) ).
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(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(t67301,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)],[t67301]) ).
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(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(t67362,plain,
star(X1) = addition(multiplication(X1,star(X1)),star(X1)),
inference(step,[status(thm)],[t352,t30]) ).
cnf(t67363,plain,
star(X1) = addition(star(X1),multiplication(X1,star(X1))),
inference(step,[status(thm)],[t67362,t48]) ).
cnf(t67364,plain,
star(X1) = multiplication(addition(one,X1),star(X1)),
inference(step,[status(thm)],[t67363,t234]) ).
cnf(t1731,plain,
multiplication(addition(one,X1),star(X1)) = star(X1),
inference(orient,[status(thm)],[t67364]) ).
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(t67829,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(t67830,plain,
true = leq(multiplication(star(X1),multiplication(one,star(X1))),star(X1)),
inference(step,[status(thm)],[t67829,t29]) ).
cnf(t67831,plain,
true = leq(multiplication(star(X1),star(X1)),star(X1)),
inference(step,[status(thm)],[t67830,t26]) ).
cnf(t48137,plain,
leq(multiplication(star(X1),star(X1)),star(X1)) = true,
inference(orient,[status(thm)],[t67831]) ).
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(t67832,plain,
star(X1) = addition(star(X1),multiplication(star(X1),star(X1))),
inference(step,[status(thm)],[t48149,t30]) ).
cnf(t67833,plain,
star(X1) = multiplication(addition(one,star(X1)),star(X1)),
inference(step,[status(thm)],[t67832,t234]) ).
cnf(t67834,plain,
star(X1) = multiplication(star(X1),addition(one,star(X1))),
inference(step,[status(thm)],[t67833,t269]) ).
cnf(t153,plain,
addition(one,multiplication(star(X1),X1)) = addition(one,star(X1)),
inference(cp,[status(thm)],[t150,t77]) ).
cnf(t67297,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)],[t67297]) ).
cnf(t67835,plain,
star(X1) = multiplication(star(X1),star(X1)),
inference(step,[status(thm)],[t67834,t163]) ).
cnf(t48151,plain,
multiplication(star(X1),star(X1)) = star(X1),
inference(orient,[status(thm)],[t67835]) ).
cnf(t67836,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)],[t67836]) ).
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(t67849,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)],[t67849]) ).
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(t67854,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)],[t67854]) ).
cnf(t67895,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)],[t67895]) ).
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(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(t67886,plain,
multiplication(addition(X1,multiplication(X2,zero)),zero) = multiplication(addition(X1,X2),multiplication(zero,zero)),
inference(step,[status(thm)],[t51385,t35]) ).
cnf(t67887,plain,
multiplication(addition(X1,multiplication(X2,zero)),zero) = multiplication(addition(X1,X2),zero),
inference(step,[status(thm)],[t67886,t46]) ).
cnf(t51595,plain,
multiplication(addition(X1,multiplication(X2,zero)),zero) = multiplication(addition(X1,X2),zero),
inference(orient,[status(thm)],[t67887]) ).
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(t67888,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(t67889,plain,
addition(X1,multiplication(X2,zero)) = addition(addition(X1,multiplication(X2,zero)),multiplication(addition(X1,X2),zero)),
inference(step,[status(thm)],[t67888,t25]) ).
cnf(t67890,plain,
addition(X1,multiplication(X2,zero)) = addition(X1,addition(multiplication(X2,zero),multiplication(addition(X1,X2),zero))),
inference(step,[status(thm)],[t67889,t53]) ).
cnf(t67891,plain,
addition(X1,multiplication(X2,zero)) = addition(X1,multiplication(addition(multiplication(X2,zero),addition(X1,X2)),zero)),
inference(step,[status(thm)],[t67890,t51045]) ).
cnf(t67892,plain,
addition(X1,multiplication(X2,zero)) = addition(X1,multiplication(addition(X2,addition(X1,X2)),zero)),
inference(step,[status(thm)],[t67891,t51381]) ).
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(t67893,plain,
addition(X1,multiplication(X2,zero)) = addition(X1,multiplication(addition(X2,X1),zero)),
inference(step,[status(thm)],[t67892,t201]) ).
cnf(t51769,plain,
addition(X1,multiplication(addition(X2,X1),zero)) = addition(X1,multiplication(X2,zero)),
inference(orient,[status(thm)],[t67893]) ).
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(t68051,plain,
addition(X1,addition(X2,multiplication(X2,zero))) = addition(addition(X1,X2),multiplication(addition(X2,X1),zero)),
inference(step,[status(thm)],[t51819,t53]) ).
cnf(t68052,plain,
addition(X1,multiplication(X2,addition(one,zero))) = addition(addition(X1,X2),multiplication(addition(X2,X1),zero)),
inference(step,[status(thm)],[t68051,t222]) ).
cnf(t68053,plain,
addition(X1,multiplication(X2,one)) = addition(addition(X1,X2),multiplication(addition(X2,X1),zero)),
inference(step,[status(thm)],[t68052,t28]) ).
cnf(t68054,plain,
addition(X1,X2) = addition(addition(X1,X2),multiplication(addition(X2,X1),zero)),
inference(step,[status(thm)],[t68053,t25]) ).
cnf(t68055,plain,
addition(X1,X2) = addition(X1,addition(X2,multiplication(addition(X2,X1),zero))),
inference(step,[status(thm)],[t68054,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(t68056,plain,
addition(X1,X2) = addition(X1,addition(X2,multiplication(X1,zero))),
inference(step,[status(thm)],[t68055,t52076]) ).
cnf(t65114,plain,
addition(X1,addition(X2,multiplication(X1,zero))) = addition(X1,X2),
inference(orient,[status(thm)],[t68056]) ).
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(t68068,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(t68069,plain,
multiplication(star(X1),X2) = multiplication(addition(star(X1),multiplication(X2,zero)),X2),
inference(step,[status(thm)],[t68068,t52328]) ).
cnf(t67031,plain,
multiplication(addition(star(X1),multiplication(X2,zero)),X2) = multiplication(star(X1),X2),
inference(orient,[status(thm)],[t68069]) ).
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(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(t67706,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(t67707,plain,
multiplication(strong_iteration(X1),addition(one,X2)) = addition(star(X1),multiplication(strong_iteration(X1),X2)),
inference(step,[status(thm)],[t67706,t136]) ).
cnf(t29557,plain,
addition(star(X1),multiplication(strong_iteration(X1),X2)) = multiplication(strong_iteration(X1),addition(one,X2)),
inference(orient,[status(thm)],[t67707]) ).
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(t12,axiom,
addition(multiplication(X1,strong_iteration(X1)),one) = strong_iteration(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t67291,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)],[t67291]) ).
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(t67359,plain,
strong_iteration(X1) = addition(multiplication(X1,strong_iteration(X1)),strong_iteration(X1)),
inference(step,[status(thm)],[t347,t30]) ).
cnf(t67360,plain,
strong_iteration(X1) = addition(strong_iteration(X1),multiplication(X1,strong_iteration(X1))),
inference(step,[status(thm)],[t67359,t48]) ).
cnf(t67361,plain,
strong_iteration(X1) = multiplication(addition(one,X1),strong_iteration(X1)),
inference(step,[status(thm)],[t67360,t234]) ).
cnf(t1625,plain,
multiplication(addition(one,X1),strong_iteration(X1)) = strong_iteration(X1),
inference(orient,[status(thm)],[t67361]) ).
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(t67840,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(t67841,plain,
true = leq(multiplication(star(X1),multiplication(one,strong_iteration(X1))),strong_iteration(X1)),
inference(step,[status(thm)],[t67840,t29]) ).
cnf(t67842,plain,
true = leq(multiplication(star(X1),strong_iteration(X1)),strong_iteration(X1)),
inference(step,[status(thm)],[t67841,t26]) ).
cnf(t48193,plain,
leq(multiplication(star(X1),strong_iteration(X1)),strong_iteration(X1)) = true,
inference(orient,[status(thm)],[t67842]) ).
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(t67843,plain,
strong_iteration(X1) = addition(strong_iteration(X1),multiplication(star(X1),strong_iteration(X1))),
inference(step,[status(thm)],[t48199,t30]) ).
cnf(t67844,plain,
strong_iteration(X1) = multiplication(addition(one,star(X1)),strong_iteration(X1)),
inference(step,[status(thm)],[t67843,t234]) ).
cnf(t67845,plain,
strong_iteration(X1) = multiplication(star(X1),strong_iteration(X1)),
inference(step,[status(thm)],[t67844,t163]) ).
cnf(t48202,plain,
multiplication(star(X1),strong_iteration(X1)) = strong_iteration(X1),
inference(orient,[status(thm)],[t67845]) ).
cnf(t68070,plain,
strong_iteration(X1) = multiplication(multiplication(strong_iteration(X1),addition(one,zero)),strong_iteration(X1)),
inference(step,[status(thm)],[t67032,t48202]) ).
cnf(t68071,plain,
strong_iteration(X1) = multiplication(strong_iteration(X1),multiplication(addition(one,zero),strong_iteration(X1))),
inference(step,[status(thm)],[t68070,t35]) ).
cnf(t68072,plain,
strong_iteration(X1) = multiplication(strong_iteration(X1),multiplication(one,strong_iteration(X1))),
inference(step,[status(thm)],[t68071,t28]) ).
cnf(t68073,plain,
strong_iteration(X1) = multiplication(strong_iteration(X1),strong_iteration(X1)),
inference(step,[status(thm)],[t68072,t26]) ).
cnf(t67170,plain,
multiplication(strong_iteration(X1),strong_iteration(X1)) = strong_iteration(X1),
inference(orient,[status(thm)],[t68073]) ).
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(t68077,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(t68078,plain,
true = leq(multiplication(strong_iteration(X1),multiplication(star(strong_iteration(X1)),strong_iteration(X1))),strong_iteration(X1)),
inference(step,[status(thm)],[t68077,t29]) ).
cnf(t154,plain,
addition(one,multiplication(X1,strong_iteration(X1))) = addition(one,strong_iteration(X1)),
inference(cp,[status(thm)],[t150,t62]) ).
cnf(t67299,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)],[t67299]) ).
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(t68079,plain,
true = leq(multiplication(star(strong_iteration(X1)),strong_iteration(X1)),strong_iteration(X1)),
inference(step,[status(thm)],[t68078,t60397]) ).
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(t67325,plain,
star(X1) = addition(multiplication(star(X1),X1),star(X1)),
inference(step,[status(thm)],[t341,t30]) ).
cnf(t67326,plain,
star(X1) = addition(star(X1),multiplication(star(X1),X1)),
inference(step,[status(thm)],[t67325,t48]) ).
cnf(t67327,plain,
star(X1) = multiplication(star(X1),addition(one,X1)),
inference(step,[status(thm)],[t67326,t222]) ).
cnf(t660,plain,
multiplication(star(X1),addition(one,X1)) = star(X1),
inference(orient,[status(thm)],[t67327]) ).
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(t68080,plain,
true = leq(star(strong_iteration(X1)),strong_iteration(X1)),
inference(step,[status(thm)],[t68079,t947]) ).
cnf(t67215,plain,
leq(star(strong_iteration(X1)),strong_iteration(X1)) = true,
inference(orient,[status(thm)],[t68080]) ).
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(t68081,plain,
strong_iteration(X1) = addition(strong_iteration(X1),star(strong_iteration(X1))),
inference(step,[status(thm)],[t67218,t30]) ).
cnf(t673,plain,
multiplication(addition(one,star(X1)),addition(one,X1)) = addition(addition(one,X1),star(X1)),
inference(cp,[status(thm)],[t234,t660]) ).
cnf(t67328,plain,
multiplication(star(X1),addition(one,X1)) = addition(addition(one,X1),star(X1)),
inference(step,[status(thm)],[t673,t163]) ).
cnf(t67329,plain,
star(X1) = addition(addition(one,X1),star(X1)),
inference(step,[status(thm)],[t67328,t660]) ).
cnf(t67330,plain,
star(X1) = addition(one,addition(X1,star(X1))),
inference(step,[status(thm)],[t67329,t53]) ).
cnf(t358,plain,
true = leq(X1,addition(addition(X2,X1),X3)),
inference(cp,[status(thm)],[t356,t48]) ).
cnf(t67306,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)],[t67306]) ).
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(t67313,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)],[t67313]) ).
cnf(t67331,plain,
star(X1) = addition(X1,star(X1)),
inference(step,[status(thm)],[t67330,t589]) ).
cnf(t688,plain,
addition(X1,star(X1)) = star(X1),
inference(orient,[status(thm)],[t67331]) ).
cnf(t68082,plain,
strong_iteration(X1) = star(strong_iteration(X1)),
inference(step,[status(thm)],[t68081,t688]) ).
cnf(t67223,plain,
star(strong_iteration(X1)) = strong_iteration(X1),
inference(orient,[status(thm)],[t68082]) ).
cnf(goal_0,negated_conjecture,
star(strong_iteration(sK1_goals_X0)) != strong_iteration(sK1_goals_X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
strong_iteration(sK1_goals_X0) != strong_iteration(sK1_goals_X0),
inference(rw,[status(thm)],[goal_0,t67223]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KLE145-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n010.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 : Wed Sep 23 19:04:42 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 84.43/12.63 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 84.43/12.63 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------