%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ALG251^3 : TPTP v9.3.1. Bugfixed v5.2.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 : n026.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 07:45:02 AM UTC 2026
% Result : Theorem 57.15s 17.54s
% Output : Refutation 57.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 13
% Syntax : Number of formulae : 262 ( 100 unt; 0 typ; 12 def)
% Number of atoms : 808 ( 383 equ; 30 cnn)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 3323 ( 524 ~; 373 |; 10 &;2373 @)
% ( 0 <=>; 43 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 6 avg)
% Number of types : 3 ( 2 usr)
% Number of type conns : 56 ( 56 >; 0 *; 0 +; 0 <<)
% Number of symbols : 22 ( 18 usr; 15 con; 0-2 aty)
% Number of variables : 424 ( 22 ^; 397 !; 0 ?; 424 :)
% ( 0 !>; 0 ?*; 0 @-; 5 @+)
% Comments :
%------------------------------------------------------------------------------
thf(term_type,type,
term: $tType ).
thf(subst_type,type,
subst: $tType ).
thf(one_decl,type,
one: term ).
thf(sub_decl,type,
sub: term > subst > term ).
thf(sh_decl,type,
sh: subst ).
thf(push_decl,type,
push: term > subst > subst ).
thf(comp_decl,type,
comp: subst > subst > subst ).
thf(var_decl,type,
var: term > $o ).
thf(ulamvar1_decl,type,
ulamvar1: $o ).
thf(pushprop_lthm_orig_decl,type,
pushprop_lthm_orig: $o ).
thf(ulamvarind_decl,type,
ulamvarind: $o ).
thf(axclos_decl,type,
axclos: $o ).
thf(axvarcons_decl,type,
axvarcons: $o ).
thf(pushprop_decl,type,
pushprop: $o ).
thf(axshiftcons_decl,type,
axshiftcons: $o ).
thf(sk1_decl,type,
sk1: ( term > $o ) > term ).
thf(sk2_decl,type,
sk2: term > $o ).
thf(sk3_decl,type,
sk3: term ).
thf(sk4_decl,type,
sk4: subst ).
thf(sk5_decl,type,
sk5: term ).
thf(ulamvar1_def,definition,
( ulamvar1
= ( var @ one ) ) ).
thf(pushprop_lthm_orig_def,definition,
( pushprop_lthm_orig
= ( ulamvar1
=> ( axvarcons
=> ( axclos
=> ( axshiftcons
=> ( ulamvarind
=> pushprop ) ) ) ) ) ) ).
thf(ulamvarind_def,definition,
( ulamvarind
= ( ! [A: term > $o] :
( ( A @ one )
=> ( ! [B: term] :
( ( var @ B )
=> ( ( A @ B )
=> ( A @ ( sub @ B @ sh ) ) ) )
=> ! [B: term] :
( ( var @ B )
=> ( A @ B ) ) ) ) ) ) ).
thf(axclos_def,definition,
( axclos
= ( ! [A: term,B: subst,C: subst] :
( ( sub @ ( sub @ A @ B ) @ C )
= ( sub @ A @ ( comp @ B @ C ) ) ) ) ) ).
thf(axvarcons_def,definition,
( axvarcons
= ( ! [A: term,B: subst] :
( ( sub @ one @ ( push @ A @ B ) )
= A ) ) ) ).
thf(pushprop_def,definition,
( pushprop
= ( ! [A: term > $o,B: term,C: subst] :
( ! [D: term] :
( ( var @ D )
=> ( A @ ( sub @ D @ C ) ) )
=> ( ( A @ B )
=> ! [D: term] :
( ( var @ D )
=> ( A @ ( sub @ D @ ( push @ B @ C ) ) ) ) ) ) ) ) ).
thf(axshiftcons_def,definition,
( axshiftcons
= ( ! [A: term,B: subst] :
( ( comp @ sh @ ( push @ A @ B ) )
= B ) ) ) ).
thf(sk1_def,definition,
( sk1
= ( ^ [A: term > $o] :
@+[B: term] :
~ ( ( var @ B )
=> ( ( A @ B )
=> ( A @ ( sub @ B @ sh ) ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: term > $o] :
~ ! [B: term,C: subst] :
( ! [D: term] :
( ( var @ D )
=> ( A @ ( sub @ D @ C ) ) )
=> ( ( A @ B )
=> ! [D: term] :
( ( var @ D )
=> ( A @ ( sub @ D @ ( push @ B @ C ) ) ) ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: term] :
~ ! [B: subst] :
( ! [C: term] :
( ( var @ C )
=> ( sk2 @ ( sub @ C @ B ) ) )
=> ( ( sk2 @ A )
=> ! [C: term] :
( ( var @ C )
=> ( sk2 @ ( sub @ C @ ( push @ A @ B ) ) ) ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( @+[A: subst] :
~ ( ! [B: term] :
( ( var @ B )
=> ( sk2 @ ( sub @ B @ A ) ) )
=> ( ( sk2 @ sk3 )
=> ! [B: term] :
( ( var @ B )
=> ( sk2 @ ( sub @ B @ ( push @ sk3 @ A ) ) ) ) ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( @+[A: term] :
~ ( ( var @ A )
=> ( sk2 @ ( sub @ A @ ( push @ sk3 @ sk4 ) ) ) ) ) ) ).
thf(1,conjecture,
pushprop_lthm_orig,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm) ).
thf(2,negated_conjecture,
~ pushprop_lthm_orig,
inference(neg_conjecture,[status(cth)],[1]) ).
thf(3,plain,
~ ( ( var @ one )
=> ( ! [A: term,B: subst] :
( ( sub @ one @ ( push @ A @ B ) )
= A )
=> ( ! [A: term,B: subst,C: subst] :
( ( sub @ ( sub @ A @ B ) @ C )
= ( sub @ A @ ( comp @ B @ C ) ) )
=> ( ! [A: term,B: subst] :
( ( comp @ sh @ ( push @ A @ B ) )
= B )
=> ( ! [A: term > $o] :
( ( A @ one )
=> ( ! [B: term] :
( ( var @ B )
=> ( ( A @ B )
=> ( A @ ( sub @ B @ sh ) ) ) )
=> ! [B: term] :
( ( var @ B )
=> ( A @ B ) ) ) )
=> ! [A: term > $o,B: term,C: subst] :
( ! [D: term] :
( ( var @ D )
=> ( A @ ( sub @ D @ C ) ) )
=> ( ( A @ B )
=> ! [D: term] :
( ( var @ D )
=> ( A @ ( sub @ D @ ( push @ B @ C ) ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(4,plain,
! [J: term,I: term,H: term > $o,G: subst,F: term,E: subst,D: subst,C: term,B: subst,A: term] :
( ( var @ one )
& ( ( sub @ one @ ( push @ A @ B ) )
= A )
& ( ( sub @ ( sub @ C @ D ) @ E )
= ( sub @ C @ ( comp @ D @ E ) ) )
& ( ( comp @ sh @ ( push @ F @ G ) )
= G )
& ( ~ ( H @ one )
| ( var @ ( sk1 @ H ) )
| ~ ( var @ I )
| ( H @ I ) )
& ( ~ ( H @ one )
| ( H @ ( sk1 @ H ) )
| ~ ( var @ I )
| ( H @ I ) )
& ( ~ ( H @ one )
| ~ ( H @ ( sub @ ( sk1 @ H ) @ sh ) )
| ~ ( var @ I )
| ( H @ I ) )
& ( ~ ( var @ J )
| ( sk2 @ ( sub @ J @ sk4 ) ) )
& ( sk2 @ sk3 )
& ( var @ sk5 )
& ~ ( sk2 @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) ) ),
inference(cnf,[status(esa)],[3]) ).
thf(5,plain,
var @ one,
inference(cnfConj,[status(thm)],[4]) ).
thf(13,plain,
var @ sk5,
inference(cnfConj,[status(thm)],[4]) ).
thf(14,plain,
! [B: term,A: term > $o] :
( ~ ( A @ one )
| ~ ( A @ ( sub @ ( sk1 @ A ) @ sh ) )
| ~ ( var @ B )
| ( A @ B ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(20,plain,
! [B: term,A: term > $o] :
( ~ ( A @ one )
| ~ ( A @ ( sub @ ( sk1 @ A ) @ sh ) )
| ~ ( var @ B )
| ( A @ B ) ),
inference(simp,[status(thm)],[14]) ).
thf(54,plain,
! [B: term,A: term > $o] :
( ~ ( A @ one )
| ~ ( A @ ( sub @ ( sk1 @ A ) @ sh ) )
| ~ $true
| ( A @ B )
| ( ( var @ sk5 )
!= ( var @ B ) ) ),
inference(paramod_ordered,[status(thm)],[13,20]) ).
thf(55,plain,
! [B: term,A: term > $o] :
( ~ ( A @ one )
| ~ ( A @ ( sub @ ( sk1 @ A ) @ sh ) )
| ( A @ B )
| ( ( var @ sk5 )
!= ( var @ B ) ) ),
inference(simp,[status(thm)],[54]) ).
thf(56,plain,
! [A: term > $o] :
( ~ ( A @ one )
| ~ ( A @ ( sub @ ( sk1 @ A ) @ sh ) )
| ( A @ sk5 ) ),
inference(pattern_uni,[status(thm)],[55:[bind(A,$thf( A )),bind(B,$thf( sk5 ))]]) ).
thf(9,plain,
! [B: term,A: term > $o] :
( ~ ( A @ one )
| ( var @ ( sk1 @ A ) )
| ~ ( var @ B )
| ( A @ B ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(22,plain,
! [B: term,A: term > $o] :
( ~ ( A @ one )
| ( var @ ( sk1 @ A ) )
| ~ ( var @ B )
| ( A @ B ) ),
inference(simp,[status(thm)],[9]) ).
thf(265,plain,
! [B: term,A: term > $o] :
( ~ ( A @ one )
| ( var @ ( sk1 @ A ) )
| ~ $true
| ( A @ B )
| ( ( var @ sk5 )
!= ( var @ B ) ) ),
inference(paramod_ordered,[status(thm)],[13,22]) ).
thf(266,plain,
! [B: term,A: term > $o] :
( ~ ( A @ one )
| ( var @ ( sk1 @ A ) )
| ( A @ B )
| ( ( var @ sk5 )
!= ( var @ B ) ) ),
inference(simp,[status(thm)],[265]) ).
thf(267,plain,
! [A: term > $o] :
( ~ ( A @ one )
| ( var @ ( sk1 @ A ) )
| ( A @ sk5 ) ),
inference(pattern_uni,[status(thm)],[266:[bind(A,$thf( A )),bind(B,$thf( sk5 ))]]) ).
thf(303,plain,
( ( one != one )
| ( var @ ( sk1 @ ( (=) @ term @ one ) ) )
| ( one = sk5 ) ),
inference(replace_leibeq,[status(thm)],[267:[bind(A,$thf( (=) @ term @ one ))]]) ).
thf(313,plain,
( ( one != one )
| ( sk5 = one )
| ( var @ ( sk1 @ ( (=) @ term @ one ) ) ) ),
inference(lifteq,[status(thm)],[303]) ).
thf(332,plain,
( ( var @ ( sk1 @ ( (=) @ term @ one ) ) )
| ( sk5 = one ) ),
inference(pattern_uni,[status(thm)],[313:[]]) ).
thf(10,plain,
! [B: subst,A: term] :
( ( sub @ one @ ( push @ A @ B ) )
= A ),
inference(cnfConj,[status(thm)],[4]) ).
thf(19,plain,
! [B: subst,A: term] :
( ( sub @ one @ ( push @ A @ B ) )
= A ),
inference(lifteq,[status(thm)],[10]) ).
thf(7,plain,
sk2 @ sk3,
inference(cnfConj,[status(thm)],[4]) ).
thf(15,plain,
~ ( sk2 @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(34,plain,
( ~ $true
| ( ( sk2 @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
!= ( sk2 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[7,15]) ).
thf(35,plain,
( ( sk2 @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
!= ( sk2 @ sk3 ) ),
inference(simp,[status(thm)],[34]) ).
thf(36,plain,
( ( sub @ sk5 @ ( push @ sk3 @ sk4 ) )
!= sk3 ),
inference(simp,[status(thm)],[35]) ).
thf(174,plain,
! [B: subst,A: term] :
( ( A != sk3 )
| ( ( sub @ one @ ( push @ A @ B ) )
!= ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,36]) ).
thf(180,plain,
! [A: subst] :
( ( sk5 != one )
| ( ( push @ sk3 @ A )
!= ( push @ sk3 @ sk4 ) ) ),
inference(simp,[status(thm)],[174]) ).
thf(183,plain,
! [A: subst] :
( ( sk5 != one )
| ( ( push @ sk3 @ A )
!= ( push @ sk3 @ sk4 ) ) ),
inference(simp,[status(thm)],[180]) ).
thf(686,plain,
! [A: subst] :
( ( sk5 != one )
| ( sk3 != sk3 )
| ( A != sk4 ) ),
inference(simp,[status(thm)],[183]) ).
thf(700,plain,
sk5 != one,
inference(simp,[status(thm)],[686]) ).
thf(702,plain,
var @ ( sk1 @ ( (=) @ term @ one ) ),
inference(simplifyReflect,[status(thm)],[332,700]) ).
thf(8,plain,
! [B: term,A: term > $o] :
( ~ ( A @ one )
| ( A @ ( sk1 @ A ) )
| ~ ( var @ B )
| ( A @ B ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(18,plain,
! [A: term] :
( ( one != one )
| ( one
= ( sk1 @ ( (=) @ term @ one ) ) )
| ~ ( var @ A )
| ( one = A ) ),
inference(replace_leibeq,[status(thm)],[8:[bind(A,$thf( (=) @ term @ one ))]]) ).
thf(27,plain,
! [A: term] :
( ( one != one )
| ( ( sk1 @ ( (=) @ term @ one ) )
= one )
| ( one = A )
| ~ ( var @ A ) ),
inference(lifteq,[status(thm)],[18]) ).
thf(28,plain,
! [A: term] :
( ( ( sk1 @ ( (=) @ term @ one ) )
= one )
| ( one = A )
| ~ ( var @ A ) ),
inference(simp,[status(thm)],[27]) ).
thf(950,plain,
! [A: term] :
( ( ( sk1 @ ( (=) @ term @ one ) )
= one )
| ( one = A )
| ~ $true
| ( ( var @ ( sk1 @ ( (=) @ term @ one ) ) )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[702,28]) ).
thf(951,plain,
! [A: term] :
( ( ( sk1 @ ( (=) @ term @ one ) )
= one )
| ( one = A )
| ( ( var @ ( sk1 @ ( (=) @ term @ one ) ) )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[950]) ).
thf(952,plain,
( ( ( sk1 @ ( (=) @ term @ one ) )
= one )
| ( ( sk1 @ ( (=) @ term @ one ) )
= one ) ),
inference(pattern_uni,[status(thm)],[951:[bind(A,$thf( sk1 @ ( (=) @ term @ one ) ))]]) ).
thf(1095,plain,
( ( sk1 @ ( (=) @ term @ one ) )
= one ),
inference(simp,[status(thm)],[952]) ).
thf(12,plain,
! [C: subst,B: subst,A: term] :
( ( sub @ ( sub @ A @ B ) @ C )
= ( sub @ A @ ( comp @ B @ C ) ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(25,plain,
! [C: subst,B: subst,A: term] :
( ( sub @ ( sub @ A @ B ) @ C )
= ( sub @ A @ ( comp @ B @ C ) ) ),
inference(lifteq,[status(thm)],[12]) ).
thf(26,plain,
! [C: subst,B: subst,A: term] :
( ( sub @ ( sub @ A @ B ) @ C )
= ( sub @ A @ ( comp @ B @ C ) ) ),
inference(simp,[status(thm)],[25]) ).
thf(774,plain,
! [E: subst,D: subst,C: term,B: subst,A: term] :
( ( ( sub @ A @ E )
= ( sub @ C @ ( comp @ D @ E ) ) )
| ( ( sub @ one @ ( push @ A @ B ) )
!= ( sub @ C @ D ) ) ),
inference(paramod_ordered,[status(thm)],[19,26]) ).
thf(775,plain,
! [C: subst,B: term,A: subst] :
( ( sub @ B @ A )
= ( sub @ one @ ( comp @ ( push @ B @ C ) @ A ) ) ),
inference(pattern_uni,[status(thm)],[774:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( one )),bind(D,$thf( push @ F @ G ))]]) ).
thf(813,plain,
! [C: subst,B: term,A: subst] :
( ( sub @ B @ A )
= ( sub @ one @ ( comp @ ( push @ B @ C ) @ A ) ) ),
inference(simp,[status(thm)],[775]) ).
thf(6,plain,
! [A: term] :
( ~ ( var @ A )
| ( sk2 @ ( sub @ A @ sk4 ) ) ),
inference(cnfConj,[status(thm)],[4]) ).
thf(21,plain,
! [A: term] :
( ~ ( var @ A )
| ( sk2 @ ( sub @ A @ sk4 ) ) ),
inference(simp,[status(thm)],[6]) ).
thf(184,plain,
! [A: term] :
( ~ $true
| ( sk2 @ ( sub @ A @ sk4 ) )
| ( ( var @ one )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[5,21]) ).
thf(185,plain,
! [A: term] :
( ( sk2 @ ( sub @ A @ sk4 ) )
| ( ( var @ one )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[184]) ).
thf(186,plain,
sk2 @ ( sub @ one @ sk4 ),
inference(pattern_uni,[status(thm)],[185:[bind(A,$thf( one ))]]) ).
thf(217,plain,
( ~ $true
| ( ( sk2 @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
!= ( sk2 @ ( sub @ one @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[186,15]) ).
thf(218,plain,
( ( sk2 @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
!= ( sk2 @ ( sub @ one @ sk4 ) ) ),
inference(simp,[status(thm)],[217]) ).
thf(226,plain,
( ( sub @ sk5 @ ( push @ sk3 @ sk4 ) )
!= ( sub @ one @ sk4 ) ),
inference(simp,[status(thm)],[218]) ).
thf(1247,plain,
! [C: subst,B: term,A: subst] :
( ( ( sub @ B @ A )
!= ( sub @ one @ sk4 ) )
| ( ( sub @ one @ ( comp @ ( push @ B @ C ) @ A ) )
!= ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[813,226]) ).
thf(1298,plain,
! [C: subst,B: term,A: subst] :
( ( B != one )
| ( A != sk4 )
| ( ( sub @ one @ ( comp @ ( push @ B @ C ) @ A ) )
!= ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) ) ),
inference(simp,[status(thm)],[1247]) ).
thf(1323,plain,
! [A: subst] :
( ( sub @ one @ ( comp @ ( push @ one @ A ) @ sk4 ) )
!= ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) ),
inference(simp,[status(thm)],[1298]) ).
thf(2514,plain,
! [D: subst,C: subst,B: term,A: subst] :
( ( ( sub @ one @ ( comp @ ( push @ B @ C ) @ A ) )
!= ( sub @ one @ ( comp @ ( push @ one @ D ) @ sk4 ) ) )
| ( ( sub @ B @ A )
!= ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[813,1323]) ).
thf(2515,plain,
! [B: subst,A: subst] :
( ( sub @ one @ ( comp @ ( push @ sk5 @ A ) @ ( push @ sk3 @ sk4 ) ) )
!= ( sub @ one @ ( comp @ ( push @ one @ B ) @ sk4 ) ) ),
inference(pattern_uni,[status(thm)],[2514:[bind(A,$thf( push @ sk3 @ sk4 )),bind(B,$thf( sk5 )),bind(C,$thf( C )),bind(D,$thf( D ))]]) ).
thf(2561,plain,
! [B: subst,A: subst] :
( ( sub @ one @ ( comp @ ( push @ sk5 @ A ) @ ( push @ sk3 @ sk4 ) ) )
!= ( sub @ one @ ( comp @ ( push @ one @ B ) @ sk4 ) ) ),
inference(simp,[status(thm)],[2515]) ).
thf(1282,plain,
! [C: subst,B: term,A: subst] :
( ( ( sub @ one @ ( comp @ ( push @ B @ C ) @ A ) )
!= sk3 )
| ( ( sub @ B @ A )
!= ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[813,36]) ).
thf(1283,plain,
! [A: subst] :
( ( sub @ one @ ( comp @ ( push @ sk5 @ A ) @ ( push @ sk3 @ sk4 ) ) )
!= sk3 ),
inference(pattern_uni,[status(thm)],[1282:[bind(A,$thf( push @ sk3 @ sk4 )),bind(B,$thf( sk5 )),bind(C,$thf( C ))]]) ).
thf(1317,plain,
! [A: subst] :
( ( sub @ one @ ( comp @ ( push @ sk5 @ A ) @ ( push @ sk3 @ sk4 ) ) )
!= sk3 ),
inference(simp,[status(thm)],[1283]) ).
thf(1983,plain,
! [C: subst,B: subst,A: term] :
( ( A != sk3 )
| ( ( sub @ one @ ( push @ A @ B ) )
!= ( sub @ one @ ( comp @ ( push @ sk5 @ C ) @ ( push @ sk3 @ sk4 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,1317]) ).
thf(1984,plain,
! [B: subst,A: subst] :
( ( sub @ one @ ( push @ sk3 @ A ) )
!= ( sub @ one @ ( comp @ ( push @ sk5 @ B ) @ ( push @ sk3 @ sk4 ) ) ) ),
inference(simp,[status(thm)],[1983]) ).
thf(1988,plain,
! [B: subst,A: subst] :
( ( sub @ one @ ( push @ sk3 @ A ) )
!= ( sub @ one @ ( comp @ ( push @ sk5 @ B ) @ ( push @ sk3 @ sk4 ) ) ) ),
inference(simp,[status(thm)],[1984]) ).
thf(1287,plain,
! [E: subst,D: term,C: subst,B: subst,A: term] :
( ( A
= ( sub @ one @ ( comp @ ( push @ D @ E ) @ C ) ) )
| ( ( sub @ one @ ( push @ A @ B ) )
!= ( sub @ D @ C ) ) ),
inference(paramod_ordered,[status(thm)],[19,813]) ).
thf(1288,plain,
! [C: subst,B: term,A: subst] :
( ( sub @ one @ ( comp @ ( push @ one @ A ) @ ( push @ B @ C ) ) )
= B ),
inference(pattern_uni,[status(thm)],[1287:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( push @ F @ G )),bind(D,$thf( one ))]]) ).
thf(1318,plain,
! [C: subst,B: term,A: subst] :
( ( sub @ one @ ( comp @ ( push @ one @ A ) @ ( push @ B @ C ) ) )
= B ),
inference(simp,[status(thm)],[1288]) ).
thf(4044,plain,
! [F: subst,E: subst,D: term,C: subst,B: term,A: subst] :
( ( B
= ( sub @ ( sub @ D @ E ) @ F ) )
| ( ( sub @ one @ ( comp @ ( push @ one @ A ) @ ( push @ B @ C ) ) )
!= ( sub @ D @ ( comp @ E @ F ) ) ) ),
inference(paramod_ordered,[status(thm)],[1318,26]) ).
thf(4045,plain,
! [C: subst,B: term,A: subst] :
( ( sub @ ( sub @ one @ ( push @ one @ A ) ) @ ( push @ B @ C ) )
= B ),
inference(pattern_uni,[status(thm)],[4044:[bind(A,$thf( H )),bind(B,$thf( I )),bind(C,$thf( J )),bind(D,$thf( one )),bind(E,$thf( push @ one @ H )),bind(F,$thf( push @ I @ J ))]]) ).
thf(4203,plain,
! [C: subst,B: term,A: subst] :
( ( sub @ ( sub @ one @ ( push @ one @ A ) ) @ ( push @ B @ C ) )
= B ),
inference(simp,[status(thm)],[4045]) ).
thf(5819,plain,
! [B: subst,A: term] :
( ( sub @ one @ ( push @ A @ B ) )
= A ),
inference(rewrite,[status(thm)],[4203,19]) ).
thf(8734,plain,
! [A: subst] :
( ( sub @ one @ ( comp @ ( push @ sk5 @ A ) @ ( push @ sk3 @ sk4 ) ) )
!= sk3 ),
inference(rewrite,[status(thm)],[1988,5819]) ).
thf(11,plain,
! [B: subst,A: term] :
( ( comp @ sh @ ( push @ A @ B ) )
= B ),
inference(cnfConj,[status(thm)],[4]) ).
thf(31,plain,
! [B: subst,A: term] :
( ( comp @ sh @ ( push @ A @ B ) )
= B ),
inference(lifteq,[status(thm)],[11]) ).
thf(32,plain,
! [B: subst,A: term] :
( ( comp @ sh @ ( push @ A @ B ) )
= B ),
inference(simp,[status(thm)],[31]) ).
thf(754,plain,
! [E: subst,D: subst,C: term,B: subst,A: term] :
( ( ( sub @ C @ B )
= ( sub @ ( sub @ C @ D ) @ E ) )
| ( ( comp @ sh @ ( push @ A @ B ) )
!= ( comp @ D @ E ) ) ),
inference(paramod_ordered,[status(thm)],[32,26]) ).
thf(755,plain,
! [C: subst,B: term,A: term] :
( ( sub @ ( sub @ A @ sh ) @ ( push @ B @ C ) )
= ( sub @ A @ C ) ),
inference(pattern_uni,[status(thm)],[754:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( C )),bind(D,$thf( sh )),bind(E,$thf( push @ F @ G ))]]) ).
thf(846,plain,
! [C: subst,B: term,A: term] :
( ( sub @ ( sub @ A @ sh ) @ ( push @ B @ C ) )
= ( sub @ A @ C ) ),
inference(simp,[status(thm)],[755]) ).
thf(2518,plain,
! [D: subst,C: subst,B: term,A: subst] :
( ( ( sub @ B @ A )
!= ( sub @ one @ ( comp @ ( push @ one @ D ) @ sk4 ) ) )
| ( ( sub @ one @ ( comp @ ( push @ B @ C ) @ A ) )
!= ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[813,1323]) ).
thf(2542,plain,
! [D: subst,C: subst,B: term,A: subst] :
( ( B != one )
| ( A
!= ( comp @ ( push @ one @ D ) @ sk4 ) )
| ( ( sub @ one @ ( comp @ ( push @ B @ C ) @ A ) )
!= ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) ) ),
inference(simp,[status(thm)],[2518]) ).
thf(2559,plain,
! [B: subst,A: subst] :
( ( sub @ one @ ( comp @ ( push @ one @ A ) @ ( comp @ ( push @ one @ B ) @ sk4 ) ) )
!= ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) ),
inference(simp,[status(thm)],[2542]) ).
thf(61,plain,
! [B: term,A: term > $o] :
( ~ ( A @ one )
| ~ ( A @ ( sub @ ( sk1 @ A ) @ sh ) )
| ~ ( var @ B )
| ~ $true
| ( ( A @ B )
!= ( sk2 @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[20,15]) ).
thf(62,plain,
! [B: term,A: term > $o] :
( ~ ( A @ one )
| ~ ( A @ ( sub @ ( sk1 @ A ) @ sh ) )
| ~ ( var @ B )
| ( ( A @ B )
!= ( sk2 @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) ) ) ),
inference(simp,[status(thm)],[61]) ).
thf(129,plain,
( ~ ( sk2 @ one )
| ~ ( sk2 @ ( sub @ ( sk1 @ sk2 ) @ sh ) )
| ~ ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) ) ),
inference(pre_uni,[status(thm)],[62:[bind(A,$thf( sk2 )),bind(B,$thf( sub @ sk5 @ ( push @ sk3 @ sk4 ) ))]]) ).
thf(1156,plain,
( ~ $true
| ~ ( sk2 @ ( sub @ ( sk1 @ sk2 ) @ sh ) )
| ~ ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
| ( ( sk2 @ sk3 )
!= ( sk2 @ one ) ) ),
inference(paramod_ordered,[status(thm)],[7,129]) ).
thf(1157,plain,
( ~ ( sk2 @ ( sub @ ( sk1 @ sk2 ) @ sh ) )
| ~ ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
| ( ( sk2 @ sk3 )
!= ( sk2 @ one ) ) ),
inference(simp,[status(thm)],[1156]) ).
thf(1199,plain,
( ~ ( sk2 @ ( sub @ ( sk1 @ sk2 ) @ sh ) )
| ~ ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
| ( sk3 != one ) ),
inference(simp,[status(thm)],[1157]) ).
thf(2068,plain,
( ~ ( sk2 @ ( sub @ ( sk1 @ sk2 ) @ sh ) )
| ~ $true
| ( sk3 != one )
| ( ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
!= ( var @ sk5 ) ) ),
inference(paramod_ordered,[status(thm)],[13,1199]) ).
thf(2069,plain,
( ~ ( sk2 @ ( sub @ ( sk1 @ sk2 ) @ sh ) )
| ( sk3 != one )
| ( ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
!= ( var @ sk5 ) ) ),
inference(simp,[status(thm)],[2068]) ).
thf(2131,plain,
( ~ ( sk2 @ ( sub @ ( sk1 @ sk2 ) @ sh ) )
| ( sk3 != one )
| ( ( sub @ sk5 @ ( push @ sk3 @ sk4 ) )
!= sk5 ) ),
inference(simp,[status(thm)],[2069]) ).
thf(1174,plain,
( ~ ( sk2 @ one )
| ~ ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
| ( ( sk2 @ ( sub @ ( sk1 @ sk2 ) @ sh ) )
!= ( sk2 @ one ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[129]) ).
thf(1187,plain,
( ~ ( sk2 @ one )
| ~ ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
| ( ( sub @ ( sk1 @ sk2 ) @ sh )
!= one ) ),
inference(simp,[status(thm)],[1174]) ).
thf(1413,plain,
( ~ $true
| ~ ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
| ( ( sub @ ( sk1 @ sk2 ) @ sh )
!= one )
| ( ( sk2 @ sk3 )
!= ( sk2 @ one ) ) ),
inference(paramod_ordered,[status(thm)],[7,1187]) ).
thf(1414,plain,
( ~ ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
| ( ( sub @ ( sk1 @ sk2 ) @ sh )
!= one )
| ( ( sk2 @ sk3 )
!= ( sk2 @ one ) ) ),
inference(simp,[status(thm)],[1413]) ).
thf(1454,plain,
( ~ ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
| ( ( sub @ ( sk1 @ sk2 ) @ sh )
!= one )
| ( sk3 != one ) ),
inference(simp,[status(thm)],[1414]) ).
thf(67,plain,
! [B: term,A: term > $o] :
( ~ ( A @ one )
| ~ ( A @ ( sub @ ( sk1 @ A ) @ sh ) )
| ~ ( var @ B )
| ( ( A @ B )
!= ( ~ ( A @ one ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[20]) ).
thf(110,plain,
! [B: term,A: term > $o] :
( ~ ( A @ one )
| ~ ( A @ ( sub @ ( sk1 @ A ) @ sh ) )
| ~ ( var @ B )
| ( ( A @ B )
!= ( ~ ( A @ one ) ) ) ),
inference(simp,[status(thm)],[67]) ).
thf(132,plain,
( ~ ( sk2 @ ( sub @ one @ ( push @ sk3 @ sk4 ) ) )
| ~ ( sk2
@ ( sub
@ ( sub
@ ( sk1
@ ^ [A: term] : ( sk2 @ ( sub @ A @ ( push @ sk3 @ sk4 ) ) ) )
@ sh )
@ ( push @ sk3 @ sk4 ) ) )
| ~ ( var @ sk5 ) ),
inference(pre_uni,[status(thm)],[62:[bind(A,$thf( ^ [C: term] : ( sk2 @ ( sub @ C @ ( push @ sk3 @ sk4 ) ) ) )),bind(B,$thf( sk5 ))]]) ).
thf(12941,plain,
( ~ ( sk2 @ sk3 )
| ~ ( sk2
@ ( sub
@ ( sk1
@ ^ [A: term] : ( sk2 @ ( sub @ A @ ( push @ sk3 @ sk4 ) ) ) )
@ sk4 ) )
| ~ $true ),
inference(rewrite,[status(thm)],[132,5819,13,846]) ).
thf(12942,plain,
( ~ ( sk2 @ sk3 )
| ~ ( sk2
@ ( sub
@ ( sk1
@ ^ [A: term] : ( sk2 @ ( sub @ A @ ( push @ sk3 @ sk4 ) ) ) )
@ sk4 ) ) ),
inference(simp,[status(thm)],[12941]) ).
thf(12988,plain,
( ~ $true
| ~ ( sk2
@ ( sub
@ ( sk1
@ ^ [A: term] : ( sk2 @ ( sub @ A @ ( push @ sk3 @ sk4 ) ) ) )
@ sk4 ) )
| ( ( sk2 @ sk3 )
!= ( sk2 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[7,12942]) ).
thf(12989,plain,
( ~ ( sk2
@ ( sub
@ ( sk1
@ ^ [A: term] : ( sk2 @ ( sub @ A @ ( push @ sk3 @ sk4 ) ) ) )
@ sk4 ) )
| ( ( sk2 @ sk3 )
!= ( sk2 @ sk3 ) ) ),
inference(simp,[status(thm)],[12988]) ).
thf(12990,plain,
~ ( sk2
@ ( sub
@ ( sk1
@ ^ [A: term] : ( sk2 @ ( sub @ A @ ( push @ sk3 @ sk4 ) ) ) )
@ sk4 ) ),
inference(pattern_uni,[status(thm)],[12989:[]]) ).
thf(13149,plain,
! [A: term] :
( ~ ( var @ A )
| ~ $true
| ( ( sk2 @ ( sub @ A @ sk4 ) )
!= ( sk2
@ ( sub
@ ( sk1
@ ^ [B: term] : ( sk2 @ ( sub @ B @ ( push @ sk3 @ sk4 ) ) ) )
@ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[21,12990]) ).
thf(13150,plain,
! [A: term] :
( ~ ( var @ A )
| ( ( sk2 @ ( sub @ A @ sk4 ) )
!= ( sk2
@ ( sub
@ ( sk1
@ ^ [B: term] : ( sk2 @ ( sub @ B @ ( push @ sk3 @ sk4 ) ) ) )
@ sk4 ) ) ) ),
inference(simp,[status(thm)],[13149]) ).
thf(13151,plain,
~ ( var
@ ( sk1
@ ^ [A: term] : ( sk2 @ ( sub @ A @ ( push @ sk3 @ sk4 ) ) ) ) ),
inference(pattern_uni,[status(thm)],[13150:[bind(A,$thf( sk1 @ ^ [B: term] : ( sk2 @ ( sub @ B @ ( push @ sk3 @ sk4 ) ) ) ))]]) ).
thf(1411,plain,
( ~ ( sk2 @ one )
| ~ $true
| ( ( sub @ ( sk1 @ sk2 ) @ sh )
!= one )
| ( ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
!= ( var @ sk5 ) ) ),
inference(paramod_ordered,[status(thm)],[13,1187]) ).
thf(1412,plain,
( ~ ( sk2 @ one )
| ( ( sub @ ( sk1 @ sk2 ) @ sh )
!= one )
| ( ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
!= ( var @ sk5 ) ) ),
inference(simp,[status(thm)],[1411]) ).
thf(1462,plain,
( ~ ( sk2 @ one )
| ( ( sub @ ( sk1 @ sk2 ) @ sh )
!= one )
| ( ( sub @ sk5 @ ( push @ sk3 @ sk4 ) )
!= sk5 ) ),
inference(simp,[status(thm)],[1412]) ).
thf(193,plain,
! [A: term] :
( ~ $true
| ( sk2 @ ( sub @ A @ sk4 ) )
| ( ( var @ sk5 )
!= ( var @ A ) ) ),
inference(paramod_ordered,[status(thm)],[13,21]) ).
thf(194,plain,
! [A: term] :
( ( sk2 @ ( sub @ A @ sk4 ) )
| ( ( var @ sk5 )
!= ( var @ A ) ) ),
inference(simp,[status(thm)],[193]) ).
thf(195,plain,
sk2 @ ( sub @ sk5 @ sk4 ),
inference(pattern_uni,[status(thm)],[194:[bind(A,$thf( sk5 ))]]) ).
thf(1290,plain,
! [C: subst,B: term,A: subst] :
( ( sk2 @ ( sub @ one @ ( comp @ ( push @ B @ C ) @ A ) ) )
| ( ( sub @ B @ A )
!= ( sub @ sk5 @ sk4 ) ) ),
inference(paramod_ordered,[status(thm)],[813,195]) ).
thf(1291,plain,
! [A: subst] : ( sk2 @ ( sub @ one @ ( comp @ ( push @ sk5 @ A ) @ sk4 ) ) ),
inference(pattern_uni,[status(thm)],[1290:[bind(A,$thf( sk4 )),bind(B,$thf( sk5 ))]]) ).
thf(1319,plain,
! [A: subst] : ( sk2 @ ( sub @ one @ ( comp @ ( push @ sk5 @ A ) @ sk4 ) ) ),
inference(simp,[status(thm)],[1291]) ).
thf(37,plain,
! [B: term,A: term > $o] :
( ~ $true
| ~ ( A @ ( sub @ ( sk1 @ A ) @ sh ) )
| ~ ( var @ B )
| ( A @ B )
| ( ( var @ one )
!= ( A @ one ) ) ),
inference(paramod_ordered,[status(thm)],[5,20]) ).
thf(38,plain,
! [B: term,A: term > $o] :
( ~ ( A @ ( sub @ ( sk1 @ A ) @ sh ) )
| ~ ( var @ B )
| ( A @ B )
| ( ( var @ one )
!= ( A @ one ) ) ),
inference(simp,[status(thm)],[37]) ).
thf(84,plain,
! [B: term,A: term > $o] :
( ( ( sub @ ( sk1 @ A ) @ sh )
!= ( sub @ ( sk1 @ ( (=) @ term @ ( sub @ ( sk1 @ A ) @ sh ) ) ) @ sh ) )
| ~ ( var @ B )
| ( ( sub @ ( sk1 @ A ) @ sh )
= B )
| ( ( var @ one )
!= ( ( sub @ ( sk1 @ A ) @ sh )
= one ) ) ),
inference(replace_leibeq,[status(thm)],[38:[bind(A,$thf( (=) @ term @ ( sub @ ( sk1 @ A ) @ sh ) ))]]) ).
thf(92,plain,
! [B: term,A: term > $o] :
( ( ( sub @ ( sk1 @ A ) @ sh )
!= ( sub @ ( sk1 @ ( (=) @ term @ ( sub @ ( sk1 @ A ) @ sh ) ) ) @ sh ) )
| ( ( sub @ ( sk1 @ A ) @ sh )
= B )
| ~ ( var @ B )
| ( ( var @ one )
!= ( ( sub @ ( sk1 @ A ) @ sh )
= one ) ) ),
inference(lifteq,[status(thm)],[84]) ).
thf(2851,plain,
! [B: term,A: term > $o] :
( ( ( sub @ ( sk1 @ A ) @ sh )
!= ( sub @ ( sk1 @ ( (=) @ term @ ( sub @ ( sk1 @ A ) @ sh ) ) ) @ sh ) )
| ( ( sub @ ( sk1 @ A ) @ sh )
= B )
| ~ ( var @ B )
| ( ( sub @ ( sk1 @ A ) @ sh )
!= one ) ),
inference(rewrite,[status(thm)],[92,5]) ).
thf(2852,plain,
! [B: term,A: term > $o] :
( ( ( sub @ ( sk1 @ A ) @ sh )
!= one )
| ( ( sub @ ( sk1 @ A ) @ sh )
!= ( sub @ ( sk1 @ ( (=) @ term @ ( sub @ ( sk1 @ A ) @ sh ) ) ) @ sh ) )
| ( ( sub @ ( sk1 @ A ) @ sh )
= B )
| ~ ( var @ B ) ),
inference(lifteq,[status(thm)],[2851]) ).
thf(1394,plain,
( ~ ( sk2 @ one )
| ~ $true
| ( ( sub @ ( sk1 @ sk2 ) @ sh )
!= one )
| ( ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
!= ( var @ one ) ) ),
inference(paramod_ordered,[status(thm)],[5,1187]) ).
thf(1395,plain,
( ~ ( sk2 @ one )
| ( ( sub @ ( sk1 @ sk2 ) @ sh )
!= one )
| ( ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
!= ( var @ one ) ) ),
inference(simp,[status(thm)],[1394]) ).
thf(1448,plain,
( ~ ( sk2 @ one )
| ( ( sub @ ( sk1 @ sk2 ) @ sh )
!= one )
| ( ( sub @ sk5 @ ( push @ sk3 @ sk4 ) )
!= one ) ),
inference(simp,[status(thm)],[1395]) ).
thf(2782,plain,
( ~ $true
| ( ( sub @ ( sk1 @ sk2 ) @ sh )
!= one )
| ( ( sub @ sk5 @ ( push @ sk3 @ sk4 ) )
!= one )
| ( ( sk2 @ sk3 )
!= ( sk2 @ one ) ) ),
inference(paramod_ordered,[status(thm)],[7,1448]) ).
thf(2783,plain,
( ( ( sub @ ( sk1 @ sk2 ) @ sh )
!= one )
| ( ( sub @ sk5 @ ( push @ sk3 @ sk4 ) )
!= one )
| ( ( sk2 @ sk3 )
!= ( sk2 @ one ) ) ),
inference(simp,[status(thm)],[2782]) ).
thf(2829,plain,
( ( ( sub @ ( sk1 @ sk2 ) @ sh )
!= one )
| ( ( sub @ sk5 @ ( push @ sk3 @ sk4 ) )
!= one )
| ( sk3 != one ) ),
inference(simp,[status(thm)],[2783]) ).
thf(1245,plain,
! [C: subst,B: term,A: subst] :
( ( ( sub @ one @ ( comp @ ( push @ B @ C ) @ A ) )
!= ( sub @ one @ sk4 ) )
| ( ( sub @ B @ A )
!= ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[813,226]) ).
thf(1246,plain,
! [A: subst] :
( ( sub @ one @ ( comp @ ( push @ sk5 @ A ) @ ( push @ sk3 @ sk4 ) ) )
!= ( sub @ one @ sk4 ) ),
inference(pattern_uni,[status(thm)],[1245:[bind(A,$thf( push @ sk3 @ sk4 )),bind(B,$thf( sk5 )),bind(C,$thf( C ))]]) ).
thf(1332,plain,
! [A: subst] :
( ( sub @ one @ ( comp @ ( push @ sk5 @ A ) @ ( push @ sk3 @ sk4 ) ) )
!= ( sub @ one @ sk4 ) ),
inference(simp,[status(thm)],[1246]) ).
thf(2572,plain,
! [C: subst,B: subst,A: term] :
( ( A
!= ( sub @ one @ sk4 ) )
| ( ( sub @ one @ ( push @ A @ B ) )
!= ( sub @ one @ ( comp @ ( push @ sk5 @ C ) @ ( push @ sk3 @ sk4 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,1332]) ).
thf(2580,plain,
! [B: subst,A: subst] :
( ( one != one )
| ( ( push @ ( sub @ one @ sk4 ) @ A )
!= ( comp @ ( push @ sk5 @ B ) @ ( push @ sk3 @ sk4 ) ) ) ),
inference(simp,[status(thm)],[2572]) ).
thf(2586,plain,
! [B: subst,A: subst] :
( ( push @ ( sub @ one @ sk4 ) @ A )
!= ( comp @ ( push @ sk5 @ B ) @ ( push @ sk3 @ sk4 ) ) ),
inference(simp,[status(thm)],[2580]) ).
thf(411,plain,
( ~ $true
| ( ( sk2 @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
!= ( sk2 @ ( sub @ sk5 @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[195,15]) ).
thf(412,plain,
( ( sk2 @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
!= ( sk2 @ ( sub @ sk5 @ sk4 ) ) ),
inference(simp,[status(thm)],[411]) ).
thf(419,plain,
( ( sub @ sk5 @ ( push @ sk3 @ sk4 ) )
!= ( sub @ sk5 @ sk4 ) ),
inference(simp,[status(thm)],[412]) ).
thf(1257,plain,
! [C: subst,B: term,A: subst] :
( ( ( sub @ one @ ( comp @ ( push @ B @ C ) @ A ) )
!= ( sub @ sk5 @ sk4 ) )
| ( ( sub @ B @ A )
!= ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[813,419]) ).
thf(1258,plain,
! [A: subst] :
( ( sub @ one @ ( comp @ ( push @ sk5 @ A ) @ ( push @ sk3 @ sk4 ) ) )
!= ( sub @ sk5 @ sk4 ) ),
inference(pattern_uni,[status(thm)],[1257:[bind(A,$thf( push @ sk3 @ sk4 )),bind(B,$thf( sk5 )),bind(C,$thf( C ))]]) ).
thf(1340,plain,
! [A: subst] :
( ( sub @ one @ ( comp @ ( push @ sk5 @ A ) @ ( push @ sk3 @ sk4 ) ) )
!= ( sub @ sk5 @ sk4 ) ),
inference(simp,[status(thm)],[1258]) ).
thf(3549,plain,
! [C: subst,B: subst,A: term] :
( ( A
!= ( sub @ sk5 @ sk4 ) )
| ( ( sub @ one @ ( push @ A @ B ) )
!= ( sub @ one @ ( comp @ ( push @ sk5 @ C ) @ ( push @ sk3 @ sk4 ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,1340]) ).
thf(3552,plain,
! [B: subst,A: subst] :
( ( one != one )
| ( ( push @ ( sub @ sk5 @ sk4 ) @ A )
!= ( comp @ ( push @ sk5 @ B ) @ ( push @ sk3 @ sk4 ) ) ) ),
inference(simp,[status(thm)],[3549]) ).
thf(3582,plain,
! [B: subst,A: subst] :
( ( push @ ( sub @ sk5 @ sk4 ) @ A )
!= ( comp @ ( push @ sk5 @ B ) @ ( push @ sk3 @ sk4 ) ) ),
inference(simp,[status(thm)],[3552]) ).
thf(4034,plain,
! [F: subst,E: term,D: subst,C: subst,B: term,A: subst] :
( ( B
= ( sub @ one @ ( comp @ ( push @ E @ F ) @ D ) ) )
| ( ( sub @ one @ ( comp @ ( push @ one @ A ) @ ( push @ B @ C ) ) )
!= ( sub @ E @ D ) ) ),
inference(paramod_ordered,[status(thm)],[1318,813]) ).
thf(4035,plain,
! [D: subst,C: term,B: subst,A: subst] :
( ( sub @ one @ ( comp @ ( push @ one @ A ) @ ( comp @ ( push @ one @ B ) @ ( push @ C @ D ) ) ) )
= C ),
inference(pattern_uni,[status(thm)],[4034:[bind(A,$thf( J )),bind(B,$thf( K )),bind(C,$thf( L )),bind(D,$thf( comp @ ( push @ one @ J ) @ ( push @ K @ L ) )),bind(E,$thf( one )),bind(F,$thf( F ))]]) ).
thf(4199,plain,
! [D: subst,C: term,B: subst,A: subst] :
( ( sub @ one @ ( comp @ ( push @ one @ A ) @ ( comp @ ( push @ one @ B ) @ ( push @ C @ D ) ) ) )
= C ),
inference(simp,[status(thm)],[4035]) ).
thf(1259,plain,
! [C: subst,B: term,A: subst] :
( ( ( sub @ B @ A )
!= ( sub @ sk5 @ sk4 ) )
| ( ( sub @ one @ ( comp @ ( push @ B @ C ) @ A ) )
!= ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[813,419]) ).
thf(1312,plain,
! [C: subst,B: term,A: subst] :
( ( B != sk5 )
| ( A != sk4 )
| ( ( sub @ one @ ( comp @ ( push @ B @ C ) @ A ) )
!= ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) ) ),
inference(simp,[status(thm)],[1259]) ).
thf(1335,plain,
! [A: subst] :
( ( sub @ one @ ( comp @ ( push @ sk5 @ A ) @ sk4 ) )
!= ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) ),
inference(simp,[status(thm)],[1312]) ).
thf(2608,plain,
! [C: subst,B: subst,A: term] :
( ( A
!= ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
| ( ( sub @ one @ ( push @ A @ B ) )
!= ( sub @ one @ ( comp @ ( push @ sk5 @ C ) @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,1335]) ).
thf(2622,plain,
! [B: subst,A: subst] :
( ( one != one )
| ( ( push @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) @ A )
!= ( comp @ ( push @ sk5 @ B ) @ sk4 ) ) ),
inference(simp,[status(thm)],[2608]) ).
thf(2646,plain,
! [B: subst,A: subst] :
( ( push @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) @ A )
!= ( comp @ ( push @ sk5 @ B ) @ sk4 ) ),
inference(simp,[status(thm)],[2622]) ).
thf(33,plain,
! [B: term,A: term > $o] :
( ~ ( A @ one )
| ( A @ ( sk1 @ A ) )
| ~ ( var @ B )
| ( A @ B ) ),
inference(simp,[status(thm)],[8]) ).
thf(2565,plain,
! [C: subst,B: subst,A: term] :
( ( ( sub @ one @ B )
!= ( sub @ one @ sk4 ) )
| ( ( comp @ sh @ ( push @ A @ B ) )
!= ( comp @ ( push @ sk5 @ C ) @ ( push @ sk3 @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[32,1332]) ).
thf(2573,plain,
! [C: subst,B: subst,A: term] :
( ( one != one )
| ( B != sk4 )
| ( ( comp @ sh @ ( push @ A @ B ) )
!= ( comp @ ( push @ sk5 @ C ) @ ( push @ sk3 @ sk4 ) ) ) ),
inference(simp,[status(thm)],[2565]) ).
thf(2588,plain,
! [B: subst,A: term] :
( ( comp @ sh @ ( push @ A @ sk4 ) )
!= ( comp @ ( push @ sk5 @ B ) @ ( push @ sk3 @ sk4 ) ) ),
inference(simp,[status(thm)],[2573]) ).
thf(6677,plain,
! [A: subst] :
( ( comp @ ( push @ sk5 @ A ) @ ( push @ sk3 @ sk4 ) )
!= sk4 ),
inference(rewrite,[status(thm)],[2588,32]) ).
thf(76,plain,
( ( one != one )
| ( one
!= ( sub @ ( sk1 @ ( (=) @ term @ one ) ) @ sh ) )
| ( one = sk5 ) ),
inference(replace_leibeq,[status(thm)],[56:[bind(A,$thf( (=) @ term @ one ))]]) ).
thf(102,plain,
( ( one != one )
| ( ( sub @ ( sk1 @ ( (=) @ term @ one ) ) @ sh )
!= one )
| ( sk5 = one ) ),
inference(lifteq,[status(thm)],[76]) ).
thf(153,plain,
( ( ( sub @ ( sk1 @ ( (=) @ term @ one ) ) @ sh )
!= one )
| ( sk5 = one ) ),
inference(simp,[status(thm)],[102]) ).
thf(701,plain,
( ( sub @ ( sk1 @ ( (=) @ term @ one ) ) @ sh )
!= one ),
inference(simplifyReflect,[status(thm)],[153,700]) ).
thf(742,plain,
! [B: subst,A: term] :
( ( A != one )
| ( ( sub @ one @ ( push @ A @ B ) )
!= ( sub @ ( sk1 @ ( (=) @ term @ one ) ) @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[19,701]) ).
thf(744,plain,
! [A: subst] :
( ( ( sk1 @ ( (=) @ term @ one ) )
!= one )
| ( ( push @ one @ A )
!= sh ) ),
inference(simp,[status(thm)],[742]) ).
thf(746,plain,
! [A: subst] :
( ( ( sk1 @ ( (=) @ term @ one ) )
!= one )
| ( ( push @ one @ A )
!= sh ) ),
inference(simp,[status(thm)],[744]) ).
thf(1110,plain,
! [A: subst] :
( ( one != one )
| ( ( push @ one @ A )
!= sh ) ),
inference(rewrite,[status(thm)],[746,1095]) ).
thf(1111,plain,
! [A: subst] :
( ( push @ one @ A )
!= sh ),
inference(simp,[status(thm)],[1110]) ).
thf(3633,plain,
( ~ $true
| ( ( sub @ ( sk1 @ sk2 ) @ sh )
!= one )
| ( sk3 != one )
| ( ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
!= ( var @ sk5 ) ) ),
inference(paramod_ordered,[status(thm)],[13,1454]) ).
thf(3634,plain,
( ( ( sub @ ( sk1 @ sk2 ) @ sh )
!= one )
| ( sk3 != one )
| ( ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
!= ( var @ sk5 ) ) ),
inference(simp,[status(thm)],[3633]) ).
thf(3656,plain,
( ( ( sub @ ( sk1 @ sk2 ) @ sh )
!= one )
| ( sk3 != one )
| ( ( sub @ sk5 @ ( push @ sk3 @ sk4 ) )
!= sk5 ) ),
inference(simp,[status(thm)],[3634]) ).
thf(1158,plain,
( ~ ( sk2 @ one )
| ~ $true
| ~ ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
| ( ( sk2 @ ( sub @ ( sk1 @ sk2 ) @ sh ) )
!= ( sk2 @ sk3 ) ) ),
inference(paramod_ordered,[status(thm)],[7,129]) ).
thf(1159,plain,
( ~ ( sk2 @ one )
| ~ ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
| ( ( sk2 @ ( sub @ ( sk1 @ sk2 ) @ sh ) )
!= ( sk2 @ sk3 ) ) ),
inference(simp,[status(thm)],[1158]) ).
thf(1188,plain,
( ~ ( sk2 @ one )
| ~ ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
| ( ( sub @ ( sk1 @ sk2 ) @ sh )
!= sk3 ) ),
inference(simp,[status(thm)],[1159]) ).
thf(1495,plain,
( ~ $true
| ~ ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
| ( ( sub @ ( sk1 @ sk2 ) @ sh )
!= sk3 )
| ( ( sk2 @ sk3 )
!= ( sk2 @ one ) ) ),
inference(paramod_ordered,[status(thm)],[7,1188]) ).
thf(1496,plain,
( ~ ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
| ( ( sub @ ( sk1 @ sk2 ) @ sh )
!= sk3 )
| ( ( sk2 @ sk3 )
!= ( sk2 @ one ) ) ),
inference(simp,[status(thm)],[1495]) ).
thf(1539,plain,
( ~ ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
| ( ( sub @ ( sk1 @ sk2 ) @ sh )
!= sk3 )
| ( sk3 != one ) ),
inference(simp,[status(thm)],[1496]) ).
thf(1112,plain,
( ( sub @ one @ sh )
!= one ),
inference(rewrite,[status(thm)],[701,1095]) ).
thf(4020,plain,
! [C: subst,B: term,A: subst] :
( ( B != one )
| ( ( sub @ one @ ( comp @ ( push @ one @ A ) @ ( push @ B @ C ) ) )
!= ( sub @ one @ sh ) ) ),
inference(paramod_ordered,[status(thm)],[1318,1112]) ).
thf(4124,plain,
! [B: subst,A: subst] :
( ( one != one )
| ( ( comp @ ( push @ one @ A ) @ ( push @ one @ B ) )
!= sh ) ),
inference(simp,[status(thm)],[4020]) ).
thf(4176,plain,
! [B: subst,A: subst] :
( ( comp @ ( push @ one @ A ) @ ( push @ one @ B ) )
!= sh ),
inference(simp,[status(thm)],[4124]) ).
thf(5479,plain,
! [D: subst,C: subst,B: subst,A: term] :
( ( B != sh )
| ( ( comp @ sh @ ( push @ A @ B ) )
!= ( comp @ ( push @ one @ C ) @ ( push @ one @ D ) ) ) ),
inference(paramod_ordered,[status(thm)],[32,4176]) ).
thf(5482,plain,
! [C: subst,B: subst,A: term] :
( ( comp @ sh @ ( push @ A @ sh ) )
!= ( comp @ ( push @ one @ B ) @ ( push @ one @ C ) ) ),
inference(simp,[status(thm)],[5479]) ).
thf(5484,plain,
! [C: subst,B: subst,A: term] :
( ( comp @ sh @ ( push @ A @ sh ) )
!= ( comp @ ( push @ one @ B ) @ ( push @ one @ C ) ) ),
inference(simp,[status(thm)],[5482]) ).
thf(10122,plain,
! [B: subst,A: subst] :
( ( comp @ ( push @ one @ A ) @ ( push @ one @ B ) )
!= sh ),
inference(rewrite,[status(thm)],[5484,32]) ).
thf(72,plain,
! [B: term > term,A: term] :
( ~ ( var @ ( B @ one ) )
| ~ ( var
@ ( B
@ ( sub
@ ( sk1
@ ^ [C: term] : ( var @ ( B @ C ) ) )
@ sh ) ) )
| ~ ( var @ A )
| ( var @ ( B @ A ) ) ),
inference(prim_subst,[status(thm)],[20:[bind(A,$thf( ^ [D: term] : ( var @ ( C @ D ) ) ))]]) ).
thf(134,plain,
! [B: term > term,A: term] :
( ~ ( var @ ( B @ one ) )
| ~ ( var
@ ( B
@ ( sub
@ ( sk1
@ ^ [C: term] : ( var @ ( B @ C ) ) )
@ sh ) ) )
| ~ ( var @ A )
| ( var @ ( B @ A ) ) ),
inference(simp,[status(thm)],[72]) ).
thf(68,plain,
! [B: term,A: term > $o] :
( ~ ( A @ one )
| ~ ( A @ ( sub @ ( sk1 @ A ) @ sh ) )
| ~ ( var @ B )
| ( ( A @ B )
!= ( ~ ( A @ ( sub @ ( sk1 @ A ) @ sh ) ) ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[20]) ).
thf(128,plain,
! [B: term,A: term > $o] :
( ~ ( A @ one )
| ~ ( A @ ( sub @ ( sk1 @ A ) @ sh ) )
| ~ ( var @ B )
| ( ( A @ B )
!= ( ~ ( A @ ( sub @ ( sk1 @ A ) @ sh ) ) ) ) ),
inference(simp,[status(thm)],[68]) ).
thf(2524,plain,
! [C: subst,B: subst,A: term] :
( ( A
!= ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
| ( ( sub @ one @ ( push @ A @ B ) )
!= ( sub @ one @ ( comp @ ( push @ one @ C ) @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[19,1323]) ).
thf(2539,plain,
! [B: subst,A: subst] :
( ( one != one )
| ( ( push @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) @ A )
!= ( comp @ ( push @ one @ B ) @ sk4 ) ) ),
inference(simp,[status(thm)],[2524]) ).
thf(2556,plain,
! [B: subst,A: subst] :
( ( push @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) @ A )
!= ( comp @ ( push @ one @ B ) @ sk4 ) ),
inference(simp,[status(thm)],[2539]) ).
thf(2564,plain,
! [A: subst] :
( ( one != one )
| ( ( comp @ ( push @ sk5 @ A ) @ ( push @ sk3 @ sk4 ) )
!= sk4 ) ),
inference(simp,[status(thm)],[1332]) ).
thf(2585,plain,
! [A: subst] :
( ( comp @ ( push @ sk5 @ A ) @ ( push @ sk3 @ sk4 ) )
!= sk4 ),
inference(simp,[status(thm)],[2564]) ).
thf(44,plain,
! [D: term,C: term > $o,B: term,A: term > $o] :
( ~ ( A @ one )
| ~ ( A @ ( sub @ ( sk1 @ A ) @ sh ) )
| ~ ( var @ B )
| ~ $true
| ~ ( C @ ( sub @ ( sk1 @ C ) @ sh ) )
| ~ ( var @ D )
| ( C @ D )
| ( ( A @ B )
!= ( C @ one ) ) ),
inference(paramod_ordered,[status(thm)],[20,20]) ).
thf(45,plain,
! [D: term,C: term > $o,B: term,A: term > $o] :
( ~ ( A @ one )
| ~ ( A @ ( sub @ ( sk1 @ A ) @ sh ) )
| ~ ( var @ B )
| ~ ( C @ ( sub @ ( sk1 @ C ) @ sh ) )
| ~ ( var @ D )
| ( C @ D )
| ( ( A @ B )
!= ( C @ one ) ) ),
inference(simp,[status(thm)],[44]) ).
thf(117,plain,
! [D: term,C: term > $o,B: term,A: term > $o] :
( ~ ( A @ one )
| ~ ( A @ ( sub @ ( sk1 @ A ) @ sh ) )
| ~ ( var @ B )
| ~ ( C @ ( sub @ ( sk1 @ C ) @ sh ) )
| ~ ( var @ D )
| ( C @ D )
| ( ( A @ B )
!= ( C @ one ) ) ),
inference(pre_uni,[status(thm)],[45:[]]) ).
thf(118,plain,
! [D: term,C: term > $o,B: term,A: term > $o] :
( ( C @ D )
| ~ ( var @ D )
| ~ ( C @ ( sub @ ( sk1 @ C ) @ sh ) )
| ~ ( var @ B )
| ~ ( A @ ( sub @ ( sk1 @ A ) @ sh ) )
| ~ ( A @ one )
| ( ( A @ B )
!= ( C @ one ) ) ),
inference(pre_uni,[status(thm)],[117:[]]) ).
thf(1248,plain,
! [C: subst,B: term,A: subst] :
( ~ ( sk2 @ ( sub @ one @ ( comp @ ( push @ B @ C ) @ A ) ) )
| ( ( sub @ B @ A )
!= ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) ) ),
inference(paramod_ordered,[status(thm)],[813,15]) ).
thf(1249,plain,
! [A: subst] :
~ ( sk2 @ ( sub @ one @ ( comp @ ( push @ sk5 @ A ) @ ( push @ sk3 @ sk4 ) ) ) ),
inference(pattern_uni,[status(thm)],[1248:[bind(A,$thf( push @ sk3 @ sk4 )),bind(B,$thf( sk5 )),bind(C,$thf( C ))]]) ).
thf(1336,plain,
! [A: subst] :
~ ( sk2 @ ( sub @ one @ ( comp @ ( push @ sk5 @ A ) @ ( push @ sk3 @ sk4 ) ) ) ),
inference(simp,[status(thm)],[1249]) ).
thf(1997,plain,
! [B: subst,A: subst] :
( ~ $true
| ( ( sk2 @ ( sub @ one @ ( comp @ ( push @ sk5 @ A ) @ sk4 ) ) )
!= ( sk2 @ ( sub @ one @ ( comp @ ( push @ sk5 @ B ) @ ( push @ sk3 @ sk4 ) ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[1319,1336]) ).
thf(1998,plain,
! [B: subst,A: subst] :
( ( sk2 @ ( sub @ one @ ( comp @ ( push @ sk5 @ A ) @ sk4 ) ) )
!= ( sk2 @ ( sub @ one @ ( comp @ ( push @ sk5 @ B ) @ ( push @ sk3 @ sk4 ) ) ) ) ),
inference(simp,[status(thm)],[1997]) ).
thf(2029,plain,
! [B: subst,A: subst] :
( ( sub @ one @ ( comp @ ( push @ sk5 @ A ) @ sk4 ) )
!= ( sub @ one @ ( comp @ ( push @ sk5 @ B ) @ ( push @ sk3 @ sk4 ) ) ) ),
inference(simp,[status(thm)],[1998]) ).
thf(219,plain,
! [B: subst,A: term] :
( ( sk2 @ A )
| ( ( sub @ one @ ( push @ A @ B ) )
!= ( sub @ one @ sk4 ) ) ),
inference(paramod_ordered,[status(thm)],[19,186]) ).
thf(225,plain,
! [B: subst,A: term] :
( ( sk2 @ A )
| ( one != one )
| ( ( push @ A @ B )
!= sk4 ) ),
inference(simp,[status(thm)],[219]) ).
thf(230,plain,
! [B: subst,A: term] :
( ( sk2 @ A )
| ( ( push @ A @ B )
!= sk4 ) ),
inference(simp,[status(thm)],[225]) ).
thf(1133,plain,
( ~ ( sk2 @ one )
| ~ ( sk2 @ ( sub @ ( sk1 @ sk2 ) @ sh ) )
| ~ $true
| ( ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
!= ( var @ one ) ) ),
inference(paramod_ordered,[status(thm)],[5,129]) ).
thf(1134,plain,
( ~ ( sk2 @ one )
| ~ ( sk2 @ ( sub @ ( sk1 @ sk2 ) @ sh ) )
| ( ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
!= ( var @ one ) ) ),
inference(simp,[status(thm)],[1133]) ).
thf(1213,plain,
( ~ ( sk2 @ one )
| ~ ( sk2 @ ( sub @ ( sk1 @ sk2 ) @ sh ) )
| ( ( sub @ sk5 @ ( push @ sk3 @ sk4 ) )
!= one ) ),
inference(simp,[status(thm)],[1134]) ).
thf(1154,plain,
( ~ ( sk2 @ one )
| ~ ( sk2 @ ( sub @ ( sk1 @ sk2 ) @ sh ) )
| ~ $true
| ( ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
!= ( var @ sk5 ) ) ),
inference(paramod_ordered,[status(thm)],[13,129]) ).
thf(1155,plain,
( ~ ( sk2 @ one )
| ~ ( sk2 @ ( sub @ ( sk1 @ sk2 ) @ sh ) )
| ( ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
!= ( var @ sk5 ) ) ),
inference(simp,[status(thm)],[1154]) ).
thf(1208,plain,
( ~ ( sk2 @ one )
| ~ ( sk2 @ ( sub @ ( sk1 @ sk2 ) @ sh ) )
| ( ( sub @ sk5 @ ( push @ sk3 @ sk4 ) )
!= sk5 ) ),
inference(simp,[status(thm)],[1155]) ).
thf(13244,plain,
( ~ $true
| ( ( var
@ ( sk1
@ ^ [A: term] : ( sk2 @ ( sub @ A @ ( push @ sk3 @ sk4 ) ) ) ) )
!= ( var @ one ) ) ),
inference(paramod_ordered,[status(thm)],[5,13151]) ).
thf(13245,plain,
( ( var
@ ( sk1
@ ^ [A: term] : ( sk2 @ ( sub @ A @ ( push @ sk3 @ sk4 ) ) ) ) )
!= ( var @ one ) ),
inference(simp,[status(thm)],[13244]) ).
thf(13293,plain,
( ( sk1
@ ^ [A: term] : ( sk2 @ ( sub @ A @ ( push @ sk3 @ sk4 ) ) ) )
!= one ),
inference(simp,[status(thm)],[13245]) ).
thf(2538,plain,
! [B: subst,A: subst] :
( ( sub @ one @ ( push @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) @ A ) )
!= ( sub @ one @ ( comp @ ( push @ one @ B ) @ sk4 ) ) ),
inference(simp,[status(thm)],[2524]) ).
thf(2555,plain,
! [B: subst,A: subst] :
( ( sub @ one @ ( push @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) @ A ) )
!= ( sub @ one @ ( comp @ ( push @ one @ B ) @ sk4 ) ) ),
inference(simp,[status(thm)],[2538]) ).
thf(10788,plain,
! [A: subst] :
( ( sub @ sk5 @ ( push @ sk3 @ sk4 ) )
!= ( sub @ one @ ( comp @ ( push @ one @ A ) @ sk4 ) ) ),
inference(rewrite,[status(thm)],[2555,5819]) ).
thf(10639,plain,
! [B: subst,A: subst] :
( ( one != one )
| ( ( comp @ ( push @ sk5 @ A ) @ sk4 )
!= ( comp @ ( push @ sk5 @ B ) @ ( push @ sk3 @ sk4 ) ) ) ),
inference(simp,[status(thm)],[2029]) ).
thf(10724,plain,
! [B: subst,A: subst] :
( ( comp @ ( push @ sk5 @ A ) @ sk4 )
!= ( comp @ ( push @ sk5 @ B ) @ ( push @ sk3 @ sk4 ) ) ),
inference(simp,[status(thm)],[10639]) ).
thf(46,plain,
! [D: term,C: term > $o,B: term,A: term > $o] :
( ~ ( A @ one )
| ~ ( A @ ( sub @ ( sk1 @ A ) @ sh ) )
| ~ ( var @ B )
| ~ ( C @ one )
| ~ $true
| ~ ( var @ D )
| ( C @ D )
| ( ( A @ B )
!= ( C @ ( sub @ ( sk1 @ C ) @ sh ) ) ) ),
inference(paramod_ordered,[status(thm)],[20,20]) ).
thf(47,plain,
! [D: term,C: term > $o,B: term,A: term > $o] :
( ~ ( A @ one )
| ~ ( A @ ( sub @ ( sk1 @ A ) @ sh ) )
| ~ ( var @ B )
| ~ ( C @ one )
| ~ ( var @ D )
| ( C @ D )
| ( ( A @ B )
!= ( C @ ( sub @ ( sk1 @ C ) @ sh ) ) ) ),
inference(simp,[status(thm)],[46]) ).
thf(126,plain,
! [D: term,C: term > $o,B: term,A: term > $o] :
( ~ ( A @ one )
| ~ ( A @ ( sub @ ( sk1 @ A ) @ sh ) )
| ~ ( var @ B )
| ~ ( C @ one )
| ~ ( var @ D )
| ( C @ D )
| ( ( A @ B )
!= ( C @ ( sub @ ( sk1 @ C ) @ sh ) ) ) ),
inference(pre_uni,[status(thm)],[47:[]]) ).
thf(127,plain,
! [D: term,C: term > $o,B: term,A: term > $o] :
( ( C @ D )
| ~ ( var @ D )
| ~ ( C @ one )
| ~ ( var @ B )
| ~ ( A @ ( sub @ ( sk1 @ A ) @ sh ) )
| ~ ( A @ one )
| ( ( A @ B )
!= ( C @ ( sub @ ( sk1 @ C ) @ sh ) ) ) ),
inference(pre_uni,[status(thm)],[126:[]]) ).
thf(1476,plain,
( ~ ( sk2 @ one )
| ~ $true
| ( ( sub @ ( sk1 @ sk2 ) @ sh )
!= sk3 )
| ( ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
!= ( var @ one ) ) ),
inference(paramod_ordered,[status(thm)],[5,1188]) ).
thf(1477,plain,
( ~ ( sk2 @ one )
| ( ( sub @ ( sk1 @ sk2 ) @ sh )
!= sk3 )
| ( ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
!= ( var @ one ) ) ),
inference(simp,[status(thm)],[1476]) ).
thf(1538,plain,
( ~ ( sk2 @ one )
| ( ( sub @ ( sk1 @ sk2 ) @ sh )
!= sk3 )
| ( ( sub @ sk5 @ ( push @ sk3 @ sk4 ) )
!= one ) ),
inference(simp,[status(thm)],[1477]) ).
thf(85,plain,
! [D: term,C: term > $o,B: term,A: term > $o] :
( ~ ( A @ one )
| ~ ( A @ ( sub @ ( sk1 @ A ) @ sh ) )
| ~ ( var @ B )
| ( ( sub @ ( sk1 @ C ) @ sh )
!= ( sub @ ( sk1 @ ( (=) @ term @ ( sub @ ( sk1 @ C ) @ sh ) ) ) @ sh ) )
| ~ ( var @ D )
| ( ( sub @ ( sk1 @ C ) @ sh )
= D )
| ( ( A @ B )
!= ( ( sub @ ( sk1 @ C ) @ sh )
= one ) ) ),
inference(replace_leibeq,[status(thm)],[45:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( (=) @ term @ ( sub @ ( sk1 @ C ) @ sh ) ))]]) ).
thf(99,plain,
! [D: term,C: term > $o,B: term,A: term > $o] :
( ( ( sub @ ( sk1 @ C ) @ sh )
!= ( sub @ ( sk1 @ ( (=) @ term @ ( sub @ ( sk1 @ C ) @ sh ) ) ) @ sh ) )
| ( ( sub @ ( sk1 @ C ) @ sh )
= D )
| ~ ( A @ one )
| ~ ( A @ ( sub @ ( sk1 @ A ) @ sh ) )
| ~ ( var @ B )
| ~ ( var @ D )
| ( ( A @ B )
!= ( ( sub @ ( sk1 @ C ) @ sh )
= one ) ) ),
inference(lifteq,[status(thm)],[85]) ).
thf(2043,plain,
( ~ ( sk2 @ ( sub @ ( sk1 @ sk2 ) @ sh ) )
| ~ $true
| ( sk3 != one )
| ( ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
!= ( var @ one ) ) ),
inference(paramod_ordered,[status(thm)],[5,1199]) ).
thf(2044,plain,
( ~ ( sk2 @ ( sub @ ( sk1 @ sk2 ) @ sh ) )
| ( sk3 != one )
| ( ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
!= ( var @ one ) ) ),
inference(simp,[status(thm)],[2043]) ).
thf(2110,plain,
( ~ ( sk2 @ ( sub @ ( sk1 @ sk2 ) @ sh ) )
| ( sk3 != one )
| ( ( sub @ sk5 @ ( push @ sk3 @ sk4 ) )
!= one ) ),
inference(simp,[status(thm)],[2044]) ).
thf(13258,plain,
( ~ $true
| ( ( var
@ ( sk1
@ ^ [A: term] : ( sk2 @ ( sub @ A @ ( push @ sk3 @ sk4 ) ) ) ) )
!= ( var @ sk5 ) ) ),
inference(paramod_ordered,[status(thm)],[13,13151]) ).
thf(13259,plain,
( ( var
@ ( sk1
@ ^ [A: term] : ( sk2 @ ( sub @ A @ ( push @ sk3 @ sk4 ) ) ) ) )
!= ( var @ sk5 ) ),
inference(simp,[status(thm)],[13258]) ).
thf(13294,plain,
( ( sk1
@ ^ [A: term] : ( sk2 @ ( sub @ A @ ( push @ sk3 @ sk4 ) ) ) )
!= sk5 ),
inference(simp,[status(thm)],[13259]) ).
thf(1985,plain,
! [B: subst,A: subst] :
( ( one != one )
| ( ( push @ sk3 @ A )
!= ( comp @ ( push @ sk5 @ B ) @ ( push @ sk3 @ sk4 ) ) ) ),
inference(simp,[status(thm)],[1983]) ).
thf(1989,plain,
! [B: subst,A: subst] :
( ( push @ sk3 @ A )
!= ( comp @ ( push @ sk5 @ B ) @ ( push @ sk3 @ sk4 ) ) ),
inference(simp,[status(thm)],[1985]) ).
thf(433,plain,
( ( sk5 != sk5 )
| ( ( push @ sk3 @ sk4 )
!= sk4 ) ),
inference(simp,[status(thm)],[419]) ).
thf(437,plain,
( ( push @ sk3 @ sk4 )
!= sk4 ),
inference(simp,[status(thm)],[433]) ).
thf(1493,plain,
( ~ ( sk2 @ one )
| ~ $true
| ( ( sub @ ( sk1 @ sk2 ) @ sh )
!= sk3 )
| ( ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
!= ( var @ sk5 ) ) ),
inference(paramod_ordered,[status(thm)],[13,1188]) ).
thf(1494,plain,
( ~ ( sk2 @ one )
| ( ( sub @ ( sk1 @ sk2 ) @ sh )
!= sk3 )
| ( ( var @ ( sub @ sk5 @ ( push @ sk3 @ sk4 ) ) )
!= ( var @ sk5 ) ) ),
inference(simp,[status(thm)],[1493]) ).
thf(1537,plain,
( ~ ( sk2 @ one )
| ( ( sub @ ( sk1 @ sk2 ) @ sh )
!= sk3 )
| ( ( sub @ sk5 @ ( push @ sk3 @ sk4 ) )
!= sk5 ) ),
inference(simp,[status(thm)],[1494]) ).
thf(131,plain,
( ~ ( sk2 @ ( sub @ sk5 @ ( push @ one @ sk4 ) ) )
| ~ ( sk2
@ ( sub @ sk5
@ ( push
@ ( sub
@ ( sk1
@ ^ [A: term] : ( sk2 @ ( sub @ sk5 @ ( push @ A @ sk4 ) ) ) )
@ sh )
@ sk4 ) ) )
| ~ ( var @ sk3 ) ),
inference(pre_uni,[status(thm)],[62:[bind(A,$thf( ^ [C: term] : ( sk2 @ ( sub @ sk5 @ ( push @ C @ sk4 ) ) ) )),bind(B,$thf( sk3 ))]]) ).
thf(63,plain,
! [B: term,A: term > $o] :
( ~ ( A @ one )
| ~ ( var @ B )
| ( A @ B )
| ( ( A @ ( sub @ ( sk1 @ A ) @ sh ) )
!= ( A @ one ) )
| ~ $true ),
inference(eqfactor_ordered,[status(thm)],[20]) ).
thf(121,plain,
! [B: term,A: term > $o] :
( ~ ( A @ one )
| ~ ( var @ B )
| ( A @ B )
| ( ( A @ ( sub @ ( sk1 @ A ) @ sh ) )
!= ( A @ one ) ) ),
inference(pre_uni,[status(thm)],[63:[]]) ).
thf(122,plain,
! [B: term,A: term > $o] :
( ( A @ B )
| ~ ( var @ B )
| ~ ( A @ one )
| ( ( A @ ( sub @ ( sk1 @ A ) @ sh ) )
!= ( A @ one ) ) ),
inference(pre_uni,[status(thm)],[121:[]]) ).
thf(13302,plain,
( ( one != one )
| ( ( sk1
@ ^ [A: term] : ( sk2 @ ( sub @ A @ ( push @ sk3 @ sk4 ) ) ) )
!= ( sk1 @ ( (=) @ term @ one ) ) ) ),
inference(paramod_ordered,[status(thm)],[1095,13293]) ).
thf(13303,plain,
( ( sk1
@ ^ [A: term] : ( sk2 @ ( sub @ A @ ( push @ sk3 @ sk4 ) ) ) )
!= ( sk1 @ ( (=) @ term @ one ) ) ),
inference(simp,[status(thm)],[13302]) ).
thf(13311,plain,
( ( ^ [A: term] : ( sk2 @ ( sub @ A @ ( push @ sk3 @ sk4 ) ) ) )
!= ( (=) @ term @ one ) ),
inference(simp,[status(thm)],[13303]) ).
thf(14077,plain,
$false,
inference(e,[status(thm)],[5,56,1095,2561,8734,846,2559,2131,1454,110,13151,1323,1462,20,1319,2852,2829,5819,2586,3582,4199,2646,1199,21,33,6677,1111,3656,1539,13,129,10122,134,1187,128,1318,2556,2585,32,22,118,2029,1332,12990,419,230,7,4176,700,1112,1213,267,226,3,1208,13293,1340,10788,1188,10724,127,1317,1538,1336,99,1448,2110,813,26,186,36,13294,1989,195,437,1335,1537,131,15,122,13311]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG251^3 : TPTP v9.3.1. Bugfixed v5.2.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.09/0.22 % Computer : n026.cluster.edu
% 0.09/0.22 % Model : x86_64 x86_64
% 0.09/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.22 % Memory : 8046.5625MB
% 0.09/0.22 % OS : Linux 6.8.0-71-generic
% 0.09/0.22 % CPULimit : 300
% 0.09/0.22 % WCLimit : 300
% 0.09/0.22 % DateTime : Tue Sep 29 17:35:12 UTC 2026
% 0.09/0.22 % CPUTime :
% 0.09/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
% 1.02/0.80 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 2.02/1.18 % [INFO] Parsing done (375ms).
% 2.02/1.20 % [INFO] Running in sequential loop mode.
% 3.02/1.60 % [INFO] eprover registered as external prover.
% 3.23/1.60 % [INFO] Scanning for conjecture ...
% 4.35/2.08 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 4.35/2.11 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 4.35/2.11 % [INFO] Problem is higher-order (TPTP THF).
% 4.35/2.11 % [INFO] Type checking passed.
% 4.35/2.12 % [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 ...
% 57.15/17.54 % External prover 'e' found a proof!
% 57.15/17.54 % [INFO] Killing All external provers ...
% 57.15/17.54 % Time passed: 17182ms (effective reasoning time: 16336ms)
% 57.15/17.54 % 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)>
% 57.15/17.54 % Axioms used in derivation (0):
% 57.15/17.54 % No. of inferences in proof: 250
% 57.15/17.54 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 17182 ms resp. 16336 ms w/o parsing
% 57.75/17.68 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 57.75/17.68 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------