%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ALG267^1 : TPTP v9.3.1. Bugfixed v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n005.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:48 AM UTC 2026
% Result : Theorem 0.62s 0.39s
% Output : CNFRefutation 0.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 40
% Syntax : Number of formulae : 57 ( 15 unt; 0 typ; 0 def)
% Number of atoms : 357 ( 171 equ; 0 cnn)
% Maximal formula atoms : 82 ( 6 avg)
% Number of connectives : 3474 ( 178 ~; 239 |; 102 &;2613 @)
% ( 41 <=>; 301 =>; 0 <=; 0 <~>)
% Maximal formula depth : 183 ( 10 avg)
% Number of types : 3 ( 2 usr)
% Number of type conns : 103 ( 103 >; 0 *; 0 +; 0 <<)
% Number of symbols : 98 ( 96 usr; 43 con; 0-4 aty)
% Number of variables : 567 ( 32 ^; 532 !; 3 ?; 567 :)
% 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_59,type,
hoasinduction_lem2: $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_80,type,
hoasinduction_lem3b_gthm: $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_120,type,
hoasinduction_lem3b: $o ).
thf(decl_121,type,
substmonoid: $o ).
thf(decl_122,type,
lamnotvar: $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,
esk27_1: ( subst > term > subst > $o ) > subst ).
thf(decl_172,type,
esk28_1: ( subst > term > subst > $o ) > term ).
thf(decl_173,type,
esk29_1: ( subst > term > subst > $o ) > subst ).
thf(decl_174,type,
esk30_1: ( subst > term > subst > $o ) > subst ).
thf(decl_175,type,
esk31_1: ( subst > term > subst > $o ) > subst ).
thf(decl_176,type,
esk32_1: ( subst > term > subst > $o ) > term ).
thf(decl_177,type,
esk33_1: ( subst > term > subst > $o ) > subst ).
thf(decl_178,type,
esk34_1: ( subst > term > subst > $o ) > subst ).
thf(decl_179,type,
esk35_1: ( subst > term > subst > $o ) > term ).
thf(decl_180,type,
esk36_1: ( subst > term > subst > $o ) > subst ).
thf(decl_181,type,
esk37_1: ( subst > term > subst > $o ) > term ).
thf(decl_182,type,
esk38_1: ( subst > term > subst > $o ) > subst ).
thf(decl_183,type,
esk39_1: ( subst > term > subst > $o ) > subst ).
thf(decl_184,type,
esk40_1: ( subst > term > subst > $o ) > subst ).
thf(decl_185,type,
esk41_1: ( subst > term > subst > $o ) > term ).
thf(decl_186,type,
esk42_1: ( subst > term > subst > $o ) > subst ).
thf(decl_187,type,
esk43_1: ( subst > term > subst > $o ) > subst ).
thf(decl_188,type,
esk44_1: ( subst > term > subst > $o ) > term ).
thf(decl_189,type,
esk45_1: ( subst > term > subst > $o ) > term ).
thf(decl_190,type,
esk46_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/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.p',hoaslamnotvar) ).
thf(hoasvar,axiom,
( hoasvar
= ( ^ [X3: subst,X1: term,X4: subst] : ( var @ ( sub @ X1 @ X4 ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.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/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.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/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.p',hoaslamnotap) ).
thf(hoasapnotvar,axiom,
( hoasapnotvar
<=> ! [X1: term,X2: term] :
~ ( hoasvar @ id @ ( hoasap @ id @ X1 @ id @ X2 ) @ id ) ),
file('/export/starexec/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.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/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.p',hoasinduction_lem1) ).
thf(thm,conjecture,
hoasinduction_lem3b_gthm,
file('/export/starexec/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.p',thm) ).
thf(hoasinduction_lem3b_gthm,axiom,
( hoasinduction_lem3b_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
=> ( hoasinduction_lem2
=> hoasinduction_lem3b ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.p',hoasinduction_lem3b_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/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.p',axapp) ).
thf(axvarcons,axiom,
( axvarcons
<=> ! [X1: term,X3: subst] :
( ( sub @ one @ ( push @ X1 @ X3 ) )
= X1 ) ),
file('/export/starexec/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.p',axvarcons) ).
thf(axvarid,axiom,
( axvarid
<=> ! [X1: term] :
( ( sub @ X1 @ id )
= X1 ) ),
file('/export/starexec/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.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/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.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/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.p',axclos) ).
thf(axidl,axiom,
( axidl
<=> ! [X3: subst] :
( ( comp @ id @ X3 )
= X3 ) ),
file('/export/starexec/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.p',axidl) ).
thf(axshiftcons,axiom,
( axshiftcons
<=> ! [X1: term,X3: subst] :
( ( comp @ sh @ ( push @ X1 @ X3 ) )
= X3 ) ),
file('/export/starexec/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.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/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.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/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.p',axmap) ).
thf(axidr,axiom,
( axidr
<=> ! [X3: subst] :
( ( comp @ X3 @ id )
= X3 ) ),
file('/export/starexec/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.p',axidr) ).
thf(axvarshift,axiom,
( axvarshift
<=> ( ( push @ one @ sh )
= id ) ),
file('/export/starexec/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.p',axvarshift) ).
thf(axscons,axiom,
( axscons
<=> ! [X3: subst] :
( ( push @ ( sub @ one @ X3 ) @ ( comp @ sh @ X3 ) )
= X3 ) ),
file('/export/starexec/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.p',axscons) ).
thf(ulamvar1,axiom,
( ulamvar1
<=> ( var @ one ) ),
file('/export/starexec/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.p',ulamvar1) ).
thf(ulamvarsh,axiom,
( ulamvarsh
<=> ! [X1: term] :
( ( var @ X1 )
=> ( var @ ( sub @ X1 @ sh ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.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/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.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/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.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/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.p',apinj2) ).
thf(laminj,axiom,
( laminj
<=> ! [X1: term,X2: term] :
( ( ( lam @ X1 )
= ( lam @ X2 ) )
=> ( X1 = X2 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.p',laminj) ).
thf(shinj,axiom,
( shinj
<=> ! [X1: term,X2: term] :
( ( ( sub @ X1 @ sh )
= ( sub @ X2 @ sh ) )
=> ( X1 = X2 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.p',shinj) ).
thf(lamnotap,axiom,
( lamnotap
<=> ! [X1: term,X2: term,X7: term] :
( ( lam @ X1 )
!= ( ap @ X2 @ X7 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.p',lamnotap) ).
thf(apnotvar,axiom,
( apnotvar
<=> ! [X1: term,X2: term] :
~ ( var @ ( ap @ X1 @ X2 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.p',apnotvar) ).
thf(lamnotvar,axiom,
( lamnotvar
<=> ! [X1: term] :
~ ( var @ ( lam @ X1 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.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/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.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/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.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/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.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/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.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/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.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/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.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/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.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/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.p',hoasapinj2) ).
thf(hoasinduction_lem2,axiom,
( hoasinduction_lem2
<=> ! [X21: subst > term > subst > $o] :
( ! [X3: subst,X1: term,X4: subst,X5: subst] :
( ( X21 @ X3 @ X1 @ ( comp @ X5 @ X4 ) )
=> ( X21 @ ( comp @ X3 @ X5 ) @ ( sub @ X1 @ X5 ) @ X4 ) )
=> ( ! [X3: subst,X1: term,X4: subst,X5: subst] :
( ( X21 @ ( comp @ X3 @ X5 ) @ ( sub @ X1 @ X5 ) @ X4 )
=> ( X21 @ X3 @ X1 @ ( comp @ X5 @ X4 ) ) )
=> ( ! [X1: term,X2: term] :
( ( X21 @ id @ X1 @ id )
=> ( ( X21 @ id @ X2 @ id )
=> ( X21 @ id @ ( hoasap @ id @ X1 @ id @ X2 ) @ id ) ) )
=> ! [X1: term,X2: term] :
( ( X21 @ id @ X1 @ id )
=> ( ( X21 @ id @ X2 @ id )
=> ( X21 @ id @ ( ap @ X1 @ X2 ) @ id ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.p',hoasinduction_lem2) ).
thf(hoasinduction_lem3b,axiom,
( hoasinduction_lem3b
<=> ! [X2: term] :
? [X12: subst > term > term] :
( ( sub @ X2 @ ( push @ one @ sh ) )
= ( X12 @ sh @ one ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.p',hoasinduction_lem3b) ).
thf(c_0_40,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_41,plain,
( hoasvar
= ( ^ [Z0: subst,Z1: term,Z2: subst] : ( var @ ( sub @ Z1 @ Z2 ) ) ) ),
inference(fof_simplification,[status(thm)],[hoasvar]) ).
thf(c_0_42,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_43,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_44,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_40,c_0_41]) ).
thf(c_0_45,axiom,
( hoasapnotvar
= ( ! [X1: term,X2: term] :
~ ( var @ ( sub @ ( hoasap @ id @ X1 @ id @ X2 ) @ id ) ) ) ),
inference(apply_def,[status(thm)],[hoasapnotvar,c_0_41]) ).
thf(c_0_46,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_41]) ).
thf(c_0_47,negated_conjecture,
~ hoasinduction_lem3b_gthm,
inference(assume_negation,[status(cth)],[thm]) ).
thf(c_0_48,axiom,
( hoasinduction_lem3b_gthm
= ( ! [X1581: term,X1582: term,X1583: subst] :
( ( sub @ ( ap @ X1581 @ X1582 ) @ X1583 )
= ( ap @ ( sub @ X1581 @ X1583 ) @ ( sub @ X1582 @ X1583 ) ) )
=> ( ! [X1584: term,X1585: subst] :
( ( sub @ one @ ( push @ X1584 @ X1585 ) )
= X1584 )
=> ( ! [X1586: term] :
( ( sub @ X1586 @ id )
= X1586 )
=> ( ! [X1587: term,X1588: subst] :
( ( sub @ ( lam @ X1587 ) @ X1588 )
= ( lam @ ( sub @ X1587 @ ( push @ one @ ( comp @ X1588 @ sh ) ) ) ) )
=> ( ! [X1589: term,X1590: subst,X1591: subst] :
( ( sub @ ( sub @ X1589 @ X1590 ) @ X1591 )
= ( sub @ X1589 @ ( comp @ X1590 @ X1591 ) ) )
=> ( ! [X1592: subst] :
( ( comp @ id @ X1592 )
= X1592 )
=> ( ! [X1593: term,X1594: subst] :
( ( comp @ sh @ ( push @ X1593 @ X1594 ) )
= X1594 )
=> ( ! [X1595: subst,X1596: subst,X1597: subst] :
( ( comp @ ( comp @ X1595 @ X1596 ) @ X1597 )
= ( comp @ X1595 @ ( comp @ X1596 @ X1597 ) ) )
=> ( ! [X1598: term,X1599: subst,X1600: subst] :
( ( comp @ ( push @ X1598 @ X1599 ) @ X1600 )
= ( push @ ( sub @ X1598 @ X1600 ) @ ( comp @ X1599 @ X1600 ) ) )
=> ( ! [X1601: subst] :
( ( comp @ X1601 @ id )
= X1601 )
=> ( ( ( push @ one @ sh )
= id )
=> ( ! [X1602: subst] :
( ( push @ ( sub @ one @ X1602 ) @ ( comp @ sh @ X1602 ) )
= X1602 )
=> ( ( var @ one )
=> ( ! [X1603: term] :
( ( var @ X1603 )
=> ( var @ ( sub @ X1603 @ sh ) ) )
=> ( ! [X1604: term > $o] :
( ( X1604 @ one )
=> ( ! [X1605: term] :
( ( var @ X1605 )
=> ( ( X1604 @ X1605 )
=> ( X1604 @ ( sub @ X1605 @ sh ) ) ) )
=> ! [X1606: term] :
( ( var @ X1606 )
=> ( X1604 @ X1606 ) ) ) )
=> ( ! [X1607: term,X1608: term,X1609: term,X1610: term] :
( ( ( ap @ X1607 @ X1609 )
= ( ap @ X1608 @ X1610 ) )
=> ( X1607 = X1608 ) )
=> ( ! [X1611: term,X1612: term,X1613: term,X1614: term] :
( ( ( ap @ X1611 @ X1613 )
= ( ap @ X1612 @ X1614 ) )
=> ( X1613 = X1614 ) )
=> ( ! [X1615: term,X1616: term] :
( ( ( lam @ X1615 )
= ( lam @ X1616 ) )
=> ( X1615 = X1616 ) )
=> ( ! [X1617: term,X1618: term] :
( ( ( sub @ X1617 @ sh )
= ( sub @ X1618 @ sh ) )
=> ( X1617 = X1618 ) )
=> ( ! [X1619: term,X1620: term,X1621: term] :
( ( lam @ X1619 )
!= ( ap @ X1620 @ X1621 ) )
=> ( ! [X1622: term,X1623: term] :
~ ( var @ ( ap @ X1622 @ X1623 ) )
=> ( ! [X1624: term] :
~ ( var @ ( lam @ X1624 ) )
=> ( ! [X1625: term > $o] :
( ! [X1626: term] :
( ( var @ X1626 )
=> ( X1625 @ X1626 ) )
=> ( ! [X1627: term,X1628: term] :
( ( X1625 @ X1627 )
=> ( ( X1625 @ X1628 )
=> ( X1625 @ ( ap @ X1627 @ X1628 ) ) ) )
=> ( ! [X1629: term] :
( ( X1625 @ X1629 )
=> ( X1625 @ ( lam @ X1629 ) ) )
=> ! [X1630: term] : ( X1625 @ X1630 ) ) ) )
=> ( ! [X1631: term > $o,X1632: term,X1633: subst] :
( ! [X1634: term] :
( ( var @ X1634 )
=> ( X1631 @ ( sub @ X1634 @ X1633 ) ) )
=> ( ( X1631 @ X1632 )
=> ! [X1635: term] :
( ( var @ X1635 )
=> ( X1631 @ ( sub @ X1635 @ ( push @ X1632 @ X1633 ) ) ) ) ) )
=> ( ! [X1636: term > $o] :
( ! [X1637: term,X1638: term] :
( ( X1636 @ X1637 )
=> ( ( X1636 @ X1638 )
=> ( X1636 @ ( ap @ X1637 @ X1638 ) ) ) )
=> ( ! [X1639: term] :
( ! [X1640: term] :
( ( X1636 @ X1640 )
=> ( X1636 @ ( sub @ X1639 @ ( push @ X1640 @ id ) ) ) )
=> ( X1636 @ ( lam @ X1639 ) ) )
=> ! [X1641: term,X1642: subst] :
( ! [X1643: term] :
( ( var @ X1643 )
=> ( X1636 @ ( sub @ X1643 @ X1642 ) ) )
=> ( X1636 @ ( sub @ X1641 @ X1642 ) ) ) ) )
=> ( ! [X1644: term > $o] :
( ! [X1645: term] :
( ( var @ X1645 )
=> ( X1644 @ X1645 ) )
=> ( ! [X1646: term,X1647: term] :
( ( X1644 @ X1646 )
=> ( ( X1644 @ X1647 )
=> ( X1644 @ ( ap @ X1646 @ X1647 ) ) ) )
=> ( ! [X1648: term] :
( ! [X1649: term] :
( ( X1644 @ X1649 )
=> ( X1644 @ ( sub @ X1648 @ ( push @ X1649 @ id ) ) ) )
=> ( X1644 @ ( lam @ X1648 ) ) )
=> ! [X1650: term] : ( X1644 @ X1650 ) ) ) )
=> ( ( ! [X1651: subst,X1652: subst,X1653: subst] :
( ( comp @ ( comp @ X1651 @ X1652 ) @ X1653 )
= ( comp @ X1651 @ ( comp @ X1652 @ X1653 ) ) )
& ! [X1654: subst] :
( ( comp @ id @ X1654 )
= X1654 )
& ! [X1655: subst] :
( ( comp @ X1655 @ id )
= X1655 ) )
=> ( ( ! [X1656: term,X1657: subst,X1658: subst] :
( ( sub @ ( sub @ X1656 @ X1657 ) @ X1658 )
= ( sub @ X1656 @ ( comp @ X1657 @ X1658 ) ) )
& ! [X1659: term] :
( ( sub @ X1659 @ id )
= X1659 ) )
=> ( ! [X1660: term,X1661: term,X1662: term,X1663: term] :
( ( ( hoasap @ id @ X1660 @ id @ X1662 )
= ( hoasap @ id @ X1661 @ id @ X1663 ) )
=> ( X1660 = X1661 ) )
=> ( ! [X1664: term,X1665: term,X1666: term,X1667: term] :
( ( ( hoasap @ id @ X1664 @ id @ X1666 )
= ( hoasap @ id @ X1665 @ id @ X1667 ) )
=> ( X1666 = X1667 ) )
=> ( ! [X1668: subst > term > term] :
( ! [X1669: subst,X1670: term,X1671: subst] :
( ( sub @ ( X1668 @ X1669 @ X1670 ) @ X1671 )
= ( X1668 @ ( comp @ X1669 @ X1671 ) @ ( sub @ X1670 @ X1671 ) ) )
=> ! [X1672: subst > term > term] :
( ! [X1673: subst,X1674: term,X1675: subst] :
( ( sub @ ( X1672 @ X1673 @ X1674 ) @ X1675 )
= ( X1672 @ ( comp @ X1673 @ X1675 ) @ ( sub @ X1674 @ X1675 ) ) )
=> ( ( ( hoaslam @ id
@ ^ [Z0: subst,Z1: term] : ( X1668 @ Z0 @ Z1 ) )
= ( hoaslam @ id
@ ^ [Z0: subst,Z1: term] : ( X1672 @ Z0 @ Z1 ) ) )
=> ! [X1676: subst,X1677: term] :
( ( X1668 @ X1676 @ X1677 )
= ( X1672 @ X1676 @ X1677 ) ) ) ) )
=> ( ! [X1678: subst > term > term] :
( ! [X1679: subst,X1680: term,X1681: subst] :
( ( sub @ ( X1678 @ X1679 @ X1680 ) @ X1681 )
= ( X1678 @ ( comp @ X1679 @ X1681 ) @ ( sub @ X1680 @ X1681 ) ) )
=> ! [X1682: term,X1683: term] :
( ( hoaslam @ id
@ ^ [Z0: subst,Z1: term] : ( X1678 @ Z0 @ Z1 ) )
!= ( hoasap @ id @ X1682 @ id @ X1683 ) ) )
=> ( ! [X1684: subst > term > term] :
( ! [X1685: subst,X1686: term,X1687: subst] :
( ( sub @ ( X1684 @ X1685 @ X1686 ) @ X1687 )
= ( X1684 @ ( comp @ X1685 @ X1687 ) @ ( sub @ X1686 @ X1687 ) ) )
=> ~ ( var
@ ( sub
@ ( hoaslam @ id
@ ^ [Z0: subst,Z1: term] : ( X1684 @ Z0 @ Z1 ) )
@ id ) ) )
=> ( ! [X1688: term,X1689: term] :
~ ( var @ ( sub @ ( hoasap @ id @ X1688 @ id @ X1689 ) @ id ) )
=> ( ! [X1690: subst > term > subst > $o] :
( ! [X1691: subst,X1692: term,X1693: subst,X1694: subst] :
( ( X1690 @ X1691 @ X1692 @ ( comp @ X1694 @ X1693 ) )
=> ( X1690 @ ( comp @ X1691 @ X1694 ) @ ( sub @ X1692 @ X1694 ) @ X1693 ) )
=> ( ! [X1695: subst,X1696: term,X1697: subst,X1698: subst] :
( ( X1690 @ ( comp @ X1695 @ X1698 ) @ ( sub @ X1696 @ X1698 ) @ X1697 )
=> ( X1690 @ X1695 @ X1696 @ ( comp @ X1698 @ X1697 ) ) )
=> ( ! [X1699: term] :
( ( var @ ( sub @ X1699 @ id ) )
=> ( X1690 @ id @ X1699 @ id ) )
=> ! [X1700: term] :
( ( var @ X1700 )
=> ( X1690 @ id @ X1700 @ id ) ) ) ) )
=> ( ! [X1701: subst > term > subst > $o] :
( ! [X1702: subst,X1703: term,X1704: subst,X1705: subst] :
( ( X1701 @ X1702 @ X1703 @ ( comp @ X1705 @ X1704 ) )
=> ( X1701 @ ( comp @ X1702 @ X1705 ) @ ( sub @ X1703 @ X1705 ) @ X1704 ) )
=> ( ! [X1706: subst,X1707: term,X1708: subst,X1709: subst] :
( ( X1701 @ ( comp @ X1706 @ X1709 ) @ ( sub @ X1707 @ X1709 ) @ X1708 )
=> ( X1701 @ X1706 @ X1707 @ ( comp @ X1709 @ X1708 ) ) )
=> ( ! [X1710: term,X1711: term] :
( ( X1701 @ id @ X1710 @ id )
=> ( ( X1701 @ id @ X1711 @ id )
=> ( X1701 @ id @ ( hoasap @ id @ X1710 @ id @ X1711 ) @ id ) ) )
=> ! [X1712: term,X1713: term] :
( ( X1701 @ id @ X1712 @ id )
=> ( ( X1701 @ id @ X1713 @ id )
=> ( X1701 @ id @ ( ap @ X1712 @ X1713 ) @ id ) ) ) ) ) )
=> ! [X1714: term] :
? [X1715: subst > term > term] :
( ( sub @ X1714 @ ( push @ one @ sh ) )
= ( X1715 @ sh @ one ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
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)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[hoasinduction_lem3b_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]),c_0_41]),hoasapinj1]),hoasapinj2]),c_0_42]),c_0_43]),c_0_44]),c_0_45]),c_0_46]),hoasinduction_lem2]),hoasinduction_lem3b]) ).
thf(c_0_49,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 ) ) ) ) )
=> ( ! [X3493: subst > term > subst > $o] :
( ! [X3494: subst,X3495: term,X3496: subst,X3497: subst] :
( ( X3493 @ X3494 @ X3495 @ ( comp @ X3497 @ X3496 ) )
=> ( X3493 @ ( comp @ X3494 @ X3497 ) @ ( sub @ X3495 @ X3497 ) @ X3496 ) )
=> ( ! [X3498: subst,X3499: term,X3500: subst,X3501: subst] :
( ( X3493 @ ( comp @ X3498 @ X3501 ) @ ( sub @ X3499 @ X3501 ) @ X3500 )
=> ( X3493 @ X3498 @ X3499 @ ( comp @ X3501 @ X3500 ) ) )
=> ( ! [X3502: term,X3503: term] :
( ( X3493 @ id @ X3502 @ id )
=> ( ( X3493 @ id @ X3503 @ id )
=> ( X3493 @ id @ ( hoasap @ id @ X3502 @ id @ X3503 ) @ id ) ) )
=> ! [X3504: term,X3505: term] :
( ( X3493 @ id @ X3504 @ id )
=> ( ( X3493 @ id @ X3505 @ id )
=> ( X3493 @ id @ ( ap @ X3504 @ X3505 ) @ id ) ) ) ) ) )
=> ! [X3506: term] :
? [X3507: subst > term > term] :
( ( sub @ X3506 @ ( push @ one @ sh ) )
= ( X3507 @ sh @ one ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[inference(fool_unroll,[status(thm)],[inference(apply_def,[status(thm)],[c_0_47,c_0_48])])]) ).
thf(c_0_50,negated_conjecture,
! [X3520: term,X3521: term,X3522: subst,X3523: term,X3524: subst,X3525: term,X3526: term,X3527: subst,X3528: term,X3529: subst,X3530: subst,X3531: subst,X3532: term,X3533: subst,X3534: subst,X3535: subst,X3536: subst,X3537: term,X3538: subst,X3539: subst,X3540: subst,X3541: subst,X3542: term,X3543: term > $o,X3545: term,X3546: term,X3547: term,X3548: term,X3549: term,X3550: term,X3551: term,X3552: term,X3553: term,X3554: term,X3555: term,X3556: term,X3557: term,X3558: term,X3559: term,X3560: term,X3561: term,X3562: term,X3563: term,X3564: term > $o,X3569: term,X3570: term > $o,X3571: term,X3572: subst,X3574: term,X3575: term > $o,X3579: term,X3580: term,X3581: subst,X3583: term > $o,X3588: term,X3589: term,X3590: subst,X3591: subst,X3592: subst,X3593: subst,X3594: subst,X3595: term,X3596: subst,X3597: subst,X3598: term,X3599: term,X3600: term,X3601: term,X3602: term,X3603: term,X3604: term,X3605: term,X3606: term,X3607: subst > term > term,X3611: subst > term > term,X3615: subst,X3616: term,X3617: subst > term > term,X3621: term,X3622: term,X3623: subst > term > term,X3627: term,X3628: term,X3629: subst > term > subst > $o,X3639: term,X3640: subst > term > subst > $o,X3651: term,X3652: term,X3654: subst > term > term] :
( ( ( sub @ ( ap @ X3520 @ X3521 ) @ X3522 )
= ( ap @ ( sub @ X3520 @ X3522 ) @ ( sub @ X3521 @ X3522 ) ) )
& ( ( sub @ one @ ( push @ X3523 @ X3524 ) )
= X3523 )
& ( ( sub @ X3525 @ id )
= X3525 )
& ( ( sub @ ( lam @ X3526 ) @ X3527 )
= ( lam @ ( sub @ X3526 @ ( push @ one @ ( comp @ X3527 @ sh ) ) ) ) )
& ( ( sub @ ( sub @ X3528 @ X3529 ) @ X3530 )
= ( sub @ X3528 @ ( comp @ X3529 @ X3530 ) ) )
& ( ( comp @ id @ X3531 )
= X3531 )
& ( ( comp @ sh @ ( push @ X3532 @ X3533 ) )
= X3533 )
& ( ( comp @ ( comp @ X3534 @ X3535 ) @ X3536 )
= ( comp @ X3534 @ ( comp @ X3535 @ X3536 ) ) )
& ( ( comp @ ( push @ X3537 @ X3538 ) @ X3539 )
= ( push @ ( sub @ X3537 @ X3539 ) @ ( comp @ X3538 @ X3539 ) ) )
& ( ( comp @ X3540 @ id )
= X3540 )
& ( ( push @ one @ sh )
= id )
& ( ( push @ ( sub @ one @ X3541 ) @ ( comp @ sh @ X3541 ) )
= X3541 )
& ( var @ one )
& ( ~ ( var @ X3542 )
| ( var @ ( sub @ X3542 @ sh ) ) )
& ( ( var @ ( esk1_1 @ X3543 ) )
| ~ ( var @ X3545 )
| ( X3543 @ X3545 )
| ~ ( X3543 @ one ) )
& ( ( X3543 @ ( esk1_1 @ X3543 ) )
| ~ ( var @ X3545 )
| ( X3543 @ X3545 )
| ~ ( X3543 @ one ) )
& ( ~ ( X3543 @ ( sub @ ( esk1_1 @ X3543 ) @ sh ) )
| ~ ( var @ X3545 )
| ( X3543 @ X3545 )
| ~ ( X3543 @ one ) )
& ( ( ( ap @ X3546 @ X3548 )
!= ( ap @ X3547 @ X3549 ) )
| ( X3546 = X3547 ) )
& ( ( ( ap @ X3550 @ X3552 )
!= ( ap @ X3551 @ X3553 ) )
| ( X3552 = X3553 ) )
& ( ( ( lam @ X3554 )
!= ( lam @ X3555 ) )
| ( X3554 = X3555 ) )
& ( ( ( sub @ X3556 @ sh )
!= ( sub @ X3557 @ sh ) )
| ( X3556 = X3557 ) )
& ( ( lam @ X3558 )
!= ( ap @ X3559 @ X3560 ) )
& ~ ( var @ ( ap @ X3561 @ X3562 ) )
& ~ ( var @ ( lam @ X3563 ) )
& ( ( X3564 @ ( esk5_1 @ X3564 ) )
| ( X3564 @ X3569 )
| ( X3564 @ ( esk3_1 @ X3564 ) )
| ( var @ ( esk2_1 @ X3564 ) ) )
& ( ~ ( X3564 @ ( lam @ ( esk5_1 @ X3564 ) ) )
| ( X3564 @ X3569 )
| ( X3564 @ ( esk3_1 @ X3564 ) )
| ( var @ ( esk2_1 @ X3564 ) ) )
& ( ( X3564 @ ( esk5_1 @ X3564 ) )
| ( X3564 @ X3569 )
| ( X3564 @ ( esk4_1 @ X3564 ) )
| ( var @ ( esk2_1 @ X3564 ) ) )
& ( ~ ( X3564 @ ( lam @ ( esk5_1 @ X3564 ) ) )
| ( X3564 @ X3569 )
| ( X3564 @ ( esk4_1 @ X3564 ) )
| ( var @ ( esk2_1 @ X3564 ) ) )
& ( ( X3564 @ ( esk5_1 @ X3564 ) )
| ( X3564 @ X3569 )
| ~ ( X3564 @ ( ap @ ( esk3_1 @ X3564 ) @ ( esk4_1 @ X3564 ) ) )
| ( var @ ( esk2_1 @ X3564 ) ) )
& ( ~ ( X3564 @ ( lam @ ( esk5_1 @ X3564 ) ) )
| ( X3564 @ X3569 )
| ~ ( X3564 @ ( ap @ ( esk3_1 @ X3564 ) @ ( esk4_1 @ X3564 ) ) )
| ( var @ ( esk2_1 @ X3564 ) ) )
& ( ( X3564 @ ( esk5_1 @ X3564 ) )
| ( X3564 @ X3569 )
| ( X3564 @ ( esk3_1 @ X3564 ) )
| ~ ( X3564 @ ( esk2_1 @ X3564 ) ) )
& ( ~ ( X3564 @ ( lam @ ( esk5_1 @ X3564 ) ) )
| ( X3564 @ X3569 )
| ( X3564 @ ( esk3_1 @ X3564 ) )
| ~ ( X3564 @ ( esk2_1 @ X3564 ) ) )
& ( ( X3564 @ ( esk5_1 @ X3564 ) )
| ( X3564 @ X3569 )
| ( X3564 @ ( esk4_1 @ X3564 ) )
| ~ ( X3564 @ ( esk2_1 @ X3564 ) ) )
& ( ~ ( X3564 @ ( lam @ ( esk5_1 @ X3564 ) ) )
| ( X3564 @ X3569 )
| ( X3564 @ ( esk4_1 @ X3564 ) )
| ~ ( X3564 @ ( esk2_1 @ X3564 ) ) )
& ( ( X3564 @ ( esk5_1 @ X3564 ) )
| ( X3564 @ X3569 )
| ~ ( X3564 @ ( ap @ ( esk3_1 @ X3564 ) @ ( esk4_1 @ X3564 ) ) )
| ~ ( X3564 @ ( esk2_1 @ X3564 ) ) )
& ( ~ ( X3564 @ ( lam @ ( esk5_1 @ X3564 ) ) )
| ( X3564 @ X3569 )
| ~ ( X3564 @ ( ap @ ( esk3_1 @ X3564 ) @ ( esk4_1 @ X3564 ) ) )
| ~ ( X3564 @ ( esk2_1 @ X3564 ) ) )
& ( ( var @ ( esk6_3 @ X3570 @ X3571 @ X3572 ) )
| ~ ( X3570 @ X3571 )
| ~ ( var @ X3574 )
| ( X3570 @ ( sub @ X3574 @ ( push @ X3571 @ X3572 ) ) ) )
& ( ~ ( X3570 @ ( sub @ ( esk6_3 @ X3570 @ X3571 @ X3572 ) @ X3572 ) )
| ~ ( X3570 @ X3571 )
| ~ ( var @ X3574 )
| ( X3570 @ ( sub @ X3574 @ ( push @ X3571 @ X3572 ) ) ) )
& ( ( var @ ( esk10_3 @ X3575 @ X3580 @ X3581 ) )
| ( X3575 @ ( sub @ X3580 @ X3581 ) )
| ~ ( X3575 @ X3579 )
| ( X3575 @ ( sub @ ( esk9_1 @ X3575 ) @ ( push @ X3579 @ id ) ) )
| ( X3575 @ ( esk7_1 @ X3575 ) ) )
& ( ~ ( X3575 @ ( sub @ ( esk10_3 @ X3575 @ X3580 @ X3581 ) @ X3581 ) )
| ( X3575 @ ( sub @ X3580 @ X3581 ) )
| ~ ( X3575 @ X3579 )
| ( X3575 @ ( sub @ ( esk9_1 @ X3575 ) @ ( push @ X3579 @ id ) ) )
| ( X3575 @ ( esk7_1 @ X3575 ) ) )
& ( ( var @ ( esk10_3 @ X3575 @ X3580 @ X3581 ) )
| ( X3575 @ ( sub @ X3580 @ X3581 ) )
| ~ ( X3575 @ ( lam @ ( esk9_1 @ X3575 ) ) )
| ( X3575 @ ( esk7_1 @ X3575 ) ) )
& ( ~ ( X3575 @ ( sub @ ( esk10_3 @ X3575 @ X3580 @ X3581 ) @ X3581 ) )
| ( X3575 @ ( sub @ X3580 @ X3581 ) )
| ~ ( X3575 @ ( lam @ ( esk9_1 @ X3575 ) ) )
| ( X3575 @ ( esk7_1 @ X3575 ) ) )
& ( ( var @ ( esk10_3 @ X3575 @ X3580 @ X3581 ) )
| ( X3575 @ ( sub @ X3580 @ X3581 ) )
| ~ ( X3575 @ X3579 )
| ( X3575 @ ( sub @ ( esk9_1 @ X3575 ) @ ( push @ X3579 @ id ) ) )
| ( X3575 @ ( esk8_1 @ X3575 ) ) )
& ( ~ ( X3575 @ ( sub @ ( esk10_3 @ X3575 @ X3580 @ X3581 ) @ X3581 ) )
| ( X3575 @ ( sub @ X3580 @ X3581 ) )
| ~ ( X3575 @ X3579 )
| ( X3575 @ ( sub @ ( esk9_1 @ X3575 ) @ ( push @ X3579 @ id ) ) )
| ( X3575 @ ( esk8_1 @ X3575 ) ) )
& ( ( var @ ( esk10_3 @ X3575 @ X3580 @ X3581 ) )
| ( X3575 @ ( sub @ X3580 @ X3581 ) )
| ~ ( X3575 @ ( lam @ ( esk9_1 @ X3575 ) ) )
| ( X3575 @ ( esk8_1 @ X3575 ) ) )
& ( ~ ( X3575 @ ( sub @ ( esk10_3 @ X3575 @ X3580 @ X3581 ) @ X3581 ) )
| ( X3575 @ ( sub @ X3580 @ X3581 ) )
| ~ ( X3575 @ ( lam @ ( esk9_1 @ X3575 ) ) )
| ( X3575 @ ( esk8_1 @ X3575 ) ) )
& ( ( var @ ( esk10_3 @ X3575 @ X3580 @ X3581 ) )
| ( X3575 @ ( sub @ X3580 @ X3581 ) )
| ~ ( X3575 @ X3579 )
| ( X3575 @ ( sub @ ( esk9_1 @ X3575 ) @ ( push @ X3579 @ id ) ) )
| ~ ( X3575 @ ( ap @ ( esk7_1 @ X3575 ) @ ( esk8_1 @ X3575 ) ) ) )
& ( ~ ( X3575 @ ( sub @ ( esk10_3 @ X3575 @ X3580 @ X3581 ) @ X3581 ) )
| ( X3575 @ ( sub @ X3580 @ X3581 ) )
| ~ ( X3575 @ X3579 )
| ( X3575 @ ( sub @ ( esk9_1 @ X3575 ) @ ( push @ X3579 @ id ) ) )
| ~ ( X3575 @ ( ap @ ( esk7_1 @ X3575 ) @ ( esk8_1 @ X3575 ) ) ) )
& ( ( var @ ( esk10_3 @ X3575 @ X3580 @ X3581 ) )
| ( X3575 @ ( sub @ X3580 @ X3581 ) )
| ~ ( X3575 @ ( lam @ ( esk9_1 @ X3575 ) ) )
| ~ ( X3575 @ ( ap @ ( esk7_1 @ X3575 ) @ ( esk8_1 @ X3575 ) ) ) )
& ( ~ ( X3575 @ ( sub @ ( esk10_3 @ X3575 @ X3580 @ X3581 ) @ X3581 ) )
| ( X3575 @ ( sub @ X3580 @ X3581 ) )
| ~ ( X3575 @ ( lam @ ( esk9_1 @ X3575 ) ) )
| ~ ( X3575 @ ( ap @ ( esk7_1 @ X3575 ) @ ( esk8_1 @ X3575 ) ) ) )
& ( ~ ( X3583 @ X3588 )
| ( X3583 @ ( sub @ ( esk14_1 @ X3583 ) @ ( push @ X3588 @ id ) ) )
| ( X3583 @ X3589 )
| ( X3583 @ ( esk12_1 @ X3583 ) )
| ( var @ ( esk11_1 @ X3583 ) ) )
& ( ~ ( X3583 @ ( lam @ ( esk14_1 @ X3583 ) ) )
| ( X3583 @ X3589 )
| ( X3583 @ ( esk12_1 @ X3583 ) )
| ( var @ ( esk11_1 @ X3583 ) ) )
& ( ~ ( X3583 @ X3588 )
| ( X3583 @ ( sub @ ( esk14_1 @ X3583 ) @ ( push @ X3588 @ id ) ) )
| ( X3583 @ X3589 )
| ( X3583 @ ( esk13_1 @ X3583 ) )
| ( var @ ( esk11_1 @ X3583 ) ) )
& ( ~ ( X3583 @ ( lam @ ( esk14_1 @ X3583 ) ) )
| ( X3583 @ X3589 )
| ( X3583 @ ( esk13_1 @ X3583 ) )
| ( var @ ( esk11_1 @ X3583 ) ) )
& ( ~ ( X3583 @ X3588 )
| ( X3583 @ ( sub @ ( esk14_1 @ X3583 ) @ ( push @ X3588 @ id ) ) )
| ( X3583 @ X3589 )
| ~ ( X3583 @ ( ap @ ( esk12_1 @ X3583 ) @ ( esk13_1 @ X3583 ) ) )
| ( var @ ( esk11_1 @ X3583 ) ) )
& ( ~ ( X3583 @ ( lam @ ( esk14_1 @ X3583 ) ) )
| ( X3583 @ X3589 )
| ~ ( X3583 @ ( ap @ ( esk12_1 @ X3583 ) @ ( esk13_1 @ X3583 ) ) )
| ( var @ ( esk11_1 @ X3583 ) ) )
& ( ~ ( X3583 @ X3588 )
| ( X3583 @ ( sub @ ( esk14_1 @ X3583 ) @ ( push @ X3588 @ id ) ) )
| ( X3583 @ X3589 )
| ( X3583 @ ( esk12_1 @ X3583 ) )
| ~ ( X3583 @ ( esk11_1 @ X3583 ) ) )
& ( ~ ( X3583 @ ( lam @ ( esk14_1 @ X3583 ) ) )
| ( X3583 @ X3589 )
| ( X3583 @ ( esk12_1 @ X3583 ) )
| ~ ( X3583 @ ( esk11_1 @ X3583 ) ) )
& ( ~ ( X3583 @ X3588 )
| ( X3583 @ ( sub @ ( esk14_1 @ X3583 ) @ ( push @ X3588 @ id ) ) )
| ( X3583 @ X3589 )
| ( X3583 @ ( esk13_1 @ X3583 ) )
| ~ ( X3583 @ ( esk11_1 @ X3583 ) ) )
& ( ~ ( X3583 @ ( lam @ ( esk14_1 @ X3583 ) ) )
| ( X3583 @ X3589 )
| ( X3583 @ ( esk13_1 @ X3583 ) )
| ~ ( X3583 @ ( esk11_1 @ X3583 ) ) )
& ( ~ ( X3583 @ X3588 )
| ( X3583 @ ( sub @ ( esk14_1 @ X3583 ) @ ( push @ X3588 @ id ) ) )
| ( X3583 @ X3589 )
| ~ ( X3583 @ ( ap @ ( esk12_1 @ X3583 ) @ ( esk13_1 @ X3583 ) ) )
| ~ ( X3583 @ ( esk11_1 @ X3583 ) ) )
& ( ~ ( X3583 @ ( lam @ ( esk14_1 @ X3583 ) ) )
| ( X3583 @ X3589 )
| ~ ( X3583 @ ( ap @ ( esk12_1 @ X3583 ) @ ( esk13_1 @ X3583 ) ) )
| ~ ( X3583 @ ( esk11_1 @ X3583 ) ) )
& ( ( comp @ ( comp @ X3590 @ X3591 ) @ X3592 )
= ( comp @ X3590 @ ( comp @ X3591 @ X3592 ) ) )
& ( ( comp @ id @ X3593 )
= X3593 )
& ( ( comp @ X3594 @ id )
= X3594 )
& ( ( sub @ ( sub @ X3595 @ X3596 ) @ X3597 )
= ( sub @ X3595 @ ( comp @ X3596 @ X3597 ) ) )
& ( ( sub @ X3598 @ id )
= X3598 )
& ( ( ( hoasap @ id @ X3599 @ id @ X3601 )
!= ( hoasap @ id @ X3600 @ id @ X3602 ) )
| ( X3599 = X3600 ) )
& ( ( ( hoasap @ id @ X3603 @ id @ X3605 )
!= ( hoasap @ id @ X3604 @ id @ X3606 ) )
| ( X3605 = X3606 ) )
& ( ( ( sub @ ( X3607 @ ( esk15_1 @ X3607 ) @ ( esk16_1 @ X3607 ) ) @ ( esk17_1 @ X3607 ) )
!= ( X3607 @ ( comp @ ( esk15_1 @ X3607 ) @ ( esk17_1 @ X3607 ) ) @ ( sub @ ( esk16_1 @ X3607 ) @ ( esk17_1 @ X3607 ) ) ) )
| ( ( sub @ ( X3611 @ ( esk18_2 @ X3607 @ X3611 ) @ ( esk19_2 @ X3607 @ X3611 ) ) @ ( esk20_2 @ X3607 @ X3611 ) )
!= ( X3611 @ ( comp @ ( esk18_2 @ X3607 @ X3611 ) @ ( esk20_2 @ X3607 @ X3611 ) ) @ ( sub @ ( esk19_2 @ X3607 @ X3611 ) @ ( esk20_2 @ X3607 @ X3611 ) ) ) )
| ( ( hoaslam @ id @ X3607 )
!= ( hoaslam @ id @ X3611 ) )
| ( ( X3607 @ X3615 @ X3616 )
= ( X3611 @ X3615 @ X3616 ) ) )
& ( ( ( sub @ ( X3617 @ ( esk21_1 @ X3617 ) @ ( esk22_1 @ X3617 ) ) @ ( esk23_1 @ X3617 ) )
!= ( X3617 @ ( comp @ ( esk21_1 @ X3617 ) @ ( esk23_1 @ X3617 ) ) @ ( sub @ ( esk22_1 @ X3617 ) @ ( esk23_1 @ X3617 ) ) ) )
| ( ( hoaslam @ id @ X3617 )
!= ( hoasap @ id @ X3621 @ id @ X3622 ) ) )
& ( ( ( sub @ ( X3623 @ ( esk24_1 @ X3623 ) @ ( esk25_1 @ X3623 ) ) @ ( esk26_1 @ X3623 ) )
!= ( X3623 @ ( comp @ ( esk24_1 @ X3623 ) @ ( esk26_1 @ X3623 ) ) @ ( sub @ ( esk25_1 @ X3623 ) @ ( esk26_1 @ X3623 ) ) ) )
| ~ ( var @ ( sub @ ( hoaslam @ id @ X3623 ) @ id ) ) )
& ~ ( var @ ( sub @ ( hoasap @ id @ X3627 @ id @ X3628 ) @ id ) )
& ( ( var @ ( sub @ ( esk35_1 @ X3629 ) @ id ) )
| ~ ( var @ X3639 )
| ( X3629 @ id @ X3639 @ id )
| ( X3629 @ ( comp @ ( esk31_1 @ X3629 ) @ ( esk34_1 @ X3629 ) ) @ ( sub @ ( esk32_1 @ X3629 ) @ ( esk34_1 @ X3629 ) ) @ ( esk33_1 @ X3629 ) )
| ( X3629 @ ( esk27_1 @ X3629 ) @ ( esk28_1 @ X3629 ) @ ( comp @ ( esk30_1 @ X3629 ) @ ( esk29_1 @ X3629 ) ) ) )
& ( ~ ( X3629 @ id @ ( esk35_1 @ X3629 ) @ id )
| ~ ( var @ X3639 )
| ( X3629 @ id @ X3639 @ id )
| ( X3629 @ ( comp @ ( esk31_1 @ X3629 ) @ ( esk34_1 @ X3629 ) ) @ ( sub @ ( esk32_1 @ X3629 ) @ ( esk34_1 @ X3629 ) ) @ ( esk33_1 @ X3629 ) )
| ( X3629 @ ( esk27_1 @ X3629 ) @ ( esk28_1 @ X3629 ) @ ( comp @ ( esk30_1 @ X3629 ) @ ( esk29_1 @ X3629 ) ) ) )
& ( ( var @ ( sub @ ( esk35_1 @ X3629 ) @ id ) )
| ~ ( var @ X3639 )
| ( X3629 @ id @ X3639 @ id )
| ~ ( X3629 @ ( esk31_1 @ X3629 ) @ ( esk32_1 @ X3629 ) @ ( comp @ ( esk34_1 @ X3629 ) @ ( esk33_1 @ X3629 ) ) )
| ( X3629 @ ( esk27_1 @ X3629 ) @ ( esk28_1 @ X3629 ) @ ( comp @ ( esk30_1 @ X3629 ) @ ( esk29_1 @ X3629 ) ) ) )
& ( ~ ( X3629 @ id @ ( esk35_1 @ X3629 ) @ id )
| ~ ( var @ X3639 )
| ( X3629 @ id @ X3639 @ id )
| ~ ( X3629 @ ( esk31_1 @ X3629 ) @ ( esk32_1 @ X3629 ) @ ( comp @ ( esk34_1 @ X3629 ) @ ( esk33_1 @ X3629 ) ) )
| ( X3629 @ ( esk27_1 @ X3629 ) @ ( esk28_1 @ X3629 ) @ ( comp @ ( esk30_1 @ X3629 ) @ ( esk29_1 @ X3629 ) ) ) )
& ( ( var @ ( sub @ ( esk35_1 @ X3629 ) @ id ) )
| ~ ( var @ X3639 )
| ( X3629 @ id @ X3639 @ id )
| ( X3629 @ ( comp @ ( esk31_1 @ X3629 ) @ ( esk34_1 @ X3629 ) ) @ ( sub @ ( esk32_1 @ X3629 ) @ ( esk34_1 @ X3629 ) ) @ ( esk33_1 @ X3629 ) )
| ~ ( X3629 @ ( comp @ ( esk27_1 @ X3629 ) @ ( esk30_1 @ X3629 ) ) @ ( sub @ ( esk28_1 @ X3629 ) @ ( esk30_1 @ X3629 ) ) @ ( esk29_1 @ X3629 ) ) )
& ( ~ ( X3629 @ id @ ( esk35_1 @ X3629 ) @ id )
| ~ ( var @ X3639 )
| ( X3629 @ id @ X3639 @ id )
| ( X3629 @ ( comp @ ( esk31_1 @ X3629 ) @ ( esk34_1 @ X3629 ) ) @ ( sub @ ( esk32_1 @ X3629 ) @ ( esk34_1 @ X3629 ) ) @ ( esk33_1 @ X3629 ) )
| ~ ( X3629 @ ( comp @ ( esk27_1 @ X3629 ) @ ( esk30_1 @ X3629 ) ) @ ( sub @ ( esk28_1 @ X3629 ) @ ( esk30_1 @ X3629 ) ) @ ( esk29_1 @ X3629 ) ) )
& ( ( var @ ( sub @ ( esk35_1 @ X3629 ) @ id ) )
| ~ ( var @ X3639 )
| ( X3629 @ id @ X3639 @ id )
| ~ ( X3629 @ ( esk31_1 @ X3629 ) @ ( esk32_1 @ X3629 ) @ ( comp @ ( esk34_1 @ X3629 ) @ ( esk33_1 @ X3629 ) ) )
| ~ ( X3629 @ ( comp @ ( esk27_1 @ X3629 ) @ ( esk30_1 @ X3629 ) ) @ ( sub @ ( esk28_1 @ X3629 ) @ ( esk30_1 @ X3629 ) ) @ ( esk29_1 @ X3629 ) ) )
& ( ~ ( X3629 @ id @ ( esk35_1 @ X3629 ) @ id )
| ~ ( var @ X3639 )
| ( X3629 @ id @ X3639 @ id )
| ~ ( X3629 @ ( esk31_1 @ X3629 ) @ ( esk32_1 @ X3629 ) @ ( comp @ ( esk34_1 @ X3629 ) @ ( esk33_1 @ X3629 ) ) )
| ~ ( X3629 @ ( comp @ ( esk27_1 @ X3629 ) @ ( esk30_1 @ X3629 ) ) @ ( sub @ ( esk28_1 @ X3629 ) @ ( esk30_1 @ X3629 ) ) @ ( esk29_1 @ X3629 ) ) )
& ( ( X3640 @ id @ ( esk44_1 @ X3640 ) @ id )
| ~ ( X3640 @ id @ X3651 @ id )
| ~ ( X3640 @ id @ X3652 @ id )
| ( X3640 @ id @ ( ap @ X3651 @ X3652 ) @ id )
| ( X3640 @ ( comp @ ( esk40_1 @ X3640 ) @ ( esk43_1 @ X3640 ) ) @ ( sub @ ( esk41_1 @ X3640 ) @ ( esk43_1 @ X3640 ) ) @ ( esk42_1 @ X3640 ) )
| ( X3640 @ ( esk36_1 @ X3640 ) @ ( esk37_1 @ X3640 ) @ ( comp @ ( esk39_1 @ X3640 ) @ ( esk38_1 @ X3640 ) ) ) )
& ( ( X3640 @ id @ ( esk45_1 @ X3640 ) @ id )
| ~ ( X3640 @ id @ X3651 @ id )
| ~ ( X3640 @ id @ X3652 @ id )
| ( X3640 @ id @ ( ap @ X3651 @ X3652 ) @ id )
| ( X3640 @ ( comp @ ( esk40_1 @ X3640 ) @ ( esk43_1 @ X3640 ) ) @ ( sub @ ( esk41_1 @ X3640 ) @ ( esk43_1 @ X3640 ) ) @ ( esk42_1 @ X3640 ) )
| ( X3640 @ ( esk36_1 @ X3640 ) @ ( esk37_1 @ X3640 ) @ ( comp @ ( esk39_1 @ X3640 ) @ ( esk38_1 @ X3640 ) ) ) )
& ( ~ ( X3640 @ id @ ( hoasap @ id @ ( esk44_1 @ X3640 ) @ id @ ( esk45_1 @ X3640 ) ) @ id )
| ~ ( X3640 @ id @ X3651 @ id )
| ~ ( X3640 @ id @ X3652 @ id )
| ( X3640 @ id @ ( ap @ X3651 @ X3652 ) @ id )
| ( X3640 @ ( comp @ ( esk40_1 @ X3640 ) @ ( esk43_1 @ X3640 ) ) @ ( sub @ ( esk41_1 @ X3640 ) @ ( esk43_1 @ X3640 ) ) @ ( esk42_1 @ X3640 ) )
| ( X3640 @ ( esk36_1 @ X3640 ) @ ( esk37_1 @ X3640 ) @ ( comp @ ( esk39_1 @ X3640 ) @ ( esk38_1 @ X3640 ) ) ) )
& ( ( X3640 @ id @ ( esk44_1 @ X3640 ) @ id )
| ~ ( X3640 @ id @ X3651 @ id )
| ~ ( X3640 @ id @ X3652 @ id )
| ( X3640 @ id @ ( ap @ X3651 @ X3652 ) @ id )
| ~ ( X3640 @ ( esk40_1 @ X3640 ) @ ( esk41_1 @ X3640 ) @ ( comp @ ( esk43_1 @ X3640 ) @ ( esk42_1 @ X3640 ) ) )
| ( X3640 @ ( esk36_1 @ X3640 ) @ ( esk37_1 @ X3640 ) @ ( comp @ ( esk39_1 @ X3640 ) @ ( esk38_1 @ X3640 ) ) ) )
& ( ( X3640 @ id @ ( esk45_1 @ X3640 ) @ id )
| ~ ( X3640 @ id @ X3651 @ id )
| ~ ( X3640 @ id @ X3652 @ id )
| ( X3640 @ id @ ( ap @ X3651 @ X3652 ) @ id )
| ~ ( X3640 @ ( esk40_1 @ X3640 ) @ ( esk41_1 @ X3640 ) @ ( comp @ ( esk43_1 @ X3640 ) @ ( esk42_1 @ X3640 ) ) )
| ( X3640 @ ( esk36_1 @ X3640 ) @ ( esk37_1 @ X3640 ) @ ( comp @ ( esk39_1 @ X3640 ) @ ( esk38_1 @ X3640 ) ) ) )
& ( ~ ( X3640 @ id @ ( hoasap @ id @ ( esk44_1 @ X3640 ) @ id @ ( esk45_1 @ X3640 ) ) @ id )
| ~ ( X3640 @ id @ X3651 @ id )
| ~ ( X3640 @ id @ X3652 @ id )
| ( X3640 @ id @ ( ap @ X3651 @ X3652 ) @ id )
| ~ ( X3640 @ ( esk40_1 @ X3640 ) @ ( esk41_1 @ X3640 ) @ ( comp @ ( esk43_1 @ X3640 ) @ ( esk42_1 @ X3640 ) ) )
| ( X3640 @ ( esk36_1 @ X3640 ) @ ( esk37_1 @ X3640 ) @ ( comp @ ( esk39_1 @ X3640 ) @ ( esk38_1 @ X3640 ) ) ) )
& ( ( X3640 @ id @ ( esk44_1 @ X3640 ) @ id )
| ~ ( X3640 @ id @ X3651 @ id )
| ~ ( X3640 @ id @ X3652 @ id )
| ( X3640 @ id @ ( ap @ X3651 @ X3652 ) @ id )
| ( X3640 @ ( comp @ ( esk40_1 @ X3640 ) @ ( esk43_1 @ X3640 ) ) @ ( sub @ ( esk41_1 @ X3640 ) @ ( esk43_1 @ X3640 ) ) @ ( esk42_1 @ X3640 ) )
| ~ ( X3640 @ ( comp @ ( esk36_1 @ X3640 ) @ ( esk39_1 @ X3640 ) ) @ ( sub @ ( esk37_1 @ X3640 ) @ ( esk39_1 @ X3640 ) ) @ ( esk38_1 @ X3640 ) ) )
& ( ( X3640 @ id @ ( esk45_1 @ X3640 ) @ id )
| ~ ( X3640 @ id @ X3651 @ id )
| ~ ( X3640 @ id @ X3652 @ id )
| ( X3640 @ id @ ( ap @ X3651 @ X3652 ) @ id )
| ( X3640 @ ( comp @ ( esk40_1 @ X3640 ) @ ( esk43_1 @ X3640 ) ) @ ( sub @ ( esk41_1 @ X3640 ) @ ( esk43_1 @ X3640 ) ) @ ( esk42_1 @ X3640 ) )
| ~ ( X3640 @ ( comp @ ( esk36_1 @ X3640 ) @ ( esk39_1 @ X3640 ) ) @ ( sub @ ( esk37_1 @ X3640 ) @ ( esk39_1 @ X3640 ) ) @ ( esk38_1 @ X3640 ) ) )
& ( ~ ( X3640 @ id @ ( hoasap @ id @ ( esk44_1 @ X3640 ) @ id @ ( esk45_1 @ X3640 ) ) @ id )
| ~ ( X3640 @ id @ X3651 @ id )
| ~ ( X3640 @ id @ X3652 @ id )
| ( X3640 @ id @ ( ap @ X3651 @ X3652 ) @ id )
| ( X3640 @ ( comp @ ( esk40_1 @ X3640 ) @ ( esk43_1 @ X3640 ) ) @ ( sub @ ( esk41_1 @ X3640 ) @ ( esk43_1 @ X3640 ) ) @ ( esk42_1 @ X3640 ) )
| ~ ( X3640 @ ( comp @ ( esk36_1 @ X3640 ) @ ( esk39_1 @ X3640 ) ) @ ( sub @ ( esk37_1 @ X3640 ) @ ( esk39_1 @ X3640 ) ) @ ( esk38_1 @ X3640 ) ) )
& ( ( X3640 @ id @ ( esk44_1 @ X3640 ) @ id )
| ~ ( X3640 @ id @ X3651 @ id )
| ~ ( X3640 @ id @ X3652 @ id )
| ( X3640 @ id @ ( ap @ X3651 @ X3652 ) @ id )
| ~ ( X3640 @ ( esk40_1 @ X3640 ) @ ( esk41_1 @ X3640 ) @ ( comp @ ( esk43_1 @ X3640 ) @ ( esk42_1 @ X3640 ) ) )
| ~ ( X3640 @ ( comp @ ( esk36_1 @ X3640 ) @ ( esk39_1 @ X3640 ) ) @ ( sub @ ( esk37_1 @ X3640 ) @ ( esk39_1 @ X3640 ) ) @ ( esk38_1 @ X3640 ) ) )
& ( ( X3640 @ id @ ( esk45_1 @ X3640 ) @ id )
| ~ ( X3640 @ id @ X3651 @ id )
| ~ ( X3640 @ id @ X3652 @ id )
| ( X3640 @ id @ ( ap @ X3651 @ X3652 ) @ id )
| ~ ( X3640 @ ( esk40_1 @ X3640 ) @ ( esk41_1 @ X3640 ) @ ( comp @ ( esk43_1 @ X3640 ) @ ( esk42_1 @ X3640 ) ) )
| ~ ( X3640 @ ( comp @ ( esk36_1 @ X3640 ) @ ( esk39_1 @ X3640 ) ) @ ( sub @ ( esk37_1 @ X3640 ) @ ( esk39_1 @ X3640 ) ) @ ( esk38_1 @ X3640 ) ) )
& ( ~ ( X3640 @ id @ ( hoasap @ id @ ( esk44_1 @ X3640 ) @ id @ ( esk45_1 @ X3640 ) ) @ id )
| ~ ( X3640 @ id @ X3651 @ id )
| ~ ( X3640 @ id @ X3652 @ id )
| ( X3640 @ id @ ( ap @ X3651 @ X3652 ) @ id )
| ~ ( X3640 @ ( esk40_1 @ X3640 ) @ ( esk41_1 @ X3640 ) @ ( comp @ ( esk43_1 @ X3640 ) @ ( esk42_1 @ X3640 ) ) )
| ~ ( X3640 @ ( comp @ ( esk36_1 @ X3640 ) @ ( esk39_1 @ X3640 ) ) @ ( sub @ ( esk37_1 @ X3640 ) @ ( esk39_1 @ X3640 ) ) @ ( esk38_1 @ X3640 ) ) )
& ( ( sub @ esk46_0 @ ( push @ one @ sh ) )
!= ( X3654 @ sh @ one ) ) ),
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_49])])])])])])]) ).
thf(c_0_51,negated_conjecture,
! [X12: subst > term > term] :
( ( sub @ esk46_0 @ ( push @ one @ sh ) )
!= ( X12 @ sh @ one ) ),
inference(split_conjunct,[status(thm)],[c_0_50]) ).
thf(c_0_52,negated_conjecture,
( ( push @ one @ sh )
= id ),
inference(split_conjunct,[status(thm)],[c_0_50]) ).
thf(c_0_53,negated_conjecture,
! [X12: subst > term > term] :
( ( sub @ esk46_0 @ id )
!= ( X12 @ sh @ one ) ),
inference(rw,[status(thm)],[c_0_51,c_0_52]) ).
thf(c_0_54,negated_conjecture,
! [X1: term] :
( ( sub @ X1 @ id )
= X1 ),
inference(split_conjunct,[status(thm)],[c_0_50]) ).
thf(c_0_55,negated_conjecture,
! [X12: subst > term > term] :
( esk46_0
!= ( X12 @ sh @ one ) ),
inference(rw,[status(thm)],[c_0_53,c_0_54]) ).
thf(c_0_56,negated_conjecture,
$false,
inference(er,[status(thm)],[c_0_55]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG267^1 : TPTP v9.3.1. Bugfixed v5.2.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 % Computer : n005.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Tue Sep 29 17:34:46 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.25 Running higher-order theorem proving
% 0.22/0.28 Running: /export/starexec/sandbox2/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/sandbox2/tmp/tmp.aPh9SsP4t2/E---3.1_1973414.p
% 0.62/0.39 % Version: 3.5.1-ho
% 0.62/0.39 % Preprocessing class: HSMMSLSSLLLNHFA.
% 0.62/0.39 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.62/0.39 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 0.62/0.39 % Starting post_as_ho1 with 300s (1) cores
% 0.62/0.39 % Starting post_as_ho5 with 300s (1) cores
% 0.62/0.39 % Starting post_as_ho10 with 300s (1) cores
% 0.62/0.39 % new_ho_10_cnf2 with pid 1973427 completed with status 0
% 0.62/0.39 % Result found by new_ho_10_cnf2
% 0.62/0.39 % Preprocessing class: HSMMSLSSLLLNHFA.
% 0.62/0.39 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.62/0.39 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 0.62/0.39 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.62/0.39 % No SInE strategy applied
% 0.62/0.39 % Search class: HGHSM-FFLF31-MHFMMMBN
% 0.62/0.39 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.62/0.39 % Starting SubtermCWHack with 136s (1) cores
% 0.62/0.39 % Starting new_ho_10_cnf2 with 151s (1) cores
% 0.62/0.39 % Starting new_ho_8 with 226s (1) cores
% 0.62/0.39 % Starting new_ho_4 with 226s (1) cores
% 0.62/0.39 % Starting post_as_ho5 with 226s (1) cores
% 0.62/0.39 % new_ho_8 with pid 1973435 completed with status 0
% 0.62/0.39 % Result found by new_ho_8
% 0.62/0.39 % Preprocessing class: HSMMSLSSLLLNHFA.
% 0.62/0.39 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.62/0.39 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 0.62/0.39 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.62/0.39 % No SInE strategy applied
% 0.62/0.39 % Search class: HGHSM-FFLF31-MHFMMMBN
% 0.62/0.39 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.62/0.39 % Starting SubtermCWHack with 136s (1) cores
% 0.62/0.39 % Starting new_ho_10_cnf2 with 151s (1) cores
% 0.62/0.39 % Starting new_ho_8 with 226s (1) cores
% 0.62/0.39 % Preprocessing time : 0.004 s
% 0.62/0.39 % Presaturation interreduction done
% 0.62/0.39
% 0.62/0.39 % Proof found!
% 0.62/0.39 % SZS status Theorem
% 0.62/0.39 % SZS output start CNFRefutation
% See solution above
% 0.62/0.39 % Parsed axioms : 238
% 0.62/0.39 % Removed by relevancy pruning/SinE : 0
% 0.62/0.39 % Initial clauses : 220
% 0.62/0.39 % Removed in clause preprocessing : 124
% 0.62/0.39 % Initial clauses in saturation : 96
% 0.62/0.39 % Processed clauses : 104
% 0.62/0.39 % ...of these trivial : 5
% 0.62/0.39 % ...subsumed : 3
% 0.62/0.39 % ...remaining for further processing : 96
% 0.62/0.39 % Other redundant clauses eliminated : 0
% 0.62/0.39 % Clauses deleted for lack of memory : 0
% 0.62/0.39 % Backward-subsumed : 0
% 0.62/0.39 % Backward-rewritten : 5
% 0.62/0.39 % Generated clauses : 1
% 0.62/0.39 % ...of the previous two non-redundant : 4
% 0.62/0.39 % ...aggressively subsumed : 0
% 0.62/0.39 % Contextual simplify-reflections : 0
% 0.62/0.39 % Paramodulations : 0
% 0.62/0.39 % Factorizations : 0
% 0.62/0.39 % NegExts : 0
% 0.62/0.39 % Equation resolutions : 1
% 0.62/0.39 % Disequality decompositions : 0
% 0.62/0.39 % Total rewrite steps : 36
% 0.62/0.39 % ...of those cached : 15
% 0.62/0.39 % Propositional unsat checks : 0
% 0.62/0.39 % Propositional check models : 0
% 0.62/0.39 % Propositional check unsatisfiable : 0
% 0.62/0.39 % Propositional clauses : 0
% 0.62/0.39 % Propositional clauses after purity: 0
% 0.62/0.39 % Propositional unsat core size : 0
% 0.62/0.39 % Propositional preprocessing time : 0.000
% 0.62/0.39 % Propositional encoding time : 0.000
% 0.62/0.39 % Propositional solver time : 0.000
% 0.62/0.39 % Success case prop preproc time : 0.000
% 0.62/0.39 % Success case prop encoding time : 0.000
% 0.62/0.39 % Success case prop solver time : 0.000
% 0.62/0.39 % Current number of processed clauses : 4
% 0.62/0.39 % Positive orientable unit clauses : 2
% 0.62/0.39 % Positive unorientable unit clauses: 0
% 0.62/0.39 % Negative unit clauses : 2
% 0.62/0.39 % Non-unit-clauses : 0
% 0.62/0.39 % Current number of unprocessed clauses: 83
% 0.62/0.39 % ...number of literals in the above : 320
% 0.62/0.39 % Current number of archived formulas : 0
% 0.62/0.39 % Current number of archived clauses : 92
% 0.62/0.39 % Clause-clause subsumption calls (NU) : 575
% 0.62/0.39 % Rec. Clause-clause subsumption calls : 82
% 0.62/0.39 % Non-unit clause-clause subsumptions : 2
% 0.62/0.39 % Unit Clause-clause subsumption calls : 13
% 0.62/0.39 % Rewrite failures with RHS unbound : 0
% 0.62/0.39 % BW rewrite match attempts : 10
% 0.62/0.39 % BW rewrite match successes : 8
% 0.62/0.39 % Condensation attempts : 0
% 0.62/0.39 % Condensation successes : 0
% 0.62/0.39 % Termbank termtop insertions : 49650
% 0.62/0.39 % Search garbage collected termcells : 4930
% 0.62/0.39
% 0.62/0.39 % -------------------------------------------------
% 0.62/0.39 % User time : 0.045 s
% 0.62/0.39 % System time : 0.016 s
% 0.62/0.39 % Total time : 0.061 s
% 0.62/0.39 % Maximum resident set size: 8076 pages
% 0.62/0.39
% 0.62/0.39 % -------------------------------------------------
% 0.62/0.39 % User time : 0.116 s
% 0.62/0.39 % System time : 0.035 s
% 0.62/0.39 % Total time : 0.151 s
% 0.62/0.39 % Maximum resident set size: 5120 pages
% 0.62/0.39 % E exiting
%------------------------------------------------------------------------------