%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO545^1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n019.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:50:24 AM UTC 2026
% Result : Theorem 0.20s 0.36s
% Output : Refutation 0.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO545^1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.20 % Computer : n019.cluster.edu
% 0.10/0.20 % Model : x86_64 x86_64
% 0.10/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.20 % Memory : 8046.5625MB
% 0.10/0.20 % OS : Linux 6.8.0-71-generic
% 0.10/0.20 % CPULimit : 300
% 0.10/0.20 % WCLimit : 300
% 0.10/0.20 % DateTime : Tue Sep 29 17:14:18 UTC 2026
% 0.10/0.20 % CPUTime :
% 0.10/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.24 Running first-order model finding
% 0.10/0.24 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
% 0.20/0.36 % (1098069)Will run a generic schedule for satisfiability detection.
% 0.20/0.36 % (1098077)dis+10_1_sil=32000:sp=arity:random_seed=4287616897:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.20/0.36 % (1098075)% WARNING: option uhcvi not known.
% 0.20/0.36 % (1098077)Refutation not found, incomplete strategy
% 0.20/0.36 % (1098077)------------------------------
% 0.20/0.36 % (1098077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.36 % (1098077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.36 % (1098077)CaDiCaL version: 2.1.3
% 0.20/0.36 % (1098077)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.36 % (1098077)Time elapsed: 0.005 s
% 0.20/0.36 % (1098077)Peak memory usage: 12 MB
% 0.20/0.36 % (1098077)Instructions burned: 15 (million)
% 0.20/0.36 % (1098077)------------------------------
% 0.20/0.36 % (1098077)------------------------------
% 0.20/0.36 % (1098074)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2242789984_2999 on theBenchmark for (2999ds/0Mi)
% 0.20/0.36 % (1098075)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1820587416:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.20/0.36 % (1098076)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1132230019:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.20/0.36 % (1098078)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1567194103:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.20/0.36 % (1098075)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.20/0.36 % (1098078)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.20/0.36 % Exception at run slice level
% 0.20/0.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.20/0.36 % (1098075)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.20/0.36 % (1098079)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2941155260:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.20/0.36 % (1098075)Refutation not found, incomplete strategy
% 0.20/0.36 % (1098075)------------------------------
% 0.20/0.36 % (1098075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.36 % (1098075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.36 % (1098075)CaDiCaL version: 2.1.3
% 0.20/0.36 % (1098075)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.36 % (1098075)Time elapsed: 0.009 s
% 0.20/0.36 % (1098075)Peak memory usage: 12 MB
% 0.20/0.36 % (1098075)Instructions burned: 15 (million)
% 0.20/0.36 % (1098075)------------------------------
% 0.20/0.36 % (1098075)------------------------------
% 0.20/0.36 % (1098080)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3134872801:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.20/0.36 % (1098079)Refutation not found, incomplete strategy
% 0.20/0.36 % (1098079)------------------------------
% 0.20/0.36 % (1098079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.36 % (1098079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.36 % (1098079)CaDiCaL version: 2.1.3
% 0.20/0.36 % (1098079)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.36 % (1098079)Time elapsed: 0.004 s
% 0.20/0.36 % (1098079)Peak memory usage: 12 MB
% 0.20/0.36 % (1098079)Instructions burned: 14 (million)
% 0.20/0.36 % (1098079)------------------------------
% 0.20/0.36 % (1098079)------------------------------
% 0.20/0.36 % (1098078)Refutation not found, incomplete strategy
% 0.20/0.36 % (1098078)------------------------------
% 0.20/0.36 % (1098078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.36 % (1098078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.36 % (1098078)CaDiCaL version: 2.1.3
% 0.20/0.36 % (1098078)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.36 % (1098078)Time elapsed: 0.013 s
% 0.20/0.36 % (1098078)Peak memory usage: 12 MB
% 0.20/0.36 % (1098078)Instructions burned: 25 (million)
% 0.20/0.36 % (1098078)------------------------------
% 0.20/0.36 % (1098078)------------------------------
% 0.20/0.36 % (1098076)Refutation not found, incomplete strategy
% 0.20/0.36 % (1098076)------------------------------
% 0.20/0.36 % (1098076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.36 % (1098076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.36 % (1098076)CaDiCaL version: 2.1.3
% 0.20/0.36 % (1098076)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.36 % (1098076)Time elapsed: 0.015 s
% 0.20/0.36 % (1098076)Peak memory usage: 12 MB
% 0.20/0.36 % (1098076)Instructions burned: 24 (million)
% 0.20/0.36 % (1098076)------------------------------
% 0.20/0.36 % (1098076)------------------------------
% 0.20/0.36 % (1098082)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=976565358:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.20/0.36 % (1098080)Refutation not found, incomplete strategy
% 0.20/0.36 % (1098080)------------------------------
% 0.20/0.36 % (1098080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.36 % Exception at run slice level
% 0.20/0.36 % (1098080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.20/0.36 % (1098080)CaDiCaL version: 2.1.3
% 0.20/0.36 % (1098080)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.36 % (1098080)Time elapsed: 0.008 s
% 0.20/0.36 % (1098080)Peak memory usage: 12 MB
% 0.20/0.36 % (1098080)Instructions burned: 15 (million)
% 0.20/0.36 % (1098087)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3507170435:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.20/0.36 % (1098080)------------------------------
% 0.20/0.36 % (1098080)------------------------------
% 0.20/0.36 % (1098091)ott-21_1_sil=16000:fs=off:random_seed=1240249107:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 0.20/0.36 % (1098089)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=2054732313:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 0.20/0.36 % (1098087)Refutation not found, incomplete strategy
% 0.20/0.36 % (1098087)------------------------------
% 0.20/0.36 % (1098087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.36 % (1098087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.36 % (1098087)CaDiCaL version: 2.1.3
% 0.20/0.36 % (1098087)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.36 % (1098087)Time elapsed: 0.008 s
% 0.20/0.36 % (1098087)Peak memory usage: 12 MB
% 0.20/0.36 % (1098087)Instructions burned: 13 (million)
% 0.20/0.36 % (1098089)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.20/0.36 % (1098087)------------------------------
% 0.20/0.36 % (1098087)------------------------------
% 0.20/0.36 % (1098089)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.20/0.36 % (1098092)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1684331761:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 0.20/0.36 % (1098093)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=787227418:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi)
% 0.20/0.36 % Exception at run slice level
% 0.20/0.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.20/0.36 % (1098089)Refutation not found, incomplete strategy
% 0.20/0.36 % (1098089)------------------------------
% 0.20/0.36 % (1098089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.36 % (1098089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.36 % (1098089)CaDiCaL version: 2.1.3
% 0.20/0.36 % (1098089)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.36 % (1098089)Time elapsed: 0.009 s
% 0.20/0.36 % (1098089)Peak memory usage: 12 MB
% 0.20/0.36 % (1098089)Instructions burned: 15 (million)
% 0.20/0.36 % (1098089)------------------------------
% 0.20/0.36 % (1098089)------------------------------
% 0.20/0.36 % (1098096)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3210008028:i=1179_2999 on theBenchmark for (2999ds/1179Mi)
% 0.20/0.36 % (1098097)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=980459215:i=889:ins=1_2999 on theBenchmark for (2999ds/889Mi)
% 0.20/0.36 % Exception at run slice level
% 0.20/0.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.20/0.36 % (1098105)fmb+10_1_sil=64000:random_seed=3610492866:i=22061:nm=2:gsp=on_2999 on theBenchmark for (2999ds/22061Mi)
% 0.20/0.36 % (1098092)Refutation not found, incomplete strategy
% 0.20/0.36 % (1098092)------------------------------
% 0.20/0.36 % (1098092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.36 % (1098092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.36 % (1098092)CaDiCaL version: 2.1.3
% 0.20/0.36 % (1098092)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.36 % (1098092)Time elapsed: 0.025 s
% 0.20/0.36 % (1098092)Peak memory usage: 12 MB
% 0.20/0.36 % (1098092)Instructions burned: 44 (million)
% 0.20/0.36 % (1098105)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 0.20/0.36 % (1098100)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=2180197175:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2999 on theBenchmark for (2999ds/692Mi)
% 0.20/0.36 % Exception at run slice level
% 0.20/0.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.20/0.36 % (1098092)------------------------------
% 0.20/0.36 % (1098092)------------------------------
% 0.20/0.36 % (1098100)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.20/0.36 % (1098107)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2120161475:i=9515:nm=5_2999 on theBenchmark for (2999ds/9515Mi)
% 0.20/0.36 % Exception at run slice level
% 0.20/0.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.20/0.36 % (1098103)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2277514693:i=879:kws=inv_precedence:fsr=off_2999 on theBenchmark for (2999ds/879Mi)
% 0.20/0.36 % (1098103)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.20/0.36 % (1098091)Instruction limit reached!
% 0.20/0.36 % (1098091)------------------------------
% 0.20/0.36 % (1098091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.36 % (1098091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.36 % (1098091)CaDiCaL version: 2.1.3
% 0.20/0.36 % (1098091)Termination reason: Instruction limit
% 0.20/0.36 % (1098091)Termination phase: Saturation
% 0.20/0.36 % (1098091)Time elapsed: 0.044 s
% 0.20/0.36 % (1098091)Peak memory usage: 12 MB
% 0.20/0.36 % (1098091)Instructions burned: 183 (million)
% 0.20/0.36 % (1098100)Refutation not found, incomplete strategy
% 0.20/0.36 % (1098100)------------------------------
% 0.20/0.36 % (1098100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.36 % (1098100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.36 % (1098100)CaDiCaL version: 2.1.3
% 0.20/0.36 % (1098100)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.36 % (1098100)Time elapsed: 0.009 s
% 0.20/0.36 % (1098100)Peak memory usage: 12 MB
% 0.20/0.36 % (1098100)Instructions burned: 14 (million)
% 0.20/0.36 % (1098100)------------------------------
% 0.20/0.36 % (1098100)------------------------------
% 0.20/0.36 % (1098096) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1098069-1098096"...
% 0.20/0.36 % (1098110)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1787296637:fmbsr=1.7:i=920_2999 on theBenchmark for (2999ds/920Mi)
% 0.20/0.36 % (1098115)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2363486871:i=6324_2999 on theBenchmark for (2999ds/6324Mi)
% 0.20/0.36 % Exception at run slice level
% 0.20/0.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.20/0.36 % Exception at run slice level
% 0.20/0.36 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.20/0.36 % (1098113)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3595842177:i=1472:ins=7:fdi=8:gsp=on_2999 on theBenchmark for (2999ds/1472Mi)
% 0.20/0.36 % (1098096)...printing done.
% 0.20/0.36 % (1098113)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 0.20/0.36 % (1098113)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.20/0.36 % (1098096)Refutation found. Thanks to Tanya!
% 0.20/0.36 % SZS status Theorem for theBenchmark
% 0.20/0.36 % SZS output start Proof for theBenchmark
% 0.20/0.36 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 0.20/0.36 thf(func_def_0, type, eps: (($i > $o) > $i)).
% 0.20/0.36 thf(func_def_2, type, case: (($o > $o) > $i > $i > $i > $i > $i)).
% 0.20/0.36 thf(func_def_3, type, vNOT: ($o > $o)).
% 0.20/0.36 thf(func_def_4, type, f: ($o > $o)).
% 0.20/0.36 thf(func_def_7, type, vOR: ($o > $o > $o)).
% 0.20/0.36 thf(func_def_8, type, vAND: ($o > $o > $o)).
% 0.20/0.36 thf(func_def_9, type, db5: !>[X0: $tType]:(X0)).
% 0.20/0.36 thf(func_def_10, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.20/0.36 thf(func_def_11, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.20/0.36 thf(func_def_12, type, db4: !>[X0: $tType]:(X0)).
% 0.20/0.36 thf(func_def_13, type, db0: !>[X0: $tType]:(X0)).
% 0.20/0.36 thf(func_def_14, type, db3: !>[X0: $tType]:(X0)).
% 0.20/0.36 thf(func_def_15, type, db2: !>[X0: $tType]:(X0)).
% 0.20/0.36 thf(func_def_16, type, db1: !>[X0: $tType]:(X0)).
% 0.20/0.36 thf(func_def_23, type, sK6: $o).
% 0.20/0.36 thf(func_def_24, type, sK7: $o).
% 0.20/0.36 thf(func_def_25, type, sK8: $o).
% 0.20/0.36 thf(func_def_26, type, sK9: $o).
% 0.20/0.36 thf(func_def_27, type, sK10: $o).
% 0.20/0.36 thf(func_def_28, type, sK11: $o).
% 0.20/0.36 thf(func_def_29, type, sK12: $o).
% 0.20/0.36 thf(func_def_30, type, sK13: $o).
% 0.20/0.36 thf(f1,axiom,(
% 0.20/0.36 ! [X0 : ($i > $o)] : (? [X1 : $i] : (X0 @ X1) => (X0 @ (eps @ X0)))),
% 0.20/0.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p',choiceax)).
% 0.20/0.36 thf(f2,axiom,(
% 0.20/0.36 (case = (^[X0 : ($o > $o), X1 : $i, X2 : $i, X3 : $i, X4 : $i] : ((eps @ (^[X5 : $i] : (((X5 = X4) & (X0 = (^[X6 : $o] : ($true)))) | ((X5 = X3) & (X0 = (^[X6 : $o] : (X6)))) | ((X5 = X2) & (X0 = ~)) | ((X5 = X1) & (X0 = (^[X6 : $o] : ($false))))))))))),
% 0.20/0.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p',caseood)).
% 0.20/0.36 thf(f3,conjecture,(
% 0.20/0.36 ! [X0 : $i,X1 : $i,X2 : $i,X3 : $i] : ((((case @ f @ X0 @ X1 @ X2 @ X3)) = X3) | (((case @ f @ X0 @ X1 @ X2 @ X3)) = X2) | (((case @ f @ X0 @ X1 @ X2 @ X3)) = X1) | (((case @ f @ X0 @ X1 @ X2 @ X3)) = X0))),
% 0.20/0.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj)).
% 0.20/0.36 thf(f4,negated_conjecture,(
% 0.20/0.36 ~ ! [X0 : $i,X1 : $i,X2 : $i,X3 : $i] : ((((case @ f @ X0 @ X1 @ X2 @ X3)) = X3) | (((case @ f @ X0 @ X1 @ X2 @ X3)) = X2) | (((case @ f @ X0 @ X1 @ X2 @ X3)) = X1) | (((case @ f @ X0 @ X1 @ X2 @ X3)) = X0))),
% 0.20/0.36 inference(negated_conjecture,[status(cth)],[f3])).
% 0.20/0.36 thf(f5,plain,(
% 0.20/0.36 ! [X0 : ($i > $o)] : (? [X1 : $i] : (X0 @ X1) => (X0 @ (eps @ X0)))),
% 0.20/0.36 inference(rectify,[],[f1])).
% 0.20/0.36 thf(f6,plain,(
% 0.20/0.36 ! [X0 : ($i > $o)] : (? [X1 : $i] : (((X0 @ X1)) = $true) => (((X0 @ (eps @ X0))) = $true))),
% 0.20/0.36 inference(fool_elimination,[],[f5])).
% 0.20/0.36 thf(f7,plain,(
% 0.20/0.36 (case = (^[X0 : ($o > $o), X1 : $i, X2 : $i, X3 : $i, X4 : $i] : ((eps @ (^[X5 : $i] : (((X5 = X4) & (X0 = (^[X6 : $o] : ($true)))) | ((X5 = X3) & (X0 = (^[X7 : $o] : (X7)))) | ((X5 = X2) & (X0 = ~)) | ((X5 = X1) & (X0 = (^[X8 : $o] : ($false))))))))))),
% 0.20/0.36 inference(rectify,[],[f2])).
% 0.20/0.36 thf(f8,plain,(
% 0.20/0.36 (case = (^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((~ = Y0) & (Y2 = Y5))) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5))) | ((Y0 = (^[Y6 : $o]: ($true))) & (Y4 = Y5)))))))))))))))),
% 0.20/0.36 inference(fool_elimination,[],[f7])).
% 0.20/0.36 thf(f9,plain,(
% 0.20/0.36 ! [X0 : ($i > $o)] : ((((X0 @ (eps @ X0))) = $true) | ! [X1 : $i] : (((X0 @ X1)) != $true))),
% 0.20/0.36 inference(ennf_transformation,[],[f6])).
% 0.20/0.36 thf(f10,plain,(
% 0.20/0.36 ? [X0 : $i,X1 : $i,X2 : $i,X3 : $i] : ((((case @ f @ X0 @ X1 @ X2 @ X3)) != X3) & (((case @ f @ X0 @ X1 @ X2 @ X3)) != X2) & (((case @ f @ X0 @ X1 @ X2 @ X3)) != X1) & (((case @ f @ X0 @ X1 @ X2 @ X3)) != X0))),
% 0.20/0.36 inference(ennf_transformation,[],[f4])).
% 0.20/0.36 thf(f11,plain,(
% 0.20/0.36 (sK3 != ((case @ f @ sK0 @ sK1 @ sK2 @ sK3))) & (sK2 != ((case @ f @ sK0 @ sK1 @ sK2 @ sK3))) & (sK1 != ((case @ f @ sK0 @ sK1 @ sK2 @ sK3))) & (sK0 != ((case @ f @ sK0 @ sK1 @ sK2 @ sK3)))),
% 0.20/0.36 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3)],[f10])).
% 0.20/0.36 thf(f12,plain,(
% 0.20/0.36 ( ! [X0 : ($i > $o),X1 : $i] : ((((X0 @ X1)) != $true) | (((X0 @ (eps @ X0))) = $true)) )),
% 0.20/0.36 inference(cnf_transformation,[],[f9])).
% 0.20/0.36 thf(f13,plain,(
% 0.20/0.36 (case = (^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((~ = Y0) & (Y2 = Y5))) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5))) | ((Y0 = (^[Y6 : $o]: ($true))) & (Y4 = Y5)))))))))))))))),
% 0.20/0.36 inference(cnf_transformation,[],[f8])).
% 0.20/0.36 thf(f14,plain,(
% 0.20/0.36 (sK0 != ((case @ f @ sK0 @ sK1 @ sK2 @ sK3)))),
% 0.20/0.36 inference(cnf_transformation,[],[f11])).
% 0.20/0.36 thf(f15,plain,(
% 0.20/0.36 (sK1 != ((case @ f @ sK0 @ sK1 @ sK2 @ sK3)))),
% 0.20/0.36 inference(cnf_transformation,[],[f11])).
% 0.20/0.36 thf(f16,plain,(
% 0.20/0.36 (sK2 != ((case @ f @ sK0 @ sK1 @ sK2 @ sK3)))),
% 0.20/0.36 inference(cnf_transformation,[],[f11])).
% 0.20/0.36 thf(f17,plain,(
% 0.20/0.36 (sK3 != ((case @ f @ sK0 @ sK1 @ sK2 @ sK3)))),
% 0.20/0.36 inference(cnf_transformation,[],[f11])).
% 0.20/0.36 thf(f19,definition,(
% 0.20/0.36 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.20/0.36 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.20/0.36 thf(f20,plain,(
% 0.20/0.36 (sK3 != (((^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((~ = Y0) & (Y2 = Y5))) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5))) | ((Y0 = (^[Y6 : $o]: ($true))) & (Y4 = Y5)))))))))))))) @ f @ sK0 @ sK1 @ sK2 @ sK3)))),
% 0.20/0.36 inference(definition_unfolding,[],[f17,f13])).
% 0.20/0.36 thf(f21,plain,(
% 0.20/0.36 (sK2 != (((^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((~ = Y0) & (Y2 = Y5))) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5))) | ((Y0 = (^[Y6 : $o]: ($true))) & (Y4 = Y5)))))))))))))) @ f @ sK0 @ sK1 @ sK2 @ sK3)))),
% 0.20/0.36 inference(definition_unfolding,[],[f16,f13])).
% 0.20/0.36 thf(f22,plain,(
% 0.20/0.36 (sK1 != (((^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((~ = Y0) & (Y2 = Y5))) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5))) | ((Y0 = (^[Y6 : $o]: ($true))) & (Y4 = Y5)))))))))))))) @ f @ sK0 @ sK1 @ sK2 @ sK3)))),
% 0.20/0.36 inference(definition_unfolding,[],[f15,f13])).
% 0.20/0.36 thf(f23,plain,(
% 0.20/0.36 (sK0 != (((^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((~ = Y0) & (Y2 = Y5))) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5))) | ((Y0 = (^[Y6 : $o]: ($true))) & (Y4 = Y5)))))))))))))) @ f @ sK0 @ sK1 @ sK2 @ sK3)))),
% 0.20/0.36 inference(definition_unfolding,[],[f14,f13])).
% 0.20/0.36 thf(f24,definition,(
% 0.20/0.36 (sF4 = (((^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((~ = Y0) & (Y2 = Y5))) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5))) | ((Y0 = (^[Y6 : $o]: ($true))) & (Y4 = Y5)))))))))))))) @ f @ sK0 @ sK1 @ sK2 @ sK3)))),
% 0.20/0.36 introduced(definition,[new_symbols(definition,[sF4])],[function_definition])).
% 0.20/0.36 thf(f25,plain,(
% 0.20/0.36 ((((^[Y0 : $o > $o]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (eps @ (^[Y5 : $i]: (((((Y0 = (^[Y6 : $o]: ($false))) & (Y1 = Y5)) | ((~ = Y0) & (Y2 = Y5))) | ((Y0 = (^[Y6 : $o]: (Y6))) & (Y3 = Y5))) | ((Y0 = (^[Y6 : $o]: ($true))) & (Y4 = Y5)))))))))))))) @ f @ sK0 @ sK1 @ sK2 @ sK3)) = sF4)),
% 0.20/0.36 inference(reorient_equations,[],[f24])).
% 0.20/0.36 thf(f26,plain,(
% 0.20/0.36 (sK3 != sF4)),
% 0.20/0.36 inference(definition_folding,[],[f20,f25])).
% 0.20/0.36 thf(f27,plain,(
% 0.20/0.36 (sK2 != sF4)),
% 0.20/0.36 inference(definition_folding,[],[f21,f25])).
% 0.20/0.36 thf(f28,plain,(
% 0.20/0.36 (sK1 != sF4)),
% 0.20/0.36 inference(definition_folding,[],[f22,f25])).
% 0.20/0.36 thf(f29,plain,(
% 0.20/0.36 (sK0 != sF4)),
% 0.20/0.36 inference(definition_folding,[],[f23,f25])).
% 0.20/0.36 thf(f30,plain,(
% 0.20/0.36 (sF4 = ((eps @ (^[Y0 : $i]: (((((f = (^[Y1 : $o]: ($false))) & (sK0 = Y0)) | ((~ = f) & (sK1 = Y0))) | ((f = (^[Y1 : $o]: (Y1))) & (sK2 = Y0))) | ((f = (^[Y1 : $o]: ($true))) & (sK3 = Y0)))))))),
% 0.20/0.36 inference(beta-eta_normalization,[],[f25])).
% 0.20/0.36 thf(f41,plain,(
% 0.20/0.36 ( ! [X2 : ($i > $o),X1 : $i] : (($true != (((^[Y0 : $i]: (~ (X2 @ Y0))) @ X1))) | ($true = (((^[Y0 : $i]: (~ (X2 @ Y0))) @ (eps @ (^[Y0 : $i]: (~ (X2 @ Y0)))))))) )),
% 0.20/0.36 inference(primitive_instantiation,[],[f12])).
% 0.20/0.36 thf(f43,plain,(
% 0.20/0.36 ( ! [X0 : ($i > $o),X1 : $i] : (($true != $true) | (((X0 @ (eps @ X0))) = $true) | (((X0 @ X1)) = $false)) )),
% 0.20/0.36 inference(constrained_superposition,[],[f12,f19])).
% 0.20/0.36 thf(f46,plain,(
% 0.20/0.36 ( ! [X0 : ($i > $o),X1 : $i] : ((((X0 @ (eps @ X0))) = $true) | (((X0 @ X1)) = $false)) )),
% 0.20/0.36 inference(trivial_inequality_removal,[],[f43])).
% 0.20/0.36 thf(f48,plain,(
% 0.20/0.36 ( ! [X2 : ($i > $o),X1 : $i] : (($true != ((~ (X2 @ X1)))) | ($true = ((~ (X2 @ (eps @ (^[Y0 : $i]: (~ (X2 @ Y0))))))))) )),
% 0.20/0.36 inference(beta-eta_normalization,[],[f41])).
% 0.20/0.36 thf(f49,plain,(
% 0.20/0.36 ( ! [X2 : ($i > $o),X1 : $i] : (($true = ((X2 @ X1))) | ($true = ((~ (X2 @ (eps @ (^[Y0 : $i]: (~ (X2 @ Y0))))))))) )),
% 0.20/0.36 inference(not_proxy_clausification,[],[f48])).
% 0.20/0.36 thf(f50,plain,(
% 0.20/0.36 ( ! [X2 : ($i > $o),X1 : $i] : (($true = ((X2 @ X1))) | ($false = ((X2 @ (eps @ (^[Y0 : $i]: (~ (X2 @ Y0)))))))) )),
% 0.20/0.36 inference(not_proxy_clausification,[],[f49])).
% 0.20/0.36 thf(f60,plain,(
% 0.20/0.36 ( ! [X0 : $i] : (($true = (((^[Y0 : $i]: (((((f = (^[Y1 : $o]: ($false))) & (sK0 = Y0)) | ((~ = f) & (sK1 = Y0))) | ((f = (^[Y1 : $o]: (Y1))) & (sK2 = Y0))) | ((f = (^[Y1 : $o]: ($true))) & (sK3 = Y0)))) @ sF4))) | ($false = (((^[Y0 : $i]: (((((f = (^[Y1 : $o]: ($false))) & (sK0 = Y0)) | ((~ = f) & (sK1 = Y0))) | ((f = (^[Y1 : $o]: (Y1))) & (sK2 = Y0))) | ((f = (^[Y1 : $o]: ($true))) & (sK3 = Y0)))) @ X0)))) )),
% 0.20/0.36 inference(constrained_superposition,[],[f46,f30])).
% 0.20/0.36 thf(f106,plain,(
% 0.20/0.36 ( ! [X0 : $i] : (($true = ((((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4))) | ((f = (^[Y0 : $o]: (Y0))) & (sK2 = sF4))) | ((f = (^[Y0 : $o]: ($true))) & (sK3 = sF4))))) | ($false = ((((((f = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((~ = f) & (sK1 = X0))) | ((f = (^[Y0 : $o]: (Y0))) & (sK2 = X0))) | ((f = (^[Y0 : $o]: ($true))) & (sK3 = X0)))))) )),
% 0.20/0.36 inference(beta-eta_normalization,[],[f60])).
% 0.20/0.36 thf(f107,plain,(
% 0.20/0.36 ( ! [X0 : $i] : (($true = (((f = (^[Y0 : $o]: ($true))) & (sK3 = sF4)))) | ($false = ((((((f = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((~ = f) & (sK1 = X0))) | ((f = (^[Y0 : $o]: (Y0))) & (sK2 = X0))) | ((f = (^[Y0 : $o]: ($true))) & (sK3 = X0))))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4))) | ((f = (^[Y0 : $o]: (Y0))) & (sK2 = sF4)))))) )),
% 0.20/0.36 inference(or_proxy_clausification,[],[f106])).
% 0.20/0.36 thf(f108,plain,(
% 0.20/0.36 ( ! [X0 : $i] : (($true = ((sK3 = sF4))) | ($false = ((((((f = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((~ = f) & (sK1 = X0))) | ((f = (^[Y0 : $o]: (Y0))) & (sK2 = X0))) | ((f = (^[Y0 : $o]: ($true))) & (sK3 = X0))))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4))) | ((f = (^[Y0 : $o]: (Y0))) & (sK2 = sF4)))))) )),
% 0.20/0.36 inference(and_proxy_clausification,[],[f107])).
% 0.20/0.36 thf(f257,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | ($false = ((((((f = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((~ = f) & (sK1 = X0))) | ((f = (^[Y0 : $o]: (Y0))) & (sK2 = X0))) | ((f = (^[Y0 : $o]: ($true))) & (sK3 = X0))))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4))) | ((f = (^[Y0 : $o]: (Y0))) & (sK2 = sF4)))))) )),
% 0.20/0.36 inference(equality_proxy_clausification,[],[f108])).
% 0.20/0.36 thf(f258,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | ($false = (((f = (^[Y0 : $o]: ($true))) & (sK3 = X0)))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4))) | ((f = (^[Y0 : $o]: (Y0))) & (sK2 = sF4)))))) )),
% 0.20/0.36 inference(or_proxy_clausification,[],[f257])).
% 0.20/0.36 thf(f259,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | ($false = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((~ = f) & (sK1 = X0))) | ((f = (^[Y0 : $o]: (Y0))) & (sK2 = X0))))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4))) | ((f = (^[Y0 : $o]: (Y0))) & (sK2 = sF4)))))) )),
% 0.20/0.36 inference(or_proxy_clausification,[],[f257])).
% 0.20/0.36 thf(f260,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | ($false = (((f = (^[Y0 : $o]: (Y0))) & (sK2 = X0)))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4))) | ((f = (^[Y0 : $o]: (Y0))) & (sK2 = sF4)))))) )),
% 0.20/0.36 inference(or_proxy_clausification,[],[f259])).
% 0.20/0.36 thf(f261,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | ($false = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = X0)) | ((~ = f) & (sK1 = X0))))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4))) | ((f = (^[Y0 : $o]: (Y0))) & (sK2 = sF4)))))) )),
% 0.20/0.36 inference(or_proxy_clausification,[],[f259])).
% 0.20/0.36 thf(f262,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | ($false = (((~ = f) & (sK1 = X0)))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4))) | ((f = (^[Y0 : $o]: (Y0))) & (sK2 = sF4)))))) )),
% 0.20/0.36 inference(or_proxy_clausification,[],[f261])).
% 0.20/0.36 thf(f263,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | ($false = (((f = (^[Y0 : $o]: ($false))) & (sK0 = X0)))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4))) | ((f = (^[Y0 : $o]: (Y0))) & (sK2 = sF4)))))) )),
% 0.20/0.36 inference(or_proxy_clausification,[],[f261])).
% 0.20/0.36 thf(f264,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | ($false = ((sK0 = X0))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4))) | ((f = (^[Y0 : $o]: (Y0))) & (sK2 = sF4))))) | ($false = ((f = (^[Y0 : $o]: ($false)))))) )),
% 0.20/0.36 inference(and_proxy_clausification,[],[f263])).
% 0.20/0.36 thf(f265,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK0 != X0) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4))) | ((f = (^[Y0 : $o]: (Y0))) & (sK2 = sF4))))) | ($false = ((f = (^[Y0 : $o]: ($false)))))) )),
% 0.20/0.36 inference(equality_proxy_clausification,[],[f264])).
% 0.20/0.36 thf(f266,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK0 != X0) | ($true = (((f = (^[Y0 : $o]: (Y0))) & (sK2 = sF4)))) | ($false = ((f = (^[Y0 : $o]: ($false))))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4)))))) )),
% 0.20/0.36 inference(or_proxy_clausification,[],[f265])).
% 0.20/0.36 thf(f267,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK0 != X0) | ($true = ((sK2 = sF4))) | ($false = ((f = (^[Y0 : $o]: ($false))))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4)))))) )),
% 0.20/0.36 inference(and_proxy_clausification,[],[f266])).
% 0.20/0.36 thf(f284,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK0 != X0) | (sK2 = sF4) | ($false = ((f = (^[Y0 : $o]: ($false))))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4)))))) )),
% 0.20/0.36 inference(equality_proxy_clausification,[],[f267])).
% 0.20/0.36 thf(f285,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK0 != X0) | (sK2 = sF4) | (f != (^[Y0 : $o]: ($false))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4)))))) )),
% 0.20/0.36 inference(equality_proxy_clausification,[],[f284])).
% 0.20/0.36 thf(f286,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK0 != X0) | (sK2 = sF4) | (f != (^[Y0 : $o]: ($false))) | ($true = (((~ = f) & (sK1 = sF4)))) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4))))) )),
% 0.20/0.36 inference(or_proxy_clausification,[],[f285])).
% 0.20/0.36 thf(f287,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK0 != X0) | (sK2 = sF4) | (f != (^[Y0 : $o]: ($false))) | ($true = ((sK1 = sF4))) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4))))) )),
% 0.20/0.36 inference(and_proxy_clausification,[],[f286])).
% 0.20/0.36 thf(f294,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK0 != X0) | (sK2 = sF4) | (f != (^[Y0 : $o]: ($false))) | (sK1 = sF4) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4))))) )),
% 0.20/0.36 inference(equality_proxy_clausification,[],[f287])).
% 0.20/0.36 thf(f295,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK0 != X0) | (sK2 = sF4) | (f != (^[Y0 : $o]: ($false))) | (sK1 = sF4) | ($true = ((sK0 = sF4)))) )),
% 0.20/0.36 inference(and_proxy_clausification,[],[f294])).
% 0.20/0.36 thf(f298,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK0 != X0) | (sK2 = sF4) | (f != (^[Y0 : $o]: ($false))) | (sK1 = sF4) | (sK0 = sF4)) )),
% 0.20/0.36 inference(equality_proxy_clausification,[],[f295])).
% 0.20/0.36 thf(f299,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | ($false = ((sK1 = X0))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4))) | ((f = (^[Y0 : $o]: (Y0))) & (sK2 = sF4))))) | ($false = ((~ = f)))) )),
% 0.20/0.36 inference(and_proxy_clausification,[],[f262])).
% 0.20/0.36 thf(f300,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK1 != X0) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4))) | ((f = (^[Y0 : $o]: (Y0))) & (sK2 = sF4))))) | ($false = ((~ = f)))) )),
% 0.20/0.36 inference(equality_proxy_clausification,[],[f299])).
% 0.20/0.36 thf(f301,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK1 != X0) | ($true = (((f = (^[Y0 : $o]: (Y0))) & (sK2 = sF4)))) | ($false = ((~ = f))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4)))))) )),
% 0.20/0.36 inference(or_proxy_clausification,[],[f300])).
% 0.20/0.36 thf(f302,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK1 != X0) | ($true = ((sK2 = sF4))) | ($false = ((~ = f))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4)))))) )),
% 0.20/0.36 inference(and_proxy_clausification,[],[f301])).
% 0.20/0.36 thf(f319,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK1 != X0) | (sK2 = sF4) | ($false = ((~ = f))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4)))))) )),
% 0.20/0.36 inference(equality_proxy_clausification,[],[f302])).
% 0.20/0.36 thf(f320,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK1 != X0) | (sK2 = sF4) | (~ != f) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4)))))) )),
% 0.20/0.36 inference(equality_proxy_clausification,[],[f319])).
% 0.20/0.36 thf(f321,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK1 != X0) | (sK2 = sF4) | (~ != f) | ($true = (((~ = f) & (sK1 = sF4)))) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4))))) )),
% 0.20/0.36 inference(or_proxy_clausification,[],[f320])).
% 0.20/0.36 thf(f322,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK1 != X0) | (sK2 = sF4) | (~ != f) | ($true = ((sK1 = sF4))) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4))))) )),
% 0.20/0.36 inference(and_proxy_clausification,[],[f321])).
% 0.20/0.36 thf(f329,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK1 != X0) | (sK2 = sF4) | (~ != f) | (sK1 = sF4) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4))))) )),
% 0.20/0.36 inference(equality_proxy_clausification,[],[f322])).
% 0.20/0.36 thf(f330,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK1 != X0) | (sK2 = sF4) | (~ != f) | (sK1 = sF4) | ($true = ((sK0 = sF4)))) )),
% 0.20/0.36 inference(and_proxy_clausification,[],[f329])).
% 0.20/0.36 thf(f333,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK1 != X0) | (sK2 = sF4) | (~ != f) | (sK1 = sF4) | (sK0 = sF4)) )),
% 0.20/0.36 inference(equality_proxy_clausification,[],[f330])).
% 0.20/0.36 thf(f334,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | ($false = ((sK2 = X0))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4))) | ((f = (^[Y0 : $o]: (Y0))) & (sK2 = sF4))))) | ($false = ((f = (^[Y0 : $o]: (Y0)))))) )),
% 0.20/0.36 inference(and_proxy_clausification,[],[f260])).
% 0.20/0.36 thf(f335,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK2 != X0) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4))) | ((f = (^[Y0 : $o]: (Y0))) & (sK2 = sF4))))) | ($false = ((f = (^[Y0 : $o]: (Y0)))))) )),
% 0.20/0.36 inference(equality_proxy_clausification,[],[f334])).
% 0.20/0.36 thf(f336,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK2 != X0) | ($true = (((f = (^[Y0 : $o]: (Y0))) & (sK2 = sF4)))) | ($false = ((f = (^[Y0 : $o]: (Y0))))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4)))))) )),
% 0.20/0.36 inference(or_proxy_clausification,[],[f335])).
% 0.20/0.36 thf(f337,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK2 != X0) | ($true = ((sK2 = sF4))) | ($false = ((f = (^[Y0 : $o]: (Y0))))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4)))))) )),
% 0.20/0.36 inference(and_proxy_clausification,[],[f336])).
% 0.20/0.36 thf(f354,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK2 != X0) | (sK2 = sF4) | ($false = ((f = (^[Y0 : $o]: (Y0))))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4)))))) )),
% 0.20/0.36 inference(equality_proxy_clausification,[],[f337])).
% 0.20/0.36 thf(f355,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK2 != X0) | (sK2 = sF4) | (f != (^[Y0 : $o]: (Y0))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4)))))) )),
% 0.20/0.36 inference(equality_proxy_clausification,[],[f354])).
% 0.20/0.36 thf(f356,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK2 != X0) | (sK2 = sF4) | (f != (^[Y0 : $o]: (Y0))) | ($true = (((~ = f) & (sK1 = sF4)))) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4))))) )),
% 0.20/0.36 inference(or_proxy_clausification,[],[f355])).
% 0.20/0.36 thf(f357,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK2 != X0) | (sK2 = sF4) | (f != (^[Y0 : $o]: (Y0))) | ($true = ((sK1 = sF4))) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4))))) )),
% 0.20/0.36 inference(and_proxy_clausification,[],[f356])).
% 0.20/0.36 thf(f364,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK2 != X0) | (sK2 = sF4) | (f != (^[Y0 : $o]: (Y0))) | (sK1 = sF4) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4))))) )),
% 0.20/0.36 inference(equality_proxy_clausification,[],[f357])).
% 0.20/0.36 thf(f365,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK2 != X0) | (sK2 = sF4) | (f != (^[Y0 : $o]: (Y0))) | (sK1 = sF4) | ($true = ((sK0 = sF4)))) )),
% 0.20/0.36 inference(and_proxy_clausification,[],[f364])).
% 0.20/0.36 thf(f368,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK2 != X0) | (sK2 = sF4) | (f != (^[Y0 : $o]: (Y0))) | (sK1 = sF4) | (sK0 = sF4)) )),
% 0.20/0.36 inference(equality_proxy_clausification,[],[f365])).
% 0.20/0.36 thf(f369,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | ($false = ((sK3 = X0))) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4))) | ((f = (^[Y0 : $o]: (Y0))) & (sK2 = sF4))))) | ($false = ((f = (^[Y0 : $o]: ($true)))))) )),
% 0.20/0.36 inference(and_proxy_clausification,[],[f258])).
% 0.20/0.36 thf(f370,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK3 != X0) | ($true = (((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4))) | ((f = (^[Y0 : $o]: (Y0))) & (sK2 = sF4))))) | ($false = ((f = (^[Y0 : $o]: ($true)))))) )),
% 0.20/0.36 inference(equality_proxy_clausification,[],[f369])).
% 0.20/0.36 thf(f371,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK3 != X0) | ($true = (((f = (^[Y0 : $o]: (Y0))) & (sK2 = sF4)))) | ($false = ((f = (^[Y0 : $o]: ($true))))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4)))))) )),
% 0.20/0.36 inference(or_proxy_clausification,[],[f370])).
% 0.20/0.36 thf(f372,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK3 != X0) | ($true = ((sK2 = sF4))) | ($false = ((f = (^[Y0 : $o]: ($true))))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4)))))) )),
% 0.20/0.36 inference(and_proxy_clausification,[],[f371])).
% 0.20/0.36 thf(f389,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK3 != X0) | (sK2 = sF4) | ($false = ((f = (^[Y0 : $o]: ($true))))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4)))))) )),
% 0.20/0.36 inference(equality_proxy_clausification,[],[f372])).
% 0.20/0.36 thf(f390,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK3 != X0) | (sK2 = sF4) | (f != (^[Y0 : $o]: ($true))) | ($true = ((((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4)) | ((~ = f) & (sK1 = sF4)))))) )),
% 0.20/0.36 inference(equality_proxy_clausification,[],[f389])).
% 0.20/0.36 thf(f391,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK3 != X0) | (sK2 = sF4) | (f != (^[Y0 : $o]: ($true))) | ($true = (((~ = f) & (sK1 = sF4)))) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4))))) )),
% 0.20/0.36 inference(or_proxy_clausification,[],[f390])).
% 0.20/0.36 thf(f392,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK3 != X0) | (sK2 = sF4) | (f != (^[Y0 : $o]: ($true))) | ($true = ((sK1 = sF4))) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4))))) )),
% 0.20/0.36 inference(and_proxy_clausification,[],[f391])).
% 0.20/0.36 thf(f399,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK3 != X0) | (sK2 = sF4) | (f != (^[Y0 : $o]: ($true))) | (sK1 = sF4) | ($true = (((f = (^[Y0 : $o]: ($false))) & (sK0 = sF4))))) )),
% 0.20/0.36 inference(equality_proxy_clausification,[],[f392])).
% 0.20/0.36 thf(f400,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK3 != X0) | (sK2 = sF4) | (f != (^[Y0 : $o]: ($true))) | (sK1 = sF4) | ($true = ((sK0 = sF4)))) )),
% 0.20/0.36 inference(and_proxy_clausification,[],[f399])).
% 0.20/0.36 thf(f403,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 = sF4) | (sK3 != X0) | (sK2 = sF4) | (f != (^[Y0 : $o]: ($true))) | (sK1 = sF4) | (sK0 = sF4)) )),
% 0.20/0.36 inference(equality_proxy_clausification,[],[f400])).
% 0.20/0.36 thf(f431,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK0 != X0) | (sK2 = sF4) | (f != (^[Y0 : $o]: ($false))) | (sK1 = sF4) | (sK0 = sF4)) )),
% 0.20/0.36 inference(forward_subsumption_resolution,[],[f298,f26])).
% 0.20/0.36 thf(f435,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK1 != X0) | (sK2 = sF4) | (~ != f) | (sK1 = sF4) | (sK0 = sF4)) )),
% 0.20/0.36 inference(forward_subsumption_resolution,[],[f333,f26])).
% 0.20/0.36 thf(f439,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK2 != X0) | (sK2 = sF4) | (f != (^[Y0 : $o]: (Y0))) | (sK1 = sF4) | (sK0 = sF4)) )),
% 0.20/0.36 inference(forward_subsumption_resolution,[],[f368,f26])).
% 0.20/0.36 thf(f447,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 != X0) | (sK2 = sF4) | (f != (^[Y0 : $o]: ($true))) | (sK1 = sF4) | (sK0 = sF4)) )),
% 0.20/0.36 inference(forward_subsumption_resolution,[],[f403,f26])).
% 0.20/0.36 thf(f449,definition,(
% 0.20/0.36 spl5_1 <=> (~ = f)),
% 0.20/0.36 introduced(definition,[new_symbols(definition,[spl5_1])],[avatar_definition])).
% 0.20/0.36 thf(f450,plain,(
% 0.20/0.36 (~ != f) | spl5_1),
% 0.20/0.36 inference(avatar_component_clause,[],[f449])).
% 0.20/0.36 thf(f453,definition,(
% 0.20/0.36 spl5_2 <=> (f = (^[Y0 : $o]: ($false)))),
% 0.20/0.36 introduced(definition,[new_symbols(definition,[spl5_2])],[avatar_definition])).
% 0.20/0.36 thf(f455,plain,(
% 0.20/0.36 (f != (^[Y0 : $o]: ($false))) | spl5_2),
% 0.20/0.36 inference(avatar_component_clause,[],[f453])).
% 0.20/0.36 thf(f457,definition,(
% 0.20/0.36 spl5_3 <=> (f = (^[Y0 : $o]: (Y0)))),
% 0.20/0.36 introduced(definition,[new_symbols(definition,[spl5_3])],[avatar_definition])).
% 0.20/0.36 thf(f458,plain,(
% 0.20/0.36 (f != (^[Y0 : $o]: (Y0))) | spl5_3),
% 0.20/0.36 inference(avatar_component_clause,[],[f457])).
% 0.20/0.36 thf(f461,definition,(
% 0.20/0.36 spl5_4 <=> ! [X0 : $i] : (sK0 != X0)),
% 0.20/0.36 introduced(definition,[new_symbols(definition,[spl5_4])],[avatar_definition])).
% 0.20/0.36 thf(f462,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK0 != X0)) ) | ~spl5_4),
% 0.20/0.36 inference(avatar_component_clause,[],[f461])).
% 0.20/0.36 thf(f464,definition,(
% 0.20/0.36 spl5_5 <=> (f = (^[Y0 : $o]: ($true)))),
% 0.20/0.36 introduced(definition,[new_symbols(definition,[spl5_5])],[avatar_definition])).
% 0.20/0.36 thf(f465,plain,(
% 0.20/0.36 (f != (^[Y0 : $o]: ($true))) | spl5_5),
% 0.20/0.36 inference(avatar_component_clause,[],[f464])).
% 0.20/0.36 thf(f472,definition,(
% 0.20/0.36 spl5_6 <=> ! [X0 : $i] : (sK1 != X0)),
% 0.20/0.36 introduced(definition,[new_symbols(definition,[spl5_6])],[avatar_definition])).
% 0.20/0.36 thf(f473,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK1 != X0)) ) | ~spl5_6),
% 0.20/0.36 inference(avatar_component_clause,[],[f472])).
% 0.20/0.36 thf(f479,definition,(
% 0.20/0.36 spl5_7 <=> ! [X0 : $i] : (sK2 != X0)),
% 0.20/0.36 introduced(definition,[new_symbols(definition,[spl5_7])],[avatar_definition])).
% 0.20/0.36 thf(f480,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK2 != X0)) ) | ~spl5_7),
% 0.20/0.36 inference(avatar_component_clause,[],[f479])).
% 0.20/0.36 thf(f488,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK0 != X0) | (f != (^[Y0 : $o]: ($false))) | (sK1 = sF4) | (sK0 = sF4)) )),
% 0.20/0.36 inference(forward_subsumption_resolution,[],[f431,f27])).
% 0.20/0.36 thf(f492,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK1 != X0) | (~ != f) | (sK1 = sF4) | (sK0 = sF4)) )),
% 0.20/0.36 inference(forward_subsumption_resolution,[],[f435,f27])).
% 0.20/0.36 thf(f496,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK2 != X0) | (f != (^[Y0 : $o]: (Y0))) | (sK1 = sF4) | (sK0 = sF4)) )),
% 0.20/0.36 inference(forward_subsumption_resolution,[],[f439,f27])).
% 0.20/0.36 thf(f498,definition,(
% 0.20/0.36 spl5_8 <=> ! [X0 : $i] : (sK3 != X0)),
% 0.20/0.36 introduced(definition,[new_symbols(definition,[spl5_8])],[avatar_definition])).
% 0.20/0.36 thf(f499,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 != X0)) ) | ~spl5_8),
% 0.20/0.36 inference(avatar_component_clause,[],[f498])).
% 0.20/0.36 thf(f507,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 != X0) | (f != (^[Y0 : $o]: ($true))) | (sK1 = sF4) | (sK0 = sF4)) )),
% 0.20/0.36 inference(forward_subsumption_resolution,[],[f447,f27])).
% 0.20/0.36 thf(f520,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK0 != X0) | (f != (^[Y0 : $o]: ($false))) | (sK0 = sF4)) )),
% 0.20/0.36 inference(forward_subsumption_resolution,[],[f488,f28])).
% 0.20/0.36 thf(f524,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK1 != X0) | (~ != f) | (sK0 = sF4)) )),
% 0.20/0.36 inference(forward_subsumption_resolution,[],[f492,f28])).
% 0.20/0.36 thf(f528,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK2 != X0) | (f != (^[Y0 : $o]: (Y0))) | (sK0 = sF4)) )),
% 0.20/0.36 inference(forward_subsumption_resolution,[],[f496,f28])).
% 0.20/0.36 thf(f535,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 != X0) | (f != (^[Y0 : $o]: ($true))) | (sK0 = sF4)) )),
% 0.20/0.36 inference(forward_subsumption_resolution,[],[f507,f28])).
% 0.20/0.36 thf(f541,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK0 != X0) | (f != (^[Y0 : $o]: ($false)))) )),
% 0.20/0.36 inference(forward_subsumption_resolution,[],[f520,f29])).
% 0.20/0.36 thf(f544,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK1 != X0) | (~ != f)) )),
% 0.20/0.36 inference(forward_subsumption_resolution,[],[f524,f29])).
% 0.20/0.36 thf(f547,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK2 != X0) | (f != (^[Y0 : $o]: (Y0)))) )),
% 0.20/0.36 inference(forward_subsumption_resolution,[],[f528,f29])).
% 0.20/0.36 thf(f551,plain,(
% 0.20/0.36 ( ! [X0 : $i] : ((sK3 != X0) | (f != (^[Y0 : $o]: ($true)))) )),
% 0.20/0.36 inference(forward_subsumption_resolution,[],[f535,f29])).
% 0.20/0.36 thf(f552,plain,(
% 0.20/0.36 ~spl5_2 | spl5_4),
% 0.20/0.36 inference(avatar_split_clause,[],[f541,f461,f453])).
% 0.20/0.36 thf(f553,plain,(
% 0.20/0.36 ~spl5_1 | spl5_6),
% 0.20/0.36 inference(avatar_split_clause,[],[f544,f472,f449])).
% 0.20/0.36 thf(f554,plain,(
% 0.20/0.36 ~spl5_3 | spl5_7),
% 0.20/0.36 inference(avatar_split_clause,[],[f547,f479,f457])).
% 0.20/0.36 thf(f555,plain,(
% 0.20/0.36 ~spl5_5 | spl5_8),
% 0.20/0.36 inference(avatar_split_clause,[],[f551,f498,f464])).
% 0.20/0.36 thf(f556,plain,(
% 0.20/0.36 (((~ sK6)) != ((f @ sK6))) | spl5_1),
% 0.20/0.36 inference(negative_extensionality,[],[f450])).
% 0.20/0.36 thf(f557,plain,(
% 0.20/0.36 ($true = ((~ sK6))) | ($true = ((f @ sK6))) | spl5_1),
% 0.20/0.36 inference(xor_proxy_clausification,[],[f556])).
% 0.20/0.36 thf(f558,plain,(
% 0.20/0.36 ($false = ((~ sK6))) | ($false = ((f @ sK6))) | spl5_1),
% 0.20/0.36 inference(xor_proxy_clausification,[],[f556])).
% 0.20/0.36 thf(f559,plain,(
% 0.20/0.36 ($true = sK6) | ($false = ((f @ sK6))) | spl5_1),
% 0.20/0.36 inference(not_proxy_clausification,[],[f558])).
% 0.20/0.36 thf(f560,plain,(
% 0.20/0.36 ($false = sK6) | ($true = ((f @ sK6))) | spl5_1),
% 0.20/0.36 inference(not_proxy_clausification,[],[f557])).
% 0.20/0.36 thf(f562,definition,(
% 0.20/0.36 spl5_9 <=> ($false = ((f @ sK6)))),
% 0.20/0.36 introduced(definition,[new_symbols(definition,[spl5_9])],[avatar_definition])).
% 0.20/0.36 thf(f564,plain,(
% 0.20/0.36 ($false = ((f @ sK6))) | ~spl5_9),
% 0.20/0.36 inference(avatar_component_clause,[],[f562])).
% 0.20/0.36 thf(f566,definition,(
% 0.20/0.36 spl5_10 <=> ($true = sK6)),
% 0.20/0.36 introduced(definition,[new_symbols(definition,[spl5_10])],[avatar_definition])).
% 0.20/0.36 thf(f568,plain,(
% 0.20/0.36 ($true = sK6) | ~spl5_10),
% 0.20/0.36 inference(avatar_component_clause,[],[f566])).
% 0.20/0.36 thf(f569,plain,(
% 0.20/0.36 spl5_9 | spl5_10 | spl5_1),
% 0.20/0.36 inference(avatar_split_clause,[],[f559,f449,f566,f562])).
% 0.20/0.36 thf(f571,definition,(
% 0.20/0.36 spl5_11 <=> ($true = ((f @ sK6)))),
% 0.20/0.36 introduced(definition,[new_symbols(definition,[spl5_11])],[avatar_definition])).
% 0.20/0.36 thf(f572,plain,(
% 0.20/0.36 ($true != ((f @ sK6))) | spl5_11),
% 0.20/0.36 inference(avatar_component_clause,[],[f571])).
% 0.20/0.36 thf(f573,plain,(
% 0.20/0.36 ($true = ((f @ sK6))) | ~spl5_11),
% 0.20/0.36 inference(avatar_component_clause,[],[f571])).
% 0.20/0.36 thf(f575,definition,(
% 0.20/0.36 spl5_12 <=> ($false = sK6)),
% 0.20/0.36 introduced(definition,[new_symbols(definition,[spl5_12])],[avatar_definition])).
% 0.20/0.36 thf(f577,plain,(
% 0.20/0.36 ($false = sK6) | ~spl5_12),
% 0.20/0.36 inference(avatar_component_clause,[],[f575])).
% 0.20/0.36 thf(f578,plain,(
% 0.20/0.36 spl5_11 | spl5_12 | spl5_1),
% 0.20/0.36 inference(avatar_split_clause,[],[f560,f449,f575,f571])).
% 0.20/0.36 thf(f666,plain,(
% 0.20/0.36 $false | ~spl5_6),
% 0.20/0.36 inference(equality_resolution,[],[f473])).
% 0.20/0.36 thf(f667,plain,(
% 0.20/0.36 ~spl5_6),
% 0.20/0.36 inference(avatar_contradiction_clause,[],[f666])).
% 0.20/0.36 thf(f668,plain,(
% 0.20/0.36 ($true = $false) | (~spl5_9 | ~spl5_11)),
% 0.20/0.36 inference(forward_demodulation,[],[f573,f564])).
% 0.20/0.36 thf(f669,plain,(
% 0.20/0.36 $false | (~spl5_9 | ~spl5_11)),
% 0.20/0.36 inference(trivial_inequality_removal,[],[f668])).
% 0.20/0.36 thf(f670,plain,(
% 0.20/0.36 ~spl5_9 | ~spl5_11),
% 0.20/0.36 inference(avatar_contradiction_clause,[],[f669])).
% 0.20/0.36 thf(f671,plain,(
% 0.20/0.36 ($true = ((f @ $true))) | (~spl5_10 | ~spl5_11)),
% 0.20/0.36 inference(forward_demodulation,[],[f573,f568])).
% 0.20/0.36 thf(f1210,plain,(
% 0.20/0.36 (((f @ sK8)) != (((^[Y0 : $o]: ($false)) @ sK8))) | spl5_2),
% 0.20/0.36 inference(negative_extensionality,[],[f455])).
% 0.20/0.36 thf(f1211,plain,(
% 0.20/0.36 ($true = ((f @ sK8))) | ($true = (((^[Y0 : $o]: ($false)) @ sK8))) | spl5_2),
% 0.20/0.36 inference(xor_proxy_clausification,[],[f1210])).
% 0.20/0.36 thf(f1214,plain,(
% 0.20/0.36 ($true = ((f @ sK8))) | ($true = $false) | spl5_2),
% 0.20/0.36 inference(beta-eta_normalization,[],[f1211])).
% 0.20/0.36 thf(f1215,plain,(
% 0.20/0.36 ($true = ((f @ sK8))) | spl5_2),
% 0.20/0.36 inference(trivial_inequality_removal,[],[f1214])).
% 0.20/0.36 thf(f1243,plain,(
% 0.20/0.36 (((f @ sK9)) != (((^[Y0 : $o]: ($true)) @ sK9))) | spl5_5),
% 0.20/0.36 inference(negative_extensionality,[],[f465])).
% 0.20/0.36 thf(f1245,plain,(
% 0.20/0.36 ($false = ((f @ sK9))) | ($false = (((^[Y0 : $o]: ($true)) @ sK9))) | spl5_5),
% 0.20/0.36 inference(xor_proxy_clausification,[],[f1243])).
% 0.20/0.36 thf(f1246,plain,(
% 0.20/0.36 ($false = ((f @ sK9))) | ($true = $false) | spl5_5),
% 0.20/0.36 inference(beta-eta_normalization,[],[f1245])).
% 0.20/0.36 thf(f1247,plain,(
% 0.20/0.36 ($false = ((f @ sK9))) | spl5_5),
% 0.20/0.36 inference(trivial_inequality_removal,[],[f1246])).
% 0.20/0.36 thf(f1251,plain,(
% 0.20/0.36 ( ! [X0 : $i] : (($true = ((f @ $false))) | ($true = (((^[Y0 : $i]: (sK8)) @ X0)))) ) | spl5_2),
% 0.20/0.36 inference(constrained_superposition,[],[f1215,f50])).
% 0.20/0.36 thf(f1278,plain,(
% 0.20/0.36 ($true = ((f @ $false))) | ($true = sK8) | spl5_2),
% 0.20/0.36 inference(beta-eta_normalization,[],[f1251])).
% 0.20/0.36 thf(f1281,definition,(
% 0.20/0.36 spl5_17 <=> ($true = sK8)),
% 0.20/0.36 introduced(definition,[new_symbols(definition,[spl5_17])],[avatar_definition])).
% 0.20/0.36 thf(f1283,plain,(
% 0.20/0.36 ($true = sK8) | ~spl5_17),
% 0.20/0.36 inference(avatar_component_clause,[],[f1281])).
% 0.20/0.36 thf(f1285,definition,(
% 0.20/0.36 spl5_18 <=> ($true = ((f @ $false)))),
% 0.20/0.36 introduced(definition,[new_symbols(definition,[spl5_18])],[avatar_definition])).
% 0.20/0.36 thf(f1286,plain,(
% 0.20/0.36 ($true != ((f @ $false))) | spl5_18),
% 0.20/0.36 inference(avatar_component_clause,[],[f1285])).
% 0.20/0.36 thf(f1287,plain,(
% 0.20/0.36 ($true = ((f @ $false))) | ~spl5_18),
% 0.20/0.36 inference(avatar_component_clause,[],[f1285])).
% 0.20/0.36 thf(f1289,plain,(
% 0.20/0.36 spl5_17 | spl5_18 | spl5_2),
% 0.20/0.36 inference(avatar_split_clause,[],[f1278,f453,f1285,f1281])).
% 0.20/0.36 thf(f1290,plain,(
% 0.20/0.36 $false | ~spl5_4),
% 0.20/0.36 inference(equality_resolution,[],[f462])).
% 0.20/0.36 thf(f1291,plain,(
% 0.20/0.36 ~spl5_4),
% 0.20/0.36 inference(avatar_contradiction_clause,[],[f1290])).
% 0.20/0.36 thf(f1325,plain,(
% 0.20/0.36 ($true = ((f @ $true))) | (spl5_2 | ~spl5_17)),
% 0.20/0.36 inference(constrained_superposition,[],[f1215,f1283])).
% 0.20/0.36 thf(f1352,plain,(
% 0.20/0.36 (((f @ sK11)) != (((^[Y0 : $o]: (Y0)) @ sK11))) | spl5_3),
% 0.20/0.36 inference(negative_extensionality,[],[f458])).
% 0.20/0.36 thf(f1353,plain,(
% 0.20/0.36 ($true = ((f @ sK11))) | ($true = (((^[Y0 : $o]: (Y0)) @ sK11))) | spl5_3),
% 0.20/0.36 inference(xor_proxy_clausification,[],[f1352])).
% 0.20/0.36 thf(f1354,plain,(
% 0.20/0.36 ($false = ((f @ sK11))) | ($false = (((^[Y0 : $o]: (Y0)) @ sK11))) | spl5_3),
% 0.20/0.36 inference(xor_proxy_clausification,[],[f1352])).
% 0.20/0.36 thf(f1355,plain,(
% 0.20/0.36 ($false = ((f @ sK11))) | ($false = sK11) | spl5_3),
% 0.20/0.36 inference(beta-eta_normalization,[],[f1354])).
% 0.20/0.36 thf(f1356,plain,(
% 0.20/0.36 ($true = ((f @ sK11))) | ($true = sK11) | spl5_3),
% 0.20/0.36 inference(beta-eta_normalization,[],[f1353])).
% 0.20/0.36 thf(f1358,definition,(
% 0.20/0.36 spl5_19 <=> ($false = sK11)),
% 0.20/0.36 introduced(definition,[new_symbols(definition,[spl5_19])],[avatar_definition])).
% 0.20/0.36 thf(f1359,plain,(
% 0.20/0.36 ($false != sK11) | spl5_19),
% 0.20/0.36 inference(avatar_component_clause,[],[f1358])).
% 0.20/0.36 thf(f1360,plain,(
% 0.20/0.36 ($false = sK11) | ~spl5_19),
% 0.20/0.36 inference(avatar_component_clause,[],[f1358])).
% 0.20/0.36 thf(f1362,definition,(
% 0.20/0.36 spl5_20 <=> ($false = ((f @ sK11)))),
% 0.20/0.36 introduced(definition,[new_symbols(definition,[spl5_20])],[avatar_definition])).
% 0.20/0.36 thf(f1364,plain,(
% 0.20/0.36 ($false = ((f @ sK11))) | ~spl5_20),
% 0.20/0.36 inference(avatar_component_clause,[],[f1362])).
% 0.20/0.36 thf(f1365,plain,(
% 0.20/0.36 spl5_19 | spl5_20 | spl5_3),
% 0.20/0.36 inference(avatar_split_clause,[],[f1355,f457,f1362,f1358])).
% 0.20/0.36 thf(f1367,definition,(
% 0.20/0.36 spl5_21 <=> ($true = sK11)),
% 0.20/0.36 introduced(definition,[new_symbols(definition,[spl5_21])],[avatar_definition])).
% 0.20/0.36 thf(f1369,plain,(
% 0.20/0.36 ($true = sK11) | ~spl5_21),
% 0.20/0.36 inference(avatar_component_clause,[],[f1367])).
% 0.20/0.36 thf(f1371,definition,(
% 0.20/0.36 spl5_22 <=> ($true = ((f @ sK11)))),
% 0.20/0.36 introduced(definition,[new_symbols(definition,[spl5_22])],[avatar_definition])).
% 0.20/0.36 thf(f1373,plain,(
% 0.20/0.36 ($true = ((f @ sK11))) | ~spl5_22),
% 0.20/0.36 inference(avatar_component_clause,[],[f1371])).
% 0.20/0.36 thf(f1374,plain,(
% 0.20/0.36 spl5_21 | spl5_22 | spl5_3),
% 0.20/0.36 inference(avatar_split_clause,[],[f1356,f457,f1371,f1367])).
% 0.20/0.36 thf(f1375,plain,(
% 0.20/0.36 $false | ~spl5_7),
% 0.20/0.36 inference(equality_resolution,[],[f480])).
% 0.20/0.36 thf(f1376,plain,(
% 0.20/0.36 ~spl5_7),
% 0.20/0.36 inference(avatar_contradiction_clause,[],[f1375])).
% 0.20/0.36 thf(f1377,plain,(
% 0.20/0.36 ($true = $false) | (~spl5_19 | ~spl5_21)),
% 0.20/0.36 inference(forward_demodulation,[],[f1369,f1360])).
% 0.20/0.36 thf(f1378,plain,(
% 0.20/0.36 $false | (~spl5_19 | ~spl5_21)),
% 0.20/0.36 inference(trivial_inequality_removal,[],[f1377])).
% 0.20/0.36 thf(f1379,plain,(
% 0.20/0.36 ~spl5_19 | ~spl5_21),
% 0.20/0.36 inference(avatar_contradiction_clause,[],[f1378])).
% 0.20/0.36 thf(f1380,plain,(
% 0.20/0.36 (((f @ sK12)) != (((^[Y0 : $o]: (Y0)) @ sK12))) | spl5_3),
% 0.20/0.36 inference(negative_extensionality,[],[f458])).
% 0.20/0.36 thf(f1381,plain,(
% 0.20/0.36 ($true = ((f @ sK12))) | ($true = (((^[Y0 : $o]: (Y0)) @ sK12))) | spl5_3),
% 0.20/0.36 inference(xor_proxy_clausification,[],[f1380])).
% 0.20/0.36 thf(f1382,plain,(
% 0.20/0.36 ($false = ((f @ sK12))) | ($false = (((^[Y0 : $o]: (Y0)) @ sK12))) | spl5_3),
% 0.20/0.36 inference(xor_proxy_clausification,[],[f1380])).
% 0.20/0.36 thf(f1383,plain,(
% 0.20/0.36 ($false = ((f @ sK12))) | ($false = sK12) | spl5_3),
% 0.20/0.36 inference(beta-eta_normalization,[],[f1382])).
% 0.20/0.36 thf(f1384,plain,(
% 0.20/0.36 ($true = ((f @ sK12))) | ($true = sK12) | spl5_3),
% 0.20/0.36 inference(beta-eta_normalization,[],[f1381])).
% 0.20/0.36 thf(f1386,definition,(
% 0.20/0.36 spl5_23 <=> ($false = sK12)),
% 0.20/0.36 introduced(definition,[new_symbols(definition,[spl5_23])],[avatar_definition])).
% 0.20/0.36 thf(f1387,plain,(
% 0.20/0.36 ($false != sK12) | spl5_23),
% 0.20/0.36 inference(avatar_component_clause,[],[f1386])).
% 0.20/0.36 thf(f1388,plain,(
% 0.20/0.36 ($false = sK12) | ~spl5_23),
% 0.20/0.36 inference(avatar_component_clause,[],[f1386])).
% 0.20/0.36 thf(f1390,definition,(
% 0.20/0.36 spl5_24 <=> ($false = ((f @ sK12)))),
% 0.20/0.36 introduced(definition,[new_symbols(definition,[spl5_24])],[avatar_definition])).
% 0.20/0.36 thf(f1392,plain,(
% 0.20/0.36 ($false = ((f @ sK12))) | ~spl5_24),
% 0.20/0.36 inference(avatar_component_clause,[],[f1390])).
% 0.20/0.36 thf(f1393,plain,(
% 0.20/0.36 spl5_23 | spl5_24 | spl5_3),
% 0.20/0.36 inference(avatar_split_clause,[],[f1383,f457,f1390,f1386])).
% 0.20/0.36 thf(f1395,definition,(
% 0.20/0.36 spl5_25 <=> ($true = sK12)),
% 0.20/0.36 introduced(definition,[new_symbols(definition,[spl5_25])],[avatar_definition])).
% 0.20/0.36 thf(f1397,plain,(
% 0.20/0.36 ($true = sK12) | ~spl5_25),
% 0.20/0.36 inference(avatar_component_clause,[],[f1395])).
% 0.20/0.36 thf(f1399,definition,(
% 0.20/0.36 spl5_26 <=> ($true = ((f @ sK12)))),
% 0.20/0.36 introduced(definition,[new_symbols(definition,[spl5_26])],[avatar_definition])).
% 0.20/0.36 thf(f1401,plain,(
% 0.20/0.36 ($true = ((f @ sK12))) | ~spl5_26),
% 0.20/0.36 inference(avatar_component_clause,[],[f1399])).
% 0.20/0.36 thf(f1402,plain,(
% 0.20/0.36 spl5_25 | spl5_26 | spl5_3),
% 0.20/0.36 inference(avatar_split_clause,[],[f1384,f457,f1399,f1395])).
% 0.20/0.36 thf(f1403,plain,(
% 0.20/0.36 ($true = $false) | (~spl5_23 | ~spl5_25)),
% 0.20/0.36 inference(forward_demodulation,[],[f1397,f1388])).
% 0.20/0.36 thf(f1404,plain,(
% 0.20/0.36 $false | (~spl5_23 | ~spl5_25)),
% 0.20/0.36 inference(trivial_inequality_removal,[],[f1403])).
% 0.20/0.36 thf(f1405,plain,(
% 0.20/0.36 ~spl5_23 | ~spl5_25),
% 0.20/0.36 inference(avatar_contradiction_clause,[],[f1404])).
% 0.20/0.36 thf(f1410,plain,(
% 0.20/0.36 ($false != $false) | ($true = (((^[Y0 : $i]: (sK11)) @ (eps @ (^[Y0 : $i]: (sK11)))))) | spl5_19),
% 0.20/0.36 inference(constrained_superposition,[],[f1359,f46])).
% 0.20/0.36 thf(f1411,plain,(
% 0.20/0.36 ($true = (((^[Y0 : $i]: (sK11)) @ (eps @ (^[Y0 : $i]: (sK11)))))) | spl5_19),
% 0.20/0.36 inference(trivial_inequality_removal,[],[f1410])).
% 0.20/0.36 thf(f1412,plain,(
% 0.20/0.36 ($true = sK11) | spl5_19),
% 0.20/0.36 inference(beta-eta_normalization,[],[f1411])).
% 0.20/0.36 thf(f1444,plain,(
% 0.20/0.36 ($false != $false) | ($true = (((^[Y0 : $i]: (sK12)) @ (eps @ (^[Y0 : $i]: (sK12)))))) | spl5_23),
% 0.20/0.36 inference(constrained_superposition,[],[f1387,f46])).
% 0.20/0.36 thf(f1445,plain,(
% 0.20/0.36 ($true = (((^[Y0 : $i]: (sK12)) @ (eps @ (^[Y0 : $i]: (sK12)))))) | spl5_23),
% 0.20/0.36 inference(trivial_inequality_removal,[],[f1444])).
% 0.20/0.36 thf(f1446,plain,(
% 0.20/0.36 ($true = sK12) | spl5_23),
% 0.20/0.36 inference(beta-eta_normalization,[],[f1445])).
% 0.20/0.36 thf(f1475,plain,(
% 0.20/0.36 ( ! [X0 : $i] : (($false = ((f @ $true))) | ($false = (((^[Y0 : $i]: (sK9)) @ X0)))) ) | spl5_5),
% 0.20/0.36 inference(constrained_superposition,[],[f1247,f46])).
% 0.20/0.36 thf(f1506,plain,(
% 0.20/0.36 ($false = ((f @ $true))) | ($false = sK9) | spl5_5),
% 0.20/0.36 inference(beta-eta_normalization,[],[f1475])).
% 0.20/0.36 thf(f1512,definition,(
% 0.20/0.36 spl5_28 <=> ($false = ((f @ $false)))),
% 0.20/0.36 introduced(definition,[new_symbols(definition,[spl5_28])],[avatar_definition])).
% 0.20/0.36 thf(f1514,plain,(
% 0.20/0.36 ($false = ((f @ $false))) | ~spl5_28),
% 0.20/0.36 inference(avatar_component_clause,[],[f1512])).
% 0.20/0.36 thf(f1519,plain,(
% 0.20/0.36 ($true = $false) | ($false = sK9) | (spl5_5 | ~spl5_10 | ~spl5_11)),
% 0.20/0.36 inference(forward_demodulation,[],[f1506,f671])).
% 0.20/0.36 thf(f1523,plain,(
% 0.20/0.36 $false | ~spl5_8),
% 0.20/0.36 inference(equality_resolution,[],[f499])).
% 0.20/0.36 thf(f1524,plain,(
% 0.20/0.36 ~spl5_8),
% 0.20/0.36 inference(avatar_contradiction_clause,[],[f1523])).
% 0.20/0.36 thf(f1525,plain,(
% 0.20/0.36 ($false = sK9) | (spl5_5 | ~spl5_10 | ~spl5_11)),
% 0.20/0.36 inference(trivial_inequality_removal,[],[f1519])).
% 0.20/0.36 thf(f1528,plain,(
% 0.20/0.36 ($false = ((f @ $false))) | (spl5_5 | ~spl5_10 | ~spl5_11)),
% 0.20/0.36 inference(forward_demodulation,[],[f1247,f1525])).
% 0.20/0.36 thf(f1532,plain,(
% 0.20/0.36 spl5_28 | spl5_5 | ~spl5_10 | ~spl5_11),
% 0.20/0.36 inference(avatar_split_clause,[],[f1528,f571,f566,f464,f1512])).
% 0.20/0.36 thf(f1604,plain,(
% 0.20/0.36 ($false = ((f @ $true))) | (~spl5_20 | ~spl5_21)),
% 0.20/0.36 inference(constrained_superposition,[],[f1364,f1369])).
% 0.20/0.36 thf(f1661,plain,(
% 0.20/0.36 ($false = ((f @ $true))) | (~spl5_24 | ~spl5_25)),
% 0.20/0.36 inference(constrained_superposition,[],[f1392,f1397])).
% 0.20/0.36 thf(f1753,plain,(
% 0.20/0.36 ($true = $false) | (~spl5_10 | ~spl5_11 | ~spl5_20 | ~spl5_21)),
% 0.20/0.36 inference(constrained_superposition,[],[f1604,f671])).
% 0.20/0.36 thf(f1773,plain,(
% 0.20/0.36 $false | (~spl5_10 | ~spl5_11 | ~spl5_20 | ~spl5_21)),
% 0.20/0.36 inference(trivial_inequality_removal,[],[f1753])).
% 0.20/0.36 thf(f1774,plain,(
% 0.20/0.36 ~spl5_10 | ~spl5_11 | ~spl5_20 | ~spl5_21),
% 0.20/0.36 inference(avatar_contradiction_clause,[],[f1773])).
% 0.20/0.36 thf(f1783,plain,(
% 0.20/0.36 ($true = ((f @ $false))) | (~spl5_19 | ~spl5_22)),
% 0.20/0.36 inference(forward_demodulation,[],[f1373,f1360])).
% 0.20/0.36 thf(f1784,plain,(
% 0.20/0.36 ($true = $false) | (~spl5_19 | ~spl5_22 | ~spl5_28)),
% 0.20/0.36 inference(forward_demodulation,[],[f1783,f1514])).
% 0.20/0.36 thf(f1785,plain,(
% 0.20/0.36 $false | (~spl5_19 | ~spl5_22 | ~spl5_28)),
% 0.20/0.36 inference(trivial_inequality_removal,[],[f1784])).
% 0.20/0.36 thf(f1786,plain,(
% 0.20/0.36 ~spl5_19 | ~spl5_22 | ~spl5_28),
% 0.20/0.36 inference(avatar_contradiction_clause,[],[f1785])).
% 0.20/0.36 thf(f1819,plain,(
% 0.20/0.36 ($true = $false) | (spl5_2 | ~spl5_17 | ~spl5_24 | ~spl5_25)),
% 0.20/0.36 inference(forward_demodulation,[],[f1325,f1661])).
% 0.20/0.36 thf(f1820,plain,(
% 0.20/0.36 $false | (spl5_2 | ~spl5_17 | ~spl5_24 | ~spl5_25)),
% 0.20/0.36 inference(trivial_inequality_removal,[],[f1819])).
% 0.20/0.36 thf(f1821,plain,(
% 0.20/0.36 spl5_2 | ~spl5_17 | ~spl5_24 | ~spl5_25),
% 0.20/0.36 inference(avatar_contradiction_clause,[],[f1820])).
% 0.20/0.36 thf(f1843,plain,(
% 0.20/0.36 ($true = $false) | (~spl5_10 | ~spl5_12)),
% 0.20/0.36 inference(constrained_superposition,[],[f577,f568])).
% 0.20/0.36 thf(f1863,plain,(
% 0.20/0.36 $false | (~spl5_10 | ~spl5_12)),
% 0.20/0.36 inference(trivial_inequality_removal,[],[f1843])).
% 0.20/0.36 thf(f1864,plain,(
% 0.20/0.36 ~spl5_10 | ~spl5_12),
% 0.20/0.36 inference(avatar_contradiction_clause,[],[f1863])).
% 0.20/0.36 thf(f1871,plain,(
% 0.20/0.36 ($true != ((f @ $false))) | (spl5_11 | ~spl5_12)),
% 0.20/0.36 inference(forward_demodulation,[],[f572,f577])).
% 0.20/0.36 thf(f1873,plain,(
% 0.20/0.36 $false | (spl5_11 | ~spl5_12 | ~spl5_18)),
% 0.20/0.36 inference(forward_subsumption_resolution,[],[f1871,f1287])).
% 0.20/0.36 thf(f1874,plain,(
% 0.20/0.36 spl5_11 | ~spl5_12 | ~spl5_18),
% 0.20/0.36 inference(avatar_contradiction_clause,[],[f1873])).
% 0.20/0.36 thf(f1879,plain,(
% 0.20/0.36 spl5_21 | spl5_19),
% 0.20/0.36 inference(avatar_split_clause,[],[f1412,f1358,f1367])).
% 0.20/0.36 thf(f1881,plain,(
% 0.20/0.36 ($true = ((f @ $false))) | (~spl5_23 | ~spl5_26)),
% 0.20/0.36 inference(forward_demodulation,[],[f1401,f1388])).
% 0.20/0.36 thf(f1892,plain,(
% 0.20/0.36 $false | (spl5_18 | ~spl5_23 | ~spl5_26)),
% 0.20/0.36 inference(forward_subsumption_resolution,[],[f1881,f1286])).
% 0.20/0.36 thf(f1893,plain,(
% 0.20/0.36 spl5_18 | ~spl5_23 | ~spl5_26),
% 0.20/0.36 inference(avatar_contradiction_clause,[],[f1892])).
% 0.20/0.36 thf(f1895,plain,(
% 0.20/0.36 spl5_25 | spl5_23),
% 0.20/0.36 inference(avatar_split_clause,[],[f1446,f1386,f1395])).
% 0.20/0.36 cnf(s29, plain, ~spl5_2 | spl5_4, inference(sat_conversion,[],[f552])).
% 0.20/0.36 cnf(s30, plain, ~spl5_1 | spl5_6, inference(sat_conversion,[],[f553])).
% 0.20/0.36 cnf(s31, plain, ~spl5_3 | spl5_7, inference(sat_conversion,[],[f554])).
% 0.20/0.36 cnf(s32, plain, ~spl5_5 | spl5_8, inference(sat_conversion,[],[f555])).
% 0.20/0.36 cnf(s33, plain, spl5_1 | spl5_9 | spl5_10, inference(sat_conversion,[],[f569])).
% 0.20/0.36 cnf(s34, plain, spl5_1 | spl5_11 | spl5_12, inference(sat_conversion,[],[f578])).
% 0.20/0.36 cnf(s35, plain, ~spl5_6, inference(sat_conversion,[],[f667])).
% 0.20/0.36 cnf(s36, plain, ~spl5_9 | ~spl5_11, inference(sat_conversion,[],[f670])).
% 0.20/0.36 cnf(s41, plain, spl5_2 | spl5_17 | spl5_18, inference(sat_conversion,[],[f1289])).
% 0.20/0.36 cnf(s42, plain, ~spl5_4, inference(sat_conversion,[],[f1291])).
% 0.20/0.36 cnf(s43, plain, spl5_3 | spl5_19 | spl5_20, inference(sat_conversion,[],[f1365])).
% 0.20/0.36 cnf(s44, plain, spl5_3 | spl5_21 | spl5_22, inference(sat_conversion,[],[f1374])).
% 0.20/0.36 cnf(s45, plain, ~spl5_7, inference(sat_conversion,[],[f1376])).
% 0.20/0.36 cnf(s46, plain, ~spl5_19 | ~spl5_21, inference(sat_conversion,[],[f1379])).
% 0.20/0.36 cnf(s47, plain, spl5_3 | spl5_23 | spl5_24, inference(sat_conversion,[],[f1393])).
% 0.20/0.36 cnf(s48, plain, spl5_3 | spl5_25 | spl5_26, inference(sat_conversion,[],[f1402])).
% 0.20/0.36 cnf(s49, plain, ~spl5_23 | ~spl5_25, inference(sat_conversion,[],[f1405])).
% 0.20/0.36 cnf(s52, plain, ~spl5_8, inference(sat_conversion,[],[f1524])).
% 0.20/0.36 cnf(s54, plain, spl5_5 | ~spl5_10 | ~spl5_11 | spl5_28, inference(sat_conversion,[],[f1532])).
% 0.20/0.36 cnf(s56, plain, ~spl5_10 | ~spl5_11 | ~spl5_20 | ~spl5_21, inference(sat_conversion,[],[f1774])).
% 0.20/0.36 cnf(s57, plain, ~spl5_19 | ~spl5_22 | ~spl5_28, inference(sat_conversion,[],[f1786])).
% 0.20/0.36 cnf(s68, plain, spl5_2 | ~spl5_17 | ~spl5_24 | ~spl5_25, inference(sat_conversion,[],[f1821])).
% 0.20/0.36 cnf(s73, plain, ~spl5_10 | ~spl5_12, inference(sat_conversion,[],[f1864])).
% 0.20/0.36 cnf(s74, plain, spl5_11 | ~spl5_12 | ~spl5_18, inference(sat_conversion,[],[f1874])).
% 0.20/0.36 cnf(s76, plain, spl5_19 | spl5_21, inference(sat_conversion,[],[f1879])).
% 0.20/0.36 cnf(s82, plain, spl5_18 | ~spl5_23 | ~spl5_26, inference(sat_conversion,[],[f1893])).
% 0.20/0.36 cnf(s83, plain, spl5_23 | spl5_25, inference(sat_conversion,[],[f1895])).
% 0.20/0.36 cnf(s86, plain, ~spl5_5, inference(rat,[],[s32,s52])).
% 0.20/0.36 cnf(s87, plain, ~spl5_3, inference(rat,[],[s31,s45])).
% 0.20/0.36 cnf(s88, plain, ~spl5_1, inference(rat,[],[s30,s35])).
% 0.20/0.36 cnf(s89, plain, ~spl5_2, inference(rat,[],[s29,s42])).
% 0.20/0.36 cnf(s90, plain, spl5_19 | ~spl5_10, inference(rat,[],[s56,s43,s76,s34,s73,s87,s88])).
% 0.20/0.36 cnf(s91, plain, ~spl5_11 | ~spl5_10, inference(rat,[],[s44,s57,s46,s90,s54,s86,s87])).
% 0.20/0.36 cnf(s92, plain, ~spl5_10, inference(rat,[],[s91,s34,s73,s88])).
% 0.20/0.36 cnf(s93, plain, spl5_9, inference(rat,[],[s33,s88,s92])).
% 0.20/0.36 cnf(s94, plain, ~spl5_11, inference(rat,[],[s36,s93])).
% 0.20/0.36 cnf(s95, plain, spl5_12, inference(rat,[],[s34,s88,s94])).
% 0.20/0.36 cnf(s97, plain, ~spl5_18, inference(rat,[],[s74,s94,s95])).
% 0.20/0.36 cnf(s99, plain, spl5_17, inference(rat,[],[s41,s89,s97])).
% 0.20/0.36 cnf(s101, plain, ~spl5_23, inference(rat,[],[s48,s82,s49,s87,s97])).
% 0.20/0.36 cnf(s102, plain, spl5_25, inference(rat,[],[s83,s101])).
% 0.20/0.36 cnf(s103, plain, spl5_24, inference(rat,[],[s47,s87,s101])).
% 0.20/0.36 cnf(s105, plain, $false, inference(rat,[],[s68,s99,s89,s102,s103])).
% 0.20/0.36 thf(f1899,plain,(
% 0.20/0.36 $false),
% 0.20/0.36 inference(avatar_sat_refutation,[],[s105])).
% 0.20/0.36 % SZS output end Proof for theBenchmark
% 0.20/0.36 % (1098096)------------------------------
% 0.20/0.36 % (1098096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.36 % (1098096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.36 % (1098096)CaDiCaL version: 2.1.3
% 0.20/0.36 % (1098096)Termination reason: Refutation
% 0.20/0.36 % (1098096)Time elapsed: 0.042 s
% 0.20/0.36 % (1098096)Peak memory usage: 13 MB
% 0.20/0.36 % (1098096)Instructions burned: 70 (million)
% 0.20/0.36 % (1098069)Success in time 0.114 s
% 0.20/0.36 % Vampire exiting
%------------------------------------------------------------------------------