Prover9---2026-6A.UNS-CRf.s

%------------------------------------------------------------------------------
% File     : Prover9---2026-6A
% Problem  : GRP180-2 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm  : none
% Format   : tptp:raw
% Command  : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p

% Computer : n007.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 : Sun Sep 27 07:28:15 AM UTC 2026

% Result   : Unsatisfiable 224.27s 29.96s
% Output   : CNFRefutation 224.27s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :  166
%            Number of leaves      :   19
% Syntax   : Number of formulae    :  600 ( 600 unt;   0 def)
%            Number of atoms       :  600 ( 599 equ)
%            Maximal formula atoms :    1 (   1 avg)
%            Number of connectives :   50 (  50   ~;   0   |;   0   &)
%                                         (   0 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    4 (   1 avg)
%            Maximal term depth    :   14 (   2 avg)
%            Number of predicates  :    2 (   0 usr;   1 prp; 0-2 aty)
%            Number of functors    :    7 (   7 usr;   3 con; 0-2 aty)
%            Number of variables   : 1080 (  26 sgn  36   !;   0   ?)

% Comments : 
%------------------------------------------------------------------------------
fof(left_identity,axiom,
    ! [VAR_0] : multiply(identity,VAR_0) = VAR_0,
    file('theBenchmark.p',left_identity) ).

cnf(c_1,plain,
    multiply(identity,A) = A,
    inference(clausify,[status(thm)],[left_identity]) ).

fof(left_inverse,axiom,
    ! [VAR_0] : multiply(inverse(VAR_0),VAR_0) = identity,
    file('theBenchmark.p',left_inverse) ).

cnf(c_2,plain,
    multiply(inverse(A),A) = identity,
    inference(clausify,[status(thm)],[left_inverse]) ).

fof(associativity,axiom,
    ! [VAR_0,VAR_1,VAR_2] : multiply(multiply(VAR_0,VAR_1),VAR_2) = multiply(VAR_0,multiply(VAR_1,VAR_2)),
    file('theBenchmark.p',associativity) ).

cnf(c_3,plain,
    multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
    inference(clausify,[status(thm)],[associativity]) ).

fof(symmetry_of_glb,axiom,
    ! [VAR_0,VAR_1] : greatest_lower_bound(VAR_0,VAR_1) = greatest_lower_bound(VAR_1,VAR_0),
    file('theBenchmark.p',symmetry_of_glb) ).

cnf(c_4,plain,
    greatest_lower_bound(A,B) = greatest_lower_bound(B,A),
    inference(clausify,[status(thm)],[symmetry_of_glb]) ).

fof(symmetry_of_lub,axiom,
    ! [VAR_0,VAR_1] : least_upper_bound(VAR_0,VAR_1) = least_upper_bound(VAR_1,VAR_0),
    file('theBenchmark.p',symmetry_of_lub) ).

cnf(c_5,plain,
    least_upper_bound(A,B) = least_upper_bound(B,A),
    inference(clausify,[status(thm)],[symmetry_of_lub]) ).

fof(associativity_of_glb,axiom,
    ! [VAR_0,VAR_1,VAR_2] : greatest_lower_bound(VAR_0,greatest_lower_bound(VAR_1,VAR_2)) = greatest_lower_bound(greatest_lower_bound(VAR_0,VAR_1),VAR_2),
    file('theBenchmark.p',associativity_of_glb) ).

cnf(c_6,plain,
    greatest_lower_bound(A,greatest_lower_bound(B,C)) = greatest_lower_bound(greatest_lower_bound(A,B),C),
    inference(clausify,[status(thm)],[associativity_of_glb]) ).

cnf(c_7,plain,
    greatest_lower_bound(greatest_lower_bound(A,B),C) = greatest_lower_bound(A,greatest_lower_bound(B,C)),
    inference(copy,[status(thm)],[c_6]) ).

fof(associativity_of_lub,axiom,
    ! [VAR_0,VAR_1,VAR_2] : least_upper_bound(VAR_0,least_upper_bound(VAR_1,VAR_2)) = least_upper_bound(least_upper_bound(VAR_0,VAR_1),VAR_2),
    file('theBenchmark.p',associativity_of_lub) ).

cnf(c_8,plain,
    least_upper_bound(A,least_upper_bound(B,C)) = least_upper_bound(least_upper_bound(A,B),C),
    inference(clausify,[status(thm)],[associativity_of_lub]) ).

cnf(c_9,plain,
    least_upper_bound(least_upper_bound(A,B),C) = least_upper_bound(A,least_upper_bound(B,C)),
    inference(copy,[status(thm)],[c_8]) ).

fof(idempotence_of_lub,axiom,
    ! [VAR_0] : least_upper_bound(VAR_0,VAR_0) = VAR_0,
    file('theBenchmark.p',idempotence_of_lub) ).

cnf(c_10,plain,
    least_upper_bound(A,A) = A,
    inference(clausify,[status(thm)],[idempotence_of_lub]) ).

fof(idempotence_of_gld,axiom,
    ! [VAR_0] : greatest_lower_bound(VAR_0,VAR_0) = VAR_0,
    file('theBenchmark.p',idempotence_of_gld) ).

cnf(c_11,plain,
    greatest_lower_bound(A,A) = A,
    inference(clausify,[status(thm)],[idempotence_of_gld]) ).

fof(lub_absorbtion,axiom,
    ! [VAR_0,VAR_1] : least_upper_bound(VAR_0,greatest_lower_bound(VAR_0,VAR_1)) = VAR_0,
    file('theBenchmark.p',lub_absorbtion) ).

cnf(c_12,plain,
    least_upper_bound(A,greatest_lower_bound(A,B)) = A,
    inference(clausify,[status(thm)],[lub_absorbtion]) ).

fof(glb_absorbtion,axiom,
    ! [VAR_0,VAR_1] : greatest_lower_bound(VAR_0,least_upper_bound(VAR_0,VAR_1)) = VAR_0,
    file('theBenchmark.p',glb_absorbtion) ).

cnf(c_13,plain,
    greatest_lower_bound(A,least_upper_bound(A,B)) = A,
    inference(clausify,[status(thm)],[glb_absorbtion]) ).

fof(monotony_lub1,axiom,
    ! [VAR_0,VAR_1,VAR_2] : multiply(VAR_0,least_upper_bound(VAR_1,VAR_2)) = least_upper_bound(multiply(VAR_0,VAR_1),multiply(VAR_0,VAR_2)),
    file('theBenchmark.p',monotony_lub1) ).

cnf(c_14,plain,
    multiply(A,least_upper_bound(B,C)) = least_upper_bound(multiply(A,B),multiply(A,C)),
    inference(clausify,[status(thm)],[monotony_lub1]) ).

cnf(c_15,plain,
    least_upper_bound(multiply(A,B),multiply(A,C)) = multiply(A,least_upper_bound(B,C)),
    inference(copy,[status(thm)],[c_14]) ).

fof(monotony_glb1,axiom,
    ! [VAR_0,VAR_1,VAR_2] : multiply(VAR_0,greatest_lower_bound(VAR_1,VAR_2)) = greatest_lower_bound(multiply(VAR_0,VAR_1),multiply(VAR_0,VAR_2)),
    file('theBenchmark.p',monotony_glb1) ).

cnf(c_16,plain,
    multiply(A,greatest_lower_bound(B,C)) = greatest_lower_bound(multiply(A,B),multiply(A,C)),
    inference(clausify,[status(thm)],[monotony_glb1]) ).

cnf(c_17,plain,
    greatest_lower_bound(multiply(A,B),multiply(A,C)) = multiply(A,greatest_lower_bound(B,C)),
    inference(copy,[status(thm)],[c_16]) ).

fof(monotony_lub2,axiom,
    ! [VAR_0,VAR_1,VAR_2] : multiply(least_upper_bound(VAR_0,VAR_1),VAR_2) = least_upper_bound(multiply(VAR_0,VAR_2),multiply(VAR_1,VAR_2)),
    file('theBenchmark.p',monotony_lub2) ).

cnf(c_18,plain,
    multiply(least_upper_bound(A,B),C) = least_upper_bound(multiply(A,C),multiply(B,C)),
    inference(clausify,[status(thm)],[monotony_lub2]) ).

cnf(c_19,plain,
    least_upper_bound(multiply(A,B),multiply(C,B)) = multiply(least_upper_bound(A,C),B),
    inference(copy,[status(thm)],[c_18]) ).

fof(monotony_glb2,axiom,
    ! [VAR_0,VAR_1,VAR_2] : multiply(greatest_lower_bound(VAR_0,VAR_1),VAR_2) = greatest_lower_bound(multiply(VAR_0,VAR_2),multiply(VAR_1,VAR_2)),
    file('theBenchmark.p',monotony_glb2) ).

cnf(c_20,plain,
    multiply(greatest_lower_bound(A,B),C) = greatest_lower_bound(multiply(A,C),multiply(B,C)),
    inference(clausify,[status(thm)],[monotony_glb2]) ).

cnf(c_21,plain,
    greatest_lower_bound(multiply(A,B),multiply(C,B)) = multiply(greatest_lower_bound(A,C),B),
    inference(copy,[status(thm)],[c_20]) ).

fof(p11_1,axiom,
    inverse(identity) = identity,
    file('theBenchmark.p',p11_1) ).

cnf(c_22,plain,
    inverse(identity) = identity,
    inference(clausify,[status(thm)],[p11_1]) ).

fof(p11_2,axiom,
    ! [VAR_0] : inverse(inverse(VAR_0)) = VAR_0,
    file('theBenchmark.p',p11_2) ).

cnf(c_23,plain,
    inverse(inverse(A)) = A,
    inference(clausify,[status(thm)],[p11_2]) ).

fof(p11_3,axiom,
    ! [VAR_0,VAR_1] : inverse(multiply(VAR_0,VAR_1)) = multiply(inverse(VAR_1),inverse(VAR_0)),
    file('theBenchmark.p',p11_3) ).

cnf(c_24,plain,
    inverse(multiply(A,B)) = multiply(inverse(B),inverse(A)),
    inference(clausify,[status(thm)],[p11_3]) ).

fof(prove_p11,axiom,
    multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)) != least_upper_bound(a,b),
    file('theBenchmark.p',prove_p11) ).

cnf(c_25,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)) != least_upper_bound(a,b),
    inference(clausify,[status(thm)],[prove_p11]) ).

cnf(c_26,plain,
    least_upper_bound(a,b) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(copy,[status(thm)],[c_25]) ).

cnf(c_11089,plain,
    multiply(identity,A) = multiply(inverse(B),multiply(B,A)),
    inference(paramod,[status(thm)],[c_2,c_3]) ).

cnf(c_11090,plain,
    A = multiply(inverse(B),multiply(B,A)),
    inference(paramod,[status(thm)],[c_1,c_11089]) ).

cnf(c_27,plain,
    multiply(inverse(A),multiply(A,B)) = B,
    inference(copy,[status(thm)],[c_11090]) ).

cnf(c_11091,plain,
    greatest_lower_bound(greatest_lower_bound(A,B),C) = greatest_lower_bound(B,greatest_lower_bound(A,C)),
    inference(paramod,[status(thm)],[c_4,c_7]) ).

cnf(c_29,plain,
    greatest_lower_bound(A,greatest_lower_bound(B,C)) = greatest_lower_bound(B,greatest_lower_bound(A,C)),
    inference(paramod,[status(thm)],[c_7,c_11091]) ).

cnf(c_11092,plain,
    least_upper_bound(least_upper_bound(A,B),C) = least_upper_bound(B,least_upper_bound(A,C)),
    inference(paramod,[status(thm)],[c_5,c_9]) ).

cnf(c_31,plain,
    least_upper_bound(A,least_upper_bound(B,C)) = least_upper_bound(B,least_upper_bound(A,C)),
    inference(paramod,[status(thm)],[c_9,c_11092]) ).

cnf(c_11093,plain,
    least_upper_bound(A,B) = least_upper_bound(A,least_upper_bound(A,B)),
    inference(paramod,[status(thm)],[c_10,c_9]) ).

cnf(c_32,plain,
    least_upper_bound(A,least_upper_bound(A,B)) = least_upper_bound(A,B),
    inference(copy,[status(thm)],[c_11093]) ).

cnf(c_11094,plain,
    least_upper_bound(least_upper_bound(A,B),B) = least_upper_bound(A,B),
    inference(paramod,[status(thm)],[c_10,c_9]) ).

cnf(c_34,plain,
    least_upper_bound(A,least_upper_bound(B,A)) = least_upper_bound(B,A),
    inference(paramod,[status(thm)],[c_5,c_11094]) ).

cnf(c_11095,plain,
    greatest_lower_bound(A,B) = greatest_lower_bound(A,greatest_lower_bound(A,B)),
    inference(paramod,[status(thm)],[c_11,c_7]) ).

cnf(c_35,plain,
    greatest_lower_bound(A,greatest_lower_bound(A,B)) = greatest_lower_bound(A,B),
    inference(copy,[status(thm)],[c_11095]) ).

cnf(c_11096,plain,
    greatest_lower_bound(greatest_lower_bound(A,B),B) = greatest_lower_bound(A,B),
    inference(paramod,[status(thm)],[c_11,c_7]) ).

cnf(c_37,plain,
    greatest_lower_bound(A,greatest_lower_bound(B,A)) = greatest_lower_bound(B,A),
    inference(paramod,[status(thm)],[c_4,c_11096]) ).

cnf(c_38,plain,
    least_upper_bound(A,greatest_lower_bound(B,A)) = A,
    inference(paramod,[status(thm)],[c_4,c_12]) ).

cnf(c_39,plain,
    least_upper_bound(greatest_lower_bound(A,B),greatest_lower_bound(A,greatest_lower_bound(B,C))) = greatest_lower_bound(A,B),
    inference(paramod,[status(thm)],[c_7,c_12]) ).

cnf(c_11097,plain,
    least_upper_bound(A,B) = least_upper_bound(A,least_upper_bound(greatest_lower_bound(A,C),B)),
    inference(paramod,[status(thm)],[c_12,c_9]) ).

cnf(c_40,plain,
    least_upper_bound(A,least_upper_bound(greatest_lower_bound(A,B),C)) = least_upper_bound(A,C),
    inference(copy,[status(thm)],[c_11097]) ).

cnf(c_42,plain,
    greatest_lower_bound(A,least_upper_bound(B,A)) = A,
    inference(paramod,[status(thm)],[c_5,c_13]) ).

cnf(c_45,plain,
    greatest_lower_bound(least_upper_bound(A,B),least_upper_bound(A,least_upper_bound(B,C))) = least_upper_bound(A,B),
    inference(paramod,[status(thm)],[c_9,c_13]) ).

cnf(c_46,plain,
    least_upper_bound(identity,multiply(inverse(A),B)) = multiply(inverse(A),least_upper_bound(A,B)),
    inference(paramod,[status(thm)],[c_2,c_15]) ).

cnf(c_11098,plain,
    least_upper_bound(multiply(inverse(A),B),identity) = multiply(inverse(A),least_upper_bound(B,A)),
    inference(paramod,[status(thm)],[c_2,c_15]) ).

cnf(c_47,plain,
    least_upper_bound(identity,multiply(inverse(A),B)) = multiply(inverse(A),least_upper_bound(B,A)),
    inference(paramod,[status(thm)],[c_5,c_11098]) ).

cnf(c_49,plain,
    greatest_lower_bound(identity,multiply(inverse(A),B)) = multiply(inverse(A),greatest_lower_bound(A,B)),
    inference(paramod,[status(thm)],[c_2,c_17]) ).

cnf(c_11099,plain,
    greatest_lower_bound(multiply(inverse(A),B),identity) = multiply(inverse(A),greatest_lower_bound(B,A)),
    inference(paramod,[status(thm)],[c_2,c_17]) ).

cnf(c_50,plain,
    greatest_lower_bound(identity,multiply(inverse(A),B)) = multiply(inverse(A),greatest_lower_bound(B,A)),
    inference(paramod,[status(thm)],[c_4,c_11099]) ).

cnf(c_52,plain,
    least_upper_bound(A,multiply(B,A)) = multiply(least_upper_bound(identity,B),A),
    inference(paramod,[status(thm)],[c_1,c_19]) ).

cnf(c_11100,plain,
    least_upper_bound(multiply(A,B),B) = multiply(least_upper_bound(A,identity),B),
    inference(paramod,[status(thm)],[c_1,c_19]) ).

cnf(c_53,plain,
    least_upper_bound(A,multiply(B,A)) = multiply(least_upper_bound(B,identity),A),
    inference(paramod,[status(thm)],[c_5,c_11100]) ).

cnf(c_11101,plain,
    least_upper_bound(multiply(A,B),identity) = multiply(least_upper_bound(A,inverse(B)),B),
    inference(paramod,[status(thm)],[c_2,c_19]) ).

cnf(c_55,plain,
    least_upper_bound(identity,multiply(A,B)) = multiply(least_upper_bound(A,inverse(B)),B),
    inference(paramod,[status(thm)],[c_5,c_11101]) ).

cnf(c_59,plain,
    greatest_lower_bound(A,multiply(B,A)) = multiply(greatest_lower_bound(identity,B),A),
    inference(paramod,[status(thm)],[c_1,c_21]) ).

cnf(c_11102,plain,
    greatest_lower_bound(multiply(A,B),B) = multiply(greatest_lower_bound(A,identity),B),
    inference(paramod,[status(thm)],[c_1,c_21]) ).

cnf(c_60,plain,
    greatest_lower_bound(A,multiply(B,A)) = multiply(greatest_lower_bound(B,identity),A),
    inference(paramod,[status(thm)],[c_4,c_11102]) ).

cnf(c_11103,plain,
    greatest_lower_bound(multiply(A,B),identity) = multiply(greatest_lower_bound(A,inverse(B)),B),
    inference(paramod,[status(thm)],[c_2,c_21]) ).

cnf(c_62,plain,
    greatest_lower_bound(identity,multiply(A,B)) = multiply(greatest_lower_bound(A,inverse(B)),B),
    inference(paramod,[status(thm)],[c_4,c_11103]) ).

cnf(c_66,plain,
    multiply(A,inverse(A)) = identity,
    inference(paramod,[status(thm)],[c_23,c_2]) ).

cnf(c_11104,plain,
    inverse(A) = multiply(inverse(A),inverse(identity)),
    inference(paramod,[status(thm)],[c_1,c_24]) ).

cnf(c_11105,plain,
    inverse(A) = multiply(inverse(A),identity),
    inference(paramod,[status(thm)],[c_22,c_11104]) ).

cnf(c_67,plain,
    multiply(inverse(A),identity) = inverse(A),
    inference(copy,[status(thm)],[c_11105]) ).

cnf(c_11106,plain,
    multiply(identity,A) = multiply(B,multiply(inverse(B),A)),
    inference(paramod,[status(thm)],[c_66,c_3]) ).

cnf(c_11107,plain,
    A = multiply(B,multiply(inverse(B),A)),
    inference(paramod,[status(thm)],[c_1,c_11106]) ).

cnf(c_68,plain,
    multiply(A,multiply(inverse(A),B)) = B,
    inference(copy,[status(thm)],[c_11107]) ).

cnf(c_11108,plain,
    greatest_lower_bound(multiply(A,B),identity) = multiply(A,greatest_lower_bound(B,inverse(A))),
    inference(paramod,[status(thm)],[c_66,c_17]) ).

cnf(c_72,plain,
    greatest_lower_bound(identity,multiply(A,B)) = multiply(A,greatest_lower_bound(B,inverse(A))),
    inference(paramod,[status(thm)],[c_4,c_11108]) ).

cnf(c_73,plain,
    least_upper_bound(identity,multiply(A,inverse(B))) = multiply(least_upper_bound(B,A),inverse(B)),
    inference(paramod,[status(thm)],[c_66,c_19]) ).

cnf(c_75,plain,
    greatest_lower_bound(identity,multiply(A,inverse(B))) = multiply(greatest_lower_bound(B,A),inverse(B)),
    inference(paramod,[status(thm)],[c_66,c_21]) ).

cnf(c_11109,plain,
    least_upper_bound(A,B) = least_upper_bound(A,least_upper_bound(greatest_lower_bound(C,A),B)),
    inference(paramod,[status(thm)],[c_38,c_9]) ).

cnf(c_78,plain,
    least_upper_bound(A,least_upper_bound(greatest_lower_bound(B,A),C)) = least_upper_bound(A,C),
    inference(copy,[status(thm)],[c_11109]) ).

cnf(c_11110,plain,
    greatest_lower_bound(A,B) = greatest_lower_bound(A,greatest_lower_bound(least_upper_bound(C,A),B)),
    inference(paramod,[status(thm)],[c_42,c_7]) ).

cnf(c_80,plain,
    greatest_lower_bound(A,greatest_lower_bound(least_upper_bound(B,A),C)) = greatest_lower_bound(A,C),
    inference(copy,[status(thm)],[c_11110]) ).

cnf(c_11111,plain,
    multiply(A,identity) = inverse(inverse(A)),
    inference(paramod,[status(thm)],[c_23,c_67]) ).

cnf(c_89,plain,
    multiply(A,identity) = A,
    inference(paramod,[status(thm)],[c_23,c_11111]) ).

cnf(c_90,plain,
    least_upper_bound(A,multiply(A,B)) = multiply(A,least_upper_bound(identity,B)),
    inference(paramod,[status(thm)],[c_89,c_15]) ).

cnf(c_11112,plain,
    least_upper_bound(multiply(A,B),A) = multiply(A,least_upper_bound(B,identity)),
    inference(paramod,[status(thm)],[c_89,c_15]) ).

cnf(c_91,plain,
    least_upper_bound(A,multiply(A,B)) = multiply(A,least_upper_bound(B,identity)),
    inference(paramod,[status(thm)],[c_5,c_11112]) ).

cnf(c_92,plain,
    greatest_lower_bound(A,multiply(A,B)) = multiply(A,greatest_lower_bound(identity,B)),
    inference(paramod,[status(thm)],[c_89,c_17]) ).

cnf(c_11113,plain,
    greatest_lower_bound(multiply(A,B),A) = multiply(A,greatest_lower_bound(B,identity)),
    inference(paramod,[status(thm)],[c_89,c_17]) ).

cnf(c_93,plain,
    greatest_lower_bound(A,multiply(A,B)) = multiply(A,greatest_lower_bound(B,identity)),
    inference(paramod,[status(thm)],[c_4,c_11113]) ).

cnf(c_11114,plain,
    least_upper_bound(inverse(A),identity) = multiply(least_upper_bound(identity,A),inverse(A)),
    inference(paramod,[status(thm)],[c_66,c_52]) ).

cnf(c_127,plain,
    least_upper_bound(identity,inverse(A)) = multiply(least_upper_bound(identity,A),inverse(A)),
    inference(paramod,[status(thm)],[c_5,c_11114]) ).

cnf(c_130,plain,
    least_upper_bound(A,multiply(least_upper_bound(identity,B),A)) = least_upper_bound(A,multiply(B,A)),
    inference(paramod,[status(thm)],[c_52,c_32]) ).

cnf(c_11115,plain,
    least_upper_bound(inverse(least_upper_bound(A,identity)),multiply(A,inverse(least_upper_bound(A,identity)))) = identity,
    inference(paramod,[status(thm)],[c_53,c_66]) ).

cnf(c_145,plain,
    multiply(least_upper_bound(identity,A),inverse(least_upper_bound(A,identity))) = identity,
    inference(paramod,[status(thm)],[c_52,c_11115]) ).

cnf(c_11116,plain,
    greatest_lower_bound(inverse(A),identity) = multiply(greatest_lower_bound(identity,A),inverse(A)),
    inference(paramod,[status(thm)],[c_66,c_59]) ).

cnf(c_162,plain,
    greatest_lower_bound(identity,inverse(A)) = multiply(greatest_lower_bound(identity,A),inverse(A)),
    inference(paramod,[status(thm)],[c_4,c_11116]) ).

cnf(c_164,plain,
    greatest_lower_bound(A,multiply(greatest_lower_bound(identity,B),A)) = greatest_lower_bound(A,multiply(B,A)),
    inference(paramod,[status(thm)],[c_59,c_35]) ).

cnf(c_11117,plain,
    least_upper_bound(inverse(A),identity) = multiply(inverse(A),least_upper_bound(identity,A)),
    inference(paramod,[status(thm)],[c_2,c_90]) ).

cnf(c_11118,plain,
    least_upper_bound(identity,inverse(A)) = multiply(inverse(A),least_upper_bound(identity,A)),
    inference(paramod,[status(thm)],[c_5,c_11117]) ).

cnf(c_179,plain,
    multiply(least_upper_bound(identity,A),inverse(A)) = multiply(inverse(A),least_upper_bound(identity,A)),
    inference(paramod,[status(thm)],[c_127,c_11118]) ).

cnf(c_194,plain,
    inverse(least_upper_bound(A,multiply(A,B))) = multiply(inverse(least_upper_bound(identity,B)),inverse(A)),
    inference(paramod,[status(thm)],[c_90,c_24]) ).

cnf(c_11119,plain,
    multiply(inverse(A),least_upper_bound(A,multiply(A,B))) = least_upper_bound(identity,B),
    inference(paramod,[status(thm)],[c_90,c_27]) ).

cnf(c_196,plain,
    least_upper_bound(identity,A) = multiply(inverse(B),least_upper_bound(B,multiply(B,A))),
    inference(copy,[status(thm)],[c_11119]) ).

cnf(c_11120,plain,
    multiply(A,least_upper_bound(identity,A)) = multiply(least_upper_bound(identity,A),A),
    inference(paramod,[status(thm)],[c_90,c_52]) ).

cnf(c_200,plain,
    multiply(least_upper_bound(identity,A),A) = multiply(A,least_upper_bound(identity,A)),
    inference(copy,[status(thm)],[c_11120]) ).

cnf(c_208,plain,
    least_upper_bound(identity,inverse(A)) = multiply(inverse(A),least_upper_bound(identity,A)),
    inference(paramod,[status(thm)],[c_179,c_127]) ).

cnf(c_11121,plain,
    least_upper_bound(inverse(least_upper_bound(A,identity)),multiply(inverse(least_upper_bound(A,identity)),A)) = identity,
    inference(paramod,[status(thm)],[c_91,c_2]) ).

cnf(c_211,plain,
    multiply(inverse(least_upper_bound(A,identity)),least_upper_bound(identity,A)) = identity,
    inference(paramod,[status(thm)],[c_90,c_11121]) ).

cnf(c_11122,plain,
    multiply(least_upper_bound(A,B),least_upper_bound(C,identity)) = least_upper_bound(A,least_upper_bound(B,multiply(least_upper_bound(A,B),C))),
    inference(paramod,[status(thm)],[c_91,c_9]) ).

cnf(c_214,plain,
    least_upper_bound(A,least_upper_bound(B,multiply(least_upper_bound(A,B),C))) = multiply(least_upper_bound(A,B),least_upper_bound(C,identity)),
    inference(copy,[status(thm)],[c_11122]) ).

cnf(c_217,plain,
    greatest_lower_bound(A,multiply(A,least_upper_bound(B,identity))) = A,
    inference(paramod,[status(thm)],[c_91,c_13]) ).

cnf(c_11123,plain,
    multiply(A,least_upper_bound(A,identity)) = multiply(least_upper_bound(A,identity),A),
    inference(paramod,[status(thm)],[c_91,c_53]) ).

cnf(c_227,plain,
    multiply(least_upper_bound(A,identity),A) = multiply(A,least_upper_bound(A,identity)),
    inference(copy,[status(thm)],[c_11123]) ).

cnf(c_11124,plain,
    greatest_lower_bound(inverse(A),identity) = multiply(inverse(A),greatest_lower_bound(identity,A)),
    inference(paramod,[status(thm)],[c_2,c_92]) ).

cnf(c_11125,plain,
    greatest_lower_bound(identity,inverse(A)) = multiply(inverse(A),greatest_lower_bound(identity,A)),
    inference(paramod,[status(thm)],[c_4,c_11124]) ).

cnf(c_229,plain,
    multiply(greatest_lower_bound(identity,A),inverse(A)) = multiply(inverse(A),greatest_lower_bound(identity,A)),
    inference(paramod,[status(thm)],[c_162,c_11125]) ).

cnf(c_11126,plain,
    multiply(inverse(A),greatest_lower_bound(A,multiply(A,B))) = greatest_lower_bound(identity,B),
    inference(paramod,[status(thm)],[c_92,c_27]) ).

cnf(c_243,plain,
    greatest_lower_bound(identity,A) = multiply(inverse(B),greatest_lower_bound(B,multiply(B,A))),
    inference(copy,[status(thm)],[c_11126]) ).

cnf(c_244,plain,
    greatest_lower_bound(inverse(A),B) = multiply(inverse(A),greatest_lower_bound(identity,multiply(A,B))),
    inference(paramod,[status(thm)],[c_27,c_92]) ).

cnf(c_11127,plain,
    multiply(A,greatest_lower_bound(identity,A)) = multiply(greatest_lower_bound(identity,A),A),
    inference(paramod,[status(thm)],[c_92,c_59]) ).

cnf(c_250,plain,
    multiply(greatest_lower_bound(identity,A),A) = multiply(A,greatest_lower_bound(identity,A)),
    inference(copy,[status(thm)],[c_11127]) ).

cnf(c_255,plain,
    greatest_lower_bound(identity,inverse(A)) = multiply(inverse(A),greatest_lower_bound(identity,A)),
    inference(paramod,[status(thm)],[c_229,c_162]) ).

cnf(c_11128,plain,
    multiply(A,greatest_lower_bound(A,identity)) = multiply(greatest_lower_bound(A,identity),A),
    inference(paramod,[status(thm)],[c_93,c_60]) ).

cnf(c_273,plain,
    multiply(greatest_lower_bound(A,identity),A) = multiply(A,greatest_lower_bound(A,identity)),
    inference(copy,[status(thm)],[c_11128]) ).

cnf(c_11129,plain,
    inverse(multiply(A,least_upper_bound(identity,A))) = multiply(inverse(A),inverse(least_upper_bound(identity,A))),
    inference(paramod,[status(thm)],[c_200,c_24]) ).

cnf(c_279,plain,
    multiply(inverse(least_upper_bound(identity,A)),inverse(A)) = multiply(inverse(A),inverse(least_upper_bound(identity,A))),
    inference(paramod,[status(thm)],[c_24,c_11129]) ).

cnf(c_11130,plain,
    greatest_lower_bound(least_upper_bound(identity,A),multiply(A,least_upper_bound(identity,A))) = multiply(least_upper_bound(identity,A),greatest_lower_bound(identity,A)),
    inference(paramod,[status(thm)],[c_200,c_92]) ).

cnf(c_11131,plain,
    multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A)) = multiply(least_upper_bound(identity,A),greatest_lower_bound(identity,A)),
    inference(paramod,[status(thm)],[c_59,c_11130]) ).

cnf(c_281,plain,
    multiply(least_upper_bound(identity,A),greatest_lower_bound(identity,A)) = multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A)),
    inference(copy,[status(thm)],[c_11131]) ).

cnf(c_11132,plain,
    least_upper_bound(identity,multiply(inverse(A),least_upper_bound(identity,A))) = least_upper_bound(identity,inverse(A)),
    inference(paramod,[status(thm)],[c_208,c_32]) ).

cnf(c_287,plain,
    least_upper_bound(identity,multiply(inverse(A),least_upper_bound(identity,A))) = multiply(inverse(A),least_upper_bound(identity,A)),
    inference(paramod,[status(thm)],[c_208,c_11132]) ).

cnf(c_11133,plain,
    multiply(multiply(A,least_upper_bound(A,identity)),B) = multiply(least_upper_bound(A,identity),multiply(A,B)),
    inference(paramod,[status(thm)],[c_227,c_3]) ).

cnf(c_11134,plain,
    multiply(A,multiply(least_upper_bound(A,identity),B)) = multiply(least_upper_bound(A,identity),multiply(A,B)),
    inference(paramod,[status(thm)],[c_3,c_11133]) ).

cnf(c_288,plain,
    multiply(least_upper_bound(A,identity),multiply(A,B)) = multiply(A,multiply(least_upper_bound(A,identity),B)),
    inference(copy,[status(thm)],[c_11134]) ).

cnf(c_290,plain,
    greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),multiply(least_upper_bound(A,identity),B)) = multiply(least_upper_bound(A,identity),greatest_lower_bound(A,B)),
    inference(paramod,[status(thm)],[c_227,c_17]) ).

cnf(c_11135,plain,
    greatest_lower_bound(least_upper_bound(A,identity),multiply(A,least_upper_bound(A,identity))) = multiply(least_upper_bound(A,identity),greatest_lower_bound(identity,A)),
    inference(paramod,[status(thm)],[c_227,c_92]) ).

cnf(c_11136,plain,
    multiply(greatest_lower_bound(identity,A),least_upper_bound(A,identity)) = multiply(least_upper_bound(A,identity),greatest_lower_bound(identity,A)),
    inference(paramod,[status(thm)],[c_59,c_11135]) ).

cnf(c_296,plain,
    multiply(least_upper_bound(A,identity),greatest_lower_bound(identity,A)) = multiply(greatest_lower_bound(identity,A),least_upper_bound(A,identity)),
    inference(copy,[status(thm)],[c_11136]) ).

cnf(c_11137,plain,
    greatest_lower_bound(least_upper_bound(A,identity),multiply(A,least_upper_bound(A,identity))) = multiply(least_upper_bound(A,identity),greatest_lower_bound(A,identity)),
    inference(paramod,[status(thm)],[c_227,c_93]) ).

cnf(c_11138,plain,
    multiply(greatest_lower_bound(identity,A),least_upper_bound(A,identity)) = multiply(least_upper_bound(A,identity),greatest_lower_bound(A,identity)),
    inference(paramod,[status(thm)],[c_59,c_11137]) ).

cnf(c_297,plain,
    multiply(least_upper_bound(A,identity),greatest_lower_bound(A,identity)) = multiply(greatest_lower_bound(identity,A),least_upper_bound(A,identity)),
    inference(copy,[status(thm)],[c_11138]) ).

cnf(c_11139,plain,
    inverse(multiply(A,greatest_lower_bound(identity,A))) = multiply(inverse(A),inverse(greatest_lower_bound(identity,A))),
    inference(paramod,[status(thm)],[c_250,c_24]) ).

cnf(c_303,plain,
    multiply(inverse(greatest_lower_bound(identity,A)),inverse(A)) = multiply(inverse(A),inverse(greatest_lower_bound(identity,A))),
    inference(paramod,[status(thm)],[c_24,c_11139]) ).

cnf(c_11140,plain,
    greatest_lower_bound(identity,multiply(inverse(A),greatest_lower_bound(identity,A))) = greatest_lower_bound(identity,inverse(A)),
    inference(paramod,[status(thm)],[c_255,c_35]) ).

cnf(c_309,plain,
    greatest_lower_bound(identity,multiply(inverse(A),greatest_lower_bound(identity,A))) = multiply(inverse(A),greatest_lower_bound(identity,A)),
    inference(paramod,[status(thm)],[c_255,c_11140]) ).

cnf(c_11141,plain,
    multiply(multiply(A,greatest_lower_bound(A,identity)),B) = multiply(greatest_lower_bound(A,identity),multiply(A,B)),
    inference(paramod,[status(thm)],[c_273,c_3]) ).

cnf(c_11142,plain,
    multiply(A,multiply(greatest_lower_bound(A,identity),B)) = multiply(greatest_lower_bound(A,identity),multiply(A,B)),
    inference(paramod,[status(thm)],[c_3,c_11141]) ).

cnf(c_310,plain,
    multiply(greatest_lower_bound(A,identity),multiply(A,B)) = multiply(A,multiply(greatest_lower_bound(A,identity),B)),
    inference(copy,[status(thm)],[c_11142]) ).

cnf(c_319,plain,
    multiply(least_upper_bound(A,identity),inverse(A)) = multiply(inverse(A),least_upper_bound(identity,A)),
    inference(paramod,[status(thm)],[c_5,c_179]) ).

cnf(c_11143,plain,
    multiply(multiply(inverse(A),greatest_lower_bound(identity,A)),B) = multiply(greatest_lower_bound(identity,A),multiply(inverse(A),B)),
    inference(paramod,[status(thm)],[c_229,c_3]) ).

cnf(c_11144,plain,
    multiply(inverse(A),multiply(greatest_lower_bound(identity,A),B)) = multiply(greatest_lower_bound(identity,A),multiply(inverse(A),B)),
    inference(paramod,[status(thm)],[c_3,c_11143]) ).

cnf(c_331,plain,
    multiply(greatest_lower_bound(identity,A),multiply(inverse(A),B)) = multiply(inverse(A),multiply(greatest_lower_bound(identity,A),B)),
    inference(copy,[status(thm)],[c_11144]) ).

cnf(c_332,plain,
    multiply(greatest_lower_bound(A,identity),inverse(A)) = multiply(inverse(A),greatest_lower_bound(identity,A)),
    inference(paramod,[status(thm)],[c_4,c_229]) ).

cnf(c_11145,plain,
    inverse(multiply(inverse(A),greatest_lower_bound(identity,A))) = multiply(inverse(inverse(A)),inverse(greatest_lower_bound(identity,A))),
    inference(paramod,[status(thm)],[c_229,c_24]) ).

cnf(c_11146,plain,
    multiply(inverse(greatest_lower_bound(identity,A)),inverse(inverse(A))) = multiply(inverse(inverse(A)),inverse(greatest_lower_bound(identity,A))),
    inference(paramod,[status(thm)],[c_24,c_11145]) ).

cnf(c_11147,plain,
    multiply(inverse(greatest_lower_bound(identity,A)),A) = multiply(inverse(inverse(A)),inverse(greatest_lower_bound(identity,A))),
    inference(paramod,[status(thm)],[c_23,c_11146]) ).

cnf(c_341,plain,
    multiply(inverse(greatest_lower_bound(identity,A)),A) = multiply(A,inverse(greatest_lower_bound(identity,A))),
    inference(paramod,[status(thm)],[c_23,c_11147]) ).

cnf(c_346,plain,
    multiply(least_upper_bound(A,identity),inverse(A)) = multiply(inverse(A),least_upper_bound(A,identity)),
    inference(paramod,[status(thm)],[c_5,c_319]) ).

cnf(c_11148,plain,
    greatest_lower_bound(least_upper_bound(identity,A),multiply(least_upper_bound(A,identity),inverse(A))) = multiply(greatest_lower_bound(identity,inverse(A)),least_upper_bound(identity,A)),
    inference(paramod,[status(thm)],[c_319,c_59]) ).

cnf(c_11149,plain,
    greatest_lower_bound(least_upper_bound(identity,A),multiply(inverse(A),least_upper_bound(A,identity))) = multiply(greatest_lower_bound(identity,inverse(A)),least_upper_bound(identity,A)),
    inference(paramod,[status(thm)],[c_346,c_11148]) ).

cnf(c_11150,plain,
    greatest_lower_bound(least_upper_bound(identity,A),multiply(inverse(A),least_upper_bound(A,identity))) = multiply(multiply(inverse(A),greatest_lower_bound(identity,A)),least_upper_bound(identity,A)),
    inference(paramod,[status(thm)],[c_255,c_11149]) ).

cnf(c_358,plain,
    greatest_lower_bound(least_upper_bound(identity,A),multiply(inverse(A),least_upper_bound(A,identity))) = multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A))),
    inference(paramod,[status(thm)],[c_3,c_11150]) ).

cnf(c_11151,plain,
    least_upper_bound(least_upper_bound(A,identity),multiply(inverse(A),least_upper_bound(identity,A))) = multiply(least_upper_bound(A,identity),least_upper_bound(identity,inverse(A))),
    inference(paramod,[status(thm)],[c_319,c_90]) ).

cnf(c_11152,plain,
    least_upper_bound(A,least_upper_bound(identity,multiply(inverse(A),least_upper_bound(identity,A)))) = multiply(least_upper_bound(A,identity),least_upper_bound(identity,inverse(A))),
    inference(paramod,[status(thm)],[c_9,c_11151]) ).

cnf(c_11153,plain,
    least_upper_bound(A,multiply(inverse(A),least_upper_bound(identity,A))) = multiply(least_upper_bound(A,identity),least_upper_bound(identity,inverse(A))),
    inference(paramod,[status(thm)],[c_287,c_11152]) ).

cnf(c_359,plain,
    least_upper_bound(A,multiply(inverse(A),least_upper_bound(identity,A))) = multiply(least_upper_bound(A,identity),multiply(inverse(A),least_upper_bound(identity,A))),
    inference(paramod,[status(thm)],[c_208,c_11153]) ).

cnf(c_363,plain,
    multiply(greatest_lower_bound(A,identity),inverse(A)) = multiply(inverse(A),greatest_lower_bound(A,identity)),
    inference(paramod,[status(thm)],[c_4,c_332]) ).

cnf(c_11154,plain,
    least_upper_bound(greatest_lower_bound(identity,A),multiply(greatest_lower_bound(A,identity),inverse(A))) = multiply(least_upper_bound(identity,inverse(A)),greatest_lower_bound(identity,A)),
    inference(paramod,[status(thm)],[c_332,c_52]) ).

cnf(c_11155,plain,
    least_upper_bound(greatest_lower_bound(identity,A),multiply(inverse(A),greatest_lower_bound(A,identity))) = multiply(least_upper_bound(identity,inverse(A)),greatest_lower_bound(identity,A)),
    inference(paramod,[status(thm)],[c_363,c_11154]) ).

cnf(c_11156,plain,
    least_upper_bound(greatest_lower_bound(identity,A),multiply(inverse(A),greatest_lower_bound(A,identity))) = multiply(multiply(inverse(A),least_upper_bound(identity,A)),greatest_lower_bound(identity,A)),
    inference(paramod,[status(thm)],[c_208,c_11155]) ).

cnf(c_11157,plain,
    least_upper_bound(greatest_lower_bound(identity,A),multiply(inverse(A),greatest_lower_bound(A,identity))) = multiply(inverse(A),multiply(least_upper_bound(identity,A),greatest_lower_bound(identity,A))),
    inference(paramod,[status(thm)],[c_3,c_11156]) ).

cnf(c_374,plain,
    least_upper_bound(greatest_lower_bound(identity,A),multiply(inverse(A),greatest_lower_bound(A,identity))) = multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A))),
    inference(paramod,[status(thm)],[c_281,c_11157]) ).

cnf(c_11158,plain,
    greatest_lower_bound(greatest_lower_bound(A,identity),multiply(inverse(A),greatest_lower_bound(identity,A))) = multiply(greatest_lower_bound(A,identity),greatest_lower_bound(identity,inverse(A))),
    inference(paramod,[status(thm)],[c_332,c_92]) ).

cnf(c_11159,plain,
    greatest_lower_bound(A,greatest_lower_bound(identity,multiply(inverse(A),greatest_lower_bound(identity,A)))) = multiply(greatest_lower_bound(A,identity),greatest_lower_bound(identity,inverse(A))),
    inference(paramod,[status(thm)],[c_7,c_11158]) ).

cnf(c_11160,plain,
    greatest_lower_bound(A,multiply(inverse(A),greatest_lower_bound(identity,A))) = multiply(greatest_lower_bound(A,identity),greatest_lower_bound(identity,inverse(A))),
    inference(paramod,[status(thm)],[c_309,c_11159]) ).

cnf(c_377,plain,
    greatest_lower_bound(A,multiply(inverse(A),greatest_lower_bound(identity,A))) = multiply(greatest_lower_bound(A,identity),multiply(inverse(A),greatest_lower_bound(identity,A))),
    inference(paramod,[status(thm)],[c_255,c_11160]) ).

cnf(c_11161,plain,
    multiply(multiply(inverse(A),least_upper_bound(A,identity)),B) = multiply(least_upper_bound(A,identity),multiply(inverse(A),B)),
    inference(paramod,[status(thm)],[c_346,c_3]) ).

cnf(c_11162,plain,
    multiply(inverse(A),multiply(least_upper_bound(A,identity),B)) = multiply(least_upper_bound(A,identity),multiply(inverse(A),B)),
    inference(paramod,[status(thm)],[c_3,c_11161]) ).

cnf(c_378,plain,
    multiply(least_upper_bound(A,identity),multiply(inverse(A),B)) = multiply(inverse(A),multiply(least_upper_bound(A,identity),B)),
    inference(copy,[status(thm)],[c_11162]) ).

cnf(c_388,plain,
    least_upper_bound(A,multiply(inverse(A),least_upper_bound(identity,A))) = multiply(inverse(A),multiply(least_upper_bound(A,identity),least_upper_bound(identity,A))),
    inference(paramod,[status(thm)],[c_378,c_359]) ).

cnf(c_11163,plain,
    multiply(multiply(inverse(A),greatest_lower_bound(A,identity)),B) = multiply(greatest_lower_bound(A,identity),multiply(inverse(A),B)),
    inference(paramod,[status(thm)],[c_363,c_3]) ).

cnf(c_11164,plain,
    multiply(inverse(A),multiply(greatest_lower_bound(A,identity),B)) = multiply(greatest_lower_bound(A,identity),multiply(inverse(A),B)),
    inference(paramod,[status(thm)],[c_3,c_11163]) ).

cnf(c_391,plain,
    multiply(greatest_lower_bound(A,identity),multiply(inverse(A),B)) = multiply(inverse(A),multiply(greatest_lower_bound(A,identity),B)),
    inference(copy,[status(thm)],[c_11164]) ).

cnf(c_400,plain,
    greatest_lower_bound(A,multiply(inverse(A),greatest_lower_bound(identity,A))) = multiply(inverse(A),multiply(greatest_lower_bound(A,identity),greatest_lower_bound(identity,A))),
    inference(paramod,[status(thm)],[c_391,c_377]) ).

cnf(c_482,plain,
    least_upper_bound(multiply(A,B),C) = multiply(A,least_upper_bound(B,multiply(inverse(A),C))),
    inference(paramod,[status(thm)],[c_68,c_15]) ).

cnf(c_483,plain,
    greatest_lower_bound(multiply(A,B),C) = multiply(A,greatest_lower_bound(B,multiply(inverse(A),C))),
    inference(paramod,[status(thm)],[c_68,c_17]) ).

cnf(c_550,plain,
    multiply(A,greatest_lower_bound(least_upper_bound(A,identity),multiply(inverse(A),multiply(least_upper_bound(A,identity),B)))) = multiply(least_upper_bound(A,identity),greatest_lower_bound(A,B)),
    inference(paramod,[status(thm)],[c_483,c_290]) ).

cnf(c_11165,plain,
    inverse(identity) = multiply(inverse(inverse(least_upper_bound(A,identity))),inverse(least_upper_bound(identity,A))),
    inference(paramod,[status(thm)],[c_145,c_24]) ).

cnf(c_11166,plain,
    identity = multiply(inverse(inverse(least_upper_bound(A,identity))),inverse(least_upper_bound(identity,A))),
    inference(paramod,[status(thm)],[c_22,c_11165]) ).

cnf(c_11167,plain,
    identity = multiply(least_upper_bound(A,identity),inverse(least_upper_bound(identity,A))),
    inference(paramod,[status(thm)],[c_23,c_11166]) ).

cnf(c_571,plain,
    multiply(least_upper_bound(A,identity),inverse(least_upper_bound(identity,A))) = identity,
    inference(copy,[status(thm)],[c_11167]) ).

cnf(c_11168,plain,
    multiply(identity,A) = multiply(inverse(least_upper_bound(B,identity)),multiply(least_upper_bound(identity,B),A)),
    inference(paramod,[status(thm)],[c_211,c_3]) ).

cnf(c_11169,plain,
    A = multiply(inverse(least_upper_bound(B,identity)),multiply(least_upper_bound(identity,B),A)),
    inference(paramod,[status(thm)],[c_1,c_11168]) ).

cnf(c_576,plain,
    multiply(inverse(least_upper_bound(A,identity)),multiply(least_upper_bound(identity,A),B)) = B,
    inference(copy,[status(thm)],[c_11169]) ).

cnf(c_11170,plain,
    inverse(identity) = multiply(inverse(least_upper_bound(identity,A)),inverse(inverse(least_upper_bound(A,identity)))),
    inference(paramod,[status(thm)],[c_211,c_24]) ).

cnf(c_11171,plain,
    identity = multiply(inverse(least_upper_bound(identity,A)),inverse(inverse(least_upper_bound(A,identity)))),
    inference(paramod,[status(thm)],[c_22,c_11170]) ).

cnf(c_11172,plain,
    identity = multiply(inverse(least_upper_bound(identity,A)),least_upper_bound(A,identity)),
    inference(paramod,[status(thm)],[c_23,c_11171]) ).

cnf(c_578,plain,
    multiply(inverse(least_upper_bound(identity,A)),least_upper_bound(A,identity)) = identity,
    inference(copy,[status(thm)],[c_11172]) ).

cnf(c_11173,plain,
    multiply(multiply(greatest_lower_bound(identity,A),least_upper_bound(A,identity)),B) = multiply(least_upper_bound(A,identity),multiply(greatest_lower_bound(A,identity),B)),
    inference(paramod,[status(thm)],[c_297,c_3]) ).

cnf(c_11174,plain,
    multiply(greatest_lower_bound(identity,A),multiply(least_upper_bound(A,identity),B)) = multiply(least_upper_bound(A,identity),multiply(greatest_lower_bound(A,identity),B)),
    inference(paramod,[status(thm)],[c_3,c_11173]) ).

cnf(c_602,plain,
    multiply(least_upper_bound(A,identity),multiply(greatest_lower_bound(A,identity),B)) = multiply(greatest_lower_bound(identity,A),multiply(least_upper_bound(A,identity),B)),
    inference(copy,[status(thm)],[c_11174]) ).

cnf(c_11175,plain,
    multiply(identity,A) = multiply(inverse(least_upper_bound(identity,B)),multiply(least_upper_bound(B,identity),A)),
    inference(paramod,[status(thm)],[c_578,c_3]) ).

cnf(c_11176,plain,
    A = multiply(inverse(least_upper_bound(identity,B)),multiply(least_upper_bound(B,identity),A)),
    inference(paramod,[status(thm)],[c_1,c_11175]) ).

cnf(c_618,plain,
    multiply(inverse(least_upper_bound(identity,A)),multiply(least_upper_bound(A,identity),B)) = B,
    inference(copy,[status(thm)],[c_11176]) ).

cnf(c_11177,plain,
    least_upper_bound(identity,multiply(A,least_upper_bound(A,identity))) = multiply(least_upper_bound(least_upper_bound(A,identity),inverse(A)),A),
    inference(paramod,[status(thm)],[c_227,c_55]) ).

cnf(c_11178,plain,
    least_upper_bound(identity,multiply(A,least_upper_bound(A,identity))) = multiply(least_upper_bound(inverse(A),least_upper_bound(A,identity)),A),
    inference(paramod,[status(thm)],[c_5,c_11177]) ).

cnf(c_11179,plain,
    least_upper_bound(identity,multiply(A,least_upper_bound(A,identity))) = multiply(least_upper_bound(A,least_upper_bound(inverse(A),identity)),A),
    inference(paramod,[status(thm)],[c_31,c_11178]) ).

cnf(c_11180,plain,
    least_upper_bound(identity,multiply(A,least_upper_bound(A,identity))) = multiply(least_upper_bound(A,least_upper_bound(identity,inverse(A))),A),
    inference(paramod,[status(thm)],[c_5,c_11179]) ).

cnf(c_11181,plain,
    least_upper_bound(identity,multiply(A,least_upper_bound(A,identity))) = multiply(least_upper_bound(A,multiply(inverse(A),least_upper_bound(identity,A))),A),
    inference(paramod,[status(thm)],[c_208,c_11180]) ).

cnf(c_11182,plain,
    least_upper_bound(identity,multiply(A,least_upper_bound(A,identity))) = multiply(multiply(inverse(A),multiply(least_upper_bound(A,identity),least_upper_bound(identity,A))),A),
    inference(paramod,[status(thm)],[c_388,c_11181]) ).

cnf(c_11183,plain,
    least_upper_bound(identity,multiply(A,least_upper_bound(A,identity))) = multiply(inverse(A),multiply(multiply(least_upper_bound(A,identity),least_upper_bound(identity,A)),A)),
    inference(paramod,[status(thm)],[c_3,c_11182]) ).

cnf(c_11184,plain,
    least_upper_bound(identity,multiply(A,least_upper_bound(A,identity))) = multiply(inverse(A),multiply(least_upper_bound(A,identity),multiply(least_upper_bound(identity,A),A))),
    inference(paramod,[status(thm)],[c_3,c_11183]) ).

cnf(c_11185,plain,
    least_upper_bound(identity,multiply(A,least_upper_bound(A,identity))) = multiply(inverse(A),multiply(least_upper_bound(A,identity),multiply(A,least_upper_bound(identity,A)))),
    inference(paramod,[status(thm)],[c_200,c_11184]) ).

cnf(c_11186,plain,
    least_upper_bound(identity,multiply(A,least_upper_bound(A,identity))) = multiply(inverse(A),multiply(A,multiply(least_upper_bound(A,identity),least_upper_bound(identity,A)))),
    inference(paramod,[status(thm)],[c_288,c_11185]) ).

cnf(c_720,plain,
    least_upper_bound(identity,multiply(A,least_upper_bound(A,identity))) = multiply(least_upper_bound(A,identity),least_upper_bound(identity,A)),
    inference(paramod,[status(thm)],[c_27,c_11186]) ).

cnf(c_11187,plain,
    greatest_lower_bound(identity,multiply(A,greatest_lower_bound(A,identity))) = multiply(greatest_lower_bound(greatest_lower_bound(A,identity),inverse(A)),A),
    inference(paramod,[status(thm)],[c_273,c_62]) ).

cnf(c_11188,plain,
    greatest_lower_bound(identity,multiply(A,greatest_lower_bound(A,identity))) = multiply(greatest_lower_bound(inverse(A),greatest_lower_bound(A,identity)),A),
    inference(paramod,[status(thm)],[c_4,c_11187]) ).

cnf(c_11189,plain,
    greatest_lower_bound(identity,multiply(A,greatest_lower_bound(A,identity))) = multiply(greatest_lower_bound(A,greatest_lower_bound(inverse(A),identity)),A),
    inference(paramod,[status(thm)],[c_29,c_11188]) ).

cnf(c_11190,plain,
    greatest_lower_bound(identity,multiply(A,greatest_lower_bound(A,identity))) = multiply(greatest_lower_bound(A,greatest_lower_bound(identity,inverse(A))),A),
    inference(paramod,[status(thm)],[c_4,c_11189]) ).

cnf(c_11191,plain,
    greatest_lower_bound(identity,multiply(A,greatest_lower_bound(A,identity))) = multiply(greatest_lower_bound(A,multiply(inverse(A),greatest_lower_bound(identity,A))),A),
    inference(paramod,[status(thm)],[c_255,c_11190]) ).

cnf(c_11192,plain,
    greatest_lower_bound(identity,multiply(A,greatest_lower_bound(A,identity))) = multiply(multiply(inverse(A),multiply(greatest_lower_bound(A,identity),greatest_lower_bound(identity,A))),A),
    inference(paramod,[status(thm)],[c_400,c_11191]) ).

cnf(c_11193,plain,
    greatest_lower_bound(identity,multiply(A,greatest_lower_bound(A,identity))) = multiply(inverse(A),multiply(multiply(greatest_lower_bound(A,identity),greatest_lower_bound(identity,A)),A)),
    inference(paramod,[status(thm)],[c_3,c_11192]) ).

cnf(c_11194,plain,
    greatest_lower_bound(identity,multiply(A,greatest_lower_bound(A,identity))) = multiply(inverse(A),multiply(greatest_lower_bound(A,identity),multiply(greatest_lower_bound(identity,A),A))),
    inference(paramod,[status(thm)],[c_3,c_11193]) ).

cnf(c_11195,plain,
    greatest_lower_bound(identity,multiply(A,greatest_lower_bound(A,identity))) = multiply(inverse(A),multiply(greatest_lower_bound(A,identity),multiply(A,greatest_lower_bound(identity,A)))),
    inference(paramod,[status(thm)],[c_250,c_11194]) ).

cnf(c_11196,plain,
    greatest_lower_bound(identity,multiply(A,greatest_lower_bound(A,identity))) = multiply(inverse(A),multiply(A,multiply(greatest_lower_bound(A,identity),greatest_lower_bound(identity,A)))),
    inference(paramod,[status(thm)],[c_310,c_11195]) ).

cnf(c_778,plain,
    greatest_lower_bound(identity,multiply(A,greatest_lower_bound(A,identity))) = multiply(greatest_lower_bound(A,identity),greatest_lower_bound(identity,A)),
    inference(paramod,[status(thm)],[c_27,c_11196]) ).

cnf(c_11197,plain,
    multiply(inverse(A),greatest_lower_bound(identity,multiply(A,B))) = greatest_lower_bound(B,inverse(A)),
    inference(paramod,[status(thm)],[c_72,c_27]) ).

cnf(c_861,plain,
    greatest_lower_bound(A,inverse(B)) = multiply(inverse(B),greatest_lower_bound(identity,multiply(B,A))),
    inference(copy,[status(thm)],[c_11197]) ).

cnf(c_880,plain,
    greatest_lower_bound(identity,multiply(A,least_upper_bound(A,identity))) = multiply(least_upper_bound(A,identity),greatest_lower_bound(A,inverse(least_upper_bound(A,identity)))),
    inference(paramod,[status(thm)],[c_227,c_72]) ).

cnf(c_967,plain,
    least_upper_bound(identity,A) = multiply(inverse(least_upper_bound(B,C)),least_upper_bound(B,least_upper_bound(C,multiply(least_upper_bound(B,C),A)))),
    inference(paramod,[status(thm)],[c_9,c_196]) ).

cnf(c_11198,plain,
    greatest_lower_bound(least_upper_bound(greatest_lower_bound(A,B),C),least_upper_bound(A,C)) = least_upper_bound(greatest_lower_bound(A,B),C),
    inference(paramod,[status(thm)],[c_40,c_42]) ).

cnf(c_1108,plain,
    greatest_lower_bound(least_upper_bound(A,B),least_upper_bound(greatest_lower_bound(A,C),B)) = least_upper_bound(greatest_lower_bound(A,C),B),
    inference(paramod,[status(thm)],[c_4,c_11198]) ).

cnf(c_11199,plain,
    least_upper_bound(identity,multiply(inverse(A),greatest_lower_bound(A,B))) = multiply(inverse(A),A),
    inference(paramod,[status(thm)],[c_12,c_46]) ).

cnf(c_1691,plain,
    least_upper_bound(identity,multiply(inverse(A),greatest_lower_bound(A,B))) = identity,
    inference(paramod,[status(thm)],[c_2,c_11199]) ).

cnf(c_1692,plain,
    greatest_lower_bound(identity,multiply(inverse(A),least_upper_bound(A,B))) = identity,
    inference(paramod,[status(thm)],[c_46,c_13]) ).

cnf(c_11200,plain,
    multiply(inverse(A),least_upper_bound(A,B)) = multiply(inverse(C),least_upper_bound(C,multiply(C,multiply(inverse(A),B)))),
    inference(paramod,[status(thm)],[c_46,c_196]) ).

cnf(c_1733,plain,
    multiply(inverse(A),least_upper_bound(A,multiply(A,multiply(inverse(B),C)))) = multiply(inverse(B),least_upper_bound(B,C)),
    inference(copy,[status(thm)],[c_11200]) ).

cnf(c_11201,plain,
    multiply(multiply(inverse(A),least_upper_bound(B,A)),greatest_lower_bound(identity,multiply(inverse(A),B))) = multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),least_upper_bound(identity,multiply(inverse(A),B))),
    inference(paramod,[status(thm)],[c_47,c_281]) ).

cnf(c_11202,plain,
    multiply(inverse(A),multiply(least_upper_bound(B,A),greatest_lower_bound(identity,multiply(inverse(A),B)))) = multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),least_upper_bound(identity,multiply(inverse(A),B))),
    inference(paramod,[status(thm)],[c_3,c_11201]) ).

cnf(c_1856,plain,
    multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),least_upper_bound(identity,multiply(inverse(A),B))) = multiply(inverse(A),multiply(least_upper_bound(B,A),greatest_lower_bound(identity,multiply(inverse(A),B)))),
    inference(copy,[status(thm)],[c_11202]) ).

cnf(c_11203,plain,
    multiply(least_upper_bound(multiply(inverse(A),B),identity),inverse(multiply(inverse(A),least_upper_bound(B,A)))) = identity,
    inference(paramod,[status(thm)],[c_47,c_571]) ).

cnf(c_11204,plain,
    multiply(least_upper_bound(identity,multiply(inverse(A),B)),inverse(multiply(inverse(A),least_upper_bound(B,A)))) = identity,
    inference(paramod,[status(thm)],[c_5,c_11203]) ).

cnf(c_11205,plain,
    multiply(least_upper_bound(identity,multiply(inverse(A),B)),multiply(inverse(least_upper_bound(B,A)),inverse(inverse(A)))) = identity,
    inference(paramod,[status(thm)],[c_24,c_11204]) ).

cnf(c_1857,plain,
    multiply(least_upper_bound(identity,multiply(inverse(A),B)),multiply(inverse(least_upper_bound(B,A)),A)) = identity,
    inference(paramod,[status(thm)],[c_23,c_11205]) ).

cnf(c_1900,plain,
    greatest_lower_bound(identity,multiply(inverse(A),multiply(B,A))) = multiply(inverse(A),multiply(greatest_lower_bound(identity,B),A)),
    inference(paramod,[status(thm)],[c_59,c_49]) ).

cnf(c_11206,plain,
    greatest_lower_bound(identity,multiply(multiply(A,B),inverse(A))) = multiply(multiply(A,greatest_lower_bound(identity,B)),inverse(A)),
    inference(paramod,[status(thm)],[c_92,c_75]) ).

cnf(c_11207,plain,
    greatest_lower_bound(identity,multiply(A,multiply(B,inverse(A)))) = multiply(multiply(A,greatest_lower_bound(identity,B)),inverse(A)),
    inference(paramod,[status(thm)],[c_3,c_11206]) ).

cnf(c_2258,plain,
    greatest_lower_bound(identity,multiply(A,multiply(B,inverse(A)))) = multiply(A,multiply(greatest_lower_bound(identity,B),inverse(A))),
    inference(paramod,[status(thm)],[c_3,c_11207]) ).

cnf(c_11208,plain,
    greatest_lower_bound(least_upper_bound(greatest_lower_bound(A,B),C),least_upper_bound(B,C)) = least_upper_bound(greatest_lower_bound(A,B),C),
    inference(paramod,[status(thm)],[c_78,c_42]) ).

cnf(c_2364,plain,
    greatest_lower_bound(least_upper_bound(A,B),least_upper_bound(greatest_lower_bound(C,A),B)) = least_upper_bound(greatest_lower_bound(C,A),B),
    inference(paramod,[status(thm)],[c_4,c_11208]) ).

cnf(c_11209,plain,
    least_upper_bound(identity,multiply(multiply(least_upper_bound(identity,A),B),inverse(B))) = multiply(least_upper_bound(B,multiply(A,B)),inverse(B)),
    inference(paramod,[status(thm)],[c_130,c_73]) ).

cnf(c_11210,plain,
    least_upper_bound(identity,multiply(least_upper_bound(identity,A),multiply(B,inverse(B)))) = multiply(least_upper_bound(B,multiply(A,B)),inverse(B)),
    inference(paramod,[status(thm)],[c_3,c_11209]) ).

cnf(c_11211,plain,
    least_upper_bound(identity,multiply(least_upper_bound(identity,A),identity)) = multiply(least_upper_bound(B,multiply(A,B)),inverse(B)),
    inference(paramod,[status(thm)],[c_66,c_11210]) ).

cnf(c_11212,plain,
    least_upper_bound(identity,least_upper_bound(identity,A)) = multiply(least_upper_bound(B,multiply(A,B)),inverse(B)),
    inference(paramod,[status(thm)],[c_89,c_11211]) ).

cnf(c_2466,plain,
    least_upper_bound(identity,A) = multiply(least_upper_bound(B,multiply(A,B)),inverse(B)),
    inference(paramod,[status(thm)],[c_32,c_11212]) ).

cnf(c_11213,plain,
    greatest_lower_bound(multiply(inverse(A),B),multiply(greatest_lower_bound(identity,A),multiply(inverse(A),B))) = greatest_lower_bound(multiply(inverse(A),B),B),
    inference(paramod,[status(thm)],[c_68,c_164]) ).

cnf(c_11214,plain,
    greatest_lower_bound(multiply(inverse(A),B),multiply(inverse(A),multiply(greatest_lower_bound(identity,A),B))) = greatest_lower_bound(multiply(inverse(A),B),B),
    inference(paramod,[status(thm)],[c_331,c_11213]) ).

cnf(c_11215,plain,
    multiply(inverse(A),greatest_lower_bound(B,multiply(inverse(inverse(A)),multiply(inverse(A),multiply(greatest_lower_bound(identity,A),B))))) = greatest_lower_bound(multiply(inverse(A),B),B),
    inference(paramod,[status(thm)],[c_483,c_11214]) ).

cnf(c_11216,plain,
    multiply(inverse(A),greatest_lower_bound(B,multiply(A,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),B))))) = greatest_lower_bound(multiply(inverse(A),B),B),
    inference(paramod,[status(thm)],[c_23,c_11215]) ).

cnf(c_11217,plain,
    multiply(inverse(A),greatest_lower_bound(B,multiply(greatest_lower_bound(identity,A),B))) = greatest_lower_bound(multiply(inverse(A),B),B),
    inference(paramod,[status(thm)],[c_68,c_11216]) ).

cnf(c_11218,plain,
    multiply(inverse(A),greatest_lower_bound(B,multiply(A,B))) = greatest_lower_bound(multiply(inverse(A),B),B),
    inference(paramod,[status(thm)],[c_164,c_11217]) ).

cnf(c_11219,plain,
    multiply(inverse(A),greatest_lower_bound(B,multiply(A,B))) = greatest_lower_bound(B,multiply(inverse(A),B)),
    inference(paramod,[status(thm)],[c_4,c_11218]) ).

cnf(c_2574,plain,
    greatest_lower_bound(A,multiply(inverse(B),A)) = multiply(inverse(B),greatest_lower_bound(A,multiply(B,A))),
    inference(copy,[status(thm)],[c_11219]) ).

cnf(c_3834,plain,
    inverse(least_upper_bound(A,B)) = multiply(inverse(least_upper_bound(identity,multiply(inverse(A),B))),inverse(A)),
    inference(paramod,[status(thm)],[c_68,c_194]) ).

cnf(c_11220,plain,
    multiply(inverse(least_upper_bound(multiply(inverse(A),B),identity)),multiply(multiply(inverse(A),least_upper_bound(A,B)),C)) = C,
    inference(paramod,[status(thm)],[c_46,c_576]) ).

cnf(c_11221,plain,
    multiply(inverse(least_upper_bound(identity,multiply(inverse(A),B))),multiply(multiply(inverse(A),least_upper_bound(A,B)),C)) = C,
    inference(paramod,[status(thm)],[c_5,c_11220]) ).

cnf(c_4143,plain,
    multiply(inverse(least_upper_bound(identity,multiply(inverse(A),B))),multiply(inverse(A),multiply(least_upper_bound(A,B),C))) = C,
    inference(paramod,[status(thm)],[c_3,c_11221]) ).

cnf(c_4177,plain,
    multiply(inverse(least_upper_bound(identity,A)),multiply(greatest_lower_bound(identity,A),least_upper_bound(A,identity))) = greatest_lower_bound(identity,A),
    inference(paramod,[status(thm)],[c_296,c_618]) ).

cnf(c_11222,plain,
    multiply(inverse(multiply(least_upper_bound(A,multiply(B,A)),inverse(A))),multiply(least_upper_bound(B,identity),C)) = C,
    inference(paramod,[status(thm)],[c_2466,c_618]) ).

cnf(c_11223,plain,
    multiply(multiply(inverse(inverse(A)),inverse(least_upper_bound(A,multiply(B,A)))),multiply(least_upper_bound(B,identity),C)) = C,
    inference(paramod,[status(thm)],[c_24,c_11222]) ).

cnf(c_11224,plain,
    multiply(multiply(A,inverse(least_upper_bound(A,multiply(B,A)))),multiply(least_upper_bound(B,identity),C)) = C,
    inference(paramod,[status(thm)],[c_23,c_11223]) ).

cnf(c_4191,plain,
    multiply(A,multiply(inverse(least_upper_bound(A,multiply(B,A))),multiply(least_upper_bound(B,identity),C))) = C,
    inference(paramod,[status(thm)],[c_3,c_11224]) ).

cnf(c_4276,plain,
    least_upper_bound(greatest_lower_bound(A,B),greatest_lower_bound(B,A)) = greatest_lower_bound(A,B),
    inference(paramod,[status(thm)],[c_37,c_39]) ).

cnf(c_11225,plain,
    least_upper_bound(identity,multiply(inverse(greatest_lower_bound(A,B)),greatest_lower_bound(B,A))) = multiply(inverse(greatest_lower_bound(A,B)),greatest_lower_bound(A,B)),
    inference(paramod,[status(thm)],[c_4276,c_46]) ).

cnf(c_4345,plain,
    least_upper_bound(identity,multiply(inverse(greatest_lower_bound(A,B)),greatest_lower_bound(B,A))) = identity,
    inference(paramod,[status(thm)],[c_2,c_11225]) ).

cnf(c_11226,plain,
    least_upper_bound(identity,multiply(inverse(greatest_lower_bound(A,B)),greatest_lower_bound(B,A))) = multiply(inverse(greatest_lower_bound(A,B)),greatest_lower_bound(B,A)),
    inference(paramod,[status(thm)],[c_4276,c_47]) ).

cnf(c_11227,plain,
    identity = multiply(inverse(greatest_lower_bound(A,B)),greatest_lower_bound(B,A)),
    inference(paramod,[status(thm)],[c_4345,c_11226]) ).

cnf(c_4347,plain,
    multiply(inverse(greatest_lower_bound(A,B)),greatest_lower_bound(B,A)) = identity,
    inference(copy,[status(thm)],[c_11227]) ).

cnf(c_4403,plain,
    greatest_lower_bound(least_upper_bound(A,B),least_upper_bound(B,A)) = least_upper_bound(A,B),
    inference(paramod,[status(thm)],[c_34,c_45]) ).

cnf(c_11228,plain,
    greatest_lower_bound(identity,multiply(inverse(least_upper_bound(A,B)),least_upper_bound(B,A))) = multiply(inverse(least_upper_bound(A,B)),least_upper_bound(A,B)),
    inference(paramod,[status(thm)],[c_4403,c_49]) ).

cnf(c_4475,plain,
    greatest_lower_bound(identity,multiply(inverse(least_upper_bound(A,B)),least_upper_bound(B,A))) = identity,
    inference(paramod,[status(thm)],[c_2,c_11228]) ).

cnf(c_11229,plain,
    greatest_lower_bound(identity,multiply(inverse(least_upper_bound(A,B)),least_upper_bound(B,A))) = multiply(inverse(least_upper_bound(A,B)),least_upper_bound(B,A)),
    inference(paramod,[status(thm)],[c_4403,c_50]) ).

cnf(c_11230,plain,
    identity = multiply(inverse(least_upper_bound(A,B)),least_upper_bound(B,A)),
    inference(paramod,[status(thm)],[c_4475,c_11229]) ).

cnf(c_4476,plain,
    multiply(inverse(least_upper_bound(A,B)),least_upper_bound(B,A)) = identity,
    inference(copy,[status(thm)],[c_11230]) ).

cnf(c_11231,plain,
    multiply(multiply(inverse(A),inverse(least_upper_bound(identity,A))),B) = multiply(inverse(least_upper_bound(identity,A)),multiply(inverse(A),B)),
    inference(paramod,[status(thm)],[c_279,c_3]) ).

cnf(c_11232,plain,
    multiply(inverse(A),multiply(inverse(least_upper_bound(identity,A)),B)) = multiply(inverse(least_upper_bound(identity,A)),multiply(inverse(A),B)),
    inference(paramod,[status(thm)],[c_3,c_11231]) ).

cnf(c_4529,plain,
    multiply(inverse(least_upper_bound(identity,A)),multiply(inverse(A),B)) = multiply(inverse(A),multiply(inverse(least_upper_bound(identity,A)),B)),
    inference(copy,[status(thm)],[c_11232]) ).

cnf(c_11233,plain,
    multiply(multiply(inverse(A),inverse(greatest_lower_bound(identity,A))),B) = multiply(inverse(greatest_lower_bound(identity,A)),multiply(inverse(A),B)),
    inference(paramod,[status(thm)],[c_303,c_3]) ).

cnf(c_11234,plain,
    multiply(inverse(A),multiply(inverse(greatest_lower_bound(identity,A)),B)) = multiply(inverse(greatest_lower_bound(identity,A)),multiply(inverse(A),B)),
    inference(paramod,[status(thm)],[c_3,c_11233]) ).

cnf(c_4574,plain,
    multiply(inverse(greatest_lower_bound(identity,A)),multiply(inverse(A),B)) = multiply(inverse(A),multiply(inverse(greatest_lower_bound(identity,A)),B)),
    inference(copy,[status(thm)],[c_11234]) ).

cnf(c_11235,plain,
    greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),greatest_lower_bound(multiply(least_upper_bound(A,identity),least_upper_bound(identity,A)),B)) = greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),B),
    inference(paramod,[status(thm)],[c_720,c_80]) ).

cnf(c_11236,plain,
    greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),multiply(least_upper_bound(A,identity),greatest_lower_bound(least_upper_bound(identity,A),multiply(inverse(least_upper_bound(A,identity)),B)))) = greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),B),
    inference(paramod,[status(thm)],[c_483,c_11235]) ).

cnf(c_11237,plain,
    multiply(A,greatest_lower_bound(least_upper_bound(A,identity),multiply(inverse(A),multiply(least_upper_bound(A,identity),greatest_lower_bound(least_upper_bound(identity,A),multiply(inverse(least_upper_bound(A,identity)),B)))))) = greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),B),
    inference(paramod,[status(thm)],[c_483,c_11236]) ).

cnf(c_11238,plain,
    multiply(least_upper_bound(A,identity),greatest_lower_bound(A,greatest_lower_bound(least_upper_bound(identity,A),multiply(inverse(least_upper_bound(A,identity)),B)))) = greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),B),
    inference(paramod,[status(thm)],[c_550,c_11237]) ).

cnf(c_11239,plain,
    multiply(least_upper_bound(A,identity),greatest_lower_bound(A,multiply(inverse(least_upper_bound(A,identity)),B))) = greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),B),
    inference(paramod,[status(thm)],[c_80,c_11238]) ).

cnf(c_11240,plain,
    multiply(least_upper_bound(A,identity),greatest_lower_bound(A,multiply(inverse(least_upper_bound(A,identity)),B))) = multiply(A,greatest_lower_bound(least_upper_bound(A,identity),multiply(inverse(A),B))),
    inference(paramod,[status(thm)],[c_483,c_11239]) ).

cnf(c_4943,plain,
    multiply(A,greatest_lower_bound(least_upper_bound(A,identity),multiply(inverse(A),B))) = multiply(least_upper_bound(A,identity),greatest_lower_bound(A,multiply(inverse(least_upper_bound(A,identity)),B))),
    inference(copy,[status(thm)],[c_11240]) ).

cnf(c_11241,plain,
    greatest_lower_bound(identity,multiply(A,multiply(B,greatest_lower_bound(multiply(A,B),identity)))) = multiply(greatest_lower_bound(multiply(A,B),identity),greatest_lower_bound(identity,multiply(A,B))),
    inference(paramod,[status(thm)],[c_3,c_778]) ).

cnf(c_11242,plain,
    greatest_lower_bound(identity,multiply(A,multiply(B,greatest_lower_bound(identity,multiply(A,B))))) = multiply(greatest_lower_bound(multiply(A,B),identity),greatest_lower_bound(identity,multiply(A,B))),
    inference(paramod,[status(thm)],[c_4,c_11241]) ).

cnf(c_4985,plain,
    greatest_lower_bound(identity,multiply(A,multiply(B,greatest_lower_bound(identity,multiply(A,B))))) = multiply(greatest_lower_bound(identity,multiply(A,B)),greatest_lower_bound(identity,multiply(A,B))),
    inference(paramod,[status(thm)],[c_4,c_11242]) ).

cnf(c_11243,plain,
    greatest_lower_bound(least_upper_bound(identity,A),least_upper_bound(multiply(greatest_lower_bound(B,inverse(C)),C),A)) = least_upper_bound(greatest_lower_bound(identity,multiply(B,C)),A),
    inference(paramod,[status(thm)],[c_62,c_1108]) ).

cnf(c_11244,plain,
    greatest_lower_bound(least_upper_bound(identity,A),multiply(greatest_lower_bound(B,inverse(C)),least_upper_bound(C,multiply(inverse(greatest_lower_bound(B,inverse(C))),A)))) = least_upper_bound(greatest_lower_bound(identity,multiply(B,C)),A),
    inference(paramod,[status(thm)],[c_482,c_11243]) ).

cnf(c_5930,plain,
    least_upper_bound(greatest_lower_bound(identity,multiply(A,B)),C) = greatest_lower_bound(least_upper_bound(identity,C),multiply(greatest_lower_bound(A,inverse(B)),least_upper_bound(B,multiply(inverse(greatest_lower_bound(A,inverse(B))),C)))),
    inference(copy,[status(thm)],[c_11244]) ).

cnf(c_11245,plain,
    greatest_lower_bound(least_upper_bound(identity,A),least_upper_bound(greatest_lower_bound(identity,multiply(B,C)),A)) = least_upper_bound(multiply(greatest_lower_bound(B,inverse(C)),C),A),
    inference(paramod,[status(thm)],[c_62,c_1108]) ).

cnf(c_11246,plain,
    greatest_lower_bound(least_upper_bound(identity,A),greatest_lower_bound(least_upper_bound(identity,A),multiply(greatest_lower_bound(B,inverse(C)),least_upper_bound(C,multiply(inverse(greatest_lower_bound(B,inverse(C))),A))))) = least_upper_bound(multiply(greatest_lower_bound(B,inverse(C)),C),A),
    inference(paramod,[status(thm)],[c_5930,c_11245]) ).

cnf(c_11247,plain,
    greatest_lower_bound(least_upper_bound(identity,A),multiply(greatest_lower_bound(B,inverse(C)),least_upper_bound(C,multiply(inverse(greatest_lower_bound(B,inverse(C))),A)))) = least_upper_bound(multiply(greatest_lower_bound(B,inverse(C)),C),A),
    inference(paramod,[status(thm)],[c_35,c_11246]) ).

cnf(c_5931,plain,
    greatest_lower_bound(least_upper_bound(identity,A),multiply(greatest_lower_bound(B,inverse(C)),least_upper_bound(C,multiply(inverse(greatest_lower_bound(B,inverse(C))),A)))) = multiply(greatest_lower_bound(B,inverse(C)),least_upper_bound(C,multiply(inverse(greatest_lower_bound(B,inverse(C))),A))),
    inference(paramod,[status(thm)],[c_482,c_11247]) ).

cnf(c_11248,plain,
    greatest_lower_bound(least_upper_bound(identity,A),least_upper_bound(multiply(inverse(B),greatest_lower_bound(B,multiply(B,C))),A)) = least_upper_bound(greatest_lower_bound(identity,C),A),
    inference(paramod,[status(thm)],[c_243,c_1108]) ).

cnf(c_11249,plain,
    greatest_lower_bound(least_upper_bound(identity,A),multiply(inverse(B),least_upper_bound(greatest_lower_bound(B,multiply(B,C)),multiply(inverse(inverse(B)),A)))) = least_upper_bound(greatest_lower_bound(identity,C),A),
    inference(paramod,[status(thm)],[c_482,c_11248]) ).

cnf(c_11250,plain,
    greatest_lower_bound(least_upper_bound(identity,A),multiply(inverse(B),least_upper_bound(greatest_lower_bound(B,multiply(B,C)),multiply(B,A)))) = least_upper_bound(greatest_lower_bound(identity,C),A),
    inference(paramod,[status(thm)],[c_23,c_11249]) ).

cnf(c_5939,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),least_upper_bound(greatest_lower_bound(C,multiply(C,A)),multiply(C,B)))),
    inference(copy,[status(thm)],[c_11250]) ).

cnf(c_11251,plain,
    greatest_lower_bound(least_upper_bound(identity,A),least_upper_bound(greatest_lower_bound(identity,multiply(inverse(B),C)),A)) = least_upper_bound(multiply(inverse(B),greatest_lower_bound(B,C)),A),
    inference(paramod,[status(thm)],[c_49,c_1108]) ).

cnf(c_11252,plain,
    greatest_lower_bound(least_upper_bound(identity,A),greatest_lower_bound(least_upper_bound(identity,A),multiply(greatest_lower_bound(inverse(B),inverse(C)),least_upper_bound(C,multiply(inverse(greatest_lower_bound(inverse(B),inverse(C))),A))))) = least_upper_bound(multiply(inverse(B),greatest_lower_bound(B,C)),A),
    inference(paramod,[status(thm)],[c_5930,c_11251]) ).

cnf(c_11253,plain,
    greatest_lower_bound(least_upper_bound(identity,A),greatest_lower_bound(least_upper_bound(identity,A),multiply(multiply(inverse(B),greatest_lower_bound(identity,multiply(B,inverse(C)))),least_upper_bound(C,multiply(inverse(greatest_lower_bound(inverse(B),inverse(C))),A))))) = least_upper_bound(multiply(inverse(B),greatest_lower_bound(B,C)),A),
    inference(paramod,[status(thm)],[c_244,c_11252]) ).

cnf(c_11254,plain,
    greatest_lower_bound(least_upper_bound(identity,A),greatest_lower_bound(least_upper_bound(identity,A),multiply(multiply(inverse(B),greatest_lower_bound(identity,multiply(B,inverse(C)))),least_upper_bound(C,multiply(inverse(multiply(inverse(B),greatest_lower_bound(identity,multiply(B,inverse(C))))),A))))) = least_upper_bound(multiply(inverse(B),greatest_lower_bound(B,C)),A),
    inference(paramod,[status(thm)],[c_244,c_11253]) ).

cnf(c_11255,plain,
    greatest_lower_bound(least_upper_bound(identity,A),greatest_lower_bound(least_upper_bound(identity,A),multiply(multiply(inverse(B),greatest_lower_bound(identity,multiply(B,inverse(C)))),least_upper_bound(C,multiply(multiply(inverse(greatest_lower_bound(identity,multiply(B,inverse(C)))),inverse(inverse(B))),A))))) = least_upper_bound(multiply(inverse(B),greatest_lower_bound(B,C)),A),
    inference(paramod,[status(thm)],[c_24,c_11254]) ).

cnf(c_11256,plain,
    greatest_lower_bound(least_upper_bound(identity,A),greatest_lower_bound(least_upper_bound(identity,A),multiply(multiply(inverse(B),greatest_lower_bound(identity,multiply(B,inverse(C)))),least_upper_bound(C,multiply(multiply(inverse(greatest_lower_bound(identity,multiply(B,inverse(C)))),B),A))))) = least_upper_bound(multiply(inverse(B),greatest_lower_bound(B,C)),A),
    inference(paramod,[status(thm)],[c_23,c_11255]) ).

cnf(c_11257,plain,
    greatest_lower_bound(least_upper_bound(identity,A),greatest_lower_bound(least_upper_bound(identity,A),multiply(multiply(inverse(B),greatest_lower_bound(identity,multiply(B,inverse(C)))),least_upper_bound(C,multiply(inverse(greatest_lower_bound(identity,multiply(B,inverse(C)))),multiply(B,A)))))) = least_upper_bound(multiply(inverse(B),greatest_lower_bound(B,C)),A),
    inference(paramod,[status(thm)],[c_3,c_11256]) ).

cnf(c_11258,plain,
    greatest_lower_bound(least_upper_bound(identity,A),greatest_lower_bound(least_upper_bound(identity,A),multiply(inverse(B),multiply(greatest_lower_bound(identity,multiply(B,inverse(C))),least_upper_bound(C,multiply(inverse(greatest_lower_bound(identity,multiply(B,inverse(C)))),multiply(B,A))))))) = least_upper_bound(multiply(inverse(B),greatest_lower_bound(B,C)),A),
    inference(paramod,[status(thm)],[c_3,c_11257]) ).

cnf(c_11259,plain,
    greatest_lower_bound(least_upper_bound(identity,A),multiply(inverse(B),multiply(greatest_lower_bound(identity,multiply(B,inverse(C))),least_upper_bound(C,multiply(inverse(greatest_lower_bound(identity,multiply(B,inverse(C)))),multiply(B,A)))))) = least_upper_bound(multiply(inverse(B),greatest_lower_bound(B,C)),A),
    inference(paramod,[status(thm)],[c_35,c_11258]) ).

cnf(c_11260,plain,
    greatest_lower_bound(least_upper_bound(identity,A),multiply(inverse(B),multiply(greatest_lower_bound(identity,multiply(B,inverse(C))),least_upper_bound(C,multiply(inverse(greatest_lower_bound(identity,multiply(B,inverse(C)))),multiply(B,A)))))) = multiply(inverse(B),least_upper_bound(greatest_lower_bound(B,C),multiply(inverse(inverse(B)),A))),
    inference(paramod,[status(thm)],[c_482,c_11259]) ).

cnf(c_11261,plain,
    greatest_lower_bound(least_upper_bound(identity,A),multiply(inverse(B),multiply(greatest_lower_bound(identity,multiply(B,inverse(C))),least_upper_bound(C,multiply(inverse(greatest_lower_bound(identity,multiply(B,inverse(C)))),multiply(B,A)))))) = multiply(inverse(B),least_upper_bound(greatest_lower_bound(B,C),multiply(B,A))),
    inference(paramod,[status(thm)],[c_23,c_11260]) ).

cnf(c_5966,plain,
    multiply(inverse(A),least_upper_bound(greatest_lower_bound(A,B),multiply(A,C))) = greatest_lower_bound(least_upper_bound(identity,C),multiply(inverse(A),multiply(greatest_lower_bound(identity,multiply(A,inverse(B))),least_upper_bound(B,multiply(inverse(greatest_lower_bound(identity,multiply(A,inverse(B)))),multiply(A,C)))))),
    inference(copy,[status(thm)],[c_11261]) ).

cnf(c_11262,plain,
    greatest_lower_bound(least_upper_bound(A,B),least_upper_bound(multiply(inverse(C),greatest_lower_bound(identity,multiply(C,A))),B)) = least_upper_bound(greatest_lower_bound(A,inverse(C)),B),
    inference(paramod,[status(thm)],[c_861,c_1108]) ).

cnf(c_11263,plain,
    greatest_lower_bound(least_upper_bound(A,B),multiply(inverse(C),least_upper_bound(greatest_lower_bound(identity,multiply(C,A)),multiply(inverse(inverse(C)),B)))) = least_upper_bound(greatest_lower_bound(A,inverse(C)),B),
    inference(paramod,[status(thm)],[c_482,c_11262]) ).

cnf(c_11264,plain,
    greatest_lower_bound(least_upper_bound(A,B),multiply(inverse(C),least_upper_bound(greatest_lower_bound(identity,multiply(C,A)),multiply(C,B)))) = least_upper_bound(greatest_lower_bound(A,inverse(C)),B),
    inference(paramod,[status(thm)],[c_23,c_11263]) ).

cnf(c_11265,plain,
    greatest_lower_bound(least_upper_bound(A,B),multiply(inverse(C),greatest_lower_bound(least_upper_bound(identity,multiply(C,B)),multiply(greatest_lower_bound(C,inverse(A)),least_upper_bound(A,multiply(inverse(greatest_lower_bound(C,inverse(A))),multiply(C,B))))))) = least_upper_bound(greatest_lower_bound(A,inverse(C)),B),
    inference(paramod,[status(thm)],[c_5930,c_11264]) ).

cnf(c_11266,plain,
    greatest_lower_bound(least_upper_bound(A,B),multiply(inverse(C),multiply(greatest_lower_bound(C,inverse(A)),least_upper_bound(A,multiply(inverse(greatest_lower_bound(C,inverse(A))),multiply(C,B)))))) = least_upper_bound(greatest_lower_bound(A,inverse(C)),B),
    inference(paramod,[status(thm)],[c_5931,c_11265]) ).

cnf(c_5997,plain,
    least_upper_bound(greatest_lower_bound(A,inverse(B)),C) = greatest_lower_bound(least_upper_bound(A,C),multiply(inverse(B),multiply(greatest_lower_bound(B,inverse(A)),least_upper_bound(A,multiply(inverse(greatest_lower_bound(B,inverse(A))),multiply(B,C)))))),
    inference(copy,[status(thm)],[c_11266]) ).

cnf(c_11267,plain,
    greatest_lower_bound(least_upper_bound(A,B),least_upper_bound(greatest_lower_bound(A,inverse(C)),B)) = least_upper_bound(multiply(inverse(C),greatest_lower_bound(identity,multiply(C,A))),B),
    inference(paramod,[status(thm)],[c_861,c_1108]) ).

cnf(c_11268,plain,
    greatest_lower_bound(least_upper_bound(A,B),greatest_lower_bound(least_upper_bound(A,B),multiply(inverse(C),multiply(greatest_lower_bound(C,inverse(A)),least_upper_bound(A,multiply(inverse(greatest_lower_bound(C,inverse(A))),multiply(C,B))))))) = least_upper_bound(multiply(inverse(C),greatest_lower_bound(identity,multiply(C,A))),B),
    inference(paramod,[status(thm)],[c_5997,c_11267]) ).

cnf(c_11269,plain,
    greatest_lower_bound(least_upper_bound(A,B),multiply(inverse(C),multiply(greatest_lower_bound(C,inverse(A)),least_upper_bound(A,multiply(inverse(greatest_lower_bound(C,inverse(A))),multiply(C,B)))))) = least_upper_bound(multiply(inverse(C),greatest_lower_bound(identity,multiply(C,A))),B),
    inference(paramod,[status(thm)],[c_35,c_11268]) ).

cnf(c_11270,plain,
    greatest_lower_bound(least_upper_bound(A,B),multiply(inverse(C),multiply(greatest_lower_bound(C,inverse(A)),least_upper_bound(A,multiply(inverse(greatest_lower_bound(C,inverse(A))),multiply(C,B)))))) = multiply(inverse(C),least_upper_bound(greatest_lower_bound(identity,multiply(C,A)),multiply(inverse(inverse(C)),B))),
    inference(paramod,[status(thm)],[c_482,c_11269]) ).

cnf(c_11271,plain,
    greatest_lower_bound(least_upper_bound(A,B),multiply(inverse(C),multiply(greatest_lower_bound(C,inverse(A)),least_upper_bound(A,multiply(inverse(greatest_lower_bound(C,inverse(A))),multiply(C,B)))))) = multiply(inverse(C),least_upper_bound(greatest_lower_bound(identity,multiply(C,A)),multiply(C,B))),
    inference(paramod,[status(thm)],[c_23,c_11270]) ).

cnf(c_11272,plain,
    greatest_lower_bound(least_upper_bound(A,B),multiply(inverse(C),multiply(greatest_lower_bound(C,inverse(A)),least_upper_bound(A,multiply(inverse(greatest_lower_bound(C,inverse(A))),multiply(C,B)))))) = multiply(inverse(C),greatest_lower_bound(least_upper_bound(identity,multiply(C,B)),multiply(greatest_lower_bound(C,inverse(A)),least_upper_bound(A,multiply(inverse(greatest_lower_bound(C,inverse(A))),multiply(C,B)))))),
    inference(paramod,[status(thm)],[c_5930,c_11271]) ).

cnf(c_5998,plain,
    greatest_lower_bound(least_upper_bound(A,B),multiply(inverse(C),multiply(greatest_lower_bound(C,inverse(A)),least_upper_bound(A,multiply(inverse(greatest_lower_bound(C,inverse(A))),multiply(C,B)))))) = multiply(inverse(C),multiply(greatest_lower_bound(C,inverse(A)),least_upper_bound(A,multiply(inverse(greatest_lower_bound(C,inverse(A))),multiply(C,B))))),
    inference(paramod,[status(thm)],[c_5931,c_11272]) ).

cnf(c_11273,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),multiply(greatest_lower_bound(identity,multiply(C,inverse(multiply(C,A)))),least_upper_bound(multiply(C,A),multiply(inverse(greatest_lower_bound(identity,multiply(C,inverse(multiply(C,A))))),multiply(C,B))))))),
    inference(paramod,[status(thm)],[c_5966,c_5939]) ).

cnf(c_11274,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),multiply(greatest_lower_bound(identity,multiply(C,multiply(inverse(A),inverse(C)))),least_upper_bound(multiply(C,A),multiply(inverse(greatest_lower_bound(identity,multiply(C,inverse(multiply(C,A))))),multiply(C,B))))))),
    inference(paramod,[status(thm)],[c_24,c_11273]) ).

cnf(c_11275,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),multiply(multiply(C,multiply(greatest_lower_bound(identity,inverse(A)),inverse(C))),least_upper_bound(multiply(C,A),multiply(inverse(greatest_lower_bound(identity,multiply(C,inverse(multiply(C,A))))),multiply(C,B))))))),
    inference(paramod,[status(thm)],[c_2258,c_11274]) ).

cnf(c_11276,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),multiply(multiply(C,multiply(multiply(inverse(A),greatest_lower_bound(identity,A)),inverse(C))),least_upper_bound(multiply(C,A),multiply(inverse(greatest_lower_bound(identity,multiply(C,inverse(multiply(C,A))))),multiply(C,B))))))),
    inference(paramod,[status(thm)],[c_255,c_11275]) ).

cnf(c_11277,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),multiply(multiply(C,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),inverse(C)))),least_upper_bound(multiply(C,A),multiply(inverse(greatest_lower_bound(identity,multiply(C,inverse(multiply(C,A))))),multiply(C,B))))))),
    inference(paramod,[status(thm)],[c_3,c_11276]) ).

cnf(c_11278,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),multiply(multiply(C,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),inverse(C)))),least_upper_bound(multiply(C,A),multiply(inverse(greatest_lower_bound(identity,multiply(C,multiply(inverse(A),inverse(C))))),multiply(C,B))))))),
    inference(paramod,[status(thm)],[c_24,c_11277]) ).

cnf(c_11279,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),multiply(multiply(C,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),inverse(C)))),least_upper_bound(multiply(C,A),multiply(inverse(multiply(C,multiply(greatest_lower_bound(identity,inverse(A)),inverse(C)))),multiply(C,B))))))),
    inference(paramod,[status(thm)],[c_2258,c_11278]) ).

cnf(c_11280,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),multiply(multiply(C,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),inverse(C)))),least_upper_bound(multiply(C,A),multiply(inverse(multiply(C,multiply(multiply(inverse(A),greatest_lower_bound(identity,A)),inverse(C)))),multiply(C,B))))))),
    inference(paramod,[status(thm)],[c_255,c_11279]) ).

cnf(c_11281,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),multiply(multiply(C,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),inverse(C)))),least_upper_bound(multiply(C,A),multiply(inverse(multiply(C,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),inverse(C))))),multiply(C,B))))))),
    inference(paramod,[status(thm)],[c_3,c_11280]) ).

cnf(c_11282,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),multiply(multiply(C,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),inverse(C)))),least_upper_bound(multiply(C,A),multiply(multiply(inverse(multiply(inverse(A),multiply(greatest_lower_bound(identity,A),inverse(C)))),inverse(C)),multiply(C,B))))))),
    inference(paramod,[status(thm)],[c_24,c_11281]) ).

cnf(c_11283,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),multiply(multiply(C,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),inverse(C)))),least_upper_bound(multiply(C,A),multiply(multiply(multiply(inverse(multiply(greatest_lower_bound(identity,A),inverse(C))),inverse(inverse(A))),inverse(C)),multiply(C,B))))))),
    inference(paramod,[status(thm)],[c_24,c_11282]) ).

cnf(c_11284,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),multiply(multiply(C,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),inverse(C)))),least_upper_bound(multiply(C,A),multiply(multiply(multiply(multiply(inverse(inverse(C)),inverse(greatest_lower_bound(identity,A))),inverse(inverse(A))),inverse(C)),multiply(C,B))))))),
    inference(paramod,[status(thm)],[c_24,c_11283]) ).

cnf(c_11285,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),multiply(multiply(C,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),inverse(C)))),least_upper_bound(multiply(C,A),multiply(multiply(multiply(multiply(C,inverse(greatest_lower_bound(identity,A))),inverse(inverse(A))),inverse(C)),multiply(C,B))))))),
    inference(paramod,[status(thm)],[c_23,c_11284]) ).

cnf(c_11286,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),multiply(multiply(C,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),inverse(C)))),least_upper_bound(multiply(C,A),multiply(multiply(multiply(multiply(C,inverse(greatest_lower_bound(identity,A))),A),inverse(C)),multiply(C,B))))))),
    inference(paramod,[status(thm)],[c_23,c_11285]) ).

cnf(c_11287,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),multiply(multiply(C,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),inverse(C)))),least_upper_bound(multiply(C,A),multiply(multiply(multiply(C,multiply(inverse(greatest_lower_bound(identity,A)),A)),inverse(C)),multiply(C,B))))))),
    inference(paramod,[status(thm)],[c_3,c_11286]) ).

cnf(c_11288,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),multiply(multiply(C,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),inverse(C)))),least_upper_bound(multiply(C,A),multiply(multiply(multiply(C,multiply(A,inverse(greatest_lower_bound(identity,A)))),inverse(C)),multiply(C,B))))))),
    inference(paramod,[status(thm)],[c_341,c_11287]) ).

cnf(c_11289,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),multiply(multiply(C,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),inverse(C)))),least_upper_bound(multiply(C,A),multiply(multiply(C,multiply(multiply(A,inverse(greatest_lower_bound(identity,A))),inverse(C))),multiply(C,B))))))),
    inference(paramod,[status(thm)],[c_3,c_11288]) ).

cnf(c_11290,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),multiply(multiply(C,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),inverse(C)))),least_upper_bound(multiply(C,A),multiply(multiply(C,multiply(A,multiply(inverse(greatest_lower_bound(identity,A)),inverse(C)))),multiply(C,B))))))),
    inference(paramod,[status(thm)],[c_3,c_11289]) ).

cnf(c_11291,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),multiply(multiply(C,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),inverse(C)))),least_upper_bound(multiply(C,A),multiply(C,multiply(multiply(A,multiply(inverse(greatest_lower_bound(identity,A)),inverse(C))),multiply(C,B)))))))),
    inference(paramod,[status(thm)],[c_3,c_11290]) ).

cnf(c_11292,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),multiply(multiply(C,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),inverse(C)))),least_upper_bound(multiply(C,A),multiply(C,multiply(A,multiply(multiply(inverse(greatest_lower_bound(identity,A)),inverse(C)),multiply(C,B))))))))),
    inference(paramod,[status(thm)],[c_3,c_11291]) ).

cnf(c_11293,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),multiply(multiply(C,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),inverse(C)))),least_upper_bound(multiply(C,A),multiply(C,multiply(A,multiply(inverse(greatest_lower_bound(identity,A)),multiply(inverse(C),multiply(C,B)))))))))),
    inference(paramod,[status(thm)],[c_3,c_11292]) ).

cnf(c_11294,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),multiply(multiply(C,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),inverse(C)))),least_upper_bound(multiply(C,A),multiply(C,multiply(A,multiply(inverse(greatest_lower_bound(identity,A)),B)))))))),
    inference(paramod,[status(thm)],[c_27,c_11293]) ).

cnf(c_11295,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),multiply(multiply(C,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),inverse(C)))),multiply(C,least_upper_bound(A,multiply(inverse(C),multiply(C,multiply(A,multiply(inverse(greatest_lower_bound(identity,A)),B)))))))))),
    inference(paramod,[status(thm)],[c_482,c_11294]) ).

cnf(c_11296,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),multiply(multiply(C,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),inverse(C)))),multiply(C,least_upper_bound(A,multiply(A,multiply(inverse(greatest_lower_bound(identity,A)),B)))))))),
    inference(paramod,[status(thm)],[c_27,c_11295]) ).

cnf(c_11297,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),multiply(C,multiply(multiply(inverse(A),multiply(greatest_lower_bound(identity,A),inverse(C))),multiply(C,least_upper_bound(A,multiply(A,multiply(inverse(greatest_lower_bound(identity,A)),B))))))))),
    inference(paramod,[status(thm)],[c_3,c_11296]) ).

cnf(c_11298,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),multiply(C,multiply(inverse(A),multiply(multiply(greatest_lower_bound(identity,A),inverse(C)),multiply(C,least_upper_bound(A,multiply(A,multiply(inverse(greatest_lower_bound(identity,A)),B)))))))))),
    inference(paramod,[status(thm)],[c_3,c_11297]) ).

cnf(c_11299,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),multiply(C,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),multiply(inverse(C),multiply(C,least_upper_bound(A,multiply(A,multiply(inverse(greatest_lower_bound(identity,A)),B))))))))))),
    inference(paramod,[status(thm)],[c_3,c_11298]) ).

cnf(c_11300,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(C),multiply(C,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(A,multiply(A,multiply(inverse(greatest_lower_bound(identity,A)),B))))))))),
    inference(paramod,[status(thm)],[c_27,c_11299]) ).

cnf(c_11301,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(A,multiply(A,multiply(inverse(greatest_lower_bound(identity,A)),B))))))),
    inference(paramod,[status(thm)],[c_27,c_11300]) ).

cnf(c_6090,plain,
    least_upper_bound(greatest_lower_bound(identity,A),B) = greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(A,multiply(A,multiply(inverse(greatest_lower_bound(identity,A)),B)))))),
    inference(paramod,[status(thm)],[c_35,c_11301]) ).

cnf(c_6122,plain,
    least_upper_bound(greatest_lower_bound(A,inverse(B)),C) = multiply(inverse(B),multiply(greatest_lower_bound(B,inverse(A)),least_upper_bound(A,multiply(inverse(greatest_lower_bound(B,inverse(A))),multiply(B,C))))),
    inference(paramod,[status(thm)],[c_5998,c_5997]) ).

cnf(c_11302,plain,
    greatest_lower_bound(least_upper_bound(identity,multiply(inverse(A),greatest_lower_bound(A,identity))),multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(A,multiply(A,multiply(inverse(greatest_lower_bound(identity,A)),multiply(inverse(A),greatest_lower_bound(A,identity)))))))) = multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A))),
    inference(paramod,[status(thm)],[c_6090,c_374]) ).

cnf(c_11303,plain,
    greatest_lower_bound(identity,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(A,multiply(A,multiply(inverse(greatest_lower_bound(identity,A)),multiply(inverse(A),greatest_lower_bound(A,identity)))))))) = multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A))),
    inference(paramod,[status(thm)],[c_1691,c_11302]) ).

cnf(c_11304,plain,
    greatest_lower_bound(identity,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(A,multiply(A,multiply(inverse(A),multiply(inverse(greatest_lower_bound(identity,A)),greatest_lower_bound(A,identity)))))))) = multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A))),
    inference(paramod,[status(thm)],[c_4574,c_11303]) ).

cnf(c_11305,plain,
    greatest_lower_bound(identity,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(A,multiply(A,multiply(inverse(A),identity)))))) = multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A))),
    inference(paramod,[status(thm)],[c_4347,c_11304]) ).

cnf(c_11306,plain,
    greatest_lower_bound(identity,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(A,multiply(A,inverse(A)))))) = multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A))),
    inference(paramod,[status(thm)],[c_89,c_11305]) ).

cnf(c_6165,plain,
    greatest_lower_bound(identity,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(A,identity)))) = multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A))),
    inference(paramod,[status(thm)],[c_66,c_11306]) ).

cnf(c_11307,plain,
    greatest_lower_bound(least_upper_bound(multiply(A,least_upper_bound(B,identity)),C),least_upper_bound(A,C)) = least_upper_bound(greatest_lower_bound(A,multiply(A,least_upper_bound(B,identity))),C),
    inference(paramod,[status(thm)],[c_217,c_2364]) ).

cnf(c_11308,plain,
    greatest_lower_bound(multiply(A,least_upper_bound(least_upper_bound(B,identity),multiply(inverse(A),C))),least_upper_bound(A,C)) = least_upper_bound(greatest_lower_bound(A,multiply(A,least_upper_bound(B,identity))),C),
    inference(paramod,[status(thm)],[c_482,c_11307]) ).

cnf(c_11309,plain,
    greatest_lower_bound(multiply(A,least_upper_bound(B,least_upper_bound(identity,multiply(inverse(A),C)))),least_upper_bound(A,C)) = least_upper_bound(greatest_lower_bound(A,multiply(A,least_upper_bound(B,identity))),C),
    inference(paramod,[status(thm)],[c_9,c_11308]) ).

cnf(c_11310,plain,
    multiply(A,greatest_lower_bound(least_upper_bound(B,least_upper_bound(identity,multiply(inverse(A),C))),multiply(inverse(A),least_upper_bound(A,C)))) = least_upper_bound(greatest_lower_bound(A,multiply(A,least_upper_bound(B,identity))),C),
    inference(paramod,[status(thm)],[c_483,c_11309]) ).

cnf(c_6986,plain,
    multiply(A,greatest_lower_bound(least_upper_bound(B,least_upper_bound(identity,multiply(inverse(A),C))),multiply(inverse(A),least_upper_bound(A,C)))) = least_upper_bound(A,C),
    inference(paramod,[status(thm)],[c_217,c_11310]) ).

cnf(c_11311,plain,
    greatest_lower_bound(A,multiply(inverse(B),greatest_lower_bound(least_upper_bound(C,A),multiply(B,least_upper_bound(C,A))))) = greatest_lower_bound(A,multiply(inverse(B),least_upper_bound(C,A))),
    inference(paramod,[status(thm)],[c_2574,c_80]) ).

cnf(c_7543,plain,
    greatest_lower_bound(A,multiply(inverse(B),multiply(greatest_lower_bound(identity,B),least_upper_bound(C,A)))) = greatest_lower_bound(A,multiply(inverse(B),least_upper_bound(C,A))),
    inference(paramod,[status(thm)],[c_59,c_11311]) ).

cnf(c_11312,plain,
    greatest_lower_bound(identity,multiply(inverse(A),least_upper_bound(A,identity))) = multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A))),
    inference(paramod,[status(thm)],[c_7543,c_6165]) ).

cnf(c_11313,plain,
    identity = multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A))),
    inference(paramod,[status(thm)],[c_1692,c_11312]) ).

cnf(c_7597,plain,
    multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A))) = identity,
    inference(copy,[status(thm)],[c_11313]) ).

cnf(c_7602,plain,
    greatest_lower_bound(least_upper_bound(identity,A),multiply(inverse(A),least_upper_bound(A,identity))) = identity,
    inference(paramod,[status(thm)],[c_7597,c_358]) ).

cnf(c_11314,plain,
    greatest_lower_bound(identity,multiply(inverse(least_upper_bound(identity,A)),multiply(inverse(A),least_upper_bound(A,identity)))) = multiply(inverse(least_upper_bound(identity,A)),identity),
    inference(paramod,[status(thm)],[c_7602,c_49]) ).

cnf(c_11315,plain,
    greatest_lower_bound(identity,multiply(inverse(A),multiply(inverse(least_upper_bound(identity,A)),least_upper_bound(A,identity)))) = multiply(inverse(least_upper_bound(identity,A)),identity),
    inference(paramod,[status(thm)],[c_4529,c_11314]) ).

cnf(c_11316,plain,
    greatest_lower_bound(identity,multiply(inverse(A),identity)) = multiply(inverse(least_upper_bound(identity,A)),identity),
    inference(paramod,[status(thm)],[c_4476,c_11315]) ).

cnf(c_11317,plain,
    greatest_lower_bound(identity,inverse(A)) = multiply(inverse(least_upper_bound(identity,A)),identity),
    inference(paramod,[status(thm)],[c_89,c_11316]) ).

cnf(c_11318,plain,
    multiply(inverse(A),greatest_lower_bound(identity,A)) = multiply(inverse(least_upper_bound(identity,A)),identity),
    inference(paramod,[status(thm)],[c_255,c_11317]) ).

cnf(c_11319,plain,
    multiply(inverse(A),greatest_lower_bound(identity,A)) = inverse(least_upper_bound(identity,A)),
    inference(paramod,[status(thm)],[c_89,c_11318]) ).

cnf(c_7616,plain,
    inverse(least_upper_bound(identity,A)) = multiply(inverse(A),greatest_lower_bound(identity,A)),
    inference(copy,[status(thm)],[c_11319]) ).

cnf(c_11320,plain,
    greatest_lower_bound(A,identity) = greatest_lower_bound(A,multiply(inverse(A),least_upper_bound(A,identity))),
    inference(paramod,[status(thm)],[c_7602,c_80]) ).

cnf(c_7622,plain,
    greatest_lower_bound(A,multiply(inverse(A),least_upper_bound(A,identity))) = greatest_lower_bound(A,identity),
    inference(copy,[status(thm)],[c_11320]) ).

cnf(c_11321,plain,
    multiply(multiply(inverse(A),greatest_lower_bound(identity,A)),multiply(greatest_lower_bound(identity,A),least_upper_bound(A,identity))) = greatest_lower_bound(identity,A),
    inference(paramod,[status(thm)],[c_7616,c_4177]) ).

cnf(c_7940,plain,
    multiply(inverse(A),multiply(greatest_lower_bound(identity,A),multiply(greatest_lower_bound(identity,A),least_upper_bound(A,identity)))) = greatest_lower_bound(identity,A),
    inference(paramod,[status(thm)],[c_3,c_11321]) ).

cnf(c_11322,plain,
    multiply(multiply(inverse(multiply(inverse(A),B)),greatest_lower_bound(identity,multiply(inverse(A),B))),multiply(inverse(A),multiply(least_upper_bound(A,B),C))) = C,
    inference(paramod,[status(thm)],[c_7616,c_4143]) ).

cnf(c_11323,plain,
    multiply(multiply(multiply(inverse(B),inverse(inverse(A))),greatest_lower_bound(identity,multiply(inverse(A),B))),multiply(inverse(A),multiply(least_upper_bound(A,B),C))) = C,
    inference(paramod,[status(thm)],[c_24,c_11322]) ).

cnf(c_11324,plain,
    multiply(multiply(multiply(inverse(B),A),greatest_lower_bound(identity,multiply(inverse(A),B))),multiply(inverse(A),multiply(least_upper_bound(A,B),C))) = C,
    inference(paramod,[status(thm)],[c_23,c_11323]) ).

cnf(c_11325,plain,
    multiply(multiply(inverse(B),multiply(A,greatest_lower_bound(identity,multiply(inverse(A),B)))),multiply(inverse(A),multiply(least_upper_bound(A,B),C))) = C,
    inference(paramod,[status(thm)],[c_3,c_11324]) ).

cnf(c_11326,plain,
    multiply(inverse(B),multiply(multiply(A,greatest_lower_bound(identity,multiply(inverse(A),B))),multiply(inverse(A),multiply(least_upper_bound(A,B),C)))) = C,
    inference(paramod,[status(thm)],[c_3,c_11325]) ).

cnf(c_7944,plain,
    multiply(inverse(A),multiply(B,multiply(greatest_lower_bound(identity,multiply(inverse(B),A)),multiply(inverse(B),multiply(least_upper_bound(B,A),C))))) = C,
    inference(paramod,[status(thm)],[c_3,c_11326]) ).

cnf(c_11327,plain,
    inverse(least_upper_bound(A,B)) = multiply(multiply(inverse(multiply(inverse(A),B)),greatest_lower_bound(identity,multiply(inverse(A),B))),inverse(A)),
    inference(paramod,[status(thm)],[c_7616,c_3834]) ).

cnf(c_11328,plain,
    inverse(least_upper_bound(A,B)) = multiply(multiply(multiply(inverse(B),inverse(inverse(A))),greatest_lower_bound(identity,multiply(inverse(A),B))),inverse(A)),
    inference(paramod,[status(thm)],[c_24,c_11327]) ).

cnf(c_11329,plain,
    inverse(least_upper_bound(A,B)) = multiply(multiply(multiply(inverse(B),A),greatest_lower_bound(identity,multiply(inverse(A),B))),inverse(A)),
    inference(paramod,[status(thm)],[c_23,c_11328]) ).

cnf(c_11330,plain,
    inverse(least_upper_bound(A,B)) = multiply(multiply(inverse(B),multiply(A,greatest_lower_bound(identity,multiply(inverse(A),B)))),inverse(A)),
    inference(paramod,[status(thm)],[c_3,c_11329]) ).

cnf(c_11331,plain,
    inverse(least_upper_bound(A,B)) = multiply(inverse(B),multiply(multiply(A,greatest_lower_bound(identity,multiply(inverse(A),B))),inverse(A))),
    inference(paramod,[status(thm)],[c_3,c_11330]) ).

cnf(c_8019,plain,
    inverse(least_upper_bound(A,B)) = multiply(inverse(B),multiply(A,multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),inverse(A)))),
    inference(paramod,[status(thm)],[c_3,c_11331]) ).

cnf(c_11332,plain,
    multiply(A,greatest_lower_bound(least_upper_bound(A,identity),multiply(inverse(A),B))) = multiply(least_upper_bound(A,identity),greatest_lower_bound(A,multiply(multiply(inverse(identity),multiply(A,multiply(greatest_lower_bound(identity,multiply(inverse(A),identity)),inverse(A)))),B))),
    inference(paramod,[status(thm)],[c_8019,c_4943]) ).

cnf(c_11333,plain,
    multiply(A,greatest_lower_bound(least_upper_bound(A,identity),multiply(inverse(A),B))) = multiply(least_upper_bound(A,identity),greatest_lower_bound(A,multiply(multiply(identity,multiply(A,multiply(greatest_lower_bound(identity,multiply(inverse(A),identity)),inverse(A)))),B))),
    inference(paramod,[status(thm)],[c_22,c_11332]) ).

cnf(c_11334,plain,
    multiply(A,greatest_lower_bound(least_upper_bound(A,identity),multiply(inverse(A),B))) = multiply(least_upper_bound(A,identity),greatest_lower_bound(A,multiply(multiply(identity,multiply(A,multiply(greatest_lower_bound(identity,inverse(A)),inverse(A)))),B))),
    inference(paramod,[status(thm)],[c_89,c_11333]) ).

cnf(c_11335,plain,
    multiply(A,greatest_lower_bound(least_upper_bound(A,identity),multiply(inverse(A),B))) = multiply(least_upper_bound(A,identity),greatest_lower_bound(A,multiply(multiply(identity,multiply(A,multiply(multiply(inverse(A),greatest_lower_bound(identity,A)),inverse(A)))),B))),
    inference(paramod,[status(thm)],[c_255,c_11334]) ).

cnf(c_11336,plain,
    multiply(A,greatest_lower_bound(least_upper_bound(A,identity),multiply(inverse(A),B))) = multiply(least_upper_bound(A,identity),greatest_lower_bound(A,multiply(multiply(identity,multiply(A,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),inverse(A))))),B))),
    inference(paramod,[status(thm)],[c_3,c_11335]) ).

cnf(c_11337,plain,
    multiply(A,greatest_lower_bound(least_upper_bound(A,identity),multiply(inverse(A),B))) = multiply(least_upper_bound(A,identity),greatest_lower_bound(A,multiply(multiply(identity,multiply(A,multiply(inverse(A),multiply(inverse(A),greatest_lower_bound(identity,A))))),B))),
    inference(paramod,[status(thm)],[c_229,c_11336]) ).

cnf(c_11338,plain,
    multiply(A,greatest_lower_bound(least_upper_bound(A,identity),multiply(inverse(A),B))) = multiply(least_upper_bound(A,identity),greatest_lower_bound(A,multiply(multiply(identity,multiply(inverse(A),greatest_lower_bound(identity,A))),B))),
    inference(paramod,[status(thm)],[c_68,c_11337]) ).

cnf(c_11339,plain,
    multiply(A,greatest_lower_bound(least_upper_bound(A,identity),multiply(inverse(A),B))) = multiply(least_upper_bound(A,identity),greatest_lower_bound(A,multiply(multiply(inverse(A),greatest_lower_bound(identity,A)),B))),
    inference(paramod,[status(thm)],[c_1,c_11338]) ).

cnf(c_8520,plain,
    multiply(A,greatest_lower_bound(least_upper_bound(A,identity),multiply(inverse(A),B))) = multiply(least_upper_bound(A,identity),greatest_lower_bound(A,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),B)))),
    inference(paramod,[status(thm)],[c_3,c_11339]) ).

cnf(c_11340,plain,
    multiply(A,multiply(multiply(inverse(multiply(B,A)),multiply(A,multiply(greatest_lower_bound(identity,multiply(inverse(A),multiply(B,A))),inverse(A)))),multiply(least_upper_bound(B,identity),C))) = C,
    inference(paramod,[status(thm)],[c_8019,c_4191]) ).

cnf(c_11341,plain,
    multiply(A,multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,multiply(greatest_lower_bound(identity,multiply(inverse(A),multiply(B,A))),inverse(A)))),multiply(least_upper_bound(B,identity),C))) = C,
    inference(paramod,[status(thm)],[c_24,c_11340]) ).

cnf(c_11342,plain,
    multiply(A,multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,multiply(multiply(inverse(A),multiply(greatest_lower_bound(identity,B),A)),inverse(A)))),multiply(least_upper_bound(B,identity),C))) = C,
    inference(paramod,[status(thm)],[c_1900,c_11341]) ).

cnf(c_11343,plain,
    multiply(A,multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,multiply(inverse(A),multiply(multiply(greatest_lower_bound(identity,B),A),inverse(A))))),multiply(least_upper_bound(B,identity),C))) = C,
    inference(paramod,[status(thm)],[c_3,c_11342]) ).

cnf(c_11344,plain,
    multiply(A,multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,multiply(inverse(A),multiply(greatest_lower_bound(identity,B),multiply(A,inverse(A)))))),multiply(least_upper_bound(B,identity),C))) = C,
    inference(paramod,[status(thm)],[c_3,c_11343]) ).

cnf(c_11345,plain,
    multiply(A,multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,multiply(inverse(A),multiply(greatest_lower_bound(identity,B),identity)))),multiply(least_upper_bound(B,identity),C))) = C,
    inference(paramod,[status(thm)],[c_66,c_11344]) ).

cnf(c_11346,plain,
    multiply(A,multiply(multiply(multiply(inverse(A),inverse(B)),multiply(A,multiply(inverse(A),greatest_lower_bound(identity,B)))),multiply(least_upper_bound(B,identity),C))) = C,
    inference(paramod,[status(thm)],[c_89,c_11345]) ).

cnf(c_11347,plain,
    multiply(A,multiply(multiply(multiply(inverse(A),inverse(B)),greatest_lower_bound(identity,B)),multiply(least_upper_bound(B,identity),C))) = C,
    inference(paramod,[status(thm)],[c_68,c_11346]) ).

cnf(c_11348,plain,
    multiply(A,multiply(multiply(inverse(A),multiply(inverse(B),greatest_lower_bound(identity,B))),multiply(least_upper_bound(B,identity),C))) = C,
    inference(paramod,[status(thm)],[c_3,c_11347]) ).

cnf(c_11349,plain,
    multiply(A,multiply(inverse(A),multiply(multiply(inverse(B),greatest_lower_bound(identity,B)),multiply(least_upper_bound(B,identity),C)))) = C,
    inference(paramod,[status(thm)],[c_3,c_11348]) ).

cnf(c_11350,plain,
    multiply(A,multiply(inverse(A),multiply(inverse(B),multiply(greatest_lower_bound(identity,B),multiply(least_upper_bound(B,identity),C))))) = C,
    inference(paramod,[status(thm)],[c_3,c_11349]) ).

cnf(c_8571,plain,
    multiply(inverse(A),multiply(greatest_lower_bound(identity,A),multiply(least_upper_bound(A,identity),B))) = B,
    inference(paramod,[status(thm)],[c_68,c_11350]) ).

cnf(c_11351,plain,
    multiply(least_upper_bound(identity,multiply(inverse(A),B)),multiply(multiply(inverse(A),multiply(B,multiply(greatest_lower_bound(identity,multiply(inverse(B),A)),inverse(B)))),A)) = identity,
    inference(paramod,[status(thm)],[c_8019,c_1857]) ).

cnf(c_11352,plain,
    multiply(least_upper_bound(identity,multiply(inverse(A),B)),multiply(inverse(A),multiply(multiply(B,multiply(greatest_lower_bound(identity,multiply(inverse(B),A)),inverse(B))),A))) = identity,
    inference(paramod,[status(thm)],[c_3,c_11351]) ).

cnf(c_11353,plain,
    multiply(least_upper_bound(identity,multiply(inverse(A),B)),multiply(inverse(A),multiply(B,multiply(multiply(greatest_lower_bound(identity,multiply(inverse(B),A)),inverse(B)),A)))) = identity,
    inference(paramod,[status(thm)],[c_3,c_11352]) ).

cnf(c_11354,plain,
    multiply(least_upper_bound(identity,multiply(inverse(A),B)),multiply(inverse(A),multiply(B,multiply(greatest_lower_bound(identity,multiply(inverse(B),A)),multiply(inverse(B),A))))) = identity,
    inference(paramod,[status(thm)],[c_3,c_11353]) ).

cnf(c_11355,plain,
    multiply(least_upper_bound(identity,multiply(inverse(A),B)),multiply(inverse(A),multiply(B,multiply(multiply(inverse(B),A),greatest_lower_bound(identity,multiply(inverse(B),A)))))) = identity,
    inference(paramod,[status(thm)],[c_250,c_11354]) ).

cnf(c_11356,plain,
    multiply(least_upper_bound(identity,multiply(inverse(A),B)),multiply(inverse(A),multiply(B,multiply(inverse(B),multiply(A,greatest_lower_bound(identity,multiply(inverse(B),A))))))) = identity,
    inference(paramod,[status(thm)],[c_3,c_11355]) ).

cnf(c_11357,plain,
    multiply(least_upper_bound(identity,multiply(inverse(A),B)),multiply(inverse(A),multiply(A,greatest_lower_bound(identity,multiply(inverse(B),A))))) = identity,
    inference(paramod,[status(thm)],[c_68,c_11356]) ).

cnf(c_8685,plain,
    multiply(least_upper_bound(identity,multiply(inverse(A),B)),greatest_lower_bound(identity,multiply(inverse(B),A))) = identity,
    inference(paramod,[status(thm)],[c_27,c_11357]) ).

cnf(c_11358,plain,
    least_upper_bound(identity,A) = multiply(multiply(inverse(C),multiply(B,multiply(greatest_lower_bound(identity,multiply(inverse(B),C)),inverse(B)))),least_upper_bound(B,least_upper_bound(C,multiply(least_upper_bound(B,C),A)))),
    inference(paramod,[status(thm)],[c_8019,c_967]) ).

cnf(c_11359,plain,
    least_upper_bound(identity,A) = multiply(inverse(C),multiply(multiply(B,multiply(greatest_lower_bound(identity,multiply(inverse(B),C)),inverse(B))),least_upper_bound(B,least_upper_bound(C,multiply(least_upper_bound(B,C),A))))),
    inference(paramod,[status(thm)],[c_3,c_11358]) ).

cnf(c_11360,plain,
    least_upper_bound(identity,A) = multiply(inverse(C),multiply(B,multiply(multiply(greatest_lower_bound(identity,multiply(inverse(B),C)),inverse(B)),least_upper_bound(B,least_upper_bound(C,multiply(least_upper_bound(B,C),A)))))),
    inference(paramod,[status(thm)],[c_3,c_11359]) ).

cnf(c_8737,plain,
    least_upper_bound(identity,A) = multiply(inverse(B),multiply(C,multiply(greatest_lower_bound(identity,multiply(inverse(C),B)),multiply(inverse(C),least_upper_bound(C,least_upper_bound(B,multiply(least_upper_bound(C,B),A))))))),
    inference(paramod,[status(thm)],[c_3,c_11360]) ).

cnf(c_11361,plain,
    greatest_lower_bound(identity,multiply(A,least_upper_bound(A,identity))) = multiply(least_upper_bound(A,identity),greatest_lower_bound(A,multiply(inverse(identity),multiply(A,multiply(greatest_lower_bound(identity,multiply(inverse(A),identity)),inverse(A)))))),
    inference(paramod,[status(thm)],[c_8019,c_880]) ).

cnf(c_11362,plain,
    greatest_lower_bound(identity,multiply(A,least_upper_bound(A,identity))) = multiply(least_upper_bound(A,identity),greatest_lower_bound(A,multiply(identity,multiply(A,multiply(greatest_lower_bound(identity,multiply(inverse(A),identity)),inverse(A)))))),
    inference(paramod,[status(thm)],[c_22,c_11361]) ).

cnf(c_11363,plain,
    greatest_lower_bound(identity,multiply(A,least_upper_bound(A,identity))) = multiply(least_upper_bound(A,identity),greatest_lower_bound(A,multiply(identity,multiply(A,multiply(greatest_lower_bound(identity,inverse(A)),inverse(A)))))),
    inference(paramod,[status(thm)],[c_89,c_11362]) ).

cnf(c_11364,plain,
    greatest_lower_bound(identity,multiply(A,least_upper_bound(A,identity))) = multiply(least_upper_bound(A,identity),greatest_lower_bound(A,multiply(identity,multiply(A,multiply(multiply(inverse(A),greatest_lower_bound(identity,A)),inverse(A)))))),
    inference(paramod,[status(thm)],[c_255,c_11363]) ).

cnf(c_11365,plain,
    greatest_lower_bound(identity,multiply(A,least_upper_bound(A,identity))) = multiply(least_upper_bound(A,identity),greatest_lower_bound(A,multiply(identity,multiply(A,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),inverse(A))))))),
    inference(paramod,[status(thm)],[c_3,c_11364]) ).

cnf(c_11366,plain,
    greatest_lower_bound(identity,multiply(A,least_upper_bound(A,identity))) = multiply(least_upper_bound(A,identity),greatest_lower_bound(A,multiply(identity,multiply(A,multiply(inverse(A),multiply(inverse(A),greatest_lower_bound(identity,A))))))),
    inference(paramod,[status(thm)],[c_229,c_11365]) ).

cnf(c_11367,plain,
    greatest_lower_bound(identity,multiply(A,least_upper_bound(A,identity))) = multiply(least_upper_bound(A,identity),greatest_lower_bound(A,multiply(identity,multiply(inverse(A),greatest_lower_bound(identity,A))))),
    inference(paramod,[status(thm)],[c_68,c_11366]) ).

cnf(c_11368,plain,
    greatest_lower_bound(identity,multiply(A,least_upper_bound(A,identity))) = multiply(least_upper_bound(A,identity),greatest_lower_bound(A,multiply(inverse(A),greatest_lower_bound(identity,A)))),
    inference(paramod,[status(thm)],[c_1,c_11367]) ).

cnf(c_11369,plain,
    greatest_lower_bound(identity,multiply(A,least_upper_bound(A,identity))) = multiply(least_upper_bound(A,identity),multiply(inverse(A),multiply(greatest_lower_bound(A,identity),greatest_lower_bound(identity,A)))),
    inference(paramod,[status(thm)],[c_400,c_11368]) ).

cnf(c_11370,plain,
    greatest_lower_bound(identity,multiply(A,least_upper_bound(A,identity))) = multiply(inverse(A),multiply(least_upper_bound(A,identity),multiply(greatest_lower_bound(A,identity),greatest_lower_bound(identity,A)))),
    inference(paramod,[status(thm)],[c_378,c_11369]) ).

cnf(c_11371,plain,
    greatest_lower_bound(identity,multiply(A,least_upper_bound(A,identity))) = multiply(inverse(A),multiply(greatest_lower_bound(identity,A),multiply(least_upper_bound(A,identity),greatest_lower_bound(identity,A)))),
    inference(paramod,[status(thm)],[c_602,c_11370]) ).

cnf(c_11372,plain,
    greatest_lower_bound(identity,multiply(A,least_upper_bound(A,identity))) = multiply(inverse(A),multiply(greatest_lower_bound(identity,A),multiply(greatest_lower_bound(identity,A),least_upper_bound(A,identity)))),
    inference(paramod,[status(thm)],[c_296,c_11371]) ).

cnf(c_8741,plain,
    greatest_lower_bound(identity,multiply(A,least_upper_bound(A,identity))) = greatest_lower_bound(identity,A),
    inference(paramod,[status(thm)],[c_7940,c_11372]) ).

cnf(c_8846,plain,
    greatest_lower_bound(A,multiply(inverse(A),least_upper_bound(identity,A))) = greatest_lower_bound(A,identity),
    inference(paramod,[status(thm)],[c_5,c_7622]) ).

cnf(c_11373,plain,
    greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),multiply(inverse(multiply(A,least_upper_bound(A,identity))),multiply(least_upper_bound(A,identity),least_upper_bound(identity,A)))) = greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),identity),
    inference(paramod,[status(thm)],[c_720,c_8846]) ).

cnf(c_11374,plain,
    greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),multiply(multiply(inverse(least_upper_bound(A,identity)),inverse(A)),multiply(least_upper_bound(A,identity),least_upper_bound(identity,A)))) = greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),identity),
    inference(paramod,[status(thm)],[c_24,c_11373]) ).

cnf(c_11375,plain,
    greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),multiply(multiply(multiply(inverse(identity),multiply(A,multiply(greatest_lower_bound(identity,multiply(inverse(A),identity)),inverse(A)))),inverse(A)),multiply(least_upper_bound(A,identity),least_upper_bound(identity,A)))) = greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),identity),
    inference(paramod,[status(thm)],[c_8019,c_11374]) ).

cnf(c_11376,plain,
    greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),multiply(multiply(multiply(identity,multiply(A,multiply(greatest_lower_bound(identity,multiply(inverse(A),identity)),inverse(A)))),inverse(A)),multiply(least_upper_bound(A,identity),least_upper_bound(identity,A)))) = greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),identity),
    inference(paramod,[status(thm)],[c_22,c_11375]) ).

cnf(c_11377,plain,
    greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),multiply(multiply(multiply(identity,multiply(A,multiply(greatest_lower_bound(identity,inverse(A)),inverse(A)))),inverse(A)),multiply(least_upper_bound(A,identity),least_upper_bound(identity,A)))) = greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),identity),
    inference(paramod,[status(thm)],[c_89,c_11376]) ).

cnf(c_11378,plain,
    greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),multiply(multiply(multiply(identity,multiply(A,multiply(multiply(inverse(A),greatest_lower_bound(identity,A)),inverse(A)))),inverse(A)),multiply(least_upper_bound(A,identity),least_upper_bound(identity,A)))) = greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),identity),
    inference(paramod,[status(thm)],[c_255,c_11377]) ).

cnf(c_11379,plain,
    greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),multiply(multiply(multiply(identity,multiply(A,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),inverse(A))))),inverse(A)),multiply(least_upper_bound(A,identity),least_upper_bound(identity,A)))) = greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),identity),
    inference(paramod,[status(thm)],[c_3,c_11378]) ).

cnf(c_11380,plain,
    greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),multiply(multiply(multiply(identity,multiply(A,multiply(inverse(A),multiply(inverse(A),greatest_lower_bound(identity,A))))),inverse(A)),multiply(least_upper_bound(A,identity),least_upper_bound(identity,A)))) = greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),identity),
    inference(paramod,[status(thm)],[c_229,c_11379]) ).

cnf(c_11381,plain,
    greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),multiply(multiply(multiply(identity,multiply(inverse(A),greatest_lower_bound(identity,A))),inverse(A)),multiply(least_upper_bound(A,identity),least_upper_bound(identity,A)))) = greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),identity),
    inference(paramod,[status(thm)],[c_68,c_11380]) ).

cnf(c_11382,plain,
    greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),multiply(multiply(multiply(inverse(A),greatest_lower_bound(identity,A)),inverse(A)),multiply(least_upper_bound(A,identity),least_upper_bound(identity,A)))) = greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),identity),
    inference(paramod,[status(thm)],[c_1,c_11381]) ).

cnf(c_11383,plain,
    greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),multiply(multiply(inverse(A),multiply(greatest_lower_bound(identity,A),inverse(A))),multiply(least_upper_bound(A,identity),least_upper_bound(identity,A)))) = greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),identity),
    inference(paramod,[status(thm)],[c_3,c_11382]) ).

cnf(c_11384,plain,
    greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),multiply(multiply(inverse(A),multiply(inverse(A),greatest_lower_bound(identity,A))),multiply(least_upper_bound(A,identity),least_upper_bound(identity,A)))) = greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),identity),
    inference(paramod,[status(thm)],[c_229,c_11383]) ).

cnf(c_11385,plain,
    greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),multiply(inverse(A),multiply(multiply(inverse(A),greatest_lower_bound(identity,A)),multiply(least_upper_bound(A,identity),least_upper_bound(identity,A))))) = greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),identity),
    inference(paramod,[status(thm)],[c_3,c_11384]) ).

cnf(c_11386,plain,
    greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),multiply(inverse(A),multiply(inverse(A),multiply(greatest_lower_bound(identity,A),multiply(least_upper_bound(A,identity),least_upper_bound(identity,A)))))) = greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),identity),
    inference(paramod,[status(thm)],[c_3,c_11385]) ).

cnf(c_11387,plain,
    greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),multiply(inverse(A),least_upper_bound(identity,A))) = greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),identity),
    inference(paramod,[status(thm)],[c_8571,c_11386]) ).

cnf(c_11388,plain,
    multiply(A,greatest_lower_bound(least_upper_bound(A,identity),multiply(inverse(A),multiply(inverse(A),least_upper_bound(identity,A))))) = greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),identity),
    inference(paramod,[status(thm)],[c_483,c_11387]) ).

cnf(c_11389,plain,
    multiply(least_upper_bound(A,identity),greatest_lower_bound(A,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),multiply(inverse(A),least_upper_bound(identity,A)))))) = greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),identity),
    inference(paramod,[status(thm)],[c_8520,c_11388]) ).

cnf(c_11390,plain,
    multiply(least_upper_bound(A,identity),greatest_lower_bound(A,multiply(inverse(A),multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A)))))) = greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),identity),
    inference(paramod,[status(thm)],[c_331,c_11389]) ).

cnf(c_11391,plain,
    multiply(least_upper_bound(A,identity),greatest_lower_bound(A,multiply(inverse(A),identity))) = greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),identity),
    inference(paramod,[status(thm)],[c_7597,c_11390]) ).

cnf(c_11392,plain,
    multiply(least_upper_bound(A,identity),greatest_lower_bound(A,inverse(A))) = greatest_lower_bound(multiply(A,least_upper_bound(A,identity)),identity),
    inference(paramod,[status(thm)],[c_89,c_11391]) ).

cnf(c_11393,plain,
    multiply(least_upper_bound(A,identity),greatest_lower_bound(A,inverse(A))) = greatest_lower_bound(identity,multiply(A,least_upper_bound(A,identity))),
    inference(paramod,[status(thm)],[c_4,c_11392]) ).

cnf(c_8934,plain,
    multiply(least_upper_bound(A,identity),greatest_lower_bound(A,inverse(A))) = greatest_lower_bound(identity,A),
    inference(paramod,[status(thm)],[c_8741,c_11393]) ).

cnf(c_11394,plain,
    least_upper_bound(greatest_lower_bound(A,inverse(A)),greatest_lower_bound(identity,A)) = multiply(least_upper_bound(identity,least_upper_bound(A,identity)),greatest_lower_bound(A,inverse(A))),
    inference(paramod,[status(thm)],[c_8934,c_52]) ).

cnf(c_11395,plain,
    multiply(inverse(A),multiply(greatest_lower_bound(A,inverse(A)),least_upper_bound(A,multiply(inverse(greatest_lower_bound(A,inverse(A))),multiply(A,greatest_lower_bound(identity,A)))))) = multiply(least_upper_bound(identity,least_upper_bound(A,identity)),greatest_lower_bound(A,inverse(A))),
    inference(paramod,[status(thm)],[c_6122,c_11394]) ).

cnf(c_11396,plain,
    multiply(inverse(A),multiply(greatest_lower_bound(A,inverse(A)),least_upper_bound(A,multiply(inverse(greatest_lower_bound(A,inverse(A))),multiply(A,greatest_lower_bound(identity,A)))))) = multiply(least_upper_bound(A,identity),greatest_lower_bound(A,inverse(A))),
    inference(paramod,[status(thm)],[c_34,c_11395]) ).

cnf(c_8975,plain,
    multiply(inverse(A),multiply(greatest_lower_bound(A,inverse(A)),least_upper_bound(A,multiply(inverse(greatest_lower_bound(A,inverse(A))),multiply(A,greatest_lower_bound(identity,A)))))) = greatest_lower_bound(identity,A),
    inference(paramod,[status(thm)],[c_8934,c_11396]) ).

cnf(c_11397,plain,
    least_upper_bound(identity,least_upper_bound(A,identity)) = multiply(least_upper_bound(greatest_lower_bound(A,inverse(A)),greatest_lower_bound(identity,A)),inverse(greatest_lower_bound(A,inverse(A)))),
    inference(paramod,[status(thm)],[c_8934,c_2466]) ).

cnf(c_11398,plain,
    least_upper_bound(A,identity) = multiply(least_upper_bound(greatest_lower_bound(A,inverse(A)),greatest_lower_bound(identity,A)),inverse(greatest_lower_bound(A,inverse(A)))),
    inference(paramod,[status(thm)],[c_34,c_11397]) ).

cnf(c_11399,plain,
    least_upper_bound(A,identity) = multiply(multiply(inverse(A),multiply(greatest_lower_bound(A,inverse(A)),least_upper_bound(A,multiply(inverse(greatest_lower_bound(A,inverse(A))),multiply(A,greatest_lower_bound(identity,A)))))),inverse(greatest_lower_bound(A,inverse(A)))),
    inference(paramod,[status(thm)],[c_6122,c_11398]) ).

cnf(c_8985,plain,
    least_upper_bound(A,identity) = multiply(greatest_lower_bound(identity,A),inverse(greatest_lower_bound(A,inverse(A)))),
    inference(paramod,[status(thm)],[c_8975,c_11399]) ).

cnf(c_9772,plain,
    least_upper_bound(A,least_upper_bound(B,multiply(least_upper_bound(A,B),C))) = multiply(least_upper_bound(A,B),multiply(greatest_lower_bound(identity,C),inverse(greatest_lower_bound(C,inverse(C))))),
    inference(paramod,[status(thm)],[c_8985,c_214]) ).

cnf(c_9783,plain,
    least_upper_bound(A,multiply(A,B)) = multiply(A,multiply(greatest_lower_bound(identity,B),inverse(greatest_lower_bound(B,inverse(B))))),
    inference(paramod,[status(thm)],[c_8985,c_91]) ).

cnf(c_11400,plain,
    least_upper_bound(identity,A) = multiply(inverse(B),multiply(C,multiply(greatest_lower_bound(identity,multiply(inverse(C),B)),multiply(inverse(C),multiply(least_upper_bound(C,B),multiply(greatest_lower_bound(identity,A),inverse(greatest_lower_bound(A,inverse(A))))))))),
    inference(paramod,[status(thm)],[c_9772,c_8737]) ).

cnf(c_9876,plain,
    least_upper_bound(identity,A) = multiply(greatest_lower_bound(identity,A),inverse(greatest_lower_bound(A,inverse(A)))),
    inference(paramod,[status(thm)],[c_7944,c_11400]) ).

cnf(c_11401,plain,
    multiply(inverse(A),multiply(A,multiply(greatest_lower_bound(identity,multiply(inverse(B),C)),inverse(greatest_lower_bound(multiply(inverse(B),C),inverse(multiply(inverse(B),C))))))) = multiply(inverse(B),least_upper_bound(B,C)),
    inference(paramod,[status(thm)],[c_9783,c_1733]) ).

cnf(c_11402,plain,
    multiply(inverse(A),multiply(A,multiply(greatest_lower_bound(identity,multiply(inverse(B),C)),inverse(greatest_lower_bound(multiply(inverse(B),C),multiply(inverse(C),inverse(inverse(B)))))))) = multiply(inverse(B),least_upper_bound(B,C)),
    inference(paramod,[status(thm)],[c_24,c_11401]) ).

cnf(c_11403,plain,
    multiply(inverse(A),multiply(A,multiply(greatest_lower_bound(identity,multiply(inverse(B),C)),inverse(greatest_lower_bound(multiply(inverse(B),C),multiply(inverse(C),B)))))) = multiply(inverse(B),least_upper_bound(B,C)),
    inference(paramod,[status(thm)],[c_23,c_11402]) ).

cnf(c_11404,plain,
    multiply(inverse(A),multiply(A,multiply(greatest_lower_bound(identity,multiply(inverse(B),C)),inverse(multiply(inverse(B),greatest_lower_bound(C,multiply(inverse(inverse(B)),multiply(inverse(C),B)))))))) = multiply(inverse(B),least_upper_bound(B,C)),
    inference(paramod,[status(thm)],[c_483,c_11403]) ).

cnf(c_11405,plain,
    multiply(inverse(A),multiply(A,multiply(greatest_lower_bound(identity,multiply(inverse(B),C)),inverse(multiply(inverse(B),greatest_lower_bound(C,multiply(B,multiply(inverse(C),B)))))))) = multiply(inverse(B),least_upper_bound(B,C)),
    inference(paramod,[status(thm)],[c_23,c_11404]) ).

cnf(c_11406,plain,
    multiply(inverse(A),multiply(A,multiply(greatest_lower_bound(identity,multiply(inverse(B),C)),multiply(inverse(greatest_lower_bound(C,multiply(B,multiply(inverse(C),B)))),inverse(inverse(B)))))) = multiply(inverse(B),least_upper_bound(B,C)),
    inference(paramod,[status(thm)],[c_24,c_11405]) ).

cnf(c_11407,plain,
    multiply(inverse(A),multiply(A,multiply(greatest_lower_bound(identity,multiply(inverse(B),C)),multiply(inverse(greatest_lower_bound(C,multiply(B,multiply(inverse(C),B)))),B)))) = multiply(inverse(B),least_upper_bound(B,C)),
    inference(paramod,[status(thm)],[c_23,c_11406]) ).

cnf(c_11408,plain,
    multiply(greatest_lower_bound(identity,multiply(inverse(B),C)),multiply(inverse(greatest_lower_bound(C,multiply(B,multiply(inverse(C),B)))),B)) = multiply(inverse(B),least_upper_bound(B,C)),
    inference(paramod,[status(thm)],[c_27,c_11407]) ).

cnf(c_9925,plain,
    multiply(inverse(A),least_upper_bound(A,B)) = multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(inverse(greatest_lower_bound(B,multiply(A,multiply(inverse(B),A)))),A)),
    inference(copy,[status(thm)],[c_11408]) ).

cnf(c_11409,plain,
    multiply(multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),inverse(greatest_lower_bound(multiply(inverse(A),B),inverse(multiply(inverse(A),B))))),greatest_lower_bound(identity,multiply(inverse(B),A))) = identity,
    inference(paramod,[status(thm)],[c_9876,c_8685]) ).

cnf(c_11410,plain,
    multiply(multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),inverse(greatest_lower_bound(multiply(inverse(A),B),multiply(inverse(B),inverse(inverse(A)))))),greatest_lower_bound(identity,multiply(inverse(B),A))) = identity,
    inference(paramod,[status(thm)],[c_24,c_11409]) ).

cnf(c_11411,plain,
    multiply(multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),inverse(greatest_lower_bound(multiply(inverse(A),B),multiply(inverse(B),A)))),greatest_lower_bound(identity,multiply(inverse(B),A))) = identity,
    inference(paramod,[status(thm)],[c_23,c_11410]) ).

cnf(c_11412,plain,
    multiply(multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),inverse(multiply(inverse(A),greatest_lower_bound(B,multiply(inverse(inverse(A)),multiply(inverse(B),A)))))),greatest_lower_bound(identity,multiply(inverse(B),A))) = identity,
    inference(paramod,[status(thm)],[c_483,c_11411]) ).

cnf(c_11413,plain,
    multiply(multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),inverse(multiply(inverse(A),greatest_lower_bound(B,multiply(A,multiply(inverse(B),A)))))),greatest_lower_bound(identity,multiply(inverse(B),A))) = identity,
    inference(paramod,[status(thm)],[c_23,c_11412]) ).

cnf(c_11414,plain,
    multiply(multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(inverse(greatest_lower_bound(B,multiply(A,multiply(inverse(B),A)))),inverse(inverse(A)))),greatest_lower_bound(identity,multiply(inverse(B),A))) = identity,
    inference(paramod,[status(thm)],[c_24,c_11413]) ).

cnf(c_11415,plain,
    multiply(multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(inverse(greatest_lower_bound(B,multiply(A,multiply(inverse(B),A)))),A)),greatest_lower_bound(identity,multiply(inverse(B),A))) = identity,
    inference(paramod,[status(thm)],[c_23,c_11414]) ).

cnf(c_11416,plain,
    multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(multiply(inverse(greatest_lower_bound(B,multiply(A,multiply(inverse(B),A)))),A),greatest_lower_bound(identity,multiply(inverse(B),A)))) = identity,
    inference(paramod,[status(thm)],[c_3,c_11415]) ).

cnf(c_10021,plain,
    multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(inverse(greatest_lower_bound(B,multiply(A,multiply(inverse(B),A)))),multiply(A,greatest_lower_bound(identity,multiply(inverse(B),A))))) = identity,
    inference(paramod,[status(thm)],[c_3,c_11416]) ).

cnf(c_11417,plain,
    multiply(A,greatest_lower_bound(least_upper_bound(B,multiply(greatest_lower_bound(identity,multiply(inverse(A),C)),inverse(greatest_lower_bound(multiply(inverse(A),C),inverse(multiply(inverse(A),C)))))),multiply(inverse(A),least_upper_bound(A,C)))) = least_upper_bound(A,C),
    inference(paramod,[status(thm)],[c_9876,c_6986]) ).

cnf(c_11418,plain,
    multiply(A,greatest_lower_bound(least_upper_bound(B,multiply(greatest_lower_bound(identity,multiply(inverse(A),C)),inverse(greatest_lower_bound(multiply(inverse(A),C),multiply(inverse(C),inverse(inverse(A))))))),multiply(inverse(A),least_upper_bound(A,C)))) = least_upper_bound(A,C),
    inference(paramod,[status(thm)],[c_24,c_11417]) ).

cnf(c_11419,plain,
    multiply(A,greatest_lower_bound(least_upper_bound(B,multiply(greatest_lower_bound(identity,multiply(inverse(A),C)),inverse(greatest_lower_bound(multiply(inverse(A),C),multiply(inverse(C),A))))),multiply(inverse(A),least_upper_bound(A,C)))) = least_upper_bound(A,C),
    inference(paramod,[status(thm)],[c_23,c_11418]) ).

cnf(c_11420,plain,
    multiply(A,greatest_lower_bound(least_upper_bound(B,multiply(greatest_lower_bound(identity,multiply(inverse(A),C)),inverse(multiply(inverse(A),greatest_lower_bound(C,multiply(inverse(inverse(A)),multiply(inverse(C),A))))))),multiply(inverse(A),least_upper_bound(A,C)))) = least_upper_bound(A,C),
    inference(paramod,[status(thm)],[c_483,c_11419]) ).

cnf(c_11421,plain,
    multiply(A,greatest_lower_bound(least_upper_bound(B,multiply(greatest_lower_bound(identity,multiply(inverse(A),C)),inverse(multiply(inverse(A),greatest_lower_bound(C,multiply(A,multiply(inverse(C),A))))))),multiply(inverse(A),least_upper_bound(A,C)))) = least_upper_bound(A,C),
    inference(paramod,[status(thm)],[c_23,c_11420]) ).

cnf(c_11422,plain,
    multiply(A,greatest_lower_bound(least_upper_bound(B,multiply(greatest_lower_bound(identity,multiply(inverse(A),C)),multiply(inverse(greatest_lower_bound(C,multiply(A,multiply(inverse(C),A)))),inverse(inverse(A))))),multiply(inverse(A),least_upper_bound(A,C)))) = least_upper_bound(A,C),
    inference(paramod,[status(thm)],[c_24,c_11421]) ).

cnf(c_11423,plain,
    multiply(A,greatest_lower_bound(least_upper_bound(B,multiply(greatest_lower_bound(identity,multiply(inverse(A),C)),multiply(inverse(greatest_lower_bound(C,multiply(A,multiply(inverse(C),A)))),A))),multiply(inverse(A),least_upper_bound(A,C)))) = least_upper_bound(A,C),
    inference(paramod,[status(thm)],[c_23,c_11422]) ).

cnf(c_11424,plain,
    multiply(A,greatest_lower_bound(least_upper_bound(B,multiply(greatest_lower_bound(identity,multiply(inverse(A),C)),multiply(inverse(greatest_lower_bound(C,multiply(A,multiply(inverse(C),A)))),A))),multiply(greatest_lower_bound(identity,multiply(inverse(A),C)),multiply(inverse(greatest_lower_bound(C,multiply(A,multiply(inverse(C),A)))),A)))) = least_upper_bound(A,C),
    inference(paramod,[status(thm)],[c_9925,c_11423]) ).

cnf(c_11425,plain,
    multiply(A,greatest_lower_bound(multiply(greatest_lower_bound(identity,multiply(inverse(A),C)),multiply(inverse(greatest_lower_bound(C,multiply(A,multiply(inverse(C),A)))),A)),least_upper_bound(B,multiply(greatest_lower_bound(identity,multiply(inverse(A),C)),multiply(inverse(greatest_lower_bound(C,multiply(A,multiply(inverse(C),A)))),A))))) = least_upper_bound(A,C),
    inference(paramod,[status(thm)],[c_4,c_11424]) ).

cnf(c_11426,plain,
    multiply(A,multiply(greatest_lower_bound(identity,multiply(inverse(A),C)),multiply(inverse(greatest_lower_bound(C,multiply(A,multiply(inverse(C),A)))),A))) = least_upper_bound(A,C),
    inference(paramod,[status(thm)],[c_42,c_11425]) ).

cnf(c_10062,plain,
    least_upper_bound(A,B) = multiply(A,multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(inverse(greatest_lower_bound(B,multiply(A,multiply(inverse(B),A)))),A))),
    inference(copy,[status(thm)],[c_11426]) ).

cnf(c_11427,plain,
    multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(identity,multiply(greatest_lower_bound(identity,multiply(inverse(identity),multiply(inverse(A),B))),multiply(inverse(greatest_lower_bound(multiply(inverse(A),B),multiply(identity,multiply(inverse(multiply(inverse(A),B)),identity)))),identity)))) = multiply(inverse(A),multiply(least_upper_bound(B,A),greatest_lower_bound(identity,multiply(inverse(A),B)))),
    inference(paramod,[status(thm)],[c_10062,c_1856]) ).

cnf(c_11428,plain,
    multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(identity,multiply(greatest_lower_bound(identity,multiply(identity,multiply(inverse(A),B))),multiply(inverse(greatest_lower_bound(multiply(inverse(A),B),multiply(identity,multiply(inverse(multiply(inverse(A),B)),identity)))),identity)))) = multiply(inverse(A),multiply(least_upper_bound(B,A),greatest_lower_bound(identity,multiply(inverse(A),B)))),
    inference(paramod,[status(thm)],[c_22,c_11427]) ).

cnf(c_11429,plain,
    multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(identity,multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(inverse(greatest_lower_bound(multiply(inverse(A),B),multiply(identity,multiply(inverse(multiply(inverse(A),B)),identity)))),identity)))) = multiply(inverse(A),multiply(least_upper_bound(B,A),greatest_lower_bound(identity,multiply(inverse(A),B)))),
    inference(paramod,[status(thm)],[c_1,c_11428]) ).

cnf(c_11430,plain,
    multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(identity,multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(inverse(greatest_lower_bound(multiply(inverse(A),B),multiply(identity,multiply(multiply(inverse(B),inverse(inverse(A))),identity)))),identity)))) = multiply(inverse(A),multiply(least_upper_bound(B,A),greatest_lower_bound(identity,multiply(inverse(A),B)))),
    inference(paramod,[status(thm)],[c_24,c_11429]) ).

cnf(c_11431,plain,
    multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(identity,multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(inverse(greatest_lower_bound(multiply(inverse(A),B),multiply(identity,multiply(multiply(inverse(B),A),identity)))),identity)))) = multiply(inverse(A),multiply(least_upper_bound(B,A),greatest_lower_bound(identity,multiply(inverse(A),B)))),
    inference(paramod,[status(thm)],[c_23,c_11430]) ).

cnf(c_11432,plain,
    multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(identity,multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(inverse(greatest_lower_bound(multiply(inverse(A),B),multiply(identity,multiply(inverse(B),A)))),identity)))) = multiply(inverse(A),multiply(least_upper_bound(B,A),greatest_lower_bound(identity,multiply(inverse(A),B)))),
    inference(paramod,[status(thm)],[c_89,c_11431]) ).

cnf(c_11433,plain,
    multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(identity,multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(inverse(greatest_lower_bound(multiply(inverse(A),B),multiply(inverse(B),A))),identity)))) = multiply(inverse(A),multiply(least_upper_bound(B,A),greatest_lower_bound(identity,multiply(inverse(A),B)))),
    inference(paramod,[status(thm)],[c_1,c_11432]) ).

cnf(c_11434,plain,
    multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(identity,multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(inverse(multiply(inverse(A),greatest_lower_bound(B,multiply(inverse(inverse(A)),multiply(inverse(B),A))))),identity)))) = multiply(inverse(A),multiply(least_upper_bound(B,A),greatest_lower_bound(identity,multiply(inverse(A),B)))),
    inference(paramod,[status(thm)],[c_483,c_11433]) ).

cnf(c_11435,plain,
    multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(identity,multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(inverse(multiply(inverse(A),greatest_lower_bound(B,multiply(A,multiply(inverse(B),A))))),identity)))) = multiply(inverse(A),multiply(least_upper_bound(B,A),greatest_lower_bound(identity,multiply(inverse(A),B)))),
    inference(paramod,[status(thm)],[c_23,c_11434]) ).

cnf(c_11436,plain,
    multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(identity,multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(multiply(inverse(greatest_lower_bound(B,multiply(A,multiply(inverse(B),A)))),inverse(inverse(A))),identity)))) = multiply(inverse(A),multiply(least_upper_bound(B,A),greatest_lower_bound(identity,multiply(inverse(A),B)))),
    inference(paramod,[status(thm)],[c_24,c_11435]) ).

cnf(c_11437,plain,
    multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(identity,multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(multiply(inverse(greatest_lower_bound(B,multiply(A,multiply(inverse(B),A)))),A),identity)))) = multiply(inverse(A),multiply(least_upper_bound(B,A),greatest_lower_bound(identity,multiply(inverse(A),B)))),
    inference(paramod,[status(thm)],[c_23,c_11436]) ).

cnf(c_11438,plain,
    multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(identity,multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(inverse(greatest_lower_bound(B,multiply(A,multiply(inverse(B),A)))),A)))) = multiply(inverse(A),multiply(least_upper_bound(B,A),greatest_lower_bound(identity,multiply(inverse(A),B)))),
    inference(paramod,[status(thm)],[c_89,c_11437]) ).

cnf(c_11439,plain,
    multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(inverse(greatest_lower_bound(B,multiply(A,multiply(inverse(B),A)))),A))) = multiply(inverse(A),multiply(least_upper_bound(B,A),greatest_lower_bound(identity,multiply(inverse(A),B)))),
    inference(paramod,[status(thm)],[c_1,c_11438]) ).

cnf(c_11440,plain,
    multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(inverse(greatest_lower_bound(B,multiply(A,multiply(inverse(B),A)))),A))) = multiply(inverse(A),multiply(multiply(B,multiply(greatest_lower_bound(identity,multiply(inverse(B),A)),multiply(inverse(greatest_lower_bound(A,multiply(B,multiply(inverse(A),B)))),B))),greatest_lower_bound(identity,multiply(inverse(A),B)))),
    inference(paramod,[status(thm)],[c_10062,c_11439]) ).

cnf(c_11441,plain,
    multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(inverse(greatest_lower_bound(B,multiply(A,multiply(inverse(B),A)))),A))) = multiply(inverse(A),multiply(B,multiply(multiply(greatest_lower_bound(identity,multiply(inverse(B),A)),multiply(inverse(greatest_lower_bound(A,multiply(B,multiply(inverse(A),B)))),B)),greatest_lower_bound(identity,multiply(inverse(A),B))))),
    inference(paramod,[status(thm)],[c_3,c_11440]) ).

cnf(c_11442,plain,
    multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(inverse(greatest_lower_bound(B,multiply(A,multiply(inverse(B),A)))),A))) = multiply(inverse(A),multiply(B,multiply(greatest_lower_bound(identity,multiply(inverse(B),A)),multiply(multiply(inverse(greatest_lower_bound(A,multiply(B,multiply(inverse(A),B)))),B),greatest_lower_bound(identity,multiply(inverse(A),B)))))),
    inference(paramod,[status(thm)],[c_3,c_11441]) ).

cnf(c_11443,plain,
    multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(inverse(greatest_lower_bound(B,multiply(A,multiply(inverse(B),A)))),A))) = multiply(inverse(A),multiply(B,multiply(greatest_lower_bound(identity,multiply(inverse(B),A)),multiply(inverse(greatest_lower_bound(A,multiply(B,multiply(inverse(A),B)))),multiply(B,greatest_lower_bound(identity,multiply(inverse(A),B))))))),
    inference(paramod,[status(thm)],[c_3,c_11442]) ).

cnf(c_11444,plain,
    multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(inverse(greatest_lower_bound(B,multiply(A,multiply(inverse(B),A)))),A))) = multiply(inverse(A),multiply(B,identity)),
    inference(paramod,[status(thm)],[c_10021,c_11443]) ).

cnf(c_10097,plain,
    multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(greatest_lower_bound(identity,multiply(inverse(A),B)),multiply(inverse(greatest_lower_bound(B,multiply(A,multiply(inverse(B),A)))),A))) = multiply(inverse(A),B),
    inference(paramod,[status(thm)],[c_89,c_11444]) ).

cnf(c_10180,plain,
    multiply(a,multiply(greatest_lower_bound(identity,multiply(inverse(a),b)),multiply(inverse(greatest_lower_bound(b,multiply(a,multiply(inverse(b),a)))),a))) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(paramod,[status(thm)],[c_10062,c_26]) ).

cnf(c_11445,plain,
    multiply(a,multiply(multiply(inverse(A),greatest_lower_bound(A,multiply(A,multiply(inverse(a),b)))),multiply(inverse(greatest_lower_bound(b,multiply(a,multiply(inverse(b),a)))),a))) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(paramod,[status(thm)],[c_243,c_10180]) ).

cnf(c_10205,plain,
    multiply(a,multiply(inverse(A),multiply(greatest_lower_bound(A,multiply(A,multiply(inverse(a),b))),multiply(inverse(greatest_lower_bound(b,multiply(a,multiply(inverse(b),a)))),a)))) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(paramod,[status(thm)],[c_3,c_11445]) ).

cnf(c_11446,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(identity,multiply(inverse(a),b))),multiply(greatest_lower_bound(greatest_lower_bound(identity,multiply(inverse(a),b)),multiply(multiply(inverse(a),b),greatest_lower_bound(identity,multiply(inverse(a),b)))),multiply(inverse(greatest_lower_bound(b,multiply(a,multiply(inverse(b),a)))),a)))) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(paramod,[status(thm)],[c_250,c_10205]) ).

cnf(c_11447,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(identity,multiply(inverse(a),b))),multiply(greatest_lower_bound(greatest_lower_bound(identity,multiply(inverse(a),b)),multiply(inverse(a),multiply(b,greatest_lower_bound(identity,multiply(inverse(a),b))))),multiply(inverse(greatest_lower_bound(b,multiply(a,multiply(inverse(b),a)))),a)))) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(paramod,[status(thm)],[c_3,c_11446]) ).

cnf(c_11448,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(identity,multiply(inverse(a),b))),multiply(greatest_lower_bound(identity,greatest_lower_bound(multiply(inverse(a),b),multiply(inverse(a),multiply(b,greatest_lower_bound(identity,multiply(inverse(a),b)))))),multiply(inverse(greatest_lower_bound(b,multiply(a,multiply(inverse(b),a)))),a)))) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(paramod,[status(thm)],[c_7,c_11447]) ).

cnf(c_11449,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(identity,multiply(inverse(a),b))),multiply(greatest_lower_bound(identity,multiply(inverse(a),greatest_lower_bound(b,multiply(inverse(inverse(a)),multiply(inverse(a),multiply(b,greatest_lower_bound(identity,multiply(inverse(a),b)))))))),multiply(inverse(greatest_lower_bound(b,multiply(a,multiply(inverse(b),a)))),a)))) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(paramod,[status(thm)],[c_483,c_11448]) ).

cnf(c_11450,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(identity,multiply(inverse(a),b))),multiply(greatest_lower_bound(identity,multiply(inverse(a),greatest_lower_bound(b,multiply(a,multiply(inverse(a),multiply(b,greatest_lower_bound(identity,multiply(inverse(a),b)))))))),multiply(inverse(greatest_lower_bound(b,multiply(a,multiply(inverse(b),a)))),a)))) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(paramod,[status(thm)],[c_23,c_11449]) ).

cnf(c_11451,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(identity,multiply(inverse(a),b))),multiply(greatest_lower_bound(identity,multiply(inverse(a),greatest_lower_bound(b,multiply(b,greatest_lower_bound(identity,multiply(inverse(a),b)))))),multiply(inverse(greatest_lower_bound(b,multiply(a,multiply(inverse(b),a)))),a)))) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(paramod,[status(thm)],[c_68,c_11450]) ).

cnf(c_11452,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(identity,multiply(inverse(a),b))),multiply(greatest_lower_bound(identity,multiply(inverse(a),multiply(b,greatest_lower_bound(identity,greatest_lower_bound(identity,multiply(inverse(a),b)))))),multiply(inverse(greatest_lower_bound(b,multiply(a,multiply(inverse(b),a)))),a)))) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(paramod,[status(thm)],[c_92,c_11451]) ).

cnf(c_11453,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(identity,multiply(inverse(a),b))),multiply(greatest_lower_bound(identity,multiply(inverse(a),multiply(b,greatest_lower_bound(identity,multiply(inverse(a),b))))),multiply(inverse(greatest_lower_bound(b,multiply(a,multiply(inverse(b),a)))),a)))) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(paramod,[status(thm)],[c_35,c_11452]) ).

cnf(c_11454,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(identity,multiply(inverse(a),b))),multiply(multiply(greatest_lower_bound(identity,multiply(inverse(a),b)),greatest_lower_bound(identity,multiply(inverse(a),b))),multiply(inverse(greatest_lower_bound(b,multiply(a,multiply(inverse(b),a)))),a)))) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(paramod,[status(thm)],[c_4985,c_11453]) ).

cnf(c_11455,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(identity,multiply(inverse(a),b))),multiply(greatest_lower_bound(identity,multiply(inverse(a),b)),multiply(greatest_lower_bound(identity,multiply(inverse(a),b)),multiply(inverse(greatest_lower_bound(b,multiply(a,multiply(inverse(b),a)))),a))))) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(paramod,[status(thm)],[c_3,c_11454]) ).

cnf(c_11456,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(identity,multiply(inverse(a),b))),multiply(inverse(a),b))) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(paramod,[status(thm)],[c_10097,c_11455]) ).

cnf(c_11457,plain,
    multiply(a,multiply(multiply(inverse(a),b),inverse(greatest_lower_bound(identity,multiply(inverse(a),b))))) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(paramod,[status(thm)],[c_341,c_11456]) ).

cnf(c_11458,plain,
    multiply(a,multiply(inverse(a),multiply(b,inverse(greatest_lower_bound(identity,multiply(inverse(a),b)))))) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(paramod,[status(thm)],[c_3,c_11457]) ).

cnf(c_11459,plain,
    multiply(b,inverse(greatest_lower_bound(identity,multiply(inverse(a),b)))) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(paramod,[status(thm)],[c_68,c_11458]) ).

cnf(c_10210,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)) != multiply(b,inverse(greatest_lower_bound(identity,multiply(inverse(a),b)))),
    inference(copy,[status(thm)],[c_11459]) ).

cnf(c_11460,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)) != multiply(b,inverse(multiply(greatest_lower_bound(inverse(a),inverse(b)),b))),
    inference(paramod,[status(thm)],[c_62,c_10210]) ).

cnf(c_11461,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)) != multiply(b,inverse(multiply(multiply(inverse(a),greatest_lower_bound(identity,multiply(a,inverse(b)))),b))),
    inference(paramod,[status(thm)],[c_244,c_11460]) ).

cnf(c_11462,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)) != multiply(b,inverse(multiply(inverse(a),multiply(greatest_lower_bound(identity,multiply(a,inverse(b))),b)))),
    inference(paramod,[status(thm)],[c_3,c_11461]) ).

cnf(c_11463,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)) != multiply(b,multiply(inverse(multiply(greatest_lower_bound(identity,multiply(a,inverse(b))),b)),inverse(inverse(a)))),
    inference(paramod,[status(thm)],[c_24,c_11462]) ).

cnf(c_11464,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)) != multiply(b,multiply(multiply(inverse(b),inverse(greatest_lower_bound(identity,multiply(a,inverse(b))))),inverse(inverse(a)))),
    inference(paramod,[status(thm)],[c_24,c_11463]) ).

cnf(c_11465,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)) != multiply(b,multiply(multiply(inverse(b),inverse(greatest_lower_bound(identity,multiply(a,inverse(b))))),a)),
    inference(paramod,[status(thm)],[c_23,c_11464]) ).

cnf(c_11466,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)) != multiply(b,multiply(inverse(b),multiply(inverse(greatest_lower_bound(identity,multiply(a,inverse(b)))),a))),
    inference(paramod,[status(thm)],[c_3,c_11465]) ).

cnf(c_10568,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)) != multiply(inverse(greatest_lower_bound(identity,multiply(a,inverse(b)))),a),
    inference(paramod,[status(thm)],[c_68,c_11466]) ).

cnf(c_11467,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)) != multiply(inverse(multiply(inverse(A),greatest_lower_bound(A,multiply(A,multiply(a,inverse(b)))))),a),
    inference(paramod,[status(thm)],[c_243,c_10568]) ).

cnf(c_11468,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)) != multiply(multiply(inverse(greatest_lower_bound(A,multiply(A,multiply(a,inverse(b))))),inverse(inverse(A))),a),
    inference(paramod,[status(thm)],[c_24,c_11467]) ).

cnf(c_11469,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)) != multiply(multiply(inverse(greatest_lower_bound(A,multiply(A,multiply(a,inverse(b))))),A),a),
    inference(paramod,[status(thm)],[c_23,c_11468]) ).

cnf(c_11470,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)) != multiply(inverse(greatest_lower_bound(A,multiply(A,multiply(a,inverse(b))))),multiply(A,a)),
    inference(paramod,[status(thm)],[c_3,c_11469]) ).

cnf(c_10572,plain,
    multiply(inverse(greatest_lower_bound(A,multiply(A,multiply(a,inverse(b))))),multiply(A,a)) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(copy,[status(thm)],[c_11470]) ).

cnf(c_11471,plain,
    multiply(inverse(greatest_lower_bound(inverse(multiply(a,inverse(b))),identity)),multiply(inverse(multiply(a,inverse(b))),a)) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(paramod,[status(thm)],[c_2,c_10572]) ).

cnf(c_11472,plain,
    multiply(inverse(greatest_lower_bound(multiply(inverse(inverse(b)),inverse(a)),identity)),multiply(inverse(multiply(a,inverse(b))),a)) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(paramod,[status(thm)],[c_24,c_11471]) ).

cnf(c_11473,plain,
    multiply(inverse(greatest_lower_bound(multiply(b,inverse(a)),identity)),multiply(inverse(multiply(a,inverse(b))),a)) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(paramod,[status(thm)],[c_23,c_11472]) ).

cnf(c_11474,plain,
    multiply(inverse(greatest_lower_bound(identity,multiply(b,inverse(a)))),multiply(inverse(multiply(a,inverse(b))),a)) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(paramod,[status(thm)],[c_4,c_11473]) ).

cnf(c_11475,plain,
    multiply(inverse(greatest_lower_bound(identity,multiply(b,inverse(a)))),multiply(multiply(inverse(inverse(b)),inverse(a)),a)) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(paramod,[status(thm)],[c_24,c_11474]) ).

cnf(c_11476,plain,
    multiply(inverse(greatest_lower_bound(identity,multiply(b,inverse(a)))),multiply(multiply(b,inverse(a)),a)) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(paramod,[status(thm)],[c_23,c_11475]) ).

cnf(c_11477,plain,
    multiply(inverse(greatest_lower_bound(identity,multiply(b,inverse(a)))),multiply(b,multiply(inverse(a),a))) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(paramod,[status(thm)],[c_3,c_11476]) ).

cnf(c_11478,plain,
    multiply(inverse(greatest_lower_bound(identity,multiply(b,inverse(a)))),multiply(b,identity)) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(paramod,[status(thm)],[c_2,c_11477]) ).

cnf(c_11479,plain,
    multiply(inverse(greatest_lower_bound(identity,multiply(b,inverse(a)))),b) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(paramod,[status(thm)],[c_89,c_11478]) ).

cnf(c_11080,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)) != multiply(inverse(greatest_lower_bound(identity,multiply(b,inverse(a)))),b),
    inference(copy,[status(thm)],[c_11479]) ).

cnf(c_11480,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)) != multiply(inverse(multiply(greatest_lower_bound(b,inverse(inverse(a))),inverse(a))),b),
    inference(paramod,[status(thm)],[c_62,c_11080]) ).

cnf(c_11481,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)) != multiply(inverse(multiply(greatest_lower_bound(b,a),inverse(a))),b),
    inference(paramod,[status(thm)],[c_23,c_11480]) ).

cnf(c_11482,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)) != multiply(inverse(multiply(greatest_lower_bound(a,b),inverse(a))),b),
    inference(paramod,[status(thm)],[c_4,c_11481]) ).

cnf(c_11483,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)) != multiply(multiply(inverse(inverse(a)),inverse(greatest_lower_bound(a,b))),b),
    inference(paramod,[status(thm)],[c_24,c_11482]) ).

cnf(c_11484,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)) != multiply(multiply(a,inverse(greatest_lower_bound(a,b))),b),
    inference(paramod,[status(thm)],[c_23,c_11483]) ).

cnf(c_11485,plain,
    multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)) != multiply(a,multiply(inverse(greatest_lower_bound(a,b)),b)),
    inference(paramod,[status(thm)],[c_3,c_11484]) ).

cnf(c_11088,plain,
    $false,
    inference(copy,[status(thm)],[c_11485]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05  % Problem  : GRP180-2 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.07  % Command  : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.45  % Computer : n007.cluster.edu
% 0.18/0.45  % Model    : x86_64 x86_64
% 0.18/0.45  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45  % Memory   : 8046.5625MB
% 0.18/0.45  % OS       : Linux 6.8.0-71-generic
% 0.18/0.45  % CPULimit : 300
% 0.18/0.45  % WCLimit  : 300
% 0.18/0.45  % DateTime : Fri Sep 25 14:32:23 UTC 2026
% 0.18/0.45  % CPUTime  : 
% 0.18/0.45  % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/0.45  % Process 1218483 was started by sandbox on n007,
% 0.18/0.45  % Fri Sep 25 14:32:23 2026
% 0.18/0.45  % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.18/0.46  
% 0.18/0.46  % From the command line: assign(max_seconds, 300).
% 224.27/29.96  
% 224.27/29.96  % SZS status Unsatisfiable for theBenchmark
% 224.27/29.96  
% 224.27/29.96  % Proof 1 at 4.35 (+ 0.81) seconds.
% 224.27/29.96  % Length of proof is 184.
% 224.27/29.96  % Level of proof is 26.
% 224.27/29.96  % Maximum clause weight is 96.000.
% 224.27/29.96  % Given clauses 281.
% 224.27/29.96  
% 224.27/29.96  % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------