%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO066^4.002 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n015.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:48:52 AM UTC 2026
% Result : Theorem 2.69s 0.67s
% Output : Refutation 2.69s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO066^4.002 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n015.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Tue Sep 29 16:31:27 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.23 Running first-order model finding
% 0.08/0.23 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.69/0.67 % (3744438)Will run a generic schedule for satisfiability detection.
% 2.69/0.67 % (3744444)% WARNING: option uhcvi not known.
% 2.69/0.67 % (3744444)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1438061797:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 2.69/0.67 % (3744444)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.69/0.67 % (3744444)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 2.69/0.67 % (3744443)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=485082063_2999 on theBenchmark for (2999ds/0Mi)
% 2.69/0.67 % Exception at run slice level
% 2.69/0.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.69/0.67 % (3744448)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3473714324:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 2.69/0.67 % (3744449)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3425357475:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 2.69/0.67 % (3744445)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3957760533:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 2.69/0.67 % (3744446)dis+10_1_sil=32000:sp=arity:random_seed=1699467265:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 2.69/0.67 % (3744452)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2650015962:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 2.69/0.67 % (3744447)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4278038244:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 2.69/0.67 % (3744447)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.69/0.67 % Exception at run slice level
% 2.69/0.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.69/0.67 % (3744459)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3412226455:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 2.69/0.67 % (3744448)Instruction limit reached!
% 2.69/0.67 % (3744448)------------------------------
% 2.69/0.67 % (3744448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.67 % (3744448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.67 % (3744448)CaDiCaL version: 2.1.3
% 2.69/0.67 % (3744448)Termination reason: Instruction limit
% 2.69/0.67 % (3744448)Termination phase: Saturation
% 2.69/0.67 % (3744448)Time elapsed: 0.062 s
% 2.69/0.67 % (3744448)Peak memory usage: 12 MB
% 2.69/0.67 % (3744448)Instructions burned: 131 (million)
% 2.69/0.67 % (3744446)Instruction limit reached!
% 2.69/0.67 % (3744446)------------------------------
% 2.69/0.67 % (3744446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.67 % (3744446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.67 % (3744446)CaDiCaL version: 2.1.3
% 2.69/0.67 % (3744446)Termination reason: Instruction limit
% 2.69/0.67 % (3744446)Termination phase: Saturation
% 2.69/0.67 % (3744446)Time elapsed: 0.063 s
% 2.69/0.67 % (3744446)Peak memory usage: 12 MB
% 2.69/0.67 % (3744446)Instructions burned: 104 (million)
% 2.69/0.67 % (3744449)Instruction limit reached!
% 2.69/0.67 % (3744449)------------------------------
% 2.69/0.67 % (3744449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.67 % (3744449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.67 % (3744449)CaDiCaL version: 2.1.3
% 2.69/0.67 % (3744449)Termination reason: Instruction limit
% 2.69/0.67 % (3744449)Termination phase: Saturation
% 2.69/0.67 % (3744449)Time elapsed: 0.072 s
% 2.69/0.67 % (3744449)Peak memory usage: 12 MB
% 2.69/0.67 % (3744449)Instructions burned: 159 (million)
% 2.69/0.67 % (3744447)Instruction limit reached!
% 2.69/0.67 % (3744447)------------------------------
% 2.69/0.67 % (3744447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.67 % (3744447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.67 % (3744447)CaDiCaL version: 2.1.3
% 2.69/0.67 % (3744447)Termination reason: Instruction limit
% 2.69/0.67 % (3744447)Termination phase: Saturation
% 2.69/0.67 % (3744447)Time elapsed: 0.062 s
% 2.69/0.67 % (3744447)Peak memory usage: 12 MB
% 2.69/0.67 % (3744447)Instructions burned: 116 (million)
% 2.69/0.67 % (3744461)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=2328077988:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 2.69/0.67 % (3744461)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.69/0.67 % (3744461)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 2.69/0.67 % (3744462)ott-21_1_sil=16000:fs=off:random_seed=2771616999:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 2.69/0.67 % (3744463)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1350602283:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 2.69/0.67 % (3744464)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1663494695:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 2.69/0.67 % Exception at run slice level
% 2.69/0.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.69/0.67 % (3744469)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=466826618:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 2.69/0.67 % (3744459)Instruction limit reached!
% 2.69/0.67 % (3744459)------------------------------
% 2.69/0.67 % (3744459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.67 % (3744459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.67 % (3744459)CaDiCaL version: 2.1.3
% 2.69/0.67 % (3744459)Termination reason: Instruction limit
% 2.69/0.67 % (3744459)Termination phase: Saturation
% 2.69/0.67 % (3744459)Time elapsed: 0.096 s
% 2.69/0.67 % (3744459)Peak memory usage: 12 MB
% 2.69/0.67 % (3744459)Instructions burned: 133 (million)
% 2.69/0.67 % (3744471)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2128549643:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 2.69/0.67 % Exception at run slice level
% 2.69/0.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.69/0.67 % (3744473)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=3385772803: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.69/0.67 % (3744473)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.69/0.67 % (3744462)Instruction limit reached!
% 2.69/0.67 % (3744462)------------------------------
% 2.69/0.67 % (3744462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.67 % (3744462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.67 % (3744462)CaDiCaL version: 2.1.3
% 2.69/0.67 % (3744462)Termination reason: Instruction limit
% 2.69/0.67 % (3744462)Termination phase: Saturation
% 2.69/0.67 % (3744462)Time elapsed: 0.087 s
% 2.69/0.67 % (3744462)Peak memory usage: 12 MB
% 2.69/0.67 % (3744462)Instructions burned: 182 (million)
% 2.69/0.67 % (3744475)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4182896187:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 2.69/0.67 % (3744475)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.69/0.67 % (3744463)Instruction limit reached!
% 2.69/0.67 % (3744463)------------------------------
% 2.69/0.67 % (3744463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.67 % (3744463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.67 % (3744463)CaDiCaL version: 2.1.3
% 2.69/0.67 % (3744463)Termination reason: Instruction limit
% 2.69/0.67 % (3744463)Termination phase: Saturation
% 2.69/0.67 % (3744463)Time elapsed: 0.242 s
% 2.69/0.67 % (3744463)Peak memory usage: 13 MB
% 2.69/0.67 % (3744463)Instructions burned: 480 (million)
% 2.69/0.67 % (3744477)fmb+10_1_sil=64000:random_seed=1627860021:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 2.69/0.67 % (3744477)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 2.69/0.67 % Exception at run slice level
% 2.69/0.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.69/0.67 % (3744461) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3744438-3744461"...
% 2.69/0.67 % (3744479)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=463216708:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 2.69/0.67 % Exception at run slice level
% 2.69/0.67 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.69/0.67 % (3744461)...printing done.
% 2.69/0.67 % (3744461)Refutation found. Thanks to Tanya!
% 2.69/0.67 % SZS status Theorem for theBenchmark
% 2.69/0.67 % SZS output start Proof for theBenchmark
% 2.69/0.67 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 2.69/0.67 thf(func_def_0, type, irel: ($i > $i > $o)).
% 2.69/0.67 thf(func_def_2, type, mnot: (($i > $o) > $i > $o)).
% 2.69/0.67 thf(func_def_3, type, mor: (($i > $o) > ($i > $o) > $i > $o)).
% 2.69/0.67 thf(func_def_4, type, mand: (($i > $o) > ($i > $o) > $i > $o)).
% 2.69/0.67 thf(func_def_5, type, mimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 2.69/0.67 thf(func_def_6, type, mbox_s4: (($i > $o) > $i > $o)).
% 2.69/0.67 thf(func_def_7, type, iatom: (($i > $o) > $i > $o)).
% 2.69/0.67 thf(func_def_8, type, inot: (($i > $o) > $i > $o)).
% 2.69/0.67 thf(func_def_9, type, itrue: ($i > $o)).
% 2.69/0.67 thf(func_def_10, type, ifalse: ($i > $o)).
% 2.69/0.67 thf(func_def_11, type, iand: (($i > $o) > ($i > $o) > $i > $o)).
% 2.69/0.67 thf(func_def_12, type, ior: (($i > $o) > ($i > $o) > $i > $o)).
% 2.69/0.67 thf(func_def_13, type, iimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 2.69/0.67 thf(func_def_14, type, iimplied: (($i > $o) > ($i > $o) > $i > $o)).
% 2.69/0.67 thf(func_def_15, type, iequiv: (($i > $o) > ($i > $o) > $i > $o)).
% 2.69/0.67 thf(func_def_16, type, ixor: (($i > $o) > ($i > $o) > $i > $o)).
% 2.69/0.67 thf(func_def_17, type, ivalid: (($i > $o) > $o)).
% 2.69/0.67 thf(func_def_18, type, isatisfiable: (($i > $o) > $o)).
% 2.69/0.67 thf(func_def_19, type, icountersatisfiable: (($i > $o) > $o)).
% 2.69/0.67 thf(func_def_20, type, iinvalid: (($i > $o) > $o)).
% 2.69/0.67 thf(func_def_21, type, o11: ($i > $o)).
% 2.69/0.67 thf(func_def_22, type, o12: ($i > $o)).
% 2.69/0.67 thf(func_def_23, type, o21: ($i > $o)).
% 2.69/0.67 thf(func_def_24, type, o22: ($i > $o)).
% 2.69/0.67 thf(func_def_25, type, o31: ($i > $o)).
% 2.69/0.67 thf(func_def_26, type, o32: ($i > $o)).
% 2.69/0.67 thf(func_def_29, type, vNOT: ($o > $o)).
% 2.69/0.67 thf(func_def_30, type, db1: !>[X0: $tType]:(X0)).
% 2.69/0.67 thf(func_def_31, type, db0: !>[X0: $tType]:(X0)).
% 2.69/0.67 thf(func_def_32, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 2.69/0.67 thf(func_def_33, type, vOR: ($o > $o > $o)).
% 2.69/0.67 thf(func_def_34, type, db2: !>[X0: $tType]:(X0)).
% 2.69/0.67 thf(func_def_35, type, vAND: ($o > $o > $o)).
% 2.69/0.67 thf(func_def_36, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 2.69/0.67 thf(func_def_37, type, vIMP: ($o > $o > $o)).
% 2.69/0.67 thf(func_def_38, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 2.69/0.67 thf(f1,axiom,(
% 2.69/0.67 ! [X0 : $i] : (irel @ X0 @ X0)),
% 2.69/0.67 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',refl_axiom)).
% 2.69/0.67 thf(f2,axiom,(
% 2.69/0.67 ! [X0 : $i,X1 : $i,X2 : $i] : (((irel @ X1 @ X2) & (irel @ X0 @ X1)) => (irel @ X0 @ X2))),
% 2.69/0.67 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',trans_axiom)).
% 2.69/0.67 thf(f4,axiom,(
% 2.69/0.67 (mor = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X1 @ X2) | (X0 @ X2))))),
% 2.69/0.67 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',mor)).
% 2.69/0.67 thf(f5,axiom,(
% 2.69/0.67 (mand = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X1 @ X2) & (X0 @ X2))))),
% 2.69/0.67 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',mand)).
% 2.69/0.67 thf(f7,axiom,(
% 2.69/0.67 (mbox_s4 = (^[X0 : ($i > $o), X1 : $i] : (! [X2 : $i] : ((irel @ X1 @ X2) => (X0 @ X2)))))),
% 2.69/0.67 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',mbox_s4)).
% 2.69/0.67 thf(f8,axiom,(
% 2.69/0.67 (iatom = (^[X0 : ($i > $o)] : (X0)))),
% 2.69/0.67 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',iatom)).
% 2.69/0.67 thf(f12,axiom,(
% 2.69/0.67 (iand = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mand @ X0 @ X1))))),
% 2.69/0.67 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',iand)).
% 2.69/0.67 thf(f13,axiom,(
% 2.69/0.67 (ior = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mor @ (mbox_s4 @ X0) @ (mbox_s4 @ X1)))))),
% 2.69/0.67 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',ior)).
% 2.69/0.67 thf(f18,axiom,(
% 2.69/0.67 (ivalid = (^[X0 : ($i > $o)] : (! [X1 : $i] : (X0 @ X1))))),
% 2.69/0.67 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',ivalid)).
% 2.69/0.67 thf(f22,axiom,(
% 2.69/0.67 (ivalid @ (ior @ (iatom @ o11) @ (iatom @ o12)))),
% 2.69/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom1)).
% 2.69/0.67 thf(f23,axiom,(
% 2.69/0.67 (ivalid @ (ior @ (iatom @ o21) @ (iatom @ o22)))),
% 2.69/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom2)).
% 2.69/0.67 thf(f24,axiom,(
% 2.69/0.67 (ivalid @ (ior @ (iatom @ o31) @ (iatom @ o32)))),
% 2.69/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom3)).
% 2.69/0.67 thf(f25,conjecture,(
% 2.69/0.67 (ivalid @ (ior @ (iand @ (iatom @ o11) @ (iatom @ o21)) @ (ior @ (iand @ (iatom @ o11) @ (iatom @ o31)) @ (ior @ (iand @ (iatom @ o21) @ (iatom @ o31)) @ (ior @ (iand @ (iatom @ o12) @ (iatom @ o22)) @ (ior @ (iand @ (iatom @ o12) @ (iatom @ o32)) @ (iand @ (iatom @ o22) @ (iatom @ o32))))))))),
% 2.69/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p',con)).
% 2.69/0.67 thf(f26,negated_conjecture,(
% 2.69/0.67 ~(ivalid @ (ior @ (iand @ (iatom @ o11) @ (iatom @ o21)) @ (ior @ (iand @ (iatom @ o11) @ (iatom @ o31)) @ (ior @ (iand @ (iatom @ o21) @ (iatom @ o31)) @ (ior @ (iand @ (iatom @ o12) @ (iatom @ o22)) @ (ior @ (iand @ (iatom @ o12) @ (iatom @ o32)) @ (iand @ (iatom @ o22) @ (iatom @ o32))))))))),
% 2.69/0.67 inference(negated_conjecture,[status(cth)],[f25])).
% 2.69/0.67 thf(f27,plain,(
% 2.69/0.67 ! [X0 : $i] : (irel @ X0 @ X0)),
% 2.69/0.67 inference(rectify,[],[f1])).
% 2.69/0.67 thf(f28,plain,(
% 2.69/0.67 ! [X0 : $i] : (((irel @ X0 @ X0)) = $true)),
% 2.69/0.67 inference(fool_elimination,[],[f27])).
% 2.69/0.67 thf(f29,plain,(
% 2.69/0.67 ! [X0 : $i,X1 : $i,X2 : $i] : (((irel @ X1 @ X2) & (irel @ X0 @ X1)) => (irel @ X0 @ X2))),
% 2.69/0.67 inference(rectify,[],[f2])).
% 2.69/0.67 thf(f30,plain,(
% 2.69/0.67 ! [X0 : $i,X1 : $i,X2 : $i] : (((((irel @ X1 @ X2)) = $true) & (((irel @ X0 @ X1)) = $true)) => (((irel @ X0 @ X2)) = $true))),
% 2.69/0.67 inference(fool_elimination,[],[f29])).
% 2.69/0.67 thf(f33,plain,(
% 2.69/0.67 (mor = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X1 @ X2) | (X0 @ X2))))),
% 2.69/0.67 inference(rectify,[],[f4])).
% 2.69/0.67 thf(f34,plain,(
% 2.69/0.67 (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))))),
% 2.69/0.67 inference(fool_elimination,[],[f33])).
% 2.69/0.67 thf(f35,plain,(
% 2.69/0.67 (mand = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X1 @ X2) & (X0 @ X2))))),
% 2.69/0.67 inference(rectify,[],[f5])).
% 2.69/0.67 thf(f36,plain,(
% 2.69/0.67 (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2))))))))),
% 2.69/0.67 inference(fool_elimination,[],[f35])).
% 2.69/0.67 thf(f38,plain,(
% 2.69/0.67 (mbox_s4 = (^[X0 : ($i > $o), X1 : $i] : (! [X2 : $i] : ((irel @ X1 @ X2) => (X0 @ X2)))))),
% 2.69/0.67 inference(rectify,[],[f7])).
% 2.69/0.67 thf(f39,plain,(
% 2.69/0.67 (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (Y0 @ Y2))))))))),
% 2.69/0.67 inference(fool_elimination,[],[f38])).
% 2.69/0.67 thf(f40,plain,(
% 2.69/0.67 (iatom = (^[Y0 : $i > $o]: (Y0)))),
% 2.69/0.67 inference(fool_elimination,[],[f8])).
% 2.69/0.67 thf(f43,plain,(
% 2.69/0.67 (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mand @ Y0 @ Y1)))))),
% 2.69/0.67 inference(fool_elimination,[],[f12])).
% 2.69/0.67 thf(f44,plain,(
% 2.69/0.67 (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 2.69/0.67 inference(fool_elimination,[],[f13])).
% 2.69/0.67 thf(f49,plain,(
% 2.69/0.67 (ivalid = (^[X0 : ($i > $o)] : (! [X1 : $i] : (X0 @ X1))))),
% 2.69/0.67 inference(rectify,[],[f18])).
% 2.69/0.67 thf(f50,plain,(
% 2.69/0.67 (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))),
% 2.69/0.67 inference(fool_elimination,[],[f49])).
% 2.69/0.67 thf(f57,plain,(
% 2.69/0.67 (ivalid @ (ior @ (iatom @ o11) @ (iatom @ o12)))),
% 2.69/0.67 inference(rectify,[],[f22])).
% 2.69/0.67 thf(f58,plain,(
% 2.69/0.67 (((ivalid @ (ior @ (iatom @ o11) @ (iatom @ o12)))) = $true)),
% 2.69/0.67 inference(fool_elimination,[],[f57])).
% 2.69/0.67 thf(f59,plain,(
% 2.69/0.67 (ivalid @ (ior @ (iatom @ o21) @ (iatom @ o22)))),
% 2.69/0.67 inference(rectify,[],[f23])).
% 2.69/0.67 thf(f60,plain,(
% 2.69/0.67 (((ivalid @ (ior @ (iatom @ o21) @ (iatom @ o22)))) = $true)),
% 2.69/0.67 inference(fool_elimination,[],[f59])).
% 2.69/0.67 thf(f61,plain,(
% 2.69/0.67 (ivalid @ (ior @ (iatom @ o31) @ (iatom @ o32)))),
% 2.69/0.67 inference(rectify,[],[f24])).
% 2.69/0.67 thf(f62,plain,(
% 2.69/0.67 (((ivalid @ (ior @ (iatom @ o31) @ (iatom @ o32)))) = $true)),
% 2.69/0.67 inference(fool_elimination,[],[f61])).
% 2.69/0.67 thf(f63,plain,(
% 2.69/0.67 ~(ivalid @ (ior @ (iand @ (iatom @ o11) @ (iatom @ o21)) @ (ior @ (iand @ (iatom @ o11) @ (iatom @ o31)) @ (ior @ (iand @ (iatom @ o21) @ (iatom @ o31)) @ (ior @ (iand @ (iatom @ o12) @ (iatom @ o22)) @ (ior @ (iand @ (iatom @ o12) @ (iatom @ o32)) @ (iand @ (iatom @ o22) @ (iatom @ o32))))))))),
% 2.69/0.67 inference(rectify,[],[f26])).
% 2.69/0.67 thf(f64,plain,(
% 2.69/0.67 ~ (((ivalid @ (ior @ (iand @ (iatom @ o11) @ (iatom @ o21)) @ (ior @ (iand @ (iatom @ o11) @ (iatom @ o31)) @ (ior @ (iand @ (iatom @ o21) @ (iatom @ o31)) @ (ior @ (iand @ (iatom @ o12) @ (iatom @ o22)) @ (ior @ (iand @ (iatom @ o12) @ (iatom @ o32)) @ (iand @ (iatom @ o22) @ (iatom @ o32))))))))) = $true)),
% 2.69/0.67 inference(fool_elimination,[],[f63])).
% 2.69/0.67 thf(f65,plain,(
% 2.69/0.67 (((ivalid @ (ior @ (iand @ (iatom @ o11) @ (iatom @ o21)) @ (ior @ (iand @ (iatom @ o11) @ (iatom @ o31)) @ (ior @ (iand @ (iatom @ o21) @ (iatom @ o31)) @ (ior @ (iand @ (iatom @ o12) @ (iatom @ o22)) @ (ior @ (iand @ (iatom @ o12) @ (iatom @ o32)) @ (iand @ (iatom @ o22) @ (iatom @ o32))))))))) != $true)),
% 2.69/0.67 inference(flattening,[],[f64])).
% 2.69/0.67 thf(f66,plain,(
% 2.69/0.67 ! [X0 : $i,X1 : $i,X2 : $i] : ((((irel @ X0 @ X2)) = $true) | ((((irel @ X1 @ X2)) != $true) | (((irel @ X0 @ X1)) != $true)))),
% 2.69/0.67 inference(ennf_transformation,[],[f30])).
% 2.69/0.67 thf(f67,plain,(
% 2.69/0.67 ! [X0 : $i,X1 : $i,X2 : $i] : ((((irel @ X0 @ X2)) = $true) | (((irel @ X1 @ X2)) != $true) | (((irel @ X0 @ X1)) != $true))),
% 2.69/0.67 inference(flattening,[],[f66])).
% 2.69/0.67 thf(f68,plain,(
% 2.69/0.67 ( ! [X0 : $i] : ((((irel @ X0 @ X0)) = $true)) )),
% 2.69/0.67 inference(cnf_transformation,[],[f28])).
% 2.69/0.67 thf(f69,plain,(
% 2.69/0.67 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((irel @ X1 @ X2)) != $true) | (((irel @ X0 @ X2)) = $true) | (((irel @ X0 @ X1)) != $true)) )),
% 2.69/0.67 inference(cnf_transformation,[],[f67])).
% 2.69/0.67 thf(f71,plain,(
% 2.69/0.67 (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))))),
% 2.69/0.67 inference(cnf_transformation,[],[f34])).
% 2.69/0.67 thf(f72,plain,(
% 2.69/0.67 (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2))))))))),
% 2.69/0.67 inference(cnf_transformation,[],[f36])).
% 2.69/0.67 thf(f74,plain,(
% 2.69/0.67 (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (Y0 @ Y2))))))))),
% 2.69/0.67 inference(cnf_transformation,[],[f39])).
% 2.69/0.67 thf(f75,plain,(
% 2.69/0.67 (iatom = (^[Y0 : $i > $o]: (Y0)))),
% 2.69/0.67 inference(cnf_transformation,[],[f40])).
% 2.69/0.67 thf(f79,plain,(
% 2.69/0.67 (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mand @ Y0 @ Y1)))))),
% 2.69/0.67 inference(cnf_transformation,[],[f43])).
% 2.69/0.67 thf(f80,plain,(
% 2.69/0.67 (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 2.69/0.67 inference(cnf_transformation,[],[f44])).
% 2.69/0.67 thf(f85,plain,(
% 2.69/0.67 (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))),
% 2.69/0.67 inference(cnf_transformation,[],[f50])).
% 2.69/0.67 thf(f89,plain,(
% 2.69/0.67 (((ivalid @ (ior @ (iatom @ o11) @ (iatom @ o12)))) = $true)),
% 2.69/0.67 inference(cnf_transformation,[],[f58])).
% 2.69/0.67 thf(f90,plain,(
% 2.69/0.67 (((ivalid @ (ior @ (iatom @ o21) @ (iatom @ o22)))) = $true)),
% 2.69/0.67 inference(cnf_transformation,[],[f60])).
% 2.69/0.67 thf(f91,plain,(
% 2.69/0.67 (((ivalid @ (ior @ (iatom @ o31) @ (iatom @ o32)))) = $true)),
% 2.69/0.67 inference(cnf_transformation,[],[f62])).
% 2.69/0.67 thf(f92,plain,(
% 2.69/0.67 (((ivalid @ (ior @ (iand @ (iatom @ o11) @ (iatom @ o21)) @ (ior @ (iand @ (iatom @ o11) @ (iatom @ o31)) @ (ior @ (iand @ (iatom @ o21) @ (iatom @ o31)) @ (ior @ (iand @ (iatom @ o12) @ (iatom @ o22)) @ (ior @ (iand @ (iatom @ o12) @ (iatom @ o32)) @ (iand @ (iatom @ o22) @ (iatom @ o32))))))))) != $true)),
% 2.69/0.67 inference(cnf_transformation,[],[f65])).
% 2.69/0.67 thf(f94,definition,(
% 2.69/0.67 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 2.69/0.67 introduced(theory,[fool_exhaustiveness_axiom])).
% 2.69/0.67 thf(f98,plain,(
% 2.69/0.67 (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) & (Y3 @ Y4))))))) @ Y0 @ Y1)))))),
% 2.69/0.67 inference(definition_unfolding,[],[f79,f72])).
% 2.69/0.67 thf(f99,plain,(
% 2.69/0.67 (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))))),
% 2.69/0.67 inference(definition_unfolding,[],[f80,f71,f74,f74])).
% 2.69/0.67 thf(f104,plain,(
% 2.69/0.67 ($true = (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))) @ ((^[Y0 : $i > $o]: (Y0)) @ o11) @ ((^[Y0 : $i > $o]: (Y0)) @ o12)))))),
% 2.69/0.67 inference(definition_unfolding,[],[f89,f85,f99,f75,f75])).
% 2.69/0.67 thf(f105,plain,(
% 2.69/0.67 ($true = (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))) @ ((^[Y0 : $i > $o]: (Y0)) @ o21) @ ((^[Y0 : $i > $o]: (Y0)) @ o22)))))),
% 2.69/0.67 inference(definition_unfolding,[],[f90,f85,f99,f75,f75])).
% 2.69/0.67 thf(f106,plain,(
% 2.69/0.67 ($true = (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))) @ ((^[Y0 : $i > $o]: (Y0)) @ o31) @ ((^[Y0 : $i > $o]: (Y0)) @ o32)))))),
% 2.69/0.67 inference(definition_unfolding,[],[f91,f85,f99,f75,f75])).
% 2.69/0.67 thf(f107,plain,(
% 2.69/0.67 ($true != (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) & (Y3 @ Y4))))))) @ Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: (Y0)) @ o11) @ ((^[Y0 : $i > $o]: (Y0)) @ o21)) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) & (Y3 @ Y4))))))) @ Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: (Y0)) @ o11) @ ((^[Y0 : $i > $o]: (Y0)) @ o31)) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) & (Y3 @ Y4))))))) @ Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: (Y0)) @ o21) @ ((^[Y0 : $i > $o]: (Y0)) @ o31)) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) & (Y3 @ Y4))))))) @ Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: (Y0)) @ o12) @ ((^[Y0 : $i > $o]: (Y0)) @ o22)) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y0) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => (Y2 @ Y4))))))) @ Y1))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) & (Y3 @ Y4))))))) @ Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: (Y0)) @ o12) @ ((^[Y0 : $i > $o]: (Y0)) @ o32)) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) & (Y3 @ Y4))))))) @ Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: (Y0)) @ o22) @ ((^[Y0 : $i > $o]: (Y0)) @ o32))))))))))),
% 2.69/0.67 inference(definition_unfolding,[],[f92,f85,f99,f98,f75,f75,f99,f98,f75,f75,f99,f98,f75,f75,f99,f98,f75,f75,f99,f98,f75,f75,f98,f75,f75])).
% 2.69/0.67 thf(f108,plain,(
% 2.69/0.67 ($true != ((!! @ $i @ (^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((o11 @ Y1) & (o21 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((o11 @ Y2) & (o31 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => ((o21 @ Y3) & (o31 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => ((!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => ((o12 @ Y4) & (o22 @ Y4))))) | (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => ((!! @ $i @ (^[Y5 : $i]: ((irel @ Y4 @ Y5) => ((o12 @ Y5) & (o32 @ Y5))))) | (!! @ $i @ (^[Y5 : $i]: ((irel @ Y4 @ Y5) => ((o22 @ Y5) & (o32 @ Y5))))))))))))))))))))))))))),
% 2.69/0.67 inference(beta-eta_normalization,[],[f107])).
% 2.69/0.67 thf(f109,plain,(
% 2.69/0.67 ($false = (((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((o11 @ Y1) & (o21 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((o11 @ Y2) & (o31 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => ((o21 @ Y3) & (o31 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => ((!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => ((o12 @ Y4) & (o22 @ Y4))))) | (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => ((!! @ $i @ (^[Y5 : $i]: ((irel @ Y4 @ Y5) => ((o12 @ Y5) & (o32 @ Y5))))) | (!! @ $i @ (^[Y5 : $i]: ((irel @ Y4 @ Y5) => ((o22 @ Y5) & (o32 @ Y5))))))))))))))))))))))) @ sK0)))),
% 2.69/0.67 inference(sigma_proxy_clausification,[],[f108])).
% 2.69/0.67 thf(f110,plain,(
% 2.69/0.67 ($false = (((!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => ((o11 @ Y0) & (o21 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((o11 @ Y1) & (o31 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((o21 @ Y2) & (o31 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => ((o12 @ Y3) & (o22 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => ((!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => ((o12 @ Y4) & (o32 @ Y4))))) | (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => ((o22 @ Y4) & (o32 @ Y4))))))))))))))))))))))))),
% 2.69/0.67 inference(beta-eta_normalization,[],[f109])).
% 2.69/0.67 thf(f111,plain,(
% 2.69/0.67 ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((o11 @ Y1) & (o31 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((o21 @ Y2) & (o31 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => ((o12 @ Y3) & (o22 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => ((!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => ((o12 @ Y4) & (o32 @ Y4))))) | (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => ((o22 @ Y4) & (o32 @ Y4)))))))))))))))))))))))),
% 2.69/0.67 inference(or_proxy_clausification,[],[f110])).
% 2.69/0.67 thf(f112,plain,(
% 2.69/0.67 ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => ((o11 @ Y0) & (o21 @ Y0)))))))),
% 2.69/0.67 inference(or_proxy_clausification,[],[f110])).
% 2.69/0.67 thf(f113,plain,(
% 2.69/0.67 ($false = (((^[Y0 : $i]: ((irel @ sK0 @ Y0) => ((o11 @ Y0) & (o21 @ Y0)))) @ sK1)))),
% 2.69/0.67 inference(sigma_proxy_clausification,[],[f112])).
% 2.69/0.67 thf(f114,plain,(
% 2.69/0.67 ($false = (((irel @ sK0 @ sK1) => ((o11 @ sK1) & (o21 @ sK1)))))),
% 2.69/0.67 inference(beta-eta_normalization,[],[f113])).
% 2.69/0.67 thf(f115,plain,(
% 2.69/0.67 ($false = (((o11 @ sK1) & (o21 @ sK1))))),
% 2.69/0.67 inference(imp_proxy_clausification,[],[f114])).
% 2.69/0.67 thf(f116,plain,(
% 2.69/0.67 ($true = ((irel @ sK0 @ sK1)))),
% 2.69/0.67 inference(imp_proxy_clausification,[],[f114])).
% 2.69/0.67 thf(f117,plain,(
% 2.69/0.67 ($false = ((o21 @ sK1))) | ($false = ((o11 @ sK1)))),
% 2.69/0.67 inference(and_proxy_clausification,[],[f115])).
% 2.69/0.67 thf(f118,plain,(
% 2.69/0.67 ($false = (((^[Y0 : $i]: ((irel @ sK0 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((o11 @ Y1) & (o31 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((o21 @ Y2) & (o31 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => ((o12 @ Y3) & (o22 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => ((!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => ((o12 @ Y4) & (o32 @ Y4))))) | (!! @ $i @ (^[Y4 : $i]: ((irel @ Y3 @ Y4) => ((o22 @ Y4) & (o32 @ Y4)))))))))))))))))))) @ sK2)))),
% 2.69/0.67 inference(sigma_proxy_clausification,[],[f111])).
% 2.69/0.67 thf(f119,plain,(
% 2.69/0.67 ($false = (((irel @ sK0 @ sK2) => ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK2 @ Y0) => ((o11 @ Y0) & (o31 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ sK2 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((o21 @ Y1) & (o31 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((o12 @ Y2) & (o22 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => ((o12 @ Y3) & (o32 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => ((o22 @ Y3) & (o32 @ Y3)))))))))))))))))))))),
% 2.69/0.67 inference(beta-eta_normalization,[],[f118])).
% 2.69/0.67 thf(f120,plain,(
% 2.69/0.67 ($false = (((!! @ $i @ (^[Y0 : $i]: ((irel @ sK2 @ Y0) => ((o11 @ Y0) & (o31 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ sK2 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((o21 @ Y1) & (o31 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((o12 @ Y2) & (o22 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => ((o12 @ Y3) & (o32 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => ((o22 @ Y3) & (o32 @ Y3))))))))))))))))))))),
% 2.69/0.67 inference(imp_proxy_clausification,[],[f119])).
% 2.69/0.67 thf(f121,plain,(
% 2.69/0.67 ($true = ((irel @ sK0 @ sK2)))),
% 2.69/0.67 inference(imp_proxy_clausification,[],[f119])).
% 2.69/0.67 thf(f122,plain,(
% 2.69/0.67 ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK2 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((o21 @ Y1) & (o31 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((o12 @ Y2) & (o22 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => ((o12 @ Y3) & (o32 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => ((o22 @ Y3) & (o32 @ Y3)))))))))))))))))))),
% 2.69/0.67 inference(or_proxy_clausification,[],[f120])).
% 2.69/0.67 thf(f123,plain,(
% 2.69/0.67 ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK2 @ Y0) => ((o11 @ Y0) & (o31 @ Y0)))))))),
% 2.69/0.67 inference(or_proxy_clausification,[],[f120])).
% 2.69/0.67 thf(f124,plain,(
% 2.69/0.67 ($false = (((^[Y0 : $i]: ((irel @ sK2 @ Y0) => ((o11 @ Y0) & (o31 @ Y0)))) @ sK3)))),
% 2.69/0.67 inference(sigma_proxy_clausification,[],[f123])).
% 2.69/0.67 thf(f125,plain,(
% 2.69/0.67 ($false = (((irel @ sK2 @ sK3) => ((o11 @ sK3) & (o31 @ sK3)))))),
% 2.69/0.67 inference(beta-eta_normalization,[],[f124])).
% 2.69/0.67 thf(f126,plain,(
% 2.69/0.67 ($false = (((o11 @ sK3) & (o31 @ sK3))))),
% 2.69/0.67 inference(imp_proxy_clausification,[],[f125])).
% 2.69/0.67 thf(f127,plain,(
% 2.69/0.67 ($true = ((irel @ sK2 @ sK3)))),
% 2.69/0.67 inference(imp_proxy_clausification,[],[f125])).
% 2.69/0.67 thf(f128,plain,(
% 2.69/0.67 ($false = ((o31 @ sK3))) | ($false = ((o11 @ sK3)))),
% 2.69/0.67 inference(and_proxy_clausification,[],[f126])).
% 2.69/0.68 thf(f129,plain,(
% 2.69/0.68 ($false = (((^[Y0 : $i]: ((irel @ sK2 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((o21 @ Y1) & (o31 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((o12 @ Y2) & (o22 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => ((o12 @ Y3) & (o32 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => ((o22 @ Y3) & (o32 @ Y3)))))))))))))))) @ sK4)))),
% 2.69/0.68 inference(sigma_proxy_clausification,[],[f122])).
% 2.69/0.68 thf(f130,plain,(
% 2.69/0.68 ($false = (((irel @ sK2 @ sK4) => ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK4 @ Y0) => ((o21 @ Y0) & (o31 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ sK4 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((o12 @ Y1) & (o22 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((o12 @ Y2) & (o32 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((o22 @ Y2) & (o32 @ Y2)))))))))))))))))),
% 2.69/0.68 inference(beta-eta_normalization,[],[f129])).
% 2.69/0.68 thf(f131,plain,(
% 2.69/0.68 ($false = (((!! @ $i @ (^[Y0 : $i]: ((irel @ sK4 @ Y0) => ((o21 @ Y0) & (o31 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ sK4 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((o12 @ Y1) & (o22 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((o12 @ Y2) & (o32 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((o22 @ Y2) & (o32 @ Y2))))))))))))))))),
% 2.69/0.68 inference(imp_proxy_clausification,[],[f130])).
% 2.69/0.68 thf(f132,plain,(
% 2.69/0.68 ($true = ((irel @ sK2 @ sK4)))),
% 2.69/0.68 inference(imp_proxy_clausification,[],[f130])).
% 2.69/0.68 thf(f133,plain,(
% 2.69/0.68 ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK4 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((o12 @ Y1) & (o22 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((o12 @ Y2) & (o32 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((o22 @ Y2) & (o32 @ Y2)))))))))))))))),
% 2.69/0.68 inference(or_proxy_clausification,[],[f131])).
% 2.69/0.68 thf(f134,plain,(
% 2.69/0.68 ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK4 @ Y0) => ((o21 @ Y0) & (o31 @ Y0)))))))),
% 2.69/0.68 inference(or_proxy_clausification,[],[f131])).
% 2.69/0.68 thf(f135,plain,(
% 2.69/0.68 ($false = (((^[Y0 : $i]: ((irel @ sK4 @ Y0) => ((o21 @ Y0) & (o31 @ Y0)))) @ sK5)))),
% 2.69/0.68 inference(sigma_proxy_clausification,[],[f134])).
% 2.69/0.68 thf(f136,plain,(
% 2.69/0.68 ($false = (((irel @ sK4 @ sK5) => ((o21 @ sK5) & (o31 @ sK5)))))),
% 2.69/0.68 inference(beta-eta_normalization,[],[f135])).
% 2.69/0.68 thf(f137,plain,(
% 2.69/0.68 ($false = (((o21 @ sK5) & (o31 @ sK5))))),
% 2.69/0.68 inference(imp_proxy_clausification,[],[f136])).
% 2.69/0.68 thf(f138,plain,(
% 2.69/0.68 ($true = ((irel @ sK4 @ sK5)))),
% 2.69/0.68 inference(imp_proxy_clausification,[],[f136])).
% 2.69/0.68 thf(f139,plain,(
% 2.69/0.68 ($false = ((o31 @ sK5))) | ($false = ((o21 @ sK5)))),
% 2.69/0.68 inference(and_proxy_clausification,[],[f137])).
% 2.69/0.68 thf(f140,plain,(
% 2.69/0.68 ($false = (((^[Y0 : $i]: ((irel @ sK4 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((o12 @ Y1) & (o22 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((o12 @ Y2) & (o32 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((o22 @ Y2) & (o32 @ Y2)))))))))))) @ sK6)))),
% 2.69/0.68 inference(sigma_proxy_clausification,[],[f133])).
% 2.69/0.68 thf(f141,plain,(
% 2.69/0.68 ($false = (((irel @ sK4 @ sK6) => ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK6 @ Y0) => ((o12 @ Y0) & (o22 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ sK6 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((o12 @ Y1) & (o32 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((o22 @ Y1) & (o32 @ Y1)))))))))))))),
% 2.69/0.68 inference(beta-eta_normalization,[],[f140])).
% 2.69/0.68 thf(f142,plain,(
% 2.69/0.68 ($false = (((!! @ $i @ (^[Y0 : $i]: ((irel @ sK6 @ Y0) => ((o12 @ Y0) & (o22 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ sK6 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((o12 @ Y1) & (o32 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((o22 @ Y1) & (o32 @ Y1))))))))))))),
% 2.69/0.68 inference(imp_proxy_clausification,[],[f141])).
% 2.69/0.68 thf(f143,plain,(
% 2.69/0.68 ($true = ((irel @ sK4 @ sK6)))),
% 2.69/0.68 inference(imp_proxy_clausification,[],[f141])).
% 2.69/0.68 thf(f144,plain,(
% 2.69/0.68 ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK6 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((o12 @ Y1) & (o32 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((o22 @ Y1) & (o32 @ Y1)))))))))))),
% 2.69/0.68 inference(or_proxy_clausification,[],[f142])).
% 2.69/0.68 thf(f145,plain,(
% 2.69/0.68 ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK6 @ Y0) => ((o12 @ Y0) & (o22 @ Y0)))))))),
% 2.69/0.68 inference(or_proxy_clausification,[],[f142])).
% 2.69/0.68 thf(f146,plain,(
% 2.69/0.68 ($false = (((^[Y0 : $i]: ((irel @ sK6 @ Y0) => ((o12 @ Y0) & (o22 @ Y0)))) @ sK7)))),
% 2.69/0.68 inference(sigma_proxy_clausification,[],[f145])).
% 2.69/0.68 thf(f147,plain,(
% 2.69/0.68 ($false = (((irel @ sK6 @ sK7) => ((o12 @ sK7) & (o22 @ sK7)))))),
% 2.69/0.68 inference(beta-eta_normalization,[],[f146])).
% 2.69/0.68 thf(f148,plain,(
% 2.69/0.68 ($false = (((o12 @ sK7) & (o22 @ sK7))))),
% 2.69/0.68 inference(imp_proxy_clausification,[],[f147])).
% 2.69/0.68 thf(f149,plain,(
% 2.69/0.68 ($true = ((irel @ sK6 @ sK7)))),
% 2.69/0.68 inference(imp_proxy_clausification,[],[f147])).
% 2.69/0.68 thf(f150,plain,(
% 2.69/0.68 ($false = ((o22 @ sK7))) | ($false = ((o12 @ sK7)))),
% 2.69/0.68 inference(and_proxy_clausification,[],[f148])).
% 2.69/0.68 thf(f151,plain,(
% 2.69/0.68 ($false = (((^[Y0 : $i]: ((irel @ sK6 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((o12 @ Y1) & (o32 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((o22 @ Y1) & (o32 @ Y1)))))))) @ sK8)))),
% 2.69/0.68 inference(sigma_proxy_clausification,[],[f144])).
% 2.69/0.68 thf(f152,plain,(
% 2.69/0.68 ($false = (((irel @ sK6 @ sK8) => ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK8 @ Y0) => ((o12 @ Y0) & (o32 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ sK8 @ Y0) => ((o22 @ Y0) & (o32 @ Y0)))))))))),
% 2.69/0.68 inference(beta-eta_normalization,[],[f151])).
% 2.69/0.68 thf(f153,plain,(
% 2.69/0.68 ($false = (((!! @ $i @ (^[Y0 : $i]: ((irel @ sK8 @ Y0) => ((o12 @ Y0) & (o32 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ sK8 @ Y0) => ((o22 @ Y0) & (o32 @ Y0))))))))),
% 2.69/0.68 inference(imp_proxy_clausification,[],[f152])).
% 2.69/0.68 thf(f154,plain,(
% 2.69/0.68 ($true = ((irel @ sK6 @ sK8)))),
% 2.69/0.68 inference(imp_proxy_clausification,[],[f152])).
% 2.69/0.68 thf(f155,plain,(
% 2.69/0.68 ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK8 @ Y0) => ((o22 @ Y0) & (o32 @ Y0)))))))),
% 2.69/0.68 inference(or_proxy_clausification,[],[f153])).
% 2.69/0.68 thf(f156,plain,(
% 2.69/0.68 ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK8 @ Y0) => ((o12 @ Y0) & (o32 @ Y0)))))))),
% 2.69/0.68 inference(or_proxy_clausification,[],[f153])).
% 2.69/0.68 thf(f157,plain,(
% 2.69/0.68 ($false = (((^[Y0 : $i]: ((irel @ sK8 @ Y0) => ((o12 @ Y0) & (o32 @ Y0)))) @ sK9)))),
% 2.69/0.68 inference(sigma_proxy_clausification,[],[f156])).
% 2.69/0.68 thf(f158,plain,(
% 2.69/0.68 ($false = (((irel @ sK8 @ sK9) => ((o12 @ sK9) & (o32 @ sK9)))))),
% 2.69/0.68 inference(beta-eta_normalization,[],[f157])).
% 2.69/0.68 thf(f159,plain,(
% 2.69/0.68 ($false = (((o12 @ sK9) & (o32 @ sK9))))),
% 2.69/0.68 inference(imp_proxy_clausification,[],[f158])).
% 2.69/0.68 thf(f160,plain,(
% 2.69/0.68 ($true = ((irel @ sK8 @ sK9)))),
% 2.69/0.68 inference(imp_proxy_clausification,[],[f158])).
% 2.69/0.68 thf(f161,plain,(
% 2.69/0.68 ($false = ((o32 @ sK9))) | ($false = ((o12 @ sK9)))),
% 2.69/0.68 inference(and_proxy_clausification,[],[f159])).
% 2.69/0.68 thf(f162,plain,(
% 2.69/0.68 ($false = (((^[Y0 : $i]: ((irel @ sK8 @ Y0) => ((o22 @ Y0) & (o32 @ Y0)))) @ sK10)))),
% 2.69/0.68 inference(sigma_proxy_clausification,[],[f155])).
% 2.69/0.68 thf(f163,plain,(
% 2.69/0.68 ($false = (((irel @ sK8 @ sK10) => ((o22 @ sK10) & (o32 @ sK10)))))),
% 2.69/0.68 inference(beta-eta_normalization,[],[f162])).
% 2.69/0.68 thf(f164,plain,(
% 2.69/0.68 ($false = (((o22 @ sK10) & (o32 @ sK10))))),
% 2.69/0.68 inference(imp_proxy_clausification,[],[f163])).
% 2.69/0.68 thf(f165,plain,(
% 2.69/0.68 ($true = ((irel @ sK8 @ sK10)))),
% 2.69/0.68 inference(imp_proxy_clausification,[],[f163])).
% 2.69/0.68 thf(f166,plain,(
% 2.69/0.68 ($false = ((o32 @ sK10))) | ($false = ((o22 @ sK10)))),
% 2.69/0.68 inference(and_proxy_clausification,[],[f164])).
% 2.69/0.68 thf(f167,plain,(
% 2.69/0.68 ($true = ((!! @ $i @ (^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (o31 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (o32 @ Y1)))))))))),
% 2.69/0.68 inference(beta-eta_normalization,[],[f106])).
% 2.69/0.68 thf(f168,plain,(
% 2.69/0.68 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (o31 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (o32 @ Y1)))))) @ X1)))) )),
% 2.69/0.68 inference(pi_proxy_clausification,[],[f167])).
% 2.69/0.68 thf(f169,plain,(
% 2.69/0.68 ( ! [X1 : $i] : (($true = (((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (o31 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (o32 @ Y0)))))))) )),
% 2.69/0.68 inference(beta-eta_normalization,[],[f168])).
% 2.69/0.68 thf(f170,plain,(
% 2.69/0.68 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (o32 @ Y0)))))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (o31 @ Y0))))))) )),
% 2.69/0.68 inference(or_proxy_clausification,[],[f169])).
% 2.69/0.68 thf(f171,plain,(
% 2.69/0.68 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (o32 @ Y0))) @ X2))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (o31 @ Y0))))))) )),
% 2.69/0.68 inference(pi_proxy_clausification,[],[f170])).
% 2.69/0.68 thf(f172,plain,(
% 2.69/0.68 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (o32 @ Y0))) @ X2))) | ($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (o31 @ Y0))) @ X3)))) )),
% 2.69/0.68 inference(pi_proxy_clausification,[],[f171])).
% 2.69/0.68 thf(f173,plain,(
% 2.69/0.68 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((irel @ X1 @ X2) => (o32 @ X2)))) | ($true = (((irel @ X1 @ X3) => (o31 @ X3))))) )),
% 2.69/0.68 inference(beta-eta_normalization,[],[f172])).
% 2.69/0.68 thf(f174,plain,(
% 2.69/0.68 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = (((irel @ X1 @ X3) => (o31 @ X3)))) | ($true = ((o32 @ X2)))) )),
% 2.69/0.68 inference(imp_proxy_clausification,[],[f173])).
% 2.69/0.68 thf(f175,plain,(
% 2.69/0.68 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ X1 @ X3))) | (((irel @ X1 @ X2)) = $false) | ($true = ((o32 @ X2))) | ($true = ((o31 @ X3)))) )),
% 2.69/0.68 inference(imp_proxy_clausification,[],[f174])).
% 2.69/0.68 thf(f176,plain,(
% 2.69/0.68 ($true = ((!! @ $i @ (^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (o21 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (o22 @ Y1)))))))))),
% 2.69/0.68 inference(beta-eta_normalization,[],[f105])).
% 2.69/0.68 thf(f177,plain,(
% 2.69/0.68 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (o21 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (o22 @ Y1)))))) @ X1)))) )),
% 2.69/0.68 inference(pi_proxy_clausification,[],[f176])).
% 2.69/0.68 thf(f178,plain,(
% 2.69/0.68 ( ! [X1 : $i] : (($true = (((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (o21 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (o22 @ Y0)))))))) )),
% 2.69/0.68 inference(beta-eta_normalization,[],[f177])).
% 2.69/0.68 thf(f179,plain,(
% 2.69/0.68 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (o22 @ Y0)))))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (o21 @ Y0))))))) )),
% 2.69/0.68 inference(or_proxy_clausification,[],[f178])).
% 2.69/0.68 thf(f180,plain,(
% 2.69/0.68 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (o22 @ Y0))) @ X2))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (o21 @ Y0))))))) )),
% 2.69/0.68 inference(pi_proxy_clausification,[],[f179])).
% 2.69/0.68 thf(f181,plain,(
% 2.69/0.68 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (o22 @ Y0))) @ X2))) | ($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (o21 @ Y0))) @ X3)))) )),
% 2.69/0.68 inference(pi_proxy_clausification,[],[f180])).
% 2.69/0.68 thf(f182,plain,(
% 2.69/0.68 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((irel @ X1 @ X2) => (o22 @ X2)))) | ($true = (((irel @ X1 @ X3) => (o21 @ X3))))) )),
% 2.69/0.68 inference(beta-eta_normalization,[],[f181])).
% 2.69/0.68 thf(f183,plain,(
% 2.69/0.68 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = (((irel @ X1 @ X3) => (o21 @ X3)))) | ($true = ((o22 @ X2)))) )),
% 2.69/0.68 inference(imp_proxy_clausification,[],[f182])).
% 2.69/0.68 thf(f184,plain,(
% 2.69/0.68 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ X1 @ X3))) | (((irel @ X1 @ X2)) = $false) | ($true = ((o22 @ X2))) | ($true = ((o21 @ X3)))) )),
% 2.69/0.68 inference(imp_proxy_clausification,[],[f183])).
% 2.69/0.68 thf(f185,plain,(
% 2.69/0.68 ($true = ((!! @ $i @ (^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (o11 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (o12 @ Y1)))))))))),
% 2.69/0.68 inference(beta-eta_normalization,[],[f104])).
% 2.69/0.68 thf(f186,plain,(
% 2.69/0.68 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (o11 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (o12 @ Y1)))))) @ X1)))) )),
% 2.69/0.68 inference(pi_proxy_clausification,[],[f185])).
% 2.69/0.68 thf(f187,plain,(
% 2.69/0.68 ( ! [X1 : $i] : (($true = (((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (o11 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (o12 @ Y0)))))))) )),
% 2.69/0.68 inference(beta-eta_normalization,[],[f186])).
% 2.69/0.68 thf(f188,plain,(
% 2.69/0.68 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (o12 @ Y0)))))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (o11 @ Y0))))))) )),
% 2.69/0.68 inference(or_proxy_clausification,[],[f187])).
% 2.69/0.68 thf(f189,plain,(
% 2.69/0.68 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (o12 @ Y0))) @ X2))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (o11 @ Y0))))))) )),
% 2.69/0.68 inference(pi_proxy_clausification,[],[f188])).
% 2.69/0.68 thf(f190,plain,(
% 2.69/0.68 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (o12 @ Y0))) @ X2))) | ($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (o11 @ Y0))) @ X3)))) )),
% 2.69/0.68 inference(pi_proxy_clausification,[],[f189])).
% 2.69/0.68 thf(f191,plain,(
% 2.69/0.68 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((irel @ X1 @ X2) => (o12 @ X2)))) | ($true = (((irel @ X1 @ X3) => (o11 @ X3))))) )),
% 2.69/0.68 inference(beta-eta_normalization,[],[f190])).
% 2.69/0.68 thf(f192,plain,(
% 2.69/0.68 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = (((irel @ X1 @ X3) => (o11 @ X3)))) | ($true = ((o12 @ X2)))) )),
% 2.69/0.68 inference(imp_proxy_clausification,[],[f191])).
% 2.69/0.68 thf(f193,plain,(
% 2.69/0.68 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ X1 @ X3))) | (((irel @ X1 @ X2)) = $false) | ($true = ((o12 @ X2))) | ($true = ((o11 @ X3)))) )),
% 2.69/0.68 inference(imp_proxy_clausification,[],[f192])).
% 2.69/0.68 thf(f195,definition,(
% 2.69/0.68 spl11_1 <=> ($false = ((o11 @ sK1)))),
% 2.69/0.68 introduced(definition,[new_symbols(definition,[spl11_1])],[avatar_definition])).
% 2.69/0.68 thf(f197,plain,(
% 2.69/0.68 ($false = ((o11 @ sK1))) | ~spl11_1),
% 2.69/0.68 inference(avatar_component_clause,[],[f195])).
% 2.69/0.68 thf(f199,definition,(
% 2.69/0.68 spl11_2 <=> ($false = ((o21 @ sK1)))),
% 2.69/0.68 introduced(definition,[new_symbols(definition,[spl11_2])],[avatar_definition])).
% 2.69/0.68 thf(f201,plain,(
% 2.69/0.68 ($false = ((o21 @ sK1))) | ~spl11_2),
% 2.69/0.68 inference(avatar_component_clause,[],[f199])).
% 2.69/0.68 thf(f202,plain,(
% 2.69/0.68 spl11_1 | spl11_2),
% 2.69/0.68 inference(avatar_split_clause,[],[f117,f199,f195])).
% 2.69/0.68 thf(f204,definition,(
% 2.69/0.68 spl11_3 <=> ($false = ((o11 @ sK3)))),
% 2.69/0.68 introduced(definition,[new_symbols(definition,[spl11_3])],[avatar_definition])).
% 2.69/0.68 thf(f206,plain,(
% 2.69/0.68 ($false = ((o11 @ sK3))) | ~spl11_3),
% 2.69/0.68 inference(avatar_component_clause,[],[f204])).
% 2.69/0.68 thf(f208,definition,(
% 2.69/0.68 spl11_4 <=> ($false = ((o31 @ sK3)))),
% 2.69/0.68 introduced(definition,[new_symbols(definition,[spl11_4])],[avatar_definition])).
% 2.69/0.68 thf(f210,plain,(
% 2.69/0.68 ($false = ((o31 @ sK3))) | ~spl11_4),
% 2.69/0.68 inference(avatar_component_clause,[],[f208])).
% 2.69/0.68 thf(f211,plain,(
% 2.69/0.68 spl11_3 | spl11_4),
% 2.69/0.68 inference(avatar_split_clause,[],[f128,f208,f204])).
% 2.69/0.68 thf(f213,definition,(
% 2.69/0.68 spl11_5 <=> ($false = ((o21 @ sK5)))),
% 2.69/0.68 introduced(definition,[new_symbols(definition,[spl11_5])],[avatar_definition])).
% 2.69/0.68 thf(f215,plain,(
% 2.69/0.68 ($false = ((o21 @ sK5))) | ~spl11_5),
% 2.69/0.68 inference(avatar_component_clause,[],[f213])).
% 2.69/0.68 thf(f217,definition,(
% 2.69/0.68 spl11_6 <=> ($false = ((o31 @ sK5)))),
% 2.69/0.68 introduced(definition,[new_symbols(definition,[spl11_6])],[avatar_definition])).
% 2.69/0.68 thf(f219,plain,(
% 2.69/0.68 ($false = ((o31 @ sK5))) | ~spl11_6),
% 2.69/0.68 inference(avatar_component_clause,[],[f217])).
% 2.69/0.68 thf(f220,plain,(
% 2.69/0.68 spl11_5 | spl11_6),
% 2.69/0.68 inference(avatar_split_clause,[],[f139,f217,f213])).
% 2.69/0.68 thf(f222,definition,(
% 2.69/0.68 spl11_7 <=> ($false = ((o12 @ sK7)))),
% 2.69/0.68 introduced(definition,[new_symbols(definition,[spl11_7])],[avatar_definition])).
% 2.69/0.68 thf(f224,plain,(
% 2.69/0.68 ($false = ((o12 @ sK7))) | ~spl11_7),
% 2.69/0.68 inference(avatar_component_clause,[],[f222])).
% 2.69/0.68 thf(f226,definition,(
% 2.69/0.68 spl11_8 <=> ($false = ((o22 @ sK7)))),
% 2.69/0.68 introduced(definition,[new_symbols(definition,[spl11_8])],[avatar_definition])).
% 2.69/0.68 thf(f228,plain,(
% 2.69/0.68 ($false = ((o22 @ sK7))) | ~spl11_8),
% 2.69/0.68 inference(avatar_component_clause,[],[f226])).
% 2.69/0.68 thf(f229,plain,(
% 2.69/0.68 spl11_7 | spl11_8),
% 2.69/0.68 inference(avatar_split_clause,[],[f150,f226,f222])).
% 2.69/0.68 thf(f231,definition,(
% 2.69/0.68 spl11_9 <=> ($false = ((o12 @ sK9)))),
% 2.69/0.68 introduced(definition,[new_symbols(definition,[spl11_9])],[avatar_definition])).
% 2.69/0.68 thf(f233,plain,(
% 2.69/0.68 ($false = ((o12 @ sK9))) | ~spl11_9),
% 2.69/0.68 inference(avatar_component_clause,[],[f231])).
% 2.69/0.68 thf(f235,definition,(
% 2.69/0.68 spl11_10 <=> ($false = ((o32 @ sK9)))),
% 2.69/0.68 introduced(definition,[new_symbols(definition,[spl11_10])],[avatar_definition])).
% 2.69/0.68 thf(f237,plain,(
% 2.69/0.68 ($false = ((o32 @ sK9))) | ~spl11_10),
% 2.69/0.68 inference(avatar_component_clause,[],[f235])).
% 2.69/0.68 thf(f238,plain,(
% 2.69/0.68 spl11_9 | spl11_10),
% 2.69/0.68 inference(avatar_split_clause,[],[f161,f235,f231])).
% 2.69/0.68 thf(f240,definition,(
% 2.69/0.68 spl11_11 <=> ($false = ((o22 @ sK10)))),
% 2.69/0.68 introduced(definition,[new_symbols(definition,[spl11_11])],[avatar_definition])).
% 2.69/0.68 thf(f242,plain,(
% 2.69/0.68 ($false = ((o22 @ sK10))) | ~spl11_11),
% 2.69/0.68 inference(avatar_component_clause,[],[f240])).
% 2.69/0.68 thf(f244,definition,(
% 2.69/0.68 spl11_12 <=> ($false = ((o32 @ sK10)))),
% 2.69/0.68 introduced(definition,[new_symbols(definition,[spl11_12])],[avatar_definition])).
% 2.69/0.68 thf(f246,plain,(
% 2.69/0.68 ($false = ((o32 @ sK10))) | ~spl11_12),
% 2.69/0.68 inference(avatar_component_clause,[],[f244])).
% 2.69/0.68 thf(f247,plain,(
% 2.69/0.68 spl11_11 | spl11_12),
% 2.69/0.68 inference(avatar_split_clause,[],[f166,f244,f240])).
% 2.69/0.68 thf(f268,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true != $true) | ($true = ((irel @ X0 @ sK1))) | ($true != ((irel @ X0 @ sK0)))) )),
% 2.69/0.68 inference(constrained_superposition,[],[f69,f116])).
% 2.69/0.68 thf(f269,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true != $true) | ($true = ((irel @ X0 @ sK2))) | ($true != ((irel @ X0 @ sK0)))) )),
% 2.69/0.68 inference(constrained_superposition,[],[f69,f121])).
% 2.69/0.68 thf(f270,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true != $true) | ($true = ((irel @ X0 @ sK3))) | ($true != ((irel @ X0 @ sK2)))) )),
% 2.69/0.68 inference(constrained_superposition,[],[f69,f127])).
% 2.69/0.68 thf(f271,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true != $true) | ($true = ((irel @ X0 @ sK4))) | ($true != ((irel @ X0 @ sK2)))) )),
% 2.69/0.68 inference(constrained_superposition,[],[f69,f132])).
% 2.69/0.68 thf(f273,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true != $true) | ($true = ((irel @ X0 @ sK6))) | ($true != ((irel @ X0 @ sK4)))) )),
% 2.69/0.68 inference(constrained_superposition,[],[f69,f143])).
% 2.69/0.68 thf(f274,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true != $true) | ($true = ((irel @ X0 @ sK7))) | ($true != ((irel @ X0 @ sK6)))) )),
% 2.69/0.68 inference(constrained_superposition,[],[f69,f149])).
% 2.69/0.68 thf(f275,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true != $true) | ($true = ((irel @ X0 @ sK8))) | ($true != ((irel @ X0 @ sK6)))) )),
% 2.69/0.68 inference(constrained_superposition,[],[f69,f154])).
% 2.69/0.68 thf(f276,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true != $true) | ($true = ((irel @ X0 @ sK9))) | ($true != ((irel @ X0 @ sK8)))) )),
% 2.69/0.68 inference(constrained_superposition,[],[f69,f160])).
% 2.69/0.68 thf(f277,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true != $true) | ($true = ((irel @ X0 @ sK10))) | ($true != ((irel @ X0 @ sK8)))) )),
% 2.69/0.68 inference(constrained_superposition,[],[f69,f165])).
% 2.69/0.68 thf(f280,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true != ((irel @ X0 @ sK8))) | ($true = ((irel @ X0 @ sK10)))) )),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f277])).
% 2.69/0.68 thf(f281,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true != ((irel @ X0 @ sK8))) | ($true = ((irel @ X0 @ sK9)))) )),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f276])).
% 2.69/0.68 thf(f282,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true != ((irel @ X0 @ sK6))) | ($true = ((irel @ X0 @ sK8)))) )),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f275])).
% 2.69/0.68 thf(f283,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true != ((irel @ X0 @ sK6))) | ($true = ((irel @ X0 @ sK7)))) )),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f274])).
% 2.69/0.68 thf(f284,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true != ((irel @ X0 @ sK4))) | ($true = ((irel @ X0 @ sK6)))) )),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f273])).
% 2.69/0.68 thf(f286,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true != ((irel @ X0 @ sK2))) | ($true = ((irel @ X0 @ sK4)))) )),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f271])).
% 2.69/0.68 thf(f287,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true != ((irel @ X0 @ sK2))) | ($true = ((irel @ X0 @ sK3)))) )),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f270])).
% 2.69/0.68 thf(f288,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true != ((irel @ X0 @ sK0))) | ($true = ((irel @ X0 @ sK2)))) )),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f269])).
% 2.69/0.68 thf(f289,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true != ((irel @ X0 @ sK0))) | ($true = ((irel @ X0 @ sK1)))) )),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f268])).
% 2.69/0.68 thf(f291,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true != $true) | ($true = ((irel @ X0 @ sK2))) | ($false = ((irel @ X0 @ sK0)))) )),
% 2.69/0.68 inference(constrained_superposition,[],[f288,f94])).
% 2.69/0.68 thf(f292,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true = ((irel @ X0 @ sK2))) | ($false = ((irel @ X0 @ sK0)))) )),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f291])).
% 2.69/0.68 thf(f295,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true != $true) | ($true = ((irel @ X0 @ sK1))) | ($false = ((irel @ X0 @ sK0)))) )),
% 2.69/0.68 inference(constrained_superposition,[],[f289,f94])).
% 2.69/0.68 thf(f296,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true = ((irel @ X0 @ sK1))) | ($false = ((irel @ X0 @ sK0)))) )),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f295])).
% 2.69/0.68 thf(f304,plain,(
% 2.69/0.68 ($true != $true) | ($true = ((irel @ sK0 @ sK4)))),
% 2.69/0.68 inference(constrained_superposition,[],[f286,f121])).
% 2.69/0.68 thf(f307,plain,(
% 2.69/0.68 ($true = ((irel @ sK0 @ sK4)))),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f304])).
% 2.69/0.68 thf(f313,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true != $true) | ($true = ((irel @ X0 @ sK3))) | ($false = ((irel @ X0 @ sK0)))) )),
% 2.69/0.68 inference(constrained_superposition,[],[f287,f292])).
% 2.69/0.68 thf(f318,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true = ((irel @ X0 @ sK3))) | ($false = ((irel @ X0 @ sK0)))) )),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f313])).
% 2.69/0.68 thf(f333,plain,(
% 2.69/0.68 ($true != $true) | ($true = ((irel @ sK0 @ sK6)))),
% 2.69/0.68 inference(constrained_superposition,[],[f284,f307])).
% 2.69/0.68 thf(f338,plain,(
% 2.69/0.68 ($true = ((irel @ sK0 @ sK6)))),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f333])).
% 2.69/0.68 thf(f355,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ sK4 @ X0))) | ($true = ((o32 @ X0))) | ($true = ((o31 @ sK5)))) )),
% 2.69/0.68 inference(constrained_superposition,[],[f175,f138])).
% 2.69/0.68 thf(f500,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($false = ((irel @ sK4 @ X0))) | ($true = ((o32 @ X0))) | ($true = ((o31 @ sK5)))) )),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f355])).
% 2.69/0.68 thf(f558,definition,(
% 2.69/0.68 spl11_22 <=> ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($true = ((o31 @ X0))))),
% 2.69/0.68 introduced(definition,[new_symbols(definition,[spl11_22])],[avatar_definition])).
% 2.69/0.68 thf(f559,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($true = ((o31 @ X0)))) ) | ~spl11_22),
% 2.69/0.68 inference(avatar_component_clause,[],[f558])).
% 2.69/0.68 thf(f615,definition,(
% 2.69/0.68 spl11_34 <=> ! [X0 : $i] : (($false = ((irel @ sK4 @ X0))) | ($true = ((o32 @ X0))))),
% 2.69/0.68 introduced(definition,[new_symbols(definition,[spl11_34])],[avatar_definition])).
% 2.69/0.68 thf(f616,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($false = ((irel @ sK4 @ X0))) | ($true = ((o32 @ X0)))) ) | ~spl11_34),
% 2.69/0.68 inference(avatar_component_clause,[],[f615])).
% 2.69/0.68 thf(f619,definition,(
% 2.69/0.68 spl11_35 <=> ($true = ((o31 @ sK5)))),
% 2.69/0.68 introduced(definition,[new_symbols(definition,[spl11_35])],[avatar_definition])).
% 2.69/0.68 thf(f621,plain,(
% 2.69/0.68 ($true = ((o31 @ sK5))) | ~spl11_35),
% 2.69/0.68 inference(avatar_component_clause,[],[f619])).
% 2.69/0.68 thf(f688,plain,(
% 2.69/0.68 spl11_35 | spl11_34),
% 2.69/0.68 inference(avatar_split_clause,[],[f500,f615,f619])).
% 2.69/0.68 thf(f861,plain,(
% 2.69/0.68 ($true = $false) | ($true = ((o31 @ sK3))) | ($false = ((irel @ sK0 @ sK0))) | ~spl11_22),
% 2.69/0.68 inference(constrained_superposition,[],[f559,f318])).
% 2.69/0.68 thf(f910,plain,(
% 2.69/0.68 ($true = ((o31 @ sK3))) | ($false = ((irel @ sK0 @ sK0))) | ~spl11_22),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f861])).
% 2.69/0.68 thf(f926,plain,(
% 2.69/0.68 ($true = $false) | ($false = ((irel @ sK0 @ sK0))) | (~spl11_4 | ~spl11_22)),
% 2.69/0.68 inference(forward_demodulation,[],[f910,f210])).
% 2.69/0.68 thf(f927,plain,(
% 2.69/0.68 ($false = ((irel @ sK0 @ sK0))) | (~spl11_4 | ~spl11_22)),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f926])).
% 2.69/0.68 thf(f934,plain,(
% 2.69/0.68 ($true = $false) | (~spl11_4 | ~spl11_22)),
% 2.69/0.68 inference(forward_demodulation,[],[f927,f68])).
% 2.69/0.68 thf(f935,plain,(
% 2.69/0.68 $false | (~spl11_4 | ~spl11_22)),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f934])).
% 2.69/0.68 thf(f936,plain,(
% 2.69/0.68 ~spl11_4 | ~spl11_22),
% 2.69/0.68 inference(avatar_contradiction_clause,[],[f935])).
% 2.69/0.68 thf(f988,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ sK0 @ X0))) | ($true = ((o22 @ X0))) | ($true = ((o21 @ sK1)))) )),
% 2.69/0.68 inference(constrained_superposition,[],[f184,f116])).
% 2.69/0.68 thf(f1046,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ sK4 @ X0))) | ($true = ((o22 @ X0))) | ($true = ((o21 @ sK5)))) )),
% 2.69/0.68 inference(constrained_superposition,[],[f138,f184])).
% 2.69/0.68 thf(f1109,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($false = ((irel @ sK4 @ X0))) | ($true = ((o22 @ X0))) | ($true = ((o21 @ sK5)))) )),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f1046])).
% 2.69/0.68 thf(f1161,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($true = ((o22 @ X0))) | ($true = ((o21 @ sK1)))) )),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f988])).
% 2.69/0.68 thf(f1220,definition,(
% 2.69/0.68 spl11_55 <=> ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($true = ((o21 @ X0))))),
% 2.69/0.68 introduced(definition,[new_symbols(definition,[spl11_55])],[avatar_definition])).
% 2.69/0.68 thf(f1221,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($true = ((o21 @ X0)))) ) | ~spl11_55),
% 2.69/0.68 inference(avatar_component_clause,[],[f1220])).
% 2.69/0.68 thf(f1281,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ sK4 @ X0))) | ($true = ((o22 @ X0)))) ) | ~spl11_5),
% 2.69/0.68 inference(forward_demodulation,[],[f1109,f215])).
% 2.69/0.68 thf(f1282,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($false = ((irel @ sK4 @ X0))) | ($true = ((o22 @ X0)))) ) | ~spl11_5),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f1281])).
% 2.69/0.68 thf(f1298,definition,(
% 2.69/0.68 spl11_71 <=> ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($true = ((o22 @ X0))))),
% 2.69/0.68 introduced(definition,[new_symbols(definition,[spl11_71])],[avatar_definition])).
% 2.69/0.68 thf(f1299,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($true = ((o22 @ X0)))) ) | ~spl11_71),
% 2.69/0.68 inference(avatar_component_clause,[],[f1298])).
% 2.69/0.68 thf(f1309,definition,(
% 2.69/0.68 spl11_73 <=> ($true = ((o21 @ sK1)))),
% 2.69/0.68 introduced(definition,[new_symbols(definition,[spl11_73])],[avatar_definition])).
% 2.69/0.68 thf(f1311,plain,(
% 2.69/0.68 ($true = ((o21 @ sK1))) | ~spl11_73),
% 2.69/0.68 inference(avatar_component_clause,[],[f1309])).
% 2.69/0.68 thf(f1360,plain,(
% 2.69/0.68 spl11_73 | spl11_71),
% 2.69/0.68 inference(avatar_split_clause,[],[f1161,f1298,f1309])).
% 2.69/0.68 thf(f1728,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ sK0 @ X0))) | ($true = ((o12 @ X0))) | ($true = ((o11 @ sK1)))) )),
% 2.69/0.68 inference(constrained_superposition,[],[f116,f193])).
% 2.69/0.68 thf(f1807,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($true = ((o12 @ X0))) | ($true = ((o11 @ sK1)))) )),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f1728])).
% 2.69/0.68 thf(f1881,definition,(
% 2.69/0.68 spl11_81 <=> ($true = ((o12 @ sK7)))),
% 2.69/0.68 introduced(definition,[new_symbols(definition,[spl11_81])],[avatar_definition])).
% 2.69/0.68 thf(f1883,plain,(
% 2.69/0.68 ($true = ((o12 @ sK7))) | ~spl11_81),
% 2.69/0.68 inference(avatar_component_clause,[],[f1881])).
% 2.69/0.68 thf(f1913,definition,(
% 2.69/0.68 spl11_88 <=> ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($true = ((o11 @ X0))))),
% 2.69/0.68 introduced(definition,[new_symbols(definition,[spl11_88])],[avatar_definition])).
% 2.69/0.68 thf(f1914,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($true = ((o11 @ X0)))) ) | ~spl11_88),
% 2.69/0.68 inference(avatar_component_clause,[],[f1913])).
% 2.69/0.68 thf(f2004,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ sK0 @ X0))) | ($true = ((o12 @ X0)))) ) | ~spl11_1),
% 2.69/0.68 inference(forward_demodulation,[],[f1807,f197])).
% 2.69/0.68 thf(f2005,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($true = ((o12 @ X0)))) ) | ~spl11_1),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f2004])).
% 2.69/0.68 thf(f2386,plain,(
% 2.69/0.68 ($true = $false) | ($true = ((o21 @ sK1))) | ($false = ((irel @ sK0 @ sK0))) | ~spl11_55),
% 2.69/0.68 inference(constrained_superposition,[],[f1221,f296])).
% 2.69/0.68 thf(f2439,plain,(
% 2.69/0.68 ($true = ((o21 @ sK1))) | ($false = ((irel @ sK0 @ sK0))) | ~spl11_55),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f2386])).
% 2.69/0.68 thf(f2443,plain,(
% 2.69/0.68 ($true = $false) | ($true = ((o21 @ sK1))) | ~spl11_55),
% 2.69/0.68 inference(forward_demodulation,[],[f2439,f68])).
% 2.69/0.68 thf(f2846,plain,(
% 2.69/0.68 ($true = $false) | ($false = ((irel @ sK0 @ sK0))) | ($true = ((o11 @ sK3))) | ~spl11_88),
% 2.69/0.68 inference(constrained_superposition,[],[f318,f1914])).
% 2.69/0.68 thf(f2864,plain,(
% 2.69/0.68 ($false = ((irel @ sK0 @ sK0))) | ($true = ((o11 @ sK3))) | ~spl11_88),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f2846])).
% 2.69/0.68 thf(f4387,plain,(
% 2.69/0.68 ($true != $true) | ($true = ((irel @ sK0 @ sK8)))),
% 2.69/0.68 inference(constrained_superposition,[],[f282,f338])).
% 2.69/0.68 thf(f4397,plain,(
% 2.69/0.68 ($true != $true) | ($true = ((irel @ sK4 @ sK8)))),
% 2.69/0.68 inference(constrained_superposition,[],[f282,f143])).
% 2.69/0.68 thf(f4410,plain,(
% 2.69/0.68 ($true = ((irel @ sK4 @ sK8)))),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f4397])).
% 2.69/0.68 thf(f4412,plain,(
% 2.69/0.68 ($true = ((irel @ sK0 @ sK8)))),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f4387])).
% 2.69/0.68 thf(f4591,plain,(
% 2.69/0.68 ($true != $true) | ($true = ((irel @ sK0 @ sK7)))),
% 2.69/0.68 inference(constrained_superposition,[],[f283,f338])).
% 2.69/0.68 thf(f4601,plain,(
% 2.69/0.68 ($true != $true) | ($true = ((irel @ sK4 @ sK7)))),
% 2.69/0.68 inference(constrained_superposition,[],[f283,f143])).
% 2.69/0.68 thf(f4614,plain,(
% 2.69/0.68 ($true = ((irel @ sK4 @ sK7)))),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f4601])).
% 2.69/0.68 thf(f4616,plain,(
% 2.69/0.68 ($true = ((irel @ sK0 @ sK7)))),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f4591])).
% 2.69/0.68 thf(f4632,plain,(
% 2.69/0.68 ($true = $false) | ($true = ((o22 @ sK7))) | ~spl11_5),
% 2.69/0.68 inference(constrained_superposition,[],[f4614,f1282])).
% 2.69/0.68 thf(f4667,plain,(
% 2.69/0.68 ($true = ((o22 @ sK7))) | ~spl11_5),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f4632])).
% 2.69/0.68 thf(f4684,plain,(
% 2.69/0.68 ($true = $false) | (~spl11_5 | ~spl11_8)),
% 2.69/0.68 inference(forward_demodulation,[],[f4667,f228])).
% 2.69/0.68 thf(f4685,plain,(
% 2.69/0.68 $false | (~spl11_5 | ~spl11_8)),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f4684])).
% 2.69/0.68 thf(f4686,plain,(
% 2.69/0.68 ~spl11_5 | ~spl11_8),
% 2.69/0.68 inference(avatar_contradiction_clause,[],[f4685])).
% 2.69/0.68 thf(f4690,definition,(
% 2.69/0.68 spl11_109 <=> ($true = ((o22 @ sK7)))),
% 2.69/0.68 introduced(definition,[new_symbols(definition,[spl11_109])],[avatar_definition])).
% 2.69/0.68 thf(f4692,plain,(
% 2.69/0.68 ($true = ((o22 @ sK7))) | ~spl11_109),
% 2.69/0.68 inference(avatar_component_clause,[],[f4690])).
% 2.69/0.68 thf(f4790,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ sK0 @ X0))) | ($true = ((o22 @ sK7))) | ($true = ((o21 @ X0)))) )),
% 2.69/0.68 inference(constrained_superposition,[],[f4616,f184])).
% 2.69/0.68 thf(f4792,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ sK0 @ X0))) | ($true = ((o12 @ sK7))) | ($true = ((o11 @ X0)))) )),
% 2.69/0.68 inference(constrained_superposition,[],[f4616,f193])).
% 2.69/0.68 thf(f4798,plain,(
% 2.69/0.68 ($true = $false) | ($true = ((o12 @ sK7))) | ~spl11_1),
% 2.69/0.68 inference(constrained_superposition,[],[f4616,f2005])).
% 2.69/0.68 thf(f4827,plain,(
% 2.69/0.68 ($true = ((o12 @ sK7))) | ~spl11_1),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f4798])).
% 2.69/0.68 thf(f4833,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($true = ((o12 @ sK7))) | ($true = ((o11 @ X0)))) )),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f4792])).
% 2.69/0.68 thf(f4835,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($true = ((o22 @ sK7))) | ($true = ((o21 @ X0)))) )),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f4790])).
% 2.69/0.68 thf(f4843,plain,(
% 2.69/0.68 ($true = $false) | (~spl11_1 | ~spl11_7)),
% 2.69/0.68 inference(forward_demodulation,[],[f4827,f224])).
% 2.69/0.68 thf(f4844,plain,(
% 2.69/0.68 $false | (~spl11_1 | ~spl11_7)),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f4843])).
% 2.69/0.68 thf(f4845,plain,(
% 2.69/0.68 ~spl11_1 | ~spl11_7),
% 2.69/0.68 inference(avatar_contradiction_clause,[],[f4844])).
% 2.69/0.68 thf(f4849,plain,(
% 2.69/0.68 spl11_81 | spl11_88),
% 2.69/0.68 inference(avatar_split_clause,[],[f4833,f1913,f1881])).
% 2.69/0.68 thf(f4922,plain,(
% 2.69/0.68 ($true = $false) | (~spl11_8 | ~spl11_109)),
% 2.69/0.68 inference(constrained_superposition,[],[f228,f4692])).
% 2.69/0.68 thf(f4928,plain,(
% 2.69/0.68 $false | (~spl11_8 | ~spl11_109)),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f4922])).
% 2.69/0.68 thf(f4929,plain,(
% 2.69/0.68 ~spl11_8 | ~spl11_109),
% 2.69/0.68 inference(avatar_contradiction_clause,[],[f4928])).
% 2.69/0.68 thf(f6458,plain,(
% 2.69/0.68 ($true != $true) | ($true = ((irel @ sK0 @ sK10)))),
% 2.69/0.68 inference(constrained_superposition,[],[f280,f4412])).
% 2.69/0.68 thf(f6482,plain,(
% 2.69/0.68 ($true = ((irel @ sK0 @ sK10)))),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f6458])).
% 2.69/0.68 thf(f6952,plain,(
% 2.69/0.68 ($true = $false) | (~spl11_6 | ~spl11_35)),
% 2.69/0.68 inference(forward_demodulation,[],[f621,f219])).
% 2.69/0.68 thf(f6953,plain,(
% 2.69/0.68 $false | (~spl11_6 | ~spl11_35)),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f6952])).
% 2.69/0.68 thf(f6954,plain,(
% 2.69/0.68 ~spl11_6 | ~spl11_35),
% 2.69/0.68 inference(avatar_contradiction_clause,[],[f6953])).
% 2.69/0.68 thf(f7054,definition,(
% 2.69/0.68 spl11_126 <=> ($true = ((o32 @ sK10)))),
% 2.69/0.68 introduced(definition,[new_symbols(definition,[spl11_126])],[avatar_definition])).
% 2.69/0.68 thf(f7056,plain,(
% 2.69/0.68 ($true = ((o32 @ sK10))) | ~spl11_126),
% 2.69/0.68 inference(avatar_component_clause,[],[f7054])).
% 2.69/0.68 thf(f7574,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ sK0 @ X0))) | ($true = ((o32 @ sK10))) | ($true = ((o31 @ X0)))) )),
% 2.69/0.68 inference(constrained_superposition,[],[f6482,f175])).
% 2.69/0.68 thf(f7635,plain,(
% 2.69/0.68 ( ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($true = ((o32 @ sK10))) | ($true = ((o31 @ X0)))) )),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f7574])).
% 2.69/0.68 thf(f8023,plain,(
% 2.69/0.68 ($true != $true) | ($true = ((irel @ sK0 @ sK9)))),
% 2.69/0.68 inference(constrained_superposition,[],[f281,f4412])).
% 2.69/0.68 thf(f8031,plain,(
% 2.69/0.68 ($true != $true) | ($true = ((irel @ sK4 @ sK9)))),
% 2.69/0.68 inference(constrained_superposition,[],[f281,f4410])).
% 2.69/0.68 thf(f8043,plain,(
% 2.69/0.68 ($true = ((irel @ sK4 @ sK9)))),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f8031])).
% 2.69/0.68 thf(f8045,plain,(
% 2.69/0.68 ($true = ((irel @ sK0 @ sK9)))),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f8023])).
% 2.69/0.68 thf(f8125,plain,(
% 2.69/0.68 ($true = $false) | ($true = ((o32 @ sK9))) | ~spl11_34),
% 2.69/0.68 inference(constrained_superposition,[],[f8043,f616])).
% 2.69/0.68 thf(f8162,plain,(
% 2.69/0.68 ($true = ((o32 @ sK9))) | ~spl11_34),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f8125])).
% 2.69/0.68 thf(f8180,plain,(
% 2.69/0.68 ($true = $false) | (~spl11_10 | ~spl11_34)),
% 2.69/0.68 inference(forward_demodulation,[],[f8162,f237])).
% 2.69/0.68 thf(f8181,plain,(
% 2.69/0.68 $false | (~spl11_10 | ~spl11_34)),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f8180])).
% 2.69/0.68 thf(f8182,plain,(
% 2.69/0.68 ~spl11_10 | ~spl11_34),
% 2.69/0.68 inference(avatar_contradiction_clause,[],[f8181])).
% 2.69/0.68 thf(f8288,plain,(
% 2.69/0.68 ($true = $false) | ($true = ((o12 @ sK9))) | ~spl11_1),
% 2.69/0.68 inference(constrained_superposition,[],[f8045,f2005])).
% 2.69/0.68 thf(f8323,plain,(
% 2.69/0.68 ($true = ((o12 @ sK9))) | ~spl11_1),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f8288])).
% 2.69/0.68 thf(f8342,plain,(
% 2.69/0.68 ($true = $false) | (~spl11_1 | ~spl11_9)),
% 2.69/0.68 inference(forward_demodulation,[],[f8323,f233])).
% 2.69/0.68 thf(f8343,plain,(
% 2.69/0.68 $false | (~spl11_1 | ~spl11_9)),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f8342])).
% 2.69/0.68 thf(f8344,plain,(
% 2.69/0.68 ~spl11_1 | ~spl11_9),
% 2.69/0.68 inference(avatar_contradiction_clause,[],[f8343])).
% 2.69/0.68 thf(f8399,plain,(
% 2.69/0.68 ($true = ((o21 @ sK1))) | ~spl11_55),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f2443])).
% 2.69/0.68 thf(f8448,plain,(
% 2.69/0.68 ($true = $false) | ($true = ((o11 @ sK3))) | ~spl11_88),
% 2.69/0.68 inference(forward_demodulation,[],[f2864,f68])).
% 2.69/0.68 thf(f8449,plain,(
% 2.69/0.68 ($true = ((o11 @ sK3))) | ~spl11_88),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f8448])).
% 2.69/0.68 thf(f8704,plain,(
% 2.69/0.68 ($true = $false) | (~spl11_2 | ~spl11_73)),
% 2.69/0.68 inference(constrained_superposition,[],[f201,f1311])).
% 2.69/0.68 thf(f8710,plain,(
% 2.69/0.68 $false | (~spl11_2 | ~spl11_73)),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f8704])).
% 2.69/0.68 thf(f8711,plain,(
% 2.69/0.68 ~spl11_2 | ~spl11_73),
% 2.69/0.68 inference(avatar_contradiction_clause,[],[f8710])).
% 2.69/0.68 thf(f8928,plain,(
% 2.69/0.68 ($true = $false) | (~spl11_2 | ~spl11_55)),
% 2.69/0.68 inference(forward_demodulation,[],[f8399,f201])).
% 2.69/0.68 thf(f8929,plain,(
% 2.69/0.68 $false | (~spl11_2 | ~spl11_55)),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f8928])).
% 2.69/0.68 thf(f8930,plain,(
% 2.69/0.68 ~spl11_2 | ~spl11_55),
% 2.69/0.68 inference(avatar_contradiction_clause,[],[f8929])).
% 2.69/0.68 thf(f9280,plain,(
% 2.69/0.68 spl11_109 | spl11_55),
% 2.69/0.68 inference(avatar_split_clause,[],[f4835,f1220,f4690])).
% 2.69/0.68 thf(f10661,plain,(
% 2.69/0.68 ($true = $false) | ($true = ((o22 @ sK10))) | ~spl11_71),
% 2.69/0.68 inference(constrained_superposition,[],[f1299,f6482])).
% 2.69/0.68 thf(f10744,plain,(
% 2.69/0.68 ($true = ((o22 @ sK10))) | ~spl11_71),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f10661])).
% 2.69/0.68 thf(f10778,plain,(
% 2.69/0.68 ($true = $false) | (~spl11_11 | ~spl11_71)),
% 2.69/0.68 inference(forward_demodulation,[],[f10744,f242])).
% 2.69/0.68 thf(f10779,plain,(
% 2.69/0.68 $false | (~spl11_11 | ~spl11_71)),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f10778])).
% 2.69/0.68 thf(f10780,plain,(
% 2.69/0.68 ~spl11_11 | ~spl11_71),
% 2.69/0.68 inference(avatar_contradiction_clause,[],[f10779])).
% 2.69/0.68 thf(f10951,plain,(
% 2.69/0.68 spl11_126 | spl11_22),
% 2.69/0.68 inference(avatar_split_clause,[],[f7635,f558,f7054])).
% 2.69/0.68 thf(f11116,plain,(
% 2.69/0.68 ($true = $false) | (~spl11_12 | ~spl11_126)),
% 2.69/0.68 inference(forward_demodulation,[],[f7056,f246])).
% 2.69/0.68 thf(f11117,plain,(
% 2.69/0.68 $false | (~spl11_12 | ~spl11_126)),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f11116])).
% 2.69/0.68 thf(f11118,plain,(
% 2.69/0.68 ~spl11_12 | ~spl11_126),
% 2.69/0.68 inference(avatar_contradiction_clause,[],[f11117])).
% 2.69/0.68 thf(f11352,plain,(
% 2.69/0.68 ($true = $false) | (~spl11_3 | ~spl11_88)),
% 2.69/0.68 inference(forward_demodulation,[],[f8449,f206])).
% 2.69/0.68 thf(f11353,plain,(
% 2.69/0.68 $false | (~spl11_3 | ~spl11_88)),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f11352])).
% 2.69/0.68 thf(f11354,plain,(
% 2.69/0.68 ~spl11_3 | ~spl11_88),
% 2.69/0.68 inference(avatar_contradiction_clause,[],[f11353])).
% 2.69/0.68 thf(f11458,plain,(
% 2.69/0.68 ($true = $false) | (~spl11_7 | ~spl11_81)),
% 2.69/0.68 inference(forward_demodulation,[],[f1883,f224])).
% 2.69/0.68 thf(f11459,plain,(
% 2.69/0.68 $false | (~spl11_7 | ~spl11_81)),
% 2.69/0.68 inference(trivial_inequality_removal,[],[f11458])).
% 2.69/0.68 thf(f11460,plain,(
% 2.69/0.68 ~spl11_7 | ~spl11_81),
% 2.69/0.68 inference(avatar_contradiction_clause,[],[f11459])).
% 2.69/0.68 cnf(s1, plain, spl11_1 | spl11_2, inference(sat_conversion,[],[f202])).
% 2.69/0.68 cnf(s2, plain, spl11_3 | spl11_4, inference(sat_conversion,[],[f211])).
% 2.69/0.68 cnf(s3, plain, spl11_5 | spl11_6, inference(sat_conversion,[],[f220])).
% 2.69/0.68 cnf(s4, plain, spl11_7 | spl11_8, inference(sat_conversion,[],[f229])).
% 2.69/0.68 cnf(s5, plain, spl11_9 | spl11_10, inference(sat_conversion,[],[f238])).
% 2.69/0.68 cnf(s6, plain, spl11_11 | spl11_12, inference(sat_conversion,[],[f247])).
% 2.69/0.68 cnf(s58, plain, spl11_34 | spl11_35, inference(sat_conversion,[],[f688])).
% 2.69/0.68 cnf(s81, plain, ~spl11_4 | ~spl11_22, inference(sat_conversion,[],[f936])).
% 2.69/0.68 cnf(s151, plain, spl11_71 | spl11_73, inference(sat_conversion,[],[f1360])).
% 2.69/0.68 cnf(s251, plain, ~spl11_5 | ~spl11_8, inference(sat_conversion,[],[f4686])).
% 2.69/0.68 cnf(s271, plain, ~spl11_1 | ~spl11_7, inference(sat_conversion,[],[f4845])).
% 2.69/0.68 cnf(s273, plain, spl11_81 | spl11_88, inference(sat_conversion,[],[f4849])).
% 2.69/0.68 cnf(s287, plain, ~spl11_8 | ~spl11_109, inference(sat_conversion,[],[f4929])).
% 2.69/0.68 cnf(s360, plain, ~spl11_6 | ~spl11_35, inference(sat_conversion,[],[f6954])).
% 2.69/0.68 cnf(s402, plain, ~spl11_10 | ~spl11_34, inference(sat_conversion,[],[f8182])).
% 2.69/0.68 cnf(s420, plain, ~spl11_1 | ~spl11_9, inference(sat_conversion,[],[f8344])).
% 2.69/0.68 cnf(s604, plain, ~spl11_2 | ~spl11_73, inference(sat_conversion,[],[f8711])).
% 2.69/0.68 cnf(s675, plain, ~spl11_2 | ~spl11_55, inference(sat_conversion,[],[f8930])).
% 2.69/0.68 cnf(s956, plain, spl11_55 | spl11_109, inference(sat_conversion,[],[f9280])).
% 2.69/0.68 cnf(s1119, plain, ~spl11_11 | ~spl11_71, inference(sat_conversion,[],[f10780])).
% 2.69/0.68 cnf(s1183, plain, spl11_22 | spl11_126, inference(sat_conversion,[],[f10951])).
% 2.69/0.68 cnf(s1310, plain, ~spl11_12 | ~spl11_126, inference(sat_conversion,[],[f11118])).
% 2.69/0.68 cnf(s1436, plain, ~spl11_3 | ~spl11_88, inference(sat_conversion,[],[f11354])).
% 2.69/0.68 cnf(s1515, plain, ~spl11_7 | ~spl11_81, inference(sat_conversion,[],[f11460])).
% 2.69/0.68 cnf(s1704, plain, ~spl11_2, inference(rat,[],[s2,s81,s1436,s1183,s273,s1310,s1515,s6,s4,s1119,s287,s151,s956,s604,s675])).
% 2.69/0.68 cnf(s1705, plain, spl11_1, inference(rat,[],[s1,s1704])).
% 2.69/0.68 cnf(s1706, plain, ~spl11_9, inference(rat,[],[s420,s1705])).
% 2.69/0.68 cnf(s1707, plain, ~spl11_7, inference(rat,[],[s271,s1705])).
% 2.69/0.68 cnf(s1709, plain, spl11_10, inference(rat,[],[s5,s1706])).
% 2.69/0.68 cnf(s1710, plain, spl11_8, inference(rat,[],[s4,s1707])).
% 2.69/0.68 cnf(s1721, plain, ~spl11_34, inference(rat,[],[s402,s1709])).
% 2.69/0.68 cnf(s1726, plain, ~spl11_5, inference(rat,[],[s251,s1710])).
% 2.69/0.68 cnf(s1732, plain, spl11_35, inference(rat,[],[s58,s1721])).
% 2.69/0.68 cnf(s1757, plain, spl11_6, inference(rat,[],[s3,s1726])).
% 2.69/0.68 cnf(s1758, plain, $false, inference(rat,[],[s360,s1732,s1757])).
% 2.69/0.68 thf(f11699,plain,(
% 2.69/0.68 $false),
% 2.69/0.68 inference(avatar_sat_refutation,[],[s1758])).
% 2.69/0.68 % SZS output end Proof for theBenchmark
% 2.69/0.68 % (3744461)------------------------------
% 2.69/0.68 % (3744461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.69/0.68 % (3744461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.69/0.68 % (3744461)CaDiCaL version: 2.1.3
% 2.69/0.68 % (3744461)Termination reason: Refutation
% 2.69/0.68 % (3744461)Time elapsed: 0.301 s
% 2.69/0.68 % (3744461)Peak memory usage: 16 MB
% 2.69/0.68 % (3744461)Instructions burned: 650 (million)
% 2.69/0.68 % (3744438)Success in time 0.432 s
% 2.69/0.68 % Vampire exiting
%------------------------------------------------------------------------------