%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SEV037^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 : n015.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:44 AM UTC 2026
% Result : Theorem 32.90s 7.64s
% Output : Refutation 30.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 13
% Syntax : Number of formulae : 108 ( 22 unt; 0 typ; 12 def)
% Number of atoms : 541 ( 86 equ; 0 cnn)
% Maximal formula atoms : 36 ( 5 avg)
% Number of connectives : 2208 ( 206 ~; 203 |; 75 &;1557 @)
% ( 0 <=>; 167 =>; 0 <=; 0 <~>)
% Maximal formula depth : 36 ( 7 avg)
% Number of types : 3 ( 2 usr)
% Number of type conns : 187 ( 187 >; 0 *; 0 +; 0 <<)
% Number of symbols : 16 ( 13 usr; 7 con; 0-3 aty)
% Number of variables : 596 ( 100 ^; 484 !; 0 ?; 596 :)
% ( 0 !>; 0 ?*; 0 @-; 12 @+)
% Comments :
%------------------------------------------------------------------------------
thf(a_type,type,
a: $tType ).
thf(b_type,type,
b: $tType ).
thf(sk1_decl,type,
sk1: a > a > $o ).
thf(sk2_decl,type,
sk2: a > a > $o ).
thf(sk3_decl,type,
sk3: a > b > b > $o ).
thf(sk4_decl,type,
sk4: $o ).
thf(sk5_decl,type,
sk5: a > b ).
thf(sk6_decl,type,
sk6: a > b ).
thf(sk7_decl,type,
sk7: a ).
thf(sk8_decl,type,
sk8: a ).
thf(sk9_decl,type,
sk9: a > b ).
thf(sk10_decl,type,
sk10: a > b ).
thf(sk11_decl,type,
sk11: a > b ).
thf(sk12_decl,type,
sk12: a ).
thf(sk13_decl,type,
sk13: a ).
thf(sk1_def,definition,
( sk1
= ( @+[A: a > a > $o] :
~ ! [B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( A @ C @ D )
=> ( A @ D @ C ) )
& ! [C: a,D: a,E: a] :
( ( ( A @ C @ D )
& ( A @ D @ E ) )
=> ( A @ C @ E ) )
& ( A = B ) )
=> ! [C: a > b > b > $o] :
( ! [D: a,E: a] :
( ( A @ D @ E )
=> ( ! [F: b,G: b] :
( ( C @ D @ F @ G )
=> ( C @ D @ G @ F ) )
& ! [F: b,G: b,H: b] :
( ( ( C @ D @ F @ G )
& ( C @ D @ G @ H ) )
=> ( C @ D @ F @ H ) )
& ( ( C @ D )
= ( C @ E ) ) ) )
=> ( ! [D: a > b,E: a > b] :
( ! [F: a,G: a] :
( ( A @ F @ G )
=> ( C @ F @ ( D @ F ) @ ( E @ G ) ) )
=> ! [F: a,G: a] :
( ( A @ F @ G )
=> ( C @ F @ ( E @ F ) @ ( D @ G ) ) ) )
& ! [D: a > b,E: a > b,F: a > b] :
( ( ! [G: a,H: a] :
( ( A @ G @ H )
=> ( C @ G @ ( D @ G ) @ ( E @ H ) ) )
& ! [G: a,H: a] :
( ( A @ G @ H )
=> ( C @ G @ ( E @ G ) @ ( F @ H ) ) ) )
=> ! [G: a,H: a] :
( ( A @ G @ H )
=> ( C @ G @ ( D @ G ) @ ( F @ H ) ) ) )
& ( ( ^ [D: a > b,E: a > b] :
! [F: a,G: a] :
( ( A @ F @ G )
=> ( C @ F @ ( D @ F ) @ ( E @ G ) ) ) )
= ( ^ [D: a > b,E: a > b] :
! [F: a,G: a] :
( ( B @ F @ G )
=> ( C @ F @ ( D @ F ) @ ( E @ G ) ) ) ) ) ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: a > a > $o] :
~ ( ( ! [B: a,C: a] :
( ( sk1 @ B @ C )
=> ( sk1 @ C @ B ) )
& ! [B: a,C: a,D: a] :
( ( ( sk1 @ B @ C )
& ( sk1 @ C @ D ) )
=> ( sk1 @ B @ D ) )
& ( sk1 = A ) )
=> ! [B: a > b > b > $o] :
( ! [C: a,D: a] :
( ( sk1 @ C @ D )
=> ( ! [E: b,F: b] :
( ( B @ C @ E @ F )
=> ( B @ C @ F @ E ) )
& ! [E: b,F: b,G: b] :
( ( ( B @ C @ E @ F )
& ( B @ C @ F @ G ) )
=> ( B @ C @ E @ G ) )
& ( ( B @ C )
= ( B @ D ) ) ) )
=> ( ! [C: a > b,D: a > b] :
( ! [E: a,F: a] :
( ( sk1 @ E @ F )
=> ( B @ E @ ( C @ E ) @ ( D @ F ) ) )
=> ! [E: a,F: a] :
( ( sk1 @ E @ F )
=> ( B @ E @ ( D @ E ) @ ( C @ F ) ) ) )
& ! [C: a > b,D: a > b,E: a > b] :
( ( ! [F: a,G: a] :
( ( sk1 @ F @ G )
=> ( B @ F @ ( C @ F ) @ ( D @ G ) ) )
& ! [F: a,G: a] :
( ( sk1 @ F @ G )
=> ( B @ F @ ( D @ F ) @ ( E @ G ) ) ) )
=> ! [F: a,G: a] :
( ( sk1 @ F @ G )
=> ( B @ F @ ( C @ F ) @ ( E @ G ) ) ) )
& ( ( ^ [C: a > b,D: a > b] :
! [E: a,F: a] :
( ( sk1 @ E @ F )
=> ( B @ E @ ( C @ E ) @ ( D @ F ) ) ) )
= ( ^ [C: a > b,D: a > b] :
! [E: a,F: a] :
( ( A @ E @ F )
=> ( B @ E @ ( C @ E ) @ ( D @ F ) ) ) ) ) ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: a > b > b > $o] :
~ ( ! [B: a,C: a] :
( ( sk1 @ B @ C )
=> ( ! [D: b,E: b] :
( ( A @ B @ D @ E )
=> ( A @ B @ E @ D ) )
& ! [D: b,E: b,F: b] :
( ( ( A @ B @ D @ E )
& ( A @ B @ E @ F ) )
=> ( A @ B @ D @ F ) )
& ( ( A @ B )
= ( A @ C ) ) ) )
=> ( ! [B: a > b,C: a > b] :
( ! [D: a,E: a] :
( ( sk1 @ D @ E )
=> ( A @ D @ ( B @ D ) @ ( C @ E ) ) )
=> ! [D: a,E: a] :
( ( sk1 @ D @ E )
=> ( A @ D @ ( C @ D ) @ ( B @ E ) ) ) )
& ! [B: a > b,C: a > b,D: a > b] :
( ( ! [E: a,F: a] :
( ( sk1 @ E @ F )
=> ( A @ E @ ( B @ E ) @ ( C @ F ) ) )
& ! [E: a,F: a] :
( ( sk1 @ E @ F )
=> ( A @ E @ ( C @ E ) @ ( D @ F ) ) ) )
=> ! [E: a,F: a] :
( ( sk1 @ E @ F )
=> ( A @ E @ ( B @ E ) @ ( D @ F ) ) ) )
& ( ( ^ [B: a > b,C: a > b] :
! [D: a,E: a] :
( ( sk1 @ D @ E )
=> ( A @ D @ ( B @ D ) @ ( C @ E ) ) ) )
= ( ^ [B: a > b,C: a > b] :
! [D: a,E: a] :
( ( sk2 @ D @ E )
=> ( A @ D @ ( B @ D ) @ ( C @ E ) ) ) ) ) ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( @+[A: a > b] :
~ ! [B: a > b] :
( ! [C: a,D: a] :
( ( sk1 @ C @ D )
=> ( sk3 @ C @ ( A @ C ) @ ( B @ D ) ) )
=> ! [C: a,D: a] :
( ( sk1 @ C @ D )
=> ( sk3 @ C @ ( B @ C ) @ ( A @ D ) ) ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( @+[A: a > b] :
~ ( ! [B: a,C: a] :
( ( sk1 @ B @ C )
=> ( sk3 @ B @ ( sk5 @ B ) @ ( A @ C ) ) )
=> ! [B: a,C: a] :
( ( sk1 @ B @ C )
=> ( sk3 @ B @ ( A @ B ) @ ( sk5 @ C ) ) ) ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( @+[A: a] :
~ ! [B: a] :
( ( sk1 @ A @ B )
=> ( sk3 @ A @ ( sk6 @ A ) @ ( sk5 @ B ) ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( @+[A: a] :
~ ( ( sk1 @ sk7 @ A )
=> ( sk3 @ sk7 @ ( sk6 @ sk7 ) @ ( sk5 @ A ) ) ) ) ) ).
thf(sk9_def,definition,
( sk9
= ( @+[A: a > b] :
~ ! [B: a > b,C: a > b] :
( ( ! [D: a,E: a] :
( ( sk1 @ D @ E )
=> ( sk3 @ D @ ( A @ D ) @ ( B @ E ) ) )
& ! [D: a,E: a] :
( ( sk1 @ D @ E )
=> ( sk3 @ D @ ( B @ D ) @ ( C @ E ) ) ) )
=> ! [D: a,E: a] :
( ( sk1 @ D @ E )
=> ( sk3 @ D @ ( A @ D ) @ ( C @ E ) ) ) ) ) ) ).
thf(sk10_def,definition,
( sk10
= ( @+[A: a > b] :
~ ! [B: a > b] :
( ( ! [C: a,D: a] :
( ( sk1 @ C @ D )
=> ( sk3 @ C @ ( sk9 @ C ) @ ( A @ D ) ) )
& ! [C: a,D: a] :
( ( sk1 @ C @ D )
=> ( sk3 @ C @ ( A @ C ) @ ( B @ D ) ) ) )
=> ! [C: a,D: a] :
( ( sk1 @ C @ D )
=> ( sk3 @ C @ ( sk9 @ C ) @ ( B @ D ) ) ) ) ) ) ).
thf(sk11_def,definition,
( sk11
= ( @+[A: a > b] :
~ ( ( ! [B: a,C: a] :
( ( sk1 @ B @ C )
=> ( sk3 @ B @ ( sk9 @ B ) @ ( sk10 @ C ) ) )
& ! [B: a,C: a] :
( ( sk1 @ B @ C )
=> ( sk3 @ B @ ( sk10 @ B ) @ ( A @ C ) ) ) )
=> ! [B: a,C: a] :
( ( sk1 @ B @ C )
=> ( sk3 @ B @ ( sk9 @ B ) @ ( A @ C ) ) ) ) ) ) ).
thf(sk12_def,definition,
( sk12
= ( @+[A: a] :
~ ! [B: a] :
( ( sk1 @ A @ B )
=> ( sk3 @ A @ ( sk9 @ A ) @ ( sk11 @ B ) ) ) ) ) ).
thf(sk13_def,definition,
( sk13
= ( @+[A: a] :
~ ( ( sk1 @ sk12 @ A )
=> ( sk3 @ sk12 @ ( sk9 @ sk12 ) @ ( sk11 @ A ) ) ) ) ) ).
thf(1,conjecture,
! [A: a > a > $o,B: a > a > $o,C: a > b > b > $o] :
( ( ! [D: a,E: a] :
( ( A @ D @ E )
=> ( A @ E @ D ) )
& ! [D: a,E: a,F: a] :
( ( ( A @ D @ E )
& ( A @ E @ F ) )
=> ( A @ D @ F ) )
& ( A = B ) )
=> ( ! [D: a,E: a] :
( ( A @ D @ E )
=> ( ! [F: b,G: b] :
( ( C @ D @ F @ G )
=> ( C @ D @ G @ F ) )
& ! [F: b,G: b,H: b] :
( ( ( C @ D @ F @ G )
& ( C @ D @ G @ H ) )
=> ( C @ D @ F @ H ) )
& ( ( C @ D )
= ( C @ E ) ) ) )
=> ( ! [D: a > b,E: a > b] :
( ! [F: a,G: a] :
( ( A @ F @ G )
=> ( C @ F @ ( D @ F ) @ ( E @ G ) ) )
=> ! [F: a,G: a] :
( ( A @ F @ G )
=> ( C @ F @ ( E @ F ) @ ( D @ G ) ) ) )
& ! [D: a > b,E: a > b,F: a > b] :
( ( ! [G: a,H: a] :
( ( A @ G @ H )
=> ( C @ G @ ( D @ G ) @ ( E @ H ) ) )
& ! [G: a,H: a] :
( ( A @ G @ H )
=> ( C @ G @ ( E @ G ) @ ( F @ H ) ) ) )
=> ! [G: a,H: a] :
( ( A @ G @ H )
=> ( C @ G @ ( D @ G ) @ ( F @ H ) ) ) )
& ( ( ^ [D: a > b,E: a > b] :
! [F: a,G: a] :
( ( A @ F @ G )
=> ( C @ F @ ( D @ F ) @ ( E @ G ) ) ) )
= ( ^ [D: a > b,E: a > b] :
! [F: a,G: a] :
( ( B @ F @ G )
=> ( C @ F @ ( D @ F ) @ ( E @ G ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cTHM516_pme) ).
thf(2,negated_conjecture,
~ ! [A: a > a > $o,B: a > a > $o,C: a > b > b > $o] :
( ( ! [D: a,E: a] :
( ( A @ D @ E )
=> ( A @ E @ D ) )
& ! [D: a,E: a,F: a] :
( ( ( A @ D @ E )
& ( A @ E @ F ) )
=> ( A @ D @ F ) )
& ( A = B ) )
=> ( ! [D: a,E: a] :
( ( A @ D @ E )
=> ( ! [F: b,G: b] :
( ( C @ D @ F @ G )
=> ( C @ D @ G @ F ) )
& ! [F: b,G: b,H: b] :
( ( ( C @ D @ F @ G )
& ( C @ D @ G @ H ) )
=> ( C @ D @ F @ H ) )
& ( ( C @ D )
= ( C @ E ) ) ) )
=> ( ! [D: a > b,E: a > b] :
( ! [F: a,G: a] :
( ( A @ F @ G )
=> ( C @ F @ ( D @ F ) @ ( E @ G ) ) )
=> ! [F: a,G: a] :
( ( A @ F @ G )
=> ( C @ F @ ( E @ F ) @ ( D @ G ) ) ) )
& ! [D: a > b,E: a > b,F: a > b] :
( ( ! [G: a,H: a] :
( ( A @ G @ H )
=> ( C @ G @ ( D @ G ) @ ( E @ H ) ) )
& ! [G: a,H: a] :
( ( A @ G @ H )
=> ( C @ G @ ( E @ G ) @ ( F @ H ) ) ) )
=> ! [G: a,H: a] :
( ( A @ G @ H )
=> ( C @ G @ ( D @ G ) @ ( F @ H ) ) ) )
& ( ( ^ [D: a > b,E: a > b] :
! [F: a,G: a] :
( ( A @ F @ G )
=> ( C @ F @ ( D @ F ) @ ( E @ G ) ) ) )
= ( ^ [D: a > b,E: a > b] :
! [F: a,G: a] :
( ( B @ F @ G )
=> ( C @ F @ ( D @ F ) @ ( E @ G ) ) ) ) ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(3,plain,
~ ! [A: a > a > $o,B: a > a > $o,C: a > b > b > $o] :
( ( ! [D: a,E: a] :
( ( A @ D @ E )
=> ( A @ E @ D ) )
& ! [D: a,E: a,F: a] :
( ( ( A @ D @ E )
& ( A @ E @ F ) )
=> ( A @ D @ F ) )
& ( A = B ) )
=> ( ! [D: a,E: a] :
( ( A @ D @ E )
=> ( ! [F: b,G: b] :
( ( C @ D @ F @ G )
=> ( C @ D @ G @ F ) )
& ! [F: b,G: b,H: b] :
( ( ( C @ D @ F @ G )
& ( C @ D @ G @ H ) )
=> ( C @ D @ F @ H ) )
& ( ( C @ D )
= ( C @ E ) ) ) )
=> ( ! [D: a > b,E: a > b] :
( ! [F: a,G: a] :
( ( A @ F @ G )
=> ( C @ F @ ( D @ F ) @ ( E @ G ) ) )
=> ! [F: a,G: a] :
( ( A @ F @ G )
=> ( C @ F @ ( E @ F ) @ ( D @ G ) ) ) )
& ! [D: a > b,E: a > b,F: a > b] :
( ( ! [G: a,H: a] :
( ( A @ G @ H )
=> ( C @ G @ ( D @ G ) @ ( E @ H ) ) )
& ! [G: a,H: a] :
( ( A @ G @ H )
=> ( C @ G @ ( E @ G ) @ ( F @ H ) ) ) )
=> ! [G: a,H: a] :
( ( A @ G @ H )
=> ( C @ G @ ( D @ G ) @ ( F @ H ) ) ) )
& ( ( ^ [D: a > b,E: a > b] :
! [F: a,G: a] :
( ( A @ F @ G )
=> ( C @ F @ ( D @ F ) @ ( E @ G ) ) ) )
= ( ^ [D: a > b,E: a > b] :
! [F: a,G: a] :
( ( B @ F @ G )
=> ( C @ F @ ( D @ F ) @ ( E @ G ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(4,plain,
~ ! [A: a > a > $o,B: a > a > $o] :
( ( ! [C: a,D: a] :
( ( A @ C @ D )
=> ( A @ D @ C ) )
& ! [C: a,D: a,E: a] :
( ( ( A @ C @ D )
& ( A @ D @ E ) )
=> ( A @ C @ E ) )
& ( A = B ) )
=> ! [C: a > b > b > $o] :
( ! [D: a,E: a] :
( ( A @ D @ E )
=> ( ! [F: b,G: b] :
( ( C @ D @ F @ G )
=> ( C @ D @ G @ F ) )
& ! [F: b,G: b,H: b] :
( ( ( C @ D @ F @ G )
& ( C @ D @ G @ H ) )
=> ( C @ D @ F @ H ) )
& ( ( C @ D )
= ( C @ E ) ) ) )
=> ( ! [D: a > b,E: a > b] :
( ! [F: a,G: a] :
( ( A @ F @ G )
=> ( C @ F @ ( D @ F ) @ ( E @ G ) ) )
=> ! [F: a,G: a] :
( ( A @ F @ G )
=> ( C @ F @ ( E @ F ) @ ( D @ G ) ) ) )
& ! [D: a > b,E: a > b,F: a > b] :
( ( ! [G: a,H: a] :
( ( A @ G @ H )
=> ( C @ G @ ( D @ G ) @ ( E @ H ) ) )
& ! [G: a,H: a] :
( ( A @ G @ H )
=> ( C @ G @ ( E @ G ) @ ( F @ H ) ) ) )
=> ! [G: a,H: a] :
( ( A @ G @ H )
=> ( C @ G @ ( D @ G ) @ ( F @ H ) ) ) )
& ( ( ^ [D: a > b,E: a > b] :
! [F: a,G: a] :
( ( A @ F @ G )
=> ( C @ F @ ( D @ F ) @ ( E @ G ) ) ) )
= ( ^ [D: a > b,E: a > b] :
! [F: a,G: a] :
( ( B @ F @ G )
=> ( C @ F @ ( D @ F ) @ ( E @ G ) ) ) ) ) ) ) ),
inference(miniscope,[status(thm)],[3]) ).
thf(5,plain,
! [R: a,Q: a,P: a,O: a,N: a,M: a,L: b,K: b,J: b,I: b,H: b,G: a,F: a,E: a,D: a,C: a,B: a,A: a] :
( ( ~ ( sk1 @ A @ B )
| ( sk1 @ B @ A ) )
& ( ~ ( sk1 @ C @ D )
| ~ ( sk1 @ D @ E )
| ( sk1 @ C @ E ) )
& ( sk1 = sk2 )
& ( ~ ( sk1 @ F @ G )
| ~ ( sk3 @ F @ H @ I )
| ( sk3 @ F @ I @ H ) )
& ( ~ ( sk1 @ F @ G )
| ~ ( sk3 @ F @ J @ K )
| ~ ( sk3 @ F @ K @ L )
| ( sk3 @ F @ J @ L ) )
& ( ~ ( sk1 @ F @ G )
| ( ( sk3 @ F )
= ( sk3 @ G ) ) )
& ( ~ ( sk1 @ M @ N )
| ( sk3 @ M @ ( sk5 @ M ) @ ( sk6 @ N ) )
| ~ sk4 )
& ( ( sk1 @ sk7 @ sk8 )
| ~ sk4 )
& ( ~ ( sk3 @ sk7 @ ( sk6 @ sk7 ) @ ( sk5 @ sk8 ) )
| ~ sk4 )
& ( sk4
| ~ ( sk1 @ O @ P )
| ( sk3 @ O @ ( sk9 @ O ) @ ( sk10 @ P ) )
| ( ( ^ [S: a > b,T: a > b] :
! [U: a,V: a] :
( ( sk1 @ U @ V )
=> ( sk3 @ U @ ( S @ U ) @ ( T @ V ) ) ) )
!= ( ^ [S: a > b,T: a > b] :
! [U: a,V: a] :
( ( sk2 @ U @ V )
=> ( sk3 @ U @ ( S @ U ) @ ( T @ V ) ) ) ) ) )
& ( sk4
| ~ ( sk1 @ Q @ R )
| ( sk3 @ Q @ ( sk10 @ Q ) @ ( sk11 @ R ) )
| ( ( ^ [S: a > b,T: a > b] :
! [U: a,V: a] :
( ( sk1 @ U @ V )
=> ( sk3 @ U @ ( S @ U ) @ ( T @ V ) ) ) )
!= ( ^ [S: a > b,T: a > b] :
! [U: a,V: a] :
( ( sk2 @ U @ V )
=> ( sk3 @ U @ ( S @ U ) @ ( T @ V ) ) ) ) ) )
& ( sk4
| ( sk1 @ sk12 @ sk13 )
| ( ( ^ [S: a > b,T: a > b] :
! [U: a,V: a] :
( ( sk1 @ U @ V )
=> ( sk3 @ U @ ( S @ U ) @ ( T @ V ) ) ) )
!= ( ^ [S: a > b,T: a > b] :
! [U: a,V: a] :
( ( sk2 @ U @ V )
=> ( sk3 @ U @ ( S @ U ) @ ( T @ V ) ) ) ) ) )
& ( sk4
| ~ ( sk3 @ sk12 @ ( sk9 @ sk12 ) @ ( sk11 @ sk13 ) )
| ( ( ^ [S: a > b,T: a > b] :
! [U: a,V: a] :
( ( sk1 @ U @ V )
=> ( sk3 @ U @ ( S @ U ) @ ( T @ V ) ) ) )
!= ( ^ [S: a > b,T: a > b] :
! [U: a,V: a] :
( ( sk2 @ U @ V )
=> ( sk3 @ U @ ( S @ U ) @ ( T @ V ) ) ) ) ) ) ),
inference(cnf,[status(esa)],[4]) ).
thf(7,plain,
( sk4
| ( sk1 @ sk12 @ sk13 )
| ( ( ^ [A: a > b,B: a > b] :
! [C: a,D: a] :
( ( sk1 @ C @ D )
=> ( sk3 @ C @ ( A @ C ) @ ( B @ D ) ) ) )
!= ( ^ [A: a > b,B: a > b] :
! [C: a,D: a] :
( ( sk2 @ C @ D )
=> ( sk3 @ C @ ( A @ C ) @ ( B @ D ) ) ) ) ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(27,plain,
( ( ( ^ [A: a > b,B: a > b] :
! [C: a,D: a] :
( ( sk2 @ C @ D )
=> ( sk3 @ C @ ( A @ C ) @ ( B @ D ) ) ) )
!= ( ^ [A: a > b,B: a > b] :
! [C: a,D: a] :
( ( sk1 @ C @ D )
=> ( sk3 @ C @ ( A @ C ) @ ( B @ D ) ) ) ) )
| sk4
| ( sk1 @ sk12 @ sk13 ) ),
inference(lifteq,[status(thm)],[7]) ).
thf(11,plain,
sk1 = sk2,
inference(cnfConj,[status(thm)],[5]) ).
thf(28,plain,
sk2 = sk1,
inference(lifteq,[status(thm)],[11]) ).
thf(33,plain,
! [B: a,A: a] :
( ( sk2 @ A @ B )
= ( sk1 @ A @ B ) ),
inference(func_ext,[status(esa)],[28]) ).
thf(59,plain,
( ( ( ^ [A: a > b,B: a > b] :
! [C: a,D: a] :
( ( sk1 @ C @ D )
=> ( sk3 @ C @ ( A @ C ) @ ( B @ D ) ) ) )
!= ( ^ [A: a > b,B: a > b] :
! [C: a,D: a] :
( ( sk1 @ C @ D )
=> ( sk3 @ C @ ( A @ C ) @ ( B @ D ) ) ) ) )
| sk4
| ( sk1 @ sk12 @ sk13 ) ),
inference(rewrite,[status(thm)],[27,33]) ).
thf(60,plain,
( sk4
| ( sk1 @ sk12 @ sk13 ) ),
inference(simp,[status(thm)],[59]) ).
thf(18,plain,
! [B: a,A: a] :
( ~ ( sk1 @ A @ B )
| ( sk1 @ B @ A ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(74,plain,
! [B: a,A: a] :
( sk4
| ~ $true
| ( sk1 @ B @ A )
| ( ( sk1 @ sk12 @ sk13 )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[60,18]) ).
thf(75,plain,
! [B: a,A: a] :
( sk4
| ( sk1 @ B @ A )
| ( ( sk1 @ sk12 @ sk13 )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[74]) ).
thf(76,plain,
( sk4
| ( sk1 @ sk13 @ sk12 ) ),
inference(pattern_uni,[status(thm)],[75:[bind(A,$thf( sk12 )),bind(B,$thf( sk13 ))]]) ).
thf(9,plain,
! [C: a,B: a,A: a] :
( ~ ( sk1 @ A @ B )
| ~ ( sk1 @ B @ C )
| ( sk1 @ A @ C ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(21,plain,
! [C: a,B: a,A: a] :
( ~ ( sk1 @ A @ B )
| ~ ( sk1 @ B @ C )
| ( sk1 @ A @ C ) ),
inference(simp,[status(thm)],[9]) ).
thf(214,plain,
! [C: a,B: a,A: a] :
( sk4
| ~ ( sk1 @ A @ B )
| ~ $true
| ( sk1 @ A @ C )
| ( ( sk1 @ sk13 @ sk12 )
!= ( sk1 @ B @ C ) ) ),
inference(paramod_ordered,[status(thm)],[76,21]) ).
thf(215,plain,
! [C: a,B: a,A: a] :
( sk4
| ~ ( sk1 @ A @ B )
| ( sk1 @ A @ C )
| ( ( sk1 @ sk13 @ sk12 )
!= ( sk1 @ B @ C ) ) ),
inference(simp,[status(thm)],[214]) ).
thf(216,plain,
! [A: a] :
( sk4
| ~ ( sk1 @ A @ sk13 )
| ( sk1 @ A @ sk12 ) ),
inference(pattern_uni,[status(thm)],[215:[bind(A,$thf( A )),bind(B,$thf( sk13 )),bind(C,$thf( sk12 ))]]) ).
thf(297,plain,
! [A: a] :
( sk4
| sk4
| ~ $true
| ( sk1 @ A @ sk12 )
| ( ( sk1 @ sk12 @ sk13 )
!= ( sk1 @ A @ sk13 ) ) ),
inference(paramod_ordered,[status(thm)],[60,216]) ).
thf(298,plain,
! [A: a] :
( sk4
| ( sk1 @ A @ sk12 )
| ( ( sk1 @ sk12 @ sk13 )
!= ( sk1 @ A @ sk13 ) ) ),
inference(simp,[status(thm)],[297]) ).
thf(299,plain,
( sk4
| ( sk1 @ sk12 @ sk12 ) ),
inference(pattern_uni,[status(thm)],[298:[bind(A,$thf( sk12 ))]]) ).
thf(6,plain,
( ( sk1 @ sk7 @ sk8 )
| ~ sk4 ),
inference(cnfConj,[status(thm)],[5]) ).
thf(71,plain,
! [B: a,A: a] :
( ~ sk4
| ~ $true
| ( sk1 @ B @ A )
| ( ( sk1 @ sk7 @ sk8 )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[6,18]) ).
thf(72,plain,
! [B: a,A: a] :
( ~ sk4
| ( sk1 @ B @ A )
| ( ( sk1 @ sk7 @ sk8 )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[71]) ).
thf(73,plain,
( ~ sk4
| ( sk1 @ sk8 @ sk7 ) ),
inference(pattern_uni,[status(thm)],[72:[bind(A,$thf( sk7 )),bind(B,$thf( sk8 ))]]) ).
thf(15,plain,
! [B: a,A: a] :
( ~ ( sk1 @ A @ B )
| ( sk3 @ A @ ( sk5 @ A ) @ ( sk6 @ B ) )
| ~ sk4 ),
inference(cnfConj,[status(thm)],[5]) ).
thf(31,plain,
! [B: a,A: a] :
( ~ ( sk1 @ A @ B )
| ( sk3 @ A @ ( sk5 @ A ) @ ( sk6 @ B ) )
| ~ sk4 ),
inference(simp,[status(thm)],[15]) ).
thf(13,plain,
! [B: a,A: a] :
( ~ ( sk1 @ A @ B )
| ( ( sk3 @ A )
= ( sk3 @ B ) ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(22,plain,
! [B: a,A: a] :
( ( ( sk3 @ A )
= ( sk3 @ B ) )
| ~ ( sk1 @ A @ B ) ),
inference(lifteq,[status(thm)],[13]) ).
thf(23,plain,
! [B: a,A: a] :
( ( ( sk3 @ A )
= ( sk3 @ B ) )
| ~ ( sk1 @ A @ B ) ),
inference(simp,[status(thm)],[22]) ).
thf(134,plain,
! [D: b,C: b,B: a,A: a] :
( ( ( sk3 @ A @ C @ D )
= ( sk3 @ B @ C @ D ) )
| ~ ( sk1 @ A @ B ) ),
inference(func_ext,[status(esa)],[23]) ).
thf(10,plain,
! [D: b,C: b,B: a,A: a] :
( ~ ( sk1 @ A @ B )
| ~ ( sk3 @ A @ C @ D )
| ( sk3 @ A @ D @ C ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(19,plain,
! [D: b,C: b,B: a,A: a] :
( ~ ( sk1 @ A @ B )
| ~ ( sk3 @ A @ C @ D )
| ( sk3 @ A @ D @ C ) ),
inference(simp,[status(thm)],[10]) ).
thf(16,plain,
( ~ ( sk3 @ sk7 @ ( sk6 @ sk7 ) @ ( sk5 @ sk8 ) )
| ~ sk4 ),
inference(cnfConj,[status(thm)],[5]) ).
thf(100,plain,
! [D: b,C: b,B: a,A: a] :
( ~ ( sk1 @ A @ B )
| ~ ( sk3 @ A @ C @ D )
| ~ $true
| ~ sk4
| ( ( sk3 @ A @ D @ C )
!= ( sk3 @ sk7 @ ( sk6 @ sk7 ) @ ( sk5 @ sk8 ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,16]) ).
thf(101,plain,
! [D: b,C: b,B: a,A: a] :
( ~ ( sk1 @ A @ B )
| ~ ( sk3 @ A @ C @ D )
| ~ sk4
| ( ( sk3 @ A @ D @ C )
!= ( sk3 @ sk7 @ ( sk6 @ sk7 ) @ ( sk5 @ sk8 ) ) ) ),
inference(simp,[status(thm)],[100]) ).
thf(102,plain,
! [A: a] :
( ~ ( sk1 @ sk7 @ A )
| ~ ( sk3 @ sk7 @ ( sk5 @ sk8 ) @ ( sk6 @ sk7 ) )
| ~ sk4 ),
inference(pattern_uni,[status(thm)],[101:[bind(A,$thf( sk7 )),bind(B,$thf( B )),bind(C,$thf( sk5 @ sk8 )),bind(D,$thf( sk6 @ sk7 ))]]) ).
thf(114,plain,
! [A: a] :
( ~ ( sk1 @ sk7 @ A )
| ~ ( sk3 @ sk7 @ ( sk5 @ sk8 ) @ ( sk6 @ sk7 ) )
| ~ sk4 ),
inference(simp,[status(thm)],[102]) ).
thf(162,plain,
! [A: a] :
( ~ sk4
| ~ $true
| ~ ( sk3 @ sk7 @ ( sk5 @ sk8 ) @ ( sk6 @ sk7 ) )
| ~ sk4
| ( ( sk1 @ sk7 @ sk8 )
!= ( sk1 @ sk7 @ A ) ) ),
inference(paramod_ordered,[status(thm)],[6,114]) ).
thf(163,plain,
! [A: a] :
( ~ sk4
| ~ ( sk3 @ sk7 @ ( sk5 @ sk8 ) @ ( sk6 @ sk7 ) )
| ( ( sk1 @ sk7 @ sk8 )
!= ( sk1 @ sk7 @ A ) ) ),
inference(simp,[status(thm)],[162]) ).
thf(164,plain,
( ~ sk4
| ~ ( sk3 @ sk7 @ ( sk5 @ sk8 ) @ ( sk6 @ sk7 ) ) ),
inference(pattern_uni,[status(thm)],[163:[bind(A,$thf( sk8 ))]]) ).
thf(474,plain,
! [D: b,C: b,B: a,A: a] :
( ~ ( sk1 @ A @ B )
| ~ sk4
| ~ ( sk3 @ A @ C @ D )
| ( ( sk3 @ B @ C @ D )
!= ( sk3 @ sk7 @ ( sk5 @ sk8 ) @ ( sk6 @ sk7 ) ) ) ),
inference(paramod_ordered,[status(thm)],[134,164]) ).
thf(475,plain,
! [A: a] :
( ~ ( sk1 @ A @ sk7 )
| ~ sk4
| ~ ( sk3 @ A @ ( sk5 @ sk8 ) @ ( sk6 @ sk7 ) ) ),
inference(pattern_uni,[status(thm)],[474:[bind(A,$thf( A )),bind(B,$thf( sk7 )),bind(C,$thf( sk5 @ sk8 )),bind(D,$thf( sk6 @ sk7 ))]]) ).
thf(844,plain,
! [A: a] :
( ~ sk4
| ~ $true
| ~ sk4
| ~ ( sk3 @ A @ ( sk5 @ sk8 ) @ ( sk6 @ sk7 ) )
| ( ( sk1 @ sk8 @ sk7 )
!= ( sk1 @ A @ sk7 ) ) ),
inference(paramod_ordered,[status(thm)],[73,475]) ).
thf(845,plain,
! [A: a] :
( ~ sk4
| ~ ( sk3 @ A @ ( sk5 @ sk8 ) @ ( sk6 @ sk7 ) )
| ( ( sk1 @ sk8 @ sk7 )
!= ( sk1 @ A @ sk7 ) ) ),
inference(simp,[status(thm)],[844]) ).
thf(846,plain,
( ~ sk4
| ~ ( sk3 @ sk8 @ ( sk5 @ sk8 ) @ ( sk6 @ sk7 ) ) ),
inference(pattern_uni,[status(thm)],[845:[bind(A,$thf( sk8 ))]]) ).
thf(1226,plain,
! [B: a,A: a] :
( ~ ( sk1 @ A @ B )
| ~ sk4
| ~ sk4
| ~ $true
| ( ( sk3 @ A @ ( sk5 @ A ) @ ( sk6 @ B ) )
!= ( sk3 @ sk8 @ ( sk5 @ sk8 ) @ ( sk6 @ sk7 ) ) ) ),
inference(paramod_ordered,[status(thm)],[31,846]) ).
thf(1227,plain,
! [B: a,A: a] :
( ~ ( sk1 @ A @ B )
| ~ sk4
| ( ( sk3 @ A @ ( sk5 @ A ) @ ( sk6 @ B ) )
!= ( sk3 @ sk8 @ ( sk5 @ sk8 ) @ ( sk6 @ sk7 ) ) ) ),
inference(simp,[status(thm)],[1226]) ).
thf(1228,plain,
( ~ ( sk1 @ sk8 @ sk7 )
| ~ sk4 ),
inference(pattern_uni,[status(thm)],[1227:[bind(A,$thf( sk8 )),bind(B,$thf( sk7 ))]]) ).
thf(1310,plain,
( ~ sk4
| ~ $true
| ~ sk4
| ( ( sk1 @ sk8 @ sk7 )
!= ( sk1 @ sk8 @ sk7 ) ) ),
inference(paramod_ordered,[status(thm)],[73,1228]) ).
thf(1311,plain,
( ~ sk4
| ( ( sk1 @ sk8 @ sk7 )
!= ( sk1 @ sk8 @ sk7 ) ) ),
inference(simp,[status(thm)],[1310]) ).
thf(1312,plain,
~ sk4,
inference(pattern_uni,[status(thm)],[1311:[]]) ).
thf(1350,plain,
( $false
| ( sk1 @ sk12 @ sk12 ) ),
inference(rewrite,[status(thm)],[299,1312]) ).
thf(1351,plain,
sk1 @ sk12 @ sk12,
inference(simp,[status(thm)],[1350]) ).
thf(12,plain,
! [B: a,A: a] :
( sk4
| ~ ( sk1 @ A @ B )
| ( sk3 @ A @ ( sk9 @ A ) @ ( sk10 @ B ) )
| ( ( ^ [C: a > b,D: a > b] :
! [E: a,F: a] :
( ( sk1 @ E @ F )
=> ( sk3 @ E @ ( C @ E ) @ ( D @ F ) ) ) )
!= ( ^ [C: a > b,D: a > b] :
! [E: a,F: a] :
( ( sk2 @ E @ F )
=> ( sk3 @ E @ ( C @ E ) @ ( D @ F ) ) ) ) ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(25,plain,
! [B: a,A: a] :
( ( ( ^ [C: a > b,D: a > b] :
! [E: a,F: a] :
( ( sk2 @ E @ F )
=> ( sk3 @ E @ ( C @ E ) @ ( D @ F ) ) ) )
!= ( ^ [C: a > b,D: a > b] :
! [E: a,F: a] :
( ( sk1 @ E @ F )
=> ( sk3 @ E @ ( C @ E ) @ ( D @ F ) ) ) ) )
| sk4
| ~ ( sk1 @ A @ B )
| ( sk3 @ A @ ( sk9 @ A ) @ ( sk10 @ B ) ) ),
inference(lifteq,[status(thm)],[12]) ).
thf(26,plain,
! [B: a,A: a] :
( ( ( ^ [C: a > b,D: a > b] :
! [E: a,F: a] :
( ( sk2 @ E @ F )
=> ( sk3 @ E @ ( C @ E ) @ ( D @ F ) ) ) )
!= ( ^ [C: a > b,D: a > b] :
! [E: a,F: a] :
( ( sk1 @ E @ F )
=> ( sk3 @ E @ ( C @ E ) @ ( D @ F ) ) ) ) )
| sk4
| ~ ( sk1 @ A @ B )
| ( sk3 @ A @ ( sk9 @ A ) @ ( sk10 @ B ) ) ),
inference(simp,[status(thm)],[25]) ).
thf(621,plain,
! [B: a,A: a] :
( ( ( ^ [C: a > b,D: a > b] :
! [E: a,F: a] :
( ( sk1 @ E @ F )
=> ( sk3 @ E @ ( C @ E ) @ ( D @ F ) ) ) )
!= ( ^ [C: a > b,D: a > b] :
! [E: a,F: a] :
( ( sk1 @ E @ F )
=> ( sk3 @ E @ ( C @ E ) @ ( D @ F ) ) ) ) )
| sk4
| ~ ( sk1 @ A @ B )
| ( sk3 @ A @ ( sk9 @ A ) @ ( sk10 @ B ) ) ),
inference(rewrite,[status(thm)],[26,33]) ).
thf(622,plain,
! [B: a,A: a] :
( sk4
| ~ ( sk1 @ A @ B )
| ( sk3 @ A @ ( sk9 @ A ) @ ( sk10 @ B ) ) ),
inference(simp,[status(thm)],[621]) ).
thf(629,plain,
! [B: a,A: a] :
( sk4
| sk4
| ~ $true
| ( sk3 @ A @ ( sk9 @ A ) @ ( sk10 @ B ) )
| ( ( sk1 @ sk12 @ sk12 )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[299,622]) ).
thf(630,plain,
! [B: a,A: a] :
( sk4
| ( sk3 @ A @ ( sk9 @ A ) @ ( sk10 @ B ) )
| ( ( sk1 @ sk12 @ sk12 )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[629]) ).
thf(631,plain,
( sk4
| ( sk3 @ sk12 @ ( sk9 @ sk12 ) @ ( sk10 @ sk12 ) ) ),
inference(pattern_uni,[status(thm)],[630:[bind(A,$thf( sk12 )),bind(B,$thf( sk12 ))]]) ).
thf(1346,plain,
( $false
| ( sk3 @ sk12 @ ( sk9 @ sk12 ) @ ( sk10 @ sk12 ) ) ),
inference(rewrite,[status(thm)],[631,1312]) ).
thf(1347,plain,
sk3 @ sk12 @ ( sk9 @ sk12 ) @ ( sk10 @ sk12 ),
inference(simp,[status(thm)],[1346]) ).
thf(14,plain,
! [E: b,D: b,C: b,B: a,A: a] :
( ~ ( sk1 @ A @ B )
| ~ ( sk3 @ A @ C @ D )
| ~ ( sk3 @ A @ D @ E )
| ( sk3 @ A @ C @ E ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(20,plain,
! [E: b,D: b,C: b,B: a,A: a] :
( ~ ( sk1 @ A @ B )
| ~ ( sk3 @ A @ C @ D )
| ~ ( sk3 @ A @ D @ E )
| ( sk3 @ A @ C @ E ) ),
inference(simp,[status(thm)],[14]) ).
thf(17,plain,
( sk4
| ~ ( sk3 @ sk12 @ ( sk9 @ sk12 ) @ ( sk11 @ sk13 ) )
| ( ( ^ [A: a > b,B: a > b] :
! [C: a,D: a] :
( ( sk1 @ C @ D )
=> ( sk3 @ C @ ( A @ C ) @ ( B @ D ) ) ) )
!= ( ^ [A: a > b,B: a > b] :
! [C: a,D: a] :
( ( sk2 @ C @ D )
=> ( sk3 @ C @ ( A @ C ) @ ( B @ D ) ) ) ) ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(24,plain,
( ( ( ^ [A: a > b,B: a > b] :
! [C: a,D: a] :
( ( sk2 @ C @ D )
=> ( sk3 @ C @ ( A @ C ) @ ( B @ D ) ) ) )
!= ( ^ [A: a > b,B: a > b] :
! [C: a,D: a] :
( ( sk1 @ C @ D )
=> ( sk3 @ C @ ( A @ C ) @ ( B @ D ) ) ) ) )
| sk4
| ~ ( sk3 @ sk12 @ ( sk9 @ sk12 ) @ ( sk11 @ sk13 ) ) ),
inference(lifteq,[status(thm)],[17]) ).
thf(330,plain,
( ( ( ^ [A: a > b,B: a > b] :
! [C: a,D: a] :
( ( sk1 @ C @ D )
=> ( sk3 @ C @ ( A @ C ) @ ( B @ D ) ) ) )
!= ( ^ [A: a > b,B: a > b] :
! [C: a,D: a] :
( ( sk1 @ C @ D )
=> ( sk3 @ C @ ( A @ C ) @ ( B @ D ) ) ) ) )
| sk4
| ~ ( sk3 @ sk12 @ ( sk9 @ sk12 ) @ ( sk11 @ sk13 ) ) ),
inference(rewrite,[status(thm)],[24,33]) ).
thf(331,plain,
( sk4
| ~ ( sk3 @ sk12 @ ( sk9 @ sk12 ) @ ( sk11 @ sk13 ) ) ),
inference(simp,[status(thm)],[330]) ).
thf(332,plain,
! [E: b,D: b,C: b,B: a,A: a] :
( ~ ( sk1 @ A @ B )
| ~ ( sk3 @ A @ C @ D )
| ~ ( sk3 @ A @ D @ E )
| sk4
| ~ $true
| ( ( sk3 @ A @ C @ E )
!= ( sk3 @ sk12 @ ( sk9 @ sk12 ) @ ( sk11 @ sk13 ) ) ) ),
inference(paramod_ordered,[status(thm)],[20,331]) ).
thf(333,plain,
! [E: b,D: b,C: b,B: a,A: a] :
( ~ ( sk1 @ A @ B )
| ~ ( sk3 @ A @ C @ D )
| ~ ( sk3 @ A @ D @ E )
| sk4
| ( ( sk3 @ A @ C @ E )
!= ( sk3 @ sk12 @ ( sk9 @ sk12 ) @ ( sk11 @ sk13 ) ) ) ),
inference(simp,[status(thm)],[332]) ).
thf(334,plain,
! [B: b,A: a] :
( ~ ( sk1 @ sk12 @ A )
| ~ ( sk3 @ sk12 @ ( sk9 @ sk12 ) @ B )
| ~ ( sk3 @ sk12 @ B @ ( sk11 @ sk13 ) )
| sk4 ),
inference(pattern_uni,[status(thm)],[333:[bind(A,$thf( sk12 )),bind(B,$thf( B )),bind(C,$thf( sk9 @ sk12 )),bind(D,$thf( D )),bind(E,$thf( sk11 @ sk13 ))]]) ).
thf(341,plain,
! [B: b,A: a] :
( ~ ( sk1 @ sk12 @ A )
| ~ ( sk3 @ sk12 @ ( sk9 @ sk12 ) @ B )
| ~ ( sk3 @ sk12 @ B @ ( sk11 @ sk13 ) )
| sk4 ),
inference(simp,[status(thm)],[334]) ).
thf(11948,plain,
! [B: b,A: a] :
( ~ ( sk1 @ sk12 @ A )
| ~ ( sk3 @ sk12 @ ( sk9 @ sk12 ) @ B )
| ~ ( sk3 @ sk12 @ B @ ( sk11 @ sk13 ) )
| $false ),
inference(rewrite,[status(thm)],[341,1312]) ).
thf(11949,plain,
! [B: b,A: a] :
( ~ ( sk1 @ sk12 @ A )
| ~ ( sk3 @ sk12 @ ( sk9 @ sk12 ) @ B )
| ~ ( sk3 @ sk12 @ B @ ( sk11 @ sk13 ) ) ),
inference(simp,[status(thm)],[11948]) ).
thf(12004,plain,
! [B: b,A: a] :
( ~ ( sk1 @ sk12 @ A )
| ~ $true
| ~ ( sk3 @ sk12 @ B @ ( sk11 @ sk13 ) )
| ( ( sk3 @ sk12 @ ( sk9 @ sk12 ) @ ( sk10 @ sk12 ) )
!= ( sk3 @ sk12 @ ( sk9 @ sk12 ) @ B ) ) ),
inference(paramod_ordered,[status(thm)],[1347,11949]) ).
thf(12005,plain,
! [B: b,A: a] :
( ~ ( sk1 @ sk12 @ A )
| ~ ( sk3 @ sk12 @ B @ ( sk11 @ sk13 ) )
| ( ( sk3 @ sk12 @ ( sk9 @ sk12 ) @ ( sk10 @ sk12 ) )
!= ( sk3 @ sk12 @ ( sk9 @ sk12 ) @ B ) ) ),
inference(simp,[status(thm)],[12004]) ).
thf(12006,plain,
! [A: a] :
( ~ ( sk1 @ sk12 @ A )
| ~ ( sk3 @ sk12 @ ( sk10 @ sk12 ) @ ( sk11 @ sk13 ) ) ),
inference(pattern_uni,[status(thm)],[12005:[bind(A,$thf( A )),bind(B,$thf( sk10 @ sk12 ))]]) ).
thf(8,plain,
! [B: a,A: a] :
( sk4
| ~ ( sk1 @ A @ B )
| ( sk3 @ A @ ( sk10 @ A ) @ ( sk11 @ B ) )
| ( ( ^ [C: a > b,D: a > b] :
! [E: a,F: a] :
( ( sk1 @ E @ F )
=> ( sk3 @ E @ ( C @ E ) @ ( D @ F ) ) ) )
!= ( ^ [C: a > b,D: a > b] :
! [E: a,F: a] :
( ( sk2 @ E @ F )
=> ( sk3 @ E @ ( C @ E ) @ ( D @ F ) ) ) ) ) ),
inference(cnfConj,[status(thm)],[5]) ).
thf(29,plain,
! [B: a,A: a] :
( ( ( ^ [C: a > b,D: a > b] :
! [E: a,F: a] :
( ( sk2 @ E @ F )
=> ( sk3 @ E @ ( C @ E ) @ ( D @ F ) ) ) )
!= ( ^ [C: a > b,D: a > b] :
! [E: a,F: a] :
( ( sk1 @ E @ F )
=> ( sk3 @ E @ ( C @ E ) @ ( D @ F ) ) ) ) )
| sk4
| ~ ( sk1 @ A @ B )
| ( sk3 @ A @ ( sk10 @ A ) @ ( sk11 @ B ) ) ),
inference(lifteq,[status(thm)],[8]) ).
thf(30,plain,
! [B: a,A: a] :
( ( ( ^ [C: a > b,D: a > b] :
! [E: a,F: a] :
( ( sk2 @ E @ F )
=> ( sk3 @ E @ ( C @ E ) @ ( D @ F ) ) ) )
!= ( ^ [C: a > b,D: a > b] :
! [E: a,F: a] :
( ( sk1 @ E @ F )
=> ( sk3 @ E @ ( C @ E ) @ ( D @ F ) ) ) ) )
| sk4
| ~ ( sk1 @ A @ B )
| ( sk3 @ A @ ( sk10 @ A ) @ ( sk11 @ B ) ) ),
inference(simp,[status(thm)],[29]) ).
thf(922,plain,
! [B: a,A: a] :
( ( ( ^ [C: a > b,D: a > b] :
! [E: a,F: a] :
( ( sk1 @ E @ F )
=> ( sk3 @ E @ ( C @ E ) @ ( D @ F ) ) ) )
!= ( ^ [C: a > b,D: a > b] :
! [E: a,F: a] :
( ( sk1 @ E @ F )
=> ( sk3 @ E @ ( C @ E ) @ ( D @ F ) ) ) ) )
| sk4
| ~ ( sk1 @ A @ B )
| ( sk3 @ A @ ( sk10 @ A ) @ ( sk11 @ B ) ) ),
inference(rewrite,[status(thm)],[30,33]) ).
thf(923,plain,
! [B: a,A: a] :
( sk4
| ~ ( sk1 @ A @ B )
| ( sk3 @ A @ ( sk10 @ A ) @ ( sk11 @ B ) ) ),
inference(simp,[status(thm)],[922]) ).
thf(958,plain,
! [B: a,A: a] :
( sk4
| sk4
| ~ $true
| ( sk3 @ A @ ( sk10 @ A ) @ ( sk11 @ B ) )
| ( ( sk1 @ sk12 @ sk13 )
!= ( sk1 @ A @ B ) ) ),
inference(paramod_ordered,[status(thm)],[60,923]) ).
thf(959,plain,
! [B: a,A: a] :
( sk4
| ( sk3 @ A @ ( sk10 @ A ) @ ( sk11 @ B ) )
| ( ( sk1 @ sk12 @ sk13 )
!= ( sk1 @ A @ B ) ) ),
inference(simp,[status(thm)],[958]) ).
thf(960,plain,
( sk4
| ( sk3 @ sk12 @ ( sk10 @ sk12 ) @ ( sk11 @ sk13 ) ) ),
inference(pattern_uni,[status(thm)],[959:[bind(A,$thf( sk12 )),bind(B,$thf( sk13 ))]]) ).
thf(1362,plain,
( $false
| ( sk3 @ sk12 @ ( sk10 @ sk12 ) @ ( sk11 @ sk13 ) ) ),
inference(rewrite,[status(thm)],[960,1312]) ).
thf(1363,plain,
sk3 @ sk12 @ ( sk10 @ sk12 ) @ ( sk11 @ sk13 ),
inference(simp,[status(thm)],[1362]) ).
thf(12578,plain,
! [A: a] :
( ~ ( sk1 @ sk12 @ A )
| ~ $true ),
inference(rewrite,[status(thm)],[12006,1363]) ).
thf(12579,plain,
! [A: a] :
~ ( sk1 @ sk12 @ A ),
inference(simp,[status(thm)],[12578]) ).
thf(12584,plain,
$false,
inference(rewrite,[status(thm)],[1351,12579]) ).
thf(12585,plain,
$false,
inference(simp,[status(thm)],[12584]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV037^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.11/0.22 % Computer : n015.cluster.edu
% 0.11/0.22 % Model : x86_64 x86_64
% 0.11/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.22 % Memory : 8046.5625MB
% 0.11/0.22 % OS : Linux 6.8.0-71-generic
% 0.11/0.22 % CPULimit : 300
% 0.11/0.22 % WCLimit : 300
% 0.11/0.22 % DateTime : Tue Sep 29 15:07:38 UTC 2026
% 0.11/0.22 % CPUTime :
% 0.11/0.22 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.88/0.79 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.22/0.99 % [INFO] Parsing done (202ms).
% 1.22/1.01 % [INFO] Running in sequential loop mode.
% 2.24/1.51 % [INFO] eprover registered as external prover.
% 2.24/1.52 % [INFO] Scanning for conjecture ...
% 2.46/1.69 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 2.65/1.75 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 2.65/1.75 % [INFO] Problem is higher-order (TPTP THF).
% 2.65/1.76 % [INFO] Type checking passed.
% 2.65/1.76 % [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 ...
% 32.90/7.64 % [INFO] Killing All external provers ...
% 32.90/7.64 % Time passed: 7287ms (effective reasoning time: 6623ms)
% 32.90/7.64 % 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)>
% 32.90/7.64 % Axioms used in derivation (0):
% 32.90/7.64 % No. of inferences in proof: 96
% 32.90/7.64 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 7287 ms resp. 6623 ms w/o parsing
% 30.47/7.71 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 30.47/7.71 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------