%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ALG010-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 12:51:10 PM UTC 2026
% Result : Unsatisfiable 22.50s 3.52s
% Output : Proof 22.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 77
% Number of leaves : 17
% Syntax : Number of formulae : 388 ( 384 unt; 0 def)
% Number of atoms : 396 ( 395 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 29 ( 21 ~; 8 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 11 con; 0-4 aty)
% Number of variables : 254 ( 11 sgn 28 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(t8,axiom,
sFlat0 = multiply(b,a),
introduced(definition) ).
cnf(t123,plain,
multiply(b,a) = sFlat0,
inference(orient,[status(thm)],[t8]) ).
cnf(t9,axiom,
sFlat1 = multiply(multiply(b,a),a),
introduced(definition) ).
cnf(t106,plain,
multiply(multiply(b,a),a) = sFlat1,
inference(orient,[status(thm)],[t9]) ).
cnf(t12336,plain,
multiply(sFlat0,a) = sFlat1,
inference(step,[status(thm)],[t106,t123]) ).
cnf(t129,plain,
multiply(sFlat0,a) = sFlat1,
inference(rw,[status(thm)],[t12336]) ).
cnf(t160,plain,
multiply(sFlat0,a) = sFlat1,
inference(orient,[status(thm)],[t129]) ).
cnf(t10,axiom,
sFlat2 = multiply(multiply(multiply(b,a),a),b),
introduced(definition) ).
cnf(t86,plain,
multiply(multiply(multiply(b,a),a),b) = sFlat2,
inference(orient,[status(thm)],[t10]) ).
cnf(t12334,plain,
multiply(sFlat1,b) = sFlat2,
inference(step,[status(thm)],[t86,t106]) ).
cnf(t114,plain,
multiply(sFlat1,b) = sFlat2,
inference(rw,[status(thm)],[t12334]) ).
cnf(t148,plain,
multiply(sFlat1,b) = sFlat2,
inference(orient,[status(thm)],[t114]) ).
cnf(t11,axiom,
sFlat3 = multiply(multiply(multiply(multiply(b,a),a),b),b),
introduced(definition) ).
cnf(t67,plain,
multiply(multiply(multiply(multiply(b,a),a),b),b) = sFlat3,
inference(orient,[status(thm)],[t11]) ).
cnf(t12332,plain,
multiply(sFlat2,b) = sFlat3,
inference(step,[status(thm)],[t67,t86]) ).
cnf(t95,plain,
multiply(sFlat2,b) = sFlat3,
inference(rw,[status(thm)],[t12332]) ).
cnf(t136,plain,
multiply(sFlat2,b) = sFlat3,
inference(orient,[status(thm)],[t95]) ).
cnf(t12,axiom,
sFlat4 = multiply(a,b),
introduced(definition) ).
cnf(t115,plain,
multiply(a,b) = sFlat4,
inference(orient,[status(thm)],[t12]) ).
cnf(t13,axiom,
sFlat5 = multiply(multiply(a,b),b),
introduced(definition) ).
cnf(t96,plain,
multiply(multiply(a,b),b) = sFlat5,
inference(orient,[status(thm)],[t13]) ).
cnf(t12335,plain,
multiply(sFlat4,b) = sFlat5,
inference(step,[status(thm)],[t96,t115]) ).
cnf(t122,plain,
multiply(sFlat4,b) = sFlat5,
inference(rw,[status(thm)],[t12335]) ).
cnf(t154,plain,
multiply(sFlat4,b) = sFlat5,
inference(orient,[status(thm)],[t122]) ).
cnf(t14,axiom,
sFlat6 = multiply(multiply(multiply(a,b),b),a),
introduced(definition) ).
cnf(t76,plain,
multiply(multiply(multiply(a,b),b),a) = sFlat6,
inference(orient,[status(thm)],[t14]) ).
cnf(t12333,plain,
multiply(sFlat5,a) = sFlat6,
inference(step,[status(thm)],[t76,t96]) ).
cnf(t105,plain,
multiply(sFlat5,a) = sFlat6,
inference(rw,[status(thm)],[t12333]) ).
cnf(t142,plain,
multiply(sFlat5,a) = sFlat6,
inference(orient,[status(thm)],[t105]) ).
cnf(t15,axiom,
sFlat7 = multiply(multiply(multiply(multiply(a,b),b),a),a),
introduced(definition) ).
cnf(t58,plain,
multiply(multiply(multiply(multiply(a,b),b),a),a) = sFlat7,
inference(orient,[status(thm)],[t15]) ).
cnf(t12331,plain,
multiply(sFlat6,a) = sFlat7,
inference(step,[status(thm)],[t58,t76]) ).
cnf(t85,plain,
multiply(sFlat6,a) = sFlat7,
inference(rw,[status(thm)],[t12331]) ).
cnf(t130,plain,
multiply(sFlat6,a) = sFlat7,
inference(orient,[status(thm)],[t85]) ).
cnf(f3,axiom,
( A = B
| multiply(B,A) != one
| multiply(A,B) != one ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m7) ).
fof(f3_nnf,plain,
! [A,B] :
( A = B
| multiply(B,A) != one
| multiply(A,B) != one ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A,B] :
( A = B
| multiply(B,A) != one
| multiply(A,B) != one ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( X0 = X1
| multiply(X1,X0) != one
| multiply(X0,X1) != one ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t6,plain,
ifeq(multiply(X1,X2),one,ifeq(multiply(X2,X1),one,X1,X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t18,plain,
ifeq(multiply(X1,X2),one,ifeq(multiply(X2,X1),one,X1,X2),X2) = X2,
inference(orient,[status(thm)],[t6]) ).
cnf(f5,axiom,
multiply(A,multiply(B,C)) = multiply(B,multiply(A,C)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m9) ).
fof(f5_nnf,plain,
! [A,B,C] : multiply(A,multiply(B,C)) = multiply(B,multiply(A,C)),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [A,B,C] : multiply(A,multiply(B,C)) = multiply(B,multiply(A,C)),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
multiply(X0,multiply(X1,X2)) = multiply(X1,multiply(X0,X2)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t4,plain,
multiply(X1,multiply(X2,X3)) = multiply(X2,multiply(X1,X3)),
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t22,plain,
multiply(X1,multiply(X2,X3)) = multiply(X2,multiply(X1,X3)),
inference(orient,[status(thm)],[t4]) ).
cnf(f6,axiom,
multiply(multiply(A,B),multiply(A,C)) = multiply(multiply(B,A),multiply(B,C)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',h) ).
fof(f6_nnf,plain,
! [A,B,C] : multiply(multiply(A,B),multiply(A,C)) = multiply(multiply(B,A),multiply(B,C)),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [A,B,C] : multiply(multiply(A,B),multiply(A,C)) = multiply(multiply(B,A),multiply(B,C)),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
multiply(multiply(X0,X1),multiply(X0,X2)) = multiply(multiply(X1,X0),multiply(X1,X2)),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t7,plain,
multiply(multiply(X1,X2),multiply(X1,X3)) = multiply(multiply(X2,X1),multiply(X2,X3)),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t12328,plain,
multiply(X1,multiply(multiply(X1,X2),X3)) = multiply(multiply(X2,X1),multiply(X2,X3)),
inference(step,[status(thm)],[t7,t22]) ).
cnf(t12329,plain,
multiply(X1,multiply(multiply(X1,X2),X3)) = multiply(X2,multiply(multiply(X2,X1),X3)),
inference(step,[status(thm)],[t12328,t22]) ).
cnf(t31,plain,
multiply(X1,multiply(multiply(X1,X2),X3)) = multiply(X2,multiply(multiply(X2,X1),X3)),
inference(orient,[status(thm)],[t12329]) ).
cnf(f2,axiom,
multiply(multiply(A,B),multiply(multiply(C,A),multiply(C,B))) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m5) ).
fof(f2_nnf,plain,
! [A,B,C] : multiply(multiply(A,B),multiply(multiply(C,A),multiply(C,B))) = one,
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A,B,C] : multiply(multiply(A,B),multiply(multiply(C,A),multiply(C,B))) = one,
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
multiply(multiply(X0,X1),multiply(multiply(X2,X0),multiply(X2,X1))) = one,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t5,plain,
multiply(multiply(X1,X2),multiply(multiply(X3,X1),multiply(X3,X2))) = one,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t12330,plain,
multiply(multiply(X1,X2),multiply(X3,multiply(multiply(X3,X1),X2))) = one,
inference(step,[status(thm)],[t5,t22]) ).
cnf(t39,plain,
multiply(multiply(X1,X2),multiply(X3,multiply(multiply(X3,X1),X2))) = one,
inference(orient,[status(thm)],[t12330]) ).
cnf(f1,axiom,
multiply(one,A) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m4) ).
fof(f1_nnf,plain,
! [A] : multiply(one,A) = A,
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A] : multiply(one,A) = A,
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
multiply(one,X0) = X0,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t2,plain,
multiply(one,X1) = X1,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t16,plain,
multiply(one,X1) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t43,plain,
one = multiply(X1,multiply(X2,multiply(multiply(X2,one),X1))),
inference(cp,[status(thm)],[t39,t16]) ).
cnf(f0,axiom,
multiply(A,one) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m3) ).
fof(f0_nnf,plain,
! [A] : multiply(A,one) = one,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A] : multiply(A,one) = one,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
multiply(X0,one) = one,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t1,plain,
multiply(X1,one) = one,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t28,plain,
multiply(X1,one) = one,
inference(orient,[status(thm)],[t1]) ).
cnf(t12341,plain,
one = multiply(X1,multiply(X2,multiply(one,X1))),
inference(step,[status(thm)],[t43,t28]) ).
cnf(t12342,plain,
one = multiply(X1,multiply(X2,X1)),
inference(step,[status(thm)],[t12341,t16]) ).
cnf(t168,plain,
multiply(X1,multiply(X2,X1)) = one,
inference(orient,[status(thm)],[t12342]) ).
cnf(t177,plain,
one = multiply(b,sFlat4),
inference(cp,[status(thm)],[t168,t115]) ).
cnf(t235,plain,
multiply(b,sFlat4) = one,
inference(orient,[status(thm)],[t177]) ).
cnf(t241,plain,
multiply(sFlat4,multiply(multiply(sFlat4,b),X1)) = multiply(b,multiply(one,X1)),
inference(cp,[status(thm)],[t31,t235]) ).
cnf(t12406,plain,
multiply(sFlat4,multiply(sFlat5,X1)) = multiply(b,multiply(one,X1)),
inference(step,[status(thm)],[t241,t154]) ).
cnf(t12407,plain,
multiply(sFlat4,multiply(sFlat5,X1)) = multiply(one,multiply(b,X1)),
inference(step,[status(thm)],[t12406,t22]) ).
cnf(t12408,plain,
multiply(sFlat4,multiply(sFlat5,X1)) = multiply(b,X1),
inference(step,[status(thm)],[t12407,t16]) ).
cnf(t686,plain,
multiply(sFlat4,multiply(sFlat5,X1)) = multiply(b,X1),
inference(orient,[status(thm)],[t12408]) ).
cnf(f4,axiom,
multiply(A,A) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m8) ).
fof(f4_nnf,plain,
! [A] : multiply(A,A) = one,
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [A] : multiply(A,A) = one,
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
multiply(X0,X0) = one,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t0,plain,
multiply(X1,X1) = one,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t21,plain,
multiply(X1,X1) = one,
inference(orient,[status(thm)],[t0]) ).
cnf(t23,plain,
multiply(X1,multiply(multiply(X1,X2),X2)) = one,
inference(cp,[status(thm)],[t22,t21]) ).
cnf(t325,plain,
multiply(X1,multiply(multiply(X1,X2),X2)) = one,
inference(orient,[status(thm)],[t23]) ).
cnf(t330,plain,
one = multiply(sFlat5,multiply(sFlat6,a)),
inference(cp,[status(thm)],[t325,t142]) ).
cnf(t12369,plain,
one = multiply(sFlat5,sFlat7),
inference(step,[status(thm)],[t330,t130]) ).
cnf(t349,plain,
multiply(sFlat5,sFlat7) = one,
inference(orient,[status(thm)],[t12369]) ).
cnf(t692,plain,
multiply(b,sFlat7) = multiply(sFlat4,one),
inference(cp,[status(thm)],[t686,t349]) ).
cnf(t128,plain,
multiply(b,multiply(X1,a)) = multiply(X1,sFlat0),
inference(cp,[status(thm)],[t22,t123]) ).
cnf(t449,plain,
multiply(b,multiply(X1,a)) = multiply(X1,sFlat0),
inference(orient,[status(thm)],[t128]) ).
cnf(t452,plain,
multiply(sFlat6,sFlat0) = multiply(b,sFlat7),
inference(cp,[status(thm)],[t449,t130]) ).
cnf(t470,plain,
multiply(b,sFlat7) = multiply(sFlat6,sFlat0),
inference(orient,[status(thm)],[t452]) ).
cnf(t12410,plain,
multiply(sFlat6,sFlat0) = multiply(sFlat4,one),
inference(step,[status(thm)],[t692,t470]) ).
cnf(t12411,plain,
multiply(sFlat6,sFlat0) = one,
inference(step,[status(thm)],[t12410,t28]) ).
cnf(t711,plain,
multiply(sFlat6,sFlat0) = one,
inference(orient,[status(thm)],[t12411]) ).
cnf(t719,plain,
multiply(sFlat0,multiply(multiply(sFlat0,sFlat6),X1)) = multiply(sFlat6,multiply(one,X1)),
inference(cp,[status(thm)],[t31,t711]) ).
cnf(t12695,plain,
multiply(sFlat0,multiply(multiply(sFlat0,sFlat6),X1)) = multiply(sFlat6,X1),
inference(step,[status(thm)],[t719,t16]) ).
cnf(t7079,plain,
multiply(sFlat0,multiply(multiply(sFlat0,sFlat6),X1)) = multiply(sFlat6,X1),
inference(orient,[status(thm)],[t12695]) ).
cnf(t165,plain,
multiply(sFlat0,multiply(X1,a)) = multiply(X1,sFlat1),
inference(cp,[status(thm)],[t22,t160]) ).
cnf(t609,plain,
multiply(sFlat0,multiply(X1,a)) = multiply(X1,sFlat1),
inference(orient,[status(thm)],[t165]) ).
cnf(t7082,plain,
multiply(sFlat6,a) = multiply(multiply(sFlat0,sFlat6),sFlat1),
inference(cp,[status(thm)],[t7079,t609]) ).
cnf(t12699,plain,
sFlat7 = multiply(multiply(sFlat0,sFlat6),sFlat1),
inference(step,[status(thm)],[t7082,t130]) ).
cnf(t7183,plain,
multiply(multiply(sFlat0,sFlat6),sFlat1) = sFlat7,
inference(orient,[status(thm)],[t12699]) ).
cnf(t7198,plain,
multiply(multiply(sFlat0,sFlat6),multiply(X1,sFlat1)) = multiply(X1,sFlat7),
inference(cp,[status(thm)],[t22,t7183]) ).
cnf(t9150,plain,
multiply(multiply(sFlat0,sFlat6),multiply(X1,sFlat1)) = multiply(X1,sFlat7),
inference(orient,[status(thm)],[t7198]) ).
cnf(t141,plain,
multiply(sFlat2,multiply(X1,b)) = multiply(X1,sFlat3),
inference(cp,[status(thm)],[t22,t136]) ).
cnf(t519,plain,
multiply(sFlat2,multiply(X1,b)) = multiply(X1,sFlat3),
inference(orient,[status(thm)],[t141]) ).
cnf(t120,plain,
multiply(a,multiply(X1,b)) = multiply(X1,sFlat4),
inference(cp,[status(thm)],[t22,t115]) ).
cnf(t306,plain,
multiply(a,multiply(X1,b)) = multiply(X1,sFlat4),
inference(orient,[status(thm)],[t120]) ).
cnf(t308,plain,
multiply(sFlat4,sFlat4) = multiply(a,sFlat5),
inference(cp,[status(thm)],[t306,t154]) ).
cnf(t12367,plain,
one = multiply(a,sFlat5),
inference(step,[status(thm)],[t308,t21]) ).
cnf(t318,plain,
multiply(a,sFlat5) = one,
inference(orient,[status(thm)],[t12367]) ).
cnf(t322,plain,
one = multiply(multiply(sFlat5,X1),multiply(a,multiply(one,X1))),
inference(cp,[status(thm)],[t39,t318]) ).
cnf(t12483,plain,
one = multiply(a,multiply(multiply(sFlat5,X1),multiply(one,X1))),
inference(step,[status(thm)],[t322,t22]) ).
cnf(t12484,plain,
one = multiply(a,multiply(one,multiply(multiply(sFlat5,X1),X1))),
inference(step,[status(thm)],[t12483,t22]) ).
cnf(t12485,plain,
one = multiply(a,multiply(multiply(sFlat5,X1),X1)),
inference(step,[status(thm)],[t12484,t16]) ).
cnf(t1965,plain,
multiply(a,multiply(multiply(sFlat5,X1),X1)) = one,
inference(orient,[status(thm)],[t12485]) ).
cnf(t1966,plain,
one = multiply(multiply(sFlat5,b),sFlat4),
inference(cp,[status(thm)],[t1965,t306]) ).
cnf(t1988,plain,
multiply(multiply(sFlat5,b),sFlat4) = one,
inference(orient,[status(thm)],[t1966]) ).
cnf(t1989,plain,
sFlat4 = ifeq(one,one,ifeq(multiply(sFlat4,multiply(sFlat5,b)),one,multiply(sFlat5,b),sFlat4),sFlat4),
inference(cp,[status(thm)],[t18,t1988]) ).
cnf(t3,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t17,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t3]) ).
cnf(t12486,plain,
sFlat4 = ifeq(multiply(sFlat4,multiply(sFlat5,b)),one,multiply(sFlat5,b),sFlat4),
inference(step,[status(thm)],[t1989,t17]) ).
cnf(t328,plain,
one = multiply(sFlat4,multiply(sFlat5,b)),
inference(cp,[status(thm)],[t325,t154]) ).
cnf(t395,plain,
multiply(sFlat4,multiply(sFlat5,b)) = one,
inference(orient,[status(thm)],[t328]) ).
cnf(t12487,plain,
sFlat4 = ifeq(one,one,multiply(sFlat5,b),sFlat4),
inference(step,[status(thm)],[t12486,t395]) ).
cnf(t12488,plain,
sFlat4 = multiply(sFlat5,b),
inference(step,[status(thm)],[t12487,t17]) ).
cnf(t2004,plain,
multiply(sFlat5,b) = sFlat4,
inference(orient,[status(thm)],[t12488]) ).
cnf(t2006,plain,
multiply(sFlat5,sFlat3) = multiply(sFlat2,sFlat4),
inference(cp,[status(thm)],[t519,t2004]) ).
cnf(t176,plain,
one = multiply(a,sFlat0),
inference(cp,[status(thm)],[t168,t123]) ).
cnf(t228,plain,
multiply(a,sFlat0) = one,
inference(orient,[status(thm)],[t176]) ).
cnf(t234,plain,
multiply(sFlat0,multiply(multiply(sFlat0,a),X1)) = multiply(a,multiply(one,X1)),
inference(cp,[status(thm)],[t31,t228]) ).
cnf(t12396,plain,
multiply(sFlat0,multiply(sFlat1,X1)) = multiply(a,multiply(one,X1)),
inference(step,[status(thm)],[t234,t160]) ).
cnf(t12397,plain,
multiply(sFlat0,multiply(sFlat1,X1)) = multiply(one,multiply(a,X1)),
inference(step,[status(thm)],[t12396,t22]) ).
cnf(t12398,plain,
multiply(sFlat0,multiply(sFlat1,X1)) = multiply(a,X1),
inference(step,[status(thm)],[t12397,t16]) ).
cnf(t641,plain,
multiply(sFlat0,multiply(sFlat1,X1)) = multiply(a,X1),
inference(orient,[status(thm)],[t12398]) ).
cnf(t329,plain,
one = multiply(sFlat1,multiply(sFlat2,b)),
inference(cp,[status(thm)],[t325,t148]) ).
cnf(t12368,plain,
one = multiply(sFlat1,sFlat3),
inference(step,[status(thm)],[t329,t136]) ).
cnf(t343,plain,
multiply(sFlat1,sFlat3) = one,
inference(orient,[status(thm)],[t12368]) ).
cnf(t646,plain,
multiply(a,sFlat3) = multiply(sFlat0,one),
inference(cp,[status(thm)],[t641,t343]) ).
cnf(t310,plain,
multiply(sFlat2,sFlat4) = multiply(a,sFlat3),
inference(cp,[status(thm)],[t306,t136]) ).
cnf(t371,plain,
multiply(a,sFlat3) = multiply(sFlat2,sFlat4),
inference(orient,[status(thm)],[t310]) ).
cnf(t12400,plain,
multiply(sFlat2,sFlat4) = multiply(sFlat0,one),
inference(step,[status(thm)],[t646,t371]) ).
cnf(t12401,plain,
multiply(sFlat2,sFlat4) = one,
inference(step,[status(thm)],[t12400,t28]) ).
cnf(t664,plain,
multiply(sFlat2,sFlat4) = one,
inference(orient,[status(thm)],[t12401]) ).
cnf(t12491,plain,
multiply(sFlat5,sFlat3) = one,
inference(step,[status(thm)],[t2006,t664]) ).
cnf(t2022,plain,
multiply(sFlat5,sFlat3) = one,
inference(orient,[status(thm)],[t12491]) ).
cnf(t2035,plain,
multiply(sFlat3,multiply(multiply(sFlat3,sFlat5),X1)) = multiply(sFlat5,multiply(one,X1)),
inference(cp,[status(thm)],[t31,t2022]) ).
cnf(t159,plain,
multiply(sFlat4,multiply(X1,b)) = multiply(X1,sFlat5),
inference(cp,[status(thm)],[t22,t154]) ).
cnf(t599,plain,
multiply(sFlat4,multiply(X1,b)) = multiply(X1,sFlat5),
inference(orient,[status(thm)],[t159]) ).
cnf(t347,plain,
one = multiply(multiply(sFlat3,X1),multiply(sFlat1,multiply(one,X1))),
inference(cp,[status(thm)],[t39,t343]) ).
cnf(t12507,plain,
one = multiply(sFlat1,multiply(multiply(sFlat3,X1),multiply(one,X1))),
inference(step,[status(thm)],[t347,t22]) ).
cnf(t12508,plain,
one = multiply(sFlat1,multiply(one,multiply(multiply(sFlat3,X1),X1))),
inference(step,[status(thm)],[t12507,t22]) ).
cnf(t12509,plain,
one = multiply(sFlat1,multiply(multiply(sFlat3,X1),X1)),
inference(step,[status(thm)],[t12508,t16]) ).
cnf(t2254,plain,
multiply(sFlat1,multiply(multiply(sFlat3,X1),X1)) = one,
inference(orient,[status(thm)],[t12509]) ).
cnf(t153,plain,
multiply(sFlat1,multiply(X1,b)) = multiply(X1,sFlat2),
inference(cp,[status(thm)],[t22,t148]) ).
cnf(t579,plain,
multiply(sFlat1,multiply(X1,b)) = multiply(X1,sFlat2),
inference(orient,[status(thm)],[t153]) ).
cnf(t2255,plain,
one = multiply(multiply(sFlat3,b),sFlat2),
inference(cp,[status(thm)],[t2254,t579]) ).
cnf(t2282,plain,
multiply(multiply(sFlat3,b),sFlat2) = one,
inference(orient,[status(thm)],[t2255]) ).
cnf(t2284,plain,
sFlat2 = ifeq(one,one,ifeq(multiply(sFlat2,multiply(sFlat3,b)),one,multiply(sFlat3,b),sFlat2),sFlat2),
inference(cp,[status(thm)],[t18,t2282]) ).
cnf(t12510,plain,
sFlat2 = ifeq(multiply(sFlat2,multiply(sFlat3,b)),one,multiply(sFlat3,b),sFlat2),
inference(step,[status(thm)],[t2284,t17]) ).
cnf(t331,plain,
one = multiply(sFlat2,multiply(sFlat3,b)),
inference(cp,[status(thm)],[t325,t136]) ).
cnf(t401,plain,
multiply(sFlat2,multiply(sFlat3,b)) = one,
inference(orient,[status(thm)],[t331]) ).
cnf(t12511,plain,
sFlat2 = ifeq(one,one,multiply(sFlat3,b),sFlat2),
inference(step,[status(thm)],[t12510,t401]) ).
cnf(t12512,plain,
sFlat2 = multiply(sFlat3,b),
inference(step,[status(thm)],[t12511,t17]) ).
cnf(t2299,plain,
multiply(sFlat3,b) = sFlat2,
inference(orient,[status(thm)],[t12512]) ).
cnf(t2301,plain,
multiply(sFlat3,sFlat5) = multiply(sFlat4,sFlat2),
inference(cp,[status(thm)],[t599,t2299]) ).
cnf(t581,plain,
multiply(sFlat4,sFlat2) = multiply(sFlat1,sFlat5),
inference(cp,[status(thm)],[t579,t154]) ).
cnf(t590,plain,
multiply(sFlat4,sFlat2) = multiply(sFlat1,sFlat5),
inference(orient,[status(thm)],[t581]) ).
cnf(t12516,plain,
multiply(sFlat3,sFlat5) = multiply(sFlat1,sFlat5),
inference(step,[status(thm)],[t2301,t590]) ).
cnf(t2333,plain,
multiply(sFlat3,sFlat5) = multiply(sFlat1,sFlat5),
inference(orient,[status(thm)],[t12516]) ).
cnf(t12709,plain,
multiply(sFlat3,multiply(multiply(sFlat1,sFlat5),X1)) = multiply(sFlat5,multiply(one,X1)),
inference(step,[status(thm)],[t2035,t2333]) ).
cnf(t12710,plain,
multiply(sFlat3,multiply(multiply(sFlat1,sFlat5),X1)) = multiply(sFlat5,X1),
inference(step,[status(thm)],[t12709,t16]) ).
cnf(t7261,plain,
multiply(sFlat3,multiply(multiply(sFlat1,sFlat5),X1)) = multiply(sFlat5,X1),
inference(orient,[status(thm)],[t12710]) ).
cnf(t34,plain,
multiply(multiply(X1,X2),multiply(multiply(multiply(X1,X2),X3),Y3)) = multiply(X3,multiply(multiply(X1,multiply(X3,X2)),Y3)),
inference(cp,[status(thm)],[t31,t22]) ).
cnf(t5732,plain,
multiply(multiply(X1,X2),multiply(multiply(multiply(X1,X2),X3),Y3)) = multiply(X3,multiply(multiply(X1,multiply(X3,X2)),Y3)),
inference(orient,[status(thm)],[t34]) ).
cnf(t2316,plain,
multiply(sFlat3,multiply(X1,b)) = multiply(X1,sFlat2),
inference(cp,[status(thm)],[t22,t2299]) ).
cnf(t2365,plain,
multiply(sFlat3,multiply(X1,b)) = multiply(X1,sFlat2),
inference(orient,[status(thm)],[t2316]) ).
cnf(t7263,plain,
multiply(sFlat5,b) = multiply(multiply(sFlat1,sFlat5),sFlat2),
inference(cp,[status(thm)],[t7261,t2365]) ).
cnf(t12711,plain,
sFlat4 = multiply(multiply(sFlat1,sFlat5),sFlat2),
inference(step,[status(thm)],[t7263,t2004]) ).
cnf(t7313,plain,
multiply(multiply(sFlat1,sFlat5),sFlat2) = sFlat4,
inference(orient,[status(thm)],[t12711]) ).
cnf(t7339,plain,
multiply(sFlat2,multiply(multiply(sFlat1,multiply(sFlat2,sFlat5)),X1)) = multiply(multiply(sFlat1,sFlat5),multiply(sFlat4,X1)),
inference(cp,[status(thm)],[t5732,t7313]) ).
cnf(t348,plain,
multiply(sFlat1,multiply(X1,sFlat3)) = multiply(X1,one),
inference(cp,[status(thm)],[t22,t343]) ).
cnf(t12376,plain,
multiply(sFlat1,multiply(X1,sFlat3)) = one,
inference(step,[status(thm)],[t348,t28]) ).
cnf(t413,plain,
multiply(sFlat1,multiply(X1,sFlat3)) = one,
inference(orient,[status(thm)],[t12376]) ).
cnf(t521,plain,
multiply(sFlat4,sFlat3) = multiply(sFlat2,sFlat5),
inference(cp,[status(thm)],[t519,t154]) ).
cnf(t530,plain,
multiply(sFlat4,sFlat3) = multiply(sFlat2,sFlat5),
inference(orient,[status(thm)],[t521]) ).
cnf(t532,plain,
one = multiply(sFlat1,multiply(sFlat2,sFlat5)),
inference(cp,[status(thm)],[t413,t530]) ).
cnf(t546,plain,
multiply(sFlat1,multiply(sFlat2,sFlat5)) = one,
inference(orient,[status(thm)],[t532]) ).
cnf(t12788,plain,
multiply(sFlat2,multiply(one,X1)) = multiply(multiply(sFlat1,sFlat5),multiply(sFlat4,X1)),
inference(step,[status(thm)],[t7339,t546]) ).
cnf(t12789,plain,
multiply(sFlat2,X1) = multiply(multiply(sFlat1,sFlat5),multiply(sFlat4,X1)),
inference(step,[status(thm)],[t12788,t16]) ).
cnf(t12790,plain,
multiply(sFlat2,X1) = multiply(sFlat4,multiply(multiply(sFlat1,sFlat5),X1)),
inference(step,[status(thm)],[t12789,t22]) ).
cnf(t9802,plain,
multiply(sFlat4,multiply(multiply(sFlat1,sFlat5),X1)) = multiply(sFlat2,X1),
inference(orient,[status(thm)],[t12790]) ).
cnf(t670,plain,
one = multiply(multiply(sFlat4,X1),multiply(sFlat2,multiply(one,X1))),
inference(cp,[status(thm)],[t39,t664]) ).
cnf(t27,plain,
multiply(X1,multiply(X2,multiply(X3,Y3))) = multiply(X2,multiply(X3,multiply(X1,Y3))),
inference(cp,[status(thm)],[t22,t22]) ).
cnf(t2652,plain,
multiply(X1,multiply(X2,multiply(X3,Y3))) = multiply(X2,multiply(X3,multiply(X1,Y3))),
inference(orient,[status(thm)],[t27]) ).
cnf(t12597,plain,
one = multiply(one,multiply(multiply(sFlat4,X1),multiply(sFlat2,X1))),
inference(step,[status(thm)],[t670,t2652]) ).
cnf(t12598,plain,
one = multiply(multiply(sFlat4,X1),multiply(sFlat2,X1)),
inference(step,[status(thm)],[t12597,t16]) ).
cnf(t12599,plain,
one = multiply(sFlat2,multiply(multiply(sFlat4,X1),X1)),
inference(step,[status(thm)],[t12598,t22]) ).
cnf(t3909,plain,
multiply(sFlat2,multiply(multiply(sFlat4,X1),X1)) = one,
inference(orient,[status(thm)],[t12599]) ).
cnf(t333,plain,
one = multiply(b,multiply(sFlat0,a)),
inference(cp,[status(thm)],[t325,t123]) ).
cnf(t12370,plain,
one = multiply(b,sFlat1),
inference(step,[status(thm)],[t333,t160]) ).
cnf(t355,plain,
multiply(b,sFlat1) = one,
inference(orient,[status(thm)],[t12370]) ).
cnf(t359,plain,
one = multiply(multiply(sFlat1,X1),multiply(b,multiply(one,X1))),
inference(cp,[status(thm)],[t39,t355]) ).
cnf(t12540,plain,
one = multiply(b,multiply(multiply(sFlat1,X1),multiply(one,X1))),
inference(step,[status(thm)],[t359,t22]) ).
cnf(t12541,plain,
one = multiply(b,multiply(one,multiply(multiply(sFlat1,X1),X1))),
inference(step,[status(thm)],[t12540,t22]) ).
cnf(t12542,plain,
one = multiply(b,multiply(multiply(sFlat1,X1),X1)),
inference(step,[status(thm)],[t12541,t16]) ).
cnf(t2578,plain,
multiply(b,multiply(multiply(sFlat1,X1),X1)) = one,
inference(orient,[status(thm)],[t12542]) ).
cnf(t2579,plain,
one = multiply(multiply(sFlat1,a),sFlat0),
inference(cp,[status(thm)],[t2578,t449]) ).
cnf(t2601,plain,
multiply(multiply(sFlat1,a),sFlat0) = one,
inference(orient,[status(thm)],[t2579]) ).
cnf(t2602,plain,
sFlat0 = ifeq(one,one,ifeq(multiply(sFlat0,multiply(sFlat1,a)),one,multiply(sFlat1,a),sFlat0),sFlat0),
inference(cp,[status(thm)],[t18,t2601]) ).
cnf(t12543,plain,
sFlat0 = ifeq(multiply(sFlat0,multiply(sFlat1,a)),one,multiply(sFlat1,a),sFlat0),
inference(step,[status(thm)],[t2602,t17]) ).
cnf(t327,plain,
one = multiply(sFlat0,multiply(sFlat1,a)),
inference(cp,[status(thm)],[t325,t160]) ).
cnf(t389,plain,
multiply(sFlat0,multiply(sFlat1,a)) = one,
inference(orient,[status(thm)],[t327]) ).
cnf(t12544,plain,
sFlat0 = ifeq(one,one,multiply(sFlat1,a),sFlat0),
inference(step,[status(thm)],[t12543,t389]) ).
cnf(t12545,plain,
sFlat0 = multiply(sFlat1,a),
inference(step,[status(thm)],[t12544,t17]) ).
cnf(t2617,plain,
multiply(sFlat1,a) = sFlat0,
inference(orient,[status(thm)],[t12545]) ).
cnf(t2636,plain,
multiply(sFlat1,multiply(X1,a)) = multiply(X1,sFlat0),
inference(cp,[status(thm)],[t22,t2617]) ).
cnf(t3258,plain,
multiply(sFlat1,multiply(X1,a)) = multiply(X1,sFlat0),
inference(orient,[status(thm)],[t2636]) ).
cnf(t361,plain,
multiply(sFlat1,multiply(multiply(sFlat1,b),X1)) = multiply(b,multiply(one,X1)),
inference(cp,[status(thm)],[t31,t355]) ).
cnf(t12419,plain,
multiply(sFlat1,multiply(sFlat2,X1)) = multiply(b,multiply(one,X1)),
inference(step,[status(thm)],[t361,t148]) ).
cnf(t12420,plain,
multiply(sFlat1,multiply(sFlat2,X1)) = multiply(one,multiply(b,X1)),
inference(step,[status(thm)],[t12419,t22]) ).
cnf(t12421,plain,
multiply(sFlat1,multiply(sFlat2,X1)) = multiply(b,X1),
inference(step,[status(thm)],[t12420,t16]) ).
cnf(t959,plain,
multiply(sFlat1,multiply(sFlat2,X1)) = multiply(b,X1),
inference(orient,[status(thm)],[t12421]) ).
cnf(t3259,plain,
multiply(sFlat2,sFlat0) = multiply(b,a),
inference(cp,[status(thm)],[t3258,t959]) ).
cnf(t12559,plain,
multiply(sFlat2,sFlat0) = sFlat0,
inference(step,[status(thm)],[t3259,t123]) ).
cnf(t3282,plain,
multiply(sFlat2,sFlat0) = sFlat0,
inference(orient,[status(thm)],[t12559]) ).
cnf(t3292,plain,
multiply(sFlat2,multiply(X1,sFlat0)) = multiply(X1,sFlat0),
inference(cp,[status(thm)],[t22,t3282]) ).
cnf(t3296,plain,
multiply(sFlat2,multiply(X1,sFlat0)) = multiply(X1,sFlat0),
inference(orient,[status(thm)],[t3292]) ).
cnf(t3910,plain,
one = multiply(multiply(sFlat4,sFlat0),sFlat0),
inference(cp,[status(thm)],[t3909,t3296]) ).
cnf(t3952,plain,
multiply(multiply(sFlat4,sFlat0),sFlat0) = one,
inference(orient,[status(thm)],[t3910]) ).
cnf(t3953,plain,
sFlat0 = ifeq(one,one,ifeq(multiply(sFlat0,multiply(sFlat4,sFlat0)),one,multiply(sFlat4,sFlat0),sFlat0),sFlat0),
inference(cp,[status(thm)],[t18,t3952]) ).
cnf(t12600,plain,
sFlat0 = ifeq(multiply(sFlat0,multiply(sFlat4,sFlat0)),one,multiply(sFlat4,sFlat0),sFlat0),
inference(step,[status(thm)],[t3953,t17]) ).
cnf(t3293,plain,
multiply(sFlat0,multiply(multiply(sFlat0,sFlat2),X1)) = multiply(sFlat2,multiply(sFlat0,X1)),
inference(cp,[status(thm)],[t31,t3282]) ).
cnf(t645,plain,
multiply(a,b) = multiply(sFlat0,sFlat2),
inference(cp,[status(thm)],[t641,t148]) ).
cnf(t12399,plain,
sFlat4 = multiply(sFlat0,sFlat2),
inference(step,[status(thm)],[t645,t115]) ).
cnf(t657,plain,
multiply(sFlat0,sFlat2) = sFlat4,
inference(orient,[status(thm)],[t12399]) ).
cnf(t12562,plain,
multiply(sFlat0,multiply(sFlat4,X1)) = multiply(sFlat2,multiply(sFlat0,X1)),
inference(step,[status(thm)],[t3293,t657]) ).
cnf(t12563,plain,
multiply(sFlat0,multiply(sFlat4,X1)) = multiply(sFlat0,multiply(sFlat2,X1)),
inference(step,[status(thm)],[t12562,t22]) ).
cnf(t3339,plain,
multiply(sFlat0,multiply(sFlat4,X1)) = multiply(sFlat0,multiply(sFlat2,X1)),
inference(orient,[status(thm)],[t12563]) ).
cnf(t12601,plain,
sFlat0 = ifeq(multiply(sFlat0,multiply(sFlat2,sFlat0)),one,multiply(sFlat4,sFlat0),sFlat0),
inference(step,[status(thm)],[t12600,t3339]) ).
cnf(t12602,plain,
sFlat0 = ifeq(one,one,multiply(sFlat4,sFlat0),sFlat0),
inference(step,[status(thm)],[t12601,t168]) ).
cnf(t12603,plain,
sFlat0 = multiply(sFlat4,sFlat0),
inference(step,[status(thm)],[t12602,t17]) ).
cnf(t3970,plain,
multiply(sFlat4,sFlat0) = sFlat0,
inference(orient,[status(thm)],[t12603]) ).
cnf(t3980,plain,
multiply(sFlat4,multiply(X1,sFlat0)) = multiply(X1,sFlat0),
inference(cp,[status(thm)],[t22,t3970]) ).
cnf(t3984,plain,
multiply(sFlat4,multiply(X1,sFlat0)) = multiply(X1,sFlat0),
inference(orient,[status(thm)],[t3980]) ).
cnf(t9803,plain,
multiply(sFlat2,sFlat0) = multiply(multiply(sFlat1,sFlat5),sFlat0),
inference(cp,[status(thm)],[t9802,t3984]) ).
cnf(t12791,plain,
sFlat0 = multiply(multiply(sFlat1,sFlat5),sFlat0),
inference(step,[status(thm)],[t9803,t3282]) ).
cnf(t9867,plain,
multiply(multiply(sFlat1,sFlat5),sFlat0) = sFlat0,
inference(orient,[status(thm)],[t12791]) ).
cnf(t9885,plain,
multiply(sFlat0,multiply(multiply(sFlat0,multiply(sFlat1,sFlat5)),X1)) = multiply(multiply(sFlat1,sFlat5),multiply(sFlat0,X1)),
inference(cp,[status(thm)],[t31,t9867]) ).
cnf(t12868,plain,
multiply(sFlat0,multiply(multiply(a,sFlat5),X1)) = multiply(multiply(sFlat1,sFlat5),multiply(sFlat0,X1)),
inference(step,[status(thm)],[t9885,t641]) ).
cnf(t12869,plain,
multiply(sFlat0,multiply(one,X1)) = multiply(multiply(sFlat1,sFlat5),multiply(sFlat0,X1)),
inference(step,[status(thm)],[t12868,t318]) ).
cnf(t12870,plain,
multiply(sFlat0,X1) = multiply(multiply(sFlat1,sFlat5),multiply(sFlat0,X1)),
inference(step,[status(thm)],[t12869,t16]) ).
cnf(t12871,plain,
multiply(sFlat0,X1) = multiply(sFlat0,multiply(multiply(sFlat1,sFlat5),X1)),
inference(step,[status(thm)],[t12870,t22]) ).
cnf(t12135,plain,
multiply(sFlat0,multiply(multiply(sFlat1,sFlat5),X1)) = multiply(sFlat0,X1),
inference(orient,[status(thm)],[t12871]) ).
cnf(t12136,plain,
multiply(sFlat0,a) = multiply(multiply(sFlat1,sFlat5),sFlat1),
inference(cp,[status(thm)],[t12135,t609]) ).
cnf(t12872,plain,
sFlat1 = multiply(multiply(sFlat1,sFlat5),sFlat1),
inference(step,[status(thm)],[t12136,t160]) ).
cnf(t12198,plain,
multiply(multiply(sFlat1,sFlat5),sFlat1) = sFlat1,
inference(orient,[status(thm)],[t12872]) ).
cnf(t12202,plain,
multiply(sFlat5,sFlat1) = multiply(sFlat3,sFlat1),
inference(cp,[status(thm)],[t7261,t12198]) ).
cnf(t147,plain,
multiply(sFlat5,multiply(X1,a)) = multiply(X1,sFlat6),
inference(cp,[status(thm)],[t22,t142]) ).
cnf(t552,plain,
multiply(sFlat5,multiply(X1,a)) = multiply(X1,sFlat6),
inference(orient,[status(thm)],[t147]) ).
cnf(t554,plain,
multiply(sFlat0,sFlat6) = multiply(sFlat5,sFlat1),
inference(cp,[status(thm)],[t552,t160]) ).
cnf(t563,plain,
multiply(sFlat5,sFlat1) = multiply(sFlat0,sFlat6),
inference(orient,[status(thm)],[t554]) ).
cnf(t12873,plain,
multiply(sFlat0,sFlat6) = multiply(sFlat3,sFlat1),
inference(step,[status(thm)],[t12202,t563]) ).
cnf(t12230,plain,
multiply(sFlat3,sFlat1) = multiply(sFlat0,sFlat6),
inference(orient,[status(thm)],[t12873]) ).
cnf(t12232,plain,
multiply(sFlat3,sFlat7) = multiply(multiply(sFlat0,sFlat6),multiply(sFlat0,sFlat6)),
inference(cp,[status(thm)],[t9150,t12230]) ).
cnf(t643,plain,
multiply(a,multiply(X1,b)) = multiply(sFlat0,multiply(X1,sFlat2)),
inference(cp,[status(thm)],[t641,t579]) ).
cnf(t12422,plain,
multiply(X1,sFlat4) = multiply(sFlat0,multiply(X1,sFlat2)),
inference(step,[status(thm)],[t643,t306]) ).
cnf(t977,plain,
multiply(sFlat0,multiply(X1,sFlat2)) = multiply(X1,sFlat4),
inference(orient,[status(thm)],[t12422]) ).
cnf(t669,plain,
one = multiply(one,multiply(X1,multiply(multiply(X1,sFlat2),sFlat4))),
inference(cp,[status(thm)],[t39,t664]) ).
cnf(t12584,plain,
one = multiply(X1,multiply(multiply(X1,sFlat2),sFlat4)),
inference(step,[status(thm)],[t669,t16]) ).
cnf(t3729,plain,
multiply(X1,multiply(multiply(X1,sFlat2),sFlat4)) = one,
inference(orient,[status(thm)],[t12584]) ).
cnf(t2019,plain,
multiply(sFlat5,multiply(X1,b)) = multiply(X1,sFlat4),
inference(cp,[status(thm)],[t22,t2004]) ).
cnf(t2084,plain,
multiply(sFlat5,multiply(X1,b)) = multiply(X1,sFlat4),
inference(orient,[status(thm)],[t2019]) ).
cnf(t324,plain,
multiply(sFlat5,multiply(multiply(sFlat5,a),X1)) = multiply(a,multiply(one,X1)),
inference(cp,[status(thm)],[t31,t318]) ).
cnf(t12416,plain,
multiply(sFlat5,multiply(sFlat6,X1)) = multiply(a,multiply(one,X1)),
inference(step,[status(thm)],[t324,t142]) ).
cnf(t12417,plain,
multiply(sFlat5,multiply(sFlat6,X1)) = multiply(one,multiply(a,X1)),
inference(step,[status(thm)],[t12416,t22]) ).
cnf(t12418,plain,
multiply(sFlat5,multiply(sFlat6,X1)) = multiply(a,X1),
inference(step,[status(thm)],[t12417,t16]) ).
cnf(t941,plain,
multiply(sFlat5,multiply(sFlat6,X1)) = multiply(a,X1),
inference(orient,[status(thm)],[t12418]) ).
cnf(t2085,plain,
multiply(sFlat6,sFlat4) = multiply(a,b),
inference(cp,[status(thm)],[t2084,t941]) ).
cnf(t12497,plain,
multiply(sFlat6,sFlat4) = sFlat4,
inference(step,[status(thm)],[t2085,t115]) ).
cnf(t2104,plain,
multiply(sFlat6,sFlat4) = sFlat4,
inference(orient,[status(thm)],[t12497]) ).
cnf(t2114,plain,
multiply(sFlat6,multiply(X1,sFlat4)) = multiply(X1,sFlat4),
inference(cp,[status(thm)],[t22,t2104]) ).
cnf(t2116,plain,
multiply(sFlat6,multiply(X1,sFlat4)) = multiply(X1,sFlat4),
inference(orient,[status(thm)],[t2114]) ).
cnf(t3731,plain,
one = multiply(multiply(sFlat6,sFlat2),sFlat4),
inference(cp,[status(thm)],[t3729,t2116]) ).
cnf(t3764,plain,
multiply(multiply(sFlat6,sFlat2),sFlat4) = one,
inference(orient,[status(thm)],[t3731]) ).
cnf(t3765,plain,
sFlat4 = ifeq(one,one,ifeq(multiply(sFlat4,multiply(sFlat6,sFlat2)),one,multiply(sFlat6,sFlat2),sFlat4),sFlat4),
inference(cp,[status(thm)],[t18,t3764]) ).
cnf(t12585,plain,
sFlat4 = ifeq(multiply(sFlat4,multiply(sFlat6,sFlat2)),one,multiply(sFlat6,sFlat2),sFlat4),
inference(step,[status(thm)],[t3765,t17]) ).
cnf(t2115,plain,
multiply(sFlat4,multiply(multiply(sFlat4,sFlat6),X1)) = multiply(sFlat6,multiply(sFlat4,X1)),
inference(cp,[status(thm)],[t31,t2104]) ).
cnf(t691,plain,
multiply(b,a) = multiply(sFlat4,sFlat6),
inference(cp,[status(thm)],[t686,t142]) ).
cnf(t12409,plain,
sFlat0 = multiply(sFlat4,sFlat6),
inference(step,[status(thm)],[t691,t123]) ).
cnf(t703,plain,
multiply(sFlat4,sFlat6) = sFlat0,
inference(orient,[status(thm)],[t12409]) ).
cnf(t12498,plain,
multiply(sFlat4,multiply(sFlat0,X1)) = multiply(sFlat6,multiply(sFlat4,X1)),
inference(step,[status(thm)],[t2115,t703]) ).
cnf(t12499,plain,
multiply(sFlat0,multiply(sFlat4,X1)) = multiply(sFlat6,multiply(sFlat4,X1)),
inference(step,[status(thm)],[t12498,t22]) ).
cnf(t12500,plain,
multiply(sFlat0,multiply(sFlat4,X1)) = multiply(sFlat4,multiply(sFlat6,X1)),
inference(step,[status(thm)],[t12499,t22]) ).
cnf(t2130,plain,
multiply(sFlat4,multiply(sFlat6,X1)) = multiply(sFlat0,multiply(sFlat4,X1)),
inference(orient,[status(thm)],[t12500]) ).
cnf(t12564,plain,
multiply(sFlat4,multiply(sFlat6,X1)) = multiply(sFlat0,multiply(sFlat2,X1)),
inference(step,[status(thm)],[t2130,t3339]) ).
cnf(t3340,plain,
multiply(sFlat4,multiply(sFlat6,X1)) = multiply(sFlat0,multiply(sFlat2,X1)),
inference(orient,[status(thm)],[t12564]) ).
cnf(t12586,plain,
sFlat4 = ifeq(multiply(sFlat0,multiply(sFlat2,sFlat2)),one,multiply(sFlat6,sFlat2),sFlat4),
inference(step,[status(thm)],[t12585,t3340]) ).
cnf(t12587,plain,
sFlat4 = ifeq(multiply(sFlat2,sFlat4),one,multiply(sFlat6,sFlat2),sFlat4),
inference(step,[status(thm)],[t12586,t977]) ).
cnf(t12588,plain,
sFlat4 = ifeq(one,one,multiply(sFlat6,sFlat2),sFlat4),
inference(step,[status(thm)],[t12587,t664]) ).
cnf(t12589,plain,
sFlat4 = multiply(sFlat6,sFlat2),
inference(step,[status(thm)],[t12588,t17]) ).
cnf(t3782,plain,
multiply(sFlat6,sFlat2) = sFlat4,
inference(orient,[status(thm)],[t12589]) ).
cnf(t3783,plain,
multiply(sFlat6,sFlat4) = multiply(sFlat0,sFlat4),
inference(cp,[status(thm)],[t977,t3782]) ).
cnf(t12590,plain,
sFlat4 = multiply(sFlat0,sFlat4),
inference(step,[status(thm)],[t3783,t2104]) ).
cnf(t3801,plain,
multiply(sFlat0,sFlat4) = sFlat4,
inference(orient,[status(thm)],[t12590]) ).
cnf(t3811,plain,
multiply(sFlat0,multiply(X1,sFlat4)) = multiply(X1,sFlat4),
inference(cp,[status(thm)],[t22,t3801]) ).
cnf(t3860,plain,
multiply(sFlat0,multiply(X1,sFlat4)) = multiply(X1,sFlat4),
inference(orient,[status(thm)],[t3811]) ).
cnf(t7080,plain,
multiply(sFlat6,sFlat4) = multiply(multiply(sFlat0,sFlat6),sFlat4),
inference(cp,[status(thm)],[t7079,t3860]) ).
cnf(t12698,plain,
sFlat4 = multiply(multiply(sFlat0,sFlat6),sFlat4),
inference(step,[status(thm)],[t7080,t2104]) ).
cnf(t7160,plain,
multiply(multiply(sFlat0,sFlat6),sFlat4) = sFlat4,
inference(orient,[status(thm)],[t12698]) ).
cnf(t7173,plain,
multiply(sFlat4,multiply(multiply(sFlat4,multiply(sFlat0,sFlat6)),X1)) = multiply(multiply(sFlat0,sFlat6),multiply(sFlat4,X1)),
inference(cp,[status(thm)],[t31,t7160]) ).
cnf(t689,plain,
multiply(b,multiply(X1,a)) = multiply(sFlat4,multiply(X1,sFlat6)),
inference(cp,[status(thm)],[t686,t552]) ).
cnf(t12423,plain,
multiply(X1,sFlat0) = multiply(sFlat4,multiply(X1,sFlat6)),
inference(step,[status(thm)],[t689,t449]) ).
cnf(t991,plain,
multiply(sFlat4,multiply(X1,sFlat6)) = multiply(X1,sFlat0),
inference(orient,[status(thm)],[t12423]) ).
cnf(t12718,plain,
multiply(sFlat4,multiply(multiply(sFlat0,sFlat0),X1)) = multiply(multiply(sFlat0,sFlat6),multiply(sFlat4,X1)),
inference(step,[status(thm)],[t7173,t991]) ).
cnf(t12719,plain,
multiply(sFlat4,multiply(one,X1)) = multiply(multiply(sFlat0,sFlat6),multiply(sFlat4,X1)),
inference(step,[status(thm)],[t12718,t21]) ).
cnf(t12720,plain,
multiply(sFlat4,X1) = multiply(multiply(sFlat0,sFlat6),multiply(sFlat4,X1)),
inference(step,[status(thm)],[t12719,t16]) ).
cnf(t12721,plain,
multiply(sFlat4,X1) = multiply(sFlat4,multiply(multiply(sFlat0,sFlat6),X1)),
inference(step,[status(thm)],[t12720,t22]) ).
cnf(t7396,plain,
multiply(sFlat4,multiply(multiply(sFlat0,sFlat6),X1)) = multiply(sFlat4,X1),
inference(orient,[status(thm)],[t12721]) ).
cnf(t716,plain,
one = multiply(one,multiply(X1,multiply(multiply(X1,sFlat6),sFlat0))),
inference(cp,[status(thm)],[t39,t711]) ).
cnf(t12618,plain,
one = multiply(X1,multiply(multiply(X1,sFlat6),sFlat0)),
inference(step,[status(thm)],[t716,t16]) ).
cnf(t4092,plain,
multiply(X1,multiply(multiply(X1,sFlat6),sFlat0)) = one,
inference(orient,[status(thm)],[t12618]) ).
cnf(t7404,plain,
multiply(sFlat4,multiply(multiply(multiply(sFlat0,sFlat6),sFlat6),sFlat0)) = multiply(sFlat4,one),
inference(cp,[status(thm)],[t7396,t4092]) ).
cnf(t12727,plain,
multiply(multiply(multiply(sFlat0,sFlat6),sFlat6),sFlat0) = multiply(sFlat4,one),
inference(step,[status(thm)],[t7404,t3984]) ).
cnf(t12728,plain,
multiply(multiply(multiply(sFlat0,sFlat6),sFlat6),sFlat0) = one,
inference(step,[status(thm)],[t12727,t28]) ).
cnf(t8856,plain,
multiply(multiply(multiply(sFlat0,sFlat6),sFlat6),sFlat0) = one,
inference(orient,[status(thm)],[t12728]) ).
cnf(t8857,plain,
sFlat0 = ifeq(one,one,ifeq(multiply(sFlat0,multiply(multiply(sFlat0,sFlat6),sFlat6)),one,multiply(multiply(sFlat0,sFlat6),sFlat6),sFlat0),sFlat0),
inference(cp,[status(thm)],[t18,t8856]) ).
cnf(t12729,plain,
sFlat0 = ifeq(multiply(sFlat0,multiply(multiply(sFlat0,sFlat6),sFlat6)),one,multiply(multiply(sFlat0,sFlat6),sFlat6),sFlat0),
inference(step,[status(thm)],[t8857,t17]) ).
cnf(t12730,plain,
sFlat0 = ifeq(multiply(sFlat6,sFlat6),one,multiply(multiply(sFlat0,sFlat6),sFlat6),sFlat0),
inference(step,[status(thm)],[t12729,t7079]) ).
cnf(t12731,plain,
sFlat0 = ifeq(one,one,multiply(multiply(sFlat0,sFlat6),sFlat6),sFlat0),
inference(step,[status(thm)],[t12730,t21]) ).
cnf(t12732,plain,
sFlat0 = multiply(multiply(sFlat0,sFlat6),sFlat6),
inference(step,[status(thm)],[t12731,t17]) ).
cnf(t8886,plain,
multiply(multiply(sFlat0,sFlat6),sFlat6) = sFlat0,
inference(orient,[status(thm)],[t12732]) ).
cnf(t8904,plain,
multiply(multiply(sFlat0,sFlat6),multiply(X1,sFlat6)) = multiply(X1,sFlat0),
inference(cp,[status(thm)],[t22,t8886]) ).
cnf(t11839,plain,
multiply(multiply(sFlat0,sFlat6),multiply(X1,sFlat6)) = multiply(X1,sFlat0),
inference(orient,[status(thm)],[t8904]) ).
cnf(t12876,plain,
multiply(sFlat3,sFlat7) = multiply(sFlat0,sFlat0),
inference(step,[status(thm)],[t12232,t11839]) ).
cnf(t12877,plain,
multiply(sFlat3,sFlat7) = one,
inference(step,[status(thm)],[t12876,t21]) ).
cnf(t12269,plain,
multiply(sFlat3,sFlat7) = one,
inference(orient,[status(thm)],[t12877]) ).
cnf(t12270,plain,
sFlat7 = ifeq(one,one,ifeq(multiply(sFlat7,sFlat3),one,sFlat3,sFlat7),sFlat7),
inference(cp,[status(thm)],[t18,t12269]) ).
cnf(t12882,plain,
sFlat7 = ifeq(multiply(sFlat7,sFlat3),one,sFlat3,sFlat7),
inference(step,[status(thm)],[t12270,t17]) ).
cnf(t7207,plain,
multiply(sFlat1,multiply(multiply(sFlat0,multiply(sFlat1,sFlat6)),X1)) = multiply(multiply(sFlat0,sFlat6),multiply(sFlat7,X1)),
inference(cp,[status(thm)],[t5732,t7183]) ).
cnf(t564,plain,
one = multiply(sFlat1,multiply(sFlat0,sFlat6)),
inference(cp,[status(thm)],[t168,t563]) ).
cnf(t12389,plain,
one = multiply(sFlat0,multiply(sFlat1,sFlat6)),
inference(step,[status(thm)],[t564,t22]) ).
cnf(t573,plain,
multiply(sFlat0,multiply(sFlat1,sFlat6)) = one,
inference(orient,[status(thm)],[t12389]) ).
cnf(t12767,plain,
multiply(sFlat1,multiply(one,X1)) = multiply(multiply(sFlat0,sFlat6),multiply(sFlat7,X1)),
inference(step,[status(thm)],[t7207,t573]) ).
cnf(t12768,plain,
multiply(sFlat1,X1) = multiply(multiply(sFlat0,sFlat6),multiply(sFlat7,X1)),
inference(step,[status(thm)],[t12767,t16]) ).
cnf(t12769,plain,
multiply(sFlat1,X1) = multiply(sFlat7,multiply(multiply(sFlat0,sFlat6),X1)),
inference(step,[status(thm)],[t12768,t22]) ).
cnf(t9449,plain,
multiply(sFlat7,multiply(multiply(sFlat0,sFlat6),X1)) = multiply(sFlat1,X1),
inference(orient,[status(thm)],[t12769]) ).
cnf(t7398,plain,
multiply(sFlat4,b) = multiply(multiply(sFlat0,sFlat6),sFlat5),
inference(cp,[status(thm)],[t7396,t599]) ).
cnf(t12723,plain,
sFlat5 = multiply(multiply(sFlat0,sFlat6),sFlat5),
inference(step,[status(thm)],[t7398,t154]) ).
cnf(t7479,plain,
multiply(multiply(sFlat0,sFlat6),sFlat5) = sFlat5,
inference(orient,[status(thm)],[t12723]) ).
cnf(t9452,plain,
multiply(sFlat1,sFlat5) = multiply(sFlat7,sFlat5),
inference(cp,[status(thm)],[t9449,t7479]) ).
cnf(t9505,plain,
multiply(sFlat7,sFlat5) = multiply(sFlat1,sFlat5),
inference(orient,[status(thm)],[t9452]) ).
cnf(t9510,plain,
one = multiply(sFlat7,multiply(multiply(sFlat1,sFlat5),sFlat5)),
inference(cp,[status(thm)],[t325,t9505]) ).
cnf(t9602,plain,
multiply(sFlat7,multiply(multiply(sFlat1,sFlat5),sFlat5)) = one,
inference(orient,[status(thm)],[t9510]) ).
cnf(t9804,plain,
multiply(sFlat2,b) = multiply(multiply(sFlat1,sFlat5),sFlat5),
inference(cp,[status(thm)],[t9802,t599]) ).
cnf(t12792,plain,
sFlat3 = multiply(multiply(sFlat1,sFlat5),sFlat5),
inference(step,[status(thm)],[t9804,t136]) ).
cnf(t9895,plain,
multiply(multiply(sFlat1,sFlat5),sFlat5) = sFlat3,
inference(orient,[status(thm)],[t12792]) ).
cnf(t12793,plain,
multiply(sFlat7,sFlat3) = one,
inference(step,[status(thm)],[t9602,t9895]) ).
cnf(t9926,plain,
multiply(sFlat7,sFlat3) = one,
inference(rw,[status(thm)],[t12793]) ).
cnf(t9927,plain,
multiply(sFlat7,sFlat3) = one,
inference(orient,[status(thm)],[t9926]) ).
cnf(t12883,plain,
sFlat7 = ifeq(one,one,sFlat3,sFlat7),
inference(step,[status(thm)],[t12882,t9927]) ).
cnf(t12884,plain,
sFlat7 = sFlat3,
inference(step,[status(thm)],[t12883,t17]) ).
cnf(t12296,plain,
sFlat7 = sFlat3,
inference(orient,[status(thm)],[t12884]) ).
cnf(t12885,plain,
multiply(sFlat6,a) = sFlat3,
inference(step,[status(thm)],[t130,t12296]) ).
cnf(t12297,plain,
multiply(sFlat6,a) = sFlat3,
inference(orient,[status(thm)],[t12885]) ).
cnf(f7,negated_conjecture,
multiply(multiply(multiply(multiply(a,b),b),a),a) != multiply(multiply(multiply(multiply(b,a),a),b),b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_j) ).
fof(f7_nnf,plain,
multiply(multiply(multiply(multiply(a,b),b),a),a) != multiply(multiply(multiply(multiply(b,a),a),b),b),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
multiply(multiply(multiply(multiply(a,b),b),a),a) != multiply(multiply(multiply(multiply(b,a),a),b),b),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
multiply(multiply(multiply(multiply(a,b),b),a),a) != multiply(multiply(multiply(multiply(b,a),a),b),b),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(goal_0,negated_conjecture,
multiply(multiply(multiply(multiply(b,a),a),b),b) != multiply(multiply(multiply(multiply(a,b),b),a),a),
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(g0_0,plain,
multiply(multiply(multiply(sFlat0,a),b),b) != multiply(multiply(multiply(multiply(a,b),b),a),a),
inference(rw,[status(thm)],[goal_0,t123]) ).
cnf(g0_1,plain,
multiply(multiply(sFlat1,b),b) != multiply(multiply(multiply(multiply(a,b),b),a),a),
inference(rw,[status(thm)],[g0_0,t160]) ).
cnf(g0_2,plain,
multiply(sFlat2,b) != multiply(multiply(multiply(multiply(a,b),b),a),a),
inference(rw,[status(thm)],[g0_1,t148]) ).
cnf(g0_3,plain,
sFlat3 != multiply(multiply(multiply(multiply(a,b),b),a),a),
inference(rw,[status(thm)],[g0_2,t136]) ).
cnf(g0_4,plain,
sFlat3 != multiply(multiply(multiply(sFlat4,b),a),a),
inference(rw,[status(thm)],[g0_3,t115]) ).
cnf(g0_5,plain,
sFlat3 != multiply(multiply(sFlat5,a),a),
inference(rw,[status(thm)],[g0_4,t154]) ).
cnf(g0_6,plain,
sFlat3 != multiply(sFlat6,a),
inference(rw,[status(thm)],[g0_5,t142]) ).
cnf(g0_7,plain,
sFlat3 != sFlat3,
inference(rw,[status(thm)],[g0_6,t12297]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_7]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG010-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.34 % Computer : n008.cluster.edu
% 0.10/0.34 % Model : x86_64 x86_64
% 0.10/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.34 % Memory : 8046.5625MB
% 0.10/0.34 % OS : Linux 6.8.0-71-generic
% 0.10/0.34 % CPULimit : 300
% 0.10/0.34 % WCLimit : 300
% 0.10/0.34 % DateTime : Fri Sep 25 04:32:09 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.35 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 22.50/3.52 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 22.50/3.52 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------