%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : GRP178-2 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n011.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:20:20 AM UTC 2026
% Result : Unsatisfiable 217.53s 80.53s
% Output : Refutation 210.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 66
% Number of leaves : 20
% Syntax : Number of formulae : 935 ( 436 unt; 0 typ; 0 def)
% Number of atoms : 1575 (1574 equ; 0 cnn)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 8196 ( 869 ~; 640 |; 0 &;6687 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 10 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 1352 ( 0 ^;1352 !; 0 ?;1352 :)
% Comments :
%------------------------------------------------------------------------------
thf(greatest_lower_bound_decl,type,
greatest_lower_bound: $i > $i > $i ).
thf(a_decl,type,
a: $i ).
thf(multiply_decl,type,
multiply: $i > $i > $i ).
thf(b_decl,type,
b: $i ).
thf(c_decl,type,
c: $i ).
thf(least_upper_bound_decl,type,
least_upper_bound: $i > $i > $i ).
thf(identity_decl,type,
identity: $i ).
thf(inverse_decl,type,
inverse: $i > $i ).
thf(4,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= ( C @ ( B @ ( A @ least_upper_bound ) @ least_upper_bound ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_of_lub) ).
thf(28,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= ( C @ ( B @ ( A @ least_upper_bound ) @ least_upper_bound ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(29,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ least_upper_bound ) @ least_upper_bound ) )
= ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) ) ),
inference(lifteq,[status(thm)],[28]) ).
thf(11,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ greatest_lower_bound ) @ ( A @ least_upper_bound ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lub_absorbtion) ).
thf(42,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ greatest_lower_bound ) @ ( A @ least_upper_bound ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(43,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ greatest_lower_bound ) @ ( A @ least_upper_bound ) )
= A ),
inference(lifteq,[status(thm)],[42]) ).
thf(7,axiom,
( ( b @ ( a @ greatest_lower_bound ) )
= identity ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p09b_4) ).
thf(34,plain,
( ( b @ ( a @ greatest_lower_bound ) )
= identity ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(35,plain,
( ( b @ ( a @ greatest_lower_bound ) )
= identity ),
inference(lifteq,[status(thm)],[34]) ).
thf(235,plain,
! [B: $i,A: $i] :
( ( ( b @ ( a @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( identity @ ( A @ least_upper_bound ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[35,43]) ).
thf(236,plain,
( ( identity @ ( a @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[235:[bind(A,$thf( a )),bind(B,$thf( b ))]]) ).
thf(267,plain,
! [C: $i,B: $i,A: $i] :
( ( ( identity @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( C @ ( a @ least_upper_bound ) )
= ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[236,29]) ).
thf(268,plain,
! [A: $i] :
( ( A @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= ( A @ ( a @ least_upper_bound ) ) ),
inference(pattern_uni,[status(thm)],[267:[bind(A,$thf( a )),bind(B,$thf( identity ))]]) ).
thf(290,plain,
! [A: $i] :
( ( A @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= ( A @ ( a @ least_upper_bound ) ) ),
inference(simp,[status(thm)],[268]) ).
thf(381,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) @ ( A @ least_upper_bound ) )
!= ( C @ ( identity @ least_upper_bound ) ) )
| ( ( A @ ( a @ least_upper_bound ) )
= ( C @ ( a @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[43,290]) ).
thf(382,plain,
! [A: $i] :
( ( A @ ( identity @ greatest_lower_bound ) @ ( a @ least_upper_bound ) )
= ( identity @ ( a @ least_upper_bound ) ) ),
inference(pattern_uni,[status(thm)],[381:[bind(A,$thf( identity )),bind(B,$thf( E )),bind(C,$thf( E @ ( identity @ greatest_lower_bound ) ))]]) ).
thf(429,plain,
! [A: $i] :
( ( A @ ( identity @ greatest_lower_bound ) @ ( a @ least_upper_bound ) )
= ( identity @ ( a @ least_upper_bound ) ) ),
inference(simp,[status(thm)],[382]) ).
thf(432,plain,
! [A: $i] :
( ( A @ ( identity @ greatest_lower_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[429,236]) ).
thf(436,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ least_upper_bound ) @ least_upper_bound ) )
!= ( D @ ( identity @ greatest_lower_bound ) @ ( a @ least_upper_bound ) ) )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[29,432]) ).
thf(468,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C
!= ( D @ ( identity @ greatest_lower_bound ) ) )
| ( ( B @ ( A @ least_upper_bound ) )
!= a )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[436]) ).
thf(481,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ least_upper_bound ) )
!= a )
| ( ( C @ ( identity @ greatest_lower_bound ) @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[468]) ).
thf(13,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= ( C @ ( B @ ( A @ greatest_lower_bound ) @ greatest_lower_bound ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_of_glb) ).
thf(46,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= ( C @ ( B @ ( A @ greatest_lower_bound ) @ greatest_lower_bound ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(47,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ greatest_lower_bound ) @ greatest_lower_bound ) )
= ( C @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) ) ),
inference(lifteq,[status(thm)],[46]) ).
thf(915,plain,
! [C: $i,B: $i,A: $i] :
( ( ( b @ ( a @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( C @ ( identity @ greatest_lower_bound ) )
= ( C @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[35,47]) ).
thf(916,plain,
! [A: $i] :
( ( A @ ( identity @ greatest_lower_bound ) )
= ( A @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) ) ),
inference(pattern_uni,[status(thm)],[915:[bind(A,$thf( a )),bind(B,$thf( b ))]]) ).
thf(984,plain,
! [A: $i] :
( ( A @ ( identity @ greatest_lower_bound ) )
= ( A @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) ) ),
inference(simp,[status(thm)],[916]) ).
thf(39961,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ least_upper_bound ) )
!= a )
| ( ( C @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(rewrite,[status(thm)],[481,984]) ).
thf(2,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ least_upper_bound ) )
= ( A @ ( B @ least_upper_bound ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',symmetry_of_lub) ).
thf(24,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ least_upper_bound ) )
= ( A @ ( B @ least_upper_bound ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(25,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ least_upper_bound ) )
= ( A @ ( B @ least_upper_bound ) ) ),
inference(lifteq,[status(thm)],[24]) ).
thf(241,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) @ ( A @ least_upper_bound ) )
!= ( D @ ( C @ least_upper_bound ) ) )
| ( A
= ( C @ ( D @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[43,25]) ).
thf(242,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ greatest_lower_bound ) @ least_upper_bound ) )
= A ),
inference(pattern_uni,[status(thm)],[241:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( E )),bind(D,$thf( F @ ( E @ greatest_lower_bound ) ))]]) ).
thf(252,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ greatest_lower_bound ) @ least_upper_bound ) )
= A ),
inference(simp,[status(thm)],[242]) ).
thf(12,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ least_upper_bound ) @ ( A @ greatest_lower_bound ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',glb_absorbtion) ).
thf(44,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ least_upper_bound ) @ ( A @ greatest_lower_bound ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(45,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ least_upper_bound ) @ ( A @ greatest_lower_bound ) )
= A ),
inference(lifteq,[status(thm)],[44]) ).
thf(15,axiom,
( ( b @ ( identity @ greatest_lower_bound ) )
= identity ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p09b_2) ).
thf(50,plain,
( ( b @ ( identity @ greatest_lower_bound ) )
= identity ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(51,plain,
( ( b @ ( identity @ greatest_lower_bound ) )
= identity ),
inference(lifteq,[status(thm)],[50]) ).
thf(10,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ greatest_lower_bound ) @ multiply ) )
= ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ greatest_lower_bound ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',monotony_glb2) ).
thf(40,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ greatest_lower_bound ) @ multiply ) )
= ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ greatest_lower_bound ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(41,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ greatest_lower_bound ) @ multiply ) )
= ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ greatest_lower_bound ) ) ),
inference(lifteq,[status(thm)],[40]) ).
thf(510,plain,
! [C: $i,B: $i,A: $i] :
( ( ( b @ ( identity @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( C @ ( identity @ multiply ) )
= ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[51,41]) ).
thf(511,plain,
! [A: $i] :
( ( A @ ( b @ multiply ) @ ( A @ ( identity @ multiply ) @ greatest_lower_bound ) )
= ( A @ ( identity @ multiply ) ) ),
inference(pattern_uni,[status(thm)],[510:[bind(A,$thf( identity )),bind(B,$thf( b ))]]) ).
thf(541,plain,
! [A: $i] :
( ( A @ ( b @ multiply ) @ ( A @ ( identity @ multiply ) @ greatest_lower_bound ) )
= ( A @ ( identity @ multiply ) ) ),
inference(simp,[status(thm)],[511]) ).
thf(17,axiom,
! [A: $i] :
( ( A @ ( identity @ multiply ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_identity) ).
thf(54,plain,
! [A: $i] :
( ( A @ ( identity @ multiply ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(55,plain,
! [A: $i] :
( ( A @ ( identity @ multiply ) )
= A ),
inference(lifteq,[status(thm)],[54]) ).
thf(62679,plain,
! [A: $i] :
( ( A @ ( b @ multiply ) @ ( A @ greatest_lower_bound ) )
= A ),
inference(rewrite,[status(thm)],[541,55]) ).
thf(1,negated_conjecture,
( ( c @ ( b @ multiply ) @ ( a @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_p09b) ).
thf(21,plain,
( ( c @ ( b @ multiply ) @ ( a @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[1]) ).
thf(22,plain,
( ( c @ ( b @ multiply ) @ ( a @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) ),
inference(polarity_switch,[status(thm)],[21]) ).
thf(23,plain,
( ( c @ ( b @ multiply ) @ ( a @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) ),
inference(lifteq,[status(thm)],[22]) ).
thf(944,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ greatest_lower_bound ) @ greatest_lower_bound ) )
!= ( c @ ( b @ multiply ) @ ( a @ greatest_lower_bound ) ) )
| ( ( C @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[47,23]) ).
thf(967,plain,
! [C: $i,B: $i,A: $i] :
( ( C
!= ( c @ ( b @ multiply ) ) )
| ( ( B @ ( A @ greatest_lower_bound ) )
!= a )
| ( ( C @ ( B @ greatest_lower_bound ) )
!= c )
| ( A != a ) ),
inference(simp,[status(thm)],[944]) ).
thf(977,plain,
! [A: $i] :
( ( ( A @ ( a @ greatest_lower_bound ) )
!= a )
| ( ( c @ ( b @ multiply ) @ ( A @ greatest_lower_bound ) )
!= c ) ),
inference(simp,[status(thm)],[967]) ).
thf(150596,plain,
! [B: $i,A: $i] :
( ( ( A @ ( b @ multiply ) @ ( A @ greatest_lower_bound ) )
!= ( c @ ( b @ multiply ) @ ( B @ greatest_lower_bound ) ) )
| ( ( B @ ( a @ greatest_lower_bound ) )
!= a )
| ( A != c ) ),
inference(paramod_ordered,[status(thm)],[62679,977]) ).
thf(150597,plain,
( ( ( c @ ( a @ greatest_lower_bound ) )
!= a )
| ( c != c ) ),
inference(pattern_uni,[status(thm)],[150596:[bind(A,$thf( c )),bind(B,$thf( c ))]]) ).
thf(150839,plain,
( ( c @ ( a @ greatest_lower_bound ) )
!= a ),
inference(simp,[status(thm)],[150597]) ).
thf(151022,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ least_upper_bound ) @ ( A @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) )
| ( A != a ) ),
inference(paramod_ordered,[status(thm)],[45,150839]) ).
thf(151105,plain,
! [A: $i] :
( ( ( A @ ( a @ least_upper_bound ) )
!= c )
| ( a != a ) ),
inference(simp,[status(thm)],[151022]) ).
thf(151184,plain,
! [A: $i] :
( ( A @ ( a @ least_upper_bound ) )
!= c ),
inference(simp,[status(thm)],[151105]) ).
thf(158348,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ greatest_lower_bound ) @ least_upper_bound ) )
!= ( C @ ( a @ least_upper_bound ) ) )
| ( A != c ) ),
inference(paramod_ordered,[status(thm)],[252,151184]) ).
thf(158491,plain,
! [B: $i,A: $i] :
( ( c != B )
| ( ( A @ ( c @ greatest_lower_bound ) )
!= a ) ),
inference(simp,[status(thm)],[158348]) ).
thf(158533,plain,
! [A: $i] :
( ( A @ ( c @ greatest_lower_bound ) )
!= a ),
inference(simp,[status(thm)],[158491]) ).
thf(3,axiom,
! [A: $i] :
( ( A @ ( A @ least_upper_bound ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',idempotence_of_lub) ).
thf(26,plain,
! [A: $i] :
( ( A @ ( A @ least_upper_bound ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(27,plain,
! [A: $i] :
( ( A @ ( A @ least_upper_bound ) )
= A ),
inference(lifteq,[status(thm)],[26]) ).
thf(194,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ least_upper_bound ) @ least_upper_bound ) )
!= ( D @ ( D @ least_upper_bound ) ) )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= D ) ),
inference(paramod_ordered,[status(thm)],[29,27]) ).
thf(195,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ least_upper_bound ) @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= ( B @ ( A @ least_upper_bound ) ) ),
inference(pattern_uni,[status(thm)],[194:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( H @ ( G @ least_upper_bound ) )),bind(D,$thf( H @ ( G @ least_upper_bound ) ))]]) ).
thf(214,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ least_upper_bound ) @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= ( B @ ( A @ least_upper_bound ) ) ),
inference(simp,[status(thm)],[195]) ).
thf(6494,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( a @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= ( B @ ( A @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[236,214]) ).
thf(6495,plain,
( ( a @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= ( identity @ ( a @ least_upper_bound ) ) ),
inference(pattern_uni,[status(thm)],[6494:[bind(A,$thf( a )),bind(B,$thf( identity ))]]) ).
thf(8704,plain,
( ( a @ ( a @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[6495,290,236]) ).
thf(372,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( C @ ( B @ least_upper_bound ) ) )
| ( ( D @ ( A @ ( a @ least_upper_bound ) @ least_upper_bound ) )
= ( D @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[290,29]) ).
thf(373,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( a @ least_upper_bound ) @ least_upper_bound ) )
= ( A @ ( B @ ( identity @ least_upper_bound ) @ least_upper_bound ) @ ( a @ least_upper_bound ) ) ),
inference(pattern_uni,[status(thm)],[372:[bind(A,$thf( F )),bind(B,$thf( a )),bind(C,$thf( F @ ( identity @ least_upper_bound ) )),bind(D,$thf( D ))]]) ).
thf(421,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( a @ least_upper_bound ) @ least_upper_bound ) )
= ( A @ ( B @ ( identity @ least_upper_bound ) @ least_upper_bound ) @ ( a @ least_upper_bound ) ) ),
inference(simp,[status(thm)],[373]) ).
thf(192,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ least_upper_bound ) @ least_upper_bound ) )
!= ( E @ ( D @ least_upper_bound ) ) )
| ( ( F @ ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) @ least_upper_bound ) )
= ( F @ ( E @ least_upper_bound ) @ ( D @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[29,29]) ).
thf(193,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( D @ least_upper_bound ) @ ( C @ least_upper_bound ) @ least_upper_bound ) )
= ( B @ ( A @ least_upper_bound ) @ ( D @ ( C @ least_upper_bound ) @ least_upper_bound ) ) ),
inference(pattern_uni,[status(thm)],[192:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( G @ least_upper_bound ) )),bind(E,$thf( C ))]]) ).
thf(212,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( D @ least_upper_bound ) @ ( C @ least_upper_bound ) @ least_upper_bound ) )
= ( B @ ( A @ least_upper_bound ) @ ( D @ ( C @ least_upper_bound ) @ least_upper_bound ) ) ),
inference(simp,[status(thm)],[193]) ).
thf(4926,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( D @ least_upper_bound ) @ least_upper_bound ) @ ( C @ least_upper_bound ) )
= ( B @ ( A @ least_upper_bound ) @ ( D @ least_upper_bound ) @ ( C @ least_upper_bound ) ) ),
inference(rewrite,[status(thm)],[212,29]) ).
thf(33115,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ least_upper_bound ) @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= ( A @ ( B @ least_upper_bound ) @ ( a @ least_upper_bound ) ) ),
inference(rewrite,[status(thm)],[421,29,4926]) ).
thf(33255,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( a @ least_upper_bound ) )
!= ( A @ ( B @ least_upper_bound ) ) )
| ( ( a @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= ( A @ ( B @ least_upper_bound ) @ ( a @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[236,33115]) ).
thf(33256,plain,
( ( a @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= ( identity @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) ) ),
inference(pattern_uni,[status(thm)],[33255:[bind(A,$thf( identity )),bind(B,$thf( a ))]]) ).
thf(198,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ least_upper_bound ) )
!= ( C @ ( B @ least_upper_bound ) ) )
| ( ( D @ ( A @ least_upper_bound ) )
= ( D @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[27,29]) ).
thf(199,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= ( B @ ( A @ least_upper_bound ) ) ),
inference(pattern_uni,[status(thm)],[198:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(217,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= ( B @ ( A @ least_upper_bound ) ) ),
inference(simp,[status(thm)],[199]) ).
thf(35360,plain,
( ( identity @ ( a @ least_upper_bound ) )
= ( a @ ( a @ least_upper_bound ) ) ),
inference(rewrite,[status(thm)],[33256,290,217]) ).
thf(35485,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( a @ ( a @ least_upper_bound ) @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= ( B @ ( A @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[35360,214]) ).
thf(35486,plain,
( ( a @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= ( identity @ ( a @ least_upper_bound ) ) ),
inference(pattern_uni,[status(thm)],[35485:[bind(A,$thf( a )),bind(B,$thf( identity ))]]) ).
thf(41009,plain,
( ( a @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= ( a @ ( a @ least_upper_bound ) ) ),
inference(rewrite,[status(thm)],[35486,35360,33115]) ).
thf(41035,plain,
! [B: $i,A: $i] :
( ( ( a @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( a @ ( a @ least_upper_bound ) )
= ( A @ ( B @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[41009,25]) ).
thf(41036,plain,
( ( a @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) )
= ( a @ ( a @ least_upper_bound ) ) ),
inference(pattern_uni,[status(thm)],[41035:[bind(A,$thf( a )),bind(B,$thf( a @ ( a @ least_upper_bound ) ))]]) ).
thf(41990,plain,
( ( a @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[41036,8704,29]) ).
thf(269,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ least_upper_bound ) @ least_upper_bound ) )
!= ( identity @ ( a @ least_upper_bound ) ) )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[29,236]) ).
thf(280,plain,
! [C: $i,B: $i,A: $i] :
( ( C != identity )
| ( ( B @ ( A @ least_upper_bound ) )
!= a )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[269]) ).
thf(286,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ least_upper_bound ) )
!= a )
| ( ( identity @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[280]) ).
thf(42128,plain,
! [B: $i,A: $i] :
( ( ( a @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( a != a )
| ( ( identity @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[41990,286]) ).
thf(42129,plain,
! [B: $i,A: $i] :
( ( ( a @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( identity @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[42128]) ).
thf(42130,plain,
( ( identity @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[42129:[bind(A,$thf( a )),bind(B,$thf( a @ ( a @ least_upper_bound ) ))]]) ).
thf(42517,plain,
( ( identity @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[42130,4926]) ).
thf(42550,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[42517,25]) ).
thf(42551,plain,
( ( a @ ( identity @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[42550:[bind(A,$thf( a )),bind(B,$thf( identity @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) ))]]) ).
thf(45124,plain,
( ( a @ ( identity @ ( a @ least_upper_bound ) @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[42551,29]) ).
thf(45154,plain,
! [B: $i,A: $i] :
( ( ( a @ ( identity @ ( a @ least_upper_bound ) @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[45124,25]) ).
thf(45155,plain,
( ( a @ ( a @ ( identity @ ( a @ least_upper_bound ) @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[45154:[bind(A,$thf( a )),bind(B,$thf( a @ ( identity @ ( a @ least_upper_bound ) @ least_upper_bound ) ))]]) ).
thf(47373,plain,
( ( a @ ( a @ least_upper_bound ) @ ( identity @ ( a @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[45155,29]) ).
thf(47486,plain,
( ( ( a @ ( a @ least_upper_bound ) )
!= ( a @ ( a @ least_upper_bound ) ) )
| ( ( a @ ( identity @ ( a @ least_upper_bound ) @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[8704,47373]) ).
thf(47487,plain,
( ( a @ ( identity @ ( a @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[47486:[]]) ).
thf(48084,plain,
( ( a @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[47487,29]) ).
thf(48110,plain,
! [B: $i,A: $i] :
( ( ( a @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[48084,25]) ).
thf(48111,plain,
( ( a @ ( a @ ( identity @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[48110:[bind(A,$thf( a )),bind(B,$thf( a @ ( identity @ least_upper_bound ) ))]]) ).
thf(49465,plain,
( ( a @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[48111,29]) ).
thf(49491,plain,
! [B: $i,A: $i] :
( ( ( a @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[49465,25]) ).
thf(49492,plain,
( ( identity @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[49491:[bind(A,$thf( identity )),bind(B,$thf( a @ ( a @ least_upper_bound ) ))]]) ).
thf(50361,plain,
( ( identity @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[49492,29]) ).
thf(50519,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( a != a )
| ( ( identity @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[50361,286]) ).
thf(50520,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( identity @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[50519]) ).
thf(50521,plain,
( ( identity @ ( identity @ ( a @ least_upper_bound ) @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[50520:[bind(A,$thf( a )),bind(B,$thf( identity @ ( a @ least_upper_bound ) ))]]) ).
thf(58446,plain,
( ( identity @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[50521,4926]) ).
thf(58480,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[58446,25]) ).
thf(58481,plain,
( ( a @ ( identity @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[58480:[bind(A,$thf( a )),bind(B,$thf( identity @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) ))]]) ).
thf(71612,plain,
( ( a @ ( identity @ ( identity @ least_upper_bound ) @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[58481,29]) ).
thf(71661,plain,
! [B: $i,A: $i] :
( ( ( a @ ( identity @ ( identity @ least_upper_bound ) @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[71612,25]) ).
thf(71662,plain,
( ( a @ ( a @ ( identity @ ( identity @ least_upper_bound ) @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[71661:[bind(A,$thf( a )),bind(B,$thf( a @ ( identity @ ( identity @ least_upper_bound ) @ least_upper_bound ) ))]]) ).
thf(86331,plain,
( ( a @ ( a @ least_upper_bound ) @ ( identity @ ( identity @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[71662,29]) ).
thf(86491,plain,
( ( ( a @ ( a @ least_upper_bound ) )
!= ( a @ ( a @ least_upper_bound ) ) )
| ( ( a @ ( identity @ ( identity @ least_upper_bound ) @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[8704,86331]) ).
thf(86492,plain,
( ( a @ ( identity @ ( identity @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[86491:[]]) ).
thf(87389,plain,
( ( a @ ( identity @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[86492,29]) ).
thf(87619,plain,
! [B: $i,A: $i] :
( ( ( a @ ( identity @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( a != a )
| ( ( identity @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[87389,286]) ).
thf(87620,plain,
! [B: $i,A: $i] :
( ( ( a @ ( identity @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( identity @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[87619]) ).
thf(87621,plain,
( ( identity @ ( a @ ( identity @ least_upper_bound ) @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[87620:[bind(A,$thf( identity )),bind(B,$thf( a @ ( identity @ least_upper_bound ) ))]]) ).
thf(117134,plain,
( ( identity @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[87621,4926]) ).
thf(8,axiom,
! [A: $i] :
( ( A @ ( A @ greatest_lower_bound ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',idempotence_of_gld) ).
thf(36,plain,
! [A: $i] :
( ( A @ ( A @ greatest_lower_bound ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(37,plain,
! [A: $i] :
( ( A @ ( A @ greatest_lower_bound ) )
= A ),
inference(lifteq,[status(thm)],[36]) ).
thf(947,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ greatest_lower_bound ) @ greatest_lower_bound ) )
!= ( b @ ( identity @ greatest_lower_bound ) ) )
| ( ( C @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[51,47]) ).
thf(962,plain,
! [C: $i,B: $i,A: $i] :
( ( C != b )
| ( ( B @ ( A @ greatest_lower_bound ) )
!= identity )
| ( ( C @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= identity ) ),
inference(simp,[status(thm)],[947]) ).
thf(972,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= identity )
| ( ( b @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= identity ) ),
inference(simp,[status(thm)],[962]) ).
thf(131994,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ greatest_lower_bound ) )
!= ( C @ ( B @ greatest_lower_bound ) ) )
| ( A != identity )
| ( ( b @ ( C @ greatest_lower_bound ) @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[37,972]) ).
thf(131995,plain,
! [A: $i] :
( ( A != identity )
| ( ( b @ ( A @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= identity ) ),
inference(pattern_uni,[status(thm)],[131994:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(133288,plain,
( ( b @ ( identity @ greatest_lower_bound ) @ ( identity @ greatest_lower_bound ) )
= identity ),
inference(simp,[status(thm)],[131995]) ).
thf(138007,plain,
( ( b @ ( identity @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[133288,984]) ).
thf(704,plain,
! [B: $i,A: $i] :
( ( ( b @ ( a @ greatest_lower_bound ) )
!= ( B @ ( A @ least_upper_bound ) @ ( A @ greatest_lower_bound ) ) )
| ( identity = A ) ),
inference(paramod_ordered,[status(thm)],[35,45]) ).
thf(738,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ least_upper_bound ) )
!= b )
| ( a != A )
| ( identity = A ) ),
inference(simp,[status(thm)],[704]) ).
thf(757,plain,
! [A: $i] :
( ( ( A @ ( a @ least_upper_bound ) )
!= b )
| ( identity = a ) ),
inference(simp,[status(thm)],[738]) ).
thf(16,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ greatest_lower_bound ) )
= ( A @ ( B @ greatest_lower_bound ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',symmetry_of_glb) ).
thf(52,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ greatest_lower_bound ) )
= ( A @ ( B @ greatest_lower_bound ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(53,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ greatest_lower_bound ) )
= ( A @ ( B @ greatest_lower_bound ) ) ),
inference(lifteq,[status(thm)],[52]) ).
thf(6,axiom,
( ( c @ ( identity @ greatest_lower_bound ) )
= identity ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p09b_3) ).
thf(32,plain,
( ( c @ ( identity @ greatest_lower_bound ) )
= identity ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(33,plain,
( ( c @ ( identity @ greatest_lower_bound ) )
= identity ),
inference(lifteq,[status(thm)],[32]) ).
thf(1156,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= ( c @ ( identity @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[53,33]) ).
thf(1157,plain,
( ( identity @ ( c @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[1156:[bind(A,$thf( identity )),bind(B,$thf( c ))]]) ).
thf(1307,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( c @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( identity @ ( A @ least_upper_bound ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[1157,43]) ).
thf(1308,plain,
( ( identity @ ( c @ least_upper_bound ) )
= c ),
inference(pattern_uni,[status(thm)],[1307:[bind(A,$thf( c )),bind(B,$thf( identity ))]]) ).
thf(1989,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( c @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= c ) ),
inference(paramod_ordered,[status(thm)],[1308,25]) ).
thf(1990,plain,
( ( c @ ( identity @ least_upper_bound ) )
= c ),
inference(pattern_uni,[status(thm)],[1989:[bind(A,$thf( c )),bind(B,$thf( identity ))]]) ).
thf(158409,plain,
! [A: $i] :
( ( ( c @ ( identity @ least_upper_bound ) )
!= ( A @ ( a @ least_upper_bound ) ) )
| ( c != c ) ),
inference(paramod_ordered,[status(thm)],[1990,151184]) ).
thf(158410,plain,
! [A: $i] :
( ( c @ ( identity @ least_upper_bound ) )
!= ( A @ ( a @ least_upper_bound ) ) ),
inference(simp,[status(thm)],[158409]) ).
thf(158460,plain,
! [A: $i] :
( ( c != A )
| ( identity != a ) ),
inference(simp,[status(thm)],[158410]) ).
thf(158581,plain,
identity != a,
inference(simp,[status(thm)],[158460]) ).
thf(158583,plain,
! [A: $i] :
( ( A @ ( a @ least_upper_bound ) )
!= b ),
inference(simplifyReflect,[status(thm)],[757,158581]) ).
thf(5,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ greatest_lower_bound ) @ ( A @ multiply ) )
= ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ greatest_lower_bound ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',monotony_glb1) ).
thf(30,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ greatest_lower_bound ) @ ( A @ multiply ) )
= ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ greatest_lower_bound ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(31,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ greatest_lower_bound ) @ ( A @ multiply ) )
= ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ greatest_lower_bound ) ) ),
inference(lifteq,[status(thm)],[30]) ).
thf(89,plain,
( ( ( c @ ( b @ multiply ) @ ( a @ greatest_lower_bound ) )
!= ( b @ ( a @ greatest_lower_bound ) ) )
| ( ( c @ ( a @ greatest_lower_bound ) )
!= identity ) ),
inference(paramod_ordered,[status(thm)],[35,23]) ).
thf(92,plain,
( ( ( c @ ( b @ multiply ) )
!= b )
| ( a != a )
| ( ( c @ ( a @ greatest_lower_bound ) )
!= identity ) ),
inference(simp,[status(thm)],[89]) ).
thf(96,plain,
( ( ( c @ ( b @ multiply ) )
!= b )
| ( ( c @ ( a @ greatest_lower_bound ) )
!= identity ) ),
inference(simp,[status(thm)],[92]) ).
thf(167,plain,
( ( ( c @ ( a @ greatest_lower_bound ) )
!= ( b @ ( a @ greatest_lower_bound ) ) )
| ( ( c @ ( b @ multiply ) )
!= b )
| ( identity != identity ) ),
inference(paramod_ordered,[status(thm)],[35,96]) ).
thf(168,plain,
( ( ( c @ ( a @ greatest_lower_bound ) )
!= ( b @ ( a @ greatest_lower_bound ) ) )
| ( ( c @ ( b @ multiply ) )
!= b ) ),
inference(simp,[status(thm)],[167]) ).
thf(180,plain,
( ( c != b )
| ( a != a )
| ( ( c @ ( b @ multiply ) )
!= b ) ),
inference(simp,[status(thm)],[168]) ).
thf(182,plain,
( ( c != b )
| ( ( c @ ( b @ multiply ) )
!= b ) ),
inference(simp,[status(thm)],[180]) ).
thf(307,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ greatest_lower_bound ) @ ( A @ multiply ) )
!= ( c @ ( b @ multiply ) ) )
| ( c != b )
| ( ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ greatest_lower_bound ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[31,182]) ).
thf(319,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ greatest_lower_bound ) )
!= c )
| ( A != b )
| ( c != b )
| ( ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ greatest_lower_bound ) )
!= b ) ),
inference(simp,[status(thm)],[307]) ).
thf(333,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= c )
| ( c != b )
| ( ( B @ ( b @ multiply ) @ ( A @ ( b @ multiply ) @ greatest_lower_bound ) )
!= b ) ),
inference(simp,[status(thm)],[319]) ).
thf(223,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) @ ( A @ least_upper_bound ) )
!= ( E @ ( D @ ( C @ least_upper_bound ) @ least_upper_bound ) ) )
| ( A
= ( E @ ( D @ least_upper_bound ) @ ( C @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[43,29]) ).
thf(224,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ ( B @ least_upper_bound ) @ greatest_lower_bound ) @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) )
= ( C @ ( B @ least_upper_bound ) ) ),
inference(pattern_uni,[status(thm)],[223:[bind(A,$thf( K @ ( J @ least_upper_bound ) )),bind(B,$thf( I )),bind(C,$thf( J )),bind(D,$thf( K )),bind(E,$thf( I @ ( K @ ( J @ least_upper_bound ) @ greatest_lower_bound ) ))]]) ).
thf(249,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ ( B @ least_upper_bound ) @ greatest_lower_bound ) @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) )
= ( C @ ( B @ least_upper_bound ) ) ),
inference(simp,[status(thm)],[224]) ).
thf(300,plain,
! [C: $i,B: $i,A: $i] :
( ( ( b @ ( a @ greatest_lower_bound ) )
!= ( C @ ( B @ greatest_lower_bound ) ) )
| ( ( identity @ ( A @ multiply ) )
= ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[35,31]) ).
thf(301,plain,
! [A: $i] :
( ( identity @ ( A @ multiply ) )
= ( b @ ( A @ multiply ) @ ( a @ ( A @ multiply ) @ greatest_lower_bound ) ) ),
inference(pattern_uni,[status(thm)],[300:[bind(A,$thf( A )),bind(B,$thf( a )),bind(C,$thf( b ))]]) ).
thf(9,axiom,
! [A: $i] :
( ( A @ ( A @ inverse @ multiply ) )
= identity ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_inverse) ).
thf(38,plain,
! [A: $i] :
( ( A @ ( A @ inverse @ multiply ) )
= identity ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(39,plain,
! [A: $i] :
( ( A @ ( A @ inverse @ multiply ) )
= identity ),
inference(lifteq,[status(thm)],[38]) ).
thf(14059,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( A @ multiply ) )
!= ( B @ ( B @ inverse @ multiply ) ) )
| ( ( b @ ( A @ multiply ) @ ( a @ ( A @ multiply ) @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[301,39]) ).
thf(14060,plain,
( ( b @ ( identity @ inverse @ multiply ) @ ( a @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[14059:[bind(A,$thf( identity @ inverse )),bind(B,$thf( identity ))]]) ).
thf(17136,plain,
! [B: $i,A: $i] :
( ( ( b @ ( identity @ inverse @ multiply ) @ ( a @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[14060,53]) ).
thf(17137,plain,
( ( a @ ( identity @ inverse @ multiply ) @ ( b @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[17136:[bind(A,$thf( a @ ( identity @ inverse @ multiply ) )),bind(B,$thf( b @ ( identity @ inverse @ multiply ) ))]]) ).
thf(26968,plain,
! [B: $i,A: $i] :
( ( ( a @ ( identity @ inverse @ multiply ) @ ( b @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( A @ ( identity @ least_upper_bound ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[17137,252]) ).
thf(26969,plain,
( ( b @ ( identity @ inverse @ multiply ) @ ( identity @ least_upper_bound ) )
= ( b @ ( identity @ inverse @ multiply ) ) ),
inference(pattern_uni,[status(thm)],[26968:[bind(A,$thf( b @ ( identity @ inverse @ multiply ) )),bind(B,$thf( a @ ( identity @ inverse @ multiply ) ))]]) ).
thf(28598,plain,
! [B: $i,A: $i] :
( ( ( b @ ( identity @ inverse @ multiply ) @ ( identity @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( b @ ( identity @ inverse @ multiply ) @ ( A @ greatest_lower_bound ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[26969,45]) ).
thf(28599,plain,
( ( b @ ( identity @ inverse @ multiply ) @ ( identity @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[28598:[bind(A,$thf( identity )),bind(B,$thf( b @ ( identity @ inverse @ multiply ) ))]]) ).
thf(28853,plain,
( ( b @ ( identity @ inverse @ multiply ) @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[28599,984]) ).
thf(28967,plain,
! [B: $i,A: $i] :
( ( ( b @ ( identity @ inverse @ multiply ) @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[28853,53]) ).
thf(28968,plain,
( ( a @ ( b @ ( identity @ inverse @ multiply ) @ ( b @ greatest_lower_bound ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[28967:[bind(A,$thf( a )),bind(B,$thf( b @ ( identity @ inverse @ multiply ) @ ( b @ greatest_lower_bound ) ))]]) ).
thf(29532,plain,
( ( a @ ( b @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[28968,47]) ).
thf(29658,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= ( a @ ( b @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[53,29532]) ).
thf(29659,plain,
( ( b @ ( identity @ inverse @ multiply ) @ ( a @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[29658:[bind(A,$thf( b @ ( identity @ inverse @ multiply ) )),bind(B,$thf( a ))]]) ).
thf(31463,plain,
! [B: $i,A: $i] :
( ( ( b @ ( identity @ inverse @ multiply ) @ ( a @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[29659,53]) ).
thf(31464,plain,
( ( b @ ( b @ ( identity @ inverse @ multiply ) @ ( a @ greatest_lower_bound ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[31463:[bind(A,$thf( b )),bind(B,$thf( b @ ( identity @ inverse @ multiply ) @ ( a @ greatest_lower_bound ) ))]]) ).
thf(31931,plain,
( ( b @ ( b @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[31464,47]) ).
thf(32056,plain,
! [B: $i,A: $i] :
( ( ( b @ ( b @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[31931,53]) ).
thf(32057,plain,
( ( a @ ( b @ ( b @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[32056:[bind(A,$thf( a )),bind(B,$thf( b @ ( b @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) ))]]) ).
thf(32522,plain,
( ( a @ ( b @ greatest_lower_bound ) @ ( b @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[32057,47]) ).
thf(208,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ least_upper_bound ) )
!= ( E @ ( D @ ( C @ least_upper_bound ) @ least_upper_bound ) ) )
| ( ( B @ ( A @ least_upper_bound ) )
= ( E @ ( D @ least_upper_bound ) @ ( C @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[25,29]) ).
thf(209,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= ( A @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) ) ),
inference(pattern_uni,[status(thm)],[208:[bind(A,$thf( A )),bind(B,$thf( G @ ( F @ least_upper_bound ) )),bind(C,$thf( F )),bind(D,$thf( G )),bind(E,$thf( A ))]]) ).
thf(213,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= ( A @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) ) ),
inference(simp,[status(thm)],[209]) ).
thf(42730,plain,
! [C: $i,B: $i,A: $i] :
( ( ( identity @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( A @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) ) )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[42517,213]) ).
thf(42731,plain,
( ( a @ ( a @ least_upper_bound ) @ ( identity @ ( a @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[42730:[bind(A,$thf( identity @ ( a @ least_upper_bound ) )),bind(B,$thf( a )),bind(C,$thf( a ))]]) ).
thf(45799,plain,
( ( a @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[42731,29]) ).
thf(45829,plain,
! [B: $i,A: $i] :
( ( ( a @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[45799,25]) ).
thf(45830,plain,
( ( a @ ( a @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[45829:[bind(A,$thf( a )),bind(B,$thf( a @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) ))]]) ).
thf(53029,plain,
( ( a @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[45830,29]) ).
thf(379,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ least_upper_bound ) )
!= ( B @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) ) )
| ( A
= ( B @ ( a @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[27,290]) ).
thf(402,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ ( identity @ least_upper_bound ) ) )
| ( A != a )
| ( A
= ( B @ ( a @ least_upper_bound ) ) ) ),
inference(simp,[status(thm)],[379]) ).
thf(418,plain,
! [A: $i] :
( ( ( A @ ( identity @ least_upper_bound ) )
!= a )
| ( ( A @ ( a @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[402]) ).
thf(53344,plain,
! [A: $i] :
( ( ( a @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
!= ( A @ ( identity @ least_upper_bound ) ) )
| ( a != a )
| ( ( A @ ( a @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[53029,418]) ).
thf(53345,plain,
! [A: $i] :
( ( ( a @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
!= ( A @ ( identity @ least_upper_bound ) ) )
| ( ( A @ ( a @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[53344]) ).
thf(53346,plain,
( ( a @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[53345:[bind(A,$thf( a @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) ))]]) ).
thf(63709,plain,
( ( a @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[53346,4926]) ).
thf(63750,plain,
! [B: $i,A: $i] :
( ( ( a @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[63709,25]) ).
thf(63751,plain,
( ( a @ ( a @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[63750:[bind(A,$thf( a )),bind(B,$thf( a @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) ))]]) ).
thf(77651,plain,
( ( a @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[63751,29]) ).
thf(77700,plain,
! [B: $i,A: $i] :
( ( ( a @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[77651,25]) ).
thf(77701,plain,
( ( a @ ( a @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[77700:[bind(A,$thf( a )),bind(B,$thf( a @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) ))]]) ).
thf(98395,plain,
( ( a @ ( a @ least_upper_bound ) @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[77701,29]) ).
thf(86,plain,
( ( ( c @ ( b @ multiply ) )
!= c )
| ( a != a ) ),
inference(simp,[status(thm)],[23]) ).
thf(95,plain,
( ( c @ ( b @ multiply ) )
!= c ),
inference(simp,[status(thm)],[86]) ).
thf(110,plain,
! [A: $i] :
( ( ( A @ ( A @ inverse @ multiply ) )
!= ( c @ ( b @ multiply ) ) )
| ( identity != c ) ),
inference(paramod_ordered,[status(thm)],[39,95]) ).
thf(114,plain,
! [A: $i] :
( ( A != c )
| ( ( A @ inverse )
!= b )
| ( identity != c ) ),
inference(simp,[status(thm)],[110]) ).
thf(120,plain,
( ( ( c @ inverse )
!= b )
| ( identity != c ) ),
inference(simp,[status(thm)],[114]) ).
thf(274,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[236,25]) ).
thf(275,plain,
( ( a @ ( identity @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[274:[bind(A,$thf( a )),bind(B,$thf( identity ))]]) ).
thf(337,plain,
! [C: $i,B: $i,A: $i] :
( ( ( a @ ( identity @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( C @ ( a @ least_upper_bound ) )
= ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[275,29]) ).
thf(338,plain,
! [A: $i] :
( ( A @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
= ( A @ ( a @ least_upper_bound ) ) ),
inference(pattern_uni,[status(thm)],[337:[bind(A,$thf( identity )),bind(B,$thf( a ))]]) ).
thf(362,plain,
! [A: $i] :
( ( A @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
= ( A @ ( a @ least_upper_bound ) ) ),
inference(simp,[status(thm)],[338]) ).
thf(610,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ least_upper_bound ) @ least_upper_bound ) )
!= ( D @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) ) )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= ( D @ ( a @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[29,362]) ).
thf(662,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C
!= ( D @ ( a @ least_upper_bound ) ) )
| ( ( B @ ( A @ least_upper_bound ) )
!= identity )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= ( D @ ( a @ least_upper_bound ) ) ) ),
inference(simp,[status(thm)],[610]) ).
thf(677,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ least_upper_bound ) )
!= identity )
| ( ( C @ ( a @ least_upper_bound ) @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= ( C @ ( a @ least_upper_bound ) ) ) ),
inference(simp,[status(thm)],[662]) ).
thf(725,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
!= ( C @ ( B @ least_upper_bound ) ) )
| ( ( A @ ( a @ least_upper_bound ) @ ( B @ greatest_lower_bound ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[362,45]) ).
thf(726,plain,
! [A: $i] :
( ( A @ ( a @ least_upper_bound ) @ ( identity @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[725:[bind(A,$thf( E )),bind(B,$thf( identity )),bind(C,$thf( E @ ( a @ least_upper_bound ) ))]]) ).
thf(753,plain,
! [A: $i] :
( ( A @ ( a @ least_upper_bound ) @ ( identity @ greatest_lower_bound ) )
= identity ),
inference(simp,[status(thm)],[726]) ).
thf(1168,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( a @ least_upper_bound ) @ ( identity @ greatest_lower_bound ) )
!= ( C @ ( B @ greatest_lower_bound ) ) )
| ( ( B @ ( C @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[753,53]) ).
thf(1169,plain,
! [A: $i] :
( ( identity @ ( A @ ( a @ least_upper_bound ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[1168:[bind(A,$thf( E )),bind(B,$thf( identity )),bind(C,$thf( E @ ( a @ least_upper_bound ) ))]]) ).
thf(1200,plain,
! [A: $i] :
( ( identity @ ( A @ ( a @ least_upper_bound ) @ greatest_lower_bound ) )
= identity ),
inference(simp,[status(thm)],[1169]) ).
thf(3795,plain,
( ( c @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[33,984]) ).
thf(3903,plain,
! [B: $i,A: $i] :
( ( ( c @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[3795,53]) ).
thf(3904,plain,
( ( a @ ( c @ ( b @ greatest_lower_bound ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[3903:[bind(A,$thf( a )),bind(B,$thf( c @ ( b @ greatest_lower_bound ) ))]]) ).
thf(4030,plain,
( ( a @ ( c @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[3904,47]) ).
thf(4042,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= ( a @ ( c @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[53,4030]) ).
thf(4043,plain,
( ( c @ ( a @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[4042:[bind(A,$thf( c )),bind(B,$thf( a ))]]) ).
thf(117202,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[117134,25]) ).
thf(117203,plain,
( ( identity @ ( identity @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[117202:[bind(A,$thf( identity )),bind(B,$thf( identity @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) ))]]) ).
thf(143991,plain,
( ( identity @ ( identity @ ( a @ least_upper_bound ) @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[117203,29]) ).
thf(498,plain,
! [C: $i,B: $i,A: $i] :
( ( ( c @ ( identity @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( C @ ( identity @ multiply ) )
= ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[33,41]) ).
thf(499,plain,
! [A: $i] :
( ( A @ ( c @ multiply ) @ ( A @ ( identity @ multiply ) @ greatest_lower_bound ) )
= ( A @ ( identity @ multiply ) ) ),
inference(pattern_uni,[status(thm)],[498:[bind(A,$thf( identity )),bind(B,$thf( c ))]]) ).
thf(537,plain,
! [A: $i] :
( ( A @ ( c @ multiply ) @ ( A @ ( identity @ multiply ) @ greatest_lower_bound ) )
= ( A @ ( identity @ multiply ) ) ),
inference(simp,[status(thm)],[499]) ).
thf(57665,plain,
! [A: $i] :
( ( A @ ( c @ multiply ) @ ( A @ greatest_lower_bound ) )
= A ),
inference(rewrite,[status(thm)],[537,55]) ).
thf(27114,plain,
! [B: $i,A: $i] :
( ( ( a @ ( identity @ inverse @ multiply ) @ ( b @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( identity @ ( A @ least_upper_bound ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[17137,43]) ).
thf(27115,plain,
( ( identity @ ( b @ ( identity @ inverse @ multiply ) @ least_upper_bound ) )
= ( b @ ( identity @ inverse @ multiply ) ) ),
inference(pattern_uni,[status(thm)],[27114:[bind(A,$thf( b @ ( identity @ inverse @ multiply ) )),bind(B,$thf( a @ ( identity @ inverse @ multiply ) ))]]) ).
thf(18,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ multiply ) @ multiply ) )
= ( C @ ( B @ multiply ) @ ( A @ multiply ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity) ).
thf(56,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ multiply ) @ multiply ) )
= ( C @ ( B @ multiply ) @ ( A @ multiply ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(113,plain,
! [A: $i] :
( ( ( A @ ( A @ inverse @ multiply ) )
!= ( c @ ( b @ multiply ) ) )
| ( ( identity @ ( a @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[39,23]) ).
thf(117,plain,
! [A: $i] :
( ( ( A @ ( A @ inverse @ multiply ) )
!= ( c @ ( b @ multiply ) ) )
| ( identity != c )
| ( a != a ) ),
inference(simp,[status(thm)],[113]) ).
thf(123,plain,
! [A: $i] :
( ( ( A @ ( A @ inverse @ multiply ) )
!= ( c @ ( b @ multiply ) ) )
| ( identity != c ) ),
inference(simp,[status(thm)],[117]) ).
thf(3415,plain,
! [B: $i,A: $i] :
( ( ( A @ ( identity @ multiply ) )
!= ( B @ ( B @ inverse @ multiply ) ) )
| ( A
!= ( c @ ( b @ multiply ) ) )
| ( identity != c ) ),
inference(paramod_ordered,[status(thm)],[55,123]) ).
thf(3421,plain,
! [A: $i] :
( ( A
!= ( c @ ( b @ multiply ) ) )
| ( ( A @ inverse )
!= identity )
| ( identity != c ) ),
inference(simp,[status(thm)],[3415]) ).
thf(3429,plain,
( ( ( c @ ( b @ multiply ) @ inverse )
!= identity )
| ( identity != c ) ),
inference(simp,[status(thm)],[3421]) ).
thf(210,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ least_upper_bound ) )
!= ( D @ ( C @ least_upper_bound ) ) )
| ( ( E @ ( B @ ( A @ least_upper_bound ) @ least_upper_bound ) )
= ( E @ ( D @ least_upper_bound ) @ ( C @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[25,29]) ).
thf(211,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ least_upper_bound ) @ least_upper_bound ) )
= ( C @ ( A @ least_upper_bound ) @ ( B @ least_upper_bound ) ) ),
inference(pattern_uni,[status(thm)],[210:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(215,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ least_upper_bound ) @ least_upper_bound ) )
= ( C @ ( A @ least_upper_bound ) @ ( B @ least_upper_bound ) ) ),
inference(simp,[status(thm)],[211]) ).
thf(7367,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= ( C @ ( A @ least_upper_bound ) @ ( B @ least_upper_bound ) ) ),
inference(rewrite,[status(thm)],[215,29]) ).
thf(53391,plain,
! [C: $i,B: $i,A: $i] :
( ( ( a @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
!= ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) ) )
| ( ( C @ ( A @ least_upper_bound ) @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[53029,7367]) ).
thf(53392,plain,
( ( a @ ( identity @ least_upper_bound ) @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[53391:[bind(A,$thf( identity )),bind(B,$thf( a @ ( a @ least_upper_bound ) )),bind(C,$thf( a ))]]) ).
thf(64523,plain,
( ( a @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[53392,29]) ).
thf(64563,plain,
! [B: $i,A: $i] :
( ( ( a @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[64523,25]) ).
thf(64564,plain,
( ( a @ ( a @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[64563:[bind(A,$thf( a )),bind(B,$thf( a @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) ))]]) ).
thf(78895,plain,
( ( a @ ( a @ ( identity @ least_upper_bound ) @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[64564,29]) ).
thf(78944,plain,
! [B: $i,A: $i] :
( ( ( a @ ( a @ ( identity @ least_upper_bound ) @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[78895,25]) ).
thf(78945,plain,
( ( a @ ( a @ ( a @ ( identity @ least_upper_bound ) @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[78944:[bind(A,$thf( a )),bind(B,$thf( a @ ( a @ ( identity @ least_upper_bound ) @ least_upper_bound ) ))]]) ).
thf(107087,plain,
( ( a @ ( a @ least_upper_bound ) @ ( a @ ( identity @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[78945,29]) ).
thf(447,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( identity @ greatest_lower_bound ) @ ( a @ least_upper_bound ) )
!= ( C @ ( B @ least_upper_bound ) ) )
| ( ( B @ ( C @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[432,25]) ).
thf(448,plain,
! [A: $i] :
( ( a @ ( A @ ( identity @ greatest_lower_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[447:[bind(A,$thf( E )),bind(B,$thf( a )),bind(C,$thf( E @ ( identity @ greatest_lower_bound ) ))]]) ).
thf(477,plain,
! [A: $i] :
( ( a @ ( A @ ( identity @ greatest_lower_bound ) @ least_upper_bound ) )
= a ),
inference(simp,[status(thm)],[448]) ).
thf(542,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( a @ ( A @ ( identity @ greatest_lower_bound ) @ least_upper_bound ) )
!= ( D @ ( C @ ( B @ least_upper_bound ) @ least_upper_bound ) ) )
| ( ( D @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[477,29]) ).
thf(583,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( a != D )
| ( ( A @ ( identity @ greatest_lower_bound ) )
!= ( C @ ( B @ least_upper_bound ) ) )
| ( ( D @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[542]) ).
thf(594,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( identity @ greatest_lower_bound ) )
!= ( C @ ( B @ least_upper_bound ) ) )
| ( ( a @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[583]) ).
thf(69313,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( C @ ( B @ least_upper_bound ) ) )
| ( ( a @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) )
= a ) ),
inference(rewrite,[status(thm)],[594,984]) ).
thf(4352,plain,
! [B: $i,A: $i] :
( ( ( c @ ( a @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[4043,53]) ).
thf(4353,plain,
( ( b @ ( c @ ( a @ greatest_lower_bound ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[4352:[bind(A,$thf( b )),bind(B,$thf( c @ ( a @ greatest_lower_bound ) ))]]) ).
thf(4521,plain,
( ( b @ ( c @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[4353,47]) ).
thf(118,plain,
! [A: $i] :
( ( A != c )
| ( ( A @ inverse )
!= b )
| ( ( identity @ ( a @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) ) ),
inference(simp,[status(thm)],[113]) ).
thf(124,plain,
( ( ( c @ inverse )
!= b )
| ( ( identity @ ( a @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) ) ),
inference(simp,[status(thm)],[118]) ).
thf(14,axiom,
( ( a @ ( identity @ greatest_lower_bound ) )
= identity ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p09b_1) ).
thf(48,plain,
( ( a @ ( identity @ greatest_lower_bound ) )
= identity ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(49,plain,
( ( a @ ( identity @ greatest_lower_bound ) )
= identity ),
inference(lifteq,[status(thm)],[48]) ).
thf(1174,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= ( a @ ( identity @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[53,49]) ).
thf(1175,plain,
( ( identity @ ( a @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[1174:[bind(A,$thf( identity )),bind(B,$thf( a ))]]) ).
thf(1462,plain,
( ( ( c @ inverse )
!= b )
| ( ( c @ ( a @ greatest_lower_bound ) )
!= identity ) ),
inference(rewrite,[status(thm)],[124,1175]) ).
thf(4559,plain,
( ( ( b @ ( c @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) )
| ( ( c @ inverse )
!= b )
| ( identity != identity ) ),
inference(paramod_ordered,[status(thm)],[4521,1462]) ).
thf(4560,plain,
( ( ( b @ ( c @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) )
| ( ( c @ inverse )
!= b ) ),
inference(simp,[status(thm)],[4559]) ).
thf(4634,plain,
( ( ( b @ ( c @ greatest_lower_bound ) )
!= c )
| ( a != a )
| ( ( c @ inverse )
!= b ) ),
inference(simp,[status(thm)],[4560]) ).
thf(4665,plain,
( ( ( b @ ( c @ greatest_lower_bound ) )
!= c )
| ( ( c @ inverse )
!= b ) ),
inference(simp,[status(thm)],[4634]) ).
thf(4856,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ least_upper_bound ) @ ( A @ greatest_lower_bound ) )
!= ( b @ ( c @ greatest_lower_bound ) ) )
| ( A != c )
| ( ( c @ inverse )
!= b ) ),
inference(paramod_ordered,[status(thm)],[45,4665]) ).
thf(4884,plain,
! [A: $i] :
( ( ( A @ ( c @ least_upper_bound ) )
!= b )
| ( c != c )
| ( ( c @ inverse )
!= b ) ),
inference(simp,[status(thm)],[4856]) ).
thf(4900,plain,
! [A: $i] :
( ( ( A @ ( c @ least_upper_bound ) )
!= b )
| ( ( c @ inverse )
!= b ) ),
inference(simp,[status(thm)],[4884]) ).
thf(8104,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ least_upper_bound ) )
!= ( C @ ( c @ least_upper_bound ) ) )
| ( ( B @ ( A @ least_upper_bound ) )
!= b )
| ( ( c @ inverse )
!= b ) ),
inference(paramod_ordered,[status(thm)],[25,4900]) ).
thf(8105,plain,
! [A: $i] :
( ( ( c @ ( A @ least_upper_bound ) )
!= b )
| ( ( c @ inverse )
!= b ) ),
inference(pattern_uni,[status(thm)],[8104:[bind(A,$thf( A )),bind(B,$thf( c )),bind(C,$thf( A ))]]) ).
thf(10779,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) @ ( A @ least_upper_bound ) )
!= ( c @ ( C @ least_upper_bound ) ) )
| ( A != b )
| ( ( c @ inverse )
!= b ) ),
inference(paramod_ordered,[status(thm)],[43,8105]) ).
thf(10796,plain,
! [B: $i,A: $i] :
( ( ( A @ ( b @ greatest_lower_bound ) )
!= c )
| ( b != B )
| ( ( c @ inverse )
!= b ) ),
inference(simp,[status(thm)],[10779]) ).
thf(10827,plain,
! [A: $i] :
( ( ( A @ ( b @ greatest_lower_bound ) )
!= c )
| ( ( c @ inverse )
!= b ) ),
inference(simp,[status(thm)],[10796]) ).
thf(17134,plain,
! [B: $i,A: $i] :
( ( ( b @ ( identity @ inverse @ multiply ) @ ( a @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( A @ ( identity @ least_upper_bound ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[14060,252]) ).
thf(17135,plain,
( ( a @ ( identity @ inverse @ multiply ) @ ( identity @ least_upper_bound ) )
= ( a @ ( identity @ inverse @ multiply ) ) ),
inference(pattern_uni,[status(thm)],[17134:[bind(A,$thf( a @ ( identity @ inverse @ multiply ) )),bind(B,$thf( b @ ( identity @ inverse @ multiply ) ))]]) ).
thf(21526,plain,
! [B: $i,A: $i] :
( ( ( a @ ( identity @ inverse @ multiply ) @ ( identity @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( a @ ( identity @ inverse @ multiply ) @ ( A @ greatest_lower_bound ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[17135,45]) ).
thf(21527,plain,
( ( a @ ( identity @ inverse @ multiply ) @ ( identity @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[21526:[bind(A,$thf( identity )),bind(B,$thf( a @ ( identity @ inverse @ multiply ) ))]]) ).
thf(21747,plain,
( ( a @ ( identity @ inverse @ multiply ) @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[21527,984]) ).
thf(21846,plain,
! [B: $i,A: $i] :
( ( ( a @ ( identity @ inverse @ multiply ) @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[21747,53]) ).
thf(21847,plain,
( ( a @ ( a @ ( identity @ inverse @ multiply ) @ ( b @ greatest_lower_bound ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[21846:[bind(A,$thf( a )),bind(B,$thf( a @ ( identity @ inverse @ multiply ) @ ( b @ greatest_lower_bound ) ))]]) ).
thf(22213,plain,
( ( a @ ( a @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[21847,47]) ).
thf(22322,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= ( a @ ( a @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[53,22213]) ).
thf(22323,plain,
( ( a @ ( identity @ inverse @ multiply ) @ ( a @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[22322:[bind(A,$thf( a @ ( identity @ inverse @ multiply ) )),bind(B,$thf( a ))]]) ).
thf(24540,plain,
! [B: $i,A: $i] :
( ( ( a @ ( identity @ inverse @ multiply ) @ ( a @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[22323,53]) ).
thf(24541,plain,
( ( b @ ( a @ ( identity @ inverse @ multiply ) @ ( a @ greatest_lower_bound ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[24540:[bind(A,$thf( b )),bind(B,$thf( a @ ( identity @ inverse @ multiply ) @ ( a @ greatest_lower_bound ) ))]]) ).
thf(24951,plain,
( ( b @ ( a @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[24541,47]) ).
thf(25060,plain,
! [B: $i,A: $i] :
( ( ( b @ ( a @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[24951,53]) ).
thf(25061,plain,
( ( a @ ( b @ ( a @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[25060:[bind(A,$thf( a )),bind(B,$thf( b @ ( a @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) ))]]) ).
thf(25727,plain,
( ( a @ ( b @ greatest_lower_bound ) @ ( a @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[25061,47]) ).
thf(500,plain,
! [C: $i,B: $i,A: $i] :
( ( ( a @ ( identity @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( C @ ( identity @ multiply ) )
= ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[49,41]) ).
thf(501,plain,
! [A: $i] :
( ( A @ ( a @ multiply ) @ ( A @ ( identity @ multiply ) @ greatest_lower_bound ) )
= ( A @ ( identity @ multiply ) ) ),
inference(pattern_uni,[status(thm)],[500:[bind(A,$thf( identity )),bind(B,$thf( a ))]]) ).
thf(538,plain,
! [A: $i] :
( ( A @ ( a @ multiply ) @ ( A @ ( identity @ multiply ) @ greatest_lower_bound ) )
= ( A @ ( identity @ multiply ) ) ),
inference(simp,[status(thm)],[501]) ).
thf(59231,plain,
! [A: $i] :
( ( A @ ( a @ multiply ) @ ( A @ greatest_lower_bound ) )
= A ),
inference(rewrite,[status(thm)],[538,55]) ).
thf(493,plain,
! [C: $i,B: $i,A: $i] :
( ( ( b @ ( a @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( C @ ( identity @ multiply ) )
= ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[35,41]) ).
thf(494,plain,
! [A: $i] :
( ( A @ ( identity @ multiply ) )
= ( A @ ( b @ multiply ) @ ( A @ ( a @ multiply ) @ greatest_lower_bound ) ) ),
inference(pattern_uni,[status(thm)],[493:[bind(A,$thf( a )),bind(B,$thf( b ))]]) ).
thf(535,plain,
! [A: $i] :
( ( A @ ( identity @ multiply ) )
= ( A @ ( b @ multiply ) @ ( A @ ( a @ multiply ) @ greatest_lower_bound ) ) ),
inference(simp,[status(thm)],[494]) ).
thf(55432,plain,
! [A: $i] :
( ( A @ ( b @ multiply ) @ ( A @ ( a @ multiply ) @ greatest_lower_bound ) )
= A ),
inference(rewrite,[status(thm)],[535,55]) ).
thf(150532,plain,
! [B: $i,A: $i] :
( ( ( A @ ( b @ multiply ) @ ( A @ ( a @ multiply ) @ greatest_lower_bound ) )
!= ( c @ ( b @ multiply ) @ ( B @ greatest_lower_bound ) ) )
| ( ( B @ ( a @ greatest_lower_bound ) )
!= a )
| ( A != c ) ),
inference(paramod_ordered,[status(thm)],[55432,977]) ).
thf(150533,plain,
( ( ( c @ ( a @ multiply ) @ ( a @ greatest_lower_bound ) )
!= a )
| ( c != c ) ),
inference(pattern_uni,[status(thm)],[150532:[bind(A,$thf( c )),bind(B,$thf( c @ ( a @ multiply ) ))]]) ).
thf(150816,plain,
( ( c @ ( a @ multiply ) @ ( a @ greatest_lower_bound ) )
!= a ),
inference(simp,[status(thm)],[150533]) ).
thf(153108,plain,
! [A: $i] :
( ( ( A @ ( a @ multiply ) @ ( A @ greatest_lower_bound ) )
!= ( c @ ( a @ multiply ) @ ( a @ greatest_lower_bound ) ) )
| ( A != a ) ),
inference(paramod_ordered,[status(thm)],[59231,150816]) ).
thf(153187,plain,
( ( ( c @ ( a @ multiply ) )
!= ( a @ ( a @ multiply ) ) )
| ( a != a ) ),
inference(simp,[status(thm)],[153108]) ).
thf(153278,plain,
( ( c @ ( a @ multiply ) )
!= ( a @ ( a @ multiply ) ) ),
inference(simp,[status(thm)],[153187]) ).
thf(932,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ greatest_lower_bound ) @ greatest_lower_bound ) )
!= ( D @ ( a @ least_upper_bound ) @ ( identity @ greatest_lower_bound ) ) )
| ( ( C @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[47,753]) ).
thf(963,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C
!= ( D @ ( a @ least_upper_bound ) ) )
| ( ( B @ ( A @ greatest_lower_bound ) )
!= identity )
| ( ( C @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= identity ) ),
inference(simp,[status(thm)],[932]) ).
thf(973,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= identity )
| ( ( C @ ( a @ least_upper_bound ) @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= identity ) ),
inference(simp,[status(thm)],[963]) ).
thf(1118,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ greatest_lower_bound ) )
!= ( C @ ( identity @ greatest_lower_bound ) ) )
| ( ( a @ ( B @ ( A @ greatest_lower_bound ) @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[53,477]) ).
thf(1119,plain,
! [A: $i] :
( ( a @ ( identity @ ( A @ greatest_lower_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[1118:[bind(A,$thf( A )),bind(B,$thf( identity )),bind(C,$thf( A ))]]) ).
thf(3827,plain,
! [B: $i,A: $i] :
( ( ( A @ ( identity @ greatest_lower_bound ) )
!= ( identity @ ( B @ greatest_lower_bound ) ) )
| ( ( a @ ( A @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[984,1119]) ).
thf(3828,plain,
( ( a @ ( identity @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[3827:[bind(A,$thf( identity )),bind(B,$thf( identity ))]]) ).
thf(1192,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= ( b @ ( identity @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[53,51]) ).
thf(1193,plain,
( ( identity @ ( b @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[1192:[bind(A,$thf( identity )),bind(B,$thf( b ))]]) ).
thf(5187,plain,
( ( a @ ( identity @ ( a @ greatest_lower_bound ) @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[3828,1193]) ).
thf(5188,plain,
! [B: $i,A: $i] :
( ( ( a @ ( identity @ ( a @ greatest_lower_bound ) @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( a @ ( A @ greatest_lower_bound ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[5187,45]) ).
thf(5189,plain,
( ( a @ ( identity @ ( a @ greatest_lower_bound ) @ greatest_lower_bound ) )
= ( identity @ ( a @ greatest_lower_bound ) ) ),
inference(pattern_uni,[status(thm)],[5188:[bind(A,$thf( identity @ ( a @ greatest_lower_bound ) )),bind(B,$thf( a ))]]) ).
thf(6003,plain,
( ( a @ ( identity @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[5189,1175,47]) ).
thf(1510,plain,
( ( ( c @ ( b @ multiply ) @ ( a @ greatest_lower_bound ) )
!= ( identity @ ( a @ greatest_lower_bound ) ) )
| ( ( c @ ( a @ greatest_lower_bound ) )
!= identity ) ),
inference(paramod_ordered,[status(thm)],[1175,23]) ).
thf(1521,plain,
( ( ( c @ ( b @ multiply ) )
!= identity )
| ( a != a )
| ( ( c @ ( a @ greatest_lower_bound ) )
!= identity ) ),
inference(simp,[status(thm)],[1510]) ).
thf(1532,plain,
( ( ( c @ ( b @ multiply ) )
!= identity )
| ( ( c @ ( a @ greatest_lower_bound ) )
!= identity ) ),
inference(simp,[status(thm)],[1521]) ).
thf(6116,plain,
( ( ( a @ ( identity @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) )
| ( ( c @ ( b @ multiply ) )
!= identity )
| ( identity != identity ) ),
inference(paramod_ordered,[status(thm)],[6003,1532]) ).
thf(6117,plain,
( ( ( a @ ( identity @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(simp,[status(thm)],[6116]) ).
thf(6138,plain,
( ( ( a @ ( identity @ greatest_lower_bound ) )
!= c )
| ( a != a )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(simp,[status(thm)],[6117]) ).
thf(6189,plain,
( ( ( a @ ( identity @ greatest_lower_bound ) )
!= c )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(simp,[status(thm)],[6138]) ).
thf(9027,plain,
( ( ( a @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= c )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(rewrite,[status(thm)],[6189,984]) ).
thf(503,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ greatest_lower_bound ) @ multiply ) )
!= ( F @ ( E @ greatest_lower_bound ) @ ( D @ multiply ) ) )
| ( ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ greatest_lower_bound ) )
= ( F @ ( D @ multiply ) @ ( E @ ( D @ multiply ) @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[41,31]) ).
thf(504,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ greatest_lower_bound ) @ ( B @ multiply ) @ ( D @ ( C @ greatest_lower_bound ) @ ( A @ multiply ) @ greatest_lower_bound ) )
= ( D @ ( B @ ( A @ greatest_lower_bound ) @ multiply ) @ ( C @ ( B @ ( A @ greatest_lower_bound ) @ multiply ) @ greatest_lower_bound ) ) ),
inference(pattern_uni,[status(thm)],[503:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( J @ ( I @ greatest_lower_bound ) )),bind(D,$thf( H @ ( G @ greatest_lower_bound ) )),bind(E,$thf( I )),bind(F,$thf( J ))]]) ).
thf(539,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ greatest_lower_bound ) @ ( B @ multiply ) @ ( D @ ( C @ greatest_lower_bound ) @ ( A @ multiply ) @ greatest_lower_bound ) )
= ( D @ ( B @ ( A @ greatest_lower_bound ) @ multiply ) @ ( C @ ( B @ ( A @ greatest_lower_bound ) @ multiply ) @ greatest_lower_bound ) ) ),
inference(simp,[status(thm)],[504]) ).
thf(60036,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ multiply ) @ ( C @ ( B @ multiply ) @ greatest_lower_bound ) @ ( D @ ( A @ multiply ) @ ( C @ ( A @ multiply ) @ greatest_lower_bound ) @ greatest_lower_bound ) )
= ( D @ ( B @ multiply ) @ ( D @ ( A @ multiply ) @ greatest_lower_bound ) @ ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ greatest_lower_bound ) @ greatest_lower_bound ) ) ),
inference(rewrite,[status(thm)],[539,41,31]) ).
thf(49621,plain,
! [B: $i,A: $i] :
( ( ( a @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( a != a )
| ( ( identity @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[49465,286]) ).
thf(49622,plain,
! [B: $i,A: $i] :
( ( ( a @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( identity @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[49621]) ).
thf(49623,plain,
( ( identity @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[49622:[bind(A,$thf( identity )),bind(B,$thf( a @ ( a @ least_upper_bound ) ))]]) ).
thf(56851,plain,
( ( identity @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[49623,4926]) ).
thf(57106,plain,
! [C: $i,B: $i,A: $i] :
( ( ( identity @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
!= ( A @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) ) )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[56851,213]) ).
thf(57107,plain,
( ( a @ ( identity @ least_upper_bound ) @ ( identity @ ( a @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[57106:[bind(A,$thf( identity @ ( a @ least_upper_bound ) )),bind(B,$thf( identity )),bind(C,$thf( a ))]]) ).
thf(68448,plain,
( ( a @ ( identity @ least_upper_bound ) @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[57107,29]) ).
thf(68487,plain,
! [B: $i,A: $i] :
( ( ( a @ ( identity @ least_upper_bound ) @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[68448,25]) ).
thf(68488,plain,
( ( a @ ( a @ ( identity @ least_upper_bound ) @ ( identity @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[68487:[bind(A,$thf( a )),bind(B,$thf( a @ ( identity @ least_upper_bound ) @ ( identity @ least_upper_bound ) ))]]) ).
thf(84741,plain,
( ( a @ ( a @ ( identity @ least_upper_bound ) @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[68488,29]) ).
thf(84789,plain,
! [B: $i,A: $i] :
( ( ( a @ ( a @ ( identity @ least_upper_bound ) @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[84741,25]) ).
thf(84790,plain,
( ( identity @ ( a @ ( a @ ( identity @ least_upper_bound ) @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[84789:[bind(A,$thf( identity )),bind(B,$thf( a @ ( a @ ( identity @ least_upper_bound ) @ least_upper_bound ) ))]]) ).
thf(113012,plain,
( ( identity @ ( a @ least_upper_bound ) @ ( a @ ( identity @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[84790,29]) ).
thf(113629,plain,
! [C: $i,B: $i,A: $i] :
( ( ( identity @ ( a @ least_upper_bound ) @ ( a @ ( identity @ least_upper_bound ) @ least_upper_bound ) )
!= ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) ) )
| ( ( C @ ( A @ least_upper_bound ) @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[113012,7367]) ).
thf(113630,plain,
( ( identity @ ( a @ ( identity @ least_upper_bound ) @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[113629:[bind(A,$thf( a @ ( identity @ least_upper_bound ) )),bind(B,$thf( a )),bind(C,$thf( identity ))]]) ).
thf(141026,plain,
( ( identity @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[113630,4926]) ).
thf(385,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( C @ ( B @ least_upper_bound ) ) )
| ( ( A @ ( a @ least_upper_bound ) )
= ( B @ ( C @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[290,25]) ).
thf(386,plain,
! [A: $i] :
( ( a @ ( A @ ( identity @ least_upper_bound ) @ least_upper_bound ) )
= ( A @ ( a @ least_upper_bound ) ) ),
inference(pattern_uni,[status(thm)],[385:[bind(A,$thf( E )),bind(B,$thf( a )),bind(C,$thf( E @ ( identity @ least_upper_bound ) ))]]) ).
thf(415,plain,
! [A: $i] :
( ( a @ ( A @ ( identity @ least_upper_bound ) @ least_upper_bound ) )
= ( A @ ( a @ least_upper_bound ) ) ),
inference(simp,[status(thm)],[386]) ).
thf(3221,plain,
! [A: $i] :
( ( a @ ( A @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
= ( A @ ( a @ least_upper_bound ) ) ),
inference(rewrite,[status(thm)],[415,29]) ).
thf(778,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ least_upper_bound ) @ least_upper_bound ) )
!= ( D @ ( a @ least_upper_bound ) ) )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) @ ( identity @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[29,753]) ).
thf(833,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C != D )
| ( ( B @ ( A @ least_upper_bound ) )
!= a )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) @ ( identity @ greatest_lower_bound ) )
= identity ) ),
inference(simp,[status(thm)],[778]) ).
thf(841,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ least_upper_bound ) )
!= a )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) @ ( identity @ greatest_lower_bound ) )
= identity ) ),
inference(simp,[status(thm)],[833]) ).
thf(114761,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ least_upper_bound ) )
!= a )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= identity ) ),
inference(rewrite,[status(thm)],[841,984]) ).
thf(779,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( a @ least_upper_bound ) @ ( identity @ greatest_lower_bound ) )
!= ( C @ ( B @ greatest_lower_bound ) ) )
| ( ( D @ ( identity @ multiply ) )
= ( D @ ( C @ multiply ) @ ( D @ ( B @ multiply ) @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[753,41]) ).
thf(780,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( a @ least_upper_bound ) @ multiply ) @ ( A @ ( identity @ multiply ) @ greatest_lower_bound ) )
= ( A @ ( identity @ multiply ) ) ),
inference(pattern_uni,[status(thm)],[779:[bind(A,$thf( F )),bind(B,$thf( identity )),bind(C,$thf( F @ ( a @ least_upper_bound ) )),bind(D,$thf( D ))]]) ).
thf(846,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( a @ least_upper_bound ) @ multiply ) @ ( A @ ( identity @ multiply ) @ greatest_lower_bound ) )
= ( A @ ( identity @ multiply ) ) ),
inference(simp,[status(thm)],[780]) ).
thf(120885,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( a @ least_upper_bound ) @ multiply ) @ ( A @ greatest_lower_bound ) )
= A ),
inference(rewrite,[status(thm)],[846,55]) ).
thf(58711,plain,
! [C: $i,B: $i,A: $i] :
( ( ( identity @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( A @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) ) )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[58446,213]) ).
thf(58712,plain,
( ( a @ ( a @ least_upper_bound ) @ ( identity @ ( identity @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[58711:[bind(A,$thf( identity @ ( identity @ least_upper_bound ) )),bind(B,$thf( a )),bind(C,$thf( a ))]]) ).
thf(73977,plain,
( ( a @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[58712,29]) ).
thf(74026,plain,
! [B: $i,A: $i] :
( ( ( a @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[73977,25]) ).
thf(74027,plain,
( ( identity @ ( a @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[74026:[bind(A,$thf( identity )),bind(B,$thf( a @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) ))]]) ).
thf(96170,plain,
( ( identity @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[74027,29]) ).
thf(86564,plain,
! [B: $i,A: $i] :
( ( ( a @ ( a @ least_upper_bound ) @ ( identity @ ( identity @ least_upper_bound ) @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( a @ ( A @ greatest_lower_bound ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[86331,45]) ).
thf(86565,plain,
( ( a @ ( identity @ ( identity @ least_upper_bound ) @ greatest_lower_bound ) )
= ( identity @ ( identity @ least_upper_bound ) ) ),
inference(pattern_uni,[status(thm)],[86564:[bind(A,$thf( identity @ ( identity @ least_upper_bound ) )),bind(B,$thf( a @ ( a @ least_upper_bound ) ))]]) ).
thf(3816,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( identity @ greatest_lower_bound ) )
!= ( C @ ( B @ greatest_lower_bound ) ) )
| ( ( A @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) @ ( B @ least_upper_bound ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[984,43]) ).
thf(3817,plain,
! [A: $i] :
( ( A @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) @ ( identity @ least_upper_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[3816:[bind(A,$thf( A )),bind(B,$thf( identity )),bind(C,$thf( A ))]]) ).
thf(11610,plain,
! [A: $i] :
( ( ( c @ ( a @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
!= ( A @ ( b @ greatest_lower_bound ) ) )
| ( ( identity @ ( a @ greatest_lower_bound ) @ ( identity @ least_upper_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[4043,3817]) ).
thf(11611,plain,
( ( identity @ ( a @ greatest_lower_bound ) @ ( identity @ least_upper_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[11610:[bind(A,$thf( c @ ( a @ greatest_lower_bound ) ))]]) ).
thf(12290,plain,
( ( identity @ ( identity @ least_upper_bound ) )
= identity ),
inference(rewrite,[status(thm)],[11611,1175]) ).
thf(116436,plain,
( ( a @ ( identity @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[86565,12290]) ).
thf(965,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ greatest_lower_bound ) @ greatest_lower_bound ) )
!= ( c @ ( b @ multiply ) @ ( a @ greatest_lower_bound ) ) )
| ( ( C @ ( B @ greatest_lower_bound ) )
!= c )
| ( A != a ) ),
inference(simp,[status(thm)],[944]) ).
thf(975,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ( a @ greatest_lower_bound ) @ greatest_lower_bound ) )
!= ( c @ ( b @ multiply ) @ ( a @ greatest_lower_bound ) ) )
| ( ( B @ ( A @ greatest_lower_bound ) )
!= c ) ),
inference(simp,[status(thm)],[965]) ).
thf(145335,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( c @ ( b @ multiply ) @ ( a @ greatest_lower_bound ) ) )
| ( ( B @ ( A @ greatest_lower_bound ) )
!= c ) ),
inference(rewrite,[status(thm)],[975,47]) ).
thf(1190,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ greatest_lower_bound ) )
!= ( C @ ( identity @ greatest_lower_bound ) ) )
| ( ( B @ ( A @ greatest_lower_bound ) @ ( a @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[53,432]) ).
thf(1191,plain,
! [A: $i] :
( ( identity @ ( A @ greatest_lower_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[1190:[bind(A,$thf( A )),bind(B,$thf( identity )),bind(C,$thf( A ))]]) ).
thf(151033,plain,
! [A: $i] :
( ( ( A @ ( b @ multiply ) @ ( A @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) )
| ( A != a ) ),
inference(paramod_ordered,[status(thm)],[62679,150839]) ).
thf(151129,plain,
( ( ( a @ ( b @ multiply ) )
!= c )
| ( a != a ) ),
inference(simp,[status(thm)],[151033]) ).
thf(151197,plain,
( ( a @ ( b @ multiply ) )
!= c ),
inference(simp,[status(thm)],[151129]) ).
thf(151232,plain,
! [A: $i] :
( ( ( A @ ( A @ inverse @ multiply ) )
!= ( a @ ( b @ multiply ) ) )
| ( identity != c ) ),
inference(paramod_ordered,[status(thm)],[39,151197]) ).
thf(151240,plain,
! [A: $i] :
( ( A != a )
| ( ( A @ inverse )
!= b )
| ( identity != c ) ),
inference(simp,[status(thm)],[151232]) ).
thf(151245,plain,
( ( ( a @ inverse )
!= b )
| ( identity != c ) ),
inference(simp,[status(thm)],[151240]) ).
thf(293,plain,
! [C: $i,B: $i,A: $i] :
( ( ( c @ ( identity @ greatest_lower_bound ) )
!= ( C @ ( B @ greatest_lower_bound ) ) )
| ( ( identity @ ( A @ multiply ) )
= ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[33,31]) ).
thf(294,plain,
! [A: $i] :
( ( c @ ( A @ multiply ) @ ( identity @ ( A @ multiply ) @ greatest_lower_bound ) )
= ( identity @ ( A @ multiply ) ) ),
inference(pattern_uni,[status(thm)],[293:[bind(A,$thf( A )),bind(B,$thf( identity )),bind(C,$thf( c ))]]) ).
thf(13539,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ inverse @ multiply ) )
!= ( identity @ ( B @ multiply ) ) )
| ( ( identity @ ( B @ multiply ) )
= ( c @ ( B @ multiply ) @ ( identity @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[39,294]) ).
thf(13540,plain,
( ( identity @ ( identity @ inverse @ multiply ) )
= ( c @ ( identity @ inverse @ multiply ) @ ( identity @ greatest_lower_bound ) ) ),
inference(pattern_uni,[status(thm)],[13539:[bind(A,$thf( identity )),bind(B,$thf( identity @ inverse ))]]) ).
thf(15998,plain,
( ( b @ ( identity @ inverse @ multiply ) @ ( a @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) )
= ( c @ ( identity @ inverse @ multiply ) @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) ) ),
inference(rewrite,[status(thm)],[13540,984,301]) ).
thf(17065,plain,
( ( c @ ( identity @ inverse @ multiply ) @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[15998,14060]) ).
thf(17761,plain,
! [B: $i,A: $i] :
( ( ( c @ ( identity @ inverse @ multiply ) @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[17065,53]) ).
thf(17762,plain,
( ( a @ ( c @ ( identity @ inverse @ multiply ) @ ( b @ greatest_lower_bound ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[17761:[bind(A,$thf( a )),bind(B,$thf( c @ ( identity @ inverse @ multiply ) @ ( b @ greatest_lower_bound ) ))]]) ).
thf(18061,plain,
( ( a @ ( c @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[17762,47]) ).
thf(18148,plain,
! [B: $i,A: $i] :
( ( ( a @ ( c @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[18061,53]) ).
thf(18149,plain,
( ( b @ ( a @ ( c @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[18148:[bind(A,$thf( b )),bind(B,$thf( a @ ( c @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) ))]]) ).
thf(18451,plain,
( ( b @ ( a @ greatest_lower_bound ) @ ( c @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[18149,47]) ).
thf(47525,plain,
! [B: $i,A: $i] :
( ( ( a @ ( a @ least_upper_bound ) @ ( identity @ ( a @ least_upper_bound ) @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( a @ ( A @ greatest_lower_bound ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[47373,45]) ).
thf(47526,plain,
( ( a @ ( identity @ ( a @ least_upper_bound ) @ greatest_lower_bound ) )
= ( identity @ ( a @ least_upper_bound ) ) ),
inference(pattern_uni,[status(thm)],[47525:[bind(A,$thf( identity @ ( a @ least_upper_bound ) )),bind(B,$thf( a @ ( a @ least_upper_bound ) ))]]) ).
thf(42535,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) @ ( A @ least_upper_bound ) ) )
| ( ( B @ ( A @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[42517,217]) ).
thf(42536,plain,
( ( identity @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[42535:[bind(A,$thf( a )),bind(B,$thf( identity @ ( a @ least_upper_bound ) ))]]) ).
thf(43629,plain,
( ( identity @ ( a @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[42536,217]) ).
thf(54828,plain,
( ( a @ ( a @ greatest_lower_bound ) )
= a ),
inference(rewrite,[status(thm)],[47526,43629]) ).
thf(695,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ least_upper_bound ) @ ( A @ greatest_lower_bound ) )
!= ( D @ ( C @ greatest_lower_bound ) ) )
| ( ( E @ ( A @ multiply ) )
= ( E @ ( D @ multiply ) @ ( E @ ( C @ multiply ) @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[45,41]) ).
thf(696,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ ( B @ least_upper_bound ) @ multiply ) @ ( A @ ( B @ multiply ) @ greatest_lower_bound ) )
= ( A @ ( B @ multiply ) ) ),
inference(pattern_uni,[status(thm)],[695:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( F )),bind(D,$thf( G @ ( F @ least_upper_bound ) ))]]) ).
thf(770,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ ( B @ least_upper_bound ) @ multiply ) @ ( A @ ( B @ multiply ) @ greatest_lower_bound ) )
= ( A @ ( B @ multiply ) ) ),
inference(simp,[status(thm)],[696]) ).
thf(302,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ greatest_lower_bound ) @ ( A @ multiply ) )
!= ( c @ ( b @ multiply ) ) )
| ( ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ greatest_lower_bound ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[31,95]) ).
thf(322,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ greatest_lower_bound ) )
!= c )
| ( A != b )
| ( ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ greatest_lower_bound ) )
!= c ) ),
inference(simp,[status(thm)],[302]) ).
thf(325,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= c )
| ( ( B @ ( b @ multiply ) @ ( A @ ( b @ multiply ) @ greatest_lower_bound ) )
!= c ) ),
inference(simp,[status(thm)],[322]) ).
thf(57,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ multiply ) @ multiply ) )
= ( C @ ( B @ multiply ) @ ( A @ multiply ) ) ),
inference(lifteq,[status(thm)],[56]) ).
thf(57771,plain,
! [B: $i,A: $i] :
( ( ( A @ ( c @ multiply ) @ ( A @ greatest_lower_bound ) )
!= ( B @ ( identity @ greatest_lower_bound ) ) )
| ( A
= ( B @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[57665,984]) ).
thf(57772,plain,
( ( identity @ ( c @ multiply ) @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[57771:[bind(A,$thf( identity )),bind(B,$thf( identity @ ( c @ multiply ) ))]]) ).
thf(70701,plain,
( ( b @ ( c @ multiply ) @ ( a @ ( c @ multiply ) @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[57772,301]) ).
thf(13012,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ greatest_lower_bound ) )
!= ( C @ ( b @ greatest_lower_bound ) ) )
| ( ( B @ ( A @ greatest_lower_bound ) )
!= c )
| ( ( c @ inverse )
!= b ) ),
inference(paramod_ordered,[status(thm)],[53,10827]) ).
thf(13013,plain,
! [A: $i] :
( ( ( b @ ( A @ greatest_lower_bound ) )
!= c )
| ( ( c @ inverse )
!= b ) ),
inference(pattern_uni,[status(thm)],[13012:[bind(A,$thf( A )),bind(B,$thf( b )),bind(C,$thf( A ))]]) ).
thf(111,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ inverse @ multiply ) )
!= ( B @ ( identity @ multiply ) ) )
| ( identity = B ) ),
inference(paramod_ordered,[status(thm)],[39,55]) ).
thf(115,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( ( A @ inverse )
!= identity )
| ( identity = B ) ),
inference(simp,[status(thm)],[111]) ).
thf(121,plain,
! [A: $i] :
( ( ( A @ inverse )
!= identity )
| ( identity = A ) ),
inference(simp,[status(thm)],[115]) ).
thf(4574,plain,
! [B: $i,A: $i] :
( ( ( b @ ( c @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[4521,53]) ).
thf(4575,plain,
( ( a @ ( b @ ( c @ greatest_lower_bound ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[4574:[bind(A,$thf( a )),bind(B,$thf( b @ ( c @ greatest_lower_bound ) ))]]) ).
thf(4686,plain,
( ( a @ ( b @ greatest_lower_bound ) @ ( c @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[4575,47]) ).
thf(549,plain,
! [C: $i,B: $i,A: $i] :
( ( ( a @ ( A @ ( identity @ greatest_lower_bound ) @ least_upper_bound ) )
!= ( C @ ( B @ greatest_lower_bound ) @ ( B @ least_upper_bound ) ) )
| ( a = B ) ),
inference(paramod_ordered,[status(thm)],[477,43]) ).
thf(589,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ greatest_lower_bound ) )
!= a )
| ( ( A @ ( identity @ greatest_lower_bound ) )
!= B )
| ( a = B ) ),
inference(simp,[status(thm)],[549]) ).
thf(600,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ( identity @ greatest_lower_bound ) @ greatest_lower_bound ) )
!= a )
| ( ( A @ ( identity @ greatest_lower_bound ) )
= a ) ),
inference(simp,[status(thm)],[589]) ).
thf(74947,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) @ ( identity @ greatest_lower_bound ) )
!= a )
| ( ( A @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= a ) ),
inference(rewrite,[status(thm)],[600,984,47]) ).
thf(140,plain,
! [A: $i] :
( ( ( b @ ( a @ greatest_lower_bound ) )
!= ( A @ ( A @ greatest_lower_bound ) ) )
| ( identity = A ) ),
inference(paramod_ordered,[status(thm)],[35,37]) ).
thf(148,plain,
! [A: $i] :
( ( b != A )
| ( a != A )
| ( identity = A ) ),
inference(simp,[status(thm)],[140]) ).
thf(158,plain,
( ( b != a )
| ( identity = a ) ),
inference(simp,[status(thm)],[148]) ).
thf(97,plain,
! [A: $i] :
( ( ( A @ ( identity @ multiply ) )
!= ( c @ ( b @ multiply ) ) )
| ( A != c ) ),
inference(paramod_ordered,[status(thm)],[55,95]) ).
thf(100,plain,
( ( c != c )
| ( identity != b ) ),
inference(simp,[status(thm)],[97]) ).
thf(104,plain,
identity != b,
inference(simp,[status(thm)],[100]) ).
thf(3769,plain,
( ( identity != identity )
| ( b != a )
| ( b != a ) ),
inference(paramod_ordered,[status(thm)],[158,104]) ).
thf(3770,plain,
( ( identity != identity )
| ( b != a ) ),
inference(simp,[status(thm)],[3769]) ).
thf(3771,plain,
b != a,
inference(pattern_uni,[status(thm)],[3770:[]]) ).
thf(906,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ greatest_lower_bound ) @ greatest_lower_bound ) )
!= ( E @ ( D @ least_upper_bound ) @ ( D @ greatest_lower_bound ) ) )
| ( ( C @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= D ) ),
inference(paramod_ordered,[status(thm)],[47,45]) ).
thf(907,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ ( B @ greatest_lower_bound ) @ least_upper_bound ) @ ( C @ greatest_lower_bound ) @ ( B @ greatest_lower_bound ) )
= ( C @ ( B @ greatest_lower_bound ) ) ),
inference(pattern_uni,[status(thm)],[906:[bind(A,$thf( J )),bind(B,$thf( K )),bind(C,$thf( I @ ( K @ ( J @ greatest_lower_bound ) @ least_upper_bound ) )),bind(D,$thf( K @ ( J @ greatest_lower_bound ) )),bind(E,$thf( I ))]]) ).
thf(981,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ ( B @ greatest_lower_bound ) @ least_upper_bound ) @ ( C @ greatest_lower_bound ) @ ( B @ greatest_lower_bound ) )
= ( C @ ( B @ greatest_lower_bound ) ) ),
inference(simp,[status(thm)],[907]) ).
thf(939,plain,
! [C: $i,B: $i,A: $i] :
( ( ( a @ ( identity @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( C @ ( identity @ greatest_lower_bound ) )
= ( C @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[49,47]) ).
thf(940,plain,
! [A: $i] :
( ( A @ ( a @ greatest_lower_bound ) @ ( identity @ greatest_lower_bound ) )
= ( A @ ( identity @ greatest_lower_bound ) ) ),
inference(pattern_uni,[status(thm)],[939:[bind(A,$thf( identity )),bind(B,$thf( a ))]]) ).
thf(992,plain,
! [A: $i] :
( ( A @ ( a @ greatest_lower_bound ) @ ( identity @ greatest_lower_bound ) )
= ( A @ ( identity @ greatest_lower_bound ) ) ),
inference(simp,[status(thm)],[940]) ).
thf(179681,plain,
! [A: $i] :
( ( A @ ( a @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= ( A @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) ) ),
inference(rewrite,[status(thm)],[992,984]) ).
thf(20,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ least_upper_bound ) @ multiply ) )
= ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ least_upper_bound ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',monotony_lub2) ).
thf(60,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ least_upper_bound ) @ multiply ) )
= ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ least_upper_bound ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(61,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ least_upper_bound ) )
= ( C @ ( B @ ( A @ least_upper_bound ) @ multiply ) ) ),
inference(lifteq,[status(thm)],[60]) ).
thf(62802,plain,
! [B: $i,A: $i] :
( ( ( A @ ( b @ multiply ) @ ( A @ greatest_lower_bound ) )
!= ( B @ ( identity @ greatest_lower_bound ) ) )
| ( A
= ( B @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[62679,984]) ).
thf(62803,plain,
( ( identity @ ( b @ multiply ) @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[62802:[bind(A,$thf( identity )),bind(B,$thf( identity @ ( b @ multiply ) ))]]) ).
thf(76215,plain,
( ( b @ ( b @ multiply ) @ ( a @ ( b @ multiply ) @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[62803,301]) ).
thf(56881,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[56851,25]) ).
thf(56882,plain,
( ( identity @ ( identity @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[56881:[bind(A,$thf( identity )),bind(B,$thf( identity @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) ))]]) ).
thf(67576,plain,
( ( identity @ ( identity @ ( a @ least_upper_bound ) @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[56882,29]) ).
thf(67614,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( identity @ ( a @ least_upper_bound ) @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[67576,25]) ).
thf(67615,plain,
( ( a @ ( identity @ ( identity @ ( a @ least_upper_bound ) @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[67614:[bind(A,$thf( a )),bind(B,$thf( identity @ ( identity @ ( a @ least_upper_bound ) @ least_upper_bound ) ))]]) ).
thf(82489,plain,
( ( a @ ( identity @ least_upper_bound ) @ ( identity @ ( a @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[67615,29]) ).
thf(82537,plain,
! [B: $i,A: $i] :
( ( ( a @ ( identity @ least_upper_bound ) @ ( identity @ ( a @ least_upper_bound ) @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[82489,25]) ).
thf(82538,plain,
( ( identity @ ( a @ least_upper_bound ) @ ( a @ ( identity @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[82537:[bind(A,$thf( identity @ ( a @ least_upper_bound ) )),bind(B,$thf( a @ ( identity @ least_upper_bound ) ))]]) ).
thf(111819,plain,
( ( identity @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[82538,29]) ).
thf(371,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( D @ ( C @ ( B @ least_upper_bound ) @ least_upper_bound ) ) )
| ( ( A @ ( a @ least_upper_bound ) )
= ( D @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[290,29]) ).
thf(413,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( identity @ least_upper_bound ) )
!= D )
| ( ( C @ ( B @ least_upper_bound ) )
!= a )
| ( ( A @ ( a @ least_upper_bound ) )
= ( D @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) ) ) ),
inference(simp,[status(thm)],[371]) ).
thf(428,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ least_upper_bound ) )
!= a )
| ( ( A @ ( a @ least_upper_bound ) )
= ( A @ ( identity @ least_upper_bound ) @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) ) ) ),
inference(simp,[status(thm)],[413]) ).
thf(927,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ greatest_lower_bound ) @ greatest_lower_bound ) )
!= ( c @ ( identity @ greatest_lower_bound ) ) )
| ( ( C @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[47,33]) ).
thf(968,plain,
! [C: $i,B: $i,A: $i] :
( ( C != c )
| ( ( B @ ( A @ greatest_lower_bound ) )
!= identity )
| ( ( C @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= identity ) ),
inference(simp,[status(thm)],[927]) ).
thf(978,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= identity )
| ( ( c @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= identity ) ),
inference(simp,[status(thm)],[968]) ).
thf(151377,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ greatest_lower_bound ) )
!= ( C @ ( B @ greatest_lower_bound ) ) )
| ( A != identity )
| ( ( c @ ( C @ greatest_lower_bound ) @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[37,978]) ).
thf(151378,plain,
! [A: $i] :
( ( A != identity )
| ( ( c @ ( A @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= identity ) ),
inference(pattern_uni,[status(thm)],[151377:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(152740,plain,
( ( c @ ( identity @ greatest_lower_bound ) @ ( identity @ greatest_lower_bound ) )
= identity ),
inference(simp,[status(thm)],[151378]) ).
thf(161168,plain,
( ( c @ ( identity @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[152740,984]) ).
thf(22318,plain,
! [B: $i,A: $i] :
( ( ( a @ ( a @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[22213,53]) ).
thf(22319,plain,
( ( b @ ( a @ ( a @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[22318:[bind(A,$thf( b )),bind(B,$thf( a @ ( a @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) ))]]) ).
thf(22680,plain,
( ( b @ ( a @ greatest_lower_bound ) @ ( a @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[22319,47]) ).
thf(22684,plain,
( ( ( b @ ( a @ greatest_lower_bound ) )
!= ( b @ ( a @ greatest_lower_bound ) ) )
| ( ( identity @ ( a @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[35,22680]) ).
thf(22685,plain,
( ( identity @ ( a @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[22684:[]]) ).
thf(3810,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( identity @ greatest_lower_bound ) )
!= ( C @ ( B @ least_upper_bound ) @ ( B @ greatest_lower_bound ) ) )
| ( ( A @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[984,45]) ).
thf(3811,plain,
! [A: $i] :
( ( A @ ( identity @ least_upper_bound ) @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[3810:[bind(A,$thf( E @ ( identity @ least_upper_bound ) )),bind(B,$thf( identity )),bind(C,$thf( E ))]]) ).
thf(3899,plain,
! [A: $i] :
( ( A @ ( identity @ least_upper_bound ) @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= identity ),
inference(simp,[status(thm)],[3811]) ).
thf(938,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ greatest_lower_bound ) @ greatest_lower_bound ) )
!= ( a @ ( identity @ greatest_lower_bound ) ) )
| ( ( C @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[49,47]) ).
thf(960,plain,
! [C: $i,B: $i,A: $i] :
( ( C != a )
| ( ( B @ ( A @ greatest_lower_bound ) )
!= identity )
| ( ( C @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= identity ) ),
inference(simp,[status(thm)],[938]) ).
thf(970,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= identity )
| ( ( a @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= identity ) ),
inference(simp,[status(thm)],[960]) ).
thf(128388,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ greatest_lower_bound ) )
!= ( C @ ( B @ greatest_lower_bound ) ) )
| ( A != identity )
| ( ( a @ ( C @ greatest_lower_bound ) @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[37,970]) ).
thf(128389,plain,
! [A: $i] :
( ( A != identity )
| ( ( a @ ( A @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= identity ) ),
inference(pattern_uni,[status(thm)],[128388:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(129611,plain,
( ( a @ ( identity @ greatest_lower_bound ) @ ( identity @ greatest_lower_bound ) )
= identity ),
inference(simp,[status(thm)],[128389]) ).
thf(130767,plain,
( ( a @ ( identity @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[129611,984]) ).
thf(620,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) @ ( A @ least_upper_bound ) )
!= ( C @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) ) )
| ( A
= ( C @ ( a @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[43,362]) ).
thf(659,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= ( C @ ( a @ least_upper_bound ) ) )
| ( A != identity )
| ( A
= ( C @ ( a @ least_upper_bound ) ) ) ),
inference(simp,[status(thm)],[620]) ).
thf(674,plain,
! [B: $i,A: $i] :
( ( ( A @ ( identity @ greatest_lower_bound ) )
!= ( B @ ( a @ least_upper_bound ) ) )
| ( ( B @ ( a @ least_upper_bound ) )
= identity ) ),
inference(simp,[status(thm)],[659]) ).
thf(90513,plain,
! [B: $i,A: $i] :
( ( ( A @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( B @ ( a @ least_upper_bound ) ) )
| ( ( B @ ( a @ least_upper_bound ) )
= identity ) ),
inference(rewrite,[status(thm)],[674,984]) ).
thf(904,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ greatest_lower_bound ) @ greatest_lower_bound ) )
!= ( E @ ( D @ greatest_lower_bound ) ) )
| ( ( F @ ( C @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) @ multiply ) )
= ( F @ ( E @ multiply ) @ ( F @ ( D @ multiply ) @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[47,41]) ).
thf(905,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( D @ greatest_lower_bound ) @ ( C @ greatest_lower_bound ) @ multiply ) )
= ( B @ ( A @ multiply ) @ ( B @ ( D @ ( C @ greatest_lower_bound ) @ multiply ) @ greatest_lower_bound ) ) ),
inference(pattern_uni,[status(thm)],[904:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( G @ greatest_lower_bound ) )),bind(E,$thf( C ))]]) ).
thf(979,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( D @ greatest_lower_bound ) @ ( C @ greatest_lower_bound ) @ multiply ) )
= ( B @ ( A @ multiply ) @ ( B @ ( D @ ( C @ greatest_lower_bound ) @ multiply ) @ greatest_lower_bound ) ) ),
inference(simp,[status(thm)],[905]) ).
thf(154623,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( D @ greatest_lower_bound ) @ multiply ) @ ( B @ ( C @ multiply ) @ greatest_lower_bound ) )
= ( B @ ( A @ multiply ) @ ( B @ ( D @ multiply ) @ ( B @ ( C @ multiply ) @ greatest_lower_bound ) @ greatest_lower_bound ) ) ),
inference(rewrite,[status(thm)],[979,41]) ).
thf(713,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ least_upper_bound ) )
!= ( D @ ( C @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) @ ( C @ greatest_lower_bound ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[25,45]) ).
thf(714,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ least_upper_bound ) @ ( A @ greatest_lower_bound ) )
= A ),
inference(pattern_uni,[status(thm)],[713:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(509,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ greatest_lower_bound ) @ multiply ) )
!= ( c @ ( b @ multiply ) ) )
| ( ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[41,23]) ).
thf(518,plain,
! [C: $i,B: $i,A: $i] :
( ( C != c )
| ( ( B @ ( A @ greatest_lower_bound ) )
!= b )
| ( ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) ) ),
inference(simp,[status(thm)],[509]) ).
thf(529,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= b )
| ( ( c @ ( B @ multiply ) @ ( c @ ( A @ multiply ) @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) ) ),
inference(simp,[status(thm)],[518]) ).
thf(608,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
!= ( C @ ( B @ least_upper_bound ) ) )
| ( ( D @ ( A @ ( a @ least_upper_bound ) @ least_upper_bound ) )
= ( D @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[362,29]) ).
thf(609,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( a @ least_upper_bound ) @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
= ( A @ ( B @ ( a @ least_upper_bound ) @ least_upper_bound ) ) ),
inference(pattern_uni,[status(thm)],[608:[bind(A,$thf( F )),bind(B,$thf( identity )),bind(C,$thf( F @ ( a @ least_upper_bound ) )),bind(D,$thf( D ))]]) ).
thf(680,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( a @ least_upper_bound ) @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
= ( A @ ( B @ ( a @ least_upper_bound ) @ least_upper_bound ) ) ),
inference(simp,[status(thm)],[609]) ).
thf(95053,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ least_upper_bound ) @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
= ( A @ ( B @ least_upper_bound ) @ ( a @ least_upper_bound ) ) ),
inference(rewrite,[status(thm)],[680,29,4926]) ).
thf(1122,plain,
! [B: $i,A: $i] :
( ( ( b @ ( a @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[35,53]) ).
thf(1123,plain,
( ( a @ ( b @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[1122:[bind(A,$thf( a )),bind(B,$thf( b ))]]) ).
thf(4037,plain,
! [B: $i,A: $i] :
( ( ( a @ ( c @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[4030,53]) ).
thf(4038,plain,
( ( b @ ( a @ ( c @ greatest_lower_bound ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[4037:[bind(A,$thf( b )),bind(B,$thf( a @ ( c @ greatest_lower_bound ) ))]]) ).
thf(4204,plain,
( ( b @ ( a @ greatest_lower_bound ) @ ( c @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[4038,47]) ).
thf(153072,plain,
! [A: $i] :
( ( ( A @ ( c @ multiply ) @ ( A @ greatest_lower_bound ) )
!= ( c @ ( a @ multiply ) @ ( a @ greatest_lower_bound ) ) )
| ( A != a ) ),
inference(paramod_ordered,[status(thm)],[57665,150816]) ).
thf(153265,plain,
( ( ( a @ ( c @ multiply ) )
!= ( c @ ( a @ multiply ) ) )
| ( a != a ) ),
inference(simp,[status(thm)],[153072]) ).
thf(153324,plain,
( ( a @ ( c @ multiply ) )
!= ( c @ ( a @ multiply ) ) ),
inference(simp,[status(thm)],[153265]) ).
thf(399,plain,
! [A: $i] :
( ( ( A @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( identity @ ( a @ least_upper_bound ) ) )
| ( ( A @ ( a @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[290,236]) ).
thf(408,plain,
! [A: $i] :
( ( ( A @ ( identity @ least_upper_bound ) )
!= identity )
| ( a != a )
| ( ( A @ ( a @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[399]) ).
thf(424,plain,
! [A: $i] :
( ( ( A @ ( identity @ least_upper_bound ) )
!= identity )
| ( ( A @ ( a @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[408]) ).
thf(64798,plain,
! [C: $i,B: $i,A: $i] :
( ( ( a @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( A @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) ) )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[64523,213]) ).
thf(64799,plain,
( ( a @ ( a @ least_upper_bound ) @ ( a @ ( identity @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[64798:[bind(A,$thf( a @ ( identity @ least_upper_bound ) )),bind(B,$thf( a )),bind(C,$thf( a ))]]) ).
thf(79866,plain,
( ( a @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[64799,29]) ).
thf(79914,plain,
! [B: $i,A: $i] :
( ( ( a @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[79866,25]) ).
thf(79915,plain,
( ( identity @ ( a @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[79914:[bind(A,$thf( identity )),bind(B,$thf( a @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) ))]]) ).
thf(108263,plain,
( ( identity @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[79915,29]) ).
thf(4616,plain,
( ( ( b @ ( c @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) )
| ( ( c @ ( b @ multiply ) )
!= identity )
| ( identity != identity ) ),
inference(paramod_ordered,[status(thm)],[4521,1532]) ).
thf(4617,plain,
( ( ( b @ ( c @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(simp,[status(thm)],[4616]) ).
thf(4641,plain,
( ( ( b @ ( c @ greatest_lower_bound ) )
!= c )
| ( a != a )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(simp,[status(thm)],[4617]) ).
thf(4671,plain,
( ( ( b @ ( c @ greatest_lower_bound ) )
!= c )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(simp,[status(thm)],[4641]) ).
thf(7018,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ least_upper_bound ) @ ( A @ greatest_lower_bound ) )
!= ( b @ ( c @ greatest_lower_bound ) ) )
| ( A != c )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(paramod_ordered,[status(thm)],[45,4671]) ).
thf(7030,plain,
! [A: $i] :
( ( ( A @ ( c @ least_upper_bound ) )
!= b )
| ( c != c )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(simp,[status(thm)],[7018]) ).
thf(7065,plain,
! [A: $i] :
( ( ( A @ ( c @ least_upper_bound ) )
!= b )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(simp,[status(thm)],[7030]) ).
thf(26268,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ greatest_lower_bound ) @ least_upper_bound ) )
!= ( C @ ( c @ least_upper_bound ) ) )
| ( A != b )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(paramod_ordered,[status(thm)],[252,7065]) ).
thf(26321,plain,
! [B: $i,A: $i] :
( ( b != B )
| ( ( A @ ( b @ greatest_lower_bound ) )
!= c )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(simp,[status(thm)],[26268]) ).
thf(26354,plain,
! [A: $i] :
( ( ( A @ ( b @ greatest_lower_bound ) )
!= c )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(simp,[status(thm)],[26321]) ).
thf(55599,plain,
! [B: $i,A: $i] :
( ( ( A @ ( b @ multiply ) @ ( A @ ( a @ multiply ) @ greatest_lower_bound ) )
!= ( B @ ( b @ greatest_lower_bound ) ) )
| ( A != c )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(paramod_ordered,[status(thm)],[55432,26354]) ).
thf(55832,plain,
! [A: $i] :
( ( ( c @ ( b @ multiply ) )
!= A )
| ( ( c @ ( a @ multiply ) )
!= b )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(simp,[status(thm)],[55599]) ).
thf(55973,plain,
( ( ( c @ ( a @ multiply ) )
!= b )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(simp,[status(thm)],[55832]) ).
thf(166878,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ greatest_lower_bound ) @ least_upper_bound ) )
!= ( C @ ( a @ least_upper_bound ) ) )
| ( A != b ) ),
inference(paramod_ordered,[status(thm)],[252,158583]) ).
thf(167005,plain,
! [B: $i,A: $i] :
( ( b != B )
| ( ( A @ ( b @ greatest_lower_bound ) )
!= a ) ),
inference(simp,[status(thm)],[166878]) ).
thf(167069,plain,
! [A: $i] :
( ( A @ ( b @ greatest_lower_bound ) )
!= a ),
inference(simp,[status(thm)],[167005]) ).
thf(169433,plain,
! [B: $i,A: $i] :
( ( ( A @ ( b @ multiply ) @ ( A @ ( a @ multiply ) @ greatest_lower_bound ) )
!= ( B @ ( b @ greatest_lower_bound ) ) )
| ( A != a ) ),
inference(paramod_ordered,[status(thm)],[55432,167069]) ).
thf(169553,plain,
! [A: $i] :
( ( ( a @ ( b @ multiply ) )
!= A )
| ( ( a @ ( a @ multiply ) )
!= b ) ),
inference(simp,[status(thm)],[169433]) ).
thf(169628,plain,
( ( a @ ( a @ multiply ) )
!= b ),
inference(simp,[status(thm)],[169553]) ).
thf(912,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ greatest_lower_bound ) @ greatest_lower_bound ) )
!= ( D @ ( identity @ greatest_lower_bound ) ) )
| ( ( a @ ( C @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[47,477]) ).
thf(964,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C != D )
| ( ( B @ ( A @ greatest_lower_bound ) )
!= identity )
| ( ( a @ ( C @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[912]) ).
thf(974,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= identity )
| ( ( a @ ( C @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[964]) ).
thf(2621,plain,
( ( ( identity @ ( a @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) )
| ( ( c @ ( b @ multiply ) )
!= identity )
| ( identity != identity ) ),
inference(paramod_ordered,[status(thm)],[1175,1532]) ).
thf(2622,plain,
( ( ( identity @ ( a @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(simp,[status(thm)],[2621]) ).
thf(2632,plain,
( ( identity != c )
| ( a != a )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(simp,[status(thm)],[2622]) ).
thf(2653,plain,
( ( identity != c )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(simp,[status(thm)],[2632]) ).
thf(1566,plain,
( ( ( c @ ( a @ greatest_lower_bound ) )
!= ( b @ ( a @ greatest_lower_bound ) ) )
| ( ( c @ inverse )
!= b )
| ( identity != identity ) ),
inference(paramod_ordered,[status(thm)],[35,1462]) ).
thf(1567,plain,
( ( ( c @ ( a @ greatest_lower_bound ) )
!= ( b @ ( a @ greatest_lower_bound ) ) )
| ( ( c @ inverse )
!= b ) ),
inference(simp,[status(thm)],[1566]) ).
thf(1591,plain,
( ( c != b )
| ( a != a )
| ( ( c @ inverse )
!= b ) ),
inference(simp,[status(thm)],[1567]) ).
thf(1602,plain,
( ( c != b )
| ( ( c @ inverse )
!= b ) ),
inference(simp,[status(thm)],[1591]) ).
thf(150481,plain,
! [A: $i] :
( ( ( a @ ( a @ greatest_lower_bound ) )
!= ( A @ ( a @ greatest_lower_bound ) ) )
| ( a != a )
| ( ( c @ ( b @ multiply ) @ ( A @ greatest_lower_bound ) )
!= c ) ),
inference(paramod_ordered,[status(thm)],[54828,977]) ).
thf(150482,plain,
! [A: $i] :
( ( ( a @ ( a @ greatest_lower_bound ) )
!= ( A @ ( a @ greatest_lower_bound ) ) )
| ( ( c @ ( b @ multiply ) @ ( A @ greatest_lower_bound ) )
!= c ) ),
inference(simp,[status(thm)],[150481]) ).
thf(150483,plain,
( ( c @ ( b @ multiply ) @ ( a @ greatest_lower_bound ) )
!= c ),
inference(pattern_uni,[status(thm)],[150482:[bind(A,$thf( a ))]]) ).
thf(15539,plain,
! [B: $i,A: $i] :
( ( ( A @ ( identity @ greatest_lower_bound ) )
!= ( b @ ( B @ greatest_lower_bound ) ) )
| ( ( A @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= c )
| ( ( c @ inverse )
!= b ) ),
inference(paramod_ordered,[status(thm)],[984,13013]) ).
thf(15540,plain,
( ( ( b @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= c )
| ( ( c @ inverse )
!= b ) ),
inference(pattern_uni,[status(thm)],[15539:[bind(A,$thf( b )),bind(B,$thf( identity ))]]) ).
thf(31080,plain,
( ( ( b @ ( a @ greatest_lower_bound ) )
!= c )
| ( ( c @ inverse )
!= b ) ),
inference(rewrite,[status(thm)],[15540,37]) ).
thf(925,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ greatest_lower_bound ) )
!= ( C @ ( B @ greatest_lower_bound ) ) )
| ( ( D @ ( A @ greatest_lower_bound ) )
= ( D @ ( C @ greatest_lower_bound ) @ ( B @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,47]) ).
thf(926,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= ( B @ ( A @ greatest_lower_bound ) ) ),
inference(pattern_uni,[status(thm)],[925:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(989,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= ( B @ ( A @ greatest_lower_bound ) ) ),
inference(simp,[status(thm)],[926]) ).
thf(150977,plain,
! [A: $i] :
( ( ( A @ ( c @ multiply ) @ ( A @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) )
| ( A != a ) ),
inference(paramod_ordered,[status(thm)],[57665,150839]) ).
thf(151090,plain,
( ( ( a @ ( c @ multiply ) )
!= c )
| ( a != a ) ),
inference(simp,[status(thm)],[150977]) ).
thf(151171,plain,
( ( a @ ( c @ multiply ) )
!= c ),
inference(simp,[status(thm)],[151090]) ).
thf(151212,plain,
! [A: $i] :
( ( ( A @ ( A @ inverse @ multiply ) )
!= ( a @ ( c @ multiply ) ) )
| ( identity != c ) ),
inference(paramod_ordered,[status(thm)],[39,151171]) ).
thf(151217,plain,
! [A: $i] :
( ( A != a )
| ( ( A @ inverse )
!= c )
| ( identity != c ) ),
inference(simp,[status(thm)],[151212]) ).
thf(151225,plain,
( ( ( a @ inverse )
!= c )
| ( identity != c ) ),
inference(simp,[status(thm)],[151217]) ).
thf(150981,plain,
! [A: $i] :
( ( ( A @ ( A @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) )
| ( A != a ) ),
inference(paramod_ordered,[status(thm)],[37,150839]) ).
thf(151100,plain,
( ( c != a )
| ( a != a ) ),
inference(simp,[status(thm)],[150981]) ).
thf(151180,plain,
c != a,
inference(simp,[status(thm)],[151100]) ).
thf(18652,plain,
! [B: $i,A: $i] :
( ( ( b @ ( a @ greatest_lower_bound ) @ ( c @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( identity @ ( A @ least_upper_bound ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[18451,43]) ).
thf(18653,plain,
( ( identity @ ( c @ ( identity @ inverse @ multiply ) @ least_upper_bound ) )
= ( c @ ( identity @ inverse @ multiply ) ) ),
inference(pattern_uni,[status(thm)],[18652:[bind(A,$thf( c @ ( identity @ inverse @ multiply ) )),bind(B,$thf( b @ ( a @ greatest_lower_bound ) ))]]) ).
thf(802,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ least_upper_bound ) )
!= ( C @ ( a @ least_upper_bound ) ) )
| ( ( B @ ( A @ least_upper_bound ) @ ( identity @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[25,753]) ).
thf(803,plain,
! [A: $i] :
( ( a @ ( A @ least_upper_bound ) @ ( identity @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[802:[bind(A,$thf( A )),bind(B,$thf( a )),bind(C,$thf( A ))]]) ).
thf(1144,plain,
! [C: $i,B: $i,A: $i] :
( ( ( a @ ( A @ least_upper_bound ) @ ( identity @ greatest_lower_bound ) )
!= ( C @ ( B @ greatest_lower_bound ) ) )
| ( ( B @ ( C @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[803,53]) ).
thf(1145,plain,
! [A: $i] :
( ( identity @ ( a @ ( A @ least_upper_bound ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[1144:[bind(A,$thf( D )),bind(B,$thf( identity )),bind(C,$thf( a @ ( D @ least_upper_bound ) ))]]) ).
thf(1214,plain,
! [A: $i] :
( ( identity @ ( a @ ( A @ least_upper_bound ) @ greatest_lower_bound ) )
= identity ),
inference(simp,[status(thm)],[1145]) ).
thf(543,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( a @ ( A @ ( identity @ greatest_lower_bound ) @ least_upper_bound ) )
!= ( C @ ( B @ least_upper_bound ) ) )
| ( ( D @ ( a @ least_upper_bound ) )
= ( D @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[477,29]) ).
thf(544,plain,
! [B: $i,A: $i] :
( ( A @ ( a @ least_upper_bound ) @ ( B @ ( identity @ greatest_lower_bound ) @ least_upper_bound ) )
= ( A @ ( a @ least_upper_bound ) ) ),
inference(pattern_uni,[status(thm)],[543:[bind(A,$thf( F )),bind(B,$thf( F @ ( identity @ greatest_lower_bound ) )),bind(C,$thf( a )),bind(D,$thf( D ))]]) ).
thf(592,plain,
! [B: $i,A: $i] :
( ( A @ ( a @ least_upper_bound ) @ ( B @ ( identity @ greatest_lower_bound ) @ least_upper_bound ) )
= ( A @ ( a @ least_upper_bound ) ) ),
inference(simp,[status(thm)],[544]) ).
thf(66182,plain,
! [B: $i,A: $i] :
( ( A @ ( a @ least_upper_bound ) @ ( B @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) @ least_upper_bound ) )
= ( A @ ( a @ least_upper_bound ) ) ),
inference(rewrite,[status(thm)],[592,984]) ).
thf(55450,plain,
! [B: $i,A: $i] :
( ( ( A @ ( b @ multiply ) @ ( A @ ( a @ multiply ) @ greatest_lower_bound ) )
!= ( B @ ( b @ greatest_lower_bound ) ) )
| ( A != c )
| ( ( c @ inverse )
!= b ) ),
inference(paramod_ordered,[status(thm)],[55432,10827]) ).
thf(55916,plain,
! [A: $i] :
( ( ( c @ ( b @ multiply ) )
!= A )
| ( ( c @ ( a @ multiply ) )
!= b )
| ( ( c @ inverse )
!= b ) ),
inference(simp,[status(thm)],[55450]) ).
thf(56001,plain,
( ( ( c @ ( a @ multiply ) )
!= b )
| ( ( c @ inverse )
!= b ) ),
inference(simp,[status(thm)],[55916]) ).
thf(392,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ least_upper_bound ) )
!= ( C @ ( identity @ least_upper_bound ) ) )
| ( ( B @ ( A @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= ( C @ ( a @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[25,290]) ).
thf(393,plain,
! [A: $i] :
( ( identity @ ( A @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= ( A @ ( a @ least_upper_bound ) ) ),
inference(pattern_uni,[status(thm)],[392:[bind(A,$thf( A )),bind(B,$thf( identity )),bind(C,$thf( A ))]]) ).
thf(917,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ greatest_lower_bound ) @ greatest_lower_bound ) )
!= ( E @ ( D @ greatest_lower_bound ) ) )
| ( ( C @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) @ ( D @ least_upper_bound ) )
= D ) ),
inference(paramod_ordered,[status(thm)],[47,43]) ).
thf(918,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ greatest_lower_bound ) @ ( B @ greatest_lower_bound ) @ ( C @ ( B @ greatest_lower_bound ) @ least_upper_bound ) )
= ( C @ ( B @ greatest_lower_bound ) ) ),
inference(pattern_uni,[status(thm)],[917:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( C )),bind(D,$thf( G @ ( F @ greatest_lower_bound ) )),bind(E,$thf( C ))]]) ).
thf(985,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ greatest_lower_bound ) @ ( B @ greatest_lower_bound ) @ ( C @ ( B @ greatest_lower_bound ) @ least_upper_bound ) )
= ( C @ ( B @ greatest_lower_bound ) ) ),
inference(simp,[status(thm)],[918]) ).
thf(6069,plain,
! [B: $i,A: $i] :
( ( ( a @ ( identity @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[6003,53]) ).
thf(6070,plain,
( ( a @ ( a @ ( identity @ greatest_lower_bound ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[6069:[bind(A,$thf( a )),bind(B,$thf( a @ ( identity @ greatest_lower_bound ) ))]]) ).
thf(6192,plain,
( ( a @ ( a @ greatest_lower_bound ) @ ( identity @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[6070,47]) ).
thf(6221,plain,
! [A: $i] :
( ( ( A @ ( A @ greatest_lower_bound ) )
!= ( a @ ( a @ greatest_lower_bound ) ) )
| ( ( A @ ( identity @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[37,6192]) ).
thf(6222,plain,
( ( a @ ( identity @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[6221:[bind(A,$thf( a ))]]) ).
thf(6784,plain,
( ( a @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[6222,984]) ).
thf(545,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ least_upper_bound ) @ least_upper_bound ) )
!= ( a @ ( D @ ( identity @ greatest_lower_bound ) @ least_upper_bound ) ) )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[29,477]) ).
thf(587,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C != a )
| ( ( B @ ( A @ least_upper_bound ) )
!= ( D @ ( identity @ greatest_lower_bound ) ) )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[545]) ).
thf(598,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ least_upper_bound ) )
!= ( C @ ( identity @ greatest_lower_bound ) ) )
| ( ( a @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[587]) ).
thf(72520,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ least_upper_bound ) )
!= ( C @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) ) )
| ( ( a @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(rewrite,[status(thm)],[598,984]) ).
thf(29653,plain,
! [B: $i,A: $i] :
( ( ( a @ ( b @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[29532,53]) ).
thf(29654,plain,
( ( b @ ( a @ ( b @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[29653:[bind(A,$thf( b )),bind(B,$thf( a @ ( b @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) ))]]) ).
thf(30082,plain,
( ( b @ ( a @ greatest_lower_bound ) @ ( b @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[29654,47]) ).
thf(13565,plain,
! [B: $i,A: $i] :
( ( ( A @ ( identity @ multiply ) )
!= ( identity @ ( B @ multiply ) ) )
| ( ( c @ ( B @ multiply ) @ ( A @ greatest_lower_bound ) )
= ( identity @ ( B @ multiply ) ) ) ),
inference(paramod_ordered,[status(thm)],[55,294]) ).
thf(13566,plain,
( ( identity @ ( identity @ multiply ) )
= ( c @ ( identity @ multiply ) @ ( identity @ greatest_lower_bound ) ) ),
inference(pattern_uni,[status(thm)],[13565:[bind(A,$thf( identity )),bind(B,$thf( identity ))]]) ).
thf(13714,plain,
( ( c @ ( identity @ multiply ) @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[13566,55,984]) ).
thf(1234,plain,
! [B: $i,A: $i] :
( ( ( a @ ( b @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( identity @ ( A @ least_upper_bound ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[1123,43]) ).
thf(1235,plain,
( ( identity @ ( b @ least_upper_bound ) )
= b ),
inference(pattern_uni,[status(thm)],[1234:[bind(A,$thf( b )),bind(B,$thf( a ))]]) ).
thf(6624,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( b @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( b @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= ( B @ ( A @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[1235,214]) ).
thf(6625,plain,
( ( b @ ( identity @ least_upper_bound ) @ ( b @ least_upper_bound ) )
= ( identity @ ( b @ least_upper_bound ) ) ),
inference(pattern_uni,[status(thm)],[6624:[bind(A,$thf( b )),bind(B,$thf( identity ))]]) ).
thf(1805,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( b @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= b ) ),
inference(paramod_ordered,[status(thm)],[1235,25]) ).
thf(1806,plain,
( ( b @ ( identity @ least_upper_bound ) )
= b ),
inference(pattern_uni,[status(thm)],[1805:[bind(A,$thf( b )),bind(B,$thf( identity ))]]) ).
thf(9169,plain,
( ( b @ ( b @ least_upper_bound ) )
= b ),
inference(rewrite,[status(thm)],[6625,1235,1806]) ).
thf(74282,plain,
! [C: $i,B: $i,A: $i] :
( ( ( a @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
!= ( A @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) ) )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[73977,213]) ).
thf(74283,plain,
( ( identity @ ( identity @ least_upper_bound ) @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[74282:[bind(A,$thf( a @ ( a @ least_upper_bound ) )),bind(B,$thf( identity )),bind(C,$thf( identity ))]]) ).
thf(97277,plain,
( ( identity @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[74283,29]) ).
thf(519,plain,
! [C: $i,B: $i,A: $i] :
( ( C != c )
| ( ( B @ ( A @ greatest_lower_bound ) )
!= b )
| ( ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ greatest_lower_bound ) )
!= c )
| ( a != a ) ),
inference(simp,[status(thm)],[509]) ).
thf(530,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= b )
| ( ( c @ ( B @ multiply ) @ ( c @ ( A @ multiply ) @ greatest_lower_bound ) )
!= c ) ),
inference(simp,[status(thm)],[519]) ).
thf(18152,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= ( a @ ( c @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[53,18061]) ).
thf(18153,plain,
( ( c @ ( identity @ inverse @ multiply ) @ ( a @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[18152:[bind(A,$thf( c @ ( identity @ inverse @ multiply ) )),bind(B,$thf( a ))]]) ).
thf(19697,plain,
! [B: $i,A: $i] :
( ( ( c @ ( identity @ inverse @ multiply ) @ ( a @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[18153,53]) ).
thf(19698,plain,
( ( b @ ( c @ ( identity @ inverse @ multiply ) @ ( a @ greatest_lower_bound ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[19697:[bind(A,$thf( b )),bind(B,$thf( c @ ( identity @ inverse @ multiply ) @ ( a @ greatest_lower_bound ) ))]]) ).
thf(20578,plain,
( ( b @ ( c @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[19698,47]) ).
thf(20676,plain,
! [B: $i,A: $i] :
( ( ( b @ ( c @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[20578,53]) ).
thf(20677,plain,
( ( a @ ( b @ ( c @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[20676:[bind(A,$thf( a )),bind(B,$thf( b @ ( c @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) ))]]) ).
thf(21023,plain,
( ( a @ ( b @ greatest_lower_bound ) @ ( c @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[20677,47]) ).
thf(374,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ least_upper_bound ) @ least_upper_bound ) )
!= ( D @ ( identity @ least_upper_bound ) ) )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= ( D @ ( a @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[29,290]) ).
thf(409,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C != D )
| ( ( B @ ( A @ least_upper_bound ) )
!= identity )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= ( D @ ( a @ least_upper_bound ) ) ) ),
inference(simp,[status(thm)],[374]) ).
thf(425,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ least_upper_bound ) )
!= identity )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= ( C @ ( a @ least_upper_bound ) ) ) ),
inference(simp,[status(thm)],[409]) ).
thf(305,plain,
! [C: $i,B: $i,A: $i] :
( ( ( a @ ( identity @ greatest_lower_bound ) )
!= ( C @ ( B @ greatest_lower_bound ) ) )
| ( ( identity @ ( A @ multiply ) )
= ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[49,31]) ).
thf(306,plain,
! [A: $i] :
( ( a @ ( A @ multiply ) @ ( identity @ ( A @ multiply ) @ greatest_lower_bound ) )
= ( identity @ ( A @ multiply ) ) ),
inference(pattern_uni,[status(thm)],[305:[bind(A,$thf( A )),bind(B,$thf( identity )),bind(C,$thf( a ))]]) ).
thf(15147,plain,
! [A: $i] :
( ( a @ ( A @ multiply ) @ ( b @ ( A @ multiply ) @ ( a @ ( A @ multiply ) @ greatest_lower_bound ) @ greatest_lower_bound ) )
= ( b @ ( A @ multiply ) @ ( a @ ( A @ multiply ) @ greatest_lower_bound ) ) ),
inference(rewrite,[status(thm)],[306,301]) ).
thf(151002,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ least_upper_bound ) @ ( A @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) )
| ( A != a ) ),
inference(paramod_ordered,[status(thm)],[714,150839]) ).
thf(151151,plain,
! [A: $i] :
( ( ( a @ ( A @ least_upper_bound ) )
!= c )
| ( a != a ) ),
inference(simp,[status(thm)],[151002]) ).
thf(151205,plain,
! [A: $i] :
( ( a @ ( A @ least_upper_bound ) )
!= c ),
inference(simp,[status(thm)],[151151]) ).
thf(48233,plain,
! [B: $i,A: $i] :
( ( ( a @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( a != a )
| ( ( identity @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[48084,286]) ).
thf(48234,plain,
! [B: $i,A: $i] :
( ( ( a @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( identity @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[48233]) ).
thf(48235,plain,
( ( identity @ ( a @ ( identity @ least_upper_bound ) @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[48234:[bind(A,$thf( a )),bind(B,$thf( a @ ( identity @ least_upper_bound ) ))]]) ).
thf(56070,plain,
( ( identity @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[48235,4926]) ).
thf(56100,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[56070,25]) ).
thf(56101,plain,
( ( a @ ( identity @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[56100:[bind(A,$thf( a )),bind(B,$thf( identity @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) ))]]) ).
thf(65345,plain,
( ( a @ ( identity @ ( a @ least_upper_bound ) @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[56101,29]) ).
thf(375,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ least_upper_bound ) @ least_upper_bound ) )
!= ( D @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) ) )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= ( D @ ( a @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[29,290]) ).
thf(407,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C
!= ( D @ ( identity @ least_upper_bound ) ) )
| ( ( B @ ( A @ least_upper_bound ) )
!= a )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= ( D @ ( a @ least_upper_bound ) ) ) ),
inference(simp,[status(thm)],[375]) ).
thf(423,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ least_upper_bound ) )
!= a )
| ( ( C @ ( identity @ least_upper_bound ) @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= ( C @ ( a @ least_upper_bound ) ) ) ),
inference(simp,[status(thm)],[407]) ).
thf(132644,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( c @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( identity != identity )
| ( ( b @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[1157,972]) ).
thf(132645,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( c @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( b @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= identity ) ),
inference(simp,[status(thm)],[132644]) ).
thf(132646,plain,
( ( b @ ( identity @ greatest_lower_bound ) @ ( c @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[132645:[bind(A,$thf( c )),bind(B,$thf( identity ))]]) ).
thf(135668,plain,
( ( b @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) @ ( c @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[132646,984]) ).
thf(19,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ least_upper_bound ) @ ( A @ multiply ) )
= ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ least_upper_bound ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',monotony_lub1) ).
thf(58,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ least_upper_bound ) @ ( A @ multiply ) )
= ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ least_upper_bound ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(59,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ least_upper_bound ) )
= ( C @ ( B @ least_upper_bound ) @ ( A @ multiply ) ) ),
inference(lifteq,[status(thm)],[58]) ).
thf(433,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( identity @ greatest_lower_bound ) @ ( a @ least_upper_bound ) )
!= ( D @ ( C @ ( B @ least_upper_bound ) @ least_upper_bound ) ) )
| ( ( D @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[432,29]) ).
thf(474,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( identity @ greatest_lower_bound ) )
!= D )
| ( ( C @ ( B @ least_upper_bound ) )
!= a )
| ( ( D @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[433]) ).
thf(487,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ least_upper_bound ) )
!= a )
| ( ( A @ ( identity @ greatest_lower_bound ) @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[474]) ).
thf(44041,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ least_upper_bound ) )
!= a )
| ( ( A @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) )
= a ) ),
inference(rewrite,[status(thm)],[487,984]) ).
thf(87434,plain,
! [B: $i,A: $i] :
( ( ( a @ ( identity @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[87389,25]) ).
thf(87435,plain,
( ( identity @ ( a @ ( identity @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[87434:[bind(A,$thf( identity )),bind(B,$thf( a @ ( identity @ least_upper_bound ) ))]]) ).
thf(88248,plain,
( ( identity @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[87435,29]) ).
thf(88462,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( a != a )
| ( ( identity @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[88248,286]) ).
thf(88463,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( identity @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[88462]) ).
thf(88464,plain,
( ( identity @ ( identity @ ( a @ least_upper_bound ) @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[88463:[bind(A,$thf( identity )),bind(B,$thf( identity @ ( a @ least_upper_bound ) ))]]) ).
thf(118372,plain,
( ( identity @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[88464,4926]) ).
thf(118443,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[118372,25]) ).
thf(118444,plain,
( ( identity @ ( identity @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[118443:[bind(A,$thf( identity )),bind(B,$thf( identity @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) ))]]) ).
thf(147711,plain,
( ( identity @ ( identity @ ( identity @ least_upper_bound ) @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[118444,29]) ).
thf(619,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
!= ( C @ ( B @ greatest_lower_bound ) @ ( B @ least_upper_bound ) ) )
| ( ( A @ ( a @ least_upper_bound ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[362,43]) ).
thf(651,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( a @ least_upper_bound ) )
!= ( C @ ( B @ greatest_lower_bound ) ) )
| ( identity != B )
| ( ( A @ ( a @ least_upper_bound ) )
= B ) ),
inference(simp,[status(thm)],[619]) ).
thf(670,plain,
! [B: $i,A: $i] :
( ( ( A @ ( a @ least_upper_bound ) )
!= ( B @ ( identity @ greatest_lower_bound ) ) )
| ( ( A @ ( a @ least_upper_bound ) )
= identity ) ),
inference(simp,[status(thm)],[651]) ).
thf(85769,plain,
! [B: $i,A: $i] :
( ( ( A @ ( a @ least_upper_bound ) )
!= ( B @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) ) )
| ( ( A @ ( a @ least_upper_bound ) )
= identity ) ),
inference(rewrite,[status(thm)],[670,984]) ).
thf(3796,plain,
! [A: $i] :
( ( A @ ( a @ least_upper_bound ) @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[753,984]) ).
thf(169431,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ greatest_lower_bound ) )
!= ( C @ ( b @ greatest_lower_bound ) ) )
| ( ( B @ ( A @ greatest_lower_bound ) )
!= a ) ),
inference(paramod_ordered,[status(thm)],[53,167069]) ).
thf(169432,plain,
! [A: $i] :
( ( b @ ( A @ greatest_lower_bound ) )
!= a ),
inference(pattern_uni,[status(thm)],[169431:[bind(A,$thf( A )),bind(B,$thf( b )),bind(C,$thf( A ))]]) ).
thf(173268,plain,
! [B: $i,A: $i] :
( ( ( A @ ( b @ multiply ) @ ( A @ ( a @ multiply ) @ greatest_lower_bound ) )
!= ( b @ ( B @ greatest_lower_bound ) ) )
| ( A != a ) ),
inference(paramod_ordered,[status(thm)],[55432,169432]) ).
thf(173376,plain,
! [A: $i] :
( ( ( a @ ( b @ multiply ) )
!= b )
| ( ( a @ ( a @ multiply ) )
!= A ) ),
inference(simp,[status(thm)],[173268]) ).
thf(173481,plain,
( ( a @ ( b @ multiply ) )
!= b ),
inference(simp,[status(thm)],[173376]) ).
thf(88289,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[88248,25]) ).
thf(88290,plain,
( ( identity @ ( identity @ ( a @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[88289:[bind(A,$thf( identity )),bind(B,$thf( identity @ ( a @ least_upper_bound ) ))]]) ).
thf(91074,plain,
( ( identity @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[88290,29]) ).
thf(611,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ least_upper_bound ) @ least_upper_bound ) )
!= ( D @ ( a @ least_upper_bound ) ) )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
= ( D @ ( a @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[29,362]) ).
thf(655,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C != D )
| ( ( B @ ( A @ least_upper_bound ) )
!= a )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
= ( D @ ( a @ least_upper_bound ) ) ) ),
inference(simp,[status(thm)],[611]) ).
thf(672,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ least_upper_bound ) )
!= a )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
= ( C @ ( a @ least_upper_bound ) ) ) ),
inference(simp,[status(thm)],[655]) ).
thf(818,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( a @ least_upper_bound ) @ ( identity @ greatest_lower_bound ) )
!= ( D @ ( C @ greatest_lower_bound ) ) )
| ( ( identity @ ( B @ multiply ) )
= ( D @ ( B @ multiply ) @ ( C @ ( B @ multiply ) @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[753,31]) ).
thf(819,plain,
! [B: $i,A: $i] :
( ( B @ ( a @ least_upper_bound ) @ ( A @ multiply ) @ ( identity @ ( A @ multiply ) @ greatest_lower_bound ) )
= ( identity @ ( A @ multiply ) ) ),
inference(pattern_uni,[status(thm)],[818:[bind(A,$thf( F )),bind(B,$thf( B )),bind(C,$thf( identity )),bind(D,$thf( F @ ( a @ least_upper_bound ) ))]]) ).
thf(847,plain,
! [B: $i,A: $i] :
( ( B @ ( a @ least_upper_bound ) @ ( A @ multiply ) @ ( identity @ ( A @ multiply ) @ greatest_lower_bound ) )
= ( identity @ ( A @ multiply ) ) ),
inference(simp,[status(thm)],[819]) ).
thf(122185,plain,
! [B: $i,A: $i] :
( ( B @ ( a @ least_upper_bound ) @ ( A @ multiply ) @ ( b @ ( A @ multiply ) @ ( a @ ( A @ multiply ) @ greatest_lower_bound ) @ greatest_lower_bound ) )
= ( b @ ( A @ multiply ) @ ( a @ ( A @ multiply ) @ greatest_lower_bound ) ) ),
inference(rewrite,[status(thm)],[847,301]) ).
thf(4589,plain,
( ( ( b @ ( c @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) )
| ( ( c @ ( b @ multiply ) )
!= b )
| ( identity != identity ) ),
inference(paramod_ordered,[status(thm)],[4521,96]) ).
thf(4590,plain,
( ( ( b @ ( c @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) )
| ( ( c @ ( b @ multiply ) )
!= b ) ),
inference(simp,[status(thm)],[4589]) ).
thf(4647,plain,
( ( ( b @ ( c @ greatest_lower_bound ) )
!= c )
| ( a != a )
| ( ( c @ ( b @ multiply ) )
!= b ) ),
inference(simp,[status(thm)],[4590]) ).
thf(4676,plain,
( ( ( b @ ( c @ greatest_lower_bound ) )
!= c )
| ( ( c @ ( b @ multiply ) )
!= b ) ),
inference(simp,[status(thm)],[4647]) ).
thf(62793,plain,
! [A: $i] :
( ( ( A @ ( b @ multiply ) @ ( A @ greatest_lower_bound ) )
!= ( b @ ( c @ greatest_lower_bound ) ) )
| ( A != c )
| ( ( c @ ( b @ multiply ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[62679,4676]) ).
thf(63115,plain,
( ( ( c @ ( b @ multiply ) )
!= b )
| ( c != c )
| ( ( c @ ( b @ multiply ) )
!= b ) ),
inference(simp,[status(thm)],[62793]) ).
thf(63338,plain,
( ( c @ ( b @ multiply ) )
!= b ),
inference(simp,[status(thm)],[63115]) ).
thf(295,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ greatest_lower_bound ) @ ( A @ multiply ) )
!= ( c @ ( b @ multiply ) ) )
| ( ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ greatest_lower_bound ) )
!= b )
| ( ( c @ ( a @ greatest_lower_bound ) )
!= identity ) ),
inference(paramod_ordered,[status(thm)],[31,96]) ).
thf(320,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ greatest_lower_bound ) )
!= c )
| ( A != b )
| ( ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ greatest_lower_bound ) )
!= b )
| ( ( c @ ( a @ greatest_lower_bound ) )
!= identity ) ),
inference(simp,[status(thm)],[295]) ).
thf(323,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= c )
| ( ( B @ ( b @ multiply ) @ ( A @ ( b @ multiply ) @ greatest_lower_bound ) )
!= b )
| ( ( c @ ( a @ greatest_lower_bound ) )
!= identity ) ),
inference(simp,[status(thm)],[320]) ).
thf(692,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ least_upper_bound ) @ least_upper_bound ) )
!= ( E @ ( D @ least_upper_bound ) ) )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) @ ( D @ greatest_lower_bound ) )
= D ) ),
inference(paramod_ordered,[status(thm)],[29,45]) ).
thf(693,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) @ ( C @ ( B @ least_upper_bound ) @ greatest_lower_bound ) )
= ( C @ ( B @ least_upper_bound ) ) ),
inference(pattern_uni,[status(thm)],[692:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( C )),bind(D,$thf( G @ ( F @ least_upper_bound ) )),bind(E,$thf( C ))]]) ).
thf(769,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) @ ( C @ ( B @ least_upper_bound ) @ greatest_lower_bound ) )
= ( C @ ( B @ least_upper_bound ) ) ),
inference(simp,[status(thm)],[693]) ).
thf(910,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ least_upper_bound ) @ ( A @ greatest_lower_bound ) )
!= ( D @ ( C @ greatest_lower_bound ) ) )
| ( ( E @ ( A @ greatest_lower_bound ) )
= ( E @ ( D @ greatest_lower_bound ) @ ( C @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[45,47]) ).
thf(911,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ ( B @ least_upper_bound ) @ greatest_lower_bound ) @ ( B @ greatest_lower_bound ) )
= ( A @ ( B @ greatest_lower_bound ) ) ),
inference(pattern_uni,[status(thm)],[910:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( F )),bind(D,$thf( G @ ( F @ least_upper_bound ) ))]]) ).
thf(983,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ ( B @ least_upper_bound ) @ greatest_lower_bound ) @ ( B @ greatest_lower_bound ) )
= ( A @ ( B @ greatest_lower_bound ) ) ),
inference(simp,[status(thm)],[911]) ).
thf(175506,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
!= ( c @ ( b @ multiply ) @ ( a @ greatest_lower_bound ) ) )
| ( ( B @ ( A @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[989,23]) ).
thf(175847,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= ( c @ ( b @ multiply ) ) )
| ( A != a )
| ( B != c )
| ( A != a ) ),
inference(simp,[status(thm)],[175506]) ).
thf(176236,plain,
( ( c @ ( b @ multiply ) )
!= ( c @ ( a @ greatest_lower_bound ) ) ),
inference(simp,[status(thm)],[175847]) ).
thf(17222,plain,
! [B: $i,A: $i] :
( ( ( b @ ( identity @ inverse @ multiply ) @ ( a @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( identity @ ( A @ least_upper_bound ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[14060,43]) ).
thf(17223,plain,
( ( identity @ ( a @ ( identity @ inverse @ multiply ) @ least_upper_bound ) )
= ( a @ ( identity @ inverse @ multiply ) ) ),
inference(pattern_uni,[status(thm)],[17222:[bind(A,$thf( a @ ( identity @ inverse @ multiply ) )),bind(B,$thf( b @ ( identity @ inverse @ multiply ) ))]]) ).
thf(607,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
!= ( D @ ( C @ ( B @ least_upper_bound ) @ least_upper_bound ) ) )
| ( ( A @ ( a @ least_upper_bound ) )
= ( D @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[362,29]) ).
thf(660,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( a @ least_upper_bound ) )
!= D )
| ( ( C @ ( B @ least_upper_bound ) )
!= identity )
| ( ( A @ ( a @ least_upper_bound ) )
= ( D @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) ) ) ),
inference(simp,[status(thm)],[607]) ).
thf(675,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ least_upper_bound ) )
!= identity )
| ( ( A @ ( a @ least_upper_bound ) @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) )
= ( A @ ( a @ least_upper_bound ) ) ) ),
inference(simp,[status(thm)],[660]) ).
thf(383,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) @ ( A @ least_upper_bound ) )
!= ( C @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) ) )
| ( A
= ( C @ ( a @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[43,290]) ).
thf(410,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= ( C @ ( identity @ least_upper_bound ) ) )
| ( A != a )
| ( A
= ( C @ ( a @ least_upper_bound ) ) ) ),
inference(simp,[status(thm)],[383]) ).
thf(426,plain,
! [B: $i,A: $i] :
( ( ( A @ ( a @ greatest_lower_bound ) )
!= ( B @ ( identity @ least_upper_bound ) ) )
| ( ( B @ ( a @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[410]) ).
thf(99939,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( b @ least_upper_bound ) )
!= ( A @ ( B @ least_upper_bound ) ) )
| ( ( b @ ( A @ greatest_lower_bound ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[1235,714]) ).
thf(99940,plain,
( ( b @ ( identity @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[99939:[bind(A,$thf( identity )),bind(B,$thf( b ))]]) ).
thf(100686,plain,
( ( b @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[99940,984]) ).
thf(443,plain,
! [B: $i,A: $i] :
( ( ( A @ ( identity @ greatest_lower_bound ) @ ( a @ least_upper_bound ) )
!= ( B @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) ) )
| ( ( B @ ( a @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[432,290]) ).
thf(469,plain,
! [B: $i,A: $i] :
( ( ( A @ ( identity @ greatest_lower_bound ) )
!= ( B @ ( identity @ least_upper_bound ) ) )
| ( a != a )
| ( ( B @ ( a @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[443]) ).
thf(482,plain,
! [B: $i,A: $i] :
( ( ( A @ ( identity @ greatest_lower_bound ) )
!= ( B @ ( identity @ least_upper_bound ) ) )
| ( ( B @ ( a @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[469]) ).
thf(41517,plain,
! [B: $i,A: $i] :
( ( ( A @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( B @ ( identity @ least_upper_bound ) ) )
| ( ( B @ ( a @ least_upper_bound ) )
= a ) ),
inference(rewrite,[status(thm)],[482,984]) ).
thf(517,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ greatest_lower_bound ) @ multiply ) )
!= ( c @ ( b @ multiply ) ) )
| ( ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ greatest_lower_bound ) )
!= c )
| ( a != a ) ),
inference(simp,[status(thm)],[509]) ).
thf(528,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ greatest_lower_bound ) @ multiply ) )
!= ( c @ ( b @ multiply ) ) )
| ( ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ greatest_lower_bound ) )
!= c ) ),
inference(simp,[status(thm)],[517]) ).
thf(50948,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ greatest_lower_bound ) )
!= ( c @ ( b @ multiply ) ) )
| ( ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ greatest_lower_bound ) )
!= c ) ),
inference(rewrite,[status(thm)],[528,41]) ).
thf(727,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ least_upper_bound ) @ ( A @ greatest_lower_bound ) )
!= ( E @ ( D @ greatest_lower_bound ) ) )
| ( ( A @ ( C @ multiply ) )
= ( E @ ( C @ multiply ) @ ( D @ ( C @ multiply ) @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[45,31]) ).
thf(728,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ least_upper_bound ) @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ greatest_lower_bound ) )
= ( B @ ( A @ multiply ) ) ),
inference(pattern_uni,[status(thm)],[727:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( C )),bind(D,$thf( F )),bind(E,$thf( G @ ( F @ least_upper_bound ) ))]]) ).
thf(754,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ least_upper_bound ) @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ greatest_lower_bound ) )
= ( B @ ( A @ multiply ) ) ),
inference(simp,[status(thm)],[728]) ).
thf(26259,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ least_upper_bound ) )
!= ( C @ ( c @ least_upper_bound ) ) )
| ( ( B @ ( A @ least_upper_bound ) )
!= b )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(paramod_ordered,[status(thm)],[25,7065]) ).
thf(26260,plain,
! [A: $i] :
( ( ( c @ ( A @ least_upper_bound ) )
!= b )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(pattern_uni,[status(thm)],[26259:[bind(A,$thf( A )),bind(B,$thf( c )),bind(C,$thf( A ))]]) ).
thf(13793,plain,
! [B: $i,A: $i] :
( ( ( c @ ( identity @ multiply ) @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[13714,53]) ).
thf(13794,plain,
( ( a @ ( c @ ( identity @ multiply ) @ ( b @ greatest_lower_bound ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[13793:[bind(A,$thf( a )),bind(B,$thf( c @ ( identity @ multiply ) @ ( b @ greatest_lower_bound ) ))]]) ).
thf(14485,plain,
( ( a @ ( c @ ( identity @ multiply ) @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[13794,47]) ).
thf(14567,plain,
! [B: $i,A: $i] :
( ( ( a @ ( c @ ( identity @ multiply ) @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[14485,53]) ).
thf(14568,plain,
( ( b @ ( a @ ( c @ ( identity @ multiply ) @ greatest_lower_bound ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[14567:[bind(A,$thf( b )),bind(B,$thf( a @ ( c @ ( identity @ multiply ) @ greatest_lower_bound ) ))]]) ).
thf(14813,plain,
( ( b @ ( a @ greatest_lower_bound ) @ ( c @ ( identity @ multiply ) @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[14568,47]) ).
thf(490,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ greatest_lower_bound ) @ multiply ) )
!= ( c @ ( b @ multiply ) ) )
| ( ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ greatest_lower_bound ) )
!= b )
| ( ( c @ ( a @ greatest_lower_bound ) )
!= identity ) ),
inference(paramod_ordered,[status(thm)],[41,96]) ).
thf(520,plain,
! [C: $i,B: $i,A: $i] :
( ( C != c )
| ( ( B @ ( A @ greatest_lower_bound ) )
!= b )
| ( ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ greatest_lower_bound ) )
!= b )
| ( ( c @ ( a @ greatest_lower_bound ) )
!= identity ) ),
inference(simp,[status(thm)],[490]) ).
thf(531,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= b )
| ( ( c @ ( B @ multiply ) @ ( c @ ( A @ multiply ) @ greatest_lower_bound ) )
!= b )
| ( ( c @ ( a @ greatest_lower_bound ) )
!= identity ) ),
inference(simp,[status(thm)],[520]) ).
thf(100869,plain,
! [B: $i,A: $i] :
( ( ( b @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[100686,53]) ).
thf(100870,plain,
( ( a @ ( b @ ( b @ greatest_lower_bound ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[100869:[bind(A,$thf( a )),bind(B,$thf( b @ ( b @ greatest_lower_bound ) ))]]) ).
thf(102403,plain,
( ( a @ ( b @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[100870,47]) ).
thf(102588,plain,
! [B: $i,A: $i] :
( ( ( a @ ( b @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[102403,53]) ).
thf(102589,plain,
( ( b @ ( a @ ( b @ greatest_lower_bound ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[102588:[bind(A,$thf( b )),bind(B,$thf( a @ ( b @ greatest_lower_bound ) ))]]) ).
thf(103206,plain,
( ( b @ ( a @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[102589,47]) ).
thf(312,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ greatest_lower_bound ) @ ( A @ multiply ) )
!= ( c @ ( b @ multiply ) ) )
| ( ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[31,23]) ).
thf(316,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ greatest_lower_bound ) @ ( A @ multiply ) )
!= ( c @ ( b @ multiply ) ) )
| ( ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ greatest_lower_bound ) )
!= c )
| ( a != a ) ),
inference(simp,[status(thm)],[312]) ).
thf(330,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ greatest_lower_bound ) @ ( A @ multiply ) )
!= ( c @ ( b @ multiply ) ) )
| ( ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ greatest_lower_bound ) )
!= c ) ),
inference(simp,[status(thm)],[316]) ).
thf(23151,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ greatest_lower_bound ) )
!= ( c @ ( b @ multiply ) ) )
| ( ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ greatest_lower_bound ) )
!= c ) ),
inference(rewrite,[status(thm)],[330,31]) ).
thf(65382,plain,
! [B: $i,A: $i] :
( ( ( a @ ( identity @ ( a @ least_upper_bound ) @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[65345,25]) ).
thf(65383,plain,
( ( identity @ ( a @ ( identity @ ( a @ least_upper_bound ) @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[65382:[bind(A,$thf( identity )),bind(B,$thf( a @ ( identity @ ( a @ least_upper_bound ) @ least_upper_bound ) ))]]) ).
thf(80856,plain,
( ( identity @ ( a @ least_upper_bound ) @ ( identity @ ( a @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[65383,29]) ).
thf(57892,plain,
! [A: $i] :
( ( ( A @ ( c @ multiply ) @ ( A @ greatest_lower_bound ) )
!= ( b @ ( c @ greatest_lower_bound ) ) )
| ( A != c )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(paramod_ordered,[status(thm)],[57665,4671]) ).
thf(57974,plain,
( ( ( c @ ( c @ multiply ) )
!= b )
| ( c != c )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(simp,[status(thm)],[57892]) ).
thf(58226,plain,
( ( ( c @ ( c @ multiply ) )
!= b )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(simp,[status(thm)],[57974]) ).
thf(934,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( a @ least_upper_bound ) @ ( identity @ greatest_lower_bound ) )
!= ( C @ ( B @ greatest_lower_bound ) ) )
| ( ( D @ ( identity @ greatest_lower_bound ) )
= ( D @ ( C @ greatest_lower_bound ) @ ( B @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[753,47]) ).
thf(935,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( a @ least_upper_bound ) @ greatest_lower_bound ) @ ( identity @ greatest_lower_bound ) )
= ( A @ ( identity @ greatest_lower_bound ) ) ),
inference(pattern_uni,[status(thm)],[934:[bind(A,$thf( F )),bind(B,$thf( identity )),bind(C,$thf( F @ ( a @ least_upper_bound ) )),bind(D,$thf( D ))]]) ).
thf(991,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( a @ least_upper_bound ) @ greatest_lower_bound ) @ ( identity @ greatest_lower_bound ) )
= ( A @ ( identity @ greatest_lower_bound ) ) ),
inference(simp,[status(thm)],[935]) ).
thf(177859,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( a @ least_upper_bound ) @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= ( A @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) ) ),
inference(rewrite,[status(thm)],[991,984]) ).
thf(57717,plain,
! [B: $i,A: $i] :
( ( ( A @ ( c @ multiply ) @ ( A @ greatest_lower_bound ) )
!= ( b @ ( B @ greatest_lower_bound ) ) )
| ( A != c )
| ( ( c @ inverse )
!= b ) ),
inference(paramod_ordered,[status(thm)],[57665,13013]) ).
thf(58094,plain,
! [A: $i] :
( ( ( c @ ( c @ multiply ) )
!= b )
| ( c != A )
| ( ( c @ inverse )
!= b ) ),
inference(simp,[status(thm)],[57717]) ).
thf(58335,plain,
( ( ( c @ ( c @ multiply ) )
!= b )
| ( ( c @ inverse )
!= b ) ),
inference(simp,[status(thm)],[58094]) ).
thf(13567,plain,
! [B: $i,A: $i] :
( ( ( A @ ( identity @ multiply ) )
!= ( c @ ( B @ multiply ) ) )
| ( ( A @ ( identity @ ( B @ multiply ) @ greatest_lower_bound ) )
= ( identity @ ( B @ multiply ) ) ) ),
inference(paramod_ordered,[status(thm)],[55,294]) ).
thf(13568,plain,
( ( c @ ( identity @ ( identity @ multiply ) @ greatest_lower_bound ) )
= ( identity @ ( identity @ multiply ) ) ),
inference(pattern_uni,[status(thm)],[13567:[bind(A,$thf( c )),bind(B,$thf( identity ))]]) ).
thf(14158,plain,
( ( c @ ( b @ ( identity @ multiply ) @ ( a @ ( identity @ multiply ) @ greatest_lower_bound ) @ greatest_lower_bound ) )
= ( b @ ( identity @ multiply ) @ ( a @ ( identity @ multiply ) @ greatest_lower_bound ) ) ),
inference(rewrite,[status(thm)],[13568,301]) ).
thf(507,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ greatest_lower_bound ) @ multiply ) )
!= ( D @ ( identity @ multiply ) ) )
| ( ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ greatest_lower_bound ) )
= D ) ),
inference(paramod_ordered,[status(thm)],[41,55]) ).
thf(514,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C != D )
| ( ( B @ ( A @ greatest_lower_bound ) )
!= identity )
| ( ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ greatest_lower_bound ) )
= D ) ),
inference(simp,[status(thm)],[507]) ).
thf(525,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= identity )
| ( ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ greatest_lower_bound ) )
= C ) ),
inference(simp,[status(thm)],[514]) ).
thf(317,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ greatest_lower_bound ) )
!= c )
| ( A != b )
| ( ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) ) ),
inference(simp,[status(thm)],[312]) ).
thf(331,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= c )
| ( ( B @ ( b @ multiply ) @ ( A @ ( b @ multiply ) @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) ) ),
inference(simp,[status(thm)],[317]) ).
thf(3801,plain,
! [A: $i] :
( ( a @ ( A @ least_upper_bound ) @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[803,984]) ).
thf(929,plain,
! [C: $i,B: $i,A: $i] :
( ( ( c @ ( identity @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( C @ ( identity @ greatest_lower_bound ) )
= ( C @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[33,47]) ).
thf(930,plain,
! [A: $i] :
( ( A @ ( c @ greatest_lower_bound ) @ ( identity @ greatest_lower_bound ) )
= ( A @ ( identity @ greatest_lower_bound ) ) ),
inference(pattern_uni,[status(thm)],[929:[bind(A,$thf( identity )),bind(B,$thf( c ))]]) ).
thf(990,plain,
! [A: $i] :
( ( A @ ( c @ greatest_lower_bound ) @ ( identity @ greatest_lower_bound ) )
= ( A @ ( identity @ greatest_lower_bound ) ) ),
inference(simp,[status(thm)],[930]) ).
thf(176323,plain,
! [A: $i] :
( ( A @ ( c @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= ( A @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) ) ),
inference(rewrite,[status(thm)],[990,984]) ).
thf(18455,plain,
( ( ( b @ ( a @ greatest_lower_bound ) )
!= ( b @ ( a @ greatest_lower_bound ) ) )
| ( ( identity @ ( c @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[35,18451]) ).
thf(18456,plain,
( ( identity @ ( c @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[18455:[]]) ).
thf(13541,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ inverse @ multiply ) )
!= ( c @ ( B @ multiply ) ) )
| ( ( identity @ ( identity @ ( B @ multiply ) @ greatest_lower_bound ) )
= ( identity @ ( B @ multiply ) ) ) ),
inference(paramod_ordered,[status(thm)],[39,294]) ).
thf(13542,plain,
( ( identity @ ( identity @ ( c @ inverse @ multiply ) @ greatest_lower_bound ) )
= ( identity @ ( c @ inverse @ multiply ) ) ),
inference(pattern_uni,[status(thm)],[13541:[bind(A,$thf( c )),bind(B,$thf( c @ inverse ))]]) ).
thf(16678,plain,
( ( identity @ ( b @ ( c @ inverse @ multiply ) @ ( a @ ( c @ inverse @ multiply ) @ greatest_lower_bound ) @ greatest_lower_bound ) )
= ( b @ ( c @ inverse @ multiply ) @ ( a @ ( c @ inverse @ multiply ) @ greatest_lower_bound ) ) ),
inference(rewrite,[status(thm)],[13542,301]) ).
thf(173228,plain,
! [B: $i,A: $i] :
( ( ( A @ ( c @ multiply ) @ ( A @ greatest_lower_bound ) )
!= ( b @ ( B @ greatest_lower_bound ) ) )
| ( A != a ) ),
inference(paramod_ordered,[status(thm)],[57665,169432]) ).
thf(173367,plain,
! [A: $i] :
( ( ( a @ ( c @ multiply ) )
!= b )
| ( a != A ) ),
inference(simp,[status(thm)],[173228]) ).
thf(173468,plain,
( ( a @ ( c @ multiply ) )
!= b ),
inference(simp,[status(thm)],[173367]) ).
thf(108327,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[108263,25]) ).
thf(108328,plain,
( ( a @ ( identity @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[108327:[bind(A,$thf( a )),bind(B,$thf( identity @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) ))]]) ).
thf(125892,plain,
( ( a @ ( identity @ least_upper_bound ) @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[108328,29]) ).
thf(59339,plain,
! [B: $i,A: $i] :
( ( ( A @ ( a @ multiply ) @ ( A @ greatest_lower_bound ) )
!= ( B @ ( identity @ greatest_lower_bound ) ) )
| ( A
= ( B @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[59231,984]) ).
thf(59340,plain,
( ( identity @ ( a @ multiply ) @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[59339:[bind(A,$thf( identity )),bind(B,$thf( identity @ ( a @ multiply ) ))]]) ).
thf(75272,plain,
( ( b @ ( a @ multiply ) @ ( a @ ( a @ multiply ) @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[59340,301]) ).
thf(91290,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( a != a )
| ( ( identity @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[91074,286]) ).
thf(91291,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( identity @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[91290]) ).
thf(91292,plain,
( ( identity @ ( identity @ ( identity @ least_upper_bound ) @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[91291:[bind(A,$thf( a )),bind(B,$thf( identity @ ( identity @ least_upper_bound ) ))]]) ).
thf(119620,plain,
( ( identity @ ( identity @ least_upper_bound ) @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[91292,4926]) ).
thf(225,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) @ ( A @ least_upper_bound ) )
!= ( D @ ( C @ least_upper_bound ) ) )
| ( ( E @ ( A @ least_upper_bound ) )
= ( E @ ( D @ least_upper_bound ) @ ( C @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[43,29]) ).
thf(226,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ ( B @ greatest_lower_bound ) @ least_upper_bound ) @ ( B @ least_upper_bound ) )
= ( A @ ( B @ least_upper_bound ) ) ),
inference(pattern_uni,[status(thm)],[225:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( F )),bind(D,$thf( G @ ( F @ greatest_lower_bound ) ))]]) ).
thf(250,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ ( B @ greatest_lower_bound ) @ least_upper_bound ) @ ( B @ least_upper_bound ) )
= ( A @ ( B @ least_upper_bound ) ) ),
inference(simp,[status(thm)],[226]) ).
thf(966,plain,
! [C: $i,B: $i,A: $i] :
( ( C
!= ( c @ ( b @ multiply ) ) )
| ( ( B @ ( A @ greatest_lower_bound ) )
!= a )
| ( ( C @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) ) ),
inference(simp,[status(thm)],[944]) ).
thf(976,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= a )
| ( ( c @ ( b @ multiply ) @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) ) ),
inference(simp,[status(thm)],[966]) ).
thf(492,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ inverse @ multiply ) )
!= ( D @ ( C @ ( B @ greatest_lower_bound ) @ multiply ) ) )
| ( ( D @ ( C @ multiply ) @ ( D @ ( B @ multiply ) @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[39,41]) ).
thf(513,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A != D )
| ( ( A @ inverse )
!= ( C @ ( B @ greatest_lower_bound ) ) )
| ( ( D @ ( C @ multiply ) @ ( D @ ( B @ multiply ) @ greatest_lower_bound ) )
= identity ) ),
inference(simp,[status(thm)],[492]) ).
thf(524,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ inverse )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ greatest_lower_bound ) )
= identity ) ),
inference(simp,[status(thm)],[513]) ).
thf(118797,plain,
! [C: $i,B: $i,A: $i] :
( ( ( identity @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
!= ( A @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) ) )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[118372,213]) ).
thf(118798,plain,
( ( a @ ( identity @ least_upper_bound ) @ ( identity @ ( identity @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[118797:[bind(A,$thf( identity @ ( identity @ least_upper_bound ) )),bind(B,$thf( identity )),bind(C,$thf( a ))]]) ).
thf(149066,plain,
( ( a @ ( identity @ least_upper_bound ) @ ( identity @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[118798,29]) ).
thf(152057,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( c @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( identity != identity )
| ( ( c @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[1157,978]) ).
thf(152058,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( c @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( c @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= identity ) ),
inference(simp,[status(thm)],[152057]) ).
thf(152059,plain,
( ( c @ ( identity @ greatest_lower_bound ) @ ( c @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[152058:[bind(A,$thf( c )),bind(B,$thf( identity ))]]) ).
thf(158585,plain,
( ( c @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) @ ( c @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[152059,984]) ).
thf(151011,plain,
! [A: $i] :
( ( ( A @ ( a @ multiply ) @ ( A @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) )
| ( A != a ) ),
inference(paramod_ordered,[status(thm)],[59231,150839]) ).
thf(151149,plain,
( ( ( a @ ( a @ multiply ) )
!= c )
| ( a != a ) ),
inference(simp,[status(thm)],[151011]) ).
thf(151206,plain,
( ( a @ ( a @ multiply ) )
!= c ),
inference(simp,[status(thm)],[151149]) ).
thf(550,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) @ ( A @ least_upper_bound ) )
!= ( a @ ( C @ ( identity @ greatest_lower_bound ) @ least_upper_bound ) ) )
| ( A = a ) ),
inference(paramod_ordered,[status(thm)],[43,477]) ).
thf(582,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= a )
| ( A
!= ( C @ ( identity @ greatest_lower_bound ) ) )
| ( A = a ) ),
inference(simp,[status(thm)],[550]) ).
thf(593,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( identity @ greatest_lower_bound ) @ greatest_lower_bound ) )
!= a )
| ( ( B @ ( identity @ greatest_lower_bound ) )
= a ) ),
inference(simp,[status(thm)],[582]) ).
thf(67254,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ greatest_lower_bound ) @ ( identity @ greatest_lower_bound ) )
!= a )
| ( ( B @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
= a ) ),
inference(rewrite,[status(thm)],[593,984,47]) ).
thf(434,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( identity @ greatest_lower_bound ) @ ( a @ least_upper_bound ) )
!= ( C @ ( B @ least_upper_bound ) ) )
| ( ( D @ ( a @ least_upper_bound ) )
= ( D @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[432,29]) ).
thf(435,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( identity @ greatest_lower_bound ) @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= ( A @ ( a @ least_upper_bound ) ) ),
inference(pattern_uni,[status(thm)],[434:[bind(A,$thf( F )),bind(B,$thf( a )),bind(C,$thf( F @ ( identity @ greatest_lower_bound ) )),bind(D,$thf( D ))]]) ).
thf(479,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( identity @ greatest_lower_bound ) @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= ( A @ ( a @ least_upper_bound ) ) ),
inference(simp,[status(thm)],[435]) ).
thf(39124,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= ( A @ ( a @ least_upper_bound ) ) ),
inference(rewrite,[status(thm)],[479,984]) ).
thf(132684,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( b @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( identity != identity )
| ( ( b @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[1193,972]) ).
thf(132685,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( b @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( b @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= identity ) ),
inference(simp,[status(thm)],[132684]) ).
thf(132686,plain,
( ( b @ ( identity @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[132685:[bind(A,$thf( b )),bind(B,$thf( identity ))]]) ).
thf(136826,plain,
( ( b @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[132686,984]) ).
thf(152840,plain,
! [A: $i] :
( ( ( A @ ( b @ multiply ) @ ( A @ ( a @ multiply ) @ greatest_lower_bound ) )
!= ( c @ ( b @ multiply ) @ ( a @ greatest_lower_bound ) ) )
| ( A != c ) ),
inference(paramod_ordered,[status(thm)],[55432,150483]) ).
thf(152948,plain,
( ( ( c @ ( b @ multiply ) )
!= ( c @ ( b @ multiply ) ) )
| ( ( c @ ( a @ multiply ) )
!= a ) ),
inference(simp,[status(thm)],[152840]) ).
thf(153026,plain,
( ( c @ ( a @ multiply ) )
!= a ),
inference(simp,[status(thm)],[152948]) ).
thf(35900,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) @ ( A @ least_upper_bound ) )
!= ( C @ ( identity @ least_upper_bound ) ) )
| ( A != identity )
| ( ( C @ ( a @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[43,424]) ).
thf(35901,plain,
! [A: $i] :
( ( identity != identity )
| ( ( A @ ( identity @ greatest_lower_bound ) @ ( a @ least_upper_bound ) )
= a ) ),
inference(pattern_uni,[status(thm)],[35900:[bind(A,$thf( identity )),bind(B,$thf( E )),bind(C,$thf( E @ ( identity @ greatest_lower_bound ) ))]]) ).
thf(35979,plain,
! [A: $i] :
( ( A @ ( identity @ greatest_lower_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(simp,[status(thm)],[35901]) ).
thf(37216,plain,
! [A: $i] :
( ( A @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[35979,984]) ).
thf(166850,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ least_upper_bound ) )
!= ( C @ ( a @ least_upper_bound ) ) )
| ( ( B @ ( A @ least_upper_bound ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[25,158583]) ).
thf(166851,plain,
! [A: $i] :
( ( a @ ( A @ least_upper_bound ) )
!= b ),
inference(pattern_uni,[status(thm)],[166850:[bind(A,$thf( A )),bind(B,$thf( a )),bind(C,$thf( A ))]]) ).
thf(153132,plain,
! [A: $i] :
( ( ( A @ ( b @ multiply ) @ ( A @ greatest_lower_bound ) )
!= ( c @ ( a @ multiply ) @ ( a @ greatest_lower_bound ) ) )
| ( A != a ) ),
inference(paramod_ordered,[status(thm)],[62679,150816]) ).
thf(153212,plain,
( ( ( a @ ( b @ multiply ) )
!= ( c @ ( a @ multiply ) ) )
| ( a != a ) ),
inference(simp,[status(thm)],[153132]) ).
thf(153294,plain,
( ( a @ ( b @ multiply ) )
!= ( c @ ( a @ multiply ) ) ),
inference(simp,[status(thm)],[153212]) ).
thf(55057,plain,
( ( ( c @ ( b @ multiply ) @ ( a @ greatest_lower_bound ) )
!= ( a @ ( a @ greatest_lower_bound ) ) )
| ( ( c @ ( a @ greatest_lower_bound ) )
!= a ) ),
inference(paramod_ordered,[status(thm)],[54828,23]) ).
thf(55298,plain,
( ( ( c @ ( b @ multiply ) )
!= a )
| ( a != a )
| ( ( c @ ( a @ greatest_lower_bound ) )
!= a ) ),
inference(simp,[status(thm)],[55057]) ).
thf(55309,plain,
( ( ( c @ ( b @ multiply ) )
!= a )
| ( ( c @ ( a @ greatest_lower_bound ) )
!= a ) ),
inference(simp,[status(thm)],[55298]) ).
thf(63531,plain,
! [A: $i] :
( ( ( A @ ( a @ multiply ) @ ( A @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) )
| ( ( c @ ( b @ multiply ) )
!= a )
| ( A != a ) ),
inference(paramod_ordered,[status(thm)],[59231,55309]) ).
thf(63603,plain,
( ( ( a @ ( a @ multiply ) )
!= c )
| ( a != a )
| ( ( c @ ( b @ multiply ) )
!= a ) ),
inference(simp,[status(thm)],[63531]) ).
thf(63681,plain,
( ( ( a @ ( a @ multiply ) )
!= c )
| ( ( c @ ( b @ multiply ) )
!= a ) ),
inference(simp,[status(thm)],[63603]) ).
thf(84101,plain,
! [A: $i] :
( ( ( A @ ( A @ inverse @ multiply ) )
!= ( a @ ( a @ multiply ) ) )
| ( identity != c )
| ( ( c @ ( b @ multiply ) )
!= a ) ),
inference(paramod_ordered,[status(thm)],[39,63681]) ).
thf(84117,plain,
! [A: $i] :
( ( A != a )
| ( ( A @ inverse )
!= a )
| ( identity != c )
| ( ( c @ ( b @ multiply ) )
!= a ) ),
inference(simp,[status(thm)],[84101]) ).
thf(84128,plain,
( ( ( a @ inverse )
!= a )
| ( identity != c )
| ( ( c @ ( b @ multiply ) )
!= a ) ),
inference(simp,[status(thm)],[84117]) ).
thf(164891,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ greatest_lower_bound ) )
!= ( C @ ( c @ greatest_lower_bound ) ) )
| ( ( B @ ( A @ greatest_lower_bound ) )
!= a ) ),
inference(paramod_ordered,[status(thm)],[53,158533]) ).
thf(164892,plain,
! [A: $i] :
( ( c @ ( A @ greatest_lower_bound ) )
!= a ),
inference(pattern_uni,[status(thm)],[164891:[bind(A,$thf( A )),bind(B,$thf( c )),bind(C,$thf( A ))]]) ).
thf(46035,plain,
! [C: $i,B: $i,A: $i] :
( ( ( a @ ( a @ least_upper_bound ) @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( A @ ( C @ least_upper_bound ) @ ( B @ least_upper_bound ) ) )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[45799,213]) ).
thf(46036,plain,
( ( identity @ ( a @ least_upper_bound ) @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[46035:[bind(A,$thf( a @ ( a @ least_upper_bound ) )),bind(B,$thf( a )),bind(C,$thf( identity ))]]) ).
thf(53766,plain,
( ( identity @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) @ ( a @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[46036,29]) ).
thf(3930,plain,
( ( ( c @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) )
| ( ( c @ inverse )
!= b )
| ( identity != identity ) ),
inference(paramod_ordered,[status(thm)],[3795,1462]) ).
thf(3931,plain,
( ( ( c @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) )
| ( ( c @ inverse )
!= b ) ),
inference(simp,[status(thm)],[3930]) ).
thf(3990,plain,
( ( ( c @ ( b @ greatest_lower_bound ) )
!= c )
| ( a != a )
| ( ( c @ inverse )
!= b ) ),
inference(simp,[status(thm)],[3931]) ).
thf(4014,plain,
( ( ( c @ ( b @ greatest_lower_bound ) )
!= c )
| ( ( c @ inverse )
!= b ) ),
inference(simp,[status(thm)],[3990]) ).
thf(380,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( C @ ( B @ greatest_lower_bound ) @ ( B @ least_upper_bound ) ) )
| ( ( A @ ( a @ least_upper_bound ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[290,43]) ).
thf(405,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( identity @ least_upper_bound ) )
!= ( C @ ( B @ greatest_lower_bound ) ) )
| ( a != B )
| ( ( A @ ( a @ least_upper_bound ) )
= B ) ),
inference(simp,[status(thm)],[380]) ).
thf(422,plain,
! [B: $i,A: $i] :
( ( ( A @ ( identity @ least_upper_bound ) )
!= ( B @ ( a @ greatest_lower_bound ) ) )
| ( ( A @ ( a @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[405]) ).
thf(296,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ greatest_lower_bound ) @ ( A @ multiply ) )
!= ( D @ ( D @ inverse @ multiply ) ) )
| ( ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[31,39]) ).
thf(297,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ greatest_lower_bound ) @ inverse @ multiply ) @ ( A @ ( B @ ( A @ greatest_lower_bound ) @ inverse @ multiply ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[296:[bind(A,$thf( G @ ( F @ greatest_lower_bound ) @ inverse )),bind(B,$thf( F )),bind(C,$thf( G )),bind(D,$thf( G @ ( F @ greatest_lower_bound ) ))]]) ).
thf(326,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ greatest_lower_bound ) @ inverse @ multiply ) @ ( A @ ( B @ ( A @ greatest_lower_bound ) @ inverse @ multiply ) @ greatest_lower_bound ) )
= identity ),
inference(simp,[status(thm)],[297]) ).
thf(96216,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[96170,25]) ).
thf(96217,plain,
( ( identity @ ( identity @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[96216:[bind(A,$thf( identity )),bind(B,$thf( identity @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) ))]]) ).
thf(123383,plain,
( ( identity @ ( identity @ least_upper_bound ) @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[96217,29]) ).
thf(18537,plain,
! [B: $i,A: $i] :
( ( ( b @ ( a @ greatest_lower_bound ) @ ( c @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( A @ ( identity @ least_upper_bound ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[18451,252]) ).
thf(18538,plain,
( ( c @ ( identity @ inverse @ multiply ) @ ( identity @ least_upper_bound ) )
= ( c @ ( identity @ inverse @ multiply ) ) ),
inference(pattern_uni,[status(thm)],[18537:[bind(A,$thf( c @ ( identity @ inverse @ multiply ) )),bind(B,$thf( b @ ( a @ greatest_lower_bound ) ))]]) ).
thf(502,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ greatest_lower_bound ) @ multiply ) )
!= ( c @ ( b @ multiply ) ) )
| ( c != b )
| ( ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ greatest_lower_bound ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[41,182]) ).
thf(521,plain,
! [C: $i,B: $i,A: $i] :
( ( C != c )
| ( ( B @ ( A @ greatest_lower_bound ) )
!= b )
| ( c != b )
| ( ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ greatest_lower_bound ) )
!= b ) ),
inference(simp,[status(thm)],[502]) ).
thf(532,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= b )
| ( c != b )
| ( ( c @ ( B @ multiply ) @ ( c @ ( A @ multiply ) @ greatest_lower_bound ) )
!= b ) ),
inference(simp,[status(thm)],[521]) ).
thf(30325,plain,
( ( ( b @ ( a @ greatest_lower_bound ) )
!= ( b @ ( a @ greatest_lower_bound ) ) )
| ( ( identity @ ( b @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[35,30082]) ).
thf(30326,plain,
( ( identity @ ( b @ ( identity @ inverse @ multiply ) @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[30325:[]]) ).
thf(3969,plain,
( ( ( c @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) )
| ( ( c @ ( b @ multiply ) )
!= identity )
| ( identity != identity ) ),
inference(paramod_ordered,[status(thm)],[3795,1532]) ).
thf(3970,plain,
( ( ( c @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) )
!= ( c @ ( a @ greatest_lower_bound ) ) )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(simp,[status(thm)],[3969]) ).
thf(3981,plain,
( ( ( c @ ( b @ greatest_lower_bound ) )
!= c )
| ( a != a )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(simp,[status(thm)],[3970]) ).
thf(4007,plain,
( ( ( c @ ( b @ greatest_lower_bound ) )
!= c )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(simp,[status(thm)],[3981]) ).
thf(152112,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( b @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( identity != identity )
| ( ( c @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[1193,978]) ).
thf(152113,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( b @ greatest_lower_bound ) )
!= ( B @ ( A @ greatest_lower_bound ) ) )
| ( ( c @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= identity ) ),
inference(simp,[status(thm)],[152112]) ).
thf(152114,plain,
( ( c @ ( identity @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
= identity ),
inference(pattern_uni,[status(thm)],[152113:[bind(A,$thf( b )),bind(B,$thf( identity ))]]) ).
thf(159862,plain,
( ( c @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) @ ( b @ greatest_lower_bound ) )
= identity ),
inference(rewrite,[status(thm)],[152114,984]) ).
thf(313,plain,
! [C: $i,B: $i,A: $i] :
( ( ( b @ ( identity @ greatest_lower_bound ) )
!= ( C @ ( B @ greatest_lower_bound ) ) )
| ( ( identity @ ( A @ multiply ) )
= ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[51,31]) ).
thf(314,plain,
! [A: $i] :
( ( b @ ( A @ multiply ) @ ( identity @ ( A @ multiply ) @ greatest_lower_bound ) )
= ( identity @ ( A @ multiply ) ) ),
inference(pattern_uni,[status(thm)],[313:[bind(A,$thf( A )),bind(B,$thf( identity )),bind(C,$thf( b ))]]) ).
thf(15617,plain,
! [A: $i] :
( ( b @ ( A @ multiply ) @ ( b @ ( A @ multiply ) @ ( a @ ( A @ multiply ) @ greatest_lower_bound ) @ greatest_lower_bound ) )
= ( b @ ( A @ multiply ) @ ( a @ ( A @ multiply ) @ greatest_lower_bound ) ) ),
inference(rewrite,[status(thm)],[314,301]) ).
thf(921,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ greatest_lower_bound ) @ greatest_lower_bound ) )
!= ( D @ ( D @ greatest_lower_bound ) ) )
| ( ( C @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= D ) ),
inference(paramod_ordered,[status(thm)],[47,37]) ).
thf(922,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ greatest_lower_bound ) @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= ( B @ ( A @ greatest_lower_bound ) ) ),
inference(pattern_uni,[status(thm)],[921:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( H @ ( G @ greatest_lower_bound ) )),bind(D,$thf( H @ ( G @ greatest_lower_bound ) ))]]) ).
thf(987,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ greatest_lower_bound ) @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= ( B @ ( A @ greatest_lower_bound ) ) ),
inference(simp,[status(thm)],[922]) ).
thf(6639,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( c @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( c @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= ( B @ ( A @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[1308,214]) ).
thf(6640,plain,
( ( c @ ( identity @ least_upper_bound ) @ ( c @ least_upper_bound ) )
= ( identity @ ( c @ least_upper_bound ) ) ),
inference(pattern_uni,[status(thm)],[6639:[bind(A,$thf( c )),bind(B,$thf( identity ))]]) ).
thf(9816,plain,
( ( c @ ( c @ least_upper_bound ) )
= c ),
inference(rewrite,[status(thm)],[6640,1990,1308]) ).
thf(119693,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( identity @ least_upper_bound ) @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[119620,25]) ).
thf(119694,plain,
( ( a @ ( identity @ ( identity @ least_upper_bound ) @ ( identity @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[119693:[bind(A,$thf( a )),bind(B,$thf( identity @ ( identity @ least_upper_bound ) @ ( identity @ least_upper_bound ) ))]]) ).
thf(173570,plain,
( ( a @ ( identity @ ( identity @ least_upper_bound ) @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[119694,29]) ).
thf(444,plain,
! [B: $i,A: $i] :
( ( ( A @ ( identity @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= ( B @ ( identity @ greatest_lower_bound ) @ ( a @ least_upper_bound ) ) )
| ( ( A @ ( a @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[290,432]) ).
thf(471,plain,
! [B: $i,A: $i] :
( ( ( A @ ( identity @ least_upper_bound ) )
!= ( B @ ( identity @ greatest_lower_bound ) ) )
| ( a != a )
| ( ( A @ ( a @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[444]) ).
thf(484,plain,
! [B: $i,A: $i] :
( ( ( A @ ( identity @ least_upper_bound ) )
!= ( B @ ( identity @ greatest_lower_bound ) ) )
| ( ( A @ ( a @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[471]) ).
thf(43166,plain,
! [B: $i,A: $i] :
( ( ( A @ ( identity @ least_upper_bound ) )
!= ( B @ ( b @ greatest_lower_bound ) @ ( a @ greatest_lower_bound ) ) )
| ( ( A @ ( a @ least_upper_bound ) )
= a ) ),
inference(rewrite,[status(thm)],[484,984]) ).
thf(53058,plain,
! [B: $i,A: $i] :
( ( ( a @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) @ ( identity @ least_upper_bound ) )
!= ( B @ ( A @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[53029,25]) ).
thf(53059,plain,
( ( identity @ ( a @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(pattern_uni,[status(thm)],[53058:[bind(A,$thf( identity )),bind(B,$thf( a @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) ))]]) ).
thf(61860,plain,
( ( identity @ ( a @ least_upper_bound ) @ ( a @ ( a @ least_upper_bound ) @ least_upper_bound ) )
= a ),
inference(rewrite,[status(thm)],[53059,29]) ).
thf(339,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ least_upper_bound ) @ least_upper_bound ) )
!= ( a @ ( identity @ least_upper_bound ) ) )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(paramod_ordered,[status(thm)],[29,275]) ).
thf(357,plain,
! [C: $i,B: $i,A: $i] :
( ( C != a )
| ( ( B @ ( A @ least_upper_bound ) )
!= identity )
| ( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[339]) ).
thf(364,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ least_upper_bound ) )
!= identity )
| ( ( a @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= a ) ),
inference(simp,[status(thm)],[357]) ).
thf(2605,plain,
( ( ( c @ ( a @ greatest_lower_bound ) )
!= ( b @ ( a @ greatest_lower_bound ) ) )
| ( ( c @ ( b @ multiply ) )
!= identity )
| ( identity != identity ) ),
inference(paramod_ordered,[status(thm)],[35,1532]) ).
thf(2606,plain,
( ( ( c @ ( a @ greatest_lower_bound ) )
!= ( b @ ( a @ greatest_lower_bound ) ) )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(simp,[status(thm)],[2605]) ).
thf(2636,plain,
( ( c != b )
| ( a != a )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(simp,[status(thm)],[2606]) ).
thf(2655,plain,
( ( c != b )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(simp,[status(thm)],[2636]) ).
thf(36751,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ greatest_lower_bound ) )
!= ( C @ ( b @ greatest_lower_bound ) ) )
| ( ( B @ ( A @ greatest_lower_bound ) )
!= c )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(paramod_ordered,[status(thm)],[53,26354]) ).
thf(36752,plain,
! [A: $i] :
( ( ( b @ ( A @ greatest_lower_bound ) )
!= c )
| ( ( c @ ( b @ multiply ) )
!= identity ) ),
inference(pattern_uni,[status(thm)],[36751:[bind(A,$thf( A )),bind(B,$thf( b )),bind(C,$thf( A ))]]) ).
thf(919,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ greatest_lower_bound ) @ greatest_lower_bound ) )
!= ( E @ ( D @ greatest_lower_bound ) ) )
| ( ( F @ ( C @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) @ greatest_lower_bound ) )
= ( F @ ( E @ greatest_lower_bound ) @ ( D @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[47,47]) ).
thf(920,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( D @ greatest_lower_bound ) @ ( C @ greatest_lower_bound ) @ greatest_lower_bound ) )
= ( B @ ( A @ greatest_lower_bound ) @ ( D @ ( C @ greatest_lower_bound ) @ greatest_lower_bound ) ) ),
inference(pattern_uni,[status(thm)],[919:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( G @ greatest_lower_bound ) )),bind(E,$thf( C ))]]) ).
thf(986,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( D @ greatest_lower_bound ) @ ( C @ greatest_lower_bound ) @ greatest_lower_bound ) )
= ( B @ ( A @ greatest_lower_bound ) @ ( D @ ( C @ greatest_lower_bound ) @ greatest_lower_bound ) ) ),
inference(simp,[status(thm)],[920]) ).
thf(169657,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( D @ greatest_lower_bound ) @ greatest_lower_bound ) @ ( C @ greatest_lower_bound ) )
= ( B @ ( A @ greatest_lower_bound ) @ ( D @ greatest_lower_bound ) @ ( C @ greatest_lower_bound ) ) ),
inference(rewrite,[status(thm)],[986,47]) ).
thf(226125,plain,
$false,
inference(e,[status(thm)],[39961,158533,117134,138007,158583,333,249,977,217,32522,98395,120,677,1200,4043,28853,143991,57665,27115,56,3429,107087,69313,10827,25727,153278,29532,42,24,4030,37,25,973,9027,60036,301,4665,141026,52,3221,114761,120885,96170,116436,145335,1191,1462,151245,18451,54828,46,770,325,57,48084,29,43629,70701,13013,121,4686,74947,84741,3771,981,179681,61,1119,76215,111819,428,161168,77651,22685,14060,3899,158581,60,21747,130767,90513,154623,714,3795,529,95053,1123,4204,153324,28,38,4521,424,275,21,108263,151197,55973,169628,974,2653,252,1602,150483,31080,53,55432,17065,989,7065,151225,151180,8704,8105,18653,59231,45124,1214,970,26969,66182,56001,393,985,984,50361,63709,6784,41,22213,72520,30082,150839,13714,9169,97277,530,21023,31931,425,15147,151205,45,12290,29659,65345,20578,32,34,423,44,135668,286,4926,59,44041,147711,85769,27,3796,54,173481,169432,91074,22323,672,1806,24951,17137,362,122185,1175,73977,63338,39,62679,41990,323,213,71612,769,33115,26354,983,176236,17223,78895,150816,35,675,426,100686,41517,50948,86331,1990,123,754,26260,14813,531,87389,88248,103206,23151,80856,14485,95,58226,177859,58335,14158,151184,48,525,50,331,18153,3801,22680,176323,18456,31,16678,1235,47373,173468,978,125892,75272,43,4671,119620,250,49465,1157,18061,976,524,149066,158585,64523,151206,104,67254,39124,40,167069,26,55,151171,118372,136826,418,23,4900,153026,37216,166851,1308,153294,67576,84128,214,290,58,164892,53766,82489,1193,4014,36,30,422,326,123383,18538,532,113012,30326,4007,17135,159862,15617,987,9816,173570,1532,43166,3817,47,61860,7367,53029,364,2655,972,36752,169657]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP178-2 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.14/0.39 % Computer : n011.cluster.edu
% 0.14/0.39 % Model : x86_64 x86_64
% 0.14/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.39 % Memory : 8046.5625MB
% 0.14/0.39 % OS : Linux 6.8.0-71-generic
% 0.14/0.39 % CPULimit : 300
% 0.14/0.39 % WCLimit : 300
% 0.14/0.39 % DateTime : Fri Sep 25 14:34:43 UTC 2026
% 0.14/0.39 % CPUTime :
% 0.14/0.39 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.86/0.96 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.24/1.16 % [INFO] Parsing done (199ms).
% 1.24/1.18 % [INFO] Running in sequential loop mode.
% 1.90/1.58 % [INFO] eprover registered as external prover.
% 1.90/1.59 % [INFO] Scanning for conjecture ...
% 2.10/1.67 % [INFO] Found a conjecture (or negated_conjecture) and 19 axioms. Running axiom selection ...
% 2.26/1.73 % [INFO] Axiom selection finished. Selected 19 axioms (removed 0 axioms).
% 2.26/1.76 % [INFO] Problem is propositional (TPTP CNF).
% 2.26/1.76 % [INFO] Type checking passed.
% 2.26/1.77 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 217.53/80.53 % External prover 'e' found a proof!
% 217.53/80.53 % [INFO] Killing All external provers ...
% 217.53/80.53 % Time passed: 79992ms (effective reasoning time: 79344ms)
% 217.53/80.53 % Axioms used in derivation (19): monotony_lub1, idempotence_of_lub, p09b_2, monotony_glb1, left_inverse, symmetry_of_glb, monotony_glb2, glb_absorbtion, p09b_3, associativity_of_glb, symmetry_of_lub, p09b_1, associativity, monotony_lub2, left_identity, associativity_of_lub, lub_absorbtion, p09b_4, idempotence_of_gld
% 217.53/80.53 % No. of inferences in proof: 935
% 217.53/80.53 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p : 79992 ms resp. 79344 ms w/o parsing
% 210.78/80.79 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 210.78/80.79 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------