%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP179-1 : 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 : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:28:14 AM UTC 2026
% Result : Unsatisfiable 102.60s 14.42s
% Output : CNFRefutation 102.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 73
% Number of leaves : 16
% Syntax : Number of formulae : 331 ( 331 unt; 0 def)
% Number of atoms : 331 ( 330 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 27 ( 27 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 13 ( 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 : 544 ( 10 sgn 33 !; 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(prove_p10,axiom,
inverse(least_upper_bound(a,b)) != greatest_lower_bound(inverse(a),inverse(b)),
file('theBenchmark.p',prove_p10) ).
cnf(c_22,plain,
inverse(least_upper_bound(a,b)) != greatest_lower_bound(inverse(a),inverse(b)),
inference(clausify,[status(thm)],[prove_p10]) ).
cnf(c_11046,plain,
multiply(identity,A) = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_11047,plain,
A = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_1,c_11046]) ).
cnf(c_23,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(copy,[status(thm)],[c_11047]) ).
cnf(c_11048,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_28,plain,
least_upper_bound(A,least_upper_bound(A,B)) = least_upper_bound(A,B),
inference(copy,[status(thm)],[c_11048]) ).
cnf(c_11049,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_30,plain,
least_upper_bound(A,least_upper_bound(B,A)) = least_upper_bound(B,A),
inference(paramod,[status(thm)],[c_5,c_11049]) ).
cnf(c_11050,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_31,plain,
greatest_lower_bound(A,greatest_lower_bound(A,B)) = greatest_lower_bound(A,B),
inference(copy,[status(thm)],[c_11050]) ).
cnf(c_34,plain,
least_upper_bound(A,greatest_lower_bound(B,A)) = A,
inference(paramod,[status(thm)],[c_4,c_12]) ).
cnf(c_11051,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_36,plain,
least_upper_bound(A,least_upper_bound(greatest_lower_bound(A,B),C)) = least_upper_bound(A,C),
inference(copy,[status(thm)],[c_11051]) ).
cnf(c_38,plain,
greatest_lower_bound(A,least_upper_bound(B,A)) = A,
inference(paramod,[status(thm)],[c_5,c_13]) ).
cnf(c_11052,plain,
greatest_lower_bound(A,B) = greatest_lower_bound(A,greatest_lower_bound(least_upper_bound(A,C),B)),
inference(paramod,[status(thm)],[c_13,c_7]) ).
cnf(c_39,plain,
greatest_lower_bound(A,greatest_lower_bound(least_upper_bound(A,B),C)) = greatest_lower_bound(A,C),
inference(copy,[status(thm)],[c_11052]) ).
cnf(c_42,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_45,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_48,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_11053,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_49,plain,
least_upper_bound(A,multiply(B,A)) = multiply(least_upper_bound(B,identity),A),
inference(paramod,[status(thm)],[c_5,c_11053]) ).
cnf(c_11054,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_51,plain,
least_upper_bound(identity,multiply(A,B)) = multiply(least_upper_bound(A,inverse(B)),B),
inference(paramod,[status(thm)],[c_5,c_11054]) ).
cnf(c_55,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_11055,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_56,plain,
greatest_lower_bound(A,multiply(B,A)) = multiply(greatest_lower_bound(B,identity),A),
inference(paramod,[status(thm)],[c_4,c_11055]) ).
cnf(c_11056,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_58,plain,
greatest_lower_bound(identity,multiply(A,B)) = multiply(greatest_lower_bound(A,inverse(B)),B),
inference(paramod,[status(thm)],[c_4,c_11056]) ).
cnf(c_69,plain,
multiply(inverse(inverse(A)),identity) = A,
inference(paramod,[status(thm)],[c_2,c_23]) ).
cnf(c_70,plain,
multiply(inverse(multiply(A,B)),multiply(A,multiply(B,C))) = C,
inference(paramod,[status(thm)],[c_3,c_23]) ).
cnf(c_79,plain,
multiply(inverse(inverse(A)),B) = multiply(A,B),
inference(paramod,[status(thm)],[c_23,c_23]) ).
cnf(c_80,plain,
multiply(A,identity) = A,
inference(paramod,[status(thm)],[c_79,c_69]) ).
cnf(c_81,plain,
inverse(identity) = identity,
inference(paramod,[status(thm)],[c_80,c_2]) ).
cnf(c_82,plain,
least_upper_bound(A,multiply(A,B)) = multiply(A,least_upper_bound(identity,B)),
inference(paramod,[status(thm)],[c_80,c_15]) ).
cnf(c_11057,plain,
least_upper_bound(multiply(A,B),A) = multiply(A,least_upper_bound(B,identity)),
inference(paramod,[status(thm)],[c_80,c_15]) ).
cnf(c_83,plain,
least_upper_bound(A,multiply(A,B)) = multiply(A,least_upper_bound(B,identity)),
inference(paramod,[status(thm)],[c_5,c_11057]) ).
cnf(c_84,plain,
greatest_lower_bound(A,multiply(A,B)) = multiply(A,greatest_lower_bound(identity,B)),
inference(paramod,[status(thm)],[c_80,c_17]) ).
cnf(c_11058,plain,
greatest_lower_bound(multiply(A,B),A) = multiply(A,greatest_lower_bound(B,identity)),
inference(paramod,[status(thm)],[c_80,c_17]) ).
cnf(c_85,plain,
greatest_lower_bound(A,multiply(A,B)) = multiply(A,greatest_lower_bound(B,identity)),
inference(paramod,[status(thm)],[c_4,c_11058]) ).
cnf(c_111,plain,
multiply(inverse(least_upper_bound(identity,A)),least_upper_bound(B,multiply(A,B))) = B,
inference(paramod,[status(thm)],[c_48,c_23]) ).
cnf(c_113,plain,
least_upper_bound(A,multiply(least_upper_bound(identity,B),A)) = least_upper_bound(A,multiply(B,A)),
inference(paramod,[status(thm)],[c_48,c_28]) ).
cnf(c_144,plain,
greatest_lower_bound(A,multiply(greatest_lower_bound(identity,B),A)) = greatest_lower_bound(A,multiply(B,A)),
inference(paramod,[status(thm)],[c_55,c_31]) ).
cnf(c_156,plain,
multiply(inverse(greatest_lower_bound(A,identity)),greatest_lower_bound(B,multiply(A,B))) = B,
inference(paramod,[status(thm)],[c_56,c_23]) ).
cnf(c_11059,plain,
least_upper_bound(inverse(A),identity) = multiply(inverse(A),least_upper_bound(identity,A)),
inference(paramod,[status(thm)],[c_2,c_82]) ).
cnf(c_157,plain,
least_upper_bound(identity,inverse(A)) = multiply(inverse(A),least_upper_bound(identity,A)),
inference(paramod,[status(thm)],[c_5,c_11059]) ).
cnf(c_174,plain,
least_upper_bound(inverse(A),B) = multiply(inverse(A),least_upper_bound(identity,multiply(A,B))),
inference(paramod,[status(thm)],[c_23,c_82]) ).
cnf(c_175,plain,
least_upper_bound(A,multiply(A,least_upper_bound(identity,B))) = least_upper_bound(A,multiply(A,B)),
inference(paramod,[status(thm)],[c_82,c_28]) ).
cnf(c_11060,plain,
multiply(A,least_upper_bound(identity,A)) = multiply(least_upper_bound(identity,A),A),
inference(paramod,[status(thm)],[c_82,c_48]) ).
cnf(c_177,plain,
multiply(least_upper_bound(identity,A),A) = multiply(A,least_upper_bound(identity,A)),
inference(copy,[status(thm)],[c_11060]) ).
cnf(c_11061,plain,
multiply(A,least_upper_bound(A,identity)) = multiply(least_upper_bound(A,identity),A),
inference(paramod,[status(thm)],[c_83,c_49]) ).
cnf(c_203,plain,
multiply(least_upper_bound(A,identity),A) = multiply(A,least_upper_bound(A,identity)),
inference(copy,[status(thm)],[c_11061]) ).
cnf(c_11062,plain,
greatest_lower_bound(inverse(A),identity) = multiply(inverse(A),greatest_lower_bound(identity,A)),
inference(paramod,[status(thm)],[c_2,c_84]) ).
cnf(c_205,plain,
greatest_lower_bound(identity,inverse(A)) = multiply(inverse(A),greatest_lower_bound(identity,A)),
inference(paramod,[status(thm)],[c_4,c_11062]) ).
cnf(c_11063,plain,
multiply(inverse(A),greatest_lower_bound(A,multiply(A,B))) = greatest_lower_bound(identity,B),
inference(paramod,[status(thm)],[c_84,c_23]) ).
cnf(c_218,plain,
greatest_lower_bound(identity,A) = multiply(inverse(B),greatest_lower_bound(B,multiply(B,A))),
inference(copy,[status(thm)],[c_11063]) ).
cnf(c_219,plain,
greatest_lower_bound(inverse(A),B) = multiply(inverse(A),greatest_lower_bound(identity,multiply(A,B))),
inference(paramod,[status(thm)],[c_23,c_84]) ).
cnf(c_11064,plain,
multiply(A,greatest_lower_bound(identity,A)) = multiply(greatest_lower_bound(identity,A),A),
inference(paramod,[status(thm)],[c_84,c_55]) ).
cnf(c_225,plain,
multiply(greatest_lower_bound(identity,A),A) = multiply(A,greatest_lower_bound(identity,A)),
inference(copy,[status(thm)],[c_11064]) ).
cnf(c_233,plain,
inverse(least_upper_bound(a,b)) != multiply(inverse(a),greatest_lower_bound(identity,multiply(a,inverse(b)))),
inference(paramod,[status(thm)],[c_219,c_22]) ).
cnf(c_11065,plain,
greatest_lower_bound(inverse(greatest_lower_bound(A,identity)),multiply(inverse(greatest_lower_bound(A,identity)),A)) = identity,
inference(paramod,[status(thm)],[c_85,c_2]) ).
cnf(c_234,plain,
multiply(inverse(greatest_lower_bound(A,identity)),greatest_lower_bound(identity,A)) = identity,
inference(paramod,[status(thm)],[c_84,c_11065]) ).
cnf(c_258,plain,
multiply(inverse(least_upper_bound(identity,A)),multiply(A,least_upper_bound(identity,A))) = A,
inference(paramod,[status(thm)],[c_177,c_23]) ).
cnf(c_11066,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_177,c_84]) ).
cnf(c_11067,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_55,c_11066]) ).
cnf(c_259,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_11067]) ).
cnf(c_11068,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(A,identity)),
inference(paramod,[status(thm)],[c_177,c_85]) ).
cnf(c_11069,plain,
multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A)) = multiply(least_upper_bound(identity,A),greatest_lower_bound(A,identity)),
inference(paramod,[status(thm)],[c_55,c_11068]) ).
cnf(c_260,plain,
multiply(least_upper_bound(identity,A),greatest_lower_bound(A,identity)) = multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A)),
inference(copy,[status(thm)],[c_11069]) ).
cnf(c_11070,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_203,c_84]) ).
cnf(c_11071,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_55,c_11070]) ).
cnf(c_269,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_11071]) ).
cnf(c_11072,plain,
multiply(multiply(A,greatest_lower_bound(identity,A)),B) = multiply(greatest_lower_bound(identity,A),multiply(A,B)),
inference(paramod,[status(thm)],[c_225,c_3]) ).
cnf(c_11073,plain,
multiply(A,multiply(greatest_lower_bound(identity,A),B)) = multiply(greatest_lower_bound(identity,A),multiply(A,B)),
inference(paramod,[status(thm)],[c_3,c_11072]) ).
cnf(c_275,plain,
multiply(greatest_lower_bound(identity,A),multiply(A,B)) = multiply(A,multiply(greatest_lower_bound(identity,A),B)),
inference(copy,[status(thm)],[c_11073]) ).
cnf(c_11074,plain,
multiply(identity,A) = multiply(inverse(greatest_lower_bound(B,identity)),multiply(greatest_lower_bound(identity,B),A)),
inference(paramod,[status(thm)],[c_234,c_3]) ).
cnf(c_11075,plain,
A = multiply(inverse(greatest_lower_bound(B,identity)),multiply(greatest_lower_bound(identity,B),A)),
inference(paramod,[status(thm)],[c_1,c_11074]) ).
cnf(c_377,plain,
multiply(inverse(greatest_lower_bound(A,identity)),multiply(greatest_lower_bound(identity,A),B)) = B,
inference(copy,[status(thm)],[c_11075]) ).
cnf(c_455,plain,
multiply(A,inverse(A)) = identity,
inference(paramod,[status(thm)],[c_79,c_2]) ).
cnf(c_460,plain,
multiply(A,multiply(inverse(A),B)) = B,
inference(paramod,[status(thm)],[c_79,c_23]) ).
cnf(c_11076,plain,
multiply(A,identity) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_79,c_80]) ).
cnf(c_11077,plain,
A = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_80,c_11076]) ).
cnf(c_461,plain,
inverse(inverse(A)) = A,
inference(copy,[status(thm)],[c_11077]) ).
cnf(c_11078,plain,
least_upper_bound(multiply(A,B),identity) = multiply(A,least_upper_bound(B,inverse(A))),
inference(paramod,[status(thm)],[c_455,c_15]) ).
cnf(c_463,plain,
least_upper_bound(identity,multiply(A,B)) = multiply(A,least_upper_bound(B,inverse(A))),
inference(paramod,[status(thm)],[c_5,c_11078]) ).
cnf(c_11079,plain,
greatest_lower_bound(multiply(A,B),identity) = multiply(A,greatest_lower_bound(B,inverse(A))),
inference(paramod,[status(thm)],[c_455,c_17]) ).
cnf(c_464,plain,
greatest_lower_bound(identity,multiply(A,B)) = multiply(A,greatest_lower_bound(B,inverse(A))),
inference(paramod,[status(thm)],[c_4,c_11079]) ).
cnf(c_465,plain,
least_upper_bound(identity,multiply(A,inverse(B))) = multiply(least_upper_bound(B,A),inverse(B)),
inference(paramod,[status(thm)],[c_455,c_19]) ).
cnf(c_467,plain,
greatest_lower_bound(identity,multiply(A,inverse(B))) = multiply(greatest_lower_bound(B,A),inverse(B)),
inference(paramod,[status(thm)],[c_455,c_21]) ).
cnf(c_11080,plain,
least_upper_bound(inverse(A),identity) = multiply(least_upper_bound(identity,A),inverse(A)),
inference(paramod,[status(thm)],[c_455,c_48]) ).
cnf(c_11081,plain,
least_upper_bound(identity,inverse(A)) = multiply(least_upper_bound(identity,A),inverse(A)),
inference(paramod,[status(thm)],[c_5,c_11080]) ).
cnf(c_11082,plain,
multiply(inverse(A),least_upper_bound(identity,A)) = multiply(least_upper_bound(identity,A),inverse(A)),
inference(paramod,[status(thm)],[c_157,c_11081]) ).
cnf(c_469,plain,
multiply(least_upper_bound(identity,A),inverse(A)) = multiply(inverse(A),least_upper_bound(identity,A)),
inference(copy,[status(thm)],[c_11082]) ).
cnf(c_11083,plain,
greatest_lower_bound(inverse(A),identity) = multiply(greatest_lower_bound(identity,A),inverse(A)),
inference(paramod,[status(thm)],[c_455,c_55]) ).
cnf(c_11084,plain,
greatest_lower_bound(identity,inverse(A)) = multiply(greatest_lower_bound(identity,A),inverse(A)),
inference(paramod,[status(thm)],[c_4,c_11083]) ).
cnf(c_11085,plain,
multiply(inverse(A),greatest_lower_bound(identity,A)) = multiply(greatest_lower_bound(identity,A),inverse(A)),
inference(paramod,[status(thm)],[c_205,c_11084]) ).
cnf(c_472,plain,
multiply(greatest_lower_bound(identity,A),inverse(A)) = multiply(inverse(A),greatest_lower_bound(identity,A)),
inference(copy,[status(thm)],[c_11085]) ).
cnf(c_11086,plain,
greatest_lower_bound(inverse(A),identity) = multiply(greatest_lower_bound(A,identity),inverse(A)),
inference(paramod,[status(thm)],[c_455,c_56]) ).
cnf(c_11087,plain,
greatest_lower_bound(identity,inverse(A)) = multiply(greatest_lower_bound(A,identity),inverse(A)),
inference(paramod,[status(thm)],[c_4,c_11086]) ).
cnf(c_11088,plain,
multiply(inverse(A),greatest_lower_bound(identity,A)) = multiply(greatest_lower_bound(A,identity),inverse(A)),
inference(paramod,[status(thm)],[c_205,c_11087]) ).
cnf(c_473,plain,
multiply(greatest_lower_bound(A,identity),inverse(A)) = multiply(inverse(A),greatest_lower_bound(identity,A)),
inference(copy,[status(thm)],[c_11088]) ).
cnf(c_11089,plain,
multiply(multiply(inverse(A),least_upper_bound(identity,A)),B) = multiply(least_upper_bound(identity,A),multiply(inverse(A),B)),
inference(paramod,[status(thm)],[c_469,c_3]) ).
cnf(c_11090,plain,
multiply(inverse(A),multiply(least_upper_bound(identity,A),B)) = multiply(least_upper_bound(identity,A),multiply(inverse(A),B)),
inference(paramod,[status(thm)],[c_3,c_11089]) ).
cnf(c_475,plain,
multiply(least_upper_bound(identity,A),multiply(inverse(A),B)) = multiply(inverse(A),multiply(least_upper_bound(identity,A),B)),
inference(copy,[status(thm)],[c_11090]) ).
cnf(c_11091,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_472,c_3]) ).
cnf(c_11092,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_11091]) ).
cnf(c_503,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_11092]) ).
cnf(c_516,plain,
multiply(greatest_lower_bound(A,identity),inverse(A)) = multiply(inverse(A),greatest_lower_bound(A,identity)),
inference(paramod,[status(thm)],[c_4,c_473]) ).
cnf(c_11093,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_516,c_3]) ).
cnf(c_11094,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_11093]) ).
cnf(c_542,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_11094]) ).
cnf(c_555,plain,
least_upper_bound(multiply(A,B),C) = multiply(A,least_upper_bound(B,multiply(inverse(A),C))),
inference(paramod,[status(thm)],[c_460,c_15]) ).
cnf(c_556,plain,
greatest_lower_bound(multiply(A,B),C) = multiply(A,greatest_lower_bound(B,multiply(inverse(A),C))),
inference(paramod,[status(thm)],[c_460,c_17]) ).
cnf(c_804,plain,
multiply(inverse(least_upper_bound(identity,A)),multiply(A,least_upper_bound(A,identity))) = A,
inference(paramod,[status(thm)],[c_83,c_111]) ).
cnf(c_853,plain,
multiply(inverse(greatest_lower_bound(A,identity)),multiply(A,greatest_lower_bound(identity,A))) = A,
inference(paramod,[status(thm)],[c_84,c_156]) ).
cnf(c_11095,plain,
greatest_lower_bound(identity,inverse(A)) = multiply(inverse(least_upper_bound(identity,A)),greatest_lower_bound(least_upper_bound(identity,A),multiply(inverse(A),least_upper_bound(identity,A)))),
inference(paramod,[status(thm)],[c_469,c_218]) ).
cnf(c_11096,plain,
multiply(inverse(A),greatest_lower_bound(identity,A)) = multiply(inverse(least_upper_bound(identity,A)),greatest_lower_bound(least_upper_bound(identity,A),multiply(inverse(A),least_upper_bound(identity,A)))),
inference(paramod,[status(thm)],[c_205,c_11095]) ).
cnf(c_11097,plain,
multiply(inverse(A),greatest_lower_bound(identity,A)) = multiply(inverse(least_upper_bound(identity,A)),multiply(greatest_lower_bound(identity,inverse(A)),least_upper_bound(identity,A))),
inference(paramod,[status(thm)],[c_55,c_11096]) ).
cnf(c_11098,plain,
multiply(inverse(A),greatest_lower_bound(identity,A)) = multiply(inverse(least_upper_bound(identity,A)),multiply(multiply(inverse(A),greatest_lower_bound(identity,A)),least_upper_bound(identity,A))),
inference(paramod,[status(thm)],[c_205,c_11097]) ).
cnf(c_11099,plain,
multiply(inverse(A),greatest_lower_bound(identity,A)) = multiply(inverse(least_upper_bound(identity,A)),multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A)))),
inference(paramod,[status(thm)],[c_3,c_11098]) ).
cnf(c_950,plain,
multiply(inverse(least_upper_bound(identity,A)),multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A)))) = multiply(inverse(A),greatest_lower_bound(identity,A)),
inference(copy,[status(thm)],[c_11099]) ).
cnf(c_11100,plain,
multiply(A,least_upper_bound(B,inverse(A))) = multiply(least_upper_bound(A,inverse(B)),B),
inference(paramod,[status(thm)],[c_463,c_51]) ).
cnf(c_1038,plain,
multiply(least_upper_bound(A,inverse(B)),B) = multiply(A,least_upper_bound(B,inverse(A))),
inference(copy,[status(thm)],[c_11100]) ).
cnf(c_11101,plain,
multiply(inverse(A),greatest_lower_bound(identity,multiply(A,B))) = greatest_lower_bound(B,inverse(A)),
inference(paramod,[status(thm)],[c_464,c_23]) ).
cnf(c_1105,plain,
greatest_lower_bound(A,inverse(B)) = multiply(inverse(B),greatest_lower_bound(identity,multiply(B,A))),
inference(copy,[status(thm)],[c_11101]) ).
cnf(c_11102,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_36,c_38]) ).
cnf(c_1165,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_11102]) ).
cnf(c_1984,plain,
greatest_lower_bound(identity,multiply(inverse(A),least_upper_bound(A,B))) = identity,
inference(paramod,[status(thm)],[c_42,c_13]) ).
cnf(c_2183,plain,
greatest_lower_bound(identity,multiply(inverse(A),least_upper_bound(B,A))) = identity,
inference(paramod,[status(thm)],[c_5,c_1984]) ).
cnf(c_11103,plain,
least_upper_bound(multiply(inverse(A),B),multiply(least_upper_bound(identity,A),multiply(inverse(A),B))) = least_upper_bound(multiply(inverse(A),B),B),
inference(paramod,[status(thm)],[c_460,c_113]) ).
cnf(c_11104,plain,
least_upper_bound(multiply(inverse(A),B),multiply(inverse(A),multiply(least_upper_bound(identity,A),B))) = least_upper_bound(multiply(inverse(A),B),B),
inference(paramod,[status(thm)],[c_475,c_11103]) ).
cnf(c_11105,plain,
multiply(inverse(A),least_upper_bound(B,multiply(inverse(inverse(A)),multiply(inverse(A),multiply(least_upper_bound(identity,A),B))))) = least_upper_bound(multiply(inverse(A),B),B),
inference(paramod,[status(thm)],[c_555,c_11104]) ).
cnf(c_11106,plain,
multiply(inverse(A),least_upper_bound(B,multiply(A,multiply(inverse(A),multiply(least_upper_bound(identity,A),B))))) = least_upper_bound(multiply(inverse(A),B),B),
inference(paramod,[status(thm)],[c_461,c_11105]) ).
cnf(c_11107,plain,
multiply(inverse(A),least_upper_bound(B,multiply(least_upper_bound(identity,A),B))) = least_upper_bound(multiply(inverse(A),B),B),
inference(paramod,[status(thm)],[c_460,c_11106]) ).
cnf(c_11108,plain,
multiply(inverse(A),least_upper_bound(B,multiply(A,B))) = least_upper_bound(multiply(inverse(A),B),B),
inference(paramod,[status(thm)],[c_113,c_11107]) ).
cnf(c_11109,plain,
multiply(inverse(A),least_upper_bound(B,multiply(A,B))) = least_upper_bound(B,multiply(inverse(A),B)),
inference(paramod,[status(thm)],[c_5,c_11108]) ).
cnf(c_2586,plain,
least_upper_bound(A,multiply(inverse(B),A)) = multiply(inverse(B),least_upper_bound(A,multiply(B,A))),
inference(copy,[status(thm)],[c_11109]) ).
cnf(c_11110,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_460,c_144]) ).
cnf(c_11111,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_503,c_11110]) ).
cnf(c_11112,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_556,c_11111]) ).
cnf(c_11113,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_461,c_11112]) ).
cnf(c_11114,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_460,c_11113]) ).
cnf(c_11115,plain,
multiply(inverse(A),greatest_lower_bound(B,multiply(A,B))) = greatest_lower_bound(multiply(inverse(A),B),B),
inference(paramod,[status(thm)],[c_144,c_11114]) ).
cnf(c_11116,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_11115]) ).
cnf(c_2625,plain,
greatest_lower_bound(A,multiply(inverse(B),A)) = multiply(inverse(B),greatest_lower_bound(A,multiply(B,A))),
inference(copy,[status(thm)],[c_11116]) ).
cnf(c_11117,plain,
least_upper_bound(greatest_lower_bound(A,identity),multiply(greatest_lower_bound(A,identity),least_upper_bound(identity,inverse(A)))) = least_upper_bound(greatest_lower_bound(A,identity),multiply(inverse(A),greatest_lower_bound(A,identity))),
inference(paramod,[status(thm)],[c_516,c_175]) ).
cnf(c_11118,plain,
least_upper_bound(greatest_lower_bound(A,identity),multiply(greatest_lower_bound(A,identity),multiply(inverse(A),least_upper_bound(identity,A)))) = least_upper_bound(greatest_lower_bound(A,identity),multiply(inverse(A),greatest_lower_bound(A,identity))),
inference(paramod,[status(thm)],[c_157,c_11117]) ).
cnf(c_11119,plain,
least_upper_bound(greatest_lower_bound(A,identity),multiply(inverse(A),multiply(greatest_lower_bound(A,identity),least_upper_bound(identity,A)))) = least_upper_bound(greatest_lower_bound(A,identity),multiply(inverse(A),greatest_lower_bound(A,identity))),
inference(paramod,[status(thm)],[c_542,c_11118]) ).
cnf(c_11120,plain,
least_upper_bound(greatest_lower_bound(A,identity),multiply(inverse(A),multiply(greatest_lower_bound(A,identity),least_upper_bound(identity,A)))) = multiply(least_upper_bound(identity,inverse(A)),greatest_lower_bound(A,identity)),
inference(paramod,[status(thm)],[c_48,c_11119]) ).
cnf(c_11121,plain,
least_upper_bound(greatest_lower_bound(A,identity),multiply(inverse(A),multiply(greatest_lower_bound(A,identity),least_upper_bound(identity,A)))) = multiply(multiply(inverse(A),least_upper_bound(identity,A)),greatest_lower_bound(A,identity)),
inference(paramod,[status(thm)],[c_157,c_11120]) ).
cnf(c_11122,plain,
least_upper_bound(greatest_lower_bound(A,identity),multiply(inverse(A),multiply(greatest_lower_bound(A,identity),least_upper_bound(identity,A)))) = multiply(inverse(A),multiply(least_upper_bound(identity,A),greatest_lower_bound(A,identity))),
inference(paramod,[status(thm)],[c_3,c_11121]) ).
cnf(c_2877,plain,
least_upper_bound(greatest_lower_bound(A,identity),multiply(inverse(A),multiply(greatest_lower_bound(A,identity),least_upper_bound(identity,A)))) = multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A))),
inference(paramod,[status(thm)],[c_260,c_11122]) ).
cnf(c_11123,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_113,c_465]) ).
cnf(c_11124,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_11123]) ).
cnf(c_11125,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_455,c_11124]) ).
cnf(c_11126,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_80,c_11125]) ).
cnf(c_3731,plain,
least_upper_bound(identity,A) = multiply(least_upper_bound(B,multiply(A,B)),inverse(B)),
inference(paramod,[status(thm)],[c_28,c_11126]) ).
cnf(c_11127,plain,
least_upper_bound(identity,least_upper_bound(identity,A)) = multiply(least_upper_bound(greatest_lower_bound(identity,A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A))),inverse(greatest_lower_bound(identity,A))),
inference(paramod,[status(thm)],[c_259,c_3731]) ).
cnf(c_11128,plain,
least_upper_bound(identity,A) = multiply(least_upper_bound(greatest_lower_bound(identity,A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A))),inverse(greatest_lower_bound(identity,A))),
inference(paramod,[status(thm)],[c_28,c_11127]) ).
cnf(c_11129,plain,
least_upper_bound(identity,A) = multiply(multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,least_upper_bound(identity,A))),inverse(greatest_lower_bound(identity,A))),
inference(paramod,[status(thm)],[c_82,c_11128]) ).
cnf(c_11130,plain,
least_upper_bound(identity,A) = multiply(multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A)),inverse(greatest_lower_bound(identity,A))),
inference(paramod,[status(thm)],[c_28,c_11129]) ).
cnf(c_11131,plain,
least_upper_bound(identity,A) = multiply(greatest_lower_bound(identity,A),multiply(least_upper_bound(identity,A),inverse(greatest_lower_bound(identity,A)))),
inference(paramod,[status(thm)],[c_3,c_11130]) ).
cnf(c_3957,plain,
multiply(greatest_lower_bound(identity,A),multiply(least_upper_bound(identity,A),inverse(greatest_lower_bound(identity,A)))) = least_upper_bound(identity,A),
inference(copy,[status(thm)],[c_11131]) ).
cnf(c_11132,plain,
least_upper_bound(identity,least_upper_bound(A,identity)) = multiply(least_upper_bound(greatest_lower_bound(identity,A),multiply(greatest_lower_bound(identity,A),least_upper_bound(A,identity))),inverse(greatest_lower_bound(identity,A))),
inference(paramod,[status(thm)],[c_269,c_3731]) ).
cnf(c_11133,plain,
least_upper_bound(A,identity) = multiply(least_upper_bound(greatest_lower_bound(identity,A),multiply(greatest_lower_bound(identity,A),least_upper_bound(A,identity))),inverse(greatest_lower_bound(identity,A))),
inference(paramod,[status(thm)],[c_30,c_11132]) ).
cnf(c_11134,plain,
least_upper_bound(A,identity) = multiply(multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,least_upper_bound(A,identity))),inverse(greatest_lower_bound(identity,A))),
inference(paramod,[status(thm)],[c_82,c_11133]) ).
cnf(c_11135,plain,
least_upper_bound(A,identity) = multiply(multiply(greatest_lower_bound(identity,A),least_upper_bound(A,identity)),inverse(greatest_lower_bound(identity,A))),
inference(paramod,[status(thm)],[c_30,c_11134]) ).
cnf(c_11136,plain,
least_upper_bound(A,identity) = multiply(greatest_lower_bound(identity,A),multiply(least_upper_bound(A,identity),inverse(greatest_lower_bound(identity,A)))),
inference(paramod,[status(thm)],[c_3,c_11135]) ).
cnf(c_3960,plain,
multiply(greatest_lower_bound(identity,A),multiply(least_upper_bound(A,identity),inverse(greatest_lower_bound(identity,A)))) = least_upper_bound(A,identity),
inference(copy,[status(thm)],[c_11136]) ).
cnf(c_11137,plain,
greatest_lower_bound(identity,multiply(multiply(greatest_lower_bound(identity,A),B),inverse(B))) = multiply(greatest_lower_bound(B,multiply(A,B)),inverse(B)),
inference(paramod,[status(thm)],[c_144,c_467]) ).
cnf(c_11138,plain,
greatest_lower_bound(identity,multiply(greatest_lower_bound(identity,A),multiply(B,inverse(B)))) = multiply(greatest_lower_bound(B,multiply(A,B)),inverse(B)),
inference(paramod,[status(thm)],[c_3,c_11137]) ).
cnf(c_11139,plain,
greatest_lower_bound(identity,multiply(greatest_lower_bound(identity,A),identity)) = multiply(greatest_lower_bound(B,multiply(A,B)),inverse(B)),
inference(paramod,[status(thm)],[c_455,c_11138]) ).
cnf(c_11140,plain,
greatest_lower_bound(identity,greatest_lower_bound(identity,A)) = multiply(greatest_lower_bound(B,multiply(A,B)),inverse(B)),
inference(paramod,[status(thm)],[c_80,c_11139]) ).
cnf(c_4387,plain,
greatest_lower_bound(identity,A) = multiply(greatest_lower_bound(B,multiply(A,B)),inverse(B)),
inference(paramod,[status(thm)],[c_31,c_11140]) ).
cnf(c_11141,plain,
inverse(least_upper_bound(a,b)) != multiply(inverse(a),multiply(greatest_lower_bound(A,multiply(multiply(a,inverse(b)),A)),inverse(A))),
inference(paramod,[status(thm)],[c_4387,c_233]) ).
cnf(c_4417,plain,
inverse(least_upper_bound(a,b)) != multiply(inverse(a),multiply(greatest_lower_bound(A,multiply(a,multiply(inverse(b),A))),inverse(A))),
inference(paramod,[status(thm)],[c_3,c_11141]) ).
cnf(c_11142,plain,
inverse(least_upper_bound(a,b)) != multiply(inverse(a),multiply(multiply(a,greatest_lower_bound(identity,multiply(inverse(b),a))),inverse(a))),
inference(paramod,[status(thm)],[c_84,c_4417]) ).
cnf(c_11143,plain,
inverse(least_upper_bound(a,b)) != multiply(inverse(a),multiply(a,multiply(greatest_lower_bound(identity,multiply(inverse(b),a)),inverse(a)))),
inference(paramod,[status(thm)],[c_3,c_11142]) ).
cnf(c_4643,plain,
inverse(least_upper_bound(a,b)) != multiply(greatest_lower_bound(identity,multiply(inverse(b),a)),inverse(a)),
inference(paramod,[status(thm)],[c_23,c_11143]) ).
cnf(c_11144,plain,
inverse(least_upper_bound(a,b)) != multiply(multiply(inverse(b),greatest_lower_bound(a,inverse(inverse(b)))),inverse(a)),
inference(paramod,[status(thm)],[c_464,c_4643]) ).
cnf(c_11145,plain,
inverse(least_upper_bound(a,b)) != multiply(multiply(inverse(b),greatest_lower_bound(a,b)),inverse(a)),
inference(paramod,[status(thm)],[c_461,c_11144]) ).
cnf(c_4655,plain,
inverse(least_upper_bound(a,b)) != multiply(inverse(b),multiply(greatest_lower_bound(a,b),inverse(a))),
inference(paramod,[status(thm)],[c_3,c_11145]) ).
cnf(c_4657,plain,
inverse(least_upper_bound(a,b)) != multiply(inverse(b),greatest_lower_bound(identity,multiply(b,inverse(a)))),
inference(paramod,[status(thm)],[c_467,c_4655]) ).
cnf(c_11146,plain,
multiply(A,multiply(least_upper_bound(inverse(A),inverse(B)),B)) = least_upper_bound(B,inverse(inverse(A))),
inference(paramod,[status(thm)],[c_1038,c_460]) ).
cnf(c_11147,plain,
multiply(A,multiply(multiply(inverse(A),least_upper_bound(identity,multiply(A,inverse(B)))),B)) = least_upper_bound(B,inverse(inverse(A))),
inference(paramod,[status(thm)],[c_174,c_11146]) ).
cnf(c_11148,plain,
multiply(A,multiply(inverse(A),multiply(least_upper_bound(identity,multiply(A,inverse(B))),B))) = least_upper_bound(B,inverse(inverse(A))),
inference(paramod,[status(thm)],[c_3,c_11147]) ).
cnf(c_11149,plain,
multiply(least_upper_bound(identity,multiply(A,inverse(B))),B) = least_upper_bound(B,inverse(inverse(A))),
inference(paramod,[status(thm)],[c_460,c_11148]) ).
cnf(c_11150,plain,
multiply(least_upper_bound(identity,multiply(A,inverse(B))),B) = least_upper_bound(B,A),
inference(paramod,[status(thm)],[c_461,c_11149]) ).
cnf(c_4687,plain,
least_upper_bound(A,B) = multiply(least_upper_bound(identity,multiply(B,inverse(A))),A),
inference(copy,[status(thm)],[c_11150]) ).
cnf(c_4750,plain,
multiply(inverse(A),greatest_lower_bound(identity,multiply(A,inverse(B)))) = multiply(inverse(B),greatest_lower_bound(identity,multiply(B,inverse(A)))),
inference(paramod,[status(thm)],[c_1105,c_219]) ).
cnf(c_11151,plain,
multiply(A,B) = multiply(inverse(least_upper_bound(identity,A)),multiply(multiply(A,least_upper_bound(identity,A)),B)),
inference(paramod,[status(thm)],[c_258,c_3]) ).
cnf(c_11152,plain,
multiply(A,B) = multiply(inverse(least_upper_bound(identity,A)),multiply(A,multiply(least_upper_bound(identity,A),B))),
inference(paramod,[status(thm)],[c_3,c_11151]) ).
cnf(c_4956,plain,
multiply(inverse(least_upper_bound(identity,A)),multiply(A,multiply(least_upper_bound(identity,A),B))) = multiply(A,B),
inference(copy,[status(thm)],[c_11152]) ).
cnf(c_11153,plain,
multiply(inverse(greatest_lower_bound(inverse(A),identity)),greatest_lower_bound(identity,multiply(identity,A))) = A,
inference(paramod,[status(thm)],[c_58,c_377]) ).
cnf(c_11154,plain,
multiply(inverse(greatest_lower_bound(identity,inverse(A))),greatest_lower_bound(identity,multiply(identity,A))) = A,
inference(paramod,[status(thm)],[c_4,c_11153]) ).
cnf(c_11155,plain,
multiply(inverse(multiply(inverse(A),greatest_lower_bound(identity,A))),greatest_lower_bound(identity,multiply(identity,A))) = A,
inference(paramod,[status(thm)],[c_205,c_11154]) ).
cnf(c_5084,plain,
multiply(inverse(multiply(inverse(A),greatest_lower_bound(identity,A))),greatest_lower_bound(identity,A)) = A,
inference(paramod,[status(thm)],[c_1,c_11155]) ).
cnf(c_11156,plain,
multiply(A,B) = multiply(inverse(least_upper_bound(identity,A)),multiply(multiply(A,least_upper_bound(A,identity)),B)),
inference(paramod,[status(thm)],[c_804,c_3]) ).
cnf(c_11157,plain,
multiply(A,B) = multiply(inverse(least_upper_bound(identity,A)),multiply(A,multiply(least_upper_bound(A,identity),B))),
inference(paramod,[status(thm)],[c_3,c_11156]) ).
cnf(c_5128,plain,
multiply(inverse(least_upper_bound(identity,A)),multiply(A,multiply(least_upper_bound(A,identity),B))) = multiply(A,B),
inference(copy,[status(thm)],[c_11157]) ).
cnf(c_11158,plain,
least_upper_bound(inverse(inverse(greatest_lower_bound(A,identity))),multiply(A,greatest_lower_bound(identity,A))) = multiply(inverse(inverse(greatest_lower_bound(A,identity))),least_upper_bound(identity,A)),
inference(paramod,[status(thm)],[c_853,c_174]) ).
cnf(c_11159,plain,
least_upper_bound(greatest_lower_bound(A,identity),multiply(A,greatest_lower_bound(identity,A))) = multiply(inverse(inverse(greatest_lower_bound(A,identity))),least_upper_bound(identity,A)),
inference(paramod,[status(thm)],[c_461,c_11158]) ).
cnf(c_5198,plain,
least_upper_bound(greatest_lower_bound(A,identity),multiply(A,greatest_lower_bound(identity,A))) = multiply(greatest_lower_bound(A,identity),least_upper_bound(identity,A)),
inference(paramod,[status(thm)],[c_461,c_11159]) ).
cnf(c_11160,plain,
greatest_lower_bound(multiply(A,least_upper_bound(identity,B)),least_upper_bound(greatest_lower_bound(A,C),multiply(A,B))) = least_upper_bound(greatest_lower_bound(A,C),multiply(A,B)),
inference(paramod,[status(thm)],[c_82,c_1165]) ).
cnf(c_7072,plain,
multiply(A,greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(A),least_upper_bound(greatest_lower_bound(A,C),multiply(A,B))))) = least_upper_bound(greatest_lower_bound(A,C),multiply(A,B)),
inference(paramod,[status(thm)],[c_556,c_11160]) ).
cnf(c_11161,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_58,c_1165]) ).
cnf(c_11162,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_555,c_11161]) ).
cnf(c_7091,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_11162]) ).
cnf(c_11163,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_45,c_1165]) ).
cnf(c_11164,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_7091,c_11163]) ).
cnf(c_11165,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_219,c_11164]) ).
cnf(c_11166,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_219,c_11165]) ).
cnf(c_11167,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(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_3,c_11166]) ).
cnf(c_11168,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(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_31,c_11167]) ).
cnf(c_11169,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(multiply(inverse(B),greatest_lower_bound(identity,multiply(B,inverse(C))))),A))))) = multiply(inverse(B),least_upper_bound(greatest_lower_bound(B,C),multiply(inverse(inverse(B)),A))),
inference(paramod,[status(thm)],[c_555,c_11168]) ).
cnf(c_11170,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(multiply(inverse(B),greatest_lower_bound(identity,multiply(B,inverse(C))))),A))))) = multiply(inverse(B),least_upper_bound(greatest_lower_bound(B,C),multiply(B,A))),
inference(paramod,[status(thm)],[c_461,c_11169]) ).
cnf(c_7127,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(multiply(inverse(A),greatest_lower_bound(identity,multiply(A,inverse(B))))),C))))),
inference(copy,[status(thm)],[c_11170]) ).
cnf(c_11171,plain,
multiply(A,greatest_lower_bound(least_upper_bound(identity,B),greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(A),multiply(greatest_lower_bound(identity,multiply(A,inverse(C))),least_upper_bound(C,multiply(inverse(multiply(inverse(A),greatest_lower_bound(identity,multiply(A,inverse(C))))),B))))))) = least_upper_bound(greatest_lower_bound(A,C),multiply(A,B)),
inference(paramod,[status(thm)],[c_7127,c_7072]) ).
cnf(c_11172,plain,
multiply(A,greatest_lower_bound(least_upper_bound(identity,B),multiply(inverse(A),multiply(greatest_lower_bound(identity,multiply(A,inverse(C))),least_upper_bound(C,multiply(inverse(multiply(inverse(A),greatest_lower_bound(identity,multiply(A,inverse(C))))),B)))))) = least_upper_bound(greatest_lower_bound(A,C),multiply(A,B)),
inference(paramod,[status(thm)],[c_31,c_11171]) ).
cnf(c_7243,plain,
least_upper_bound(greatest_lower_bound(A,B),multiply(A,C)) = multiply(A,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(multiply(inverse(A),greatest_lower_bound(identity,multiply(A,inverse(B))))),C)))))),
inference(copy,[status(thm)],[c_11172]) ).
cnf(c_11173,plain,
multiply(A,greatest_lower_bound(least_upper_bound(identity,greatest_lower_bound(identity,A)),multiply(inverse(A),multiply(greatest_lower_bound(identity,multiply(A,inverse(identity))),least_upper_bound(identity,multiply(inverse(multiply(inverse(A),greatest_lower_bound(identity,multiply(A,inverse(identity))))),greatest_lower_bound(identity,A))))))) = multiply(greatest_lower_bound(A,identity),least_upper_bound(identity,A)),
inference(paramod,[status(thm)],[c_7243,c_5198]) ).
cnf(c_11174,plain,
multiply(A,greatest_lower_bound(identity,multiply(inverse(A),multiply(greatest_lower_bound(identity,multiply(A,inverse(identity))),least_upper_bound(identity,multiply(inverse(multiply(inverse(A),greatest_lower_bound(identity,multiply(A,inverse(identity))))),greatest_lower_bound(identity,A))))))) = multiply(greatest_lower_bound(A,identity),least_upper_bound(identity,A)),
inference(paramod,[status(thm)],[c_12,c_11173]) ).
cnf(c_11175,plain,
multiply(A,greatest_lower_bound(identity,multiply(inverse(A),multiply(greatest_lower_bound(identity,multiply(A,identity)),least_upper_bound(identity,multiply(inverse(multiply(inverse(A),greatest_lower_bound(identity,multiply(A,inverse(identity))))),greatest_lower_bound(identity,A))))))) = multiply(greatest_lower_bound(A,identity),least_upper_bound(identity,A)),
inference(paramod,[status(thm)],[c_81,c_11174]) ).
cnf(c_11176,plain,
multiply(A,greatest_lower_bound(identity,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,multiply(inverse(multiply(inverse(A),greatest_lower_bound(identity,multiply(A,inverse(identity))))),greatest_lower_bound(identity,A))))))) = multiply(greatest_lower_bound(A,identity),least_upper_bound(identity,A)),
inference(paramod,[status(thm)],[c_80,c_11175]) ).
cnf(c_11177,plain,
multiply(A,greatest_lower_bound(identity,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,multiply(inverse(multiply(inverse(A),greatest_lower_bound(identity,multiply(A,identity)))),greatest_lower_bound(identity,A))))))) = multiply(greatest_lower_bound(A,identity),least_upper_bound(identity,A)),
inference(paramod,[status(thm)],[c_81,c_11176]) ).
cnf(c_11178,plain,
multiply(A,greatest_lower_bound(identity,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,multiply(inverse(multiply(inverse(A),greatest_lower_bound(identity,A))),greatest_lower_bound(identity,A))))))) = multiply(greatest_lower_bound(A,identity),least_upper_bound(identity,A)),
inference(paramod,[status(thm)],[c_80,c_11177]) ).
cnf(c_7286,plain,
multiply(A,greatest_lower_bound(identity,multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A))))) = multiply(greatest_lower_bound(A,identity),least_upper_bound(identity,A)),
inference(paramod,[status(thm)],[c_5084,c_11178]) ).
cnf(c_11179,plain,
greatest_lower_bound(A,multiply(inverse(B),greatest_lower_bound(least_upper_bound(A,C),multiply(B,least_upper_bound(A,C))))) = greatest_lower_bound(A,multiply(inverse(B),least_upper_bound(A,C))),
inference(paramod,[status(thm)],[c_2625,c_39]) ).
cnf(c_8356,plain,
greatest_lower_bound(A,multiply(inverse(B),multiply(greatest_lower_bound(identity,B),least_upper_bound(A,C)))) = greatest_lower_bound(A,multiply(inverse(B),least_upper_bound(A,C))),
inference(paramod,[status(thm)],[c_55,c_11179]) ).
cnf(c_11180,plain,
multiply(A,greatest_lower_bound(identity,multiply(inverse(A),least_upper_bound(identity,A)))) = multiply(greatest_lower_bound(A,identity),least_upper_bound(identity,A)),
inference(paramod,[status(thm)],[c_8356,c_7286]) ).
cnf(c_11181,plain,
multiply(A,identity) = multiply(greatest_lower_bound(A,identity),least_upper_bound(identity,A)),
inference(paramod,[status(thm)],[c_2183,c_11180]) ).
cnf(c_11182,plain,
A = multiply(greatest_lower_bound(A,identity),least_upper_bound(identity,A)),
inference(paramod,[status(thm)],[c_80,c_11181]) ).
cnf(c_8413,plain,
multiply(greatest_lower_bound(A,identity),least_upper_bound(identity,A)) = A,
inference(copy,[status(thm)],[c_11182]) ).
cnf(c_11183,plain,
least_upper_bound(greatest_lower_bound(A,identity),multiply(inverse(A),A)) = multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A))),
inference(paramod,[status(thm)],[c_8413,c_2877]) ).
cnf(c_11184,plain,
least_upper_bound(greatest_lower_bound(A,identity),identity) = multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A))),
inference(paramod,[status(thm)],[c_2,c_11183]) ).
cnf(c_11185,plain,
least_upper_bound(identity,greatest_lower_bound(A,identity)) = multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A))),
inference(paramod,[status(thm)],[c_5,c_11184]) ).
cnf(c_11186,plain,
identity = multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A))),
inference(paramod,[status(thm)],[c_34,c_11185]) ).
cnf(c_8416,plain,
multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A))) = identity,
inference(copy,[status(thm)],[c_11186]) ).
cnf(c_11187,plain,
multiply(inverse(least_upper_bound(identity,A)),identity) = multiply(inverse(A),greatest_lower_bound(identity,A)),
inference(paramod,[status(thm)],[c_8416,c_950]) ).
cnf(c_8418,plain,
inverse(least_upper_bound(identity,A)) = multiply(inverse(A),greatest_lower_bound(identity,A)),
inference(paramod,[status(thm)],[c_80,c_11187]) ).
cnf(c_11188,plain,
multiply(multiply(inverse(A),greatest_lower_bound(identity,A)),multiply(A,multiply(least_upper_bound(A,identity),B))) = multiply(A,B),
inference(paramod,[status(thm)],[c_8418,c_5128]) ).
cnf(c_11189,plain,
multiply(inverse(A),multiply(greatest_lower_bound(identity,A),multiply(A,multiply(least_upper_bound(A,identity),B)))) = multiply(A,B),
inference(paramod,[status(thm)],[c_3,c_11188]) ).
cnf(c_11190,plain,
multiply(inverse(A),multiply(A,multiply(greatest_lower_bound(identity,A),multiply(least_upper_bound(A,identity),B)))) = multiply(A,B),
inference(paramod,[status(thm)],[c_275,c_11189]) ).
cnf(c_8655,plain,
multiply(greatest_lower_bound(identity,A),multiply(least_upper_bound(A,identity),B)) = multiply(A,B),
inference(paramod,[status(thm)],[c_23,c_11190]) ).
cnf(c_11191,plain,
multiply(multiply(inverse(A),greatest_lower_bound(identity,A)),multiply(A,multiply(least_upper_bound(identity,A),B))) = multiply(A,B),
inference(paramod,[status(thm)],[c_8418,c_4956]) ).
cnf(c_11192,plain,
multiply(inverse(A),multiply(greatest_lower_bound(identity,A),multiply(A,multiply(least_upper_bound(identity,A),B)))) = multiply(A,B),
inference(paramod,[status(thm)],[c_3,c_11191]) ).
cnf(c_11193,plain,
multiply(inverse(A),multiply(A,multiply(greatest_lower_bound(identity,A),multiply(least_upper_bound(identity,A),B)))) = multiply(A,B),
inference(paramod,[status(thm)],[c_275,c_11192]) ).
cnf(c_8686,plain,
multiply(greatest_lower_bound(identity,A),multiply(least_upper_bound(identity,A),B)) = multiply(A,B),
inference(paramod,[status(thm)],[c_23,c_11193]) ).
cnf(c_11194,plain,
multiply(A,inverse(greatest_lower_bound(identity,A))) = least_upper_bound(A,identity),
inference(paramod,[status(thm)],[c_8655,c_3960]) ).
cnf(c_9029,plain,
least_upper_bound(A,identity) = multiply(A,inverse(greatest_lower_bound(identity,A))),
inference(copy,[status(thm)],[c_11194]) ).
cnf(c_11195,plain,
multiply(A,inverse(greatest_lower_bound(identity,A))) = least_upper_bound(identity,A),
inference(paramod,[status(thm)],[c_8686,c_3957]) ).
cnf(c_9032,plain,
least_upper_bound(identity,A) = multiply(A,inverse(greatest_lower_bound(identity,A))),
inference(copy,[status(thm)],[c_11195]) ).
cnf(c_11196,plain,
least_upper_bound(A,B) = multiply(multiply(multiply(B,inverse(A)),inverse(greatest_lower_bound(identity,multiply(B,inverse(A))))),A),
inference(paramod,[status(thm)],[c_9032,c_4687]) ).
cnf(c_11197,plain,
least_upper_bound(A,B) = multiply(multiply(B,multiply(inverse(A),inverse(greatest_lower_bound(identity,multiply(B,inverse(A)))))),A),
inference(paramod,[status(thm)],[c_3,c_11196]) ).
cnf(c_11198,plain,
least_upper_bound(A,B) = multiply(B,multiply(multiply(inverse(A),inverse(greatest_lower_bound(identity,multiply(B,inverse(A))))),A)),
inference(paramod,[status(thm)],[c_3,c_11197]) ).
cnf(c_10114,plain,
least_upper_bound(A,B) = multiply(B,multiply(inverse(A),multiply(inverse(greatest_lower_bound(identity,multiply(B,inverse(A)))),A))),
inference(paramod,[status(thm)],[c_3,c_11198]) ).
cnf(c_11199,plain,
multiply(multiply(inverse(B),A),multiply(inverse(A),multiply(inverse(greatest_lower_bound(identity,multiply(multiply(inverse(B),A),inverse(A)))),A))) = multiply(inverse(B),least_upper_bound(A,multiply(B,A))),
inference(paramod,[status(thm)],[c_10114,c_2586]) ).
cnf(c_11200,plain,
multiply(multiply(inverse(B),A),multiply(inverse(A),multiply(inverse(greatest_lower_bound(identity,multiply(inverse(B),multiply(A,inverse(A))))),A))) = multiply(inverse(B),least_upper_bound(A,multiply(B,A))),
inference(paramod,[status(thm)],[c_3,c_11199]) ).
cnf(c_11201,plain,
multiply(multiply(inverse(B),A),multiply(inverse(A),multiply(inverse(greatest_lower_bound(identity,multiply(inverse(B),identity))),A))) = multiply(inverse(B),least_upper_bound(A,multiply(B,A))),
inference(paramod,[status(thm)],[c_455,c_11200]) ).
cnf(c_11202,plain,
multiply(multiply(inverse(B),A),multiply(inverse(A),multiply(inverse(greatest_lower_bound(identity,inverse(B))),A))) = multiply(inverse(B),least_upper_bound(A,multiply(B,A))),
inference(paramod,[status(thm)],[c_80,c_11201]) ).
cnf(c_11203,plain,
multiply(multiply(inverse(B),A),multiply(inverse(A),multiply(inverse(multiply(inverse(B),greatest_lower_bound(identity,B))),A))) = multiply(inverse(B),least_upper_bound(A,multiply(B,A))),
inference(paramod,[status(thm)],[c_205,c_11202]) ).
cnf(c_11204,plain,
multiply(inverse(B),multiply(A,multiply(inverse(A),multiply(inverse(multiply(inverse(B),greatest_lower_bound(identity,B))),A)))) = multiply(inverse(B),least_upper_bound(A,multiply(B,A))),
inference(paramod,[status(thm)],[c_3,c_11203]) ).
cnf(c_11205,plain,
multiply(inverse(B),multiply(inverse(multiply(inverse(B),greatest_lower_bound(identity,B))),A)) = multiply(inverse(B),least_upper_bound(A,multiply(B,A))),
inference(paramod,[status(thm)],[c_460,c_11204]) ).
cnf(c_11206,plain,
multiply(inverse(B),multiply(inverse(multiply(inverse(B),greatest_lower_bound(identity,B))),A)) = multiply(inverse(B),multiply(multiply(B,A),multiply(inverse(A),multiply(inverse(greatest_lower_bound(identity,multiply(multiply(B,A),inverse(A)))),A)))),
inference(paramod,[status(thm)],[c_10114,c_11205]) ).
cnf(c_11207,plain,
multiply(inverse(B),multiply(inverse(multiply(inverse(B),greatest_lower_bound(identity,B))),A)) = multiply(inverse(B),multiply(multiply(B,A),multiply(inverse(A),multiply(inverse(greatest_lower_bound(identity,multiply(B,multiply(A,inverse(A))))),A)))),
inference(paramod,[status(thm)],[c_3,c_11206]) ).
cnf(c_11208,plain,
multiply(inverse(B),multiply(inverse(multiply(inverse(B),greatest_lower_bound(identity,B))),A)) = multiply(inverse(B),multiply(multiply(B,A),multiply(inverse(A),multiply(inverse(greatest_lower_bound(identity,multiply(B,identity))),A)))),
inference(paramod,[status(thm)],[c_455,c_11207]) ).
cnf(c_11209,plain,
multiply(inverse(B),multiply(inverse(multiply(inverse(B),greatest_lower_bound(identity,B))),A)) = multiply(inverse(B),multiply(multiply(B,A),multiply(inverse(A),multiply(inverse(greatest_lower_bound(identity,B)),A)))),
inference(paramod,[status(thm)],[c_80,c_11208]) ).
cnf(c_11210,plain,
multiply(inverse(B),multiply(inverse(multiply(inverse(B),greatest_lower_bound(identity,B))),A)) = multiply(inverse(B),multiply(B,multiply(A,multiply(inverse(A),multiply(inverse(greatest_lower_bound(identity,B)),A))))),
inference(paramod,[status(thm)],[c_3,c_11209]) ).
cnf(c_11211,plain,
multiply(inverse(B),multiply(inverse(multiply(inverse(B),greatest_lower_bound(identity,B))),A)) = multiply(inverse(B),multiply(B,multiply(inverse(greatest_lower_bound(identity,B)),A))),
inference(paramod,[status(thm)],[c_460,c_11210]) ).
cnf(c_10370,plain,
multiply(inverse(A),multiply(inverse(multiply(inverse(A),greatest_lower_bound(identity,A))),B)) = multiply(inverse(greatest_lower_bound(identity,A)),B),
inference(paramod,[status(thm)],[c_23,c_11211]) ).
cnf(c_11212,plain,
multiply(identity,multiply(inverse(A),multiply(inverse(greatest_lower_bound(identity,multiply(identity,inverse(A)))),A))) = multiply(A,inverse(greatest_lower_bound(identity,A))),
inference(paramod,[status(thm)],[c_10114,c_9029]) ).
cnf(c_11213,plain,
multiply(identity,multiply(inverse(A),multiply(inverse(greatest_lower_bound(identity,inverse(A))),A))) = multiply(A,inverse(greatest_lower_bound(identity,A))),
inference(paramod,[status(thm)],[c_1,c_11212]) ).
cnf(c_11214,plain,
multiply(identity,multiply(inverse(A),multiply(inverse(multiply(inverse(A),greatest_lower_bound(identity,A))),A))) = multiply(A,inverse(greatest_lower_bound(identity,A))),
inference(paramod,[status(thm)],[c_205,c_11213]) ).
cnf(c_11215,plain,
multiply(identity,multiply(inverse(greatest_lower_bound(identity,A)),A)) = multiply(A,inverse(greatest_lower_bound(identity,A))),
inference(paramod,[status(thm)],[c_10370,c_11214]) ).
cnf(c_10454,plain,
multiply(inverse(greatest_lower_bound(identity,A)),A) = multiply(A,inverse(greatest_lower_bound(identity,A))),
inference(paramod,[status(thm)],[c_1,c_11215]) ).
cnf(c_10584,plain,
inverse(multiply(b,multiply(inverse(a),multiply(inverse(greatest_lower_bound(identity,multiply(b,inverse(a)))),a)))) != multiply(inverse(b),greatest_lower_bound(identity,multiply(b,inverse(a)))),
inference(paramod,[status(thm)],[c_10114,c_4657]) ).
cnf(c_11216,plain,
inverse(multiply(b,multiply(inverse(a),multiply(inverse(multiply(b,greatest_lower_bound(inverse(a),inverse(b)))),a)))) != multiply(inverse(b),greatest_lower_bound(identity,multiply(b,inverse(a)))),
inference(paramod,[status(thm)],[c_464,c_10584]) ).
cnf(c_10937,plain,
inverse(multiply(b,multiply(inverse(a),multiply(inverse(multiply(b,multiply(inverse(a),greatest_lower_bound(identity,multiply(a,inverse(b)))))),a)))) != multiply(inverse(b),greatest_lower_bound(identity,multiply(b,inverse(a)))),
inference(paramod,[status(thm)],[c_219,c_11216]) ).
cnf(c_11217,plain,
multiply(inverse(multiply(A,B)),multiply(A,identity)) = inverse(B),
inference(paramod,[status(thm)],[c_455,c_70]) ).
cnf(c_10969,plain,
multiply(inverse(multiply(A,B)),A) = inverse(B),
inference(paramod,[status(thm)],[c_80,c_11217]) ).
cnf(c_11218,plain,
multiply(inverse(A),inverse(B)) = inverse(multiply(B,A)),
inference(paramod,[status(thm)],[c_23,c_10969]) ).
cnf(c_11009,plain,
inverse(multiply(A,B)) = multiply(inverse(B),inverse(A)),
inference(copy,[status(thm)],[c_11218]) ).
cnf(c_11219,plain,
inverse(multiply(b,multiply(inverse(a),multiply(multiply(inverse(multiply(inverse(a),greatest_lower_bound(identity,multiply(a,inverse(b))))),inverse(b)),a)))) != multiply(inverse(b),greatest_lower_bound(identity,multiply(b,inverse(a)))),
inference(paramod,[status(thm)],[c_11009,c_10937]) ).
cnf(c_11220,plain,
inverse(multiply(b,multiply(inverse(a),multiply(multiply(multiply(inverse(greatest_lower_bound(identity,multiply(a,inverse(b)))),inverse(inverse(a))),inverse(b)),a)))) != multiply(inverse(b),greatest_lower_bound(identity,multiply(b,inverse(a)))),
inference(paramod,[status(thm)],[c_11009,c_11219]) ).
cnf(c_11221,plain,
inverse(multiply(b,multiply(inverse(a),multiply(multiply(multiply(inverse(greatest_lower_bound(identity,multiply(a,inverse(b)))),a),inverse(b)),a)))) != multiply(inverse(b),greatest_lower_bound(identity,multiply(b,inverse(a)))),
inference(paramod,[status(thm)],[c_461,c_11220]) ).
cnf(c_11222,plain,
inverse(multiply(b,multiply(inverse(a),multiply(multiply(inverse(greatest_lower_bound(identity,multiply(a,inverse(b)))),multiply(a,inverse(b))),a)))) != multiply(inverse(b),greatest_lower_bound(identity,multiply(b,inverse(a)))),
inference(paramod,[status(thm)],[c_3,c_11221]) ).
cnf(c_11223,plain,
inverse(multiply(b,multiply(inverse(a),multiply(multiply(multiply(a,inverse(b)),inverse(greatest_lower_bound(identity,multiply(a,inverse(b))))),a)))) != multiply(inverse(b),greatest_lower_bound(identity,multiply(b,inverse(a)))),
inference(paramod,[status(thm)],[c_10454,c_11222]) ).
cnf(c_11224,plain,
inverse(multiply(b,multiply(inverse(a),multiply(multiply(a,multiply(inverse(b),inverse(greatest_lower_bound(identity,multiply(a,inverse(b)))))),a)))) != multiply(inverse(b),greatest_lower_bound(identity,multiply(b,inverse(a)))),
inference(paramod,[status(thm)],[c_3,c_11223]) ).
cnf(c_11225,plain,
inverse(multiply(b,multiply(inverse(a),multiply(a,multiply(multiply(inverse(b),inverse(greatest_lower_bound(identity,multiply(a,inverse(b))))),a))))) != multiply(inverse(b),greatest_lower_bound(identity,multiply(b,inverse(a)))),
inference(paramod,[status(thm)],[c_3,c_11224]) ).
cnf(c_11226,plain,
inverse(multiply(b,multiply(inverse(a),multiply(a,multiply(inverse(b),multiply(inverse(greatest_lower_bound(identity,multiply(a,inverse(b)))),a)))))) != multiply(inverse(b),greatest_lower_bound(identity,multiply(b,inverse(a)))),
inference(paramod,[status(thm)],[c_3,c_11225]) ).
cnf(c_11227,plain,
inverse(multiply(b,multiply(inverse(b),multiply(inverse(greatest_lower_bound(identity,multiply(a,inverse(b)))),a)))) != multiply(inverse(b),greatest_lower_bound(identity,multiply(b,inverse(a)))),
inference(paramod,[status(thm)],[c_23,c_11226]) ).
cnf(c_11228,plain,
inverse(multiply(inverse(greatest_lower_bound(identity,multiply(a,inverse(b)))),a)) != multiply(inverse(b),greatest_lower_bound(identity,multiply(b,inverse(a)))),
inference(paramod,[status(thm)],[c_460,c_11227]) ).
cnf(c_11229,plain,
multiply(inverse(a),inverse(inverse(greatest_lower_bound(identity,multiply(a,inverse(b)))))) != multiply(inverse(b),greatest_lower_bound(identity,multiply(b,inverse(a)))),
inference(paramod,[status(thm)],[c_11009,c_11228]) ).
cnf(c_11230,plain,
multiply(inverse(a),greatest_lower_bound(identity,multiply(a,inverse(b)))) != multiply(inverse(b),greatest_lower_bound(identity,multiply(b,inverse(a)))),
inference(paramod,[status(thm)],[c_461,c_11229]) ).
cnf(c_11045,plain,
$false,
inference(resolve,[status(thm)],[c_4750,c_11230]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP179-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.43 % Computer : n008.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Fri Sep 25 14:35:24 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/0.44 % Process 1274714 was started by sandbox on n008,
% 0.18/0.44 % Fri Sep 25 14:35:24 2026
% 0.18/0.44 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.18/0.44
% 0.18/0.44 % From the command line: assign(max_seconds, 300).
% 102.60/14.42
% 102.60/14.42 % SZS status Unsatisfiable for theBenchmark
% 102.60/14.42
% 102.60/14.42 % Proof 1 at 4.85 (+ 1.04) seconds.
% 102.60/14.42 % Length of proof is 130.
% 102.60/14.42 % Level of proof is 18.
% 102.60/14.42 % Maximum clause weight is 100.000.
% 102.60/14.42 % Given clauses 347.
% 102.60/14.42
% 102.60/14.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------