%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEV146^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 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 08:39:03 AM UTC 2026
% Result : Theorem 129.82s 18.53s
% Output : Refutation 129.82s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV146^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n009.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 15:16:16 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.90/1.07 % (4121966)Will run a generic schedule for satisfiability detection.
% 5.90/1.07 % (4121977)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4081727273:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.90/1.07 % (4121972)% WARNING: option uhcvi not known.
% 5.90/1.07 % (4121972)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2163971709:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.90/1.07 % (4121973)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3852730234:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.90/1.07 % (4121974)dis+10_1_sil=32000:sp=arity:random_seed=1630031335:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.90/1.07 % (4121975)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3624144777:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.90/1.07 % (4121971)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3867024306_2999 on theBenchmark for (2999ds/0Mi)
% 5.90/1.07 % (4121975)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 5.90/1.07 % (4121972)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 5.90/1.07 % (4121972)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 5.90/1.07 % Exception at run slice level
% 5.90/1.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 5.90/1.07 % (4121976)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1808117576:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.90/1.07 % (4121984)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=281990142:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 5.90/1.07 % Exception at run slice level
% 5.90/1.07 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 5.90/1.07 % (4121977)Instruction limit reached!
% 5.90/1.07 % (4121977)------------------------------
% 5.90/1.07 % (4121977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.90/1.07 % (4121977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.90/1.07 % (4121977)CaDiCaL version: 2.1.3
% 5.90/1.07 % (4121977)Termination reason: Instruction limit
% 5.90/1.07 % (4121977)Termination phase: Saturation
% 5.90/1.07 % (4121977)Time elapsed: 0.045 s
% 5.90/1.07 % (4121977)Peak memory usage: 13 MB
% 5.90/1.07 % (4121977)Instructions burned: 161 (million)
% 5.90/1.07 % (4121987)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3658196550:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 5.90/1.07 % (4121988)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=2088161178:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 5.90/1.07 % (4121988)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 5.90/1.07 % (4121988)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 5.90/1.07 % (4121974)Instruction limit reached!
% 5.90/1.07 % (4121974)------------------------------
% 5.90/1.07 % (4121974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.90/1.07 % (4121974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.90/1.07 % (4121974)CaDiCaL version: 2.1.3
% 5.90/1.07 % (4121974)Termination reason: Instruction limit
% 5.90/1.07 % (4121974)Termination phase: Saturation
% 5.90/1.07 % (4121974)Time elapsed: 0.052 s
% 5.90/1.07 % (4121974)Peak memory usage: 12 MB
% 5.90/1.07 % (4121974)Instructions burned: 104 (million)
% 5.90/1.07 % (4121975)Instruction limit reached!
% 5.90/1.07 % (4121975)------------------------------
% 5.90/1.07 % (4121975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.90/1.07 % (4121975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.90/1.07 % (4121975)CaDiCaL version: 2.1.3
% 5.90/1.07 % (4121975)Termination reason: Instruction limit
% 5.90/1.07 % (4121975)Termination phase: Saturation
% 5.90/1.07 % (4121975)Time elapsed: 0.057 s
% 5.90/1.07 % (4121975)Peak memory usage: 13 MB
% 5.90/1.07 % (4121975)Instructions burned: 116 (million)
% 5.90/1.07 % (4121991)ott-21_1_sil=16000:fs=off:random_seed=4078365997:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 5.90/1.07 % (4121992)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=488146206:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 22.28/3.40 % (4121976)Instruction limit reached!
% 22.28/3.40 % (4121976)------------------------------
% 22.28/3.40 % (4121976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.28/3.40 % (4121976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.28/3.40 % (4121976)CaDiCaL version: 2.1.3
% 22.28/3.40 % (4121976)Termination reason: Instruction limit
% 22.28/3.40 % (4121976)Termination phase: Saturation
% 22.28/3.40 % (4121976)Time elapsed: 0.115 s
% 22.28/3.40 % (4121976)Peak memory usage: 13 MB
% 22.28/3.40 % (4121976)Instructions burned: 131 (million)
% 22.28/3.40 % (4121987)Instruction limit reached!
% 22.28/3.40 % (4121987)------------------------------
% 22.28/3.40 % (4121987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.28/3.40 % (4121987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.28/3.40 % (4121987)CaDiCaL version: 2.1.3
% 22.28/3.40 % (4121987)Termination reason: Instruction limit
% 22.28/3.40 % (4121987)Termination phase: Saturation
% 22.28/3.40 % (4121987)Time elapsed: 0.088 s
% 22.28/3.40 % (4121987)Peak memory usage: 12 MB
% 22.28/3.40 % (4121987)Instructions burned: 132 (million)
% 22.28/3.40 % (4121995)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=891262340:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 22.28/3.40 % Exception at run slice level
% 22.28/3.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.28/3.40 % (4121996)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1076999031:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 22.28/3.40 % (4121998)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1067813798:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 22.28/3.40 % Exception at run slice level
% 22.28/3.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.28/3.40 % (4122001)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=942057080:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 22.28/3.40 % (4122001)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 22.28/3.40 % (4121991)Instruction limit reached!
% 22.28/3.40 % (4121991)------------------------------
% 22.28/3.40 % (4121991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.28/3.40 % (4121991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.28/3.40 % (4121991)CaDiCaL version: 2.1.3
% 22.28/3.40 % (4121991)Termination reason: Instruction limit
% 22.28/3.40 % (4121991)Termination phase: Saturation
% 22.28/3.40 % (4121991)Time elapsed: 0.129 s
% 22.28/3.40 % (4121991)Peak memory usage: 12 MB
% 22.28/3.40 % (4121991)Instructions burned: 181 (million)
% 22.28/3.40 % (4121988)Instruction limit reached!
% 22.28/3.40 % (4121988)------------------------------
% 22.28/3.40 % (4121988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.28/3.40 % (4121988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.28/3.40 % (4121988)CaDiCaL version: 2.1.3
% 22.28/3.40 % (4121988)Termination reason: Instruction limit
% 22.28/3.40 % (4121988)Termination phase: Saturation
% 22.28/3.40 % (4121988)Time elapsed: 0.171 s
% 22.28/3.40 % (4121988)Peak memory usage: 15 MB
% 22.28/3.40 % (4121988)Instructions burned: 687 (million)
% 22.28/3.40 % (4122003)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1897612321:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 22.28/3.40 % (4122003)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 22.28/3.40 % (4122005)fmb+10_1_sil=64000:random_seed=3236529133:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi)
% 22.28/3.40 % (4122005)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 22.28/3.40 % Exception at run slice level
% 22.28/3.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.28/3.40 % (4122007)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2592520960:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi)
% 22.28/3.40 % Exception at run slice level
% 22.28/3.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 44.08/6.58 % (4122009)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3186457696:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi)
% 44.08/6.58 % Exception at run slice level
% 44.08/6.58 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 44.08/6.58 % (4122011)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2871330449:i=5131_2996 on theBenchmark for (2996ds/5131Mi)
% 44.08/6.58 % (4122011)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 44.08/6.58 % (4121992)Instruction limit reached!
% 44.08/6.58 % (4121992)------------------------------
% 44.08/6.58 % (4121992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.08/6.58 % (4121992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.08/6.58 % (4121992)CaDiCaL version: 2.1.3
% 44.08/6.58 % (4121992)Termination reason: Instruction limit
% 44.08/6.58 % (4121992)Termination phase: Saturation
% 44.08/6.58 % (4121992)Time elapsed: 0.243 s
% 44.08/6.58 % (4121992)Peak memory usage: 15 MB
% 44.08/6.58 % (4121992)Instructions burned: 479 (million)
% 44.08/6.58 % (4122013)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3177873976:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi)
% 44.08/6.58 % (4122013)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 44.08/6.58 % (4122013)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 44.08/6.58 % (4122001)Instruction limit reached!
% 44.08/6.58 % (4122001)------------------------------
% 44.08/6.58 % (4122001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.08/6.58 % (4122001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.08/6.58 % (4122001)CaDiCaL version: 2.1.3
% 44.08/6.58 % (4122001)Termination reason: Instruction limit
% 44.08/6.58 % (4122001)Termination phase: Saturation
% 44.08/6.58 % (4122001)Time elapsed: 0.411 s
% 44.08/6.58 % (4122001)Peak memory usage: 17 MB
% 44.08/6.58 % (4122001)Instructions burned: 693 (million)
% 44.08/6.58 % (4122016)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2688561978:i=6324_2993 on theBenchmark for (2993ds/6324Mi)
% 44.08/6.58 % Exception at run slice level
% 44.08/6.58 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 44.08/6.58 % (4122018)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2485306821:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi)
% 44.08/6.58 % Exception at run slice level
% 44.08/6.58 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 44.08/6.58 % (4122020)ott-2_1_sil=16000:newcnf=on:random_seed=1225772047:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi)
% 44.08/6.58 % (4122020)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 44.08/6.58 % (4122003)Instruction limit reached!
% 44.08/6.58 % (4122003)------------------------------
% 44.08/6.58 % (4122003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.08/6.58 % (4122003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.08/6.58 % (4122003)CaDiCaL version: 2.1.3
% 44.08/6.59 % (4122003)Termination reason: Instruction limit
% 44.08/6.59 % (4122003)Termination phase: Saturation
% 44.08/6.59 % (4122003)Time elapsed: 0.568 s
% 44.08/6.59 % (4122003)Peak memory usage: 17 MB
% 44.08/6.59 % (4122003)Instructions burned: 879 (million)
% 44.08/6.59 % (4121996)Instruction limit reached!
% 44.08/6.59 % (4121996)------------------------------
% 44.08/6.59 % (4121996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.08/6.59 % (4121996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.08/6.59 % (4121996)CaDiCaL version: 2.1.3
% 44.08/6.59 % (4121996)Termination reason: Instruction limit
% 44.08/6.59 % (4121996)Termination phase: Saturation
% 44.08/6.59 % (4121996)Time elapsed: 0.636 s
% 44.08/6.59 % (4121996)Peak memory usage: 18 MB
% 44.08/6.59 % (4121996)Instructions burned: 1179 (million)
% 44.08/6.59 % (4122023)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1107895476:i=54282_2991 on theBenchmark for (2991ds/54282Mi)
% 44.08/6.59 % Exception at run slice level
% 44.08/6.59 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 44.08/6.59 % (4122022)ott+10_1_sil=32000:tgt=ground:random_seed=3781408326:i=5114:av=off_2991 on theBenchmark for (2991ds/5114Mi)
% 129.82/18.53 % (4122026)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2623205244:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi)
% 129.82/18.53 % (4122026)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 129.82/18.53 % (4122013)Instruction limit reached!
% 129.82/18.53 % (4122013)------------------------------
% 129.82/18.53 % (4122013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 129.82/18.53 % (4122013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.82/18.53 % (4122013)CaDiCaL version: 2.1.3
% 129.82/18.53 % (4122013)Termination reason: Instruction limit
% 129.82/18.53 % (4122013)Termination phase: Saturation
% 129.82/18.53 % (4122013)Time elapsed: 0.795 s
% 129.82/18.53 % (4122013)Peak memory usage: 19 MB
% 129.82/18.53 % (4122013)Instructions burned: 1472 (million)
% 129.82/18.53 % (4122031)dis+21_1_sil=32000:sas=cadical:random_seed=4278335205:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi)
% 129.82/18.53 % (4122020)Instruction limit reached!
% 129.82/18.53 % (4122020)------------------------------
% 129.82/18.53 % (4122020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 129.82/18.53 % (4122020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.82/18.53 % (4122020)CaDiCaL version: 2.1.3
% 129.82/18.53 % (4122020)Termination reason: Instruction limit
% 129.82/18.53 % (4122020)Termination phase: Saturation
% 129.82/18.53 % (4122020)Time elapsed: 0.516 s
% 129.82/18.53 % (4122020)Peak memory usage: 27 MB
% 129.82/18.53 % (4122020)Instructions burned: 870 (million)
% 129.82/18.53 % (4122036)ott+11_1_sil=16000:gs=on:random_seed=3229261357:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi)
% 129.82/18.53 % (4122036)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 129.82/18.53 % (4122011)Instruction limit reached!
% 129.82/18.53 % (4122011)------------------------------
% 129.82/18.53 % (4122011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 129.82/18.53 % (4122011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.82/18.53 % (4122011)CaDiCaL version: 2.1.3
% 129.82/18.53 % (4122011)Termination reason: Instruction limit
% 129.82/18.53 % (4122011)Termination phase: Saturation
% 129.82/18.53 % (4122011)Time elapsed: 1.542 s
% 129.82/18.53 % (4122011)Peak memory usage: 28 MB
% 129.82/18.53 % (4122011)Instructions burned: 5134 (million)
% 129.82/18.53 % (4122045)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1375124722:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi)
% 129.82/18.53 % Exception at run slice level
% 129.82/18.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 129.82/18.53 % (4122047)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3653864011:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi)
% 129.82/18.53 % (4122036)Instruction limit reached!
% 129.82/18.53 % (4122036)------------------------------
% 129.82/18.53 % (4122036)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 129.82/18.53 % (4122036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.82/18.53 % (4122036)CaDiCaL version: 2.1.3
% 129.82/18.53 % (4122036)Termination reason: Instruction limit
% 129.82/18.53 % (4122036)Termination phase: Saturation
% 129.82/18.53 % (4122036)Time elapsed: 1.671 s
% 129.82/18.53 % (4122036)Peak memory usage: 24 MB
% 129.82/18.53 % (4122036)Instructions burned: 2252 (million)
% 129.82/18.53 % (4122049)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3300150363:i=29340_2970 on theBenchmark for (2970ds/29340Mi)
% 129.82/18.53 % (4122031)Instruction limit reached!
% 129.82/18.53 % (4122031)------------------------------
% 129.82/18.53 % (4122031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 129.82/18.53 % (4122031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.82/18.53 % (4122031)CaDiCaL version: 2.1.3
% 129.82/18.53 % (4122031)Termination reason: Instruction limit
% 129.82/18.53 % (4122031)Termination phase: Saturation
% 129.82/18.53 % (4122031)Time elapsed: 1.954 s
% 129.82/18.53 % (4122031)Peak memory usage: 24 MB
% 129.82/18.53 % (4122031)Instructions burned: 3775 (million)
% 129.82/18.53 % (4122051)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2026198275:i=5211_2968 on theBenchmark for (2968ds/5211Mi)
% 129.82/18.53 % (4122026)Instruction limit reached!
% 129.82/18.53 % (4122026)------------------------------
% 129.82/18.53 % (4122026)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 129.82/18.53 % (4122026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.82/18.53 % (4122026)CaDiCaL version: 2.1.3
% 129.82/18.53 % (4122026)Termination reason: Instruction limit
% 129.82/18.53 % (4122026)Termination phase: Saturation
% 129.82/18.53 % (4122026)Time elapsed: 2.504 s
% 129.82/18.53 % (4122026)Peak memory usage: 24 MB
% 129.82/18.53 % (4122026)Instructions burned: 3512 (million)
% 129.82/18.53 % (4122053)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3266469627:i=5497:nm=2_2966 on theBenchmark for (2966ds/5497Mi)
% 129.82/18.53 % Exception at run slice level
% 129.82/18.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 129.82/18.53 % (4122055)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2541152900:fmbsr=2:i=46332_2965 on theBenchmark for (2965ds/46332Mi)
% 129.82/18.53 % Exception at run slice level
% 129.82/18.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 129.82/18.53 % (4122057)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1074970683:i=14071_2965 on theBenchmark for (2965ds/14071Mi)
% 129.82/18.53 % Exception at run slice level
% 129.82/18.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 129.82/18.53 % (4122059)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2401680660:i=22565:add=on:rawr=on_2965 on theBenchmark for (2965ds/22565Mi)
% 129.82/18.53 % (4122047)Instruction limit reached!
% 129.82/18.53 % (4122047)------------------------------
% 129.82/18.53 % (4122047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 129.82/18.53 % (4122047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.82/18.53 % (4122047)CaDiCaL version: 2.1.3
% 129.82/18.53 % (4122047)Termination reason: Instruction limit
% 129.82/18.53 % (4122047)Termination phase: Saturation
% 129.82/18.53 % (4122047)Time elapsed: 1.652 s
% 129.82/18.53 % (4122047)Peak memory usage: 26 MB
% 129.82/18.53 % (4122047)Instructions burned: 4591 (million)
% 129.82/18.53 % (4122061)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1187309096:i=8173:av=off_2964 on theBenchmark for (2964ds/8173Mi)
% 129.82/18.53 % (4122022)Instruction limit reached!
% 129.82/18.53 % (4122022)------------------------------
% 129.82/18.53 % (4122022)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 129.82/18.53 % (4122022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.82/18.53 % (4122022)CaDiCaL version: 2.1.3
% 129.82/18.53 % (4122022)Termination reason: Instruction limit
% 129.82/18.53 % (4122022)Termination phase: Saturation
% 129.82/18.53 % (4122022)Time elapsed: 3.374 s
% 129.82/18.53 % (4122022)Peak memory usage: 30 MB
% 129.82/18.53 % (4122022)Instructions burned: 5115 (million)
% 129.82/18.53 % (4122063)dis+10_16:1_sil=16000:random_seed=705504878:i=9155:fsr=off_2957 on theBenchmark for (2957ds/9155Mi)
% 129.82/18.53 % (4122051)Instruction limit reached!
% 129.82/18.53 % (4122051)------------------------------
% 129.82/18.53 % (4122051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 129.82/18.53 % (4122051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.82/18.53 % (4122051)CaDiCaL version: 2.1.3
% 129.82/18.53 % (4122051)Termination reason: Instruction limit
% 129.82/18.53 % (4122051)Termination phase: Saturation
% 129.82/18.53 % (4122051)Time elapsed: 2.604 s
% 129.82/18.53 % (4122051)Peak memory usage: 31 MB
% 129.82/18.53 % (4122051)Instructions burned: 5212 (million)
% 129.82/18.53 % (4122070)ott-3_8_sil=64000:random_seed=2162336722:i=20139:bs=on_2942 on theBenchmark for (2942ds/20139Mi)
% 129.82/18.53 % (4122061)Instruction limit reached!
% 129.82/18.53 % (4122061)------------------------------
% 129.82/18.53 % (4122061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 129.82/18.53 % (4122061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.82/18.53 % (4122061)CaDiCaL version: 2.1.3
% 129.82/18.53 % (4122061)Termination reason: Instruction limit
% 129.82/18.53 % (4122061)Termination phase: Saturation
% 129.82/18.53 % (4122061)Time elapsed: 2.769 s
% 129.82/18.53 % (4122061)Peak memory usage: 41 MB
% 129.82/18.53 % (4122061)Instructions burned: 8175 (million)
% 129.82/18.53 % (4122072)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=890169384:fmbsr=2:i=32576_2936 on theBenchmark for (2936ds/32576Mi)
% 129.82/18.53 % Exception at run slice level
% 129.82/18.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 129.82/18.53 % (4122074)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2920830728:i=11404_2936 on theBenchmark for (2936ds/11404Mi)
% 129.82/18.53 % (4122074)Instruction limit reached!
% 129.82/18.53 % (4122074)------------------------------
% 129.82/18.53 % (4122074)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 129.82/18.53 % (4122074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.82/18.53 % (4122074)CaDiCaL version: 2.1.3
% 129.82/18.53 % (4122074)Termination reason: Instruction limit
% 129.82/18.53 % (4122074)Termination phase: Saturation
% 129.82/18.53 % (4122074)Time elapsed: 4.091 s
% 129.82/18.53 % (4122074)Peak memory usage: 62 MB
% 129.82/18.53 % (4122074)Instructions burned: 11404 (million)
% 129.82/18.53 % (4122079)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3080460601:i=14134_2895 on theBenchmark for (2895ds/14134Mi)
% 129.82/18.53 % (4122079)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 129.82/18.53 % (4122063)Instruction limit reached!
% 129.82/18.53 % (4122063)------------------------------
% 129.82/18.53 % (4122063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 129.82/18.53 % (4122063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.82/18.53 % (4122063)CaDiCaL version: 2.1.3
% 129.82/18.53 % (4122063)Termination reason: Instruction limit
% 129.82/18.53 % (4122063)Termination phase: Saturation
% 129.82/18.53 % (4122063)Time elapsed: 6.612 s
% 129.82/18.53 % (4122063)Peak memory usage: 37 MB
% 129.82/18.53 % (4122063)Instructions burned: 9155 (million)
% 129.82/18.53 % (4122081)dis+33_16_sil=32000:sac=on:random_seed=1992823523:i=15851:nm=0_2891 on theBenchmark for (2891ds/15851Mi)
% 129.82/18.53 % (4122079)Instruction limit reached!
% 129.82/18.53 % (4122079)------------------------------
% 129.82/18.53 % (4122079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 129.82/18.53 % (4122079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.82/18.53 % (4122079)CaDiCaL version: 2.1.3
% 129.82/18.53 % (4122079)Termination reason: Instruction limit
% 129.82/18.53 % (4122079)Termination phase: Saturation
% 129.82/18.53 % (4122079)Time elapsed: 4.605 s
% 129.82/18.53 % (4122079)Peak memory usage: 59 MB
% 129.82/18.53 % (4122079)Instructions burned: 14136 (million)
% 129.82/18.53 % (4122091)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=599684484:avsq=on:i=17627:add=on:amm=off_2848 on theBenchmark for (2848ds/17627Mi)
% 129.82/18.53 % (4122070)Instruction limit reached!
% 129.82/18.53 % (4122070)------------------------------
% 129.82/18.53 % (4122070)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 129.82/18.53 % (4122070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.82/18.53 % (4122070)CaDiCaL version: 2.1.3
% 129.82/18.53 % (4122070)Termination reason: Instruction limit
% 129.82/18.53 % (4122070)Termination phase: Saturation
% 129.82/18.53 % (4122070)Time elapsed: 10.530 s
% 129.82/18.53 % (4122070)Peak memory usage: 41 MB
% 129.82/18.53 % (4122070)Instructions burned: 20141 (million)
% 129.82/18.53 % (4122096)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=4221927661:s2a=on:i=53295_2836 on theBenchmark for (2836ds/53295Mi)
% 129.82/18.53 % (4122081) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-4121966-4122081"...
% 129.82/18.53 % (4122081)...printing done.
% 129.82/18.53 % (4122081)Refutation found. Thanks to Tanya!
% 129.82/18.53 % SZS status Theorem for theBenchmark
% 129.82/18.53 % SZS output start Proof for theBenchmark
% 129.82/18.53 thf(type_def_5, type, a: $tType).
% 129.82/18.53 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 129.82/18.53 thf(func_def_3, type, sK0: (a > a > $o)).
% 129.82/18.53 thf(func_def_4, type, sK1: a).
% 129.82/18.53 thf(func_def_5, type, sK2: a).
% 129.82/18.53 thf(func_def_6, type, sK3: a).
% 129.82/18.53 thf(func_def_7, type, sK4: (a > $o)).
% 129.82/18.53 thf(func_def_8, type, sK5: ((a > $o) > a)).
% 129.82/18.53 thf(func_def_9, type, sK6: ((a > $o) > a)).
% 129.82/18.53 thf(func_def_10, type, sK7: ((a > $o) > a)).
% 129.82/18.53 thf(func_def_11, type, sK8: ((a > $o) > a)).
% 129.82/18.53 thf(func_def_12, type, sK9: ((a > $o) > a)).
% 129.82/18.53 thf(func_def_13, type, sK10: ((a > $o) > a)).
% 129.82/18.53 thf(func_def_14, type, sK11: a).
% 129.82/18.53 thf(func_def_15, type, sK12: a).
% 129.82/18.53 thf(func_def_16, type, sK13: (a > $o)).
% 129.82/18.53 thf(func_def_17, type, vNOT: ($o > $o)).
% 129.82/18.53 thf(func_def_19, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 129.82/18.53 thf(func_def_20, type, db0: !>[X0: $tType]:(X0)).
% 129.82/18.53 thf(func_def_21, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 129.82/18.53 thf(func_def_22, type, db1: !>[X0: $tType]:(X0)).
% 129.82/18.53 thf(func_def_23, type, sK15: ((a > $o) > a)).
% 129.82/18.53 thf(func_def_24, type, sK16: ((a > $o) > a)).
% 129.82/18.53 thf(func_def_25, type, sK17: ((a > $o) > a)).
% 129.82/18.53 thf(func_def_26, type, sK18: ((a > a > $o) > a)).
% 129.82/18.53 thf(func_def_27, type, sK19: ((a > a > $o) > a)).
% 129.82/18.53 thf(func_def_28, type, sK20: ((a > a > $o) > a)).
% 129.82/18.53 thf(func_def_29, type, sK21: ((a > a > $o) > a)).
% 129.82/18.53 thf(func_def_30, type, sK22: ((a > a > a) > a)).
% 129.82/18.53 thf(func_def_31, type, sK23: ((a > a > $o) > a)).
% 129.82/18.53 thf(func_def_32, type, sK24: ((a > a > $o) > a)).
% 129.82/18.53 thf(func_def_33, type, sK25: ((a > a > $o) > a)).
% 129.82/18.53 thf(func_def_34, type, sK26: ((a > a > $o) > a)).
% 129.82/18.53 thf(func_def_35, type, sK27: ((a > a > $o) > a)).
% 129.82/18.53 thf(func_def_36, type, sK28: ((a > $o) > a)).
% 129.82/18.53 thf(func_def_37, type, sK29: ((a > $o) > a)).
% 129.82/18.53 thf(func_def_38, type, sK30: ((a > $o) > a)).
% 129.82/18.53 thf(func_def_39, type, sK31: a).
% 129.82/18.53 thf(func_def_40, type, sK32: a).
% 129.82/18.53 thf(func_def_41, type, sK33: ((a > a > $o) > a)).
% 129.82/18.53 thf(func_def_42, type, sK34: ((a > a > $o) > a)).
% 129.82/18.53 thf(func_def_43, type, sK35: ((a > a > $o) > a)).
% 129.82/18.53 thf(func_def_44, type, sK36: ((a > a > $o) > a)).
% 129.82/18.53 thf(func_def_45, type, sK37: ((a > a > $o) > a)).
% 129.82/18.53 thf(func_def_46, type, sK38: ((a > a > $o) > a)).
% 129.82/18.53 thf(func_def_47, type, sK39: ((a > $o) > a)).
% 129.82/18.53 thf(func_def_48, type, sK40: ((a > $o) > a)).
% 129.82/18.53 thf(func_def_49, type, sK41: ((a > a > $o) > a)).
% 129.82/18.53 thf(func_def_50, type, sK42: ((a > a > $o) > a)).
% 129.82/18.53 thf(func_def_51, type, sK43: ((a > a > $o) > a)).
% 129.82/18.53 thf(func_def_52, type, sK44: ((a > a > $o) > a)).
% 129.82/18.53 thf(func_def_53, type, sK45: ((a > a > $o) > a)).
% 129.82/18.53 thf(func_def_54, type, sK46: ((a > a > $o) > a)).
% 129.82/18.53 thf(func_def_55, type, sK47: ((a > a > $o) > a)).
% 129.82/18.53 thf(func_def_56, type, sK48: ((a > a > $o) > a)).
% 129.82/18.53 thf(func_def_57, type, sK49: ((a > $o) > a)).
% 129.82/18.53 thf(func_def_58, type, sK50: ((a > $o) > a)).
% 129.82/18.53 thf(func_def_59, type, sK51: ((a > $o) > a)).
% 129.82/18.53 thf(func_def_60, type, sK52: ((a > $o) > a)).
% 129.82/18.53 thf(func_def_61, type, sK53: ((a > $o) > a)).
% 129.82/18.53 thf(f1,conjecture,(
% 129.82/18.53 ! [X0 : (a > a > $o)] : (! [X1 : a,X2 : a,X6 : a] : ((! [X3 : (a > $o)] : ((! [X5 : a,X4 : a] : (((X0 @ X5 @ X4) & (X3 @ X5)) => (X3 @ X4)) & ! [X4 : a] : ((X0 @ X2 @ X4) => (X3 @ X4))) => (X3 @ X6)) & ! [X3 : (a > $o)] : ((! [X5 : a,X4 : a] : (((X0 @ X5 @ X4) & (X3 @ X5)) => (X3 @ X4)) & ! [X4 : a] : ((X0 @ X1 @ X4) => (X3 @ X4))) => (X3 @ X2))) => ! [X3 : (a > $o)] : ((! [X5 : a,X4 : a] : (((X0 @ X5 @ X4) & (X3 @ X5)) => (X3 @ X4)) & ! [X4 : a] : ((X0 @ X1 @ X4) => (X3 @ X4))) => (X3 @ X6))) & ! [X1 : a,X2 : a] : ((X0 @ X1 @ X2) => ! [X3 : (a > $o)] : ((! [X5 : a,X4 : a] : (((X0 @ X5 @ X4) & (X3 @ X5)) => (X3 @ X4)) & ! [X4 : a] : ((X0 @ X1 @ X4) => (X3 @ X4))) => (X3 @ X2))))),
% 129.82/18.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cTHM525_pme)).
% 129.82/18.53 thf(f2,negated_conjecture,(
% 129.82/18.53 ~ ! [X0 : (a > a > $o)] : (! [X1 : a,X2 : a,X6 : a] : ((! [X3 : (a > $o)] : ((! [X5 : a,X4 : a] : (((X0 @ X5 @ X4) & (X3 @ X5)) => (X3 @ X4)) & ! [X4 : a] : ((X0 @ X2 @ X4) => (X3 @ X4))) => (X3 @ X6)) & ! [X3 : (a > $o)] : ((! [X5 : a,X4 : a] : (((X0 @ X5 @ X4) & (X3 @ X5)) => (X3 @ X4)) & ! [X4 : a] : ((X0 @ X1 @ X4) => (X3 @ X4))) => (X3 @ X2))) => ! [X3 : (a > $o)] : ((! [X5 : a,X4 : a] : (((X0 @ X5 @ X4) & (X3 @ X5)) => (X3 @ X4)) & ! [X4 : a] : ((X0 @ X1 @ X4) => (X3 @ X4))) => (X3 @ X6))) & ! [X1 : a,X2 : a] : ((X0 @ X1 @ X2) => ! [X3 : (a > $o)] : ((! [X5 : a,X4 : a] : (((X0 @ X5 @ X4) & (X3 @ X5)) => (X3 @ X4)) & ! [X4 : a] : ((X0 @ X1 @ X4) => (X3 @ X4))) => (X3 @ X2))))),
% 129.82/18.53 inference(negated_conjecture,[status(cth)],[f1])).
% 129.82/18.53 thf(f3,plain,(
% 129.82/18.53 ~ ! [X0 : (a > a > $o)] : (! [X1 : a,X2 : a,X3 : a] : ((! [X4 : (a > $o)] : ((! [X5 : a,X6 : a] : (((X0 @ X5 @ X6) & (X4 @ X5)) => (X4 @ X6)) & ! [X7 : a] : ((X0 @ X2 @ X7) => (X4 @ X7))) => (X4 @ X3)) & ! [X8 : (a > $o)] : ((! [X9 : a,X10 : a] : (((X0 @ X9 @ X10) & (X8 @ X9)) => (X8 @ X10)) & ! [X11 : a] : ((X0 @ X1 @ X11) => (X8 @ X11))) => (X8 @ X2))) => ! [X12 : (a > $o)] : ((! [X13 : a,X14 : a] : (((X0 @ X13 @ X14) & (X12 @ X13)) => (X12 @ X14)) & ! [X15 : a] : ((X0 @ X1 @ X15) => (X12 @ X15))) => (X12 @ X3))) & ! [X16 : a,X17 : a] : ((X0 @ X16 @ X17) => ! [X18 : (a > $o)] : ((! [X19 : a,X20 : a] : (((X0 @ X19 @ X20) & (X18 @ X19)) => (X18 @ X20)) & ! [X21 : a] : ((X0 @ X16 @ X21) => (X18 @ X21))) => (X18 @ X17))))),
% 129.82/18.53 inference(rectify,[],[f2])).
% 129.82/18.53 thf(f4,plain,(
% 129.82/18.53 ~ ! [X0 : (a > a > $o)] : (! [X1 : a,X2 : a,X3 : a] : ((! [X4 : (a > $o)] : ((! [X5 : a,X6 : a] : (((((X0 @ X5 @ X6)) = $true) & (((X4 @ X5)) = $true)) => (((X4 @ X6)) = $true)) & ! [X7 : a] : ((((X0 @ X2 @ X7)) = $true) => (((X4 @ X7)) = $true))) => (((X4 @ X3)) = $true)) & ! [X8 : (a > $o)] : ((! [X9 : a,X10 : a] : (((((X0 @ X9 @ X10)) = $true) & (((X8 @ X9)) = $true)) => (((X8 @ X10)) = $true)) & ! [X11 : a] : ((((X0 @ X1 @ X11)) = $true) => (((X8 @ X11)) = $true))) => (((X8 @ X2)) = $true))) => ! [X12 : (a > $o)] : ((! [X13 : a,X14 : a] : (((((X0 @ X13 @ X14)) = $true) & (((X12 @ X13)) = $true)) => (((X12 @ X14)) = $true)) & ! [X15 : a] : ((((X0 @ X1 @ X15)) = $true) => (((X12 @ X15)) = $true))) => (((X12 @ X3)) = $true))) & ! [X16 : a,X17 : a] : ((((X0 @ X16 @ X17)) = $true) => ! [X18 : (a > $o)] : ((! [X19 : a,X20 : a] : (((((X0 @ X19 @ X20)) = $true) & (((X18 @ X19)) = $true)) => (((X18 @ X20)) = $true)) & ! [X21 : a] : ((((X0 @ X16 @ X21)) = $true) => (((X18 @ X21)) = $true))) => (((X18 @ X17)) = $true))))),
% 129.82/18.53 inference(fool_elimination,[],[f3])).
% 129.82/18.53 thf(f5,plain,(
% 129.82/18.53 ? [X0 : (a > a > $o)] : (? [X1 : a,X2 : a,X3 : a] : (? [X12 : (a > $o)] : ((((X12 @ X3)) != $true) & (! [X13 : a,X14 : a] : ((((X12 @ X14)) = $true) | ((((X0 @ X13 @ X14)) != $true) | (((X12 @ X13)) != $true))) & ! [X15 : a] : ((((X12 @ X15)) = $true) | (((X0 @ X1 @ X15)) != $true)))) & (! [X4 : (a > $o)] : ((((X4 @ X3)) = $true) | (? [X5 : a,X6 : a] : ((((X4 @ X6)) != $true) & ((((X0 @ X5 @ X6)) = $true) & (((X4 @ X5)) = $true))) | ? [X7 : a] : ((((X4 @ X7)) != $true) & (((X0 @ X2 @ X7)) = $true)))) & ! [X8 : (a > $o)] : ((((X8 @ X2)) = $true) | (? [X9 : a,X10 : a] : ((((X8 @ X10)) != $true) & ((((X0 @ X9 @ X10)) = $true) & (((X8 @ X9)) = $true))) | ? [X11 : a] : ((((X8 @ X11)) != $true) & (((X0 @ X1 @ X11)) = $true)))))) | ? [X16 : a,X17 : a] : (? [X18 : (a > $o)] : ((((X18 @ X17)) != $true) & (! [X19 : a,X20 : a] : ((((X18 @ X20)) = $true) | ((((X0 @ X19 @ X20)) != $true) | (((X18 @ X19)) != $true))) & ! [X21 : a] : ((((X18 @ X21)) = $true) | (((X0 @ X16 @ X21)) != $true)))) & (((X0 @ X16 @ X17)) = $true)))),
% 129.82/18.53 inference(ennf_transformation,[],[f4])).
% 129.82/18.53 thf(f6,plain,(
% 129.82/18.53 ? [X0 : (a > a > $o)] : (? [X1 : a,X2 : a,X3 : a] : (? [X12 : (a > $o)] : ((((X12 @ X3)) != $true) & ! [X13 : a,X14 : a] : ((((X12 @ X14)) = $true) | (((X0 @ X13 @ X14)) != $true) | (((X12 @ X13)) != $true)) & ! [X15 : a] : ((((X12 @ X15)) = $true) | (((X0 @ X1 @ X15)) != $true))) & ! [X4 : (a > $o)] : ((((X4 @ X3)) = $true) | ? [X5 : a,X6 : a] : ((((X4 @ X6)) != $true) & (((X0 @ X5 @ X6)) = $true) & (((X4 @ X5)) = $true)) | ? [X7 : a] : ((((X4 @ X7)) != $true) & (((X0 @ X2 @ X7)) = $true))) & ! [X8 : (a > $o)] : ((((X8 @ X2)) = $true) | ? [X9 : a,X10 : a] : ((((X8 @ X10)) != $true) & (((X0 @ X9 @ X10)) = $true) & (((X8 @ X9)) = $true)) | ? [X11 : a] : ((((X8 @ X11)) != $true) & (((X0 @ X1 @ X11)) = $true)))) | ? [X16 : a,X17 : a] : (? [X18 : (a > $o)] : ((((X18 @ X17)) != $true) & ! [X19 : a,X20 : a] : ((((X18 @ X20)) = $true) | (((X0 @ X19 @ X20)) != $true) | (((X18 @ X19)) != $true)) & ! [X21 : a] : ((((X18 @ X21)) = $true) | (((X0 @ X16 @ X21)) != $true))) & (((X0 @ X16 @ X17)) = $true)))),
% 129.82/18.53 inference(flattening,[],[f5])).
% 129.82/18.53 thf(f7,plain,(
% 129.82/18.53 ? [X0 : (a > a > $o)] : (? [X1 : a,X2 : a,X3 : a] : (? [X4 : (a > $o)] : ((((X4 @ X3)) != $true) & ! [X5 : a,X6 : a] : ((((X4 @ X6)) = $true) | (((X0 @ X5 @ X6)) != $true) | (((X4 @ X5)) != $true)) & ! [X7 : a] : ((((X4 @ X7)) = $true) | ($true != ((X0 @ X1 @ X7))))) & ! [X8 : (a > $o)] : (($true = ((X8 @ X3))) | ? [X9 : a,X10 : a] : ((((X8 @ X10)) != $true) & (((X0 @ X9 @ X10)) = $true) & (((X8 @ X9)) = $true)) | ? [X11 : a] : ((((X8 @ X11)) != $true) & ($true = ((X0 @ X2 @ X11))))) & ! [X12 : (a > $o)] : (($true = ((X12 @ X2))) | ? [X13 : a,X14 : a] : ((((X12 @ X14)) != $true) & (((X0 @ X13 @ X14)) = $true) & (((X12 @ X13)) = $true)) | ? [X15 : a] : ((((X12 @ X15)) != $true) & (((X0 @ X1 @ X15)) = $true)))) | ? [X16 : a,X17 : a] : (? [X18 : (a > $o)] : ((((X18 @ X17)) != $true) & ! [X19 : a,X20 : a] : ((((X18 @ X20)) = $true) | (((X0 @ X19 @ X20)) != $true) | (((X18 @ X19)) != $true)) & ! [X21 : a] : ((((X18 @ X21)) = $true) | (((X0 @ X16 @ X21)) != $true))) & (((X0 @ X16 @ X17)) = $true)))),
% 129.82/18.53 inference(rectify,[],[f6])).
% 129.82/18.53 thf(f8,plain,(
% 129.82/18.53 ((($true != ((sK4 @ sK3))) & ! [X5 : a,X6 : a] : (($true = ((sK4 @ X6))) | ($true != ((sK0 @ X5 @ X6))) | ($true != ((sK4 @ X5)))) & ! [X7 : a] : (($true = ((sK4 @ X7))) | ($true != ((sK0 @ sK1 @ X7))))) & ! [X8 : (a > $o)] : (($true = ((X8 @ sK3))) | (($true != ((X8 @ (sK6 @ X8)))) & ($true = ((sK0 @ (sK5 @ X8) @ (sK6 @ X8)))) & ($true = ((X8 @ (sK5 @ X8))))) | (($true != ((X8 @ (sK7 @ X8)))) & ($true = ((sK0 @ sK2 @ (sK7 @ X8)))))) & ! [X12 : (a > $o)] : (($true = ((X12 @ sK2))) | (($true != ((X12 @ (sK9 @ X12)))) & ($true = ((sK0 @ (sK8 @ X12) @ (sK9 @ X12)))) & ($true = ((X12 @ (sK8 @ X12))))) | (($true != ((X12 @ (sK10 @ X12)))) & ($true = ((sK0 @ sK1 @ (sK10 @ X12))))))) | ((($true != ((sK13 @ sK12))) & ! [X19 : a,X20 : a] : (($true = ((sK13 @ X20))) | ($true != ((sK0 @ X19 @ X20))) | ($true != ((sK13 @ X19)))) & ! [X21 : a] : (($true = ((sK13 @ X21))) | ($true != ((sK0 @ sK11 @ X21))))) & ($true = ((sK0 @ sK11 @ sK12))))),
% 129.82/18.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,vAPP,vAPP,vAPP,vAPP,vAPP,vAPP,sK11,sK12,sK13]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4),skolemize(X15,sK10 @ X12),skolemize(X15,sK10 @ X12),skolemize(X15,sK10 @ X12),skolemize(X15,sK10 @ X12),skolemize(X15,sK10 @ X12),skolemize(X15,sK10 @ X12),skolemize(X16,sK11),skolemize(X17,sK12),skolemize(X18,sK13)],[f7])).
% 129.82/18.53 thf(f9,plain,(
% 129.82/18.53 ( ! [X12 : (a > $o)] : (($true = ((X12 @ sK2))) | ($true = ((X12 @ (sK8 @ X12)))) | ($true = ((sK0 @ sK1 @ (sK10 @ X12)))) | ($true = ((sK0 @ sK11 @ sK12)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f10,plain,(
% 129.82/18.53 ( ! [X21 : a,X12 : (a > $o)] : (($true = ((X12 @ sK2))) | ($true = ((X12 @ (sK8 @ X12)))) | ($true = ((sK0 @ sK1 @ (sK10 @ X12)))) | ($true = ((sK13 @ X21))) | ($true != ((sK0 @ sK11 @ X21)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f12,plain,(
% 129.82/18.53 ( ! [X12 : (a > $o)] : (($true = ((X12 @ sK2))) | ($true = ((X12 @ (sK8 @ X12)))) | ($true = ((sK0 @ sK1 @ (sK10 @ X12)))) | ($true != ((sK13 @ sK12)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f13,plain,(
% 129.82/18.53 ( ! [X12 : (a > $o)] : (($true = ((X12 @ sK2))) | ($true = ((X12 @ (sK8 @ X12)))) | ($true != ((X12 @ (sK10 @ X12)))) | ($true = ((sK0 @ sK11 @ sK12)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f14,plain,(
% 129.82/18.53 ( ! [X21 : a,X12 : (a > $o)] : (($true = ((X12 @ sK2))) | ($true = ((X12 @ (sK8 @ X12)))) | ($true != ((X12 @ (sK10 @ X12)))) | ($true = ((sK13 @ X21))) | ($true != ((sK0 @ sK11 @ X21)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f16,plain,(
% 129.82/18.53 ( ! [X12 : (a > $o)] : (($true = ((X12 @ sK2))) | ($true = ((X12 @ (sK8 @ X12)))) | ($true != ((X12 @ (sK10 @ X12)))) | ($true != ((sK13 @ sK12)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f17,plain,(
% 129.82/18.53 ( ! [X12 : (a > $o)] : (($true = ((X12 @ sK2))) | ($true = ((sK0 @ (sK8 @ X12) @ (sK9 @ X12)))) | ($true = ((sK0 @ sK1 @ (sK10 @ X12)))) | ($true = ((sK0 @ sK11 @ sK12)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f18,plain,(
% 129.82/18.53 ( ! [X21 : a,X12 : (a > $o)] : (($true = ((X12 @ sK2))) | ($true = ((sK0 @ (sK8 @ X12) @ (sK9 @ X12)))) | ($true = ((sK0 @ sK1 @ (sK10 @ X12)))) | ($true = ((sK13 @ X21))) | ($true != ((sK0 @ sK11 @ X21)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f20,plain,(
% 129.82/18.53 ( ! [X12 : (a > $o)] : (($true = ((X12 @ sK2))) | ($true = ((sK0 @ (sK8 @ X12) @ (sK9 @ X12)))) | ($true = ((sK0 @ sK1 @ (sK10 @ X12)))) | ($true != ((sK13 @ sK12)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f21,plain,(
% 129.82/18.53 ( ! [X12 : (a > $o)] : (($true = ((X12 @ sK2))) | ($true = ((sK0 @ (sK8 @ X12) @ (sK9 @ X12)))) | ($true != ((X12 @ (sK10 @ X12)))) | ($true = ((sK0 @ sK11 @ sK12)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f22,plain,(
% 129.82/18.53 ( ! [X21 : a,X12 : (a > $o)] : (($true = ((X12 @ sK2))) | ($true = ((sK0 @ (sK8 @ X12) @ (sK9 @ X12)))) | ($true != ((X12 @ (sK10 @ X12)))) | ($true = ((sK13 @ X21))) | ($true != ((sK0 @ sK11 @ X21)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f24,plain,(
% 129.82/18.53 ( ! [X12 : (a > $o)] : (($true = ((X12 @ sK2))) | ($true = ((sK0 @ (sK8 @ X12) @ (sK9 @ X12)))) | ($true != ((X12 @ (sK10 @ X12)))) | ($true != ((sK13 @ sK12)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f25,plain,(
% 129.82/18.53 ( ! [X12 : (a > $o)] : (($true = ((X12 @ sK2))) | ($true != ((X12 @ (sK9 @ X12)))) | ($true = ((sK0 @ sK1 @ (sK10 @ X12)))) | ($true = ((sK0 @ sK11 @ sK12)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f26,plain,(
% 129.82/18.53 ( ! [X21 : a,X12 : (a > $o)] : (($true = ((X12 @ sK2))) | ($true != ((X12 @ (sK9 @ X12)))) | ($true = ((sK0 @ sK1 @ (sK10 @ X12)))) | ($true = ((sK13 @ X21))) | ($true != ((sK0 @ sK11 @ X21)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f28,plain,(
% 129.82/18.53 ( ! [X12 : (a > $o)] : (($true = ((X12 @ sK2))) | ($true != ((X12 @ (sK9 @ X12)))) | ($true = ((sK0 @ sK1 @ (sK10 @ X12)))) | ($true != ((sK13 @ sK12)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f29,plain,(
% 129.82/18.53 ( ! [X12 : (a > $o)] : (($true = ((X12 @ sK2))) | ($true != ((X12 @ (sK9 @ X12)))) | ($true != ((X12 @ (sK10 @ X12)))) | ($true = ((sK0 @ sK11 @ sK12)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f30,plain,(
% 129.82/18.53 ( ! [X21 : a,X12 : (a > $o)] : (($true = ((X12 @ sK2))) | ($true != ((X12 @ (sK9 @ X12)))) | ($true != ((X12 @ (sK10 @ X12)))) | ($true = ((sK13 @ X21))) | ($true != ((sK0 @ sK11 @ X21)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f32,plain,(
% 129.82/18.53 ( ! [X12 : (a > $o)] : (($true = ((X12 @ sK2))) | ($true != ((X12 @ (sK9 @ X12)))) | ($true != ((X12 @ (sK10 @ X12)))) | ($true != ((sK13 @ sK12)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f33,plain,(
% 129.82/18.53 ( ! [X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true = ((X8 @ (sK5 @ X8)))) | ($true = ((sK0 @ sK2 @ (sK7 @ X8)))) | ($true = ((sK0 @ sK11 @ sK12)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f34,plain,(
% 129.82/18.53 ( ! [X21 : a,X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true = ((X8 @ (sK5 @ X8)))) | ($true = ((sK0 @ sK2 @ (sK7 @ X8)))) | ($true = ((sK13 @ X21))) | ($true != ((sK0 @ sK11 @ X21)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f36,plain,(
% 129.82/18.53 ( ! [X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true = ((X8 @ (sK5 @ X8)))) | ($true = ((sK0 @ sK2 @ (sK7 @ X8)))) | ($true != ((sK13 @ sK12)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f37,plain,(
% 129.82/18.53 ( ! [X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true = ((X8 @ (sK5 @ X8)))) | ($true != ((X8 @ (sK7 @ X8)))) | ($true = ((sK0 @ sK11 @ sK12)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f38,plain,(
% 129.82/18.53 ( ! [X21 : a,X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true = ((X8 @ (sK5 @ X8)))) | ($true != ((X8 @ (sK7 @ X8)))) | ($true = ((sK13 @ X21))) | ($true != ((sK0 @ sK11 @ X21)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f40,plain,(
% 129.82/18.53 ( ! [X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true = ((X8 @ (sK5 @ X8)))) | ($true != ((X8 @ (sK7 @ X8)))) | ($true != ((sK13 @ sK12)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f41,plain,(
% 129.82/18.53 ( ! [X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true = ((sK0 @ (sK5 @ X8) @ (sK6 @ X8)))) | ($true = ((sK0 @ sK2 @ (sK7 @ X8)))) | ($true = ((sK0 @ sK11 @ sK12)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f42,plain,(
% 129.82/18.53 ( ! [X21 : a,X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true = ((sK0 @ (sK5 @ X8) @ (sK6 @ X8)))) | ($true = ((sK0 @ sK2 @ (sK7 @ X8)))) | ($true = ((sK13 @ X21))) | ($true != ((sK0 @ sK11 @ X21)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f44,plain,(
% 129.82/18.53 ( ! [X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true = ((sK0 @ (sK5 @ X8) @ (sK6 @ X8)))) | ($true = ((sK0 @ sK2 @ (sK7 @ X8)))) | ($true != ((sK13 @ sK12)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f45,plain,(
% 129.82/18.53 ( ! [X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true = ((sK0 @ (sK5 @ X8) @ (sK6 @ X8)))) | ($true != ((X8 @ (sK7 @ X8)))) | ($true = ((sK0 @ sK11 @ sK12)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f46,plain,(
% 129.82/18.53 ( ! [X21 : a,X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true = ((sK0 @ (sK5 @ X8) @ (sK6 @ X8)))) | ($true != ((X8 @ (sK7 @ X8)))) | ($true = ((sK13 @ X21))) | ($true != ((sK0 @ sK11 @ X21)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f48,plain,(
% 129.82/18.53 ( ! [X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true = ((sK0 @ (sK5 @ X8) @ (sK6 @ X8)))) | ($true != ((X8 @ (sK7 @ X8)))) | ($true != ((sK13 @ sK12)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f49,plain,(
% 129.82/18.53 ( ! [X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true != ((X8 @ (sK6 @ X8)))) | ($true = ((sK0 @ sK2 @ (sK7 @ X8)))) | ($true = ((sK0 @ sK11 @ sK12)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f50,plain,(
% 129.82/18.53 ( ! [X21 : a,X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true != ((X8 @ (sK6 @ X8)))) | ($true = ((sK0 @ sK2 @ (sK7 @ X8)))) | ($true = ((sK13 @ X21))) | ($true != ((sK0 @ sK11 @ X21)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f52,plain,(
% 129.82/18.53 ( ! [X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true != ((X8 @ (sK6 @ X8)))) | ($true = ((sK0 @ sK2 @ (sK7 @ X8)))) | ($true != ((sK13 @ sK12)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f53,plain,(
% 129.82/18.53 ( ! [X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true != ((X8 @ (sK6 @ X8)))) | ($true != ((X8 @ (sK7 @ X8)))) | ($true = ((sK0 @ sK11 @ sK12)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f54,plain,(
% 129.82/18.53 ( ! [X21 : a,X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true != ((X8 @ (sK6 @ X8)))) | ($true != ((X8 @ (sK7 @ X8)))) | ($true = ((sK13 @ X21))) | ($true != ((sK0 @ sK11 @ X21)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f56,plain,(
% 129.82/18.53 ( ! [X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true != ((X8 @ (sK6 @ X8)))) | ($true != ((X8 @ (sK7 @ X8)))) | ($true != ((sK13 @ sK12)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f57,plain,(
% 129.82/18.53 ( ! [X7 : a] : (($true = ((sK4 @ X7))) | ($true != ((sK0 @ sK1 @ X7))) | ($true = ((sK0 @ sK11 @ sK12)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f58,plain,(
% 129.82/18.53 ( ! [X21 : a,X7 : a] : (($true = ((sK4 @ X7))) | ($true != ((sK0 @ sK1 @ X7))) | ($true = ((sK13 @ X21))) | ($true != ((sK0 @ sK11 @ X21)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f60,plain,(
% 129.82/18.53 ( ! [X7 : a] : (($true = ((sK4 @ X7))) | ($true != ((sK0 @ sK1 @ X7))) | ($true != ((sK13 @ sK12)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f61,plain,(
% 129.82/18.53 ( ! [X6 : a,X5 : a] : (($true = ((sK4 @ X6))) | ($true != ((sK0 @ X5 @ X6))) | ($true != ((sK4 @ X5))) | ($true = ((sK0 @ sK11 @ sK12)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f62,plain,(
% 129.82/18.53 ( ! [X21 : a,X6 : a,X5 : a] : (($true = ((sK4 @ X6))) | ($true != ((sK0 @ X5 @ X6))) | ($true != ((sK4 @ X5))) | ($true = ((sK13 @ X21))) | ($true != ((sK0 @ sK11 @ X21)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f64,plain,(
% 129.82/18.53 ( ! [X6 : a,X5 : a] : (($true = ((sK4 @ X6))) | ($true != ((sK0 @ X5 @ X6))) | ($true != ((sK4 @ X5))) | ($true != ((sK13 @ sK12)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f65,plain,(
% 129.82/18.53 ($true != ((sK4 @ sK3))) | ($true = ((sK0 @ sK11 @ sK12)))),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f66,plain,(
% 129.82/18.53 ( ! [X21 : a] : (($true != ((sK4 @ sK3))) | ($true = ((sK13 @ X21))) | ($true != ((sK0 @ sK11 @ X21)))) )),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f68,plain,(
% 129.82/18.53 ($true != ((sK4 @ sK3))) | ($true != ((sK13 @ sK12)))),
% 129.82/18.53 inference(cnf_transformation,[],[f8])).
% 129.82/18.53 thf(f70,definition,(
% 129.82/18.53 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 129.82/18.53 introduced(theory,[fool_exhaustiveness_axiom])).
% 129.82/18.53 thf(f72,definition,(
% 129.82/18.53 spl14_1 <=> ($true = ((sK13 @ sK12)))),
% 129.82/18.53 introduced(definition,[new_symbols(definition,[spl14_1])],[avatar_definition])).
% 129.82/18.53 thf(f73,plain,(
% 129.82/18.53 ($true = ((sK13 @ sK12))) | ~spl14_1),
% 129.82/18.53 inference(avatar_component_clause,[],[f72])).
% 129.82/18.53 thf(f74,plain,(
% 129.82/18.53 ($true != ((sK13 @ sK12))) | spl14_1),
% 129.82/18.53 inference(avatar_component_clause,[],[f72])).
% 129.82/18.53 thf(f76,definition,(
% 129.82/18.53 spl14_2 <=> ($true = ((sK4 @ sK3)))),
% 129.82/18.53 introduced(definition,[new_symbols(definition,[spl14_2])],[avatar_definition])).
% 129.82/18.53 thf(f77,plain,(
% 129.82/18.53 ($true = ((sK4 @ sK3))) | ~spl14_2),
% 129.82/18.53 inference(avatar_component_clause,[],[f76])).
% 129.82/18.53 thf(f78,plain,(
% 129.82/18.53 ($true != ((sK4 @ sK3))) | spl14_2),
% 129.82/18.53 inference(avatar_component_clause,[],[f76])).
% 129.82/18.53 thf(f79,plain,(
% 129.82/18.53 ~spl14_1 | ~spl14_2),
% 129.82/18.53 inference(avatar_split_clause,[],[f68,f76,f72])).
% 129.82/18.53 thf(f81,definition,(
% 129.82/18.53 spl14_3 <=> ($true = ((sK0 @ sK11 @ sK12)))),
% 129.82/18.53 introduced(definition,[new_symbols(definition,[spl14_3])],[avatar_definition])).
% 129.82/18.53 thf(f82,plain,(
% 129.82/18.53 ($true != ((sK0 @ sK11 @ sK12))) | spl14_3),
% 129.82/18.53 inference(avatar_component_clause,[],[f81])).
% 129.82/18.53 thf(f83,plain,(
% 129.82/18.53 ($true = ((sK0 @ sK11 @ sK12))) | ~spl14_3),
% 129.82/18.53 inference(avatar_component_clause,[],[f81])).
% 129.82/18.53 thf(f84,plain,(
% 129.82/18.53 spl14_3 | ~spl14_2),
% 129.82/18.53 inference(avatar_split_clause,[],[f65,f76,f81])).
% 129.82/18.53 thf(f86,definition,(
% 129.82/18.53 spl14_4 <=> ! [X7 : a] : (($true = ((sK4 @ X7))) | ($true != ((sK0 @ sK1 @ X7))))),
% 129.82/18.53 introduced(definition,[new_symbols(definition,[spl14_4])],[avatar_definition])).
% 129.82/18.53 thf(f87,plain,(
% 129.82/18.53 ( ! [X7 : a] : (($true != ((sK0 @ sK1 @ X7))) | ($true = ((sK4 @ X7)))) ) | ~spl14_4),
% 129.82/18.53 inference(avatar_component_clause,[],[f86])).
% 129.82/18.53 thf(f88,plain,(
% 129.82/18.53 spl14_3 | spl14_4),
% 129.82/18.53 inference(avatar_split_clause,[],[f57,f86,f81])).
% 129.82/18.53 thf(f90,definition,(
% 129.82/18.53 spl14_5 <=> ! [X21 : a] : (($true = ((sK13 @ X21))) | ($true != ((sK0 @ sK11 @ X21))))),
% 129.82/18.53 introduced(definition,[new_symbols(definition,[spl14_5])],[avatar_definition])).
% 129.82/18.53 thf(f91,plain,(
% 129.82/18.53 ( ! [X21 : a] : (($true != ((sK0 @ sK11 @ X21))) | ($true = ((sK13 @ X21)))) ) | ~spl14_5),
% 129.82/18.53 inference(avatar_component_clause,[],[f90])).
% 129.82/18.53 thf(f92,plain,(
% 129.82/18.53 spl14_5 | spl14_4),
% 129.82/18.53 inference(avatar_split_clause,[],[f58,f86,f90])).
% 129.82/18.53 thf(f94,definition,(
% 129.82/18.53 spl14_6 <=> ! [X6 : a,X5 : a] : (($true = ((sK4 @ X6))) | ($true != ((sK4 @ X5))) | ($true != ((sK0 @ X5 @ X6))))),
% 129.82/18.53 introduced(definition,[new_symbols(definition,[spl14_6])],[avatar_definition])).
% 129.82/18.53 thf(f95,plain,(
% 129.82/18.53 ( ! [X6 : a,X5 : a] : (($true != ((sK0 @ X5 @ X6))) | ($true != ((sK4 @ X5))) | ($true = ((sK4 @ X6)))) ) | ~spl14_6),
% 129.82/18.53 inference(avatar_component_clause,[],[f94])).
% 129.82/18.53 thf(f96,plain,(
% 129.82/18.53 spl14_5 | spl14_6),
% 129.82/18.53 inference(avatar_split_clause,[],[f62,f94,f90])).
% 129.82/18.53 thf(f97,plain,(
% 129.82/18.53 ($true != $true) | ($true = ((sK13 @ sK12))) | (~spl14_3 | ~spl14_5)),
% 129.82/18.53 inference(constrained_superposition,[],[f91,f83])).
% 129.82/18.53 thf(f98,plain,(
% 129.82/18.53 ($true = ((sK13 @ sK12))) | (~spl14_3 | ~spl14_5)),
% 129.82/18.53 inference(trivial_inequality_removal,[],[f97])).
% 129.82/18.53 thf(f99,plain,(
% 129.82/18.53 $false | (spl14_1 | ~spl14_3 | ~spl14_5)),
% 129.82/18.53 inference(forward_subsumption_resolution,[],[f98,f74])).
% 129.82/18.53 thf(f100,plain,(
% 129.82/18.53 spl14_1 | ~spl14_3 | ~spl14_5),
% 129.82/18.53 inference(avatar_contradiction_clause,[],[f99])).
% 129.82/18.53 thf(f113,definition,(
% 129.82/18.53 spl14_9 <=> ! [X12 : (a > $o)] : (($true = ((X12 @ sK2))) | ($true != ((X12 @ (sK10 @ X12)))) | ($true = ((X12 @ (sK8 @ X12)))))),
% 129.82/18.53 introduced(definition,[new_symbols(definition,[spl14_9])],[avatar_definition])).
% 129.82/18.53 thf(f114,plain,(
% 129.82/18.53 ( ! [X12 : (a > $o)] : (($true != ((X12 @ (sK10 @ X12)))) | ($true = ((X12 @ sK2))) | ($true = ((X12 @ (sK8 @ X12))))) ) | ~spl14_9),
% 129.82/18.53 inference(avatar_component_clause,[],[f113])).
% 129.82/18.53 thf(f115,plain,(
% 129.82/18.53 spl14_5 | spl14_9),
% 129.82/18.53 inference(avatar_split_clause,[],[f14,f113,f90])).
% 129.82/18.53 thf(f116,plain,(
% 129.82/18.53 ( ! [X12 : (a > $o)] : (($true = ((X12 @ sK2))) | ($true = ((X12 @ (sK8 @ X12)))) | ($true != ((X12 @ (sK10 @ X12))))) ) | spl14_3),
% 129.82/18.53 inference(forward_subsumption_resolution,[],[f13,f82])).
% 129.82/18.53 thf(f117,plain,(
% 129.82/18.53 spl14_9 | spl14_3),
% 129.82/18.53 inference(avatar_split_clause,[],[f116,f81,f113])).
% 129.82/18.53 thf(f124,plain,(
% 129.82/18.53 ( ! [X12 : (a > $o)] : (($true = ((X12 @ sK2))) | ($true = ((X12 @ (sK8 @ X12)))) | ($true != ((X12 @ (sK10 @ X12))))) ) | ~spl14_1),
% 129.82/18.53 inference(forward_subsumption_resolution,[],[f16,f73])).
% 129.82/18.53 thf(f125,plain,(
% 129.82/18.53 spl14_9 | ~spl14_1),
% 129.82/18.53 inference(avatar_split_clause,[],[f124,f72,f113])).
% 129.82/18.53 thf(f145,definition,(
% 129.82/18.53 spl14_10 <=> ! [X12 : (a > $o)] : (($true = ((X12 @ sK2))) | ($true != ((X12 @ (sK10 @ X12)))) | ($true != ((X12 @ (sK9 @ X12)))))),
% 129.82/18.53 introduced(definition,[new_symbols(definition,[spl14_10])],[avatar_definition])).
% 129.82/18.53 thf(f146,plain,(
% 129.82/18.53 ( ! [X12 : (a > $o)] : (($true != ((X12 @ (sK9 @ X12)))) | ($true != ((X12 @ (sK10 @ X12)))) | ($true = ((X12 @ sK2)))) ) | ~spl14_10),
% 129.82/18.53 inference(avatar_component_clause,[],[f145])).
% 129.82/18.53 thf(f147,plain,(
% 129.82/18.53 ~spl14_1 | spl14_10),
% 129.82/18.53 inference(avatar_split_clause,[],[f32,f145,f72])).
% 129.82/18.53 thf(f148,plain,(
% 129.82/18.53 ( ! [X12 : (a > $o)] : (($true = ((X12 @ sK2))) | ($true != ((X12 @ (sK9 @ X12)))) | ($true != ((X12 @ (sK10 @ X12))))) ) | spl14_3),
% 129.82/18.53 inference(forward_subsumption_resolution,[],[f29,f82])).
% 129.82/18.53 thf(f149,plain,(
% 129.82/18.53 spl14_10 | spl14_3),
% 129.82/18.53 inference(avatar_split_clause,[],[f148,f81,f145])).
% 129.82/18.53 thf(f153,plain,(
% 129.82/18.53 ( ! [X13 : (a > $o)] : (($true != (((^[Y0 : a]: (~ (X13 @ Y0))) @ (sK9 @ (^[Y0 : a]: (~ (X13 @ Y0))))))) | ($true != (((^[Y0 : a]: (~ (X13 @ Y0))) @ (sK10 @ (^[Y0 : a]: (~ (X13 @ Y0))))))) | ($true = (((^[Y0 : a]: (~ (X13 @ Y0))) @ sK2)))) ) | ~spl14_10),
% 129.82/18.53 inference(primitive_instantiation,[],[f146])).
% 129.82/18.53 thf(f156,plain,(
% 129.82/18.53 ( ! [X13 : (a > $o)] : (($true != ((~ (X13 @ (sK9 @ (^[Y0 : a]: (~ (X13 @ Y0)))))))) | ($true != ((~ (X13 @ (sK10 @ (^[Y0 : a]: (~ (X13 @ Y0)))))))) | ($true = ((~ (X13 @ sK2))))) ) | ~spl14_10),
% 129.82/18.54 inference(beta-eta_normalization,[],[f153])).
% 129.82/18.54 thf(f157,plain,(
% 129.82/18.54 ( ! [X13 : (a > $o)] : (($true = ((X13 @ (sK9 @ (^[Y0 : a]: (~ (X13 @ Y0))))))) | ($true != ((~ (X13 @ (sK10 @ (^[Y0 : a]: (~ (X13 @ Y0)))))))) | ($true = ((~ (X13 @ sK2))))) ) | ~spl14_10),
% 129.82/18.54 inference(not_proxy_clausification,[],[f156])).
% 129.82/18.54 thf(f158,plain,(
% 129.82/18.54 ( ! [X13 : (a > $o)] : (($true = ((X13 @ (sK9 @ (^[Y0 : a]: (~ (X13 @ Y0))))))) | ($true = ((X13 @ (sK10 @ (^[Y0 : a]: (~ (X13 @ Y0))))))) | ($true = ((~ (X13 @ sK2))))) ) | ~spl14_10),
% 129.82/18.54 inference(not_proxy_clausification,[],[f157])).
% 129.82/18.54 thf(f159,plain,(
% 129.82/18.54 ( ! [X13 : (a > $o)] : (($true = ((X13 @ (sK9 @ (^[Y0 : a]: (~ (X13 @ Y0))))))) | ($true = ((X13 @ (sK10 @ (^[Y0 : a]: (~ (X13 @ Y0))))))) | ($false = ((X13 @ sK2)))) ) | ~spl14_10),
% 129.82/18.54 inference(not_proxy_clausification,[],[f158])).
% 129.82/18.54 thf(f167,plain,(
% 129.82/18.54 ( ! [X8 : (a > $o)] : (($true != ((X8 @ (sK7 @ X8)))) | ($true = ((X8 @ (sK5 @ X8)))) | ($true = ((X8 @ sK3)))) ) | spl14_3),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f37,f82])).
% 129.82/18.54 thf(f182,plain,(
% 129.82/18.54 ( ! [X8 : (a > $o)] : (($true != ((X8 @ (sK7 @ X8)))) | ($true != ((X8 @ (sK6 @ X8)))) | ($true = ((X8 @ sK3)))) ) | spl14_3),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f53,f82])).
% 129.82/18.54 thf(f200,plain,(
% 129.82/18.54 ( ! [X12 : (a > $o)] : (($true = ((X12 @ (sK8 @ X12)))) | ($true = ((sK0 @ sK1 @ (sK10 @ X12)))) | ($true = ((X12 @ sK2)))) ) | spl14_3),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f9,f82])).
% 129.82/18.54 thf(f220,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true != $true) | ($true = ((sK4 @ (sK10 @ X0)))) | ($true = ((X0 @ (sK8 @ X0)))) | ($true = ((X0 @ sK2)))) ) | (spl14_3 | ~spl14_4)),
% 129.82/18.54 inference(constrained_superposition,[],[f87,f200])).
% 129.82/18.54 thf(f249,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true = ((sK4 @ (sK10 @ X0)))) | ($true = ((X0 @ (sK8 @ X0)))) | ($true = ((X0 @ sK2)))) ) | (spl14_3 | ~spl14_4)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f220])).
% 129.82/18.54 thf(f436,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true != $true) | ($true = ((sK4 @ (sK10 @ X0)))) | ($true = ((X0 @ sK2))) | (((X0 @ (sK8 @ X0))) != ((sK4 @ (sK10 @ X0))))) ) | (spl14_3 | ~spl14_4)),
% 129.82/18.54 inference(equality_factoring,[],[f249])).
% 129.82/18.54 thf(f445,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true != $true) | ($true = ((sK4 @ (sK10 @ X0)))) | ($true = ((X0 @ sK2))) | ($false = ((X0 @ (sK8 @ X0)))) | ($false = ((sK4 @ (sK10 @ X0))))) ) | (spl14_3 | ~spl14_4)),
% 129.82/18.54 inference(xor_proxy_clausification,[],[f436])).
% 129.82/18.54 thf(f446,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true = ((sK4 @ (sK10 @ X0)))) | ($false = ((X0 @ (sK8 @ X0)))) | ($true = ((X0 @ sK2))) | ($false = ((sK4 @ (sK10 @ X0))))) ) | (spl14_3 | ~spl14_4)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f445])).
% 129.82/18.54 thf(f1501,definition,(
% 129.82/18.54 spl14_12 <=> ($true = ((sK4 @ (sK8 @ sK4))))),
% 129.82/18.54 introduced(definition,[new_symbols(definition,[spl14_12])],[avatar_definition])).
% 129.82/18.54 thf(f1502,plain,(
% 129.82/18.54 ($true != ((sK4 @ (sK8 @ sK4)))) | spl14_12),
% 129.82/18.54 inference(avatar_component_clause,[],[f1501])).
% 129.82/18.54 thf(f1503,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK8 @ sK4)))) | ~spl14_12),
% 129.82/18.54 inference(avatar_component_clause,[],[f1501])).
% 129.82/18.54 thf(f1505,definition,(
% 129.82/18.54 spl14_13 <=> ($true = ((sK4 @ sK2)))),
% 129.82/18.54 introduced(definition,[new_symbols(definition,[spl14_13])],[avatar_definition])).
% 129.82/18.54 thf(f1506,plain,(
% 129.82/18.54 ($true != ((sK4 @ sK2))) | spl14_13),
% 129.82/18.54 inference(avatar_component_clause,[],[f1505])).
% 129.82/18.54 thf(f1507,plain,(
% 129.82/18.54 ($true = ((sK4 @ sK2))) | ~spl14_13),
% 129.82/18.54 inference(avatar_component_clause,[],[f1505])).
% 129.82/18.54 thf(f1551,plain,(
% 129.82/18.54 ( ! [X12 : (a > $o)] : (($true != ((X12 @ (sK9 @ X12)))) | ($true = ((X12 @ sK2))) | ($true = ((sK0 @ sK1 @ (sK10 @ X12))))) ) | spl14_3),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f25,f82])).
% 129.82/18.54 thf(f1553,definition,(
% 129.82/18.54 spl14_14 <=> ($false = ((sK4 @ sK2)))),
% 129.82/18.54 introduced(definition,[new_symbols(definition,[spl14_14])],[avatar_definition])).
% 129.82/18.54 thf(f1555,plain,(
% 129.82/18.54 ($false = ((sK4 @ sK2))) | ~spl14_14),
% 129.82/18.54 inference(avatar_component_clause,[],[f1553])).
% 129.82/18.54 thf(f1833,plain,(
% 129.82/18.54 ($true = $false) | ($true = ((sK4 @ (sK10 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK2))) | ($false = ((sK4 @ (sK10 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | (spl14_3 | ~spl14_4 | ~spl14_12)),
% 129.82/18.54 inference(constrained_superposition,[],[f1503,f446])).
% 129.82/18.54 thf(f1877,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK10 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK2))) | ($false = ((sK4 @ (sK10 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | (spl14_3 | ~spl14_4 | ~spl14_12)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f1833])).
% 129.82/18.54 thf(f1878,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK10 @ sK4)))) | ($true = ((sK4 @ sK2))) | ($false = ((sK4 @ (sK10 @ sK4)))) | (spl14_3 | ~spl14_4 | ~spl14_12)),
% 129.82/18.54 inference(beta-eta_normalization,[],[f1877])).
% 129.82/18.54 thf(f2019,plain,(
% 129.82/18.54 ($true = $false) | ($true = ((sK4 @ (sK10 @ sK4)))) | ($false = ((sK4 @ (sK10 @ sK4)))) | (spl14_3 | ~spl14_4 | ~spl14_12 | ~spl14_14)),
% 129.82/18.54 inference(forward_demodulation,[],[f1878,f1555])).
% 129.82/18.54 thf(f2020,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK10 @ sK4)))) | ($false = ((sK4 @ (sK10 @ sK4)))) | (spl14_3 | ~spl14_4 | ~spl14_12 | ~spl14_14)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f2019])).
% 129.82/18.54 thf(f2024,definition,(
% 129.82/18.54 spl14_15 <=> ($false = ((sK4 @ (sK10 @ sK4))))),
% 129.82/18.54 introduced(definition,[new_symbols(definition,[spl14_15])],[avatar_definition])).
% 129.82/18.54 thf(f2026,plain,(
% 129.82/18.54 ($false = ((sK4 @ (sK10 @ sK4)))) | ~spl14_15),
% 129.82/18.54 inference(avatar_component_clause,[],[f2024])).
% 129.82/18.54 thf(f2028,definition,(
% 129.82/18.54 spl14_16 <=> ($true = ((sK4 @ (sK10 @ sK4))))),
% 129.82/18.54 introduced(definition,[new_symbols(definition,[spl14_16])],[avatar_definition])).
% 129.82/18.54 thf(f2029,plain,(
% 129.82/18.54 ($true != ((sK4 @ (sK10 @ sK4)))) | spl14_16),
% 129.82/18.54 inference(avatar_component_clause,[],[f2028])).
% 129.82/18.54 thf(f2030,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK10 @ sK4)))) | ~spl14_16),
% 129.82/18.54 inference(avatar_component_clause,[],[f2028])).
% 129.82/18.54 thf(f2031,plain,(
% 129.82/18.54 spl14_15 | spl14_16 | spl14_3 | ~spl14_4 | ~spl14_12 | ~spl14_14),
% 129.82/18.54 inference(avatar_split_clause,[],[f2020,f1553,f1501,f86,f81,f2028,f2024])).
% 129.82/18.54 thf(f2076,plain,(
% 129.82/18.54 ( ! [X8 : (a > $o)] : (($true = ((X8 @ (sK5 @ X8)))) | ($true = ((sK0 @ sK2 @ (sK7 @ X8)))) | ($true = ((X8 @ sK3)))) ) | spl14_3),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f33,f82])).
% 129.82/18.54 thf(f2127,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true != $true) | ($true != ((sK4 @ sK2))) | ($true = ((sK4 @ (sK7 @ X0)))) | ($true = ((X0 @ (sK5 @ X0)))) | ($true = ((X0 @ sK3)))) ) | (spl14_3 | ~spl14_6)),
% 129.82/18.54 inference(constrained_superposition,[],[f95,f2076])).
% 129.82/18.54 thf(f2154,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true != ((sK4 @ sK2))) | ($true = ((sK4 @ (sK7 @ X0)))) | ($true = ((X0 @ (sK5 @ X0)))) | ($true = ((X0 @ sK3)))) ) | (spl14_3 | ~spl14_6)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f2127])).
% 129.82/18.54 thf(f4065,plain,(
% 129.82/18.54 ( ! [X8 : (a > $o)] : (($true != ((X8 @ (sK6 @ X8)))) | ($true = ((X8 @ sK3))) | ($true = ((sK0 @ sK2 @ (sK7 @ X8))))) ) | spl14_3),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f49,f82])).
% 129.82/18.54 thf(f6292,plain,(
% 129.82/18.54 ($true != $true) | ($true = ((sK4 @ (sK10 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK2))) | (spl14_3 | ~spl14_4 | spl14_12)),
% 129.82/18.54 inference(constrained_superposition,[],[f1502,f249])).
% 129.82/18.54 thf(f6368,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK10 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK2))) | (spl14_3 | ~spl14_4 | spl14_12)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f6292])).
% 129.82/18.54 thf(f6369,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK10 @ sK4)))) | ($true = ((sK4 @ sK2))) | (spl14_3 | ~spl14_4 | spl14_12)),
% 129.82/18.54 inference(beta-eta_normalization,[],[f6368])).
% 129.82/18.54 thf(f6381,plain,(
% 129.82/18.54 ($true = $false) | ($true = ((sK4 @ (sK10 @ sK4)))) | (spl14_3 | ~spl14_4 | spl14_12 | ~spl14_14)),
% 129.82/18.54 inference(forward_demodulation,[],[f6369,f1555])).
% 129.82/18.54 thf(f6382,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK10 @ sK4)))) | (spl14_3 | ~spl14_4 | spl14_12 | ~spl14_14)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f6381])).
% 129.82/18.54 thf(f6383,plain,(
% 129.82/18.54 spl14_16 | spl14_3 | ~spl14_4 | spl14_12 | ~spl14_14),
% 129.82/18.54 inference(avatar_split_clause,[],[f6382,f1553,f1501,f86,f81,f2028])).
% 129.82/18.54 thf(f6456,plain,(
% 129.82/18.54 ($true != $true) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK2))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ (sK8 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | (~spl14_9 | ~spl14_16)),
% 129.82/18.54 inference(constrained_superposition,[],[f114,f2030])).
% 129.82/18.54 thf(f6471,plain,(
% 129.82/18.54 ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK2))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ (sK8 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | (~spl14_9 | ~spl14_16)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f6456])).
% 129.82/18.54 thf(f6472,plain,(
% 129.82/18.54 ($true = ((sK4 @ sK2))) | ($true = ((sK4 @ (sK8 @ sK4)))) | (~spl14_9 | ~spl14_16)),
% 129.82/18.54 inference(beta-eta_normalization,[],[f6471])).
% 129.82/18.54 thf(f6513,plain,(
% 129.82/18.54 ($true = ((sK4 @ sK2))) | (~spl14_9 | spl14_12 | ~spl14_16)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f6472,f1502])).
% 129.82/18.54 thf(f6514,plain,(
% 129.82/18.54 ($true = $false) | (~spl14_9 | spl14_12 | ~spl14_14 | ~spl14_16)),
% 129.82/18.54 inference(forward_demodulation,[],[f6513,f1555])).
% 129.82/18.54 thf(f6515,plain,(
% 129.82/18.54 $false | (~spl14_9 | spl14_12 | ~spl14_14 | ~spl14_16)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f6514])).
% 129.82/18.54 thf(f6516,plain,(
% 129.82/18.54 ~spl14_9 | spl14_12 | ~spl14_14 | ~spl14_16),
% 129.82/18.54 inference(avatar_contradiction_clause,[],[f6515])).
% 129.82/18.54 thf(f6518,plain,(
% 129.82/18.54 spl14_13 | ~spl14_9 | spl14_12 | ~spl14_16),
% 129.82/18.54 inference(avatar_split_clause,[],[f6513,f2028,f1501,f113,f1505])).
% 129.82/18.54 thf(f7489,plain,(
% 129.82/18.54 ( ! [X12 : (a > $o)] : (($true != ((X12 @ (sK10 @ X12)))) | ($true = ((sK0 @ (sK8 @ X12) @ (sK9 @ X12)))) | ($true = ((X12 @ sK2)))) ) | spl14_3),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f21,f82])).
% 129.82/18.54 thf(f8162,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true = ((sK4 @ (sK7 @ X0)))) | ($true = ((X0 @ (sK5 @ X0)))) | ($true = ((X0 @ sK3)))) ) | (spl14_3 | ~spl14_6 | ~spl14_13)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f2154,f1507])).
% 129.82/18.54 thf(f8198,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true != $true) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ (sK5 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK3))) | ($true = ((X0 @ (sK5 @ X0)))) | ($true = ((X0 @ sK3))) | (sK4 != X0)) ) | (spl14_3 | ~spl14_6 | ~spl14_13)),
% 129.82/18.54 inference(constrained_superposition,[],[f167,f8162])).
% 129.82/18.54 thf(f8401,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ (sK5 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK3))) | ($true = ((X0 @ (sK5 @ X0)))) | ($true = ((X0 @ sK3))) | (sK4 != X0)) ) | (spl14_3 | ~spl14_6 | ~spl14_13)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f8198])).
% 129.82/18.54 thf(f8402,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true = ((sK4 @ (sK5 @ sK4)))) | ($true = ((sK4 @ sK3))) | ($true = ((X0 @ (sK5 @ X0)))) | ($true = ((X0 @ sK3))) | (sK4 != X0)) ) | (spl14_3 | ~spl14_6 | ~spl14_13)),
% 129.82/18.54 inference(beta-eta_normalization,[],[f8401])).
% 129.82/18.54 thf(f8502,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true = ((sK4 @ (sK5 @ sK4)))) | ($true = ((X0 @ (sK5 @ X0)))) | ($true = ((X0 @ sK3))) | (sK4 != X0)) ) | (spl14_2 | spl14_3 | ~spl14_6 | ~spl14_13)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f8402,f78])).
% 129.82/18.54 thf(f8505,definition,(
% 129.82/18.54 spl14_20 <=> ! [X0 : (a > $o)] : (($true = ((X0 @ (sK5 @ X0)))) | (sK4 != X0) | ($true = ((X0 @ sK3))))),
% 129.82/18.54 introduced(definition,[new_symbols(definition,[spl14_20])],[avatar_definition])).
% 129.82/18.54 thf(f8506,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : ((sK4 != X0) | ($true = ((X0 @ (sK5 @ X0)))) | ($true = ((X0 @ sK3)))) ) | ~spl14_20),
% 129.82/18.54 inference(avatar_component_clause,[],[f8505])).
% 129.82/18.54 thf(f8508,definition,(
% 129.82/18.54 spl14_21 <=> ($true = ((sK4 @ (sK5 @ sK4))))),
% 129.82/18.54 introduced(definition,[new_symbols(definition,[spl14_21])],[avatar_definition])).
% 129.82/18.54 thf(f8509,plain,(
% 129.82/18.54 ($true != ((sK4 @ (sK5 @ sK4)))) | spl14_21),
% 129.82/18.54 inference(avatar_component_clause,[],[f8508])).
% 129.82/18.54 thf(f8510,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK5 @ sK4)))) | ~spl14_21),
% 129.82/18.54 inference(avatar_component_clause,[],[f8508])).
% 129.82/18.54 thf(f8511,plain,(
% 129.82/18.54 spl14_20 | spl14_21 | spl14_2 | spl14_3 | ~spl14_6 | ~spl14_13),
% 129.82/18.54 inference(avatar_split_clause,[],[f8502,f1505,f94,f81,f76,f8508,f8505])).
% 129.82/18.54 thf(f8512,plain,(
% 129.82/18.54 ( ! [X6 : a,X5 : a] : (($true = ((sK4 @ X6))) | ($true != ((sK0 @ X5 @ X6))) | ($true != ((sK4 @ X5)))) ) | spl14_3),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f61,f82])).
% 129.82/18.54 thf(f8513,plain,(
% 129.82/18.54 spl14_6 | spl14_3),
% 129.82/18.54 inference(avatar_split_clause,[],[f8512,f81,f94])).
% 129.82/18.54 thf(f8621,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true != $true) | ($true != ((sK4 @ sK2))) | ($true = ((sK4 @ (sK7 @ X0)))) | ($true = ((X0 @ (sK5 @ X0)))) | ($true = ((X0 @ sK3)))) ) | (spl14_3 | ~spl14_6)),
% 129.82/18.54 inference(constrained_superposition,[],[f95,f2076])).
% 129.82/18.54 thf(f8663,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true != ((sK4 @ sK2))) | ($true = ((sK4 @ (sK7 @ X0)))) | ($true = ((X0 @ (sK5 @ X0)))) | ($true = ((X0 @ sK3)))) ) | (spl14_3 | ~spl14_6)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f8621])).
% 129.82/18.54 thf(f8698,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true = ((sK4 @ (sK7 @ X0)))) | ($true = ((X0 @ (sK5 @ X0)))) | ($true = ((X0 @ sK3)))) ) | (spl14_3 | ~spl14_6 | ~spl14_13)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f8663,f1507])).
% 129.82/18.54 thf(f8928,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK5 @ sK4)))) | ($true = ((sK4 @ sK3))) | ~spl14_20),
% 129.82/18.54 inference(equality_resolution,[],[f8506])).
% 129.82/18.54 thf(f8931,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK5 @ sK4)))) | (spl14_2 | ~spl14_20)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f8928,f78])).
% 129.82/18.54 thf(f8932,plain,(
% 129.82/18.54 spl14_21 | spl14_2 | ~spl14_20),
% 129.82/18.54 inference(avatar_split_clause,[],[f8931,f8505,f76,f8508])).
% 129.82/18.54 thf(f9107,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true != $true) | ($true = ((sK4 @ (sK7 @ X0)))) | ($true = ((X0 @ sK3))) | (((X0 @ (sK5 @ X0))) != ((sK4 @ (sK7 @ X0))))) ) | (spl14_3 | ~spl14_6 | ~spl14_13)),
% 129.82/18.54 inference(equality_factoring,[],[f8698])).
% 129.82/18.54 thf(f9116,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true != $true) | ($true = ((sK4 @ (sK7 @ X0)))) | ($true = ((X0 @ sK3))) | ($false = ((X0 @ (sK5 @ X0)))) | ($false = ((sK4 @ (sK7 @ X0))))) ) | (spl14_3 | ~spl14_6 | ~spl14_13)),
% 129.82/18.54 inference(xor_proxy_clausification,[],[f9107])).
% 129.82/18.54 thf(f9117,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true = ((sK4 @ (sK7 @ X0)))) | ($false = ((X0 @ (sK5 @ X0)))) | ($true = ((X0 @ sK3))) | ($false = ((sK4 @ (sK7 @ X0))))) ) | (spl14_3 | ~spl14_6 | ~spl14_13)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f9116])).
% 129.82/18.54 thf(f9384,plain,(
% 129.82/18.54 ($true != $true) | ($true = ((sK0 @ (sK8 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0)))) @ (sK9 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK2))) | (spl14_3 | ~spl14_16)),
% 129.82/18.54 inference(constrained_superposition,[],[f7489,f2030])).
% 129.82/18.54 thf(f9402,plain,(
% 129.82/18.54 ($true = ((sK0 @ (sK8 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0)))) @ (sK9 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK2))) | (spl14_3 | ~spl14_16)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f9384])).
% 129.82/18.54 thf(f9403,plain,(
% 129.82/18.54 ($true = ((sK0 @ (sK8 @ sK4) @ (sK9 @ sK4)))) | ($true = ((sK4 @ sK2))) | (spl14_3 | ~spl14_16)),
% 129.82/18.54 inference(beta-eta_normalization,[],[f9402])).
% 129.82/18.54 thf(f14034,plain,(
% 129.82/18.54 ($true = $false) | ($true = ((sK4 @ (sK7 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK3))) | ($false = ((sK4 @ (sK7 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | (spl14_3 | ~spl14_6 | ~spl14_13 | ~spl14_21)),
% 129.82/18.54 inference(constrained_superposition,[],[f8510,f9117])).
% 129.82/18.54 thf(f14134,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK7 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK3))) | ($false = ((sK4 @ (sK7 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | (spl14_3 | ~spl14_6 | ~spl14_13 | ~spl14_21)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f14034])).
% 129.82/18.54 thf(f14135,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK7 @ sK4)))) | ($true = ((sK4 @ sK3))) | ($false = ((sK4 @ (sK7 @ sK4)))) | (spl14_3 | ~spl14_6 | ~spl14_13 | ~spl14_21)),
% 129.82/18.54 inference(beta-eta_normalization,[],[f14134])).
% 129.82/18.54 thf(f14469,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK7 @ sK4)))) | ($false = ((sK4 @ (sK7 @ sK4)))) | (spl14_2 | spl14_3 | ~spl14_6 | ~spl14_13 | ~spl14_21)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f14135,f78])).
% 129.82/18.54 thf(f14475,definition,(
% 129.82/18.54 spl14_22 <=> ($false = ((sK4 @ (sK7 @ sK4))))),
% 129.82/18.54 introduced(definition,[new_symbols(definition,[spl14_22])],[avatar_definition])).
% 129.82/18.54 thf(f14476,plain,(
% 129.82/18.54 ($false != ((sK4 @ (sK7 @ sK4)))) | spl14_22),
% 129.82/18.54 inference(avatar_component_clause,[],[f14475])).
% 129.82/18.54 thf(f14477,plain,(
% 129.82/18.54 ($false = ((sK4 @ (sK7 @ sK4)))) | ~spl14_22),
% 129.82/18.54 inference(avatar_component_clause,[],[f14475])).
% 129.82/18.54 thf(f14479,definition,(
% 129.82/18.54 spl14_23 <=> ($true = ((sK4 @ (sK7 @ sK4))))),
% 129.82/18.54 introduced(definition,[new_symbols(definition,[spl14_23])],[avatar_definition])).
% 129.82/18.54 thf(f14480,plain,(
% 129.82/18.54 ($true != ((sK4 @ (sK7 @ sK4)))) | spl14_23),
% 129.82/18.54 inference(avatar_component_clause,[],[f14479])).
% 129.82/18.54 thf(f14481,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK7 @ sK4)))) | ~spl14_23),
% 129.82/18.54 inference(avatar_component_clause,[],[f14479])).
% 129.82/18.54 thf(f14482,plain,(
% 129.82/18.54 spl14_22 | spl14_23 | spl14_2 | spl14_3 | ~spl14_6 | ~spl14_13 | ~spl14_21),
% 129.82/18.54 inference(avatar_split_clause,[],[f14469,f8508,f1505,f94,f81,f76,f14479,f14475])).
% 129.82/18.54 thf(f14498,plain,(
% 129.82/18.54 ($true != $true) | ($true != (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ (sK6 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK3))) | (spl14_3 | ~spl14_23)),
% 129.82/18.54 inference(constrained_superposition,[],[f182,f14481])).
% 129.82/18.54 thf(f14563,plain,(
% 129.82/18.54 ($true != (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ (sK6 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK3))) | (spl14_3 | ~spl14_23)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f14498])).
% 129.82/18.54 thf(f14564,plain,(
% 129.82/18.54 ($true != ((sK4 @ (sK6 @ sK4)))) | ($true = ((sK4 @ sK3))) | (spl14_3 | ~spl14_23)),
% 129.82/18.54 inference(beta-eta_normalization,[],[f14563])).
% 129.82/18.54 thf(f14595,plain,(
% 129.82/18.54 ($true != ((sK4 @ (sK6 @ sK4)))) | (spl14_2 | spl14_3 | ~spl14_23)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f14564,f78])).
% 129.82/18.54 thf(f17494,plain,(
% 129.82/18.54 ( ! [X8 : (a > $o)] : (($true != ((X8 @ (sK7 @ X8)))) | ($true = ((sK0 @ (sK5 @ X8) @ (sK6 @ X8)))) | ($true = ((X8 @ sK3)))) ) | spl14_3),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f45,f82])).
% 129.82/18.54 thf(f17701,plain,(
% 129.82/18.54 ($true != $true) | ($true = ((sK0 @ (sK5 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0)))) @ (sK6 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK3))) | (spl14_3 | ~spl14_23)),
% 129.82/18.54 inference(constrained_superposition,[],[f17494,f14481])).
% 129.82/18.54 thf(f17719,plain,(
% 129.82/18.54 ($true = ((sK0 @ (sK5 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0)))) @ (sK6 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK3))) | (spl14_3 | ~spl14_23)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f17701])).
% 129.82/18.54 thf(f17720,plain,(
% 129.82/18.54 ($true = ((sK0 @ (sK5 @ sK4) @ (sK6 @ sK4)))) | ($true = ((sK4 @ sK3))) | (spl14_3 | ~spl14_23)),
% 129.82/18.54 inference(beta-eta_normalization,[],[f17719])).
% 129.82/18.54 thf(f17943,plain,(
% 129.82/18.54 ($true = ((sK0 @ (sK5 @ sK4) @ (sK6 @ sK4)))) | (spl14_2 | spl14_3 | ~spl14_23)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f17720,f78])).
% 129.82/18.54 thf(f17985,plain,(
% 129.82/18.54 ($true != $true) | ($true != ((sK4 @ (sK5 @ sK4)))) | ($true = ((sK4 @ (sK6 @ sK4)))) | (spl14_2 | spl14_3 | ~spl14_6 | ~spl14_23)),
% 129.82/18.54 inference(constrained_superposition,[],[f95,f17943])).
% 129.82/18.54 thf(f17986,plain,(
% 129.82/18.54 ($true != ((sK4 @ (sK5 @ sK4)))) | ($true = ((sK4 @ (sK6 @ sK4)))) | (spl14_2 | spl14_3 | ~spl14_6 | ~spl14_23)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f17985])).
% 129.82/18.54 thf(f18065,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK6 @ sK4)))) | (spl14_2 | spl14_3 | ~spl14_6 | ~spl14_21 | ~spl14_23)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f17986,f8510])).
% 129.82/18.54 thf(f18066,plain,(
% 129.82/18.54 $false | (spl14_2 | spl14_3 | ~spl14_6 | ~spl14_21 | ~spl14_23)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f18065,f14595])).
% 129.82/18.54 thf(f18067,plain,(
% 129.82/18.54 spl14_2 | spl14_3 | ~spl14_6 | ~spl14_21 | ~spl14_23),
% 129.82/18.54 inference(avatar_contradiction_clause,[],[f18066])).
% 129.82/18.54 thf(f20300,definition,(
% 129.82/18.54 spl14_25 <=> ($true = ((sK4 @ (sK6 @ sK4))))),
% 129.82/18.54 introduced(definition,[new_symbols(definition,[spl14_25])],[avatar_definition])).
% 129.82/18.54 thf(f20301,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK6 @ sK4)))) | ~spl14_25),
% 129.82/18.54 inference(avatar_component_clause,[],[f20300])).
% 129.82/18.54 thf(f20302,plain,(
% 129.82/18.54 ($true != ((sK4 @ (sK6 @ sK4)))) | spl14_25),
% 129.82/18.54 inference(avatar_component_clause,[],[f20300])).
% 129.82/18.54 thf(f20962,definition,(
% 129.82/18.54 spl14_27 <=> ! [X0 : (a > $o)] : (($true = ((X0 @ (sK5 @ X0)))) | ($false = ((X0 @ (sK7 @ X0)))) | ($true = ((X0 @ sK3))))),
% 129.82/18.54 introduced(definition,[new_symbols(definition,[spl14_27])],[avatar_definition])).
% 129.82/18.54 thf(f20963,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true = ((X0 @ (sK5 @ X0)))) | ($false = ((X0 @ (sK7 @ X0)))) | ($true = ((X0 @ sK3)))) ) | ~spl14_27),
% 129.82/18.54 inference(avatar_component_clause,[],[f20962])).
% 129.82/18.54 thf(f29108,definition,(
% 129.82/18.54 spl14_39 <=> ! [X0 : (a > $o)] : (($false = ((X0 @ (sK9 @ X0)))) | ($false = ((X0 @ (sK10 @ X0)))) | ($true = ((X0 @ sK2))))),
% 129.82/18.54 introduced(definition,[new_symbols(definition,[spl14_39])],[avatar_definition])).
% 129.82/18.54 thf(f29109,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($false = ((X0 @ (sK9 @ X0)))) | ($false = ((X0 @ (sK10 @ X0)))) | ($true = ((X0 @ sK2)))) ) | ~spl14_39),
% 129.82/18.54 inference(avatar_component_clause,[],[f29108])).
% 129.82/18.54 thf(f30953,definition,(
% 129.82/18.54 spl14_40 <=> ! [X0 : (a > $o)] : (($true = ((X0 @ sK2))) | ($false = ((X0 @ (sK9 @ X0)))) | ($true = ((sK0 @ sK1 @ (sK10 @ X0)))))),
% 129.82/18.54 introduced(definition,[new_symbols(definition,[spl14_40])],[avatar_definition])).
% 129.82/18.54 thf(f30954,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($false = ((X0 @ (sK9 @ X0)))) | ($true = ((sK0 @ sK1 @ (sK10 @ X0)))) | ($true = ((X0 @ sK2)))) ) | ~spl14_40),
% 129.82/18.54 inference(avatar_component_clause,[],[f30953])).
% 129.82/18.54 thf(f40086,plain,(
% 129.82/18.54 ( ! [X0 : a] : (($true != $true) | ($true = ((sK4 @ X0))) | ($false = ((sK0 @ sK1 @ X0)))) ) | ~spl14_4),
% 129.82/18.54 inference(constrained_superposition,[],[f87,f70])).
% 129.82/18.54 thf(f40088,plain,(
% 129.82/18.54 ( ! [X0 : a,X1 : a] : (($true != $true) | ($true != ((sK4 @ X0))) | ($true = ((sK4 @ X1))) | ($false = ((sK0 @ X0 @ X1)))) ) | ~spl14_6),
% 129.82/18.54 inference(constrained_superposition,[],[f95,f70])).
% 129.82/18.54 thf(f40147,plain,(
% 129.82/18.54 ( ! [X0 : a,X1 : a] : (($true != ((sK4 @ X0))) | ($true = ((sK4 @ X1))) | ($false = ((sK0 @ X0 @ X1)))) ) | ~spl14_6),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f40088])).
% 129.82/18.54 thf(f40149,plain,(
% 129.82/18.54 ( ! [X0 : a] : (($false = ((sK0 @ sK1 @ X0))) | ($true = ((sK4 @ X0)))) ) | ~spl14_4),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f40086])).
% 129.82/18.54 thf(f40835,plain,(
% 129.82/18.54 ( ! [X0 : a] : (($true != $true) | ($true = ((sK4 @ X0))) | ($false = ((sK0 @ (sK5 @ sK4) @ X0)))) ) | (~spl14_6 | ~spl14_21)),
% 129.82/18.54 inference(constrained_superposition,[],[f40147,f8510])).
% 129.82/18.54 thf(f40840,plain,(
% 129.82/18.54 ( ! [X0 : a] : (($true != $true) | ($true = ((sK4 @ X0))) | ($false = ((sK0 @ sK2 @ X0)))) ) | (~spl14_6 | ~spl14_13)),
% 129.82/18.54 inference(constrained_superposition,[],[f40147,f1507])).
% 129.82/18.54 thf(f40848,plain,(
% 129.82/18.54 ( ! [X0 : a] : (($false = ((sK0 @ sK2 @ X0))) | ($true = ((sK4 @ X0)))) ) | (~spl14_6 | ~spl14_13)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f40840])).
% 129.82/18.54 thf(f40850,plain,(
% 129.82/18.54 ( ! [X0 : a] : (($false = ((sK0 @ (sK5 @ sK4) @ X0))) | ($true = ((sK4 @ X0)))) ) | (~spl14_6 | ~spl14_21)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f40835])).
% 129.82/18.54 thf(f43523,plain,(
% 129.82/18.54 ( ! [X12 : (a > $o)] : (($true = ((sK0 @ (sK8 @ X12) @ (sK9 @ X12)))) | ($true = ((X12 @ sK2))) | ($true = ((sK0 @ sK1 @ (sK10 @ X12))))) ) | spl14_3),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f17,f82])).
% 129.82/18.54 thf(f49016,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($false != ((X0 @ sK2))) | ($true = ((sK0 @ sK1 @ (sK10 @ X0)))) | ($true = ((X0 @ sK2))) | ($true != ((X0 @ (sK9 @ X0))))) ) | ~spl14_40),
% 129.82/18.54 inference(equality_factoring,[],[f30954])).
% 129.82/18.54 thf(f50606,plain,(
% 129.82/18.54 ( ! [X8 : (a > $o)] : (($true = ((sK0 @ (sK5 @ X8) @ (sK6 @ X8)))) | ($true = ((X8 @ sK3))) | ($true = ((sK0 @ sK2 @ (sK7 @ X8))))) ) | spl14_3),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f41,f82])).
% 129.82/18.54 thf(f52678,plain,(
% 129.82/18.54 ($true = $false) | ($true = ((sK4 @ (sK6 @ sK4)))) | ($true = ((sK4 @ sK3))) | ($true = ((sK0 @ sK2 @ (sK7 @ sK4)))) | (spl14_3 | ~spl14_6 | ~spl14_21)),
% 129.82/18.54 inference(constrained_superposition,[],[f40850,f50606])).
% 129.82/18.54 thf(f52695,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK6 @ sK4)))) | ($true = ((sK4 @ sK3))) | ($true = ((sK0 @ sK2 @ (sK7 @ sK4)))) | (spl14_3 | ~spl14_6 | ~spl14_21)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f52678])).
% 129.82/18.54 thf(f52833,plain,(
% 129.82/18.54 ($true = ((sK4 @ sK3))) | ($true = ((sK0 @ sK2 @ (sK7 @ sK4)))) | (spl14_3 | ~spl14_6 | ~spl14_21)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f52695,f4065])).
% 129.82/18.54 thf(f52837,plain,(
% 129.82/18.54 ($true = ((sK0 @ sK2 @ (sK7 @ sK4)))) | (spl14_2 | spl14_3 | ~spl14_6 | ~spl14_21)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f52833,f78])).
% 129.82/18.54 thf(f52912,plain,(
% 129.82/18.54 ($true != $true) | ($true != ((sK4 @ sK2))) | ($true = ((sK4 @ (sK7 @ sK4)))) | (spl14_2 | spl14_3 | ~spl14_6 | ~spl14_21)),
% 129.82/18.54 inference(constrained_superposition,[],[f95,f52837])).
% 129.82/18.54 thf(f52926,plain,(
% 129.82/18.54 ($true != ((sK4 @ sK2))) | ($true = ((sK4 @ (sK7 @ sK4)))) | (spl14_2 | spl14_3 | ~spl14_6 | ~spl14_21)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f52912])).
% 129.82/18.54 thf(f53059,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK7 @ sK4)))) | (spl14_2 | spl14_3 | ~spl14_6 | ~spl14_13 | ~spl14_21)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f52926,f1507])).
% 129.82/18.54 thf(f53084,plain,(
% 129.82/18.54 ($true = $false) | (spl14_2 | spl14_3 | ~spl14_6 | ~spl14_13 | ~spl14_21 | ~spl14_22)),
% 129.82/18.54 inference(forward_demodulation,[],[f53059,f14477])).
% 129.82/18.54 thf(f53085,plain,(
% 129.82/18.54 $false | (spl14_2 | spl14_3 | ~spl14_6 | ~spl14_13 | ~spl14_21 | ~spl14_22)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f53084])).
% 129.82/18.54 thf(f53086,plain,(
% 129.82/18.54 spl14_2 | spl14_3 | ~spl14_6 | ~spl14_13 | ~spl14_21 | ~spl14_22),
% 129.82/18.54 inference(avatar_contradiction_clause,[],[f53085])).
% 129.82/18.54 thf(f53141,plain,(
% 129.82/18.54 ($true != $true) | ($false = ((sK4 @ sK2))) | spl14_13),
% 129.82/18.54 inference(constrained_superposition,[],[f1506,f70])).
% 129.82/18.54 thf(f53142,plain,(
% 129.82/18.54 ($false = ((sK4 @ sK2))) | spl14_13),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f53141])).
% 129.82/18.54 thf(f53236,plain,(
% 129.82/18.54 spl14_14 | spl14_13),
% 129.82/18.54 inference(avatar_split_clause,[],[f53142,f1505,f1553])).
% 129.82/18.54 thf(f53522,plain,(
% 129.82/18.54 ( ! [X0 : a] : (($true != $true) | ($true = ((sK4 @ X0))) | ($false = ((sK0 @ (sK8 @ sK4) @ X0)))) ) | (~spl14_6 | ~spl14_12)),
% 129.82/18.54 inference(constrained_superposition,[],[f40147,f1503])).
% 129.82/18.54 thf(f53526,plain,(
% 129.82/18.54 ( ! [X0 : a] : (($false = ((sK0 @ (sK8 @ sK4) @ X0))) | ($true = ((sK4 @ X0)))) ) | (~spl14_6 | ~spl14_12)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f53522])).
% 129.82/18.54 thf(f53704,plain,(
% 129.82/18.54 ($true != $true) | ($false = ((sK4 @ (sK7 @ sK4)))) | spl14_23),
% 129.82/18.54 inference(constrained_superposition,[],[f14480,f70])).
% 129.82/18.54 thf(f53705,plain,(
% 129.82/18.54 ($false = ((sK4 @ (sK7 @ sK4)))) | spl14_23),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f53704])).
% 129.82/18.54 thf(f53796,plain,(
% 129.82/18.54 spl14_22 | spl14_23),
% 129.82/18.54 inference(avatar_split_clause,[],[f53705,f14479,f14475])).
% 129.82/18.54 thf(f55404,plain,(
% 129.82/18.54 ($true = $false) | ($true = ((sK4 @ sK2))) | ($true = ((sK0 @ sK1 @ (sK10 @ sK4)))) | ($true = ((sK4 @ (sK9 @ sK4)))) | (spl14_3 | ~spl14_6 | ~spl14_12)),
% 129.82/18.54 inference(constrained_superposition,[],[f43523,f53526])).
% 129.82/18.54 thf(f55405,plain,(
% 129.82/18.54 ($true = ((sK4 @ sK2))) | ($true = ((sK0 @ sK1 @ (sK10 @ sK4)))) | ($true = ((sK4 @ (sK9 @ sK4)))) | (spl14_3 | ~spl14_6 | ~spl14_12)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f55404])).
% 129.82/18.54 thf(f55534,plain,(
% 129.82/18.54 ($true = ((sK4 @ sK2))) | ($true = ((sK0 @ sK1 @ (sK10 @ sK4)))) | (spl14_3 | ~spl14_6 | ~spl14_12)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f55405,f1551])).
% 129.82/18.54 thf(f55538,plain,(
% 129.82/18.54 ($true = ((sK0 @ sK1 @ (sK10 @ sK4)))) | (spl14_3 | ~spl14_6 | ~spl14_12 | spl14_13)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f55534,f1506])).
% 129.82/18.54 thf(f55601,plain,(
% 129.82/18.54 ($true != $true) | ($true = ((sK4 @ (sK10 @ sK4)))) | (spl14_3 | ~spl14_4 | ~spl14_6 | ~spl14_12 | spl14_13)),
% 129.82/18.54 inference(constrained_superposition,[],[f87,f55538])).
% 129.82/18.54 thf(f55619,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK10 @ sK4)))) | (spl14_3 | ~spl14_4 | ~spl14_6 | ~spl14_12 | spl14_13)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f55601])).
% 129.82/18.54 thf(f55747,plain,(
% 129.82/18.54 ($true = ((sK0 @ (sK8 @ sK4) @ (sK9 @ sK4)))) | (spl14_3 | spl14_13 | ~spl14_16)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f9403,f1506])).
% 129.82/18.54 thf(f55805,plain,(
% 129.82/18.54 ($true = $false) | ($true = ((sK4 @ (sK9 @ sK4)))) | (spl14_3 | ~spl14_6 | ~spl14_12 | spl14_13 | ~spl14_16)),
% 129.82/18.54 inference(constrained_superposition,[],[f53526,f55747])).
% 129.82/18.54 thf(f55814,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK9 @ sK4)))) | (spl14_3 | ~spl14_6 | ~spl14_12 | spl14_13 | ~spl14_16)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f55805])).
% 129.82/18.54 thf(f56157,plain,(
% 129.82/18.54 ($true = $false) | (spl14_3 | ~spl14_4 | ~spl14_6 | ~spl14_12 | spl14_13 | ~spl14_15)),
% 129.82/18.54 inference(forward_demodulation,[],[f55619,f2026])).
% 129.82/18.54 thf(f56158,plain,(
% 129.82/18.54 $false | (spl14_3 | ~spl14_4 | ~spl14_6 | ~spl14_12 | spl14_13 | ~spl14_15)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f56157])).
% 129.82/18.54 thf(f56159,plain,(
% 129.82/18.54 spl14_3 | ~spl14_4 | ~spl14_6 | ~spl14_12 | spl14_13 | ~spl14_15),
% 129.82/18.54 inference(avatar_contradiction_clause,[],[f56158])).
% 129.82/18.54 thf(f56237,plain,(
% 129.82/18.54 ($true != $true) | ($false = ((sK4 @ (sK5 @ sK4)))) | spl14_21),
% 129.82/18.54 inference(constrained_superposition,[],[f8509,f70])).
% 129.82/18.54 thf(f56238,plain,(
% 129.82/18.54 ($false = ((sK4 @ (sK5 @ sK4)))) | spl14_21),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f56237])).
% 129.82/18.54 thf(f56341,plain,(
% 129.82/18.54 ($true = $false) | ($false = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ (sK7 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK3))) | (spl14_21 | ~spl14_27)),
% 129.82/18.54 inference(constrained_superposition,[],[f56238,f20963])).
% 129.82/18.54 thf(f56528,plain,(
% 129.82/18.54 ($false = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ (sK7 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK3))) | (spl14_21 | ~spl14_27)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f56341])).
% 129.82/18.54 thf(f56529,plain,(
% 129.82/18.54 ($false = ((sK4 @ (sK7 @ sK4)))) | ($true = ((sK4 @ sK3))) | (spl14_21 | ~spl14_27)),
% 129.82/18.54 inference(beta-eta_normalization,[],[f56528])).
% 129.82/18.54 thf(f56867,plain,(
% 129.82/18.54 ($true != $true) | ($true != (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ (sK10 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK2))) | (spl14_3 | ~spl14_6 | ~spl14_10 | ~spl14_12 | spl14_13 | ~spl14_16)),
% 129.82/18.54 inference(constrained_superposition,[],[f146,f55814])).
% 129.82/18.54 thf(f56945,plain,(
% 129.82/18.54 ($true != (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ (sK10 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK2))) | (spl14_3 | ~spl14_6 | ~spl14_10 | ~spl14_12 | spl14_13 | ~spl14_16)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f56867])).
% 129.82/18.54 thf(f56946,plain,(
% 129.82/18.54 ($true != ((sK4 @ (sK10 @ sK4)))) | ($true = ((sK4 @ sK2))) | (spl14_3 | ~spl14_6 | ~spl14_10 | ~spl14_12 | spl14_13 | ~spl14_16)),
% 129.82/18.54 inference(beta-eta_normalization,[],[f56945])).
% 129.82/18.54 thf(f57019,plain,(
% 129.82/18.54 ($true = ((sK4 @ sK2))) | (spl14_3 | ~spl14_6 | ~spl14_10 | ~spl14_12 | spl14_13 | ~spl14_16)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f56946,f2030])).
% 129.82/18.54 thf(f57024,plain,(
% 129.82/18.54 $false | (spl14_3 | ~spl14_6 | ~spl14_10 | ~spl14_12 | spl14_13 | ~spl14_16)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f57019,f1506])).
% 129.82/18.54 thf(f57025,plain,(
% 129.82/18.54 spl14_3 | ~spl14_6 | ~spl14_10 | ~spl14_12 | spl14_13 | ~spl14_16),
% 129.82/18.54 inference(avatar_contradiction_clause,[],[f57024])).
% 129.82/18.54 thf(f57037,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true != ((X0 @ (sK9 @ X0)))) | ($true = ((X0 @ sK2))) | ($true = ((sK0 @ sK1 @ (sK10 @ X0))))) ) | ~spl14_40),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f49016,f70])).
% 129.82/18.54 thf(f66257,plain,(
% 129.82/18.54 ( ! [X12 : (a > $o)] : (($true != ((X12 @ (sK10 @ X12)))) | ($true = ((sK0 @ (sK8 @ X12) @ (sK9 @ X12)))) | ($true = ((X12 @ sK2)))) ) | ~spl14_1),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f24,f73])).
% 129.82/18.54 thf(f66353,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true != $true) | ($true = ((sK0 @ (sK8 @ X0) @ (sK9 @ X0)))) | ($true = ((X0 @ sK2))) | ($false = ((X0 @ (sK10 @ X0))))) ) | ~spl14_1),
% 129.82/18.54 inference(constrained_superposition,[],[f66257,f70])).
% 129.82/18.54 thf(f66356,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true = ((sK0 @ (sK8 @ X0) @ (sK9 @ X0)))) | ($true = ((X0 @ sK2))) | ($false = ((X0 @ (sK10 @ X0))))) ) | ~spl14_1),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f66353])).
% 129.82/18.54 thf(f66622,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true != $true) | ($true != ((sK4 @ (sK8 @ X0)))) | ($true = ((sK4 @ (sK9 @ X0)))) | ($true = ((X0 @ sK2))) | ($false = ((X0 @ (sK10 @ X0))))) ) | (~spl14_1 | ~spl14_6)),
% 129.82/18.54 inference(constrained_superposition,[],[f95,f66356])).
% 129.82/18.54 thf(f66633,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true != ((sK4 @ (sK8 @ X0)))) | ($true = ((sK4 @ (sK9 @ X0)))) | ($true = ((X0 @ sK2))) | ($false = ((X0 @ (sK10 @ X0))))) ) | (~spl14_1 | ~spl14_6)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f66622])).
% 129.82/18.54 thf(f66759,plain,(
% 129.82/18.54 ( ! [X12 : (a > $o)] : (($true != ((X12 @ (sK9 @ X12)))) | ($true = ((X12 @ sK2))) | ($true = ((sK0 @ sK1 @ (sK10 @ X12))))) ) | ~spl14_1),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f28,f73])).
% 129.82/18.54 thf(f67579,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($false != ((X0 @ sK2))) | ($false = ((X0 @ (sK10 @ X0)))) | ($true = ((X0 @ sK2))) | ($true != ((X0 @ (sK9 @ X0))))) ) | ~spl14_39),
% 129.82/18.54 inference(equality_factoring,[],[f29109])).
% 129.82/18.54 thf(f67892,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true != ((X0 @ (sK9 @ X0)))) | ($true = ((X0 @ sK2))) | ($false = ((X0 @ (sK10 @ X0))))) ) | ~spl14_39),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f67579,f70])).
% 129.82/18.54 thf(f69835,plain,(
% 129.82/18.54 ($true != $true) | ($true = ((sK4 @ (sK9 @ sK4)))) | ($true = ((sK4 @ sK2))) | ($false = ((sK4 @ (sK10 @ sK4)))) | (~spl14_1 | ~spl14_6 | ~spl14_12)),
% 129.82/18.54 inference(constrained_superposition,[],[f66633,f1503])).
% 129.82/18.54 thf(f69838,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK9 @ sK4)))) | ($true = ((sK4 @ sK2))) | ($false = ((sK4 @ (sK10 @ sK4)))) | (~spl14_1 | ~spl14_6 | ~spl14_12)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f69835])).
% 129.82/18.54 thf(f69895,plain,(
% 129.82/18.54 ($true = ((sK4 @ sK2))) | ($false = ((sK4 @ (sK10 @ sK4)))) | (~spl14_1 | ~spl14_6 | ~spl14_12 | ~spl14_39)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f69838,f67892])).
% 129.82/18.54 thf(f73722,plain,(
% 129.82/18.54 ( ! [X12 : (a > $o)] : (($true = ((sK0 @ (sK8 @ X12) @ (sK9 @ X12)))) | ($true = ((X12 @ sK2))) | ($true = ((sK0 @ sK1 @ (sK10 @ X12))))) ) | ~spl14_1),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f20,f73])).
% 129.82/18.54 thf(f73788,plain,(
% 129.82/18.54 ($true = $false) | ($true = ((sK4 @ (sK9 @ sK4)))) | ($true = ((sK4 @ sK2))) | ($true = ((sK0 @ sK1 @ (sK10 @ sK4)))) | (~spl14_1 | ~spl14_6 | ~spl14_12)),
% 129.82/18.54 inference(constrained_superposition,[],[f53526,f73722])).
% 129.82/18.54 thf(f73799,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK9 @ sK4)))) | ($true = ((sK4 @ sK2))) | ($true = ((sK0 @ sK1 @ (sK10 @ sK4)))) | (~spl14_1 | ~spl14_6 | ~spl14_12)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f73788])).
% 129.82/18.54 thf(f73923,plain,(
% 129.82/18.54 ($true = ((sK4 @ sK2))) | ($true = ((sK0 @ sK1 @ (sK10 @ sK4)))) | (~spl14_1 | ~spl14_6 | ~spl14_12)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f73799,f66759])).
% 129.82/18.54 thf(f73926,plain,(
% 129.82/18.54 ($true = ((sK0 @ sK1 @ (sK10 @ sK4)))) | (~spl14_1 | ~spl14_6 | ~spl14_12 | spl14_13)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f73923,f1506])).
% 129.82/18.54 thf(f73928,plain,(
% 129.82/18.54 ($true = $false) | ($true = ((sK4 @ (sK10 @ sK4)))) | (~spl14_1 | ~spl14_4 | ~spl14_6 | ~spl14_12 | spl14_13)),
% 129.82/18.54 inference(constrained_superposition,[],[f73926,f40149])).
% 129.82/18.54 thf(f74084,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK10 @ sK4)))) | (~spl14_1 | ~spl14_4 | ~spl14_6 | ~spl14_12 | spl14_13)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f73928])).
% 129.82/18.54 thf(f74093,plain,(
% 129.82/18.54 $false | (~spl14_1 | ~spl14_4 | ~spl14_6 | ~spl14_12 | spl14_13 | spl14_16)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f74084,f2029])).
% 129.82/18.54 thf(f74094,plain,(
% 129.82/18.54 ~spl14_1 | ~spl14_4 | ~spl14_6 | ~spl14_12 | spl14_13 | spl14_16),
% 129.82/18.54 inference(avatar_contradiction_clause,[],[f74093])).
% 129.82/18.54 thf(f77698,plain,(
% 129.82/18.54 ( ! [X14 : (a > $o)] : (($true = (((^[Y0 : a]: (~ (X14 @ Y0))) @ (sK9 @ (^[Y0 : a]: (~ ((^[Y1 : a]: (~ (X14 @ Y1))) @ Y0))))))) | ($true = (((^[Y0 : a]: (~ (X14 @ Y0))) @ (sK10 @ (^[Y0 : a]: (~ ((^[Y1 : a]: (~ (X14 @ Y1))) @ Y0))))))) | ($false = (((^[Y0 : a]: (~ (X14 @ Y0))) @ sK2)))) ) | ~spl14_10),
% 129.82/18.54 inference(primitive_instantiation,[],[f159])).
% 129.82/18.54 thf(f78149,plain,(
% 129.82/18.54 ( ! [X14 : (a > $o)] : (($true = ((~ (X14 @ (sK9 @ (^[Y0 : a]: (~ (~ (X14 @ Y0))))))))) | ($true = ((~ (X14 @ (sK10 @ (^[Y0 : a]: (~ (~ (X14 @ Y0))))))))) | ($false = ((~ (X14 @ sK2))))) ) | ~spl14_10),
% 129.82/18.54 inference(beta-eta_normalization,[],[f77698])).
% 129.82/18.54 thf(f78150,plain,(
% 129.82/18.54 ( ! [X14 : (a > $o)] : (($false = ((X14 @ (sK9 @ (^[Y0 : a]: (~ (~ (X14 @ Y0)))))))) | ($true = ((~ (X14 @ (sK10 @ (^[Y0 : a]: (~ (~ (X14 @ Y0))))))))) | ($false = ((~ (X14 @ sK2))))) ) | ~spl14_10),
% 129.82/18.54 inference(not_proxy_clausification,[],[f78149])).
% 129.82/18.54 thf(f78151,plain,(
% 129.82/18.54 ( ! [X14 : (a > $o)] : (($false = ((X14 @ (sK9 @ (^[Y0 : a]: (~ (~ (X14 @ Y0)))))))) | ($false = ((X14 @ (sK10 @ (^[Y0 : a]: (~ (~ (X14 @ Y0)))))))) | ($false = ((~ (X14 @ sK2))))) ) | ~spl14_10),
% 129.82/18.54 inference(not_proxy_clausification,[],[f78150])).
% 129.82/18.54 thf(f78152,plain,(
% 129.82/18.54 ( ! [X14 : (a > $o)] : (($false = ((X14 @ (sK9 @ (^[Y0 : a]: (~ (~ (X14 @ Y0)))))))) | ($false = ((X14 @ (sK10 @ (^[Y0 : a]: (~ (~ (X14 @ Y0)))))))) | ($true = ((X14 @ sK2)))) ) | ~spl14_10),
% 129.82/18.54 inference(not_proxy_clausification,[],[f78151])).
% 129.82/18.54 thf(f78153,plain,(
% 129.82/18.54 ( ! [X14 : (a > $o)] : (($false = ((X14 @ (sK9 @ (^[Y0 : a]: (X14 @ Y0)))))) | ($false = ((X14 @ (sK10 @ (^[Y0 : a]: (~ (~ (X14 @ Y0)))))))) | ($true = ((X14 @ sK2)))) ) | ~spl14_10),
% 129.82/18.54 inference(boolean_simplification,[],[f78152])).
% 129.82/18.54 thf(f78154,plain,(
% 129.82/18.54 ( ! [X14 : (a > $o)] : (($false = ((X14 @ (sK9 @ X14)))) | ($false = ((X14 @ (sK10 @ (^[Y0 : a]: (~ (~ (X14 @ Y0)))))))) | ($true = ((X14 @ sK2)))) ) | ~spl14_10),
% 129.82/18.54 inference(beta-eta_normalization,[],[f78153])).
% 129.82/18.54 thf(f78155,plain,(
% 129.82/18.54 ( ! [X14 : (a > $o)] : (($false = ((X14 @ (sK9 @ X14)))) | ($false = ((X14 @ (sK10 @ (^[Y0 : a]: (X14 @ Y0)))))) | ($true = ((X14 @ sK2)))) ) | ~spl14_10),
% 129.82/18.54 inference(boolean_simplification,[],[f78154])).
% 129.82/18.54 thf(f78156,plain,(
% 129.82/18.54 ( ! [X14 : (a > $o)] : (($false = ((X14 @ (sK9 @ X14)))) | ($false = ((X14 @ (sK10 @ X14)))) | ($true = ((X14 @ sK2)))) ) | ~spl14_10),
% 129.82/18.54 inference(beta-eta_normalization,[],[f78155])).
% 129.82/18.54 thf(f78210,definition,(
% 129.82/18.54 spl14_60 <=> ! [X0 : a] : (($false = ((sK0 @ sK2 @ X0))) | ($true = ((sK4 @ X0))))),
% 129.82/18.54 introduced(definition,[new_symbols(definition,[spl14_60])],[avatar_definition])).
% 129.82/18.54 thf(f78211,plain,(
% 129.82/18.54 ( ! [X0 : a] : (($false = ((sK0 @ sK2 @ X0))) | ($true = ((sK4 @ X0)))) ) | ~spl14_60),
% 129.82/18.54 inference(avatar_component_clause,[],[f78210])).
% 129.82/18.54 thf(f80774,definition,(
% 129.82/18.54 spl14_61 <=> ! [X12 : (a > $o)] : (($true = ((X12 @ sK2))) | ($true = ((sK0 @ sK1 @ (sK10 @ X12)))) | ($true = ((X12 @ (sK8 @ X12)))))),
% 129.82/18.54 introduced(definition,[new_symbols(definition,[spl14_61])],[avatar_definition])).
% 129.82/18.54 thf(f80775,plain,(
% 129.82/18.54 ( ! [X12 : (a > $o)] : (($true = ((sK0 @ sK1 @ (sK10 @ X12)))) | ($true = ((X12 @ (sK8 @ X12)))) | ($true = ((X12 @ sK2)))) ) | ~spl14_61),
% 129.82/18.54 inference(avatar_component_clause,[],[f80774])).
% 129.82/18.54 thf(f80776,plain,(
% 129.82/18.54 spl14_5 | spl14_61),
% 129.82/18.54 inference(avatar_split_clause,[],[f10,f80774,f90])).
% 129.82/18.54 thf(f91046,definition,(
% 129.82/18.54 spl14_63 <=> ! [X12 : (a > $o)] : (($true = ((X12 @ sK2))) | ($true != ((X12 @ (sK10 @ X12)))) | ($true = ((sK0 @ (sK8 @ X12) @ (sK9 @ X12)))))),
% 129.82/18.54 introduced(definition,[new_symbols(definition,[spl14_63])],[avatar_definition])).
% 129.82/18.54 thf(f91047,plain,(
% 129.82/18.54 ( ! [X12 : (a > $o)] : (($true != ((X12 @ (sK10 @ X12)))) | ($true = ((X12 @ sK2))) | ($true = ((sK0 @ (sK8 @ X12) @ (sK9 @ X12))))) ) | ~spl14_63),
% 129.82/18.54 inference(avatar_component_clause,[],[f91046])).
% 129.82/18.54 thf(f91048,plain,(
% 129.82/18.54 spl14_5 | spl14_63),
% 129.82/18.54 inference(avatar_split_clause,[],[f22,f91046,f90])).
% 129.82/18.54 thf(f91186,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true != $true) | ($true = ((X0 @ sK2))) | ($true = ((sK0 @ (sK8 @ X0) @ (sK9 @ X0)))) | ($false = ((X0 @ (sK10 @ X0))))) ) | ~spl14_63),
% 129.82/18.54 inference(constrained_superposition,[],[f91047,f70])).
% 129.82/18.54 thf(f91189,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true = ((sK0 @ (sK8 @ X0) @ (sK9 @ X0)))) | ($true = ((X0 @ sK2))) | ($false = ((X0 @ (sK10 @ X0))))) ) | ~spl14_63),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f91186])).
% 129.82/18.54 thf(f91550,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true != $true) | ($true != ((sK4 @ (sK8 @ X0)))) | ($true = ((sK4 @ (sK9 @ X0)))) | ($true = ((X0 @ sK2))) | ($false = ((X0 @ (sK10 @ X0))))) ) | (~spl14_6 | ~spl14_63)),
% 129.82/18.54 inference(constrained_superposition,[],[f95,f91189])).
% 129.82/18.54 thf(f91561,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true != ((sK4 @ (sK8 @ X0)))) | ($true = ((sK4 @ (sK9 @ X0)))) | ($true = ((X0 @ sK2))) | ($false = ((X0 @ (sK10 @ X0))))) ) | (~spl14_6 | ~spl14_63)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f91550])).
% 129.82/18.54 thf(f91765,plain,(
% 129.82/18.54 ($true != $true) | ($true = ((sK4 @ (sK9 @ sK4)))) | ($true = ((sK4 @ sK2))) | ($false = ((sK4 @ (sK10 @ sK4)))) | (~spl14_6 | ~spl14_12 | ~spl14_63)),
% 129.82/18.54 inference(constrained_superposition,[],[f91561,f1503])).
% 129.82/18.54 thf(f91768,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK9 @ sK4)))) | ($true = ((sK4 @ sK2))) | ($false = ((sK4 @ (sK10 @ sK4)))) | (~spl14_6 | ~spl14_12 | ~spl14_63)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f91765])).
% 129.82/18.54 thf(f91845,plain,(
% 129.82/18.54 ($true = ((sK4 @ sK2))) | ($false = ((sK4 @ (sK10 @ sK4)))) | (~spl14_6 | ~spl14_12 | ~spl14_39 | ~spl14_63)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f91768,f67892])).
% 129.82/18.54 thf(f103565,definition,(
% 129.82/18.54 spl14_67 <=> ! [X12 : (a > $o)] : (($true = ((X12 @ sK2))) | ($true = ((sK0 @ sK1 @ (sK10 @ X12)))) | ($true = ((sK0 @ (sK8 @ X12) @ (sK9 @ X12)))))),
% 129.82/18.54 introduced(definition,[new_symbols(definition,[spl14_67])],[avatar_definition])).
% 129.82/18.54 thf(f103566,plain,(
% 129.82/18.54 ( ! [X12 : (a > $o)] : (($true = ((sK0 @ (sK8 @ X12) @ (sK9 @ X12)))) | ($true = ((sK0 @ sK1 @ (sK10 @ X12)))) | ($true = ((X12 @ sK2)))) ) | ~spl14_67),
% 129.82/18.54 inference(avatar_component_clause,[],[f103565])).
% 129.82/18.54 thf(f103567,plain,(
% 129.82/18.54 spl14_5 | spl14_67),
% 129.82/18.54 inference(avatar_split_clause,[],[f18,f103565,f90])).
% 129.82/18.54 thf(f103661,plain,(
% 129.82/18.54 ($true = $false) | ($true = ((sK4 @ (sK9 @ sK4)))) | ($true = ((sK0 @ sK1 @ (sK10 @ sK4)))) | ($true = ((sK4 @ sK2))) | (~spl14_6 | ~spl14_12 | ~spl14_67)),
% 129.82/18.54 inference(constrained_superposition,[],[f53526,f103566])).
% 129.82/18.54 thf(f103676,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK9 @ sK4)))) | ($true = ((sK0 @ sK1 @ (sK10 @ sK4)))) | ($true = ((sK4 @ sK2))) | (~spl14_6 | ~spl14_12 | ~spl14_67)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f103661])).
% 129.82/18.54 thf(f103849,plain,(
% 129.82/18.54 ($true = ((sK0 @ sK1 @ (sK10 @ sK4)))) | ($true = ((sK4 @ sK2))) | (~spl14_6 | ~spl14_12 | ~spl14_40 | ~spl14_67)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f103676,f57037])).
% 129.82/18.54 thf(f103853,plain,(
% 129.82/18.54 ($true = ((sK0 @ sK1 @ (sK10 @ sK4)))) | (~spl14_6 | ~spl14_12 | spl14_13 | ~spl14_40 | ~spl14_67)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f103849,f1506])).
% 129.82/18.54 thf(f103855,plain,(
% 129.82/18.54 ($true = $false) | ($true = ((sK4 @ (sK10 @ sK4)))) | (~spl14_4 | ~spl14_6 | ~spl14_12 | spl14_13 | ~spl14_40 | ~spl14_67)),
% 129.82/18.54 inference(constrained_superposition,[],[f103853,f40149])).
% 129.82/18.54 thf(f104090,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK10 @ sK4)))) | (~spl14_4 | ~spl14_6 | ~spl14_12 | spl14_13 | ~spl14_40 | ~spl14_67)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f103855])).
% 129.82/18.54 thf(f104103,plain,(
% 129.82/18.54 $false | (~spl14_4 | ~spl14_6 | ~spl14_12 | spl14_13 | spl14_16 | ~spl14_40 | ~spl14_67)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f104090,f2029])).
% 129.82/18.54 thf(f104104,plain,(
% 129.82/18.54 ~spl14_4 | ~spl14_6 | ~spl14_12 | spl14_13 | spl14_16 | ~spl14_40 | ~spl14_67),
% 129.82/18.54 inference(avatar_contradiction_clause,[],[f104103])).
% 129.82/18.54 thf(f104432,definition,(
% 129.82/18.54 spl14_68 <=> ($true = ((sK0 @ sK1 @ (sK10 @ sK4))))),
% 129.82/18.54 introduced(definition,[new_symbols(definition,[spl14_68])],[avatar_definition])).
% 129.82/18.54 thf(f104434,plain,(
% 129.82/18.54 ($true = ((sK0 @ sK1 @ (sK10 @ sK4)))) | ~spl14_68),
% 129.82/18.54 inference(avatar_component_clause,[],[f104432])).
% 129.82/18.54 thf(f105435,definition,(
% 129.82/18.54 spl14_72 <=> ! [X12 : (a > $o)] : (($true = ((X12 @ sK2))) | ($true = ((sK0 @ sK1 @ (sK10 @ X12)))) | ($true != ((X12 @ (sK9 @ X12)))))),
% 129.82/18.54 introduced(definition,[new_symbols(definition,[spl14_72])],[avatar_definition])).
% 129.82/18.54 thf(f105436,plain,(
% 129.82/18.54 ( ! [X12 : (a > $o)] : (($true != ((X12 @ (sK9 @ X12)))) | ($true = ((sK0 @ sK1 @ (sK10 @ X12)))) | ($true = ((X12 @ sK2)))) ) | ~spl14_72),
% 129.82/18.54 inference(avatar_component_clause,[],[f105435])).
% 129.82/18.54 thf(f105437,plain,(
% 129.82/18.54 spl14_5 | spl14_72),
% 129.82/18.54 inference(avatar_split_clause,[],[f26,f105435,f90])).
% 129.82/18.54 thf(f105581,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true != $true) | ($true = ((sK0 @ sK1 @ (sK10 @ X0)))) | ($true = ((X0 @ sK2))) | ($false = ((X0 @ (sK9 @ X0))))) ) | ~spl14_72),
% 129.82/18.54 inference(constrained_superposition,[],[f105436,f70])).
% 129.82/18.54 thf(f105584,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true = ((sK0 @ sK1 @ (sK10 @ X0)))) | ($true = ((X0 @ sK2))) | ($false = ((X0 @ (sK9 @ X0))))) ) | ~spl14_72),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f105581])).
% 129.82/18.54 thf(f105891,plain,(
% 129.82/18.54 ($true = $false) | ($true = ((sK4 @ (sK10 @ sK4)))) | (~spl14_4 | ~spl14_68)),
% 129.82/18.54 inference(constrained_superposition,[],[f104434,f40149])).
% 129.82/18.54 thf(f106076,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK10 @ sK4)))) | (~spl14_4 | ~spl14_68)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f105891])).
% 129.82/18.54 thf(f106089,plain,(
% 129.82/18.54 $false | (~spl14_4 | spl14_16 | ~spl14_68)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f106076,f2029])).
% 129.82/18.54 thf(f106090,plain,(
% 129.82/18.54 ~spl14_4 | spl14_16 | ~spl14_68),
% 129.82/18.54 inference(avatar_contradiction_clause,[],[f106089])).
% 129.82/18.54 thf(f106092,plain,(
% 129.82/18.54 ($true = $false) | (~spl14_15 | ~spl14_16)),
% 129.82/18.54 inference(forward_demodulation,[],[f2030,f2026])).
% 129.82/18.54 thf(f106093,plain,(
% 129.82/18.54 $false | (~spl14_15 | ~spl14_16)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f106092])).
% 129.82/18.54 thf(f106094,plain,(
% 129.82/18.54 ~spl14_15 | ~spl14_16),
% 129.82/18.54 inference(avatar_contradiction_clause,[],[f106093])).
% 129.82/18.54 thf(f106153,plain,(
% 129.82/18.54 ($false = ((sK4 @ (sK10 @ sK4)))) | (~spl14_6 | ~spl14_12 | spl14_13 | ~spl14_39 | ~spl14_63)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f91845,f1506])).
% 129.82/18.54 thf(f106169,plain,(
% 129.82/18.54 spl14_15 | ~spl14_6 | ~spl14_12 | spl14_13 | ~spl14_39 | ~spl14_63),
% 129.82/18.54 inference(avatar_split_clause,[],[f106153,f91046,f29108,f1505,f1501,f94,f2024])).
% 129.82/18.54 thf(f106600,plain,(
% 129.82/18.54 spl14_5 | spl14_10),
% 129.82/18.54 inference(avatar_split_clause,[],[f30,f145,f90])).
% 129.82/18.54 thf(f106713,plain,(
% 129.82/18.54 ($false = ((sK4 @ (sK10 @ sK4)))) | (~spl14_1 | ~spl14_6 | ~spl14_12 | spl14_13 | ~spl14_39)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f69895,f1506])).
% 129.82/18.54 thf(f107171,plain,(
% 129.82/18.54 ( ! [X7 : a] : (($true = ((sK4 @ X7))) | ($true != ((sK0 @ sK1 @ X7)))) ) | ~spl14_1),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f60,f73])).
% 129.82/18.54 thf(f107172,plain,(
% 129.82/18.54 spl14_15 | ~spl14_1 | ~spl14_6 | ~spl14_12 | spl14_13 | ~spl14_39),
% 129.82/18.54 inference(avatar_split_clause,[],[f106713,f29108,f1505,f1501,f94,f72,f2024])).
% 129.82/18.54 thf(f107321,plain,(
% 129.82/18.54 spl14_4 | ~spl14_1),
% 129.82/18.54 inference(avatar_split_clause,[],[f107171,f72,f86])).
% 129.82/18.54 thf(f107509,plain,(
% 129.82/18.54 ($true != $true) | ($true = ((sK0 @ sK1 @ (sK10 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK2))) | (spl14_12 | ~spl14_61)),
% 129.82/18.54 inference(constrained_superposition,[],[f1502,f80775])).
% 129.82/18.54 thf(f107577,plain,(
% 129.82/18.54 ($true = ((sK0 @ sK1 @ (sK10 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK2))) | (spl14_12 | ~spl14_61)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f107509])).
% 129.82/18.54 thf(f107578,plain,(
% 129.82/18.54 ($true = ((sK0 @ sK1 @ (sK10 @ sK4)))) | ($true = ((sK4 @ sK2))) | (spl14_12 | ~spl14_61)),
% 129.82/18.54 inference(beta-eta_normalization,[],[f107577])).
% 129.82/18.54 thf(f107591,plain,(
% 129.82/18.54 ($true = ((sK0 @ sK1 @ (sK10 @ sK4)))) | (spl14_12 | spl14_13 | ~spl14_61)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f107578,f1506])).
% 129.82/18.54 thf(f108159,plain,(
% 129.82/18.54 spl14_68 | spl14_12 | spl14_13 | ~spl14_61),
% 129.82/18.54 inference(avatar_split_clause,[],[f107591,f80774,f1505,f1501,f104432])).
% 129.82/18.54 thf(f109596,plain,(
% 129.82/18.54 ( ! [X12 : (a > $o)] : (($true = ((X12 @ sK2))) | ($true = ((X12 @ (sK8 @ X12)))) | ($true = ((sK0 @ sK1 @ (sK10 @ X12))))) ) | ~spl14_1),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f12,f73])).
% 129.82/18.54 thf(f109712,plain,(
% 129.82/18.54 spl14_39 | ~spl14_10),
% 129.82/18.54 inference(avatar_split_clause,[],[f78156,f145,f29108])).
% 129.82/18.54 thf(f109713,plain,(
% 129.82/18.54 spl14_61 | ~spl14_1),
% 129.82/18.54 inference(avatar_split_clause,[],[f109596,f72,f80774])).
% 129.82/18.54 thf(f111348,plain,(
% 129.82/18.54 spl14_60 | ~spl14_6 | ~spl14_13),
% 129.82/18.54 inference(avatar_split_clause,[],[f40848,f1505,f94,f78210])).
% 129.82/18.54 thf(f112471,definition,(
% 129.82/18.54 spl14_74 <=> ! [X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true != ((X8 @ (sK7 @ X8)))) | ($true = ((X8 @ (sK5 @ X8)))))),
% 129.82/18.54 introduced(definition,[new_symbols(definition,[spl14_74])],[avatar_definition])).
% 129.82/18.54 thf(f112472,plain,(
% 129.82/18.54 ( ! [X8 : (a > $o)] : (($true != ((X8 @ (sK7 @ X8)))) | ($true = ((X8 @ sK3))) | ($true = ((X8 @ (sK5 @ X8))))) ) | ~spl14_74),
% 129.82/18.54 inference(avatar_component_clause,[],[f112471])).
% 129.82/18.54 thf(f112473,plain,(
% 129.82/18.54 spl14_5 | spl14_74),
% 129.82/18.54 inference(avatar_split_clause,[],[f38,f112471,f90])).
% 129.82/18.54 thf(f112848,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true != $true) | ($true = ((X0 @ sK3))) | ($true = ((X0 @ (sK5 @ X0)))) | ($false = ((X0 @ (sK7 @ X0))))) ) | ~spl14_74),
% 129.82/18.54 inference(constrained_superposition,[],[f112472,f70])).
% 129.82/18.54 thf(f112852,plain,(
% 129.82/18.54 ( ! [X0 : (a > $o)] : (($true = ((X0 @ sK3))) | ($true = ((X0 @ (sK5 @ X0)))) | ($false = ((X0 @ (sK7 @ X0))))) ) | ~spl14_74),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f112848])).
% 129.82/18.54 thf(f113161,definition,(
% 129.82/18.54 spl14_75 <=> ! [X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true != ((X8 @ (sK7 @ X8)))) | ($true != ((X8 @ (sK6 @ X8)))))),
% 129.82/18.54 introduced(definition,[new_symbols(definition,[spl14_75])],[avatar_definition])).
% 129.82/18.54 thf(f113162,plain,(
% 129.82/18.54 ( ! [X8 : (a > $o)] : (($true != ((X8 @ (sK6 @ X8)))) | ($true != ((X8 @ (sK7 @ X8)))) | ($true = ((X8 @ sK3)))) ) | ~spl14_75),
% 129.82/18.54 inference(avatar_component_clause,[],[f113161])).
% 129.82/18.54 thf(f113163,plain,(
% 129.82/18.54 spl14_5 | spl14_75),
% 129.82/18.54 inference(avatar_split_clause,[],[f54,f113161,f90])).
% 129.82/18.54 thf(f113517,definition,(
% 129.82/18.54 spl14_76 <=> ! [X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true = ((sK0 @ sK2 @ (sK7 @ X8)))) | ($true = ((X8 @ (sK5 @ X8)))))),
% 129.82/18.54 introduced(definition,[new_symbols(definition,[spl14_76])],[avatar_definition])).
% 129.82/18.54 thf(f113518,plain,(
% 129.82/18.54 ( ! [X8 : (a > $o)] : (($true = ((sK0 @ sK2 @ (sK7 @ X8)))) | ($true = ((X8 @ (sK5 @ X8)))) | ($true = ((X8 @ sK3)))) ) | ~spl14_76),
% 129.82/18.54 inference(avatar_component_clause,[],[f113517])).
% 129.82/18.54 thf(f113519,plain,(
% 129.82/18.54 spl14_5 | spl14_76),
% 129.82/18.54 inference(avatar_split_clause,[],[f34,f113517,f90])).
% 129.82/18.54 thf(f114043,plain,(
% 129.82/18.54 spl14_27 | ~spl14_74),
% 129.82/18.54 inference(avatar_split_clause,[],[f112852,f112471,f20962])).
% 129.82/18.54 thf(f114417,plain,(
% 129.82/18.54 ($true != $true) | ($true = ((sK0 @ sK2 @ (sK7 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK3))) | (spl14_21 | ~spl14_76)),
% 129.82/18.54 inference(constrained_superposition,[],[f8509,f113518])).
% 129.82/18.54 thf(f114525,plain,(
% 129.82/18.54 ($true = ((sK0 @ sK2 @ (sK7 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK3))) | (spl14_21 | ~spl14_76)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f114417])).
% 129.82/18.54 thf(f114526,plain,(
% 129.82/18.54 ($true = ((sK0 @ sK2 @ (sK7 @ sK4)))) | ($true = ((sK4 @ sK3))) | (spl14_21 | ~spl14_76)),
% 129.82/18.54 inference(beta-eta_normalization,[],[f114525])).
% 129.82/18.54 thf(f114824,plain,(
% 129.82/18.54 ($true = ((sK0 @ sK2 @ (sK7 @ sK4)))) | (spl14_2 | spl14_21 | ~spl14_76)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f114526,f78])).
% 129.82/18.54 thf(f114849,plain,(
% 129.82/18.54 ($true = $false) | ($true = ((sK4 @ (sK7 @ sK4)))) | (spl14_2 | spl14_21 | ~spl14_60 | ~spl14_76)),
% 129.82/18.54 inference(constrained_superposition,[],[f114824,f78211])).
% 129.82/18.54 thf(f114885,plain,(
% 129.82/18.54 ($true != $true) | ($true != ((sK4 @ sK2))) | ($true = ((sK4 @ (sK7 @ sK4)))) | (spl14_2 | ~spl14_6 | spl14_21 | ~spl14_76)),
% 129.82/18.54 inference(constrained_superposition,[],[f95,f114824])).
% 129.82/18.54 thf(f114886,plain,(
% 129.82/18.54 ($true != ((sK4 @ sK2))) | ($true = ((sK4 @ (sK7 @ sK4)))) | (spl14_2 | ~spl14_6 | spl14_21 | ~spl14_76)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f114885])).
% 129.82/18.54 thf(f114952,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK7 @ sK4)))) | (spl14_2 | spl14_21 | ~spl14_60 | ~spl14_76)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f114849])).
% 129.82/18.54 thf(f114953,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK7 @ sK4)))) | (spl14_2 | ~spl14_6 | ~spl14_13 | spl14_21 | ~spl14_76)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f114886,f1507])).
% 129.82/18.54 thf(f114962,plain,(
% 129.82/18.54 ($true = $false) | (spl14_2 | spl14_21 | ~spl14_22 | ~spl14_60 | ~spl14_76)),
% 129.82/18.54 inference(forward_demodulation,[],[f114952,f14477])).
% 129.82/18.54 thf(f114963,plain,(
% 129.82/18.54 $false | (spl14_2 | spl14_21 | ~spl14_22 | ~spl14_60 | ~spl14_76)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f114962])).
% 129.82/18.54 thf(f114964,plain,(
% 129.82/18.54 spl14_2 | spl14_21 | ~spl14_22 | ~spl14_60 | ~spl14_76),
% 129.82/18.54 inference(avatar_contradiction_clause,[],[f114963])).
% 129.82/18.54 thf(f114965,plain,(
% 129.82/18.54 ($true = $false) | (spl14_2 | ~spl14_6 | ~spl14_13 | spl14_21 | ~spl14_22 | ~spl14_76)),
% 129.82/18.54 inference(forward_demodulation,[],[f114953,f14477])).
% 129.82/18.54 thf(f114966,plain,(
% 129.82/18.54 $false | (spl14_2 | ~spl14_6 | ~spl14_13 | spl14_21 | ~spl14_22 | ~spl14_76)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f114965])).
% 129.82/18.54 thf(f114967,plain,(
% 129.82/18.54 spl14_2 | ~spl14_6 | ~spl14_13 | spl14_21 | ~spl14_22 | ~spl14_76),
% 129.82/18.54 inference(avatar_contradiction_clause,[],[f114966])).
% 129.82/18.54 thf(f115590,definition,(
% 129.82/18.54 spl14_77 <=> ! [X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true = ((sK0 @ sK2 @ (sK7 @ X8)))) | ($true != ((X8 @ (sK6 @ X8)))))),
% 129.82/18.54 introduced(definition,[new_symbols(definition,[spl14_77])],[avatar_definition])).
% 129.82/18.54 thf(f115591,plain,(
% 129.82/18.54 ( ! [X8 : (a > $o)] : (($true != ((X8 @ (sK6 @ X8)))) | ($true = ((sK0 @ sK2 @ (sK7 @ X8)))) | ($true = ((X8 @ sK3)))) ) | ~spl14_77),
% 129.82/18.54 inference(avatar_component_clause,[],[f115590])).
% 129.82/18.54 thf(f115592,plain,(
% 129.82/18.54 spl14_5 | spl14_77),
% 129.82/18.54 inference(avatar_split_clause,[],[f50,f115590,f90])).
% 129.82/18.54 thf(f119941,definition,(
% 129.82/18.54 spl14_78 <=> ! [X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true != ((X8 @ (sK7 @ X8)))) | ($true = ((sK0 @ (sK5 @ X8) @ (sK6 @ X8)))))),
% 129.82/18.54 introduced(definition,[new_symbols(definition,[spl14_78])],[avatar_definition])).
% 129.82/18.54 thf(f119942,plain,(
% 129.82/18.54 ( ! [X8 : (a > $o)] : (($true != ((X8 @ (sK7 @ X8)))) | ($true = ((X8 @ sK3))) | ($true = ((sK0 @ (sK5 @ X8) @ (sK6 @ X8))))) ) | ~spl14_78),
% 129.82/18.54 inference(avatar_component_clause,[],[f119941])).
% 129.82/18.54 thf(f119943,plain,(
% 129.82/18.54 spl14_5 | spl14_78),
% 129.82/18.54 inference(avatar_split_clause,[],[f46,f119941,f90])).
% 129.82/18.54 thf(f121459,plain,(
% 129.82/18.54 ($true != $true) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK3))) | ($true = ((sK0 @ (sK5 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0)))) @ (sK6 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | (~spl14_23 | ~spl14_78)),
% 129.82/18.54 inference(constrained_superposition,[],[f119942,f14481])).
% 129.82/18.54 thf(f121501,plain,(
% 129.82/18.54 ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK3))) | ($true = ((sK0 @ (sK5 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0)))) @ (sK6 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | (~spl14_23 | ~spl14_78)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f121459])).
% 129.82/18.54 thf(f121502,plain,(
% 129.82/18.54 ($true = ((sK4 @ sK3))) | ($true = ((sK0 @ (sK5 @ sK4) @ (sK6 @ sK4)))) | (~spl14_23 | ~spl14_78)),
% 129.82/18.54 inference(beta-eta_normalization,[],[f121501])).
% 129.82/18.54 thf(f121700,plain,(
% 129.82/18.54 ($true = ((sK0 @ (sK5 @ sK4) @ (sK6 @ sK4)))) | (spl14_2 | ~spl14_23 | ~spl14_78)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f121502,f78])).
% 129.82/18.54 thf(f121761,plain,(
% 129.82/18.54 ($true != $true) | ($true != ((sK4 @ (sK5 @ sK4)))) | ($true = ((sK4 @ (sK6 @ sK4)))) | (spl14_2 | ~spl14_6 | ~spl14_23 | ~spl14_78)),
% 129.82/18.54 inference(constrained_superposition,[],[f95,f121700])).
% 129.82/18.54 thf(f121762,plain,(
% 129.82/18.54 ($true != ((sK4 @ (sK5 @ sK4)))) | ($true = ((sK4 @ (sK6 @ sK4)))) | (spl14_2 | ~spl14_6 | ~spl14_23 | ~spl14_78)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f121761])).
% 129.82/18.54 thf(f121848,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK6 @ sK4)))) | (spl14_2 | ~spl14_6 | ~spl14_21 | ~spl14_23 | ~spl14_78)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f121762,f8510])).
% 129.82/18.54 thf(f121856,plain,(
% 129.82/18.54 $false | (spl14_2 | ~spl14_6 | ~spl14_21 | ~spl14_23 | spl14_25 | ~spl14_78)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f121848,f20302])).
% 129.82/18.54 thf(f121857,plain,(
% 129.82/18.54 spl14_2 | ~spl14_6 | ~spl14_21 | ~spl14_23 | spl14_25 | ~spl14_78),
% 129.82/18.54 inference(avatar_contradiction_clause,[],[f121856])).
% 129.82/18.54 thf(f121879,plain,(
% 129.82/18.54 ($true != $true) | ($true != (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ (sK7 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK3))) | (~spl14_25 | ~spl14_75)),
% 129.82/18.54 inference(constrained_superposition,[],[f113162,f20301])).
% 129.82/18.54 thf(f121973,plain,(
% 129.82/18.54 ($true != (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ (sK7 @ (^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = (((^[Y0 : a]: (sK4 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ sK3))) | (~spl14_25 | ~spl14_75)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f121879])).
% 129.82/18.54 thf(f121974,plain,(
% 129.82/18.54 ($true != ((sK4 @ (sK7 @ sK4)))) | ($true = ((sK4 @ sK3))) | (~spl14_25 | ~spl14_75)),
% 129.82/18.54 inference(beta-eta_normalization,[],[f121973])).
% 129.82/18.54 thf(f122007,plain,(
% 129.82/18.54 ($true = ((sK4 @ sK3))) | (~spl14_23 | ~spl14_25 | ~spl14_75)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f121974,f14481])).
% 129.82/18.54 thf(f122010,plain,(
% 129.82/18.54 $false | (spl14_2 | ~spl14_23 | ~spl14_25 | ~spl14_75)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f122007,f78])).
% 129.82/18.54 thf(f122011,plain,(
% 129.82/18.54 spl14_2 | ~spl14_23 | ~spl14_25 | ~spl14_75),
% 129.82/18.54 inference(avatar_contradiction_clause,[],[f122010])).
% 129.82/18.54 thf(f123248,plain,(
% 129.82/18.54 spl14_40 | ~spl14_72),
% 129.82/18.54 inference(avatar_split_clause,[],[f105584,f105435,f30953])).
% 129.82/18.54 thf(f130511,definition,(
% 129.82/18.54 spl14_79 <=> ! [X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true = ((sK0 @ sK2 @ (sK7 @ X8)))) | ($true = ((sK0 @ (sK5 @ X8) @ (sK6 @ X8)))))),
% 129.82/18.54 introduced(definition,[new_symbols(definition,[spl14_79])],[avatar_definition])).
% 129.82/18.54 thf(f130512,plain,(
% 129.82/18.54 ( ! [X8 : (a > $o)] : (($true = ((sK0 @ (sK5 @ X8) @ (sK6 @ X8)))) | ($true = ((sK0 @ sK2 @ (sK7 @ X8)))) | ($true = ((X8 @ sK3)))) ) | ~spl14_79),
% 129.82/18.54 inference(avatar_component_clause,[],[f130511])).
% 129.82/18.54 thf(f130513,plain,(
% 129.82/18.54 spl14_5 | spl14_79),
% 129.82/18.54 inference(avatar_split_clause,[],[f42,f130511,f90])).
% 129.82/18.54 thf(f133580,plain,(
% 129.82/18.54 ($true = $false) | ($true = ((sK4 @ (sK6 @ sK4)))) | ($true = ((sK0 @ sK2 @ (sK7 @ sK4)))) | ($true = ((sK4 @ sK3))) | (~spl14_6 | ~spl14_21 | ~spl14_79)),
% 129.82/18.54 inference(constrained_superposition,[],[f40850,f130512])).
% 129.82/18.54 thf(f133591,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK6 @ sK4)))) | ($true = ((sK0 @ sK2 @ (sK7 @ sK4)))) | ($true = ((sK4 @ sK3))) | (~spl14_6 | ~spl14_21 | ~spl14_79)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f133580])).
% 129.82/18.54 thf(f133729,plain,(
% 129.82/18.54 ($true = ((sK0 @ sK2 @ (sK7 @ sK4)))) | ($true = ((sK4 @ sK3))) | (~spl14_6 | ~spl14_21 | ~spl14_77 | ~spl14_79)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f133591,f115591])).
% 129.82/18.54 thf(f133732,plain,(
% 129.82/18.54 ($true = ((sK0 @ sK2 @ (sK7 @ sK4)))) | (spl14_2 | ~spl14_6 | ~spl14_21 | ~spl14_77 | ~spl14_79)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f133729,f78])).
% 129.82/18.54 thf(f133734,plain,(
% 129.82/18.54 ($true = $false) | ($true = ((sK4 @ (sK7 @ sK4)))) | (spl14_2 | ~spl14_6 | ~spl14_21 | ~spl14_60 | ~spl14_77 | ~spl14_79)),
% 129.82/18.54 inference(constrained_superposition,[],[f133732,f78211])).
% 129.82/18.54 thf(f133795,plain,(
% 129.82/18.54 ($true != $true) | ($true != ((sK4 @ sK2))) | ($true = ((sK4 @ (sK7 @ sK4)))) | (spl14_2 | ~spl14_6 | ~spl14_21 | ~spl14_77 | ~spl14_79)),
% 129.82/18.54 inference(constrained_superposition,[],[f95,f133732])).
% 129.82/18.54 thf(f133796,plain,(
% 129.82/18.54 ($true != ((sK4 @ sK2))) | ($true = ((sK4 @ (sK7 @ sK4)))) | (spl14_2 | ~spl14_6 | ~spl14_21 | ~spl14_77 | ~spl14_79)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f133795])).
% 129.82/18.54 thf(f133909,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK7 @ sK4)))) | (spl14_2 | ~spl14_6 | ~spl14_21 | ~spl14_60 | ~spl14_77 | ~spl14_79)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f133734])).
% 129.82/18.54 thf(f133910,plain,(
% 129.82/18.54 ($true = ((sK4 @ (sK7 @ sK4)))) | (spl14_2 | ~spl14_6 | ~spl14_13 | ~spl14_21 | ~spl14_77 | ~spl14_79)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f133796,f1507])).
% 129.82/18.54 thf(f133919,plain,(
% 129.82/18.54 ($true = $false) | (spl14_2 | ~spl14_6 | ~spl14_21 | ~spl14_22 | ~spl14_60 | ~spl14_77 | ~spl14_79)),
% 129.82/18.54 inference(forward_demodulation,[],[f133909,f14477])).
% 129.82/18.54 thf(f133920,plain,(
% 129.82/18.54 $false | (spl14_2 | ~spl14_6 | ~spl14_21 | ~spl14_22 | ~spl14_60 | ~spl14_77 | ~spl14_79)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f133919])).
% 129.82/18.54 thf(f133921,plain,(
% 129.82/18.54 spl14_2 | ~spl14_6 | ~spl14_21 | ~spl14_22 | ~spl14_60 | ~spl14_77 | ~spl14_79),
% 129.82/18.54 inference(avatar_contradiction_clause,[],[f133920])).
% 129.82/18.54 thf(f133922,plain,(
% 129.82/18.54 ($true = $false) | (spl14_2 | ~spl14_6 | ~spl14_13 | ~spl14_21 | ~spl14_22 | ~spl14_77 | ~spl14_79)),
% 129.82/18.54 inference(forward_demodulation,[],[f133910,f14477])).
% 129.82/18.54 thf(f133923,plain,(
% 129.82/18.54 $false | (spl14_2 | ~spl14_6 | ~spl14_13 | ~spl14_21 | ~spl14_22 | ~spl14_77 | ~spl14_79)),
% 129.82/18.54 inference(trivial_inequality_removal,[],[f133922])).
% 129.82/18.54 thf(f133924,plain,(
% 129.82/18.54 spl14_2 | ~spl14_6 | ~spl14_13 | ~spl14_21 | ~spl14_22 | ~spl14_77 | ~spl14_79),
% 129.82/18.54 inference(avatar_contradiction_clause,[],[f133923])).
% 129.82/18.54 thf(f134620,plain,(
% 129.82/18.54 ( ! [X21 : a] : (($true = ((sK13 @ X21))) | ($true != ((sK0 @ sK11 @ X21)))) ) | ~spl14_2),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f66,f77])).
% 129.82/18.54 thf(f134621,plain,(
% 129.82/18.54 spl14_5 | ~spl14_2),
% 129.82/18.54 inference(avatar_split_clause,[],[f134620,f76,f90])).
% 129.82/18.54 thf(f135660,plain,(
% 129.82/18.54 ( ! [X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true != ((X8 @ (sK6 @ X8)))) | ($true = ((sK0 @ sK2 @ (sK7 @ X8))))) ) | ~spl14_1),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f52,f73])).
% 129.82/18.54 thf(f135945,plain,(
% 129.82/18.54 spl14_77 | ~spl14_1),
% 129.82/18.54 inference(avatar_split_clause,[],[f135660,f72,f115590])).
% 129.82/18.54 thf(f135994,plain,(
% 129.82/18.54 ( ! [X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true = ((sK0 @ (sK5 @ X8) @ (sK6 @ X8)))) | ($true = ((sK0 @ sK2 @ (sK7 @ X8))))) ) | ~spl14_1),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f44,f73])).
% 129.82/18.54 thf(f136705,plain,(
% 129.82/18.54 spl14_79 | ~spl14_1),
% 129.82/18.54 inference(avatar_split_clause,[],[f135994,f72,f130511])).
% 129.82/18.54 thf(f136766,plain,(
% 129.82/18.54 ( ! [X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true != ((X8 @ (sK6 @ X8)))) | ($true != ((X8 @ (sK7 @ X8))))) ) | ~spl14_1),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f56,f73])).
% 129.82/18.54 thf(f137145,plain,(
% 129.82/18.54 spl14_75 | ~spl14_1),
% 129.82/18.54 inference(avatar_split_clause,[],[f136766,f72,f113161])).
% 129.82/18.54 thf(f137153,plain,(
% 129.82/18.54 ( ! [X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true = ((sK0 @ (sK5 @ X8) @ (sK6 @ X8)))) | ($true != ((X8 @ (sK7 @ X8))))) ) | ~spl14_1),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f48,f73])).
% 129.82/18.54 thf(f137991,plain,(
% 129.82/18.54 spl14_78 | ~spl14_1),
% 129.82/18.54 inference(avatar_split_clause,[],[f137153,f72,f119941])).
% 129.82/18.54 thf(f138005,plain,(
% 129.82/18.54 ($false = ((sK4 @ (sK7 @ sK4)))) | (spl14_2 | spl14_21 | ~spl14_27)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f56529,f78])).
% 129.82/18.54 thf(f138022,plain,(
% 129.82/18.54 ( ! [X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true = ((X8 @ (sK5 @ X8)))) | ($true = ((sK0 @ sK2 @ (sK7 @ X8))))) ) | ~spl14_1),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f36,f73])).
% 129.82/18.54 thf(f138325,plain,(
% 129.82/18.54 spl14_76 | ~spl14_1),
% 129.82/18.54 inference(avatar_split_clause,[],[f138022,f72,f113517])).
% 129.82/18.54 thf(f138511,plain,(
% 129.82/18.54 ( ! [X8 : (a > $o)] : (($true = ((X8 @ sK3))) | ($true = ((X8 @ (sK5 @ X8)))) | ($true != ((X8 @ (sK7 @ X8))))) ) | ~spl14_1),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f40,f73])).
% 129.82/18.54 thf(f138669,plain,(
% 129.82/18.54 $false | (spl14_2 | spl14_21 | spl14_22 | ~spl14_27)),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f138005,f14476])).
% 129.82/18.54 thf(f138670,plain,(
% 129.82/18.54 spl14_2 | spl14_21 | spl14_22 | ~spl14_27),
% 129.82/18.54 inference(avatar_contradiction_clause,[],[f138669])).
% 129.82/18.54 thf(f138773,plain,(
% 129.82/18.54 spl14_74 | ~spl14_1),
% 129.82/18.54 inference(avatar_split_clause,[],[f138511,f72,f112471])).
% 129.82/18.54 thf(f138799,plain,(
% 129.82/18.54 ( ! [X6 : a,X5 : a] : (($true = ((sK4 @ X6))) | ($true != ((sK0 @ X5 @ X6))) | ($true != ((sK4 @ X5)))) ) | ~spl14_1),
% 129.82/18.54 inference(forward_subsumption_resolution,[],[f64,f73])).
% 129.82/18.54 thf(f138892,plain,(
% 129.82/18.54 spl14_6 | ~spl14_1),
% 129.82/18.54 inference(avatar_split_clause,[],[f138799,f72,f94])).
% 129.82/18.54 cnf(s1, plain, ~spl14_1 | ~spl14_2, inference(sat_conversion,[],[f79])).
% 129.82/18.54 cnf(s2, plain, ~spl14_2 | spl14_3, inference(sat_conversion,[],[f84])).
% 129.82/18.54 cnf(s3, plain, spl14_3 | spl14_4, inference(sat_conversion,[],[f88])).
% 129.82/18.54 cnf(s4, plain, spl14_4 | spl14_5, inference(sat_conversion,[],[f92])).
% 129.82/18.54 cnf(s5, plain, spl14_5 | spl14_6, inference(sat_conversion,[],[f96])).
% 129.82/18.54 cnf(s6, plain, spl14_1 | ~spl14_3 | ~spl14_5, inference(sat_conversion,[],[f100])).
% 129.82/18.54 cnf(s8, plain, spl14_5 | spl14_9, inference(sat_conversion,[],[f115])).
% 129.82/18.54 cnf(s9, plain, spl14_3 | spl14_9, inference(sat_conversion,[],[f117])).
% 129.82/18.54 cnf(s10, plain, ~spl14_1 | spl14_9, inference(sat_conversion,[],[f125])).
% 129.82/18.54 cnf(s11, plain, ~spl14_1 | spl14_10, inference(sat_conversion,[],[f147])).
% 129.82/18.54 cnf(s12, plain, spl14_3 | spl14_10, inference(sat_conversion,[],[f149])).
% 129.82/18.54 cnf(s15, plain, spl14_3 | ~spl14_4 | ~spl14_12 | ~spl14_14 | spl14_15 | spl14_16, inference(sat_conversion,[],[f2031])).
% 129.82/18.54 cnf(s21, plain, spl14_3 | ~spl14_4 | spl14_12 | ~spl14_14 | spl14_16, inference(sat_conversion,[],[f6383])).
% 129.82/18.54 cnf(s22, plain, ~spl14_9 | spl14_12 | ~spl14_14 | ~spl14_16, inference(sat_conversion,[],[f6516])).
% 129.82/18.54 cnf(s23, plain, ~spl14_9 | spl14_12 | spl14_13 | ~spl14_16, inference(sat_conversion,[],[f6518])).
% 129.82/18.54 cnf(s24, plain, spl14_2 | spl14_3 | ~spl14_6 | ~spl14_13 | spl14_20 | spl14_21, inference(sat_conversion,[],[f8511])).
% 129.82/18.54 cnf(s25, plain, spl14_3 | spl14_6, inference(sat_conversion,[],[f8513])).
% 129.82/18.54 cnf(s26, plain, spl14_2 | ~spl14_20 | spl14_21, inference(sat_conversion,[],[f8932])).
% 129.82/18.54 cnf(s30, plain, spl14_2 | spl14_3 | ~spl14_6 | ~spl14_13 | ~spl14_21 | spl14_22 | spl14_23, inference(sat_conversion,[],[f14482])).
% 129.82/18.54 cnf(s31, plain, spl14_2 | spl14_3 | ~spl14_6 | ~spl14_21 | ~spl14_23, inference(sat_conversion,[],[f18067])).
% 129.82/18.54 cnf(s56, plain, spl14_2 | spl14_3 | ~spl14_6 | ~spl14_13 | ~spl14_21 | ~spl14_22, inference(sat_conversion,[],[f53086])).
% 129.82/18.54 cnf(s57, plain, spl14_13 | spl14_14, inference(sat_conversion,[],[f53236])).
% 129.82/18.54 cnf(s58, plain, spl14_22 | spl14_23, inference(sat_conversion,[],[f53796])).
% 129.82/18.54 cnf(s62, plain, spl14_3 | ~spl14_4 | ~spl14_6 | ~spl14_12 | spl14_13 | ~spl14_15, inference(sat_conversion,[],[f56159])).
% 129.82/18.54 cnf(s64, plain, spl14_3 | ~spl14_6 | ~spl14_10 | ~spl14_12 | spl14_13 | ~spl14_16, inference(sat_conversion,[],[f57025])).
% 129.82/18.54 cnf(s87, plain, ~spl14_1 | ~spl14_4 | ~spl14_6 | ~spl14_12 | spl14_13 | spl14_16, inference(sat_conversion,[],[f74094])).
% 129.82/18.54 cnf(s100, plain, spl14_5 | spl14_61, inference(sat_conversion,[],[f80776])).
% 129.82/18.54 cnf(s102, plain, spl14_5 | spl14_63, inference(sat_conversion,[],[f91048])).
% 129.82/18.54 cnf(s105, plain, spl14_5 | spl14_67, inference(sat_conversion,[],[f103567])).
% 129.82/18.54 cnf(s108, plain, ~spl14_4 | ~spl14_6 | ~spl14_12 | spl14_13 | spl14_16 | ~spl14_40 | ~spl14_67, inference(sat_conversion,[],[f104104])).
% 129.82/18.54 cnf(s115, plain, spl14_5 | spl14_72, inference(sat_conversion,[],[f105437])).
% 129.82/18.54 cnf(s119, plain, ~spl14_4 | spl14_16 | ~spl14_68, inference(sat_conversion,[],[f106090])).
% 129.82/18.54 cnf(s120, plain, ~spl14_15 | ~spl14_16, inference(sat_conversion,[],[f106094])).
% 129.82/18.54 cnf(s127, plain, ~spl14_6 | ~spl14_12 | spl14_13 | spl14_15 | ~spl14_39 | ~spl14_63, inference(sat_conversion,[],[f106169])).
% 129.82/18.54 cnf(s130, plain, spl14_5 | spl14_10, inference(sat_conversion,[],[f106600])).
% 129.82/18.54 cnf(s132, plain, ~spl14_1 | ~spl14_6 | ~spl14_12 | spl14_13 | spl14_15 | ~spl14_39, inference(sat_conversion,[],[f107172])).
% 129.82/18.54 cnf(s134, plain, ~spl14_1 | spl14_4, inference(sat_conversion,[],[f107321])).
% 129.82/18.54 cnf(s137, plain, spl14_12 | spl14_13 | ~spl14_61 | spl14_68, inference(sat_conversion,[],[f108159])).
% 129.82/18.54 cnf(s140, plain, ~spl14_10 | spl14_39, inference(sat_conversion,[],[f109712])).
% 129.82/18.54 cnf(s142, plain, ~spl14_1 | spl14_61, inference(sat_conversion,[],[f109713])).
% 129.82/18.54 cnf(s151, plain, ~spl14_6 | ~spl14_13 | spl14_60, inference(sat_conversion,[],[f111348])).
% 129.82/18.54 cnf(s158, plain, spl14_5 | spl14_74, inference(sat_conversion,[],[f112473])).
% 129.82/18.54 cnf(s160, plain, spl14_5 | spl14_75, inference(sat_conversion,[],[f113163])).
% 129.82/18.54 cnf(s161, plain, spl14_5 | spl14_76, inference(sat_conversion,[],[f113519])).
% 129.82/18.54 cnf(s162, plain, spl14_27 | ~spl14_74, inference(sat_conversion,[],[f114043])).
% 129.82/18.54 cnf(s164, plain, spl14_2 | spl14_21 | ~spl14_22 | ~spl14_60 | ~spl14_76, inference(sat_conversion,[],[f114964])).
% 129.82/18.54 cnf(s165, plain, spl14_2 | ~spl14_6 | ~spl14_13 | spl14_21 | ~spl14_22 | ~spl14_76, inference(sat_conversion,[],[f114967])).
% 129.82/18.54 cnf(s166, plain, spl14_5 | spl14_77, inference(sat_conversion,[],[f115592])).
% 129.82/18.54 cnf(s170, plain, spl14_5 | spl14_78, inference(sat_conversion,[],[f119943])).
% 129.82/18.54 cnf(s173, plain, spl14_2 | ~spl14_6 | ~spl14_21 | ~spl14_23 | spl14_25 | ~spl14_78, inference(sat_conversion,[],[f121857])).
% 129.82/18.54 cnf(s174, plain, spl14_2 | ~spl14_23 | ~spl14_25 | ~spl14_75, inference(sat_conversion,[],[f122011])).
% 129.82/18.54 cnf(s178, plain, spl14_40 | ~spl14_72, inference(sat_conversion,[],[f123248])).
% 129.82/18.54 cnf(s180, plain, spl14_5 | spl14_79, inference(sat_conversion,[],[f130513])).
% 129.82/18.54 cnf(s182, plain, spl14_2 | ~spl14_6 | ~spl14_21 | ~spl14_22 | ~spl14_60 | ~spl14_77 | ~spl14_79, inference(sat_conversion,[],[f133921])).
% 129.82/18.54 cnf(s183, plain, spl14_2 | ~spl14_6 | ~spl14_13 | ~spl14_21 | ~spl14_22 | ~spl14_77 | ~spl14_79, inference(sat_conversion,[],[f133924])).
% 129.82/18.54 cnf(s184, plain, ~spl14_2 | spl14_5, inference(sat_conversion,[],[f134621])).
% 129.82/18.54 cnf(s185, plain, ~spl14_1 | spl14_77, inference(sat_conversion,[],[f135945])).
% 129.82/18.54 cnf(s186, plain, ~spl14_1 | spl14_79, inference(sat_conversion,[],[f136705])).
% 129.82/18.54 cnf(s190, plain, ~spl14_1 | spl14_75, inference(sat_conversion,[],[f137145])).
% 129.82/18.54 cnf(s191, plain, ~spl14_1 | spl14_78, inference(sat_conversion,[],[f137991])).
% 129.82/18.54 cnf(s192, plain, ~spl14_1 | spl14_76, inference(sat_conversion,[],[f138325])).
% 129.82/18.54 cnf(s193, plain, spl14_2 | spl14_21 | spl14_22 | ~spl14_27, inference(sat_conversion,[],[f138670])).
% 129.82/18.54 cnf(s194, plain, ~spl14_1 | spl14_74, inference(sat_conversion,[],[f138773])).
% 129.82/18.54 cnf(s195, plain, ~spl14_1 | spl14_6, inference(sat_conversion,[],[f138892])).
% 129.82/18.54 cnf(s200, plain, spl14_21 | ~spl14_13 | spl14_5 | ~spl14_6 | spl14_2, inference(rat,[],[s165,s193,s161,s162,s158])).
% 129.82/18.54 cnf(s202, plain, ~spl14_12 | spl14_13 | spl14_3, inference(rat,[],[s15,s62,s64,s25,s12,s3,s57])).
% 129.82/18.54 cnf(s203, plain, spl14_13 | spl14_3, inference(rat,[],[s21,s22,s202,s57,s9,s3])).
% 129.82/18.54 cnf(s204, plain, ~spl14_21 | spl14_3 | spl14_2, inference(rat,[],[s30,s56,s31,s25,s203])).
% 129.82/18.54 cnf(s205, plain, spl14_3 | spl14_2, inference(rat,[],[s24,s26,s204,s203,s25])).
% 129.82/18.54 cnf(s206, plain, ~spl14_13 | spl14_5 | spl14_2, inference(rat,[],[s173,s174,s58,s182,s200,s151,s180,s170,s166,s160,s5])).
% 129.82/18.54 cnf(s207, plain, spl14_12 | spl14_13 | ~spl14_4 | ~spl14_9 | ~spl14_61, inference(rat,[],[s119,s23,s137])).
% 129.82/18.54 cnf(s208, plain, spl14_2 | spl14_1, inference(rat,[],[s120,s108,s127,s207,s206,s178,s140,s4,s5,s8,s100,s102,s105,s115,s130,s6,s205])).
% 129.82/18.54 cnf(s209, plain, spl14_1, inference(rat,[],[s6,s2,s184,s208])).
% 129.82/18.54 cnf(s210, plain, spl14_6, inference(rat,[],[s195,s209])).
% 129.82/18.54 cnf(s211, plain, spl14_74, inference(rat,[],[s194,s209])).
% 129.82/18.54 cnf(s212, plain, spl14_76, inference(rat,[],[s192,s209])).
% 129.82/18.54 cnf(s213, plain, spl14_78, inference(rat,[],[s191,s209])).
% 129.82/18.54 cnf(s214, plain, spl14_75, inference(rat,[],[s190,s209])).
% 129.82/18.54 cnf(s215, plain, spl14_79, inference(rat,[],[s186,s209])).
% 129.82/18.54 cnf(s216, plain, spl14_77, inference(rat,[],[s185,s209])).
% 129.82/18.54 cnf(s217, plain, spl14_61, inference(rat,[],[s142,s209])).
% 129.82/18.54 cnf(s218, plain, spl14_4, inference(rat,[],[s134,s209])).
% 129.82/18.54 cnf(s220, plain, spl14_10, inference(rat,[],[s11,s209])).
% 129.82/18.54 cnf(s221, plain, spl14_9, inference(rat,[],[s10,s209])).
% 129.82/18.54 cnf(s222, plain, ~spl14_2, inference(rat,[],[s1,s209])).
% 129.82/18.54 cnf(s223, plain, spl14_27, inference(rat,[],[s162,s211])).
% 129.82/18.54 cnf(s224, plain, spl14_39, inference(rat,[],[s140,s220])).
% 129.82/18.54 cnf(s227, plain, ~spl14_21 | ~spl14_13, inference(rat,[],[s173,s174,s58,s183,s215,s216,s214,s213,s222,s210])).
% 129.82/18.54 cnf(s228, plain, spl14_21 | ~spl14_60, inference(rat,[],[s193,s164,s212,s223,s222])).
% 129.82/18.54 cnf(s229, plain, ~spl14_13, inference(rat,[],[s228,s227,s151,s210])).
% 129.82/18.54 cnf(s231, plain, spl14_12, inference(rat,[],[s207,s217,s221,s218,s229])).
% 129.82/18.54 cnf(s232, plain, spl14_15, inference(rat,[],[s132,s224,s229,s210,s209,s231])).
% 129.82/18.54 cnf(s233, plain, spl14_16, inference(rat,[],[s87,s229,s218,s209,s210,s231])).
% 129.82/18.54 cnf(s236, plain, $false, inference(rat,[],[s120,s233,s232])).
% 129.82/18.54 thf(f138893,plain,(
% 129.82/18.54 $false),
% 129.82/18.54 inference(avatar_sat_refutation,[],[s236])).
% 129.82/18.54 % SZS output end Proof for theBenchmark
% 129.82/18.54 % (4122081)------------------------------
% 129.82/18.54 % (4122081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 129.82/18.54 % (4122081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.82/18.54 % (4122081)CaDiCaL version: 2.1.3
% 129.82/18.54 % (4122081)Termination reason: Refutation
% 129.82/18.54 % (4122081)Time elapsed: 7.407 s
% 129.82/18.54 % (4122081)Peak memory usage: 45 MB
% 129.82/18.54 % (4122081)Instructions burned: 15860 (million)
% 129.82/18.54 % (4121966)Success in time 18.308 s
% 129.82/18.54 % Vampire exiting
%------------------------------------------------------------------------------