%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ALG258^1 : TPTP v9.2.0. Bugfixed v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Oct 9 01:12:13 PM UTC 2025
% Result : Theorem 94.30s 94.22s
% Output : Proof 94.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 70
% Syntax : Number of formulae : 183 ( 79 unt; 0 typ; 34 def)
% Number of atoms : 1270 ( 227 equ; 0 cnn)
% Maximal formula atoms : 73 ( 6 avg)
% Number of connectives : 1813 ( 165 ~; 111 |; 10 &;1202 @)
% ( 0 <=>; 316 =>; 1 <=; 0 <~>)
% Maximal formula depth : 40 ( 3 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 42 ( 42 >; 0 *; 0 +; 0 <<)
% Number of symbols : 90 ( 87 usr; 89 con; 0-2 aty)
% ( 8 !!; 0 ??; 0 @@+; 0 @@-)
% Number of variables : 482 ( 5 ^; 477 !; 0 ?; 482 :)
% Comments :
%------------------------------------------------------------------------------
thf(def_axapp,definition,
( axapp
= ( ! [X1: term,X2: term,X3: subst] :
( ( sub @ ( ap @ X1 @ X2 ) @ X3 )
= ( ap @ ( sub @ X1 @ X3 ) @ ( sub @ X2 @ X3 ) ) ) ) ) ).
thf(def_axvarcons,definition,
( axvarcons
= ( ! [X1: term,X2: subst] :
( ( sub @ one @ ( push @ X1 @ X2 ) )
= X1 ) ) ) ).
thf(def_axvarid,definition,
( axvarid
= ( ! [X1: term] :
( ( sub @ X1 @ id )
= X1 ) ) ) ).
thf(def_axabs,definition,
( axabs
= ( ! [X1: term,X2: subst] :
( ( sub @ ( lam @ X1 ) @ X2 )
= ( lam @ ( sub @ X1 @ ( push @ one @ ( comp @ X2 @ sh ) ) ) ) ) ) ) ).
thf(def_axclos,definition,
( axclos
= ( ! [X1: term,X2: subst,X3: subst] :
( ( sub @ ( sub @ X1 @ X2 ) @ X3 )
= ( sub @ X1 @ ( comp @ X2 @ X3 ) ) ) ) ) ).
thf(def_axidl,definition,
( axidl
= ( ! [X1: subst] :
( ( comp @ id @ X1 )
= X1 ) ) ) ).
thf(def_axshiftcons,definition,
( axshiftcons
= ( ! [X1: term,X2: subst] :
( ( comp @ sh @ ( push @ X1 @ X2 ) )
= X2 ) ) ) ).
thf(def_axassoc,definition,
( axassoc
= ( ! [X1: subst,X2: subst,X3: subst] :
( ( comp @ ( comp @ X1 @ X2 ) @ X3 )
= ( comp @ X1 @ ( comp @ X2 @ X3 ) ) ) ) ) ).
thf(def_axmap,definition,
( axmap
= ( ! [X1: term,X2: subst,X3: subst] :
( ( comp @ ( push @ X1 @ X2 ) @ X3 )
= ( push @ ( sub @ X1 @ X3 ) @ ( comp @ X2 @ X3 ) ) ) ) ) ).
thf(def_axidr,definition,
( axidr
= ( ! [X1: subst] :
( ( comp @ X1 @ id )
= X1 ) ) ) ).
thf(def_axvarshift,definition,
( axvarshift
= ( ( push @ one @ sh )
= id ) ) ).
thf(def_axscons,definition,
( axscons
= ( ! [X1: subst] :
( ( push @ ( sub @ one @ X1 ) @ ( comp @ sh @ X1 ) )
= X1 ) ) ) ).
thf(def_ulamvar1,definition,
( ulamvar1
= ( var @ one ) ) ).
thf(def_ulamvarsh,definition,
( ulamvarsh
= ( ! [X1: term] :
( ( var @ X1 )
=> ( var @ ( sub @ X1 @ sh ) ) ) ) ) ).
thf(def_ulamvarind,definition,
( ulamvarind
= ( ! [X1: term > $o] :
( ( X1 @ one )
=> ( ! [X2: term] :
( ( var @ X2 )
=> ( ( X1 @ X2 )
=> ( X1 @ ( sub @ X2 @ sh ) ) ) )
=> ! [X2: term] :
( ( var @ X2 )
=> ( X1 @ X2 ) ) ) ) ) ) ).
thf(def_apinj1,definition,
( apinj1
= ( ! [X1: term,X2: term,X3: term,X4: term] :
( ( ( ap @ X1 @ X3 )
= ( ap @ X2 @ X4 ) )
=> ( X1 = X2 ) ) ) ) ).
thf(def_apinj2,definition,
( apinj2
= ( ! [X1: term,X2: term,X3: term,X4: term] :
( ( ( ap @ X1 @ X3 )
= ( ap @ X2 @ X4 ) )
=> ( X3 = X4 ) ) ) ) ).
thf(def_laminj,definition,
( laminj
= ( ! [X1: term,X2: term] :
( ( ( lam @ X1 )
= ( lam @ X2 ) )
=> ( X1 = X2 ) ) ) ) ).
thf(def_shinj,definition,
( shinj
= ( ! [X1: term,X2: term] :
( ( ( sub @ X1 @ sh )
= ( sub @ X2 @ sh ) )
=> ( X1 = X2 ) ) ) ) ).
thf(def_lamnotap,definition,
( lamnotap
= ( ! [X1: term,X2: term,X3: term] :
( ( lam @ X1 )
!= ( ap @ X2 @ X3 ) ) ) ) ).
thf(def_apnotvar,definition,
( apnotvar
= ( ! [X1: term,X2: term] :
~ ( var @ ( ap @ X1 @ X2 ) ) ) ) ).
thf(def_lamnotvar,definition,
( lamnotvar
= ( ! [X1: term] :
~ ( var @ ( lam @ X1 ) ) ) ) ).
thf(def_induction,definition,
( induction
= ( ! [X1: term > $o] :
( ! [X2: term] :
( ( var @ X2 )
=> ( X1 @ X2 ) )
=> ( ! [X2: term,X3: term] :
( ( X1 @ X2 )
=> ( ( X1 @ X3 )
=> ( X1 @ ( ap @ X2 @ X3 ) ) ) )
=> ( ! [X2: term] :
( ( X1 @ X2 )
=> ( X1 @ ( lam @ X2 ) ) )
=> ( !! @ X1 ) ) ) ) ) ) ).
thf(def_pushprop,definition,
( pushprop
= ( ! [X1: term > $o,X2: term,X3: subst] :
( ! [X4: term] :
( ( var @ X4 )
=> ( X1 @ ( sub @ X4 @ X3 ) ) )
=> ( ( X1 @ X2 )
=> ! [X4: term] :
( ( var @ X4 )
=> ( X1 @ ( sub @ X4 @ ( push @ X2 @ X3 ) ) ) ) ) ) ) ) ).
thf(def_induction2lem,definition,
( induction2lem
= ( ! [X1: term > $o] :
( ! [X2: term,X3: term] :
( ( X1 @ X2 )
=> ( ( X1 @ X3 )
=> ( X1 @ ( ap @ X2 @ X3 ) ) ) )
=> ( ! [X2: term] :
( ! [X3: term] :
( ( X1 @ X3 )
=> ( X1 @ ( sub @ X2 @ ( push @ X3 @ id ) ) ) )
=> ( X1 @ ( lam @ X2 ) ) )
=> ! [X2: term,X3: subst] :
( ! [X4: term] :
( ( var @ X4 )
=> ( X1 @ ( sub @ X4 @ X3 ) ) )
=> ( X1 @ ( sub @ X2 @ X3 ) ) ) ) ) ) ) ).
thf(def_induction2,definition,
( induction2
= ( ! [X1: term > $o] :
( ! [X2: term] :
( ( var @ X2 )
=> ( X1 @ X2 ) )
=> ( ! [X2: term,X3: term] :
( ( X1 @ X2 )
=> ( ( X1 @ X3 )
=> ( X1 @ ( ap @ X2 @ X3 ) ) ) )
=> ( ! [X2: term] :
( ! [X3: term] :
( ( X1 @ X3 )
=> ( X1 @ ( sub @ X2 @ ( push @ X3 @ id ) ) ) )
=> ( X1 @ ( lam @ X2 ) ) )
=> ( !! @ X1 ) ) ) ) ) ) ).
thf(def_substmonoid,definition,
( substmonoid
= ( ~ ( ~ ( ! [X1: subst,X2: subst,X3: subst] :
( ( comp @ ( comp @ X1 @ X2 ) @ X3 )
= ( comp @ X1 @ ( comp @ X2 @ X3 ) ) )
=> ~ ! [X1: subst] :
( ( comp @ id @ X1 )
= X1 ) )
=> ~ ! [X1: subst] :
( ( comp @ X1 @ id )
= X1 ) ) ) ) ).
thf(def_termmset,definition,
( termmset
= ( ~ ( ! [X1: term,X2: subst,X3: subst] :
( ( sub @ ( sub @ X1 @ X2 ) @ X3 )
= ( sub @ X1 @ ( comp @ X2 @ X3 ) ) )
=> ~ ! [X1: term] :
( ( sub @ X1 @ id )
= X1 ) ) ) ) ).
thf(def_hoasap,definition,
( hoasap
= ( ^ [X1: subst,X2: term,X3: subst] : ( ap @ ( sub @ X2 @ X3 ) ) ) ) ).
thf(def_hoaslam,definition,
( hoaslam
= ( ^ [X1: subst,X2: subst > term > term] : ( lam @ ( X2 @ sh @ one ) ) ) ) ).
thf(def_hoasapinj1,definition,
( hoasapinj1
= ( ! [X1: term,X2: term,X3: term,X4: term] :
( ( ( hoasap @ id @ X1 @ id @ X3 )
= ( hoasap @ id @ X2 @ id @ X4 ) )
=> ( X1 = X2 ) ) ) ) ).
thf(def_hoasapinj2,definition,
( hoasapinj2
= ( ! [X1: term,X2: term,X3: term,X4: term] :
( ( ( hoasap @ id @ X1 @ id @ X3 )
= ( hoasap @ id @ X2 @ id @ X4 ) )
=> ( X3 = X4 ) ) ) ) ).
thf(def_hoaslaminj,definition,
( hoaslaminj
= ( ! [X1: subst > term > term] :
( ! [X2: subst,X3: term,X4: subst] :
( ( sub @ ( X1 @ X2 @ X3 ) @ X4 )
= ( X1 @ ( comp @ X2 @ X4 ) @ ( sub @ X3 @ X4 ) ) )
=> ! [X2: subst > term > term] :
( ! [X3: subst,X4: term,X5: subst] :
( ( sub @ ( X2 @ X3 @ X4 ) @ X5 )
= ( X2 @ ( comp @ X3 @ X5 ) @ ( sub @ X4 @ X5 ) ) )
=> ( ( ( hoaslam @ id @ X1 )
= ( hoaslam @ id @ X2 ) )
=> ! [X3: subst,X4: term] :
( ( X1 @ X3 @ X4 )
= ( X2 @ X3 @ X4 ) ) ) ) ) ) ) ).
thf(def_hoaslaminj_gthm,definition,
( hoaslaminj_gthm
= ( axapp
=> ( axvarcons
=> ( axvarid
=> ( axabs
=> ( axclos
=> ( axidl
=> ( axshiftcons
=> ( axassoc
=> ( axmap
=> ( axidr
=> ( axvarshift
=> ( axscons
=> ( ulamvar1
=> ( ulamvarsh
=> ( ulamvarind
=> ( apinj1
=> ( apinj2
=> ( laminj
=> ( shinj
=> ( lamnotap
=> ( apnotvar
=> ( lamnotvar
=> ( induction
=> ( pushprop
=> ( induction2lem
=> ( induction2
=> ( substmonoid
=> ( termmset
=> ( hoasapinj1
=> ( hoasapinj2
=> hoaslaminj ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ).
thf(thm,conjecture,
( ! [X1: term,X2: term,X3: subst] :
( ( sub @ ( ap @ X1 @ X2 ) @ X3 )
= ( ap @ ( sub @ X1 @ X3 ) @ ( sub @ X2 @ X3 ) ) )
=> ( ! [X1: term,X2: subst] :
( ( sub @ one @ ( push @ X1 @ X2 ) )
= X1 )
=> ( ! [X1: term] :
( ( sub @ X1 @ id )
= X1 )
=> ( ! [X1: term,X2: subst] :
( ( sub @ ( lam @ X1 ) @ X2 )
= ( lam @ ( sub @ X1 @ ( push @ one @ ( comp @ X2 @ sh ) ) ) ) )
=> ( ! [X1: term,X2: subst,X3: subst] :
( ( sub @ ( sub @ X1 @ X2 ) @ X3 )
= ( sub @ X1 @ ( comp @ X2 @ X3 ) ) )
=> ( ! [X1: subst] :
( ( comp @ id @ X1 )
= X1 )
=> ( ! [X1: term,X2: subst] :
( ( comp @ sh @ ( push @ X1 @ X2 ) )
= X2 )
=> ( ! [X1: subst,X2: subst,X3: subst] :
( ( comp @ ( comp @ X1 @ X2 ) @ X3 )
= ( comp @ X1 @ ( comp @ X2 @ X3 ) ) )
=> ( ! [X1: term,X2: subst,X3: subst] :
( ( comp @ ( push @ X1 @ X2 ) @ X3 )
= ( push @ ( sub @ X1 @ X3 ) @ ( comp @ X2 @ X3 ) ) )
=> ( ! [X1: subst] :
( ( comp @ X1 @ id )
= X1 )
=> ( ( ( push @ one @ sh )
= id )
=> ( ! [X1: subst] :
( ( push @ ( sub @ one @ X1 ) @ ( comp @ sh @ X1 ) )
= X1 )
=> ( ( var @ one )
=> ( ! [X1: term] :
( ( var @ X1 )
=> ( var @ ( sub @ X1 @ sh ) ) )
=> ( ! [X1: term > $o] :
( ( X1 @ one )
=> ( ! [X2: term] :
( ( var @ X2 )
=> ( ( X1 @ X2 )
=> ( X1 @ ( sub @ X2 @ sh ) ) ) )
=> ! [X2: term] :
( ( var @ X2 )
=> ( X1 @ X2 ) ) ) )
=> ( ! [X1: term,X2: term,X3: term,X4: term] :
( ( ( ap @ X1 @ X3 )
= ( ap @ X2 @ X4 ) )
=> ( X1 = X2 ) )
=> ( ! [X1: term,X2: term,X3: term,X4: term] :
( ( ( ap @ X1 @ X3 )
= ( ap @ X2 @ X4 ) )
=> ( X3 = X4 ) )
=> ( ! [X1: term,X2: term] :
( ( ( lam @ X1 )
= ( lam @ X2 ) )
=> ( X1 = X2 ) )
=> ( ! [X1: term,X2: term] :
( ( ( sub @ X1 @ sh )
= ( sub @ X2 @ sh ) )
=> ( X1 = X2 ) )
=> ( ! [X1: term,X2: term,X3: term] :
( ( lam @ X1 )
!= ( ap @ X2 @ X3 ) )
=> ( ! [X1: term,X2: term] :
~ ( var @ ( ap @ X1 @ X2 ) )
=> ( ! [X1: term] :
~ ( var @ ( lam @ X1 ) )
=> ( ! [X1: term > $o] :
( ! [X2: term] :
( ( var @ X2 )
=> ( X1 @ X2 ) )
=> ( ! [X2: term,X3: term] :
( ( X1 @ X2 )
=> ( ( X1 @ X3 )
=> ( X1 @ ( ap @ X2 @ X3 ) ) ) )
=> ( ! [X2: term] :
( ( X1 @ X2 )
=> ( X1 @ ( lam @ X2 ) ) )
=> ( !! @ X1 ) ) ) )
=> ( ! [X1: term > $o,X2: term,X3: subst] :
( ! [X4: term] :
( ( var @ X4 )
=> ( X1 @ ( sub @ X4 @ X3 ) ) )
=> ( ( X1 @ X2 )
=> ! [X4: term] :
( ( var @ X4 )
=> ( X1 @ ( sub @ X4 @ ( push @ X2 @ X3 ) ) ) ) ) )
=> ( ! [X1: term > $o] :
( ! [X2: term,X3: term] :
( ( X1 @ X2 )
=> ( ( X1 @ X3 )
=> ( X1 @ ( ap @ X2 @ X3 ) ) ) )
=> ( ! [X2: term] :
( ! [X3: term] :
( ( X1 @ X3 )
=> ( X1 @ ( sub @ X2 @ ( push @ X3 @ id ) ) ) )
=> ( X1 @ ( lam @ X2 ) ) )
=> ! [X2: term,X3: subst] :
( ! [X4: term] :
( ( var @ X4 )
=> ( X1 @ ( sub @ X4 @ X3 ) ) )
=> ( X1 @ ( sub @ X2 @ X3 ) ) ) ) )
=> ( ! [X1: term > $o] :
( ! [X2: term] :
( ( var @ X2 )
=> ( X1 @ X2 ) )
=> ( ! [X2: term,X3: term] :
( ( X1 @ X2 )
=> ( ( X1 @ X3 )
=> ( X1 @ ( ap @ X2 @ X3 ) ) ) )
=> ( ! [X2: term] :
( ! [X3: term] :
( ( X1 @ X3 )
=> ( X1 @ ( sub @ X2 @ ( push @ X3 @ id ) ) ) )
=> ( X1 @ ( lam @ X2 ) ) )
=> ( !! @ X1 ) ) ) )
=> ( ~ ( ~ ( ! [X1: subst,X2: subst,X3: subst] :
( ( comp @ ( comp @ X1 @ X2 ) @ X3 )
= ( comp @ X1 @ ( comp @ X2 @ X3 ) ) )
=> ~ ! [X1: subst] :
( ( comp @ id @ X1 )
= X1 ) )
=> ~ ! [X1: subst] :
( ( comp @ X1 @ id )
= X1 ) )
=> ( ~ ( ! [X1: term,X2: subst,X3: subst] :
( ( sub @ ( sub @ X1 @ X2 ) @ X3 )
= ( sub @ X1 @ ( comp @ X2 @ X3 ) ) )
=> ~ ! [X1: term] :
( ( sub @ X1 @ id )
= X1 ) )
=> ( ! [X1: term,X2: term,X3: term,X4: term] :
( ( ( ap @ ( sub @ X1 @ id ) @ X3 )
= ( ap @ ( sub @ X2 @ id ) @ X4 ) )
=> ( X1 = X2 ) )
=> ( ! [X1: term,X2: term,X3: term,X4: term] :
( ( ( ap @ ( sub @ X1 @ id ) @ X3 )
= ( ap @ ( sub @ X2 @ id ) @ X4 ) )
=> ( X3 = X4 ) )
=> ! [X1: subst > term > term] :
( ! [X2: subst,X3: term,X4: subst] :
( ( sub @ ( X1 @ X2 @ X3 ) @ X4 )
= ( X1 @ ( comp @ X2 @ X4 ) @ ( sub @ X3 @ X4 ) ) )
=> ! [X2: subst > term > term] :
( ! [X3: subst,X4: term,X5: subst] :
( ( sub @ ( X2 @ X3 @ X4 ) @ X5 )
= ( X2 @ ( comp @ X3 @ X5 ) @ ( sub @ X4 @ X5 ) ) )
=> ( ( ( lam @ ( X1 @ sh @ one ) )
= ( lam @ ( X2 @ sh @ one ) ) )
=> ! [X3: subst,X4: term] :
( ( X1 @ X3 @ X4 )
= ( X2 @ X3 @ X4 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ).
thf(h0,negated_conjecture,
~ ( ! [X1: term,X2: term,X3: subst] :
( ( sub @ ( ap @ X1 @ X2 ) @ X3 )
= ( ap @ ( sub @ X1 @ X3 ) @ ( sub @ X2 @ X3 ) ) )
=> ( ! [X1: term,X2: subst] :
( ( sub @ one @ ( push @ X1 @ X2 ) )
= X1 )
=> ( ! [X1: term] :
( ( sub @ X1 @ id )
= X1 )
=> ( ! [X1: term,X2: subst] :
( ( sub @ ( lam @ X1 ) @ X2 )
= ( lam @ ( sub @ X1 @ ( push @ one @ ( comp @ X2 @ sh ) ) ) ) )
=> ( ! [X1: term,X2: subst,X3: subst] :
( ( sub @ ( sub @ X1 @ X2 ) @ X3 )
= ( sub @ X1 @ ( comp @ X2 @ X3 ) ) )
=> ( ! [X1: subst] :
( ( comp @ id @ X1 )
= X1 )
=> ( ! [X1: term,X2: subst] :
( ( comp @ sh @ ( push @ X1 @ X2 ) )
= X2 )
=> ( ! [X1: subst,X2: subst,X3: subst] :
( ( comp @ ( comp @ X1 @ X2 ) @ X3 )
= ( comp @ X1 @ ( comp @ X2 @ X3 ) ) )
=> ( ! [X1: term,X2: subst,X3: subst] :
( ( comp @ ( push @ X1 @ X2 ) @ X3 )
= ( push @ ( sub @ X1 @ X3 ) @ ( comp @ X2 @ X3 ) ) )
=> ( ! [X1: subst] :
( ( comp @ X1 @ id )
= X1 )
=> ( ( ( push @ one @ sh )
= id )
=> ( ! [X1: subst] :
( ( push @ ( sub @ one @ X1 ) @ ( comp @ sh @ X1 ) )
= X1 )
=> ( ( var @ one )
=> ( ! [X1: term] :
( ( var @ X1 )
=> ( var @ ( sub @ X1 @ sh ) ) )
=> ( ! [X1: term > $o] :
( ( X1 @ one )
=> ( ! [X2: term] :
( ( var @ X2 )
=> ( ( X1 @ X2 )
=> ( X1 @ ( sub @ X2 @ sh ) ) ) )
=> ! [X2: term] :
( ( var @ X2 )
=> ( X1 @ X2 ) ) ) )
=> ( ! [X1: term,X2: term,X3: term,X4: term] :
( ( ( ap @ X1 @ X3 )
= ( ap @ X2 @ X4 ) )
=> ( X1 = X2 ) )
=> ( ! [X1: term,X2: term,X3: term,X4: term] :
( ( ( ap @ X1 @ X3 )
= ( ap @ X2 @ X4 ) )
=> ( X3 = X4 ) )
=> ( ! [X1: term,X2: term] :
( ( ( lam @ X1 )
= ( lam @ X2 ) )
=> ( X1 = X2 ) )
=> ( ! [X1: term,X2: term] :
( ( ( sub @ X1 @ sh )
= ( sub @ X2 @ sh ) )
=> ( X1 = X2 ) )
=> ( ! [X1: term,X2: term,X3: term] :
( ( lam @ X1 )
!= ( ap @ X2 @ X3 ) )
=> ( ! [X1: term,X2: term] :
~ ( var @ ( ap @ X1 @ X2 ) )
=> ( ! [X1: term] :
~ ( var @ ( lam @ X1 ) )
=> ( ! [X1: term > $o] :
( ! [X2: term] :
( ( var @ X2 )
=> ( X1 @ X2 ) )
=> ( ! [X2: term,X3: term] :
( ( X1 @ X2 )
=> ( ( X1 @ X3 )
=> ( X1 @ ( ap @ X2 @ X3 ) ) ) )
=> ( ! [X2: term] :
( ( X1 @ X2 )
=> ( X1 @ ( lam @ X2 ) ) )
=> ( !! @ X1 ) ) ) )
=> ( ! [X1: term > $o,X2: term,X3: subst] :
( ! [X4: term] :
( ( var @ X4 )
=> ( X1 @ ( sub @ X4 @ X3 ) ) )
=> ( ( X1 @ X2 )
=> ! [X4: term] :
( ( var @ X4 )
=> ( X1 @ ( sub @ X4 @ ( push @ X2 @ X3 ) ) ) ) ) )
=> ( ! [X1: term > $o] :
( ! [X2: term,X3: term] :
( ( X1 @ X2 )
=> ( ( X1 @ X3 )
=> ( X1 @ ( ap @ X2 @ X3 ) ) ) )
=> ( ! [X2: term] :
( ! [X3: term] :
( ( X1 @ X3 )
=> ( X1 @ ( sub @ X2 @ ( push @ X3 @ id ) ) ) )
=> ( X1 @ ( lam @ X2 ) ) )
=> ! [X2: term,X3: subst] :
( ! [X4: term] :
( ( var @ X4 )
=> ( X1 @ ( sub @ X4 @ X3 ) ) )
=> ( X1 @ ( sub @ X2 @ X3 ) ) ) ) )
=> ( ! [X1: term > $o] :
( ! [X2: term] :
( ( var @ X2 )
=> ( X1 @ X2 ) )
=> ( ! [X2: term,X3: term] :
( ( X1 @ X2 )
=> ( ( X1 @ X3 )
=> ( X1 @ ( ap @ X2 @ X3 ) ) ) )
=> ( ! [X2: term] :
( ! [X3: term] :
( ( X1 @ X3 )
=> ( X1 @ ( sub @ X2 @ ( push @ X3 @ id ) ) ) )
=> ( X1 @ ( lam @ X2 ) ) )
=> ( !! @ X1 ) ) ) )
=> ( ~ ( ~ ( ! [X1: subst,X2: subst,X3: subst] :
( ( comp @ ( comp @ X1 @ X2 ) @ X3 )
= ( comp @ X1 @ ( comp @ X2 @ X3 ) ) )
=> ~ ! [X1: subst] :
( ( comp @ id @ X1 )
= X1 ) )
=> ~ ! [X1: subst] :
( ( comp @ X1 @ id )
= X1 ) )
=> ( ~ ( ! [X1: term,X2: subst,X3: subst] :
( ( sub @ ( sub @ X1 @ X2 ) @ X3 )
= ( sub @ X1 @ ( comp @ X2 @ X3 ) ) )
=> ~ ! [X1: term] :
( ( sub @ X1 @ id )
= X1 ) )
=> ( ! [X1: term,X2: term,X3: term,X4: term] :
( ( ( ap @ ( sub @ X1 @ id ) @ X3 )
= ( ap @ ( sub @ X2 @ id ) @ X4 ) )
=> ( X1 = X2 ) )
=> ( ! [X1: term,X2: term,X3: term,X4: term] :
( ( ( ap @ ( sub @ X1 @ id ) @ X3 )
= ( ap @ ( sub @ X2 @ id ) @ X4 ) )
=> ( X3 = X4 ) )
=> ! [X1: subst > term > term] :
( ! [X2: subst,X3: term,X4: subst] :
( ( sub @ ( X1 @ X2 @ X3 ) @ X4 )
= ( X1 @ ( comp @ X2 @ X4 ) @ ( sub @ X3 @ X4 ) ) )
=> ! [X2: subst > term > term] :
( ! [X3: subst,X4: term,X5: subst] :
( ( sub @ ( X2 @ X3 @ X4 ) @ X5 )
= ( X2 @ ( comp @ X3 @ X5 ) @ ( sub @ X4 @ X5 ) ) )
=> ( ( ( lam @ ( X1 @ sh @ one ) )
= ( lam @ ( X2 @ sh @ one ) ) )
=> ! [X3: subst,X4: term] :
( ( X1 @ X3 @ X4 )
= ( X2 @ X3 @ X4 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(assume_negation,[status(cth)],[thm]) ).
thf(ax1261,axiom,
( p1
| ~ p3 ),
file('<stdin>',ax1261) ).
thf(ax1263,axiom,
~ p1,
file('<stdin>',ax1263) ).
thf(ax1259,axiom,
( p3
| ~ p5 ),
file('<stdin>',ax1259) ).
thf(ax1257,axiom,
( p5
| ~ p7 ),
file('<stdin>',ax1257) ).
thf(ax1255,axiom,
( p7
| ~ p9 ),
file('<stdin>',ax1255) ).
thf(ax1253,axiom,
( p9
| ~ p11 ),
file('<stdin>',ax1253) ).
thf(ax1251,axiom,
( p11
| ~ p13 ),
file('<stdin>',ax1251) ).
thf(ax1249,axiom,
( p13
| ~ p15 ),
file('<stdin>',ax1249) ).
thf(ax1247,axiom,
( p15
| ~ p17 ),
file('<stdin>',ax1247) ).
thf(ax1245,axiom,
( p17
| ~ p19 ),
file('<stdin>',ax1245) ).
thf(ax1243,axiom,
( p19
| ~ p21 ),
file('<stdin>',ax1243) ).
thf(ax1241,axiom,
( p21
| ~ p23 ),
file('<stdin>',ax1241) ).
thf(ax1239,axiom,
( p23
| ~ p25 ),
file('<stdin>',ax1239) ).
thf(ax1237,axiom,
( p25
| ~ p27 ),
file('<stdin>',ax1237) ).
thf(ax1235,axiom,
( p27
| ~ p29 ),
file('<stdin>',ax1235) ).
thf(ax1233,axiom,
( p29
| ~ p31 ),
file('<stdin>',ax1233) ).
thf(ax1231,axiom,
( p31
| ~ p33 ),
file('<stdin>',ax1231) ).
thf(ax1229,axiom,
( p33
| ~ p35 ),
file('<stdin>',ax1229) ).
thf(ax1227,axiom,
( p35
| ~ p37 ),
file('<stdin>',ax1227) ).
thf(ax1225,axiom,
( p37
| ~ p39 ),
file('<stdin>',ax1225) ).
thf(ax1223,axiom,
( p39
| ~ p41 ),
file('<stdin>',ax1223) ).
thf(ax1221,axiom,
( p41
| ~ p43 ),
file('<stdin>',ax1221) ).
thf(ax1219,axiom,
( p43
| ~ p45 ),
file('<stdin>',ax1219) ).
thf(ax1217,axiom,
( p45
| ~ p47 ),
file('<stdin>',ax1217) ).
thf(ax1215,axiom,
( p47
| ~ p49 ),
file('<stdin>',ax1215) ).
thf(ax1213,axiom,
( p49
| ~ p51 ),
file('<stdin>',ax1213) ).
thf(ax1211,axiom,
( p51
| ~ p53 ),
file('<stdin>',ax1211) ).
thf(pax36,axiom,
( p36
=> ! [X155: term,X156: term] :
( ( ( flam @ X155 )
= ( flam @ X156 ) )
=> ( X155 = X156 ) ) ),
file('<stdin>',pax36) ).
thf(ax1228,axiom,
( p35
| p36 ),
file('<stdin>',ax1228) ).
thf(nax53,axiom,
( p53
<= ( ~ ( ~ ( ! [X144: subst,X145: subst,X142: subst] :
( ( fcomp @ ( fcomp @ X144 @ X145 ) @ X142 )
= ( fcomp @ X144 @ ( fcomp @ X145 @ X142 ) ) )
=> ~ ! [X144: subst] :
( ( fcomp @ fid @ X144 )
= X144 ) )
=> ~ ! [X144: subst] :
( ( fcomp @ X144 @ fid )
= X144 ) )
=> ( ~ ( ! [X146: term,X145: subst,X142: subst] :
( ( fsub @ ( fsub @ X146 @ X145 ) @ X142 )
= ( fsub @ X146 @ ( fcomp @ X145 @ X142 ) ) )
=> ~ ! [X146: term] :
( ( fsub @ X146 @ fid )
= X146 ) )
=> ( ! [X146: term,X147: term,X148: term,X143: term] :
( ( ( fap @ ( fsub @ X146 @ fid ) @ X148 )
= ( fap @ ( fsub @ X147 @ fid ) @ X143 ) )
=> ( X146 = X147 ) )
=> ( ! [X146: term,X147: term,X148: term,X143: term] :
( ( ( fap @ ( fsub @ X146 @ fid ) @ X148 )
= ( fap @ ( fsub @ X147 @ fid ) @ X143 ) )
=> ( X148 = X143 ) )
=> ! [X149: subst > term > term] :
( ! [X150: subst,X148: term,X151: subst] :
( ( fsub @ ( X149 @ X150 @ X148 ) @ X151 )
= ( X149 @ ( fcomp @ X150 @ X151 ) @ ( fsub @ X148 @ X151 ) ) )
=> ! [X152: subst > term > term] :
( ! [X153: subst,X154: term,X70: subst] :
( ( fsub @ ( X152 @ X153 @ X154 ) @ X70 )
= ( X152 @ ( fcomp @ X153 @ X70 ) @ ( fsub @ X154 @ X70 ) ) )
=> ( ( ( flam @ ( X149 @ fsh @ fone ) )
= ( flam @ ( X152 @ fsh @ fone ) ) )
=> ! [X153: subst,X154: term] :
( ( X149 @ X153 @ X154 )
= ( X152 @ X153 @ X154 ) ) ) ) ) ) ) ) ) ),
file('<stdin>',nax53) ).
thf(pax4,axiom,
( p4
=> ! [X165: term,X160: subst] :
( ( fsub @ fone @ ( fpush @ X165 @ X160 ) )
= X165 ) ),
file('<stdin>',pax4) ).
thf(ax1260,axiom,
( p3
| p4 ),
file('<stdin>',ax1260) ).
thf(pax14,axiom,
( p14
=> ! [X163: term,X160: subst] :
( ( fcomp @ fsh @ ( fpush @ X163 @ X160 ) )
= X160 ) ),
file('<stdin>',pax14) ).
thf(ax1250,axiom,
( p13
| p14 ),
file('<stdin>',ax1250) ).
thf(c_0_34,plain,
( p1
| ~ p3 ),
inference(fof_simplification,[status(thm)],[ax1261]) ).
thf(c_0_35,plain,
~ p1,
inference(fof_simplification,[status(thm)],[ax1263]) ).
thf(c_0_36,plain,
( p3
| ~ p5 ),
inference(fof_simplification,[status(thm)],[ax1259]) ).
thf(c_0_37,plain,
( p1
| ~ p3 ),
inference(split_conjunct,[status(thm)],[c_0_34]) ).
thf(c_0_38,plain,
~ p1,
inference(split_conjunct,[status(thm)],[c_0_35]) ).
thf(c_0_39,plain,
( p5
| ~ p7 ),
inference(fof_simplification,[status(thm)],[ax1257]) ).
thf(c_0_40,plain,
( p3
| ~ p5 ),
inference(split_conjunct,[status(thm)],[c_0_36]) ).
thf(c_0_41,plain,
~ p3,
inference(sr,[status(thm)],[c_0_37,c_0_38]) ).
thf(c_0_42,plain,
( p7
| ~ p9 ),
inference(fof_simplification,[status(thm)],[ax1255]) ).
thf(c_0_43,plain,
( p5
| ~ p7 ),
inference(split_conjunct,[status(thm)],[c_0_39]) ).
thf(c_0_44,plain,
~ p5,
inference(sr,[status(thm)],[c_0_40,c_0_41]) ).
thf(c_0_45,plain,
( p9
| ~ p11 ),
inference(fof_simplification,[status(thm)],[ax1253]) ).
thf(c_0_46,plain,
( p7
| ~ p9 ),
inference(split_conjunct,[status(thm)],[c_0_42]) ).
thf(c_0_47,plain,
~ p7,
inference(sr,[status(thm)],[c_0_43,c_0_44]) ).
thf(c_0_48,plain,
( p11
| ~ p13 ),
inference(fof_simplification,[status(thm)],[ax1251]) ).
thf(c_0_49,plain,
( p9
| ~ p11 ),
inference(split_conjunct,[status(thm)],[c_0_45]) ).
thf(c_0_50,plain,
~ p9,
inference(sr,[status(thm)],[c_0_46,c_0_47]) ).
thf(c_0_51,plain,
( p13
| ~ p15 ),
inference(fof_simplification,[status(thm)],[ax1249]) ).
thf(c_0_52,plain,
( p11
| ~ p13 ),
inference(split_conjunct,[status(thm)],[c_0_48]) ).
thf(c_0_53,plain,
~ p11,
inference(sr,[status(thm)],[c_0_49,c_0_50]) ).
thf(c_0_54,plain,
( p15
| ~ p17 ),
inference(fof_simplification,[status(thm)],[ax1247]) ).
thf(c_0_55,plain,
( p13
| ~ p15 ),
inference(split_conjunct,[status(thm)],[c_0_51]) ).
thf(c_0_56,plain,
~ p13,
inference(sr,[status(thm)],[c_0_52,c_0_53]) ).
thf(c_0_57,plain,
( p17
| ~ p19 ),
inference(fof_simplification,[status(thm)],[ax1245]) ).
thf(c_0_58,plain,
( p15
| ~ p17 ),
inference(split_conjunct,[status(thm)],[c_0_54]) ).
thf(c_0_59,plain,
~ p15,
inference(sr,[status(thm)],[c_0_55,c_0_56]) ).
thf(c_0_60,plain,
( p19
| ~ p21 ),
inference(fof_simplification,[status(thm)],[ax1243]) ).
thf(c_0_61,plain,
( p17
| ~ p19 ),
inference(split_conjunct,[status(thm)],[c_0_57]) ).
thf(c_0_62,plain,
~ p17,
inference(sr,[status(thm)],[c_0_58,c_0_59]) ).
thf(c_0_63,plain,
( p21
| ~ p23 ),
inference(fof_simplification,[status(thm)],[ax1241]) ).
thf(c_0_64,plain,
( p19
| ~ p21 ),
inference(split_conjunct,[status(thm)],[c_0_60]) ).
thf(c_0_65,plain,
~ p19,
inference(sr,[status(thm)],[c_0_61,c_0_62]) ).
thf(c_0_66,plain,
( p23
| ~ p25 ),
inference(fof_simplification,[status(thm)],[ax1239]) ).
thf(c_0_67,plain,
( p21
| ~ p23 ),
inference(split_conjunct,[status(thm)],[c_0_63]) ).
thf(c_0_68,plain,
~ p21,
inference(sr,[status(thm)],[c_0_64,c_0_65]) ).
thf(c_0_69,plain,
( p25
| ~ p27 ),
inference(fof_simplification,[status(thm)],[ax1237]) ).
thf(c_0_70,plain,
( p23
| ~ p25 ),
inference(split_conjunct,[status(thm)],[c_0_66]) ).
thf(c_0_71,plain,
~ p23,
inference(sr,[status(thm)],[c_0_67,c_0_68]) ).
thf(c_0_72,plain,
( p27
| ~ p29 ),
inference(fof_simplification,[status(thm)],[ax1235]) ).
thf(c_0_73,plain,
( p25
| ~ p27 ),
inference(split_conjunct,[status(thm)],[c_0_69]) ).
thf(c_0_74,plain,
~ p25,
inference(sr,[status(thm)],[c_0_70,c_0_71]) ).
thf(c_0_75,plain,
( p29
| ~ p31 ),
inference(fof_simplification,[status(thm)],[ax1233]) ).
thf(c_0_76,plain,
( p27
| ~ p29 ),
inference(split_conjunct,[status(thm)],[c_0_72]) ).
thf(c_0_77,plain,
~ p27,
inference(sr,[status(thm)],[c_0_73,c_0_74]) ).
thf(c_0_78,plain,
( p31
| ~ p33 ),
inference(fof_simplification,[status(thm)],[ax1231]) ).
thf(c_0_79,plain,
( p29
| ~ p31 ),
inference(split_conjunct,[status(thm)],[c_0_75]) ).
thf(c_0_80,plain,
~ p29,
inference(sr,[status(thm)],[c_0_76,c_0_77]) ).
thf(c_0_81,plain,
( p33
| ~ p35 ),
inference(fof_simplification,[status(thm)],[ax1229]) ).
thf(c_0_82,plain,
( p31
| ~ p33 ),
inference(split_conjunct,[status(thm)],[c_0_78]) ).
thf(c_0_83,plain,
~ p31,
inference(sr,[status(thm)],[c_0_79,c_0_80]) ).
thf(c_0_84,plain,
( p35
| ~ p37 ),
inference(fof_simplification,[status(thm)],[ax1227]) ).
thf(c_0_85,plain,
( p33
| ~ p35 ),
inference(split_conjunct,[status(thm)],[c_0_81]) ).
thf(c_0_86,plain,
~ p33,
inference(sr,[status(thm)],[c_0_82,c_0_83]) ).
thf(c_0_87,plain,
( p37
| ~ p39 ),
inference(fof_simplification,[status(thm)],[ax1225]) ).
thf(c_0_88,plain,
( p35
| ~ p37 ),
inference(split_conjunct,[status(thm)],[c_0_84]) ).
thf(c_0_89,plain,
~ p35,
inference(sr,[status(thm)],[c_0_85,c_0_86]) ).
thf(c_0_90,plain,
( p39
| ~ p41 ),
inference(fof_simplification,[status(thm)],[ax1223]) ).
thf(c_0_91,plain,
( p37
| ~ p39 ),
inference(split_conjunct,[status(thm)],[c_0_87]) ).
thf(c_0_92,plain,
~ p37,
inference(sr,[status(thm)],[c_0_88,c_0_89]) ).
thf(c_0_93,plain,
( p41
| ~ p43 ),
inference(fof_simplification,[status(thm)],[ax1221]) ).
thf(c_0_94,plain,
( p39
| ~ p41 ),
inference(split_conjunct,[status(thm)],[c_0_90]) ).
thf(c_0_95,plain,
~ p39,
inference(sr,[status(thm)],[c_0_91,c_0_92]) ).
thf(c_0_96,plain,
( p43
| ~ p45 ),
inference(fof_simplification,[status(thm)],[ax1219]) ).
thf(c_0_97,plain,
( p41
| ~ p43 ),
inference(split_conjunct,[status(thm)],[c_0_93]) ).
thf(c_0_98,plain,
~ p41,
inference(sr,[status(thm)],[c_0_94,c_0_95]) ).
thf(c_0_99,plain,
( p45
| ~ p47 ),
inference(fof_simplification,[status(thm)],[ax1217]) ).
thf(c_0_100,plain,
( p43
| ~ p45 ),
inference(split_conjunct,[status(thm)],[c_0_96]) ).
thf(c_0_101,plain,
~ p43,
inference(sr,[status(thm)],[c_0_97,c_0_98]) ).
thf(c_0_102,plain,
( p47
| ~ p49 ),
inference(fof_simplification,[status(thm)],[ax1215]) ).
thf(c_0_103,plain,
( p45
| ~ p47 ),
inference(split_conjunct,[status(thm)],[c_0_99]) ).
thf(c_0_104,plain,
~ p45,
inference(sr,[status(thm)],[c_0_100,c_0_101]) ).
thf(c_0_105,plain,
( p49
| ~ p51 ),
inference(fof_simplification,[status(thm)],[ax1213]) ).
thf(c_0_106,plain,
( p47
| ~ p49 ),
inference(split_conjunct,[status(thm)],[c_0_102]) ).
thf(c_0_107,plain,
~ p47,
inference(sr,[status(thm)],[c_0_103,c_0_104]) ).
thf(c_0_108,plain,
( p51
| ~ p53 ),
inference(fof_simplification,[status(thm)],[ax1211]) ).
thf(c_0_109,plain,
( p49
| ~ p51 ),
inference(split_conjunct,[status(thm)],[c_0_105]) ).
thf(c_0_110,plain,
~ p49,
inference(sr,[status(thm)],[c_0_106,c_0_107]) ).
thf(c_0_111,plain,
! [X1887: term,X1888: term] :
( ~ p36
| ( ( flam @ X1887 )
!= ( flam @ X1888 ) )
| ( X1887 = X1888 ) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax36])])]) ).
thf(c_0_112,plain,
( p35
| p36 ),
inference(split_conjunct,[status(thm)],[ax1228]) ).
thf(c_0_113,plain,
! [X1844: subst,X1845: subst,X1846: subst,X1847: subst,X1848: subst,X1849: term,X1850: subst,X1851: subst,X1852: term,X1853: term,X1854: term,X1855: term,X1856: term,X1857: term,X1858: term,X1859: term,X1860: term,X1862: subst,X1863: term,X1864: subst,X1866: subst,X1867: term,X1868: subst] :
( ( ( ( fcomp @ ( fcomp @ X1844 @ X1845 ) @ X1846 )
= ( fcomp @ X1844 @ ( fcomp @ X1845 @ X1846 ) ) )
| p53 )
& ( ( ( fcomp @ fid @ X1847 )
= X1847 )
| p53 )
& ( ( ( fcomp @ X1848 @ fid )
= X1848 )
| p53 )
& ( ( ( fsub @ ( fsub @ X1849 @ X1850 ) @ X1851 )
= ( fsub @ X1849 @ ( fcomp @ X1850 @ X1851 ) ) )
| p53 )
& ( ( ( fsub @ X1852 @ fid )
= X1852 )
| p53 )
& ( ( ( fap @ ( fsub @ X1853 @ fid ) @ X1855 )
!= ( fap @ ( fsub @ X1854 @ fid ) @ X1856 ) )
| ( X1853 = X1854 )
| p53 )
& ( ( ( fap @ ( fsub @ X1857 @ fid ) @ X1859 )
!= ( fap @ ( fsub @ X1858 @ fid ) @ X1860 ) )
| ( X1859 = X1860 )
| p53 )
& ( ( ( fsub @ ( esk849_0 @ X1862 @ X1863 ) @ X1864 )
= ( esk849_0 @ ( fcomp @ X1862 @ X1864 ) @ ( fsub @ X1863 @ X1864 ) ) )
| p53 )
& ( ( ( fsub @ ( esk850_0 @ X1866 @ X1867 ) @ X1868 )
= ( esk850_0 @ ( fcomp @ X1866 @ X1868 ) @ ( fsub @ X1867 @ X1868 ) ) )
| p53 )
& ( ( ( flam @ ( esk849_0 @ fsh @ fone ) )
= ( flam @ ( esk850_0 @ fsh @ fone ) ) )
| p53 )
& ( ( ( esk849_0 @ esk851_0 @ esk852_0 )
!= ( esk850_0 @ esk851_0 @ esk852_0 ) )
| p53 ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax53])])])])])]) ).
thf(c_0_114,plain,
( p51
| ~ p53 ),
inference(split_conjunct,[status(thm)],[c_0_108]) ).
thf(c_0_115,plain,
~ p51,
inference(sr,[status(thm)],[c_0_109,c_0_110]) ).
thf(c_0_116,plain,
! [X1943: term,X1944: subst] :
( ~ p4
| ( ( fsub @ fone @ ( fpush @ X1943 @ X1944 ) )
= X1943 ) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax4])])]) ).
thf(c_0_117,plain,
( p3
| p4 ),
inference(split_conjunct,[status(thm)],[ax1260]) ).
thf(c_0_118,plain,
! [X1: term,X2: term] :
( ( X1 = X2 )
| ~ p36
| ( ( flam @ X1 )
!= ( flam @ X2 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_111]) ).
thf(c_0_119,plain,
p36,
inference(sr,[status(thm)],[c_0_112,c_0_89]) ).
thf(c_0_120,plain,
( ( ( flam @ ( esk849_0 @ fsh @ fone ) )
= ( flam @ ( esk850_0 @ fsh @ fone ) ) )
| p53 ),
inference(split_conjunct,[status(thm)],[c_0_113]) ).
thf(c_0_121,plain,
~ p53,
inference(sr,[status(thm)],[c_0_114,c_0_115]) ).
thf(c_0_122,plain,
! [X1: term,X4: subst,X6: subst] :
( ( ( fsub @ ( esk849_0 @ X4 @ X1 ) @ X6 )
= ( esk849_0 @ ( fcomp @ X4 @ X6 ) @ ( fsub @ X1 @ X6 ) ) )
| p53 ),
inference(split_conjunct,[status(thm)],[c_0_113]) ).
thf(c_0_123,plain,
! [X4: subst,X1: term] :
( ( ( fsub @ fone @ ( fpush @ X1 @ X4 ) )
= X1 )
| ~ p4 ),
inference(split_conjunct,[status(thm)],[c_0_116]) ).
thf(c_0_124,plain,
p4,
inference(sr,[status(thm)],[c_0_117,c_0_41]) ).
thf(c_0_125,plain,
! [X1925: term,X1926: subst] :
( ~ p14
| ( ( fcomp @ fsh @ ( fpush @ X1925 @ X1926 ) )
= X1926 ) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax14])])]) ).
thf(c_0_126,plain,
( p13
| p14 ),
inference(split_conjunct,[status(thm)],[ax1250]) ).
thf(c_0_127,plain,
! [X1: term,X2: term] :
( ( X1 = X2 )
| ( ( flam @ X1 )
!= ( flam @ X2 ) ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_118,c_0_119])]) ).
thf(c_0_128,plain,
( ( flam @ ( esk849_0 @ fsh @ fone ) )
= ( flam @ ( esk850_0 @ fsh @ fone ) ) ),
inference(sr,[status(thm)],[c_0_120,c_0_121]) ).
thf(c_0_129,plain,
! [X1: term,X4: subst,X6: subst] :
( ( ( fsub @ ( esk850_0 @ X4 @ X1 ) @ X6 )
= ( esk850_0 @ ( fcomp @ X4 @ X6 ) @ ( fsub @ X1 @ X6 ) ) )
| p53 ),
inference(split_conjunct,[status(thm)],[c_0_113]) ).
thf(c_0_130,plain,
! [X1: term,X4: subst,X6: subst] :
( ( esk849_0 @ ( fcomp @ X4 @ X6 ) @ ( fsub @ X1 @ X6 ) )
= ( fsub @ ( esk849_0 @ X4 @ X1 ) @ X6 ) ),
inference(sr,[status(thm)],[c_0_122,c_0_121]) ).
thf(c_0_131,plain,
! [X4: subst,X1: term] :
( ( fsub @ fone @ ( fpush @ X1 @ X4 ) )
= X1 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_123,c_0_124])]) ).
thf(c_0_132,plain,
! [X1: term,X4: subst] :
( ( ( fcomp @ fsh @ ( fpush @ X1 @ X4 ) )
= X4 )
| ~ p14 ),
inference(split_conjunct,[status(thm)],[c_0_125]) ).
thf(c_0_133,plain,
p14,
inference(sr,[status(thm)],[c_0_126,c_0_56]) ).
thf(c_0_134,plain,
! [X1: term] :
( ( X1
= ( esk849_0 @ fsh @ fone ) )
| ( ( flam @ X1 )
!= ( flam @ ( esk850_0 @ fsh @ fone ) ) ) ),
inference(spm,[status(thm)],[c_0_127,c_0_128]) ).
thf(c_0_135,plain,
! [X1: term,X4: subst,X6: subst] :
( ( esk850_0 @ ( fcomp @ X4 @ X6 ) @ ( fsub @ X1 @ X6 ) )
= ( fsub @ ( esk850_0 @ X4 @ X1 ) @ X6 ) ),
inference(sr,[status(thm)],[c_0_129,c_0_121]) ).
thf(c_0_136,plain,
! [X1: term,X4: subst,X6: subst] :
( ( esk849_0 @ ( fcomp @ X4 @ ( fpush @ X1 @ X6 ) ) @ X1 )
= ( fsub @ ( esk849_0 @ X4 @ fone ) @ ( fpush @ X1 @ X6 ) ) ),
inference(spm,[status(thm)],[c_0_130,c_0_131]) ).
thf(c_0_137,plain,
! [X1: term,X4: subst] :
( ( fcomp @ fsh @ ( fpush @ X1 @ X4 ) )
= X4 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_132,c_0_133])]) ).
thf(c_0_138,plain,
( ( esk849_0 @ fsh @ fone )
= ( esk850_0 @ fsh @ fone ) ),
inference(er,[status(thm)],[c_0_134]) ).
thf(c_0_139,plain,
( p53
| ( ( esk849_0 @ esk851_0 @ esk852_0 )
!= ( esk850_0 @ esk851_0 @ esk852_0 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_113]) ).
thf(c_0_140,plain,
! [X1: term,X4: subst,X6: subst] :
( ( esk850_0 @ ( fcomp @ X4 @ ( fpush @ X1 @ X6 ) ) @ X1 )
= ( fsub @ ( esk850_0 @ X4 @ fone ) @ ( fpush @ X1 @ X6 ) ) ),
inference(spm,[status(thm)],[c_0_135,c_0_131]) ).
thf(c_0_141,plain,
! [X4: subst,X1: term] :
( ( fsub @ ( esk850_0 @ fsh @ fone ) @ ( fpush @ X1 @ X4 ) )
= ( esk849_0 @ X4 @ X1 ) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_136,c_0_137]),c_0_138]) ).
thf(c_0_142,plain,
( ( esk849_0 @ esk851_0 @ esk852_0 )
!= ( esk850_0 @ esk851_0 @ esk852_0 ) ),
inference(sr,[status(thm)],[c_0_139,c_0_121]) ).
thf(c_0_143,plain,
! [X4: subst,X1: term] :
( ( esk849_0 @ X4 @ X1 )
= ( esk850_0 @ X4 @ X1 ) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_140,c_0_137]),c_0_141]) ).
thf(c_0_144,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_142,c_0_143])]),
[proof] ).
thf(1,plain,
$false,
inference(eprover,[status(thm),assumptions([h0])],[]) ).
thf(0,theorem,
( ! [X1: term,X2: term,X3: subst] :
( ( sub @ ( ap @ X1 @ X2 ) @ X3 )
= ( ap @ ( sub @ X1 @ X3 ) @ ( sub @ X2 @ X3 ) ) )
=> ( ! [X1: term,X2: subst] :
( ( sub @ one @ ( push @ X1 @ X2 ) )
= X1 )
=> ( ! [X1: term] :
( ( sub @ X1 @ id )
= X1 )
=> ( ! [X1: term,X2: subst] :
( ( sub @ ( lam @ X1 ) @ X2 )
= ( lam @ ( sub @ X1 @ ( push @ one @ ( comp @ X2 @ sh ) ) ) ) )
=> ( ! [X1: term,X2: subst,X3: subst] :
( ( sub @ ( sub @ X1 @ X2 ) @ X3 )
= ( sub @ X1 @ ( comp @ X2 @ X3 ) ) )
=> ( ! [X1: subst] :
( ( comp @ id @ X1 )
= X1 )
=> ( ! [X1: term,X2: subst] :
( ( comp @ sh @ ( push @ X1 @ X2 ) )
= X2 )
=> ( ! [X1: subst,X2: subst,X3: subst] :
( ( comp @ ( comp @ X1 @ X2 ) @ X3 )
= ( comp @ X1 @ ( comp @ X2 @ X3 ) ) )
=> ( ! [X1: term,X2: subst,X3: subst] :
( ( comp @ ( push @ X1 @ X2 ) @ X3 )
= ( push @ ( sub @ X1 @ X3 ) @ ( comp @ X2 @ X3 ) ) )
=> ( ! [X1: subst] :
( ( comp @ X1 @ id )
= X1 )
=> ( ( ( push @ one @ sh )
= id )
=> ( ! [X1: subst] :
( ( push @ ( sub @ one @ X1 ) @ ( comp @ sh @ X1 ) )
= X1 )
=> ( ( var @ one )
=> ( ! [X1: term] :
( ( var @ X1 )
=> ( var @ ( sub @ X1 @ sh ) ) )
=> ( ! [X1: term > $o] :
( ( X1 @ one )
=> ( ! [X2: term] :
( ( var @ X2 )
=> ( ( X1 @ X2 )
=> ( X1 @ ( sub @ X2 @ sh ) ) ) )
=> ! [X2: term] :
( ( var @ X2 )
=> ( X1 @ X2 ) ) ) )
=> ( ! [X1: term,X2: term,X3: term,X4: term] :
( ( ( ap @ X1 @ X3 )
= ( ap @ X2 @ X4 ) )
=> ( X1 = X2 ) )
=> ( ! [X1: term,X2: term,X3: term,X4: term] :
( ( ( ap @ X1 @ X3 )
= ( ap @ X2 @ X4 ) )
=> ( X3 = X4 ) )
=> ( ! [X1: term,X2: term] :
( ( ( lam @ X1 )
= ( lam @ X2 ) )
=> ( X1 = X2 ) )
=> ( ! [X1: term,X2: term] :
( ( ( sub @ X1 @ sh )
= ( sub @ X2 @ sh ) )
=> ( X1 = X2 ) )
=> ( ! [X1: term,X2: term,X3: term] :
( ( lam @ X1 )
!= ( ap @ X2 @ X3 ) )
=> ( ! [X1: term,X2: term] :
~ ( var @ ( ap @ X1 @ X2 ) )
=> ( ! [X1: term] :
~ ( var @ ( lam @ X1 ) )
=> ( ! [X1: term > $o] :
( ! [X2: term] :
( ( var @ X2 )
=> ( X1 @ X2 ) )
=> ( ! [X2: term,X3: term] :
( ( X1 @ X2 )
=> ( ( X1 @ X3 )
=> ( X1 @ ( ap @ X2 @ X3 ) ) ) )
=> ( ! [X2: term] :
( ( X1 @ X2 )
=> ( X1 @ ( lam @ X2 ) ) )
=> ( !! @ X1 ) ) ) )
=> ( ! [X1: term > $o,X2: term,X3: subst] :
( ! [X4: term] :
( ( var @ X4 )
=> ( X1 @ ( sub @ X4 @ X3 ) ) )
=> ( ( X1 @ X2 )
=> ! [X4: term] :
( ( var @ X4 )
=> ( X1 @ ( sub @ X4 @ ( push @ X2 @ X3 ) ) ) ) ) )
=> ( ! [X1: term > $o] :
( ! [X2: term,X3: term] :
( ( X1 @ X2 )
=> ( ( X1 @ X3 )
=> ( X1 @ ( ap @ X2 @ X3 ) ) ) )
=> ( ! [X2: term] :
( ! [X3: term] :
( ( X1 @ X3 )
=> ( X1 @ ( sub @ X2 @ ( push @ X3 @ id ) ) ) )
=> ( X1 @ ( lam @ X2 ) ) )
=> ! [X2: term,X3: subst] :
( ! [X4: term] :
( ( var @ X4 )
=> ( X1 @ ( sub @ X4 @ X3 ) ) )
=> ( X1 @ ( sub @ X2 @ X3 ) ) ) ) )
=> ( ! [X1: term > $o] :
( ! [X2: term] :
( ( var @ X2 )
=> ( X1 @ X2 ) )
=> ( ! [X2: term,X3: term] :
( ( X1 @ X2 )
=> ( ( X1 @ X3 )
=> ( X1 @ ( ap @ X2 @ X3 ) ) ) )
=> ( ! [X2: term] :
( ! [X3: term] :
( ( X1 @ X3 )
=> ( X1 @ ( sub @ X2 @ ( push @ X3 @ id ) ) ) )
=> ( X1 @ ( lam @ X2 ) ) )
=> ( !! @ X1 ) ) ) )
=> ( ~ ( ~ ( ! [X1: subst,X2: subst,X3: subst] :
( ( comp @ ( comp @ X1 @ X2 ) @ X3 )
= ( comp @ X1 @ ( comp @ X2 @ X3 ) ) )
=> ~ ! [X1: subst] :
( ( comp @ id @ X1 )
= X1 ) )
=> ~ ! [X1: subst] :
( ( comp @ X1 @ id )
= X1 ) )
=> ( ~ ( ! [X1: term,X2: subst,X3: subst] :
( ( sub @ ( sub @ X1 @ X2 ) @ X3 )
= ( sub @ X1 @ ( comp @ X2 @ X3 ) ) )
=> ~ ! [X1: term] :
( ( sub @ X1 @ id )
= X1 ) )
=> ( ! [X1: term,X2: term,X3: term,X4: term] :
( ( ( ap @ ( sub @ X1 @ id ) @ X3 )
= ( ap @ ( sub @ X2 @ id ) @ X4 ) )
=> ( X1 = X2 ) )
=> ( ! [X1: term,X2: term,X3: term,X4: term] :
( ( ( ap @ ( sub @ X1 @ id ) @ X3 )
= ( ap @ ( sub @ X2 @ id ) @ X4 ) )
=> ( X3 = X4 ) )
=> ! [X1: subst > term > term] :
( ! [X2: subst,X3: term,X4: subst] :
( ( sub @ ( X1 @ X2 @ X3 ) @ X4 )
= ( X1 @ ( comp @ X2 @ X4 ) @ ( sub @ X3 @ X4 ) ) )
=> ! [X2: subst > term > term] :
( ! [X3: subst,X4: term,X5: subst] :
( ( sub @ ( X2 @ X3 @ X4 ) @ X5 )
= ( X2 @ ( comp @ X3 @ X5 ) @ ( sub @ X4 @ X5 ) ) )
=> ( ( ( lam @ ( X1 @ sh @ one ) )
= ( lam @ ( X2 @ sh @ one ) ) )
=> ! [X3: subst,X4: term] :
( ( X1 @ X3 @ X4 )
= ( X2 @ X3 @ X4 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(contra,[status(thm),contra(discharge,[h0])],[1,h0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : ALG258^1 : TPTP v9.2.0. Bugfixed v5.2.0.
% 0.10/0.12 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.13/0.33 % Computer : n006.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Wed Oct 8 23:19:08 EDT 2025
% 0.13/0.33 % CPUTime :
% 94.30/94.22 % SZS status Theorem
% 94.30/94.22 % Mode: mode503:USE_SINE=true:SINE_TOLERANCE=1.2:SINE_GENERALITY_THRESHOLD=0:SINE_RANK_LIMIT=4.:SINE_DEPTH=0
% 94.30/94.22 % Inferences: 541
% 94.30/94.22 % SZS output start Proof
% See solution above
%------------------------------------------------------------------------------