%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM809^5 : TPTP v9.3.1. Bugfixed v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n004.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:19:35 AM UTC 2026
% Result : Theorem 10.05s 1.83s
% Output : Refutation 10.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM809^5 : TPTP v9.3.1. Bugfixed v5.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.21 % Computer : n004.cluster.edu
% 0.10/0.21 % Model : x86_64 x86_64
% 0.10/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.21 % Memory : 8046.5625MB
% 0.10/0.21 % OS : Linux 6.8.0-71-generic
% 0.10/0.21 % CPULimit : 300
% 0.10/0.21 % WCLimit : 300
% 0.10/0.21 % DateTime : Tue Sep 29 13:01:07 UTC 2026
% 0.10/0.21 % CPUTime :
% 0.10/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.25 Running first-order model finding
% 0.10/0.25 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.10/0.98 % (1242216)Will run a generic schedule for satisfiability detection.
% 4.10/0.98 % (1242223)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=730656920:i=88024:add=on:rawr=on_3000 on theBenchmark for (3000ds/88024Mi)
% 4.10/0.98 % (1242222)% WARNING: option uhcvi not known.
% 4.10/0.98 % (1242221)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=581804489_3000 on theBenchmark for (3000ds/0Mi)
% 4.10/0.98 % (1242222)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1857463789:i=135531:add=off:rawr=on_3000 on theBenchmark for (3000ds/135531Mi)
% 4.10/0.98 % (1242224)dis+10_1_sil=32000:sp=arity:random_seed=3772499876:i=103:fgj=on_3000 on theBenchmark for (3000ds/103Mi)
% 4.10/0.98 % (1242227)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=129967420:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_3000 on theBenchmark for (3000ds/159Mi)
% 4.10/0.98 % (1242225)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=889800797:i=116_3000 on theBenchmark for (3000ds/116Mi)
% 4.10/0.98 % Exception at run slice level
% 4.10/0.98 User error: % (1242222)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.10/0.98 Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.10/0.98 % (1242226)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=916053873:i=131_3000 on theBenchmark for (3000ds/131Mi)
% 4.10/0.98 % (1242225)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.10/0.98 % (1242222)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.10/0.98 % (1242235)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3192286367:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.10/0.98 % Exception at run slice level
% 4.10/0.98 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.10/0.98 % (1242224)Instruction limit reached!
% 4.10/0.98 % (1242224)------------------------------
% 4.10/0.98 % (1242224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.10/0.98 % (1242224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.10/0.98 % (1242224)CaDiCaL version: 2.1.3
% 4.10/0.98 % (1242224)Termination reason: Instruction limit
% 4.10/0.98 % (1242224)Termination phase: Saturation
% 4.10/0.98 % (1242224)Time elapsed: 0.051 s
% 4.10/0.98 % (1242224)Peak memory usage: 12 MB
% 4.10/0.98 % (1242224)Instructions burned: 103 (million)
% 4.10/0.98 % (1242237)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2721262881:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.10/0.98 % (1242225)Instruction limit reached!
% 4.10/0.98 % (1242225)------------------------------
% 4.10/0.98 % (1242225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.10/0.98 % (1242225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.10/0.98 % (1242225)CaDiCaL version: 2.1.3
% 4.10/0.98 % (1242225)Termination reason: Instruction limit
% 4.10/0.98 % (1242225)Termination phase: Saturation
% 4.10/0.98 % (1242225)Time elapsed: 0.057 s
% 4.10/0.98 % (1242225)Peak memory usage: 12 MB
% 4.10/0.98 % (1242225)Instructions burned: 117 (million)
% 4.10/0.98 % (1242226)Instruction limit reached!
% 4.10/0.98 % (1242226)------------------------------
% 4.10/0.98 % (1242226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.10/0.98 % (1242226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.10/0.98 % (1242226)CaDiCaL version: 2.1.3
% 4.10/0.98 % (1242226)Termination reason: Instruction limit
% 4.10/0.98 % (1242226)Termination phase: Saturation
% 4.10/0.98 % (1242226)Time elapsed: 0.066 s
% 4.10/0.98 % (1242226)Peak memory usage: 12 MB
% 4.10/0.98 % (1242226)Instructions burned: 133 (million)
% 4.10/0.98 % (1242246)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=2095921758:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.10/0.98 % (1242246)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.10/0.98 % (1242246)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.10/0.98 % (1242249)ott-21_1_sil=16000:fs=off:random_seed=454251402:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 4.10/0.98 % (1242227)Instruction limit reached!
% 10.05/1.83 % (1242227)------------------------------
% 10.05/1.83 % (1242227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.05/1.83 % (1242227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/1.83 % (1242227)CaDiCaL version: 2.1.3
% 10.05/1.83 % (1242227)Termination reason: Instruction limit
% 10.05/1.83 % (1242227)Termination phase: Saturation
% 10.05/1.83 % (1242227)Time elapsed: 0.085 s
% 10.05/1.83 % (1242227)Peak memory usage: 12 MB
% 10.05/1.83 % (1242227)Instructions burned: 159 (million)
% 10.05/1.83 % (1242254)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1437593532:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 10.05/1.83 % (1242266)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=414764087:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 10.05/1.83 % Exception at run slice level
% 10.05/1.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 10.05/1.83 % (1242237)Instruction limit reached!
% 10.05/1.83 % (1242237)------------------------------
% 10.05/1.83 % (1242237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.05/1.83 % (1242237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/1.83 % (1242237)CaDiCaL version: 2.1.3
% 10.05/1.83 % (1242237)Termination reason: Instruction limit
% 10.05/1.83 % (1242237)Termination phase: Saturation
% 10.05/1.83 % (1242237)Time elapsed: 0.068 s
% 10.05/1.83 % (1242237)Peak memory usage: 12 MB
% 10.05/1.83 % (1242237)Instructions burned: 131 (million)
% 10.05/1.83 % (1242275)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3267681635:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 10.05/1.83 % (1242287)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2757809582:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 10.05/1.83 % Exception at run slice level
% 10.05/1.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 10.05/1.83 % (1242293)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=610999327: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)
% 10.05/1.83 % (1242293)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 10.05/1.83 % (1242249)Instruction limit reached!
% 10.05/1.83 % (1242249)------------------------------
% 10.05/1.83 % (1242249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.05/1.83 % (1242249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/1.83 % (1242249)CaDiCaL version: 2.1.3
% 10.05/1.83 % (1242249)Termination reason: Instruction limit
% 10.05/1.83 % (1242249)Termination phase: Saturation
% 10.05/1.83 % (1242249)Time elapsed: 0.085 s
% 10.05/1.83 % (1242249)Peak memory usage: 12 MB
% 10.05/1.83 % (1242249)Instructions burned: 181 (million)
% 10.05/1.83 % (1242304)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2097729724:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 10.05/1.83 % (1242304)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 10.05/1.83 % (1242254)Instruction limit reached!
% 10.05/1.83 % (1242254)------------------------------
% 10.05/1.83 % (1242254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.05/1.83 % (1242254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/1.83 % (1242254)CaDiCaL version: 2.1.3
% 10.05/1.83 % (1242254)Termination reason: Instruction limit
% 10.05/1.83 % (1242254)Termination phase: Saturation
% 10.05/1.83 % (1242254)Time elapsed: 0.239 s
% 10.05/1.83 % (1242254)Peak memory usage: 13 MB
% 10.05/1.83 % (1242254)Instructions burned: 479 (million)
% 10.05/1.83 % (1242359)fmb+10_1_sil=64000:random_seed=1270826662:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 10.05/1.83 % (1242359)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 10.05/1.83 % Exception at run slice level
% 10.05/1.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 10.05/1.83 % (1242362)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2425853778:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi)
% 10.05/1.83 % Exception at run slice level
% 10.05/1.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 10.05/1.83 % (1242364)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1756903791:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi)
% 10.05/1.83 % Exception at run slice level
% 10.05/1.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 10.05/1.83 % (1242246)Instruction limit reached!
% 10.05/1.83 % (1242246)------------------------------
% 10.05/1.83 % (1242246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.05/1.83 % (1242246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/1.83 % (1242246)CaDiCaL version: 2.1.3
% 10.05/1.83 % (1242246)Termination reason: Instruction limit
% 10.05/1.83 % (1242246)Termination phase: Saturation
% 10.05/1.83 % (1242246)Time elapsed: 0.318 s
% 10.05/1.83 % (1242246)Peak memory usage: 14 MB
% 10.05/1.83 % (1242246)Instructions burned: 685 (million)
% 10.05/1.83 % (1242366)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2013808734:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 10.05/1.83 % (1242366)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 10.05/1.83 % (1242367)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4289324002:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 10.05/1.83 % (1242367)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 10.05/1.83 % (1242367)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 10.05/1.83 % (1242293)Instruction limit reached!
% 10.05/1.83 % (1242293)------------------------------
% 10.05/1.83 % (1242293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.05/1.83 % (1242293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/1.83 % (1242293)CaDiCaL version: 2.1.3
% 10.05/1.83 % (1242293)Termination reason: Instruction limit
% 10.05/1.83 % (1242293)Termination phase: Saturation
% 10.05/1.83 % (1242293)Time elapsed: 0.282 s
% 10.05/1.83 % (1242293)Peak memory usage: 13 MB
% 10.05/1.83 % (1242293)Instructions burned: 694 (million)
% 10.05/1.83 % (1242374)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=185491292:i=6324_2995 on theBenchmark for (2995ds/6324Mi)
% 10.05/1.83 % Exception at run slice level
% 10.05/1.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 10.05/1.83 % (1242378)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1435399161:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi)
% 10.05/1.83 % Exception at run slice level
% 10.05/1.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 10.05/1.83 % (1242388)ott-2_1_sil=16000:newcnf=on:random_seed=161788143:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi)
% 10.05/1.83 % (1242388)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 10.05/1.83 % (1242304)Instruction limit reached!
% 10.05/1.83 % (1242304)------------------------------
% 10.05/1.83 % (1242304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.05/1.83 % (1242304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/1.83 % (1242304)CaDiCaL version: 2.1.3
% 10.05/1.83 % (1242304)Termination reason: Instruction limit
% 10.05/1.83 % (1242304)Termination phase: Saturation
% 10.05/1.83 % (1242304)Time elapsed: 0.434 s
% 10.05/1.83 % (1242304)Peak memory usage: 15 MB
% 10.05/1.83 % (1242304)Instructions burned: 881 (million)
% 10.05/1.83 % (1242423)ott+10_1_sil=32000:tgt=ground:random_seed=3503661865:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi)
% 10.05/1.83 % (1242275)Instruction limit reached!
% 10.05/1.83 % (1242275)------------------------------
% 10.05/1.83 % (1242275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.05/1.83 % (1242275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/1.83 % (1242275)CaDiCaL version: 2.1.3
% 10.05/1.83 % (1242275)Termination reason: Instruction limit
% 10.05/1.83 % (1242275)Termination phase: Saturation
% 10.05/1.83 % (1242275)Time elapsed: 0.561 s
% 10.05/1.83 % (1242275)Peak memory usage: 16 MB
% 10.05/1.83 % (1242275)Instructions burned: 1179 (million)
% 10.05/1.83 % (1242425)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=331444906:i=54282_2992 on theBenchmark for (2992ds/54282Mi)
% 10.05/1.83 % Exception at run slice level
% 10.05/1.83 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 10.05/1.83 % (1242427)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3490457477:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi)
% 10.05/1.83 % (1242427)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 10.05/1.83 % (1242388)Instruction limit reached!
% 10.05/1.83 % (1242388)------------------------------
% 10.05/1.83 % (1242388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.05/1.83 % (1242388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/1.83 % (1242388)CaDiCaL version: 2.1.3
% 10.05/1.83 % (1242388)Termination reason: Instruction limit
% 10.05/1.83 % (1242388)Termination phase: Saturation
% 10.05/1.83 % (1242388)Time elapsed: 0.377 s
% 10.05/1.83 % (1242388)Peak memory usage: 14 MB
% 10.05/1.83 % (1242388)Instructions burned: 871 (million)
% 10.05/1.83 % (1242429)dis+21_1_sil=32000:sas=cadical:random_seed=191282066:i=3773:amm=off_2991 on theBenchmark for (2991ds/3773Mi)
% 10.05/1.83 % (1242367)Instruction limit reached!
% 10.05/1.83 % (1242367)------------------------------
% 10.05/1.83 % (1242367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.05/1.83 % (1242367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/1.83 % (1242367)CaDiCaL version: 2.1.3
% 10.05/1.83 % (1242367)Termination reason: Instruction limit
% 10.05/1.83 % (1242367)Termination phase: Saturation
% 10.05/1.83 % (1242367)Time elapsed: 0.758 s
% 10.05/1.83 % (1242367)Peak memory usage: 20 MB
% 10.05/1.83 % (1242367)Instructions burned: 1472 (million)
% 10.05/1.83 % (1242431)ott+11_1_sil=16000:gs=on:random_seed=2286786837:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi)
% 10.05/1.83 % (1242431)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 10.05/1.83 % (1242429) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1242216-1242429"...
% 10.05/1.83 % (1242429)...printing done.
% 10.05/1.83 % (1242429)Refutation found. Thanks to Tanya!
% 10.05/1.83 % SZS status Theorem for theBenchmark
% 10.05/1.83 % SZS output start Proof for theBenchmark
% 10.05/1.83 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 10.05/1.83 thf(func_def_1, type, cS: ($i > $i)).
% 10.05/1.83 thf(func_def_2, type, r: ($i > $i > $o)).
% 10.05/1.83 thf(func_def_3, type, cIND: $o).
% 10.05/1.83 thf(func_def_5, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 10.05/1.83 thf(func_def_6, type, vIMP: ($o > $o > $o)).
% 10.05/1.83 thf(func_def_7, type, vAND: ($o > $o > $o)).
% 10.05/1.83 thf(func_def_8, type, db0: !>[X0: $tType]:(X0)).
% 10.05/1.83 thf(func_def_9, type, db1: !>[X0: $tType]:(X0)).
% 10.05/1.83 thf(func_def_10, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 10.05/1.83 thf(func_def_14, type, vNOT: ($o > $o)).
% 10.05/1.83 thf(func_def_15, type, sK1: (($i > $o) > $i)).
% 10.05/1.83 thf(func_def_16, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 10.05/1.83 thf(func_def_18, type, sK3: ($i > $i)).
% 10.05/1.83 thf(func_def_19, type, sK4: ($i > $i)).
% 10.05/1.83 thf(func_def_20, type, sK5: ($i > $i)).
% 10.05/1.83 thf(func_def_22, type, sK7: ($i > $i)).
% 10.05/1.83 thf(func_def_23, type, sK8: ($i > $i)).
% 10.05/1.83 thf(func_def_24, type, sK9: ($i > $i)).
% 10.05/1.83 thf(func_def_25, type, sK10: ($i > $i)).
% 10.05/1.83 thf(func_def_26, type, sK11: ($i > $i)).
% 10.05/1.83 thf(func_def_27, type, sK12: (($i > $i) > ($i > $o) > $i)).
% 10.05/1.83 thf(func_def_29, type, sK14: (($i > $i) > ($i > $o) > $i)).
% 10.05/1.83 thf(func_def_30, type, sK15: ($i > $i)).
% 10.05/1.83 thf(func_def_31, type, sK16: ($i > $i)).
% 10.05/1.83 thf(func_def_32, type, sK17: ($i > ($i > $i > $o) > $i)).
% 10.05/1.83 thf(func_def_33, type, db2: !>[X0: $tType]:(X0)).
% 10.05/1.83 thf(func_def_34, type, sK18: (($i > $i) > $i > ($i > $i > $o) > $i)).
% 10.05/1.83 thf(func_def_36, type, sK20: (($i > $i > $i) > ($i > $i > $i) > $i)).
% 10.05/1.83 thf(func_def_37, type, sK21: (($i > $i > $i) > ($i > $i > $i) > $i)).
% 10.05/1.83 thf(func_def_38, type, sK22: (($i > $i) > ($i > $i > $i) > ($i > $i > $i) > $i)).
% 10.05/1.83 thf(f1,axiom,(
% 10.05/1.83 (cIND = ! [X0 : ($i > $o)] : ((! [X1 : $i] : ((X0 @ X1) => (X0 @ (cS @ X1))) & (X0 @ c0)) => ! [X1 : $i] : (X0 @ X1)))),
% 10.05/1.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cIND_def)).
% 10.05/1.83 thf(f2,conjecture,(
% 10.05/1.83 (! [X0 : $i,X1 : $i] : ((r @ X0 @ X1) => (r @ (cS @ X0) @ (cS @ X1))) & (r @ c0 @ c0) & cIND) => ! [X0 : $i] : ? [X1 : $i] : (r @ X0 @ X1)),
% 10.05/1.83 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cTHM130)).
% 10.05/1.83 thf(f3,negated_conjecture,(
% 10.05/1.83 ~((! [X0 : $i,X1 : $i] : ((r @ X0 @ X1) => (r @ (cS @ X0) @ (cS @ X1))) & (r @ c0 @ c0) & cIND) => ! [X0 : $i] : ? [X1 : $i] : (r @ X0 @ X1))),
% 10.05/1.83 inference(negated_conjecture,[status(cth)],[f2])).
% 10.05/1.83 thf(f4,plain,(
% 10.05/1.83 (cIND = ! [X0 : ($i > $o)] : ((! [X1 : $i] : ((X0 @ X1) => (X0 @ (cS @ X1))) & (X0 @ c0)) => ! [X2 : $i] : (X0 @ X2)))),
% 10.05/1.83 inference(rectify,[],[f1])).
% 10.05/1.83 thf(f5,plain,(
% 10.05/1.83 (cIND = ((!! @ ($i > $o) @ (^[Y0 : $i > $o]: (((Y0 @ c0) & (!! @ $i @ (^[Y1 : $i]: ((Y0 @ Y1) => (Y0 @ (cS @ Y1)))))) => (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))))))),
% 10.05/1.83 inference(fool_elimination,[],[f4])).
% 10.05/1.83 thf(f6,plain,(
% 10.05/1.83 ~((! [X0 : $i,X1 : $i] : ((r @ X0 @ X1) => (r @ (cS @ X0) @ (cS @ X1))) & (r @ c0 @ c0) & cIND) => ! [X2 : $i] : ? [X3 : $i] : (r @ X2 @ X3))),
% 10.05/1.83 inference(rectify,[],[f3])).
% 10.05/1.83 thf(f7,plain,(
% 10.05/1.83 ~((! [X0 : $i,X1 : $i] : ((((r @ X0 @ X1)) = $true) => (((r @ (cS @ X0) @ (cS @ X1))) = $true)) & (((r @ c0 @ c0)) = $true) & (cIND = $true)) => ! [X2 : $i] : ? [X3 : $i] : (((r @ X2 @ X3)) = $true))),
% 10.05/1.83 inference(fool_elimination,[],[f6])).
% 10.05/1.83 thf(f8,plain,(
% 10.05/1.83 ? [X2 : $i] : ! [X3 : $i] : (((r @ X2 @ X3)) != $true) & (! [X0 : $i,X1 : $i] : ((((r @ (cS @ X0) @ (cS @ X1))) = $true) | (((r @ X0 @ X1)) != $true)) & (((r @ c0 @ c0)) = $true) & (cIND = $true))),
% 10.05/1.83 inference(ennf_transformation,[],[f7])).
% 10.05/1.83 thf(f9,plain,(
% 10.05/1.83 ? [X2 : $i] : ! [X3 : $i] : (((r @ X2 @ X3)) != $true) & ! [X0 : $i,X1 : $i] : ((((r @ (cS @ X0) @ (cS @ X1))) = $true) | (((r @ X0 @ X1)) != $true)) & (((r @ c0 @ c0)) = $true) & (cIND = $true)),
% 10.05/1.83 inference(flattening,[],[f8])).
% 10.05/1.83 thf(f10,plain,(
% 10.05/1.83 ? [X0 : $i] : ! [X1 : $i] : (((r @ X0 @ X1)) != $true) & ! [X2 : $i,X3 : $i] : (($true = ((r @ (cS @ X2) @ (cS @ X3)))) | (((r @ X2 @ X3)) != $true)) & (((r @ c0 @ c0)) = $true) & (cIND = $true)),
% 10.05/1.83 inference(rectify,[],[f9])).
% 10.05/1.83 thf(f11,plain,(
% 10.05/1.83 ! [X1 : $i] : ($true != ((r @ sK0 @ X1))) & ! [X2 : $i,X3 : $i] : (($true = ((r @ (cS @ X2) @ (cS @ X3)))) | (((r @ X2 @ X3)) != $true)) & (((r @ c0 @ c0)) = $true) & (cIND = $true)),
% 10.05/1.83 inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0)],[f10])).
% 10.05/1.83 thf(f12,plain,(
% 10.05/1.83 (cIND = ((!! @ ($i > $o) @ (^[Y0 : $i > $o]: (((Y0 @ c0) & (!! @ $i @ (^[Y1 : $i]: ((Y0 @ Y1) => (Y0 @ (cS @ Y1)))))) => (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))))))),
% 10.05/1.83 inference(cnf_transformation,[],[f5])).
% 10.05/1.83 thf(f13,plain,(
% 10.05/1.83 (cIND = $true)),
% 10.05/1.83 inference(cnf_transformation,[],[f11])).
% 10.05/1.83 thf(f14,plain,(
% 10.05/1.83 (((r @ c0 @ c0)) = $true)),
% 10.05/1.83 inference(cnf_transformation,[],[f11])).
% 10.05/1.83 thf(f15,plain,(
% 10.05/1.83 ( ! [X2 : $i,X3 : $i] : (($true = ((r @ (cS @ X2) @ (cS @ X3)))) | (((r @ X2 @ X3)) != $true)) )),
% 10.05/1.83 inference(cnf_transformation,[],[f11])).
% 10.05/1.83 thf(f16,plain,(
% 10.05/1.83 ( ! [X1 : $i] : (($true != ((r @ sK0 @ X1)))) )),
% 10.05/1.83 inference(cnf_transformation,[],[f11])).
% 10.05/1.83 thf(f18,definition,(
% 10.05/1.83 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 10.05/1.83 introduced(theory,[fool_exhaustiveness_axiom])).
% 10.05/1.83 thf(f19,plain,(
% 10.05/1.83 (((!! @ ($i > $o) @ (^[Y0 : $i > $o]: (((Y0 @ c0) & (!! @ $i @ (^[Y1 : $i]: ((Y0 @ Y1) => (Y0 @ (cS @ Y1)))))) => (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))))) = $true)),
% 10.05/1.83 inference(definition_unfolding,[],[f12,f13])).
% 10.05/1.83 thf(f20,plain,(
% 10.05/1.83 ( ! [X1 : ($i > $o)] : (($true = (((^[Y0 : $i > $o]: (((Y0 @ c0) & (!! @ $i @ (^[Y1 : $i]: ((Y0 @ Y1) => (Y0 @ (cS @ Y1)))))) => (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1))))) @ X1)))) )),
% 10.05/1.83 inference(pi_proxy_clausification,[],[f19])).
% 10.05/1.83 thf(f21,plain,(
% 10.05/1.83 ( ! [X1 : ($i > $o)] : (($true = ((((X1 @ c0) & (!! @ $i @ (^[Y0 : $i]: ((X1 @ Y0) => (X1 @ (cS @ Y0)))))) => (!! @ $i @ X1))))) )),
% 10.05/1.83 inference(beta-eta_normalization,[],[f20])).
% 10.05/1.83 thf(f22,plain,(
% 10.05/1.83 ( ! [X1 : ($i > $o)] : (($false = (((X1 @ c0) & (!! @ $i @ (^[Y0 : $i]: ((X1 @ Y0) => (X1 @ (cS @ Y0)))))))) | ($true = ((!! @ $i @ X1)))) )),
% 10.05/1.83 inference(imp_proxy_clausification,[],[f21])).
% 10.05/1.83 thf(f23,plain,(
% 10.05/1.83 ( ! [X1 : ($i > $o)] : (($false = ((!! @ $i @ (^[Y0 : $i]: ((X1 @ Y0) => (X1 @ (cS @ Y0))))))) | ($true = ((!! @ $i @ X1))) | ($false = ((X1 @ c0)))) )),
% 10.05/1.83 inference(and_proxy_clausification,[],[f22])).
% 10.05/1.83 thf(f24,plain,(
% 10.05/1.83 ( ! [X1 : ($i > $o)] : (($false = (((^[Y0 : $i]: ((X1 @ Y0) => (X1 @ (cS @ Y0)))) @ (sK1 @ X1)))) | ($true = ((!! @ $i @ X1))) | ($false = ((X1 @ c0)))) )),
% 10.05/1.83 inference(sigma_proxy_clausification,[],[f23])).
% 10.05/1.83 thf(f25,plain,(
% 10.05/1.83 ( ! [X2 : $i,X1 : ($i > $o)] : (($false = (((^[Y0 : $i]: ((X1 @ Y0) => (X1 @ (cS @ Y0)))) @ (sK1 @ X1)))) | ($true = ((X1 @ X2))) | ($false = ((X1 @ c0)))) )),
% 10.05/1.83 inference(pi_proxy_clausification,[],[f24])).
% 10.05/1.83 thf(f26,plain,(
% 10.05/1.83 ( ! [X2 : $i,X1 : ($i > $o)] : (($false = (((X1 @ (sK1 @ X1)) => (X1 @ (cS @ (sK1 @ X1)))))) | ($true = ((X1 @ X2))) | ($false = ((X1 @ c0)))) )),
% 10.05/1.83 inference(beta-eta_normalization,[],[f25])).
% 10.05/1.83 thf(f27,plain,(
% 10.05/1.83 ( ! [X2 : $i,X1 : ($i > $o)] : (($false = ((X1 @ (cS @ (sK1 @ X1))))) | ($true = ((X1 @ X2))) | ($false = ((X1 @ c0)))) )),
% 10.05/1.83 inference(imp_proxy_clausification,[],[f26])).
% 10.05/1.83 thf(f28,plain,(
% 10.05/1.83 ( ! [X2 : $i,X1 : ($i > $o)] : (($true = ((X1 @ (sK1 @ X1)))) | ($true = ((X1 @ X2))) | ($false = ((X1 @ c0)))) )),
% 10.05/1.83 inference(imp_proxy_clausification,[],[f26])).
% 10.05/1.83 thf(f37,plain,(
% 10.05/1.83 ( ! [X2 : $i,X0 : $i,X1 : ($i > $i)] : (($true != $true) | ($true = (((^[Y0 : $i]: (r @ ((^[Y1 : $i]: (Y1)) @ Y0) @ (X1 @ Y0))) @ (sK1 @ (^[Y0 : $i]: (r @ ((^[Y1 : $i]: (Y1)) @ Y0) @ (X1 @ Y0))))))) | ($false = (((^[Y0 : $i]: (r @ ((^[Y1 : $i]: (Y1)) @ Y0) @ (X1 @ Y0))) @ c0))) | (sK0 != X2) | (((X1 @ X2)) != X0)) )),
% 10.05/1.83 inference(constrained_superposition,[],[f16,f28])).
% 10.05/1.83 thf(f65,plain,(
% 10.05/1.83 ( ! [X2 : $i,X0 : $i,X1 : ($i > $i)] : (($true = (((^[Y0 : $i]: (r @ ((^[Y1 : $i]: (Y1)) @ Y0) @ (X1 @ Y0))) @ (sK1 @ (^[Y0 : $i]: (r @ ((^[Y1 : $i]: (Y1)) @ Y0) @ (X1 @ Y0))))))) | ($false = (((^[Y0 : $i]: (r @ ((^[Y1 : $i]: (Y1)) @ Y0) @ (X1 @ Y0))) @ c0))) | (sK0 != X2) | (((X1 @ X2)) != X0)) )),
% 10.05/1.83 inference(trivial_inequality_removal,[],[f37])).
% 10.05/1.83 thf(f66,plain,(
% 10.05/1.83 ( ! [X2 : $i,X0 : $i,X1 : ($i > $i)] : ((sK0 != X2) | ($false = ((r @ c0 @ (X1 @ c0)))) | ($true = ((r @ (sK1 @ (^[Y0 : $i]: (r @ Y0 @ (X1 @ Y0)))) @ (X1 @ (sK1 @ (^[Y0 : $i]: (r @ Y0 @ (X1 @ Y0)))))))) | (((X1 @ X2)) != X0)) )),
% 10.05/1.83 inference(beta-eta_normalization,[],[f65])).
% 10.05/1.83 thf(f122,plain,(
% 10.05/1.83 ( ! [X0 : $i] : (($true != $true) | ($false = ((r @ sK0 @ X0)))) )),
% 10.05/1.83 inference(constrained_superposition,[],[f16,f18])).
% 10.05/1.83 thf(f124,plain,(
% 10.05/1.83 ( ! [X0 : $i] : (($false = ((r @ sK0 @ X0)))) )),
% 10.05/1.83 inference(trivial_inequality_removal,[],[f122])).
% 10.05/1.83 thf(f218,plain,(
% 10.05/1.83 ( ! [X2 : ($i > $i),X3 : $i,X0 : $i,X1 : $i] : (($true = $false) | (((r @ X0 @ X1)) != $true) | ($true = (((^[Y0 : $i]: (r @ (X2 @ Y0) @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X3))) | ($false = (((^[Y0 : $i]: (r @ (X2 @ Y0) @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ c0))) | (((sK1 @ (^[Y0 : $i]: (r @ (X2 @ Y0) @ Y0)))) != X1) | (((cS @ X0)) != ((X2 @ (cS @ (sK1 @ (^[Y0 : $i]: (r @ (X2 @ Y0) @ Y0)))))))) )),
% 10.05/1.83 inference(constrained_superposition,[],[f15,f27])).
% 10.05/1.83 thf(f262,plain,(
% 10.05/1.83 ( ! [X2 : ($i > $i),X3 : $i,X0 : $i,X1 : $i] : ((((r @ X0 @ X1)) != $true) | ($true = (((^[Y0 : $i]: (r @ (X2 @ Y0) @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X3))) | ($false = (((^[Y0 : $i]: (r @ (X2 @ Y0) @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ c0))) | (((sK1 @ (^[Y0 : $i]: (r @ (X2 @ Y0) @ Y0)))) != X1) | (((cS @ X0)) != ((X2 @ (cS @ (sK1 @ (^[Y0 : $i]: (r @ (X2 @ Y0) @ Y0)))))))) )),
% 10.05/1.83 inference(trivial_inequality_removal,[],[f218])).
% 10.05/1.83 thf(f263,plain,(
% 10.05/1.83 ( ! [X2 : ($i > $i),X3 : $i,X0 : $i,X1 : $i] : ((((cS @ X0)) != ((X2 @ (cS @ (sK1 @ (^[Y0 : $i]: (r @ (X2 @ Y0) @ Y0))))))) | ($true = ((r @ (X2 @ X3) @ X3))) | ($false = ((r @ (X2 @ c0) @ c0))) | (((sK1 @ (^[Y0 : $i]: (r @ (X2 @ Y0) @ Y0)))) != X1) | (((r @ X0 @ X1)) != $true)) )),
% 10.05/1.83 inference(beta-eta_normalization,[],[f262])).
% 10.05/1.83 thf(f1122,plain,(
% 10.05/1.83 ( ! [X0 : ($i > $i),X1 : $i] : (($true = ((r @ (sK1 @ (^[Y0 : $i]: (r @ Y0 @ (X0 @ Y0)))) @ (X0 @ (sK1 @ (^[Y0 : $i]: (r @ Y0 @ (X0 @ Y0)))))))) | ($false = ((r @ c0 @ (X0 @ c0)))) | (((X0 @ sK0)) != X1)) )),
% 10.05/1.83 inference(equality_resolution,[],[f66])).
% 10.05/1.83 thf(f1377,definition,(
% 10.05/1.83 spl2_12 <=> ! [X2 : $i] : (sK0 != X2)),
% 10.05/1.83 introduced(definition,[new_symbols(definition,[spl2_12])],[avatar_definition])).
% 10.05/1.83 thf(f1378,plain,(
% 10.05/1.83 ( ! [X2 : $i] : ((sK0 != X2)) ) | ~spl2_12),
% 10.05/1.83 inference(avatar_component_clause,[],[f1377])).
% 10.05/1.83 thf(f1430,plain,(
% 10.05/1.83 $false | ~spl2_12),
% 10.05/1.83 inference(equality_resolution,[],[f1378])).
% 10.05/1.83 thf(f1431,plain,(
% 10.05/1.83 ~spl2_12),
% 10.05/1.83 inference(avatar_contradiction_clause,[],[f1430])).
% 10.05/1.83 thf(f1470,plain,(
% 10.05/1.83 ( ! [X2 : ($i > $o),X0 : $i,X1 : $i] : (($true = ((r @ ((^[Y0 : $i]: (Y0)) @ X0) @ X0))) | ($false = ((r @ ((^[Y0 : $i]: (Y0)) @ c0) @ c0))) | (((sK1 @ (^[Y0 : $i]: (r @ ((^[Y1 : $i]: (Y1)) @ Y0) @ Y0)))) != X1) | ($true != ((r @ (sK1 @ X2) @ X1))) | ((^[Y0 : $i]: (r @ Y0 @ Y0)) != X2)) )),
% 10.05/1.83 inference(equality_resolution,[],[f263])).
% 10.05/1.83 thf(f1473,plain,(
% 10.05/1.83 ( ! [X2 : ($i > $o),X0 : $i,X1 : $i] : (($true = ((r @ X0 @ X0))) | (((r @ c0 @ c0)) = $false) | (((sK1 @ (^[Y0 : $i]: (r @ Y0 @ Y0)))) != X1) | ($true != ((r @ (sK1 @ X2) @ X1))) | ((^[Y0 : $i]: (r @ Y0 @ Y0)) != X2)) )),
% 10.05/1.83 inference(beta-eta_normalization,[],[f1470])).
% 10.05/1.83 thf(f1491,plain,(
% 10.05/1.83 ( ! [X2 : ($i > $o),X0 : $i,X1 : $i] : (($true = $false) | ($true = ((r @ X0 @ X0))) | (((sK1 @ (^[Y0 : $i]: (r @ Y0 @ Y0)))) != X1) | ($true != ((r @ (sK1 @ X2) @ X1))) | ((^[Y0 : $i]: (r @ Y0 @ Y0)) != X2)) )),
% 10.05/1.83 inference(forward_demodulation,[],[f1473,f14])).
% 10.05/1.83 thf(f1492,plain,(
% 10.05/1.83 ( ! [X2 : ($i > $o),X0 : $i,X1 : $i] : (($true = ((r @ X0 @ X0))) | (((sK1 @ (^[Y0 : $i]: (r @ Y0 @ Y0)))) != X1) | ($true != ((r @ (sK1 @ X2) @ X1))) | ((^[Y0 : $i]: (r @ Y0 @ Y0)) != X2)) )),
% 10.05/1.83 inference(trivial_inequality_removal,[],[f1491])).
% 10.05/1.83 thf(f1501,definition,(
% 10.05/1.83 spl2_23 <=> ! [X2 : ($i > $o),X1 : $i] : ((((sK1 @ (^[Y0 : $i]: (r @ Y0 @ Y0)))) != X1) | ((^[Y0 : $i]: (r @ Y0 @ Y0)) != X2) | ($true != ((r @ (sK1 @ X2) @ X1))))),
% 10.05/1.83 introduced(definition,[new_symbols(definition,[spl2_23])],[avatar_definition])).
% 10.05/1.83 thf(f1502,plain,(
% 10.05/1.83 ( ! [X2 : ($i > $o),X1 : $i] : ((((sK1 @ (^[Y0 : $i]: (r @ Y0 @ Y0)))) != X1) | ((^[Y0 : $i]: (r @ Y0 @ Y0)) != X2) | ($true != ((r @ (sK1 @ X2) @ X1)))) ) | ~spl2_23),
% 10.05/1.83 inference(avatar_component_clause,[],[f1501])).
% 10.05/1.83 thf(f1504,definition,(
% 10.05/1.83 spl2_24 <=> ! [X0 : $i] : ($true = ((r @ X0 @ X0)))),
% 10.05/1.83 introduced(definition,[new_symbols(definition,[spl2_24])],[avatar_definition])).
% 10.05/1.83 thf(f1505,plain,(
% 10.05/1.83 ( ! [X0 : $i] : (($true = ((r @ X0 @ X0)))) ) | ~spl2_24),
% 10.05/1.83 inference(avatar_component_clause,[],[f1504])).
% 10.05/1.83 thf(f1506,plain,(
% 10.05/1.83 spl2_23 | spl2_24),
% 10.05/1.83 inference(avatar_split_clause,[],[f1492,f1504,f1501])).
% 10.05/1.83 thf(f1605,plain,(
% 10.05/1.83 ($true = $false) | ~spl2_24),
% 10.05/1.83 inference(constrained_superposition,[],[f1505,f124])).
% 10.05/1.83 thf(f1645,plain,(
% 10.05/1.83 $false | ~spl2_24),
% 10.05/1.83 inference(trivial_inequality_removal,[],[f1605])).
% 10.05/1.83 thf(f1646,plain,(
% 10.05/1.83 ~spl2_24),
% 10.05/1.83 inference(avatar_contradiction_clause,[],[f1645])).
% 10.05/1.83 thf(f3074,plain,(
% 10.05/1.83 ( ! [X0 : ($i > $o)] : (($true != ((r @ (sK1 @ X0) @ (sK1 @ (^[Y0 : $i]: (r @ Y0 @ Y0)))))) | ((^[Y0 : $i]: (r @ Y0 @ Y0)) != X0)) ) | ~spl2_23),
% 10.05/1.83 inference(equality_resolution,[],[f1502])).
% 10.05/1.83 thf(f11011,plain,(
% 10.05/1.83 ( ! [X0 : $i] : (($true != $true) | ((^[Y0 : $i]: (r @ Y0 @ Y0)) != (^[Y0 : $i]: (r @ Y0 @ ((^[Y1 : $i]: (Y1)) @ Y0)))) | ($false = ((r @ c0 @ ((^[Y0 : $i]: (Y0)) @ c0)))) | ((((^[Y0 : $i]: (Y0)) @ sK0)) != X0)) ) | ~spl2_23),
% 10.05/1.83 inference(constrained_superposition,[],[f3074,f1122])).
% 10.05/1.83 thf(f11056,plain,(
% 10.05/1.83 ( ! [X0 : $i] : (((^[Y0 : $i]: (r @ Y0 @ Y0)) != (^[Y0 : $i]: (r @ Y0 @ ((^[Y1 : $i]: (Y1)) @ Y0)))) | ($false = ((r @ c0 @ ((^[Y0 : $i]: (Y0)) @ c0)))) | ((((^[Y0 : $i]: (Y0)) @ sK0)) != X0)) ) | ~spl2_23),
% 10.05/1.83 inference(trivial_inequality_removal,[],[f11011])).
% 10.05/1.83 thf(f11057,plain,(
% 10.05/1.83 ( ! [X0 : $i] : (((^[Y0 : $i]: (r @ Y0 @ Y0)) != (^[Y0 : $i]: (r @ Y0 @ Y0))) | (((r @ c0 @ c0)) = $false) | (sK0 != X0)) ) | ~spl2_23),
% 10.05/1.83 inference(beta-eta_normalization,[],[f11056])).
% 10.05/1.83 thf(f11058,plain,(
% 10.05/1.83 ( ! [X0 : $i] : ((((r @ c0 @ c0)) = $false) | (sK0 != X0)) ) | ~spl2_23),
% 10.05/1.83 inference(trivial_inequality_removal,[],[f11057])).
% 10.05/1.83 thf(f11076,plain,(
% 10.05/1.83 ( ! [X0 : $i] : (($true = $false) | (sK0 != X0)) ) | ~spl2_23),
% 10.05/1.83 inference(forward_demodulation,[],[f11058,f14])).
% 10.05/1.83 thf(f11077,plain,(
% 10.05/1.83 ( ! [X0 : $i] : ((sK0 != X0)) ) | ~spl2_23),
% 10.05/1.83 inference(trivial_inequality_removal,[],[f11076])).
% 10.05/1.83 thf(f11095,plain,(
% 10.05/1.83 spl2_12 | ~spl2_23),
% 10.05/1.83 inference(avatar_split_clause,[],[f11077,f1501,f1377])).
% 10.05/1.83 cnf(s22, plain, ~spl2_12, inference(sat_conversion,[],[f1431])).
% 10.05/1.83 cnf(s23, plain, spl2_23 | spl2_24, inference(sat_conversion,[],[f1506])).
% 10.05/1.83 cnf(s34, plain, ~spl2_24, inference(sat_conversion,[],[f1646])).
% 10.05/1.83 cnf(s498, plain, spl2_12 | ~spl2_23, inference(sat_conversion,[],[f11095])).
% 10.05/1.83 cnf(s522, plain, spl2_23, inference(rat,[],[s23,s34])).
% 10.05/1.83 cnf(s523, plain, spl2_12, inference(rat,[],[s498,s522])).
% 10.05/1.83 cnf(s525, plain, $false, inference(rat,[],[s22,s523])).
% 10.05/1.83 thf(f11096,plain,(
% 10.05/1.83 $false),
% 10.05/1.83 inference(avatar_sat_refutation,[],[s525])).
% 10.05/1.83 % SZS output end Proof for theBenchmark
% 10.05/1.83 % (1242429)------------------------------
% 10.05/1.83 % (1242429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.05/1.83 % (1242429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.05/1.83 % (1242429)CaDiCaL version: 2.1.3
% 10.05/1.83 % (1242429)Termination reason: Refutation
% 10.05/1.83 % (1242429)Time elapsed: 0.650 s
% 10.05/1.83 % (1242429)Peak memory usage: 17 MB
% 10.05/1.83 % (1242429)Instructions burned: 1363 (million)
% 10.05/1.83 % (1242216)Success in time 1.575 s
% 10.05/1.83 % Vampire exiting
%------------------------------------------------------------------------------