%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEV094^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n007.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:38:59 AM UTC 2026
% Result : Theorem 7.39s 1.50s
% Output : Refutation 7.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEV094^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.27 % Computer : n007.cluster.edu
% 0.11/0.27 % Model : x86_64 x86_64
% 0.11/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.27 % Memory : 8046.5625MB
% 0.11/0.27 % OS : Linux 6.8.0-71-generic
% 0.11/0.27 % CPULimit : 300
% 0.11/0.27 % WCLimit : 300
% 0.11/0.27 % DateTime : Tue Sep 29 15:07:56 UTC 2026
% 0.11/0.27 % CPUTime :
% 0.11/0.27 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.27/0.32 Running first-order model finding
% 0.27/0.32 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.39/1.50 % (3481820)Will run a generic schedule for satisfiability detection.
% 7.39/1.50 % (3481831)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3478840308:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.39/1.50 % (3481826)% WARNING: option uhcvi not known.
% 7.39/1.50 % (3481826)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4173562116:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.39/1.50 % (3481827)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1973819972:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.39/1.50 % (3481828)dis+10_1_sil=32000:sp=arity:random_seed=3257887834:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.39/1.50 % (3481829)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4094680681:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.39/1.50 % (3481830)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=538148689:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.39/1.50 % (3481826)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.39/1.50 % (3481829)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.39/1.50 % (3481826)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 7.39/1.50 % (3481825)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2677874406_2999 on theBenchmark for (2999ds/0Mi)
% 7.39/1.50 % Exception at run slice level
% 7.39/1.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.39/1.50 % (3481831)Instruction limit reached!
% 7.39/1.50 % (3481831)------------------------------
% 7.39/1.50 % (3481831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.39/1.50 % (3481831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.50 % (3481831)CaDiCaL version: 2.1.3
% 7.39/1.50 % (3481831)Termination reason: Instruction limit
% 7.39/1.50 % (3481831)Termination phase: Saturation
% 7.39/1.50 % (3481831)Time elapsed: 0.074 s
% 7.39/1.50 % (3481831)Peak memory usage: 12 MB
% 7.39/1.50 % (3481831)Instructions burned: 161 (million)
% 7.39/1.50 % (3481840)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2581842396:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 7.39/1.50 % (3481828)Instruction limit reached!
% 7.39/1.50 % (3481828)------------------------------
% 7.39/1.50 % (3481828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.39/1.50 % (3481828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.50 % (3481828)CaDiCaL version: 2.1.3
% 7.39/1.50 % (3481828)Termination reason: Instruction limit
% 7.39/1.50 % (3481828)Termination phase: Saturation
% 7.39/1.50 % (3481828)Time elapsed: 0.092 s
% 7.39/1.50 % (3481828)Peak memory usage: 12 MB
% 7.39/1.50 % (3481828)Instructions burned: 103 (million)
% 7.39/1.50 % (3481839)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2918536255:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 7.39/1.50 % Exception at run slice level
% 7.39/1.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.39/1.50 % (3481829)Instruction limit reached!
% 7.39/1.50 % (3481829)------------------------------
% 7.39/1.50 % (3481829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.39/1.50 % (3481829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.50 % (3481829)CaDiCaL version: 2.1.3
% 7.39/1.50 % (3481829)Termination reason: Instruction limit
% 7.39/1.50 % (3481829)Termination phase: Saturation
% 7.39/1.50 % (3481829)Time elapsed: 0.101 s
% 7.39/1.50 % (3481829)Peak memory usage: 12 MB
% 7.39/1.50 % (3481829)Instructions burned: 117 (million)
% 7.39/1.50 % (3481830)Instruction limit reached!
% 7.39/1.50 % (3481830)------------------------------
% 7.39/1.50 % (3481830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.39/1.50 % (3481830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.50 % (3481830)CaDiCaL version: 2.1.3
% 7.39/1.50 % (3481830)Termination reason: Instruction limit
% 7.39/1.50 % (3481830)Termination phase: Saturation
% 7.39/1.50 % (3481830)Time elapsed: 0.116 s
% 7.39/1.50 % (3481830)Peak memory usage: 12 MB
% 7.39/1.50 % (3481830)Instructions burned: 131 (million)
% 7.39/1.50 % (3481842)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=558104422:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 7.39/1.50 % (3481842)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.39/1.50 % (3481842)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 7.39/1.50 % (3481844)ott-21_1_sil=16000:fs=off:random_seed=3581015041:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 7.39/1.50 % (3481845)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=874251731:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 7.39/1.50 % (3481840)Instruction limit reached!
% 7.39/1.50 % (3481840)------------------------------
% 7.39/1.50 % (3481840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.39/1.50 % (3481840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.50 % (3481840)CaDiCaL version: 2.1.3
% 7.39/1.50 % (3481840)Termination reason: Instruction limit
% 7.39/1.50 % (3481840)Termination phase: Saturation
% 7.39/1.50 % (3481840)Time elapsed: 0.066 s
% 7.39/1.50 % (3481840)Peak memory usage: 12 MB
% 7.39/1.50 % (3481840)Instructions burned: 133 (million)
% 7.39/1.50 % (3481846)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3484873088:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 7.39/1.50 % Exception at run slice level
% 7.39/1.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.39/1.50 % (3481852)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=441598082:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 7.39/1.50 % Exception at run slice level
% 7.39/1.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.39/1.50 % (3481850)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3051645444:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 7.39/1.50 % (3481854)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=1628412874:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 7.39/1.50 % (3481854)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.39/1.50 % (3481844)Instruction limit reached!
% 7.39/1.50 % (3481844)------------------------------
% 7.39/1.50 % (3481844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.39/1.50 % (3481844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.50 % (3481844)CaDiCaL version: 2.1.3
% 7.39/1.50 % (3481844)Termination reason: Instruction limit
% 7.39/1.50 % (3481844)Termination phase: Saturation
% 7.39/1.50 % (3481844)Time elapsed: 0.161 s
% 7.39/1.50 % (3481844)Peak memory usage: 12 MB
% 7.39/1.50 % (3481844)Instructions burned: 180 (million)
% 7.39/1.50 % (3481857)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4246567184:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 7.39/1.50 % (3481857)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.39/1.50 % (3481854)Instruction limit reached!
% 7.39/1.50 % (3481854)------------------------------
% 7.39/1.50 % (3481854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.39/1.50 % (3481854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.50 % (3481854)CaDiCaL version: 2.1.3
% 7.39/1.50 % (3481854)Termination reason: Instruction limit
% 7.39/1.50 % (3481854)Termination phase: Saturation
% 7.39/1.50 % (3481854)Time elapsed: 0.274 s
% 7.39/1.50 % (3481854)Peak memory usage: 14 MB
% 7.39/1.50 % (3481854)Instructions burned: 693 (million)
% 7.39/1.50 % (3481859)fmb+10_1_sil=64000:random_seed=3736168018:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 7.39/1.50 % (3481859)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 7.39/1.50 % Exception at run slice level
% 7.39/1.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.39/1.50 % (3481861)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=246167042:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi)
% 7.39/1.50 % Exception at run slice level
% 7.39/1.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.39/1.50 % (3481863)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2928947577:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi)
% 7.39/1.50 % Exception at run slice level
% 7.39/1.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.39/1.50 % (3481865)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1103005235:i=5131_2994 on theBenchmark for (2994ds/5131Mi)
% 7.39/1.50 % (3481865)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.39/1.50 % (3481845)Instruction limit reached!
% 7.39/1.50 % (3481845)------------------------------
% 7.39/1.50 % (3481845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.39/1.50 % (3481845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.50 % (3481845)CaDiCaL version: 2.1.3
% 7.39/1.50 % (3481845)Termination reason: Instruction limit
% 7.39/1.50 % (3481845)Termination phase: Saturation
% 7.39/1.50 % (3481845)Time elapsed: 0.449 s
% 7.39/1.50 % (3481845)Peak memory usage: 13 MB
% 7.39/1.50 % (3481845)Instructions burned: 477 (million)
% 7.39/1.50 % (3481867)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3065555392:i=1472:ins=7:fdi=8:gsp=on_2993 on theBenchmark for (2993ds/1472Mi)
% 7.39/1.50 % (3481867)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 7.39/1.50 % (3481867)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 7.39/1.50 % (3481842)Instruction limit reached!
% 7.39/1.50 % (3481842)------------------------------
% 7.39/1.50 % (3481842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.39/1.50 % (3481842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.50 % (3481842)CaDiCaL version: 2.1.3
% 7.39/1.50 % (3481842)Termination reason: Instruction limit
% 7.39/1.50 % (3481842)Termination phase: Saturation
% 7.39/1.50 % (3481842)Time elapsed: 0.560 s
% 7.39/1.50 % (3481842)Peak memory usage: 14 MB
% 7.39/1.50 % (3481842)Instructions burned: 684 (million)
% 7.39/1.50 % (3481869)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=137959312:i=6324_2992 on theBenchmark for (2992ds/6324Mi)
% 7.39/1.50 % Exception at run slice level
% 7.39/1.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.39/1.50 % (3481871)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3355443402:fmbsr=2.30978:i=2174_2992 on theBenchmark for (2992ds/2174Mi)
% 7.39/1.50 % Exception at run slice level
% 7.39/1.50 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.39/1.50 % (3481873)ott-2_1_sil=16000:newcnf=on:random_seed=1705173586:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi)
% 7.39/1.50 % (3481873)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.39/1.50 % (3481857)Instruction limit reached!
% 7.39/1.50 % (3481857)------------------------------
% 7.39/1.50 % (3481857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.39/1.50 % (3481857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.50 % (3481857)CaDiCaL version: 2.1.3
% 7.39/1.50 % (3481857)Termination reason: Instruction limit
% 7.39/1.50 % (3481857)Termination phase: Saturation
% 7.39/1.50 % (3481857)Time elapsed: 0.775 s
% 7.39/1.50 % (3481857)Peak memory usage: 16 MB
% 7.39/1.50 % (3481857)Instructions burned: 880 (million)
% 7.39/1.50 % (3481865) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3481820-3481865"...
% 7.39/1.50 % (3481865)...printing done.
% 7.39/1.50 % (3481865)Refutation found. Thanks to Tanya!
% 7.39/1.50 % SZS status Theorem for theBenchmark
% 7.39/1.50 % SZS output start Proof for theBenchmark
% 7.39/1.50 thf(type_def_5, type, a: $tType).
% 7.39/1.50 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 7.39/1.50 thf(func_def_3, type, sK0: (a > $o)).
% 7.39/1.50 thf(func_def_4, type, sK1: (a > $o)).
% 7.39/1.50 thf(func_def_5, type, sK2: ((a > a) > a)).
% 7.39/1.50 thf(func_def_6, type, sK3: (a > (a > a) > a)).
% 7.39/1.50 thf(func_def_7, type, sK4: ((a > a) > a)).
% 7.39/1.50 thf(func_def_8, type, sK5: (a > a)).
% 7.39/1.50 thf(func_def_9, type, sK6: (a > a)).
% 7.39/1.50 thf(func_def_10, type, vNOT: ($o > $o)).
% 7.39/1.50 thf(func_def_11, type, db0: !>[X0: $tType]:(X0)).
% 7.39/1.50 thf(func_def_12, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 7.39/1.50 thf(func_def_13, type, db1: !>[X0: $tType]:(X0)).
% 7.39/1.50 thf(func_def_15, type, db2: !>[X0: $tType]:(X0)).
% 7.39/1.50 thf(func_def_16, type, db3: !>[X0: $tType]:(X0)).
% 7.39/1.50 thf(func_def_17, type, sK8: (a > (a > a > a > a) > a)).
% 7.39/1.50 thf(func_def_18, type, db5: !>[X0: $tType]:(X0)).
% 7.39/1.50 thf(func_def_19, type, db4: !>[X0: $tType]:(X0)).
% 7.39/1.50 thf(func_def_20, type, sK9: (a > (a > a > a > a) > a)).
% 7.39/1.50 thf(func_def_21, type, sK10: (a > (a > a > a > a) > a)).
% 7.39/1.50 thf(f1,conjecture,(
% 7.39/1.50 ! [X0 : (a > $o),X1 : (a > $o)] : (? [X2 : (a > a)] : (! [X4 : a] : ((X1 @ X4) => ? [X3 : a] : (! [X5 : a] : (((X4 = ((X2 @ X5))) & (X0 @ X5)) => (X5 = X3)) & (X4 = ((X2 @ X3))) & (X0 @ X3))) & ! [X3 : a] : ((X0 @ X3) => (X1 @ (X2 @ X3)))) => ? [X2 : (a > a)] : (! [X4 : a] : ((X0 @ X4) => ? [X3 : a] : (! [X5 : a] : (((X4 = ((X2 @ X5))) & (X1 @ X5)) => (X5 = X3)) & (X4 = ((X2 @ X3))) & (X1 @ X3))) & ! [X3 : a] : ((X1 @ X3) => (X0 @ (X2 @ X3)))))),
% 7.39/1.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cEQP1_1B_pme)).
% 7.39/1.50 thf(f2,negated_conjecture,(
% 7.39/1.50 ~ ! [X0 : (a > $o),X1 : (a > $o)] : (? [X2 : (a > a)] : (! [X4 : a] : ((X1 @ X4) => ? [X3 : a] : (! [X5 : a] : (((X4 = ((X2 @ X5))) & (X0 @ X5)) => (X5 = X3)) & (X4 = ((X2 @ X3))) & (X0 @ X3))) & ! [X3 : a] : ((X0 @ X3) => (X1 @ (X2 @ X3)))) => ? [X2 : (a > a)] : (! [X4 : a] : ((X0 @ X4) => ? [X3 : a] : (! [X5 : a] : (((X4 = ((X2 @ X5))) & (X1 @ X5)) => (X5 = X3)) & (X4 = ((X2 @ X3))) & (X1 @ X3))) & ! [X3 : a] : ((X1 @ X3) => (X0 @ (X2 @ X3)))))),
% 7.39/1.50 inference(negated_conjecture,[status(cth)],[f1])).
% 7.39/1.50 thf(f3,plain,(
% 7.39/1.50 ~ ! [X0 : (a > $o),X1 : (a > $o)] : (? [X2 : (a > a)] : (! [X3 : a] : ((X1 @ X3) => ? [X4 : a] : (! [X5 : a] : (((((X2 @ X5)) = X3) & (X0 @ X5)) => (X4 = X5)) & (((X2 @ X4)) = X3) & (X0 @ X4))) & ! [X6 : a] : ((X0 @ X6) => (X1 @ (X2 @ X6)))) => ? [X7 : (a > a)] : (! [X8 : a] : ((X0 @ X8) => ? [X9 : a] : (! [X10 : a] : (((((X7 @ X10)) = X8) & (X1 @ X10)) => (X9 = X10)) & (((X7 @ X9)) = X8) & (X1 @ X9))) & ! [X11 : a] : ((X1 @ X11) => (X0 @ (X7 @ X11)))))),
% 7.39/1.50 inference(rectify,[],[f2])).
% 7.39/1.50 thf(f4,plain,(
% 7.39/1.50 ~ ! [X0 : (a > $o),X1 : (a > $o)] : (? [X2 : (a > a)] : (! [X3 : a] : ((((X1 @ X3)) = $true) => ? [X4 : a] : (! [X5 : a] : (((((X2 @ X5)) = X3) & (((X0 @ X5)) = $true)) => (X4 = X5)) & (((X2 @ X4)) = X3) & (((X0 @ X4)) = $true))) & ! [X6 : a] : ((((X0 @ X6)) = $true) => (((X1 @ (X2 @ X6))) = $true))) => ? [X7 : (a > a)] : (! [X8 : a] : ((((X0 @ X8)) = $true) => ? [X9 : a] : (! [X10 : a] : (((((X7 @ X10)) = X8) & (((X1 @ X10)) = $true)) => (X9 = X10)) & (((X7 @ X9)) = X8) & (((X1 @ X9)) = $true))) & ! [X11 : a] : ((((X1 @ X11)) = $true) => (((X0 @ (X7 @ X11))) = $true))))),
% 7.39/1.50 inference(fool_elimination,[],[f3])).
% 7.39/1.50 thf(f5,plain,(
% 7.39/1.50 ? [X0 : (a > $o),X1 : (a > $o)] : (! [X7 : (a > a)] : (? [X8 : a] : (! [X9 : a] : (? [X10 : a] : ((X9 != X10) & ((((X7 @ X10)) = X8) & (((X1 @ X10)) = $true))) | (((X7 @ X9)) != X8) | (((X1 @ X9)) != $true)) & (((X0 @ X8)) = $true)) | ? [X11 : a] : ((((X0 @ (X7 @ X11))) != $true) & (((X1 @ X11)) = $true))) & ? [X2 : (a > a)] : (! [X3 : a] : (? [X4 : a] : (! [X5 : a] : ((X4 = X5) | ((((X2 @ X5)) != X3) | (((X0 @ X5)) != $true))) & (((X2 @ X4)) = X3) & (((X0 @ X4)) = $true)) | (((X1 @ X3)) != $true)) & ! [X6 : a] : ((((X1 @ (X2 @ X6))) = $true) | (((X0 @ X6)) != $true))))),
% 7.39/1.50 inference(ennf_transformation,[],[f4])).
% 7.39/1.50 thf(f6,plain,(
% 7.39/1.50 ? [X0 : (a > $o),X1 : (a > $o)] : (! [X7 : (a > a)] : (? [X8 : a] : (! [X9 : a] : (? [X10 : a] : ((X9 != X10) & (((X7 @ X10)) = X8) & (((X1 @ X10)) = $true)) | (((X7 @ X9)) != X8) | (((X1 @ X9)) != $true)) & (((X0 @ X8)) = $true)) | ? [X11 : a] : ((((X0 @ (X7 @ X11))) != $true) & (((X1 @ X11)) = $true))) & ? [X2 : (a > a)] : (! [X3 : a] : (? [X4 : a] : (! [X5 : a] : ((X4 = X5) | (((X2 @ X5)) != X3) | (((X0 @ X5)) != $true)) & (((X2 @ X4)) = X3) & (((X0 @ X4)) = $true)) | (((X1 @ X3)) != $true)) & ! [X6 : a] : ((((X1 @ (X2 @ X6))) = $true) | (((X0 @ X6)) != $true))))),
% 7.39/1.50 inference(flattening,[],[f5])).
% 7.39/1.50 thf(f7,plain,(
% 7.39/1.50 ? [X0 : (a > $o),X1 : (a > $o)] : (! [X2 : (a > a)] : (? [X3 : a] : (! [X4 : a] : (? [X5 : a] : ((X4 != X5) & (((X2 @ X5)) = X3) & (((X1 @ X5)) = $true)) | (((X2 @ X4)) != X3) | (((X1 @ X4)) != $true)) & (((X0 @ X3)) = $true)) | ? [X6 : a] : (($true != ((X0 @ (X2 @ X6)))) & ($true = ((X1 @ X6))))) & ? [X7 : (a > a)] : (! [X8 : a] : (? [X9 : a] : (! [X10 : a] : ((X9 = X10) | (((X7 @ X10)) != X8) | ($true != ((X0 @ X10)))) & (((X7 @ X9)) = X8) & ($true = ((X0 @ X9)))) | ($true != ((X1 @ X8)))) & ! [X11 : a] : (($true = ((X1 @ (X7 @ X11)))) | ($true != ((X0 @ X11))))))),
% 7.39/1.50 inference(rectify,[],[f6])).
% 7.39/1.50 thf(f8,plain,(
% 7.39/1.50 ! [X2 : (a > a)] : ((! [X4 : a] : (((((sK3 @ X4 @ X2)) != X4) & (((sK2 @ X2)) = ((X2 @ (sK3 @ X4 @ X2)))) & ($true = ((sK1 @ (sK3 @ X4 @ X2))))) | (((X2 @ X4)) != ((sK2 @ X2))) | ($true != ((sK1 @ X4)))) & ($true = ((sK0 @ (sK2 @ X2))))) | (($true != ((sK0 @ (X2 @ (sK4 @ X2))))) & ($true = ((sK1 @ (sK4 @ X2)))))) & (! [X8 : a] : ((! [X10 : a] : ((((sK6 @ X8)) = X10) | (((sK5 @ X10)) != X8) | ($true != ((sK0 @ X10)))) & (((sK5 @ (sK6 @ X8))) = X8) & ($true = ((sK0 @ (sK6 @ X8))))) | ($true != ((sK1 @ X8)))) & ! [X11 : a] : (($true = ((sK1 @ (sK5 @ X11)))) | ($true != ((sK0 @ X11)))))),
% 7.39/1.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,vAPP,vAPP,vAPP,sK5,vAPP]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X9,sK6 @ X8),skolemize(X9,sK6 @ X8),skolemize(X9,sK6 @ X8),skolemize(X7,sK5),skolemize(X9,sK6 @ X8)],[f7])).
% 7.39/1.50 thf(f9,plain,(
% 7.39/1.50 ( ! [X11 : a] : (($true != ((sK0 @ X11))) | ($true = ((sK1 @ (sK5 @ X11))))) )),
% 7.39/1.50 inference(cnf_transformation,[],[f8])).
% 7.39/1.50 thf(f10,plain,(
% 7.39/1.50 ( ! [X8 : a] : (($true != ((sK1 @ X8))) | ($true = ((sK0 @ (sK6 @ X8))))) )),
% 7.39/1.50 inference(cnf_transformation,[],[f8])).
% 7.39/1.50 thf(f11,plain,(
% 7.39/1.50 ( ! [X8 : a] : (($true != ((sK1 @ X8))) | (((sK5 @ (sK6 @ X8))) = X8)) )),
% 7.39/1.50 inference(cnf_transformation,[],[f8])).
% 7.39/1.50 thf(f12,plain,(
% 7.39/1.50 ( ! [X10 : a,X8 : a] : ((((sK6 @ X8)) = X10) | (((sK5 @ X10)) != X8) | ($true != ((sK0 @ X10))) | ($true != ((sK1 @ X8)))) )),
% 7.39/1.50 inference(cnf_transformation,[],[f8])).
% 7.39/1.50 thf(f13,plain,(
% 7.39/1.50 ( ! [X2 : (a > a)] : (($true = ((sK0 @ (sK2 @ X2)))) | ($true = ((sK1 @ (sK4 @ X2))))) )),
% 7.39/1.50 inference(cnf_transformation,[],[f8])).
% 7.39/1.50 thf(f14,plain,(
% 7.39/1.50 ( ! [X2 : (a > a)] : (($true != ((sK0 @ (X2 @ (sK4 @ X2))))) | ($true = ((sK0 @ (sK2 @ X2))))) )),
% 7.39/1.50 inference(cnf_transformation,[],[f8])).
% 7.39/1.50 thf(f15,plain,(
% 7.39/1.50 ( ! [X2 : (a > a),X4 : a] : (($true != ((sK1 @ X4))) | (((X2 @ X4)) != ((sK2 @ X2))) | ($true = ((sK1 @ (sK3 @ X4 @ X2)))) | ($true = ((sK1 @ (sK4 @ X2))))) )),
% 7.39/1.50 inference(cnf_transformation,[],[f8])).
% 7.39/1.50 thf(f16,plain,(
% 7.39/1.50 ( ! [X2 : (a > a),X4 : a] : (($true != ((sK1 @ X4))) | (((X2 @ X4)) != ((sK2 @ X2))) | ($true = ((sK1 @ (sK3 @ X4 @ X2)))) | ($true != ((sK0 @ (X2 @ (sK4 @ X2)))))) )),
% 7.39/1.50 inference(cnf_transformation,[],[f8])).
% 7.39/1.50 thf(f17,plain,(
% 7.39/1.50 ( ! [X2 : (a > a),X4 : a] : (($true != ((sK1 @ X4))) | (((X2 @ X4)) != ((sK2 @ X2))) | (((sK2 @ X2)) = ((X2 @ (sK3 @ X4 @ X2)))) | ($true = ((sK1 @ (sK4 @ X2))))) )),
% 7.39/1.50 inference(cnf_transformation,[],[f8])).
% 7.39/1.50 thf(f18,plain,(
% 7.39/1.50 ( ! [X2 : (a > a),X4 : a] : (($true != ((sK1 @ X4))) | (((X2 @ X4)) != ((sK2 @ X2))) | (((sK2 @ X2)) = ((X2 @ (sK3 @ X4 @ X2)))) | ($true != ((sK0 @ (X2 @ (sK4 @ X2)))))) )),
% 7.39/1.51 inference(cnf_transformation,[],[f8])).
% 7.39/1.51 thf(f19,plain,(
% 7.39/1.51 ( ! [X2 : (a > a),X4 : a] : (($true != ((sK1 @ X4))) | (((X2 @ X4)) != ((sK2 @ X2))) | (((sK3 @ X4 @ X2)) != X4) | ($true = ((sK1 @ (sK4 @ X2))))) )),
% 7.39/1.51 inference(cnf_transformation,[],[f8])).
% 7.39/1.51 thf(f20,plain,(
% 7.39/1.51 ( ! [X2 : (a > a),X4 : a] : (($true != ((sK1 @ X4))) | (((X2 @ X4)) != ((sK2 @ X2))) | (((sK3 @ X4 @ X2)) != X4) | ($true != ((sK0 @ (X2 @ (sK4 @ X2)))))) )),
% 7.39/1.51 inference(cnf_transformation,[],[f8])).
% 7.39/1.51 thf(f22,definition,(
% 7.39/1.51 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 7.39/1.51 introduced(theory,[fool_exhaustiveness_axiom])).
% 7.39/1.51 thf(f23,plain,(
% 7.39/1.51 ( ! [X10 : a] : ((((sK6 @ (sK5 @ X10))) = X10) | ($true != ((sK0 @ X10))) | ($true != ((sK1 @ (sK5 @ X10))))) )),
% 7.39/1.51 inference(equality_resolution,[],[f12])).
% 7.39/1.51 thf(f24,plain,(
% 7.39/1.51 ( ! [X0 : (a > a)] : (($true != $true) | ($true = ((sK1 @ (sK5 @ (sK2 @ X0))))) | ($true = ((sK1 @ (sK4 @ X0))))) )),
% 7.39/1.51 inference(constrained_superposition,[],[f9,f13])).
% 7.39/1.51 thf(f25,plain,(
% 7.39/1.51 ( ! [X0 : (a > a)] : (($true = ((sK1 @ (sK5 @ (sK2 @ X0))))) | ($true = ((sK1 @ (sK4 @ X0))))) )),
% 7.39/1.51 inference(trivial_inequality_removal,[],[f24])).
% 7.39/1.51 thf(f26,plain,(
% 7.39/1.51 ( ! [X10 : a] : (($true != ((sK0 @ X10))) | (((sK6 @ (sK5 @ X10))) = X10)) )),
% 7.39/1.51 inference(forward_subsumption_resolution,[],[f23,f9])).
% 7.39/1.51 thf(f27,plain,(
% 7.39/1.51 ( ! [X0 : (a > a)] : (($true != $true) | (((sK2 @ X0)) = ((sK6 @ (sK5 @ (sK2 @ X0))))) | ($true = ((sK1 @ (sK4 @ X0))))) )),
% 7.39/1.51 inference(constrained_superposition,[],[f26,f13])).
% 7.39/1.51 thf(f28,plain,(
% 7.39/1.51 ( ! [X0 : (a > a)] : ((((sK2 @ X0)) = ((sK6 @ (sK5 @ (sK2 @ X0))))) | ($true = ((sK1 @ (sK4 @ X0))))) )),
% 7.39/1.51 inference(trivial_inequality_removal,[],[f27])).
% 7.39/1.51 thf(f93,plain,(
% 7.39/1.51 ( ! [X0 : a] : (($true != $true) | (((sK5 @ (sK6 @ X0))) = X0) | ($false = ((sK1 @ X0)))) )),
% 7.39/1.51 inference(constrained_superposition,[],[f11,f22])).
% 7.39/1.51 thf(f94,plain,(
% 7.39/1.51 ( ! [X0 : a,X1 : (a > a)] : (($true != $true) | (((sK2 @ X1)) != ((X1 @ X0))) | ($true = ((sK1 @ (sK3 @ X0 @ X1)))) | ($true = ((sK1 @ (sK4 @ X1)))) | ($false = ((sK1 @ X0)))) )),
% 7.39/1.51 inference(constrained_superposition,[],[f15,f22])).
% 7.39/1.51 thf(f95,plain,(
% 7.39/1.51 ( ! [X0 : a,X1 : (a > a)] : (($true != $true) | (((sK2 @ X1)) != ((X1 @ X0))) | ($true = ((sK1 @ (sK3 @ X0 @ X1)))) | ($true != ((sK0 @ (X1 @ (sK4 @ X1))))) | ($false = ((sK1 @ X0)))) )),
% 7.39/1.51 inference(constrained_superposition,[],[f16,f22])).
% 7.39/1.51 thf(f96,plain,(
% 7.39/1.51 ( ! [X0 : a,X1 : (a > a)] : (($true != $true) | (((sK2 @ X1)) != ((X1 @ X0))) | (((sK2 @ X1)) = ((X1 @ (sK3 @ X0 @ X1)))) | ($true = ((sK1 @ (sK4 @ X1)))) | ($false = ((sK1 @ X0)))) )),
% 7.39/1.51 inference(constrained_superposition,[],[f17,f22])).
% 7.39/1.51 thf(f97,plain,(
% 7.39/1.51 ( ! [X0 : a,X1 : (a > a)] : (($true != $true) | (((sK2 @ X1)) != ((X1 @ X0))) | (((sK3 @ X0 @ X1)) != X0) | ($true = ((sK1 @ (sK4 @ X1)))) | ($false = ((sK1 @ X0)))) )),
% 7.39/1.51 inference(constrained_superposition,[],[f19,f22])).
% 7.39/1.51 thf(f98,plain,(
% 7.39/1.51 ( ! [X0 : a,X1 : (a > a)] : (($true != $true) | (((sK2 @ X1)) != ((X1 @ X0))) | (((sK3 @ X0 @ X1)) != X0) | ($true != ((sK0 @ (X1 @ (sK4 @ X1))))) | ($false = ((sK1 @ X0)))) )),
% 7.39/1.51 inference(constrained_superposition,[],[f20,f22])).
% 7.39/1.51 thf(f99,plain,(
% 7.39/1.51 ( ! [X0 : (a > a)] : (($true != $true) | ($true = ((sK0 @ (sK2 @ X0)))) | ($false = ((sK0 @ (X0 @ (sK4 @ X0)))))) )),
% 7.39/1.51 inference(constrained_superposition,[],[f14,f22])).
% 7.39/1.51 thf(f101,plain,(
% 7.39/1.51 ( ! [X0 : (a > a)] : (($false = ((sK0 @ (X0 @ (sK4 @ X0))))) | ($true = ((sK0 @ (sK2 @ X0))))) )),
% 7.39/1.51 inference(trivial_inequality_removal,[],[f99])).
% 7.39/1.51 thf(f102,plain,(
% 7.39/1.51 ( ! [X0 : a,X1 : (a > a)] : (($true != ((sK0 @ (X1 @ (sK4 @ X1))))) | (((sK3 @ X0 @ X1)) != X0) | (((sK2 @ X1)) != ((X1 @ X0))) | ($false = ((sK1 @ X0)))) )),
% 7.39/1.51 inference(trivial_inequality_removal,[],[f98])).
% 7.39/1.51 thf(f103,plain,(
% 7.39/1.51 ( ! [X0 : a,X1 : (a > a)] : ((((sK2 @ X1)) != ((X1 @ X0))) | (((sK3 @ X0 @ X1)) != X0) | ($true = ((sK1 @ (sK4 @ X1)))) | ($false = ((sK1 @ X0)))) )),
% 7.39/1.51 inference(trivial_inequality_removal,[],[f97])).
% 7.39/1.51 thf(f104,plain,(
% 7.39/1.51 ( ! [X0 : a,X1 : (a > a)] : ((((sK2 @ X1)) != ((X1 @ X0))) | (((sK2 @ X1)) = ((X1 @ (sK3 @ X0 @ X1)))) | ($true = ((sK1 @ (sK4 @ X1)))) | ($false = ((sK1 @ X0)))) )),
% 7.39/1.51 inference(trivial_inequality_removal,[],[f96])).
% 7.39/1.51 thf(f105,plain,(
% 7.39/1.51 ( ! [X0 : a,X1 : (a > a)] : (($true != ((sK0 @ (X1 @ (sK4 @ X1))))) | ($true = ((sK1 @ (sK3 @ X0 @ X1)))) | (((sK2 @ X1)) != ((X1 @ X0))) | ($false = ((sK1 @ X0)))) )),
% 7.39/1.51 inference(trivial_inequality_removal,[],[f95])).
% 7.39/1.51 thf(f106,plain,(
% 7.39/1.51 ( ! [X0 : a,X1 : (a > a)] : ((((sK2 @ X1)) != ((X1 @ X0))) | ($true = ((sK1 @ (sK3 @ X0 @ X1)))) | ($true = ((sK1 @ (sK4 @ X1)))) | ($false = ((sK1 @ X0)))) )),
% 7.39/1.51 inference(trivial_inequality_removal,[],[f94])).
% 7.39/1.51 thf(f107,plain,(
% 7.39/1.51 ( ! [X0 : a] : ((((sK5 @ (sK6 @ X0))) = X0) | ($false = ((sK1 @ X0)))) )),
% 7.39/1.51 inference(trivial_inequality_removal,[],[f93])).
% 7.39/1.51 thf(f121,plain,(
% 7.39/1.51 ( ! [X0 : a,X1 : (a > a)] : (($true != $true) | (((sK2 @ X1)) != ((X1 @ X0))) | (((sK2 @ X1)) = ((X1 @ (sK3 @ X0 @ X1)))) | ($true != ((sK0 @ (X1 @ (sK4 @ X1))))) | ($false = ((sK1 @ X0)))) )),
% 7.39/1.51 inference(constrained_superposition,[],[f18,f22])).
% 7.39/1.51 thf(f122,plain,(
% 7.39/1.51 ( ! [X0 : a,X1 : (a > a)] : (($true != ((sK0 @ (X1 @ (sK4 @ X1))))) | (((sK2 @ X1)) = ((X1 @ (sK3 @ X0 @ X1)))) | (((sK2 @ X1)) != ((X1 @ X0))) | ($false = ((sK1 @ X0)))) )),
% 7.39/1.51 inference(trivial_inequality_removal,[],[f121])).
% 7.39/1.51 thf(f215,plain,(
% 7.39/1.51 ( ! [X2 : a,X0 : (a > a)] : ((((sK2 @ X0)) != ((sK2 @ (^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0)))))) | (((sK3 @ X2 @ (^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))))) != X2) | ($true = ((sK1 @ (sK4 @ (^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($false = ((sK1 @ X2))) | ($true = ((sK1 @ (sK4 @ X0)))) | (((sK5 @ (sK2 @ X0))) != X2)) )),
% 7.39/1.51 inference(constrained_superposition,[],[f103,f28])).
% 7.39/1.51 thf(f238,plain,(
% 7.39/1.51 ( ! [X2 : a,X0 : (a > a)] : ((((sK2 @ X0)) != ((sK2 @ sK6))) | (((sK3 @ X2 @ sK6)) != X2) | ($true = ((sK1 @ (sK4 @ sK6)))) | ($false = ((sK1 @ X2))) | ($true = ((sK1 @ (sK4 @ X0)))) | (((sK5 @ (sK2 @ X0))) != X2)) )),
% 7.39/1.51 inference(beta-eta_normalization,[],[f215])).
% 7.39/1.51 thf(f306,plain,(
% 7.39/1.51 ( ! [X2 : a,X0 : (a > a)] : ((((sK2 @ X0)) != ((sK2 @ (^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0)))))) | ($true = ((sK1 @ (sK3 @ X2 @ (^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = ((sK1 @ (sK4 @ (^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($false = ((sK1 @ X2))) | ($true = ((sK1 @ (sK4 @ X0)))) | (((sK5 @ (sK2 @ X0))) != X2)) )),
% 7.39/1.51 inference(constrained_superposition,[],[f106,f28])).
% 7.39/1.51 thf(f334,plain,(
% 7.39/1.51 ( ! [X2 : a,X0 : (a > a)] : ((((sK2 @ X0)) != ((sK2 @ sK6))) | ($true = ((sK1 @ (sK3 @ X2 @ sK6)))) | ($true = ((sK1 @ (sK4 @ sK6)))) | ($false = ((sK1 @ X2))) | ($true = ((sK1 @ (sK4 @ X0)))) | (((sK5 @ (sK2 @ X0))) != X2)) )),
% 7.39/1.51 inference(beta-eta_normalization,[],[f306])).
% 7.39/1.51 thf(f422,plain,(
% 7.39/1.51 ( ! [X2 : a,X0 : (a > a)] : ((((sK2 @ X0)) != ((sK2 @ (^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0)))))) | (((sK2 @ (^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))))) = (((^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ (sK3 @ X2 @ (^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($true = ((sK1 @ (sK4 @ (^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ($false = ((sK1 @ X2))) | ($true = ((sK1 @ (sK4 @ X0)))) | (((sK5 @ (sK2 @ X0))) != X2)) )),
% 7.39/1.51 inference(constrained_superposition,[],[f104,f28])).
% 7.39/1.51 thf(f461,plain,(
% 7.39/1.51 ( ! [X2 : a,X0 : (a > a)] : ((((sK2 @ X0)) != ((sK2 @ sK6))) | (((sK2 @ sK6)) = ((sK6 @ (sK3 @ X2 @ sK6)))) | ($true = ((sK1 @ (sK4 @ sK6)))) | ($false = ((sK1 @ X2))) | ($true = ((sK1 @ (sK4 @ X0)))) | (((sK5 @ (sK2 @ X0))) != X2)) )),
% 7.39/1.51 inference(beta-eta_normalization,[],[f422])).
% 7.39/1.51 thf(f1021,definition,(
% 7.39/1.51 spl7_1 <=> ($true = ((sK1 @ (sK4 @ sK6))))),
% 7.39/1.51 introduced(definition,[new_symbols(definition,[spl7_1])],[avatar_definition])).
% 7.39/1.51 thf(f1022,plain,(
% 7.39/1.51 ($true != ((sK1 @ (sK4 @ sK6)))) | spl7_1),
% 7.39/1.51 inference(avatar_component_clause,[],[f1021])).
% 7.39/1.51 thf(f1023,plain,(
% 7.39/1.51 ($true = ((sK1 @ (sK4 @ sK6)))) | ~spl7_1),
% 7.39/1.51 inference(avatar_component_clause,[],[f1021])).
% 7.39/1.51 thf(f2010,plain,(
% 7.39/1.51 ($true != $true) | ($true = ((sK0 @ (sK6 @ (sK4 @ sK6))))) | ~spl7_1),
% 7.39/1.51 inference(constrained_superposition,[],[f10,f1023])).
% 7.39/1.51 thf(f2025,plain,(
% 7.39/1.51 ($true = ((sK0 @ (sK6 @ (sK4 @ sK6))))) | ~spl7_1),
% 7.39/1.51 inference(trivial_inequality_removal,[],[f2010])).
% 7.39/1.51 thf(f2032,plain,(
% 7.39/1.51 ($true = $false) | ($true = ((sK0 @ (sK2 @ (^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ~spl7_1),
% 7.39/1.51 inference(constrained_superposition,[],[f101,f2025])).
% 7.39/1.51 thf(f2034,plain,(
% 7.39/1.51 ( ! [X0 : a] : (($true != $true) | (((sK3 @ X0 @ (^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))))) != X0) | (((sK2 @ (^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))))) != (((^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ X0))) | ($false = ((sK1 @ X0)))) ) | ~spl7_1),
% 7.39/1.51 inference(constrained_superposition,[],[f102,f2025])).
% 7.39/1.51 thf(f2036,plain,(
% 7.39/1.51 ( ! [X0 : a] : (($true != $true) | ($true = ((sK1 @ (sK3 @ X0 @ (^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | (((sK2 @ (^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))))) != (((^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ X0))) | ($false = ((sK1 @ X0)))) ) | ~spl7_1),
% 7.39/1.51 inference(constrained_superposition,[],[f105,f2025])).
% 7.39/1.51 thf(f2038,plain,(
% 7.39/1.51 ( ! [X0 : a] : (($true != $true) | (((sK2 @ (^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))))) = (((^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ (sK3 @ X0 @ (^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | (((sK2 @ (^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))))) != (((^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ X0))) | ($false = ((sK1 @ X0)))) ) | ~spl7_1),
% 7.39/1.51 inference(constrained_superposition,[],[f122,f2025])).
% 7.39/1.51 thf(f2054,plain,(
% 7.39/1.51 ( ! [X0 : a] : ((((sK2 @ (^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))))) = (((^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ (sK3 @ X0 @ (^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | (((sK2 @ (^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))))) != (((^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ X0))) | ($false = ((sK1 @ X0)))) ) | ~spl7_1),
% 7.39/1.51 inference(trivial_inequality_removal,[],[f2038])).
% 7.39/1.51 thf(f2055,plain,(
% 7.39/1.51 ( ! [X0 : a] : ((((sK6 @ X0)) != ((sK2 @ sK6))) | (((sK2 @ sK6)) = ((sK6 @ (sK3 @ X0 @ sK6)))) | ($false = ((sK1 @ X0)))) ) | ~spl7_1),
% 7.39/1.51 inference(beta-eta_normalization,[],[f2054])).
% 7.39/1.51 thf(f2058,plain,(
% 7.39/1.51 ( ! [X0 : a] : (($true = ((sK1 @ (sK3 @ X0 @ (^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | (((sK2 @ (^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))))) != (((^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ X0))) | ($false = ((sK1 @ X0)))) ) | ~spl7_1),
% 7.39/1.51 inference(trivial_inequality_removal,[],[f2036])).
% 7.39/1.51 thf(f2059,plain,(
% 7.39/1.51 ( ! [X0 : a] : ((((sK6 @ X0)) != ((sK2 @ sK6))) | ($true = ((sK1 @ (sK3 @ X0 @ sK6)))) | ($false = ((sK1 @ X0)))) ) | ~spl7_1),
% 7.39/1.51 inference(beta-eta_normalization,[],[f2058])).
% 7.39/1.51 thf(f2062,plain,(
% 7.39/1.51 ( ! [X0 : a] : ((((sK3 @ X0 @ (^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))))) != X0) | (((sK2 @ (^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))))) != (((^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))) @ X0))) | ($false = ((sK1 @ X0)))) ) | ~spl7_1),
% 7.39/1.51 inference(trivial_inequality_removal,[],[f2034])).
% 7.39/1.51 thf(f2063,plain,(
% 7.39/1.51 ( ! [X0 : a] : ((((sK6 @ X0)) != ((sK2 @ sK6))) | (((sK3 @ X0 @ sK6)) != X0) | ($false = ((sK1 @ X0)))) ) | ~spl7_1),
% 7.39/1.51 inference(beta-eta_normalization,[],[f2062])).
% 7.39/1.51 thf(f2066,plain,(
% 7.39/1.51 ($true = ((sK0 @ (sK2 @ (^[Y0 : a]: (sK6 @ ((^[Y1 : a]: (Y1)) @ Y0))))))) | ~spl7_1),
% 7.39/1.51 inference(trivial_inequality_removal,[],[f2032])).
% 7.39/1.51 thf(f2067,plain,(
% 7.39/1.51 ($true = ((sK0 @ (sK2 @ sK6)))) | ~spl7_1),
% 7.39/1.51 inference(beta-eta_normalization,[],[f2066])).
% 7.39/1.51 thf(f2114,plain,(
% 7.39/1.51 ($true != $true) | (((sK2 @ sK6)) = ((sK6 @ (sK5 @ (sK2 @ sK6))))) | ~spl7_1),
% 7.39/1.51 inference(constrained_superposition,[],[f26,f2067])).
% 7.39/1.51 thf(f2115,plain,(
% 7.39/1.51 ($true != $true) | ($true = ((sK1 @ (sK5 @ (sK2 @ sK6))))) | ~spl7_1),
% 7.39/1.51 inference(constrained_superposition,[],[f9,f2067])).
% 7.39/1.51 thf(f2137,plain,(
% 7.39/1.51 ($true = ((sK1 @ (sK5 @ (sK2 @ sK6))))) | ~spl7_1),
% 7.39/1.51 inference(trivial_inequality_removal,[],[f2115])).
% 7.39/1.51 thf(f2138,plain,(
% 7.39/1.51 (((sK2 @ sK6)) = ((sK6 @ (sK5 @ (sK2 @ sK6))))) | ~spl7_1),
% 7.39/1.51 inference(trivial_inequality_removal,[],[f2114])).
% 7.39/1.51 thf(f3318,plain,(
% 7.39/1.51 (((sK2 @ sK6)) != ((sK2 @ sK6))) | (((sK5 @ (sK2 @ sK6))) != ((sK3 @ (sK5 @ (sK2 @ sK6)) @ sK6))) | ($false = ((sK1 @ (sK5 @ (sK2 @ sK6))))) | ~spl7_1),
% 7.39/1.51 inference(constrained_superposition,[],[f2063,f2138])).
% 7.39/1.51 thf(f3320,plain,(
% 7.39/1.51 (((sK5 @ (sK2 @ sK6))) != ((sK3 @ (sK5 @ (sK2 @ sK6)) @ sK6))) | ($false = ((sK1 @ (sK5 @ (sK2 @ sK6))))) | ~spl7_1),
% 7.39/1.51 inference(trivial_inequality_removal,[],[f3318])).
% 7.39/1.51 thf(f3321,plain,(
% 7.39/1.51 ($true = $false) | (((sK5 @ (sK2 @ sK6))) != ((sK3 @ (sK5 @ (sK2 @ sK6)) @ sK6))) | ~spl7_1),
% 7.39/1.51 inference(forward_demodulation,[],[f3320,f2137])).
% 7.39/1.51 thf(f3322,plain,(
% 7.39/1.51 (((sK5 @ (sK2 @ sK6))) != ((sK3 @ (sK5 @ (sK2 @ sK6)) @ sK6))) | ~spl7_1),
% 7.39/1.51 inference(trivial_inequality_removal,[],[f3321])).
% 7.39/1.51 thf(f3663,plain,(
% 7.39/1.51 (((sK2 @ sK6)) != ((sK2 @ sK6))) | ($true = ((sK1 @ (sK3 @ (sK5 @ (sK2 @ sK6)) @ sK6)))) | ($false = ((sK1 @ (sK5 @ (sK2 @ sK6))))) | ~spl7_1),
% 7.39/1.51 inference(constrained_superposition,[],[f2059,f2138])).
% 7.39/1.51 thf(f3665,plain,(
% 7.39/1.51 ($true = ((sK1 @ (sK3 @ (sK5 @ (sK2 @ sK6)) @ sK6)))) | ($false = ((sK1 @ (sK5 @ (sK2 @ sK6))))) | ~spl7_1),
% 7.39/1.51 inference(trivial_inequality_removal,[],[f3663])).
% 7.39/1.51 thf(f3666,plain,(
% 7.39/1.51 ($true = $false) | ($true = ((sK1 @ (sK3 @ (sK5 @ (sK2 @ sK6)) @ sK6)))) | ~spl7_1),
% 7.39/1.51 inference(forward_demodulation,[],[f3665,f2137])).
% 7.39/1.51 thf(f3667,plain,(
% 7.39/1.51 ($true = ((sK1 @ (sK3 @ (sK5 @ (sK2 @ sK6)) @ sK6)))) | ~spl7_1),
% 7.39/1.51 inference(trivial_inequality_removal,[],[f3666])).
% 7.39/1.51 thf(f4413,plain,(
% 7.39/1.51 (((sK2 @ sK6)) != ((sK2 @ sK6))) | (((sK2 @ sK6)) = ((sK6 @ (sK3 @ (sK5 @ (sK2 @ sK6)) @ sK6)))) | ($false = ((sK1 @ (sK5 @ (sK2 @ sK6))))) | ~spl7_1),
% 7.39/1.51 inference(constrained_superposition,[],[f2055,f2138])).
% 7.39/1.51 thf(f4416,plain,(
% 7.39/1.51 (((sK2 @ sK6)) = ((sK6 @ (sK3 @ (sK5 @ (sK2 @ sK6)) @ sK6)))) | ($false = ((sK1 @ (sK5 @ (sK2 @ sK6))))) | ~spl7_1),
% 7.39/1.51 inference(trivial_inequality_removal,[],[f4413])).
% 7.39/1.51 thf(f4417,plain,(
% 7.39/1.51 ($true = $false) | (((sK2 @ sK6)) = ((sK6 @ (sK3 @ (sK5 @ (sK2 @ sK6)) @ sK6)))) | ~spl7_1),
% 7.39/1.51 inference(forward_demodulation,[],[f4416,f2137])).
% 7.39/1.51 thf(f4418,plain,(
% 7.39/1.51 (((sK2 @ sK6)) = ((sK6 @ (sK3 @ (sK5 @ (sK2 @ sK6)) @ sK6)))) | ~spl7_1),
% 7.39/1.51 inference(trivial_inequality_removal,[],[f4417])).
% 7.39/1.51 thf(f4420,plain,(
% 7.39/1.51 (((sK5 @ (sK2 @ sK6))) = ((sK3 @ (sK5 @ (sK2 @ sK6)) @ sK6))) | ($false = ((sK1 @ (sK3 @ (sK5 @ (sK2 @ sK6)) @ sK6)))) | ~spl7_1),
% 7.39/1.51 inference(constrained_superposition,[],[f107,f4418])).
% 7.39/1.51 thf(f4569,plain,(
% 7.39/1.51 ($false = ((sK1 @ (sK3 @ (sK5 @ (sK2 @ sK6)) @ sK6)))) | ~spl7_1),
% 7.39/1.51 inference(forward_subsumption_resolution,[],[f4420,f3322])).
% 7.39/1.51 thf(f4574,plain,(
% 7.39/1.51 ($true = $false) | ~spl7_1),
% 7.39/1.51 inference(constrained_superposition,[],[f4569,f3667])).
% 7.39/1.51 thf(f4588,plain,(
% 7.39/1.51 $false | ~spl7_1),
% 7.39/1.51 inference(trivial_inequality_removal,[],[f4574])).
% 7.39/1.51 thf(f4589,plain,(
% 7.39/1.51 ~spl7_1),
% 7.39/1.51 inference(avatar_contradiction_clause,[],[f4588])).
% 7.39/1.51 thf(f4605,plain,(
% 7.39/1.51 ( ! [X2 : a,X0 : (a > a)] : ((((sK2 @ X0)) != ((sK2 @ sK6))) | (((sK3 @ X2 @ sK6)) != X2) | ($false = ((sK1 @ X2))) | ($true = ((sK1 @ (sK4 @ X0)))) | (((sK5 @ (sK2 @ X0))) != X2)) ) | spl7_1),
% 7.39/1.51 inference(forward_subsumption_resolution,[],[f238,f1022])).
% 7.39/1.51 thf(f4720,plain,(
% 7.39/1.51 ( ! [X0 : a] : ((((sK3 @ X0 @ sK6)) != X0) | ($false = ((sK1 @ X0))) | ($true = ((sK1 @ (sK4 @ sK6)))) | (((sK5 @ (sK2 @ sK6))) != X0)) ) | spl7_1),
% 7.39/1.51 inference(equality_resolution,[],[f4605])).
% 7.39/1.51 thf(f4721,plain,(
% 7.39/1.51 ( ! [X0 : a] : ((((sK5 @ (sK2 @ sK6))) != X0) | ($false = ((sK1 @ X0))) | (((sK3 @ X0 @ sK6)) != X0)) ) | spl7_1),
% 7.39/1.51 inference(forward_subsumption_resolution,[],[f4720,f1022])).
% 7.39/1.51 thf(f4722,plain,(
% 7.39/1.51 ($false = ((sK1 @ (sK5 @ (sK2 @ sK6))))) | (((sK5 @ (sK2 @ sK6))) != ((sK3 @ (sK5 @ (sK2 @ sK6)) @ sK6))) | spl7_1),
% 7.39/1.51 inference(equality_resolution,[],[f4721])).
% 7.39/1.51 thf(f4723,plain,(
% 7.39/1.51 ( ! [X2 : a,X0 : (a > a)] : ((((sK2 @ X0)) != ((sK2 @ sK6))) | ($true = ((sK1 @ (sK3 @ X2 @ sK6)))) | ($false = ((sK1 @ X2))) | ($true = ((sK1 @ (sK4 @ X0)))) | (((sK5 @ (sK2 @ X0))) != X2)) ) | spl7_1),
% 7.39/1.51 inference(forward_subsumption_resolution,[],[f334,f1022])).
% 7.39/1.51 thf(f4724,plain,(
% 7.39/1.51 ( ! [X0 : a] : (($true = ((sK1 @ (sK3 @ X0 @ sK6)))) | ($false = ((sK1 @ X0))) | ($true = ((sK1 @ (sK4 @ sK6)))) | (((sK5 @ (sK2 @ sK6))) != X0)) ) | spl7_1),
% 7.39/1.51 inference(equality_resolution,[],[f4723])).
% 7.39/1.51 thf(f4725,plain,(
% 7.39/1.51 ( ! [X0 : a] : ((((sK5 @ (sK2 @ sK6))) != X0) | ($false = ((sK1 @ X0))) | ($true = ((sK1 @ (sK3 @ X0 @ sK6))))) ) | spl7_1),
% 7.39/1.51 inference(forward_subsumption_resolution,[],[f4724,f1022])).
% 7.39/1.51 thf(f4726,plain,(
% 7.39/1.51 ($false = ((sK1 @ (sK5 @ (sK2 @ sK6))))) | ($true = ((sK1 @ (sK3 @ (sK5 @ (sK2 @ sK6)) @ sK6)))) | spl7_1),
% 7.39/1.51 inference(equality_resolution,[],[f4725])).
% 7.39/1.51 thf(f4727,plain,(
% 7.39/1.51 ( ! [X2 : a,X0 : (a > a)] : ((((sK2 @ X0)) != ((sK2 @ sK6))) | (((sK2 @ sK6)) = ((sK6 @ (sK3 @ X2 @ sK6)))) | ($false = ((sK1 @ X2))) | ($true = ((sK1 @ (sK4 @ X0)))) | (((sK5 @ (sK2 @ X0))) != X2)) ) | spl7_1),
% 7.39/1.51 inference(forward_subsumption_resolution,[],[f461,f1022])).
% 7.39/1.51 thf(f4729,definition,(
% 7.39/1.51 spl7_11 <=> ($true = ((sK1 @ (sK3 @ (sK5 @ (sK2 @ sK6)) @ sK6))))),
% 7.39/1.51 introduced(definition,[new_symbols(definition,[spl7_11])],[avatar_definition])).
% 7.39/1.51 thf(f4731,plain,(
% 7.39/1.51 ($true = ((sK1 @ (sK3 @ (sK5 @ (sK2 @ sK6)) @ sK6)))) | ~spl7_11),
% 7.39/1.51 inference(avatar_component_clause,[],[f4729])).
% 7.39/1.51 thf(f4733,definition,(
% 7.39/1.51 spl7_12 <=> ($false = ((sK1 @ (sK5 @ (sK2 @ sK6)))))),
% 7.39/1.51 introduced(definition,[new_symbols(definition,[spl7_12])],[avatar_definition])).
% 7.39/1.51 thf(f4735,plain,(
% 7.39/1.51 ($false = ((sK1 @ (sK5 @ (sK2 @ sK6))))) | ~spl7_12),
% 7.39/1.51 inference(avatar_component_clause,[],[f4733])).
% 7.39/1.51 thf(f4736,plain,(
% 7.39/1.51 spl7_11 | spl7_12 | spl7_1),
% 7.39/1.51 inference(avatar_split_clause,[],[f4726,f1021,f4733,f4729])).
% 7.39/1.51 thf(f4737,plain,(
% 7.39/1.51 ( ! [X0 : a] : ((((sK2 @ sK6)) = ((sK6 @ (sK3 @ X0 @ sK6)))) | ($false = ((sK1 @ X0))) | ($true = ((sK1 @ (sK4 @ sK6)))) | (((sK5 @ (sK2 @ sK6))) != X0)) ) | spl7_1),
% 7.39/1.51 inference(equality_resolution,[],[f4727])).
% 7.39/1.51 thf(f4738,plain,(
% 7.39/1.51 ( ! [X0 : a] : ((((sK5 @ (sK2 @ sK6))) != X0) | ($false = ((sK1 @ X0))) | (((sK2 @ sK6)) = ((sK6 @ (sK3 @ X0 @ sK6))))) ) | spl7_1),
% 7.39/1.51 inference(forward_subsumption_resolution,[],[f4737,f1022])).
% 7.39/1.51 thf(f5319,plain,(
% 7.39/1.51 ($false = ((sK1 @ (sK5 @ (sK2 @ sK6))))) | (((sK2 @ sK6)) = ((sK6 @ (sK3 @ (sK5 @ (sK2 @ sK6)) @ sK6)))) | spl7_1),
% 7.39/1.51 inference(equality_resolution,[],[f4738])).
% 7.39/1.51 thf(f7218,definition,(
% 7.39/1.51 spl7_13 <=> (((sK5 @ (sK2 @ sK6))) = ((sK3 @ (sK5 @ (sK2 @ sK6)) @ sK6)))),
% 7.39/1.51 introduced(definition,[new_symbols(definition,[spl7_13])],[avatar_definition])).
% 7.39/1.51 thf(f7220,plain,(
% 7.39/1.51 (((sK5 @ (sK2 @ sK6))) != ((sK3 @ (sK5 @ (sK2 @ sK6)) @ sK6))) | spl7_13),
% 7.39/1.51 inference(avatar_component_clause,[],[f7218])).
% 7.39/1.51 thf(f7221,plain,(
% 7.39/1.51 ~spl7_13 | spl7_12 | spl7_1),
% 7.39/1.51 inference(avatar_split_clause,[],[f4722,f1021,f4733,f7218])).
% 7.39/1.51 thf(f7365,definition,(
% 7.39/1.51 spl7_14 <=> (((sK2 @ sK6)) = ((sK6 @ (sK3 @ (sK5 @ (sK2 @ sK6)) @ sK6))))),
% 7.39/1.51 introduced(definition,[new_symbols(definition,[spl7_14])],[avatar_definition])).
% 7.39/1.51 thf(f7367,plain,(
% 7.39/1.51 (((sK2 @ sK6)) = ((sK6 @ (sK3 @ (sK5 @ (sK2 @ sK6)) @ sK6)))) | ~spl7_14),
% 7.39/1.51 inference(avatar_component_clause,[],[f7365])).
% 7.39/1.51 thf(f7368,plain,(
% 7.39/1.51 spl7_14 | spl7_12 | spl7_1),
% 7.39/1.51 inference(avatar_split_clause,[],[f5319,f1021,f4733,f7365])).
% 7.39/1.51 thf(f7370,plain,(
% 7.39/1.51 ($true = $false) | ($true = ((sK1 @ (sK4 @ sK6)))) | ~spl7_12),
% 7.39/1.51 inference(constrained_superposition,[],[f4735,f25])).
% 7.39/1.51 thf(f7387,plain,(
% 7.39/1.51 ($true = ((sK1 @ (sK4 @ sK6)))) | ~spl7_12),
% 7.39/1.51 inference(trivial_inequality_removal,[],[f7370])).
% 7.39/1.51 thf(f7390,plain,(
% 7.39/1.51 $false | (spl7_1 | ~spl7_12)),
% 7.39/1.51 inference(forward_subsumption_resolution,[],[f7387,f1022])).
% 7.39/1.51 thf(f7391,plain,(
% 7.39/1.51 spl7_1 | ~spl7_12),
% 7.39/1.51 inference(avatar_contradiction_clause,[],[f7390])).
% 7.39/1.51 thf(f7601,plain,(
% 7.39/1.51 (((sK5 @ (sK2 @ sK6))) = ((sK3 @ (sK5 @ (sK2 @ sK6)) @ sK6))) | ($false = ((sK1 @ (sK3 @ (sK5 @ (sK2 @ sK6)) @ sK6)))) | ~spl7_14),
% 7.39/1.51 inference(constrained_superposition,[],[f107,f7367])).
% 7.39/1.51 thf(f7782,plain,(
% 7.39/1.51 ($false = ((sK1 @ (sK3 @ (sK5 @ (sK2 @ sK6)) @ sK6)))) | (spl7_13 | ~spl7_14)),
% 7.39/1.51 inference(forward_subsumption_resolution,[],[f7601,f7220])).
% 7.39/1.51 thf(f8599,plain,(
% 7.39/1.51 ($true = $false) | (~spl7_11 | spl7_13 | ~spl7_14)),
% 7.39/1.51 inference(constrained_superposition,[],[f7782,f4731])).
% 7.39/1.51 thf(f8613,plain,(
% 7.39/1.51 $false | (~spl7_11 | spl7_13 | ~spl7_14)),
% 7.39/1.51 inference(trivial_inequality_removal,[],[f8599])).
% 7.39/1.51 thf(f8614,plain,(
% 7.39/1.51 ~spl7_11 | spl7_13 | ~spl7_14),
% 7.39/1.51 inference(avatar_contradiction_clause,[],[f8613])).
% 7.39/1.51 cnf(s8, plain, ~spl7_1, inference(sat_conversion,[],[f4589])).
% 7.39/1.51 cnf(s9, plain, spl7_1 | spl7_11 | spl7_12, inference(sat_conversion,[],[f4736])).
% 7.39/1.51 cnf(s10, plain, spl7_1 | spl7_12 | ~spl7_13, inference(sat_conversion,[],[f7221])).
% 7.39/1.51 cnf(s11, plain, spl7_1 | spl7_12 | spl7_14, inference(sat_conversion,[],[f7368])).
% 7.39/1.51 cnf(s13, plain, spl7_1 | ~spl7_12, inference(sat_conversion,[],[f7391])).
% 7.39/1.51 cnf(s15, plain, ~spl7_11 | spl7_13 | ~spl7_14, inference(sat_conversion,[],[f8614])).
% 7.39/1.51 cnf(s16, plain, ~spl7_12, inference(rat,[],[s13,s8])).
% 7.39/1.51 cnf(s17, plain, spl7_11, inference(rat,[],[s9,s16,s8])).
% 7.39/1.51 cnf(s18, plain, spl7_14, inference(rat,[],[s11,s8,s16])).
% 7.39/1.51 cnf(s19, plain, ~spl7_13, inference(rat,[],[s10,s8,s16])).
% 7.39/1.51 cnf(s20, plain, $false, inference(rat,[],[s15,s18,s19,s17])).
% 7.39/1.51 thf(f8615,plain,(
% 7.39/1.51 $false),
% 7.39/1.51 inference(avatar_sat_refutation,[],[s20])).
% 7.39/1.51 % SZS output end Proof for theBenchmark
% 7.39/1.51 % (3481865)------------------------------
% 7.39/1.51 % (3481865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.39/1.51 % (3481865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.51 % (3481865)CaDiCaL version: 2.1.3
% 7.39/1.51 % (3481865)Termination reason: Refutation
% 7.39/1.51 % (3481865)Time elapsed: 0.580 s
% 7.39/1.51 % (3481865)Peak memory usage: 15 MB
% 7.39/1.51 % (3481865)Instructions burned: 1372 (million)
% 7.39/1.51 % (3481820)Success in time 1.173 s
% 7.39/1.51 % Vampire exiting
%------------------------------------------------------------------------------