TPTP Problem File: SWX182^1.p
View Solutions
- Solve Problem
%------------------------------------------------------------------------------
% File : SWX182^1 : TPTP v9.3.0. Released v9.3.0.
% Domain : Software Verification
% Problem : Benchmark: SEV441^1, Active target: satisfying_the_induction_principle
% Version : Especial.
% English :
% Refs : [Kon26] Kondylidou (2026), Email to Geoff Sutcliffe
% Source : [Kon26]
% Names : ALG444^1__005__axclos.verify [Kon26]
% Status : Theorem
% Rating : 0.67 v9.3.0
% Syntax : Number of formulae : 35 ( 1 unt; 33 typ; 0 def)
% Number of atoms : 82 ( 51 equ; 0 cnn)
% Maximal formula atoms : 33 ( 41 avg)
% Number of connectives : 985 ( 227 ~; 218 |; 43 &; 493 @)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 17 avg)
% Number of types : 4 ( 2 usr)
% Number of type conns : 263 ( 263 >; 0 *; 0 +; 0 <<)
% Number of symbols : 32 ( 31 usr; 1 con; 0-3 aty)
% Number of variables : 315 ( 48 ^; 266 !; 1 ?; 315 :)
% SPC : TH0_THM_EQU_NAR
% Comments :
%------------------------------------------------------------------------------
thf(unsorted_type,type,
unsorted: $tType ).
thf(subrel_decl,type,
subrel: ( $i > $i > $o ) > ( $i > $i > $o ) > $o ).
thf(inv_decl,type,
inv: ( $i > $i > $o ) > $i > $i > $o ).
thf(idem_decl,type,
idem: ( ( $i > $i > $o ) > $i > $i > $o ) > $o ).
thf(infl_decl,type,
infl: ( ( $i > $i > $o ) > $i > $i > $o ) > $o ).
thf(mono_decl,type,
mono: ( ( $i > $i > $o ) > $i > $i > $o ) > $o ).
thf(refl_decl,type,
refl: ( $i > $i > $o ) > $o ).
thf(irrefl_decl,type,
irrefl: ( $i > $i > $o ) > $o ).
thf(rc_decl,type,
rc: ( $i > $i > $o ) > $i > $i > $o ).
thf(symm_decl,type,
symm: ( $i > $i > $o ) > $o ).
thf(antisymm_decl,type,
antisymm: ( $i > $i > $o ) > $o ).
thf(asymm_decl,type,
asymm: ( $i > $i > $o ) > $o ).
thf(sc_decl,type,
sc: ( $i > $i > $o ) > $i > $i > $o ).
thf(trans_decl,type,
trans: ( $i > $i > $o ) > $o ).
thf(tc_decl,type,
tc: ( $i > $i > $o ) > $i > $i > $o ).
thf(trc_decl,type,
trc: ( $i > $i > $o ) > $i > $i > $o ).
thf(trsc_decl,type,
trsc: ( $i > $i > $o ) > $i > $i > $o ).
thf(po_decl,type,
po: ( $i > $i > $o ) > $o ).
thf(so_decl,type,
so: ( $i > $i > $o ) > $o ).
thf(total_decl,type,
total: ( $i > $i > $o ) > $o ).
thf(term_decl,type,
term: ( $i > $i > $o ) > $o ).
thf(ind_decl,type,
ind: ( $i > $i > $o ) > $o ).
thf(innf_decl,type,
innf: ( $i > $i > $o ) > $i > $o ).
thf(nfof_decl,type,
nfof: ( $i > $i > $o ) > $i > $i > $o ).
thf(norm_decl,type,
norm: ( $i > $i > $o ) > $o ).
thf(join_decl,type,
join: ( $i > $i > $o ) > $i > $i > $o ).
thf(lconfl_decl,type,
lconfl: ( $i > $i > $o ) > $o ).
thf(sconfl_decl,type,
sconfl: ( $i > $i > $o ) > $o ).
thf(confl_decl,type,
confl: ( $i > $i > $o ) > $o ).
thf(cr_decl,type,
cr: ( $i > $i > $o ) > $o ).
%----Types of the domains
thf(d_unsorted_type,type,
d_unsorted: $tType ).
%----Types of the promotion functions
thf(d2unsorted_decl,type,
d2unsorted: d_unsorted > $i ).
%----Types of the domain elements
thf(d_unsorted_0_decl,type,
d_unsorted_0: d_unsorted ).
thf(sev441_1,axiom,
( ! [U: $i] :
? [DU: d_unsorted] :
( U
= ( d2unsorted @ DU ) )
& ! [DU: d_unsorted] : ( DU = d_unsorted_0 )
& ! [DU1: d_unsorted,DU2: d_unsorted] :
( ( ( d2unsorted @ DU1 )
= ( d2unsorted @ DU2 ) )
=> ( DU1 = DU2 ) )
& ( subrel
= ( ^ [R: $i > $i > $o,S: $i > $i > $o] :
! [X: $i,Y: $i] :
( ~ ( R @ X @ Y )
| ( S @ X @ Y ) ) ) )
& ( inv
= ( ^ [R: $i > $i > $o,X: $i,Y: $i] : ( R @ Y @ X ) ) )
& ( idem
= ( ^ [F: ( $i > $i > $o ) > $i > $i > $o] :
! [R: $i > $i > $o] :
( ( F @ R )
= ( F @ ( F @ R ) ) ) ) )
& ( infl
= ( ^ [F: ( $i > $i > $o ) > $i > $i > $o] :
! [R: $i > $i > $o,X: $i,Y: $i] :
( ~ ( R @ X @ Y )
| ( F @ R @ X @ Y ) ) ) )
& ( mono
= ( ^ [F: ( $i > $i > $o ) > $i > $i > $o] :
! [R: $i > $i > $o,S: $i > $i > $o,Bound_variable_510: $i,Bound_variable_512: $i] :
( ~ ! [X: $i,Y: $i] :
( ~ ( R @ X @ Y )
| ( S @ X @ Y ) )
| ~ ( F @ R @ Bound_variable_510 @ Bound_variable_512 )
| ( F @ S @ Bound_variable_510 @ Bound_variable_512 ) ) ) )
& ( refl
= ( ^ [R: $i > $i > $o] :
! [X: $i] : ( R @ X @ X ) ) )
& ( irrefl
= ( ^ [R: $i > $i > $o] :
! [X: $i] :
~ ( R @ X @ X ) ) )
& ( rc
= ( ^ [R: $i > $i > $o,X: $i,Y: $i] :
( ( X = Y )
| ( R @ X @ Y ) ) ) )
& ( symm
= ( ^ [R: $i > $i > $o] :
! [X: $i,Y: $i] :
( ~ ( R @ X @ Y )
| ( R @ Y @ X ) ) ) )
& ( antisymm
= ( ^ [R: $i > $i > $o] :
! [X: $i,Y: $i] :
( ~ ( R @ X @ Y )
| ~ ( R @ Y @ X )
| ( X = Y ) ) ) )
& ( asymm
= ( ^ [R: $i > $i > $o] :
! [X: $i,Y: $i] :
( ~ ( R @ X @ Y )
| ~ ( R @ Y @ X ) ) ) )
& ( sc
= ( ^ [R: $i > $i > $o,X: $i,Y: $i] :
( ( R @ Y @ X )
| ( R @ X @ Y ) ) ) )
& ( trans
= ( ^ [R: $i > $i > $o] :
! [X: $i,Y: $i,Z: $i] :
( ~ ( R @ X @ Y )
| ~ ( R @ Y @ Z )
| ( R @ X @ Z ) ) ) )
& ( tc
= ( ^ [R: $i > $i > $o,X: $i,Y: $i] :
! [S: $i > $i > $o] :
( ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Z: $i] :
( ~ ( S @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( S @ Bound_variable_674 @ Z )
| ( S @ Bound_variable_672 @ Z ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( S @ Bound_variable_661 @ Bound_variable_663 ) )
| ( S @ X @ Y ) ) ) )
& ( trc
= ( ^ [R: $i > $i > $o,Flatten_var_0: $i,Flatten_var_1: $i] :
( ( Flatten_var_0 = Flatten_var_1 )
| ! [S: $i > $i > $o] :
( ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Z: $i] :
( ~ ( S @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( S @ Bound_variable_674 @ Z )
| ( S @ Bound_variable_672 @ Z ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( S @ Bound_variable_661 @ Bound_variable_663 ) )
| ( S @ Flatten_var_0 @ Flatten_var_1 ) ) ) ) )
& ( trsc
= ( ^ [R: $i > $i > $o,Flatten_var_0: $i,Flatten_var_1: $i] :
( ( Flatten_var_0 = Flatten_var_1 )
| ! [S: $i > $i > $o] :
( ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Z: $i] :
( ~ ( S @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( S @ Bound_variable_674 @ Z )
| ( S @ Bound_variable_672 @ Z ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( S @ Bound_variable_661 @ Bound_variable_663 ) )
| ( S @ Flatten_var_1 @ Flatten_var_0 ) )
| ! [S: $i > $i > $o] :
( ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Z: $i] :
( ~ ( S @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( S @ Bound_variable_674 @ Z )
| ( S @ Bound_variable_672 @ Z ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( S @ Bound_variable_661 @ Bound_variable_663 ) )
| ( S @ Flatten_var_0 @ Flatten_var_1 ) ) ) ) )
& ( po
= ( ^ [R: $i > $i > $o] :
( ! [X: $i] : ( R @ X @ X )
& ! [X: $i,Y: $i] :
( ~ ( R @ X @ Y )
| ~ ( R @ Y @ X )
| ( X = Y ) )
& ! [X: $i,Y: $i,Z: $i] :
( ~ ( R @ X @ Y )
| ~ ( R @ Y @ Z )
| ( R @ X @ Z ) ) ) ) )
& ( so
= ( ^ [R: $i > $i > $o] :
( ! [X: $i,Y: $i] :
( ~ ( R @ X @ Y )
| ~ ( R @ Y @ X ) )
& ! [X: $i,Y: $i,Z: $i] :
( ~ ( R @ X @ Y )
| ~ ( R @ Y @ Z )
| ( R @ X @ Z ) ) ) ) )
& ( total
= ( ^ [R: $i > $i > $o] :
! [X: $i,Y: $i] :
( ( X = Y )
| ( R @ X @ Y )
| ( R @ Y @ X ) ) ) )
& ( term
= ( ^ [R: $i > $i > $o] :
! [A: $i > $o,Bound_variable_862: $i] :
( ~ ( A @ Bound_variable_862 )
| ~ ! [X: $i] :
( ~ ( A @ X )
| ~ ! [Y: $i] :
( ~ ( A @ Y )
| ~ ( R @ X @ Y ) ) ) ) ) )
& ( ind
= ( ^ [R: $i > $i > $o] :
! [P: $i > $o,Bound_variable_917: $i] :
( ~ ! [X: $i] :
( ~ ! [Y: $i] :
( ~ ! [S: $i > $i > $o] :
( ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Z: $i] :
( ~ ( S @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( S @ Bound_variable_674 @ Z )
| ( S @ Bound_variable_672 @ Z ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( S @ Bound_variable_661 @ Bound_variable_663 ) )
| ( S @ X @ Y ) )
| ( P @ Y ) )
| ( P @ X ) )
| ( P @ Bound_variable_917 ) ) ) )
& ( innf
= ( ^ [R: $i > $i > $o,X: $i] :
! [Y: $i] :
~ ( R @ X @ Y ) ) )
& ( nfof
= ( ^ [R: $i > $i > $o,X: $i,Y: $i] :
( ( ( X = Y )
| ! [S: $i > $i > $o] :
( ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Z: $i] :
( ~ ( S @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( S @ Bound_variable_674 @ Z )
| ( S @ Bound_variable_672 @ Z ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( S @ Bound_variable_661 @ Bound_variable_663 ) )
| ( S @ Y @ X ) ) )
& ! [Bound_variable_985: $i] :
~ ( R @ X @ Bound_variable_985 ) ) ) )
& ( norm
= ( ^ [R: $i > $i > $o] :
! [X: $i,Bound_variable_1075: $i] :
( ~ ( R @ X @ Bound_variable_1075 )
| ~ ! [Bound_variable_1049: $i] :
( ~ ! [S: $i > $i > $o] :
( ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Z: $i] :
( ~ ( S @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( S @ Bound_variable_674 @ Z )
| ( S @ Bound_variable_672 @ Z ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( S @ Bound_variable_661 @ Bound_variable_663 ) )
| ( S @ X @ Bound_variable_1049 ) )
| ~ ! [Bound_variable_985: $i] :
~ ( R @ Bound_variable_1049 @ Bound_variable_985 ) ) ) ) )
& ( join
= ( ^ [R: $i > $i > $o,X: $i,Y: $i] :
~ ( ( X != Y )
& ~ ! [S: $i > $i > $o] :
( ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Bound_variable_1125: $i] :
( ~ ( S @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( S @ Bound_variable_674 @ Bound_variable_1125 )
| ( S @ Bound_variable_672 @ Bound_variable_1125 ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( S @ Bound_variable_661 @ Bound_variable_663 ) )
| ( S @ Y @ X ) )
& ~ ! [S: $i > $i > $o] :
( ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Bound_variable_1106: $i] :
( ~ ( S @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( S @ Bound_variable_674 @ Bound_variable_1106 )
| ( S @ Bound_variable_672 @ Bound_variable_1106 ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( S @ Bound_variable_661 @ Bound_variable_663 ) )
| ( S @ X @ Y ) )
& ! [Bound_variable_1218: $i] :
( ~ ! [S: $i > $i > $o] :
( ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Bound_variable_1125: $i] :
( ~ ( S @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( S @ Bound_variable_674 @ Bound_variable_1125 )
| ( S @ Bound_variable_672 @ Bound_variable_1125 ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( S @ Bound_variable_661 @ Bound_variable_663 ) )
| ( S @ Y @ Bound_variable_1218 ) )
| ~ ! [S: $i > $i > $o] :
( ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Bound_variable_1106: $i] :
( ~ ( S @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( S @ Bound_variable_674 @ Bound_variable_1106 )
| ( S @ Bound_variable_672 @ Bound_variable_1106 ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( S @ Bound_variable_661 @ Bound_variable_663 ) )
| ( S @ X @ Bound_variable_1218 ) ) ) ) ) )
& ( lconfl
= ( ^ [R: $i > $i > $o] :
! [X: $i,Y: $i,Z: $i,Bound_variable_1293: $i > $i > $o,Bound_variable_1309: $i > $i > $o] :
( ~ ( R @ X @ Z )
| ~ ( R @ X @ Y )
| ( Y = Z )
| ~ ! [Bound_variable_1218: $i] :
( ~ ! [S: $i > $i > $o] :
( ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Bound_variable_1125: $i] :
( ~ ( S @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( S @ Bound_variable_674 @ Bound_variable_1125 )
| ( S @ Bound_variable_672 @ Bound_variable_1125 ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( S @ Bound_variable_661 @ Bound_variable_663 ) )
| ( S @ Y @ Bound_variable_1218 ) )
| ~ ! [S: $i > $i > $o] :
( ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Bound_variable_1106: $i] :
( ~ ( S @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( S @ Bound_variable_674 @ Bound_variable_1106 )
| ( S @ Bound_variable_672 @ Bound_variable_1106 ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( S @ Bound_variable_661 @ Bound_variable_663 ) )
| ( S @ Z @ Bound_variable_1218 ) ) )
| ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Bound_variable_1125: $i] :
( ~ ( Bound_variable_1293 @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( Bound_variable_1293 @ Bound_variable_674 @ Bound_variable_1125 )
| ( Bound_variable_1293 @ Bound_variable_672 @ Bound_variable_1125 ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( Bound_variable_1293 @ Bound_variable_661 @ Bound_variable_663 ) )
| ( Bound_variable_1293 @ Y @ Z )
| ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Bound_variable_1106: $i] :
( ~ ( Bound_variable_1309 @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( Bound_variable_1309 @ Bound_variable_674 @ Bound_variable_1106 )
| ( Bound_variable_1309 @ Bound_variable_672 @ Bound_variable_1106 ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( Bound_variable_1309 @ Bound_variable_661 @ Bound_variable_663 ) )
| ( Bound_variable_1309 @ Z @ Y ) ) ) )
& ( sconfl
= ( ^ [R: $i > $i > $o] :
! [X: $i,Y: $i,Z: $i,Bound_variable_1371: $i > $i > $o,Bound_variable_1387: $i > $i > $o] :
( ~ ( R @ X @ Z )
| ( ( X != Y )
& ~ ! [S: $i > $i > $o] :
( ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Bound_variable_1347: $i] :
( ~ ( S @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( S @ Bound_variable_674 @ Bound_variable_1347 )
| ( S @ Bound_variable_672 @ Bound_variable_1347 ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( S @ Bound_variable_661 @ Bound_variable_663 ) )
| ( S @ X @ Y ) ) )
| ( Y = Z )
| ~ ! [Bound_variable_1218: $i] :
( ~ ! [S: $i > $i > $o] :
( ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Bound_variable_1125: $i] :
( ~ ( S @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( S @ Bound_variable_674 @ Bound_variable_1125 )
| ( S @ Bound_variable_672 @ Bound_variable_1125 ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( S @ Bound_variable_661 @ Bound_variable_663 ) )
| ( S @ Y @ Bound_variable_1218 ) )
| ~ ! [S: $i > $i > $o] :
( ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Bound_variable_1106: $i] :
( ~ ( S @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( S @ Bound_variable_674 @ Bound_variable_1106 )
| ( S @ Bound_variable_672 @ Bound_variable_1106 ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( S @ Bound_variable_661 @ Bound_variable_663 ) )
| ( S @ Z @ Bound_variable_1218 ) ) )
| ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Bound_variable_1125: $i] :
( ~ ( Bound_variable_1371 @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( Bound_variable_1371 @ Bound_variable_674 @ Bound_variable_1125 )
| ( Bound_variable_1371 @ Bound_variable_672 @ Bound_variable_1125 ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( Bound_variable_1371 @ Bound_variable_661 @ Bound_variable_663 ) )
| ( Bound_variable_1371 @ Y @ Z )
| ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Bound_variable_1106: $i] :
( ~ ( Bound_variable_1387 @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( Bound_variable_1387 @ Bound_variable_674 @ Bound_variable_1106 )
| ( Bound_variable_1387 @ Bound_variable_672 @ Bound_variable_1106 ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( Bound_variable_1387 @ Bound_variable_661 @ Bound_variable_663 ) )
| ( Bound_variable_1387 @ Z @ Y ) ) ) )
& ( confl
= ( ^ [R: $i > $i > $o] :
! [X: $i,Y: $i,Z: $i,Bound_variable_1444: $i > $i > $o,Bound_variable_1460: $i > $i > $o] :
( ( ( X != Z )
& ~ ! [S: $i > $i > $o] :
( ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Bound_variable_1106: $i] :
( ~ ( S @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( S @ Bound_variable_674 @ Bound_variable_1106 )
| ( S @ Bound_variable_672 @ Bound_variable_1106 ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( S @ Bound_variable_661 @ Bound_variable_663 ) )
| ( S @ X @ Z ) ) )
| ( ( X != Y )
& ~ ! [S: $i > $i > $o] :
( ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Bound_variable_1422: $i] :
( ~ ( S @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( S @ Bound_variable_674 @ Bound_variable_1422 )
| ( S @ Bound_variable_672 @ Bound_variable_1422 ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( S @ Bound_variable_661 @ Bound_variable_663 ) )
| ( S @ X @ Y ) ) )
| ( Y = Z )
| ~ ! [Bound_variable_1218: $i] :
( ~ ! [S: $i > $i > $o] :
( ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Bound_variable_1125: $i] :
( ~ ( S @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( S @ Bound_variable_674 @ Bound_variable_1125 )
| ( S @ Bound_variable_672 @ Bound_variable_1125 ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( S @ Bound_variable_661 @ Bound_variable_663 ) )
| ( S @ Y @ Bound_variable_1218 ) )
| ~ ! [S: $i > $i > $o] :
( ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Bound_variable_1106: $i] :
( ~ ( S @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( S @ Bound_variable_674 @ Bound_variable_1106 )
| ( S @ Bound_variable_672 @ Bound_variable_1106 ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( S @ Bound_variable_661 @ Bound_variable_663 ) )
| ( S @ Z @ Bound_variable_1218 ) ) )
| ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Bound_variable_1125: $i] :
( ~ ( Bound_variable_1444 @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( Bound_variable_1444 @ Bound_variable_674 @ Bound_variable_1125 )
| ( Bound_variable_1444 @ Bound_variable_672 @ Bound_variable_1125 ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( Bound_variable_1444 @ Bound_variable_661 @ Bound_variable_663 ) )
| ( Bound_variable_1444 @ Y @ Z )
| ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Bound_variable_1106: $i] :
( ~ ( Bound_variable_1460 @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( Bound_variable_1460 @ Bound_variable_674 @ Bound_variable_1106 )
| ( Bound_variable_1460 @ Bound_variable_672 @ Bound_variable_1106 ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( Bound_variable_1460 @ Bound_variable_661 @ Bound_variable_663 ) )
| ( Bound_variable_1460 @ Z @ Y ) ) ) )
& ( cr
= ( ^ [R: $i > $i > $o] :
! [X: $i,Y: $i,Bound_variable_1522: $i > $i > $o,Bound_variable_1538: $i > $i > $o] :
( ( ( X != Y )
& ~ ! [S: $i > $i > $o] :
( ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Z: $i] :
( ~ ( S @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( S @ Bound_variable_674 @ Z )
| ( S @ Bound_variable_672 @ Z ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( S @ Bound_variable_661 @ Bound_variable_663 ) )
| ( S @ Y @ X ) )
& ~ ! [S: $i > $i > $o] :
( ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Z: $i] :
( ~ ( S @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( S @ Bound_variable_674 @ Z )
| ( S @ Bound_variable_672 @ Z ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( S @ Bound_variable_661 @ Bound_variable_663 ) )
| ( S @ X @ Y ) ) )
| ( X = Y )
| ~ ! [Bound_variable_1218: $i] :
( ~ ! [S: $i > $i > $o] :
( ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Bound_variable_1125: $i] :
( ~ ( S @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( S @ Bound_variable_674 @ Bound_variable_1125 )
| ( S @ Bound_variable_672 @ Bound_variable_1125 ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( S @ Bound_variable_661 @ Bound_variable_663 ) )
| ( S @ Y @ Bound_variable_1218 ) )
| ~ ! [S: $i > $i > $o] :
( ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Bound_variable_1106: $i] :
( ~ ( S @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( S @ Bound_variable_674 @ Bound_variable_1106 )
| ( S @ Bound_variable_672 @ Bound_variable_1106 ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( S @ Bound_variable_661 @ Bound_variable_663 ) )
| ( S @ X @ Bound_variable_1218 ) ) )
| ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Bound_variable_1125: $i] :
( ~ ( Bound_variable_1522 @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( Bound_variable_1522 @ Bound_variable_674 @ Bound_variable_1125 )
| ( Bound_variable_1522 @ Bound_variable_672 @ Bound_variable_1125 ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( Bound_variable_1522 @ Bound_variable_661 @ Bound_variable_663 ) )
| ( Bound_variable_1522 @ Y @ X )
| ~ ! [Bound_variable_672: $i,Bound_variable_674: $i,Bound_variable_1106: $i] :
( ~ ( Bound_variable_1538 @ Bound_variable_672 @ Bound_variable_674 )
| ~ ( Bound_variable_1538 @ Bound_variable_674 @ Bound_variable_1106 )
| ( Bound_variable_1538 @ Bound_variable_672 @ Bound_variable_1106 ) )
| ~ ! [Bound_variable_661: $i,Bound_variable_663: $i] :
( ~ ( R @ Bound_variable_661 @ Bound_variable_663 )
| ( Bound_variable_1538 @ Bound_variable_661 @ Bound_variable_663 ) )
| ( Bound_variable_1538 @ X @ Y ) ) ) ) ) ).
thf(satisfying_the_induction_principle,conjecture,
( ind
= ( ^ [R: $i > $i > $o] :
! [P: $i > $o] :
( ! [X: $i] :
( ! [Y: $i] :
( ( tc @ R @ X @ Y )
=> ( P @ Y ) )
=> ( P @ X ) )
=> ! [X: $i] : ( P @ X ) ) ) ) ).
%------------------------------------------------------------------------------