%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU477^1 : TPTP v9.3.1. Released v3.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:32:09 AM UTC 2026
% Result : Theorem 2.52s 0.63s
% Output : Refutation 2.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU477^1 : TPTP v9.3.1. Released v3.6.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.18 % Computer : n010.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Tue Sep 29 13:43:18 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.21 Running first-order model finding
% 0.07/0.21 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
% 2.52/0.63 % (2873978)Will run a generic schedule for satisfiability detection.
% 2.52/0.63 % (2873995)dis+10_1_sil=32000:sp=arity:random_seed=1526715699:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 2.52/0.63 % (2873993)% WARNING: option uhcvi not known.
% 2.52/0.63 % (2873993)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=154445331:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 2.52/0.63 % (2873994)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2230771020:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 2.52/0.63 % (2873993)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.52/0.63 % (2873993)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 2.52/0.63 % (2873998)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3254505740:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 2.52/0.63 % (2873992)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=129308918_2999 on theBenchmark for (2999ds/0Mi)
% 2.52/0.63 % Exception at run slice level
% 2.52/0.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.52/0.63 % (2873995)Instruction limit reached!
% 2.52/0.63 % (2873995)------------------------------
% 2.52/0.63 % (2873995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.52/0.63 % (2873995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.52/0.63 % (2873995)CaDiCaL version: 2.1.3
% 2.52/0.63 % (2873995)Termination reason: Instruction limit
% 2.52/0.63 % (2873995)Termination phase: Saturation
% 2.52/0.63 % (2873995)Time elapsed: 0.028 s
% 2.52/0.63 % (2873995)Peak memory usage: 12 MB
% 2.52/0.63 % (2873995)Instructions burned: 104 (million)
% 2.52/0.63 % (2873996)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1965754650:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 2.52/0.63 % (2873997)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3640257406:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 2.52/0.63 % (2874007)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1443937342:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 2.52/0.63 % (2873996)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.52/0.63 % (2874006)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1943571482:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 2.52/0.63 % Exception at run slice level
% 2.52/0.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.52/0.63 % (2874013)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=2113242003:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 2.52/0.63 % (2874007)Instruction limit reached!
% 2.52/0.63 % (2874007)------------------------------
% 2.52/0.63 % (2874007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.52/0.63 % (2874007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.52/0.63 % (2874007)CaDiCaL version: 2.1.3
% 2.52/0.63 % (2874007)Termination reason: Instruction limit
% 2.52/0.63 % (2874007)Termination phase: Saturation
% 2.52/0.63 % (2874007)Time elapsed: 0.039 s
% 2.52/0.63 % (2874007)Peak memory usage: 13 MB
% 2.52/0.63 % (2874007)Instructions burned: 134 (million)
% 2.52/0.63 % (2874013)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.52/0.63 % (2874013)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 2.52/0.63 % (2874015)ott-21_1_sil=16000:fs=off:random_seed=3039689771:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 2.52/0.63 % (2873998)Instruction limit reached!
% 2.52/0.63 % (2873998)------------------------------
% 2.52/0.63 % (2873998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.52/0.63 % (2873998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.52/0.63 % (2873998)CaDiCaL version: 2.1.3
% 2.52/0.63 % (2873998)Termination reason: Instruction limit
% 2.52/0.63 % (2873998)Termination phase: Saturation
% 2.52/0.63 % (2873998)Time elapsed: 0.092 s
% 2.52/0.63 % (2873998)Peak memory usage: 13 MB
% 2.52/0.63 % (2873998)Instructions burned: 160 (million)
% 2.52/0.63 % (2874017)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2684814402:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 2.52/0.63 % (2873997)Instruction limit reached!
% 2.52/0.63 % (2873997)------------------------------
% 2.52/0.63 % (2873997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.52/0.63 % (2873997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.52/0.63 % (2873997)CaDiCaL version: 2.1.3
% 2.52/0.63 % (2873997)Termination reason: Instruction limit
% 2.52/0.63 % (2873997)Termination phase: Saturation
% 2.52/0.63 % (2873997)Time elapsed: 0.094 s
% 2.52/0.63 % (2873997)Peak memory usage: 12 MB
% 2.52/0.63 % (2873997)Instructions burned: 133 (million)
% 2.52/0.63 % (2874015)Instruction limit reached!
% 2.52/0.63 % (2874015)------------------------------
% 2.52/0.63 % (2874015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.52/0.63 % (2874015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.52/0.63 % (2874015)CaDiCaL version: 2.1.3
% 2.52/0.63 % (2874015)Termination reason: Instruction limit
% 2.52/0.63 % (2874015)Termination phase: Saturation
% 2.52/0.63 % (2874015)Time elapsed: 0.042 s
% 2.52/0.63 % (2874015)Peak memory usage: 13 MB
% 2.52/0.63 % (2874015)Instructions burned: 184 (million)
% 2.52/0.63 % (2874020)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1652241213:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 2.52/0.63 % (2874019)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2463947743:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 2.52/0.63 % (2873996)Instruction limit reached!
% 2.52/0.63 % (2873996)------------------------------
% 2.52/0.63 % (2873996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.52/0.63 % (2873996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.52/0.63 % (2873996)CaDiCaL version: 2.1.3
% 2.52/0.63 % (2873996)Termination reason: Instruction limit
% 2.52/0.63 % (2873996)Termination phase: Saturation
% 2.52/0.63 % (2873996)Time elapsed: 0.118 s
% 2.52/0.63 % (2873996)Peak memory usage: 12 MB
% 2.52/0.63 % (2873996)Instructions burned: 116 (million)
% 2.52/0.63 % Exception at run slice level
% 2.52/0.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.52/0.63 % (2874023)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1643540288:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 2.52/0.63 % (2874024)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=3982074325:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 2.52/0.63 % (2874024)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.52/0.63 % Exception at run slice level
% 2.52/0.63 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.52/0.63 % (2874027)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2044498285:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 2.52/0.63 % (2874027)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.52/0.63 % (2874013) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2873978-2874013"...
% 2.52/0.63 % (2874017)Instruction limit reached!
% 2.52/0.63 % (2874017)------------------------------
% 2.52/0.63 % (2874017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.52/0.63 % (2874017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.52/0.63 % (2874017)CaDiCaL version: 2.1.3
% 2.52/0.63 % (2874017)Termination reason: Instruction limit
% 2.52/0.63 % (2874017)Termination phase: Saturation
% 2.52/0.63 % (2874017)Time elapsed: 0.243 s
% 2.52/0.63 % (2874017)Peak memory usage: 14 MB
% 2.52/0.63 % (2874017)Instructions burned: 478 (million)
% 2.52/0.63 % (2874013)...printing done.
% 2.52/0.63 % (2874013)Refutation found. Thanks to Tanya!
% 2.52/0.63 % SZS status Theorem for theBenchmark
% 2.52/0.63 % SZS output start Proof for theBenchmark
% 2.52/0.63 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 2.52/0.63 thf(func_def_0, type, subrel: (($i > $i > $o) > ($i > $i > $o) > $o)).
% 2.52/0.63 thf(func_def_2, type, inv: (($i > $i > $o) > $i > $i > $o)).
% 2.52/0.63 thf(func_def_3, type, idem: ((($i > $i > $o) > $i > $i > $o) > $o)).
% 2.52/0.63 thf(func_def_4, type, infl: ((($i > $i > $o) > $i > $i > $o) > $o)).
% 2.52/0.63 thf(func_def_5, type, mono: ((($i > $i > $o) > $i > $i > $o) > $o)).
% 2.52/0.63 thf(func_def_6, type, refl: (($i > $i > $o) > $o)).
% 2.52/0.63 thf(func_def_7, type, irrefl: (($i > $i > $o) > $o)).
% 2.52/0.63 thf(func_def_8, type, rc: (($i > $i > $o) > $i > $i > $o)).
% 2.52/0.63 thf(func_def_9, type, symm: (($i > $i > $o) > $o)).
% 2.52/0.63 thf(func_def_10, type, antisymm: (($i > $i > $o) > $o)).
% 2.52/0.63 thf(func_def_11, type, asymm: (($i > $i > $o) > $o)).
% 2.52/0.63 thf(func_def_12, type, sc: (($i > $i > $o) > $i > $i > $o)).
% 2.52/0.63 thf(func_def_13, type, trans: (($i > $i > $o) > $o)).
% 2.52/0.63 thf(func_def_14, type, tc: (($i > $i > $o) > $i > $i > $o)).
% 2.52/0.63 thf(func_def_15, type, trc: (($i > $i > $o) > $i > $i > $o)).
% 2.52/0.63 thf(func_def_16, type, trsc: (($i > $i > $o) > $i > $i > $o)).
% 2.52/0.63 thf(func_def_17, type, po: (($i > $i > $o) > $o)).
% 2.52/0.63 thf(func_def_18, type, so: (($i > $i > $o) > $o)).
% 2.52/0.63 thf(func_def_19, type, total: (($i > $i > $o) > $o)).
% 2.52/0.63 thf(func_def_20, type, term: (($i > $i > $o) > $o)).
% 2.52/0.63 thf(func_def_21, type, ind: (($i > $i > $o) > $o)).
% 2.52/0.63 thf(func_def_22, type, innf: (($i > $i > $o) > $i > $o)).
% 2.52/0.63 thf(func_def_23, type, nfof: (($i > $i > $o) > $i > $i > $o)).
% 2.52/0.63 thf(func_def_24, type, norm: (($i > $i > $o) > $o)).
% 2.52/0.63 thf(func_def_25, type, join: (($i > $i > $o) > $i > $i > $o)).
% 2.52/0.63 thf(func_def_26, type, lconfl: (($i > $i > $o) > $o)).
% 2.52/0.63 thf(func_def_27, type, sconfl: (($i > $i > $o) > $o)).
% 2.52/0.63 thf(func_def_28, type, confl: (($i > $i > $o) > $o)).
% 2.52/0.63 thf(func_def_29, type, cr: (($i > $i > $o) > $o)).
% 2.52/0.63 thf(func_def_30, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 2.52/0.63 thf(func_def_31, type, vIMP: ($o > $o > $o)).
% 2.52/0.63 thf(func_def_32, type, db3: !>[X0: $tType]:(X0)).
% 2.52/0.63 thf(func_def_33, type, db0: !>[X0: $tType]:(X0)).
% 2.52/0.63 thf(func_def_34, type, db1: !>[X0: $tType]:(X0)).
% 2.52/0.63 thf(func_def_35, type, db2: !>[X0: $tType]:(X0)).
% 2.52/0.63 thf(func_def_36, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 2.52/0.63 thf(func_def_37, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 2.52/0.63 thf(func_def_38, type, vNOT: ($o > $o)).
% 2.52/0.63 thf(func_def_39, type, vOR: ($o > $o > $o)).
% 2.52/0.63 thf(func_def_40, type, vAND: ($o > $o > $o)).
% 2.52/0.63 thf(func_def_41, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 2.52/0.63 thf(func_def_44, type, sK0: ($i > $i > $o)).
% 2.52/0.63 thf(func_def_45, type, sK1: ($i > $o)).
% 2.52/0.63 thf(func_def_46, type, sK2: ($i > $o)).
% 2.52/0.63 thf(func_def_49, type, sK5: ($i > $i)).
% 2.52/0.63 thf(func_def_51, type, sK7: ($i > $i)).
% 2.52/0.63 thf(func_def_52, type, sK8: ($i > $i)).
% 2.52/0.63 thf(func_def_53, type, sK9: ($i > $i)).
% 2.52/0.63 thf(func_def_54, type, sK10: (($i > $o) > $i)).
% 2.52/0.63 thf(func_def_55, type, sK11: (($i > $o) > $i)).
% 2.52/0.63 thf(f20,axiom,(
% 2.52/0.63 (term = (^[X0 : ($i > $i > $o)] : (! [X1 : ($i > $o)] : (? [X2 : $i] : (X1 @ X2) => ? [X2 : $i] : (! [X3 : $i] : ((X1 @ X3) => ~(X0 @ X2 @ X3)) & (X1 @ X2))))))),
% 2.52/0.63 file('/export/starexec/sandbox/benchmark/Axioms/SET009^0.ax',terminating)).
% 2.52/0.63 thf(f30,conjecture,(
% 2.52/0.63 (term = (^[X0 : ($i > $i > $o)] : (~ ? [X1 : ($i > $o)] : (! [X2 : $i] : ((X1 @ X2) => ? [X3 : $i] : ((X0 @ X2 @ X3) & (X1 @ X3))) & ? [X2 : $i] : (X1 @ X2)))))),
% 2.52/0.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p',alternative_formulation_of_terminating)).
% 2.52/0.63 thf(f31,negated_conjecture,(
% 2.52/0.63 ~ (term = (^[X0 : ($i > $i > $o)] : (~ ? [X1 : ($i > $o)] : (! [X2 : $i] : ((X1 @ X2) => ? [X3 : $i] : ((X0 @ X2 @ X3) & (X1 @ X3))) & ? [X2 : $i] : (X1 @ X2)))))),
% 2.52/0.63 inference(negated_conjecture,[status(cth)],[f30])).
% 2.52/0.63 thf(f66,plain,(
% 2.52/0.63 (term = (^[X0 : ($i > $i > $o)] : (! [X1 : ($i > $o)] : (? [X2 : $i] : (X1 @ X2) => ? [X3 : $i] : (! [X4 : $i] : ((X1 @ X4) => ~(X0 @ X3 @ X4)) & (X1 @ X3))))))),
% 2.52/0.63 inference(rectify,[],[f20])).
% 2.52/0.63 thf(f67,plain,(
% 2.52/0.63 (term = (^[Y0 : $i > $i > $o]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: ((?? @ $i @ (^[Y2 : $i]: (Y1 @ Y2))) => (?? @ $i @ (^[Y2 : $i]: ((Y1 @ Y2) & (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) => (~ (Y0 @ Y2 @ Y3)))))))))))))),
% 2.52/0.63 inference(fool_elimination,[],[f66])).
% 2.52/0.63 thf(f86,plain,(
% 2.52/0.63 ~ (term = (^[X0 : ($i > $i > $o)] : (~ ? [X1 : ($i > $o)] : (! [X2 : $i] : ((X1 @ X2) => ? [X3 : $i] : ((X0 @ X2 @ X3) & (X1 @ X3))) & ? [X4 : $i] : (X1 @ X4)))))),
% 2.52/0.63 inference(rectify,[],[f31])).
% 2.52/0.63 thf(f87,plain,(
% 2.52/0.63 ~ (term = (^[Y0 : $i > $i > $o]: (~ (?? @ ($i > $o) @ (^[Y1 : $i > $o]: ((?? @ $i @ (^[Y2 : $i]: (Y1 @ Y2))) & (!! @ $i @ (^[Y2 : $i]: ((Y1 @ Y2) => (?? @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) & (Y0 @ Y2 @ Y3)))))))))))))),
% 2.52/0.63 inference(fool_elimination,[],[f86])).
% 2.52/0.63 thf(f88,plain,(
% 2.52/0.63 (term != (^[Y0 : $i > $i > $o]: (~ (?? @ ($i > $o) @ (^[Y1 : $i > $o]: ((?? @ $i @ (^[Y2 : $i]: (Y1 @ Y2))) & (!! @ $i @ (^[Y2 : $i]: ((Y1 @ Y2) => (?? @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) & (Y0 @ Y2 @ Y3)))))))))))))),
% 2.52/0.63 inference(flattening,[],[f87])).
% 2.52/0.63 thf(f108,plain,(
% 2.52/0.63 (term = (^[Y0 : $i > $i > $o]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: ((?? @ $i @ (^[Y2 : $i]: (Y1 @ Y2))) => (?? @ $i @ (^[Y2 : $i]: ((Y1 @ Y2) & (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) => (~ (Y0 @ Y2 @ Y3)))))))))))))),
% 2.52/0.63 inference(cnf_transformation,[],[f67])).
% 2.52/0.63 thf(f118,plain,(
% 2.52/0.63 (term != (^[Y0 : $i > $i > $o]: (~ (?? @ ($i > $o) @ (^[Y1 : $i > $o]: ((?? @ $i @ (^[Y2 : $i]: (Y1 @ Y2))) & (!! @ $i @ (^[Y2 : $i]: ((Y1 @ Y2) => (?? @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) & (Y0 @ Y2 @ Y3)))))))))))))),
% 2.52/0.63 inference(cnf_transformation,[],[f88])).
% 2.52/0.63 thf(f120,definition,(
% 2.52/0.63 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 2.52/0.63 introduced(theory,[fool_exhaustiveness_axiom])).
% 2.52/0.63 thf(f136,plain,(
% 2.52/0.63 ((^[Y0 : $i > $i > $o]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: ((?? @ $i @ (^[Y2 : $i]: (Y1 @ Y2))) => (?? @ $i @ (^[Y2 : $i]: ((Y1 @ Y2) & (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) => (~ (Y0 @ Y2 @ Y3)))))))))))) != (^[Y0 : $i > $i > $o]: (~ (?? @ ($i > $o) @ (^[Y1 : $i > $o]: ((?? @ $i @ (^[Y2 : $i]: (Y1 @ Y2))) & (!! @ $i @ (^[Y2 : $i]: ((Y1 @ Y2) => (?? @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) & (Y0 @ Y2 @ Y3)))))))))))))),
% 2.52/0.63 inference(definition_unfolding,[],[f118,f108])).
% 2.52/0.63 thf(f137,plain,(
% 2.52/0.63 ((^[Y0 : $i > $i > $o]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: ((?? @ $i @ Y1) => (?? @ $i @ (^[Y2 : $i]: ((Y1 @ Y2) & (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) => (~ (Y0 @ Y2 @ Y3)))))))))))) != (^[Y0 : $i > $i > $o]: (~ (?? @ ($i > $o) @ (^[Y1 : $i > $o]: ((?? @ $i @ Y1) & (!! @ $i @ (^[Y2 : $i]: ((Y1 @ Y2) => (?? @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) & (Y0 @ Y2 @ Y3)))))))))))))),
% 2.52/0.63 inference(beta-eta_normalization,[],[f136])).
% 2.52/0.63 thf(f138,plain,(
% 2.52/0.63 ((((^[Y0 : $i > $i > $o]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: ((?? @ $i @ Y1) => (?? @ $i @ (^[Y2 : $i]: ((Y1 @ Y2) & (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) => (~ (Y0 @ Y2 @ Y3)))))))))))) @ sK0)) != (((^[Y0 : $i > $i > $o]: (~ (?? @ ($i > $o) @ (^[Y1 : $i > $o]: ((?? @ $i @ Y1) & (!! @ $i @ (^[Y2 : $i]: ((Y1 @ Y2) => (?? @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) & (Y0 @ Y2 @ Y3)))))))))))) @ sK0)))),
% 2.52/0.63 inference(negative_extensionality,[],[f137])).
% 2.52/0.63 thf(f139,plain,(
% 2.52/0.63 ($true = (((^[Y0 : $i > $i > $o]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: ((?? @ $i @ Y1) => (?? @ $i @ (^[Y2 : $i]: ((Y1 @ Y2) & (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) => (~ (Y0 @ Y2 @ Y3)))))))))))) @ sK0))) | ($true = (((^[Y0 : $i > $i > $o]: (~ (?? @ ($i > $o) @ (^[Y1 : $i > $o]: ((?? @ $i @ Y1) & (!! @ $i @ (^[Y2 : $i]: ((Y1 @ Y2) => (?? @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) & (Y0 @ Y2 @ Y3)))))))))))) @ sK0)))),
% 2.52/0.63 inference(xor_proxy_clausification,[],[f138])).
% 2.52/0.63 thf(f140,plain,(
% 2.52/0.63 ($false = (((^[Y0 : $i > $i > $o]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: ((?? @ $i @ Y1) => (?? @ $i @ (^[Y2 : $i]: ((Y1 @ Y2) & (!! @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) => (~ (Y0 @ Y2 @ Y3)))))))))))) @ sK0))) | ($false = (((^[Y0 : $i > $i > $o]: (~ (?? @ ($i > $o) @ (^[Y1 : $i > $o]: ((?? @ $i @ Y1) & (!! @ $i @ (^[Y2 : $i]: ((Y1 @ Y2) => (?? @ $i @ (^[Y3 : $i]: ((Y1 @ Y3) & (Y0 @ Y2 @ Y3)))))))))))) @ sK0)))),
% 2.52/0.63 inference(xor_proxy_clausification,[],[f138])).
% 2.52/0.63 thf(f141,plain,(
% 2.52/0.63 ($false = ((!! @ ($i > $o) @ (^[Y0 : $i > $o]: ((?? @ $i @ Y0) => (?? @ $i @ (^[Y1 : $i]: ((Y0 @ Y1) & (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) => (~ (sK0 @ Y1 @ Y2))))))))))))) | ($false = ((~ (?? @ ($i > $o) @ (^[Y0 : $i > $o]: ((?? @ $i @ Y0) & (!! @ $i @ (^[Y1 : $i]: ((Y0 @ Y1) => (?? @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) & (sK0 @ Y1 @ Y2)))))))))))))),
% 2.52/0.63 inference(beta-eta_normalization,[],[f140])).
% 2.52/0.63 thf(f142,plain,(
% 2.52/0.63 ($false = (((^[Y0 : $i > $o]: ((?? @ $i @ Y0) => (?? @ $i @ (^[Y1 : $i]: ((Y0 @ Y1) & (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) => (~ (sK0 @ Y1 @ Y2)))))))))) @ sK1))) | ($false = ((~ (?? @ ($i > $o) @ (^[Y0 : $i > $o]: ((?? @ $i @ Y0) & (!! @ $i @ (^[Y1 : $i]: ((Y0 @ Y1) => (?? @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) & (sK0 @ Y1 @ Y2)))))))))))))),
% 2.52/0.63 inference(sigma_proxy_clausification,[],[f141])).
% 2.52/0.63 thf(f143,plain,(
% 2.52/0.63 ($false = (((^[Y0 : $i > $o]: ((?? @ $i @ Y0) => (?? @ $i @ (^[Y1 : $i]: ((Y0 @ Y1) & (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) => (~ (sK0 @ Y1 @ Y2)))))))))) @ sK1))) | ($true = ((?? @ ($i > $o) @ (^[Y0 : $i > $o]: ((?? @ $i @ Y0) & (!! @ $i @ (^[Y1 : $i]: ((Y0 @ Y1) => (?? @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) & (sK0 @ Y1 @ Y2))))))))))))),
% 2.52/0.63 inference(not_proxy_clausification,[],[f142])).
% 2.52/0.63 thf(f144,plain,(
% 2.52/0.63 ($false = (((^[Y0 : $i > $o]: ((?? @ $i @ Y0) => (?? @ $i @ (^[Y1 : $i]: ((Y0 @ Y1) & (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) => (~ (sK0 @ Y1 @ Y2)))))))))) @ sK1))) | ($true = (((^[Y0 : $i > $o]: ((?? @ $i @ Y0) & (!! @ $i @ (^[Y1 : $i]: ((Y0 @ Y1) => (?? @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) & (sK0 @ Y1 @ Y2))))))))) @ sK2)))),
% 2.52/0.63 inference(sigma_proxy_clausification,[],[f143])).
% 2.52/0.63 thf(f145,plain,(
% 2.52/0.63 ($false = (((?? @ $i @ sK1) => (?? @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) & (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) => (~ (sK0 @ Y0 @ Y1))))))))))) | ($true = (((?? @ $i @ sK2) & (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) => (?? @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) & (sK0 @ Y0 @ Y1))))))))))),
% 2.52/0.63 inference(beta-eta_normalization,[],[f144])).
% 2.52/0.63 thf(f146,plain,(
% 2.52/0.63 ($false = ((?? @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) & (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) => (~ (sK0 @ Y0 @ Y1)))))))))) | ($true = (((?? @ $i @ sK2) & (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) => (?? @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) & (sK0 @ Y0 @ Y1))))))))))),
% 2.52/0.63 inference(imp_proxy_clausification,[],[f145])).
% 2.52/0.63 thf(f147,plain,(
% 2.52/0.63 ($true = ((?? @ $i @ sK1))) | ($true = (((?? @ $i @ sK2) & (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) => (?? @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) & (sK0 @ Y0 @ Y1))))))))))),
% 2.52/0.63 inference(imp_proxy_clausification,[],[f145])).
% 2.52/0.63 thf(f148,plain,(
% 2.52/0.63 ($true = ((sK1 @ sK3))) | ($true = (((?? @ $i @ sK2) & (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) => (?? @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) & (sK0 @ Y0 @ Y1))))))))))),
% 2.52/0.63 inference(sigma_proxy_clausification,[],[f147])).
% 2.52/0.63 thf(f149,plain,(
% 2.52/0.63 ($true = ((sK1 @ sK3))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) => (?? @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) & (sK0 @ Y0 @ Y1)))))))))),
% 2.52/0.63 inference(and_proxy_clausification,[],[f148])).
% 2.52/0.63 thf(f150,plain,(
% 2.52/0.63 ($true = ((sK1 @ sK3))) | ($true = ((?? @ $i @ sK2)))),
% 2.52/0.63 inference(and_proxy_clausification,[],[f148])).
% 2.52/0.63 thf(f151,plain,(
% 2.52/0.63 ($true = ((sK1 @ sK3))) | ($true = ((sK2 @ sK4)))),
% 2.52/0.63 inference(sigma_proxy_clausification,[],[f150])).
% 2.52/0.63 thf(f152,plain,(
% 2.52/0.63 ( ! [X1 : $i] : (($true = ((sK1 @ sK3))) | ($true = (((^[Y0 : $i]: ((sK2 @ Y0) => (?? @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) & (sK0 @ Y0 @ Y1)))))) @ X1)))) )),
% 2.52/0.63 inference(pi_proxy_clausification,[],[f149])).
% 2.52/0.63 thf(f153,plain,(
% 2.52/0.63 ( ! [X1 : $i] : (($true = ((sK1 @ sK3))) | ($true = (((sK2 @ X1) => (?? @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) & (sK0 @ X1 @ Y0)))))))) )),
% 2.52/0.63 inference(beta-eta_normalization,[],[f152])).
% 2.52/0.63 thf(f154,plain,(
% 2.52/0.63 ( ! [X1 : $i] : (($true = ((sK1 @ sK3))) | ($false = ((sK2 @ X1))) | ($true = ((?? @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) & (sK0 @ X1 @ Y0))))))) )),
% 2.52/0.63 inference(imp_proxy_clausification,[],[f153])).
% 2.52/0.63 thf(f155,plain,(
% 2.52/0.63 ( ! [X1 : $i] : (($true = ((sK1 @ sK3))) | ($false = ((sK2 @ X1))) | ($true = (((^[Y0 : $i]: ((sK2 @ Y0) & (sK0 @ X1 @ Y0))) @ (sK5 @ X1))))) )),
% 2.52/0.63 inference(sigma_proxy_clausification,[],[f154])).
% 2.52/0.63 thf(f156,plain,(
% 2.52/0.63 ( ! [X1 : $i] : (($true = ((sK1 @ sK3))) | ($false = ((sK2 @ X1))) | ($true = (((sK2 @ (sK5 @ X1)) & (sK0 @ X1 @ (sK5 @ X1)))))) )),
% 2.52/0.63 inference(beta-eta_normalization,[],[f155])).
% 2.52/0.63 thf(f157,plain,(
% 2.52/0.63 ( ! [X1 : $i] : (($true = ((sK1 @ sK3))) | ($false = ((sK2 @ X1))) | ($true = ((sK0 @ X1 @ (sK5 @ X1))))) )),
% 2.52/0.63 inference(and_proxy_clausification,[],[f156])).
% 2.52/0.63 thf(f158,plain,(
% 2.52/0.63 ( ! [X1 : $i] : (($true = ((sK1 @ sK3))) | ($false = ((sK2 @ X1))) | ($true = ((sK2 @ (sK5 @ X1))))) )),
% 2.52/0.63 inference(and_proxy_clausification,[],[f156])).
% 2.52/0.63 thf(f159,plain,(
% 2.52/0.63 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((sK1 @ Y0) & (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) => (~ (sK0 @ Y0 @ Y1))))))) @ X1))) | ($true = (((?? @ $i @ sK2) & (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) => (?? @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) & (sK0 @ Y0 @ Y1))))))))))) )),
% 2.52/0.63 inference(pi_proxy_clausification,[],[f146])).
% 2.52/0.63 thf(f160,plain,(
% 2.52/0.63 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((sK1 @ Y0) & (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) => (~ (sK0 @ Y0 @ Y1))))))) @ X1))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) => (?? @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) & (sK0 @ Y0 @ Y1)))))))))) )),
% 2.52/0.63 inference(and_proxy_clausification,[],[f159])).
% 2.52/0.63 thf(f161,plain,(
% 2.52/0.63 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((sK1 @ Y0) & (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) => (~ (sK0 @ Y0 @ Y1))))))) @ X1))) | ($true = ((?? @ $i @ sK2)))) )),
% 2.52/0.63 inference(and_proxy_clausification,[],[f159])).
% 2.52/0.63 thf(f162,plain,(
% 2.52/0.63 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((sK1 @ Y0) & (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) => (~ (sK0 @ Y0 @ Y1))))))) @ X1))) | ($true = ((sK2 @ sK6)))) )),
% 2.52/0.63 inference(sigma_proxy_clausification,[],[f161])).
% 2.52/0.63 thf(f163,plain,(
% 2.52/0.63 ( ! [X1 : $i] : (($false = (((sK1 @ X1) & (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) => (~ (sK0 @ X1 @ Y0)))))))) | ($true = ((sK2 @ sK6)))) )),
% 2.52/0.63 inference(beta-eta_normalization,[],[f162])).
% 2.52/0.63 thf(f164,plain,(
% 2.52/0.63 ( ! [X1 : $i] : (($false = ((!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) => (~ (sK0 @ X1 @ Y0))))))) | ($true = ((sK2 @ sK6))) | ($false = ((sK1 @ X1)))) )),
% 2.52/0.63 inference(and_proxy_clausification,[],[f163])).
% 2.52/0.63 thf(f165,plain,(
% 2.52/0.63 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((sK1 @ Y0) => (~ (sK0 @ X1 @ Y0)))) @ (sK7 @ X1)))) | ($true = ((sK2 @ sK6))) | ($false = ((sK1 @ X1)))) )),
% 2.52/0.63 inference(sigma_proxy_clausification,[],[f164])).
% 2.52/0.63 thf(f166,plain,(
% 2.52/0.63 ( ! [X1 : $i] : (($false = (((sK1 @ (sK7 @ X1)) => (~ (sK0 @ X1 @ (sK7 @ X1)))))) | ($true = ((sK2 @ sK6))) | ($false = ((sK1 @ X1)))) )),
% 2.52/0.63 inference(beta-eta_normalization,[],[f165])).
% 2.52/0.63 thf(f167,plain,(
% 2.52/0.63 ( ! [X1 : $i] : (($false = ((~ (sK0 @ X1 @ (sK7 @ X1))))) | ($true = ((sK2 @ sK6))) | ($false = ((sK1 @ X1)))) )),
% 2.52/0.63 inference(imp_proxy_clausification,[],[f166])).
% 2.52/0.63 thf(f168,plain,(
% 2.52/0.63 ( ! [X1 : $i] : (($true = ((sK1 @ (sK7 @ X1)))) | ($true = ((sK2 @ sK6))) | ($false = ((sK1 @ X1)))) )),
% 2.52/0.63 inference(imp_proxy_clausification,[],[f166])).
% 2.52/0.63 thf(f169,plain,(
% 2.52/0.63 ( ! [X1 : $i] : (($true = ((sK0 @ X1 @ (sK7 @ X1)))) | ($true = ((sK2 @ sK6))) | ($false = ((sK1 @ X1)))) )),
% 2.52/0.63 inference(not_proxy_clausification,[],[f167])).
% 2.52/0.63 thf(f170,plain,(
% 2.52/0.63 ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ((sK1 @ Y0) & (!! @ $i @ (^[Y1 : $i]: ((sK1 @ Y1) => (~ (sK0 @ Y0 @ Y1))))))) @ X1))) | ($true = (((^[Y0 : $i]: ((sK2 @ Y0) => (?? @ $i @ (^[Y1 : $i]: ((sK2 @ Y1) & (sK0 @ Y0 @ Y1)))))) @ X2)))) )),
% 2.52/0.63 inference(pi_proxy_clausification,[],[f160])).
% 2.52/0.63 thf(f171,plain,(
% 2.52/0.63 ( ! [X2 : $i,X1 : $i] : (($false = (((sK1 @ X1) & (!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) => (~ (sK0 @ X1 @ Y0)))))))) | ($true = (((sK2 @ X2) => (?? @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) & (sK0 @ X2 @ Y0)))))))) )),
% 2.52/0.63 inference(beta-eta_normalization,[],[f170])).
% 2.52/0.63 thf(f172,plain,(
% 2.52/0.63 ( ! [X2 : $i,X1 : $i] : (($false = ((!! @ $i @ (^[Y0 : $i]: ((sK1 @ Y0) => (~ (sK0 @ X1 @ Y0))))))) | ($true = (((sK2 @ X2) => (?? @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) & (sK0 @ X2 @ Y0))))))) | ($false = ((sK1 @ X1)))) )),
% 2.52/0.63 inference(and_proxy_clausification,[],[f171])).
% 2.52/0.63 thf(f173,plain,(
% 2.52/0.63 ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ((sK1 @ Y0) => (~ (sK0 @ X1 @ Y0)))) @ (sK8 @ X1)))) | ($true = (((sK2 @ X2) => (?? @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) & (sK0 @ X2 @ Y0))))))) | ($false = ((sK1 @ X1)))) )),
% 2.52/0.63 inference(sigma_proxy_clausification,[],[f172])).
% 2.52/0.63 thf(f174,plain,(
% 2.52/0.63 ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ((sK1 @ Y0) => (~ (sK0 @ X1 @ Y0)))) @ (sK8 @ X1)))) | ($false = ((sK2 @ X2))) | ($false = ((sK1 @ X1))) | ($true = ((?? @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) & (sK0 @ X2 @ Y0))))))) )),
% 2.52/0.63 inference(imp_proxy_clausification,[],[f173])).
% 2.52/0.63 thf(f175,plain,(
% 2.52/0.63 ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ((sK1 @ Y0) => (~ (sK0 @ X1 @ Y0)))) @ (sK8 @ X1)))) | ($false = ((sK2 @ X2))) | ($false = ((sK1 @ X1))) | ($true = (((^[Y0 : $i]: ((sK2 @ Y0) & (sK0 @ X2 @ Y0))) @ (sK9 @ X2))))) )),
% 2.52/0.63 inference(sigma_proxy_clausification,[],[f174])).
% 2.52/0.63 thf(f176,plain,(
% 2.52/0.63 ( ! [X2 : $i,X1 : $i] : (($false = (((sK1 @ (sK8 @ X1)) => (~ (sK0 @ X1 @ (sK8 @ X1)))))) | ($false = ((sK2 @ X2))) | ($false = ((sK1 @ X1))) | ($true = (((sK2 @ (sK9 @ X2)) & (sK0 @ X2 @ (sK9 @ X2)))))) )),
% 2.52/0.63 inference(beta-eta_normalization,[],[f175])).
% 2.52/0.63 thf(f177,plain,(
% 2.52/0.63 ( ! [X2 : $i,X1 : $i] : (($false = ((~ (sK0 @ X1 @ (sK8 @ X1))))) | ($false = ((sK2 @ X2))) | ($false = ((sK1 @ X1))) | ($true = (((sK2 @ (sK9 @ X2)) & (sK0 @ X2 @ (sK9 @ X2)))))) )),
% 2.52/0.63 inference(imp_proxy_clausification,[],[f176])).
% 2.52/0.63 thf(f178,plain,(
% 2.52/0.63 ( ! [X2 : $i,X1 : $i] : (($true = ((sK1 @ (sK8 @ X1)))) | ($false = ((sK2 @ X2))) | ($false = ((sK1 @ X1))) | ($true = (((sK2 @ (sK9 @ X2)) & (sK0 @ X2 @ (sK9 @ X2)))))) )),
% 2.52/0.63 inference(imp_proxy_clausification,[],[f176])).
% 2.52/0.63 thf(f179,plain,(
% 2.52/0.63 ( ! [X2 : $i,X1 : $i] : (($true = ((sK1 @ (sK8 @ X1)))) | ($false = ((sK2 @ X2))) | ($false = ((sK1 @ X1))) | ($true = ((sK0 @ X2 @ (sK9 @ X2))))) )),
% 2.52/0.63 inference(and_proxy_clausification,[],[f178])).
% 2.52/0.63 thf(f180,plain,(
% 2.52/0.63 ( ! [X2 : $i,X1 : $i] : (($true = ((sK1 @ (sK8 @ X1)))) | ($false = ((sK2 @ X2))) | ($false = ((sK1 @ X1))) | ($true = ((sK2 @ (sK9 @ X2))))) )),
% 2.52/0.63 inference(and_proxy_clausification,[],[f178])).
% 2.52/0.63 thf(f181,plain,(
% 2.52/0.63 ( ! [X2 : $i,X1 : $i] : (($true = ((sK0 @ X1 @ (sK8 @ X1)))) | ($false = ((sK2 @ X2))) | ($false = ((sK1 @ X1))) | ($true = (((sK2 @ (sK9 @ X2)) & (sK0 @ X2 @ (sK9 @ X2)))))) )),
% 2.52/0.63 inference(not_proxy_clausification,[],[f177])).
% 2.52/0.63 thf(f182,plain,(
% 2.52/0.63 ( ! [X2 : $i,X1 : $i] : (($true = ((sK0 @ X1 @ (sK8 @ X1)))) | ($false = ((sK2 @ X2))) | ($false = ((sK1 @ X1))) | ($true = ((sK0 @ X2 @ (sK9 @ X2))))) )),
% 2.52/0.63 inference(and_proxy_clausification,[],[f181])).
% 2.52/0.63 thf(f183,plain,(
% 2.52/0.63 ( ! [X2 : $i,X1 : $i] : (($true = ((sK0 @ X1 @ (sK8 @ X1)))) | ($false = ((sK2 @ X2))) | ($false = ((sK1 @ X1))) | ($true = ((sK2 @ (sK9 @ X2))))) )),
% 2.52/0.63 inference(and_proxy_clausification,[],[f181])).
% 2.52/0.63 thf(f184,plain,(
% 2.52/0.63 ($true = ((!! @ ($i > $o) @ (^[Y0 : $i > $o]: ((?? @ $i @ Y0) => (?? @ $i @ (^[Y1 : $i]: ((Y0 @ Y1) & (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) => (~ (sK0 @ Y1 @ Y2))))))))))))) | ($true = ((~ (?? @ ($i > $o) @ (^[Y0 : $i > $o]: ((?? @ $i @ Y0) & (!! @ $i @ (^[Y1 : $i]: ((Y0 @ Y1) => (?? @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) & (sK0 @ Y1 @ Y2)))))))))))))),
% 2.52/0.63 inference(beta-eta_normalization,[],[f139])).
% 2.52/0.63 thf(f185,plain,(
% 2.52/0.63 ( ! [X1 : ($i > $o)] : (($true = (((^[Y0 : $i > $o]: ((?? @ $i @ Y0) => (?? @ $i @ (^[Y1 : $i]: ((Y0 @ Y1) & (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) => (~ (sK0 @ Y1 @ Y2)))))))))) @ X1))) | ($true = ((~ (?? @ ($i > $o) @ (^[Y0 : $i > $o]: ((?? @ $i @ Y0) & (!! @ $i @ (^[Y1 : $i]: ((Y0 @ Y1) => (?? @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) & (sK0 @ Y1 @ Y2)))))))))))))) )),
% 2.52/0.63 inference(pi_proxy_clausification,[],[f184])).
% 2.52/0.63 thf(f186,plain,(
% 2.52/0.63 ( ! [X1 : ($i > $o)] : (($true = (((^[Y0 : $i > $o]: ((?? @ $i @ Y0) => (?? @ $i @ (^[Y1 : $i]: ((Y0 @ Y1) & (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) => (~ (sK0 @ Y1 @ Y2)))))))))) @ X1))) | ($false = ((?? @ ($i > $o) @ (^[Y0 : $i > $o]: ((?? @ $i @ Y0) & (!! @ $i @ (^[Y1 : $i]: ((Y0 @ Y1) => (?? @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) & (sK0 @ Y1 @ Y2))))))))))))) )),
% 2.52/0.63 inference(not_proxy_clausification,[],[f185])).
% 2.52/0.63 thf(f187,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X1 : ($i > $o)] : (($true = (((^[Y0 : $i > $o]: ((?? @ $i @ Y0) => (?? @ $i @ (^[Y1 : $i]: ((Y0 @ Y1) & (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) => (~ (sK0 @ Y1 @ Y2)))))))))) @ X1))) | ($false = (((^[Y0 : $i > $o]: ((?? @ $i @ Y0) & (!! @ $i @ (^[Y1 : $i]: ((Y0 @ Y1) => (?? @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) & (sK0 @ Y1 @ Y2))))))))) @ X2)))) )),
% 2.52/0.63 inference(pi_proxy_clausification,[],[f186])).
% 2.52/0.63 thf(f188,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X1 : ($i > $o)] : (($true = (((?? @ $i @ X1) => (?? @ $i @ (^[Y0 : $i]: ((X1 @ Y0) & (!! @ $i @ (^[Y1 : $i]: ((X1 @ Y1) => (~ (sK0 @ Y0 @ Y1))))))))))) | ($false = (((?? @ $i @ X2) & (!! @ $i @ (^[Y0 : $i]: ((X2 @ Y0) => (?? @ $i @ (^[Y1 : $i]: ((X2 @ Y1) & (sK0 @ Y0 @ Y1))))))))))) )),
% 2.52/0.63 inference(beta-eta_normalization,[],[f187])).
% 2.52/0.63 thf(f189,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X1 : ($i > $o)] : (($false = ((?? @ $i @ X1))) | ($false = (((?? @ $i @ X2) & (!! @ $i @ (^[Y0 : $i]: ((X2 @ Y0) => (?? @ $i @ (^[Y1 : $i]: ((X2 @ Y1) & (sK0 @ Y0 @ Y1)))))))))) | ($true = ((?? @ $i @ (^[Y0 : $i]: ((X1 @ Y0) & (!! @ $i @ (^[Y1 : $i]: ((X1 @ Y1) => (~ (sK0 @ Y0 @ Y1))))))))))) )),
% 2.52/0.63 inference(imp_proxy_clausification,[],[f188])).
% 2.52/0.63 thf(f190,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X3 : $i,X1 : ($i > $o)] : ((((X1 @ X3)) = $false) | ($false = (((?? @ $i @ X2) & (!! @ $i @ (^[Y0 : $i]: ((X2 @ Y0) => (?? @ $i @ (^[Y1 : $i]: ((X2 @ Y1) & (sK0 @ Y0 @ Y1)))))))))) | ($true = ((?? @ $i @ (^[Y0 : $i]: ((X1 @ Y0) & (!! @ $i @ (^[Y1 : $i]: ((X1 @ Y1) => (~ (sK0 @ Y0 @ Y1))))))))))) )),
% 2.52/0.63 inference(pi_proxy_clausification,[],[f189])).
% 2.52/0.63 thf(f191,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X3 : $i,X1 : ($i > $o)] : ((((X1 @ X3)) = $false) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((X2 @ Y0) => (?? @ $i @ (^[Y1 : $i]: ((X2 @ Y1) & (sK0 @ Y0 @ Y1))))))))) | ($true = ((?? @ $i @ (^[Y0 : $i]: ((X1 @ Y0) & (!! @ $i @ (^[Y1 : $i]: ((X1 @ Y1) => (~ (sK0 @ Y0 @ Y1)))))))))) | ($false = ((?? @ $i @ X2)))) )),
% 2.52/0.63 inference(and_proxy_clausification,[],[f190])).
% 2.52/0.63 thf(f192,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X3 : $i,X1 : ($i > $o)] : ((((X1 @ X3)) = $false) | ($false = (((^[Y0 : $i]: ((X2 @ Y0) => (?? @ $i @ (^[Y1 : $i]: ((X2 @ Y1) & (sK0 @ Y0 @ Y1)))))) @ (sK10 @ X2)))) | ($true = ((?? @ $i @ (^[Y0 : $i]: ((X1 @ Y0) & (!! @ $i @ (^[Y1 : $i]: ((X1 @ Y1) => (~ (sK0 @ Y0 @ Y1)))))))))) | ($false = ((?? @ $i @ X2)))) )),
% 2.52/0.63 inference(sigma_proxy_clausification,[],[f191])).
% 2.52/0.63 thf(f193,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X3 : $i,X1 : ($i > $o)] : ((((X1 @ X3)) = $false) | ($false = (((^[Y0 : $i]: ((X2 @ Y0) => (?? @ $i @ (^[Y1 : $i]: ((X2 @ Y1) & (sK0 @ Y0 @ Y1)))))) @ (sK10 @ X2)))) | ($true = (((^[Y0 : $i]: ((X1 @ Y0) & (!! @ $i @ (^[Y1 : $i]: ((X1 @ Y1) => (~ (sK0 @ Y0 @ Y1))))))) @ (sK11 @ X1)))) | ($false = ((?? @ $i @ X2)))) )),
% 2.52/0.63 inference(sigma_proxy_clausification,[],[f192])).
% 2.52/0.63 thf(f194,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X3 : $i,X1 : ($i > $o),X4 : $i] : ((((X1 @ X3)) = $false) | ($false = (((^[Y0 : $i]: ((X2 @ Y0) => (?? @ $i @ (^[Y1 : $i]: ((X2 @ Y1) & (sK0 @ Y0 @ Y1)))))) @ (sK10 @ X2)))) | ($true = (((^[Y0 : $i]: ((X1 @ Y0) & (!! @ $i @ (^[Y1 : $i]: ((X1 @ Y1) => (~ (sK0 @ Y0 @ Y1))))))) @ (sK11 @ X1)))) | ($false = ((X2 @ X4)))) )),
% 2.52/0.63 inference(pi_proxy_clausification,[],[f193])).
% 2.52/0.63 thf(f195,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X3 : $i,X1 : ($i > $o),X4 : $i] : ((((X1 @ X3)) = $false) | ($false = (((X2 @ (sK10 @ X2)) => (?? @ $i @ (^[Y0 : $i]: ((X2 @ Y0) & (sK0 @ (sK10 @ X2) @ Y0))))))) | ($true = (((X1 @ (sK11 @ X1)) & (!! @ $i @ (^[Y0 : $i]: ((X1 @ Y0) => (~ (sK0 @ (sK11 @ X1) @ Y0)))))))) | ($false = ((X2 @ X4)))) )),
% 2.52/0.63 inference(beta-eta_normalization,[],[f194])).
% 2.52/0.63 thf(f196,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X3 : $i,X1 : ($i > $o),X4 : $i] : ((((X1 @ X3)) = $false) | ($false = ((?? @ $i @ (^[Y0 : $i]: ((X2 @ Y0) & (sK0 @ (sK10 @ X2) @ Y0)))))) | ($true = (((X1 @ (sK11 @ X1)) & (!! @ $i @ (^[Y0 : $i]: ((X1 @ Y0) => (~ (sK0 @ (sK11 @ X1) @ Y0)))))))) | ($false = ((X2 @ X4)))) )),
% 2.52/0.63 inference(imp_proxy_clausification,[],[f195])).
% 2.52/0.63 thf(f197,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X3 : $i,X1 : ($i > $o),X4 : $i] : ((((X1 @ X3)) = $false) | ($true = ((X2 @ (sK10 @ X2)))) | ($true = (((X1 @ (sK11 @ X1)) & (!! @ $i @ (^[Y0 : $i]: ((X1 @ Y0) => (~ (sK0 @ (sK11 @ X1) @ Y0)))))))) | ($false = ((X2 @ X4)))) )),
% 2.52/0.63 inference(imp_proxy_clausification,[],[f195])).
% 2.52/0.63 thf(f198,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X3 : $i,X1 : ($i > $o),X4 : $i] : ((((X1 @ X3)) = $false) | ($true = ((X2 @ (sK10 @ X2)))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((X1 @ Y0) => (~ (sK0 @ (sK11 @ X1) @ Y0))))))) | ($false = ((X2 @ X4)))) )),
% 2.52/0.63 inference(and_proxy_clausification,[],[f197])).
% 2.52/0.63 thf(f199,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X3 : $i,X1 : ($i > $o),X4 : $i] : ((((X1 @ X3)) = $false) | ($true = ((X2 @ (sK10 @ X2)))) | ($true = ((X1 @ (sK11 @ X1)))) | ($false = ((X2 @ X4)))) )),
% 2.52/0.63 inference(and_proxy_clausification,[],[f197])).
% 2.52/0.63 thf(f200,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X3 : $i,X1 : ($i > $o),X4 : $i,X5 : $i] : ((((X1 @ X3)) = $false) | ($true = ((X2 @ (sK10 @ X2)))) | ($true = (((^[Y0 : $i]: ((X1 @ Y0) => (~ (sK0 @ (sK11 @ X1) @ Y0)))) @ X5))) | ($false = ((X2 @ X4)))) )),
% 2.52/0.63 inference(pi_proxy_clausification,[],[f198])).
% 2.52/0.63 thf(f201,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X3 : $i,X1 : ($i > $o),X4 : $i,X5 : $i] : ((((X1 @ X3)) = $false) | ($true = ((X2 @ (sK10 @ X2)))) | ($true = (((X1 @ X5) => (~ (sK0 @ (sK11 @ X1) @ X5))))) | ($false = ((X2 @ X4)))) )),
% 2.52/0.63 inference(beta-eta_normalization,[],[f200])).
% 2.52/0.63 thf(f202,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X3 : $i,X1 : ($i > $o),X4 : $i,X5 : $i] : ((((X1 @ X3)) = $false) | ($true = ((X2 @ (sK10 @ X2)))) | ($false = ((X1 @ X5))) | ($false = ((X2 @ X4))) | ($true = ((~ (sK0 @ (sK11 @ X1) @ X5))))) )),
% 2.52/0.63 inference(imp_proxy_clausification,[],[f201])).
% 2.52/0.63 thf(f203,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X3 : $i,X1 : ($i > $o),X4 : $i,X5 : $i] : ((((X1 @ X3)) = $false) | ($true = ((X2 @ (sK10 @ X2)))) | ($false = ((X1 @ X5))) | ($false = ((X2 @ X4))) | ($false = ((sK0 @ (sK11 @ X1) @ X5)))) )),
% 2.52/0.63 inference(not_proxy_clausification,[],[f202])).
% 2.52/0.63 thf(f204,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X3 : $i,X1 : ($i > $o),X4 : $i,X5 : $i] : ((((X1 @ X3)) = $false) | ($false = (((^[Y0 : $i]: ((X2 @ Y0) & (sK0 @ (sK10 @ X2) @ Y0))) @ X5))) | ($true = (((X1 @ (sK11 @ X1)) & (!! @ $i @ (^[Y0 : $i]: ((X1 @ Y0) => (~ (sK0 @ (sK11 @ X1) @ Y0)))))))) | ($false = ((X2 @ X4)))) )),
% 2.52/0.63 inference(pi_proxy_clausification,[],[f196])).
% 2.52/0.63 thf(f205,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X3 : $i,X1 : ($i > $o),X4 : $i,X5 : $i] : ((((X1 @ X3)) = $false) | ($false = (((^[Y0 : $i]: ((X2 @ Y0) & (sK0 @ (sK10 @ X2) @ Y0))) @ X5))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((X1 @ Y0) => (~ (sK0 @ (sK11 @ X1) @ Y0))))))) | ($false = ((X2 @ X4)))) )),
% 2.52/0.63 inference(and_proxy_clausification,[],[f204])).
% 2.52/0.63 thf(f206,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X3 : $i,X1 : ($i > $o),X4 : $i,X5 : $i] : ((((X1 @ X3)) = $false) | ($false = (((^[Y0 : $i]: ((X2 @ Y0) & (sK0 @ (sK10 @ X2) @ Y0))) @ X5))) | ($true = ((X1 @ (sK11 @ X1)))) | ($false = ((X2 @ X4)))) )),
% 2.52/0.63 inference(and_proxy_clausification,[],[f204])).
% 2.52/0.63 thf(f207,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X3 : $i,X1 : ($i > $o),X4 : $i,X5 : $i] : ((((X1 @ X3)) = $false) | ($false = (((X2 @ X5) & (sK0 @ (sK10 @ X2) @ X5)))) | ($true = ((X1 @ (sK11 @ X1)))) | ($false = ((X2 @ X4)))) )),
% 2.52/0.63 inference(beta-eta_normalization,[],[f206])).
% 2.52/0.63 thf(f208,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X3 : $i,X1 : ($i > $o),X4 : $i,X5 : $i] : ((((X1 @ X3)) = $false) | ($false = ((sK0 @ (sK10 @ X2) @ X5))) | ($true = ((X1 @ (sK11 @ X1)))) | ($false = ((X2 @ X4))) | ($false = ((X2 @ X5)))) )),
% 2.52/0.63 inference(and_proxy_clausification,[],[f207])).
% 2.52/0.63 thf(f209,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X3 : $i,X1 : ($i > $o),X6 : $i,X4 : $i,X5 : $i] : ((((X1 @ X3)) = $false) | ($false = (((^[Y0 : $i]: ((X2 @ Y0) & (sK0 @ (sK10 @ X2) @ Y0))) @ X5))) | ($true = (((^[Y0 : $i]: ((X1 @ Y0) => (~ (sK0 @ (sK11 @ X1) @ Y0)))) @ X6))) | ($false = ((X2 @ X4)))) )),
% 2.52/0.63 inference(pi_proxy_clausification,[],[f205])).
% 2.52/0.63 thf(f210,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X3 : $i,X1 : ($i > $o),X6 : $i,X4 : $i,X5 : $i] : ((((X1 @ X3)) = $false) | ($false = (((X2 @ X5) & (sK0 @ (sK10 @ X2) @ X5)))) | ($true = (((X1 @ X6) => (~ (sK0 @ (sK11 @ X1) @ X6))))) | ($false = ((X2 @ X4)))) )),
% 2.52/0.63 inference(beta-eta_normalization,[],[f209])).
% 2.52/0.63 thf(f211,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X3 : $i,X1 : ($i > $o),X6 : $i,X4 : $i,X5 : $i] : ((((X1 @ X3)) = $false) | ($false = ((sK0 @ (sK10 @ X2) @ X5))) | ($true = (((X1 @ X6) => (~ (sK0 @ (sK11 @ X1) @ X6))))) | ($false = ((X2 @ X4))) | ($false = ((X2 @ X5)))) )),
% 2.52/0.63 inference(and_proxy_clausification,[],[f210])).
% 2.52/0.63 thf(f212,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X3 : $i,X1 : ($i > $o),X6 : $i,X4 : $i,X5 : $i] : ((((X1 @ X3)) = $false) | ($false = ((sK0 @ (sK10 @ X2) @ X5))) | ($false = ((X1 @ X6))) | ($false = ((X2 @ X4))) | ($false = ((X2 @ X5))) | ($true = ((~ (sK0 @ (sK11 @ X1) @ X6))))) )),
% 2.52/0.63 inference(imp_proxy_clausification,[],[f211])).
% 2.52/0.63 thf(f213,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X3 : $i,X1 : ($i > $o),X6 : $i,X4 : $i,X5 : $i] : ((((X1 @ X3)) = $false) | ($false = ((sK0 @ (sK10 @ X2) @ X5))) | ($false = ((X1 @ X6))) | ($false = ((X2 @ X4))) | ($false = ((X2 @ X5))) | ($false = ((sK0 @ (sK11 @ X1) @ X6)))) )),
% 2.52/0.63 inference(not_proxy_clausification,[],[f212])).
% 2.52/0.63 thf(f215,definition,(
% 2.52/0.63 spl12_1 <=> ($true = ((sK2 @ sK4)))),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_1])],[avatar_definition])).
% 2.52/0.63 thf(f217,plain,(
% 2.52/0.63 ($true = ((sK2 @ sK4))) | ~spl12_1),
% 2.52/0.63 inference(avatar_component_clause,[],[f215])).
% 2.52/0.63 thf(f219,definition,(
% 2.52/0.63 spl12_2 <=> ($true = ((sK1 @ sK3)))),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_2])],[avatar_definition])).
% 2.52/0.63 thf(f221,plain,(
% 2.52/0.63 ($true = ((sK1 @ sK3))) | ~spl12_2),
% 2.52/0.63 inference(avatar_component_clause,[],[f219])).
% 2.52/0.63 thf(f222,plain,(
% 2.52/0.63 spl12_1 | spl12_2),
% 2.52/0.63 inference(avatar_split_clause,[],[f151,f219,f215])).
% 2.52/0.63 thf(f224,definition,(
% 2.52/0.63 spl12_3 <=> ! [X1 : $i] : (($false = ((sK2 @ X1))) | ($true = ((sK2 @ (sK5 @ X1)))))),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_3])],[avatar_definition])).
% 2.52/0.63 thf(f225,plain,(
% 2.52/0.63 ( ! [X1 : $i] : (($true = ((sK2 @ (sK5 @ X1)))) | ($false = ((sK2 @ X1)))) ) | ~spl12_3),
% 2.52/0.63 inference(avatar_component_clause,[],[f224])).
% 2.52/0.63 thf(f226,plain,(
% 2.52/0.63 spl12_3 | spl12_2),
% 2.52/0.63 inference(avatar_split_clause,[],[f158,f219,f224])).
% 2.52/0.63 thf(f228,definition,(
% 2.52/0.63 spl12_4 <=> ! [X1 : $i] : (($false = ((sK2 @ X1))) | ($true = ((sK0 @ X1 @ (sK5 @ X1)))))),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_4])],[avatar_definition])).
% 2.52/0.63 thf(f229,plain,(
% 2.52/0.63 ( ! [X1 : $i] : (($true = ((sK0 @ X1 @ (sK5 @ X1)))) | ($false = ((sK2 @ X1)))) ) | ~spl12_4),
% 2.52/0.63 inference(avatar_component_clause,[],[f228])).
% 2.52/0.63 thf(f230,plain,(
% 2.52/0.63 spl12_4 | spl12_2),
% 2.52/0.63 inference(avatar_split_clause,[],[f157,f219,f228])).
% 2.52/0.63 thf(f232,definition,(
% 2.52/0.63 spl12_5 <=> ($true = ((sK2 @ sK6)))),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_5])],[avatar_definition])).
% 2.52/0.63 thf(f234,plain,(
% 2.52/0.63 ($true = ((sK2 @ sK6))) | ~spl12_5),
% 2.52/0.63 inference(avatar_component_clause,[],[f232])).
% 2.52/0.63 thf(f236,definition,(
% 2.52/0.63 spl12_6 <=> ! [X1 : $i] : (($true = ((sK1 @ (sK7 @ X1)))) | ($false = ((sK1 @ X1))))),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_6])],[avatar_definition])).
% 2.52/0.63 thf(f237,plain,(
% 2.52/0.63 ( ! [X1 : $i] : (($true = ((sK1 @ (sK7 @ X1)))) | ($false = ((sK1 @ X1)))) ) | ~spl12_6),
% 2.52/0.63 inference(avatar_component_clause,[],[f236])).
% 2.52/0.63 thf(f238,plain,(
% 2.52/0.63 spl12_5 | spl12_6),
% 2.52/0.63 inference(avatar_split_clause,[],[f168,f236,f232])).
% 2.52/0.63 thf(f240,definition,(
% 2.52/0.63 spl12_7 <=> ! [X1 : $i] : (($true = ((sK0 @ X1 @ (sK7 @ X1)))) | ($false = ((sK1 @ X1))))),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_7])],[avatar_definition])).
% 2.52/0.63 thf(f241,plain,(
% 2.52/0.63 ( ! [X1 : $i] : (($true = ((sK0 @ X1 @ (sK7 @ X1)))) | ($false = ((sK1 @ X1)))) ) | ~spl12_7),
% 2.52/0.63 inference(avatar_component_clause,[],[f240])).
% 2.52/0.63 thf(f242,plain,(
% 2.52/0.63 spl12_5 | spl12_7),
% 2.52/0.63 inference(avatar_split_clause,[],[f169,f240,f232])).
% 2.52/0.63 thf(f244,definition,(
% 2.52/0.63 spl12_8 <=> ! [X2 : $i] : (($false = ((sK2 @ X2))) | ($true = ((sK2 @ (sK9 @ X2)))))),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_8])],[avatar_definition])).
% 2.52/0.63 thf(f245,plain,(
% 2.52/0.63 ( ! [X2 : $i] : (($true = ((sK2 @ (sK9 @ X2)))) | ($false = ((sK2 @ X2)))) ) | ~spl12_8),
% 2.52/0.63 inference(avatar_component_clause,[],[f244])).
% 2.52/0.63 thf(f247,definition,(
% 2.52/0.63 spl12_9 <=> ! [X1 : $i] : (($true = ((sK1 @ (sK8 @ X1)))) | ($false = ((sK1 @ X1))))),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_9])],[avatar_definition])).
% 2.52/0.63 thf(f248,plain,(
% 2.52/0.63 ( ! [X1 : $i] : (($true = ((sK1 @ (sK8 @ X1)))) | ($false = ((sK1 @ X1)))) ) | ~spl12_9),
% 2.52/0.63 inference(avatar_component_clause,[],[f247])).
% 2.52/0.63 thf(f249,plain,(
% 2.52/0.63 spl12_8 | spl12_9),
% 2.52/0.63 inference(avatar_split_clause,[],[f180,f247,f244])).
% 2.52/0.63 thf(f251,definition,(
% 2.52/0.63 spl12_10 <=> ! [X2 : $i] : (($false = ((sK2 @ X2))) | ($true = ((sK0 @ X2 @ (sK9 @ X2)))))),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_10])],[avatar_definition])).
% 2.52/0.63 thf(f252,plain,(
% 2.52/0.63 ( ! [X2 : $i] : (($true = ((sK0 @ X2 @ (sK9 @ X2)))) | ($false = ((sK2 @ X2)))) ) | ~spl12_10),
% 2.52/0.63 inference(avatar_component_clause,[],[f251])).
% 2.52/0.63 thf(f253,plain,(
% 2.52/0.63 spl12_10 | spl12_9),
% 2.52/0.63 inference(avatar_split_clause,[],[f179,f247,f251])).
% 2.52/0.63 thf(f255,definition,(
% 2.52/0.63 spl12_11 <=> ! [X1 : $i] : (($true = ((sK0 @ X1 @ (sK8 @ X1)))) | ($false = ((sK1 @ X1))))),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_11])],[avatar_definition])).
% 2.52/0.63 thf(f256,plain,(
% 2.52/0.63 ( ! [X1 : $i] : (($true = ((sK0 @ X1 @ (sK8 @ X1)))) | ($false = ((sK1 @ X1)))) ) | ~spl12_11),
% 2.52/0.63 inference(avatar_component_clause,[],[f255])).
% 2.52/0.63 thf(f257,plain,(
% 2.52/0.63 spl12_8 | spl12_11),
% 2.52/0.63 inference(avatar_split_clause,[],[f183,f255,f244])).
% 2.52/0.63 thf(f258,plain,(
% 2.52/0.63 spl12_10 | spl12_11),
% 2.52/0.63 inference(avatar_split_clause,[],[f182,f255,f251])).
% 2.52/0.63 thf(f260,definition,(
% 2.52/0.63 spl12_12 <=> ! [X2 : ($i > $o),X4 : $i] : (($true = ((X2 @ (sK10 @ X2)))) | ($false = ((X2 @ X4))))),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_12])],[avatar_definition])).
% 2.52/0.63 thf(f261,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X4 : $i] : (($true = ((X2 @ (sK10 @ X2)))) | ($false = ((X2 @ X4)))) ) | ~spl12_12),
% 2.52/0.63 inference(avatar_component_clause,[],[f260])).
% 2.52/0.63 thf(f263,definition,(
% 2.52/0.63 spl12_13 <=> ! [X1 : ($i > $o),X3 : $i] : ((((X1 @ X3)) = $false) | ($true = ((X1 @ (sK11 @ X1)))))),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_13])],[avatar_definition])).
% 2.52/0.63 thf(f264,plain,(
% 2.52/0.63 ( ! [X3 : $i,X1 : ($i > $o)] : ((((X1 @ X3)) = $false) | ($true = ((X1 @ (sK11 @ X1))))) ) | ~spl12_13),
% 2.52/0.63 inference(avatar_component_clause,[],[f263])).
% 2.52/0.63 thf(f265,plain,(
% 2.52/0.63 spl12_12 | spl12_13),
% 2.52/0.63 inference(avatar_split_clause,[],[f199,f263,f260])).
% 2.52/0.63 thf(f267,definition,(
% 2.52/0.63 spl12_14 <=> ! [X5 : $i,X1 : ($i > $o),X3 : $i] : ((((X1 @ X3)) = $false) | ($false = ((sK0 @ (sK11 @ X1) @ X5))) | ($false = ((X1 @ X5))))),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_14])],[avatar_definition])).
% 2.52/0.63 thf(f268,plain,(
% 2.52/0.63 ( ! [X3 : $i,X1 : ($i > $o),X5 : $i] : (($false = ((sK0 @ (sK11 @ X1) @ X5))) | (((X1 @ X3)) = $false) | ($false = ((X1 @ X5)))) ) | ~spl12_14),
% 2.52/0.63 inference(avatar_component_clause,[],[f267])).
% 2.52/0.63 thf(f269,plain,(
% 2.52/0.63 spl12_12 | spl12_14),
% 2.52/0.63 inference(avatar_split_clause,[],[f203,f267,f260])).
% 2.52/0.63 thf(f271,definition,(
% 2.52/0.63 spl12_15 <=> ! [X2 : ($i > $o),X5 : $i,X4 : $i] : (($false = ((sK0 @ (sK10 @ X2) @ X5))) | ($false = ((X2 @ X5))) | ($false = ((X2 @ X4))))),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_15])],[avatar_definition])).
% 2.52/0.63 thf(f272,plain,(
% 2.52/0.63 ( ! [X2 : ($i > $o),X4 : $i,X5 : $i] : (($false = ((sK0 @ (sK10 @ X2) @ X5))) | ($false = ((X2 @ X4))) | ($false = ((X2 @ X5)))) ) | ~spl12_15),
% 2.52/0.63 inference(avatar_component_clause,[],[f271])).
% 2.52/0.63 thf(f273,plain,(
% 2.52/0.63 spl12_15 | spl12_13),
% 2.52/0.63 inference(avatar_split_clause,[],[f208,f263,f271])).
% 2.52/0.63 thf(f274,plain,(
% 2.52/0.63 spl12_15 | spl12_14),
% 2.52/0.63 inference(avatar_split_clause,[],[f213,f267,f271])).
% 2.52/0.63 thf(f293,plain,(
% 2.52/0.63 ( ! [X0 : $i] : (($true = $false) | ($true = (((^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ (sK10 @ (^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))))))) | (sK6 != X0)) ) | (~spl12_5 | ~spl12_12)),
% 2.52/0.63 inference(constrained_superposition,[],[f261,f234])).
% 2.52/0.63 thf(f308,plain,(
% 2.52/0.63 ( ! [X0 : ($i > $o),X1 : $i] : (($true != ((X0 @ X1))) | ($false = ((X0 @ X1))) | ($false != ((X0 @ (sK10 @ X0))))) ) | ~spl12_12),
% 2.52/0.63 inference(equality_factoring,[],[f261])).
% 2.52/0.63 thf(f310,plain,(
% 2.52/0.63 ( ! [X0 : ($i > $o),X1 : $i] : (($false != ((X0 @ (sK10 @ X0)))) | ($true = ((X0 @ (sK10 @ X0)))) | ($true != ((X0 @ X1)))) ) | ~spl12_12),
% 2.52/0.63 inference(equality_factoring,[],[f261])).
% 2.52/0.63 thf(f347,plain,(
% 2.52/0.63 ( ! [X0 : $i] : (($true = (((^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ (sK10 @ (^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))))))) | (sK6 != X0)) ) | (~spl12_5 | ~spl12_12)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f293])).
% 2.52/0.63 thf(f348,plain,(
% 2.52/0.63 ( ! [X0 : $i] : (($true = ((sK2 @ (sK10 @ sK2)))) | (sK6 != X0)) ) | (~spl12_5 | ~spl12_12)),
% 2.52/0.63 inference(beta-eta_normalization,[],[f347])).
% 2.52/0.63 thf(f369,plain,(
% 2.52/0.63 ( ! [X0 : ($i > $o),X1 : $i] : (($true != ((X0 @ X1))) | ($true = ((X0 @ (sK10 @ X0))))) ) | ~spl12_12),
% 2.52/0.63 inference(forward_subsumption_resolution,[],[f310,f261])).
% 2.52/0.63 thf(f370,plain,(
% 2.52/0.63 ( ! [X0 : ($i > $o),X1 : $i] : (($false != ((X0 @ (sK10 @ X0)))) | ($false = ((X0 @ X1)))) ) | ~spl12_12),
% 2.52/0.63 inference(forward_subsumption_resolution,[],[f308,f120])).
% 2.52/0.63 thf(f372,definition,(
% 2.52/0.63 spl12_16 <=> ! [X0 : $i] : (sK6 != X0)),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_16])],[avatar_definition])).
% 2.52/0.63 thf(f373,plain,(
% 2.52/0.63 ( ! [X0 : $i] : ((sK6 != X0)) ) | ~spl12_16),
% 2.52/0.63 inference(avatar_component_clause,[],[f372])).
% 2.52/0.63 thf(f375,definition,(
% 2.52/0.63 spl12_17 <=> ($true = ((sK2 @ (sK10 @ sK2))))),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_17])],[avatar_definition])).
% 2.52/0.63 thf(f376,plain,(
% 2.52/0.63 ($true != ((sK2 @ (sK10 @ sK2)))) | spl12_17),
% 2.52/0.63 inference(avatar_component_clause,[],[f375])).
% 2.52/0.63 thf(f377,plain,(
% 2.52/0.63 ($true = ((sK2 @ (sK10 @ sK2)))) | ~spl12_17),
% 2.52/0.63 inference(avatar_component_clause,[],[f375])).
% 2.52/0.63 thf(f380,definition,(
% 2.52/0.63 spl12_18 <=> ! [X0 : $i] : (sK3 != X0)),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_18])],[avatar_definition])).
% 2.52/0.63 thf(f381,plain,(
% 2.52/0.63 ( ! [X0 : $i] : ((sK3 != X0)) ) | ~spl12_18),
% 2.52/0.63 inference(avatar_component_clause,[],[f380])).
% 2.52/0.63 thf(f383,definition,(
% 2.52/0.63 spl12_19 <=> ($true = ((sK1 @ (sK10 @ sK1))))),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_19])],[avatar_definition])).
% 2.52/0.63 thf(f385,plain,(
% 2.52/0.63 ($true = ((sK1 @ (sK10 @ sK1)))) | ~spl12_19),
% 2.52/0.63 inference(avatar_component_clause,[],[f383])).
% 2.52/0.63 thf(f387,plain,(
% 2.52/0.63 spl12_16 | spl12_17 | ~spl12_5 | ~spl12_12),
% 2.52/0.63 inference(avatar_split_clause,[],[f348,f260,f232,f375,f372])).
% 2.52/0.63 thf(f389,plain,(
% 2.52/0.63 $false | ~spl12_16),
% 2.52/0.63 inference(equality_resolution,[],[f373])).
% 2.52/0.63 thf(f390,plain,(
% 2.52/0.63 ~spl12_16),
% 2.52/0.63 inference(avatar_contradiction_clause,[],[f389])).
% 2.52/0.63 thf(f422,plain,(
% 2.52/0.63 ( ! [X0 : $i] : (($true != $true) | ($true = (((^[Y0 : $i]: (sK1 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ (sK10 @ (^[Y0 : $i]: (sK1 @ ((^[Y1 : $i]: (Y1)) @ Y0))))))) | (sK3 != X0)) ) | (~spl12_2 | ~spl12_12)),
% 2.52/0.63 inference(constrained_superposition,[],[f369,f221])).
% 2.52/0.63 thf(f464,plain,(
% 2.52/0.63 ( ! [X0 : $i] : (($true = (((^[Y0 : $i]: (sK1 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ (sK10 @ (^[Y0 : $i]: (sK1 @ ((^[Y1 : $i]: (Y1)) @ Y0))))))) | (sK3 != X0)) ) | (~spl12_2 | ~spl12_12)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f422])).
% 2.52/0.63 thf(f465,plain,(
% 2.52/0.63 ( ! [X0 : $i] : (($true = ((sK1 @ (sK10 @ sK1)))) | (sK3 != X0)) ) | (~spl12_2 | ~spl12_12)),
% 2.52/0.63 inference(beta-eta_normalization,[],[f464])).
% 2.52/0.63 thf(f799,plain,(
% 2.52/0.63 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((sK0 @ (sK10 @ (^[Y0 : $i]: (sK1 @ ((^[Y1 : $i]: (Y1)) @ Y0)))) @ X1))) | ($false = (((^[Y0 : $i]: (sK1 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X1))) | (sK3 != X0)) ) | (~spl12_2 | ~spl12_15)),
% 2.52/0.63 inference(constrained_superposition,[],[f272,f221])).
% 2.52/0.63 thf(f803,plain,(
% 2.52/0.63 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((sK0 @ (sK10 @ (^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0)))) @ X1))) | ($false = (((^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X1))) | (sK6 != X0)) ) | (~spl12_5 | ~spl12_15)),
% 2.52/0.63 inference(constrained_superposition,[],[f272,f234])).
% 2.52/0.63 thf(f955,plain,(
% 2.52/0.63 ( ! [X0 : $i,X1 : $i] : (($false = ((sK0 @ (sK10 @ (^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0)))) @ X1))) | ($false = (((^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X1))) | (sK6 != X0)) ) | (~spl12_5 | ~spl12_15)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f803])).
% 2.52/0.63 thf(f956,plain,(
% 2.52/0.63 ( ! [X0 : $i,X1 : $i] : (($false = ((sK0 @ (sK10 @ sK2) @ X1))) | ($false = ((sK2 @ X1))) | (sK6 != X0)) ) | (~spl12_5 | ~spl12_15)),
% 2.52/0.63 inference(beta-eta_normalization,[],[f955])).
% 2.52/0.63 thf(f963,plain,(
% 2.52/0.63 ( ! [X0 : $i,X1 : $i] : (($false = ((sK0 @ (sK10 @ (^[Y0 : $i]: (sK1 @ ((^[Y1 : $i]: (Y1)) @ Y0)))) @ X1))) | ($false = (((^[Y0 : $i]: (sK1 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X1))) | (sK3 != X0)) ) | (~spl12_2 | ~spl12_15)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f799])).
% 2.52/0.63 thf(f964,plain,(
% 2.52/0.63 ( ! [X0 : $i,X1 : $i] : (($false = ((sK0 @ (sK10 @ sK1) @ X1))) | ($false = ((sK1 @ X1))) | (sK3 != X0)) ) | (~spl12_2 | ~spl12_15)),
% 2.52/0.63 inference(beta-eta_normalization,[],[f963])).
% 2.52/0.63 thf(f1008,definition,(
% 2.52/0.63 spl12_22 <=> ! [X0 : $i] : (((sK10 @ sK2)) != X0)),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_22])],[avatar_definition])).
% 2.52/0.63 thf(f1009,plain,(
% 2.52/0.63 ( ! [X0 : $i] : ((((sK10 @ sK2)) != X0)) ) | ~spl12_22),
% 2.52/0.63 inference(avatar_component_clause,[],[f1008])).
% 2.52/0.63 thf(f1011,definition,(
% 2.52/0.63 spl12_23 <=> ! [X1 : $i] : (($false = ((sK0 @ (sK10 @ sK2) @ X1))) | ($false = ((sK2 @ X1))))),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_23])],[avatar_definition])).
% 2.52/0.63 thf(f1012,plain,(
% 2.52/0.63 ( ! [X1 : $i] : (($false = ((sK0 @ (sK10 @ sK2) @ X1))) | ($false = ((sK2 @ X1)))) ) | ~spl12_23),
% 2.52/0.63 inference(avatar_component_clause,[],[f1011])).
% 2.52/0.63 thf(f1021,definition,(
% 2.52/0.63 spl12_25 <=> ! [X1 : $i] : (($false = ((sK0 @ (sK10 @ sK1) @ X1))) | ($false = ((sK1 @ X1))))),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_25])],[avatar_definition])).
% 2.52/0.63 thf(f1022,plain,(
% 2.52/0.63 ( ! [X1 : $i] : (($false = ((sK0 @ (sK10 @ sK1) @ X1))) | ($false = ((sK1 @ X1)))) ) | ~spl12_25),
% 2.52/0.63 inference(avatar_component_clause,[],[f1021])).
% 2.52/0.63 thf(f1031,plain,(
% 2.52/0.63 spl12_16 | spl12_23 | ~spl12_5 | ~spl12_15),
% 2.52/0.63 inference(avatar_split_clause,[],[f956,f271,f232,f1011,f372])).
% 2.52/0.63 thf(f1035,plain,(
% 2.52/0.63 spl12_18 | spl12_25 | ~spl12_2 | ~spl12_15),
% 2.52/0.63 inference(avatar_split_clause,[],[f964,f271,f219,f1021,f380])).
% 2.52/0.63 thf(f1334,plain,(
% 2.52/0.63 ($true = $false) | ($false = ((sK2 @ (sK10 @ sK2)))) | ($false = ((sK2 @ (sK9 @ (sK10 @ sK2))))) | (~spl12_10 | ~spl12_23)),
% 2.52/0.63 inference(constrained_superposition,[],[f252,f1012])).
% 2.52/0.63 thf(f1335,plain,(
% 2.52/0.63 ($false = ((sK2 @ (sK10 @ sK2)))) | ($false = ((sK2 @ (sK9 @ (sK10 @ sK2))))) | (~spl12_10 | ~spl12_23)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f1334])).
% 2.52/0.63 thf(f1359,plain,(
% 2.52/0.63 ($false = ((sK2 @ (sK9 @ (sK10 @ sK2))))) | (~spl12_10 | ~spl12_12 | ~spl12_23)),
% 2.52/0.63 inference(forward_subsumption_resolution,[],[f1335,f370])).
% 2.52/0.63 thf(f1375,plain,(
% 2.52/0.63 ($true = $false) | ($false = ((sK2 @ (sK10 @ sK2)))) | (~spl12_8 | ~spl12_10 | ~spl12_12 | ~spl12_23)),
% 2.52/0.63 inference(constrained_superposition,[],[f245,f1359])).
% 2.52/0.63 thf(f1376,plain,(
% 2.52/0.63 ($false = ((sK2 @ (sK10 @ sK2)))) | (~spl12_8 | ~spl12_10 | ~spl12_12 | ~spl12_23)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f1375])).
% 2.52/0.63 thf(f1404,plain,(
% 2.52/0.63 ($true = $false) | (~spl12_8 | ~spl12_10 | ~spl12_12 | ~spl12_17 | ~spl12_23)),
% 2.52/0.63 inference(constrained_superposition,[],[f1376,f377])).
% 2.52/0.63 thf(f1440,plain,(
% 2.52/0.63 $false | (~spl12_8 | ~spl12_10 | ~spl12_12 | ~spl12_17 | ~spl12_23)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f1404])).
% 2.52/0.63 thf(f1441,plain,(
% 2.52/0.63 ~spl12_8 | ~spl12_10 | ~spl12_12 | ~spl12_17 | ~spl12_23),
% 2.52/0.63 inference(avatar_contradiction_clause,[],[f1440])).
% 2.52/0.63 thf(f1515,plain,(
% 2.52/0.63 ( ! [X0 : ($i > $o),X1 : $i] : (($true != ((X0 @ X1))) | ($false = ((X0 @ X1))) | ($false != ((X0 @ (sK11 @ X0))))) ) | ~spl12_13),
% 2.52/0.63 inference(equality_factoring,[],[f264])).
% 2.52/0.63 thf(f1669,plain,(
% 2.52/0.63 ( ! [X0 : ($i > $o),X1 : $i] : (($false != ((X0 @ (sK11 @ X0)))) | ($false = ((X0 @ X1)))) ) | ~spl12_13),
% 2.52/0.63 inference(forward_subsumption_resolution,[],[f1515,f120])).
% 2.52/0.63 thf(f1676,definition,(
% 2.52/0.63 spl12_32 <=> ($true = ((sK2 @ (sK11 @ sK2))))),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_32])],[avatar_definition])).
% 2.52/0.63 thf(f1677,plain,(
% 2.52/0.63 ($true != ((sK2 @ (sK11 @ sK2)))) | spl12_32),
% 2.52/0.63 inference(avatar_component_clause,[],[f1676])).
% 2.52/0.63 thf(f1678,plain,(
% 2.52/0.63 ($true = ((sK2 @ (sK11 @ sK2)))) | ~spl12_32),
% 2.52/0.63 inference(avatar_component_clause,[],[f1676])).
% 2.52/0.63 thf(f1682,definition,(
% 2.52/0.63 spl12_33 <=> ($true = ((sK1 @ (sK11 @ sK1))))),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_33])],[avatar_definition])).
% 2.52/0.63 thf(f1684,plain,(
% 2.52/0.63 ($true = ((sK1 @ (sK11 @ sK1)))) | ~spl12_33),
% 2.52/0.63 inference(avatar_component_clause,[],[f1682])).
% 2.52/0.63 thf(f1918,definition,(
% 2.52/0.63 spl12_35 <=> ! [X1 : $i] : (($false = ((sK0 @ (sK11 @ sK2) @ X1))) | ($false = ((sK2 @ X1))))),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_35])],[avatar_definition])).
% 2.52/0.63 thf(f1919,plain,(
% 2.52/0.63 ( ! [X1 : $i] : (($false = ((sK0 @ (sK11 @ sK2) @ X1))) | ($false = ((sK2 @ X1)))) ) | ~spl12_35),
% 2.52/0.63 inference(avatar_component_clause,[],[f1918])).
% 2.52/0.63 thf(f1925,definition,(
% 2.52/0.63 spl12_36 <=> ! [X1 : $i] : (($false = ((sK0 @ (sK11 @ sK1) @ X1))) | ($false = ((sK1 @ X1))))),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_36])],[avatar_definition])).
% 2.52/0.63 thf(f1926,plain,(
% 2.52/0.63 ( ! [X1 : $i] : (($false = ((sK0 @ (sK11 @ sK1) @ X1))) | ($false = ((sK1 @ X1)))) ) | ~spl12_36),
% 2.52/0.63 inference(avatar_component_clause,[],[f1925])).
% 2.52/0.63 thf(f3723,definition,(
% 2.52/0.63 spl12_42 <=> ! [X0 : $i] : (((sK11 @ sK2)) != X0)),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_42])],[avatar_definition])).
% 2.52/0.63 thf(f3724,plain,(
% 2.52/0.63 ( ! [X0 : $i] : ((((sK11 @ sK2)) != X0)) ) | ~spl12_42),
% 2.52/0.63 inference(avatar_component_clause,[],[f3723])).
% 2.52/0.63 thf(f3812,plain,(
% 2.52/0.63 ($true = $false) | ($false = ((sK2 @ (sK11 @ sK2)))) | ($false = ((sK2 @ (sK9 @ (sK11 @ sK2))))) | (~spl12_10 | ~spl12_35)),
% 2.52/0.63 inference(constrained_superposition,[],[f252,f1919])).
% 2.52/0.63 thf(f3813,plain,(
% 2.52/0.63 ($false = ((sK2 @ (sK11 @ sK2)))) | ($false = ((sK2 @ (sK9 @ (sK11 @ sK2))))) | (~spl12_10 | ~spl12_35)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f3812])).
% 2.52/0.63 thf(f3833,plain,(
% 2.52/0.63 ($false = ((sK2 @ (sK9 @ (sK11 @ sK2))))) | (~spl12_10 | ~spl12_13 | ~spl12_35)),
% 2.52/0.63 inference(forward_subsumption_resolution,[],[f3813,f1669])).
% 2.52/0.63 thf(f3848,plain,(
% 2.52/0.63 ($true = $false) | ($false = ((sK2 @ (sK11 @ sK2)))) | (~spl12_8 | ~spl12_10 | ~spl12_13 | ~spl12_35)),
% 2.52/0.63 inference(constrained_superposition,[],[f245,f3833])).
% 2.52/0.63 thf(f3849,plain,(
% 2.52/0.63 ($false = ((sK2 @ (sK11 @ sK2)))) | (~spl12_8 | ~spl12_10 | ~spl12_13 | ~spl12_35)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f3848])).
% 2.52/0.63 thf(f3872,plain,(
% 2.52/0.63 ($true = $false) | (~spl12_8 | ~spl12_10 | ~spl12_13 | ~spl12_32 | ~spl12_35)),
% 2.52/0.63 inference(constrained_superposition,[],[f3849,f1678])).
% 2.52/0.63 thf(f3906,plain,(
% 2.52/0.63 $false | (~spl12_8 | ~spl12_10 | ~spl12_13 | ~spl12_32 | ~spl12_35)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f3872])).
% 2.52/0.63 thf(f3907,plain,(
% 2.52/0.63 ~spl12_8 | ~spl12_10 | ~spl12_13 | ~spl12_32 | ~spl12_35),
% 2.52/0.63 inference(avatar_contradiction_clause,[],[f3906])).
% 2.52/0.63 thf(f3956,plain,(
% 2.52/0.63 ( ! [X0 : $i] : (($true != $true) | ($false = (((^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X0)))) ) | (~spl12_13 | spl12_32)),
% 2.52/0.63 inference(constrained_superposition,[],[f1677,f264])).
% 2.52/0.63 thf(f3970,plain,(
% 2.52/0.63 ( ! [X0 : $i] : (($false = (((^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X0)))) ) | (~spl12_13 | spl12_32)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f3956])).
% 2.52/0.63 thf(f3971,plain,(
% 2.52/0.63 ( ! [X0 : $i] : (($false = ((sK2 @ X0)))) ) | (~spl12_13 | spl12_32)),
% 2.52/0.63 inference(beta-eta_normalization,[],[f3970])).
% 2.52/0.63 thf(f4068,plain,(
% 2.52/0.63 ($true = $false) | ($false = ((sK1 @ (sK7 @ (sK11 @ sK1))))) | ($false = ((sK1 @ (sK11 @ sK1)))) | (~spl12_7 | ~spl12_36)),
% 2.52/0.63 inference(constrained_superposition,[],[f1926,f241])).
% 2.52/0.63 thf(f4073,plain,(
% 2.52/0.63 ($false = ((sK1 @ (sK7 @ (sK11 @ sK1))))) | ($false = ((sK1 @ (sK11 @ sK1)))) | (~spl12_7 | ~spl12_36)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f4068])).
% 2.52/0.63 thf(f4100,plain,(
% 2.52/0.63 ($false = ((sK1 @ (sK7 @ (sK11 @ sK1))))) | (~spl12_7 | ~spl12_13 | ~spl12_36)),
% 2.52/0.63 inference(forward_subsumption_resolution,[],[f4073,f1669])).
% 2.52/0.63 thf(f4124,plain,(
% 2.52/0.63 ($true = $false) | ($false = ((sK1 @ (sK11 @ sK1)))) | (~spl12_6 | ~spl12_7 | ~spl12_13 | ~spl12_36)),
% 2.52/0.63 inference(constrained_superposition,[],[f237,f4100])).
% 2.52/0.63 thf(f4125,plain,(
% 2.52/0.63 ($false = ((sK1 @ (sK11 @ sK1)))) | (~spl12_6 | ~spl12_7 | ~spl12_13 | ~spl12_36)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f4124])).
% 2.52/0.63 thf(f4138,plain,(
% 2.52/0.63 ($true = $false) | (~spl12_6 | ~spl12_7 | ~spl12_13 | ~spl12_33 | ~spl12_36)),
% 2.52/0.63 inference(constrained_superposition,[],[f4125,f1684])).
% 2.52/0.63 thf(f4160,plain,(
% 2.52/0.63 $false | (~spl12_6 | ~spl12_7 | ~spl12_13 | ~spl12_33 | ~spl12_36)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f4138])).
% 2.52/0.63 thf(f4161,plain,(
% 2.52/0.63 ~spl12_6 | ~spl12_7 | ~spl12_13 | ~spl12_33 | ~spl12_36),
% 2.52/0.63 inference(avatar_contradiction_clause,[],[f4160])).
% 2.52/0.63 thf(f4171,plain,(
% 2.52/0.63 ($true = $false) | (~spl12_1 | ~spl12_13 | spl12_32)),
% 2.52/0.63 inference(forward_demodulation,[],[f217,f3971])).
% 2.52/0.63 thf(f4172,plain,(
% 2.52/0.63 $false | (~spl12_1 | ~spl12_13 | spl12_32)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f4171])).
% 2.52/0.63 thf(f4173,plain,(
% 2.52/0.63 ~spl12_1 | ~spl12_13 | spl12_32),
% 2.52/0.63 inference(avatar_contradiction_clause,[],[f4172])).
% 2.52/0.63 thf(f4190,plain,(
% 2.52/0.63 $false | ~spl12_18),
% 2.52/0.63 inference(equality_resolution,[],[f381])).
% 2.52/0.63 thf(f4191,plain,(
% 2.52/0.63 ~spl12_18),
% 2.52/0.63 inference(avatar_contradiction_clause,[],[f4190])).
% 2.52/0.63 thf(f4212,plain,(
% 2.52/0.63 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((sK0 @ (sK11 @ (^[Y0 : $i]: (sK1 @ ((^[Y1 : $i]: (Y1)) @ Y0)))) @ X1))) | ($false = (((^[Y0 : $i]: (sK1 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X1))) | (sK3 != X0)) ) | (~spl12_2 | ~spl12_14)),
% 2.52/0.63 inference(constrained_superposition,[],[f221,f268])).
% 2.52/0.63 thf(f4214,plain,(
% 2.52/0.63 ( ! [X0 : $i] : (($true = $false) | ($true = (((^[Y0 : $i]: (sK1 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ (sK11 @ (^[Y0 : $i]: (sK1 @ ((^[Y1 : $i]: (Y1)) @ Y0))))))) | (sK3 != X0)) ) | (~spl12_2 | ~spl12_13)),
% 2.52/0.63 inference(constrained_superposition,[],[f221,f264])).
% 2.52/0.63 thf(f4238,plain,(
% 2.52/0.63 ( ! [X0 : $i] : (($true = (((^[Y0 : $i]: (sK1 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ (sK11 @ (^[Y0 : $i]: (sK1 @ ((^[Y1 : $i]: (Y1)) @ Y0))))))) | (sK3 != X0)) ) | (~spl12_2 | ~spl12_13)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f4214])).
% 2.52/0.63 thf(f4239,plain,(
% 2.52/0.63 ( ! [X0 : $i] : (($true = ((sK1 @ (sK11 @ sK1)))) | (sK3 != X0)) ) | (~spl12_2 | ~spl12_13)),
% 2.52/0.63 inference(beta-eta_normalization,[],[f4238])).
% 2.52/0.63 thf(f4242,plain,(
% 2.52/0.63 ( ! [X0 : $i,X1 : $i] : (($false = ((sK0 @ (sK11 @ (^[Y0 : $i]: (sK1 @ ((^[Y1 : $i]: (Y1)) @ Y0)))) @ X1))) | ($false = (((^[Y0 : $i]: (sK1 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X1))) | (sK3 != X0)) ) | (~spl12_2 | ~spl12_14)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f4212])).
% 2.52/0.63 thf(f4243,plain,(
% 2.52/0.63 ( ! [X0 : $i,X1 : $i] : (($false = ((sK0 @ (sK11 @ sK1) @ X1))) | ($false = ((sK1 @ X1))) | (sK3 != X0)) ) | (~spl12_2 | ~spl12_14)),
% 2.52/0.63 inference(beta-eta_normalization,[],[f4242])).
% 2.52/0.63 thf(f4249,plain,(
% 2.52/0.63 spl12_18 | spl12_33 | ~spl12_2 | ~spl12_13),
% 2.52/0.63 inference(avatar_split_clause,[],[f4239,f263,f219,f1682,f380])).
% 2.52/0.63 thf(f4252,plain,(
% 2.52/0.63 spl12_18 | spl12_36 | ~spl12_2 | ~spl12_14),
% 2.52/0.63 inference(avatar_split_clause,[],[f4243,f267,f219,f1925,f380])).
% 2.52/0.63 thf(f4253,plain,(
% 2.52/0.63 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((sK0 @ (sK11 @ (^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0)))) @ X1))) | ($false = (((^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X1))) | (sK6 != X0)) ) | (~spl12_5 | ~spl12_14)),
% 2.52/0.63 inference(constrained_superposition,[],[f234,f268])).
% 2.52/0.63 thf(f4255,plain,(
% 2.52/0.63 ( ! [X0 : $i] : (($true = $false) | ($true = (((^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ (sK11 @ (^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))))))) | (sK6 != X0)) ) | (~spl12_5 | ~spl12_13)),
% 2.52/0.63 inference(constrained_superposition,[],[f234,f264])).
% 2.52/0.63 thf(f4279,plain,(
% 2.52/0.63 ( ! [X0 : $i] : (($true = (((^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ (sK11 @ (^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))))))) | (sK6 != X0)) ) | (~spl12_5 | ~spl12_13)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f4255])).
% 2.52/0.63 thf(f4280,plain,(
% 2.52/0.63 ( ! [X0 : $i] : (($true = ((sK2 @ (sK11 @ sK2)))) | (sK6 != X0)) ) | (~spl12_5 | ~spl12_13)),
% 2.52/0.63 inference(beta-eta_normalization,[],[f4279])).
% 2.52/0.63 thf(f4283,plain,(
% 2.52/0.63 ( ! [X0 : $i,X1 : $i] : (($false = ((sK0 @ (sK11 @ (^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0)))) @ X1))) | ($false = (((^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X1))) | (sK6 != X0)) ) | (~spl12_5 | ~spl12_14)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f4253])).
% 2.52/0.63 thf(f4284,plain,(
% 2.52/0.63 ( ! [X0 : $i,X1 : $i] : (($false = ((sK0 @ (sK11 @ sK2) @ X1))) | ($false = ((sK2 @ X1))) | (sK6 != X0)) ) | (~spl12_5 | ~spl12_14)),
% 2.52/0.63 inference(beta-eta_normalization,[],[f4283])).
% 2.52/0.63 thf(f4290,plain,(
% 2.52/0.63 spl12_16 | spl12_32 | ~spl12_5 | ~spl12_13),
% 2.52/0.63 inference(avatar_split_clause,[],[f4280,f263,f232,f1676,f372])).
% 2.52/0.63 thf(f4293,plain,(
% 2.52/0.63 spl12_16 | spl12_35 | ~spl12_5 | ~spl12_14),
% 2.52/0.63 inference(avatar_split_clause,[],[f4284,f267,f232,f1918,f372])).
% 2.52/0.63 thf(f4622,plain,(
% 2.52/0.63 ($true = $false) | ($false = ((sK1 @ (sK7 @ (sK10 @ sK1))))) | ($false = ((sK1 @ (sK10 @ sK1)))) | (~spl12_7 | ~spl12_25)),
% 2.52/0.63 inference(constrained_superposition,[],[f1022,f241])).
% 2.52/0.63 thf(f4624,plain,(
% 2.52/0.63 ($true = $false) | ($false = ((sK1 @ (sK8 @ (sK10 @ sK1))))) | ($false = ((sK1 @ (sK10 @ sK1)))) | (~spl12_11 | ~spl12_25)),
% 2.52/0.63 inference(constrained_superposition,[],[f1022,f256])).
% 2.52/0.63 thf(f4643,plain,(
% 2.52/0.63 ($false = ((sK1 @ (sK8 @ (sK10 @ sK1))))) | ($false = ((sK1 @ (sK10 @ sK1)))) | (~spl12_11 | ~spl12_25)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f4624])).
% 2.52/0.63 thf(f4645,plain,(
% 2.52/0.63 ($false = ((sK1 @ (sK7 @ (sK10 @ sK1))))) | ($false = ((sK1 @ (sK10 @ sK1)))) | (~spl12_7 | ~spl12_25)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f4622])).
% 2.52/0.63 thf(f4649,definition,(
% 2.52/0.63 spl12_44 <=> ($false = ((sK1 @ (sK8 @ (sK10 @ sK1)))))),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_44])],[avatar_definition])).
% 2.52/0.63 thf(f4651,plain,(
% 2.52/0.63 ($false = ((sK1 @ (sK8 @ (sK10 @ sK1))))) | ~spl12_44),
% 2.52/0.63 inference(avatar_component_clause,[],[f4649])).
% 2.52/0.63 thf(f4653,definition,(
% 2.52/0.63 spl12_45 <=> ($false = ((sK1 @ (sK10 @ sK1))))),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_45])],[avatar_definition])).
% 2.52/0.63 thf(f4655,plain,(
% 2.52/0.63 ($false = ((sK1 @ (sK10 @ sK1)))) | ~spl12_45),
% 2.52/0.63 inference(avatar_component_clause,[],[f4653])).
% 2.52/0.63 thf(f4658,definition,(
% 2.52/0.63 spl12_46 <=> ($false = ((sK1 @ (sK7 @ (sK10 @ sK1)))))),
% 2.52/0.63 introduced(definition,[new_symbols(definition,[spl12_46])],[avatar_definition])).
% 2.52/0.63 thf(f4660,plain,(
% 2.52/0.63 ($false = ((sK1 @ (sK7 @ (sK10 @ sK1))))) | ~spl12_46),
% 2.52/0.63 inference(avatar_component_clause,[],[f4658])).
% 2.52/0.63 thf(f4662,plain,(
% 2.52/0.63 spl12_45 | spl12_44 | ~spl12_11 | ~spl12_25),
% 2.52/0.63 inference(avatar_split_clause,[],[f4643,f1021,f255,f4649,f4653])).
% 2.52/0.63 thf(f4663,plain,(
% 2.52/0.63 spl12_45 | spl12_46 | ~spl12_7 | ~spl12_25),
% 2.52/0.63 inference(avatar_split_clause,[],[f4645,f1021,f240,f4658,f4653])).
% 2.52/0.63 thf(f4690,plain,(
% 2.52/0.63 ($true = $false) | ($false = ((sK1 @ (sK11 @ sK1)))) | ($false = ((sK1 @ (sK8 @ (sK11 @ sK1))))) | (~spl12_11 | ~spl12_36)),
% 2.52/0.63 inference(constrained_superposition,[],[f256,f1926])).
% 2.52/0.63 thf(f4691,plain,(
% 2.52/0.63 ($false = ((sK1 @ (sK11 @ sK1)))) | ($false = ((sK1 @ (sK8 @ (sK11 @ sK1))))) | (~spl12_11 | ~spl12_36)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f4690])).
% 2.52/0.63 thf(f4706,plain,(
% 2.52/0.63 ($false = ((sK1 @ (sK8 @ (sK11 @ sK1))))) | (~spl12_11 | ~spl12_13 | ~spl12_36)),
% 2.52/0.63 inference(forward_subsumption_resolution,[],[f4691,f1669])).
% 2.52/0.63 thf(f4717,plain,(
% 2.52/0.63 ($true = $false) | ($false = ((sK1 @ (sK11 @ sK1)))) | (~spl12_9 | ~spl12_11 | ~spl12_13 | ~spl12_36)),
% 2.52/0.63 inference(constrained_superposition,[],[f248,f4706])).
% 2.52/0.63 thf(f4718,plain,(
% 2.52/0.63 ($false = ((sK1 @ (sK11 @ sK1)))) | (~spl12_9 | ~spl12_11 | ~spl12_13 | ~spl12_36)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f4717])).
% 2.52/0.63 thf(f4731,plain,(
% 2.52/0.63 ($true = $false) | (~spl12_9 | ~spl12_11 | ~spl12_13 | ~spl12_33 | ~spl12_36)),
% 2.52/0.63 inference(constrained_superposition,[],[f4718,f1684])).
% 2.52/0.63 thf(f4753,plain,(
% 2.52/0.63 $false | (~spl12_9 | ~spl12_11 | ~spl12_13 | ~spl12_33 | ~spl12_36)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f4731])).
% 2.52/0.63 thf(f4754,plain,(
% 2.52/0.63 ~spl12_9 | ~spl12_11 | ~spl12_13 | ~spl12_33 | ~spl12_36),
% 2.52/0.63 inference(avatar_contradiction_clause,[],[f4753])).
% 2.52/0.63 thf(f4829,plain,(
% 2.52/0.63 ($true = $false) | (~spl12_19 | ~spl12_45)),
% 2.52/0.63 inference(forward_demodulation,[],[f385,f4655])).
% 2.52/0.63 thf(f4830,plain,(
% 2.52/0.63 $false | (~spl12_19 | ~spl12_45)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f4829])).
% 2.52/0.63 thf(f4831,plain,(
% 2.52/0.63 ~spl12_19 | ~spl12_45),
% 2.52/0.63 inference(avatar_contradiction_clause,[],[f4830])).
% 2.52/0.63 thf(f4838,plain,(
% 2.52/0.63 spl12_18 | spl12_19 | ~spl12_2 | ~spl12_12),
% 2.52/0.63 inference(avatar_split_clause,[],[f465,f260,f219,f383,f380])).
% 2.52/0.63 thf(f4858,plain,(
% 2.52/0.63 ($true = $false) | ($false = ((sK1 @ (sK10 @ sK1)))) | (~spl12_9 | ~spl12_44)),
% 2.52/0.63 inference(constrained_superposition,[],[f248,f4651])).
% 2.52/0.63 thf(f4859,plain,(
% 2.52/0.63 ($false = ((sK1 @ (sK10 @ sK1)))) | (~spl12_9 | ~spl12_44)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f4858])).
% 2.52/0.63 thf(f4862,plain,(
% 2.52/0.63 ($true = $false) | (~spl12_9 | ~spl12_19 | ~spl12_44)),
% 2.52/0.63 inference(constrained_superposition,[],[f4859,f385])).
% 2.52/0.63 thf(f4868,plain,(
% 2.52/0.63 $false | (~spl12_9 | ~spl12_19 | ~spl12_44)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f4862])).
% 2.52/0.63 thf(f4869,plain,(
% 2.52/0.63 ~spl12_9 | ~spl12_19 | ~spl12_44),
% 2.52/0.63 inference(avatar_contradiction_clause,[],[f4868])).
% 2.52/0.63 thf(f4890,plain,(
% 2.52/0.63 ($true = $false) | ($false = ((sK1 @ (sK10 @ sK1)))) | (~spl12_6 | ~spl12_46)),
% 2.52/0.63 inference(constrained_superposition,[],[f4660,f237])).
% 2.52/0.63 thf(f4891,plain,(
% 2.52/0.63 ($false = ((sK1 @ (sK10 @ sK1)))) | (~spl12_6 | ~spl12_46)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f4890])).
% 2.52/0.63 thf(f4893,plain,(
% 2.52/0.63 ($true = $false) | (~spl12_6 | ~spl12_19 | ~spl12_46)),
% 2.52/0.63 inference(constrained_superposition,[],[f4891,f385])).
% 2.52/0.63 thf(f4899,plain,(
% 2.52/0.63 $false | (~spl12_6 | ~spl12_19 | ~spl12_46)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f4893])).
% 2.52/0.63 thf(f4900,plain,(
% 2.52/0.63 ~spl12_6 | ~spl12_19 | ~spl12_46),
% 2.52/0.63 inference(avatar_contradiction_clause,[],[f4899])).
% 2.52/0.63 thf(f4990,plain,(
% 2.52/0.63 ( ! [X0 : $i] : (($true = $false) | ($true = (((^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ (sK10 @ (^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))))))) | (sK4 != X0)) ) | (~spl12_1 | ~spl12_12)),
% 2.52/0.63 inference(constrained_superposition,[],[f217,f261])).
% 2.52/0.63 thf(f5010,plain,(
% 2.52/0.63 ( ! [X0 : $i] : (($true = (((^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ (sK10 @ (^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))))))) | (sK4 != X0)) ) | (~spl12_1 | ~spl12_12)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f4990])).
% 2.52/0.63 thf(f5011,plain,(
% 2.52/0.63 ( ! [X0 : $i] : (($true = ((sK2 @ (sK10 @ sK2)))) | (sK4 != X0)) ) | (~spl12_1 | ~spl12_12)),
% 2.52/0.63 inference(beta-eta_normalization,[],[f5010])).
% 2.52/0.63 thf(f5157,plain,(
% 2.52/0.63 ( ! [X0 : $i] : ((sK4 != X0)) ) | (~spl12_1 | ~spl12_12 | spl12_17)),
% 2.52/0.63 inference(forward_subsumption_resolution,[],[f5011,f376])).
% 2.52/0.63 thf(f5165,plain,(
% 2.52/0.63 $false | (~spl12_1 | ~spl12_12 | spl12_17)),
% 2.52/0.63 inference(equality_resolution,[],[f5157])).
% 2.52/0.63 thf(f5166,plain,(
% 2.52/0.63 ~spl12_1 | ~spl12_12 | spl12_17),
% 2.52/0.63 inference(avatar_contradiction_clause,[],[f5165])).
% 2.52/0.63 thf(f5222,plain,(
% 2.52/0.63 $false | ~spl12_42),
% 2.52/0.63 inference(equality_resolution,[],[f3724])).
% 2.52/0.63 thf(f5223,plain,(
% 2.52/0.63 ~spl12_42),
% 2.52/0.63 inference(avatar_contradiction_clause,[],[f5222])).
% 2.52/0.63 thf(f5592,plain,(
% 2.52/0.63 $false | ~spl12_22),
% 2.52/0.63 inference(equality_resolution,[],[f1009])).
% 2.52/0.63 thf(f5593,plain,(
% 2.52/0.63 ~spl12_22),
% 2.52/0.63 inference(avatar_contradiction_clause,[],[f5592])).
% 2.52/0.63 thf(f6005,plain,(
% 2.52/0.63 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((sK0 @ (sK10 @ (^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0)))) @ X1))) | ($false = (((^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X1))) | (((sK11 @ sK2)) != X0)) ) | (~spl12_15 | ~spl12_32)),
% 2.52/0.63 inference(constrained_superposition,[],[f272,f1678])).
% 2.52/0.63 thf(f6007,plain,(
% 2.52/0.63 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((sK0 @ (sK10 @ (^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0)))) @ X1))) | ($false = (((^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X1))) | (((sK10 @ sK2)) != X0)) ) | (~spl12_15 | ~spl12_17)),
% 2.52/0.63 inference(constrained_superposition,[],[f272,f377])).
% 2.52/0.63 thf(f6151,plain,(
% 2.52/0.63 ( ! [X0 : $i,X1 : $i] : (($false = ((sK0 @ (sK10 @ (^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0)))) @ X1))) | ($false = (((^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X1))) | (((sK10 @ sK2)) != X0)) ) | (~spl12_15 | ~spl12_17)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f6007])).
% 2.52/0.63 thf(f6152,plain,(
% 2.52/0.63 ( ! [X0 : $i,X1 : $i] : (($false = ((sK0 @ (sK10 @ sK2) @ X1))) | ($false = ((sK2 @ X1))) | (((sK10 @ sK2)) != X0)) ) | (~spl12_15 | ~spl12_17)),
% 2.52/0.63 inference(beta-eta_normalization,[],[f6151])).
% 2.52/0.63 thf(f6155,plain,(
% 2.52/0.63 ( ! [X0 : $i,X1 : $i] : (($false = ((sK0 @ (sK10 @ (^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0)))) @ X1))) | ($false = (((^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X1))) | (((sK11 @ sK2)) != X0)) ) | (~spl12_15 | ~spl12_32)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f6005])).
% 2.52/0.63 thf(f6156,plain,(
% 2.52/0.63 ( ! [X0 : $i,X1 : $i] : (($false = ((sK0 @ (sK10 @ sK2) @ X1))) | ($false = ((sK2 @ X1))) | (((sK11 @ sK2)) != X0)) ) | (~spl12_15 | ~spl12_32)),
% 2.52/0.63 inference(beta-eta_normalization,[],[f6155])).
% 2.52/0.63 thf(f6192,plain,(
% 2.52/0.63 spl12_22 | spl12_23 | ~spl12_15 | ~spl12_17),
% 2.52/0.63 inference(avatar_split_clause,[],[f6152,f375,f271,f1011,f1008])).
% 2.52/0.63 thf(f6193,plain,(
% 2.52/0.63 spl12_42 | spl12_23 | ~spl12_15 | ~spl12_32),
% 2.52/0.63 inference(avatar_split_clause,[],[f6156,f1676,f271,f1011,f3723])).
% 2.52/0.63 thf(f6410,plain,(
% 2.52/0.63 ($true = $false) | ($false = ((sK2 @ (sK10 @ sK2)))) | ($false = ((sK2 @ (sK5 @ (sK10 @ sK2))))) | (~spl12_4 | ~spl12_23)),
% 2.52/0.63 inference(constrained_superposition,[],[f229,f1012])).
% 2.52/0.63 thf(f6411,plain,(
% 2.52/0.63 ($false = ((sK2 @ (sK10 @ sK2)))) | ($false = ((sK2 @ (sK5 @ (sK10 @ sK2))))) | (~spl12_4 | ~spl12_23)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f6410])).
% 2.52/0.63 thf(f6430,plain,(
% 2.52/0.63 ($false = ((sK2 @ (sK5 @ (sK10 @ sK2))))) | (~spl12_4 | ~spl12_12 | ~spl12_23)),
% 2.52/0.63 inference(forward_subsumption_resolution,[],[f6411,f370])).
% 2.52/0.63 thf(f6444,plain,(
% 2.52/0.63 ($true = $false) | ($false = ((sK2 @ (sK10 @ sK2)))) | (~spl12_3 | ~spl12_4 | ~spl12_12 | ~spl12_23)),
% 2.52/0.63 inference(constrained_superposition,[],[f225,f6430])).
% 2.52/0.63 thf(f6445,plain,(
% 2.52/0.63 ($false = ((sK2 @ (sK10 @ sK2)))) | (~spl12_3 | ~spl12_4 | ~spl12_12 | ~spl12_23)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f6444])).
% 2.52/0.63 thf(f6467,plain,(
% 2.52/0.63 ($true = $false) | (~spl12_3 | ~spl12_4 | ~spl12_12 | ~spl12_17 | ~spl12_23)),
% 2.52/0.63 inference(constrained_superposition,[],[f6445,f377])).
% 2.52/0.63 thf(f6499,plain,(
% 2.52/0.63 $false | (~spl12_3 | ~spl12_4 | ~spl12_12 | ~spl12_17 | ~spl12_23)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f6467])).
% 2.52/0.63 thf(f6500,plain,(
% 2.52/0.63 ~spl12_3 | ~spl12_4 | ~spl12_12 | ~spl12_17 | ~spl12_23),
% 2.52/0.63 inference(avatar_contradiction_clause,[],[f6499])).
% 2.52/0.63 thf(f6610,plain,(
% 2.52/0.63 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((sK0 @ (sK11 @ (^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0)))) @ X1))) | ($false = (((^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X1))) | (((sK11 @ sK2)) != X0)) ) | (~spl12_14 | ~spl12_32)),
% 2.52/0.63 inference(constrained_superposition,[],[f268,f1678])).
% 2.52/0.63 thf(f6739,plain,(
% 2.52/0.63 ( ! [X0 : $i,X1 : $i] : (($false = ((sK0 @ (sK11 @ (^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0)))) @ X1))) | ($false = (((^[Y0 : $i]: (sK2 @ ((^[Y1 : $i]: (Y1)) @ Y0))) @ X1))) | (((sK11 @ sK2)) != X0)) ) | (~spl12_14 | ~spl12_32)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f6610])).
% 2.52/0.63 thf(f6740,plain,(
% 2.52/0.63 ( ! [X0 : $i,X1 : $i] : (($false = ((sK0 @ (sK11 @ sK2) @ X1))) | ($false = ((sK2 @ X1))) | (((sK11 @ sK2)) != X0)) ) | (~spl12_14 | ~spl12_32)),
% 2.52/0.63 inference(beta-eta_normalization,[],[f6739])).
% 2.52/0.63 thf(f6778,plain,(
% 2.52/0.63 spl12_42 | spl12_35 | ~spl12_14 | ~spl12_32),
% 2.52/0.63 inference(avatar_split_clause,[],[f6740,f1676,f267,f1918,f3723])).
% 2.52/0.63 thf(f6803,plain,(
% 2.52/0.63 ($true = $false) | ($false = ((sK2 @ (sK11 @ sK2)))) | ($false = ((sK2 @ (sK5 @ (sK11 @ sK2))))) | (~spl12_4 | ~spl12_35)),
% 2.52/0.63 inference(constrained_superposition,[],[f229,f1919])).
% 2.52/0.63 thf(f6804,plain,(
% 2.52/0.63 ($false = ((sK2 @ (sK11 @ sK2)))) | ($false = ((sK2 @ (sK5 @ (sK11 @ sK2))))) | (~spl12_4 | ~spl12_35)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f6803])).
% 2.52/0.63 thf(f6815,plain,(
% 2.52/0.63 ($false = ((sK2 @ (sK5 @ (sK11 @ sK2))))) | (~spl12_4 | ~spl12_13 | ~spl12_35)),
% 2.52/0.63 inference(forward_subsumption_resolution,[],[f6804,f1669])).
% 2.52/0.63 thf(f6824,plain,(
% 2.52/0.63 ($true = $false) | ($false = ((sK2 @ (sK11 @ sK2)))) | (~spl12_3 | ~spl12_4 | ~spl12_13 | ~spl12_35)),
% 2.52/0.63 inference(constrained_superposition,[],[f225,f6815])).
% 2.52/0.63 thf(f6825,plain,(
% 2.52/0.63 ($false = ((sK2 @ (sK11 @ sK2)))) | (~spl12_3 | ~spl12_4 | ~spl12_13 | ~spl12_35)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f6824])).
% 2.52/0.63 thf(f6838,plain,(
% 2.52/0.63 ($true = $false) | (~spl12_3 | ~spl12_4 | ~spl12_13 | ~spl12_32 | ~spl12_35)),
% 2.52/0.63 inference(constrained_superposition,[],[f6825,f1678])).
% 2.52/0.63 thf(f6860,plain,(
% 2.52/0.63 $false | (~spl12_3 | ~spl12_4 | ~spl12_13 | ~spl12_32 | ~spl12_35)),
% 2.52/0.63 inference(trivial_inequality_removal,[],[f6838])).
% 2.52/0.63 thf(f6861,plain,(
% 2.52/0.63 ~spl12_3 | ~spl12_4 | ~spl12_13 | ~spl12_32 | ~spl12_35),
% 2.52/0.63 inference(avatar_contradiction_clause,[],[f6860])).
% 2.52/0.63 cnf(s1, plain, spl12_1 | spl12_2, inference(sat_conversion,[],[f222])).
% 2.52/0.63 cnf(s2, plain, spl12_2 | spl12_3, inference(sat_conversion,[],[f226])).
% 2.52/0.63 cnf(s3, plain, spl12_2 | spl12_4, inference(sat_conversion,[],[f230])).
% 2.52/0.63 cnf(s4, plain, spl12_5 | spl12_6, inference(sat_conversion,[],[f238])).
% 2.52/0.63 cnf(s5, plain, spl12_5 | spl12_7, inference(sat_conversion,[],[f242])).
% 2.52/0.63 cnf(s6, plain, spl12_8 | spl12_9, inference(sat_conversion,[],[f249])).
% 2.52/0.63 cnf(s7, plain, spl12_9 | spl12_10, inference(sat_conversion,[],[f253])).
% 2.52/0.63 cnf(s8, plain, spl12_8 | spl12_11, inference(sat_conversion,[],[f257])).
% 2.52/0.63 cnf(s9, plain, spl12_10 | spl12_11, inference(sat_conversion,[],[f258])).
% 2.52/0.63 cnf(s10, plain, spl12_12 | spl12_13, inference(sat_conversion,[],[f265])).
% 2.52/0.63 cnf(s11, plain, spl12_12 | spl12_14, inference(sat_conversion,[],[f269])).
% 2.52/0.63 cnf(s12, plain, spl12_13 | spl12_15, inference(sat_conversion,[],[f273])).
% 2.52/0.63 cnf(s13, plain, spl12_14 | spl12_15, inference(sat_conversion,[],[f274])).
% 2.52/0.63 cnf(s16, plain, ~spl12_5 | ~spl12_12 | spl12_16 | spl12_17, inference(sat_conversion,[],[f387])).
% 2.52/0.63 cnf(s18, plain, ~spl12_16, inference(sat_conversion,[],[f390])).
% 2.52/0.63 cnf(s26, plain, ~spl12_5 | ~spl12_15 | spl12_16 | spl12_23, inference(sat_conversion,[],[f1031])).
% 2.52/0.63 cnf(s28, plain, ~spl12_2 | ~spl12_15 | spl12_18 | spl12_25, inference(sat_conversion,[],[f1035])).
% 2.52/0.63 cnf(s40, plain, ~spl12_8 | ~spl12_10 | ~spl12_12 | ~spl12_17 | ~spl12_23, inference(sat_conversion,[],[f1441])).
% 2.52/0.63 cnf(s87, plain, ~spl12_8 | ~spl12_10 | ~spl12_13 | ~spl12_32 | ~spl12_35, inference(sat_conversion,[],[f3907])).
% 2.52/0.63 cnf(s89, plain, ~spl12_6 | ~spl12_7 | ~spl12_13 | ~spl12_33 | ~spl12_36, inference(sat_conversion,[],[f4161])).
% 2.52/0.63 cnf(s90, plain, ~spl12_1 | ~spl12_13 | spl12_32, inference(sat_conversion,[],[f4173])).
% 2.52/0.63 cnf(s102, plain, ~spl12_18, inference(sat_conversion,[],[f4191])).
% 2.52/0.63 cnf(s117, plain, ~spl12_2 | ~spl12_13 | spl12_18 | spl12_33, inference(sat_conversion,[],[f4249])).
% 2.52/0.63 cnf(s118, plain, ~spl12_2 | ~spl12_14 | spl12_18 | spl12_36, inference(sat_conversion,[],[f4252])).
% 2.52/0.63 cnf(s122, plain, ~spl12_5 | ~spl12_13 | spl12_16 | spl12_32, inference(sat_conversion,[],[f4290])).
% 2.52/0.63 cnf(s123, plain, ~spl12_5 | ~spl12_14 | spl12_16 | spl12_35, inference(sat_conversion,[],[f4293])).
% 2.52/0.63 cnf(s130, plain, ~spl12_11 | ~spl12_25 | spl12_44 | spl12_45, inference(sat_conversion,[],[f4662])).
% 2.52/0.63 cnf(s131, plain, ~spl12_7 | ~spl12_25 | spl12_45 | spl12_46, inference(sat_conversion,[],[f4663])).
% 2.52/0.63 cnf(s133, plain, ~spl12_9 | ~spl12_11 | ~spl12_13 | ~spl12_33 | ~spl12_36, inference(sat_conversion,[],[f4754])).
% 2.52/0.63 cnf(s134, plain, ~spl12_19 | ~spl12_45, inference(sat_conversion,[],[f4831])).
% 2.52/0.63 cnf(s141, plain, ~spl12_2 | ~spl12_12 | spl12_18 | spl12_19, inference(sat_conversion,[],[f4838])).
% 2.52/0.63 cnf(s143, plain, ~spl12_9 | ~spl12_19 | ~spl12_44, inference(sat_conversion,[],[f4869])).
% 2.52/0.63 cnf(s145, plain, ~spl12_6 | ~spl12_19 | ~spl12_46, inference(sat_conversion,[],[f4900])).
% 2.52/0.63 cnf(s146, plain, ~spl12_1 | ~spl12_12 | spl12_17, inference(sat_conversion,[],[f5166])).
% 2.52/0.63 cnf(s153, plain, ~spl12_42, inference(sat_conversion,[],[f5223])).
% 2.52/0.63 cnf(s169, plain, ~spl12_22, inference(sat_conversion,[],[f5593])).
% 2.52/0.63 cnf(s177, plain, ~spl12_15 | ~spl12_17 | spl12_22 | spl12_23, inference(sat_conversion,[],[f6192])).
% 2.52/0.63 cnf(s178, plain, ~spl12_15 | spl12_23 | ~spl12_32 | spl12_42, inference(sat_conversion,[],[f6193])).
% 2.52/0.63 cnf(s180, plain, ~spl12_3 | ~spl12_4 | ~spl12_12 | ~spl12_17 | ~spl12_23, inference(sat_conversion,[],[f6500])).
% 2.52/0.63 cnf(s186, plain, ~spl12_14 | ~spl12_32 | spl12_35 | spl12_42, inference(sat_conversion,[],[f6778])).
% 2.52/0.63 cnf(s188, plain, ~spl12_3 | ~spl12_4 | ~spl12_13 | ~spl12_32 | ~spl12_35, inference(sat_conversion,[],[f6861])).
% 2.52/0.63 cnf(s224, plain, ~spl12_2 | ~spl12_15 | spl12_25, inference(rat,[],[s28,s102])).
% 2.52/0.63 cnf(s231, plain, ~spl12_5 | ~spl12_12 | spl12_17, inference(rat,[],[s16,s18])).
% 2.52/0.63 cnf(s234, plain, spl12_12 | spl12_5 | ~spl12_2, inference(rat,[],[s89,s117,s118,s10,s11,s5,s4,s102])).
% 2.52/0.63 cnf(s235, plain, spl12_15 | spl12_5 | ~spl12_2, inference(rat,[],[s89,s117,s118,s12,s13,s5,s4,s102])).
% 2.52/0.63 cnf(s236, plain, spl12_5 | ~spl12_2, inference(rat,[],[s224,s131,s235,s134,s145,s141,s234,s4,s5,s102])).
% 2.52/0.63 cnf(s240, plain, spl12_9 | ~spl12_32 | ~spl12_35 | ~spl12_13, inference(rat,[],[s87,s6,s7])).
% 2.52/0.63 cnf(s241, plain, spl12_15 | ~spl12_2, inference(rat,[],[s87,s8,s9,s133,s240,s122,s117,s123,s118,s12,s13,s236,s18,s102])).
% 2.52/0.63 cnf(s242, plain, ~spl12_13 | ~spl12_14 | ~spl12_2, inference(rat,[],[s87,s8,s9,s133,s240,s122,s117,s118,s123,s236,s18,s102])).
% 2.52/0.63 cnf(s243, plain, spl12_9 | ~spl12_17 | ~spl12_12 | ~spl12_23, inference(rat,[],[s40,s6,s7])).
% 2.52/0.63 cnf(s244, plain, ~spl12_12 | ~spl12_2, inference(rat,[],[s40,s8,s9,s130,s143,s243,s134,s231,s141,s224,s26,s241,s236,s102,s18])).
% 2.52/0.63 cnf(s245, plain, ~spl12_2, inference(rat,[],[s242,s10,s11,s244])).
% 2.52/0.63 cnf(s246, plain, spl12_4, inference(rat,[],[s3,s245])).
% 2.52/0.63 cnf(s247, plain, spl12_3, inference(rat,[],[s2,s245])).
% 2.52/0.63 cnf(s248, plain, spl12_1, inference(rat,[],[s1,s245])).
% 2.52/0.63 cnf(s249, plain, spl12_13, inference(rat,[],[s177,s180,s146,s10,s12,s169,s247,s246,s248])).
% 2.52/0.63 cnf(s250, plain, spl12_32, inference(rat,[],[s90,s248,s249])).
% 2.52/0.63 cnf(s251, plain, ~spl12_35, inference(rat,[],[s188,s249,s247,s246,s250])).
% 2.52/0.63 cnf(s252, plain, ~spl12_14, inference(rat,[],[s186,s153,s251,s250])).
% 2.52/0.63 cnf(s253, plain, spl12_15, inference(rat,[],[s13,s252])).
% 2.52/0.63 cnf(s254, plain, spl12_12, inference(rat,[],[s11,s252])).
% 2.52/0.63 cnf(s256, plain, spl12_23, inference(rat,[],[s178,s153,s250,s253])).
% 2.52/0.63 cnf(s257, plain, spl12_17, inference(rat,[],[s146,s248,s254])).
% 2.52/0.63 cnf(s259, plain, $false, inference(rat,[],[s180,s254,s246,s247,s256,s257])).
% 2.52/0.63 thf(f6866,plain,(
% 2.52/0.63 $false),
% 2.52/0.63 inference(avatar_sat_refutation,[],[s259])).
% 2.52/0.63 % SZS output end Proof for theBenchmark
% 2.52/0.63 % (2874013)------------------------------
% 2.52/0.63 % (2874013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.52/0.63 % (2874013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.52/0.63 % (2874013)CaDiCaL version: 2.1.3
% 2.52/0.63 % (2874013)Termination reason: Refutation
% 2.52/0.63 % (2874013)Time elapsed: 0.298 s
% 2.52/0.63 % (2874013)Peak memory usage: 15 MB
% 2.52/0.63 % (2874013)Instructions burned: 488 (million)
% 2.52/0.63 % (2873978)Success in time 0.405 s
% 2.52/0.63 % Vampire exiting
%------------------------------------------------------------------------------