%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : KLE012+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n018.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:21 PM UTC 2026
% Result : Theorem 47.96s 6.43s
% Output : Proof 47.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 104
% Number of leaves : 17
% Syntax : Number of formulae : 608 ( 582 unt; 0 def)
% Number of atoms : 671 ( 618 equ)
% Maximal formula atoms : 8 ( 1 avg)
% Number of connectives : 105 ( 42 ~; 36 |; 20 &)
% ( 4 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 6 con; 0-4 aty)
% Number of variables : 493 ( 35 sgn 81 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [A,B,C] : multiplication(A,multiplication(B,C)) = multiplication(multiplication(A,B),C),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiplicative_associativity) ).
fof(f4_nnf,plain,
! [A,B,C] : multiplication(A,multiplication(B,C)) = multiplication(multiplication(A,B),C),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [A,B,C] : multiplication(A,multiplication(B,C)) = multiplication(multiplication(A,B),C),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t130,plain,
multiplication(multiplication(X1,X2),X3) = multiplication(X1,multiplication(X2,X3)),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t585,plain,
multiplication(multiplication(X1,X2),X3) = multiplication(X1,multiplication(X2,X3)),
inference(orient,[status(thm)],[t130]) ).
fof(f7,axiom,
! [A,B,C] : multiplication(A,addition(B,C)) = addition(multiplication(A,B),multiplication(A,C)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',right_distributivity) ).
fof(f7_nnf,plain,
! [A,B,C] : multiplication(A,addition(B,C)) = addition(multiplication(A,B),multiplication(A,C)),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [A,B,C] : multiplication(A,addition(B,C)) = addition(multiplication(A,B),multiplication(A,C)),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t159,plain,
addition(multiplication(X1,X2),multiplication(X1,X3)) = multiplication(X1,addition(X2,X3)),
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t343,plain,
addition(multiplication(X1,X2),multiplication(X1,X3)) = multiplication(X1,addition(X2,X3)),
inference(orient,[status(thm)],[t159]) ).
fof(f12,axiom,
! [X0] :
( test(X0)
<=> ? [X1] : complement(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',test_1) ).
fof(f12_nnf,plain,
! [X0] :
( ( ! [X1] : ~ complement(X1,X0)
| test(X0) )
& ( ? [X1] : complement(X1,X0)
| ~ test(X0) ) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [X0,X1] :
( ( ~ complement(X1,X0)
| test(X0) )
& ( complement(sk0(X0),X0)
| ~ test(X0) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f12_nnf]) ).
cnf(c13,plain,
( complement(sk0(X0),X0)
| ~ test(X0) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(hi13,axiom,
ifeq(test(X0),true,complement(sk0(X0),X0),true) = true,
inference(equality_encoding,[status(esa)],[c13]) ).
fof(f16,conjecture,
! [X0,X1] :
( ( test(X0)
& test(X1) )
=> multiplication(X0,X1) = multiplication(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f16_neg,negated_conjecture,
~ ! [X0,X1] :
( ( test(X0)
& test(X1) )
=> multiplication(X0,X1) = multiplication(X1,X0) ),
inference(negated_conjecture,[status(cth)],[f16]) ).
fof(f16_nnf,plain,
? [X0,X1] :
( multiplication(X0,X1) != multiplication(X1,X0)
& test(X0)
& test(X1) ),
inference(nnf_transformation,[status(thm)],[f16_neg]) ).
fof(f16_sk,plain,
( multiplication(sk1,sk2) != multiplication(sk2,sk1)
& test(sk1)
& test(sk2) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk1,sk2])],[f16_nnf]) ).
cnf(c22,plain,
test(sk2),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(hi22,negated_conjecture,
test(sk2) = true,
inference(equality_encoding,[status(esa)],[c22]) ).
cnf(h0,plain,
complement(sk0(sk2),sk2) = true,
inference(hyper_resolution,[status(thm)],[hi13,hi22]) ).
fof(f13,axiom,
! [X0,X1] :
( complement(X1,X0)
<=> ( addition(X0,X1) = one
& multiplication(X1,X0) = zero
& multiplication(X0,X1) = zero ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',test_2) ).
fof(f13_nnf,plain,
! [X0,X1] :
( ( addition(X0,X1) != one
| multiplication(X1,X0) != zero
| multiplication(X0,X1) != zero
| complement(X1,X0) )
& ( ( addition(X0,X1) = one
& multiplication(X1,X0) = zero
& multiplication(X0,X1) = zero )
| ~ complement(X1,X0) ) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [X1,X0] :
( ( addition(X0,X1) != one
| multiplication(X1,X0) != zero
| multiplication(X0,X1) != zero
| complement(X1,X0) )
& ( ( addition(X0,X1) = one
& multiplication(X1,X0) = zero
& multiplication(X0,X1) = zero )
| ~ complement(X1,X0) ) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c15,plain,
( multiplication(X0,X1) = zero
| ~ complement(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(hi15,axiom,
ifeq(complement(X0,X1),true,multiplication(X1,X0),zero) = zero,
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(t20,plain,
multiplication(sk2,sk0(sk2)) = zero,
inference(hyper_resolution,[status(thm)],[hi15,h0]) ).
cnf(t524,plain,
multiplication(sk2,sk0(sk2)) = zero,
inference(orient,[status(thm)],[t20]) ).
cnf(t526,plain,
multiplication(sk2,addition(X1,sk0(sk2))) = addition(multiplication(sk2,X1),zero),
inference(cp,[status(thm)],[t343,t524]) ).
fof(f2,axiom,
! [A] : addition(A,zero) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_identity) ).
fof(f2_nnf,plain,
! [A] : addition(A,zero) = A,
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A] : addition(A,zero) = A,
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
addition(X0,zero) = X0,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t3,plain,
addition(X1,zero) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t259,plain,
addition(X1,zero) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t54048,plain,
multiplication(sk2,addition(X1,sk0(sk2))) = multiplication(sk2,X1),
inference(step,[status(thm)],[t526,t259]) ).
cnf(t1364,plain,
multiplication(sk2,addition(X1,sk0(sk2))) = multiplication(sk2,X1),
inference(orient,[status(thm)],[t54048]) ).
fof(f0,axiom,
! [A,B] : addition(A,B) = addition(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_commutativity) ).
fof(f0_nnf,plain,
! [A,B] : addition(A,B) = addition(B,A),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,B] : addition(A,B) = addition(B,A),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
addition(X0,X1) = addition(X1,X0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t21,plain,
addition(X1,X2) = addition(X2,X1),
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t273,plain,
addition(X1,X2) = addition(X2,X1),
inference(orient,[status(thm)],[t21]) ).
cnf(t1366,plain,
multiplication(sk2,X1) = multiplication(sk2,addition(sk0(sk2),X1)),
inference(cp,[status(thm)],[t1364,t273]) ).
cnf(t1655,plain,
multiplication(sk2,addition(sk0(sk2),X1)) = multiplication(sk2,X1),
inference(orient,[status(thm)],[t1366]) ).
cnf(t1658,plain,
multiplication(sk2,multiplication(addition(sk0(sk2),X1),X2)) = multiplication(multiplication(sk2,X1),X2),
inference(cp,[status(thm)],[t585,t1655]) ).
cnf(t55069,plain,
multiplication(sk2,multiplication(addition(sk0(sk2),X1),X2)) = multiplication(sk2,multiplication(X1,X2)),
inference(step,[status(thm)],[t1658,t585]) ).
cnf(t51052,plain,
multiplication(sk2,multiplication(addition(sk0(sk2),X1),X2)) = multiplication(sk2,multiplication(X1,X2)),
inference(orient,[status(thm)],[t55069]) ).
fof(f8,axiom,
! [A,B,C] : multiplication(addition(A,B),C) = addition(multiplication(A,C),multiplication(B,C)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_distributivity) ).
fof(f8_nnf,plain,
! [A,B,C] : multiplication(addition(A,B),C) = addition(multiplication(A,C),multiplication(B,C)),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [A,B,C] : multiplication(addition(A,B),C) = addition(multiplication(A,C),multiplication(B,C)),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t160,plain,
addition(multiplication(X1,X2),multiplication(X3,X2)) = multiplication(addition(X1,X3),X2),
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t337,plain,
addition(multiplication(X1,X2),multiplication(X3,X2)) = multiplication(addition(X1,X3),X2),
inference(orient,[status(thm)],[t160]) ).
cnf(t601,plain,
multiplication(addition(multiplication(X1,X2),X3),Y3) = addition(multiplication(X1,multiplication(X2,Y3)),multiplication(X3,Y3)),
inference(cp,[status(thm)],[t337,t585]) ).
cnf(t45735,plain,
addition(multiplication(X1,multiplication(X2,X3)),multiplication(Y3,X3)) = multiplication(addition(multiplication(X1,X2),Y3),X3),
inference(orient,[status(thm)],[t601]) ).
fof(f14,axiom,
! [X0,X1] :
( test(X0)
=> ( c(X0) = X1
<=> complement(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',test_3) ).
fof(f14_nnf,plain,
! [X0,X1] :
( ( ( ~ complement(X0,X1)
| c(X0) = X1 )
& ( complement(X0,X1)
| c(X0) != X1 ) )
| ~ test(X0) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [X0,X1] :
( ( ( ~ complement(X0,X1)
| c(X0) = X1 )
& ( complement(X0,X1)
| c(X0) != X1 ) )
| ~ test(X0) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c19,plain,
( complement(X0,X1)
| c(X0) != X1
| ~ test(X0) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(hi19,axiom,
ifeq(test(X0),true,ifeq(c(X0),X1,complement(X0,X1),true),true) = true,
inference(equality_encoding,[status(esa)],[c19]) ).
cnf(c23,plain,
test(sk1),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(hi23,negated_conjecture,
test(sk1) = true,
inference(equality_encoding,[status(esa)],[c23]) ).
cnf(hi28,axiom,
or(X0,false) = X0,
introduced(definition) ).
cnf(h15,plain,
complement(sk1,or(c(sk1),false)) = true,
inference(hyper_resolution,[status(thm)],[hi19,hi23,hi28]) ).
cnf(t73,plain,
multiplication(or(c(sk1),false),sk1) = zero,
inference(hyper_resolution,[status(thm)],[hi15,h15]) ).
cnf(t9,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t256,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t9]) ).
cnf(t53961,plain,
multiplication(c(sk1),sk1) = zero,
inference(step,[status(thm)],[t73,t256]) ).
cnf(t468,plain,
multiplication(c(sk1),sk1) = zero,
inference(orient,[status(thm)],[t53961]) ).
cnf(t472,plain,
multiplication(addition(X1,c(sk1)),sk1) = addition(multiplication(X1,sk1),zero),
inference(cp,[status(thm)],[t337,t468]) ).
cnf(t54029,plain,
multiplication(addition(X1,c(sk1)),sk1) = multiplication(X1,sk1),
inference(step,[status(thm)],[t472,t259]) ).
cnf(t1085,plain,
multiplication(addition(X1,c(sk1)),sk1) = multiplication(X1,sk1),
inference(orient,[status(thm)],[t54029]) ).
cnf(c17,plain,
( addition(X0,X1) = one
| ~ complement(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(hi17,axiom,
ifeq(complement(X0,X1),true,addition(X1,X0),one) = one,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(t53,plain,
addition(or(c(sk1),false),sk1) = one,
inference(hyper_resolution,[status(thm)],[hi17,h15]) ).
cnf(t53895,plain,
addition(sk1,or(c(sk1),false)) = one,
inference(step,[status(thm)],[t53,t273]) ).
cnf(t53896,plain,
addition(sk1,c(sk1)) = one,
inference(step,[status(thm)],[t53895,t256]) ).
cnf(t289,plain,
addition(sk1,c(sk1)) = one,
inference(orient,[status(thm)],[t53896]) ).
cnf(t1086,plain,
multiplication(sk1,sk1) = multiplication(one,sk1),
inference(cp,[status(thm)],[t1085,t289]) ).
fof(f6,axiom,
! [A] : multiplication(one,A) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiplicative_left_identity) ).
fof(f6_nnf,plain,
! [A] : multiplication(one,A) = A,
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [A] : multiplication(one,A) = A,
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
multiplication(one,X0) = X0,
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t7,plain,
multiplication(one,X1) = X1,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t261,plain,
multiplication(one,X1) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t54030,plain,
multiplication(sk1,sk1) = sk1,
inference(step,[status(thm)],[t1086,t261]) ).
cnf(t1100,plain,
multiplication(sk1,sk1) = sk1,
inference(orient,[status(thm)],[t54030]) ).
cnf(t1103,plain,
multiplication(sk1,multiplication(sk1,X1)) = multiplication(sk1,X1),
inference(cp,[status(thm)],[t585,t1100]) ).
cnf(t1112,plain,
multiplication(sk1,multiplication(sk1,X1)) = multiplication(sk1,X1),
inference(orient,[status(thm)],[t1103]) ).
cnf(t1118,plain,
multiplication(sk1,addition(X1,multiplication(sk1,X2))) = addition(multiplication(sk1,X1),multiplication(sk1,X2)),
inference(cp,[status(thm)],[t343,t1112]) ).
cnf(t54239,plain,
multiplication(sk1,addition(X1,multiplication(sk1,X2))) = multiplication(sk1,addition(X1,X2)),
inference(step,[status(thm)],[t1118,t343]) ).
cnf(t4515,plain,
multiplication(sk1,addition(X1,multiplication(sk1,X2))) = multiplication(sk1,addition(X1,X2)),
inference(orient,[status(thm)],[t54239]) ).
fof(f5,axiom,
! [A] : multiplication(A,one) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiplicative_right_identity) ).
fof(f5_nnf,plain,
! [A] : multiplication(A,one) = A,
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [A] : multiplication(A,one) = A,
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
multiplication(X0,one) = X0,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t5,plain,
multiplication(X1,one) = X1,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t260,plain,
multiplication(X1,one) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t4531,plain,
multiplication(sk1,addition(X1,one)) = multiplication(sk1,addition(X1,sk1)),
inference(cp,[status(thm)],[t4515,t260]) ).
cnf(t4545,plain,
multiplication(sk1,addition(X1,one)) = multiplication(sk1,addition(X1,sk1)),
inference(orient,[status(thm)],[t4531]) ).
fof(f1,axiom,
! [C,B,A] : addition(A,addition(B,C)) = addition(addition(A,B),C),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_associativity) ).
fof(f1_nnf,plain,
! [C,B,A] : addition(A,addition(B,C)) = addition(addition(A,B),C),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A,B,C] : addition(A,addition(B,C)) = addition(addition(A,B),C),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t123,plain,
addition(addition(X1,X2),X3) = addition(X1,addition(X2,X3)),
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t276,plain,
addition(addition(X1,X2),X3) = addition(X1,addition(X2,X3)),
inference(orient,[status(thm)],[t123]) ).
fof(f3,axiom,
! [A] : addition(A,A) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_idempotence) ).
fof(f3_nnf,plain,
! [A] : addition(A,A) = A,
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A] : addition(A,A) = A,
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
addition(X0,X0) = X0,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t2,plain,
addition(X1,X1) = X1,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t258,plain,
addition(X1,X1) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t279,plain,
addition(X1,addition(X1,X2)) = addition(X1,X2),
inference(cp,[status(thm)],[t276,t258]) ).
cnf(t655,plain,
addition(X1,addition(X1,X2)) = addition(X1,X2),
inference(orient,[status(thm)],[t279]) ).
cnf(h16,plain,
complement(sk2,or(c(sk2),false)) = true,
inference(hyper_resolution,[status(thm)],[hi19,hi22,hi28]) ).
cnf(t54,plain,
addition(or(c(sk2),false),sk2) = one,
inference(hyper_resolution,[status(thm)],[hi17,h16]) ).
cnf(t53899,plain,
addition(sk2,or(c(sk2),false)) = one,
inference(step,[status(thm)],[t54,t273]) ).
cnf(t53900,plain,
addition(sk2,c(sk2)) = one,
inference(step,[status(thm)],[t53899,t256]) ).
cnf(t295,plain,
addition(sk2,c(sk2)) = one,
inference(orient,[status(thm)],[t53900]) ).
cnf(t657,plain,
addition(sk2,c(sk2)) = addition(sk2,one),
inference(cp,[status(thm)],[t655,t295]) ).
cnf(t54000,plain,
one = addition(sk2,one),
inference(step,[status(thm)],[t657,t295]) ).
cnf(t669,plain,
addition(sk2,one) = one,
inference(orient,[status(thm)],[t54000]) ).
cnf(t4546,plain,
multiplication(sk1,addition(sk2,sk1)) = multiplication(sk1,one),
inference(cp,[status(thm)],[t4545,t669]) ).
cnf(t54240,plain,
multiplication(sk1,addition(sk2,sk1)) = sk1,
inference(step,[status(thm)],[t4546,t260]) ).
cnf(t4561,plain,
multiplication(sk1,addition(sk2,sk1)) = sk1,
inference(orient,[status(thm)],[t54240]) ).
cnf(t4564,plain,
multiplication(sk1,multiplication(addition(sk2,sk1),X1)) = multiplication(sk1,X1),
inference(cp,[status(thm)],[t585,t4561]) ).
cnf(t4575,plain,
multiplication(sk1,multiplication(addition(sk2,sk1),X1)) = multiplication(sk1,X1),
inference(orient,[status(thm)],[t4564]) ).
cnf(h4,plain,
complement(sk0(sk1),sk1) = true,
inference(hyper_resolution,[status(thm)],[hi13,hi23]) ).
cnf(t19,plain,
multiplication(sk1,sk0(sk1)) = zero,
inference(hyper_resolution,[status(thm)],[hi15,h4]) ).
cnf(t510,plain,
multiplication(sk1,sk0(sk1)) = zero,
inference(orient,[status(thm)],[t19]) ).
cnf(t514,plain,
multiplication(addition(X1,sk1),sk0(sk1)) = addition(multiplication(X1,sk0(sk1)),zero),
inference(cp,[status(thm)],[t337,t510]) ).
cnf(t54119,plain,
multiplication(addition(X1,sk1),sk0(sk1)) = multiplication(X1,sk0(sk1)),
inference(step,[status(thm)],[t514,t259]) ).
cnf(t2679,plain,
multiplication(addition(X1,sk1),sk0(sk1)) = multiplication(X1,sk0(sk1)),
inference(orient,[status(thm)],[t54119]) ).
cnf(t4576,plain,
multiplication(sk1,sk0(sk1)) = multiplication(sk1,multiplication(sk2,sk0(sk1))),
inference(cp,[status(thm)],[t4575,t2679]) ).
cnf(t54241,plain,
zero = multiplication(sk1,multiplication(sk2,sk0(sk1))),
inference(step,[status(thm)],[t4576,t510]) ).
cnf(t4589,plain,
multiplication(sk1,multiplication(sk2,sk0(sk1))) = zero,
inference(orient,[status(thm)],[t54241]) ).
cnf(t4595,plain,
multiplication(sk1,addition(multiplication(sk2,sk0(sk1)),X1)) = addition(zero,multiplication(sk1,X1)),
inference(cp,[status(thm)],[t343,t4589]) ).
cnf(t274,plain,
addition(zero,X1) = X1,
inference(cp,[status(thm)],[t273,t259]) ).
cnf(t630,plain,
addition(zero,X1) = X1,
inference(orient,[status(thm)],[t274]) ).
cnf(t54368,plain,
multiplication(sk1,addition(multiplication(sk2,sk0(sk1)),X1)) = multiplication(sk1,X1),
inference(step,[status(thm)],[t4595,t630]) ).
cnf(t6312,plain,
multiplication(sk1,addition(multiplication(sk2,sk0(sk1)),X1)) = multiplication(sk1,X1),
inference(orient,[status(thm)],[t54368]) ).
cnf(t6314,plain,
multiplication(sk1,multiplication(sk2,X1)) = multiplication(sk1,multiplication(sk2,addition(sk0(sk1),X1))),
inference(cp,[status(thm)],[t6312,t343]) ).
cnf(t52525,plain,
multiplication(sk1,multiplication(sk2,addition(sk0(sk1),X1))) = multiplication(sk1,multiplication(sk2,X1)),
inference(orient,[status(thm)],[t6314]) ).
cnf(t345,plain,
multiplication(X1,addition(one,X2)) = addition(X1,multiplication(X1,X2)),
inference(cp,[status(thm)],[t343,t260]) ).
cnf(t948,plain,
addition(X1,multiplication(X1,X2)) = multiplication(X1,addition(one,X2)),
inference(orient,[status(thm)],[t345]) ).
cnf(t2682,plain,
multiplication(addition(X1,sk1),addition(one,sk0(sk1))) = addition(addition(X1,sk1),multiplication(X1,sk0(sk1))),
inference(cp,[status(thm)],[t948,t2679]) ).
fof(f11,axiom,
! [A,B] :
( leq(A,B)
<=> addition(A,B) = B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',order) ).
fof(f11_nnf,plain,
! [A,B] :
( ( addition(A,B) != B
| leq(A,B) )
& ( addition(A,B) = B
| ~ leq(A,B) ) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [A,B] :
( ( addition(A,B) != B
| leq(A,B) )
& ( addition(A,B) = B
| ~ leq(A,B) ) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
( addition(X0,X1) = X1
| ~ leq(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t128,plain,
ifeq(leq(X1,X2),true,addition(X1,X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t264,plain,
ifeq(leq(X1,X2),true,addition(X1,X2),X2) = X2,
inference(orient,[status(thm)],[t128]) ).
cnf(c12,plain,
( addition(X0,X1) != X1
| leq(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t124,plain,
ifeq(addition(X1,X2),X2,leq(X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t379,plain,
ifeq(addition(X1,X2),X2,leq(X1,X2),true) = true,
inference(orient,[status(thm)],[t124]) ).
cnf(t667,plain,
true = ifeq(addition(X1,X2),addition(X1,X2),leq(X1,addition(X1,X2)),true),
inference(cp,[status(thm)],[t379,t655]) ).
cnf(t24,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t262,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t24]) ).
cnf(t54004,plain,
true = leq(X1,addition(X1,X2)),
inference(step,[status(thm)],[t667,t262]) ).
cnf(t683,plain,
leq(X1,addition(X1,X2)) = true,
inference(orient,[status(thm)],[t54004]) ).
cnf(t689,plain,
true = leq(X1,addition(X2,X1)),
inference(cp,[status(thm)],[t683,t273]) ).
cnf(t696,plain,
leq(X1,addition(X2,X1)) = true,
inference(orient,[status(thm)],[t689]) ).
cnf(t13,plain,
addition(sk1,sk0(sk1)) = one,
inference(hyper_resolution,[status(thm)],[hi17,h4]) ).
cnf(t307,plain,
addition(sk1,sk0(sk1)) = one,
inference(orient,[status(thm)],[t13]) ).
cnf(t700,plain,
true = leq(sk0(sk1),one),
inference(cp,[status(thm)],[t696,t307]) ).
cnf(t709,plain,
leq(sk0(sk1),one) = true,
inference(orient,[status(thm)],[t700]) ).
cnf(t710,plain,
one = ifeq(true,true,addition(sk0(sk1),one),one),
inference(cp,[status(thm)],[t264,t709]) ).
cnf(t54007,plain,
one = addition(sk0(sk1),one),
inference(step,[status(thm)],[t710,t262]) ).
cnf(t54008,plain,
one = addition(one,sk0(sk1)),
inference(step,[status(thm)],[t54007,t273]) ).
cnf(t718,plain,
addition(one,sk0(sk1)) = one,
inference(orient,[status(thm)],[t54008]) ).
cnf(t54312,plain,
multiplication(addition(X1,sk1),one) = addition(addition(X1,sk1),multiplication(X1,sk0(sk1))),
inference(step,[status(thm)],[t2682,t718]) ).
cnf(t54313,plain,
addition(X1,sk1) = addition(addition(X1,sk1),multiplication(X1,sk0(sk1))),
inference(step,[status(thm)],[t54312,t260]) ).
cnf(t54314,plain,
addition(X1,sk1) = addition(X1,addition(sk1,multiplication(X1,sk0(sk1)))),
inference(step,[status(thm)],[t54313,t276]) ).
cnf(t5658,plain,
addition(X1,addition(sk1,multiplication(X1,sk0(sk1)))) = addition(X1,sk1),
inference(orient,[status(thm)],[t54314]) ).
cnf(t52528,plain,
multiplication(sk1,multiplication(sk2,addition(sk1,multiplication(sk0(sk1),sk0(sk1))))) = multiplication(sk1,multiplication(sk2,addition(sk0(sk1),sk1))),
inference(cp,[status(thm)],[t52525,t5658]) ).
cnf(t2681,plain,
multiplication(X1,sk0(sk1)) = multiplication(addition(sk1,X1),sk0(sk1)),
inference(cp,[status(thm)],[t2679,t273]) ).
cnf(t3046,plain,
multiplication(addition(sk1,X1),sk0(sk1)) = multiplication(X1,sk0(sk1)),
inference(orient,[status(thm)],[t2681]) ).
cnf(t3053,plain,
multiplication(sk0(sk1),sk0(sk1)) = multiplication(one,sk0(sk1)),
inference(cp,[status(thm)],[t3046,t307]) ).
cnf(t54168,plain,
multiplication(sk0(sk1),sk0(sk1)) = sk0(sk1),
inference(step,[status(thm)],[t3053,t261]) ).
cnf(t3153,plain,
multiplication(sk0(sk1),sk0(sk1)) = sk0(sk1),
inference(orient,[status(thm)],[t54168]) ).
cnf(t55076,plain,
multiplication(sk1,multiplication(sk2,addition(sk1,sk0(sk1)))) = multiplication(sk1,multiplication(sk2,addition(sk0(sk1),sk1))),
inference(step,[status(thm)],[t52528,t3153]) ).
cnf(t55077,plain,
multiplication(sk1,multiplication(sk2,one)) = multiplication(sk1,multiplication(sk2,addition(sk0(sk1),sk1))),
inference(step,[status(thm)],[t55076,t307]) ).
cnf(t55078,plain,
multiplication(sk1,sk2) = multiplication(sk1,multiplication(sk2,addition(sk0(sk1),sk1))),
inference(step,[status(thm)],[t55077,t260]) ).
cnf(t55079,plain,
multiplication(sk1,sk2) = multiplication(sk1,multiplication(sk2,sk1)),
inference(step,[status(thm)],[t55078,t52525]) ).
cnf(t52630,plain,
multiplication(sk1,multiplication(sk2,sk1)) = multiplication(sk1,sk2),
inference(orient,[status(thm)],[t55079]) ).
cnf(t52644,plain,
multiplication(addition(multiplication(sk1,sk2),X1),sk1) = addition(multiplication(sk1,sk2),multiplication(X1,sk1)),
inference(cp,[status(thm)],[t45735,t52630]) ).
cnf(t53624,plain,
addition(multiplication(sk1,sk2),multiplication(X1,sk1)) = multiplication(addition(multiplication(sk1,sk2),X1),sk1),
inference(orient,[status(thm)],[t52644]) ).
cnf(t528,plain,
multiplication(addition(X1,sk2),sk0(sk2)) = addition(multiplication(X1,sk0(sk2)),zero),
inference(cp,[status(thm)],[t337,t524]) ).
cnf(t54121,plain,
multiplication(addition(X1,sk2),sk0(sk2)) = multiplication(X1,sk0(sk2)),
inference(step,[status(thm)],[t528,t259]) ).
cnf(t2707,plain,
multiplication(addition(X1,sk2),sk0(sk2)) = multiplication(X1,sk0(sk2)),
inference(orient,[status(thm)],[t54121]) ).
cnf(t2709,plain,
multiplication(X1,sk0(sk2)) = multiplication(addition(sk2,X1),sk0(sk2)),
inference(cp,[status(thm)],[t2707,t273]) ).
cnf(t3291,plain,
multiplication(addition(sk2,X1),sk0(sk2)) = multiplication(X1,sk0(sk2)),
inference(orient,[status(thm)],[t2709]) ).
cnf(t703,plain,
true = leq(X1,addition(X2,addition(X3,X1))),
inference(cp,[status(thm)],[t696,t276]) ).
cnf(t1785,plain,
leq(X1,addition(X2,addition(X3,X1))) = true,
inference(orient,[status(thm)],[t703]) ).
cnf(t1795,plain,
true = leq(X1,addition(addition(X2,X1),X3)),
inference(cp,[status(thm)],[t1785,t273]) ).
cnf(t54104,plain,
true = leq(X1,addition(X2,addition(X1,X3))),
inference(step,[status(thm)],[t1795,t276]) ).
cnf(t2469,plain,
leq(X1,addition(X2,addition(X1,X3))) = true,
inference(orient,[status(thm)],[t54104]) ).
cnf(t698,plain,
true = leq(multiplication(X1,X2),multiplication(X1,addition(X3,X2))),
inference(cp,[status(thm)],[t696,t343]) ).
cnf(t7887,plain,
leq(multiplication(X1,X2),multiplication(X1,addition(X3,X2))) = true,
inference(orient,[status(thm)],[t698]) ).
cnf(t697,plain,
true = leq(multiplication(X1,X2),multiplication(addition(X3,X1),X2)),
inference(cp,[status(thm)],[t696,t337]) ).
cnf(t7591,plain,
leq(multiplication(X1,X2),multiplication(addition(X3,X1),X2)) = true,
inference(orient,[status(thm)],[t697]) ).
cnf(t722,plain,
addition(one,addition(sk0(sk1),X1)) = addition(one,X1),
inference(cp,[status(thm)],[t276,t718]) ).
cnf(t1421,plain,
addition(one,addition(sk0(sk1),X1)) = addition(one,X1),
inference(orient,[status(thm)],[t722]) ).
cnf(t684,plain,
true = leq(multiplication(X1,X2),multiplication(addition(X1,X3),X2)),
inference(cp,[status(thm)],[t683,t337]) ).
cnf(t7000,plain,
leq(multiplication(X1,X2),multiplication(addition(X1,X3),X2)) = true,
inference(orient,[status(thm)],[t684]) ).
cnf(t7105,plain,
true = leq(multiplication(sk2,X1),multiplication(one,X1)),
inference(cp,[status(thm)],[t7000,t669]) ).
cnf(t54372,plain,
true = leq(multiplication(sk2,X1),X1),
inference(step,[status(thm)],[t7105,t261]) ).
cnf(t7129,plain,
leq(multiplication(sk2,X1),X1) = true,
inference(orient,[status(thm)],[t54372]) ).
cnf(t7140,plain,
true = leq(multiplication(sk2,X1),addition(X1,sk0(sk2))),
inference(cp,[status(thm)],[t7129,t1364]) ).
cnf(t7209,plain,
leq(multiplication(sk2,X1),addition(X1,sk0(sk2))) = true,
inference(orient,[status(thm)],[t7140]) ).
cnf(t7227,plain,
addition(X1,sk0(sk2)) = ifeq(true,true,addition(multiplication(sk2,X1),addition(X1,sk0(sk2))),addition(X1,sk0(sk2))),
inference(cp,[status(thm)],[t264,t7209]) ).
cnf(t54442,plain,
addition(X1,sk0(sk2)) = addition(multiplication(sk2,X1),addition(X1,sk0(sk2))),
inference(step,[status(thm)],[t7227,t262]) ).
cnf(t281,plain,
addition(X1,addition(X2,X3)) = addition(addition(X2,X1),X3),
inference(cp,[status(thm)],[t276,t273]) ).
cnf(t54132,plain,
addition(X1,addition(X2,X3)) = addition(X2,addition(X1,X3)),
inference(step,[status(thm)],[t281,t276]) ).
cnf(t2887,plain,
addition(X1,addition(X2,X3)) = addition(X2,addition(X1,X3)),
inference(orient,[status(thm)],[t54132]) ).
cnf(t54443,plain,
addition(X1,sk0(sk2)) = addition(X1,addition(multiplication(sk2,X1),sk0(sk2))),
inference(step,[status(thm)],[t54442,t2887]) ).
cnf(t54444,plain,
addition(X1,sk0(sk2)) = addition(X1,addition(sk0(sk2),multiplication(sk2,X1))),
inference(step,[status(thm)],[t54443,t273]) ).
cnf(t15928,plain,
addition(X1,addition(sk0(sk2),multiplication(sk2,X1))) = addition(X1,sk0(sk2)),
inference(orient,[status(thm)],[t54444]) ).
cnf(t16038,plain,
addition(one,addition(sk0(sk2),multiplication(sk2,sk0(sk1)))) = addition(one,addition(sk0(sk1),sk0(sk2))),
inference(cp,[status(thm)],[t1421,t15928]) ).
cnf(t14,plain,
addition(sk2,sk0(sk2)) = one,
inference(hyper_resolution,[status(thm)],[hi17,h0]) ).
cnf(t310,plain,
addition(sk2,sk0(sk2)) = one,
inference(orient,[status(thm)],[t14]) ).
cnf(t699,plain,
true = leq(sk0(sk2),one),
inference(cp,[status(thm)],[t696,t310]) ).
cnf(t706,plain,
leq(sk0(sk2),one) = true,
inference(orient,[status(thm)],[t699]) ).
cnf(t707,plain,
one = ifeq(true,true,addition(sk0(sk2),one),one),
inference(cp,[status(thm)],[t264,t706]) ).
cnf(t54005,plain,
one = addition(sk0(sk2),one),
inference(step,[status(thm)],[t707,t262]) ).
cnf(t54006,plain,
one = addition(one,sk0(sk2)),
inference(step,[status(thm)],[t54005,t273]) ).
cnf(t712,plain,
addition(one,sk0(sk2)) = one,
inference(orient,[status(thm)],[t54006]) ).
cnf(t716,plain,
addition(one,addition(sk0(sk2),X1)) = addition(one,X1),
inference(cp,[status(thm)],[t276,t712]) ).
cnf(t1406,plain,
addition(one,addition(sk0(sk2),X1)) = addition(one,X1),
inference(orient,[status(thm)],[t716]) ).
cnf(t54445,plain,
addition(one,multiplication(sk2,sk0(sk1))) = addition(one,addition(sk0(sk1),sk0(sk2))),
inference(step,[status(thm)],[t16038,t1406]) ).
cnf(t54446,plain,
addition(one,multiplication(sk2,sk0(sk1))) = addition(one,sk0(sk2)),
inference(step,[status(thm)],[t54445,t1421]) ).
cnf(t54447,plain,
addition(one,multiplication(sk2,sk0(sk1))) = one,
inference(step,[status(thm)],[t54446,t712]) ).
cnf(t16067,plain,
addition(one,multiplication(sk2,sk0(sk1))) = one,
inference(orient,[status(thm)],[t54447]) ).
cnf(t16106,plain,
true = leq(multiplication(multiplication(sk2,sk0(sk1)),X1),multiplication(one,X1)),
inference(cp,[status(thm)],[t7591,t16067]) ).
cnf(t54456,plain,
true = leq(multiplication(sk2,multiplication(sk0(sk1),X1)),multiplication(one,X1)),
inference(step,[status(thm)],[t16106,t585]) ).
cnf(t54457,plain,
true = leq(multiplication(sk2,multiplication(sk0(sk1),X1)),X1),
inference(step,[status(thm)],[t54456,t261]) ).
cnf(t16225,plain,
leq(multiplication(sk2,multiplication(sk0(sk1),X1)),X1) = true,
inference(orient,[status(thm)],[t54457]) ).
cnf(t16234,plain,
X1 = ifeq(true,true,addition(multiplication(sk2,multiplication(sk0(sk1),X1)),X1),X1),
inference(cp,[status(thm)],[t264,t16225]) ).
cnf(t54458,plain,
X1 = addition(multiplication(sk2,multiplication(sk0(sk1),X1)),X1),
inference(step,[status(thm)],[t16234,t262]) ).
cnf(t54459,plain,
X1 = addition(X1,multiplication(sk2,multiplication(sk0(sk1),X1))),
inference(step,[status(thm)],[t54458,t273]) ).
cnf(t16245,plain,
addition(X1,multiplication(sk2,multiplication(sk0(sk1),X1))) = X1,
inference(orient,[status(thm)],[t54459]) ).
cnf(c16,plain,
( multiplication(X1,X0) = zero
| ~ complement(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(hi16,axiom,
ifeq(complement(X0,X1),true,multiplication(X0,X1),zero) = zero,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t17,plain,
multiplication(sk0(sk1),sk1) = zero,
inference(hyper_resolution,[status(thm)],[hi16,h4]) ).
cnf(t547,plain,
multiplication(sk0(sk1),sk1) = zero,
inference(orient,[status(thm)],[t17]) ).
cnf(t549,plain,
multiplication(sk0(sk1),addition(X1,sk1)) = addition(multiplication(sk0(sk1),X1),zero),
inference(cp,[status(thm)],[t343,t547]) ).
cnf(t54122,plain,
multiplication(sk0(sk1),addition(X1,sk1)) = multiplication(sk0(sk1),X1),
inference(step,[status(thm)],[t549,t259]) ).
cnf(t2721,plain,
multiplication(sk0(sk1),addition(X1,sk1)) = multiplication(sk0(sk1),X1),
inference(orient,[status(thm)],[t54122]) ).
cnf(t2723,plain,
multiplication(sk0(sk1),X1) = multiplication(sk0(sk1),addition(sk1,X1)),
inference(cp,[status(thm)],[t2721,t273]) ).
cnf(t3506,plain,
multiplication(sk0(sk1),addition(sk1,X1)) = multiplication(sk0(sk1),X1),
inference(orient,[status(thm)],[t2723]) ).
cnf(t1108,plain,
multiplication(addition(sk1,X1),sk1) = addition(sk1,multiplication(X1,sk1)),
inference(cp,[status(thm)],[t337,t1100]) ).
cnf(t339,plain,
multiplication(addition(one,X1),X2) = addition(X2,multiplication(X1,X2)),
inference(cp,[status(thm)],[t337,t261]) ).
cnf(t926,plain,
addition(X1,multiplication(X2,X1)) = multiplication(addition(one,X2),X1),
inference(orient,[status(thm)],[t339]) ).
cnf(t54034,plain,
multiplication(addition(sk1,X1),sk1) = multiplication(addition(one,X1),sk1),
inference(step,[status(thm)],[t1108,t926]) ).
cnf(t1163,plain,
multiplication(addition(one,X1),sk1) = multiplication(addition(sk1,X1),sk1),
inference(orient,[status(thm)],[t54034]) ).
cnf(t2710,plain,
multiplication(addition(X1,sk2),addition(one,sk0(sk2))) = addition(addition(X1,sk2),multiplication(X1,sk0(sk2))),
inference(cp,[status(thm)],[t948,t2707]) ).
cnf(t54329,plain,
multiplication(addition(X1,sk2),one) = addition(addition(X1,sk2),multiplication(X1,sk0(sk2))),
inference(step,[status(thm)],[t2710,t712]) ).
cnf(t54330,plain,
addition(X1,sk2) = addition(addition(X1,sk2),multiplication(X1,sk0(sk2))),
inference(step,[status(thm)],[t54329,t260]) ).
cnf(t54331,plain,
addition(X1,sk2) = addition(X1,addition(sk2,multiplication(X1,sk0(sk2)))),
inference(step,[status(thm)],[t54330,t276]) ).
cnf(t5808,plain,
addition(X1,addition(sk2,multiplication(X1,sk0(sk2)))) = addition(X1,sk2),
inference(orient,[status(thm)],[t54331]) ).
cnf(t5824,plain,
multiplication(addition(sk1,addition(sk2,multiplication(one,sk0(sk2)))),sk1) = multiplication(addition(one,sk2),sk1),
inference(cp,[status(thm)],[t1163,t5808]) ).
cnf(t54332,plain,
multiplication(addition(sk2,addition(sk1,multiplication(one,sk0(sk2)))),sk1) = multiplication(addition(one,sk2),sk1),
inference(step,[status(thm)],[t5824,t2887]) ).
cnf(t54333,plain,
multiplication(addition(sk2,addition(sk1,sk0(sk2))),sk1) = multiplication(addition(one,sk2),sk1),
inference(step,[status(thm)],[t54332,t261]) ).
cnf(t312,plain,
addition(sk2,addition(sk0(sk2),X1)) = addition(one,X1),
inference(cp,[status(thm)],[t276,t310]) ).
cnf(t1045,plain,
addition(sk2,addition(sk0(sk2),X1)) = addition(one,X1),
inference(orient,[status(thm)],[t312]) ).
cnf(t1051,plain,
addition(one,X1) = addition(sk2,addition(X1,sk0(sk2))),
inference(cp,[status(thm)],[t1045,t273]) ).
cnf(t1537,plain,
addition(sk2,addition(X1,sk0(sk2))) = addition(one,X1),
inference(orient,[status(thm)],[t1051]) ).
cnf(t54334,plain,
multiplication(addition(one,sk1),sk1) = multiplication(addition(one,sk2),sk1),
inference(step,[status(thm)],[t54333,t1537]) ).
cnf(t54335,plain,
multiplication(addition(sk1,one),sk1) = multiplication(addition(one,sk2),sk1),
inference(step,[status(thm)],[t54334,t273]) ).
cnf(t659,plain,
addition(sk1,c(sk1)) = addition(sk1,one),
inference(cp,[status(thm)],[t655,t289]) ).
cnf(t54001,plain,
one = addition(sk1,one),
inference(step,[status(thm)],[t659,t289]) ).
cnf(t675,plain,
addition(sk1,one) = one,
inference(orient,[status(thm)],[t54001]) ).
cnf(t54336,plain,
multiplication(one,sk1) = multiplication(addition(one,sk2),sk1),
inference(step,[status(thm)],[t54335,t675]) ).
cnf(t54337,plain,
sk1 = multiplication(addition(one,sk2),sk1),
inference(step,[status(thm)],[t54336,t261]) ).
cnf(t54338,plain,
sk1 = multiplication(addition(sk1,sk2),sk1),
inference(step,[status(thm)],[t54337,t1163]) ).
cnf(t54339,plain,
sk1 = multiplication(addition(sk2,sk1),sk1),
inference(step,[status(thm)],[t54338,t273]) ).
cnf(t5863,plain,
multiplication(addition(sk2,sk1),sk1) = sk1,
inference(orient,[status(thm)],[t54339]) ).
cnf(t5871,plain,
multiplication(addition(addition(sk2,sk1),X1),sk1) = addition(sk1,multiplication(X1,sk1)),
inference(cp,[status(thm)],[t337,t5863]) ).
cnf(t54346,plain,
multiplication(addition(sk2,addition(sk1,X1)),sk1) = addition(sk1,multiplication(X1,sk1)),
inference(step,[status(thm)],[t5871,t276]) ).
cnf(t54347,plain,
multiplication(addition(sk2,addition(sk1,X1)),sk1) = multiplication(addition(one,X1),sk1),
inference(step,[status(thm)],[t54346,t926]) ).
cnf(t54348,plain,
multiplication(addition(sk2,addition(sk1,X1)),sk1) = multiplication(addition(sk1,X1),sk1),
inference(step,[status(thm)],[t54347,t1163]) ).
cnf(t5923,plain,
multiplication(addition(sk2,addition(sk1,X1)),sk1) = multiplication(addition(sk1,X1),sk1),
inference(orient,[status(thm)],[t54348]) ).
cnf(t2725,plain,
multiplication(addition(one,sk0(sk1)),addition(X1,sk1)) = addition(addition(X1,sk1),multiplication(sk0(sk1),X1)),
inference(cp,[status(thm)],[t926,t2721]) ).
cnf(t54353,plain,
multiplication(one,addition(X1,sk1)) = addition(addition(X1,sk1),multiplication(sk0(sk1),X1)),
inference(step,[status(thm)],[t2725,t718]) ).
cnf(t54354,plain,
addition(X1,sk1) = addition(addition(X1,sk1),multiplication(sk0(sk1),X1)),
inference(step,[status(thm)],[t54353,t261]) ).
cnf(t54355,plain,
addition(X1,sk1) = addition(X1,addition(sk1,multiplication(sk0(sk1),X1))),
inference(step,[status(thm)],[t54354,t276]) ).
cnf(t5992,plain,
addition(X1,addition(sk1,multiplication(sk0(sk1),X1))) = addition(X1,sk1),
inference(orient,[status(thm)],[t54355]) ).
cnf(t6010,plain,
multiplication(addition(sk1,multiplication(sk0(sk1),sk2)),sk1) = multiplication(addition(sk2,sk1),sk1),
inference(cp,[status(thm)],[t5923,t5992]) ).
cnf(t54356,plain,
multiplication(addition(sk1,multiplication(sk0(sk1),sk2)),sk1) = sk1,
inference(step,[status(thm)],[t6010,t5863]) ).
cnf(t6045,plain,
multiplication(addition(sk1,multiplication(sk0(sk1),sk2)),sk1) = sk1,
inference(orient,[status(thm)],[t54356]) ).
cnf(t7690,plain,
true = leq(multiplication(multiplication(sk0(sk1),sk2),sk1),sk1),
inference(cp,[status(thm)],[t7591,t6045]) ).
cnf(t54383,plain,
true = leq(multiplication(sk0(sk1),multiplication(sk2,sk1)),sk1),
inference(step,[status(thm)],[t7690,t585]) ).
cnf(t7756,plain,
leq(multiplication(sk0(sk1),multiplication(sk2,sk1)),sk1) = true,
inference(orient,[status(thm)],[t54383]) ).
cnf(t7757,plain,
sk1 = ifeq(true,true,addition(multiplication(sk0(sk1),multiplication(sk2,sk1)),sk1),sk1),
inference(cp,[status(thm)],[t264,t7756]) ).
cnf(t54388,plain,
sk1 = addition(multiplication(sk0(sk1),multiplication(sk2,sk1)),sk1),
inference(step,[status(thm)],[t7757,t262]) ).
cnf(t54389,plain,
sk1 = addition(sk1,multiplication(sk0(sk1),multiplication(sk2,sk1))),
inference(step,[status(thm)],[t54388,t273]) ).
cnf(t7794,plain,
addition(sk1,multiplication(sk0(sk1),multiplication(sk2,sk1))) = sk1,
inference(orient,[status(thm)],[t54389]) ).
cnf(t7797,plain,
multiplication(sk0(sk1),multiplication(sk0(sk1),multiplication(sk2,sk1))) = multiplication(sk0(sk1),sk1),
inference(cp,[status(thm)],[t3506,t7794]) ).
cnf(t3154,plain,
multiplication(sk0(sk1),multiplication(sk0(sk1),X1)) = multiplication(sk0(sk1),X1),
inference(cp,[status(thm)],[t585,t3153]) ).
cnf(t4047,plain,
multiplication(sk0(sk1),multiplication(sk0(sk1),X1)) = multiplication(sk0(sk1),X1),
inference(orient,[status(thm)],[t3154]) ).
cnf(t54390,plain,
multiplication(sk0(sk1),multiplication(sk2,sk1)) = multiplication(sk0(sk1),sk1),
inference(step,[status(thm)],[t7797,t4047]) ).
cnf(t54391,plain,
multiplication(sk0(sk1),multiplication(sk2,sk1)) = zero,
inference(step,[status(thm)],[t54390,t547]) ).
cnf(t7815,plain,
multiplication(sk0(sk1),multiplication(sk2,sk1)) = zero,
inference(orient,[status(thm)],[t54391]) ).
cnf(t7816,plain,
multiplication(sk0(sk1),addition(one,multiplication(sk2,sk1))) = addition(sk0(sk1),zero),
inference(cp,[status(thm)],[t948,t7815]) ).
cnf(t54397,plain,
multiplication(sk0(sk1),addition(one,multiplication(sk2,sk1))) = sk0(sk1),
inference(step,[status(thm)],[t7816,t259]) ).
cnf(t7871,plain,
multiplication(sk0(sk1),addition(one,multiplication(sk2,sk1))) = sk0(sk1),
inference(orient,[status(thm)],[t54397]) ).
cnf(t16250,plain,
addition(one,multiplication(sk2,sk1)) = addition(addition(one,multiplication(sk2,sk1)),multiplication(sk2,sk0(sk1))),
inference(cp,[status(thm)],[t16245,t7871]) ).
cnf(t54460,plain,
addition(one,multiplication(sk2,sk1)) = addition(one,addition(multiplication(sk2,sk1),multiplication(sk2,sk0(sk1)))),
inference(step,[status(thm)],[t16250,t276]) ).
cnf(t54461,plain,
addition(one,multiplication(sk2,sk1)) = addition(one,multiplication(sk2,addition(sk1,sk0(sk1)))),
inference(step,[status(thm)],[t54460,t343]) ).
cnf(t54462,plain,
addition(one,multiplication(sk2,sk1)) = addition(one,multiplication(sk2,one)),
inference(step,[status(thm)],[t54461,t307]) ).
cnf(t54463,plain,
addition(one,multiplication(sk2,sk1)) = addition(one,sk2),
inference(step,[status(thm)],[t54462,t260]) ).
cnf(t54464,plain,
addition(one,multiplication(sk2,sk1)) = addition(sk2,one),
inference(step,[status(thm)],[t54463,t273]) ).
cnf(t54465,plain,
addition(one,multiplication(sk2,sk1)) = one,
inference(step,[status(thm)],[t54464,t669]) ).
cnf(t16322,plain,
addition(one,multiplication(sk2,sk1)) = one,
inference(orient,[status(thm)],[t54465]) ).
cnf(t16367,plain,
true = leq(multiplication(X1,multiplication(sk2,sk1)),multiplication(X1,one)),
inference(cp,[status(thm)],[t7887,t16322]) ).
cnf(t54469,plain,
true = leq(multiplication(X1,multiplication(sk2,sk1)),X1),
inference(step,[status(thm)],[t16367,t260]) ).
cnf(t16407,plain,
leq(multiplication(X1,multiplication(sk2,sk1)),X1) = true,
inference(orient,[status(thm)],[t54469]) ).
cnf(t74,plain,
multiplication(or(c(sk2),false),sk2) = zero,
inference(hyper_resolution,[status(thm)],[hi15,h16]) ).
cnf(t53964,plain,
multiplication(c(sk2),sk2) = zero,
inference(step,[status(thm)],[t74,t256]) ).
cnf(t482,plain,
multiplication(c(sk2),sk2) = zero,
inference(orient,[status(thm)],[t53964]) ).
cnf(t486,plain,
multiplication(addition(X1,c(sk2)),sk2) = addition(multiplication(X1,sk2),zero),
inference(cp,[status(thm)],[t337,t482]) ).
cnf(t54037,plain,
multiplication(addition(X1,c(sk2)),sk2) = multiplication(X1,sk2),
inference(step,[status(thm)],[t486,t259]) ).
cnf(t1203,plain,
multiplication(addition(X1,c(sk2)),sk2) = multiplication(X1,sk2),
inference(orient,[status(thm)],[t54037]) ).
cnf(t1206,plain,
multiplication(X1,sk2) = multiplication(addition(c(sk2),X1),sk2),
inference(cp,[status(thm)],[t1203,t273]) ).
cnf(t1572,plain,
multiplication(addition(c(sk2),X1),sk2) = multiplication(X1,sk2),
inference(orient,[status(thm)],[t1206]) ).
cnf(c14,plain,
( ~ complement(X1,X0)
| test(X0) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(hi14,axiom,
ifeq(complement(X0,X1),true,test(X1),true) = true,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(h94,plain,
test(or(c(sk2),false)) = true,
inference(hyper_resolution,[status(thm)],[hi14,h16]) ).
cnf(h213,plain,
complement(sk0(or(c(sk2),false)),or(c(sk2),false)) = true,
inference(hyper_resolution,[status(thm)],[hi13,h94]) ).
cnf(t138,plain,
addition(or(c(sk2),false),sk0(or(c(sk2),false))) = one,
inference(hyper_resolution,[status(thm)],[hi17,h213]) ).
cnf(t53901,plain,
addition(c(sk2),sk0(or(c(sk2),false))) = one,
inference(step,[status(thm)],[t138,t256]) ).
cnf(t53902,plain,
addition(c(sk2),sk0(c(sk2))) = one,
inference(step,[status(thm)],[t53901,t256]) ).
cnf(t298,plain,
addition(c(sk2),sk0(c(sk2))) = one,
inference(orient,[status(thm)],[t53902]) ).
cnf(t1573,plain,
multiplication(sk0(c(sk2)),sk2) = multiplication(one,sk2),
inference(cp,[status(thm)],[t1572,t298]) ).
cnf(t54056,plain,
multiplication(sk0(c(sk2)),sk2) = sk2,
inference(step,[status(thm)],[t1573,t261]) ).
cnf(t1584,plain,
multiplication(sk0(c(sk2)),sk2) = sk2,
inference(orient,[status(thm)],[t54056]) ).
cnf(t3297,plain,
multiplication(c(sk2),sk0(sk2)) = multiplication(one,sk0(sk2)),
inference(cp,[status(thm)],[t3291,t295]) ).
cnf(t484,plain,
multiplication(c(sk2),addition(X1,sk2)) = addition(multiplication(c(sk2),X1),zero),
inference(cp,[status(thm)],[t343,t482]) ).
cnf(t54117,plain,
multiplication(c(sk2),addition(X1,sk2)) = multiplication(c(sk2),X1),
inference(step,[status(thm)],[t484,t259]) ).
cnf(t2651,plain,
multiplication(c(sk2),addition(X1,sk2)) = multiplication(c(sk2),X1),
inference(orient,[status(thm)],[t54117]) ).
cnf(t2653,plain,
multiplication(c(sk2),X1) = multiplication(c(sk2),addition(sk2,X1)),
inference(cp,[status(thm)],[t2651,t273]) ).
cnf(t2818,plain,
multiplication(c(sk2),addition(sk2,X1)) = multiplication(c(sk2),X1),
inference(orient,[status(thm)],[t2653]) ).
cnf(t2825,plain,
multiplication(c(sk2),sk0(sk2)) = multiplication(c(sk2),one),
inference(cp,[status(thm)],[t2818,t310]) ).
cnf(t54129,plain,
multiplication(c(sk2),sk0(sk2)) = c(sk2),
inference(step,[status(thm)],[t2825,t260]) ).
cnf(t2848,plain,
multiplication(c(sk2),sk0(sk2)) = c(sk2),
inference(orient,[status(thm)],[t54129]) ).
cnf(t54170,plain,
c(sk2) = multiplication(one,sk0(sk2)),
inference(step,[status(thm)],[t3297,t2848]) ).
cnf(t54171,plain,
c(sk2) = sk0(sk2),
inference(step,[status(thm)],[t54170,t261]) ).
cnf(t3312,plain,
c(sk2) = sk0(sk2),
inference(orient,[status(thm)],[t54171]) ).
cnf(t54187,plain,
multiplication(sk0(sk0(sk2)),sk2) = sk2,
inference(step,[status(thm)],[t1584,t3312]) ).
cnf(t3325,plain,
multiplication(sk0(sk0(sk2)),sk2) = sk2,
inference(rw,[status(thm)],[t54187]) ).
cnf(t3362,plain,
multiplication(sk0(sk0(sk2)),sk2) = sk2,
inference(orient,[status(thm)],[t3325]) ).
cnf(t3365,plain,
multiplication(sk0(sk0(sk2)),multiplication(sk2,X1)) = multiplication(sk2,X1),
inference(cp,[status(thm)],[t585,t3362]) ).
cnf(t3722,plain,
multiplication(sk0(sk0(sk2)),multiplication(sk2,X1)) = multiplication(sk2,X1),
inference(orient,[status(thm)],[t3365]) ).
cnf(t16409,plain,
true = leq(multiplication(sk2,sk1),sk0(sk0(sk2))),
inference(cp,[status(thm)],[t16407,t3722]) ).
cnf(t16451,plain,
leq(multiplication(sk2,sk1),sk0(sk0(sk2))) = true,
inference(orient,[status(thm)],[t16409]) ).
cnf(t16452,plain,
sk0(sk0(sk2)) = ifeq(true,true,addition(multiplication(sk2,sk1),sk0(sk0(sk2))),sk0(sk0(sk2))),
inference(cp,[status(thm)],[t264,t16451]) ).
cnf(t54475,plain,
sk0(sk0(sk2)) = addition(multiplication(sk2,sk1),sk0(sk0(sk2))),
inference(step,[status(thm)],[t16452,t262]) ).
cnf(t16772,plain,
addition(multiplication(sk2,sk1),sk0(sk0(sk2))) = sk0(sk0(sk2)),
inference(orient,[status(thm)],[t54475]) ).
cnf(t16805,plain,
true = leq(multiplication(sk2,sk1),addition(X1,sk0(sk0(sk2)))),
inference(cp,[status(thm)],[t2469,t16772]) ).
cnf(t19040,plain,
leq(multiplication(sk2,sk1),addition(X1,sk0(sk0(sk2)))) = true,
inference(orient,[status(thm)],[t16805]) ).
cnf(t19042,plain,
true = leq(multiplication(sk2,sk1),addition(sk0(sk0(sk2)),X1)),
inference(cp,[status(thm)],[t19040,t273]) ).
cnf(t19897,plain,
leq(multiplication(sk2,sk1),addition(sk0(sk0(sk2)),X1)) = true,
inference(orient,[status(thm)],[t19042]) ).
cnf(c20,plain,
( ~ complement(X0,X1)
| c(X0) = X1
| ~ test(X0) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(t227,plain,
ifeq(test(X1),true,ifeq(complement(X1,X2),true,c(X1),X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(t263,plain,
ifeq(test(X1),true,ifeq(complement(X1,X2),true,c(X1),X2),X2) = X2,
inference(orient,[status(thm)],[t227]) ).
cnf(c18,plain,
( addition(X0,X1) != one
| multiplication(X1,X0) != zero
| multiplication(X0,X1) != zero
| complement(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(t255,plain,
ifeq(multiplication(X1,X2),zero,ifeq(multiplication(X2,X1),zero,ifeq(addition(X1,X2),one,complement(X2,X1),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(t404,plain,
ifeq(multiplication(X1,X2),zero,ifeq(multiplication(X2,X1),zero,ifeq(addition(X1,X2),one,complement(X2,X1),true),true),true) = true,
inference(orient,[status(thm)],[t255]) ).
cnf(t432,plain,
true = ifeq(multiplication(X1,X2),zero,ifeq(multiplication(X2,X1),zero,ifeq(addition(X2,X1),one,complement(X2,X1),true),true),true),
inference(cp,[status(thm)],[t404,t273]) ).
cnf(t31125,plain,
ifeq(multiplication(X1,X2),zero,ifeq(multiplication(X2,X1),zero,ifeq(addition(X2,X1),one,complement(X2,X1),true),true),true) = true,
inference(orient,[status(thm)],[t432]) ).
cnf(t152,plain,
multiplication(sk0(or(c(sk2),false)),or(c(sk2),false)) = zero,
inference(hyper_resolution,[status(thm)],[hi16,h213]) ).
cnf(t53974,plain,
multiplication(sk0(c(sk2)),or(c(sk2),false)) = zero,
inference(step,[status(thm)],[t152,t256]) ).
cnf(t53975,plain,
multiplication(sk0(c(sk2)),c(sk2)) = zero,
inference(step,[status(thm)],[t53974,t256]) ).
cnf(t541,plain,
multiplication(sk0(c(sk2)),c(sk2)) = zero,
inference(orient,[status(thm)],[t53975]) ).
cnf(t54190,plain,
multiplication(sk0(sk0(sk2)),c(sk2)) = zero,
inference(step,[status(thm)],[t541,t3312]) ).
cnf(t54191,plain,
multiplication(sk0(sk0(sk2)),sk0(sk2)) = zero,
inference(step,[status(thm)],[t54190,t3312]) ).
cnf(t3328,plain,
multiplication(sk0(sk0(sk2)),sk0(sk2)) = zero,
inference(rw,[status(thm)],[t54191]) ).
cnf(t3408,plain,
multiplication(sk0(sk0(sk2)),sk0(sk2)) = zero,
inference(orient,[status(thm)],[t3328]) ).
cnf(t31154,plain,
true = ifeq(zero,zero,ifeq(multiplication(sk0(sk2),sk0(sk0(sk2))),zero,ifeq(addition(sk0(sk2),sk0(sk0(sk2))),one,complement(sk0(sk2),sk0(sk0(sk2))),true),true),true),
inference(cp,[status(thm)],[t31125,t3408]) ).
cnf(t54755,plain,
true = ifeq(multiplication(sk0(sk2),sk0(sk0(sk2))),zero,ifeq(addition(sk0(sk2),sk0(sk0(sk2))),one,complement(sk0(sk2),sk0(sk0(sk2))),true),true),
inference(step,[status(thm)],[t31154,t262]) ).
cnf(t148,plain,
multiplication(or(c(sk2),false),sk0(or(c(sk2),false))) = zero,
inference(hyper_resolution,[status(thm)],[hi15,h213]) ).
cnf(t53965,plain,
multiplication(c(sk2),sk0(or(c(sk2),false))) = zero,
inference(step,[status(thm)],[t148,t256]) ).
cnf(t53966,plain,
multiplication(c(sk2),sk0(c(sk2))) = zero,
inference(step,[status(thm)],[t53965,t256]) ).
cnf(t489,plain,
multiplication(c(sk2),sk0(c(sk2))) = zero,
inference(orient,[status(thm)],[t53966]) ).
cnf(t54192,plain,
multiplication(sk0(sk2),sk0(c(sk2))) = zero,
inference(step,[status(thm)],[t489,t3312]) ).
cnf(t54193,plain,
multiplication(sk0(sk2),sk0(sk0(sk2))) = zero,
inference(step,[status(thm)],[t54192,t3312]) ).
cnf(t3329,plain,
multiplication(sk0(sk2),sk0(sk0(sk2))) = zero,
inference(rw,[status(thm)],[t54193]) ).
cnf(t3418,plain,
multiplication(sk0(sk2),sk0(sk0(sk2))) = zero,
inference(orient,[status(thm)],[t3329]) ).
cnf(t54756,plain,
true = ifeq(zero,zero,ifeq(addition(sk0(sk2),sk0(sk0(sk2))),one,complement(sk0(sk2),sk0(sk0(sk2))),true),true),
inference(step,[status(thm)],[t54755,t3418]) ).
cnf(t54757,plain,
true = ifeq(addition(sk0(sk2),sk0(sk0(sk2))),one,complement(sk0(sk2),sk0(sk0(sk2))),true),
inference(step,[status(thm)],[t54756,t262]) ).
cnf(t54196,plain,
addition(sk0(sk2),sk0(c(sk2))) = one,
inference(step,[status(thm)],[t298,t3312]) ).
cnf(t54197,plain,
addition(sk0(sk2),sk0(sk0(sk2))) = one,
inference(step,[status(thm)],[t54196,t3312]) ).
cnf(t3331,plain,
addition(sk0(sk2),sk0(sk0(sk2))) = one,
inference(rw,[status(thm)],[t54197]) ).
cnf(t3433,plain,
addition(sk0(sk2),sk0(sk0(sk2))) = one,
inference(orient,[status(thm)],[t3331]) ).
cnf(t54758,plain,
true = ifeq(one,one,complement(sk0(sk2),sk0(sk0(sk2))),true),
inference(step,[status(thm)],[t54757,t3433]) ).
cnf(t54759,plain,
true = complement(sk0(sk2),sk0(sk0(sk2))),
inference(step,[status(thm)],[t54758,t262]) ).
cnf(t31601,plain,
complement(sk0(sk2),sk0(sk0(sk2))) = true,
inference(orient,[status(thm)],[t54759]) ).
cnf(t31604,plain,
sk0(sk0(sk2)) = ifeq(test(sk0(sk2)),true,ifeq(true,true,c(sk0(sk2)),sk0(sk0(sk2))),sk0(sk0(sk2))),
inference(cp,[status(thm)],[t263,t31601]) ).
cnf(t42,plain,
test(or(c(sk2),false)) = true,
inference(hyper_resolution,[status(thm)],[hi14,h16]) ).
cnf(t53936,plain,
test(c(sk2)) = true,
inference(step,[status(thm)],[t42,t256]) ).
cnf(t355,plain,
test(c(sk2)) = true,
inference(orient,[status(thm)],[t53936]) ).
cnf(t54183,plain,
test(sk0(sk2)) = true,
inference(step,[status(thm)],[t355,t3312]) ).
cnf(t3321,plain,
test(sk0(sk2)) = true,
inference(rw,[status(thm)],[t54183]) ).
cnf(t3342,plain,
test(sk0(sk2)) = true,
inference(orient,[status(thm)],[t3321]) ).
cnf(t54760,plain,
sk0(sk0(sk2)) = ifeq(true,true,ifeq(true,true,c(sk0(sk2)),sk0(sk0(sk2))),sk0(sk0(sk2))),
inference(step,[status(thm)],[t31604,t3342]) ).
cnf(t54761,plain,
sk0(sk0(sk2)) = ifeq(true,true,c(sk0(sk2)),sk0(sk0(sk2))),
inference(step,[status(thm)],[t54760,t262]) ).
cnf(t54762,plain,
sk0(sk0(sk2)) = c(sk0(sk2)),
inference(step,[status(thm)],[t54761,t262]) ).
cnf(t85,plain,
multiplication(sk2,or(c(sk2),false)) = zero,
inference(hyper_resolution,[status(thm)],[hi16,h16]) ).
cnf(t53971,plain,
multiplication(sk2,c(sk2)) = zero,
inference(step,[status(thm)],[t85,t256]) ).
cnf(t517,plain,
multiplication(sk2,c(sk2)) = zero,
inference(orient,[status(thm)],[t53971]) ).
cnf(t522,plain,
true = ifeq(zero,zero,ifeq(multiplication(c(sk2),sk2),zero,ifeq(addition(sk2,c(sk2)),one,complement(c(sk2),sk2),true),true),true),
inference(cp,[status(thm)],[t404,t517]) ).
cnf(t53991,plain,
true = ifeq(multiplication(c(sk2),sk2),zero,ifeq(addition(sk2,c(sk2)),one,complement(c(sk2),sk2),true),true),
inference(step,[status(thm)],[t522,t262]) ).
cnf(t53992,plain,
true = ifeq(zero,zero,ifeq(addition(sk2,c(sk2)),one,complement(c(sk2),sk2),true),true),
inference(step,[status(thm)],[t53991,t482]) ).
cnf(t53993,plain,
true = ifeq(addition(sk2,c(sk2)),one,complement(c(sk2),sk2),true),
inference(step,[status(thm)],[t53992,t262]) ).
cnf(t53994,plain,
true = ifeq(one,one,complement(c(sk2),sk2),true),
inference(step,[status(thm)],[t53993,t295]) ).
cnf(t53995,plain,
true = complement(c(sk2),sk2),
inference(step,[status(thm)],[t53994,t262]) ).
cnf(t648,plain,
complement(c(sk2),sk2) = true,
inference(orient,[status(thm)],[t53995]) ).
cnf(t649,plain,
sk2 = ifeq(test(c(sk2)),true,ifeq(true,true,c(c(sk2)),sk2),sk2),
inference(cp,[status(thm)],[t263,t648]) ).
cnf(t53996,plain,
sk2 = ifeq(true,true,ifeq(true,true,c(c(sk2)),sk2),sk2),
inference(step,[status(thm)],[t649,t355]) ).
cnf(t53997,plain,
sk2 = ifeq(true,true,c(c(sk2)),sk2),
inference(step,[status(thm)],[t53996,t262]) ).
cnf(t53998,plain,
sk2 = c(c(sk2)),
inference(step,[status(thm)],[t53997,t262]) ).
cnf(t651,plain,
c(c(sk2)) = sk2,
inference(orient,[status(thm)],[t53998]) ).
cnf(t54181,plain,
c(sk0(sk2)) = sk2,
inference(step,[status(thm)],[t651,t3312]) ).
cnf(t3319,plain,
c(sk0(sk2)) = sk2,
inference(rw,[status(thm)],[t54181]) ).
cnf(t3338,plain,
c(sk0(sk2)) = sk2,
inference(orient,[status(thm)],[t3319]) ).
cnf(t54763,plain,
sk0(sk0(sk2)) = sk2,
inference(step,[status(thm)],[t54762,t3338]) ).
cnf(t31609,plain,
sk0(sk0(sk2)) = sk2,
inference(orient,[status(thm)],[t54763]) ).
cnf(t54770,plain,
leq(multiplication(sk2,sk1),addition(sk2,X1)) = true,
inference(step,[status(thm)],[t19897,t31609]) ).
cnf(t31614,plain,
leq(multiplication(sk2,sk1),addition(sk2,X1)) = true,
inference(rw,[status(thm)],[t54770]) ).
cnf(t31658,plain,
leq(multiplication(sk2,sk1),addition(sk2,X1)) = true,
inference(orient,[status(thm)],[t31614]) ).
cnf(t31665,plain,
addition(sk2,X1) = ifeq(true,true,addition(multiplication(sk2,sk1),addition(sk2,X1)),addition(sk2,X1)),
inference(cp,[status(thm)],[t264,t31658]) ).
cnf(t54836,plain,
addition(sk2,X1) = addition(multiplication(sk2,sk1),addition(sk2,X1)),
inference(step,[status(thm)],[t31665,t262]) ).
cnf(t54837,plain,
addition(sk2,X1) = addition(sk2,addition(multiplication(sk2,sk1),X1)),
inference(step,[status(thm)],[t54836,t2887]) ).
cnf(t31690,plain,
addition(sk2,addition(multiplication(sk2,sk1),X1)) = addition(sk2,X1),
inference(orient,[status(thm)],[t54837]) ).
cnf(t31694,plain,
addition(sk2,multiplication(X1,sk1)) = addition(sk2,multiplication(addition(sk2,X1),sk1)),
inference(cp,[status(thm)],[t31690,t337]) ).
cnf(t32057,plain,
addition(sk2,multiplication(addition(sk2,X1),sk1)) = addition(sk2,multiplication(X1,sk1)),
inference(orient,[status(thm)],[t31694]) ).
cnf(t32072,plain,
addition(sk2,multiplication(sk0(sk2),sk1)) = addition(sk2,multiplication(one,sk1)),
inference(cp,[status(thm)],[t32057,t310]) ).
cnf(t54844,plain,
addition(sk2,multiplication(sk0(sk2),sk1)) = addition(sk2,sk1),
inference(step,[status(thm)],[t32072,t261]) ).
cnf(t32166,plain,
addition(sk2,multiplication(sk0(sk2),sk1)) = addition(sk2,sk1),
inference(orient,[status(thm)],[t54844]) ).
cnf(t32172,plain,
multiplication(multiplication(sk0(sk2),sk1),sk0(sk2)) = multiplication(addition(sk2,sk1),sk0(sk2)),
inference(cp,[status(thm)],[t3291,t32166]) ).
cnf(t54845,plain,
multiplication(sk0(sk2),multiplication(sk1,sk0(sk2))) = multiplication(addition(sk2,sk1),sk0(sk2)),
inference(step,[status(thm)],[t32172,t585]) ).
cnf(t18,plain,
multiplication(sk0(sk2),sk2) = zero,
inference(hyper_resolution,[status(thm)],[hi16,h0]) ).
cnf(t553,plain,
multiplication(sk0(sk2),sk2) = zero,
inference(orient,[status(thm)],[t18]) ).
cnf(t555,plain,
multiplication(sk0(sk2),addition(X1,sk2)) = addition(multiplication(sk0(sk2),X1),zero),
inference(cp,[status(thm)],[t343,t553]) ).
cnf(t54123,plain,
multiplication(sk0(sk2),addition(X1,sk2)) = multiplication(sk0(sk2),X1),
inference(step,[status(thm)],[t555,t259]) ).
cnf(t2735,plain,
multiplication(sk0(sk2),addition(X1,sk2)) = multiplication(sk0(sk2),X1),
inference(orient,[status(thm)],[t54123]) ).
cnf(t2737,plain,
multiplication(sk0(sk2),X1) = multiplication(sk0(sk2),addition(sk2,X1)),
inference(cp,[status(thm)],[t2735,t273]) ).
cnf(t3523,plain,
multiplication(sk0(sk2),addition(sk2,X1)) = multiplication(sk0(sk2),X1),
inference(orient,[status(thm)],[t2737]) ).
cnf(t7116,plain,
true = leq(multiplication(sk1,X1),multiplication(one,X1)),
inference(cp,[status(thm)],[t7000,t675]) ).
cnf(t54373,plain,
true = leq(multiplication(sk1,X1),X1),
inference(step,[status(thm)],[t7116,t261]) ).
cnf(t7150,plain,
leq(multiplication(sk1,X1),X1) = true,
inference(orient,[status(thm)],[t54373]) ).
cnf(t512,plain,
multiplication(sk1,addition(X1,sk0(sk1))) = addition(multiplication(sk1,X1),zero),
inference(cp,[status(thm)],[t343,t510]) ).
cnf(t54046,plain,
multiplication(sk1,addition(X1,sk0(sk1))) = multiplication(sk1,X1),
inference(step,[status(thm)],[t512,t259]) ).
cnf(t1336,plain,
multiplication(sk1,addition(X1,sk0(sk1))) = multiplication(sk1,X1),
inference(orient,[status(thm)],[t54046]) ).
cnf(t7162,plain,
true = leq(multiplication(sk1,X1),addition(X1,sk0(sk1))),
inference(cp,[status(thm)],[t7150,t1336]) ).
cnf(t7262,plain,
leq(multiplication(sk1,X1),addition(X1,sk0(sk1))) = true,
inference(orient,[status(thm)],[t7162]) ).
cnf(t7280,plain,
addition(X1,sk0(sk1)) = ifeq(true,true,addition(multiplication(sk1,X1),addition(X1,sk0(sk1))),addition(X1,sk0(sk1))),
inference(cp,[status(thm)],[t264,t7262]) ).
cnf(t54556,plain,
addition(X1,sk0(sk1)) = addition(multiplication(sk1,X1),addition(X1,sk0(sk1))),
inference(step,[status(thm)],[t7280,t262]) ).
cnf(t54557,plain,
addition(X1,sk0(sk1)) = addition(X1,addition(multiplication(sk1,X1),sk0(sk1))),
inference(step,[status(thm)],[t54556,t2887]) ).
cnf(t54558,plain,
addition(X1,sk0(sk1)) = addition(X1,addition(sk0(sk1),multiplication(sk1,X1))),
inference(step,[status(thm)],[t54557,t273]) ).
cnf(t20611,plain,
addition(X1,addition(sk0(sk1),multiplication(sk1,X1))) = addition(X1,sk0(sk1)),
inference(orient,[status(thm)],[t54558]) ).
cnf(t20731,plain,
addition(one,addition(sk0(sk1),multiplication(sk1,sk0(sk2)))) = addition(one,addition(sk0(sk2),sk0(sk1))),
inference(cp,[status(thm)],[t1406,t20611]) ).
cnf(t54559,plain,
addition(one,multiplication(sk1,sk0(sk2))) = addition(one,addition(sk0(sk2),sk0(sk1))),
inference(step,[status(thm)],[t20731,t1421]) ).
cnf(t54560,plain,
addition(one,multiplication(sk1,sk0(sk2))) = addition(one,sk0(sk1)),
inference(step,[status(thm)],[t54559,t1406]) ).
cnf(t54561,plain,
addition(one,multiplication(sk1,sk0(sk2))) = one,
inference(step,[status(thm)],[t54560,t718]) ).
cnf(t20762,plain,
addition(one,multiplication(sk1,sk0(sk2))) = one,
inference(orient,[status(thm)],[t54561]) ).
cnf(t20803,plain,
true = leq(multiplication(multiplication(sk1,sk0(sk2)),X1),multiplication(one,X1)),
inference(cp,[status(thm)],[t7591,t20762]) ).
cnf(t54579,plain,
true = leq(multiplication(sk1,multiplication(sk0(sk2),X1)),multiplication(one,X1)),
inference(step,[status(thm)],[t20803,t585]) ).
cnf(t54580,plain,
true = leq(multiplication(sk1,multiplication(sk0(sk2),X1)),X1),
inference(step,[status(thm)],[t54579,t261]) ).
cnf(t21077,plain,
leq(multiplication(sk1,multiplication(sk0(sk2),X1)),X1) = true,
inference(orient,[status(thm)],[t54580]) ).
cnf(t21086,plain,
X1 = ifeq(true,true,addition(multiplication(sk1,multiplication(sk0(sk2),X1)),X1),X1),
inference(cp,[status(thm)],[t264,t21077]) ).
cnf(t54582,plain,
X1 = addition(multiplication(sk1,multiplication(sk0(sk2),X1)),X1),
inference(step,[status(thm)],[t21086,t262]) ).
cnf(t54583,plain,
X1 = addition(X1,multiplication(sk1,multiplication(sk0(sk2),X1))),
inference(step,[status(thm)],[t54582,t273]) ).
cnf(t21116,plain,
addition(X1,multiplication(sk1,multiplication(sk0(sk2),X1))) = X1,
inference(orient,[status(thm)],[t54583]) ).
cnf(t1204,plain,
multiplication(sk2,sk2) = multiplication(one,sk2),
inference(cp,[status(thm)],[t1203,t295]) ).
cnf(t54038,plain,
multiplication(sk2,sk2) = sk2,
inference(step,[status(thm)],[t1204,t261]) ).
cnf(t1218,plain,
multiplication(sk2,sk2) = sk2,
inference(orient,[status(thm)],[t54038]) ).
cnf(t1226,plain,
multiplication(addition(sk2,X1),sk2) = addition(sk2,multiplication(X1,sk2)),
inference(cp,[status(thm)],[t337,t1218]) ).
cnf(t54042,plain,
multiplication(addition(sk2,X1),sk2) = multiplication(addition(one,X1),sk2),
inference(step,[status(thm)],[t1226,t926]) ).
cnf(t1281,plain,
multiplication(addition(one,X1),sk2) = multiplication(addition(sk2,X1),sk2),
inference(orient,[status(thm)],[t54042]) ).
cnf(t5674,plain,
multiplication(addition(sk2,addition(sk1,multiplication(one,sk0(sk1)))),sk2) = multiplication(addition(one,sk1),sk2),
inference(cp,[status(thm)],[t1281,t5658]) ).
cnf(t54315,plain,
multiplication(addition(sk2,addition(sk1,sk0(sk1))),sk2) = multiplication(addition(one,sk1),sk2),
inference(step,[status(thm)],[t5674,t261]) ).
cnf(t54316,plain,
multiplication(addition(sk2,one),sk2) = multiplication(addition(one,sk1),sk2),
inference(step,[status(thm)],[t54315,t307]) ).
cnf(t54317,plain,
multiplication(one,sk2) = multiplication(addition(one,sk1),sk2),
inference(step,[status(thm)],[t54316,t669]) ).
cnf(t54318,plain,
sk2 = multiplication(addition(one,sk1),sk2),
inference(step,[status(thm)],[t54317,t261]) ).
cnf(t54319,plain,
sk2 = multiplication(addition(sk2,sk1),sk2),
inference(step,[status(thm)],[t54318,t1281]) ).
cnf(t5710,plain,
multiplication(addition(sk2,sk1),sk2) = sk2,
inference(orient,[status(thm)],[t54319]) ).
cnf(t5717,plain,
multiplication(addition(addition(sk2,sk1),X1),sk2) = addition(sk2,multiplication(X1,sk2)),
inference(cp,[status(thm)],[t337,t5710]) ).
cnf(t54322,plain,
multiplication(addition(sk2,addition(sk1,X1)),sk2) = addition(sk2,multiplication(X1,sk2)),
inference(step,[status(thm)],[t5717,t276]) ).
cnf(t54323,plain,
multiplication(addition(sk2,addition(sk1,X1)),sk2) = multiplication(addition(one,X1),sk2),
inference(step,[status(thm)],[t54322,t926]) ).
cnf(t54324,plain,
multiplication(addition(sk2,addition(sk1,X1)),sk2) = multiplication(addition(sk2,X1),sk2),
inference(step,[status(thm)],[t54323,t1281]) ).
cnf(t5757,plain,
multiplication(addition(sk2,addition(sk1,X1)),sk2) = multiplication(addition(sk2,X1),sk2),
inference(orient,[status(thm)],[t54324]) ).
cnf(t2739,plain,
multiplication(addition(one,sk0(sk2)),addition(X1,sk2)) = addition(addition(X1,sk2),multiplication(sk0(sk2),X1)),
inference(cp,[status(thm)],[t926,t2735]) ).
cnf(t54359,plain,
multiplication(one,addition(X1,sk2)) = addition(addition(X1,sk2),multiplication(sk0(sk2),X1)),
inference(step,[status(thm)],[t2739,t712]) ).
cnf(t54360,plain,
addition(X1,sk2) = addition(addition(X1,sk2),multiplication(sk0(sk2),X1)),
inference(step,[status(thm)],[t54359,t261]) ).
cnf(t54361,plain,
addition(X1,sk2) = addition(X1,addition(sk2,multiplication(sk0(sk2),X1))),
inference(step,[status(thm)],[t54360,t276]) ).
cnf(t6080,plain,
addition(X1,addition(sk2,multiplication(sk0(sk2),X1))) = addition(X1,sk2),
inference(orient,[status(thm)],[t54361]) ).
cnf(t6101,plain,
multiplication(addition(sk2,addition(sk2,multiplication(sk0(sk2),sk1))),sk2) = multiplication(addition(sk2,addition(sk1,sk2)),sk2),
inference(cp,[status(thm)],[t5757,t6080]) ).
cnf(t54362,plain,
multiplication(addition(sk2,multiplication(sk0(sk2),sk1)),sk2) = multiplication(addition(sk2,addition(sk1,sk2)),sk2),
inference(step,[status(thm)],[t6101,t655]) ).
cnf(t54363,plain,
multiplication(addition(sk2,multiplication(sk0(sk2),sk1)),sk2) = multiplication(addition(sk2,sk2),sk2),
inference(step,[status(thm)],[t54362,t5757]) ).
cnf(t54364,plain,
multiplication(addition(sk2,multiplication(sk0(sk2),sk1)),sk2) = multiplication(sk2,sk2),
inference(step,[status(thm)],[t54363,t258]) ).
cnf(t54365,plain,
multiplication(addition(sk2,multiplication(sk0(sk2),sk1)),sk2) = sk2,
inference(step,[status(thm)],[t54364,t1218]) ).
cnf(t6136,plain,
multiplication(addition(sk2,multiplication(sk0(sk2),sk1)),sk2) = sk2,
inference(orient,[status(thm)],[t54365]) ).
cnf(t7685,plain,
true = leq(multiplication(multiplication(sk0(sk2),sk1),sk2),sk2),
inference(cp,[status(thm)],[t7591,t6136]) ).
cnf(t54382,plain,
true = leq(multiplication(sk0(sk2),multiplication(sk1,sk2)),sk2),
inference(step,[status(thm)],[t7685,t585]) ).
cnf(t7751,plain,
leq(multiplication(sk0(sk2),multiplication(sk1,sk2)),sk2) = true,
inference(orient,[status(thm)],[t54382]) ).
cnf(t7752,plain,
sk2 = ifeq(true,true,addition(multiplication(sk0(sk2),multiplication(sk1,sk2)),sk2),sk2),
inference(cp,[status(thm)],[t264,t7751]) ).
cnf(t54384,plain,
sk2 = addition(multiplication(sk0(sk2),multiplication(sk1,sk2)),sk2),
inference(step,[status(thm)],[t7752,t262]) ).
cnf(t54385,plain,
sk2 = addition(sk2,multiplication(sk0(sk2),multiplication(sk1,sk2))),
inference(step,[status(thm)],[t54384,t273]) ).
cnf(t7761,plain,
addition(sk2,multiplication(sk0(sk2),multiplication(sk1,sk2))) = sk2,
inference(orient,[status(thm)],[t54385]) ).
cnf(t7764,plain,
multiplication(sk0(sk2),multiplication(sk0(sk2),multiplication(sk1,sk2))) = multiplication(sk0(sk2),sk2),
inference(cp,[status(thm)],[t3523,t7761]) ).
cnf(t3298,plain,
multiplication(sk0(sk2),sk0(sk2)) = multiplication(one,sk0(sk2)),
inference(cp,[status(thm)],[t3291,t310]) ).
cnf(t54204,plain,
multiplication(sk0(sk2),sk0(sk2)) = sk0(sk2),
inference(step,[status(thm)],[t3298,t261]) ).
cnf(t3398,plain,
multiplication(sk0(sk2),sk0(sk2)) = sk0(sk2),
inference(orient,[status(thm)],[t54204]) ).
cnf(t3399,plain,
multiplication(sk0(sk2),multiplication(sk0(sk2),X1)) = multiplication(sk0(sk2),X1),
inference(cp,[status(thm)],[t585,t3398]) ).
cnf(t4057,plain,
multiplication(sk0(sk2),multiplication(sk0(sk2),X1)) = multiplication(sk0(sk2),X1),
inference(orient,[status(thm)],[t3399]) ).
cnf(t54386,plain,
multiplication(sk0(sk2),multiplication(sk1,sk2)) = multiplication(sk0(sk2),sk2),
inference(step,[status(thm)],[t7764,t4057]) ).
cnf(t54387,plain,
multiplication(sk0(sk2),multiplication(sk1,sk2)) = zero,
inference(step,[status(thm)],[t54386,t553]) ).
cnf(t7780,plain,
multiplication(sk0(sk2),multiplication(sk1,sk2)) = zero,
inference(orient,[status(thm)],[t54387]) ).
cnf(t7781,plain,
multiplication(sk0(sk2),addition(one,multiplication(sk1,sk2))) = addition(sk0(sk2),zero),
inference(cp,[status(thm)],[t948,t7780]) ).
cnf(t54396,plain,
multiplication(sk0(sk2),addition(one,multiplication(sk1,sk2))) = sk0(sk2),
inference(step,[status(thm)],[t7781,t259]) ).
cnf(t7855,plain,
multiplication(sk0(sk2),addition(one,multiplication(sk1,sk2))) = sk0(sk2),
inference(orient,[status(thm)],[t54396]) ).
cnf(t21120,plain,
addition(one,multiplication(sk1,sk2)) = addition(addition(one,multiplication(sk1,sk2)),multiplication(sk1,sk0(sk2))),
inference(cp,[status(thm)],[t21116,t7855]) ).
cnf(t54584,plain,
addition(one,multiplication(sk1,sk2)) = addition(one,addition(multiplication(sk1,sk2),multiplication(sk1,sk0(sk2)))),
inference(step,[status(thm)],[t21120,t276]) ).
cnf(t54585,plain,
addition(one,multiplication(sk1,sk2)) = addition(one,multiplication(sk1,addition(sk2,sk0(sk2)))),
inference(step,[status(thm)],[t54584,t343]) ).
cnf(t54586,plain,
addition(one,multiplication(sk1,sk2)) = addition(one,multiplication(sk1,one)),
inference(step,[status(thm)],[t54585,t310]) ).
cnf(t54587,plain,
addition(one,multiplication(sk1,sk2)) = addition(one,sk1),
inference(step,[status(thm)],[t54586,t260]) ).
cnf(t54588,plain,
addition(one,multiplication(sk1,sk2)) = addition(sk1,one),
inference(step,[status(thm)],[t54587,t273]) ).
cnf(t54589,plain,
addition(one,multiplication(sk1,sk2)) = one,
inference(step,[status(thm)],[t54588,t675]) ).
cnf(t21200,plain,
addition(one,multiplication(sk1,sk2)) = one,
inference(orient,[status(thm)],[t54589]) ).
cnf(t21248,plain,
true = leq(multiplication(multiplication(sk1,sk2),X1),multiplication(one,X1)),
inference(cp,[status(thm)],[t7591,t21200]) ).
cnf(t54594,plain,
true = leq(multiplication(sk1,multiplication(sk2,X1)),multiplication(one,X1)),
inference(step,[status(thm)],[t21248,t585]) ).
cnf(t54595,plain,
true = leq(multiplication(sk1,multiplication(sk2,X1)),X1),
inference(step,[status(thm)],[t54594,t261]) ).
cnf(t21297,plain,
leq(multiplication(sk1,multiplication(sk2,X1)),X1) = true,
inference(orient,[status(thm)],[t54595]) ).
cnf(t21322,plain,
X1 = ifeq(true,true,addition(multiplication(sk1,multiplication(sk2,X1)),X1),X1),
inference(cp,[status(thm)],[t264,t21297]) ).
cnf(t54596,plain,
X1 = addition(multiplication(sk1,multiplication(sk2,X1)),X1),
inference(step,[status(thm)],[t21322,t262]) ).
cnf(t54597,plain,
X1 = addition(X1,multiplication(sk1,multiplication(sk2,X1))),
inference(step,[status(thm)],[t54596,t273]) ).
cnf(t21343,plain,
addition(X1,multiplication(sk1,multiplication(sk2,X1))) = X1,
inference(orient,[status(thm)],[t54597]) ).
cnf(t21435,plain,
true = leq(multiplication(sk1,multiplication(sk2,X1)),addition(X2,X1)),
inference(cp,[status(thm)],[t1785,t21343]) ).
cnf(t24266,plain,
leq(multiplication(sk1,multiplication(sk2,X1)),addition(X2,X1)) = true,
inference(orient,[status(thm)],[t21435]) ).
cnf(t24291,plain,
true = leq(multiplication(sk1,sk2),addition(X1,sk2)),
inference(cp,[status(thm)],[t24266,t1218]) ).
cnf(t24371,plain,
leq(multiplication(sk1,sk2),addition(X1,sk2)) = true,
inference(orient,[status(thm)],[t24291]) ).
cnf(t24374,plain,
addition(X1,sk2) = ifeq(true,true,addition(multiplication(sk1,sk2),addition(X1,sk2)),addition(X1,sk2)),
inference(cp,[status(thm)],[t264,t24371]) ).
cnf(t54646,plain,
addition(X1,sk2) = addition(multiplication(sk1,sk2),addition(X1,sk2)),
inference(step,[status(thm)],[t24374,t262]) ).
cnf(t278,plain,
addition(X1,addition(X2,X3)) = addition(X3,addition(X1,X2)),
inference(cp,[status(thm)],[t276,t273]) ).
cnf(t2237,plain,
addition(X1,addition(X2,X3)) = addition(X3,addition(X1,X2)),
inference(orient,[status(thm)],[t278]) ).
cnf(t54647,plain,
addition(X1,sk2) = addition(sk2,addition(multiplication(sk1,sk2),X1)),
inference(step,[status(thm)],[t54646,t2237]) ).
cnf(t24387,plain,
addition(sk2,addition(multiplication(sk1,sk2),X1)) = addition(X1,sk2),
inference(orient,[status(thm)],[t54647]) ).
cnf(t24399,plain,
addition(multiplication(sk1,X1),sk2) = addition(sk2,multiplication(sk1,addition(sk2,X1))),
inference(cp,[status(thm)],[t24387,t343]) ).
cnf(t54650,plain,
addition(sk2,multiplication(sk1,X1)) = addition(sk2,multiplication(sk1,addition(sk2,X1))),
inference(step,[status(thm)],[t24399,t273]) ).
cnf(t24569,plain,
addition(sk2,multiplication(sk1,addition(sk2,X1))) = addition(sk2,multiplication(sk1,X1)),
inference(orient,[status(thm)],[t54650]) ).
cnf(t24580,plain,
addition(sk2,multiplication(sk1,sk0(sk2))) = addition(sk2,multiplication(sk1,one)),
inference(cp,[status(thm)],[t24569,t310]) ).
cnf(t54651,plain,
addition(sk2,multiplication(sk1,sk0(sk2))) = addition(sk2,sk1),
inference(step,[status(thm)],[t24580,t260]) ).
cnf(t24660,plain,
addition(sk2,multiplication(sk1,sk0(sk2))) = addition(sk2,sk1),
inference(orient,[status(thm)],[t54651]) ).
cnf(t24666,plain,
multiplication(sk0(sk2),multiplication(sk1,sk0(sk2))) = multiplication(sk0(sk2),addition(sk2,sk1)),
inference(cp,[status(thm)],[t3523,t24660]) ).
cnf(t54652,plain,
multiplication(sk0(sk2),multiplication(sk1,sk0(sk2))) = multiplication(sk0(sk2),sk1),
inference(step,[status(thm)],[t24666,t3523]) ).
cnf(t24714,plain,
multiplication(sk0(sk2),multiplication(sk1,sk0(sk2))) = multiplication(sk0(sk2),sk1),
inference(orient,[status(thm)],[t54652]) ).
cnf(t54846,plain,
multiplication(sk0(sk2),sk1) = multiplication(addition(sk2,sk1),sk0(sk2)),
inference(step,[status(thm)],[t54845,t24714]) ).
cnf(t54847,plain,
multiplication(sk0(sk2),sk1) = multiplication(sk1,sk0(sk2)),
inference(step,[status(thm)],[t54846,t3291]) ).
cnf(t32227,plain,
multiplication(sk0(sk2),sk1) = multiplication(sk1,sk0(sk2)),
inference(orient,[status(thm)],[t54847]) ).
cnf(t53647,plain,
multiplication(addition(multiplication(sk1,sk2),sk0(sk2)),sk1) = addition(multiplication(sk1,sk2),multiplication(sk1,sk0(sk2))),
inference(cp,[status(thm)],[t53624,t32227]) ).
cnf(t55100,plain,
multiplication(addition(sk0(sk2),multiplication(sk1,sk2)),sk1) = addition(multiplication(sk1,sk2),multiplication(sk1,sk0(sk2))),
inference(step,[status(thm)],[t53647,t273]) ).
cnf(t55101,plain,
multiplication(addition(sk0(sk2),multiplication(sk1,sk2)),sk1) = multiplication(sk1,addition(sk2,sk0(sk2))),
inference(step,[status(thm)],[t55100,t343]) ).
cnf(t55102,plain,
multiplication(addition(sk0(sk2),multiplication(sk1,sk2)),sk1) = multiplication(sk1,one),
inference(step,[status(thm)],[t55101,t310]) ).
cnf(t55103,plain,
multiplication(addition(sk0(sk2),multiplication(sk1,sk2)),sk1) = sk1,
inference(step,[status(thm)],[t55102,t260]) ).
cnf(t53751,plain,
multiplication(addition(sk0(sk2),multiplication(sk1,sk2)),sk1) = sk1,
inference(orient,[status(thm)],[t55103]) ).
cnf(t53812,plain,
multiplication(sk2,multiplication(multiplication(sk1,sk2),sk1)) = multiplication(sk2,sk1),
inference(cp,[status(thm)],[t51052,t53751]) ).
cnf(t55104,plain,
multiplication(sk2,multiplication(sk1,multiplication(sk2,sk1))) = multiplication(sk2,sk1),
inference(step,[status(thm)],[t53812,t585]) ).
cnf(t55105,plain,
multiplication(sk2,multiplication(sk1,sk2)) = multiplication(sk2,sk1),
inference(step,[status(thm)],[t55104,t52630]) ).
cnf(t45886,plain,
multiplication(addition(multiplication(X1,sk2),X2),sk2) = addition(multiplication(X1,sk2),multiplication(X2,sk2)),
inference(cp,[status(thm)],[t45735,t1218]) ).
cnf(t54996,plain,
multiplication(addition(multiplication(X1,sk2),X2),sk2) = multiplication(addition(X1,X2),sk2),
inference(step,[status(thm)],[t45886,t337]) ).
cnf(t46193,plain,
multiplication(addition(multiplication(X1,sk2),X2),sk2) = multiplication(addition(X1,X2),sk2),
inference(orient,[status(thm)],[t54996]) ).
cnf(t46196,plain,
multiplication(addition(X1,multiplication(X2,sk2)),sk2) = multiplication(multiplication(addition(X1,X2),sk2),sk2),
inference(cp,[status(thm)],[t46193,t337]) ).
cnf(t54998,plain,
multiplication(addition(X1,multiplication(X2,sk2)),sk2) = multiplication(addition(X1,X2),multiplication(sk2,sk2)),
inference(step,[status(thm)],[t46196,t585]) ).
cnf(t54999,plain,
multiplication(addition(X1,multiplication(X2,sk2)),sk2) = multiplication(addition(X1,X2),sk2),
inference(step,[status(thm)],[t54998,t1218]) ).
cnf(t46441,plain,
multiplication(addition(X1,multiplication(X2,sk2)),sk2) = multiplication(addition(X1,X2),sk2),
inference(orient,[status(thm)],[t54999]) ).
cnf(t52633,plain,
multiplication(addition(one,sk1),multiplication(sk2,sk1)) = addition(multiplication(sk2,sk1),multiplication(sk1,sk2)),
inference(cp,[status(thm)],[t926,t52630]) ).
cnf(t1221,plain,
multiplication(sk2,multiplication(sk2,X1)) = multiplication(sk2,X1),
inference(cp,[status(thm)],[t585,t1218]) ).
cnf(t1230,plain,
multiplication(sk2,multiplication(sk2,X1)) = multiplication(sk2,X1),
inference(orient,[status(thm)],[t1221]) ).
cnf(t1237,plain,
multiplication(addition(sk2,X1),multiplication(sk2,X2)) = addition(multiplication(sk2,X2),multiplication(X1,multiplication(sk2,X2))),
inference(cp,[status(thm)],[t337,t1230]) ).
cnf(t54920,plain,
multiplication(addition(sk2,X1),multiplication(sk2,X2)) = multiplication(addition(one,X1),multiplication(sk2,X2)),
inference(step,[status(thm)],[t1237,t926]) ).
cnf(t37027,plain,
multiplication(addition(one,X1),multiplication(sk2,X2)) = multiplication(addition(sk2,X1),multiplication(sk2,X2)),
inference(orient,[status(thm)],[t54920]) ).
cnf(t55080,plain,
multiplication(addition(sk2,sk1),multiplication(sk2,sk1)) = addition(multiplication(sk2,sk1),multiplication(sk1,sk2)),
inference(step,[status(thm)],[t52633,t37027]) ).
cnf(t5712,plain,
multiplication(addition(sk2,sk1),multiplication(sk2,X1)) = multiplication(sk2,X1),
inference(cp,[status(thm)],[t585,t5710]) ).
cnf(t5721,plain,
multiplication(addition(sk2,sk1),multiplication(sk2,X1)) = multiplication(sk2,X1),
inference(orient,[status(thm)],[t5712]) ).
cnf(t55081,plain,
multiplication(sk2,sk1) = addition(multiplication(sk2,sk1),multiplication(sk1,sk2)),
inference(step,[status(thm)],[t55080,t5721]) ).
cnf(t52709,plain,
addition(multiplication(sk2,sk1),multiplication(sk1,sk2)) = multiplication(sk2,sk1),
inference(orient,[status(thm)],[t55081]) ).
cnf(t52718,plain,
multiplication(addition(multiplication(sk2,sk1),sk1),sk2) = multiplication(multiplication(sk2,sk1),sk2),
inference(cp,[status(thm)],[t46441,t52709]) ).
cnf(t55086,plain,
multiplication(addition(sk1,multiplication(sk2,sk1)),sk2) = multiplication(multiplication(sk2,sk1),sk2),
inference(step,[status(thm)],[t52718,t273]) ).
cnf(t55087,plain,
multiplication(multiplication(addition(one,sk2),sk1),sk2) = multiplication(multiplication(sk2,sk1),sk2),
inference(step,[status(thm)],[t55086,t926]) ).
cnf(t55088,plain,
multiplication(multiplication(addition(sk1,sk2),sk1),sk2) = multiplication(multiplication(sk2,sk1),sk2),
inference(step,[status(thm)],[t55087,t1163]) ).
cnf(t55089,plain,
multiplication(addition(sk1,sk2),multiplication(sk1,sk2)) = multiplication(multiplication(sk2,sk1),sk2),
inference(step,[status(thm)],[t55088,t585]) ).
cnf(t55090,plain,
multiplication(addition(sk2,sk1),multiplication(sk1,sk2)) = multiplication(multiplication(sk2,sk1),sk2),
inference(step,[status(thm)],[t55089,t273]) ).
cnf(t5866,plain,
multiplication(addition(sk2,sk1),multiplication(sk1,X1)) = multiplication(sk1,X1),
inference(cp,[status(thm)],[t585,t5863]) ).
cnf(t5875,plain,
multiplication(addition(sk2,sk1),multiplication(sk1,X1)) = multiplication(sk1,X1),
inference(orient,[status(thm)],[t5866]) ).
cnf(t55091,plain,
multiplication(sk1,sk2) = multiplication(multiplication(sk2,sk1),sk2),
inference(step,[status(thm)],[t55090,t5875]) ).
cnf(t55092,plain,
multiplication(sk1,sk2) = multiplication(sk2,multiplication(sk1,sk2)),
inference(step,[status(thm)],[t55091,t585]) ).
cnf(t53068,plain,
multiplication(sk2,multiplication(sk1,sk2)) = multiplication(sk1,sk2),
inference(orient,[status(thm)],[t55092]) ).
cnf(t55106,plain,
multiplication(sk1,sk2) = multiplication(sk2,sk1),
inference(step,[status(thm)],[t55105,t53068]) ).
cnf(t53825,plain,
multiplication(sk1,sk2) = multiplication(sk2,sk1),
inference(orient,[status(thm)],[t55106]) ).
cnf(c24,plain,
multiplication(sk1,sk2) != multiplication(sk2,sk1),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(goal_0,negated_conjecture,
multiplication(sk2,sk1) != multiplication(sk1,sk2),
inference(equality_encoding,[status(esa)],[c24]) ).
cnf(g0_0,plain,
multiplication(sk2,sk1) != multiplication(sk2,sk1),
inference(rw,[status(thm)],[goal_0,t53825]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KLE012+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n018.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 18:38:03 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 47.96/6.43 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 47.96/6.43 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------