%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP682+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n009.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:28:01 PM UTC 2026
% Result : Theorem 6.30s 1.38s
% Output : Proof 6.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 117
% Number of leaves : 9
% Syntax : Number of formulae : 300 ( 295 unt; 0 def)
% Number of atoms : 305 ( 304 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 18 ( 13 ~; 3 |; 2 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-4 aty)
% Number of variables : 712 ( 2 sgn 54 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [B,A] : mult(rd(A,B),B) = rd(mult(A,B),B),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f04) ).
fof(f3_nnf,plain,
! [B,A] : mult(rd(A,B),B) = rd(mult(A,B),B),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A,B] : mult(rd(A,B),B) = rd(mult(A,B),B),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
mult(rd(X1,X0),X0) = rd(mult(X1,X0),X0),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t4,plain,
rd(mult(X1,X2),X2) = mult(rd(X1,X2),X2),
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t26,plain,
mult(rd(X1,X2),X2) = rd(mult(X1,X2),X2),
inference(orient,[status(thm)],[t4]) ).
fof(f4,axiom,
! [D,C,B,A] : ld(ld(A,B),mult(ld(A,B),mult(C,D))) = mult(ld(A,mult(A,C)),D),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f05) ).
fof(f4_nnf,plain,
! [D,C,B,A] : ld(ld(A,B),mult(ld(A,B),mult(C,D))) = mult(ld(A,mult(A,C)),D),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [A,B,C,D] : ld(ld(A,B),mult(ld(A,B),mult(C,D))) = mult(ld(A,mult(A,C)),D),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
ld(ld(X3,X2),mult(ld(X3,X2),mult(X1,X0))) = mult(ld(X3,mult(X3,X1)),X0),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t6,plain,
ld(ld(X1,X2),mult(ld(X1,X2),mult(X3,X4))) = mult(ld(X1,mult(X1,X3)),X4),
inference(equality_encoding,[status(esa)],[c4]) ).
fof(f2,axiom,
! [B,A] : mult(A,ld(A,B)) = ld(A,mult(A,B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f03) ).
fof(f2_nnf,plain,
! [B,A] : mult(A,ld(A,B)) = ld(A,mult(A,B)),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A,B] : mult(A,ld(A,B)) = ld(A,mult(A,B)),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
mult(X1,ld(X1,X0)) = ld(X1,mult(X1,X0)),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t3,plain,
mult(X1,ld(X1,X2)) = ld(X1,mult(X1,X2)),
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t12,plain,
ld(X1,mult(X1,X2)) = mult(X1,ld(X1,X2)),
inference(orient,[status(thm)],[t3]) ).
cnf(t2495,plain,
mult(ld(X1,X2),ld(ld(X1,X2),mult(X3,X4))) = mult(ld(X1,mult(X1,X3)),X4),
inference(step,[status(thm)],[t6,t12]) ).
cnf(t2496,plain,
mult(ld(X1,X2),ld(ld(X1,X2),mult(X3,X4))) = mult(mult(X1,ld(X1,X3)),X4),
inference(step,[status(thm)],[t2495,t12]) ).
cnf(t19,plain,
mult(ld(X1,X2),ld(ld(X1,X2),mult(X3,X4))) = mult(mult(X1,ld(X1,X3)),X4),
inference(orient,[status(thm)],[t2496]) ).
cnf(t20,plain,
mult(mult(X1,ld(X1,X2)),X3) = mult(mult(X1,ld(X1,X4)),ld(ld(X1,mult(X1,X4)),mult(X2,X3))),
inference(cp,[status(thm)],[t19,t12]) ).
cnf(t2542,plain,
mult(mult(X1,ld(X1,X2)),X3) = mult(mult(X1,ld(X1,X4)),ld(mult(X1,ld(X1,X4)),mult(X2,X3))),
inference(step,[status(thm)],[t20,t12]) ).
cnf(t625,plain,
mult(mult(X1,ld(X1,X2)),ld(mult(X1,ld(X1,X2)),mult(X3,X4))) = mult(mult(X1,ld(X1,X3)),X4),
inference(orient,[status(thm)],[t2542]) ).
fof(f0,axiom,
! [A] : ld(A,mult(A,A)) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f01) ).
fof(f0_nnf,plain,
! [A] : ld(A,mult(A,A)) = A,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A] : ld(A,mult(A,A)) = A,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
ld(X0,mult(X0,X0)) = X0,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t1,plain,
ld(X1,mult(X1,X1)) = X1,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t9,plain,
ld(X1,mult(X1,X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t2494,plain,
mult(X1,ld(X1,X1)) = X1,
inference(step,[status(thm)],[t9,t12]) ).
cnf(t13,plain,
mult(X1,ld(X1,X1)) = X1,
inference(rw,[status(thm)],[t2494]) ).
cnf(t37,plain,
mult(X1,ld(X1,X1)) = X1,
inference(orient,[status(thm)],[t13]) ).
cnf(t39,plain,
mult(X1,ld(X1,ld(X1,X1))) = ld(X1,X1),
inference(cp,[status(thm)],[t12,t37]) ).
fof(f6,axiom,
! [B,A] : ld(A,mult(A,ld(B,B))) = rd(mult(rd(A,A),B),B),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f07) ).
fof(f6_nnf,plain,
! [B,A] : ld(A,mult(A,ld(B,B))) = rd(mult(rd(A,A),B),B),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [A,B] : ld(A,mult(A,ld(B,B))) = rd(mult(rd(A,A),B),B),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
ld(X1,mult(X1,ld(X0,X0))) = rd(mult(rd(X1,X1),X0),X0),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t5,plain,
rd(mult(rd(X1,X1),X2),X2) = ld(X1,mult(X1,ld(X2,X2))),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t2497,plain,
rd(mult(rd(X1,X1),X2),X2) = mult(X1,ld(X1,ld(X2,X2))),
inference(step,[status(thm)],[t5,t12]) ).
cnf(t32,plain,
mult(X1,ld(X1,ld(X2,X2))) = rd(mult(rd(X1,X1),X2),X2),
inference(orient,[status(thm)],[t2497]) ).
cnf(t2502,plain,
rd(mult(rd(X1,X1),X1),X1) = ld(X1,X1),
inference(step,[status(thm)],[t39,t32]) ).
cnf(t2503,plain,
rd(rd(mult(X1,X1),X1),X1) = ld(X1,X1),
inference(step,[status(thm)],[t2502,t26]) ).
fof(f1,axiom,
! [A] : rd(mult(A,A),A) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f02) ).
fof(f1_nnf,plain,
! [A] : rd(mult(A,A),A) = A,
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A] : rd(mult(A,A),A) = A,
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
rd(mult(X0,X0),X0) = X0,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t2,plain,
rd(mult(X1,X1),X1) = X1,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t10,plain,
rd(mult(X1,X1),X1) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t2504,plain,
rd(X1,X1) = ld(X1,X1),
inference(step,[status(thm)],[t2503,t10]) ).
cnf(t42,plain,
ld(X1,X1) = rd(X1,X1),
inference(orient,[status(thm)],[t2504]) ).
cnf(t629,plain,
mult(mult(X1,ld(X1,X2)),X3) = mult(mult(X1,rd(X1,X1)),ld(mult(X1,ld(X1,X1)),mult(X2,X3))),
inference(cp,[status(thm)],[t625,t42]) ).
cnf(t2505,plain,
mult(X1,rd(X1,X1)) = X1,
inference(step,[status(thm)],[t37,t42]) ).
cnf(t45,plain,
mult(X1,rd(X1,X1)) = X1,
inference(rw,[status(thm)],[t2505]) ).
cnf(t47,plain,
mult(X1,rd(X1,X1)) = X1,
inference(orient,[status(thm)],[t45]) ).
cnf(t2543,plain,
mult(mult(X1,ld(X1,X2)),X3) = mult(X1,ld(mult(X1,ld(X1,X1)),mult(X2,X3))),
inference(step,[status(thm)],[t629,t47]) ).
cnf(t2544,plain,
mult(mult(X1,ld(X1,X2)),X3) = mult(X1,ld(mult(X1,rd(X1,X1)),mult(X2,X3))),
inference(step,[status(thm)],[t2543,t42]) ).
cnf(t2545,plain,
mult(mult(X1,ld(X1,X2)),X3) = mult(X1,ld(X1,mult(X2,X3))),
inference(step,[status(thm)],[t2544,t47]) ).
cnf(t680,plain,
mult(mult(X1,ld(X1,X2)),X3) = mult(X1,ld(X1,mult(X2,X3))),
inference(orient,[status(thm)],[t2545]) ).
cnf(t693,plain,
mult(X1,ld(X1,mult(X1,X2))) = mult(mult(X1,rd(X1,X1)),X2),
inference(cp,[status(thm)],[t680,t42]) ).
cnf(t2552,plain,
mult(X1,mult(X1,ld(X1,X2))) = mult(mult(X1,rd(X1,X1)),X2),
inference(step,[status(thm)],[t693,t12]) ).
cnf(t2553,plain,
mult(X1,mult(X1,ld(X1,X2))) = mult(X1,X2),
inference(step,[status(thm)],[t2552,t47]) ).
cnf(t731,plain,
mult(X1,mult(X1,ld(X1,X2))) = mult(X1,X2),
inference(orient,[status(thm)],[t2553]) ).
cnf(t2506,plain,
mult(X1,ld(X1,rd(X2,X2))) = rd(mult(rd(X1,X1),X2),X2),
inference(step,[status(thm)],[t32,t42]) ).
cnf(t46,plain,
mult(X1,ld(X1,rd(X2,X2))) = rd(mult(rd(X1,X1),X2),X2),
inference(rw,[status(thm)],[t2506]) ).
cnf(t90,plain,
mult(X1,ld(X1,rd(X2,X2))) = rd(mult(rd(X1,X1),X2),X2),
inference(orient,[status(thm)],[t46]) ).
fof(f5,axiom,
! [D,C,B,A] : rd(mult(mult(A,B),rd(C,D)),rd(C,D)) = mult(A,rd(mult(B,D),D)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f06) ).
fof(f5_nnf,plain,
! [D,C,B,A] : rd(mult(mult(A,B),rd(C,D)),rd(C,D)) = mult(A,rd(mult(B,D),D)),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [A,B,C,D] : rd(mult(mult(A,B),rd(C,D)),rd(C,D)) = mult(A,rd(mult(B,D),D)),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
rd(mult(mult(X3,X2),rd(X1,X0)),rd(X1,X0)) = mult(X3,rd(mult(X2,X0),X0)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t7,plain,
rd(mult(mult(X1,X2),rd(X3,X4)),rd(X3,X4)) = mult(X1,rd(mult(X2,X4),X4)),
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t14,plain,
rd(mult(mult(X1,X2),rd(X3,X4)),rd(X3,X4)) = mult(X1,rd(mult(X2,X4),X4)),
inference(orient,[status(thm)],[t7]) ).
cnf(t15,plain,
mult(X1,rd(mult(X2,X3),X3)) = rd(mult(mult(X1,X2),X3),rd(mult(X3,X3),X3)),
inference(cp,[status(thm)],[t14,t10]) ).
cnf(t2508,plain,
mult(X1,rd(mult(X2,X3),X3)) = rd(mult(mult(X1,X2),X3),X3),
inference(step,[status(thm)],[t15,t10]) ).
cnf(t61,plain,
mult(X1,rd(mult(X2,X3),X3)) = rd(mult(mult(X1,X2),X3),X3),
inference(orient,[status(thm)],[t2508]) ).
cnf(t2509,plain,
rd(mult(mult(X1,X2),rd(X3,X4)),rd(X3,X4)) = rd(mult(mult(X1,X2),X4),X4),
inference(step,[status(thm)],[t14,t61]) ).
cnf(t62,plain,
rd(mult(mult(X1,X2),rd(X3,X4)),rd(X3,X4)) = rd(mult(mult(X1,X2),X4),X4),
inference(orient,[status(thm)],[t2509]) ).
cnf(t91,plain,
rd(mult(rd(rd(X1,X1),rd(X1,X1)),X1),X1) = mult(rd(X1,X1),rd(rd(X1,X1),rd(X1,X1))),
inference(cp,[status(thm)],[t90,t42]) ).
cnf(t2513,plain,
rd(mult(rd(rd(X1,X1),rd(X1,X1)),X1),X1) = rd(X1,X1),
inference(step,[status(thm)],[t91,t47]) ).
cnf(t113,plain,
rd(mult(rd(rd(X1,X1),rd(X1,X1)),X1),X1) = rd(X1,X1),
inference(orient,[status(thm)],[t2513]) ).
cnf(t115,plain,
rd(mult(mult(rd(rd(X1,X1),rd(X1,X1)),X1),X1),X1) = mult(rd(X1,X1),X1),
inference(cp,[status(thm)],[t26,t113]) ).
cnf(t65,plain,
rd(mult(mult(X1,X2),X2),X2) = mult(X1,X2),
inference(cp,[status(thm)],[t61,t10]) ).
cnf(t79,plain,
rd(mult(mult(X1,X2),X2),X2) = mult(X1,X2),
inference(orient,[status(thm)],[t65]) ).
cnf(t2514,plain,
mult(rd(rd(X1,X1),rd(X1,X1)),X1) = mult(rd(X1,X1),X1),
inference(step,[status(thm)],[t115,t79]) ).
cnf(t2515,plain,
mult(rd(rd(X1,X1),rd(X1,X1)),X1) = rd(mult(X1,X1),X1),
inference(step,[status(thm)],[t2514,t26]) ).
cnf(t2516,plain,
mult(rd(rd(X1,X1),rd(X1,X1)),X1) = X1,
inference(step,[status(thm)],[t2515,t10]) ).
cnf(t119,plain,
mult(rd(rd(X1,X1),rd(X1,X1)),X1) = X1,
inference(orient,[status(thm)],[t2516]) ).
cnf(t122,plain,
rd(mult(mult(rd(rd(X1,X1),rd(X1,X1)),X1),X2),X2) = rd(mult(X1,rd(X3,X2)),rd(X3,X2)),
inference(cp,[status(thm)],[t62,t119]) ).
cnf(t2519,plain,
rd(mult(X1,X2),X2) = rd(mult(X1,rd(X3,X2)),rd(X3,X2)),
inference(step,[status(thm)],[t122,t119]) ).
cnf(t132,plain,
rd(mult(X1,rd(X2,X3)),rd(X2,X3)) = rd(mult(X1,X3),X3),
inference(orient,[status(thm)],[t2519]) ).
cnf(t43,plain,
mult(mult(X1,ld(X1,X2)),X3) = mult(rd(X1,X1),ld(ld(X1,X1),mult(X2,X3))),
inference(cp,[status(thm)],[t19,t42]) ).
cnf(t2527,plain,
mult(mult(X1,ld(X1,X2)),X3) = mult(rd(X1,X1),ld(rd(X1,X1),mult(X2,X3))),
inference(step,[status(thm)],[t43,t42]) ).
cnf(t343,plain,
mult(rd(X1,X1),ld(rd(X1,X1),mult(X2,X3))) = mult(mult(X1,ld(X1,X2)),X3),
inference(orient,[status(thm)],[t2527]) ).
cnf(t136,plain,
rd(mult(rd(X1,rd(X2,X3)),X3),X3) = rd(rd(mult(X1,rd(X2,X3)),rd(X2,X3)),rd(X2,X3)),
inference(cp,[status(thm)],[t132,t26]) ).
cnf(t80,plain,
mult(X1,rd(X2,X3)) = rd(mult(mult(X1,rd(X2,X3)),X3),X3),
inference(cp,[status(thm)],[t79,t62]) ).
cnf(t97,plain,
rd(mult(mult(X1,rd(X2,X3)),X3),X3) = mult(X1,rd(X2,X3)),
inference(orient,[status(thm)],[t80]) ).
cnf(t125,plain,
mult(rd(rd(rd(X1,X2),rd(X1,X2)),rd(rd(X1,X2),rd(X1,X2))),rd(X1,X2)) = rd(mult(rd(X1,X2),X2),X2),
inference(cp,[status(thm)],[t97,t119]) ).
cnf(t2517,plain,
rd(X1,X2) = rd(mult(rd(X1,X2),X2),X2),
inference(step,[status(thm)],[t125,t119]) ).
cnf(t2518,plain,
rd(X1,X2) = rd(rd(mult(X1,X2),X2),X2),
inference(step,[status(thm)],[t2517,t26]) ).
cnf(t126,plain,
rd(rd(mult(X1,X2),X2),X2) = rd(X1,X2),
inference(orient,[status(thm)],[t2518]) ).
cnf(t2520,plain,
rd(mult(rd(X1,rd(X2,X3)),X3),X3) = rd(X1,rd(X2,X3)),
inference(step,[status(thm)],[t136,t126]) ).
cnf(t149,plain,
rd(mult(rd(X1,rd(X2,X3)),X3),X3) = rd(X1,rd(X2,X3)),
inference(orient,[status(thm)],[t2520]) ).
cnf(t151,plain,
rd(rd(X1,X1),rd(X1,X1)) = rd(X1,X1),
inference(cp,[status(thm)],[t149,t119]) ).
cnf(t162,plain,
rd(rd(X1,X1),rd(X1,X1)) = rd(X1,X1),
inference(orient,[status(thm)],[t151]) ).
cnf(t163,plain,
rd(X1,X1) = mult(rd(X1,X1),rd(X1,X1)),
inference(cp,[status(thm)],[t47,t162]) ).
cnf(t165,plain,
mult(rd(X1,X1),rd(X1,X1)) = rd(X1,X1),
inference(orient,[status(thm)],[t163]) ).
cnf(t358,plain,
mult(mult(X1,ld(X1,rd(X2,X2))),rd(X2,X2)) = mult(rd(X1,X1),ld(rd(X1,X1),rd(X2,X2))),
inference(cp,[status(thm)],[t343,t165]) ).
cnf(t2528,plain,
mult(rd(mult(rd(X1,X1),X2),X2),rd(X2,X2)) = mult(rd(X1,X1),ld(rd(X1,X1),rd(X2,X2))),
inference(step,[status(thm)],[t358,t90]) ).
cnf(t144,plain,
rd(mult(mult(X1,rd(X2,X3)),rd(X2,X3)),rd(X2,X3)) = mult(rd(mult(X1,X3),X3),rd(X2,X3)),
inference(cp,[status(thm)],[t26,t132]) ).
cnf(t2522,plain,
rd(mult(mult(X1,rd(X2,X3)),X3),X3) = mult(rd(mult(X1,X3),X3),rd(X2,X3)),
inference(step,[status(thm)],[t144,t62]) ).
cnf(t2523,plain,
mult(X1,rd(X2,X3)) = mult(rd(mult(X1,X3),X3),rd(X2,X3)),
inference(step,[status(thm)],[t2522,t97]) ).
cnf(t184,plain,
mult(rd(mult(X1,X2),X2),rd(X3,X2)) = mult(X1,rd(X3,X2)),
inference(orient,[status(thm)],[t2523]) ).
cnf(t2529,plain,
mult(rd(X1,X1),rd(X2,X2)) = mult(rd(X1,X1),ld(rd(X1,X1),rd(X2,X2))),
inference(step,[status(thm)],[t2528,t184]) ).
cnf(t2530,plain,
mult(rd(X1,X1),rd(X2,X2)) = rd(mult(rd(rd(X1,X1),rd(X1,X1)),X2),X2),
inference(step,[status(thm)],[t2529,t90]) ).
cnf(t2531,plain,
mult(rd(X1,X1),rd(X2,X2)) = rd(mult(rd(X1,X1),X2),X2),
inference(step,[status(thm)],[t2530,t162]) ).
cnf(t379,plain,
mult(rd(X1,X1),rd(X2,X2)) = rd(mult(rd(X1,X1),X2),X2),
inference(orient,[status(thm)],[t2531]) ).
cnf(t393,plain,
rd(mult(rd(X1,X1),X2),X2) = rd(rd(mult(rd(X1,X1),X2),X2),rd(X2,X2)),
inference(cp,[status(thm)],[t132,t379]) ).
cnf(t145,plain,
rd(X1,rd(X2,X3)) = rd(rd(mult(X1,X3),X3),rd(X2,X3)),
inference(cp,[status(thm)],[t126,t132]) ).
cnf(t201,plain,
rd(rd(mult(X1,X2),X2),rd(X3,X2)) = rd(X1,rd(X3,X2)),
inference(orient,[status(thm)],[t145]) ).
cnf(t2532,plain,
rd(mult(rd(X1,X1),X2),X2) = rd(rd(X1,X1),rd(X2,X2)),
inference(step,[status(thm)],[t393,t201]) ).
cnf(t400,plain,
rd(mult(rd(X1,X1),X2),X2) = rd(rd(X1,X1),rd(X2,X2)),
inference(orient,[status(thm)],[t2532]) ).
cnf(t2533,plain,
mult(X1,ld(X1,rd(X2,X2))) = rd(rd(X1,X1),rd(X2,X2)),
inference(step,[status(thm)],[t90,t400]) ).
cnf(t401,plain,
mult(X1,ld(X1,rd(X2,X2))) = rd(rd(X1,X1),rd(X2,X2)),
inference(orient,[status(thm)],[t2533]) ).
cnf(t733,plain,
mult(X1,rd(X2,X2)) = mult(X1,rd(rd(X1,X1),rd(X2,X2))),
inference(cp,[status(thm)],[t731,t401]) ).
cnf(t394,plain,
rd(mult(mult(X1,rd(X2,X2)),rd(X3,X3)),rd(X3,X3)) = mult(X1,rd(rd(mult(rd(X2,X2),X3),X3),rd(X3,X3))),
inference(cp,[status(thm)],[t61,t379]) ).
cnf(t2539,plain,
rd(mult(mult(X1,rd(X2,X2)),X3),X3) = mult(X1,rd(rd(mult(rd(X2,X2),X3),X3),rd(X3,X3))),
inference(step,[status(thm)],[t394,t62]) ).
cnf(t2540,plain,
rd(mult(mult(X1,rd(X2,X2)),X3),X3) = mult(X1,rd(rd(X2,X2),rd(X3,X3))),
inference(step,[status(thm)],[t2539,t201]) ).
cnf(t455,plain,
mult(X1,rd(rd(X2,X2),rd(X3,X3))) = rd(mult(mult(X1,rd(X2,X2)),X3),X3),
inference(orient,[status(thm)],[t2540]) ).
cnf(t2557,plain,
mult(X1,rd(X2,X2)) = rd(mult(mult(X1,rd(X1,X1)),X2),X2),
inference(step,[status(thm)],[t733,t455]) ).
cnf(t2558,plain,
mult(X1,rd(X2,X2)) = rd(mult(X1,X2),X2),
inference(step,[status(thm)],[t2557,t47]) ).
cnf(t763,plain,
mult(X1,rd(X2,X2)) = rd(mult(X1,X2),X2),
inference(orient,[status(thm)],[t2558]) ).
cnf(t767,plain,
rd(mult(rd(X1,rd(X2,X2)),X2),X2) = rd(mult(X1,rd(X2,X2)),rd(X2,X2)),
inference(cp,[status(thm)],[t763,t26]) ).
cnf(t2561,plain,
rd(X1,rd(X2,X2)) = rd(mult(X1,rd(X2,X2)),rd(X2,X2)),
inference(step,[status(thm)],[t767,t149]) ).
cnf(t2562,plain,
rd(X1,rd(X2,X2)) = rd(mult(X1,X2),X2),
inference(step,[status(thm)],[t2561,t132]) ).
cnf(t794,plain,
rd(mult(X1,X2),X2) = rd(X1,rd(X2,X2)),
inference(orient,[status(thm)],[t2562]) ).
cnf(t2563,plain,
mult(rd(X1,X2),X2) = rd(X1,rd(X2,X2)),
inference(step,[status(thm)],[t26,t794]) ).
cnf(t795,plain,
mult(rd(X1,X2),X2) = rd(X1,rd(X2,X2)),
inference(orient,[status(thm)],[t2563]) ).
cnf(t811,plain,
rd(mult(X1,X2),rd(X2,X2)) = mult(rd(X1,rd(X2,X2)),X2),
inference(cp,[status(thm)],[t795,t794]) ).
cnf(t2581,plain,
rd(mult(X1,X2),rd(X2,X2)) = mult(X1,X2),
inference(step,[status(thm)],[t79,t794]) ).
cnf(t820,plain,
rd(mult(X1,X2),rd(X2,X2)) = mult(X1,X2),
inference(rw,[status(thm)],[t2581]) ).
cnf(t836,plain,
rd(mult(X1,X2),rd(X2,X2)) = mult(X1,X2),
inference(orient,[status(thm)],[t820]) ).
cnf(t2598,plain,
mult(X1,X2) = mult(rd(X1,rd(X2,X2)),X2),
inference(step,[status(thm)],[t811,t836]) ).
cnf(t860,plain,
mult(rd(X1,rd(X2,X2)),X2) = mult(X1,X2),
inference(orient,[status(thm)],[t2598]) ).
cnf(t140,plain,
rd(mult(X1,X2),X2) = rd(mult(X1,mult(X3,X2)),rd(mult(mult(X3,X2),X2),X2)),
inference(cp,[status(thm)],[t132,t79]) ).
cnf(t2521,plain,
rd(mult(X1,X2),X2) = rd(mult(X1,mult(X3,X2)),mult(X3,X2)),
inference(step,[status(thm)],[t140,t79]) ).
cnf(t167,plain,
rd(mult(X1,mult(X2,X3)),mult(X2,X3)) = rd(mult(X1,X3),X3),
inference(orient,[status(thm)],[t2521]) ).
cnf(t2577,plain,
rd(X1,rd(mult(X2,X3),mult(X2,X3))) = rd(mult(X1,X3),X3),
inference(step,[status(thm)],[t167,t794]) ).
cnf(t2578,plain,
rd(X1,rd(mult(X2,X3),mult(X2,X3))) = rd(X1,rd(X3,X3)),
inference(step,[status(thm)],[t2577,t794]) ).
cnf(t818,plain,
rd(X1,rd(mult(X2,X3),mult(X2,X3))) = rd(X1,rd(X3,X3)),
inference(rw,[status(thm)],[t2578]) ).
cnf(t916,plain,
rd(X1,rd(mult(X2,X3),mult(X2,X3))) = rd(X1,rd(X3,X3)),
inference(orient,[status(thm)],[t818]) ).
cnf(t696,plain,
mult(X1,ld(X1,mult(mult(X1,X2),X3))) = mult(mult(X1,mult(X1,ld(X1,X2))),X3),
inference(cp,[status(thm)],[t680,t12]) ).
cnf(t2628,plain,
mult(X1,ld(X1,mult(mult(X1,X2),X3))) = mult(mult(X1,X2),X3),
inference(step,[status(thm)],[t696,t731]) ).
cnf(t1557,plain,
mult(X1,ld(X1,mult(mult(X1,X2),X3))) = mult(mult(X1,X2),X3),
inference(orient,[status(thm)],[t2628]) ).
cnf(t1581,plain,
rd(X1,rd(ld(X2,mult(mult(X2,X3),X4)),ld(X2,mult(mult(X2,X3),X4)))) = rd(X1,rd(mult(X2,ld(X2,mult(mult(X2,X3),X4))),mult(mult(X2,X3),X4))),
inference(cp,[status(thm)],[t916,t1557]) ).
cnf(t921,plain,
rd(X1,rd(mult(X2,ld(X2,X3)),mult(X2,ld(X2,X3)))) = rd(X1,rd(mult(X2,X3),mult(X2,mult(X2,ld(X2,X3))))),
inference(cp,[status(thm)],[t916,t731]) ).
cnf(t2600,plain,
rd(X1,rd(ld(X2,X3),ld(X2,X3))) = rd(X1,rd(mult(X2,X3),mult(X2,mult(X2,ld(X2,X3))))),
inference(step,[status(thm)],[t921,t916]) ).
cnf(t2601,plain,
rd(X1,rd(ld(X2,X3),ld(X2,X3))) = rd(X1,rd(mult(X2,X3),mult(X2,X3))),
inference(step,[status(thm)],[t2600,t731]) ).
cnf(t2602,plain,
rd(X1,rd(ld(X2,X3),ld(X2,X3))) = rd(X1,rd(X3,X3)),
inference(step,[status(thm)],[t2601,t916]) ).
cnf(t1056,plain,
rd(X1,rd(ld(X2,X3),ld(X2,X3))) = rd(X1,rd(X3,X3)),
inference(orient,[status(thm)],[t2602]) ).
cnf(t2629,plain,
rd(X1,rd(mult(mult(X2,X3),X4),mult(mult(X2,X3),X4))) = rd(X1,rd(mult(X2,ld(X2,mult(mult(X2,X3),X4))),mult(mult(X2,X3),X4))),
inference(step,[status(thm)],[t1581,t1056]) ).
cnf(t2630,plain,
rd(X1,rd(X4,X4)) = rd(X1,rd(mult(X2,ld(X2,mult(mult(X2,X3),X4))),mult(mult(X2,X3),X4))),
inference(step,[status(thm)],[t2629,t916]) ).
cnf(t690,plain,
mult(X1,ld(X1,mult(rd(X2,X2),X3))) = mult(rd(rd(X1,X1),rd(X2,X2)),X3),
inference(cp,[status(thm)],[t680,t401]) ).
cnf(t1271,plain,
mult(rd(rd(X1,X1),rd(X2,X2)),X3) = mult(X1,ld(X1,mult(rd(X2,X2),X3))),
inference(orient,[status(thm)],[t690]) ).
cnf(t1272,plain,
mult(X1,ld(X1,mult(rd(X2,X2),X2))) = mult(rd(X1,X1),X2),
inference(cp,[status(thm)],[t1271,t860]) ).
cnf(t2605,plain,
mult(X1,ld(X1,rd(X2,rd(X2,X2)))) = mult(rd(X1,X1),X2),
inference(step,[status(thm)],[t1272,t795]) ).
cnf(t82,plain,
mult(X1,rd(X1,X1)) = rd(mult(X1,rd(X1,X1)),rd(X1,X1)),
inference(cp,[status(thm)],[t79,t47]) ).
cnf(t2511,plain,
X1 = rd(mult(X1,rd(X1,X1)),rd(X1,X1)),
inference(step,[status(thm)],[t82,t47]) ).
cnf(t2512,plain,
X1 = rd(X1,rd(X1,X1)),
inference(step,[status(thm)],[t2511,t47]) ).
cnf(t89,plain,
rd(X1,rd(X1,X1)) = X1,
inference(orient,[status(thm)],[t2512]) ).
cnf(t2606,plain,
mult(X1,ld(X1,X2)) = mult(rd(X1,X1),X2),
inference(step,[status(thm)],[t2605,t89]) ).
cnf(t1308,plain,
mult(rd(X1,X1),X2) = mult(X1,ld(X1,X2)),
inference(orient,[status(thm)],[t2606]) ).
cnf(t1323,plain,
rd(rd(X1,X1),rd(X2,X2)) = rd(mult(X1,ld(X1,X2)),X2),
inference(cp,[status(thm)],[t794,t1308]) ).
cnf(t1336,plain,
rd(mult(X1,ld(X1,X2)),X2) = rd(rd(X1,X1),rd(X2,X2)),
inference(orient,[status(thm)],[t1323]) ).
cnf(t2631,plain,
rd(X1,rd(X4,X4)) = rd(X1,rd(rd(X2,X2),rd(mult(mult(X2,X3),X4),mult(mult(X2,X3),X4)))),
inference(step,[status(thm)],[t2630,t1336]) ).
cnf(t2632,plain,
rd(X1,rd(X4,X4)) = rd(X1,rd(rd(X2,X2),rd(X4,X4))),
inference(step,[status(thm)],[t2631,t916]) ).
cnf(t1584,plain,
rd(X1,rd(rd(X2,X2),rd(X3,X3))) = rd(X1,rd(X3,X3)),
inference(orient,[status(thm)],[t2632]) ).
cnf(t1593,plain,
rd(mult(X1,rd(rd(X2,X2),rd(X3,X3))),rd(X3,X3)) = rd(X1,rd(rd(rd(X2,X2),rd(X3,X3)),rd(rd(X2,X2),rd(X3,X3)))),
inference(cp,[status(thm)],[t1584,t794]) ).
cnf(t2559,plain,
mult(X1,rd(rd(X2,X2),rd(X3,X3))) = rd(mult(rd(mult(X1,X2),X2),X3),X3),
inference(step,[status(thm)],[t455,t763]) ).
cnf(t764,plain,
mult(X1,rd(rd(X2,X2),rd(X3,X3))) = rd(mult(rd(mult(X1,X2),X2),X3),X3),
inference(orient,[status(thm)],[t2559]) ).
cnf(t2565,plain,
mult(X1,rd(rd(X2,X2),rd(X3,X3))) = rd(rd(mult(X1,X2),X2),rd(X3,X3)),
inference(step,[status(thm)],[t764,t794]) ).
cnf(t2566,plain,
mult(X1,rd(rd(X2,X2),rd(X3,X3))) = rd(rd(X1,rd(X2,X2)),rd(X3,X3)),
inference(step,[status(thm)],[t2565,t794]) ).
cnf(t797,plain,
mult(X1,rd(rd(X2,X2),rd(X3,X3))) = rd(rd(X1,rd(X2,X2)),rd(X3,X3)),
inference(orient,[status(thm)],[t2566]) ).
cnf(t2633,plain,
rd(rd(rd(X1,rd(X2,X2)),rd(X3,X3)),rd(X3,X3)) = rd(X1,rd(rd(rd(X2,X2),rd(X3,X3)),rd(rd(X2,X2),rd(X3,X3)))),
inference(step,[status(thm)],[t1593,t797]) ).
cnf(t2588,plain,
rd(rd(X1,rd(X2,X3)),rd(X3,X3)) = rd(X1,rd(X2,X3)),
inference(step,[status(thm)],[t149,t794]) ).
cnf(t825,plain,
rd(rd(X1,rd(X2,X3)),rd(X3,X3)) = rd(X1,rd(X2,X3)),
inference(rw,[status(thm)],[t2588]) ).
cnf(t1023,plain,
rd(rd(X1,rd(X2,X3)),rd(X3,X3)) = rd(X1,rd(X2,X3)),
inference(orient,[status(thm)],[t825]) ).
cnf(t2634,plain,
rd(rd(X1,rd(X2,X2)),rd(X3,X3)) = rd(X1,rd(rd(rd(X2,X2),rd(X3,X3)),rd(rd(X2,X2),rd(X3,X3)))),
inference(step,[status(thm)],[t2633,t1023]) ).
cnf(t2579,plain,
rd(X1,rd(rd(X2,X3),rd(X2,X3))) = rd(mult(X1,X3),X3),
inference(step,[status(thm)],[t132,t794]) ).
cnf(t2580,plain,
rd(X1,rd(rd(X2,X3),rd(X2,X3))) = rd(X1,rd(X3,X3)),
inference(step,[status(thm)],[t2579,t794]) ).
cnf(t819,plain,
rd(X1,rd(rd(X2,X3),rd(X2,X3))) = rd(X1,rd(X3,X3)),
inference(rw,[status(thm)],[t2580]) ).
cnf(t962,plain,
rd(X1,rd(rd(X2,X3),rd(X2,X3))) = rd(X1,rd(X3,X3)),
inference(orient,[status(thm)],[t819]) ).
cnf(t2635,plain,
rd(rd(X1,rd(X2,X2)),rd(X3,X3)) = rd(X1,rd(rd(X3,X3),rd(X3,X3))),
inference(step,[status(thm)],[t2634,t962]) ).
cnf(t2636,plain,
rd(rd(X1,rd(X2,X2)),rd(X3,X3)) = rd(X1,rd(X3,X3)),
inference(step,[status(thm)],[t2635,t962]) ).
cnf(t1641,plain,
rd(rd(X1,rd(X2,X2)),rd(X3,X3)) = rd(X1,rd(X3,X3)),
inference(orient,[status(thm)],[t2636]) ).
cnf(t1669,plain,
mult(rd(X1,rd(X2,X2)),X3) = mult(rd(X1,rd(X3,X3)),X3),
inference(cp,[status(thm)],[t860,t1641]) ).
cnf(t2637,plain,
mult(rd(X1,rd(X2,X2)),X3) = mult(X1,X3),
inference(step,[status(thm)],[t1669,t860]) ).
cnf(t1677,plain,
mult(rd(X1,rd(X2,X2)),X3) = mult(X1,X3),
inference(orient,[status(thm)],[t2637]) ).
cnf(t1684,plain,
mult(mult(X1,ld(X1,rd(X2,X2))),X3) = mult(rd(rd(X1,X1),rd(rd(X2,X2),rd(X2,X2))),X3),
inference(cp,[status(thm)],[t1677,t1336]) ).
cnf(t2641,plain,
mult(X1,ld(X1,mult(rd(X2,X2),X3))) = mult(rd(rd(X1,X1),rd(rd(X2,X2),rd(X2,X2))),X3),
inference(step,[status(thm)],[t1684,t680]) ).
cnf(t2642,plain,
mult(X1,ld(X1,mult(X2,ld(X2,X3)))) = mult(rd(rd(X1,X1),rd(rd(X2,X2),rd(X2,X2))),X3),
inference(step,[status(thm)],[t2641,t1308]) ).
cnf(t2643,plain,
mult(X1,ld(X1,mult(X2,ld(X2,X3)))) = mult(rd(X1,X1),X3),
inference(step,[status(thm)],[t2642,t1677]) ).
cnf(t2644,plain,
mult(X1,ld(X1,mult(X2,ld(X2,X3)))) = mult(X1,ld(X1,X3)),
inference(step,[status(thm)],[t2643,t1308]) ).
cnf(t1724,plain,
mult(X1,ld(X1,mult(X2,ld(X2,X3)))) = mult(X1,ld(X1,X3)),
inference(orient,[status(thm)],[t2644]) ).
cnf(t2546,plain,
mult(ld(X1,X2),ld(ld(X1,X2),mult(X3,X4))) = mult(X1,ld(X1,mult(X3,X4))),
inference(step,[status(thm)],[t19,t680]) ).
cnf(t681,plain,
mult(ld(X1,X2),ld(ld(X1,X2),mult(X3,X4))) = mult(X1,ld(X1,mult(X3,X4))),
inference(orient,[status(thm)],[t2546]) ).
cnf(t1728,plain,
mult(ld(X1,X2),ld(ld(X1,X2),X3)) = mult(X1,ld(X1,mult(X4,ld(X4,X3)))),
inference(cp,[status(thm)],[t1724,t681]) ).
cnf(t2651,plain,
mult(ld(X1,X2),ld(ld(X1,X2),X3)) = mult(X1,ld(X1,X3)),
inference(step,[status(thm)],[t1728,t1724]) ).
cnf(t1838,plain,
mult(ld(X1,X2),ld(ld(X1,X2),X3)) = mult(X1,ld(X1,X3)),
inference(orient,[status(thm)],[t2651]) ).
cnf(t0,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t11,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t1847,plain,
mult(X1,ld(X1,ld(X1,X2))) = mult(ld(X1,X2),rd(ld(X1,X2),ld(X1,X2))),
inference(cp,[status(thm)],[t1838,t42]) ).
cnf(t2569,plain,
mult(X1,rd(X2,X2)) = rd(X1,rd(X2,X2)),
inference(step,[status(thm)],[t763,t794]) ).
cnf(t799,plain,
mult(X1,rd(X2,X2)) = rd(X1,rd(X2,X2)),
inference(orient,[status(thm)],[t2569]) ).
cnf(t2654,plain,
mult(X1,ld(X1,ld(X1,X2))) = rd(ld(X1,X2),rd(ld(X1,X2),ld(X1,X2))),
inference(step,[status(thm)],[t1847,t799]) ).
cnf(t2655,plain,
mult(X1,ld(X1,ld(X1,X2))) = rd(ld(X1,X2),rd(X2,X2)),
inference(step,[status(thm)],[t2654,t1056]) ).
cnf(t1057,plain,
rd(ld(X1,X2),rd(X2,X2)) = ld(X1,X2),
inference(cp,[status(thm)],[t1056,t89]) ).
cnf(t1097,plain,
rd(ld(X1,X2),rd(X2,X2)) = ld(X1,X2),
inference(orient,[status(thm)],[t1057]) ).
cnf(t2656,plain,
mult(X1,ld(X1,ld(X1,X2))) = ld(X1,X2),
inference(step,[status(thm)],[t2655,t1097]) ).
cnf(t1864,plain,
mult(X1,ld(X1,ld(X1,X2))) = ld(X1,X2),
inference(orient,[status(thm)],[t2656]) ).
cnf(t1738,plain,
mult(X1,mult(X2,ld(X2,X3))) = mult(X1,mult(X1,ld(X1,X3))),
inference(cp,[status(thm)],[t731,t1724]) ).
cnf(t2645,plain,
mult(X1,mult(X2,ld(X2,X3))) = mult(X1,X3),
inference(step,[status(thm)],[t1738,t731]) ).
cnf(t1746,plain,
mult(X1,mult(X2,ld(X2,X3))) = mult(X1,X3),
inference(orient,[status(thm)],[t2645]) ).
cnf(t2607,plain,
mult(rd(rd(X1,X1),rd(X2,X2)),X3) = mult(X1,ld(X1,mult(X2,ld(X2,X3)))),
inference(step,[status(thm)],[t1271,t1308]) ).
cnf(t1309,plain,
mult(rd(rd(X1,X1),rd(X2,X2)),X3) = mult(X1,ld(X1,mult(X2,ld(X2,X3)))),
inference(orient,[status(thm)],[t2607]) ).
cnf(t1314,plain,
mult(rd(X1,X1),ld(rd(X1,X1),X2)) = mult(X1,ld(X1,mult(X1,ld(X1,X2)))),
inference(cp,[status(thm)],[t1308,t1309]) ).
cnf(t2610,plain,
mult(X1,ld(X1,ld(rd(X1,X1),X2))) = mult(X1,ld(X1,mult(X1,ld(X1,X2)))),
inference(step,[status(thm)],[t1314,t1308]) ).
cnf(t2611,plain,
mult(X1,ld(X1,ld(rd(X1,X1),X2))) = mult(X1,mult(X1,ld(X1,ld(X1,X2)))),
inference(step,[status(thm)],[t2610,t12]) ).
cnf(t2612,plain,
mult(X1,ld(X1,ld(rd(X1,X1),X2))) = mult(X1,ld(X1,X2)),
inference(step,[status(thm)],[t2611,t731]) ).
cnf(t1355,plain,
mult(X1,ld(X1,ld(rd(X1,X1),X2))) = mult(X1,ld(X1,X2)),
inference(orient,[status(thm)],[t2612]) ).
cnf(t1748,plain,
mult(X1,ld(rd(X2,X2),X3)) = mult(X1,mult(X2,ld(X2,X3))),
inference(cp,[status(thm)],[t1746,t1355]) ).
cnf(t2648,plain,
mult(X1,ld(rd(X2,X2),X3)) = mult(X1,X3),
inference(step,[status(thm)],[t1748,t1746]) ).
cnf(t1772,plain,
mult(X1,ld(rd(X2,X2),X3)) = mult(X1,X3),
inference(orient,[status(thm)],[t2648]) ).
cnf(t1867,plain,
ld(rd(X1,X1),X2) = mult(rd(X1,X1),ld(rd(X1,X1),X2)),
inference(cp,[status(thm)],[t1864,t1772]) ).
cnf(t2659,plain,
ld(rd(X1,X1),X2) = mult(X1,ld(X1,ld(rd(X1,X1),X2))),
inference(step,[status(thm)],[t1867,t1308]) ).
cnf(t2660,plain,
ld(rd(X1,X1),X2) = mult(X1,ld(X1,X2)),
inference(step,[status(thm)],[t2659,t1355]) ).
cnf(t1877,plain,
ld(rd(X1,X1),X2) = mult(X1,ld(X1,X2)),
inference(orient,[status(thm)],[t2660]) ).
cnf(t1725,plain,
mult(X1,ld(X1,X2)) = mult(mult(X1,X3),ld(mult(X1,X3),X2)),
inference(cp,[status(thm)],[t1724,t1557]) ).
cnf(t1794,plain,
mult(mult(X1,X2),ld(mult(X1,X2),X3)) = mult(X1,ld(X1,X3)),
inference(orient,[status(thm)],[t1725]) ).
cnf(t1803,plain,
mult(X1,ld(X1,X2)) = mult(rd(X1,rd(X3,X3)),ld(mult(X1,rd(X3,X3)),X2)),
inference(cp,[status(thm)],[t1794,t799]) ).
cnf(t2668,plain,
mult(X1,ld(X1,X2)) = mult(X1,ld(mult(X1,rd(X3,X3)),X2)),
inference(step,[status(thm)],[t1803,t1677]) ).
cnf(t2669,plain,
mult(X1,ld(X1,X2)) = mult(X1,ld(rd(X1,rd(X3,X3)),X2)),
inference(step,[status(thm)],[t2668,t799]) ).
cnf(t1938,plain,
mult(X1,ld(rd(X1,rd(X2,X2)),X3)) = mult(X1,ld(X1,X3)),
inference(orient,[status(thm)],[t2669]) ).
cnf(t1944,plain,
mult(X1,ld(X1,ld(rd(X1,rd(X2,X2)),X3))) = ld(X1,mult(X1,ld(X1,X3))),
inference(cp,[status(thm)],[t12,t1938]) ).
cnf(t2689,plain,
mult(X1,ld(X1,ld(rd(X1,rd(X2,X2)),X3))) = mult(X1,ld(X1,ld(X1,X3))),
inference(step,[status(thm)],[t1944,t12]) ).
cnf(t2690,plain,
mult(X1,ld(X1,ld(rd(X1,rd(X2,X2)),X3))) = ld(X1,X3),
inference(step,[status(thm)],[t2689,t1864]) ).
cnf(t2149,plain,
mult(X1,ld(X1,ld(rd(X1,rd(X2,X2)),X3))) = ld(X1,X3),
inference(orient,[status(thm)],[t2690]) ).
cnf(t2151,plain,
ld(rd(X1,rd(X2,X2)),X3) = mult(X1,ld(rd(X1,rd(X2,X2)),ld(rd(rd(X1,rd(X2,X2)),rd(X4,X4)),X3))),
inference(cp,[status(thm)],[t2149,t1677]) ).
cnf(t2691,plain,
ld(rd(X1,rd(X2,X2)),X3) = mult(X1,ld(X1,ld(rd(rd(X1,rd(X2,X2)),rd(X4,X4)),X3))),
inference(step,[status(thm)],[t2151,t1938]) ).
cnf(t2692,plain,
ld(rd(X1,rd(X2,X2)),X3) = mult(X1,ld(X1,ld(rd(X1,rd(X4,X4)),X3))),
inference(step,[status(thm)],[t2691,t1641]) ).
cnf(t2693,plain,
ld(rd(X1,rd(X2,X2)),X3) = ld(X1,X3),
inference(step,[status(thm)],[t2692,t2149]) ).
cnf(t2178,plain,
ld(rd(X1,rd(X2,X2)),X3) = ld(X1,X3),
inference(orient,[status(thm)],[t2693]) ).
cnf(t2179,plain,
ld(X1,rd(X1,rd(X2,X2))) = rd(rd(X1,rd(X2,X2)),rd(X1,rd(X2,X2))),
inference(cp,[status(thm)],[t2178,t42]) ).
cnf(t769,plain,
mult(X1,ld(X1,rd(X2,X2))) = ld(X1,rd(mult(X1,X2),X2)),
inference(cp,[status(thm)],[t12,t763]) ).
cnf(t2595,plain,
rd(rd(X1,X1),rd(X2,X2)) = ld(X1,rd(mult(X1,X2),X2)),
inference(step,[status(thm)],[t769,t401]) ).
cnf(t2596,plain,
rd(rd(X1,X1),rd(X2,X2)) = ld(X1,rd(X1,rd(X2,X2))),
inference(step,[status(thm)],[t2595,t794]) ).
cnf(t846,plain,
ld(X1,rd(X1,rd(X2,X2))) = rd(rd(X1,X1),rd(X2,X2)),
inference(orient,[status(thm)],[t2596]) ).
cnf(t2694,plain,
rd(rd(X1,X1),rd(X2,X2)) = rd(rd(X1,rd(X2,X2)),rd(X1,rd(X2,X2))),
inference(step,[status(thm)],[t2179,t846]) ).
cnf(t2571,plain,
rd(rd(X1,rd(X2,X2)),X2) = rd(X1,X2),
inference(step,[status(thm)],[t126,t794]) ).
cnf(t812,plain,
rd(rd(X1,rd(X2,X2)),X2) = rd(X1,X2),
inference(rw,[status(thm)],[t2571]) ).
cnf(t832,plain,
rd(rd(X1,rd(X2,X2)),X2) = rd(X1,X2),
inference(orient,[status(thm)],[t812]) ).
cnf(t1671,plain,
rd(rd(X1,rd(X2,X2)),X3) = rd(rd(X1,rd(X3,X3)),X3),
inference(cp,[status(thm)],[t832,t1641]) ).
cnf(t2640,plain,
rd(rd(X1,rd(X2,X2)),X3) = rd(X1,X3),
inference(step,[status(thm)],[t1671,t832]) ).
cnf(t1695,plain,
rd(rd(X1,rd(X2,X2)),X3) = rd(X1,X3),
inference(orient,[status(thm)],[t2640]) ).
cnf(t2695,plain,
rd(rd(X1,X1),rd(X2,X2)) = rd(X1,rd(X1,rd(X2,X2))),
inference(step,[status(thm)],[t2694,t1695]) ).
cnf(t2188,plain,
rd(rd(X1,X1),rd(X2,X2)) = rd(X1,rd(X1,rd(X2,X2))),
inference(orient,[status(thm)],[t2695]) ).
cnf(t2700,plain,
rd(mult(X1,ld(X1,X2)),X2) = rd(X1,rd(X1,rd(X2,X2))),
inference(step,[status(thm)],[t1336,t2188]) ).
cnf(t2193,plain,
rd(mult(X1,ld(X1,X2)),X2) = rd(X1,rd(X1,rd(X2,X2))),
inference(orient,[status(thm)],[t2700]) ).
cnf(t29,plain,
mult(rd(X1,X2),ld(rd(X1,X2),X2)) = ld(rd(X1,X2),rd(mult(X1,X2),X2)),
inference(cp,[status(thm)],[t12,t26]) ).
cnf(t261,plain,
ld(rd(X1,X2),rd(mult(X1,X2),X2)) = mult(rd(X1,X2),ld(rd(X1,X2),X2)),
inference(orient,[status(thm)],[t29]) ).
cnf(t2572,plain,
ld(rd(X1,X2),rd(X1,rd(X2,X2))) = mult(rd(X1,X2),ld(rd(X1,X2),X2)),
inference(step,[status(thm)],[t261,t794]) ).
cnf(t813,plain,
ld(rd(X1,X2),rd(X1,rd(X2,X2))) = mult(rd(X1,X2),ld(rd(X1,X2),X2)),
inference(rw,[status(thm)],[t2572]) ).
cnf(t2343,plain,
ld(rd(X1,X2),rd(X1,rd(X2,X2))) = mult(rd(X1,X2),ld(rd(X1,X2),X2)),
inference(orient,[status(thm)],[t813]) ).
cnf(t2389,plain,
rd(rd(X1,X2),rd(rd(X1,X2),rd(rd(X1,rd(X2,X2)),rd(X1,rd(X2,X2))))) = rd(mult(rd(X1,X2),mult(rd(X1,X2),ld(rd(X1,X2),X2))),rd(X1,rd(X2,X2))),
inference(cp,[status(thm)],[t2193,t2343]) ).
cnf(t2723,plain,
rd(rd(X1,X2),rd(rd(X1,X2),rd(rd(X2,X2),rd(X2,X2)))) = rd(mult(rd(X1,X2),mult(rd(X1,X2),ld(rd(X1,X2),X2))),rd(X1,rd(X2,X2))),
inference(step,[status(thm)],[t2389,t962]) ).
cnf(t2724,plain,
rd(rd(X1,X2),rd(rd(X1,X2),rd(X2,X2))) = rd(mult(rd(X1,X2),mult(rd(X1,X2),ld(rd(X1,X2),X2))),rd(X1,rd(X2,X2))),
inference(step,[status(thm)],[t2723,t962]) ).
cnf(t809,plain,
rd(rd(X1,X2),rd(X2,X2)) = rd(rd(X1,rd(X2,X2)),X2),
inference(cp,[status(thm)],[t794,t795]) ).
cnf(t2597,plain,
rd(rd(X1,X2),rd(X2,X2)) = rd(X1,X2),
inference(step,[status(thm)],[t809,t832]) ).
cnf(t853,plain,
rd(rd(X1,X2),rd(X2,X2)) = rd(X1,X2),
inference(orient,[status(thm)],[t2597]) ).
cnf(t2725,plain,
rd(rd(X1,X2),rd(X1,X2)) = rd(mult(rd(X1,X2),mult(rd(X1,X2),ld(rd(X1,X2),X2))),rd(X1,rd(X2,X2))),
inference(step,[status(thm)],[t2724,t853]) ).
cnf(t2726,plain,
rd(rd(X1,X2),rd(X1,X2)) = rd(mult(rd(X1,X2),X2),rd(X1,rd(X2,X2))),
inference(step,[status(thm)],[t2725,t1746]) ).
cnf(t2727,plain,
rd(rd(X1,X2),rd(X1,X2)) = rd(rd(X1,rd(X2,X2)),rd(X1,rd(X2,X2))),
inference(step,[status(thm)],[t2726,t795]) ).
cnf(t2728,plain,
rd(rd(X1,X2),rd(X1,X2)) = rd(X1,rd(X1,rd(X2,X2))),
inference(step,[status(thm)],[t2727,t1695]) ).
cnf(t2435,plain,
rd(rd(X1,X2),rd(X1,X2)) = rd(X1,rd(X1,rd(X2,X2))),
inference(orient,[status(thm)],[t2728]) ).
cnf(t2439,plain,
mult(rd(X1,X2),ld(rd(X1,X2),X3)) = ld(rd(X1,rd(X1,rd(X2,X2))),X3),
inference(cp,[status(thm)],[t1877,t2435]) ).
cnf(t2204,plain,
ld(rd(X1,X1),X2) = ld(rd(X1,rd(X1,rd(X3,X3))),X2),
inference(cp,[status(thm)],[t2178,t2188]) ).
cnf(t2702,plain,
mult(X1,ld(X1,X2)) = ld(rd(X1,rd(X1,rd(X3,X3))),X2),
inference(step,[status(thm)],[t2204,t1877]) ).
cnf(t2233,plain,
ld(rd(X1,rd(X1,rd(X2,X2))),X3) = mult(X1,ld(X1,X3)),
inference(orient,[status(thm)],[t2702]) ).
cnf(t2732,plain,
mult(rd(X1,X2),ld(rd(X1,X2),X3)) = mult(X1,ld(X1,X3)),
inference(step,[status(thm)],[t2439,t2233]) ).
cnf(t2471,plain,
mult(rd(X1,X2),ld(rd(X1,X2),X3)) = mult(X1,ld(X1,X3)),
inference(orient,[status(thm)],[t2732]) ).
fof(f7,conjecture,
! [X0,X1,X2] :
( ld(rd(X0,X1),mult(rd(X0,X1),X2)) = ld(X0,mult(X0,X2))
& ld(ld(X0,X1),mult(ld(X0,X1),X2)) = ld(X0,mult(X0,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f7_neg,negated_conjecture,
~ ! [X0,X1,X2] :
( ld(rd(X0,X1),mult(rd(X0,X1),X2)) = ld(X0,mult(X0,X2))
& ld(ld(X0,X1),mult(ld(X0,X1),X2)) = ld(X0,mult(X0,X2)) ),
inference(negated_conjecture,[status(cth)],[f7]) ).
fof(f7_nnf,plain,
? [X0,X1,X2] :
( ld(rd(X0,X1),mult(rd(X0,X1),X2)) != ld(X0,mult(X0,X2))
| ld(ld(X0,X1),mult(ld(X0,X1),X2)) != ld(X0,mult(X0,X2)) ),
inference(nnf_transformation,[status(thm)],[f7_neg]) ).
fof(f7_sk,plain,
( ld(rd(sk0,sk1),mult(rd(sk0,sk1),sk2)) != ld(sk0,mult(sk0,sk2))
| ld(ld(sk0,sk1),mult(ld(sk0,sk1),sk2)) != ld(sk0,mult(sk0,sk2)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2])],[f7_nnf]) ).
cnf(c7,plain,
( ld(rd(sk0,sk1),mult(rd(sk0,sk1),sk2)) != ld(sk0,mult(sk0,sk2))
| ld(ld(sk0,sk1),mult(ld(sk0,sk1),sk2)) != ld(sk0,mult(sk0,sk2)) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(g0_0,plain,
true != ifeq(mult(ld(sk0,sk1),ld(ld(sk0,sk1),sk2)),mult(sk0,ld(sk0,sk2)),ifeq(mult(rd(sk0,sk1),ld(rd(sk0,sk1),sk2)),mult(sk0,ld(sk0,sk2)),false,true),true),
inference(rw,[status(thm)],[goal_0]) ).
cnf(g0_1,plain,
true != ifeq(mult(sk0,ld(sk0,sk2)),mult(sk0,ld(sk0,sk2)),ifeq(mult(rd(sk0,sk1),ld(rd(sk0,sk1),sk2)),mult(sk0,ld(sk0,sk2)),false,true),true),
inference(rw,[status(thm)],[g0_0,t1838]) ).
cnf(g0_2,plain,
true != ifeq(mult(rd(sk0,sk1),ld(rd(sk0,sk1),sk2)),mult(sk0,ld(sk0,sk2)),false,true),
inference(rw,[status(thm)],[g0_1,t11]) ).
cnf(g0_3,plain,
true != ifeq(mult(sk0,ld(sk0,sk2)),mult(sk0,ld(sk0,sk2)),false,true),
inference(rw,[status(thm)],[g0_2,t2471]) ).
cnf(g0_4,plain,
true != false,
inference(rw,[status(thm)],[g0_3,t11]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP682+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n009.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 15:41:43 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 6.30/1.38 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.30/1.38 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------