%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO067^4.001 : 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 : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:48:52 AM UTC 2026
% Result : Theorem 1.70s 0.90s
% Output : Refutation 1.70s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO067^4.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n007.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Sep 29 16:25:56 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/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
% 1.70/0.90 % (3588242)Will run a generic schedule for satisfiability detection.
% 1.70/0.90 % (3588248)% WARNING: option uhcvi not known.
% 1.70/0.90 % (3588248)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3711332017:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.70/0.90 % (3588248)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.70/0.90 % (3588248)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 1.70/0.90 % (3588247)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=108088057_2999 on theBenchmark for (2999ds/0Mi)
% 1.70/0.90 % (3588249)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4005587024:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.70/0.90 % (3588250)dis+10_1_sil=32000:sp=arity:random_seed=3097768937:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.70/0.90 % (3588251)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=703124912:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.70/0.90 % (3588251)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.70/0.90 % Exception at run slice level
% 1.70/0.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.70/0.90 % (3588252)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3610462456:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.70/0.90 % (3588253)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3697486990:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.70/0.90 % (3588259)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=632016011:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.70/0.90 % Exception at run slice level
% 1.70/0.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.70/0.90 % (3588263)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3891736625:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.70/0.90 % (3588250)Instruction limit reached!
% 1.70/0.90 % (3588250)------------------------------
% 1.70/0.90 % (3588250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.70/0.90 % (3588250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.70/0.90 % (3588250)CaDiCaL version: 2.1.3
% 1.70/0.90 % (3588250)Termination reason: Instruction limit
% 1.70/0.90 % (3588250)Termination phase: Saturation
% 1.70/0.90 % (3588250)Time elapsed: 0.084 s
% 1.70/0.90 % (3588250)Peak memory usage: 12 MB
% 1.70/0.90 % (3588250)Instructions burned: 104 (million)
% 1.70/0.90 % (3588251)Instruction limit reached!
% 1.70/0.90 % (3588251)------------------------------
% 1.70/0.90 % (3588251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.70/0.90 % (3588251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.70/0.90 % (3588251)CaDiCaL version: 2.1.3
% 1.70/0.90 % (3588251)Termination reason: Instruction limit
% 1.70/0.90 % (3588251)Termination phase: Saturation
% 1.70/0.90 % (3588251)Time elapsed: 0.094 s
% 1.70/0.90 % (3588251)Peak memory usage: 12 MB
% 1.70/0.90 % (3588251)Instructions burned: 116 (million)
% 1.70/0.90 % (3588266)ott-21_1_sil=16000:fs=off:random_seed=1513832910:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.70/0.90 % (3588265)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=2660273760:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.70/0.90 % (3588265)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.70/0.90 % (3588265)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 1.70/0.90 % (3588252)Instruction limit reached!
% 1.70/0.90 % (3588252)------------------------------
% 1.70/0.90 % (3588252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.70/0.90 % (3588252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.70/0.90 % (3588252)CaDiCaL version: 2.1.3
% 1.70/0.90 % (3588252)Termination reason: Instruction limit
% 1.70/0.90 % (3588252)Termination phase: Saturation
% 1.70/0.90 % (3588252)Time elapsed: 0.135 s
% 1.70/0.90 % (3588252)Peak memory usage: 12 MB
% 1.70/0.90 % (3588252)Instructions burned: 131 (million)
% 1.70/0.90 % (3588253)Instruction limit reached!
% 1.70/0.90 % (3588253)------------------------------
% 1.70/0.90 % (3588253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.70/0.90 % (3588253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.70/0.90 % (3588253)CaDiCaL version: 2.1.3
% 1.70/0.90 % (3588253)Termination reason: Instruction limit
% 1.70/0.90 % (3588253)Termination phase: Saturation
% 1.70/0.90 % (3588253)Time elapsed: 0.160 s
% 1.70/0.90 % (3588253)Peak memory usage: 12 MB
% 1.70/0.90 % (3588253)Instructions burned: 159 (million)
% 1.70/0.90 % (3588263)Instruction limit reached!
% 1.70/0.90 % (3588263)------------------------------
% 1.70/0.90 % (3588263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.70/0.90 % (3588263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.70/0.90 % (3588263)CaDiCaL version: 2.1.3
% 1.70/0.90 % (3588263)Termination reason: Instruction limit
% 1.70/0.90 % (3588263)Termination phase: Saturation
% 1.70/0.90 % (3588263)Time elapsed: 0.132 s
% 1.70/0.90 % (3588263)Peak memory usage: 12 MB
% 1.70/0.90 % (3588263)Instructions burned: 132 (million)
% 1.70/0.90 % (3588269)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=650391379:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 1.70/0.90 % (3588270)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2207113809:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 1.70/0.90 % Exception at run slice level
% 1.70/0.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.70/0.90 % (3588271)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1546857340:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 1.70/0.90 % (3588274)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1996219094:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 1.70/0.90 % Exception at run slice level
% 1.70/0.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.70/0.90 % (3588277)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=2803896523:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi)
% 1.70/0.90 % (3588277)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.70/0.90 % (3588266)Instruction limit reached!
% 1.70/0.90 % (3588266)------------------------------
% 1.70/0.90 % (3588266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.70/0.90 % (3588266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.70/0.90 % (3588266)CaDiCaL version: 2.1.3
% 1.70/0.90 % (3588266)Termination reason: Instruction limit
% 1.70/0.90 % (3588266)Termination phase: Saturation
% 1.70/0.90 % (3588266)Time elapsed: 0.182 s
% 1.70/0.90 % (3588266)Peak memory usage: 13 MB
% 1.70/0.90 % (3588266)Instructions burned: 181 (million)
% 1.70/0.90 % (3588279)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=343021806:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 1.70/0.90 % (3588279)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.70/0.90 % (3588265) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3588242-3588265"...
% 1.70/0.90 % (3588265)...printing done.
% 1.70/0.90 % (3588265)Refutation found. Thanks to Tanya!
% 1.70/0.90 % SZS status Theorem for theBenchmark
% 1.70/0.90 % SZS output start Proof for theBenchmark
% 1.70/0.90 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 1.70/0.90 thf(func_def_0, type, irel: ($i > $i > $o)).
% 1.70/0.90 thf(func_def_2, type, mnot: (($i > $o) > $i > $o)).
% 1.70/0.90 thf(func_def_3, type, mor: (($i > $o) > ($i > $o) > $i > $o)).
% 1.70/0.90 thf(func_def_4, type, mand: (($i > $o) > ($i > $o) > $i > $o)).
% 1.70/0.90 thf(func_def_5, type, mimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 1.70/0.90 thf(func_def_6, type, mbox_s4: (($i > $o) > $i > $o)).
% 1.70/0.90 thf(func_def_7, type, iatom: (($i > $o) > $i > $o)).
% 1.70/0.90 thf(func_def_8, type, inot: (($i > $o) > $i > $o)).
% 1.70/0.90 thf(func_def_9, type, itrue: ($i > $o)).
% 1.70/0.90 thf(func_def_10, type, ifalse: ($i > $o)).
% 1.70/0.90 thf(func_def_11, type, iand: (($i > $o) > ($i > $o) > $i > $o)).
% 1.70/0.90 thf(func_def_12, type, ior: (($i > $o) > ($i > $o) > $i > $o)).
% 1.70/0.90 thf(func_def_13, type, iimplies: (($i > $o) > ($i > $o) > $i > $o)).
% 1.70/0.90 thf(func_def_14, type, iimplied: (($i > $o) > ($i > $o) > $i > $o)).
% 1.70/0.90 thf(func_def_15, type, iequiv: (($i > $o) > ($i > $o) > $i > $o)).
% 1.70/0.90 thf(func_def_16, type, ixor: (($i > $o) > ($i > $o) > $i > $o)).
% 1.70/0.90 thf(func_def_17, type, ivalid: (($i > $o) > $o)).
% 1.70/0.90 thf(func_def_18, type, isatisfiable: (($i > $o) > $o)).
% 1.70/0.90 thf(func_def_19, type, icountersatisfiable: (($i > $o) > $o)).
% 1.70/0.90 thf(func_def_20, type, iinvalid: (($i > $o) > $o)).
% 1.70/0.90 thf(func_def_21, type, f: ($i > $o)).
% 1.70/0.90 thf(func_def_22, type, p1: ($i > $o)).
% 1.70/0.90 thf(func_def_25, type, vNOT: ($o > $o)).
% 1.70/0.90 thf(func_def_26, type, db1: !>[X0: $tType]:(X0)).
% 1.70/0.90 thf(func_def_27, type, db0: !>[X0: $tType]:(X0)).
% 1.70/0.90 thf(func_def_28, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 1.70/0.90 thf(func_def_29, type, vOR: ($o > $o > $o)).
% 1.70/0.90 thf(func_def_30, type, db2: !>[X0: $tType]:(X0)).
% 1.70/0.90 thf(func_def_31, type, vAND: ($o > $o > $o)).
% 1.70/0.90 thf(func_def_32, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 1.70/0.90 thf(func_def_33, type, vIMP: ($o > $o > $o)).
% 1.70/0.90 thf(func_def_34, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 1.70/0.90 thf(func_def_36, type, sK1: ($i > $i)).
% 1.70/0.90 thf(func_def_37, type, sK2: ($i > $i)).
% 1.70/0.90 thf(func_def_38, type, sK3: ($i > $i)).
% 1.70/0.90 thf(func_def_39, type, sK4: ($i > $i)).
% 1.70/0.90 thf(f1,axiom,(
% 1.70/0.90 ! [X0 : $i] : (irel @ X0 @ X0)),
% 1.70/0.90 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',refl_axiom)).
% 1.70/0.90 thf(f2,axiom,(
% 1.70/0.90 ! [X0 : $i,X1 : $i,X2 : $i] : (((irel @ X1 @ X2) & (irel @ X0 @ X1)) => (irel @ X0 @ X2))),
% 1.70/0.90 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',trans_axiom)).
% 1.70/0.90 thf(f3,axiom,(
% 1.70/0.90 (mnot = (^[X0 : ($i > $o), X1 : $i] : (~(X0 @ X1))))),
% 1.70/0.90 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',mnot)).
% 1.70/0.90 thf(f4,axiom,(
% 1.70/0.90 (mor = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X1 @ X2) | (X0 @ X2))))),
% 1.70/0.90 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',mor)).
% 1.70/0.90 thf(f6,axiom,(
% 1.70/0.90 (mimplies = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mor @ (mnot @ X0) @ X1))))),
% 1.70/0.90 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',mimplies)).
% 1.70/0.90 thf(f7,axiom,(
% 1.70/0.90 (mbox_s4 = (^[X0 : ($i > $o), X1 : $i] : (! [X2 : $i] : ((irel @ X1 @ X2) => (X0 @ X2)))))),
% 1.70/0.90 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',mbox_s4)).
% 1.70/0.91 thf(f8,axiom,(
% 1.70/0.91 (iatom = (^[X0 : ($i > $o)] : (X0)))),
% 1.70/0.91 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',iatom)).
% 1.70/0.91 thf(f13,axiom,(
% 1.70/0.91 (ior = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mor @ (mbox_s4 @ X0) @ (mbox_s4 @ X1)))))),
% 1.70/0.91 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',ior)).
% 1.70/0.91 thf(f14,axiom,(
% 1.70/0.91 (iimplies = (^[X0 : ($i > $o), X1 : ($i > $o)] : ((mimplies @ (mbox_s4 @ X0) @ (mbox_s4 @ X1)))))),
% 1.70/0.91 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',iimplies)).
% 1.70/0.91 thf(f18,axiom,(
% 1.70/0.91 (ivalid = (^[X0 : ($i > $o)] : (! [X1 : $i] : (X0 @ X1))))),
% 1.70/0.91 file('/export/starexec/sandbox/benchmark/Axioms/LCL010^0.ax',ivalid)).
% 1.70/0.91 thf(f22,axiom,(
% 1.70/0.91 (ivalid @ (iimplies @ (ior @ (iatom @ p1) @ (iimplies @ (iatom @ p1) @ (iatom @ f))) @ (iatom @ f)))),
% 1.70/0.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom1)).
% 1.70/0.91 thf(f23,conjecture,(
% 1.70/0.91 (ivalid @ (iatom @ f))),
% 1.70/0.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p',con)).
% 1.70/0.91 thf(f24,negated_conjecture,(
% 1.70/0.91 ~(ivalid @ (iatom @ f))),
% 1.70/0.91 inference(negated_conjecture,[status(cth)],[f23])).
% 1.70/0.91 thf(f25,plain,(
% 1.70/0.91 ! [X0 : $i] : (irel @ X0 @ X0)),
% 1.70/0.91 inference(rectify,[],[f1])).
% 1.70/0.91 thf(f26,plain,(
% 1.70/0.91 ! [X0 : $i] : (((irel @ X0 @ X0)) = $true)),
% 1.70/0.91 inference(fool_elimination,[],[f25])).
% 1.70/0.91 thf(f27,plain,(
% 1.70/0.91 ! [X0 : $i,X1 : $i,X2 : $i] : (((irel @ X1 @ X2) & (irel @ X0 @ X1)) => (irel @ X0 @ X2))),
% 1.70/0.91 inference(rectify,[],[f2])).
% 1.70/0.91 thf(f28,plain,(
% 1.70/0.91 ! [X0 : $i,X1 : $i,X2 : $i] : (((((irel @ X1 @ X2)) = $true) & (((irel @ X0 @ X1)) = $true)) => (((irel @ X0 @ X2)) = $true))),
% 1.70/0.91 inference(fool_elimination,[],[f27])).
% 1.70/0.91 thf(f29,plain,(
% 1.70/0.91 (mnot = (^[X0 : ($i > $o), X1 : $i] : (~(X0 @ X1))))),
% 1.70/0.91 inference(rectify,[],[f3])).
% 1.70/0.91 thf(f30,plain,(
% 1.70/0.91 (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))))),
% 1.70/0.91 inference(fool_elimination,[],[f29])).
% 1.70/0.91 thf(f31,plain,(
% 1.70/0.91 (mor = (^[X0 : ($i > $o), X1 : ($i > $o), X2 : $i] : ((X1 @ X2) | (X0 @ X2))))),
% 1.70/0.91 inference(rectify,[],[f4])).
% 1.70/0.91 thf(f32,plain,(
% 1.70/0.91 (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))))),
% 1.70/0.91 inference(fool_elimination,[],[f31])).
% 1.70/0.91 thf(f35,plain,(
% 1.70/0.91 (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mnot @ Y0) @ Y1)))))),
% 1.70/0.91 inference(fool_elimination,[],[f6])).
% 1.70/0.91 thf(f36,plain,(
% 1.70/0.91 (mbox_s4 = (^[X0 : ($i > $o), X1 : $i] : (! [X2 : $i] : ((irel @ X1 @ X2) => (X0 @ X2)))))),
% 1.70/0.91 inference(rectify,[],[f7])).
% 1.70/0.91 thf(f37,plain,(
% 1.70/0.91 (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (Y0 @ Y2))))))))),
% 1.70/0.91 inference(fool_elimination,[],[f36])).
% 1.70/0.91 thf(f38,plain,(
% 1.70/0.91 (iatom = (^[Y0 : $i > $o]: (Y0)))),
% 1.70/0.91 inference(fool_elimination,[],[f8])).
% 1.70/0.91 thf(f42,plain,(
% 1.70/0.91 (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 1.70/0.91 inference(fool_elimination,[],[f13])).
% 1.70/0.91 thf(f43,plain,(
% 1.70/0.91 (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mimplies @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 1.70/0.91 inference(fool_elimination,[],[f14])).
% 1.70/0.91 thf(f47,plain,(
% 1.70/0.91 (ivalid = (^[X0 : ($i > $o)] : (! [X1 : $i] : (X0 @ X1))))),
% 1.70/0.91 inference(rectify,[],[f18])).
% 1.70/0.91 thf(f48,plain,(
% 1.70/0.91 (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))),
% 1.70/0.91 inference(fool_elimination,[],[f47])).
% 1.70/0.91 thf(f55,plain,(
% 1.70/0.91 (ivalid @ (iimplies @ (ior @ (iatom @ p1) @ (iimplies @ (iatom @ p1) @ (iatom @ f))) @ (iatom @ f)))),
% 1.70/0.91 inference(rectify,[],[f22])).
% 1.70/0.91 thf(f56,plain,(
% 1.70/0.91 (((ivalid @ (iimplies @ (ior @ (iatom @ p1) @ (iimplies @ (iatom @ p1) @ (iatom @ f))) @ (iatom @ f)))) = $true)),
% 1.70/0.91 inference(fool_elimination,[],[f55])).
% 1.70/0.91 thf(f57,plain,(
% 1.70/0.91 ~(ivalid @ (iatom @ f))),
% 1.70/0.91 inference(rectify,[],[f24])).
% 1.70/0.91 thf(f58,plain,(
% 1.70/0.91 ~ (((ivalid @ (iatom @ f))) = $true)),
% 1.70/0.91 inference(fool_elimination,[],[f57])).
% 1.70/0.91 thf(f59,plain,(
% 1.70/0.91 (((ivalid @ (iatom @ f))) != $true)),
% 1.70/0.91 inference(flattening,[],[f58])).
% 1.70/0.91 thf(f60,plain,(
% 1.70/0.91 ! [X0 : $i,X1 : $i,X2 : $i] : ((((irel @ X0 @ X2)) = $true) | ((((irel @ X1 @ X2)) != $true) | (((irel @ X0 @ X1)) != $true)))),
% 1.70/0.91 inference(ennf_transformation,[],[f28])).
% 1.70/0.91 thf(f61,plain,(
% 1.70/0.91 ! [X0 : $i,X1 : $i,X2 : $i] : ((((irel @ X0 @ X2)) = $true) | (((irel @ X1 @ X2)) != $true) | (((irel @ X0 @ X1)) != $true))),
% 1.70/0.91 inference(flattening,[],[f60])).
% 1.70/0.91 thf(f62,plain,(
% 1.70/0.91 ( ! [X0 : $i] : ((((irel @ X0 @ X0)) = $true)) )),
% 1.70/0.91 inference(cnf_transformation,[],[f26])).
% 1.70/0.91 thf(f63,plain,(
% 1.70/0.91 ( ! [X2 : $i,X0 : $i,X1 : $i] : ((((irel @ X1 @ X2)) != $true) | (((irel @ X0 @ X2)) = $true) | (((irel @ X0 @ X1)) != $true)) )),
% 1.70/0.91 inference(cnf_transformation,[],[f61])).
% 1.70/0.91 thf(f64,plain,(
% 1.70/0.91 (mnot = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (~ (Y0 @ Y1))))))),
% 1.70/0.91 inference(cnf_transformation,[],[f30])).
% 1.70/0.91 thf(f65,plain,(
% 1.70/0.91 (mor = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))))),
% 1.70/0.91 inference(cnf_transformation,[],[f32])).
% 1.70/0.91 thf(f67,plain,(
% 1.70/0.91 (mimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mnot @ Y0) @ Y1)))))),
% 1.70/0.91 inference(cnf_transformation,[],[f35])).
% 1.70/0.91 thf(f68,plain,(
% 1.70/0.91 (mbox_s4 = (^[Y0 : $i > $o]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (Y0 @ Y2))))))))),
% 1.70/0.91 inference(cnf_transformation,[],[f37])).
% 1.70/0.91 thf(f69,plain,(
% 1.70/0.91 (iatom = (^[Y0 : $i > $o]: (Y0)))),
% 1.70/0.91 inference(cnf_transformation,[],[f38])).
% 1.70/0.91 thf(f74,plain,(
% 1.70/0.91 (ior = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mor @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 1.70/0.91 inference(cnf_transformation,[],[f42])).
% 1.70/0.91 thf(f75,plain,(
% 1.70/0.91 (iimplies = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (mimplies @ (mbox_s4 @ Y0) @ (mbox_s4 @ Y1))))))),
% 1.70/0.91 inference(cnf_transformation,[],[f43])).
% 1.70/0.91 thf(f79,plain,(
% 1.70/0.91 (ivalid = (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))))),
% 1.70/0.91 inference(cnf_transformation,[],[f48])).
% 1.70/0.91 thf(f83,plain,(
% 1.70/0.91 (((ivalid @ (iimplies @ (ior @ (iatom @ p1) @ (iimplies @ (iatom @ p1) @ (iatom @ f))) @ (iatom @ f)))) = $true)),
% 1.70/0.91 inference(cnf_transformation,[],[f56])).
% 1.70/0.91 thf(f84,plain,(
% 1.70/0.91 (((ivalid @ (iatom @ f))) != $true)),
% 1.70/0.91 inference(cnf_transformation,[],[f59])).
% 1.70/0.91 thf(f86,definition,(
% 1.70/0.91 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 1.70/0.91 introduced(theory,[fool_exhaustiveness_axiom])).
% 1.70/0.91 thf(f87,plain,(
% 1.70/0.91 (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)))))),
% 1.70/0.91 inference(definition_unfolding,[],[f67,f65,f64])).
% 1.70/0.91 thf(f91,plain,(
% 1.70/0.91 (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))))))),
% 1.70/0.91 inference(definition_unfolding,[],[f74,f65,f68,f68])).
% 1.70/0.91 thf(f92,plain,(
% 1.70/0.91 (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))))))),
% 1.70/0.91 inference(definition_unfolding,[],[f75,f87,f68,f68])).
% 1.70/0.91 thf(f96,plain,(
% 1.70/0.91 ($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]: ((^[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)) @ p1) @ ((^[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)) @ p1) @ ((^[Y0 : $i > $o]: (Y0)) @ f))) @ ((^[Y0 : $i > $o]: (Y0)) @ f)))))),
% 1.70/0.91 inference(definition_unfolding,[],[f83,f79,f92,f91,f69,f92,f69,f69,f69])).
% 1.70/0.91 thf(f97,plain,(
% 1.70/0.91 ($true != (((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: (Y0 @ Y1)))) @ ((^[Y0 : $i > $o]: (Y0)) @ f))))),
% 1.70/0.91 inference(definition_unfolding,[],[f84,f79,f69])).
% 1.70/0.91 thf(f98,plain,(
% 1.70/0.91 ($true != ((!! @ $i @ f)))),
% 1.70/0.91 inference(beta-eta_normalization,[],[f97])).
% 1.70/0.91 thf(f99,plain,(
% 1.70/0.91 ($false = ((f @ sK0)))),
% 1.70/0.91 inference(sigma_proxy_clausification,[],[f98])).
% 1.70/0.91 thf(f100,plain,(
% 1.70/0.91 ($true = ((!! @ $i @ (^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p1 @ Y2)))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((~ (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (p1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (f @ Y3))))))))))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (f @ Y1)))))))))),
% 1.70/0.91 inference(beta-eta_normalization,[],[f96])).
% 1.70/0.91 thf(f101,plain,(
% 1.70/0.91 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p1 @ Y2)))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => ((~ (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (p1 @ Y3))))) | (!! @ $i @ (^[Y3 : $i]: ((irel @ Y2 @ Y3) => (f @ Y3))))))))))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (f @ Y1)))))) @ X1)))) )),
% 1.70/0.91 inference(pi_proxy_clausification,[],[f100])).
% 1.70/0.91 thf(f102,plain,(
% 1.70/0.91 ( ! [X1 : $i] : (($true = (((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p1 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (f @ Y2))))))))))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (f @ Y0)))))))) )),
% 1.70/0.91 inference(beta-eta_normalization,[],[f101])).
% 1.70/0.91 thf(f103,plain,(
% 1.70/0.91 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => (f @ Y0)))))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p1 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (f @ Y2)))))))))))))))) )),
% 1.70/0.91 inference(or_proxy_clausification,[],[f102])).
% 1.70/0.91 thf(f104,plain,(
% 1.70/0.91 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (f @ Y0))) @ X2))) | ($true = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p1 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (f @ Y2)))))))))))))))) )),
% 1.70/0.91 inference(pi_proxy_clausification,[],[f103])).
% 1.70/0.91 thf(f105,plain,(
% 1.70/0.91 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (f @ Y0))) @ X2))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ X1 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p1 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (f @ Y2))))))))))))))) )),
% 1.70/0.91 inference(not_proxy_clausification,[],[f104])).
% 1.70/0.91 thf(f106,plain,(
% 1.70/0.91 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => (f @ Y0))) @ X2))) | ($false = (((^[Y0 : $i]: ((irel @ X1 @ Y0) => ((!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1)))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => ((~ (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (p1 @ Y2))))) | (!! @ $i @ (^[Y2 : $i]: ((irel @ Y1 @ Y2) => (f @ Y2))))))))))) @ (sK1 @ X1))))) )),
% 1.70/0.91 inference(sigma_proxy_clausification,[],[f105])).
% 1.70/0.91 thf(f107,plain,(
% 1.70/0.91 ( ! [X2 : $i,X1 : $i] : (($true = (((irel @ X1 @ X2) => (f @ X2)))) | ($false = (((irel @ X1 @ (sK1 @ X1)) => ((!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (p1 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (f @ Y1))))))))))))) )),
% 1.70/0.91 inference(beta-eta_normalization,[],[f106])).
% 1.70/0.91 thf(f108,plain,(
% 1.70/0.91 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = (((irel @ X1 @ (sK1 @ X1)) => ((!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (p1 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (f @ Y1)))))))))))) | ($true = ((f @ X2)))) )),
% 1.70/0.91 inference(imp_proxy_clausification,[],[f107])).
% 1.70/0.91 thf(f109,plain,(
% 1.70/0.91 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = (((!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (p1 @ Y0)))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (f @ Y1))))))))))) | ($true = ((f @ X2)))) )),
% 1.70/0.91 inference(imp_proxy_clausification,[],[f108])).
% 1.70/0.91 thf(f110,plain,(
% 1.70/0.91 ( ! [X2 : $i,X1 : $i] : (($true = ((irel @ X1 @ (sK1 @ X1)))) | (((irel @ X1 @ X2)) = $false) | ($true = ((f @ X2)))) )),
% 1.70/0.91 inference(imp_proxy_clausification,[],[f108])).
% 1.70/0.91 thf(f111,plain,(
% 1.70/0.91 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (f @ Y1)))))))))) | ($true = ((f @ X2)))) )),
% 1.70/0.91 inference(or_proxy_clausification,[],[f109])).
% 1.70/0.91 thf(f112,plain,(
% 1.70/0.91 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (p1 @ Y0)))))) | ($true = ((f @ X2)))) )),
% 1.70/0.91 inference(or_proxy_clausification,[],[f109])).
% 1.70/0.91 thf(f113,plain,(
% 1.70/0.91 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = (((^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => (p1 @ Y0))) @ (sK2 @ X1)))) | ($true = ((f @ X2)))) )),
% 1.70/0.91 inference(sigma_proxy_clausification,[],[f112])).
% 1.70/0.91 thf(f114,plain,(
% 1.70/0.91 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = (((irel @ (sK1 @ X1) @ (sK2 @ X1)) => (p1 @ (sK2 @ X1))))) | ($true = ((f @ X2)))) )),
% 1.70/0.91 inference(beta-eta_normalization,[],[f113])).
% 1.70/0.91 thf(f115,plain,(
% 1.70/0.91 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((p1 @ (sK2 @ X1)))) | ($true = ((f @ X2)))) )),
% 1.70/0.91 inference(imp_proxy_clausification,[],[f114])).
% 1.70/0.91 thf(f116,plain,(
% 1.70/0.91 ( ! [X2 : $i,X1 : $i] : (($true = ((irel @ (sK1 @ X1) @ (sK2 @ X1)))) | (((irel @ X1 @ X2)) = $false) | ($true = ((f @ X2)))) )),
% 1.70/0.91 inference(imp_proxy_clausification,[],[f114])).
% 1.70/0.91 thf(f117,plain,(
% 1.70/0.91 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = (((^[Y0 : $i]: ((irel @ (sK1 @ X1) @ Y0) => ((~ (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (p1 @ Y1))))) | (!! @ $i @ (^[Y1 : $i]: ((irel @ Y0 @ Y1) => (f @ Y1))))))) @ (sK3 @ X1)))) | ($true = ((f @ X2)))) )),
% 1.70/0.91 inference(sigma_proxy_clausification,[],[f111])).
% 1.70/0.91 thf(f118,plain,(
% 1.70/0.91 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = (((irel @ (sK1 @ X1) @ (sK3 @ X1)) => ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK3 @ X1) @ Y0) => (p1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK3 @ X1) @ Y0) => (f @ Y0)))))))) | ($true = ((f @ X2)))) )),
% 1.70/0.91 inference(beta-eta_normalization,[],[f117])).
% 1.70/0.91 thf(f119,plain,(
% 1.70/0.91 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = (((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK3 @ X1) @ Y0) => (p1 @ Y0))))) | (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK3 @ X1) @ Y0) => (f @ Y0))))))) | ($true = ((f @ X2)))) )),
% 1.70/0.91 inference(imp_proxy_clausification,[],[f118])).
% 1.70/0.91 thf(f121,plain,(
% 1.70/0.91 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((irel @ (sK3 @ X1) @ Y0) => (f @ Y0)))))) | ($true = ((f @ X2)))) )),
% 1.70/0.91 inference(or_proxy_clausification,[],[f119])).
% 1.70/0.91 thf(f122,plain,(
% 1.70/0.91 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: ((irel @ (sK3 @ X1) @ Y0) => (p1 @ Y0))))))) | ($true = ((f @ X2)))) )),
% 1.70/0.91 inference(or_proxy_clausification,[],[f119])).
% 1.70/0.91 thf(f123,plain,(
% 1.70/0.91 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((irel @ (sK3 @ X1) @ Y0) => (p1 @ Y0)))))) | ($true = ((f @ X2)))) )),
% 1.70/0.91 inference(not_proxy_clausification,[],[f122])).
% 1.70/0.91 thf(f124,plain,(
% 1.70/0.91 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = (((^[Y0 : $i]: ((irel @ (sK3 @ X1) @ Y0) => (p1 @ Y0))) @ X3))) | ($true = ((f @ X2)))) )),
% 1.70/0.91 inference(pi_proxy_clausification,[],[f123])).
% 1.70/0.91 thf(f125,plain,(
% 1.70/0.91 ( ! [X2 : $i,X3 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($true = (((irel @ (sK3 @ X1) @ X3) => (p1 @ X3)))) | ($true = ((f @ X2)))) )),
% 1.70/0.91 inference(beta-eta_normalization,[],[f124])).
% 1.70/0.91 thf(f126,plain,(
% 1.70/0.91 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((irel @ (sK3 @ X1) @ X3))) | (((irel @ X1 @ X2)) = $false) | ($true = ((f @ X2))) | ($true = ((p1 @ X3)))) )),
% 1.70/0.91 inference(imp_proxy_clausification,[],[f125])).
% 1.70/0.91 thf(f127,plain,(
% 1.70/0.91 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = (((^[Y0 : $i]: ((irel @ (sK3 @ X1) @ Y0) => (f @ Y0))) @ (sK4 @ X1)))) | ($true = ((f @ X2)))) )),
% 1.70/0.91 inference(sigma_proxy_clausification,[],[f121])).
% 1.70/0.91 thf(f128,plain,(
% 1.70/0.91 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = (((irel @ (sK3 @ X1) @ (sK4 @ X1)) => (f @ (sK4 @ X1))))) | ($true = ((f @ X2)))) )),
% 1.70/0.91 inference(beta-eta_normalization,[],[f127])).
% 1.70/0.91 thf(f129,plain,(
% 1.70/0.91 ( ! [X2 : $i,X1 : $i] : ((((irel @ X1 @ X2)) = $false) | ($false = ((f @ (sK4 @ X1)))) | ($true = ((f @ X2)))) )),
% 1.70/0.91 inference(imp_proxy_clausification,[],[f128])).
% 1.70/0.91 thf(f130,plain,(
% 1.70/0.91 ( ! [X2 : $i,X1 : $i] : (($true = ((irel @ (sK3 @ X1) @ (sK4 @ X1)))) | (((irel @ X1 @ X2)) = $false) | ($true = ((f @ X2)))) )),
% 1.70/0.91 inference(imp_proxy_clausification,[],[f128])).
% 1.70/0.91 thf(f142,plain,(
% 1.70/0.91 ( ! [X0 : $i] : (($true = $false) | ($false = ((p1 @ (sK2 @ X0)))) | ($true = ((f @ X0)))) )),
% 1.70/0.91 inference(constrained_superposition,[],[f62,f115])).
% 1.70/0.91 thf(f143,plain,(
% 1.70/0.91 ( ! [X0 : $i] : (($false = ((p1 @ (sK2 @ X0)))) | ($true = ((f @ X0)))) )),
% 1.70/0.91 inference(trivial_inequality_removal,[],[f142])).
% 1.70/0.91 thf(f150,plain,(
% 1.70/0.91 ( ! [X0 : $i] : (($true = $false) | ($false = ((f @ (sK4 @ X0)))) | ($true = ((f @ X0)))) )),
% 1.70/0.91 inference(constrained_superposition,[],[f62,f129])).
% 1.70/0.91 thf(f151,plain,(
% 1.70/0.91 ( ! [X0 : $i] : (($false = ((f @ (sK4 @ X0)))) | ($true = ((f @ X0)))) )),
% 1.70/0.91 inference(trivial_inequality_removal,[],[f150])).
% 1.70/0.91 thf(f163,plain,(
% 1.70/0.91 ( ! [X0 : $i] : (($true = $false) | ($true = ((irel @ X0 @ (sK1 @ X0)))) | ($true = ((f @ X0)))) )),
% 1.70/0.91 inference(constrained_superposition,[],[f62,f110])).
% 1.70/0.91 thf(f166,plain,(
% 1.70/0.91 ( ! [X0 : $i] : (($true = ((irel @ X0 @ (sK1 @ X0)))) | ($true = ((f @ X0)))) )),
% 1.70/0.91 inference(trivial_inequality_removal,[],[f163])).
% 1.70/0.91 thf(f184,plain,(
% 1.70/0.91 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != $true) | ($true = ((irel @ X2 @ X1))) | ($true != ((irel @ X2 @ X0))) | (((irel @ X0 @ X1)) = $false)) )),
% 1.70/0.91 inference(constrained_superposition,[],[f63,f86])).
% 1.70/0.91 thf(f193,plain,(
% 1.70/0.91 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((irel @ X2 @ X0))) | ($true = ((irel @ X2 @ X1))) | (((irel @ X0 @ X1)) = $false)) )),
% 1.70/0.91 inference(trivial_inequality_removal,[],[f184])).
% 1.70/0.91 thf(f229,plain,(
% 1.70/0.91 ( ! [X0 : $i,X1 : $i] : (($true != $true) | (((irel @ X0 @ X1)) = $true) | ($false = ((irel @ (sK1 @ X0) @ X1))) | ($true = ((f @ X0)))) )),
% 1.70/0.91 inference(constrained_superposition,[],[f193,f166])).
% 1.70/0.91 thf(f234,plain,(
% 1.70/0.91 ( ! [X0 : $i,X1 : $i] : (($false = ((irel @ (sK1 @ X0) @ X1))) | (((irel @ X0 @ X1)) = $true) | ($true = ((f @ X0)))) )),
% 1.70/0.91 inference(trivial_inequality_removal,[],[f229])).
% 1.70/0.91 thf(f392,plain,(
% 1.70/0.91 ( ! [X0 : $i] : (($true = $false) | ($true = ((irel @ (sK1 @ X0) @ (sK2 @ X0)))) | ($true = ((f @ X0)))) )),
% 1.70/0.91 inference(constrained_superposition,[],[f62,f116])).
% 1.70/0.91 thf(f407,plain,(
% 1.70/0.91 ( ! [X0 : $i] : (($true = ((irel @ (sK1 @ X0) @ (sK2 @ X0)))) | ($true = ((f @ X0)))) )),
% 1.70/0.91 inference(trivial_inequality_removal,[],[f392])).
% 1.70/0.91 thf(f448,plain,(
% 1.70/0.91 ( ! [X0 : $i] : (($true = $false) | ($true = ((irel @ X0 @ (sK2 @ X0)))) | ($true = ((f @ X0))) | ($true = ((f @ X0)))) )),
% 1.70/0.91 inference(constrained_superposition,[],[f234,f407])).
% 1.70/0.91 thf(f449,plain,(
% 1.70/0.91 ( ! [X0 : $i] : (($true = $false) | ($true = ((irel @ X0 @ (sK2 @ X0)))) | ($true = ((f @ X0)))) )),
% 1.70/0.91 inference(duplicate_literal_removal,[],[f448])).
% 1.70/0.91 thf(f450,plain,(
% 1.70/0.91 ( ! [X0 : $i] : (($true = ((irel @ X0 @ (sK2 @ X0)))) | ($true = ((f @ X0)))) )),
% 1.70/0.91 inference(trivial_inequality_removal,[],[f449])).
% 1.70/0.91 thf(f475,plain,(
% 1.70/0.91 ( ! [X0 : $i,X1 : $i] : (($true != $true) | ($true = ((irel @ X1 @ (sK2 @ X0)))) | ($true != ((irel @ X1 @ X0))) | ($true = ((f @ X0)))) )),
% 1.70/0.91 inference(constrained_superposition,[],[f63,f450])).
% 1.70/0.91 thf(f494,plain,(
% 1.70/0.91 ( ! [X0 : $i,X1 : $i] : (($true != ((irel @ X1 @ X0))) | ($true = ((irel @ X1 @ (sK2 @ X0)))) | ($true = ((f @ X0)))) )),
% 1.70/0.91 inference(trivial_inequality_removal,[],[f475])).
% 1.70/0.91 thf(f1427,plain,(
% 1.70/0.91 ( ! [X0 : $i] : (($true = $false) | ($true = ((irel @ (sK3 @ X0) @ (sK4 @ X0)))) | ($true = ((f @ X0)))) )),
% 1.70/0.91 inference(constrained_superposition,[],[f62,f130])).
% 1.70/0.91 thf(f1479,plain,(
% 1.70/0.91 ( ! [X0 : $i] : (($true = ((irel @ (sK3 @ X0) @ (sK4 @ X0)))) | ($true = ((f @ X0)))) )),
% 1.70/0.91 inference(trivial_inequality_removal,[],[f1427])).
% 1.70/0.91 thf(f1548,plain,(
% 1.70/0.91 ( ! [X0 : $i] : (($true != $true) | ($true = ((irel @ (sK3 @ X0) @ (sK2 @ (sK4 @ X0))))) | ($true = ((f @ (sK4 @ X0)))) | ($true = ((f @ X0)))) )),
% 1.70/0.91 inference(constrained_superposition,[],[f494,f1479])).
% 1.70/0.91 thf(f1554,plain,(
% 1.70/0.91 ( ! [X0 : $i] : (($true = ((irel @ (sK3 @ X0) @ (sK2 @ (sK4 @ X0))))) | ($true = ((f @ (sK4 @ X0)))) | ($true = ((f @ X0)))) )),
% 1.70/0.91 inference(trivial_inequality_removal,[],[f1548])).
% 1.70/0.91 thf(f6515,plain,(
% 1.70/0.91 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((irel @ (sK3 @ X0) @ X1))) | ($true = ((f @ X0))) | ($true = ((p1 @ X1)))) )),
% 1.70/0.91 inference(constrained_superposition,[],[f62,f126])).
% 1.70/0.91 thf(f6659,plain,(
% 1.70/0.91 ( ! [X0 : $i,X1 : $i] : (($false = ((irel @ (sK3 @ X0) @ X1))) | ($true = ((f @ X0))) | ($true = ((p1 @ X1)))) )),
% 1.70/0.91 inference(trivial_inequality_removal,[],[f6515])).
% 1.70/0.91 thf(f6910,plain,(
% 1.70/0.91 ( ! [X0 : $i] : (($true = $false) | ($true = ((f @ (sK4 @ X0)))) | ($true = ((f @ X0))) | ($true = ((f @ X0))) | ($true = ((p1 @ (sK2 @ (sK4 @ X0)))))) )),
% 1.70/0.91 inference(constrained_superposition,[],[f1554,f6659])).
% 1.70/0.91 thf(f6922,plain,(
% 1.70/0.91 ( ! [X0 : $i] : (($true = $false) | ($true = ((f @ (sK4 @ X0)))) | ($true = ((f @ X0))) | ($true = ((p1 @ (sK2 @ (sK4 @ X0)))))) )),
% 1.70/0.91 inference(duplicate_literal_removal,[],[f6910])).
% 1.70/0.91 thf(f6923,plain,(
% 1.70/0.91 ( ! [X0 : $i] : (($true = ((p1 @ (sK2 @ (sK4 @ X0))))) | ($true = ((f @ X0))) | ($true = ((f @ (sK4 @ X0))))) )),
% 1.70/0.91 inference(trivial_inequality_removal,[],[f6922])).
% 1.70/0.91 thf(f7306,plain,(
% 1.70/0.91 ( ! [X0 : $i] : (($true = $false) | ($true = ((f @ (sK4 @ X0)))) | ($true = ((f @ X0))) | ($true = ((f @ (sK4 @ X0))))) )),
% 1.70/0.91 inference(constrained_superposition,[],[f143,f6923])).
% 1.70/0.91 thf(f7307,plain,(
% 1.70/0.91 ( ! [X0 : $i] : (($true = $false) | ($true = ((f @ (sK4 @ X0)))) | ($true = ((f @ X0)))) )),
% 1.70/0.91 inference(duplicate_literal_removal,[],[f7306])).
% 1.70/0.91 thf(f7308,plain,(
% 1.70/0.91 ( ! [X0 : $i] : (($true = ((f @ (sK4 @ X0)))) | ($true = ((f @ X0)))) )),
% 1.70/0.91 inference(trivial_inequality_removal,[],[f7307])).
% 1.70/0.91 thf(f7316,plain,(
% 1.70/0.91 ( ! [X0 : $i] : (($true = $false) | ($true = ((f @ X0))) | ($true = ((f @ X0)))) )),
% 1.70/0.91 inference(constrained_superposition,[],[f151,f7308])).
% 1.70/0.91 thf(f7325,plain,(
% 1.70/0.91 ( ! [X0 : $i] : (($true = $false) | ($true = ((f @ X0)))) )),
% 1.70/0.91 inference(duplicate_literal_removal,[],[f7316])).
% 1.70/0.91 thf(f7326,plain,(
% 1.70/0.91 ( ! [X0 : $i] : (($true = ((f @ X0)))) )),
% 1.70/0.91 inference(trivial_inequality_removal,[],[f7325])).
% 1.70/0.91 thf(f7334,plain,(
% 1.70/0.91 ($true = $false)),
% 1.70/0.91 inference(constrained_superposition,[],[f99,f7326])).
% 1.70/0.91 thf(f7335,plain,(
% 1.70/0.91 $false),
% 1.70/0.91 inference(trivial_inequality_removal,[],[f7334])).
% 1.70/0.91 % SZS output end Proof for theBenchmark
% 1.70/0.91 % (3588265)------------------------------
% 1.70/0.91 % (3588265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.70/0.91 % (3588265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.70/0.91 % (3588265)CaDiCaL version: 2.1.3
% 1.70/0.91 % (3588265)Termination reason: Refutation
% 1.70/0.91 % (3588265)Time elapsed: 0.462 s
% 1.70/0.91 % (3588265)Peak memory usage: 14 MB
% 1.70/0.91 % (3588265)Instructions burned: 572 (million)
% 1.70/0.91 % (3588242)Success in time 0.662 s
% 1.70/0.91 % Vampire exiting
%------------------------------------------------------------------------------