%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU859^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n012.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 08:34:18 AM UTC 2026
% Result : Theorem 4.34s 0.82s
% Output : Refutation 4.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SEU859^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.00/0.11 % Computer : n012.cluster.edu
% 0.00/0.11 % Model : x86_64 x86_64
% 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.11 % Memory : 8046.5625MB
% 0.00/0.11 % OS : Linux 6.8.0-71-generic
% 0.00/0.11 % CPULimit : 300
% 0.00/0.11 % WCLimit : 300
% 0.00/0.11 % DateTime : Tue Sep 29 14:40:47 UTC 2026
% 0.00/0.11 % CPUTime :
% 0.00/0.11 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.12 Running first-order model finding
% 0.09/0.12 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.86/0.79 % (193905)Will run a generic schedule for satisfiability detection.
% 3.86/0.79 % (193918)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4251477299_3000 on theBenchmark for (3000ds/0Mi)
% 3.86/0.79 % Exception at run slice level
% 3.86/0.79 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.86/0.79 % (193923)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4126903931:i=131_3000 on theBenchmark for (3000ds/131Mi)
% 3.86/0.79 % (193922)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1247188338:i=116_3000 on theBenchmark for (3000ds/116Mi)
% 3.86/0.79 % (193921)dis+10_1_sil=32000:sp=arity:random_seed=196541784:i=103:fgj=on_3000 on theBenchmark for (3000ds/103Mi)
% 3.86/0.79 % (193920)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=13398258:i=88024:add=on:rawr=on_3000 on theBenchmark for (3000ds/88024Mi)
% 3.86/0.79 % (193924)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3097700159:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_3000 on theBenchmark for (3000ds/159Mi)
% 3.86/0.79 % (193922)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.86/0.79 % (193919)% WARNING: option uhcvi not known.
% 3.86/0.79 % (193919)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3780569821:i=135531:add=off:rawr=on_3000 on theBenchmark for (3000ds/135531Mi)
% 3.86/0.79 % (193919)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.86/0.79 % (193919)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.86/0.79 % (193933)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3462577898:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.86/0.79 % Exception at run slice level
% 3.86/0.79 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.86/0.79 % (193944)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=579492599:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.86/0.79 % (193921)Instruction limit reached!
% 3.86/0.79 % (193921)------------------------------
% 3.86/0.79 % (193921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.86/0.79 % (193921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/0.79 % (193921)CaDiCaL version: 2.1.3
% 3.86/0.79 % (193921)Termination reason: Instruction limit
% 3.86/0.79 % (193921)Termination phase: Saturation
% 3.86/0.79 % (193921)Time elapsed: 0.048 s
% 3.86/0.79 % (193921)Peak memory usage: 12 MB
% 3.86/0.79 % (193921)Instructions burned: 103 (million)
% 3.86/0.79 % (193922)Instruction limit reached!
% 3.86/0.79 % (193922)------------------------------
% 3.86/0.79 % (193922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.86/0.79 % (193922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/0.79 % (193922)CaDiCaL version: 2.1.3
% 3.86/0.79 % (193922)Termination reason: Instruction limit
% 3.86/0.79 % (193922)Termination phase: Saturation
% 3.86/0.79 % (193922)Time elapsed: 0.052 s
% 3.86/0.79 % (193922)Peak memory usage: 12 MB
% 3.86/0.79 % (193922)Instructions burned: 117 (million)
% 3.86/0.79 % (193923)Instruction limit reached!
% 3.86/0.79 % (193923)------------------------------
% 3.86/0.79 % (193923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.86/0.79 % (193923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/0.79 % (193923)CaDiCaL version: 2.1.3
% 3.86/0.79 % (193923)Termination reason: Instruction limit
% 3.86/0.79 % (193923)Termination phase: Saturation
% 3.86/0.79 % (193923)Time elapsed: 0.053 s
% 3.86/0.79 % (193923)Peak memory usage: 12 MB
% 3.86/0.79 % (193923)Instructions burned: 133 (million)
% 3.86/0.79 % (193956)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3032130314:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 3.86/0.79 % (193956)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.86/0.79 % (193956)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.86/0.79 % (193961)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=597695623:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 3.86/0.79 % (193924)Instruction limit reached!
% 4.34/0.82 % (193924)------------------------------
% 4.34/0.82 % (193924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.34/0.82 % (193924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.34/0.82 % (193924)CaDiCaL version: 2.1.3
% 4.34/0.82 % (193924)Termination reason: Instruction limit
% 4.34/0.82 % (193924)Termination phase: Saturation
% 4.34/0.82 % (193924)Time elapsed: 0.074 s
% 4.34/0.82 % (193924)Peak memory usage: 13 MB
% 4.34/0.82 % (193924)Instructions burned: 159 (million)
% 4.34/0.82 % (193960)ott-21_1_sil=16000:fs=off:random_seed=1870854814:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 4.34/0.82 % (193972)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1925177460:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi)
% 4.34/0.82 % Exception at run slice level
% 4.34/0.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.34/0.82 % (193944)Instruction limit reached!
% 4.34/0.82 % (193944)------------------------------
% 4.34/0.82 % (193944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.34/0.82 % (193944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.34/0.82 % (193944)CaDiCaL version: 2.1.3
% 4.34/0.82 % (193944)Termination reason: Instruction limit
% 4.34/0.82 % (193944)Termination phase: Saturation
% 4.34/0.82 % (193944)Time elapsed: 0.060 s
% 4.34/0.82 % (193944)Peak memory usage: 13 MB
% 4.34/0.82 % (193944)Instructions burned: 133 (million)
% 4.34/0.82 % (193980)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=943048033:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 4.34/0.82 % Exception at run slice level
% 4.34/0.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.34/0.82 % (193978)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3017947019:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 4.34/0.82 % (193988)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3333233883:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 4.34/0.82 % (193988)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.34/0.82 % (193960)Instruction limit reached!
% 4.34/0.82 % (193960)------------------------------
% 4.34/0.82 % (193960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.34/0.82 % (193960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.34/0.82 % (193960)CaDiCaL version: 2.1.3
% 4.34/0.82 % (193960)Termination reason: Instruction limit
% 4.34/0.82 % (193960)Termination phase: Saturation
% 4.34/0.82 % (193960)Time elapsed: 0.081 s
% 4.34/0.82 % (193960)Peak memory usage: 12 MB
% 4.34/0.82 % (193960)Instructions burned: 182 (million)
% 4.34/0.82 % (194012)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3835807589:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 4.34/0.82 % (194012)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.34/0.82 % (193961)Instruction limit reached!
% 4.34/0.82 % (193961)------------------------------
% 4.34/0.82 % (193961)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.34/0.82 % (193961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.34/0.82 % (193961)CaDiCaL version: 2.1.3
% 4.34/0.82 % (193961)Termination reason: Instruction limit
% 4.34/0.82 % (193961)Termination phase: Saturation
% 4.34/0.82 % (193961)Time elapsed: 0.211 s
% 4.34/0.82 % (193961)Peak memory usage: 13 MB
% 4.34/0.82 % (193961)Instructions burned: 479 (million)
% 4.34/0.82 % (194039)fmb+10_1_sil=64000:random_seed=1473363134:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 4.34/0.82 % (194039)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 4.34/0.82 % Exception at run slice level
% 4.34/0.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.34/0.82 % (194045)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3548419146:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi)
% 4.34/0.82 % Exception at run slice level
% 4.34/0.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.34/0.82 % (194051)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2772983176:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi)
% 4.34/0.82 % Exception at run slice level
% 4.34/0.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.34/0.82 % (193956)Instruction limit reached!
% 4.34/0.82 % (193956)------------------------------
% 4.34/0.82 % (193956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.34/0.82 % (193956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.34/0.82 % (193956)CaDiCaL version: 2.1.3
% 4.34/0.82 % (193956)Termination reason: Instruction limit
% 4.34/0.82 % (193956)Termination phase: Saturation
% 4.34/0.82 % (193956)Time elapsed: 0.283 s
% 4.34/0.82 % (193956)Peak memory usage: 14 MB
% 4.34/0.82 % (193956)Instructions burned: 684 (million)
% 4.34/0.82 % (194056)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2073900849:i=5131_2996 on theBenchmark for (2996ds/5131Mi)
% 4.34/0.82 % (194056)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.34/0.82 % (194058)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1556022208:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi)
% 4.34/0.82 % (194058)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 4.34/0.82 % (194058)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.34/0.82 % (193988)Instruction limit reached!
% 4.34/0.82 % (193988)------------------------------
% 4.34/0.82 % (193988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.34/0.82 % (193988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.34/0.82 % (193988)CaDiCaL version: 2.1.3
% 4.34/0.82 % (193988)Termination reason: Instruction limit
% 4.34/0.82 % (193988)Termination phase: Saturation
% 4.34/0.82 % (193988)Time elapsed: 0.257 s
% 4.34/0.82 % (193988)Peak memory usage: 16 MB
% 4.34/0.82 % (193988)Instructions burned: 692 (million)
% 4.34/0.82 % (194064)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1524485918:i=6324_2996 on theBenchmark for (2996ds/6324Mi)
% 4.34/0.82 % Exception at run slice level
% 4.34/0.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.34/0.82 % (194069)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2868171046:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi)
% 4.34/0.82 % Exception at run slice level
% 4.34/0.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.34/0.82 % (194074)ott-2_1_sil=16000:newcnf=on:random_seed=1861274199:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2995 on theBenchmark for (2995ds/869Mi)
% 4.34/0.82 % (194074)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.34/0.82 % (194012)Instruction limit reached!
% 4.34/0.82 % (194012)------------------------------
% 4.34/0.82 % (194012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.34/0.82 % (194012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.34/0.82 % (194012)CaDiCaL version: 2.1.3
% 4.34/0.82 % (194012)Termination reason: Instruction limit
% 4.34/0.82 % (194012)Termination phase: Saturation
% 4.34/0.82 % (194012)Time elapsed: 0.358 s
% 4.34/0.82 % (194012)Peak memory usage: 15 MB
% 4.34/0.82 % (194012)Instructions burned: 880 (million)
% 4.34/0.82 % (194094)ott+10_1_sil=32000:tgt=ground:random_seed=17016174:i=5114:av=off_2994 on theBenchmark for (2994ds/5114Mi)
% 4.34/0.82 % (193978)Instruction limit reached!
% 4.34/0.82 % (193978)------------------------------
% 4.34/0.82 % (193978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.34/0.82 % (193978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.34/0.82 % (193978)CaDiCaL version: 2.1.3
% 4.34/0.82 % (193978)Termination reason: Instruction limit
% 4.34/0.82 % (193978)Termination phase: Saturation
% 4.34/0.82 % (193978)Time elapsed: 0.498 s
% 4.34/0.82 % (193978)Peak memory usage: 17 MB
% 4.34/0.82 % (193978)Instructions burned: 1179 (million)
% 4.34/0.82 % (194104)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2276323304:i=54282_2993 on theBenchmark for (2993ds/54282Mi)
% 4.34/0.82 % Exception at run slice level
% 4.34/0.82 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.34/0.82 % (194108)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1250296823:i=3512:aac=none_2993 on theBenchmark for (2993ds/3512Mi)
% 4.34/0.82 % (194108)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.34/0.82 % (194056) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-193905-194056"...
% 4.34/0.82 % (194056)...printing done.
% 4.34/0.82 % (194056)Refutation found. Thanks to Tanya!
% 4.34/0.82 % SZS status Theorem for theBenchmark
% 4.34/0.82 % SZS output start Proof for theBenchmark
% 4.34/0.82 thf(type_def_5, type, a: $tType).
% 4.34/0.82 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 4.34/0.82 thf(func_def_3, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 4.34/0.82 thf(func_def_4, type, vOR: ($o > $o > $o)).
% 4.34/0.82 thf(func_def_5, type, db0: !>[X0: $tType]:(X0)).
% 4.34/0.82 thf(func_def_6, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 4.34/0.82 thf(func_def_7, type, sK0: (a > $o)).
% 4.34/0.82 thf(func_def_8, type, sK1: a).
% 4.34/0.82 thf(func_def_9, type, sK2: ((a > $o) > $o)).
% 4.34/0.82 thf(func_def_10, type, sK3: (((a > $o) > $o) > a > $o)).
% 4.34/0.82 thf(func_def_11, type, sK4: (((a > $o) > $o) > a)).
% 4.34/0.82 thf(func_def_12, type, vNOT: ($o > $o)).
% 4.34/0.82 thf(func_def_13, type, db1: !>[X0: $tType]:(X0)).
% 4.34/0.82 thf(func_def_15, type, sK6: ((a > a) > a)).
% 4.34/0.82 thf(func_def_16, type, sK7: a).
% 4.34/0.82 thf(func_def_17, type, db2: !>[X0: $tType]:(X0)).
% 4.34/0.82 thf(func_def_18, type, sK8: a).
% 4.34/0.82 thf(func_def_19, type, sK9: a).
% 4.34/0.82 thf(func_def_20, type, sK10: a).
% 4.34/0.82 thf(func_def_21, type, db3: !>[X0: $tType]:(X0)).
% 4.34/0.82 thf(func_def_22, type, sK11: (((a > $o) > a > $o) > (a > a) > a)).
% 4.34/0.82 thf(func_def_23, type, sK12: (((a > $o) > $o) > a)).
% 4.34/0.82 thf(func_def_24, type, sK13: (((a > $o) > $o) > a > $o)).
% 4.34/0.82 thf(func_def_25, type, sK14: ((a > (a > $o) > $o) > a)).
% 4.34/0.82 thf(func_def_26, type, sK15: (((a > $o) > a > a) > a)).
% 4.34/0.82 thf(func_def_27, type, sK16: ((a > a) > a)).
% 4.34/0.82 thf(func_def_28, type, sK17: (((a > $o) > a > $o) > ((a > $o) > a > $o) > a)).
% 4.34/0.82 thf(func_def_29, type, sK18: a).
% 4.34/0.82 thf(func_def_30, type, sK19: (((a > $o) > a > a) > a)).
% 4.34/0.82 thf(func_def_31, type, sK20: a).
% 4.34/0.82 thf(func_def_32, type, sK21: (a > ((a > $o) > a > $o) > a)).
% 4.34/0.82 thf(func_def_33, type, sK22: (((a > $o) > a > a) > ((a > $o) > a > a) > a)).
% 4.34/0.82 thf(func_def_34, type, sK23: (((a > $o) > a > $o) > a > ((a > $o) > a > $o) > a)).
% 4.34/0.82 thf(func_def_35, type, sK24: ((a > (a > $o) > $o) > a > $o)).
% 4.34/0.82 thf(func_def_36, type, sK25: ((a > a) > a)).
% 4.34/0.82 thf(func_def_37, type, sK26: (((a > $o) > a > a) > a > a)).
% 4.34/0.82 thf(func_def_38, type, sK27: (((a > $o) > a > (a > $o) > $o) > ((a > $o) > a > a) > a)).
% 4.34/0.82 thf(func_def_39, type, db4: !>[X0: $tType]:(X0)).
% 4.34/0.82 thf(func_def_40, type, db5: !>[X0: $tType]:(X0)).
% 4.34/0.82 thf(func_def_41, type, sK28: (((a > $o) > a > a) > ((a > $o) > a > (a > $o) > $o) > ((a > $o) > a > a) > a)).
% 4.34/0.82 thf(func_def_42, type, sK29: (((a > $o) > $o) > ((a > $o) > a > a) > a)).
% 4.34/0.82 thf(func_def_43, type, sK30: (((a > $o) > a > a) > a)).
% 4.34/0.82 thf(func_def_44, type, sK31: (((a > $o) > a > a) > ((a > $o) > a > a) > a)).
% 4.34/0.82 thf(func_def_45, type, sK32: (a > ((a > $o) > a > $o) > a)).
% 4.34/0.82 thf(func_def_46, type, sK33: (((a > $o) > a > $o) > ((a > $o) > a > $o) > a > a)).
% 4.34/0.82 thf(func_def_47, type, sK34: (((a > $o) > a > $o) > ((a > $o) > a > $o) > a)).
% 4.34/0.82 thf(func_def_48, type, sK35: ((a > (a > $o) > $o) > a)).
% 4.34/0.82 thf(func_def_49, type, sK36: (((a > $o) > a > a) > ((a > $o) > a > (a > $o) > $o) > ((a > $o) > a > a) > a)).
% 4.34/0.82 thf(func_def_50, type, sK37: (((a > $o) > a > (a > $o) > $o) > ((a > $o) > a > a) > a)).
% 4.34/0.82 thf(func_def_51, type, sK38: (((a > $o) > a > $o) > ((a > $o) > a > a) > ((a > $o) > a > $o) > a)).
% 4.34/0.82 thf(func_def_52, type, sK39: (((a > $o) > a > $o) > ((a > $o) > a > a) > ((a > $o) > a > $o) > a)).
% 4.34/0.82 thf(func_def_53, type, sK40: (a > (a > $o) > ((a > $o) > a > $o) > a)).
% 4.34/0.82 thf(func_def_54, type, sK41: (((a > $o) > a > a) > a)).
% 4.34/0.82 thf(func_def_55, type, sK42: ((a > a) > a)).
% 4.34/0.82 thf(func_def_56, type, sK43: (((a > $o) > $o) > a)).
% 4.34/0.82 thf(func_def_57, type, sK44: (((a > $o) > $o) > a)).
% 4.34/0.82 thf(func_def_58, type, sK45: (((a > $o) > $o) > a > $o)).
% 4.34/0.82 thf(func_def_59, type, sK46: (((a > $o) > a > a) > a)).
% 4.34/0.82 thf(f1,conjecture,(
% 4.34/0.82 ! [X0 : (a > $o),X1 : a] : (! [X2 : ((a > $o) > $o)] : ((! [X4 : (a > $o),X3 : a] : ((X2 @ X4) => (X2 @ (^[X5 : a] : ((X5 = X3) | (X4 @ X5))))) & (X2 @ (^[X3 : a] : ($false)))) => (X2 @ X0)) => ! [X2 : ((a > $o) > $o)] : ((! [X4 : (a > $o),X3 : a] : ((X2 @ X4) => (X2 @ (^[X5 : a] : ((X5 = X3) | (X4 @ X5))))) & (X2 @ (^[X3 : a] : ($false)))) => (X2 @ (^[X5 : a] : ((X5 = X1) | (X0 @ X5))))))),
% 4.34/0.82 file('/export/starexec/sandbox/benchmark/theBenchmark.p',cTHM164_pme)).
% 4.34/0.82 thf(f2,negated_conjecture,(
% 4.34/0.82 ~ ! [X0 : (a > $o),X1 : a] : (! [X2 : ((a > $o) > $o)] : ((! [X4 : (a > $o),X3 : a] : ((X2 @ X4) => (X2 @ (^[X5 : a] : ((X5 = X3) | (X4 @ X5))))) & (X2 @ (^[X3 : a] : ($false)))) => (X2 @ X0)) => ! [X2 : ((a > $o) > $o)] : ((! [X4 : (a > $o),X3 : a] : ((X2 @ X4) => (X2 @ (^[X5 : a] : ((X5 = X3) | (X4 @ X5))))) & (X2 @ (^[X3 : a] : ($false)))) => (X2 @ (^[X5 : a] : ((X5 = X1) | (X0 @ X5))))))),
% 4.34/0.82 inference(negated_conjecture,[status(cth)],[f1])).
% 4.34/0.82 thf(f3,plain,(
% 4.34/0.82 ~ ! [X0 : (a > $o),X1 : a] : (! [X2 : ((a > $o) > $o)] : ((! [X3 : (a > $o),X4 : a] : ((X2 @ X3) => (X2 @ (^[X5 : a] : ((X4 = X5) | (X3 @ X5))))) & (X2 @ (^[X6 : a] : ($false)))) => (X2 @ X0)) => ! [X7 : ((a > $o) > $o)] : ((! [X8 : (a > $o),X9 : a] : ((X7 @ X8) => (X7 @ (^[X10 : a] : ((X9 = X10) | (X8 @ X10))))) & (X7 @ (^[X11 : a] : ($false)))) => (X7 @ (^[X12 : a] : ((X1 = X12) | (X0 @ X12))))))),
% 4.34/0.82 inference(rectify,[],[f2])).
% 4.34/0.82 thf(f4,plain,(
% 4.34/0.82 ~ ! [X0 : (a > $o),X1 : a] : (! [X2 : ((a > $o) > $o)] : ((! [X3 : (a > $o),X4 : a] : ((((X2 @ X3)) = $true) => ($true = ((X2 @ (^[Y0 : a]: ((X3 @ Y0) | (X4 = Y0))))))) & (((X2 @ (^[Y0 : a]: ($false)))) = $true)) => (((X2 @ X0)) = $true)) => ! [X7 : ((a > $o) > $o)] : ((! [X8 : (a > $o),X9 : a] : ((((X7 @ X8)) = $true) => ($true = ((X7 @ (^[Y0 : a]: ((X8 @ Y0) | (X9 = Y0))))))) & ($true = ((X7 @ (^[Y0 : a]: ($false)))))) => ($true = ((X7 @ (^[Y0 : a]: ((X0 @ Y0) | (X1 = Y0))))))))),
% 4.34/0.82 inference(fool_elimination,[],[f3])).
% 4.34/0.82 thf(f5,plain,(
% 4.34/0.82 ~ ! [X0 : (a > $o),X1 : a] : (! [X2 : ((a > $o) > $o)] : ((! [X3 : (a > $o),X4 : a] : ((((X2 @ X3)) = $true) => ($true = ((X2 @ (^[Y0 : a]: ((X3 @ Y0) | (X4 = Y0))))))) & (((X2 @ (^[Y0 : a]: ($false)))) = $true)) => (((X2 @ X0)) = $true)) => ! [X5 : ((a > $o) > $o)] : ((! [X6 : (a > $o),X7 : a] : (($true = ((X5 @ X6))) => ($true = ((X5 @ (^[Y0 : a]: ((X6 @ Y0) | (X7 = Y0))))))) & ($true = ((X5 @ (^[Y0 : a]: ($false)))))) => ($true = ((X5 @ (^[Y0 : a]: ((X0 @ Y0) | (X1 = Y0))))))))),
% 4.34/0.82 inference(rectify,[],[f4])).
% 4.34/0.82 thf(f6,plain,(
% 4.34/0.82 ? [X0 : (a > $o),X1 : a] : (? [X5 : ((a > $o) > $o)] : (($true != ((X5 @ (^[Y0 : a]: ((X0 @ Y0) | (X1 = Y0)))))) & (! [X6 : (a > $o),X7 : a] : (($true = ((X5 @ (^[Y0 : a]: ((X6 @ Y0) | (X7 = Y0)))))) | ($true != ((X5 @ X6)))) & ($true = ((X5 @ (^[Y0 : a]: ($false))))))) & ! [X2 : ((a > $o) > $o)] : ((((X2 @ X0)) = $true) | (? [X3 : (a > $o),X4 : a] : (($true != ((X2 @ (^[Y0 : a]: ((X3 @ Y0) | (X4 = Y0)))))) & (((X2 @ X3)) = $true)) | (((X2 @ (^[Y0 : a]: ($false)))) != $true))))),
% 4.34/0.82 inference(ennf_transformation,[],[f5])).
% 4.34/0.82 thf(f7,plain,(
% 4.34/0.82 ? [X0 : (a > $o),X1 : a] : (? [X5 : ((a > $o) > $o)] : (($true != ((X5 @ (^[Y0 : a]: ((X0 @ Y0) | (X1 = Y0)))))) & ! [X6 : (a > $o),X7 : a] : (($true = ((X5 @ (^[Y0 : a]: ((X6 @ Y0) | (X7 = Y0)))))) | ($true != ((X5 @ X6)))) & ($true = ((X5 @ (^[Y0 : a]: ($false)))))) & ! [X2 : ((a > $o) > $o)] : ((((X2 @ X0)) = $true) | ? [X3 : (a > $o),X4 : a] : (($true != ((X2 @ (^[Y0 : a]: ((X3 @ Y0) | (X4 = Y0)))))) & (((X2 @ X3)) = $true)) | (((X2 @ (^[Y0 : a]: ($false)))) != $true)))),
% 4.34/0.82 inference(flattening,[],[f6])).
% 4.34/0.82 thf(f8,plain,(
% 4.34/0.82 ? [X0 : (a > $o),X1 : a] : (? [X2 : ((a > $o) > $o)] : (($true != ((X2 @ (^[Y0 : a]: ((X0 @ Y0) | (X1 = Y0)))))) & ! [X3 : (a > $o),X4 : a] : (($true = ((X2 @ (^[Y0 : a]: ((X3 @ Y0) | (X4 = Y0)))))) | (((X2 @ X3)) != $true)) & (((X2 @ (^[Y0 : a]: ($false)))) = $true)) & ! [X5 : ((a > $o) > $o)] : (($true = ((X5 @ X0))) | ? [X6 : (a > $o),X7 : a] : (($true != ((X5 @ (^[Y0 : a]: ((X6 @ Y0) | (X7 = Y0)))))) & ($true = ((X5 @ X6)))) | ($true != ((X5 @ (^[Y0 : a]: ($false)))))))),
% 4.34/0.82 inference(rectify,[],[f7])).
% 4.34/0.82 thf(f9,plain,(
% 4.34/0.82 (($true != ((sK2 @ (^[Y0 : a]: ((sK0 @ Y0) | (sK1 = Y0)))))) & ! [X3 : (a > $o),X4 : a] : (($true = ((sK2 @ (^[Y0 : a]: ((X3 @ Y0) | (X4 = Y0)))))) | ($true != ((sK2 @ X3)))) & ($true = ((sK2 @ (^[Y0 : a]: ($false)))))) & ! [X5 : ((a > $o) > $o)] : (($true = ((X5 @ sK0))) | (($true != ((X5 @ (^[Y0 : a]: ((sK3 @ X5 @ Y0) | ((sK4 @ X5) = Y0)))))) & ($true = ((X5 @ (sK3 @ X5))))) | ($true != ((X5 @ (^[Y0 : a]: ($false))))))),
% 4.34/0.82 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,vAPP,vAPP]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X7,sK4 @ X5),skolemize(X7,sK4 @ X5)],[f8])).
% 4.34/0.82 thf(f10,plain,(
% 4.34/0.82 ( ! [X5 : ((a > $o) > $o)] : (($true != ((X5 @ (^[Y0 : a]: ($false))))) | ($true = ((X5 @ (sK3 @ X5)))) | ($true = ((X5 @ sK0)))) )),
% 4.34/0.82 inference(cnf_transformation,[],[f9])).
% 4.34/0.82 thf(f11,plain,(
% 4.34/0.82 ( ! [X5 : ((a > $o) > $o)] : (($true != ((X5 @ (^[Y0 : a]: ($false))))) | ($true != ((X5 @ (^[Y0 : a]: ((sK3 @ X5 @ Y0) | ((sK4 @ X5) = Y0)))))) | ($true = ((X5 @ sK0)))) )),
% 4.34/0.82 inference(cnf_transformation,[],[f9])).
% 4.34/0.82 thf(f12,plain,(
% 4.34/0.82 ($true = ((sK2 @ (^[Y0 : a]: ($false)))))),
% 4.34/0.82 inference(cnf_transformation,[],[f9])).
% 4.34/0.82 thf(f13,plain,(
% 4.34/0.82 ( ! [X3 : (a > $o),X4 : a] : (($true != ((sK2 @ X3))) | ($true = ((sK2 @ (^[Y0 : a]: ((X3 @ Y0) | (X4 = Y0))))))) )),
% 4.34/0.82 inference(cnf_transformation,[],[f9])).
% 4.34/0.82 thf(f14,plain,(
% 4.34/0.82 ($true != ((sK2 @ (^[Y0 : a]: ((sK0 @ Y0) | (sK1 = Y0))))))),
% 4.34/0.82 inference(cnf_transformation,[],[f9])).
% 4.34/0.82 thf(f16,definition,(
% 4.34/0.82 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 4.34/0.82 introduced(theory,[fool_exhaustiveness_axiom])).
% 4.34/0.82 thf(f21,plain,(
% 4.34/0.82 ( ! [X0 : ((a > $o) > a > a)] : (($true != $true) | ($true = (((^[Y0 : a > $o]: (sK2 @ ((^[Y1 : a > $o]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))) @ (sK3 @ (^[Y0 : a > $o]: (sK2 @ ((^[Y1 : a > $o]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))))))) | ($true = (((^[Y0 : a > $o]: (sK2 @ ((^[Y1 : a > $o]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))) @ sK0)))) )),
% 4.34/0.82 inference(constrained_superposition,[],[f10,f12])).
% 4.34/0.82 thf(f29,plain,(
% 4.34/0.82 ( ! [X0 : ((a > $o) > a > a)] : (($true = (((^[Y0 : a > $o]: (sK2 @ ((^[Y1 : a > $o]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))) @ (sK3 @ (^[Y0 : a > $o]: (sK2 @ ((^[Y1 : a > $o]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))))))) | ($true = (((^[Y0 : a > $o]: (sK2 @ ((^[Y1 : a > $o]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))) @ sK0)))) )),
% 4.34/0.82 inference(trivial_inequality_removal,[],[f21])).
% 4.34/0.82 thf(f30,plain,(
% 4.34/0.82 ( ! [X0 : ((a > $o) > a > a)] : (($true = ((sK2 @ (^[Y0 : a]: (sK3 @ (^[Y1 : a > $o]: (sK2 @ (^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ (X0 @ (sK3 @ (^[Y1 : a > $o]: (sK2 @ (^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2)))))) @ Y0)))))) | ($true = ((sK2 @ (^[Y0 : a]: (sK0 @ (X0 @ sK0 @ Y0))))))) )),
% 4.34/0.82 inference(beta-eta_normalization,[],[f29])).
% 4.34/0.82 thf(f64,plain,(
% 4.34/0.82 ( ! [X0 : (a > $o),X1 : a] : (($true != $true) | ($true = ((sK2 @ (^[Y0 : a]: ((X0 @ Y0) | (X1 = Y0)))))) | ($false = ((sK2 @ X0)))) )),
% 4.34/0.82 inference(constrained_superposition,[],[f13,f16])).
% 4.34/0.82 thf(f66,plain,(
% 4.34/0.82 ( ! [X0 : (a > $o),X1 : a] : (($true = ((sK2 @ (^[Y0 : a]: ((X0 @ Y0) | (X1 = Y0)))))) | ($false = ((sK2 @ X0)))) )),
% 4.34/0.82 inference(trivial_inequality_removal,[],[f64])).
% 4.34/0.82 thf(f86,plain,(
% 4.34/0.82 ( ! [X0 : ((a > $o) > a > a)] : (($true != $true) | ($true != (((^[Y0 : a > $o]: (sK2 @ ((^[Y1 : a > $o]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))) @ (^[Y0 : a]: ((sK3 @ (^[Y1 : a > $o]: (sK2 @ ((^[Y2 : a > $o]: ((^[Y3 : a]: (Y2 @ (X0 @ Y2 @ Y3))))) @ Y1))) @ Y0) | ((sK4 @ (^[Y1 : a > $o]: (sK2 @ ((^[Y2 : a > $o]: ((^[Y3 : a]: (Y2 @ (X0 @ Y2 @ Y3))))) @ Y1)))) = Y0)))))) | ($true = (((^[Y0 : a > $o]: (sK2 @ ((^[Y1 : a > $o]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))) @ sK0)))) )),
% 4.34/0.82 inference(constrained_superposition,[],[f11,f12])).
% 4.34/0.82 thf(f99,plain,(
% 4.34/0.82 ( ! [X0 : ((a > $o) > a > a)] : (($true != (((^[Y0 : a > $o]: (sK2 @ ((^[Y1 : a > $o]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))) @ (^[Y0 : a]: ((sK3 @ (^[Y1 : a > $o]: (sK2 @ ((^[Y2 : a > $o]: ((^[Y3 : a]: (Y2 @ (X0 @ Y2 @ Y3))))) @ Y1))) @ Y0) | ((sK4 @ (^[Y1 : a > $o]: (sK2 @ ((^[Y2 : a > $o]: ((^[Y3 : a]: (Y2 @ (X0 @ Y2 @ Y3))))) @ Y1)))) = Y0)))))) | ($true = (((^[Y0 : a > $o]: (sK2 @ ((^[Y1 : a > $o]: ((^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ Y0))) @ sK0)))) )),
% 4.34/0.82 inference(trivial_inequality_removal,[],[f86])).
% 4.34/0.82 thf(f100,plain,(
% 4.34/0.82 ( ! [X0 : ((a > $o) > a > a)] : (($true != ((sK2 @ (^[Y0 : a]: ((sK3 @ (^[Y1 : a > $o]: (sK2 @ (^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ (X0 @ (^[Y1 : a]: ((sK3 @ (^[Y2 : a > $o]: (sK2 @ (^[Y3 : a]: (Y2 @ (X0 @ Y2 @ Y3))))) @ Y1) | ((sK4 @ (^[Y2 : a > $o]: (sK2 @ (^[Y3 : a]: (Y2 @ (X0 @ Y2 @ Y3)))))) = Y1))) @ Y0)) | ((sK4 @ (^[Y1 : a > $o]: (sK2 @ (^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2)))))) = (X0 @ (^[Y1 : a]: ((sK3 @ (^[Y2 : a > $o]: (sK2 @ (^[Y3 : a]: (Y2 @ (X0 @ Y2 @ Y3))))) @ Y1) | ((sK4 @ (^[Y2 : a > $o]: (sK2 @ (^[Y3 : a]: (Y2 @ (X0 @ Y2 @ Y3)))))) = Y1))) @ Y0))))))) | ($true = ((sK2 @ (^[Y0 : a]: (sK0 @ (X0 @ sK0 @ Y0))))))) )),
% 4.34/0.82 inference(beta-eta_normalization,[],[f99])).
% 4.34/0.82 thf(f191,plain,(
% 4.34/0.82 ( ! [X0 : (a > a)] : (($true != $true) | ($false = ((sK2 @ (^[Y0 : a]: (sK0 @ (X0 @ Y0)))))) | ((^[Y0 : a]: (Y0)) != X0)) )),
% 4.34/0.82 inference(constrained_superposition,[],[f14,f66])).
% 4.34/0.82 thf(f201,plain,(
% 4.34/0.82 ( ! [X0 : (a > a)] : (((^[Y0 : a]: (Y0)) != X0) | ($false = ((sK2 @ (^[Y0 : a]: (sK0 @ (X0 @ Y0))))))) )),
% 4.34/0.82 inference(trivial_inequality_removal,[],[f191])).
% 4.34/0.82 thf(f205,plain,(
% 4.34/0.82 ($false = ((sK2 @ (^[Y0 : a]: (sK0 @ ((^[Y1 : a]: (Y1)) @ Y0))))))),
% 4.34/0.82 inference(equality_resolution,[],[f201])).
% 4.34/0.82 thf(f206,plain,(
% 4.34/0.82 ($false = ((sK2 @ sK0)))),
% 4.34/0.82 inference(beta-eta_normalization,[],[f205])).
% 4.34/0.82 thf(f550,plain,(
% 4.34/0.82 ( ! [X0 : ((a > $o) > a > a),X1 : a] : (($true != $true) | ($true = ((sK2 @ (^[Y0 : a]: (((^[Y1 : a]: (sK3 @ (^[Y2 : a > $o]: (sK2 @ (^[Y3 : a]: (Y2 @ (X0 @ Y2 @ Y3))))) @ (X0 @ (sK3 @ (^[Y2 : a > $o]: (sK2 @ (^[Y3 : a]: (Y2 @ (X0 @ Y2 @ Y3)))))) @ Y1))) @ Y0) | (X1 = Y0)))))) | ($true = ((sK2 @ (^[Y0 : a]: (sK0 @ (X0 @ sK0 @ Y0))))))) )),
% 4.34/0.82 inference(constrained_superposition,[],[f13,f30])).
% 4.34/0.82 thf(f569,plain,(
% 4.34/0.82 ( ! [X0 : ((a > $o) > a > a),X1 : a] : (($true = ((sK2 @ (^[Y0 : a]: (((^[Y1 : a]: (sK3 @ (^[Y2 : a > $o]: (sK2 @ (^[Y3 : a]: (Y2 @ (X0 @ Y2 @ Y3))))) @ (X0 @ (sK3 @ (^[Y2 : a > $o]: (sK2 @ (^[Y3 : a]: (Y2 @ (X0 @ Y2 @ Y3)))))) @ Y1))) @ Y0) | (X1 = Y0)))))) | ($true = ((sK2 @ (^[Y0 : a]: (sK0 @ (X0 @ sK0 @ Y0))))))) )),
% 4.34/0.82 inference(trivial_inequality_removal,[],[f550])).
% 4.34/0.82 thf(f570,plain,(
% 4.34/0.82 ( ! [X0 : ((a > $o) > a > a),X1 : a] : (($true = ((sK2 @ (^[Y0 : a]: ((sK3 @ (^[Y1 : a > $o]: (sK2 @ (^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2))))) @ (X0 @ (sK3 @ (^[Y1 : a > $o]: (sK2 @ (^[Y2 : a]: (Y1 @ (X0 @ Y1 @ Y2)))))) @ Y0)) | (X1 = Y0)))))) | ($true = ((sK2 @ (^[Y0 : a]: (sK0 @ (X0 @ sK0 @ Y0))))))) )),
% 4.34/0.82 inference(beta-eta_normalization,[],[f569])).
% 4.34/0.82 thf(f1482,plain,(
% 4.34/0.82 ( ! [X0 : ((a > $o) > a > a),X1 : ((a > $o) > $o)] : (($true != $true) | ($true = ((sK2 @ (^[Y0 : a]: (sK0 @ ((^[Y1 : a > $o]: ((^[Y2 : a]: (Y2)))) @ sK0 @ Y0)))))) | ($true = ((sK2 @ (^[Y0 : a]: (sK0 @ (X0 @ sK0 @ Y0)))))) | (((X0 @ (sK3 @ (^[Y0 : a > $o]: (sK2 @ (^[Y1 : a]: (Y0 @ (X0 @ Y0 @ Y1)))))))) != (^[Y0 : a]: (Y0))) | ((^[Y0 : a]: (sK2)) != (^[Y0 : a]: (X1))) | ((^[Y0 : a]: ((^[Y1 : a > $o]: ((^[Y2 : a]: (Y2)))))) != (^[Y0 : a]: (X0)))) )),
% 4.34/0.82 inference(constrained_superposition,[],[f100,f570])).
% 4.34/0.82 thf(f1505,plain,(
% 4.34/0.82 ( ! [X0 : ((a > $o) > a > a),X1 : ((a > $o) > $o)] : (($true = ((sK2 @ (^[Y0 : a]: (sK0 @ ((^[Y1 : a > $o]: ((^[Y2 : a]: (Y2)))) @ sK0 @ Y0)))))) | ($true = ((sK2 @ (^[Y0 : a]: (sK0 @ (X0 @ sK0 @ Y0)))))) | (((X0 @ (sK3 @ (^[Y0 : a > $o]: (sK2 @ (^[Y1 : a]: (Y0 @ (X0 @ Y0 @ Y1)))))))) != (^[Y0 : a]: (Y0))) | ((^[Y0 : a]: (sK2)) != (^[Y0 : a]: (X1))) | ((^[Y0 : a]: ((^[Y1 : a > $o]: ((^[Y2 : a]: (Y2)))))) != (^[Y0 : a]: (X0)))) )),
% 4.34/0.82 inference(trivial_inequality_removal,[],[f1482])).
% 4.34/0.82 thf(f1506,plain,(
% 4.34/0.82 ( ! [X0 : ((a > $o) > a > a),X1 : ((a > $o) > $o)] : (($true = ((sK2 @ sK0))) | ($true = ((sK2 @ (^[Y0 : a]: (sK0 @ (X0 @ sK0 @ Y0)))))) | (((X0 @ (sK3 @ (^[Y0 : a > $o]: (sK2 @ (^[Y1 : a]: (Y0 @ (X0 @ Y0 @ Y1)))))))) != (^[Y0 : a]: (Y0))) | ((^[Y0 : a]: (sK2)) != (^[Y0 : a]: (X1))) | ((^[Y0 : a]: ((^[Y1 : a > $o]: ((^[Y2 : a]: (Y2)))))) != (^[Y0 : a]: (X0)))) )),
% 4.34/0.82 inference(beta-eta_normalization,[],[f1505])).
% 4.34/0.82 thf(f1528,plain,(
% 4.34/0.82 ( ! [X0 : ((a > $o) > a > a),X1 : ((a > $o) > $o)] : (($false = $true) | ($true = ((sK2 @ (^[Y0 : a]: (sK0 @ (X0 @ sK0 @ Y0)))))) | (((X0 @ (sK3 @ (^[Y0 : a > $o]: (sK2 @ (^[Y1 : a]: (Y0 @ (X0 @ Y0 @ Y1)))))))) != (^[Y0 : a]: (Y0))) | ((^[Y0 : a]: (sK2)) != (^[Y0 : a]: (X1))) | ((^[Y0 : a]: ((^[Y1 : a > $o]: ((^[Y2 : a]: (Y2)))))) != (^[Y0 : a]: (X0)))) )),
% 4.34/0.82 inference(forward_demodulation,[],[f1506,f206])).
% 4.34/0.82 thf(f1529,plain,(
% 4.34/0.82 ( ! [X0 : ((a > $o) > a > a),X1 : ((a > $o) > $o)] : (($true = ((sK2 @ (^[Y0 : a]: (sK0 @ (X0 @ sK0 @ Y0)))))) | (((X0 @ (sK3 @ (^[Y0 : a > $o]: (sK2 @ (^[Y1 : a]: (Y0 @ (X0 @ Y0 @ Y1)))))))) != (^[Y0 : a]: (Y0))) | ((^[Y0 : a]: (sK2)) != (^[Y0 : a]: (X1))) | ((^[Y0 : a]: ((^[Y1 : a > $o]: ((^[Y2 : a]: (Y2)))))) != (^[Y0 : a]: (X0)))) )),
% 4.34/0.82 inference(trivial_inequality_removal,[],[f1528])).
% 4.34/0.82 thf(f2748,definition,(
% 4.34/0.82 spl5_20 <=> ! [X1 : ((a > $o) > $o)] : ((^[Y0 : a]: (sK2)) != (^[Y0 : a]: (X1)))),
% 4.34/0.82 introduced(definition,[new_symbols(definition,[spl5_20])],[avatar_definition])).
% 4.34/0.82 thf(f2749,plain,(
% 4.34/0.82 ( ! [X1 : ((a > $o) > $o)] : (((^[Y0 : a]: (sK2)) != (^[Y0 : a]: (X1)))) ) | ~spl5_20),
% 4.34/0.82 inference(avatar_component_clause,[],[f2748])).
% 4.34/0.82 thf(f2751,definition,(
% 4.34/0.82 spl5_21 <=> ! [X0 : ((a > $o) > a > a)] : (($true = ((sK2 @ (^[Y0 : a]: (sK0 @ (X0 @ sK0 @ Y0)))))) | ((^[Y0 : a]: ((^[Y1 : a > $o]: ((^[Y2 : a]: (Y2)))))) != (^[Y0 : a]: (X0))) | (((X0 @ (sK3 @ (^[Y0 : a > $o]: (sK2 @ (^[Y1 : a]: (Y0 @ (X0 @ Y0 @ Y1)))))))) != (^[Y0 : a]: (Y0))))),
% 4.34/0.82 introduced(definition,[new_symbols(definition,[spl5_21])],[avatar_definition])).
% 4.34/0.82 thf(f2752,plain,(
% 4.34/0.82 ( ! [X0 : ((a > $o) > a > a)] : (((^[Y0 : a]: ((^[Y1 : a > $o]: ((^[Y2 : a]: (Y2)))))) != (^[Y0 : a]: (X0))) | ($true = ((sK2 @ (^[Y0 : a]: (sK0 @ (X0 @ sK0 @ Y0)))))) | (((X0 @ (sK3 @ (^[Y0 : a > $o]: (sK2 @ (^[Y1 : a]: (Y0 @ (X0 @ Y0 @ Y1)))))))) != (^[Y0 : a]: (Y0)))) ) | ~spl5_21),
% 4.34/0.82 inference(avatar_component_clause,[],[f2751])).
% 4.34/0.82 thf(f2753,plain,(
% 4.34/0.82 spl5_20 | spl5_21),
% 4.34/0.82 inference(avatar_split_clause,[],[f1529,f2751,f2748])).
% 4.34/0.82 thf(f2754,plain,(
% 4.34/0.82 ( ! [X1 : ((a > $o) > $o)] : (((((^[Y0 : a]: (sK2)) @ (sK44 @ X1))) != (((^[Y0 : a]: (X1)) @ (sK44 @ X1))))) ) | ~spl5_20),
% 4.34/0.82 inference(negative_extensionality,[],[f2749])).
% 4.34/0.82 thf(f2756,plain,(
% 4.34/0.82 ( ! [X1 : ((a > $o) > $o)] : ((sK2 != X1)) ) | ~spl5_20),
% 4.34/0.82 inference(beta-eta_normalization,[],[f2754])).
% 4.34/0.82 thf(f2758,plain,(
% 4.34/0.82 $false | ~spl5_20),
% 4.34/0.82 inference(equality_resolution,[],[f2756])).
% 4.34/0.82 thf(f2759,plain,(
% 4.34/0.82 ~spl5_20),
% 4.34/0.82 inference(avatar_contradiction_clause,[],[f2758])).
% 4.34/0.82 thf(f2763,plain,(
% 4.34/0.82 ($true = ((sK2 @ (^[Y0 : a]: (sK0 @ ((^[Y1 : a > $o]: ((^[Y2 : a]: (Y2)))) @ sK0 @ Y0)))))) | ((^[Y0 : a]: (Y0)) != (((^[Y0 : a > $o]: ((^[Y1 : a]: (Y1)))) @ (sK3 @ (^[Y0 : a > $o]: (sK2 @ (^[Y1 : a]: (Y0 @ ((^[Y2 : a > $o]: ((^[Y3 : a]: (Y3)))) @ Y0 @ Y1))))))))) | ~spl5_21),
% 4.34/0.82 inference(equality_resolution,[],[f2752])).
% 4.34/0.82 thf(f2764,plain,(
% 4.34/0.82 ($true = ((sK2 @ sK0))) | ((^[Y0 : a]: (Y0)) != (^[Y0 : a]: (Y0))) | ~spl5_21),
% 4.34/0.82 inference(beta-eta_normalization,[],[f2763])).
% 4.34/0.82 thf(f2765,plain,(
% 4.34/0.82 ($true = ((sK2 @ sK0))) | ~spl5_21),
% 4.34/0.82 inference(trivial_inequality_removal,[],[f2764])).
% 4.34/0.82 thf(f2767,plain,(
% 4.34/0.82 ($false = $true) | ~spl5_21),
% 4.34/0.82 inference(forward_demodulation,[],[f2765,f206])).
% 4.34/0.82 thf(f2768,plain,(
% 4.34/0.82 $false | ~spl5_21),
% 4.34/0.82 inference(trivial_inequality_removal,[],[f2767])).
% 4.34/0.82 thf(f2769,plain,(
% 4.34/0.82 ~spl5_21),
% 4.34/0.82 inference(avatar_contradiction_clause,[],[f2768])).
% 4.34/0.82 cnf(s14, plain, spl5_20 | spl5_21, inference(sat_conversion,[],[f2753])).
% 4.34/0.82 cnf(s15, plain, ~spl5_20, inference(sat_conversion,[],[f2759])).
% 4.34/0.82 cnf(s16, plain, ~spl5_21, inference(sat_conversion,[],[f2769])).
% 4.34/0.82 cnf(s17, plain, $false, inference(rat,[],[s14,s16,s15])).
% 4.34/0.82 thf(f2770,plain,(
% 4.34/0.82 $false),
% 4.34/0.82 inference(avatar_sat_refutation,[],[s17])).
% 4.34/0.82 % SZS output end Proof for theBenchmark
% 4.34/0.82 % (194056)------------------------------
% 4.34/0.82 % (194056)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.34/0.82 % (194056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.34/0.82 % (194056)CaDiCaL version: 2.1.3
% 4.34/0.82 % (194056)Termination reason: Refutation
% 4.34/0.82 % (194056)Time elapsed: 0.315 s
% 4.34/0.82 % (194056)Peak memory usage: 16 MB
% 4.34/0.82 % (194056)Instructions burned: 786 (million)
% 4.34/0.82 % (193905)Success in time 0.693 s
% 4.34/0.82 % Vampire exiting
%------------------------------------------------------------------------------