%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : NUM469+2 : 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 : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:08:55 AM UTC 2026
% Result : Theorem 116.63s 56.74s
% Output : Refutation 116.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 9
% Syntax : Number of formulae : 83 ( 20 unt; 0 typ; 2 def)
% Number of atoms : 227 ( 113 equ; 0 cnn)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 639 ( 76 ~; 71 |; 47 &; 437 @)
% ( 0 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 14 ( 11 usr; 8 con; 0-2 aty)
% Number of variables : 38 ( 0 ^; 29 !; 7 ?; 38 :)
% ( 0 !>; 0 ?*; 0 @-; 2 @+)
% Comments :
%------------------------------------------------------------------------------
thf(aNaturalNumber0_decl,type,
aNaturalNumber0: $i > $o ).
thf(sdtpldt0_decl,type,
sdtpldt0: $i > $i > $i ).
thf(doDivides0_decl,type,
doDivides0: $i > $i > $o ).
thf(sdtasdt0_decl,type,
sdtasdt0: $i > $i > $i ).
thf(sz00_decl,type,
sz00: $i ).
thf(sdtsldt0_decl,type,
sdtsldt0: $i > $i > $i ).
thf(xm_decl,type,
xm: $i ).
thf(xn_decl,type,
xn: $i ).
thf(xl_decl,type,
xl: $i ).
thf(sk3_decl,type,
sk3: $i ).
thf(sk4_decl,type,
sk4: $i ).
thf(sk3_def,definition,
( sk3
= ( @+[A: $i] :
( ( xm
= ( A @ ( xl @ sdtasdt0 ) ) )
& ( A @ aNaturalNumber0 ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( @+[A: $i] :
( ( xn
= ( A @ ( xl @ sdtasdt0 ) ) )
& ( A @ aNaturalNumber0 ) ) ) ) ).
thf(26,axiom,
! [A: $i,B: $i] :
( ( ( B @ aNaturalNumber0 )
& ( A @ aNaturalNumber0 ) )
=> ( B @ ( A @ sdtpldt0 ) @ aNaturalNumber0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsB) ).
thf(158,plain,
! [A: $i,B: $i] :
( ( ( B @ aNaturalNumber0 )
& ( A @ aNaturalNumber0 ) )
=> ( B @ ( A @ sdtpldt0 ) @ aNaturalNumber0 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(159,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ sdtpldt0 ) @ aNaturalNumber0 )
| ~ ( B @ aNaturalNumber0 )
| ~ ( A @ aNaturalNumber0 ) ),
inference(cnf,[status(esa)],[158]) ).
thf(29,axiom,
( ( xl != sz00 )
=> ( ( ( xn @ ( xm @ sdtpldt0 ) )
= ( xl @ ( xn @ sdtsldt0 ) @ ( xl @ ( xm @ sdtsldt0 ) @ sdtpldt0 ) @ ( xl @ sdtasdt0 ) ) )
& ( xn
= ( xl @ ( xn @ sdtsldt0 ) @ ( xl @ sdtasdt0 ) ) )
& ( xl @ ( xn @ sdtsldt0 ) @ aNaturalNumber0 )
& ( xm
= ( xl @ ( xm @ sdtsldt0 ) @ ( xl @ sdtasdt0 ) ) )
& ( xl @ ( xm @ sdtsldt0 ) @ aNaturalNumber0 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1298) ).
thf(168,plain,
( ( xl != sz00 )
=> ( ( ( xn @ ( xm @ sdtpldt0 ) )
= ( xl @ ( xn @ sdtsldt0 ) @ ( xl @ ( xm @ sdtsldt0 ) @ sdtpldt0 ) @ ( xl @ sdtasdt0 ) ) )
& ( xn
= ( xl @ ( xn @ sdtsldt0 ) @ ( xl @ sdtasdt0 ) ) )
& ( xl @ ( xn @ sdtsldt0 ) @ aNaturalNumber0 )
& ( xm
= ( xl @ ( xm @ sdtsldt0 ) @ ( xl @ sdtasdt0 ) ) )
& ( xl @ ( xm @ sdtsldt0 ) @ aNaturalNumber0 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(169,plain,
( ( ( ( xn @ ( xm @ sdtpldt0 ) )
= ( xl @ ( xn @ sdtsldt0 ) @ ( xl @ ( xm @ sdtsldt0 ) @ sdtpldt0 ) @ ( xl @ sdtasdt0 ) ) )
| ( xl = sz00 ) )
& ( ( xn
= ( xl @ ( xn @ sdtsldt0 ) @ ( xl @ sdtasdt0 ) ) )
| ( xl = sz00 ) )
& ( ( xl @ ( xn @ sdtsldt0 ) @ aNaturalNumber0 )
| ( xl = sz00 ) )
& ( ( xm
= ( xl @ ( xm @ sdtsldt0 ) @ ( xl @ sdtasdt0 ) ) )
| ( xl = sz00 ) )
& ( ( xl @ ( xm @ sdtsldt0 ) @ aNaturalNumber0 )
| ( xl = sz00 ) ) ),
inference(cnf,[status(esa)],[168]) ).
thf(170,plain,
( ( ( xn @ ( xm @ sdtpldt0 ) )
= ( xl @ ( xn @ sdtsldt0 ) @ ( xl @ ( xm @ sdtsldt0 ) @ sdtpldt0 ) @ ( xl @ sdtasdt0 ) ) )
| ( xl = sz00 ) ),
inference(cnfConj,[status(thm)],[169]) ).
thf(175,plain,
( ( ( xl @ ( xn @ sdtsldt0 ) @ ( xl @ ( xm @ sdtsldt0 ) @ sdtpldt0 ) @ ( xl @ sdtasdt0 ) )
= ( xn @ ( xm @ sdtpldt0 ) ) )
| ( xl = sz00 ) ),
inference(lifteq,[status(thm)],[170]) ).
thf(35,axiom,
( ( xn @ ( xl @ doDivides0 ) )
& ? [A: $i] :
( ( xn
= ( A @ ( xl @ sdtasdt0 ) ) )
& ( A @ aNaturalNumber0 ) )
& ( xm @ ( xl @ doDivides0 ) )
& ? [A: $i] :
( ( xm
= ( A @ ( xl @ sdtasdt0 ) ) )
& ( A @ aNaturalNumber0 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1240_04) ).
thf(201,plain,
( ( xn @ ( xl @ doDivides0 ) )
& ? [A: $i] :
( ( xn
= ( A @ ( xl @ sdtasdt0 ) ) )
& ( A @ aNaturalNumber0 ) )
& ( xm @ ( xl @ doDivides0 ) )
& ? [A: $i] :
( ( xm
= ( A @ ( xl @ sdtasdt0 ) ) )
& ( A @ aNaturalNumber0 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(202,plain,
( ( xn @ ( xl @ doDivides0 ) )
& ( xn
= ( sk4 @ ( xl @ sdtasdt0 ) ) )
& ( sk4 @ aNaturalNumber0 )
& ( xm @ ( xl @ doDivides0 ) )
& ( xm
= ( sk3 @ ( xl @ sdtasdt0 ) ) )
& ( sk3 @ aNaturalNumber0 ) ),
inference(cnf,[status(esa)],[201]) ).
thf(207,plain,
sk4 @ aNaturalNumber0,
inference(cnfConj,[status(thm)],[202]) ).
thf(3,axiom,
! [A: $i] :
( ( A @ aNaturalNumber0 )
=> ( ( sz00
= ( A @ ( sz00 @ sdtasdt0 ) ) )
& ( ( sz00 @ ( A @ sdtasdt0 ) )
= sz00 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_MulZero) ).
thf(43,plain,
! [A: $i] :
( ( A @ aNaturalNumber0 )
=> ( ( sz00
= ( A @ ( sz00 @ sdtasdt0 ) ) )
& ( ( sz00 @ ( A @ sdtasdt0 ) )
= sz00 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(44,plain,
! [A: $i] :
( ( ( sz00
= ( A @ ( sz00 @ sdtasdt0 ) ) )
| ~ ( A @ aNaturalNumber0 ) )
& ( ( ( sz00 @ ( A @ sdtasdt0 ) )
= sz00 )
| ~ ( A @ aNaturalNumber0 ) ) ),
inference(cnf,[status(esa)],[43]) ).
thf(46,plain,
! [A: $i] :
( ( sz00
= ( A @ ( sz00 @ sdtasdt0 ) ) )
| ~ ( A @ aNaturalNumber0 ) ),
inference(cnfConj,[status(thm)],[44]) ).
thf(48,plain,
! [A: $i] :
( ~ ( A @ aNaturalNumber0 )
| ( ( A @ ( sz00 @ sdtasdt0 ) )
= sz00 ) ),
inference(lifteq,[status(thm)],[46]) ).
thf(319,plain,
! [A: $i] :
( ( ( sk4 @ aNaturalNumber0 )
!= ( A @ aNaturalNumber0 ) )
| ~ $true
| ( ( A @ ( sz00 @ sdtasdt0 ) )
= sz00 ) ),
inference(paramod_ordered,[status(thm)],[207,48]) ).
thf(320,plain,
! [A: $i] :
( ( ( sk4 @ aNaturalNumber0 )
!= ( A @ aNaturalNumber0 ) )
| ( ( A @ ( sz00 @ sdtasdt0 ) )
= sz00 ) ),
inference(simp,[status(thm)],[319]) ).
thf(321,plain,
( ( sk4 @ ( sz00 @ sdtasdt0 ) )
= sz00 ),
inference(pattern_uni,[status(thm)],[320:[bind(A,$thf( sk4 ))]]) ).
thf(204,plain,
( xn
= ( sk4 @ ( xl @ sdtasdt0 ) ) ),
inference(cnfConj,[status(thm)],[202]) ).
thf(209,plain,
( ( sk4 @ ( xl @ sdtasdt0 ) )
= xn ),
inference(lifteq,[status(thm)],[204]) ).
thf(1993,plain,
( ( ( sk4 @ ( xl @ sdtasdt0 ) )
!= ( sk4 @ ( sz00 @ sdtasdt0 ) ) )
| ( xn = sz00 ) ),
inference(paramod_ordered,[status(thm)],[321,209]) ).
thf(2025,plain,
( ( sk4 != sk4 )
| ( xl != sz00 )
| ( xn = sz00 ) ),
inference(simp,[status(thm)],[1993]) ).
thf(2039,plain,
( ( xl != sz00 )
| ( xn = sz00 ) ),
inference(simp,[status(thm)],[2025]) ).
thf(31,axiom,
( ( xn @ aNaturalNumber0 )
& ( xm @ aNaturalNumber0 )
& ( xl @ aNaturalNumber0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1240) ).
thf(186,plain,
( ( xn @ aNaturalNumber0 )
& ( xm @ aNaturalNumber0 )
& ( xl @ aNaturalNumber0 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(187,plain,
( ( xn @ aNaturalNumber0 )
& ( xm @ aNaturalNumber0 )
& ( xl @ aNaturalNumber0 ) ),
inference(cnf,[status(esa)],[186]) ).
thf(189,plain,
xm @ aNaturalNumber0,
inference(cnfConj,[status(thm)],[187]) ).
thf(16,axiom,
! [A: $i] :
( ( A @ aNaturalNumber0 )
=> ( ( A
= ( A @ ( sz00 @ sdtpldt0 ) ) )
& ( ( sz00 @ ( A @ sdtpldt0 ) )
= A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_AddZero) ).
thf(115,plain,
! [A: $i] :
( ( A @ aNaturalNumber0 )
=> ( ( A
= ( A @ ( sz00 @ sdtpldt0 ) ) )
& ( ( sz00 @ ( A @ sdtpldt0 ) )
= A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(116,plain,
! [A: $i] :
( ( ( A
= ( A @ ( sz00 @ sdtpldt0 ) ) )
| ~ ( A @ aNaturalNumber0 ) )
& ( ( ( sz00 @ ( A @ sdtpldt0 ) )
= A )
| ~ ( A @ aNaturalNumber0 ) ) ),
inference(cnf,[status(esa)],[115]) ).
thf(117,plain,
! [A: $i] :
( ( ( sz00 @ ( A @ sdtpldt0 ) )
= A )
| ~ ( A @ aNaturalNumber0 ) ),
inference(cnfConj,[status(thm)],[116]) ).
thf(119,plain,
! [A: $i] :
( ~ ( A @ aNaturalNumber0 )
| ( ( sz00 @ ( A @ sdtpldt0 ) )
= A ) ),
inference(lifteq,[status(thm)],[117]) ).
thf(20166,plain,
! [A: $i] :
( ( ( xm @ aNaturalNumber0 )
!= ( A @ aNaturalNumber0 ) )
| ~ $true
| ( ( sz00 @ ( A @ sdtpldt0 ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[189,119]) ).
thf(20167,plain,
! [A: $i] :
( ( ( xm @ aNaturalNumber0 )
!= ( A @ aNaturalNumber0 ) )
| ( ( sz00 @ ( A @ sdtpldt0 ) )
= A ) ),
inference(simp,[status(thm)],[20166]) ).
thf(20168,plain,
( ( sz00 @ ( xm @ sdtpldt0 ) )
= xm ),
inference(pattern_uni,[status(thm)],[20167:[bind(A,$thf( xm ))]]) ).
thf(205,plain,
xm @ ( xl @ doDivides0 ),
inference(cnfConj,[status(thm)],[202]) ).
thf(1,conjecture,
( ( xn @ ( xm @ sdtpldt0 ) @ ( xl @ doDivides0 ) )
| ? [A: $i] :
( ( ( xn @ ( xm @ sdtpldt0 ) )
= ( A @ ( xl @ sdtasdt0 ) ) )
& ( A @ aNaturalNumber0 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
thf(2,negated_conjecture,
~ ( ( xn @ ( xm @ sdtpldt0 ) @ ( xl @ doDivides0 ) )
| ? [A: $i] :
( ( ( xn @ ( xm @ sdtpldt0 ) )
= ( A @ ( xl @ sdtasdt0 ) ) )
& ( A @ aNaturalNumber0 ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(38,plain,
~ ( ( xn @ ( xm @ sdtpldt0 ) @ ( xl @ doDivides0 ) )
| ? [A: $i] :
( ( ( xn @ ( xm @ sdtpldt0 ) )
= ( A @ ( xl @ sdtasdt0 ) ) )
& ( A @ aNaturalNumber0 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(39,plain,
! [A: $i] :
( ~ ( xn @ ( xm @ sdtpldt0 ) @ ( xl @ doDivides0 ) )
& ( ( ( xn @ ( xm @ sdtpldt0 ) )
!= ( A @ ( xl @ sdtasdt0 ) ) )
| ~ ( A @ aNaturalNumber0 ) ) ),
inference(cnf,[status(esa)],[38]) ).
thf(41,plain,
~ ( xn @ ( xm @ sdtpldt0 ) @ ( xl @ doDivides0 ) ),
inference(cnfConj,[status(thm)],[39]) ).
thf(283,plain,
( ( ( xn @ ( xm @ sdtpldt0 ) @ ( xl @ doDivides0 ) )
!= ( xm @ ( xl @ doDivides0 ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[205,41]) ).
thf(284,plain,
( ( xn @ ( xm @ sdtpldt0 ) @ ( xl @ doDivides0 ) )
!= ( xm @ ( xl @ doDivides0 ) ) ),
inference(simp,[status(thm)],[283]) ).
thf(285,plain,
( ( ( xn @ ( xm @ sdtpldt0 ) )
!= xm )
| ( xl != xl ) ),
inference(simp,[status(thm)],[284]) ).
thf(286,plain,
( ( xn @ ( xm @ sdtpldt0 ) )
!= xm ),
inference(simp,[status(thm)],[285]) ).
thf(20816,plain,
( ( ( xn @ ( xm @ sdtpldt0 ) )
!= ( sz00 @ ( xm @ sdtpldt0 ) ) )
| ( xm != xm ) ),
inference(paramod_ordered,[status(thm)],[20168,286]) ).
thf(20817,plain,
( ( xn @ ( xm @ sdtpldt0 ) )
!= ( sz00 @ ( xm @ sdtpldt0 ) ) ),
inference(simp,[status(thm)],[20816]) ).
thf(20877,plain,
( ( xn != sz00 )
| ( xm != xm ) ),
inference(simp,[status(thm)],[20817]) ).
thf(20891,plain,
xn != sz00,
inference(simp,[status(thm)],[20877]) ).
thf(20926,plain,
xl != sz00,
inference(simplifyReflect,[status(thm)],[2039,20891]) ).
thf(34567,plain,
( ( xl @ ( xn @ sdtsldt0 ) @ ( xl @ ( xm @ sdtsldt0 ) @ sdtpldt0 ) @ ( xl @ sdtasdt0 ) )
= ( xn @ ( xm @ sdtpldt0 ) ) ),
inference(simplifyReflect,[status(thm)],[175,20926]) ).
thf(40,plain,
! [A: $i] :
( ( ( xn @ ( xm @ sdtpldt0 ) )
!= ( A @ ( xl @ sdtasdt0 ) ) )
| ~ ( A @ aNaturalNumber0 ) ),
inference(cnfConj,[status(thm)],[39]) ).
thf(42,plain,
! [A: $i] :
( ~ ( A @ aNaturalNumber0 )
| ( ( A @ ( xl @ sdtasdt0 ) )
!= ( xn @ ( xm @ sdtpldt0 ) ) ) ),
inference(lifteq,[status(thm)],[40]) ).
thf(34618,plain,
! [A: $i] :
( ( ( xl @ ( xn @ sdtsldt0 ) @ ( xl @ ( xm @ sdtsldt0 ) @ sdtpldt0 ) @ ( xl @ sdtasdt0 ) )
!= ( A @ ( xl @ sdtasdt0 ) ) )
| ~ ( A @ aNaturalNumber0 )
| ( ( xn @ ( xm @ sdtpldt0 ) )
!= ( xn @ ( xm @ sdtpldt0 ) ) ) ),
inference(paramod_ordered,[status(thm)],[34567,42]) ).
thf(34619,plain,
! [A: $i] :
( ( ( xl @ ( xn @ sdtsldt0 ) @ ( xl @ ( xm @ sdtsldt0 ) @ sdtpldt0 ) @ ( xl @ sdtasdt0 ) )
!= ( A @ ( xl @ sdtasdt0 ) ) )
| ~ ( A @ aNaturalNumber0 ) ),
inference(simp,[status(thm)],[34618]) ).
thf(34620,plain,
~ ( xl @ ( xn @ sdtsldt0 ) @ ( xl @ ( xm @ sdtsldt0 ) @ sdtpldt0 ) @ aNaturalNumber0 ),
inference(pattern_uni,[status(thm)],[34619:[bind(A,$thf( xl @ ( xn @ sdtsldt0 ) @ ( xl @ ( xm @ sdtsldt0 ) @ sdtpldt0 ) ))]]) ).
thf(36905,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ sdtpldt0 ) @ aNaturalNumber0 )
!= ( xl @ ( xn @ sdtsldt0 ) @ ( xl @ ( xm @ sdtsldt0 ) @ sdtpldt0 ) @ aNaturalNumber0 ) )
| ~ $true
| ~ ( B @ aNaturalNumber0 )
| ~ ( A @ aNaturalNumber0 ) ),
inference(paramod_ordered,[status(thm)],[159,34620]) ).
thf(36906,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ sdtpldt0 ) @ aNaturalNumber0 )
!= ( xl @ ( xn @ sdtsldt0 ) @ ( xl @ ( xm @ sdtsldt0 ) @ sdtpldt0 ) @ aNaturalNumber0 ) )
| ~ ( B @ aNaturalNumber0 )
| ~ ( A @ aNaturalNumber0 ) ),
inference(simp,[status(thm)],[36905]) ).
thf(36907,plain,
( ~ ( xl @ ( xn @ sdtsldt0 ) @ aNaturalNumber0 )
| ~ ( xl @ ( xm @ sdtsldt0 ) @ aNaturalNumber0 ) ),
inference(pattern_uni,[status(thm)],[36906:[bind(A,$thf( xl @ ( xm @ sdtsldt0 ) )),bind(B,$thf( xl @ ( xn @ sdtsldt0 ) ))]]) ).
thf(172,plain,
( ( xl @ ( xn @ sdtsldt0 ) @ aNaturalNumber0 )
| ( xl = sz00 ) ),
inference(cnfConj,[status(thm)],[169]) ).
thf(178,plain,
( ( xl @ ( xn @ sdtsldt0 ) @ aNaturalNumber0 )
| ( xl = sz00 ) ),
inference(lifteq,[status(thm)],[172]) ).
thf(3166,plain,
( ( xl != xl )
| ( sz00 != sz00 )
| ( xn = sz00 )
| ( xl @ ( xn @ sdtsldt0 ) @ aNaturalNumber0 ) ),
inference(paramod_ordered,[status(thm)],[178,2039]) ).
thf(3167,plain,
( ( xl != xl )
| ( xn = sz00 )
| ( xl @ ( xn @ sdtsldt0 ) @ aNaturalNumber0 ) ),
inference(simp,[status(thm)],[3166]) ).
thf(3168,plain,
( ( xn = sz00 )
| ( xl @ ( xn @ sdtsldt0 ) @ aNaturalNumber0 ) ),
inference(pattern_uni,[status(thm)],[3167:[]]) ).
thf(4512,plain,
( ( xn != xn )
| ( ( sz00 @ ( xm @ sdtpldt0 ) )
!= xm )
| ( xl @ ( xn @ sdtsldt0 ) @ aNaturalNumber0 ) ),
inference(paramod_ordered,[status(thm)],[3168,286]) ).
thf(4513,plain,
( ( ( sz00 @ ( xm @ sdtpldt0 ) )
!= xm )
| ( xl @ ( xn @ sdtsldt0 ) @ aNaturalNumber0 ) ),
inference(pattern_uni,[status(thm)],[4512:[]]) ).
thf(20746,plain,
( ( xm != xm )
| ( xl @ ( xn @ sdtsldt0 ) @ aNaturalNumber0 ) ),
inference(rewrite,[status(thm)],[4513,20168]) ).
thf(20747,plain,
xl @ ( xn @ sdtsldt0 ) @ aNaturalNumber0,
inference(simp,[status(thm)],[20746]) ).
thf(173,plain,
( ( xl @ ( xm @ sdtsldt0 ) @ aNaturalNumber0 )
| ( xl = sz00 ) ),
inference(cnfConj,[status(thm)],[169]) ).
thf(177,plain,
( ( xl @ ( xm @ sdtsldt0 ) @ aNaturalNumber0 )
| ( xl = sz00 ) ),
inference(lifteq,[status(thm)],[173]) ).
thf(3155,plain,
( ( xl != xl )
| ( sz00 != sz00 )
| ( xn = sz00 )
| ( xl @ ( xm @ sdtsldt0 ) @ aNaturalNumber0 ) ),
inference(paramod_ordered,[status(thm)],[177,2039]) ).
thf(3156,plain,
( ( xl != xl )
| ( xn = sz00 )
| ( xl @ ( xm @ sdtsldt0 ) @ aNaturalNumber0 ) ),
inference(simp,[status(thm)],[3155]) ).
thf(3157,plain,
( ( xn = sz00 )
| ( xl @ ( xm @ sdtsldt0 ) @ aNaturalNumber0 ) ),
inference(pattern_uni,[status(thm)],[3156:[]]) ).
thf(4345,plain,
( ( xn != xn )
| ( ( sz00 @ ( xm @ sdtpldt0 ) )
!= xm )
| ( xl @ ( xm @ sdtsldt0 ) @ aNaturalNumber0 ) ),
inference(paramod_ordered,[status(thm)],[3157,286]) ).
thf(4346,plain,
( ( ( sz00 @ ( xm @ sdtpldt0 ) )
!= xm )
| ( xl @ ( xm @ sdtsldt0 ) @ aNaturalNumber0 ) ),
inference(pattern_uni,[status(thm)],[4345:[]]) ).
thf(20750,plain,
( ( xm != xm )
| ( xl @ ( xm @ sdtsldt0 ) @ aNaturalNumber0 ) ),
inference(rewrite,[status(thm)],[4346,20168]) ).
thf(20751,plain,
xl @ ( xm @ sdtsldt0 ) @ aNaturalNumber0,
inference(simp,[status(thm)],[20750]) ).
thf(102997,plain,
( ~ $true
| ~ $true ),
inference(rewrite,[status(thm)],[36907,20747,20751]) ).
thf(102998,plain,
$false,
inference(simp,[status(thm)],[102997]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM469+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.13 % 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.22/5.47 % Computer : n008.cluster.edu
% 0.22/5.47 % Model : x86_64 x86_64
% 0.22/5.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.22/5.47 % Memory : 8046.5625MB
% 0.22/5.47 % OS : Linux 6.8.0-71-generic
% 0.22/5.47 % CPULimit : 300
% 0.22/5.47 % WCLimit : 300
% 0.22/5.47 % DateTime : Sat Sep 26 02:53:32 UTC 2026
% 0.22/5.47 % CPUTime :
% 0.22/5.47 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.26/5.77 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 0.26/5.90 % [INFO] Parsing done (124ms).
% 0.26/5.90 % [INFO] Running in sequential loop mode.
% 1.55/6.10 % [INFO] eprover registered as external prover.
% 1.55/6.10 % [INFO] Scanning for conjecture ...
% 1.81/6.14 % [INFO] Definitions in FOF are currently treated as axioms.
% 1.81/6.15 % [INFO] Definitions in FOF are currently treated as axioms.
% 1.81/6.15 % [INFO] Definitions in FOF are currently treated as axioms.
% 1.81/6.16 % [INFO] Definitions in FOF are currently treated as axioms.
% 1.81/6.17 % [INFO] Found a conjecture (or negated_conjecture) and 35 axioms. Running axiom selection ...
% 1.99/6.22 % [INFO] Axiom selection finished. Selected 35 axioms (removed 0 axioms).
% 1.99/6.23 % [INFO] Definitions in FOF are currently treated as axioms.
% 1.99/6.24 % [INFO] Definitions in FOF are currently treated as axioms.
% 1.99/6.24 % [INFO] Definitions in FOF are currently treated as axioms.
% 1.99/6.25 % [INFO] Definitions in FOF are currently treated as axioms.
% 1.99/6.26 % [INFO] Problem is first-order (TPTP FOF).
% 1.99/6.27 % [INFO] Type checking passed.
% 1.99/6.27 % [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 ...
% 116.63/56.73 % [INFO] Killing All external provers ...
% 116.63/56.74 % Time passed: 51159ms (effective reasoning time: 50822ms)
% 116.63/56.74 % 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)>
% 116.63/56.74 % Axioms used in derivation (6): m__1240, m_MulZero, m__1298, m_AddZero, m__1240_04, mSortsB
% 116.63/56.74 % No. of inferences in proof: 81
% 116.63/56.74 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 51159 ms resp. 50822 ms w/o parsing
% 116.63/56.80 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 116.63/56.80 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------