%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : HWV052-1.002.002 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n017.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:32:31 AM UTC 2026
% Result : Unsatisfiable 191.95s 54.89s
% Output : Refutation 193.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 12
% Syntax : Number of formulae : 723 ( 59 unt; 0 typ; 0 def)
% Number of atoms : 1980 (1979 equ; 0 cnn)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 9182 ( 893 ~;1257 |; 0 &;7032 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 9 ( 7 usr; 3 con; 0-4 aty)
% Number of variables : 1184 ( 0 ^;1184 !; 0 ?;1184 :)
% Comments :
%------------------------------------------------------------------------------
thf(o_decl,type,
o: $i ).
thf(i_decl,type,
i: $i ).
thf(inv_decl,type,
inv: $i > $i ).
thf(unpack1_decl,type,
unpack1: $i > $i > $i > $i > $i ).
thf(pack1_decl,type,
pack1: $i > $i > $i ).
thf(pack2_decl,type,
pack2: $i > $i > $i ).
thf(unpack2_decl,type,
unpack2: $i > $i > $i > $i > $i ).
thf(1,axiom,
! [A: $i] :
( ( A = i )
| ( A = o ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bit_domain) ).
thf(13,plain,
! [A: $i] :
( ( A = i )
| ( A = o ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[1]) ).
thf(14,plain,
! [A: $i] :
( ( A = i )
| ( A = o ) ),
inference(cnf,[status(esa)],[13]) ).
thf(15,plain,
! [A: $i] :
( ( A = i )
| ( A = o ) ),
inference(lifteq,[status(thm)],[14]) ).
thf(2,axiom,
! [A: $i] :
( ( A @ inv )
!= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bit_inverse) ).
thf(16,plain,
! [A: $i] :
( ( A @ inv )
!= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(17,plain,
! [A: $i] :
( ( A @ inv )
!= A ),
inference(polarity_switch,[status(thm)],[16]) ).
thf(18,plain,
! [A: $i] :
( ( A @ inv )
!= A ),
inference(lifteq,[status(thm)],[17]) ).
thf(76,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ inv ) )
| ( i != B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,18]) ).
thf(77,plain,
! [A: $i] :
( ( i != A )
| ( ( A @ inv )
= o ) ),
inference(pattern_uni,[status(thm)],[76:[bind(A,$thf( C @ inv )),bind(B,$thf( C ))]]) ).
thf(97,plain,
( ( i @ inv )
= o ),
inference(simp,[status(thm)],[77]) ).
thf(125,plain,
! [A: $i] :
( ( i != i )
| ( ( A @ inv )
= o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,97]) ).
thf(126,plain,
! [A: $i] :
( ( ( A @ inv )
= o )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[125:[]]) ).
thf(12,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ inv @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack2 ) ) ) )
= B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unpack2_08) ).
thf(37,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ inv @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack2 ) ) ) )
= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(38,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ inv @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack2 ) ) ) )
= B ),
inference(lifteq,[status(thm)],[37]) ).
thf(599,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ inv )
!= ( C @ ( B @ pack2 ) @ inv ) )
| ( ( o @ ( C @ ( B @ pack1 ) @ ( C @ ( B @ unpack2 ) ) ) )
= C )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[126,38]) ).
thf(600,plain,
! [B: $i,A: $i] :
( ( ( o @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack2 ) ) ) )
= B )
| ( ( B @ ( A @ pack2 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[599:[bind(A,$thf( E @ ( D @ pack2 ) )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(645,plain,
! [B: $i,A: $i] :
( ( ( o @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack2 ) ) ) )
= B )
| ( ( B @ ( A @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[600]) ).
thf(8,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack2 ) ) ) )
= B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unpack2) ).
thf(29,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack2 ) ) ) )
= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(30,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack2 ) ) ) )
= B ),
inference(lifteq,[status(thm)],[29]) ).
thf(84,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ pack2 ) @ ( C @ ( B @ pack1 ) @ ( C @ ( B @ unpack2 ) ) ) ) )
| ( i = C )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,30]) ).
thf(85,plain,
! [B: $i,A: $i] :
( ( i = B )
| ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack2 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[84:[bind(A,$thf( K @ ( J @ pack2 ) @ ( K @ ( J @ pack1 ) @ ( K @ ( J @ unpack2 ) ) ) )),bind(B,$thf( J )),bind(C,$thf( K ))]]) ).
thf(101,plain,
! [B: $i,A: $i] :
( ( i = B )
| ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack2 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[85]) ).
thf(4511,plain,
! [A: $i] :
( ( i = A )
| ( A = o ) ),
inference(rewrite,[status(thm)],[101,30]) ).
thf(4621,plain,
! [B: $i,A: $i] :
( ( i != i )
| ( A = B )
| ( B = o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[4511,15]) ).
thf(4622,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( B = o )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[4621:[]]) ).
thf(5270,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( B = o )
| ( A = o ) ),
inference(simp,[status(thm)],[4622]) ).
thf(7911,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ inv ) )
| ( o != C )
| ( A = B )
| ( B = o ) ),
inference(paramod_ordered,[status(thm)],[5270,18]) ).
thf(7912,plain,
! [B: $i,A: $i] :
( ( o != B )
| ( ( B @ inv )
= A )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[7911:[bind(A,$thf( D @ inv )),bind(B,$thf( B )),bind(C,$thf( D ))]]) ).
thf(9477,plain,
! [A: $i] :
( ( ( o @ inv )
= A )
| ( A = o ) ),
inference(simp,[status(thm)],[7912]) ).
thf(10281,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ inv ) )
| ( ( o @ inv )
!= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[9477,18]) ).
thf(10282,plain,
! [A: $i] :
( ( ( o @ inv )
!= A )
| ( ( A @ inv )
= o ) ),
inference(pattern_uni,[status(thm)],[10281:[bind(A,$thf( C @ inv )),bind(B,$thf( C ))]]) ).
thf(10467,plain,
( ( o @ inv @ inv )
= o ),
inference(simp,[status(thm)],[10282]) ).
thf(10710,plain,
! [A: $i] :
( ( ( o @ inv @ inv )
!= ( A @ inv ) )
| ( o != A ) ),
inference(paramod_ordered,[status(thm)],[10467,18]) ).
thf(10711,plain,
( ( o @ inv )
!= o ),
inference(pattern_uni,[status(thm)],[10710:[bind(A,$thf( o @ inv ))]]) ).
thf(10776,plain,
! [B: $i,A: $i] :
( ( o != o )
| ( ( A @ inv )
!= o )
| ( A = B )
| ( B = o ) ),
inference(paramod_ordered,[status(thm)],[5270,10711]) ).
thf(10777,plain,
! [B: $i,A: $i] :
( ( ( A @ inv )
!= o )
| ( A = B )
| ( B = o ) ),
inference(pattern_uni,[status(thm)],[10776:[]]) ).
thf(26966,plain,
! [B: $i,A: $i] :
( ( B
!= ( o @ inv ) )
| ( o != o )
| ( ( A @ inv )
!= o )
| ( A = B ) ),
inference(paramod_ordered,[status(thm)],[10777,10711]) ).
thf(26967,plain,
! [B: $i,A: $i] :
( ( B
!= ( o @ inv ) )
| ( ( A @ inv )
!= o )
| ( A = B ) ),
inference(simp,[status(thm)],[26966]) ).
thf(26968,plain,
! [A: $i] :
( ( ( A @ inv )
!= o )
| ( A
= ( o @ inv ) ) ),
inference(pattern_uni,[status(thm)],[26967:[bind(A,$thf( A )),bind(B,$thf( o @ inv ))]]) ).
thf(31672,plain,
! [A: $i] :
( ( ( i @ inv )
!= ( A @ inv ) )
| ( o != o )
| ( A
= ( o @ inv ) ) ),
inference(paramod_ordered,[status(thm)],[97,26968]) ).
thf(31673,plain,
! [A: $i] :
( ( ( i @ inv )
!= ( A @ inv ) )
| ( A
= ( o @ inv ) ) ),
inference(simp,[status(thm)],[31672]) ).
thf(31674,plain,
( ( o @ inv )
= i ),
inference(pattern_uni,[status(thm)],[31673:[bind(A,$thf( i ))]]) ).
thf(32346,plain,
! [A: $i] :
( ( ( A @ inv )
!= o )
| ( A = i ) ),
inference(rewrite,[status(thm)],[26968,31674]) ).
thf(33375,plain,
! [C: $i,B: $i,A: $i] :
( ( B
!= ( C @ inv ) )
| ( o != o )
| ( C = i )
| ( A = B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[5270,32346]) ).
thf(33376,plain,
! [C: $i,B: $i,A: $i] :
( ( B
!= ( C @ inv ) )
| ( C = i )
| ( A = B )
| ( A = o ) ),
inference(simp,[status(thm)],[33375]) ).
thf(33377,plain,
! [B: $i,A: $i] :
( ( B = i )
| ( A
= ( B @ inv ) )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[33376:[bind(A,$thf( A )),bind(B,$thf( D @ inv )),bind(C,$thf( D ))]]) ).
thf(33394,plain,
! [B: $i,A: $i] :
( ( B = i )
| ( A
= ( B @ inv ) )
| ( A = o ) ),
inference(simp,[status(thm)],[33377]) ).
thf(10783,plain,
! [B: $i,A: $i] :
( ( o != o )
| ( ( B @ inv )
!= o )
| ( A = B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[5270,10711]) ).
thf(10784,plain,
! [B: $i,A: $i] :
( ( ( B @ inv )
!= o )
| ( A = B )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[10783:[]]) ).
thf(9,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ inv @ unpack2 ) ) ) )
= B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unpack2_05) ).
thf(31,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ inv @ unpack2 ) ) ) )
= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(32,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ inv @ unpack2 ) ) ) )
= B ),
inference(lifteq,[status(thm)],[31]) ).
thf(381,plain,
! [B: $i,A: $i] :
( ( ( i @ inv )
!= ( A @ inv ) )
| ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( o @ unpack2 ) ) ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[97,32]) ).
thf(382,plain,
! [A: $i] :
( ( A @ ( i @ pack2 ) @ ( A @ ( i @ pack1 ) @ ( A @ ( o @ unpack2 ) ) ) )
= A ),
inference(pattern_uni,[status(thm)],[381:[bind(A,$thf( i ))]]) ).
thf(404,plain,
! [A: $i] :
( ( A @ ( i @ pack2 ) @ ( A @ ( i @ pack1 ) @ ( A @ ( o @ unpack2 ) ) ) )
= A ),
inference(simp,[status(thm)],[382]) ).
thf(418,plain,
! [B: $i,A: $i] :
( ( i != i )
| ( ( B @ ( i @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( o @ unpack2 ) ) ) )
= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,404]) ).
thf(419,plain,
! [B: $i,A: $i] :
( ( ( B @ ( i @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( o @ unpack2 ) ) ) )
= B )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[418:[]]) ).
thf(46390,plain,
! [B: $i,A: $i] :
( ( B != o )
| ( ( B @ ( i @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( o @ unpack2 ) ) ) )
!= A )
| ( A = o ) ),
inference(eqfactor_ordered,[status(thm)],[419]) ).
thf(46424,plain,
! [A: $i] :
( ( ( o @ ( i @ pack2 ) @ ( o @ ( A @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
!= A )
| ( A = o ) ),
inference(simp,[status(thm)],[46390]) ).
thf(46730,plain,
! [B: $i,A: $i] :
( ( A
!= ( o @ ( B @ pack1 ) ) )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
!= B )
| ( B = o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,46424]) ).
thf(46731,plain,
! [A: $i] :
( ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
!= A )
| ( A = o )
| ( ( o @ ( A @ pack1 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[46730:[bind(A,$thf( o @ ( C @ pack1 ) )),bind(B,$thf( C ))]]) ).
thf(46818,plain,
( ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( o @ ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) @ pack1 ) )
= o ) ),
inference(simp,[status(thm)],[46731]) ).
thf(46912,plain,
! [A: $i] :
( ( ( o @ ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) @ pack1 ) )
!= ( o @ ( A @ pack1 ) ) )
| ( ( o @ ( i @ pack2 ) @ ( o @ ( o @ ( o @ unpack2 ) ) ) )
!= A )
| ( A = o )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(paramod_ordered,[status(thm)],[46818,46424]) ).
thf(46913,plain,
( ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
!= ( o @ ( i @ pack2 ) @ ( o @ ( o @ ( o @ unpack2 ) ) ) ) )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[46912:[bind(A,$thf( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) ))]]) ).
thf(47493,plain,
( ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
!= ( o @ ( i @ pack2 ) @ ( o @ ( o @ ( o @ unpack2 ) ) ) ) )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[46913]) ).
thf(78607,plain,
! [B: $i,A: $i] :
( ( A
!= ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) ) )
| ( B
!= ( o @ ( i @ pack2 ) @ ( o @ ( o @ ( o @ unpack2 ) ) ) ) )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( B @ inv )
!= o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[10784,47493]) ).
thf(78608,plain,
! [A: $i] :
( ( A
!= ( o @ ( i @ pack2 ) @ ( o @ ( o @ ( o @ unpack2 ) ) ) ) )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( A @ inv )
!= o )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[78607:[bind(A,$thf( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )),bind(B,$thf( B ))]]) ).
thf(78945,plain,
( ( ( o @ ( i @ pack2 ) @ ( o @ ( o @ ( o @ unpack2 ) ) ) @ inv )
!= o )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[78608]) ).
thf(4,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ inv @ unpack1 ) ) ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unpack1_01) ).
thf(21,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ inv @ unpack1 ) ) ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(22,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ inv @ unpack1 ) ) ) )
= A ),
inference(lifteq,[status(thm)],[21]) ).
thf(113,plain,
! [B: $i,A: $i] :
( ( ( i @ inv )
!= ( A @ inv ) )
| ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( o @ unpack1 ) ) ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[97,22]) ).
thf(114,plain,
! [A: $i] :
( ( A @ ( i @ pack2 ) @ ( A @ ( i @ pack1 ) @ ( A @ ( o @ unpack1 ) ) ) )
= i ),
inference(pattern_uni,[status(thm)],[113:[bind(A,$thf( i ))]]) ).
thf(128,plain,
! [A: $i] :
( ( A @ ( i @ pack2 ) @ ( A @ ( i @ pack1 ) @ ( A @ ( o @ unpack1 ) ) ) )
= i ),
inference(simp,[status(thm)],[114]) ).
thf(170,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ ( i @ pack2 ) ) )
| ( ( i @ ( B @ ( i @ pack1 ) @ ( B @ ( o @ unpack1 ) ) ) )
= i )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,128]) ).
thf(171,plain,
! [A: $i] :
( ( ( i @ ( A @ ( i @ pack1 ) @ ( A @ ( o @ unpack1 ) ) ) )
= i )
| ( ( A @ ( i @ pack2 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[170:[bind(A,$thf( D @ ( i @ pack2 ) )),bind(B,$thf( D ))]]) ).
thf(191,plain,
! [A: $i] :
( ( ( i @ ( A @ ( i @ pack1 ) @ ( A @ ( o @ unpack1 ) ) ) )
= i )
| ( ( A @ ( i @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[171]) ).
thf(6,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ inv @ ( B @ ( A @ unpack1 ) ) ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unpack1_03) ).
thf(25,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ inv @ ( B @ ( A @ unpack1 ) ) ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(26,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ inv @ ( B @ ( A @ unpack1 ) ) ) )
= A ),
inference(lifteq,[status(thm)],[25]) ).
thf(734,plain,
! [C: $i,B: $i,A: $i] :
( ( ( i @ ( A @ ( i @ pack1 ) @ ( A @ ( o @ unpack1 ) ) ) )
!= ( C @ ( B @ pack2 ) @ ( C @ ( B @ pack1 ) @ inv @ ( C @ ( B @ unpack1 ) ) ) ) )
| ( i = B )
| ( ( A @ ( i @ pack2 ) )
= o ) ),
inference(paramod_ordered,[status(thm)],[191,26]) ).
thf(744,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ pack2 ) )
!= i )
| ( ( A @ ( i @ pack1 ) )
!= ( C @ ( B @ pack1 ) @ inv ) )
| ( A != C )
| ( o != B )
| ( i = B )
| ( ( A @ ( i @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[734]) ).
thf(756,plain,
! [A: $i] :
( ( ( A @ ( o @ pack2 ) )
!= i )
| ( ( A @ ( i @ pack1 ) )
!= ( A @ ( o @ pack1 ) @ inv ) )
| ( i = o )
| ( ( A @ ( i @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[744]) ).
thf(115,plain,
! [A: $i] :
( ( ( i @ inv )
!= ( A @ inv ) )
| ( o != A ) ),
inference(paramod_ordered,[status(thm)],[97,18]) ).
thf(116,plain,
i != o,
inference(pattern_uni,[status(thm)],[115:[bind(A,$thf( i ))]]) ).
thf(114041,plain,
! [A: $i] :
( ( ( A @ ( o @ pack2 ) )
!= i )
| ( ( A @ ( i @ pack1 ) )
!= ( A @ ( o @ pack1 ) @ inv ) )
| ( ( A @ ( i @ pack2 ) )
= o ) ),
inference(simplifyReflect,[status(thm)],[756,116]) ).
thf(5,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ inv @ ( A @ unpack1 ) ) ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unpack1_02) ).
thf(23,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ inv @ ( A @ unpack1 ) ) ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(24,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ inv @ ( A @ unpack1 ) ) ) )
= A ),
inference(lifteq,[status(thm)],[23]) ).
thf(346,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ inv )
!= ( C @ inv ) )
| ( ( C @ ( B @ pack2 ) @ ( C @ ( B @ pack1 ) @ ( o @ ( B @ unpack1 ) ) ) )
= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[126,24]) ).
thf(347,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ pack2 ) @ ( A @ ( B @ pack1 ) @ ( o @ ( B @ unpack1 ) ) ) )
= B )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[346:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A ))]]) ).
thf(10,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ inv @ ( A @ unpack2 ) ) ) )
= B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unpack2_06) ).
thf(33,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ inv @ ( A @ unpack2 ) ) ) )
= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(34,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ inv @ ( A @ unpack2 ) ) ) )
= B ),
inference(lifteq,[status(thm)],[33]) ).
thf(439,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ inv @ ( A @ unpack2 ) ) ) )
!= ( D @ ( C @ pack2 ) @ ( D @ ( C @ pack1 ) @ ( D @ ( C @ unpack2 ) ) ) ) )
| ( B = D ) ),
inference(paramod_ordered,[status(thm)],[34,30]) ).
thf(460,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) )
!= ( D @ ( C @ pack2 ) ) )
| ( ( B @ ( A @ pack1 ) )
!= ( D @ ( C @ pack1 ) ) )
| ( ( B @ inv )
!= D )
| ( A != C )
| ( B = D ) ),
inference(simp,[status(thm)],[439]) ).
thf(468,plain,
! [B: $i,A: $i] :
( ( ( A @ inv @ ( B @ pack2 ) )
!= ( A @ ( B @ pack2 ) ) )
| ( ( A @ inv @ ( B @ pack1 ) )
!= ( A @ ( B @ pack1 ) ) )
| ( ( A @ inv )
= A ) ),
inference(simp,[status(thm)],[460]) ).
thf(60848,plain,
! [B: $i,A: $i] :
( ( ( A @ inv @ ( B @ pack2 ) )
!= ( A @ ( B @ pack2 ) ) )
| ( ( A @ inv @ ( B @ pack1 ) )
!= ( A @ ( B @ pack1 ) ) ) ),
inference(simplifyReflect,[status(thm)],[468,18]) ).
thf(60850,plain,
! [B: $i,A: $i] :
( ( ( A @ inv )
!= A )
| ( B != B )
| ( ( A @ inv @ ( B @ pack1 ) )
!= ( A @ ( B @ pack1 ) ) ) ),
inference(simp,[status(thm)],[60848]) ).
thf(61022,plain,
! [B: $i,A: $i] :
( ( ( A @ inv )
!= A )
| ( ( A @ inv @ ( B @ pack1 ) )
!= ( A @ ( B @ pack1 ) ) ) ),
inference(simp,[status(thm)],[60850]) ).
thf(138,plain,
! [B: $i,A: $i] :
( ( ( i @ inv )
!= ( B @ inv ) )
| ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( o @ ( A @ unpack1 ) ) ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[97,24]) ).
thf(139,plain,
! [A: $i] :
( ( i @ ( A @ pack2 ) @ ( i @ ( A @ pack1 ) @ ( o @ ( A @ unpack1 ) ) ) )
= A ),
inference(pattern_uni,[status(thm)],[138:[bind(A,$thf( A )),bind(B,$thf( i ))]]) ).
thf(219,plain,
! [B: $i,A: $i] :
( ( i != i )
| ( ( i @ ( B @ pack2 ) @ ( A @ ( B @ pack1 ) @ ( o @ ( B @ unpack1 ) ) ) )
= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,139]) ).
thf(220,plain,
! [B: $i,A: $i] :
( ( ( i @ ( B @ pack2 ) @ ( A @ ( B @ pack1 ) @ ( o @ ( B @ unpack1 ) ) ) )
= B )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[219:[]]) ).
thf(2548,plain,
! [B: $i,A: $i] :
( ( B != o )
| ( ( i @ ( B @ pack2 ) @ ( A @ ( B @ pack1 ) @ ( o @ ( B @ unpack1 ) ) ) )
!= A )
| ( A = o ) ),
inference(eqfactor_ordered,[status(thm)],[220]) ).
thf(2559,plain,
! [A: $i] :
( ( ( i @ ( o @ pack2 ) @ ( A @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
!= A )
| ( A = o ) ),
inference(simp,[status(thm)],[2548]) ).
thf(614,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ inv @ ( A @ unpack2 ) ) ) )
!= ( D @ ( C @ pack2 ) @ inv @ ( D @ ( C @ pack1 ) @ ( D @ ( C @ unpack2 ) ) ) ) )
| ( B = D ) ),
inference(paramod_ordered,[status(thm)],[34,38]) ).
thf(625,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) )
!= ( D @ ( C @ pack2 ) @ inv ) )
| ( ( B @ ( A @ pack1 ) )
!= ( D @ ( C @ pack1 ) ) )
| ( ( B @ inv )
!= D )
| ( A != C )
| ( B = D ) ),
inference(simp,[status(thm)],[614]) ).
thf(638,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ pack2 ) )
!= ( A @ inv @ ( B @ pack2 ) @ inv ) )
| ( ( A @ inv @ ( B @ pack1 ) )
!= ( A @ ( B @ pack1 ) ) )
| ( ( A @ inv )
= A ) ),
inference(simp,[status(thm)],[625]) ).
thf(89650,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ pack2 ) )
!= ( A @ inv @ ( B @ pack2 ) @ inv ) )
| ( ( A @ inv @ ( B @ pack1 ) )
!= ( A @ ( B @ pack1 ) ) ) ),
inference(simplifyReflect,[status(thm)],[638,18]) ).
thf(89652,plain,
! [B: $i,A: $i] :
( ( ( o @ inv )
!= ( A @ inv ) )
| ( ( A @ ( B @ pack2 ) )
!= ( A @ inv @ ( B @ pack2 ) @ inv ) )
| ( ( i @ ( B @ pack1 ) )
!= ( A @ ( B @ pack1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[31674,89650]) ).
thf(89653,plain,
! [A: $i] :
( ( ( o @ ( A @ pack2 ) )
!= ( o @ inv @ ( A @ pack2 ) @ inv ) )
| ( ( i @ ( A @ pack1 ) )
!= ( o @ ( A @ pack1 ) ) ) ),
inference(pattern_uni,[status(thm)],[89652:[bind(A,$thf( o ))]]) ).
thf(89936,plain,
! [A: $i] :
( ( ( o @ ( A @ pack2 ) )
!= ( o @ inv @ ( A @ pack2 ) @ inv ) )
| ( ( i @ ( A @ pack1 ) )
!= ( o @ ( A @ pack1 ) ) ) ),
inference(simp,[status(thm)],[89653]) ).
thf(109444,plain,
! [A: $i] :
( ( ( o @ ( A @ pack2 ) )
!= ( i @ ( A @ pack2 ) @ inv ) )
| ( ( i @ ( A @ pack1 ) )
!= ( o @ ( A @ pack1 ) ) ) ),
inference(rewrite,[status(thm)],[89936,31674]) ).
thf(259,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ pack2 ) ) )
| ( ( i @ ( C @ ( B @ pack1 ) @ inv @ ( C @ ( B @ unpack1 ) ) ) )
= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,26]) ).
thf(260,plain,
! [B: $i,A: $i] :
( ( ( i @ ( B @ ( A @ pack1 ) @ inv @ ( B @ ( A @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack2 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[259:[bind(A,$thf( E @ ( D @ pack2 ) )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(276,plain,
! [B: $i,A: $i] :
( ( ( i @ ( B @ ( A @ pack1 ) @ inv @ ( B @ ( A @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[260]) ).
thf(162,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( i @ pack2 ) @ ( A @ ( i @ pack1 ) @ ( A @ ( o @ unpack1 ) ) ) )
!= ( C @ ( B @ pack2 ) @ ( C @ ( B @ pack1 ) @ ( C @ inv @ ( B @ unpack1 ) ) ) ) )
| ( i = B ) ),
inference(paramod_ordered,[status(thm)],[128,24]) ).
thf(187,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( i @ pack2 ) )
!= ( C @ ( B @ pack2 ) ) )
| ( ( A @ ( i @ pack1 ) )
!= ( C @ ( B @ pack1 ) ) )
| ( A
!= ( C @ inv ) )
| ( o != B )
| ( i = B ) ),
inference(simp,[status(thm)],[162]) ).
thf(197,plain,
! [A: $i] :
( ( ( A @ inv @ ( i @ pack2 ) )
!= ( A @ ( o @ pack2 ) ) )
| ( ( A @ inv @ ( i @ pack1 ) )
!= ( A @ ( o @ pack1 ) ) )
| ( i = o ) ),
inference(simp,[status(thm)],[187]) ).
thf(16184,plain,
! [A: $i] :
( ( ( A @ inv @ ( i @ pack2 ) )
!= ( A @ ( o @ pack2 ) ) )
| ( ( A @ inv @ ( i @ pack1 ) )
!= ( A @ ( o @ pack1 ) ) ) ),
inference(simplifyReflect,[status(thm)],[197,116]) ).
thf(47085,plain,
! [B: $i,A: $i] :
( ( ( o @ ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) @ pack1 ) )
!= ( B @ ( A @ pack1 ) ) )
| ( ( B @ ( i @ pack2 ) @ ( o @ ( B @ ( o @ unpack2 ) ) ) )
= B )
| ( A = o )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(paramod_ordered,[status(thm)],[46818,419]) ).
thf(47086,plain,
( ( ( o @ ( i @ pack2 ) @ ( o @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[47085:[bind(A,$thf( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )),bind(B,$thf( o ))]]) ).
thf(47514,plain,
( ( ( o @ ( i @ pack2 ) @ ( o @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[47086]) ).
thf(48788,plain,
( ( o != o )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
!= ( o @ ( i @ pack2 ) @ ( o @ ( o @ ( o @ unpack2 ) ) ) ) )
| ( ( o @ ( i @ pack2 ) @ ( o @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(eqfactor_ordered,[status(thm)],[47514]) ).
thf(48793,plain,
( ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
!= ( o @ ( i @ pack2 ) @ ( o @ ( o @ ( o @ unpack2 ) ) ) ) )
| ( ( o @ ( i @ pack2 ) @ ( o @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[48788]) ).
thf(32385,plain,
! [B: $i,A: $i] :
( ( o != o )
| ( ( A @ inv )
= i )
| ( A = B )
| ( B = o ) ),
inference(paramod_ordered,[status(thm)],[5270,31674]) ).
thf(32386,plain,
! [B: $i,A: $i] :
( ( ( A @ inv )
= i )
| ( A = B )
| ( B = o ) ),
inference(pattern_uni,[status(thm)],[32385:[]]) ).
thf(94340,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ inv ) )
| ( B != C )
| ( ( A @ inv )
= i )
| ( B = o ) ),
inference(paramod_ordered,[status(thm)],[32386,18]) ).
thf(94341,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( ( B @ inv @ inv )
= i )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[94340:[bind(A,$thf( D @ inv )),bind(B,$thf( B )),bind(C,$thf( D ))]]) ).
thf(96584,plain,
! [A: $i] :
( ( ( A @ inv @ inv )
= i )
| ( A = o ) ),
inference(simp,[status(thm)],[94341]) ).
thf(437,plain,
! [B: $i,A: $i] :
( ( ( i @ inv )
!= ( B @ inv ) )
| ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( o @ ( A @ unpack2 ) ) ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[97,34]) ).
thf(438,plain,
! [A: $i] :
( ( i @ ( A @ pack2 ) @ ( i @ ( A @ pack1 ) @ ( o @ ( A @ unpack2 ) ) ) )
= i ),
inference(pattern_uni,[status(thm)],[437:[bind(A,$thf( A )),bind(B,$thf( i ))]]) ).
thf(473,plain,
! [B: $i,A: $i] :
( ( A
!= ( i @ ( B @ pack2 ) ) )
| ( ( i @ ( i @ ( B @ pack1 ) @ ( o @ ( B @ unpack2 ) ) ) )
= i )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,438]) ).
thf(474,plain,
! [A: $i] :
( ( ( i @ ( i @ ( A @ pack1 ) @ ( o @ ( A @ unpack2 ) ) ) )
= i )
| ( ( i @ ( A @ pack2 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[473:[bind(A,$thf( i @ ( C @ pack2 ) )),bind(B,$thf( C ))]]) ).
thf(513,plain,
! [A: $i] :
( ( ( i @ ( i @ ( A @ pack1 ) @ ( o @ ( A @ unpack2 ) ) ) )
= i )
| ( ( i @ ( A @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[474]) ).
thf(860,plain,
! [B: $i,A: $i] :
( ( i != i )
| ( ( A @ ( i @ ( B @ pack1 ) @ ( o @ ( B @ unpack2 ) ) ) )
= i )
| ( ( i @ ( B @ pack2 ) )
= o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,513]) ).
thf(861,plain,
! [B: $i,A: $i] :
( ( ( A @ ( i @ ( B @ pack1 ) @ ( o @ ( B @ unpack2 ) ) ) )
= i )
| ( ( i @ ( B @ pack2 ) )
= o )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[860:[]]) ).
thf(249,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ inv @ ( B @ ( A @ unpack1 ) ) ) )
!= ( C @ ( i @ pack2 ) @ ( C @ ( i @ pack1 ) @ ( C @ ( o @ unpack1 ) ) ) ) )
| ( A = i ) ),
inference(paramod_ordered,[status(thm)],[26,128]) ).
thf(263,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) )
!= ( C @ ( i @ pack2 ) ) )
| ( ( B @ ( A @ pack1 ) @ inv )
!= ( C @ ( i @ pack1 ) ) )
| ( B != C )
| ( A != o )
| ( A = i ) ),
inference(simp,[status(thm)],[249]) ).
thf(277,plain,
! [A: $i] :
( ( ( A @ ( i @ pack2 ) )
!= ( A @ ( o @ pack2 ) ) )
| ( ( A @ ( i @ pack1 ) )
!= ( A @ ( o @ pack1 ) @ inv ) )
| ( i = o ) ),
inference(simp,[status(thm)],[263]) ).
thf(26333,plain,
! [A: $i] :
( ( ( A @ ( i @ pack2 ) )
!= ( A @ ( o @ pack2 ) ) )
| ( ( A @ ( i @ pack1 ) )
!= ( A @ ( o @ pack1 ) @ inv ) ) ),
inference(simplifyReflect,[status(thm)],[277,116]) ).
thf(11,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ inv @ ( B @ ( A @ unpack2 ) ) ) )
= B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unpack2_07) ).
thf(35,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ inv @ ( B @ ( A @ unpack2 ) ) ) )
= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(36,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ inv @ ( B @ ( A @ unpack2 ) ) ) )
= B ),
inference(lifteq,[status(thm)],[35]) ).
thf(518,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ inv )
!= ( C @ ( B @ pack1 ) @ inv ) )
| ( ( C @ ( B @ pack2 ) @ ( o @ ( C @ ( B @ unpack2 ) ) ) )
= C )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[126,36]) ).
thf(519,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( o @ ( B @ ( A @ unpack2 ) ) ) )
= B )
| ( ( B @ ( A @ pack1 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[518:[bind(A,$thf( E @ ( D @ pack1 ) )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(550,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( o @ ( B @ ( A @ unpack2 ) ) ) )
= B )
| ( ( B @ ( A @ pack1 ) )
= o ) ),
inference(simp,[status(thm)],[519]) ).
thf(168,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ ( i @ pack1 ) ) )
| ( ( B @ ( i @ pack2 ) @ ( i @ ( B @ ( o @ unpack1 ) ) ) )
= i )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,128]) ).
thf(169,plain,
! [A: $i] :
( ( ( A @ ( i @ pack2 ) @ ( i @ ( A @ ( o @ unpack1 ) ) ) )
= i )
| ( ( A @ ( i @ pack1 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[168:[bind(A,$thf( D @ ( i @ pack1 ) )),bind(B,$thf( D ))]]) ).
thf(190,plain,
! [A: $i] :
( ( ( A @ ( i @ pack2 ) @ ( i @ ( A @ ( o @ unpack1 ) ) ) )
= i )
| ( ( A @ ( i @ pack1 ) )
= o ) ),
inference(simp,[status(thm)],[169]) ).
thf(669,plain,
! [B: $i,A: $i] :
( ( i != i )
| ( ( B @ ( A @ pack2 ) @ ( i @ ( B @ ( o @ unpack1 ) ) ) )
= i )
| ( ( B @ ( i @ pack1 ) )
= o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,190]) ).
thf(670,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( i @ ( B @ ( o @ unpack1 ) ) ) )
= i )
| ( ( B @ ( i @ pack1 ) )
= o )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[669:[]]) ).
thf(47223,plain,
! [A: $i] :
( ( A
!= ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) ) )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( o @ ( i @ pack1 ) )
= o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,46818]) ).
thf(47224,plain,
( ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( o @ ( i @ pack1 ) )
= o )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[47223:[bind(A,$thf( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) ))]]) ).
thf(47382,plain,
( ( ( o @ ( i @ pack1 ) )
= o )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[47224]) ).
thf(47530,plain,
! [A: $i] :
( ( A
!= ( o @ ( i @ pack2 ) ) )
| ( ( o @ ( i @ pack1 ) )
= o )
| ( ( i @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[4511,47382]) ).
thf(47531,plain,
( ( ( o @ ( i @ pack1 ) )
= o )
| ( ( i @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( o @ ( i @ pack2 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[47530:[bind(A,$thf( o @ ( i @ pack2 ) ))]]) ).
thf(78573,plain,
! [A: $i] :
( ( A
!= ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) ) )
| ( ( o @ ( i @ pack2 ) @ ( o @ ( o @ ( o @ unpack2 ) ) ) )
!= i )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[4511,47493]) ).
thf(78574,plain,
( ( ( o @ ( i @ pack2 ) @ ( o @ ( o @ ( o @ unpack2 ) ) ) )
!= i )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[78573:[bind(A,$thf( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) ))]]) ).
thf(79025,plain,
( ( ( o @ ( i @ pack2 ) @ ( o @ ( o @ ( o @ unpack2 ) ) ) )
!= i )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[78574]) ).
thf(32391,plain,
! [B: $i,A: $i] :
( ( o != o )
| ( ( B @ inv )
= i )
| ( A = B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[5270,31674]) ).
thf(32392,plain,
! [B: $i,A: $i] :
( ( ( B @ inv )
= i )
| ( A = B )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[32391:[]]) ).
thf(128422,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ inv ) )
| ( ( B @ inv )
!= C )
| ( B = i )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[33394,18]) ).
thf(128423,plain,
! [B: $i,A: $i] :
( ( ( A @ inv )
!= B )
| ( A = i )
| ( ( B @ inv )
= o ) ),
inference(pattern_uni,[status(thm)],[128422:[bind(A,$thf( D @ inv )),bind(B,$thf( B )),bind(C,$thf( D ))]]) ).
thf(129481,plain,
! [A: $i] :
( ( A = i )
| ( ( A @ inv @ inv )
= o ) ),
inference(simp,[status(thm)],[128423]) ).
thf(2821,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ ( o @ pack1 ) ) )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
!= B )
| ( B = o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,2559]) ).
thf(2822,plain,
! [A: $i] :
( ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
!= A )
| ( A = o )
| ( ( A @ ( o @ pack1 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[2821:[bind(A,$thf( D @ ( o @ pack1 ) )),bind(B,$thf( D ))]]) ).
thf(2895,plain,
( ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) @ ( o @ pack1 ) )
= o ) ),
inference(simp,[status(thm)],[2822]) ).
thf(2928,plain,
! [A: $i] :
( ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) @ ( o @ pack1 ) )
!= ( A @ ( o @ pack1 ) ) )
| ( ( i @ ( o @ pack2 ) @ ( o @ ( o @ ( o @ unpack1 ) ) ) )
!= A )
| ( A = o )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(paramod_ordered,[status(thm)],[2895,2559]) ).
thf(2929,plain,
( ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
!= ( i @ ( o @ pack2 ) @ ( o @ ( o @ ( o @ unpack1 ) ) ) ) )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[2928:[bind(A,$thf( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) ))]]) ).
thf(3133,plain,
( ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
!= ( i @ ( o @ pack2 ) @ ( o @ ( o @ ( o @ unpack1 ) ) ) ) )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[2929]) ).
thf(3760,plain,
! [A: $i] :
( ( A
!= ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) ) )
| ( ( i @ ( o @ pack2 ) @ ( o @ ( o @ ( o @ unpack1 ) ) ) )
!= i )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,3133]) ).
thf(3761,plain,
( ( ( i @ ( o @ pack2 ) @ ( o @ ( o @ ( o @ unpack1 ) ) ) )
!= i )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[3760:[bind(A,$thf( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) ))]]) ).
thf(3845,plain,
( ( ( i @ ( o @ pack2 ) @ ( o @ ( o @ ( o @ unpack1 ) ) ) )
!= i )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[3761]) ).
thf(221,plain,
! [B: $i,A: $i] :
( ( i != i )
| ( ( A @ ( B @ pack2 ) @ ( i @ ( B @ pack1 ) @ ( o @ ( B @ unpack1 ) ) ) )
= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,139]) ).
thf(222,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ pack2 ) @ ( i @ ( B @ pack1 ) @ ( o @ ( B @ unpack1 ) ) ) )
= B )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[221:[]]) ).
thf(21420,plain,
! [B: $i,A: $i] :
( ( B != o )
| ( ( A @ ( B @ pack2 ) @ ( i @ ( B @ pack1 ) @ ( o @ ( B @ unpack1 ) ) ) )
!= A )
| ( A = o ) ),
inference(eqfactor_ordered,[status(thm)],[222]) ).
thf(21474,plain,
! [A: $i] :
( ( ( A @ ( o @ pack2 ) @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
!= A )
| ( A = o ) ),
inference(simp,[status(thm)],[21420]) ).
thf(21780,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ ( o @ pack2 ) @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) ) )
| ( ( o @ inv )
!= B )
| ( B = o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[9477,21474]) ).
thf(21781,plain,
! [A: $i] :
( ( ( o @ inv )
!= A )
| ( A = o )
| ( ( A @ ( o @ pack2 ) @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[21780:[bind(A,$thf( J @ ( o @ pack2 ) @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )),bind(B,$thf( J ))]]) ).
thf(21882,plain,
( ( ( o @ inv )
= o )
| ( ( o @ inv @ ( o @ pack2 ) @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[21781]) ).
thf(22181,plain,
( ( o @ inv @ ( o @ pack2 ) @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o ),
inference(simplifyReflect,[status(thm)],[21882,10711]) ).
thf(31732,plain,
! [A: $i] :
( ( ( o @ inv )
!= ( o @ inv ) )
| ( ( A @ ( o @ pack2 ) @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( A @ inv )
!= o ) ),
inference(paramod_ordered,[status(thm)],[26968,22181]) ).
thf(31733,plain,
! [A: $i] :
( ( ( A @ ( o @ pack2 ) @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( A @ inv )
!= o ) ),
inference(pattern_uni,[status(thm)],[31732:[]]) ).
thf(420,plain,
! [B: $i,A: $i] :
( ( i != i )
| ( ( B @ ( A @ pack2 ) @ ( B @ ( i @ pack1 ) @ ( B @ ( o @ unpack2 ) ) ) )
= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,404]) ).
thf(421,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( B @ ( i @ pack1 ) @ ( B @ ( o @ unpack2 ) ) ) )
= B )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[420:[]]) ).
thf(48040,plain,
! [B: $i,A: $i] :
( ( B != o )
| ( ( B @ ( A @ pack2 ) @ ( B @ ( i @ pack1 ) @ ( B @ ( o @ unpack2 ) ) ) )
!= A )
| ( A = o ) ),
inference(eqfactor_ordered,[status(thm)],[421]) ).
thf(48055,plain,
! [A: $i] :
( ( ( o @ ( A @ pack2 ) @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
!= A )
| ( A = o ) ),
inference(simp,[status(thm)],[48040]) ).
thf(49947,plain,
! [B: $i,A: $i] :
( ( A
!= ( o @ ( B @ pack2 ) ) )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
!= B )
| ( B = o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,48055]) ).
thf(49948,plain,
! [A: $i] :
( ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
!= A )
| ( A = o )
| ( ( o @ ( A @ pack2 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[49947:[bind(A,$thf( o @ ( C @ pack2 ) )),bind(B,$thf( C ))]]) ).
thf(50011,plain,
( ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( o @ ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[49948]) ).
thf(56403,plain,
! [A: $i] :
( ( ( o @ ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) @ pack2 ) )
!= ( o @ ( A @ pack2 ) ) )
| ( ( o @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
!= A )
| ( A = o )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(paramod_ordered,[status(thm)],[50011,48055]) ).
thf(56404,plain,
( ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
!= ( o @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) ) )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[56403:[bind(A,$thf( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) ))]]) ).
thf(56806,plain,
( ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
!= ( o @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) ) )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[56404]) ).
thf(83433,plain,
! [A: $i] :
( ( A
!= ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) ) )
| ( ( o @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
!= i )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[4511,56806]) ).
thf(83434,plain,
( ( ( o @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
!= i )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[83433:[bind(A,$thf( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) ))]]) ).
thf(83868,plain,
( ( ( o @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
!= i )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[83434]) ).
thf(657,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ ( i @ pack2 ) ) )
| ( ( i @ ( i @ ( B @ ( o @ unpack1 ) ) ) )
= i )
| ( ( B @ ( i @ pack1 ) )
= o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,190]) ).
thf(658,plain,
! [A: $i] :
( ( ( i @ ( i @ ( A @ ( o @ unpack1 ) ) ) )
= i )
| ( ( A @ ( i @ pack1 ) )
= o )
| ( ( A @ ( i @ pack2 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[657:[bind(A,$thf( D @ ( i @ pack2 ) )),bind(B,$thf( D ))]]) ).
thf(702,plain,
! [A: $i] :
( ( ( i @ ( i @ ( A @ ( o @ unpack1 ) ) ) )
= i )
| ( ( A @ ( i @ pack1 ) )
= o )
| ( ( A @ ( i @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[658]) ).
thf(532,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ inv @ ( B @ ( A @ unpack2 ) ) ) )
!= ( D @ ( C @ pack2 ) @ ( D @ ( C @ pack1 ) @ ( D @ inv @ ( C @ unpack2 ) ) ) ) )
| ( B = D ) ),
inference(paramod_ordered,[status(thm)],[36,34]) ).
thf(541,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) )
!= ( D @ ( C @ pack2 ) ) )
| ( ( B @ ( A @ pack1 ) @ inv )
!= ( D @ ( C @ pack1 ) ) )
| ( B
!= ( D @ inv ) )
| ( A != C )
| ( B = D ) ),
inference(simp,[status(thm)],[532]) ).
thf(559,plain,
! [B: $i,A: $i] :
( ( ( B @ inv @ ( A @ pack2 ) )
!= ( B @ ( A @ pack2 ) ) )
| ( ( B @ inv @ ( A @ pack1 ) @ inv )
!= ( B @ ( A @ pack1 ) ) )
| ( ( B @ inv )
= B ) ),
inference(simp,[status(thm)],[541]) ).
thf(485,plain,
! [B: $i,A: $i] :
( ( i != i )
| ( ( i @ ( B @ pack2 ) @ ( A @ ( B @ pack1 ) @ ( o @ ( B @ unpack2 ) ) ) )
= i )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,438]) ).
thf(486,plain,
! [B: $i,A: $i] :
( ( ( i @ ( B @ pack2 ) @ ( A @ ( B @ pack1 ) @ ( o @ ( B @ unpack2 ) ) ) )
= i )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[485:[]]) ).
thf(2964,plain,
! [B: $i,A: $i] :
( ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) @ ( o @ pack1 ) )
!= ( A @ ( B @ pack1 ) ) )
| ( ( i @ ( B @ pack2 ) @ ( o @ ( o @ ( B @ unpack2 ) ) ) )
= i )
| ( A = o )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(paramod_ordered,[status(thm)],[2895,486]) ).
thf(2965,plain,
( ( ( i @ ( o @ pack2 ) @ ( o @ ( o @ ( o @ unpack2 ) ) ) )
= i )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[2964:[bind(A,$thf( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )),bind(B,$thf( o ))]]) ).
thf(3099,plain,
( ( ( i @ ( o @ pack2 ) @ ( o @ ( o @ ( o @ unpack2 ) ) ) )
= i )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[2965]) ).
thf(32418,plain,
! [B: $i,A: $i] :
( ( ( o @ inv )
!= ( A @ inv ) )
| ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( i @ unpack2 ) ) ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[31674,32]) ).
thf(32419,plain,
! [A: $i] :
( ( A @ ( o @ pack2 ) @ ( A @ ( o @ pack1 ) @ ( A @ ( i @ unpack2 ) ) ) )
= A ),
inference(pattern_uni,[status(thm)],[32418:[bind(A,$thf( o ))]]) ).
thf(32504,plain,
! [A: $i] :
( ( A @ ( o @ pack2 ) @ ( A @ ( o @ pack1 ) @ ( A @ ( i @ unpack2 ) ) ) )
= A ),
inference(simp,[status(thm)],[32419]) ).
thf(3,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack1 ) ) ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unpack1) ).
thf(19,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack1 ) ) ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(20,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack1 ) ) ) )
= A ),
inference(lifteq,[status(thm)],[19]) ).
thf(385,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ inv )
!= ( B @ inv ) )
| ( ( C @ ( B @ pack2 ) @ ( C @ ( B @ pack1 ) @ ( C @ ( o @ unpack2 ) ) ) )
= C )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[126,32]) ).
thf(386,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( o @ unpack2 ) ) ) )
= B )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[385:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(397,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( o @ unpack2 ) ) ) )
= B )
| ( A = o ) ),
inference(simp,[status(thm)],[386]) ).
thf(56204,plain,
! [B: $i,A: $i] :
( ( ( o @ ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) @ pack2 ) )
!= ( B @ ( A @ pack2 ) ) )
| ( ( o @ ( B @ ( A @ pack1 ) @ ( B @ ( o @ unpack2 ) ) ) )
= B )
| ( A = o )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(paramod_ordered,[status(thm)],[50011,397]) ).
thf(56205,plain,
( ( ( o @ ( o @ ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[56204:[bind(A,$thf( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )),bind(B,$thf( o ))]]) ).
thf(56901,plain,
( ( ( o @ ( o @ ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[56205]) ).
thf(9850,plain,
! [B: $i,A: $i] :
( ( A
!= ( i @ ( o @ pack2 ) @ ( B @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) ) )
| ( ( o @ inv )
!= B )
| ( B = o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[9477,2559]) ).
thf(9851,plain,
! [A: $i] :
( ( ( o @ inv )
!= A )
| ( A = o )
| ( ( i @ ( o @ pack2 ) @ ( A @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[9850:[bind(A,$thf( i @ ( o @ pack2 ) @ ( H @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )),bind(B,$thf( H ))]]) ).
thf(10495,plain,
( ( ( o @ inv )
= o )
| ( ( i @ ( o @ pack2 ) @ ( o @ inv @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[9851]) ).
thf(13128,plain,
( ( i @ ( o @ pack2 ) @ ( o @ inv @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o ),
inference(simplifyReflect,[status(thm)],[10495,10711]) ).
thf(32093,plain,
! [A: $i] :
( ( ( o @ inv )
!= ( o @ inv ) )
| ( ( i @ ( o @ pack2 ) @ ( A @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( A @ inv )
!= o ) ),
inference(paramod_ordered,[status(thm)],[26968,13128]) ).
thf(32094,plain,
! [A: $i] :
( ( ( i @ ( o @ pack2 ) @ ( A @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( A @ inv )
!= o ) ),
inference(pattern_uni,[status(thm)],[32093:[]]) ).
thf(130992,plain,
! [B: $i,A: $i] :
( ( ( A @ inv @ inv )
!= ( B @ inv ) )
| ( ( i @ ( o @ pack2 ) @ ( B @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( o != o )
| ( A = i ) ),
inference(paramod_ordered,[status(thm)],[129481,32094]) ).
thf(130993,plain,
! [B: $i,A: $i] :
( ( ( A @ inv @ inv )
!= ( B @ inv ) )
| ( ( i @ ( o @ pack2 ) @ ( B @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( A = i ) ),
inference(simp,[status(thm)],[130992]) ).
thf(130994,plain,
! [A: $i] :
( ( ( i @ ( o @ pack2 ) @ ( A @ inv @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( A = i ) ),
inference(pattern_uni,[status(thm)],[130993:[bind(A,$thf( C )),bind(B,$thf( C @ inv ))]]) ).
thf(131405,plain,
! [A: $i] :
( ( ( i @ ( o @ pack2 ) @ ( A @ inv @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( A = i ) ),
inference(simp,[status(thm)],[130994]) ).
thf(10241,plain,
! [C: $i,B: $i,A: $i] :
( ( ( o @ inv )
!= ( B @ inv ) )
| ( ( C @ ( B @ pack2 ) @ ( C @ ( B @ pack1 ) @ ( C @ ( A @ unpack1 ) ) ) )
= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[9477,22]) ).
thf(10242,plain,
! [B: $i,A: $i] :
( ( ( B @ ( o @ pack2 ) @ ( B @ ( o @ pack1 ) @ ( B @ ( A @ unpack1 ) ) ) )
= o )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[10241:[bind(A,$thf( A )),bind(B,$thf( o ))]]) ).
thf(10454,plain,
! [B: $i,A: $i] :
( ( ( B @ ( o @ pack2 ) @ ( B @ ( o @ pack1 ) @ ( B @ ( A @ unpack1 ) ) ) )
= o )
| ( A = o ) ),
inference(simp,[status(thm)],[10242]) ).
thf(472,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack2 ) ) ) )
!= ( i @ ( C @ pack2 ) @ ( i @ ( C @ pack1 ) @ ( o @ ( C @ unpack2 ) ) ) ) )
| ( B = i ) ),
inference(paramod_ordered,[status(thm)],[30,438]) ).
thf(495,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) )
!= ( i @ ( C @ pack2 ) ) )
| ( ( B @ ( A @ pack1 ) )
!= ( i @ ( C @ pack1 ) ) )
| ( B != o )
| ( A != C )
| ( B = i ) ),
inference(simp,[status(thm)],[472]) ).
thf(505,plain,
! [A: $i] :
( ( ( i @ ( A @ pack2 ) )
!= ( o @ ( A @ pack2 ) ) )
| ( ( i @ ( A @ pack1 ) )
!= ( o @ ( A @ pack1 ) ) )
| ( i = o ) ),
inference(simp,[status(thm)],[495]) ).
thf(61511,plain,
! [A: $i] :
( ( ( i @ ( A @ pack2 ) )
!= ( o @ ( A @ pack2 ) ) )
| ( ( i @ ( A @ pack1 ) )
!= ( o @ ( A @ pack1 ) ) ) ),
inference(simplifyReflect,[status(thm)],[505,116]) ).
thf(39,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ inv @ unpack1 ) ) ) )
!= ( D @ ( C @ pack2 ) @ ( D @ ( C @ pack1 ) @ ( D @ ( C @ unpack1 ) ) ) ) )
| ( A = C ) ),
inference(paramod_ordered,[status(thm)],[22,20]) ).
thf(41,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) )
!= ( D @ ( C @ pack2 ) ) )
| ( ( B @ ( A @ pack1 ) )
!= ( D @ ( C @ pack1 ) ) )
| ( B != D )
| ( ( A @ inv )
!= C )
| ( A = C ) ),
inference(simp,[status(thm)],[39]) ).
thf(43,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ inv @ pack2 ) )
!= ( B @ ( A @ pack2 ) ) )
| ( ( B @ ( A @ inv @ pack1 ) )
!= ( B @ ( A @ pack1 ) ) )
| ( ( A @ inv )
= A ) ),
inference(simp,[status(thm)],[41]) ).
thf(45,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ inv @ pack2 ) )
!= ( B @ ( A @ pack2 ) ) )
| ( ( B @ ( A @ inv @ pack1 ) )
!= ( B @ ( A @ pack1 ) ) ) ),
inference(simplifyReflect,[status(thm)],[43,18]) ).
thf(356,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ inv )
!= ( B @ inv ) )
| ( ( C @ ( B @ inv @ pack2 ) )
!= ( C @ ( B @ pack2 ) ) )
| ( ( C @ ( o @ pack1 ) )
!= ( C @ ( B @ pack1 ) ) )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[126,45]) ).
thf(357,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ inv @ pack2 ) )
!= ( B @ ( A @ pack2 ) ) )
| ( ( B @ ( o @ pack1 ) )
!= ( B @ ( A @ pack1 ) ) )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[356:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(376,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ inv @ pack2 ) )
!= ( B @ ( A @ pack2 ) ) )
| ( ( B @ ( o @ pack1 ) )
!= ( B @ ( A @ pack1 ) ) )
| ( A = o ) ),
inference(simp,[status(thm)],[357]) ).
thf(601,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ pack2 ) @ inv ) )
| ( ( i @ ( C @ ( B @ pack1 ) @ ( C @ ( B @ unpack2 ) ) ) )
= C )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,38]) ).
thf(602,plain,
! [B: $i,A: $i] :
( ( ( i @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack2 ) ) ) )
= B )
| ( ( B @ ( A @ pack2 ) @ inv )
= o ) ),
inference(pattern_uni,[status(thm)],[601:[bind(A,$thf( F @ ( E @ pack2 ) @ inv )),bind(B,$thf( E )),bind(C,$thf( F ))]]) ).
thf(646,plain,
! [B: $i,A: $i] :
( ( ( i @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack2 ) ) ) )
= B )
| ( ( B @ ( A @ pack2 ) @ inv )
= o ) ),
inference(simp,[status(thm)],[602]) ).
thf(141,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ inv @ unpack1 ) ) ) )
!= ( D @ ( C @ pack2 ) @ ( D @ ( C @ pack1 ) @ ( D @ inv @ ( C @ unpack1 ) ) ) ) )
| ( A = C ) ),
inference(paramod_ordered,[status(thm)],[22,24]) ).
thf(151,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) )
!= ( D @ ( C @ pack2 ) ) )
| ( ( B @ ( A @ pack1 ) )
!= ( D @ ( C @ pack1 ) ) )
| ( B
!= ( D @ inv ) )
| ( ( A @ inv )
!= C )
| ( A = C ) ),
inference(simp,[status(thm)],[141]) ).
thf(158,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ inv @ pack2 ) )
!= ( B @ inv @ ( A @ pack2 ) ) )
| ( ( B @ ( A @ inv @ pack1 ) )
!= ( B @ inv @ ( A @ pack1 ) ) )
| ( ( A @ inv )
= A ) ),
inference(simp,[status(thm)],[151]) ).
thf(15623,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ inv @ pack2 ) )
!= ( B @ inv @ ( A @ pack2 ) ) )
| ( ( B @ ( A @ inv @ pack1 ) )
!= ( B @ inv @ ( A @ pack1 ) ) ) ),
inference(simplifyReflect,[status(thm)],[158,18]) ).
thf(58,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ pack2 ) ) )
| ( ( i @ ( C @ ( B @ pack1 ) @ ( C @ ( B @ unpack1 ) ) ) )
= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,20]) ).
thf(59,plain,
! [B: $i,A: $i] :
( ( ( i @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack2 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[58:[bind(A,$thf( E @ ( D @ pack2 ) )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(106,plain,
! [B: $i,A: $i] :
( ( ( i @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[59]) ).
thf(208,plain,
! [B: $i,A: $i] :
( ( A
!= ( i @ ( B @ pack2 ) ) )
| ( ( i @ ( i @ ( B @ pack1 ) @ ( o @ ( B @ unpack1 ) ) ) )
= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,139]) ).
thf(209,plain,
! [A: $i] :
( ( ( i @ ( i @ ( A @ pack1 ) @ ( o @ ( A @ unpack1 ) ) ) )
= A )
| ( ( i @ ( A @ pack2 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[208:[bind(A,$thf( i @ ( C @ pack2 ) )),bind(B,$thf( C ))]]) ).
thf(238,plain,
! [A: $i] :
( ( ( i @ ( i @ ( A @ pack1 ) @ ( o @ ( A @ unpack1 ) ) ) )
= A )
| ( ( i @ ( A @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[209]) ).
thf(478,plain,
! [B: $i,A: $i] :
( ( A
!= ( i @ ( B @ pack1 ) ) )
| ( ( i @ ( B @ pack2 ) @ ( i @ ( o @ ( B @ unpack2 ) ) ) )
= i )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,438]) ).
thf(479,plain,
! [A: $i] :
( ( ( i @ ( A @ pack2 ) @ ( i @ ( o @ ( A @ unpack2 ) ) ) )
= i )
| ( ( i @ ( A @ pack1 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[478:[bind(A,$thf( i @ ( C @ pack1 ) )),bind(B,$thf( C ))]]) ).
thf(514,plain,
! [A: $i] :
( ( ( i @ ( A @ pack2 ) @ ( i @ ( o @ ( A @ unpack2 ) ) ) )
= i )
| ( ( i @ ( A @ pack1 ) )
= o ) ),
inference(simp,[status(thm)],[479]) ).
thf(7,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ inv @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack1 ) ) ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unpack1_04) ).
thf(27,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ inv @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack1 ) ) ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(28,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ pack2 ) @ inv @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack1 ) ) ) )
= A ),
inference(lifteq,[status(thm)],[27]) ).
thf(730,plain,
! [C: $i,B: $i,A: $i] :
( ( ( i @ ( A @ ( i @ pack1 ) @ ( A @ ( o @ unpack1 ) ) ) )
!= ( C @ ( B @ pack2 ) @ inv @ ( C @ ( B @ pack1 ) @ ( C @ ( B @ unpack1 ) ) ) ) )
| ( i = B )
| ( ( A @ ( i @ pack2 ) )
= o ) ),
inference(paramod_ordered,[status(thm)],[191,28]) ).
thf(742,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ pack2 ) @ inv )
!= i )
| ( ( A @ ( i @ pack1 ) )
!= ( C @ ( B @ pack1 ) ) )
| ( A != C )
| ( o != B )
| ( i = B )
| ( ( A @ ( i @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[730]) ).
thf(754,plain,
! [A: $i] :
( ( ( A @ ( o @ pack2 ) @ inv )
!= i )
| ( ( A @ ( i @ pack1 ) )
!= ( A @ ( o @ pack1 ) ) )
| ( i = o )
| ( ( A @ ( i @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[742]) ).
thf(112477,plain,
! [A: $i] :
( ( ( A @ ( o @ pack2 ) @ inv )
!= i )
| ( ( A @ ( i @ pack1 ) )
!= ( A @ ( o @ pack1 ) ) )
| ( ( A @ ( i @ pack2 ) )
= o ) ),
inference(simplifyReflect,[status(thm)],[754,116]) ).
thf(2956,plain,
! [A: $i] :
( ( A
!= ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) ) )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( i @ ( o @ pack1 ) )
= o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,2895]) ).
thf(2957,plain,
( ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( i @ ( o @ pack1 ) )
= o )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[2956:[bind(A,$thf( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) ))]]) ).
thf(3097,plain,
( ( ( i @ ( o @ pack1 ) )
= o )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[2957]) ).
thf(3168,plain,
! [A: $i] :
( ( A
!= ( i @ ( o @ pack2 ) ) )
| ( ( i @ ( o @ pack1 ) )
= o )
| ( ( i @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,3097]) ).
thf(3169,plain,
( ( ( i @ ( o @ pack1 ) )
= o )
| ( ( i @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( i @ ( o @ pack2 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[3168:[bind(A,$thf( i @ ( o @ pack2 ) ))]]) ).
thf(205,plain,
! [B: $i,A: $i] :
( ( ( A @ ( i @ pack2 ) @ ( A @ ( i @ pack1 ) @ ( A @ ( o @ unpack1 ) ) ) )
!= ( i @ ( B @ pack2 ) @ ( i @ ( B @ pack1 ) @ ( o @ ( B @ unpack1 ) ) ) ) )
| ( i = B ) ),
inference(paramod_ordered,[status(thm)],[128,139]) ).
thf(225,plain,
! [B: $i,A: $i] :
( ( ( A @ ( i @ pack2 ) )
!= ( i @ ( B @ pack2 ) ) )
| ( ( A @ ( i @ pack1 ) )
!= ( i @ ( B @ pack1 ) ) )
| ( A != o )
| ( o != B )
| ( i = B ) ),
inference(simp,[status(thm)],[205]) ).
thf(232,plain,
( ( ( o @ ( i @ pack2 ) )
!= ( i @ ( o @ pack2 ) ) )
| ( ( o @ ( i @ pack1 ) )
!= ( i @ ( o @ pack1 ) ) )
| ( i = o ) ),
inference(simp,[status(thm)],[225]) ).
thf(901,plain,
( ( ( o @ ( i @ pack2 ) )
!= ( i @ ( o @ pack2 ) ) )
| ( ( o @ ( i @ pack1 ) )
!= ( i @ ( o @ pack1 ) ) ) ),
inference(simplifyReflect,[status(thm)],[232,116]) ).
thf(910,plain,
! [A: $i] :
( ( A
!= ( o @ ( i @ pack2 ) ) )
| ( ( i @ ( o @ pack2 ) )
!= i )
| ( ( o @ ( i @ pack1 ) )
!= ( i @ ( o @ pack1 ) ) )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,901]) ).
thf(911,plain,
( ( ( i @ ( o @ pack2 ) )
!= i )
| ( ( o @ ( i @ pack1 ) )
!= ( i @ ( o @ pack1 ) ) )
| ( ( o @ ( i @ pack2 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[910:[bind(A,$thf( o @ ( i @ pack2 ) ))]]) ).
thf(294,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( i @ pack2 ) @ ( A @ ( i @ pack1 ) @ ( A @ ( o @ unpack1 ) ) ) )
!= ( C @ ( B @ pack2 ) @ inv @ ( C @ ( B @ pack1 ) @ ( C @ ( B @ unpack1 ) ) ) ) )
| ( i = B ) ),
inference(paramod_ordered,[status(thm)],[128,28]) ).
thf(321,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( i @ pack2 ) )
!= ( C @ ( B @ pack2 ) @ inv ) )
| ( ( A @ ( i @ pack1 ) )
!= ( C @ ( B @ pack1 ) ) )
| ( A != C )
| ( o != B )
| ( i = B ) ),
inference(simp,[status(thm)],[294]) ).
thf(323,plain,
! [A: $i] :
( ( ( A @ ( i @ pack2 ) )
!= ( A @ ( o @ pack2 ) @ inv ) )
| ( ( A @ ( i @ pack1 ) )
!= ( A @ ( o @ pack1 ) ) )
| ( i = o ) ),
inference(simp,[status(thm)],[321]) ).
thf(34875,plain,
! [A: $i] :
( ( ( A @ ( i @ pack2 ) )
!= ( A @ ( o @ pack2 ) @ inv ) )
| ( ( A @ ( i @ pack1 ) )
!= ( A @ ( o @ pack1 ) ) ) ),
inference(simplifyReflect,[status(thm)],[323,116]) ).
thf(34924,plain,
! [A: $i] :
( ( ( o @ ( i @ pack2 ) )
!= ( A @ ( i @ pack2 ) ) )
| ( ( A @ ( o @ pack2 ) @ inv )
!= o )
| ( ( A @ ( i @ pack1 ) )
!= ( A @ ( o @ pack1 ) ) )
| ( ( i @ ( o @ pack2 ) )
!= i )
| ( ( o @ ( i @ pack1 ) )
!= ( i @ ( o @ pack1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[911,34875]) ).
thf(34925,plain,
( ( ( o @ ( o @ pack2 ) @ inv )
!= o )
| ( ( o @ ( i @ pack1 ) )
!= ( o @ ( o @ pack1 ) ) )
| ( ( i @ ( o @ pack2 ) )
!= i )
| ( ( o @ ( i @ pack1 ) )
!= ( i @ ( o @ pack1 ) ) ) ),
inference(pattern_uni,[status(thm)],[34924:[bind(A,$thf( o ))]]) ).
thf(59224,plain,
( ( ( o @ ( o @ pack2 ) @ inv )
!= ( i @ inv ) )
| ( o != o )
| ( ( o @ ( i @ pack1 ) )
!= ( o @ ( o @ pack1 ) ) )
| ( ( i @ ( o @ pack2 ) )
!= i )
| ( ( o @ ( i @ pack1 ) )
!= ( i @ ( o @ pack1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[97,34925]) ).
thf(59225,plain,
( ( ( o @ ( o @ pack2 ) @ inv )
!= ( i @ inv ) )
| ( ( o @ ( i @ pack1 ) )
!= ( o @ ( o @ pack1 ) ) )
| ( ( i @ ( o @ pack2 ) )
!= i )
| ( ( o @ ( i @ pack1 ) )
!= ( i @ ( o @ pack1 ) ) ) ),
inference(simp,[status(thm)],[59224]) ).
thf(59594,plain,
( ( ( o @ ( o @ pack2 ) )
!= i )
| ( ( o @ ( i @ pack1 ) )
!= ( o @ ( o @ pack1 ) ) )
| ( ( i @ ( o @ pack2 ) )
!= i )
| ( ( o @ ( i @ pack1 ) )
!= ( i @ ( o @ pack1 ) ) ) ),
inference(simp,[status(thm)],[59225]) ).
thf(21627,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ ( o @ pack2 ) ) )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
!= B )
| ( B = o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,21474]) ).
thf(21628,plain,
! [A: $i] :
( ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
!= A )
| ( A = o )
| ( ( A @ ( o @ pack2 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[21627:[bind(A,$thf( D @ ( o @ pack2 ) )),bind(B,$thf( D ))]]) ).
thf(21932,plain,
( ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) @ ( o @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[21628]) ).
thf(40904,plain,
! [B: $i,A: $i] :
( ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) @ ( o @ pack2 ) )
!= ( A @ ( B @ pack2 ) ) )
| ( ( o @ ( A @ ( B @ pack1 ) @ ( o @ ( B @ unpack1 ) ) ) )
= B )
| ( A = o )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(paramod_ordered,[status(thm)],[21932,347]) ).
thf(40905,plain,
( ( ( o @ ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[40904:[bind(A,$thf( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )),bind(B,$thf( o ))]]) ).
thf(41605,plain,
( ( ( o @ ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[40905]) ).
thf(64,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ inv @ pack2 ) ) )
| ( ( C @ ( B @ pack2 ) )
!= i )
| ( ( C @ ( B @ inv @ pack1 ) )
!= ( C @ ( B @ pack1 ) ) )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,45]) ).
thf(65,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ pack2 ) )
!= i )
| ( ( A @ ( B @ inv @ pack1 ) )
!= ( A @ ( B @ pack1 ) ) )
| ( ( A @ ( B @ inv @ pack2 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[64:[bind(A,$thf( E @ ( F @ inv @ pack2 ) )),bind(B,$thf( F )),bind(C,$thf( E ))]]) ).
thf(91,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ pack2 ) )
!= i )
| ( ( A @ ( B @ inv @ pack1 ) )
!= ( A @ ( B @ pack1 ) ) )
| ( ( A @ ( B @ inv @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[65]) ).
thf(929,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ inv @ pack2 ) )
!= ( o @ ( i @ pack2 ) ) )
| ( ( i @ ( o @ pack2 ) )
!= o )
| ( ( o @ ( i @ pack1 ) )
!= ( i @ ( o @ pack1 ) ) )
| ( ( A @ ( B @ pack2 ) )
!= i )
| ( ( A @ ( B @ inv @ pack1 ) )
!= ( A @ ( B @ pack1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[91,901]) ).
thf(996,plain,
! [B: $i,A: $i] :
( ( A != o )
| ( ( B @ inv )
!= i )
| ( ( i @ ( o @ pack2 ) )
!= o )
| ( ( o @ ( i @ pack1 ) )
!= ( i @ ( o @ pack1 ) ) )
| ( ( A @ ( B @ pack2 ) )
!= i )
| ( ( A @ ( B @ inv @ pack1 ) )
!= ( A @ ( B @ pack1 ) ) ) ),
inference(simp,[status(thm)],[929]) ).
thf(1047,plain,
! [A: $i] :
( ( ( A @ inv )
!= i )
| ( ( i @ ( o @ pack2 ) )
!= o )
| ( ( o @ ( i @ pack1 ) )
!= ( i @ ( o @ pack1 ) ) )
| ( ( o @ ( A @ pack2 ) )
!= i )
| ( ( o @ ( A @ inv @ pack1 ) )
!= ( o @ ( A @ pack1 ) ) ) ),
inference(simp,[status(thm)],[996]) ).
thf(407,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ ( i @ pack1 ) ) )
| ( ( B @ ( i @ pack2 ) @ ( i @ ( B @ ( o @ unpack2 ) ) ) )
= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,404]) ).
thf(408,plain,
! [A: $i] :
( ( ( A @ ( i @ pack2 ) @ ( i @ ( A @ ( o @ unpack2 ) ) ) )
= A )
| ( ( A @ ( i @ pack1 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[407:[bind(A,$thf( D @ ( i @ pack1 ) )),bind(B,$thf( D ))]]) ).
thf(429,plain,
! [A: $i] :
( ( ( A @ ( i @ pack2 ) @ ( i @ ( A @ ( o @ unpack2 ) ) ) )
= A )
| ( ( A @ ( i @ pack1 ) )
= o ) ),
inference(simp,[status(thm)],[408]) ).
thf(66,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( B @ inv ) )
| ( ( C @ ( i @ pack2 ) )
!= ( C @ ( B @ pack2 ) ) )
| ( ( C @ ( B @ inv @ pack1 ) )
!= ( C @ ( B @ pack1 ) ) )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,45]) ).
thf(67,plain,
! [B: $i,A: $i] :
( ( ( A @ ( i @ pack2 ) )
!= ( A @ ( B @ pack2 ) ) )
| ( ( A @ ( B @ inv @ pack1 ) )
!= ( A @ ( B @ pack1 ) ) )
| ( ( B @ inv )
= o ) ),
inference(pattern_uni,[status(thm)],[66:[bind(A,$thf( D @ inv )),bind(B,$thf( D ))]]) ).
thf(92,plain,
! [B: $i,A: $i] :
( ( ( A @ ( i @ pack2 ) )
!= ( A @ ( B @ pack2 ) ) )
| ( ( A @ ( B @ inv @ pack1 ) )
!= ( A @ ( B @ pack1 ) ) )
| ( ( B @ inv )
= o ) ),
inference(simp,[status(thm)],[67]) ).
thf(111,plain,
! [B: $i,A: $i] :
( ( ( i @ inv )
!= ( A @ inv ) )
| ( ( B @ ( o @ pack2 ) )
!= ( B @ ( A @ pack2 ) ) )
| ( ( B @ ( A @ inv @ pack1 ) )
!= ( B @ ( A @ pack1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[97,45]) ).
thf(112,plain,
! [A: $i] :
( ( ( A @ ( i @ pack2 ) )
!= ( A @ ( o @ pack2 ) ) )
| ( ( A @ ( i @ inv @ pack1 ) )
!= ( A @ ( i @ pack1 ) ) ) ),
inference(pattern_uni,[status(thm)],[111:[bind(A,$thf( i ))]]) ).
thf(127,plain,
! [A: $i] :
( ( ( A @ ( i @ pack2 ) )
!= ( A @ ( o @ pack2 ) ) )
| ( ( A @ ( i @ inv @ pack1 ) )
!= ( A @ ( i @ pack1 ) ) ) ),
inference(simp,[status(thm)],[112]) ).
thf(562,plain,
! [A: $i] :
( ( ( A @ ( i @ pack2 ) )
!= ( A @ ( o @ pack2 ) ) )
| ( ( A @ ( i @ pack1 ) )
!= ( A @ ( o @ pack1 ) ) ) ),
inference(rewrite,[status(thm)],[127,97]) ).
thf(570,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ ( i @ pack2 ) ) )
| ( ( B @ ( o @ pack2 ) )
!= i )
| ( ( B @ ( i @ pack1 ) )
!= ( B @ ( o @ pack1 ) ) )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,562]) ).
thf(571,plain,
! [A: $i] :
( ( ( A @ ( o @ pack2 ) )
!= i )
| ( ( A @ ( i @ pack1 ) )
!= ( A @ ( o @ pack1 ) ) )
| ( ( A @ ( i @ pack2 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[570:[bind(A,$thf( D @ ( i @ pack2 ) )),bind(B,$thf( D ))]]) ).
thf(583,plain,
! [A: $i] :
( ( ( A @ ( o @ pack2 ) )
!= i )
| ( ( A @ ( i @ pack1 ) )
!= ( A @ ( o @ pack1 ) ) )
| ( ( A @ ( i @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[571]) ).
thf(447,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ pack1 ) ) )
| ( ( C @ ( B @ pack2 ) @ ( i @ ( C @ inv @ ( B @ unpack2 ) ) ) )
= C )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,34]) ).
thf(448,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( i @ ( B @ inv @ ( A @ unpack2 ) ) ) )
= B )
| ( ( B @ ( A @ pack1 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[447:[bind(A,$thf( E @ ( D @ pack1 ) )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(461,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( i @ ( B @ inv @ ( A @ unpack2 ) ) ) )
= B )
| ( ( B @ ( A @ pack1 ) )
= o ) ),
inference(simp,[status(thm)],[448]) ).
thf(487,plain,
! [B: $i,A: $i] :
( ( i != i )
| ( ( A @ ( B @ pack2 ) @ ( i @ ( B @ pack1 ) @ ( o @ ( B @ unpack2 ) ) ) )
= i )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,438]) ).
thf(488,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ pack2 ) @ ( i @ ( B @ pack1 ) @ ( o @ ( B @ unpack2 ) ) ) )
= i )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[487:[]]) ).
thf(41065,plain,
! [B: $i,A: $i] :
( ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) @ ( o @ pack2 ) )
!= ( A @ ( B @ pack2 ) ) )
| ( ( o @ ( i @ ( B @ pack1 ) @ ( o @ ( B @ unpack2 ) ) ) )
= i )
| ( A = o )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(paramod_ordered,[status(thm)],[21932,488]) ).
thf(41066,plain,
( ( ( o @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= i )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[41065:[bind(A,$thf( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )),bind(B,$thf( o ))]]) ).
thf(41466,plain,
( ( ( o @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= i )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[41066]) ).
thf(520,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ pack1 ) @ inv ) )
| ( ( C @ ( B @ pack2 ) @ ( i @ ( C @ ( B @ unpack2 ) ) ) )
= C )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,36]) ).
thf(521,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( i @ ( B @ ( A @ unpack2 ) ) ) )
= B )
| ( ( B @ ( A @ pack1 ) @ inv )
= o ) ),
inference(pattern_uni,[status(thm)],[520:[bind(A,$thf( F @ ( E @ pack1 ) @ inv )),bind(B,$thf( E )),bind(C,$thf( F ))]]) ).
thf(551,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( i @ ( B @ ( A @ unpack2 ) ) ) )
= B )
| ( ( B @ ( A @ pack1 ) @ inv )
= o ) ),
inference(simp,[status(thm)],[521]) ).
thf(297,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ pack1 ) ) )
| ( ( C @ ( B @ pack2 ) @ inv @ ( i @ ( C @ ( B @ unpack1 ) ) ) )
= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,28]) ).
thf(298,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ inv @ ( i @ ( B @ ( A @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack1 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[297:[bind(A,$thf( E @ ( D @ pack1 ) )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(324,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ inv @ ( i @ ( B @ ( A @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack1 ) )
= o ) ),
inference(simp,[status(thm)],[298]) ).
thf(295,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ inv @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack1 ) ) ) )
!= ( D @ ( C @ pack2 ) @ ( D @ ( C @ pack1 ) @ ( D @ ( C @ inv @ unpack1 ) ) ) ) )
| ( A = C ) ),
inference(paramod_ordered,[status(thm)],[28,22]) ).
thf(315,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ inv )
!= ( D @ ( C @ pack2 ) ) )
| ( ( B @ ( A @ pack1 ) )
!= ( D @ ( C @ pack1 ) ) )
| ( B != D )
| ( A
!= ( C @ inv ) )
| ( A = C ) ),
inference(simp,[status(thm)],[295]) ).
thf(334,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ inv @ pack2 ) @ inv )
!= ( B @ ( A @ pack2 ) ) )
| ( ( B @ ( A @ inv @ pack1 ) )
!= ( B @ ( A @ pack1 ) ) )
| ( ( A @ inv )
= A ) ),
inference(simp,[status(thm)],[315]) ).
thf(37870,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ inv @ pack2 ) @ inv )
!= ( B @ ( A @ pack2 ) ) )
| ( ( B @ ( A @ inv @ pack1 ) )
!= ( B @ ( A @ pack1 ) ) ) ),
inference(simplifyReflect,[status(thm)],[334,18]) ).
thf(37872,plain,
! [B: $i,A: $i] :
( ( ( o @ inv )
!= ( A @ inv ) )
| ( ( B @ ( A @ inv @ pack2 ) @ inv )
!= ( B @ ( A @ pack2 ) ) )
| ( ( B @ ( i @ pack1 ) )
!= ( B @ ( A @ pack1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[31674,37870]) ).
thf(37873,plain,
! [A: $i] :
( ( ( A @ ( o @ inv @ pack2 ) @ inv )
!= ( A @ ( o @ pack2 ) ) )
| ( ( A @ ( i @ pack1 ) )
!= ( A @ ( o @ pack1 ) ) ) ),
inference(pattern_uni,[status(thm)],[37872:[bind(A,$thf( o ))]]) ).
thf(38102,plain,
! [A: $i] :
( ( ( A @ ( o @ inv @ pack2 ) @ inv )
!= ( A @ ( o @ pack2 ) ) )
| ( ( A @ ( i @ pack1 ) )
!= ( A @ ( o @ pack1 ) ) ) ),
inference(simp,[status(thm)],[37873]) ).
thf(108466,plain,
! [A: $i] :
( ( ( A @ ( i @ pack2 ) @ inv )
!= ( A @ ( o @ pack2 ) ) )
| ( ( A @ ( i @ pack1 ) )
!= ( A @ ( o @ pack1 ) ) ) ),
inference(rewrite,[status(thm)],[38102,31674]) ).
thf(39611,plain,
! [B: $i,A: $i] :
( ( B != o )
| ( ( A @ ( B @ pack2 ) @ ( A @ ( B @ pack1 ) @ ( o @ ( B @ unpack1 ) ) ) )
!= A )
| ( A = o ) ),
inference(eqfactor_ordered,[status(thm)],[347]) ).
thf(39615,plain,
! [A: $i] :
( ( ( A @ ( o @ pack2 ) @ ( A @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
!= A )
| ( A = o ) ),
inference(simp,[status(thm)],[39611]) ).
thf(148,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ pack2 ) ) )
| ( ( i @ ( C @ ( B @ pack1 ) @ ( C @ inv @ ( B @ unpack1 ) ) ) )
= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,24]) ).
thf(149,plain,
! [B: $i,A: $i] :
( ( ( i @ ( B @ ( A @ pack1 ) @ ( B @ inv @ ( A @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack2 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[148:[bind(A,$thf( E @ ( D @ pack2 ) )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(156,plain,
! [B: $i,A: $i] :
( ( ( i @ ( B @ ( A @ pack1 ) @ ( B @ inv @ ( A @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[149]) ).
thf(32420,plain,
! [B: $i,A: $i] :
( ( ( o @ inv )
!= ( B @ inv ) )
| ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( i @ ( A @ unpack2 ) ) ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[31674,34]) ).
thf(32421,plain,
! [A: $i] :
( ( o @ ( A @ pack2 ) @ ( o @ ( A @ pack1 ) @ ( i @ ( A @ unpack2 ) ) ) )
= o ),
inference(pattern_uni,[status(thm)],[32420:[bind(A,$thf( A )),bind(B,$thf( o ))]]) ).
thf(32539,plain,
! [B: $i,A: $i] :
( ( A
!= ( o @ ( B @ pack2 ) ) )
| ( ( i @ ( o @ ( B @ pack1 ) @ ( i @ ( B @ unpack2 ) ) ) )
= o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[4511,32421]) ).
thf(32540,plain,
! [A: $i] :
( ( ( i @ ( o @ ( A @ pack1 ) @ ( i @ ( A @ unpack2 ) ) ) )
= o )
| ( ( o @ ( A @ pack2 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[32539:[bind(A,$thf( o @ ( C @ pack2 ) )),bind(B,$thf( C ))]]) ).
thf(32735,plain,
! [A: $i] :
( ( ( i @ ( o @ ( A @ pack1 ) @ ( i @ ( A @ unpack2 ) ) ) )
= o )
| ( ( o @ ( A @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[32540]) ).
thf(46927,plain,
! [B: $i,A: $i] :
( ( ( o @ ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) @ pack1 ) )
!= ( B @ ( A @ pack1 ) ) )
| ( ( B @ ( A @ pack2 ) @ ( o @ ( B @ ( o @ unpack2 ) ) ) )
= B )
| ( A = o )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(paramod_ordered,[status(thm)],[46818,397]) ).
thf(46928,plain,
( ( ( o @ ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) @ pack2 ) @ ( o @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[46927:[bind(A,$thf( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )),bind(B,$thf( o ))]]) ).
thf(47495,plain,
( ( ( o @ ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) @ pack2 ) @ ( o @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[46928]) ).
thf(130913,plain,
! [B: $i,A: $i] :
( ( ( A @ inv @ inv )
!= ( B @ inv ) )
| ( ( B @ ( o @ pack2 ) @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( o != o )
| ( A = i ) ),
inference(paramod_ordered,[status(thm)],[129481,31733]) ).
thf(130914,plain,
! [B: $i,A: $i] :
( ( ( A @ inv @ inv )
!= ( B @ inv ) )
| ( ( B @ ( o @ pack2 ) @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( A = i ) ),
inference(simp,[status(thm)],[130913]) ).
thf(130915,plain,
! [A: $i] :
( ( ( A @ inv @ ( o @ pack2 ) @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( A = i ) ),
inference(pattern_uni,[status(thm)],[130914:[bind(A,$thf( C )),bind(B,$thf( C @ inv ))]]) ).
thf(131381,plain,
! [A: $i] :
( ( ( A @ inv @ ( o @ pack2 ) @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( A = i ) ),
inference(simp,[status(thm)],[130915]) ).
thf(40902,plain,
! [A: $i] :
( ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) @ ( o @ pack2 ) )
!= ( A @ ( o @ pack2 ) ) )
| ( ( o @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
!= A )
| ( A = o )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(paramod_ordered,[status(thm)],[21932,21474]) ).
thf(40903,plain,
( ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
!= ( o @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) ) )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[40902:[bind(A,$thf( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) ))]]) ).
thf(41602,plain,
( ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
!= ( o @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) ) )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[40903]) ).
thf(74085,plain,
! [A: $i] :
( ( A
!= ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) ) )
| ( ( o @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
!= i )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[4511,41602]) ).
thf(74086,plain,
( ( ( o @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
!= i )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[74085:[bind(A,$thf( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) ))]]) ).
thf(74471,plain,
( ( ( o @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
!= i )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[74086]) ).
thf(724,plain,
! [B: $i,A: $i] :
( ( i != i )
| ( ( i @ ( B @ ( A @ pack1 ) @ ( B @ ( o @ unpack1 ) ) ) )
= i )
| ( ( B @ ( i @ pack2 ) )
= o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,191]) ).
thf(725,plain,
! [B: $i,A: $i] :
( ( ( i @ ( B @ ( A @ pack1 ) @ ( B @ ( o @ unpack1 ) ) ) )
= i )
| ( ( B @ ( i @ pack2 ) )
= o )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[724:[]]) ).
thf(252,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ inv @ unpack1 ) ) ) )
!= ( D @ ( C @ pack2 ) @ ( D @ ( C @ pack1 ) @ inv @ ( D @ ( C @ unpack1 ) ) ) ) )
| ( A = C ) ),
inference(paramod_ordered,[status(thm)],[22,26]) ).
thf(267,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) )
!= ( D @ ( C @ pack2 ) ) )
| ( ( B @ ( A @ pack1 ) )
!= ( D @ ( C @ pack1 ) @ inv ) )
| ( B != D )
| ( ( A @ inv )
!= C )
| ( A = C ) ),
inference(simp,[status(thm)],[252]) ).
thf(280,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ inv @ pack2 ) )
!= ( B @ ( A @ pack2 ) ) )
| ( ( B @ ( A @ pack1 ) )
!= ( B @ ( A @ inv @ pack1 ) @ inv ) )
| ( ( A @ inv )
= A ) ),
inference(simp,[status(thm)],[267]) ).
thf(26473,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ inv @ pack2 ) )
!= ( B @ ( A @ pack2 ) ) )
| ( ( B @ ( A @ pack1 ) )
!= ( B @ ( A @ inv @ pack1 ) @ inv ) ) ),
inference(simplifyReflect,[status(thm)],[280,18]) ).
thf(26474,plain,
! [B: $i,A: $i] :
( ( B != B )
| ( ( A @ inv )
!= A )
| ( ( B @ ( A @ pack1 ) )
!= ( B @ ( A @ inv @ pack1 ) @ inv ) ) ),
inference(simp,[status(thm)],[26473]) ).
thf(26695,plain,
! [B: $i,A: $i] :
( ( ( A @ inv )
!= A )
| ( ( B @ ( A @ pack1 ) )
!= ( B @ ( A @ inv @ pack1 ) @ inv ) ) ),
inference(simp,[status(thm)],[26474]) ).
thf(32366,plain,
! [B: $i,A: $i] :
( ( ( o @ inv )
!= ( A @ inv ) )
| ( ( B @ ( A @ inv @ pack2 ) )
!= ( B @ inv @ ( A @ pack2 ) ) )
| ( ( B @ ( i @ pack1 ) )
!= ( B @ inv @ ( A @ pack1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[31674,15623]) ).
thf(32367,plain,
! [A: $i] :
( ( ( A @ ( o @ inv @ pack2 ) )
!= ( A @ inv @ ( o @ pack2 ) ) )
| ( ( A @ ( i @ pack1 ) )
!= ( A @ inv @ ( o @ pack1 ) ) ) ),
inference(pattern_uni,[status(thm)],[32366:[bind(A,$thf( o ))]]) ).
thf(32516,plain,
! [A: $i] :
( ( ( A @ ( o @ inv @ pack2 ) )
!= ( A @ inv @ ( o @ pack2 ) ) )
| ( ( A @ ( i @ pack1 ) )
!= ( A @ inv @ ( o @ pack1 ) ) ) ),
inference(simp,[status(thm)],[32367]) ).
thf(133815,plain,
! [A: $i] :
( ( ( A @ ( i @ pack2 ) )
!= ( A @ inv @ ( o @ pack2 ) ) )
| ( ( A @ ( i @ pack1 ) )
!= ( A @ inv @ ( o @ pack1 ) ) ) ),
inference(rewrite,[status(thm)],[32516,31674]) ).
thf(95844,plain,
! [B: $i,A: $i] :
( ( B
!= ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) ) )
| ( A
!= ( o @ ( i @ pack2 ) @ ( o @ ( o @ ( o @ unpack2 ) ) ) ) )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( A @ inv )
= i )
| ( B = o ) ),
inference(paramod_ordered,[status(thm)],[32386,47493]) ).
thf(95845,plain,
! [A: $i] :
( ( A
!= ( o @ ( i @ pack2 ) @ ( o @ ( o @ ( o @ unpack2 ) ) ) ) )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( A @ inv )
= i )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[95844:[bind(A,$thf( A )),bind(B,$thf( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) ))]]) ).
thf(97531,plain,
( ( ( o @ ( i @ pack2 ) @ ( o @ ( o @ ( o @ unpack2 ) ) ) @ inv )
= i )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[95845]) ).
thf(74,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ pack2 ) ) )
| ( ( i @ ( C @ ( B @ pack1 ) @ ( C @ ( B @ inv @ unpack1 ) ) ) )
= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,22]) ).
thf(75,plain,
! [B: $i,A: $i] :
( ( ( i @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ inv @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack2 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[74:[bind(A,$thf( E @ ( D @ pack2 ) )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(96,plain,
! [B: $i,A: $i] :
( ( ( i @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ inv @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[75]) ).
thf(37871,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ inv @ pack2 ) @ inv )
!= ( B @ ( A @ pack2 ) ) )
| ( B != B )
| ( ( A @ inv )
!= A ) ),
inference(simp,[status(thm)],[37870]) ).
thf(38100,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ inv @ pack2 ) @ inv )
!= ( B @ ( A @ pack2 ) ) )
| ( ( A @ inv )
!= A ) ),
inference(simp,[status(thm)],[37871]) ).
thf(515,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack1 ) @ inv )
!= ( i @ inv ) )
| ( ( B @ ( A @ pack2 ) @ ( o @ ( B @ ( A @ unpack2 ) ) ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[97,36]) ).
thf(537,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack1 ) )
!= i )
| ( ( B @ ( A @ pack2 ) @ ( o @ ( B @ ( A @ unpack2 ) ) ) )
= B ) ),
inference(simp,[status(thm)],[515]) ).
thf(13133,plain,
! [A: $i] :
( ( A
!= ( i @ ( o @ pack2 ) ) )
| ( ( i @ ( o @ inv @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,13128]) ).
thf(13134,plain,
( ( ( i @ ( o @ inv @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( i @ ( o @ pack2 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[13133:[bind(A,$thf( i @ ( o @ pack2 ) ))]]) ).
thf(32327,plain,
( ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( i @ ( o @ pack2 ) )
= o ) ),
inference(rewrite,[status(thm)],[13134,31674]) ).
thf(93919,plain,
! [B: $i,A: $i] :
( ( B
!= ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) ) )
| ( A
!= ( i @ ( o @ pack2 ) @ ( o @ ( o @ ( o @ unpack1 ) ) ) ) )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( A @ inv )
= i )
| ( B = o ) ),
inference(paramod_ordered,[status(thm)],[32386,3133]) ).
thf(93920,plain,
! [A: $i] :
( ( A
!= ( i @ ( o @ pack2 ) @ ( o @ ( o @ ( o @ unpack1 ) ) ) ) )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( A @ inv )
= i )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[93919:[bind(A,$thf( A )),bind(B,$thf( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) ))]]) ).
thf(98350,plain,
( ( ( i @ ( o @ pack2 ) @ ( o @ ( o @ ( o @ unpack1 ) ) ) @ inv )
= i )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[93920]) ).
thf(672,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ inv @ ( A @ unpack1 ) ) ) )
!= ( C @ ( i @ pack2 ) @ ( i @ ( C @ ( o @ unpack1 ) ) ) ) )
| ( A = i )
| ( ( C @ ( i @ pack1 ) )
= o ) ),
inference(paramod_ordered,[status(thm)],[24,190]) ).
thf(686,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) )
!= ( C @ ( i @ pack2 ) ) )
| ( ( B @ ( A @ pack1 ) )
!= i )
| ( ( B @ inv )
!= C )
| ( A != o )
| ( A = i )
| ( ( C @ ( i @ pack1 ) )
= o ) ),
inference(simp,[status(thm)],[672]) ).
thf(698,plain,
! [A: $i] :
( ( ( A @ inv @ ( i @ pack2 ) )
!= ( A @ ( o @ pack2 ) ) )
| ( ( A @ ( o @ pack1 ) )
!= i )
| ( i = o )
| ( ( A @ inv @ ( i @ pack1 ) )
= o ) ),
inference(simp,[status(thm)],[686]) ).
thf(107687,plain,
! [A: $i] :
( ( ( A @ inv @ ( i @ pack2 ) )
!= ( A @ ( o @ pack2 ) ) )
| ( ( A @ ( o @ pack1 ) )
!= i )
| ( ( A @ inv @ ( i @ pack1 ) )
= o ) ),
inference(simplifyReflect,[status(thm)],[698,116]) ).
thf(603,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ pack1 ) ) )
| ( ( C @ ( B @ pack2 ) @ inv @ ( i @ ( C @ ( B @ unpack2 ) ) ) )
= C )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,38]) ).
thf(604,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ inv @ ( i @ ( B @ ( A @ unpack2 ) ) ) )
= B )
| ( ( B @ ( A @ pack1 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[603:[bind(A,$thf( E @ ( D @ pack1 ) )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(647,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ inv @ ( i @ ( B @ ( A @ unpack2 ) ) ) )
= B )
| ( ( B @ ( A @ pack1 ) )
= o ) ),
inference(simp,[status(thm)],[604]) ).
thf(32541,plain,
! [B: $i,A: $i] :
( ( A
!= ( o @ ( B @ pack1 ) ) )
| ( ( o @ ( B @ pack2 ) @ ( i @ ( i @ ( B @ unpack2 ) ) ) )
= o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[4511,32421]) ).
thf(32542,plain,
! [A: $i] :
( ( ( o @ ( A @ pack2 ) @ ( i @ ( i @ ( A @ unpack2 ) ) ) )
= o )
| ( ( o @ ( A @ pack1 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[32541:[bind(A,$thf( o @ ( C @ pack1 ) )),bind(B,$thf( C ))]]) ).
thf(32736,plain,
! [A: $i] :
( ( ( o @ ( A @ pack2 ) @ ( i @ ( i @ ( A @ unpack2 ) ) ) )
= o )
| ( ( o @ ( A @ pack1 ) )
= o ) ),
inference(simp,[status(thm)],[32542]) ).
thf(74323,plain,
! [B: $i,A: $i] :
( ( B
!= ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) ) )
| ( A
!= ( o @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) ) )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( A @ inv )
!= o )
| ( B = o ) ),
inference(paramod_ordered,[status(thm)],[10777,41602]) ).
thf(74324,plain,
! [A: $i] :
( ( A
!= ( o @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) ) )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( A @ inv )
!= o )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[74323:[bind(A,$thf( A )),bind(B,$thf( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) ))]]) ).
thf(74467,plain,
( ( ( o @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) @ inv )
!= o )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[74324]) ).
thf(2005,plain,
! [A: $i] :
( ( ( o @ ( i @ pack2 ) )
!= ( A @ ( i @ pack2 ) ) )
| ( ( A @ ( o @ pack2 ) )
!= o )
| ( ( A @ ( i @ pack1 ) )
!= ( A @ ( o @ pack1 ) ) )
| ( ( i @ ( o @ pack2 ) )
!= i )
| ( ( o @ ( i @ pack1 ) )
!= ( i @ ( o @ pack1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[911,562]) ).
thf(2006,plain,
( ( ( o @ ( o @ pack2 ) )
!= o )
| ( ( o @ ( i @ pack1 ) )
!= ( o @ ( o @ pack1 ) ) )
| ( ( i @ ( o @ pack2 ) )
!= i )
| ( ( o @ ( i @ pack1 ) )
!= ( i @ ( o @ pack1 ) ) ) ),
inference(pattern_uni,[status(thm)],[2005:[bind(A,$thf( o ))]]) ).
thf(88,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ pack2 ) ) )
| ( ( i @ ( C @ ( B @ pack1 ) @ ( C @ ( B @ unpack2 ) ) ) )
= C )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,30]) ).
thf(89,plain,
! [B: $i,A: $i] :
( ( ( i @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack2 ) ) ) )
= B )
| ( ( B @ ( A @ pack2 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[88:[bind(A,$thf( E @ ( D @ pack2 ) )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(105,plain,
! [B: $i,A: $i] :
( ( ( i @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack2 ) ) ) )
= B )
| ( ( B @ ( A @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[89]) ).
thf(26401,plain,
! [A: $i] :
( ( ( o @ ( i @ pack2 ) )
!= ( A @ ( i @ pack2 ) ) )
| ( ( A @ ( o @ pack2 ) )
!= o )
| ( ( A @ ( i @ pack1 ) )
!= ( A @ ( o @ pack1 ) @ inv ) )
| ( ( i @ ( o @ pack2 ) )
!= i )
| ( ( o @ ( i @ pack1 ) )
!= ( i @ ( o @ pack1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[911,26333]) ).
thf(26402,plain,
( ( ( o @ ( o @ pack2 ) )
!= o )
| ( ( o @ ( i @ pack1 ) )
!= ( o @ ( o @ pack1 ) @ inv ) )
| ( ( i @ ( o @ pack2 ) )
!= i )
| ( ( o @ ( i @ pack1 ) )
!= ( i @ ( o @ pack1 ) ) ) ),
inference(pattern_uni,[status(thm)],[26401:[bind(A,$thf( o ))]]) ).
thf(56195,plain,
! [B: $i,A: $i] :
( ( ( o @ ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) @ pack2 ) )
!= ( B @ ( A @ pack2 ) ) )
| ( ( o @ ( B @ ( i @ pack1 ) @ ( B @ ( o @ unpack2 ) ) ) )
= B )
| ( A = o )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(paramod_ordered,[status(thm)],[50011,421]) ).
thf(56196,plain,
( ( ( o @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[56195:[bind(A,$thf( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )),bind(B,$thf( o ))]]) ).
thf(56892,plain,
( ( ( o @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[56196]) ).
thf(248,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack1 ) @ inv )
!= ( i @ inv ) )
| ( ( B @ ( A @ pack2 ) @ ( o @ ( B @ ( A @ unpack1 ) ) ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[97,26]) ).
thf(266,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack1 ) )
!= i )
| ( ( B @ ( A @ pack2 ) @ ( o @ ( B @ ( A @ unpack1 ) ) ) )
= A ) ),
inference(simp,[status(thm)],[248]) ).
thf(182,plain,
! [B: $i,A: $i] :
( ( i != i )
| ( ( B @ ( A @ pack2 ) @ ( B @ ( i @ pack1 ) @ ( B @ ( o @ unpack1 ) ) ) )
= i )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,128]) ).
thf(183,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( B @ ( i @ pack1 ) @ ( B @ ( o @ unpack1 ) ) ) )
= i )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[182:[]]) ).
thf(56553,plain,
! [B: $i,A: $i] :
( ( ( o @ ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) @ pack2 ) )
!= ( B @ ( A @ pack2 ) ) )
| ( ( o @ ( B @ ( i @ pack1 ) @ ( B @ ( o @ unpack1 ) ) ) )
= i )
| ( A = o )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(paramod_ordered,[status(thm)],[50011,183]) ).
thf(56554,plain,
( ( ( o @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= i )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[56553:[bind(A,$thf( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )),bind(B,$thf( o ))]]) ).
thf(56819,plain,
( ( ( o @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= i )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[56554]) ).
thf(15626,plain,
! [B: $i,A: $i] :
( ( ( B @ inv )
!= B )
| ( ( A @ inv )
!= A )
| ( ( B @ inv )
!= B )
| ( ( A @ inv )
!= A ) ),
inference(simp,[status(thm)],[15623]) ).
thf(15715,plain,
! [B: $i,A: $i] :
( ( ( B @ inv )
!= B )
| ( ( A @ inv )
!= A ) ),
inference(simp,[status(thm)],[15626]) ).
thf(2972,plain,
! [B: $i,A: $i] :
( ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) @ ( o @ pack1 ) )
!= ( A @ ( B @ pack1 ) ) )
| ( ( i @ ( B @ pack2 ) @ ( o @ ( o @ ( B @ unpack1 ) ) ) )
= B )
| ( A = o )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(paramod_ordered,[status(thm)],[2895,220]) ).
thf(2973,plain,
( ( ( i @ ( o @ pack2 ) @ ( o @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[2972:[bind(A,$thf( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )),bind(B,$thf( o ))]]) ).
thf(3100,plain,
( ( ( i @ ( o @ pack2 ) @ ( o @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[2973]) ).
thf(3669,plain,
( ( o != o )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
!= ( i @ ( o @ pack2 ) @ ( o @ ( o @ ( o @ unpack1 ) ) ) ) )
| ( ( i @ ( o @ pack2 ) @ ( o @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(eqfactor_ordered,[status(thm)],[3100]) ).
thf(3686,plain,
( ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
!= ( i @ ( o @ pack2 ) @ ( o @ ( o @ ( o @ unpack1 ) ) ) ) )
| ( ( i @ ( o @ pack2 ) @ ( o @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[3669]) ).
thf(516,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ inv @ ( B @ ( A @ unpack2 ) ) ) )
!= ( i @ ( C @ pack2 ) @ ( i @ ( C @ pack1 ) @ ( o @ ( C @ unpack2 ) ) ) ) )
| ( B = i ) ),
inference(paramod_ordered,[status(thm)],[36,438]) ).
thf(546,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) )
!= ( i @ ( C @ pack2 ) ) )
| ( ( B @ ( A @ pack1 ) @ inv )
!= ( i @ ( C @ pack1 ) ) )
| ( B != o )
| ( A != C )
| ( B = i ) ),
inference(simp,[status(thm)],[516]) ).
thf(549,plain,
! [A: $i] :
( ( ( i @ ( A @ pack2 ) )
!= ( o @ ( A @ pack2 ) ) )
| ( ( i @ ( A @ pack1 ) )
!= ( o @ ( A @ pack1 ) @ inv ) )
| ( i = o ) ),
inference(simp,[status(thm)],[546]) ).
thf(68691,plain,
! [A: $i] :
( ( ( i @ ( A @ pack2 ) )
!= ( o @ ( A @ pack2 ) ) )
| ( ( i @ ( A @ pack1 ) )
!= ( o @ ( A @ pack1 ) @ inv ) ) ),
inference(simplifyReflect,[status(thm)],[549,116]) ).
thf(905,plain,
! [A: $i] :
( ( A
!= ( o @ ( i @ pack1 ) ) )
| ( ( o @ ( i @ pack2 ) )
!= ( i @ ( o @ pack2 ) ) )
| ( ( i @ ( o @ pack1 ) )
!= i )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,901]) ).
thf(906,plain,
( ( ( o @ ( i @ pack2 ) )
!= ( i @ ( o @ pack2 ) ) )
| ( ( i @ ( o @ pack1 ) )
!= i )
| ( ( o @ ( i @ pack1 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[905:[bind(A,$thf( o @ ( i @ pack1 ) ))]]) ).
thf(533,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ inv @ ( A @ unpack2 ) ) ) )
!= ( D @ ( C @ pack2 ) @ ( D @ ( C @ pack1 ) @ inv @ ( D @ ( C @ unpack2 ) ) ) ) )
| ( B = D ) ),
inference(paramod_ordered,[status(thm)],[34,36]) ).
thf(536,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) )
!= ( D @ ( C @ pack2 ) ) )
| ( ( B @ ( A @ pack1 ) )
!= ( D @ ( C @ pack1 ) @ inv ) )
| ( ( B @ inv )
!= D )
| ( A != C )
| ( B = D ) ),
inference(simp,[status(thm)],[533]) ).
thf(555,plain,
! [B: $i,A: $i] :
( ( ( A @ inv @ ( B @ pack2 ) )
!= ( A @ ( B @ pack2 ) ) )
| ( ( A @ ( B @ pack1 ) )
!= ( A @ inv @ ( B @ pack1 ) @ inv ) )
| ( ( A @ inv )
= A ) ),
inference(simp,[status(thm)],[536]) ).
thf(75648,plain,
! [B: $i,A: $i] :
( ( ( A @ inv @ ( B @ pack2 ) )
!= ( A @ ( B @ pack2 ) ) )
| ( ( A @ ( B @ pack1 ) )
!= ( A @ inv @ ( B @ pack1 ) @ inv ) ) ),
inference(simplifyReflect,[status(thm)],[555,18]) ).
thf(75650,plain,
! [B: $i,A: $i] :
( ( ( o @ inv )
!= ( A @ inv ) )
| ( ( A @ inv @ ( B @ pack2 ) )
!= ( A @ ( B @ pack2 ) ) )
| ( ( i @ ( B @ pack1 ) @ inv )
!= ( A @ ( B @ pack1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[31674,75648]) ).
thf(75651,plain,
! [A: $i] :
( ( ( o @ inv @ ( A @ pack2 ) )
!= ( o @ ( A @ pack2 ) ) )
| ( ( i @ ( A @ pack1 ) @ inv )
!= ( o @ ( A @ pack1 ) ) ) ),
inference(pattern_uni,[status(thm)],[75650:[bind(A,$thf( o ))]]) ).
thf(75951,plain,
! [A: $i] :
( ( ( o @ inv @ ( A @ pack2 ) )
!= ( o @ ( A @ pack2 ) ) )
| ( ( i @ ( A @ pack1 ) @ inv )
!= ( o @ ( A @ pack1 ) ) ) ),
inference(simp,[status(thm)],[75651]) ).
thf(108988,plain,
! [A: $i] :
( ( ( i @ ( A @ pack2 ) )
!= ( o @ ( A @ pack2 ) ) )
| ( ( i @ ( A @ pack1 ) @ inv )
!= ( o @ ( A @ pack1 ) ) ) ),
inference(rewrite,[status(thm)],[75951,31674]) ).
thf(870,plain,
! [C: $i,B: $i,A: $i] :
( ( ( i @ ( i @ ( A @ pack1 ) @ ( o @ ( A @ unpack2 ) ) ) )
!= ( C @ ( B @ pack2 ) @ ( C @ ( B @ pack1 ) @ inv @ ( C @ ( B @ unpack2 ) ) ) ) )
| ( i = C )
| ( ( i @ ( A @ pack2 ) )
= o ) ),
inference(paramod_ordered,[status(thm)],[513,36]) ).
thf(874,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ pack2 ) )
!= i )
| ( ( i @ ( A @ pack1 ) )
!= ( C @ ( B @ pack1 ) @ inv ) )
| ( o != C )
| ( A != B )
| ( i = C )
| ( ( i @ ( A @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[870]) ).
thf(886,plain,
! [A: $i] :
( ( ( o @ ( A @ pack2 ) )
!= i )
| ( ( i @ ( A @ pack1 ) )
!= ( o @ ( A @ pack1 ) @ inv ) )
| ( i = o )
| ( ( i @ ( A @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[874]) ).
thf(140773,plain,
! [A: $i] :
( ( ( o @ ( A @ pack2 ) )
!= i )
| ( ( i @ ( A @ pack1 ) )
!= ( o @ ( A @ pack1 ) @ inv ) )
| ( ( i @ ( A @ pack2 ) )
= o ) ),
inference(simplifyReflect,[status(thm)],[886,116]) ).
thf(29650,plain,
! [B: $i,A: $i] :
( ( A
!= ( i @ ( o @ pack2 ) @ ( o @ inv @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) ) )
| ( B = o )
| ( ( A @ inv )
!= o )
| ( B = o ) ),
inference(paramod_ordered,[status(thm)],[10777,13128]) ).
thf(29651,plain,
! [B: $i,A: $i] :
( ( A
!= ( i @ ( o @ pack2 ) @ ( o @ inv @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) ) )
| ( ( A @ inv )
!= o )
| ( B = o ) ),
inference(simp,[status(thm)],[29650]) ).
thf(29652,plain,
! [A: $i] :
( ( ( i @ ( o @ pack2 ) @ ( o @ inv @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) @ inv )
!= o )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[29651:[bind(A,$thf( i @ ( o @ pack2 ) @ ( o @ inv @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )),bind(B,$thf( B ))]]) ).
thf(30860,plain,
! [A: $i] :
( ( ( i @ ( o @ pack2 ) @ ( o @ inv @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) @ inv )
!= o )
| ( A = o ) ),
inference(simp,[status(thm)],[29652]) ).
thf(35786,plain,
! [A: $i] :
( ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) @ inv )
!= o )
| ( A = o ) ),
inference(rewrite,[status(thm)],[30860,31674]) ).
thf(36627,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ inv ) )
| ( o != B )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) @ inv )
!= o ) ),
inference(paramod_ordered,[status(thm)],[35786,18]) ).
thf(36628,plain,
! [A: $i] :
( ( o != A )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) @ inv )
!= o ) ),
inference(pattern_uni,[status(thm)],[36627:[bind(A,$thf( C @ inv )),bind(B,$thf( C ))]]) ).
thf(37344,plain,
( ( i @ ( o @ pack2 ) @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) @ inv )
!= o ),
inference(simp,[status(thm)],[36628]) ).
thf(37418,plain,
( ( o @ inv )
!= o ),
inference(rewrite,[status(thm)],[37344,139]) ).
thf(32410,plain,
! [B: $i,A: $i] :
( ( ( o @ inv )
!= ( A @ inv ) )
| ( ( B @ ( A @ inv @ pack2 ) )
!= ( B @ ( A @ pack2 ) ) )
| ( ( B @ ( i @ pack1 ) @ inv )
!= ( B @ ( A @ pack1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[31674,26473]) ).
thf(32411,plain,
! [A: $i] :
( ( ( A @ ( o @ inv @ pack2 ) )
!= ( A @ ( o @ pack2 ) ) )
| ( ( A @ ( i @ pack1 ) @ inv )
!= ( A @ ( o @ pack1 ) ) ) ),
inference(pattern_uni,[status(thm)],[32410:[bind(A,$thf( o ))]]) ).
thf(32501,plain,
! [A: $i] :
( ( ( A @ ( o @ inv @ pack2 ) )
!= ( A @ ( o @ pack2 ) ) )
| ( ( A @ ( i @ pack1 ) @ inv )
!= ( A @ ( o @ pack1 ) ) ) ),
inference(simp,[status(thm)],[32411]) ).
thf(108012,plain,
! [A: $i] :
( ( ( A @ ( i @ pack2 ) )
!= ( A @ ( o @ pack2 ) ) )
| ( ( A @ ( i @ pack1 ) @ inv )
!= ( A @ ( o @ pack1 ) ) ) ),
inference(rewrite,[status(thm)],[32501,31674]) ).
thf(22398,plain,
! [A: $i] :
( ( ( o @ inv )
!= ( o @ inv ) )
| ( ( A @ ( o @ pack2 ) @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[9477,22181]) ).
thf(22399,plain,
! [A: $i] :
( ( ( A @ ( o @ pack2 ) @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[22398:[]]) ).
thf(41099,plain,
! [A: $i] :
( ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) @ ( o @ pack2 ) )
!= ( A @ ( o @ pack2 ) ) )
| ( ( o @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( A = o )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(paramod_ordered,[status(thm)],[21932,22399]) ).
thf(41100,plain,
( ( ( o @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[41099:[bind(A,$thf( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) ))]]) ).
thf(41467,plain,
( ( ( o @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[41100]) ).
thf(576,plain,
! [B: $i,A: $i] :
( ( i != i )
| ( ( B @ ( A @ pack2 ) )
!= ( B @ ( o @ pack2 ) ) )
| ( ( B @ ( i @ pack1 ) )
!= ( B @ ( o @ pack1 ) ) )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,562]) ).
thf(577,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) )
!= ( B @ ( o @ pack2 ) ) )
| ( ( B @ ( i @ pack1 ) )
!= ( B @ ( o @ pack1 ) ) )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[576:[]]) ).
thf(96301,plain,
! [B: $i,A: $i] :
( ( B
!= ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) ) )
| ( A
!= ( o @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) ) )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( A @ inv )
= i )
| ( B = o ) ),
inference(paramod_ordered,[status(thm)],[32386,56806]) ).
thf(96302,plain,
! [A: $i] :
( ( A
!= ( o @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) ) )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( A @ inv )
= i )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[96301:[bind(A,$thf( A )),bind(B,$thf( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) ))]]) ).
thf(97785,plain,
( ( ( o @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) @ inv )
= i )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[96302]) ).
thf(39492,plain,
! [B: $i,A: $i] :
( ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) @ ( o @ pack1 ) )
!= ( A @ ( B @ pack1 ) ) )
| ( ( A @ ( B @ pack2 ) @ ( o @ ( o @ ( B @ unpack1 ) ) ) )
= B )
| ( A = o )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(paramod_ordered,[status(thm)],[2895,347]) ).
thf(39493,plain,
( ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) @ ( o @ pack2 ) @ ( o @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[39492:[bind(A,$thf( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )),bind(B,$thf( o ))]]) ).
thf(39718,plain,
( ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) @ ( o @ pack2 ) @ ( o @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[39493]) ).
thf(180,plain,
! [B: $i,A: $i] :
( ( i != i )
| ( ( B @ ( i @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( o @ unpack1 ) ) ) )
= i )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,128]) ).
thf(181,plain,
! [B: $i,A: $i] :
( ( ( B @ ( i @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( o @ unpack1 ) ) ) )
= i )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[180:[]]) ).
thf(31902,plain,
! [C: $i,B: $i,A: $i] :
( ( ( o @ inv )
!= ( B @ inv ) )
| ( ( C @ ( B @ pack2 ) @ ( C @ ( B @ pack1 ) @ ( C @ ( A @ unpack1 ) ) ) )
= B )
| ( ( A @ inv )
!= o ) ),
inference(paramod_ordered,[status(thm)],[26968,22]) ).
thf(31903,plain,
! [B: $i,A: $i] :
( ( ( B @ ( o @ pack2 ) @ ( B @ ( o @ pack1 ) @ ( B @ ( A @ unpack1 ) ) ) )
= o )
| ( ( A @ inv )
!= o ) ),
inference(pattern_uni,[status(thm)],[31902:[bind(A,$thf( A )),bind(B,$thf( o ))]]) ).
thf(32299,plain,
! [B: $i,A: $i] :
( ( ( B @ ( o @ pack2 ) @ ( B @ ( o @ pack1 ) @ ( B @ ( A @ unpack1 ) ) ) )
= o )
| ( ( A @ inv )
!= o ) ),
inference(simp,[status(thm)],[31903]) ).
thf(135015,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ inv @ inv )
!= ( B @ inv ) )
| ( ( C @ ( o @ pack2 ) @ ( C @ ( o @ pack1 ) @ ( C @ ( B @ unpack1 ) ) ) )
= o )
| ( o != o )
| ( A = i ) ),
inference(paramod_ordered,[status(thm)],[129481,32299]) ).
thf(135016,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ inv @ inv )
!= ( B @ inv ) )
| ( ( C @ ( o @ pack2 ) @ ( C @ ( o @ pack1 ) @ ( C @ ( B @ unpack1 ) ) ) )
= o )
| ( A = i ) ),
inference(simp,[status(thm)],[135015]) ).
thf(135017,plain,
! [B: $i,A: $i] :
( ( ( A @ ( o @ pack2 ) @ ( A @ ( o @ pack1 ) @ ( A @ ( B @ inv @ unpack1 ) ) ) )
= o )
| ( B = i ) ),
inference(pattern_uni,[status(thm)],[135016:[bind(A,$thf( D )),bind(B,$thf( D @ inv ))]]) ).
thf(135700,plain,
! [B: $i,A: $i] :
( ( ( A @ ( o @ pack2 ) @ ( A @ ( o @ pack1 ) @ ( A @ ( B @ inv @ unpack1 ) ) ) )
= o )
| ( B = i ) ),
inference(simp,[status(thm)],[135017]) ).
thf(255,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ pack1 ) @ inv ) )
| ( ( C @ ( B @ pack2 ) @ ( i @ ( C @ ( B @ unpack1 ) ) ) )
= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,26]) ).
thf(256,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( i @ ( B @ ( A @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack1 ) @ inv )
= o ) ),
inference(pattern_uni,[status(thm)],[255:[bind(A,$thf( F @ ( E @ pack1 ) @ inv )),bind(B,$thf( E )),bind(C,$thf( F ))]]) ).
thf(274,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( i @ ( B @ ( A @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack1 ) @ inv )
= o ) ),
inference(simp,[status(thm)],[256]) ).
thf(997,plain,
! [B: $i,A: $i] :
( ( A != o )
| ( ( B @ inv )
!= i )
| ( ( i @ ( o @ pack2 ) )
!= o )
| ( ( o @ ( i @ pack1 ) )
!= ( i @ ( o @ pack1 ) ) )
| ( ( A @ ( B @ pack2 ) )
!= i )
| ( A != A )
| ( ( B @ inv )
!= B ) ),
inference(simp,[status(thm)],[929]) ).
thf(1048,plain,
! [A: $i] :
( ( ( A @ inv )
!= i )
| ( ( i @ ( o @ pack2 ) )
!= o )
| ( ( o @ ( i @ pack1 ) )
!= ( i @ ( o @ pack1 ) ) )
| ( ( o @ ( A @ pack2 ) )
!= i )
| ( ( A @ inv )
!= A ) ),
inference(simp,[status(thm)],[997]) ).
thf(292,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ inv )
!= ( i @ inv ) )
| ( ( o @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack1 ) ) ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[97,28]) ).
thf(318,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) )
!= i )
| ( ( o @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack1 ) ) ) )
= A ) ),
inference(simp,[status(thm)],[292]) ).
thf(493,plain,
! [C: $i,B: $i,A: $i] :
( ( ( i @ ( A @ pack2 ) @ ( i @ ( A @ pack1 ) @ ( o @ ( A @ unpack2 ) ) ) )
!= ( C @ ( B @ pack2 ) @ ( C @ ( B @ pack1 ) @ ( C @ inv @ ( B @ unpack2 ) ) ) ) )
| ( i = C ) ),
inference(paramod_ordered,[status(thm)],[438,34]) ).
thf(499,plain,
! [C: $i,B: $i,A: $i] :
( ( ( i @ ( A @ pack2 ) )
!= ( C @ ( B @ pack2 ) ) )
| ( ( i @ ( A @ pack1 ) )
!= ( C @ ( B @ pack1 ) ) )
| ( ( C @ inv )
!= o )
| ( A != B )
| ( i = C ) ),
inference(simp,[status(thm)],[493]) ).
thf(509,plain,
! [B: $i,A: $i] :
( ( ( i @ ( A @ pack2 ) )
!= ( B @ ( A @ pack2 ) ) )
| ( ( i @ ( A @ pack1 ) )
!= ( B @ ( A @ pack1 ) ) )
| ( ( B @ inv )
!= o )
| ( i = B ) ),
inference(simp,[status(thm)],[499]) ).
thf(598,plain,
! [C: $i,B: $i,A: $i] :
( ( ( i @ ( A @ pack2 ) @ ( i @ ( A @ pack1 ) @ ( o @ ( A @ unpack2 ) ) ) )
!= ( C @ ( B @ pack2 ) @ inv @ ( C @ ( B @ pack1 ) @ ( C @ ( B @ unpack2 ) ) ) ) )
| ( i = C ) ),
inference(paramod_ordered,[status(thm)],[438,38]) ).
thf(619,plain,
! [C: $i,B: $i,A: $i] :
( ( ( i @ ( A @ pack2 ) )
!= ( C @ ( B @ pack2 ) @ inv ) )
| ( ( i @ ( A @ pack1 ) )
!= ( C @ ( B @ pack1 ) ) )
| ( o != C )
| ( A != B )
| ( i = C ) ),
inference(simp,[status(thm)],[598]) ).
thf(633,plain,
! [A: $i] :
( ( ( i @ ( A @ pack2 ) )
!= ( o @ ( A @ pack2 ) @ inv ) )
| ( ( i @ ( A @ pack1 ) )
!= ( o @ ( A @ pack1 ) ) )
| ( i = o ) ),
inference(simp,[status(thm)],[619]) ).
thf(89418,plain,
! [A: $i] :
( ( ( i @ ( A @ pack2 ) )
!= ( o @ ( A @ pack2 ) @ inv ) )
| ( ( i @ ( A @ pack1 ) )
!= ( o @ ( A @ pack1 ) ) ) ),
inference(simplifyReflect,[status(thm)],[633,116]) ).
thf(358,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ inv )
!= ( B @ inv ) )
| ( ( C @ ( o @ pack2 ) )
!= ( C @ ( B @ pack2 ) ) )
| ( ( C @ ( B @ inv @ pack1 ) )
!= ( C @ ( B @ pack1 ) ) )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[126,45]) ).
thf(359,plain,
! [B: $i,A: $i] :
( ( ( B @ ( o @ pack2 ) )
!= ( B @ ( A @ pack2 ) ) )
| ( ( B @ ( A @ inv @ pack1 ) )
!= ( B @ ( A @ pack1 ) ) )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[358:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(377,plain,
! [B: $i,A: $i] :
( ( ( B @ ( o @ pack2 ) )
!= ( B @ ( A @ pack2 ) ) )
| ( ( B @ ( A @ inv @ pack1 ) )
!= ( B @ ( A @ pack1 ) ) )
| ( A = o ) ),
inference(simp,[status(thm)],[359]) ).
thf(32422,plain,
! [B: $i,A: $i] :
( ( ( o @ inv )
!= ( A @ inv ) )
| ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( i @ unpack1 ) ) ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[31674,22]) ).
thf(32423,plain,
! [A: $i] :
( ( A @ ( o @ pack2 ) @ ( A @ ( o @ pack1 ) @ ( A @ ( i @ unpack1 ) ) ) )
= o ),
inference(pattern_uni,[status(thm)],[32422:[bind(A,$thf( o ))]]) ).
thf(32505,plain,
! [A: $i] :
( ( A @ ( o @ pack2 ) @ ( A @ ( o @ pack1 ) @ ( A @ ( i @ unpack1 ) ) ) )
= o ),
inference(simp,[status(thm)],[32423]) ).
thf(10218,plain,
! [C: $i,B: $i,A: $i] :
( ( ( o @ inv )
!= ( C @ inv ) )
| ( ( C @ ( B @ pack2 ) @ ( C @ ( B @ pack1 ) @ ( A @ ( B @ unpack2 ) ) ) )
= C )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[9477,34]) ).
thf(10219,plain,
! [B: $i,A: $i] :
( ( ( o @ ( B @ pack2 ) @ ( o @ ( B @ pack1 ) @ ( A @ ( B @ unpack2 ) ) ) )
= o )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[10218:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( o ))]]) ).
thf(31679,plain,
! [C: $i,B: $i,A: $i] :
( ( A != o )
| ( ( C @ inv )
!= o )
| ( ( o @ inv )
= C )
| ( A = B )
| ( B = o ) ),
inference(paramod_ordered,[status(thm)],[5270,26968]) ).
thf(31680,plain,
! [B: $i,A: $i] :
( ( ( B @ inv )
!= o )
| ( ( o @ inv )
= B )
| ( o = A )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[31679:[bind(A,$thf( o ))]]) ).
thf(32303,plain,
! [B: $i,A: $i] :
( ( ( B @ inv )
!= o )
| ( ( o @ inv )
= B )
| ( A = o ) ),
inference(simp,[status(thm)],[31680]) ).
thf(62611,plain,
! [B: $i,A: $i] :
( ( ( B @ inv )
!= o )
| ( i = B )
| ( A = o ) ),
inference(rewrite,[status(thm)],[32303,31674]) ).
thf(63534,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ inv ) )
| ( o != o )
| ( C = i )
| ( ( B @ inv )
!= o )
| ( i = B ) ),
inference(paramod_ordered,[status(thm)],[62611,32346]) ).
thf(63535,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ inv ) )
| ( C = i )
| ( ( B @ inv )
!= o )
| ( i = B ) ),
inference(simp,[status(thm)],[63534]) ).
thf(63536,plain,
! [B: $i,A: $i] :
( ( B = i )
| ( ( A @ inv )
!= o )
| ( i = A ) ),
inference(pattern_uni,[status(thm)],[63535:[bind(A,$thf( D @ inv )),bind(B,$thf( B )),bind(C,$thf( D ))]]) ).
thf(64392,plain,
! [B: $i,A: $i] :
( ( B = i )
| ( ( A @ inv )
!= o )
| ( i = A ) ),
inference(simp,[status(thm)],[63536]) ).
thf(449,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ pack2 ) ) )
| ( ( i @ ( C @ ( B @ pack1 ) @ ( C @ inv @ ( B @ unpack2 ) ) ) )
= C )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,34]) ).
thf(450,plain,
! [B: $i,A: $i] :
( ( ( i @ ( B @ ( A @ pack1 ) @ ( B @ inv @ ( A @ unpack2 ) ) ) )
= B )
| ( ( B @ ( A @ pack2 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[449:[bind(A,$thf( E @ ( D @ pack2 ) )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(462,plain,
! [B: $i,A: $i] :
( ( ( i @ ( B @ ( A @ pack1 ) @ ( B @ inv @ ( A @ unpack2 ) ) ) )
= B )
| ( ( B @ ( A @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[450]) ).
thf(93257,plain,
! [B: $i,A: $i] :
( ( B
!= ( o @ inv ) )
| ( o != o )
| ( ( A @ inv )
= i )
| ( A = B ) ),
inference(paramod_ordered,[status(thm)],[32386,37418]) ).
thf(93258,plain,
! [B: $i,A: $i] :
( ( B
!= ( o @ inv ) )
| ( ( A @ inv )
= i )
| ( A = B ) ),
inference(simp,[status(thm)],[93257]) ).
thf(93259,plain,
! [A: $i] :
( ( ( A @ inv )
= i )
| ( A
= ( o @ inv ) ) ),
inference(pattern_uni,[status(thm)],[93258:[bind(A,$thf( A )),bind(B,$thf( o @ inv ))]]) ).
thf(98477,plain,
! [A: $i] :
( ( ( A @ inv )
= i )
| ( A = i ) ),
inference(rewrite,[status(thm)],[93259,31674]) ).
thf(86,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ pack1 ) ) )
| ( ( C @ ( B @ pack2 ) @ ( i @ ( C @ ( B @ unpack2 ) ) ) )
= C )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,30]) ).
thf(87,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( i @ ( B @ ( A @ unpack2 ) ) ) )
= B )
| ( ( B @ ( A @ pack1 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[86:[bind(A,$thf( E @ ( D @ pack1 ) )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(103,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( i @ ( B @ ( A @ unpack2 ) ) ) )
= B )
| ( ( B @ ( A @ pack1 ) )
= o ) ),
inference(simp,[status(thm)],[87]) ).
thf(667,plain,
! [B: $i,A: $i] :
( ( i != i )
| ( ( B @ ( i @ pack2 ) @ ( A @ ( B @ ( o @ unpack1 ) ) ) )
= i )
| ( ( B @ ( i @ pack1 ) )
= o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,190]) ).
thf(668,plain,
! [B: $i,A: $i] :
( ( ( B @ ( i @ pack2 ) @ ( A @ ( B @ ( o @ unpack1 ) ) ) )
= i )
| ( ( B @ ( i @ pack1 ) )
= o )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[667:[]]) ).
thf(146,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ pack1 ) ) )
| ( ( C @ ( B @ pack2 ) @ ( i @ ( C @ inv @ ( B @ unpack1 ) ) ) )
= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,24]) ).
thf(147,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( i @ ( B @ inv @ ( A @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack1 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[146:[bind(A,$thf( E @ ( D @ pack1 ) )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(155,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( i @ ( B @ inv @ ( A @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack1 ) )
= o ) ),
inference(simp,[status(thm)],[147]) ).
thf(32360,plain,
! [B: $i,A: $i] :
( ( ( o @ inv )
!= ( B @ inv ) )
| ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( i @ ( A @ unpack1 ) ) ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[31674,24]) ).
thf(32361,plain,
! [A: $i] :
( ( o @ ( A @ pack2 ) @ ( o @ ( A @ pack1 ) @ ( i @ ( A @ unpack1 ) ) ) )
= A ),
inference(pattern_uni,[status(thm)],[32360:[bind(A,$thf( A )),bind(B,$thf( o ))]]) ).
thf(62,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( B @ inv ) )
| ( ( C @ ( B @ inv @ pack2 ) )
!= ( C @ ( B @ pack2 ) ) )
| ( ( C @ ( i @ pack1 ) )
!= ( C @ ( B @ pack1 ) ) )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,45]) ).
thf(63,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ inv @ pack2 ) )
!= ( A @ ( B @ pack2 ) ) )
| ( ( A @ ( i @ pack1 ) )
!= ( A @ ( B @ pack1 ) ) )
| ( ( B @ inv )
= o ) ),
inference(pattern_uni,[status(thm)],[62:[bind(A,$thf( D @ inv )),bind(B,$thf( D ))]]) ).
thf(108,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ inv @ pack2 ) )
!= ( A @ ( B @ pack2 ) ) )
| ( ( A @ ( i @ pack1 ) )
!= ( A @ ( B @ pack1 ) ) )
| ( ( B @ inv )
= o ) ),
inference(simp,[status(thm)],[63]) ).
thf(389,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( B @ inv ) )
| ( ( C @ ( B @ pack2 ) @ ( C @ ( B @ pack1 ) @ ( C @ ( i @ unpack2 ) ) ) )
= C )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,32]) ).
thf(390,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ pack2 ) @ ( A @ ( B @ pack1 ) @ ( A @ ( i @ unpack2 ) ) ) )
= A )
| ( ( B @ inv )
= o ) ),
inference(pattern_uni,[status(thm)],[389:[bind(A,$thf( D @ inv )),bind(B,$thf( D ))]]) ).
thf(399,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ pack2 ) @ ( A @ ( B @ pack1 ) @ ( A @ ( i @ unpack2 ) ) ) )
= A )
| ( ( B @ inv )
= o ) ),
inference(simp,[status(thm)],[390]) ).
thf(34151,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ ( o @ pack1 ) ) )
| ( ( B @ ( o @ pack2 ) @ ( i @ ( B @ ( i @ unpack2 ) ) ) )
= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[4511,32504]) ).
thf(34152,plain,
! [A: $i] :
( ( ( A @ ( o @ pack2 ) @ ( i @ ( A @ ( i @ unpack2 ) ) ) )
= A )
| ( ( A @ ( o @ pack1 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[34151:[bind(A,$thf( D @ ( o @ pack1 ) )),bind(B,$thf( D ))]]) ).
thf(34404,plain,
! [A: $i] :
( ( ( A @ ( o @ pack2 ) @ ( i @ ( A @ ( i @ unpack2 ) ) ) )
= A )
| ( ( A @ ( o @ pack1 ) )
= o ) ),
inference(simp,[status(thm)],[34152]) ).
thf(60849,plain,
! [B: $i,A: $i] :
( ( ( A @ inv @ ( B @ pack2 ) )
!= ( A @ ( B @ pack2 ) ) )
| ( ( A @ inv )
!= A )
| ( B != B ) ),
inference(simp,[status(thm)],[60848]) ).
thf(61020,plain,
! [B: $i,A: $i] :
( ( ( A @ inv @ ( B @ pack2 ) )
!= ( A @ ( B @ pack2 ) ) )
| ( ( A @ inv )
!= A ) ),
inference(simp,[status(thm)],[60849]) ).
thf(63526,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A
!= ( D @ ( C @ pack2 ) @ ( D @ ( C @ pack1 ) @ ( D @ ( C @ inv @ unpack1 ) ) ) ) )
| ( o = C )
| ( ( B @ inv )
!= o )
| ( i = B ) ),
inference(paramod_ordered,[status(thm)],[62611,22]) ).
thf(63527,plain,
! [B: $i,A: $i] :
( ( o = B )
| ( ( A @ inv )
!= o )
| ( i = A ) ),
inference(pattern_uni,[status(thm)],[63526:[bind(A,$thf( M @ ( L @ pack2 ) @ ( M @ ( L @ pack1 ) @ ( M @ ( L @ inv @ unpack1 ) ) ) )),bind(B,$thf( B )),bind(C,$thf( L )),bind(D,$thf( M ))]]) ).
thf(64388,plain,
! [B: $i,A: $i] :
( ( o = B )
| ( ( A @ inv )
!= o )
| ( i = A ) ),
inference(simp,[status(thm)],[63527]) ).
thf(524,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ pack2 ) ) )
| ( ( i @ ( C @ ( B @ pack1 ) @ inv @ ( C @ ( B @ unpack2 ) ) ) )
= C )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,36]) ).
thf(525,plain,
! [B: $i,A: $i] :
( ( ( i @ ( B @ ( A @ pack1 ) @ inv @ ( B @ ( A @ unpack2 ) ) ) )
= B )
| ( ( B @ ( A @ pack2 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[524:[bind(A,$thf( E @ ( D @ pack2 ) )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(553,plain,
! [B: $i,A: $i] :
( ( ( i @ ( B @ ( A @ pack1 ) @ inv @ ( B @ ( A @ unpack2 ) ) ) )
= B )
| ( ( B @ ( A @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[525]) ).
thf(677,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( i @ pack2 ) @ ( i @ ( A @ ( o @ unpack1 ) ) ) )
!= ( C @ ( B @ pack2 ) @ ( C @ ( B @ pack1 ) @ inv @ ( C @ ( B @ unpack1 ) ) ) ) )
| ( i = B )
| ( ( A @ ( i @ pack1 ) )
= o ) ),
inference(paramod_ordered,[status(thm)],[190,26]) ).
thf(681,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( i @ pack2 ) )
!= ( C @ ( B @ pack2 ) ) )
| ( ( C @ ( B @ pack1 ) @ inv )
!= i )
| ( A != C )
| ( o != B )
| ( i = B )
| ( ( A @ ( i @ pack1 ) )
= o ) ),
inference(simp,[status(thm)],[677]) ).
thf(693,plain,
! [A: $i] :
( ( ( A @ ( i @ pack2 ) )
!= ( A @ ( o @ pack2 ) ) )
| ( ( A @ ( o @ pack1 ) @ inv )
!= i )
| ( i = o )
| ( ( A @ ( i @ pack1 ) )
= o ) ),
inference(simp,[status(thm)],[681]) ).
thf(105700,plain,
! [A: $i] :
( ( ( A @ ( i @ pack2 ) )
!= ( A @ ( o @ pack2 ) ) )
| ( ( A @ ( o @ pack1 ) @ inv )
!= i )
| ( ( A @ ( i @ pack1 ) )
= o ) ),
inference(simplifyReflect,[status(thm)],[693,116]) ).
thf(72,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ pack1 ) ) )
| ( ( C @ ( B @ pack2 ) @ ( i @ ( C @ ( B @ inv @ unpack1 ) ) ) )
= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,22]) ).
thf(73,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( i @ ( B @ ( A @ inv @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack1 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[72:[bind(A,$thf( E @ ( D @ pack1 ) )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(95,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( i @ ( B @ ( A @ inv @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack1 ) )
= o ) ),
inference(simp,[status(thm)],[73]) ).
thf(303,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ pack2 ) @ inv ) )
| ( ( i @ ( C @ ( B @ pack1 ) @ ( C @ ( B @ unpack1 ) ) ) )
= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,28]) ).
thf(304,plain,
! [B: $i,A: $i] :
( ( ( i @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack2 ) @ inv )
= o ) ),
inference(pattern_uni,[status(thm)],[303:[bind(A,$thf( F @ ( E @ pack2 ) @ inv )),bind(B,$thf( E )),bind(C,$thf( F ))]]) ).
thf(327,plain,
! [B: $i,A: $i] :
( ( ( i @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack2 ) @ inv )
= o ) ),
inference(simp,[status(thm)],[304]) ).
thf(56594,plain,
! [A: $i] :
( ( A
!= ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) ) )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( o @ ( i @ pack2 ) )
= o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,50011]) ).
thf(56595,plain,
( ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( o @ ( i @ pack2 ) )
= o )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[56594:[bind(A,$thf( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) ))]]) ).
thf(56820,plain,
( ( ( o @ ( i @ pack2 ) )
= o )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[56595]) ).
thf(46,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ inv @ pack2 ) )
!= ( B @ ( A @ pack2 ) ) )
| ( B != B )
| ( ( A @ inv )
!= A ) ),
inference(simp,[status(thm)],[45]) ).
thf(50,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ inv @ pack2 ) )
!= ( B @ ( A @ pack2 ) ) )
| ( ( A @ inv )
!= A ) ),
inference(simp,[status(thm)],[46]) ).
thf(44847,plain,
! [B: $i,A: $i] :
( ( B != o )
| ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( o @ unpack2 ) ) ) )
!= A )
| ( A = o ) ),
inference(eqfactor_ordered,[status(thm)],[397]) ).
thf(44863,plain,
! [A: $i] :
( ( ( o @ ( A @ pack2 ) @ ( o @ ( A @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
!= A )
| ( A = o ) ),
inference(simp,[status(thm)],[44847]) ).
thf(47,plain,
! [B: $i,A: $i] :
( ( B != B )
| ( ( A @ inv )
!= A )
| ( ( B @ ( A @ inv @ pack1 ) )
!= ( B @ ( A @ pack1 ) ) ) ),
inference(simp,[status(thm)],[45]) ).
thf(51,plain,
! [B: $i,A: $i] :
( ( ( A @ inv )
!= A )
| ( ( B @ ( A @ inv @ pack1 ) )
!= ( B @ ( A @ pack1 ) ) ) ),
inference(simp,[status(thm)],[47]) ).
thf(781,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( B @ inv ) )
| ( ( B @ inv )
!= B )
| ( ( C @ ( i @ pack1 ) )
!= ( C @ ( B @ pack1 ) ) )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,51]) ).
thf(782,plain,
! [B: $i,A: $i] :
( ( ( B @ inv )
!= B )
| ( ( A @ ( i @ pack1 ) )
!= ( A @ ( B @ pack1 ) ) )
| ( ( B @ inv )
= o ) ),
inference(pattern_uni,[status(thm)],[781:[bind(A,$thf( D @ inv )),bind(B,$thf( D ))]]) ).
thf(791,plain,
! [B: $i,A: $i] :
( ( ( B @ inv )
!= B )
| ( ( A @ ( i @ pack1 ) )
!= ( A @ ( B @ pack1 ) ) )
| ( ( B @ inv )
= o ) ),
inference(simp,[status(thm)],[782]) ).
thf(29097,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ inv ) )
| ( B != C )
| ( ( A @ inv )
!= o )
| ( B = o ) ),
inference(paramod_ordered,[status(thm)],[10777,18]) ).
thf(29098,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( ( B @ inv @ inv )
!= o )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[29097:[bind(A,$thf( D @ inv )),bind(B,$thf( B )),bind(C,$thf( D ))]]) ).
thf(30565,plain,
! [A: $i] :
( ( ( A @ inv @ inv )
!= o )
| ( A = o ) ),
inference(simp,[status(thm)],[29098]) ).
thf(34811,plain,
! [A: $i] :
( ( ( A @ inv @ inv )
!= ( i @ inv ) )
| ( o != o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[97,30565]) ).
thf(34812,plain,
! [A: $i] :
( ( ( A @ inv @ inv )
!= ( i @ inv ) )
| ( A = o ) ),
inference(simp,[status(thm)],[34811]) ).
thf(34856,plain,
! [A: $i] :
( ( ( A @ inv )
!= i )
| ( A = o ) ),
inference(simp,[status(thm)],[34812]) ).
thf(445,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ inv ) )
| ( ( C @ ( B @ pack2 ) @ ( C @ ( B @ pack1 ) @ ( i @ ( B @ unpack2 ) ) ) )
= C )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,34]) ).
thf(446,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( i @ ( A @ unpack2 ) ) ) )
= B )
| ( ( B @ inv )
= o ) ),
inference(pattern_uni,[status(thm)],[445:[bind(A,$thf( D @ inv )),bind(B,$thf( B )),bind(C,$thf( D ))]]) ).
thf(470,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( i @ ( A @ unpack2 ) ) ) )
= B )
| ( ( B @ inv )
= o ) ),
inference(simp,[status(thm)],[446]) ).
thf(613,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ inv @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack2 ) ) ) )
!= ( D @ ( C @ pack2 ) @ ( D @ ( C @ pack1 ) @ ( D @ inv @ ( C @ unpack2 ) ) ) ) )
| ( B = D ) ),
inference(paramod_ordered,[status(thm)],[38,34]) ).
thf(630,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ inv )
!= ( D @ ( C @ pack2 ) ) )
| ( ( B @ ( A @ pack1 ) )
!= ( D @ ( C @ pack1 ) ) )
| ( B
!= ( D @ inv ) )
| ( A != C )
| ( B = D ) ),
inference(simp,[status(thm)],[613]) ).
thf(643,plain,
! [B: $i,A: $i] :
( ( ( B @ inv @ ( A @ pack2 ) @ inv )
!= ( B @ ( A @ pack2 ) ) )
| ( ( B @ inv @ ( A @ pack1 ) )
!= ( B @ ( A @ pack1 ) ) )
| ( ( B @ inv )
= B ) ),
inference(simp,[status(thm)],[630]) ).
thf(10630,plain,
! [B: $i,A: $i] :
( ( ( o @ inv @ inv )
!= ( B @ inv ) )
| ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( o @ ( A @ unpack1 ) ) ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[10467,24]) ).
thf(10631,plain,
! [A: $i] :
( ( o @ inv @ ( A @ pack2 ) @ ( o @ inv @ ( A @ pack1 ) @ ( o @ ( A @ unpack1 ) ) ) )
= A ),
inference(pattern_uni,[status(thm)],[10630:[bind(A,$thf( A )),bind(B,$thf( o @ inv ))]]) ).
thf(11674,plain,
! [B: $i,A: $i] :
( ( A
!= ( o @ inv @ ( B @ pack2 ) @ ( o @ inv @ ( B @ pack1 ) @ ( o @ ( B @ unpack1 ) ) ) ) )
| ( i = B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,10631]) ).
thf(11675,plain,
! [A: $i] :
( ( i = A )
| ( ( o @ inv @ ( A @ pack2 ) @ ( o @ inv @ ( A @ pack1 ) @ ( o @ ( A @ unpack1 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[11674:[bind(A,$thf( o @ inv @ ( J @ pack2 ) @ ( o @ inv @ ( J @ pack1 ) @ ( o @ ( J @ unpack1 ) ) ) )),bind(B,$thf( J ))]]) ).
thf(11981,plain,
! [A: $i] :
( ( i = A )
| ( ( o @ inv @ ( A @ pack2 ) @ ( o @ inv @ ( A @ pack1 ) @ ( o @ ( A @ unpack1 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[11675]) ).
thf(106041,plain,
! [A: $i] :
( ( i = A )
| ( ( i @ ( A @ pack2 ) @ ( i @ ( A @ pack1 ) @ ( o @ ( A @ unpack1 ) ) ) )
= o ) ),
inference(rewrite,[status(thm)],[11981,31674]) ).
thf(144,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ inv ) )
| ( ( C @ ( B @ pack2 ) @ ( C @ ( B @ pack1 ) @ ( i @ ( B @ unpack1 ) ) ) )
= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,24]) ).
thf(145,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( i @ ( A @ unpack1 ) ) ) )
= A )
| ( ( B @ inv )
= o ) ),
inference(pattern_uni,[status(thm)],[144:[bind(A,$thf( D @ inv )),bind(B,$thf( B )),bind(C,$thf( D ))]]) ).
thf(154,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( i @ ( A @ unpack1 ) ) ) )
= A )
| ( ( B @ inv )
= o ) ),
inference(simp,[status(thm)],[145]) ).
thf(31887,plain,
! [C: $i,B: $i,A: $i] :
( ( ( o @ inv )
!= ( C @ inv ) )
| ( ( C @ ( B @ pack2 ) @ ( C @ ( B @ pack1 ) @ ( A @ ( B @ unpack2 ) ) ) )
= C )
| ( ( A @ inv )
!= o ) ),
inference(paramod_ordered,[status(thm)],[26968,34]) ).
thf(31888,plain,
! [B: $i,A: $i] :
( ( ( o @ ( B @ pack2 ) @ ( o @ ( B @ pack1 ) @ ( A @ ( B @ unpack2 ) ) ) )
= o )
| ( ( A @ inv )
!= o ) ),
inference(pattern_uni,[status(thm)],[31887:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( o ))]]) ).
thf(32401,plain,
! [B: $i,A: $i] :
( ( ( o @ inv )
!= ( B @ inv ) )
| ( ( i @ ( B @ ( A @ pack1 ) @ ( i @ ( A @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack2 ) )
= o ) ),
inference(paramod_ordered,[status(thm)],[31674,156]) ).
thf(32402,plain,
! [A: $i] :
( ( ( i @ ( o @ ( A @ pack1 ) @ ( i @ ( A @ unpack1 ) ) ) )
= A )
| ( ( o @ ( A @ pack2 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[32401:[bind(A,$thf( A )),bind(B,$thf( o ))]]) ).
thf(94342,plain,
! [C: $i,B: $i,A: $i] :
( ( B
!= ( C @ inv ) )
| ( A != C )
| ( ( A @ inv )
= i )
| ( B = o ) ),
inference(paramod_ordered,[status(thm)],[32386,18]) ).
thf(94343,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( ( A @ inv )
= i )
| ( ( B @ inv )
= o ) ),
inference(pattern_uni,[status(thm)],[94342:[bind(A,$thf( A )),bind(B,$thf( D @ inv )),bind(C,$thf( D ))]]) ).
thf(96586,plain,
! [A: $i] :
( ( ( A @ inv )
= i )
| ( ( A @ inv )
= o ) ),
inference(simp,[status(thm)],[94343]) ).
thf(858,plain,
! [B: $i,A: $i] :
( ( i != i )
| ( ( i @ ( A @ ( B @ pack1 ) @ ( o @ ( B @ unpack2 ) ) ) )
= i )
| ( ( i @ ( B @ pack2 ) )
= o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,513]) ).
thf(859,plain,
! [B: $i,A: $i] :
( ( ( i @ ( A @ ( B @ pack1 ) @ ( o @ ( B @ unpack2 ) ) ) )
= i )
| ( ( i @ ( B @ pack2 ) )
= o )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[858:[]]) ).
thf(729,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ inv @ ( A @ unpack1 ) ) ) )
!= ( i @ ( C @ ( i @ pack1 ) @ ( C @ ( o @ unpack1 ) ) ) ) )
| ( A = i )
| ( ( C @ ( i @ pack2 ) )
= o ) ),
inference(paramod_ordered,[status(thm)],[24,191]) ).
thf(745,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) )
!= i )
| ( ( B @ ( A @ pack1 ) )
!= ( C @ ( i @ pack1 ) ) )
| ( ( B @ inv )
!= C )
| ( A != o )
| ( A = i )
| ( ( C @ ( i @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[729]) ).
thf(757,plain,
! [A: $i] :
( ( ( A @ ( o @ pack2 ) )
!= i )
| ( ( A @ inv @ ( i @ pack1 ) )
!= ( A @ ( o @ pack1 ) ) )
| ( i = o )
| ( ( A @ inv @ ( i @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[745]) ).
thf(115052,plain,
! [A: $i] :
( ( ( A @ ( o @ pack2 ) )
!= i )
| ( ( A @ inv @ ( i @ pack1 ) )
!= ( A @ ( o @ pack1 ) ) )
| ( ( A @ inv @ ( i @ pack2 ) )
= o ) ),
inference(simplifyReflect,[status(thm)],[757,116]) ).
thf(726,plain,
! [B: $i,A: $i] :
( ( i != i )
| ( ( A @ ( B @ ( i @ pack1 ) @ ( B @ ( o @ unpack1 ) ) ) )
= i )
| ( ( B @ ( i @ pack2 ) )
= o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,191]) ).
thf(727,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( i @ pack1 ) @ ( B @ ( o @ unpack1 ) ) ) )
= i )
| ( ( B @ ( i @ pack2 ) )
= o )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[726:[]]) ).
thf(1938,plain,
( ( ( o @ ( i @ pack2 ) )
!= ( o @ ( i @ pack2 ) ) )
| ( ( i @ ( o @ pack2 ) )
!= o )
| ( ( o @ ( i @ pack1 ) )
!= ( i @ ( o @ pack1 ) ) )
| ( ( i @ ( o @ pack2 ) )
!= i )
| ( ( o @ ( i @ pack1 ) )
!= ( i @ ( o @ pack1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[911,901]) ).
thf(1939,plain,
( ( ( o @ ( i @ pack2 ) )
!= ( o @ ( i @ pack2 ) ) )
| ( ( i @ ( o @ pack2 ) )
!= o )
| ( ( i @ ( o @ pack2 ) )
!= i )
| ( ( o @ ( i @ pack1 ) )
!= ( i @ ( o @ pack1 ) ) ) ),
inference(simp,[status(thm)],[1938]) ).
thf(1940,plain,
( ( ( i @ ( o @ pack2 ) )
!= o )
| ( ( i @ ( o @ pack2 ) )
!= i )
| ( ( o @ ( i @ pack1 ) )
!= ( i @ ( o @ pack1 ) ) ) ),
inference(pattern_uni,[status(thm)],[1939:[]]) ).
thf(42392,plain,
( ( o != o )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
!= ( o @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) ) )
| ( ( o @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(eqfactor_ordered,[status(thm)],[41467]) ).
thf(42398,plain,
( ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
!= ( o @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) ) )
| ( ( o @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[42392]) ).
thf(80,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ inv @ pack2 ) ) )
| ( ( C @ ( B @ pack2 ) )
!= i )
| ( ( B @ inv )
!= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,50]) ).
thf(81,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ pack2 ) )
!= i )
| ( ( B @ inv )
!= B )
| ( ( A @ ( B @ inv @ pack2 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[80:[bind(A,$thf( E @ ( F @ inv @ pack2 ) )),bind(B,$thf( F )),bind(C,$thf( E ))]]) ).
thf(99,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ pack2 ) )
!= i )
| ( ( B @ inv )
!= B )
| ( ( A @ ( B @ inv @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[81]) ).
thf(32433,plain,
! [B: $i,A: $i] :
( ( ( o @ inv )
!= ( B @ inv ) )
| ( ( B @ ( A @ pack2 ) @ ( i @ ( i @ ( A @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack1 ) )
= o ) ),
inference(paramod_ordered,[status(thm)],[31674,155]) ).
thf(32434,plain,
! [A: $i] :
( ( ( o @ ( A @ pack2 ) @ ( i @ ( i @ ( A @ unpack1 ) ) ) )
= A )
| ( ( o @ ( A @ pack1 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[32433:[bind(A,$thf( A )),bind(B,$thf( o ))]]) ).
thf(566,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ ( i @ pack1 ) ) )
| ( ( B @ ( i @ pack2 ) )
!= ( B @ ( o @ pack2 ) ) )
| ( ( B @ ( o @ pack1 ) )
!= i )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,562]) ).
thf(567,plain,
! [A: $i] :
( ( ( A @ ( i @ pack2 ) )
!= ( A @ ( o @ pack2 ) ) )
| ( ( A @ ( o @ pack1 ) )
!= i )
| ( ( A @ ( i @ pack1 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[566:[bind(A,$thf( D @ ( i @ pack1 ) )),bind(B,$thf( D ))]]) ).
thf(581,plain,
! [A: $i] :
( ( ( A @ ( i @ pack2 ) )
!= ( A @ ( o @ pack2 ) ) )
| ( ( A @ ( o @ pack1 ) )
!= i )
| ( ( A @ ( i @ pack1 ) )
= o ) ),
inference(simp,[status(thm)],[567]) ).
thf(56,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ pack1 ) ) )
| ( ( C @ ( B @ pack2 ) @ ( i @ ( C @ ( B @ unpack1 ) ) ) )
= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,20]) ).
thf(57,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( i @ ( B @ ( A @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack1 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[56:[bind(A,$thf( E @ ( D @ pack1 ) )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(104,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( i @ ( B @ ( A @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack1 ) )
= o ) ),
inference(simp,[status(thm)],[57]) ).
thf(134223,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ inv @ inv )
!= ( B @ inv ) )
| ( ( o @ ( C @ pack2 ) @ ( o @ ( C @ pack1 ) @ ( B @ ( C @ unpack2 ) ) ) )
= o )
| ( o != o )
| ( A = i ) ),
inference(paramod_ordered,[status(thm)],[129481,31888]) ).
thf(134224,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ inv @ inv )
!= ( B @ inv ) )
| ( ( o @ ( C @ pack2 ) @ ( o @ ( C @ pack1 ) @ ( B @ ( C @ unpack2 ) ) ) )
= o )
| ( A = i ) ),
inference(simp,[status(thm)],[134223]) ).
thf(134225,plain,
! [B: $i,A: $i] :
( ( ( o @ ( A @ pack2 ) @ ( o @ ( A @ pack1 ) @ ( B @ inv @ ( A @ unpack2 ) ) ) )
= o )
| ( B = i ) ),
inference(pattern_uni,[status(thm)],[134224:[bind(A,$thf( D )),bind(B,$thf( D @ inv ))]]) ).
thf(134837,plain,
! [B: $i,A: $i] :
( ( ( o @ ( A @ pack2 ) @ ( o @ ( A @ pack1 ) @ ( B @ inv @ ( A @ unpack2 ) ) ) )
= o )
| ( B = i ) ),
inference(simp,[status(thm)],[134225]) ).
thf(453,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ inv @ ( A @ unpack2 ) ) ) )
!= ( D @ ( C @ pack2 ) @ ( D @ ( C @ pack1 ) @ ( D @ ( C @ inv @ unpack2 ) ) ) ) )
| ( B = D ) ),
inference(paramod_ordered,[status(thm)],[34,32]) ).
thf(456,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) )
!= ( D @ ( C @ pack2 ) ) )
| ( ( B @ ( A @ pack1 ) )
!= ( D @ ( C @ pack1 ) ) )
| ( ( B @ inv )
!= D )
| ( A
!= ( C @ inv ) )
| ( B = D ) ),
inference(simp,[status(thm)],[453]) ).
thf(464,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ inv @ pack2 ) )
!= ( A @ inv @ ( B @ pack2 ) ) )
| ( ( A @ ( B @ inv @ pack1 ) )
!= ( A @ inv @ ( B @ pack1 ) ) )
| ( ( A @ inv )
= A ) ),
inference(simp,[status(thm)],[456]) ).
thf(58879,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ inv @ pack2 ) )
!= ( A @ inv @ ( B @ pack2 ) ) )
| ( ( A @ ( B @ inv @ pack1 ) )
!= ( A @ inv @ ( B @ pack1 ) ) ) ),
inference(simplifyReflect,[status(thm)],[464,18]) ).
thf(32439,plain,
! [B: $i,A: $i] :
( ( ( o @ inv )
!= ( A @ inv ) )
| ( ( B @ ( A @ pack2 ) @ ( i @ ( B @ ( i @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack1 ) )
= o ) ),
inference(paramod_ordered,[status(thm)],[31674,95]) ).
thf(32440,plain,
! [A: $i] :
( ( ( A @ ( o @ pack2 ) @ ( i @ ( A @ ( i @ unpack1 ) ) ) )
= o )
| ( ( A @ ( o @ pack1 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[32439:[bind(A,$thf( o ))]]) ).
thf(32506,plain,
! [A: $i] :
( ( ( A @ ( o @ pack2 ) @ ( i @ ( A @ ( i @ unpack1 ) ) ) )
= o )
| ( ( A @ ( o @ pack1 ) )
= o ) ),
inference(simp,[status(thm)],[32440]) ).
thf(98718,plain,
! [A: $i] :
( ( i != i )
| ( ( A @ inv )
!= A )
| ( A = i ) ),
inference(eqfactor_ordered,[status(thm)],[98477]) ).
thf(98719,plain,
! [A: $i] :
( ( ( A @ inv )
!= A )
| ( A = i ) ),
inference(simp,[status(thm)],[98718]) ).
thf(34153,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ ( o @ pack2 ) ) )
| ( ( i @ ( B @ ( o @ pack1 ) @ ( B @ ( i @ unpack2 ) ) ) )
= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[4511,32504]) ).
thf(34154,plain,
! [A: $i] :
( ( ( i @ ( A @ ( o @ pack1 ) @ ( A @ ( i @ unpack2 ) ) ) )
= A )
| ( ( A @ ( o @ pack2 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[34153:[bind(A,$thf( D @ ( o @ pack2 ) )),bind(B,$thf( D ))]]) ).
thf(34405,plain,
! [A: $i] :
( ( ( i @ ( A @ ( o @ pack1 ) @ ( A @ ( i @ unpack2 ) ) ) )
= A )
| ( ( A @ ( o @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[34154]) ).
thf(299,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ pack2 ) ) )
| ( ( i @ inv @ ( C @ ( B @ pack1 ) @ ( C @ ( B @ unpack1 ) ) ) )
= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,28]) ).
thf(300,plain,
! [B: $i,A: $i] :
( ( ( i @ inv @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack2 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[299:[bind(A,$thf( E @ ( D @ pack2 ) )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(325,plain,
! [B: $i,A: $i] :
( ( ( i @ inv @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[300]) ).
thf(35441,plain,
! [B: $i,A: $i] :
( ( ( o @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack2 ) )
= o ) ),
inference(rewrite,[status(thm)],[325,97]) ).
thf(393,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ pack2 ) ) )
| ( ( i @ ( C @ ( B @ pack1 ) @ ( C @ ( B @ inv @ unpack2 ) ) ) )
= C )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,32]) ).
thf(394,plain,
! [B: $i,A: $i] :
( ( ( i @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ inv @ unpack2 ) ) ) )
= B )
| ( ( B @ ( A @ pack2 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[393:[bind(A,$thf( E @ ( D @ pack2 ) )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(401,plain,
! [B: $i,A: $i] :
( ( ( i @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ inv @ unpack2 ) ) ) )
= B )
| ( ( B @ ( A @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[394]) ).
thf(360,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ inv )
!= ( B @ inv ) )
| ( ( C @ ( B @ pack2 ) @ ( C @ ( B @ pack1 ) @ ( C @ ( o @ unpack1 ) ) ) )
= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[126,22]) ).
thf(361,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( o @ unpack1 ) ) ) )
= A )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[360:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(378,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( o @ unpack1 ) ) ) )
= A )
| ( A = o ) ),
inference(simp,[status(thm)],[361]) ).
thf(257,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ pack1 ) ) )
| ( ( C @ ( B @ pack2 ) @ ( i @ inv @ ( C @ ( B @ unpack1 ) ) ) )
= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,26]) ).
thf(258,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( i @ inv @ ( B @ ( A @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack1 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[257:[bind(A,$thf( E @ ( D @ pack1 ) )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(275,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( i @ inv @ ( B @ ( A @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack1 ) )
= o ) ),
inference(simp,[status(thm)],[258]) ).
thf(24549,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( o @ ( B @ ( A @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack1 ) )
= o ) ),
inference(rewrite,[status(thm)],[275,97]) ).
thf(94193,plain,
! [B: $i,A: $i] :
( ( B
!= ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) ) )
| ( A
!= ( o @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) ) )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( A @ inv )
= i )
| ( B = o ) ),
inference(paramod_ordered,[status(thm)],[32386,41602]) ).
thf(94194,plain,
! [A: $i] :
( ( A
!= ( o @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) ) )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( A @ inv )
= i )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[94193:[bind(A,$thf( A )),bind(B,$thf( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) ))]]) ).
thf(98460,plain,
( ( ( o @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) @ inv )
= i )
| ( ( i @ ( i @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[94194]) ).
thf(58368,plain,
( ( o != o )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
!= ( o @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) ) )
| ( ( o @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(eqfactor_ordered,[status(thm)],[56892]) ).
thf(58391,plain,
( ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
!= ( o @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) ) )
| ( ( o @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[58368]) ).
thf(674,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ inv @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack1 ) ) ) )
!= ( C @ ( i @ pack2 ) @ ( i @ ( C @ ( o @ unpack1 ) ) ) ) )
| ( A = i )
| ( ( C @ ( i @ pack1 ) )
= o ) ),
inference(paramod_ordered,[status(thm)],[28,190]) ).
thf(685,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ inv )
!= ( C @ ( i @ pack2 ) ) )
| ( ( B @ ( A @ pack1 ) )
!= i )
| ( B != C )
| ( A != o )
| ( A = i )
| ( ( C @ ( i @ pack1 ) )
= o ) ),
inference(simp,[status(thm)],[674]) ).
thf(697,plain,
! [A: $i] :
( ( ( A @ ( i @ pack2 ) )
!= ( A @ ( o @ pack2 ) @ inv ) )
| ( ( A @ ( o @ pack1 ) )
!= i )
| ( i = o )
| ( ( A @ ( i @ pack1 ) )
= o ) ),
inference(simp,[status(thm)],[685]) ).
thf(107445,plain,
! [A: $i] :
( ( ( A @ ( i @ pack2 ) )
!= ( A @ ( o @ pack2 ) @ inv ) )
| ( ( A @ ( o @ pack1 ) )
!= i )
| ( ( A @ ( i @ pack1 ) )
= o ) ),
inference(simplifyReflect,[status(thm)],[697,116]) ).
thf(409,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ ( i @ pack2 ) ) )
| ( ( i @ ( B @ ( i @ pack1 ) @ ( B @ ( o @ unpack2 ) ) ) )
= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,404]) ).
thf(410,plain,
! [A: $i] :
( ( ( i @ ( A @ ( i @ pack1 ) @ ( A @ ( o @ unpack2 ) ) ) )
= A )
| ( ( A @ ( i @ pack2 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[409:[bind(A,$thf( D @ ( i @ pack2 ) )),bind(B,$thf( D ))]]) ).
thf(432,plain,
! [A: $i] :
( ( ( i @ ( A @ ( i @ pack1 ) @ ( A @ ( o @ unpack2 ) ) ) )
= A )
| ( ( A @ ( i @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[410]) ).
thf(46880,plain,
! [B: $i,A: $i] :
( ( ( o @ ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) @ pack1 ) )
!= ( B @ ( A @ pack1 ) ) )
| ( ( B @ ( i @ pack2 ) @ ( o @ ( B @ ( o @ unpack1 ) ) ) )
= i )
| ( A = o )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(paramod_ordered,[status(thm)],[46818,181]) ).
thf(46881,plain,
( ( ( o @ ( i @ pack2 ) @ ( o @ ( o @ ( o @ unpack1 ) ) ) )
= i )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[46880:[bind(A,$thf( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )),bind(B,$thf( o ))]]) ).
thf(47489,plain,
( ( ( o @ ( i @ pack2 ) @ ( o @ ( o @ ( o @ unpack1 ) ) ) )
= i )
| ( ( o @ ( i @ pack2 ) @ ( i @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[46881]) ).
thf(779,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ inv @ pack1 ) ) )
| ( ( B @ inv )
!= B )
| ( ( C @ ( B @ pack1 ) )
!= i )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,51]) ).
thf(780,plain,
! [B: $i,A: $i] :
( ( ( B @ inv )
!= B )
| ( ( A @ ( B @ pack1 ) )
!= i )
| ( ( A @ ( B @ inv @ pack1 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[779:[bind(A,$thf( E @ ( F @ inv @ pack1 ) )),bind(B,$thf( F )),bind(C,$thf( E ))]]) ).
thf(790,plain,
! [B: $i,A: $i] :
( ( ( B @ inv )
!= B )
| ( ( A @ ( B @ pack1 ) )
!= i )
| ( ( A @ ( B @ inv @ pack1 ) )
= o ) ),
inference(simp,[status(thm)],[780]) ).
thf(372,plain,
! [A: $i] :
( ( o != o )
| ( ( A @ inv )
!= A )
| ( A = o ) ),
inference(eqfactor_ordered,[status(thm)],[126]) ).
thf(373,plain,
! [A: $i] :
( ( ( A @ inv )
!= A )
| ( A = o ) ),
inference(simp,[status(thm)],[372]) ).
thf(60,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ inv @ pack1 ) ) )
| ( ( C @ ( B @ inv @ pack2 ) )
!= ( C @ ( B @ pack2 ) ) )
| ( ( C @ ( B @ pack1 ) )
!= i )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,45]) ).
thf(61,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ inv @ pack2 ) )
!= ( A @ ( B @ pack2 ) ) )
| ( ( A @ ( B @ pack1 ) )
!= i )
| ( ( A @ ( B @ inv @ pack1 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[60:[bind(A,$thf( E @ ( F @ inv @ pack1 ) )),bind(B,$thf( F )),bind(C,$thf( E ))]]) ).
thf(107,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ inv @ pack2 ) )
!= ( A @ ( B @ pack2 ) ) )
| ( ( A @ ( B @ pack1 ) )
!= i )
| ( ( A @ ( B @ inv @ pack1 ) )
= o ) ),
inference(simp,[status(thm)],[61]) ).
thf(210,plain,
! [B: $i,A: $i] :
( ( A
!= ( i @ ( B @ pack1 ) ) )
| ( ( i @ ( B @ pack2 ) @ ( i @ ( o @ ( B @ unpack1 ) ) ) )
= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,139]) ).
thf(211,plain,
! [A: $i] :
( ( ( i @ ( A @ pack2 ) @ ( i @ ( o @ ( A @ unpack1 ) ) ) )
= A )
| ( ( i @ ( A @ pack1 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[210:[bind(A,$thf( i @ ( C @ pack1 ) )),bind(B,$thf( C ))]]) ).
thf(239,plain,
! [A: $i] :
( ( ( i @ ( A @ pack2 ) @ ( i @ ( o @ ( A @ unpack1 ) ) ) )
= A )
| ( ( i @ ( A @ pack1 ) )
= o ) ),
inference(simp,[status(thm)],[211]) ).
thf(32372,plain,
! [A: $i] :
( ( ( o @ inv )
!= ( A @ inv ) )
| ( i != i )
| ( ( i @ ( o @ pack2 ) )
!= o )
| ( ( o @ ( i @ pack1 ) )
!= ( i @ ( o @ pack1 ) ) )
| ( ( o @ ( A @ pack2 ) )
!= i )
| ( ( o @ ( A @ inv @ pack1 ) )
!= ( o @ ( A @ pack1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[31674,1047]) ).
thf(32373,plain,
! [A: $i] :
( ( ( o @ inv )
!= ( A @ inv ) )
| ( ( i @ ( o @ pack2 ) )
!= o )
| ( ( o @ ( i @ pack1 ) )
!= ( i @ ( o @ pack1 ) ) )
| ( ( o @ ( A @ pack2 ) )
!= i )
| ( ( o @ ( A @ inv @ pack1 ) )
!= ( o @ ( A @ pack1 ) ) ) ),
inference(simp,[status(thm)],[32372]) ).
thf(32374,plain,
( ( ( i @ ( o @ pack2 ) )
!= o )
| ( ( o @ ( i @ pack1 ) )
!= ( i @ ( o @ pack1 ) ) )
| ( ( o @ ( o @ pack2 ) )
!= i )
| ( ( o @ ( o @ inv @ pack1 ) )
!= ( o @ ( o @ pack1 ) ) ) ),
inference(pattern_uni,[status(thm)],[32373:[bind(A,$thf( o ))]]) ).
thf(48915,plain,
( ( ( i @ ( o @ pack2 ) )
!= o )
| ( ( o @ ( i @ pack1 ) )
!= ( i @ ( o @ pack1 ) ) )
| ( ( o @ ( o @ pack2 ) )
!= i )
| ( ( o @ ( i @ pack1 ) )
!= ( o @ ( o @ pack1 ) ) ) ),
inference(rewrite,[status(thm)],[32374,31674]) ).
thf(391,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ pack1 ) ) )
| ( ( C @ ( B @ pack2 ) @ ( i @ ( C @ ( B @ inv @ unpack2 ) ) ) )
= C )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,32]) ).
thf(392,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( i @ ( B @ ( A @ inv @ unpack2 ) ) ) )
= B )
| ( ( B @ ( A @ pack1 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[391:[bind(A,$thf( E @ ( D @ pack1 ) )),bind(B,$thf( D )),bind(C,$thf( E ))]]) ).
thf(400,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ ( i @ ( B @ ( A @ inv @ unpack2 ) ) ) )
= B )
| ( ( B @ ( A @ pack1 ) )
= o ) ),
inference(simp,[status(thm)],[392]) ).
thf(70,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( B @ inv ) )
| ( ( C @ ( B @ pack2 ) @ ( C @ ( B @ pack1 ) @ ( C @ ( i @ unpack1 ) ) ) )
= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,22]) ).
thf(71,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ pack2 ) @ ( A @ ( B @ pack1 ) @ ( A @ ( i @ unpack1 ) ) ) )
= B )
| ( ( B @ inv )
= o ) ),
inference(pattern_uni,[status(thm)],[70:[bind(A,$thf( D @ inv )),bind(B,$thf( D ))]]) ).
thf(94,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ pack2 ) @ ( A @ ( B @ pack1 ) @ ( A @ ( i @ unpack1 ) ) ) )
= B )
| ( ( B @ inv )
= o ) ),
inference(simp,[status(thm)],[71]) ).
thf(166,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( i @ pack2 ) @ ( A @ ( i @ pack1 ) @ ( A @ ( o @ unpack1 ) ) ) )
!= ( C @ ( B @ pack2 ) @ ( C @ ( B @ pack1 ) @ ( C @ ( B @ inv @ unpack1 ) ) ) ) )
| ( i = B ) ),
inference(paramod_ordered,[status(thm)],[128,22]) ).
thf(185,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( i @ pack2 ) )
!= ( C @ ( B @ pack2 ) ) )
| ( ( A @ ( i @ pack1 ) )
!= ( C @ ( B @ pack1 ) ) )
| ( A != C )
| ( ( B @ inv )
!= o )
| ( i = B ) ),
inference(simp,[status(thm)],[166]) ).
thf(195,plain,
! [B: $i,A: $i] :
( ( ( B @ ( i @ pack2 ) )
!= ( B @ ( A @ pack2 ) ) )
| ( ( B @ ( i @ pack1 ) )
!= ( B @ ( A @ pack1 ) ) )
| ( ( A @ inv )
!= o )
| ( i = A ) ),
inference(simp,[status(thm)],[185]) ).
thf(596,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) @ inv )
!= ( i @ inv ) )
| ( ( o @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack2 ) ) ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[97,38]) ).
thf(624,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ pack2 ) )
!= i )
| ( ( o @ ( B @ ( A @ pack1 ) @ ( B @ ( A @ unpack2 ) ) ) )
= B ) ),
inference(simp,[status(thm)],[596]) ).
thf(574,plain,
! [B: $i,A: $i] :
( ( i != i )
| ( ( B @ ( i @ pack2 ) )
!= ( B @ ( o @ pack2 ) ) )
| ( ( B @ ( A @ pack1 ) )
!= ( B @ ( o @ pack1 ) ) )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,562]) ).
thf(575,plain,
! [B: $i,A: $i] :
( ( ( B @ ( i @ pack2 ) )
!= ( B @ ( o @ pack2 ) ) )
| ( ( B @ ( A @ pack1 ) )
!= ( B @ ( o @ pack1 ) ) )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[574:[]]) ).
thf(32356,plain,
! [A: $i] :
( ( ( o @ inv )
!= ( A @ inv ) )
| ( ( A @ inv @ ( i @ pack2 ) )
!= ( A @ ( o @ pack2 ) ) )
| ( ( i @ ( i @ pack1 ) )
!= ( A @ ( o @ pack1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[31674,16184]) ).
thf(32357,plain,
( ( ( o @ inv @ ( i @ pack2 ) )
!= ( o @ ( o @ pack2 ) ) )
| ( ( i @ ( i @ pack1 ) )
!= ( o @ ( o @ pack1 ) ) ) ),
inference(pattern_uni,[status(thm)],[32356:[bind(A,$thf( o ))]]) ).
thf(33171,plain,
( ( ( i @ ( i @ pack2 ) )
!= ( o @ ( o @ pack2 ) ) )
| ( ( i @ ( i @ pack1 ) )
!= ( o @ ( o @ pack1 ) ) ) ),
inference(rewrite,[status(thm)],[32357,31674]) ).
thf(206,plain,
! [C: $i,B: $i,A: $i] :
( ( ( i @ ( A @ pack2 ) @ ( i @ ( A @ pack1 ) @ ( o @ ( A @ unpack1 ) ) ) )
!= ( C @ ( B @ pack2 ) @ ( C @ ( B @ pack1 ) @ ( C @ ( B @ inv @ unpack1 ) ) ) ) )
| ( A = B ) ),
inference(paramod_ordered,[status(thm)],[139,22]) ).
thf(224,plain,
! [C: $i,B: $i,A: $i] :
( ( ( i @ ( A @ pack2 ) )
!= ( C @ ( B @ pack2 ) ) )
| ( ( i @ ( A @ pack1 ) )
!= ( C @ ( B @ pack1 ) ) )
| ( o != C )
| ( A
!= ( B @ inv ) )
| ( A = B ) ),
inference(simp,[status(thm)],[206]) ).
thf(231,plain,
! [A: $i] :
( ( ( i @ ( A @ inv @ pack2 ) )
!= ( o @ ( A @ pack2 ) ) )
| ( ( i @ ( A @ inv @ pack1 ) )
!= ( o @ ( A @ pack1 ) ) )
| ( ( A @ inv )
= A ) ),
inference(simp,[status(thm)],[224]) ).
thf(21971,plain,
! [A: $i] :
( ( ( i @ ( A @ inv @ pack2 ) )
!= ( o @ ( A @ pack2 ) ) )
| ( ( i @ ( A @ inv @ pack1 ) )
!= ( o @ ( A @ pack1 ) ) ) ),
inference(simplifyReflect,[status(thm)],[231,18]) ).
thf(10699,plain,
! [B: $i,A: $i] :
( ( ( o @ inv @ inv )
!= ( A @ inv ) )
| ( ( B @ ( A @ pack2 ) @ ( B @ ( A @ pack1 ) @ ( B @ ( o @ unpack2 ) ) ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[10467,32]) ).
thf(10700,plain,
! [A: $i] :
( ( A @ ( o @ inv @ pack2 ) @ ( A @ ( o @ inv @ pack1 ) @ ( A @ ( o @ unpack2 ) ) ) )
= A ),
inference(pattern_uni,[status(thm)],[10699:[bind(A,$thf( o @ inv )),bind(B,$thf( B ))]]) ).
thf(10756,plain,
! [A: $i] :
( ( A @ ( o @ inv @ pack2 ) @ ( A @ ( o @ inv @ pack1 ) @ ( A @ ( o @ unpack2 ) ) ) )
= A ),
inference(simp,[status(thm)],[10700]) ).
thf(12012,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ ( o @ inv @ pack2 ) @ ( B @ ( o @ inv @ pack1 ) @ ( B @ ( o @ unpack2 ) ) ) ) )
| ( i = B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,10756]) ).
thf(12013,plain,
! [A: $i] :
( ( i = A )
| ( ( A @ ( o @ inv @ pack2 ) @ ( A @ ( o @ inv @ pack1 ) @ ( A @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[12012:[bind(A,$thf( K @ ( o @ inv @ pack2 ) @ ( K @ ( o @ inv @ pack1 ) @ ( K @ ( o @ unpack2 ) ) ) )),bind(B,$thf( K ))]]) ).
thf(12283,plain,
! [A: $i] :
( ( i = A )
| ( ( A @ ( o @ inv @ pack2 ) @ ( A @ ( o @ inv @ pack1 ) @ ( A @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[12013]) ).
thf(106766,plain,
! [A: $i] :
( ( i = A )
| ( ( A @ ( i @ pack2 ) @ ( A @ ( i @ pack1 ) @ ( A @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(rewrite,[status(thm)],[12283,31674]) ).
thf(32403,plain,
! [B: $i,A: $i] :
( ( ( o @ inv )
!= ( A @ inv ) )
| ( ( i @ ( B @ ( A @ pack1 ) @ ( B @ ( i @ unpack1 ) ) ) )
= A )
| ( ( B @ ( A @ pack2 ) )
= o ) ),
inference(paramod_ordered,[status(thm)],[31674,96]) ).
thf(32404,plain,
! [A: $i] :
( ( ( i @ ( A @ ( o @ pack1 ) @ ( A @ ( i @ unpack1 ) ) ) )
= o )
| ( ( A @ ( o @ pack2 ) )
= o ) ),
inference(pattern_uni,[status(thm)],[32403:[bind(A,$thf( o ))]]) ).
thf(32498,plain,
! [A: $i] :
( ( ( i @ ( A @ ( o @ pack1 ) @ ( A @ ( i @ unpack1 ) ) ) )
= o )
| ( ( A @ ( o @ pack2 ) )
= o ) ),
inference(simp,[status(thm)],[32404]) ).
thf(28965,plain,
! [B: $i,A: $i] :
( ( B
!= ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) ) )
| ( A
!= ( i @ ( o @ pack2 ) @ ( o @ ( o @ ( o @ unpack1 ) ) ) ) )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( A @ inv )
!= o )
| ( B = o ) ),
inference(paramod_ordered,[status(thm)],[10777,3133]) ).
thf(28966,plain,
! [A: $i] :
( ( A
!= ( i @ ( o @ pack2 ) @ ( o @ ( o @ ( o @ unpack1 ) ) ) ) )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( ( A @ inv )
!= o )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[28965:[bind(A,$thf( A )),bind(B,$thf( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) ))]]) ).
thf(30465,plain,
( ( ( i @ ( o @ pack2 ) @ ( o @ ( o @ ( o @ unpack1 ) ) ) @ inv )
!= o )
| ( ( i @ ( o @ pack2 ) @ ( i @ ( o @ ( o @ unpack1 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[28966]) ).
thf(441,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ inv )
!= ( C @ inv ) )
| ( ( C @ ( B @ pack2 ) @ ( C @ ( B @ pack1 ) @ ( o @ ( B @ unpack2 ) ) ) )
= C )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[126,34]) ).
thf(442,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ pack2 ) @ ( A @ ( B @ pack1 ) @ ( o @ ( B @ unpack2 ) ) ) )
= A )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[441:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A ))]]) ).
thf(13305,plain,
! [A: $i] :
( ( ( o @ inv )
!= ( o @ inv ) )
| ( ( i @ ( o @ pack2 ) @ ( A @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[9477,13128]) ).
thf(13306,plain,
! [A: $i] :
( ( ( i @ ( o @ pack2 ) @ ( A @ ( o @ pack1 ) @ ( o @ ( o @ unpack1 ) ) ) )
= o )
| ( A = o ) ),
inference(pattern_uni,[status(thm)],[13305:[]]) ).
thf(83466,plain,
! [B: $i,A: $i] :
( ( A
!= ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) ) )
| ( B
!= ( o @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) ) )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( B @ inv )
!= o )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[10784,56806]) ).
thf(83467,plain,
! [A: $i] :
( ( A
!= ( o @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) ) )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o )
| ( ( A @ inv )
!= o )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(pattern_uni,[status(thm)],[83466:[bind(A,$thf( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )),bind(B,$thf( B ))]]) ).
thf(83795,plain,
( ( ( o @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) @ inv )
!= o )
| ( ( i @ ( o @ ( i @ pack1 ) @ ( o @ ( o @ unpack2 ) ) ) )
= o ) ),
inference(simp,[status(thm)],[83467]) ).
thf(82,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( B @ inv ) )
| ( ( C @ ( i @ pack2 ) )
!= ( C @ ( B @ pack2 ) ) )
| ( ( B @ inv )
!= B )
| ( A = o ) ),
inference(paramod_ordered,[status(thm)],[15,50]) ).
thf(83,plain,
! [B: $i,A: $i] :
( ( ( A @ ( i @ pack2 ) )
!= ( A @ ( B @ pack2 ) ) )
| ( ( B @ inv )
!= B )
| ( ( B @ inv )
= o ) ),
inference(pattern_uni,[status(thm)],[82:[bind(A,$thf( D @ inv )),bind(B,$thf( D ))]]) ).
thf(100,plain,
! [B: $i,A: $i] :
( ( ( A @ ( i @ pack2 ) )
!= ( A @ ( B @ pack2 ) ) )
| ( ( B @ inv )
!= B )
| ( ( B @ inv )
= o ) ),
inference(simp,[status(thm)],[83]) ).
thf(87597,plain,
! [B: $i,A: $i] :
( ( ( A @ ( i @ pack2 ) )
!= ( i @ ( B @ pack2 ) ) )
| ( ( o @ ( B @ pack2 ) )
!= o )
| ( ( i @ ( B @ pack1 ) )
!= ( o @ ( B @ pack1 ) ) )
| ( ( A @ ( o @ pack2 ) )
!= i )
| ( ( A @ ( i @ pack1 ) )
!= ( A @ ( o @ pack1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[583,61511]) ).
thf(87598,plain,
( ( ( o @ ( i @ pack2 ) )
!= o )
| ( ( i @ ( i @ pack1 ) )
!= ( o @ ( i @ pack1 ) ) )
| ( ( i @ ( o @ pack2 ) )
!= i )
| ( ( i @ ( i @ pack1 ) )
!= ( i @ ( o @ pack1 ) ) ) ),
inference(pattern_uni,[status(thm)],[87597:[bind(A,$thf( i )),bind(B,$thf( i ))]]) ).
thf(191021,plain,
$false,
inference(e,[status(thm)],[645,33394,78945,114041,347,61022,2559,31674,109444,276,16184,48793,96584,47514,861,26333,550,89650,670,404,47531,24,79025,37,25,4511,32392,129481,3845,31733,83868,46424,702,559,3099,32504,20,421,56901,131405,47382,29,10454,61511,376,646,15623,106,238,514,112477,397,10784,116,3097,3169,59594,41605,220,1047,429,21,33,28,38,92,583,461,41466,551,324,108466,97,39615,5270,156,2895,32735,47495,131381,74471,725,488,26695,901,133815,97531,96,38100,537,32327,98350,107687,911,13,647,32736,74467,2006,128,105,26402,56892,46818,32094,266,56819,513,45,26473,15715,3686,68691,906,108988,140773,48055,37418,32,34,562,108012,41467,191,22,577,32346,27,97785,39718,181,135700,22399,274,419,1048,318,509,89418,377,32505,3133,91,10219,64392,462,98477,103,668,155,32361,108,399,438,35,41602,34404,61020,62611,64388,553,21474,105700,18,95,327,56820,50,44863,791,34856,470,643,31,32386,16,106041,34875,154,31888,32402,96586,859,115052,727,1940,42398,99,32434,581,104,134837,58879,32506,98719,37870,26,30565,139,34405,23,35441,401,10777,378,24549,98460,58391,60848,32421,107445,432,36,21932,47489,30,51,3100,75648,190,790,373,183,19,107,239,126,48915,400,94,195,50011,624,47493,575,33171,21971,35786,15,34925,106766,32498,30465,442,486,32299,13306,222,83795,100,87598,56806]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV052-1.002.002 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.12/0.40 % Computer : n017.cluster.edu
% 0.12/0.40 % Model : x86_64 x86_64
% 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40 % Memory : 8046.5625MB
% 0.12/0.40 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Fri Sep 25 16:16:32 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.71/0.70 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 0.93/0.80 % [INFO] Parsing done (95ms).
% 0.93/0.80 % [INFO] Running in sequential loop mode.
% 1.11/1.00 % [INFO] eprover registered as external prover.
% 1.11/1.00 % [INFO] Scanning for conjecture ...
% 1.42/1.03 % [INFO] 12 axioms and no conjecture found.
% 1.42/1.06 % [INFO] Problem is propositional (TPTP CNF).
% 1.42/1.06 % [INFO] Type checking passed.
% 1.42/1.07 % [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 ...
% 1.64/1.14 % [INFO] [Domain constraints] Detected constraint on $i
% 1.64/1.15 % [INFO] [Domain constraints] dom($i) ⊆ {o,i}
% 191.95/54.89 % External prover 'e' found a proof!
% 191.95/54.89 % [INFO] Killing All external provers ...
% 191.95/54.89 % Time passed: 54400ms (effective reasoning time: 54080ms)
% 191.95/54.89 % Axioms used in derivation (12): bit_inverse, unpack2_07, unpack2, unpack2_06, unpack1, unpack1_04, bit_domain, unpack1_02, unpack1_03, unpack1_01, unpack2_05, unpack2_08
% 191.95/54.89 % No. of inferences in proof: 723
% 191.95/54.89 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p : 54400 ms resp. 54080 ms w/o parsing
% 193.20/55.04 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 193.20/55.04 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------