%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SEV119^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n026.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:36:52 AM UTC 2026
% Result : Theorem 249.12s 125.90s
% Output : Refutation 249.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 76
% Syntax : Number of formulae : 259 ( 122 unt; 0 typ; 75 def)
% Number of atoms : 2216 ( 181 equ; 0 cnn)
% Maximal formula atoms : 132 ( 8 avg)
% Number of connectives : 8402 ( 865 ~;1194 |; 463 &;5290 @)
% ( 0 <=>; 590 =>; 0 <=; 0 <~>)
% Maximal formula depth : 48 ( 6 avg)
% Number of types : 2 ( 1 usr)
% Number of type conns : 662 ( 662 >; 0 *; 0 +; 0 <<)
% Number of symbols : 99 ( 96 usr; 38 con; 0-6 aty)
% Number of variables : 1255 ( 270 ^; 910 !; 0 ?;1255 :)
% ( 0 !>; 0 ?*; 0 @-; 75 @+)
% Comments :
%------------------------------------------------------------------------------
thf(a_type,type,
a: $tType ).
thf(sk1_decl,type,
sk1: ( a > a > $o ) > $o ).
thf(sk2_decl,type,
sk2: a > a > $o ).
thf(sk3_decl,type,
sk3: a > a > $o ).
thf(sk4_decl,type,
sk4: a ).
thf(sk5_decl,type,
sk5: a ).
thf(sk6_decl,type,
sk6: a ).
thf(sk7_decl,type,
sk7: a ).
thf(sk8_decl,type,
sk8: a > a > $o ).
thf(sk11_decl,type,
sk11: a > a > $o ).
thf(sk14_decl,type,
sk14: a > a > $o ).
thf(sk17_decl,type,
sk17: a > a > $o ).
thf(sk18_decl,type,
sk18: a ).
thf(sk21_decl,type,
sk21: a > a > $o ).
thf(sk22_decl,type,
sk22: a ).
thf(sk23_decl,type,
sk23: a ).
thf(sk27_decl,type,
sk27: a ).
thf(sk28_decl,type,
sk28: a ).
thf(sk32_decl,type,
sk32: a ).
thf(sk33_decl,type,
sk33: a ).
thf(sk37_decl,type,
sk37: a ).
thf(sk38_decl,type,
sk38: a ).
thf(sk39_decl,type,
sk39: a > a > $o ).
thf(sk40_decl,type,
sk40: a > a > a > a > $o ).
thf(sk51_decl,type,
sk51: a > a > $o ).
thf(sk52_decl,type,
sk52: a > a > a > a > $o ).
thf(sk53_decl,type,
sk53: a > a > a > a > a > a > $o ).
thf(sk54_decl,type,
sk54: a > a > a > a > a > a > $o ).
thf(sk63_decl,type,
sk63: a ).
thf(sk64_decl,type,
sk64: a ).
thf(sk65_decl,type,
sk65: a ).
thf(sk66_decl,type,
sk66: a ).
thf(sk67_decl,type,
sk67: ( a > a > $o ) > a ).
thf(sk68_decl,type,
sk68: ( a > a > $o ) > a ).
thf(sk69_decl,type,
sk69: ( a > a > $o ) > a ).
thf(sk70_decl,type,
sk70: ( a > a > $o ) > a ).
thf(sk73_decl,type,
sk73: a > a > a > a > a > a > $o ).
thf(sk74_decl,type,
sk74: a > a > a > a > a > a > $o ).
thf(sk83_decl,type,
sk83: a > a > $o ).
thf(sk84_decl,type,
sk84: a > a > $o ).
thf(sk89_decl,type,
sk89: a ).
thf(sk90_decl,type,
sk90: a ).
thf(sk91_decl,type,
sk91: ( a > a > $o ) > a ).
thf(sk92_decl,type,
sk92: ( a > a > $o ) > a ).
thf(sk93_decl,type,
sk93: ( a > a > $o ) > a ).
thf(sk94_decl,type,
sk94: ( a > a > $o ) > a ).
thf(sk95_decl,type,
sk95: a > a > a > a > $o ).
thf(sk96_decl,type,
sk96: a > a > a > a > $o ).
thf(sk97_decl,type,
sk97: a ).
thf(sk98_decl,type,
sk98: a ).
thf(sk99_decl,type,
sk99: a ).
thf(sk100_decl,type,
sk100: a ).
thf(sk101_decl,type,
sk101: ( a > a > $o ) > a ).
thf(sk102_decl,type,
sk102: ( a > a > $o ) > a ).
thf(sk103_decl,type,
sk103: ( a > a > $o ) > a ).
thf(sk104_decl,type,
sk104: ( a > a > $o ) > a ).
thf(sk105_decl,type,
sk105: a > a > a > a > a > a > $o ).
thf(sk106_decl,type,
sk106: a > a > a > a > a > a > $o ).
thf(sk107_decl,type,
sk107: a ).
thf(sk108_decl,type,
sk108: a ).
thf(sk109_decl,type,
sk109: a ).
thf(sk110_decl,type,
sk110: a ).
thf(sk111_decl,type,
sk111: ( a > a > $o ) > a ).
thf(sk112_decl,type,
sk112: ( a > a > $o ) > a ).
thf(sk113_decl,type,
sk113: ( a > a > $o ) > a ).
thf(sk114_decl,type,
sk114: ( a > a > $o ) > a ).
thf(sk117_decl,type,
sk117: ( a > a > $o ) > a ).
thf(sk118_decl,type,
sk118: ( a > a > $o ) > a ).
thf(sk119_decl,type,
sk119: ( a > a > $o ) > a ).
thf(sk120_decl,type,
sk120: ( a > a > $o ) > a ).
thf(sk121_decl,type,
sk121: a > a > $o ).
thf(sk122_decl,type,
sk122: a > a > $o ).
thf(sk123_decl,type,
sk123: a > a > $o ).
thf(sk124_decl,type,
sk124: a > a > $o ).
thf(sk129_decl,type,
sk129: a ).
thf(sk130_decl,type,
sk130: a ).
thf(sk131_decl,type,
sk131: a ).
thf(sk132_decl,type,
sk132: a ).
thf(sk133_decl,type,
sk133: ( a > a > $o ) > a ).
thf(sk134_decl,type,
sk134: ( a > a > $o ) > a ).
thf(sk135_decl,type,
sk135: ( a > a > $o ) > a ).
thf(sk136_decl,type,
sk136: ( a > a > $o ) > a ).
thf(sk139_decl,type,
sk139: a ).
thf(sk140_decl,type,
sk140: a ).
thf(sk141_decl,type,
sk141: a ).
thf(sk142_decl,type,
sk142: a ).
thf(sk143_decl,type,
sk143: a ).
thf(sk144_decl,type,
sk144: ( a > a > $o ) > a ).
thf(sk145_decl,type,
sk145: ( a > a > $o ) > a ).
thf(sk146_decl,type,
sk146: ( a > a > $o ) > a ).
thf(sk147_decl,type,
sk147: ( a > a > $o ) > a ).
thf(sk150_decl,type,
sk150: ( a > a > $o ) > a ).
thf(sk151_decl,type,
sk151: ( a > a > $o ) > a ).
thf(sk152_decl,type,
sk152: ( a > a > $o ) > a ).
thf(sk153_decl,type,
sk153: ( a > a > $o ) > a ).
thf(sk156_decl,type,
sk156: a > a > $o ).
thf(sk157_decl,type,
sk157: a > a > $o ).
thf(sk1_def,definition,
( sk1
= ( @+[A: ( a > a > $o ) > $o] :
~ ! [B: a > a > $o,C: a > a > $o] :
( ( ^ [D: a,E: a] :
! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( ( B @ G @ H )
| ( C @ G @ H ) )
=> ( F @ G @ H ) )
& ( A @ F ) )
=> ( F @ D @ E ) ) )
= ( ^ [D: a,E: a] :
! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( ! [I: a > a > $o] :
( ( ! [J: a,K: a] :
( ( B @ J @ K )
=> ( I @ J @ K ) )
& ( A @ I ) )
=> ( I @ G @ H ) )
| ! [I: a > a > $o] :
( ( ! [J: a,K: a] :
( ( C @ J @ K )
=> ( I @ J @ K ) )
& ( A @ I ) )
=> ( I @ G @ H ) ) )
=> ( F @ G @ H ) )
& ( A @ F ) )
=> ( F @ D @ E ) ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: a > a > $o] :
~ ! [B: a > a > $o] :
( ( ^ [C: a,D: a] :
! [E: a > a > $o] :
( ( ! [F: a,G: a] :
( ( ( A @ F @ G )
| ( B @ F @ G ) )
=> ( E @ F @ G ) )
& ( sk1 @ E ) )
=> ( E @ C @ D ) ) )
= ( ^ [C: a,D: a] :
! [E: a > a > $o] :
( ( ! [F: a,G: a] :
( ( ! [H: a > a > $o] :
( ( ! [I: a,J: a] :
( ( A @ I @ J )
=> ( H @ I @ J ) )
& ( sk1 @ H ) )
=> ( H @ F @ G ) )
| ! [H: a > a > $o] :
( ( ! [I: a,J: a] :
( ( B @ I @ J )
=> ( H @ I @ J ) )
& ( sk1 @ H ) )
=> ( H @ F @ G ) ) )
=> ( E @ F @ G ) )
& ( sk1 @ E ) )
=> ( E @ C @ D ) ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: a > a > $o] :
( ( ^ [B: a,C: a] :
! [D: a > a > $o] :
( ( ! [E: a,F: a] :
( ( ( sk2 @ E @ F )
| ( A @ E @ F ) )
=> ( D @ E @ F ) )
& ( sk1 @ D ) )
=> ( D @ B @ C ) ) )
!= ( ^ [B: a,C: a] :
! [D: a > a > $o] :
( ( ! [E: a,F: a] :
( ( ! [G: a > a > $o] :
( ( ! [H: a,I: a] :
( ( sk2 @ H @ I )
=> ( G @ H @ I ) )
& ( sk1 @ G ) )
=> ( G @ E @ F ) )
| ! [G: a > a > $o] :
( ( ! [H: a,I: a] :
( ( A @ H @ I )
=> ( G @ H @ I ) )
& ( sk1 @ G ) )
=> ( G @ E @ F ) ) )
=> ( D @ E @ F ) )
& ( sk1 @ D ) )
=> ( D @ B @ C ) ) ) ) ) ) ).
thf(sk39_def,definition,
( sk39
= ( @+[A: a > a > $o] :
~ ( ( ! [B: a,C: a] :
( ( sk2 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk32 @ sk33 ) ) ) ) ).
thf(sk40_def,definition,
( sk40
= ( ^ [A: a,B: a] :
@+[C: a > a > $o] :
~ ( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ sk37 @ sk38 ) ) ) ) ).
thf(sk51_def,definition,
( sk51
= ( @+[A: a > a > $o] :
~ ( ( ! [B: a,C: a] :
( ( ( sk2 @ B @ C )
| ( sk3 @ B @ C ) )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk4 @ sk5 ) ) ) ) ).
thf(sk52_def,definition,
( sk52
= ( ^ [A: a,B: a] :
@+[C: a > a > $o] :
~ ( ( ! [D: a,E: a] :
( ( ! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( sk2 @ G @ H )
=> ( F @ G @ H ) )
& ( sk1 @ F ) )
=> ( F @ D @ E ) )
| ! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( sk3 @ G @ H )
=> ( F @ G @ H ) )
& ( sk1 @ F ) )
=> ( F @ D @ E ) ) )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ sk4 @ sk5 ) ) ) ) ).
thf(sk53_def,definition,
( sk53
= ( ^ [A: a,B: a,C: a,D: a] :
@+[E: a > a > $o] :
~ ( ( ! [F: a,G: a] :
( ( sk2 @ F @ G )
=> ( E @ F @ G ) )
& ( sk1 @ E ) )
=> ( E @ B @ A ) ) ) ) ).
thf(sk54_def,definition,
( sk54
= ( ^ [A: a,B: a,C: a,D: a] :
@+[E: a > a > $o] :
~ ( ( ! [F: a,G: a] :
( ( sk3 @ F @ G )
=> ( E @ F @ G ) )
& ( sk1 @ E ) )
=> ( E @ B @ A ) ) ) ) ).
thf(sk63_def,definition,
( sk63
= ( @+[A: a] :
~ ! [B: a] :
( ( ( sk2 @ A @ B )
| ( sk3 @ A @ B ) )
=> ( sk14 @ A @ B ) ) ) ) ).
thf(sk64_def,definition,
( sk64
= ( @+[A: a] :
~ ( ( ( sk2 @ sk63 @ A )
| ( sk3 @ sk63 @ A ) )
=> ( sk14 @ sk63 @ A ) ) ) ) ).
thf(sk65_def,definition,
( sk65
= ( @+[A: a] :
~ ! [B: a] :
( ( ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) )
| ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) )
=> ( sk14 @ A @ B ) ) ) ) ).
thf(sk66_def,definition,
( sk66
= ( @+[A: a] :
~ ( ( ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk2 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk65 @ A ) )
| ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk3 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk65 @ A ) ) )
=> ( sk14 @ sk65 @ A ) ) ) ) ).
thf(sk67_def,definition,
( sk67
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ! [C: a] :
( ( sk2 @ B @ C )
=> ( A @ B @ C ) ) ) ) ).
thf(sk68_def,definition,
( sk68
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ( ( sk2 @ ( sk67 @ A ) @ B )
=> ( A @ ( sk67 @ A ) @ B ) ) ) ) ).
thf(sk69_def,definition,
( sk69
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ! [C: a] :
( ( sk3 @ B @ C )
=> ( A @ B @ C ) ) ) ) ).
thf(sk70_def,definition,
( sk70
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ( ( sk3 @ ( sk69 @ A ) @ B )
=> ( A @ ( sk69 @ A ) @ B ) ) ) ) ).
thf(sk73_def,definition,
( sk73
= ( ^ [A: a,B: a,C: a,D: a] :
@+[E: a > a > $o] :
~ ( ( ! [F: a,G: a] :
( ( sk2 @ F @ G )
=> ( E @ F @ G ) )
& ( sk1 @ E ) )
=> ( E @ B @ A ) ) ) ) ).
thf(sk74_def,definition,
( sk74
= ( ^ [A: a,B: a,C: a,D: a] :
@+[E: a > a > $o] :
~ ( ( ! [F: a,G: a] :
( ( sk3 @ F @ G )
=> ( E @ F @ G ) )
& ( sk1 @ E ) )
=> ( E @ B @ A ) ) ) ) ).
thf(sk83_def,definition,
( sk83
= ( @+[A: a > a > $o] :
~ ( ( ! [B: a,C: a] :
( ( sk2 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk27 @ sk28 ) ) ) ) ).
thf(sk84_def,definition,
( sk84
= ( @+[A: a > a > $o] :
~ ( ( ! [B: a,C: a] :
( ( sk3 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk27 @ sk28 ) ) ) ) ).
thf(sk89_def,definition,
( sk89
= ( @+[A: a] :
~ ( ( ( sk2 @ sk18 @ A )
| ( sk3 @ sk18 @ A ) )
=> ( sk17 @ sk18 @ A ) ) ) ) ).
thf(sk90_def,definition,
( sk90
= ( @+[A: a] :
~ ( ( ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk2 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk18 @ A ) )
| ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk3 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk18 @ A ) ) )
=> ( sk17 @ sk18 @ A ) ) ) ) ).
thf(sk91_def,definition,
( sk91
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ! [C: a] :
( ( sk2 @ B @ C )
=> ( A @ B @ C ) ) ) ) ).
thf(sk92_def,definition,
( sk92
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ( ( sk2 @ ( sk91 @ A ) @ B )
=> ( A @ ( sk91 @ A ) @ B ) ) ) ) ).
thf(sk93_def,definition,
( sk93
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ! [C: a] :
( ( sk3 @ B @ C )
=> ( A @ B @ C ) ) ) ) ).
thf(sk94_def,definition,
( sk94
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ( ( sk3 @ ( sk93 @ A ) @ B )
=> ( A @ ( sk93 @ A ) @ B ) ) ) ) ).
thf(sk95_def,definition,
( sk95
= ( ^ [A: a,B: a] :
@+[C: a > a > $o] :
~ ( ( ! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ sk18 @ A ) ) ) ) ).
thf(sk96_def,definition,
( sk96
= ( ^ [A: a,B: a] :
@+[C: a > a > $o] :
~ ( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ sk18 @ A ) ) ) ) ).
thf(sk97_def,definition,
( sk97
= ( @+[A: a] :
~ ! [B: a] :
( ( ( sk2 @ A @ B )
| ( sk3 @ A @ B ) )
=> ( sk11 @ A @ B ) ) ) ) ).
thf(sk98_def,definition,
( sk98
= ( @+[A: a] :
~ ( ( ( sk2 @ sk97 @ A )
| ( sk3 @ sk97 @ A ) )
=> ( sk11 @ sk97 @ A ) ) ) ) ).
thf(sk99_def,definition,
( sk99
= ( @+[A: a] :
~ ! [B: a] :
( ( ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) )
| ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) )
=> ( sk11 @ A @ B ) ) ) ) ).
thf(sk100_def,definition,
( sk100
= ( @+[A: a] :
~ ( ( ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk2 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk99 @ A ) )
| ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk3 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk99 @ A ) ) )
=> ( sk11 @ sk99 @ A ) ) ) ) ).
thf(sk101_def,definition,
( sk101
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ! [C: a] :
( ( sk2 @ B @ C )
=> ( A @ B @ C ) ) ) ) ).
thf(sk102_def,definition,
( sk102
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ( ( sk2 @ ( sk101 @ A ) @ B )
=> ( A @ ( sk101 @ A ) @ B ) ) ) ) ).
thf(sk103_def,definition,
( sk103
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ! [C: a] :
( ( sk3 @ B @ C )
=> ( A @ B @ C ) ) ) ) ).
thf(sk104_def,definition,
( sk104
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ( ( sk3 @ ( sk103 @ A ) @ B )
=> ( A @ ( sk103 @ A ) @ B ) ) ) ) ).
thf(sk105_def,definition,
( sk105
= ( ^ [A: a,B: a,C: a,D: a] :
@+[E: a > a > $o] :
~ ( ( ! [F: a,G: a] :
( ( sk2 @ F @ G )
=> ( E @ F @ G ) )
& ( sk1 @ E ) )
=> ( E @ B @ A ) ) ) ) ).
thf(sk106_def,definition,
( sk106
= ( ^ [A: a,B: a,C: a,D: a] :
@+[E: a > a > $o] :
~ ( ( ! [F: a,G: a] :
( ( sk3 @ F @ G )
=> ( E @ F @ G ) )
& ( sk1 @ E ) )
=> ( E @ B @ A ) ) ) ) ).
thf(sk107_def,definition,
( sk107
= ( @+[A: a] :
~ ! [B: a] :
( ( ( sk2 @ A @ B )
| ( sk3 @ A @ B ) )
=> ( sk11 @ A @ B ) ) ) ) ).
thf(sk108_def,definition,
( sk108
= ( @+[A: a] :
~ ( ( ( sk2 @ sk107 @ A )
| ( sk3 @ sk107 @ A ) )
=> ( sk11 @ sk107 @ A ) ) ) ) ).
thf(sk109_def,definition,
( sk109
= ( @+[A: a] :
~ ! [B: a] :
( ( ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) )
| ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) )
=> ( sk11 @ A @ B ) ) ) ) ).
thf(sk110_def,definition,
( sk110
= ( @+[A: a] :
~ ( ( ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk2 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk109 @ A ) )
| ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk3 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk109 @ A ) ) )
=> ( sk11 @ sk109 @ A ) ) ) ) ).
thf(sk111_def,definition,
( sk111
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ! [C: a] :
( ( sk2 @ B @ C )
=> ( A @ B @ C ) ) ) ) ).
thf(sk112_def,definition,
( sk112
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ( ( sk2 @ ( sk111 @ A ) @ B )
=> ( A @ ( sk111 @ A ) @ B ) ) ) ) ).
thf(sk113_def,definition,
( sk113
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ! [C: a] :
( ( sk3 @ B @ C )
=> ( A @ B @ C ) ) ) ) ).
thf(sk114_def,definition,
( sk114
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ( ( sk3 @ ( sk113 @ A ) @ B )
=> ( A @ ( sk113 @ A ) @ B ) ) ) ) ).
thf(sk117_def,definition,
( sk117
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ! [C: a] :
( ( sk2 @ B @ C )
=> ( A @ B @ C ) ) ) ) ).
thf(sk118_def,definition,
( sk118
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ( ( sk2 @ ( sk117 @ A ) @ B )
=> ( A @ ( sk117 @ A ) @ B ) ) ) ) ).
thf(sk119_def,definition,
( sk119
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ! [C: a] :
( ( sk3 @ B @ C )
=> ( A @ B @ C ) ) ) ) ).
thf(sk120_def,definition,
( sk120
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ( ( sk3 @ ( sk119 @ A ) @ B )
=> ( A @ ( sk119 @ A ) @ B ) ) ) ) ).
thf(sk121_def,definition,
( sk121
= ( @+[A: a > a > $o] :
~ ( ( ! [B: a,C: a] :
( ( sk2 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk22 @ sk23 ) ) ) ) ).
thf(sk122_def,definition,
( sk122
= ( @+[A: a > a > $o] :
~ ( ( ! [B: a,C: a] :
( ( sk3 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk22 @ sk23 ) ) ) ) ).
thf(sk123_def,definition,
( sk123
= ( @+[A: a > a > $o] :
~ ( ( ! [B: a,C: a] :
( ( sk2 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk22 @ sk23 ) ) ) ) ).
thf(sk124_def,definition,
( sk124
= ( @+[A: a > a > $o] :
~ ( ( ! [B: a,C: a] :
( ( sk3 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk22 @ sk23 ) ) ) ) ).
thf(sk129_def,definition,
( sk129
= ( @+[A: a] :
~ ! [B: a] :
( ( ( sk2 @ A @ B )
| ( sk3 @ A @ B ) )
=> ( sk8 @ A @ B ) ) ) ) ).
thf(sk130_def,definition,
( sk130
= ( @+[A: a] :
~ ( ( ( sk2 @ sk129 @ A )
| ( sk3 @ sk129 @ A ) )
=> ( sk8 @ sk129 @ A ) ) ) ) ).
thf(sk131_def,definition,
( sk131
= ( @+[A: a] :
~ ! [B: a] :
( ( ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) )
| ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) )
=> ( sk8 @ A @ B ) ) ) ) ).
thf(sk132_def,definition,
( sk132
= ( @+[A: a] :
~ ( ( ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk2 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk131 @ A ) )
| ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk3 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk131 @ A ) ) )
=> ( sk8 @ sk131 @ A ) ) ) ) ).
thf(sk133_def,definition,
( sk133
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ! [C: a] :
( ( sk2 @ B @ C )
=> ( A @ B @ C ) ) ) ) ).
thf(sk134_def,definition,
( sk134
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ( ( sk2 @ ( sk133 @ A ) @ B )
=> ( A @ ( sk133 @ A ) @ B ) ) ) ) ).
thf(sk135_def,definition,
( sk135
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ! [C: a] :
( ( sk3 @ B @ C )
=> ( A @ B @ C ) ) ) ) ).
thf(sk136_def,definition,
( sk136
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ( ( sk3 @ ( sk135 @ A ) @ B )
=> ( A @ ( sk135 @ A ) @ B ) ) ) ) ).
thf(sk142_def,definition,
( sk142
= ( @+[A: a] :
~ ( ( ( sk2 @ sk139 @ A )
| ( sk3 @ sk139 @ A ) )
=> ( sk8 @ sk139 @ A ) ) ) ) ).
thf(sk143_def,definition,
( sk143
= ( @+[A: a] :
~ ( ( ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk2 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk139 @ A ) )
| ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk3 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk139 @ A ) ) )
=> ( sk8 @ sk139 @ A ) ) ) ) ).
thf(sk144_def,definition,
( sk144
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ! [C: a] :
( ( sk2 @ B @ C )
=> ( A @ B @ C ) ) ) ) ).
thf(sk145_def,definition,
( sk145
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ( ( sk2 @ ( sk144 @ A ) @ B )
=> ( A @ ( sk144 @ A ) @ B ) ) ) ) ).
thf(sk146_def,definition,
( sk146
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ! [C: a] :
( ( sk3 @ B @ C )
=> ( A @ B @ C ) ) ) ) ).
thf(sk147_def,definition,
( sk147
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ( ( sk3 @ ( sk146 @ A ) @ B )
=> ( A @ ( sk146 @ A ) @ B ) ) ) ) ).
thf(sk150_def,definition,
( sk150
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ! [C: a] :
( ( sk2 @ B @ C )
=> ( A @ B @ C ) ) ) ) ).
thf(sk151_def,definition,
( sk151
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ( ( sk2 @ ( sk150 @ A ) @ B )
=> ( A @ ( sk150 @ A ) @ B ) ) ) ) ).
thf(sk152_def,definition,
( sk152
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ! [C: a] :
( ( sk3 @ B @ C )
=> ( A @ B @ C ) ) ) ) ).
thf(sk153_def,definition,
( sk153
= ( ^ [A: a > a > $o] :
@+[B: a] :
~ ( ( sk3 @ ( sk152 @ A ) @ B )
=> ( A @ ( sk152 @ A ) @ B ) ) ) ) ).
thf(sk156_def,definition,
( sk156
= ( @+[A: a > a > $o] :
~ ( ( ! [B: a,C: a] :
( ( sk2 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk140 @ sk141 ) ) ) ) ).
thf(sk157_def,definition,
( sk157
= ( @+[A: a > a > $o] :
~ ( ( ! [B: a,C: a] :
( ( sk3 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk140 @ sk141 ) ) ) ) ).
thf(1,conjecture,
! [A: ( a > a > $o ) > $o,B: a > a > $o,C: a > a > $o] :
( ( ^ [D: a,E: a] :
! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( ( B @ G @ H )
| ( C @ G @ H ) )
=> ( F @ G @ H ) )
& ( A @ F ) )
=> ( F @ D @ E ) ) )
= ( ^ [D: a,E: a] :
! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( ! [I: a > a > $o] :
( ( ! [J: a,K: a] :
( ( B @ J @ K )
=> ( I @ J @ K ) )
& ( A @ I ) )
=> ( I @ G @ H ) )
| ! [I: a > a > $o] :
( ( ! [J: a,K: a] :
( ( C @ J @ K )
=> ( I @ J @ K ) )
& ( A @ I ) )
=> ( I @ G @ H ) ) )
=> ( F @ G @ H ) )
& ( A @ F ) )
=> ( F @ D @ E ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cTHM252_pme) ).
thf(2,negated_conjecture,
~ ! [A: ( a > a > $o ) > $o,B: a > a > $o,C: a > a > $o] :
( ( ^ [D: a,E: a] :
! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( ( B @ G @ H )
| ( C @ G @ H ) )
=> ( F @ G @ H ) )
& ( A @ F ) )
=> ( F @ D @ E ) ) )
= ( ^ [D: a,E: a] :
! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( ! [I: a > a > $o] :
( ( ! [J: a,K: a] :
( ( B @ J @ K )
=> ( I @ J @ K ) )
& ( A @ I ) )
=> ( I @ G @ H ) )
| ! [I: a > a > $o] :
( ( ! [J: a,K: a] :
( ( C @ J @ K )
=> ( I @ J @ K ) )
& ( A @ I ) )
=> ( I @ G @ H ) ) )
=> ( F @ G @ H ) )
& ( A @ F ) )
=> ( F @ D @ E ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(3,plain,
~ ! [A: ( a > a > $o ) > $o,B: a > a > $o,C: a > a > $o] :
( ( ^ [D: a,E: a] :
! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( ( B @ G @ H )
| ( C @ G @ H ) )
=> ( F @ G @ H ) )
& ( A @ F ) )
=> ( F @ D @ E ) ) )
= ( ^ [D: a,E: a] :
! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( ! [I: a > a > $o] :
( ( ! [J: a,K: a] :
( ( B @ J @ K )
=> ( I @ J @ K ) )
& ( A @ I ) )
=> ( I @ G @ H ) )
| ! [I: a > a > $o] :
( ( ! [J: a,K: a] :
( ( C @ J @ K )
=> ( I @ J @ K ) )
& ( A @ I ) )
=> ( I @ G @ H ) ) )
=> ( F @ G @ H ) )
& ( A @ F ) )
=> ( F @ D @ E ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(4,plain,
( ( ^ [A: a,B: a] :
! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( ( sk2 @ D @ E )
| ( sk3 @ D @ E ) )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) )
!= ( ^ [A: a,B: a] :
! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( ! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( sk2 @ G @ H )
=> ( F @ G @ H ) )
& ( sk1 @ F ) )
=> ( F @ D @ E ) )
| ! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( sk3 @ G @ H )
=> ( F @ G @ H ) )
& ( sk1 @ F ) )
=> ( F @ D @ E ) ) )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) ) ),
inference(cnf,[status(esa)],[3]) ).
thf(5,plain,
( ( ^ [A: a,B: a] :
! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( ( sk2 @ D @ E )
| ( sk3 @ D @ E ) )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) )
!= ( ^ [A: a,B: a] :
! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( ! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( sk2 @ G @ H )
=> ( F @ G @ H ) )
& ( sk1 @ F ) )
=> ( F @ D @ E ) )
| ! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( sk3 @ G @ H )
=> ( F @ G @ H ) )
& ( sk1 @ F ) )
=> ( F @ D @ E ) ) )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) ) ),
inference(lifteq,[status(thm)],[4]) ).
thf(6,plain,
( ( ^ [A: a,B: a,C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( ( sk2 @ D @ E )
| ( sk3 @ D @ E ) )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) )
!= ( ^ [A: a,B: a,C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( ! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( sk2 @ G @ H )
=> ( F @ G @ H ) )
& ( sk1 @ F ) )
=> ( F @ D @ E ) )
| ! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( sk3 @ G @ H )
=> ( F @ G @ H ) )
& ( sk1 @ F ) )
=> ( F @ D @ E ) ) )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) ) ),
inference(simp,[status(thm)],[5]) ).
thf(9,plain,
( ( ( ! [A: a,B: a] :
( ( ( sk2 @ A @ B )
| ( sk3 @ A @ B ) )
=> ( sk8 @ A @ B ) )
& ( sk1 @ sk8 ) )
=> ( sk8 @ sk6 @ sk7 ) )
!= ( ( ! [A: a,B: a] :
( ( ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) )
| ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) )
=> ( sk8 @ A @ B ) )
& ( sk1 @ sk8 ) )
=> ( sk8 @ sk6 @ sk7 ) ) ),
inference(func_ext,[status(esa)],[6]) ).
thf(147,plain,
( ( ( ! [A: a,B: a] :
( ( ( sk2 @ A @ B )
| ( sk3 @ A @ B ) )
=> ( sk8 @ A @ B ) )
& ( sk1 @ sk8 ) )
!= ( ! [A: a,B: a] :
( ( ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) )
| ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) )
=> ( sk8 @ A @ B ) )
& ( sk1 @ sk8 ) ) )
| ( ( sk8 @ sk6 @ sk7 )
!= ( sk8 @ sk6 @ sk7 ) ) ),
inference(simp,[status(thm)],[9]) ).
thf(177,plain,
( ( ! [A: a,B: a] :
( ( ( sk2 @ A @ B )
| ( sk3 @ A @ B ) )
=> ( sk8 @ A @ B ) )
& ( sk1 @ sk8 ) )
!= ( ! [A: a,B: a] :
( ( ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) )
| ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) )
=> ( sk8 @ A @ B ) )
& ( sk1 @ sk8 ) ) ),
inference(simp,[status(thm)],[147]) ).
thf(148,plain,
( ~ ( ( ! [A: a,B: a] :
( ( ( sk2 @ A @ B )
| ( sk3 @ A @ B ) )
=> ( sk8 @ A @ B ) )
& ( sk1 @ sk8 ) )
=> ( sk8 @ sk6 @ sk7 ) )
| ~ ( ( ! [A: a,B: a] :
( ( ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) )
| ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) )
=> ( sk8 @ A @ B ) )
& ( sk1 @ sk8 ) )
=> ( sk8 @ sk6 @ sk7 ) ) ),
inference(bool_ext,[status(thm)],[9]) ).
thf(178,plain,
! [H: a,G: a,F: a,E: a,D: a,C: a,B: a,A: a] :
( ( ~ ( sk2 @ A @ B )
| ( sk8 @ A @ B )
| ~ ( sk2 @ E @ F )
| ( sk73 @ D @ C @ B @ A @ E @ F )
| ( sk8 @ C @ D ) )
& ( ~ ( sk2 @ A @ B )
| ( sk8 @ A @ B )
| ( sk1 @ ( sk73 @ D @ C @ B @ A ) )
| ( sk8 @ C @ D ) )
& ( ~ ( sk2 @ A @ B )
| ( sk8 @ A @ B )
| ~ ( sk73 @ D @ C @ B @ A @ C @ D )
| ( sk8 @ C @ D ) )
& ( ~ ( sk2 @ A @ B )
| ( sk8 @ A @ B )
| ~ ( sk3 @ G @ H )
| ( sk74 @ D @ C @ B @ A @ G @ H )
| ( sk8 @ C @ D ) )
& ( ~ ( sk2 @ A @ B )
| ( sk8 @ A @ B )
| ( sk1 @ ( sk74 @ D @ C @ B @ A ) )
| ( sk8 @ C @ D ) )
& ( ~ ( sk2 @ A @ B )
| ( sk8 @ A @ B )
| ~ ( sk74 @ D @ C @ B @ A @ C @ D )
| ( sk8 @ C @ D ) )
& ( ~ ( sk2 @ A @ B )
| ( sk8 @ A @ B )
| ( sk1 @ sk8 ) )
& ( ~ ( sk2 @ A @ B )
| ( sk8 @ A @ B )
| ~ ( sk8 @ sk6 @ sk7 ) )
& ( ~ ( sk3 @ A @ B )
| ( sk8 @ A @ B )
| ~ ( sk2 @ E @ F )
| ( sk73 @ D @ C @ B @ A @ E @ F )
| ( sk8 @ C @ D ) )
& ( ~ ( sk3 @ A @ B )
| ( sk8 @ A @ B )
| ( sk1 @ ( sk73 @ D @ C @ B @ A ) )
| ( sk8 @ C @ D ) )
& ( ~ ( sk3 @ A @ B )
| ( sk8 @ A @ B )
| ~ ( sk73 @ D @ C @ B @ A @ C @ D )
| ( sk8 @ C @ D ) )
& ( ~ ( sk3 @ A @ B )
| ( sk8 @ A @ B )
| ~ ( sk3 @ G @ H )
| ( sk74 @ D @ C @ B @ A @ G @ H )
| ( sk8 @ C @ D ) )
& ( ~ ( sk3 @ A @ B )
| ( sk8 @ A @ B )
| ( sk1 @ ( sk74 @ D @ C @ B @ A ) )
| ( sk8 @ C @ D ) )
& ( ~ ( sk3 @ A @ B )
| ( sk8 @ A @ B )
| ~ ( sk74 @ D @ C @ B @ A @ C @ D )
| ( sk8 @ C @ D ) )
& ( ~ ( sk3 @ A @ B )
| ( sk8 @ A @ B )
| ( sk1 @ sk8 ) )
& ( ~ ( sk3 @ A @ B )
| ( sk8 @ A @ B )
| ~ ( sk8 @ sk6 @ sk7 ) )
& ( ( sk1 @ sk8 )
| ~ ( sk2 @ E @ F )
| ( sk73 @ D @ C @ B @ A @ E @ F )
| ( sk8 @ C @ D ) )
& ( ( sk1 @ sk8 )
| ( sk1 @ ( sk73 @ D @ C @ B @ A ) )
| ( sk8 @ C @ D ) )
& ( ( sk1 @ sk8 )
| ~ ( sk73 @ D @ C @ B @ A @ C @ D )
| ( sk8 @ C @ D ) )
& ( ( sk1 @ sk8 )
| ~ ( sk3 @ G @ H )
| ( sk74 @ D @ C @ B @ A @ G @ H )
| ( sk8 @ C @ D ) )
& ( ( sk1 @ sk8 )
| ( sk1 @ ( sk74 @ D @ C @ B @ A ) )
| ( sk8 @ C @ D ) )
& ( ( sk1 @ sk8 )
| ~ ( sk74 @ D @ C @ B @ A @ C @ D )
| ( sk8 @ C @ D ) )
& ( ( sk1 @ sk8 )
| ( sk1 @ sk8 ) )
& ( ( sk1 @ sk8 )
| ~ ( sk8 @ sk6 @ sk7 ) )
& ( ~ ( sk8 @ sk6 @ sk7 )
| ~ ( sk2 @ E @ F )
| ( sk73 @ D @ C @ B @ A @ E @ F )
| ( sk8 @ C @ D ) )
& ( ~ ( sk8 @ sk6 @ sk7 )
| ( sk1 @ ( sk73 @ D @ C @ B @ A ) )
| ( sk8 @ C @ D ) )
& ( ~ ( sk8 @ sk6 @ sk7 )
| ~ ( sk73 @ D @ C @ B @ A @ C @ D )
| ( sk8 @ C @ D ) )
& ( ~ ( sk8 @ sk6 @ sk7 )
| ~ ( sk3 @ G @ H )
| ( sk74 @ D @ C @ B @ A @ G @ H )
| ( sk8 @ C @ D ) )
& ( ~ ( sk8 @ sk6 @ sk7 )
| ( sk1 @ ( sk74 @ D @ C @ B @ A ) )
| ( sk8 @ C @ D ) )
& ( ~ ( sk8 @ sk6 @ sk7 )
| ~ ( sk74 @ D @ C @ B @ A @ C @ D )
| ( sk8 @ C @ D ) )
& ( ~ ( sk8 @ sk6 @ sk7 )
| ( sk1 @ sk8 ) )
& ( ~ ( sk8 @ sk6 @ sk7 )
| ~ ( sk8 @ sk6 @ sk7 ) ) ),
inference(cnf,[status(esa)],[148]) ).
thf(209,plain,
( ( sk1 @ sk8 )
| ( sk1 @ sk8 ) ),
inference(cnfConj,[status(thm)],[178]) ).
thf(213,plain,
sk1 @ sk8,
inference(simp,[status(thm)],[209]) ).
thf(478,plain,
( ( ! [A: a,B: a] :
( ( ( sk2 @ A @ B )
| ( sk3 @ A @ B ) )
=> ( sk8 @ A @ B ) )
& $true )
!= ( ! [A: a,B: a] :
( ( ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) )
| ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) )
=> ( sk8 @ A @ B ) )
& $true ) ),
inference(rewrite,[status(thm)],[177,213]) ).
thf(479,plain,
( ( ! [A: a,B: a] :
( ( ( sk2 @ A @ B )
| ( sk3 @ A @ B ) )
=> ( sk8 @ A @ B ) ) )
!= ( ! [A: a,B: a] :
( ( ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) )
| ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) )
=> ( sk8 @ A @ B ) ) ) ),
inference(simp,[status(thm)],[478]) ).
thf(480,plain,
( ( ^ [A: a] :
! [B: a] :
( ( ( sk2 @ A @ B )
| ( sk3 @ A @ B ) )
=> ( sk8 @ A @ B ) ) )
!= ( ^ [A: a] :
! [B: a] :
( ( ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) )
| ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) )
=> ( sk8 @ A @ B ) ) ) ),
inference(simp,[status(thm)],[479]) ).
thf(509,plain,
( ( ^ [A: a,B: a] :
( ( ( sk2 @ A @ B )
| ( sk3 @ A @ B ) )
=> ( sk8 @ A @ B ) ) )
!= ( ^ [A: a,B: a] :
( ( ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) )
| ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) )
=> ( sk8 @ A @ B ) ) ) ),
inference(simp,[status(thm)],[480]) ).
thf(519,plain,
( ( ( ( sk2 @ sk140 @ sk141 )
| ( sk3 @ sk140 @ sk141 ) )
=> ( sk8 @ sk140 @ sk141 ) )
!= ( ( ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk2 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk140 @ sk141 ) )
| ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk3 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk140 @ sk141 ) ) )
=> ( sk8 @ sk140 @ sk141 ) ) ),
inference(func_ext,[status(esa)],[509]) ).
thf(581,plain,
( ( ( ( sk2 @ sk140 @ sk141 )
| ( sk3 @ sk140 @ sk141 ) )
!= ( ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk2 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk140 @ sk141 ) )
| ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk3 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk140 @ sk141 ) ) ) )
| ( ( sk8 @ sk140 @ sk141 )
!= ( sk8 @ sk140 @ sk141 ) ) ),
inference(simp,[status(thm)],[519]) ).
thf(584,plain,
( ( ( sk2 @ sk140 @ sk141 )
| ( sk3 @ sk140 @ sk141 ) )
!= ( ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk2 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk140 @ sk141 ) )
| ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk3 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk140 @ sk141 ) ) ) ),
inference(simp,[status(thm)],[581]) ).
thf(658,plain,
( ~ ( ( sk2 @ sk140 @ sk141 )
| ( sk3 @ sk140 @ sk141 ) )
| ~ ( ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk2 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk140 @ sk141 ) )
| ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk3 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk140 @ sk141 ) ) ) ),
inference(bool_ext,[status(thm)],[584]) ).
thf(660,plain,
! [D: a,C: a,B: a,A: a] :
( ( ~ ( sk2 @ sk140 @ sk141 )
| ~ ( sk2 @ A @ B )
| ( sk156 @ A @ B ) )
& ( ~ ( sk2 @ sk140 @ sk141 )
| ( sk1 @ sk156 ) )
& ( ~ ( sk2 @ sk140 @ sk141 )
| ~ ( sk156 @ sk140 @ sk141 ) )
& ( ~ ( sk2 @ sk140 @ sk141 )
| ~ ( sk3 @ C @ D )
| ( sk157 @ C @ D ) )
& ( ~ ( sk2 @ sk140 @ sk141 )
| ( sk1 @ sk157 ) )
& ( ~ ( sk2 @ sk140 @ sk141 )
| ~ ( sk157 @ sk140 @ sk141 ) )
& ( ~ ( sk3 @ sk140 @ sk141 )
| ~ ( sk2 @ A @ B )
| ( sk156 @ A @ B ) )
& ( ~ ( sk3 @ sk140 @ sk141 )
| ( sk1 @ sk156 ) )
& ( ~ ( sk3 @ sk140 @ sk141 )
| ~ ( sk156 @ sk140 @ sk141 ) )
& ( ~ ( sk3 @ sk140 @ sk141 )
| ~ ( sk3 @ C @ D )
| ( sk157 @ C @ D ) )
& ( ~ ( sk3 @ sk140 @ sk141 )
| ( sk1 @ sk157 ) )
& ( ~ ( sk3 @ sk140 @ sk141 )
| ~ ( sk157 @ sk140 @ sk141 ) ) ),
inference(cnf,[status(esa)],[658]) ).
thf(662,plain,
( ~ ( sk3 @ sk140 @ sk141 )
| ~ ( sk156 @ sk140 @ sk141 ) ),
inference(cnfConj,[status(thm)],[660]) ).
thf(8,plain,
( ( ( ^ [A: a,B: a,C: a > a > $o] :
( ! [D: a,E: a] :
( ( ( sk2 @ D @ E )
| ( sk3 @ D @ E ) )
=> ( C @ D @ E ) )
& ( sk1 @ C ) ) )
!= ( ^ [A: a,B: a,C: a > a > $o] :
( ! [D: a,E: a] :
( ( ! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( sk2 @ G @ H )
=> ( F @ G @ H ) )
& ( sk1 @ F ) )
=> ( F @ D @ E ) )
| ! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( sk3 @ G @ H )
=> ( F @ G @ H ) )
& ( sk1 @ F ) )
=> ( F @ D @ E ) ) )
=> ( C @ D @ E ) )
& ( sk1 @ C ) ) ) )
| ( ( ^ [A: a,B: a,C: a > a > $o] : ( C @ A @ B ) )
!= ( ^ [A: a,B: a,C: a > a > $o] : ( C @ A @ B ) ) ) ),
inference(simp,[status(thm)],[6]) ).
thf(10,plain,
( ( ^ [A: a,B: a,C: a > a > $o] :
( ! [D: a,E: a] :
( ( ( sk2 @ D @ E )
| ( sk3 @ D @ E ) )
=> ( C @ D @ E ) )
& ( sk1 @ C ) ) )
!= ( ^ [A: a,B: a,C: a > a > $o] :
( ! [D: a,E: a] :
( ( ! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( sk2 @ G @ H )
=> ( F @ G @ H ) )
& ( sk1 @ F ) )
=> ( F @ D @ E ) )
| ! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( sk3 @ G @ H )
=> ( F @ G @ H ) )
& ( sk1 @ F ) )
=> ( F @ D @ E ) ) )
=> ( C @ D @ E ) )
& ( sk1 @ C ) ) ) ),
inference(simp,[status(thm)],[8]) ).
thf(11,plain,
( ( ( ^ [A: a,B: a,C: a > a > $o] :
! [D: a,E: a] :
( ( ( sk2 @ D @ E )
| ( sk3 @ D @ E ) )
=> ( C @ D @ E ) ) )
!= ( ^ [A: a,B: a,C: a > a > $o] :
! [D: a,E: a] :
( ( ! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( sk2 @ G @ H )
=> ( F @ G @ H ) )
& ( sk1 @ F ) )
=> ( F @ D @ E ) )
| ! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( sk3 @ G @ H )
=> ( F @ G @ H ) )
& ( sk1 @ F ) )
=> ( F @ D @ E ) ) )
=> ( C @ D @ E ) ) ) )
| ( ( ^ [A: a,B: a] : sk1 )
!= ( ^ [A: a,B: a] : sk1 ) ) ),
inference(simp,[status(thm)],[10]) ).
thf(13,plain,
( ( ^ [A: a,B: a,C: a > a > $o] :
! [D: a,E: a] :
( ( ( sk2 @ D @ E )
| ( sk3 @ D @ E ) )
=> ( C @ D @ E ) ) )
!= ( ^ [A: a,B: a,C: a > a > $o] :
! [D: a,E: a] :
( ( ! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( sk2 @ G @ H )
=> ( F @ G @ H ) )
& ( sk1 @ F ) )
=> ( F @ D @ E ) )
| ! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( sk3 @ G @ H )
=> ( F @ G @ H ) )
& ( sk1 @ F ) )
=> ( F @ D @ E ) ) )
=> ( C @ D @ E ) ) ) ),
inference(simp,[status(thm)],[11]) ).
thf(14,plain,
( ( ^ [A: a,B: a,C: a > a > $o,D: a] :
! [E: a] :
( ( ( sk2 @ D @ E )
| ( sk3 @ D @ E ) )
=> ( C @ D @ E ) ) )
!= ( ^ [A: a,B: a,C: a > a > $o,D: a] :
! [E: a] :
( ( ! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( sk2 @ G @ H )
=> ( F @ G @ H ) )
& ( sk1 @ F ) )
=> ( F @ D @ E ) )
| ! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( sk3 @ G @ H )
=> ( F @ G @ H ) )
& ( sk1 @ F ) )
=> ( F @ D @ E ) ) )
=> ( C @ D @ E ) ) ) ),
inference(simp,[status(thm)],[13]) ).
thf(16,plain,
( ( ^ [A: a,B: a,C: a > a > $o,D: a,E: a] :
( ( ( sk2 @ D @ E )
| ( sk3 @ D @ E ) )
=> ( C @ D @ E ) ) )
!= ( ^ [A: a,B: a,C: a > a > $o,D: a,E: a] :
( ( ! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( sk2 @ G @ H )
=> ( F @ G @ H ) )
& ( sk1 @ F ) )
=> ( F @ D @ E ) )
| ! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( sk3 @ G @ H )
=> ( F @ G @ H ) )
& ( sk1 @ F ) )
=> ( F @ D @ E ) ) )
=> ( C @ D @ E ) ) ) ),
inference(simp,[status(thm)],[14]) ).
thf(18,plain,
( ( ( ^ [A: a,B: a,C: a > a > $o,D: a,E: a] :
( ( sk2 @ D @ E )
| ( sk3 @ D @ E ) ) )
!= ( ^ [A: a,B: a,C: a > a > $o,D: a,E: a] :
( ! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( sk2 @ G @ H )
=> ( F @ G @ H ) )
& ( sk1 @ F ) )
=> ( F @ D @ E ) )
| ! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( sk3 @ G @ H )
=> ( F @ G @ H ) )
& ( sk1 @ F ) )
=> ( F @ D @ E ) ) ) ) )
| ( ( ^ [A: a,B: a,C: a > a > $o] : C )
!= ( ^ [A: a,B: a,C: a > a > $o] : C ) ) ),
inference(simp,[status(thm)],[16]) ).
thf(20,plain,
( ( ^ [A: a,B: a,C: a > a > $o,D: a,E: a] :
( ( sk2 @ D @ E )
| ( sk3 @ D @ E ) ) )
!= ( ^ [A: a,B: a,C: a > a > $o,D: a,E: a] :
( ! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( sk2 @ G @ H )
=> ( F @ G @ H ) )
& ( sk1 @ F ) )
=> ( F @ D @ E ) )
| ! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( sk3 @ G @ H )
=> ( F @ G @ H ) )
& ( sk1 @ F ) )
=> ( F @ D @ E ) ) ) ) ),
inference(simp,[status(thm)],[18]) ).
thf(22,plain,
( ( ( sk2 @ sk27 @ sk28 )
| ( sk3 @ sk27 @ sk28 ) )
!= ( ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk2 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk27 @ sk28 ) )
| ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk3 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk27 @ sk28 ) ) ) ),
inference(func_ext,[status(esa)],[20]) ).
thf(241,plain,
( ~ ( ( sk2 @ sk27 @ sk28 )
| ( sk3 @ sk27 @ sk28 ) )
| ~ ( ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk2 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk27 @ sk28 ) )
| ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk3 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk27 @ sk28 ) ) ) ),
inference(bool_ext,[status(thm)],[22]) ).
thf(243,plain,
! [D: a,C: a,B: a,A: a] :
( ( ~ ( sk2 @ sk27 @ sk28 )
| ~ ( sk2 @ A @ B )
| ( sk83 @ A @ B ) )
& ( ~ ( sk2 @ sk27 @ sk28 )
| ( sk1 @ sk83 ) )
& ( ~ ( sk2 @ sk27 @ sk28 )
| ~ ( sk83 @ sk27 @ sk28 ) )
& ( ~ ( sk2 @ sk27 @ sk28 )
| ~ ( sk3 @ C @ D )
| ( sk84 @ C @ D ) )
& ( ~ ( sk2 @ sk27 @ sk28 )
| ( sk1 @ sk84 ) )
& ( ~ ( sk2 @ sk27 @ sk28 )
| ~ ( sk84 @ sk27 @ sk28 ) )
& ( ~ ( sk3 @ sk27 @ sk28 )
| ~ ( sk2 @ A @ B )
| ( sk83 @ A @ B ) )
& ( ~ ( sk3 @ sk27 @ sk28 )
| ( sk1 @ sk83 ) )
& ( ~ ( sk3 @ sk27 @ sk28 )
| ~ ( sk83 @ sk27 @ sk28 ) )
& ( ~ ( sk3 @ sk27 @ sk28 )
| ~ ( sk3 @ C @ D )
| ( sk84 @ C @ D ) )
& ( ~ ( sk3 @ sk27 @ sk28 )
| ( sk1 @ sk84 ) )
& ( ~ ( sk3 @ sk27 @ sk28 )
| ~ ( sk84 @ sk27 @ sk28 ) ) ),
inference(cnf,[status(esa)],[241]) ).
thf(249,plain,
( ~ ( sk3 @ sk27 @ sk28 )
| ~ ( sk83 @ sk27 @ sk28 ) ),
inference(cnfConj,[status(thm)],[243]) ).
thf(666,plain,
( ~ ( sk3 @ sk140 @ sk141 )
| ~ ( sk157 @ sk140 @ sk141 ) ),
inference(cnfConj,[status(thm)],[660]) ).
thf(247,plain,
( ~ ( sk2 @ sk27 @ sk28 )
| ( sk1 @ sk84 ) ),
inference(cnfConj,[status(thm)],[243]) ).
thf(12,plain,
( ( ! [A: a,B: a] :
( ( ( sk2 @ A @ B )
| ( sk3 @ A @ B ) )
=> ( sk11 @ A @ B ) )
& ( sk1 @ sk11 ) )
!= ( ! [A: a,B: a] :
( ( ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) )
| ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) )
=> ( sk11 @ A @ B ) )
& ( sk1 @ sk11 ) ) ),
inference(func_ext,[status(esa)],[10]) ).
thf(294,plain,
( ( ( ! [A: a,B: a] :
( ( ( sk2 @ A @ B )
| ( sk3 @ A @ B ) )
=> ( sk11 @ A @ B ) ) )
!= ( ! [A: a,B: a] :
( ( ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) )
| ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) )
=> ( sk11 @ A @ B ) ) ) )
| ( ( sk1 @ sk11 )
!= ( sk1 @ sk11 ) ) ),
inference(simp,[status(thm)],[12]) ).
thf(321,plain,
( ( ! [A: a,B: a] :
( ( ( sk2 @ A @ B )
| ( sk3 @ A @ B ) )
=> ( sk11 @ A @ B ) ) )
!= ( ! [A: a,B: a] :
( ( ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) )
| ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) )
=> ( sk11 @ A @ B ) ) ) ),
inference(simp,[status(thm)],[294]) ).
thf(372,plain,
( ~ ! [A: a,B: a] :
( ( ( sk2 @ A @ B )
| ( sk3 @ A @ B ) )
=> ( sk11 @ A @ B ) )
| ~ ! [A: a,B: a] :
( ( ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) )
| ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) )
=> ( sk11 @ A @ B ) ) ),
inference(bool_ext,[status(thm)],[321]) ).
thf(374,plain,
! [B: a > a > $o,A: a > a > $o] :
( ( ( sk2 @ sk107 @ sk108 )
| ( sk3 @ sk107 @ sk108 )
| ( sk2 @ ( sk111 @ A ) @ ( sk112 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk109 @ sk110 )
| ( sk3 @ ( sk113 @ B ) @ ( sk114 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk109 @ sk110 ) )
& ( ( sk2 @ sk107 @ sk108 )
| ( sk3 @ sk107 @ sk108 )
| ( sk2 @ ( sk111 @ A ) @ ( sk112 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk109 @ sk110 )
| ~ ( B @ ( sk113 @ B ) @ ( sk114 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk109 @ sk110 ) )
& ( ( sk2 @ sk107 @ sk108 )
| ( sk3 @ sk107 @ sk108 )
| ~ ( A @ ( sk111 @ A ) @ ( sk112 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk109 @ sk110 )
| ( sk3 @ ( sk113 @ B ) @ ( sk114 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk109 @ sk110 ) )
& ( ( sk2 @ sk107 @ sk108 )
| ( sk3 @ sk107 @ sk108 )
| ~ ( A @ ( sk111 @ A ) @ ( sk112 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk109 @ sk110 )
| ~ ( B @ ( sk113 @ B ) @ ( sk114 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk109 @ sk110 ) )
& ( ( sk2 @ sk107 @ sk108 )
| ( sk3 @ sk107 @ sk108 )
| ~ ( sk11 @ sk109 @ sk110 ) )
& ( ~ ( sk11 @ sk107 @ sk108 )
| ( sk2 @ ( sk111 @ A ) @ ( sk112 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk109 @ sk110 )
| ( sk3 @ ( sk113 @ B ) @ ( sk114 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk109 @ sk110 ) )
& ( ~ ( sk11 @ sk107 @ sk108 )
| ( sk2 @ ( sk111 @ A ) @ ( sk112 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk109 @ sk110 )
| ~ ( B @ ( sk113 @ B ) @ ( sk114 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk109 @ sk110 ) )
& ( ~ ( sk11 @ sk107 @ sk108 )
| ~ ( A @ ( sk111 @ A ) @ ( sk112 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk109 @ sk110 )
| ( sk3 @ ( sk113 @ B ) @ ( sk114 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk109 @ sk110 ) )
& ( ~ ( sk11 @ sk107 @ sk108 )
| ~ ( A @ ( sk111 @ A ) @ ( sk112 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk109 @ sk110 )
| ~ ( B @ ( sk113 @ B ) @ ( sk114 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk109 @ sk110 ) )
& ( ~ ( sk11 @ sk107 @ sk108 )
| ~ ( sk11 @ sk109 @ sk110 ) ) ),
inference(cnf,[status(esa)],[372]) ).
thf(384,plain,
( ~ ( sk11 @ sk107 @ sk108 )
| ~ ( sk11 @ sk109 @ sk110 ) ),
inference(cnfConj,[status(thm)],[374]) ).
thf(15,plain,
( ( ! [A: a,B: a] :
( ( ( sk2 @ A @ B )
| ( sk3 @ A @ B ) )
=> ( sk14 @ A @ B ) ) )
!= ( ! [A: a,B: a] :
( ( ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) )
| ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) )
=> ( sk14 @ A @ B ) ) ) ),
inference(func_ext,[status(esa)],[13]) ).
thf(109,plain,
( ~ ! [A: a,B: a] :
( ( ( sk2 @ A @ B )
| ( sk3 @ A @ B ) )
=> ( sk14 @ A @ B ) )
| ~ ! [A: a,B: a] :
( ( ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) )
| ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) )
=> ( sk14 @ A @ B ) ) ),
inference(bool_ext,[status(thm)],[15]) ).
thf(111,plain,
! [B: a > a > $o,A: a > a > $o] :
( ( ( sk2 @ sk63 @ sk64 )
| ( sk3 @ sk63 @ sk64 )
| ( sk2 @ ( sk67 @ A ) @ ( sk68 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk65 @ sk66 )
| ( sk3 @ ( sk69 @ B ) @ ( sk70 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk65 @ sk66 ) )
& ( ( sk2 @ sk63 @ sk64 )
| ( sk3 @ sk63 @ sk64 )
| ( sk2 @ ( sk67 @ A ) @ ( sk68 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk65 @ sk66 )
| ~ ( B @ ( sk69 @ B ) @ ( sk70 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk65 @ sk66 ) )
& ( ( sk2 @ sk63 @ sk64 )
| ( sk3 @ sk63 @ sk64 )
| ~ ( A @ ( sk67 @ A ) @ ( sk68 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk65 @ sk66 )
| ( sk3 @ ( sk69 @ B ) @ ( sk70 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk65 @ sk66 ) )
& ( ( sk2 @ sk63 @ sk64 )
| ( sk3 @ sk63 @ sk64 )
| ~ ( A @ ( sk67 @ A ) @ ( sk68 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk65 @ sk66 )
| ~ ( B @ ( sk69 @ B ) @ ( sk70 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk65 @ sk66 ) )
& ( ( sk2 @ sk63 @ sk64 )
| ( sk3 @ sk63 @ sk64 )
| ~ ( sk14 @ sk65 @ sk66 ) )
& ( ~ ( sk14 @ sk63 @ sk64 )
| ( sk2 @ ( sk67 @ A ) @ ( sk68 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk65 @ sk66 )
| ( sk3 @ ( sk69 @ B ) @ ( sk70 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk65 @ sk66 ) )
& ( ~ ( sk14 @ sk63 @ sk64 )
| ( sk2 @ ( sk67 @ A ) @ ( sk68 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk65 @ sk66 )
| ~ ( B @ ( sk69 @ B ) @ ( sk70 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk65 @ sk66 ) )
& ( ~ ( sk14 @ sk63 @ sk64 )
| ~ ( A @ ( sk67 @ A ) @ ( sk68 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk65 @ sk66 )
| ( sk3 @ ( sk69 @ B ) @ ( sk70 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk65 @ sk66 ) )
& ( ~ ( sk14 @ sk63 @ sk64 )
| ~ ( A @ ( sk67 @ A ) @ ( sk68 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk65 @ sk66 )
| ~ ( B @ ( sk69 @ B ) @ ( sk70 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk65 @ sk66 ) )
& ( ~ ( sk14 @ sk63 @ sk64 )
| ~ ( sk14 @ sk65 @ sk66 ) ) ),
inference(cnf,[status(esa)],[109]) ).
thf(121,plain,
( ~ ( sk14 @ sk63 @ sk64 )
| ~ ( sk14 @ sk65 @ sk66 ) ),
inference(cnfConj,[status(thm)],[111]) ).
thf(141,plain,
( ~ ( sk14 @ sk63 @ sk64 )
| ( ( sk14 @ sk65 @ sk66 )
!= ( sk14 @ sk63 @ sk64 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[121]) ).
thf(142,plain,
( ~ ( sk14 @ sk63 @ sk64 )
| ( ( sk14 @ sk65 @ sk66 )
!= ( sk14 @ sk63 @ sk64 ) ) ),
inference(simp,[status(thm)],[141]) ).
thf(7,plain,
( ( ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( ( sk2 @ B @ C )
| ( sk3 @ B @ C ) )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk4 @ sk5 ) ) )
!= ( ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( ! [D: a > a > $o] :
( ( ! [E: a,F: a] :
( ( sk2 @ E @ F )
=> ( D @ E @ F ) )
& ( sk1 @ D ) )
=> ( D @ B @ C ) )
| ! [D: a > a > $o] :
( ( ! [E: a,F: a] :
( ( sk3 @ E @ F )
=> ( D @ E @ F ) )
& ( sk1 @ D ) )
=> ( D @ B @ C ) ) )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk4 @ sk5 ) ) ) ),
inference(func_ext,[status(esa)],[5]) ).
thf(57,plain,
( ( ^ [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( ( sk2 @ B @ C )
| ( sk3 @ B @ C ) )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk4 @ sk5 ) ) )
!= ( ^ [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( ! [D: a > a > $o] :
( ( ! [E: a,F: a] :
( ( sk2 @ E @ F )
=> ( D @ E @ F ) )
& ( sk1 @ D ) )
=> ( D @ B @ C ) )
| ! [D: a > a > $o] :
( ( ! [E: a,F: a] :
( ( sk3 @ E @ F )
=> ( D @ E @ F ) )
& ( sk1 @ D ) )
=> ( D @ B @ C ) ) )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk4 @ sk5 ) ) ) ),
inference(simp,[status(thm)],[7]) ).
thf(560,plain,
( ( ( ^ [A: a > a > $o] :
( ! [B: a,C: a] :
( ( ( sk2 @ B @ C )
| ( sk3 @ B @ C ) )
=> ( A @ B @ C ) )
& ( sk1 @ A ) ) )
!= ( ^ [A: a > a > $o] :
( ! [B: a,C: a] :
( ( ! [D: a > a > $o] :
( ( ! [E: a,F: a] :
( ( sk2 @ E @ F )
=> ( D @ E @ F ) )
& ( sk1 @ D ) )
=> ( D @ B @ C ) )
| ! [D: a > a > $o] :
( ( ! [E: a,F: a] :
( ( sk3 @ E @ F )
=> ( D @ E @ F ) )
& ( sk1 @ D ) )
=> ( D @ B @ C ) ) )
=> ( A @ B @ C ) )
& ( sk1 @ A ) ) ) )
| ( ( ^ [A: a > a > $o] : ( A @ sk4 @ sk5 ) )
!= ( ^ [A: a > a > $o] : ( A @ sk4 @ sk5 ) ) ) ),
inference(simp,[status(thm)],[57]) ).
thf(561,plain,
( ( ^ [A: a > a > $o] :
( ! [B: a,C: a] :
( ( ( sk2 @ B @ C )
| ( sk3 @ B @ C ) )
=> ( A @ B @ C ) )
& ( sk1 @ A ) ) )
!= ( ^ [A: a > a > $o] :
( ! [B: a,C: a] :
( ( ! [D: a > a > $o] :
( ( ! [E: a,F: a] :
( ( sk2 @ E @ F )
=> ( D @ E @ F ) )
& ( sk1 @ D ) )
=> ( D @ B @ C ) )
| ! [D: a > a > $o] :
( ( ! [E: a,F: a] :
( ( sk3 @ E @ F )
=> ( D @ E @ F ) )
& ( sk1 @ D ) )
=> ( D @ B @ C ) ) )
=> ( A @ B @ C ) )
& ( sk1 @ A ) ) ) ),
inference(simp,[status(thm)],[560]) ).
thf(562,plain,
( ( ( ^ [A: a > a > $o] :
! [B: a,C: a] :
( ( ( sk2 @ B @ C )
| ( sk3 @ B @ C ) )
=> ( A @ B @ C ) ) )
!= ( ^ [A: a > a > $o] :
! [B: a,C: a] :
( ( ! [D: a > a > $o] :
( ( ! [E: a,F: a] :
( ( sk2 @ E @ F )
=> ( D @ E @ F ) )
& ( sk1 @ D ) )
=> ( D @ B @ C ) )
| ! [D: a > a > $o] :
( ( ! [E: a,F: a] :
( ( sk3 @ E @ F )
=> ( D @ E @ F ) )
& ( sk1 @ D ) )
=> ( D @ B @ C ) ) )
=> ( A @ B @ C ) ) ) )
| ( sk1 != sk1 ) ),
inference(simp,[status(thm)],[561]) ).
thf(563,plain,
( ( ^ [A: a > a > $o] :
! [B: a,C: a] :
( ( ( sk2 @ B @ C )
| ( sk3 @ B @ C ) )
=> ( A @ B @ C ) ) )
!= ( ^ [A: a > a > $o] :
! [B: a,C: a] :
( ( ! [D: a > a > $o] :
( ( ! [E: a,F: a] :
( ( sk2 @ E @ F )
=> ( D @ E @ F ) )
& ( sk1 @ D ) )
=> ( D @ B @ C ) )
| ! [D: a > a > $o] :
( ( ! [E: a,F: a] :
( ( sk3 @ E @ F )
=> ( D @ E @ F ) )
& ( sk1 @ D ) )
=> ( D @ B @ C ) ) )
=> ( A @ B @ C ) ) ) ),
inference(simp,[status(thm)],[562]) ).
thf(564,plain,
( ( ^ [A: a > a > $o,B: a] :
! [C: a] :
( ( ( sk2 @ B @ C )
| ( sk3 @ B @ C ) )
=> ( A @ B @ C ) ) )
!= ( ^ [A: a > a > $o,B: a] :
! [C: a] :
( ( ! [D: a > a > $o] :
( ( ! [E: a,F: a] :
( ( sk2 @ E @ F )
=> ( D @ E @ F ) )
& ( sk1 @ D ) )
=> ( D @ B @ C ) )
| ! [D: a > a > $o] :
( ( ! [E: a,F: a] :
( ( sk3 @ E @ F )
=> ( D @ E @ F ) )
& ( sk1 @ D ) )
=> ( D @ B @ C ) ) )
=> ( A @ B @ C ) ) ) ),
inference(simp,[status(thm)],[563]) ).
thf(565,plain,
( ( ^ [A: a > a > $o,B: a,C: a] :
( ( ( sk2 @ B @ C )
| ( sk3 @ B @ C ) )
=> ( A @ B @ C ) ) )
!= ( ^ [A: a > a > $o,B: a,C: a] :
( ( ! [D: a > a > $o] :
( ( ! [E: a,F: a] :
( ( sk2 @ E @ F )
=> ( D @ E @ F ) )
& ( sk1 @ D ) )
=> ( D @ B @ C ) )
| ! [D: a > a > $o] :
( ( ! [E: a,F: a] :
( ( sk3 @ E @ F )
=> ( D @ E @ F ) )
& ( sk1 @ D ) )
=> ( D @ B @ C ) ) )
=> ( A @ B @ C ) ) ) ),
inference(simp,[status(thm)],[564]) ).
thf(295,plain,
( ~ ( ! [A: a,B: a] :
( ( ( sk2 @ A @ B )
| ( sk3 @ A @ B ) )
=> ( sk11 @ A @ B ) )
& ( sk1 @ sk11 ) )
| ~ ( ! [A: a,B: a] :
( ( ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) )
| ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) )
=> ( sk11 @ A @ B ) )
& ( sk1 @ sk11 ) ) ),
inference(bool_ext,[status(thm)],[12]) ).
thf(322,plain,
! [B: a > a > $o,A: a > a > $o] :
( ( ( sk2 @ sk97 @ sk98 )
| ( sk3 @ sk97 @ sk98 )
| ~ ( sk1 @ sk11 )
| ( sk2 @ ( sk101 @ A ) @ ( sk102 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk99 @ sk100 )
| ( sk3 @ ( sk103 @ B ) @ ( sk104 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk99 @ sk100 )
| ~ ( sk1 @ sk11 ) )
& ( ( sk2 @ sk97 @ sk98 )
| ( sk3 @ sk97 @ sk98 )
| ~ ( sk1 @ sk11 )
| ( sk2 @ ( sk101 @ A ) @ ( sk102 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk99 @ sk100 )
| ~ ( B @ ( sk103 @ B ) @ ( sk104 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk99 @ sk100 )
| ~ ( sk1 @ sk11 ) )
& ( ( sk2 @ sk97 @ sk98 )
| ( sk3 @ sk97 @ sk98 )
| ~ ( sk1 @ sk11 )
| ~ ( A @ ( sk101 @ A ) @ ( sk102 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk99 @ sk100 )
| ( sk3 @ ( sk103 @ B ) @ ( sk104 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk99 @ sk100 )
| ~ ( sk1 @ sk11 ) )
& ( ( sk2 @ sk97 @ sk98 )
| ( sk3 @ sk97 @ sk98 )
| ~ ( sk1 @ sk11 )
| ~ ( A @ ( sk101 @ A ) @ ( sk102 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk99 @ sk100 )
| ~ ( B @ ( sk103 @ B ) @ ( sk104 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk99 @ sk100 )
| ~ ( sk1 @ sk11 ) )
& ( ( sk2 @ sk97 @ sk98 )
| ( sk3 @ sk97 @ sk98 )
| ~ ( sk1 @ sk11 )
| ~ ( sk11 @ sk99 @ sk100 )
| ~ ( sk1 @ sk11 ) )
& ( ~ ( sk11 @ sk97 @ sk98 )
| ~ ( sk1 @ sk11 )
| ( sk2 @ ( sk101 @ A ) @ ( sk102 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk99 @ sk100 )
| ( sk3 @ ( sk103 @ B ) @ ( sk104 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk99 @ sk100 )
| ~ ( sk1 @ sk11 ) )
& ( ~ ( sk11 @ sk97 @ sk98 )
| ~ ( sk1 @ sk11 )
| ( sk2 @ ( sk101 @ A ) @ ( sk102 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk99 @ sk100 )
| ~ ( B @ ( sk103 @ B ) @ ( sk104 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk99 @ sk100 )
| ~ ( sk1 @ sk11 ) )
& ( ~ ( sk11 @ sk97 @ sk98 )
| ~ ( sk1 @ sk11 )
| ~ ( A @ ( sk101 @ A ) @ ( sk102 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk99 @ sk100 )
| ( sk3 @ ( sk103 @ B ) @ ( sk104 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk99 @ sk100 )
| ~ ( sk1 @ sk11 ) )
& ( ~ ( sk11 @ sk97 @ sk98 )
| ~ ( sk1 @ sk11 )
| ~ ( A @ ( sk101 @ A ) @ ( sk102 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk99 @ sk100 )
| ~ ( B @ ( sk103 @ B ) @ ( sk104 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk99 @ sk100 )
| ~ ( sk1 @ sk11 ) )
& ( ~ ( sk11 @ sk97 @ sk98 )
| ~ ( sk1 @ sk11 )
| ~ ( sk11 @ sk99 @ sk100 )
| ~ ( sk1 @ sk11 ) ) ),
inference(cnf,[status(esa)],[295]) ).
thf(329,plain,
( ~ ( sk11 @ sk97 @ sk98 )
| ~ ( sk1 @ sk11 )
| ~ ( sk11 @ sk99 @ sk100 )
| ~ ( sk1 @ sk11 ) ),
inference(cnfConj,[status(thm)],[322]) ).
thf(339,plain,
( ~ ( sk11 @ sk97 @ sk98 )
| ~ ( sk1 @ sk11 )
| ~ ( sk11 @ sk99 @ sk100 ) ),
inference(simp,[status(thm)],[329]) ).
thf(296,plain,
( ( ! [A: a,B: a] :
( ( ( sk2 @ A @ B )
| ( sk3 @ A @ B ) )
=> ( sk11 @ A @ B ) )
& ( sk1 @ sk11 ) )
| ( ! [A: a,B: a] :
( ( ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) )
| ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) )
=> ( sk11 @ A @ B ) )
& ( sk1 @ sk11 ) ) ),
inference(bool_ext,[status(thm)],[12]) ).
thf(343,plain,
! [H: a,G: a,F: a,E: a,D: a,C: a,B: a,A: a] :
( ( ~ ( sk2 @ A @ B )
| ( sk11 @ A @ B )
| ~ ( sk2 @ E @ F )
| ( sk105 @ D @ C @ B @ A @ E @ F )
| ( sk11 @ C @ D ) )
& ( ~ ( sk2 @ A @ B )
| ( sk11 @ A @ B )
| ( sk1 @ ( sk105 @ D @ C @ B @ A ) )
| ( sk11 @ C @ D ) )
& ( ~ ( sk2 @ A @ B )
| ( sk11 @ A @ B )
| ~ ( sk105 @ D @ C @ B @ A @ C @ D )
| ( sk11 @ C @ D ) )
& ( ~ ( sk2 @ A @ B )
| ( sk11 @ A @ B )
| ~ ( sk3 @ G @ H )
| ( sk106 @ D @ C @ B @ A @ G @ H )
| ( sk11 @ C @ D ) )
& ( ~ ( sk2 @ A @ B )
| ( sk11 @ A @ B )
| ( sk1 @ ( sk106 @ D @ C @ B @ A ) )
| ( sk11 @ C @ D ) )
& ( ~ ( sk2 @ A @ B )
| ( sk11 @ A @ B )
| ~ ( sk106 @ D @ C @ B @ A @ C @ D )
| ( sk11 @ C @ D ) )
& ( ~ ( sk2 @ A @ B )
| ( sk11 @ A @ B )
| ( sk1 @ sk11 ) )
& ( ~ ( sk3 @ A @ B )
| ( sk11 @ A @ B )
| ~ ( sk2 @ E @ F )
| ( sk105 @ D @ C @ B @ A @ E @ F )
| ( sk11 @ C @ D ) )
& ( ~ ( sk3 @ A @ B )
| ( sk11 @ A @ B )
| ( sk1 @ ( sk105 @ D @ C @ B @ A ) )
| ( sk11 @ C @ D ) )
& ( ~ ( sk3 @ A @ B )
| ( sk11 @ A @ B )
| ~ ( sk105 @ D @ C @ B @ A @ C @ D )
| ( sk11 @ C @ D ) )
& ( ~ ( sk3 @ A @ B )
| ( sk11 @ A @ B )
| ~ ( sk3 @ G @ H )
| ( sk106 @ D @ C @ B @ A @ G @ H )
| ( sk11 @ C @ D ) )
& ( ~ ( sk3 @ A @ B )
| ( sk11 @ A @ B )
| ( sk1 @ ( sk106 @ D @ C @ B @ A ) )
| ( sk11 @ C @ D ) )
& ( ~ ( sk3 @ A @ B )
| ( sk11 @ A @ B )
| ~ ( sk106 @ D @ C @ B @ A @ C @ D )
| ( sk11 @ C @ D ) )
& ( ~ ( sk3 @ A @ B )
| ( sk11 @ A @ B )
| ( sk1 @ sk11 ) )
& ( ( sk1 @ sk11 )
| ~ ( sk2 @ E @ F )
| ( sk105 @ D @ C @ B @ A @ E @ F )
| ( sk11 @ C @ D ) )
& ( ( sk1 @ sk11 )
| ( sk1 @ ( sk105 @ D @ C @ B @ A ) )
| ( sk11 @ C @ D ) )
& ( ( sk1 @ sk11 )
| ~ ( sk105 @ D @ C @ B @ A @ C @ D )
| ( sk11 @ C @ D ) )
& ( ( sk1 @ sk11 )
| ~ ( sk3 @ G @ H )
| ( sk106 @ D @ C @ B @ A @ G @ H )
| ( sk11 @ C @ D ) )
& ( ( sk1 @ sk11 )
| ( sk1 @ ( sk106 @ D @ C @ B @ A ) )
| ( sk11 @ C @ D ) )
& ( ( sk1 @ sk11 )
| ~ ( sk106 @ D @ C @ B @ A @ C @ D )
| ( sk11 @ C @ D ) )
& ( ( sk1 @ sk11 )
| ( sk1 @ sk11 ) ) ),
inference(cnf,[status(esa)],[296]) ).
thf(344,plain,
( ( sk1 @ sk11 )
| ( sk1 @ sk11 ) ),
inference(cnfConj,[status(thm)],[343]) ).
thf(368,plain,
sk1 @ sk11,
inference(simp,[status(thm)],[344]) ).
thf(648,plain,
( ~ ( sk11 @ sk97 @ sk98 )
| ~ $true
| ~ ( sk11 @ sk99 @ sk100 ) ),
inference(rewrite,[status(thm)],[339,368]) ).
thf(649,plain,
( ~ ( sk11 @ sk97 @ sk98 )
| ~ ( sk11 @ sk99 @ sk100 ) ),
inference(simp,[status(thm)],[648]) ).
thf(650,plain,
( ~ ( sk11 @ sk97 @ sk98 )
| ( ( sk11 @ sk99 @ sk100 )
!= ( sk11 @ sk97 @ sk98 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[649]) ).
thf(651,plain,
( ~ ( sk11 @ sk97 @ sk98 )
| ( ( sk11 @ sk99 @ sk100 )
!= ( sk11 @ sk97 @ sk98 ) ) ),
inference(simp,[status(thm)],[650]) ).
thf(510,plain,
( ( ! [A: a] :
( ( ( sk2 @ sk139 @ A )
| ( sk3 @ sk139 @ A ) )
=> ( sk8 @ sk139 @ A ) ) )
!= ( ! [A: a] :
( ( ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk2 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk139 @ A ) )
| ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk3 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk139 @ A ) ) )
=> ( sk8 @ sk139 @ A ) ) ) ),
inference(func_ext,[status(esa)],[480]) ).
thf(522,plain,
( ~ ! [A: a] :
( ( ( sk2 @ sk139 @ A )
| ( sk3 @ sk139 @ A ) )
=> ( sk8 @ sk139 @ A ) )
| ~ ! [A: a] :
( ( ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk2 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk139 @ A ) )
| ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk3 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk139 @ A ) ) )
=> ( sk8 @ sk139 @ A ) ) ),
inference(bool_ext,[status(thm)],[510]) ).
thf(524,plain,
! [B: a > a > $o,A: a > a > $o] :
( ( ( sk2 @ sk139 @ sk142 )
| ( sk3 @ sk139 @ sk142 )
| ( sk2 @ ( sk144 @ A ) @ ( sk145 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk139 @ sk143 )
| ( sk3 @ ( sk146 @ B ) @ ( sk147 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk139 @ sk143 ) )
& ( ( sk2 @ sk139 @ sk142 )
| ( sk3 @ sk139 @ sk142 )
| ( sk2 @ ( sk144 @ A ) @ ( sk145 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk139 @ sk143 )
| ~ ( B @ ( sk146 @ B ) @ ( sk147 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk139 @ sk143 ) )
& ( ( sk2 @ sk139 @ sk142 )
| ( sk3 @ sk139 @ sk142 )
| ~ ( A @ ( sk144 @ A ) @ ( sk145 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk139 @ sk143 )
| ( sk3 @ ( sk146 @ B ) @ ( sk147 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk139 @ sk143 ) )
& ( ( sk2 @ sk139 @ sk142 )
| ( sk3 @ sk139 @ sk142 )
| ~ ( A @ ( sk144 @ A ) @ ( sk145 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk139 @ sk143 )
| ~ ( B @ ( sk146 @ B ) @ ( sk147 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk139 @ sk143 ) )
& ( ( sk2 @ sk139 @ sk142 )
| ( sk3 @ sk139 @ sk142 )
| ~ ( sk8 @ sk139 @ sk143 ) )
& ( ~ ( sk8 @ sk139 @ sk142 )
| ( sk2 @ ( sk144 @ A ) @ ( sk145 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk139 @ sk143 )
| ( sk3 @ ( sk146 @ B ) @ ( sk147 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk139 @ sk143 ) )
& ( ~ ( sk8 @ sk139 @ sk142 )
| ( sk2 @ ( sk144 @ A ) @ ( sk145 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk139 @ sk143 )
| ~ ( B @ ( sk146 @ B ) @ ( sk147 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk139 @ sk143 ) )
& ( ~ ( sk8 @ sk139 @ sk142 )
| ~ ( A @ ( sk144 @ A ) @ ( sk145 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk139 @ sk143 )
| ( sk3 @ ( sk146 @ B ) @ ( sk147 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk139 @ sk143 ) )
& ( ~ ( sk8 @ sk139 @ sk142 )
| ~ ( A @ ( sk144 @ A ) @ ( sk145 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk139 @ sk143 )
| ~ ( B @ ( sk146 @ B ) @ ( sk147 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk139 @ sk143 ) )
& ( ~ ( sk8 @ sk139 @ sk142 )
| ~ ( sk8 @ sk139 @ sk143 ) ) ),
inference(cnf,[status(esa)],[522]) ).
thf(525,plain,
( ~ ( sk8 @ sk139 @ sk142 )
| ~ ( sk8 @ sk139 @ sk143 ) ),
inference(cnfConj,[status(thm)],[524]) ).
thf(569,plain,
( ~ ( sk8 @ sk139 @ sk142 )
| ( ( sk8 @ sk139 @ sk143 )
!= ( sk8 @ sk139 @ sk142 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[525]) ).
thf(570,plain,
( ~ ( sk8 @ sk139 @ sk142 )
| ( ( sk8 @ sk139 @ sk143 )
!= ( sk8 @ sk139 @ sk142 ) ) ),
inference(simp,[status(thm)],[569]) ).
thf(21,plain,
( ( ( ^ [A: a,B: a,C: a > a > $o] : sk2 )
!= ( ^ [A: a,B: a,C: a > a > $o,D: a,E: a] :
! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( sk2 @ G @ H )
=> ( F @ G @ H ) )
& ( sk1 @ F ) )
=> ( F @ D @ E ) ) ) )
| ( ( ^ [A: a,B: a,C: a > a > $o] : sk3 )
!= ( ^ [A: a,B: a,C: a > a > $o,D: a,E: a] :
! [F: a > a > $o] :
( ( ! [G: a,H: a] :
( ( sk3 @ G @ H )
=> ( F @ G @ H ) )
& ( sk1 @ F ) )
=> ( F @ D @ E ) ) ) ) ),
inference(simp,[status(thm)],[20]) ).
thf(23,plain,
( ( ( sk2 @ sk32 @ sk33 )
!= ( ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk2 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk32 @ sk33 ) ) ) )
| ( ( sk3 @ sk37 @ sk38 )
!= ( ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk3 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk37 @ sk38 ) ) ) ) ),
inference(func_ext,[status(esa)],[21]) ).
thf(24,plain,
( ~ ( sk2 @ sk32 @ sk33 )
| ~ ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk2 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk32 @ sk33 ) )
| ~ ( sk3 @ sk37 @ sk38 )
| ~ ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk3 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk37 @ sk38 ) ) ),
inference(bool_ext,[status(thm)],[23]) ).
thf(28,plain,
! [D: a,C: a,B: a,A: a] :
( ( ~ ( sk2 @ sk32 @ sk33 )
| ~ ( sk2 @ A @ B )
| ( sk39 @ A @ B )
| ~ ( sk3 @ sk37 @ sk38 )
| ~ ( sk3 @ C @ D )
| ( sk40 @ B @ A @ C @ D ) )
& ( ~ ( sk2 @ sk32 @ sk33 )
| ~ ( sk2 @ A @ B )
| ( sk39 @ A @ B )
| ~ ( sk3 @ sk37 @ sk38 )
| ( sk1 @ ( sk40 @ B @ A ) ) )
& ( ~ ( sk2 @ sk32 @ sk33 )
| ~ ( sk2 @ A @ B )
| ( sk39 @ A @ B )
| ~ ( sk3 @ sk37 @ sk38 )
| ~ ( sk40 @ B @ A @ sk37 @ sk38 ) )
& ( ~ ( sk2 @ sk32 @ sk33 )
| ( sk1 @ sk39 )
| ~ ( sk3 @ sk37 @ sk38 )
| ~ ( sk3 @ C @ D )
| ( sk40 @ B @ A @ C @ D ) )
& ( ~ ( sk2 @ sk32 @ sk33 )
| ( sk1 @ sk39 )
| ~ ( sk3 @ sk37 @ sk38 )
| ( sk1 @ ( sk40 @ B @ A ) ) )
& ( ~ ( sk2 @ sk32 @ sk33 )
| ( sk1 @ sk39 )
| ~ ( sk3 @ sk37 @ sk38 )
| ~ ( sk40 @ B @ A @ sk37 @ sk38 ) )
& ( ~ ( sk2 @ sk32 @ sk33 )
| ~ ( sk39 @ sk32 @ sk33 )
| ~ ( sk3 @ sk37 @ sk38 )
| ~ ( sk3 @ C @ D )
| ( sk40 @ B @ A @ C @ D ) )
& ( ~ ( sk2 @ sk32 @ sk33 )
| ~ ( sk39 @ sk32 @ sk33 )
| ~ ( sk3 @ sk37 @ sk38 )
| ( sk1 @ ( sk40 @ B @ A ) ) )
& ( ~ ( sk2 @ sk32 @ sk33 )
| ~ ( sk39 @ sk32 @ sk33 )
| ~ ( sk3 @ sk37 @ sk38 )
| ~ ( sk40 @ B @ A @ sk37 @ sk38 ) ) ),
inference(cnf,[status(esa)],[24]) ).
thf(31,plain,
! [D: a,C: a,B: a,A: a] :
( ~ ( sk2 @ sk32 @ sk33 )
| ~ ( sk39 @ sk32 @ sk33 )
| ~ ( sk3 @ sk37 @ sk38 )
| ~ ( sk3 @ C @ D )
| ( sk40 @ B @ A @ C @ D ) ),
inference(cnfConj,[status(thm)],[28]) ).
thf(29,plain,
! [B: a,A: a] :
( ~ ( sk2 @ sk32 @ sk33 )
| ~ ( sk39 @ sk32 @ sk33 )
| ~ ( sk3 @ sk37 @ sk38 )
| ~ ( sk40 @ B @ A @ sk37 @ sk38 ) ),
inference(cnfConj,[status(thm)],[28]) ).
thf(556,plain,
! [F: a,E: a,D: a,C: a,B: a,A: a] :
( ~ ( sk2 @ sk32 @ sk33 )
| ~ ( sk39 @ sk32 @ sk33 )
| ~ ( sk3 @ sk37 @ sk38 )
| ~ ( sk3 @ C @ D )
| ~ ( sk2 @ sk32 @ sk33 )
| ~ ( sk39 @ sk32 @ sk33 )
| ~ ( sk3 @ sk37 @ sk38 )
| ~ $true
| ( ( sk40 @ B @ A @ C @ D )
!= ( sk40 @ F @ E @ sk37 @ sk38 ) ) ),
inference(paramod_ordered,[status(thm)],[31,29]) ).
thf(557,plain,
! [F: a,E: a,D: a,C: a,B: a,A: a] :
( ~ ( sk2 @ sk32 @ sk33 )
| ~ ( sk39 @ sk32 @ sk33 )
| ~ ( sk3 @ sk37 @ sk38 )
| ~ ( sk3 @ C @ D )
| ( ( sk40 @ B @ A @ C @ D )
!= ( sk40 @ F @ E @ sk37 @ sk38 ) ) ),
inference(simp,[status(thm)],[556]) ).
thf(558,plain,
( ~ ( sk2 @ sk32 @ sk33 )
| ~ ( sk39 @ sk32 @ sk33 )
| ~ ( sk3 @ sk37 @ sk38 )
| ~ ( sk3 @ sk37 @ sk38 ) ),
inference(pattern_uni,[status(thm)],[557:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( sk37 )),bind(D,$thf( sk38 )),bind(E,$thf( A )),bind(F,$thf( B ))]]) ).
thf(559,plain,
( ~ ( sk2 @ sk32 @ sk33 )
| ~ ( sk39 @ sk32 @ sk33 )
| ~ ( sk3 @ sk37 @ sk38 ) ),
inference(simp,[status(thm)],[558]) ).
thf(248,plain,
( ~ ( sk3 @ sk27 @ sk28 )
| ( sk1 @ sk83 ) ),
inference(cnfConj,[status(thm)],[243]) ).
thf(511,plain,
( ~ ( sk11 @ sk107 @ sk108 )
| ( ( sk11 @ sk109 @ sk110 )
!= ( sk11 @ sk107 @ sk108 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[384]) ).
thf(512,plain,
( ~ ( sk11 @ sk107 @ sk108 )
| ( ( sk11 @ sk109 @ sk110 )
!= ( sk11 @ sk107 @ sk108 ) ) ),
inference(simp,[status(thm)],[511]) ).
thf(661,plain,
( ~ ( sk3 @ sk140 @ sk141 )
| ( sk1 @ sk157 ) ),
inference(cnfConj,[status(thm)],[660]) ).
thf(19,plain,
( ( ( ( sk2 @ sk22 @ sk23 )
| ( sk3 @ sk22 @ sk23 ) )
=> ( sk21 @ sk22 @ sk23 ) )
!= ( ( ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk2 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk22 @ sk23 ) )
| ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk3 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk22 @ sk23 ) ) )
=> ( sk21 @ sk22 @ sk23 ) ) ),
inference(func_ext,[status(esa)],[16]) ).
thf(404,plain,
( ( ( ( sk2 @ sk22 @ sk23 )
| ( sk3 @ sk22 @ sk23 ) )
!= ( ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk2 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk22 @ sk23 ) )
| ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk3 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk22 @ sk23 ) ) ) )
| ( ( sk21 @ sk22 @ sk23 )
!= ( sk21 @ sk22 @ sk23 ) ) ),
inference(simp,[status(thm)],[19]) ).
thf(407,plain,
( ( ( sk2 @ sk22 @ sk23 )
| ( sk3 @ sk22 @ sk23 ) )
!= ( ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk2 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk22 @ sk23 ) )
| ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk3 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk22 @ sk23 ) ) ) ),
inference(simp,[status(thm)],[404]) ).
thf(448,plain,
( ~ ( ( sk2 @ sk22 @ sk23 )
| ( sk3 @ sk22 @ sk23 ) )
| ~ ( ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk2 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk22 @ sk23 ) )
| ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk3 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk22 @ sk23 ) ) ) ),
inference(bool_ext,[status(thm)],[407]) ).
thf(450,plain,
! [D: a,C: a,B: a,A: a] :
( ( ~ ( sk2 @ sk22 @ sk23 )
| ~ ( sk2 @ A @ B )
| ( sk123 @ A @ B ) )
& ( ~ ( sk2 @ sk22 @ sk23 )
| ( sk1 @ sk123 ) )
& ( ~ ( sk2 @ sk22 @ sk23 )
| ~ ( sk123 @ sk22 @ sk23 ) )
& ( ~ ( sk2 @ sk22 @ sk23 )
| ~ ( sk3 @ C @ D )
| ( sk124 @ C @ D ) )
& ( ~ ( sk2 @ sk22 @ sk23 )
| ( sk1 @ sk124 ) )
& ( ~ ( sk2 @ sk22 @ sk23 )
| ~ ( sk124 @ sk22 @ sk23 ) )
& ( ~ ( sk3 @ sk22 @ sk23 )
| ~ ( sk2 @ A @ B )
| ( sk123 @ A @ B ) )
& ( ~ ( sk3 @ sk22 @ sk23 )
| ( sk1 @ sk123 ) )
& ( ~ ( sk3 @ sk22 @ sk23 )
| ~ ( sk123 @ sk22 @ sk23 ) )
& ( ~ ( sk3 @ sk22 @ sk23 )
| ~ ( sk3 @ C @ D )
| ( sk124 @ C @ D ) )
& ( ~ ( sk3 @ sk22 @ sk23 )
| ( sk1 @ sk124 ) )
& ( ~ ( sk3 @ sk22 @ sk23 )
| ~ ( sk124 @ sk22 @ sk23 ) ) ),
inference(cnf,[status(esa)],[448]) ).
thf(452,plain,
( ~ ( sk3 @ sk22 @ sk23 )
| ( sk1 @ sk123 ) ),
inference(cnfConj,[status(thm)],[450]) ).
thf(33,plain,
! [D: a,C: a,B: a,A: a] :
( ~ ( sk2 @ sk32 @ sk33 )
| ~ ( sk2 @ A @ B )
| ( sk39 @ A @ B )
| ~ ( sk3 @ sk37 @ sk38 )
| ~ ( sk3 @ C @ D )
| ( sk40 @ B @ A @ C @ D ) ),
inference(cnfConj,[status(thm)],[28]) ).
thf(108,plain,
( ( ^ [A: a] :
! [B: a] :
( ( ( sk2 @ A @ B )
| ( sk3 @ A @ B ) )
=> ( sk14 @ A @ B ) ) )
!= ( ^ [A: a] :
! [B: a] :
( ( ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) )
| ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) )
=> ( sk14 @ A @ B ) ) ) ),
inference(simp,[status(thm)],[15]) ).
thf(137,plain,
( ( ^ [A: a,B: a] :
( ( ( sk2 @ A @ B )
| ( sk3 @ A @ B ) )
=> ( sk14 @ A @ B ) ) )
!= ( ^ [A: a,B: a] :
( ( ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) )
| ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) )
=> ( sk14 @ A @ B ) ) ) ),
inference(simp,[status(thm)],[108]) ).
thf(252,plain,
( ~ ( sk3 @ sk27 @ sk28 )
| ~ ( sk84 @ sk27 @ sk28 ) ),
inference(cnfConj,[status(thm)],[243]) ).
thf(58,plain,
( ~ ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( ( sk2 @ B @ C )
| ( sk3 @ B @ C ) )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk4 @ sk5 ) )
| ~ ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( ! [D: a > a > $o] :
( ( ! [E: a,F: a] :
( ( sk2 @ E @ F )
=> ( D @ E @ F ) )
& ( sk1 @ D ) )
=> ( D @ B @ C ) )
| ! [D: a > a > $o] :
( ( ! [E: a,F: a] :
( ( sk3 @ E @ F )
=> ( D @ E @ F ) )
& ( sk1 @ D ) )
=> ( D @ B @ C ) ) )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk4 @ sk5 ) ) ),
inference(bool_ext,[status(thm)],[7]) ).
thf(60,plain,
! [H: a,G: a,F: a,E: a,D: a,C: a,B: a,A: a] :
( ( ~ ( sk2 @ A @ B )
| ( sk51 @ A @ B )
| ~ ( sk2 @ E @ F )
| ( sk53 @ D @ C @ B @ A @ E @ F )
| ( sk52 @ B @ A @ C @ D ) )
& ( ~ ( sk2 @ A @ B )
| ( sk51 @ A @ B )
| ( sk1 @ ( sk53 @ D @ C @ B @ A ) )
| ( sk52 @ B @ A @ C @ D ) )
& ( ~ ( sk2 @ A @ B )
| ( sk51 @ A @ B )
| ~ ( sk53 @ D @ C @ B @ A @ C @ D )
| ( sk52 @ B @ A @ C @ D ) )
& ( ~ ( sk2 @ A @ B )
| ( sk51 @ A @ B )
| ~ ( sk3 @ G @ H )
| ( sk54 @ D @ C @ B @ A @ G @ H )
| ( sk52 @ B @ A @ C @ D ) )
& ( ~ ( sk2 @ A @ B )
| ( sk51 @ A @ B )
| ( sk1 @ ( sk54 @ D @ C @ B @ A ) )
| ( sk52 @ B @ A @ C @ D ) )
& ( ~ ( sk2 @ A @ B )
| ( sk51 @ A @ B )
| ~ ( sk54 @ D @ C @ B @ A @ C @ D )
| ( sk52 @ B @ A @ C @ D ) )
& ( ~ ( sk2 @ A @ B )
| ( sk51 @ A @ B )
| ( sk1 @ ( sk52 @ B @ A ) ) )
& ( ~ ( sk2 @ A @ B )
| ( sk51 @ A @ B )
| ~ ( sk52 @ B @ A @ sk4 @ sk5 ) )
& ( ~ ( sk3 @ A @ B )
| ( sk51 @ A @ B )
| ~ ( sk2 @ E @ F )
| ( sk53 @ D @ C @ B @ A @ E @ F )
| ( sk52 @ B @ A @ C @ D ) )
& ( ~ ( sk3 @ A @ B )
| ( sk51 @ A @ B )
| ( sk1 @ ( sk53 @ D @ C @ B @ A ) )
| ( sk52 @ B @ A @ C @ D ) )
& ( ~ ( sk3 @ A @ B )
| ( sk51 @ A @ B )
| ~ ( sk53 @ D @ C @ B @ A @ C @ D )
| ( sk52 @ B @ A @ C @ D ) )
& ( ~ ( sk3 @ A @ B )
| ( sk51 @ A @ B )
| ~ ( sk3 @ G @ H )
| ( sk54 @ D @ C @ B @ A @ G @ H )
| ( sk52 @ B @ A @ C @ D ) )
& ( ~ ( sk3 @ A @ B )
| ( sk51 @ A @ B )
| ( sk1 @ ( sk54 @ D @ C @ B @ A ) )
| ( sk52 @ B @ A @ C @ D ) )
& ( ~ ( sk3 @ A @ B )
| ( sk51 @ A @ B )
| ~ ( sk54 @ D @ C @ B @ A @ C @ D )
| ( sk52 @ B @ A @ C @ D ) )
& ( ~ ( sk3 @ A @ B )
| ( sk51 @ A @ B )
| ( sk1 @ ( sk52 @ B @ A ) ) )
& ( ~ ( sk3 @ A @ B )
| ( sk51 @ A @ B )
| ~ ( sk52 @ B @ A @ sk4 @ sk5 ) )
& ( ( sk1 @ sk51 )
| ~ ( sk2 @ E @ F )
| ( sk53 @ D @ C @ B @ A @ E @ F )
| ( sk52 @ B @ A @ C @ D ) )
& ( ( sk1 @ sk51 )
| ( sk1 @ ( sk53 @ D @ C @ B @ A ) )
| ( sk52 @ B @ A @ C @ D ) )
& ( ( sk1 @ sk51 )
| ~ ( sk53 @ D @ C @ B @ A @ C @ D )
| ( sk52 @ B @ A @ C @ D ) )
& ( ( sk1 @ sk51 )
| ~ ( sk3 @ G @ H )
| ( sk54 @ D @ C @ B @ A @ G @ H )
| ( sk52 @ B @ A @ C @ D ) )
& ( ( sk1 @ sk51 )
| ( sk1 @ ( sk54 @ D @ C @ B @ A ) )
| ( sk52 @ B @ A @ C @ D ) )
& ( ( sk1 @ sk51 )
| ~ ( sk54 @ D @ C @ B @ A @ C @ D )
| ( sk52 @ B @ A @ C @ D ) )
& ( ( sk1 @ sk51 )
| ( sk1 @ ( sk52 @ B @ A ) ) )
& ( ( sk1 @ sk51 )
| ~ ( sk52 @ B @ A @ sk4 @ sk5 ) )
& ( ~ ( sk51 @ sk4 @ sk5 )
| ~ ( sk2 @ E @ F )
| ( sk53 @ D @ C @ B @ A @ E @ F )
| ( sk52 @ B @ A @ C @ D ) )
& ( ~ ( sk51 @ sk4 @ sk5 )
| ( sk1 @ ( sk53 @ D @ C @ B @ A ) )
| ( sk52 @ B @ A @ C @ D ) )
& ( ~ ( sk51 @ sk4 @ sk5 )
| ~ ( sk53 @ D @ C @ B @ A @ C @ D )
| ( sk52 @ B @ A @ C @ D ) )
& ( ~ ( sk51 @ sk4 @ sk5 )
| ~ ( sk3 @ G @ H )
| ( sk54 @ D @ C @ B @ A @ G @ H )
| ( sk52 @ B @ A @ C @ D ) )
& ( ~ ( sk51 @ sk4 @ sk5 )
| ( sk1 @ ( sk54 @ D @ C @ B @ A ) )
| ( sk52 @ B @ A @ C @ D ) )
& ( ~ ( sk51 @ sk4 @ sk5 )
| ~ ( sk54 @ D @ C @ B @ A @ C @ D )
| ( sk52 @ B @ A @ C @ D ) )
& ( ~ ( sk51 @ sk4 @ sk5 )
| ( sk1 @ ( sk52 @ B @ A ) ) )
& ( ~ ( sk51 @ sk4 @ sk5 )
| ~ ( sk52 @ B @ A @ sk4 @ sk5 ) ) ),
inference(cnf,[status(esa)],[58]) ).
thf(65,plain,
! [D: a,C: a,B: a,A: a] :
( ( sk1 @ sk51 )
| ( sk1 @ ( sk53 @ D @ C @ B @ A ) )
| ( sk52 @ B @ A @ C @ D ) ),
inference(cnfConj,[status(thm)],[60]) ).
thf(665,plain,
( ~ ( sk2 @ sk140 @ sk141 )
| ~ ( sk156 @ sk140 @ sk141 ) ),
inference(cnfConj,[status(thm)],[660]) ).
thf(461,plain,
( ~ ( sk3 @ sk22 @ sk23 )
| ( sk1 @ sk124 ) ),
inference(cnfConj,[status(thm)],[450]) ).
thf(521,plain,
( ( ^ [A: a] :
( ( ( sk2 @ sk139 @ A )
| ( sk3 @ sk139 @ A ) )
=> ( sk8 @ sk139 @ A ) ) )
!= ( ^ [A: a] :
( ( ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk2 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk139 @ A ) )
| ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk3 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk139 @ A ) ) )
=> ( sk8 @ sk139 @ A ) ) ) ),
inference(simp,[status(thm)],[510]) ).
thf(550,plain,
( ( ( ^ [A: a] :
( ( sk2 @ sk139 @ A )
| ( sk3 @ sk139 @ A ) ) )
!= ( ^ [A: a] :
( ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk2 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk139 @ A ) )
| ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk3 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk139 @ A ) ) ) ) )
| ( ( sk8 @ sk139 )
!= ( sk8 @ sk139 ) ) ),
inference(simp,[status(thm)],[521]) ).
thf(551,plain,
( ( ^ [A: a] :
( ( sk2 @ sk139 @ A )
| ( sk3 @ sk139 @ A ) ) )
!= ( ^ [A: a] :
( ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk2 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk139 @ A ) )
| ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk3 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk139 @ A ) ) ) ) ),
inference(simp,[status(thm)],[550]) ).
thf(456,plain,
( ~ ( sk2 @ sk22 @ sk23 )
| ~ ( sk124 @ sk22 @ sk23 ) ),
inference(cnfConj,[status(thm)],[450]) ).
thf(17,plain,
( ( ! [A: a] :
( ( ( sk2 @ sk18 @ A )
| ( sk3 @ sk18 @ A ) )
=> ( sk17 @ sk18 @ A ) ) )
!= ( ! [A: a] :
( ( ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk2 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk18 @ A ) )
| ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk3 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk18 @ A ) ) )
=> ( sk17 @ sk18 @ A ) ) ) ),
inference(func_ext,[status(esa)],[14]) ).
thf(264,plain,
( ~ ! [A: a] :
( ( ( sk2 @ sk18 @ A )
| ( sk3 @ sk18 @ A ) )
=> ( sk17 @ sk18 @ A ) )
| ~ ! [A: a] :
( ( ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk2 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk18 @ A ) )
| ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk3 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk18 @ A ) ) )
=> ( sk17 @ sk18 @ A ) ) ),
inference(bool_ext,[status(thm)],[17]) ).
thf(266,plain,
! [B: a > a > $o,A: a > a > $o] :
( ( ( sk2 @ sk18 @ sk89 )
| ( sk3 @ sk18 @ sk89 )
| ( sk2 @ ( sk91 @ A ) @ ( sk92 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk18 @ sk90 )
| ( sk3 @ ( sk93 @ B ) @ ( sk94 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk18 @ sk90 ) )
& ( ( sk2 @ sk18 @ sk89 )
| ( sk3 @ sk18 @ sk89 )
| ( sk2 @ ( sk91 @ A ) @ ( sk92 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk18 @ sk90 )
| ~ ( B @ ( sk93 @ B ) @ ( sk94 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk18 @ sk90 ) )
& ( ( sk2 @ sk18 @ sk89 )
| ( sk3 @ sk18 @ sk89 )
| ~ ( A @ ( sk91 @ A ) @ ( sk92 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk18 @ sk90 )
| ( sk3 @ ( sk93 @ B ) @ ( sk94 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk18 @ sk90 ) )
& ( ( sk2 @ sk18 @ sk89 )
| ( sk3 @ sk18 @ sk89 )
| ~ ( A @ ( sk91 @ A ) @ ( sk92 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk18 @ sk90 )
| ~ ( B @ ( sk93 @ B ) @ ( sk94 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk18 @ sk90 ) )
& ( ( sk2 @ sk18 @ sk89 )
| ( sk3 @ sk18 @ sk89 )
| ~ ( sk17 @ sk18 @ sk90 ) )
& ( ~ ( sk17 @ sk18 @ sk89 )
| ( sk2 @ ( sk91 @ A ) @ ( sk92 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk18 @ sk90 )
| ( sk3 @ ( sk93 @ B ) @ ( sk94 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk18 @ sk90 ) )
& ( ~ ( sk17 @ sk18 @ sk89 )
| ( sk2 @ ( sk91 @ A ) @ ( sk92 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk18 @ sk90 )
| ~ ( B @ ( sk93 @ B ) @ ( sk94 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk18 @ sk90 ) )
& ( ~ ( sk17 @ sk18 @ sk89 )
| ~ ( A @ ( sk91 @ A ) @ ( sk92 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk18 @ sk90 )
| ( sk3 @ ( sk93 @ B ) @ ( sk94 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk18 @ sk90 ) )
& ( ~ ( sk17 @ sk18 @ sk89 )
| ~ ( A @ ( sk91 @ A ) @ ( sk92 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk18 @ sk90 )
| ~ ( B @ ( sk93 @ B ) @ ( sk94 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk18 @ sk90 ) )
& ( ~ ( sk17 @ sk18 @ sk89 )
| ~ ( sk17 @ sk18 @ sk90 ) ) ),
inference(cnf,[status(esa)],[264]) ).
thf(273,plain,
( ~ ( sk17 @ sk18 @ sk89 )
| ~ ( sk17 @ sk18 @ sk90 ) ),
inference(cnfConj,[status(thm)],[266]) ).
thf(470,plain,
( ~ ( sk17 @ sk18 @ sk89 )
| ( ( sk17 @ sk18 @ sk90 )
!= ( sk17 @ sk18 @ sk89 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[273]) ).
thf(471,plain,
( ~ ( sk17 @ sk18 @ sk89 )
| ( ( sk17 @ sk18 @ sk90 )
!= ( sk17 @ sk18 @ sk89 ) ) ),
inference(simp,[status(thm)],[470]) ).
thf(263,plain,
( ( ^ [A: a] :
( ( ( sk2 @ sk18 @ A )
| ( sk3 @ sk18 @ A ) )
=> ( sk17 @ sk18 @ A ) ) )
!= ( ^ [A: a] :
( ( ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk2 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk18 @ A ) )
| ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk3 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk18 @ A ) ) )
=> ( sk17 @ sk18 @ A ) ) ) ),
inference(simp,[status(thm)],[17]) ).
thf(475,plain,
( ( ( ^ [A: a] :
( ( sk2 @ sk18 @ A )
| ( sk3 @ sk18 @ A ) ) )
!= ( ^ [A: a] :
( ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk2 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk18 @ A ) )
| ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk3 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk18 @ A ) ) ) ) )
| ( ( sk17 @ sk18 )
!= ( sk17 @ sk18 ) ) ),
inference(simp,[status(thm)],[263]) ).
thf(476,plain,
( ( ^ [A: a] :
( ( sk2 @ sk18 @ A )
| ( sk3 @ sk18 @ A ) ) )
!= ( ^ [A: a] :
( ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk2 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk18 @ A ) )
| ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk3 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk18 @ A ) ) ) ) ),
inference(simp,[status(thm)],[475]) ).
thf(180,plain,
( ~ ( sk8 @ sk6 @ sk7 )
| ~ ( sk8 @ sk6 @ sk7 ) ),
inference(cnfConj,[status(thm)],[178]) ).
thf(212,plain,
~ ( sk8 @ sk6 @ sk7 ),
inference(simp,[status(thm)],[180]) ).
thf(406,plain,
( ( ( ( sk2 @ sk22 @ sk23 )
| ( sk3 @ sk22 @ sk23 ) )
=> ( sk21 @ sk22 @ sk23 ) )
| ( ( ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk2 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk22 @ sk23 ) )
| ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk3 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk22 @ sk23 ) ) )
=> ( sk21 @ sk22 @ sk23 ) ) ),
inference(bool_ext,[status(thm)],[19]) ).
thf(420,plain,
! [D: a,C: a,B: a,A: a] :
( ( ~ ( sk2 @ sk22 @ sk23 )
| ( sk21 @ sk22 @ sk23 )
| ~ ( sk2 @ A @ B )
| ( sk121 @ A @ B )
| ( sk21 @ sk22 @ sk23 ) )
& ( ~ ( sk2 @ sk22 @ sk23 )
| ( sk21 @ sk22 @ sk23 )
| ( sk1 @ sk121 )
| ( sk21 @ sk22 @ sk23 ) )
& ( ~ ( sk2 @ sk22 @ sk23 )
| ( sk21 @ sk22 @ sk23 )
| ~ ( sk121 @ sk22 @ sk23 )
| ( sk21 @ sk22 @ sk23 ) )
& ( ~ ( sk2 @ sk22 @ sk23 )
| ( sk21 @ sk22 @ sk23 )
| ~ ( sk3 @ C @ D )
| ( sk122 @ C @ D )
| ( sk21 @ sk22 @ sk23 ) )
& ( ~ ( sk2 @ sk22 @ sk23 )
| ( sk21 @ sk22 @ sk23 )
| ( sk1 @ sk122 )
| ( sk21 @ sk22 @ sk23 ) )
& ( ~ ( sk2 @ sk22 @ sk23 )
| ( sk21 @ sk22 @ sk23 )
| ~ ( sk122 @ sk22 @ sk23 )
| ( sk21 @ sk22 @ sk23 ) )
& ( ~ ( sk3 @ sk22 @ sk23 )
| ( sk21 @ sk22 @ sk23 )
| ~ ( sk2 @ A @ B )
| ( sk121 @ A @ B )
| ( sk21 @ sk22 @ sk23 ) )
& ( ~ ( sk3 @ sk22 @ sk23 )
| ( sk21 @ sk22 @ sk23 )
| ( sk1 @ sk121 )
| ( sk21 @ sk22 @ sk23 ) )
& ( ~ ( sk3 @ sk22 @ sk23 )
| ( sk21 @ sk22 @ sk23 )
| ~ ( sk121 @ sk22 @ sk23 )
| ( sk21 @ sk22 @ sk23 ) )
& ( ~ ( sk3 @ sk22 @ sk23 )
| ( sk21 @ sk22 @ sk23 )
| ~ ( sk3 @ C @ D )
| ( sk122 @ C @ D )
| ( sk21 @ sk22 @ sk23 ) )
& ( ~ ( sk3 @ sk22 @ sk23 )
| ( sk21 @ sk22 @ sk23 )
| ( sk1 @ sk122 )
| ( sk21 @ sk22 @ sk23 ) )
& ( ~ ( sk3 @ sk22 @ sk23 )
| ( sk21 @ sk22 @ sk23 )
| ~ ( sk122 @ sk22 @ sk23 )
| ( sk21 @ sk22 @ sk23 ) ) ),
inference(cnf,[status(esa)],[406]) ).
thf(421,plain,
( ~ ( sk2 @ sk22 @ sk23 )
| ( sk21 @ sk22 @ sk23 )
| ( sk1 @ sk122 )
| ( sk21 @ sk22 @ sk23 ) ),
inference(cnfConj,[status(thm)],[420]) ).
thf(433,plain,
( ~ ( sk2 @ sk22 @ sk23 )
| ( sk21 @ sk22 @ sk23 )
| ( sk1 @ sk122 ) ),
inference(simp,[status(thm)],[421]) ).
thf(405,plain,
( ~ ( ( ( sk2 @ sk22 @ sk23 )
| ( sk3 @ sk22 @ sk23 ) )
=> ( sk21 @ sk22 @ sk23 ) )
| ~ ( ( ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk2 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk22 @ sk23 ) )
| ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk3 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk22 @ sk23 ) ) )
=> ( sk21 @ sk22 @ sk23 ) ) ),
inference(bool_ext,[status(thm)],[19]) ).
thf(408,plain,
! [B: a > a > $o,A: a > a > $o] :
( ( ( sk2 @ sk22 @ sk23 )
| ( sk3 @ sk22 @ sk23 )
| ( sk2 @ ( sk117 @ A ) @ ( sk118 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk22 @ sk23 )
| ( sk3 @ ( sk119 @ B ) @ ( sk120 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk22 @ sk23 ) )
& ( ( sk2 @ sk22 @ sk23 )
| ( sk3 @ sk22 @ sk23 )
| ( sk2 @ ( sk117 @ A ) @ ( sk118 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk22 @ sk23 )
| ~ ( B @ ( sk119 @ B ) @ ( sk120 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk22 @ sk23 ) )
& ( ( sk2 @ sk22 @ sk23 )
| ( sk3 @ sk22 @ sk23 )
| ~ ( A @ ( sk117 @ A ) @ ( sk118 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk22 @ sk23 )
| ( sk3 @ ( sk119 @ B ) @ ( sk120 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk22 @ sk23 ) )
& ( ( sk2 @ sk22 @ sk23 )
| ( sk3 @ sk22 @ sk23 )
| ~ ( A @ ( sk117 @ A ) @ ( sk118 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk22 @ sk23 )
| ~ ( B @ ( sk119 @ B ) @ ( sk120 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk22 @ sk23 ) )
& ( ( sk2 @ sk22 @ sk23 )
| ( sk3 @ sk22 @ sk23 )
| ~ ( sk21 @ sk22 @ sk23 ) )
& ( ~ ( sk21 @ sk22 @ sk23 )
| ( sk2 @ ( sk117 @ A ) @ ( sk118 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk22 @ sk23 )
| ( sk3 @ ( sk119 @ B ) @ ( sk120 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk22 @ sk23 ) )
& ( ~ ( sk21 @ sk22 @ sk23 )
| ( sk2 @ ( sk117 @ A ) @ ( sk118 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk22 @ sk23 )
| ~ ( B @ ( sk119 @ B ) @ ( sk120 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk22 @ sk23 ) )
& ( ~ ( sk21 @ sk22 @ sk23 )
| ~ ( A @ ( sk117 @ A ) @ ( sk118 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk22 @ sk23 )
| ( sk3 @ ( sk119 @ B ) @ ( sk120 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk22 @ sk23 ) )
& ( ~ ( sk21 @ sk22 @ sk23 )
| ~ ( A @ ( sk117 @ A ) @ ( sk118 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk22 @ sk23 )
| ~ ( B @ ( sk119 @ B ) @ ( sk120 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk22 @ sk23 ) )
& ( ~ ( sk21 @ sk22 @ sk23 )
| ~ ( sk21 @ sk22 @ sk23 ) ) ),
inference(cnf,[status(esa)],[405]) ).
thf(411,plain,
( ~ ( sk21 @ sk22 @ sk23 )
| ~ ( sk21 @ sk22 @ sk23 ) ),
inference(cnfConj,[status(thm)],[408]) ).
thf(419,plain,
~ ( sk21 @ sk22 @ sk23 ),
inference(simp,[status(thm)],[411]) ).
thf(778,plain,
( ~ ( sk2 @ sk22 @ sk23 )
| $false
| ( sk1 @ sk122 ) ),
inference(rewrite,[status(thm)],[433,419]) ).
thf(779,plain,
( ~ ( sk2 @ sk22 @ sk23 )
| ( sk1 @ sk122 ) ),
inference(simp,[status(thm)],[778]) ).
thf(371,plain,
( ( ^ [A: a] :
! [B: a] :
( ( ( sk2 @ A @ B )
| ( sk3 @ A @ B ) )
=> ( sk11 @ A @ B ) ) )
!= ( ^ [A: a] :
! [B: a] :
( ( ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) )
| ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) )
=> ( sk11 @ A @ B ) ) ) ),
inference(simp,[status(thm)],[321]) ).
thf(513,plain,
( ~ ( sk11 @ sk107 @ sk108 )
| ( sk109 != sk107 )
| ( sk110 != sk108 ) ),
inference(simp,[status(thm)],[511]) ).
thf(34,plain,
! [D: a,C: a,B: a,A: a] :
( ~ ( sk2 @ sk32 @ sk33 )
| ( sk1 @ sk39 )
| ~ ( sk3 @ sk37 @ sk38 )
| ~ ( sk3 @ C @ D )
| ( sk40 @ B @ A @ C @ D ) ),
inference(cnfConj,[status(thm)],[28]) ).
thf(265,plain,
( ! [A: a] :
( ( ( sk2 @ sk18 @ A )
| ( sk3 @ sk18 @ A ) )
=> ( sk17 @ sk18 @ A ) )
| ! [A: a] :
( ( ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk2 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk18 @ A ) )
| ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( sk3 @ C @ D )
=> ( B @ C @ D ) )
& ( sk1 @ B ) )
=> ( B @ sk18 @ A ) ) )
=> ( sk17 @ sk18 @ A ) ) ),
inference(bool_ext,[status(thm)],[17]) ).
thf(277,plain,
! [F: a,E: a,D: a,C: a,B: a,A: a] :
( ( ~ ( sk2 @ sk18 @ A )
| ( sk17 @ sk18 @ A )
| ~ ( sk2 @ C @ D )
| ( sk95 @ B @ A @ C @ D )
| ( sk17 @ sk18 @ B ) )
& ( ~ ( sk2 @ sk18 @ A )
| ( sk17 @ sk18 @ A )
| ( sk1 @ ( sk95 @ B @ A ) )
| ( sk17 @ sk18 @ B ) )
& ( ~ ( sk2 @ sk18 @ A )
| ( sk17 @ sk18 @ A )
| ~ ( sk95 @ B @ A @ sk18 @ B )
| ( sk17 @ sk18 @ B ) )
& ( ~ ( sk2 @ sk18 @ A )
| ( sk17 @ sk18 @ A )
| ~ ( sk3 @ E @ F )
| ( sk96 @ B @ A @ E @ F )
| ( sk17 @ sk18 @ B ) )
& ( ~ ( sk2 @ sk18 @ A )
| ( sk17 @ sk18 @ A )
| ( sk1 @ ( sk96 @ B @ A ) )
| ( sk17 @ sk18 @ B ) )
& ( ~ ( sk2 @ sk18 @ A )
| ( sk17 @ sk18 @ A )
| ~ ( sk96 @ B @ A @ sk18 @ B )
| ( sk17 @ sk18 @ B ) )
& ( ~ ( sk3 @ sk18 @ A )
| ( sk17 @ sk18 @ A )
| ~ ( sk2 @ C @ D )
| ( sk95 @ B @ A @ C @ D )
| ( sk17 @ sk18 @ B ) )
& ( ~ ( sk3 @ sk18 @ A )
| ( sk17 @ sk18 @ A )
| ( sk1 @ ( sk95 @ B @ A ) )
| ( sk17 @ sk18 @ B ) )
& ( ~ ( sk3 @ sk18 @ A )
| ( sk17 @ sk18 @ A )
| ~ ( sk95 @ B @ A @ sk18 @ B )
| ( sk17 @ sk18 @ B ) )
& ( ~ ( sk3 @ sk18 @ A )
| ( sk17 @ sk18 @ A )
| ~ ( sk3 @ E @ F )
| ( sk96 @ B @ A @ E @ F )
| ( sk17 @ sk18 @ B ) )
& ( ~ ( sk3 @ sk18 @ A )
| ( sk17 @ sk18 @ A )
| ( sk1 @ ( sk96 @ B @ A ) )
| ( sk17 @ sk18 @ B ) )
& ( ~ ( sk3 @ sk18 @ A )
| ( sk17 @ sk18 @ A )
| ~ ( sk96 @ B @ A @ sk18 @ B )
| ( sk17 @ sk18 @ B ) ) ),
inference(cnf,[status(esa)],[265]) ).
thf(286,plain,
! [B: a,A: a] :
( ~ ( sk3 @ sk18 @ A )
| ( sk17 @ sk18 @ A )
| ( sk1 @ ( sk96 @ B @ A ) )
| ( sk17 @ sk18 @ B ) ),
inference(cnfConj,[status(thm)],[277]) ).
thf(576,plain,
( ( ( ^ [A: a > a > $o,B: a,C: a] :
( ( sk2 @ B @ C )
| ( sk3 @ B @ C ) ) )
!= ( ^ [A: a > a > $o,B: a,C: a] :
( ! [D: a > a > $o] :
( ( ! [E: a,F: a] :
( ( sk2 @ E @ F )
=> ( D @ E @ F ) )
& ( sk1 @ D ) )
=> ( D @ B @ C ) )
| ! [D: a > a > $o] :
( ( ! [E: a,F: a] :
( ( sk3 @ E @ F )
=> ( D @ E @ F ) )
& ( sk1 @ D ) )
=> ( D @ B @ C ) ) ) ) )
| ( ( ^ [A: a > a > $o] : A )
!= ( ^ [A: a > a > $o] : A ) ) ),
inference(simp,[status(thm)],[565]) ).
thf(577,plain,
( ( ^ [A: a > a > $o,B: a,C: a] :
( ( sk2 @ B @ C )
| ( sk3 @ B @ C ) ) )
!= ( ^ [A: a > a > $o,B: a,C: a] :
( ! [D: a > a > $o] :
( ( ! [E: a,F: a] :
( ( sk2 @ E @ F )
=> ( D @ E @ F ) )
& ( sk1 @ D ) )
=> ( D @ B @ C ) )
| ! [D: a > a > $o] :
( ( ! [E: a,F: a] :
( ( sk3 @ E @ F )
=> ( D @ E @ F ) )
& ( sk1 @ D ) )
=> ( D @ B @ C ) ) ) ) ),
inference(simp,[status(thm)],[576]) ).
thf(71,plain,
! [D: a,C: a,B: a,A: a] :
( ( sk1 @ sk51 )
| ( sk1 @ ( sk54 @ D @ C @ B @ A ) )
| ( sk52 @ B @ A @ C @ D ) ),
inference(cnfConj,[status(thm)],[60]) ).
thf(571,plain,
( ~ ( sk8 @ sk139 @ sk142 )
| ( sk139 != sk139 )
| ( sk143 != sk142 ) ),
inference(simp,[status(thm)],[569]) ).
thf(572,plain,
( ~ ( sk8 @ sk139 @ sk142 )
| ( sk143 != sk142 ) ),
inference(simp,[status(thm)],[571]) ).
thf(86,plain,
! [B: a,A: a] :
( ( sk1 @ sk51 )
| ( sk1 @ ( sk52 @ B @ A ) ) ),
inference(cnfConj,[status(thm)],[60]) ).
thf(245,plain,
( ~ ( sk2 @ sk27 @ sk28 )
| ~ ( sk84 @ sk27 @ sk28 ) ),
inference(cnfConj,[status(thm)],[243]) ).
thf(451,plain,
( ~ ( sk2 @ sk22 @ sk23 )
| ( sk1 @ sk124 ) ),
inference(cnfConj,[status(thm)],[450]) ).
thf(481,plain,
( ~ ! [A: a,B: a] :
( ( ( sk2 @ A @ B )
| ( sk3 @ A @ B ) )
=> ( sk8 @ A @ B ) )
| ~ ! [A: a,B: a] :
( ( ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) )
| ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) )
=> ( sk8 @ A @ B ) ) ),
inference(bool_ext,[status(thm)],[479]) ).
thf(483,plain,
! [B: a > a > $o,A: a > a > $o] :
( ( ( sk2 @ sk129 @ sk130 )
| ( sk3 @ sk129 @ sk130 )
| ( sk2 @ ( sk133 @ A ) @ ( sk134 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk131 @ sk132 )
| ( sk3 @ ( sk135 @ B ) @ ( sk136 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk131 @ sk132 ) )
& ( ( sk2 @ sk129 @ sk130 )
| ( sk3 @ sk129 @ sk130 )
| ( sk2 @ ( sk133 @ A ) @ ( sk134 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk131 @ sk132 )
| ~ ( B @ ( sk135 @ B ) @ ( sk136 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk131 @ sk132 ) )
& ( ( sk2 @ sk129 @ sk130 )
| ( sk3 @ sk129 @ sk130 )
| ~ ( A @ ( sk133 @ A ) @ ( sk134 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk131 @ sk132 )
| ( sk3 @ ( sk135 @ B ) @ ( sk136 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk131 @ sk132 ) )
& ( ( sk2 @ sk129 @ sk130 )
| ( sk3 @ sk129 @ sk130 )
| ~ ( A @ ( sk133 @ A ) @ ( sk134 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk131 @ sk132 )
| ~ ( B @ ( sk135 @ B ) @ ( sk136 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk131 @ sk132 ) )
& ( ( sk2 @ sk129 @ sk130 )
| ( sk3 @ sk129 @ sk130 )
| ~ ( sk8 @ sk131 @ sk132 ) )
& ( ~ ( sk8 @ sk129 @ sk130 )
| ( sk2 @ ( sk133 @ A ) @ ( sk134 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk131 @ sk132 )
| ( sk3 @ ( sk135 @ B ) @ ( sk136 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk131 @ sk132 ) )
& ( ~ ( sk8 @ sk129 @ sk130 )
| ( sk2 @ ( sk133 @ A ) @ ( sk134 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk131 @ sk132 )
| ~ ( B @ ( sk135 @ B ) @ ( sk136 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk131 @ sk132 ) )
& ( ~ ( sk8 @ sk129 @ sk130 )
| ~ ( A @ ( sk133 @ A ) @ ( sk134 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk131 @ sk132 )
| ( sk3 @ ( sk135 @ B ) @ ( sk136 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk131 @ sk132 ) )
& ( ~ ( sk8 @ sk129 @ sk130 )
| ~ ( A @ ( sk133 @ A ) @ ( sk134 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk131 @ sk132 )
| ~ ( B @ ( sk135 @ B ) @ ( sk136 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk131 @ sk132 ) )
& ( ~ ( sk8 @ sk129 @ sk130 )
| ~ ( sk8 @ sk131 @ sk132 ) ) ),
inference(cnf,[status(esa)],[481]) ).
thf(486,plain,
( ~ ( sk8 @ sk129 @ sk130 )
| ~ ( sk8 @ sk131 @ sk132 ) ),
inference(cnfConj,[status(thm)],[483]) ).
thf(566,plain,
( ~ ( sk8 @ sk129 @ sk130 )
| ( ( sk8 @ sk131 @ sk132 )
!= ( sk8 @ sk129 @ sk130 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[486]) ).
thf(567,plain,
( ~ ( sk8 @ sk129 @ sk130 )
| ( ( sk8 @ sk131 @ sk132 )
!= ( sk8 @ sk129 @ sk130 ) ) ),
inference(simp,[status(thm)],[566]) ).
thf(668,plain,
( ~ ( sk2 @ sk140 @ sk141 )
| ( sk1 @ sk156 ) ),
inference(cnfConj,[status(thm)],[660]) ).
thf(462,plain,
( ~ ( sk2 @ sk22 @ sk23 )
| ~ ( sk123 @ sk22 @ sk23 ) ),
inference(cnfConj,[status(thm)],[450]) ).
thf(35,plain,
! [B: a,A: a] :
( ~ ( sk2 @ sk32 @ sk33 )
| ( sk1 @ sk39 )
| ~ ( sk3 @ sk37 @ sk38 )
| ~ ( sk40 @ B @ A @ sk37 @ sk38 ) ),
inference(cnfConj,[status(thm)],[28]) ).
thf(472,plain,
( ~ ( sk17 @ sk18 @ sk89 )
| ( sk18 != sk18 )
| ( sk90 != sk89 ) ),
inference(simp,[status(thm)],[470]) ).
thf(473,plain,
( ~ ( sk17 @ sk18 @ sk89 )
| ( sk90 != sk89 ) ),
inference(simp,[status(thm)],[472]) ).
thf(663,plain,
( ~ ( sk3 @ sk140 @ sk141 )
| ( sk1 @ sk156 ) ),
inference(cnfConj,[status(thm)],[660]) ).
thf(255,plain,
( ~ ( sk2 @ sk27 @ sk28 )
| ~ ( sk83 @ sk27 @ sk28 ) ),
inference(cnfConj,[status(thm)],[243]) ).
thf(458,plain,
( ~ ( sk3 @ sk22 @ sk23 )
| ~ ( sk123 @ sk22 @ sk23 ) ),
inference(cnfConj,[status(thm)],[450]) ).
thf(282,plain,
! [B: a,A: a] :
( ~ ( sk2 @ sk18 @ A )
| ( sk17 @ sk18 @ A )
| ( sk1 @ ( sk95 @ B @ A ) )
| ( sk17 @ sk18 @ B ) ),
inference(cnfConj,[status(thm)],[277]) ).
thf(72,plain,
! [B: a,A: a] :
( ~ ( sk51 @ sk4 @ sk5 )
| ( sk1 @ ( sk52 @ B @ A ) ) ),
inference(cnfConj,[status(thm)],[60]) ).
thf(143,plain,
( ~ ( sk14 @ sk63 @ sk64 )
| ( sk65 != sk63 )
| ( sk66 != sk64 ) ),
inference(simp,[status(thm)],[141]) ).
thf(250,plain,
( ~ ( sk3 @ sk27 @ sk28 )
| ( sk1 @ sk84 ) ),
inference(cnfConj,[status(thm)],[243]) ).
thf(652,plain,
( ~ ( sk11 @ sk97 @ sk98 )
| ( sk99 != sk97 )
| ( sk100 != sk98 ) ),
inference(simp,[status(thm)],[650]) ).
thf(138,plain,
( ( ( ^ [A: a,B: a] :
( ( sk2 @ A @ B )
| ( sk3 @ A @ B ) ) )
!= ( ^ [A: a,B: a] :
( ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) )
| ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) ) ) )
| ( sk14 != sk14 ) ),
inference(simp,[status(thm)],[137]) ).
thf(139,plain,
( ( ^ [A: a,B: a] :
( ( sk2 @ A @ B )
| ( sk3 @ A @ B ) ) )
!= ( ^ [A: a,B: a] :
( ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) )
| ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) ) ) ),
inference(simp,[status(thm)],[138]) ).
thf(431,plain,
( ~ ( sk3 @ sk22 @ sk23 )
| ( sk21 @ sk22 @ sk23 )
| ( sk1 @ sk121 )
| ( sk21 @ sk22 @ sk23 ) ),
inference(cnfConj,[status(thm)],[420]) ).
thf(436,plain,
( ~ ( sk3 @ sk22 @ sk23 )
| ( sk21 @ sk22 @ sk23 )
| ( sk1 @ sk121 ) ),
inference(simp,[status(thm)],[431]) ).
thf(780,plain,
( ~ ( sk3 @ sk22 @ sk23 )
| $false
| ( sk1 @ sk121 ) ),
inference(rewrite,[status(thm)],[436,419]) ).
thf(781,plain,
( ~ ( sk3 @ sk22 @ sk23 )
| ( sk1 @ sk121 ) ),
inference(simp,[status(thm)],[780]) ).
thf(568,plain,
( ~ ( sk8 @ sk129 @ sk130 )
| ( sk131 != sk129 )
| ( sk132 != sk130 ) ),
inference(simp,[status(thm)],[566]) ).
thf(246,plain,
( ~ ( sk2 @ sk27 @ sk28 )
| ( sk1 @ sk83 ) ),
inference(cnfConj,[status(thm)],[243]) ).
thf(667,plain,
( ~ ( sk2 @ sk140 @ sk141 )
| ~ ( sk157 @ sk140 @ sk141 ) ),
inference(cnfConj,[status(thm)],[660]) ).
thf(287,plain,
! [B: a,A: a] :
( ~ ( sk3 @ sk18 @ A )
| ( sk17 @ sk18 @ A )
| ( sk1 @ ( sk95 @ B @ A ) )
| ( sk17 @ sk18 @ B ) ),
inference(cnfConj,[status(thm)],[277]) ).
thf(144,plain,
! [B: a,A: a] :
( ( sk1 @ sk51 )
| ( ( sk1 @ ( sk52 @ B @ A ) )
!= ( sk1 @ sk51 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[86]) ).
thf(146,plain,
! [B: a,A: a] :
( ( sk1 @ sk51 )
| ( ( sk52 @ B @ A )
!= sk51 ) ),
inference(simp,[status(thm)],[144]) ).
thf(30,plain,
! [B: a,A: a] :
( ~ ( sk2 @ sk32 @ sk33 )
| ( sk1 @ sk39 )
| ~ ( sk3 @ sk37 @ sk38 )
| ( sk1 @ ( sk40 @ B @ A ) ) ),
inference(cnfConj,[status(thm)],[28]) ).
thf(664,plain,
( ~ ( sk2 @ sk140 @ sk141 )
| ( sk1 @ sk157 ) ),
inference(cnfConj,[status(thm)],[660]) ).
thf(400,plain,
( ( ^ [A: a,B: a] :
( ( ( sk2 @ A @ B )
| ( sk3 @ A @ B ) )
=> ( sk11 @ A @ B ) ) )
!= ( ^ [A: a,B: a] :
( ( ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) )
| ! [C: a > a > $o] :
( ( ! [D: a,E: a] :
( ( sk3 @ D @ E )
=> ( C @ D @ E ) )
& ( sk1 @ C ) )
=> ( C @ A @ B ) ) )
=> ( sk11 @ A @ B ) ) ) ),
inference(simp,[status(thm)],[371]) ).
thf(582,plain,
( ~ ( ( ( sk2 @ sk140 @ sk141 )
| ( sk3 @ sk140 @ sk141 ) )
=> ( sk8 @ sk140 @ sk141 ) )
| ~ ( ( ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk2 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk140 @ sk141 ) )
| ! [A: a > a > $o] :
( ( ! [B: a,C: a] :
( ( sk3 @ B @ C )
=> ( A @ B @ C ) )
& ( sk1 @ A ) )
=> ( A @ sk140 @ sk141 ) ) )
=> ( sk8 @ sk140 @ sk141 ) ) ),
inference(bool_ext,[status(thm)],[519]) ).
thf(585,plain,
! [B: a > a > $o,A: a > a > $o] :
( ( ( sk2 @ sk140 @ sk141 )
| ( sk3 @ sk140 @ sk141 )
| ( sk2 @ ( sk150 @ A ) @ ( sk151 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk140 @ sk141 )
| ( sk3 @ ( sk152 @ B ) @ ( sk153 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk140 @ sk141 ) )
& ( ( sk2 @ sk140 @ sk141 )
| ( sk3 @ sk140 @ sk141 )
| ( sk2 @ ( sk150 @ A ) @ ( sk151 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk140 @ sk141 )
| ~ ( B @ ( sk152 @ B ) @ ( sk153 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk140 @ sk141 ) )
& ( ( sk2 @ sk140 @ sk141 )
| ( sk3 @ sk140 @ sk141 )
| ~ ( A @ ( sk150 @ A ) @ ( sk151 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk140 @ sk141 )
| ( sk3 @ ( sk152 @ B ) @ ( sk153 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk140 @ sk141 ) )
& ( ( sk2 @ sk140 @ sk141 )
| ( sk3 @ sk140 @ sk141 )
| ~ ( A @ ( sk150 @ A ) @ ( sk151 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk140 @ sk141 )
| ~ ( B @ ( sk152 @ B ) @ ( sk153 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk140 @ sk141 ) )
& ( ( sk2 @ sk140 @ sk141 )
| ( sk3 @ sk140 @ sk141 )
| ~ ( sk8 @ sk140 @ sk141 ) )
& ( ~ ( sk8 @ sk140 @ sk141 )
| ( sk2 @ ( sk150 @ A ) @ ( sk151 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk140 @ sk141 )
| ( sk3 @ ( sk152 @ B ) @ ( sk153 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk140 @ sk141 ) )
& ( ~ ( sk8 @ sk140 @ sk141 )
| ( sk2 @ ( sk150 @ A ) @ ( sk151 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk140 @ sk141 )
| ~ ( B @ ( sk152 @ B ) @ ( sk153 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk140 @ sk141 ) )
& ( ~ ( sk8 @ sk140 @ sk141 )
| ~ ( A @ ( sk150 @ A ) @ ( sk151 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk140 @ sk141 )
| ( sk3 @ ( sk152 @ B ) @ ( sk153 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk140 @ sk141 ) )
& ( ~ ( sk8 @ sk140 @ sk141 )
| ~ ( A @ ( sk150 @ A ) @ ( sk151 @ A ) )
| ~ ( sk1 @ A )
| ( A @ sk140 @ sk141 )
| ~ ( B @ ( sk152 @ B ) @ ( sk153 @ B ) )
| ~ ( sk1 @ B )
| ( B @ sk140 @ sk141 ) )
& ( ~ ( sk8 @ sk140 @ sk141 )
| ~ ( sk8 @ sk140 @ sk141 ) ) ),
inference(cnf,[status(esa)],[582]) ).
thf(587,plain,
( ~ ( sk8 @ sk140 @ sk141 )
| ~ ( sk8 @ sk140 @ sk141 ) ),
inference(cnfConj,[status(thm)],[585]) ).
thf(596,plain,
~ ( sk8 @ sk140 @ sk141 ),
inference(simp,[status(thm)],[587]) ).
thf(459,plain,
( ~ ( sk2 @ sk22 @ sk23 )
| ( sk1 @ sk123 ) ),
inference(cnfConj,[status(thm)],[450]) ).
thf(83,plain,
! [B: a,A: a] :
( ( sk1 @ sk51 )
| ~ ( sk52 @ B @ A @ sk4 @ sk5 ) ),
inference(cnfConj,[status(thm)],[60]) ).
thf(454,plain,
( ~ ( sk3 @ sk22 @ sk23 )
| ~ ( sk124 @ sk22 @ sk23 ) ),
inference(cnfConj,[status(thm)],[450]) ).
thf(8264,plain,
$false,
inference(e,[status(thm)],[662,16,479,249,666,5,247,10,384,142,565,651,14,570,559,20,57,321,121,480,248,512,661,452,6,561,407,33,21,137,252,65,665,461,551,456,471,476,212,13,779,371,513,34,17,584,22,286,577,71,572,86,419,7,245,451,567,509,649,213,668,108,462,521,563,3,35,473,663,255,458,525,282,263,72,143,250,368,652,139,781,23,568,246,510,667,287,146,30,273,564,664,400,596,459,15,486,83,454]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV119^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.09/0.22 % Computer : n026.cluster.edu
% 0.09/0.22 % Model : x86_64 x86_64
% 0.09/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.22 % Memory : 8046.5625MB
% 0.09/0.22 % OS : Linux 6.8.0-71-generic
% 0.09/0.22 % CPULimit : 300
% 0.09/0.22 % WCLimit : 300
% 0.09/0.22 % DateTime : Tue Sep 29 15:14:27 UTC 2026
% 0.09/0.22 % CPUTime :
% 0.09/0.22 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 1.03/0.81 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.20/0.99 % [INFO] Parsing done (176ms).
% 1.20/1.00 % [INFO] Running in sequential loop mode.
% 1.96/1.40 % [INFO] eprover registered as external prover.
% 1.96/1.41 % [INFO] Scanning for conjecture ...
% 2.15/1.51 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 2.15/1.55 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 2.15/1.55 % [INFO] Problem is higher-order (TPTP THF).
% 2.15/1.56 % [INFO] Type checking passed.
% 2.15/1.56 % [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 ...
% 249.12/125.90 % External prover 'e' found a proof!
% 249.12/125.90 % [INFO] Killing All external provers ...
% 249.12/125.90 % Time passed: 125538ms (effective reasoning time: 124890ms)
% 249.12/125.90 % 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)>
% 249.12/125.90 % Axioms used in derivation (0):
% 249.12/125.90 % No. of inferences in proof: 184
% 249.12/125.90 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 125538 ms resp. 124890 ms w/o parsing
% 249.92/126.19 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 249.92/126.20 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------