%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SEU496^1 : TPTP v9.3.1. Released v3.6.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 : n002.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 : Wed Sep 30 08:28:17 AM UTC 2026
% Result : Theorem 90.81s 19.36s
% Output : Refutation 78.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 33
% Syntax : Number of formulae : 586 ( 62 unt; 0 typ; 32 def)
% Number of atoms : 3432 ( 627 equ; 0 cnn)
% Maximal formula atoms : 50 ( 5 avg)
% Number of connectives : 8086 (1532 ~;1584 |; 102 &;4755 @)
% ( 0 <=>; 113 =>; 0 <=; 0 <~>)
% Maximal formula depth : 48 ( 7 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 346 ( 346 >; 0 *; 0 +; 0 <<)
% Number of symbols : 36 ( 33 usr; 8 con; 0-3 aty)
% Number of variables : 1914 (1200 ^; 687 !; 0 ?;1914 :)
% ( 0 !>; 0 ?*; 0 @-; 27 @+)
% Comments :
%------------------------------------------------------------------------------
thf(subrel_decl,type,
subrel: ( $i > $i > $o ) > ( $i > $i > $o ) > $o ).
thf(asymm_decl,type,
asymm: ( $i > $i > $o ) > $o ).
thf(trans_decl,type,
trans: ( $i > $i > $o ) > $o ).
thf(tc_decl,type,
tc: ( $i > $i > $o ) > $i > $i > $o ).
thf(so_decl,type,
so: ( $i > $i > $o ) > $o ).
thf(sk1_decl,type,
sk1: $i > $i > $o ).
thf(sk2_decl,type,
sk2: $o ).
thf(sk3_decl,type,
sk3: $i ).
thf(sk4_decl,type,
sk4: $i ).
thf(sk5_decl,type,
sk5: ( $i > $i > $o ) > $i ).
thf(sk6_decl,type,
sk6: ( $i > $i > $o ) > $i ).
thf(sk7_decl,type,
sk7: ( $i > $i > $o ) > $i ).
thf(sk8_decl,type,
sk8: ( $i > $i > $o ) > $i ).
thf(sk9_decl,type,
sk9: ( $i > $i > $o ) > $i ).
thf(sk10_decl,type,
sk10: ( $i > $i > $o ) > $i ).
thf(sk11_decl,type,
sk11: ( $i > $i > $o ) > $i ).
thf(sk12_decl,type,
sk12: ( $i > $i > $o ) > $i ).
thf(sk13_decl,type,
sk13: ( $i > $i > $o ) > $i ).
thf(sk14_decl,type,
sk14: ( $i > $i > $o ) > $i ).
thf(sk15_decl,type,
sk15: $i ).
thf(sk16_decl,type,
sk16: $i ).
thf(sk17_decl,type,
sk17: $i ).
thf(sk18_decl,type,
sk18: ( $i > $i > $o ) > $i ).
thf(sk19_decl,type,
sk19: ( $i > $i > $o ) > $i ).
thf(sk20_decl,type,
sk20: ( $i > $i > $o ) > $i ).
thf(sk21_decl,type,
sk21: ( $i > $i > $o ) > $i ).
thf(sk22_decl,type,
sk22: ( $i > $i > $o ) > $i ).
thf(sk23_decl,type,
sk23: ( $i > $i > $o ) > $i ).
thf(sk24_decl,type,
sk24: ( $i > $i > $o ) > $i ).
thf(sk25_decl,type,
sk25: ( $i > $i > $o ) > $i ).
thf(sk26_decl,type,
sk26: ( $i > $i > $o ) > $i ).
thf(sk27_decl,type,
sk27: ( $i > $i > $o ) > $i ).
thf(sk28_decl,type,
sk28: $i > $i > $o ).
thf(subrel_def,definition,
( subrel
= ( ^ [A: $i > $i > $o,B: $i > $i > $o] :
! [C: $i,D: $i] :
( ( A @ C @ D )
=> ( B @ C @ D ) ) ) ) ).
thf(asymm_def,definition,
( asymm
= ( ^ [A: $i > $i > $o] :
! [B: $i,C: $i] :
( ( A @ B @ C )
=> ~ ( A @ C @ B ) ) ) ) ).
thf(trans_def,definition,
( trans
= ( ^ [A: $i > $i > $o] :
! [B: $i,C: $i,D: $i] :
( ( ( A @ B @ C )
& ( A @ C @ D ) )
=> ( A @ B @ D ) ) ) ) ).
thf(tc_def,definition,
( tc
= ( ^ [A: $i > $i > $o,B: $i,C: $i] :
! [D: $i > $i > $o] :
( ( ( trans @ D )
& ( subrel @ A @ D ) )
=> ( D @ B @ C ) ) ) ) ).
thf(so_def,definition,
( so
= ( ^ [A: $i > $i > $o] :
( ( asymm @ A )
& ( trans @ A ) ) ) ) ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i > $i > $o] :
~ ( ( ! [B: $i,C: $i] :
( ( A @ B @ C )
=> ~ ( A @ C @ B ) )
& ! [B: $i,C: $i,D: $i] :
( ( ( A @ B @ C )
& ( A @ C @ D ) )
=> ( A @ B @ D ) ) )
=> ( ! [B: $i,C: $i] :
( ! [D: $i > $i > $o] :
( ( ! [E: $i,F: $i,G: $i] :
( ( ( D @ E @ F )
& ( D @ F @ G ) )
=> ( D @ E @ G ) )
& ! [E: $i,F: $i] :
( ( A @ E @ F )
=> ( D @ E @ F ) ) )
=> ( D @ B @ C ) )
=> ~ ! [D: $i > $i > $o] :
( ( ! [E: $i,F: $i,G: $i] :
( ( ( D @ E @ F )
& ( D @ F @ G ) )
=> ( D @ E @ G ) )
& ! [E: $i,F: $i] :
( ( A @ E @ F )
=> ( D @ E @ F ) ) )
=> ( D @ C @ B ) ) )
& ! [B: $i,C: $i,D: $i] :
( ( ! [E: $i > $i > $o] :
( ( ! [F: $i,G: $i,H: $i] :
( ( ( E @ F @ G )
& ( E @ G @ H ) )
=> ( E @ F @ H ) )
& ! [F: $i,G: $i] :
( ( A @ F @ G )
=> ( E @ F @ G ) ) )
=> ( E @ B @ C ) )
& ! [E: $i > $i > $o] :
( ( ! [F: $i,G: $i,H: $i] :
( ( ( E @ F @ G )
& ( E @ G @ H ) )
=> ( E @ F @ H ) )
& ! [F: $i,G: $i] :
( ( A @ F @ G )
=> ( E @ F @ G ) ) )
=> ( E @ C @ D ) ) )
=> ! [E: $i > $i > $o] :
( ( ! [F: $i,G: $i,H: $i] :
( ( ( E @ F @ G )
& ( E @ G @ H ) )
=> ( E @ F @ H ) )
& ! [F: $i,G: $i] :
( ( A @ F @ G )
=> ( E @ F @ G ) ) )
=> ( E @ B @ D ) ) ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: $i] :
~ ! [B: $i] :
( ! [C: $i > $i > $o] :
( ( ! [D: $i,E: $i,F: $i] :
( ( ( C @ D @ E )
& ( C @ E @ F ) )
=> ( C @ D @ F ) )
& ! [D: $i,E: $i] :
( ( sk1 @ D @ E )
=> ( C @ D @ E ) ) )
=> ( C @ A @ B ) )
=> ~ ! [C: $i > $i > $o] :
( ( ! [D: $i,E: $i,F: $i] :
( ( ( C @ D @ E )
& ( C @ E @ F ) )
=> ( C @ D @ F ) )
& ! [D: $i,E: $i] :
( ( sk1 @ D @ E )
=> ( C @ D @ E ) ) )
=> ( C @ B @ A ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( @+[A: $i] :
~ ( ! [B: $i > $i > $o] :
( ( ! [C: $i,D: $i,E: $i] :
( ( ( B @ C @ D )
& ( B @ D @ E ) )
=> ( B @ C @ E ) )
& ! [C: $i,D: $i] :
( ( sk1 @ C @ D )
=> ( B @ C @ D ) ) )
=> ( B @ sk3 @ A ) )
=> ~ ! [B: $i > $i > $o] :
( ( ! [C: $i,D: $i,E: $i] :
( ( ( B @ C @ D )
& ( B @ D @ E ) )
=> ( B @ C @ E ) )
& ! [C: $i,D: $i] :
( ( sk1 @ C @ D )
=> ( B @ C @ D ) ) )
=> ( B @ A @ sk3 ) ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( ^ [A: $i > $i > $o] :
@+[B: $i] :
~ ! [C: $i,D: $i] :
( ( ( A @ B @ C )
& ( A @ C @ D ) )
=> ( A @ B @ D ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( ^ [A: $i > $i > $o] :
@+[B: $i] :
~ ! [C: $i] :
( ( ( A @ ( sk5 @ A ) @ B )
& ( A @ B @ C ) )
=> ( A @ ( sk5 @ A ) @ C ) ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( ^ [A: $i > $i > $o] :
@+[B: $i] :
~ ( ( ( A @ ( sk5 @ A ) @ ( sk6 @ A ) )
& ( A @ ( sk6 @ A ) @ B ) )
=> ( A @ ( sk5 @ A ) @ B ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( ^ [A: $i > $i > $o] :
@+[B: $i] :
~ ! [C: $i] :
( ( sk1 @ B @ C )
=> ( A @ B @ C ) ) ) ) ).
thf(sk9_def,definition,
( sk9
= ( ^ [A: $i > $i > $o] :
@+[B: $i] :
~ ( ( sk1 @ ( sk8 @ A ) @ B )
=> ( A @ ( sk8 @ A ) @ B ) ) ) ) ).
thf(sk10_def,definition,
( sk10
= ( ^ [A: $i > $i > $o] :
@+[B: $i] :
~ ! [C: $i,D: $i] :
( ( ( A @ B @ C )
& ( A @ C @ D ) )
=> ( A @ B @ D ) ) ) ) ).
thf(sk11_def,definition,
( sk11
= ( ^ [A: $i > $i > $o] :
@+[B: $i] :
~ ! [C: $i] :
( ( ( A @ ( sk10 @ A ) @ B )
& ( A @ B @ C ) )
=> ( A @ ( sk10 @ A ) @ C ) ) ) ) ).
thf(sk12_def,definition,
( sk12
= ( ^ [A: $i > $i > $o] :
@+[B: $i] :
~ ( ( ( A @ ( sk10 @ A ) @ ( sk11 @ A ) )
& ( A @ ( sk11 @ A ) @ B ) )
=> ( A @ ( sk10 @ A ) @ B ) ) ) ) ).
thf(sk13_def,definition,
( sk13
= ( ^ [A: $i > $i > $o] :
@+[B: $i] :
~ ! [C: $i] :
( ( sk1 @ B @ C )
=> ( A @ B @ C ) ) ) ) ).
thf(sk14_def,definition,
( sk14
= ( ^ [A: $i > $i > $o] :
@+[B: $i] :
~ ( ( sk1 @ ( sk13 @ A ) @ B )
=> ( A @ ( sk13 @ A ) @ B ) ) ) ) ).
thf(sk15_def,definition,
( sk15
= ( @+[A: $i] :
~ ! [B: $i,C: $i] :
( ( ! [D: $i > $i > $o] :
( ( ! [E: $i,F: $i,G: $i] :
( ( ( D @ E @ F )
& ( D @ F @ G ) )
=> ( D @ E @ G ) )
& ! [E: $i,F: $i] :
( ( sk1 @ E @ F )
=> ( D @ E @ F ) ) )
=> ( D @ A @ B ) )
& ! [D: $i > $i > $o] :
( ( ! [E: $i,F: $i,G: $i] :
( ( ( D @ E @ F )
& ( D @ F @ G ) )
=> ( D @ E @ G ) )
& ! [E: $i,F: $i] :
( ( sk1 @ E @ F )
=> ( D @ E @ F ) ) )
=> ( D @ B @ C ) ) )
=> ! [D: $i > $i > $o] :
( ( ! [E: $i,F: $i,G: $i] :
( ( ( D @ E @ F )
& ( D @ F @ G ) )
=> ( D @ E @ G ) )
& ! [E: $i,F: $i] :
( ( sk1 @ E @ F )
=> ( D @ E @ F ) ) )
=> ( D @ A @ C ) ) ) ) ) ).
thf(sk16_def,definition,
( sk16
= ( @+[A: $i] :
~ ! [B: $i] :
( ( ! [C: $i > $i > $o] :
( ( ! [D: $i,E: $i,F: $i] :
( ( ( C @ D @ E )
& ( C @ E @ F ) )
=> ( C @ D @ F ) )
& ! [D: $i,E: $i] :
( ( sk1 @ D @ E )
=> ( C @ D @ E ) ) )
=> ( C @ sk15 @ A ) )
& ! [C: $i > $i > $o] :
( ( ! [D: $i,E: $i,F: $i] :
( ( ( C @ D @ E )
& ( C @ E @ F ) )
=> ( C @ D @ F ) )
& ! [D: $i,E: $i] :
( ( sk1 @ D @ E )
=> ( C @ D @ E ) ) )
=> ( C @ A @ B ) ) )
=> ! [C: $i > $i > $o] :
( ( ! [D: $i,E: $i,F: $i] :
( ( ( C @ D @ E )
& ( C @ E @ F ) )
=> ( C @ D @ F ) )
& ! [D: $i,E: $i] :
( ( sk1 @ D @ E )
=> ( C @ D @ E ) ) )
=> ( C @ sk15 @ B ) ) ) ) ) ).
thf(sk17_def,definition,
( sk17
= ( @+[A: $i] :
~ ( ( ! [B: $i > $i > $o] :
( ( ! [C: $i,D: $i,E: $i] :
( ( ( B @ C @ D )
& ( B @ D @ E ) )
=> ( B @ C @ E ) )
& ! [C: $i,D: $i] :
( ( sk1 @ C @ D )
=> ( B @ C @ D ) ) )
=> ( B @ sk15 @ sk16 ) )
& ! [B: $i > $i > $o] :
( ( ! [C: $i,D: $i,E: $i] :
( ( ( B @ C @ D )
& ( B @ D @ E ) )
=> ( B @ C @ E ) )
& ! [C: $i,D: $i] :
( ( sk1 @ C @ D )
=> ( B @ C @ D ) ) )
=> ( B @ sk16 @ A ) ) )
=> ! [B: $i > $i > $o] :
( ( ! [C: $i,D: $i,E: $i] :
( ( ( B @ C @ D )
& ( B @ D @ E ) )
=> ( B @ C @ E ) )
& ! [C: $i,D: $i] :
( ( sk1 @ C @ D )
=> ( B @ C @ D ) ) )
=> ( B @ sk15 @ A ) ) ) ) ) ).
thf(sk18_def,definition,
( sk18
= ( ^ [A: $i > $i > $o] :
@+[B: $i] :
~ ! [C: $i,D: $i] :
( ( ( A @ B @ C )
& ( A @ C @ D ) )
=> ( A @ B @ D ) ) ) ) ).
thf(sk19_def,definition,
( sk19
= ( ^ [A: $i > $i > $o] :
@+[B: $i] :
~ ! [C: $i] :
( ( ( A @ ( sk18 @ A ) @ B )
& ( A @ B @ C ) )
=> ( A @ ( sk18 @ A ) @ C ) ) ) ) ).
thf(sk20_def,definition,
( sk20
= ( ^ [A: $i > $i > $o] :
@+[B: $i] :
~ ( ( ( A @ ( sk18 @ A ) @ ( sk19 @ A ) )
& ( A @ ( sk19 @ A ) @ B ) )
=> ( A @ ( sk18 @ A ) @ B ) ) ) ) ).
thf(sk21_def,definition,
( sk21
= ( ^ [A: $i > $i > $o] :
@+[B: $i] :
~ ! [C: $i] :
( ( sk1 @ B @ C )
=> ( A @ B @ C ) ) ) ) ).
thf(sk22_def,definition,
( sk22
= ( ^ [A: $i > $i > $o] :
@+[B: $i] :
~ ( ( sk1 @ ( sk21 @ A ) @ B )
=> ( A @ ( sk21 @ A ) @ B ) ) ) ) ).
thf(sk23_def,definition,
( sk23
= ( ^ [A: $i > $i > $o] :
@+[B: $i] :
~ ! [C: $i,D: $i] :
( ( ( A @ B @ C )
& ( A @ C @ D ) )
=> ( A @ B @ D ) ) ) ) ).
thf(sk24_def,definition,
( sk24
= ( ^ [A: $i > $i > $o] :
@+[B: $i] :
~ ! [C: $i] :
( ( ( A @ ( sk23 @ A ) @ B )
& ( A @ B @ C ) )
=> ( A @ ( sk23 @ A ) @ C ) ) ) ) ).
thf(sk25_def,definition,
( sk25
= ( ^ [A: $i > $i > $o] :
@+[B: $i] :
~ ( ( ( A @ ( sk23 @ A ) @ ( sk24 @ A ) )
& ( A @ ( sk24 @ A ) @ B ) )
=> ( A @ ( sk23 @ A ) @ B ) ) ) ) ).
thf(sk26_def,definition,
( sk26
= ( ^ [A: $i > $i > $o] :
@+[B: $i] :
~ ! [C: $i] :
( ( sk1 @ B @ C )
=> ( A @ B @ C ) ) ) ) ).
thf(sk27_def,definition,
( sk27
= ( ^ [A: $i > $i > $o] :
@+[B: $i] :
~ ( ( sk1 @ ( sk26 @ A ) @ B )
=> ( A @ ( sk26 @ A ) @ B ) ) ) ) ).
thf(sk28_def,definition,
( sk28
= ( @+[A: $i > $i > $o] :
~ ( ( ! [B: $i,C: $i,D: $i] :
( ( ( A @ B @ C )
& ( A @ C @ D ) )
=> ( A @ B @ D ) )
& ! [B: $i,C: $i] :
( ( sk1 @ B @ C )
=> ( A @ B @ C ) ) )
=> ( A @ sk15 @ sk17 ) ) ) ) ).
thf(1,conjecture,
! [A: $i > $i > $o] :
( ( so @ A )
=> ( so @ ( tc @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitive_closure_of_strict_order_is_strict_order) ).
thf(2,negated_conjecture,
~ ! [A: $i > $i > $o] :
( ( so @ A )
=> ( so @ ( tc @ A ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(3,plain,
~ ! [A: $i > $i > $o] :
( ( ! [B: $i,C: $i] :
( ( A @ B @ C )
=> ~ ( A @ C @ B ) )
& ! [B: $i,C: $i,D: $i] :
( ( ( A @ B @ C )
& ( A @ C @ D ) )
=> ( A @ B @ D ) ) )
=> ( ! [B: $i,C: $i] :
( ! [D: $i > $i > $o] :
( ( ! [E: $i,F: $i,G: $i] :
( ( ( D @ E @ F )
& ( D @ F @ G ) )
=> ( D @ E @ G ) )
& ! [E: $i,F: $i] :
( ( A @ E @ F )
=> ( D @ E @ F ) ) )
=> ( D @ B @ C ) )
=> ~ ! [D: $i > $i > $o] :
( ( ! [E: $i,F: $i,G: $i] :
( ( ( D @ E @ F )
& ( D @ F @ G ) )
=> ( D @ E @ G ) )
& ! [E: $i,F: $i] :
( ( A @ E @ F )
=> ( D @ E @ F ) ) )
=> ( D @ C @ B ) ) )
& ! [B: $i,C: $i,D: $i] :
( ( ! [E: $i > $i > $o] :
( ( ! [F: $i,G: $i,H: $i] :
( ( ( E @ F @ G )
& ( E @ G @ H ) )
=> ( E @ F @ H ) )
& ! [F: $i,G: $i] :
( ( A @ F @ G )
=> ( E @ F @ G ) ) )
=> ( E @ B @ C ) )
& ! [E: $i > $i > $o] :
( ( ! [F: $i,G: $i,H: $i] :
( ( ( E @ F @ G )
& ( E @ G @ H ) )
=> ( E @ F @ H ) )
& ! [F: $i,G: $i] :
( ( A @ F @ G )
=> ( E @ F @ G ) ) )
=> ( E @ C @ D ) ) )
=> ! [E: $i > $i > $o] :
( ( ! [F: $i,G: $i,H: $i] :
( ( ( E @ F @ G )
& ( E @ G @ H ) )
=> ( E @ F @ H ) )
& ! [F: $i,G: $i] :
( ( A @ F @ G )
=> ( E @ F @ G ) ) )
=> ( E @ B @ D ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(4,plain,
! [N: $i,M: $i,L: $i,K: $i,J: $i,I: $i > $i > $o,H: $i > $i > $o,G: $i > $i > $o,F: $i > $i > $o,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ~ ( sk1 @ A @ B )
| ~ ( sk1 @ B @ A ) )
& ( ~ ( sk1 @ C @ D )
| ~ ( sk1 @ D @ E )
| ( sk1 @ C @ E ) )
& ( ( F @ ( sk5 @ F ) @ ( sk6 @ F ) )
| ( sk1 @ ( sk8 @ F ) @ ( sk9 @ F ) )
| ( F @ sk3 @ sk4 )
| ~ sk2 )
& ( ( F @ ( sk5 @ F ) @ ( sk6 @ F ) )
| ~ ( F @ ( sk8 @ F ) @ ( sk9 @ F ) )
| ( F @ sk3 @ sk4 )
| ~ sk2 )
& ( ( F @ ( sk6 @ F ) @ ( sk7 @ F ) )
| ( sk1 @ ( sk8 @ F ) @ ( sk9 @ F ) )
| ( F @ sk3 @ sk4 )
| ~ sk2 )
& ( ( F @ ( sk6 @ F ) @ ( sk7 @ F ) )
| ~ ( F @ ( sk8 @ F ) @ ( sk9 @ F ) )
| ( F @ sk3 @ sk4 )
| ~ sk2 )
& ( ~ ( F @ ( sk5 @ F ) @ ( sk7 @ F ) )
| ( sk1 @ ( sk8 @ F ) @ ( sk9 @ F ) )
| ( F @ sk3 @ sk4 )
| ~ sk2 )
& ( ~ ( F @ ( sk5 @ F ) @ ( sk7 @ F ) )
| ~ ( F @ ( sk8 @ F ) @ ( sk9 @ F ) )
| ( F @ sk3 @ sk4 )
| ~ sk2 )
& ( ( G @ ( sk10 @ G ) @ ( sk11 @ G ) )
| ( sk1 @ ( sk13 @ G ) @ ( sk14 @ G ) )
| ( G @ sk4 @ sk3 )
| ~ sk2 )
& ( ( G @ ( sk10 @ G ) @ ( sk11 @ G ) )
| ~ ( G @ ( sk13 @ G ) @ ( sk14 @ G ) )
| ( G @ sk4 @ sk3 )
| ~ sk2 )
& ( ( G @ ( sk11 @ G ) @ ( sk12 @ G ) )
| ( sk1 @ ( sk13 @ G ) @ ( sk14 @ G ) )
| ( G @ sk4 @ sk3 )
| ~ sk2 )
& ( ( G @ ( sk11 @ G ) @ ( sk12 @ G ) )
| ~ ( G @ ( sk13 @ G ) @ ( sk14 @ G ) )
| ( G @ sk4 @ sk3 )
| ~ sk2 )
& ( ~ ( G @ ( sk10 @ G ) @ ( sk12 @ G ) )
| ( sk1 @ ( sk13 @ G ) @ ( sk14 @ G ) )
| ( G @ sk4 @ sk3 )
| ~ sk2 )
& ( ~ ( G @ ( sk10 @ G ) @ ( sk12 @ G ) )
| ~ ( G @ ( sk13 @ G ) @ ( sk14 @ G ) )
| ( G @ sk4 @ sk3 )
| ~ sk2 )
& ( sk2
| ( H @ ( sk18 @ H ) @ ( sk19 @ H ) )
| ( sk1 @ ( sk21 @ H ) @ ( sk22 @ H ) )
| ( H @ sk15 @ sk16 ) )
& ( sk2
| ( H @ ( sk18 @ H ) @ ( sk19 @ H ) )
| ~ ( H @ ( sk21 @ H ) @ ( sk22 @ H ) )
| ( H @ sk15 @ sk16 ) )
& ( sk2
| ( H @ ( sk19 @ H ) @ ( sk20 @ H ) )
| ( sk1 @ ( sk21 @ H ) @ ( sk22 @ H ) )
| ( H @ sk15 @ sk16 ) )
& ( sk2
| ( H @ ( sk19 @ H ) @ ( sk20 @ H ) )
| ~ ( H @ ( sk21 @ H ) @ ( sk22 @ H ) )
| ( H @ sk15 @ sk16 ) )
& ( sk2
| ~ ( H @ ( sk18 @ H ) @ ( sk20 @ H ) )
| ( sk1 @ ( sk21 @ H ) @ ( sk22 @ H ) )
| ( H @ sk15 @ sk16 ) )
& ( sk2
| ~ ( H @ ( sk18 @ H ) @ ( sk20 @ H ) )
| ~ ( H @ ( sk21 @ H ) @ ( sk22 @ H ) )
| ( H @ sk15 @ sk16 ) )
& ( sk2
| ( I @ ( sk23 @ I ) @ ( sk24 @ I ) )
| ( sk1 @ ( sk26 @ I ) @ ( sk27 @ I ) )
| ( I @ sk16 @ sk17 ) )
& ( sk2
| ( I @ ( sk23 @ I ) @ ( sk24 @ I ) )
| ~ ( I @ ( sk26 @ I ) @ ( sk27 @ I ) )
| ( I @ sk16 @ sk17 ) )
& ( sk2
| ( I @ ( sk24 @ I ) @ ( sk25 @ I ) )
| ( sk1 @ ( sk26 @ I ) @ ( sk27 @ I ) )
| ( I @ sk16 @ sk17 ) )
& ( sk2
| ( I @ ( sk24 @ I ) @ ( sk25 @ I ) )
| ~ ( I @ ( sk26 @ I ) @ ( sk27 @ I ) )
| ( I @ sk16 @ sk17 ) )
& ( sk2
| ~ ( I @ ( sk23 @ I ) @ ( sk25 @ I ) )
| ( sk1 @ ( sk26 @ I ) @ ( sk27 @ I ) )
| ( I @ sk16 @ sk17 ) )
& ( sk2
| ~ ( I @ ( sk23 @ I ) @ ( sk25 @ I ) )
| ~ ( I @ ( sk26 @ I ) @ ( sk27 @ I ) )
| ( I @ sk16 @ sk17 ) )
& ( sk2
| ~ ( sk28 @ J @ K )
| ~ ( sk28 @ K @ L )
| ( sk28 @ J @ L ) )
& ( sk2
| ~ ( sk1 @ M @ N )
| ( sk28 @ M @ N ) )
& ( sk2
| ~ ( sk28 @ sk15 @ sk17 ) ) ),
inference(cnf,[status(esa)],[3]) ).
thf(24,plain,
! [A: $i > $i > $o] :
( ( A @ ( sk6 @ A ) @ ( sk7 @ A ) )
| ( sk1 @ ( sk8 @ A ) @ ( sk9 @ A ) )
| ( A @ sk3 @ sk4 )
| ~ sk2 ),
inference(cnfConj,[status(thm)],[4]) ).
thf(46,plain,
! [A: $i > $i > $o] :
( ( A @ ( sk6 @ A ) @ ( sk7 @ A ) )
| ( sk1 @ ( sk8 @ A ) @ ( sk9 @ A ) )
| ( A @ sk3 @ sk4 )
| ~ sk2 ),
inference(simp,[status(thm)],[24]) ).
thf(28,plain,
! [A: $i > $i > $o] :
( ( A @ ( sk6 @ A ) @ ( sk7 @ A ) )
| ~ ( A @ ( sk8 @ A ) @ ( sk9 @ A ) )
| ( A @ sk3 @ sk4 )
| ~ sk2 ),
inference(cnfConj,[status(thm)],[4]) ).
thf(50,plain,
! [A: $i > $i > $o] :
( ( A @ ( sk6 @ A ) @ ( sk7 @ A ) )
| ~ ( A @ ( sk8 @ A ) @ ( sk9 @ A ) )
| ( A @ sk3 @ sk4 )
| ~ sk2 ),
inference(simp,[status(thm)],[28]) ).
thf(8058,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( ( A @ ( sk6 @ A ) @ ( sk7 @ A ) )
| ( A @ sk3 @ sk4 )
| ~ sk2
| ( B @ ( sk6 @ B ) @ ( sk7 @ B ) )
| ~ $true
| ( B @ sk3 @ sk4 )
| ~ sk2
| ( ( sk1 @ ( sk8 @ A ) @ ( sk9 @ A ) )
!= ( B @ ( sk8 @ B ) @ ( sk9 @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[46,50]) ).
thf(8059,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( ( A @ ( sk6 @ A ) @ ( sk7 @ A ) )
| ( A @ sk3 @ sk4 )
| ~ sk2
| ( B @ ( sk6 @ B ) @ ( sk7 @ B ) )
| ( B @ sk3 @ sk4 )
| ( ( sk1 @ ( sk8 @ A ) @ ( sk9 @ A ) )
!= ( B @ ( sk8 @ B ) @ ( sk9 @ B ) ) ) ),
inference(simp,[status(thm)],[8058]) ).
thf(8135,plain,
( ( sk1 @ ( sk6 @ sk1 ) @ ( sk7 @ sk1 ) )
| ( sk1 @ sk3 @ sk4 )
| ~ sk2
| ( sk1 @ ( sk6 @ sk1 ) @ ( sk7 @ sk1 ) )
| ( sk1 @ sk3 @ sk4 ) ),
inference(pre_uni,[status(thm)],[8059:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 ))]]) ).
thf(8148,plain,
( ( sk1 @ ( sk6 @ sk1 ) @ ( sk7 @ sk1 ) )
| ( sk1 @ sk3 @ sk4 )
| ~ sk2 ),
inference(simp,[status(thm)],[8135]) ).
thf(31,plain,
! [B: $i,A: $i] :
( ~ ( sk1 @ A @ B )
| ~ ( sk1 @ B @ A ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(11392,plain,
! [B: $i,A: $i] :
( ( sk1 @ sk3 @ sk4 )
| ~ sk2
| ~ $true
| ~ ( sk1 @ B @ A )
| ( ( sk1 @ ( sk6 @ sk1 ) @ ( sk7 @ sk1 ) )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[8148,31]) ).
thf(11393,plain,
! [B: $i,A: $i] :
( ( sk1 @ sk3 @ sk4 )
| ~ sk2
| ~ ( sk1 @ B @ A )
| ( ( sk1 @ ( sk6 @ sk1 ) @ ( sk7 @ sk1 ) )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[11392]) ).
thf(11394,plain,
( ( sk1 @ sk3 @ sk4 )
| ~ sk2
| ~ ( sk1 @ ( sk7 @ sk1 ) @ ( sk6 @ sk1 ) ) ),
inference(pattern_uni,[status(thm)],[11393:[bind(A,$thf( sk6 @ sk1 )),bind(B,$thf( sk7 @ sk1 ))]]) ).
thf(13,plain,
! [A: $i > $i > $o] :
( sk2
| ( A @ ( sk19 @ A ) @ ( sk20 @ A ) )
| ( sk1 @ ( sk21 @ A ) @ ( sk22 @ A ) )
| ( A @ sk15 @ sk16 ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(39,plain,
! [A: $i > $i > $o] :
( sk2
| ( A @ ( sk19 @ A ) @ ( sk20 @ A ) )
| ( sk1 @ ( sk21 @ A ) @ ( sk22 @ A ) )
| ( A @ sk15 @ sk16 ) ),
inference(simp,[status(thm)],[13]) ).
thf(1327,plain,
( sk2
| sk2
| ( sk1
@ ( sk21
@ ^ [A: $i,B: $i] : sk2 )
@ ( sk22
@ ^ [A: $i,B: $i] : sk2 ) )
| sk2 ),
inference(prim_subst,[status(thm)],[39:[bind(A,$thf( ^ [B: $i] : ^ [C: $i] : sk2 ))]]) ).
thf(1401,plain,
( sk2
| ( sk1
@ ( sk21
@ ^ [A: $i,B: $i] : sk2 )
@ ( sk22
@ ^ [A: $i,B: $i] : sk2 ) ) ),
inference(simp,[status(thm)],[1327]) ).
thf(9,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( sk1 @ A @ B )
| ~ ( sk1 @ B @ C )
| ( sk1 @ A @ C ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(38,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( sk1 @ A @ B )
| ~ ( sk1 @ B @ C )
| ( sk1 @ A @ C ) ),
inference(simp,[status(thm)],[9]) ).
thf(12,plain,
! [B: $i,A: $i] :
( sk2
| ~ ( sk1 @ A @ B )
| ( sk28 @ A @ B ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(40,plain,
! [B: $i,A: $i] :
( sk2
| ~ ( sk1 @ A @ B )
| ( sk28 @ A @ B ) ),
inference(simp,[status(thm)],[12]) ).
thf(26,plain,
( sk2
| ~ ( sk28 @ sk15 @ sk17 ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(64,plain,
! [B: $i,A: $i] :
( sk2
| ~ ( sk1 @ A @ B )
| sk2
| ~ $true
| ( ( sk28 @ A @ B )
!= ( sk28 @ sk15 @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[40,26]) ).
thf(65,plain,
! [B: $i,A: $i] :
( sk2
| ~ ( sk1 @ A @ B )
| ( ( sk28 @ A @ B )
!= ( sk28 @ sk15 @ sk17 ) ) ),
inference(simp,[status(thm)],[64]) ).
thf(66,plain,
( sk2
| ~ ( sk1 @ sk15 @ sk17 ) ),
inference(pattern_uni,[status(thm)],[65:[bind(A,$thf( sk15 )),bind(B,$thf( sk17 ))]]) ).
thf(864,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( sk1 @ A @ B )
| ~ ( sk1 @ B @ C )
| sk2
| ~ $true
| ( ( sk1 @ A @ C )
!= ( sk1 @ sk15 @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[38,66]) ).
thf(865,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( sk1 @ A @ B )
| ~ ( sk1 @ B @ C )
| sk2
| ( ( sk1 @ A @ C )
!= ( sk1 @ sk15 @ sk17 ) ) ),
inference(simp,[status(thm)],[864]) ).
thf(866,plain,
! [A: $i] :
( ~ ( sk1 @ sk15 @ A )
| ~ ( sk1 @ A @ sk17 )
| sk2 ),
inference(pattern_uni,[status(thm)],[865:[bind(A,$thf( sk15 )),bind(B,$thf( B )),bind(C,$thf( sk17 ))]]) ).
thf(960,plain,
! [A: $i] :
( ~ ( sk1 @ sk15 @ A )
| ~ ( sk1 @ A @ sk17 )
| sk2 ),
inference(simp,[status(thm)],[866]) ).
thf(1515,plain,
! [A: $i] :
( sk2
| ~ $true
| ~ ( sk1 @ A @ sk17 )
| sk2
| ( ( sk1
@ ( sk21
@ ^ [B: $i,C: $i] : sk2 )
@ ( sk22
@ ^ [B: $i,C: $i] : sk2 ) )
!= ( sk1 @ sk15 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[1401,960]) ).
thf(1516,plain,
! [A: $i] :
( sk2
| ~ ( sk1 @ A @ sk17 )
| ( ( sk1
@ ( sk21
@ ^ [B: $i,C: $i] : sk2 )
@ ( sk22
@ ^ [B: $i,C: $i] : sk2 ) )
!= ( sk1 @ sk15 @ A ) ) ),
inference(simp,[status(thm)],[1515]) ).
thf(1535,plain,
! [A: $i] :
( sk2
| ~ ( sk1 @ A @ sk17 )
| ( ( sk21
@ ^ [B: $i,C: $i] : sk2 )
!= sk15 )
| ( ( sk22
@ ^ [B: $i,C: $i] : sk2 )
!= A ) ),
inference(simp,[status(thm)],[1516]) ).
thf(1549,plain,
( sk2
| ~ ( sk1
@ ( sk22
@ ^ [A: $i,B: $i] : sk2 )
@ sk17 )
| ( ( sk21
@ ^ [A: $i,B: $i] : sk2 )
!= sk15 ) ),
inference(simp,[status(thm)],[1535]) ).
thf(5,plain,
! [A: $i > $i > $o] :
( sk2
| ( A @ ( sk24 @ A ) @ ( sk25 @ A ) )
| ( sk1 @ ( sk26 @ A ) @ ( sk27 @ A ) )
| ( A @ sk16 @ sk17 ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(34,plain,
! [A: $i > $i > $o] :
( sk2
| ( A @ ( sk24 @ A ) @ ( sk25 @ A ) )
| ( sk1 @ ( sk26 @ A ) @ ( sk27 @ A ) )
| ( A @ sk16 @ sk17 ) ),
inference(simp,[status(thm)],[5]) ).
thf(179,plain,
( sk2
| $false
| ( sk1
@ ( sk26
@ ^ [A: $i,B: $i] : $false )
@ ( sk27
@ ^ [A: $i,B: $i] : $false ) )
| $false ),
inference(prim_subst,[status(thm)],[34:[bind(A,$thf( ^ [B: $i] : ^ [C: $i] : $false ))]]) ).
thf(202,plain,
( sk2
| ( sk1
@ ( sk26
@ ^ [A: $i,B: $i] : $false )
@ ( sk27
@ ^ [A: $i,B: $i] : $false ) ) ),
inference(simp,[status(thm)],[179]) ).
thf(61,plain,
! [B: $i,A: $i] :
( ~ ( sk1 @ A @ B )
| ( ( sk1 @ B @ A )
!= ( sk1 @ A @ B ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[31]) ).
thf(62,plain,
! [A: $i] :
~ ( sk1 @ A @ A ),
inference(pattern_uni,[status(thm)],[61:[bind(A,$thf( B ))]]) ).
thf(63,plain,
! [A: $i] :
~ ( sk1 @ A @ A ),
inference(simp,[status(thm)],[62]) ).
thf(325,plain,
! [A: $i] :
( sk2
| ~ $true
| ( ( sk1
@ ( sk26
@ ^ [B: $i,C: $i] : $false )
@ ( sk27
@ ^ [B: $i,C: $i] : $false ) )
!= ( sk1 @ A @ A ) ) ),
inference(paramod_ordered,[status(thm)],[202,63]) ).
thf(326,plain,
! [A: $i] :
( sk2
| ( ( sk1
@ ( sk26
@ ^ [B: $i,C: $i] : $false )
@ ( sk27
@ ^ [B: $i,C: $i] : $false ) )
!= ( sk1 @ A @ A ) ) ),
inference(simp,[status(thm)],[325]) ).
thf(348,plain,
! [A: $i] :
( sk2
| ( ( sk26
@ ^ [B: $i,C: $i] : $false )
!= A )
| ( ( sk27
@ ^ [B: $i,C: $i] : $false )
!= A ) ),
inference(simp,[status(thm)],[326]) ).
thf(352,plain,
( sk2
| ( ( sk27
@ ^ [A: $i,B: $i] : $false )
!= ( sk26
@ ^ [A: $i,B: $i] : $false ) ) ),
inference(simp,[status(thm)],[348]) ).
thf(18,plain,
! [A: $i > $i > $o] :
( ~ ( A @ ( sk10 @ A ) @ ( sk12 @ A ) )
| ~ ( A @ ( sk13 @ A ) @ ( sk14 @ A ) )
| ( A @ sk4 @ sk3 )
| ~ sk2 ),
inference(cnfConj,[status(thm)],[4]) ).
thf(42,plain,
! [A: $i > $i > $o] :
( ~ ( A @ ( sk10 @ A ) @ ( sk12 @ A ) )
| ~ ( A @ ( sk13 @ A ) @ ( sk14 @ A ) )
| ( A @ sk4 @ sk3 )
| ~ sk2 ),
inference(simp,[status(thm)],[18]) ).
thf(104,plain,
! [A: $i > $i > $o] :
( ~ ( A @ ( sk10 @ A ) @ ( sk12 @ A ) )
| ( A @ sk4 @ sk3 )
| ~ sk2
| ( ( A @ ( sk13 @ A ) @ ( sk14 @ A ) )
!= ( ~ ( A @ sk4 @ sk3 ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[42]) ).
thf(115,plain,
! [A: $i > $i > $o] :
( ( A @ sk4 @ sk3 )
| ~ ( A @ ( sk10 @ A ) @ ( sk12 @ A ) )
| ~ sk2
| ( ( A @ ( sk13 @ A ) @ ( sk14 @ A ) )
!= ( ~ ( A @ sk4 @ sk3 ) ) ) ),
inference(simp,[status(thm)],[104]) ).
thf(4170,plain,
( $false
| ( sk1
@ ( sk8
@ ^ [A: $i,B: $i] : $false )
@ ( sk9
@ ^ [A: $i,B: $i] : $false ) )
| $false
| ~ sk2 ),
inference(prim_subst,[status(thm)],[46:[bind(A,$thf( ^ [B: $i] : ^ [C: $i] : $false ))]]) ).
thf(4294,plain,
( ( sk1
@ ( sk8
@ ^ [A: $i,B: $i] : $false )
@ ( sk9
@ ^ [A: $i,B: $i] : $false ) )
| ~ sk2 ),
inference(simp,[status(thm)],[4170]) ).
thf(4433,plain,
! [A: $i] :
( ~ sk2
| ~ $true
| ( ( sk1
@ ( sk8
@ ^ [B: $i,C: $i] : $false )
@ ( sk9
@ ^ [B: $i,C: $i] : $false ) )
!= ( sk1 @ A @ A ) ) ),
inference(paramod_ordered,[status(thm)],[4294,63]) ).
thf(4434,plain,
! [A: $i] :
( ~ sk2
| ( ( sk1
@ ( sk8
@ ^ [B: $i,C: $i] : $false )
@ ( sk9
@ ^ [B: $i,C: $i] : $false ) )
!= ( sk1 @ A @ A ) ) ),
inference(simp,[status(thm)],[4433]) ).
thf(4498,plain,
! [A: $i] :
( ~ sk2
| ( ( sk8
@ ^ [B: $i,C: $i] : $false )
!= A )
| ( ( sk9
@ ^ [B: $i,C: $i] : $false )
!= A ) ),
inference(simp,[status(thm)],[4434]) ).
thf(4515,plain,
( ~ sk2
| ( ( sk9
@ ^ [A: $i,B: $i] : $false )
!= ( sk8
@ ^ [A: $i,B: $i] : $false ) ) ),
inference(simp,[status(thm)],[4498]) ).
thf(25,plain,
! [A: $i > $i > $o] :
( sk2
| ( A @ ( sk18 @ A ) @ ( sk19 @ A ) )
| ( sk1 @ ( sk21 @ A ) @ ( sk22 @ A ) )
| ( A @ sk15 @ sk16 ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(47,plain,
! [A: $i > $i > $o] :
( sk2
| ( A @ ( sk18 @ A ) @ ( sk19 @ A ) )
| ( sk1 @ ( sk21 @ A ) @ ( sk22 @ A ) )
| ( A @ sk15 @ sk16 ) ),
inference(simp,[status(thm)],[25]) ).
thf(30,plain,
! [A: $i > $i > $o] :
( sk2
| ( A @ ( sk18 @ A ) @ ( sk19 @ A ) )
| ~ ( A @ ( sk21 @ A ) @ ( sk22 @ A ) )
| ( A @ sk15 @ sk16 ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(59,plain,
! [A: $i > $i > $o] :
( sk2
| ( A @ ( sk18 @ A ) @ ( sk19 @ A ) )
| ~ ( A @ ( sk21 @ A ) @ ( sk22 @ A ) )
| ( A @ sk15 @ sk16 ) ),
inference(simp,[status(thm)],[30]) ).
thf(18389,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( sk2
| ( A @ ( sk18 @ A ) @ ( sk19 @ A ) )
| ( A @ sk15 @ sk16 )
| sk2
| ( B @ ( sk18 @ B ) @ ( sk19 @ B ) )
| ~ $true
| ( B @ sk15 @ sk16 )
| ( ( sk1 @ ( sk21 @ A ) @ ( sk22 @ A ) )
!= ( B @ ( sk21 @ B ) @ ( sk22 @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[47,59]) ).
thf(18390,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( sk2
| ( A @ ( sk18 @ A ) @ ( sk19 @ A ) )
| ( A @ sk15 @ sk16 )
| ( B @ ( sk18 @ B ) @ ( sk19 @ B ) )
| ( B @ sk15 @ sk16 )
| ( ( sk1 @ ( sk21 @ A ) @ ( sk22 @ A ) )
!= ( B @ ( sk21 @ B ) @ ( sk22 @ B ) ) ) ),
inference(simp,[status(thm)],[18389]) ).
thf(18407,plain,
( sk2
| ( sk1 @ ( sk18 @ sk1 ) @ ( sk19 @ sk1 ) )
| ( sk1 @ sk15 @ sk16 )
| ( sk1 @ ( sk18 @ sk1 ) @ ( sk19 @ sk1 ) )
| ( sk1 @ sk15 @ sk16 ) ),
inference(pre_uni,[status(thm)],[18390:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 ))]]) ).
thf(18459,plain,
( sk2
| ( sk1 @ ( sk18 @ sk1 ) @ ( sk19 @ sk1 ) )
| ( sk1 @ sk15 @ sk16 ) ),
inference(simp,[status(thm)],[18407]) ).
thf(14,plain,
! [A: $i > $i > $o] :
( ( A @ ( sk5 @ A ) @ ( sk6 @ A ) )
| ~ ( A @ ( sk8 @ A ) @ ( sk9 @ A ) )
| ( A @ sk3 @ sk4 )
| ~ sk2 ),
inference(cnfConj,[status(thm)],[4]) ).
thf(36,plain,
! [A: $i > $i > $o] :
( ( A @ ( sk5 @ A ) @ ( sk6 @ A ) )
| ~ ( A @ ( sk8 @ A ) @ ( sk9 @ A ) )
| ( A @ sk3 @ sk4 )
| ~ sk2 ),
inference(simp,[status(thm)],[14]) ).
thf(512,plain,
! [A: $i > $i > $o] :
( ~ ( A
@ ( sk5
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
@ ( sk6
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) ) )
| ~ ~ ( A
@ ( sk8
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
@ ( sk9
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) ) )
| ~ ( A @ sk3 @ sk4 )
| ~ sk2 ),
inference(prim_subst,[status(thm)],[36:[bind(A,$thf( ^ [C: $i] : ^ [D: $i] : ~ ( B @ C @ D ) ))]]) ).
thf(521,plain,
! [A: $i > $i > $o] :
( ~ ( A
@ ( sk5
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
@ ( sk6
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) ) )
| ( A
@ ( sk8
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
@ ( sk9
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) ) )
| ~ ( A @ sk3 @ sk4 )
| ~ sk2 ),
inference(cnf,[status(esa)],[512]) ).
thf(522,plain,
! [A: $i > $i > $o] :
( ~ ( A
@ ( sk5
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
@ ( sk6
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) ) )
| ( A
@ ( sk8
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
@ ( sk9
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) ) )
| ~ ( A @ sk3 @ sk4 )
| ~ sk2 ),
inference(simp,[status(thm)],[521]) ).
thf(29,plain,
! [A: $i > $i > $o] :
( ( A @ ( sk10 @ A ) @ ( sk11 @ A ) )
| ( sk1 @ ( sk13 @ A ) @ ( sk14 @ A ) )
| ( A @ sk4 @ sk3 )
| ~ sk2 ),
inference(cnfConj,[status(thm)],[4]) ).
thf(49,plain,
! [A: $i > $i > $o] :
( ( A @ ( sk10 @ A ) @ ( sk11 @ A ) )
| ( sk1 @ ( sk13 @ A ) @ ( sk14 @ A ) )
| ( A @ sk4 @ sk3 )
| ~ sk2 ),
inference(simp,[status(thm)],[29]) ).
thf(7281,plain,
! [A: $i > $i > $o] :
( ( sk1 @ ( sk13 @ A ) @ ( sk14 @ A ) )
| ( A @ sk4 @ sk3 )
| ~ sk2
| ( ( A @ ( sk10 @ A ) @ ( sk11 @ A ) )
!= ( ~ sk2 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[49]) ).
thf(7334,plain,
( ( sk1
@ ( sk13
@ ^ [A: $i,B: $i] : ~ sk2 )
@ ( sk14
@ ^ [A: $i,B: $i] : ~ sk2 ) )
| ~ sk2
| ~ sk2 ),
inference(pre_uni,[status(thm)],[7281:[bind(A,$thf( ^ [B: $i] : ^ [C: $i] : ~ ( sk2 ) ))]]) ).
thf(7493,plain,
( ( sk1
@ ( sk13
@ ^ [A: $i,B: $i] : ~ sk2 )
@ ( sk14
@ ^ [A: $i,B: $i] : ~ sk2 ) )
| ~ sk2
| ~ sk2 ),
inference(cnf,[status(esa)],[7334]) ).
thf(7494,plain,
( ( sk1
@ ( sk13
@ ^ [A: $i,B: $i] : ~ sk2 )
@ ( sk14
@ ^ [A: $i,B: $i] : ~ sk2 ) )
| ~ sk2 ),
inference(simp,[status(thm)],[7493]) ).
thf(8246,plain,
! [A: $i > $i > $o] :
( ~ ( A
@ ( sk5
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
@ ( sk6
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) ) )
| ~ ( A @ sk3 @ sk4 )
| ~ sk2
| ( sk1
@ ( sk13
@ ^ [B: $i,C: $i] : ~ sk2 )
@ ( sk14
@ ^ [B: $i,C: $i] : ~ $true ) )
| ~ sk2
| ( ( A
@ ( sk8
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
@ ( sk9
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) ) )
!= sk2 ) ),
inference(paramod_ordered,[status(thm)],[522,7494]) ).
thf(8247,plain,
! [A: $i > $i > $o] :
( ~ ( A
@ ( sk5
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
@ ( sk6
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) ) )
| ~ ( A @ sk3 @ sk4 )
| ~ sk2
| ( sk1
@ ( sk13
@ ^ [B: $i,C: $i] : ~ sk2 )
@ ( sk14
@ ^ [B: $i,C: $i] : $false ) )
| ( ( A
@ ( sk8
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
@ ( sk9
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) ) )
!= sk2 ) ),
inference(simp,[status(thm)],[8246]) ).
thf(8386,plain,
( ~ sk2
| ~ sk2
| ~ sk2
| ( sk1
@ ( sk13
@ ^ [A: $i,B: $i] : ~ sk2 )
@ ( sk14
@ ^ [A: $i,B: $i] : $false ) ) ),
inference(pre_uni,[status(thm)],[8247:[bind(A,$thf( ^ [B: $i] : ^ [C: $i] : sk2 ))]]) ).
thf(8426,plain,
( ~ sk2
| ( sk1
@ ( sk13
@ ^ [A: $i,B: $i] : ~ sk2 )
@ ( sk14
@ ^ [A: $i,B: $i] : $false ) ) ),
inference(simp,[status(thm)],[8386]) ).
thf(8573,plain,
! [A: $i] :
( ~ sk2
| ~ $true
| ( ( sk1
@ ( sk13
@ ^ [B: $i,C: $i] : ~ sk2 )
@ ( sk14
@ ^ [B: $i,C: $i] : $false ) )
!= ( sk1 @ A @ A ) ) ),
inference(paramod_ordered,[status(thm)],[8426,63]) ).
thf(8574,plain,
! [A: $i] :
( ~ sk2
| ( ( sk1
@ ( sk13
@ ^ [B: $i,C: $i] : ~ sk2 )
@ ( sk14
@ ^ [B: $i,C: $i] : $false ) )
!= ( sk1 @ A @ A ) ) ),
inference(simp,[status(thm)],[8573]) ).
thf(8663,plain,
! [A: $i] :
( ~ sk2
| ( ( sk13
@ ^ [B: $i,C: $i] : ~ sk2 )
!= A )
| ( ( sk14
@ ^ [B: $i,C: $i] : $false )
!= A ) ),
inference(simp,[status(thm)],[8574]) ).
thf(8695,plain,
( ~ sk2
| ( ( sk14
@ ^ [A: $i,B: $i] : $false )
!= ( sk13
@ ^ [A: $i,B: $i] : ~ sk2 ) ) ),
inference(simp,[status(thm)],[8663]) ).
thf(177,plain,
( sk2
| sk2
| ( sk1
@ ( sk26
@ ^ [A: $i,B: $i] : sk2 )
@ ( sk27
@ ^ [A: $i,B: $i] : sk2 ) )
| sk2 ),
inference(prim_subst,[status(thm)],[34:[bind(A,$thf( ^ [B: $i] : ^ [C: $i] : sk2 ))]]) ).
thf(199,plain,
( sk2
| ( sk1
@ ( sk26
@ ^ [A: $i,B: $i] : sk2 )
@ ( sk27
@ ^ [A: $i,B: $i] : sk2 ) ) ),
inference(simp,[status(thm)],[177]) ).
thf(223,plain,
! [A: $i] :
( sk2
| ~ $true
| ( ( sk1
@ ( sk26
@ ^ [B: $i,C: $i] : sk2 )
@ ( sk27
@ ^ [B: $i,C: $i] : sk2 ) )
!= ( sk1 @ A @ A ) ) ),
inference(paramod_ordered,[status(thm)],[199,63]) ).
thf(224,plain,
! [A: $i] :
( sk2
| ( ( sk1
@ ( sk26
@ ^ [B: $i,C: $i] : sk2 )
@ ( sk27
@ ^ [B: $i,C: $i] : sk2 ) )
!= ( sk1 @ A @ A ) ) ),
inference(simp,[status(thm)],[223]) ).
thf(243,plain,
! [A: $i] :
( sk2
| ( ( sk26
@ ^ [B: $i,C: $i] : sk2 )
!= A )
| ( ( sk27
@ ^ [B: $i,C: $i] : sk2 )
!= A ) ),
inference(simp,[status(thm)],[224]) ).
thf(247,plain,
( sk2
| ( ( sk27
@ ^ [A: $i,B: $i] : sk2 )
!= ( sk26
@ ^ [A: $i,B: $i] : sk2 ) ) ),
inference(simp,[status(thm)],[243]) ).
thf(16,plain,
! [A: $i > $i > $o] :
( sk2
| ( A @ ( sk19 @ A ) @ ( sk20 @ A ) )
| ~ ( A @ ( sk21 @ A ) @ ( sk22 @ A ) )
| ( A @ sk15 @ sk16 ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(57,plain,
! [A: $i > $i > $o] :
( sk2
| ( A @ ( sk19 @ A ) @ ( sk20 @ A ) )
| ~ ( A @ ( sk21 @ A ) @ ( sk22 @ A ) )
| ( A @ sk15 @ sk16 ) ),
inference(simp,[status(thm)],[16]) ).
thf(15095,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( sk2
| ( A @ ( sk19 @ A ) @ ( sk20 @ A ) )
| ( A @ sk15 @ sk16 )
| sk2
| ( B @ ( sk19 @ B ) @ ( sk20 @ B ) )
| ~ $true
| ( B @ sk15 @ sk16 )
| ( ( sk1 @ ( sk21 @ A ) @ ( sk22 @ A ) )
!= ( B @ ( sk21 @ B ) @ ( sk22 @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[39,57]) ).
thf(15096,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( sk2
| ( A @ ( sk19 @ A ) @ ( sk20 @ A ) )
| ( A @ sk15 @ sk16 )
| ( B @ ( sk19 @ B ) @ ( sk20 @ B ) )
| ( B @ sk15 @ sk16 )
| ( ( sk1 @ ( sk21 @ A ) @ ( sk22 @ A ) )
!= ( B @ ( sk21 @ B ) @ ( sk22 @ B ) ) ) ),
inference(simp,[status(thm)],[15095]) ).
thf(15150,plain,
( sk2
| ( sk1 @ ( sk19 @ sk1 ) @ ( sk20 @ sk1 ) )
| ( sk1 @ sk15 @ sk16 )
| ( sk1 @ ( sk19 @ sk1 ) @ ( sk20 @ sk1 ) )
| ( sk1 @ sk15 @ sk16 ) ),
inference(pre_uni,[status(thm)],[15096:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 ))]]) ).
thf(15190,plain,
( sk2
| ( sk1 @ ( sk19 @ sk1 ) @ ( sk20 @ sk1 ) )
| ( sk1 @ sk15 @ sk16 ) ),
inference(simp,[status(thm)],[15150]) ).
thf(23,plain,
! [A: $i > $i > $o] :
( sk2
| ( A @ ( sk23 @ A ) @ ( sk24 @ A ) )
| ( sk1 @ ( sk26 @ A ) @ ( sk27 @ A ) )
| ( A @ sk16 @ sk17 ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(58,plain,
! [A: $i > $i > $o] :
( sk2
| ( A @ ( sk23 @ A ) @ ( sk24 @ A ) )
| ( sk1 @ ( sk26 @ A ) @ ( sk27 @ A ) )
| ( A @ sk16 @ sk17 ) ),
inference(simp,[status(thm)],[23]) ).
thf(20,plain,
! [A: $i > $i > $o] :
( sk2
| ( A @ ( sk23 @ A ) @ ( sk24 @ A ) )
| ~ ( A @ ( sk26 @ A ) @ ( sk27 @ A ) )
| ( A @ sk16 @ sk17 ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(48,plain,
! [A: $i > $i > $o] :
( sk2
| ( A @ ( sk23 @ A ) @ ( sk24 @ A ) )
| ~ ( A @ ( sk26 @ A ) @ ( sk27 @ A ) )
| ( A @ sk16 @ sk17 ) ),
inference(simp,[status(thm)],[20]) ).
thf(16912,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( sk2
| ( A @ ( sk23 @ A ) @ ( sk24 @ A ) )
| ( A @ sk16 @ sk17 )
| sk2
| ( B @ ( sk23 @ B ) @ ( sk24 @ B ) )
| ~ $true
| ( B @ sk16 @ sk17 )
| ( ( sk1 @ ( sk26 @ A ) @ ( sk27 @ A ) )
!= ( B @ ( sk26 @ B ) @ ( sk27 @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[58,48]) ).
thf(16913,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( sk2
| ( A @ ( sk23 @ A ) @ ( sk24 @ A ) )
| ( A @ sk16 @ sk17 )
| ( B @ ( sk23 @ B ) @ ( sk24 @ B ) )
| ( B @ sk16 @ sk17 )
| ( ( sk1 @ ( sk26 @ A ) @ ( sk27 @ A ) )
!= ( B @ ( sk26 @ B ) @ ( sk27 @ B ) ) ) ),
inference(simp,[status(thm)],[16912]) ).
thf(17260,plain,
( sk2
| ( sk1 @ ( sk23 @ sk1 ) @ ( sk24 @ sk1 ) )
| ( sk1 @ sk16 @ sk17 )
| ( sk1 @ ( sk23 @ sk1 ) @ ( sk24 @ sk1 ) )
| ( sk1 @ sk16 @ sk17 ) ),
inference(pre_uni,[status(thm)],[16913:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 ))]]) ).
thf(17482,plain,
( sk2
| ( sk1 @ ( sk23 @ sk1 ) @ ( sk24 @ sk1 ) )
| ( sk1 @ sk16 @ sk17 ) ),
inference(simp,[status(thm)],[17260]) ).
thf(8,plain,
! [A: $i > $i > $o] :
( sk2
| ( A @ ( sk24 @ A ) @ ( sk25 @ A ) )
| ~ ( A @ ( sk26 @ A ) @ ( sk27 @ A ) )
| ( A @ sk16 @ sk17 ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(44,plain,
! [A: $i > $i > $o] :
( sk2
| ( A @ ( sk24 @ A ) @ ( sk25 @ A ) )
| ~ ( A @ ( sk26 @ A ) @ ( sk27 @ A ) )
| ( A @ sk16 @ sk17 ) ),
inference(simp,[status(thm)],[8]) ).
thf(2718,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( sk2
| ( A @ ( sk24 @ A ) @ ( sk25 @ A ) )
| ( A @ sk16 @ sk17 )
| sk2
| ( B @ ( sk24 @ B ) @ ( sk25 @ B ) )
| ~ $true
| ( B @ sk16 @ sk17 )
| ( ( sk1 @ ( sk26 @ A ) @ ( sk27 @ A ) )
!= ( B @ ( sk26 @ B ) @ ( sk27 @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[34,44]) ).
thf(2719,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( sk2
| ( A @ ( sk24 @ A ) @ ( sk25 @ A ) )
| ( A @ sk16 @ sk17 )
| ( B @ ( sk24 @ B ) @ ( sk25 @ B ) )
| ( B @ sk16 @ sk17 )
| ( ( sk1 @ ( sk26 @ A ) @ ( sk27 @ A ) )
!= ( B @ ( sk26 @ B ) @ ( sk27 @ B ) ) ) ),
inference(simp,[status(thm)],[2718]) ).
thf(2760,plain,
( sk2
| ( sk1 @ ( sk24 @ sk1 ) @ ( sk25 @ sk1 ) )
| ( sk1 @ sk16 @ sk17 )
| ( sk1 @ ( sk24 @ sk1 ) @ ( sk25 @ sk1 ) )
| ( sk1 @ sk16 @ sk17 ) ),
inference(pre_uni,[status(thm)],[2719:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 ))]]) ).
thf(2767,plain,
( sk2
| ( sk1 @ ( sk24 @ sk1 ) @ ( sk25 @ sk1 ) )
| ( sk1 @ sk16 @ sk17 ) ),
inference(simp,[status(thm)],[2760]) ).
thf(3351,plain,
! [B: $i,A: $i] :
( sk2
| ( sk1 @ sk16 @ sk17 )
| ~ $true
| ~ ( sk1 @ B @ A )
| ( ( sk1 @ ( sk24 @ sk1 ) @ ( sk25 @ sk1 ) )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[2767,31]) ).
thf(3352,plain,
! [B: $i,A: $i] :
( sk2
| ( sk1 @ sk16 @ sk17 )
| ~ ( sk1 @ B @ A )
| ( ( sk1 @ ( sk24 @ sk1 ) @ ( sk25 @ sk1 ) )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[3351]) ).
thf(3353,plain,
( sk2
| ( sk1 @ sk16 @ sk17 )
| ~ ( sk1 @ ( sk25 @ sk1 ) @ ( sk24 @ sk1 ) ) ),
inference(pattern_uni,[status(thm)],[3352:[bind(A,$thf( sk24 @ sk1 )),bind(B,$thf( sk25 @ sk1 ))]]) ).
thf(18878,plain,
( sk2
| ( sk1 @ sk16 @ sk17 )
| sk2
| ( sk1 @ sk16 @ sk17 )
| ~ $true
| ( ( sk1 @ ( sk25 @ sk1 ) @ ( sk24 @ sk1 ) )
!= ( sk1 @ ( sk23 @ sk1 ) @ ( sk24 @ sk1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[17482,3353]) ).
thf(18879,plain,
( sk2
| ( sk1 @ sk16 @ sk17 )
| ( ( sk1 @ ( sk25 @ sk1 ) @ ( sk24 @ sk1 ) )
!= ( sk1 @ ( sk23 @ sk1 ) @ ( sk24 @ sk1 ) ) ) ),
inference(simp,[status(thm)],[18878]) ).
thf(19070,plain,
( sk2
| ( sk1 @ sk16 @ sk17 )
| ( ( sk25 @ sk1 )
!= ( sk23 @ sk1 ) )
| ( ( sk24 @ sk1 )
!= ( sk24 @ sk1 ) ) ),
inference(simp,[status(thm)],[18879]) ).
thf(19090,plain,
( sk2
| ( sk1 @ sk16 @ sk17 )
| ( ( sk25 @ sk1 )
!= ( sk23 @ sk1 ) ) ),
inference(simp,[status(thm)],[19070]) ).
thf(20796,plain,
! [B: $i,A: $i] :
( sk2
| ( ( sk25 @ sk1 )
!= ( sk23 @ sk1 ) )
| sk2
| ~ $true
| ( sk28 @ A @ B )
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[19090,40]) ).
thf(20797,plain,
! [B: $i,A: $i] :
( sk2
| ( ( sk25 @ sk1 )
!= ( sk23 @ sk1 ) )
| ( sk28 @ A @ B )
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[20796]) ).
thf(20798,plain,
( sk2
| ( ( sk25 @ sk1 )
!= ( sk23 @ sk1 ) )
| ( sk28 @ sk16 @ sk17 ) ),
inference(pattern_uni,[status(thm)],[20797:[bind(A,$thf( sk16 )),bind(B,$thf( sk17 ))]]) ).
thf(7284,plain,
( $false
| ( sk1
@ ( sk13
@ ^ [A: $i,B: $i] : $false )
@ ( sk14
@ ^ [A: $i,B: $i] : $false ) )
| $false
| ~ sk2 ),
inference(prim_subst,[status(thm)],[49:[bind(A,$thf( ^ [B: $i] : ^ [C: $i] : $false ))]]) ).
thf(7463,plain,
( ( sk1
@ ( sk13
@ ^ [A: $i,B: $i] : $false )
@ ( sk14
@ ^ [A: $i,B: $i] : $false ) )
| ~ sk2 ),
inference(simp,[status(thm)],[7284]) ).
thf(7669,plain,
! [A: $i] :
( ~ sk2
| ~ $true
| ( ( sk1
@ ( sk13
@ ^ [B: $i,C: $i] : $false )
@ ( sk14
@ ^ [B: $i,C: $i] : $false ) )
!= ( sk1 @ A @ A ) ) ),
inference(paramod_ordered,[status(thm)],[7463,63]) ).
thf(7670,plain,
! [A: $i] :
( ~ sk2
| ( ( sk1
@ ( sk13
@ ^ [B: $i,C: $i] : $false )
@ ( sk14
@ ^ [B: $i,C: $i] : $false ) )
!= ( sk1 @ A @ A ) ) ),
inference(simp,[status(thm)],[7669]) ).
thf(7753,plain,
! [A: $i] :
( ~ sk2
| ( ( sk13
@ ^ [B: $i,C: $i] : $false )
!= A )
| ( ( sk14
@ ^ [B: $i,C: $i] : $false )
!= A ) ),
inference(simp,[status(thm)],[7670]) ).
thf(7781,plain,
( ~ sk2
| ( ( sk14
@ ^ [A: $i,B: $i] : $false )
!= ( sk13
@ ^ [A: $i,B: $i] : $false ) ) ),
inference(simp,[status(thm)],[7753]) ).
thf(335,plain,
! [B: $i,A: $i] :
( sk2
| ~ $true
| ~ ( sk1 @ B @ A )
| ( ( sk1
@ ( sk26
@ ^ [C: $i,D: $i] : $false )
@ ( sk27
@ ^ [C: $i,D: $i] : $false ) )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[202,31]) ).
thf(336,plain,
! [B: $i,A: $i] :
( sk2
| ~ ( sk1 @ B @ A )
| ( ( sk1
@ ( sk26
@ ^ [C: $i,D: $i] : $false )
@ ( sk27
@ ^ [C: $i,D: $i] : $false ) )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[335]) ).
thf(337,plain,
( sk2
| ~ ( sk1
@ ( sk27
@ ^ [A: $i,B: $i] : $false )
@ ( sk26
@ ^ [A: $i,B: $i] : $false ) ) ),
inference(pattern_uni,[status(thm)],[336:[bind(A,$thf( sk26 @ ^ [C: $i] : ^ [D: $i] : $false )),bind(B,$thf( sk27 @ ^ [C: $i] : ^ [D: $i] : $false ))]]) ).
thf(1470,plain,
( sk2
| sk2
| ~ $true
| ( ( sk1
@ ( sk27
@ ^ [A: $i,B: $i] : $false )
@ ( sk26
@ ^ [A: $i,B: $i] : $false ) )
!= ( sk1
@ ( sk21
@ ^ [A: $i,B: $i] : sk2 )
@ ( sk22
@ ^ [A: $i,B: $i] : sk2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[1401,337]) ).
thf(1471,plain,
( sk2
| ( ( sk1
@ ( sk27
@ ^ [A: $i,B: $i] : $false )
@ ( sk26
@ ^ [A: $i,B: $i] : $false ) )
!= ( sk1
@ ( sk21
@ ^ [A: $i,B: $i] : sk2 )
@ ( sk22
@ ^ [A: $i,B: $i] : sk2 ) ) ) ),
inference(simp,[status(thm)],[1470]) ).
thf(1533,plain,
( sk2
| ( ( sk27
@ ^ [A: $i,B: $i] : $false )
!= ( sk21
@ ^ [A: $i,B: $i] : sk2 ) )
| ( ( sk26
@ ^ [A: $i,B: $i] : $false )
!= ( sk22
@ ^ [A: $i,B: $i] : sk2 ) ) ),
inference(simp,[status(thm)],[1471]) ).
thf(27,plain,
! [A: $i > $i > $o] :
( ( A @ ( sk10 @ A ) @ ( sk11 @ A ) )
| ~ ( A @ ( sk13 @ A ) @ ( sk14 @ A ) )
| ( A @ sk4 @ sk3 )
| ~ sk2 ),
inference(cnfConj,[status(thm)],[4]) ).
thf(56,plain,
! [A: $i > $i > $o] :
( ( A @ ( sk10 @ A ) @ ( sk11 @ A ) )
| ~ ( A @ ( sk13 @ A ) @ ( sk14 @ A ) )
| ( A @ sk4 @ sk3 )
| ~ sk2 ),
inference(simp,[status(thm)],[27]) ).
thf(21,plain,
! [A: $i > $i > $o] :
( sk2
| ~ ( A @ ( sk23 @ A ) @ ( sk25 @ A ) )
| ( sk1 @ ( sk26 @ A ) @ ( sk27 @ A ) )
| ( A @ sk16 @ sk17 ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(51,plain,
! [A: $i > $i > $o] :
( sk2
| ~ ( A @ ( sk23 @ A ) @ ( sk25 @ A ) )
| ( sk1 @ ( sk26 @ A ) @ ( sk27 @ A ) )
| ( A @ sk16 @ sk17 ) ),
inference(simp,[status(thm)],[21]) ).
thf(10,plain,
! [A: $i > $i > $o] :
( sk2
| ~ ( A @ ( sk23 @ A ) @ ( sk25 @ A ) )
| ~ ( A @ ( sk26 @ A ) @ ( sk27 @ A ) )
| ( A @ sk16 @ sk17 ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(35,plain,
! [A: $i > $i > $o] :
( sk2
| ~ ( A @ ( sk23 @ A ) @ ( sk25 @ A ) )
| ~ ( A @ ( sk26 @ A ) @ ( sk27 @ A ) )
| ( A @ sk16 @ sk17 ) ),
inference(simp,[status(thm)],[10]) ).
thf(9391,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( sk2
| ~ ( A @ ( sk23 @ A ) @ ( sk25 @ A ) )
| ( A @ sk16 @ sk17 )
| sk2
| ~ ( B @ ( sk23 @ B ) @ ( sk25 @ B ) )
| ~ $true
| ( B @ sk16 @ sk17 )
| ( ( sk1 @ ( sk26 @ A ) @ ( sk27 @ A ) )
!= ( B @ ( sk26 @ B ) @ ( sk27 @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[51,35]) ).
thf(9392,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( sk2
| ~ ( A @ ( sk23 @ A ) @ ( sk25 @ A ) )
| ( A @ sk16 @ sk17 )
| ~ ( B @ ( sk23 @ B ) @ ( sk25 @ B ) )
| ( B @ sk16 @ sk17 )
| ( ( sk1 @ ( sk26 @ A ) @ ( sk27 @ A ) )
!= ( B @ ( sk26 @ B ) @ ( sk27 @ B ) ) ) ),
inference(simp,[status(thm)],[9391]) ).
thf(9511,plain,
( sk2
| ~ ( sk1 @ ( sk23 @ sk1 ) @ ( sk25 @ sk1 ) )
| ( sk1 @ sk16 @ sk17 )
| ~ ( sk1 @ ( sk23 @ sk1 ) @ ( sk25 @ sk1 ) )
| ( sk1 @ sk16 @ sk17 ) ),
inference(pre_uni,[status(thm)],[9392:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 ))]]) ).
thf(9557,plain,
( sk2
| ~ ( sk1 @ ( sk23 @ sk1 ) @ ( sk25 @ sk1 ) )
| ( sk1 @ sk16 @ sk17 ) ),
inference(simp,[status(thm)],[9511]) ).
thf(12671,plain,
( sk2
| ( sk1 @ sk16 @ sk17 )
| sk2
| ~ $true
| ( sk1 @ sk16 @ sk17 )
| ( ( sk1 @ ( sk24 @ sk1 ) @ ( sk25 @ sk1 ) )
!= ( sk1 @ ( sk23 @ sk1 ) @ ( sk25 @ sk1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[2767,9557]) ).
thf(12672,plain,
( sk2
| ( sk1 @ sk16 @ sk17 )
| ( ( sk1 @ ( sk24 @ sk1 ) @ ( sk25 @ sk1 ) )
!= ( sk1 @ ( sk23 @ sk1 ) @ ( sk25 @ sk1 ) ) ) ),
inference(simp,[status(thm)],[12671]) ).
thf(12735,plain,
( sk2
| ( sk1 @ sk16 @ sk17 )
| ( ( sk24 @ sk1 )
!= ( sk23 @ sk1 ) )
| ( ( sk25 @ sk1 )
!= ( sk25 @ sk1 ) ) ),
inference(simp,[status(thm)],[12672]) ).
thf(12737,plain,
( sk2
| ( sk1 @ sk16 @ sk17 )
| ( ( sk24 @ sk1 )
!= ( sk23 @ sk1 ) ) ),
inference(simp,[status(thm)],[12735]) ).
thf(12850,plain,
! [B: $i,A: $i] :
( sk2
| ( ( sk24 @ sk1 )
!= ( sk23 @ sk1 ) )
| ~ $true
| ~ ( sk1 @ B @ A )
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[12737,31]) ).
thf(12851,plain,
! [B: $i,A: $i] :
( sk2
| ( ( sk24 @ sk1 )
!= ( sk23 @ sk1 ) )
| ~ ( sk1 @ B @ A )
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[12850]) ).
thf(12852,plain,
( sk2
| ( ( sk24 @ sk1 )
!= ( sk23 @ sk1 ) )
| ~ ( sk1 @ sk17 @ sk16 ) ),
inference(pattern_uni,[status(thm)],[12851:[bind(A,$thf( sk16 )),bind(B,$thf( sk17 ))]]) ).
thf(4165,plain,
! [A: $i > $i > $o] :
( ( sk1 @ ( sk8 @ A ) @ ( sk9 @ A ) )
| ( A @ sk3 @ sk4 )
| ~ sk2
| ( ( A @ ( sk6 @ A ) @ ( sk7 @ A ) )
!= ( ~ sk2 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[46]) ).
thf(4232,plain,
( ( sk1
@ ( sk8
@ ^ [A: $i,B: $i] : ~ sk2 )
@ ( sk9
@ ^ [A: $i,B: $i] : ~ sk2 ) )
| ~ sk2
| ~ sk2 ),
inference(pre_uni,[status(thm)],[4165:[bind(A,$thf( ^ [B: $i] : ^ [C: $i] : ~ ( sk2 ) ))]]) ).
thf(4271,plain,
( ( sk1
@ ( sk8
@ ^ [A: $i,B: $i] : ~ sk2 )
@ ( sk9
@ ^ [A: $i,B: $i] : ~ sk2 ) )
| ~ sk2
| ~ sk2 ),
inference(cnf,[status(esa)],[4232]) ).
thf(4272,plain,
( ( sk1
@ ( sk8
@ ^ [A: $i,B: $i] : ~ sk2 )
@ ( sk9
@ ^ [A: $i,B: $i] : ~ sk2 ) )
| ~ sk2 ),
inference(simp,[status(thm)],[4271]) ).
thf(4882,plain,
! [B: $i,A: $i] :
( ~ sk2
| ~ $true
| ~ ( sk1 @ B @ A )
| ( ( sk1
@ ( sk8
@ ^ [C: $i,D: $i] : ~ sk2 )
@ ( sk9
@ ^ [C: $i,D: $i] : ~ sk2 ) )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[4272,31]) ).
thf(4883,plain,
! [B: $i,A: $i] :
( ~ sk2
| ~ ( sk1 @ B @ A )
| ( ( sk1
@ ( sk8
@ ^ [C: $i,D: $i] : ~ sk2 )
@ ( sk9
@ ^ [C: $i,D: $i] : ~ sk2 ) )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[4882]) ).
thf(4884,plain,
( ~ sk2
| ~ ( sk1
@ ( sk9
@ ^ [A: $i,B: $i] : ~ sk2 )
@ ( sk8
@ ^ [A: $i,B: $i] : ~ sk2 ) ) ),
inference(pattern_uni,[status(thm)],[4883:[bind(A,$thf( sk8 @ ^ [C: $i] : ^ [D: $i] : ~ ( sk2 ) )),bind(B,$thf( sk9 @ ^ [C: $i] : ^ [D: $i] : ~ ( sk2 ) ))]]) ).
thf(20759,plain,
! [A: $i] :
( sk2
| ( ( sk25 @ sk1 )
!= ( sk23 @ sk1 ) )
| ~ $true
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ A @ A ) ) ),
inference(paramod_ordered,[status(thm)],[19090,63]) ).
thf(20760,plain,
! [A: $i] :
( sk2
| ( ( sk25 @ sk1 )
!= ( sk23 @ sk1 ) )
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ A @ A ) ) ),
inference(simp,[status(thm)],[20759]) ).
thf(20840,plain,
! [A: $i] :
( sk2
| ( ( sk25 @ sk1 )
!= ( sk23 @ sk1 ) )
| ( sk16 != A )
| ( sk17 != A ) ),
inference(simp,[status(thm)],[20760]) ).
thf(20882,plain,
( sk2
| ( ( sk25 @ sk1 )
!= ( sk23 @ sk1 ) )
| ( sk17 != sk16 ) ),
inference(simp,[status(thm)],[20840]) ).
thf(20743,plain,
( sk2
| ( ( sk25 @ sk1 )
!= ( sk23 @ sk1 ) )
| sk2
| ~ $true
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ sk15 @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[19090,66]) ).
thf(20744,plain,
( sk2
| ( ( sk25 @ sk1 )
!= ( sk23 @ sk1 ) )
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ sk15 @ sk17 ) ) ),
inference(simp,[status(thm)],[20743]) ).
thf(20843,plain,
( sk2
| ( ( sk25 @ sk1 )
!= ( sk23 @ sk1 ) )
| ( sk16 != sk15 )
| ( sk17 != sk17 ) ),
inference(simp,[status(thm)],[20744]) ).
thf(20885,plain,
( sk2
| ( ( sk25 @ sk1 )
!= ( sk23 @ sk1 ) )
| ( sk16 != sk15 ) ),
inference(simp,[status(thm)],[20843]) ).
thf(3334,plain,
! [A: $i] :
( sk2
| ( sk1 @ sk16 @ sk17 )
| ~ $true
| ( ( sk1 @ ( sk24 @ sk1 ) @ ( sk25 @ sk1 ) )
!= ( sk1 @ A @ A ) ) ),
inference(paramod_ordered,[status(thm)],[2767,63]) ).
thf(3335,plain,
! [A: $i] :
( sk2
| ( sk1 @ sk16 @ sk17 )
| ( ( sk1 @ ( sk24 @ sk1 ) @ ( sk25 @ sk1 ) )
!= ( sk1 @ A @ A ) ) ),
inference(simp,[status(thm)],[3334]) ).
thf(3387,plain,
! [A: $i] :
( sk2
| ( sk1 @ sk16 @ sk17 )
| ( ( sk24 @ sk1 )
!= A )
| ( ( sk25 @ sk1 )
!= A ) ),
inference(simp,[status(thm)],[3335]) ).
thf(3414,plain,
( sk2
| ( sk1 @ sk16 @ sk17 )
| ( ( sk25 @ sk1 )
!= ( sk24 @ sk1 ) ) ),
inference(simp,[status(thm)],[3387]) ).
thf(32,plain,
! [A: $i > $i > $o] :
( ( A @ ( sk5 @ A ) @ ( sk6 @ A ) )
| ( sk1 @ ( sk8 @ A ) @ ( sk9 @ A ) )
| ( A @ sk3 @ sk4 )
| ~ sk2 ),
inference(cnfConj,[status(thm)],[4]) ).
thf(53,plain,
! [A: $i > $i > $o] :
( ( A @ ( sk5 @ A ) @ ( sk6 @ A ) )
| ( sk1 @ ( sk8 @ A ) @ ( sk9 @ A ) )
| ( A @ sk3 @ sk4 )
| ~ sk2 ),
inference(simp,[status(thm)],[32]) ).
thf(10857,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( ( A @ ( sk5 @ A ) @ ( sk6 @ A ) )
| ( A @ sk3 @ sk4 )
| ~ sk2
| ( B @ ( sk5 @ B ) @ ( sk6 @ B ) )
| ~ $true
| ( B @ sk3 @ sk4 )
| ~ sk2
| ( ( sk1 @ ( sk8 @ A ) @ ( sk9 @ A ) )
!= ( B @ ( sk8 @ B ) @ ( sk9 @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[53,36]) ).
thf(10858,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( ( A @ ( sk5 @ A ) @ ( sk6 @ A ) )
| ( A @ sk3 @ sk4 )
| ~ sk2
| ( B @ ( sk5 @ B ) @ ( sk6 @ B ) )
| ( B @ sk3 @ sk4 )
| ( ( sk1 @ ( sk8 @ A ) @ ( sk9 @ A ) )
!= ( B @ ( sk8 @ B ) @ ( sk9 @ B ) ) ) ),
inference(simp,[status(thm)],[10857]) ).
thf(10968,plain,
( ( sk1 @ ( sk5 @ sk1 ) @ ( sk6 @ sk1 ) )
| ( sk1 @ sk3 @ sk4 )
| ~ sk2
| ( sk1 @ ( sk5 @ sk1 ) @ ( sk6 @ sk1 ) )
| ( sk1 @ sk3 @ sk4 ) ),
inference(pre_uni,[status(thm)],[10858:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 ))]]) ).
thf(11168,plain,
( ( sk1 @ ( sk5 @ sk1 ) @ ( sk6 @ sk1 ) )
| ( sk1 @ sk3 @ sk4 )
| ~ sk2 ),
inference(simp,[status(thm)],[10968]) ).
thf(14388,plain,
( ( sk1 @ sk3 @ sk4 )
| ~ sk2
| ( sk1 @ sk3 @ sk4 )
| ~ sk2
| ~ $true
| ( ( sk1 @ ( sk7 @ sk1 ) @ ( sk6 @ sk1 ) )
!= ( sk1 @ ( sk5 @ sk1 ) @ ( sk6 @ sk1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[11168,11394]) ).
thf(14389,plain,
( ( sk1 @ sk3 @ sk4 )
| ~ sk2
| ( ( sk1 @ ( sk7 @ sk1 ) @ ( sk6 @ sk1 ) )
!= ( sk1 @ ( sk5 @ sk1 ) @ ( sk6 @ sk1 ) ) ) ),
inference(simp,[status(thm)],[14388]) ).
thf(14467,plain,
( ( sk1 @ sk3 @ sk4 )
| ~ sk2
| ( ( sk7 @ sk1 )
!= ( sk5 @ sk1 ) )
| ( ( sk6 @ sk1 )
!= ( sk6 @ sk1 ) ) ),
inference(simp,[status(thm)],[14389]) ).
thf(14483,plain,
( ( sk1 @ sk3 @ sk4 )
| ~ sk2
| ( ( sk7 @ sk1 )
!= ( sk5 @ sk1 ) ) ),
inference(simp,[status(thm)],[14467]) ).
thf(6,plain,
! [A: $i > $i > $o] :
( ~ ( A @ ( sk5 @ A ) @ ( sk7 @ A ) )
| ~ ( A @ ( sk8 @ A ) @ ( sk9 @ A ) )
| ( A @ sk3 @ sk4 )
| ~ sk2 ),
inference(cnfConj,[status(thm)],[4]) ).
thf(37,plain,
! [A: $i > $i > $o] :
( ~ ( A @ ( sk5 @ A ) @ ( sk7 @ A ) )
| ~ ( A @ ( sk8 @ A ) @ ( sk9 @ A ) )
| ( A @ sk3 @ sk4 )
| ~ sk2 ),
inference(simp,[status(thm)],[6]) ).
thf(1328,plain,
( sk2
| $false
| ( sk1
@ ( sk21
@ ^ [A: $i,B: $i] : $false )
@ ( sk22
@ ^ [A: $i,B: $i] : $false ) )
| $false ),
inference(prim_subst,[status(thm)],[39:[bind(A,$thf( ^ [B: $i] : ^ [C: $i] : $false ))]]) ).
thf(1402,plain,
( sk2
| ( sk1
@ ( sk21
@ ^ [A: $i,B: $i] : $false )
@ ( sk22
@ ^ [A: $i,B: $i] : $false ) ) ),
inference(simp,[status(thm)],[1328]) ).
thf(1621,plain,
! [B: $i,A: $i] :
( sk2
| sk2
| ~ $true
| ( sk28 @ A @ B )
| ( ( sk1
@ ( sk21
@ ^ [C: $i,D: $i] : $false )
@ ( sk22
@ ^ [C: $i,D: $i] : $false ) )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[1402,40]) ).
thf(1622,plain,
! [B: $i,A: $i] :
( sk2
| ( sk28 @ A @ B )
| ( ( sk1
@ ( sk21
@ ^ [C: $i,D: $i] : $false )
@ ( sk22
@ ^ [C: $i,D: $i] : $false ) )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[1621]) ).
thf(1623,plain,
( sk2
| ( sk28
@ ( sk21
@ ^ [A: $i,B: $i] : $false )
@ ( sk22
@ ^ [A: $i,B: $i] : $false ) ) ),
inference(pattern_uni,[status(thm)],[1622:[bind(A,$thf( sk21 @ ^ [C: $i] : ^ [D: $i] : $false )),bind(B,$thf( sk22 @ ^ [C: $i] : ^ [D: $i] : $false ))]]) ).
thf(14628,plain,
! [B: $i,A: $i] :
( ~ sk2
| ( ( sk7 @ sk1 )
!= ( sk5 @ sk1 ) )
| ~ $true
| ~ ( sk1 @ B @ A )
| ( ( sk1 @ sk3 @ sk4 )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[14483,31]) ).
thf(14629,plain,
! [B: $i,A: $i] :
( ~ sk2
| ( ( sk7 @ sk1 )
!= ( sk5 @ sk1 ) )
| ~ ( sk1 @ B @ A )
| ( ( sk1 @ sk3 @ sk4 )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[14628]) ).
thf(14630,plain,
( ~ sk2
| ( ( sk7 @ sk1 )
!= ( sk5 @ sk1 ) )
| ~ ( sk1 @ sk4 @ sk3 ) ),
inference(pattern_uni,[status(thm)],[14629:[bind(A,$thf( sk3 )),bind(B,$thf( sk4 ))]]) ).
thf(33,plain,
! [A: $i > $i > $o] :
( sk2
| ~ ( A @ ( sk18 @ A ) @ ( sk20 @ A ) )
| ~ ( A @ ( sk21 @ A ) @ ( sk22 @ A ) )
| ( A @ sk15 @ sk16 ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(52,plain,
! [A: $i > $i > $o] :
( sk2
| ~ ( A @ ( sk18 @ A ) @ ( sk20 @ A ) )
| ~ ( A @ ( sk21 @ A ) @ ( sk22 @ A ) )
| ( A @ sk15 @ sk16 ) ),
inference(simp,[status(thm)],[33]) ).
thf(319,plain,
( sk2
| sk2
| ~ $true
| ( ( sk1
@ ( sk26
@ ^ [A: $i,B: $i] : $false )
@ ( sk27
@ ^ [A: $i,B: $i] : $false ) )
!= ( sk1 @ sk15 @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[202,66]) ).
thf(320,plain,
( sk2
| ( ( sk1
@ ( sk26
@ ^ [A: $i,B: $i] : $false )
@ ( sk27
@ ^ [A: $i,B: $i] : $false ) )
!= ( sk1 @ sk15 @ sk17 ) ) ),
inference(simp,[status(thm)],[319]) ).
thf(344,plain,
( sk2
| ( ( sk26
@ ^ [A: $i,B: $i] : $false )
!= sk15 )
| ( ( sk27
@ ^ [A: $i,B: $i] : $false )
!= sk17 ) ),
inference(simp,[status(thm)],[320]) ).
thf(4826,plain,
! [A: $i > $i > $o] :
( ~ ( A
@ ( sk5
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
@ ( sk6
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) ) )
| ~ ( A @ sk3 @ sk4 )
| ~ sk2
| ( sk1
@ ( sk8
@ ^ [B: $i,C: $i] : ~ sk2 )
@ ( sk9
@ ^ [B: $i,C: $i] : ~ $true ) )
| ~ sk2
| ( ( A
@ ( sk8
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
@ ( sk9
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) ) )
!= sk2 ) ),
inference(paramod_ordered,[status(thm)],[522,4272]) ).
thf(4827,plain,
! [A: $i > $i > $o] :
( ~ ( A
@ ( sk5
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
@ ( sk6
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) ) )
| ~ ( A @ sk3 @ sk4 )
| ~ sk2
| ( sk1
@ ( sk8
@ ^ [B: $i,C: $i] : ~ sk2 )
@ ( sk9
@ ^ [B: $i,C: $i] : $false ) )
| ( ( A
@ ( sk8
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
@ ( sk9
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) ) )
!= sk2 ) ),
inference(simp,[status(thm)],[4826]) ).
thf(4948,plain,
( ~ sk2
| ~ sk2
| ~ sk2
| ( sk1
@ ( sk8
@ ^ [A: $i,B: $i] : ~ sk2 )
@ ( sk9
@ ^ [A: $i,B: $i] : $false ) ) ),
inference(pre_uni,[status(thm)],[4827:[bind(A,$thf( ^ [B: $i] : ^ [C: $i] : sk2 ))]]) ).
thf(4975,plain,
( ~ sk2
| ( sk1
@ ( sk8
@ ^ [A: $i,B: $i] : ~ sk2 )
@ ( sk9
@ ^ [A: $i,B: $i] : $false ) ) ),
inference(simp,[status(thm)],[4948]) ).
thf(6057,plain,
! [B: $i,A: $i] :
( ~ sk2
| ~ $true
| ~ ( sk1 @ B @ A )
| ( ( sk1
@ ( sk8
@ ^ [C: $i,D: $i] : ~ sk2 )
@ ( sk9
@ ^ [C: $i,D: $i] : $false ) )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[4975,31]) ).
thf(6058,plain,
! [B: $i,A: $i] :
( ~ sk2
| ~ ( sk1 @ B @ A )
| ( ( sk1
@ ( sk8
@ ^ [C: $i,D: $i] : ~ sk2 )
@ ( sk9
@ ^ [C: $i,D: $i] : $false ) )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[6057]) ).
thf(6059,plain,
( ~ sk2
| ~ ( sk1
@ ( sk9
@ ^ [A: $i,B: $i] : $false )
@ ( sk8
@ ^ [A: $i,B: $i] : ~ sk2 ) ) ),
inference(pattern_uni,[status(thm)],[6058:[bind(A,$thf( sk8 @ ^ [C: $i] : ^ [D: $i] : ~ ( sk2 ) )),bind(B,$thf( sk9 @ ^ [C: $i] : ^ [D: $i] : $false ))]]) ).
thf(7653,plain,
( ~ sk2
| ~ sk2
| ~ $true
| ( ( sk1
@ ( sk13
@ ^ [A: $i,B: $i] : $false )
@ ( sk14
@ ^ [A: $i,B: $i] : $false ) )
!= ( sk1
@ ( sk9
@ ^ [A: $i,B: $i] : $false )
@ ( sk8
@ ^ [A: $i,B: $i] : ~ sk2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[7463,6059]) ).
thf(7654,plain,
( ~ sk2
| ( ( sk1
@ ( sk13
@ ^ [A: $i,B: $i] : $false )
@ ( sk14
@ ^ [A: $i,B: $i] : $false ) )
!= ( sk1
@ ( sk9
@ ^ [A: $i,B: $i] : $false )
@ ( sk8
@ ^ [A: $i,B: $i] : ~ sk2 ) ) ) ),
inference(simp,[status(thm)],[7653]) ).
thf(7743,plain,
( ~ sk2
| ( ( sk13
@ ^ [A: $i,B: $i] : $false )
!= ( sk9
@ ^ [A: $i,B: $i] : $false ) )
| ( ( sk14
@ ^ [A: $i,B: $i] : $false )
!= ( sk8
@ ^ [A: $i,B: $i] : ~ sk2 ) ) ),
inference(simp,[status(thm)],[7654]) ).
thf(1117,plain,
! [A: $i] :
( sk2
| ~ ( sk1 @ sk15 @ A )
| ~ $true
| sk2
| ( ( sk1
@ ( sk26
@ ^ [B: $i,C: $i] : sk2 )
@ ( sk27
@ ^ [B: $i,C: $i] : sk2 ) )
!= ( sk1 @ A @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[199,960]) ).
thf(1118,plain,
! [A: $i] :
( sk2
| ~ ( sk1 @ sk15 @ A )
| ( ( sk1
@ ( sk26
@ ^ [B: $i,C: $i] : sk2 )
@ ( sk27
@ ^ [B: $i,C: $i] : sk2 ) )
!= ( sk1 @ A @ sk17 ) ) ),
inference(simp,[status(thm)],[1117]) ).
thf(1122,plain,
! [A: $i] :
( sk2
| ~ ( sk1 @ sk15 @ A )
| ( ( sk26
@ ^ [B: $i,C: $i] : sk2 )
!= A )
| ( ( sk27
@ ^ [B: $i,C: $i] : sk2 )
!= sk17 ) ),
inference(simp,[status(thm)],[1118]) ).
thf(1132,plain,
( sk2
| ~ ( sk1 @ sk15
@ ( sk26
@ ^ [A: $i,B: $i] : sk2 ) )
| ( ( sk27
@ ^ [A: $i,B: $i] : sk2 )
!= sk17 ) ),
inference(simp,[status(thm)],[1122]) ).
thf(1512,plain,
! [B: $i,A: $i] :
( sk2
| sk2
| ~ $true
| ( sk28 @ A @ B )
| ( ( sk1
@ ( sk21
@ ^ [C: $i,D: $i] : sk2 )
@ ( sk22
@ ^ [C: $i,D: $i] : sk2 ) )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[1401,40]) ).
thf(1513,plain,
! [B: $i,A: $i] :
( sk2
| ( sk28 @ A @ B )
| ( ( sk1
@ ( sk21
@ ^ [C: $i,D: $i] : sk2 )
@ ( sk22
@ ^ [C: $i,D: $i] : sk2 ) )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[1512]) ).
thf(1514,plain,
( sk2
| ( sk28
@ ( sk21
@ ^ [A: $i,B: $i] : sk2 )
@ ( sk22
@ ^ [A: $i,B: $i] : sk2 ) ) ),
inference(pattern_uni,[status(thm)],[1513:[bind(A,$thf( sk21 @ ^ [C: $i] : ^ [D: $i] : sk2 )),bind(B,$thf( sk22 @ ^ [C: $i] : ^ [D: $i] : sk2 ))]]) ).
thf(11,plain,
! [A: $i > $i > $o] :
( ~ ( A @ ( sk5 @ A ) @ ( sk7 @ A ) )
| ( sk1 @ ( sk8 @ A ) @ ( sk9 @ A ) )
| ( A @ sk3 @ sk4 )
| ~ sk2 ),
inference(cnfConj,[status(thm)],[4]) ).
thf(43,plain,
! [A: $i > $i > $o] :
( ~ ( A @ ( sk5 @ A ) @ ( sk7 @ A ) )
| ( sk1 @ ( sk8 @ A ) @ ( sk9 @ A ) )
| ( A @ sk3 @ sk4 )
| ~ sk2 ),
inference(simp,[status(thm)],[11]) ).
thf(73,plain,
! [A: $i > $i > $o] :
( ~ ( A @ ( sk5 @ A ) @ ( sk7 @ A ) )
| ( A @ sk3 @ sk4 )
| ~ sk2
| ( ( A @ ( sk8 @ A ) @ ( sk9 @ A ) )
!= ( ~ ( A @ sk3 @ sk4 ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[37]) ).
thf(81,plain,
! [A: $i > $i > $o] :
( ( A @ sk3 @ sk4 )
| ~ ( A @ ( sk5 @ A ) @ ( sk7 @ A ) )
| ~ sk2
| ( ( A @ ( sk8 @ A ) @ ( sk9 @ A ) )
!= ( ~ ( A @ sk3 @ sk4 ) ) ) ),
inference(simp,[status(thm)],[73]) ).
thf(2353,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( ~ ( A @ ( sk5 @ A ) @ ( sk7 @ A ) )
| ( A @ sk3 @ sk4 )
| ~ sk2
| ( B @ sk3 @ sk4 )
| ~ ( B @ ( sk5 @ B ) @ ( sk7 @ B ) )
| ~ sk2
| ~ ~ ( B @ sk3 @ sk4 )
| ( ( sk1 @ ( sk8 @ A ) @ ( sk9 @ A ) )
!= ( B @ ( sk8 @ B ) @ ( sk9 @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[43,81]) ).
thf(2354,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( ~ ( A @ ( sk5 @ A ) @ ( sk7 @ A ) )
| ( A @ sk3 @ sk4 )
| ~ sk2
| ( B @ sk3 @ sk4 )
| ~ ( B @ ( sk5 @ B ) @ ( sk7 @ B ) )
| ( ( sk1 @ ( sk8 @ A ) @ ( sk9 @ A ) )
!= ( B @ ( sk8 @ B ) @ ( sk9 @ B ) ) ) ),
inference(simp,[status(thm)],[2353]) ).
thf(2438,plain,
( ~ ( sk1 @ ( sk5 @ sk1 ) @ ( sk7 @ sk1 ) )
| ( sk1 @ sk3 @ sk4 )
| ~ sk2
| ( sk1 @ sk3 @ sk4 )
| ~ ( sk1 @ ( sk5 @ sk1 ) @ ( sk7 @ sk1 ) ) ),
inference(pre_uni,[status(thm)],[2354:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 ))]]) ).
thf(2450,plain,
( ~ ( sk1 @ ( sk5 @ sk1 ) @ ( sk7 @ sk1 ) )
| ( sk1 @ sk3 @ sk4 )
| ~ sk2 ),
inference(simp,[status(thm)],[2438]) ).
thf(11338,plain,
( ( sk1 @ sk3 @ sk4 )
| ~ sk2
| ~ $true
| ( sk1 @ sk3 @ sk4 )
| ~ sk2
| ( ( sk1 @ ( sk6 @ sk1 ) @ ( sk7 @ sk1 ) )
!= ( sk1 @ ( sk5 @ sk1 ) @ ( sk7 @ sk1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[8148,2450]) ).
thf(11339,plain,
( ( sk1 @ sk3 @ sk4 )
| ~ sk2
| ( ( sk1 @ ( sk6 @ sk1 ) @ ( sk7 @ sk1 ) )
!= ( sk1 @ ( sk5 @ sk1 ) @ ( sk7 @ sk1 ) ) ) ),
inference(simp,[status(thm)],[11338]) ).
thf(11457,plain,
( ( sk1 @ sk3 @ sk4 )
| ~ sk2
| ( ( sk6 @ sk1 )
!= ( sk5 @ sk1 ) )
| ( ( sk7 @ sk1 )
!= ( sk7 @ sk1 ) ) ),
inference(simp,[status(thm)],[11339]) ).
thf(11467,plain,
( ( sk1 @ sk3 @ sk4 )
| ~ sk2
| ( ( sk6 @ sk1 )
!= ( sk5 @ sk1 ) ) ),
inference(simp,[status(thm)],[11457]) ).
thf(11607,plain,
! [B: $i,A: $i] :
( ~ sk2
| ( ( sk6 @ sk1 )
!= ( sk5 @ sk1 ) )
| ~ $true
| ~ ( sk1 @ B @ A )
| ( ( sk1 @ sk3 @ sk4 )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[11467,31]) ).
thf(11608,plain,
! [B: $i,A: $i] :
( ~ sk2
| ( ( sk6 @ sk1 )
!= ( sk5 @ sk1 ) )
| ~ ( sk1 @ B @ A )
| ( ( sk1 @ sk3 @ sk4 )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[11607]) ).
thf(11609,plain,
( ~ sk2
| ( ( sk6 @ sk1 )
!= ( sk5 @ sk1 ) )
| ~ ( sk1 @ sk4 @ sk3 ) ),
inference(pattern_uni,[status(thm)],[11608:[bind(A,$thf( sk3 )),bind(B,$thf( sk4 ))]]) ).
thf(14009,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( ( A @ ( sk10 @ A ) @ ( sk11 @ A ) )
| ( A @ sk4 @ sk3 )
| ~ sk2
| ( B @ ( sk10 @ B ) @ ( sk11 @ B ) )
| ~ $true
| ( B @ sk4 @ sk3 )
| ~ sk2
| ( ( sk1 @ ( sk13 @ A ) @ ( sk14 @ A ) )
!= ( B @ ( sk13 @ B ) @ ( sk14 @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[49,56]) ).
thf(14010,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( ( A @ ( sk10 @ A ) @ ( sk11 @ A ) )
| ( A @ sk4 @ sk3 )
| ~ sk2
| ( B @ ( sk10 @ B ) @ ( sk11 @ B ) )
| ( B @ sk4 @ sk3 )
| ( ( sk1 @ ( sk13 @ A ) @ ( sk14 @ A ) )
!= ( B @ ( sk13 @ B ) @ ( sk14 @ B ) ) ) ),
inference(simp,[status(thm)],[14009]) ).
thf(14085,plain,
( ( sk1 @ ( sk10 @ sk1 ) @ ( sk11 @ sk1 ) )
| ( sk1 @ sk4 @ sk3 )
| ~ sk2
| ( sk1 @ ( sk10 @ sk1 ) @ ( sk11 @ sk1 ) )
| ( sk1 @ sk4 @ sk3 ) ),
inference(pre_uni,[status(thm)],[14010:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 ))]]) ).
thf(14101,plain,
( ( sk1 @ ( sk10 @ sk1 ) @ ( sk11 @ sk1 ) )
| ( sk1 @ sk4 @ sk3 )
| ~ sk2 ),
inference(simp,[status(thm)],[14085]) ).
thf(17,plain,
! [A: $i > $i > $o] :
( ~ ( A @ ( sk10 @ A ) @ ( sk12 @ A ) )
| ( sk1 @ ( sk13 @ A ) @ ( sk14 @ A ) )
| ( A @ sk4 @ sk3 )
| ~ sk2 ),
inference(cnfConj,[status(thm)],[4]) ).
thf(54,plain,
! [A: $i > $i > $o] :
( ~ ( A @ ( sk10 @ A ) @ ( sk12 @ A ) )
| ( sk1 @ ( sk13 @ A ) @ ( sk14 @ A ) )
| ( A @ sk4 @ sk3 )
| ~ sk2 ),
inference(simp,[status(thm)],[17]) ).
thf(12162,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( ~ ( A @ ( sk10 @ A ) @ ( sk12 @ A ) )
| ( A @ sk4 @ sk3 )
| ~ sk2
| ~ ( B @ ( sk10 @ B ) @ ( sk12 @ B ) )
| ~ $true
| ( B @ sk4 @ sk3 )
| ~ sk2
| ( ( sk1 @ ( sk13 @ A ) @ ( sk14 @ A ) )
!= ( B @ ( sk13 @ B ) @ ( sk14 @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[54,42]) ).
thf(12163,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( ~ ( A @ ( sk10 @ A ) @ ( sk12 @ A ) )
| ( A @ sk4 @ sk3 )
| ~ sk2
| ~ ( B @ ( sk10 @ B ) @ ( sk12 @ B ) )
| ( B @ sk4 @ sk3 )
| ( ( sk1 @ ( sk13 @ A ) @ ( sk14 @ A ) )
!= ( B @ ( sk13 @ B ) @ ( sk14 @ B ) ) ) ),
inference(simp,[status(thm)],[12162]) ).
thf(12455,plain,
( ~ ( sk1 @ ( sk10 @ sk1 ) @ ( sk12 @ sk1 ) )
| ( sk1 @ sk4 @ sk3 )
| ~ sk2
| ~ ( sk1 @ ( sk10 @ sk1 ) @ ( sk12 @ sk1 ) )
| ( sk1 @ sk4 @ sk3 ) ),
inference(pre_uni,[status(thm)],[12163:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 ))]]) ).
thf(12493,plain,
( ~ ( sk1 @ ( sk10 @ sk1 ) @ ( sk12 @ sk1 ) )
| ( sk1 @ sk4 @ sk3 )
| ~ sk2 ),
inference(simp,[status(thm)],[12455]) ).
thf(15282,plain,
( ( sk1 @ sk4 @ sk3 )
| ~ sk2
| ~ $true
| ( sk1 @ sk4 @ sk3 )
| ~ sk2
| ( ( sk1 @ ( sk10 @ sk1 ) @ ( sk12 @ sk1 ) )
!= ( sk1 @ ( sk10 @ sk1 ) @ ( sk11 @ sk1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[14101,12493]) ).
thf(15283,plain,
( ( sk1 @ sk4 @ sk3 )
| ~ sk2
| ( ( sk1 @ ( sk10 @ sk1 ) @ ( sk12 @ sk1 ) )
!= ( sk1 @ ( sk10 @ sk1 ) @ ( sk11 @ sk1 ) ) ) ),
inference(simp,[status(thm)],[15282]) ).
thf(15429,plain,
( ( sk1 @ sk4 @ sk3 )
| ~ sk2
| ( ( sk10 @ sk1 )
!= ( sk10 @ sk1 ) )
| ( ( sk12 @ sk1 )
!= ( sk11 @ sk1 ) ) ),
inference(simp,[status(thm)],[15283]) ).
thf(15437,plain,
( ( sk1 @ sk4 @ sk3 )
| ~ sk2
| ( ( sk12 @ sk1 )
!= ( sk11 @ sk1 ) ) ),
inference(simp,[status(thm)],[15429]) ).
thf(11386,plain,
! [A: $i] :
( ( sk1 @ sk3 @ sk4 )
| ~ sk2
| ~ $true
| ( ( sk1 @ ( sk6 @ sk1 ) @ ( sk7 @ sk1 ) )
!= ( sk1 @ A @ A ) ) ),
inference(paramod_ordered,[status(thm)],[8148,63]) ).
thf(11387,plain,
! [A: $i] :
( ( sk1 @ sk3 @ sk4 )
| ~ sk2
| ( ( sk1 @ ( sk6 @ sk1 ) @ ( sk7 @ sk1 ) )
!= ( sk1 @ A @ A ) ) ),
inference(simp,[status(thm)],[11386]) ).
thf(11448,plain,
! [A: $i] :
( ( sk1 @ sk3 @ sk4 )
| ~ sk2
| ( ( sk6 @ sk1 )
!= A )
| ( ( sk7 @ sk1 )
!= A ) ),
inference(simp,[status(thm)],[11387]) ).
thf(11483,plain,
( ( sk1 @ sk3 @ sk4 )
| ~ sk2
| ( ( sk7 @ sk1 )
!= ( sk6 @ sk1 ) ) ),
inference(simp,[status(thm)],[11448]) ).
thf(11983,plain,
! [B: $i,A: $i] :
( ~ sk2
| ( ( sk7 @ sk1 )
!= ( sk6 @ sk1 ) )
| ~ $true
| ~ ( sk1 @ B @ A )
| ( ( sk1 @ sk3 @ sk4 )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[11483,31]) ).
thf(11984,plain,
! [B: $i,A: $i] :
( ~ sk2
| ( ( sk7 @ sk1 )
!= ( sk6 @ sk1 ) )
| ~ ( sk1 @ B @ A )
| ( ( sk1 @ sk3 @ sk4 )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[11983]) ).
thf(11985,plain,
( ~ sk2
| ( ( sk7 @ sk1 )
!= ( sk6 @ sk1 ) )
| ~ ( sk1 @ sk4 @ sk3 ) ),
inference(pattern_uni,[status(thm)],[11984:[bind(A,$thf( sk3 )),bind(B,$thf( sk4 ))]]) ).
thf(15657,plain,
( ~ sk2
| ( ( sk12 @ sk1 )
!= ( sk11 @ sk1 ) )
| ~ sk2
| ( ( sk7 @ sk1 )
!= ( sk6 @ sk1 ) )
| ~ $true
| ( ( sk1 @ sk4 @ sk3 )
!= ( sk1 @ sk4 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[15437,11985]) ).
thf(15658,plain,
( ~ sk2
| ( ( sk12 @ sk1 )
!= ( sk11 @ sk1 ) )
| ( ( sk7 @ sk1 )
!= ( sk6 @ sk1 ) )
| ( ( sk1 @ sk4 @ sk3 )
!= ( sk1 @ sk4 @ sk3 ) ) ),
inference(simp,[status(thm)],[15657]) ).
thf(15659,plain,
( ~ sk2
| ( ( sk12 @ sk1 )
!= ( sk11 @ sk1 ) )
| ( ( sk7 @ sk1 )
!= ( sk6 @ sk1 ) ) ),
inference(pattern_uni,[status(thm)],[15658:[]]) ).
thf(1115,plain,
! [A: $i] :
( sk2
| ~ $true
| ~ ( sk1 @ A @ sk17 )
| sk2
| ( ( sk1
@ ( sk26
@ ^ [B: $i,C: $i] : sk2 )
@ ( sk27
@ ^ [B: $i,C: $i] : sk2 ) )
!= ( sk1 @ sk15 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[199,960]) ).
thf(1116,plain,
! [A: $i] :
( sk2
| ~ ( sk1 @ A @ sk17 )
| ( ( sk1
@ ( sk26
@ ^ [B: $i,C: $i] : sk2 )
@ ( sk27
@ ^ [B: $i,C: $i] : sk2 ) )
!= ( sk1 @ sk15 @ A ) ) ),
inference(simp,[status(thm)],[1115]) ).
thf(1126,plain,
! [A: $i] :
( sk2
| ~ ( sk1 @ A @ sk17 )
| ( ( sk26
@ ^ [B: $i,C: $i] : sk2 )
!= sk15 )
| ( ( sk27
@ ^ [B: $i,C: $i] : sk2 )
!= A ) ),
inference(simp,[status(thm)],[1116]) ).
thf(1136,plain,
( sk2
| ~ ( sk1
@ ( sk27
@ ^ [A: $i,B: $i] : sk2 )
@ sk17 )
| ( ( sk26
@ ^ [A: $i,B: $i] : sk2 )
!= sk15 ) ),
inference(simp,[status(thm)],[1126]) ).
thf(926,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( sk1 @ A @ B )
| ~ ( sk1 @ B @ C )
| ~ $true
| ~ ( sk1 @ E @ D )
| ( ( sk1 @ A @ C )
!= ( sk1 @ D @ E ) ) ),
inference(paramod_ordered,[status(thm)],[38,31]) ).
thf(927,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( sk1 @ A @ B )
| ~ ( sk1 @ B @ C )
| ~ ( sk1 @ E @ D )
| ( ( sk1 @ A @ C )
!= ( sk1 @ D @ E ) ) ),
inference(simp,[status(thm)],[926]) ).
thf(928,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( sk1 @ A @ B )
| ~ ( sk1 @ B @ C )
| ~ ( sk1 @ C @ A ) ),
inference(pattern_uni,[status(thm)],[927:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( A )),bind(E,$thf( C ))]]) ).
thf(1018,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( sk1 @ A @ B )
| ~ ( sk1 @ B @ C )
| ~ ( sk1 @ D @ E )
| ~ $true
| ~ ( sk1 @ F @ D )
| ( ( sk1 @ A @ C )
!= ( sk1 @ E @ F ) ) ),
inference(paramod_ordered,[status(thm)],[38,928]) ).
thf(1019,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( sk1 @ A @ B )
| ~ ( sk1 @ B @ C )
| ~ ( sk1 @ D @ E )
| ~ ( sk1 @ F @ D )
| ( ( sk1 @ A @ C )
!= ( sk1 @ E @ F ) ) ),
inference(simp,[status(thm)],[1018]) ).
thf(1020,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( sk1 @ A @ B )
| ~ ( sk1 @ B @ C )
| ~ ( sk1 @ D @ A )
| ~ ( sk1 @ C @ D ) ),
inference(pattern_uni,[status(thm)],[1019:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( A )),bind(F,$thf( C ))]]) ).
thf(3525,plain,
! [A: $i] :
( sk2
| ( ( sk25 @ sk1 )
!= ( sk24 @ sk1 ) )
| ~ ( sk1 @ sk15 @ A )
| ~ $true
| sk2
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ A @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[3414,960]) ).
thf(3526,plain,
! [A: $i] :
( sk2
| ( ( sk25 @ sk1 )
!= ( sk24 @ sk1 ) )
| ~ ( sk1 @ sk15 @ A )
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ A @ sk17 ) ) ),
inference(simp,[status(thm)],[3525]) ).
thf(3527,plain,
( sk2
| ( ( sk25 @ sk1 )
!= ( sk24 @ sk1 ) )
| ~ ( sk1 @ sk15 @ sk16 ) ),
inference(pattern_uni,[status(thm)],[3526:[bind(A,$thf( sk16 ))]]) ).
thf(11977,plain,
! [A: $i] :
( ~ sk2
| ( ( sk7 @ sk1 )
!= ( sk6 @ sk1 ) )
| ~ $true
| ( ( sk1 @ sk3 @ sk4 )
!= ( sk1 @ A @ A ) ) ),
inference(paramod_ordered,[status(thm)],[11483,63]) ).
thf(11978,plain,
! [A: $i] :
( ~ sk2
| ( ( sk7 @ sk1 )
!= ( sk6 @ sk1 ) )
| ( ( sk1 @ sk3 @ sk4 )
!= ( sk1 @ A @ A ) ) ),
inference(simp,[status(thm)],[11977]) ).
thf(12065,plain,
! [A: $i] :
( ~ sk2
| ( ( sk7 @ sk1 )
!= ( sk6 @ sk1 ) )
| ( sk3 != A )
| ( sk4 != A ) ),
inference(simp,[status(thm)],[11978]) ).
thf(12090,plain,
( ~ sk2
| ( ( sk7 @ sk1 )
!= ( sk6 @ sk1 ) )
| ( sk4 != sk3 ) ),
inference(simp,[status(thm)],[12065]) ).
thf(12890,plain,
! [A: $i] :
( sk2
| ( ( sk24 @ sk1 )
!= ( sk23 @ sk1 ) )
| ~ ( sk1 @ sk15 @ A )
| ~ $true
| sk2
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ A @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[12737,960]) ).
thf(12891,plain,
! [A: $i] :
( sk2
| ( ( sk24 @ sk1 )
!= ( sk23 @ sk1 ) )
| ~ ( sk1 @ sk15 @ A )
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ A @ sk17 ) ) ),
inference(simp,[status(thm)],[12890]) ).
thf(12892,plain,
( sk2
| ( ( sk24 @ sk1 )
!= ( sk23 @ sk1 ) )
| ~ ( sk1 @ sk15 @ sk16 ) ),
inference(pattern_uni,[status(thm)],[12891:[bind(A,$thf( sk16 ))]]) ).
thf(22,plain,
! [C: $i,B: $i,A: $i] :
( sk2
| ~ ( sk28 @ A @ B )
| ~ ( sk28 @ B @ C )
| ( sk28 @ A @ C ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(55,plain,
! [C: $i,B: $i,A: $i] :
( sk2
| ~ ( sk28 @ A @ B )
| ~ ( sk28 @ B @ C )
| ( sk28 @ A @ C ) ),
inference(simp,[status(thm)],[22]) ).
thf(13201,plain,
! [C: $i,B: $i,A: $i] :
( sk2
| ~ ( sk28 @ A @ B )
| ~ ( sk28 @ B @ C )
| sk2
| ~ $true
| ( ( sk28 @ A @ C )
!= ( sk28 @ sk15 @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[55,26]) ).
thf(13202,plain,
! [C: $i,B: $i,A: $i] :
( sk2
| ~ ( sk28 @ A @ B )
| ~ ( sk28 @ B @ C )
| ( ( sk28 @ A @ C )
!= ( sk28 @ sk15 @ sk17 ) ) ),
inference(simp,[status(thm)],[13201]) ).
thf(13203,plain,
! [A: $i] :
( sk2
| ~ ( sk28 @ sk15 @ A )
| ~ ( sk28 @ A @ sk17 ) ),
inference(pattern_uni,[status(thm)],[13202:[bind(A,$thf( sk15 )),bind(B,$thf( B )),bind(C,$thf( sk17 ))]]) ).
thf(13231,plain,
! [A: $i] :
( sk2
| ~ ( sk28 @ sk15 @ A )
| ~ ( sk28 @ A @ sk17 ) ),
inference(simp,[status(thm)],[13203]) ).
thf(16012,plain,
! [A: $i] :
( sk2
| ( sk1 @ sk15 @ sk16 )
| ~ $true
| ( ( sk1 @ ( sk19 @ sk1 ) @ ( sk20 @ sk1 ) )
!= ( sk1 @ A @ A ) ) ),
inference(paramod_ordered,[status(thm)],[15190,63]) ).
thf(16013,plain,
! [A: $i] :
( sk2
| ( sk1 @ sk15 @ sk16 )
| ( ( sk1 @ ( sk19 @ sk1 ) @ ( sk20 @ sk1 ) )
!= ( sk1 @ A @ A ) ) ),
inference(simp,[status(thm)],[16012]) ).
thf(16078,plain,
! [A: $i] :
( sk2
| ( sk1 @ sk15 @ sk16 )
| ( ( sk19 @ sk1 )
!= A )
| ( ( sk20 @ sk1 )
!= A ) ),
inference(simp,[status(thm)],[16013]) ).
thf(16106,plain,
( sk2
| ( sk1 @ sk15 @ sk16 )
| ( ( sk20 @ sk1 )
!= ( sk19 @ sk1 ) ) ),
inference(simp,[status(thm)],[16078]) ).
thf(17698,plain,
! [A: $i] :
( sk2
| ( ( sk20 @ sk1 )
!= ( sk19 @ sk1 ) )
| ~ $true
| ( ( sk1 @ sk15 @ sk16 )
!= ( sk1 @ A @ A ) ) ),
inference(paramod_ordered,[status(thm)],[16106,63]) ).
thf(17699,plain,
! [A: $i] :
( sk2
| ( ( sk20 @ sk1 )
!= ( sk19 @ sk1 ) )
| ( ( sk1 @ sk15 @ sk16 )
!= ( sk1 @ A @ A ) ) ),
inference(simp,[status(thm)],[17698]) ).
thf(17780,plain,
! [A: $i] :
( sk2
| ( ( sk20 @ sk1 )
!= ( sk19 @ sk1 ) )
| ( sk15 != A )
| ( sk16 != A ) ),
inference(simp,[status(thm)],[17699]) ).
thf(17811,plain,
( sk2
| ( ( sk20 @ sk1 )
!= ( sk19 @ sk1 ) )
| ( sk16 != sk15 ) ),
inference(simp,[status(thm)],[17780]) ).
thf(19,plain,
! [A: $i > $i > $o] :
( ( A @ ( sk11 @ A ) @ ( sk12 @ A ) )
| ( sk1 @ ( sk13 @ A ) @ ( sk14 @ A ) )
| ( A @ sk4 @ sk3 )
| ~ sk2 ),
inference(cnfConj,[status(thm)],[4]) ).
thf(60,plain,
! [A: $i > $i > $o] :
( ( A @ ( sk11 @ A ) @ ( sk12 @ A ) )
| ( sk1 @ ( sk13 @ A ) @ ( sk14 @ A ) )
| ( A @ sk4 @ sk3 )
| ~ sk2 ),
inference(simp,[status(thm)],[19]) ).
thf(4478,plain,
! [C: $i,B: $i,A: $i] :
( ~ sk2
| ~ ( sk1 @ A @ B )
| ~ $true
| ~ ( sk1 @ C @ A )
| ( ( sk1
@ ( sk8
@ ^ [D: $i,E: $i] : $false )
@ ( sk9
@ ^ [D: $i,E: $i] : $false ) )
!= ( sk1 @ B @ C ) ) ),
inference(paramod_ordered,[status(thm)],[4294,928]) ).
thf(4479,plain,
! [C: $i,B: $i,A: $i] :
( ~ sk2
| ~ ( sk1 @ A @ B )
| ~ ( sk1 @ C @ A )
| ( ( sk1
@ ( sk8
@ ^ [D: $i,E: $i] : $false )
@ ( sk9
@ ^ [D: $i,E: $i] : $false ) )
!= ( sk1 @ B @ C ) ) ),
inference(simp,[status(thm)],[4478]) ).
thf(4480,plain,
! [A: $i] :
( ~ sk2
| ~ ( sk1 @ A
@ ( sk8
@ ^ [B: $i,C: $i] : $false ) )
| ~ ( sk1
@ ( sk9
@ ^ [B: $i,C: $i] : $false )
@ A ) ),
inference(pattern_uni,[status(thm)],[4479:[bind(A,$thf( A )),bind(B,$thf( sk8 @ ^ [D: $i] : ^ [E: $i] : $false )),bind(C,$thf( sk9 @ ^ [D: $i] : ^ [E: $i] : $false ))]]) ).
thf(8244,plain,
! [A: $i > $i > $o] :
( ~ ( A
@ ( sk5
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
@ ( sk6
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) ) )
| ~ ( A @ sk3 @ sk4 )
| ~ sk2
| ( sk1
@ ( sk13
@ ^ [B: $i,C: $i] : ~ $true )
@ ( sk14
@ ^ [B: $i,C: $i] : ~ sk2 ) )
| ~ sk2
| ( ( A
@ ( sk8
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
@ ( sk9
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) ) )
!= sk2 ) ),
inference(paramod_ordered,[status(thm)],[522,7494]) ).
thf(8245,plain,
! [A: $i > $i > $o] :
( ~ ( A
@ ( sk5
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
@ ( sk6
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) ) )
| ~ ( A @ sk3 @ sk4 )
| ~ sk2
| ( sk1
@ ( sk13
@ ^ [B: $i,C: $i] : $false )
@ ( sk14
@ ^ [B: $i,C: $i] : ~ sk2 ) )
| ( ( A
@ ( sk8
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
@ ( sk9
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) ) )
!= sk2 ) ),
inference(simp,[status(thm)],[8244]) ).
thf(8408,plain,
( ~ sk2
| ~ sk2
| ~ sk2
| ( sk1
@ ( sk13
@ ^ [A: $i,B: $i] : $false )
@ ( sk14
@ ^ [A: $i,B: $i] : ~ sk2 ) ) ),
inference(pre_uni,[status(thm)],[8245:[bind(A,$thf( ^ [B: $i] : ^ [C: $i] : sk2 ))]]) ).
thf(8441,plain,
( ~ sk2
| ( sk1
@ ( sk13
@ ^ [A: $i,B: $i] : $false )
@ ( sk14
@ ^ [A: $i,B: $i] : ~ sk2 ) ) ),
inference(simp,[status(thm)],[8408]) ).
thf(9066,plain,
! [A: $i] :
( ~ sk2
| ~ $true
| ( ( sk1
@ ( sk13
@ ^ [B: $i,C: $i] : $false )
@ ( sk14
@ ^ [B: $i,C: $i] : ~ sk2 ) )
!= ( sk1 @ A @ A ) ) ),
inference(paramod_ordered,[status(thm)],[8441,63]) ).
thf(9067,plain,
! [A: $i] :
( ~ sk2
| ( ( sk1
@ ( sk13
@ ^ [B: $i,C: $i] : $false )
@ ( sk14
@ ^ [B: $i,C: $i] : ~ sk2 ) )
!= ( sk1 @ A @ A ) ) ),
inference(simp,[status(thm)],[9066]) ).
thf(9136,plain,
! [A: $i] :
( ~ sk2
| ( ( sk13
@ ^ [B: $i,C: $i] : $false )
!= A )
| ( ( sk14
@ ^ [B: $i,C: $i] : ~ sk2 )
!= A ) ),
inference(simp,[status(thm)],[9067]) ).
thf(9175,plain,
( ~ sk2
| ( ( sk14
@ ^ [A: $i,B: $i] : ~ sk2 )
!= ( sk13
@ ^ [A: $i,B: $i] : $false ) ) ),
inference(simp,[status(thm)],[9136]) ).
thf(4824,plain,
! [A: $i > $i > $o] :
( ~ ( A
@ ( sk5
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
@ ( sk6
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) ) )
| ~ ( A @ sk3 @ sk4 )
| ~ sk2
| ( sk1
@ ( sk8
@ ^ [B: $i,C: $i] : ~ $true )
@ ( sk9
@ ^ [B: $i,C: $i] : ~ sk2 ) )
| ~ sk2
| ( ( A
@ ( sk8
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
@ ( sk9
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) ) )
!= sk2 ) ),
inference(paramod_ordered,[status(thm)],[522,4272]) ).
thf(4825,plain,
! [A: $i > $i > $o] :
( ~ ( A
@ ( sk5
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
@ ( sk6
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) ) )
| ~ ( A @ sk3 @ sk4 )
| ~ sk2
| ( sk1
@ ( sk8
@ ^ [B: $i,C: $i] : $false )
@ ( sk9
@ ^ [B: $i,C: $i] : ~ sk2 ) )
| ( ( A
@ ( sk8
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
@ ( sk9
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) ) )
!= sk2 ) ),
inference(simp,[status(thm)],[4824]) ).
thf(4942,plain,
( ~ sk2
| ~ sk2
| ~ sk2
| ( sk1
@ ( sk8
@ ^ [A: $i,B: $i] : $false )
@ ( sk9
@ ^ [A: $i,B: $i] : ~ sk2 ) ) ),
inference(pre_uni,[status(thm)],[4825:[bind(A,$thf( ^ [B: $i] : ^ [C: $i] : sk2 ))]]) ).
thf(4971,plain,
( ~ sk2
| ( sk1
@ ( sk8
@ ^ [A: $i,B: $i] : $false )
@ ( sk9
@ ^ [A: $i,B: $i] : ~ sk2 ) ) ),
inference(simp,[status(thm)],[4942]) ).
thf(5102,plain,
! [B: $i,A: $i] :
( ~ sk2
| ~ $true
| ~ ( sk1 @ B @ A )
| ( ( sk1
@ ( sk8
@ ^ [C: $i,D: $i] : $false )
@ ( sk9
@ ^ [C: $i,D: $i] : ~ sk2 ) )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[4971,31]) ).
thf(5103,plain,
! [B: $i,A: $i] :
( ~ sk2
| ~ ( sk1 @ B @ A )
| ( ( sk1
@ ( sk8
@ ^ [C: $i,D: $i] : $false )
@ ( sk9
@ ^ [C: $i,D: $i] : ~ sk2 ) )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[5102]) ).
thf(5104,plain,
( ~ sk2
| ~ ( sk1
@ ( sk9
@ ^ [A: $i,B: $i] : ~ sk2 )
@ ( sk8
@ ^ [A: $i,B: $i] : $false ) ) ),
inference(pattern_uni,[status(thm)],[5103:[bind(A,$thf( sk8 @ ^ [C: $i] : ^ [D: $i] : $false )),bind(B,$thf( sk9 @ ^ [C: $i] : ^ [D: $i] : ~ ( sk2 ) ))]]) ).
thf(7701,plain,
( ~ sk2
| ~ sk2
| ~ $true
| ( ( sk1
@ ( sk13
@ ^ [A: $i,B: $i] : $false )
@ ( sk14
@ ^ [A: $i,B: $i] : $false ) )
!= ( sk1
@ ( sk9
@ ^ [A: $i,B: $i] : ~ sk2 )
@ ( sk8
@ ^ [A: $i,B: $i] : $false ) ) ) ),
inference(paramod_ordered,[status(thm)],[7463,5104]) ).
thf(7702,plain,
( ~ sk2
| ( ( sk1
@ ( sk13
@ ^ [A: $i,B: $i] : $false )
@ ( sk14
@ ^ [A: $i,B: $i] : $false ) )
!= ( sk1
@ ( sk9
@ ^ [A: $i,B: $i] : ~ sk2 )
@ ( sk8
@ ^ [A: $i,B: $i] : $false ) ) ) ),
inference(simp,[status(thm)],[7701]) ).
thf(7735,plain,
( ~ sk2
| ( ( sk13
@ ^ [A: $i,B: $i] : $false )
!= ( sk9
@ ^ [A: $i,B: $i] : ~ sk2 ) )
| ( ( sk14
@ ^ [A: $i,B: $i] : $false )
!= ( sk8
@ ^ [A: $i,B: $i] : $false ) ) ),
inference(simp,[status(thm)],[7702]) ).
thf(22099,plain,
! [A: $i] :
( sk2
| ~ ( sk28 @ sk15 @ A )
| ( ( sk28 @ A @ sk17 )
!= ( sk28 @ sk15 @ A ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[13231]) ).
thf(22108,plain,
! [A: $i] :
( sk2
| ~ ( sk28 @ sk15 @ A )
| ( A != sk15 )
| ( sk17 != A ) ),
inference(simp,[status(thm)],[22099]) ).
thf(22136,plain,
( sk2
| ~ ( sk28 @ sk15 @ sk15 )
| ( sk17 != sk15 ) ),
inference(simp,[status(thm)],[22108]) ).
thf(15340,plain,
! [A: $i] :
( ( sk1 @ sk4 @ sk3 )
| ~ sk2
| ~ $true
| ( ( sk1 @ ( sk10 @ sk1 ) @ ( sk11 @ sk1 ) )
!= ( sk1 @ A @ A ) ) ),
inference(paramod_ordered,[status(thm)],[14101,63]) ).
thf(15341,plain,
! [A: $i] :
( ( sk1 @ sk4 @ sk3 )
| ~ sk2
| ( ( sk1 @ ( sk10 @ sk1 ) @ ( sk11 @ sk1 ) )
!= ( sk1 @ A @ A ) ) ),
inference(simp,[status(thm)],[15340]) ).
thf(15432,plain,
! [A: $i] :
( ( sk1 @ sk4 @ sk3 )
| ~ sk2
| ( ( sk10 @ sk1 )
!= A )
| ( ( sk11 @ sk1 )
!= A ) ),
inference(simp,[status(thm)],[15341]) ).
thf(15439,plain,
( ( sk1 @ sk4 @ sk3 )
| ~ sk2
| ( ( sk11 @ sk1 )
!= ( sk10 @ sk1 ) ) ),
inference(simp,[status(thm)],[15432]) ).
thf(15489,plain,
( ~ sk2
| ( ( sk12 @ sk1 )
!= ( sk11 @ sk1 ) )
| ~ sk2
| ( ( sk6 @ sk1 )
!= ( sk5 @ sk1 ) )
| ~ $true
| ( ( sk1 @ sk4 @ sk3 )
!= ( sk1 @ sk4 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[15437,11609]) ).
thf(15490,plain,
( ~ sk2
| ( ( sk12 @ sk1 )
!= ( sk11 @ sk1 ) )
| ( ( sk6 @ sk1 )
!= ( sk5 @ sk1 ) )
| ( ( sk1 @ sk4 @ sk3 )
!= ( sk1 @ sk4 @ sk3 ) ) ),
inference(simp,[status(thm)],[15489]) ).
thf(15491,plain,
( ~ sk2
| ( ( sk12 @ sk1 )
!= ( sk11 @ sk1 ) )
| ( ( sk6 @ sk1 )
!= ( sk5 @ sk1 ) ) ),
inference(pattern_uni,[status(thm)],[15490:[]]) ).
thf(1624,plain,
! [A: $i] :
( sk2
| ~ $true
| ~ ( sk1 @ A @ sk17 )
| sk2
| ( ( sk1
@ ( sk21
@ ^ [B: $i,C: $i] : $false )
@ ( sk22
@ ^ [B: $i,C: $i] : $false ) )
!= ( sk1 @ sk15 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[1402,960]) ).
thf(1625,plain,
! [A: $i] :
( sk2
| ~ ( sk1 @ A @ sk17 )
| ( ( sk1
@ ( sk21
@ ^ [B: $i,C: $i] : $false )
@ ( sk22
@ ^ [B: $i,C: $i] : $false ) )
!= ( sk1 @ sk15 @ A ) ) ),
inference(simp,[status(thm)],[1624]) ).
thf(1647,plain,
! [A: $i] :
( sk2
| ~ ( sk1 @ A @ sk17 )
| ( ( sk21
@ ^ [B: $i,C: $i] : $false )
!= sk15 )
| ( ( sk22
@ ^ [B: $i,C: $i] : $false )
!= A ) ),
inference(simp,[status(thm)],[1625]) ).
thf(1656,plain,
( sk2
| ~ ( sk1
@ ( sk22
@ ^ [A: $i,B: $i] : $false )
@ sk17 )
| ( ( sk21
@ ^ [A: $i,B: $i] : $false )
!= sk15 ) ),
inference(simp,[status(thm)],[1647]) ).
thf(6053,plain,
! [A: $i] :
( ~ sk2
| ~ $true
| ( ( sk1
@ ( sk8
@ ^ [B: $i,C: $i] : ~ sk2 )
@ ( sk9
@ ^ [B: $i,C: $i] : $false ) )
!= ( sk1 @ A @ A ) ) ),
inference(paramod_ordered,[status(thm)],[4975,63]) ).
thf(6054,plain,
! [A: $i] :
( ~ sk2
| ( ( sk1
@ ( sk8
@ ^ [B: $i,C: $i] : ~ sk2 )
@ ( sk9
@ ^ [B: $i,C: $i] : $false ) )
!= ( sk1 @ A @ A ) ) ),
inference(simp,[status(thm)],[6053]) ).
thf(6118,plain,
! [A: $i] :
( ~ sk2
| ( ( sk8
@ ^ [B: $i,C: $i] : ~ sk2 )
!= A )
| ( ( sk9
@ ^ [B: $i,C: $i] : $false )
!= A ) ),
inference(simp,[status(thm)],[6054]) ).
thf(6143,plain,
( ~ sk2
| ( ( sk9
@ ^ [A: $i,B: $i] : $false )
!= ( sk8
@ ^ [A: $i,B: $i] : ~ sk2 ) ) ),
inference(simp,[status(thm)],[6118]) ).
thf(5098,plain,
! [A: $i] :
( ~ sk2
| ~ $true
| ( ( sk1
@ ( sk8
@ ^ [B: $i,C: $i] : $false )
@ ( sk9
@ ^ [B: $i,C: $i] : ~ sk2 ) )
!= ( sk1 @ A @ A ) ) ),
inference(paramod_ordered,[status(thm)],[4971,63]) ).
thf(5099,plain,
! [A: $i] :
( ~ sk2
| ( ( sk1
@ ( sk8
@ ^ [B: $i,C: $i] : $false )
@ ( sk9
@ ^ [B: $i,C: $i] : ~ sk2 ) )
!= ( sk1 @ A @ A ) ) ),
inference(simp,[status(thm)],[5098]) ).
thf(5165,plain,
! [A: $i] :
( ~ sk2
| ( ( sk8
@ ^ [B: $i,C: $i] : $false )
!= A )
| ( ( sk9
@ ^ [B: $i,C: $i] : ~ sk2 )
!= A ) ),
inference(simp,[status(thm)],[5099]) ).
thf(5189,plain,
( ~ sk2
| ( ( sk9
@ ^ [A: $i,B: $i] : ~ sk2 )
!= ( sk8
@ ^ [A: $i,B: $i] : $false ) ) ),
inference(simp,[status(thm)],[5165]) ).
thf(233,plain,
! [B: $i,A: $i] :
( sk2
| ~ $true
| ~ ( sk1 @ B @ A )
| ( ( sk1
@ ( sk26
@ ^ [C: $i,D: $i] : sk2 )
@ ( sk27
@ ^ [C: $i,D: $i] : sk2 ) )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[199,31]) ).
thf(234,plain,
! [B: $i,A: $i] :
( sk2
| ~ ( sk1 @ B @ A )
| ( ( sk1
@ ( sk26
@ ^ [C: $i,D: $i] : sk2 )
@ ( sk27
@ ^ [C: $i,D: $i] : sk2 ) )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[233]) ).
thf(235,plain,
( sk2
| ~ ( sk1
@ ( sk27
@ ^ [A: $i,B: $i] : sk2 )
@ ( sk26
@ ^ [A: $i,B: $i] : sk2 ) ) ),
inference(pattern_uni,[status(thm)],[234:[bind(A,$thf( sk26 @ ^ [C: $i] : ^ [D: $i] : sk2 )),bind(B,$thf( sk27 @ ^ [C: $i] : ^ [D: $i] : sk2 ))]]) ).
thf(1466,plain,
( sk2
| sk2
| ~ $true
| ( ( sk1
@ ( sk27
@ ^ [A: $i,B: $i] : sk2 )
@ ( sk26
@ ^ [A: $i,B: $i] : sk2 ) )
!= ( sk1
@ ( sk21
@ ^ [A: $i,B: $i] : sk2 )
@ ( sk22
@ ^ [A: $i,B: $i] : sk2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[1401,235]) ).
thf(1467,plain,
( sk2
| ( ( sk1
@ ( sk27
@ ^ [A: $i,B: $i] : sk2 )
@ ( sk26
@ ^ [A: $i,B: $i] : sk2 ) )
!= ( sk1
@ ( sk21
@ ^ [A: $i,B: $i] : sk2 )
@ ( sk22
@ ^ [A: $i,B: $i] : sk2 ) ) ) ),
inference(simp,[status(thm)],[1466]) ).
thf(1534,plain,
( sk2
| ( ( sk27
@ ^ [A: $i,B: $i] : sk2 )
!= ( sk21
@ ^ [A: $i,B: $i] : sk2 ) )
| ( ( sk26
@ ^ [A: $i,B: $i] : sk2 )
!= ( sk22
@ ^ [A: $i,B: $i] : sk2 ) ) ),
inference(simp,[status(thm)],[1467]) ).
thf(8310,plain,
! [A: $i] :
( ~ sk2
| ~ $true
| ( ( sk1
@ ( sk13
@ ^ [B: $i,C: $i] : ~ sk2 )
@ ( sk14
@ ^ [B: $i,C: $i] : ~ sk2 ) )
!= ( sk1 @ A @ A ) ) ),
inference(paramod_ordered,[status(thm)],[7494,63]) ).
thf(8311,plain,
! [A: $i] :
( ~ sk2
| ( ( sk1
@ ( sk13
@ ^ [B: $i,C: $i] : ~ sk2 )
@ ( sk14
@ ^ [B: $i,C: $i] : ~ sk2 ) )
!= ( sk1 @ A @ A ) ) ),
inference(simp,[status(thm)],[8310]) ).
thf(8391,plain,
! [A: $i] :
( ~ sk2
| ( ( sk13
@ ^ [B: $i,C: $i] : ~ sk2 )
!= A )
| ( ( sk14
@ ^ [B: $i,C: $i] : ~ sk2 )
!= A ) ),
inference(simp,[status(thm)],[8311]) ).
thf(8429,plain,
( ~ sk2
| ( ( sk14
@ ^ [A: $i,B: $i] : ~ sk2 )
!= ( sk13
@ ^ [A: $i,B: $i] : ~ sk2 ) ) ),
inference(simp,[status(thm)],[8391]) ).
thf(7,plain,
! [A: $i > $i > $o] :
( sk2
| ~ ( A @ ( sk18 @ A ) @ ( sk20 @ A ) )
| ( sk1 @ ( sk21 @ A ) @ ( sk22 @ A ) )
| ( A @ sk15 @ sk16 ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(41,plain,
! [A: $i > $i > $o] :
( sk2
| ~ ( A @ ( sk18 @ A ) @ ( sk20 @ A ) )
| ( sk1 @ ( sk21 @ A ) @ ( sk22 @ A ) )
| ( A @ sk15 @ sk16 ) ),
inference(simp,[status(thm)],[7]) ).
thf(9964,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( sk2
| ~ ( A @ ( sk18 @ A ) @ ( sk20 @ A ) )
| ( A @ sk15 @ sk16 )
| sk2
| ~ ( B @ ( sk18 @ B ) @ ( sk20 @ B ) )
| ~ $true
| ( B @ sk15 @ sk16 )
| ( ( sk1 @ ( sk21 @ A ) @ ( sk22 @ A ) )
!= ( B @ ( sk21 @ B ) @ ( sk22 @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[41,52]) ).
thf(9965,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( sk2
| ~ ( A @ ( sk18 @ A ) @ ( sk20 @ A ) )
| ( A @ sk15 @ sk16 )
| ~ ( B @ ( sk18 @ B ) @ ( sk20 @ B ) )
| ( B @ sk15 @ sk16 )
| ( ( sk1 @ ( sk21 @ A ) @ ( sk22 @ A ) )
!= ( B @ ( sk21 @ B ) @ ( sk22 @ B ) ) ) ),
inference(simp,[status(thm)],[9964]) ).
thf(10059,plain,
( sk2
| ~ ( sk1 @ ( sk18 @ sk1 ) @ ( sk20 @ sk1 ) )
| ( sk1 @ sk15 @ sk16 )
| ~ ( sk1 @ ( sk18 @ sk1 ) @ ( sk20 @ sk1 ) )
| ( sk1 @ sk15 @ sk16 ) ),
inference(pre_uni,[status(thm)],[9965:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 ))]]) ).
thf(10127,plain,
( sk2
| ~ ( sk1 @ ( sk18 @ sk1 ) @ ( sk20 @ sk1 ) )
| ( sk1 @ sk15 @ sk16 ) ),
inference(simp,[status(thm)],[10059]) ).
thf(15984,plain,
( sk2
| ( sk1 @ sk15 @ sk16 )
| sk2
| ~ $true
| ( sk1 @ sk15 @ sk16 )
| ( ( sk1 @ ( sk19 @ sk1 ) @ ( sk20 @ sk1 ) )
!= ( sk1 @ ( sk18 @ sk1 ) @ ( sk20 @ sk1 ) ) ) ),
inference(paramod_ordered,[status(thm)],[15190,10127]) ).
thf(15985,plain,
( sk2
| ( sk1 @ sk15 @ sk16 )
| ( ( sk1 @ ( sk19 @ sk1 ) @ ( sk20 @ sk1 ) )
!= ( sk1 @ ( sk18 @ sk1 ) @ ( sk20 @ sk1 ) ) ) ),
inference(simp,[status(thm)],[15984]) ).
thf(16101,plain,
( sk2
| ( sk1 @ sk15 @ sk16 )
| ( ( sk19 @ sk1 )
!= ( sk18 @ sk1 ) )
| ( ( sk20 @ sk1 )
!= ( sk20 @ sk1 ) ) ),
inference(simp,[status(thm)],[15985]) ).
thf(16112,plain,
( sk2
| ( sk1 @ sk15 @ sk16 )
| ( ( sk19 @ sk1 )
!= ( sk18 @ sk1 ) ) ),
inference(simp,[status(thm)],[16101]) ).
thf(4435,plain,
! [B: $i,A: $i] :
( ~ sk2
| ~ $true
| ~ ( sk1 @ B @ A )
| ( ( sk1
@ ( sk8
@ ^ [C: $i,D: $i] : $false )
@ ( sk9
@ ^ [C: $i,D: $i] : $false ) )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[4294,31]) ).
thf(4436,plain,
! [B: $i,A: $i] :
( ~ sk2
| ~ ( sk1 @ B @ A )
| ( ( sk1
@ ( sk8
@ ^ [C: $i,D: $i] : $false )
@ ( sk9
@ ^ [C: $i,D: $i] : $false ) )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[4435]) ).
thf(4437,plain,
( ~ sk2
| ~ ( sk1
@ ( sk9
@ ^ [A: $i,B: $i] : $false )
@ ( sk8
@ ^ [A: $i,B: $i] : $false ) ) ),
inference(pattern_uni,[status(thm)],[4436:[bind(A,$thf( sk8 @ ^ [C: $i] : ^ [D: $i] : $false )),bind(B,$thf( sk9 @ ^ [C: $i] : ^ [D: $i] : $false ))]]) ).
thf(7671,plain,
( ~ sk2
| ~ sk2
| ~ $true
| ( ( sk1
@ ( sk13
@ ^ [A: $i,B: $i] : $false )
@ ( sk14
@ ^ [A: $i,B: $i] : $false ) )
!= ( sk1
@ ( sk9
@ ^ [A: $i,B: $i] : $false )
@ ( sk8
@ ^ [A: $i,B: $i] : $false ) ) ) ),
inference(paramod_ordered,[status(thm)],[7463,4437]) ).
thf(7672,plain,
( ~ sk2
| ( ( sk1
@ ( sk13
@ ^ [A: $i,B: $i] : $false )
@ ( sk14
@ ^ [A: $i,B: $i] : $false ) )
!= ( sk1
@ ( sk9
@ ^ [A: $i,B: $i] : $false )
@ ( sk8
@ ^ [A: $i,B: $i] : $false ) ) ) ),
inference(simp,[status(thm)],[7671]) ).
thf(7749,plain,
( ~ sk2
| ( ( sk13
@ ^ [A: $i,B: $i] : $false )
!= ( sk9
@ ^ [A: $i,B: $i] : $false ) )
| ( ( sk14
@ ^ [A: $i,B: $i] : $false )
!= ( sk8
@ ^ [A: $i,B: $i] : $false ) ) ),
inference(simp,[status(thm)],[7672]) ).
thf(1105,plain,
! [A: $i] :
( sk2
| ~ ( sk1 @ sk15 @ A )
| ~ $true
| sk2
| ( ( sk1
@ ( sk26
@ ^ [B: $i,C: $i] : $false )
@ ( sk27
@ ^ [B: $i,C: $i] : $false ) )
!= ( sk1 @ A @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[202,960]) ).
thf(1106,plain,
! [A: $i] :
( sk2
| ~ ( sk1 @ sk15 @ A )
| ( ( sk1
@ ( sk26
@ ^ [B: $i,C: $i] : $false )
@ ( sk27
@ ^ [B: $i,C: $i] : $false ) )
!= ( sk1 @ A @ sk17 ) ) ),
inference(simp,[status(thm)],[1105]) ).
thf(1121,plain,
! [A: $i] :
( sk2
| ~ ( sk1 @ sk15 @ A )
| ( ( sk26
@ ^ [B: $i,C: $i] : $false )
!= A )
| ( ( sk27
@ ^ [B: $i,C: $i] : $false )
!= sk17 ) ),
inference(simp,[status(thm)],[1106]) ).
thf(1131,plain,
( sk2
| ~ ( sk1 @ sk15
@ ( sk26
@ ^ [A: $i,B: $i] : $false ) )
| ( ( sk27
@ ^ [A: $i,B: $i] : $false )
!= sk17 ) ),
inference(simp,[status(thm)],[1121]) ).
thf(15600,plain,
! [B: $i,A: $i] :
( ~ sk2
| ( ( sk12 @ sk1 )
!= ( sk11 @ sk1 ) )
| ~ $true
| ~ ( sk1 @ B @ A )
| ( ( sk1 @ sk4 @ sk3 )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[15437,31]) ).
thf(15601,plain,
! [B: $i,A: $i] :
( ~ sk2
| ( ( sk12 @ sk1 )
!= ( sk11 @ sk1 ) )
| ~ ( sk1 @ B @ A )
| ( ( sk1 @ sk4 @ sk3 )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[15600]) ).
thf(15602,plain,
( ~ sk2
| ( ( sk12 @ sk1 )
!= ( sk11 @ sk1 ) )
| ~ ( sk1 @ sk3 @ sk4 ) ),
inference(pattern_uni,[status(thm)],[15601:[bind(A,$thf( sk4 )),bind(B,$thf( sk3 ))]]) ).
thf(341,plain,
! [B: $i,A: $i] :
( sk2
| sk2
| ~ $true
| ( sk28 @ A @ B )
| ( ( sk1
@ ( sk26
@ ^ [C: $i,D: $i] : $false )
@ ( sk27
@ ^ [C: $i,D: $i] : $false ) )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[202,40]) ).
thf(342,plain,
! [B: $i,A: $i] :
( sk2
| ( sk28 @ A @ B )
| ( ( sk1
@ ( sk26
@ ^ [C: $i,D: $i] : $false )
@ ( sk27
@ ^ [C: $i,D: $i] : $false ) )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[341]) ).
thf(343,plain,
( sk2
| ( sk28
@ ( sk26
@ ^ [A: $i,B: $i] : $false )
@ ( sk27
@ ^ [A: $i,B: $i] : $false ) ) ),
inference(pattern_uni,[status(thm)],[342:[bind(A,$thf( sk26 @ ^ [C: $i] : ^ [D: $i] : $false )),bind(B,$thf( sk27 @ ^ [C: $i] : ^ [D: $i] : $false ))]]) ).
thf(17929,plain,
( sk2
| ( ( sk19 @ sk1 )
!= ( sk18 @ sk1 ) )
| sk2
| ~ $true
| ( ( sk1 @ sk15 @ sk17 )
!= ( sk1 @ sk15 @ sk16 ) ) ),
inference(paramod_ordered,[status(thm)],[16112,66]) ).
thf(17930,plain,
( sk2
| ( ( sk19 @ sk1 )
!= ( sk18 @ sk1 ) )
| ( ( sk1 @ sk15 @ sk17 )
!= ( sk1 @ sk15 @ sk16 ) ) ),
inference(simp,[status(thm)],[17929]) ).
thf(18034,plain,
( sk2
| ( ( sk19 @ sk1 )
!= ( sk18 @ sk1 ) )
| ( sk15 != sk15 )
| ( sk17 != sk16 ) ),
inference(simp,[status(thm)],[17930]) ).
thf(18059,plain,
( sk2
| ( ( sk19 @ sk1 )
!= ( sk18 @ sk1 ) )
| ( sk17 != sk16 ) ),
inference(simp,[status(thm)],[18034]) ).
thf(16257,plain,
! [A: $i] :
( ~ sk2
| ( ( sk11 @ sk1 )
!= ( sk10 @ sk1 ) )
| ~ $true
| ( ( sk1 @ sk4 @ sk3 )
!= ( sk1 @ A @ A ) ) ),
inference(paramod_ordered,[status(thm)],[15439,63]) ).
thf(16258,plain,
! [A: $i] :
( ~ sk2
| ( ( sk11 @ sk1 )
!= ( sk10 @ sk1 ) )
| ( ( sk1 @ sk4 @ sk3 )
!= ( sk1 @ A @ A ) ) ),
inference(simp,[status(thm)],[16257]) ).
thf(16355,plain,
! [A: $i] :
( ~ sk2
| ( ( sk11 @ sk1 )
!= ( sk10 @ sk1 ) )
| ( sk4 != A )
| ( sk3 != A ) ),
inference(simp,[status(thm)],[16258]) ).
thf(16390,plain,
( ~ sk2
| ( ( sk11 @ sk1 )
!= ( sk10 @ sk1 ) )
| ( sk4 != sk3 ) ),
inference(simp,[status(thm)],[16355]) ).
thf(15,plain,
! [A: $i > $i > $o] :
( ( A @ ( sk11 @ A ) @ ( sk12 @ A ) )
| ~ ( A @ ( sk13 @ A ) @ ( sk14 @ A ) )
| ( A @ sk4 @ sk3 )
| ~ sk2 ),
inference(cnfConj,[status(thm)],[4]) ).
thf(45,plain,
! [A: $i > $i > $o] :
( ( A @ ( sk11 @ A ) @ ( sk12 @ A ) )
| ~ ( A @ ( sk13 @ A ) @ ( sk14 @ A ) )
| ( A @ sk4 @ sk3 )
| ~ sk2 ),
inference(simp,[status(thm)],[15]) ).
thf(19015,plain,
! [B: $i,A: $i] :
( sk2
| ( sk1 @ sk16 @ sk17 )
| sk2
| ~ $true
| ( sk28 @ A @ B )
| ( ( sk1 @ ( sk23 @ sk1 ) @ ( sk24 @ sk1 ) )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[17482,40]) ).
thf(19016,plain,
! [B: $i,A: $i] :
( sk2
| ( sk1 @ sk16 @ sk17 )
| ( sk28 @ A @ B )
| ( ( sk1 @ ( sk23 @ sk1 ) @ ( sk24 @ sk1 ) )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[19015]) ).
thf(19017,plain,
( sk2
| ( sk1 @ sk16 @ sk17 )
| ( sk28 @ ( sk23 @ sk1 ) @ ( sk24 @ sk1 ) ) ),
inference(pattern_uni,[status(thm)],[19016:[bind(A,$thf( sk23 @ sk1 )),bind(B,$thf( sk24 @ sk1 ))]]) ).
thf(695,plain,
! [A: $i > $i > $o] :
( ~ ( A
@ ( sk5
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
@ ( sk6
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) ) )
| ~ ( A @ sk3 @ sk4 )
| ~ sk2
| ( ( A
@ ( sk8
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
@ ( sk9
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) ) )
!= ( ~ ( A @ sk3 @ sk4 ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[522]) ).
thf(733,plain,
! [A: $i > $i > $o] :
( ~ ( A
@ ( sk5
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
@ ( sk6
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) ) )
| ~ ( A @ sk3 @ sk4 )
| ~ sk2
| ( ( A
@ ( sk8
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
@ ( sk9
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) ) )
!= ( ~ ( A @ sk3 @ sk4 ) ) ) ),
inference(simp,[status(thm)],[695]) ).
thf(17746,plain,
! [A: $i] :
( sk2
| ( ( sk20 @ sk1 )
!= ( sk19 @ sk1 ) )
| ~ $true
| ~ ( sk1 @ A @ sk17 )
| sk2
| ( ( sk1 @ sk15 @ sk16 )
!= ( sk1 @ sk15 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[16106,960]) ).
thf(17747,plain,
! [A: $i] :
( sk2
| ( ( sk20 @ sk1 )
!= ( sk19 @ sk1 ) )
| ~ ( sk1 @ A @ sk17 )
| ( ( sk1 @ sk15 @ sk16 )
!= ( sk1 @ sk15 @ A ) ) ),
inference(simp,[status(thm)],[17746]) ).
thf(17748,plain,
( sk2
| ( ( sk20 @ sk1 )
!= ( sk19 @ sk1 ) )
| ~ ( sk1 @ sk16 @ sk17 ) ),
inference(pattern_uni,[status(thm)],[17747:[bind(A,$thf( sk16 ))]]) ).
thf(1626,plain,
! [A: $i] :
( sk2
| ~ ( sk1 @ sk15 @ A )
| ~ $true
| sk2
| ( ( sk1
@ ( sk21
@ ^ [B: $i,C: $i] : $false )
@ ( sk22
@ ^ [B: $i,C: $i] : $false ) )
!= ( sk1 @ A @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[1402,960]) ).
thf(1627,plain,
! [A: $i] :
( sk2
| ~ ( sk1 @ sk15 @ A )
| ( ( sk1
@ ( sk21
@ ^ [B: $i,C: $i] : $false )
@ ( sk22
@ ^ [B: $i,C: $i] : $false ) )
!= ( sk1 @ A @ sk17 ) ) ),
inference(simp,[status(thm)],[1626]) ).
thf(1641,plain,
! [A: $i] :
( sk2
| ~ ( sk1 @ sk15 @ A )
| ( ( sk21
@ ^ [B: $i,C: $i] : $false )
!= A )
| ( ( sk22
@ ^ [B: $i,C: $i] : $false )
!= sk17 ) ),
inference(simp,[status(thm)],[1627]) ).
thf(1652,plain,
( sk2
| ~ ( sk1 @ sk15
@ ( sk21
@ ^ [A: $i,B: $i] : $false ) )
| ( ( sk22
@ ^ [A: $i,B: $i] : $false )
!= sk17 ) ),
inference(simp,[status(thm)],[1641]) ).
thf(8579,plain,
! [B: $i,A: $i] :
( ~ sk2
| ~ $true
| ~ ( sk1 @ B @ A )
| ( ( sk1
@ ( sk13
@ ^ [C: $i,D: $i] : ~ sk2 )
@ ( sk14
@ ^ [C: $i,D: $i] : $false ) )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[8426,31]) ).
thf(8580,plain,
! [B: $i,A: $i] :
( ~ sk2
| ~ ( sk1 @ B @ A )
| ( ( sk1
@ ( sk13
@ ^ [C: $i,D: $i] : ~ sk2 )
@ ( sk14
@ ^ [C: $i,D: $i] : $false ) )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[8579]) ).
thf(8581,plain,
( ~ sk2
| ~ ( sk1
@ ( sk14
@ ^ [A: $i,B: $i] : $false )
@ ( sk13
@ ^ [A: $i,B: $i] : ~ sk2 ) ) ),
inference(pattern_uni,[status(thm)],[8580:[bind(A,$thf( sk13 @ ^ [C: $i] : ^ [D: $i] : ~ ( sk2 ) )),bind(B,$thf( sk14 @ ^ [C: $i] : ^ [D: $i] : $false ))]]) ).
thf(12875,plain,
! [B: $i,A: $i] :
( sk2
| ( ( sk24 @ sk1 )
!= ( sk23 @ sk1 ) )
| sk2
| ~ $true
| ( sk28 @ A @ B )
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[12737,40]) ).
thf(12876,plain,
! [B: $i,A: $i] :
( sk2
| ( ( sk24 @ sk1 )
!= ( sk23 @ sk1 ) )
| ( sk28 @ A @ B )
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[12875]) ).
thf(12877,plain,
( sk2
| ( ( sk24 @ sk1 )
!= ( sk23 @ sk1 ) )
| ( sk28 @ sk16 @ sk17 ) ),
inference(pattern_uni,[status(thm)],[12876:[bind(A,$thf( sk16 )),bind(B,$thf( sk17 ))]]) ).
thf(15592,plain,
! [A: $i] :
( ~ sk2
| ( ( sk12 @ sk1 )
!= ( sk11 @ sk1 ) )
| ~ $true
| ( ( sk1 @ sk4 @ sk3 )
!= ( sk1 @ A @ A ) ) ),
inference(paramod_ordered,[status(thm)],[15437,63]) ).
thf(15593,plain,
! [A: $i] :
( ~ sk2
| ( ( sk12 @ sk1 )
!= ( sk11 @ sk1 ) )
| ( ( sk1 @ sk4 @ sk3 )
!= ( sk1 @ A @ A ) ) ),
inference(simp,[status(thm)],[15592]) ).
thf(15664,plain,
! [A: $i] :
( ~ sk2
| ( ( sk12 @ sk1 )
!= ( sk11 @ sk1 ) )
| ( sk4 != A )
| ( sk3 != A ) ),
inference(simp,[status(thm)],[15593]) ).
thf(15718,plain,
( ~ sk2
| ( ( sk12 @ sk1 )
!= ( sk11 @ sk1 ) )
| ( sk4 != sk3 ) ),
inference(simp,[status(thm)],[15664]) ).
thf(1571,plain,
( sk2
| sk2
| ~ $true
| ( ( sk1
@ ( sk21
@ ^ [A: $i,B: $i] : $false )
@ ( sk22
@ ^ [A: $i,B: $i] : $false ) )
!= ( sk1 @ sk15 @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[1402,66]) ).
thf(1572,plain,
( sk2
| ( ( sk1
@ ( sk21
@ ^ [A: $i,B: $i] : $false )
@ ( sk22
@ ^ [A: $i,B: $i] : $false ) )
!= ( sk1 @ sk15 @ sk17 ) ) ),
inference(simp,[status(thm)],[1571]) ).
thf(1638,plain,
( sk2
| ( ( sk21
@ ^ [A: $i,B: $i] : $false )
!= sk15 )
| ( ( sk22
@ ^ [A: $i,B: $i] : $false )
!= sk17 ) ),
inference(simp,[status(thm)],[1572]) ).
thf(1103,plain,
! [A: $i] :
( sk2
| ~ $true
| ~ ( sk1 @ A @ sk17 )
| sk2
| ( ( sk1
@ ( sk26
@ ^ [B: $i,C: $i] : $false )
@ ( sk27
@ ^ [B: $i,C: $i] : $false ) )
!= ( sk1 @ sk15 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[202,960]) ).
thf(1104,plain,
! [A: $i] :
( sk2
| ~ ( sk1 @ A @ sk17 )
| ( ( sk1
@ ( sk26
@ ^ [B: $i,C: $i] : $false )
@ ( sk27
@ ^ [B: $i,C: $i] : $false ) )
!= ( sk1 @ sk15 @ A ) ) ),
inference(simp,[status(thm)],[1103]) ).
thf(1129,plain,
! [A: $i] :
( sk2
| ~ ( sk1 @ A @ sk17 )
| ( ( sk26
@ ^ [B: $i,C: $i] : $false )
!= sk15 )
| ( ( sk27
@ ^ [B: $i,C: $i] : $false )
!= A ) ),
inference(simp,[status(thm)],[1104]) ).
thf(1139,plain,
( sk2
| ~ ( sk1
@ ( sk27
@ ^ [A: $i,B: $i] : $false )
@ sk17 )
| ( ( sk26
@ ^ [A: $i,B: $i] : $false )
!= sk15 ) ),
inference(simp,[status(thm)],[1129]) ).
thf(8316,plain,
! [B: $i,A: $i] :
( ~ sk2
| ~ $true
| ~ ( sk1 @ B @ A )
| ( ( sk1
@ ( sk13
@ ^ [C: $i,D: $i] : ~ sk2 )
@ ( sk14
@ ^ [C: $i,D: $i] : ~ sk2 ) )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[7494,31]) ).
thf(8317,plain,
! [B: $i,A: $i] :
( ~ sk2
| ~ ( sk1 @ B @ A )
| ( ( sk1
@ ( sk13
@ ^ [C: $i,D: $i] : ~ sk2 )
@ ( sk14
@ ^ [C: $i,D: $i] : ~ sk2 ) )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[8316]) ).
thf(8318,plain,
( ~ sk2
| ~ ( sk1
@ ( sk14
@ ^ [A: $i,B: $i] : ~ sk2 )
@ ( sk13
@ ^ [A: $i,B: $i] : ~ sk2 ) ) ),
inference(pattern_uni,[status(thm)],[8317:[bind(A,$thf( sk13 @ ^ [C: $i] : ^ [D: $i] : ~ ( sk2 ) )),bind(B,$thf( sk14 @ ^ [C: $i] : ^ [D: $i] : ~ ( sk2 ) ))]]) ).
thf(12844,plain,
! [A: $i] :
( sk2
| ( ( sk24 @ sk1 )
!= ( sk23 @ sk1 ) )
| ~ $true
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ A @ A ) ) ),
inference(paramod_ordered,[status(thm)],[12737,63]) ).
thf(12845,plain,
! [A: $i] :
( sk2
| ( ( sk24 @ sk1 )
!= ( sk23 @ sk1 ) )
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ A @ A ) ) ),
inference(simp,[status(thm)],[12844]) ).
thf(12929,plain,
! [A: $i] :
( sk2
| ( ( sk24 @ sk1 )
!= ( sk23 @ sk1 ) )
| ( sk16 != A )
| ( sk17 != A ) ),
inference(simp,[status(thm)],[12845]) ).
thf(12936,plain,
( sk2
| ( ( sk24 @ sk1 )
!= ( sk23 @ sk1 ) )
| ( sk17 != sk16 ) ),
inference(simp,[status(thm)],[12929]) ).
thf(221,plain,
( sk2
| sk2
| ~ $true
| ( ( sk1
@ ( sk26
@ ^ [A: $i,B: $i] : sk2 )
@ ( sk27
@ ^ [A: $i,B: $i] : sk2 ) )
!= ( sk1 @ sk15 @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[199,66]) ).
thf(222,plain,
( sk2
| ( ( sk1
@ ( sk26
@ ^ [A: $i,B: $i] : sk2 )
@ ( sk27
@ ^ [A: $i,B: $i] : sk2 ) )
!= ( sk1 @ sk15 @ sk17 ) ) ),
inference(simp,[status(thm)],[221]) ).
thf(245,plain,
( sk2
| ( ( sk26
@ ^ [A: $i,B: $i] : sk2 )
!= sk15 )
| ( ( sk27
@ ^ [A: $i,B: $i] : sk2 )
!= sk17 ) ),
inference(simp,[status(thm)],[222]) ).
thf(17684,plain,
( sk2
| ( ( sk20 @ sk1 )
!= ( sk19 @ sk1 ) )
| sk2
| ~ $true
| ( ( sk1 @ sk15 @ sk17 )
!= ( sk1 @ sk15 @ sk16 ) ) ),
inference(paramod_ordered,[status(thm)],[16106,66]) ).
thf(17685,plain,
( sk2
| ( ( sk20 @ sk1 )
!= ( sk19 @ sk1 ) )
| ( ( sk1 @ sk15 @ sk17 )
!= ( sk1 @ sk15 @ sk16 ) ) ),
inference(simp,[status(thm)],[17684]) ).
thf(17788,plain,
( sk2
| ( ( sk20 @ sk1 )
!= ( sk19 @ sk1 ) )
| ( sk15 != sk15 )
| ( sk17 != sk16 ) ),
inference(simp,[status(thm)],[17685]) ).
thf(17813,plain,
( sk2
| ( ( sk20 @ sk1 )
!= ( sk19 @ sk1 ) )
| ( sk17 != sk16 ) ),
inference(simp,[status(thm)],[17788]) ).
thf(14620,plain,
! [A: $i] :
( ~ sk2
| ( ( sk7 @ sk1 )
!= ( sk5 @ sk1 ) )
| ~ $true
| ( ( sk1 @ sk3 @ sk4 )
!= ( sk1 @ A @ A ) ) ),
inference(paramod_ordered,[status(thm)],[14483,63]) ).
thf(14621,plain,
! [A: $i] :
( ~ sk2
| ( ( sk7 @ sk1 )
!= ( sk5 @ sk1 ) )
| ( ( sk1 @ sk3 @ sk4 )
!= ( sk1 @ A @ A ) ) ),
inference(simp,[status(thm)],[14620]) ).
thf(14734,plain,
! [A: $i] :
( ~ sk2
| ( ( sk7 @ sk1 )
!= ( sk5 @ sk1 ) )
| ( sk3 != A )
| ( sk4 != A ) ),
inference(simp,[status(thm)],[14621]) ).
thf(14736,plain,
( ~ sk2
| ( ( sk7 @ sk1 )
!= ( sk5 @ sk1 ) )
| ( sk4 != sk3 ) ),
inference(simp,[status(thm)],[14734]) ).
thf(7553,plain,
! [A: $i] :
( ~ sk2
| ~ sk2
| ~ $true
| ~ ( sk1
@ ( sk9
@ ^ [B: $i,C: $i] : $false )
@ A )
| ( ( sk1
@ ( sk13
@ ^ [B: $i,C: $i] : $false )
@ ( sk14
@ ^ [B: $i,C: $i] : $false ) )
!= ( sk1 @ A
@ ( sk8
@ ^ [B: $i,C: $i] : $false ) ) ) ),
inference(paramod_ordered,[status(thm)],[7463,4480]) ).
thf(7554,plain,
! [A: $i] :
( ~ sk2
| ~ ( sk1
@ ( sk9
@ ^ [B: $i,C: $i] : $false )
@ A )
| ( ( sk1
@ ( sk13
@ ^ [B: $i,C: $i] : $false )
@ ( sk14
@ ^ [B: $i,C: $i] : $false ) )
!= ( sk1 @ A
@ ( sk8
@ ^ [B: $i,C: $i] : $false ) ) ) ),
inference(simp,[status(thm)],[7553]) ).
thf(7746,plain,
! [A: $i] :
( ~ sk2
| ~ ( sk1
@ ( sk9
@ ^ [B: $i,C: $i] : $false )
@ A )
| ( ( sk13
@ ^ [B: $i,C: $i] : $false )
!= A )
| ( ( sk14
@ ^ [B: $i,C: $i] : $false )
!= ( sk8
@ ^ [B: $i,C: $i] : $false ) ) ),
inference(simp,[status(thm)],[7554]) ).
thf(7778,plain,
( ~ sk2
| ~ ( sk1
@ ( sk9
@ ^ [A: $i,B: $i] : $false )
@ ( sk13
@ ^ [A: $i,B: $i] : $false ) )
| ( ( sk14
@ ^ [A: $i,B: $i] : $false )
!= ( sk8
@ ^ [A: $i,B: $i] : $false ) ) ),
inference(simp,[status(thm)],[7746]) ).
thf(7673,plain,
! [B: $i,A: $i] :
( ~ sk2
| ~ $true
| ~ ( sk1 @ B @ A )
| ( ( sk1
@ ( sk13
@ ^ [C: $i,D: $i] : $false )
@ ( sk14
@ ^ [C: $i,D: $i] : $false ) )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[7463,31]) ).
thf(7674,plain,
! [B: $i,A: $i] :
( ~ sk2
| ~ ( sk1 @ B @ A )
| ( ( sk1
@ ( sk13
@ ^ [C: $i,D: $i] : $false )
@ ( sk14
@ ^ [C: $i,D: $i] : $false ) )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[7673]) ).
thf(7675,plain,
( ~ sk2
| ~ ( sk1
@ ( sk14
@ ^ [A: $i,B: $i] : $false )
@ ( sk13
@ ^ [A: $i,B: $i] : $false ) ) ),
inference(pattern_uni,[status(thm)],[7674:[bind(A,$thf( sk13 @ ^ [C: $i] : ^ [D: $i] : $false )),bind(B,$thf( sk14 @ ^ [C: $i] : ^ [D: $i] : $false ))]]) ).
thf(9072,plain,
! [B: $i,A: $i] :
( ~ sk2
| ~ $true
| ~ ( sk1 @ B @ A )
| ( ( sk1
@ ( sk13
@ ^ [C: $i,D: $i] : $false )
@ ( sk14
@ ^ [C: $i,D: $i] : ~ sk2 ) )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[8441,31]) ).
thf(9073,plain,
! [B: $i,A: $i] :
( ~ sk2
| ~ ( sk1 @ B @ A )
| ( ( sk1
@ ( sk13
@ ^ [C: $i,D: $i] : $false )
@ ( sk14
@ ^ [C: $i,D: $i] : ~ sk2 ) )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[9072]) ).
thf(9074,plain,
( ~ sk2
| ~ ( sk1
@ ( sk14
@ ^ [A: $i,B: $i] : ~ sk2 )
@ ( sk13
@ ^ [A: $i,B: $i] : $false ) ) ),
inference(pattern_uni,[status(thm)],[9073:[bind(A,$thf( sk13 @ ^ [C: $i] : ^ [D: $i] : $false )),bind(B,$thf( sk14 @ ^ [C: $i] : ^ [D: $i] : ~ ( sk2 ) ))]]) ).
thf(11601,plain,
! [A: $i] :
( ~ sk2
| ( ( sk6 @ sk1 )
!= ( sk5 @ sk1 ) )
| ~ $true
| ( ( sk1 @ sk3 @ sk4 )
!= ( sk1 @ A @ A ) ) ),
inference(paramod_ordered,[status(thm)],[11467,63]) ).
thf(11602,plain,
! [A: $i] :
( ~ sk2
| ( ( sk6 @ sk1 )
!= ( sk5 @ sk1 ) )
| ( ( sk1 @ sk3 @ sk4 )
!= ( sk1 @ A @ A ) ) ),
inference(simp,[status(thm)],[11601]) ).
thf(11677,plain,
! [A: $i] :
( ~ sk2
| ( ( sk6 @ sk1 )
!= ( sk5 @ sk1 ) )
| ( sk3 != A )
| ( sk4 != A ) ),
inference(simp,[status(thm)],[11602]) ).
thf(11711,plain,
( ~ sk2
| ( ( sk6 @ sk1 )
!= ( sk5 @ sk1 ) )
| ( sk4 != sk3 ) ),
inference(simp,[status(thm)],[11677]) ).
thf(3361,plain,
! [B: $i,A: $i] :
( sk2
| ( sk1 @ sk16 @ sk17 )
| sk2
| ~ $true
| ( sk28 @ A @ B )
| ( ( sk1 @ ( sk24 @ sk1 ) @ ( sk25 @ sk1 ) )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[2767,40]) ).
thf(3362,plain,
! [B: $i,A: $i] :
( sk2
| ( sk1 @ sk16 @ sk17 )
| ( sk28 @ A @ B )
| ( ( sk1 @ ( sk24 @ sk1 ) @ ( sk25 @ sk1 ) )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[3361]) ).
thf(3363,plain,
( sk2
| ( sk1 @ sk16 @ sk17 )
| ( sk28 @ ( sk24 @ sk1 ) @ ( sk25 @ sk1 ) ) ),
inference(pattern_uni,[status(thm)],[3362:[bind(A,$thf( sk24 @ sk1 )),bind(B,$thf( sk25 @ sk1 ))]]) ).
thf(239,plain,
! [B: $i,A: $i] :
( sk2
| sk2
| ~ $true
| ( sk28 @ A @ B )
| ( ( sk1
@ ( sk26
@ ^ [C: $i,D: $i] : sk2 )
@ ( sk27
@ ^ [C: $i,D: $i] : sk2 ) )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[199,40]) ).
thf(240,plain,
! [B: $i,A: $i] :
( sk2
| ( sk28 @ A @ B )
| ( ( sk1
@ ( sk26
@ ^ [C: $i,D: $i] : sk2 )
@ ( sk27
@ ^ [C: $i,D: $i] : sk2 ) )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[239]) ).
thf(241,plain,
( sk2
| ( sk28
@ ( sk26
@ ^ [A: $i,B: $i] : sk2 )
@ ( sk27
@ ^ [A: $i,B: $i] : sk2 ) ) ),
inference(pattern_uni,[status(thm)],[240:[bind(A,$thf( sk26 @ ^ [C: $i] : ^ [D: $i] : sk2 )),bind(B,$thf( sk27 @ ^ [C: $i] : ^ [D: $i] : sk2 ))]]) ).
thf(17706,plain,
! [B: $i,A: $i] :
( sk2
| ( ( sk20 @ sk1 )
!= ( sk19 @ sk1 ) )
| ~ $true
| ~ ( sk1 @ B @ A )
| ( ( sk1 @ sk15 @ sk16 )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[16106,31]) ).
thf(17707,plain,
! [B: $i,A: $i] :
( sk2
| ( ( sk20 @ sk1 )
!= ( sk19 @ sk1 ) )
| ~ ( sk1 @ B @ A )
| ( ( sk1 @ sk15 @ sk16 )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[17706]) ).
thf(17708,plain,
( sk2
| ( ( sk20 @ sk1 )
!= ( sk19 @ sk1 ) )
| ~ ( sk1 @ sk16 @ sk15 ) ),
inference(pattern_uni,[status(thm)],[17707:[bind(A,$thf( sk15 )),bind(B,$thf( sk16 ))]]) ).
thf(20813,plain,
! [A: $i] :
( sk2
| ( ( sk25 @ sk1 )
!= ( sk23 @ sk1 ) )
| ~ ( sk1 @ sk15 @ A )
| ~ $true
| sk2
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ A @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[19090,960]) ).
thf(20814,plain,
! [A: $i] :
( sk2
| ( ( sk25 @ sk1 )
!= ( sk23 @ sk1 ) )
| ~ ( sk1 @ sk15 @ A )
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ A @ sk17 ) ) ),
inference(simp,[status(thm)],[20813]) ).
thf(20815,plain,
( sk2
| ( ( sk25 @ sk1 )
!= ( sk23 @ sk1 ) )
| ~ ( sk1 @ sk15 @ sk16 ) ),
inference(pattern_uni,[status(thm)],[20814:[bind(A,$thf( sk16 ))]]) ).
thf(17943,plain,
! [A: $i] :
( sk2
| ( ( sk19 @ sk1 )
!= ( sk18 @ sk1 ) )
| ~ $true
| ( ( sk1 @ sk15 @ sk16 )
!= ( sk1 @ A @ A ) ) ),
inference(paramod_ordered,[status(thm)],[16112,63]) ).
thf(17944,plain,
! [A: $i] :
( sk2
| ( ( sk19 @ sk1 )
!= ( sk18 @ sk1 ) )
| ( ( sk1 @ sk15 @ sk16 )
!= ( sk1 @ A @ A ) ) ),
inference(simp,[status(thm)],[17943]) ).
thf(18037,plain,
! [A: $i] :
( sk2
| ( ( sk19 @ sk1 )
!= ( sk18 @ sk1 ) )
| ( sk15 != A )
| ( sk16 != A ) ),
inference(simp,[status(thm)],[17944]) ).
thf(18060,plain,
( sk2
| ( ( sk19 @ sk1 )
!= ( sk18 @ sk1 ) )
| ( sk16 != sk15 ) ),
inference(simp,[status(thm)],[18037]) ).
thf(1464,plain,
! [A: $i] :
( sk2
| ~ $true
| ( ( sk1
@ ( sk21
@ ^ [B: $i,C: $i] : sk2 )
@ ( sk22
@ ^ [B: $i,C: $i] : sk2 ) )
!= ( sk1 @ A @ A ) ) ),
inference(paramod_ordered,[status(thm)],[1401,63]) ).
thf(1465,plain,
! [A: $i] :
( sk2
| ( ( sk1
@ ( sk21
@ ^ [B: $i,C: $i] : sk2 )
@ ( sk22
@ ^ [B: $i,C: $i] : sk2 ) )
!= ( sk1 @ A @ A ) ) ),
inference(simp,[status(thm)],[1464]) ).
thf(1530,plain,
! [A: $i] :
( sk2
| ( ( sk21
@ ^ [B: $i,C: $i] : sk2 )
!= A )
| ( ( sk22
@ ^ [B: $i,C: $i] : sk2 )
!= A ) ),
inference(simp,[status(thm)],[1465]) ).
thf(1547,plain,
( sk2
| ( ( sk22
@ ^ [A: $i,B: $i] : sk2 )
!= ( sk21
@ ^ [A: $i,B: $i] : sk2 ) ) ),
inference(simp,[status(thm)],[1530]) ).
thf(17951,plain,
! [B: $i,A: $i] :
( sk2
| ( ( sk19 @ sk1 )
!= ( sk18 @ sk1 ) )
| ~ $true
| ~ ( sk1 @ B @ A )
| ( ( sk1 @ sk15 @ sk16 )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[16112,31]) ).
thf(17952,plain,
! [B: $i,A: $i] :
( sk2
| ( ( sk19 @ sk1 )
!= ( sk18 @ sk1 ) )
| ~ ( sk1 @ B @ A )
| ( ( sk1 @ sk15 @ sk16 )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[17951]) ).
thf(17953,plain,
( sk2
| ( ( sk19 @ sk1 )
!= ( sk18 @ sk1 ) )
| ~ ( sk1 @ sk16 @ sk15 ) ),
inference(pattern_uni,[status(thm)],[17952:[bind(A,$thf( sk15 )),bind(B,$thf( sk16 ))]]) ).
thf(7555,plain,
! [A: $i] :
( ~ sk2
| ~ sk2
| ~ ( sk1 @ A
@ ( sk8
@ ^ [B: $i,C: $i] : $false ) )
| ~ $true
| ( ( sk1
@ ( sk13
@ ^ [B: $i,C: $i] : $false )
@ ( sk14
@ ^ [B: $i,C: $i] : $false ) )
!= ( sk1
@ ( sk9
@ ^ [B: $i,C: $i] : $false )
@ A ) ) ),
inference(paramod_ordered,[status(thm)],[7463,4480]) ).
thf(7556,plain,
! [A: $i] :
( ~ sk2
| ~ ( sk1 @ A
@ ( sk8
@ ^ [B: $i,C: $i] : $false ) )
| ( ( sk1
@ ( sk13
@ ^ [B: $i,C: $i] : $false )
@ ( sk14
@ ^ [B: $i,C: $i] : $false ) )
!= ( sk1
@ ( sk9
@ ^ [B: $i,C: $i] : $false )
@ A ) ) ),
inference(simp,[status(thm)],[7555]) ).
thf(7732,plain,
! [A: $i] :
( ~ sk2
| ~ ( sk1 @ A
@ ( sk8
@ ^ [B: $i,C: $i] : $false ) )
| ( ( sk13
@ ^ [B: $i,C: $i] : $false )
!= ( sk9
@ ^ [B: $i,C: $i] : $false ) )
| ( ( sk14
@ ^ [B: $i,C: $i] : $false )
!= A ) ),
inference(simp,[status(thm)],[7556]) ).
thf(7769,plain,
( ~ sk2
| ~ ( sk1
@ ( sk14
@ ^ [A: $i,B: $i] : $false )
@ ( sk8
@ ^ [A: $i,B: $i] : $false ) )
| ( ( sk13
@ ^ [A: $i,B: $i] : $false )
!= ( sk9
@ ^ [A: $i,B: $i] : $false ) ) ),
inference(simp,[status(thm)],[7732]) ).
thf(1462,plain,
( sk2
| sk2
| ~ $true
| ( ( sk1
@ ( sk21
@ ^ [A: $i,B: $i] : sk2 )
@ ( sk22
@ ^ [A: $i,B: $i] : sk2 ) )
!= ( sk1 @ sk15 @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[1401,66]) ).
thf(1463,plain,
( sk2
| ( ( sk1
@ ( sk21
@ ^ [A: $i,B: $i] : sk2 )
@ ( sk22
@ ^ [A: $i,B: $i] : sk2 ) )
!= ( sk1 @ sk15 @ sk17 ) ) ),
inference(simp,[status(thm)],[1462]) ).
thf(1538,plain,
( sk2
| ( ( sk21
@ ^ [A: $i,B: $i] : sk2 )
!= sk15 )
| ( ( sk22
@ ^ [A: $i,B: $i] : sk2 )
!= sk17 ) ),
inference(simp,[status(thm)],[1463]) ).
thf(16045,plain,
! [B: $i,A: $i] :
( sk2
| ( sk1 @ sk15 @ sk16 )
| sk2
| ~ $true
| ( sk28 @ A @ B )
| ( ( sk1 @ ( sk19 @ sk1 ) @ ( sk20 @ sk1 ) )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[15190,40]) ).
thf(16046,plain,
! [B: $i,A: $i] :
( sk2
| ( sk1 @ sk15 @ sk16 )
| ( sk28 @ A @ B )
| ( ( sk1 @ ( sk19 @ sk1 ) @ ( sk20 @ sk1 ) )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[16045]) ).
thf(16047,plain,
( sk2
| ( sk1 @ sk15 @ sk16 )
| ( sk28 @ ( sk19 @ sk1 ) @ ( sk20 @ sk1 ) ) ),
inference(pattern_uni,[status(thm)],[16046:[bind(A,$thf( sk19 @ sk1 )),bind(B,$thf( sk20 @ sk1 ))]]) ).
thf(1677,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( sk1 @ A @ B )
| ~ ( sk1 @ B @ C )
| ~ ( sk1 @ D @ E )
| ~ ( sk1 @ E @ F )
| ~ ( sk1 @ G @ D )
| ~ $true
| ( ( sk1 @ A @ C )
!= ( sk1 @ F @ G ) ) ),
inference(paramod_ordered,[status(thm)],[38,1020]) ).
thf(1678,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( sk1 @ A @ B )
| ~ ( sk1 @ B @ C )
| ~ ( sk1 @ D @ E )
| ~ ( sk1 @ E @ F )
| ~ ( sk1 @ G @ D )
| ( ( sk1 @ A @ C )
!= ( sk1 @ F @ G ) ) ),
inference(simp,[status(thm)],[1677]) ).
thf(1679,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( sk1 @ A @ B )
| ~ ( sk1 @ B @ C )
| ~ ( sk1 @ D @ E )
| ~ ( sk1 @ E @ A )
| ~ ( sk1 @ C @ D ) ),
inference(pattern_uni,[status(thm)],[1678:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( E )),bind(F,$thf( A )),bind(G,$thf( C ))]]) ).
thf(3421,plain,
( sk2
| ( ( sk25 @ sk1 )
!= ( sk24 @ sk1 ) )
| sk2
| ~ $true
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ sk15 @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[3414,66]) ).
thf(3422,plain,
( sk2
| ( ( sk25 @ sk1 )
!= ( sk24 @ sk1 ) )
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ sk15 @ sk17 ) ) ),
inference(simp,[status(thm)],[3421]) ).
thf(3549,plain,
( sk2
| ( ( sk25 @ sk1 )
!= ( sk24 @ sk1 ) )
| ( sk16 != sk15 )
| ( sk17 != sk17 ) ),
inference(simp,[status(thm)],[3422]) ).
thf(3564,plain,
( sk2
| ( ( sk25 @ sk1 )
!= ( sk24 @ sk1 ) )
| ( sk16 != sk15 ) ),
inference(simp,[status(thm)],[3549]) ).
thf(4878,plain,
! [A: $i] :
( ~ sk2
| ~ $true
| ( ( sk1
@ ( sk8
@ ^ [B: $i,C: $i] : ~ sk2 )
@ ( sk9
@ ^ [B: $i,C: $i] : ~ sk2 ) )
!= ( sk1 @ A @ A ) ) ),
inference(paramod_ordered,[status(thm)],[4272,63]) ).
thf(4879,plain,
! [A: $i] :
( ~ sk2
| ( ( sk1
@ ( sk8
@ ^ [B: $i,C: $i] : ~ sk2 )
@ ( sk9
@ ^ [B: $i,C: $i] : ~ sk2 ) )
!= ( sk1 @ A @ A ) ) ),
inference(simp,[status(thm)],[4878]) ).
thf(4949,plain,
! [A: $i] :
( ~ sk2
| ( ( sk8
@ ^ [B: $i,C: $i] : ~ sk2 )
!= A )
| ( ( sk9
@ ^ [B: $i,C: $i] : ~ sk2 )
!= A ) ),
inference(simp,[status(thm)],[4879]) ).
thf(4976,plain,
( ~ sk2
| ( ( sk9
@ ^ [A: $i,B: $i] : ~ sk2 )
!= ( sk8
@ ^ [A: $i,B: $i] : ~ sk2 ) ) ),
inference(simp,[status(thm)],[4949]) ).
thf(482,plain,
( sk2
| sk2
| ~ $true
| ( ( sk1
@ ( sk27
@ ^ [A: $i,B: $i] : sk2 )
@ ( sk26
@ ^ [A: $i,B: $i] : sk2 ) )
!= ( sk1
@ ( sk26
@ ^ [A: $i,B: $i] : $false )
@ ( sk27
@ ^ [A: $i,B: $i] : $false ) ) ) ),
inference(paramod_ordered,[status(thm)],[202,235]) ).
thf(483,plain,
( sk2
| ( ( sk1
@ ( sk27
@ ^ [A: $i,B: $i] : sk2 )
@ ( sk26
@ ^ [A: $i,B: $i] : sk2 ) )
!= ( sk1
@ ( sk26
@ ^ [A: $i,B: $i] : $false )
@ ( sk27
@ ^ [A: $i,B: $i] : $false ) ) ) ),
inference(simp,[status(thm)],[482]) ).
thf(491,plain,
( sk2
| ( ( sk27
@ ^ [A: $i,B: $i] : sk2 )
!= ( sk26
@ ^ [A: $i,B: $i] : $false ) )
| ( ( sk27
@ ^ [A: $i,B: $i] : $false )
!= ( sk26
@ ^ [A: $i,B: $i] : sk2 ) ) ),
inference(simp,[status(thm)],[483]) ).
thf(991,plain,
( sk2
| ( ( sk27
@ ^ [A: $i,B: $i] : $false )
!= ( sk26
@ ^ [A: $i,B: $i] : sk2 ) )
| ( ( sk27
@ ^ [A: $i,B: $i] : sk2 )
!= ( sk27
@ ^ [A: $i,B: $i] : $false ) )
| ( ( sk26
@ ^ [A: $i,B: $i] : sk2 )
!= ( sk26
@ ^ [A: $i,B: $i] : $false ) ) ),
inference(eqfactor_ordered,[status(thm)],[491]) ).
thf(996,plain,
( sk2
| ( ( sk27
@ ^ [A: $i,B: $i] : $false )
!= ( sk26
@ ^ [A: $i,B: $i] : sk2 ) )
| ( ( ^ [A: $i,B: $i] : sk2 )
!= ( ^ [A: $i,B: $i] : $false ) )
| ( ( ^ [A: $i,B: $i] : sk2 )
!= ( ^ [A: $i,B: $i] : $false ) ) ),
inference(simp,[status(thm)],[991]) ).
thf(999,plain,
( sk2
| ( ( sk27
@ ^ [A: $i,B: $i] : $false )
!= ( sk26
@ ^ [A: $i,B: $i] : sk2 ) )
| ( ( ^ [A: $i,B: $i] : sk2 )
!= ( ^ [A: $i,B: $i] : $false ) ) ),
inference(simp,[status(thm)],[996]) ).
thf(1000,plain,
( sk2
| sk2
| ( ( sk27
@ ^ [A: $i,B: $i] : $false )
!= ( sk26
@ ^ [A: $i,B: $i] : sk2 ) ) ),
inference(func_ext,[status(esa)],[999]) ).
thf(1008,plain,
( sk2
| ( ( sk27
@ ^ [A: $i,B: $i] : $false )
!= ( sk26
@ ^ [A: $i,B: $i] : sk2 ) ) ),
inference(simp,[status(thm)],[1000]) ).
thf(1615,plain,
! [B: $i,A: $i] :
( sk2
| ~ $true
| ~ ( sk1 @ B @ A )
| ( ( sk1
@ ( sk21
@ ^ [C: $i,D: $i] : $false )
@ ( sk22
@ ^ [C: $i,D: $i] : $false ) )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[1402,31]) ).
thf(1616,plain,
! [B: $i,A: $i] :
( sk2
| ~ ( sk1 @ B @ A )
| ( ( sk1
@ ( sk21
@ ^ [C: $i,D: $i] : $false )
@ ( sk22
@ ^ [C: $i,D: $i] : $false ) )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[1615]) ).
thf(1617,plain,
( sk2
| ~ ( sk1
@ ( sk22
@ ^ [A: $i,B: $i] : $false )
@ ( sk21
@ ^ [A: $i,B: $i] : $false ) ) ),
inference(pattern_uni,[status(thm)],[1616:[bind(A,$thf( sk21 @ ^ [C: $i] : ^ [D: $i] : $false )),bind(B,$thf( sk22 @ ^ [C: $i] : ^ [D: $i] : $false ))]]) ).
thf(17731,plain,
! [B: $i,A: $i] :
( sk2
| ( ( sk20 @ sk1 )
!= ( sk19 @ sk1 ) )
| sk2
| ~ $true
| ( sk28 @ A @ B )
| ( ( sk1 @ sk15 @ sk16 )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[16106,40]) ).
thf(17732,plain,
! [B: $i,A: $i] :
( sk2
| ( ( sk20 @ sk1 )
!= ( sk19 @ sk1 ) )
| ( sk28 @ A @ B )
| ( ( sk1 @ sk15 @ sk16 )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[17731]) ).
thf(17733,plain,
( sk2
| ( ( sk20 @ sk1 )
!= ( sk19 @ sk1 ) )
| ( sk28 @ sk15 @ sk16 ) ),
inference(pattern_uni,[status(thm)],[17732:[bind(A,$thf( sk15 )),bind(B,$thf( sk16 ))]]) ).
thf(1613,plain,
! [A: $i] :
( sk2
| ~ $true
| ( ( sk1
@ ( sk21
@ ^ [B: $i,C: $i] : $false )
@ ( sk22
@ ^ [B: $i,C: $i] : $false ) )
!= ( sk1 @ A @ A ) ) ),
inference(paramod_ordered,[status(thm)],[1402,63]) ).
thf(1614,plain,
! [A: $i] :
( sk2
| ( ( sk1
@ ( sk21
@ ^ [B: $i,C: $i] : $false )
@ ( sk22
@ ^ [B: $i,C: $i] : $false ) )
!= ( sk1 @ A @ A ) ) ),
inference(simp,[status(thm)],[1613]) ).
thf(1644,plain,
! [A: $i] :
( sk2
| ( ( sk21
@ ^ [B: $i,C: $i] : $false )
!= A )
| ( ( sk22
@ ^ [B: $i,C: $i] : $false )
!= A ) ),
inference(simp,[status(thm)],[1614]) ).
thf(1654,plain,
( sk2
| ( ( sk22
@ ^ [A: $i,B: $i] : $false )
!= ( sk21
@ ^ [A: $i,B: $i] : $false ) ) ),
inference(simp,[status(thm)],[1644]) ).
thf(1577,plain,
( sk2
| sk2
| ~ $true
| ( ( sk1
@ ( sk27
@ ^ [A: $i,B: $i] : $false )
@ ( sk26
@ ^ [A: $i,B: $i] : $false ) )
!= ( sk1
@ ( sk21
@ ^ [A: $i,B: $i] : $false )
@ ( sk22
@ ^ [A: $i,B: $i] : $false ) ) ) ),
inference(paramod_ordered,[status(thm)],[1402,337]) ).
thf(1578,plain,
( sk2
| ( ( sk1
@ ( sk27
@ ^ [A: $i,B: $i] : $false )
@ ( sk26
@ ^ [A: $i,B: $i] : $false ) )
!= ( sk1
@ ( sk21
@ ^ [A: $i,B: $i] : $false )
@ ( sk22
@ ^ [A: $i,B: $i] : $false ) ) ) ),
inference(simp,[status(thm)],[1577]) ).
thf(1646,plain,
( sk2
| ( ( sk27
@ ^ [A: $i,B: $i] : $false )
!= ( sk21
@ ^ [A: $i,B: $i] : $false ) )
| ( ( sk26
@ ^ [A: $i,B: $i] : $false )
!= ( sk22
@ ^ [A: $i,B: $i] : $false ) ) ),
inference(simp,[status(thm)],[1578]) ).
thf(16265,plain,
! [B: $i,A: $i] :
( ~ sk2
| ( ( sk11 @ sk1 )
!= ( sk10 @ sk1 ) )
| ~ $true
| ~ ( sk1 @ B @ A )
| ( ( sk1 @ sk4 @ sk3 )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[15439,31]) ).
thf(16266,plain,
! [B: $i,A: $i] :
( ~ sk2
| ( ( sk11 @ sk1 )
!= ( sk10 @ sk1 ) )
| ~ ( sk1 @ B @ A )
| ( ( sk1 @ sk4 @ sk3 )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[16265]) ).
thf(16267,plain,
( ~ sk2
| ( ( sk11 @ sk1 )
!= ( sk10 @ sk1 ) )
| ~ ( sk1 @ sk3 @ sk4 ) ),
inference(pattern_uni,[status(thm)],[16266:[bind(A,$thf( sk4 )),bind(B,$thf( sk3 ))]]) ).
thf(1506,plain,
! [B: $i,A: $i] :
( sk2
| ~ $true
| ~ ( sk1 @ B @ A )
| ( ( sk1
@ ( sk21
@ ^ [C: $i,D: $i] : sk2 )
@ ( sk22
@ ^ [C: $i,D: $i] : sk2 ) )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[1401,31]) ).
thf(1507,plain,
! [B: $i,A: $i] :
( sk2
| ~ ( sk1 @ B @ A )
| ( ( sk1
@ ( sk21
@ ^ [C: $i,D: $i] : sk2 )
@ ( sk22
@ ^ [C: $i,D: $i] : sk2 ) )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[1506]) ).
thf(1508,plain,
( sk2
| ~ ( sk1
@ ( sk22
@ ^ [A: $i,B: $i] : sk2 )
@ ( sk21
@ ^ [A: $i,B: $i] : sk2 ) ) ),
inference(pattern_uni,[status(thm)],[1507:[bind(A,$thf( sk21 @ ^ [C: $i] : ^ [D: $i] : sk2 )),bind(B,$thf( sk22 @ ^ [C: $i] : ^ [D: $i] : sk2 ))]]) ).
thf(1849,plain,
( sk2
| sk2
| ~ $true
| ( ( sk1
@ ( sk22
@ ^ [A: $i,B: $i] : sk2 )
@ ( sk21
@ ^ [A: $i,B: $i] : sk2 ) )
!= ( sk1
@ ( sk21
@ ^ [A: $i,B: $i] : $false )
@ ( sk22
@ ^ [A: $i,B: $i] : $false ) ) ) ),
inference(paramod_ordered,[status(thm)],[1402,1508]) ).
thf(1850,plain,
( sk2
| ( ( sk1
@ ( sk22
@ ^ [A: $i,B: $i] : sk2 )
@ ( sk21
@ ^ [A: $i,B: $i] : sk2 ) )
!= ( sk1
@ ( sk21
@ ^ [A: $i,B: $i] : $false )
@ ( sk22
@ ^ [A: $i,B: $i] : $false ) ) ) ),
inference(simp,[status(thm)],[1849]) ).
thf(1873,plain,
( sk2
| ( ( sk22
@ ^ [A: $i,B: $i] : sk2 )
!= ( sk21
@ ^ [A: $i,B: $i] : $false ) )
| ( ( sk22
@ ^ [A: $i,B: $i] : $false )
!= ( sk21
@ ^ [A: $i,B: $i] : sk2 ) ) ),
inference(simp,[status(thm)],[1850]) ).
thf(6810,plain,
( sk2
| ( ( sk22
@ ^ [A: $i,B: $i] : $false )
!= ( sk21
@ ^ [A: $i,B: $i] : sk2 ) )
| ( ( sk22
@ ^ [A: $i,B: $i] : sk2 )
!= ( sk22
@ ^ [A: $i,B: $i] : $false ) )
| ( ( sk21
@ ^ [A: $i,B: $i] : sk2 )
!= ( sk21
@ ^ [A: $i,B: $i] : $false ) ) ),
inference(eqfactor_ordered,[status(thm)],[1873]) ).
thf(6817,plain,
( sk2
| ( ( sk22
@ ^ [A: $i,B: $i] : $false )
!= ( sk21
@ ^ [A: $i,B: $i] : sk2 ) )
| ( ( ^ [A: $i,B: $i] : sk2 )
!= ( ^ [A: $i,B: $i] : $false ) )
| ( ( ^ [A: $i,B: $i] : sk2 )
!= ( ^ [A: $i,B: $i] : $false ) ) ),
inference(simp,[status(thm)],[6810]) ).
thf(6820,plain,
( sk2
| ( ( sk22
@ ^ [A: $i,B: $i] : $false )
!= ( sk21
@ ^ [A: $i,B: $i] : sk2 ) )
| ( ( ^ [A: $i,B: $i] : sk2 )
!= ( ^ [A: $i,B: $i] : $false ) ) ),
inference(simp,[status(thm)],[6817]) ).
thf(7989,plain,
( sk2
| sk2
| ( ( sk22
@ ^ [A: $i,B: $i] : $false )
!= ( sk21
@ ^ [A: $i,B: $i] : sk2 ) ) ),
inference(func_ext,[status(esa)],[6820]) ).
thf(8011,plain,
( sk2
| ( ( sk22
@ ^ [A: $i,B: $i] : $false )
!= ( sk21
@ ^ [A: $i,B: $i] : sk2 ) ) ),
inference(simp,[status(thm)],[7989]) ).
thf(3514,plain,
! [B: $i,A: $i] :
( sk2
| ( ( sk25 @ sk1 )
!= ( sk24 @ sk1 ) )
| sk2
| ~ $true
| ( sk28 @ A @ B )
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[3414,40]) ).
thf(3515,plain,
! [B: $i,A: $i] :
( sk2
| ( ( sk25 @ sk1 )
!= ( sk24 @ sk1 ) )
| ( sk28 @ A @ B )
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[3514]) ).
thf(3516,plain,
( sk2
| ( ( sk25 @ sk1 )
!= ( sk24 @ sk1 ) )
| ( sk28 @ sk16 @ sk17 ) ),
inference(pattern_uni,[status(thm)],[3515:[bind(A,$thf( sk16 )),bind(B,$thf( sk17 ))]]) ).
thf(1573,plain,
( sk2
| sk2
| ~ $true
| ( ( sk1
@ ( sk27
@ ^ [A: $i,B: $i] : sk2 )
@ ( sk26
@ ^ [A: $i,B: $i] : sk2 ) )
!= ( sk1
@ ( sk21
@ ^ [A: $i,B: $i] : $false )
@ ( sk22
@ ^ [A: $i,B: $i] : $false ) ) ) ),
inference(paramod_ordered,[status(thm)],[1402,235]) ).
thf(1574,plain,
( sk2
| ( ( sk1
@ ( sk27
@ ^ [A: $i,B: $i] : sk2 )
@ ( sk26
@ ^ [A: $i,B: $i] : sk2 ) )
!= ( sk1
@ ( sk21
@ ^ [A: $i,B: $i] : $false )
@ ( sk22
@ ^ [A: $i,B: $i] : $false ) ) ) ),
inference(simp,[status(thm)],[1573]) ).
thf(1642,plain,
( sk2
| ( ( sk27
@ ^ [A: $i,B: $i] : sk2 )
!= ( sk21
@ ^ [A: $i,B: $i] : $false ) )
| ( ( sk26
@ ^ [A: $i,B: $i] : sk2 )
!= ( sk22
@ ^ [A: $i,B: $i] : $false ) ) ),
inference(simp,[status(thm)],[1574]) ).
thf(1517,plain,
! [A: $i] :
( sk2
| ~ ( sk1 @ sk15 @ A )
| ~ $true
| sk2
| ( ( sk1
@ ( sk21
@ ^ [B: $i,C: $i] : sk2 )
@ ( sk22
@ ^ [B: $i,C: $i] : sk2 ) )
!= ( sk1 @ A @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[1401,960]) ).
thf(1518,plain,
! [A: $i] :
( sk2
| ~ ( sk1 @ sk15 @ A )
| ( ( sk1
@ ( sk21
@ ^ [B: $i,C: $i] : sk2 )
@ ( sk22
@ ^ [B: $i,C: $i] : sk2 ) )
!= ( sk1 @ A @ sk17 ) ) ),
inference(simp,[status(thm)],[1517]) ).
thf(1529,plain,
! [A: $i] :
( sk2
| ~ ( sk1 @ sk15 @ A )
| ( ( sk21
@ ^ [B: $i,C: $i] : sk2 )
!= A )
| ( ( sk22
@ ^ [B: $i,C: $i] : sk2 )
!= sk17 ) ),
inference(simp,[status(thm)],[1518]) ).
thf(1546,plain,
( sk2
| ~ ( sk1 @ sk15
@ ( sk21
@ ^ [A: $i,B: $i] : sk2 ) )
| ( ( sk22
@ ^ [A: $i,B: $i] : sk2 )
!= sk17 ) ),
inference(simp,[status(thm)],[1529]) ).
thf(15478,plain,
( ~ sk2
| ( ( sk12 @ sk1 )
!= ( sk11 @ sk1 ) )
| ~ sk2
| ( ( sk7 @ sk1 )
!= ( sk5 @ sk1 ) )
| ~ $true
| ( ( sk1 @ sk4 @ sk3 )
!= ( sk1 @ sk4 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[15437,14630]) ).
thf(15479,plain,
( ~ sk2
| ( ( sk12 @ sk1 )
!= ( sk11 @ sk1 ) )
| ( ( sk7 @ sk1 )
!= ( sk5 @ sk1 ) )
| ( ( sk1 @ sk4 @ sk3 )
!= ( sk1 @ sk4 @ sk3 ) ) ),
inference(simp,[status(thm)],[15478]) ).
thf(15480,plain,
( ~ sk2
| ( ( sk12 @ sk1 )
!= ( sk11 @ sk1 ) )
| ( ( sk7 @ sk1 )
!= ( sk5 @ sk1 ) ) ),
inference(pattern_uni,[status(thm)],[15479:[]]) ).
thf(20767,plain,
! [B: $i,A: $i] :
( sk2
| ( ( sk25 @ sk1 )
!= ( sk23 @ sk1 ) )
| ~ $true
| ~ ( sk1 @ B @ A )
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[19090,31]) ).
thf(20768,plain,
! [B: $i,A: $i] :
( sk2
| ( ( sk25 @ sk1 )
!= ( sk23 @ sk1 ) )
| ~ ( sk1 @ B @ A )
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[20767]) ).
thf(20769,plain,
( sk2
| ( ( sk25 @ sk1 )
!= ( sk23 @ sk1 ) )
| ~ ( sk1 @ sk17 @ sk16 ) ),
inference(pattern_uni,[status(thm)],[20768:[bind(A,$thf( sk16 )),bind(B,$thf( sk17 ))]]) ).
thf(3487,plain,
! [A: $i] :
( sk2
| ( ( sk25 @ sk1 )
!= ( sk24 @ sk1 ) )
| ~ $true
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ A @ A ) ) ),
inference(paramod_ordered,[status(thm)],[3414,63]) ).
thf(3488,plain,
! [A: $i] :
( sk2
| ( ( sk25 @ sk1 )
!= ( sk24 @ sk1 ) )
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ A @ A ) ) ),
inference(simp,[status(thm)],[3487]) ).
thf(3542,plain,
! [A: $i] :
( sk2
| ( ( sk25 @ sk1 )
!= ( sk24 @ sk1 ) )
| ( sk16 != A )
| ( sk17 != A ) ),
inference(simp,[status(thm)],[3488]) ).
thf(3560,plain,
( sk2
| ( ( sk25 @ sk1 )
!= ( sk24 @ sk1 ) )
| ( sk17 != sk16 ) ),
inference(simp,[status(thm)],[3542]) ).
thf(3504,plain,
! [B: $i,A: $i] :
( sk2
| ( ( sk25 @ sk1 )
!= ( sk24 @ sk1 ) )
| ~ $true
| ~ ( sk1 @ B @ A )
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[3414,31]) ).
thf(3505,plain,
! [B: $i,A: $i] :
( sk2
| ( ( sk25 @ sk1 )
!= ( sk24 @ sk1 ) )
| ~ ( sk1 @ B @ A )
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[3504]) ).
thf(3506,plain,
( sk2
| ( ( sk25 @ sk1 )
!= ( sk24 @ sk1 ) )
| ~ ( sk1 @ sk17 @ sk16 ) ),
inference(pattern_uni,[status(thm)],[3505:[bind(A,$thf( sk16 )),bind(B,$thf( sk17 ))]]) ).
thf(17976,plain,
! [B: $i,A: $i] :
( sk2
| ( ( sk19 @ sk1 )
!= ( sk18 @ sk1 ) )
| sk2
| ~ $true
| ( sk28 @ A @ B )
| ( ( sk1 @ sk15 @ sk16 )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[16112,40]) ).
thf(17977,plain,
! [B: $i,A: $i] :
( sk2
| ( ( sk19 @ sk1 )
!= ( sk18 @ sk1 ) )
| ( sk28 @ A @ B )
| ( ( sk1 @ sk15 @ sk16 )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[17976]) ).
thf(17978,plain,
( sk2
| ( ( sk19 @ sk1 )
!= ( sk18 @ sk1 ) )
| ( sk28 @ sk15 @ sk16 ) ),
inference(pattern_uni,[status(thm)],[17977:[bind(A,$thf( sk15 )),bind(B,$thf( sk16 ))]]) ).
thf(17991,plain,
! [A: $i] :
( sk2
| ( ( sk19 @ sk1 )
!= ( sk18 @ sk1 ) )
| ~ $true
| ~ ( sk1 @ A @ sk17 )
| sk2
| ( ( sk1 @ sk15 @ sk16 )
!= ( sk1 @ sk15 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[16112,960]) ).
thf(17992,plain,
! [A: $i] :
( sk2
| ( ( sk19 @ sk1 )
!= ( sk18 @ sk1 ) )
| ~ ( sk1 @ A @ sk17 )
| ( ( sk1 @ sk15 @ sk16 )
!= ( sk1 @ sk15 @ A ) ) ),
inference(simp,[status(thm)],[17991]) ).
thf(17993,plain,
( sk2
| ( ( sk19 @ sk1 )
!= ( sk18 @ sk1 ) )
| ~ ( sk1 @ sk16 @ sk17 ) ),
inference(pattern_uni,[status(thm)],[17992:[bind(A,$thf( sk16 ))]]) ).
thf(14267,plain,
! [B: $i,A: $i] :
( ( sk1 @ sk3 @ sk4 )
| ~ sk2
| ~ $true
| ~ ( sk1 @ B @ A )
| ( ( sk1 @ ( sk5 @ sk1 ) @ ( sk6 @ sk1 ) )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[11168,31]) ).
thf(14268,plain,
! [B: $i,A: $i] :
( ( sk1 @ sk3 @ sk4 )
| ~ sk2
| ~ ( sk1 @ B @ A )
| ( ( sk1 @ ( sk5 @ sk1 ) @ ( sk6 @ sk1 ) )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[14267]) ).
thf(14269,plain,
( ( sk1 @ sk3 @ sk4 )
| ~ sk2
| ~ ( sk1 @ ( sk6 @ sk1 ) @ ( sk5 @ sk1 ) ) ),
inference(pattern_uni,[status(thm)],[14268:[bind(A,$thf( sk5 @ sk1 )),bind(B,$thf( sk6 @ sk1 ))]]) ).
thf(12832,plain,
( sk2
| ( ( sk24 @ sk1 )
!= ( sk23 @ sk1 ) )
| sk2
| ~ $true
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ sk15 @ sk17 ) ) ),
inference(paramod_ordered,[status(thm)],[12737,66]) ).
thf(12833,plain,
( sk2
| ( ( sk24 @ sk1 )
!= ( sk23 @ sk1 ) )
| ( ( sk1 @ sk16 @ sk17 )
!= ( sk1 @ sk15 @ sk17 ) ) ),
inference(simp,[status(thm)],[12832]) ).
thf(12917,plain,
( sk2
| ( ( sk24 @ sk1 )
!= ( sk23 @ sk1 ) )
| ( sk16 != sk15 )
| ( sk17 != sk17 ) ),
inference(simp,[status(thm)],[12833]) ).
thf(12948,plain,
( sk2
| ( ( sk24 @ sk1 )
!= ( sk23 @ sk1 ) )
| ( sk16 != sk15 ) ),
inference(simp,[status(thm)],[12917]) ).
thf(71,plain,
! [A: $i > $i > $o] :
( ~ ( A @ ( sk5 @ A ) @ ( sk7 @ A ) )
| ( A @ sk3 @ sk4 )
| ~ sk2
| ( ( A @ ( sk8 @ A ) @ ( sk9 @ A ) )
!= ( A @ ( sk5 @ A ) @ ( sk7 @ A ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[37]) ).
thf(82,plain,
! [A: $i > $i > $o] :
( ~ ( A @ ( sk5 @ A ) @ ( sk7 @ A ) )
| ( A @ sk3 @ sk4 )
| ~ sk2
| ( ( A @ ( sk8 @ A ) @ ( sk9 @ A ) )
!= ( A @ ( sk5 @ A ) @ ( sk7 @ A ) ) ) ),
inference(pre_uni,[status(thm)],[71:[]]) ).
thf(83,plain,
! [A: $i > $i > $o] :
( ~ sk2
| ( A @ sk3 @ sk4 )
| ~ ( A @ ( sk5 @ A ) @ ( sk7 @ A ) )
| ( ( A @ ( sk8 @ A ) @ ( sk9 @ A ) )
!= ( A @ ( sk5 @ A ) @ ( sk7 @ A ) ) ) ),
inference(pre_uni,[status(thm)],[82:[]]) ).
thf(27711,plain,
$false,
inference(e,[status(thm)],[11394,1549,352,115,4515,18459,1401,8695,247,202,15190,20798,7781,1533,56,12852,4884,20882,20885,3414,4294,42,14483,37,1623,14630,52,8426,344,3353,7743,1132,1514,11609,2767,46,57,15659,1136,1020,11168,3527,9557,12090,12892,13231,17811,60,4480,9175,7735,22136,15439,12737,38,15491,1656,6143,522,1402,5189,12493,1534,53,8429,11467,2450,7463,16112,7749,41,1131,15602,343,17482,19090,18059,34,16390,45,19017,733,17748,44,1652,59,8581,4975,10127,12877,11483,54,15718,1638,1139,8318,49,12936,6059,81,245,39,17813,14736,66,7778,7675,9074,11711,3363,8441,3,241,35,17708,20815,18060,1547,48,63,17953,14101,4272,4971,50,199,7494,7769,8148,1538,31,4437,16047,1679,3564,16106,4976,1008,43,1617,17733,1654,1646,16267,40,8011,55,3516,5104,15437,26,1508,58,235,1642,36,1546,51,15480,20769,3560,960,3506,17978,928,17993,14269,47,12948,337,83,11985]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU496^1 : TPTP v9.3.1. Released v3.6.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.11/0.21 % Computer : n002.cluster.edu
% 0.11/0.21 % Model : x86_64 x86_64
% 0.11/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.21 % Memory : 8046.5625MB
% 0.11/0.21 % OS : Linux 6.8.0-71-generic
% 0.11/0.21 % CPULimit : 300
% 0.11/0.21 % WCLimit : 300
% 0.11/0.21 % DateTime : Tue Sep 29 13:49:01 UTC 2026
% 0.11/0.22 % CPUTime :
% 0.11/0.22 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.75/0.55 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.20/0.77 % [INFO] Parsing done (221ms).
% 1.20/0.78 % [INFO] Running in sequential loop mode.
% 2.45/1.35 % [INFO] eprover registered as external prover.
% 2.45/1.36 % [INFO] Scanning for conjecture ...
% 3.13/1.62 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 3.13/1.66 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 3.13/1.66 % [INFO] Problem is higher-order (TPTP THF).
% 3.13/1.67 % [INFO] Type checking passed.
% 3.13/1.67 % [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 ...
% 90.81/19.35 % External prover 'e' found a proof!
% 90.81/19.35 % [INFO] Killing All external provers ...
% 90.81/19.36 % Time passed: 19046ms (effective reasoning time: 18570ms)
% 90.81/19.36 % 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)>
% 90.81/19.36 % Axioms used in derivation (0):
% 90.81/19.36 % No. of inferences in proof: 554
% 90.81/19.36 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 19046 ms resp. 18570 ms w/o parsing
% 78.07/19.69 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 78.07/19.69 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------