%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP179-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 : n014.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 90.42s 13.06s
% Output : CNFRefutation 90.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 16
% Syntax : Number of formulae : 238 ( 238 unt; 0 def)
% Number of atoms : 238 ( 237 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 33 ( 33 ~; 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 : 6 ( 6 usr; 2 con; 0-2 aty)
% Number of variables : 402 ( 28 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_p18,axiom,
least_upper_bound(inverse(a),identity) != inverse(greatest_lower_bound(a,identity)),
file('theBenchmark.p',prove_p18) ).
cnf(c_22,plain,
least_upper_bound(inverse(a),identity) != inverse(greatest_lower_bound(a,identity)),
inference(clausify,[status(thm)],[prove_p18]) ).
cnf(c_8156,plain,
least_upper_bound(identity,inverse(a)) != inverse(greatest_lower_bound(a,identity)),
inference(paramod,[status(thm)],[c_5,c_22]) ).
cnf(c_23,plain,
least_upper_bound(identity,inverse(a)) != inverse(greatest_lower_bound(identity,a)),
inference(paramod,[status(thm)],[c_4,c_8156]) ).
cnf(c_8157,plain,
multiply(identity,A) = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_3]) ).
cnf(c_8158,plain,
A = multiply(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_1,c_8157]) ).
cnf(c_24,plain,
multiply(inverse(A),multiply(A,B)) = B,
inference(copy,[status(thm)],[c_8158]) ).
cnf(c_8159,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_29,plain,
least_upper_bound(A,least_upper_bound(A,B)) = least_upper_bound(A,B),
inference(copy,[status(thm)],[c_8159]) ).
cnf(c_8160,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_32,plain,
greatest_lower_bound(A,greatest_lower_bound(A,B)) = greatest_lower_bound(A,B),
inference(copy,[status(thm)],[c_8160]) ).
cnf(c_35,plain,
least_upper_bound(A,greatest_lower_bound(B,A)) = A,
inference(paramod,[status(thm)],[c_4,c_12]) ).
cnf(c_8161,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_37,plain,
least_upper_bound(A,least_upper_bound(greatest_lower_bound(A,B),C)) = least_upper_bound(A,C),
inference(copy,[status(thm)],[c_8161]) ).
cnf(c_39,plain,
greatest_lower_bound(A,least_upper_bound(B,A)) = A,
inference(paramod,[status(thm)],[c_5,c_13]) ).
cnf(c_8162,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_40,plain,
greatest_lower_bound(A,greatest_lower_bound(least_upper_bound(A,B),C)) = greatest_lower_bound(A,C),
inference(copy,[status(thm)],[c_8162]) ).
cnf(c_43,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_46,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_8163,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_47,plain,
greatest_lower_bound(identity,multiply(inverse(A),B)) = multiply(inverse(A),greatest_lower_bound(B,A)),
inference(paramod,[status(thm)],[c_4,c_8163]) ).
cnf(c_49,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_8164,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_52,plain,
least_upper_bound(identity,multiply(A,B)) = multiply(least_upper_bound(A,inverse(B)),B),
inference(paramod,[status(thm)],[c_5,c_8164]) ).
cnf(c_56,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_8165,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_57,plain,
greatest_lower_bound(A,multiply(B,A)) = multiply(greatest_lower_bound(B,identity),A),
inference(paramod,[status(thm)],[c_4,c_8165]) ).
cnf(c_8166,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_59,plain,
greatest_lower_bound(identity,multiply(A,B)) = multiply(greatest_lower_bound(A,inverse(B)),B),
inference(paramod,[status(thm)],[c_4,c_8166]) ).
cnf(c_70,plain,
multiply(inverse(inverse(A)),identity) = A,
inference(paramod,[status(thm)],[c_2,c_24]) ).
cnf(c_80,plain,
multiply(inverse(inverse(A)),B) = multiply(A,B),
inference(paramod,[status(thm)],[c_24,c_24]) ).
cnf(c_81,plain,
multiply(A,identity) = A,
inference(paramod,[status(thm)],[c_80,c_70]) ).
cnf(c_82,plain,
inverse(identity) = identity,
inference(paramod,[status(thm)],[c_81,c_2]) ).
cnf(c_83,plain,
least_upper_bound(A,multiply(A,B)) = multiply(A,least_upper_bound(identity,B)),
inference(paramod,[status(thm)],[c_81,c_15]) ).
cnf(c_85,plain,
greatest_lower_bound(A,multiply(A,B)) = multiply(A,greatest_lower_bound(identity,B)),
inference(paramod,[status(thm)],[c_81,c_17]) ).
cnf(c_8167,plain,
greatest_lower_bound(multiply(A,B),A) = multiply(A,greatest_lower_bound(B,identity)),
inference(paramod,[status(thm)],[c_81,c_17]) ).
cnf(c_86,plain,
greatest_lower_bound(A,multiply(A,B)) = multiply(A,greatest_lower_bound(B,identity)),
inference(paramod,[status(thm)],[c_4,c_8167]) ).
cnf(c_145,plain,
greatest_lower_bound(A,multiply(greatest_lower_bound(identity,B),A)) = greatest_lower_bound(A,multiply(B,A)),
inference(paramod,[status(thm)],[c_56,c_32]) ).
cnf(c_157,plain,
multiply(inverse(greatest_lower_bound(A,identity)),greatest_lower_bound(B,multiply(A,B))) = B,
inference(paramod,[status(thm)],[c_57,c_24]) ).
cnf(c_8168,plain,
least_upper_bound(inverse(A),identity) = multiply(inverse(A),least_upper_bound(identity,A)),
inference(paramod,[status(thm)],[c_2,c_83]) ).
cnf(c_158,plain,
least_upper_bound(identity,inverse(A)) = multiply(inverse(A),least_upper_bound(identity,A)),
inference(paramod,[status(thm)],[c_5,c_8168]) ).
cnf(c_8169,plain,
least_upper_bound(A,multiply(A,greatest_lower_bound(identity,B))) = multiply(A,identity),
inference(paramod,[status(thm)],[c_12,c_83]) ).
cnf(c_163,plain,
least_upper_bound(A,multiply(A,greatest_lower_bound(identity,B))) = A,
inference(paramod,[status(thm)],[c_81,c_8169]) ).
cnf(c_8170,plain,
multiply(inverse(A),least_upper_bound(A,multiply(A,B))) = least_upper_bound(identity,B),
inference(paramod,[status(thm)],[c_83,c_24]) ).
cnf(c_174,plain,
least_upper_bound(identity,A) = multiply(inverse(B),least_upper_bound(B,multiply(B,A))),
inference(copy,[status(thm)],[c_8170]) ).
cnf(c_175,plain,
least_upper_bound(inverse(A),B) = multiply(inverse(A),least_upper_bound(identity,multiply(A,B))),
inference(paramod,[status(thm)],[c_24,c_83]) ).
cnf(c_176,plain,
least_upper_bound(A,multiply(A,least_upper_bound(identity,B))) = least_upper_bound(A,multiply(A,B)),
inference(paramod,[status(thm)],[c_83,c_29]) ).
cnf(c_8171,plain,
multiply(A,least_upper_bound(identity,A)) = multiply(least_upper_bound(identity,A),A),
inference(paramod,[status(thm)],[c_83,c_49]) ).
cnf(c_178,plain,
multiply(least_upper_bound(identity,A),A) = multiply(A,least_upper_bound(identity,A)),
inference(copy,[status(thm)],[c_8171]) ).
cnf(c_187,plain,
multiply(inverse(a),least_upper_bound(identity,a)) != inverse(greatest_lower_bound(identity,a)),
inference(paramod,[status(thm)],[c_158,c_23]) ).
cnf(c_8172,plain,
greatest_lower_bound(inverse(A),identity) = multiply(inverse(A),greatest_lower_bound(identity,A)),
inference(paramod,[status(thm)],[c_2,c_85]) ).
cnf(c_207,plain,
greatest_lower_bound(identity,inverse(A)) = multiply(inverse(A),greatest_lower_bound(identity,A)),
inference(paramod,[status(thm)],[c_4,c_8172]) ).
cnf(c_8173,plain,
multiply(inverse(A),greatest_lower_bound(A,multiply(A,B))) = greatest_lower_bound(identity,B),
inference(paramod,[status(thm)],[c_85,c_24]) ).
cnf(c_220,plain,
greatest_lower_bound(identity,A) = multiply(inverse(B),greatest_lower_bound(B,multiply(B,A))),
inference(copy,[status(thm)],[c_8173]) ).
cnf(c_221,plain,
greatest_lower_bound(inverse(A),B) = multiply(inverse(A),greatest_lower_bound(identity,multiply(A,B))),
inference(paramod,[status(thm)],[c_24,c_85]) ).
cnf(c_8174,plain,
greatest_lower_bound(inverse(greatest_lower_bound(A,identity)),multiply(inverse(greatest_lower_bound(A,identity)),A)) = identity,
inference(paramod,[status(thm)],[c_86,c_2]) ).
cnf(c_235,plain,
multiply(inverse(greatest_lower_bound(A,identity)),greatest_lower_bound(identity,A)) = identity,
inference(paramod,[status(thm)],[c_85,c_8174]) ).
cnf(c_8175,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_178,c_86]) ).
cnf(c_8176,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_56,c_8175]) ).
cnf(c_261,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_8176]) ).
cnf(c_8177,plain,
multiply(identity,A) = multiply(inverse(greatest_lower_bound(B,identity)),multiply(greatest_lower_bound(identity,B),A)),
inference(paramod,[status(thm)],[c_235,c_3]) ).
cnf(c_8178,plain,
A = multiply(inverse(greatest_lower_bound(B,identity)),multiply(greatest_lower_bound(identity,B),A)),
inference(paramod,[status(thm)],[c_1,c_8177]) ).
cnf(c_378,plain,
multiply(inverse(greatest_lower_bound(A,identity)),multiply(greatest_lower_bound(identity,A),B)) = B,
inference(copy,[status(thm)],[c_8178]) ).
cnf(c_456,plain,
multiply(A,inverse(A)) = identity,
inference(paramod,[status(thm)],[c_80,c_2]) ).
cnf(c_461,plain,
multiply(A,multiply(inverse(A),B)) = B,
inference(paramod,[status(thm)],[c_80,c_24]) ).
cnf(c_8179,plain,
multiply(A,identity) = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_80,c_81]) ).
cnf(c_8180,plain,
A = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_81,c_8179]) ).
cnf(c_462,plain,
inverse(inverse(A)) = A,
inference(copy,[status(thm)],[c_8180]) ).
cnf(c_8181,plain,
least_upper_bound(inverse(A),identity) = multiply(least_upper_bound(identity,A),inverse(A)),
inference(paramod,[status(thm)],[c_456,c_49]) ).
cnf(c_8182,plain,
least_upper_bound(identity,inverse(A)) = multiply(least_upper_bound(identity,A),inverse(A)),
inference(paramod,[status(thm)],[c_5,c_8181]) ).
cnf(c_8183,plain,
multiply(inverse(A),least_upper_bound(identity,A)) = multiply(least_upper_bound(identity,A),inverse(A)),
inference(paramod,[status(thm)],[c_158,c_8182]) ).
cnf(c_470,plain,
multiply(least_upper_bound(identity,A),inverse(A)) = multiply(inverse(A),least_upper_bound(identity,A)),
inference(copy,[status(thm)],[c_8183]) ).
cnf(c_8184,plain,
greatest_lower_bound(inverse(A),identity) = multiply(greatest_lower_bound(identity,A),inverse(A)),
inference(paramod,[status(thm)],[c_456,c_56]) ).
cnf(c_8185,plain,
greatest_lower_bound(identity,inverse(A)) = multiply(greatest_lower_bound(identity,A),inverse(A)),
inference(paramod,[status(thm)],[c_4,c_8184]) ).
cnf(c_8186,plain,
multiply(inverse(A),greatest_lower_bound(identity,A)) = multiply(greatest_lower_bound(identity,A),inverse(A)),
inference(paramod,[status(thm)],[c_207,c_8185]) ).
cnf(c_473,plain,
multiply(greatest_lower_bound(identity,A),inverse(A)) = multiply(inverse(A),greatest_lower_bound(identity,A)),
inference(copy,[status(thm)],[c_8186]) ).
cnf(c_8187,plain,
greatest_lower_bound(inverse(A),identity) = multiply(greatest_lower_bound(A,identity),inverse(A)),
inference(paramod,[status(thm)],[c_456,c_57]) ).
cnf(c_8188,plain,
greatest_lower_bound(identity,inverse(A)) = multiply(greatest_lower_bound(A,identity),inverse(A)),
inference(paramod,[status(thm)],[c_4,c_8187]) ).
cnf(c_8189,plain,
multiply(inverse(A),greatest_lower_bound(identity,A)) = multiply(greatest_lower_bound(A,identity),inverse(A)),
inference(paramod,[status(thm)],[c_207,c_8188]) ).
cnf(c_474,plain,
multiply(greatest_lower_bound(A,identity),inverse(A)) = multiply(inverse(A),greatest_lower_bound(identity,A)),
inference(copy,[status(thm)],[c_8189]) ).
cnf(c_8190,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_473,c_3]) ).
cnf(c_8191,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_8190]) ).
cnf(c_504,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_8191]) ).
cnf(c_517,plain,
multiply(greatest_lower_bound(A,identity),inverse(A)) = multiply(inverse(A),greatest_lower_bound(A,identity)),
inference(paramod,[status(thm)],[c_4,c_474]) ).
cnf(c_8192,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_517,c_3]) ).
cnf(c_8193,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_8192]) ).
cnf(c_543,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_8193]) ).
cnf(c_556,plain,
least_upper_bound(multiply(A,B),C) = multiply(A,least_upper_bound(B,multiply(inverse(A),C))),
inference(paramod,[status(thm)],[c_461,c_15]) ).
cnf(c_557,plain,
greatest_lower_bound(multiply(A,B),C) = multiply(A,greatest_lower_bound(B,multiply(inverse(A),C))),
inference(paramod,[status(thm)],[c_461,c_17]) ).
cnf(c_853,plain,
multiply(inverse(greatest_lower_bound(A,identity)),multiply(A,greatest_lower_bound(identity,A))) = A,
inference(paramod,[status(thm)],[c_85,c_157]) ).
cnf(c_8194,plain,
least_upper_bound(identity,inverse(A)) = multiply(inverse(greatest_lower_bound(A,identity)),least_upper_bound(greatest_lower_bound(A,identity),multiply(inverse(A),greatest_lower_bound(A,identity)))),
inference(paramod,[status(thm)],[c_517,c_174]) ).
cnf(c_8195,plain,
multiply(inverse(A),least_upper_bound(identity,A)) = multiply(inverse(greatest_lower_bound(A,identity)),least_upper_bound(greatest_lower_bound(A,identity),multiply(inverse(A),greatest_lower_bound(A,identity)))),
inference(paramod,[status(thm)],[c_158,c_8194]) ).
cnf(c_8196,plain,
multiply(inverse(A),least_upper_bound(identity,A)) = multiply(inverse(greatest_lower_bound(A,identity)),multiply(least_upper_bound(identity,inverse(A)),greatest_lower_bound(A,identity))),
inference(paramod,[status(thm)],[c_49,c_8195]) ).
cnf(c_8197,plain,
multiply(inverse(A),least_upper_bound(identity,A)) = multiply(inverse(greatest_lower_bound(A,identity)),multiply(multiply(inverse(A),least_upper_bound(identity,A)),greatest_lower_bound(A,identity))),
inference(paramod,[status(thm)],[c_158,c_8196]) ).
cnf(c_8198,plain,
multiply(inverse(A),least_upper_bound(identity,A)) = multiply(inverse(greatest_lower_bound(A,identity)),multiply(inverse(A),multiply(least_upper_bound(identity,A),greatest_lower_bound(A,identity)))),
inference(paramod,[status(thm)],[c_3,c_8197]) ).
cnf(c_8199,plain,
multiply(inverse(A),least_upper_bound(identity,A)) = multiply(inverse(greatest_lower_bound(A,identity)),multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A)))),
inference(paramod,[status(thm)],[c_261,c_8198]) ).
cnf(c_889,plain,
multiply(inverse(greatest_lower_bound(A,identity)),multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A)))) = multiply(inverse(A),least_upper_bound(identity,A)),
inference(copy,[status(thm)],[c_8199]) ).
cnf(c_8200,plain,
multiply(inverse(a),least_upper_bound(identity,a)) != inverse(multiply(inverse(A),greatest_lower_bound(A,multiply(A,a)))),
inference(paramod,[status(thm)],[c_220,c_187]) ).
cnf(c_938,plain,
inverse(multiply(inverse(A),greatest_lower_bound(A,multiply(A,a)))) != multiply(inverse(a),least_upper_bound(identity,a)),
inference(copy,[status(thm)],[c_8200]) ).
cnf(c_8201,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_470,c_220]) ).
cnf(c_8202,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_207,c_8201]) ).
cnf(c_8203,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_56,c_8202]) ).
cnf(c_8204,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_207,c_8203]) ).
cnf(c_8205,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_8204]) ).
cnf(c_951,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_8205]) ).
cnf(c_8206,plain,
inverse(multiply(inverse(multiply(A,B)),greatest_lower_bound(multiply(A,B),multiply(A,multiply(B,a))))) != multiply(inverse(a),least_upper_bound(identity,a)),
inference(paramod,[status(thm)],[c_3,c_938]) ).
cnf(c_8207,plain,
inverse(multiply(inverse(multiply(A,B)),multiply(A,greatest_lower_bound(B,multiply(inverse(A),multiply(A,multiply(B,a))))))) != multiply(inverse(a),least_upper_bound(identity,a)),
inference(paramod,[status(thm)],[c_557,c_8206]) ).
cnf(c_1053,plain,
inverse(multiply(inverse(multiply(A,B)),multiply(A,greatest_lower_bound(B,multiply(B,a))))) != multiply(inverse(a),least_upper_bound(identity,a)),
inference(paramod,[status(thm)],[c_24,c_8207]) ).
cnf(c_8208,plain,
inverse(multiply(inverse(multiply(inverse(greatest_lower_bound(A,multiply(A,a))),A)),identity)) != multiply(inverse(a),least_upper_bound(identity,a)),
inference(paramod,[status(thm)],[c_2,c_1053]) ).
cnf(c_8209,plain,
inverse(inverse(multiply(inverse(greatest_lower_bound(A,multiply(A,a))),A))) != multiply(inverse(a),least_upper_bound(identity,a)),
inference(paramod,[status(thm)],[c_81,c_8208]) ).
cnf(c_1070,plain,
multiply(inverse(greatest_lower_bound(A,multiply(A,a))),A) != multiply(inverse(a),least_upper_bound(identity,a)),
inference(paramod,[status(thm)],[c_462,c_8209]) ).
cnf(c_8210,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_37,c_39]) ).
cnf(c_1170,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_8210]) ).
cnf(c_8211,plain,
least_upper_bound(A,greatest_lower_bound(A,B)) = least_upper_bound(A,multiply(greatest_lower_bound(A,B),greatest_lower_bound(identity,C))),
inference(paramod,[status(thm)],[c_163,c_37]) ).
cnf(c_8212,plain,
A = least_upper_bound(A,multiply(greatest_lower_bound(A,B),greatest_lower_bound(identity,C))),
inference(paramod,[status(thm)],[c_12,c_8211]) ).
cnf(c_1181,plain,
least_upper_bound(A,multiply(greatest_lower_bound(A,B),greatest_lower_bound(identity,C))) = A,
inference(copy,[status(thm)],[c_8212]) ).
cnf(c_1304,plain,
multiply(inverse(multiply(A,greatest_lower_bound(identity,a))),A) != multiply(inverse(a),least_upper_bound(identity,a)),
inference(paramod,[status(thm)],[c_85,c_1070]) ).
cnf(c_1314,plain,
multiply(inverse(least_upper_bound(identity,multiply(A,greatest_lower_bound(identity,a)))),least_upper_bound(A,inverse(greatest_lower_bound(identity,a)))) != multiply(inverse(a),least_upper_bound(identity,a)),
inference(paramod,[status(thm)],[c_52,c_1304]) ).
cnf(c_1815,plain,
greatest_lower_bound(identity,multiply(inverse(A),least_upper_bound(A,B))) = identity,
inference(paramod,[status(thm)],[c_43,c_13]) ).
cnf(c_1931,plain,
greatest_lower_bound(identity,multiply(inverse(A),least_upper_bound(B,A))) = identity,
inference(paramod,[status(thm)],[c_5,c_1815]) ).
cnf(c_2202,plain,
least_upper_bound(A,multiply(greatest_lower_bound(A,B),multiply(inverse(C),greatest_lower_bound(D,C)))) = A,
inference(paramod,[status(thm)],[c_47,c_1181]) ).
cnf(c_8213,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_461,c_145]) ).
cnf(c_8214,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_504,c_8213]) ).
cnf(c_8215,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_557,c_8214]) ).
cnf(c_8216,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_462,c_8215]) ).
cnf(c_8217,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_461,c_8216]) ).
cnf(c_8218,plain,
multiply(inverse(A),greatest_lower_bound(B,multiply(A,B))) = greatest_lower_bound(multiply(inverse(A),B),B),
inference(paramod,[status(thm)],[c_145,c_8217]) ).
cnf(c_8219,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_8218]) ).
cnf(c_2334,plain,
greatest_lower_bound(A,multiply(inverse(B),A)) = multiply(inverse(B),greatest_lower_bound(A,multiply(B,A))),
inference(copy,[status(thm)],[c_8219]) ).
cnf(c_8220,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_517,c_176]) ).
cnf(c_8221,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_158,c_8220]) ).
cnf(c_8222,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_543,c_8221]) ).
cnf(c_8223,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_49,c_8222]) ).
cnf(c_8224,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_158,c_8223]) ).
cnf(c_8225,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_8224]) ).
cnf(c_2573,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_261,c_8225]) ).
cnf(c_8226,plain,
multiply(inverse(least_upper_bound(identity,greatest_lower_bound(greatest_lower_bound(identity,a),multiply(A,greatest_lower_bound(identity,a))))),least_upper_bound(greatest_lower_bound(identity,A),inverse(greatest_lower_bound(identity,a)))) != multiply(inverse(a),least_upper_bound(identity,a)),
inference(paramod,[status(thm)],[c_56,c_1314]) ).
cnf(c_8227,plain,
multiply(inverse(least_upper_bound(identity,multiply(greatest_lower_bound(identity,A),greatest_lower_bound(identity,a)))),least_upper_bound(greatest_lower_bound(identity,A),inverse(greatest_lower_bound(identity,a)))) != multiply(inverse(a),least_upper_bound(identity,a)),
inference(paramod,[status(thm)],[c_56,c_8226]) ).
cnf(c_8228,plain,
multiply(inverse(identity),least_upper_bound(greatest_lower_bound(identity,A),inverse(greatest_lower_bound(identity,a)))) != multiply(inverse(a),least_upper_bound(identity,a)),
inference(paramod,[status(thm)],[c_1181,c_8227]) ).
cnf(c_8229,plain,
multiply(identity,least_upper_bound(greatest_lower_bound(identity,A),inverse(greatest_lower_bound(identity,a)))) != multiply(inverse(a),least_upper_bound(identity,a)),
inference(paramod,[status(thm)],[c_82,c_8228]) ).
cnf(c_2842,plain,
least_upper_bound(greatest_lower_bound(identity,A),inverse(greatest_lower_bound(identity,a))) != multiply(inverse(a),least_upper_bound(identity,a)),
inference(paramod,[status(thm)],[c_1,c_8229]) ).
cnf(c_8230,plain,
least_upper_bound(multiply(inverse(A),greatest_lower_bound(B,A)),inverse(greatest_lower_bound(identity,a))) != multiply(inverse(a),least_upper_bound(identity,a)),
inference(paramod,[status(thm)],[c_47,c_2842]) ).
cnf(c_8231,plain,
multiply(inverse(A),least_upper_bound(greatest_lower_bound(B,A),multiply(inverse(inverse(A)),inverse(greatest_lower_bound(identity,a))))) != multiply(inverse(a),least_upper_bound(identity,a)),
inference(paramod,[status(thm)],[c_556,c_8230]) ).
cnf(c_3126,plain,
multiply(inverse(A),least_upper_bound(greatest_lower_bound(B,A),multiply(A,inverse(greatest_lower_bound(identity,a))))) != multiply(inverse(a),least_upper_bound(identity,a)),
inference(paramod,[status(thm)],[c_462,c_8231]) ).
cnf(c_8232,plain,
multiply(inverse(greatest_lower_bound(inverse(A),identity)),greatest_lower_bound(identity,multiply(identity,A))) = A,
inference(paramod,[status(thm)],[c_59,c_378]) ).
cnf(c_8233,plain,
multiply(inverse(greatest_lower_bound(identity,inverse(A))),greatest_lower_bound(identity,multiply(identity,A))) = A,
inference(paramod,[status(thm)],[c_4,c_8232]) ).
cnf(c_8234,plain,
multiply(inverse(multiply(inverse(A),greatest_lower_bound(identity,A))),greatest_lower_bound(identity,multiply(identity,A))) = A,
inference(paramod,[status(thm)],[c_207,c_8233]) ).
cnf(c_4452,plain,
multiply(inverse(multiply(inverse(A),greatest_lower_bound(identity,A))),greatest_lower_bound(identity,A)) = A,
inference(paramod,[status(thm)],[c_1,c_8234]) ).
cnf(c_8235,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_175]) ).
cnf(c_8236,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_462,c_8235]) ).
cnf(c_4603,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_462,c_8236]) ).
cnf(c_4745,plain,
multiply(inverse(least_upper_bound(A,B)),least_upper_bound(A,multiply(least_upper_bound(A,B),inverse(greatest_lower_bound(identity,a))))) != multiply(inverse(a),least_upper_bound(identity,a)),
inference(paramod,[status(thm)],[c_13,c_3126]) ).
cnf(c_8237,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_83,c_1170]) ).
cnf(c_6609,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_557,c_8237]) ).
cnf(c_8238,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_59,c_1170]) ).
cnf(c_8239,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_556,c_8238]) ).
cnf(c_6628,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_8239]) ).
cnf(c_8240,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_46,c_1170]) ).
cnf(c_8241,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_6628,c_8240]) ).
cnf(c_8242,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_221,c_8241]) ).
cnf(c_8243,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_221,c_8242]) ).
cnf(c_8244,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_8243]) ).
cnf(c_8245,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_32,c_8244]) ).
cnf(c_8246,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_556,c_8245]) ).
cnf(c_8247,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_462,c_8246]) ).
cnf(c_6664,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_8247]) ).
cnf(c_8248,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_6664,c_6609]) ).
cnf(c_8249,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_32,c_8248]) ).
cnf(c_6783,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_8249]) ).
cnf(c_8250,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_6783,c_4603]) ).
cnf(c_8251,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_8250]) ).
cnf(c_8252,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_82,c_8251]) ).
cnf(c_8253,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_81,c_8252]) ).
cnf(c_8254,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_82,c_8253]) ).
cnf(c_8255,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_81,c_8254]) ).
cnf(c_6954,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_4452,c_8255]) ).
cnf(c_8256,plain,
least_upper_bound(inverse(least_upper_bound(identity,A)),multiply(inverse(least_upper_bound(identity,A)),multiply(least_upper_bound(identity,A),inverse(greatest_lower_bound(identity,a))))) != multiply(inverse(a),least_upper_bound(identity,a)),
inference(paramod,[status(thm)],[c_83,c_4745]) ).
cnf(c_8257,plain,
least_upper_bound(inverse(least_upper_bound(identity,A)),inverse(greatest_lower_bound(identity,a))) != multiply(inverse(a),least_upper_bound(identity,a)),
inference(paramod,[status(thm)],[c_24,c_8256]) ).
cnf(c_8258,plain,
least_upper_bound(inverse(greatest_lower_bound(identity,a)),inverse(least_upper_bound(identity,A))) != multiply(inverse(a),least_upper_bound(identity,a)),
inference(paramod,[status(thm)],[c_5,c_8257]) ).
cnf(c_7877,plain,
multiply(inverse(greatest_lower_bound(identity,a)),least_upper_bound(identity,multiply(greatest_lower_bound(identity,a),inverse(least_upper_bound(identity,A))))) != multiply(inverse(a),least_upper_bound(identity,a)),
inference(paramod,[status(thm)],[c_175,c_8258]) ).
cnf(c_8259,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_2334,c_40]) ).
cnf(c_8073,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_56,c_8259]) ).
cnf(c_8260,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_8073,c_6954]) ).
cnf(c_8261,plain,
multiply(A,identity) = multiply(greatest_lower_bound(A,identity),least_upper_bound(identity,A)),
inference(paramod,[status(thm)],[c_1931,c_8260]) ).
cnf(c_8262,plain,
A = multiply(greatest_lower_bound(A,identity),least_upper_bound(identity,A)),
inference(paramod,[status(thm)],[c_81,c_8261]) ).
cnf(c_8128,plain,
multiply(greatest_lower_bound(A,identity),least_upper_bound(identity,A)) = A,
inference(copy,[status(thm)],[c_8262]) ).
cnf(c_8263,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_8128,c_2573]) ).
cnf(c_8264,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_8263]) ).
cnf(c_8265,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_8264]) ).
cnf(c_8266,plain,
identity = multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A))),
inference(paramod,[status(thm)],[c_35,c_8265]) ).
cnf(c_8131,plain,
multiply(inverse(A),multiply(greatest_lower_bound(identity,A),least_upper_bound(identity,A))) = identity,
inference(copy,[status(thm)],[c_8266]) ).
cnf(c_8267,plain,
multiply(inverse(least_upper_bound(identity,A)),identity) = multiply(inverse(A),greatest_lower_bound(identity,A)),
inference(paramod,[status(thm)],[c_8131,c_951]) ).
cnf(c_8132,plain,
inverse(least_upper_bound(identity,A)) = multiply(inverse(A),greatest_lower_bound(identity,A)),
inference(paramod,[status(thm)],[c_81,c_8267]) ).
cnf(c_8268,plain,
multiply(inverse(greatest_lower_bound(A,identity)),identity) = multiply(inverse(A),least_upper_bound(identity,A)),
inference(paramod,[status(thm)],[c_8131,c_889]) ).
cnf(c_8269,plain,
inverse(greatest_lower_bound(A,identity)) = multiply(inverse(A),least_upper_bound(identity,A)),
inference(paramod,[status(thm)],[c_81,c_8268]) ).
cnf(c_8133,plain,
multiply(inverse(A),least_upper_bound(identity,A)) = inverse(greatest_lower_bound(A,identity)),
inference(copy,[status(thm)],[c_8269]) ).
cnf(c_8270,plain,
multiply(inverse(greatest_lower_bound(identity,a)),least_upper_bound(identity,multiply(greatest_lower_bound(identity,a),multiply(inverse(A),greatest_lower_bound(identity,A))))) != multiply(inverse(a),least_upper_bound(identity,a)),
inference(paramod,[status(thm)],[c_8132,c_7877]) ).
cnf(c_8271,plain,
multiply(inverse(greatest_lower_bound(identity,a)),identity) != multiply(inverse(a),least_upper_bound(identity,a)),
inference(paramod,[status(thm)],[c_2202,c_8270]) ).
cnf(c_8272,plain,
inverse(greatest_lower_bound(identity,a)) != multiply(inverse(a),least_upper_bound(identity,a)),
inference(paramod,[status(thm)],[c_81,c_8271]) ).
cnf(c_8273,plain,
inverse(greatest_lower_bound(identity,a)) != inverse(greatest_lower_bound(a,identity)),
inference(paramod,[status(thm)],[c_8133,c_8272]) ).
cnf(c_8274,plain,
inverse(greatest_lower_bound(identity,a)) != inverse(greatest_lower_bound(identity,a)),
inference(paramod,[status(thm)],[c_4,c_8273]) ).
cnf(c_8155,plain,
$false,
inference(copy,[status(thm)],[c_8274]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP179-2 : 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.44 % Computer : n014.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Fri Sep 25 14:34:32 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/0.45 % Process 436526 was started by sandbox on n014,
% 0.18/0.45 % Fri Sep 25 14:34:32 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.45
% 0.18/0.45 % From the command line: assign(max_seconds, 300).
% 90.42/13.06
% 90.42/13.06 % SZS status Unsatisfiable for theBenchmark
% 90.42/13.06
% 90.42/13.06 % Proof 1 at 3.57 (+ 0.91) seconds.
% 90.42/13.06 % Length of proof is 103.
% 90.42/13.06 % Level of proof is 16.
% 90.42/13.06 % Maximum clause weight is 100.000.
% 90.42/13.06 % Given clauses 326.
% 90.42/13.06
% 90.42/13.06 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------