%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ALG255^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 : n009.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:45 AM UTC 2026
% Result : Theorem 0.36s 0.45s
% Output : CNFRefutation 0.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 30
% Syntax : Number of formulae : 38 ( 6 unt; 0 typ; 0 def)
% Number of atoms : 236 ( 109 equ; 0 cnn)
% Maximal formula atoms : 56 ( 6 avg)
% Number of connectives : 1685 ( 95 ~; 142 |; 74 &;1153 @)
% ( 29 <=>; 192 =>; 0 <=; 0 <~>)
% Maximal formula depth : 127 ( 10 avg)
% Number of types : 3 ( 2 usr)
% Number of type conns : 20 ( 20 >; 0 *; 0 +; 0 <<)
% Number of symbols : 58 ( 56 usr; 37 con; 0-3 aty)
% Number of variables : 302 ( 0 ^; 302 !; 0 ?; 302 :)
% 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_40,type,
induction2lem: $o ).
thf(decl_42,type,
axvarshift: $o ).
thf(decl_46,type,
ulamvar1: $o ).
thf(decl_49,type,
apnotvar: $o ).
thf(decl_68,type,
axapp: $o ).
thf(decl_72,type,
ulamvarind: $o ).
thf(decl_73,type,
induction: $o ).
thf(decl_75,type,
termmset_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_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_112,type,
axidl: $o ).
thf(decl_117,type,
pushprop: $o ).
thf(decl_121,type,
substmonoid: $o ).
thf(decl_122,type,
lamnotvar: $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_0: term ).
thf(decl_160,type,
esk16_0: subst ).
thf(decl_161,type,
esk17_0: subst ).
thf(decl_162,type,
esk18_0: term ).
thf(thm,conjecture,
termmset_gthm,
file('/export/starexec/sandbox/tmp/tmp.KHBqYtGr8Q/E---3.1_115084.p',thm) ).
thf(termmset_gthm,axiom,
( termmset_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 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.KHBqYtGr8Q/E---3.1_115084.p',termmset_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.KHBqYtGr8Q/E---3.1_115084.p',axapp) ).
thf(axvarcons,axiom,
( axvarcons
<=> ! [X1: term,X3: subst] :
( ( sub @ one @ ( push @ X1 @ X3 ) )
= X1 ) ),
file('/export/starexec/sandbox/tmp/tmp.KHBqYtGr8Q/E---3.1_115084.p',axvarcons) ).
thf(axvarid,axiom,
( axvarid
<=> ! [X1: term] :
( ( sub @ X1 @ id )
= X1 ) ),
file('/export/starexec/sandbox/tmp/tmp.KHBqYtGr8Q/E---3.1_115084.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.KHBqYtGr8Q/E---3.1_115084.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.KHBqYtGr8Q/E---3.1_115084.p',axclos) ).
thf(axidl,axiom,
( axidl
<=> ! [X3: subst] :
( ( comp @ id @ X3 )
= X3 ) ),
file('/export/starexec/sandbox/tmp/tmp.KHBqYtGr8Q/E---3.1_115084.p',axidl) ).
thf(axshiftcons,axiom,
( axshiftcons
<=> ! [X1: term,X3: subst] :
( ( comp @ sh @ ( push @ X1 @ X3 ) )
= X3 ) ),
file('/export/starexec/sandbox/tmp/tmp.KHBqYtGr8Q/E---3.1_115084.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.KHBqYtGr8Q/E---3.1_115084.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.KHBqYtGr8Q/E---3.1_115084.p',axmap) ).
thf(axidr,axiom,
( axidr
<=> ! [X3: subst] :
( ( comp @ X3 @ id )
= X3 ) ),
file('/export/starexec/sandbox/tmp/tmp.KHBqYtGr8Q/E---3.1_115084.p',axidr) ).
thf(axvarshift,axiom,
( axvarshift
<=> ( ( push @ one @ sh )
= id ) ),
file('/export/starexec/sandbox/tmp/tmp.KHBqYtGr8Q/E---3.1_115084.p',axvarshift) ).
thf(axscons,axiom,
( axscons
<=> ! [X3: subst] :
( ( push @ ( sub @ one @ X3 ) @ ( comp @ sh @ X3 ) )
= X3 ) ),
file('/export/starexec/sandbox/tmp/tmp.KHBqYtGr8Q/E---3.1_115084.p',axscons) ).
thf(ulamvar1,axiom,
( ulamvar1
<=> ( var @ one ) ),
file('/export/starexec/sandbox/tmp/tmp.KHBqYtGr8Q/E---3.1_115084.p',ulamvar1) ).
thf(ulamvarsh,axiom,
( ulamvarsh
<=> ! [X1: term] :
( ( var @ X1 )
=> ( var @ ( sub @ X1 @ sh ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.KHBqYtGr8Q/E---3.1_115084.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.KHBqYtGr8Q/E---3.1_115084.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.KHBqYtGr8Q/E---3.1_115084.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.KHBqYtGr8Q/E---3.1_115084.p',apinj2) ).
thf(laminj,axiom,
( laminj
<=> ! [X1: term,X2: term] :
( ( ( lam @ X1 )
= ( lam @ X2 ) )
=> ( X1 = X2 ) ) ),
file('/export/starexec/sandbox/tmp/tmp.KHBqYtGr8Q/E---3.1_115084.p',laminj) ).
thf(shinj,axiom,
( shinj
<=> ! [X1: term,X2: term] :
( ( ( sub @ X1 @ sh )
= ( sub @ X2 @ sh ) )
=> ( X1 = X2 ) ) ),
file('/export/starexec/sandbox/tmp/tmp.KHBqYtGr8Q/E---3.1_115084.p',shinj) ).
thf(lamnotap,axiom,
( lamnotap
<=> ! [X1: term,X2: term,X7: term] :
( ( lam @ X1 )
!= ( ap @ X2 @ X7 ) ) ),
file('/export/starexec/sandbox/tmp/tmp.KHBqYtGr8Q/E---3.1_115084.p',lamnotap) ).
thf(apnotvar,axiom,
( apnotvar
<=> ! [X1: term,X2: term] :
~ ( var @ ( ap @ X1 @ X2 ) ) ),
file('/export/starexec/sandbox/tmp/tmp.KHBqYtGr8Q/E---3.1_115084.p',apnotvar) ).
thf(lamnotvar,axiom,
( lamnotvar
<=> ! [X1: term] :
~ ( var @ ( lam @ X1 ) ) ),
file('/export/starexec/sandbox/tmp/tmp.KHBqYtGr8Q/E---3.1_115084.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.KHBqYtGr8Q/E---3.1_115084.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.KHBqYtGr8Q/E---3.1_115084.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.KHBqYtGr8Q/E---3.1_115084.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.KHBqYtGr8Q/E---3.1_115084.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.KHBqYtGr8Q/E---3.1_115084.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.KHBqYtGr8Q/E---3.1_115084.p',termmset) ).
thf(c_0_30,negated_conjecture,
~ termmset_gthm,
inference(assume_negation,[status(cth)],[thm]) ).
thf(c_0_31,axiom,
( termmset_gthm
= ( ! [X107: term,X108: term,X109: subst] :
( ( sub @ ( ap @ X107 @ X108 ) @ X109 )
= ( ap @ ( sub @ X107 @ X109 ) @ ( sub @ X108 @ X109 ) ) )
=> ( ! [X110: term,X111: subst] :
( ( sub @ one @ ( push @ X110 @ X111 ) )
= X110 )
=> ( ! [X112: term] :
( ( sub @ X112 @ id )
= X112 )
=> ( ! [X113: term,X114: subst] :
( ( sub @ ( lam @ X113 ) @ X114 )
= ( lam @ ( sub @ X113 @ ( push @ one @ ( comp @ X114 @ sh ) ) ) ) )
=> ( ! [X115: term,X116: subst,X117: subst] :
( ( sub @ ( sub @ X115 @ X116 ) @ X117 )
= ( sub @ X115 @ ( comp @ X116 @ X117 ) ) )
=> ( ! [X118: subst] :
( ( comp @ id @ X118 )
= X118 )
=> ( ! [X119: term,X120: subst] :
( ( comp @ sh @ ( push @ X119 @ X120 ) )
= X120 )
=> ( ! [X121: subst,X122: subst,X123: subst] :
( ( comp @ ( comp @ X121 @ X122 ) @ X123 )
= ( comp @ X121 @ ( comp @ X122 @ X123 ) ) )
=> ( ! [X124: term,X125: subst,X126: subst] :
( ( comp @ ( push @ X124 @ X125 ) @ X126 )
= ( push @ ( sub @ X124 @ X126 ) @ ( comp @ X125 @ X126 ) ) )
=> ( ! [X127: subst] :
( ( comp @ X127 @ id )
= X127 )
=> ( ( ( push @ one @ sh )
= id )
=> ( ! [X128: subst] :
( ( push @ ( sub @ one @ X128 ) @ ( comp @ sh @ X128 ) )
= X128 )
=> ( ( var @ one )
=> ( ! [X129: term] :
( ( var @ X129 )
=> ( var @ ( sub @ X129 @ sh ) ) )
=> ( ! [X130: term > $o] :
( ( X130 @ one )
=> ( ! [X131: term] :
( ( var @ X131 )
=> ( ( X130 @ X131 )
=> ( X130 @ ( sub @ X131 @ sh ) ) ) )
=> ! [X132: term] :
( ( var @ X132 )
=> ( X130 @ X132 ) ) ) )
=> ( ! [X133: term,X134: term,X135: term,X136: term] :
( ( ( ap @ X133 @ X135 )
= ( ap @ X134 @ X136 ) )
=> ( X133 = X134 ) )
=> ( ! [X137: term,X138: term,X139: term,X140: term] :
( ( ( ap @ X137 @ X139 )
= ( ap @ X138 @ X140 ) )
=> ( X139 = X140 ) )
=> ( ! [X141: term,X142: term] :
( ( ( lam @ X141 )
= ( lam @ X142 ) )
=> ( X141 = X142 ) )
=> ( ! [X143: term,X144: term] :
( ( ( sub @ X143 @ sh )
= ( sub @ X144 @ sh ) )
=> ( X143 = X144 ) )
=> ( ! [X145: term,X146: term,X147: term] :
( ( lam @ X145 )
!= ( ap @ X146 @ X147 ) )
=> ( ! [X148: term,X149: term] :
~ ( var @ ( ap @ X148 @ X149 ) )
=> ( ! [X150: term] :
~ ( var @ ( lam @ X150 ) )
=> ( ! [X151: term > $o] :
( ! [X152: term] :
( ( var @ X152 )
=> ( X151 @ X152 ) )
=> ( ! [X153: term,X154: term] :
( ( X151 @ X153 )
=> ( ( X151 @ X154 )
=> ( X151 @ ( ap @ X153 @ X154 ) ) ) )
=> ( ! [X155: term] :
( ( X151 @ X155 )
=> ( X151 @ ( lam @ X155 ) ) )
=> ! [X156: term] : ( X151 @ X156 ) ) ) )
=> ( ! [X157: term > $o,X158: term,X159: subst] :
( ! [X160: term] :
( ( var @ X160 )
=> ( X157 @ ( sub @ X160 @ X159 ) ) )
=> ( ( X157 @ X158 )
=> ! [X161: term] :
( ( var @ X161 )
=> ( X157 @ ( sub @ X161 @ ( push @ X158 @ X159 ) ) ) ) ) )
=> ( ! [X162: term > $o] :
( ! [X163: term,X164: term] :
( ( X162 @ X163 )
=> ( ( X162 @ X164 )
=> ( X162 @ ( ap @ X163 @ X164 ) ) ) )
=> ( ! [X165: term] :
( ! [X166: term] :
( ( X162 @ X166 )
=> ( X162 @ ( sub @ X165 @ ( push @ X166 @ id ) ) ) )
=> ( X162 @ ( lam @ X165 ) ) )
=> ! [X167: term,X168: subst] :
( ! [X169: term] :
( ( var @ X169 )
=> ( X162 @ ( sub @ X169 @ X168 ) ) )
=> ( X162 @ ( sub @ X167 @ X168 ) ) ) ) )
=> ( ! [X170: term > $o] :
( ! [X171: term] :
( ( var @ X171 )
=> ( X170 @ X171 ) )
=> ( ! [X172: term,X173: term] :
( ( X170 @ X172 )
=> ( ( X170 @ X173 )
=> ( X170 @ ( ap @ X172 @ X173 ) ) ) )
=> ( ! [X174: term] :
( ! [X175: term] :
( ( X170 @ X175 )
=> ( X170 @ ( sub @ X174 @ ( push @ X175 @ id ) ) ) )
=> ( X170 @ ( lam @ X174 ) ) )
=> ! [X176: term] : ( X170 @ X176 ) ) ) )
=> ( ( ! [X177: subst,X178: subst,X179: subst] :
( ( comp @ ( comp @ X177 @ X178 ) @ X179 )
= ( comp @ X177 @ ( comp @ X178 @ X179 ) ) )
& ! [X180: subst] :
( ( comp @ id @ X180 )
= X180 )
& ! [X181: subst] :
( ( comp @ X181 @ id )
= X181 ) )
=> ( ! [X182: term,X183: subst,X184: subst] :
( ( sub @ ( sub @ X182 @ X183 ) @ X184 )
= ( sub @ X182 @ ( comp @ X183 @ X184 ) ) )
& ! [X185: term] :
( ( sub @ X185 @ id )
= X185 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
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)],[termmset_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]) ).
thf(c_0_32,negated_conjecture,
~ ( ! [X186: term,X187: term,X188: subst] :
( ( sub @ ( ap @ X186 @ X187 ) @ X188 )
= ( ap @ ( sub @ X186 @ X188 ) @ ( sub @ X187 @ X188 ) ) )
=> ( ! [X189: term,X190: subst] :
( ( sub @ one @ ( push @ X189 @ X190 ) )
= X189 )
=> ( ! [X191: term] :
( ( sub @ X191 @ id )
= X191 )
=> ( ! [X192: term,X193: subst] :
( ( sub @ ( lam @ X192 ) @ X193 )
= ( lam @ ( sub @ X192 @ ( push @ one @ ( comp @ X193 @ sh ) ) ) ) )
=> ( ! [X194: term,X195: subst,X196: subst] :
( ( sub @ ( sub @ X194 @ X195 ) @ X196 )
= ( sub @ X194 @ ( comp @ X195 @ X196 ) ) )
=> ( ! [X197: subst] :
( ( comp @ id @ X197 )
= X197 )
=> ( ! [X198: term,X199: subst] :
( ( comp @ sh @ ( push @ X198 @ X199 ) )
= X199 )
=> ( ! [X200: subst,X201: subst,X202: subst] :
( ( comp @ ( comp @ X200 @ X201 ) @ X202 )
= ( comp @ X200 @ ( comp @ X201 @ X202 ) ) )
=> ( ! [X203: term,X204: subst,X205: subst] :
( ( comp @ ( push @ X203 @ X204 ) @ X205 )
= ( push @ ( sub @ X203 @ X205 ) @ ( comp @ X204 @ X205 ) ) )
=> ( ! [X206: subst] :
( ( comp @ X206 @ id )
= X206 )
=> ( ( ( push @ one @ sh )
= id )
=> ( ! [X207: subst] :
( ( push @ ( sub @ one @ X207 ) @ ( comp @ sh @ X207 ) )
= X207 )
=> ( ( var @ one )
=> ( ! [X208: term] :
( ( var @ X208 )
=> ( var @ ( sub @ X208 @ sh ) ) )
=> ( ! [X209: term > $o] :
( ( X209 @ one )
=> ( ! [X210: term] :
( ( var @ X210 )
=> ( ( X209 @ X210 )
=> ( X209 @ ( sub @ X210 @ sh ) ) ) )
=> ! [X211: term] :
( ( var @ X211 )
=> ( X209 @ X211 ) ) ) )
=> ( ! [X212: term,X213: term,X214: term,X215: term] :
( ( ( ap @ X212 @ X214 )
= ( ap @ X213 @ X215 ) )
=> ( X212 = X213 ) )
=> ( ! [X216: term,X217: term,X218: term,X219: term] :
( ( ( ap @ X216 @ X218 )
= ( ap @ X217 @ X219 ) )
=> ( X218 = X219 ) )
=> ( ! [X220: term,X221: term] :
( ( ( lam @ X220 )
= ( lam @ X221 ) )
=> ( X220 = X221 ) )
=> ( ! [X222: term,X223: term] :
( ( ( sub @ X222 @ sh )
= ( sub @ X223 @ sh ) )
=> ( X222 = X223 ) )
=> ( ! [X224: term,X225: term,X226: term] :
( ( lam @ X224 )
!= ( ap @ X225 @ X226 ) )
=> ( ! [X227: term,X228: term] :
~ ( var @ ( ap @ X227 @ X228 ) )
=> ( ! [X229: term] :
~ ( var @ ( lam @ X229 ) )
=> ( ! [X230: term > $o] :
( ! [X231: term] :
( ( var @ X231 )
=> ( X230 @ X231 ) )
=> ( ! [X232: term,X233: term] :
( ( X230 @ X232 )
=> ( ( X230 @ X233 )
=> ( X230 @ ( ap @ X232 @ X233 ) ) ) )
=> ( ! [X234: term] :
( ( X230 @ X234 )
=> ( X230 @ ( lam @ X234 ) ) )
=> ! [X235: term] : ( X230 @ X235 ) ) ) )
=> ( ! [X236: term > $o,X237: term,X238: subst] :
( ! [X239: term] :
( ( var @ X239 )
=> ( X236 @ ( sub @ X239 @ X238 ) ) )
=> ( ( X236 @ X237 )
=> ! [X240: term] :
( ( var @ X240 )
=> ( X236 @ ( sub @ X240 @ ( push @ X237 @ X238 ) ) ) ) ) )
=> ( ! [X241: term > $o] :
( ! [X242: term,X243: term] :
( ( X241 @ X242 )
=> ( ( X241 @ X243 )
=> ( X241 @ ( ap @ X242 @ X243 ) ) ) )
=> ( ! [X244: term] :
( ! [X245: term] :
( ( X241 @ X245 )
=> ( X241 @ ( sub @ X244 @ ( push @ X245 @ id ) ) ) )
=> ( X241 @ ( lam @ X244 ) ) )
=> ! [X246: term,X247: subst] :
( ! [X248: term] :
( ( var @ X248 )
=> ( X241 @ ( sub @ X248 @ X247 ) ) )
=> ( X241 @ ( sub @ X246 @ X247 ) ) ) ) )
=> ( ! [X249: term > $o] :
( ! [X250: term] :
( ( var @ X250 )
=> ( X249 @ X250 ) )
=> ( ! [X251: term,X252: term] :
( ( X249 @ X251 )
=> ( ( X249 @ X252 )
=> ( X249 @ ( ap @ X251 @ X252 ) ) ) )
=> ( ! [X253: term] :
( ! [X254: term] :
( ( X249 @ X254 )
=> ( X249 @ ( sub @ X253 @ ( push @ X254 @ id ) ) ) )
=> ( X249 @ ( lam @ X253 ) ) )
=> ! [X255: term] : ( X249 @ X255 ) ) ) )
=> ( ( ! [X256: subst,X257: subst,X258: subst] :
( ( comp @ ( comp @ X256 @ X257 ) @ X258 )
= ( comp @ X256 @ ( comp @ X257 @ X258 ) ) )
& ! [X259: subst] :
( ( comp @ id @ X259 )
= X259 )
& ! [X260: subst] :
( ( comp @ X260 @ id )
= X260 ) )
=> ( ! [X261: term,X262: subst,X263: subst] :
( ( sub @ ( sub @ X261 @ X262 ) @ X263 )
= ( sub @ X261 @ ( comp @ X262 @ X263 ) ) )
& ! [X264: term] :
( ( sub @ X264 @ id )
= X264 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[c_0_30,c_0_31])]) ).
thf(c_0_33,negated_conjecture,
! [X265: term,X266: term,X267: subst,X268: term,X269: subst,X270: term,X271: term,X272: subst,X273: term,X274: subst,X275: subst,X276: subst,X277: term,X278: subst,X279: subst,X280: subst,X281: subst,X282: term,X283: subst,X284: subst,X285: subst,X286: subst,X287: term,X288: term > $o,X290: term,X291: term,X292: term,X293: term,X294: term,X295: term,X296: term,X297: term,X298: term,X299: term,X300: term,X301: term,X302: term,X303: term,X304: term,X305: term,X306: term,X307: term,X308: term,X309: term > $o,X314: term,X315: term > $o,X316: term,X317: subst,X319: term,X320: term > $o,X324: term,X325: term,X326: subst,X328: term > $o,X333: term,X334: term,X335: subst,X336: subst,X337: subst,X338: subst,X339: subst] :
( ( ( sub @ ( ap @ X265 @ X266 ) @ X267 )
= ( ap @ ( sub @ X265 @ X267 ) @ ( sub @ X266 @ X267 ) ) )
& ( ( sub @ one @ ( push @ X268 @ X269 ) )
= X268 )
& ( ( sub @ X270 @ id )
= X270 )
& ( ( sub @ ( lam @ X271 ) @ X272 )
= ( lam @ ( sub @ X271 @ ( push @ one @ ( comp @ X272 @ sh ) ) ) ) )
& ( ( sub @ ( sub @ X273 @ X274 ) @ X275 )
= ( sub @ X273 @ ( comp @ X274 @ X275 ) ) )
& ( ( comp @ id @ X276 )
= X276 )
& ( ( comp @ sh @ ( push @ X277 @ X278 ) )
= X278 )
& ( ( comp @ ( comp @ X279 @ X280 ) @ X281 )
= ( comp @ X279 @ ( comp @ X280 @ X281 ) ) )
& ( ( comp @ ( push @ X282 @ X283 ) @ X284 )
= ( push @ ( sub @ X282 @ X284 ) @ ( comp @ X283 @ X284 ) ) )
& ( ( comp @ X285 @ id )
= X285 )
& ( ( push @ one @ sh )
= id )
& ( ( push @ ( sub @ one @ X286 ) @ ( comp @ sh @ X286 ) )
= X286 )
& ( var @ one )
& ( ~ ( var @ X287 )
| ( var @ ( sub @ X287 @ sh ) ) )
& ( ( var @ ( esk1_1 @ X288 ) )
| ~ ( var @ X290 )
| ( X288 @ X290 )
| ~ ( X288 @ one ) )
& ( ( X288 @ ( esk1_1 @ X288 ) )
| ~ ( var @ X290 )
| ( X288 @ X290 )
| ~ ( X288 @ one ) )
& ( ~ ( X288 @ ( sub @ ( esk1_1 @ X288 ) @ sh ) )
| ~ ( var @ X290 )
| ( X288 @ X290 )
| ~ ( X288 @ one ) )
& ( ( ( ap @ X291 @ X293 )
!= ( ap @ X292 @ X294 ) )
| ( X291 = X292 ) )
& ( ( ( ap @ X295 @ X297 )
!= ( ap @ X296 @ X298 ) )
| ( X297 = X298 ) )
& ( ( ( lam @ X299 )
!= ( lam @ X300 ) )
| ( X299 = X300 ) )
& ( ( ( sub @ X301 @ sh )
!= ( sub @ X302 @ sh ) )
| ( X301 = X302 ) )
& ( ( lam @ X303 )
!= ( ap @ X304 @ X305 ) )
& ~ ( var @ ( ap @ X306 @ X307 ) )
& ~ ( var @ ( lam @ X308 ) )
& ( ( X309 @ ( esk5_1 @ X309 ) )
| ( X309 @ X314 )
| ( X309 @ ( esk3_1 @ X309 ) )
| ( var @ ( esk2_1 @ X309 ) ) )
& ( ~ ( X309 @ ( lam @ ( esk5_1 @ X309 ) ) )
| ( X309 @ X314 )
| ( X309 @ ( esk3_1 @ X309 ) )
| ( var @ ( esk2_1 @ X309 ) ) )
& ( ( X309 @ ( esk5_1 @ X309 ) )
| ( X309 @ X314 )
| ( X309 @ ( esk4_1 @ X309 ) )
| ( var @ ( esk2_1 @ X309 ) ) )
& ( ~ ( X309 @ ( lam @ ( esk5_1 @ X309 ) ) )
| ( X309 @ X314 )
| ( X309 @ ( esk4_1 @ X309 ) )
| ( var @ ( esk2_1 @ X309 ) ) )
& ( ( X309 @ ( esk5_1 @ X309 ) )
| ( X309 @ X314 )
| ~ ( X309 @ ( ap @ ( esk3_1 @ X309 ) @ ( esk4_1 @ X309 ) ) )
| ( var @ ( esk2_1 @ X309 ) ) )
& ( ~ ( X309 @ ( lam @ ( esk5_1 @ X309 ) ) )
| ( X309 @ X314 )
| ~ ( X309 @ ( ap @ ( esk3_1 @ X309 ) @ ( esk4_1 @ X309 ) ) )
| ( var @ ( esk2_1 @ X309 ) ) )
& ( ( X309 @ ( esk5_1 @ X309 ) )
| ( X309 @ X314 )
| ( X309 @ ( esk3_1 @ X309 ) )
| ~ ( X309 @ ( esk2_1 @ X309 ) ) )
& ( ~ ( X309 @ ( lam @ ( esk5_1 @ X309 ) ) )
| ( X309 @ X314 )
| ( X309 @ ( esk3_1 @ X309 ) )
| ~ ( X309 @ ( esk2_1 @ X309 ) ) )
& ( ( X309 @ ( esk5_1 @ X309 ) )
| ( X309 @ X314 )
| ( X309 @ ( esk4_1 @ X309 ) )
| ~ ( X309 @ ( esk2_1 @ X309 ) ) )
& ( ~ ( X309 @ ( lam @ ( esk5_1 @ X309 ) ) )
| ( X309 @ X314 )
| ( X309 @ ( esk4_1 @ X309 ) )
| ~ ( X309 @ ( esk2_1 @ X309 ) ) )
& ( ( X309 @ ( esk5_1 @ X309 ) )
| ( X309 @ X314 )
| ~ ( X309 @ ( ap @ ( esk3_1 @ X309 ) @ ( esk4_1 @ X309 ) ) )
| ~ ( X309 @ ( esk2_1 @ X309 ) ) )
& ( ~ ( X309 @ ( lam @ ( esk5_1 @ X309 ) ) )
| ( X309 @ X314 )
| ~ ( X309 @ ( ap @ ( esk3_1 @ X309 ) @ ( esk4_1 @ X309 ) ) )
| ~ ( X309 @ ( esk2_1 @ X309 ) ) )
& ( ( var @ ( esk6_3 @ X315 @ X316 @ X317 ) )
| ~ ( X315 @ X316 )
| ~ ( var @ X319 )
| ( X315 @ ( sub @ X319 @ ( push @ X316 @ X317 ) ) ) )
& ( ~ ( X315 @ ( sub @ ( esk6_3 @ X315 @ X316 @ X317 ) @ X317 ) )
| ~ ( X315 @ X316 )
| ~ ( var @ X319 )
| ( X315 @ ( sub @ X319 @ ( push @ X316 @ X317 ) ) ) )
& ( ( var @ ( esk10_3 @ X320 @ X325 @ X326 ) )
| ( X320 @ ( sub @ X325 @ X326 ) )
| ~ ( X320 @ X324 )
| ( X320 @ ( sub @ ( esk9_1 @ X320 ) @ ( push @ X324 @ id ) ) )
| ( X320 @ ( esk7_1 @ X320 ) ) )
& ( ~ ( X320 @ ( sub @ ( esk10_3 @ X320 @ X325 @ X326 ) @ X326 ) )
| ( X320 @ ( sub @ X325 @ X326 ) )
| ~ ( X320 @ X324 )
| ( X320 @ ( sub @ ( esk9_1 @ X320 ) @ ( push @ X324 @ id ) ) )
| ( X320 @ ( esk7_1 @ X320 ) ) )
& ( ( var @ ( esk10_3 @ X320 @ X325 @ X326 ) )
| ( X320 @ ( sub @ X325 @ X326 ) )
| ~ ( X320 @ ( lam @ ( esk9_1 @ X320 ) ) )
| ( X320 @ ( esk7_1 @ X320 ) ) )
& ( ~ ( X320 @ ( sub @ ( esk10_3 @ X320 @ X325 @ X326 ) @ X326 ) )
| ( X320 @ ( sub @ X325 @ X326 ) )
| ~ ( X320 @ ( lam @ ( esk9_1 @ X320 ) ) )
| ( X320 @ ( esk7_1 @ X320 ) ) )
& ( ( var @ ( esk10_3 @ X320 @ X325 @ X326 ) )
| ( X320 @ ( sub @ X325 @ X326 ) )
| ~ ( X320 @ X324 )
| ( X320 @ ( sub @ ( esk9_1 @ X320 ) @ ( push @ X324 @ id ) ) )
| ( X320 @ ( esk8_1 @ X320 ) ) )
& ( ~ ( X320 @ ( sub @ ( esk10_3 @ X320 @ X325 @ X326 ) @ X326 ) )
| ( X320 @ ( sub @ X325 @ X326 ) )
| ~ ( X320 @ X324 )
| ( X320 @ ( sub @ ( esk9_1 @ X320 ) @ ( push @ X324 @ id ) ) )
| ( X320 @ ( esk8_1 @ X320 ) ) )
& ( ( var @ ( esk10_3 @ X320 @ X325 @ X326 ) )
| ( X320 @ ( sub @ X325 @ X326 ) )
| ~ ( X320 @ ( lam @ ( esk9_1 @ X320 ) ) )
| ( X320 @ ( esk8_1 @ X320 ) ) )
& ( ~ ( X320 @ ( sub @ ( esk10_3 @ X320 @ X325 @ X326 ) @ X326 ) )
| ( X320 @ ( sub @ X325 @ X326 ) )
| ~ ( X320 @ ( lam @ ( esk9_1 @ X320 ) ) )
| ( X320 @ ( esk8_1 @ X320 ) ) )
& ( ( var @ ( esk10_3 @ X320 @ X325 @ X326 ) )
| ( X320 @ ( sub @ X325 @ X326 ) )
| ~ ( X320 @ X324 )
| ( X320 @ ( sub @ ( esk9_1 @ X320 ) @ ( push @ X324 @ id ) ) )
| ~ ( X320 @ ( ap @ ( esk7_1 @ X320 ) @ ( esk8_1 @ X320 ) ) ) )
& ( ~ ( X320 @ ( sub @ ( esk10_3 @ X320 @ X325 @ X326 ) @ X326 ) )
| ( X320 @ ( sub @ X325 @ X326 ) )
| ~ ( X320 @ X324 )
| ( X320 @ ( sub @ ( esk9_1 @ X320 ) @ ( push @ X324 @ id ) ) )
| ~ ( X320 @ ( ap @ ( esk7_1 @ X320 ) @ ( esk8_1 @ X320 ) ) ) )
& ( ( var @ ( esk10_3 @ X320 @ X325 @ X326 ) )
| ( X320 @ ( sub @ X325 @ X326 ) )
| ~ ( X320 @ ( lam @ ( esk9_1 @ X320 ) ) )
| ~ ( X320 @ ( ap @ ( esk7_1 @ X320 ) @ ( esk8_1 @ X320 ) ) ) )
& ( ~ ( X320 @ ( sub @ ( esk10_3 @ X320 @ X325 @ X326 ) @ X326 ) )
| ( X320 @ ( sub @ X325 @ X326 ) )
| ~ ( X320 @ ( lam @ ( esk9_1 @ X320 ) ) )
| ~ ( X320 @ ( ap @ ( esk7_1 @ X320 ) @ ( esk8_1 @ X320 ) ) ) )
& ( ~ ( X328 @ X333 )
| ( X328 @ ( sub @ ( esk14_1 @ X328 ) @ ( push @ X333 @ id ) ) )
| ( X328 @ X334 )
| ( X328 @ ( esk12_1 @ X328 ) )
| ( var @ ( esk11_1 @ X328 ) ) )
& ( ~ ( X328 @ ( lam @ ( esk14_1 @ X328 ) ) )
| ( X328 @ X334 )
| ( X328 @ ( esk12_1 @ X328 ) )
| ( var @ ( esk11_1 @ X328 ) ) )
& ( ~ ( X328 @ X333 )
| ( X328 @ ( sub @ ( esk14_1 @ X328 ) @ ( push @ X333 @ id ) ) )
| ( X328 @ X334 )
| ( X328 @ ( esk13_1 @ X328 ) )
| ( var @ ( esk11_1 @ X328 ) ) )
& ( ~ ( X328 @ ( lam @ ( esk14_1 @ X328 ) ) )
| ( X328 @ X334 )
| ( X328 @ ( esk13_1 @ X328 ) )
| ( var @ ( esk11_1 @ X328 ) ) )
& ( ~ ( X328 @ X333 )
| ( X328 @ ( sub @ ( esk14_1 @ X328 ) @ ( push @ X333 @ id ) ) )
| ( X328 @ X334 )
| ~ ( X328 @ ( ap @ ( esk12_1 @ X328 ) @ ( esk13_1 @ X328 ) ) )
| ( var @ ( esk11_1 @ X328 ) ) )
& ( ~ ( X328 @ ( lam @ ( esk14_1 @ X328 ) ) )
| ( X328 @ X334 )
| ~ ( X328 @ ( ap @ ( esk12_1 @ X328 ) @ ( esk13_1 @ X328 ) ) )
| ( var @ ( esk11_1 @ X328 ) ) )
& ( ~ ( X328 @ X333 )
| ( X328 @ ( sub @ ( esk14_1 @ X328 ) @ ( push @ X333 @ id ) ) )
| ( X328 @ X334 )
| ( X328 @ ( esk12_1 @ X328 ) )
| ~ ( X328 @ ( esk11_1 @ X328 ) ) )
& ( ~ ( X328 @ ( lam @ ( esk14_1 @ X328 ) ) )
| ( X328 @ X334 )
| ( X328 @ ( esk12_1 @ X328 ) )
| ~ ( X328 @ ( esk11_1 @ X328 ) ) )
& ( ~ ( X328 @ X333 )
| ( X328 @ ( sub @ ( esk14_1 @ X328 ) @ ( push @ X333 @ id ) ) )
| ( X328 @ X334 )
| ( X328 @ ( esk13_1 @ X328 ) )
| ~ ( X328 @ ( esk11_1 @ X328 ) ) )
& ( ~ ( X328 @ ( lam @ ( esk14_1 @ X328 ) ) )
| ( X328 @ X334 )
| ( X328 @ ( esk13_1 @ X328 ) )
| ~ ( X328 @ ( esk11_1 @ X328 ) ) )
& ( ~ ( X328 @ X333 )
| ( X328 @ ( sub @ ( esk14_1 @ X328 ) @ ( push @ X333 @ id ) ) )
| ( X328 @ X334 )
| ~ ( X328 @ ( ap @ ( esk12_1 @ X328 ) @ ( esk13_1 @ X328 ) ) )
| ~ ( X328 @ ( esk11_1 @ X328 ) ) )
& ( ~ ( X328 @ ( lam @ ( esk14_1 @ X328 ) ) )
| ( X328 @ X334 )
| ~ ( X328 @ ( ap @ ( esk12_1 @ X328 ) @ ( esk13_1 @ X328 ) ) )
| ~ ( X328 @ ( esk11_1 @ X328 ) ) )
& ( ( comp @ ( comp @ X335 @ X336 ) @ X337 )
= ( comp @ X335 @ ( comp @ X336 @ X337 ) ) )
& ( ( comp @ id @ X338 )
= X338 )
& ( ( comp @ X339 @ id )
= X339 )
& ( ( ( sub @ ( sub @ esk15_0 @ esk16_0 ) @ esk17_0 )
!= ( sub @ esk15_0 @ ( comp @ esk16_0 @ esk17_0 ) ) )
| ( ( sub @ esk18_0 @ id )
!= esk18_0 ) ) ),
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_32])])])])])])]) ).
thf(c_0_34,negated_conjecture,
( ( ( sub @ ( sub @ esk15_0 @ esk16_0 ) @ esk17_0 )
!= ( sub @ esk15_0 @ ( comp @ esk16_0 @ esk17_0 ) ) )
| ( ( sub @ esk18_0 @ id )
!= esk18_0 ) ),
inference(split_conjunct,[status(thm)],[c_0_33]) ).
thf(c_0_35,negated_conjecture,
! [X1: term] :
( ( sub @ X1 @ id )
= X1 ),
inference(split_conjunct,[status(thm)],[c_0_33]) ).
thf(c_0_36,negated_conjecture,
! [X1: term,X3: subst,X4: subst] :
( ( sub @ ( sub @ X1 @ X3 ) @ X4 )
= ( sub @ X1 @ ( comp @ X3 @ X4 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_33]) ).
thf(c_0_37,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_34,c_0_35]),c_0_36])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ALG255^1 : TPTP v9.3.1. Bugfixed v5.2.0.
% 0.00/0.07 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.25 % Computer : n009.cluster.edu
% 0.11/0.25 % Model : x86_64 x86_64
% 0.11/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.25 % Memory : 8046.5625MB
% 0.11/0.25 % OS : Linux 6.8.0-71-generic
% 0.11/0.25 % CPULimit : 300
% 0.11/0.25 % WCLimit : 300
% 0.11/0.25 % DateTime : Tue Sep 29 17:33:00 UTC 2026
% 0.11/0.26 % CPUTime :
% 0.11/0.26 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.25/0.32 Running higher-order theorem proving
% 0.25/0.38 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.KHBqYtGr8Q/E---3.1_115084.p
% 0.36/0.45 % Version: 3.5.1-ho
% 0.36/0.45 % Preprocessing class: HSMMSLSSLLLNHFA.
% 0.36/0.45 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.36/0.45 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 0.36/0.45 % Starting post_as_ho1 with 300s (1) cores
% 0.36/0.45 % Starting post_as_ho5 with 300s (1) cores
% 0.36/0.45 % Starting post_as_ho10 with 300s (1) cores
% 0.36/0.45 % post_as_ho5 with pid 115099 completed with status 0
% 0.36/0.45 % Result found by post_as_ho5
% 0.36/0.45 % Preprocessing class: HSMMSLSSLLLNHFA.
% 0.36/0.45 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.36/0.45 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 0.36/0.45 % Starting post_as_ho1 with 300s (1) cores
% 0.36/0.45 % Starting post_as_ho5 with 300s (1) cores
% 0.36/0.45 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 1, sine = GSinE(CountFormulas,,true,1.0,0,2,20000,1.0,true))
% 0.36/0.45 % SinE strategy is GSinE(CountFormulas,,true,1.0,0,2,20000,1.0,true)
% 0.36/0.45 % Search class: HGHSM-FFMF31-MHFMMMBN
% 0.36/0.45 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.36/0.45 % Starting SubtermCWHack with 28s (1) cores
% 0.36/0.45 % SubtermCWHack with pid 115101 completed with status 0
% 0.36/0.45 % Result found by SubtermCWHack
% 0.36/0.45 % Preprocessing class: HSMMSLSSLLLNHFA.
% 0.36/0.45 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.36/0.45 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 0.36/0.45 % Starting post_as_ho1 with 300s (1) cores
% 0.36/0.45 % Starting post_as_ho5 with 300s (1) cores
% 0.36/0.45 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 1, sine = GSinE(CountFormulas,,true,1.0,0,2,20000,1.0,true))
% 0.36/0.45 % SinE strategy is GSinE(CountFormulas,,true,1.0,0,2,20000,1.0,true)
% 0.36/0.45 % Search class: HGHSM-FFMF31-MHFMMMBN
% 0.36/0.45 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.36/0.45 % Starting SubtermCWHack with 28s (1) cores
% 0.36/0.45 % Preprocessing time : 0.004 s
% 0.36/0.45
% 0.36/0.45 % Proof found!
% 0.36/0.45 % SZS status Theorem
% 0.36/0.45 % SZS output start CNFRefutation
% See solution above
% 0.36/0.45 % Parsed axioms : 238
% 0.36/0.45 % Removed by relevancy pruning/SinE : 208
% 0.36/0.45 % Initial clauses : 66
% 0.36/0.45 % Removed in clause preprocessing : 0
% 0.36/0.45 % Initial clauses in saturation : 66
% 0.36/0.45 % Processed clauses : 77
% 0.36/0.45 % ...of these trivial : 3
% 0.36/0.45 % ...subsumed : 24
% 0.36/0.45 % ...remaining for further processing : 49
% 0.36/0.45 % Other redundant clauses eliminated : 0
% 0.36/0.45 % Clauses deleted for lack of memory : 0
% 0.36/0.45 % Backward-subsumed : 0
% 0.36/0.45 % Backward-rewritten : 1
% 0.36/0.45 % Generated clauses : 141
% 0.36/0.45 % ...of the previous two non-redundant : 104
% 0.36/0.45 % ...aggressively subsumed : 0
% 0.36/0.45 % Contextual simplify-reflections : 0
% 0.36/0.45 % Paramodulations : 137
% 0.36/0.45 % Factorizations : 0
% 0.36/0.45 % NegExts : 0
% 0.36/0.45 % Equation resolutions : 4
% 0.36/0.45 % Disequality decompositions : 0
% 0.36/0.45 % Total rewrite steps : 72
% 0.36/0.45 % ...of those cached : 23
% 0.36/0.45 % Propositional unsat checks : 0
% 0.36/0.45 % Propositional check models : 0
% 0.36/0.45 % Propositional check unsatisfiable : 0
% 0.36/0.45 % Propositional clauses : 0
% 0.36/0.45 % Propositional clauses after purity: 0
% 0.36/0.45 % Propositional unsat core size : 0
% 0.36/0.45 % Propositional preprocessing time : 0.000
% 0.36/0.45 % Propositional encoding time : 0.000
% 0.36/0.45 % Propositional solver time : 0.000
% 0.36/0.45 % Success case prop preproc time : 0.000
% 0.36/0.45 % Success case prop encoding time : 0.000
% 0.36/0.45 % Success case prop solver time : 0.000
% 0.36/0.45 % Current number of processed clauses : 48
% 0.36/0.45 % Positive orientable unit clauses : 13
% 0.36/0.45 % Positive unorientable unit clauses: 0
% 0.36/0.45 % Negative unit clauses : 7
% 0.36/0.45 % Non-unit-clauses : 28
% 0.36/0.45 % Current number of unprocessed clauses: 93
% 0.36/0.45 % ...number of literals in the above : 386
% 0.36/0.45 % Current number of archived formulas : 0
% 0.36/0.45 % Current number of archived clauses : 1
% 0.36/0.45 % Clause-clause subsumption calls (NU) : 99
% 0.36/0.45 % Rec. Clause-clause subsumption calls : 68
% 0.36/0.45 % Non-unit clause-clause subsumptions : 12
% 0.36/0.45 % Unit Clause-clause subsumption calls : 0
% 0.36/0.45 % Rewrite failures with RHS unbound : 0
% 0.36/0.45 % BW rewrite match attempts : 1
% 0.36/0.45 % BW rewrite match successes : 1
% 0.36/0.45 % Condensation attempts : 0
% 0.36/0.45 % Condensation successes : 0
% 0.36/0.45 % Termbank termtop insertions : 13493
% 0.36/0.45 % Search garbage collected termcells : 3920
% 0.36/0.45
% 0.36/0.45 % -------------------------------------------------
% 0.36/0.45 % User time : 0.024 s
% 0.36/0.45 % System time : 0.006 s
% 0.36/0.45 % Total time : 0.030 s
% 0.36/0.45 % Maximum resident set size: 4952 pages
% 0.36/0.45
% 0.36/0.45 % -------------------------------------------------
% 0.36/0.45 % User time : 0.039 s
% 0.36/0.45 % System time : 0.013 s
% 0.36/0.45 % Total time : 0.052 s
% 0.36/0.45 % Maximum resident set size: 5120 pages
% 0.36/0.45 % E exiting
%------------------------------------------------------------------------------