%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : LAT299+3 : TPTP v9.3.1. Released v3.4.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 : n012.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:05 AM UTC 2026
% Result : Theorem 259.00s 79.60s
% Output : Refutation 259.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 16
% Syntax : Number of formulae : 94 ( 52 unt; 0 typ; 4 def)
% Number of atoms : 225 ( 117 equ; 0 cnn)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 685 ( 69 ~; 40 |; 46 &; 501 @)
% ( 1 <=>; 28 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 4 ( 4 >; 0 *; 0 +; 0 <<)
% Number of symbols : 29 ( 26 usr; 6 con; 0-3 aty)
% Number of variables : 165 ( 0 ^; 159 !; 2 ?; 165 :)
% ( 0 !>; 0 ?*; 0 @-; 4 @+)
% Comments :
%------------------------------------------------------------------------------
thf(v3_struct_0_decl,type,
v3_struct_0: $i > $o ).
thf(v10_lattices_decl,type,
v10_lattices: $i > $o ).
thf(l3_lattices_decl,type,
l3_lattices: $i > $o ).
thf(g3_lattices_decl,type,
g3_lattices: $i > $i > $i > $i ).
thf(u1_struct_0_decl,type,
u1_struct_0: $i > $i ).
thf(u2_lattices_decl,type,
u2_lattices: $i > $i ).
thf(u1_lattices_decl,type,
u1_lattices: $i > $i ).
thf(m2_filter_2_decl,type,
m2_filter_2: $i > $i > $o ).
thf(v1_funct_1_decl,type,
v1_funct_1: $i > $o ).
thf(k1_xboole_0_decl,type,
k1_xboole_0: $i ).
thf(k2_funcop_1_decl,type,
k2_funcop_1: $i > $i > $i ).
thf(v1_relat_1_decl,type,
v1_relat_1: $i > $o ).
thf(k2_zfmisc_1_decl,type,
k2_zfmisc_1: $i > $i > $i ).
thf(k1_zfmisc_1_decl,type,
k1_zfmisc_1: $i > $i ).
thf(v1_xboole_0_decl,type,
v1_xboole_0: $i > $o ).
thf(v2_funct_1_decl,type,
v2_funct_1: $i > $o ).
thf(k1_tarski_decl,type,
k1_tarski: $i > $i ).
thf(r1_tarski_decl,type,
r1_tarski: $i > $i > $o ).
thf(v1_finset_1_decl,type,
v1_finset_1: $i > $o ).
thf(k4_xboole_0_decl,type,
k4_xboole_0: $i > $i > $i ).
thf(k3_tarski_decl,type,
k3_tarski: $i > $i ).
thf(k3_xboole_0_decl,type,
k3_xboole_0: $i > $i > $i ).
thf(sk1_decl,type,
sk1: $i ).
thf(sk2_decl,type,
sk2: $i ).
thf(sk3_decl,type,
sk3: $i ).
thf(sk25_decl,type,
sk25: $i > $i > $i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i] :
~ ( ( ( A @ l3_lattices )
& ( A @ v10_lattices )
& ~ ( A @ v3_struct_0 ) )
=> ! [B: $i] :
( ( ( B @ l3_lattices )
& ( B @ v10_lattices )
& ~ ( B @ v3_struct_0 ) )
=> ( ( ( A @ u1_lattices @ ( A @ u2_lattices @ ( A @ u1_struct_0 @ g3_lattices ) ) )
= ( B @ u1_lattices @ ( B @ u2_lattices @ ( B @ u1_struct_0 @ g3_lattices ) ) ) )
=> ! [C: $i] :
( ( A @ ( C @ m2_filter_2 ) )
=> ( B @ ( C @ m2_filter_2 ) ) ) ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: $i] :
~ ( ( ( A @ l3_lattices )
& ( A @ v10_lattices )
& ~ ( A @ v3_struct_0 ) )
=> ( ( ( sk1 @ u1_lattices @ ( sk1 @ u2_lattices @ ( sk1 @ u1_struct_0 @ g3_lattices ) ) )
= ( A @ u1_lattices @ ( A @ u2_lattices @ ( A @ u1_struct_0 @ g3_lattices ) ) ) )
=> ! [B: $i] :
( ( sk1 @ ( B @ m2_filter_2 ) )
=> ( A @ ( B @ m2_filter_2 ) ) ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: $i] :
~ ( ( sk1 @ ( A @ m2_filter_2 ) )
=> ( sk2 @ ( A @ m2_filter_2 ) ) ) ) ) ).
thf(sk25_def,definition,
( sk25
= ( @+[A: $i > $i > $i] :
! [B: $i,C: $i] :
( ( C @ ( B @ k4_xboole_0 ) @ ( C @ A ) )
= B ) ) ) ).
thf(150,axiom,
! [A: $i] : ( A @ k3_tarski @ k1_zfmisc_1 @ ( A @ r1_tarski ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t100_zfmisc_1) ).
thf(2026,plain,
! [A: $i] : ( A @ k3_tarski @ k1_zfmisc_1 @ ( A @ r1_tarski ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[150]) ).
thf(2027,plain,
! [A: $i] : ( A @ k3_tarski @ k1_zfmisc_1 @ ( A @ r1_tarski ) ),
inference(cnf,[status(esa)],[2026]) ).
thf(616,axiom,
! [A: $i,B: $i] :
( ( ( B @ ( A @ k2_zfmisc_1 ) )
= k1_xboole_0 )
<=> ( ( B = k1_xboole_0 )
| ( A = k1_xboole_0 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t113_zfmisc_1) ).
thf(4510,plain,
! [A: $i,B: $i] :
( ( ( ( B = k1_xboole_0 )
| ( A = k1_xboole_0 ) )
=> ( ( B @ ( A @ k2_zfmisc_1 ) )
= k1_xboole_0 ) )
& ( ( ( B @ ( A @ k2_zfmisc_1 ) )
= k1_xboole_0 )
=> ( ( B = k1_xboole_0 )
| ( A = k1_xboole_0 ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[616]) ).
thf(4511,plain,
( ! [A: $i,B: $i] :
( ( ( B = k1_xboole_0 )
| ( A = k1_xboole_0 ) )
=> ( ( B @ ( A @ k2_zfmisc_1 ) )
= k1_xboole_0 ) )
& ! [A: $i,B: $i] :
( ( ( B @ ( A @ k2_zfmisc_1 ) )
= k1_xboole_0 )
=> ( ( B = k1_xboole_0 )
| ( A = k1_xboole_0 ) ) ) ),
inference(miniscope,[status(thm)],[4510]) ).
thf(4512,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( ( D @ ( C @ k2_zfmisc_1 ) )
= k1_xboole_0 )
| ( D != k1_xboole_0 ) )
& ( ( ( D @ ( C @ k2_zfmisc_1 ) )
= k1_xboole_0 )
| ( C != k1_xboole_0 ) )
& ( ( B = k1_xboole_0 )
| ( A = k1_xboole_0 )
| ( ( B @ ( A @ k2_zfmisc_1 ) )
!= k1_xboole_0 ) ) ),
inference(cnf,[status(esa)],[4511]) ).
thf(4514,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ k2_zfmisc_1 ) )
= k1_xboole_0 )
| ( A != k1_xboole_0 ) ),
inference(cnfConj,[status(thm)],[4512]) ).
thf(4517,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ k2_zfmisc_1 ) )
= k1_xboole_0 )
| ( A != k1_xboole_0 ) ),
inference(lifteq,[status(thm)],[4514]) ).
thf(4518,plain,
! [A: $i] :
( ( A @ ( k1_xboole_0 @ k2_zfmisc_1 ) )
= k1_xboole_0 ),
inference(simp,[status(thm)],[4517]) ).
thf(13,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ k2_funcop_1 ) )
= ( B @ k1_tarski @ ( A @ k2_zfmisc_1 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_funcop_1) ).
thf(1377,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ k2_funcop_1 ) )
= ( B @ k1_tarski @ ( A @ k2_zfmisc_1 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(1378,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ k2_funcop_1 ) )
= ( B @ k1_tarski @ ( A @ k2_zfmisc_1 ) ) ),
inference(cnf,[status(esa)],[1377]) ).
thf(1379,plain,
! [B: $i,A: $i] :
( ( B @ k1_tarski @ ( A @ k2_zfmisc_1 ) )
= ( B @ ( A @ k2_funcop_1 ) ) ),
inference(lifteq,[status(thm)],[1378]) ).
thf(14037,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( k1_xboole_0 @ k2_zfmisc_1 ) )
!= ( C @ k1_tarski @ ( B @ k2_zfmisc_1 ) ) )
| ( ( C @ ( B @ k2_funcop_1 ) )
= k1_xboole_0 ) ),
inference(paramod_ordered,[status(thm)],[4518,1379]) ).
thf(14038,plain,
! [A: $i] :
( ( A @ ( k1_xboole_0 @ k2_funcop_1 ) )
= k1_xboole_0 ),
inference(pattern_uni,[status(thm)],[14037:[bind(A,$thf( D @ k1_tarski )),bind(B,$thf( k1_xboole_0 )),bind(C,$thf( D ))]]) ).
thf(14058,plain,
! [A: $i] :
( ( A @ ( k1_xboole_0 @ k2_funcop_1 ) )
= k1_xboole_0 ),
inference(simp,[status(thm)],[14038]) ).
thf(16,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ k2_funcop_1 ) @ ( B @ ( A @ k2_funcop_1 ) @ r1_tarski ) )
=> ( ( B = D )
| ( A = k1_xboole_0 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_funct_4) ).
thf(1390,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ k2_funcop_1 ) @ ( B @ ( A @ k2_funcop_1 ) @ r1_tarski ) )
=> ( ( B = D )
| ( A = k1_xboole_0 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(1391,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B = D )
| ( A = k1_xboole_0 )
| ~ ( D @ ( C @ k2_funcop_1 ) @ ( B @ ( A @ k2_funcop_1 ) @ r1_tarski ) ) ),
inference(cnf,[status(esa)],[1390]) ).
thf(1392,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( D @ ( C @ k2_funcop_1 ) @ ( B @ ( A @ k2_funcop_1 ) @ r1_tarski ) )
| ( B = D )
| ( A = k1_xboole_0 ) ),
inference(lifteq,[status(thm)],[1391]) ).
thf(1,conjecture,
! [A: $i] :
( ( ( A @ l3_lattices )
& ( A @ v10_lattices )
& ~ ( A @ v3_struct_0 ) )
=> ! [B: $i] :
( ( ( B @ l3_lattices )
& ( B @ v10_lattices )
& ~ ( B @ v3_struct_0 ) )
=> ( ( ( A @ u1_lattices @ ( A @ u2_lattices @ ( A @ u1_struct_0 @ g3_lattices ) ) )
= ( B @ u1_lattices @ ( B @ u2_lattices @ ( B @ u1_struct_0 @ g3_lattices ) ) ) )
=> ! [C: $i] :
( ( A @ ( C @ m2_filter_2 ) )
=> ( B @ ( C @ m2_filter_2 ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t17_filter_2) ).
thf(2,negated_conjecture,
~ ! [A: $i] :
( ( ( A @ l3_lattices )
& ( A @ v10_lattices )
& ~ ( A @ v3_struct_0 ) )
=> ! [B: $i] :
( ( ( B @ l3_lattices )
& ( B @ v10_lattices )
& ~ ( B @ v3_struct_0 ) )
=> ( ( ( A @ u1_lattices @ ( A @ u2_lattices @ ( A @ u1_struct_0 @ g3_lattices ) ) )
= ( B @ u1_lattices @ ( B @ u2_lattices @ ( B @ u1_struct_0 @ g3_lattices ) ) ) )
=> ! [C: $i] :
( ( A @ ( C @ m2_filter_2 ) )
=> ( B @ ( C @ m2_filter_2 ) ) ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(1312,plain,
~ ! [A: $i] :
( ( ( A @ l3_lattices )
& ( A @ v10_lattices )
& ~ ( A @ v3_struct_0 ) )
=> ! [B: $i] :
( ( ( B @ l3_lattices )
& ( B @ v10_lattices )
& ~ ( B @ v3_struct_0 ) )
=> ( ( ( A @ u1_lattices @ ( A @ u2_lattices @ ( A @ u1_struct_0 @ g3_lattices ) ) )
= ( B @ u1_lattices @ ( B @ u2_lattices @ ( B @ u1_struct_0 @ g3_lattices ) ) ) )
=> ! [C: $i] :
( ( A @ ( C @ m2_filter_2 ) )
=> ( B @ ( C @ m2_filter_2 ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(1313,plain,
( ~ ( sk2 @ ( sk3 @ m2_filter_2 ) )
& ( sk1 @ ( sk3 @ m2_filter_2 ) )
& ( ( sk1 @ u1_lattices @ ( sk1 @ u2_lattices @ ( sk1 @ u1_struct_0 @ g3_lattices ) ) )
= ( sk2 @ u1_lattices @ ( sk2 @ u2_lattices @ ( sk2 @ u1_struct_0 @ g3_lattices ) ) ) )
& ( sk2 @ l3_lattices )
& ( sk2 @ v10_lattices )
& ~ ( sk2 @ v3_struct_0 )
& ( sk1 @ l3_lattices )
& ( sk1 @ v10_lattices )
& ~ ( sk1 @ v3_struct_0 ) ),
inference(cnf,[status(esa)],[1312]) ).
thf(1320,plain,
sk1 @ ( sk3 @ m2_filter_2 ),
inference(cnfConj,[status(thm)],[1313]) ).
thf(1314,plain,
~ ( sk2 @ ( sk3 @ m2_filter_2 ) ),
inference(cnfConj,[status(thm)],[1313]) ).
thf(8015,plain,
( ( ( sk2 @ ( sk3 @ m2_filter_2 ) )
!= ( sk1 @ ( sk3 @ m2_filter_2 ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1320,1314]) ).
thf(8016,plain,
( ( sk2 @ ( sk3 @ m2_filter_2 ) )
!= ( sk1 @ ( sk3 @ m2_filter_2 ) ) ),
inference(simp,[status(thm)],[8015]) ).
thf(8017,plain,
( ( sk2 != sk1 )
| ( sk3 != sk3 ) ),
inference(simp,[status(thm)],[8016]) ).
thf(8018,plain,
sk2 != sk1,
inference(simp,[status(thm)],[8017]) ).
thf(15876,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B != sk2 )
| ( D != sk1 )
| ~ ( D @ ( C @ k2_funcop_1 ) @ ( B @ ( A @ k2_funcop_1 ) @ r1_tarski ) )
| ( A = k1_xboole_0 ) ),
inference(paramod_ordered,[status(thm)],[1392,8018]) ).
thf(15877,plain,
! [C: $i,B: $i,A: $i] :
( ( C != sk1 )
| ~ ( C @ ( B @ k2_funcop_1 ) @ ( sk2 @ ( A @ k2_funcop_1 ) @ r1_tarski ) )
| ( A = k1_xboole_0 ) ),
inference(pattern_uni,[status(thm)],[15876:[bind(A,$thf( A )),bind(B,$thf( sk2 ))]]) ).
thf(20257,plain,
! [B: $i,A: $i] :
( ~ ( sk1 @ ( B @ k2_funcop_1 ) @ ( sk2 @ ( A @ k2_funcop_1 ) @ r1_tarski ) )
| ( A = k1_xboole_0 ) ),
inference(simp,[status(thm)],[15877]) ).
thf(21961,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( k1_xboole_0 @ k2_funcop_1 ) )
!= ( sk1 @ ( C @ k2_funcop_1 ) ) )
| ~ ( k1_xboole_0 @ ( sk2 @ ( B @ k2_funcop_1 ) @ r1_tarski ) )
| ( B = k1_xboole_0 ) ),
inference(paramod_ordered,[status(thm)],[14058,20257]) ).
thf(21962,plain,
! [A: $i] :
( ~ ( k1_xboole_0 @ ( sk2 @ ( A @ k2_funcop_1 ) @ r1_tarski ) )
| ( A = k1_xboole_0 ) ),
inference(pattern_uni,[status(thm)],[21961:[bind(A,$thf( sk1 )),bind(B,$thf( B )),bind(C,$thf( k1_xboole_0 ))]]) ).
thf(22551,plain,
! [A: $i] :
( ~ ( k1_xboole_0 @ ( sk2 @ ( A @ k2_funcop_1 ) @ r1_tarski ) )
| ( A = k1_xboole_0 ) ),
inference(simp,[status(thm)],[21962]) ).
thf(11,axiom,
! [A: $i] :
( ( A @ ( k1_xboole_0 @ k2_funcop_1 ) @ v2_funct_1 )
& ( A @ ( k1_xboole_0 @ k2_funcop_1 ) @ v1_funct_1 )
& ( A @ ( k1_xboole_0 @ k2_funcop_1 ) @ v1_relat_1 )
& ( A @ ( k1_xboole_0 @ k2_funcop_1 ) @ v1_xboole_0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_funcop_1) ).
thf(1365,plain,
! [A: $i] :
( ( A @ ( k1_xboole_0 @ k2_funcop_1 ) @ v2_funct_1 )
& ( A @ ( k1_xboole_0 @ k2_funcop_1 ) @ v1_funct_1 )
& ( A @ ( k1_xboole_0 @ k2_funcop_1 ) @ v1_relat_1 )
& ( A @ ( k1_xboole_0 @ k2_funcop_1 ) @ v1_xboole_0 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(1366,plain,
( ! [A: $i] : ( A @ ( k1_xboole_0 @ k2_funcop_1 ) @ v2_funct_1 )
& ! [A: $i] : ( A @ ( k1_xboole_0 @ k2_funcop_1 ) @ v1_funct_1 )
& ! [A: $i] : ( A @ ( k1_xboole_0 @ k2_funcop_1 ) @ v1_relat_1 )
& ! [A: $i] : ( A @ ( k1_xboole_0 @ k2_funcop_1 ) @ v1_xboole_0 ) ),
inference(miniscope,[status(thm)],[1365]) ).
thf(1367,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( k1_xboole_0 @ k2_funcop_1 ) @ v2_funct_1 )
& ( C @ ( k1_xboole_0 @ k2_funcop_1 ) @ v1_funct_1 )
& ( B @ ( k1_xboole_0 @ k2_funcop_1 ) @ v1_relat_1 )
& ( A @ ( k1_xboole_0 @ k2_funcop_1 ) @ v1_xboole_0 ) ),
inference(cnf,[status(esa)],[1366]) ).
thf(1368,plain,
! [A: $i] : ( A @ ( k1_xboole_0 @ k2_funcop_1 ) @ v1_xboole_0 ),
inference(cnfConj,[status(thm)],[1367]) ).
thf(531,axiom,
! [A: $i] :
( ( A @ k1_tarski @ v1_finset_1 )
& ~ ( A @ k1_tarski @ v1_xboole_0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_finset_1) ).
thf(4046,plain,
! [A: $i] :
( ( A @ k1_tarski @ v1_finset_1 )
& ~ ( A @ k1_tarski @ v1_xboole_0 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[531]) ).
thf(4047,plain,
( ! [A: $i] : ( A @ k1_tarski @ v1_finset_1 )
& ~ ? [A: $i] : ( A @ k1_tarski @ v1_xboole_0 ) ),
inference(miniscope,[status(thm)],[4046]) ).
thf(4048,plain,
! [B: $i,A: $i] :
( ( B @ k1_tarski @ v1_finset_1 )
& ~ ( A @ k1_tarski @ v1_xboole_0 ) ),
inference(cnf,[status(esa)],[4047]) ).
thf(4049,plain,
! [A: $i] :
~ ( A @ k1_tarski @ v1_xboole_0 ),
inference(cnfConj,[status(thm)],[4048]) ).
thf(12439,plain,
! [B: $i,A: $i] :
( ( ( A @ ( k1_xboole_0 @ k2_funcop_1 ) @ v1_xboole_0 )
!= ( B @ k1_tarski @ v1_xboole_0 ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1368,4049]) ).
thf(12440,plain,
! [B: $i,A: $i] :
( ( A @ ( k1_xboole_0 @ k2_funcop_1 ) @ v1_xboole_0 )
!= ( B @ k1_tarski @ v1_xboole_0 ) ),
inference(simp,[status(thm)],[12439]) ).
thf(12460,plain,
! [B: $i,A: $i] :
( ( A @ ( k1_xboole_0 @ k2_funcop_1 ) )
!= ( B @ k1_tarski ) ),
inference(simp,[status(thm)],[12440]) ).
thf(35535,plain,
! [A: $i] :
( ( A @ k1_tarski )
!= k1_xboole_0 ),
inference(rewrite,[status(thm)],[12460,14058]) ).
thf(69705,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ k1_tarski ) )
| ( k1_xboole_0 != k1_xboole_0 )
| ~ ( k1_xboole_0 @ ( sk2 @ ( A @ k2_funcop_1 ) @ r1_tarski ) ) ),
inference(paramod_ordered,[status(thm)],[22551,35535]) ).
thf(69706,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ k1_tarski ) )
| ~ ( k1_xboole_0 @ ( sk2 @ ( A @ k2_funcop_1 ) @ r1_tarski ) ) ),
inference(simp,[status(thm)],[69705]) ).
thf(69707,plain,
! [A: $i] :
~ ( k1_xboole_0 @ ( sk2 @ ( A @ k1_tarski @ k2_funcop_1 ) @ r1_tarski ) ),
inference(pattern_uni,[status(thm)],[69706:[bind(A,$thf( C @ k1_tarski )),bind(B,$thf( C ))]]) ).
thf(70680,plain,
! [A: $i] :
~ ( k1_xboole_0 @ ( sk2 @ ( A @ k1_tarski @ k2_funcop_1 ) @ r1_tarski ) ),
inference(simp,[status(thm)],[69707]) ).
thf(80348,plain,
! [B: $i,A: $i] :
( ( ( A @ k3_tarski @ k1_zfmisc_1 @ ( A @ r1_tarski ) )
!= ( k1_xboole_0 @ ( sk2 @ ( B @ k1_tarski @ k2_funcop_1 ) @ r1_tarski ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2027,70680]) ).
thf(80349,plain,
! [B: $i,A: $i] :
( ( A @ k3_tarski @ k1_zfmisc_1 @ ( A @ r1_tarski ) )
!= ( k1_xboole_0 @ ( sk2 @ ( B @ k1_tarski @ k2_funcop_1 ) @ r1_tarski ) ) ),
inference(simp,[status(thm)],[80348]) ).
thf(80460,plain,
! [B: $i,A: $i] :
( ( ( A @ k3_tarski @ k1_zfmisc_1 )
!= k1_xboole_0 )
| ( A
!= ( sk2 @ ( B @ k1_tarski @ k2_funcop_1 ) ) ) ),
inference(simp,[status(thm)],[80349]) ).
thf(80497,plain,
! [A: $i] :
( ( sk2 @ ( A @ k1_tarski @ k2_funcop_1 ) @ k3_tarski @ k1_zfmisc_1 )
!= k1_xboole_0 ),
inference(simp,[status(thm)],[80460]) ).
thf(411,axiom,
! [A: $i] :
( ( k1_xboole_0 @ ( A @ k3_xboole_0 ) )
= k1_xboole_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_boole) ).
thf(3359,plain,
! [A: $i] :
( ( k1_xboole_0 @ ( A @ k3_xboole_0 ) )
= k1_xboole_0 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[411]) ).
thf(3360,plain,
! [A: $i] :
( ( k1_xboole_0 @ ( A @ k3_xboole_0 ) )
= k1_xboole_0 ),
inference(cnf,[status(esa)],[3359]) ).
thf(3361,plain,
! [A: $i] :
( ( k1_xboole_0 @ ( A @ k3_xboole_0 ) )
= k1_xboole_0 ),
inference(lifteq,[status(thm)],[3360]) ).
thf(97,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ k4_xboole_0 ) @ ( A @ k4_xboole_0 ) )
= ( B @ ( A @ k3_xboole_0 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t48_xboole_1) ).
thf(1758,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ k4_xboole_0 ) @ ( A @ k4_xboole_0 ) )
= ( B @ ( A @ k3_xboole_0 ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[97]) ).
thf(1759,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ k4_xboole_0 ) @ ( A @ k4_xboole_0 ) )
= ( B @ ( A @ k3_xboole_0 ) ) ),
inference(cnf,[status(esa)],[1758]) ).
thf(1760,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ k3_xboole_0 ) )
= ( B @ ( A @ k4_xboole_0 ) @ ( A @ k4_xboole_0 ) ) ),
inference(lifteq,[status(thm)],[1759]) ).
thf(197470,plain,
! [A: $i] :
( ( k1_xboole_0 @ ( A @ k4_xboole_0 ) @ ( A @ k4_xboole_0 ) )
= k1_xboole_0 ),
inference(rewrite,[status(thm)],[3361,1760]) ).
thf(64,axiom,
! [A: $i] :
( ( k1_xboole_0 @ ( A @ k4_xboole_0 ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_boole) ).
thf(1628,plain,
! [A: $i] :
( ( k1_xboole_0 @ ( A @ k4_xboole_0 ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[64]) ).
thf(1629,plain,
! [A: $i] :
( ( k1_xboole_0 @ ( A @ k4_xboole_0 ) )
= A ),
inference(cnf,[status(esa)],[1628]) ).
thf(1630,plain,
! [A: $i] :
( ( k1_xboole_0 @ ( A @ k4_xboole_0 ) )
= A ),
inference(lifteq,[status(thm)],[1629]) ).
thf(211631,plain,
! [A: $i] :
( ( A @ ( A @ k4_xboole_0 ) )
= k1_xboole_0 ),
inference(rewrite,[status(thm)],[197470,1630]) ).
thf(103,axiom,
! [A: $i,B: $i] :
( ( ( B @ ( A @ k4_xboole_0 ) )
= ( A @ ( B @ k4_xboole_0 ) ) )
=> ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t32_xboole_1) ).
thf(1781,plain,
! [A: $i,B: $i] :
( ( ( B @ ( A @ k4_xboole_0 ) )
= ( A @ ( B @ k4_xboole_0 ) ) )
=> ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[103]) ).
thf(1782,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( ( B @ ( A @ k4_xboole_0 ) )
!= ( A @ ( B @ k4_xboole_0 ) ) ) ),
inference(cnf,[status(esa)],[1781]) ).
thf(1783,plain,
! [B: $i,A: $i] :
( ( A = B )
| ( ( B @ ( A @ k4_xboole_0 ) )
!= ( A @ ( B @ k4_xboole_0 ) ) ) ),
inference(lifteq,[status(thm)],[1782]) ).
thf(1784,plain,
? [A: $i > $i > $i] :
! [B: $i,C: $i] :
( ( C @ ( B @ k4_xboole_0 ) @ ( C @ A ) )
= B ),
inference(detectInverse,[status(thm)],[1783]) ).
thf(1785,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ k4_xboole_0 ) @ ( B @ sk25 ) )
= A ),
inference(cnf,[status(esa)],[1784]) ).
thf(212612,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ k4_xboole_0 ) @ ( B @ sk25 ) )
= A ),
inference(lifteq,[status(thm)],[1785]) ).
thf(212649,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ k4_xboole_0 ) )
!= ( C @ ( B @ k4_xboole_0 ) ) )
| ( ( k1_xboole_0 @ ( C @ sk25 ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[211631,212612]) ).
thf(212650,plain,
! [A: $i] :
( ( k1_xboole_0 @ ( A @ sk25 ) )
= A ),
inference(pattern_uni,[status(thm)],[212649:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(255,axiom,
! [A: $i] :
( ( A @ ( k1_xboole_0 @ k4_xboole_0 ) )
= k1_xboole_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_boole) ).
thf(2534,plain,
! [A: $i] :
( ( A @ ( k1_xboole_0 @ k4_xboole_0 ) )
= k1_xboole_0 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[255]) ).
thf(2535,plain,
! [A: $i] :
( ( A @ ( k1_xboole_0 @ k4_xboole_0 ) )
= k1_xboole_0 ),
inference(cnf,[status(esa)],[2534]) ).
thf(2536,plain,
! [A: $i] :
( ( A @ ( k1_xboole_0 @ k4_xboole_0 ) )
= k1_xboole_0 ),
inference(lifteq,[status(thm)],[2535]) ).
thf(212643,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( k1_xboole_0 @ k4_xboole_0 ) )
!= ( C @ ( B @ k4_xboole_0 ) ) )
| ( ( k1_xboole_0 @ ( C @ sk25 ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[2536,212612]) ).
thf(212644,plain,
! [A: $i] :
( ( k1_xboole_0 @ ( A @ sk25 ) )
= k1_xboole_0 ),
inference(pattern_uni,[status(thm)],[212643:[bind(A,$thf( A )),bind(B,$thf( k1_xboole_0 )),bind(C,$thf( A ))]]) ).
thf(215818,plain,
! [A: $i] : ( k1_xboole_0 = A ),
inference(rewrite,[status(thm)],[212650,212644]) ).
thf(215943,plain,
$false,
inference(simplifyReflect,[status(thm)],[80497,215818]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LAT299+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % 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.05/0.31 % Computer : n012.cluster.edu
% 0.05/0.31 % Model : x86_64 x86_64
% 0.05/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.31 % Memory : 8046.5625MB
% 0.05/0.31 % OS : Linux 6.8.0-71-generic
% 0.05/0.31 % CPULimit : 300
% 0.05/0.31 % WCLimit : 300
% 0.05/0.31 % DateTime : Fri Sep 25 20:36:21 UTC 2026
% 0.05/0.32 % CPUTime :
% 0.05/0.32 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.39/0.59 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 3.44/1.40 % [INFO] Parsing done (809ms).
% 3.44/1.42 % [INFO] Running in sequential loop mode.
% 3.60/1.59 % [INFO] eprover registered as external prover.
% 3.79/1.60 % [INFO] Scanning for conjecture ...
% 5.42/2.10 % [INFO] Found a conjecture (or negated_conjecture) and 13593 axioms. Running axiom selection ...
% 7.91/3.55 % [INFO] Axiom selection finished. Selected 1309 axioms (removed 12284 axioms).
% 9.49/4.04 % [INFO] Problem is first-order (TPTP FOF).
% 9.49/4.09 % [INFO] Type checking passed.
% 9.49/4.09 % [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 ...
% 269.19/79.59 % [INFO] Killing All external provers ...
% 269.19/79.59 % Time passed: 79203ms (effective reasoning time: 78168ms)
% 269.19/79.59 % 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)>
% 269.19/79.60 % Axioms used in derivation (11): t113_zfmisc_1, t2_boole, d2_funcop_1, t48_xboole_1, fc1_finset_1, t100_zfmisc_1, t7_funct_4, fc2_funcop_1, t3_boole, t4_boole, t32_xboole_1
% 269.19/79.60 % No. of inferences in proof: 90
% 259.00/79.60 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 79203 ms resp. 78168 ms w/o parsing
% 259.00/79.63 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 259.00/79.63 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------