%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SYO250^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 : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:45:28 AM UTC 2026
% Result : Theorem 4.70s 2.61s
% Output : Refutation 5.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 2
% Syntax : Number of formulae : 9 ( 4 unt; 0 typ; 1 def)
% Number of atoms : 486 ( 485 equ; 0 cnn)
% Maximal formula atoms : 90 ( 54 avg)
% Number of connectives : 2004 ( 376 ~; 45 |; 392 &;1152 @)
% ( 0 <=>; 39 =>; 0 <=; 0 <~>)
% Maximal formula depth : 199 ( 54 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 5 ( 5 >; 0 *; 0 +; 0 <<)
% Number of symbols : 3 ( 1 usr; 1 con; 0-13 aty)
% Number of variables : 313 ( 12 ^; 136 !; 164 ?; 313 :)
% ( 0 !>; 0 ?*; 0 @-; 1 @+)
% Comments :
%------------------------------------------------------------------------------
thf(sk1_decl,type,
sk1: $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $i > $i ).
thf(sk1_def,definition,
( sk1
= ( ^ [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i,I: $i,J: $i,K: $i,L: $i] :
@+[M: $i > $i] :
~ ( ( ( ( ( ( M @ L )
= ( M @ K ) )
& ( ( M @ J )
= ( M @ I ) )
& ( ( M @ D )
= ( M @ A ) ) )
=> ( ( M @ H )
= ( M @ E ) ) )
& ( ( ( ( M @ L )
= ( M @ K ) )
& ( ( M @ B )
= ( M @ A ) )
& ( ( M @ J )
= ( M @ G ) ) )
=> ( ( M @ F )
!= ( M @ C ) ) )
& ( ( ( ( M @ H )
= ( M @ G ) )
& ( ( M @ G )
= ( M @ F ) )
& ( ( M @ F )
= ( M @ E ) )
& ( ( M @ L )
!= ( M @ I ) ) )
=> ( ( M @ D )
!= ( M @ A ) ) )
& ( ( ( ( M @ L )
= ( M @ K ) )
& ( ( M @ F )
= ( M @ E ) )
& ( ( M @ J )
!= ( M @ G ) ) )
=> ( ( M @ D )
= ( M @ A ) ) )
& ( ( ( ( M @ D )
= ( M @ C ) )
& ( ( M @ B )
= ( M @ A ) )
& ( ( M @ H )
= ( M @ E ) ) )
=> ( ( M @ L )
!= ( M @ I ) ) )
& ( ( ( ( M @ J )
= ( M @ I ) )
& ( ( M @ I )
= ( M @ H ) )
& ( ( M @ H )
= ( M @ G ) )
& ( ( M @ D )
!= ( M @ A ) ) )
=> ( ( M @ F )
= ( M @ C ) ) ) )
=> ( ( ( M @ L )
!= ( M @ K ) )
| ( ( M @ J )
!= ( M @ I ) )
| ( ( M @ H )
!= ( M @ G ) )
| ( ( M @ F )
!= ( M @ E ) )
| ( ( M @ D )
!= ( M @ C ) )
| ( ( M @ B )
!= ( M @ A ) ) ) ) ) ) ).
thf(1,conjecture,
? [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i,I: $i,J: $i,K: $i,L: $i] :
( ( ( A != B )
& ( A != C )
& ( A != D )
& ( A != E )
& ( A != F )
& ( A != G )
& ( A != H )
& ( A != I )
& ( A != J )
& ( A != K )
& ( A != L )
& ( B != C )
& ( B != D )
& ( B != E )
& ( B != F )
& ( B != G )
& ( B != H )
& ( B != I )
& ( B != J )
& ( B != K )
& ( B != L )
& ( C != D )
& ( C != E )
& ( C != F )
& ( C != G )
& ( C != H )
& ( C != I )
& ( C != J )
& ( C != K )
& ( C != L )
& ( E != F )
& ( E != G )
& ( E != H )
& ( E != I )
& ( E != J )
& ( E != K )
& ( E != L )
& ( F != G )
& ( F != H )
& ( F != I )
& ( F != J )
& ( F != K )
& ( F != L )
& ( G != H )
& ( G != I )
& ( G != J )
& ( G != K )
& ( G != L )
& ( H != I )
& ( H != J )
& ( H != K )
& ( H != L )
& ( I != J )
& ( I != K )
& ( I != L )
& ( J != K )
& ( J != L )
& ( K != L ) )
=> ! [M: $i > $i] :
( ( ( ( ( ( M @ A )
= ( M @ B ) )
& ( ( M @ C )
= ( M @ D ) )
& ( ( M @ I )
= ( M @ L ) ) )
=> ( ( M @ E )
= ( M @ H ) ) )
& ( ( ( ( M @ A )
= ( M @ B ) )
& ( ( M @ K )
= ( M @ L ) )
& ( ( M @ C )
= ( M @ F ) ) )
=> ( ( M @ G )
!= ( M @ J ) ) )
& ( ( ( ( M @ E )
= ( M @ F ) )
& ( ( M @ F )
= ( M @ G ) )
& ( ( M @ G )
= ( M @ H ) )
& ( ( M @ A )
!= ( M @ D ) ) )
=> ( ( M @ I )
!= ( M @ L ) ) )
& ( ( ( ( M @ A )
= ( M @ B ) )
& ( ( M @ G )
= ( M @ H ) )
& ( ( M @ C )
!= ( M @ F ) ) )
=> ( ( M @ I )
= ( M @ L ) ) )
& ( ( ( ( M @ I )
= ( M @ J ) )
& ( ( M @ K )
= ( M @ L ) )
& ( ( M @ E )
= ( M @ H ) ) )
=> ( ( M @ A )
!= ( M @ D ) ) )
& ( ( ( ( M @ C )
= ( M @ D ) )
& ( ( M @ D )
= ( M @ E ) )
& ( ( M @ E )
= ( M @ F ) )
& ( ( M @ I )
!= ( M @ L ) ) )
=> ( ( M @ G )
= ( M @ J ) ) ) )
=> ( ( ( M @ A )
!= ( M @ B ) )
| ( ( M @ C )
!= ( M @ D ) )
| ( ( M @ E )
!= ( M @ F ) )
| ( ( M @ G )
!= ( M @ H ) )
| ( ( M @ I )
!= ( M @ J ) )
| ( ( M @ K )
!= ( M @ L ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cSIXFRIENDS) ).
thf(2,negated_conjecture,
~ ? [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i,I: $i,J: $i,K: $i,L: $i] :
( ( ( A != B )
& ( A != C )
& ( A != D )
& ( A != E )
& ( A != F )
& ( A != G )
& ( A != H )
& ( A != I )
& ( A != J )
& ( A != K )
& ( A != L )
& ( B != C )
& ( B != D )
& ( B != E )
& ( B != F )
& ( B != G )
& ( B != H )
& ( B != I )
& ( B != J )
& ( B != K )
& ( B != L )
& ( C != D )
& ( C != E )
& ( C != F )
& ( C != G )
& ( C != H )
& ( C != I )
& ( C != J )
& ( C != K )
& ( C != L )
& ( E != F )
& ( E != G )
& ( E != H )
& ( E != I )
& ( E != J )
& ( E != K )
& ( E != L )
& ( F != G )
& ( F != H )
& ( F != I )
& ( F != J )
& ( F != K )
& ( F != L )
& ( G != H )
& ( G != I )
& ( G != J )
& ( G != K )
& ( G != L )
& ( H != I )
& ( H != J )
& ( H != K )
& ( H != L )
& ( I != J )
& ( I != K )
& ( I != L )
& ( J != K )
& ( J != L )
& ( K != L ) )
=> ! [M: $i > $i] :
( ( ( ( ( ( M @ A )
= ( M @ B ) )
& ( ( M @ C )
= ( M @ D ) )
& ( ( M @ I )
= ( M @ L ) ) )
=> ( ( M @ E )
= ( M @ H ) ) )
& ( ( ( ( M @ A )
= ( M @ B ) )
& ( ( M @ K )
= ( M @ L ) )
& ( ( M @ C )
= ( M @ F ) ) )
=> ( ( M @ G )
!= ( M @ J ) ) )
& ( ( ( ( M @ E )
= ( M @ F ) )
& ( ( M @ F )
= ( M @ G ) )
& ( ( M @ G )
= ( M @ H ) )
& ( ( M @ A )
!= ( M @ D ) ) )
=> ( ( M @ I )
!= ( M @ L ) ) )
& ( ( ( ( M @ A )
= ( M @ B ) )
& ( ( M @ G )
= ( M @ H ) )
& ( ( M @ C )
!= ( M @ F ) ) )
=> ( ( M @ I )
= ( M @ L ) ) )
& ( ( ( ( M @ I )
= ( M @ J ) )
& ( ( M @ K )
= ( M @ L ) )
& ( ( M @ E )
= ( M @ H ) ) )
=> ( ( M @ A )
!= ( M @ D ) ) )
& ( ( ( ( M @ C )
= ( M @ D ) )
& ( ( M @ D )
= ( M @ E ) )
& ( ( M @ E )
= ( M @ F ) )
& ( ( M @ I )
!= ( M @ L ) ) )
=> ( ( M @ G )
= ( M @ J ) ) ) )
=> ( ( ( M @ A )
!= ( M @ B ) )
| ( ( M @ C )
!= ( M @ D ) )
| ( ( M @ E )
!= ( M @ F ) )
| ( ( M @ G )
!= ( M @ H ) )
| ( ( M @ I )
!= ( M @ J ) )
| ( ( M @ K )
!= ( M @ L ) ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(3,plain,
~ ? [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i,I: $i,J: $i,K: $i,L: $i] :
( ( ( A != B )
& ( A != C )
& ( A != D )
& ( A != E )
& ( A != F )
& ( A != G )
& ( A != H )
& ( A != I )
& ( A != J )
& ( A != K )
& ( A != L )
& ( B != C )
& ( B != D )
& ( B != E )
& ( B != F )
& ( B != G )
& ( B != H )
& ( B != I )
& ( B != J )
& ( B != K )
& ( B != L )
& ( C != D )
& ( C != E )
& ( C != F )
& ( C != G )
& ( C != H )
& ( C != I )
& ( C != J )
& ( C != K )
& ( C != L )
& ( E != F )
& ( E != G )
& ( E != H )
& ( E != I )
& ( E != J )
& ( E != K )
& ( E != L )
& ( F != G )
& ( F != H )
& ( F != I )
& ( F != J )
& ( F != K )
& ( F != L )
& ( G != H )
& ( G != I )
& ( G != J )
& ( G != K )
& ( G != L )
& ( H != I )
& ( H != J )
& ( H != K )
& ( H != L )
& ( I != J )
& ( I != K )
& ( I != L )
& ( J != K )
& ( J != L )
& ( K != L ) )
=> ! [M: $i > $i] :
( ( ( ( ( ( M @ A )
= ( M @ B ) )
& ( ( M @ C )
= ( M @ D ) )
& ( ( M @ I )
= ( M @ L ) ) )
=> ( ( M @ E )
= ( M @ H ) ) )
& ( ( ( ( M @ A )
= ( M @ B ) )
& ( ( M @ K )
= ( M @ L ) )
& ( ( M @ C )
= ( M @ F ) ) )
=> ( ( M @ G )
!= ( M @ J ) ) )
& ( ( ( ( M @ E )
= ( M @ F ) )
& ( ( M @ F )
= ( M @ G ) )
& ( ( M @ G )
= ( M @ H ) )
& ( ( M @ A )
!= ( M @ D ) ) )
=> ( ( M @ I )
!= ( M @ L ) ) )
& ( ( ( ( M @ A )
= ( M @ B ) )
& ( ( M @ G )
= ( M @ H ) )
& ( ( M @ C )
!= ( M @ F ) ) )
=> ( ( M @ I )
= ( M @ L ) ) )
& ( ( ( ( M @ I )
= ( M @ J ) )
& ( ( M @ K )
= ( M @ L ) )
& ( ( M @ E )
= ( M @ H ) ) )
=> ( ( M @ A )
!= ( M @ D ) ) )
& ( ( ( ( M @ C )
= ( M @ D ) )
& ( ( M @ D )
= ( M @ E ) )
& ( ( M @ E )
= ( M @ F ) )
& ( ( M @ I )
!= ( M @ L ) ) )
=> ( ( M @ G )
= ( M @ J ) ) ) )
=> ( ( ( M @ A )
!= ( M @ B ) )
| ( ( M @ C )
!= ( M @ D ) )
| ( ( M @ E )
!= ( M @ F ) )
| ( ( M @ G )
!= ( M @ H ) )
| ( ( M @ I )
!= ( M @ J ) )
| ( ( M @ K )
!= ( M @ L ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(4,plain,
~ ( ( ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B )
& ~ ? [A: $i,B: $i] : ( A = B ) )
=> ? [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i,I: $i,J: $i,K: $i,L: $i] :
! [M: $i > $i] :
( ( ( ( ( ( M @ A )
= ( M @ B ) )
& ( ( M @ C )
= ( M @ D ) )
& ( ( M @ I )
= ( M @ L ) ) )
=> ( ( M @ E )
= ( M @ H ) ) )
& ( ( ( ( M @ A )
= ( M @ B ) )
& ( ( M @ K )
= ( M @ L ) )
& ( ( M @ C )
= ( M @ F ) ) )
=> ( ( M @ G )
!= ( M @ J ) ) )
& ( ( ( ( M @ E )
= ( M @ F ) )
& ( ( M @ F )
= ( M @ G ) )
& ( ( M @ G )
= ( M @ H ) )
& ( ( M @ A )
!= ( M @ D ) ) )
=> ( ( M @ I )
!= ( M @ L ) ) )
& ( ( ( ( M @ A )
= ( M @ B ) )
& ( ( M @ G )
= ( M @ H ) )
& ( ( M @ C )
!= ( M @ F ) ) )
=> ( ( M @ I )
= ( M @ L ) ) )
& ( ( ( ( M @ I )
= ( M @ J ) )
& ( ( M @ K )
= ( M @ L ) )
& ( ( M @ E )
= ( M @ H ) ) )
=> ( ( M @ A )
!= ( M @ D ) ) )
& ( ( ( ( M @ C )
= ( M @ D ) )
& ( ( M @ D )
= ( M @ E ) )
& ( ( M @ E )
= ( M @ F ) )
& ( ( M @ I )
!= ( M @ L ) ) )
=> ( ( M @ G )
= ( M @ J ) ) ) )
=> ( ( ( M @ A )
!= ( M @ B ) )
| ( ( M @ C )
!= ( M @ D ) )
| ( ( M @ E )
!= ( M @ F ) )
| ( ( M @ G )
!= ( M @ H ) )
| ( ( M @ I )
!= ( M @ J ) )
| ( ( M @ K )
!= ( M @ L ) ) ) ) ),
inference(miniscope,[status(thm)],[3]) ).
thf(5,plain,
! [ZZZZX: $i,ZZZZW: $i,ZZZZV: $i,ZZZZU: $i,ZZZZT: $i,ZZZZS: $i,ZZZZR: $i,ZZZZQ: $i,ZZZZP: $i,ZZZZO: $i,ZZZZN: $i,ZZZZM: $i,ZZZZL: $i,ZZZZK: $i,ZZZZJ: $i,ZZZZI: $i,ZZZZH: $i,ZZZZG: $i,ZZZZF: $i,ZZZZE: $i,ZZZZD: $i,ZZZZC: $i,ZZZZB: $i,ZZZZA: $i,ZZZZ: $i,ZZZY: $i,ZZZX: $i,ZZZW: $i,ZZZV: $i,ZZZU: $i,ZZZT: $i,ZZZS: $i,ZZZR: $i,ZZZQ: $i,ZZZP: $i,ZZZO: $i,ZZZN: $i,ZZZM: $i,ZZZL: $i,ZZZK: $i,ZZZJ: $i,ZZZI: $i,ZZZH: $i,ZZZG: $i,ZZZF: $i,ZZZE: $i,ZZZD: $i,ZZZC: $i,ZZZB: $i,ZZZA: $i,ZZZ: $i,ZZY: $i,ZZX: $i,ZZW: $i,ZZV: $i,ZZU: $i,ZZT: $i,ZZS: $i,ZZR: $i,ZZQ: $i,ZZP: $i,ZZO: $i,ZZN: $i,ZZM: $i,ZZL: $i,ZZK: $i,ZZJ: $i,ZZI: $i,ZZH: $i,ZZG: $i,ZZF: $i,ZZE: $i,ZZD: $i,ZZC: $i,ZZB: $i,ZZA: $i,ZZ: $i,ZY: $i,ZX: $i,ZW: $i,ZV: $i,ZU: $i,ZT: $i,ZS: $i,ZR: $i,ZQ: $i,ZP: $i,ZO: $i,ZN: $i,ZM: $i,ZL: $i,ZK: $i,ZJ: $i,ZI: $i,ZH: $i,ZG: $i,ZF: $i,ZE: $i,ZD: $i,ZC: $i,ZB: $i,ZA: $i,Z: $i,Y: $i,X: $i,W: $i,V: $i,U: $i,T: $i,S: $i,R: $i,Q: $i,P: $i,O: $i,N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( A != B )
& ( C != D )
& ( E != F )
& ( G != H )
& ( I != J )
& ( K != L )
& ( M != N )
& ( O != P )
& ( Q != R )
& ( S != T )
& ( U != V )
& ( W != X )
& ( Y != Z )
& ( ZA != ZB )
& ( ZC != ZD )
& ( ZE != ZF )
& ( ZG != ZH )
& ( ZI != ZJ )
& ( ZK != ZL )
& ( ZM != ZN )
& ( ZO != ZP )
& ( ZQ != ZR )
& ( ZS != ZT )
& ( ZU != ZV )
& ( ZW != ZX )
& ( ZY != ZZ )
& ( ZZA != ZZB )
& ( ZZC != ZZD )
& ( ZZE != ZZF )
& ( ZZG != ZZH )
& ( ZZI != ZZJ )
& ( ZZK != ZZL )
& ( ZZM != ZZN )
& ( ZZO != ZZP )
& ( ZZQ != ZZR )
& ( ZZS != ZZT )
& ( ZZU != ZZV )
& ( ZZW != ZZX )
& ( ZZY != ZZZ )
& ( ZZZA != ZZZB )
& ( ZZZC != ZZZD )
& ( ZZZE != ZZZF )
& ( ZZZG != ZZZH )
& ( ZZZI != ZZZJ )
& ( ZZZK != ZZZL )
& ( ZZZM != ZZZN )
& ( ZZZO != ZZZP )
& ( ZZZQ != ZZZR )
& ( ZZZS != ZZZT )
& ( ZZZU != ZZZV )
& ( ZZZW != ZZZX )
& ( ZZZY != ZZZZ )
& ( ZZZZA != ZZZZB )
& ( ZZZZC != ZZZZD )
& ( ZZZZE != ZZZZF )
& ( ZZZZG != ZZZZH )
& ( ZZZZI != ZZZZJ )
& ( ZZZZK != ZZZZL )
& ( ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZM )
!= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZN ) )
| ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZO )
!= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZP ) )
| ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZU )
!= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZX ) )
| ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZQ )
= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZT ) ) )
& ( ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZM )
!= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZN ) )
| ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZW )
!= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZX ) )
| ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZO )
!= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZR ) )
| ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZS )
!= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZV ) ) )
& ( ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZQ )
!= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZR ) )
| ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZR )
!= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZS ) )
| ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZS )
!= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZT ) )
| ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZM )
= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZP ) )
| ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZU )
!= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZX ) ) )
& ( ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZM )
!= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZN ) )
| ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZS )
!= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZT ) )
| ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZO )
= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZR ) )
| ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZU )
= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZX ) ) )
& ( ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZU )
!= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZV ) )
| ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZW )
!= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZX ) )
| ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZQ )
!= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZT ) )
| ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZM )
!= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZP ) ) )
& ( ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZO )
!= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZP ) )
| ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZP )
!= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZQ ) )
| ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZQ )
!= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZR ) )
| ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZU )
= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZX ) )
| ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZS )
= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZV ) ) )
& ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZM )
= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZN ) )
& ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZO )
= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZP ) )
& ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZQ )
= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZR ) )
& ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZS )
= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZT ) )
& ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZU )
= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZV ) )
& ( ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZW )
= ( sk1 @ ZZZZX @ ZZZZW @ ZZZZV @ ZZZZU @ ZZZZT @ ZZZZS @ ZZZZR @ ZZZZQ @ ZZZZP @ ZZZZO @ ZZZZN @ ZZZZM @ ZZZZX ) ) ),
inference(cnf,[status(esa)],[4]) ).
thf(65,plain,
! [B: $i,A: $i] : ( A != B ),
inference(cnfConj,[status(thm)],[5]) ).
thf(78,plain,
! [B: $i,A: $i] : ( A != B ),
inference(lifteq,[status(thm)],[65]) ).
thf(79,plain,
$false,
inference(simp,[status(thm)],[78]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO250^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.10/0.23 % Computer : n002.cluster.edu
% 0.10/0.23 % Model : x86_64 x86_64
% 0.10/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.23 % Memory : 8046.5625MB
% 0.10/0.23 % OS : Linux 6.8.0-71-generic
% 0.10/0.23 % CPULimit : 300
% 0.10/0.23 % WCLimit : 300
% 0.10/0.23 % DateTime : Tue Sep 29 16:44:07 UTC 2026
% 0.10/0.24 % CPUTime :
% 0.10/0.24 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.81 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.20/1.02 % [INFO] Parsing done (208ms).
% 1.50/1.03 % [INFO] Running in sequential loop mode.
% 2.07/1.44 % [INFO] eprover registered as external prover.
% 2.07/1.45 % [INFO] Scanning for conjecture ...
% 2.49/1.61 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 2.49/1.68 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 2.49/1.68 % [INFO] Problem is higher-order (TPTP THF).
% 2.49/1.69 % [INFO] Type checking passed.
% 2.49/1.70 % [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 ...
% 4.70/2.60 % [INFO] Killing All external provers ...
% 4.70/2.61 % Time passed: 2223ms (effective reasoning time: 1561ms)
% 4.70/2.61 % 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)>
% 4.70/2.61 % Axioms used in derivation (0):
% 4.70/2.61 % No. of inferences in proof: 8
% 4.70/2.61 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 2223 ms resp. 1561 ms w/o parsing
% 5.04/2.75 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 5.04/2.75 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------