%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN044^4 : 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 : n011.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:41:48 AM UTC 2026
% Result : Theorem 3.84s 0.88s
% Output : Refutation 3.84s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN044^4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.18 % Computer : n011.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.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Tue Sep 29 16:14:31 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.22 Running first-order model finding
% 0.07/0.22 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
% 3.84/0.88 % (278273)Will run a generic schedule for satisfiability detection.
% 3.84/0.88 % (278279)% WARNING: option uhcvi not known.
% 3.84/0.88 % (278279)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=814090614:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.84/0.88 % (278278)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1044958843_2999 on theBenchmark for (2999ds/0Mi)
% 3.84/0.88 % (278281)dis+10_1_sil=32000:sp=arity:random_seed=74356612:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.84/0.88 % (278282)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=288967520:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.84/0.88 % (278280)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3970957554:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.84/0.88 % (278282)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.84/0.88 % (278279)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.84/0.88 % (278283)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2926403484:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.84/0.88 % Exception at run slice level% (278279)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.84/0.88
% 3.84/0.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.84/0.88 % (278284)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=341079068:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.84/0.88 % (278291)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2863823434:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.84/0.88 % Exception at run slice level
% 3.84/0.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.84/0.88 % (278283)Instruction limit reached!
% 3.84/0.88 % (278283)------------------------------
% 3.84/0.88 % (278283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.84/0.88 % (278283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.84/0.88 % (278283)CaDiCaL version: 2.1.3
% 3.84/0.88 % (278283)Termination reason: Instruction limit
% 3.84/0.88 % (278283)Termination phase: Saturation
% 3.84/0.88 % (278283)Time elapsed: 0.034 s
% 3.84/0.88 % (278283)Peak memory usage: 12 MB
% 3.84/0.88 % (278283)Instructions burned: 132 (million)
% 3.84/0.88 % (278294)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=529670529:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.84/0.88 % (278295)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=1419961301:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 3.84/0.88 % (278295)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.84/0.88 % (278295)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.84/0.88 % (278281)Instruction limit reached!
% 3.84/0.88 % (278281)------------------------------
% 3.84/0.88 % (278281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.84/0.88 % (278281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.84/0.88 % (278281)CaDiCaL version: 2.1.3
% 3.84/0.88 % (278281)Termination reason: Instruction limit
% 3.84/0.88 % (278281)Termination phase: Saturation
% 3.84/0.88 % (278281)Time elapsed: 0.050 s
% 3.84/0.88 % (278281)Peak memory usage: 12 MB
% 3.84/0.88 % (278281)Instructions burned: 103 (million)
% 3.84/0.88 % (278282)Instruction limit reached!
% 3.84/0.88 % (278282)------------------------------
% 3.84/0.88 % (278282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.84/0.88 % (278282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.84/0.88 % (278282)CaDiCaL version: 2.1.3
% 3.84/0.88 % (278282)Termination reason: Instruction limit
% 3.84/0.88 % (278282)Termination phase: Saturation
% 3.84/0.88 % (278282)Time elapsed: 0.057 s
% 3.84/0.88 % (278282)Peak memory usage: 12 MB
% 3.84/0.88 % (278282)Instructions burned: 117 (million)
% 3.84/0.88 % (278298)ott-21_1_sil=16000:fs=off:random_seed=694090813:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 3.84/0.88 % (278299)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=304661177:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 3.84/0.88 % (278294)Instruction limit reached!
% 3.84/0.88 % (278294)------------------------------
% 3.84/0.88 % (278294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.84/0.88 % (278294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.84/0.88 % (278294)CaDiCaL version: 2.1.3
% 3.84/0.88 % (278294)Termination reason: Instruction limit
% 3.84/0.88 % (278294)Termination phase: Saturation
% 3.84/0.88 % (278294)Time elapsed: 0.063 s
% 3.84/0.88 % (278294)Peak memory usage: 12 MB
% 3.84/0.88 % (278294)Instructions burned: 132 (million)
% 3.84/0.88 % (278284)Instruction limit reached!
% 3.84/0.88 % (278284)------------------------------
% 3.84/0.88 % (278284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.84/0.88 % (278284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.84/0.88 % (278302)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1058523173:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 3.84/0.88 % (278284)CaDiCaL version: 2.1.3
% 3.84/0.88 % (278284)Termination reason: Instruction limit
% 3.84/0.88 % (278284)Termination phase: Saturation
% 3.84/0.88 % (278284)Time elapsed: 0.122 s
% 3.84/0.88 % (278284)Peak memory usage: 12 MB
% 3.84/0.88 % (278284)Instructions burned: 159 (million)
% 3.84/0.88 % Exception at run slice level
% 3.84/0.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.84/0.88 % (278304)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4228905601:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 3.84/0.88 % (278305)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1618450999:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 3.84/0.88 % Exception at run slice level
% 3.84/0.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.84/0.88 % (278298)Instruction limit reached!
% 3.84/0.88 % (278298)------------------------------
% 3.84/0.88 % (278298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.84/0.88 % (278298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.84/0.88 % (278298)CaDiCaL version: 2.1.3
% 3.84/0.88 % (278298)Termination reason: Instruction limit
% 3.84/0.88 % (278298)Termination phase: Saturation
% 3.84/0.88 % (278298)Time elapsed: 0.082 s
% 3.84/0.88 % (278298)Peak memory usage: 12 MB
% 3.84/0.88 % (278298)Instructions burned: 182 (million)
% 3.84/0.88 % (278308)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=3071907008: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)
% 3.84/0.88 % (278308)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.84/0.88 % (278309)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=956936986:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 3.84/0.88 % (278309)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.84/0.88 % (278295)Instruction limit reached!
% 3.84/0.88 % (278295)------------------------------
% 3.84/0.88 % (278295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.84/0.88 % (278295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.84/0.88 % (278295)CaDiCaL version: 2.1.3
% 3.84/0.88 % (278295)Termination reason: Instruction limit
% 3.84/0.88 % (278295)Termination phase: Saturation
% 3.84/0.88 % (278295)Time elapsed: 0.145 s
% 3.84/0.88 % (278295)Peak memory usage: 13 MB
% 3.84/0.88 % (278295)Instructions burned: 685 (million)
% 3.84/0.88 % (278312)fmb+10_1_sil=64000:random_seed=939634864:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi)
% 3.84/0.88 % (278312)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 3.84/0.88 % Exception at run slice level
% 3.84/0.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.84/0.88 % (278314)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2960844633:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi)
% 3.84/0.88 % Exception at run slice level
% 3.84/0.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.84/0.88 % (278316)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1676761228:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi)
% 3.84/0.88 % Exception at run slice level
% 3.84/0.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.84/0.88 % (278318)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4197387988:i=5131_2997 on theBenchmark for (2997ds/5131Mi)
% 3.84/0.88 % (278318)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.84/0.88 % (278299)Instruction limit reached!
% 3.84/0.88 % (278299)------------------------------
% 3.84/0.88 % (278299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.84/0.88 % (278299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.84/0.88 % (278299)CaDiCaL version: 2.1.3
% 3.84/0.88 % (278299)Termination reason: Instruction limit
% 3.84/0.88 % (278299)Termination phase: Saturation
% 3.84/0.88 % (278299)Time elapsed: 0.246 s
% 3.84/0.88 % (278299)Peak memory usage: 13 MB
% 3.84/0.88 % (278299)Instructions burned: 478 (million)
% 3.84/0.88 % (278320)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3784940434:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi)
% 3.84/0.88 % (278320)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 3.84/0.88 % (278320)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.84/0.88 % (278309)Instruction limit reached!
% 3.84/0.88 % (278309)------------------------------
% 3.84/0.88 % (278309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.84/0.88 % (278309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.84/0.88 % (278309)CaDiCaL version: 2.1.3
% 3.84/0.88 % (278309)Termination reason: Instruction limit
% 3.84/0.88 % (278309)Termination phase: Saturation
% 3.84/0.88 % (278309)Time elapsed: 0.398 s
% 3.84/0.88 % (278309)Peak memory usage: 14 MB
% 3.84/0.88 % (278309)Instructions burned: 880 (million)
% 3.84/0.88 % (278322)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2232956089:i=6324_2993 on theBenchmark for (2993ds/6324Mi)
% 3.84/0.88 % Exception at run slice level
% 3.84/0.88 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.84/0.88 % (278279) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-278273-278279"...
% 3.84/0.88 % (278308)Instruction limit reached!
% 3.84/0.88 % (278308)------------------------------
% 3.84/0.88 % (278308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.84/0.88 % (278308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.84/0.88 % (278308)CaDiCaL version: 2.1.3
% 3.84/0.88 % (278308)Termination reason: Instruction limit
% 3.84/0.88 % (278308)Termination phase: Saturation
% 3.84/0.88 % (278308)Time elapsed: 0.439 s
% 3.84/0.88 % (278308)Peak memory usage: 15 MB
% 3.84/0.88 % (278308)Instructions burned: 694 (million)
% 3.84/0.88 % (278324)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3787902109:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi)
% 3.84/0.88 % (278279)...printing done.
% 3.84/0.88 % (278279)Refutation found. Thanks to Tanya!
% 3.84/0.88 % SZS status Theorem for theBenchmark
% 3.84/0.88 % SZS output start Proof for theBenchmark
% 3.84/0.88 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 3.84/0.88 thf(func_def_0, type, irel: ($i > $i > $o)).
% 3.84/0.88 thf(func_def_2, type, mnot: (($i > $o) > $i > $o)).
% 3.84/0.88 thf(func_def_3, type, mor: (($i > $o) > ($i > $o) > $i > $o)).
% 3.84/0.88 thf(func_def_4, type, mand: (($i > $o) > ($i > $o) > $i > $o)).
% 3.84/0.88 thf(func_def_5, type, mimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 3.84/0.88 thf(func_def_6, type, mbox_s4: (($i > $o) > $i > $o)).
% 3.84/0.88 thf(func_def_7, type, iatom: (($i > $o) > $i > $o)).
% 3.84/0.88 thf(func_def_8, type, inot: (($i > $o) > $i > $o)).
% 3.84/0.88 thf(func_def_9, type, itrue: ($i > $o)).
% 3.84/0.88 thf(func_def_10, type, ifalse: ($i > $o)).
% 3.84/0.88 thf(func_def_11, type, iand: (($i > $o) > ($i > $o) > $i > $o)).
% 3.84/0.88 thf(func_def_12, type, ior: (($i > $o) > ($i > $o) > $i > $o)).
% 3.84/0.88 thf(func_def_13, type, iimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 3.84/0.88 thf(func_def_14, type, iimplied: (($i > $o) > ($i > $o) > $i > $o)).
% 3.84/0.88 thf(func_def_15, type, iequiv: (($i > $o) > ($i > $o) > $i > $o)).
% 3.84/0.88 thf(func_def_16, type, ixor: (($i > $o) > ($i > $o) > $i > $o)).
% 3.84/0.88 thf(func_def_17, type, ivalid: (($i > $o) > $o)).
% 3.84/0.88 thf(func_def_18, type, isatisfiable: (($i > $o) > $o)).
% 3.84/0.88 thf(func_def_19, type, icountersatisfiable: (($i > $o) > $o)).
% 3.84/0.88 thf(func_def_20, type, iinvalid: (($i > $o) > $o)).
% 3.84/0.88 thf(func_def_21, type, p: ($i > $o)).
% 3.84/0.88 thf(func_def_22, type, q: ($i > $o)).
% 3.84/0.88 thf(func_def_23, type, r: ($i > $o)).
% 3.84/0.88 thf(func_def_26, type, vNOT: ($o > $o)).
% 3.84/0.88 thf(func_def_27, type, db1: !>[X0: $tType]:(X0)).
% 3.84/0.88 thf(func_def_28, type, db0: !>[X0: $tType]:(X0)).
% 3.84/0.88 thf(func_def_29, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 3.84/0.88 thf(func_def_30, type, vOR: ($o > $o > $o)).
% 3.84/0.88 thf(func_def_31, type, db2: !>[X0: $tType]:(X0)).
% 3.84/0.88 thf(func_def_32, type, vAND: ($o > $o > $o)).
% 3.84/0.88 thf(func_def_33, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 3.84/0.88 thf(func_def_34, type, vIMP: ($o > $o > $o)).
% 3.84/0.88 thf(func_def_35, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 3.84/0.88 thf(func_def_40, type, sK4: ($i > $i)).
% 3.84/0.88 thf(func_def_41, type, sK5: ($i > $i)).
% 3.84/0.88 thf(func_def_42, type, sK6: ($i > $i)).
% 3.84/0.88 thf(f1,axiom,(
% 3.84/0.88 ! [X0 : $i] : (irel @ X0 @ X0)),
% 3.84/0.88 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',refl_axiom)).
% 3.84/0.88 thf(f2,axiom,(
% 3.84/0.88 ! [X0 : $i,X1 : $i,X2 : $i] : (((irel @ X1 @ X2) & (irel @ X0 @ X1)) => (irel @ X0 @ X2))),
% 3.84/0.88 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',trans_axiom)).
% 3.84/0.88 thf(f3,axiom,(
% 3.84/0.88 (mnot = (^[X0 : ($i > $o), X1 : $i] : (~(X0 @ X1))))),
% 3.84/0.88 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',mnot)).
% 3.84/0.88 thf(f4,axiom,(
% 3.84/0.88 (mor = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X1 @ X2) | (X0 @ X2))))),
% 3.84/0.88 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',mor)).
% 3.84/0.88 thf(f5,axiom,(
% 3.84/0.88 (mand = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X1 @ X2) & (X0 @ X2))))),
% 3.84/0.88 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',mand)).
% 3.84/0.88 thf(f6,axiom,(
% 3.84/0.88 (mimplies = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mor @ (mnot @ X0) @ X1))))),
% 3.84/0.88 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',mimplies)).
% 3.84/0.88 thf(f7,axiom,(
% 3.84/0.88 (mbox_s4 = (^[X0 : ($i > $o), X1 : $i] : (! [X2 : $i] : ((irel @ X1 @ X2) => (X0 @ X2)))))),
% 3.84/0.88 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',mbox_s4)).
% 3.84/0.88 thf(f8,axiom,(
% 3.84/0.88 (iatom = (^[X0 : ($i > $o)] : (X0)))),
% 3.84/0.88 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',iatom)).
% 3.84/0.88 thf(f12,axiom,(
% 3.84/0.88 (iand = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mand @ X0 @ X1))))),
% 3.84/0.88 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',iand)).
% 3.84/0.88 thf(f13,axiom,(
% 3.84/0.88 (ior = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mor @ (mbox_s4 @ X0) @ (mbox_s4 @ X1)))))),
% 3.84/0.88 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',ior)).
% 3.84/0.88 thf(f14,axiom,(
% 3.84/0.88 (iimplies = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mimplies @ (mbox_s4 @ X0) @ (mbox_s4 @ X1)))))),
% 3.84/0.88 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',iimplies)).
% 3.84/0.88 thf(f16,axiom,(
% 3.84/0.88 (iequiv = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((iand @ (iimplies @ X0 @ X1) @ (iimplies @ X1 @ X0)))))),
% 3.84/0.88 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',iequiv)).
% 3.84/0.88 thf(f18,axiom,(
% 3.84/0.88 (ivalid = (^[X0 : ($i > $o)] : (! [X1 : $i] : (X0 @ X1))))),
% 3.84/0.88 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',ivalid)).
% 3.84/0.88 thf(f22,axiom,(
% 3.84/0.88 (ivalid @ (iimplies @ (iatom @ q) @ (iatom @ r)))),
% 3.84/0.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p',pel10_1)).
% 3.84/0.88 thf(f23,axiom,(
% 3.84/0.88 (ivalid @ (iimplies @ (iatom @ r) @ (iand @ (iatom @ p) @ (iatom @ q))))),
% 3.84/0.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p',pel10_2)).
% 3.84/0.88 thf(f24,axiom,(
% 3.84/0.88 (ivalid @ (iimplies @ (iatom @ p) @ (ior @ (iatom @ q) @ (iatom @ r))))),
% 3.84/0.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p',pel10_3)).
% 3.84/0.88 thf(f25,conjecture,(
% 3.84/0.88 (ivalid @ (iequiv @ (iatom @ p) @ (iatom @ q)))),
% 3.84/0.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p',pel10)).
% 3.84/0.88 thf(f26,negated_conjecture,(
% 3.84/0.88 ~(ivalid @ (iequiv @ (iatom @ p) @ (iatom @ q)))),
% 3.84/0.88 inference(negated_conjecture,[status(cth)],[f25])).
% 3.84/0.88 thf(f27,plain,(
% 3.84/0.88 ! [X0 : $i] : (irel @ X0 @ X0)),
% 3.84/0.88 inference(rectify,[],[f1])).
% 3.84/0.88 thf(f28,plain,(
% 3.84/0.88 ! [X0 : $i] : (((irel @ X0 @ X0)) = $true)),
% 3.84/0.88 inference(fool_elimination,[],[f27])).
% 3.84/0.88 thf(f29,plain,(
% 3.84/0.88 ! [X0 : $i,X1 : $i,X2 : $i] : (((irel @ X1 @ X2) & (irel @ X0 @ X1)) => (irel @ X0 @ X2))),
% 3.84/0.88 inference(rectify,[],[f2])).
% 3.84/0.88 thf(f30,plain,(
% 3.84/0.88 ! [X0 : $i,X1 : $i,X2 : $i] : (((((irel @ X1 @ X2)) = $true) & (((irel @ X0 @ X1)) = $true)) => (((irel @ X0 @ X2)) = $true))),
% 3.84/0.88 inference(fool_elimination,[],[f29])).
% 3.84/0.88 thf(f31,plain,(
% 3.84/0.88 (mnot = (^[X0 : ($i > $o), X1 : $i] : (~(X0 @ X1))))),
% 3.84/0.88 inference(rectify,[],[f3])).
% 3.84/0.88 thf(f32,plain,(
% 3.84/0.88 (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))))),
% 3.84/0.88 inference(fool_elimination,[],[f31])).
% 3.84/0.88 thf(f33,plain,(
% 3.84/0.88 (mor = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X1 @ X2) | (X0 @ X2))))),
% 3.84/0.88 inference(rectify,[],[f4])).
% 3.84/0.88 thf(f34,plain,(
% 3.84/0.88 (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))))),
% 3.84/0.88 inference(fool_elimination,[],[f33])).
% 3.84/0.88 thf(f35,plain,(
% 3.84/0.88 (mand = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X1 @ X2) & (X0 @ X2))))),
% 3.84/0.88 inference(rectify,[],[f5])).
% 3.84/0.88 thf(f36,plain,(
% 3.84/0.88 (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2))))))))),
% 3.84/0.88 inference(fool_elimination,[],[f35])).
% 3.84/0.88 thf(f37,plain,(
% 3.84/0.88 (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mnot @ Y0) @ Y1)))))),
% 3.84/0.88 inference(fool_elimination,[],[f6])).
% 3.84/0.88 thf(f38,plain,(
% 3.84/0.88 (mbox_s4 = (^[X0 : ($i > $o), X1 : $i] : (! [X2 : $i] : ((irel @ X1 @ X2) => (X0 @ X2)))))),
% 3.84/0.88 inference(rectify,[],[f7])).
% 3.84/0.88 thf(f39,plain,(
% 3.84/0.88 (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (Y0 @ Y2))))))))),
% 3.84/0.88 inference(fool_elimination,[],[f38])).
% 3.84/0.88 thf(f40,plain,(
% 3.84/0.88 (iatom = (^[Y0 : $i > $o]: (Y0)))),
% 3.84/0.88 inference(fool_elimination,[],[f8])).
% 3.84/0.88 thf(f43,plain,(
% 3.84/0.88 (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mand @ Y0 @ Y1)))))),
% 3.84/0.88 inference(fool_elimination,[],[f12])).
% 3.84/0.88 thf(f44,plain,(
% 3.84/0.88 (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 3.84/0.88 inference(fool_elimination,[],[f13])).
% 3.84/0.88 thf(f45,plain,(
% 3.84/0.88 (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mimplies @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 3.84/0.88 inference(fool_elimination,[],[f14])).
% 3.84/0.88 thf(f47,plain,(
% 3.84/0.88 (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (iand @ (iimplies @ Y0 @ Y1) @ (iimplies @ Y1 @ Y0))))))),
% 3.84/0.88 inference(fool_elimination,[],[f16])).
% 3.84/0.88 thf(f49,plain,(
% 3.84/0.88 (ivalid = (^[X0 : ($i > $o)] : (! [X1 : $i] : (X0 @ X1))))),
% 3.84/0.88 inference(rectify,[],[f18])).
% 3.84/0.88 thf(f50,plain,(
% 3.84/0.88 (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))),
% 3.84/0.88 inference(fool_elimination,[],[f49])).
% 3.84/0.88 thf(f57,plain,(
% 3.84/0.88 (ivalid @ (iimplies @ (iatom @ q) @ (iatom @ r)))),
% 3.84/0.88 inference(rectify,[],[f22])).
% 3.84/0.88 thf(f58,plain,(
% 3.84/0.88 (((ivalid @ (iimplies @ (iatom @ q) @ (iatom @ r)))) = $true)),
% 3.84/0.88 inference(fool_elimination,[],[f57])).
% 3.84/0.88 thf(f59,plain,(
% 3.84/0.88 (ivalid @ (iimplies @ (iatom @ r) @ (iand @ (iatom @ p) @ (iatom @ q))))),
% 3.84/0.88 inference(rectify,[],[f23])).
% 3.84/0.88 thf(f60,plain,(
% 3.84/0.88 (((ivalid @ (iimplies @ (iatom @ r) @ (iand @ (iatom @ p) @ (iatom @ q))))) = $true)),
% 3.84/0.88 inference(fool_elimination,[],[f59])).
% 3.84/0.88 thf(f61,plain,(
% 3.84/0.88 (ivalid @ (iimplies @ (iatom @ p) @ (ior @ (iatom @ q) @ (iatom @ r))))),
% 3.84/0.88 inference(rectify,[],[f24])).
% 3.84/0.88 thf(f62,plain,(
% 3.84/0.88 (((ivalid @ (iimplies @ (iatom @ p) @ (ior @ (iatom @ q) @ (iatom @ r))))) = $true)),
% 3.84/0.88 inference(fool_elimination,[],[f61])).
% 3.84/0.88 thf(f63,plain,(
% 3.84/0.88 ~(ivalid @ (iequiv @ (iatom @ p) @ (iatom @ q)))),
% 3.84/0.88 inference(rectify,[],[f26])).
% 3.84/0.88 thf(f64,plain,(
% 3.84/0.88 ~ (((ivalid @ (iequiv @ (iatom @ p) @ (iatom @ q)))) = $true)),
% 3.84/0.88 inference(fool_elimination,[],[f63])).
% 3.84/0.88 thf(f65,plain,(
% 3.84/0.88 (((ivalid @ (iequiv @ (iatom @ p) @ (iatom @ q)))) != $true)),
% 3.84/0.88 inference(flattening,[],[f64])).
% 3.84/0.88 thf(f66,plain,(
% 3.84/0.88 ! [X0 : $i,X1 : $i,X2 : $i] : ((((irel @ X0 @ X2)) = $true) | ((((irel @ X1 @ X2)) != $true) | (((irel @ X0 @ X1)) != $true)))),
% 3.84/0.88 inference(ennf_transformation,[],[f30])).
% 3.84/0.88 thf(f67,plain,(
% 3.84/0.88 ! [X0 : $i,X1 : $i,X2 : $i] : ((((irel @ X0 @ X2)) = $true) | (((irel @ X1 @ X2)) != $true) | (((irel @ X0 @ X1)) != $true))),
% 3.84/0.88 inference(flattening,[],[f66])).
% 3.84/0.88 thf(f68,plain,(
% 3.84/0.88 ( ! [X0 : $i] : ((((irel @ X0 @ X0)) = $true)) )),
% 3.84/0.88 inference(cnf_transformation,[],[f28])).
% 3.84/0.88 thf(f69,plain,(
% 3.84/0.88 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((irel @ X1 @ X2)) != $true) | (((irel @ X0 @ X2)) = $true) | (((irel @ X0 @ X1)) != $true)) )),
% 3.84/0.88 inference(cnf_transformation,[],[f67])).
% 3.84/0.88 thf(f70,plain,(
% 3.84/0.88 (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))))),
% 3.84/0.88 inference(cnf_transformation,[],[f32])).
% 3.84/0.88 thf(f71,plain,(
% 3.84/0.88 (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))))),
% 3.84/0.88 inference(cnf_transformation,[],[f34])).
% 3.84/0.88 thf(f72,plain,(
% 3.84/0.88 (mand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) & (Y1 @ Y2))))))))),
% 3.84/0.88 inference(cnf_transformation,[],[f36])).
% 3.84/0.88 thf(f73,plain,(
% 3.84/0.88 (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mnot @ Y0) @ Y1)))))),
% 3.84/0.88 inference(cnf_transformation,[],[f37])).
% 3.84/0.88 thf(f74,plain,(
% 3.84/0.88 (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (Y0 @ Y2))))))))),
% 3.84/0.88 inference(cnf_transformation,[],[f39])).
% 3.84/0.88 thf(f75,plain,(
% 3.84/0.88 (iatom = (^[Y0 : $i > $o]: (Y0)))),
% 3.84/0.88 inference(cnf_transformation,[],[f40])).
% 3.84/0.88 thf(f79,plain,(
% 3.84/0.88 (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mand @ Y0 @ Y1)))))),
% 3.84/0.88 inference(cnf_transformation,[],[f43])).
% 3.84/0.88 thf(f80,plain,(
% 3.84/0.88 (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 3.84/0.88 inference(cnf_transformation,[],[f44])).
% 3.84/0.88 thf(f81,plain,(
% 3.84/0.88 (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mimplies @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 3.84/0.88 inference(cnf_transformation,[],[f45])).
% 3.84/0.88 thf(f83,plain,(
% 3.84/0.88 (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (iand @ (iimplies @ Y0 @ Y1) @ (iimplies @ Y1 @ Y0))))))),
% 3.84/0.88 inference(cnf_transformation,[],[f47])).
% 3.84/0.88 thf(f85,plain,(
% 3.84/0.88 (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))),
% 3.84/0.88 inference(cnf_transformation,[],[f50])).
% 3.84/0.88 thf(f89,plain,(
% 3.84/0.88 (((ivalid @ (iimplies @ (iatom @ q) @ (iatom @ r)))) = $true)),
% 3.84/0.88 inference(cnf_transformation,[],[f58])).
% 3.84/0.88 thf(f90,plain,(
% 3.84/0.88 (((ivalid @ (iimplies @ (iatom @ r) @ (iand @ (iatom @ p) @ (iatom @ q))))) = $true)),
% 3.84/0.88 inference(cnf_transformation,[],[f60])).
% 3.84/0.88 thf(f91,plain,(
% 3.84/0.88 (((ivalid @ (iimplies @ (iatom @ p) @ (ior @ (iatom @ q) @ (iatom @ r))))) = $true)),
% 3.84/0.88 inference(cnf_transformation,[],[f62])).
% 3.84/0.88 thf(f92,plain,(
% 3.84/0.88 (((ivalid @ (iequiv @ (iatom @ p) @ (iatom @ q)))) != $true)),
% 3.84/0.88 inference(cnf_transformation,[],[f65])).
% 3.84/0.88 thf(f94,definition,(
% 3.84/0.88 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 3.84/0.88 introduced(theory,[fool_exhaustiveness_axiom])).
% 3.84/0.88 thf(f95,plain,(
% 3.84/0.88 (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) | (Y3 @ Y4))))))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i]: (~ (Y2 @ Y3))))) @ Y0) @ Y1)))))),
% 3.84/0.88 inference(definition_unfolding,[],[f73,f71,f70])).
% 3.84/0.88 thf(f98,plain,(
% 3.84/0.88 (iand = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) & (Y3 @ Y4))))))) @ Y0 @ Y1)))))),
% 3.84/0.88 inference(definition_unfolding,[],[f79,f72])).
% 3.84/0.88 thf(f99,plain,(
% 3.84/0.88 (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))))))),
% 3.84/0.88 inference(definition_unfolding,[],[f80,f71,f74,f74])).
% 3.84/0.88 thf(f100,plain,(
% 3.84/0.88 (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: ((Y4 @ Y6) | (Y5 @ Y6))))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y2) @ Y3)))) @ ((^[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))))))),
% 3.84/0.88 inference(definition_unfolding,[],[f81,f95,f74,f74])).
% 3.84/0.88 thf(f102,plain,(
% 3.84/0.88 (iequiv = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: ((Y4 @ Y6) & (Y5 @ Y6))))))) @ Y2 @ Y3)))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i > $o]: ((^[Y7 : $i > $o]: ((^[Y8 : $i]: ((Y6 @ Y8) | (Y7 @ Y8))))))) @ ((^[Y6 : $i > $o]: ((^[Y7 : $i]: (~ (Y6 @ Y7))))) @ Y4) @ Y5)))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((irel @ Y5 @ Y6) => (Y4 @ Y6))))))) @ Y2) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((irel @ Y5 @ Y6) => (Y4 @ Y6))))))) @ Y3))))) @ Y0 @ Y1) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i > $o]: ((^[Y7 : $i > $o]: ((^[Y8 : $i]: ((Y6 @ Y8) | (Y7 @ Y8))))))) @ ((^[Y6 : $i > $o]: ((^[Y7 : $i]: (~ (Y6 @ Y7))))) @ Y4) @ Y5)))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((irel @ Y5 @ Y6) => (Y4 @ Y6))))))) @ Y2) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((irel @ Y5 @ Y6) => (Y4 @ Y6))))))) @ Y3))))) @ Y1 @ Y0))))))),
% 3.84/0.88 inference(definition_unfolding,[],[f83,f98,f100,f100])).
% 3.84/0.88 thf(f104,plain,(
% 3.84/0.88 ($true = (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: ((Y4 @ Y6) | (Y5 @ Y6))))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y2) @ Y3)))) @ ((^[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)) @ q) @ ((^[Y0 : $i > $o]: (Y0)) @ r)))))),
% 3.84/0.88 inference(definition_unfolding,[],[f89,f85,f100,f75,f75])).
% 3.84/0.88 thf(f105,plain,(
% 3.84/0.88 ($true = (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: ((Y4 @ Y6) | (Y5 @ Y6))))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y2) @ Y3)))) @ ((^[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)) @ r) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i]: ((Y2 @ Y4) & (Y3 @ Y4))))))) @ Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: (Y0)) @ p) @ ((^[Y0 : $i > $o]: (Y0)) @ q))))))),
% 3.84/0.88 inference(definition_unfolding,[],[f90,f85,f100,f75,f98,f75,f75])).
% 3.84/0.88 thf(f106,plain,(
% 3.84/0.88 ($true = (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: ((Y4 @ Y6) | (Y5 @ Y6))))))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (~ (Y4 @ Y5))))) @ Y2) @ Y3)))) @ ((^[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)) @ p) @ ((^[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)) @ q) @ ((^[Y0 : $i > $o]: (Y0)) @ r))))))),
% 3.84/0.88 inference(definition_unfolding,[],[f91,f85,f100,f75,f99,f75,f75])).
% 3.84/0.88 thf(f107,plain,(
% 3.84/0.88 ($true != (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i]: ((Y4 @ Y6) & (Y5 @ Y6))))))) @ Y2 @ Y3)))) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i > $o]: ((^[Y7 : $i > $o]: ((^[Y8 : $i]: ((Y6 @ Y8) | (Y7 @ Y8))))))) @ ((^[Y6 : $i > $o]: ((^[Y7 : $i]: (~ (Y6 @ Y7))))) @ Y4) @ Y5)))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((irel @ Y5 @ Y6) => (Y4 @ Y6))))))) @ Y2) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((irel @ Y5 @ Y6) => (Y4 @ Y6))))))) @ Y3))))) @ Y0 @ Y1) @ ((^[Y2 : $i > $o]: ((^[Y3 : $i > $o]: ((^[Y4 : $i > $o]: ((^[Y5 : $i > $o]: ((^[Y6 : $i > $o]: ((^[Y7 : $i > $o]: ((^[Y8 : $i]: ((Y6 @ Y8) | (Y7 @ Y8))))))) @ ((^[Y6 : $i > $o]: ((^[Y7 : $i]: (~ (Y6 @ Y7))))) @ Y4) @ Y5)))) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((irel @ Y5 @ Y6) => (Y4 @ Y6))))))) @ Y2) @ ((^[Y4 : $i > $o]: ((^[Y5 : $i]: (!! @ $i @ (^[Y6 : $i]: ((irel @ Y5 @ Y6) => (Y4 @ Y6))))))) @ Y3))))) @ Y1 @ Y0))))) @ ((^[Y0 : $i > $o]: (Y0)) @ p) @ ((^[Y0 : $i > $o]: (Y0)) @ q)))))),
% 3.84/0.88 inference(definition_unfolding,[],[f92,f85,f102,f75,f75])).
% 3.84/0.88 thf(f108,plain,(
% 3.84/0.88 ($true != ((!! @ $i @ (^[Y0 : $i]: (((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (q @ Y1))))) & ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (q @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p @ Y1))))))))))),
% 3.84/0.88 inference(beta-eta_normalization,[],[f107])).
% 3.84/0.88 thf(f109,plain,(
% 3.84/0.88 ($false = (((^[Y0 : $i]: (((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (q @ Y1))))) & ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (q @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p @ Y1))))))) @ sK0)))),
% 3.84/0.88 inference(sigma_proxy_clausification,[],[f108])).
% 3.84/0.88 thf(f110,plain,(
% 3.84/0.88 ($false = ((((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (p @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (q @ Y0))))) & ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (q @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (p @ Y0))))))))),
% 3.84/0.88 inference(beta-eta_normalization,[],[f109])).
% 3.84/0.88 thf(f111,plain,(
% 3.84/0.88 ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (q @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (p @ Y0))))))) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (p @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (q @ Y0)))))))),
% 3.84/0.88 inference(and_proxy_clausification,[],[f110])).
% 3.84/0.88 thf(f112,plain,(
% 3.84/0.88 ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (p @ Y0)))))) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (p @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (q @ Y0)))))))),
% 3.84/0.88 inference(or_proxy_clausification,[],[f111])).
% 3.84/0.88 thf(f113,plain,(
% 3.84/0.88 ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (q @ Y0))))))) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (p @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (q @ Y0)))))))),
% 3.84/0.88 inference(or_proxy_clausification,[],[f111])).
% 3.84/0.88 thf(f114,plain,(
% 3.84/0.88 ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (q @ Y0)))))) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (p @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (q @ Y0)))))))),
% 3.84/0.88 inference(not_proxy_clausification,[],[f113])).
% 3.84/0.88 thf(f115,plain,(
% 3.84/0.88 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ sK0 @ Y0) => (q @ Y0))) @ X1))) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (p @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (q @ Y0)))))))) )),
% 3.84/0.88 inference(pi_proxy_clausification,[],[f114])).
% 3.84/0.88 thf(f116,plain,(
% 3.84/0.88 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ sK0 @ Y0) => (q @ Y0))) @ X1))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (q @ Y0))))))) )),
% 3.84/0.88 inference(or_proxy_clausification,[],[f115])).
% 3.84/0.88 thf(f117,plain,(
% 3.84/0.88 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ sK0 @ Y0) => (q @ Y0))) @ X1))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (p @ Y0)))))))) )),
% 3.84/0.88 inference(or_proxy_clausification,[],[f115])).
% 3.84/0.88 thf(f118,plain,(
% 3.84/0.88 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ sK0 @ Y0) => (q @ Y0))) @ X1))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (p @ Y0))))))) )),
% 3.84/0.88 inference(not_proxy_clausification,[],[f117])).
% 3.84/0.88 thf(f119,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ sK0 @ Y0) => (q @ Y0))) @ X1))) | ($true = (((^[Y0 : $i]: ((irel @ sK0 @ Y0) => (p @ Y0))) @ X2)))) )),
% 3.84/0.88 inference(pi_proxy_clausification,[],[f118])).
% 3.84/0.88 thf(f120,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : (($true = (((irel @ sK0 @ X1) => (q @ X1)))) | ($true = (((irel @ sK0 @ X2) => (p @ X2))))) )),
% 3.84/0.88 inference(beta-eta_normalization,[],[f119])).
% 3.84/0.88 thf(f121,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = (((irel @ sK0 @ X2) => (p @ X2)))) | ($true = ((q @ X1)))) )),
% 3.84/0.88 inference(imp_proxy_clausification,[],[f120])).
% 3.84/0.88 thf(f122,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($false = ((irel @ sK0 @ X2))) | ($true = ((q @ X1))) | ($true = ((p @ X2)))) )),
% 3.84/0.88 inference(imp_proxy_clausification,[],[f121])).
% 3.84/0.88 thf(f123,plain,(
% 3.84/0.88 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ sK0 @ Y0) => (q @ Y0))) @ X1))) | ($false = (((^[Y0 : $i]: ((irel @ sK0 @ Y0) => (q @ Y0))) @ sK1)))) )),
% 3.84/0.88 inference(sigma_proxy_clausification,[],[f116])).
% 3.84/0.88 thf(f124,plain,(
% 3.84/0.88 ( ! [X1 : $i] : (($true = (((irel @ sK0 @ X1) => (q @ X1)))) | ($false = (((irel @ sK0 @ sK1) => (q @ sK1))))) )),
% 3.84/0.88 inference(beta-eta_normalization,[],[f123])).
% 3.84/0.88 thf(f125,plain,(
% 3.84/0.88 ( ! [X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($false = (((irel @ sK0 @ sK1) => (q @ sK1)))) | ($true = ((q @ X1)))) )),
% 3.84/0.88 inference(imp_proxy_clausification,[],[f124])).
% 3.84/0.88 thf(f126,plain,(
% 3.84/0.88 ( ! [X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($false = ((q @ sK1))) | ($true = ((q @ X1)))) )),
% 3.84/0.88 inference(imp_proxy_clausification,[],[f125])).
% 3.84/0.88 thf(f127,plain,(
% 3.84/0.88 ( ! [X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = ((irel @ sK0 @ sK1))) | ($true = ((q @ X1)))) )),
% 3.84/0.88 inference(imp_proxy_clausification,[],[f125])).
% 3.84/0.88 thf(f128,plain,(
% 3.84/0.88 ($false = (((^[Y0 : $i]: ((irel @ sK0 @ Y0) => (p @ Y0))) @ sK2))) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (p @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (q @ Y0)))))))),
% 3.84/0.88 inference(sigma_proxy_clausification,[],[f112])).
% 3.84/0.88 thf(f129,plain,(
% 3.84/0.88 ($false = (((^[Y0 : $i]: ((irel @ sK0 @ Y0) => (p @ Y0))) @ sK2))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (q @ Y0))))))),
% 3.84/0.88 inference(or_proxy_clausification,[],[f128])).
% 3.84/0.88 thf(f130,plain,(
% 3.84/0.88 ($false = (((^[Y0 : $i]: ((irel @ sK0 @ Y0) => (p @ Y0))) @ sK2))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (p @ Y0)))))))),
% 3.84/0.88 inference(or_proxy_clausification,[],[f128])).
% 3.84/0.88 thf(f131,plain,(
% 3.84/0.88 ($false = (((^[Y0 : $i]: ((irel @ sK0 @ Y0) => (p @ Y0))) @ sK2))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ sK0 @ Y0) => (p @ Y0))))))),
% 3.84/0.88 inference(not_proxy_clausification,[],[f130])).
% 3.84/0.88 thf(f132,plain,(
% 3.84/0.88 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((irel @ sK0 @ Y0) => (p @ Y0))) @ sK2))) | ($true = (((^[Y0 : $i]: ((irel @ sK0 @ Y0) => (p @ Y0))) @ X1)))) )),
% 3.84/0.88 inference(pi_proxy_clausification,[],[f131])).
% 3.84/0.88 thf(f133,plain,(
% 3.84/0.88 ( ! [X1 : $i] : (($false = (((irel @ sK0 @ sK2) => (p @ sK2)))) | ($true = (((irel @ sK0 @ X1) => (p @ X1))))) )),
% 3.84/0.88 inference(beta-eta_normalization,[],[f132])).
% 3.84/0.88 thf(f134,plain,(
% 3.84/0.88 ( ! [X1 : $i] : (($false = ((p @ sK2))) | ($true = (((irel @ sK0 @ X1) => (p @ X1))))) )),
% 3.84/0.88 inference(imp_proxy_clausification,[],[f133])).
% 3.84/0.88 thf(f135,plain,(
% 3.84/0.88 ( ! [X1 : $i] : (($true = ((irel @ sK0 @ sK2))) | ($true = (((irel @ sK0 @ X1) => (p @ X1))))) )),
% 3.84/0.88 inference(imp_proxy_clausification,[],[f133])).
% 3.84/0.88 thf(f136,plain,(
% 3.84/0.88 ( ! [X1 : $i] : (($true = ((irel @ sK0 @ sK2))) | ($false = ((irel @ sK0 @ X1))) | ($true = ((p @ X1)))) )),
% 3.84/0.88 inference(imp_proxy_clausification,[],[f135])).
% 3.84/0.88 thf(f137,plain,(
% 3.84/0.88 ( ! [X1 : $i] : (($false = ((p @ sK2))) | ($false = ((irel @ sK0 @ X1))) | ($true = ((p @ X1)))) )),
% 3.84/0.88 inference(imp_proxy_clausification,[],[f134])).
% 3.84/0.88 thf(f138,plain,(
% 3.84/0.88 ($false = (((^[Y0 : $i]: ((irel @ sK0 @ Y0) => (p @ Y0))) @ sK2))) | ($false = (((^[Y0 : $i]: ((irel @ sK0 @ Y0) => (q @ Y0))) @ sK3)))),
% 3.84/0.88 inference(sigma_proxy_clausification,[],[f129])).
% 3.84/0.88 thf(f139,plain,(
% 3.84/0.88 ($false = (((irel @ sK0 @ sK2) => (p @ sK2)))) | ($false = (((irel @ sK0 @ sK3) => (q @ sK3))))),
% 3.84/0.88 inference(beta-eta_normalization,[],[f138])).
% 3.84/0.88 thf(f140,plain,(
% 3.84/0.88 ($false = ((p @ sK2))) | ($false = (((irel @ sK0 @ sK3) => (q @ sK3))))),
% 3.84/0.88 inference(imp_proxy_clausification,[],[f139])).
% 3.84/0.88 thf(f141,plain,(
% 3.84/0.88 ($true = ((irel @ sK0 @ sK2))) | ($false = (((irel @ sK0 @ sK3) => (q @ sK3))))),
% 3.84/0.88 inference(imp_proxy_clausification,[],[f139])).
% 3.84/0.88 thf(f142,plain,(
% 3.84/0.88 ($true = ((irel @ sK0 @ sK2))) | ($false = ((q @ sK3)))),
% 3.84/0.88 inference(imp_proxy_clausification,[],[f141])).
% 3.84/0.88 thf(f143,plain,(
% 3.84/0.88 ($true = ((irel @ sK0 @ sK2))) | ($true = ((irel @ sK0 @ sK3)))),
% 3.84/0.88 inference(imp_proxy_clausification,[],[f141])).
% 3.84/0.88 thf(f144,plain,(
% 3.84/0.88 ($false = ((p @ sK2))) | ($false = ((q @ sK3)))),
% 3.84/0.88 inference(imp_proxy_clausification,[],[f140])).
% 3.84/0.88 thf(f145,plain,(
% 3.84/0.88 ($false = ((p @ sK2))) | ($true = ((irel @ sK0 @ sK3)))),
% 3.84/0.88 inference(imp_proxy_clausification,[],[f140])).
% 3.84/0.88 thf(f146,plain,(
% 3.84/0.88 ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (q @ Y2)))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (r @ Y2)))))))))))))),
% 3.84/0.88 inference(beta-eta_normalization,[],[f106])).
% 3.84/0.88 thf(f147,plain,(
% 3.84/0.88 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (q @ Y2)))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (r @ Y2)))))))))) @ X1)))) )),
% 3.84/0.88 inference(pi_proxy_clausification,[],[f146])).
% 3.84/0.88 thf(f148,plain,(
% 3.84/0.88 ( ! [X1 : $i] : (($true = (((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (q @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (r @ Y1)))))))))))) )),
% 3.84/0.88 inference(beta-eta_normalization,[],[f147])).
% 3.84/0.88 thf(f149,plain,(
% 3.84/0.88 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (q @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (r @ Y1)))))))))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p @ Y0)))))))) )),
% 3.84/0.88 inference(or_proxy_clausification,[],[f148])).
% 3.84/0.88 thf(f150,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (q @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (r @ Y1))))))) @ X2))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p @ Y0)))))))) )),
% 3.84/0.88 inference(pi_proxy_clausification,[],[f149])).
% 3.84/0.88 thf(f151,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (q @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (r @ Y1))))))) @ X2))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (p @ Y0))))))) )),
% 3.84/0.88 inference(not_proxy_clausification,[],[f150])).
% 3.84/0.88 thf(f152,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (q @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (r @ Y1))))))) @ X2))) | ($false = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (p @ Y0))) @ (sK4 @ X1))))) )),
% 3.84/0.88 inference(sigma_proxy_clausification,[],[f151])).
% 3.84/0.88 thf(f153,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : (($true = (((irel @ X1 @ X2) => ((!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => (q @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => (r @ Y0)))))))) | ($false = (((irel @ X1 @ (sK4 @ X1)) => (p @ (sK4 @ X1)))))) )),
% 3.84/0.88 inference(beta-eta_normalization,[],[f152])).
% 3.84/0.88 thf(f154,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = (((irel @ X1 @ (sK4 @ X1)) => (p @ (sK4 @ X1))))) | ($true = (((!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => (q @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => (r @ Y0)))))))) )),
% 3.84/0.88 inference(imp_proxy_clausification,[],[f153])).
% 3.84/0.88 thf(f155,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((p @ (sK4 @ X1)))) | ($true = (((!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => (q @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => (r @ Y0)))))))) )),
% 3.84/0.88 inference(imp_proxy_clausification,[],[f154])).
% 3.84/0.88 thf(f156,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = ((irel @ X1 @ (sK4 @ X1)))) | ($true = (((!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => (q @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => (r @ Y0)))))))) )),
% 3.84/0.88 inference(imp_proxy_clausification,[],[f154])).
% 3.84/0.88 thf(f157,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = ((irel @ X1 @ (sK4 @ X1)))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => (r @ Y0)))))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => (q @ Y0))))))) )),
% 3.84/0.88 inference(or_proxy_clausification,[],[f156])).
% 3.84/0.88 thf(f158,plain,(
% 3.84/0.88 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = ((irel @ X1 @ (sK4 @ X1)))) | ($true = (((^[Y0 : $i]: ((irel @ X2 @ Y0) => (r @ Y0))) @ X3))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => (q @ Y0))))))) )),
% 3.84/0.88 inference(pi_proxy_clausification,[],[f157])).
% 3.84/0.88 thf(f159,plain,(
% 3.84/0.88 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = ((irel @ X1 @ (sK4 @ X1)))) | ($true = (((^[Y0 : $i]: ((irel @ X2 @ Y0) => (r @ Y0))) @ X3))) | ($true = (((^[Y0 : $i]: ((irel @ X2 @ Y0) => (q @ Y0))) @ X4)))) )),
% 3.84/0.88 inference(pi_proxy_clausification,[],[f158])).
% 3.84/0.88 thf(f160,plain,(
% 3.84/0.88 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = ((irel @ X1 @ (sK4 @ X1)))) | ($true = (((irel @ X2 @ X3) => (r @ X3)))) | ($true = (((irel @ X2 @ X4) => (q @ X4))))) )),
% 3.84/0.88 inference(beta-eta_normalization,[],[f159])).
% 3.84/0.88 thf(f161,plain,(
% 3.84/0.88 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = ((irel @ X1 @ (sK4 @ X1)))) | ($false = ((irel @ X2 @ X3))) | ($true = (((irel @ X2 @ X4) => (q @ X4)))) | ($true = ((r @ X3)))) )),
% 3.84/0.88 inference(imp_proxy_clausification,[],[f160])).
% 3.84/0.88 thf(f162,plain,(
% 3.84/0.88 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((irel @ X1 @ (sK4 @ X1)))) | ($false = ((irel @ X2 @ X4))) | ($false = ((irel @ X2 @ X3))) | (((irel @ X1 @ X2)) = $false) | ($true = ((r @ X3))) | ($true = ((q @ X4)))) )),
% 3.84/0.88 inference(imp_proxy_clausification,[],[f161])).
% 3.84/0.88 thf(f163,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((p @ (sK4 @ X1)))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => (r @ Y0)))))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => (q @ Y0))))))) )),
% 3.84/0.88 inference(or_proxy_clausification,[],[f155])).
% 3.84/0.88 thf(f164,plain,(
% 3.84/0.88 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((p @ (sK4 @ X1)))) | ($true = (((^[Y0 : $i]: ((irel @ X2 @ Y0) => (r @ Y0))) @ X3))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X2 @ Y0) => (q @ Y0))))))) )),
% 3.84/0.88 inference(pi_proxy_clausification,[],[f163])).
% 3.84/0.88 thf(f165,plain,(
% 3.84/0.88 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((p @ (sK4 @ X1)))) | ($true = (((^[Y0 : $i]: ((irel @ X2 @ Y0) => (r @ Y0))) @ X3))) | ($true = (((^[Y0 : $i]: ((irel @ X2 @ Y0) => (q @ Y0))) @ X4)))) )),
% 3.84/0.88 inference(pi_proxy_clausification,[],[f164])).
% 3.84/0.88 thf(f166,plain,(
% 3.84/0.88 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((p @ (sK4 @ X1)))) | ($true = (((irel @ X2 @ X3) => (r @ X3)))) | ($true = (((irel @ X2 @ X4) => (q @ X4))))) )),
% 3.84/0.88 inference(beta-eta_normalization,[],[f165])).
% 3.84/0.88 thf(f167,plain,(
% 3.84/0.88 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((p @ (sK4 @ X1)))) | ($false = ((irel @ X2 @ X3))) | ($true = (((irel @ X2 @ X4) => (q @ X4)))) | ($true = ((r @ X3)))) )),
% 3.84/0.88 inference(imp_proxy_clausification,[],[f166])).
% 3.84/0.88 thf(f168,plain,(
% 3.84/0.88 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((irel @ X2 @ X4))) | ($false = ((irel @ X2 @ X3))) | (((irel @ X1 @ X2)) = $false) | ($false = ((p @ (sK4 @ X1)))) | ($true = ((r @ X3))) | ($true = ((q @ X4)))) )),
% 3.84/0.88 inference(imp_proxy_clausification,[],[f167])).
% 3.84/0.88 thf(f169,plain,(
% 3.84/0.88 ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (r @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((p @ Y1) & (q @ Y1))))))))))),
% 3.84/0.88 inference(beta-eta_normalization,[],[f105])).
% 3.84/0.88 thf(f170,plain,(
% 3.84/0.88 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (r @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((p @ Y1) & (q @ Y1))))))) @ X1)))) )),
% 3.84/0.88 inference(pi_proxy_clausification,[],[f169])).
% 3.84/0.88 thf(f171,plain,(
% 3.84/0.88 ( ! [X1 : $i] : (($true = (((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (r @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => ((p @ Y0) & (q @ Y0))))))))) )),
% 3.84/0.88 inference(beta-eta_normalization,[],[f170])).
% 3.84/0.88 thf(f172,plain,(
% 3.84/0.88 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => ((p @ Y0) & (q @ Y0))))))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (r @ Y0)))))))) )),
% 3.84/0.88 inference(or_proxy_clausification,[],[f171])).
% 3.84/0.88 thf(f173,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => ((p @ Y0) & (q @ Y0)))) @ X2))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (r @ Y0)))))))) )),
% 3.84/0.88 inference(pi_proxy_clausification,[],[f172])).
% 3.84/0.88 thf(f174,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => ((p @ Y0) & (q @ Y0)))) @ X2))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (r @ Y0))))))) )),
% 3.84/0.88 inference(not_proxy_clausification,[],[f173])).
% 3.84/0.88 thf(f175,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => ((p @ Y0) & (q @ Y0)))) @ X2))) | ($false = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (r @ Y0))) @ (sK5 @ X1))))) )),
% 3.84/0.88 inference(sigma_proxy_clausification,[],[f174])).
% 3.84/0.88 thf(f176,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : (($true = (((irel @ X1 @ X2) => ((p @ X2) & (q @ X2))))) | ($false = (((irel @ X1 @ (sK5 @ X1)) => (r @ (sK5 @ X1)))))) )),
% 3.84/0.88 inference(beta-eta_normalization,[],[f175])).
% 3.84/0.88 thf(f177,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = (((irel @ X1 @ (sK5 @ X1)) => (r @ (sK5 @ X1))))) | ($true = (((p @ X2) & (q @ X2))))) )),
% 3.84/0.88 inference(imp_proxy_clausification,[],[f176])).
% 3.84/0.88 thf(f178,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((r @ (sK5 @ X1)))) | ($true = (((p @ X2) & (q @ X2))))) )),
% 3.84/0.88 inference(imp_proxy_clausification,[],[f177])).
% 3.84/0.88 thf(f179,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = ((irel @ X1 @ (sK5 @ X1)))) | ($true = (((p @ X2) & (q @ X2))))) )),
% 3.84/0.88 inference(imp_proxy_clausification,[],[f177])).
% 3.84/0.88 thf(f180,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : (($true = ((irel @ X1 @ (sK5 @ X1)))) | (((irel @ X1 @ X2)) = $false) | ($true = ((q @ X2)))) )),
% 3.84/0.88 inference(and_proxy_clausification,[],[f179])).
% 3.84/0.88 thf(f181,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : (($true = ((irel @ X1 @ (sK5 @ X1)))) | (((irel @ X1 @ X2)) = $false) | ($true = ((p @ X2)))) )),
% 3.84/0.88 inference(and_proxy_clausification,[],[f179])).
% 3.84/0.88 thf(f182,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((r @ (sK5 @ X1)))) | ($true = ((q @ X2)))) )),
% 3.84/0.88 inference(and_proxy_clausification,[],[f178])).
% 3.84/0.88 thf(f183,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((r @ (sK5 @ X1)))) | ($true = ((p @ X2)))) )),
% 3.84/0.88 inference(and_proxy_clausification,[],[f178])).
% 3.84/0.88 thf(f184,plain,(
% 3.84/0.88 ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (q @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (r @ Y1)))))))))),
% 3.84/0.88 inference(beta-eta_normalization,[],[f104])).
% 3.84/0.88 thf(f185,plain,(
% 3.84/0.88 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (q @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (r @ Y1)))))) @ X1)))) )),
% 3.84/0.88 inference(pi_proxy_clausification,[],[f184])).
% 3.84/0.88 thf(f186,plain,(
% 3.84/0.88 ( ! [X1 : $i] : (($true = (((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (q @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (r @ Y0)))))))) )),
% 3.84/0.88 inference(beta-eta_normalization,[],[f185])).
% 3.84/0.88 thf(f187,plain,(
% 3.84/0.88 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (r @ Y0)))))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (q @ Y0)))))))) )),
% 3.84/0.88 inference(or_proxy_clausification,[],[f186])).
% 3.84/0.88 thf(f188,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (r @ Y0))) @ X2))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (q @ Y0)))))))) )),
% 3.84/0.88 inference(pi_proxy_clausification,[],[f187])).
% 3.84/0.88 thf(f189,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (r @ Y0))) @ X2))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (q @ Y0))))))) )),
% 3.84/0.88 inference(not_proxy_clausification,[],[f188])).
% 3.84/0.88 thf(f190,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (r @ Y0))) @ X2))) | ($false = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (q @ Y0))) @ (sK6 @ X1))))) )),
% 3.84/0.88 inference(sigma_proxy_clausification,[],[f189])).
% 3.84/0.88 thf(f191,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : (($true = (((irel @ X1 @ X2) => (r @ X2)))) | ($false = (((irel @ X1 @ (sK6 @ X1)) => (q @ (sK6 @ X1)))))) )),
% 3.84/0.88 inference(beta-eta_normalization,[],[f190])).
% 3.84/0.88 thf(f192,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = (((irel @ X1 @ (sK6 @ X1)) => (q @ (sK6 @ X1))))) | ($true = ((r @ X2)))) )),
% 3.84/0.88 inference(imp_proxy_clausification,[],[f191])).
% 3.84/0.88 thf(f193,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((q @ (sK6 @ X1)))) | ($true = ((r @ X2)))) )),
% 3.84/0.88 inference(imp_proxy_clausification,[],[f192])).
% 3.84/0.88 thf(f194,plain,(
% 3.84/0.88 ( ! [X2 : $i,X1 : $i] : (($true = ((irel @ X1 @ (sK6 @ X1)))) | (((irel @ X1 @ X2)) = $false) | ($true = ((r @ X2)))) )),
% 3.84/0.88 inference(imp_proxy_clausification,[],[f192])).
% 3.84/0.88 thf(f196,definition,(
% 3.84/0.88 spl7_1 <=> ! [X2 : $i] : (($false = ((irel @ sK0 @ X2))) | ($true = ((p @ X2))))),
% 3.84/0.88 introduced(definition,[new_symbols(definition,[spl7_1])],[avatar_definition])).
% 3.84/0.88 thf(f197,plain,(
% 3.84/0.88 ( ! [X2 : $i] : (($false = ((irel @ sK0 @ X2))) | ($true = ((p @ X2)))) ) | ~spl7_1),
% 3.84/0.88 inference(avatar_component_clause,[],[f196])).
% 3.84/0.88 thf(f199,definition,(
% 3.84/0.88 spl7_2 <=> ! [X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = ((q @ X1))))),
% 3.84/0.88 introduced(definition,[new_symbols(definition,[spl7_2])],[avatar_definition])).
% 3.84/0.88 thf(f200,plain,(
% 3.84/0.88 ( ! [X1 : $i] : (($false = ((irel @ sK0 @ X1))) | ($true = ((q @ X1)))) ) | ~spl7_2),
% 3.84/0.88 inference(avatar_component_clause,[],[f199])).
% 3.84/0.88 thf(f201,plain,(
% 3.84/0.88 spl7_1 | spl7_2),
% 3.84/0.88 inference(avatar_split_clause,[],[f122,f199,f196])).
% 3.84/0.88 thf(f203,definition,(
% 3.84/0.88 spl7_3 <=> ($true = ((irel @ sK0 @ sK1)))),
% 3.84/0.88 introduced(definition,[new_symbols(definition,[spl7_3])],[avatar_definition])).
% 3.84/0.88 thf(f205,plain,(
% 3.84/0.88 ($true = ((irel @ sK0 @ sK1))) | ~spl7_3),
% 3.84/0.88 inference(avatar_component_clause,[],[f203])).
% 3.84/0.88 thf(f206,plain,(
% 3.84/0.88 spl7_3 | spl7_2),
% 3.84/0.88 inference(avatar_split_clause,[],[f127,f199,f203])).
% 3.84/0.88 thf(f208,definition,(
% 3.84/0.88 spl7_4 <=> ($false = ((q @ sK1)))),
% 3.84/0.88 introduced(definition,[new_symbols(definition,[spl7_4])],[avatar_definition])).
% 3.84/0.88 thf(f210,plain,(
% 3.84/0.88 ($false = ((q @ sK1))) | ~spl7_4),
% 3.84/0.88 inference(avatar_component_clause,[],[f208])).
% 3.84/0.88 thf(f211,plain,(
% 3.84/0.88 spl7_4 | spl7_2),
% 3.84/0.88 inference(avatar_split_clause,[],[f126,f199,f208])).
% 3.84/0.88 thf(f213,definition,(
% 3.84/0.88 spl7_5 <=> ($true = ((irel @ sK0 @ sK2)))),
% 3.84/0.88 introduced(definition,[new_symbols(definition,[spl7_5])],[avatar_definition])).
% 3.84/0.88 thf(f215,plain,(
% 3.84/0.88 ($true = ((irel @ sK0 @ sK2))) | ~spl7_5),
% 3.84/0.88 inference(avatar_component_clause,[],[f213])).
% 3.84/0.88 thf(f216,plain,(
% 3.84/0.88 spl7_1 | spl7_5),
% 3.84/0.88 inference(avatar_split_clause,[],[f136,f213,f196])).
% 3.84/0.88 thf(f218,definition,(
% 3.84/0.88 spl7_6 <=> ($false = ((p @ sK2)))),
% 3.84/0.88 introduced(definition,[new_symbols(definition,[spl7_6])],[avatar_definition])).
% 3.84/0.88 thf(f220,plain,(
% 3.84/0.88 ($false = ((p @ sK2))) | ~spl7_6),
% 3.84/0.88 inference(avatar_component_clause,[],[f218])).
% 3.84/0.88 thf(f221,plain,(
% 3.84/0.88 spl7_1 | spl7_6),
% 3.84/0.88 inference(avatar_split_clause,[],[f137,f218,f196])).
% 3.84/0.88 thf(f223,definition,(
% 3.84/0.88 spl7_7 <=> ($true = ((irel @ sK0 @ sK3)))),
% 3.84/0.88 introduced(definition,[new_symbols(definition,[spl7_7])],[avatar_definition])).
% 3.84/0.88 thf(f225,plain,(
% 3.84/0.88 ($true = ((irel @ sK0 @ sK3))) | ~spl7_7),
% 3.84/0.88 inference(avatar_component_clause,[],[f223])).
% 3.84/0.88 thf(f226,plain,(
% 3.84/0.88 spl7_7 | spl7_5),
% 3.84/0.88 inference(avatar_split_clause,[],[f143,f213,f223])).
% 3.84/0.88 thf(f228,definition,(
% 3.84/0.88 spl7_8 <=> ($false = ((q @ sK3)))),
% 3.84/0.88 introduced(definition,[new_symbols(definition,[spl7_8])],[avatar_definition])).
% 3.84/0.88 thf(f230,plain,(
% 3.84/0.88 ($false = ((q @ sK3))) | ~spl7_8),
% 3.84/0.88 inference(avatar_component_clause,[],[f228])).
% 3.84/0.88 thf(f231,plain,(
% 3.84/0.88 spl7_8 | spl7_5),
% 3.84/0.88 inference(avatar_split_clause,[],[f142,f213,f228])).
% 3.84/0.88 thf(f232,plain,(
% 3.84/0.88 spl7_7 | spl7_6),
% 3.84/0.88 inference(avatar_split_clause,[],[f145,f218,f223])).
% 3.84/0.88 thf(f233,plain,(
% 3.84/0.88 spl7_8 | spl7_6),
% 3.84/0.88 inference(avatar_split_clause,[],[f144,f218,f228])).
% 3.84/0.88 thf(f245,plain,(
% 3.84/0.88 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != $true) | ($true = ((irel @ X2 @ X1))) | ($true != ((irel @ X2 @ X0))) | (((irel @ X0 @ X1)) = $false)) )),
% 3.84/0.88 inference(constrained_superposition,[],[f69,f94])).
% 3.84/0.88 thf(f246,plain,(
% 3.84/0.88 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((irel @ X2 @ X0))) | ($true = ((irel @ X2 @ X1))) | (((irel @ X0 @ X1)) = $false)) )),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f245])).
% 3.84/0.88 thf(f264,definition,(
% 3.84/0.88 spl7_10 <=> ($false = ((q @ (sK6 @ sK0))))),
% 3.84/0.88 introduced(definition,[new_symbols(definition,[spl7_10])],[avatar_definition])).
% 3.84/0.88 thf(f265,plain,(
% 3.84/0.88 ($false != ((q @ (sK6 @ sK0)))) | spl7_10),
% 3.84/0.88 inference(avatar_component_clause,[],[f264])).
% 3.84/0.88 thf(f266,plain,(
% 3.84/0.88 ($false = ((q @ (sK6 @ sK0)))) | ~spl7_10),
% 3.84/0.88 inference(avatar_component_clause,[],[f264])).
% 3.84/0.88 thf(f304,plain,(
% 3.84/0.88 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true = $false) | (((irel @ X0 @ X1)) = $false) | (((irel @ X0 @ X2)) = $false) | ($false = ((p @ (sK4 @ X0)))) | ($true = ((r @ X2))) | ($true = ((q @ X1)))) )),
% 3.84/0.88 inference(constrained_superposition,[],[f68,f168])).
% 3.84/0.88 thf(f321,plain,(
% 3.84/0.88 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((irel @ X0 @ X2)) = $false) | (((irel @ X0 @ X1)) = $false) | ($false = ((p @ (sK4 @ X0)))) | ($true = ((r @ X2))) | ($true = ((q @ X1)))) )),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f304])).
% 3.84/0.88 thf(f419,definition,(
% 3.84/0.88 spl7_11 <=> ($true = ((p @ (sK4 @ sK0))))),
% 3.84/0.88 introduced(definition,[new_symbols(definition,[spl7_11])],[avatar_definition])).
% 3.84/0.88 thf(f421,plain,(
% 3.84/0.88 ($true = ((p @ (sK4 @ sK0)))) | ~spl7_11),
% 3.84/0.88 inference(avatar_component_clause,[],[f419])).
% 3.84/0.88 thf(f423,definition,(
% 3.84/0.88 spl7_12 <=> ! [X2 : $i,X0 : $i,X1 : $i] : ((((irel @ X0 @ X1)) = $false) | ($true = ((q @ X1))) | ($true = ((r @ X2))) | ($false = ((irel @ sK0 @ X0))) | (((irel @ X0 @ X2)) = $false))),
% 3.84/0.88 introduced(definition,[new_symbols(definition,[spl7_12])],[avatar_definition])).
% 3.84/0.88 thf(f424,plain,(
% 3.84/0.88 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X0))) | (((irel @ X0 @ X2)) = $false) | (((irel @ X0 @ X1)) = $false) | ($true = ((r @ X2))) | ($true = ((q @ X1)))) ) | ~spl7_12),
% 3.84/0.88 inference(avatar_component_clause,[],[f423])).
% 3.84/0.88 thf(f431,definition,(
% 3.84/0.88 spl7_14 <=> ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($true = ((r @ X0))))),
% 3.84/0.88 introduced(definition,[new_symbols(definition,[spl7_14])],[avatar_definition])).
% 3.84/0.88 thf(f432,plain,(
% 3.84/0.88 ( ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($true = ((r @ X0)))) ) | ~spl7_14),
% 3.84/0.88 inference(avatar_component_clause,[],[f431])).
% 3.84/0.88 thf(f444,plain,(
% 3.84/0.88 ( ! [X0 : $i] : (($true = $false) | ($true = ((q @ (sK6 @ sK0)))) | ($false = ((irel @ sK0 @ X0))) | ($true = ((r @ X0)))) ) | ~spl7_2),
% 3.84/0.88 inference(constrained_superposition,[],[f200,f194])).
% 3.84/0.88 thf(f493,plain,(
% 3.84/0.88 ( ! [X0 : $i] : (($true = $false) | ($false = ((r @ (sK5 @ X0)))) | ($true = ((p @ X0)))) )),
% 3.84/0.88 inference(constrained_superposition,[],[f68,f183])).
% 3.84/0.88 thf(f500,plain,(
% 3.84/0.88 ( ! [X0 : $i] : (($false = ((r @ (sK5 @ X0)))) | ($true = ((p @ X0)))) )),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f493])).
% 3.84/0.88 thf(f2130,plain,(
% 3.84/0.88 ($true = $false) | ($false = ((r @ (sK5 @ sK0)))) | ($true = ((p @ sK2))) | ~spl7_5),
% 3.84/0.88 inference(constrained_superposition,[],[f183,f215])).
% 3.84/0.88 thf(f2132,plain,(
% 3.84/0.88 ( ! [X0 : $i] : (($true != $true) | ($true = ((irel @ sK0 @ X0))) | ($false = ((irel @ sK2 @ X0)))) ) | ~spl7_5),
% 3.84/0.88 inference(constrained_superposition,[],[f246,f215])).
% 3.84/0.88 thf(f2159,plain,(
% 3.84/0.88 ( ! [X0 : $i] : (($false = ((irel @ sK2 @ X0))) | ($true = ((irel @ sK0 @ X0)))) ) | ~spl7_5),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f2132])).
% 3.84/0.88 thf(f2161,plain,(
% 3.84/0.88 ($false = ((r @ (sK5 @ sK0)))) | ($true = ((p @ sK2))) | ~spl7_5),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f2130])).
% 3.84/0.88 thf(f2219,plain,(
% 3.84/0.88 ($true = $false) | ($false = ((r @ (sK5 @ sK0)))) | (~spl7_5 | ~spl7_6)),
% 3.84/0.88 inference(forward_demodulation,[],[f2161,f220])).
% 3.84/0.88 thf(f2220,plain,(
% 3.84/0.88 ($false = ((r @ (sK5 @ sK0)))) | (~spl7_5 | ~spl7_6)),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f2219])).
% 3.84/0.88 thf(f2222,definition,(
% 3.84/0.88 spl7_28 <=> ($false = ((r @ (sK5 @ sK0))))),
% 3.84/0.88 introduced(definition,[new_symbols(definition,[spl7_28])],[avatar_definition])).
% 3.84/0.88 thf(f2224,plain,(
% 3.84/0.88 ($false = ((r @ (sK5 @ sK0)))) | ~spl7_28),
% 3.84/0.88 inference(avatar_component_clause,[],[f2222])).
% 3.84/0.88 thf(f2236,plain,(
% 3.84/0.88 spl7_28 | ~spl7_5 | ~spl7_6),
% 3.84/0.88 inference(avatar_split_clause,[],[f2220,f218,f213,f2222])).
% 3.84/0.88 thf(f3796,plain,(
% 3.84/0.88 ($true = $false) | ($true = ((q @ sK3))) | (~spl7_2 | ~spl7_7)),
% 3.84/0.88 inference(constrained_superposition,[],[f225,f200])).
% 3.84/0.88 thf(f3825,plain,(
% 3.84/0.88 ($true = $false) | ($false = ((r @ (sK5 @ sK0)))) | ($true = ((q @ sK3))) | ~spl7_7),
% 3.84/0.88 inference(constrained_superposition,[],[f182,f225])).
% 3.84/0.88 thf(f3872,plain,(
% 3.84/0.88 ($false = ((r @ (sK5 @ sK0)))) | ($true = ((q @ sK3))) | ~spl7_7),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f3825])).
% 3.84/0.88 thf(f3901,plain,(
% 3.84/0.88 ($true = ((q @ sK3))) | (~spl7_2 | ~spl7_7)),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f3796])).
% 3.84/0.88 thf(f3947,plain,(
% 3.84/0.88 ($true = $false) | ($false = ((r @ (sK5 @ sK0)))) | (~spl7_7 | ~spl7_8)),
% 3.84/0.88 inference(forward_demodulation,[],[f3872,f230])).
% 3.84/0.88 thf(f3948,plain,(
% 3.84/0.88 ($false = ((r @ (sK5 @ sK0)))) | (~spl7_7 | ~spl7_8)),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f3947])).
% 3.84/0.88 thf(f3979,plain,(
% 3.84/0.88 ($true = $false) | (~spl7_2 | ~spl7_7 | ~spl7_8)),
% 3.84/0.88 inference(forward_demodulation,[],[f3901,f230])).
% 3.84/0.88 thf(f3980,plain,(
% 3.84/0.88 $false | (~spl7_2 | ~spl7_7 | ~spl7_8)),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f3979])).
% 3.84/0.88 thf(f3981,plain,(
% 3.84/0.88 ~spl7_2 | ~spl7_7 | ~spl7_8),
% 3.84/0.88 inference(avatar_contradiction_clause,[],[f3980])).
% 3.84/0.88 thf(f4002,plain,(
% 3.84/0.88 spl7_28 | ~spl7_7 | ~spl7_8),
% 3.84/0.88 inference(avatar_split_clause,[],[f3948,f228,f223,f2222])).
% 3.84/0.88 thf(f5146,plain,(
% 3.84/0.88 ($true = $false) | ($true = ((p @ sK2))) | (~spl7_1 | ~spl7_5)),
% 3.84/0.88 inference(constrained_superposition,[],[f215,f197])).
% 3.84/0.88 thf(f5253,plain,(
% 3.84/0.88 ($true = ((p @ sK2))) | (~spl7_1 | ~spl7_5)),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f5146])).
% 3.84/0.88 thf(f5270,plain,(
% 3.84/0.88 ($true = $false) | (~spl7_1 | ~spl7_5 | ~spl7_6)),
% 3.84/0.88 inference(forward_demodulation,[],[f5253,f220])).
% 3.84/0.88 thf(f5271,plain,(
% 3.84/0.88 $false | (~spl7_1 | ~spl7_5 | ~spl7_6)),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f5270])).
% 3.84/0.88 thf(f5272,plain,(
% 3.84/0.88 ~spl7_1 | ~spl7_5 | ~spl7_6),
% 3.84/0.88 inference(avatar_contradiction_clause,[],[f5271])).
% 3.84/0.88 thf(f5648,plain,(
% 3.84/0.88 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ sK0 @ X0))) | ($false = ((p @ (sK4 @ sK0)))) | ($true = ((r @ X0))) | ($true = ((q @ sK1)))) ) | ~spl7_3),
% 3.84/0.88 inference(constrained_superposition,[],[f321,f205])).
% 3.84/0.88 thf(f5677,plain,(
% 3.84/0.88 ( ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($false = ((p @ (sK4 @ sK0)))) | ($true = ((r @ X0))) | ($true = ((q @ sK1)))) ) | ~spl7_3),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f5648])).
% 3.84/0.88 thf(f5745,plain,(
% 3.84/0.88 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ sK0 @ X0))) | ($true = ((r @ X0))) | ($true = ((q @ sK1)))) ) | (~spl7_3 | ~spl7_11)),
% 3.84/0.88 inference(forward_demodulation,[],[f5677,f421])).
% 3.84/0.88 thf(f5746,plain,(
% 3.84/0.88 ( ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($true = ((r @ X0))) | ($true = ((q @ sK1)))) ) | (~spl7_3 | ~spl7_11)),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f5745])).
% 3.84/0.88 thf(f5796,plain,(
% 3.84/0.88 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ sK0 @ X0))) | ($true = ((r @ X0)))) ) | (~spl7_3 | ~spl7_4 | ~spl7_11)),
% 3.84/0.88 inference(forward_demodulation,[],[f5746,f210])).
% 3.84/0.88 thf(f5797,plain,(
% 3.84/0.88 ( ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($true = ((r @ X0)))) ) | (~spl7_3 | ~spl7_4 | ~spl7_11)),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f5796])).
% 3.84/0.88 thf(f5813,plain,(
% 3.84/0.88 spl7_14 | ~spl7_3 | ~spl7_4 | ~spl7_11),
% 3.84/0.88 inference(avatar_split_clause,[],[f5797,f419,f208,f203,f431])).
% 3.84/0.88 thf(f5815,plain,(
% 3.84/0.88 ( ! [X0 : $i] : (($true = ((q @ (sK6 @ sK0)))) | ($false = ((irel @ sK0 @ X0))) | ($true = ((r @ X0)))) ) | ~spl7_2),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f444])).
% 3.84/0.88 thf(f5950,plain,(
% 3.84/0.88 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ sK0 @ X0))) | ($true = ((r @ X0)))) ) | (~spl7_2 | ~spl7_10)),
% 3.84/0.88 inference(forward_demodulation,[],[f5815,f266])).
% 3.84/0.88 thf(f5951,plain,(
% 3.84/0.88 ( ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($true = ((r @ X0)))) ) | (~spl7_2 | ~spl7_10)),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f5950])).
% 3.84/0.88 thf(f5965,plain,(
% 3.84/0.88 spl7_14 | ~spl7_2 | ~spl7_10),
% 3.84/0.88 inference(avatar_split_clause,[],[f5951,f264,f199,f431])).
% 3.84/0.88 thf(f6197,plain,(
% 3.84/0.88 ( ! [X0 : $i] : (($true = $false) | ($true = ((r @ (sK5 @ sK0)))) | ($false = ((irel @ sK0 @ X0))) | ($true = ((q @ X0)))) ) | ~spl7_14),
% 3.84/0.88 inference(constrained_superposition,[],[f432,f180])).
% 3.84/0.88 thf(f6214,plain,(
% 3.84/0.88 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ sK0 @ X0))) | ($true = ((p @ X0))) | ($true = ((r @ (sK5 @ sK0))))) ) | ~spl7_14),
% 3.84/0.88 inference(constrained_superposition,[],[f181,f432])).
% 3.84/0.88 thf(f6221,plain,(
% 3.84/0.88 ( ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($true = ((p @ X0))) | ($true = ((r @ (sK5 @ sK0))))) ) | ~spl7_14),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f6214])).
% 3.84/0.88 thf(f6246,plain,(
% 3.84/0.88 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ sK0 @ X0))) | ($true = ((p @ X0)))) ) | (~spl7_14 | ~spl7_28)),
% 3.84/0.88 inference(forward_demodulation,[],[f6221,f2224])).
% 3.84/0.88 thf(f6247,plain,(
% 3.84/0.88 ( ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($true = ((p @ X0)))) ) | (~spl7_14 | ~spl7_28)),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f6246])).
% 3.84/0.88 thf(f6266,plain,(
% 3.84/0.88 spl7_1 | ~spl7_14 | ~spl7_28),
% 3.84/0.88 inference(avatar_split_clause,[],[f6247,f2222,f431,f196])).
% 3.84/0.88 thf(f6440,definition,(
% 3.84/0.88 spl7_50 <=> ($true = ((r @ (sK5 @ sK2))))),
% 3.84/0.88 introduced(definition,[new_symbols(definition,[spl7_50])],[avatar_definition])).
% 3.84/0.88 thf(f6442,plain,(
% 3.84/0.88 ($true = ((r @ (sK5 @ sK2)))) | ~spl7_50),
% 3.84/0.88 inference(avatar_component_clause,[],[f6440])).
% 3.84/0.88 thf(f6448,definition,(
% 3.84/0.88 spl7_52 <=> ! [X0 : $i] : (($false = ((irel @ sK2 @ X0))) | ($true = ((p @ X0))))),
% 3.84/0.88 introduced(definition,[new_symbols(definition,[spl7_52])],[avatar_definition])).
% 3.84/0.88 thf(f6449,plain,(
% 3.84/0.88 ( ! [X0 : $i] : (($false = ((irel @ sK2 @ X0))) | ($true = ((p @ X0)))) ) | ~spl7_52),
% 3.84/0.88 inference(avatar_component_clause,[],[f6448])).
% 3.84/0.88 thf(f7379,plain,(
% 3.84/0.88 ($true = $false) | ($true = ((p @ sK2))) | ~spl7_50),
% 3.84/0.88 inference(constrained_superposition,[],[f500,f6442])).
% 3.84/0.88 thf(f7384,plain,(
% 3.84/0.88 ($true = ((p @ sK2))) | ~spl7_50),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f7379])).
% 3.84/0.88 thf(f7388,plain,(
% 3.84/0.88 ($true = $false) | (~spl7_6 | ~spl7_50)),
% 3.84/0.88 inference(forward_demodulation,[],[f7384,f220])).
% 3.84/0.88 thf(f7389,plain,(
% 3.84/0.88 $false | (~spl7_6 | ~spl7_50)),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f7388])).
% 3.84/0.88 thf(f7390,plain,(
% 3.84/0.88 ~spl7_6 | ~spl7_50),
% 3.84/0.88 inference(avatar_contradiction_clause,[],[f7389])).
% 3.84/0.88 thf(f7620,plain,(
% 3.84/0.88 ($true = $false) | ($true = ((p @ sK2))) | ~spl7_52),
% 3.84/0.88 inference(constrained_superposition,[],[f6449,f68])).
% 3.84/0.88 thf(f7678,plain,(
% 3.84/0.88 ($true = ((p @ sK2))) | ~spl7_52),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f7620])).
% 3.84/0.88 thf(f7700,plain,(
% 3.84/0.88 ($true = $false) | (~spl7_6 | ~spl7_52)),
% 3.84/0.88 inference(forward_demodulation,[],[f7678,f220])).
% 3.84/0.88 thf(f7701,plain,(
% 3.84/0.88 $false | (~spl7_6 | ~spl7_52)),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f7700])).
% 3.84/0.88 thf(f7702,plain,(
% 3.84/0.88 ~spl7_6 | ~spl7_52),
% 3.84/0.88 inference(avatar_contradiction_clause,[],[f7701])).
% 3.84/0.88 thf(f8834,plain,(
% 3.84/0.88 ( ! [X0 : $i] : (($true = $false) | ($true = ((irel @ sK0 @ (sK5 @ sK2)))) | ($false = ((irel @ sK2 @ X0))) | ($true = ((p @ X0)))) ) | ~spl7_5),
% 3.84/0.88 inference(constrained_superposition,[],[f2159,f181])).
% 3.84/0.88 thf(f8872,plain,(
% 3.84/0.88 ( ! [X0 : $i] : (($true = ((irel @ sK0 @ (sK5 @ sK2)))) | ($false = ((irel @ sK2 @ X0))) | ($true = ((p @ X0)))) ) | ~spl7_5),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f8834])).
% 3.84/0.88 thf(f8884,definition,(
% 3.84/0.88 spl7_109 <=> ($true = ((irel @ sK0 @ (sK5 @ sK2))))),
% 3.84/0.88 introduced(definition,[new_symbols(definition,[spl7_109])],[avatar_definition])).
% 3.84/0.88 thf(f8886,plain,(
% 3.84/0.88 ($true = ((irel @ sK0 @ (sK5 @ sK2)))) | ~spl7_109),
% 3.84/0.88 inference(avatar_component_clause,[],[f8884])).
% 3.84/0.88 thf(f8894,plain,(
% 3.84/0.88 spl7_52 | spl7_109 | ~spl7_5),
% 3.84/0.88 inference(avatar_split_clause,[],[f8872,f213,f8884,f6448])).
% 3.84/0.88 thf(f9143,plain,(
% 3.84/0.88 ($true = $false) | ($false = ((q @ (sK6 @ sK0)))) | ($true = ((r @ (sK5 @ sK2)))) | ~spl7_109),
% 3.84/0.88 inference(constrained_superposition,[],[f193,f8886])).
% 3.84/0.88 thf(f9216,plain,(
% 3.84/0.88 ($false = ((q @ (sK6 @ sK0)))) | ($true = ((r @ (sK5 @ sK2)))) | ~spl7_109),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f9143])).
% 3.84/0.88 thf(f9286,plain,(
% 3.84/0.88 ($true = ((r @ (sK5 @ sK2)))) | (spl7_10 | ~spl7_109)),
% 3.84/0.88 inference(forward_subsumption_resolution,[],[f9216,f265])).
% 3.84/0.88 thf(f9845,plain,(
% 3.84/0.88 spl7_50 | spl7_10 | ~spl7_109),
% 3.84/0.88 inference(avatar_split_clause,[],[f9286,f8884,f264,f6440])).
% 3.84/0.88 thf(f9939,plain,(
% 3.84/0.88 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true = $false) | ($true = ((p @ (sK4 @ sK0)))) | (((irel @ X0 @ X1)) = $false) | (((irel @ X0 @ X2)) = $false) | ($false = ((irel @ sK0 @ X0))) | ($true = ((r @ X2))) | ($true = ((q @ X1)))) ) | ~spl7_1),
% 3.84/0.88 inference(constrained_superposition,[],[f197,f162])).
% 3.84/0.88 thf(f10008,plain,(
% 3.84/0.88 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true = ((p @ (sK4 @ sK0)))) | (((irel @ X0 @ X1)) = $false) | (((irel @ X0 @ X2)) = $false) | ($false = ((irel @ sK0 @ X0))) | ($true = ((r @ X2))) | ($true = ((q @ X1)))) ) | ~spl7_1),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f9939])).
% 3.84/0.88 thf(f10031,plain,(
% 3.84/0.88 spl7_12 | spl7_11 | ~spl7_1),
% 3.84/0.88 inference(avatar_split_clause,[],[f10008,f196,f419,f423])).
% 3.84/0.88 thf(f10647,plain,(
% 3.84/0.88 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((irel @ sK0 @ X0))) | ($false = ((irel @ sK0 @ X1))) | ($true = ((r @ X0))) | ($true = ((q @ X1)))) ) | ~spl7_12),
% 3.84/0.88 inference(constrained_superposition,[],[f424,f68])).
% 3.84/0.88 thf(f10841,plain,(
% 3.84/0.88 ( ! [X0 : $i,X1 : $i] : (($false = ((irel @ sK0 @ X0))) | ($false = ((irel @ sK0 @ X1))) | ($true = ((r @ X0))) | ($true = ((q @ X1)))) ) | ~spl7_12),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f10647])).
% 3.84/0.88 thf(f10852,plain,(
% 3.84/0.88 spl7_2 | spl7_14 | ~spl7_12),
% 3.84/0.88 inference(avatar_split_clause,[],[f10841,f423,f431,f199])).
% 3.84/0.88 thf(f10930,plain,(
% 3.84/0.88 ( ! [X0 : $i] : (($true = ((r @ (sK5 @ sK0)))) | ($false = ((irel @ sK0 @ X0))) | ($true = ((q @ X0)))) ) | ~spl7_14),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f6197])).
% 3.84/0.88 thf(f10993,plain,(
% 3.84/0.88 ( ! [X0 : $i] : (($true = $false) | ($false = ((irel @ sK0 @ X0))) | ($true = ((q @ X0)))) ) | (~spl7_14 | ~spl7_28)),
% 3.84/0.88 inference(forward_demodulation,[],[f10930,f2224])).
% 3.84/0.88 thf(f10994,plain,(
% 3.84/0.88 ( ! [X0 : $i] : (($false = ((irel @ sK0 @ X0))) | ($true = ((q @ X0)))) ) | (~spl7_14 | ~spl7_28)),
% 3.84/0.88 inference(trivial_inequality_removal,[],[f10993])).
% 3.84/0.88 thf(f11014,plain,(
% 3.84/0.88 spl7_2 | ~spl7_14 | ~spl7_28),
% 3.84/0.88 inference(avatar_split_clause,[],[f10994,f2222,f431,f199])).
% 3.84/0.88 cnf(s1, plain, spl7_1 | spl7_2, inference(sat_conversion,[],[f201])).
% 3.84/0.88 cnf(s2, plain, spl7_2 | spl7_3, inference(sat_conversion,[],[f206])).
% 3.84/0.88 cnf(s3, plain, spl7_2 | spl7_4, inference(sat_conversion,[],[f211])).
% 3.84/0.88 cnf(s4, plain, spl7_1 | spl7_5, inference(sat_conversion,[],[f216])).
% 3.84/0.88 cnf(s5, plain, spl7_1 | spl7_6, inference(sat_conversion,[],[f221])).
% 3.84/0.88 cnf(s6, plain, spl7_5 | spl7_7, inference(sat_conversion,[],[f226])).
% 3.84/0.88 cnf(s7, plain, spl7_5 | spl7_8, inference(sat_conversion,[],[f231])).
% 3.84/0.88 cnf(s8, plain, spl7_6 | spl7_7, inference(sat_conversion,[],[f232])).
% 3.84/0.88 cnf(s9, plain, spl7_6 | spl7_8, inference(sat_conversion,[],[f233])).
% 3.84/0.88 cnf(s59, plain, ~spl7_5 | ~spl7_6 | spl7_28, inference(sat_conversion,[],[f2236])).
% 3.84/0.88 cnf(s109, plain, ~spl7_2 | ~spl7_7 | ~spl7_8, inference(sat_conversion,[],[f3981])).
% 3.84/0.88 cnf(s117, plain, ~spl7_7 | ~spl7_8 | spl7_28, inference(sat_conversion,[],[f4002])).
% 3.84/0.88 cnf(s172, plain, ~spl7_1 | ~spl7_5 | ~spl7_6, inference(sat_conversion,[],[f5272])).
% 3.84/0.88 cnf(s353, plain, ~spl7_3 | ~spl7_4 | ~spl7_11 | spl7_14, inference(sat_conversion,[],[f5813])).
% 3.84/0.88 cnf(s365, plain, ~spl7_2 | ~spl7_10 | spl7_14, inference(sat_conversion,[],[f5965])).
% 3.84/0.88 cnf(s383, plain, spl7_1 | ~spl7_14 | ~spl7_28, inference(sat_conversion,[],[f6266])).
% 3.84/0.88 cnf(s497, plain, ~spl7_6 | ~spl7_50, inference(sat_conversion,[],[f7390])).
% 3.84/0.88 cnf(s525, plain, ~spl7_6 | ~spl7_52, inference(sat_conversion,[],[f7702])).
% 3.84/0.88 cnf(s716, plain, ~spl7_5 | spl7_52 | spl7_109, inference(sat_conversion,[],[f8894])).
% 3.84/0.88 cnf(s927, plain, spl7_10 | spl7_50 | ~spl7_109, inference(sat_conversion,[],[f9845])).
% 3.84/0.88 cnf(s1037, plain, ~spl7_1 | spl7_11 | spl7_12, inference(sat_conversion,[],[f10031])).
% 3.84/0.88 cnf(s1099, plain, spl7_2 | ~spl7_12 | spl7_14, inference(sat_conversion,[],[f10852])).
% 3.84/0.88 cnf(s1164, plain, spl7_2 | ~spl7_14 | ~spl7_28, inference(sat_conversion,[],[f11014])).
% 3.84/0.88 cnf(s1168, plain, spl7_1, inference(rat,[],[s365,s927,s383,s716,s59,s497,s525,s1,s4,s5])).
% 3.84/0.88 cnf(s1169, plain, spl7_6 | ~spl7_2, inference(rat,[],[s109,s8,s9])).
% 3.84/0.88 cnf(s1170, plain, ~spl7_2, inference(rat,[],[s109,s6,s7,s172,s1169,s1168])).
% 3.84/0.88 cnf(s1172, plain, spl7_4, inference(rat,[],[s3,s1170])).
% 3.84/0.88 cnf(s1173, plain, spl7_3, inference(rat,[],[s2,s1170])).
% 3.84/0.88 cnf(s1175, plain, spl7_14, inference(rat,[],[s1037,s353,s1099,s1168,s1173,s1172,s1170])).
% 3.84/0.88 cnf(s1176, plain, ~spl7_28, inference(rat,[],[s1164,s1170,s1175])).
% 3.84/0.88 cnf(s1177, plain, spl7_6, inference(rat,[],[s117,s8,s9,s1176])).
% 3.84/0.88 cnf(s1180, plain, ~spl7_5, inference(rat,[],[s172,s1168,s1177])).
% 3.84/0.88 cnf(s1182, plain, spl7_8, inference(rat,[],[s7,s1180])).
% 3.84/0.88 cnf(s1183, plain, spl7_7, inference(rat,[],[s6,s1180])).
% 3.84/0.88 cnf(s1184, plain, $false, inference(rat,[],[s117,s1176,s1182,s1183])).
% 3.84/0.88 thf(f11015,plain,(
% 3.84/0.88 $false),
% 3.84/0.88 inference(avatar_sat_refutation,[],[s1184])).
% 3.84/0.88 % SZS output end Proof for theBenchmark
% 3.84/0.88 % (278279)------------------------------
% 3.84/0.88 % (278279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.84/0.88 % (278279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.84/0.88 % (278279)CaDiCaL version: 2.1.3
% 3.84/0.88 % (278279)Termination reason: Refutation
% 3.84/0.88 % (278279)Time elapsed: 0.611 s
% 3.84/0.88 % (278279)Peak memory usage: 15 MB
% 3.84/0.88 % (278279)Instructions burned: 1465 (million)
% 3.84/0.88 % (278273)Success in time 0.652 s
% 3.84/0.88 % Vampire exiting
%------------------------------------------------------------------------------