%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ALG064+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n005.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 06:46:01 AM UTC 2026
% Result : Theorem 71.31s 16.69s
% Output : Refutation 49.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 90
% Number of leaves : 6
% Syntax : Number of formulae : 508 ( 238 unt; 0 typ; 0 def)
% Number of atoms : 5027 (2206 equ; 0 cnn)
% Maximal formula atoms : 2068 ( 9 avg)
% Number of connectives : 14276 (3499 ~;3645 |; 810 &;6322 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 196 ( 6 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 28 ( 25 usr; 26 con; 0-2 aty)
% Number of variables : 0 ( 0 ^; 0 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
thf(op_decl,type,
op: $i > $i > $i ).
thf(e0_decl,type,
e0: $i ).
thf(e1_decl,type,
e1: $i ).
thf(e2_decl,type,
e2: $i ).
thf(e3_decl,type,
e3: $i ).
thf(e4_decl,type,
e4: $i ).
thf(unit_decl,type,
unit: $i ).
thf(sk1_decl,type,
sk1: $o ).
thf(sk2_decl,type,
sk2: $o ).
thf(sk3_decl,type,
sk3: $o ).
thf(sk4_decl,type,
sk4: $o ).
thf(sk5_decl,type,
sk5: $o ).
thf(sk6_decl,type,
sk6: $o ).
thf(sk7_decl,type,
sk7: $o ).
thf(sk8_decl,type,
sk8: $o ).
thf(sk9_decl,type,
sk9: $o ).
thf(sk10_decl,type,
sk10: $o ).
thf(sk11_decl,type,
sk11: $o ).
thf(sk12_decl,type,
sk12: $o ).
thf(sk13_decl,type,
sk13: $o ).
thf(sk14_decl,type,
sk14: $o ).
thf(sk15_decl,type,
sk15: $o ).
thf(sk16_decl,type,
sk16: $o ).
thf(sk17_decl,type,
sk17: $o ).
thf(sk18_decl,type,
sk18: $o ).
thf(1,conjecture,
~ ( ( ( ( ( e4 @ ( e4 @ ( e4 @ op ) @ op ) )
!= e4 )
& ( ( e4 @ ( e4 @ ( e4 @ op ) @ op ) )
= e4 )
& ( ( e4 @ ( e4 @ op ) )
!= ( e4 @ ( e4 @ op ) ) ) )
| ( ( ( e4 @ ( e3 @ ( e4 @ op ) @ op ) )
!= e3 )
& ( ( e3 @ ( e3 @ ( e4 @ op ) @ op ) )
= e4 )
& ( ( e4 @ ( e3 @ op ) )
!= ( e3 @ ( e4 @ op ) ) ) )
| ( ( ( e4 @ ( e2 @ ( e4 @ op ) @ op ) )
!= e2 )
& ( ( e2 @ ( e2 @ ( e4 @ op ) @ op ) )
= e4 )
& ( ( e4 @ ( e2 @ op ) )
!= ( e2 @ ( e4 @ op ) ) ) )
| ( ( ( e4 @ ( e1 @ ( e4 @ op ) @ op ) )
!= e1 )
& ( ( e1 @ ( e1 @ ( e4 @ op ) @ op ) )
= e4 )
& ( ( e4 @ ( e1 @ op ) )
!= ( e1 @ ( e4 @ op ) ) ) )
| ( ( ( e4 @ ( e0 @ ( e4 @ op ) @ op ) )
!= e0 )
& ( ( e0 @ ( e0 @ ( e4 @ op ) @ op ) )
= e4 )
& ( ( e4 @ ( e0 @ op ) )
!= ( e0 @ ( e4 @ op ) ) ) )
| ( ( ( e3 @ ( e4 @ ( e3 @ op ) @ op ) )
!= e4 )
& ( ( e4 @ ( e4 @ ( e3 @ op ) @ op ) )
= e3 )
& ( ( e3 @ ( e4 @ op ) )
!= ( e4 @ ( e3 @ op ) ) ) )
| ( ( ( e3 @ ( e3 @ ( e3 @ op ) @ op ) )
!= e3 )
& ( ( e3 @ ( e3 @ ( e3 @ op ) @ op ) )
= e3 )
& ( ( e3 @ ( e3 @ op ) )
!= ( e3 @ ( e3 @ op ) ) ) )
| ( ( ( e3 @ ( e2 @ ( e3 @ op ) @ op ) )
!= e2 )
& ( ( e2 @ ( e2 @ ( e3 @ op ) @ op ) )
= e3 )
& ( ( e3 @ ( e2 @ op ) )
!= ( e2 @ ( e3 @ op ) ) ) )
| ( ( ( e3 @ ( e1 @ ( e3 @ op ) @ op ) )
!= e1 )
& ( ( e1 @ ( e1 @ ( e3 @ op ) @ op ) )
= e3 )
& ( ( e3 @ ( e1 @ op ) )
!= ( e1 @ ( e3 @ op ) ) ) )
| ( ( ( e3 @ ( e0 @ ( e3 @ op ) @ op ) )
!= e0 )
& ( ( e0 @ ( e0 @ ( e3 @ op ) @ op ) )
= e3 )
& ( ( e3 @ ( e0 @ op ) )
!= ( e0 @ ( e3 @ op ) ) ) )
| ( ( ( e2 @ ( e4 @ ( e2 @ op ) @ op ) )
!= e4 )
& ( ( e4 @ ( e4 @ ( e2 @ op ) @ op ) )
= e2 )
& ( ( e2 @ ( e4 @ op ) )
!= ( e4 @ ( e2 @ op ) ) ) )
| ( ( ( e2 @ ( e3 @ ( e2 @ op ) @ op ) )
!= e3 )
& ( ( e3 @ ( e3 @ ( e2 @ op ) @ op ) )
= e2 )
& ( ( e2 @ ( e3 @ op ) )
!= ( e3 @ ( e2 @ op ) ) ) )
| ( ( ( e2 @ ( e2 @ ( e2 @ op ) @ op ) )
!= e2 )
& ( ( e2 @ ( e2 @ ( e2 @ op ) @ op ) )
= e2 )
& ( ( e2 @ ( e2 @ op ) )
!= ( e2 @ ( e2 @ op ) ) ) )
| ( ( ( e2 @ ( e1 @ ( e2 @ op ) @ op ) )
!= e1 )
& ( ( e1 @ ( e1 @ ( e2 @ op ) @ op ) )
= e2 )
& ( ( e2 @ ( e1 @ op ) )
!= ( e1 @ ( e2 @ op ) ) ) )
| ( ( ( e2 @ ( e0 @ ( e2 @ op ) @ op ) )
!= e0 )
& ( ( e0 @ ( e0 @ ( e2 @ op ) @ op ) )
= e2 )
& ( ( e2 @ ( e0 @ op ) )
!= ( e0 @ ( e2 @ op ) ) ) )
| ( ( ( e1 @ ( e4 @ ( e1 @ op ) @ op ) )
!= e4 )
& ( ( e4 @ ( e4 @ ( e1 @ op ) @ op ) )
= e1 )
& ( ( e1 @ ( e4 @ op ) )
!= ( e4 @ ( e1 @ op ) ) ) )
| ( ( ( e1 @ ( e3 @ ( e1 @ op ) @ op ) )
!= e3 )
& ( ( e3 @ ( e3 @ ( e1 @ op ) @ op ) )
= e1 )
& ( ( e1 @ ( e3 @ op ) )
!= ( e3 @ ( e1 @ op ) ) ) )
| ( ( ( e1 @ ( e2 @ ( e1 @ op ) @ op ) )
!= e2 )
& ( ( e2 @ ( e2 @ ( e1 @ op ) @ op ) )
= e1 )
& ( ( e1 @ ( e2 @ op ) )
!= ( e2 @ ( e1 @ op ) ) ) )
| ( ( ( e1 @ ( e1 @ ( e1 @ op ) @ op ) )
!= e1 )
& ( ( e1 @ ( e1 @ ( e1 @ op ) @ op ) )
= e1 )
& ( ( e1 @ ( e1 @ op ) )
!= ( e1 @ ( e1 @ op ) ) ) )
| ( ( ( e1 @ ( e0 @ ( e1 @ op ) @ op ) )
!= e0 )
& ( ( e0 @ ( e0 @ ( e1 @ op ) @ op ) )
= e1 )
& ( ( e1 @ ( e0 @ op ) )
!= ( e0 @ ( e1 @ op ) ) ) )
| ( ( ( e0 @ ( e4 @ ( e0 @ op ) @ op ) )
!= e4 )
& ( ( e4 @ ( e4 @ ( e0 @ op ) @ op ) )
= e0 )
& ( ( e0 @ ( e4 @ op ) )
!= ( e4 @ ( e0 @ op ) ) ) )
| ( ( ( e0 @ ( e3 @ ( e0 @ op ) @ op ) )
!= e3 )
& ( ( e3 @ ( e3 @ ( e0 @ op ) @ op ) )
= e0 )
& ( ( e0 @ ( e3 @ op ) )
!= ( e3 @ ( e0 @ op ) ) ) )
| ( ( ( e0 @ ( e2 @ ( e0 @ op ) @ op ) )
!= e2 )
& ( ( e2 @ ( e2 @ ( e0 @ op ) @ op ) )
= e0 )
& ( ( e0 @ ( e2 @ op ) )
!= ( e2 @ ( e0 @ op ) ) ) )
| ( ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 )
& ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 )
& ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
| ( ( ( e0 @ ( e0 @ ( e0 @ op ) @ op ) )
!= e0 )
& ( ( e0 @ ( e0 @ ( e0 @ op ) @ op ) )
= e0 )
& ( ( e0 @ ( e0 @ op ) )
!= ( e0 @ ( e0 @ op ) ) ) ) )
& ( ( ( e4 @ ( e4 @ op ) )
= e4 )
| ( ( e3 @ ( e3 @ op ) )
= e4 )
| ( ( e2 @ ( e2 @ op ) )
= e4 )
| ( ( e1 @ ( e1 @ op ) )
= e4 )
| ( ( e0 @ ( e0 @ op ) )
= e4 ) )
& ( ( ( e4 @ ( e4 @ op ) )
= e3 )
| ( ( e3 @ ( e3 @ op ) )
= e3 )
| ( ( e2 @ ( e2 @ op ) )
= e3 )
| ( ( e1 @ ( e1 @ op ) )
= e3 )
| ( ( e0 @ ( e0 @ op ) )
= e3 ) )
& ( ( ( e4 @ ( e4 @ op ) )
= e2 )
| ( ( e3 @ ( e3 @ op ) )
= e2 )
| ( ( e2 @ ( e2 @ op ) )
= e2 )
| ( ( e1 @ ( e1 @ op ) )
= e2 )
| ( ( e0 @ ( e0 @ op ) )
= e2 ) )
& ( ( ( e4 @ ( e4 @ op ) )
= e1 )
| ( ( e3 @ ( e3 @ op ) )
= e1 )
| ( ( e2 @ ( e2 @ op ) )
= e1 )
| ( ( e1 @ ( e1 @ op ) )
= e1 )
| ( ( e0 @ ( e0 @ op ) )
= e1 ) )
& ( ( ( e4 @ ( e4 @ op ) )
= e0 )
| ( ( e3 @ ( e3 @ op ) )
= e0 )
| ( ( e2 @ ( e2 @ op ) )
= e0 )
| ( ( e1 @ ( e1 @ op ) )
= e0 )
| ( ( e0 @ ( e0 @ op ) )
= e0 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
thf(2,negated_conjecture,
~ ~ ( ( ( ( ( e4 @ ( e4 @ ( e4 @ op ) @ op ) )
!= e4 )
& ( ( e4 @ ( e4 @ ( e4 @ op ) @ op ) )
= e4 )
& ( ( e4 @ ( e4 @ op ) )
!= ( e4 @ ( e4 @ op ) ) ) )
| ( ( ( e4 @ ( e3 @ ( e4 @ op ) @ op ) )
!= e3 )
& ( ( e3 @ ( e3 @ ( e4 @ op ) @ op ) )
= e4 )
& ( ( e4 @ ( e3 @ op ) )
!= ( e3 @ ( e4 @ op ) ) ) )
| ( ( ( e4 @ ( e2 @ ( e4 @ op ) @ op ) )
!= e2 )
& ( ( e2 @ ( e2 @ ( e4 @ op ) @ op ) )
= e4 )
& ( ( e4 @ ( e2 @ op ) )
!= ( e2 @ ( e4 @ op ) ) ) )
| ( ( ( e4 @ ( e1 @ ( e4 @ op ) @ op ) )
!= e1 )
& ( ( e1 @ ( e1 @ ( e4 @ op ) @ op ) )
= e4 )
& ( ( e4 @ ( e1 @ op ) )
!= ( e1 @ ( e4 @ op ) ) ) )
| ( ( ( e4 @ ( e0 @ ( e4 @ op ) @ op ) )
!= e0 )
& ( ( e0 @ ( e0 @ ( e4 @ op ) @ op ) )
= e4 )
& ( ( e4 @ ( e0 @ op ) )
!= ( e0 @ ( e4 @ op ) ) ) )
| ( ( ( e3 @ ( e4 @ ( e3 @ op ) @ op ) )
!= e4 )
& ( ( e4 @ ( e4 @ ( e3 @ op ) @ op ) )
= e3 )
& ( ( e3 @ ( e4 @ op ) )
!= ( e4 @ ( e3 @ op ) ) ) )
| ( ( ( e3 @ ( e3 @ ( e3 @ op ) @ op ) )
!= e3 )
& ( ( e3 @ ( e3 @ ( e3 @ op ) @ op ) )
= e3 )
& ( ( e3 @ ( e3 @ op ) )
!= ( e3 @ ( e3 @ op ) ) ) )
| ( ( ( e3 @ ( e2 @ ( e3 @ op ) @ op ) )
!= e2 )
& ( ( e2 @ ( e2 @ ( e3 @ op ) @ op ) )
= e3 )
& ( ( e3 @ ( e2 @ op ) )
!= ( e2 @ ( e3 @ op ) ) ) )
| ( ( ( e3 @ ( e1 @ ( e3 @ op ) @ op ) )
!= e1 )
& ( ( e1 @ ( e1 @ ( e3 @ op ) @ op ) )
= e3 )
& ( ( e3 @ ( e1 @ op ) )
!= ( e1 @ ( e3 @ op ) ) ) )
| ( ( ( e3 @ ( e0 @ ( e3 @ op ) @ op ) )
!= e0 )
& ( ( e0 @ ( e0 @ ( e3 @ op ) @ op ) )
= e3 )
& ( ( e3 @ ( e0 @ op ) )
!= ( e0 @ ( e3 @ op ) ) ) )
| ( ( ( e2 @ ( e4 @ ( e2 @ op ) @ op ) )
!= e4 )
& ( ( e4 @ ( e4 @ ( e2 @ op ) @ op ) )
= e2 )
& ( ( e2 @ ( e4 @ op ) )
!= ( e4 @ ( e2 @ op ) ) ) )
| ( ( ( e2 @ ( e3 @ ( e2 @ op ) @ op ) )
!= e3 )
& ( ( e3 @ ( e3 @ ( e2 @ op ) @ op ) )
= e2 )
& ( ( e2 @ ( e3 @ op ) )
!= ( e3 @ ( e2 @ op ) ) ) )
| ( ( ( e2 @ ( e2 @ ( e2 @ op ) @ op ) )
!= e2 )
& ( ( e2 @ ( e2 @ ( e2 @ op ) @ op ) )
= e2 )
& ( ( e2 @ ( e2 @ op ) )
!= ( e2 @ ( e2 @ op ) ) ) )
| ( ( ( e2 @ ( e1 @ ( e2 @ op ) @ op ) )
!= e1 )
& ( ( e1 @ ( e1 @ ( e2 @ op ) @ op ) )
= e2 )
& ( ( e2 @ ( e1 @ op ) )
!= ( e1 @ ( e2 @ op ) ) ) )
| ( ( ( e2 @ ( e0 @ ( e2 @ op ) @ op ) )
!= e0 )
& ( ( e0 @ ( e0 @ ( e2 @ op ) @ op ) )
= e2 )
& ( ( e2 @ ( e0 @ op ) )
!= ( e0 @ ( e2 @ op ) ) ) )
| ( ( ( e1 @ ( e4 @ ( e1 @ op ) @ op ) )
!= e4 )
& ( ( e4 @ ( e4 @ ( e1 @ op ) @ op ) )
= e1 )
& ( ( e1 @ ( e4 @ op ) )
!= ( e4 @ ( e1 @ op ) ) ) )
| ( ( ( e1 @ ( e3 @ ( e1 @ op ) @ op ) )
!= e3 )
& ( ( e3 @ ( e3 @ ( e1 @ op ) @ op ) )
= e1 )
& ( ( e1 @ ( e3 @ op ) )
!= ( e3 @ ( e1 @ op ) ) ) )
| ( ( ( e1 @ ( e2 @ ( e1 @ op ) @ op ) )
!= e2 )
& ( ( e2 @ ( e2 @ ( e1 @ op ) @ op ) )
= e1 )
& ( ( e1 @ ( e2 @ op ) )
!= ( e2 @ ( e1 @ op ) ) ) )
| ( ( ( e1 @ ( e1 @ ( e1 @ op ) @ op ) )
!= e1 )
& ( ( e1 @ ( e1 @ ( e1 @ op ) @ op ) )
= e1 )
& ( ( e1 @ ( e1 @ op ) )
!= ( e1 @ ( e1 @ op ) ) ) )
| ( ( ( e1 @ ( e0 @ ( e1 @ op ) @ op ) )
!= e0 )
& ( ( e0 @ ( e0 @ ( e1 @ op ) @ op ) )
= e1 )
& ( ( e1 @ ( e0 @ op ) )
!= ( e0 @ ( e1 @ op ) ) ) )
| ( ( ( e0 @ ( e4 @ ( e0 @ op ) @ op ) )
!= e4 )
& ( ( e4 @ ( e4 @ ( e0 @ op ) @ op ) )
= e0 )
& ( ( e0 @ ( e4 @ op ) )
!= ( e4 @ ( e0 @ op ) ) ) )
| ( ( ( e0 @ ( e3 @ ( e0 @ op ) @ op ) )
!= e3 )
& ( ( e3 @ ( e3 @ ( e0 @ op ) @ op ) )
= e0 )
& ( ( e0 @ ( e3 @ op ) )
!= ( e3 @ ( e0 @ op ) ) ) )
| ( ( ( e0 @ ( e2 @ ( e0 @ op ) @ op ) )
!= e2 )
& ( ( e2 @ ( e2 @ ( e0 @ op ) @ op ) )
= e0 )
& ( ( e0 @ ( e2 @ op ) )
!= ( e2 @ ( e0 @ op ) ) ) )
| ( ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 )
& ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 )
& ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
| ( ( ( e0 @ ( e0 @ ( e0 @ op ) @ op ) )
!= e0 )
& ( ( e0 @ ( e0 @ ( e0 @ op ) @ op ) )
= e0 )
& ( ( e0 @ ( e0 @ op ) )
!= ( e0 @ ( e0 @ op ) ) ) ) )
& ( ( ( e4 @ ( e4 @ op ) )
= e4 )
| ( ( e3 @ ( e3 @ op ) )
= e4 )
| ( ( e2 @ ( e2 @ op ) )
= e4 )
| ( ( e1 @ ( e1 @ op ) )
= e4 )
| ( ( e0 @ ( e0 @ op ) )
= e4 ) )
& ( ( ( e4 @ ( e4 @ op ) )
= e3 )
| ( ( e3 @ ( e3 @ op ) )
= e3 )
| ( ( e2 @ ( e2 @ op ) )
= e3 )
| ( ( e1 @ ( e1 @ op ) )
= e3 )
| ( ( e0 @ ( e0 @ op ) )
= e3 ) )
& ( ( ( e4 @ ( e4 @ op ) )
= e2 )
| ( ( e3 @ ( e3 @ op ) )
= e2 )
| ( ( e2 @ ( e2 @ op ) )
= e2 )
| ( ( e1 @ ( e1 @ op ) )
= e2 )
| ( ( e0 @ ( e0 @ op ) )
= e2 ) )
& ( ( ( e4 @ ( e4 @ op ) )
= e1 )
| ( ( e3 @ ( e3 @ op ) )
= e1 )
| ( ( e2 @ ( e2 @ op ) )
= e1 )
| ( ( e1 @ ( e1 @ op ) )
= e1 )
| ( ( e0 @ ( e0 @ op ) )
= e1 ) )
& ( ( ( e4 @ ( e4 @ op ) )
= e0 )
| ( ( e3 @ ( e3 @ op ) )
= e0 )
| ( ( e2 @ ( e2 @ op ) )
= e0 )
| ( ( e1 @ ( e1 @ op ) )
= e0 )
| ( ( e0 @ ( e0 @ op ) )
= e0 ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(9,plain,
~ ~ ( ( ( ( ( e4 @ ( e3 @ ( e4 @ op ) @ op ) )
!= e3 )
& ( ( e3 @ ( e3 @ ( e4 @ op ) @ op ) )
= e4 )
& ( ( e4 @ ( e3 @ op ) )
!= ( e3 @ ( e4 @ op ) ) ) )
| ( ( ( e4 @ ( e2 @ ( e4 @ op ) @ op ) )
!= e2 )
& ( ( e2 @ ( e2 @ ( e4 @ op ) @ op ) )
= e4 )
& ( ( e4 @ ( e2 @ op ) )
!= ( e2 @ ( e4 @ op ) ) ) )
| ( ( ( e4 @ ( e1 @ ( e4 @ op ) @ op ) )
!= e1 )
& ( ( e1 @ ( e1 @ ( e4 @ op ) @ op ) )
= e4 )
& ( ( e4 @ ( e1 @ op ) )
!= ( e1 @ ( e4 @ op ) ) ) )
| ( ( ( e4 @ ( e0 @ ( e4 @ op ) @ op ) )
!= e0 )
& ( ( e0 @ ( e0 @ ( e4 @ op ) @ op ) )
= e4 )
& ( ( e4 @ ( e0 @ op ) )
!= ( e0 @ ( e4 @ op ) ) ) )
| ( ( ( e3 @ ( e4 @ ( e3 @ op ) @ op ) )
!= e4 )
& ( ( e4 @ ( e4 @ ( e3 @ op ) @ op ) )
= e3 )
& ( ( e3 @ ( e4 @ op ) )
!= ( e4 @ ( e3 @ op ) ) ) )
| ( ( ( e3 @ ( e2 @ ( e3 @ op ) @ op ) )
!= e2 )
& ( ( e2 @ ( e2 @ ( e3 @ op ) @ op ) )
= e3 )
& ( ( e3 @ ( e2 @ op ) )
!= ( e2 @ ( e3 @ op ) ) ) )
| ( ( ( e3 @ ( e1 @ ( e3 @ op ) @ op ) )
!= e1 )
& ( ( e1 @ ( e1 @ ( e3 @ op ) @ op ) )
= e3 )
& ( ( e3 @ ( e1 @ op ) )
!= ( e1 @ ( e3 @ op ) ) ) )
| ( ( ( e3 @ ( e0 @ ( e3 @ op ) @ op ) )
!= e0 )
& ( ( e0 @ ( e0 @ ( e3 @ op ) @ op ) )
= e3 )
& ( ( e3 @ ( e0 @ op ) )
!= ( e0 @ ( e3 @ op ) ) ) )
| ( ( ( e2 @ ( e4 @ ( e2 @ op ) @ op ) )
!= e4 )
& ( ( e4 @ ( e4 @ ( e2 @ op ) @ op ) )
= e2 )
& ( ( e2 @ ( e4 @ op ) )
!= ( e4 @ ( e2 @ op ) ) ) )
| ( ( ( e2 @ ( e3 @ ( e2 @ op ) @ op ) )
!= e3 )
& ( ( e3 @ ( e3 @ ( e2 @ op ) @ op ) )
= e2 )
& ( ( e2 @ ( e3 @ op ) )
!= ( e3 @ ( e2 @ op ) ) ) )
| ( ( ( e2 @ ( e1 @ ( e2 @ op ) @ op ) )
!= e1 )
& ( ( e1 @ ( e1 @ ( e2 @ op ) @ op ) )
= e2 )
& ( ( e2 @ ( e1 @ op ) )
!= ( e1 @ ( e2 @ op ) ) ) )
| ( ( ( e2 @ ( e0 @ ( e2 @ op ) @ op ) )
!= e0 )
& ( ( e0 @ ( e0 @ ( e2 @ op ) @ op ) )
= e2 )
& ( ( e2 @ ( e0 @ op ) )
!= ( e0 @ ( e2 @ op ) ) ) )
| ( ( ( e1 @ ( e4 @ ( e1 @ op ) @ op ) )
!= e4 )
& ( ( e4 @ ( e4 @ ( e1 @ op ) @ op ) )
= e1 )
& ( ( e1 @ ( e4 @ op ) )
!= ( e4 @ ( e1 @ op ) ) ) )
| ( ( ( e1 @ ( e3 @ ( e1 @ op ) @ op ) )
!= e3 )
& ( ( e3 @ ( e3 @ ( e1 @ op ) @ op ) )
= e1 )
& ( ( e1 @ ( e3 @ op ) )
!= ( e3 @ ( e1 @ op ) ) ) )
| ( ( ( e1 @ ( e2 @ ( e1 @ op ) @ op ) )
!= e2 )
& ( ( e2 @ ( e2 @ ( e1 @ op ) @ op ) )
= e1 )
& ( ( e1 @ ( e2 @ op ) )
!= ( e2 @ ( e1 @ op ) ) ) )
| ( ( ( e1 @ ( e0 @ ( e1 @ op ) @ op ) )
!= e0 )
& ( ( e0 @ ( e0 @ ( e1 @ op ) @ op ) )
= e1 )
& ( ( e1 @ ( e0 @ op ) )
!= ( e0 @ ( e1 @ op ) ) ) )
| ( ( ( e0 @ ( e4 @ ( e0 @ op ) @ op ) )
!= e4 )
& ( ( e4 @ ( e4 @ ( e0 @ op ) @ op ) )
= e0 )
& ( ( e0 @ ( e4 @ op ) )
!= ( e4 @ ( e0 @ op ) ) ) )
| ( ( ( e0 @ ( e3 @ ( e0 @ op ) @ op ) )
!= e3 )
& ( ( e3 @ ( e3 @ ( e0 @ op ) @ op ) )
= e0 )
& ( ( e0 @ ( e3 @ op ) )
!= ( e3 @ ( e0 @ op ) ) ) )
| ( ( ( e0 @ ( e2 @ ( e0 @ op ) @ op ) )
!= e2 )
& ( ( e2 @ ( e2 @ ( e0 @ op ) @ op ) )
= e0 )
& ( ( e0 @ ( e2 @ op ) )
!= ( e2 @ ( e0 @ op ) ) ) )
| ( ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 )
& ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 )
& ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) ) )
& ( ( ( e4 @ ( e4 @ op ) )
= e4 )
| ( ( e3 @ ( e3 @ op ) )
= e4 )
| ( ( e2 @ ( e2 @ op ) )
= e4 )
| ( ( e1 @ ( e1 @ op ) )
= e4 )
| ( ( e0 @ ( e0 @ op ) )
= e4 ) )
& ( ( ( e4 @ ( e4 @ op ) )
= e3 )
| ( ( e3 @ ( e3 @ op ) )
= e3 )
| ( ( e2 @ ( e2 @ op ) )
= e3 )
| ( ( e1 @ ( e1 @ op ) )
= e3 )
| ( ( e0 @ ( e0 @ op ) )
= e3 ) )
& ( ( ( e4 @ ( e4 @ op ) )
= e2 )
| ( ( e3 @ ( e3 @ op ) )
= e2 )
| ( ( e2 @ ( e2 @ op ) )
= e2 )
| ( ( e1 @ ( e1 @ op ) )
= e2 )
| ( ( e0 @ ( e0 @ op ) )
= e2 ) )
& ( ( ( e4 @ ( e4 @ op ) )
= e1 )
| ( ( e3 @ ( e3 @ op ) )
= e1 )
| ( ( e2 @ ( e2 @ op ) )
= e1 )
| ( ( e1 @ ( e1 @ op ) )
= e1 )
| ( ( e0 @ ( e0 @ op ) )
= e1 ) )
& ( ( ( e4 @ ( e4 @ op ) )
= e0 )
| ( ( e3 @ ( e3 @ op ) )
= e0 )
| ( ( e2 @ ( e2 @ op ) )
= e0 )
| ( ( e1 @ ( e1 @ op ) )
= e0 )
| ( ( e0 @ ( e0 @ op ) )
= e0 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(10,plain,
( ( ( ( ( e4 @ ( e3 @ ( e4 @ op ) @ op ) )
!= e3 )
& ( ( e3 @ ( e3 @ ( e4 @ op ) @ op ) )
= e4 )
& ( ( e4 @ ( e3 @ op ) )
!= ( e3 @ ( e4 @ op ) ) ) )
| ( ( ( e4 @ ( e2 @ ( e4 @ op ) @ op ) )
!= e2 )
& ( ( e2 @ ( e2 @ ( e4 @ op ) @ op ) )
= e4 )
& ( ( e4 @ ( e2 @ op ) )
!= ( e2 @ ( e4 @ op ) ) ) )
| ( ( ( e4 @ ( e1 @ ( e4 @ op ) @ op ) )
!= e1 )
& ( ( e1 @ ( e1 @ ( e4 @ op ) @ op ) )
= e4 )
& ( ( e4 @ ( e1 @ op ) )
!= ( e1 @ ( e4 @ op ) ) ) )
| ( ( ( e4 @ ( e0 @ ( e4 @ op ) @ op ) )
!= e0 )
& ( ( e0 @ ( e0 @ ( e4 @ op ) @ op ) )
= e4 )
& ( ( e4 @ ( e0 @ op ) )
!= ( e0 @ ( e4 @ op ) ) ) )
| ( ( ( e3 @ ( e4 @ ( e3 @ op ) @ op ) )
!= e4 )
& ( ( e4 @ ( e4 @ ( e3 @ op ) @ op ) )
= e3 )
& ( ( e3 @ ( e4 @ op ) )
!= ( e4 @ ( e3 @ op ) ) ) )
| ( ( ( e3 @ ( e2 @ ( e3 @ op ) @ op ) )
!= e2 )
& ( ( e2 @ ( e2 @ ( e3 @ op ) @ op ) )
= e3 )
& ( ( e3 @ ( e2 @ op ) )
!= ( e2 @ ( e3 @ op ) ) ) )
| ( ( ( e3 @ ( e1 @ ( e3 @ op ) @ op ) )
!= e1 )
& ( ( e1 @ ( e1 @ ( e3 @ op ) @ op ) )
= e3 )
& ( ( e3 @ ( e1 @ op ) )
!= ( e1 @ ( e3 @ op ) ) ) )
| ( ( ( e3 @ ( e0 @ ( e3 @ op ) @ op ) )
!= e0 )
& ( ( e0 @ ( e0 @ ( e3 @ op ) @ op ) )
= e3 )
& ( ( e3 @ ( e0 @ op ) )
!= ( e0 @ ( e3 @ op ) ) ) )
| ( ( ( e2 @ ( e4 @ ( e2 @ op ) @ op ) )
!= e4 )
& ( ( e4 @ ( e4 @ ( e2 @ op ) @ op ) )
= e2 )
& ( ( e2 @ ( e4 @ op ) )
!= ( e4 @ ( e2 @ op ) ) ) )
| ( ( ( e2 @ ( e3 @ ( e2 @ op ) @ op ) )
!= e3 )
& ( ( e3 @ ( e3 @ ( e2 @ op ) @ op ) )
= e2 )
& ( ( e2 @ ( e3 @ op ) )
!= ( e3 @ ( e2 @ op ) ) ) )
| ( ( ( e2 @ ( e1 @ ( e2 @ op ) @ op ) )
!= e1 )
& ( ( e1 @ ( e1 @ ( e2 @ op ) @ op ) )
= e2 )
& ( ( e2 @ ( e1 @ op ) )
!= ( e1 @ ( e2 @ op ) ) ) )
| ( ( ( e2 @ ( e0 @ ( e2 @ op ) @ op ) )
!= e0 )
& ( ( e0 @ ( e0 @ ( e2 @ op ) @ op ) )
= e2 )
& ( ( e2 @ ( e0 @ op ) )
!= ( e0 @ ( e2 @ op ) ) ) )
| ( ( ( e1 @ ( e4 @ ( e1 @ op ) @ op ) )
!= e4 )
& ( ( e4 @ ( e4 @ ( e1 @ op ) @ op ) )
= e1 )
& ( ( e1 @ ( e4 @ op ) )
!= ( e4 @ ( e1 @ op ) ) ) )
| ( ( ( e1 @ ( e3 @ ( e1 @ op ) @ op ) )
!= e3 )
& ( ( e3 @ ( e3 @ ( e1 @ op ) @ op ) )
= e1 )
& ( ( e1 @ ( e3 @ op ) )
!= ( e3 @ ( e1 @ op ) ) ) )
| ( ( ( e1 @ ( e2 @ ( e1 @ op ) @ op ) )
!= e2 )
& ( ( e2 @ ( e2 @ ( e1 @ op ) @ op ) )
= e1 )
& ( ( e1 @ ( e2 @ op ) )
!= ( e2 @ ( e1 @ op ) ) ) )
| ( ( ( e1 @ ( e0 @ ( e1 @ op ) @ op ) )
!= e0 )
& ( ( e0 @ ( e0 @ ( e1 @ op ) @ op ) )
= e1 )
& ( ( e1 @ ( e0 @ op ) )
!= ( e0 @ ( e1 @ op ) ) ) )
| ( ( ( e0 @ ( e4 @ ( e0 @ op ) @ op ) )
!= e4 )
& ( ( e4 @ ( e4 @ ( e0 @ op ) @ op ) )
= e0 )
& ( ( e0 @ ( e4 @ op ) )
!= ( e4 @ ( e0 @ op ) ) ) )
| ( ( ( e0 @ ( e3 @ ( e0 @ op ) @ op ) )
!= e3 )
& ( ( e3 @ ( e3 @ ( e0 @ op ) @ op ) )
= e0 )
& ( ( e0 @ ( e3 @ op ) )
!= ( e3 @ ( e0 @ op ) ) ) )
| ( ( ( e0 @ ( e2 @ ( e0 @ op ) @ op ) )
!= e2 )
& ( ( e2 @ ( e2 @ ( e0 @ op ) @ op ) )
= e0 )
& ( ( e0 @ ( e2 @ op ) )
!= ( e2 @ ( e0 @ op ) ) ) )
| ( ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 )
& ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 )
& ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) ) )
& ( ( ( e4 @ ( e4 @ op ) )
= e4 )
| ( ( e3 @ ( e3 @ op ) )
= e4 )
| ( ( e2 @ ( e2 @ op ) )
= e4 )
| ( ( e1 @ ( e1 @ op ) )
= e4 )
| ( ( e0 @ ( e0 @ op ) )
= e4 ) )
& ( ( ( e4 @ ( e4 @ op ) )
= e3 )
| ( ( e3 @ ( e3 @ op ) )
= e3 )
| ( ( e2 @ ( e2 @ op ) )
= e3 )
| ( ( e1 @ ( e1 @ op ) )
= e3 )
| ( ( e0 @ ( e0 @ op ) )
= e3 ) )
& ( ( ( e4 @ ( e4 @ op ) )
= e2 )
| ( ( e3 @ ( e3 @ op ) )
= e2 )
| ( ( e2 @ ( e2 @ op ) )
= e2 )
| ( ( e1 @ ( e1 @ op ) )
= e2 )
| ( ( e0 @ ( e0 @ op ) )
= e2 ) )
& ( ( ( e4 @ ( e4 @ op ) )
= e1 )
| ( ( e3 @ ( e3 @ op ) )
= e1 )
| ( ( e2 @ ( e2 @ op ) )
= e1 )
| ( ( e1 @ ( e1 @ op ) )
= e1 )
| ( ( e0 @ ( e0 @ op ) )
= e1 ) )
& ( ( ( e4 @ ( e4 @ op ) )
= e0 )
| ( ( e3 @ ( e3 @ op ) )
= e0 )
| ( ( e2 @ ( e2 @ op ) )
= e0 )
| ( ( e1 @ ( e1 @ op ) )
= e0 )
| ( ( e0 @ ( e0 @ op ) )
= e0 ) ) ),
inference(polarity_switch,[status(thm)],[9]) ).
thf(11,plain,
( ( ( ( e4 @ ( e3 @ ( e4 @ op ) @ op ) )
!= e3 )
| ~ sk18
| ~ sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( ( ( e3 @ ( e3 @ ( e4 @ op ) @ op ) )
= e4 )
| ~ sk18
| ~ sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( ( ( e4 @ ( e3 @ op ) )
!= ( e3 @ ( e4 @ op ) ) )
| ~ sk18
| ~ sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk18
| ( ( e4 @ ( e2 @ ( e4 @ op ) @ op ) )
!= e2 )
| ~ sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk18
| ( ( e2 @ ( e2 @ ( e4 @ op ) @ op ) )
= e4 )
| ~ sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk18
| ( ( e4 @ ( e2 @ op ) )
!= ( e2 @ ( e4 @ op ) ) )
| ~ sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk17
| ( ( e4 @ ( e1 @ ( e4 @ op ) @ op ) )
!= e1 )
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk17
| ( ( e1 @ ( e1 @ ( e4 @ op ) @ op ) )
= e4 )
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk17
| ( ( e4 @ ( e1 @ op ) )
!= ( e1 @ ( e4 @ op ) ) )
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk16
| ( ( e4 @ ( e0 @ ( e4 @ op ) @ op ) )
!= e0 )
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk16
| ( ( e0 @ ( e0 @ ( e4 @ op ) @ op ) )
= e4 )
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk16
| ( ( e4 @ ( e0 @ op ) )
!= ( e0 @ ( e4 @ op ) ) )
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk15
| ( ( e3 @ ( e4 @ ( e3 @ op ) @ op ) )
!= e4 )
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk15
| ( ( e4 @ ( e4 @ ( e3 @ op ) @ op ) )
= e3 )
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk15
| ( ( e3 @ ( e4 @ op ) )
!= ( e4 @ ( e3 @ op ) ) )
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk14
| ( ( e3 @ ( e2 @ ( e3 @ op ) @ op ) )
!= e2 )
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk14
| ( ( e2 @ ( e2 @ ( e3 @ op ) @ op ) )
= e3 )
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk14
| ( ( e3 @ ( e2 @ op ) )
!= ( e2 @ ( e3 @ op ) ) )
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk13
| ( ( e3 @ ( e1 @ ( e3 @ op ) @ op ) )
!= e1 )
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk13
| ( ( e1 @ ( e1 @ ( e3 @ op ) @ op ) )
= e3 )
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk13
| ( ( e3 @ ( e1 @ op ) )
!= ( e1 @ ( e3 @ op ) ) )
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk12
| ( ( e3 @ ( e0 @ ( e3 @ op ) @ op ) )
!= e0 )
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk12
| ( ( e0 @ ( e0 @ ( e3 @ op ) @ op ) )
= e3 )
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk12
| ( ( e3 @ ( e0 @ op ) )
!= ( e0 @ ( e3 @ op ) ) )
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk11
| ( ( e2 @ ( e4 @ ( e2 @ op ) @ op ) )
!= e4 )
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk11
| ( ( e4 @ ( e4 @ ( e2 @ op ) @ op ) )
= e2 )
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk11
| ( ( e2 @ ( e4 @ op ) )
!= ( e4 @ ( e2 @ op ) ) )
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk10
| ( ( e2 @ ( e3 @ ( e2 @ op ) @ op ) )
!= e3 )
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk10
| ( ( e3 @ ( e3 @ ( e2 @ op ) @ op ) )
= e2 )
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk10
| ( ( e2 @ ( e3 @ op ) )
!= ( e3 @ ( e2 @ op ) ) )
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk9
| ( ( e2 @ ( e1 @ ( e2 @ op ) @ op ) )
!= e1 )
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk9
| ( ( e1 @ ( e1 @ ( e2 @ op ) @ op ) )
= e2 )
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk9
| ( ( e2 @ ( e1 @ op ) )
!= ( e1 @ ( e2 @ op ) ) )
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk8
| ( ( e2 @ ( e0 @ ( e2 @ op ) @ op ) )
!= e0 )
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk8
| ( ( e0 @ ( e0 @ ( e2 @ op ) @ op ) )
= e2 )
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk8
| ( ( e2 @ ( e0 @ op ) )
!= ( e0 @ ( e2 @ op ) ) )
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk7
| ( ( e1 @ ( e4 @ ( e1 @ op ) @ op ) )
!= e4 )
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk7
| ( ( e4 @ ( e4 @ ( e1 @ op ) @ op ) )
= e1 )
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk7
| ( ( e1 @ ( e4 @ op ) )
!= ( e4 @ ( e1 @ op ) ) )
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk6
| ( ( e1 @ ( e3 @ ( e1 @ op ) @ op ) )
!= e3 )
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk6
| ( ( e3 @ ( e3 @ ( e1 @ op ) @ op ) )
= e1 )
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk6
| ( ( e1 @ ( e3 @ op ) )
!= ( e3 @ ( e1 @ op ) ) )
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk5
| ( ( e1 @ ( e2 @ ( e1 @ op ) @ op ) )
!= e2 )
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk5
| ( ( e2 @ ( e2 @ ( e1 @ op ) @ op ) )
= e1 )
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk5
| ( ( e1 @ ( e2 @ op ) )
!= ( e2 @ ( e1 @ op ) ) )
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk4
| ( ( e1 @ ( e0 @ ( e1 @ op ) @ op ) )
!= e0 )
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk4
| ( ( e0 @ ( e0 @ ( e1 @ op ) @ op ) )
= e1 )
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk4
| ( ( e1 @ ( e0 @ op ) )
!= ( e0 @ ( e1 @ op ) ) )
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk3
| ( ( e0 @ ( e4 @ ( e0 @ op ) @ op ) )
!= e4 )
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk3
| ( ( e4 @ ( e4 @ ( e0 @ op ) @ op ) )
= e0 )
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk3
| ( ( e0 @ ( e4 @ op ) )
!= ( e4 @ ( e0 @ op ) ) )
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk2
| ( ( e0 @ ( e3 @ ( e0 @ op ) @ op ) )
!= e3 )
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk2
| ( ( e3 @ ( e3 @ ( e0 @ op ) @ op ) )
= e0 )
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk2
| ( ( e0 @ ( e3 @ op ) )
!= ( e3 @ ( e0 @ op ) ) )
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk1
| ( ( e0 @ ( e2 @ ( e0 @ op ) @ op ) )
!= e2 )
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk1
| ( ( e2 @ ( e2 @ ( e0 @ op ) @ op ) )
= e0 )
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( sk1
| ( ( e0 @ ( e2 @ op ) )
!= ( e2 @ ( e0 @ op ) ) )
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) )
& ( ( ( e4 @ ( e3 @ ( e4 @ op ) @ op ) )
!= e3 )
| ~ sk18
| ~ sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( ( ( e3 @ ( e3 @ ( e4 @ op ) @ op ) )
= e4 )
| ~ sk18
| ~ sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( ( ( e4 @ ( e3 @ op ) )
!= ( e3 @ ( e4 @ op ) ) )
| ~ sk18
| ~ sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk18
| ( ( e4 @ ( e2 @ ( e4 @ op ) @ op ) )
!= e2 )
| ~ sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk18
| ( ( e2 @ ( e2 @ ( e4 @ op ) @ op ) )
= e4 )
| ~ sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk18
| ( ( e4 @ ( e2 @ op ) )
!= ( e2 @ ( e4 @ op ) ) )
| ~ sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk17
| ( ( e4 @ ( e1 @ ( e4 @ op ) @ op ) )
!= e1 )
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk17
| ( ( e1 @ ( e1 @ ( e4 @ op ) @ op ) )
= e4 )
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk17
| ( ( e4 @ ( e1 @ op ) )
!= ( e1 @ ( e4 @ op ) ) )
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk16
| ( ( e4 @ ( e0 @ ( e4 @ op ) @ op ) )
!= e0 )
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk16
| ( ( e0 @ ( e0 @ ( e4 @ op ) @ op ) )
= e4 )
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk16
| ( ( e4 @ ( e0 @ op ) )
!= ( e0 @ ( e4 @ op ) ) )
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk15
| ( ( e3 @ ( e4 @ ( e3 @ op ) @ op ) )
!= e4 )
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk15
| ( ( e4 @ ( e4 @ ( e3 @ op ) @ op ) )
= e3 )
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk15
| ( ( e3 @ ( e4 @ op ) )
!= ( e4 @ ( e3 @ op ) ) )
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk14
| ( ( e3 @ ( e2 @ ( e3 @ op ) @ op ) )
!= e2 )
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk14
| ( ( e2 @ ( e2 @ ( e3 @ op ) @ op ) )
= e3 )
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk14
| ( ( e3 @ ( e2 @ op ) )
!= ( e2 @ ( e3 @ op ) ) )
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk13
| ( ( e3 @ ( e1 @ ( e3 @ op ) @ op ) )
!= e1 )
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk13
| ( ( e1 @ ( e1 @ ( e3 @ op ) @ op ) )
= e3 )
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk13
| ( ( e3 @ ( e1 @ op ) )
!= ( e1 @ ( e3 @ op ) ) )
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk12
| ( ( e3 @ ( e0 @ ( e3 @ op ) @ op ) )
!= e0 )
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk12
| ( ( e0 @ ( e0 @ ( e3 @ op ) @ op ) )
= e3 )
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk12
| ( ( e3 @ ( e0 @ op ) )
!= ( e0 @ ( e3 @ op ) ) )
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk11
| ( ( e2 @ ( e4 @ ( e2 @ op ) @ op ) )
!= e4 )
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk11
| ( ( e4 @ ( e4 @ ( e2 @ op ) @ op ) )
= e2 )
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk11
| ( ( e2 @ ( e4 @ op ) )
!= ( e4 @ ( e2 @ op ) ) )
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk10
| ( ( e2 @ ( e3 @ ( e2 @ op ) @ op ) )
!= e3 )
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk10
| ( ( e3 @ ( e3 @ ( e2 @ op ) @ op ) )
= e2 )
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk10
| ( ( e2 @ ( e3 @ op ) )
!= ( e3 @ ( e2 @ op ) ) )
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk9
| ( ( e2 @ ( e1 @ ( e2 @ op ) @ op ) )
!= e1 )
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk9
| ( ( e1 @ ( e1 @ ( e2 @ op ) @ op ) )
= e2 )
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk9
| ( ( e2 @ ( e1 @ op ) )
!= ( e1 @ ( e2 @ op ) ) )
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk8
| ( ( e2 @ ( e0 @ ( e2 @ op ) @ op ) )
!= e0 )
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk8
| ( ( e0 @ ( e0 @ ( e2 @ op ) @ op ) )
= e2 )
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk8
| ( ( e2 @ ( e0 @ op ) )
!= ( e0 @ ( e2 @ op ) ) )
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk7
| ( ( e1 @ ( e4 @ ( e1 @ op ) @ op ) )
!= e4 )
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk7
| ( ( e4 @ ( e4 @ ( e1 @ op ) @ op ) )
= e1 )
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk7
| ( ( e1 @ ( e4 @ op ) )
!= ( e4 @ ( e1 @ op ) ) )
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk6
| ( ( e1 @ ( e3 @ ( e1 @ op ) @ op ) )
!= e3 )
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk6
| ( ( e3 @ ( e3 @ ( e1 @ op ) @ op ) )
= e1 )
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk6
| ( ( e1 @ ( e3 @ op ) )
!= ( e3 @ ( e1 @ op ) ) )
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk5
| ( ( e1 @ ( e2 @ ( e1 @ op ) @ op ) )
!= e2 )
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk5
| ( ( e2 @ ( e2 @ ( e1 @ op ) @ op ) )
= e1 )
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk5
| ( ( e1 @ ( e2 @ op ) )
!= ( e2 @ ( e1 @ op ) ) )
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk4
| ( ( e1 @ ( e0 @ ( e1 @ op ) @ op ) )
!= e0 )
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk4
| ( ( e0 @ ( e0 @ ( e1 @ op ) @ op ) )
= e1 )
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk4
| ( ( e1 @ ( e0 @ op ) )
!= ( e0 @ ( e1 @ op ) ) )
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk3
| ( ( e0 @ ( e4 @ ( e0 @ op ) @ op ) )
!= e4 )
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk3
| ( ( e4 @ ( e4 @ ( e0 @ op ) @ op ) )
= e0 )
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk3
| ( ( e0 @ ( e4 @ op ) )
!= ( e4 @ ( e0 @ op ) ) )
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk2
| ( ( e0 @ ( e3 @ ( e0 @ op ) @ op ) )
!= e3 )
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk2
| ( ( e3 @ ( e3 @ ( e0 @ op ) @ op ) )
= e0 )
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk2
| ( ( e0 @ ( e3 @ op ) )
!= ( e3 @ ( e0 @ op ) ) )
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk1
| ( ( e0 @ ( e2 @ ( e0 @ op ) @ op ) )
!= e2 )
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk1
| ( ( e2 @ ( e2 @ ( e0 @ op ) @ op ) )
= e0 )
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( sk1
| ( ( e0 @ ( e2 @ op ) )
!= ( e2 @ ( e0 @ op ) ) )
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) )
& ( ( ( e4 @ ( e3 @ ( e4 @ op ) @ op ) )
!= e3 )
| ~ sk18
| ~ sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( ( ( e3 @ ( e3 @ ( e4 @ op ) @ op ) )
= e4 )
| ~ sk18
| ~ sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( ( ( e4 @ ( e3 @ op ) )
!= ( e3 @ ( e4 @ op ) ) )
| ~ sk18
| ~ sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk18
| ( ( e4 @ ( e2 @ ( e4 @ op ) @ op ) )
!= e2 )
| ~ sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk18
| ( ( e2 @ ( e2 @ ( e4 @ op ) @ op ) )
= e4 )
| ~ sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk18
| ( ( e4 @ ( e2 @ op ) )
!= ( e2 @ ( e4 @ op ) ) )
| ~ sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk17
| ( ( e4 @ ( e1 @ ( e4 @ op ) @ op ) )
!= e1 )
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk17
| ( ( e1 @ ( e1 @ ( e4 @ op ) @ op ) )
= e4 )
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk17
| ( ( e4 @ ( e1 @ op ) )
!= ( e1 @ ( e4 @ op ) ) )
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk16
| ( ( e4 @ ( e0 @ ( e4 @ op ) @ op ) )
!= e0 )
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk16
| ( ( e0 @ ( e0 @ ( e4 @ op ) @ op ) )
= e4 )
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk16
| ( ( e4 @ ( e0 @ op ) )
!= ( e0 @ ( e4 @ op ) ) )
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk15
| ( ( e3 @ ( e4 @ ( e3 @ op ) @ op ) )
!= e4 )
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk15
| ( ( e4 @ ( e4 @ ( e3 @ op ) @ op ) )
= e3 )
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk15
| ( ( e3 @ ( e4 @ op ) )
!= ( e4 @ ( e3 @ op ) ) )
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk14
| ( ( e3 @ ( e2 @ ( e3 @ op ) @ op ) )
!= e2 )
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk14
| ( ( e2 @ ( e2 @ ( e3 @ op ) @ op ) )
= e3 )
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk14
| ( ( e3 @ ( e2 @ op ) )
!= ( e2 @ ( e3 @ op ) ) )
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk13
| ( ( e3 @ ( e1 @ ( e3 @ op ) @ op ) )
!= e1 )
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk13
| ( ( e1 @ ( e1 @ ( e3 @ op ) @ op ) )
= e3 )
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk13
| ( ( e3 @ ( e1 @ op ) )
!= ( e1 @ ( e3 @ op ) ) )
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk12
| ( ( e3 @ ( e0 @ ( e3 @ op ) @ op ) )
!= e0 )
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk12
| ( ( e0 @ ( e0 @ ( e3 @ op ) @ op ) )
= e3 )
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk12
| ( ( e3 @ ( e0 @ op ) )
!= ( e0 @ ( e3 @ op ) ) )
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk11
| ( ( e2 @ ( e4 @ ( e2 @ op ) @ op ) )
!= e4 )
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk11
| ( ( e4 @ ( e4 @ ( e2 @ op ) @ op ) )
= e2 )
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk11
| ( ( e2 @ ( e4 @ op ) )
!= ( e4 @ ( e2 @ op ) ) )
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk10
| ( ( e2 @ ( e3 @ ( e2 @ op ) @ op ) )
!= e3 )
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk10
| ( ( e3 @ ( e3 @ ( e2 @ op ) @ op ) )
= e2 )
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk10
| ( ( e2 @ ( e3 @ op ) )
!= ( e3 @ ( e2 @ op ) ) )
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk9
| ( ( e2 @ ( e1 @ ( e2 @ op ) @ op ) )
!= e1 )
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk9
| ( ( e1 @ ( e1 @ ( e2 @ op ) @ op ) )
= e2 )
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk9
| ( ( e2 @ ( e1 @ op ) )
!= ( e1 @ ( e2 @ op ) ) )
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk8
| ( ( e2 @ ( e0 @ ( e2 @ op ) @ op ) )
!= e0 )
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk8
| ( ( e0 @ ( e0 @ ( e2 @ op ) @ op ) )
= e2 )
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk8
| ( ( e2 @ ( e0 @ op ) )
!= ( e0 @ ( e2 @ op ) ) )
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk7
| ( ( e1 @ ( e4 @ ( e1 @ op ) @ op ) )
!= e4 )
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk7
| ( ( e4 @ ( e4 @ ( e1 @ op ) @ op ) )
= e1 )
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk7
| ( ( e1 @ ( e4 @ op ) )
!= ( e4 @ ( e1 @ op ) ) )
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk6
| ( ( e1 @ ( e3 @ ( e1 @ op ) @ op ) )
!= e3 )
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk6
| ( ( e3 @ ( e3 @ ( e1 @ op ) @ op ) )
= e1 )
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk6
| ( ( e1 @ ( e3 @ op ) )
!= ( e3 @ ( e1 @ op ) ) )
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk5
| ( ( e1 @ ( e2 @ ( e1 @ op ) @ op ) )
!= e2 )
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk5
| ( ( e2 @ ( e2 @ ( e1 @ op ) @ op ) )
= e1 )
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk5
| ( ( e1 @ ( e2 @ op ) )
!= ( e2 @ ( e1 @ op ) ) )
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk4
| ( ( e1 @ ( e0 @ ( e1 @ op ) @ op ) )
!= e0 )
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk4
| ( ( e0 @ ( e0 @ ( e1 @ op ) @ op ) )
= e1 )
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk4
| ( ( e1 @ ( e0 @ op ) )
!= ( e0 @ ( e1 @ op ) ) )
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk3
| ( ( e0 @ ( e4 @ ( e0 @ op ) @ op ) )
!= e4 )
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk3
| ( ( e4 @ ( e4 @ ( e0 @ op ) @ op ) )
= e0 )
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk3
| ( ( e0 @ ( e4 @ op ) )
!= ( e4 @ ( e0 @ op ) ) )
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk2
| ( ( e0 @ ( e3 @ ( e0 @ op ) @ op ) )
!= e3 )
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk2
| ( ( e3 @ ( e3 @ ( e0 @ op ) @ op ) )
= e0 )
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk2
| ( ( e0 @ ( e3 @ op ) )
!= ( e3 @ ( e0 @ op ) ) )
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk1
| ( ( e0 @ ( e2 @ ( e0 @ op ) @ op ) )
!= e2 )
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk1
| ( ( e2 @ ( e2 @ ( e0 @ op ) @ op ) )
= e0 )
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( sk1
| ( ( e0 @ ( e2 @ op ) )
!= ( e2 @ ( e0 @ op ) ) )
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) )
& ( ( ( e4 @ ( e4 @ op ) )
= e4 )
| ( ( e3 @ ( e3 @ op ) )
= e4 )
| ( ( e2 @ ( e2 @ op ) )
= e4 )
| ( ( e1 @ ( e1 @ op ) )
= e4 )
| ( ( e0 @ ( e0 @ op ) )
= e4 ) )
& ( ( ( e4 @ ( e4 @ op ) )
= e3 )
| ( ( e3 @ ( e3 @ op ) )
= e3 )
| ( ( e2 @ ( e2 @ op ) )
= e3 )
| ( ( e1 @ ( e1 @ op ) )
= e3 )
| ( ( e0 @ ( e0 @ op ) )
= e3 ) )
& ( ( ( e4 @ ( e4 @ op ) )
= e2 )
| ( ( e3 @ ( e3 @ op ) )
= e2 )
| ( ( e2 @ ( e2 @ op ) )
= e2 )
| ( ( e1 @ ( e1 @ op ) )
= e2 )
| ( ( e0 @ ( e0 @ op ) )
= e2 ) )
& ( ( ( e4 @ ( e4 @ op ) )
= e1 )
| ( ( e3 @ ( e3 @ op ) )
= e1 )
| ( ( e2 @ ( e2 @ op ) )
= e1 )
| ( ( e1 @ ( e1 @ op ) )
= e1 )
| ( ( e0 @ ( e0 @ op ) )
= e1 ) )
& ( ( ( e4 @ ( e4 @ op ) )
= e0 )
| ( ( e3 @ ( e3 @ op ) )
= e0 )
| ( ( e2 @ ( e2 @ op ) )
= e0 )
| ( ( e1 @ ( e1 @ op ) )
= e0 )
| ( ( e0 @ ( e0 @ op ) )
= e0 ) ) ),
inference(cnf,[status(esa)],[10]) ).
thf(162,plain,
( sk8
| ( ( e2 @ ( e0 @ op ) )
!= ( e0 @ ( e2 @ op ) ) )
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) ),
inference(cnfConj,[status(thm)],[11]) ).
thf(303,plain,
( sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e2 @ op ) )
!= ( e2 @ ( e0 @ op ) ) )
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) ),
inference(lifteq,[status(thm)],[162]) ).
thf(4,axiom,
( ( ( unit = e4 )
| ( unit = e3 )
| ( unit = e2 )
| ( unit = e1 )
| ( unit = e0 ) )
& ( ( unit @ ( e4 @ op ) )
= e4 )
& ( ( e4 @ ( unit @ op ) )
= e4 )
& ( ( unit @ ( e3 @ op ) )
= e3 )
& ( ( e3 @ ( unit @ op ) )
= e3 )
& ( ( unit @ ( e2 @ op ) )
= e2 )
& ( ( e2 @ ( unit @ op ) )
= e2 )
& ( ( unit @ ( e1 @ op ) )
= e1 )
& ( ( e1 @ ( unit @ op ) )
= e1 )
& ( ( unit @ ( e0 @ op ) )
= e0 )
& ( ( e0 @ ( unit @ op ) )
= e0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
thf(417,plain,
( ( ( unit = e4 )
| ( unit = e3 )
| ( unit = e2 )
| ( unit = e1 )
| ( unit = e0 ) )
& ( ( unit @ ( e4 @ op ) )
= e4 )
& ( ( e4 @ ( unit @ op ) )
= e4 )
& ( ( unit @ ( e3 @ op ) )
= e3 )
& ( ( e3 @ ( unit @ op ) )
= e3 )
& ( ( unit @ ( e2 @ op ) )
= e2 )
& ( ( e2 @ ( unit @ op ) )
= e2 )
& ( ( unit @ ( e1 @ op ) )
= e1 )
& ( ( e1 @ ( unit @ op ) )
= e1 )
& ( ( unit @ ( e0 @ op ) )
= e0 )
& ( ( e0 @ ( unit @ op ) )
= e0 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(418,plain,
( ( ( unit = e4 )
| ( unit = e3 )
| ( unit = e2 )
| ( unit = e1 )
| ( unit = e0 ) )
& ( ( unit @ ( e4 @ op ) )
= e4 )
& ( ( e4 @ ( unit @ op ) )
= e4 )
& ( ( unit @ ( e3 @ op ) )
= e3 )
& ( ( e3 @ ( unit @ op ) )
= e3 )
& ( ( unit @ ( e2 @ op ) )
= e2 )
& ( ( e2 @ ( unit @ op ) )
= e2 )
& ( ( unit @ ( e1 @ op ) )
= e1 )
& ( ( e1 @ ( unit @ op ) )
= e1 )
& ( ( unit @ ( e0 @ op ) )
= e0 )
& ( ( e0 @ ( unit @ op ) )
= e0 ) ),
inference(cnf,[status(esa)],[417]) ).
thf(424,plain,
( ( e1 @ ( unit @ op ) )
= e1 ),
inference(cnfConj,[status(thm)],[418]) ).
thf(439,plain,
( ( e1 @ ( unit @ op ) )
= e1 ),
inference(lifteq,[status(thm)],[424]) ).
thf(427,plain,
( ( e2 @ ( unit @ op ) )
= e2 ),
inference(cnfConj,[status(thm)],[418]) ).
thf(438,plain,
( ( e2 @ ( unit @ op ) )
= e2 ),
inference(lifteq,[status(thm)],[427]) ).
thf(25,plain,
( sk1
| ( ( e2 @ ( e2 @ ( e0 @ op ) @ op ) )
= e0 )
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) ),
inference(cnfConj,[status(thm)],[11]) ).
thf(203,plain,
( sk1
| ( ( e2 @ ( e2 @ ( e0 @ op ) @ op ) )
= e0 )
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) ),
inference(lifteq,[status(thm)],[25]) ).
thf(6,axiom,
( ( ( e3 @ ( e4 @ op ) )
!= ( e4 @ ( e4 @ op ) ) )
& ( ( e2 @ ( e4 @ op ) )
!= ( e4 @ ( e4 @ op ) ) )
& ( ( e2 @ ( e4 @ op ) )
!= ( e3 @ ( e4 @ op ) ) )
& ( ( e1 @ ( e4 @ op ) )
!= ( e4 @ ( e4 @ op ) ) )
& ( ( e1 @ ( e4 @ op ) )
!= ( e3 @ ( e4 @ op ) ) )
& ( ( e1 @ ( e4 @ op ) )
!= ( e2 @ ( e4 @ op ) ) )
& ( ( e0 @ ( e4 @ op ) )
!= ( e4 @ ( e4 @ op ) ) )
& ( ( e0 @ ( e4 @ op ) )
!= ( e3 @ ( e4 @ op ) ) )
& ( ( e0 @ ( e4 @ op ) )
!= ( e2 @ ( e4 @ op ) ) )
& ( ( e0 @ ( e4 @ op ) )
!= ( e1 @ ( e4 @ op ) ) )
& ( ( e3 @ ( e3 @ op ) )
!= ( e4 @ ( e3 @ op ) ) )
& ( ( e2 @ ( e3 @ op ) )
!= ( e4 @ ( e3 @ op ) ) )
& ( ( e2 @ ( e3 @ op ) )
!= ( e3 @ ( e3 @ op ) ) )
& ( ( e1 @ ( e3 @ op ) )
!= ( e4 @ ( e3 @ op ) ) )
& ( ( e1 @ ( e3 @ op ) )
!= ( e3 @ ( e3 @ op ) ) )
& ( ( e1 @ ( e3 @ op ) )
!= ( e2 @ ( e3 @ op ) ) )
& ( ( e0 @ ( e3 @ op ) )
!= ( e4 @ ( e3 @ op ) ) )
& ( ( e0 @ ( e3 @ op ) )
!= ( e3 @ ( e3 @ op ) ) )
& ( ( e0 @ ( e3 @ op ) )
!= ( e2 @ ( e3 @ op ) ) )
& ( ( e0 @ ( e3 @ op ) )
!= ( e1 @ ( e3 @ op ) ) )
& ( ( e3 @ ( e2 @ op ) )
!= ( e4 @ ( e2 @ op ) ) )
& ( ( e2 @ ( e2 @ op ) )
!= ( e4 @ ( e2 @ op ) ) )
& ( ( e2 @ ( e2 @ op ) )
!= ( e3 @ ( e2 @ op ) ) )
& ( ( e1 @ ( e2 @ op ) )
!= ( e4 @ ( e2 @ op ) ) )
& ( ( e1 @ ( e2 @ op ) )
!= ( e3 @ ( e2 @ op ) ) )
& ( ( e1 @ ( e2 @ op ) )
!= ( e2 @ ( e2 @ op ) ) )
& ( ( e0 @ ( e2 @ op ) )
!= ( e4 @ ( e2 @ op ) ) )
& ( ( e0 @ ( e2 @ op ) )
!= ( e3 @ ( e2 @ op ) ) )
& ( ( e0 @ ( e2 @ op ) )
!= ( e2 @ ( e2 @ op ) ) )
& ( ( e0 @ ( e2 @ op ) )
!= ( e1 @ ( e2 @ op ) ) )
& ( ( e3 @ ( e1 @ op ) )
!= ( e4 @ ( e1 @ op ) ) )
& ( ( e2 @ ( e1 @ op ) )
!= ( e4 @ ( e1 @ op ) ) )
& ( ( e2 @ ( e1 @ op ) )
!= ( e3 @ ( e1 @ op ) ) )
& ( ( e1 @ ( e1 @ op ) )
!= ( e4 @ ( e1 @ op ) ) )
& ( ( e1 @ ( e1 @ op ) )
!= ( e3 @ ( e1 @ op ) ) )
& ( ( e1 @ ( e1 @ op ) )
!= ( e2 @ ( e1 @ op ) ) )
& ( ( e0 @ ( e1 @ op ) )
!= ( e4 @ ( e1 @ op ) ) )
& ( ( e0 @ ( e1 @ op ) )
!= ( e3 @ ( e1 @ op ) ) )
& ( ( e0 @ ( e1 @ op ) )
!= ( e2 @ ( e1 @ op ) ) )
& ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e1 @ op ) ) )
& ( ( e3 @ ( e0 @ op ) )
!= ( e4 @ ( e0 @ op ) ) )
& ( ( e2 @ ( e0 @ op ) )
!= ( e4 @ ( e0 @ op ) ) )
& ( ( e2 @ ( e0 @ op ) )
!= ( e3 @ ( e0 @ op ) ) )
& ( ( e1 @ ( e0 @ op ) )
!= ( e4 @ ( e0 @ op ) ) )
& ( ( e1 @ ( e0 @ op ) )
!= ( e3 @ ( e0 @ op ) ) )
& ( ( e1 @ ( e0 @ op ) )
!= ( e2 @ ( e0 @ op ) ) )
& ( ( e0 @ ( e0 @ op ) )
!= ( e4 @ ( e0 @ op ) ) )
& ( ( e0 @ ( e0 @ op ) )
!= ( e3 @ ( e0 @ op ) ) )
& ( ( e0 @ ( e0 @ op ) )
!= ( e2 @ ( e0 @ op ) ) )
& ( ( e0 @ ( e0 @ op ) )
!= ( e1 @ ( e0 @ op ) ) )
& ( ( e4 @ ( e3 @ op ) )
!= ( e4 @ ( e4 @ op ) ) )
& ( ( e4 @ ( e2 @ op ) )
!= ( e4 @ ( e4 @ op ) ) )
& ( ( e4 @ ( e2 @ op ) )
!= ( e4 @ ( e3 @ op ) ) )
& ( ( e4 @ ( e1 @ op ) )
!= ( e4 @ ( e4 @ op ) ) )
& ( ( e4 @ ( e1 @ op ) )
!= ( e4 @ ( e3 @ op ) ) )
& ( ( e4 @ ( e1 @ op ) )
!= ( e4 @ ( e2 @ op ) ) )
& ( ( e4 @ ( e0 @ op ) )
!= ( e4 @ ( e4 @ op ) ) )
& ( ( e4 @ ( e0 @ op ) )
!= ( e4 @ ( e3 @ op ) ) )
& ( ( e4 @ ( e0 @ op ) )
!= ( e4 @ ( e2 @ op ) ) )
& ( ( e4 @ ( e0 @ op ) )
!= ( e4 @ ( e1 @ op ) ) )
& ( ( e3 @ ( e3 @ op ) )
!= ( e3 @ ( e4 @ op ) ) )
& ( ( e3 @ ( e2 @ op ) )
!= ( e3 @ ( e4 @ op ) ) )
& ( ( e3 @ ( e2 @ op ) )
!= ( e3 @ ( e3 @ op ) ) )
& ( ( e3 @ ( e1 @ op ) )
!= ( e3 @ ( e4 @ op ) ) )
& ( ( e3 @ ( e1 @ op ) )
!= ( e3 @ ( e3 @ op ) ) )
& ( ( e3 @ ( e1 @ op ) )
!= ( e3 @ ( e2 @ op ) ) )
& ( ( e3 @ ( e0 @ op ) )
!= ( e3 @ ( e4 @ op ) ) )
& ( ( e3 @ ( e0 @ op ) )
!= ( e3 @ ( e3 @ op ) ) )
& ( ( e3 @ ( e0 @ op ) )
!= ( e3 @ ( e2 @ op ) ) )
& ( ( e3 @ ( e0 @ op ) )
!= ( e3 @ ( e1 @ op ) ) )
& ( ( e2 @ ( e3 @ op ) )
!= ( e2 @ ( e4 @ op ) ) )
& ( ( e2 @ ( e2 @ op ) )
!= ( e2 @ ( e4 @ op ) ) )
& ( ( e2 @ ( e2 @ op ) )
!= ( e2 @ ( e3 @ op ) ) )
& ( ( e2 @ ( e1 @ op ) )
!= ( e2 @ ( e4 @ op ) ) )
& ( ( e2 @ ( e1 @ op ) )
!= ( e2 @ ( e3 @ op ) ) )
& ( ( e2 @ ( e1 @ op ) )
!= ( e2 @ ( e2 @ op ) ) )
& ( ( e2 @ ( e0 @ op ) )
!= ( e2 @ ( e4 @ op ) ) )
& ( ( e2 @ ( e0 @ op ) )
!= ( e2 @ ( e3 @ op ) ) )
& ( ( e2 @ ( e0 @ op ) )
!= ( e2 @ ( e2 @ op ) ) )
& ( ( e2 @ ( e0 @ op ) )
!= ( e2 @ ( e1 @ op ) ) )
& ( ( e1 @ ( e3 @ op ) )
!= ( e1 @ ( e4 @ op ) ) )
& ( ( e1 @ ( e2 @ op ) )
!= ( e1 @ ( e4 @ op ) ) )
& ( ( e1 @ ( e2 @ op ) )
!= ( e1 @ ( e3 @ op ) ) )
& ( ( e1 @ ( e1 @ op ) )
!= ( e1 @ ( e4 @ op ) ) )
& ( ( e1 @ ( e1 @ op ) )
!= ( e1 @ ( e3 @ op ) ) )
& ( ( e1 @ ( e1 @ op ) )
!= ( e1 @ ( e2 @ op ) ) )
& ( ( e1 @ ( e0 @ op ) )
!= ( e1 @ ( e4 @ op ) ) )
& ( ( e1 @ ( e0 @ op ) )
!= ( e1 @ ( e3 @ op ) ) )
& ( ( e1 @ ( e0 @ op ) )
!= ( e1 @ ( e2 @ op ) ) )
& ( ( e1 @ ( e0 @ op ) )
!= ( e1 @ ( e1 @ op ) ) )
& ( ( e0 @ ( e3 @ op ) )
!= ( e0 @ ( e4 @ op ) ) )
& ( ( e0 @ ( e2 @ op ) )
!= ( e0 @ ( e4 @ op ) ) )
& ( ( e0 @ ( e2 @ op ) )
!= ( e0 @ ( e3 @ op ) ) )
& ( ( e0 @ ( e1 @ op ) )
!= ( e0 @ ( e4 @ op ) ) )
& ( ( e0 @ ( e1 @ op ) )
!= ( e0 @ ( e3 @ op ) ) )
& ( ( e0 @ ( e1 @ op ) )
!= ( e0 @ ( e2 @ op ) ) )
& ( ( e0 @ ( e0 @ op ) )
!= ( e0 @ ( e4 @ op ) ) )
& ( ( e0 @ ( e0 @ op ) )
!= ( e0 @ ( e3 @ op ) ) )
& ( ( e0 @ ( e0 @ op ) )
!= ( e0 @ ( e2 @ op ) ) )
& ( ( e0 @ ( e0 @ op ) )
!= ( e0 @ ( e1 @ op ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
thf(543,plain,
( ( ( e3 @ ( e4 @ op ) )
!= ( e4 @ ( e4 @ op ) ) )
& ( ( e2 @ ( e4 @ op ) )
!= ( e4 @ ( e4 @ op ) ) )
& ( ( e2 @ ( e4 @ op ) )
!= ( e3 @ ( e4 @ op ) ) )
& ( ( e1 @ ( e4 @ op ) )
!= ( e4 @ ( e4 @ op ) ) )
& ( ( e1 @ ( e4 @ op ) )
!= ( e3 @ ( e4 @ op ) ) )
& ( ( e1 @ ( e4 @ op ) )
!= ( e2 @ ( e4 @ op ) ) )
& ( ( e0 @ ( e4 @ op ) )
!= ( e4 @ ( e4 @ op ) ) )
& ( ( e0 @ ( e4 @ op ) )
!= ( e3 @ ( e4 @ op ) ) )
& ( ( e0 @ ( e4 @ op ) )
!= ( e2 @ ( e4 @ op ) ) )
& ( ( e0 @ ( e4 @ op ) )
!= ( e1 @ ( e4 @ op ) ) )
& ( ( e3 @ ( e3 @ op ) )
!= ( e4 @ ( e3 @ op ) ) )
& ( ( e2 @ ( e3 @ op ) )
!= ( e4 @ ( e3 @ op ) ) )
& ( ( e2 @ ( e3 @ op ) )
!= ( e3 @ ( e3 @ op ) ) )
& ( ( e1 @ ( e3 @ op ) )
!= ( e4 @ ( e3 @ op ) ) )
& ( ( e1 @ ( e3 @ op ) )
!= ( e3 @ ( e3 @ op ) ) )
& ( ( e1 @ ( e3 @ op ) )
!= ( e2 @ ( e3 @ op ) ) )
& ( ( e0 @ ( e3 @ op ) )
!= ( e4 @ ( e3 @ op ) ) )
& ( ( e0 @ ( e3 @ op ) )
!= ( e3 @ ( e3 @ op ) ) )
& ( ( e0 @ ( e3 @ op ) )
!= ( e2 @ ( e3 @ op ) ) )
& ( ( e0 @ ( e3 @ op ) )
!= ( e1 @ ( e3 @ op ) ) )
& ( ( e3 @ ( e2 @ op ) )
!= ( e4 @ ( e2 @ op ) ) )
& ( ( e2 @ ( e2 @ op ) )
!= ( e4 @ ( e2 @ op ) ) )
& ( ( e2 @ ( e2 @ op ) )
!= ( e3 @ ( e2 @ op ) ) )
& ( ( e1 @ ( e2 @ op ) )
!= ( e4 @ ( e2 @ op ) ) )
& ( ( e1 @ ( e2 @ op ) )
!= ( e3 @ ( e2 @ op ) ) )
& ( ( e1 @ ( e2 @ op ) )
!= ( e2 @ ( e2 @ op ) ) )
& ( ( e0 @ ( e2 @ op ) )
!= ( e4 @ ( e2 @ op ) ) )
& ( ( e0 @ ( e2 @ op ) )
!= ( e3 @ ( e2 @ op ) ) )
& ( ( e0 @ ( e2 @ op ) )
!= ( e2 @ ( e2 @ op ) ) )
& ( ( e0 @ ( e2 @ op ) )
!= ( e1 @ ( e2 @ op ) ) )
& ( ( e3 @ ( e1 @ op ) )
!= ( e4 @ ( e1 @ op ) ) )
& ( ( e2 @ ( e1 @ op ) )
!= ( e4 @ ( e1 @ op ) ) )
& ( ( e2 @ ( e1 @ op ) )
!= ( e3 @ ( e1 @ op ) ) )
& ( ( e1 @ ( e1 @ op ) )
!= ( e4 @ ( e1 @ op ) ) )
& ( ( e1 @ ( e1 @ op ) )
!= ( e3 @ ( e1 @ op ) ) )
& ( ( e1 @ ( e1 @ op ) )
!= ( e2 @ ( e1 @ op ) ) )
& ( ( e0 @ ( e1 @ op ) )
!= ( e4 @ ( e1 @ op ) ) )
& ( ( e0 @ ( e1 @ op ) )
!= ( e3 @ ( e1 @ op ) ) )
& ( ( e0 @ ( e1 @ op ) )
!= ( e2 @ ( e1 @ op ) ) )
& ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e1 @ op ) ) )
& ( ( e3 @ ( e0 @ op ) )
!= ( e4 @ ( e0 @ op ) ) )
& ( ( e2 @ ( e0 @ op ) )
!= ( e4 @ ( e0 @ op ) ) )
& ( ( e2 @ ( e0 @ op ) )
!= ( e3 @ ( e0 @ op ) ) )
& ( ( e1 @ ( e0 @ op ) )
!= ( e4 @ ( e0 @ op ) ) )
& ( ( e1 @ ( e0 @ op ) )
!= ( e3 @ ( e0 @ op ) ) )
& ( ( e1 @ ( e0 @ op ) )
!= ( e2 @ ( e0 @ op ) ) )
& ( ( e0 @ ( e0 @ op ) )
!= ( e4 @ ( e0 @ op ) ) )
& ( ( e0 @ ( e0 @ op ) )
!= ( e3 @ ( e0 @ op ) ) )
& ( ( e0 @ ( e0 @ op ) )
!= ( e2 @ ( e0 @ op ) ) )
& ( ( e0 @ ( e0 @ op ) )
!= ( e1 @ ( e0 @ op ) ) )
& ( ( e4 @ ( e3 @ op ) )
!= ( e4 @ ( e4 @ op ) ) )
& ( ( e4 @ ( e2 @ op ) )
!= ( e4 @ ( e4 @ op ) ) )
& ( ( e4 @ ( e2 @ op ) )
!= ( e4 @ ( e3 @ op ) ) )
& ( ( e4 @ ( e1 @ op ) )
!= ( e4 @ ( e4 @ op ) ) )
& ( ( e4 @ ( e1 @ op ) )
!= ( e4 @ ( e3 @ op ) ) )
& ( ( e4 @ ( e1 @ op ) )
!= ( e4 @ ( e2 @ op ) ) )
& ( ( e4 @ ( e0 @ op ) )
!= ( e4 @ ( e4 @ op ) ) )
& ( ( e4 @ ( e0 @ op ) )
!= ( e4 @ ( e3 @ op ) ) )
& ( ( e4 @ ( e0 @ op ) )
!= ( e4 @ ( e2 @ op ) ) )
& ( ( e4 @ ( e0 @ op ) )
!= ( e4 @ ( e1 @ op ) ) )
& ( ( e3 @ ( e3 @ op ) )
!= ( e3 @ ( e4 @ op ) ) )
& ( ( e3 @ ( e2 @ op ) )
!= ( e3 @ ( e4 @ op ) ) )
& ( ( e3 @ ( e2 @ op ) )
!= ( e3 @ ( e3 @ op ) ) )
& ( ( e3 @ ( e1 @ op ) )
!= ( e3 @ ( e4 @ op ) ) )
& ( ( e3 @ ( e1 @ op ) )
!= ( e3 @ ( e3 @ op ) ) )
& ( ( e3 @ ( e1 @ op ) )
!= ( e3 @ ( e2 @ op ) ) )
& ( ( e3 @ ( e0 @ op ) )
!= ( e3 @ ( e4 @ op ) ) )
& ( ( e3 @ ( e0 @ op ) )
!= ( e3 @ ( e3 @ op ) ) )
& ( ( e3 @ ( e0 @ op ) )
!= ( e3 @ ( e2 @ op ) ) )
& ( ( e3 @ ( e0 @ op ) )
!= ( e3 @ ( e1 @ op ) ) )
& ( ( e2 @ ( e3 @ op ) )
!= ( e2 @ ( e4 @ op ) ) )
& ( ( e2 @ ( e2 @ op ) )
!= ( e2 @ ( e4 @ op ) ) )
& ( ( e2 @ ( e2 @ op ) )
!= ( e2 @ ( e3 @ op ) ) )
& ( ( e2 @ ( e1 @ op ) )
!= ( e2 @ ( e4 @ op ) ) )
& ( ( e2 @ ( e1 @ op ) )
!= ( e2 @ ( e3 @ op ) ) )
& ( ( e2 @ ( e1 @ op ) )
!= ( e2 @ ( e2 @ op ) ) )
& ( ( e2 @ ( e0 @ op ) )
!= ( e2 @ ( e4 @ op ) ) )
& ( ( e2 @ ( e0 @ op ) )
!= ( e2 @ ( e3 @ op ) ) )
& ( ( e2 @ ( e0 @ op ) )
!= ( e2 @ ( e2 @ op ) ) )
& ( ( e2 @ ( e0 @ op ) )
!= ( e2 @ ( e1 @ op ) ) )
& ( ( e1 @ ( e3 @ op ) )
!= ( e1 @ ( e4 @ op ) ) )
& ( ( e1 @ ( e2 @ op ) )
!= ( e1 @ ( e4 @ op ) ) )
& ( ( e1 @ ( e2 @ op ) )
!= ( e1 @ ( e3 @ op ) ) )
& ( ( e1 @ ( e1 @ op ) )
!= ( e1 @ ( e4 @ op ) ) )
& ( ( e1 @ ( e1 @ op ) )
!= ( e1 @ ( e3 @ op ) ) )
& ( ( e1 @ ( e1 @ op ) )
!= ( e1 @ ( e2 @ op ) ) )
& ( ( e1 @ ( e0 @ op ) )
!= ( e1 @ ( e4 @ op ) ) )
& ( ( e1 @ ( e0 @ op ) )
!= ( e1 @ ( e3 @ op ) ) )
& ( ( e1 @ ( e0 @ op ) )
!= ( e1 @ ( e2 @ op ) ) )
& ( ( e1 @ ( e0 @ op ) )
!= ( e1 @ ( e1 @ op ) ) )
& ( ( e0 @ ( e3 @ op ) )
!= ( e0 @ ( e4 @ op ) ) )
& ( ( e0 @ ( e2 @ op ) )
!= ( e0 @ ( e4 @ op ) ) )
& ( ( e0 @ ( e2 @ op ) )
!= ( e0 @ ( e3 @ op ) ) )
& ( ( e0 @ ( e1 @ op ) )
!= ( e0 @ ( e4 @ op ) ) )
& ( ( e0 @ ( e1 @ op ) )
!= ( e0 @ ( e3 @ op ) ) )
& ( ( e0 @ ( e1 @ op ) )
!= ( e0 @ ( e2 @ op ) ) )
& ( ( e0 @ ( e0 @ op ) )
!= ( e0 @ ( e4 @ op ) ) )
& ( ( e0 @ ( e0 @ op ) )
!= ( e0 @ ( e3 @ op ) ) )
& ( ( e0 @ ( e0 @ op ) )
!= ( e0 @ ( e2 @ op ) ) )
& ( ( e0 @ ( e0 @ op ) )
!= ( e0 @ ( e1 @ op ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(544,plain,
( ( ( e3 @ ( e4 @ op ) )
!= ( e4 @ ( e4 @ op ) ) )
& ( ( e2 @ ( e4 @ op ) )
!= ( e4 @ ( e4 @ op ) ) )
& ( ( e2 @ ( e4 @ op ) )
!= ( e3 @ ( e4 @ op ) ) )
& ( ( e1 @ ( e4 @ op ) )
!= ( e4 @ ( e4 @ op ) ) )
& ( ( e1 @ ( e4 @ op ) )
!= ( e3 @ ( e4 @ op ) ) )
& ( ( e1 @ ( e4 @ op ) )
!= ( e2 @ ( e4 @ op ) ) )
& ( ( e0 @ ( e4 @ op ) )
!= ( e4 @ ( e4 @ op ) ) )
& ( ( e0 @ ( e4 @ op ) )
!= ( e3 @ ( e4 @ op ) ) )
& ( ( e0 @ ( e4 @ op ) )
!= ( e2 @ ( e4 @ op ) ) )
& ( ( e0 @ ( e4 @ op ) )
!= ( e1 @ ( e4 @ op ) ) )
& ( ( e3 @ ( e3 @ op ) )
!= ( e4 @ ( e3 @ op ) ) )
& ( ( e2 @ ( e3 @ op ) )
!= ( e4 @ ( e3 @ op ) ) )
& ( ( e2 @ ( e3 @ op ) )
!= ( e3 @ ( e3 @ op ) ) )
& ( ( e1 @ ( e3 @ op ) )
!= ( e4 @ ( e3 @ op ) ) )
& ( ( e1 @ ( e3 @ op ) )
!= ( e3 @ ( e3 @ op ) ) )
& ( ( e1 @ ( e3 @ op ) )
!= ( e2 @ ( e3 @ op ) ) )
& ( ( e0 @ ( e3 @ op ) )
!= ( e4 @ ( e3 @ op ) ) )
& ( ( e0 @ ( e3 @ op ) )
!= ( e3 @ ( e3 @ op ) ) )
& ( ( e0 @ ( e3 @ op ) )
!= ( e2 @ ( e3 @ op ) ) )
& ( ( e0 @ ( e3 @ op ) )
!= ( e1 @ ( e3 @ op ) ) )
& ( ( e3 @ ( e2 @ op ) )
!= ( e4 @ ( e2 @ op ) ) )
& ( ( e2 @ ( e2 @ op ) )
!= ( e4 @ ( e2 @ op ) ) )
& ( ( e2 @ ( e2 @ op ) )
!= ( e3 @ ( e2 @ op ) ) )
& ( ( e1 @ ( e2 @ op ) )
!= ( e4 @ ( e2 @ op ) ) )
& ( ( e1 @ ( e2 @ op ) )
!= ( e3 @ ( e2 @ op ) ) )
& ( ( e1 @ ( e2 @ op ) )
!= ( e2 @ ( e2 @ op ) ) )
& ( ( e0 @ ( e2 @ op ) )
!= ( e4 @ ( e2 @ op ) ) )
& ( ( e0 @ ( e2 @ op ) )
!= ( e3 @ ( e2 @ op ) ) )
& ( ( e0 @ ( e2 @ op ) )
!= ( e2 @ ( e2 @ op ) ) )
& ( ( e0 @ ( e2 @ op ) )
!= ( e1 @ ( e2 @ op ) ) )
& ( ( e3 @ ( e1 @ op ) )
!= ( e4 @ ( e1 @ op ) ) )
& ( ( e2 @ ( e1 @ op ) )
!= ( e4 @ ( e1 @ op ) ) )
& ( ( e2 @ ( e1 @ op ) )
!= ( e3 @ ( e1 @ op ) ) )
& ( ( e1 @ ( e1 @ op ) )
!= ( e4 @ ( e1 @ op ) ) )
& ( ( e1 @ ( e1 @ op ) )
!= ( e3 @ ( e1 @ op ) ) )
& ( ( e1 @ ( e1 @ op ) )
!= ( e2 @ ( e1 @ op ) ) )
& ( ( e0 @ ( e1 @ op ) )
!= ( e4 @ ( e1 @ op ) ) )
& ( ( e0 @ ( e1 @ op ) )
!= ( e3 @ ( e1 @ op ) ) )
& ( ( e0 @ ( e1 @ op ) )
!= ( e2 @ ( e1 @ op ) ) )
& ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e1 @ op ) ) )
& ( ( e3 @ ( e0 @ op ) )
!= ( e4 @ ( e0 @ op ) ) )
& ( ( e2 @ ( e0 @ op ) )
!= ( e4 @ ( e0 @ op ) ) )
& ( ( e2 @ ( e0 @ op ) )
!= ( e3 @ ( e0 @ op ) ) )
& ( ( e1 @ ( e0 @ op ) )
!= ( e4 @ ( e0 @ op ) ) )
& ( ( e1 @ ( e0 @ op ) )
!= ( e3 @ ( e0 @ op ) ) )
& ( ( e1 @ ( e0 @ op ) )
!= ( e2 @ ( e0 @ op ) ) )
& ( ( e0 @ ( e0 @ op ) )
!= ( e4 @ ( e0 @ op ) ) )
& ( ( e0 @ ( e0 @ op ) )
!= ( e3 @ ( e0 @ op ) ) )
& ( ( e0 @ ( e0 @ op ) )
!= ( e2 @ ( e0 @ op ) ) )
& ( ( e0 @ ( e0 @ op ) )
!= ( e1 @ ( e0 @ op ) ) )
& ( ( e4 @ ( e3 @ op ) )
!= ( e4 @ ( e4 @ op ) ) )
& ( ( e4 @ ( e2 @ op ) )
!= ( e4 @ ( e4 @ op ) ) )
& ( ( e4 @ ( e2 @ op ) )
!= ( e4 @ ( e3 @ op ) ) )
& ( ( e4 @ ( e1 @ op ) )
!= ( e4 @ ( e4 @ op ) ) )
& ( ( e4 @ ( e1 @ op ) )
!= ( e4 @ ( e3 @ op ) ) )
& ( ( e4 @ ( e1 @ op ) )
!= ( e4 @ ( e2 @ op ) ) )
& ( ( e4 @ ( e0 @ op ) )
!= ( e4 @ ( e4 @ op ) ) )
& ( ( e4 @ ( e0 @ op ) )
!= ( e4 @ ( e3 @ op ) ) )
& ( ( e4 @ ( e0 @ op ) )
!= ( e4 @ ( e2 @ op ) ) )
& ( ( e4 @ ( e0 @ op ) )
!= ( e4 @ ( e1 @ op ) ) )
& ( ( e3 @ ( e3 @ op ) )
!= ( e3 @ ( e4 @ op ) ) )
& ( ( e3 @ ( e2 @ op ) )
!= ( e3 @ ( e4 @ op ) ) )
& ( ( e3 @ ( e2 @ op ) )
!= ( e3 @ ( e3 @ op ) ) )
& ( ( e3 @ ( e1 @ op ) )
!= ( e3 @ ( e4 @ op ) ) )
& ( ( e3 @ ( e1 @ op ) )
!= ( e3 @ ( e3 @ op ) ) )
& ( ( e3 @ ( e1 @ op ) )
!= ( e3 @ ( e2 @ op ) ) )
& ( ( e3 @ ( e0 @ op ) )
!= ( e3 @ ( e4 @ op ) ) )
& ( ( e3 @ ( e0 @ op ) )
!= ( e3 @ ( e3 @ op ) ) )
& ( ( e3 @ ( e0 @ op ) )
!= ( e3 @ ( e2 @ op ) ) )
& ( ( e3 @ ( e0 @ op ) )
!= ( e3 @ ( e1 @ op ) ) )
& ( ( e2 @ ( e3 @ op ) )
!= ( e2 @ ( e4 @ op ) ) )
& ( ( e2 @ ( e2 @ op ) )
!= ( e2 @ ( e4 @ op ) ) )
& ( ( e2 @ ( e2 @ op ) )
!= ( e2 @ ( e3 @ op ) ) )
& ( ( e2 @ ( e1 @ op ) )
!= ( e2 @ ( e4 @ op ) ) )
& ( ( e2 @ ( e1 @ op ) )
!= ( e2 @ ( e3 @ op ) ) )
& ( ( e2 @ ( e1 @ op ) )
!= ( e2 @ ( e2 @ op ) ) )
& ( ( e2 @ ( e0 @ op ) )
!= ( e2 @ ( e4 @ op ) ) )
& ( ( e2 @ ( e0 @ op ) )
!= ( e2 @ ( e3 @ op ) ) )
& ( ( e2 @ ( e0 @ op ) )
!= ( e2 @ ( e2 @ op ) ) )
& ( ( e2 @ ( e0 @ op ) )
!= ( e2 @ ( e1 @ op ) ) )
& ( ( e1 @ ( e3 @ op ) )
!= ( e1 @ ( e4 @ op ) ) )
& ( ( e1 @ ( e2 @ op ) )
!= ( e1 @ ( e4 @ op ) ) )
& ( ( e1 @ ( e2 @ op ) )
!= ( e1 @ ( e3 @ op ) ) )
& ( ( e1 @ ( e1 @ op ) )
!= ( e1 @ ( e4 @ op ) ) )
& ( ( e1 @ ( e1 @ op ) )
!= ( e1 @ ( e3 @ op ) ) )
& ( ( e1 @ ( e1 @ op ) )
!= ( e1 @ ( e2 @ op ) ) )
& ( ( e1 @ ( e0 @ op ) )
!= ( e1 @ ( e4 @ op ) ) )
& ( ( e1 @ ( e0 @ op ) )
!= ( e1 @ ( e3 @ op ) ) )
& ( ( e1 @ ( e0 @ op ) )
!= ( e1 @ ( e2 @ op ) ) )
& ( ( e1 @ ( e0 @ op ) )
!= ( e1 @ ( e1 @ op ) ) )
& ( ( e0 @ ( e3 @ op ) )
!= ( e0 @ ( e4 @ op ) ) )
& ( ( e0 @ ( e2 @ op ) )
!= ( e0 @ ( e4 @ op ) ) )
& ( ( e0 @ ( e2 @ op ) )
!= ( e0 @ ( e3 @ op ) ) )
& ( ( e0 @ ( e1 @ op ) )
!= ( e0 @ ( e4 @ op ) ) )
& ( ( e0 @ ( e1 @ op ) )
!= ( e0 @ ( e3 @ op ) ) )
& ( ( e0 @ ( e1 @ op ) )
!= ( e0 @ ( e2 @ op ) ) )
& ( ( e0 @ ( e0 @ op ) )
!= ( e0 @ ( e4 @ op ) ) )
& ( ( e0 @ ( e0 @ op ) )
!= ( e0 @ ( e3 @ op ) ) )
& ( ( e0 @ ( e0 @ op ) )
!= ( e0 @ ( e2 @ op ) ) )
& ( ( e0 @ ( e0 @ op ) )
!= ( e0 @ ( e1 @ op ) ) ) ),
inference(cnf,[status(esa)],[543]) ).
thf(635,plain,
( ( e2 @ ( e1 @ op ) )
!= ( e2 @ ( e2 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(736,plain,
( ( e2 @ ( e2 @ op ) )
!= ( e2 @ ( e1 @ op ) ) ),
inference(lifteq,[status(thm)],[635]) ).
thf(8,axiom,
( ( e4
= ( e1 @ ( e1 @ op ) ) )
& ( e3
= ( e1 @ ( e1 @ op ) @ ( e1 @ ( e1 @ op ) @ op ) @ ( e1 @ ( e1 @ op ) @ ( e1 @ ( e1 @ op ) @ op ) @ op ) ) )
& ( e2
= ( e1 @ ( e1 @ op ) @ ( e1 @ ( e1 @ op ) @ op ) ) )
& ( e0
= ( e1 @ ( e1 @ op ) @ ( e1 @ ( e1 @ op ) @ op ) @ ( e1 @ op ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
thf(767,plain,
( ( e4
= ( e1 @ ( e1 @ op ) ) )
& ( e3
= ( e1 @ ( e1 @ op ) @ ( e1 @ ( e1 @ op ) @ op ) @ ( e1 @ ( e1 @ op ) @ ( e1 @ ( e1 @ op ) @ op ) @ op ) ) )
& ( e2
= ( e1 @ ( e1 @ op ) @ ( e1 @ ( e1 @ op ) @ op ) ) )
& ( e0
= ( e1 @ ( e1 @ op ) @ ( e1 @ ( e1 @ op ) @ op ) @ ( e1 @ op ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(768,plain,
( ( e4
= ( e1 @ ( e1 @ op ) ) )
& ( e3
= ( e1 @ ( e1 @ op ) @ ( e1 @ ( e1 @ op ) @ op ) @ ( e1 @ ( e1 @ op ) @ ( e1 @ ( e1 @ op ) @ op ) @ op ) ) )
& ( e2
= ( e1 @ ( e1 @ op ) @ ( e1 @ ( e1 @ op ) @ op ) ) )
& ( e0
= ( e1 @ ( e1 @ op ) @ ( e1 @ ( e1 @ op ) @ op ) @ ( e1 @ op ) ) ) ),
inference(cnf,[status(esa)],[767]) ).
thf(770,plain,
( e2
= ( e1 @ ( e1 @ op ) @ ( e1 @ ( e1 @ op ) @ op ) ) ),
inference(cnfConj,[status(thm)],[768]) ).
thf(774,plain,
( ( e1 @ ( e1 @ op ) @ ( e1 @ ( e1 @ op ) @ op ) )
= e2 ),
inference(lifteq,[status(thm)],[770]) ).
thf(772,plain,
( e4
= ( e1 @ ( e1 @ op ) ) ),
inference(cnfConj,[status(thm)],[768]) ).
thf(776,plain,
( ( e1 @ ( e1 @ op ) )
= e4 ),
inference(lifteq,[status(thm)],[772]) ).
thf(1627,plain,
( ( e4 @ ( e4 @ op ) )
= e2 ),
inference(rewrite,[status(thm)],[774,776]) ).
thf(769,plain,
( e0
= ( e1 @ ( e1 @ op ) @ ( e1 @ ( e1 @ op ) @ op ) @ ( e1 @ op ) ) ),
inference(cnfConj,[status(thm)],[768]) ).
thf(773,plain,
( ( e1 @ ( e1 @ op ) @ ( e1 @ ( e1 @ op ) @ op ) @ ( e1 @ op ) )
= e0 ),
inference(lifteq,[status(thm)],[769]) ).
thf(2300,plain,
( ( e4 @ ( e4 @ op ) @ ( e1 @ op ) )
= e0 ),
inference(rewrite,[status(thm)],[773,776]) ).
thf(2352,plain,
( ( ( e4 @ ( e4 @ op ) )
!= ( e4 @ ( e4 @ op ) ) )
| ( ( e2 @ ( e1 @ op ) )
= e0 ) ),
inference(paramod_ordered,[status(thm)],[1627,2300]) ).
thf(2353,plain,
( ( e2 @ ( e1 @ op ) )
= e0 ),
inference(pattern_uni,[status(thm)],[2352:[]]) ).
thf(20404,plain,
( ( e2 @ ( e2 @ op ) )
!= e0 ),
inference(rewrite,[status(thm)],[736,2353]) ).
thf(20435,plain,
( ( ( e2 @ ( e2 @ ( e0 @ op ) @ op ) )
!= ( e2 @ ( e2 @ op ) ) )
| ( e0 != e0 )
| sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) ),
inference(paramod_ordered,[status(thm)],[203,20404]) ).
thf(20436,plain,
( ( ( e2 @ ( e2 @ ( e0 @ op ) @ op ) )
!= ( e2 @ ( e2 @ op ) ) )
| sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) ),
inference(simp,[status(thm)],[20435]) ).
thf(20489,plain,
( ( e2 != e2 )
| ( ( e2 @ ( e0 @ op ) )
!= e2 )
| sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) ),
inference(simp,[status(thm)],[20436]) ).
thf(20493,plain,
( ( ( e2 @ ( e0 @ op ) )
!= e2 )
| sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) ),
inference(simp,[status(thm)],[20489]) ).
thf(28931,plain,
( ( ( e2 @ ( unit @ op ) )
!= ( e2 @ ( e0 @ op ) ) )
| ( e2 != e2 )
| sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) ),
inference(paramod_ordered,[status(thm)],[438,20493]) ).
thf(28932,plain,
( ( ( e2 @ ( unit @ op ) )
!= ( e2 @ ( e0 @ op ) ) )
| sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) ),
inference(simp,[status(thm)],[28931]) ).
thf(29087,plain,
( ( e2 != e2 )
| ( unit != e0 )
| sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) ),
inference(simp,[status(thm)],[28932]) ).
thf(29305,plain,
( ( unit != e0 )
| sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) ),
inference(simp,[status(thm)],[29087]) ).
thf(29760,plain,
( ( ( e1 @ ( unit @ op ) )
!= ( e1 @ ( e0 @ op ) ) )
| ( unit != e0 )
| sk1
| ( ( e1 @ ( e1 @ op ) )
= e0 ) ),
inference(paramod_ordered,[status(thm)],[439,29305]) ).
thf(30087,plain,
( ( e1 != e1 )
| ( unit != e0 )
| ( unit != e0 )
| sk1
| ( ( e1 @ ( e1 @ op ) )
= e0 ) ),
inference(simp,[status(thm)],[29760]) ).
thf(30222,plain,
( ( unit != e0 )
| sk1
| ( ( e1 @ ( e1 @ op ) )
= e0 ) ),
inference(simp,[status(thm)],[30087]) ).
thf(30251,plain,
( ( unit != e0 )
| sk1
| ( e4 = e0 ) ),
inference(rewrite,[status(thm)],[30222,776]) ).
thf(7,axiom,
( ( e3 != e4 )
& ( e2 != e4 )
& ( e2 != e3 )
& ( e1 != e4 )
& ( e1 != e3 )
& ( e1 != e2 )
& ( e0 != e4 )
& ( e0 != e3 )
& ( e0 != e2 )
& ( e0 != e1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
thf(745,plain,
( ( e3 != e4 )
& ( e2 != e4 )
& ( e2 != e3 )
& ( e1 != e4 )
& ( e1 != e3 )
& ( e1 != e2 )
& ( e0 != e4 )
& ( e0 != e3 )
& ( e0 != e2 )
& ( e0 != e1 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(746,plain,
( ( e3 != e4 )
& ( e2 != e4 )
& ( e2 != e3 )
& ( e1 != e4 )
& ( e1 != e3 )
& ( e1 != e2 )
& ( e0 != e4 )
& ( e0 != e3 )
& ( e0 != e2 )
& ( e0 != e1 ) ),
inference(cnf,[status(esa)],[745]) ).
thf(749,plain,
e0 != e4,
inference(cnfConj,[status(thm)],[746]) ).
thf(765,plain,
e4 != e0,
inference(lifteq,[status(thm)],[749]) ).
thf(30252,plain,
( ( unit != e0 )
| sk1 ),
inference(simplifyReflect,[status(thm)],[30251,765]) ).
thf(420,plain,
( ( unit @ ( e1 @ op ) )
= e1 ),
inference(cnfConj,[status(thm)],[418]) ).
thf(432,plain,
( ( unit @ ( e1 @ op ) )
= e1 ),
inference(lifteq,[status(thm)],[420]) ).
thf(160,plain,
( sk4
| ( ( e1 @ ( e0 @ op ) )
!= ( e0 @ ( e1 @ op ) ) )
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) ),
inference(cnfConj,[status(thm)],[11]) ).
thf(233,plain,
( sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) )
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) ),
inference(lifteq,[status(thm)],[160]) ).
thf(234,plain,
( sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) ),
inference(simp,[status(thm)],[233]) ).
thf(874,plain,
( ( ( unit @ ( e1 @ op ) )
!= ( e0 @ ( e1 @ op ) ) )
| sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e0 @ op ) )
!= e1 ) ),
inference(paramod_ordered,[status(thm)],[432,234]) ).
thf(888,plain,
( ( unit != e0 )
| ( e1 != e1 )
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e0 @ op ) )
!= e1 )
| sk4 ),
inference(simp,[status(thm)],[874]) ).
thf(900,plain,
( ( unit != e0 )
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e0 @ op ) )
!= e1 )
| sk4 ),
inference(simp,[status(thm)],[888]) ).
thf(1328,plain,
( ( ( e1 @ ( unit @ op ) )
!= ( e1 @ ( e0 @ op ) ) )
| ( unit != e0 )
| ~ sk3
| ~ sk2
| ~ sk1
| ( e1 != e1 )
| sk4 ),
inference(paramod_ordered,[status(thm)],[439,900]) ).
thf(1329,plain,
( ( ( e1 @ ( unit @ op ) )
!= ( e1 @ ( e0 @ op ) ) )
| ( unit != e0 )
| ~ sk3
| ~ sk2
| ~ sk1
| sk4 ),
inference(simp,[status(thm)],[1328]) ).
thf(1348,plain,
( ( e1 != e1 )
| ( unit != e0 )
| ( unit != e0 )
| ~ sk3
| ~ sk2
| ~ sk1
| sk4 ),
inference(simp,[status(thm)],[1329]) ).
thf(1378,plain,
( ( unit != e0 )
| ~ sk3
| ~ sk2
| ~ sk1
| sk4 ),
inference(simp,[status(thm)],[1348]) ).
thf(30351,plain,
( ( sk1 != sk1 )
| ( unit != e0 )
| ~ sk3
| ~ sk2
| ~ $true
| sk4
| ( unit != e0 ) ),
inference(paramod_ordered,[status(thm)],[30252,1378]) ).
thf(30352,plain,
( ( sk1 != sk1 )
| ~ sk3
| ~ sk2
| sk4
| ( unit != e0 ) ),
inference(simp,[status(thm)],[30351]) ).
thf(30353,plain,
( ~ sk3
| ~ sk2
| sk4
| ( unit != e0 ) ),
inference(pattern_uni,[status(thm)],[30352:[]]) ).
thf(51,plain,
( ( ( e4 @ ( e4 @ op ) )
= e1 )
| ( ( e3 @ ( e3 @ op ) )
= e1 )
| ( ( e2 @ ( e2 @ op ) )
= e1 )
| ( ( e1 @ ( e1 @ op ) )
= e1 )
| ( ( e0 @ ( e0 @ op ) )
= e1 ) ),
inference(cnfConj,[status(thm)],[11]) ).
thf(345,plain,
( ( ( e4 @ ( e4 @ op ) )
= e1 )
| ( ( e3 @ ( e3 @ op ) )
= e1 )
| ( ( e2 @ ( e2 @ op ) )
= e1 )
| ( ( e1 @ ( e1 @ op ) )
= e1 )
| ( ( e0 @ ( e0 @ op ) )
= e1 ) ),
inference(lifteq,[status(thm)],[51]) ).
thf(771,plain,
( e3
= ( e1 @ ( e1 @ op ) @ ( e1 @ ( e1 @ op ) @ op ) @ ( e1 @ ( e1 @ op ) @ ( e1 @ ( e1 @ op ) @ op ) @ op ) ) ),
inference(cnfConj,[status(thm)],[768]) ).
thf(775,plain,
( ( e1 @ ( e1 @ op ) @ ( e1 @ ( e1 @ op ) @ op ) @ ( e1 @ ( e1 @ op ) @ ( e1 @ ( e1 @ op ) @ op ) @ op ) )
= e3 ),
inference(lifteq,[status(thm)],[771]) ).
thf(21493,plain,
( ( e4 @ ( e4 @ op ) @ ( e4 @ ( e4 @ op ) @ op ) )
= e3 ),
inference(rewrite,[status(thm)],[775,776]) ).
thf(21614,plain,
( ( ( e4 @ ( e4 @ op ) )
!= ( e4 @ ( e4 @ op ) ) )
| ( ( e4 @ ( e4 @ op ) @ ( e2 @ op ) )
= e3 ) ),
inference(paramod_ordered,[status(thm)],[1627,21493]) ).
thf(21615,plain,
( ( e4 @ ( e4 @ op ) @ ( e2 @ op ) )
= e3 ),
inference(pattern_uni,[status(thm)],[21614:[]]) ).
thf(22275,plain,
( ( e2 @ ( e2 @ op ) )
= e3 ),
inference(rewrite,[status(thm)],[21615,1627]) ).
thf(46998,plain,
( ( e2 = e1 )
| ( ( e3 @ ( e3 @ op ) )
= e1 )
| ( e3 = e1 )
| ( e4 = e1 )
| ( ( e0 @ ( e0 @ op ) )
= e1 ) ),
inference(rewrite,[status(thm)],[345,22275,776,1627]) ).
thf(751,plain,
e1 != e4,
inference(cnfConj,[status(thm)],[746]) ).
thf(758,plain,
e4 != e1,
inference(lifteq,[status(thm)],[751]) ).
thf(750,plain,
e1 != e2,
inference(cnfConj,[status(thm)],[746]) ).
thf(761,plain,
e2 != e1,
inference(lifteq,[status(thm)],[750]) ).
thf(748,plain,
e1 != e3,
inference(cnfConj,[status(thm)],[746]) ).
thf(762,plain,
e3 != e1,
inference(lifteq,[status(thm)],[748]) ).
thf(46999,plain,
( ( ( e3 @ ( e3 @ op ) )
= e1 )
| ( ( e0 @ ( e0 @ op ) )
= e1 ) ),
inference(simplifyReflect,[status(thm)],[46998,758,761,762]) ).
thf(425,plain,
( ( unit = e4 )
| ( unit = e3 )
| ( unit = e2 )
| ( unit = e1 )
| ( unit = e0 ) ),
inference(cnfConj,[status(thm)],[418]) ).
thf(433,plain,
( ( unit = e4 )
| ( unit = e3 )
| ( unit = e2 )
| ( unit = e1 )
| ( unit = e0 ) ),
inference(lifteq,[status(thm)],[425]) ).
thf(429,plain,
( ( e0 @ ( unit @ op ) )
= e0 ),
inference(cnfConj,[status(thm)],[418]) ).
thf(440,plain,
( ( e0 @ ( unit @ op ) )
= e0 ),
inference(lifteq,[status(thm)],[429]) ).
thf(614,plain,
( ( e0 @ ( e1 @ op ) )
!= ( e2 @ ( e1 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(652,plain,
( ( e2 @ ( e1 @ op ) )
!= ( e0 @ ( e1 @ op ) ) ),
inference(lifteq,[status(thm)],[614]) ).
thf(2602,plain,
( ( e0 @ ( e1 @ op ) )
!= e0 ),
inference(rewrite,[status(thm)],[652,2353]) ).
thf(2792,plain,
( ( ( e0 @ ( unit @ op ) )
!= ( e0 @ ( e1 @ op ) ) )
| ( e0 != e0 ) ),
inference(paramod_ordered,[status(thm)],[440,2602]) ).
thf(2793,plain,
( ( e0 @ ( unit @ op ) )
!= ( e0 @ ( e1 @ op ) ) ),
inference(simp,[status(thm)],[2792]) ).
thf(2814,plain,
( ( e0 != e0 )
| ( unit != e1 ) ),
inference(simp,[status(thm)],[2793]) ).
thf(2833,plain,
unit != e1,
inference(simp,[status(thm)],[2814]) ).
thf(2834,plain,
( ( unit = e4 )
| ( unit = e3 )
| ( unit = e2 )
| ( unit = e0 ) ),
inference(simplifyReflect,[status(thm)],[433,2833]) ).
thf(422,plain,
( ( unit @ ( e0 @ op ) )
= e0 ),
inference(cnfConj,[status(thm)],[418]) ).
thf(437,plain,
( ( unit @ ( e0 @ op ) )
= e0 ),
inference(lifteq,[status(thm)],[422]) ).
thf(591,plain,
( ( e2 @ ( e0 @ op ) )
!= ( e2 @ ( e1 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(660,plain,
( ( e2 @ ( e1 @ op ) )
!= ( e2 @ ( e0 @ op ) ) ),
inference(lifteq,[status(thm)],[591]) ).
thf(3116,plain,
( ( e2 @ ( e0 @ op ) )
!= e0 ),
inference(rewrite,[status(thm)],[660,2353]) ).
thf(3118,plain,
( ( ( unit @ ( e0 @ op ) )
!= ( e2 @ ( e0 @ op ) ) )
| ( e0 != e0 ) ),
inference(paramod_ordered,[status(thm)],[437,3116]) ).
thf(3119,plain,
( ( unit @ ( e0 @ op ) )
!= ( e2 @ ( e0 @ op ) ) ),
inference(simp,[status(thm)],[3118]) ).
thf(3150,plain,
( ( unit != e2 )
| ( e0 != e0 ) ),
inference(simp,[status(thm)],[3119]) ).
thf(3160,plain,
unit != e2,
inference(simp,[status(thm)],[3150]) ).
thf(3161,plain,
( ( unit = e4 )
| ( unit = e3 )
| ( unit = e0 ) ),
inference(simplifyReflect,[status(thm)],[2834,3160]) ).
thf(426,plain,
( ( e4 @ ( unit @ op ) )
= e4 ),
inference(cnfConj,[status(thm)],[418]) ).
thf(436,plain,
( ( e4 @ ( unit @ op ) )
= e4 ),
inference(lifteq,[status(thm)],[426]) ).
thf(3166,plain,
( ( unit != unit )
| ( ( e4 @ ( e4 @ op ) )
= e4 )
| ( unit = e3 )
| ( unit = e0 ) ),
inference(paramod_ordered,[status(thm)],[3161,436]) ).
thf(3167,plain,
( ( ( e4 @ ( e4 @ op ) )
= e4 )
| ( unit = e3 )
| ( unit = e0 ) ),
inference(pattern_uni,[status(thm)],[3166:[]]) ).
thf(4823,plain,
( ( e4 = e2 )
| ( unit = e3 )
| ( unit = e0 ) ),
inference(rewrite,[status(thm)],[3167,1627]) ).
thf(755,plain,
e2 != e4,
inference(cnfConj,[status(thm)],[746]) ).
thf(764,plain,
e4 != e2,
inference(lifteq,[status(thm)],[755]) ).
thf(4824,plain,
( ( unit = e3 )
| ( unit = e0 ) ),
inference(simplifyReflect,[status(thm)],[4823,764]) ).
thf(419,plain,
( ( e3 @ ( unit @ op ) )
= e3 ),
inference(cnfConj,[status(thm)],[418]) ).
thf(435,plain,
( ( e3 @ ( unit @ op ) )
= e3 ),
inference(lifteq,[status(thm)],[419]) ).
thf(4833,plain,
( ( unit != unit )
| ( ( e3 @ ( e3 @ op ) )
= e3 )
| ( unit = e0 ) ),
inference(paramod_ordered,[status(thm)],[4824,435]) ).
thf(4834,plain,
( ( ( e3 @ ( e3 @ op ) )
= e3 )
| ( unit = e0 ) ),
inference(pattern_uni,[status(thm)],[4833:[]]) ).
thf(47314,plain,
( ( ( e3 @ ( e3 @ op ) )
!= ( e3 @ ( e3 @ op ) ) )
| ( e3 = e1 )
| ( unit = e0 )
| ( ( e0 @ ( e0 @ op ) )
= e1 ) ),
inference(paramod_ordered,[status(thm)],[46999,4834]) ).
thf(47315,plain,
( ( e3 = e1 )
| ( unit = e0 )
| ( ( e0 @ ( e0 @ op ) )
= e1 ) ),
inference(pattern_uni,[status(thm)],[47314:[]]) ).
thf(48457,plain,
( ( unit = e0 )
| ( ( e0 @ ( e0 @ op ) )
= e1 ) ),
inference(simplifyReflect,[status(thm)],[47315,762]) ).
thf(64,plain,
( ( ( e4 @ ( e4 @ op ) )
= e0 )
| ( ( e3 @ ( e3 @ op ) )
= e0 )
| ( ( e2 @ ( e2 @ op ) )
= e0 )
| ( ( e1 @ ( e1 @ op ) )
= e0 )
| ( ( e0 @ ( e0 @ op ) )
= e0 ) ),
inference(cnfConj,[status(thm)],[11]) ).
thf(265,plain,
( ( ( e4 @ ( e4 @ op ) )
= e0 )
| ( ( e3 @ ( e3 @ op ) )
= e0 )
| ( ( e2 @ ( e2 @ op ) )
= e0 )
| ( ( e1 @ ( e1 @ op ) )
= e0 )
| ( ( e0 @ ( e0 @ op ) )
= e0 ) ),
inference(lifteq,[status(thm)],[64]) ).
thf(41114,plain,
( ( e2 = e0 )
| ( ( e3 @ ( e3 @ op ) )
= e0 )
| ( e3 = e0 )
| ( e4 = e0 )
| ( ( e0 @ ( e0 @ op ) )
= e0 ) ),
inference(rewrite,[status(thm)],[265,22275,776,1627]) ).
thf(747,plain,
e0 != e2,
inference(cnfConj,[status(thm)],[746]) ).
thf(757,plain,
e2 != e0,
inference(lifteq,[status(thm)],[747]) ).
thf(754,plain,
e0 != e3,
inference(cnfConj,[status(thm)],[746]) ).
thf(766,plain,
e3 != e0,
inference(lifteq,[status(thm)],[754]) ).
thf(41115,plain,
( ( ( e3 @ ( e3 @ op ) )
= e0 )
| ( ( e0 @ ( e0 @ op ) )
= e0 ) ),
inference(simplifyReflect,[status(thm)],[41114,757,765,766]) ).
thf(41413,plain,
( ( ( e3 @ ( e3 @ op ) )
!= ( e3 @ ( e3 @ op ) ) )
| ( e3 = e0 )
| ( unit = e0 )
| ( ( e0 @ ( e0 @ op ) )
= e0 ) ),
inference(paramod_ordered,[status(thm)],[41115,4834]) ).
thf(41414,plain,
( ( e3 = e0 )
| ( unit = e0 )
| ( ( e0 @ ( e0 @ op ) )
= e0 ) ),
inference(pattern_uni,[status(thm)],[41413:[]]) ).
thf(43458,plain,
( ( unit = e0 )
| ( ( e0 @ ( e0 @ op ) )
= e0 ) ),
inference(simplifyReflect,[status(thm)],[41414,766]) ).
thf(48641,plain,
( ( ( e0 @ ( e0 @ op ) )
!= ( e0 @ ( e0 @ op ) ) )
| ( unit = e0 )
| ( e1 = e0 )
| ( unit = e0 ) ),
inference(paramod_ordered,[status(thm)],[48457,43458]) ).
thf(48642,plain,
( ( ( e0 @ ( e0 @ op ) )
!= ( e0 @ ( e0 @ op ) ) )
| ( e1 = e0 )
| ( unit = e0 ) ),
inference(simp,[status(thm)],[48641]) ).
thf(48643,plain,
( ( e1 = e0 )
| ( unit = e0 ) ),
inference(pattern_uni,[status(thm)],[48642:[]]) ).
thf(753,plain,
e0 != e1,
inference(cnfConj,[status(thm)],[746]) ).
thf(760,plain,
e1 != e0,
inference(lifteq,[status(thm)],[753]) ).
thf(49564,plain,
unit = e0,
inference(simplifyReflect,[status(thm)],[48643,760]) ).
thf(49565,plain,
( ~ sk3
| ~ sk2
| sk4
| ( e0 != e0 ) ),
inference(rewrite,[status(thm)],[30353,49564]) ).
thf(49566,plain,
( ~ sk3
| ~ sk2
| sk4 ),
inference(simp,[status(thm)],[49565]) ).
thf(428,plain,
( ( unit @ ( e3 @ op ) )
= e3 ),
inference(cnfConj,[status(thm)],[418]) ).
thf(431,plain,
( ( unit @ ( e3 @ op ) )
= e3 ),
inference(lifteq,[status(thm)],[428]) ).
thf(49579,plain,
( ( e0 @ ( e3 @ op ) )
= e3 ),
inference(rewrite,[status(thm)],[431,49564]) ).
thf(141,plain,
( sk2
| ( ( e0 @ ( e3 @ ( e0 @ op ) @ op ) )
!= e3 )
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) ),
inference(cnfConj,[status(thm)],[11]) ).
thf(248,plain,
( sk2
| ~ sk1
| ( ( e0 @ ( e3 @ ( e0 @ op ) @ op ) )
!= e3 )
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) ),
inference(lifteq,[status(thm)],[141]) ).
thf(49570,plain,
( ( e1 @ ( e0 @ op ) )
= e1 ),
inference(rewrite,[status(thm)],[439,49564]) ).
thf(49571,plain,
( ( e0 != e0 )
| sk1 ),
inference(rewrite,[status(thm)],[30252,49564]) ).
thf(49572,plain,
sk1,
inference(simp,[status(thm)],[49571]) ).
thf(49573,plain,
( ( e3 @ ( e0 @ op ) )
= e3 ),
inference(rewrite,[status(thm)],[435,49564]) ).
thf(49580,plain,
( ( e0 @ ( e1 @ op ) )
= e1 ),
inference(rewrite,[status(thm)],[432,49564]) ).
thf(52259,plain,
( sk2
| ~ $true
| ( ( e0 @ ( e3 @ op ) )
!= e3 )
| ( e1 != e1 ) ),
inference(rewrite,[status(thm)],[248,49570,49572,49573,49580]) ).
thf(52260,plain,
( sk2
| ( ( e0 @ ( e3 @ op ) )
!= e3 ) ),
inference(simp,[status(thm)],[52259]) ).
thf(52263,plain,
( ( ( e0 @ ( e3 @ op ) )
!= ( e0 @ ( e3 @ op ) ) )
| sk2
| ( e3 != e3 ) ),
inference(paramod_ordered,[status(thm)],[49579,52260]) ).
thf(52264,plain,
( ( ( e0 @ ( e3 @ op ) )
!= ( e0 @ ( e3 @ op ) ) )
| sk2 ),
inference(simp,[status(thm)],[52263]) ).
thf(52265,plain,
sk2,
inference(pattern_uni,[status(thm)],[52264:[]]) ).
thf(52305,plain,
( ~ sk3
| ~ $true
| sk4 ),
inference(rewrite,[status(thm)],[49566,52265]) ).
thf(52306,plain,
( ~ sk3
| sk4 ),
inference(simp,[status(thm)],[52305]) ).
thf(81,plain,
( sk5
| ( ( e1 @ ( e2 @ op ) )
!= ( e2 @ ( e1 @ op ) ) )
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) ),
inference(cnfConj,[status(thm)],[11]) ).
thf(288,plain,
( sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e2 @ op ) )
!= ( e2 @ ( e1 @ op ) ) )
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) ),
inference(lifteq,[status(thm)],[81]) ).
thf(3,axiom,
( ( ( ( e4 @ ( e4 @ op ) )
= e4 )
| ( ( e4 @ ( e4 @ op ) )
= e3 )
| ( ( e4 @ ( e4 @ op ) )
= e2 )
| ( ( e4 @ ( e4 @ op ) )
= e1 )
| ( ( e4 @ ( e4 @ op ) )
= e0 ) )
& ( ( ( e3 @ ( e4 @ op ) )
= e4 )
| ( ( e3 @ ( e4 @ op ) )
= e3 )
| ( ( e3 @ ( e4 @ op ) )
= e2 )
| ( ( e3 @ ( e4 @ op ) )
= e1 )
| ( ( e3 @ ( e4 @ op ) )
= e0 ) )
& ( ( ( e2 @ ( e4 @ op ) )
= e4 )
| ( ( e2 @ ( e4 @ op ) )
= e3 )
| ( ( e2 @ ( e4 @ op ) )
= e2 )
| ( ( e2 @ ( e4 @ op ) )
= e1 )
| ( ( e2 @ ( e4 @ op ) )
= e0 ) )
& ( ( ( e1 @ ( e4 @ op ) )
= e4 )
| ( ( e1 @ ( e4 @ op ) )
= e3 )
| ( ( e1 @ ( e4 @ op ) )
= e2 )
| ( ( e1 @ ( e4 @ op ) )
= e1 )
| ( ( e1 @ ( e4 @ op ) )
= e0 ) )
& ( ( ( e0 @ ( e4 @ op ) )
= e4 )
| ( ( e0 @ ( e4 @ op ) )
= e3 )
| ( ( e0 @ ( e4 @ op ) )
= e2 )
| ( ( e0 @ ( e4 @ op ) )
= e1 )
| ( ( e0 @ ( e4 @ op ) )
= e0 ) )
& ( ( ( e4 @ ( e3 @ op ) )
= e4 )
| ( ( e4 @ ( e3 @ op ) )
= e3 )
| ( ( e4 @ ( e3 @ op ) )
= e2 )
| ( ( e4 @ ( e3 @ op ) )
= e1 )
| ( ( e4 @ ( e3 @ op ) )
= e0 ) )
& ( ( ( e3 @ ( e3 @ op ) )
= e4 )
| ( ( e3 @ ( e3 @ op ) )
= e3 )
| ( ( e3 @ ( e3 @ op ) )
= e2 )
| ( ( e3 @ ( e3 @ op ) )
= e1 )
| ( ( e3 @ ( e3 @ op ) )
= e0 ) )
& ( ( ( e2 @ ( e3 @ op ) )
= e4 )
| ( ( e2 @ ( e3 @ op ) )
= e3 )
| ( ( e2 @ ( e3 @ op ) )
= e2 )
| ( ( e2 @ ( e3 @ op ) )
= e1 )
| ( ( e2 @ ( e3 @ op ) )
= e0 ) )
& ( ( ( e1 @ ( e3 @ op ) )
= e4 )
| ( ( e1 @ ( e3 @ op ) )
= e3 )
| ( ( e1 @ ( e3 @ op ) )
= e2 )
| ( ( e1 @ ( e3 @ op ) )
= e1 )
| ( ( e1 @ ( e3 @ op ) )
= e0 ) )
& ( ( ( e0 @ ( e3 @ op ) )
= e4 )
| ( ( e0 @ ( e3 @ op ) )
= e3 )
| ( ( e0 @ ( e3 @ op ) )
= e2 )
| ( ( e0 @ ( e3 @ op ) )
= e1 )
| ( ( e0 @ ( e3 @ op ) )
= e0 ) )
& ( ( ( e4 @ ( e2 @ op ) )
= e4 )
| ( ( e4 @ ( e2 @ op ) )
= e3 )
| ( ( e4 @ ( e2 @ op ) )
= e2 )
| ( ( e4 @ ( e2 @ op ) )
= e1 )
| ( ( e4 @ ( e2 @ op ) )
= e0 ) )
& ( ( ( e3 @ ( e2 @ op ) )
= e4 )
| ( ( e3 @ ( e2 @ op ) )
= e3 )
| ( ( e3 @ ( e2 @ op ) )
= e2 )
| ( ( e3 @ ( e2 @ op ) )
= e1 )
| ( ( e3 @ ( e2 @ op ) )
= e0 ) )
& ( ( ( e2 @ ( e2 @ op ) )
= e4 )
| ( ( e2 @ ( e2 @ op ) )
= e3 )
| ( ( e2 @ ( e2 @ op ) )
= e2 )
| ( ( e2 @ ( e2 @ op ) )
= e1 )
| ( ( e2 @ ( e2 @ op ) )
= e0 ) )
& ( ( ( e1 @ ( e2 @ op ) )
= e4 )
| ( ( e1 @ ( e2 @ op ) )
= e3 )
| ( ( e1 @ ( e2 @ op ) )
= e2 )
| ( ( e1 @ ( e2 @ op ) )
= e1 )
| ( ( e1 @ ( e2 @ op ) )
= e0 ) )
& ( ( ( e0 @ ( e2 @ op ) )
= e4 )
| ( ( e0 @ ( e2 @ op ) )
= e3 )
| ( ( e0 @ ( e2 @ op ) )
= e2 )
| ( ( e0 @ ( e2 @ op ) )
= e1 )
| ( ( e0 @ ( e2 @ op ) )
= e0 ) )
& ( ( ( e4 @ ( e1 @ op ) )
= e4 )
| ( ( e4 @ ( e1 @ op ) )
= e3 )
| ( ( e4 @ ( e1 @ op ) )
= e2 )
| ( ( e4 @ ( e1 @ op ) )
= e1 )
| ( ( e4 @ ( e1 @ op ) )
= e0 ) )
& ( ( ( e3 @ ( e1 @ op ) )
= e4 )
| ( ( e3 @ ( e1 @ op ) )
= e3 )
| ( ( e3 @ ( e1 @ op ) )
= e2 )
| ( ( e3 @ ( e1 @ op ) )
= e1 )
| ( ( e3 @ ( e1 @ op ) )
= e0 ) )
& ( ( ( e2 @ ( e1 @ op ) )
= e4 )
| ( ( e2 @ ( e1 @ op ) )
= e3 )
| ( ( e2 @ ( e1 @ op ) )
= e2 )
| ( ( e2 @ ( e1 @ op ) )
= e1 )
| ( ( e2 @ ( e1 @ op ) )
= e0 ) )
& ( ( ( e1 @ ( e1 @ op ) )
= e4 )
| ( ( e1 @ ( e1 @ op ) )
= e3 )
| ( ( e1 @ ( e1 @ op ) )
= e2 )
| ( ( e1 @ ( e1 @ op ) )
= e1 )
| ( ( e1 @ ( e1 @ op ) )
= e0 ) )
& ( ( ( e0 @ ( e1 @ op ) )
= e4 )
| ( ( e0 @ ( e1 @ op ) )
= e3 )
| ( ( e0 @ ( e1 @ op ) )
= e2 )
| ( ( e0 @ ( e1 @ op ) )
= e1 )
| ( ( e0 @ ( e1 @ op ) )
= e0 ) )
& ( ( ( e4 @ ( e0 @ op ) )
= e4 )
| ( ( e4 @ ( e0 @ op ) )
= e3 )
| ( ( e4 @ ( e0 @ op ) )
= e2 )
| ( ( e4 @ ( e0 @ op ) )
= e1 )
| ( ( e4 @ ( e0 @ op ) )
= e0 ) )
& ( ( ( e3 @ ( e0 @ op ) )
= e4 )
| ( ( e3 @ ( e0 @ op ) )
= e3 )
| ( ( e3 @ ( e0 @ op ) )
= e2 )
| ( ( e3 @ ( e0 @ op ) )
= e1 )
| ( ( e3 @ ( e0 @ op ) )
= e0 ) )
& ( ( ( e2 @ ( e0 @ op ) )
= e4 )
| ( ( e2 @ ( e0 @ op ) )
= e3 )
| ( ( e2 @ ( e0 @ op ) )
= e2 )
| ( ( e2 @ ( e0 @ op ) )
= e1 )
| ( ( e2 @ ( e0 @ op ) )
= e0 ) )
& ( ( ( e1 @ ( e0 @ op ) )
= e4 )
| ( ( e1 @ ( e0 @ op ) )
= e3 )
| ( ( e1 @ ( e0 @ op ) )
= e2 )
| ( ( e1 @ ( e0 @ op ) )
= e1 )
| ( ( e1 @ ( e0 @ op ) )
= e0 ) )
& ( ( ( e0 @ ( e0 @ op ) )
= e4 )
| ( ( e0 @ ( e0 @ op ) )
= e3 )
| ( ( e0 @ ( e0 @ op ) )
= e2 )
| ( ( e0 @ ( e0 @ op ) )
= e1 )
| ( ( e0 @ ( e0 @ op ) )
= e0 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
thf(365,plain,
( ( ( ( e4 @ ( e4 @ op ) )
= e4 )
| ( ( e4 @ ( e4 @ op ) )
= e3 )
| ( ( e4 @ ( e4 @ op ) )
= e2 )
| ( ( e4 @ ( e4 @ op ) )
= e1 )
| ( ( e4 @ ( e4 @ op ) )
= e0 ) )
& ( ( ( e3 @ ( e4 @ op ) )
= e4 )
| ( ( e3 @ ( e4 @ op ) )
= e3 )
| ( ( e3 @ ( e4 @ op ) )
= e2 )
| ( ( e3 @ ( e4 @ op ) )
= e1 )
| ( ( e3 @ ( e4 @ op ) )
= e0 ) )
& ( ( ( e2 @ ( e4 @ op ) )
= e4 )
| ( ( e2 @ ( e4 @ op ) )
= e3 )
| ( ( e2 @ ( e4 @ op ) )
= e2 )
| ( ( e2 @ ( e4 @ op ) )
= e1 )
| ( ( e2 @ ( e4 @ op ) )
= e0 ) )
& ( ( ( e1 @ ( e4 @ op ) )
= e4 )
| ( ( e1 @ ( e4 @ op ) )
= e3 )
| ( ( e1 @ ( e4 @ op ) )
= e2 )
| ( ( e1 @ ( e4 @ op ) )
= e1 )
| ( ( e1 @ ( e4 @ op ) )
= e0 ) )
& ( ( ( e0 @ ( e4 @ op ) )
= e4 )
| ( ( e0 @ ( e4 @ op ) )
= e3 )
| ( ( e0 @ ( e4 @ op ) )
= e2 )
| ( ( e0 @ ( e4 @ op ) )
= e1 )
| ( ( e0 @ ( e4 @ op ) )
= e0 ) )
& ( ( ( e4 @ ( e3 @ op ) )
= e4 )
| ( ( e4 @ ( e3 @ op ) )
= e3 )
| ( ( e4 @ ( e3 @ op ) )
= e2 )
| ( ( e4 @ ( e3 @ op ) )
= e1 )
| ( ( e4 @ ( e3 @ op ) )
= e0 ) )
& ( ( ( e3 @ ( e3 @ op ) )
= e4 )
| ( ( e3 @ ( e3 @ op ) )
= e3 )
| ( ( e3 @ ( e3 @ op ) )
= e2 )
| ( ( e3 @ ( e3 @ op ) )
= e1 )
| ( ( e3 @ ( e3 @ op ) )
= e0 ) )
& ( ( ( e2 @ ( e3 @ op ) )
= e4 )
| ( ( e2 @ ( e3 @ op ) )
= e3 )
| ( ( e2 @ ( e3 @ op ) )
= e2 )
| ( ( e2 @ ( e3 @ op ) )
= e1 )
| ( ( e2 @ ( e3 @ op ) )
= e0 ) )
& ( ( ( e1 @ ( e3 @ op ) )
= e4 )
| ( ( e1 @ ( e3 @ op ) )
= e3 )
| ( ( e1 @ ( e3 @ op ) )
= e2 )
| ( ( e1 @ ( e3 @ op ) )
= e1 )
| ( ( e1 @ ( e3 @ op ) )
= e0 ) )
& ( ( ( e0 @ ( e3 @ op ) )
= e4 )
| ( ( e0 @ ( e3 @ op ) )
= e3 )
| ( ( e0 @ ( e3 @ op ) )
= e2 )
| ( ( e0 @ ( e3 @ op ) )
= e1 )
| ( ( e0 @ ( e3 @ op ) )
= e0 ) )
& ( ( ( e4 @ ( e2 @ op ) )
= e4 )
| ( ( e4 @ ( e2 @ op ) )
= e3 )
| ( ( e4 @ ( e2 @ op ) )
= e2 )
| ( ( e4 @ ( e2 @ op ) )
= e1 )
| ( ( e4 @ ( e2 @ op ) )
= e0 ) )
& ( ( ( e3 @ ( e2 @ op ) )
= e4 )
| ( ( e3 @ ( e2 @ op ) )
= e3 )
| ( ( e3 @ ( e2 @ op ) )
= e2 )
| ( ( e3 @ ( e2 @ op ) )
= e1 )
| ( ( e3 @ ( e2 @ op ) )
= e0 ) )
& ( ( ( e2 @ ( e2 @ op ) )
= e4 )
| ( ( e2 @ ( e2 @ op ) )
= e3 )
| ( ( e2 @ ( e2 @ op ) )
= e2 )
| ( ( e2 @ ( e2 @ op ) )
= e1 )
| ( ( e2 @ ( e2 @ op ) )
= e0 ) )
& ( ( ( e1 @ ( e2 @ op ) )
= e4 )
| ( ( e1 @ ( e2 @ op ) )
= e3 )
| ( ( e1 @ ( e2 @ op ) )
= e2 )
| ( ( e1 @ ( e2 @ op ) )
= e1 )
| ( ( e1 @ ( e2 @ op ) )
= e0 ) )
& ( ( ( e0 @ ( e2 @ op ) )
= e4 )
| ( ( e0 @ ( e2 @ op ) )
= e3 )
| ( ( e0 @ ( e2 @ op ) )
= e2 )
| ( ( e0 @ ( e2 @ op ) )
= e1 )
| ( ( e0 @ ( e2 @ op ) )
= e0 ) )
& ( ( ( e4 @ ( e1 @ op ) )
= e4 )
| ( ( e4 @ ( e1 @ op ) )
= e3 )
| ( ( e4 @ ( e1 @ op ) )
= e2 )
| ( ( e4 @ ( e1 @ op ) )
= e1 )
| ( ( e4 @ ( e1 @ op ) )
= e0 ) )
& ( ( ( e3 @ ( e1 @ op ) )
= e4 )
| ( ( e3 @ ( e1 @ op ) )
= e3 )
| ( ( e3 @ ( e1 @ op ) )
= e2 )
| ( ( e3 @ ( e1 @ op ) )
= e1 )
| ( ( e3 @ ( e1 @ op ) )
= e0 ) )
& ( ( ( e2 @ ( e1 @ op ) )
= e4 )
| ( ( e2 @ ( e1 @ op ) )
= e3 )
| ( ( e2 @ ( e1 @ op ) )
= e2 )
| ( ( e2 @ ( e1 @ op ) )
= e1 )
| ( ( e2 @ ( e1 @ op ) )
= e0 ) )
& ( ( ( e1 @ ( e1 @ op ) )
= e4 )
| ( ( e1 @ ( e1 @ op ) )
= e3 )
| ( ( e1 @ ( e1 @ op ) )
= e2 )
| ( ( e1 @ ( e1 @ op ) )
= e1 )
| ( ( e1 @ ( e1 @ op ) )
= e0 ) )
& ( ( ( e0 @ ( e1 @ op ) )
= e4 )
| ( ( e0 @ ( e1 @ op ) )
= e3 )
| ( ( e0 @ ( e1 @ op ) )
= e2 )
| ( ( e0 @ ( e1 @ op ) )
= e1 )
| ( ( e0 @ ( e1 @ op ) )
= e0 ) )
& ( ( ( e4 @ ( e0 @ op ) )
= e4 )
| ( ( e4 @ ( e0 @ op ) )
= e3 )
| ( ( e4 @ ( e0 @ op ) )
= e2 )
| ( ( e4 @ ( e0 @ op ) )
= e1 )
| ( ( e4 @ ( e0 @ op ) )
= e0 ) )
& ( ( ( e3 @ ( e0 @ op ) )
= e4 )
| ( ( e3 @ ( e0 @ op ) )
= e3 )
| ( ( e3 @ ( e0 @ op ) )
= e2 )
| ( ( e3 @ ( e0 @ op ) )
= e1 )
| ( ( e3 @ ( e0 @ op ) )
= e0 ) )
& ( ( ( e2 @ ( e0 @ op ) )
= e4 )
| ( ( e2 @ ( e0 @ op ) )
= e3 )
| ( ( e2 @ ( e0 @ op ) )
= e2 )
| ( ( e2 @ ( e0 @ op ) )
= e1 )
| ( ( e2 @ ( e0 @ op ) )
= e0 ) )
& ( ( ( e1 @ ( e0 @ op ) )
= e4 )
| ( ( e1 @ ( e0 @ op ) )
= e3 )
| ( ( e1 @ ( e0 @ op ) )
= e2 )
| ( ( e1 @ ( e0 @ op ) )
= e1 )
| ( ( e1 @ ( e0 @ op ) )
= e0 ) )
& ( ( ( e0 @ ( e0 @ op ) )
= e4 )
| ( ( e0 @ ( e0 @ op ) )
= e3 )
| ( ( e0 @ ( e0 @ op ) )
= e2 )
| ( ( e0 @ ( e0 @ op ) )
= e1 )
| ( ( e0 @ ( e0 @ op ) )
= e0 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(366,plain,
( ( ( ( e4 @ ( e4 @ op ) )
= e4 )
| ( ( e4 @ ( e4 @ op ) )
= e3 )
| ( ( e4 @ ( e4 @ op ) )
= e2 )
| ( ( e4 @ ( e4 @ op ) )
= e1 )
| ( ( e4 @ ( e4 @ op ) )
= e0 ) )
& ( ( ( e3 @ ( e4 @ op ) )
= e4 )
| ( ( e3 @ ( e4 @ op ) )
= e3 )
| ( ( e3 @ ( e4 @ op ) )
= e2 )
| ( ( e3 @ ( e4 @ op ) )
= e1 )
| ( ( e3 @ ( e4 @ op ) )
= e0 ) )
& ( ( ( e2 @ ( e4 @ op ) )
= e4 )
| ( ( e2 @ ( e4 @ op ) )
= e3 )
| ( ( e2 @ ( e4 @ op ) )
= e2 )
| ( ( e2 @ ( e4 @ op ) )
= e1 )
| ( ( e2 @ ( e4 @ op ) )
= e0 ) )
& ( ( ( e1 @ ( e4 @ op ) )
= e4 )
| ( ( e1 @ ( e4 @ op ) )
= e3 )
| ( ( e1 @ ( e4 @ op ) )
= e2 )
| ( ( e1 @ ( e4 @ op ) )
= e1 )
| ( ( e1 @ ( e4 @ op ) )
= e0 ) )
& ( ( ( e0 @ ( e4 @ op ) )
= e4 )
| ( ( e0 @ ( e4 @ op ) )
= e3 )
| ( ( e0 @ ( e4 @ op ) )
= e2 )
| ( ( e0 @ ( e4 @ op ) )
= e1 )
| ( ( e0 @ ( e4 @ op ) )
= e0 ) )
& ( ( ( e4 @ ( e3 @ op ) )
= e4 )
| ( ( e4 @ ( e3 @ op ) )
= e3 )
| ( ( e4 @ ( e3 @ op ) )
= e2 )
| ( ( e4 @ ( e3 @ op ) )
= e1 )
| ( ( e4 @ ( e3 @ op ) )
= e0 ) )
& ( ( ( e3 @ ( e3 @ op ) )
= e4 )
| ( ( e3 @ ( e3 @ op ) )
= e3 )
| ( ( e3 @ ( e3 @ op ) )
= e2 )
| ( ( e3 @ ( e3 @ op ) )
= e1 )
| ( ( e3 @ ( e3 @ op ) )
= e0 ) )
& ( ( ( e2 @ ( e3 @ op ) )
= e4 )
| ( ( e2 @ ( e3 @ op ) )
= e3 )
| ( ( e2 @ ( e3 @ op ) )
= e2 )
| ( ( e2 @ ( e3 @ op ) )
= e1 )
| ( ( e2 @ ( e3 @ op ) )
= e0 ) )
& ( ( ( e1 @ ( e3 @ op ) )
= e4 )
| ( ( e1 @ ( e3 @ op ) )
= e3 )
| ( ( e1 @ ( e3 @ op ) )
= e2 )
| ( ( e1 @ ( e3 @ op ) )
= e1 )
| ( ( e1 @ ( e3 @ op ) )
= e0 ) )
& ( ( ( e0 @ ( e3 @ op ) )
= e4 )
| ( ( e0 @ ( e3 @ op ) )
= e3 )
| ( ( e0 @ ( e3 @ op ) )
= e2 )
| ( ( e0 @ ( e3 @ op ) )
= e1 )
| ( ( e0 @ ( e3 @ op ) )
= e0 ) )
& ( ( ( e4 @ ( e2 @ op ) )
= e4 )
| ( ( e4 @ ( e2 @ op ) )
= e3 )
| ( ( e4 @ ( e2 @ op ) )
= e2 )
| ( ( e4 @ ( e2 @ op ) )
= e1 )
| ( ( e4 @ ( e2 @ op ) )
= e0 ) )
& ( ( ( e3 @ ( e2 @ op ) )
= e4 )
| ( ( e3 @ ( e2 @ op ) )
= e3 )
| ( ( e3 @ ( e2 @ op ) )
= e2 )
| ( ( e3 @ ( e2 @ op ) )
= e1 )
| ( ( e3 @ ( e2 @ op ) )
= e0 ) )
& ( ( ( e2 @ ( e2 @ op ) )
= e4 )
| ( ( e2 @ ( e2 @ op ) )
= e3 )
| ( ( e2 @ ( e2 @ op ) )
= e2 )
| ( ( e2 @ ( e2 @ op ) )
= e1 )
| ( ( e2 @ ( e2 @ op ) )
= e0 ) )
& ( ( ( e1 @ ( e2 @ op ) )
= e4 )
| ( ( e1 @ ( e2 @ op ) )
= e3 )
| ( ( e1 @ ( e2 @ op ) )
= e2 )
| ( ( e1 @ ( e2 @ op ) )
= e1 )
| ( ( e1 @ ( e2 @ op ) )
= e0 ) )
& ( ( ( e0 @ ( e2 @ op ) )
= e4 )
| ( ( e0 @ ( e2 @ op ) )
= e3 )
| ( ( e0 @ ( e2 @ op ) )
= e2 )
| ( ( e0 @ ( e2 @ op ) )
= e1 )
| ( ( e0 @ ( e2 @ op ) )
= e0 ) )
& ( ( ( e4 @ ( e1 @ op ) )
= e4 )
| ( ( e4 @ ( e1 @ op ) )
= e3 )
| ( ( e4 @ ( e1 @ op ) )
= e2 )
| ( ( e4 @ ( e1 @ op ) )
= e1 )
| ( ( e4 @ ( e1 @ op ) )
= e0 ) )
& ( ( ( e3 @ ( e1 @ op ) )
= e4 )
| ( ( e3 @ ( e1 @ op ) )
= e3 )
| ( ( e3 @ ( e1 @ op ) )
= e2 )
| ( ( e3 @ ( e1 @ op ) )
= e1 )
| ( ( e3 @ ( e1 @ op ) )
= e0 ) )
& ( ( ( e2 @ ( e1 @ op ) )
= e4 )
| ( ( e2 @ ( e1 @ op ) )
= e3 )
| ( ( e2 @ ( e1 @ op ) )
= e2 )
| ( ( e2 @ ( e1 @ op ) )
= e1 )
| ( ( e2 @ ( e1 @ op ) )
= e0 ) )
& ( ( ( e1 @ ( e1 @ op ) )
= e4 )
| ( ( e1 @ ( e1 @ op ) )
= e3 )
| ( ( e1 @ ( e1 @ op ) )
= e2 )
| ( ( e1 @ ( e1 @ op ) )
= e1 )
| ( ( e1 @ ( e1 @ op ) )
= e0 ) )
& ( ( ( e0 @ ( e1 @ op ) )
= e4 )
| ( ( e0 @ ( e1 @ op ) )
= e3 )
| ( ( e0 @ ( e1 @ op ) )
= e2 )
| ( ( e0 @ ( e1 @ op ) )
= e1 )
| ( ( e0 @ ( e1 @ op ) )
= e0 ) )
& ( ( ( e4 @ ( e0 @ op ) )
= e4 )
| ( ( e4 @ ( e0 @ op ) )
= e3 )
| ( ( e4 @ ( e0 @ op ) )
= e2 )
| ( ( e4 @ ( e0 @ op ) )
= e1 )
| ( ( e4 @ ( e0 @ op ) )
= e0 ) )
& ( ( ( e3 @ ( e0 @ op ) )
= e4 )
| ( ( e3 @ ( e0 @ op ) )
= e3 )
| ( ( e3 @ ( e0 @ op ) )
= e2 )
| ( ( e3 @ ( e0 @ op ) )
= e1 )
| ( ( e3 @ ( e0 @ op ) )
= e0 ) )
& ( ( ( e2 @ ( e0 @ op ) )
= e4 )
| ( ( e2 @ ( e0 @ op ) )
= e3 )
| ( ( e2 @ ( e0 @ op ) )
= e2 )
| ( ( e2 @ ( e0 @ op ) )
= e1 )
| ( ( e2 @ ( e0 @ op ) )
= e0 ) )
& ( ( ( e1 @ ( e0 @ op ) )
= e4 )
| ( ( e1 @ ( e0 @ op ) )
= e3 )
| ( ( e1 @ ( e0 @ op ) )
= e2 )
| ( ( e1 @ ( e0 @ op ) )
= e1 )
| ( ( e1 @ ( e0 @ op ) )
= e0 ) )
& ( ( ( e0 @ ( e0 @ op ) )
= e4 )
| ( ( e0 @ ( e0 @ op ) )
= e3 )
| ( ( e0 @ ( e0 @ op ) )
= e2 )
| ( ( e0 @ ( e0 @ op ) )
= e1 )
| ( ( e0 @ ( e0 @ op ) )
= e0 ) ) ),
inference(cnf,[status(esa)],[365]) ).
thf(382,plain,
( ( ( e1 @ ( e2 @ op ) )
= e4 )
| ( ( e1 @ ( e2 @ op ) )
= e3 )
| ( ( e1 @ ( e2 @ op ) )
= e2 )
| ( ( e1 @ ( e2 @ op ) )
= e1 )
| ( ( e1 @ ( e2 @ op ) )
= e0 ) ),
inference(cnfConj,[status(thm)],[366]) ).
thf(412,plain,
( ( ( e1 @ ( e2 @ op ) )
= e4 )
| ( ( e1 @ ( e2 @ op ) )
= e3 )
| ( ( e1 @ ( e2 @ op ) )
= e2 )
| ( ( e1 @ ( e2 @ op ) )
= e1 )
| ( ( e1 @ ( e2 @ op ) )
= e0 ) ),
inference(lifteq,[status(thm)],[382]) ).
thf(573,plain,
( ( e1 @ ( e1 @ op ) )
!= ( e1 @ ( e2 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(688,plain,
( ( e1 @ ( e2 @ op ) )
!= ( e1 @ ( e1 @ op ) ) ),
inference(lifteq,[status(thm)],[573]) ).
thf(8528,plain,
( ( e1 @ ( e2 @ op ) )
!= e4 ),
inference(rewrite,[status(thm)],[688,776]) ).
thf(594,plain,
( ( e1 @ ( e0 @ op ) )
!= ( e1 @ ( e2 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(705,plain,
( ( e1 @ ( e2 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ),
inference(lifteq,[status(thm)],[594]) ).
thf(50501,plain,
( ( e1 @ ( e2 @ op ) )
!= e1 ),
inference(rewrite,[status(thm)],[705,49570]) ).
thf(584,plain,
( ( e1 @ ( e2 @ op ) )
!= ( e2 @ ( e2 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(690,plain,
( ( e2 @ ( e2 @ op ) )
!= ( e1 @ ( e2 @ op ) ) ),
inference(lifteq,[status(thm)],[584]) ).
thf(22282,plain,
( ( e1 @ ( e2 @ op ) )
!= e3 ),
inference(rewrite,[status(thm)],[690,22275]) ).
thf(567,plain,
( ( e0 @ ( e2 @ op ) )
!= ( e1 @ ( e2 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(699,plain,
( ( e1 @ ( e2 @ op ) )
!= ( e0 @ ( e2 @ op ) ) ),
inference(lifteq,[status(thm)],[567]) ).
thf(421,plain,
( ( unit @ ( e2 @ op ) )
= e2 ),
inference(cnfConj,[status(thm)],[418]) ).
thf(430,plain,
( ( unit @ ( e2 @ op ) )
= e2 ),
inference(lifteq,[status(thm)],[421]) ).
thf(49574,plain,
( ( e0 @ ( e2 @ op ) )
= e2 ),
inference(rewrite,[status(thm)],[430,49564]) ).
thf(50990,plain,
( ( e1 @ ( e2 @ op ) )
!= e2 ),
inference(rewrite,[status(thm)],[699,49574]) ).
thf(59505,plain,
( ( e1 @ ( e2 @ op ) )
= e0 ),
inference(simplifyReflect,[status(thm)],[412,8528,50501,22282,50990]) ).
thf(61340,plain,
( sk5
| ~ sk4
| ~ sk3
| ~ $true
| ~ $true
| ( e0 != e0 )
| ( ( e0 @ ( e1 @ op ) )
!= e1 ) ),
inference(rewrite,[status(thm)],[288,2353,59505,49570,49572,52265]) ).
thf(61341,plain,
( sk5
| ~ sk4
| ~ sk3
| ( ( e0 @ ( e1 @ op ) )
!= e1 ) ),
inference(simp,[status(thm)],[61340]) ).
thf(61383,plain,
( ( ( e0 @ ( e1 @ op ) )
!= ( e0 @ ( e1 @ op ) ) )
| sk5
| ~ sk4
| ~ sk3
| ( e1 != e1 ) ),
inference(paramod_ordered,[status(thm)],[49580,61341]) ).
thf(61384,plain,
( ( ( e0 @ ( e1 @ op ) )
!= ( e0 @ ( e1 @ op ) ) )
| sk5
| ~ sk4
| ~ sk3 ),
inference(simp,[status(thm)],[61383]) ).
thf(61385,plain,
( sk5
| ~ sk4
| ~ sk3 ),
inference(pattern_uni,[status(thm)],[61384:[]]) ).
thf(61474,plain,
( ( sk4 != sk4 )
| sk5
| ~ $true
| ~ sk3
| ~ sk3 ),
inference(paramod_ordered,[status(thm)],[52306,61385]) ).
thf(61475,plain,
( ( sk4 != sk4 )
| sk5
| ~ sk3 ),
inference(simp,[status(thm)],[61474]) ).
thf(61476,plain,
( sk5
| ~ sk3 ),
inference(pattern_uni,[status(thm)],[61475:[]]) ).
thf(103,plain,
( sk3
| ( ( e4 @ ( e4 @ ( e0 @ op ) @ op ) )
= e0 )
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) ),
inference(cnfConj,[status(thm)],[11]) ).
thf(292,plain,
( sk3
| ~ sk2
| ~ sk1
| ( ( e4 @ ( e4 @ ( e0 @ op ) @ op ) )
= e0 )
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) ),
inference(lifteq,[status(thm)],[103]) ).
thf(49568,plain,
( ( e4 @ ( e0 @ op ) )
= e4 ),
inference(rewrite,[status(thm)],[436,49564]) ).
thf(61921,plain,
( sk3
| ~ $true
| ~ $true
| ( ( e4 @ ( e4 @ op ) )
= e0 )
| ( e1 != e1 ) ),
inference(rewrite,[status(thm)],[292,49568,49570,49572,52265,49580]) ).
thf(61922,plain,
( sk3
| ( ( e4 @ ( e4 @ op ) )
= e0 ) ),
inference(simp,[status(thm)],[61921]) ).
thf(61935,plain,
( ( ( e4 @ ( e4 @ op ) )
!= ( e4 @ ( e4 @ op ) ) )
| ( e2 = e0 )
| sk3 ),
inference(paramod_ordered,[status(thm)],[61922,1627]) ).
thf(61936,plain,
( ( e2 = e0 )
| sk3 ),
inference(pattern_uni,[status(thm)],[61935:[]]) ).
thf(62095,plain,
sk3,
inference(simplifyReflect,[status(thm)],[61936,757]) ).
thf(62112,plain,
( sk5
| ~ $true ),
inference(rewrite,[status(thm)],[61476,62095]) ).
thf(62113,plain,
sk5,
inference(simp,[status(thm)],[62112]) ).
thf(62130,plain,
( ~ $true
| sk4 ),
inference(rewrite,[status(thm)],[52306,62095]) ).
thf(62131,plain,
sk4,
inference(simp,[status(thm)],[62130]) ).
thf(49578,plain,
( ( e2 @ ( e0 @ op ) )
= e2 ),
inference(rewrite,[status(thm)],[438,49564]) ).
thf(63248,plain,
( sk8
| ~ sk7
| ~ sk6
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ( e2 != e2 )
| ( e1 != e1 ) ),
inference(rewrite,[status(thm)],[303,62113,49570,62131,49572,49574,52265,49578,49580,62095]) ).
thf(63249,plain,
( sk8
| ~ sk7
| ~ sk6 ),
inference(simp,[status(thm)],[63248]) ).
thf(50,plain,
( sk10
| ( ( e2 @ ( e3 @ op ) )
!= ( e3 @ ( e2 @ op ) ) )
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) ),
inference(cnfConj,[status(thm)],[11]) ).
thf(312,plain,
( sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e2 @ ( e3 @ op ) )
!= ( e3 @ ( e2 @ op ) ) )
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) ),
inference(lifteq,[status(thm)],[50]) ).
thf(369,plain,
( ( ( e2 @ ( e3 @ op ) )
= e4 )
| ( ( e2 @ ( e3 @ op ) )
= e3 )
| ( ( e2 @ ( e3 @ op ) )
= e2 )
| ( ( e2 @ ( e3 @ op ) )
= e1 )
| ( ( e2 @ ( e3 @ op ) )
= e0 ) ),
inference(cnfConj,[status(thm)],[366]) ).
thf(404,plain,
( ( ( e2 @ ( e3 @ op ) )
= e4 )
| ( ( e2 @ ( e3 @ op ) )
= e3 )
| ( ( e2 @ ( e3 @ op ) )
= e2 )
| ( ( e2 @ ( e3 @ op ) )
= e1 )
| ( ( e2 @ ( e3 @ op ) )
= e0 ) ),
inference(lifteq,[status(thm)],[369]) ).
thf(621,plain,
( ( e2 @ ( e0 @ op ) )
!= ( e2 @ ( e3 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(706,plain,
( ( e2 @ ( e3 @ op ) )
!= ( e2 @ ( e0 @ op ) ) ),
inference(lifteq,[status(thm)],[621]) ).
thf(51424,plain,
( ( e2 @ ( e3 @ op ) )
!= e2 ),
inference(rewrite,[status(thm)],[706,49578]) ).
thf(619,plain,
( ( e2 @ ( e1 @ op ) )
!= ( e2 @ ( e3 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(656,plain,
( ( e2 @ ( e3 @ op ) )
!= ( e2 @ ( e1 @ op ) ) ),
inference(lifteq,[status(thm)],[619]) ).
thf(2601,plain,
( ( e2 @ ( e3 @ op ) )
!= e0 ),
inference(rewrite,[status(thm)],[656,2353]) ).
thf(616,plain,
( ( e2 @ ( e2 @ op ) )
!= ( e2 @ ( e3 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(700,plain,
( ( e2 @ ( e3 @ op ) )
!= ( e2 @ ( e2 @ op ) ) ),
inference(lifteq,[status(thm)],[616]) ).
thf(22281,plain,
( ( e2 @ ( e3 @ op ) )
!= e3 ),
inference(rewrite,[status(thm)],[700,22275]) ).
thf(607,plain,
( ( e2 @ ( e3 @ op ) )
!= ( e3 @ ( e3 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(741,plain,
( ( e3 @ ( e3 @ op ) )
!= ( e2 @ ( e3 @ op ) ) ),
inference(lifteq,[status(thm)],[607]) ).
thf(49567,plain,
( ( e0 @ ( e0 @ op ) )
= e0 ),
inference(rewrite,[status(thm)],[440,49564]) ).
thf(49970,plain,
( ( ( e3 @ ( e3 @ op ) )
= e1 )
| ( e1 = e0 ) ),
inference(rewrite,[status(thm)],[46999,49567]) ).
thf(52061,plain,
( ( e3 @ ( e3 @ op ) )
= e1 ),
inference(simplifyReflect,[status(thm)],[49970,760]) ).
thf(52062,plain,
( ( e2 @ ( e3 @ op ) )
!= e1 ),
inference(rewrite,[status(thm)],[741,52061]) ).
thf(58226,plain,
( ( e2 @ ( e3 @ op ) )
= e4 ),
inference(simplifyReflect,[status(thm)],[404,51424,2601,22281,52062]) ).
thf(367,plain,
( ( ( e3 @ ( e2 @ op ) )
= e4 )
| ( ( e3 @ ( e2 @ op ) )
= e3 )
| ( ( e3 @ ( e2 @ op ) )
= e2 )
| ( ( e3 @ ( e2 @ op ) )
= e1 )
| ( ( e3 @ ( e2 @ op ) )
= e0 ) ),
inference(cnfConj,[status(thm)],[366]) ).
thf(414,plain,
( ( ( e3 @ ( e2 @ op ) )
= e4 )
| ( ( e3 @ ( e2 @ op ) )
= e3 )
| ( ( e3 @ ( e2 @ op ) )
= e2 )
| ( ( e3 @ ( e2 @ op ) )
= e1 )
| ( ( e3 @ ( e2 @ op ) )
= e0 ) ),
inference(lifteq,[status(thm)],[367]) ).
thf(609,plain,
( ( e3 @ ( e2 @ op ) )
!= ( e3 @ ( e3 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(704,plain,
( ( e3 @ ( e3 @ op ) )
!= ( e3 @ ( e2 @ op ) ) ),
inference(lifteq,[status(thm)],[609]) ).
thf(52065,plain,
( ( e3 @ ( e2 @ op ) )
!= e1 ),
inference(rewrite,[status(thm)],[704,52061]) ).
thf(588,plain,
( ( e3 @ ( e2 @ op ) )
!= ( e3 @ ( e4 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(729,plain,
( ( e3 @ ( e4 @ op ) )
!= ( e3 @ ( e2 @ op ) ) ),
inference(lifteq,[status(thm)],[588]) ).
thf(376,plain,
( ( ( e3 @ ( e4 @ op ) )
= e4 )
| ( ( e3 @ ( e4 @ op ) )
= e3 )
| ( ( e3 @ ( e4 @ op ) )
= e2 )
| ( ( e3 @ ( e4 @ op ) )
= e1 )
| ( ( e3 @ ( e4 @ op ) )
= e0 ) ),
inference(cnfConj,[status(thm)],[366]) ).
thf(393,plain,
( ( ( e3 @ ( e4 @ op ) )
= e4 )
| ( ( e3 @ ( e4 @ op ) )
= e3 )
| ( ( e3 @ ( e4 @ op ) )
= e2 )
| ( ( e3 @ ( e4 @ op ) )
= e1 )
| ( ( e3 @ ( e4 @ op ) )
= e0 ) ),
inference(lifteq,[status(thm)],[376]) ).
thf(625,plain,
( ( e3 @ ( e0 @ op ) )
!= ( e3 @ ( e4 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(669,plain,
( ( e3 @ ( e4 @ op ) )
!= ( e3 @ ( e0 @ op ) ) ),
inference(lifteq,[status(thm)],[625]) ).
thf(50724,plain,
( ( e3 @ ( e4 @ op ) )
!= e3 ),
inference(rewrite,[status(thm)],[669,49573]) ).
thf(570,plain,
( ( e3 @ ( e4 @ op ) )
!= ( e4 @ ( e4 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(654,plain,
( ( e4 @ ( e4 @ op ) )
!= ( e3 @ ( e4 @ op ) ) ),
inference(lifteq,[status(thm)],[570]) ).
thf(2046,plain,
( ( e3 @ ( e4 @ op ) )
!= e2 ),
inference(rewrite,[status(thm)],[654,1627]) ).
thf(52936,plain,
( ( ( e3 @ ( e4 @ op ) )
= e4 )
| ( ( e3 @ ( e4 @ op ) )
= e1 )
| ( ( e3 @ ( e4 @ op ) )
= e0 ) ),
inference(simplifyReflect,[status(thm)],[393,50724,2046]) ).
thf(590,plain,
( ( e0 @ ( e4 @ op ) )
!= ( e3 @ ( e4 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(679,plain,
( ( e3 @ ( e4 @ op ) )
!= ( e0 @ ( e4 @ op ) ) ),
inference(lifteq,[status(thm)],[590]) ).
thf(423,plain,
( ( unit @ ( e4 @ op ) )
= e4 ),
inference(cnfConj,[status(thm)],[418]) ).
thf(434,plain,
( ( unit @ ( e4 @ op ) )
= e4 ),
inference(lifteq,[status(thm)],[423]) ).
thf(49576,plain,
( ( e0 @ ( e4 @ op ) )
= e4 ),
inference(rewrite,[status(thm)],[434,49564]) ).
thf(51208,plain,
( ( e3 @ ( e4 @ op ) )
!= e4 ),
inference(rewrite,[status(thm)],[679,49576]) ).
thf(53244,plain,
( ( ( e3 @ ( e4 @ op ) )
= e1 )
| ( ( e3 @ ( e4 @ op ) )
= e0 ) ),
inference(simplifyReflect,[status(thm)],[52936,51208]) ).
thf(623,plain,
( ( e3 @ ( e3 @ op ) )
!= ( e3 @ ( e4 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(661,plain,
( ( e3 @ ( e4 @ op ) )
!= ( e3 @ ( e3 @ op ) ) ),
inference(lifteq,[status(thm)],[623]) ).
thf(52064,plain,
( ( e3 @ ( e4 @ op ) )
!= e1 ),
inference(rewrite,[status(thm)],[661,52061]) ).
thf(54863,plain,
( ( e3 @ ( e4 @ op ) )
= e0 ),
inference(simplifyReflect,[status(thm)],[53244,52064]) ).
thf(55009,plain,
( ( e3 @ ( e2 @ op ) )
!= e0 ),
inference(rewrite,[status(thm)],[729,54863]) ).
thf(592,plain,
( ( e0 @ ( e2 @ op ) )
!= ( e3 @ ( e2 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(744,plain,
( ( e3 @ ( e2 @ op ) )
!= ( e0 @ ( e2 @ op ) ) ),
inference(lifteq,[status(thm)],[592]) ).
thf(50995,plain,
( ( e3 @ ( e2 @ op ) )
!= e2 ),
inference(rewrite,[status(thm)],[744,49574]) ).
thf(622,plain,
( ( e2 @ ( e2 @ op ) )
!= ( e3 @ ( e2 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(681,plain,
( ( e3 @ ( e2 @ op ) )
!= ( e2 @ ( e2 @ op ) ) ),
inference(lifteq,[status(thm)],[622]) ).
thf(22280,plain,
( ( e3 @ ( e2 @ op ) )
!= e3 ),
inference(rewrite,[status(thm)],[681,22275]) ).
thf(60078,plain,
( ( e3 @ ( e2 @ op ) )
= e4 ),
inference(simplifyReflect,[status(thm)],[414,52065,55009,50995,22280]) ).
thf(63995,plain,
( sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ( e4 != e4 )
| ( e1 != e1 ) ),
inference(rewrite,[status(thm)],[312,62113,49570,58226,62131,49572,52265,49580,60078,62095]) ).
thf(63996,plain,
( sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6 ),
inference(simp,[status(thm)],[63995]) ).
thf(64000,plain,
( ( sk8 != sk8 )
| sk10
| ~ sk9
| ~ $true
| ~ sk7
| ~ sk6
| ~ sk7
| ~ sk6 ),
inference(paramod_ordered,[status(thm)],[63249,63996]) ).
thf(64001,plain,
( ( sk8 != sk8 )
| sk10
| ~ sk9
| ~ sk7
| ~ sk6 ),
inference(simp,[status(thm)],[64000]) ).
thf(64002,plain,
( sk10
| ~ sk9
| ~ sk7
| ~ sk6 ),
inference(pattern_uni,[status(thm)],[64001:[]]) ).
thf(123,plain,
( sk11
| ( ( e2 @ ( e4 @ op ) )
!= ( e4 @ ( e2 @ op ) ) )
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) ),
inference(cnfConj,[status(thm)],[11]) ).
thf(305,plain,
( sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e2 @ ( e4 @ op ) )
!= ( e4 @ ( e2 @ op ) ) )
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) ),
inference(lifteq,[status(thm)],[123]) ).
thf(380,plain,
( ( ( e2 @ ( e4 @ op ) )
= e4 )
| ( ( e2 @ ( e4 @ op ) )
= e3 )
| ( ( e2 @ ( e4 @ op ) )
= e2 )
| ( ( e2 @ ( e4 @ op ) )
= e1 )
| ( ( e2 @ ( e4 @ op ) )
= e0 ) ),
inference(cnfConj,[status(thm)],[366]) ).
thf(409,plain,
( ( ( e2 @ ( e4 @ op ) )
= e4 )
| ( ( e2 @ ( e4 @ op ) )
= e3 )
| ( ( e2 @ ( e4 @ op ) )
= e2 )
| ( ( e2 @ ( e4 @ op ) )
= e1 )
| ( ( e2 @ ( e4 @ op ) )
= e0 ) ),
inference(lifteq,[status(thm)],[380]) ).
thf(561,plain,
( ( e2 @ ( e2 @ op ) )
!= ( e2 @ ( e4 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(666,plain,
( ( e2 @ ( e4 @ op ) )
!= ( e2 @ ( e2 @ op ) ) ),
inference(lifteq,[status(thm)],[561]) ).
thf(22276,plain,
( ( e2 @ ( e4 @ op ) )
!= e3 ),
inference(rewrite,[status(thm)],[666,22275]) ).
thf(605,plain,
( ( e2 @ ( e1 @ op ) )
!= ( e2 @ ( e4 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(683,plain,
( ( e2 @ ( e4 @ op ) )
!= ( e2 @ ( e1 @ op ) ) ),
inference(lifteq,[status(thm)],[605]) ).
thf(7175,plain,
( ( e2 @ ( e4 @ op ) )
!= e0 ),
inference(rewrite,[status(thm)],[683,2353]) ).
thf(572,plain,
( ( e0 @ ( e4 @ op ) )
!= ( e2 @ ( e4 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(696,plain,
( ( e2 @ ( e4 @ op ) )
!= ( e0 @ ( e4 @ op ) ) ),
inference(lifteq,[status(thm)],[572]) ).
thf(51213,plain,
( ( e2 @ ( e4 @ op ) )
!= e4 ),
inference(rewrite,[status(thm)],[696,49576]) ).
thf(620,plain,
( ( e2 @ ( e4 @ op ) )
!= ( e4 @ ( e4 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(733,plain,
( ( e4 @ ( e4 @ op ) )
!= ( e2 @ ( e4 @ op ) ) ),
inference(lifteq,[status(thm)],[620]) ).
thf(19806,plain,
( ( e2 @ ( e4 @ op ) )
!= e2 ),
inference(rewrite,[status(thm)],[733,1627]) ).
thf(59035,plain,
( ( e2 @ ( e4 @ op ) )
= e1 ),
inference(simplifyReflect,[status(thm)],[409,22276,7175,51213,19806]) ).
thf(384,plain,
( ( ( e4 @ ( e2 @ op ) )
= e4 )
| ( ( e4 @ ( e2 @ op ) )
= e3 )
| ( ( e4 @ ( e2 @ op ) )
= e2 )
| ( ( e4 @ ( e2 @ op ) )
= e1 )
| ( ( e4 @ ( e2 @ op ) )
= e0 ) ),
inference(cnfConj,[status(thm)],[366]) ).
thf(406,plain,
( ( ( e4 @ ( e2 @ op ) )
= e4 )
| ( ( e4 @ ( e2 @ op ) )
= e3 )
| ( ( e4 @ ( e2 @ op ) )
= e2 )
| ( ( e4 @ ( e2 @ op ) )
= e1 )
| ( ( e4 @ ( e2 @ op ) )
= e0 ) ),
inference(lifteq,[status(thm)],[384]) ).
thf(639,plain,
( ( e2 @ ( e2 @ op ) )
!= ( e4 @ ( e2 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(743,plain,
( ( e4 @ ( e2 @ op ) )
!= ( e2 @ ( e2 @ op ) ) ),
inference(lifteq,[status(thm)],[639]) ).
thf(22279,plain,
( ( e4 @ ( e2 @ op ) )
!= e3 ),
inference(rewrite,[status(thm)],[743,22275]) ).
thf(548,plain,
( ( e4 @ ( e2 @ op ) )
!= ( e4 @ ( e4 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(712,plain,
( ( e4 @ ( e4 @ op ) )
!= ( e4 @ ( e2 @ op ) ) ),
inference(lifteq,[status(thm)],[548]) ).
thf(14250,plain,
( ( e4 @ ( e2 @ op ) )
!= e2 ),
inference(rewrite,[status(thm)],[712,1627]) ).
thf(579,plain,
( ( e4 @ ( e2 @ op ) )
!= ( e4 @ ( e3 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(693,plain,
( ( e4 @ ( e3 @ op ) )
!= ( e4 @ ( e2 @ op ) ) ),
inference(lifteq,[status(thm)],[579]) ).
thf(388,plain,
( ( ( e4 @ ( e3 @ op ) )
= e4 )
| ( ( e4 @ ( e3 @ op ) )
= e3 )
| ( ( e4 @ ( e3 @ op ) )
= e2 )
| ( ( e4 @ ( e3 @ op ) )
= e1 )
| ( ( e4 @ ( e3 @ op ) )
= e0 ) ),
inference(cnfConj,[status(thm)],[366]) ).
thf(394,plain,
( ( ( e4 @ ( e3 @ op ) )
= e4 )
| ( ( e4 @ ( e3 @ op ) )
= e3 )
| ( ( e4 @ ( e3 @ op ) )
= e2 )
| ( ( e4 @ ( e3 @ op ) )
= e1 )
| ( ( e4 @ ( e3 @ op ) )
= e0 ) ),
inference(lifteq,[status(thm)],[388]) ).
thf(636,plain,
( ( e4 @ ( e3 @ op ) )
!= ( e4 @ ( e4 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(708,plain,
( ( e4 @ ( e4 @ op ) )
!= ( e4 @ ( e3 @ op ) ) ),
inference(lifteq,[status(thm)],[636]) ).
thf(12977,plain,
( ( e4 @ ( e3 @ op ) )
!= e2 ),
inference(rewrite,[status(thm)],[708,1627]) ).
thf(613,plain,
( ( e0 @ ( e3 @ op ) )
!= ( e4 @ ( e3 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(721,plain,
( ( e4 @ ( e3 @ op ) )
!= ( e0 @ ( e3 @ op ) ) ),
inference(lifteq,[status(thm)],[613]) ).
thf(51623,plain,
( ( e4 @ ( e3 @ op ) )
!= e3 ),
inference(rewrite,[status(thm)],[721,49579]) ).
thf(553,plain,
( ( e4 @ ( e0 @ op ) )
!= ( e4 @ ( e3 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(714,plain,
( ( e4 @ ( e3 @ op ) )
!= ( e4 @ ( e0 @ op ) ) ),
inference(lifteq,[status(thm)],[553]) ).
thf(50238,plain,
( ( e4 @ ( e3 @ op ) )
!= e4 ),
inference(rewrite,[status(thm)],[714,49568]) ).
thf(53978,plain,
( ( ( e4 @ ( e3 @ op ) )
= e1 )
| ( ( e4 @ ( e3 @ op ) )
= e0 ) ),
inference(simplifyReflect,[status(thm)],[394,12977,51623,50238]) ).
thf(615,plain,
( ( e3 @ ( e3 @ op ) )
!= ( e4 @ ( e3 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(673,plain,
( ( e4 @ ( e3 @ op ) )
!= ( e3 @ ( e3 @ op ) ) ),
inference(lifteq,[status(thm)],[615]) ).
thf(52066,plain,
( ( e4 @ ( e3 @ op ) )
!= e1 ),
inference(rewrite,[status(thm)],[673,52061]) ).
thf(54960,plain,
( ( e4 @ ( e3 @ op ) )
= e0 ),
inference(simplifyReflect,[status(thm)],[53978,52066]) ).
thf(55322,plain,
( ( e4 @ ( e2 @ op ) )
!= e0 ),
inference(rewrite,[status(thm)],[693,54960]) ).
thf(608,plain,
( ( e4 @ ( e0 @ op ) )
!= ( e4 @ ( e2 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(709,plain,
( ( e4 @ ( e2 @ op ) )
!= ( e4 @ ( e0 @ op ) ) ),
inference(lifteq,[status(thm)],[608]) ).
thf(50237,plain,
( ( e4 @ ( e2 @ op ) )
!= e4 ),
inference(rewrite,[status(thm)],[709,49568]) ).
thf(58700,plain,
( ( e4 @ ( e2 @ op ) )
= e1 ),
inference(simplifyReflect,[status(thm)],[406,22279,14250,55322,50237]) ).
thf(63448,plain,
( sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ( e1 != e1 )
| ( e1 != e1 ) ),
inference(rewrite,[status(thm)],[305,62113,49570,62131,49572,52265,59035,49580,58700,62095]) ).
thf(63449,plain,
( sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6 ),
inference(simp,[status(thm)],[63448]) ).
thf(63450,plain,
( ( sk8 != sk8 )
| sk11
| ~ sk10
| ~ sk9
| ~ $true
| ~ sk7
| ~ sk6
| ~ sk7
| ~ sk6 ),
inference(paramod_ordered,[status(thm)],[63249,63449]) ).
thf(63451,plain,
( ( sk8 != sk8 )
| sk11
| ~ sk10
| ~ sk9
| ~ sk7
| ~ sk6 ),
inference(simp,[status(thm)],[63450]) ).
thf(63452,plain,
( sk11
| ~ sk10
| ~ sk9
| ~ sk7
| ~ sk6 ),
inference(pattern_uni,[status(thm)],[63451:[]]) ).
thf(64016,plain,
( ( sk10 != sk10 )
| sk11
| ~ $true
| ~ sk9
| ~ sk7
| ~ sk6
| ~ sk9
| ~ sk7
| ~ sk6 ),
inference(paramod_ordered,[status(thm)],[64002,63452]) ).
thf(64017,plain,
( ( sk10 != sk10 )
| sk11
| ~ sk9
| ~ sk7
| ~ sk6 ),
inference(simp,[status(thm)],[64016]) ).
thf(64018,plain,
( sk11
| ~ sk9
| ~ sk7
| ~ sk6 ),
inference(pattern_uni,[status(thm)],[64017:[]]) ).
thf(67,plain,
( ( ( e4 @ ( e3 @ op ) )
!= ( e3 @ ( e4 @ op ) ) )
| ~ sk18
| ~ sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) ),
inference(cnfConj,[status(thm)],[11]) ).
thf(313,plain,
( ~ sk18
| ~ sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e3 @ ( e4 @ op ) )
!= ( e4 @ ( e3 @ op ) ) )
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) ),
inference(lifteq,[status(thm)],[67]) ).
thf(64037,plain,
( ~ sk18
| ~ sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ( e0 != e0 )
| ( e1 != e1 ) ),
inference(rewrite,[status(thm)],[313,54960,62113,49570,62131,49572,52265,49580,54863,62095]) ).
thf(64038,plain,
( ~ sk18
| ~ sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6 ),
inference(simp,[status(thm)],[64037]) ).
thf(64039,plain,
( ( sk11 != sk11 )
| ~ sk18
| ~ sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ $true
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk9
| ~ sk7
| ~ sk6 ),
inference(paramod_ordered,[status(thm)],[64018,64038]) ).
thf(64040,plain,
( ( sk11 != sk11 )
| ~ sk18
| ~ sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk10
| ~ sk8
| ~ sk9
| ~ sk7
| ~ sk6 ),
inference(simp,[status(thm)],[64039]) ).
thf(64041,plain,
( ~ sk18
| ~ sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk10
| ~ sk8
| ~ sk9
| ~ sk7
| ~ sk6 ),
inference(pattern_uni,[status(thm)],[64040:[]]) ).
thf(69,plain,
( sk17
| ( ( e1 @ ( e1 @ ( e4 @ op ) @ op ) )
= e4 )
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) ),
inference(cnfConj,[status(thm)],[11]) ).
thf(188,plain,
( sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e4 @ op ) @ op ) )
= e4 )
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) ),
inference(lifteq,[status(thm)],[69]) ).
thf(1729,plain,
( ( sk4 != sk4 )
| sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ $true
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e4 @ op ) @ op ) )
= e4 )
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 )
| ( unit != e0 )
| ~ sk3
| ~ sk2
| ~ sk1 ),
inference(paramod_ordered,[status(thm)],[1378,188]) ).
thf(1730,plain,
( ( sk4 != sk4 )
| sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ( ( e1 @ ( e1 @ ( e4 @ op ) @ op ) )
= e4 )
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 )
| ( unit != e0 )
| ~ sk3
| ~ sk2
| ~ sk1 ),
inference(simp,[status(thm)],[1729]) ).
thf(1731,plain,
( sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ( ( e1 @ ( e1 @ ( e4 @ op ) @ op ) )
= e4 )
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 )
| ( unit != e0 )
| ~ sk3
| ~ sk2
| ~ sk1 ),
inference(pattern_uni,[status(thm)],[1730:[]]) ).
thf(119,plain,
( sk12
| ( ( e3 @ ( e0 @ op ) )
!= ( e0 @ ( e3 @ op ) ) )
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) ),
inference(cnfConj,[status(thm)],[11]) ).
thf(338,plain,
( sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e3 @ op ) )
!= ( e3 @ ( e0 @ op ) ) )
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) ),
inference(lifteq,[status(thm)],[119]) ).
thf(31,plain,
( sk7
| ( ( e1 @ ( e4 @ op ) )
!= ( e4 @ ( e1 @ op ) ) )
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) ),
inference(cnfConj,[status(thm)],[11]) ).
thf(316,plain,
( sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e4 @ op ) )
!= ( e4 @ ( e1 @ op ) ) )
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) ),
inference(lifteq,[status(thm)],[31]) ).
thf(387,plain,
( ( ( e1 @ ( e4 @ op ) )
= e4 )
| ( ( e1 @ ( e4 @ op ) )
= e3 )
| ( ( e1 @ ( e4 @ op ) )
= e2 )
| ( ( e1 @ ( e4 @ op ) )
= e1 )
| ( ( e1 @ ( e4 @ op ) )
= e0 ) ),
inference(cnfConj,[status(thm)],[366]) ).
thf(413,plain,
( ( ( e1 @ ( e4 @ op ) )
= e4 )
| ( ( e1 @ ( e4 @ op ) )
= e3 )
| ( ( e1 @ ( e4 @ op ) )
= e2 )
| ( ( e1 @ ( e4 @ op ) )
= e1 )
| ( ( e1 @ ( e4 @ op ) )
= e0 ) ),
inference(lifteq,[status(thm)],[387]) ).
thf(562,plain,
( ( e1 @ ( e4 @ op ) )
!= ( e4 @ ( e4 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(691,plain,
( ( e4 @ ( e4 @ op ) )
!= ( e1 @ ( e4 @ op ) ) ),
inference(lifteq,[status(thm)],[562]) ).
thf(9216,plain,
( ( e1 @ ( e4 @ op ) )
!= e2 ),
inference(rewrite,[status(thm)],[691,1627]) ).
thf(555,plain,
( ( e1 @ ( e4 @ op ) )
!= ( e3 @ ( e4 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(650,plain,
( ( e3 @ ( e4 @ op ) )
!= ( e1 @ ( e4 @ op ) ) ),
inference(lifteq,[status(thm)],[555]) ).
thf(55010,plain,
( ( e1 @ ( e4 @ op ) )
!= e0 ),
inference(rewrite,[status(thm)],[650,54863]) ).
thf(643,plain,
( ( e1 @ ( e0 @ op ) )
!= ( e1 @ ( e4 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(720,plain,
( ( e1 @ ( e4 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ),
inference(lifteq,[status(thm)],[643]) ).
thf(50503,plain,
( ( e1 @ ( e4 @ op ) )
!= e1 ),
inference(rewrite,[status(thm)],[720,49570]) ).
thf(552,plain,
( ( e1 @ ( e1 @ op ) )
!= ( e1 @ ( e4 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(703,plain,
( ( e1 @ ( e4 @ op ) )
!= ( e1 @ ( e1 @ op ) ) ),
inference(lifteq,[status(thm)],[552]) ).
thf(12445,plain,
( ( e1 @ ( e4 @ op ) )
!= e4 ),
inference(rewrite,[status(thm)],[703,776]) ).
thf(59729,plain,
( ( e1 @ ( e4 @ op ) )
= e3 ),
inference(simplifyReflect,[status(thm)],[413,9216,55010,50503,12445]) ).
thf(368,plain,
( ( ( e4 @ ( e1 @ op ) )
= e4 )
| ( ( e4 @ ( e1 @ op ) )
= e3 )
| ( ( e4 @ ( e1 @ op ) )
= e2 )
| ( ( e4 @ ( e1 @ op ) )
= e1 )
| ( ( e4 @ ( e1 @ op ) )
= e0 ) ),
inference(cnfConj,[status(thm)],[366]) ).
thf(401,plain,
( ( ( e4 @ ( e1 @ op ) )
= e4 )
| ( ( e4 @ ( e1 @ op ) )
= e3 )
| ( ( e4 @ ( e1 @ op ) )
= e2 )
| ( ( e4 @ ( e1 @ op ) )
= e1 )
| ( ( e4 @ ( e1 @ op ) )
= e0 ) ),
inference(lifteq,[status(thm)],[368]) ).
thf(571,plain,
( ( e0 @ ( e1 @ op ) )
!= ( e4 @ ( e1 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(723,plain,
( ( e4 @ ( e1 @ op ) )
!= ( e0 @ ( e1 @ op ) ) ),
inference(lifteq,[status(thm)],[571]) ).
thf(51824,plain,
( ( e4 @ ( e1 @ op ) )
!= e1 ),
inference(rewrite,[status(thm)],[723,49580]) ).
thf(631,plain,
( ( e1 @ ( e1 @ op ) )
!= ( e4 @ ( e1 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(702,plain,
( ( e4 @ ( e1 @ op ) )
!= ( e1 @ ( e1 @ op ) ) ),
inference(lifteq,[status(thm)],[631]) ).
thf(12356,plain,
( ( e4 @ ( e1 @ op ) )
!= e4 ),
inference(rewrite,[status(thm)],[702,776]) ).
thf(627,plain,
( ( e2 @ ( e1 @ op ) )
!= ( e4 @ ( e1 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(726,plain,
( ( e4 @ ( e1 @ op ) )
!= ( e2 @ ( e1 @ op ) ) ),
inference(lifteq,[status(thm)],[627]) ).
thf(18309,plain,
( ( e4 @ ( e1 @ op ) )
!= e0 ),
inference(rewrite,[status(thm)],[726,2353]) ).
thf(566,plain,
( ( e4 @ ( e1 @ op ) )
!= ( e4 @ ( e4 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(668,plain,
( ( e4 @ ( e4 @ op ) )
!= ( e4 @ ( e1 @ op ) ) ),
inference(lifteq,[status(thm)],[566]) ).
thf(4120,plain,
( ( e4 @ ( e1 @ op ) )
!= e2 ),
inference(rewrite,[status(thm)],[668,1627]) ).
thf(57400,plain,
( ( e4 @ ( e1 @ op ) )
= e3 ),
inference(simplifyReflect,[status(thm)],[401,51824,12356,18309,4120]) ).
thf(64300,plain,
( sk7
| ~ sk6
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ( e3 != e3 )
| ( e1 != e1 ) ),
inference(rewrite,[status(thm)],[316,59729,62113,49570,62131,49572,57400,52265,49580,62095]) ).
thf(64301,plain,
( sk7
| ~ sk6 ),
inference(simp,[status(thm)],[64300]) ).
thf(54,plain,
( sk6
| ( ( e3 @ ( e3 @ ( e1 @ op ) @ op ) )
= e1 )
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) ),
inference(cnfConj,[status(thm)],[11]) ).
thf(279,plain,
( sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e3 @ ( e3 @ ( e1 @ op ) @ op ) )
= e1 )
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) ),
inference(lifteq,[status(thm)],[54]) ).
thf(374,plain,
( ( ( e3 @ ( e1 @ op ) )
= e4 )
| ( ( e3 @ ( e1 @ op ) )
= e3 )
| ( ( e3 @ ( e1 @ op ) )
= e2 )
| ( ( e3 @ ( e1 @ op ) )
= e1 )
| ( ( e3 @ ( e1 @ op ) )
= e0 ) ),
inference(cnfConj,[status(thm)],[366]) ).
thf(398,plain,
( ( ( e3 @ ( e1 @ op ) )
= e4 )
| ( ( e3 @ ( e1 @ op ) )
= e3 )
| ( ( e3 @ ( e1 @ op ) )
= e2 )
| ( ( e3 @ ( e1 @ op ) )
= e1 )
| ( ( e3 @ ( e1 @ op ) )
= e0 ) ),
inference(lifteq,[status(thm)],[374]) ).
thf(601,plain,
( ( e3 @ ( e0 @ op ) )
!= ( e3 @ ( e1 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(689,plain,
( ( e3 @ ( e1 @ op ) )
!= ( e3 @ ( e0 @ op ) ) ),
inference(lifteq,[status(thm)],[601]) ).
thf(50725,plain,
( ( e3 @ ( e1 @ op ) )
!= e3 ),
inference(rewrite,[status(thm)],[689,49573]) ).
thf(612,plain,
( ( e2 @ ( e1 @ op ) )
!= ( e3 @ ( e1 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(725,plain,
( ( e3 @ ( e1 @ op ) )
!= ( e2 @ ( e1 @ op ) ) ),
inference(lifteq,[status(thm)],[612]) ).
thf(18202,plain,
( ( e3 @ ( e1 @ op ) )
!= e0 ),
inference(rewrite,[status(thm)],[725,2353]) ).
thf(558,plain,
( ( e1 @ ( e1 @ op ) )
!= ( e3 @ ( e1 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(685,plain,
( ( e3 @ ( e1 @ op ) )
!= ( e1 @ ( e1 @ op ) ) ),
inference(lifteq,[status(thm)],[558]) ).
thf(8332,plain,
( ( e3 @ ( e1 @ op ) )
!= e4 ),
inference(rewrite,[status(thm)],[685,776]) ).
thf(550,plain,
( ( e0 @ ( e1 @ op ) )
!= ( e3 @ ( e1 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(645,plain,
( ( e3 @ ( e1 @ op ) )
!= ( e0 @ ( e1 @ op ) ) ),
inference(lifteq,[status(thm)],[550]) ).
thf(51822,plain,
( ( e3 @ ( e1 @ op ) )
!= e1 ),
inference(rewrite,[status(thm)],[645,49580]) ).
thf(56452,plain,
( ( e3 @ ( e1 @ op ) )
= e2 ),
inference(simplifyReflect,[status(thm)],[398,50725,18202,8332,51822]) ).
thf(60290,plain,
( sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ $true
| ~ $true
| ( ( e3 @ ( e2 @ op ) )
= e1 )
| ( e1 != e1 ) ),
inference(rewrite,[status(thm)],[279,49570,49572,56452,52265,49580]) ).
thf(60291,plain,
( sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ( ( e3 @ ( e2 @ op ) )
= e1 ) ),
inference(simp,[status(thm)],[60290]) ).
thf(60321,plain,
( ( ( e3 @ ( e2 @ op ) )
!= ( e3 @ ( e2 @ op ) ) )
| ( e4 = e1 )
| sk6
| ~ sk5
| ~ sk4
| ~ sk3 ),
inference(paramod_ordered,[status(thm)],[60291,60078]) ).
thf(60322,plain,
( ( e4 = e1 )
| sk6
| ~ sk5
| ~ sk4
| ~ sk3 ),
inference(pattern_uni,[status(thm)],[60321:[]]) ).
thf(65019,plain,
( ( e4 = e1 )
| sk6
| ~ $true
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[60322,62113,62131,62095]) ).
thf(65020,plain,
( ( e4 = e1 )
| sk6 ),
inference(simp,[status(thm)],[65019]) ).
thf(65021,plain,
sk6,
inference(simplifyReflect,[status(thm)],[65020,758]) ).
thf(65030,plain,
( sk7
| ~ $true ),
inference(rewrite,[status(thm)],[64301,65021]) ).
thf(65031,plain,
sk7,
inference(simp,[status(thm)],[65030]) ).
thf(64314,plain,
( ( sk7 != sk7 )
| sk8
| ~ $true
| ~ sk6
| ~ sk6 ),
inference(paramod_ordered,[status(thm)],[64301,63249]) ).
thf(64315,plain,
( ( sk7 != sk7 )
| sk8
| ~ sk6 ),
inference(simp,[status(thm)],[64314]) ).
thf(64316,plain,
( sk8
| ~ sk6 ),
inference(pattern_uni,[status(thm)],[64315:[]]) ).
thf(12,plain,
( sk9
| ( ( e2 @ ( e1 @ op ) )
!= ( e1 @ ( e2 @ op ) ) )
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) ),
inference(cnfConj,[status(thm)],[11]) ).
thf(278,plain,
( sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e2 @ op ) )
!= ( e2 @ ( e1 @ op ) ) )
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) ),
inference(lifteq,[status(thm)],[12]) ).
thf(60261,plain,
( sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ $true
| ~ $true
| ( e0 != e0 )
| ( e1 != e1 ) ),
inference(rewrite,[status(thm)],[278,2353,59505,49570,49572,52265,49580]) ).
thf(60262,plain,
( sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3 ),
inference(simp,[status(thm)],[60261]) ).
thf(60278,plain,
( ( sk4 != sk4 )
| sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ $true
| ~ sk3
| ~ sk3 ),
inference(paramod_ordered,[status(thm)],[52306,60262]) ).
thf(60279,plain,
( ( sk4 != sk4 )
| sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk3 ),
inference(simp,[status(thm)],[60278]) ).
thf(60280,plain,
( sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk3 ),
inference(pattern_uni,[status(thm)],[60279:[]]) ).
thf(64690,plain,
( sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[60280,62113,62095]) ).
thf(64691,plain,
( sk9
| ~ sk8
| ~ sk7
| ~ sk6 ),
inference(simp,[status(thm)],[64690]) ).
thf(64698,plain,
( ( sk7 != sk7 )
| sk9
| ~ sk8
| ~ $true
| ~ sk6
| ~ sk6 ),
inference(paramod_ordered,[status(thm)],[64301,64691]) ).
thf(64699,plain,
( ( sk7 != sk7 )
| sk9
| ~ sk8
| ~ sk6 ),
inference(simp,[status(thm)],[64698]) ).
thf(64700,plain,
( sk9
| ~ sk8
| ~ sk6 ),
inference(pattern_uni,[status(thm)],[64699:[]]) ).
thf(64731,plain,
( ( sk8 != sk8 )
| sk9
| ~ $true
| ~ sk6
| ~ sk6 ),
inference(paramod_ordered,[status(thm)],[64316,64700]) ).
thf(64732,plain,
( ( sk8 != sk8 )
| sk9
| ~ sk6 ),
inference(simp,[status(thm)],[64731]) ).
thf(64733,plain,
( sk9
| ~ sk6 ),
inference(pattern_uni,[status(thm)],[64732:[]]) ).
thf(64308,plain,
( ( sk7 != sk7 )
| sk11
| ~ sk9
| ~ $true
| ~ sk6
| ~ sk6 ),
inference(paramod_ordered,[status(thm)],[64301,64018]) ).
thf(64309,plain,
( ( sk7 != sk7 )
| sk11
| ~ sk9
| ~ sk6 ),
inference(simp,[status(thm)],[64308]) ).
thf(64310,plain,
( sk11
| ~ sk9
| ~ sk6 ),
inference(pattern_uni,[status(thm)],[64309:[]]) ).
thf(64858,plain,
( ( sk9 != sk9 )
| sk11
| ~ $true
| ~ sk6
| ~ sk6 ),
inference(paramod_ordered,[status(thm)],[64733,64310]) ).
thf(64859,plain,
( ( sk9 != sk9 )
| sk11
| ~ sk6 ),
inference(simp,[status(thm)],[64858]) ).
thf(64860,plain,
( sk11
| ~ sk6 ),
inference(pattern_uni,[status(thm)],[64859:[]]) ).
thf(65034,plain,
( sk11
| ~ $true ),
inference(rewrite,[status(thm)],[64860,65021]) ).
thf(65035,plain,
sk11,
inference(simp,[status(thm)],[65034]) ).
thf(65036,plain,
( sk9
| ~ $true ),
inference(rewrite,[status(thm)],[64733,65021]) ).
thf(65037,plain,
sk9,
inference(simp,[status(thm)],[65036]) ).
thf(64317,plain,
( ( sk7 != sk7 )
| sk10
| ~ sk9
| ~ $true
| ~ sk6
| ~ sk6 ),
inference(paramod_ordered,[status(thm)],[64301,64002]) ).
thf(64318,plain,
( ( sk7 != sk7 )
| sk10
| ~ sk9
| ~ sk6 ),
inference(simp,[status(thm)],[64317]) ).
thf(64319,plain,
( sk10
| ~ sk9
| ~ sk6 ),
inference(pattern_uni,[status(thm)],[64318:[]]) ).
thf(64855,plain,
( ( sk9 != sk9 )
| sk10
| ~ $true
| ~ sk6
| ~ sk6 ),
inference(paramod_ordered,[status(thm)],[64733,64319]) ).
thf(64856,plain,
( ( sk9 != sk9 )
| sk10
| ~ sk6 ),
inference(simp,[status(thm)],[64855]) ).
thf(64857,plain,
( sk10
| ~ sk6 ),
inference(pattern_uni,[status(thm)],[64856:[]]) ).
thf(65038,plain,
( sk10
| ~ $true ),
inference(rewrite,[status(thm)],[64857,65021]) ).
thf(65039,plain,
sk10,
inference(simp,[status(thm)],[65038]) ).
thf(65040,plain,
( sk8
| ~ $true ),
inference(rewrite,[status(thm)],[64316,65021]) ).
thf(65041,plain,
sk8,
inference(simp,[status(thm)],[65040]) ).
thf(65242,plain,
( sk12
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ( e3 != e3 )
| ( ( e1 @ ( e1 @ op ) )
= e0 ) ),
inference(rewrite,[status(thm)],[338,62113,49570,49572,49573,65031,52265,49579,65035,65037,62095,65039,65041,62131,65021]) ).
thf(65243,plain,
( sk12
| ( ( e1 @ ( e1 @ op ) )
= e0 ) ),
inference(simp,[status(thm)],[65242]) ).
thf(65303,plain,
( ( ( e1 @ ( e1 @ op ) )
!= ( e1 @ ( e1 @ op ) ) )
| ( e4 = e0 )
| sk12 ),
inference(paramod_ordered,[status(thm)],[65243,776]) ).
thf(65304,plain,
( ( e4 = e0 )
| sk12 ),
inference(pattern_uni,[status(thm)],[65303:[]]) ).
thf(65381,plain,
sk12,
inference(simplifyReflect,[status(thm)],[65304,765]) ).
thf(107,plain,
( sk15
| ( ( e4 @ ( e4 @ ( e3 @ op ) @ op ) )
= e3 )
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) ),
inference(cnfConj,[status(thm)],[11]) ).
thf(348,plain,
( sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e4 @ ( e4 @ ( e3 @ op ) @ op ) )
= e3 )
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) ),
inference(lifteq,[status(thm)],[107]) ).
thf(58,plain,
( sk13
| ( ( e3 @ ( e1 @ op ) )
!= ( e1 @ ( e3 @ op ) ) )
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) ),
inference(cnfConj,[status(thm)],[11]) ).
thf(339,plain,
( sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e3 @ op ) )
!= ( e3 @ ( e1 @ op ) ) )
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) ),
inference(lifteq,[status(thm)],[58]) ).
thf(371,plain,
( ( ( e1 @ ( e3 @ op ) )
= e4 )
| ( ( e1 @ ( e3 @ op ) )
= e3 )
| ( ( e1 @ ( e3 @ op ) )
= e2 )
| ( ( e1 @ ( e3 @ op ) )
= e1 )
| ( ( e1 @ ( e3 @ op ) )
= e0 ) ),
inference(cnfConj,[status(thm)],[366]) ).
thf(395,plain,
( ( ( e1 @ ( e3 @ op ) )
= e4 )
| ( ( e1 @ ( e3 @ op ) )
= e3 )
| ( ( e1 @ ( e3 @ op ) )
= e2 )
| ( ( e1 @ ( e3 @ op ) )
= e1 )
| ( ( e1 @ ( e3 @ op ) )
= e0 ) ),
inference(lifteq,[status(thm)],[371]) ).
thf(564,plain,
( ( e1 @ ( e0 @ op ) )
!= ( e1 @ ( e3 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(735,plain,
( ( e1 @ ( e3 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ),
inference(lifteq,[status(thm)],[564]) ).
thf(50497,plain,
( ( e1 @ ( e3 @ op ) )
!= e1 ),
inference(rewrite,[status(thm)],[735,49570]) ).
thf(595,plain,
( ( e1 @ ( e1 @ op ) )
!= ( e1 @ ( e3 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(724,plain,
( ( e1 @ ( e3 @ op ) )
!= ( e1 @ ( e1 @ op ) ) ),
inference(lifteq,[status(thm)],[595]) ).
thf(16885,plain,
( ( e1 @ ( e3 @ op ) )
!= e4 ),
inference(rewrite,[status(thm)],[724,776]) ).
thf(581,plain,
( ( e0 @ ( e3 @ op ) )
!= ( e1 @ ( e3 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(728,plain,
( ( e1 @ ( e3 @ op ) )
!= ( e0 @ ( e3 @ op ) ) ),
inference(lifteq,[status(thm)],[581]) ).
thf(51627,plain,
( ( e1 @ ( e3 @ op ) )
!= e3 ),
inference(rewrite,[status(thm)],[728,49579]) ).
thf(54489,plain,
( ( ( e1 @ ( e3 @ op ) )
= e2 )
| ( ( e1 @ ( e3 @ op ) )
= e0 ) ),
inference(simplifyReflect,[status(thm)],[395,50497,16885,51627]) ).
thf(638,plain,
( ( e1 @ ( e3 @ op ) )
!= ( e4 @ ( e3 @ op ) ) ),
inference(cnfConj,[status(thm)],[544]) ).
thf(658,plain,
( ( e4 @ ( e3 @ op ) )
!= ( e1 @ ( e3 @ op ) ) ),
inference(lifteq,[status(thm)],[638]) ).
thf(55326,plain,
( ( e1 @ ( e3 @ op ) )
!= e0 ),
inference(rewrite,[status(thm)],[658,54960]) ).
thf(55873,plain,
( ( e1 @ ( e3 @ op ) )
= e2 ),
inference(simplifyReflect,[status(thm)],[54489,55326]) ).
thf(65393,plain,
( sk13
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ( e2 != e2 )
| ( ( e1 @ ( e1 @ op ) )
= e0 ) ),
inference(rewrite,[status(thm)],[339,55873,62113,49570,49572,56452,65381,65031,52265,65035,65037,62095,65039,65041,62131,65021]) ).
thf(65394,plain,
( sk13
| ( ( e1 @ ( e1 @ op ) )
= e0 ) ),
inference(simp,[status(thm)],[65393]) ).
thf(65454,plain,
( ( ( e1 @ ( e1 @ op ) )
!= ( e1 @ ( e1 @ op ) ) )
| ( e4 = e0 )
| sk13 ),
inference(paramod_ordered,[status(thm)],[65394,776]) ).
thf(65455,plain,
( ( e4 = e0 )
| sk13 ),
inference(pattern_uni,[status(thm)],[65454:[]]) ).
thf(65532,plain,
sk13,
inference(simplifyReflect,[status(thm)],[65455,765]) ).
thf(65617,plain,
( sk15
| ~ sk14
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ( ( e4 @ ( e0 @ op ) )
= e3 )
| ( ( e0 @ ( e1 @ op ) )
!= e1 ) ),
inference(rewrite,[status(thm)],[348,62113,49570,49572,65381,65031,52265,65035,65037,62095,65039,54960,65041,62131,65532,65021]) ).
thf(65618,plain,
( sk15
| ~ sk14
| ( ( e4 @ ( e0 @ op ) )
= e3 )
| ( ( e0 @ ( e1 @ op ) )
!= e1 ) ),
inference(simp,[status(thm)],[65617]) ).
thf(65647,plain,
( ( ( e0 @ ( e1 @ op ) )
!= ( e0 @ ( e1 @ op ) ) )
| sk15
| ~ sk14
| ( ( e4 @ ( e0 @ op ) )
= e3 )
| ( e1 != e1 ) ),
inference(paramod_ordered,[status(thm)],[49580,65618]) ).
thf(65648,plain,
( ( ( e0 @ ( e1 @ op ) )
!= ( e0 @ ( e1 @ op ) ) )
| sk15
| ~ sk14
| ( ( e4 @ ( e0 @ op ) )
= e3 ) ),
inference(simp,[status(thm)],[65647]) ).
thf(65649,plain,
( sk15
| ~ sk14
| ( ( e4 @ ( e0 @ op ) )
= e3 ) ),
inference(pattern_uni,[status(thm)],[65648:[]]) ).
thf(79,plain,
( sk14
| ( ( e3 @ ( e2 @ op ) )
!= ( e2 @ ( e3 @ op ) ) )
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) ),
inference(cnfConj,[status(thm)],[11]) ).
thf(349,plain,
( sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e2 @ ( e3 @ op ) )
!= ( e3 @ ( e2 @ op ) ) )
| ( ( e1 @ ( e1 @ ( e0 @ op ) @ op ) )
= e0 ) ),
inference(lifteq,[status(thm)],[79]) ).
thf(65700,plain,
( sk14
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ( e4 != e4 )
| ( ( e1 @ ( e1 @ op ) )
= e0 ) ),
inference(rewrite,[status(thm)],[349,62113,49570,49572,65381,65031,52265,65035,65037,60078,62095,65039,65041,58226,62131,65532,65021]) ).
thf(65701,plain,
( sk14
| ( ( e1 @ ( e1 @ op ) )
= e0 ) ),
inference(simp,[status(thm)],[65700]) ).
thf(65762,plain,
( ( ( e1 @ ( e1 @ op ) )
!= ( e1 @ ( e1 @ op ) ) )
| ( e4 = e0 )
| sk14 ),
inference(paramod_ordered,[status(thm)],[65701,776]) ).
thf(65763,plain,
( ( e4 = e0 )
| sk14 ),
inference(pattern_uni,[status(thm)],[65762:[]]) ).
thf(65840,plain,
sk14,
inference(simplifyReflect,[status(thm)],[65763,765]) ).
thf(66407,plain,
( sk15
| ~ $true
| ( e4 = e3 ) ),
inference(rewrite,[status(thm)],[65649,49568,65840]) ).
thf(66408,plain,
( sk15
| ( e4 = e3 ) ),
inference(simp,[status(thm)],[66407]) ).
thf(752,plain,
e3 != e4,
inference(cnfConj,[status(thm)],[746]) ).
thf(763,plain,
e4 != e3,
inference(lifteq,[status(thm)],[752]) ).
thf(66409,plain,
sk15,
inference(simplifyReflect,[status(thm)],[66408,763]) ).
thf(183,plain,
( sk16
| ( ( e4 @ ( e0 @ op ) )
!= ( e0 @ ( e4 @ op ) ) )
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) ),
inference(cnfConj,[status(thm)],[11]) ).
thf(346,plain,
( sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e4 @ op ) )
!= ( e4 @ ( e0 @ op ) ) )
| ( ( e0 @ ( e1 @ op ) )
!= ( e1 @ ( e0 @ op ) ) ) ),
inference(lifteq,[status(thm)],[183]) ).
thf(65593,plain,
( sk16
| ~ sk15
| ~ sk14
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ( e4 != e4 )
| ( e1 != e1 ) ),
inference(rewrite,[status(thm)],[346,49568,62113,49570,49572,65381,65031,49576,52265,65035,49580,65037,62095,65039,65041,62131,65532,65021]) ).
thf(65594,plain,
( sk16
| ~ sk15
| ~ sk14 ),
inference(simp,[status(thm)],[65593]) ).
thf(65841,plain,
( sk16
| ~ sk15
| ~ $true ),
inference(rewrite,[status(thm)],[65594,65840]) ).
thf(65842,plain,
( sk16
| ~ sk15 ),
inference(simp,[status(thm)],[65841]) ).
thf(66412,plain,
( sk16
| ~ $true ),
inference(rewrite,[status(thm)],[65842,66409]) ).
thf(66413,plain,
sk16,
inference(simp,[status(thm)],[66412]) ).
thf(70298,plain,
( sk17
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ( ( e1 @ ( e3 @ op ) )
= e4 )
| ( ( e1 @ ( e1 @ op ) )
= e0 )
| ( e0 != e0 )
| ~ $true
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[1731,62113,49570,49572,65381,65031,66409,52265,65035,66413,65037,62095,65039,59729,65041,65840,49564,65532,65021]) ).
thf(70299,plain,
( sk17
| ( ( e1 @ ( e3 @ op ) )
= e4 )
| ( ( e1 @ ( e1 @ op ) )
= e0 ) ),
inference(simp,[status(thm)],[70298]) ).
thf(70337,plain,
( ( ( e1 @ ( e3 @ op ) )
!= ( e1 @ ( e3 @ op ) ) )
| ( e4 = e2 )
| sk17
| ( ( e1 @ ( e1 @ op ) )
= e0 ) ),
inference(paramod_ordered,[status(thm)],[70299,55873]) ).
thf(70338,plain,
( ( e4 = e2 )
| sk17
| ( ( e1 @ ( e1 @ op ) )
= e0 ) ),
inference(pattern_uni,[status(thm)],[70337:[]]) ).
thf(70434,plain,
( ( e4 = e2 )
| sk17
| ( e4 = e0 ) ),
inference(rewrite,[status(thm)],[70338,776]) ).
thf(70435,plain,
sk17,
inference(simplifyReflect,[status(thm)],[70434,764,765]) ).
thf(62,plain,
( sk18
| ( ( e4 @ ( e2 @ op ) )
!= ( e2 @ ( e4 @ op ) ) )
| ~ sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) ),
inference(cnfConj,[status(thm)],[11]) ).
thf(356,plain,
( sk18
| ~ sk17
| ~ sk16
| ~ sk15
| ~ sk14
| ~ sk13
| ~ sk12
| ~ sk11
| ~ sk10
| ~ sk9
| ~ sk8
| ~ sk7
| ~ sk6
| ~ sk5
| ~ sk4
| ~ sk3
| ~ sk2
| ~ sk1
| ( ( e2 @ ( e4 @ op ) )
!= ( e4 @ ( e2 @ op ) ) )
| ( ( e0 @ ( e1 @ ( e0 @ op ) @ op ) )
!= e1 ) ),
inference(lifteq,[status(thm)],[62]) ).
thf(66085,plain,
( sk18
| ~ sk17
| ~ sk16
| ~ sk15
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ( e1 != e1 )
| ( ( e0 @ ( e1 @ op ) )
!= e1 ) ),
inference(rewrite,[status(thm)],[356,62113,49570,49572,65381,65031,52265,65035,58700,65037,62095,65039,65041,65840,62131,59035,65532,65021]) ).
thf(66086,plain,
( sk18
| ~ sk17
| ~ sk16
| ~ sk15
| ( ( e0 @ ( e1 @ op ) )
!= e1 ) ),
inference(simp,[status(thm)],[66085]) ).
thf(66116,plain,
( ( ( e0 @ ( e1 @ op ) )
!= ( e0 @ ( e1 @ op ) ) )
| sk18
| ~ sk17
| ~ sk16
| ~ sk15
| ( e1 != e1 ) ),
inference(paramod_ordered,[status(thm)],[49580,66086]) ).
thf(66117,plain,
( ( ( e0 @ ( e1 @ op ) )
!= ( e0 @ ( e1 @ op ) ) )
| sk18
| ~ sk17
| ~ sk16
| ~ sk15 ),
inference(simp,[status(thm)],[66116]) ).
thf(66118,plain,
( sk18
| ~ sk17
| ~ sk16
| ~ sk15 ),
inference(pattern_uni,[status(thm)],[66117:[]]) ).
thf(66174,plain,
( ( sk16 != sk16 )
| sk18
| ~ sk17
| ~ $true
| ~ sk15
| ~ sk15 ),
inference(paramod_ordered,[status(thm)],[65842,66118]) ).
thf(66175,plain,
( ( sk16 != sk16 )
| sk18
| ~ sk17
| ~ sk15 ),
inference(simp,[status(thm)],[66174]) ).
thf(66176,plain,
( sk18
| ~ sk17
| ~ sk15 ),
inference(pattern_uni,[status(thm)],[66175:[]]) ).
thf(66410,plain,
( sk18
| ~ sk17
| ~ $true ),
inference(rewrite,[status(thm)],[66176,66409]) ).
thf(66411,plain,
( sk18
| ~ sk17 ),
inference(simp,[status(thm)],[66410]) ).
thf(70436,plain,
( sk18
| ~ $true ),
inference(rewrite,[status(thm)],[66411,70435]) ).
thf(70437,plain,
sk18,
inference(simp,[status(thm)],[70436]) ).
thf(76317,plain,
( ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[64041,70435,70437,65381,65031,66409,66413,65037,65039,65041,65840,65532,65021]) ).
thf(76318,plain,
$false,
inference(simp,[status(thm)],[76317]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG064+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.13/0.41 % Computer : n005.cluster.edu
% 0.13/0.41 % Model : x86_64 x86_64
% 0.13/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.41 % Memory : 8046.5625MB
% 0.13/0.41 % OS : Linux 6.8.0-71-generic
% 0.13/0.41 % CPULimit : 300
% 0.13/0.41 % WCLimit : 300
% 0.13/0.41 % DateTime : Sat Sep 26 21:04:32 UTC 2026
% 0.13/0.41 % CPUTime :
% 0.13/0.41 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.86/0.99 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.43/1.29 % [INFO] Parsing done (292ms).
% 1.90/1.30 % [INFO] Running in sequential loop mode.
% 2.34/1.69 % [INFO] eprover registered as external prover.
% 2.34/1.69 % [INFO] Scanning for conjecture ...
% 3.01/1.90 % [INFO] Found a conjecture (or negated_conjecture) and 6 axioms. Running axiom selection ...
% 3.01/1.97 % [INFO] Axiom selection finished. Selected 6 axioms (removed 0 axioms).
% 3.52/2.15 % [INFO] Problem is first-order (TPTP FOF).
% 3.52/2.18 % [INFO] Type checking passed.
% 3.52/2.18 % [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 ...
% 71.31/16.68 % [INFO] Killing All external provers ...
% 71.31/16.69 % Time passed: 16135ms (effective reasoning time: 15373ms)
% 71.31/16.69 % Solved by 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)>
% 71.31/16.69 % Axioms used in derivation (5): ax4, ax6, ax1, ax2, ax5
% 71.31/16.69 % No. of inferences in proof: 508
% 71.31/16.69 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 16135 ms resp. 15373 ms w/o parsing
% 49.53/16.95 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 49.53/16.95 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------