%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SEU933^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n020.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:29:36 AM UTC 2026
% Result : Theorem 45.43s 12.32s
% Output : Refutation 45.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 51
% Number of leaves : 3
% Syntax : Number of formulae : 108 ( 32 unt; 0 typ; 2 def)
% Number of atoms : 322 ( 157 equ; 9 cnn)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 1112 ( 211 ~; 181 |; 12 &; 687 @)
% ( 0 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 7 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 224 ( 224 >; 0 *; 0 +; 0 <<)
% Number of symbols : 16 ( 11 usr; 11 con; 0-4 aty)
% Number of variables : 443 ( 255 ^; 186 !; 0 ?; 443 :)
% ( 0 !>; 0 ?*; 0 @-; 2 @+)
% Comments :
%------------------------------------------------------------------------------
thf(b_decl,type,
b: $i ).
thf(a_decl,type,
a: $i ).
thf(sk1_decl,type,
sk1: ( $i > $i ) > ( $i > $i ) > $o ).
thf(sk2_decl,type,
sk2: ( $i > $i ) > ( $i > $i ) > ( $i > $i ) > $o ).
thf(sk3_decl,type,
sk3: ( ( $i > $i ) > $o ) > ( $i > $i ) > ( $i > $i ) > $i > $i ).
thf(sk4_decl,type,
sk4: ( $i > $i ) > ( $i > $i ) > $i ).
thf(sk7_decl,type,
sk7: $i ).
thf(sk8_decl,type,
sk8: $i ).
thf(sk11_decl,type,
sk11: $i ).
thf(sk13_decl,type,
sk13: $i ).
thf(sk16_decl,type,
sk16: $i ).
thf(sk2_def,definition,
( sk2
= ( ^ [A: $i > $i,B: $i > $i] :
@+[C: ( $i > $i ) > $o] :
~ ( ( ( C @ B )
& ! [D: $i > $i] :
( ( C @ D )
=> ( C
@ ^ [E: $i] : ( B @ ( D @ E ) ) ) ) )
=> ( C
@ ^ [D: $i] : ( A @ ( B @ D ) ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( ^ [A: ( $i > $i ) > $o,B: $i > $i,C: $i > $i] :
@+[D: $i > $i] :
~ ( ( A @ D )
=> ( A
@ ^ [E: $i] : ( C @ ( D @ E ) ) ) ) ) ) ).
thf(1,conjecture,
( ( a != b )
=> ~ ! [A: $i > $i,B: $i > $i] :
( ! [C: ( $i > $i ) > $o] :
( ( ( C @ A )
& ! [D: $i > $i] :
( ( C @ D )
=> ( C
@ ^ [E: $i] : ( A @ ( D @ E ) ) ) ) )
=> ( C
@ ^ [D: $i] : ( B @ ( A @ D ) ) ) )
=> ! [C: ( $i > $i ) > $o] :
( ( ( C @ A )
& ! [D: $i > $i] :
( ( C @ D )
=> ( C
@ ^ [E: $i] : ( A @ ( D @ E ) ) ) ) )
=> ( C @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cTHM196B_pme) ).
thf(2,negated_conjecture,
~ ( ( a != b )
=> ~ ! [A: $i > $i,B: $i > $i] :
( ! [C: ( $i > $i ) > $o] :
( ( ( C @ A )
& ! [D: $i > $i] :
( ( C @ D )
=> ( C
@ ^ [E: $i] : ( A @ ( D @ E ) ) ) ) )
=> ( C
@ ^ [D: $i] : ( B @ ( A @ D ) ) ) )
=> ! [C: ( $i > $i ) > $o] :
( ( ( C @ A )
& ! [D: $i > $i] :
( ( C @ D )
=> ( C
@ ^ [E: $i] : ( A @ ( D @ E ) ) ) ) )
=> ( C @ B ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(3,plain,
~ ( ( a != b )
=> ~ ! [A: $i > $i,B: $i > $i] :
( ! [C: ( $i > $i ) > $o] :
( ( ( C @ A )
& ! [D: $i > $i] :
( ( C @ D )
=> ( C
@ ^ [E: $i] : ( A @ ( D @ E ) ) ) ) )
=> ( C
@ ^ [D: $i] : ( B @ ( A @ D ) ) ) )
=> ! [C: ( $i > $i ) > $o] :
( ( ( C @ A )
& ! [D: $i > $i] :
( ( C @ D )
=> ( C
@ ^ [E: $i] : ( A @ ( D @ E ) ) ) ) )
=> ( C @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(4,plain,
! [D: ( $i > $i ) > $o,C: $i > $i,B: $i > $i,A: $i > $i] :
( ( a != b )
& ( ( sk2 @ B @ A @ A )
| ( sk1 @ A @ B ) )
& ( ~ ( sk2 @ B @ A @ C )
| ( sk2 @ B @ A
@ ^ [E: $i] : ( A @ ( C @ E ) ) )
| ( sk1 @ A @ B ) )
& ( ~ ( sk2 @ B @ A
@ ^ [E: $i] : ( B @ ( A @ E ) ) )
| ( sk1 @ A @ B ) )
& ( ~ ( sk1 @ A @ B )
| ~ ( D @ A )
| ( D @ ( sk3 @ D @ B @ A ) )
| ( D @ B ) )
& ( ~ ( sk1 @ A @ B )
| ~ ( D @ A )
| ~ ( D
@ ^ [E: $i] : ( A @ ( sk3 @ D @ B @ A @ E ) ) )
| ( D @ B ) ) ),
inference(cnf,[status(esa)],[3]) ).
thf(5,plain,
! [B: $i > $i,A: $i > $i] :
( ( sk2 @ B @ A @ A )
| ( sk1 @ A @ B ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(9,plain,
! [C: ( $i > $i ) > $o,B: $i > $i,A: $i > $i] :
( ~ ( sk1 @ A @ B )
| ~ ( C @ A )
| ( C @ ( sk3 @ C @ B @ A ) )
| ( C @ B ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(14,plain,
! [C: ( $i > $i ) > $o,B: $i > $i,A: $i > $i] :
( ~ ( sk1 @ A @ B )
| ~ ( C @ A )
| ( C @ ( sk3 @ C @ B @ A ) )
| ( C @ B ) ),
inference(simp,[status(thm)],[9]) ).
thf(12,plain,
! [B: $i > $i,A: $i > $i] :
( ~ ( sk1 @ A @ B )
| ( A != A )
| ( A
= ( sk3 @ ( (=) @ ( $i > $i ) @ A ) @ B @ A ) )
| ( A = B ) ),
inference(replace_leibeq,[status(thm)],[9:[bind(A,$thf( (@) )),bind(B,$thf( A )),bind(C,$thf( (=) @ ( $i > $i ) @ (@) ))]]) ).
thf(15,plain,
! [B: $i > $i,A: $i > $i] :
( ( A != A )
| ( A
= ( sk3 @ ( (=) @ ( $i > $i ) @ A ) @ B @ A ) )
| ( A = B )
| ~ ( sk1 @ A @ B ) ),
inference(lifteq,[status(thm)],[12]) ).
thf(16,plain,
! [B: $i > $i,A: $i > $i] :
( ( A
= ( sk3 @ ( (=) @ ( $i > $i ) @ A ) @ B @ A ) )
| ( A = B )
| ~ ( sk1 @ A @ B ) ),
inference(simp,[status(thm)],[15]) ).
thf(6,plain,
! [C: ( $i > $i ) > $o,B: $i > $i,A: $i > $i] :
( ~ ( sk1 @ A @ B )
| ~ ( C @ A )
| ~ ( C
@ ^ [D: $i] : ( A @ ( sk3 @ C @ B @ A @ D ) ) )
| ( C @ B ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(13,plain,
! [C: ( $i > $i ) > $o,B: $i > $i,A: $i > $i] :
( ~ ( sk1 @ A @ B )
| ~ ( C @ A )
| ~ ( C
@ ^ [D: $i] : ( A @ ( sk3 @ C @ B @ A @ D ) ) )
| ( C @ B ) ),
inference(simp,[status(thm)],[6]) ).
thf(238,plain,
! [E: ( $i > $i ) > $o,D: $i > $i,C: $i > $i,B: $i > $i,A: $i > $i] :
( ( A = B )
| ~ ( sk1 @ A @ B )
| ~ ( sk1 @ C @ D )
| ~ ( E @ C )
| ~ ( E @ A )
| ( E @ D )
| ( ( sk3 @ ( (=) @ ( $i > $i ) @ A ) @ B @ A )
!= ( ^ [F: $i] : ( C @ ( sk3 @ E @ D @ C @ F ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[16,13]) ).
thf(273,plain,
! [B: $i > $i,A: $i > $i] :
( ( ( ^ [C: $i] : C )
= A )
| ~ ( sk1
@ ^ [C: $i] : C
@ A )
| ~ ( sk1
@ ^ [C: $i] : C
@ B )
| ( ( ^ [C: $i] : C )
!= ( ^ [C: $i] : C ) )
| ( ( ^ [C: $i] : C )
!= ( ^ [C: $i] : C ) )
| ( ( ^ [C: $i] : C )
= B )
| ( ( ^ [C: $i] : A )
!= ( ^ [C: $i] : B ) ) ),
inference(pre_uni,[status(thm)],[238:[bind(A,$thf( ^ [F: $i] : F )),bind(B,$thf( B )),bind(C,$thf( ^ [F: $i] : F )),bind(D,$thf( D )),bind(E,$thf( (=) @ ( $i > $i ) @ ^ [F: $i] : F ))]]) ).
thf(274,plain,
! [A: $i > $i] :
( ( ( ^ [B: $i] : B )
= A )
| ( ( ^ [B: $i] : B )
!= ( ^ [B: $i] : B ) )
| ( ( ^ [B: $i] : B )
!= ( ^ [B: $i] : B ) )
| ~ ( sk1
@ ^ [B: $i] : B
@ A )
| ~ ( sk1
@ ^ [B: $i] : B
@ A )
| ( ( ^ [B: $i] : B )
= A ) ),
inference(pattern_uni,[status(thm)],[273:[bind(A,$thf( (@) )),bind(B,$thf( (@) ))]]) ).
thf(306,plain,
! [A: $i > $i] :
( ( ( ^ [B: $i] : B )
= A )
| ( ( ^ [B: $i] : B )
!= ( ^ [B: $i] : B ) )
| ( ( ^ [B: $i] : B )
!= ( ^ [B: $i] : B ) )
| ~ ( sk1
@ ^ [B: $i] : B
@ A )
| ~ ( sk1
@ ^ [B: $i] : B
@ A )
| ( ( ^ [B: $i] : B )
= A ) ),
inference(lifteq,[status(thm)],[274]) ).
thf(307,plain,
! [A: $i > $i] :
( ( ( ^ [B: $i] : B )
= A )
| ~ ( sk1
@ ^ [B: $i] : B
@ A ) ),
inference(simp,[status(thm)],[306]) ).
thf(10,plain,
! [B: $i > $i,A: $i > $i] :
( ~ ( sk2 @ B @ A
@ ^ [C: $i] : ( B @ ( A @ C ) ) )
| ( sk1 @ A @ B ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(20,plain,
! [D: $i > $i,C: $i > $i,B: $i > $i,A: $i > $i] :
( ( sk1 @ A @ B )
| ~ $true
| ( sk1 @ C @ D )
| ( ( sk2 @ B @ A @ A )
!= ( sk2 @ D @ C
@ ^ [E: $i] : ( D @ ( C @ E ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[5,10]) ).
thf(21,plain,
! [D: $i > $i,C: $i > $i,B: $i > $i,A: $i > $i] :
( ( sk1 @ A @ B )
| ( sk1 @ C @ D )
| ( ( sk2 @ B @ A @ A )
!= ( sk2 @ D @ C
@ ^ [E: $i] : ( D @ ( C @ E ) ) ) ) ),
inference(simp,[status(thm)],[20]) ).
thf(22,plain,
! [B: $i > $i,A: $i > $i] :
( ( sk1 @ A @ B )
| ( sk1 @ A @ B )
| ( A
!= ( ^ [C: $i] : ( B @ ( A @ C ) ) ) ) ),
inference(pre_uni,[status(thm)],[21:[bind(A,$thf( C )),bind(B,$thf( D ))]]) ).
thf(23,plain,
! [B: $i > $i,A: $i > $i] :
( ( sk1 @ A @ B )
| ( sk1 @ A @ B )
| ( A
!= ( ^ [C: $i] : ( B @ ( A @ C ) ) ) ) ),
inference(pre_uni,[status(thm)],[22:[]]) ).
thf(24,plain,
! [B: $i > $i,A: $i > $i] :
( ( sk1 @ A @ B )
| ( A
!= ( ^ [C: $i] : ( B @ ( A @ C ) ) ) ) ),
inference(simp,[status(thm)],[23]) ).
thf(320,plain,
! [B: $i,A: $i > $i] :
( ( ( A @ B )
= B )
| ~ ( sk1
@ ^ [C: $i] : C
@ A ) ),
inference(func_ext,[status(esa)],[307]) ).
thf(8,plain,
a != b,
inference(cnfConj,[status(thm)],[4]) ).
thf(19,plain,
a != b,
inference(lifteq,[status(thm)],[8]) ).
thf(829,plain,
! [B: $i,A: $i > $i] :
( ~ ( sk1
@ ^ [C: $i] : C
@ A )
| ( B != b )
| ( ( A @ B )
!= a ) ),
inference(paramod_ordered,[status(thm)],[320,19]) ).
thf(837,plain,
! [A: $i] :
( ~ ( sk1
@ ^ [B: $i] : B
@ ^ [B: $i] : a )
| ( A != b ) ),
inference(pre_uni,[status(thm)],[829:[bind(A,$thf( ^ [C: $i] : a ))]]) ).
thf(839,plain,
~ ( sk1
@ ^ [A: $i] : A
@ ^ [A: $i] : a ),
inference(pattern_uni,[status(thm)],[837:[bind(A,$thf( b ))]]) ).
thf(887,plain,
! [B: $i > $i,A: $i > $i] :
( ( A
!= ( ^ [C: $i] : ( B @ ( A @ C ) ) ) )
| ~ $true
| ( ( sk1 @ A @ B )
!= ( sk1
@ ^ [C: $i] : C
@ ^ [C: $i] : a ) ) ),
inference(paramod_ordered,[status(thm)],[24,839]) ).
thf(888,plain,
! [B: $i > $i,A: $i > $i] :
( ( A
!= ( ^ [C: $i] : ( B @ ( A @ C ) ) ) )
| ( ( sk1 @ A @ B )
!= ( sk1
@ ^ [C: $i] : C
@ ^ [C: $i] : a ) ) ),
inference(simp,[status(thm)],[887]) ).
thf(889,plain,
( ( ^ [A: $i] : A )
!= ( ^ [A: $i] : a ) ),
inference(pattern_uni,[status(thm)],[888:[bind(A,$thf( ^ [C: $i] : C )),bind(B,$thf( ^ [C: $i] : a ))]]) ).
thf(902,plain,
sk7 != a,
inference(func_ext,[status(esa)],[889]) ).
thf(936,plain,
! [B: $i,A: $i > $i] :
( ~ ( sk1
@ ^ [C: $i] : C
@ A )
| ( B != a )
| ( ( A @ B )
!= sk7 ) ),
inference(paramod_ordered,[status(thm)],[320,902]) ).
thf(937,plain,
! [A: $i] :
( ~ ( sk1
@ ^ [B: $i] : B
@ ^ [B: $i] : sk7 )
| ( A != a ) ),
inference(pre_uni,[status(thm)],[936:[bind(A,$thf( ^ [C: $i] : sk7 ))]]) ).
thf(939,plain,
~ ( sk1
@ ^ [A: $i] : A
@ ^ [A: $i] : sk7 ),
inference(pattern_uni,[status(thm)],[937:[bind(A,$thf( a ))]]) ).
thf(1318,plain,
! [B: $i > $i,A: $i > $i] :
( ( A
!= ( ^ [C: $i] : ( B @ ( A @ C ) ) ) )
| ~ $true
| ( ( sk1 @ A @ B )
!= ( sk1
@ ^ [C: $i] : C
@ ^ [C: $i] : sk7 ) ) ),
inference(paramod_ordered,[status(thm)],[24,939]) ).
thf(1319,plain,
! [B: $i > $i,A: $i > $i] :
( ( A
!= ( ^ [C: $i] : ( B @ ( A @ C ) ) ) )
| ( ( sk1 @ A @ B )
!= ( sk1
@ ^ [C: $i] : C
@ ^ [C: $i] : sk7 ) ) ),
inference(simp,[status(thm)],[1318]) ).
thf(1320,plain,
( ( ^ [A: $i] : A )
!= ( ^ [A: $i] : sk7 ) ),
inference(pattern_uni,[status(thm)],[1319:[bind(A,$thf( ^ [C: $i] : C )),bind(B,$thf( ^ [C: $i] : sk7 ))]]) ).
thf(1339,plain,
sk8 != sk7,
inference(func_ext,[status(esa)],[1320]) ).
thf(1373,plain,
! [B: $i,A: $i > $i] :
( ~ ( sk1
@ ^ [C: $i] : C
@ A )
| ( B != sk7 )
| ( ( A @ B )
!= sk8 ) ),
inference(paramod_ordered,[status(thm)],[320,1339]) ).
thf(1374,plain,
! [A: $i] :
( ~ ( sk1
@ ^ [B: $i] : B
@ ^ [B: $i] : sk8 )
| ( A != sk7 ) ),
inference(pre_uni,[status(thm)],[1373:[bind(A,$thf( ^ [C: $i] : sk8 ))]]) ).
thf(1376,plain,
~ ( sk1
@ ^ [A: $i] : A
@ ^ [A: $i] : sk8 ),
inference(pattern_uni,[status(thm)],[1374:[bind(A,$thf( sk7 ))]]) ).
thf(1597,plain,
! [B: $i > $i,A: $i > $i] :
( ( A
!= ( ^ [C: $i] : ( B @ ( A @ C ) ) ) )
| ~ $true
| ( ( sk1 @ A @ B )
!= ( sk1
@ ^ [C: $i] : C
@ ^ [C: $i] : sk8 ) ) ),
inference(paramod_ordered,[status(thm)],[24,1376]) ).
thf(1598,plain,
! [B: $i > $i,A: $i > $i] :
( ( A
!= ( ^ [C: $i] : ( B @ ( A @ C ) ) ) )
| ( ( sk1 @ A @ B )
!= ( sk1
@ ^ [C: $i] : C
@ ^ [C: $i] : sk8 ) ) ),
inference(simp,[status(thm)],[1597]) ).
thf(1599,plain,
( ( ^ [A: $i] : A )
!= ( ^ [A: $i] : sk8 ) ),
inference(pattern_uni,[status(thm)],[1598:[bind(A,$thf( ^ [C: $i] : C )),bind(B,$thf( ^ [C: $i] : sk8 ))]]) ).
thf(1626,plain,
sk11 != sk8,
inference(func_ext,[status(esa)],[1599]) ).
thf(1660,plain,
! [B: $i,A: $i > $i] :
( ~ ( sk1
@ ^ [C: $i] : C
@ A )
| ( B != sk8 )
| ( ( A @ B )
!= sk11 ) ),
inference(paramod_ordered,[status(thm)],[320,1626]) ).
thf(1661,plain,
! [A: $i] :
( ~ ( sk1
@ ^ [B: $i] : B
@ ^ [B: $i] : sk11 )
| ( A != sk8 ) ),
inference(pre_uni,[status(thm)],[1660:[bind(A,$thf( ^ [C: $i] : sk11 ))]]) ).
thf(1663,plain,
~ ( sk1
@ ^ [A: $i] : A
@ ^ [A: $i] : sk11 ),
inference(pattern_uni,[status(thm)],[1661:[bind(A,$thf( sk8 ))]]) ).
thf(1927,plain,
! [B: $i > $i,A: $i > $i] :
( ( A
!= ( ^ [C: $i] : ( B @ ( A @ C ) ) ) )
| ~ $true
| ( ( sk1 @ A @ B )
!= ( sk1
@ ^ [C: $i] : C
@ ^ [C: $i] : sk11 ) ) ),
inference(paramod_ordered,[status(thm)],[24,1663]) ).
thf(1928,plain,
! [B: $i > $i,A: $i > $i] :
( ( A
!= ( ^ [C: $i] : ( B @ ( A @ C ) ) ) )
| ( ( sk1 @ A @ B )
!= ( sk1
@ ^ [C: $i] : C
@ ^ [C: $i] : sk11 ) ) ),
inference(simp,[status(thm)],[1927]) ).
thf(1929,plain,
( ( ^ [A: $i] : A )
!= ( ^ [A: $i] : sk11 ) ),
inference(pattern_uni,[status(thm)],[1928:[bind(A,$thf( ^ [C: $i] : C )),bind(B,$thf( ^ [C: $i] : sk11 ))]]) ).
thf(1974,plain,
! [B: $i,A: $i > $i] :
( ~ ( sk1
@ ^ [C: $i] : C
@ A )
| ( ( ^ [C: $i] : B )
!= ( ^ [C: $i] : C ) )
| ( ( A @ B )
!= sk11 ) ),
inference(paramod_ordered,[status(thm)],[320,1929]) ).
thf(1983,plain,
( ~ ( sk1
@ ^ [A: $i] : A
@ ^ [A: $i] : A )
| ( ( ^ [A: $i] : sk11 )
!= ( ^ [A: $i] : A ) ) ),
inference(pre_uni,[status(thm)],[1974:[bind(A,$thf( ^ [C: $i] : C )),bind(B,$thf( sk11 ))]]) ).
thf(1956,plain,
sk13 != sk11,
inference(func_ext,[status(esa)],[1929]) ).
thf(1990,plain,
! [B: $i,A: $i > $i] :
( ~ ( sk1
@ ^ [C: $i] : C
@ A )
| ( B != sk11 )
| ( ( A @ B )
!= sk13 ) ),
inference(paramod_ordered,[status(thm)],[320,1956]) ).
thf(1991,plain,
! [A: $i] :
( ~ ( sk1
@ ^ [B: $i] : B
@ ^ [B: $i] : sk13 )
| ( A != sk11 ) ),
inference(pre_uni,[status(thm)],[1990:[bind(A,$thf( ^ [C: $i] : sk13 ))]]) ).
thf(1993,plain,
~ ( sk1
@ ^ [A: $i] : A
@ ^ [A: $i] : sk13 ),
inference(pattern_uni,[status(thm)],[1991:[bind(A,$thf( sk11 ))]]) ).
thf(2290,plain,
! [B: $i > $i,A: $i > $i] :
( ( A
!= ( ^ [C: $i] : ( B @ ( A @ C ) ) ) )
| ~ $true
| ( ( sk1 @ A @ B )
!= ( sk1
@ ^ [C: $i] : C
@ ^ [C: $i] : sk13 ) ) ),
inference(paramod_ordered,[status(thm)],[24,1993]) ).
thf(2291,plain,
! [B: $i > $i,A: $i > $i] :
( ( A
!= ( ^ [C: $i] : ( B @ ( A @ C ) ) ) )
| ( ( sk1 @ A @ B )
!= ( sk1
@ ^ [C: $i] : C
@ ^ [C: $i] : sk13 ) ) ),
inference(simp,[status(thm)],[2290]) ).
thf(2292,plain,
( ( ^ [A: $i] : A )
!= ( ^ [A: $i] : sk13 ) ),
inference(pattern_uni,[status(thm)],[2291:[bind(A,$thf( ^ [C: $i] : C )),bind(B,$thf( ^ [C: $i] : sk13 ))]]) ).
thf(2319,plain,
sk16 != sk13,
inference(func_ext,[status(esa)],[2292]) ).
thf(26,plain,
! [B: $i > $i,A: $i > $i] :
( ( ( B @ ( A @ ( sk4 @ B @ A ) ) )
!= ( A @ ( sk4 @ B @ A ) ) )
| ( sk1 @ A @ B ) ),
inference(func_ext,[status(esa)],[24]) ).
thf(321,plain,
! [C: $i > $i,B: $i > $i,A: $i > $i] :
( ( sk2 @ B @ A @ A )
| ( ( ^ [D: $i] : D )
= C )
| ~ $true
| ( ( sk1 @ A @ B )
!= ( sk1
@ ^ [D: $i] : D
@ C ) ) ),
inference(paramod_ordered,[status(thm)],[5,307]) ).
thf(322,plain,
! [C: $i > $i,B: $i > $i,A: $i > $i] :
( ( sk2 @ B @ A @ A )
| ( ( ^ [D: $i] : D )
= C )
| ( ( sk1 @ A @ B )
!= ( sk1
@ ^ [D: $i] : D
@ C ) ) ),
inference(simp,[status(thm)],[321]) ).
thf(323,plain,
! [A: $i > $i] :
( ( sk2 @ A
@ ^ [B: $i] : B
@ ^ [B: $i] : B )
| ( ( ^ [B: $i] : B )
= A ) ),
inference(pattern_uni,[status(thm)],[322:[bind(A,$thf( ^ [D: $i] : D )),bind(B,$thf( B )),bind(C,$thf( B ))]]) ).
thf(404,plain,
! [A: $i > $i] :
( ( sk2 @ A
@ ^ [B: $i] : B
@ ^ [B: $i] : B )
| ( ( ^ [B: $i] : B )
= A ) ),
inference(simp,[status(thm)],[323]) ).
thf(1361,plain,
! [A: $i > $i] :
( ( sk2 @ A
@ ^ [B: $i] : B
@ ^ [B: $i] : B )
| ( ( ^ [B: $i] : B )
!= ( ^ [B: $i] : B ) )
| ( A
!= ( ^ [B: $i] : sk7 ) ) ),
inference(paramod_ordered,[status(thm)],[404,1320]) ).
thf(1362,plain,
! [A: $i > $i] :
( ( sk2 @ A
@ ^ [B: $i] : B
@ ^ [B: $i] : B )
| ( A
!= ( ^ [B: $i] : sk7 ) ) ),
inference(simp,[status(thm)],[1361]) ).
thf(1363,plain,
( sk2
@ ^ [A: $i] : sk7
@ ^ [A: $i] : A
@ ^ [A: $i] : A ),
inference(pattern_uni,[status(thm)],[1362:[bind(A,$thf( ^ [B: $i] : sk7 ))]]) ).
thf(2334,plain,
! [A: $i > $i] :
( ( sk2 @ A
@ ^ [B: $i] : B
@ ^ [B: $i] : B )
| ( ( ^ [B: $i] : B )
!= ( ^ [B: $i] : B ) )
| ( A
!= ( ^ [B: $i] : sk13 ) ) ),
inference(paramod_ordered,[status(thm)],[404,2292]) ).
thf(2335,plain,
! [A: $i > $i] :
( ( sk2 @ A
@ ^ [B: $i] : B
@ ^ [B: $i] : B )
| ( A
!= ( ^ [B: $i] : sk13 ) ) ),
inference(simp,[status(thm)],[2334]) ).
thf(2336,plain,
( sk2
@ ^ [A: $i] : sk13
@ ^ [A: $i] : A
@ ^ [A: $i] : A ),
inference(pattern_uni,[status(thm)],[2335:[bind(A,$thf( ^ [B: $i] : sk13 ))]]) ).
thf(927,plain,
! [B: $i,A: $i > $i] :
( ~ ( sk1
@ ^ [C: $i] : C
@ A )
| ( ( ^ [C: $i] : B )
!= ( ^ [C: $i] : C ) )
| ( ( A @ B )
!= a ) ),
inference(paramod_ordered,[status(thm)],[320,889]) ).
thf(930,plain,
( ~ ( sk1
@ ^ [A: $i] : A
@ ^ [A: $i] : A )
| ( ( ^ [A: $i] : a )
!= ( ^ [A: $i] : A ) ) ),
inference(pre_uni,[status(thm)],[927:[bind(A,$thf( ^ [C: $i] : C )),bind(B,$thf( a ))]]) ).
thf(27,plain,
! [E: ( $i > $i ) > $o,D: $i > $i,C: $i > $i,B: $i > $i,A: $i > $i] :
( ( sk1 @ A @ B )
| ~ ( sk1 @ C @ D )
| ~ $true
| ~ ( E
@ ^ [F: $i] : ( C @ ( sk3 @ E @ D @ C @ F ) ) )
| ( E @ D )
| ( ( sk2 @ B @ A @ A )
!= ( E @ C ) ) ),
inference(paramod_ordered,[status(thm)],[5,13]) ).
thf(28,plain,
! [E: ( $i > $i ) > $o,D: $i > $i,C: $i > $i,B: $i > $i,A: $i > $i] :
( ( sk1 @ A @ B )
| ~ ( sk1 @ C @ D )
| ~ ( E
@ ^ [F: $i] : ( C @ ( sk3 @ E @ D @ C @ F ) ) )
| ( E @ D )
| ( ( sk2 @ B @ A @ A )
!= ( E @ C ) ) ),
inference(simp,[status(thm)],[27]) ).
thf(69,plain,
! [E: ( $i > $i ) > $o,D: $i > $i,C: $i > $i,B: $i > $i,A: $i > $i] :
( ( sk1 @ A @ B )
| ~ ( sk1 @ C @ D )
| ( ( ^ [F: $i] : ( C @ ( sk3 @ E @ D @ C @ F ) ) )
!= ( ^ [F: $i] :
( C
@ ( sk3
@ ( (=) @ ( $i > $i )
@ ^ [G: $i] : ( C @ ( sk3 @ E @ D @ C @ G ) ) )
@ D
@ C
@ F ) ) ) )
| ( ( ^ [F: $i] : ( C @ ( sk3 @ E @ D @ C @ F ) ) )
= D )
| ( ( sk2 @ B @ A @ A )
!= ( ( ^ [F: $i] : ( C @ ( sk3 @ E @ D @ C @ F ) ) )
= C ) ) ),
inference(replace_leibeq,[status(thm)],[28:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( (=) @ ( $i > $i ) @ ^ [F: $i] : ( C @ ( sk3 @ E @ D @ C @ F ) ) ))]]) ).
thf(78,plain,
! [E: ( $i > $i ) > $o,D: $i > $i,C: $i > $i,B: $i > $i,A: $i > $i] :
( ( ( ^ [F: $i] : ( C @ ( sk3 @ E @ D @ C @ F ) ) )
!= ( ^ [F: $i] :
( C
@ ( sk3
@ ( (=) @ ( $i > $i )
@ ^ [G: $i] : ( C @ ( sk3 @ E @ D @ C @ G ) ) )
@ D
@ C
@ F ) ) ) )
| ( ( ^ [F: $i] : ( C @ ( sk3 @ E @ D @ C @ F ) ) )
= D )
| ( sk1 @ A @ B )
| ~ ( sk1 @ C @ D )
| ( ( sk2 @ B @ A @ A )
!= ( ( ^ [F: $i] : ( C @ ( sk3 @ E @ D @ C @ F ) ) )
= C ) ) ),
inference(lifteq,[status(thm)],[69]) ).
thf(53,plain,
! [C: ( $i > $i ) > $o,B: $i > $i,A: $i > $i] :
( ~ ( sk1 @ A @ B )
| ~ ( C @ A )
| ( C @ B )
| ( ( C
@ ^ [D: $i] : ( A @ ( sk3 @ C @ B @ A @ D ) ) )
!= ( sk1 @ A @ B ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[13]) ).
thf(100,plain,
! [D: ( $i > $i ) > $i > $i,C: ( $i > $i ) > $i > $i,B: $i > $i,A: $i > $i] :
( ~ ( sk1 @ A @ B )
| ~ ( sk1 @ ( C @ A ) @ ( D @ A ) )
| ( sk1 @ ( C @ B ) @ ( D @ B ) )
| ( ( D
@ ^ [E: $i] :
( A
@ ( sk3
@ ^ [F: $i > $i] : ( sk1 @ ( C @ F ) @ ( D @ F ) )
@ B
@ A
@ E ) ) )
!= B )
| ( ( C
@ ^ [E: $i] :
( A
@ ( sk3
@ ^ [F: $i > $i] : ( sk1 @ ( C @ F ) @ ( D @ F ) )
@ B
@ A
@ E ) ) )
!= A ) ),
inference(pre_uni,[status(thm)],[53:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( ^ [F: $i > $i] : ( sk1 @ ( D @ F ) @ ( E @ F ) ) ))]]) ).
thf(101,plain,
! [D: ( $i > $i ) > $i > $i,C: ( $i > $i ) > $i > $i,B: $i > $i,A: $i > $i] :
( ( sk1 @ ( C @ B ) @ ( D @ B ) )
| ~ ( sk1 @ ( C @ A ) @ ( D @ A ) )
| ~ ( sk1 @ A @ B )
| ( ( D
@ ^ [E: $i] :
( A
@ ( sk3
@ ^ [F: $i > $i] : ( sk1 @ ( C @ F ) @ ( D @ F ) )
@ B
@ A
@ E ) ) )
!= B )
| ( ( C
@ ^ [E: $i] :
( A
@ ( sk3
@ ^ [F: $i > $i] : ( sk1 @ ( C @ F ) @ ( D @ F ) )
@ B
@ A
@ E ) ) )
!= A ) ),
inference(pre_uni,[status(thm)],[100:[]]) ).
thf(128,plain,
! [D: ( $i > $i ) > $i > $i,C: ( $i > $i ) > $i > $i,B: $i > $i,A: $i > $i] :
( ( sk1 @ ( C @ B ) @ ( D @ B ) )
| ~ ( sk1 @ ( C @ A ) @ ( D @ A ) )
| ~ ( sk1 @ A @ B )
| ( ( D
@ ^ [E: $i] :
( A
@ ( sk3
@ ^ [F: $i > $i] : ( sk1 @ ( C @ F ) @ ( D @ F ) )
@ B
@ A
@ E ) ) )
!= B )
| ( ( C
@ ^ [E: $i] :
( A
@ ( sk3
@ ^ [F: $i > $i] : ( sk1 @ ( C @ F ) @ ( D @ F ) )
@ B
@ A
@ E ) ) )
!= A ) ),
inference(simp,[status(thm)],[101]) ).
thf(924,plain,
! [A: $i > $i] :
( ( sk2 @ A
@ ^ [B: $i] : B
@ ^ [B: $i] : B )
| ( ( ^ [B: $i] : B )
!= ( ^ [B: $i] : B ) )
| ( A
!= ( ^ [B: $i] : a ) ) ),
inference(paramod_ordered,[status(thm)],[404,889]) ).
thf(925,plain,
! [A: $i > $i] :
( ( sk2 @ A
@ ^ [B: $i] : B
@ ^ [B: $i] : B )
| ( A
!= ( ^ [B: $i] : a ) ) ),
inference(simp,[status(thm)],[924]) ).
thf(926,plain,
( sk2
@ ^ [A: $i] : a
@ ^ [A: $i] : A
@ ^ [A: $i] : A ),
inference(pattern_uni,[status(thm)],[925:[bind(A,$thf( ^ [B: $i] : a ))]]) ).
thf(7,plain,
! [C: $i > $i,B: $i > $i,A: $i > $i] :
( ~ ( sk2 @ B @ A @ C )
| ( sk2 @ B @ A
@ ^ [D: $i] : ( A @ ( C @ D ) ) )
| ( sk1 @ A @ B ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(1641,plain,
! [A: $i > $i] :
( ( sk2 @ A
@ ^ [B: $i] : B
@ ^ [B: $i] : B )
| ( ( ^ [B: $i] : B )
!= ( ^ [B: $i] : B ) )
| ( A
!= ( ^ [B: $i] : sk8 ) ) ),
inference(paramod_ordered,[status(thm)],[404,1599]) ).
thf(1642,plain,
! [A: $i > $i] :
( ( sk2 @ A
@ ^ [B: $i] : B
@ ^ [B: $i] : B )
| ( A
!= ( ^ [B: $i] : sk8 ) ) ),
inference(simp,[status(thm)],[1641]) ).
thf(1643,plain,
( sk2
@ ^ [A: $i] : sk8
@ ^ [A: $i] : A
@ ^ [A: $i] : A ),
inference(pattern_uni,[status(thm)],[1642:[bind(A,$thf( ^ [B: $i] : sk8 ))]]) ).
thf(1971,plain,
! [A: $i > $i] :
( ( sk2 @ A
@ ^ [B: $i] : B
@ ^ [B: $i] : B )
| ( ( ^ [B: $i] : B )
!= ( ^ [B: $i] : B ) )
| ( A
!= ( ^ [B: $i] : sk11 ) ) ),
inference(paramod_ordered,[status(thm)],[404,1929]) ).
thf(1972,plain,
! [A: $i > $i] :
( ( sk2 @ A
@ ^ [B: $i] : B
@ ^ [B: $i] : B )
| ( A
!= ( ^ [B: $i] : sk11 ) ) ),
inference(simp,[status(thm)],[1971]) ).
thf(1973,plain,
( sk2
@ ^ [A: $i] : sk11
@ ^ [A: $i] : A
@ ^ [A: $i] : A ),
inference(pattern_uni,[status(thm)],[1972:[bind(A,$thf( ^ [B: $i] : sk11 ))]]) ).
thf(11,plain,
! [B: $i > $i,A: $i > $i] :
( ~ ( sk1 @ A @ B )
| ( A != A )
| ( A
!= ( ^ [C: $i] : ( A @ ( sk3 @ ( (=) @ ( $i > $i ) @ A ) @ B @ A @ C ) ) ) )
| ( A = B ) ),
inference(replace_leibeq,[status(thm)],[6:[bind(A,$thf( (@) )),bind(B,$thf( A )),bind(C,$thf( (=) @ ( $i > $i ) @ (@) ))]]) ).
thf(17,plain,
! [B: $i > $i,A: $i > $i] :
( ( A != A )
| ( ( ^ [C: $i] : ( A @ ( sk3 @ ( (=) @ ( $i > $i ) @ A ) @ B @ A @ C ) ) )
!= A )
| ( A = B )
| ~ ( sk1 @ A @ B ) ),
inference(lifteq,[status(thm)],[11]) ).
thf(18,plain,
! [B: $i > $i,A: $i > $i] :
( ( ( ^ [C: $i] : ( A @ ( sk3 @ ( (=) @ ( $i > $i ) @ A ) @ B @ A @ C ) ) )
!= A )
| ( A = B )
| ~ ( sk1 @ A @ B ) ),
inference(simp,[status(thm)],[17]) ).
thf(326,plain,
! [C: $i > $i,B: $i > $i,A: $i > $i] :
( ~ ( sk2 @ B @ A
@ ^ [D: $i] : ( B @ ( A @ D ) ) )
| ( ( ^ [D: $i] : D )
= C )
| ~ $true
| ( ( sk1 @ A @ B )
!= ( sk1
@ ^ [D: $i] : D
@ C ) ) ),
inference(paramod_ordered,[status(thm)],[10,307]) ).
thf(327,plain,
! [C: $i > $i,B: $i > $i,A: $i > $i] :
( ~ ( sk2 @ B @ A
@ ^ [D: $i] : ( B @ ( A @ D ) ) )
| ( ( ^ [D: $i] : D )
= C )
| ( ( sk1 @ A @ B )
!= ( sk1
@ ^ [D: $i] : D
@ C ) ) ),
inference(simp,[status(thm)],[326]) ).
thf(328,plain,
! [A: $i > $i] :
( ~ ( sk2 @ A
@ ^ [B: $i] : B
@ A )
| ( ( ^ [B: $i] : B )
= A ) ),
inference(pattern_uni,[status(thm)],[327:[bind(A,$thf( ^ [D: $i] : D )),bind(B,$thf( B )),bind(C,$thf( B ))]]) ).
thf(409,plain,
! [A: $i > $i] :
( ~ ( sk2 @ A
@ ^ [B: $i] : B
@ A )
| ( ( ^ [B: $i] : B )
= A ) ),
inference(simp,[status(thm)],[328]) ).
thf(1644,plain,
! [B: $i,A: $i > $i] :
( ~ ( sk1
@ ^ [C: $i] : C
@ A )
| ( ( ^ [C: $i] : B )
!= ( ^ [C: $i] : C ) )
| ( ( A @ B )
!= sk8 ) ),
inference(paramod_ordered,[status(thm)],[320,1599]) ).
thf(1653,plain,
( ~ ( sk1
@ ^ [A: $i] : A
@ ^ [A: $i] : A )
| ( ( ^ [A: $i] : sk8 )
!= ( ^ [A: $i] : A ) ) ),
inference(pre_uni,[status(thm)],[1644:[bind(A,$thf( ^ [C: $i] : C )),bind(B,$thf( sk8 ))]]) ).
thf(1364,plain,
! [B: $i,A: $i > $i] :
( ~ ( sk1
@ ^ [C: $i] : C
@ A )
| ( ( ^ [C: $i] : B )
!= ( ^ [C: $i] : C ) )
| ( ( A @ B )
!= sk7 ) ),
inference(paramod_ordered,[status(thm)],[320,1320]) ).
thf(1367,plain,
( ~ ( sk1
@ ^ [A: $i] : A
@ ^ [A: $i] : A )
| ( ( ^ [A: $i] : sk7 )
!= ( ^ [A: $i] : A ) ) ),
inference(pre_uni,[status(thm)],[1364:[bind(A,$thf( ^ [C: $i] : C )),bind(B,$thf( sk7 ))]]) ).
thf(3468,plain,
$false,
inference(e,[status(thm)],[5,14,307,889,1983,2292,1929,2319,16,26,19,1363,839,2336,1956,10,930,404,24,320,902,78,13,1599,128,1663,926,7,1376,1339,1993,1643,3,1973,1626,939,18,409,1320,1653,1367]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU933^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.09/0.18 % Computer : n020.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Tue Sep 29 14:47:49 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.90/0.77 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.26/0.97 % [INFO] Parsing done (197ms).
% 1.26/0.98 % [INFO] Running in sequential loop mode.
% 1.91/1.38 % [INFO] eprover registered as external prover.
% 1.91/1.39 % [INFO] Scanning for conjecture ...
% 2.10/1.49 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 2.28/1.52 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 2.28/1.52 % [INFO] Problem is higher-order (TPTP THF).
% 2.28/1.53 % [INFO] Type checking passed.
% 2.28/1.53 % [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 ...
% 45.43/12.32 % External prover 'e' found a proof!
% 45.43/12.32 % [INFO] Killing All external provers ...
% 45.43/12.32 % Time passed: 12001ms (effective reasoning time: 11332ms)
% 45.43/12.32 % 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)>
% 45.43/12.32 % Axioms used in derivation (0):
% 45.43/12.32 % No. of inferences in proof: 106
% 45.43/12.32 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 12001 ms resp. 11332 ms w/o parsing
% 45.43/12.39 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 45.43/12.39 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------