%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : LAT382+3 : 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 : n010.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 07:47:37 AM UTC 2026
% Result : Theorem 28.09s 13.43s
% Output : Refutation 28.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 7
% Syntax : Number of formulae : 51 ( 17 unt; 0 typ; 2 def)
% Number of atoms : 210 ( 23 equ; 0 cnn)
% Maximal formula atoms : 28 ( 4 avg)
% Number of connectives : 554 ( 78 ~; 70 |; 45 &; 339 @)
% ( 0 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 6 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 15 ( 12 usr; 6 con; 0-3 aty)
% Number of variables : 53 ( 2 ^; 49 !; 0 ?; 53 :)
% ( 0 !>; 0 ?*; 0 @-; 2 @+)
% Comments :
%------------------------------------------------------------------------------
thf(aSet0_decl,type,
aSet0: $i > $o ).
thf(aElementOf0_decl,type,
aElementOf0: $i > $i > $o ).
thf(aLowerBoundOfIn0_decl,type,
aLowerBoundOfIn0: $i > $i > $i > $o ).
thf(sdtlseqdt0_decl,type,
sdtlseqdt0: $i > $i > $o ).
thf(aInfimumOfIn0_decl,type,
aInfimumOfIn0: $i > $i > $i > $o ).
thf(xu_decl,type,
xu: $i ).
thf(xv_decl,type,
xv: $i ).
thf(aElement0_decl,type,
aElement0: $i > $o ).
thf(xS_decl,type,
xS: $i ).
thf(xT_decl,type,
xT: $i ).
thf(sk7_decl,type,
sk7: $i > $i ).
thf(sk8_decl,type,
sk8: $i > $i ).
thf(sk7_def,definition,
( sk7
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( xS @ ( B @ aElementOf0 ) )
=> ( B @ ( A @ sdtlseqdt0 ) ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( ^ [A: $i] :
@+[B: $i] :
~ ( ( xS @ ( B @ aElementOf0 ) )
=> ( B @ ( A @ sdtlseqdt0 ) ) ) ) ) ).
thf(19,axiom,
( ( xT @ ( xS @ ( xv @ aInfimumOfIn0 ) ) )
& ! [A: $i] :
( ( ( xT @ ( xS @ ( A @ aLowerBoundOfIn0 ) ) )
| ( ! [B: $i] :
( ( xS @ ( B @ aElementOf0 ) )
=> ( B @ ( A @ sdtlseqdt0 ) ) )
& ( xT @ ( A @ aElementOf0 ) ) ) )
=> ( xv @ ( A @ sdtlseqdt0 ) ) )
& ( xT @ ( xS @ ( xv @ aLowerBoundOfIn0 ) ) )
& ! [A: $i] :
( ( xS @ ( A @ aElementOf0 ) )
=> ( A @ ( xv @ sdtlseqdt0 ) ) )
& ( xT @ ( xv @ aElementOf0 ) )
& ( xT @ ( xv @ aElementOf0 ) )
& ( xT @ ( xS @ ( xu @ aInfimumOfIn0 ) ) )
& ! [A: $i] :
( ( ( xT @ ( xS @ ( A @ aLowerBoundOfIn0 ) ) )
| ( ! [B: $i] :
( ( xS @ ( B @ aElementOf0 ) )
=> ( B @ ( A @ sdtlseqdt0 ) ) )
& ( xT @ ( A @ aElementOf0 ) ) ) )
=> ( xu @ ( A @ sdtlseqdt0 ) ) )
& ( xT @ ( xS @ ( xu @ aLowerBoundOfIn0 ) ) )
& ! [A: $i] :
( ( xS @ ( A @ aElementOf0 ) )
=> ( A @ ( xu @ sdtlseqdt0 ) ) )
& ( xT @ ( xu @ aElementOf0 ) )
& ( xT @ ( xu @ aElementOf0 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__792) ).
thf(94,plain,
( ( xT @ ( xS @ ( xv @ aInfimumOfIn0 ) ) )
& ! [A: $i] :
( ( ( xT @ ( xS @ ( A @ aLowerBoundOfIn0 ) ) )
| ( ! [B: $i] :
( ( xS @ ( B @ aElementOf0 ) )
=> ( B @ ( A @ sdtlseqdt0 ) ) )
& ( xT @ ( A @ aElementOf0 ) ) ) )
=> ( xv @ ( A @ sdtlseqdt0 ) ) )
& ( xT @ ( xS @ ( xv @ aLowerBoundOfIn0 ) ) )
& ! [A: $i] :
( ( xS @ ( A @ aElementOf0 ) )
=> ( A @ ( xv @ sdtlseqdt0 ) ) )
& ( xT @ ( xv @ aElementOf0 ) )
& ( xT @ ( xv @ aElementOf0 ) )
& ( xT @ ( xS @ ( xu @ aInfimumOfIn0 ) ) )
& ! [A: $i] :
( ( ( xT @ ( xS @ ( A @ aLowerBoundOfIn0 ) ) )
| ( ! [B: $i] :
( ( xS @ ( B @ aElementOf0 ) )
=> ( B @ ( A @ sdtlseqdt0 ) ) )
& ( xT @ ( A @ aElementOf0 ) ) ) )
=> ( xu @ ( A @ sdtlseqdt0 ) ) )
& ( xT @ ( xS @ ( xu @ aLowerBoundOfIn0 ) ) )
& ! [A: $i] :
( ( xS @ ( A @ aElementOf0 ) )
=> ( A @ ( xu @ sdtlseqdt0 ) ) )
& ( xT @ ( xu @ aElementOf0 ) )
& ( xT @ ( xu @ aElementOf0 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(95,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( xT @ ( xS @ ( xv @ aInfimumOfIn0 ) ) )
& ( ( xv @ ( D @ sdtlseqdt0 ) )
| ~ ( xT @ ( xS @ ( D @ aLowerBoundOfIn0 ) ) ) )
& ( ( xv @ ( D @ sdtlseqdt0 ) )
| ~ ( D @ sk8 @ ( D @ sdtlseqdt0 ) )
| ~ ( xT @ ( D @ aElementOf0 ) ) )
& ( ( xv @ ( D @ sdtlseqdt0 ) )
| ( xS @ ( D @ sk8 @ aElementOf0 ) )
| ~ ( xT @ ( D @ aElementOf0 ) ) )
& ( xT @ ( xS @ ( xv @ aLowerBoundOfIn0 ) ) )
& ( ( C @ ( xv @ sdtlseqdt0 ) )
| ~ ( xS @ ( C @ aElementOf0 ) ) )
& ( xT @ ( xv @ aElementOf0 ) )
& ( xT @ ( xv @ aElementOf0 ) )
& ( xT @ ( xS @ ( xu @ aInfimumOfIn0 ) ) )
& ( ( xu @ ( B @ sdtlseqdt0 ) )
| ~ ( xT @ ( xS @ ( B @ aLowerBoundOfIn0 ) ) ) )
& ( ( xu @ ( B @ sdtlseqdt0 ) )
| ~ ( B @ sk7 @ ( B @ sdtlseqdt0 ) )
| ~ ( xT @ ( B @ aElementOf0 ) ) )
& ( ( xu @ ( B @ sdtlseqdt0 ) )
| ( xS @ ( B @ sk7 @ aElementOf0 ) )
| ~ ( xT @ ( B @ aElementOf0 ) ) )
& ( xT @ ( xS @ ( xu @ aLowerBoundOfIn0 ) ) )
& ( ( A @ ( xu @ sdtlseqdt0 ) )
| ~ ( xS @ ( A @ aElementOf0 ) ) )
& ( xT @ ( xu @ aElementOf0 ) )
& ( xT @ ( xu @ aElementOf0 ) ) ),
inference(cnf,[status(esa)],[94]) ).
thf(107,plain,
xT @ ( xu @ aElementOf0 ),
inference(cnfConj,[status(thm)],[95]) ).
thf(14,axiom,
! [A: $i] :
( ( A @ aSet0 )
=> ! [B: $i] :
( ( A @ ( B @ aElementOf0 ) )
=> ( B @ aElement0 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mEOfElem) ).
thf(78,plain,
! [A: $i] :
( ( A @ aSet0 )
=> ! [B: $i] :
( ( A @ ( B @ aElementOf0 ) )
=> ( B @ aElement0 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(79,plain,
! [B: $i,A: $i] :
( ( B @ aElement0 )
| ~ ( A @ ( B @ aElementOf0 ) )
| ~ ( A @ aSet0 ) ),
inference(cnf,[status(esa)],[78]) ).
thf(6584,plain,
! [B: $i,A: $i] :
( ( ( xT @ ( xu @ aElementOf0 ) )
!= ( A @ ( B @ aElementOf0 ) ) )
| ( B @ aElement0 )
| ~ $true
| ~ ( A @ aSet0 ) ),
inference(paramod_ordered,[status(thm)],[107,79]) ).
thf(6585,plain,
! [B: $i,A: $i] :
( ( ( xT @ ( xu @ aElementOf0 ) )
!= ( A @ ( B @ aElementOf0 ) ) )
| ( B @ aElement0 )
| ~ ( A @ aSet0 ) ),
inference(simp,[status(thm)],[6584]) ).
thf(6586,plain,
( ( xu @ aElement0 )
| ~ ( xT @ aSet0 ) ),
inference(pattern_uni,[status(thm)],[6585:[bind(A,$thf( xT )),bind(B,$thf( xu ))]]) ).
thf(16,axiom,
xT @ aSet0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__773) ).
thf(82,plain,
xT @ aSet0,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(12,axiom,
! [A: $i,B: $i] :
( ( ( B @ aElement0 )
& ( A @ aElement0 ) )
=> ( ( ( A @ ( B @ sdtlseqdt0 ) )
& ( B @ ( A @ sdtlseqdt0 ) ) )
=> ( A = B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mASymm) ).
thf(66,plain,
! [A: $i,B: $i] :
( ( ( B @ aElement0 )
& ( A @ aElement0 ) )
=> ( ( ( A @ ( B @ sdtlseqdt0 ) )
& ( B @ ( A @ sdtlseqdt0 ) ) )
=> ( A = B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(67,plain,
! [B: $i,A: $i] :
( ( A = B )
| ~ ( A @ ( B @ sdtlseqdt0 ) )
| ~ ( B @ ( A @ sdtlseqdt0 ) )
| ~ ( B @ aElement0 )
| ~ ( A @ aElement0 ) ),
inference(cnf,[status(esa)],[66]) ).
thf(68,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ sdtlseqdt0 ) )
| ~ ( B @ ( A @ sdtlseqdt0 ) )
| ~ ( B @ aElement0 )
| ~ ( A @ aElement0 )
| ( A = B ) ),
inference(lifteq,[status(thm)],[67]) ).
thf(1,conjecture,
xu = xv,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
thf(2,negated_conjecture,
xu != xv,
inference(neg_conjecture,[status(cth)],[1]) ).
thf(20,plain,
xu != xv,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(21,plain,
xv != xu,
inference(lifteq,[status(thm)],[20]) ).
thf(3795,plain,
! [B: $i,A: $i] :
( ( A != xv )
| ( B != xu )
| ~ ( A @ ( B @ sdtlseqdt0 ) )
| ~ ( B @ ( A @ sdtlseqdt0 ) )
| ~ ( B @ aElement0 )
| ~ ( A @ aElement0 ) ),
inference(paramod_ordered,[status(thm)],[68,21]) ).
thf(3796,plain,
! [A: $i] :
( ( A != xu )
| ~ ( xv @ ( A @ sdtlseqdt0 ) )
| ~ ( A @ ( xv @ sdtlseqdt0 ) )
| ~ ( A @ aElement0 )
| ~ ( xv @ aElement0 ) ),
inference(pattern_uni,[status(thm)],[3795:[bind(A,$thf( xv ))]]) ).
thf(4931,plain,
( ~ ( xv @ ( xu @ sdtlseqdt0 ) )
| ~ ( xu @ ( xv @ sdtlseqdt0 ) )
| ~ ( xu @ aElement0 )
| ~ ( xv @ aElement0 ) ),
inference(simp,[status(thm)],[3796]) ).
thf(106,plain,
xT @ ( xS @ ( xu @ aLowerBoundOfIn0 ) ),
inference(cnfConj,[status(thm)],[95]) ).
thf(100,plain,
! [A: $i] :
( ( xv @ ( A @ sdtlseqdt0 ) )
| ~ ( xT @ ( xS @ ( A @ aLowerBoundOfIn0 ) ) ) ),
inference(cnfConj,[status(thm)],[95]) ).
thf(112,plain,
! [A: $i] :
( ( xv @ ( A @ sdtlseqdt0 ) )
| ~ ( xT @ ( xS @ ( A @ aLowerBoundOfIn0 ) ) ) ),
inference(simp,[status(thm)],[100]) ).
thf(1233,plain,
! [A: $i] :
( ( ( xT @ ( xS @ ( xu @ aLowerBoundOfIn0 ) ) )
!= ( xT @ ( xS @ ( A @ aLowerBoundOfIn0 ) ) ) )
| ( xv @ ( A @ sdtlseqdt0 ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[106,112]) ).
thf(1234,plain,
! [A: $i] :
( ( ( xT @ ( xS @ ( xu @ aLowerBoundOfIn0 ) ) )
!= ( xT @ ( xS @ ( A @ aLowerBoundOfIn0 ) ) ) )
| ( xv @ ( A @ sdtlseqdt0 ) ) ),
inference(simp,[status(thm)],[1233]) ).
thf(1235,plain,
xv @ ( xu @ sdtlseqdt0 ),
inference(pattern_uni,[status(thm)],[1234:[bind(A,$thf( xu ))]]) ).
thf(104,plain,
xT @ ( xS @ ( xv @ aLowerBoundOfIn0 ) ),
inference(cnfConj,[status(thm)],[95]) ).
thf(102,plain,
! [A: $i] :
( ( xu @ ( A @ sdtlseqdt0 ) )
| ~ ( xT @ ( xS @ ( A @ aLowerBoundOfIn0 ) ) ) ),
inference(cnfConj,[status(thm)],[95]) ).
thf(110,plain,
! [A: $i] :
( ( xu @ ( A @ sdtlseqdt0 ) )
| ~ ( xT @ ( xS @ ( A @ aLowerBoundOfIn0 ) ) ) ),
inference(simp,[status(thm)],[102]) ).
thf(1035,plain,
! [A: $i] :
( ( ( xT @ ( xS @ ( xv @ aLowerBoundOfIn0 ) ) )
!= ( xT @ ( xS @ ( A @ aLowerBoundOfIn0 ) ) ) )
| ( xu @ ( A @ sdtlseqdt0 ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[104,110]) ).
thf(1036,plain,
! [A: $i] :
( ( ( xT @ ( xS @ ( xv @ aLowerBoundOfIn0 ) ) )
!= ( xT @ ( xS @ ( A @ aLowerBoundOfIn0 ) ) ) )
| ( xu @ ( A @ sdtlseqdt0 ) ) ),
inference(simp,[status(thm)],[1035]) ).
thf(1037,plain,
xu @ ( xv @ sdtlseqdt0 ),
inference(pattern_uni,[status(thm)],[1036:[bind(A,$thf( xv ))]]) ).
thf(5045,plain,
( ~ $true
| ~ $true
| ~ ( xu @ aElement0 )
| ~ ( xv @ aElement0 ) ),
inference(rewrite,[status(thm)],[4931,1235,1037]) ).
thf(5046,plain,
( ~ ( xu @ aElement0 )
| ~ ( xv @ aElement0 ) ),
inference(simp,[status(thm)],[5045]) ).
thf(5067,plain,
( ~ $true
| ( ( xv @ aElement0 )
!= ( xu @ aElement0 ) )
| ~ ( xu @ aElement0 ) ),
inference(eqfactor_ordered,[status(thm)],[5046]) ).
thf(5068,plain,
( ( ( xv @ aElement0 )
!= ( xu @ aElement0 ) )
| ~ ( xu @ aElement0 ) ),
inference(simp,[status(thm)],[5067]) ).
thf(105,plain,
xT @ ( xv @ aElementOf0 ),
inference(cnfConj,[status(thm)],[95]) ).
thf(6566,plain,
! [B: $i,A: $i] :
( ( ( xT @ ( xv @ aElementOf0 ) )
!= ( A @ ( B @ aElementOf0 ) ) )
| ( B @ aElement0 )
| ~ $true
| ~ ( A @ aSet0 ) ),
inference(paramod_ordered,[status(thm)],[105,79]) ).
thf(6567,plain,
! [B: $i,A: $i] :
( ( ( xT @ ( xv @ aElementOf0 ) )
!= ( A @ ( B @ aElementOf0 ) ) )
| ( B @ aElement0 )
| ~ ( A @ aSet0 ) ),
inference(simp,[status(thm)],[6566]) ).
thf(6568,plain,
( ( xv @ aElement0 )
| ~ ( xT @ aSet0 ) ),
inference(pattern_uni,[status(thm)],[6567:[bind(A,$thf( xT )),bind(B,$thf( xv ))]]) ).
thf(6598,plain,
( ( xv @ aElement0 )
| ~ $true ),
inference(rewrite,[status(thm)],[6568,82]) ).
thf(6599,plain,
xv @ aElement0,
inference(simp,[status(thm)],[6598]) ).
thf(6600,plain,
( ~ ( xu @ aElement0 )
| ~ ( xu @ aElement0 ) ),
inference(rewrite,[status(thm)],[5068,6599]) ).
thf(6601,plain,
~ ( xu @ aElement0 ),
inference(simp,[status(thm)],[6600]) ).
thf(6723,plain,
( $false
| ~ $true ),
inference(rewrite,[status(thm)],[6586,82,6601]) ).
thf(6724,plain,
$false,
inference(simp,[status(thm)],[6723]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT382+3 : 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.18/5.66 % Computer : n010.cluster.edu
% 0.18/5.66 % Model : x86_64 x86_64
% 0.18/5.66 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/5.66 % Memory : 8046.5625MB
% 0.18/5.66 % OS : Linux 6.8.0-71-generic
% 0.18/5.66 % CPULimit : 300
% 0.18/5.66 % WCLimit : 300
% 0.18/5.66 % DateTime : Fri Sep 25 21:38:23 UTC 2026
% 0.18/5.66 % CPUTime :
% 0.18/5.66 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/6.27 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.58/6.59 % [INFO] Parsing done (312ms).
% 1.84/6.61 % [INFO] Running in sequential loop mode.
% 2.79/7.18 % [INFO] eprover registered as external prover.
% 2.79/7.19 % [INFO] Scanning for conjecture ...
% 2.88/7.24 % [INFO] Definitions in FOF are currently treated as axioms.
% 2.88/7.25 % [INFO] Definitions in FOF are currently treated as axioms.
% 2.88/7.26 % [INFO] Definitions in FOF are currently treated as axioms.
% 2.88/7.27 % [INFO] Definitions in FOF are currently treated as axioms.
% 2.88/7.27 % [INFO] Definitions in FOF are currently treated as axioms.
% 2.88/7.28 % [INFO] Definitions in FOF are currently treated as axioms.
% 3.11/7.31 % [INFO] Found a conjecture (or negated_conjecture) and 17 axioms. Running axiom selection ...
% 3.11/7.38 % [INFO] Axiom selection finished. Selected 17 axioms (removed 0 axioms).
% 3.11/7.39 % [INFO] Definitions in FOF are currently treated as axioms.
% 3.11/7.40 % [INFO] Definitions in FOF are currently treated as axioms.
% 3.33/7.40 % [INFO] Definitions in FOF are currently treated as axioms.
% 3.33/7.40 % [INFO] Definitions in FOF are currently treated as axioms.
% 3.33/7.40 % [INFO] Definitions in FOF are currently treated as axioms.
% 3.33/7.41 % [INFO] Definitions in FOF are currently treated as axioms.
% 3.33/7.42 % [INFO] Problem is first-order (TPTP FOF).
% 3.33/7.43 % [INFO] Type checking passed.
% 3.33/7.43 % [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 ...
% 28.09/13.43 % [INFO] Killing All external provers ...
% 28.09/13.43 % Time passed: 7631ms (effective reasoning time: 6807ms)
% 28.09/13.43 % 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)>
% 28.09/13.43 % Axioms used in derivation (4): m__792, mEOfElem, m__773, mASymm
% 28.09/13.43 % No. of inferences in proof: 49
% 28.09/13.43 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 7631 ms resp. 6807 ms w/o parsing
% 28.09/13.49 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 28.09/13.49 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------