%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU558^2 : TPTP v9.3.1. Bugfixed v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n016.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:32:26 AM UTC 2026
% Result : Theorem 283.22s 40.34s
% Output : Refutation 283.22s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU558^2 : TPTP v9.3.1. Bugfixed v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 % Computer : n016.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Tue Sep 29 13:55:05 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.24 Running first-order model finding
% 0.09/0.24 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
% 7.44/1.43 % (388350)Will run a generic schedule for satisfiability detection.
% 7.44/1.43 % (388355)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3586659422_2999 on theBenchmark for (2999ds/0Mi)
% 7.44/1.43 % (388357)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1195695164:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.44/1.43 % Exception at run slice level
% 7.44/1.43 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.44/1.43 % (388361)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=353633437:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.44/1.43 % (388356)% WARNING: option uhcvi not known.
% 7.44/1.43 % (388364)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2958359424:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 7.44/1.43 % (388358)dis+10_1_sil=32000:sp=arity:random_seed=2715559970:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.44/1.43 % Exception at run slice level
% 7.44/1.43 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.44/1.43 % (388356)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1469734284:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.44/1.43 % (388356)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.44/1.43 % (388356)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 7.44/1.43 % (388369)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=50795529:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 7.44/1.43 % (388359)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=299758775:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.44/1.43 % (388359)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.44/1.43 % (388360)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1568234206:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.44/1.43 % (388361)Instruction limit reached!
% 7.44/1.43 % (388361)------------------------------
% 7.44/1.43 % (388361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.44/1.43 % (388361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.43 % (388361)CaDiCaL version: 2.1.3
% 7.44/1.43 % (388361)Termination reason: Instruction limit
% 7.44/1.43 % (388361)Termination phase: Saturation
% 7.44/1.43 % (388361)Time elapsed: 0.081 s
% 7.44/1.43 % (388361)Peak memory usage: 13 MB
% 7.44/1.43 % (388361)Instructions burned: 161 (million)
% 7.44/1.43 % (388369)Instruction limit reached!
% 7.44/1.43 % (388369)------------------------------
% 7.44/1.43 % (388369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.44/1.43 % (388369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.43 % (388369)CaDiCaL version: 2.1.3
% 7.44/1.43 % (388369)Termination reason: Instruction limit
% 7.44/1.43 % (388369)Termination phase: Saturation
% 7.44/1.43 % (388369)Time elapsed: 0.069 s
% 7.44/1.43 % (388369)Peak memory usage: 12 MB
% 7.44/1.43 % (388369)Instructions burned: 132 (million)
% 7.44/1.43 % (388358)Instruction limit reached!
% 7.44/1.43 % (388358)------------------------------
% 7.44/1.43 % (388358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.44/1.43 % (388358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.44/1.43 % (388358)CaDiCaL version: 2.1.3
% 7.44/1.43 % (388358)Termination reason: Instruction limit
% 7.44/1.43 % (388358)Termination phase: Saturation
% 7.44/1.43 % (388358)Time elapsed: 0.089 s
% 7.44/1.43 % (388358)Peak memory usage: 12 MB
% 7.44/1.43 % (388358)Instructions burned: 103 (million)
% 7.44/1.43 % (388373)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=49663522:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 7.44/1.43 % (388373)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.44/1.43 % (388373)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 7.44/1.43 % (388374)ott-21_1_sil=16000:fs=off:random_seed=4232831681:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 7.44/1.43 % (388375)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1525428374:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 27.22/4.23 % (388359)Instruction limit reached!
% 27.22/4.23 % (388359)------------------------------
% 27.22/4.23 % (388359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.22/4.23 % (388359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.22/4.23 % (388359)CaDiCaL version: 2.1.3
% 27.22/4.23 % (388359)Termination reason: Instruction limit
% 27.22/4.23 % (388359)Termination phase: Saturation
% 27.22/4.23 % (388359)Time elapsed: 0.128 s
% 27.22/4.23 % (388359)Peak memory usage: 12 MB
% 27.22/4.23 % (388359)Instructions burned: 116 (million)
% 27.22/4.23 % (388360)Instruction limit reached!
% 27.22/4.23 % (388360)------------------------------
% 27.22/4.23 % (388360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.22/4.23 % (388360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.22/4.23 % (388360)CaDiCaL version: 2.1.3
% 27.22/4.23 % (388360)Termination reason: Instruction limit
% 27.22/4.23 % (388360)Termination phase: Saturation
% 27.22/4.23 % (388360)Time elapsed: 0.137 s
% 27.22/4.23 % (388360)Peak memory usage: 12 MB
% 27.22/4.23 % (388360)Instructions burned: 131 (million)
% 27.22/4.23 % (388374)Instruction limit reached!
% 27.22/4.23 % (388374)------------------------------
% 27.22/4.23 % (388374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.22/4.23 % (388374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.22/4.23 % (388374)CaDiCaL version: 2.1.3
% 27.22/4.23 % (388374)Termination reason: Instruction limit
% 27.22/4.23 % (388374)Termination phase: Saturation
% 27.22/4.23 % (388374)Time elapsed: 0.098 s
% 27.22/4.23 % (388374)Peak memory usage: 12 MB
% 27.22/4.23 % (388374)Instructions burned: 182 (million)
% 27.22/4.23 % (388379)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2541346482:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 27.22/4.23 % Exception at run slice level
% 27.22/4.23 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 27.22/4.23 % (388380)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2632424466:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 27.22/4.23 % (388382)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=126798449:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 27.22/4.23 % Exception at run slice level
% 27.22/4.23 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 27.22/4.23 % (388383)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=3807908383: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)
% 27.22/4.23 % (388383)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 27.22/4.23 % (388386)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=227626083:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 27.22/4.23 % (388386)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 27.22/4.23 % (388373)Instruction limit reached!
% 27.22/4.23 % (388373)------------------------------
% 27.22/4.23 % (388373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.22/4.23 % (388373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.22/4.23 % (388373)CaDiCaL version: 2.1.3
% 27.22/4.23 % (388373)Termination reason: Instruction limit
% 27.22/4.23 % (388373)Termination phase: Saturation
% 27.22/4.23 % (388373)Time elapsed: 0.398 s
% 27.22/4.23 % (388373)Peak memory usage: 14 MB
% 27.22/4.23 % (388373)Instructions burned: 685 (million)
% 27.22/4.23 % (388375)Instruction limit reached!
% 27.22/4.23 % (388375)------------------------------
% 27.22/4.23 % (388375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.22/4.23 % (388375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.22/4.23 % (388375)CaDiCaL version: 2.1.3
% 27.22/4.23 % (388375)Termination reason: Instruction limit
% 27.22/4.23 % (388375)Termination phase: Saturation
% 27.22/4.23 % (388375)Time elapsed: 0.400 s
% 27.22/4.23 % (388375)Peak memory usage: 14 MB
% 27.22/4.23 % (388375)Instructions burned: 483 (million)
% 27.22/4.23 % (388390)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2809555388:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi)
% 27.22/4.23 % (388389)fmb+10_1_sil=64000:random_seed=1755725412:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 58.37/8.65 % Exception at run slice level
% 58.37/8.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 58.37/8.65 % (388389)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 58.37/8.65 % Exception at run slice level
% 58.37/8.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 58.37/8.65 % (388393)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2483993213:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi)
% 58.37/8.65 % Exception at run slice level
% 58.37/8.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 58.37/8.65 % (388394)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1875949396:i=5131_2994 on theBenchmark for (2994ds/5131Mi)
% 58.37/8.65 % (388394)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 58.37/8.65 % (388383)Instruction limit reached!
% 58.37/8.65 % (388383)------------------------------
% 58.37/8.65 % (388383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.37/8.65 % (388383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.37/8.65 % (388383)CaDiCaL version: 2.1.3
% 58.37/8.65 % (388383)Termination reason: Instruction limit
% 58.37/8.65 % (388383)Termination phase: Saturation
% 58.37/8.65 % (388383)Time elapsed: 0.336 s
% 58.37/8.65 % (388383)Peak memory usage: 15 MB
% 58.37/8.65 % (388383)Instructions burned: 692 (million)
% 58.37/8.65 % (388398)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3404278907:i=6324_2993 on theBenchmark for (2993ds/6324Mi)
% 58.37/8.65 % Exception at run slice level
% 58.37/8.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 58.37/8.65 % (388396)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=699351066:i=1472:ins=7:fdi=8:gsp=on_2993 on theBenchmark for (2993ds/1472Mi)
% 58.37/8.65 % (388396)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 58.37/8.65 % (388396)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 58.37/8.65 % (388400)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2779490:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi)
% 58.37/8.65 % Exception at run slice level
% 58.37/8.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 58.37/8.65 % (388403)ott-2_1_sil=16000:newcnf=on:random_seed=1157098441:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi)
% 58.37/8.65 % (388403)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 58.37/8.65 % (388403)Instruction limit reached!
% 58.37/8.65 % (388403)------------------------------
% 58.37/8.65 % (388403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.37/8.65 % (388403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.37/8.65 % (388403)CaDiCaL version: 2.1.3
% 58.37/8.65 % (388403)Termination reason: Instruction limit
% 58.37/8.65 % (388403)Termination phase: Saturation
% 58.37/8.65 % (388403)Time elapsed: 0.401 s
% 58.37/8.65 % (388403)Peak memory usage: 15 MB
% 58.37/8.65 % (388403)Instructions burned: 871 (million)
% 58.37/8.65 % (388405)ott+10_1_sil=32000:tgt=ground:random_seed=3411148375:i=5114:av=off_2988 on theBenchmark for (2988ds/5114Mi)
% 58.37/8.65 % (388386)Instruction limit reached!
% 58.37/8.65 % (388386)------------------------------
% 58.37/8.65 % (388386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 58.37/8.65 % (388386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.37/8.65 % (388386)CaDiCaL version: 2.1.3
% 58.37/8.65 % (388386)Termination reason: Instruction limit
% 58.37/8.65 % (388386)Termination phase: Saturation
% 58.37/8.65 % (388386)Time elapsed: 0.770 s
% 58.37/8.65 % (388386)Peak memory usage: 15 MB
% 58.37/8.65 % (388386)Instructions burned: 879 (million)
% 58.37/8.65 % (388407)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1194543792:i=54282_2988 on theBenchmark for (2988ds/54282Mi)
% 58.37/8.65 % Exception at run slice level
% 58.37/8.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 58.37/8.65 % (388409)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=885059167:i=3512:aac=none_2988 on theBenchmark for (2988ds/3512Mi)
% 166.52/24.04 % (388409)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 166.52/24.04 % (388380)Instruction limit reached!
% 166.52/24.04 % (388380)------------------------------
% 166.52/24.04 % (388380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 166.52/24.04 % (388380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.52/24.04 % (388380)CaDiCaL version: 2.1.3
% 166.52/24.04 % (388380)Termination reason: Instruction limit
% 166.52/24.04 % (388380)Termination phase: Saturation
% 166.52/24.04 % (388380)Time elapsed: 0.998 s
% 166.52/24.04 % (388380)Peak memory usage: 15 MB
% 166.52/24.04 % (388380)Instructions burned: 1180 (million)
% 166.52/24.04 % (388411)dis+21_1_sil=32000:sas=cadical:random_seed=2433625278:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi)
% 166.52/24.04 % (388396)Instruction limit reached!
% 166.52/24.04 % (388396)------------------------------
% 166.52/24.04 % (388396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 166.52/24.04 % (388396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.52/24.04 % (388396)CaDiCaL version: 2.1.3
% 166.52/24.04 % (388396)Termination reason: Instruction limit
% 166.52/24.04 % (388396)Termination phase: Saturation
% 166.52/24.04 % (388396)Time elapsed: 1.245 s
% 166.52/24.04 % (388396)Peak memory usage: 16 MB
% 166.52/24.04 % (388396)Instructions burned: 1472 (million)
% 166.52/24.04 % (388413)ott+11_1_sil=16000:gs=on:random_seed=3056315272:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2980 on theBenchmark for (2980ds/2251Mi)
% 166.52/24.04 % (388413)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 166.52/24.04 % (388394)Instruction limit reached!
% 166.52/24.04 % (388394)------------------------------
% 166.52/24.04 % (388394)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 166.52/24.04 % (388394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.52/24.04 % (388394)CaDiCaL version: 2.1.3
% 166.52/24.04 % (388394)Termination reason: Instruction limit
% 166.52/24.04 % (388394)Termination phase: Saturation
% 166.52/24.04 % (388394)Time elapsed: 2.315 s
% 166.52/24.04 % (388394)Peak memory usage: 22 MB
% 166.52/24.04 % (388394)Instructions burned: 5133 (million)
% 166.52/24.04 % (388415)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2965996547:fmbsr=1.6:i=67534_2970 on theBenchmark for (2970ds/67534Mi)
% 166.52/24.04 % Exception at run slice level
% 166.52/24.04 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 166.52/24.04 % (388417)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2299904307:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2970 on theBenchmark for (2970ds/4591Mi)
% 166.52/24.04 % (388409)Instruction limit reached!
% 166.52/24.04 % (388409)------------------------------
% 166.52/24.04 % (388409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 166.52/24.04 % (388409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.52/24.04 % (388409)CaDiCaL version: 2.1.3
% 166.52/24.04 % (388409)Termination reason: Instruction limit
% 166.52/24.04 % (388409)Termination phase: Saturation
% 166.52/24.04 % (388409)Time elapsed: 1.997 s
% 166.52/24.04 % (388409)Peak memory usage: 20 MB
% 166.52/24.04 % (388409)Instructions burned: 3512 (million)
% 166.52/24.04 % (388419)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2963280633:i=29340_2968 on theBenchmark for (2968ds/29340Mi)
% 166.52/24.04 % (388413)Instruction limit reached!
% 166.52/24.04 % (388413)------------------------------
% 166.52/24.04 % (388413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 166.52/24.04 % (388413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.52/24.04 % (388413)CaDiCaL version: 2.1.3
% 166.52/24.04 % (388413)Termination reason: Instruction limit
% 166.52/24.04 % (388413)Termination phase: Saturation
% 166.52/24.04 % (388413)Time elapsed: 1.495 s
% 166.52/24.04 % (388413)Peak memory usage: 20 MB
% 166.52/24.04 % (388413)Instructions burned: 2251 (million)
% 166.52/24.04 % (388421)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3364419930:i=5211_2965 on theBenchmark for (2965ds/5211Mi)
% 166.52/24.04 % (388411)Instruction limit reached!
% 166.52/24.04 % (388411)------------------------------
% 166.52/24.04 % (388411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 166.52/24.04 % (388411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.96/24.97 % (388411)CaDiCaL version: 2.1.3
% 172.96/24.97 % (388411)Termination reason: Instruction limit
% 172.96/24.97 % (388411)Termination phase: Saturation
% 172.96/24.97 % (388411)Time elapsed: 2.647 s
% 172.96/24.97 % (388411)Peak memory usage: 20 MB
% 172.96/24.97 % (388411)Instructions burned: 3775 (million)
% 172.96/24.97 % (388423)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3599388762:i=5497:nm=2_2960 on theBenchmark for (2960ds/5497Mi)
% 172.96/24.97 % Exception at run slice level
% 172.96/24.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 172.96/24.97 % (388425)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=325613643:fmbsr=2:i=46332_2959 on theBenchmark for (2959ds/46332Mi)
% 172.96/24.97 % Exception at run slice level
% 172.96/24.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 172.96/24.97 % (388427)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3892046862:i=14071_2959 on theBenchmark for (2959ds/14071Mi)
% 172.96/24.97 % Exception at run slice level
% 172.96/24.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 172.96/24.97 % (388429)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=941752787:i=22565:add=on:rawr=on_2959 on theBenchmark for (2959ds/22565Mi)
% 172.96/24.97 % (388405)Instruction limit reached!
% 172.96/24.97 % (388405)------------------------------
% 172.96/24.97 % (388405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 172.96/24.97 % (388405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.96/24.97 % (388405)CaDiCaL version: 2.1.3
% 172.96/24.97 % (388405)Termination reason: Instruction limit
% 172.96/24.97 % (388405)Termination phase: Saturation
% 172.96/24.97 % (388405)Time elapsed: 3.540 s
% 172.96/24.97 % (388405)Peak memory usage: 27 MB
% 172.96/24.97 % (388405)Instructions burned: 5114 (million)
% 172.96/24.97 % (388431)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=4168775758:i=8173:av=off_2953 on theBenchmark for (2953ds/8173Mi)
% 172.96/24.97 % (388417)Instruction limit reached!
% 172.96/24.97 % (388417)------------------------------
% 172.96/24.97 % (388417)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 172.96/24.97 % (388417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.96/24.97 % (388417)CaDiCaL version: 2.1.3
% 172.96/24.97 % (388417)Termination reason: Instruction limit
% 172.96/24.97 % (388417)Termination phase: Saturation
% 172.96/24.97 % (388417)Time elapsed: 3.140 s
% 172.96/24.97 % (388417)Peak memory usage: 17 MB
% 172.96/24.97 % (388417)Instructions burned: 4592 (million)
% 172.96/24.97 % (388433)dis+10_16:1_sil=16000:random_seed=1476611673:i=9155:fsr=off_2938 on theBenchmark for (2938ds/9155Mi)
% 172.96/24.97 % (388421)Instruction limit reached!
% 172.96/24.97 % (388421)------------------------------
% 172.96/24.97 % (388421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 172.96/24.97 % (388421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.96/24.97 % (388421)CaDiCaL version: 2.1.3
% 172.96/24.97 % (388421)Termination reason: Instruction limit
% 172.96/24.97 % (388421)Termination phase: Saturation
% 172.96/24.97 % (388421)Time elapsed: 3.206 s
% 172.96/24.97 % (388421)Peak memory usage: 30 MB
% 172.96/24.97 % (388421)Instructions burned: 5211 (million)
% 172.96/24.97 % (388435)ott-3_8_sil=64000:random_seed=3526791258:i=20139:bs=on_2933 on theBenchmark for (2933ds/20139Mi)
% 172.96/24.97 % (388431)Instruction limit reached!
% 172.96/24.97 % (388431)------------------------------
% 172.96/24.97 % (388431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 172.96/24.97 % (388431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.96/24.97 % (388431)CaDiCaL version: 2.1.3
% 172.96/24.97 % (388431)Termination reason: Instruction limit
% 172.96/24.97 % (388431)Termination phase: Saturation
% 172.96/24.97 % (388431)Time elapsed: 3.664 s
% 172.96/24.97 % (388431)Peak memory usage: 38 MB
% 172.96/24.97 % (388431)Instructions burned: 8173 (million)
% 172.96/24.97 % (388437)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2224566257:fmbsr=2:i=32576_2916 on theBenchmark for (2916ds/32576Mi)
% 172.96/24.97 % Exception at run slice level
% 172.96/24.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 172.96/24.97 % (388439)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=688439860:i=11404_2916 on theBenchmark for (2916ds/11404Mi)
% 183.80/26.30 % (388433)Instruction limit reached!
% 183.80/26.30 % (388433)------------------------------
% 183.80/26.30 % (388433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.80/26.30 % (388433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.80/26.30 % (388433)CaDiCaL version: 2.1.3
% 183.80/26.30 % (388433)Termination reason: Instruction limit
% 183.80/26.30 % (388433)Termination phase: Saturation
% 183.80/26.30 % (388433)Time elapsed: 2.714 s
% 183.80/26.30 % (388433)Peak memory usage: 26 MB
% 183.80/26.30 % (388433)Instructions burned: 9158 (million)
% 183.80/26.30 % (388441)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=590340841:i=14134_2911 on theBenchmark for (2911ds/14134Mi)
% 183.80/26.30 % (388441)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 183.80/26.30 % (388441)Instruction limit reached!
% 183.80/26.30 % (388441)------------------------------
% 183.80/26.30 % (388441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.80/26.30 % (388441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.80/26.30 % (388441)CaDiCaL version: 2.1.3
% 183.80/26.30 % (388441)Termination reason: Instruction limit
% 183.80/26.30 % (388441)Termination phase: Saturation
% 183.80/26.30 % (388441)Time elapsed: 4.373 s
% 183.80/26.30 % (388441)Peak memory usage: 55 MB
% 183.80/26.30 % (388441)Instructions burned: 14134 (million)
% 183.80/26.30 % (388443)dis+33_16_sil=32000:sac=on:random_seed=3741271566:i=15851:nm=0_2867 on theBenchmark for (2867ds/15851Mi)
% 183.80/26.30 % (388439)Instruction limit reached!
% 183.80/26.30 % (388439)------------------------------
% 183.80/26.30 % (388439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.80/26.30 % (388439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.80/26.30 % (388439)CaDiCaL version: 2.1.3
% 183.80/26.30 % (388439)Termination reason: Instruction limit
% 183.80/26.30 % (388439)Termination phase: Saturation
% 183.80/26.30 % (388439)Time elapsed: 5.147 s
% 183.80/26.30 % (388439)Peak memory usage: 54 MB
% 183.80/26.30 % (388439)Instructions burned: 11404 (million)
% 183.80/26.30 % (388445)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2326180512:avsq=on:i=17627:add=on:amm=off_2864 on theBenchmark for (2864ds/17627Mi)
% 183.80/26.30 % (388443)Instruction limit reached!
% 183.80/26.30 % (388443)------------------------------
% 183.80/26.30 % (388443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.80/26.30 % (388443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.80/26.30 % (388443)CaDiCaL version: 2.1.3
% 183.80/26.30 % (388443)Termination reason: Instruction limit
% 183.80/26.30 % (388443)Termination phase: Saturation
% 183.80/26.30 % (388443)Time elapsed: 5.186 s
% 183.80/26.30 % (388443)Peak memory usage: 34 MB
% 183.80/26.30 % (388443)Instructions burned: 15855 (million)
% 183.80/26.30 % (388447)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2868949080:s2a=on:i=53295_2815 on theBenchmark for (2815ds/53295Mi)
% 183.80/26.30 % (388435)Instruction limit reached!
% 183.80/26.30 % (388435)------------------------------
% 183.80/26.30 % (388435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.80/26.30 % (388435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.80/26.30 % (388435)CaDiCaL version: 2.1.3
% 183.80/26.30 % (388435)Termination reason: Instruction limit
% 183.80/26.30 % (388435)Termination phase: Saturation
% 183.80/26.30 % (388435)Time elapsed: 16.304 s
% 183.80/26.30 % (388435)Peak memory usage: 59 MB
% 183.80/26.30 % (388435)Instructions burned: 20139 (million)
% 183.80/26.30 % (388449)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=600988734:i=26857:ins=20_2769 on theBenchmark for (2769ds/26857Mi)
% 183.80/26.30 % Exception at run slice level
% 183.80/26.30 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 183.80/26.30 % (388451)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=4096340046:i=28120:bs=on:fsr=off_2769 on theBenchmark for (2769ds/28120Mi)
% 183.80/26.30 % (388445)Instruction limit reached!
% 183.80/26.30 % (388445)------------------------------
% 183.80/26.30 % (388445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.80/26.30 % (388445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.80/26.30 % (388445)CaDiCaL version: 2.1.3
% 183.80/26.30 % (388445)Termination reason: Instruction limit
% 183.80/26.30 % (388445)Termination phase: Saturation
% 183.80/26.30 % (388445)Time elapsed: 10.212 s
% 207.95/29.76 % (388445)Peak memory usage: 64 MB
% 207.95/29.76 % (388445)Instructions burned: 17628 (million)
% 207.95/29.76 % (388453)fmb+10_1_sil=256000:fmbss=7:random_seed=1567271545:fmbsr=1.6:i=182295_2762 on theBenchmark for (2762ds/182295Mi)
% 207.95/29.76 % Exception at run slice level
% 207.95/29.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 207.95/29.76 % (388455)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2029335253:i=44625:gsp=on_2761 on theBenchmark for (2761ds/44625Mi)
% 207.95/29.76 % (388455)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 207.95/29.76 % (388455)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 207.95/29.76 % Exception at run slice level
% 207.95/29.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 207.95/29.76 % (388457)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1000416179:i=160505_2761 on theBenchmark for (2761ds/160505Mi)
% 207.95/29.76 % Exception at run slice level
% 207.95/29.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 207.95/29.76 % (388459)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2176444957:fmbsr=1.3:i=225729_2761 on theBenchmark for (2761ds/225729Mi)
% 207.95/29.76 % Exception at run slice level
% 207.95/29.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 207.95/29.76 % (388461)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=678969828:fmbsr=2:i=185024:ins=7_2761 on theBenchmark for (2761ds/185024Mi)
% 207.95/29.76 % Exception at run slice level
% 207.95/29.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 207.95/29.76 % (388463)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2314459709:rtra=on_2760 on theBenchmark for (2760ds/0Mi)
% 207.95/29.76 % Exception at run slice level
% 207.95/29.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 207.95/29.76 % (388465)% WARNING: option uhcvi not known.
% 207.95/29.76 % (388465)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1962947723:i=271062:add=off:rtra=on:rawr=on_2760 on theBenchmark for (2760ds/271062Mi)
% 207.95/29.76 % (388465)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 207.95/29.76 % (388465)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 207.95/29.76 % (388429)Instruction limit reached!
% 207.95/29.76 % (388429)------------------------------
% 207.95/29.76 % (388429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.95/29.76 % (388429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.95/29.76 % (388429)CaDiCaL version: 2.1.3
% 207.95/29.76 % (388429)Termination reason: Instruction limit
% 207.95/29.76 % (388429)Termination phase: Saturation
% 207.95/29.76 % (388429)Time elapsed: 20.252 s
% 207.95/29.76 % (388429)Peak memory usage: 65 MB
% 207.95/29.76 % (388429)Instructions burned: 22565 (million)
% 207.95/29.76 % (388467)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1579793579:i=176048:add=on:rtra=on:rawr=on_2756 on theBenchmark for (2756ds/176048Mi)
% 207.95/29.76 % (388419)Instruction limit reached!
% 207.95/29.76 % (388419)------------------------------
% 207.95/29.76 % (388419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.95/29.76 % (388419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.95/29.76 % (388419)CaDiCaL version: 2.1.3
% 207.95/29.76 % (388419)Termination reason: Instruction limit
% 207.95/29.76 % (388419)Termination phase: Saturation
% 207.95/29.76 % (388419)Time elapsed: 21.290 s
% 207.95/29.76 % (388419)Peak memory usage: 47 MB
% 207.95/29.76 % (388419)Instructions burned: 29340 (million)
% 207.95/29.76 % (388469)dis+10_1_sil=32000:si=on:sp=arity:random_seed=3070266154:i=206:fgj=on:rtra=on_2755 on theBenchmark for (2755ds/206Mi)
% 207.95/29.76 % (388469)Instruction limit reached!
% 207.95/29.76 % (388469)------------------------------
% 207.95/29.76 % (388469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.95/29.76 % (388469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.95/29.76 % (388469)CaDiCaL version: 2.1.3
% 207.95/29.76 % (388469)Termination reason: Instruction limit
% 207.95/29.76 % (388469)Termination phase: Saturation
% 207.95/29.76 % (388469)Time elapsed: 0.176 s
% 251.38/36.00 % (388469)Peak memory usage: 12 MB
% 251.38/36.00 % (388469)Instructions burned: 208 (million)
% 251.38/36.00 % (388471)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3227103684:i=232:rtra=on_2752 on theBenchmark for (2752ds/232Mi)
% 251.38/36.00 % (388471)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 251.38/36.00 % (388471)Instruction limit reached!
% 251.38/36.00 % (388471)------------------------------
% 251.38/36.00 % (388471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 251.38/36.00 % (388471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 251.38/36.00 % (388471)CaDiCaL version: 2.1.3
% 251.38/36.00 % (388471)Termination reason: Instruction limit
% 251.38/36.00 % (388471)Termination phase: Saturation
% 251.38/36.00 % (388471)Time elapsed: 0.130 s
% 251.38/36.00 % (388471)Peak memory usage: 13 MB
% 251.38/36.00 % (388471)Instructions burned: 233 (million)
% 251.38/36.00 % (388473)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2034278730:i=262:rtra=on_2751 on theBenchmark for (2751ds/262Mi)
% 251.38/36.00 % (388473)Instruction limit reached!
% 251.38/36.00 % (388473)------------------------------
% 251.38/36.00 % (388473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 251.38/36.00 % (388473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 251.38/36.00 % (388473)CaDiCaL version: 2.1.3
% 251.38/36.00 % (388473)Termination reason: Instruction limit
% 251.38/36.00 % (388473)Termination phase: Saturation
% 251.38/36.00 % (388473)Time elapsed: 0.134 s
% 251.38/36.00 % (388473)Peak memory usage: 13 MB
% 251.38/36.00 % (388473)Instructions burned: 263 (million)
% 251.38/36.00 % (388475)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2823582928:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2749 on theBenchmark for (2749ds/318Mi)
% 251.38/36.00 % (388475)Instruction limit reached!
% 251.38/36.00 % (388475)------------------------------
% 251.38/36.00 % (388475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 251.38/36.00 % (388475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 251.38/36.00 % (388475)CaDiCaL version: 2.1.3
% 251.38/36.00 % (388475)Termination reason: Instruction limit
% 251.38/36.00 % (388475)Termination phase: Saturation
% 251.38/36.00 % (388475)Time elapsed: 0.161 s
% 251.38/36.00 % (388475)Peak memory usage: 13 MB
% 251.38/36.00 % (388475)Instructions burned: 319 (million)
% 251.38/36.00 % (388477)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=2824052315:i=1428:nm=2:rtra=on_2747 on theBenchmark for (2747ds/1428Mi)
% 251.38/36.00 % Exception at run slice level
% 251.38/36.00 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 251.38/36.00 % (388479)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2483075971:i=262:bd=preordered:rtra=on:fsd=on_2747 on theBenchmark for (2747ds/262Mi)
% 251.38/36.00 % (388479)Instruction limit reached!
% 251.38/36.00 % (388479)------------------------------
% 251.38/36.00 % (388479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 251.38/36.00 % (388479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 251.38/36.00 % (388479)CaDiCaL version: 2.1.3
% 251.38/36.00 % (388479)Termination reason: Instruction limit
% 251.38/36.00 % (388479)Termination phase: Saturation
% 251.38/36.00 % (388479)Time elapsed: 0.134 s
% 251.38/36.00 % (388479)Peak memory usage: 13 MB
% 251.38/36.00 % (388479)Instructions burned: 263 (million)
% 251.38/36.00 % (388481)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2752674732:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2746 on theBenchmark for (2746ds/1368Mi)
% 251.38/36.00 % (388481)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 251.38/36.00 % (388481)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 251.38/36.00 % (388481)Instruction limit reached!
% 251.38/36.00 % (388481)------------------------------
% 251.38/36.00 % (388481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 251.38/36.00 % (388481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 251.38/36.00 % (388481)CaDiCaL version: 2.1.3
% 251.38/36.00 % (388481)Termination reason: Instruction limit
% 251.38/36.00 % (388481)Termination phase: Saturation
% 251.38/36.00 % (388481)Time elapsed: 0.632 s
% 251.38/36.00 % (388481)Peak memory usage: 17 MB
% 251.38/36.00 % (388481)Instructions burned: 1370 (million)
% 251.38/36.00 % (388483)ott-21_1_sil=16000:si=on:fs=off:random_seed=3960140539:i=360:av=off:fsr=off:rtra=on_2739 on theBenchmark for (2739ds/360Mi)
% 283.22/40.34 % (388483)Instruction limit reached!
% 283.22/40.34 % (388483)------------------------------
% 283.22/40.34 % (388483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 283.22/40.34 % (388483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 283.22/40.34 % (388483)CaDiCaL version: 2.1.3
% 283.22/40.34 % (388483)Termination reason: Instruction limit
% 283.22/40.34 % (388483)Termination phase: Saturation
% 283.22/40.34 % (388483)Time elapsed: 0.165 s
% 283.22/40.34 % (388483)Peak memory usage: 12 MB
% 283.22/40.34 % (388483)Instructions burned: 362 (million)
% 283.22/40.34 % (388485)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1364211241:i=954:bd=all:rtra=on_2737 on theBenchmark for (2737ds/954Mi)
% 283.22/40.34 % (388485)Instruction limit reached!
% 283.22/40.34 % (388485)------------------------------
% 283.22/40.34 % (388485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 283.22/40.34 % (388485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 283.22/40.34 % (388485)CaDiCaL version: 2.1.3
% 283.22/40.34 % (388485)Termination reason: Instruction limit
% 283.22/40.34 % (388485)Termination phase: Saturation
% 283.22/40.34 % (388485)Time elapsed: 0.465 s
% 283.22/40.34 % (388485)Peak memory usage: 14 MB
% 283.22/40.34 % (388485)Instructions burned: 954 (million)
% 283.22/40.34 % (388487)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=2016621809:fmbsr=1.3:i=1730:ins=25:rtra=on_2732 on theBenchmark for (2732ds/1730Mi)
% 283.22/40.34 % Exception at run slice level
% 283.22/40.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 283.22/40.34 % (388489)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=4108884286:i=2358:rtra=on_2732 on theBenchmark for (2732ds/2358Mi)
% 283.22/40.34 % (388489)Instruction limit reached!
% 283.22/40.34 % (388489)------------------------------
% 283.22/40.34 % (388489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 283.22/40.34 % (388489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 283.22/40.34 % (388489)CaDiCaL version: 2.1.3
% 283.22/40.34 % (388489)Termination reason: Instruction limit
% 283.22/40.34 % (388489)Termination phase: Saturation
% 283.22/40.34 % (388489)Time elapsed: 1.196 s
% 283.22/40.34 % (388489)Peak memory usage: 20 MB
% 283.22/40.34 % (388489)Instructions burned: 2359 (million)
% 283.22/40.34 % (388491)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=2300822836:i=1778:ins=1:rtra=on_2720 on theBenchmark for (2720ds/1778Mi)
% 283.22/40.34 % Exception at run slice level
% 283.22/40.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 283.22/40.34 % (388493)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=374760345:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2720 on theBenchmark for (2720ds/1384Mi)
% 283.22/40.34 % (388493)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 283.22/40.34 % (388493)Instruction limit reached!
% 283.22/40.34 % (388493)------------------------------
% 283.22/40.34 % (388493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 283.22/40.34 % (388493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 283.22/40.34 % (388493)CaDiCaL version: 2.1.3
% 283.22/40.34 % (388493)Termination reason: Instruction limit
% 283.22/40.34 % (388493)Termination phase: Saturation
% 283.22/40.34 % (388493)Time elapsed: 0.632 s
% 283.22/40.34 % (388493)Peak memory usage: 18 MB
% 283.22/40.34 % (388493)Instructions burned: 1386 (million)
% 283.22/40.34 % (388495)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=2116584348:i=1758:kws=inv_precedence:fsr=off:rtra=on_2713 on theBenchmark for (2713ds/1758Mi)
% 283.22/40.34 % (388495)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 283.22/40.34 % (388495)Instruction limit reached!
% 283.22/40.34 % (388495)------------------------------
% 283.22/40.34 % (388495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 283.22/40.34 % (388495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 283.22/40.34 % (388495)CaDiCaL version: 2.1.3
% 283.22/40.34 % (388495)Termination reason: Instruction limit
% 283.22/40.34 % (388495)Termination phase: Saturation
% 283.22/40.34 % (388495)Time elapsed: 0.863 s
% 283.22/40.34 % (388495)Peak memory usage: 17 MB
% 283.22/40.34 % (388495)Instructions burned: 1759 (million)
% 283.22/40.34 % (388497)fmb+10_1_sil=64000:si=on:random_seed=336428842:i=44122:nm=2:rtra=on:gsp=on_2704 on theBenchmark for (2704ds/44122Mi)
% 283.22/40.34 % (388497)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 283.22/40.34 % Exception at run slice level
% 283.22/40.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 283.22/40.34 % (388499)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2280042256:i=19030:nm=5:rtra=on_2704 on theBenchmark for (2704ds/19030Mi)
% 283.22/40.34 % Exception at run slice level
% 283.22/40.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 283.22/40.34 % (388501)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=3882639122:fmbsr=1.7:i=1840:rtra=on_2704 on theBenchmark for (2704ds/1840Mi)
% 283.22/40.34 % Exception at run slice level
% 283.22/40.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 283.22/40.34 % (388503)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3184075423:i=10262:rtra=on_2704 on theBenchmark for (2704ds/10262Mi)
% 283.22/40.34 % (388503)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 283.22/40.34 % (388503)Instruction limit reached!
% 283.22/40.34 % (388503)------------------------------
% 283.22/40.34 % (388503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 283.22/40.34 % (388503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 283.22/40.34 % (388503)CaDiCaL version: 2.1.3
% 283.22/40.34 % (388503)Termination reason: Instruction limit
% 283.22/40.34 % (388503)Termination phase: Saturation
% 283.22/40.34 % (388503)Time elapsed: 4.643 s
% 283.22/40.34 % (388503)Peak memory usage: 29 MB
% 283.22/40.34 % (388503)Instructions burned: 10263 (million)
% 283.22/40.34 % (388506)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1946834247:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2657 on theBenchmark for (2657ds/2944Mi)
% 283.22/40.34 % (388506)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 283.22/40.34 % (388506)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 283.22/40.34 % (388447)Instruction limit reached!
% 283.22/40.34 % (388447)------------------------------
% 283.22/40.34 % (388447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 283.22/40.34 % (388447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 283.22/40.34 % (388447)CaDiCaL version: 2.1.3
% 283.22/40.34 % (388447)Termination reason: Instruction limit
% 283.22/40.34 % (388447)Termination phase: Saturation
% 283.22/40.34 % (388447)Time elapsed: 16.476 s
% 283.22/40.34 % (388447)Peak memory usage: 169 MB
% 283.22/40.34 % (388447)Instructions burned: 53295 (million)
% 283.22/40.34 % (388508)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1548815040:i=12648:rtra=on_2650 on theBenchmark for (2650ds/12648Mi)
% 283.22/40.34 % Exception at run slice level
% 283.22/40.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 283.22/40.34 % (388510)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=1044678662:fmbsr=2.30978:i=4348:rtra=on_2649 on theBenchmark for (2649ds/4348Mi)
% 283.22/40.34 % Exception at run slice level
% 283.22/40.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 283.22/40.34 % (388512)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=210752062:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2649 on theBenchmark for (2649ds/1738Mi)
% 283.22/40.34 % (388512)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 283.22/40.34 % (388506)Instruction limit reached!
% 283.22/40.34 % (388506)------------------------------
% 283.22/40.34 % (388506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 283.22/40.34 % (388506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 283.22/40.34 % (388506)CaDiCaL version: 2.1.3
% 283.22/40.34 % (388506)Termination reason: Instruction limit
% 283.22/40.34 % (388506)Termination phase: Saturation
% 283.22/40.34 % (388506)Time elapsed: 1.455 s
% 283.22/40.34 % (388506)Peak memory usage: 21 MB
% 283.22/40.34 % (388506)Instructions burned: 2946 (million)
% 283.22/40.34 % (388514)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=92890278:i=10228:av=off:rtra=on_2642 on theBenchmark for (2642ds/10228Mi)
% 283.22/40.34 % (388512)Instruction limit reached!
% 283.22/40.34 % (388512)------------------------------
% 283.22/40.34 % (388512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 283.22/40.34 % (388512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 283.22/40.34 % (388512)CaDiCaL version: 2.1.3
% 283.22/40.34 % (388512)Termination reason: Instruction limit
% 283.22/40.34 % (388512)Termination phase: Saturation
% 283.22/40.34 % (388512)Time elapsed: 0.804 s
% 283.22/40.34 % (388512)Peak memory usage: 19 MB
% 283.22/40.34 % (388512)Instructions burned: 1741 (million)
% 283.22/40.34 % (388516)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=552912843:i=108564:rtra=on_2641 on theBenchmark for (2641ds/108564Mi)
% 283.22/40.34 % Exception at run slice level
% 283.22/40.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 283.22/40.34 % (388518)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=1783597334:i=7024:aac=none:rtra=on_2641 on theBenchmark for (2641ds/7024Mi)
% 283.22/40.34 % (388518)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 283.22/40.34 % (388518)Instruction limit reached!
% 283.22/40.34 % (388518)------------------------------
% 283.22/40.34 % (388518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 283.22/40.34 % (388518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 283.22/40.34 % (388518)CaDiCaL version: 2.1.3
% 283.22/40.34 % (388518)Termination reason: Instruction limit
% 283.22/40.34 % (388518)Termination phase: Saturation
% 283.22/40.34 % (388518)Time elapsed: 2.099 s
% 283.22/40.34 % (388518)Peak memory usage: 26 MB
% 283.22/40.34 % (388518)Instructions burned: 7025 (million)
% 283.22/40.34 % (388520)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=3812723269:i=7546:rtra=on:amm=off_2619 on theBenchmark for (2619ds/7546Mi)
% 283.22/40.34 % (388514) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-388350-388514"...
% 283.22/40.34 % (388514)...printing done.
% 283.22/40.34 % (388514)Refutation found. Thanks to Tanya!
% 283.22/40.34 % SZS status Theorem for theBenchmark
% 283.22/40.34 % SZS output start Proof for theBenchmark
% 283.22/40.34 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 283.22/40.34 thf(func_def_0, type, in: ($i > $i > $o)).
% 283.22/40.34 thf(func_def_1, type, dsetconstr: ($i > ($i > $o) > $i)).
% 283.22/40.34 thf(func_def_2, type, dsetconstrI: $o).
% 283.22/40.34 thf(func_def_4, type, dsetconstrEL: $o).
% 283.22/40.34 thf(func_def_5, type, dsetconstrER: $o).
% 283.22/40.34 thf(func_def_6, type, setext: $o).
% 283.22/40.34 thf(func_def_7, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 283.22/40.34 thf(func_def_8, type, vIMP: ($o > $o > $o)).
% 283.22/40.34 thf(func_def_9, type, db0: !>[X0: $tType]:(X0)).
% 283.22/40.34 thf(func_def_10, type, db1: !>[X0: $tType]:(X0)).
% 283.22/40.34 thf(func_def_11, type, db2: !>[X0: $tType]:(X0)).
% 283.22/40.34 thf(func_def_12, type, db3: !>[X0: $tType]:(X0)).
% 283.22/40.34 thf(func_def_13, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 283.22/40.34 thf(func_def_14, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 283.22/40.34 thf(func_def_19, type, sK2: ($i > $o)).
% 283.22/40.34 thf(func_def_20, type, sK3: ($i > $o)).
% 283.22/40.34 thf(func_def_21, type, sF4: $o).
% 283.22/40.34 thf(func_def_22, type, sF5: $o).
% 283.22/40.34 thf(func_def_23, type, sF6: $o).
% 283.22/40.34 thf(func_def_24, type, sF7: $o).
% 283.22/40.34 thf(func_def_27, type, vNOT: ($o > $o)).
% 283.22/40.34 thf(func_def_30, type, sK12: ($i > $i > $i)).
% 283.22/40.34 thf(func_def_31, type, sK13: ($i > $i > $i)).
% 283.22/40.34 thf(func_def_33, type, sK15: ($i > $o)).
% 283.22/40.34 thf(func_def_35, type, sK17: ($i > $o)).
% 283.22/40.34 thf(func_def_40, type, sK22: ($i > $o)).
% 283.22/40.34 thf(f1,axiom,(
% 283.22/40.34 (! [X2 : $i,X0 : $i,X1 : ($i > $o)] : ((in @ X2 @ X0) => ((X1 @ X2) => (in @ X2 @ (dsetconstr @ X0 @ (^[X3 : $i] : ((X1 @ X3))))))) = dsetconstrI)),
% 283.22/40.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dsetconstrI)).
% 283.22/40.34 thf(f2,axiom,(
% 283.22/40.34 (dsetconstrEL = ! [X2 : $i,X1 : ($i > $o),X0 : $i] : ((in @ X2 @ (dsetconstr @ X0 @ (^[X3 : $i] : ((X1 @ X3))))) => (in @ X2 @ X0)))),
% 283.22/40.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dsetconstrEL)).
% 283.22/40.34 thf(f3,axiom,(
% 283.22/40.34 (dsetconstrER = ! [X1 : ($i > $o),X0 : $i,X2 : $i] : ((in @ X2 @ (dsetconstr @ X0 @ (^[X3 : $i] : ((X1 @ X3))))) => (X1 @ X2)))),
% 283.22/40.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dsetconstrER)).
% 283.22/40.34 thf(f4,axiom,(
% 283.22/40.34 (! [X1 : $i,X0 : $i] : (! [X2 : $i] : ((in @ X2 @ X0) => (in @ X2 @ X1)) => (! [X2 : $i] : ((in @ X2 @ X1) => (in @ X2 @ X0)) => (X0 = X1))) = setext)),
% 283.22/40.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',setext)).
% 283.22/40.34 thf(f5,conjecture,(
% 283.22/40.34 dsetconstrI => (dsetconstrEL => (dsetconstrER => (setext => ! [X0 : $i,X1 : $i] : ((X0 = X1) => ! [X3 : ($i > $o),X2 : ($i > $o)] : (! [X4 : $i] : ((in @ X4 @ X0) => ! [X5 : $i] : ((in @ X5 @ X1) => ((X4 = X5) => ((X2 @ X4) <=> (X3 @ X5))))) => (((dsetconstr @ X1 @ (^[X4 : $i] : ((X3 @ X4))))) = ((dsetconstr @ X0 @ (^[X4 : $i] : ((X2 @ X4)))))))))))),
% 283.22/40.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dsetconstr__Cong)).
% 283.22/40.34 thf(f6,negated_conjecture,(
% 283.22/40.34 ~(dsetconstrI => (dsetconstrEL => (dsetconstrER => (setext => ! [X0 : $i,X1 : $i] : ((X0 = X1) => ! [X3 : ($i > $o),X2 : ($i > $o)] : (! [X4 : $i] : ((in @ X4 @ X0) => ! [X5 : $i] : ((in @ X5 @ X1) => ((X4 = X5) => ((X2 @ X4) <=> (X3 @ X5))))) => (((dsetconstr @ X1 @ (^[X4 : $i] : ((X3 @ X4))))) = ((dsetconstr @ X0 @ (^[X4 : $i] : ((X2 @ X4))))))))))))),
% 283.22/40.34 inference(negated_conjecture,[status(cth)],[f5])).
% 283.22/40.34 thf(f7,plain,(
% 283.22/40.34 (! [X0 : $i,X1 : $i,X2 : ($i > $o)] : ((in @ X0 @ X1) => ((X2 @ X0) => (in @ X0 @ (dsetconstr @ X1 @ (^[X3 : $i] : ((X2 @ X3))))))) = dsetconstrI)),
% 283.22/40.34 inference(rectify,[],[f1])).
% 283.22/40.34 thf(f8,plain,(
% 283.22/40.34 (dsetconstrI = ((!! @ ($i > $o) @ (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) => ((Y0 @ Y2) => (in @ Y2 @ (dsetconstr @ Y1 @ (^[Y3 : $i]: (Y0 @ Y3))))))))))))))),
% 283.22/40.34 inference(fool_elimination,[],[f7])).
% 283.22/40.34 thf(f9,plain,(
% 283.22/40.34 (! [X0 : $i,X1 : $i] : (! [X2 : $i] : ((in @ X2 @ X1) => (in @ X2 @ X0)) => (! [X3 : $i] : ((in @ X3 @ X0) => (in @ X3 @ X1)) => (X0 = X1))) = setext)),
% 283.22/40.34 inference(rectify,[],[f4])).
% 283.22/40.34 thf(f10,plain,(
% 283.22/40.34 (setext = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y0) => (in @ Y2 @ Y1)))) => ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) => (in @ Y2 @ Y0)))) => (Y1 = Y0)))))))))),
% 283.22/40.34 inference(fool_elimination,[],[f9])).
% 283.22/40.34 thf(f11,plain,(
% 283.22/40.34 (dsetconstrEL = ! [X0 : $i,X1 : ($i > $o),X2 : $i] : ((in @ X0 @ (dsetconstr @ X2 @ (^[X3 : $i] : ((X1 @ X3))))) => (in @ X0 @ X2)))),
% 283.22/40.34 inference(rectify,[],[f2])).
% 283.22/40.34 thf(f12,plain,(
% 283.22/40.34 (dsetconstrEL = ((!! @ $i @ (^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ (dsetconstr @ Y0 @ (^[Y3 : $i]: (Y1 @ Y3)))) => (in @ Y2 @ Y0))))))))))),
% 283.22/40.34 inference(fool_elimination,[],[f11])).
% 283.22/40.34 thf(f13,plain,(
% 283.22/40.34 (dsetconstrER = ! [X0 : ($i > $o),X1 : $i,X2 : $i] : ((in @ X2 @ (dsetconstr @ X1 @ (^[X3 : $i] : ((X0 @ X3))))) => (X0 @ X2)))),
% 283.22/40.34 inference(rectify,[],[f3])).
% 283.22/40.34 thf(f14,plain,(
% 283.22/40.34 (dsetconstrER = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((in @ Y0 @ (dsetconstr @ Y1 @ (^[Y3 : $i]: (Y2 @ Y3)))) => (Y2 @ Y0))))))))))),
% 283.22/40.34 inference(fool_elimination,[],[f13])).
% 283.22/40.34 thf(f15,plain,(
% 283.22/40.34 ~(dsetconstrI => (dsetconstrEL => (dsetconstrER => (setext => ! [X0 : $i,X1 : $i] : ((X0 = X1) => ! [X2 : ($i > $o),X3 : ($i > $o)] : (! [X4 : $i] : ((in @ X4 @ X0) => ! [X5 : $i] : ((in @ X5 @ X1) => ((X4 = X5) => ((X3 @ X4) <=> (X2 @ X5))))) => (((dsetconstr @ X1 @ (^[X6 : $i] : ((X2 @ X6))))) = ((dsetconstr @ X0 @ (^[X7 : $i] : ((X3 @ X7))))))))))))),
% 283.22/40.34 inference(rectify,[],[f6])).
% 283.22/40.34 thf(f16,plain,(
% 283.22/40.34 ~((dsetconstrI = $true) => ((dsetconstrEL = $true) => ((dsetconstrER = $true) => ((setext = $true) => ! [X1 : $i,X0 : $i] : ((X0 = X1) => ! [X2 : ($i > $o),X3 : ($i > $o)] : (! [X4 : $i] : ((((in @ X4 @ X0)) = $true) => ! [X5 : $i] : ((((in @ X5 @ X1)) = $true) => ((X4 = X5) => (((X3 @ X4)) = ((X2 @ X5)))))) => (((dsetconstr @ X1 @ (^[Y0 : $i]: (X2 @ Y0)))) = ((dsetconstr @ X0 @ (^[Y0 : $i]: (X3 @ Y0)))))))))))),
% 283.22/40.34 inference(fool_elimination,[],[f15])).
% 283.22/40.34 thf(f17,plain,(
% 283.22/40.34 (((? [X1 : $i,X0 : $i] : (? [X2 : ($i > $o),X3 : ($i > $o)] : ((((dsetconstr @ X1 @ (^[Y0 : $i]: (X2 @ Y0)))) != ((dsetconstr @ X0 @ (^[Y0 : $i]: (X3 @ Y0))))) & ! [X4 : $i] : (! [X5 : $i] : (((((X3 @ X4)) = ((X2 @ X5))) | (X4 != X5)) | (((in @ X5 @ X1)) != $true)) | (((in @ X4 @ X0)) != $true))) & (X0 = X1)) & (setext = $true)) & (dsetconstrER = $true)) & (dsetconstrEL = $true)) & (dsetconstrI = $true)),
% 283.22/40.34 inference(ennf_transformation,[],[f16])).
% 283.22/40.34 thf(f18,plain,(
% 283.22/40.34 (setext = $true) & (dsetconstrEL = $true) & ? [X0 : $i,X1 : $i] : (? [X2 : ($i > $o),X3 : ($i > $o)] : (! [X4 : $i] : (! [X5 : $i] : ((((in @ X5 @ X1)) != $true) | (((X3 @ X4)) = ((X2 @ X5))) | (X4 != X5)) | (((in @ X4 @ X0)) != $true)) & (((dsetconstr @ X1 @ (^[Y0 : $i]: (X2 @ Y0)))) != ((dsetconstr @ X0 @ (^[Y0 : $i]: (X3 @ Y0)))))) & (X0 = X1)) & (dsetconstrI = $true) & (dsetconstrER = $true)),
% 283.22/40.34 inference(flattening,[],[f17])).
% 283.22/40.34 thf(f19,plain,(
% 283.22/40.34 (setext = $true) & (dsetconstrEL = $true) & ((! [X4 : $i] : (! [X5 : $i] : ((((in @ X5 @ sK1)) != $true) | (((sK2 @ X5)) = ((sK3 @ X4))) | (X4 != X5)) | (((in @ X4 @ sK0)) != $true)) & (((dsetconstr @ sK0 @ (^[Y0 : $i]: (sK3 @ Y0)))) != ((dsetconstr @ sK1 @ (^[Y0 : $i]: (sK2 @ Y0)))))) & (sK1 = sK0)) & (dsetconstrI = $true) & (dsetconstrER = $true)),
% 283.22/40.34 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3)],[f18])).
% 283.22/40.34 thf(f20,plain,(
% 283.22/40.34 (dsetconstrER = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((in @ Y0 @ (dsetconstr @ Y1 @ (^[Y3 : $i]: (Y2 @ Y3)))) => (Y2 @ Y0))))))))))),
% 283.22/40.34 inference(cnf_transformation,[],[f14])).
% 283.22/40.34 thf(f21,plain,(
% 283.22/40.34 (dsetconstrEL = ((!! @ $i @ (^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ (dsetconstr @ Y0 @ (^[Y3 : $i]: (Y1 @ Y3)))) => (in @ Y2 @ Y0))))))))))),
% 283.22/40.34 inference(cnf_transformation,[],[f12])).
% 283.22/40.34 thf(f22,plain,(
% 283.22/40.34 (setext = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y0) => (in @ Y2 @ Y1)))) => ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) => (in @ Y2 @ Y0)))) => (Y1 = Y0)))))))))),
% 283.22/40.34 inference(cnf_transformation,[],[f10])).
% 283.22/40.34 thf(f23,plain,(
% 283.22/40.34 (dsetconstrI = ((!! @ ($i > $o) @ (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) => ((Y0 @ Y2) => (in @ Y2 @ (dsetconstr @ Y1 @ (^[Y3 : $i]: (Y0 @ Y3))))))))))))))),
% 283.22/40.34 inference(cnf_transformation,[],[f8])).
% 283.22/40.34 thf(f24,plain,(
% 283.22/40.34 (dsetconstrER = $true)),
% 283.22/40.34 inference(cnf_transformation,[],[f19])).
% 283.22/40.34 thf(f25,plain,(
% 283.22/40.34 (dsetconstrI = $true)),
% 283.22/40.34 inference(cnf_transformation,[],[f19])).
% 283.22/40.34 thf(f26,plain,(
% 283.22/40.34 (sK1 = sK0)),
% 283.22/40.34 inference(cnf_transformation,[],[f19])).
% 283.22/40.34 thf(f27,plain,(
% 283.22/40.34 (((dsetconstr @ sK0 @ (^[Y0 : $i]: (sK3 @ Y0)))) != ((dsetconstr @ sK1 @ (^[Y0 : $i]: (sK2 @ Y0)))))),
% 283.22/40.34 inference(cnf_transformation,[],[f19])).
% 283.22/40.34 thf(f28,plain,(
% 283.22/40.34 ( ! [X4 : $i,X5 : $i] : ((((in @ X5 @ sK1)) != $true) | (((sK2 @ X5)) = ((sK3 @ X4))) | (X4 != X5) | (((in @ X4 @ sK0)) != $true)) )),
% 283.22/40.34 inference(cnf_transformation,[],[f19])).
% 283.22/40.34 thf(f29,plain,(
% 283.22/40.34 (dsetconstrEL = $true)),
% 283.22/40.34 inference(cnf_transformation,[],[f19])).
% 283.22/40.34 thf(f30,plain,(
% 283.22/40.34 (setext = $true)),
% 283.22/40.34 inference(cnf_transformation,[],[f19])).
% 283.22/40.34 thf(f32,definition,(
% 283.22/40.34 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 283.22/40.34 introduced(theory,[fool_exhaustiveness_axiom])).
% 283.22/40.34 thf(f33,plain,(
% 283.22/40.34 (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((in @ Y0 @ (dsetconstr @ Y1 @ (^[Y3 : $i]: (Y2 @ Y3)))) => (Y2 @ Y0))))))))) = $true)),
% 283.22/40.34 inference(definition_unfolding,[],[f20,f24])).
% 283.22/40.34 thf(f34,plain,(
% 283.22/40.34 (((!! @ $i @ (^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ (dsetconstr @ Y0 @ (^[Y3 : $i]: (Y1 @ Y3)))) => (in @ Y2 @ Y0))))))))) = $true)),
% 283.22/40.34 inference(definition_unfolding,[],[f21,f29])).
% 283.22/40.34 thf(f35,plain,(
% 283.22/40.34 (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y0) => (in @ Y2 @ Y1)))) => ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) => (in @ Y2 @ Y0)))) => (Y1 = Y0)))))))) = $true)),
% 283.22/40.34 inference(definition_unfolding,[],[f22,f30])).
% 283.22/40.34 thf(f36,plain,(
% 283.22/40.34 (((!! @ ($i > $o) @ (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) => ((Y0 @ Y2) => (in @ Y2 @ (dsetconstr @ Y1 @ (^[Y3 : $i]: (Y0 @ Y3))))))))))))) = $true)),
% 283.22/40.34 inference(definition_unfolding,[],[f23,f25])).
% 283.22/40.34 thf(f37,plain,(
% 283.22/40.34 ( ! [X4 : $i,X5 : $i] : ((((in @ X5 @ sK0)) != $true) | (((sK2 @ X5)) = ((sK3 @ X4))) | (X4 != X5) | (((in @ X4 @ sK0)) != $true)) )),
% 283.22/40.34 inference(definition_unfolding,[],[f28,f26])).
% 283.22/40.34 thf(f38,plain,(
% 283.22/40.34 (((dsetconstr @ sK0 @ (^[Y0 : $i]: (sK3 @ Y0)))) != ((dsetconstr @ sK0 @ (^[Y0 : $i]: (sK2 @ Y0)))))),
% 283.22/40.34 inference(definition_unfolding,[],[f27,f26])).
% 283.22/40.34 thf(f39,plain,(
% 283.22/40.34 ( ! [X5 : $i] : ((((in @ X5 @ sK0)) != $true) | (((in @ X5 @ sK0)) != $true) | (((sK3 @ X5)) = ((sK2 @ X5)))) )),
% 283.22/40.34 inference(equality_resolution,[],[f37])).
% 283.22/40.34 thf(f40,definition,(
% 283.22/40.34 (sF4 = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((in @ Y0 @ (dsetconstr @ Y1 @ (^[Y3 : $i]: (Y2 @ Y3)))) => (Y2 @ Y0))))))))))),
% 283.22/40.34 introduced(definition,[new_symbols(definition,[sF4])],[function_definition])).
% 283.22/40.34 thf(f41,plain,(
% 283.22/40.34 (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((in @ Y0 @ (dsetconstr @ Y1 @ (^[Y3 : $i]: (Y2 @ Y3)))) => (Y2 @ Y0))))))))) = sF4)),
% 283.22/40.34 inference(reorient_equations,[],[f40])).
% 283.22/40.34 thf(f42,plain,(
% 283.22/40.34 ($true = sF4)),
% 283.22/40.34 inference(definition_folding,[],[f33,f41])).
% 283.22/40.34 thf(f43,definition,(
% 283.22/40.34 (sF5 = ((!! @ $i @ (^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ (dsetconstr @ Y0 @ (^[Y3 : $i]: (Y1 @ Y3)))) => (in @ Y2 @ Y0))))))))))),
% 283.22/40.34 introduced(definition,[new_symbols(definition,[sF5])],[function_definition])).
% 283.22/40.34 thf(f44,plain,(
% 283.22/40.34 (sF5 = $true)),
% 283.22/40.34 inference(definition_folding,[],[f34,f43])).
% 283.22/40.34 thf(f45,definition,(
% 283.22/40.34 (sF6 = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y0) => (in @ Y2 @ Y1)))) => ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) => (in @ Y2 @ Y0)))) => (Y1 = Y0)))))))))),
% 283.22/40.34 introduced(definition,[new_symbols(definition,[sF6])],[function_definition])).
% 283.22/40.34 thf(f46,plain,(
% 283.22/40.34 (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y0) => (in @ Y2 @ Y1)))) => ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) => (in @ Y2 @ Y0)))) => (Y1 = Y0)))))))) = sF6)),
% 283.22/40.34 inference(reorient_equations,[],[f45])).
% 283.22/40.34 thf(f47,plain,(
% 283.22/40.34 ($true = sF6)),
% 283.22/40.34 inference(definition_folding,[],[f35,f46])).
% 283.22/40.34 thf(f48,definition,(
% 283.22/40.34 (sF7 = ((!! @ ($i > $o) @ (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) => ((Y0 @ Y2) => (in @ Y2 @ (dsetconstr @ Y1 @ (^[Y3 : $i]: (Y0 @ Y3))))))))))))))),
% 283.22/40.34 introduced(definition,[new_symbols(definition,[sF7])],[function_definition])).
% 283.22/40.34 thf(f49,plain,(
% 283.22/40.34 (sF7 = $true)),
% 283.22/40.34 inference(definition_folding,[],[f36,f48])).
% 283.22/40.34 thf(f50,definition,(
% 283.22/40.34 (sF8 = ((dsetconstr @ sK0 @ (^[Y0 : $i]: (sK3 @ Y0)))))),
% 283.22/40.34 introduced(definition,[new_symbols(definition,[sF8])],[function_definition])).
% 283.22/40.34 thf(f51,plain,(
% 283.22/40.34 (((dsetconstr @ sK0 @ (^[Y0 : $i]: (sK3 @ Y0)))) = sF8)),
% 283.22/40.34 inference(reorient_equations,[],[f50])).
% 283.22/40.34 thf(f52,definition,(
% 283.22/40.34 (sF9 = ((dsetconstr @ sK0 @ (^[Y0 : $i]: (sK2 @ Y0)))))),
% 283.22/40.34 introduced(definition,[new_symbols(definition,[sF9])],[function_definition])).
% 283.22/40.34 thf(f53,plain,(
% 283.22/40.34 (((dsetconstr @ sK0 @ (^[Y0 : $i]: (sK2 @ Y0)))) = sF9)),
% 283.22/40.34 inference(reorient_equations,[],[f52])).
% 283.22/40.34 thf(f54,plain,(
% 283.22/40.34 (sF8 != sF9)),
% 283.22/40.34 inference(definition_folding,[],[f38,f53,f51])).
% 283.22/40.34 thf(f55,plain,(
% 283.22/40.34 ($false = sF6) | (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y0) => (in @ Y2 @ Y1)))) => ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) => (in @ Y2 @ Y0)))) => (Y1 = Y0)))))))) = $true)),
% 283.22/40.34 inference(iff_proxy_clausification,[],[f46])).
% 283.22/40.34 thf(f72,plain,(
% 283.22/40.34 ( ! [X1 : $i] : (($false = sF6) | ((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y0) => (in @ Y2 @ Y1)))) => ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) => (in @ Y2 @ Y0)))) => (Y1 = Y0)))))) @ X1)) = $true)) )),
% 283.22/40.34 inference(pi_proxy_clausification,[],[f55])).
% 283.22/40.34 thf(f73,plain,(
% 283.22/40.34 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X1) => (in @ Y1 @ Y0)))) => ((!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ Y0) => (in @ Y1 @ X1)))) => (Y0 = X1))))))) | ($false = sF6)) )),
% 283.22/40.34 inference(beta-eta_normalization,[],[f72])).
% 283.22/40.34 thf(f74,plain,(
% 283.22/40.34 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X1) => (in @ Y1 @ Y0)))) => ((!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ Y0) => (in @ Y1 @ X1)))) => (Y0 = X1)))) @ X2))) | ($false = sF6)) )),
% 283.22/40.34 inference(pi_proxy_clausification,[],[f73])).
% 283.22/40.34 thf(f75,plain,(
% 283.22/40.34 ( ! [X2 : $i,X1 : $i] : (($true = (((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X1) => (in @ Y0 @ X2)))) => ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X2) => (in @ Y0 @ X1)))) => (X2 = X1))))) | ($false = sF6)) )),
% 283.22/40.34 inference(beta-eta_normalization,[],[f74])).
% 283.22/40.34 thf(f76,plain,(
% 283.22/40.34 ( ! [X2 : $i,X1 : $i] : ((((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X1) => (in @ Y0 @ X2))))) = $false) | ((((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X2) => (in @ Y0 @ X1)))) => (X2 = X1))) = $true) | ($false = sF6)) )),
% 283.22/40.34 inference(imp_proxy_clausification,[],[f75])).
% 283.22/40.34 thf(f77,plain,(
% 283.22/40.34 ( ! [X2 : $i,X1 : $i] : (((((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X2) => (in @ Y0 @ X1)))) => (X2 = X1))) = $true) | ($false = sF6) | ($false = (((^[Y0 : $i]: ((in @ Y0 @ X1) => (in @ Y0 @ X2))) @ (sK12 @ X1 @ X2))))) )),
% 283.22/40.34 inference(sigma_proxy_clausification,[],[f76])).
% 283.22/40.34 thf(f78,plain,(
% 283.22/40.34 ( ! [X2 : $i,X1 : $i] : ((((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X2) => (in @ Y0 @ X1))))) = $false) | ($true = ((X2 = X1))) | ($false = (((^[Y0 : $i]: ((in @ Y0 @ X1) => (in @ Y0 @ X2))) @ (sK12 @ X1 @ X2)))) | ($false = sF6)) )),
% 283.22/40.34 inference(imp_proxy_clausification,[],[f77])).
% 283.22/40.34 thf(f79,plain,(
% 283.22/40.34 ( ! [X2 : $i,X1 : $i] : (((((^[Y0 : $i]: ((in @ Y0 @ X2) => (in @ Y0 @ X1))) @ (sK13 @ X1 @ X2))) = $false) | ($false = (((^[Y0 : $i]: ((in @ Y0 @ X1) => (in @ Y0 @ X2))) @ (sK12 @ X1 @ X2)))) | ($false = sF6) | ($true = ((X2 = X1)))) )),
% 283.22/40.34 inference(sigma_proxy_clausification,[],[f78])).
% 283.22/40.34 thf(f80,plain,(
% 283.22/40.34 ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ((in @ Y0 @ X1) => (in @ Y0 @ X2))) @ (sK12 @ X1 @ X2)))) | (X1 = X2) | ((((^[Y0 : $i]: ((in @ Y0 @ X2) => (in @ Y0 @ X1))) @ (sK13 @ X1 @ X2))) = $false) | ($false = sF6)) )),
% 283.22/40.34 inference(equality_proxy_clausification,[],[f79])).
% 283.22/40.34 thf(f81,plain,(
% 283.22/40.34 ( ! [X2 : $i,X1 : $i] : (((((in @ (sK13 @ X1 @ X2) @ X2) => (in @ (sK13 @ X1 @ X2) @ X1))) = $false) | ($false = (((in @ (sK12 @ X1 @ X2) @ X1) => (in @ (sK12 @ X1 @ X2) @ X2)))) | ($false = sF6) | (X1 = X2)) )),
% 283.22/40.34 inference(beta-eta_normalization,[],[f80])).
% 283.22/40.34 thf(f82,plain,(
% 283.22/40.34 ( ! [X2 : $i,X1 : $i] : (($false = (((in @ (sK12 @ X1 @ X2) @ X1) => (in @ (sK12 @ X1 @ X2) @ X2)))) | (((in @ (sK13 @ X1 @ X2) @ X1)) = $false) | (X1 = X2) | ($false = sF6)) )),
% 283.22/40.34 inference(imp_proxy_clausification,[],[f81])).
% 283.22/40.34 thf(f83,plain,(
% 283.22/40.34 ( ! [X2 : $i,X1 : $i] : (($false = (((in @ (sK12 @ X1 @ X2) @ X1) => (in @ (sK12 @ X1 @ X2) @ X2)))) | ($false = sF6) | (X1 = X2) | (((in @ (sK13 @ X1 @ X2) @ X2)) = $true)) )),
% 283.22/40.34 inference(imp_proxy_clausification,[],[f81])).
% 283.22/40.34 thf(f84,plain,(
% 283.22/40.34 ( ! [X2 : $i,X1 : $i] : ((((in @ (sK13 @ X1 @ X2) @ X2)) = $true) | ($false = sF6) | (X1 = X2) | ($false = ((in @ (sK12 @ X1 @ X2) @ X2)))) )),
% 283.22/40.34 inference(imp_proxy_clausification,[],[f83])).
% 283.22/40.34 thf(f85,plain,(
% 283.22/40.34 ( ! [X2 : $i,X1 : $i] : ((((in @ (sK13 @ X1 @ X2) @ X2)) = $true) | (((in @ (sK12 @ X1 @ X2) @ X1)) = $true) | ($false = sF6) | (X1 = X2)) )),
% 283.22/40.34 inference(imp_proxy_clausification,[],[f83])).
% 283.22/40.34 thf(f86,plain,(
% 283.22/40.34 ( ! [X2 : $i,X1 : $i] : (($false = ((in @ (sK12 @ X1 @ X2) @ X2))) | (((in @ (sK13 @ X1 @ X2) @ X1)) = $false) | ($false = sF6) | (X1 = X2)) )),
% 283.22/40.34 inference(imp_proxy_clausification,[],[f82])).
% 283.22/40.34 thf(f87,plain,(
% 283.22/40.34 ( ! [X2 : $i,X1 : $i] : ((((in @ (sK13 @ X1 @ X2) @ X1)) = $false) | (((in @ (sK12 @ X1 @ X2) @ X1)) = $true) | ($false = sF6) | (X1 = X2)) )),
% 283.22/40.34 inference(imp_proxy_clausification,[],[f82])).
% 283.22/40.34 thf(f89,plain,(
% 283.22/40.34 (sF5 = $false) | (((!! @ $i @ (^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ (dsetconstr @ Y0 @ (^[Y3 : $i]: (Y1 @ Y3)))) => (in @ Y2 @ Y0))))))))) = $true)),
% 283.22/40.34 inference(iff_proxy_clausification,[],[f43])).
% 283.22/40.34 thf(f90,plain,(
% 283.22/40.34 ( ! [X1 : $i] : (((((^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ (dsetconstr @ Y0 @ (^[Y3 : $i]: (Y1 @ Y3)))) => (in @ Y2 @ Y0))))))) @ X1)) = $true) | (sF5 = $false)) )),
% 283.22/40.34 inference(pi_proxy_clausification,[],[f89])).
% 283.22/40.34 thf(f91,plain,(
% 283.22/40.34 ( ! [X1 : $i] : ((((!! @ ($i > $o) @ (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ (dsetconstr @ X1 @ Y0)) => (in @ Y1 @ X1))))))) = $true) | (sF5 = $false)) )),
% 283.22/40.34 inference(beta-eta_normalization,[],[f90])).
% 283.22/40.34 thf(f92,plain,(
% 283.22/40.34 ( ! [X2 : ($i > $o),X1 : $i] : ((sF5 = $false) | ($true = (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ (dsetconstr @ X1 @ Y0)) => (in @ Y1 @ X1))))) @ X2)))) )),
% 283.22/40.34 inference(pi_proxy_clausification,[],[f91])).
% 283.22/40.34 thf(f93,plain,(
% 283.22/40.34 ( ! [X2 : ($i > $o),X1 : $i] : ((sF5 = $false) | (((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ (dsetconstr @ X1 @ X2)) => (in @ Y0 @ X1))))) = $true)) )),
% 283.22/40.34 inference(beta-eta_normalization,[],[f92])).
% 283.22/40.34 thf(f94,plain,(
% 283.22/40.34 ( ! [X2 : ($i > $o),X3 : $i,X1 : $i] : ((sF5 = $false) | ((((^[Y0 : $i]: ((in @ Y0 @ (dsetconstr @ X1 @ X2)) => (in @ Y0 @ X1))) @ X3)) = $true)) )),
% 283.22/40.34 inference(pi_proxy_clausification,[],[f93])).
% 283.22/40.34 thf(f95,plain,(
% 283.22/40.34 ( ! [X2 : ($i > $o),X3 : $i,X1 : $i] : (((((in @ X3 @ (dsetconstr @ X1 @ X2)) => (in @ X3 @ X1))) = $true) | (sF5 = $false)) )),
% 283.22/40.34 inference(beta-eta_normalization,[],[f94])).
% 283.22/40.34 thf(f96,plain,(
% 283.22/40.34 ( ! [X2 : ($i > $o),X3 : $i,X1 : $i] : (($false = ((in @ X3 @ (dsetconstr @ X1 @ X2)))) | (sF5 = $false) | ($true = ((in @ X3 @ X1)))) )),
% 283.22/40.34 inference(imp_proxy_clausification,[],[f95])).
% 283.22/40.34 thf(f105,plain,(
% 283.22/40.34 ( ! [X5 : $i] : ((((in @ X5 @ sK0)) != $true) | (((in @ X5 @ sK0)) != $true) | ($false = ((sK2 @ X5))) | (((sK3 @ X5)) = $true)) )),
% 283.22/40.34 inference(iff_proxy_clausification,[],[f39])).
% 283.22/40.34 thf(f106,plain,(
% 283.22/40.34 ( ! [X5 : $i] : ((((sK3 @ X5)) = $false) | (((in @ X5 @ sK0)) != $true) | (((sK2 @ X5)) = $true) | (((in @ X5 @ sK0)) != $true)) )),
% 283.22/40.34 inference(iff_proxy_clausification,[],[f39])).
% 283.22/40.34 thf(f107,plain,(
% 283.22/40.34 ( ! [X5 : $i] : ((((in @ X5 @ sK0)) != $true) | (((sK2 @ X5)) = $true) | (((sK3 @ X5)) = $false)) )),
% 283.22/40.34 inference(duplicate_literal_removal,[],[f106])).
% 283.22/40.34 thf(f108,plain,(
% 283.22/40.34 ( ! [X5 : $i] : ((((in @ X5 @ sK0)) != $true) | (((sK3 @ X5)) = $true) | ($false = ((sK2 @ X5)))) )),
% 283.22/40.34 inference(duplicate_literal_removal,[],[f105])).
% 283.22/40.34 thf(f109,plain,(
% 283.22/40.34 (sF9 = ((dsetconstr @ sK0 @ sK2)))),
% 283.22/40.34 inference(beta-eta_normalization,[],[f53])).
% 283.22/40.34 thf(f110,plain,(
% 283.22/40.34 (sF8 = ((dsetconstr @ sK0 @ sK3)))),
% 283.22/40.34 inference(beta-eta_normalization,[],[f51])).
% 283.22/40.34 thf(f112,plain,(
% 283.22/40.34 (((!! @ ($i > $o) @ (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) => ((Y0 @ Y2) => (in @ Y2 @ (dsetconstr @ Y1 @ (^[Y3 : $i]: (Y0 @ Y3))))))))))))) = $true) | (sF7 = $false)),
% 283.22/40.34 inference(iff_proxy_clausification,[],[f48])).
% 283.22/40.34 thf(f113,plain,(
% 283.22/40.34 ( ! [X1 : ($i > $o)] : (((((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) => ((Y0 @ Y2) => (in @ Y2 @ (dsetconstr @ Y1 @ (^[Y3 : $i]: (Y0 @ Y3))))))))))) @ X1)) = $true) | (sF7 = $false)) )),
% 283.22/40.34 inference(pi_proxy_clausification,[],[f112])).
% 283.22/40.34 thf(f114,plain,(
% 283.22/40.34 ( ! [X1 : ($i > $o)] : ((sF7 = $false) | (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ Y0) => ((X1 @ Y1) => (in @ Y1 @ (dsetconstr @ Y0 @ X1))))))))) = $true)) )),
% 283.22/40.34 inference(beta-eta_normalization,[],[f113])).
% 283.22/40.34 thf(f115,plain,(
% 283.22/40.34 ( ! [X2 : $i,X1 : ($i > $o)] : (((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ Y0) => ((X1 @ Y1) => (in @ Y1 @ (dsetconstr @ Y0 @ X1))))))) @ X2)) = $true) | (sF7 = $false)) )),
% 283.22/40.34 inference(pi_proxy_clausification,[],[f114])).
% 283.22/40.34 thf(f116,plain,(
% 283.22/40.34 ( ! [X2 : $i,X1 : ($i > $o)] : ((sF7 = $false) | (((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X2) => ((X1 @ Y0) => (in @ Y0 @ (dsetconstr @ X2 @ X1))))))) = $true)) )),
% 283.22/40.34 inference(beta-eta_normalization,[],[f115])).
% 283.22/40.34 thf(f117,plain,(
% 283.22/40.34 ( ! [X2 : $i,X3 : $i,X1 : ($i > $o)] : (($true = (((^[Y0 : $i]: ((in @ Y0 @ X2) => ((X1 @ Y0) => (in @ Y0 @ (dsetconstr @ X2 @ X1))))) @ X3))) | (sF7 = $false)) )),
% 283.22/40.34 inference(pi_proxy_clausification,[],[f116])).
% 283.22/40.34 thf(f118,plain,(
% 283.22/40.34 ( ! [X2 : $i,X3 : $i,X1 : ($i > $o)] : ((sF7 = $false) | ((((in @ X3 @ X2) => ((X1 @ X3) => (in @ X3 @ (dsetconstr @ X2 @ X1))))) = $true)) )),
% 283.22/40.34 inference(beta-eta_normalization,[],[f117])).
% 283.22/40.34 thf(f119,plain,(
% 283.22/40.34 ( ! [X2 : $i,X3 : $i,X1 : ($i > $o)] : (((((X1 @ X3) => (in @ X3 @ (dsetconstr @ X2 @ X1)))) = $true) | (((in @ X3 @ X2)) = $false) | (sF7 = $false)) )),
% 283.22/40.34 inference(imp_proxy_clausification,[],[f118])).
% 283.22/40.34 thf(f120,plain,(
% 283.22/40.34 ( ! [X2 : $i,X3 : $i,X1 : ($i > $o)] : ((((in @ X3 @ X2)) = $false) | (sF7 = $false) | (((in @ X3 @ (dsetconstr @ X2 @ X1))) = $true) | (((X1 @ X3)) = $false)) )),
% 283.22/40.34 inference(imp_proxy_clausification,[],[f119])).
% 283.22/40.34 thf(f131,plain,(
% 283.22/40.34 ($false = sF4) | (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((in @ Y0 @ (dsetconstr @ Y1 @ (^[Y3 : $i]: (Y2 @ Y3)))) => (Y2 @ Y0))))))))) = $true)),
% 283.22/40.34 inference(iff_proxy_clausification,[],[f41])).
% 283.22/40.34 thf(f141,plain,(
% 283.22/40.34 ( ! [X1 : $i] : (((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((in @ Y0 @ (dsetconstr @ Y1 @ (^[Y3 : $i]: (Y2 @ Y3)))) => (Y2 @ Y0))))))) @ X1)) = $true) | ($false = sF4)) )),
% 283.22/40.34 inference(pi_proxy_clausification,[],[f131])).
% 283.22/40.34 thf(f142,plain,(
% 283.22/40.34 ( ! [X1 : $i] : (($false = sF4) | (((!! @ $i @ (^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: ((in @ X1 @ (dsetconstr @ Y0 @ Y1)) => (Y1 @ X1))))))) = $true)) )),
% 283.22/40.34 inference(beta-eta_normalization,[],[f141])).
% 283.22/40.34 thf(f143,plain,(
% 283.22/40.34 ( ! [X2 : $i,X1 : $i] : (($false = sF4) | ((((^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: ((in @ X1 @ (dsetconstr @ Y0 @ Y1)) => (Y1 @ X1))))) @ X2)) = $true)) )),
% 283.22/40.34 inference(pi_proxy_clausification,[],[f142])).
% 283.22/40.34 thf(f144,plain,(
% 283.22/40.34 ( ! [X2 : $i,X1 : $i] : ((((!! @ ($i > $o) @ (^[Y0 : $i > $o]: ((in @ X1 @ (dsetconstr @ X2 @ Y0)) => (Y0 @ X1))))) = $true) | ($false = sF4)) )),
% 283.22/40.34 inference(beta-eta_normalization,[],[f143])).
% 283.22/40.34 thf(f145,plain,(
% 283.22/40.34 ( ! [X2 : $i,X3 : ($i > $o),X1 : $i] : (($false = sF4) | ((((^[Y0 : $i > $o]: ((in @ X1 @ (dsetconstr @ X2 @ Y0)) => (Y0 @ X1))) @ X3)) = $true)) )),
% 283.22/40.34 inference(pi_proxy_clausification,[],[f144])).
% 283.22/40.34 thf(f146,plain,(
% 283.22/40.34 ( ! [X2 : $i,X3 : ($i > $o),X1 : $i] : (((((in @ X1 @ (dsetconstr @ X2 @ X3)) => (X3 @ X1))) = $true) | ($false = sF4)) )),
% 283.22/40.34 inference(beta-eta_normalization,[],[f145])).
% 283.22/40.34 thf(f147,plain,(
% 283.22/40.34 ( ! [X2 : $i,X3 : ($i > $o),X1 : $i] : (($false = sF4) | (((in @ X1 @ (dsetconstr @ X2 @ X3))) = $false) | ($true = ((X3 @ X1)))) )),
% 283.22/40.34 inference(imp_proxy_clausification,[],[f146])).
% 283.22/40.34 thf(f148,plain,(
% 283.22/40.34 ( ! [X2 : $i,X3 : $i,X1 : ($i > $o)] : ((((in @ X3 @ X2)) = $false) | ($false = $true) | (((in @ X3 @ (dsetconstr @ X2 @ X1))) = $true) | (((X1 @ X3)) = $false)) )),
% 283.22/40.34 inference(forward_demodulation,[],[f120,f49])).
% 283.22/40.34 thf(f149,plain,(
% 283.22/40.34 ( ! [X2 : $i,X3 : $i,X1 : ($i > $o)] : ((((in @ X3 @ (dsetconstr @ X2 @ X1))) = $true) | (((X1 @ X3)) = $false) | (((in @ X3 @ X2)) = $false)) )),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f148])).
% 283.22/40.34 thf(f150,plain,(
% 283.22/40.34 ( ! [X2 : $i,X3 : ($i > $o),X1 : $i] : (($false = $true) | (((in @ X1 @ (dsetconstr @ X2 @ X3))) = $false) | ($true = ((X3 @ X1)))) )),
% 283.22/40.34 inference(forward_demodulation,[],[f147,f42])).
% 283.22/40.34 thf(f151,plain,(
% 283.22/40.34 ( ! [X2 : $i,X3 : ($i > $o),X1 : $i] : ((((in @ X1 @ (dsetconstr @ X2 @ X3))) = $false) | ($true = ((X3 @ X1)))) )),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f150])).
% 283.22/40.34 thf(f154,plain,(
% 283.22/40.34 ( ! [X0 : $i] : (($true = ((sK2 @ X0))) | (((in @ X0 @ sK0)) = $false) | ($true != $true) | ($false = ((sK3 @ X0)))) )),
% 283.22/40.34 inference(constrained_superposition,[],[f107,f32])).
% 283.22/40.34 thf(f156,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((in @ X0 @ sK0)) = $false) | ($false = ((sK3 @ X0))) | ($true = ((sK2 @ X0)))) )),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f154])).
% 283.22/40.34 thf(f161,plain,(
% 283.22/40.34 ( ! [X0 : $i] : (($true != $true) | (((in @ X0 @ sK0)) = $false) | ($false = ((sK2 @ X0))) | (((sK3 @ X0)) = $true)) )),
% 283.22/40.34 inference(constrained_superposition,[],[f108,f32])).
% 283.22/40.34 thf(f162,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((in @ X0 @ sK0)) = $false) | (((sK3 @ X0)) = $true) | ($false = ((sK2 @ X0)))) )),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f161])).
% 283.22/40.34 thf(f173,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((in @ X0 @ sF9)) = $false) | ($true = ((sK2 @ X0)))) )),
% 283.22/40.34 inference(constrained_superposition,[],[f151,f109])).
% 283.22/40.34 thf(f174,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((in @ X0 @ sF8)) = $false) | (((sK3 @ X0)) = $true)) )),
% 283.22/40.34 inference(constrained_superposition,[],[f151,f110])).
% 283.22/40.34 thf(f183,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((in @ X0 @ sF9)) = $true) | ($false = ((sK2 @ X0))) | (((in @ X0 @ sK0)) = $false)) )),
% 283.22/40.34 inference(constrained_superposition,[],[f149,f109])).
% 283.22/40.34 thf(f184,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((in @ X0 @ sF8)) = $true) | (((in @ X0 @ sK0)) = $false) | ($false = ((sK3 @ X0)))) )),
% 283.22/40.34 inference(constrained_superposition,[],[f149,f110])).
% 283.22/40.34 thf(f195,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((in @ X0 @ sK0)) = $true) | (sF5 = $false) | (((in @ X0 @ sF9)) = $false)) )),
% 283.22/40.34 inference(constrained_superposition,[],[f96,f109])).
% 283.22/40.34 thf(f196,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((in @ X0 @ sK0)) = $true) | (sF5 = $false) | (((in @ X0 @ sF8)) = $false)) )),
% 283.22/40.34 inference(constrained_superposition,[],[f96,f110])).
% 283.22/40.34 thf(f203,plain,(
% 283.22/40.34 ( ! [X0 : $i] : (($false = $true) | (((in @ X0 @ sF9)) = $false) | (((in @ X0 @ sK0)) = $true)) )),
% 283.22/40.34 inference(forward_demodulation,[],[f195,f44])).
% 283.22/40.34 thf(f204,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((in @ X0 @ sF9)) = $false) | (((in @ X0 @ sK0)) = $true)) )),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f203])).
% 283.22/40.34 thf(f205,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((in @ X0 @ sF8)) = $false) | (((in @ X0 @ sK0)) = $true) | ($false = $true)) )),
% 283.22/40.34 inference(forward_demodulation,[],[f196,f44])).
% 283.22/40.34 thf(f206,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((in @ X0 @ sF8)) = $false) | (((in @ X0 @ sK0)) = $true)) )),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f205])).
% 283.22/40.34 thf(f262,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((sF9 = X0) | (((in @ (sK12 @ X0 @ sF9) @ sF9)) = $false) | (((in @ (sK13 @ X0 @ sF9) @ sK0)) = $true) | ($false = sF6) | ($false = $true)) )),
% 283.22/40.34 inference(constrained_superposition,[],[f204,f84])).
% 283.22/40.34 thf(f263,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((in @ (sK12 @ X0 @ sF9) @ sF9)) = $false) | ($false = $true) | ($false = sF6) | (sF9 = X0) | ($true = ((sK2 @ (sK13 @ X0 @ sF9))))) )),
% 283.22/40.34 inference(constrained_superposition,[],[f173,f84])).
% 283.22/40.34 thf(f274,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((sF9 = X0) | (((in @ (sK13 @ X0 @ sF9) @ sK0)) = $true) | ($false = sF6) | (((in @ (sK12 @ X0 @ sF9) @ sF9)) = $false)) )),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f262])).
% 283.22/40.34 thf(f275,plain,(
% 283.22/40.34 ( ! [X0 : $i] : (($true = ((sK2 @ (sK13 @ X0 @ sF9)))) | (sF9 = X0) | (((in @ (sK12 @ X0 @ sF9) @ sF9)) = $false) | ($false = sF6)) )),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f263])).
% 283.22/40.34 thf(f299,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((in @ (sK13 @ X0 @ sF9) @ sK0)) = $true) | (((in @ (sK12 @ X0 @ sF9) @ sF9)) = $false) | (sF9 = X0) | ($false = $true)) )),
% 283.22/40.34 inference(forward_demodulation,[],[f274,f47])).
% 283.22/40.34 thf(f300,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((in @ (sK13 @ X0 @ sF9) @ sK0)) = $true) | (((in @ (sK12 @ X0 @ sF9) @ sF9)) = $false) | (sF9 = X0)) )),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f299])).
% 283.22/40.34 thf(f301,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((sF9 = X0) | ($false = $true) | ($true = ((sK2 @ (sK13 @ X0 @ sF9)))) | (((in @ (sK12 @ X0 @ sF9) @ sF9)) = $false)) )),
% 283.22/40.34 inference(forward_demodulation,[],[f275,f47])).
% 283.22/40.34 thf(f302,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((in @ (sK12 @ X0 @ sF9) @ sF9)) = $false) | (sF9 = X0) | ($true = ((sK2 @ (sK13 @ X0 @ sF9))))) )),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f301])).
% 283.22/40.34 thf(f337,plain,(
% 283.22/40.34 ( ! [X0 : $i] : (($false = sF6) | (((in @ (sK13 @ X0 @ sF9) @ sK0)) = $true) | (sF9 = X0) | ($false = $true) | (((in @ (sK12 @ X0 @ sF9) @ X0)) = $true)) )),
% 283.22/40.34 inference(constrained_superposition,[],[f85,f204])).
% 283.22/40.34 thf(f341,plain,(
% 283.22/40.34 ( ! [X2 : $i,X0 : $i,X1 : ($i > $o)] : (($false = sF6) | ($false = $true) | ($true = ((X1 @ (sK12 @ (dsetconstr @ X0 @ X1) @ X2)))) | ($true = ((in @ (sK13 @ (dsetconstr @ X0 @ X1) @ X2) @ X2))) | (((dsetconstr @ X0 @ X1)) = X2)) )),
% 283.22/40.34 inference(constrained_superposition,[],[f85,f151])).
% 283.22/40.34 thf(f351,plain,(
% 283.22/40.34 ( ! [X0 : $i] : (($false = sF6) | (((in @ (sK12 @ X0 @ sF9) @ X0)) = $true) | ($true = ((sK2 @ (sK13 @ X0 @ sF9)))) | ($false = $true) | (sF9 = X0)) )),
% 283.22/40.34 inference(constrained_superposition,[],[f173,f85])).
% 283.22/40.34 thf(f353,plain,(
% 283.22/40.34 ( ! [X2 : $i,X0 : $i,X1 : ($i > $o)] : ((((in @ (sK12 @ (dsetconstr @ X0 @ X1) @ X2) @ X0)) = $true) | ($false = $true) | (((dsetconstr @ X0 @ X1)) = X2) | (sF5 = $false) | ($true = ((in @ (sK13 @ (dsetconstr @ X0 @ X1) @ X2) @ X2))) | ($false = sF6)) )),
% 283.22/40.34 inference(constrained_superposition,[],[f96,f85])).
% 283.22/40.34 thf(f360,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((in @ (sK12 @ X0 @ sF9) @ X0)) = $true) | ($true = ((sK2 @ (sK13 @ X0 @ sF9)))) | ($false = sF6) | (sF9 = X0)) )),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f351])).
% 283.22/40.34 thf(f361,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((in @ (sK13 @ X0 @ sF9) @ sK0)) = $true) | ($false = sF6) | (((in @ (sK12 @ X0 @ sF9) @ X0)) = $true) | (sF9 = X0)) )),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f337])).
% 283.22/40.34 thf(f362,plain,(
% 283.22/40.34 ( ! [X2 : $i,X0 : $i,X1 : ($i > $o)] : (($true = ((in @ (sK13 @ (dsetconstr @ X0 @ X1) @ X2) @ X2))) | (((in @ (sK12 @ (dsetconstr @ X0 @ X1) @ X2) @ X0)) = $true) | ($false = sF6) | (sF5 = $false) | (((dsetconstr @ X0 @ X1)) = X2)) )),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f353])).
% 283.22/40.34 thf(f368,plain,(
% 283.22/40.34 ( ! [X2 : $i,X0 : $i,X1 : ($i > $o)] : (($true = ((X1 @ (sK12 @ (dsetconstr @ X0 @ X1) @ X2)))) | ($true = ((in @ (sK13 @ (dsetconstr @ X0 @ X1) @ X2) @ X2))) | (((dsetconstr @ X0 @ X1)) = X2) | ($false = sF6)) )),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f341])).
% 283.22/40.34 thf(f389,plain,(
% 283.22/40.34 ( ! [X0 : $i] : (($false = $true) | ($true = ((sK2 @ (sK13 @ X0 @ sF9)))) | (((in @ (sK12 @ X0 @ sF9) @ X0)) = $true) | (sF9 = X0)) )),
% 283.22/40.34 inference(forward_demodulation,[],[f360,f47])).
% 283.22/40.34 thf(f390,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((in @ (sK12 @ X0 @ sF9) @ X0)) = $true) | ($true = ((sK2 @ (sK13 @ X0 @ sF9)))) | (sF9 = X0)) )),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f389])).
% 283.22/40.34 thf(f391,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((in @ (sK12 @ X0 @ sF9) @ X0)) = $true) | (sF9 = X0) | (((in @ (sK13 @ X0 @ sF9) @ sK0)) = $true) | ($false = $true)) )),
% 283.22/40.34 inference(forward_demodulation,[],[f361,f47])).
% 283.22/40.34 thf(f392,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((in @ (sK13 @ X0 @ sF9) @ sK0)) = $true) | (((in @ (sK12 @ X0 @ sF9) @ X0)) = $true) | (sF9 = X0)) )),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f391])).
% 283.22/40.34 thf(f393,plain,(
% 283.22/40.34 ( ! [X2 : $i,X0 : $i,X1 : ($i > $o)] : (($false = $true) | ($true = ((in @ (sK13 @ (dsetconstr @ X0 @ X1) @ X2) @ X2))) | (((in @ (sK12 @ (dsetconstr @ X0 @ X1) @ X2) @ X0)) = $true) | (sF5 = $false) | (((dsetconstr @ X0 @ X1)) = X2)) )),
% 283.22/40.34 inference(forward_demodulation,[],[f362,f47])).
% 283.22/40.34 thf(f394,plain,(
% 283.22/40.34 ( ! [X2 : $i,X0 : $i,X1 : ($i > $o)] : ((sF5 = $false) | (((dsetconstr @ X0 @ X1)) = X2) | (((in @ (sK12 @ (dsetconstr @ X0 @ X1) @ X2) @ X0)) = $true) | ($true = ((in @ (sK13 @ (dsetconstr @ X0 @ X1) @ X2) @ X2)))) )),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f393])).
% 283.22/40.34 thf(f403,plain,(
% 283.22/40.34 ( ! [X2 : $i,X0 : $i,X1 : ($i > $o)] : (($false = $true) | ($true = ((in @ (sK13 @ (dsetconstr @ X0 @ X1) @ X2) @ X2))) | (((dsetconstr @ X0 @ X1)) = X2) | ($true = ((X1 @ (sK12 @ (dsetconstr @ X0 @ X1) @ X2))))) )),
% 283.22/40.34 inference(forward_demodulation,[],[f368,f47])).
% 283.22/40.34 thf(f404,plain,(
% 283.22/40.34 ( ! [X2 : $i,X0 : $i,X1 : ($i > $o)] : (($true = ((in @ (sK13 @ (dsetconstr @ X0 @ X1) @ X2) @ X2))) | ($true = ((X1 @ (sK12 @ (dsetconstr @ X0 @ X1) @ X2)))) | (((dsetconstr @ X0 @ X1)) = X2)) )),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f403])).
% 283.22/40.34 thf(f423,plain,(
% 283.22/40.34 ( ! [X2 : $i,X0 : $i,X1 : ($i > $o)] : ((((dsetconstr @ X0 @ X1)) = X2) | (((in @ (sK12 @ (dsetconstr @ X0 @ X1) @ X2) @ X0)) = $true) | ($true = ((in @ (sK13 @ (dsetconstr @ X0 @ X1) @ X2) @ X2))) | ($false = $true)) )),
% 283.22/40.34 inference(forward_demodulation,[],[f394,f44])).
% 283.22/40.34 thf(f424,plain,(
% 283.22/40.34 ( ! [X2 : $i,X0 : $i,X1 : ($i > $o)] : (($true = ((in @ (sK13 @ (dsetconstr @ X0 @ X1) @ X2) @ X2))) | (((in @ (sK12 @ (dsetconstr @ X0 @ X1) @ X2) @ X0)) = $true) | (((dsetconstr @ X0 @ X1)) = X2)) )),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f423])).
% 283.22/40.34 thf(f433,plain,(
% 283.22/40.34 ( ! [X0 : $i] : (($false = ((sK2 @ (sK12 @ X0 @ sF9)))) | ($false = $true) | (sF9 = X0) | (((in @ (sK12 @ X0 @ sF9) @ sK0)) = $false) | ($true = ((sK2 @ (sK13 @ X0 @ sF9))))) )),
% 283.22/40.34 inference(constrained_superposition,[],[f183,f302])).
% 283.22/40.34 thf(f434,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((in @ (sK12 @ X0 @ sF9) @ sK0)) = $false) | ($true = ((sK2 @ (sK13 @ X0 @ sF9)))) | ($false = ((sK2 @ (sK12 @ X0 @ sF9)))) | (sF9 = X0)) )),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f433])).
% 283.22/40.34 thf(f448,plain,(
% 283.22/40.34 ( ! [X0 : $i] : (($false = $true) | ($false = sF6) | (((in @ (sK13 @ sF8 @ X0) @ sK0)) = $false) | ($false = ((in @ (sK12 @ sF8 @ X0) @ X0))) | (sF8 = X0) | (((sK3 @ (sK13 @ sF8 @ X0))) = $false)) )),
% 283.22/40.34 inference(constrained_superposition,[],[f184,f86])).
% 283.22/40.34 thf(f455,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((sF8 = X0) | ($false = sF6) | ($false = ((in @ (sK12 @ sF8 @ X0) @ X0))) | (((sK3 @ (sK13 @ sF8 @ X0))) = $false) | (((in @ (sK13 @ sF8 @ X0) @ sK0)) = $false)) )),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f448])).
% 283.22/40.34 thf(f467,plain,(
% 283.22/40.34 ( ! [X0 : $i] : (($false = ((in @ (sK12 @ sF8 @ X0) @ X0))) | (((sK3 @ (sK13 @ sF8 @ X0))) = $false) | (sF8 = X0) | ($false = $true) | (((in @ (sK13 @ sF8 @ X0) @ sK0)) = $false)) )),
% 283.22/40.34 inference(forward_demodulation,[],[f455,f47])).
% 283.22/40.34 thf(f468,plain,(
% 283.22/40.34 ( ! [X0 : $i] : (($false = ((in @ (sK12 @ sF8 @ X0) @ X0))) | (((in @ (sK13 @ sF8 @ X0) @ sK0)) = $false) | (sF8 = X0) | (((sK3 @ (sK13 @ sF8 @ X0))) = $false)) )),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f467])).
% 283.22/40.34 thf(f527,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((sK3 @ (sK13 @ sF8 @ X0))) = $false) | (((in @ (sK13 @ sF8 @ X0) @ sK0)) = $false) | ($false = sF6) | (sF8 = X0) | (((in @ (sK12 @ sF8 @ X0) @ sF8)) = $true) | ($false = $true)) )),
% 283.22/40.34 inference(constrained_superposition,[],[f184,f87])).
% 283.22/40.34 thf(f534,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((in @ (sK13 @ sF8 @ X0) @ sK0)) = $false) | ($false = sF6) | (((in @ (sK12 @ sF8 @ X0) @ sF8)) = $true) | (sF8 = X0) | (((sK3 @ (sK13 @ sF8 @ X0))) = $false)) )),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f527])).
% 283.22/40.34 thf(f543,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((sK3 @ (sK13 @ sF8 @ X0))) = $false) | (sF8 = X0) | (((in @ (sK12 @ sF8 @ X0) @ sF8)) = $true) | (((in @ (sK13 @ sF8 @ X0) @ sK0)) = $false) | ($false = $true)) )),
% 283.22/40.34 inference(forward_demodulation,[],[f534,f47])).
% 283.22/40.34 thf(f544,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((in @ (sK13 @ sF8 @ X0) @ sK0)) = $false) | (((in @ (sK12 @ sF8 @ X0) @ sF8)) = $true) | (sF8 = X0) | (((sK3 @ (sK13 @ sF8 @ X0))) = $false)) )),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f543])).
% 283.22/40.34 thf(f556,plain,(
% 283.22/40.34 ($false = $true) | (((sK3 @ (sK12 @ sF8 @ sF9))) = $true) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $true) | (sF8 = sF9)),
% 283.22/40.34 inference(constrained_superposition,[],[f390,f174])).
% 283.22/40.34 thf(f564,plain,(
% 283.22/40.34 (sF8 = sF9) | ($false = $true) | (((in @ (sK12 @ sF8 @ sF9) @ sK0)) = $true) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $true)),
% 283.22/40.34 inference(constrained_superposition,[],[f206,f390])).
% 283.22/40.34 thf(f569,plain,(
% 283.22/40.34 (((sK2 @ (sK13 @ sF8 @ sF9))) = $true) | (((sK3 @ (sK12 @ sF8 @ sF9))) = $true) | (sF8 = sF9)),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f556])).
% 283.22/40.34 thf(f572,plain,(
% 283.22/40.34 (((in @ (sK12 @ sF8 @ sF9) @ sK0)) = $true) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $true) | (sF8 = sF9)),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f564])).
% 283.22/40.34 thf(f585,plain,(
% 283.22/40.34 (((sK3 @ (sK12 @ sF8 @ sF9))) = $true) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $true)),
% 283.22/40.34 inference(forward_subsumption_resolution,[],[f569,f54])).
% 283.22/40.34 thf(f586,plain,(
% 283.22/40.34 (((in @ (sK12 @ sF8 @ sF9) @ sK0)) = $true) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $true)),
% 283.22/40.34 inference(forward_subsumption_resolution,[],[f572,f54])).
% 283.22/40.34 thf(f595,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((sK3 @ (sK13 @ X0 @ sF9))) = $true) | ($false = ((sK2 @ (sK13 @ X0 @ sF9)))) | ($false = $true) | (((in @ (sK12 @ X0 @ sF9) @ sF9)) = $false) | (sF9 = X0)) )),
% 283.22/40.34 inference(constrained_superposition,[],[f162,f300])).
% 283.22/40.34 thf(f606,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((in @ (sK12 @ X0 @ sF9) @ sF9)) = $false) | (((sK3 @ (sK13 @ X0 @ sF9))) = $true) | (sF9 = X0) | ($false = ((sK2 @ (sK13 @ X0 @ sF9))))) )),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f595])).
% 283.22/40.34 thf(f864,plain,(
% 283.22/40.34 (((sK3 @ (sK13 @ sF8 @ sF9))) = $false) | (sF8 = sF9) | (((in @ (sK12 @ sF8 @ sF9) @ sF9)) = $false) | (((in @ (sK12 @ sF8 @ sF9) @ sF9)) = $false) | ($false = $true) | (sF8 = sF9)),
% 283.22/40.34 inference(constrained_superposition,[],[f300,f468])).
% 283.22/40.34 thf(f873,plain,(
% 283.22/40.34 (sF8 = sF9) | ($false = $true) | (((sK3 @ (sK13 @ sF8 @ sF9))) = $false) | (((in @ (sK12 @ sF8 @ sF9) @ sF9)) = $false)),
% 283.22/40.34 inference(duplicate_literal_removal,[],[f864])).
% 283.22/40.34 thf(f874,plain,(
% 283.22/40.34 (((in @ (sK12 @ sF8 @ sF9) @ sF9)) = $false) | (((sK3 @ (sK13 @ sF8 @ sF9))) = $false) | (sF8 = sF9)),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f873])).
% 283.22/40.34 thf(f892,plain,(
% 283.22/40.34 (((in @ (sK12 @ sF8 @ sF9) @ sF9)) = $false) | (((sK3 @ (sK13 @ sF8 @ sF9))) = $false)),
% 283.22/40.34 inference(forward_subsumption_resolution,[],[f874,f54])).
% 283.22/40.34 thf(f958,plain,(
% 283.22/40.34 (((sK2 @ (sK12 @ sF8 @ sF9))) = $true) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $true) | (((sK3 @ (sK12 @ sF8 @ sF9))) = $false) | ($false = $true)),
% 283.22/40.34 inference(constrained_superposition,[],[f586,f156])).
% 283.22/40.34 thf(f964,plain,(
% 283.22/40.34 (((sK3 @ (sK12 @ sF8 @ sF9))) = $false) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $true) | (((sK2 @ (sK12 @ sF8 @ sF9))) = $true)),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f958])).
% 283.22/40.34 thf(f1005,plain,(
% 283.22/40.34 (((sK2 @ (sK12 @ sF8 @ sF9))) = $false) | ($false = $true) | (((in @ (sK12 @ sF8 @ sF9) @ sK0)) = $false) | (((sK3 @ (sK13 @ sF8 @ sF9))) = $false)),
% 283.22/40.34 inference(constrained_superposition,[],[f892,f183])).
% 283.22/40.34 thf(f1007,plain,(
% 283.22/40.34 (((in @ (sK12 @ sF8 @ sF9) @ sK0)) = $false) | (((sK2 @ (sK12 @ sF8 @ sF9))) = $false) | (((sK3 @ (sK13 @ sF8 @ sF9))) = $false)),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f1005])).
% 283.22/40.34 thf(f1013,plain,(
% 283.22/40.34 (sF8 = sF9) | (((sK3 @ (sK13 @ sF8 @ sF9))) = $false) | (sF8 = sF9) | ($true = ((in @ (sK12 @ sF8 @ sF9) @ sF8))) | ($false = $true) | ($true = ((in @ (sK12 @ sF8 @ sF9) @ sF8)))),
% 283.22/40.34 inference(constrained_superposition,[],[f544,f392])).
% 283.22/40.34 thf(f1021,plain,(
% 283.22/40.34 (((sK3 @ (sK13 @ sF8 @ sF9))) = $false) | ($false = $true) | (sF8 = sF9) | ($true = ((in @ (sK12 @ sF8 @ sF9) @ sF8)))),
% 283.22/40.34 inference(duplicate_literal_removal,[],[f1013])).
% 283.22/40.34 thf(f1022,plain,(
% 283.22/40.34 (sF8 = sF9) | (((sK3 @ (sK13 @ sF8 @ sF9))) = $false) | ($true = ((in @ (sK12 @ sF8 @ sF9) @ sF8)))),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f1021])).
% 283.22/40.34 thf(f1039,plain,(
% 283.22/40.34 ($true = ((in @ (sK12 @ sF8 @ sF9) @ sF8))) | (((sK3 @ (sK13 @ sF8 @ sF9))) = $false)),
% 283.22/40.34 inference(forward_subsumption_resolution,[],[f1022,f54])).
% 283.22/40.34 thf(f1348,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((in @ (sK13 @ sF8 @ X0) @ X0)) = $true) | (((sK3 @ (sK12 @ sF8 @ X0))) = $true) | (sF8 = X0)) )),
% 283.22/40.34 inference(constrained_superposition,[],[f404,f110])).
% 283.22/40.34 thf(f1645,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((in @ (sK13 @ sF8 @ X0) @ X0)) = $true) | (sF8 = X0) | (((in @ (sK12 @ sF8 @ X0) @ sK0)) = $true)) )),
% 283.22/40.34 inference(constrained_superposition,[],[f424,f110])).
% 283.22/40.34 thf(f1694,plain,(
% 283.22/40.34 ($false = $true) | (((sK3 @ (sK12 @ sF8 @ sF9))) = $true) | (((sK3 @ (sK13 @ sF8 @ sF9))) = $false)),
% 283.22/40.34 inference(constrained_superposition,[],[f1039,f174])).
% 283.22/40.34 thf(f1695,plain,(
% 283.22/40.34 (((sK3 @ (sK13 @ sF8 @ sF9))) = $false) | (((in @ (sK12 @ sF8 @ sF9) @ sK0)) = $true) | ($false = $true)),
% 283.22/40.34 inference(constrained_superposition,[],[f206,f1039])).
% 283.22/40.34 thf(f1697,plain,(
% 283.22/40.34 (((in @ (sK12 @ sF8 @ sF9) @ sK0)) = $true) | (((sK3 @ (sK13 @ sF8 @ sF9))) = $false)),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f1695])).
% 283.22/40.34 thf(f1698,plain,(
% 283.22/40.34 (((sK3 @ (sK13 @ sF8 @ sF9))) = $false) | (((sK3 @ (sK12 @ sF8 @ sF9))) = $true)),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f1694])).
% 283.22/40.34 thf(f1850,plain,(
% 283.22/40.34 (((sK3 @ (sK13 @ sF8 @ sF9))) = $false) | (((sK2 @ (sK12 @ sF8 @ sF9))) = $true) | ($false = $true) | (((sK3 @ (sK12 @ sF8 @ sF9))) = $false)),
% 283.22/40.34 inference(constrained_superposition,[],[f1697,f156])).
% 283.22/40.34 thf(f1855,plain,(
% 283.22/40.34 (((sK3 @ (sK13 @ sF8 @ sF9))) = $false) | (((sK2 @ (sK12 @ sF8 @ sF9))) = $true) | (((sK3 @ (sK12 @ sF8 @ sF9))) = $false)),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f1850])).
% 283.22/40.34 thf(f2814,plain,(
% 283.22/40.34 ($false = $true) | (((in @ (sK13 @ sF8 @ sF9) @ sK0)) = $true) | (sF8 = sF9) | (((sK3 @ (sK12 @ sF8 @ sF9))) = $true)),
% 283.22/40.34 inference(constrained_superposition,[],[f204,f1348])).
% 283.22/40.34 thf(f2824,plain,(
% 283.22/40.34 (sF8 = sF9) | (((in @ (sK13 @ sF8 @ sF9) @ sK0)) = $true) | (((sK3 @ (sK12 @ sF8 @ sF9))) = $true)),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f2814])).
% 283.22/40.34 thf(f2851,plain,(
% 283.22/40.34 (((in @ (sK13 @ sF8 @ sF9) @ sK0)) = $true) | (((sK3 @ (sK12 @ sF8 @ sF9))) = $true)),
% 283.22/40.34 inference(forward_subsumption_resolution,[],[f2824,f54])).
% 283.22/40.34 thf(f2941,plain,(
% 283.22/40.34 (((sK3 @ (sK12 @ sF8 @ sF9))) = $true) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $false) | ($false = $true) | (((sK3 @ (sK13 @ sF8 @ sF9))) = $true)),
% 283.22/40.34 inference(constrained_superposition,[],[f162,f2851])).
% 283.22/40.34 thf(f2950,plain,(
% 283.22/40.34 (((sK3 @ (sK13 @ sF8 @ sF9))) = $true) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $false) | (((sK3 @ (sK12 @ sF8 @ sF9))) = $true)),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f2941])).
% 283.22/40.34 thf(f3065,plain,(
% 283.22/40.34 ($false = $true) | (((in @ (sK13 @ sF8 @ sF9) @ sK0)) = $true) | (sF8 = sF9) | (((in @ (sK12 @ sF8 @ sF9) @ sK0)) = $true)),
% 283.22/40.34 inference(constrained_superposition,[],[f1645,f204])).
% 283.22/40.34 thf(f3083,plain,(
% 283.22/40.34 (((in @ (sK13 @ sF8 @ sF9) @ sK0)) = $true) | (sF8 = sF9) | (((in @ (sK12 @ sF8 @ sF9) @ sK0)) = $true)),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f3065])).
% 283.22/40.34 thf(f3115,plain,(
% 283.22/40.34 (((in @ (sK13 @ sF8 @ sF9) @ sK0)) = $true) | (((in @ (sK12 @ sF8 @ sF9) @ sK0)) = $true)),
% 283.22/40.34 inference(forward_subsumption_resolution,[],[f3083,f54])).
% 283.22/40.34 thf(f3620,plain,(
% 283.22/40.34 (((sK2 @ (sK12 @ sF8 @ sF9))) = $false) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $true) | ($false = $true) | (sF8 = sF9) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $true)),
% 283.22/40.34 inference(constrained_superposition,[],[f434,f586])).
% 283.22/40.34 thf(f3629,plain,(
% 283.22/40.34 ($false = $true) | (((sK2 @ (sK12 @ sF8 @ sF9))) = $false) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $true) | (sF8 = sF9)),
% 283.22/40.34 inference(duplicate_literal_removal,[],[f3620])).
% 283.22/40.34 thf(f3630,plain,(
% 283.22/40.34 (sF8 = sF9) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $true) | (((sK2 @ (sK12 @ sF8 @ sF9))) = $false)),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f3629])).
% 283.22/40.34 thf(f3653,plain,(
% 283.22/40.34 (((sK2 @ (sK13 @ sF8 @ sF9))) = $true) | (((sK2 @ (sK12 @ sF8 @ sF9))) = $false)),
% 283.22/40.34 inference(forward_subsumption_resolution,[],[f3630,f54])).
% 283.22/40.34 thf(f3675,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((sF9 = X0) | ($false = ((sK2 @ (sK13 @ X0 @ sF9)))) | (((sK3 @ (sK13 @ X0 @ sF9))) = $true) | ($false = $true) | ($false = ((sK2 @ (sK12 @ X0 @ sF9)))) | (((in @ (sK12 @ X0 @ sF9) @ sK0)) = $false)) )),
% 283.22/40.34 inference(constrained_superposition,[],[f183,f606])).
% 283.22/40.34 thf(f3679,plain,(
% 283.22/40.34 ( ! [X0 : $i] : ((((in @ (sK12 @ X0 @ sF9) @ sK0)) = $false) | (sF9 = X0) | ($false = ((sK2 @ (sK12 @ X0 @ sF9)))) | (((sK3 @ (sK13 @ X0 @ sF9))) = $true) | ($false = ((sK2 @ (sK13 @ X0 @ sF9))))) )),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f3675])).
% 283.22/40.34 thf(f3819,plain,(
% 283.22/40.34 (((sK3 @ (sK13 @ sF8 @ sF9))) = $true) | ($false = $true) | (((in @ (sK12 @ sF8 @ sF9) @ sK0)) = $true) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $false)),
% 283.22/40.34 inference(constrained_superposition,[],[f3115,f162])).
% 283.22/40.34 thf(f3831,plain,(
% 283.22/40.34 (((in @ (sK12 @ sF8 @ sF9) @ sK0)) = $true) | (((sK3 @ (sK13 @ sF8 @ sF9))) = $true) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $false)),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f3819])).
% 283.22/40.34 thf(f4318,plain,(
% 283.22/40.34 (((sK2 @ (sK13 @ sF8 @ sF9))) = $true) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $true) | (((sK2 @ (sK12 @ sF8 @ sF9))) = $true) | ($false = $true)),
% 283.22/40.34 inference(constrained_superposition,[],[f964,f585])).
% 283.22/40.34 thf(f4324,plain,(
% 283.22/40.34 (((sK2 @ (sK12 @ sF8 @ sF9))) = $true) | ($false = $true) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $true)),
% 283.22/40.34 inference(duplicate_literal_removal,[],[f4318])).
% 283.22/40.34 thf(f4325,plain,(
% 283.22/40.34 (((sK2 @ (sK13 @ sF8 @ sF9))) = $true) | (((sK2 @ (sK12 @ sF8 @ sF9))) = $true)),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f4324])).
% 283.22/40.34 thf(f4956,plain,(
% 283.22/40.34 ($false = $true) | (((sK3 @ (sK12 @ sF8 @ sF9))) = $true) | (((sK3 @ (sK12 @ sF8 @ sF9))) = $true) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $false)),
% 283.22/40.34 inference(constrained_superposition,[],[f1698,f2950])).
% 283.22/40.34 thf(f4962,plain,(
% 283.22/40.34 (((sK2 @ (sK13 @ sF8 @ sF9))) = $false) | ($false = $true) | (((sK3 @ (sK12 @ sF8 @ sF9))) = $true)),
% 283.22/40.34 inference(duplicate_literal_removal,[],[f4956])).
% 283.22/40.34 thf(f4963,plain,(
% 283.22/40.34 (((sK3 @ (sK12 @ sF8 @ sF9))) = $true) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $false)),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f4962])).
% 283.22/40.34 thf(f11753,plain,(
% 283.22/40.34 (((sK3 @ (sK13 @ sF8 @ sF9))) = $false) | (((sK2 @ (sK12 @ sF8 @ sF9))) = $false) | (((sK3 @ (sK13 @ sF8 @ sF9))) = $false) | ($false = $true)),
% 283.22/40.34 inference(constrained_superposition,[],[f1007,f1697])).
% 283.22/40.34 thf(f11781,plain,(
% 283.22/40.34 (((sK3 @ (sK13 @ sF8 @ sF9))) = $false) | (((sK2 @ (sK12 @ sF8 @ sF9))) = $false) | ($false = $true)),
% 283.22/40.34 inference(duplicate_literal_removal,[],[f11753])).
% 283.22/40.34 thf(f11782,plain,(
% 283.22/40.34 (((sK3 @ (sK13 @ sF8 @ sF9))) = $false) | (((sK2 @ (sK12 @ sF8 @ sF9))) = $false)),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f11781])).
% 283.22/40.34 thf(f15867,plain,(
% 283.22/40.34 (((sK2 @ (sK12 @ sF8 @ sF9))) = $true) | ($false = $true) | (((sK3 @ (sK13 @ sF8 @ sF9))) = $true) | (((sK3 @ (sK12 @ sF8 @ sF9))) = $false) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $false)),
% 283.22/40.34 inference(constrained_superposition,[],[f156,f3831])).
% 283.22/40.34 thf(f15872,plain,(
% 283.22/40.34 (((sK3 @ (sK13 @ sF8 @ sF9))) = $true) | (((sK3 @ (sK12 @ sF8 @ sF9))) = $false) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $false) | (((sK2 @ (sK12 @ sF8 @ sF9))) = $true)),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f15867])).
% 283.22/40.34 thf(f24087,plain,(
% 283.22/40.34 ($false = $true) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $false) | (((sK2 @ (sK12 @ sF8 @ sF9))) = $true) | (((sK3 @ (sK12 @ sF8 @ sF9))) = $false) | (((sK2 @ (sK12 @ sF8 @ sF9))) = $true) | (((sK3 @ (sK12 @ sF8 @ sF9))) = $false)),
% 283.22/40.34 inference(constrained_superposition,[],[f1855,f15872])).
% 283.22/40.34 thf(f24102,plain,(
% 283.22/40.34 (((sK2 @ (sK12 @ sF8 @ sF9))) = $true) | ($false = $true) | (((sK3 @ (sK12 @ sF8 @ sF9))) = $false) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $false)),
% 283.22/40.34 inference(duplicate_literal_removal,[],[f24087])).
% 283.22/40.34 thf(f24103,plain,(
% 283.22/40.34 (((sK3 @ (sK12 @ sF8 @ sF9))) = $false) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $false) | (((sK2 @ (sK12 @ sF8 @ sF9))) = $true)),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f24102])).
% 283.22/40.34 thf(f25418,plain,(
% 283.22/40.34 (((sK2 @ (sK12 @ sF8 @ sF9))) = $true) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $false) | ($false = $true) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $false)),
% 283.22/40.34 inference(constrained_superposition,[],[f24103,f4963])).
% 283.22/40.34 thf(f25451,plain,(
% 283.22/40.34 (((sK2 @ (sK12 @ sF8 @ sF9))) = $true) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $false) | ($false = $true)),
% 283.22/40.34 inference(duplicate_literal_removal,[],[f25418])).
% 283.22/40.34 thf(f25452,plain,(
% 283.22/40.34 (((sK2 @ (sK13 @ sF8 @ sF9))) = $false) | (((sK2 @ (sK12 @ sF8 @ sF9))) = $true)),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f25451])).
% 283.22/40.34 thf(f26827,plain,(
% 283.22/40.34 (((sK2 @ (sK12 @ sF8 @ sF9))) = $true) | ($false = $true) | (((sK2 @ (sK12 @ sF8 @ sF9))) = $true)),
% 283.22/40.34 inference(constrained_superposition,[],[f25452,f4325])).
% 283.22/40.34 thf(f26883,plain,(
% 283.22/40.34 (((sK2 @ (sK12 @ sF8 @ sF9))) = $true) | ($false = $true)),
% 283.22/40.34 inference(duplicate_literal_removal,[],[f26827])).
% 283.22/40.34 thf(f26884,plain,(
% 283.22/40.34 (((sK2 @ (sK12 @ sF8 @ sF9))) = $true)),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f26883])).
% 283.22/40.34 thf(f36202,plain,(
% 283.22/40.34 ($false = $true) | (((sK2 @ (sK12 @ sF8 @ sF9))) = $false) | (sF8 = sF9) | (((sK3 @ (sK13 @ sF8 @ sF9))) = $true) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $false) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $false) | (((sK3 @ (sK13 @ sF8 @ sF9))) = $true)),
% 283.22/40.34 inference(constrained_superposition,[],[f3831,f3679])).
% 283.22/40.34 thf(f36224,plain,(
% 283.22/40.34 (((sK3 @ (sK13 @ sF8 @ sF9))) = $true) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $false) | (sF8 = sF9) | (((sK2 @ (sK12 @ sF8 @ sF9))) = $false) | ($false = $true)),
% 283.22/40.34 inference(duplicate_literal_removal,[],[f36202])).
% 283.22/40.34 thf(f36225,plain,(
% 283.22/40.34 (sF8 = sF9) | (((sK3 @ (sK13 @ sF8 @ sF9))) = $true) | (((sK2 @ (sK12 @ sF8 @ sF9))) = $false) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $false)),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f36224])).
% 283.22/40.34 thf(f36321,plain,(
% 283.22/40.34 (((sK2 @ (sK13 @ sF8 @ sF9))) = $false) | (((sK2 @ (sK12 @ sF8 @ sF9))) = $false) | (((sK3 @ (sK13 @ sF8 @ sF9))) = $true)),
% 283.22/40.34 inference(forward_subsumption_resolution,[],[f36225,f54])).
% 283.22/40.34 thf(f36323,plain,(
% 283.22/40.34 (((sK2 @ (sK13 @ sF8 @ sF9))) = $false) | (((sK3 @ (sK13 @ sF8 @ sF9))) = $true) | ($false = $true)),
% 283.22/40.34 inference(forward_demodulation,[],[f36321,f26884])).
% 283.22/40.34 thf(f36324,plain,(
% 283.22/40.34 (((sK3 @ (sK13 @ sF8 @ sF9))) = $true) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $false)),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f36323])).
% 283.22/40.34 thf(f36720,plain,(
% 283.22/40.34 ($false = $true) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $false) | (((sK2 @ (sK12 @ sF8 @ sF9))) = $false)),
% 283.22/40.34 inference(constrained_superposition,[],[f36324,f11782])).
% 283.22/40.34 thf(f36767,plain,(
% 283.22/40.34 (((sK2 @ (sK13 @ sF8 @ sF9))) = $false) | (((sK2 @ (sK12 @ sF8 @ sF9))) = $false)),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f36720])).
% 283.22/40.34 thf(f36787,plain,(
% 283.22/40.34 ($false = $true) | (((sK2 @ (sK13 @ sF8 @ sF9))) = $false)),
% 283.22/40.34 inference(forward_demodulation,[],[f36767,f26884])).
% 283.22/40.34 thf(f36788,plain,(
% 283.22/40.34 (((sK2 @ (sK13 @ sF8 @ sF9))) = $false)),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f36787])).
% 283.22/40.34 thf(f38483,plain,(
% 283.22/40.34 (((sK2 @ (sK12 @ sF8 @ sF9))) = $false) | ($false = $true)),
% 283.22/40.34 inference(constrained_superposition,[],[f36788,f3653])).
% 283.22/40.34 thf(f38551,plain,(
% 283.22/40.34 (((sK2 @ (sK12 @ sF8 @ sF9))) = $false)),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f38483])).
% 283.22/40.34 thf(f40280,plain,(
% 283.22/40.34 ($false = $true)),
% 283.22/40.34 inference(constrained_superposition,[],[f38551,f26884])).
% 283.22/40.34 thf(f40368,plain,(
% 283.22/40.34 $false),
% 283.22/40.34 inference(trivial_inequality_removal,[],[f40280])).
% 283.22/40.34 % SZS output end Proof for theBenchmark
% 283.22/40.34 % (388514)------------------------------
% 283.22/40.34 % (388514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 283.22/40.34 % (388514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 283.22/40.34 % (388514)CaDiCaL version: 2.1.3
% 283.22/40.34 % (388514)Termination reason: Refutation
% 283.22/40.34 % (388514)Time elapsed: 4.305 s
% 283.22/40.34 % (388514)Peak memory usage: 38 MB
% 283.22/40.34 % (388514)Instructions burned: 9119 (million)
% 283.22/40.34 % (388350)Success in time 40.089 s
% 283.22/40.34 % Vampire exiting
%------------------------------------------------------------------------------