%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ALG263^1 : TPTP v9.3.1. Bugfixed v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n008.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:44:47 AM UTC 2026
% Result : Theorem 0.22s 0.34s
% Output : CNFRefutation 0.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 38
% Syntax : Number of formulae : 55 ( 12 unt; 0 typ; 0 def)
% Number of atoms : 347 ( 163 equ; 0 cnn)
% Maximal formula atoms : 77 ( 6 avg)
% Number of connectives : 2461 ( 121 ~; 152 |; 86 &;1795 @)
% ( 39 <=>; 268 =>; 0 <=; 0 <~>)
% Maximal formula depth : 170 ( 10 avg)
% Number of types : 3 ( 2 usr)
% Number of type conns : 74 ( 74 >; 0 *; 0 +; 0 <<)
% Number of symbols : 78 ( 76 usr; 41 con; 0-4 aty)
% Number of variables : 524 ( 32 ^; 492 !; 0 ?; 524 :)
% Comments :
%------------------------------------------------------------------------------
thf(decl_sort1,type,
term: $tType ).
thf(decl_sort2,type,
subst: $tType ).
thf(decl_23,type,
one: term ).
thf(decl_24,type,
ap: term > term > term ).
thf(decl_25,type,
lam: term > term ).
thf(decl_26,type,
sub: term > subst > term ).
thf(decl_27,type,
id: subst ).
thf(decl_28,type,
sh: subst ).
thf(decl_29,type,
push: term > subst > subst ).
thf(decl_30,type,
comp: subst > subst > subst ).
thf(decl_31,type,
var: term > $o ).
thf(decl_34,type,
axmap: $o ).
thf(decl_36,type,
shinj: $o ).
thf(decl_39,type,
hoasap: subst > term > subst > term > term ).
thf(decl_40,type,
induction2lem: $o ).
thf(decl_42,type,
axvarshift: $o ).
thf(decl_43,type,
hoasapinj2: $o ).
thf(decl_45,type,
hoasapinj1: $o ).
thf(decl_46,type,
ulamvar1: $o ).
thf(decl_49,type,
apnotvar: $o ).
thf(decl_54,type,
hoaslaminj: $o ).
thf(decl_61,type,
hoasinduction_lem1: $o ).
thf(decl_64,type,
hoasapnotvar: $o ).
thf(decl_68,type,
axapp: $o ).
thf(decl_72,type,
ulamvarind: $o ).
thf(decl_73,type,
induction: $o ).
thf(decl_83,type,
axclos: $o ).
thf(decl_84,type,
axassoc: $o ).
thf(decl_87,type,
apinj2: $o ).
thf(decl_88,type,
apinj1: $o ).
thf(decl_93,type,
axvarcons: $o ).
thf(decl_94,type,
hoaslam: subst > ( subst > term > term ) > term ).
thf(decl_95,type,
axscons: $o ).
thf(decl_97,type,
axidr: $o ).
thf(decl_99,type,
laminj: $o ).
thf(decl_103,type,
axabs: $o ).
thf(decl_109,type,
lamnotap: $o ).
thf(decl_111,type,
hoaslamnotvar: $o ).
thf(decl_112,type,
axidl: $o ).
thf(decl_117,type,
pushprop: $o ).
thf(decl_121,type,
substmonoid: $o ).
thf(decl_122,type,
lamnotvar: $o ).
thf(decl_124,type,
hoasinduction_lem1_gthm: $o ).
thf(decl_128,type,
hoasvar: subst > term > subst > $o ).
thf(decl_129,type,
hoaslamnotap: $o ).
thf(decl_131,type,
ulamvarsh: $o ).
thf(decl_132,type,
induction2: $o ).
thf(decl_137,type,
axshiftcons: $o ).
thf(decl_138,type,
termmset: $o ).
thf(decl_143,type,
axvarid: $o ).
thf(decl_145,type,
esk1_1: ( term > $o ) > term ).
thf(decl_146,type,
esk2_1: ( term > $o ) > term ).
thf(decl_147,type,
esk3_1: ( term > $o ) > term ).
thf(decl_148,type,
esk4_1: ( term > $o ) > term ).
thf(decl_149,type,
esk5_1: ( term > $o ) > term ).
thf(decl_150,type,
esk6_3: ( term > $o ) > term > subst > term ).
thf(decl_151,type,
esk7_1: ( term > $o ) > term ).
thf(decl_152,type,
esk8_1: ( term > $o ) > term ).
thf(decl_153,type,
esk9_1: ( term > $o ) > term ).
thf(decl_154,type,
esk10_3: ( term > $o ) > term > subst > term ).
thf(decl_155,type,
esk11_1: ( term > $o ) > term ).
thf(decl_156,type,
esk12_1: ( term > $o ) > term ).
thf(decl_157,type,
esk13_1: ( term > $o ) > term ).
thf(decl_158,type,
esk14_1: ( term > $o ) > term ).
thf(decl_159,type,
esk15_1: ( subst > term > term ) > subst ).
thf(decl_160,type,
esk16_1: ( subst > term > term ) > term ).
thf(decl_161,type,
esk17_1: ( subst > term > term ) > subst ).
thf(decl_162,type,
esk18_2: ( subst > term > term ) > ( subst > term > term ) > subst ).
thf(decl_163,type,
esk19_2: ( subst > term > term ) > ( subst > term > term ) > term ).
thf(decl_164,type,
esk20_2: ( subst > term > term ) > ( subst > term > term ) > subst ).
thf(decl_165,type,
esk21_1: ( subst > term > term ) > subst ).
thf(decl_166,type,
esk22_1: ( subst > term > term ) > term ).
thf(decl_167,type,
esk23_1: ( subst > term > term ) > subst ).
thf(decl_168,type,
esk24_1: ( subst > term > term ) > subst ).
thf(decl_169,type,
esk25_1: ( subst > term > term ) > term ).
thf(decl_170,type,
esk26_1: ( subst > term > term ) > subst ).
thf(decl_171,type,
epred1_0: subst > term > subst > $o ).
thf(decl_172,type,
esk27_0: term ).
thf(hoaslamnotvar,axiom,
( hoaslamnotvar
<=> ! [X12: subst > term > term] :
( ! [X3: subst,X1: term,X4: subst] :
( ( sub @ ( X12 @ X3 @ X1 ) @ X4 )
= ( X12 @ ( comp @ X3 @ X4 ) @ ( sub @ X1 @ X4 ) ) )
=> ~ ( hoasvar @ id
@ ( hoaslam @ id
@ ^ [X3: subst,X1: term] : ( X12 @ X3 @ X1 ) )
@ id ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',hoaslamnotvar) ).
thf(hoasvar,axiom,
( hoasvar
= ( ^ [X3: subst,X1: term,X4: subst] : ( var @ ( sub @ X1 @ X4 ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',hoasvar) ).
thf(hoaslaminj,axiom,
( hoaslaminj
<=> ! [X12: subst > term > term] :
( ! [X3: subst,X1: term,X4: subst] :
( ( sub @ ( X12 @ X3 @ X1 ) @ X4 )
= ( X12 @ ( comp @ X3 @ X4 ) @ ( sub @ X1 @ X4 ) ) )
=> ! [X13: subst > term > term] :
( ! [X3: subst,X1: term,X4: subst] :
( ( sub @ ( X13 @ X3 @ X1 ) @ X4 )
= ( X13 @ ( comp @ X3 @ X4 ) @ ( sub @ X1 @ X4 ) ) )
=> ( ( ( hoaslam @ id
@ ^ [X3: subst,X1: term] : ( X12 @ X3 @ X1 ) )
= ( hoaslam @ id
@ ^ [X3: subst,X1: term] : ( X13 @ X3 @ X1 ) ) )
=> ! [X3: subst,X1: term] :
( ( X12 @ X3 @ X1 )
= ( X13 @ X3 @ X1 ) ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',hoaslaminj) ).
thf(hoaslamnotap,axiom,
( hoaslamnotap
<=> ! [X12: subst > term > term] :
( ! [X3: subst,X1: term,X4: subst] :
( ( sub @ ( X12 @ X3 @ X1 ) @ X4 )
= ( X12 @ ( comp @ X3 @ X4 ) @ ( sub @ X1 @ X4 ) ) )
=> ! [X1: term,X2: term] :
( ( hoaslam @ id
@ ^ [X3: subst,X7: term] : ( X12 @ X3 @ X7 ) )
!= ( hoasap @ id @ X1 @ id @ X2 ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',hoaslamnotap) ).
thf(hoasapnotvar,axiom,
( hoasapnotvar
<=> ! [X1: term,X2: term] :
~ ( hoasvar @ id @ ( hoasap @ id @ X1 @ id @ X2 ) @ id ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',hoasapnotvar) ).
thf(hoasinduction_lem1,axiom,
( hoasinduction_lem1
<=> ! [X20: subst > term > subst > $o] :
( ! [X3: subst,X1: term,X4: subst,X5: subst] :
( ( X20 @ X3 @ X1 @ ( comp @ X5 @ X4 ) )
=> ( X20 @ ( comp @ X3 @ X5 ) @ ( sub @ X1 @ X5 ) @ X4 ) )
=> ( ! [X3: subst,X1: term,X4: subst,X5: subst] :
( ( X20 @ ( comp @ X3 @ X5 ) @ ( sub @ X1 @ X5 ) @ X4 )
=> ( X20 @ X3 @ X1 @ ( comp @ X5 @ X4 ) ) )
=> ( ! [X1: term] :
( ( hoasvar @ id @ X1 @ id )
=> ( X20 @ id @ X1 @ id ) )
=> ! [X1: term] :
( ( var @ X1 )
=> ( X20 @ id @ X1 @ id ) ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',hoasinduction_lem1) ).
thf(thm,conjecture,
hoasinduction_lem1_gthm,
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',thm) ).
thf(hoasinduction_lem1_gthm,axiom,
( hoasinduction_lem1_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
=> ( hoaslamnotap
=> ( hoaslamnotvar
=> ( hoasapnotvar
=> hoasinduction_lem1 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',hoasinduction_lem1_gthm) ).
thf(axapp,axiom,
( axapp
<=> ! [X1: term,X2: term,X3: subst] :
( ( sub @ ( ap @ X1 @ X2 ) @ X3 )
= ( ap @ ( sub @ X1 @ X3 ) @ ( sub @ X2 @ X3 ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',axapp) ).
thf(axvarcons,axiom,
( axvarcons
<=> ! [X1: term,X3: subst] :
( ( sub @ one @ ( push @ X1 @ X3 ) )
= X1 ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',axvarcons) ).
thf(axvarid,axiom,
( axvarid
<=> ! [X1: term] :
( ( sub @ X1 @ id )
= X1 ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',axvarid) ).
thf(axabs,axiom,
( axabs
<=> ! [X1: term,X3: subst] :
( ( sub @ ( lam @ X1 ) @ X3 )
= ( lam @ ( sub @ X1 @ ( push @ one @ ( comp @ X3 @ sh ) ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',axabs) ).
thf(axclos,axiom,
( axclos
<=> ! [X1: term,X3: subst,X4: subst] :
( ( sub @ ( sub @ X1 @ X3 ) @ X4 )
= ( sub @ X1 @ ( comp @ X3 @ X4 ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',axclos) ).
thf(axidl,axiom,
( axidl
<=> ! [X3: subst] :
( ( comp @ id @ X3 )
= X3 ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',axidl) ).
thf(axshiftcons,axiom,
( axshiftcons
<=> ! [X1: term,X3: subst] :
( ( comp @ sh @ ( push @ X1 @ X3 ) )
= X3 ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',axshiftcons) ).
thf(axassoc,axiom,
( axassoc
<=> ! [X3: subst,X4: subst,X5: subst] :
( ( comp @ ( comp @ X3 @ X4 ) @ X5 )
= ( comp @ X3 @ ( comp @ X4 @ X5 ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',axassoc) ).
thf(axmap,axiom,
( axmap
<=> ! [X1: term,X3: subst,X4: subst] :
( ( comp @ ( push @ X1 @ X3 ) @ X4 )
= ( push @ ( sub @ X1 @ X4 ) @ ( comp @ X3 @ X4 ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',axmap) ).
thf(axidr,axiom,
( axidr
<=> ! [X3: subst] :
( ( comp @ X3 @ id )
= X3 ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',axidr) ).
thf(axvarshift,axiom,
( axvarshift
<=> ( ( push @ one @ sh )
= id ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',axvarshift) ).
thf(axscons,axiom,
( axscons
<=> ! [X3: subst] :
( ( push @ ( sub @ one @ X3 ) @ ( comp @ sh @ X3 ) )
= X3 ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',axscons) ).
thf(ulamvar1,axiom,
( ulamvar1
<=> ( var @ one ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',ulamvar1) ).
thf(ulamvarsh,axiom,
( ulamvarsh
<=> ! [X1: term] :
( ( var @ X1 )
=> ( var @ ( sub @ X1 @ sh ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',ulamvarsh) ).
thf(ulamvarind,axiom,
( ulamvarind
<=> ! [X6: term > $o] :
( ( X6 @ one )
=> ( ! [X1: term] :
( ( var @ X1 )
=> ( ( X6 @ X1 )
=> ( X6 @ ( sub @ X1 @ sh ) ) ) )
=> ! [X1: term] :
( ( var @ X1 )
=> ( X6 @ X1 ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',ulamvarind) ).
thf(apinj1,axiom,
( apinj1
<=> ! [X1: term,X2: term,X7: term,X8: term] :
( ( ( ap @ X1 @ X7 )
= ( ap @ X2 @ X8 ) )
=> ( X1 = X2 ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',apinj1) ).
thf(apinj2,axiom,
( apinj2
<=> ! [X1: term,X2: term,X7: term,X8: term] :
( ( ( ap @ X1 @ X7 )
= ( ap @ X2 @ X8 ) )
=> ( X7 = X8 ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',apinj2) ).
thf(laminj,axiom,
( laminj
<=> ! [X1: term,X2: term] :
( ( ( lam @ X1 )
= ( lam @ X2 ) )
=> ( X1 = X2 ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',laminj) ).
thf(shinj,axiom,
( shinj
<=> ! [X1: term,X2: term] :
( ( ( sub @ X1 @ sh )
= ( sub @ X2 @ sh ) )
=> ( X1 = X2 ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',shinj) ).
thf(lamnotap,axiom,
( lamnotap
<=> ! [X1: term,X2: term,X7: term] :
( ( lam @ X1 )
!= ( ap @ X2 @ X7 ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',lamnotap) ).
thf(apnotvar,axiom,
( apnotvar
<=> ! [X1: term,X2: term] :
~ ( var @ ( ap @ X1 @ X2 ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',apnotvar) ).
thf(lamnotvar,axiom,
( lamnotvar
<=> ! [X1: term] :
~ ( var @ ( lam @ X1 ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',lamnotvar) ).
thf(induction,axiom,
( induction
<=> ! [X6: term > $o] :
( ! [X1: term] :
( ( var @ X1 )
=> ( X6 @ X1 ) )
=> ( ! [X1: term,X2: term] :
( ( X6 @ X1 )
=> ( ( X6 @ X2 )
=> ( X6 @ ( ap @ X1 @ X2 ) ) ) )
=> ( ! [X1: term] :
( ( X6 @ X1 )
=> ( X6 @ ( lam @ X1 ) ) )
=> ! [X1: term] : ( X6 @ X1 ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',induction) ).
thf(pushprop,axiom,
( pushprop
<=> ! [X6: term > $o,X1: term,X3: subst] :
( ! [X2: term] :
( ( var @ X2 )
=> ( X6 @ ( sub @ X2 @ X3 ) ) )
=> ( ( X6 @ X1 )
=> ! [X2: term] :
( ( var @ X2 )
=> ( X6 @ ( sub @ X2 @ ( push @ X1 @ X3 ) ) ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',pushprop) ).
thf(induction2lem,axiom,
( induction2lem
<=> ! [X6: term > $o] :
( ! [X1: term,X2: term] :
( ( X6 @ X1 )
=> ( ( X6 @ X2 )
=> ( X6 @ ( ap @ X1 @ X2 ) ) ) )
=> ( ! [X1: term] :
( ! [X2: term] :
( ( X6 @ X2 )
=> ( X6 @ ( sub @ X1 @ ( push @ X2 @ id ) ) ) )
=> ( X6 @ ( lam @ X1 ) ) )
=> ! [X1: term,X3: subst] :
( ! [X2: term] :
( ( var @ X2 )
=> ( X6 @ ( sub @ X2 @ X3 ) ) )
=> ( X6 @ ( sub @ X1 @ X3 ) ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',induction2lem) ).
thf(induction2,axiom,
( induction2
<=> ! [X6: term > $o] :
( ! [X1: term] :
( ( var @ X1 )
=> ( X6 @ X1 ) )
=> ( ! [X1: term,X2: term] :
( ( X6 @ X1 )
=> ( ( X6 @ X2 )
=> ( X6 @ ( ap @ X1 @ X2 ) ) ) )
=> ( ! [X1: term] :
( ! [X2: term] :
( ( X6 @ X2 )
=> ( X6 @ ( sub @ X1 @ ( push @ X2 @ id ) ) ) )
=> ( X6 @ ( lam @ X1 ) ) )
=> ! [X1: term] : ( X6 @ X1 ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',induction2) ).
thf(substmonoid,axiom,
( substmonoid
<=> ( ! [X3: subst,X4: subst,X5: subst] :
( ( comp @ ( comp @ X3 @ X4 ) @ X5 )
= ( comp @ X3 @ ( comp @ X4 @ X5 ) ) )
& ! [X3: subst] :
( ( comp @ id @ X3 )
= X3 )
& ! [X3: subst] :
( ( comp @ X3 @ id )
= X3 ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',substmonoid) ).
thf(termmset,axiom,
( termmset
<=> ( ! [X1: term,X3: subst,X4: subst] :
( ( sub @ ( sub @ X1 @ X3 ) @ X4 )
= ( sub @ X1 @ ( comp @ X3 @ X4 ) ) )
& ! [X1: term] :
( ( sub @ X1 @ id )
= X1 ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',termmset) ).
thf(hoasapinj1,axiom,
( hoasapinj1
<=> ! [X1: term,X2: term,X7: term,X8: term] :
( ( ( hoasap @ id @ X1 @ id @ X7 )
= ( hoasap @ id @ X2 @ id @ X8 ) )
=> ( X1 = X2 ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',hoasapinj1) ).
thf(hoasapinj2,axiom,
( hoasapinj2
<=> ! [X1: term,X2: term,X7: term,X8: term] :
( ( ( hoasap @ id @ X1 @ id @ X7 )
= ( hoasap @ id @ X2 @ id @ X8 ) )
=> ( X7 = X8 ) ) ),
file('/export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p',hoasapinj2) ).
thf(c_0_38,plain,
( hoaslamnotvar
<=> ! [X12: subst > term > term] :
( ! [X3: subst,X1: term,X4: subst] :
( ( sub @ ( X12 @ X3 @ X1 ) @ X4 )
= ( X12 @ ( comp @ X3 @ X4 ) @ ( sub @ X1 @ X4 ) ) )
=> ~ ( hoasvar @ id
@ ( hoaslam @ id
@ ^ [Z0: subst,Z1: term] : ( X12 @ Z0 @ Z1 ) )
@ id ) ) ),
inference(fof_simplification,[status(thm)],[hoaslamnotvar]) ).
thf(c_0_39,plain,
( hoasvar
= ( ^ [Z0: subst,Z1: term,Z2: subst] : ( var @ ( sub @ Z1 @ Z2 ) ) ) ),
inference(fof_simplification,[status(thm)],[hoasvar]) ).
thf(c_0_40,plain,
( hoaslaminj
<=> ! [X12: subst > term > term] :
( ! [X3: subst,X1: term,X4: subst] :
( ( sub @ ( X12 @ X3 @ X1 ) @ X4 )
= ( X12 @ ( comp @ X3 @ X4 ) @ ( sub @ X1 @ X4 ) ) )
=> ! [X13: subst > term > term] :
( ! [X3: subst,X1: term,X4: subst] :
( ( sub @ ( X13 @ X3 @ X1 ) @ X4 )
= ( X13 @ ( comp @ X3 @ X4 ) @ ( sub @ X1 @ X4 ) ) )
=> ( ( ( hoaslam @ id
@ ^ [Z0: subst,Z1: term] : ( X12 @ Z0 @ Z1 ) )
= ( hoaslam @ id
@ ^ [Z0: subst,Z1: term] : ( X13 @ Z0 @ Z1 ) ) )
=> ! [X3: subst,X1: term] :
( ( X12 @ X3 @ X1 )
= ( X13 @ X3 @ X1 ) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[hoaslaminj]) ).
thf(c_0_41,plain,
( hoaslamnotap
<=> ! [X12: subst > term > term] :
( ! [X3: subst,X1: term,X4: subst] :
( ( sub @ ( X12 @ X3 @ X1 ) @ X4 )
= ( X12 @ ( comp @ X3 @ X4 ) @ ( sub @ X1 @ X4 ) ) )
=> ! [X1: term,X2: term] :
( ( hoaslam @ id
@ ^ [Z0: subst,Z1: term] : ( X12 @ Z0 @ Z1 ) )
!= ( hoasap @ id @ X1 @ id @ X2 ) ) ) ),
inference(fof_simplification,[status(thm)],[hoaslamnotap]) ).
thf(c_0_42,plain,
( hoaslamnotvar
= ( ! [X12: subst > term > term] :
( ! [X3: subst,X1: term,X4: subst] :
( ( sub @ ( X12 @ X3 @ X1 ) @ X4 )
= ( X12 @ ( comp @ X3 @ X4 ) @ ( sub @ X1 @ X4 ) ) )
=> ~ ( var
@ ( sub
@ ( hoaslam @ id
@ ^ [Z0: subst,Z1: term] : ( X12 @ Z0 @ Z1 ) )
@ id ) ) ) ) ),
inference(apply_def,[status(thm)],[c_0_38,c_0_39]) ).
thf(c_0_43,axiom,
( hoasapnotvar
= ( ! [X1: term,X2: term] :
~ ( var @ ( sub @ ( hoasap @ id @ X1 @ id @ X2 ) @ id ) ) ) ),
inference(apply_def,[status(thm)],[hoasapnotvar,c_0_39]) ).
thf(c_0_44,axiom,
( hoasinduction_lem1
= ( ! [X20: subst > term > subst > $o] :
( ! [X3: subst,X1: term,X4: subst,X5: subst] :
( ( X20 @ X3 @ X1 @ ( comp @ X5 @ X4 ) )
=> ( X20 @ ( comp @ X3 @ X5 ) @ ( sub @ X1 @ X5 ) @ X4 ) )
=> ( ! [X3: subst,X1: term,X4: subst,X5: subst] :
( ( X20 @ ( comp @ X3 @ X5 ) @ ( sub @ X1 @ X5 ) @ X4 )
=> ( X20 @ X3 @ X1 @ ( comp @ X5 @ X4 ) ) )
=> ( ! [X1: term] :
( ( var @ ( sub @ X1 @ id ) )
=> ( X20 @ id @ X1 @ id ) )
=> ! [X1: term] :
( ( var @ X1 )
=> ( X20 @ id @ X1 @ id ) ) ) ) ) ) ),
inference(apply_def,[status(thm)],[hoasinduction_lem1,c_0_39]) ).
thf(c_0_45,negated_conjecture,
~ hoasinduction_lem1_gthm,
inference(assume_negation,[status(cth)],[thm]) ).
thf(c_0_46,axiom,
( hoasinduction_lem1_gthm
= ( ! [X2948: term,X2949: term,X2950: subst] :
( ( sub @ ( ap @ X2948 @ X2949 ) @ X2950 )
= ( ap @ ( sub @ X2948 @ X2950 ) @ ( sub @ X2949 @ X2950 ) ) )
=> ( ! [X2951: term,X2952: subst] :
( ( sub @ one @ ( push @ X2951 @ X2952 ) )
= X2951 )
=> ( ! [X2953: term] :
( ( sub @ X2953 @ id )
= X2953 )
=> ( ! [X2954: term,X2955: subst] :
( ( sub @ ( lam @ X2954 ) @ X2955 )
= ( lam @ ( sub @ X2954 @ ( push @ one @ ( comp @ X2955 @ sh ) ) ) ) )
=> ( ! [X2956: term,X2957: subst,X2958: subst] :
( ( sub @ ( sub @ X2956 @ X2957 ) @ X2958 )
= ( sub @ X2956 @ ( comp @ X2957 @ X2958 ) ) )
=> ( ! [X2959: subst] :
( ( comp @ id @ X2959 )
= X2959 )
=> ( ! [X2960: term,X2961: subst] :
( ( comp @ sh @ ( push @ X2960 @ X2961 ) )
= X2961 )
=> ( ! [X2962: subst,X2963: subst,X2964: subst] :
( ( comp @ ( comp @ X2962 @ X2963 ) @ X2964 )
= ( comp @ X2962 @ ( comp @ X2963 @ X2964 ) ) )
=> ( ! [X2965: term,X2966: subst,X2967: subst] :
( ( comp @ ( push @ X2965 @ X2966 ) @ X2967 )
= ( push @ ( sub @ X2965 @ X2967 ) @ ( comp @ X2966 @ X2967 ) ) )
=> ( ! [X2968: subst] :
( ( comp @ X2968 @ id )
= X2968 )
=> ( ( ( push @ one @ sh )
= id )
=> ( ! [X2969: subst] :
( ( push @ ( sub @ one @ X2969 ) @ ( comp @ sh @ X2969 ) )
= X2969 )
=> ( ( var @ one )
=> ( ! [X2970: term] :
( ( var @ X2970 )
=> ( var @ ( sub @ X2970 @ sh ) ) )
=> ( ! [X2971: term > $o] :
( ( X2971 @ one )
=> ( ! [X2972: term] :
( ( var @ X2972 )
=> ( ( X2971 @ X2972 )
=> ( X2971 @ ( sub @ X2972 @ sh ) ) ) )
=> ! [X2973: term] :
( ( var @ X2973 )
=> ( X2971 @ X2973 ) ) ) )
=> ( ! [X2974: term,X2975: term,X2976: term,X2977: term] :
( ( ( ap @ X2974 @ X2976 )
= ( ap @ X2975 @ X2977 ) )
=> ( X2974 = X2975 ) )
=> ( ! [X2978: term,X2979: term,X2980: term,X2981: term] :
( ( ( ap @ X2978 @ X2980 )
= ( ap @ X2979 @ X2981 ) )
=> ( X2980 = X2981 ) )
=> ( ! [X2982: term,X2983: term] :
( ( ( lam @ X2982 )
= ( lam @ X2983 ) )
=> ( X2982 = X2983 ) )
=> ( ! [X2984: term,X2985: term] :
( ( ( sub @ X2984 @ sh )
= ( sub @ X2985 @ sh ) )
=> ( X2984 = X2985 ) )
=> ( ! [X2986: term,X2987: term,X2988: term] :
( ( lam @ X2986 )
!= ( ap @ X2987 @ X2988 ) )
=> ( ! [X2989: term,X2990: term] :
~ ( var @ ( ap @ X2989 @ X2990 ) )
=> ( ! [X2991: term] :
~ ( var @ ( lam @ X2991 ) )
=> ( ! [X2992: term > $o] :
( ! [X2993: term] :
( ( var @ X2993 )
=> ( X2992 @ X2993 ) )
=> ( ! [X2994: term,X2995: term] :
( ( X2992 @ X2994 )
=> ( ( X2992 @ X2995 )
=> ( X2992 @ ( ap @ X2994 @ X2995 ) ) ) )
=> ( ! [X2996: term] :
( ( X2992 @ X2996 )
=> ( X2992 @ ( lam @ X2996 ) ) )
=> ! [X2997: term] : ( X2992 @ X2997 ) ) ) )
=> ( ! [X2998: term > $o,X2999: term,X3000: subst] :
( ! [X3001: term] :
( ( var @ X3001 )
=> ( X2998 @ ( sub @ X3001 @ X3000 ) ) )
=> ( ( X2998 @ X2999 )
=> ! [X3002: term] :
( ( var @ X3002 )
=> ( X2998 @ ( sub @ X3002 @ ( push @ X2999 @ X3000 ) ) ) ) ) )
=> ( ! [X3003: term > $o] :
( ! [X3004: term,X3005: term] :
( ( X3003 @ X3004 )
=> ( ( X3003 @ X3005 )
=> ( X3003 @ ( ap @ X3004 @ X3005 ) ) ) )
=> ( ! [X3006: term] :
( ! [X3007: term] :
( ( X3003 @ X3007 )
=> ( X3003 @ ( sub @ X3006 @ ( push @ X3007 @ id ) ) ) )
=> ( X3003 @ ( lam @ X3006 ) ) )
=> ! [X3008: term,X3009: subst] :
( ! [X3010: term] :
( ( var @ X3010 )
=> ( X3003 @ ( sub @ X3010 @ X3009 ) ) )
=> ( X3003 @ ( sub @ X3008 @ X3009 ) ) ) ) )
=> ( ! [X3011: term > $o] :
( ! [X3012: term] :
( ( var @ X3012 )
=> ( X3011 @ X3012 ) )
=> ( ! [X3013: term,X3014: term] :
( ( X3011 @ X3013 )
=> ( ( X3011 @ X3014 )
=> ( X3011 @ ( ap @ X3013 @ X3014 ) ) ) )
=> ( ! [X3015: term] :
( ! [X3016: term] :
( ( X3011 @ X3016 )
=> ( X3011 @ ( sub @ X3015 @ ( push @ X3016 @ id ) ) ) )
=> ( X3011 @ ( lam @ X3015 ) ) )
=> ! [X3017: term] : ( X3011 @ X3017 ) ) ) )
=> ( ( ! [X3018: subst,X3019: subst,X3020: subst] :
( ( comp @ ( comp @ X3018 @ X3019 ) @ X3020 )
= ( comp @ X3018 @ ( comp @ X3019 @ X3020 ) ) )
& ! [X3021: subst] :
( ( comp @ id @ X3021 )
= X3021 )
& ! [X3022: subst] :
( ( comp @ X3022 @ id )
= X3022 ) )
=> ( ( ! [X3023: term,X3024: subst,X3025: subst] :
( ( sub @ ( sub @ X3023 @ X3024 ) @ X3025 )
= ( sub @ X3023 @ ( comp @ X3024 @ X3025 ) ) )
& ! [X3026: term] :
( ( sub @ X3026 @ id )
= X3026 ) )
=> ( ! [X3027: term,X3028: term,X3029: term,X3030: term] :
( ( ( hoasap @ id @ X3027 @ id @ X3029 )
= ( hoasap @ id @ X3028 @ id @ X3030 ) )
=> ( X3027 = X3028 ) )
=> ( ! [X3031: term,X3032: term,X3033: term,X3034: term] :
( ( ( hoasap @ id @ X3031 @ id @ X3033 )
= ( hoasap @ id @ X3032 @ id @ X3034 ) )
=> ( X3033 = X3034 ) )
=> ( ! [X3035: subst > term > term] :
( ! [X3036: subst,X3037: term,X3038: subst] :
( ( sub @ ( X3035 @ X3036 @ X3037 ) @ X3038 )
= ( X3035 @ ( comp @ X3036 @ X3038 ) @ ( sub @ X3037 @ X3038 ) ) )
=> ! [X3039: subst > term > term] :
( ! [X3040: subst,X3041: term,X3042: subst] :
( ( sub @ ( X3039 @ X3040 @ X3041 ) @ X3042 )
= ( X3039 @ ( comp @ X3040 @ X3042 ) @ ( sub @ X3041 @ X3042 ) ) )
=> ( ( ( hoaslam @ id
@ ^ [Z0: subst,Z1: term] : ( X3035 @ Z0 @ Z1 ) )
= ( hoaslam @ id
@ ^ [Z0: subst,Z1: term] : ( X3039 @ Z0 @ Z1 ) ) )
=> ! [X3043: subst,X3044: term] :
( ( X3035 @ X3043 @ X3044 )
= ( X3039 @ X3043 @ X3044 ) ) ) ) )
=> ( ! [X3045: subst > term > term] :
( ! [X3046: subst,X3047: term,X3048: subst] :
( ( sub @ ( X3045 @ X3046 @ X3047 ) @ X3048 )
= ( X3045 @ ( comp @ X3046 @ X3048 ) @ ( sub @ X3047 @ X3048 ) ) )
=> ! [X3049: term,X3050: term] :
( ( hoaslam @ id
@ ^ [Z0: subst,Z1: term] : ( X3045 @ Z0 @ Z1 ) )
!= ( hoasap @ id @ X3049 @ id @ X3050 ) ) )
=> ( ! [X3051: subst > term > term] :
( ! [X3052: subst,X3053: term,X3054: subst] :
( ( sub @ ( X3051 @ X3052 @ X3053 ) @ X3054 )
= ( X3051 @ ( comp @ X3052 @ X3054 ) @ ( sub @ X3053 @ X3054 ) ) )
=> ~ ( var
@ ( sub
@ ( hoaslam @ id
@ ^ [Z0: subst,Z1: term] : ( X3051 @ Z0 @ Z1 ) )
@ id ) ) )
=> ( ! [X3055: term,X3056: term] :
~ ( var @ ( sub @ ( hoasap @ id @ X3055 @ id @ X3056 ) @ id ) )
=> ! [X3057: subst > term > subst > $o] :
( ! [X3058: subst,X3059: term,X3060: subst,X3061: subst] :
( ( X3057 @ X3058 @ X3059 @ ( comp @ X3061 @ X3060 ) )
=> ( X3057 @ ( comp @ X3058 @ X3061 ) @ ( sub @ X3059 @ X3061 ) @ X3060 ) )
=> ( ! [X3062: subst,X3063: term,X3064: subst,X3065: subst] :
( ( X3057 @ ( comp @ X3062 @ X3065 ) @ ( sub @ X3063 @ X3065 ) @ X3064 )
=> ( X3057 @ X3062 @ X3063 @ ( comp @ X3065 @ X3064 ) ) )
=> ( ! [X3066: term] :
( ( var @ ( sub @ X3066 @ id ) )
=> ( X3057 @ id @ X3066 @ id ) )
=> ! [X3067: term] :
( ( var @ X3067 )
=> ( X3057 @ id @ X3067 @ id ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[hoasinduction_lem1_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]),c_0_40]),c_0_41]),c_0_42]),c_0_43]),c_0_44]) ).
thf(c_0_47,negated_conjecture,
~ ( ! [X3373: term,X3374: term,X3375: subst] :
( ( sub @ ( ap @ X3373 @ X3374 ) @ X3375 )
= ( ap @ ( sub @ X3373 @ X3375 ) @ ( sub @ X3374 @ X3375 ) ) )
=> ( ! [X3376: term,X3377: subst] :
( ( sub @ one @ ( push @ X3376 @ X3377 ) )
= X3376 )
=> ( ! [X3378: term] :
( ( sub @ X3378 @ id )
= X3378 )
=> ( ! [X3379: term,X3380: subst] :
( ( sub @ ( lam @ X3379 ) @ X3380 )
= ( lam @ ( sub @ X3379 @ ( push @ one @ ( comp @ X3380 @ sh ) ) ) ) )
=> ( ! [X3381: term,X3382: subst,X3383: subst] :
( ( sub @ ( sub @ X3381 @ X3382 ) @ X3383 )
= ( sub @ X3381 @ ( comp @ X3382 @ X3383 ) ) )
=> ( ! [X3384: subst] :
( ( comp @ id @ X3384 )
= X3384 )
=> ( ! [X3385: term,X3386: subst] :
( ( comp @ sh @ ( push @ X3385 @ X3386 ) )
= X3386 )
=> ( ! [X3387: subst,X3388: subst,X3389: subst] :
( ( comp @ ( comp @ X3387 @ X3388 ) @ X3389 )
= ( comp @ X3387 @ ( comp @ X3388 @ X3389 ) ) )
=> ( ! [X3390: term,X3391: subst,X3392: subst] :
( ( comp @ ( push @ X3390 @ X3391 ) @ X3392 )
= ( push @ ( sub @ X3390 @ X3392 ) @ ( comp @ X3391 @ X3392 ) ) )
=> ( ! [X3393: subst] :
( ( comp @ X3393 @ id )
= X3393 )
=> ( ( ( push @ one @ sh )
= id )
=> ( ! [X3394: subst] :
( ( push @ ( sub @ one @ X3394 ) @ ( comp @ sh @ X3394 ) )
= X3394 )
=> ( ( var @ one )
=> ( ! [X3395: term] :
( ( var @ X3395 )
=> ( var @ ( sub @ X3395 @ sh ) ) )
=> ( ! [X3396: term > $o] :
( ( X3396 @ one )
=> ( ! [X3397: term] :
( ( var @ X3397 )
=> ( ( X3396 @ X3397 )
=> ( X3396 @ ( sub @ X3397 @ sh ) ) ) )
=> ! [X3398: term] :
( ( var @ X3398 )
=> ( X3396 @ X3398 ) ) ) )
=> ( ! [X3399: term,X3400: term,X3401: term,X3402: term] :
( ( ( ap @ X3399 @ X3401 )
= ( ap @ X3400 @ X3402 ) )
=> ( X3399 = X3400 ) )
=> ( ! [X3403: term,X3404: term,X3405: term,X3406: term] :
( ( ( ap @ X3403 @ X3405 )
= ( ap @ X3404 @ X3406 ) )
=> ( X3405 = X3406 ) )
=> ( ! [X3407: term,X3408: term] :
( ( ( lam @ X3407 )
= ( lam @ X3408 ) )
=> ( X3407 = X3408 ) )
=> ( ! [X3409: term,X3410: term] :
( ( ( sub @ X3409 @ sh )
= ( sub @ X3410 @ sh ) )
=> ( X3409 = X3410 ) )
=> ( ! [X3411: term,X3412: term,X3413: term] :
( ( lam @ X3411 )
!= ( ap @ X3412 @ X3413 ) )
=> ( ! [X3414: term,X3415: term] :
~ ( var @ ( ap @ X3414 @ X3415 ) )
=> ( ! [X3416: term] :
~ ( var @ ( lam @ X3416 ) )
=> ( ! [X3417: term > $o] :
( ! [X3418: term] :
( ( var @ X3418 )
=> ( X3417 @ X3418 ) )
=> ( ! [X3419: term,X3420: term] :
( ( X3417 @ X3419 )
=> ( ( X3417 @ X3420 )
=> ( X3417 @ ( ap @ X3419 @ X3420 ) ) ) )
=> ( ! [X3421: term] :
( ( X3417 @ X3421 )
=> ( X3417 @ ( lam @ X3421 ) ) )
=> ! [X3422: term] : ( X3417 @ X3422 ) ) ) )
=> ( ! [X3423: term > $o,X3424: term,X3425: subst] :
( ! [X3426: term] :
( ( var @ X3426 )
=> ( X3423 @ ( sub @ X3426 @ X3425 ) ) )
=> ( ( X3423 @ X3424 )
=> ! [X3427: term] :
( ( var @ X3427 )
=> ( X3423 @ ( sub @ X3427 @ ( push @ X3424 @ X3425 ) ) ) ) ) )
=> ( ! [X3428: term > $o] :
( ! [X3429: term,X3430: term] :
( ( X3428 @ X3429 )
=> ( ( X3428 @ X3430 )
=> ( X3428 @ ( ap @ X3429 @ X3430 ) ) ) )
=> ( ! [X3431: term] :
( ! [X3432: term] :
( ( X3428 @ X3432 )
=> ( X3428 @ ( sub @ X3431 @ ( push @ X3432 @ id ) ) ) )
=> ( X3428 @ ( lam @ X3431 ) ) )
=> ! [X3433: term,X3434: subst] :
( ! [X3435: term] :
( ( var @ X3435 )
=> ( X3428 @ ( sub @ X3435 @ X3434 ) ) )
=> ( X3428 @ ( sub @ X3433 @ X3434 ) ) ) ) )
=> ( ! [X3436: term > $o] :
( ! [X3437: term] :
( ( var @ X3437 )
=> ( X3436 @ X3437 ) )
=> ( ! [X3438: term,X3439: term] :
( ( X3436 @ X3438 )
=> ( ( X3436 @ X3439 )
=> ( X3436 @ ( ap @ X3438 @ X3439 ) ) ) )
=> ( ! [X3440: term] :
( ! [X3441: term] :
( ( X3436 @ X3441 )
=> ( X3436 @ ( sub @ X3440 @ ( push @ X3441 @ id ) ) ) )
=> ( X3436 @ ( lam @ X3440 ) ) )
=> ! [X3442: term] : ( X3436 @ X3442 ) ) ) )
=> ( ( ! [X3443: subst,X3444: subst,X3445: subst] :
( ( comp @ ( comp @ X3443 @ X3444 ) @ X3445 )
= ( comp @ X3443 @ ( comp @ X3444 @ X3445 ) ) )
& ! [X3446: subst] :
( ( comp @ id @ X3446 )
= X3446 )
& ! [X3447: subst] :
( ( comp @ X3447 @ id )
= X3447 ) )
=> ( ( ! [X3448: term,X3449: subst,X3450: subst] :
( ( sub @ ( sub @ X3448 @ X3449 ) @ X3450 )
= ( sub @ X3448 @ ( comp @ X3449 @ X3450 ) ) )
& ! [X3451: term] :
( ( sub @ X3451 @ id )
= X3451 ) )
=> ( ! [X3452: term,X3453: term,X3454: term,X3455: term] :
( ( ( hoasap @ id @ X3452 @ id @ X3454 )
= ( hoasap @ id @ X3453 @ id @ X3455 ) )
=> ( X3452 = X3453 ) )
=> ( ! [X3456: term,X3457: term,X3458: term,X3459: term] :
( ( ( hoasap @ id @ X3456 @ id @ X3458 )
= ( hoasap @ id @ X3457 @ id @ X3459 ) )
=> ( X3458 = X3459 ) )
=> ( ! [X3460: subst > term > term] :
( ! [X3461: subst,X3462: term,X3463: subst] :
( ( sub @ ( X3460 @ X3461 @ X3462 ) @ X3463 )
= ( X3460 @ ( comp @ X3461 @ X3463 ) @ ( sub @ X3462 @ X3463 ) ) )
=> ! [X3464: subst > term > term] :
( ! [X3465: subst,X3466: term,X3467: subst] :
( ( sub @ ( X3464 @ X3465 @ X3466 ) @ X3467 )
= ( X3464 @ ( comp @ X3465 @ X3467 ) @ ( sub @ X3466 @ X3467 ) ) )
=> ( ( ( hoaslam @ id @ X3460 )
= ( hoaslam @ id @ X3464 ) )
=> ! [X3468: subst,X3469: term] :
( ( X3460 @ X3468 @ X3469 )
= ( X3464 @ X3468 @ X3469 ) ) ) ) )
=> ( ! [X3470: subst > term > term] :
( ! [X3471: subst,X3472: term,X3473: subst] :
( ( sub @ ( X3470 @ X3471 @ X3472 ) @ X3473 )
= ( X3470 @ ( comp @ X3471 @ X3473 ) @ ( sub @ X3472 @ X3473 ) ) )
=> ! [X3474: term,X3475: term] :
( ( hoaslam @ id @ X3470 )
!= ( hoasap @ id @ X3474 @ id @ X3475 ) ) )
=> ( ! [X3476: subst > term > term] :
( ! [X3477: subst,X3478: term,X3479: subst] :
( ( sub @ ( X3476 @ X3477 @ X3478 ) @ X3479 )
= ( X3476 @ ( comp @ X3477 @ X3479 ) @ ( sub @ X3478 @ X3479 ) ) )
=> ~ ( var @ ( sub @ ( hoaslam @ id @ X3476 ) @ id ) ) )
=> ( ! [X3480: term,X3481: term] :
~ ( var @ ( sub @ ( hoasap @ id @ X3480 @ id @ X3481 ) @ id ) )
=> ! [X3482: subst > term > subst > $o] :
( ! [X3483: subst,X3484: term,X3485: subst,X3486: subst] :
( ( X3482 @ X3483 @ X3484 @ ( comp @ X3486 @ X3485 ) )
=> ( X3482 @ ( comp @ X3483 @ X3486 ) @ ( sub @ X3484 @ X3486 ) @ X3485 ) )
=> ( ! [X3487: subst,X3488: term,X3489: subst,X3490: subst] :
( ( X3482 @ ( comp @ X3487 @ X3490 ) @ ( sub @ X3488 @ X3490 ) @ X3489 )
=> ( X3482 @ X3487 @ X3488 @ ( comp @ X3490 @ X3489 ) ) )
=> ( ! [X3491: term] :
( ( var @ ( sub @ X3491 @ id ) )
=> ( X3482 @ id @ X3491 @ id ) )
=> ! [X3492: term] :
( ( var @ X3492 )
=> ( X3482 @ id @ X3492 @ id ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[inference(fool_unroll,[status(thm)],[inference(apply_def,[status(thm)],[c_0_45,c_0_46])])]) ).
thf(c_0_48,negated_conjecture,
! [X3505: term,X3506: term,X3507: subst,X3508: term,X3509: subst,X3510: term,X3511: term,X3512: subst,X3513: term,X3514: subst,X3515: subst,X3516: subst,X3517: term,X3518: subst,X3519: subst,X3520: subst,X3521: subst,X3522: term,X3523: subst,X3524: subst,X3525: subst,X3526: subst,X3527: term,X3528: term > $o,X3530: term,X3531: term,X3532: term,X3533: term,X3534: term,X3535: term,X3536: term,X3537: term,X3538: term,X3539: term,X3540: term,X3541: term,X3542: term,X3543: term,X3544: term,X3545: term,X3546: term,X3547: term,X3548: term,X3549: term > $o,X3554: term,X3555: term > $o,X3556: term,X3557: subst,X3559: term,X3560: term > $o,X3564: term,X3565: term,X3566: subst,X3568: term > $o,X3573: term,X3574: term,X3575: subst,X3576: subst,X3577: subst,X3578: subst,X3579: subst,X3580: term,X3581: subst,X3582: subst,X3583: term,X3584: term,X3585: term,X3586: term,X3587: term,X3588: term,X3589: term,X3590: term,X3591: term,X3592: subst > term > term,X3596: subst > term > term,X3600: subst,X3601: term,X3602: subst > term > term,X3606: term,X3607: term,X3608: subst > term > term,X3612: term,X3613: term,X3615: subst,X3616: term,X3617: subst,X3618: subst,X3619: subst,X3620: term,X3621: subst,X3622: subst,X3623: term] :
( ( ( sub @ ( ap @ X3505 @ X3506 ) @ X3507 )
= ( ap @ ( sub @ X3505 @ X3507 ) @ ( sub @ X3506 @ X3507 ) ) )
& ( ( sub @ one @ ( push @ X3508 @ X3509 ) )
= X3508 )
& ( ( sub @ X3510 @ id )
= X3510 )
& ( ( sub @ ( lam @ X3511 ) @ X3512 )
= ( lam @ ( sub @ X3511 @ ( push @ one @ ( comp @ X3512 @ sh ) ) ) ) )
& ( ( sub @ ( sub @ X3513 @ X3514 ) @ X3515 )
= ( sub @ X3513 @ ( comp @ X3514 @ X3515 ) ) )
& ( ( comp @ id @ X3516 )
= X3516 )
& ( ( comp @ sh @ ( push @ X3517 @ X3518 ) )
= X3518 )
& ( ( comp @ ( comp @ X3519 @ X3520 ) @ X3521 )
= ( comp @ X3519 @ ( comp @ X3520 @ X3521 ) ) )
& ( ( comp @ ( push @ X3522 @ X3523 ) @ X3524 )
= ( push @ ( sub @ X3522 @ X3524 ) @ ( comp @ X3523 @ X3524 ) ) )
& ( ( comp @ X3525 @ id )
= X3525 )
& ( ( push @ one @ sh )
= id )
& ( ( push @ ( sub @ one @ X3526 ) @ ( comp @ sh @ X3526 ) )
= X3526 )
& ( var @ one )
& ( ~ ( var @ X3527 )
| ( var @ ( sub @ X3527 @ sh ) ) )
& ( ( var @ ( esk1_1 @ X3528 ) )
| ~ ( var @ X3530 )
| ( X3528 @ X3530 )
| ~ ( X3528 @ one ) )
& ( ( X3528 @ ( esk1_1 @ X3528 ) )
| ~ ( var @ X3530 )
| ( X3528 @ X3530 )
| ~ ( X3528 @ one ) )
& ( ~ ( X3528 @ ( sub @ ( esk1_1 @ X3528 ) @ sh ) )
| ~ ( var @ X3530 )
| ( X3528 @ X3530 )
| ~ ( X3528 @ one ) )
& ( ( ( ap @ X3531 @ X3533 )
!= ( ap @ X3532 @ X3534 ) )
| ( X3531 = X3532 ) )
& ( ( ( ap @ X3535 @ X3537 )
!= ( ap @ X3536 @ X3538 ) )
| ( X3537 = X3538 ) )
& ( ( ( lam @ X3539 )
!= ( lam @ X3540 ) )
| ( X3539 = X3540 ) )
& ( ( ( sub @ X3541 @ sh )
!= ( sub @ X3542 @ sh ) )
| ( X3541 = X3542 ) )
& ( ( lam @ X3543 )
!= ( ap @ X3544 @ X3545 ) )
& ~ ( var @ ( ap @ X3546 @ X3547 ) )
& ~ ( var @ ( lam @ X3548 ) )
& ( ( X3549 @ ( esk5_1 @ X3549 ) )
| ( X3549 @ X3554 )
| ( X3549 @ ( esk3_1 @ X3549 ) )
| ( var @ ( esk2_1 @ X3549 ) ) )
& ( ~ ( X3549 @ ( lam @ ( esk5_1 @ X3549 ) ) )
| ( X3549 @ X3554 )
| ( X3549 @ ( esk3_1 @ X3549 ) )
| ( var @ ( esk2_1 @ X3549 ) ) )
& ( ( X3549 @ ( esk5_1 @ X3549 ) )
| ( X3549 @ X3554 )
| ( X3549 @ ( esk4_1 @ X3549 ) )
| ( var @ ( esk2_1 @ X3549 ) ) )
& ( ~ ( X3549 @ ( lam @ ( esk5_1 @ X3549 ) ) )
| ( X3549 @ X3554 )
| ( X3549 @ ( esk4_1 @ X3549 ) )
| ( var @ ( esk2_1 @ X3549 ) ) )
& ( ( X3549 @ ( esk5_1 @ X3549 ) )
| ( X3549 @ X3554 )
| ~ ( X3549 @ ( ap @ ( esk3_1 @ X3549 ) @ ( esk4_1 @ X3549 ) ) )
| ( var @ ( esk2_1 @ X3549 ) ) )
& ( ~ ( X3549 @ ( lam @ ( esk5_1 @ X3549 ) ) )
| ( X3549 @ X3554 )
| ~ ( X3549 @ ( ap @ ( esk3_1 @ X3549 ) @ ( esk4_1 @ X3549 ) ) )
| ( var @ ( esk2_1 @ X3549 ) ) )
& ( ( X3549 @ ( esk5_1 @ X3549 ) )
| ( X3549 @ X3554 )
| ( X3549 @ ( esk3_1 @ X3549 ) )
| ~ ( X3549 @ ( esk2_1 @ X3549 ) ) )
& ( ~ ( X3549 @ ( lam @ ( esk5_1 @ X3549 ) ) )
| ( X3549 @ X3554 )
| ( X3549 @ ( esk3_1 @ X3549 ) )
| ~ ( X3549 @ ( esk2_1 @ X3549 ) ) )
& ( ( X3549 @ ( esk5_1 @ X3549 ) )
| ( X3549 @ X3554 )
| ( X3549 @ ( esk4_1 @ X3549 ) )
| ~ ( X3549 @ ( esk2_1 @ X3549 ) ) )
& ( ~ ( X3549 @ ( lam @ ( esk5_1 @ X3549 ) ) )
| ( X3549 @ X3554 )
| ( X3549 @ ( esk4_1 @ X3549 ) )
| ~ ( X3549 @ ( esk2_1 @ X3549 ) ) )
& ( ( X3549 @ ( esk5_1 @ X3549 ) )
| ( X3549 @ X3554 )
| ~ ( X3549 @ ( ap @ ( esk3_1 @ X3549 ) @ ( esk4_1 @ X3549 ) ) )
| ~ ( X3549 @ ( esk2_1 @ X3549 ) ) )
& ( ~ ( X3549 @ ( lam @ ( esk5_1 @ X3549 ) ) )
| ( X3549 @ X3554 )
| ~ ( X3549 @ ( ap @ ( esk3_1 @ X3549 ) @ ( esk4_1 @ X3549 ) ) )
| ~ ( X3549 @ ( esk2_1 @ X3549 ) ) )
& ( ( var @ ( esk6_3 @ X3555 @ X3556 @ X3557 ) )
| ~ ( X3555 @ X3556 )
| ~ ( var @ X3559 )
| ( X3555 @ ( sub @ X3559 @ ( push @ X3556 @ X3557 ) ) ) )
& ( ~ ( X3555 @ ( sub @ ( esk6_3 @ X3555 @ X3556 @ X3557 ) @ X3557 ) )
| ~ ( X3555 @ X3556 )
| ~ ( var @ X3559 )
| ( X3555 @ ( sub @ X3559 @ ( push @ X3556 @ X3557 ) ) ) )
& ( ( var @ ( esk10_3 @ X3560 @ X3565 @ X3566 ) )
| ( X3560 @ ( sub @ X3565 @ X3566 ) )
| ~ ( X3560 @ X3564 )
| ( X3560 @ ( sub @ ( esk9_1 @ X3560 ) @ ( push @ X3564 @ id ) ) )
| ( X3560 @ ( esk7_1 @ X3560 ) ) )
& ( ~ ( X3560 @ ( sub @ ( esk10_3 @ X3560 @ X3565 @ X3566 ) @ X3566 ) )
| ( X3560 @ ( sub @ X3565 @ X3566 ) )
| ~ ( X3560 @ X3564 )
| ( X3560 @ ( sub @ ( esk9_1 @ X3560 ) @ ( push @ X3564 @ id ) ) )
| ( X3560 @ ( esk7_1 @ X3560 ) ) )
& ( ( var @ ( esk10_3 @ X3560 @ X3565 @ X3566 ) )
| ( X3560 @ ( sub @ X3565 @ X3566 ) )
| ~ ( X3560 @ ( lam @ ( esk9_1 @ X3560 ) ) )
| ( X3560 @ ( esk7_1 @ X3560 ) ) )
& ( ~ ( X3560 @ ( sub @ ( esk10_3 @ X3560 @ X3565 @ X3566 ) @ X3566 ) )
| ( X3560 @ ( sub @ X3565 @ X3566 ) )
| ~ ( X3560 @ ( lam @ ( esk9_1 @ X3560 ) ) )
| ( X3560 @ ( esk7_1 @ X3560 ) ) )
& ( ( var @ ( esk10_3 @ X3560 @ X3565 @ X3566 ) )
| ( X3560 @ ( sub @ X3565 @ X3566 ) )
| ~ ( X3560 @ X3564 )
| ( X3560 @ ( sub @ ( esk9_1 @ X3560 ) @ ( push @ X3564 @ id ) ) )
| ( X3560 @ ( esk8_1 @ X3560 ) ) )
& ( ~ ( X3560 @ ( sub @ ( esk10_3 @ X3560 @ X3565 @ X3566 ) @ X3566 ) )
| ( X3560 @ ( sub @ X3565 @ X3566 ) )
| ~ ( X3560 @ X3564 )
| ( X3560 @ ( sub @ ( esk9_1 @ X3560 ) @ ( push @ X3564 @ id ) ) )
| ( X3560 @ ( esk8_1 @ X3560 ) ) )
& ( ( var @ ( esk10_3 @ X3560 @ X3565 @ X3566 ) )
| ( X3560 @ ( sub @ X3565 @ X3566 ) )
| ~ ( X3560 @ ( lam @ ( esk9_1 @ X3560 ) ) )
| ( X3560 @ ( esk8_1 @ X3560 ) ) )
& ( ~ ( X3560 @ ( sub @ ( esk10_3 @ X3560 @ X3565 @ X3566 ) @ X3566 ) )
| ( X3560 @ ( sub @ X3565 @ X3566 ) )
| ~ ( X3560 @ ( lam @ ( esk9_1 @ X3560 ) ) )
| ( X3560 @ ( esk8_1 @ X3560 ) ) )
& ( ( var @ ( esk10_3 @ X3560 @ X3565 @ X3566 ) )
| ( X3560 @ ( sub @ X3565 @ X3566 ) )
| ~ ( X3560 @ X3564 )
| ( X3560 @ ( sub @ ( esk9_1 @ X3560 ) @ ( push @ X3564 @ id ) ) )
| ~ ( X3560 @ ( ap @ ( esk7_1 @ X3560 ) @ ( esk8_1 @ X3560 ) ) ) )
& ( ~ ( X3560 @ ( sub @ ( esk10_3 @ X3560 @ X3565 @ X3566 ) @ X3566 ) )
| ( X3560 @ ( sub @ X3565 @ X3566 ) )
| ~ ( X3560 @ X3564 )
| ( X3560 @ ( sub @ ( esk9_1 @ X3560 ) @ ( push @ X3564 @ id ) ) )
| ~ ( X3560 @ ( ap @ ( esk7_1 @ X3560 ) @ ( esk8_1 @ X3560 ) ) ) )
& ( ( var @ ( esk10_3 @ X3560 @ X3565 @ X3566 ) )
| ( X3560 @ ( sub @ X3565 @ X3566 ) )
| ~ ( X3560 @ ( lam @ ( esk9_1 @ X3560 ) ) )
| ~ ( X3560 @ ( ap @ ( esk7_1 @ X3560 ) @ ( esk8_1 @ X3560 ) ) ) )
& ( ~ ( X3560 @ ( sub @ ( esk10_3 @ X3560 @ X3565 @ X3566 ) @ X3566 ) )
| ( X3560 @ ( sub @ X3565 @ X3566 ) )
| ~ ( X3560 @ ( lam @ ( esk9_1 @ X3560 ) ) )
| ~ ( X3560 @ ( ap @ ( esk7_1 @ X3560 ) @ ( esk8_1 @ X3560 ) ) ) )
& ( ~ ( X3568 @ X3573 )
| ( X3568 @ ( sub @ ( esk14_1 @ X3568 ) @ ( push @ X3573 @ id ) ) )
| ( X3568 @ X3574 )
| ( X3568 @ ( esk12_1 @ X3568 ) )
| ( var @ ( esk11_1 @ X3568 ) ) )
& ( ~ ( X3568 @ ( lam @ ( esk14_1 @ X3568 ) ) )
| ( X3568 @ X3574 )
| ( X3568 @ ( esk12_1 @ X3568 ) )
| ( var @ ( esk11_1 @ X3568 ) ) )
& ( ~ ( X3568 @ X3573 )
| ( X3568 @ ( sub @ ( esk14_1 @ X3568 ) @ ( push @ X3573 @ id ) ) )
| ( X3568 @ X3574 )
| ( X3568 @ ( esk13_1 @ X3568 ) )
| ( var @ ( esk11_1 @ X3568 ) ) )
& ( ~ ( X3568 @ ( lam @ ( esk14_1 @ X3568 ) ) )
| ( X3568 @ X3574 )
| ( X3568 @ ( esk13_1 @ X3568 ) )
| ( var @ ( esk11_1 @ X3568 ) ) )
& ( ~ ( X3568 @ X3573 )
| ( X3568 @ ( sub @ ( esk14_1 @ X3568 ) @ ( push @ X3573 @ id ) ) )
| ( X3568 @ X3574 )
| ~ ( X3568 @ ( ap @ ( esk12_1 @ X3568 ) @ ( esk13_1 @ X3568 ) ) )
| ( var @ ( esk11_1 @ X3568 ) ) )
& ( ~ ( X3568 @ ( lam @ ( esk14_1 @ X3568 ) ) )
| ( X3568 @ X3574 )
| ~ ( X3568 @ ( ap @ ( esk12_1 @ X3568 ) @ ( esk13_1 @ X3568 ) ) )
| ( var @ ( esk11_1 @ X3568 ) ) )
& ( ~ ( X3568 @ X3573 )
| ( X3568 @ ( sub @ ( esk14_1 @ X3568 ) @ ( push @ X3573 @ id ) ) )
| ( X3568 @ X3574 )
| ( X3568 @ ( esk12_1 @ X3568 ) )
| ~ ( X3568 @ ( esk11_1 @ X3568 ) ) )
& ( ~ ( X3568 @ ( lam @ ( esk14_1 @ X3568 ) ) )
| ( X3568 @ X3574 )
| ( X3568 @ ( esk12_1 @ X3568 ) )
| ~ ( X3568 @ ( esk11_1 @ X3568 ) ) )
& ( ~ ( X3568 @ X3573 )
| ( X3568 @ ( sub @ ( esk14_1 @ X3568 ) @ ( push @ X3573 @ id ) ) )
| ( X3568 @ X3574 )
| ( X3568 @ ( esk13_1 @ X3568 ) )
| ~ ( X3568 @ ( esk11_1 @ X3568 ) ) )
& ( ~ ( X3568 @ ( lam @ ( esk14_1 @ X3568 ) ) )
| ( X3568 @ X3574 )
| ( X3568 @ ( esk13_1 @ X3568 ) )
| ~ ( X3568 @ ( esk11_1 @ X3568 ) ) )
& ( ~ ( X3568 @ X3573 )
| ( X3568 @ ( sub @ ( esk14_1 @ X3568 ) @ ( push @ X3573 @ id ) ) )
| ( X3568 @ X3574 )
| ~ ( X3568 @ ( ap @ ( esk12_1 @ X3568 ) @ ( esk13_1 @ X3568 ) ) )
| ~ ( X3568 @ ( esk11_1 @ X3568 ) ) )
& ( ~ ( X3568 @ ( lam @ ( esk14_1 @ X3568 ) ) )
| ( X3568 @ X3574 )
| ~ ( X3568 @ ( ap @ ( esk12_1 @ X3568 ) @ ( esk13_1 @ X3568 ) ) )
| ~ ( X3568 @ ( esk11_1 @ X3568 ) ) )
& ( ( comp @ ( comp @ X3575 @ X3576 ) @ X3577 )
= ( comp @ X3575 @ ( comp @ X3576 @ X3577 ) ) )
& ( ( comp @ id @ X3578 )
= X3578 )
& ( ( comp @ X3579 @ id )
= X3579 )
& ( ( sub @ ( sub @ X3580 @ X3581 ) @ X3582 )
= ( sub @ X3580 @ ( comp @ X3581 @ X3582 ) ) )
& ( ( sub @ X3583 @ id )
= X3583 )
& ( ( ( hoasap @ id @ X3584 @ id @ X3586 )
!= ( hoasap @ id @ X3585 @ id @ X3587 ) )
| ( X3584 = X3585 ) )
& ( ( ( hoasap @ id @ X3588 @ id @ X3590 )
!= ( hoasap @ id @ X3589 @ id @ X3591 ) )
| ( X3590 = X3591 ) )
& ( ( ( sub @ ( X3592 @ ( esk15_1 @ X3592 ) @ ( esk16_1 @ X3592 ) ) @ ( esk17_1 @ X3592 ) )
!= ( X3592 @ ( comp @ ( esk15_1 @ X3592 ) @ ( esk17_1 @ X3592 ) ) @ ( sub @ ( esk16_1 @ X3592 ) @ ( esk17_1 @ X3592 ) ) ) )
| ( ( sub @ ( X3596 @ ( esk18_2 @ X3592 @ X3596 ) @ ( esk19_2 @ X3592 @ X3596 ) ) @ ( esk20_2 @ X3592 @ X3596 ) )
!= ( X3596 @ ( comp @ ( esk18_2 @ X3592 @ X3596 ) @ ( esk20_2 @ X3592 @ X3596 ) ) @ ( sub @ ( esk19_2 @ X3592 @ X3596 ) @ ( esk20_2 @ X3592 @ X3596 ) ) ) )
| ( ( hoaslam @ id @ X3592 )
!= ( hoaslam @ id @ X3596 ) )
| ( ( X3592 @ X3600 @ X3601 )
= ( X3596 @ X3600 @ X3601 ) ) )
& ( ( ( sub @ ( X3602 @ ( esk21_1 @ X3602 ) @ ( esk22_1 @ X3602 ) ) @ ( esk23_1 @ X3602 ) )
!= ( X3602 @ ( comp @ ( esk21_1 @ X3602 ) @ ( esk23_1 @ X3602 ) ) @ ( sub @ ( esk22_1 @ X3602 ) @ ( esk23_1 @ X3602 ) ) ) )
| ( ( hoaslam @ id @ X3602 )
!= ( hoasap @ id @ X3606 @ id @ X3607 ) ) )
& ( ( ( sub @ ( X3608 @ ( esk24_1 @ X3608 ) @ ( esk25_1 @ X3608 ) ) @ ( esk26_1 @ X3608 ) )
!= ( X3608 @ ( comp @ ( esk24_1 @ X3608 ) @ ( esk26_1 @ X3608 ) ) @ ( sub @ ( esk25_1 @ X3608 ) @ ( esk26_1 @ X3608 ) ) ) )
| ~ ( var @ ( sub @ ( hoaslam @ id @ X3608 ) @ id ) ) )
& ~ ( var @ ( sub @ ( hoasap @ id @ X3612 @ id @ X3613 ) @ id ) )
& ( ~ ( epred1_0 @ X3615 @ X3616 @ ( comp @ X3618 @ X3617 ) )
| ( epred1_0 @ ( comp @ X3615 @ X3618 ) @ ( sub @ X3616 @ X3618 ) @ X3617 ) )
& ( ~ ( epred1_0 @ ( comp @ X3619 @ X3622 ) @ ( sub @ X3620 @ X3622 ) @ X3621 )
| ( epred1_0 @ X3619 @ X3620 @ ( comp @ X3622 @ X3621 ) ) )
& ( ~ ( var @ ( sub @ X3623 @ id ) )
| ( epred1_0 @ id @ X3623 @ id ) )
& ( var @ esk27_0 )
& ~ ( epred1_0 @ id @ esk27_0 @ id ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_47])])])])])])]) ).
thf(c_0_49,negated_conjecture,
! [X1: term] :
( ( epred1_0 @ id @ X1 @ id )
| ~ ( var @ ( sub @ X1 @ id ) ) ),
inference(split_conjunct,[status(thm)],[c_0_48]) ).
thf(c_0_50,negated_conjecture,
! [X1: term] :
( ( sub @ X1 @ id )
= X1 ),
inference(split_conjunct,[status(thm)],[c_0_48]) ).
thf(c_0_51,negated_conjecture,
! [X1: term] :
( ( epred1_0 @ id @ X1 @ id )
| ~ ( var @ X1 ) ),
inference(rw,[status(thm)],[c_0_49,c_0_50]) ).
thf(c_0_52,negated_conjecture,
var @ esk27_0,
inference(split_conjunct,[status(thm)],[c_0_48]) ).
thf(c_0_53,negated_conjecture,
~ ( epred1_0 @ id @ esk27_0 @ id ),
inference(split_conjunct,[status(thm)],[c_0_48]) ).
thf(c_0_54,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_51,c_0_52]),c_0_53]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG263^1 : TPTP v9.3.1. Bugfixed v5.2.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n008.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Tue Sep 29 17:35:29 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.23 Running higher-order theorem proving
% 0.22/0.26 Running: /export/starexec/sandbox/solver/bin/eprover-ho --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/tmp/tmp.LrETopl8zU/E---3.1_3474163.p
% 0.22/0.34 % Version: 3.5.1-ho
% 0.22/0.34 % Preprocessing class: HSMMSLSSLLLNHFA.
% 0.22/0.34 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.22/0.34 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 0.22/0.34 % Starting post_as_ho1 with 300s (1) cores
% 0.22/0.34 % Starting post_as_ho5 with 300s (1) cores
% 0.22/0.34 % Starting post_as_ho10 with 300s (1) cores
% 0.22/0.34 % post_as_ho1 with pid 3474198 completed with status 0
% 0.22/0.34 % Result found by post_as_ho1
% 0.22/0.34 % Preprocessing class: HSMMSLSSLLLNHFA.
% 0.22/0.34 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.22/0.34 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 0.22/0.34 % Starting post_as_ho1 with 300s (1) cores
% 0.22/0.34 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.22/0.34 % No SInE strategy applied
% 0.22/0.34 % Search class: HGHSM-FFMS31-MHFMMMBN
% 0.22/0.34 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.22/0.34 % Starting SubtermCWHack with 28s (1) cores
% 0.22/0.34 % SubtermCWHack with pid 3474212 completed with status 0
% 0.22/0.34 % Result found by SubtermCWHack
% 0.22/0.34 % Preprocessing class: HSMMSLSSLLLNHFA.
% 0.22/0.34 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.22/0.34 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 0.22/0.34 % Starting post_as_ho1 with 300s (1) cores
% 0.22/0.34 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.22/0.34 % No SInE strategy applied
% 0.22/0.34 % Search class: HGHSM-FFMS31-MHFMMMBN
% 0.22/0.34 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.22/0.34 % Starting SubtermCWHack with 28s (1) cores
% 0.22/0.34 % Preprocessing time : 0.003 s
% 0.22/0.34
% 0.22/0.34 % Proof found!
% 0.22/0.34 % SZS status Theorem
% 0.22/0.34 % SZS output start CNFRefutation
% See solution above
% 0.22/0.34 % Parsed axioms : 238
% 0.22/0.34 % Removed by relevancy pruning/SinE : 0
% 0.22/0.34 % Initial clauses : 204
% 0.22/0.34 % Removed in clause preprocessing : 124
% 0.22/0.34 % Initial clauses in saturation : 80
% 0.22/0.34 % Processed clauses : 18
% 0.22/0.34 % ...of these trivial : 3
% 0.22/0.34 % ...subsumed : 0
% 0.22/0.34 % ...remaining for further processing : 15
% 0.22/0.34 % Other redundant clauses eliminated : 0
% 0.22/0.34 % Clauses deleted for lack of memory : 0
% 0.22/0.34 % Backward-subsumed : 0
% 0.22/0.34 % Backward-rewritten : 0
% 0.22/0.34 % Generated clauses : 6
% 0.22/0.34 % ...of the previous two non-redundant : 0
% 0.22/0.34 % ...aggressively subsumed : 0
% 0.22/0.34 % Contextual simplify-reflections : 0
% 0.22/0.34 % Paramodulations : 5
% 0.22/0.34 % Factorizations : 0
% 0.22/0.34 % NegExts : 0
% 0.22/0.34 % Equation resolutions : 1
% 0.22/0.34 % Disequality decompositions : 0
% 0.22/0.34 % Total rewrite steps : 6
% 0.22/0.34 % ...of those cached : 1
% 0.22/0.34 % Propositional unsat checks : 0
% 0.22/0.34 % Propositional check models : 0
% 0.22/0.34 % Propositional check unsatisfiable : 0
% 0.22/0.34 % Propositional clauses : 0
% 0.22/0.34 % Propositional clauses after purity: 0
% 0.22/0.34 % Propositional unsat core size : 0
% 0.22/0.34 % Propositional preprocessing time : 0.000
% 0.22/0.34 % Propositional encoding time : 0.000
% 0.22/0.34 % Propositional solver time : 0.000
% 0.22/0.34 % Success case prop preproc time : 0.000
% 0.22/0.34 % Success case prop encoding time : 0.000
% 0.22/0.34 % Success case prop solver time : 0.000
% 0.22/0.34 % Current number of processed clauses : 15
% 0.22/0.34 % Positive orientable unit clauses : 8
% 0.22/0.34 % Positive unorientable unit clauses: 0
% 0.22/0.34 % Negative unit clauses : 4
% 0.22/0.34 % Non-unit-clauses : 3
% 0.22/0.34 % Current number of unprocessed clauses: 62
% 0.22/0.34 % ...number of literals in the above : 209
% 0.22/0.34 % Current number of archived formulas : 0
% 0.22/0.34 % Current number of archived clauses : 0
% 0.22/0.34 % Clause-clause subsumption calls (NU) : 0
% 0.22/0.34 % Rec. Clause-clause subsumption calls : 0
% 0.22/0.34 % Non-unit clause-clause subsumptions : 0
% 0.22/0.34 % Unit Clause-clause subsumption calls : 0
% 0.22/0.34 % Rewrite failures with RHS unbound : 0
% 0.22/0.34 % BW rewrite match attempts : 0
% 0.22/0.34 % BW rewrite match successes : 0
% 0.22/0.34 % Condensation attempts : 0
% 0.22/0.34 % Condensation successes : 0
% 0.22/0.34 % Termbank termtop insertions : 33385
% 0.22/0.34 % Search garbage collected termcells : 4461
% 0.22/0.34
% 0.22/0.34 % -------------------------------------------------
% 0.22/0.34 % User time : 0.037 s
% 0.22/0.34 % System time : 0.010 s
% 0.22/0.34 % Total time : 0.047 s
% 0.22/0.34 % Maximum resident set size: 8076 pages
% 0.22/0.34
% 0.22/0.34 % -------------------------------------------------
% 0.22/0.34 % User time : 0.046 s
% 0.22/0.34 % System time : 0.016 s
% 0.22/0.34 % Total time : 0.063 s
% 0.22/0.34 % Maximum resident set size: 5376 pages
% 0.22/0.34 % E exiting
%------------------------------------------------------------------------------