%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU505^1 : 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 : n014.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:13 AM UTC 2026
% Result : Theorem 3.97s 1.01s
% Output : Refutation 3.97s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU505^1 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n014.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 13:46:45 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.97/0.95 % (2683239)Will run a generic schedule for satisfiability detection.
% 3.97/0.95 % (2683257)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=392749676:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.97/0.95 % (2683257)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.97/0.95 % (2683254)% WARNING: option uhcvi not known.
% 3.97/0.95 % (2683254)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2708712298:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.97/0.95 % (2683255)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=320237625:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.97/0.95 % (2683253)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2123111889_2999 on theBenchmark for (2999ds/0Mi)
% 3.97/0.95 % (2683256)dis+10_1_sil=32000:sp=arity:random_seed=3935438281:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.97/0.95 % (2683258)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2618122075:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.97/0.95 % (2683260)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1709252173:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.97/0.95 % (2683254)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.97/0.95 % Exception at run slice level
% 3.97/0.95 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.97/0.95 % (2683254)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.97/0.95 % (2683257)Instruction limit reached!
% 3.97/0.95 % (2683257)------------------------------
% 3.97/0.95 % (2683257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/0.95 % (2683257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/0.95 % (2683257)CaDiCaL version: 2.1.3
% 3.97/0.95 % (2683257)Termination reason: Instruction limit
% 3.97/0.95 % (2683257)Termination phase: Saturation
% 3.97/0.95 % (2683257)Time elapsed: 0.030 s
% 3.97/0.95 % (2683257)Peak memory usage: 13 MB
% 3.97/0.95 % (2683257)Instructions burned: 117 (million)
% 3.97/0.95 % (2683278)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2023157495:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.97/0.95 % Exception at run slice level
% 3.97/0.95 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.97/0.95 % (2683285)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=5968570:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.97/0.95 % (2683290)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=3065328454:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 3.97/0.95 % (2683256)Instruction limit reached!
% 3.97/0.95 % (2683256)------------------------------
% 3.97/0.95 % (2683256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/0.95 % (2683256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/0.95 % (2683256)CaDiCaL version: 2.1.3
% 3.97/0.95 % (2683256)Termination reason: Instruction limit
% 3.97/0.95 % (2683256)Termination phase: Saturation
% 3.97/0.95 % (2683256)Time elapsed: 0.051 s
% 3.97/0.95 % (2683256)Peak memory usage: 13 MB
% 3.97/0.95 % (2683256)Instructions burned: 104 (million)
% 3.97/0.95 % (2683290)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.97/0.95 % (2683290)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.97/0.95 % (2683258)Instruction limit reached!
% 3.97/0.95 % (2683258)------------------------------
% 3.97/0.95 % (2683258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/0.95 % (2683258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/0.95 % (2683258)CaDiCaL version: 2.1.3
% 3.97/0.95 % (2683258)Termination reason: Instruction limit
% 3.97/0.95 % (2683258)Termination phase: Saturation
% 3.97/0.95 % (2683258)Time elapsed: 0.065 s
% 3.97/0.95 % (2683258)Peak memory usage: 13 MB
% 3.97/0.95 % (2683258)Instructions burned: 131 (million)
% 3.97/0.95 % (2683285)Instruction limit reached!
% 3.97/0.95 % (2683285)------------------------------
% 3.97/0.95 % (2683285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/1.01 % (2683285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/1.01 % (2683285)CaDiCaL version: 2.1.3
% 3.97/1.01 % (2683285)Termination reason: Instruction limit
% 3.97/1.01 % (2683285)Termination phase: Saturation
% 3.97/1.01 % (2683285)Time elapsed: 0.035 s
% 3.97/1.01 % (2683285)Peak memory usage: 13 MB
% 3.97/1.01 % (2683285)Instructions burned: 134 (million)
% 3.97/1.01 % (2683303)ott-21_1_sil=16000:fs=off:random_seed=12838328:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 3.97/1.01 % (2683311)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=524299555:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 3.97/1.01 % (2683260)Instruction limit reached!
% 3.97/1.01 % (2683260)------------------------------
% 3.97/1.01 % (2683260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/1.01 % (2683260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/1.01 % (2683260)CaDiCaL version: 2.1.3
% 3.97/1.01 % (2683260)Termination reason: Instruction limit
% 3.97/1.01 % (2683260)Termination phase: Saturation
% 3.97/1.01 % (2683260)Time elapsed: 0.080 s
% 3.97/1.01 % (2683260)Peak memory usage: 13 MB
% 3.97/1.01 % (2683260)Instructions burned: 160 (million)
% 3.97/1.01 % Exception at run slice level
% 3.97/1.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.97/1.01 % (2683309)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3119504453:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 3.97/1.01 % (2683320)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3416012883:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 3.97/1.01 % Exception at run slice level
% 3.97/1.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.97/1.01 % (2683319)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=924211198:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 3.97/1.01 % (2683329)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=1111734954:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 3.97/1.01 % (2683329)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.97/1.01 % (2683303)Instruction limit reached!
% 3.97/1.01 % (2683303)------------------------------
% 3.97/1.01 % (2683303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/1.01 % (2683303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/1.01 % (2683303)CaDiCaL version: 2.1.3
% 3.97/1.01 % (2683303)Termination reason: Instruction limit
% 3.97/1.01 % (2683303)Termination phase: Saturation
% 3.97/1.01 % (2683303)Time elapsed: 0.083 s
% 3.97/1.01 % (2683303)Peak memory usage: 12 MB
% 3.97/1.01 % (2683303)Instructions burned: 181 (million)
% 3.97/1.01 % (2683352)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2182202423:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 3.97/1.01 % (2683352)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.97/1.01 % (2683329)Instruction limit reached!
% 3.97/1.01 % (2683329)------------------------------
% 3.97/1.01 % (2683329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/1.01 % (2683329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/1.01 % (2683329)CaDiCaL version: 2.1.3
% 3.97/1.01 % (2683329)Termination reason: Instruction limit
% 3.97/1.01 % (2683329)Termination phase: Saturation
% 3.97/1.01 % (2683329)Time elapsed: 0.205 s
% 3.97/1.01 % (2683329)Peak memory usage: 15 MB
% 3.97/1.01 % (2683329)Instructions burned: 694 (million)
% 3.97/1.01 % (2683309)Instruction limit reached!
% 3.97/1.01 % (2683309)------------------------------
% 3.97/1.01 % (2683309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/1.01 % (2683309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/1.01 % (2683309)CaDiCaL version: 2.1.3
% 3.97/1.01 % (2683309)Termination reason: Instruction limit
% 3.97/1.01 % (2683309)Termination phase: Saturation
% 3.97/1.01 % (2683309)Time elapsed: 0.246 s
% 3.97/1.01 % (2683309)Peak memory usage: 14 MB
% 3.97/1.01 % (2683309)Instructions burned: 477 (million)
% 3.97/1.01 % (2683416)fmb+10_1_sil=64000:random_seed=1777190724:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 3.97/1.01 % (2683416)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 3.97/1.01 % Exception at run slice level
% 3.97/1.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.97/1.01 % (2683424)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1514656162:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi)
% 3.97/1.01 % Exception at run slice level
% 3.97/1.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.97/1.01 % (2683429)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2729090940:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi)
% 3.97/1.01 % Exception at run slice level
% 3.97/1.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.97/1.01 % (2683290)Instruction limit reached!
% 3.97/1.01 % (2683290)------------------------------
% 3.97/1.01 % (2683290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/1.01 % (2683290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/1.01 % (2683290)CaDiCaL version: 2.1.3
% 3.97/1.01 % (2683290)Termination reason: Instruction limit
% 3.97/1.01 % (2683290)Termination phase: Saturation
% 3.97/1.01 % (2683290)Time elapsed: 0.323 s
% 3.97/1.01 % (2683290)Peak memory usage: 15 MB
% 3.97/1.01 % (2683290)Instructions burned: 684 (million)
% 3.97/1.01 % (2683434)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1756309716:i=5131_2996 on theBenchmark for (2996ds/5131Mi)
% 3.97/1.01 % (2683434)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.97/1.01 % (2683437)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3543713997:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 3.97/1.01 % (2683437)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 3.97/1.01 % (2683437)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.97/1.01 % (2683438)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3182644014:i=6324_2995 on theBenchmark for (2995ds/6324Mi)
% 3.97/1.01 % Exception at run slice level
% 3.97/1.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.97/1.01 % (2683442)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2954573567:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi)
% 3.97/1.01 % Exception at run slice level
% 3.97/1.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.97/1.01 % (2683444)ott-2_1_sil=16000:newcnf=on:random_seed=3995216458:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2995 on theBenchmark for (2995ds/869Mi)
% 3.97/1.01 % (2683444)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.97/1.01 % (2683352)Instruction limit reached!
% 3.97/1.01 % (2683352)------------------------------
% 3.97/1.01 % (2683352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/1.01 % (2683352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/1.01 % (2683352)CaDiCaL version: 2.1.3
% 3.97/1.01 % (2683352)Termination reason: Instruction limit
% 3.97/1.01 % (2683352)Termination phase: Saturation
% 3.97/1.01 % (2683352)Time elapsed: 0.445 s
% 3.97/1.01 % (2683352)Peak memory usage: 16 MB
% 3.97/1.01 % (2683352)Instructions burned: 880 (million)
% 3.97/1.01 % (2683446)ott+10_1_sil=32000:tgt=ground:random_seed=3352433868:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi)
% 3.97/1.01 % (2683319)Instruction limit reached!
% 3.97/1.01 % (2683319)------------------------------
% 3.97/1.01 % (2683319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/1.01 % (2683319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/1.01 % (2683319)CaDiCaL version: 2.1.3
% 3.97/1.01 % (2683319)Termination reason: Instruction limit
% 3.97/1.01 % (2683319)Termination phase: Saturation
% 3.97/1.01 % (2683319)Time elapsed: 0.559 s
% 3.97/1.01 % (2683319)Peak memory usage: 17 MB
% 3.97/1.01 % (2683319)Instructions burned: 1179 (million)
% 3.97/1.01 % (2683448)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3779656201:i=54282_2993 on theBenchmark for (2993ds/54282Mi)
% 3.97/1.01 % Exception at run slice level
% 3.97/1.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.97/1.01 % (2683450)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3503204255:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi)
% 3.97/1.01 % (2683450)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.97/1.01 % (2683434) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2683239-2683434"...
% 3.97/1.01 % (2683434)...printing done.
% 3.97/1.01 % (2683434)Refutation found. Thanks to Tanya!
% 3.97/1.01 % SZS status Theorem for theBenchmark
% 3.97/1.01 % SZS output start Proof for theBenchmark
% 3.97/1.01 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 3.97/1.01 thf(func_def_0, type, in: ($i > $i > $o)).
% 3.97/1.01 thf(func_def_1, type, exu: (($i > $o) > $o)).
% 3.97/1.01 thf(func_def_3, type, setextAx: $o).
% 3.97/1.01 thf(func_def_5, type, emptysetAx: $o).
% 3.97/1.01 thf(func_def_6, type, setadjoin: ($i > $i > $i)).
% 3.97/1.01 thf(func_def_7, type, setadjoinAx: $o).
% 3.97/1.01 thf(func_def_8, type, powerset: ($i > $i)).
% 3.97/1.01 thf(func_def_9, type, powersetAx: $o).
% 3.97/1.01 thf(func_def_10, type, setunion: ($i > $i)).
% 3.97/1.01 thf(func_def_11, type, setunionAx: $o).
% 3.97/1.01 thf(func_def_13, type, omega0Ax: $o).
% 3.97/1.01 thf(func_def_14, type, omegaSAx: $o).
% 3.97/1.01 thf(func_def_15, type, omegaIndAx: $o).
% 3.97/1.01 thf(func_def_16, type, replAx: $o).
% 3.97/1.01 thf(func_def_17, type, foundationAx: $o).
% 3.97/1.01 thf(func_def_18, type, wellorderingAx: $o).
% 3.97/1.01 thf(func_def_19, type, descr: (($i > $o) > $i)).
% 3.97/1.01 thf(func_def_20, type, descrp: $o).
% 3.97/1.01 thf(func_def_21, type, dsetconstr: ($i > ($i > $o) > $i)).
% 3.97/1.01 thf(func_def_22, type, dsetconstrI: $o).
% 3.97/1.01 thf(func_def_23, type, dsetconstrEL: $o).
% 3.97/1.01 thf(func_def_24, type, dsetconstrER: $o).
% 3.97/1.01 thf(func_def_25, type, exuE1: $o).
% 3.97/1.01 thf(func_def_26, type, prop2set: ($o > $i)).
% 3.97/1.01 thf(func_def_27, type, prop2setE: $o).
% 3.97/1.01 thf(func_def_28, type, emptysetE: $o).
% 3.97/1.01 thf(func_def_29, type, emptysetimpfalse: $o).
% 3.97/1.01 thf(func_def_30, type, notinemptyset: $o).
% 3.97/1.01 thf(func_def_31, type, exuE3e: $o).
% 3.97/1.01 thf(func_def_32, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 3.97/1.01 thf(func_def_33, type, vAND: ($o > $o > $o)).
% 3.97/1.01 thf(func_def_34, type, db1: !>[X0: $tType]:(X0)).
% 3.97/1.01 thf(func_def_35, type, db0: !>[X0: $tType]:(X0)).
% 3.97/1.01 thf(func_def_36, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 3.97/1.01 thf(func_def_37, type, vIMP: ($o > $o > $o)).
% 3.97/1.01 thf(func_def_38, type, db2: !>[X0: $tType]:(X0)).
% 3.97/1.01 thf(func_def_39, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 3.97/1.01 thf(func_def_40, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 3.97/1.01 thf(func_def_41, type, vIFF: ($o > $o > $o)).
% 3.97/1.01 thf(func_def_42, type, vNOT: ($o > $o)).
% 3.97/1.01 thf(func_def_43, type, vOR: ($o > $o > $o)).
% 3.97/1.01 thf(func_def_44, type, db4: !>[X0: $tType]:(X0)).
% 3.97/1.01 thf(func_def_45, type, db3: !>[X0: $tType]:(X0)).
% 3.97/1.01 thf(func_def_50, type, sK2: (($i > $o) > $i)).
% 3.97/1.01 thf(func_def_51, type, sK3: (($i > $o) > $i > $i)).
% 3.97/1.01 thf(func_def_52, type, sK4: (($i > $o) > $i)).
% 3.97/1.01 thf(func_def_53, type, sK5: (($i > $o) > $i > $i)).
% 3.97/1.01 thf(func_def_54, type, sK6: (($i > $o) > $i > $i)).
% 3.97/1.01 thf(func_def_55, type, sK7: ($i > $i)).
% 3.97/1.01 thf(func_def_56, type, sK8: ($i > $i > $i > $i)).
% 3.97/1.01 thf(func_def_57, type, sK9: ($i > $i > $i)).
% 3.97/1.01 thf(func_def_58, type, sK10: ($i > $i > $i)).
% 3.97/1.01 thf(func_def_59, type, sK11: ($i > $i > $i)).
% 3.97/1.01 thf(func_def_60, type, sK12: ($i > $i)).
% 3.97/1.01 thf(func_def_61, type, sK13: ($i > ($i > $i > $o) > $i)).
% 3.97/1.01 thf(func_def_62, type, sK14: ($i > ($i > $i > $o) > $i)).
% 3.97/1.01 thf(func_def_63, type, sK15: ($i > $i > ($i > $i > $o) > $i)).
% 3.97/1.01 thf(func_def_64, type, sK16: ($i > $i > ($i > $i > $o) > $i)).
% 3.97/1.01 thf(func_def_65, type, sK17: ($i > $i > ($i > $i > $o) > $i)).
% 3.97/1.01 thf(func_def_66, type, sK18: ($i > $i > ($i > $i > $o) > $i)).
% 3.97/1.01 thf(func_def_67, type, sK19: ($i > $i)).
% 3.97/1.01 thf(func_def_68, type, sK20: ($i > $i > $i)).
% 3.97/1.01 thf(func_def_69, type, sK21: ($i > $i > $i)).
% 3.97/1.01 thf(func_def_70, type, sK22: ($i > $i > $i)).
% 3.97/1.01 thf(f2,axiom,(
% 3.97/1.01 (setextAx = ! [X0 : $i,X1 : $i] : (! [X2 : $i] : ((in @ X2 @ X0) <=> (in @ X2 @ X1)) => (X0 = X1)))),
% 3.97/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p',setextAx)).
% 3.97/1.01 thf(f24,conjecture,(
% 3.97/1.01 setextAx => (emptysetAx => (setadjoinAx => (powersetAx => (setunionAx => (omega0Ax => (omegaSAx => (omegaIndAx => (replAx => (foundationAx => (wellorderingAx => (descrp => (dsetconstrI => (dsetconstrEL => (dsetconstrER => (exuE1 => (prop2setE => (emptysetE => (emptysetimpfalse => (notinemptyset => (exuE3e => ! [X0 : $i,X1 : $i] : (! [X2 : $i] : ((in @ X2 @ X0) => (in @ X2 @ X1)) => (! [X2 : $i] : ((in @ X2 @ X1) => (in @ X2 @ X0)) => (X0 = X1)))))))))))))))))))))))),
% 3.97/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p',setext)).
% 3.97/1.01 thf(f25,negated_conjecture,(
% 3.97/1.01 ~(setextAx => (emptysetAx => (setadjoinAx => (powersetAx => (setunionAx => (omega0Ax => (omegaSAx => (omegaIndAx => (replAx => (foundationAx => (wellorderingAx => (descrp => (dsetconstrI => (dsetconstrEL => (dsetconstrER => (exuE1 => (prop2setE => (emptysetE => (emptysetimpfalse => (notinemptyset => (exuE3e => ! [X0 : $i,X1 : $i] : (! [X2 : $i] : ((in @ X2 @ X0) => (in @ X2 @ X1)) => (! [X2 : $i] : ((in @ X2 @ X1) => (in @ X2 @ X0)) => (X0 = X1))))))))))))))))))))))))),
% 3.97/1.01 inference(negated_conjecture,[status(cth)],[f24])).
% 3.97/1.01 thf(f28,plain,(
% 3.97/1.01 (setextAx = ! [X0 : $i,X1 : $i] : (! [X2 : $i] : ((in @ X2 @ X0) <=> (in @ X2 @ X1)) => (X0 = X1)))),
% 3.97/1.01 inference(rectify,[],[f2])).
% 3.97/1.01 thf(f29,plain,(
% 3.97/1.01 (setextAx = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) = (in @ Y2 @ Y0)))) => (Y1 = Y0))))))))),
% 3.97/1.01 inference(fool_elimination,[],[f28])).
% 3.97/1.01 thf(f70,plain,(
% 3.97/1.01 ~(setextAx => (emptysetAx => (setadjoinAx => (powersetAx => (setunionAx => (omega0Ax => (omegaSAx => (omegaIndAx => (replAx => (foundationAx => (wellorderingAx => (descrp => (dsetconstrI => (dsetconstrEL => (dsetconstrER => (exuE1 => (prop2setE => (emptysetE => (emptysetimpfalse => (notinemptyset => (exuE3e => ! [X0 : $i,X1 : $i] : (! [X2 : $i] : ((in @ X2 @ X0) => (in @ X2 @ X1)) => (! [X3 : $i] : ((in @ X3 @ X1) => (in @ X3 @ X0)) => (X0 = X1))))))))))))))))))))))))),
% 3.97/1.01 inference(rectify,[],[f25])).
% 3.97/1.01 thf(f71,plain,(
% 3.97/1.01 ~((setextAx = $true) => ((emptysetAx = $true) => ((setadjoinAx = $true) => ((powersetAx = $true) => ((setunionAx = $true) => ((omega0Ax = $true) => ((omegaSAx = $true) => ((omegaIndAx = $true) => ((replAx = $true) => ((foundationAx = $true) => ((wellorderingAx = $true) => ((descrp = $true) => ((dsetconstrI = $true) => ((dsetconstrEL = $true) => ((dsetconstrER = $true) => ((exuE1 = $true) => ((prop2setE = $true) => ((emptysetE = $true) => ((emptysetimpfalse = $true) => ((notinemptyset = $true) => ((exuE3e = $true) => ! [X0 : $i,X1 : $i] : (! [X2 : $i] : ((((in @ X2 @ X0)) = $true) => (((in @ X2 @ X1)) = $true)) => (! [X3 : $i] : ((((in @ X3 @ X1)) = $true) => (((in @ X3 @ X0)) = $true)) => (X0 = X1))))))))))))))))))))))))),
% 3.97/1.01 inference(fool_elimination,[],[f70])).
% 3.97/1.01 thf(f72,plain,(
% 3.97/1.01 ((((((((((((((((((((? [X0 : $i,X1 : $i] : (((X0 != X1) & ! [X3 : $i] : ((((in @ X3 @ X0)) = $true) | (((in @ X3 @ X1)) != $true))) & ! [X2 : $i] : ((((in @ X2 @ X1)) = $true) | (((in @ X2 @ X0)) != $true))) & (exuE3e = $true)) & (notinemptyset = $true)) & (emptysetimpfalse = $true)) & (emptysetE = $true)) & (prop2setE = $true)) & (exuE1 = $true)) & (dsetconstrER = $true)) & (dsetconstrEL = $true)) & (dsetconstrI = $true)) & (descrp = $true)) & (wellorderingAx = $true)) & (foundationAx = $true)) & (replAx = $true)) & (omegaIndAx = $true)) & (omegaSAx = $true)) & (omega0Ax = $true)) & (setunionAx = $true)) & (powersetAx = $true)) & (setadjoinAx = $true)) & (emptysetAx = $true)) & (setextAx = $true)),
% 3.97/1.01 inference(ennf_transformation,[],[f71])).
% 3.97/1.01 thf(f73,plain,(
% 3.97/1.01 ? [X0 : $i,X1 : $i] : ((X0 != X1) & ! [X3 : $i] : ((((in @ X3 @ X0)) = $true) | (((in @ X3 @ X1)) != $true)) & ! [X2 : $i] : ((((in @ X2 @ X1)) = $true) | (((in @ X2 @ X0)) != $true))) & (exuE3e = $true) & (notinemptyset = $true) & (emptysetimpfalse = $true) & (emptysetE = $true) & (prop2setE = $true) & (exuE1 = $true) & (dsetconstrER = $true) & (dsetconstrEL = $true) & (dsetconstrI = $true) & (descrp = $true) & (wellorderingAx = $true) & (foundationAx = $true) & (replAx = $true) & (omegaIndAx = $true) & (omegaSAx = $true) & (omega0Ax = $true) & (setunionAx = $true) & (powersetAx = $true) & (setadjoinAx = $true) & (emptysetAx = $true) & (setextAx = $true)),
% 3.97/1.01 inference(flattening,[],[f72])).
% 3.97/1.01 thf(f74,plain,(
% 3.97/1.01 ? [X0 : $i,X1 : $i] : ((X0 != X1) & ! [X2 : $i] : ((((in @ X2 @ X0)) = $true) | (((in @ X2 @ X1)) != $true)) & ! [X3 : $i] : ((((in @ X3 @ X1)) = $true) | (((in @ X3 @ X0)) != $true))) & (exuE3e = $true) & (notinemptyset = $true) & (emptysetimpfalse = $true) & (emptysetE = $true) & (prop2setE = $true) & (exuE1 = $true) & (dsetconstrER = $true) & (dsetconstrEL = $true) & (dsetconstrI = $true) & (descrp = $true) & (wellorderingAx = $true) & (foundationAx = $true) & (replAx = $true) & (omegaIndAx = $true) & (omegaSAx = $true) & (omega0Ax = $true) & (setunionAx = $true) & (powersetAx = $true) & (setadjoinAx = $true) & (emptysetAx = $true) & (setextAx = $true)),
% 3.97/1.01 inference(rectify,[],[f73])).
% 3.97/1.01 thf(f75,plain,(
% 3.97/1.01 ((sK0 != sK1) & ! [X2 : $i] : (($true = ((in @ X2 @ sK0))) | ($true != ((in @ X2 @ sK1)))) & ! [X3 : $i] : (($true = ((in @ X3 @ sK1))) | ($true != ((in @ X3 @ sK0))))) & (exuE3e = $true) & (notinemptyset = $true) & (emptysetimpfalse = $true) & (emptysetE = $true) & (prop2setE = $true) & (exuE1 = $true) & (dsetconstrER = $true) & (dsetconstrEL = $true) & (dsetconstrI = $true) & (descrp = $true) & (wellorderingAx = $true) & (foundationAx = $true) & (replAx = $true) & (omegaIndAx = $true) & (omegaSAx = $true) & (omega0Ax = $true) & (setunionAx = $true) & (powersetAx = $true) & (setadjoinAx = $true) & (emptysetAx = $true) & (setextAx = $true)),
% 3.97/1.01 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f74])).
% 3.97/1.01 thf(f77,plain,(
% 3.97/1.01 (setextAx = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) = (in @ Y2 @ Y0)))) => (Y1 = Y0))))))))),
% 3.97/1.01 inference(cnf_transformation,[],[f29])).
% 3.97/1.01 thf(f99,plain,(
% 3.97/1.01 (setextAx = $true)),
% 3.97/1.01 inference(cnf_transformation,[],[f75])).
% 3.97/1.01 thf(f120,plain,(
% 3.97/1.01 ( ! [X3 : $i] : (($true != ((in @ X3 @ sK0))) | ($true = ((in @ X3 @ sK1)))) )),
% 3.97/1.01 inference(cnf_transformation,[],[f75])).
% 3.97/1.01 thf(f121,plain,(
% 3.97/1.01 ( ! [X2 : $i] : (($true != ((in @ X2 @ sK1))) | ($true = ((in @ X2 @ sK0)))) )),
% 3.97/1.01 inference(cnf_transformation,[],[f75])).
% 3.97/1.01 thf(f122,plain,(
% 3.97/1.01 (sK0 != sK1)),
% 3.97/1.01 inference(cnf_transformation,[],[f75])).
% 3.97/1.01 thf(f124,definition,(
% 3.97/1.01 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 3.97/1.01 introduced(theory,[fool_exhaustiveness_axiom])).
% 3.97/1.01 thf(f125,plain,(
% 3.97/1.01 (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) = (in @ Y2 @ Y0)))) => (Y1 = Y0))))))) = $true)),
% 3.97/1.01 inference(definition_unfolding,[],[f77,f99])).
% 3.97/1.01 thf(f446,plain,(
% 3.97/1.01 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) = (in @ Y2 @ Y0)))) => (Y1 = Y0))))) @ X1)))) )),
% 3.97/1.01 inference(pi_proxy_clausification,[],[f125])).
% 3.97/1.01 thf(f447,plain,(
% 3.97/1.01 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ Y0) = (in @ Y1 @ X1)))) => (Y0 = X1))))))) )),
% 3.97/1.01 inference(beta-eta_normalization,[],[f446])).
% 3.97/1.01 thf(f448,plain,(
% 3.97/1.01 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ Y0) = (in @ Y1 @ X1)))) => (Y0 = X1))) @ X2)))) )),
% 3.97/1.01 inference(pi_proxy_clausification,[],[f447])).
% 3.97/1.01 thf(f449,plain,(
% 3.97/1.01 ( ! [X2 : $i,X1 : $i] : (($true = (((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X2) = (in @ Y0 @ X1)))) => (X2 = X1))))) )),
% 3.97/1.01 inference(beta-eta_normalization,[],[f448])).
% 3.97/1.01 thf(f450,plain,(
% 3.97/1.01 ( ! [X2 : $i,X1 : $i] : (($false = ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X2) = (in @ Y0 @ X1)))))) | ($true = ((X2 = X1)))) )),
% 3.97/1.01 inference(imp_proxy_clausification,[],[f449])).
% 3.97/1.01 thf(f451,plain,(
% 3.97/1.01 ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ((in @ Y0 @ X2) = (in @ Y0 @ X1))) @ (sK22 @ X1 @ X2)))) | ($true = ((X2 = X1)))) )),
% 3.97/1.01 inference(sigma_proxy_clausification,[],[f450])).
% 3.97/1.01 thf(f452,plain,(
% 3.97/1.01 ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ((in @ Y0 @ X2) = (in @ Y0 @ X1))) @ (sK22 @ X1 @ X2)))) | (X1 = X2)) )),
% 3.97/1.01 inference(equality_proxy_clausification,[],[f451])).
% 3.97/1.01 thf(f453,plain,(
% 3.97/1.01 ( ! [X2 : $i,X1 : $i] : (($false = (((in @ (sK22 @ X1 @ X2) @ X2) = (in @ (sK22 @ X1 @ X2) @ X1)))) | (X1 = X2)) )),
% 3.97/1.01 inference(beta-eta_normalization,[],[f452])).
% 3.97/1.01 thf(f454,plain,(
% 3.97/1.01 ( ! [X2 : $i,X1 : $i] : ((((in @ (sK22 @ X1 @ X2) @ X2)) != ((in @ (sK22 @ X1 @ X2) @ X1))) | (X1 = X2)) )),
% 3.97/1.01 inference(iff_proxy_clausification,[],[f453])).
% 3.97/1.01 thf(f455,plain,(
% 3.97/1.01 ( ! [X2 : $i,X1 : $i] : (($true = ((in @ (sK22 @ X1 @ X2) @ X2))) | ($true = ((in @ (sK22 @ X1 @ X2) @ X1))) | (X1 = X2)) )),
% 3.97/1.01 inference(xor_proxy_clausification,[],[f454])).
% 3.97/1.01 thf(f456,plain,(
% 3.97/1.01 ( ! [X2 : $i,X1 : $i] : (($false = ((in @ (sK22 @ X1 @ X2) @ X2))) | ($false = ((in @ (sK22 @ X1 @ X2) @ X1))) | (X1 = X2)) )),
% 3.97/1.01 inference(xor_proxy_clausification,[],[f454])).
% 3.97/1.01 thf(f540,plain,(
% 3.97/1.01 ( ! [X0 : $i] : (($true != $true) | ($true = ((in @ X0 @ sK0))) | ($false = ((in @ X0 @ sK1)))) )),
% 3.97/1.01 inference(constrained_superposition,[],[f121,f124])).
% 3.97/1.01 thf(f542,plain,(
% 3.97/1.01 ( ! [X0 : $i] : (($false = ((in @ X0 @ sK1))) | ($true = ((in @ X0 @ sK0)))) )),
% 3.97/1.01 inference(trivial_inequality_removal,[],[f540])).
% 3.97/1.01 thf(f1245,plain,(
% 3.97/1.01 ( ! [X0 : $i] : (($true != $true) | ($true = ((in @ (sK22 @ sK0 @ X0) @ sK1))) | ($true = ((in @ (sK22 @ sK0 @ X0) @ X0))) | (sK0 = X0)) )),
% 3.97/1.01 inference(constrained_superposition,[],[f120,f455])).
% 3.97/1.01 thf(f1252,plain,(
% 3.97/1.01 ( ! [X0 : $i] : (($true = ((in @ (sK22 @ sK0 @ X0) @ sK1))) | ($true = ((in @ (sK22 @ sK0 @ X0) @ X0))) | (sK0 = X0)) )),
% 3.97/1.01 inference(trivial_inequality_removal,[],[f1245])).
% 3.97/1.01 thf(f6343,plain,(
% 3.97/1.01 ($false = $true) | ($false = $true) | (sK0 = sK1) | ($false = ((in @ (sK22 @ sK0 @ sK1) @ sK0))) | (sK0 = sK1)),
% 3.97/1.01 inference(constrained_superposition,[],[f1252,f456])).
% 3.97/1.01 thf(f6374,plain,(
% 3.97/1.01 ($false = $true) | ($false = $true) | (sK0 = sK1) | ($true = ((in @ (sK22 @ sK0 @ sK1) @ sK0)))),
% 3.97/1.01 inference(constrained_superposition,[],[f1252,f542])).
% 3.97/1.01 thf(f6492,plain,(
% 3.97/1.01 ($false = $true) | (sK0 = sK1) | ($true = ((in @ (sK22 @ sK0 @ sK1) @ sK0)))),
% 3.97/1.01 inference(duplicate_literal_removal,[],[f6374])).
% 3.97/1.01 thf(f6493,plain,(
% 3.97/1.01 (sK0 = sK1) | ($true = ((in @ (sK22 @ sK0 @ sK1) @ sK0)))),
% 3.97/1.01 inference(trivial_inequality_removal,[],[f6492])).
% 3.97/1.01 thf(f6527,plain,(
% 3.97/1.01 ($false = $true) | (sK0 = sK1) | ($false = ((in @ (sK22 @ sK0 @ sK1) @ sK0)))),
% 3.97/1.01 inference(duplicate_literal_removal,[],[f6343])).
% 3.97/1.01 thf(f6528,plain,(
% 3.97/1.01 (sK0 = sK1) | ($false = ((in @ (sK22 @ sK0 @ sK1) @ sK0)))),
% 3.97/1.01 inference(trivial_inequality_removal,[],[f6527])).
% 3.97/1.01 thf(f6544,plain,(
% 3.97/1.01 ($true = ((in @ (sK22 @ sK0 @ sK1) @ sK0)))),
% 3.97/1.01 inference(forward_subsumption_resolution,[],[f6493,f122])).
% 3.97/1.01 thf(f6547,plain,(
% 3.97/1.01 ($false = ((in @ (sK22 @ sK0 @ sK1) @ sK0)))),
% 3.97/1.01 inference(forward_subsumption_resolution,[],[f6528,f122])).
% 3.97/1.01 thf(f7134,plain,(
% 3.97/1.01 ($false = $true)),
% 3.97/1.01 inference(constrained_superposition,[],[f6544,f6547])).
% 3.97/1.01 thf(f7156,plain,(
% 3.97/1.01 $false),
% 3.97/1.01 inference(trivial_inequality_removal,[],[f7134])).
% 3.97/1.01 % SZS output end Proof for theBenchmark
% 3.97/1.01 % (2683434)------------------------------
% 3.97/1.01 % (2683434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.97/1.01 % (2683434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.97/1.01 % (2683434)CaDiCaL version: 2.1.3
% 3.97/1.01 % (2683434)Termination reason: Refutation
% 3.97/1.01 % (2683434)Time elapsed: 0.365 s
% 3.97/1.01 % (2683434)Peak memory usage: 15 MB
% 3.97/1.01 % (2683434)Instructions burned: 791 (million)
% 3.97/1.01 % (2683239)Success in time 0.78 s
% 3.97/1.01 % Vampire exiting
%------------------------------------------------------------------------------