%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SEV386^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 : n019.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:37:13 AM UTC 2026
% Result : Theorem 37.72s 7.28s
% Output : Refutation 29.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 83
% Number of leaves : 5
% Syntax : Number of formulae : 187 ( 24 unt; 0 typ; 4 def)
% Number of atoms : 854 ( 452 equ; 84 cnn)
% Maximal formula atoms : 6 ( 4 avg)
% Number of connectives : 1186 ( 294 ~; 344 |; 17 &; 509 @)
% ( 0 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Number of types : 2 ( 1 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 13 ( 9 usr; 10 con; 0-2 aty)
% Number of variables : 91 ( 3 ^; 74 !; 10 ?; 91 :)
% ( 0 !>; 0 ?*; 0 @-; 4 @+)
% Comments :
%------------------------------------------------------------------------------
thf(a_type,type,
a: $tType ).
thf(p_decl,type,
p: a > $o ).
thf(sk2_decl,type,
sk2: a ).
thf(sk3_decl,type,
sk3: a > a ).
thf(sk4_decl,type,
sk4: a ).
thf(sk5_decl,type,
sk5: a ).
thf(sk20_decl,type,
sk20: a ).
thf(sk23_decl,type,
sk23: a ).
thf(sk24_decl,type,
sk24: a ).
thf(sk25_decl,type,
sk25: a ).
thf(sk2_def,definition,
( sk2
= ( @+[A: a] :
( ( p @ A )
& ! [B: a] :
( ( p @ B )
=> ( A = B ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( ^ [A: a] :
@+[B: a] :
( p
= ( (=) @ a @ B ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( @+[A: a] :
~ ( ( p @ A )
=> ( sk4 = A ) ) ) ) ).
thf(sk20_def,definition,
( sk20
= ( @+[A: a] :
~ ( ( p @ A )
=> ( sk2 = A ) ) ) ) ).
thf(1,conjecture,
( ( ? [A: a] :
( p
= ( (=) @ a @ A ) ) )
= ( ? [A: a] :
( ( p @ A )
& ! [B: a] :
( ( p @ B )
=> ( A = B ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cTTTP5306A_pme) ).
thf(2,negated_conjecture,
( ( ? [A: a] :
( p
= ( (=) @ a @ A ) ) )
!= ( ? [A: a] :
( ( p @ A )
& ! [B: a] :
( ( p @ B )
=> ( A = B ) ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(3,plain,
( ( ? [A: a] :
( p
= ( (=) @ a @ A ) ) )
!= ( ? [A: a] :
( ( p @ A )
& ! [B: a] :
( ( p @ B )
=> ( A = B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(4,plain,
( ( ? [A: a] :
( ( p @ A )
& ! [B: a] :
( ( p @ B )
=> ( A = B ) ) ) )
!= ( ? [A: a] :
( p
= ( (=) @ a @ A ) ) ) ),
inference(lifteq,[status(thm)],[3]) ).
thf(7,plain,
( ? [A: a] :
( ( p @ A )
& ! [B: a] :
( ( p @ B )
=> ( A = B ) ) )
| ? [A: a] :
( p
= ( (=) @ a @ A ) ) ),
inference(bool_ext,[status(thm)],[4]) ).
thf(13,plain,
! [A: a] :
( ( ( p @ sk2 )
| ( p
= ( (=) @ a @ ( sk3 @ A ) ) ) )
& ( ~ ( p @ A )
| ( sk2 = A )
| ( p
= ( (=) @ a @ ( sk3 @ A ) ) ) ) ),
inference(cnf,[status(esa)],[7]) ).
thf(14,plain,
! [A: a] :
( ( p @ sk2 )
| ( p
= ( (=) @ a @ ( sk3 @ A ) ) ) ),
inference(cnfConj,[status(thm)],[13]) ).
thf(16,plain,
! [A: a] :
( ( p
= ( (=) @ a @ ( sk3 @ A ) ) )
| ( p @ sk2 ) ),
inference(lifteq,[status(thm)],[14]) ).
thf(47,plain,
! [B: a,A: a] :
( ( ( p @ B )
= ( ( sk3 @ A )
= B ) )
| ( p @ sk2 ) ),
inference(func_ext,[status(esa)],[16]) ).
thf(5,plain,
( ( ^ [A: a] :
( ( p @ A )
& ! [B: a] :
( ( p @ B )
=> ( A = B ) ) ) )
!= ( ^ [A: a] :
( p
= ( (=) @ a @ A ) ) ) ),
inference(simp,[status(thm)],[4]) ).
thf(18,plain,
( ( ( p @ sk4 )
& ! [A: a] :
( ( p @ A )
=> ( sk4 = A ) ) )
!= ( p
= ( (=) @ a @ sk4 ) ) ),
inference(func_ext,[status(esa)],[5]) ).
thf(20,plain,
( ( ( p @ sk4 )
& ! [A: a] :
( ( p @ A )
=> ( sk4 = A ) ) )
| ( p
= ( (=) @ a @ sk4 ) ) ),
inference(bool_ext,[status(thm)],[18]) ).
thf(22,plain,
( ( p
= ( (=) @ a @ sk4 ) )
| ( ( p @ sk4 )
& ! [A: a] :
( ( p @ A )
=> ( sk4 = A ) ) ) ),
inference(lifteq,[status(thm)],[20]) ).
thf(27,plain,
! [A: a] :
( ( ( p
= ( (=) @ a @ sk4 ) )
| ( p @ sk4 ) )
& ( ( p
= ( (=) @ a @ sk4 ) )
| ~ ( p @ A )
| ( sk4 = A ) ) ),
inference(cnf,[status(esa)],[22]) ).
thf(28,plain,
( ( p
= ( (=) @ a @ sk4 ) )
| ( p @ sk4 ) ),
inference(cnfConj,[status(thm)],[27]) ).
thf(294,plain,
! [B: a,A: a] :
( ( p @ sk2 )
| ( p
= ( (=) @ a @ sk4 ) )
| ( ( sk3 @ A )
= B )
| ( ( p @ B )
!= ( p @ sk4 ) ) ),
inference(paramod_ordered,[status(thm)],[47,28]) ).
thf(295,plain,
! [A: a] :
( ( p @ sk2 )
| ( p
= ( (=) @ a @ sk4 ) )
| ( ( sk3 @ A )
= sk4 ) ),
inference(pattern_uni,[status(thm)],[294:[bind(A,$thf( A )),bind(B,$thf( sk4 ))]]) ).
thf(305,plain,
! [A: a] :
( ( ( sk3 @ A )
= sk4 )
| ( p @ sk2 )
| ( p
= ( (=) @ a @ sk4 ) ) ),
inference(lifteq,[status(thm)],[295]) ).
thf(424,plain,
! [B: a,A: a] :
( ( p @ sk2 )
| ( p
= ( (=) @ a @ sk4 ) )
| ( p
= ( (=) @ a @ sk4 ) )
| ( p @ sk2 )
| ( ( sk3 @ A )
!= ( sk3 @ B ) ) ),
inference(paramod_ordered,[status(thm)],[305,16]) ).
thf(425,plain,
! [B: a,A: a] :
( ( p @ sk2 )
| ( p
= ( (=) @ a @ sk4 ) )
| ( ( sk3 @ A )
!= ( sk3 @ B ) ) ),
inference(simp,[status(thm)],[424]) ).
thf(426,plain,
( ( p @ sk2 )
| ( p
= ( (=) @ a @ sk4 ) ) ),
inference(pattern_uni,[status(thm)],[425:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(466,plain,
! [A: a] :
( ( ( p @ A )
= ( sk4 = A ) )
| ( p @ sk2 ) ),
inference(func_ext,[status(esa)],[426]) ).
thf(19,plain,
( ~ ( ( p @ sk4 )
& ! [A: a] :
( ( p @ A )
=> ( sk4 = A ) ) )
| ( p
!= ( (=) @ a @ sk4 ) ) ),
inference(bool_ext,[status(thm)],[18]) ).
thf(21,plain,
( ( p
!= ( (=) @ a @ sk4 ) )
| ~ ( ( p @ sk4 )
& ! [A: a] :
( ( p @ A )
=> ( sk4 = A ) ) ) ),
inference(lifteq,[status(thm)],[19]) ).
thf(23,plain,
( ( ( p
!= ( (=) @ a @ sk4 ) )
| ~ ( p @ sk4 )
| ( p @ sk5 ) )
& ( ( p
!= ( (=) @ a @ sk4 ) )
| ~ ( p @ sk4 )
| ( sk4 != sk5 ) ) ),
inference(cnf,[status(esa)],[21]) ).
thf(24,plain,
( ( p
!= ( (=) @ a @ sk4 ) )
| ~ ( p @ sk4 )
| ( p @ sk5 ) ),
inference(cnfConj,[status(thm)],[23]) ).
thf(469,plain,
( ( p @ sk2 )
| ( ( (=) @ a @ sk4 )
!= ( (=) @ a @ sk4 ) )
| ~ ( p @ sk4 )
| ( p @ sk5 )
| ( p != p ) ),
inference(paramod_ordered,[status(thm)],[426,24]) ).
thf(470,plain,
( ( p @ sk2 )
| ~ ( p @ sk4 )
| ( p @ sk5 )
| ( p != p ) ),
inference(simp,[status(thm)],[469]) ).
thf(471,plain,
( ( p @ sk2 )
| ~ ( p @ sk4 )
| ( p @ sk5 ) ),
inference(pattern_uni,[status(thm)],[470:[]]) ).
thf(1279,plain,
! [A: a] :
( ( p @ sk2 )
| ( p @ sk2 )
| ( sk4 != A )
| ( p @ sk5 )
| ( ( p @ A )
!= ( p @ sk4 ) ) ),
inference(paramod_ordered,[status(thm)],[466,471]) ).
thf(1280,plain,
! [A: a] :
( ( p @ sk2 )
| ( sk4 != A )
| ( p @ sk5 )
| ( ( p @ A )
!= ( p @ sk4 ) ) ),
inference(simp,[status(thm)],[1279]) ).
thf(1281,plain,
( ( p @ sk2 )
| ( sk4 != sk4 )
| ( p @ sk5 ) ),
inference(pattern_uni,[status(thm)],[1280:[bind(A,$thf( sk4 ))]]) ).
thf(1397,plain,
( ( sk4 != sk4 )
| ( p @ sk2 )
| ( p @ sk5 ) ),
inference(lifteq,[status(thm)],[1281]) ).
thf(1438,plain,
( ( p @ sk2 )
| ( p @ sk5 ) ),
inference(simp,[status(thm)],[1397]) ).
thf(1547,plain,
! [A: a] :
( ( p @ sk2 )
| ( p @ sk2 )
| ( sk4 = A )
| ( ( p @ A )
!= ( p @ sk5 ) ) ),
inference(paramod_ordered,[status(thm)],[466,1438]) ).
thf(1548,plain,
! [A: a] :
( ( p @ sk2 )
| ( sk4 = A )
| ( ( p @ A )
!= ( p @ sk5 ) ) ),
inference(simp,[status(thm)],[1547]) ).
thf(1549,plain,
( ( p @ sk2 )
| ( sk4 = sk5 ) ),
inference(pattern_uni,[status(thm)],[1548:[bind(A,$thf( sk5 ))]]) ).
thf(1567,plain,
( ( sk5 = sk4 )
| ( p @ sk2 ) ),
inference(lifteq,[status(thm)],[1549]) ).
thf(25,plain,
( ( p
!= ( (=) @ a @ sk4 ) )
| ~ ( p @ sk4 )
| ( sk4 != sk5 ) ),
inference(cnfConj,[status(thm)],[23]) ).
thf(26,plain,
( ( sk5 != sk4 )
| ( p
!= ( (=) @ a @ sk4 ) )
| ~ ( p @ sk4 ) ),
inference(lifteq,[status(thm)],[25]) ).
thf(492,plain,
( ( p @ sk2 )
| ( sk5 != sk4 )
| ( ( (=) @ a @ sk4 )
!= ( (=) @ a @ sk4 ) )
| ~ ( p @ sk4 )
| ( p != p ) ),
inference(paramod_ordered,[status(thm)],[426,26]) ).
thf(493,plain,
( ( p @ sk2 )
| ( sk5 != sk4 )
| ~ ( p @ sk4 )
| ( p != p ) ),
inference(simp,[status(thm)],[492]) ).
thf(494,plain,
( ( p @ sk2 )
| ( sk5 != sk4 )
| ~ ( p @ sk4 ) ),
inference(pattern_uni,[status(thm)],[493:[]]) ).
thf(1299,plain,
! [A: a] :
( ( p @ sk2 )
| ( p @ sk2 )
| ( sk5 != sk4 )
| ( sk4 != A )
| ( ( p @ A )
!= ( p @ sk4 ) ) ),
inference(paramod_ordered,[status(thm)],[466,494]) ).
thf(1300,plain,
! [A: a] :
( ( p @ sk2 )
| ( sk5 != sk4 )
| ( sk4 != A )
| ( ( p @ A )
!= ( p @ sk4 ) ) ),
inference(simp,[status(thm)],[1299]) ).
thf(1301,plain,
( ( p @ sk2 )
| ( sk5 != sk4 )
| ( sk4 != sk4 ) ),
inference(pattern_uni,[status(thm)],[1300:[bind(A,$thf( sk4 ))]]) ).
thf(1402,plain,
( ( sk4 != sk4 )
| ( p @ sk2 )
| ( sk5 != sk4 ) ),
inference(lifteq,[status(thm)],[1301]) ).
thf(1443,plain,
( ( p @ sk2 )
| ( sk5 != sk4 ) ),
inference(simp,[status(thm)],[1402]) ).
thf(2070,plain,
( ( p @ sk2 )
| ( p @ sk2 )
| ( sk4 != sk4 )
| ( sk5 != sk5 ) ),
inference(paramod_ordered,[status(thm)],[1567,1443]) ).
thf(2071,plain,
( ( p @ sk2 )
| ( sk5 != sk5 ) ),
inference(simp,[status(thm)],[2070]) ).
thf(2072,plain,
p @ sk2,
inference(pattern_uni,[status(thm)],[2071:[]]) ).
thf(1256,plain,
! [A: a] :
( ( p @ sk2 )
| ( p @ A )
| ( sk4 != A ) ),
inference(bool_ext,[status(thm)],[466]) ).
thf(1382,plain,
! [A: a] :
( ( sk4 != A )
| ( p @ sk2 )
| ( p @ A ) ),
inference(lifteq,[status(thm)],[1256]) ).
thf(1430,plain,
( ( p @ sk2 )
| ( p @ sk4 ) ),
inference(simp,[status(thm)],[1382]) ).
thf(1508,plain,
( ( p @ sk2 )
| ( ( p @ sk4 )
!= ( p @ sk2 ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[1430]) ).
thf(1515,plain,
( ( p @ sk2 )
| ( sk4 != sk2 ) ),
inference(simp,[status(thm)],[1508]) ).
thf(1966,plain,
( ( sk4 != sk2 )
| ( ( $true
& ! [A: a] :
( ( p @ A )
=> ( sk4 = A ) ) )
!= ( p
= ( (=) @ a @ sk4 ) ) )
| ( ( p @ sk4 )
!= ( p @ sk2 ) ) ),
inference(paramod_ordered,[status(thm)],[1515,18]) ).
thf(1967,plain,
( ( sk4 != sk2 )
| ( ( ! [A: a] :
( ( p @ A )
=> ( sk4 = A ) ) )
!= ( p
= ( (=) @ a @ sk4 ) ) )
| ( ( p @ sk4 )
!= ( p @ sk2 ) ) ),
inference(simp,[status(thm)],[1966]) ).
thf(2022,plain,
( ( sk4 != sk2 )
| ( ( ! [A: a] :
( ( p @ A )
=> ( sk4 = A ) ) )
!= ( p
= ( (=) @ a @ sk4 ) ) )
| ( sk4 != sk2 ) ),
inference(simp,[status(thm)],[1967]) ).
thf(2031,plain,
( ( sk4 != sk2 )
| ( ( ! [A: a] :
( ( p @ A )
=> ( sk4 = A ) ) )
!= ( p
= ( (=) @ a @ sk4 ) ) ) ),
inference(simp,[status(thm)],[2022]) ).
thf(29,plain,
! [A: a] :
( ( p
= ( (=) @ a @ sk4 ) )
| ~ ( p @ A )
| ( sk4 = A ) ),
inference(cnfConj,[status(thm)],[27]) ).
thf(30,plain,
! [A: a] :
( ( sk4 = A )
| ( p
= ( (=) @ a @ sk4 ) )
| ~ ( p @ A ) ),
inference(lifteq,[status(thm)],[29]) ).
thf(495,plain,
! [A: a] :
( ( p
= ( (=) @ a @ sk4 ) )
| ( sk4 = A )
| ( p
= ( (=) @ a @ sk4 ) )
| ~ $true
| ( ( p @ sk2 )
!= ( p @ A ) ) ),
inference(paramod_ordered,[status(thm)],[426,30]) ).
thf(496,plain,
! [A: a] :
( ( p
= ( (=) @ a @ sk4 ) )
| ( sk4 = A )
| ( ( p @ sk2 )
!= ( p @ A ) ) ),
inference(simp,[status(thm)],[495]) ).
thf(497,plain,
( ( p
= ( (=) @ a @ sk4 ) )
| ( sk4 = sk2 ) ),
inference(pattern_uni,[status(thm)],[496:[bind(A,$thf( sk2 ))]]) ).
thf(530,plain,
! [A: a] :
( ( ( p @ A )
= ( sk4 = A ) )
| ( sk4 = sk2 ) ),
inference(func_ext,[status(esa)],[497]) ).
thf(2790,plain,
! [A: a] :
( ( sk4 = A )
| ( sk4 = sk2 )
| ( ( p @ sk2 )
!= ( p @ A ) ) ),
inference(paramod_ordered,[status(thm)],[2072,530]) ).
thf(2791,plain,
( ( sk4 = sk2 )
| ( sk4 = sk2 ) ),
inference(pattern_uni,[status(thm)],[2790:[bind(A,$thf( sk2 ))]]) ).
thf(2879,plain,
( ( sk4 = sk2 )
| ( sk4 = sk2 ) ),
inference(lifteq,[status(thm)],[2791]) ).
thf(2906,plain,
sk4 = sk2,
inference(simp,[status(thm)],[2879]) ).
thf(3011,plain,
( ( sk2 != sk2 )
| ( ( ! [A: a] :
( ( p @ A )
=> ( sk2 = A ) ) )
!= ( p
= ( (=) @ a @ sk2 ) ) ) ),
inference(rewrite,[status(thm)],[2031,2906]) ).
thf(3012,plain,
( ( ! [A: a] :
( ( p @ A )
=> ( sk2 = A ) ) )
!= ( p
= ( (=) @ a @ sk2 ) ) ),
inference(simp,[status(thm)],[3011]) ).
thf(3035,plain,
( ~ ! [A: a] :
( ( p @ A )
=> ( sk2 = A ) )
| ( p
!= ( (=) @ a @ sk2 ) ) ),
inference(bool_ext,[status(thm)],[3012]) ).
thf(3050,plain,
( ( p
!= ( (=) @ a @ sk2 ) )
| ~ ! [A: a] :
( ( p @ A )
=> ( sk2 = A ) ) ),
inference(lifteq,[status(thm)],[3035]) ).
thf(3054,plain,
( ( ( p
!= ( (=) @ a @ sk2 ) )
| ( p @ sk20 ) )
& ( ( p
!= ( (=) @ a @ sk2 ) )
| ( sk2 != sk20 ) ) ),
inference(cnf,[status(esa)],[3050]) ).
thf(3055,plain,
( ( p
!= ( (=) @ a @ sk2 ) )
| ( p @ sk20 ) ),
inference(cnfConj,[status(thm)],[3054]) ).
thf(3083,plain,
( ( ( p @ sk24 )
!= ( sk2 = sk24 ) )
| ( p @ sk20 ) ),
inference(func_ext,[status(esa)],[3055]) ).
thf(3210,plain,
( ( p @ sk20 )
| ( p @ sk24 )
| ( sk2 = sk24 ) ),
inference(bool_ext,[status(thm)],[3083]) ).
thf(3219,plain,
( ( sk24 = sk2 )
| ( p @ sk20 )
| ( p @ sk24 ) ),
inference(lifteq,[status(thm)],[3210]) ).
thf(15,plain,
! [A: a] :
( ~ ( p @ A )
| ( sk2 = A )
| ( p
= ( (=) @ a @ ( sk3 @ A ) ) ) ),
inference(cnfConj,[status(thm)],[13]) ).
thf(17,plain,
! [A: a] :
( ( sk2 = A )
| ( p
= ( (=) @ a @ ( sk3 @ A ) ) )
| ~ ( p @ A ) ),
inference(lifteq,[status(thm)],[15]) ).
thf(3286,plain,
! [A: a] :
( ( sk24 = sk2 )
| ( p @ sk20 )
| ( sk2 = A )
| ( p
= ( (=) @ a @ ( sk3 @ A ) ) )
| ~ $true
| ( ( p @ sk24 )
!= ( p @ A ) ) ),
inference(paramod_ordered,[status(thm)],[3219,17]) ).
thf(3287,plain,
! [A: a] :
( ( sk24 = sk2 )
| ( p @ sk20 )
| ( sk2 = A )
| ( p
= ( (=) @ a @ ( sk3 @ A ) ) )
| ( ( p @ sk24 )
!= ( p @ A ) ) ),
inference(simp,[status(thm)],[3286]) ).
thf(3288,plain,
( ( sk24 = sk2 )
| ( p @ sk20 )
| ( sk24 = sk2 )
| ( p
= ( (=) @ a @ ( sk3 @ sk24 ) ) ) ),
inference(pattern_uni,[status(thm)],[3287:[bind(A,$thf( sk24 ))]]) ).
thf(3331,plain,
( ( sk24 = sk2 )
| ( p @ sk20 )
| ( p
= ( (=) @ a @ ( sk3 @ sk24 ) ) ) ),
inference(simp,[status(thm)],[3288]) ).
thf(3209,plain,
( ( p @ sk20 )
| ~ ( p @ sk24 )
| ( sk2 != sk24 ) ),
inference(bool_ext,[status(thm)],[3083]) ).
thf(3222,plain,
( ( sk24 != sk2 )
| ( p @ sk20 )
| ~ ( p @ sk24 ) ),
inference(lifteq,[status(thm)],[3209]) ).
thf(3833,plain,
( ( sk24 != sk2 )
| ( p @ sk20 )
| ~ $true
| ( ( p @ sk24 )
!= ( p @ sk2 ) ) ),
inference(paramod_ordered,[status(thm)],[2072,3222]) ).
thf(3834,plain,
( ( sk24 != sk2 )
| ( p @ sk20 )
| ( ( p @ sk24 )
!= ( p @ sk2 ) ) ),
inference(simp,[status(thm)],[3833]) ).
thf(3848,plain,
( ( p @ sk20 )
| ( sk24 != sk2 )
| ( sk24 != sk2 ) ),
inference(simp,[status(thm)],[3834]) ).
thf(3856,plain,
( ( p @ sk20 )
| ( sk24 != sk2 ) ),
inference(simp,[status(thm)],[3848]) ).
thf(5324,plain,
( ( p @ sk20 )
| ( p
= ( (=) @ a @ ( sk3 @ sk24 ) ) )
| ( p @ sk20 )
| ( sk2 != sk2 )
| ( sk24 != sk24 ) ),
inference(paramod_ordered,[status(thm)],[3331,3856]) ).
thf(5325,plain,
( ( p @ sk20 )
| ( p
= ( (=) @ a @ ( sk3 @ sk24 ) ) )
| ( sk24 != sk24 ) ),
inference(simp,[status(thm)],[5324]) ).
thf(5326,plain,
( ( p @ sk20 )
| ( p
= ( (=) @ a @ ( sk3 @ sk24 ) ) ) ),
inference(pattern_uni,[status(thm)],[5325:[]]) ).
thf(5402,plain,
! [A: a] :
( ( ( p @ A )
= ( ( sk3 @ sk24 )
= A ) )
| ( p @ sk20 ) ),
inference(func_ext,[status(esa)],[5326]) ).
thf(6403,plain,
! [A: a] :
( ( ( sk3 @ sk24 )
= A )
| ( p @ sk20 )
| ( ( p @ sk2 )
!= ( p @ A ) ) ),
inference(paramod_ordered,[status(thm)],[2072,5402]) ).
thf(6404,plain,
( ( ( sk3 @ sk24 )
= sk2 )
| ( p @ sk20 ) ),
inference(pattern_uni,[status(thm)],[6403:[bind(A,$thf( sk2 ))]]) ).
thf(6546,plain,
( ( ( sk3 @ sk24 )
= sk2 )
| ( p @ sk20 ) ),
inference(lifteq,[status(thm)],[6404]) ).
thf(5440,plain,
( ( p @ sk20 )
| ( ( (=) @ a @ ( sk3 @ sk24 ) )
!= ( (=) @ a @ sk2 ) )
| ( p @ sk20 )
| ( p != p ) ),
inference(paramod_ordered,[status(thm)],[5326,3055]) ).
thf(5441,plain,
( ( p @ sk20 )
| ( ( (=) @ a @ ( sk3 @ sk24 ) )
!= ( (=) @ a @ sk2 ) )
| ( p != p ) ),
inference(simp,[status(thm)],[5440]) ).
thf(5442,plain,
( ( p @ sk20 )
| ( ( (=) @ a @ ( sk3 @ sk24 ) )
!= ( (=) @ a @ sk2 ) ) ),
inference(pattern_uni,[status(thm)],[5441:[]]) ).
thf(6663,plain,
( ( p @ sk20 )
| ( p @ sk20 )
| ( ( (=) @ a @ sk2 )
!= ( (=) @ a @ sk2 ) )
| ( ( sk3 @ sk24 )
!= ( sk3 @ sk24 ) ) ),
inference(paramod_ordered,[status(thm)],[6546,5442]) ).
thf(6664,plain,
( ( p @ sk20 )
| ( ( sk3 @ sk24 )
!= ( sk3 @ sk24 ) ) ),
inference(simp,[status(thm)],[6663]) ).
thf(6665,plain,
p @ sk20,
inference(pattern_uni,[status(thm)],[6664:[]]) ).
thf(102,plain,
! [A: a] :
( ( sk4 = A )
| ~ ( p @ A )
| ( ( (=) @ a @ sk4 )
!= ( (=) @ a @ sk4 ) )
| ~ ( p @ sk4 )
| ( p @ sk5 )
| ( p != p ) ),
inference(paramod_ordered,[status(thm)],[30,24]) ).
thf(103,plain,
! [A: a] :
( ( sk4 = A )
| ~ ( p @ A )
| ~ ( p @ sk4 )
| ( p @ sk5 )
| ( p != p ) ),
inference(simp,[status(thm)],[102]) ).
thf(104,plain,
! [A: a] :
( ( sk4 = A )
| ~ ( p @ A )
| ~ ( p @ sk4 )
| ( p @ sk5 ) ),
inference(pattern_uni,[status(thm)],[103:[]]) ).
thf(4321,plain,
! [A: a] :
( ( sk2 = A )
| ~ ( p @ A )
| ~ ( p @ sk2 )
| ( p @ sk5 ) ),
inference(rewrite,[status(thm)],[104,2906]) ).
thf(6699,plain,
! [A: a] :
( ( sk2 = A )
| ~ $true
| ~ ( p @ sk2 )
| ( p @ sk5 )
| ( ( p @ sk20 )
!= ( p @ A ) ) ),
inference(paramod_ordered,[status(thm)],[6665,4321]) ).
thf(6700,plain,
! [A: a] :
( ( sk2 = A )
| ~ ( p @ sk2 )
| ( p @ sk5 )
| ( ( p @ sk20 )
!= ( p @ A ) ) ),
inference(simp,[status(thm)],[6699]) ).
thf(6701,plain,
( ( sk20 = sk2 )
| ~ ( p @ sk2 )
| ( p @ sk5 ) ),
inference(pattern_uni,[status(thm)],[6700:[bind(A,$thf( sk20 ))]]) ).
thf(7657,plain,
( ( sk20 = sk2 )
| ~ $true
| ( p @ sk5 ) ),
inference(rewrite,[status(thm)],[6701,2072]) ).
thf(7658,plain,
( ( sk20 = sk2 )
| ( p @ sk5 ) ),
inference(simp,[status(thm)],[7657]) ).
thf(3056,plain,
( ( p
!= ( (=) @ a @ sk2 ) )
| ( sk2 != sk20 ) ),
inference(cnfConj,[status(thm)],[3054]) ).
thf(3057,plain,
( ( sk20 != sk2 )
| ( p
!= ( (=) @ a @ sk2 ) ) ),
inference(lifteq,[status(thm)],[3056]) ).
thf(3105,plain,
( ( ( p @ sk25 )
!= ( sk2 = sk25 ) )
| ( sk20 != sk2 ) ),
inference(func_ext,[status(esa)],[3057]) ).
thf(3224,plain,
( ( sk20 != sk2 )
| ( p @ sk25 )
| ( sk2 = sk25 ) ),
inference(bool_ext,[status(thm)],[3105]) ).
thf(3238,plain,
( ( sk25 = sk2 )
| ( sk20 != sk2 )
| ( p @ sk25 ) ),
inference(lifteq,[status(thm)],[3224]) ).
thf(3223,plain,
( ( sk20 != sk2 )
| ~ ( p @ sk25 )
| ( sk2 != sk25 ) ),
inference(bool_ext,[status(thm)],[3105]) ).
thf(3237,plain,
( ( sk25 != sk2 )
| ( sk20 != sk2 )
| ~ ( p @ sk25 ) ),
inference(lifteq,[status(thm)],[3223]) ).
thf(3549,plain,
( ( sk25 != sk2 )
| ( sk20 != sk2 )
| ~ $true
| ( ( p @ sk25 )
!= ( p @ sk2 ) ) ),
inference(paramod_ordered,[status(thm)],[2072,3237]) ).
thf(3550,plain,
( ( sk25 != sk2 )
| ( sk20 != sk2 )
| ( ( p @ sk25 )
!= ( p @ sk2 ) ) ),
inference(simp,[status(thm)],[3549]) ).
thf(3557,plain,
( ( sk25 != sk2 )
| ( sk20 != sk2 )
| ( sk25 != sk2 ) ),
inference(simp,[status(thm)],[3550]) ).
thf(3564,plain,
( ( sk25 != sk2 )
| ( sk20 != sk2 ) ),
inference(simp,[status(thm)],[3557]) ).
thf(4055,plain,
( ( sk20 != sk2 )
| ( p @ sk25 )
| ( sk2 != sk2 )
| ( sk20 != sk2 )
| ( sk25 != sk25 ) ),
inference(paramod_ordered,[status(thm)],[3238,3564]) ).
thf(4056,plain,
( ( sk20 != sk2 )
| ( p @ sk25 )
| ( sk25 != sk25 ) ),
inference(simp,[status(thm)],[4055]) ).
thf(4057,plain,
( ( sk20 != sk2 )
| ( p @ sk25 ) ),
inference(pattern_uni,[status(thm)],[4056:[]]) ).
thf(7728,plain,
( ( p @ sk5 )
| ( sk2 != sk2 )
| ( p @ sk25 )
| ( sk20 != sk20 ) ),
inference(paramod_ordered,[status(thm)],[7658,4057]) ).
thf(7729,plain,
( ( p @ sk5 )
| ( p @ sk25 )
| ( sk20 != sk20 ) ),
inference(simp,[status(thm)],[7728]) ).
thf(7730,plain,
( ( p @ sk5 )
| ( p @ sk25 ) ),
inference(pattern_uni,[status(thm)],[7729:[]]) ).
thf(7675,plain,
( ( p @ sk5 )
| ( sk25 != sk2 )
| ( sk2 != sk2 )
| ( sk20 != sk20 ) ),
inference(paramod_ordered,[status(thm)],[7658,3564]) ).
thf(7676,plain,
( ( p @ sk5 )
| ( sk25 != sk2 )
| ( sk20 != sk20 ) ),
inference(simp,[status(thm)],[7675]) ).
thf(7677,plain,
( ( p @ sk5 )
| ( sk25 != sk2 ) ),
inference(pattern_uni,[status(thm)],[7676:[]]) ).
thf(7784,plain,
! [A: a] :
( ~ ( p @ A )
| ~ ( p @ sk2 )
| ( p @ sk5 )
| ( p @ sk5 )
| ( sk2 != sk2 )
| ( A != sk25 ) ),
inference(paramod_ordered,[status(thm)],[4321,7677]) ).
thf(7785,plain,
! [A: a] :
( ~ ( p @ A )
| ~ ( p @ sk2 )
| ( p @ sk5 )
| ( A != sk25 ) ),
inference(simp,[status(thm)],[7784]) ).
thf(7786,plain,
( ~ ( p @ sk25 )
| ~ ( p @ sk2 )
| ( p @ sk5 ) ),
inference(pattern_uni,[status(thm)],[7785:[bind(A,$thf( sk25 ))]]) ).
thf(8549,plain,
( ~ ( p @ sk25 )
| ~ $true
| ( p @ sk5 ) ),
inference(rewrite,[status(thm)],[7786,2072]) ).
thf(8550,plain,
( ~ ( p @ sk25 )
| ( p @ sk5 ) ),
inference(simp,[status(thm)],[8549]) ).
thf(8571,plain,
( ( p @ sk5 )
| ~ $true
| ( p @ sk5 )
| ( ( p @ sk25 )
!= ( p @ sk25 ) ) ),
inference(paramod_ordered,[status(thm)],[7730,8550]) ).
thf(8572,plain,
( ( p @ sk5 )
| ( ( p @ sk25 )
!= ( p @ sk25 ) ) ),
inference(simp,[status(thm)],[8571]) ).
thf(8573,plain,
p @ sk5,
inference(pattern_uni,[status(thm)],[8572:[]]) ).
thf(8631,plain,
! [A: a] :
( ( sk2 = A )
| ( p
= ( (=) @ a @ ( sk3 @ A ) ) )
| ~ $true
| ( ( p @ sk5 )
!= ( p @ A ) ) ),
inference(paramod_ordered,[status(thm)],[8573,17]) ).
thf(8632,plain,
! [A: a] :
( ( sk2 = A )
| ( p
= ( (=) @ a @ ( sk3 @ A ) ) )
| ( ( p @ sk5 )
!= ( p @ A ) ) ),
inference(simp,[status(thm)],[8631]) ).
thf(8633,plain,
( ( sk5 = sk2 )
| ( p
= ( (=) @ a @ ( sk3 @ sk5 ) ) ) ),
inference(pattern_uni,[status(thm)],[8632:[bind(A,$thf( sk5 ))]]) ).
thf(1833,plain,
( ( sk5 != sk4 )
| ( sk5 != sk4 )
| ( p
!= ( (=) @ a @ sk4 ) )
| ~ $true
| ( ( p @ sk4 )
!= ( p @ sk2 ) ) ),
inference(paramod_ordered,[status(thm)],[1443,26]) ).
thf(1834,plain,
( ( sk5 != sk4 )
| ( p
!= ( (=) @ a @ sk4 ) )
| ( ( p @ sk4 )
!= ( p @ sk2 ) ) ),
inference(simp,[status(thm)],[1833]) ).
thf(1857,plain,
( ( sk5 != sk4 )
| ( p
!= ( (=) @ a @ sk4 ) )
| ( sk4 != sk2 ) ),
inference(simp,[status(thm)],[1834]) ).
thf(3020,plain,
( ( sk5 != sk2 )
| ( p
!= ( (=) @ a @ sk2 ) )
| ( sk2 != sk2 ) ),
inference(rewrite,[status(thm)],[1857,2906]) ).
thf(3021,plain,
( ( sk5 != sk2 )
| ( p
!= ( (=) @ a @ sk2 ) ) ),
inference(simp,[status(thm)],[3020]) ).
thf(3076,plain,
( ( ( p @ sk23 )
!= ( sk2 = sk23 ) )
| ( sk5 != sk2 ) ),
inference(func_ext,[status(esa)],[3021]) ).
thf(3193,plain,
( ( sk5 != sk2 )
| ( p @ sk23 )
| ( sk2 = sk23 ) ),
inference(bool_ext,[status(thm)],[3076]) ).
thf(3206,plain,
( ( sk23 = sk2 )
| ( sk5 != sk2 )
| ( p @ sk23 ) ),
inference(lifteq,[status(thm)],[3193]) ).
thf(3192,plain,
( ( sk5 != sk2 )
| ~ ( p @ sk23 )
| ( sk2 != sk23 ) ),
inference(bool_ext,[status(thm)],[3076]) ).
thf(3205,plain,
( ( sk23 != sk2 )
| ( sk5 != sk2 )
| ~ ( p @ sk23 ) ),
inference(lifteq,[status(thm)],[3192]) ).
thf(3352,plain,
( ( sk23 != sk2 )
| ( sk5 != sk2 )
| ~ $true
| ( ( p @ sk23 )
!= ( p @ sk2 ) ) ),
inference(paramod_ordered,[status(thm)],[2072,3205]) ).
thf(3353,plain,
( ( sk23 != sk2 )
| ( sk5 != sk2 )
| ( ( p @ sk23 )
!= ( p @ sk2 ) ) ),
inference(simp,[status(thm)],[3352]) ).
thf(3360,plain,
( ( sk23 != sk2 )
| ( sk5 != sk2 )
| ( sk23 != sk2 ) ),
inference(simp,[status(thm)],[3353]) ).
thf(3365,plain,
( ( sk23 != sk2 )
| ( sk5 != sk2 ) ),
inference(simp,[status(thm)],[3360]) ).
thf(3712,plain,
( ( sk5 != sk2 )
| ( p @ sk23 )
| ( sk2 != sk2 )
| ( sk5 != sk2 )
| ( sk23 != sk23 ) ),
inference(paramod_ordered,[status(thm)],[3206,3365]) ).
thf(3713,plain,
( ( sk5 != sk2 )
| ( p @ sk23 )
| ( sk23 != sk23 ) ),
inference(simp,[status(thm)],[3712]) ).
thf(3714,plain,
( ( sk5 != sk2 )
| ( p @ sk23 ) ),
inference(pattern_uni,[status(thm)],[3713:[]]) ).
thf(154,plain,
! [A: a] :
( ( sk4 = A )
| ~ ( p @ A )
| ( sk5 != sk4 )
| ( ( (=) @ a @ sk4 )
!= ( (=) @ a @ sk4 ) )
| ~ ( p @ sk4 )
| ( p != p ) ),
inference(paramod_ordered,[status(thm)],[30,26]) ).
thf(155,plain,
! [A: a] :
( ( sk4 = A )
| ~ ( p @ A )
| ( sk5 != sk4 )
| ~ ( p @ sk4 )
| ( p != p ) ),
inference(simp,[status(thm)],[154]) ).
thf(156,plain,
! [A: a] :
( ( sk4 = A )
| ~ ( p @ A )
| ( sk5 != sk4 )
| ~ ( p @ sk4 ) ),
inference(pattern_uni,[status(thm)],[155:[]]) ).
thf(8682,plain,
! [A: a] :
( ( sk2 = A )
| ~ ( p @ A )
| ( sk5 != sk2 )
| ~ ( p @ sk2 ) ),
inference(rewrite,[status(thm)],[156,2906]) ).
thf(8796,plain,
! [A: a] :
( ~ ( p @ A )
| ( sk5 != sk2 )
| ~ ( p @ sk2 )
| ( sk2 != sk2 )
| ( sk5 != sk2 )
| ( A != sk23 ) ),
inference(paramod_ordered,[status(thm)],[8682,3365]) ).
thf(8797,plain,
! [A: a] :
( ~ ( p @ A )
| ( sk5 != sk2 )
| ~ ( p @ sk2 )
| ( A != sk23 ) ),
inference(simp,[status(thm)],[8796]) ).
thf(8798,plain,
( ~ ( p @ sk23 )
| ( sk5 != sk2 )
| ~ ( p @ sk2 ) ),
inference(pattern_uni,[status(thm)],[8797:[bind(A,$thf( sk23 ))]]) ).
thf(9281,plain,
( ~ ( p @ sk23 )
| ( sk5 != sk2 )
| ~ $true ),
inference(rewrite,[status(thm)],[8798,2072]) ).
thf(9282,plain,
( ~ ( p @ sk23 )
| ( sk5 != sk2 ) ),
inference(simp,[status(thm)],[9281]) ).
thf(9286,plain,
( ( sk5 != sk2 )
| ~ $true
| ( sk5 != sk2 )
| ( ( p @ sk23 )
!= ( p @ sk23 ) ) ),
inference(paramod_ordered,[status(thm)],[3714,9282]) ).
thf(9287,plain,
( ( sk5 != sk2 )
| ( ( p @ sk23 )
!= ( p @ sk23 ) ) ),
inference(simp,[status(thm)],[9286]) ).
thf(9288,plain,
sk5 != sk2,
inference(pattern_uni,[status(thm)],[9287:[]]) ).
thf(9342,plain,
( p
= ( (=) @ a @ ( sk3 @ sk5 ) ) ),
inference(simplifyReflect,[status(thm)],[8633,9288]) ).
thf(9348,plain,
! [A: a] :
( ( p @ A )
= ( ( sk3 @ sk5 )
= A ) ),
inference(func_ext,[status(esa)],[9342]) ).
thf(9559,plain,
! [A: a] :
( ( ( sk3 @ sk5 )
= A )
| ( ( p @ A )
!= ( p @ sk5 ) ) ),
inference(paramod_ordered,[status(thm)],[9348,8573]) ).
thf(9560,plain,
( ( sk3 @ sk5 )
= sk5 ),
inference(pattern_uni,[status(thm)],[9559:[bind(A,$thf( sk5 ))]]) ).
thf(9636,plain,
( ( sk3 @ sk5 )
= sk5 ),
inference(lifteq,[status(thm)],[9560]) ).
thf(9543,plain,
! [A: a] :
( ( ( sk3 @ sk5 )
= A )
| ( ( p @ sk2 )
!= ( p @ A ) ) ),
inference(paramod_ordered,[status(thm)],[2072,9348]) ).
thf(9544,plain,
( ( sk3 @ sk5 )
= sk2 ),
inference(pattern_uni,[status(thm)],[9543:[bind(A,$thf( sk2 ))]]) ).
thf(9631,plain,
( ( sk3 @ sk5 )
= sk2 ),
inference(lifteq,[status(thm)],[9544]) ).
thf(9714,plain,
sk5 = sk2,
inference(rewrite,[status(thm)],[9636,9631]) ).
thf(9715,plain,
$false,
inference(simplifyReflect,[status(thm)],[9714,9288]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEV386^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % 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.19 % Computer : n019.cluster.edu
% 0.10/0.19 % Model : x86_64 x86_64
% 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.19 % Memory : 8046.5625MB
% 0.10/0.19 % OS : Linux 6.8.0-71-generic
% 0.10/0.19 % CPULimit : 300
% 0.10/0.19 % WCLimit : 300
% 0.10/0.19 % DateTime : Tue Sep 29 15:43:33 UTC 2026
% 0.10/0.20 % CPUTime :
% 0.10/0.20 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
% 0.76/0.53 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.02/0.64 % [INFO] Parsing done (109ms).
% 1.02/0.65 % [INFO] Running in sequential loop mode.
% 1.38/0.89 % [INFO] eprover registered as external prover.
% 1.38/0.89 % [INFO] Scanning for conjecture ...
% 1.63/0.95 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 1.63/0.97 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 1.63/0.97 % [INFO] Problem is higher-order (TPTP THF).
% 1.63/0.97 % [INFO] Type checking passed.
% 1.63/0.97 % [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 ...
% 37.72/7.27 % [INFO] Killing All external provers ...
% 37.72/7.27 % Time passed: 6983ms (effective reasoning time: 6615ms)
% 37.72/7.28 % 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)>
% 37.72/7.28 % Axioms used in derivation (0):
% 37.72/7.28 % No. of inferences in proof: 183
% 37.72/7.28 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 6983 ms resp. 6615 ms w/o parsing
% 29.32/7.41 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 29.32/7.41 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------