%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU705^2 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n015.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:33:03 AM UTC 2026
% Result : Theorem 34.68s 5.27s
% Output : Refutation 34.68s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU705^2 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.28 % Computer : n015.cluster.edu
% 0.11/0.28 % Model : x86_64 x86_64
% 0.11/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.28 % Memory : 8046.5625MB
% 0.11/0.28 % OS : Linux 6.8.0-71-generic
% 0.11/0.28 % CPULimit : 300
% 0.11/0.28 % WCLimit : 300
% 0.11/0.28 % DateTime : Tue Sep 29 14:16:03 UTC 2026
% 0.11/0.28 % CPUTime :
% 0.11/0.28 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.29/0.33 Running first-order model finding
% 0.29/0.33 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.30/1.61 % (3590111)Will run a generic schedule for satisfiability detection.
% 7.30/1.61 % (3590117)% WARNING: option uhcvi not known.
% 7.30/1.61 % (3590117)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3737646508:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.30/1.61 % (3590117)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.30/1.61 % (3590117)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 7.30/1.61 % (3590118)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=968725796:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.30/1.61 % (3590116)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=911629154_2999 on theBenchmark for (2999ds/0Mi)
% 7.30/1.61 % Exception at run slice level
% 7.30/1.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.30/1.61 % (3590120)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2678535682:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.30/1.61 % (3590119)dis+10_1_sil=32000:sp=arity:random_seed=3895537363:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.30/1.61 % (3590120)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.30/1.61 % (3590122)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1471045783:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.30/1.61 % (3590121)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3897439820:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.30/1.61 % (3590126)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=269163915:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 7.30/1.61 % Exception at run slice level
% 7.30/1.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.30/1.61 % (3590132)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=748347242:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 7.30/1.61 % (3590119)Instruction limit reached!
% 7.30/1.61 % (3590119)------------------------------
% 7.30/1.61 % (3590119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.30/1.61 % (3590119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.30/1.61 % (3590119)CaDiCaL version: 2.1.3
% 7.30/1.61 % (3590119)Termination reason: Instruction limit
% 7.30/1.61 % (3590119)Termination phase: Saturation
% 7.30/1.61 % (3590119)Time elapsed: 0.086 s
% 7.30/1.61 % (3590119)Peak memory usage: 12 MB
% 7.30/1.61 % (3590119)Instructions burned: 104 (million)
% 7.30/1.61 % (3590120)Instruction limit reached!
% 7.30/1.61 % (3590120)------------------------------
% 7.30/1.61 % (3590120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.30/1.61 % (3590120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.30/1.61 % (3590120)CaDiCaL version: 2.1.3
% 7.30/1.61 % (3590120)Termination reason: Instruction limit
% 7.30/1.61 % (3590120)Termination phase: Saturation
% 7.30/1.61 % (3590120)Time elapsed: 0.096 s
% 7.30/1.61 % (3590120)Peak memory usage: 12 MB
% 7.30/1.61 % (3590120)Instructions burned: 117 (million)
% 7.30/1.61 % (3590134)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=3361311580:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 7.30/1.61 % (3590134)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.30/1.61 % (3590134)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 7.30/1.61 % (3590135)ott-21_1_sil=16000:fs=off:random_seed=3864870742:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 7.30/1.61 % (3590122)Instruction limit reached!
% 7.30/1.61 % (3590122)------------------------------
% 7.30/1.61 % (3590122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.30/1.61 % (3590122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.30/1.61 % (3590122)CaDiCaL version: 2.1.3
% 7.30/1.61 % (3590122)Termination reason: Instruction limit
% 7.30/1.61 % (3590122)Termination phase: Saturation
% 7.30/1.61 % (3590122)Time elapsed: 0.127 s
% 7.30/1.61 % (3590122)Peak memory usage: 12 MB
% 7.30/1.61 % (3590122)Instructions burned: 160 (million)
% 7.30/1.61 % (3590121)Instruction limit reached!
% 30.36/4.88 % (3590121)------------------------------
% 30.36/4.88 % (3590121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.36/4.88 % (3590121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.36/4.88 % (3590121)CaDiCaL version: 2.1.3
% 30.36/4.88 % (3590121)Termination reason: Instruction limit
% 30.36/4.88 % (3590121)Termination phase: Saturation
% 30.36/4.88 % (3590121)Time elapsed: 0.129 s
% 30.36/4.88 % (3590121)Peak memory usage: 12 MB
% 30.36/4.88 % (3590121)Instructions burned: 132 (million)
% 30.36/4.88 % (3590132)Instruction limit reached!
% 30.36/4.88 % (3590132)------------------------------
% 30.36/4.88 % (3590132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.36/4.88 % (3590132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.36/4.88 % (3590132)CaDiCaL version: 2.1.3
% 30.36/4.88 % (3590132)Termination reason: Instruction limit
% 30.36/4.88 % (3590132)Termination phase: Saturation
% 30.36/4.88 % (3590132)Time elapsed: 0.114 s
% 30.36/4.88 % (3590132)Peak memory usage: 12 MB
% 30.36/4.88 % (3590132)Instructions burned: 131 (million)
% 30.36/4.88 % (3590139)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3532311634:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 30.36/4.88 % Exception at run slice level
% 30.36/4.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 30.36/4.88 % (3590138)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1871065116:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 30.36/4.88 % (3590140)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2617378690:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 30.36/4.88 % (3590142)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3678740186:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 30.36/4.88 % Exception at run slice level
% 30.36/4.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 30.36/4.88 % (3590146)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=3103481331:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi)
% 30.36/4.88 % (3590146)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 30.36/4.88 % (3590135)Instruction limit reached!
% 30.36/4.88 % (3590135)------------------------------
% 30.36/4.88 % (3590135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.36/4.88 % (3590135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.36/4.88 % (3590135)CaDiCaL version: 2.1.3
% 30.36/4.88 % (3590135)Termination reason: Instruction limit
% 30.36/4.88 % (3590135)Termination phase: Saturation
% 30.36/4.88 % (3590135)Time elapsed: 0.149 s
% 30.36/4.88 % (3590135)Peak memory usage: 12 MB
% 30.36/4.88 % (3590135)Instructions burned: 181 (million)
% 30.36/4.88 % (3590148)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4233443122:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 30.36/4.88 % (3590148)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 30.36/4.88 % (3590138)Instruction limit reached!
% 30.36/4.88 % (3590138)------------------------------
% 30.36/4.88 % (3590138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.36/4.88 % (3590138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.36/4.88 % (3590138)CaDiCaL version: 2.1.3
% 30.36/4.88 % (3590138)Termination reason: Instruction limit
% 30.36/4.88 % (3590138)Termination phase: Saturation
% 30.36/4.88 % (3590138)Time elapsed: 0.404 s
% 30.36/4.88 % (3590138)Peak memory usage: 13 MB
% 30.36/4.88 % (3590138)Instructions burned: 477 (million)
% 30.36/4.88 % (3590154)fmb+10_1_sil=64000:random_seed=293927263:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 30.36/4.88 % (3590154)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 30.36/4.88 % Exception at run slice level
% 30.36/4.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 30.36/4.88 % (3590134)Instruction limit reached!
% 30.36/4.88 % (3590134)------------------------------
% 30.36/4.88 % (3590134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.36/4.88 % (3590134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.68/5.27 % (3590134)CaDiCaL version: 2.1.3
% 34.68/5.27 % (3590134)Termination reason: Instruction limit
% 34.68/5.27 % (3590134)Termination phase: Saturation
% 34.68/5.27 % (3590134)Time elapsed: 0.543 s
% 34.68/5.27 % (3590134)Peak memory usage: 13 MB
% 34.68/5.27 % (3590134)Instructions burned: 684 (million)
% 34.68/5.27 % (3590157)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=206320197:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi)
% 34.68/5.27 % (3590156)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1479664539:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi)
% 34.68/5.27 % Exception at run slice level
% 34.68/5.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 34.68/5.27 % Exception at run slice level
% 34.68/5.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 34.68/5.27 % (3590160)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1406666108:i=5131_2992 on theBenchmark for (2992ds/5131Mi)
% 34.68/5.27 % (3590160)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 34.68/5.27 % (3590161)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=887033489:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi)
% 34.68/5.27 % (3590161)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 34.68/5.27 % (3590161)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 34.68/5.27 % (3590146)Instruction limit reached!
% 34.68/5.27 % (3590146)------------------------------
% 34.68/5.27 % (3590146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.68/5.27 % (3590146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.68/5.27 % (3590146)CaDiCaL version: 2.1.3
% 34.68/5.27 % (3590146)Termination reason: Instruction limit
% 34.68/5.27 % (3590146)Termination phase: Saturation
% 34.68/5.27 % (3590146)Time elapsed: 0.501 s
% 34.68/5.27 % (3590146)Peak memory usage: 13 MB
% 34.68/5.27 % (3590146)Instructions burned: 693 (million)
% 34.68/5.27 % (3590164)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=951793686:i=6324_2991 on theBenchmark for (2991ds/6324Mi)
% 34.68/5.27 % Exception at run slice level
% 34.68/5.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 34.68/5.27 % (3590166)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=98894243:fmbsr=2.30978:i=2174_2991 on theBenchmark for (2991ds/2174Mi)
% 34.68/5.27 % Exception at run slice level
% 34.68/5.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 34.68/5.27 % (3590168)ott-2_1_sil=16000:newcnf=on:random_seed=4289697482:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi)
% 34.68/5.27 % (3590168)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 34.68/5.27 % (3590148)Instruction limit reached!
% 34.68/5.27 % (3590148)------------------------------
% 34.68/5.27 % (3590148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.68/5.27 % (3590148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.68/5.27 % (3590148)CaDiCaL version: 2.1.3
% 34.68/5.27 % (3590148)Termination reason: Instruction limit
% 34.68/5.27 % (3590148)Termination phase: Saturation
% 34.68/5.27 % (3590148)Time elapsed: 0.721 s
% 34.68/5.27 % (3590148)Peak memory usage: 13 MB
% 34.68/5.27 % (3590148)Instructions burned: 879 (million)
% 34.68/5.27 % (3590170)ott+10_1_sil=32000:tgt=ground:random_seed=1305249796:i=5114:av=off_2988 on theBenchmark for (2988ds/5114Mi)
% 34.68/5.27 % (3590140)Instruction limit reached!
% 34.68/5.27 % (3590140)------------------------------
% 34.68/5.27 % (3590140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.68/5.27 % (3590140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.68/5.27 % (3590140)CaDiCaL version: 2.1.3
% 34.68/5.27 % (3590140)Termination reason: Instruction limit
% 34.68/5.27 % (3590140)Termination phase: Saturation
% 34.68/5.27 % (3590140)Time elapsed: 0.933 s
% 34.68/5.27 % (3590140)Peak memory usage: 14 MB
% 34.68/5.27 % (3590140)Instructions burned: 1179 (million)
% 34.68/5.27 % (3590172)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3576316981:i=54282_2987 on theBenchmark for (2987ds/54282Mi)
% 34.68/5.27 % Exception at run slice level
% 34.68/5.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 34.68/5.27 % (3590174)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2922296047:i=3512:aac=none_2987 on theBenchmark for (2987ds/3512Mi)
% 34.68/5.27 % (3590174)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 34.68/5.27 % (3590168)Instruction limit reached!
% 34.68/5.27 % (3590168)------------------------------
% 34.68/5.27 % (3590168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.68/5.27 % (3590168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.68/5.27 % (3590168)CaDiCaL version: 2.1.3
% 34.68/5.27 % (3590168)Termination reason: Instruction limit
% 34.68/5.27 % (3590168)Termination phase: Saturation
% 34.68/5.27 % (3590168)Time elapsed: 0.675 s
% 34.68/5.27 % (3590168)Peak memory usage: 14 MB
% 34.68/5.27 % (3590168)Instructions burned: 870 (million)
% 34.68/5.27 % (3590176)dis+21_1_sil=32000:sas=cadical:random_seed=237033203:i=3773:amm=off_2983 on theBenchmark for (2983ds/3773Mi)
% 34.68/5.27 % (3590161)Instruction limit reached!
% 34.68/5.27 % (3590161)------------------------------
% 34.68/5.27 % (3590161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.68/5.27 % (3590161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.68/5.27 % (3590161)CaDiCaL version: 2.1.3
% 34.68/5.27 % (3590161)Termination reason: Instruction limit
% 34.68/5.27 % (3590161)Termination phase: Saturation
% 34.68/5.27 % (3590161)Time elapsed: 1.237 s
% 34.68/5.27 % (3590161)Peak memory usage: 14 MB
% 34.68/5.27 % (3590161)Instructions burned: 1473 (million)
% 34.68/5.27 % (3590178)ott+11_1_sil=16000:gs=on:random_seed=3972723098:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2979 on theBenchmark for (2979ds/2251Mi)
% 34.68/5.27 % (3590178)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 34.68/5.27 % (3590178)Instruction limit reached!
% 34.68/5.27 % (3590178)------------------------------
% 34.68/5.27 % (3590178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.68/5.27 % (3590178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.68/5.27 % (3590178)CaDiCaL version: 2.1.3
% 34.68/5.27 % (3590178)Termination reason: Instruction limit
% 34.68/5.27 % (3590178)Termination phase: Saturation
% 34.68/5.27 % (3590178)Time elapsed: 1.702 s
% 34.68/5.27 % (3590178)Peak memory usage: 13 MB
% 34.68/5.27 % (3590178)Instructions burned: 2251 (million)
% 34.68/5.27 % (3590180)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1138991035:fmbsr=1.6:i=67534_2961 on theBenchmark for (2961ds/67534Mi)
% 34.68/5.27 % Exception at run slice level
% 34.68/5.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 34.68/5.27 % (3590182)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=831021802:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2961 on theBenchmark for (2961ds/4591Mi)
% 34.68/5.27 % (3590174)Instruction limit reached!
% 34.68/5.27 % (3590174)------------------------------
% 34.68/5.27 % (3590174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.68/5.27 % (3590174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.68/5.27 % (3590174)CaDiCaL version: 2.1.3
% 34.68/5.27 % (3590174)Termination reason: Instruction limit
% 34.68/5.27 % (3590174)Termination phase: Saturation
% 34.68/5.27 % (3590174)Time elapsed: 2.682 s
% 34.68/5.27 % (3590174)Peak memory usage: 15 MB
% 34.68/5.27 % (3590174)Instructions burned: 3513 (million)
% 34.68/5.27 % (3590184)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2720422795:i=29340_2960 on theBenchmark for (2960ds/29340Mi)
% 34.68/5.27 % (3590176)Instruction limit reached!
% 34.68/5.27 % (3590176)------------------------------
% 34.68/5.27 % (3590176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.68/5.27 % (3590176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.68/5.27 % (3590176)CaDiCaL version: 2.1.3
% 34.68/5.27 % (3590176)Termination reason: Instruction limit
% 34.68/5.27 % (3590176)Termination phase: Saturation
% 34.68/5.27 % (3590176)Time elapsed: 2.828 s
% 34.68/5.27 % (3590176)Peak memory usage: 16 MB
% 34.68/5.27 % (3590176)Instructions burned: 3774 (million)
% 34.68/5.27 % (3590186)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1835143790:i=5211_2954 on theBenchmark for (2954ds/5211Mi)
% 34.68/5.27 % (3590160)Instruction limit reached!
% 34.68/5.27 % (3590160)------------------------------
% 34.68/5.27 % (3590160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.68/5.27 % (3590160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.68/5.27 % (3590160)CaDiCaL version: 2.1.3
% 34.68/5.27 % (3590160)Termination reason: Instruction limit
% 34.68/5.27 % (3590160)Termination phase: Saturation
% 34.68/5.27 % (3590160)Time elapsed: 3.798 s
% 34.68/5.27 % (3590160)Peak memory usage: 17 MB
% 34.68/5.27 % (3590160)Instructions burned: 5131 (million)
% 34.68/5.27 % (3590188)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2004949899:i=5497:nm=2_2953 on theBenchmark for (2953ds/5497Mi)
% 34.68/5.27 % Exception at run slice level
% 34.68/5.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 34.68/5.27 % (3590190)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2720795493:fmbsr=2:i=46332_2953 on theBenchmark for (2953ds/46332Mi)
% 34.68/5.27 % Exception at run slice level
% 34.68/5.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 34.68/5.27 % (3590192)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=938437445:i=14071_2953 on theBenchmark for (2953ds/14071Mi)
% 34.68/5.27 % Exception at run slice level
% 34.68/5.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 34.68/5.27 % (3590194)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=829187082:i=22565:add=on:rawr=on_2952 on theBenchmark for (2952ds/22565Mi)
% 34.68/5.27 % (3590170)Instruction limit reached!
% 34.68/5.27 % (3590170)------------------------------
% 34.68/5.27 % (3590170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.68/5.27 % (3590170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.68/5.27 % (3590170)CaDiCaL version: 2.1.3
% 34.68/5.27 % (3590170)Termination reason: Instruction limit
% 34.68/5.27 % (3590170)Termination phase: Saturation
% 34.68/5.27 % (3590170)Time elapsed: 3.701 s
% 34.68/5.27 % (3590170)Peak memory usage: 16 MB
% 34.68/5.27 % (3590170)Instructions burned: 5114 (million)
% 34.68/5.27 % (3590196)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2474700462:i=8173:av=off_2951 on theBenchmark for (2951ds/8173Mi)
% 34.68/5.27 % (3590117) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3590111-3590117"...
% 34.68/5.27 % (3590117)...printing done.
% 34.68/5.27 % (3590117)Refutation found. Thanks to Tanya!
% 34.68/5.27 % SZS status Theorem for theBenchmark
% 34.68/5.27 % SZS output start Proof for theBenchmark
% 34.68/5.27 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 34.68/5.27 thf(func_def_0, type, in: ($i > $i > $o)).
% 34.68/5.27 thf(func_def_2, type, setadjoin: ($i > $i > $i)).
% 34.68/5.27 thf(func_def_3, type, setunion: ($i > $i)).
% 34.68/5.27 thf(func_def_4, type, dsetconstr: ($i > ($i > $o) > $i)).
% 34.68/5.27 thf(func_def_5, type, subset: ($i > $i > $o)).
% 34.68/5.27 thf(func_def_6, type, subsetE: $o).
% 34.68/5.27 thf(func_def_8, type, sepSubset: $o).
% 34.68/5.27 thf(func_def_9, type, singleton: ($i > $o)).
% 34.68/5.27 thf(func_def_10, type, theprop: $o).
% 34.68/5.27 thf(func_def_11, type, ifSingleton: $o).
% 34.68/5.27 thf(func_def_12, type, if: ($i > $o > $i > $i > $i)).
% 34.68/5.27 thf(func_def_13, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 34.68/5.27 thf(func_def_14, type, vIMP: ($o > $o > $o)).
% 34.68/5.27 thf(func_def_15, type, db0: !>[X0: $tType]:(X0)).
% 34.68/5.27 thf(func_def_16, type, db1: !>[X0: $tType]:(X0)).
% 34.68/5.27 thf(func_def_17, type, db2: !>[X0: $tType]:(X0)).
% 34.68/5.27 thf(func_def_18, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 34.68/5.27 thf(func_def_19, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 34.68/5.27 thf(func_def_20, type, vAND: ($o > $o > $o)).
% 34.68/5.27 thf(func_def_21, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 34.68/5.27 thf(func_def_22, type, vOR: ($o > $o > $o)).
% 34.68/5.27 thf(func_def_23, type, db3: !>[X0: $tType]:(X0)).
% 34.68/5.27 thf(func_def_24, type, db4: !>[X0: $tType]:(X0)).
% 34.68/5.27 thf(func_def_25, type, vNOT: ($o > $o)).
% 34.68/5.27 thf(func_def_29, type, sK1: $o).
% 34.68/5.27 thf(func_def_32, type, sK4: ($i > $o > $i > $i > $i)).
% 34.68/5.27 thf(func_def_34, type, sK6: ($i > $i)).
% 34.68/5.27 thf(func_def_35, type, sK7: ($i > $i)).
% 34.68/5.27 thf(func_def_36, type, sK8: ($i > $i)).
% 34.68/5.27 thf(func_def_37, type, sK9: ($i > $i)).
% 34.68/5.27 thf(func_def_38, type, sK10: ($i > $i)).
% 34.68/5.27 thf(func_def_39, type, sK11: ($i > $i)).
% 34.68/5.27 thf(func_def_40, type, sK12: ($i > $i)).
% 34.68/5.27 thf(func_def_41, type, sK13: ($i > $i)).
% 34.68/5.27 thf(f1,axiom,(
% 34.68/5.27 (subsetE = ! [X0 : $i,X1 : $i,X2 : $i] : ((subset @ X0 @ X1) => ((in @ X2 @ X0) => (in @ X2 @ X1))))),
% 34.68/5.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p',subsetE)).
% 34.68/5.27 thf(f2,axiom,(
% 34.68/5.27 (sepSubset = ! [X0 : $i,X1 : ($i > $o)] : (subset @ (dsetconstr @ X0 @ (^[X2 : $i] : ((X1 @ X2)))) @ X0))),
% 34.68/5.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p',sepSubset)).
% 34.68/5.27 thf(f3,axiom,(
% 34.68/5.27 (singleton = (^[X0 : $i] : (? [X1 : $i] : ((X0 = ((setadjoin @ X1 @ emptyset))) & (in @ X1 @ X0)))))),
% 34.68/5.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p',singleton)).
% 34.68/5.27 thf(f4,axiom,(
% 34.68/5.27 (theprop = ! [X0 : $i] : ((singleton @ X0) => (in @ (setunion @ X0) @ X0)))),
% 34.68/5.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p',theprop)).
% 34.68/5.27 thf(f5,axiom,(
% 34.68/5.27 (ifSingleton = ! [X0 : $i,X1 : $o,X2 : $i] : ((in @ X2 @ X0) => ! [X3 : $i] : ((in @ X3 @ X0) => (singleton @ (dsetconstr @ X0 @ (^[X4 : $i] : (((X4 = X3) & ~X1) | ((X4 = X2) & X1))))))))),
% 34.68/5.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ifSingleton)).
% 34.68/5.27 thf(f6,axiom,(
% 34.68/5.27 (if = (^[X0 : $i, X1 : $o, X2 : $i, X3 : $i] : ((setunion @ (dsetconstr @ X0 @ (^[X4 : $i] : (((X4 = X3) & ~X1) | ((X4 = X2) & X1))))))))),
% 34.68/5.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p',if)).
% 34.68/5.27 thf(f7,conjecture,(
% 34.68/5.27 subsetE => (sepSubset => (theprop => (ifSingleton => ! [X0 : $i,X1 : $o,X2 : $i] : ((in @ X2 @ X0) => ! [X3 : $i] : ((in @ X3 @ X0) => (in @ (if @ X0 @ X1 @ X2 @ X3) @ X0))))))),
% 34.68/5.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ifp)).
% 34.68/5.27 thf(f8,negated_conjecture,(
% 34.68/5.27 ~(subsetE => (sepSubset => (theprop => (ifSingleton => ! [X0 : $i,X1 : $o,X2 : $i] : ((in @ X2 @ X0) => ! [X3 : $i] : ((in @ X3 @ X0) => (in @ (if @ X0 @ X1 @ X2 @ X3) @ X0)))))))),
% 34.68/5.27 inference(negated_conjecture,[status(cth)],[f7])).
% 34.68/5.27 thf(f9,plain,(
% 34.68/5.27 (subsetE = ! [X0 : $i,X1 : $i,X2 : $i] : ((subset @ X0 @ X1) => ((in @ X2 @ X0) => (in @ X2 @ X1))))),
% 34.68/5.27 inference(rectify,[],[f1])).
% 34.68/5.27 thf(f10,plain,(
% 34.68/5.27 (subsetE = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((subset @ Y2 @ Y1) => ((in @ Y0 @ Y2) => (in @ Y0 @ Y1)))))))))))),
% 34.68/5.27 inference(fool_elimination,[],[f9])).
% 34.68/5.27 thf(f11,plain,(
% 34.68/5.27 (sepSubset = ! [X0 : $i,X1 : ($i > $o)] : (subset @ (dsetconstr @ X0 @ (^[X2 : $i] : ((X1 @ X2)))) @ X0))),
% 34.68/5.27 inference(rectify,[],[f2])).
% 34.68/5.27 thf(f12,plain,(
% 34.68/5.27 (sepSubset = ((!! @ ($i > $o) @ (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (subset @ (dsetconstr @ Y1 @ (^[Y2 : $i]: (Y0 @ Y2))) @ Y1)))))))),
% 34.68/5.27 inference(fool_elimination,[],[f11])).
% 34.68/5.27 thf(f13,plain,(
% 34.68/5.27 (singleton = (^[X0 : $i] : (? [X1 : $i] : ((X0 = ((setadjoin @ X1 @ emptyset))) & (in @ X1 @ X0)))))),
% 34.68/5.27 inference(rectify,[],[f3])).
% 34.68/5.27 thf(f14,plain,(
% 34.68/5.27 (singleton = (^[Y0 : $i]: (?? @ $i @ (^[Y1 : $i]: ((in @ Y1 @ Y0) & ((setadjoin @ Y1 @ emptyset) = Y0))))))),
% 34.68/5.27 inference(fool_elimination,[],[f13])).
% 34.68/5.27 thf(f15,plain,(
% 34.68/5.27 (theprop = ! [X0 : $i] : ((singleton @ X0) => (in @ (setunion @ X0) @ X0)))),
% 34.68/5.27 inference(rectify,[],[f4])).
% 34.68/5.27 thf(f16,plain,(
% 34.68/5.27 (theprop = ((!! @ $i @ (^[Y0 : $i]: ((singleton @ Y0) => (in @ (setunion @ Y0) @ Y0))))))),
% 34.68/5.28 inference(fool_elimination,[],[f15])).
% 34.68/5.28 thf(f17,plain,(
% 34.68/5.28 (ifSingleton = ! [X0 : $i,X1 : $o,X2 : $i] : ((in @ X2 @ X0) => ! [X3 : $i] : ((in @ X3 @ X0) => (singleton @ (dsetconstr @ X0 @ (^[X4 : $i] : (((X4 = X3) & ~X1) | ((X4 = X2) & X1))))))))),
% 34.68/5.28 inference(rectify,[],[f5])).
% 34.68/5.28 thf(f18,plain,(
% 34.68/5.28 (ifSingleton = ((!! @ $i @ (^[Y0 : $i]: (!! @ $o @ (^[Y1 : $o]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y0 @ Y2) => (!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ Y2) => (singleton @ (dsetconstr @ Y2 @ (^[Y4 : $i]: ((Y1 & (Y0 = Y4)) | ((~ Y1) & (Y3 = Y4))))))))))))))))))),
% 34.68/5.28 inference(fool_elimination,[],[f17])).
% 34.68/5.28 thf(f19,plain,(
% 34.68/5.28 (if = (^[X0 : $i, X1 : $o, X2 : $i, X3 : $i] : ((setunion @ (dsetconstr @ X0 @ (^[X4 : $i] : (((X4 = X3) & ~X1) | ((X4 = X2) & X1))))))))),
% 34.68/5.28 inference(rectify,[],[f6])).
% 34.68/5.28 thf(f20,plain,(
% 34.68/5.28 (if = (^[Y0 : $i]: ((^[Y1 : $o]: ((^[Y2 : $i]: ((^[Y3 : $i]: (setunion @ (dsetconstr @ Y0 @ (^[Y4 : $i]: ((Y1 & (Y2 = Y4)) | ((~ Y1) & (Y3 = Y4))))))))))))))),
% 34.68/5.28 inference(fool_elimination,[],[f19])).
% 34.68/5.28 thf(f21,plain,(
% 34.68/5.28 ~(subsetE => (sepSubset => (theprop => (ifSingleton => ! [X0 : $i,X1 : $o,X2 : $i] : ((in @ X2 @ X0) => ! [X3 : $i] : ((in @ X3 @ X0) => (in @ (if @ X0 @ X1 @ X2 @ X3) @ X0)))))))),
% 34.68/5.28 inference(rectify,[],[f8])).
% 34.68/5.28 thf(f22,plain,(
% 34.68/5.28 ~((subsetE = $true) => ((sepSubset = $true) => ((theprop = $true) => ((ifSingleton = $true) => ! [X0 : $i,X1 : $o,X2 : $i] : ((((in @ X2 @ X0)) = $true) => ! [X3 : $i] : ((((in @ X3 @ X0)) = $true) => (((in @ (if @ X0 @ X1 @ X2 @ X3) @ X0)) = $true)))))))),
% 34.68/5.28 inference(fool_elimination,[],[f21])).
% 34.68/5.28 thf(f23,plain,(
% 34.68/5.28 (((? [X0 : $i,X1 : $o,X2 : $i] : (? [X3 : $i] : ((((in @ (if @ X0 @ X1 @ X2 @ X3) @ X0)) != $true) & (((in @ X3 @ X0)) = $true)) & (((in @ X2 @ X0)) = $true)) & (ifSingleton = $true)) & (theprop = $true)) & (sepSubset = $true)) & (subsetE = $true)),
% 34.68/5.28 inference(ennf_transformation,[],[f22])).
% 34.68/5.28 thf(f24,plain,(
% 34.68/5.28 ? [X0 : $i,X1 : $o,X2 : $i] : (? [X3 : $i] : ((((in @ (if @ X0 @ X1 @ X2 @ X3) @ X0)) != $true) & (((in @ X3 @ X0)) = $true)) & (((in @ X2 @ X0)) = $true)) & (ifSingleton = $true) & (theprop = $true) & (sepSubset = $true) & (subsetE = $true)),
% 34.68/5.28 inference(flattening,[],[f23])).
% 34.68/5.28 thf(f25,plain,(
% 34.68/5.28 ((($true != ((in @ (if @ sK0 @ sK1 @ sK2 @ sK3) @ sK0))) & ($true = ((in @ sK3 @ sK0)))) & ($true = ((in @ sK2 @ sK0)))) & (ifSingleton = $true) & (theprop = $true) & (sepSubset = $true) & (subsetE = $true)),
% 34.68/5.28 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3)],[f24])).
% 34.68/5.28 thf(f26,plain,(
% 34.68/5.28 (subsetE = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((subset @ Y2 @ Y1) => ((in @ Y0 @ Y2) => (in @ Y0 @ Y1)))))))))))),
% 34.68/5.28 inference(cnf_transformation,[],[f10])).
% 34.68/5.28 thf(f27,plain,(
% 34.68/5.28 (sepSubset = ((!! @ ($i > $o) @ (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (subset @ (dsetconstr @ Y1 @ (^[Y2 : $i]: (Y0 @ Y2))) @ Y1)))))))),
% 34.68/5.28 inference(cnf_transformation,[],[f12])).
% 34.68/5.28 thf(f28,plain,(
% 34.68/5.28 (singleton = (^[Y0 : $i]: (?? @ $i @ (^[Y1 : $i]: ((in @ Y1 @ Y0) & ((setadjoin @ Y1 @ emptyset) = Y0))))))),
% 34.68/5.28 inference(cnf_transformation,[],[f14])).
% 34.68/5.28 thf(f29,plain,(
% 34.68/5.28 (theprop = ((!! @ $i @ (^[Y0 : $i]: ((singleton @ Y0) => (in @ (setunion @ Y0) @ Y0))))))),
% 34.68/5.28 inference(cnf_transformation,[],[f16])).
% 34.68/5.28 thf(f30,plain,(
% 34.68/5.28 (ifSingleton = ((!! @ $i @ (^[Y0 : $i]: (!! @ $o @ (^[Y1 : $o]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y0 @ Y2) => (!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ Y2) => (singleton @ (dsetconstr @ Y2 @ (^[Y4 : $i]: ((Y1 & (Y0 = Y4)) | ((~ Y1) & (Y3 = Y4))))))))))))))))))),
% 34.68/5.28 inference(cnf_transformation,[],[f18])).
% 34.68/5.28 thf(f31,plain,(
% 34.68/5.28 (if = (^[Y0 : $i]: ((^[Y1 : $o]: ((^[Y2 : $i]: ((^[Y3 : $i]: (setunion @ (dsetconstr @ Y0 @ (^[Y4 : $i]: ((Y1 & (Y2 = Y4)) | ((~ Y1) & (Y3 = Y4))))))))))))))),
% 34.68/5.28 inference(cnf_transformation,[],[f20])).
% 34.68/5.28 thf(f32,plain,(
% 34.68/5.28 (subsetE = $true)),
% 34.68/5.28 inference(cnf_transformation,[],[f25])).
% 34.68/5.28 thf(f33,plain,(
% 34.68/5.28 (sepSubset = $true)),
% 34.68/5.28 inference(cnf_transformation,[],[f25])).
% 34.68/5.28 thf(f34,plain,(
% 34.68/5.28 (theprop = $true)),
% 34.68/5.28 inference(cnf_transformation,[],[f25])).
% 34.68/5.28 thf(f35,plain,(
% 34.68/5.28 (ifSingleton = $true)),
% 34.68/5.28 inference(cnf_transformation,[],[f25])).
% 34.68/5.28 thf(f36,plain,(
% 34.68/5.28 ($true = ((in @ sK2 @ sK0)))),
% 34.68/5.28 inference(cnf_transformation,[],[f25])).
% 34.68/5.28 thf(f37,plain,(
% 34.68/5.28 ($true = ((in @ sK3 @ sK0)))),
% 34.68/5.28 inference(cnf_transformation,[],[f25])).
% 34.68/5.28 thf(f38,plain,(
% 34.68/5.28 ($true != ((in @ (if @ sK0 @ sK1 @ sK2 @ sK3) @ sK0)))),
% 34.68/5.28 inference(cnf_transformation,[],[f25])).
% 34.68/5.28 thf(f40,definition,(
% 34.68/5.28 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 34.68/5.28 introduced(theory,[fool_exhaustiveness_axiom])).
% 34.68/5.28 thf(f41,plain,(
% 34.68/5.28 (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((subset @ Y2 @ Y1) => ((in @ Y0 @ Y2) => (in @ Y0 @ Y1)))))))))) = $true)),
% 34.68/5.28 inference(definition_unfolding,[],[f26,f32])).
% 34.68/5.28 thf(f42,plain,(
% 34.68/5.28 (((!! @ ($i > $o) @ (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (subset @ (dsetconstr @ Y1 @ (^[Y2 : $i]: (Y0 @ Y2))) @ Y1)))))) = $true)),
% 34.68/5.28 inference(definition_unfolding,[],[f27,f33])).
% 34.68/5.28 thf(f43,plain,(
% 34.68/5.28 ($true = ((!! @ $i @ (^[Y0 : $i]: (((^[Y1 : $i]: (?? @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) & ((setadjoin @ Y2 @ emptyset) = Y1))))) @ Y0) => (in @ (setunion @ Y0) @ Y0))))))),
% 34.68/5.28 inference(definition_unfolding,[],[f29,f34,f28])).
% 34.68/5.28 thf(f44,plain,(
% 34.68/5.28 ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $o @ (^[Y1 : $o]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y0 @ Y2) => (!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ Y2) => ((^[Y4 : $i]: (?? @ $i @ (^[Y5 : $i]: ((in @ Y5 @ Y4) & ((setadjoin @ Y5 @ emptyset) = Y4))))) @ (dsetconstr @ Y2 @ (^[Y4 : $i]: ((Y1 & (Y0 = Y4)) | ((~ Y1) & (Y3 = Y4))))))))))))))))))),
% 34.68/5.28 inference(definition_unfolding,[],[f30,f35,f28])).
% 34.68/5.28 thf(f45,plain,(
% 34.68/5.28 ($true != ((in @ ((^[Y0 : $i]: ((^[Y1 : $o]: ((^[Y2 : $i]: ((^[Y3 : $i]: (setunion @ (dsetconstr @ Y0 @ (^[Y4 : $i]: ((Y1 & (Y2 = Y4)) | ((~ Y1) & (Y3 = Y4))))))))))))) @ sK0 @ sK1 @ sK2 @ sK3) @ sK0)))),
% 34.68/5.28 inference(definition_unfolding,[],[f38,f31])).
% 34.68/5.28 thf(f46,plain,(
% 34.68/5.28 ($true != ((in @ (setunion @ (dsetconstr @ sK0 @ (^[Y0 : $i]: ((sK1 & (sK2 = Y0)) | ((~ sK1) & (sK3 = Y0)))))) @ sK0)))),
% 34.68/5.28 inference(beta-eta_normalization,[],[f45])).
% 34.68/5.28 thf(f47,plain,(
% 34.68/5.28 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $o @ (^[Y1 : $o]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y0 @ Y2) => (!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ Y2) => ((^[Y4 : $i]: (?? @ $i @ (^[Y5 : $i]: ((in @ Y5 @ Y4) & ((setadjoin @ Y5 @ emptyset) = Y4))))) @ (dsetconstr @ Y2 @ (^[Y4 : $i]: ((Y1 & (Y0 = Y4)) | ((~ Y1) & (Y3 = Y4))))))))))))))) @ X1)))) )),
% 34.68/5.28 inference(pi_proxy_clausification,[],[f44])).
% 34.68/5.28 thf(f48,plain,(
% 34.68/5.28 ( ! [X1 : $i] : (($true = ((!! @ $o @ (^[Y0 : $o]: (!! @ $i @ (^[Y1 : $i]: ((in @ X1 @ Y1) => (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) => (?? @ $i @ (^[Y3 : $i]: ((in @ Y3 @ (dsetconstr @ Y1 @ (^[Y4 : $i]: ((Y0 & (X1 = Y4)) | ((~ Y0) & (Y2 = Y4)))))) & ((setadjoin @ Y3 @ emptyset) = (dsetconstr @ Y1 @ (^[Y4 : $i]: ((Y0 & (X1 = Y4)) | ((~ Y0) & (Y2 = Y4)))))))))))))))))))) )),
% 34.68/5.28 inference(beta-eta_normalization,[],[f47])).
% 34.68/5.28 thf(f49,plain,(
% 34.68/5.28 ( ! [X2 : $o,X1 : $i] : (($true = (((^[Y0 : $o]: (!! @ $i @ (^[Y1 : $i]: ((in @ X1 @ Y1) => (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) => (?? @ $i @ (^[Y3 : $i]: ((in @ Y3 @ (dsetconstr @ Y1 @ (^[Y4 : $i]: ((Y0 & (X1 = Y4)) | ((~ Y0) & (Y2 = Y4)))))) & ((setadjoin @ Y3 @ emptyset) = (dsetconstr @ Y1 @ (^[Y4 : $i]: ((Y0 & (X1 = Y4)) | ((~ Y0) & (Y2 = Y4)))))))))))))))) @ X2)))) )),
% 34.68/5.28 inference(pi_proxy_clausification,[],[f48])).
% 34.68/5.28 thf(f50,plain,(
% 34.68/5.28 ( ! [X2 : $o,X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((in @ X1 @ Y0) => (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ Y0) => (?? @ $i @ (^[Y2 : $i]: ((in @ Y2 @ (dsetconstr @ Y0 @ (^[Y3 : $i]: ((X2 & (X1 = Y3)) | ((~ X2) & (Y1 = Y3)))))) & ((setadjoin @ Y2 @ emptyset) = (dsetconstr @ Y0 @ (^[Y3 : $i]: ((X2 & (X1 = Y3)) | ((~ X2) & (Y1 = Y3)))))))))))))))))) )),
% 34.68/5.28 inference(beta-eta_normalization,[],[f49])).
% 34.68/5.28 thf(f51,plain,(
% 34.68/5.28 ( ! [X2 : $o,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((in @ X1 @ Y0) => (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ Y0) => (?? @ $i @ (^[Y2 : $i]: ((in @ Y2 @ (dsetconstr @ Y0 @ (^[Y3 : $i]: ((X2 & (X1 = Y3)) | ((~ X2) & (Y1 = Y3)))))) & ((setadjoin @ Y2 @ emptyset) = (dsetconstr @ Y0 @ (^[Y3 : $i]: ((X2 & (X1 = Y3)) | ((~ X2) & (Y1 = Y3)))))))))))))) @ X3)))) )),
% 34.68/5.28 inference(pi_proxy_clausification,[],[f50])).
% 34.68/5.28 thf(f52,plain,(
% 34.68/5.28 ( ! [X2 : $o,X3 : $i,X1 : $i] : (($true = (((in @ X1 @ X3) => (!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X3) => (?? @ $i @ (^[Y1 : $i]: ((in @ Y1 @ (dsetconstr @ X3 @ (^[Y2 : $i]: ((X2 & (X1 = Y2)) | ((~ X2) & (Y0 = Y2)))))) & ((setadjoin @ Y1 @ emptyset) = (dsetconstr @ X3 @ (^[Y2 : $i]: ((X2 & (X1 = Y2)) | ((~ X2) & (Y0 = Y2)))))))))))))))) )),
% 34.68/5.28 inference(beta-eta_normalization,[],[f51])).
% 34.68/5.28 thf(f53,plain,(
% 34.68/5.28 ( ! [X2 : $o,X3 : $i,X1 : $i] : (($false = ((in @ X1 @ X3))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X3) => (?? @ $i @ (^[Y1 : $i]: ((in @ Y1 @ (dsetconstr @ X3 @ (^[Y2 : $i]: ((X2 & (X1 = Y2)) | ((~ X2) & (Y0 = Y2)))))) & ((setadjoin @ Y1 @ emptyset) = (dsetconstr @ X3 @ (^[Y2 : $i]: ((X2 & (X1 = Y2)) | ((~ X2) & (Y0 = Y2))))))))))))))) )),
% 34.68/5.28 inference(imp_proxy_clausification,[],[f52])).
% 34.68/5.28 thf(f54,plain,(
% 34.68/5.28 ( ! [X2 : $o,X3 : $i,X1 : $i,X4 : $i] : (($false = ((in @ X1 @ X3))) | ($true = (((^[Y0 : $i]: ((in @ Y0 @ X3) => (?? @ $i @ (^[Y1 : $i]: ((in @ Y1 @ (dsetconstr @ X3 @ (^[Y2 : $i]: ((X2 & (X1 = Y2)) | ((~ X2) & (Y0 = Y2)))))) & ((setadjoin @ Y1 @ emptyset) = (dsetconstr @ X3 @ (^[Y2 : $i]: ((X2 & (X1 = Y2)) | ((~ X2) & (Y0 = Y2))))))))))) @ X4)))) )),
% 34.68/5.28 inference(pi_proxy_clausification,[],[f53])).
% 34.68/5.28 thf(f55,plain,(
% 34.68/5.28 ( ! [X2 : $o,X3 : $i,X1 : $i,X4 : $i] : (($false = ((in @ X1 @ X3))) | ($true = (((in @ X4 @ X3) => (?? @ $i @ (^[Y0 : $i]: ((in @ Y0 @ (dsetconstr @ X3 @ (^[Y1 : $i]: ((X2 & (X1 = Y1)) | ((~ X2) & (X4 = Y1)))))) & ((setadjoin @ Y0 @ emptyset) = (dsetconstr @ X3 @ (^[Y1 : $i]: ((X2 & (X1 = Y1)) | ((~ X2) & (X4 = Y1))))))))))))) )),
% 34.68/5.28 inference(beta-eta_normalization,[],[f54])).
% 34.68/5.28 thf(f56,plain,(
% 34.68/5.28 ( ! [X2 : $o,X3 : $i,X1 : $i,X4 : $i] : (($false = ((in @ X1 @ X3))) | ($false = ((in @ X4 @ X3))) | ($true = ((?? @ $i @ (^[Y0 : $i]: ((in @ Y0 @ (dsetconstr @ X3 @ (^[Y1 : $i]: ((X2 & (X1 = Y1)) | ((~ X2) & (X4 = Y1)))))) & ((setadjoin @ Y0 @ emptyset) = (dsetconstr @ X3 @ (^[Y1 : $i]: ((X2 & (X1 = Y1)) | ((~ X2) & (X4 = Y1)))))))))))) )),
% 34.68/5.28 inference(imp_proxy_clausification,[],[f55])).
% 34.68/5.28 thf(f57,plain,(
% 34.68/5.28 ( ! [X2 : $o,X3 : $i,X1 : $i,X4 : $i] : (($false = ((in @ X1 @ X3))) | ($false = ((in @ X4 @ X3))) | ($true = (((^[Y0 : $i]: ((in @ Y0 @ (dsetconstr @ X3 @ (^[Y1 : $i]: ((X2 & (X1 = Y1)) | ((~ X2) & (X4 = Y1)))))) & ((setadjoin @ Y0 @ emptyset) = (dsetconstr @ X3 @ (^[Y1 : $i]: ((X2 & (X1 = Y1)) | ((~ X2) & (X4 = Y1)))))))) @ (sK4 @ X1 @ X2 @ X3 @ X4))))) )),
% 34.68/5.28 inference(sigma_proxy_clausification,[],[f56])).
% 34.68/5.28 thf(f58,plain,(
% 34.68/5.28 ( ! [X2 : $o,X3 : $i,X1 : $i,X4 : $i] : (($false = ((in @ X1 @ X3))) | ($false = ((in @ X4 @ X3))) | ($true = (((in @ (sK4 @ X1 @ X2 @ X3 @ X4) @ (dsetconstr @ X3 @ (^[Y0 : $i]: ((X2 & (X1 = Y0)) | ((~ X2) & (X4 = Y0)))))) & ((setadjoin @ (sK4 @ X1 @ X2 @ X3 @ X4) @ emptyset) = (dsetconstr @ X3 @ (^[Y0 : $i]: ((X2 & (X1 = Y0)) | ((~ X2) & (X4 = Y0)))))))))) )),
% 34.68/5.28 inference(beta-eta_normalization,[],[f57])).
% 34.68/5.28 thf(f59,plain,(
% 34.68/5.28 ( ! [X2 : $o,X3 : $i,X1 : $i,X4 : $i] : (($false = ((in @ X1 @ X3))) | ($false = ((in @ X4 @ X3))) | ($true = (((setadjoin @ (sK4 @ X1 @ X2 @ X3 @ X4) @ emptyset) = (dsetconstr @ X3 @ (^[Y0 : $i]: ((X2 & (X1 = Y0)) | ((~ X2) & (X4 = Y0))))))))) )),
% 34.68/5.28 inference(and_proxy_clausification,[],[f58])).
% 34.68/5.28 thf(f60,plain,(
% 34.68/5.28 ( ! [X2 : $o,X3 : $i,X1 : $i,X4 : $i] : (($true = ((in @ (sK4 @ X1 @ X2 @ X3 @ X4) @ (dsetconstr @ X3 @ (^[Y0 : $i]: ((X2 & (X1 = Y0)) | ((~ X2) & (X4 = Y0)))))))) | ($false = ((in @ X4 @ X3))) | ($false = ((in @ X1 @ X3)))) )),
% 34.68/5.28 inference(and_proxy_clausification,[],[f58])).
% 34.68/5.28 thf(f61,plain,(
% 34.68/5.28 ( ! [X2 : $o,X3 : $i,X1 : $i,X4 : $i] : ((((dsetconstr @ X3 @ (^[Y0 : $i]: ((X2 & (X1 = Y0)) | ((~ X2) & (X4 = Y0)))))) = ((setadjoin @ (sK4 @ X1 @ X2 @ X3 @ X4) @ emptyset))) | ($false = ((in @ X4 @ X3))) | ($false = ((in @ X1 @ X3)))) )),
% 34.68/5.28 inference(equality_proxy_clausification,[],[f59])).
% 34.68/5.28 thf(f62,plain,(
% 34.68/5.28 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (((^[Y1 : $i]: (?? @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) & ((setadjoin @ Y2 @ emptyset) = Y1))))) @ Y0) => (in @ (setunion @ Y0) @ Y0))) @ X1)))) )),
% 34.68/5.28 inference(pi_proxy_clausification,[],[f43])).
% 34.68/5.28 thf(f63,plain,(
% 34.68/5.28 ( ! [X1 : $i] : (($true = (((?? @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X1) & ((setadjoin @ Y0 @ emptyset) = X1)))) => (in @ (setunion @ X1) @ X1))))) )),
% 34.68/5.28 inference(beta-eta_normalization,[],[f62])).
% 34.68/5.28 thf(f64,plain,(
% 34.68/5.28 ( ! [X1 : $i] : (($false = ((?? @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X1) & ((setadjoin @ Y0 @ emptyset) = X1)))))) | ($true = ((in @ (setunion @ X1) @ X1)))) )),
% 34.68/5.28 inference(imp_proxy_clausification,[],[f63])).
% 34.68/5.28 thf(f65,plain,(
% 34.68/5.28 ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ((in @ Y0 @ X1) & ((setadjoin @ Y0 @ emptyset) = X1))) @ X2))) | ($true = ((in @ (setunion @ X1) @ X1)))) )),
% 34.68/5.28 inference(pi_proxy_clausification,[],[f64])).
% 34.68/5.28 thf(f66,plain,(
% 34.68/5.28 ( ! [X2 : $i,X1 : $i] : (($false = (((in @ X2 @ X1) & ((setadjoin @ X2 @ emptyset) = X1)))) | ($true = ((in @ (setunion @ X1) @ X1)))) )),
% 34.68/5.28 inference(beta-eta_normalization,[],[f65])).
% 34.68/5.28 thf(f67,plain,(
% 34.68/5.28 ( ! [X2 : $i,X1 : $i] : (($false = (((setadjoin @ X2 @ emptyset) = X1))) | ($true = ((in @ (setunion @ X1) @ X1))) | (((in @ X2 @ X1)) = $false)) )),
% 34.68/5.28 inference(and_proxy_clausification,[],[f66])).
% 34.68/5.28 thf(f68,plain,(
% 34.68/5.28 ( ! [X2 : $i,X1 : $i] : ((((setadjoin @ X2 @ emptyset)) != X1) | ($true = ((in @ (setunion @ X1) @ X1))) | (((in @ X2 @ X1)) = $false)) )),
% 34.68/5.28 inference(equality_proxy_clausification,[],[f67])).
% 34.68/5.28 thf(f69,plain,(
% 34.68/5.28 ( ! [X1 : ($i > $o)] : (($true = (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (subset @ (dsetconstr @ Y1 @ (^[Y2 : $i]: (Y0 @ Y2))) @ Y1)))) @ X1)))) )),
% 34.68/5.28 inference(pi_proxy_clausification,[],[f42])).
% 34.68/5.28 thf(f70,plain,(
% 34.68/5.28 ( ! [X1 : ($i > $o)] : (($true = ((!! @ $i @ (^[Y0 : $i]: (subset @ (dsetconstr @ Y0 @ X1) @ Y0)))))) )),
% 34.68/5.28 inference(beta-eta_normalization,[],[f69])).
% 34.68/5.28 thf(f71,plain,(
% 34.68/5.28 ( ! [X2 : $i,X1 : ($i > $o)] : (($true = (((^[Y0 : $i]: (subset @ (dsetconstr @ Y0 @ X1) @ Y0)) @ X2)))) )),
% 34.68/5.28 inference(pi_proxy_clausification,[],[f70])).
% 34.68/5.28 thf(f72,plain,(
% 34.68/5.28 ( ! [X2 : $i,X1 : ($i > $o)] : (($true = ((subset @ (dsetconstr @ X2 @ X1) @ X2)))) )),
% 34.68/5.28 inference(beta-eta_normalization,[],[f71])).
% 34.68/5.28 thf(f73,plain,(
% 34.68/5.28 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((subset @ Y2 @ Y1) => ((in @ Y0 @ Y2) => (in @ Y0 @ Y1)))))))) @ X1)))) )),
% 34.68/5.28 inference(pi_proxy_clausification,[],[f41])).
% 34.68/5.28 thf(f74,plain,(
% 34.68/5.28 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((subset @ Y1 @ Y0) => ((in @ X1 @ Y1) => (in @ X1 @ Y0)))))))))) )),
% 34.68/5.28 inference(beta-eta_normalization,[],[f73])).
% 34.68/5.28 thf(f75,plain,(
% 34.68/5.28 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((subset @ Y1 @ Y0) => ((in @ X1 @ Y1) => (in @ X1 @ Y0)))))) @ X2)))) )),
% 34.68/5.28 inference(pi_proxy_clausification,[],[f74])).
% 34.68/5.28 thf(f76,plain,(
% 34.68/5.28 ( ! [X2 : $i,X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((subset @ Y0 @ X2) => ((in @ X1 @ Y0) => (in @ X1 @ X2)))))))) )),
% 34.68/5.28 inference(beta-eta_normalization,[],[f75])).
% 34.68/5.28 thf(f77,plain,(
% 34.68/5.28 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((subset @ Y0 @ X2) => ((in @ X1 @ Y0) => (in @ X1 @ X2)))) @ X3)))) )),
% 34.68/5.28 inference(pi_proxy_clausification,[],[f76])).
% 34.68/5.28 thf(f78,plain,(
% 34.68/5.28 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((subset @ X3 @ X2) => ((in @ X1 @ X3) => (in @ X1 @ X2)))))) )),
% 34.68/5.28 inference(beta-eta_normalization,[],[f77])).
% 34.68/5.28 thf(f79,plain,(
% 34.68/5.28 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((subset @ X3 @ X2))) | ($true = (((in @ X1 @ X3) => (in @ X1 @ X2))))) )),
% 34.68/5.28 inference(imp_proxy_clausification,[],[f78])).
% 34.68/5.28 thf(f80,plain,(
% 34.68/5.28 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((subset @ X3 @ X2))) | ($false = ((in @ X1 @ X3))) | ($true = ((in @ X1 @ X2)))) )),
% 34.68/5.28 inference(imp_proxy_clausification,[],[f79])).
% 34.68/5.28 thf(f90,plain,(
% 34.68/5.28 ( ! [X0 : $i] : (($true = ((in @ (setunion @ (setadjoin @ X0 @ emptyset)) @ (setadjoin @ X0 @ emptyset)))) | ($false = ((in @ X0 @ (setadjoin @ X0 @ emptyset))))) )),
% 34.68/5.28 inference(equality_resolution,[],[f68])).
% 34.68/5.28 thf(f104,plain,(
% 34.68/5.28 ($true != $true) | ($false = ((in @ (setunion @ (dsetconstr @ sK0 @ (^[Y0 : $i]: ((sK1 & (sK2 = Y0)) | ((~ sK1) & (sK3 = Y0)))))) @ sK0)))),
% 34.68/5.28 inference(constrained_superposition,[],[f46,f40])).
% 34.68/5.28 thf(f105,plain,(
% 34.68/5.28 ($false = ((in @ (setunion @ (dsetconstr @ sK0 @ (^[Y0 : $i]: ((sK1 & (sK2 = Y0)) | ((~ sK1) & (sK3 = Y0)))))) @ sK0)))),
% 34.68/5.28 inference(trivial_inequality_removal,[],[f104])).
% 34.68/5.28 thf(f154,plain,(
% 34.68/5.28 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((subset @ (setadjoin @ X0 @ emptyset) @ X1))) | ($true = ((in @ (setunion @ (setadjoin @ X0 @ emptyset)) @ X1))) | ($false = ((in @ X0 @ (setadjoin @ X0 @ emptyset))))) )),
% 34.68/5.28 inference(constrained_superposition,[],[f80,f90])).
% 34.68/5.28 thf(f155,plain,(
% 34.68/5.28 ( ! [X0 : $i,X1 : $i] : (($true = ((in @ (setunion @ (setadjoin @ X0 @ emptyset)) @ X1))) | ($false = ((in @ X0 @ (setadjoin @ X0 @ emptyset)))) | ($false = ((subset @ (setadjoin @ X0 @ emptyset) @ X1)))) )),
% 34.68/5.28 inference(trivial_inequality_removal,[],[f154])).
% 34.68/5.28 thf(f321,plain,(
% 34.68/5.28 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $o] : (($true = ((subset @ (setadjoin @ (sK4 @ X0 @ X1 @ X2 @ X3) @ emptyset) @ X2))) | ($false = ((in @ X3 @ X2))) | ($false = ((in @ X0 @ X2)))) )),
% 34.68/5.28 inference(constrained_superposition,[],[f72,f61])).
% 34.68/5.28 thf(f322,plain,(
% 34.68/5.28 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $o,X6 : $i,X4 : $i,X5 : $o] : (($true = ((in @ (sK4 @ X4 @ X5 @ X2 @ X6) @ (setadjoin @ (sK4 @ X0 @ X1 @ X2 @ X3) @ emptyset)))) | ($false = ((in @ X6 @ X2))) | ($false = ((in @ X4 @ X2))) | ($false = ((in @ X3 @ X2))) | ($false = ((in @ X0 @ X2))) | ((^[Y0 : $i]: (X4)) != (^[Y0 : $i]: (X0))) | ((^[Y0 : $i]: (X6)) != (^[Y0 : $i]: (X3))) | ((^[Y0 : $i]: (X1)) != (^[Y0 : $i]: (X5))) | ((^[Y0 : $i]: (X1)) != (^[Y0 : $i]: (X5)))) )),
% 34.68/5.28 inference(constrained_superposition,[],[f60,f61])).
% 34.68/5.28 thf(f325,plain,(
% 34.68/5.28 ( ! [X0 : $i] : (($false = ((in @ (setunion @ (setadjoin @ (sK4 @ sK2 @ sK1 @ sK0 @ X0) @ emptyset)) @ sK0))) | ($false = ((in @ X0 @ sK0))) | (((in @ sK2 @ sK0)) = $false) | ((^[Y0 : $i]: (X0)) != (^[Y0 : $i]: (sK3)))) )),
% 34.68/5.28 inference(constrained_superposition,[],[f105,f61])).
% 34.68/5.28 thf(f327,plain,(
% 34.68/5.28 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $o,X6 : $i,X4 : $i,X5 : $o] : (($true = ((in @ (sK4 @ X4 @ X5 @ X2 @ X6) @ (setadjoin @ (sK4 @ X0 @ X1 @ X2 @ X3) @ emptyset)))) | ($false = ((in @ X6 @ X2))) | ($false = ((in @ X4 @ X2))) | ($false = ((in @ X3 @ X2))) | ($false = ((in @ X0 @ X2))) | ((^[Y0 : $i]: (X4)) != (^[Y0 : $i]: (X0))) | ((^[Y0 : $i]: (X6)) != (^[Y0 : $i]: (X3))) | ((^[Y0 : $i]: (X1)) != (^[Y0 : $i]: (X5)))) )),
% 34.68/5.28 inference(duplicate_literal_removal,[],[f322])).
% 34.68/5.28 thf(f331,plain,(
% 34.68/5.28 ( ! [X0 : $i] : (($true = $false) | ($false = ((in @ (setunion @ (setadjoin @ (sK4 @ sK2 @ sK1 @ sK0 @ X0) @ emptyset)) @ sK0))) | ($false = ((in @ X0 @ sK0))) | ((^[Y0 : $i]: (X0)) != (^[Y0 : $i]: (sK3)))) )),
% 34.68/5.28 inference(forward_demodulation,[],[f325,f36])).
% 34.68/5.28 thf(f332,plain,(
% 34.68/5.28 ( ! [X0 : $i] : (((^[Y0 : $i]: (X0)) != (^[Y0 : $i]: (sK3))) | ($false = ((in @ X0 @ sK0))) | ($false = ((in @ (setunion @ (setadjoin @ (sK4 @ sK2 @ sK1 @ sK0 @ X0) @ emptyset)) @ sK0)))) )),
% 34.68/5.28 inference(trivial_inequality_removal,[],[f331])).
% 34.68/5.28 thf(f844,plain,(
% 34.68/5.28 (((in @ sK3 @ sK0)) = $false) | ($false = ((in @ (setunion @ (setadjoin @ (sK4 @ sK2 @ sK1 @ sK0 @ sK3) @ emptyset)) @ sK0)))),
% 34.68/5.28 inference(equality_resolution,[],[f332])).
% 34.68/5.28 thf(f846,plain,(
% 34.68/5.28 ($true = $false) | ($false = ((in @ (setunion @ (setadjoin @ (sK4 @ sK2 @ sK1 @ sK0 @ sK3) @ emptyset)) @ sK0)))),
% 34.68/5.28 inference(forward_demodulation,[],[f844,f37])).
% 34.68/5.28 thf(f847,plain,(
% 34.68/5.28 ($false = ((in @ (setunion @ (setadjoin @ (sK4 @ sK2 @ sK1 @ sK0 @ sK3) @ emptyset)) @ sK0)))),
% 34.68/5.28 inference(trivial_inequality_removal,[],[f846])).
% 34.68/5.28 thf(f1509,plain,(
% 34.68/5.28 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $o,X4 : $i] : (($true = $false) | ($true = ((in @ (setunion @ (setadjoin @ (sK4 @ X0 @ X1 @ X2 @ X3) @ emptyset)) @ X4))) | ($false = ((subset @ (setadjoin @ (sK4 @ X0 @ X1 @ X2 @ X3) @ emptyset) @ X4))) | ($false = ((in @ X3 @ X2))) | ($false = ((in @ X0 @ X2))) | ($false = ((in @ X3 @ X2))) | ($false = ((in @ X0 @ X2))) | ((^[Y0 : $i]: (X0)) != (^[Y0 : $i]: (X0))) | ((^[Y0 : $i]: (X3)) != (^[Y0 : $i]: (X3))) | ((^[Y0 : $i]: (X1)) != (^[Y0 : $i]: (X1)))) )),
% 34.68/5.28 inference(constrained_superposition,[],[f155,f327])).
% 34.68/5.28 thf(f1513,plain,(
% 34.68/5.28 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $o,X4 : $i] : (($true = $false) | ($true = ((in @ (setunion @ (setadjoin @ (sK4 @ X0 @ X1 @ X2 @ X3) @ emptyset)) @ X4))) | ($false = ((subset @ (setadjoin @ (sK4 @ X0 @ X1 @ X2 @ X3) @ emptyset) @ X4))) | ($false = ((in @ X3 @ X2))) | ($false = ((in @ X0 @ X2))) | ((^[Y0 : $i]: (X0)) != (^[Y0 : $i]: (X0))) | ((^[Y0 : $i]: (X3)) != (^[Y0 : $i]: (X3))) | ((^[Y0 : $i]: (X1)) != (^[Y0 : $i]: (X1)))) )),
% 34.68/5.28 inference(duplicate_literal_removal,[],[f1509])).
% 34.68/5.28 thf(f1514,plain,(
% 34.68/5.28 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $o,X4 : $i] : (($true = ((in @ (setunion @ (setadjoin @ (sK4 @ X0 @ X1 @ X2 @ X3) @ emptyset)) @ X4))) | ($false = ((subset @ (setadjoin @ (sK4 @ X0 @ X1 @ X2 @ X3) @ emptyset) @ X4))) | ($false = ((in @ X3 @ X2))) | ($false = ((in @ X0 @ X2)))) )),
% 34.68/5.28 inference(trivial_inequality_removal,[],[f1513])).
% 34.68/5.28 thf(f13825,definition,(
% 34.68/5.28 spl5_19 <=> ($false = ((subset @ (setadjoin @ (sK4 @ sK2 @ sK1 @ sK0 @ sK3) @ emptyset) @ sK0)))),
% 34.68/5.28 introduced(definition,[new_symbols(definition,[spl5_19])],[avatar_definition])).
% 34.68/5.28 thf(f13826,plain,(
% 34.68/5.28 ($false != ((subset @ (setadjoin @ (sK4 @ sK2 @ sK1 @ sK0 @ sK3) @ emptyset) @ sK0))) | spl5_19),
% 34.68/5.28 inference(avatar_component_clause,[],[f13825])).
% 34.68/5.28 thf(f13827,plain,(
% 34.68/5.28 ($false = ((subset @ (setadjoin @ (sK4 @ sK2 @ sK1 @ sK0 @ sK3) @ emptyset) @ sK0))) | ~spl5_19),
% 34.68/5.28 inference(avatar_component_clause,[],[f13825])).
% 34.68/5.28 thf(f13860,plain,(
% 34.68/5.28 ($true = $false) | (((in @ sK3 @ sK0)) = $false) | (((in @ sK2 @ sK0)) = $false) | ~spl5_19),
% 34.68/5.28 inference(constrained_superposition,[],[f321,f13827])).
% 34.68/5.28 thf(f13861,plain,(
% 34.68/5.28 (((in @ sK3 @ sK0)) = $false) | (((in @ sK2 @ sK0)) = $false) | ~spl5_19),
% 34.68/5.28 inference(trivial_inequality_removal,[],[f13860])).
% 34.68/5.28 thf(f13864,plain,(
% 34.68/5.28 ($true = $false) | (((in @ sK3 @ sK0)) = $false) | ~spl5_19),
% 34.68/5.28 inference(forward_demodulation,[],[f13861,f36])).
% 34.68/5.28 thf(f13865,plain,(
% 34.68/5.28 (((in @ sK3 @ sK0)) = $false) | ~spl5_19),
% 34.68/5.28 inference(trivial_inequality_removal,[],[f13864])).
% 34.68/5.28 thf(f14123,plain,(
% 34.68/5.28 ($true = $false) | ~spl5_19),
% 34.68/5.28 inference(constrained_superposition,[],[f13865,f37])).
% 34.68/5.28 thf(f14127,plain,(
% 34.68/5.28 $false | ~spl5_19),
% 34.68/5.28 inference(trivial_inequality_removal,[],[f14123])).
% 34.68/5.28 thf(f14128,plain,(
% 34.68/5.28 ~spl5_19),
% 34.68/5.28 inference(avatar_contradiction_clause,[],[f14127])).
% 34.68/5.28 thf(f45394,plain,(
% 34.68/5.28 ($true = $false) | ($false = ((subset @ (setadjoin @ (sK4 @ sK2 @ sK1 @ sK0 @ sK3) @ emptyset) @ sK0))) | (((in @ sK3 @ sK0)) = $false) | (((in @ sK2 @ sK0)) = $false)),
% 34.68/5.28 inference(constrained_superposition,[],[f1514,f847])).
% 34.68/5.28 thf(f45593,plain,(
% 34.68/5.28 ($false = ((subset @ (setadjoin @ (sK4 @ sK2 @ sK1 @ sK0 @ sK3) @ emptyset) @ sK0))) | (((in @ sK3 @ sK0)) = $false) | (((in @ sK2 @ sK0)) = $false)),
% 34.68/5.28 inference(trivial_inequality_removal,[],[f45394])).
% 34.68/5.28 thf(f45698,plain,(
% 34.68/5.28 (((in @ sK3 @ sK0)) = $false) | (((in @ sK2 @ sK0)) = $false) | spl5_19),
% 34.68/5.28 inference(forward_subsumption_resolution,[],[f45593,f13826])).
% 34.68/5.28 thf(f45707,plain,(
% 34.68/5.28 ($true = $false) | (((in @ sK3 @ sK0)) = $false) | spl5_19),
% 34.68/5.28 inference(forward_demodulation,[],[f45698,f36])).
% 34.68/5.28 thf(f45708,plain,(
% 34.68/5.28 (((in @ sK3 @ sK0)) = $false) | spl5_19),
% 34.68/5.28 inference(trivial_inequality_removal,[],[f45707])).
% 34.68/5.28 thf(f45714,definition,(
% 34.68/5.28 spl5_75 <=> (((in @ sK3 @ sK0)) = $false)),
% 34.68/5.28 introduced(definition,[new_symbols(definition,[spl5_75])],[avatar_definition])).
% 34.68/5.28 thf(f45716,plain,(
% 34.68/5.28 (((in @ sK3 @ sK0)) = $false) | ~spl5_75),
% 34.68/5.28 inference(avatar_component_clause,[],[f45714])).
% 34.68/5.28 thf(f45721,plain,(
% 34.68/5.28 spl5_75 | spl5_19),
% 34.68/5.28 inference(avatar_split_clause,[],[f45708,f13825,f45714])).
% 34.68/5.28 thf(f47947,plain,(
% 34.68/5.28 ($true = $false) | ~spl5_75),
% 34.68/5.28 inference(constrained_superposition,[],[f45716,f37])).
% 34.68/5.28 thf(f47951,plain,(
% 34.68/5.28 $false | ~spl5_75),
% 34.68/5.28 inference(trivial_inequality_removal,[],[f47947])).
% 34.68/5.28 thf(f47952,plain,(
% 34.68/5.28 ~spl5_75),
% 34.68/5.28 inference(avatar_contradiction_clause,[],[f47951])).
% 34.68/5.28 cnf(s77, plain, ~spl5_19, inference(sat_conversion,[],[f14128])).
% 34.68/5.28 cnf(s220, plain, spl5_19 | spl5_75, inference(sat_conversion,[],[f45721])).
% 34.68/5.28 cnf(s236, plain, ~spl5_75, inference(sat_conversion,[],[f47952])).
% 34.68/5.28 cnf(s239, plain, spl5_19, inference(rat,[],[s220,s236])).
% 34.68/5.28 cnf(s240, plain, $false, inference(rat,[],[s77,s239])).
% 34.68/5.28 thf(f47954,plain,(
% 34.68/5.28 $false),
% 34.68/5.28 inference(avatar_sat_refutation,[],[s240])).
% 34.68/5.28 % SZS output end Proof for theBenchmark
% 34.68/5.28 % (3590117)------------------------------
% 34.68/5.28 % (3590117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.68/5.28 % (3590117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.68/5.28 % (3590117)CaDiCaL version: 2.1.3
% 34.68/5.28 % (3590117)Termination reason: Refutation
% 34.68/5.28 % (3590117)Time elapsed: 4.858 s
% 34.68/5.28 % (3590117)Peak memory usage: 23 MB
% 34.68/5.28 % (3590117)Instructions burned: 12772 (million)
% 34.68/5.28 % (3590111)Success in time 4.929 s
% 34.68/5.28 % Vampire exiting
%------------------------------------------------------------------------------