%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ALG254^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 : n003.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.13s 0.28s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 29
% Syntax : Number of formulae : 38 ( 7 unt; 0 typ; 0 def)
% Number of atoms : 228 ( 103 equ; 0 cnn)
% Maximal formula atoms : 54 ( 6 avg)
% Number of connectives : 1643 ( 97 ~; 144 |; 68 &;1117 @)
% ( 28 <=>; 189 =>; 0 <=; 0 <~>)
% Maximal formula depth : 119 ( 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 : 286 ( 0 ^; 286 !; 0 ?; 286 :)
% 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_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_130,type,
substmonoid_gthm: $o ).
thf(decl_131,type,
ulamvarsh: $o ).
thf(decl_132,type,
induction2: $o ).
thf(decl_137,type,
axshiftcons: $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: subst ).
thf(decl_160,type,
esk16_0: subst ).
thf(decl_161,type,
esk17_0: subst ).
thf(decl_162,type,
esk18_0: subst ).
thf(decl_163,type,
esk19_0: subst ).
thf(thm,conjecture,
substmonoid_gthm,
file('/export/starexec/sandbox2/tmp/tmp.uo05HJi9dQ/E---3.1_2814272.p',thm) ).
thf(substmonoid_gthm,axiom,
( substmonoid_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 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.uo05HJi9dQ/E---3.1_2814272.p',substmonoid_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.uo05HJi9dQ/E---3.1_2814272.p',axapp) ).
thf(axvarcons,axiom,
( axvarcons
<=> ! [X1: term,X3: subst] :
( ( sub @ one @ ( push @ X1 @ X3 ) )
= X1 ) ),
file('/export/starexec/sandbox2/tmp/tmp.uo05HJi9dQ/E---3.1_2814272.p',axvarcons) ).
thf(axvarid,axiom,
( axvarid
<=> ! [X1: term] :
( ( sub @ X1 @ id )
= X1 ) ),
file('/export/starexec/sandbox2/tmp/tmp.uo05HJi9dQ/E---3.1_2814272.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.uo05HJi9dQ/E---3.1_2814272.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.uo05HJi9dQ/E---3.1_2814272.p',axclos) ).
thf(axidl,axiom,
( axidl
<=> ! [X3: subst] :
( ( comp @ id @ X3 )
= X3 ) ),
file('/export/starexec/sandbox2/tmp/tmp.uo05HJi9dQ/E---3.1_2814272.p',axidl) ).
thf(axshiftcons,axiom,
( axshiftcons
<=> ! [X1: term,X3: subst] :
( ( comp @ sh @ ( push @ X1 @ X3 ) )
= X3 ) ),
file('/export/starexec/sandbox2/tmp/tmp.uo05HJi9dQ/E---3.1_2814272.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.uo05HJi9dQ/E---3.1_2814272.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.uo05HJi9dQ/E---3.1_2814272.p',axmap) ).
thf(axidr,axiom,
( axidr
<=> ! [X3: subst] :
( ( comp @ X3 @ id )
= X3 ) ),
file('/export/starexec/sandbox2/tmp/tmp.uo05HJi9dQ/E---3.1_2814272.p',axidr) ).
thf(axvarshift,axiom,
( axvarshift
<=> ( ( push @ one @ sh )
= id ) ),
file('/export/starexec/sandbox2/tmp/tmp.uo05HJi9dQ/E---3.1_2814272.p',axvarshift) ).
thf(axscons,axiom,
( axscons
<=> ! [X3: subst] :
( ( push @ ( sub @ one @ X3 ) @ ( comp @ sh @ X3 ) )
= X3 ) ),
file('/export/starexec/sandbox2/tmp/tmp.uo05HJi9dQ/E---3.1_2814272.p',axscons) ).
thf(ulamvar1,axiom,
( ulamvar1
<=> ( var @ one ) ),
file('/export/starexec/sandbox2/tmp/tmp.uo05HJi9dQ/E---3.1_2814272.p',ulamvar1) ).
thf(ulamvarsh,axiom,
( ulamvarsh
<=> ! [X1: term] :
( ( var @ X1 )
=> ( var @ ( sub @ X1 @ sh ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.uo05HJi9dQ/E---3.1_2814272.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.uo05HJi9dQ/E---3.1_2814272.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.uo05HJi9dQ/E---3.1_2814272.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.uo05HJi9dQ/E---3.1_2814272.p',apinj2) ).
thf(laminj,axiom,
( laminj
<=> ! [X1: term,X2: term] :
( ( ( lam @ X1 )
= ( lam @ X2 ) )
=> ( X1 = X2 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.uo05HJi9dQ/E---3.1_2814272.p',laminj) ).
thf(shinj,axiom,
( shinj
<=> ! [X1: term,X2: term] :
( ( ( sub @ X1 @ sh )
= ( sub @ X2 @ sh ) )
=> ( X1 = X2 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.uo05HJi9dQ/E---3.1_2814272.p',shinj) ).
thf(lamnotap,axiom,
( lamnotap
<=> ! [X1: term,X2: term,X7: term] :
( ( lam @ X1 )
!= ( ap @ X2 @ X7 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.uo05HJi9dQ/E---3.1_2814272.p',lamnotap) ).
thf(apnotvar,axiom,
( apnotvar
<=> ! [X1: term,X2: term] :
~ ( var @ ( ap @ X1 @ X2 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.uo05HJi9dQ/E---3.1_2814272.p',apnotvar) ).
thf(lamnotvar,axiom,
( lamnotvar
<=> ! [X1: term] :
~ ( var @ ( lam @ X1 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.uo05HJi9dQ/E---3.1_2814272.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.uo05HJi9dQ/E---3.1_2814272.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.uo05HJi9dQ/E---3.1_2814272.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.uo05HJi9dQ/E---3.1_2814272.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.uo05HJi9dQ/E---3.1_2814272.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.uo05HJi9dQ/E---3.1_2814272.p',substmonoid) ).
thf(c_0_29,negated_conjecture,
~ substmonoid_gthm,
inference(assume_negation,[status(cth)],[thm]) ).
thf(c_0_30,axiom,
( substmonoid_gthm
= ( ! [X103: term,X104: term,X105: subst] :
( ( sub @ ( ap @ X103 @ X104 ) @ X105 )
= ( ap @ ( sub @ X103 @ X105 ) @ ( sub @ X104 @ X105 ) ) )
=> ( ! [X106: term,X107: subst] :
( ( sub @ one @ ( push @ X106 @ X107 ) )
= X106 )
=> ( ! [X108: term] :
( ( sub @ X108 @ id )
= X108 )
=> ( ! [X109: term,X110: subst] :
( ( sub @ ( lam @ X109 ) @ X110 )
= ( lam @ ( sub @ X109 @ ( push @ one @ ( comp @ X110 @ sh ) ) ) ) )
=> ( ! [X111: term,X112: subst,X113: subst] :
( ( sub @ ( sub @ X111 @ X112 ) @ X113 )
= ( sub @ X111 @ ( comp @ X112 @ X113 ) ) )
=> ( ! [X114: subst] :
( ( comp @ id @ X114 )
= X114 )
=> ( ! [X115: term,X116: subst] :
( ( comp @ sh @ ( push @ X115 @ X116 ) )
= X116 )
=> ( ! [X117: subst,X118: subst,X119: subst] :
( ( comp @ ( comp @ X117 @ X118 ) @ X119 )
= ( comp @ X117 @ ( comp @ X118 @ X119 ) ) )
=> ( ! [X120: term,X121: subst,X122: subst] :
( ( comp @ ( push @ X120 @ X121 ) @ X122 )
= ( push @ ( sub @ X120 @ X122 ) @ ( comp @ X121 @ X122 ) ) )
=> ( ! [X123: subst] :
( ( comp @ X123 @ id )
= X123 )
=> ( ( ( push @ one @ sh )
= id )
=> ( ! [X124: subst] :
( ( push @ ( sub @ one @ X124 ) @ ( comp @ sh @ X124 ) )
= X124 )
=> ( ( var @ one )
=> ( ! [X125: term] :
( ( var @ X125 )
=> ( var @ ( sub @ X125 @ sh ) ) )
=> ( ! [X126: term > $o] :
( ( X126 @ one )
=> ( ! [X127: term] :
( ( var @ X127 )
=> ( ( X126 @ X127 )
=> ( X126 @ ( sub @ X127 @ sh ) ) ) )
=> ! [X128: term] :
( ( var @ X128 )
=> ( X126 @ X128 ) ) ) )
=> ( ! [X129: term,X130: term,X131: term,X132: term] :
( ( ( ap @ X129 @ X131 )
= ( ap @ X130 @ X132 ) )
=> ( X129 = X130 ) )
=> ( ! [X133: term,X134: term,X135: term,X136: term] :
( ( ( ap @ X133 @ X135 )
= ( ap @ X134 @ X136 ) )
=> ( X135 = X136 ) )
=> ( ! [X137: term,X138: term] :
( ( ( lam @ X137 )
= ( lam @ X138 ) )
=> ( X137 = X138 ) )
=> ( ! [X139: term,X140: term] :
( ( ( sub @ X139 @ sh )
= ( sub @ X140 @ sh ) )
=> ( X139 = X140 ) )
=> ( ! [X141: term,X142: term,X143: term] :
( ( lam @ X141 )
!= ( ap @ X142 @ X143 ) )
=> ( ! [X144: term,X145: term] :
~ ( var @ ( ap @ X144 @ X145 ) )
=> ( ! [X146: term] :
~ ( var @ ( lam @ X146 ) )
=> ( ! [X147: term > $o] :
( ! [X148: term] :
( ( var @ X148 )
=> ( X147 @ X148 ) )
=> ( ! [X149: term,X150: term] :
( ( X147 @ X149 )
=> ( ( X147 @ X150 )
=> ( X147 @ ( ap @ X149 @ X150 ) ) ) )
=> ( ! [X151: term] :
( ( X147 @ X151 )
=> ( X147 @ ( lam @ X151 ) ) )
=> ! [X152: term] : ( X147 @ X152 ) ) ) )
=> ( ! [X153: term > $o,X154: term,X155: subst] :
( ! [X156: term] :
( ( var @ X156 )
=> ( X153 @ ( sub @ X156 @ X155 ) ) )
=> ( ( X153 @ X154 )
=> ! [X157: term] :
( ( var @ X157 )
=> ( X153 @ ( sub @ X157 @ ( push @ X154 @ X155 ) ) ) ) ) )
=> ( ! [X158: term > $o] :
( ! [X159: term,X160: term] :
( ( X158 @ X159 )
=> ( ( X158 @ X160 )
=> ( X158 @ ( ap @ X159 @ X160 ) ) ) )
=> ( ! [X161: term] :
( ! [X162: term] :
( ( X158 @ X162 )
=> ( X158 @ ( sub @ X161 @ ( push @ X162 @ id ) ) ) )
=> ( X158 @ ( lam @ X161 ) ) )
=> ! [X163: term,X164: subst] :
( ! [X165: term] :
( ( var @ X165 )
=> ( X158 @ ( sub @ X165 @ X164 ) ) )
=> ( X158 @ ( sub @ X163 @ X164 ) ) ) ) )
=> ( ! [X166: term > $o] :
( ! [X167: term] :
( ( var @ X167 )
=> ( X166 @ X167 ) )
=> ( ! [X168: term,X169: term] :
( ( X166 @ X168 )
=> ( ( X166 @ X169 )
=> ( X166 @ ( ap @ X168 @ X169 ) ) ) )
=> ( ! [X170: term] :
( ! [X171: term] :
( ( X166 @ X171 )
=> ( X166 @ ( sub @ X170 @ ( push @ X171 @ id ) ) ) )
=> ( X166 @ ( lam @ X170 ) ) )
=> ! [X172: term] : ( X166 @ X172 ) ) ) )
=> ( ! [X173: subst,X174: subst,X175: subst] :
( ( comp @ ( comp @ X173 @ X174 ) @ X175 )
= ( comp @ X173 @ ( comp @ X174 @ X175 ) ) )
& ! [X176: subst] :
( ( comp @ id @ X176 )
= X176 )
& ! [X177: subst] :
( ( comp @ X177 @ id )
= X177 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
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)],[substmonoid_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]) ).
thf(c_0_31,negated_conjecture,
~ ( ! [X178: term,X179: term,X180: subst] :
( ( sub @ ( ap @ X178 @ X179 ) @ X180 )
= ( ap @ ( sub @ X178 @ X180 ) @ ( sub @ X179 @ X180 ) ) )
=> ( ! [X181: term,X182: subst] :
( ( sub @ one @ ( push @ X181 @ X182 ) )
= X181 )
=> ( ! [X183: term] :
( ( sub @ X183 @ id )
= X183 )
=> ( ! [X184: term,X185: subst] :
( ( sub @ ( lam @ X184 ) @ X185 )
= ( lam @ ( sub @ X184 @ ( push @ one @ ( comp @ X185 @ sh ) ) ) ) )
=> ( ! [X186: term,X187: subst,X188: subst] :
( ( sub @ ( sub @ X186 @ X187 ) @ X188 )
= ( sub @ X186 @ ( comp @ X187 @ X188 ) ) )
=> ( ! [X189: subst] :
( ( comp @ id @ X189 )
= X189 )
=> ( ! [X190: term,X191: subst] :
( ( comp @ sh @ ( push @ X190 @ X191 ) )
= X191 )
=> ( ! [X192: subst,X193: subst,X194: subst] :
( ( comp @ ( comp @ X192 @ X193 ) @ X194 )
= ( comp @ X192 @ ( comp @ X193 @ X194 ) ) )
=> ( ! [X195: term,X196: subst,X197: subst] :
( ( comp @ ( push @ X195 @ X196 ) @ X197 )
= ( push @ ( sub @ X195 @ X197 ) @ ( comp @ X196 @ X197 ) ) )
=> ( ! [X198: subst] :
( ( comp @ X198 @ id )
= X198 )
=> ( ( ( push @ one @ sh )
= id )
=> ( ! [X199: subst] :
( ( push @ ( sub @ one @ X199 ) @ ( comp @ sh @ X199 ) )
= X199 )
=> ( ( var @ one )
=> ( ! [X200: term] :
( ( var @ X200 )
=> ( var @ ( sub @ X200 @ sh ) ) )
=> ( ! [X201: term > $o] :
( ( X201 @ one )
=> ( ! [X202: term] :
( ( var @ X202 )
=> ( ( X201 @ X202 )
=> ( X201 @ ( sub @ X202 @ sh ) ) ) )
=> ! [X203: term] :
( ( var @ X203 )
=> ( X201 @ X203 ) ) ) )
=> ( ! [X204: term,X205: term,X206: term,X207: term] :
( ( ( ap @ X204 @ X206 )
= ( ap @ X205 @ X207 ) )
=> ( X204 = X205 ) )
=> ( ! [X208: term,X209: term,X210: term,X211: term] :
( ( ( ap @ X208 @ X210 )
= ( ap @ X209 @ X211 ) )
=> ( X210 = X211 ) )
=> ( ! [X212: term,X213: term] :
( ( ( lam @ X212 )
= ( lam @ X213 ) )
=> ( X212 = X213 ) )
=> ( ! [X214: term,X215: term] :
( ( ( sub @ X214 @ sh )
= ( sub @ X215 @ sh ) )
=> ( X214 = X215 ) )
=> ( ! [X216: term,X217: term,X218: term] :
( ( lam @ X216 )
!= ( ap @ X217 @ X218 ) )
=> ( ! [X219: term,X220: term] :
~ ( var @ ( ap @ X219 @ X220 ) )
=> ( ! [X221: term] :
~ ( var @ ( lam @ X221 ) )
=> ( ! [X222: term > $o] :
( ! [X223: term] :
( ( var @ X223 )
=> ( X222 @ X223 ) )
=> ( ! [X224: term,X225: term] :
( ( X222 @ X224 )
=> ( ( X222 @ X225 )
=> ( X222 @ ( ap @ X224 @ X225 ) ) ) )
=> ( ! [X226: term] :
( ( X222 @ X226 )
=> ( X222 @ ( lam @ X226 ) ) )
=> ! [X227: term] : ( X222 @ X227 ) ) ) )
=> ( ! [X228: term > $o,X229: term,X230: subst] :
( ! [X231: term] :
( ( var @ X231 )
=> ( X228 @ ( sub @ X231 @ X230 ) ) )
=> ( ( X228 @ X229 )
=> ! [X232: term] :
( ( var @ X232 )
=> ( X228 @ ( sub @ X232 @ ( push @ X229 @ X230 ) ) ) ) ) )
=> ( ! [X233: term > $o] :
( ! [X234: term,X235: term] :
( ( X233 @ X234 )
=> ( ( X233 @ X235 )
=> ( X233 @ ( ap @ X234 @ X235 ) ) ) )
=> ( ! [X236: term] :
( ! [X237: term] :
( ( X233 @ X237 )
=> ( X233 @ ( sub @ X236 @ ( push @ X237 @ id ) ) ) )
=> ( X233 @ ( lam @ X236 ) ) )
=> ! [X238: term,X239: subst] :
( ! [X240: term] :
( ( var @ X240 )
=> ( X233 @ ( sub @ X240 @ X239 ) ) )
=> ( X233 @ ( sub @ X238 @ X239 ) ) ) ) )
=> ( ! [X241: term > $o] :
( ! [X242: term] :
( ( var @ X242 )
=> ( X241 @ X242 ) )
=> ( ! [X243: term,X244: term] :
( ( X241 @ X243 )
=> ( ( X241 @ X244 )
=> ( X241 @ ( ap @ X243 @ X244 ) ) ) )
=> ( ! [X245: term] :
( ! [X246: term] :
( ( X241 @ X246 )
=> ( X241 @ ( sub @ X245 @ ( push @ X246 @ id ) ) ) )
=> ( X241 @ ( lam @ X245 ) ) )
=> ! [X247: term] : ( X241 @ X247 ) ) ) )
=> ( ! [X248: subst,X249: subst,X250: subst] :
( ( comp @ ( comp @ X248 @ X249 ) @ X250 )
= ( comp @ X248 @ ( comp @ X249 @ X250 ) ) )
& ! [X251: subst] :
( ( comp @ id @ X251 )
= X251 )
& ! [X252: subst] :
( ( comp @ X252 @ id )
= X252 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[c_0_29,c_0_30])]) ).
thf(c_0_32,negated_conjecture,
! [X253: term,X254: term,X255: subst,X256: term,X257: subst,X258: term,X259: term,X260: subst,X261: term,X262: subst,X263: subst,X264: subst,X265: term,X266: subst,X267: subst,X268: subst,X269: subst,X270: term,X271: subst,X272: subst,X273: subst,X274: subst,X275: term,X276: term > $o,X278: term,X279: term,X280: term,X281: term,X282: term,X283: term,X284: term,X285: term,X286: term,X287: term,X288: term,X289: term,X290: term,X291: term,X292: term,X293: term,X294: term,X295: term,X296: term,X297: term > $o,X302: term,X303: term > $o,X304: term,X305: subst,X307: term,X308: term > $o,X312: term,X313: term,X314: subst,X316: term > $o,X321: term,X322: term] :
( ( ( sub @ ( ap @ X253 @ X254 ) @ X255 )
= ( ap @ ( sub @ X253 @ X255 ) @ ( sub @ X254 @ X255 ) ) )
& ( ( sub @ one @ ( push @ X256 @ X257 ) )
= X256 )
& ( ( sub @ X258 @ id )
= X258 )
& ( ( sub @ ( lam @ X259 ) @ X260 )
= ( lam @ ( sub @ X259 @ ( push @ one @ ( comp @ X260 @ sh ) ) ) ) )
& ( ( sub @ ( sub @ X261 @ X262 ) @ X263 )
= ( sub @ X261 @ ( comp @ X262 @ X263 ) ) )
& ( ( comp @ id @ X264 )
= X264 )
& ( ( comp @ sh @ ( push @ X265 @ X266 ) )
= X266 )
& ( ( comp @ ( comp @ X267 @ X268 ) @ X269 )
= ( comp @ X267 @ ( comp @ X268 @ X269 ) ) )
& ( ( comp @ ( push @ X270 @ X271 ) @ X272 )
= ( push @ ( sub @ X270 @ X272 ) @ ( comp @ X271 @ X272 ) ) )
& ( ( comp @ X273 @ id )
= X273 )
& ( ( push @ one @ sh )
= id )
& ( ( push @ ( sub @ one @ X274 ) @ ( comp @ sh @ X274 ) )
= X274 )
& ( var @ one )
& ( ~ ( var @ X275 )
| ( var @ ( sub @ X275 @ sh ) ) )
& ( ( var @ ( esk1_1 @ X276 ) )
| ~ ( var @ X278 )
| ( X276 @ X278 )
| ~ ( X276 @ one ) )
& ( ( X276 @ ( esk1_1 @ X276 ) )
| ~ ( var @ X278 )
| ( X276 @ X278 )
| ~ ( X276 @ one ) )
& ( ~ ( X276 @ ( sub @ ( esk1_1 @ X276 ) @ sh ) )
| ~ ( var @ X278 )
| ( X276 @ X278 )
| ~ ( X276 @ one ) )
& ( ( ( ap @ X279 @ X281 )
!= ( ap @ X280 @ X282 ) )
| ( X279 = X280 ) )
& ( ( ( ap @ X283 @ X285 )
!= ( ap @ X284 @ X286 ) )
| ( X285 = X286 ) )
& ( ( ( lam @ X287 )
!= ( lam @ X288 ) )
| ( X287 = X288 ) )
& ( ( ( sub @ X289 @ sh )
!= ( sub @ X290 @ sh ) )
| ( X289 = X290 ) )
& ( ( lam @ X291 )
!= ( ap @ X292 @ X293 ) )
& ~ ( var @ ( ap @ X294 @ X295 ) )
& ~ ( var @ ( lam @ X296 ) )
& ( ( X297 @ ( esk5_1 @ X297 ) )
| ( X297 @ X302 )
| ( X297 @ ( esk3_1 @ X297 ) )
| ( var @ ( esk2_1 @ X297 ) ) )
& ( ~ ( X297 @ ( lam @ ( esk5_1 @ X297 ) ) )
| ( X297 @ X302 )
| ( X297 @ ( esk3_1 @ X297 ) )
| ( var @ ( esk2_1 @ X297 ) ) )
& ( ( X297 @ ( esk5_1 @ X297 ) )
| ( X297 @ X302 )
| ( X297 @ ( esk4_1 @ X297 ) )
| ( var @ ( esk2_1 @ X297 ) ) )
& ( ~ ( X297 @ ( lam @ ( esk5_1 @ X297 ) ) )
| ( X297 @ X302 )
| ( X297 @ ( esk4_1 @ X297 ) )
| ( var @ ( esk2_1 @ X297 ) ) )
& ( ( X297 @ ( esk5_1 @ X297 ) )
| ( X297 @ X302 )
| ~ ( X297 @ ( ap @ ( esk3_1 @ X297 ) @ ( esk4_1 @ X297 ) ) )
| ( var @ ( esk2_1 @ X297 ) ) )
& ( ~ ( X297 @ ( lam @ ( esk5_1 @ X297 ) ) )
| ( X297 @ X302 )
| ~ ( X297 @ ( ap @ ( esk3_1 @ X297 ) @ ( esk4_1 @ X297 ) ) )
| ( var @ ( esk2_1 @ X297 ) ) )
& ( ( X297 @ ( esk5_1 @ X297 ) )
| ( X297 @ X302 )
| ( X297 @ ( esk3_1 @ X297 ) )
| ~ ( X297 @ ( esk2_1 @ X297 ) ) )
& ( ~ ( X297 @ ( lam @ ( esk5_1 @ X297 ) ) )
| ( X297 @ X302 )
| ( X297 @ ( esk3_1 @ X297 ) )
| ~ ( X297 @ ( esk2_1 @ X297 ) ) )
& ( ( X297 @ ( esk5_1 @ X297 ) )
| ( X297 @ X302 )
| ( X297 @ ( esk4_1 @ X297 ) )
| ~ ( X297 @ ( esk2_1 @ X297 ) ) )
& ( ~ ( X297 @ ( lam @ ( esk5_1 @ X297 ) ) )
| ( X297 @ X302 )
| ( X297 @ ( esk4_1 @ X297 ) )
| ~ ( X297 @ ( esk2_1 @ X297 ) ) )
& ( ( X297 @ ( esk5_1 @ X297 ) )
| ( X297 @ X302 )
| ~ ( X297 @ ( ap @ ( esk3_1 @ X297 ) @ ( esk4_1 @ X297 ) ) )
| ~ ( X297 @ ( esk2_1 @ X297 ) ) )
& ( ~ ( X297 @ ( lam @ ( esk5_1 @ X297 ) ) )
| ( X297 @ X302 )
| ~ ( X297 @ ( ap @ ( esk3_1 @ X297 ) @ ( esk4_1 @ X297 ) ) )
| ~ ( X297 @ ( esk2_1 @ X297 ) ) )
& ( ( var @ ( esk6_3 @ X303 @ X304 @ X305 ) )
| ~ ( X303 @ X304 )
| ~ ( var @ X307 )
| ( X303 @ ( sub @ X307 @ ( push @ X304 @ X305 ) ) ) )
& ( ~ ( X303 @ ( sub @ ( esk6_3 @ X303 @ X304 @ X305 ) @ X305 ) )
| ~ ( X303 @ X304 )
| ~ ( var @ X307 )
| ( X303 @ ( sub @ X307 @ ( push @ X304 @ X305 ) ) ) )
& ( ( var @ ( esk10_3 @ X308 @ X313 @ X314 ) )
| ( X308 @ ( sub @ X313 @ X314 ) )
| ~ ( X308 @ X312 )
| ( X308 @ ( sub @ ( esk9_1 @ X308 ) @ ( push @ X312 @ id ) ) )
| ( X308 @ ( esk7_1 @ X308 ) ) )
& ( ~ ( X308 @ ( sub @ ( esk10_3 @ X308 @ X313 @ X314 ) @ X314 ) )
| ( X308 @ ( sub @ X313 @ X314 ) )
| ~ ( X308 @ X312 )
| ( X308 @ ( sub @ ( esk9_1 @ X308 ) @ ( push @ X312 @ id ) ) )
| ( X308 @ ( esk7_1 @ X308 ) ) )
& ( ( var @ ( esk10_3 @ X308 @ X313 @ X314 ) )
| ( X308 @ ( sub @ X313 @ X314 ) )
| ~ ( X308 @ ( lam @ ( esk9_1 @ X308 ) ) )
| ( X308 @ ( esk7_1 @ X308 ) ) )
& ( ~ ( X308 @ ( sub @ ( esk10_3 @ X308 @ X313 @ X314 ) @ X314 ) )
| ( X308 @ ( sub @ X313 @ X314 ) )
| ~ ( X308 @ ( lam @ ( esk9_1 @ X308 ) ) )
| ( X308 @ ( esk7_1 @ X308 ) ) )
& ( ( var @ ( esk10_3 @ X308 @ X313 @ X314 ) )
| ( X308 @ ( sub @ X313 @ X314 ) )
| ~ ( X308 @ X312 )
| ( X308 @ ( sub @ ( esk9_1 @ X308 ) @ ( push @ X312 @ id ) ) )
| ( X308 @ ( esk8_1 @ X308 ) ) )
& ( ~ ( X308 @ ( sub @ ( esk10_3 @ X308 @ X313 @ X314 ) @ X314 ) )
| ( X308 @ ( sub @ X313 @ X314 ) )
| ~ ( X308 @ X312 )
| ( X308 @ ( sub @ ( esk9_1 @ X308 ) @ ( push @ X312 @ id ) ) )
| ( X308 @ ( esk8_1 @ X308 ) ) )
& ( ( var @ ( esk10_3 @ X308 @ X313 @ X314 ) )
| ( X308 @ ( sub @ X313 @ X314 ) )
| ~ ( X308 @ ( lam @ ( esk9_1 @ X308 ) ) )
| ( X308 @ ( esk8_1 @ X308 ) ) )
& ( ~ ( X308 @ ( sub @ ( esk10_3 @ X308 @ X313 @ X314 ) @ X314 ) )
| ( X308 @ ( sub @ X313 @ X314 ) )
| ~ ( X308 @ ( lam @ ( esk9_1 @ X308 ) ) )
| ( X308 @ ( esk8_1 @ X308 ) ) )
& ( ( var @ ( esk10_3 @ X308 @ X313 @ X314 ) )
| ( X308 @ ( sub @ X313 @ X314 ) )
| ~ ( X308 @ X312 )
| ( X308 @ ( sub @ ( esk9_1 @ X308 ) @ ( push @ X312 @ id ) ) )
| ~ ( X308 @ ( ap @ ( esk7_1 @ X308 ) @ ( esk8_1 @ X308 ) ) ) )
& ( ~ ( X308 @ ( sub @ ( esk10_3 @ X308 @ X313 @ X314 ) @ X314 ) )
| ( X308 @ ( sub @ X313 @ X314 ) )
| ~ ( X308 @ X312 )
| ( X308 @ ( sub @ ( esk9_1 @ X308 ) @ ( push @ X312 @ id ) ) )
| ~ ( X308 @ ( ap @ ( esk7_1 @ X308 ) @ ( esk8_1 @ X308 ) ) ) )
& ( ( var @ ( esk10_3 @ X308 @ X313 @ X314 ) )
| ( X308 @ ( sub @ X313 @ X314 ) )
| ~ ( X308 @ ( lam @ ( esk9_1 @ X308 ) ) )
| ~ ( X308 @ ( ap @ ( esk7_1 @ X308 ) @ ( esk8_1 @ X308 ) ) ) )
& ( ~ ( X308 @ ( sub @ ( esk10_3 @ X308 @ X313 @ X314 ) @ X314 ) )
| ( X308 @ ( sub @ X313 @ X314 ) )
| ~ ( X308 @ ( lam @ ( esk9_1 @ X308 ) ) )
| ~ ( X308 @ ( ap @ ( esk7_1 @ X308 ) @ ( esk8_1 @ X308 ) ) ) )
& ( ~ ( X316 @ X321 )
| ( X316 @ ( sub @ ( esk14_1 @ X316 ) @ ( push @ X321 @ id ) ) )
| ( X316 @ X322 )
| ( X316 @ ( esk12_1 @ X316 ) )
| ( var @ ( esk11_1 @ X316 ) ) )
& ( ~ ( X316 @ ( lam @ ( esk14_1 @ X316 ) ) )
| ( X316 @ X322 )
| ( X316 @ ( esk12_1 @ X316 ) )
| ( var @ ( esk11_1 @ X316 ) ) )
& ( ~ ( X316 @ X321 )
| ( X316 @ ( sub @ ( esk14_1 @ X316 ) @ ( push @ X321 @ id ) ) )
| ( X316 @ X322 )
| ( X316 @ ( esk13_1 @ X316 ) )
| ( var @ ( esk11_1 @ X316 ) ) )
& ( ~ ( X316 @ ( lam @ ( esk14_1 @ X316 ) ) )
| ( X316 @ X322 )
| ( X316 @ ( esk13_1 @ X316 ) )
| ( var @ ( esk11_1 @ X316 ) ) )
& ( ~ ( X316 @ X321 )
| ( X316 @ ( sub @ ( esk14_1 @ X316 ) @ ( push @ X321 @ id ) ) )
| ( X316 @ X322 )
| ~ ( X316 @ ( ap @ ( esk12_1 @ X316 ) @ ( esk13_1 @ X316 ) ) )
| ( var @ ( esk11_1 @ X316 ) ) )
& ( ~ ( X316 @ ( lam @ ( esk14_1 @ X316 ) ) )
| ( X316 @ X322 )
| ~ ( X316 @ ( ap @ ( esk12_1 @ X316 ) @ ( esk13_1 @ X316 ) ) )
| ( var @ ( esk11_1 @ X316 ) ) )
& ( ~ ( X316 @ X321 )
| ( X316 @ ( sub @ ( esk14_1 @ X316 ) @ ( push @ X321 @ id ) ) )
| ( X316 @ X322 )
| ( X316 @ ( esk12_1 @ X316 ) )
| ~ ( X316 @ ( esk11_1 @ X316 ) ) )
& ( ~ ( X316 @ ( lam @ ( esk14_1 @ X316 ) ) )
| ( X316 @ X322 )
| ( X316 @ ( esk12_1 @ X316 ) )
| ~ ( X316 @ ( esk11_1 @ X316 ) ) )
& ( ~ ( X316 @ X321 )
| ( X316 @ ( sub @ ( esk14_1 @ X316 ) @ ( push @ X321 @ id ) ) )
| ( X316 @ X322 )
| ( X316 @ ( esk13_1 @ X316 ) )
| ~ ( X316 @ ( esk11_1 @ X316 ) ) )
& ( ~ ( X316 @ ( lam @ ( esk14_1 @ X316 ) ) )
| ( X316 @ X322 )
| ( X316 @ ( esk13_1 @ X316 ) )
| ~ ( X316 @ ( esk11_1 @ X316 ) ) )
& ( ~ ( X316 @ X321 )
| ( X316 @ ( sub @ ( esk14_1 @ X316 ) @ ( push @ X321 @ id ) ) )
| ( X316 @ X322 )
| ~ ( X316 @ ( ap @ ( esk12_1 @ X316 ) @ ( esk13_1 @ X316 ) ) )
| ~ ( X316 @ ( esk11_1 @ X316 ) ) )
& ( ~ ( X316 @ ( lam @ ( esk14_1 @ X316 ) ) )
| ( X316 @ X322 )
| ~ ( X316 @ ( ap @ ( esk12_1 @ X316 ) @ ( esk13_1 @ X316 ) ) )
| ~ ( X316 @ ( esk11_1 @ X316 ) ) )
& ( ( ( comp @ ( comp @ esk15_0 @ esk16_0 ) @ esk17_0 )
!= ( comp @ esk15_0 @ ( comp @ esk16_0 @ esk17_0 ) ) )
| ( ( comp @ id @ esk18_0 )
!= esk18_0 )
| ( ( comp @ esk19_0 @ id )
!= esk19_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_31])])])])])])]) ).
thf(c_0_33,negated_conjecture,
( ( ( comp @ ( comp @ esk15_0 @ esk16_0 ) @ esk17_0 )
!= ( comp @ esk15_0 @ ( comp @ esk16_0 @ esk17_0 ) ) )
| ( ( comp @ id @ esk18_0 )
!= esk18_0 )
| ( ( comp @ esk19_0 @ id )
!= esk19_0 ) ),
inference(split_conjunct,[status(thm)],[c_0_32]) ).
thf(c_0_34,negated_conjecture,
! [X3: subst] :
( ( comp @ id @ X3 )
= X3 ),
inference(split_conjunct,[status(thm)],[c_0_32]) ).
thf(c_0_35,negated_conjecture,
! [X3: subst] :
( ( comp @ X3 @ id )
= X3 ),
inference(split_conjunct,[status(thm)],[c_0_32]) ).
thf(c_0_36,negated_conjecture,
! [X3: subst,X4: subst,X5: subst] :
( ( comp @ ( comp @ X3 @ X4 ) @ X5 )
= ( comp @ X3 @ ( comp @ X4 @ X5 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_32]) ).
thf(c_0_37,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_33,c_0_34]),c_0_35]),c_0_36])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG254^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.13/0.17 % Computer : n003.cluster.edu
% 0.13/0.17 % Model : x86_64 x86_64
% 0.13/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.17 % Memory : 8046.5625MB
% 0.13/0.17 % OS : Linux 6.8.0-71-generic
% 0.13/0.17 % CPULimit : 300
% 0.13/0.17 % WCLimit : 300
% 0.13/0.17 % DateTime : Tue Sep 29 17:34:44 UTC 2026
% 0.13/0.17 % CPUTime :
% 0.13/0.17 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.20 Running higher-order theorem proving
% 0.13/0.24 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.uo05HJi9dQ/E---3.1_2814272.p
% 0.13/0.28 % Version: 3.5.1-ho
% 0.13/0.28 % Preprocessing class: HSMMSLSSLLLNHFA.
% 0.13/0.28 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.13/0.28 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 0.13/0.28 % Starting post_as_ho1 with 300s (1) cores
% 0.13/0.28 % Starting post_as_ho5 with 300s (1) cores
% 0.13/0.28 % Starting post_as_ho10 with 300s (1) cores
% 0.13/0.28 % post_as_ho5 with pid 2814310 completed with status 0
% 0.13/0.28 % Result found by post_as_ho5
% 0.13/0.28 % Preprocessing class: HSMMSLSSLLLNHFA.
% 0.13/0.28 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.13/0.28 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 0.13/0.28 % Starting post_as_ho1 with 300s (1) cores
% 0.13/0.28 % Starting post_as_ho5 with 300s (1) cores
% 0.13/0.28 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 1, sine = GSinE(CountFormulas,,true,1.0,0,2,20000,1.0,true))
% 0.13/0.28 % SinE strategy is GSinE(CountFormulas,,true,1.0,0,2,20000,1.0,true)
% 0.13/0.28 % Search class: HGHSM-FFMF31-MHFMMMBN
% 0.13/0.28 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.13/0.28 % Starting SubtermCWHack with 28s (1) cores
% 0.13/0.28 % SubtermCWHack with pid 2814312 completed with status 0
% 0.13/0.28 % Result found by SubtermCWHack
% 0.13/0.28 % Preprocessing class: HSMMSLSSLLLNHFA.
% 0.13/0.28 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.13/0.28 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 0.13/0.28 % Starting post_as_ho1 with 300s (1) cores
% 0.13/0.28 % Starting post_as_ho5 with 300s (1) cores
% 0.13/0.28 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 1, sine = GSinE(CountFormulas,,true,1.0,0,2,20000,1.0,true))
% 0.13/0.28 % SinE strategy is GSinE(CountFormulas,,true,1.0,0,2,20000,1.0,true)
% 0.13/0.28 % Search class: HGHSM-FFMF31-MHFMMMBN
% 0.13/0.28 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.13/0.28 % Starting SubtermCWHack with 28s (1) cores
% 0.13/0.28 % Preprocessing time : 0.003 s
% 0.13/0.28
% 0.13/0.28 % Proof found!
% 0.13/0.28 % SZS status Theorem
% 0.13/0.28 % SZS output start CNFRefutation
% See solution above
% 0.13/0.28 % Parsed axioms : 238
% 0.13/0.28 % Removed by relevancy pruning/SinE : 209
% 0.13/0.28 % Initial clauses : 63
% 0.13/0.28 % Removed in clause preprocessing : 0
% 0.13/0.28 % Initial clauses in saturation : 63
% 0.13/0.28 % Processed clauses : 88
% 0.13/0.28 % ...of these trivial : 0
% 0.13/0.28 % ...subsumed : 35
% 0.13/0.28 % ...remaining for further processing : 52
% 0.13/0.28 % Other redundant clauses eliminated : 0
% 0.13/0.28 % Clauses deleted for lack of memory : 0
% 0.13/0.28 % Backward-subsumed : 0
% 0.13/0.28 % Backward-rewritten : 1
% 0.13/0.28 % Generated clauses : 174
% 0.13/0.28 % ...of the previous two non-redundant : 131
% 0.13/0.28 % ...aggressively subsumed : 0
% 0.13/0.28 % Contextual simplify-reflections : 0
% 0.13/0.28 % Paramodulations : 170
% 0.13/0.28 % Factorizations : 0
% 0.13/0.28 % NegExts : 0
% 0.13/0.28 % Equation resolutions : 4
% 0.13/0.28 % Disequality decompositions : 0
% 0.13/0.28 % Total rewrite steps : 84
% 0.13/0.28 % ...of those cached : 25
% 0.13/0.28 % Propositional unsat checks : 0
% 0.13/0.28 % Propositional check models : 0
% 0.13/0.28 % Propositional check unsatisfiable : 0
% 0.13/0.28 % Propositional clauses : 0
% 0.13/0.28 % Propositional clauses after purity: 0
% 0.13/0.28 % Propositional unsat core size : 0
% 0.13/0.28 % Propositional preprocessing time : 0.000
% 0.13/0.28 % Propositional encoding time : 0.000
% 0.13/0.28 % Propositional solver time : 0.000
% 0.13/0.28 % Success case prop preproc time : 0.000
% 0.13/0.28 % Success case prop encoding time : 0.000
% 0.13/0.28 % Success case prop solver time : 0.000
% 0.13/0.28 % Current number of processed clauses : 51
% 0.13/0.28 % Positive orientable unit clauses : 13
% 0.13/0.28 % Positive unorientable unit clauses: 1
% 0.13/0.28 % Negative unit clauses : 9
% 0.13/0.28 % Non-unit-clauses : 28
% 0.13/0.28 % Current number of unprocessed clauses: 106
% 0.13/0.28 % ...number of literals in the above : 405
% 0.13/0.28 % Current number of archived formulas : 0
% 0.13/0.28 % Current number of archived clauses : 1
% 0.13/0.28 % Clause-clause subsumption calls (NU) : 93
% 0.13/0.28 % Rec. Clause-clause subsumption calls : 65
% 0.13/0.28 % Non-unit clause-clause subsumptions : 12
% 0.13/0.28 % Unit Clause-clause subsumption calls : 1
% 0.13/0.28 % Rewrite failures with RHS unbound : 0
% 0.13/0.28 % BW rewrite match attempts : 2
% 0.13/0.28 % BW rewrite match successes : 1
% 0.13/0.28 % Condensation attempts : 0
% 0.13/0.28 % Condensation successes : 0
% 0.13/0.28 % Termbank termtop insertions : 13598
% 0.13/0.28 % Search garbage collected termcells : 3856
% 0.13/0.28
% 0.13/0.28 % -------------------------------------------------
% 0.13/0.28 % User time : 0.014 s
% 0.13/0.28 % System time : 0.006 s
% 0.13/0.28 % Total time : 0.020 s
% 0.13/0.28 % Maximum resident set size: 5004 pages
% 0.13/0.28
% 0.13/0.28 % -------------------------------------------------
% 0.13/0.29 % User time : 0.024 s
% 0.13/0.29 % System time : 0.010 s
% 0.13/0.29 % Total time : 0.034 s
% 0.13/0.29 % Maximum resident set size: 4864 pages
% 0.13/0.29 % E exiting
%------------------------------------------------------------------------------