%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SEV116^5 : TPTP v9.3.1. Bugfixed v5.2.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 : n008.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 93.78s 18.88s
% Output : Refutation 95.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 9
% Syntax : Number of formulae : 264 ( 46 unt; 0 typ; 8 def)
% Number of atoms : 1197 ( 271 equ; 0 cnn)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 2902 ( 611 ~; 468 |; 70 &;1708 @)
% ( 0 <=>; 45 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 6 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 229 ( 229 >; 0 *; 0 +; 0 <<)
% Number of symbols : 32 ( 29 usr; 22 con; 0-3 aty)
% Number of variables : 580 ( 471 ^; 102 !; 0 ?; 580 :)
% ( 0 !>; 0 ?*; 0 @-; 7 @+)
% Comments :
%------------------------------------------------------------------------------
thf(cS_decl,type,
cS: ( $i > $i > $o ) > $o ).
thf(x_decl,type,
x: $i ).
thf(y_decl,type,
y: $i ).
thf(cSTRANGE_HO_ABBR_decl,type,
cSTRANGE_HO_ABBR: ( ( $i > $i > $o ) > $o ) > $i > $i > $o ).
thf(sk1_decl,type,
sk1: $i > $i > $o ).
thf(sk2_decl,type,
sk2: $i > $i > $o ).
thf(sk3_decl,type,
sk3: $i ).
thf(sk4_decl,type,
sk4: $i ).
thf(sk5_decl,type,
sk5: $i ).
thf(sk6_decl,type,
sk6: $i ).
thf(sk8_decl,type,
sk8: $i > $i > $o ).
thf(sk9_decl,type,
sk9: $i > $i > $o ).
thf(sk76_decl,type,
sk76: $i ).
thf(sk77_decl,type,
sk77: $i ).
thf(sk80_decl,type,
sk80: $i ).
thf(sk81_decl,type,
sk81: $i ).
thf(sk97_decl,type,
sk97: $i ).
thf(sk98_decl,type,
sk98: $i ).
thf(sk99_decl,type,
sk99: $i ).
thf(sk100_decl,type,
sk100: $i ).
thf(sk106_decl,type,
sk106: $i ).
thf(sk107_decl,type,
sk107: $i ).
thf(sk108_decl,type,
sk108: $i ).
thf(sk109_decl,type,
sk109: $i ).
thf(sk110_decl,type,
sk110: $i ).
thf(sk111_decl,type,
sk111: $i ).
thf(sk120_decl,type,
sk120: $i > $i > $o ).
thf(sk169_decl,type,
sk169: $i > $i > $o ).
thf(sk244_decl,type,
sk244: $i > $i > $o ).
thf(cSTRANGE_HO_ABBR_def,definition,
( cSTRANGE_HO_ABBR
= ( ^ [A: ( $i > $i > $o ) > $o,B: $i,C: $i] :
! [D: $i > $i > $o] :
( ( ( A @ D )
& ( D @ B @ C ) )
=> ( D @ C @ B ) ) ) ) ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i > $i > $o] :
~ ( ( ( cS @ A )
& ( A @ y @ x ) )
=> ( A @ x @ y ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: $i > $i > $o] :
~ ( ( ( cS @ A )
& ( A @ x @ y ) )
=> ( A @ y @ x ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( @+[A: $i > $i > $o] :
~ ( ( ( cS @ A )
& ( A @ sk5 @ sk6 ) )
=> ( A @ sk6 @ sk5 ) ) ) ) ).
thf(sk9_def,definition,
( sk9
= ( @+[A: $i > $i > $o] :
~ ( ( ( cS @ A )
& ( A @ sk5 @ sk6 ) )
=> ( A @ sk6 @ sk5 ) ) ) ) ).
thf(sk120_def,definition,
( sk120
= ( @+[A: $i > $i > $o] :
~ ( ( ( cS @ A )
& ( A @ sk106 @ sk107 ) )
=> ( A @ sk107 @ sk106 ) ) ) ) ).
thf(sk169_def,definition,
( sk169
= ( @+[A: $i > $i > $o] :
~ ( ( ( cS @ A )
& ( A @ sk108 @ sk109 ) )
=> ( A @ sk109 @ sk108 ) ) ) ) ).
thf(sk244_def,definition,
( sk244
= ( @+[A: $i > $i > $o] :
~ ( ( ( cS @ A )
& ( A @ sk110 @ sk111 ) )
=> ( A @ sk111 @ sk110 ) ) ) ) ).
thf(1,conjecture,
( ( ( cS @ ( cSTRANGE_HO_ABBR @ cS ) )
& ( cSTRANGE_HO_ABBR @ cS @ x @ y ) )
=> ( cSTRANGE_HO_ABBR @ cS @ y @ x ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cSTRANGE_HO_EXAMPLE) ).
thf(2,negated_conjecture,
~ ( ( ( cS @ ( cSTRANGE_HO_ABBR @ cS ) )
& ( cSTRANGE_HO_ABBR @ cS @ x @ y ) )
=> ( cSTRANGE_HO_ABBR @ cS @ y @ x ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(3,plain,
~ ( ( ( cS
@ ^ [A: $i,B: $i] :
! [C: $i > $i > $o] :
( ( ( cS @ C )
& ( C @ A @ B ) )
=> ( C @ B @ A ) ) )
& ! [A: $i > $i > $o] :
( ( ( cS @ A )
& ( A @ x @ y ) )
=> ( A @ y @ x ) ) )
=> ! [A: $i > $i > $o] :
( ( ( cS @ A )
& ( A @ y @ x ) )
=> ( A @ x @ y ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(4,plain,
! [A: $i > $i > $o] :
( ( cS
@ ^ [B: $i,C: $i] :
! [D: $i > $i > $o] :
( ( ( cS @ D )
& ( D @ B @ C ) )
=> ( D @ C @ B ) ) )
& ( ~ ( cS @ A )
| ~ ( A @ x @ y )
| ( A @ y @ x ) )
& ( cS @ sk1 )
& ( sk1 @ y @ x )
& ~ ( sk1 @ x @ y ) ),
inference(cnf,[status(esa)],[3]) ).
thf(9,plain,
cS @ sk1,
inference(cnfConj,[status(thm)],[4]) ).
thf(8,plain,
sk1 @ y @ x,
inference(cnfConj,[status(thm)],[4]) ).
thf(5,plain,
! [A: $i > $i > $o] :
( ~ ( cS @ A )
| ~ ( A @ x @ y )
| ( A @ y @ x ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(32,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( ~ ( cS
@ ^ [C: $i,D: $i] :
( ( A @ C @ D )
| ( B @ C @ D ) ) )
| ~ ( ( A @ x @ y )
| ( B @ x @ y ) )
| ( A @ y @ x )
| ( B @ y @ x ) ),
inference(prim_subst,[status(thm)],[5:[bind(A,$thf( ^ [D: $i] : ^ [E: $i] : ( ( B @ D @ E ) | ( C @ D @ E ) ) ))]]) ).
thf(50,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( ( ~ ( cS
@ ^ [C: $i,D: $i] :
( ( A @ C @ D )
| ( B @ C @ D ) ) )
| ~ ( A @ x @ y )
| ( A @ y @ x )
| ( B @ y @ x ) )
& ( ~ ( cS
@ ^ [C: $i,D: $i] :
( ( A @ C @ D )
| ( B @ C @ D ) ) )
| ~ ( B @ x @ y )
| ( A @ y @ x )
| ( B @ y @ x ) ) ),
inference(cnf,[status(esa)],[32]) ).
thf(51,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( ~ ( cS
@ ^ [C: $i,D: $i] :
( ( A @ C @ D )
| ( B @ C @ D ) ) )
| ~ ( A @ x @ y )
| ( A @ y @ x )
| ( B @ y @ x ) ),
inference(cnfConj,[status(thm)],[50]) ).
thf(53,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( ~ ( cS
@ ^ [C: $i,D: $i] :
( ( A @ C @ D )
| ( B @ C @ D ) ) )
| ~ ( A @ x @ y )
| ( A @ y @ x )
| ( B @ y @ x ) ),
inference(simp,[status(thm)],[51]) ).
thf(2491,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( ~ ( cS
@ ^ [C: $i,D: $i] :
( ( A @ C @ D )
| ( B @ C @ D ) ) )
| ~ $true
| ( A @ y @ x )
| ( B @ y @ x )
| ( ( sk1 @ y @ x )
!= ( A @ x @ y ) ) ),
inference(paramod_ordered,[status(thm)],[8,53]) ).
thf(2492,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( ~ ( cS
@ ^ [C: $i,D: $i] :
( ( A @ C @ D )
| ( B @ C @ D ) ) )
| ( A @ y @ x )
| ( B @ y @ x )
| ( ( sk1 @ y @ x )
!= ( A @ x @ y ) ) ),
inference(simp,[status(thm)],[2491]) ).
thf(2611,plain,
! [A: $i > $i > $o] :
( ~ ( cS
@ ^ [B: $i,C: $i] :
( ( sk1 @ C @ B )
| ( A @ B @ C ) ) )
| ( sk1 @ x @ y )
| ( A @ y @ x ) ),
inference(pre_uni,[status(thm)],[2492:[bind(A,$thf( ^ [C: $i] : ^ [D: $i] : ( sk1 @ D @ C ) )),bind(B,$thf( B ))]]) ).
thf(2775,plain,
! [A: $i > $i > $o] :
( ~ ( cS
@ ^ [B: $i,C: $i] :
( ( sk1 @ C @ B )
| ( A @ B @ C ) ) )
| ( sk1 @ x @ y )
| ( A @ y @ x ) ),
inference(simp,[status(thm)],[2611]) ).
thf(6,plain,
~ ( sk1 @ x @ y ),
inference(cnfConj,[status(thm)],[4]) ).
thf(4824,plain,
! [A: $i > $i > $o] :
( ~ ( cS
@ ^ [B: $i,C: $i] :
( ( sk1 @ C @ B )
| ( A @ B @ C ) ) )
| $false
| ( A @ y @ x ) ),
inference(rewrite,[status(thm)],[2775,6]) ).
thf(4825,plain,
! [A: $i > $i > $o] :
( ~ ( cS
@ ^ [B: $i,C: $i] :
( ( sk1 @ C @ B )
| ( A @ B @ C ) ) )
| ( A @ y @ x ) ),
inference(simp,[status(thm)],[4824]) ).
thf(4879,plain,
! [A: $i > $i > $o] :
( ~ ( cS
@ ^ [B: $i,C: $i] :
( ( sk1 @ C @ B )
| ( A @ B @ C ) ) )
| ~ $true
| ( ( A @ y @ x )
!= ( sk1 @ x @ y ) ) ),
inference(paramod_ordered,[status(thm)],[4825,6]) ).
thf(4880,plain,
! [A: $i > $i > $o] :
( ~ ( cS
@ ^ [B: $i,C: $i] :
( ( sk1 @ C @ B )
| ( A @ B @ C ) ) )
| ( ( A @ y @ x )
!= ( sk1 @ x @ y ) ) ),
inference(simp,[status(thm)],[4879]) ).
thf(5095,plain,
~ ( cS
@ ^ [A: $i,B: $i] :
( ( sk1 @ B @ A )
| ( sk1 @ x @ A ) ) ),
inference(pre_uni,[status(thm)],[4880:[bind(A,$thf( ^ [B: $i] : ^ [C: $i] : ( sk1 @ x @ B ) ))]]) ).
thf(5375,plain,
( ~ $true
| ( ( cS @ sk1 )
!= ( cS
@ ^ [A: $i,B: $i] :
( ( sk1 @ B @ A )
| ( sk1 @ x @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,5095]) ).
thf(5376,plain,
( ( cS @ sk1 )
!= ( cS
@ ^ [A: $i,B: $i] :
( ( sk1 @ B @ A )
| ( sk1 @ x @ A ) ) ) ),
inference(simp,[status(thm)],[5375]) ).
thf(5397,plain,
( sk1
!= ( ^ [A: $i,B: $i] :
( ( sk1 @ B @ A )
| ( sk1 @ x @ A ) ) ) ),
inference(simp,[status(thm)],[5376]) ).
thf(5403,plain,
( ( sk1 @ sk99 @ sk100 )
!= ( ( sk1 @ sk100 @ sk99 )
| ( sk1 @ x @ sk99 ) ) ),
inference(func_ext,[status(esa)],[5397]) ).
thf(6734,plain,
( ~ ( sk1 @ sk99 @ sk100 )
| ~ ( ( sk1 @ sk100 @ sk99 )
| ( sk1 @ x @ sk99 ) ) ),
inference(bool_ext,[status(thm)],[5403]) ).
thf(6978,plain,
( ( ~ ( sk1 @ sk99 @ sk100 )
| ~ ( sk1 @ sk100 @ sk99 ) )
& ( ~ ( sk1 @ sk99 @ sk100 )
| ~ ( sk1 @ x @ sk99 ) ) ),
inference(cnf,[status(esa)],[6734]) ).
thf(6979,plain,
( ~ ( sk1 @ sk99 @ sk100 )
| ~ ( sk1 @ sk100 @ sk99 ) ),
inference(cnfConj,[status(thm)],[6978]) ).
thf(10,plain,
( ~ $true
| ( ( sk1 @ y @ x )
!= ( sk1 @ x @ y ) ) ),
inference(paramod_ordered,[status(thm)],[8,6]) ).
thf(11,plain,
( ( sk1 @ y @ x )
!= ( sk1 @ x @ y ) ),
inference(simp,[status(thm)],[10]) ).
thf(12,plain,
( ( y != x )
| ( y != x ) ),
inference(simp,[status(thm)],[11]) ).
thf(13,plain,
y != x,
inference(simp,[status(thm)],[12]) ).
thf(5094,plain,
~ ( cS
@ ^ [A: $i,B: $i] :
( ( sk1 @ B @ A )
| ( sk1 @ B @ y ) ) ),
inference(pre_uni,[status(thm)],[4880:[bind(A,$thf( ^ [B: $i] : ^ [C: $i] : ( sk1 @ C @ y ) ))]]) ).
thf(5166,plain,
( ~ $true
| ( ( cS @ sk1 )
!= ( cS
@ ^ [A: $i,B: $i] :
( ( sk1 @ B @ A )
| ( sk1 @ B @ y ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,5094]) ).
thf(5167,plain,
( ( cS @ sk1 )
!= ( cS
@ ^ [A: $i,B: $i] :
( ( sk1 @ B @ A )
| ( sk1 @ B @ y ) ) ) ),
inference(simp,[status(thm)],[5166]) ).
thf(5192,plain,
( sk1
!= ( ^ [A: $i,B: $i] :
( ( sk1 @ B @ A )
| ( sk1 @ B @ y ) ) ) ),
inference(simp,[status(thm)],[5167]) ).
thf(5402,plain,
( ( sk1 @ sk97 @ sk98 )
!= ( ( sk1 @ sk98 @ sk97 )
| ( sk1 @ sk98 @ y ) ) ),
inference(func_ext,[status(esa)],[5192]) ).
thf(6410,plain,
( ~ ( sk1 @ sk97 @ sk98 )
| ~ ( ( sk1 @ sk98 @ sk97 )
| ( sk1 @ sk98 @ y ) ) ),
inference(bool_ext,[status(thm)],[5402]) ).
thf(6617,plain,
( ( ~ ( sk1 @ sk97 @ sk98 )
| ~ ( sk1 @ sk98 @ sk97 ) )
& ( ~ ( sk1 @ sk97 @ sk98 )
| ~ ( sk1 @ sk98 @ y ) ) ),
inference(cnf,[status(esa)],[6410]) ).
thf(6618,plain,
( ~ ( sk1 @ sk97 @ sk98 )
| ~ ( sk1 @ sk98 @ sk97 ) ),
inference(cnfConj,[status(thm)],[6617]) ).
thf(7851,plain,
( ~ ( sk1 @ sk97 @ sk98 )
| ( ( sk1 @ sk98 @ sk97 )
!= ( sk1 @ sk97 @ sk98 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[6618]) ).
thf(7890,plain,
( ~ ( sk1 @ sk97 @ sk98 )
| ( sk98 != sk97 )
| ( sk98 != sk97 ) ),
inference(simp,[status(thm)],[7851]) ).
thf(7896,plain,
( ~ ( sk1 @ sk97 @ sk98 )
| ( sk98 != sk97 ) ),
inference(simp,[status(thm)],[7890]) ).
thf(18,plain,
! [A: $i > $i > $o] :
( ~ ( cS @ A )
| ~ ( A @ x @ y )
| ~ $true
| ( ( A @ y @ x )
!= ( sk1 @ x @ y ) ) ),
inference(paramod_ordered,[status(thm)],[5,6]) ).
thf(19,plain,
! [A: $i > $i > $o] :
( ~ ( cS @ A )
| ~ ( A @ x @ y )
| ( ( A @ y @ x )
!= ( sk1 @ x @ y ) ) ),
inference(simp,[status(thm)],[18]) ).
thf(48,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ x @ A ) )
| ~ ( sk1 @ x @ x ) ),
inference(pre_uni,[status(thm)],[19:[bind(A,$thf( ^ [B: $i] : ^ [C: $i] : ( sk1 @ x @ B ) ))]]) ).
thf(7,plain,
( cS
@ ^ [A: $i,B: $i] :
! [C: $i > $i > $o] :
( ( ( cS @ C )
& ( C @ A @ B ) )
=> ( C @ B @ A ) ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(30,plain,
! [A: $i > $i > $o] :
( ~ ( cS
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
| ~ ~ ( A @ x @ y )
| ~ ( A @ y @ x ) ),
inference(prim_subst,[status(thm)],[5:[bind(A,$thf( ^ [C: $i] : ^ [D: $i] : ~ ( B @ C @ D ) ))]]) ).
thf(57,plain,
! [A: $i > $i > $o] :
( ~ ( cS
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
| ( A @ x @ y )
| ~ ( A @ y @ x ) ),
inference(cnf,[status(esa)],[30]) ).
thf(58,plain,
! [A: $i > $i > $o] :
( ~ ( cS
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
| ( A @ x @ y )
| ~ ( A @ y @ x ) ),
inference(simp,[status(thm)],[57]) ).
thf(5271,plain,
! [A: $i > $i > $o] :
( ~ ( cS
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
| ( A @ x @ y )
| ~ $true
| ( ( sk1 @ y @ x )
!= ( A @ y @ x ) ) ),
inference(paramod_ordered,[status(thm)],[8,58]) ).
thf(5272,plain,
! [A: $i > $i > $o] :
( ~ ( cS
@ ^ [B: $i,C: $i] :
~ ( A @ B @ C ) )
| ( A @ x @ y )
| ( ( sk1 @ y @ x )
!= ( A @ y @ x ) ) ),
inference(simp,[status(thm)],[5271]) ).
thf(5335,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] :
~ ( sk1 @ A @ B ) )
| ( sk1 @ x @ y ) ),
inference(pre_uni,[status(thm)],[5272:[bind(A,$thf( sk1 ))]]) ).
thf(5412,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] :
~ ( sk1 @ A @ B ) )
| $false ),
inference(rewrite,[status(thm)],[5335,6]) ).
thf(5413,plain,
~ ( cS
@ ^ [A: $i,B: $i] :
~ ( sk1 @ A @ B ) ),
inference(simp,[status(thm)],[5412]) ).
thf(5436,plain,
( ~ $true
| ( ( cS
@ ^ [A: $i,B: $i] :
! [C: $i > $i > $o] :
( ( ( cS @ C )
& ( C @ A @ B ) )
=> ( C @ B @ A ) ) )
!= ( cS
@ ^ [A: $i,B: $i] :
~ ( sk1 @ A @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[7,5413]) ).
thf(5437,plain,
( ( cS
@ ^ [A: $i,B: $i] :
! [C: $i > $i > $o] :
( ( ( cS @ C )
& ( C @ A @ B ) )
=> ( C @ B @ A ) ) )
!= ( cS
@ ^ [A: $i,B: $i] :
~ ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[5436]) ).
thf(5444,plain,
( ( ^ [A: $i,B: $i] :
! [C: $i > $i > $o] :
( ( ( cS @ C )
& ( C @ A @ B ) )
=> ( C @ B @ A ) ) )
!= ( ^ [A: $i,B: $i] :
~ ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[5437]) ).
thf(49,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ A ) )
| ~ ( sk1 @ y @ x ) ),
inference(pre_uni,[status(thm)],[19:[bind(A,$thf( ^ [B: $i] : ^ [C: $i] : ( sk1 @ C @ B ) ))]]) ).
thf(59,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ A ) )
| ~ $true ),
inference(rewrite,[status(thm)],[49,8]) ).
thf(60,plain,
~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ A ) ),
inference(simp,[status(thm)],[59]) ).
thf(72,plain,
( ~ $true
| ( ( cS
@ ^ [A: $i,B: $i] :
! [C: $i > $i > $o] :
( ( ( cS @ C )
& ( C @ A @ B ) )
=> ( C @ B @ A ) ) )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[7,60]) ).
thf(73,plain,
( ( cS
@ ^ [A: $i,B: $i] :
! [C: $i > $i > $o] :
( ( ( cS @ C )
& ( C @ A @ B ) )
=> ( C @ B @ A ) ) )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ A ) ) ),
inference(simp,[status(thm)],[72]) ).
thf(74,plain,
( ( ^ [A: $i,B: $i] :
! [C: $i > $i > $o] :
( ( ( cS @ C )
& ( C @ A @ B ) )
=> ( C @ B @ A ) ) )
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ A ) ) ),
inference(simp,[status(thm)],[73]) ).
thf(83,plain,
( ( sk1 @ sk6 @ sk5 )
!= ( ! [A: $i > $i > $o] :
( ( ( cS @ A )
& ( A @ sk5 @ sk6 ) )
=> ( A @ sk6 @ sk5 ) ) ) ),
inference(func_ext,[status(esa)],[74]) ).
thf(92,plain,
( ~ ( sk1 @ sk6 @ sk5 )
| ~ ! [A: $i > $i > $o] :
( ( ( cS @ A )
& ( A @ sk5 @ sk6 ) )
=> ( A @ sk6 @ sk5 ) ) ),
inference(bool_ext,[status(thm)],[83]) ).
thf(106,plain,
( ( ~ ( sk1 @ sk6 @ sk5 )
| ( cS @ sk9 ) )
& ( ~ ( sk1 @ sk6 @ sk5 )
| ( sk9 @ sk5 @ sk6 ) )
& ( ~ ( sk1 @ sk6 @ sk5 )
| ~ ( sk9 @ sk6 @ sk5 ) ) ),
inference(cnf,[status(esa)],[92]) ).
thf(107,plain,
( ~ ( sk1 @ sk6 @ sk5 )
| ( cS @ sk9 ) ),
inference(cnfConj,[status(thm)],[106]) ).
thf(164,plain,
( ~ $true
| ( cS @ sk9 )
| ( ( sk1 @ sk6 @ sk5 )
!= ( sk1 @ y @ x ) ) ),
inference(paramod_ordered,[status(thm)],[8,107]) ).
thf(165,plain,
( ( cS @ sk9 )
| ( ( sk1 @ sk6 @ sk5 )
!= ( sk1 @ y @ x ) ) ),
inference(simp,[status(thm)],[164]) ).
thf(170,plain,
( ( cS @ sk9 )
| ( sk6 != y )
| ( sk5 != x ) ),
inference(simp,[status(thm)],[165]) ).
thf(6619,plain,
( ~ ( sk1 @ sk97 @ sk98 )
| ~ ( sk1 @ sk98 @ y ) ),
inference(cnfConj,[status(thm)],[6617]) ).
thf(14,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( ~ ( cS @ A )
| ~ ( A @ x @ y )
| ~ $true
| ~ ( B @ x @ y )
| ( B @ y @ x )
| ( ( A @ y @ x )
!= ( cS @ B ) ) ),
inference(paramod_ordered,[status(thm)],[5,5]) ).
thf(15,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( ~ ( cS @ A )
| ~ ( A @ x @ y )
| ~ ( B @ x @ y )
| ( B @ y @ x )
| ( ( A @ y @ x )
!= ( cS @ B ) ) ),
inference(simp,[status(thm)],[14]) ).
thf(42,plain,
! [A: $i > $i > $i > $i > $o] :
( ~ ( cS
@ ^ [B: $i,C: $i] : ( cS @ ( A @ B @ C ) ) )
| ~ ( cS @ ( A @ x @ y ) )
| ~ ( A @ y @ x @ x @ y )
| ( A @ y @ x @ y @ x ) ),
inference(pre_uni,[status(thm)],[15:[bind(A,$thf( ^ [D: $i] : ^ [E: $i] : ( cS @ ( C @ D @ E ) ) )),bind(B,$thf( C @ y @ x ))]]) ).
thf(56,plain,
! [A: $i > $i > $i > $i > $o] :
( ~ ( cS
@ ^ [B: $i,C: $i] : ( cS @ ( A @ B @ C ) ) )
| ~ ( cS @ ( A @ x @ y ) )
| ~ ( A @ y @ x @ x @ y )
| ( A @ y @ x @ y @ x ) ),
inference(simp,[status(thm)],[42]) ).
thf(25,plain,
! [A: $i > $i > $o] :
( ~ ( cS @ A )
| ~ $true
| ( A @ y @ x )
| ( ( sk1 @ y @ x )
!= ( A @ x @ y ) ) ),
inference(paramod_ordered,[status(thm)],[8,5]) ).
thf(26,plain,
! [A: $i > $i > $o] :
( ~ ( cS @ A )
| ( A @ y @ x )
| ( ( sk1 @ y @ x )
!= ( A @ x @ y ) ) ),
inference(simp,[status(thm)],[25]) ).
thf(39,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ x ) )
| ( sk1 @ x @ x ) ),
inference(pre_uni,[status(thm)],[26:[bind(A,$thf( ^ [B: $i] : ^ [C: $i] : ( sk1 @ C @ x ) ))]]) ).
thf(351,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ x ) )
| ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ x @ A ) )
| ~ $true
| ( ( sk1 @ x @ x )
!= ( sk1 @ x @ x ) ) ),
inference(paramod_ordered,[status(thm)],[39,48]) ).
thf(352,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ x ) )
| ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ x @ A ) )
| ( ( sk1 @ x @ x )
!= ( sk1 @ x @ x ) ) ),
inference(simp,[status(thm)],[351]) ).
thf(353,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ x ) )
| ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ x @ A ) ) ),
inference(pattern_uni,[status(thm)],[352:[]]) ).
thf(844,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ x ) )
| ( ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ x @ A ) )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ x ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[353]) ).
thf(853,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ x ) )
| ( ( ^ [A: $i,B: $i] : ( sk1 @ x @ A ) )
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ x ) ) ) ),
inference(simp,[status(thm)],[844]) ).
thf(2885,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ x ) )
| ( ( ^ [A: $i,B: $i] : x )
!= ( ^ [A: $i,B: $i] : B ) )
| ( ( ^ [A: $i,B: $i] : A )
!= ( ^ [A: $i,B: $i] : x ) ) ),
inference(simp,[status(thm)],[853]) ).
thf(2985,plain,
( ( sk76 != x )
| ( sk77 != x )
| ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ x ) ) ),
inference(func_ext,[status(esa)],[2885]) ).
thf(28,plain,
! [A: $i > $i > $o] :
( ~ ( cS @ A )
| ~ ( A @ x @ y )
| ( ( A @ y @ x )
!= ( ~ ( cS @ A ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[5]) ).
thf(37,plain,
! [A: $i > $i > $o] :
( ~ ( cS @ A )
| ~ ( A @ x @ y )
| ( ( A @ y @ x )
!= ( ~ ( cS @ A ) ) ) ),
inference(simp,[status(thm)],[28]) ).
thf(286,plain,
( ~ $true
| ( sk1 @ x @ x )
| ( ( cS @ sk1 )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ x ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,39]) ).
thf(287,plain,
( ( sk1 @ x @ x )
| ( ( cS @ sk1 )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ x ) ) ) ),
inference(simp,[status(thm)],[286]) ).
thf(325,plain,
( ( sk1 @ x @ x )
| ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ x ) ) ) ),
inference(simp,[status(thm)],[287]) ).
thf(341,plain,
( ~ $true
| ~ ( sk1 @ x @ x )
| ( ( cS @ sk1 )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ x @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,48]) ).
thf(342,plain,
( ~ ( sk1 @ x @ x )
| ( ( cS @ sk1 )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ x @ A ) ) ) ),
inference(simp,[status(thm)],[341]) ).
thf(360,plain,
( ~ ( sk1 @ x @ x )
| ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ x @ A ) ) ) ),
inference(simp,[status(thm)],[342]) ).
thf(863,plain,
( ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ x ) ) )
| ~ $true
| ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ x @ A ) ) )
| ( ( sk1 @ x @ x )
!= ( sk1 @ x @ x ) ) ),
inference(paramod_ordered,[status(thm)],[325,360]) ).
thf(864,plain,
( ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ x ) ) )
| ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ x @ A ) ) )
| ( ( sk1 @ x @ x )
!= ( sk1 @ x @ x ) ) ),
inference(simp,[status(thm)],[863]) ).
thf(865,plain,
( ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ x ) ) )
| ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ x @ A ) ) ) ),
inference(pattern_uni,[status(thm)],[864:[]]) ).
thf(2030,plain,
( ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ x ) ) )
| ( sk1 != sk1 )
| ( ( ^ [A: $i,B: $i] : ( sk1 @ x @ A ) )
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ x ) ) ) ),
inference(eqfactor_ordered,[status(thm)],[865]) ).
thf(2039,plain,
( ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ x ) ) )
| ( ( ^ [A: $i,B: $i] : ( sk1 @ x @ A ) )
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ x ) ) ) ),
inference(simp,[status(thm)],[2030]) ).
thf(5180,plain,
( ~ $true
| ( ( cS
@ ^ [A: $i,B: $i] :
! [C: $i > $i > $o] :
( ( ( cS @ C )
& ( C @ A @ B ) )
=> ( C @ B @ A ) ) )
!= ( cS
@ ^ [A: $i,B: $i] :
( ( sk1 @ B @ A )
| ( sk1 @ B @ y ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[7,5094]) ).
thf(5181,plain,
( ( cS
@ ^ [A: $i,B: $i] :
! [C: $i > $i > $o] :
( ( ( cS @ C )
& ( C @ A @ B ) )
=> ( C @ B @ A ) ) )
!= ( cS
@ ^ [A: $i,B: $i] :
( ( sk1 @ B @ A )
| ( sk1 @ B @ y ) ) ) ),
inference(simp,[status(thm)],[5180]) ).
thf(5186,plain,
( ( ^ [A: $i,B: $i] :
! [C: $i > $i > $o] :
( ( ( cS @ C )
& ( C @ A @ B ) )
=> ( C @ B @ A ) ) )
!= ( ^ [A: $i,B: $i] :
( ( sk1 @ B @ A )
| ( sk1 @ B @ y ) ) ) ),
inference(simp,[status(thm)],[5181]) ).
thf(5818,plain,
( ( ! [A: $i > $i > $o] :
( ( ( cS @ A )
& ( A @ sk108 @ sk109 ) )
=> ( A @ sk109 @ sk108 ) ) )
!= ( ( sk1 @ sk109 @ sk108 )
| ( sk1 @ sk109 @ y ) ) ),
inference(func_ext,[status(esa)],[5186]) ).
thf(7223,plain,
( ~ ! [A: $i > $i > $o] :
( ( ( cS @ A )
& ( A @ sk108 @ sk109 ) )
=> ( A @ sk109 @ sk108 ) )
| ~ ( ( sk1 @ sk109 @ sk108 )
| ( sk1 @ sk109 @ y ) ) ),
inference(bool_ext,[status(thm)],[5818]) ).
thf(7605,plain,
( ( ( cS @ sk169 )
| ~ ( sk1 @ sk109 @ sk108 ) )
& ( ( cS @ sk169 )
| ~ ( sk1 @ sk109 @ y ) )
& ( ( sk169 @ sk108 @ sk109 )
| ~ ( sk1 @ sk109 @ sk108 ) )
& ( ( sk169 @ sk108 @ sk109 )
| ~ ( sk1 @ sk109 @ y ) )
& ( ~ ( sk169 @ sk109 @ sk108 )
| ~ ( sk1 @ sk109 @ sk108 ) )
& ( ~ ( sk169 @ sk109 @ sk108 )
| ~ ( sk1 @ sk109 @ y ) ) ),
inference(cnf,[status(esa)],[7223]) ).
thf(7608,plain,
( ( cS @ sk169 )
| ~ ( sk1 @ sk109 @ y ) ),
inference(cnfConj,[status(thm)],[7605]) ).
thf(8597,plain,
( ~ ( sk1 @ sk109 @ y )
| ~ $true
| ( ( cS @ sk169 )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[7608,60]) ).
thf(8598,plain,
( ~ ( sk1 @ sk109 @ y )
| ( ( cS @ sk169 )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ A ) ) ) ),
inference(simp,[status(thm)],[8597]) ).
thf(8785,plain,
( ~ ( sk1 @ sk109 @ y )
| ( sk169
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ A ) ) ) ),
inference(simp,[status(thm)],[8598]) ).
thf(67,plain,
! [A: $i > $i > $o] :
( ~ $true
| ~ ( A @ x @ y )
| ( A @ y @ x )
| ( ( cS
@ ^ [B: $i,C: $i] :
! [D: $i > $i > $o] :
( ( ( cS @ D )
& ( D @ B @ C ) )
=> ( D @ C @ B ) ) )
!= ( cS @ A ) ) ),
inference(paramod_ordered,[status(thm)],[7,5]) ).
thf(68,plain,
! [A: $i > $i > $o] :
( ~ ( A @ x @ y )
| ( A @ y @ x )
| ( ( cS
@ ^ [B: $i,C: $i] :
! [D: $i > $i > $o] :
( ( ( cS @ D )
& ( D @ B @ C ) )
=> ( D @ C @ B ) ) )
!= ( cS @ A ) ) ),
inference(simp,[status(thm)],[67]) ).
thf(69,plain,
( ~ ! [A: $i > $i > $o] :
( ( ( cS @ A )
& ( A @ x @ y ) )
=> ( A @ y @ x ) )
| ! [A: $i > $i > $o] :
( ( ( cS @ A )
& ( A @ y @ x ) )
=> ( A @ x @ y ) ) ),
inference(pattern_uni,[status(thm)],[68:[bind(A,$thf( ^ [B: $i] : ^ [C: $i] : ! [D: $i > $i > $o] : ( ( ( cS @ D ) & ( D @ B @ C ) ) => ( D @ C @ B ) ) ))]]) ).
thf(75,plain,
! [A: $i > $i > $o] :
( ( ( cS @ sk2 )
| ~ ( cS @ A )
| ~ ( A @ y @ x )
| ( A @ x @ y ) )
& ( ( sk2 @ x @ y )
| ~ ( cS @ A )
| ~ ( A @ y @ x )
| ( A @ x @ y ) )
& ( ~ ( sk2 @ y @ x )
| ~ ( cS @ A )
| ~ ( A @ y @ x )
| ( A @ x @ y ) ) ),
inference(cnf,[status(esa)],[69]) ).
thf(78,plain,
! [A: $i > $i > $o] :
( ~ ( sk2 @ y @ x )
| ~ ( cS @ A )
| ~ ( A @ y @ x )
| ( A @ x @ y ) ),
inference(cnfConj,[status(thm)],[75]) ).
thf(40,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ y @ A ) )
| ( sk1 @ y @ y ) ),
inference(pre_uni,[status(thm)],[26:[bind(A,$thf( ^ [B: $i] : ^ [C: $i] : ( sk1 @ y @ B ) ))]]) ).
thf(47,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ y ) )
| ~ ( sk1 @ y @ y ) ),
inference(pre_uni,[status(thm)],[19:[bind(A,$thf( ^ [B: $i] : ^ [C: $i] : ( sk1 @ C @ y ) ))]]) ).
thf(385,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ y @ A ) )
| ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ y ) )
| ~ $true
| ( ( sk1 @ y @ y )
!= ( sk1 @ y @ y ) ) ),
inference(paramod_ordered,[status(thm)],[40,47]) ).
thf(386,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ y @ A ) )
| ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ y ) )
| ( ( sk1 @ y @ y )
!= ( sk1 @ y @ y ) ) ),
inference(simp,[status(thm)],[385]) ).
thf(387,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ y @ A ) )
| ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ y ) ) ),
inference(pattern_uni,[status(thm)],[386:[]]) ).
thf(1573,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ y @ A ) )
| ( ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ y ) )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ y @ A ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[387]) ).
thf(1582,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ y @ A ) )
| ( ( ^ [A: $i,B: $i] : ( sk1 @ B @ y ) )
!= ( ^ [A: $i,B: $i] : ( sk1 @ y @ A ) ) ) ),
inference(simp,[status(thm)],[1573]) ).
thf(2936,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ y @ A ) )
| ( ( ^ [A: $i,B: $i] : B )
!= ( ^ [A: $i,B: $i] : y ) )
| ( ( ^ [A: $i,B: $i] : y )
!= ( ^ [A: $i,B: $i] : A ) ) ),
inference(simp,[status(thm)],[1582]) ).
thf(3023,plain,
( ( sk80 != y )
| ( sk81 != y )
| ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ y @ A ) ) ),
inference(func_ext,[status(esa)],[2936]) ).
thf(4776,plain,
( ( sk80 != y )
| ( sk81 != y )
| ~ $true
| ( ( cS @ sk1 )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ y @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,3023]) ).
thf(4777,plain,
( ( sk80 != y )
| ( sk81 != y )
| ( ( cS @ sk1 )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ y @ A ) ) ) ),
inference(simp,[status(thm)],[4776]) ).
thf(4815,plain,
( ( sk80 != y )
| ( sk81 != y )
| ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ y @ A ) ) ) ),
inference(simp,[status(thm)],[4777]) ).
thf(63,plain,
( ~ $true
| ( ( cS @ sk1 )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,60]) ).
thf(64,plain,
( ( cS @ sk1 )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ A ) ) ),
inference(simp,[status(thm)],[63]) ).
thf(66,plain,
( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ A ) ) ),
inference(simp,[status(thm)],[64]) ).
thf(80,plain,
( ( sk1 @ sk4 @ sk3 )
!= ( sk1 @ sk3 @ sk4 ) ),
inference(func_ext,[status(esa)],[66]) ).
thf(86,plain,
( ( sk1 @ sk4 @ sk3 )
| ( sk1 @ sk3 @ sk4 ) ),
inference(bool_ext,[status(thm)],[80]) ).
thf(139,plain,
( ( sk1 @ sk3 @ sk4 )
| ~ $true
| ( ( sk1 @ sk4 @ sk3 )
!= ( sk1 @ x @ y ) ) ),
inference(paramod_ordered,[status(thm)],[86,6]) ).
thf(140,plain,
( ( sk1 @ sk3 @ sk4 )
| ( ( sk1 @ sk4 @ sk3 )
!= ( sk1 @ x @ y ) ) ),
inference(simp,[status(thm)],[139]) ).
thf(147,plain,
( ( sk1 @ sk3 @ sk4 )
| ( sk4 != x )
| ( sk3 != y ) ),
inference(simp,[status(thm)],[140]) ).
thf(5442,plain,
( ~ ( sk1 @ sk6 @ sk5 )
| ~ $true
| ( ( cS @ sk9 )
!= ( cS
@ ^ [A: $i,B: $i] :
~ ( sk1 @ A @ B ) ) ) ),
inference(paramod_ordered,[status(thm)],[107,5413]) ).
thf(5443,plain,
( ~ ( sk1 @ sk6 @ sk5 )
| ( ( cS @ sk9 )
!= ( cS
@ ^ [A: $i,B: $i] :
~ ( sk1 @ A @ B ) ) ) ),
inference(simp,[status(thm)],[5442]) ).
thf(5448,plain,
( ~ ( sk1 @ sk6 @ sk5 )
| ( sk9
!= ( ^ [A: $i,B: $i] :
~ ( sk1 @ A @ B ) ) ) ),
inference(simp,[status(thm)],[5443]) ).
thf(88,plain,
( ~ ( sk1 @ sk3 @ sk4 )
| ( ( sk1 @ sk4 @ sk3 )
!= ( sk1 @ y @ x ) ) ),
inference(paramod_ordered,[status(thm)],[8,80]) ).
thf(89,plain,
( ~ ( sk1 @ sk3 @ sk4 )
| ( sk4 != y )
| ( sk3 != x ) ),
inference(simp,[status(thm)],[88]) ).
thf(830,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ x ) )
| ~ $true
| ( ( cS @ sk1 )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ x @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,353]) ).
thf(831,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ x ) )
| ( ( cS @ sk1 )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ x @ A ) ) ) ),
inference(simp,[status(thm)],[830]) ).
thf(849,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ x ) )
| ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ x @ A ) ) ) ),
inference(simp,[status(thm)],[831]) ).
thf(5389,plain,
( ~ $true
| ( ( cS
@ ^ [A: $i,B: $i] :
! [C: $i > $i > $o] :
( ( ( cS @ C )
& ( C @ A @ B ) )
=> ( C @ B @ A ) ) )
!= ( cS
@ ^ [A: $i,B: $i] :
( ( sk1 @ B @ A )
| ( sk1 @ x @ A ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[7,5095]) ).
thf(5390,plain,
( ( cS
@ ^ [A: $i,B: $i] :
! [C: $i > $i > $o] :
( ( ( cS @ C )
& ( C @ A @ B ) )
=> ( C @ B @ A ) ) )
!= ( cS
@ ^ [A: $i,B: $i] :
( ( sk1 @ B @ A )
| ( sk1 @ x @ A ) ) ) ),
inference(simp,[status(thm)],[5389]) ).
thf(5395,plain,
( ( ^ [A: $i,B: $i] :
! [C: $i > $i > $o] :
( ( ( cS @ C )
& ( C @ A @ B ) )
=> ( C @ B @ A ) ) )
!= ( ^ [A: $i,B: $i] :
( ( sk1 @ B @ A )
| ( sk1 @ x @ A ) ) ) ),
inference(simp,[status(thm)],[5390]) ).
thf(5819,plain,
( ( ! [A: $i > $i > $o] :
( ( ( cS @ A )
& ( A @ sk110 @ sk111 ) )
=> ( A @ sk111 @ sk110 ) ) )
!= ( ( sk1 @ sk111 @ sk110 )
| ( sk1 @ x @ sk110 ) ) ),
inference(func_ext,[status(esa)],[5395]) ).
thf(85,plain,
( ~ ( sk1 @ sk4 @ sk3 )
| ~ ( sk1 @ sk3 @ sk4 ) ),
inference(bool_ext,[status(thm)],[80]) ).
thf(370,plain,
( ~ $true
| ( sk1 @ y @ y )
| ( ( cS @ sk1 )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ y @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,40]) ).
thf(371,plain,
( ( sk1 @ y @ y )
| ( ( cS @ sk1 )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ y @ A ) ) ) ),
inference(simp,[status(thm)],[370]) ).
thf(407,plain,
( ( sk1 @ y @ y )
| ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ y @ A ) ) ) ),
inference(simp,[status(thm)],[371]) ).
thf(5815,plain,
( ( ! [A: $i > $i > $o] :
( ( ( cS @ A )
& ( A @ sk106 @ sk107 ) )
=> ( A @ sk107 @ sk106 ) ) )
!= ( ~ ( sk1 @ sk106 @ sk107 ) ) ),
inference(func_ext,[status(esa)],[5444]) ).
thf(7058,plain,
( ~ ! [A: $i > $i > $o] :
( ( ( cS @ A )
& ( A @ sk106 @ sk107 ) )
=> ( A @ sk107 @ sk106 ) )
| ~ ~ ( sk1 @ sk106 @ sk107 ) ),
inference(bool_ext,[status(thm)],[5815]) ).
thf(7159,plain,
( ( ( cS @ sk120 )
| ( sk1 @ sk106 @ sk107 ) )
& ( ( sk120 @ sk106 @ sk107 )
| ( sk1 @ sk106 @ sk107 ) )
& ( ~ ( sk120 @ sk107 @ sk106 )
| ( sk1 @ sk106 @ sk107 ) ) ),
inference(cnf,[status(esa)],[7058]) ).
thf(7161,plain,
( ( sk120 @ sk106 @ sk107 )
| ( sk1 @ sk106 @ sk107 ) ),
inference(cnfConj,[status(thm)],[7159]) ).
thf(7160,plain,
( ( cS @ sk120 )
| ( sk1 @ sk106 @ sk107 ) ),
inference(cnfConj,[status(thm)],[7159]) ).
thf(8010,plain,
( ( sk1 @ sk106 @ sk107 )
| ~ $true
| ( ( cS @ sk120 )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[7160,60]) ).
thf(8011,plain,
( ( sk1 @ sk106 @ sk107 )
| ( ( cS @ sk120 )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ A ) ) ) ),
inference(simp,[status(thm)],[8010]) ).
thf(8270,plain,
( ( sk1 @ sk106 @ sk107 )
| ( sk120
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ A ) ) ) ),
inference(simp,[status(thm)],[8011]) ).
thf(7607,plain,
( ( cS @ sk169 )
| ~ ( sk1 @ sk109 @ sk108 ) ),
inference(cnfConj,[status(thm)],[7605]) ).
thf(8347,plain,
( ~ ( sk1 @ sk109 @ sk108 )
| ~ $true
| ( ( cS @ sk169 )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[7607,60]) ).
thf(8348,plain,
( ~ ( sk1 @ sk109 @ sk108 )
| ( ( cS @ sk169 )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ A ) ) ) ),
inference(simp,[status(thm)],[8347]) ).
thf(8545,plain,
( ~ ( sk1 @ sk109 @ sk108 )
| ( sk169
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ A ) ) ) ),
inference(simp,[status(thm)],[8348]) ).
thf(109,plain,
( ~ ( sk1 @ sk6 @ sk5 )
| ~ ( sk9 @ sk6 @ sk5 ) ),
inference(cnfConj,[status(thm)],[106]) ).
thf(603,plain,
( ~ $true
| ~ ( sk9 @ sk6 @ sk5 )
| ( ( sk1 @ sk6 @ sk5 )
!= ( sk1 @ y @ x ) ) ),
inference(paramod_ordered,[status(thm)],[8,109]) ).
thf(604,plain,
( ~ ( sk9 @ sk6 @ sk5 )
| ( ( sk1 @ sk6 @ sk5 )
!= ( sk1 @ y @ x ) ) ),
inference(simp,[status(thm)],[603]) ).
thf(615,plain,
( ~ ( sk9 @ sk6 @ sk5 )
| ( sk6 != y )
| ( sk5 != x ) ),
inference(simp,[status(thm)],[604]) ).
thf(10075,plain,
( ~ ( sk1 @ sk99 @ sk100 )
| ( ( sk1 @ sk100 @ sk99 )
!= ( sk1 @ sk99 @ sk100 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[6979]) ).
thf(10105,plain,
( ~ ( sk1 @ sk99 @ sk100 )
| ( sk100 != sk99 )
| ( sk100 != sk99 ) ),
inference(simp,[status(thm)],[10075]) ).
thf(10126,plain,
( ~ ( sk1 @ sk99 @ sk100 )
| ( sk100 != sk99 ) ),
inference(simp,[status(thm)],[10105]) ).
thf(77,plain,
! [A: $i > $i > $o] :
( ( sk2 @ x @ y )
| ~ ( cS @ A )
| ~ ( A @ y @ x )
| ( A @ x @ y ) ),
inference(cnfConj,[status(thm)],[75]) ).
thf(95,plain,
( ~ ! [A: $i > $i > $o] :
( ( ( cS @ A )
& ( A @ sk5 @ sk6 ) )
=> ( A @ sk6 @ sk5 ) )
| ( ( sk1 @ sk6 @ sk5 )
!= ( sk1 @ y @ x ) ) ),
inference(paramod_ordered,[status(thm)],[8,83]) ).
thf(97,plain,
( ~ ! [A: $i > $i > $o] :
( ( ( cS @ A )
& ( A @ sk5 @ sk6 ) )
=> ( A @ sk6 @ sk5 ) )
| ( sk6 != y )
| ( sk5 != x ) ),
inference(simp,[status(thm)],[95]) ).
thf(102,plain,
( ( ( cS @ sk8 )
| ( sk6 != y )
| ( sk5 != x ) )
& ( ( sk8 @ sk5 @ sk6 )
| ( sk6 != y )
| ( sk5 != x ) )
& ( ~ ( sk8 @ sk6 @ sk5 )
| ( sk6 != y )
| ( sk5 != x ) ) ),
inference(cnf,[status(esa)],[97]) ).
thf(105,plain,
( ~ ( sk8 @ sk6 @ sk5 )
| ( sk6 != y )
| ( sk5 != x ) ),
inference(cnfConj,[status(thm)],[102]) ).
thf(116,plain,
( ~ $true
| ~ ( sk1 @ y @ y )
| ( ( cS @ sk1 )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ y ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,47]) ).
thf(117,plain,
( ~ ( sk1 @ y @ y )
| ( ( cS @ sk1 )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ y ) ) ) ),
inference(simp,[status(thm)],[116]) ).
thf(127,plain,
( ~ ( sk1 @ y @ y )
| ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ y ) ) ) ),
inference(simp,[status(thm)],[117]) ).
thf(910,plain,
( ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ y @ A ) ) )
| ~ $true
| ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ y ) ) )
| ( ( sk1 @ y @ y )
!= ( sk1 @ y @ y ) ) ),
inference(paramod_ordered,[status(thm)],[407,127]) ).
thf(911,plain,
( ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ y @ A ) ) )
| ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ y ) ) )
| ( ( sk1 @ y @ y )
!= ( sk1 @ y @ y ) ) ),
inference(simp,[status(thm)],[910]) ).
thf(912,plain,
( ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ y @ A ) ) )
| ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ y ) ) ) ),
inference(pattern_uni,[status(thm)],[911:[]]) ).
thf(2053,plain,
( ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ y @ A ) ) )
| ( sk1 != sk1 )
| ( ( ^ [A: $i,B: $i] : ( sk1 @ B @ y ) )
!= ( ^ [A: $i,B: $i] : ( sk1 @ y @ A ) ) ) ),
inference(eqfactor_ordered,[status(thm)],[912]) ).
thf(2057,plain,
( ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ y @ A ) ) )
| ( ( ^ [A: $i,B: $i] : B )
!= ( ^ [A: $i,B: $i] : y ) )
| ( ( ^ [A: $i,B: $i] : y )
!= ( ^ [A: $i,B: $i] : A ) ) ),
inference(simp,[status(thm)],[2053]) ).
thf(792,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ y @ A ) )
| ~ $true
| ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ y ) ) )
| ( ( sk1 @ y @ y )
!= ( sk1 @ y @ y ) ) ),
inference(paramod_ordered,[status(thm)],[40,127]) ).
thf(793,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ y @ A ) )
| ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ y ) ) )
| ( ( sk1 @ y @ y )
!= ( sk1 @ y @ y ) ) ),
inference(simp,[status(thm)],[792]) ).
thf(794,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ y @ A ) )
| ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ y ) ) ) ),
inference(pattern_uni,[status(thm)],[793:[]]) ).
thf(108,plain,
( ~ ( sk1 @ sk6 @ sk5 )
| ( sk9 @ sk5 @ sk6 ) ),
inference(cnfConj,[status(thm)],[106]) ).
thf(607,plain,
( ~ ( sk1 @ sk6 @ sk5 )
| ~ ( sk1 @ sk6 @ sk5 )
| ~ $true
| ( ( sk9 @ sk6 @ sk5 )
!= ( sk9 @ sk5 @ sk6 ) ) ),
inference(paramod_ordered,[status(thm)],[108,109]) ).
thf(608,plain,
( ~ ( sk1 @ sk6 @ sk5 )
| ( ( sk9 @ sk6 @ sk5 )
!= ( sk9 @ sk5 @ sk6 ) ) ),
inference(simp,[status(thm)],[607]) ).
thf(616,plain,
( ~ ( sk1 @ sk6 @ sk5 )
| ( sk6 != sk5 )
| ( sk6 != sk5 ) ),
inference(simp,[status(thm)],[608]) ).
thf(618,plain,
( ~ ( sk1 @ sk6 @ sk5 )
| ( sk6 != sk5 ) ),
inference(simp,[status(thm)],[616]) ).
thf(623,plain,
( ~ $true
| ( sk6 != sk5 )
| ( ( sk1 @ sk6 @ sk5 )
!= ( sk1 @ y @ x ) ) ),
inference(paramod_ordered,[status(thm)],[8,618]) ).
thf(624,plain,
( ( sk6 != sk5 )
| ( ( sk1 @ sk6 @ sk5 )
!= ( sk1 @ y @ x ) ) ),
inference(simp,[status(thm)],[623]) ).
thf(633,plain,
( ( sk6 != sk5 )
| ( sk6 != y )
| ( sk5 != x ) ),
inference(simp,[status(thm)],[624]) ).
thf(27,plain,
! [A: $i > $i > $o] :
( ~ ( A @ x @ y )
| ( A @ y @ x )
| ( ( cS @ A )
!= ( A @ x @ y ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[5]) ).
thf(45,plain,
! [A: $i > $i > $o] :
( ( A @ y @ x )
| ~ ( A @ x @ y )
| ( ( cS @ A )
!= ( A @ x @ y ) ) ),
inference(simp,[status(thm)],[27]) ).
thf(103,plain,
( ( cS @ sk8 )
| ( sk6 != y )
| ( sk5 != x ) ),
inference(cnfConj,[status(thm)],[102]) ).
thf(764,plain,
( ( sk6 != y )
| ( sk5 != x )
| ~ $true
| ( ( cS @ sk8 )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[103,60]) ).
thf(765,plain,
( ( sk6 != y )
| ( sk5 != x )
| ( ( cS @ sk8 )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ A ) ) ) ),
inference(simp,[status(thm)],[764]) ).
thf(772,plain,
( ( sk6 != y )
| ( sk5 != x )
| ( sk8
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ A ) ) ) ),
inference(simp,[status(thm)],[765]) ).
thf(9158,plain,
( ~ ! [A: $i > $i > $o] :
( ( ( cS @ A )
& ( A @ sk110 @ sk111 ) )
=> ( A @ sk111 @ sk110 ) )
| ~ ( ( sk1 @ sk111 @ sk110 )
| ( sk1 @ x @ sk110 ) ) ),
inference(bool_ext,[status(thm)],[5819]) ).
thf(9540,plain,
( ( ( cS @ sk244 )
| ~ ( sk1 @ sk111 @ sk110 ) )
& ( ( cS @ sk244 )
| ~ ( sk1 @ x @ sk110 ) )
& ( ( sk244 @ sk110 @ sk111 )
| ~ ( sk1 @ sk111 @ sk110 ) )
& ( ( sk244 @ sk110 @ sk111 )
| ~ ( sk1 @ x @ sk110 ) )
& ( ~ ( sk244 @ sk111 @ sk110 )
| ~ ( sk1 @ sk111 @ sk110 ) )
& ( ~ ( sk244 @ sk111 @ sk110 )
| ~ ( sk1 @ x @ sk110 ) ) ),
inference(cnf,[status(esa)],[9158]) ).
thf(9543,plain,
( ( cS @ sk244 )
| ~ ( sk1 @ x @ sk110 ) ),
inference(cnfConj,[status(thm)],[9540]) ).
thf(168,plain,
( ~ ( sk1 @ sk6 @ sk5 )
| ~ $true
| ( ( cS @ sk9 )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[107,60]) ).
thf(169,plain,
( ~ ( sk1 @ sk6 @ sk5 )
| ( ( cS @ sk9 )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ A ) ) ) ),
inference(simp,[status(thm)],[168]) ).
thf(171,plain,
( ~ ( sk1 @ sk6 @ sk5 )
| ( sk9
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ A ) ) ) ),
inference(simp,[status(thm)],[169]) ).
thf(277,plain,
( ~ $true
| ( sk9
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ A ) ) )
| ( ( sk1 @ sk6 @ sk5 )
!= ( sk1 @ y @ x ) ) ),
inference(paramod_ordered,[status(thm)],[8,171]) ).
thf(278,plain,
( ( sk9
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ A ) ) )
| ( ( sk1 @ sk6 @ sk5 )
!= ( sk1 @ y @ x ) ) ),
inference(simp,[status(thm)],[277]) ).
thf(281,plain,
( ( sk9
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ A ) ) )
| ( sk6 != y )
| ( sk5 != x ) ),
inference(simp,[status(thm)],[278]) ).
thf(16,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( ~ ( cS @ A )
| ~ ( A @ x @ y )
| ~ ( cS @ B )
| ~ $true
| ( B @ y @ x )
| ( ( A @ y @ x )
!= ( B @ x @ y ) ) ),
inference(paramod_ordered,[status(thm)],[5,5]) ).
thf(17,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( ~ ( cS @ A )
| ~ ( A @ x @ y )
| ~ ( cS @ B )
| ( B @ y @ x )
| ( ( A @ y @ x )
!= ( B @ x @ y ) ) ),
inference(simp,[status(thm)],[16]) ).
thf(43,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( ~ ( cS @ A )
| ~ ( A @ x @ y )
| ~ ( cS @ B )
| ( B @ y @ x )
| ( ( A @ y @ x )
!= ( B @ x @ y ) ) ),
inference(pre_uni,[status(thm)],[17:[]]) ).
thf(44,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( ( B @ y @ x )
| ~ ( cS @ B )
| ~ ( A @ x @ y )
| ~ ( cS @ A )
| ( ( A @ y @ x )
!= ( B @ x @ y ) ) ),
inference(pre_uni,[status(thm)],[43:[]]) ).
thf(52,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( ~ ( cS
@ ^ [C: $i,D: $i] :
( ( A @ C @ D )
| ( B @ C @ D ) ) )
| ~ ( B @ x @ y )
| ( A @ y @ x )
| ( B @ y @ x ) ),
inference(cnfConj,[status(thm)],[50]) ).
thf(54,plain,
! [B: $i > $i > $o,A: $i > $i > $o] :
( ~ ( cS
@ ^ [C: $i,D: $i] :
( ( A @ C @ D )
| ( B @ C @ D ) ) )
| ~ ( B @ x @ y )
| ( A @ y @ x )
| ( B @ y @ x ) ),
inference(simp,[status(thm)],[52]) ).
thf(2055,plain,
( ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ y @ A ) ) )
| ( ( ^ [A: $i,B: $i] : ( sk1 @ B @ y ) )
!= ( ^ [A: $i,B: $i] : ( sk1 @ y @ A ) ) ) ),
inference(simp,[status(thm)],[2053]) ).
thf(76,plain,
! [A: $i > $i > $o] :
( ( cS @ sk2 )
| ~ ( cS @ A )
| ~ ( A @ y @ x )
| ( A @ x @ y ) ),
inference(cnfConj,[status(thm)],[75]) ).
thf(647,plain,
( ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ x ) ) )
| ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ x @ A ) )
| ~ $true
| ( ( sk1 @ x @ x )
!= ( sk1 @ x @ x ) ) ),
inference(paramod_ordered,[status(thm)],[325,48]) ).
thf(648,plain,
( ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ x ) ) )
| ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ x @ A ) )
| ( ( sk1 @ x @ x )
!= ( sk1 @ x @ x ) ) ),
inference(simp,[status(thm)],[647]) ).
thf(649,plain,
( ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ x ) ) )
| ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ x @ A ) ) ),
inference(pattern_uni,[status(thm)],[648:[]]) ).
thf(84,plain,
( ( sk4 != sk3 )
| ( sk4 != sk3 ) ),
inference(simp,[status(thm)],[80]) ).
thf(91,plain,
sk4 != sk3,
inference(simp,[status(thm)],[84]) ).
thf(118,plain,
( ~ $true
| ~ ( sk1 @ y @ y )
| ( ( cS
@ ^ [A: $i,B: $i] :
! [C: $i > $i > $o] :
( ( ( cS @ C )
& ( C @ A @ B ) )
=> ( C @ B @ A ) ) )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ y ) ) ) ),
inference(paramod_ordered,[status(thm)],[7,47]) ).
thf(119,plain,
( ~ ( sk1 @ y @ y )
| ( ( cS
@ ^ [A: $i,B: $i] :
! [C: $i > $i > $o] :
( ( ( cS @ C )
& ( C @ A @ B ) )
=> ( C @ B @ A ) ) )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ y ) ) ) ),
inference(simp,[status(thm)],[118]) ).
thf(130,plain,
( ~ ( sk1 @ y @ y )
| ( ( ^ [A: $i,B: $i] :
! [C: $i > $i > $o] :
( ( ( cS @ C )
& ( C @ A @ B ) )
=> ( C @ B @ A ) ) )
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ y ) ) ) ),
inference(simp,[status(thm)],[119]) ).
thf(542,plain,
( ~ ( sk1 @ sk4 @ sk3 )
| ~ $true
| ( ( sk1 @ sk3 @ sk4 )
!= ( sk1 @ y @ x ) ) ),
inference(paramod_ordered,[status(thm)],[8,85]) ).
thf(543,plain,
( ~ ( sk1 @ sk4 @ sk3 )
| ( ( sk1 @ sk3 @ sk4 )
!= ( sk1 @ y @ x ) ) ),
inference(simp,[status(thm)],[542]) ).
thf(563,plain,
( ~ ( sk1 @ sk4 @ sk3 )
| ( sk3 != y )
| ( sk4 != x ) ),
inference(simp,[status(thm)],[543]) ).
thf(4903,plain,
! [A: $i > $i > $o] :
( ~ ( cS
@ ^ [B: $i,C: $i] :
( ( sk1 @ C @ B )
| ( A @ B @ C ) ) )
| ~ $true
| ( sk1
!= ( ^ [B: $i,C: $i] : ( sk1 @ x @ B ) ) )
| ( ( A @ y @ x )
!= ( sk1 @ x @ x ) ) ),
inference(paramod_ordered,[status(thm)],[4825,360]) ).
thf(4904,plain,
! [A: $i > $i > $o] :
( ~ ( cS
@ ^ [B: $i,C: $i] :
( ( sk1 @ C @ B )
| ( A @ B @ C ) ) )
| ( sk1
!= ( ^ [B: $i,C: $i] : ( sk1 @ x @ B ) ) )
| ( ( A @ y @ x )
!= ( sk1 @ x @ x ) ) ),
inference(simp,[status(thm)],[4903]) ).
thf(5001,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] :
( ( sk1 @ B @ A )
| ( sk1 @ B @ B ) ) )
| ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ x @ A ) ) ) ),
inference(pre_uni,[status(thm)],[4904:[bind(A,$thf( ^ [B: $i] : ^ [C: $i] : ( sk1 @ C @ C ) ))]]) ).
thf(4720,plain,
( ( sk76 != x )
| ( sk77 != x )
| ~ $true
| ( ( cS @ sk1 )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ x ) ) ) ),
inference(paramod_ordered,[status(thm)],[9,2985]) ).
thf(4721,plain,
( ( sk76 != x )
| ( sk77 != x )
| ( ( cS @ sk1 )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ x ) ) ) ),
inference(simp,[status(thm)],[4720]) ).
thf(4748,plain,
( ( sk76 != x )
| ( sk77 != x )
| ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ x ) ) ) ),
inference(simp,[status(thm)],[4721]) ).
thf(576,plain,
( ~ $true
| ( sk9 @ sk5 @ sk6 )
| ( ( sk1 @ sk6 @ sk5 )
!= ( sk1 @ y @ x ) ) ),
inference(paramod_ordered,[status(thm)],[8,108]) ).
thf(577,plain,
( ( sk9 @ sk5 @ sk6 )
| ( ( sk1 @ sk6 @ sk5 )
!= ( sk1 @ y @ x ) ) ),
inference(simp,[status(thm)],[576]) ).
thf(595,plain,
( ( sk9 @ sk5 @ sk6 )
| ( sk6 != y )
| ( sk5 != x ) ),
inference(simp,[status(thm)],[577]) ).
thf(104,plain,
( ( sk8 @ sk5 @ sk6 )
| ( sk6 != y )
| ( sk5 != x ) ),
inference(cnfConj,[status(thm)],[102]) ).
thf(34,plain,
! [A: $i > $i > $i > $i > $o] :
( ~ ( cS
@ ^ [B: $i,C: $i] : ( cS @ ( A @ B @ C ) ) )
| ~ ( cS @ ( A @ x @ y ) )
| ( cS @ ( A @ y @ x ) ) ),
inference(prim_subst,[status(thm)],[5:[bind(A,$thf( ^ [C: $i] : ^ [D: $i] : ( cS @ ( B @ C @ D ) ) ))]]) ).
thf(55,plain,
! [A: $i > $i > $i > $i > $o] :
( ~ ( cS
@ ^ [B: $i,C: $i] : ( cS @ ( A @ B @ C ) ) )
| ~ ( cS @ ( A @ x @ y ) )
| ( cS @ ( A @ y @ x ) ) ),
inference(simp,[status(thm)],[34]) ).
thf(2041,plain,
( ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ x ) ) )
| ( ( ^ [A: $i,B: $i] : x )
!= ( ^ [A: $i,B: $i] : B ) )
| ( ( ^ [A: $i,B: $i] : A )
!= ( ^ [A: $i,B: $i] : x ) ) ),
inference(simp,[status(thm)],[2030]) ).
thf(29,plain,
! [A: $i > $i > $o] :
( ~ ( cS @ A )
| ~ ( A @ x @ y )
| ( ( A @ y @ x )
!= ( ~ ( A @ x @ y ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[5]) ).
thf(36,plain,
! [A: $i > $i > $o] :
( ~ ( cS @ A )
| ~ ( A @ x @ y )
| ( ( A @ y @ x )
!= ( ~ ( A @ x @ y ) ) ) ),
inference(simp,[status(thm)],[29]) ).
thf(9541,plain,
( ( cS @ sk244 )
| ~ ( sk1 @ sk111 @ sk110 ) ),
inference(cnfConj,[status(thm)],[9540]) ).
thf(10227,plain,
( ~ ( sk1 @ sk111 @ sk110 )
| ~ $true
| ( ( cS @ sk244 )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ A ) ) ) ),
inference(paramod_ordered,[status(thm)],[9541,60]) ).
thf(10228,plain,
( ~ ( sk1 @ sk111 @ sk110 )
| ( ( cS @ sk244 )
!= ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ A ) ) ) ),
inference(simp,[status(thm)],[10227]) ).
thf(10408,plain,
( ~ ( sk1 @ sk111 @ sk110 )
| ( sk244
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ A ) ) ) ),
inference(simp,[status(thm)],[10228]) ).
thf(4846,plain,
! [A: $i > $i > $o] :
( ~ ( cS
@ ^ [B: $i,C: $i] :
( ( sk1 @ C @ B )
| ( A @ B @ C ) ) )
| ~ $true
| ( sk1
!= ( ^ [B: $i,C: $i] : ( sk1 @ C @ y ) ) )
| ( ( A @ y @ x )
!= ( sk1 @ y @ y ) ) ),
inference(paramod_ordered,[status(thm)],[4825,127]) ).
thf(4847,plain,
! [A: $i > $i > $o] :
( ~ ( cS
@ ^ [B: $i,C: $i] :
( ( sk1 @ C @ B )
| ( A @ B @ C ) ) )
| ( sk1
!= ( ^ [B: $i,C: $i] : ( sk1 @ C @ y ) ) )
| ( ( A @ y @ x )
!= ( sk1 @ y @ y ) ) ),
inference(simp,[status(thm)],[4846]) ).
thf(5019,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] :
( ( sk1 @ B @ A )
| ( sk1 @ A @ A ) ) )
| ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ B @ y ) ) ) ),
inference(pre_uni,[status(thm)],[4847:[bind(A,$thf( ^ [B: $i] : ^ [C: $i] : ( sk1 @ B @ B ) ))]]) ).
thf(4978,plain,
! [A: $i > $i > $o] :
( ~ ( cS
@ ^ [B: $i,C: $i] :
( ( sk1 @ C @ B )
| ( A @ B @ C ) ) )
| ~ ( cS
@ ^ [B: $i,C: $i] : ( sk1 @ C @ y ) )
| ~ $true
| ( ( A @ y @ x )
!= ( sk1 @ y @ y ) ) ),
inference(paramod_ordered,[status(thm)],[4825,47]) ).
thf(4979,plain,
! [A: $i > $i > $o] :
( ~ ( cS
@ ^ [B: $i,C: $i] :
( ( sk1 @ C @ B )
| ( A @ B @ C ) ) )
| ~ ( cS
@ ^ [B: $i,C: $i] : ( sk1 @ C @ y ) )
| ( ( A @ y @ x )
!= ( sk1 @ y @ y ) ) ),
inference(simp,[status(thm)],[4978]) ).
thf(5036,plain,
( ~ ( cS
@ ^ [A: $i,B: $i] :
( ( sk1 @ B @ A )
| ( sk1 @ A @ A ) ) )
| ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ y ) ) ),
inference(pre_uni,[status(thm)],[4979:[bind(A,$thf( ^ [B: $i] : ^ [C: $i] : ( sk1 @ B @ B ) ))]]) ).
thf(921,plain,
( ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ y @ A ) ) )
| ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ y ) )
| ~ $true
| ( ( sk1 @ y @ y )
!= ( sk1 @ y @ y ) ) ),
inference(paramod_ordered,[status(thm)],[407,47]) ).
thf(922,plain,
( ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ y @ A ) ) )
| ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ y ) )
| ( ( sk1 @ y @ y )
!= ( sk1 @ y @ y ) ) ),
inference(simp,[status(thm)],[921]) ).
thf(923,plain,
( ( sk1
!= ( ^ [A: $i,B: $i] : ( sk1 @ y @ A ) ) )
| ~ ( cS
@ ^ [A: $i,B: $i] : ( sk1 @ B @ y ) ) ),
inference(pattern_uni,[status(thm)],[922:[]]) ).
thf(13261,plain,
$false,
inference(e,[status(thm)],[6979,13,7896,48,5444,170,6619,5,56,5192,2985,37,2039,8785,853,5397,325,78,4815,353,147,5448,89,4825,74,849,5819,6,60,85,407,7161,5815,8270,7608,8545,9,53,615,10126,109,5818,77,105,2057,794,633,360,5402,7160,2936,618,45,5095,772,9543,281,44,5395,3023,54,2055,86,7607,76,7,39,649,387,103,91,66,108,912,130,5094,563,3,5403,80,127,5001,5186,4748,595,2885,104,40,55,171,6618,8,58,2041,36,865,10408,107,9541,5019,5413,5036,1582,47,83,923]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEV116^5 : TPTP v9.3.1. Bugfixed v5.2.0.
% 0.00/0.12 % 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.27/0.31 % Computer : n008.cluster.edu
% 0.27/0.31 % Model : x86_64 x86_64
% 0.27/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.27/0.31 % Memory : 8046.5625MB
% 0.27/0.31 % OS : Linux 6.8.0-71-generic
% 0.27/0.31 % CPULimit : 300
% 0.27/0.31 % WCLimit : 300
% 0.27/0.31 % DateTime : Tue Sep 29 15:12:09 UTC 2026
% 0.27/0.31 % CPUTime :
% 0.27/0.31 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.02/0.70 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.28/0.81 % [INFO] Parsing done (107ms).
% 1.28/0.82 % [INFO] Running in sequential loop mode.
% 1.72/1.14 % [INFO] eprover registered as external prover.
% 1.72/1.15 % [INFO] Scanning for conjecture ...
% 2.07/1.22 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 2.07/1.25 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 2.07/1.25 % [INFO] Problem is higher-order (TPTP THF).
% 2.07/1.25 % [INFO] Type checking passed.
% 2.07/1.25 % [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 ...
% 93.78/18.87 % External prover 'e' found a proof!
% 93.78/18.88 % [INFO] Killing All external provers ...
% 93.78/18.88 % Time passed: 18443ms (effective reasoning time: 18057ms)
% 93.78/18.88 % 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)>
% 93.78/18.88 % Axioms used in derivation (0):
% 93.78/18.88 % No. of inferences in proof: 256
% 93.78/18.88 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 18443 ms resp. 18057 ms w/o parsing
% 95.21/19.10 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 95.21/19.10 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------