%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU774^2 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n014.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:33:21 AM UTC 2026
% Result : Theorem 2.49s 0.62s
% Output : Refutation 2.49s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU774^2 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.06/0.16 % Computer : n014.cluster.edu
% 0.06/0.16 % Model : x86_64 x86_64
% 0.06/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.16 % Memory : 8046.5625MB
% 0.06/0.16 % OS : Linux 6.8.0-71-generic
% 0.06/0.17 % CPULimit : 300
% 0.06/0.17 % WCLimit : 300
% 0.06/0.17 % DateTime : Tue Sep 29 14:27:37 UTC 2026
% 0.06/0.17 % CPUTime :
% 0.06/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.06/0.20 Running first-order model finding
% 0.06/0.20 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.49/0.62 % (2740800)Will run a generic schedule for satisfiability detection.
% 2.49/0.62 % (2740806)% WARNING: option uhcvi not known.
% 2.49/0.62 % (2740806)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1557210243:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 2.49/0.62 % (2740806)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.49/0.62 % (2740806)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 2.49/0.62 % (2740805)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2303861537_2999 on theBenchmark for (2999ds/0Mi)
% 2.49/0.62 % (2740808)dis+10_1_sil=32000:sp=arity:random_seed=3569960968:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 2.49/0.62 % (2740811)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3218113481:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 2.49/0.62 % (2740809)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2158094681:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 2.49/0.62 % (2740810)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2947934540:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 2.49/0.62 % (2740807)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2097513494:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 2.49/0.62 % (2740809)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.49/0.62 % Exception at run slice level
% 2.49/0.62 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.49/0.62 % (2740819)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2323620785:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 2.49/0.62 % Exception at run slice level
% 2.49/0.62 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.49/0.62 % (2740821)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=417693403:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 2.49/0.62 % (2740808)Instruction limit reached!
% 2.49/0.62 % (2740808)------------------------------
% 2.49/0.62 % (2740808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.49/0.62 % (2740808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.49/0.62 % (2740808)CaDiCaL version: 2.1.3
% 2.49/0.62 % (2740808)Termination reason: Instruction limit
% 2.49/0.62 % (2740808)Termination phase: Saturation
% 2.49/0.62 % (2740808)Time elapsed: 0.049 s
% 2.49/0.62 % (2740808)Peak memory usage: 12 MB
% 2.49/0.62 % (2740808)Instructions burned: 103 (million)
% 2.49/0.62 % (2740809)Instruction limit reached!
% 2.49/0.62 % (2740809)------------------------------
% 2.49/0.62 % (2740809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.49/0.62 % (2740809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.49/0.62 % (2740809)CaDiCaL version: 2.1.3
% 2.49/0.62 % (2740809)Termination reason: Instruction limit
% 2.49/0.62 % (2740809)Termination phase: Saturation
% 2.49/0.62 % (2740809)Time elapsed: 0.059 s
% 2.49/0.62 % (2740809)Peak memory usage: 12 MB
% 2.49/0.62 % (2740809)Instructions burned: 117 (million)
% 2.49/0.62 % (2740810)Instruction limit reached!
% 2.49/0.62 % (2740810)------------------------------
% 2.49/0.62 % (2740810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.49/0.62 % (2740810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.49/0.62 % (2740810)CaDiCaL version: 2.1.3
% 2.49/0.62 % (2740810)Termination reason: Instruction limit
% 2.49/0.62 % (2740810)Termination phase: Saturation
% 2.49/0.62 % (2740810)Time elapsed: 0.063 s
% 2.49/0.62 % (2740810)Peak memory usage: 12 MB
% 2.49/0.62 % (2740810)Instructions burned: 132 (million)
% 2.49/0.62 % (2740823)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=1965605334:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 2.49/0.62 % (2740823)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.49/0.62 % (2740823)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 2.49/0.62 % (2740811)Instruction limit reached!
% 2.49/0.62 % (2740811)------------------------------
% 2.49/0.62 % (2740811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.49/0.62 % (2740811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.49/0.62 % (2740811)CaDiCaL version: 2.1.3
% 2.49/0.62 % (2740811)Termination reason: Instruction limit
% 2.49/0.62 % (2740811)Termination phase: Saturation
% 2.49/0.62 % (2740811)Time elapsed: 0.078 s
% 2.49/0.62 % (2740811)Peak memory usage: 13 MB
% 2.49/0.62 % (2740811)Instructions burned: 160 (million)
% 2.49/0.62 % (2740824)ott-21_1_sil=16000:fs=off:random_seed=429777545:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 2.49/0.62 % (2740825)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=368498426:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 2.49/0.62 % (2740828)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3592452387:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 2.49/0.62 % Exception at run slice level
% 2.49/0.62 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.49/0.62 % (2740821)Instruction limit reached!
% 2.49/0.62 % (2740821)------------------------------
% 2.49/0.62 % (2740821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.49/0.62 % (2740821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.49/0.62 % (2740821)CaDiCaL version: 2.1.3
% 2.49/0.62 % (2740821)Termination reason: Instruction limit
% 2.49/0.62 % (2740821)Termination phase: Saturation
% 2.49/0.62 % (2740821)Time elapsed: 0.068 s
% 2.49/0.62 % (2740821)Peak memory usage: 12 MB
% 2.49/0.62 % (2740821)Instructions burned: 138 (million)
% 2.49/0.62 % (2740831)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1291836085:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 2.49/0.62 % (2740832)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3920621918:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 2.49/0.62 % Exception at run slice level
% 2.49/0.62 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.49/0.62 % (2740835)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=3768914514:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 2.49/0.62 % (2740835)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.49/0.62 % (2740824)Instruction limit reached!
% 2.49/0.62 % (2740824)------------------------------
% 2.49/0.62 % (2740824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.49/0.62 % (2740824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.49/0.62 % (2740824)CaDiCaL version: 2.1.3
% 2.49/0.62 % (2740824)Termination reason: Instruction limit
% 2.49/0.62 % (2740824)Termination phase: Saturation
% 2.49/0.62 % (2740824)Time elapsed: 0.078 s
% 2.49/0.62 % (2740824)Peak memory usage: 13 MB
% 2.49/0.62 % (2740824)Instructions burned: 182 (million)
% 2.49/0.62 % (2740837)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1289205562:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 2.49/0.62 % (2740837)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.49/0.62 % (2740825)Instruction limit reached!
% 2.49/0.62 % (2740825)------------------------------
% 2.49/0.62 % (2740825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.49/0.62 % (2740825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.49/0.62 % (2740825)CaDiCaL version: 2.1.3
% 2.49/0.62 % (2740825)Termination reason: Instruction limit
% 2.49/0.62 % (2740825)Termination phase: Saturation
% 2.49/0.62 % (2740825)Time elapsed: 0.257 s
% 2.49/0.62 % (2740825)Peak memory usage: 13 MB
% 2.49/0.62 % (2740825)Instructions burned: 479 (million)
% 2.49/0.62 % (2740839)fmb+10_1_sil=64000:random_seed=3589138616:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 2.49/0.62 % (2740823) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2740800-2740823"...
% 2.49/0.62 % (2740839)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 2.49/0.62 % Exception at run slice level
% 2.49/0.62 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.49/0.62 % (2740823)...printing done.
% 2.49/0.62 % (2740823)Refutation found. Thanks to Tanya!
% 2.49/0.62 % SZS status Theorem for theBenchmark
% 2.49/0.62 % SZS output start Proof for theBenchmark
% 2.49/0.62 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 2.49/0.62 thf(func_def_0, type, in: ($i > $i > $o)).
% 2.49/0.62 thf(func_def_1, type, subset: ($i > $i > $o)).
% 2.49/0.62 thf(func_def_2, type, kpair: ($i > $i > $i)).
% 2.49/0.62 thf(func_def_3, type, cartprod: ($i > $i > $i)).
% 2.49/0.62 thf(func_def_4, type, breln: ($i > $i > $i > $o)).
% 2.49/0.62 thf(func_def_6, type, eqbreln: $o).
% 2.49/0.62 thf(func_def_7, type, breln1: ($i > $i > $o)).
% 2.49/0.62 thf(func_def_8, type, db0: !>[X0: $tType]:(X0)).
% 2.49/0.62 thf(func_def_9, type, db2: !>[X0: $tType]:(X0)).
% 2.49/0.62 thf(func_def_10, type, db1: !>[X0: $tType]:(X0)).
% 2.49/0.62 thf(func_def_11, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 2.49/0.62 thf(func_def_12, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 2.49/0.62 thf(func_def_13, type, vIMP: ($o > $o > $o)).
% 2.49/0.62 thf(func_def_14, type, db4: !>[X0: $tType]:(X0)).
% 2.49/0.62 thf(func_def_15, type, db5: !>[X0: $tType]:(X0)).
% 2.49/0.62 thf(func_def_16, type, db3: !>[X0: $tType]:(X0)).
% 2.49/0.62 thf(func_def_17, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 2.49/0.62 thf(func_def_23, type, vNOT: ($o > $o)).
% 2.49/0.62 thf(func_def_24, type, sK3: ($i > $i > $i > $i > $i)).
% 2.49/0.62 thf(func_def_25, type, sK4: ($i > $i > $i > $i > $i)).
% 2.49/0.62 thf(func_def_26, type, sK5: ($i > $i > $i > $i > $i)).
% 2.49/0.62 thf(func_def_27, type, sK6: ($i > $i > $i > $i > $i)).
% 2.49/0.62 thf(func_def_28, type, sK7: ($i > $i > $i > $i > $i)).
% 2.49/0.62 thf(f1,axiom,(
% 2.49/0.62 (breln = (^[X0 : $i, X1 : $i, X2 : $i] : ((subset @ X2 @ (cartprod @ X0 @ X1)))))),
% 2.49/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p',breln)).
% 2.49/0.62 thf(f2,axiom,(
% 2.49/0.62 (eqbreln = ! [X0 : $i,X1 : $i,X2 : $i] : ((breln @ X0 @ X1 @ X2) => ! [X3 : $i] : ((breln @ X0 @ X1 @ X3) => (! [X4 : $i] : ((in @ X4 @ X0) => ! [X5 : $i] : ((in @ X5 @ X1) => ((in @ (kpair @ X4 @ X5) @ X2) => (in @ (kpair @ X4 @ X5) @ X3)))) => (! [X4 : $i] : ((in @ X4 @ X0) => ! [X5 : $i] : ((in @ X5 @ X1) => ((in @ (kpair @ X4 @ X5) @ X3) => (in @ (kpair @ X4 @ X5) @ X2)))) => (X2 = X3))))))),
% 2.49/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p',eqbreln)).
% 2.49/0.62 thf(f3,axiom,(
% 2.49/0.62 (breln1 = (^[X0 : $i, X1 : $i] : ((breln @ X0 @ X0 @ X1))))),
% 2.49/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p',breln1)).
% 2.49/0.62 thf(f4,conjecture,(
% 2.49/0.62 eqbreln => ! [X0 : $i,X1 : $i] : ((breln1 @ X0 @ X1) => ! [X2 : $i] : ((breln1 @ X0 @ X2) => (! [X3 : $i] : ((in @ X3 @ X0) => ! [X4 : $i] : ((in @ X4 @ X0) => ((in @ (kpair @ X3 @ X4) @ X1) => (in @ (kpair @ X3 @ X4) @ X2)))) => (! [X3 : $i] : ((in @ X3 @ X0) => ! [X4 : $i] : ((in @ X4 @ X0) => ((in @ (kpair @ X3 @ X4) @ X2) => (in @ (kpair @ X3 @ X4) @ X1)))) => (X1 = X2)))))),
% 2.49/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p',eqbreln1)).
% 2.49/0.62 thf(f5,negated_conjecture,(
% 2.49/0.62 ~(eqbreln => ! [X0 : $i,X1 : $i] : ((breln1 @ X0 @ X1) => ! [X2 : $i] : ((breln1 @ X0 @ X2) => (! [X3 : $i] : ((in @ X3 @ X0) => ! [X4 : $i] : ((in @ X4 @ X0) => ((in @ (kpair @ X3 @ X4) @ X1) => (in @ (kpair @ X3 @ X4) @ X2)))) => (! [X3 : $i] : ((in @ X3 @ X0) => ! [X4 : $i] : ((in @ X4 @ X0) => ((in @ (kpair @ X3 @ X4) @ X2) => (in @ (kpair @ X3 @ X4) @ X1)))) => (X1 = X2))))))),
% 2.49/0.62 inference(negated_conjecture,[status(cth)],[f4])).
% 2.49/0.62 thf(f6,plain,(
% 2.49/0.62 (breln = (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (subset @ Y2 @ (cartprod @ Y0 @ Y1))))))))),
% 2.49/0.62 inference(fool_elimination,[],[f1])).
% 2.49/0.62 thf(f7,plain,(
% 2.49/0.62 (eqbreln = ! [X0 : $i,X1 : $i,X2 : $i] : ((breln @ X0 @ X1 @ X2) => ! [X3 : $i] : ((breln @ X0 @ X1 @ X3) => (! [X4 : $i] : ((in @ X4 @ X0) => ! [X5 : $i] : ((in @ X5 @ X1) => ((in @ (kpair @ X4 @ X5) @ X2) => (in @ (kpair @ X4 @ X5) @ X3)))) => (! [X6 : $i] : ((in @ X6 @ X0) => ! [X7 : $i] : ((in @ X7 @ X1) => ((in @ (kpair @ X6 @ X7) @ X3) => (in @ (kpair @ X6 @ X7) @ X2)))) => (X2 = X3))))))),
% 2.49/0.62 inference(rectify,[],[f2])).
% 2.49/0.62 thf(f8,plain,(
% 2.49/0.62 (eqbreln = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((breln @ Y2 @ Y1 @ Y0) => (!! @ $i @ (^[Y3 : $i]: ((breln @ Y2 @ Y1 @ Y3) => ((!! @ $i @ (^[Y4 : $i]: ((in @ Y4 @ Y2) => (!! @ $i @ (^[Y5 : $i]: ((in @ Y5 @ Y1) => ((in @ (kpair @ Y4 @ Y5) @ Y0) => (in @ (kpair @ Y4 @ Y5) @ Y3)))))))) => ((!! @ $i @ (^[Y4 : $i]: ((in @ Y4 @ Y2) => (!! @ $i @ (^[Y5 : $i]: ((in @ Y5 @ Y1) => ((in @ (kpair @ Y4 @ Y5) @ Y3) => (in @ (kpair @ Y4 @ Y5) @ Y0)))))))) => (Y0 = Y3)))))))))))))))),
% 2.49/0.62 inference(fool_elimination,[],[f7])).
% 2.49/0.62 thf(f9,plain,(
% 2.49/0.62 (breln1 = (^[Y0 : $i]: ((^[Y1 : $i]: (breln @ Y0 @ Y0 @ Y1)))))),
% 2.49/0.62 inference(fool_elimination,[],[f3])).
% 2.49/0.62 thf(f10,plain,(
% 2.49/0.62 ~(eqbreln => ! [X0 : $i,X1 : $i] : ((breln1 @ X0 @ X1) => ! [X2 : $i] : ((breln1 @ X0 @ X2) => (! [X3 : $i] : ((in @ X3 @ X0) => ! [X4 : $i] : ((in @ X4 @ X0) => ((in @ (kpair @ X3 @ X4) @ X1) => (in @ (kpair @ X3 @ X4) @ X2)))) => (! [X5 : $i] : ((in @ X5 @ X0) => ! [X6 : $i] : ((in @ X6 @ X0) => ((in @ (kpair @ X5 @ X6) @ X2) => (in @ (kpair @ X5 @ X6) @ X1)))) => (X1 = X2))))))),
% 2.49/0.62 inference(rectify,[],[f5])).
% 2.49/0.62 thf(f11,plain,(
% 2.49/0.62 ~((eqbreln = $true) => ! [X0 : $i,X1 : $i] : ((((breln1 @ X0 @ X1)) = $true) => ! [X2 : $i] : ((((breln1 @ X0 @ X2)) = $true) => (! [X3 : $i] : ((((in @ X3 @ X0)) = $true) => ! [X4 : $i] : ((((in @ X4 @ X0)) = $true) => ((((in @ (kpair @ X3 @ X4) @ X1)) = $true) => (((in @ (kpair @ X3 @ X4) @ X2)) = $true)))) => (! [X5 : $i] : ((((in @ X5 @ X0)) = $true) => ! [X6 : $i] : ((((in @ X6 @ X0)) = $true) => ((((in @ (kpair @ X5 @ X6) @ X2)) = $true) => (((in @ (kpair @ X5 @ X6) @ X1)) = $true)))) => (X1 = X2))))))),
% 2.49/0.62 inference(fool_elimination,[],[f10])).
% 2.49/0.62 thf(f12,plain,(
% 2.49/0.62 ? [X0 : $i,X1 : $i] : (? [X2 : $i] : ((((X1 != X2) & ! [X5 : $i] : (! [X6 : $i] : (((((in @ (kpair @ X5 @ X6) @ X1)) = $true) | (((in @ (kpair @ X5 @ X6) @ X2)) != $true)) | (((in @ X6 @ X0)) != $true)) | (((in @ X5 @ X0)) != $true))) & ! [X3 : $i] : (! [X4 : $i] : (((((in @ (kpair @ X3 @ X4) @ X2)) = $true) | (((in @ (kpair @ X3 @ X4) @ X1)) != $true)) | (((in @ X4 @ X0)) != $true)) | (((in @ X3 @ X0)) != $true))) & (((breln1 @ X0 @ X2)) = $true)) & (((breln1 @ X0 @ X1)) = $true)) & (eqbreln = $true)),
% 2.49/0.62 inference(ennf_transformation,[],[f11])).
% 2.49/0.62 thf(f13,plain,(
% 2.49/0.62 ? [X0 : $i,X1 : $i] : (? [X2 : $i] : ((X1 != X2) & ! [X5 : $i] : (! [X6 : $i] : ((((in @ (kpair @ X5 @ X6) @ X1)) = $true) | (((in @ (kpair @ X5 @ X6) @ X2)) != $true) | (((in @ X6 @ X0)) != $true)) | (((in @ X5 @ X0)) != $true)) & ! [X3 : $i] : (! [X4 : $i] : ((((in @ (kpair @ X3 @ X4) @ X2)) = $true) | (((in @ (kpair @ X3 @ X4) @ X1)) != $true) | (((in @ X4 @ X0)) != $true)) | (((in @ X3 @ X0)) != $true)) & (((breln1 @ X0 @ X2)) = $true)) & (((breln1 @ X0 @ X1)) = $true)) & (eqbreln = $true)),
% 2.49/0.62 inference(flattening,[],[f12])).
% 2.49/0.62 thf(f14,plain,(
% 2.49/0.62 ? [X0 : $i,X1 : $i] : (? [X2 : $i] : ((X1 != X2) & ! [X3 : $i] : (! [X4 : $i] : ((((in @ (kpair @ X3 @ X4) @ X1)) = $true) | (((in @ (kpair @ X3 @ X4) @ X2)) != $true) | (((in @ X4 @ X0)) != $true)) | (((in @ X3 @ X0)) != $true)) & ! [X5 : $i] : (! [X6 : $i] : ((((in @ (kpair @ X5 @ X6) @ X2)) = $true) | (((in @ (kpair @ X5 @ X6) @ X1)) != $true) | (((in @ X6 @ X0)) != $true)) | (((in @ X5 @ X0)) != $true)) & (((breln1 @ X0 @ X2)) = $true)) & (((breln1 @ X0 @ X1)) = $true)) & (eqbreln = $true)),
% 2.49/0.62 inference(rectify,[],[f13])).
% 2.49/0.62 thf(f15,plain,(
% 2.49/0.62 (((sK1 != sK2) & ! [X3 : $i] : (! [X4 : $i] : (($true = ((in @ (kpair @ X3 @ X4) @ sK1))) | ($true != ((in @ (kpair @ X3 @ X4) @ sK2))) | ($true != ((in @ X4 @ sK0)))) | ($true != ((in @ X3 @ sK0)))) & ! [X5 : $i] : (! [X6 : $i] : (($true = ((in @ (kpair @ X5 @ X6) @ sK2))) | ($true != ((in @ (kpair @ X5 @ X6) @ sK1))) | ($true != ((in @ X6 @ sK0)))) | ($true != ((in @ X5 @ sK0)))) & ($true = ((breln1 @ sK0 @ sK2)))) & ($true = ((breln1 @ sK0 @ sK1)))) & (eqbreln = $true)),
% 2.49/0.62 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2)],[f14])).
% 2.49/0.62 thf(f16,plain,(
% 2.49/0.62 (breln = (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: (subset @ Y2 @ (cartprod @ Y0 @ Y1))))))))),
% 2.49/0.62 inference(cnf_transformation,[],[f6])).
% 2.49/0.62 thf(f17,plain,(
% 2.49/0.62 (eqbreln = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((breln @ Y2 @ Y1 @ Y0) => (!! @ $i @ (^[Y3 : $i]: ((breln @ Y2 @ Y1 @ Y3) => ((!! @ $i @ (^[Y4 : $i]: ((in @ Y4 @ Y2) => (!! @ $i @ (^[Y5 : $i]: ((in @ Y5 @ Y1) => ((in @ (kpair @ Y4 @ Y5) @ Y0) => (in @ (kpair @ Y4 @ Y5) @ Y3)))))))) => ((!! @ $i @ (^[Y4 : $i]: ((in @ Y4 @ Y2) => (!! @ $i @ (^[Y5 : $i]: ((in @ Y5 @ Y1) => ((in @ (kpair @ Y4 @ Y5) @ Y3) => (in @ (kpair @ Y4 @ Y5) @ Y0)))))))) => (Y0 = Y3)))))))))))))))),
% 2.49/0.62 inference(cnf_transformation,[],[f8])).
% 2.49/0.62 thf(f18,plain,(
% 2.49/0.62 (breln1 = (^[Y0 : $i]: ((^[Y1 : $i]: (breln @ Y0 @ Y0 @ Y1)))))),
% 2.49/0.62 inference(cnf_transformation,[],[f9])).
% 2.49/0.62 thf(f19,plain,(
% 2.49/0.62 (eqbreln = $true)),
% 2.49/0.62 inference(cnf_transformation,[],[f15])).
% 2.49/0.62 thf(f20,plain,(
% 2.49/0.62 ($true = ((breln1 @ sK0 @ sK1)))),
% 2.49/0.62 inference(cnf_transformation,[],[f15])).
% 2.49/0.62 thf(f21,plain,(
% 2.49/0.62 ($true = ((breln1 @ sK0 @ sK2)))),
% 2.49/0.62 inference(cnf_transformation,[],[f15])).
% 2.49/0.62 thf(f22,plain,(
% 2.49/0.62 ( ! [X6 : $i,X5 : $i] : (($true != ((in @ (kpair @ X5 @ X6) @ sK1))) | ($true = ((in @ (kpair @ X5 @ X6) @ sK2))) | ($true != ((in @ X6 @ sK0))) | ($true != ((in @ X5 @ sK0)))) )),
% 2.49/0.62 inference(cnf_transformation,[],[f15])).
% 2.49/0.62 thf(f23,plain,(
% 2.49/0.62 ( ! [X3 : $i,X4 : $i] : (($true != ((in @ (kpair @ X3 @ X4) @ sK2))) | ($true = ((in @ (kpair @ X3 @ X4) @ sK1))) | ($true != ((in @ X4 @ sK0))) | ($true != ((in @ X3 @ sK0)))) )),
% 2.49/0.62 inference(cnf_transformation,[],[f15])).
% 2.49/0.62 thf(f24,plain,(
% 2.49/0.62 (sK1 != sK2)),
% 2.49/0.62 inference(cnf_transformation,[],[f15])).
% 2.49/0.62 thf(f26,definition,(
% 2.49/0.62 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 2.49/0.62 introduced(theory,[fool_exhaustiveness_axiom])).
% 2.49/0.62 thf(f27,plain,(
% 2.49/0.62 (breln1 = (^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (subset @ Y4 @ (cartprod @ Y2 @ Y3))))))) @ Y0 @ Y0 @ Y1)))))),
% 2.49/0.62 inference(definition_unfolding,[],[f18,f16])).
% 2.49/0.62 thf(f28,plain,(
% 2.49/0.62 ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((^[Y3 : $i]: ((^[Y4 : $i]: ((^[Y5 : $i]: (subset @ Y5 @ (cartprod @ Y3 @ Y4))))))) @ Y2 @ Y1 @ Y0) => (!! @ $i @ (^[Y3 : $i]: (((^[Y4 : $i]: ((^[Y5 : $i]: ((^[Y6 : $i]: (subset @ Y6 @ (cartprod @ Y4 @ Y5))))))) @ Y2 @ Y1 @ Y3) => ((!! @ $i @ (^[Y4 : $i]: ((in @ Y4 @ Y2) => (!! @ $i @ (^[Y5 : $i]: ((in @ Y5 @ Y1) => ((in @ (kpair @ Y4 @ Y5) @ Y0) => (in @ (kpair @ Y4 @ Y5) @ Y3)))))))) => ((!! @ $i @ (^[Y4 : $i]: ((in @ Y4 @ Y2) => (!! @ $i @ (^[Y5 : $i]: ((in @ Y5 @ Y1) => ((in @ (kpair @ Y4 @ Y5) @ Y3) => (in @ (kpair @ Y4 @ Y5) @ Y0)))))))) => (Y0 = Y3)))))))))))))))),
% 2.49/0.62 inference(definition_unfolding,[],[f17,f19,f16,f16])).
% 2.49/0.62 thf(f29,plain,(
% 2.49/0.62 ($true = (((^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (subset @ Y4 @ (cartprod @ Y2 @ Y3))))))) @ Y0 @ Y0 @ Y1)))) @ sK0 @ sK2)))),
% 2.49/0.62 inference(definition_unfolding,[],[f21,f27])).
% 2.49/0.62 thf(f30,plain,(
% 2.49/0.62 ($true = (((^[Y0 : $i]: ((^[Y1 : $i]: ((^[Y2 : $i]: ((^[Y3 : $i]: ((^[Y4 : $i]: (subset @ Y4 @ (cartprod @ Y2 @ Y3))))))) @ Y0 @ Y0 @ Y1)))) @ sK0 @ sK1)))),
% 2.49/0.62 inference(definition_unfolding,[],[f20,f27])).
% 2.49/0.62 thf(f31,plain,(
% 2.49/0.62 ($true = ((subset @ sK1 @ (cartprod @ sK0 @ sK0))))),
% 2.49/0.62 inference(beta-eta_normalization,[],[f30])).
% 2.49/0.62 thf(f32,plain,(
% 2.49/0.62 ($true = ((subset @ sK2 @ (cartprod @ sK0 @ sK0))))),
% 2.49/0.62 inference(beta-eta_normalization,[],[f29])).
% 2.49/0.62 thf(f33,plain,(
% 2.49/0.62 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (((^[Y3 : $i]: ((^[Y4 : $i]: ((^[Y5 : $i]: (subset @ Y5 @ (cartprod @ Y3 @ Y4))))))) @ Y2 @ Y1 @ Y0) => (!! @ $i @ (^[Y3 : $i]: (((^[Y4 : $i]: ((^[Y5 : $i]: ((^[Y6 : $i]: (subset @ Y6 @ (cartprod @ Y4 @ Y5))))))) @ Y2 @ Y1 @ Y3) => ((!! @ $i @ (^[Y4 : $i]: ((in @ Y4 @ Y2) => (!! @ $i @ (^[Y5 : $i]: ((in @ Y5 @ Y1) => ((in @ (kpair @ Y4 @ Y5) @ Y0) => (in @ (kpair @ Y4 @ Y5) @ Y3)))))))) => ((!! @ $i @ (^[Y4 : $i]: ((in @ Y4 @ Y2) => (!! @ $i @ (^[Y5 : $i]: ((in @ Y5 @ Y1) => ((in @ (kpair @ Y4 @ Y5) @ Y3) => (in @ (kpair @ Y4 @ Y5) @ Y0)))))))) => (Y0 = Y3)))))))))))) @ X1)))) )),
% 2.49/0.62 inference(pi_proxy_clausification,[],[f28])).
% 2.49/0.62 thf(f34,plain,(
% 2.49/0.62 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((subset @ X1 @ (cartprod @ Y1 @ Y0)) => (!! @ $i @ (^[Y2 : $i]: ((subset @ Y2 @ (cartprod @ Y1 @ Y0)) => ((!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ Y1) => (!! @ $i @ (^[Y4 : $i]: ((in @ Y4 @ Y0) => ((in @ (kpair @ Y3 @ Y4) @ X1) => (in @ (kpair @ Y3 @ Y4) @ Y2)))))))) => ((!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ Y1) => (!! @ $i @ (^[Y4 : $i]: ((in @ Y4 @ Y0) => ((in @ (kpair @ Y3 @ Y4) @ Y2) => (in @ (kpair @ Y3 @ Y4) @ X1)))))))) => (X1 = Y2)))))))))))))) )),
% 2.49/0.62 inference(beta-eta_normalization,[],[f33])).
% 2.49/0.62 thf(f35,plain,(
% 2.49/0.62 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((subset @ X1 @ (cartprod @ Y1 @ Y0)) => (!! @ $i @ (^[Y2 : $i]: ((subset @ Y2 @ (cartprod @ Y1 @ Y0)) => ((!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ Y1) => (!! @ $i @ (^[Y4 : $i]: ((in @ Y4 @ Y0) => ((in @ (kpair @ Y3 @ Y4) @ X1) => (in @ (kpair @ Y3 @ Y4) @ Y2)))))))) => ((!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ Y1) => (!! @ $i @ (^[Y4 : $i]: ((in @ Y4 @ Y0) => ((in @ (kpair @ Y3 @ Y4) @ Y2) => (in @ (kpair @ Y3 @ Y4) @ X1)))))))) => (X1 = Y2)))))))))) @ X2)))) )),
% 2.49/0.62 inference(pi_proxy_clausification,[],[f34])).
% 2.49/0.62 thf(f36,plain,(
% 2.49/0.62 ( ! [X2 : $i,X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: ((subset @ X1 @ (cartprod @ Y0 @ X2)) => (!! @ $i @ (^[Y1 : $i]: ((subset @ Y1 @ (cartprod @ Y0 @ X2)) => ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y0) => (!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ X2) => ((in @ (kpair @ Y2 @ Y3) @ X1) => (in @ (kpair @ Y2 @ Y3) @ Y1)))))))) => ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y0) => (!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ X2) => ((in @ (kpair @ Y2 @ Y3) @ Y1) => (in @ (kpair @ Y2 @ Y3) @ X1)))))))) => (X1 = Y1)))))))))))) )),
% 2.49/0.62 inference(beta-eta_normalization,[],[f35])).
% 2.49/0.62 thf(f37,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((subset @ X1 @ (cartprod @ Y0 @ X2)) => (!! @ $i @ (^[Y1 : $i]: ((subset @ Y1 @ (cartprod @ Y0 @ X2)) => ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y0) => (!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ X2) => ((in @ (kpair @ Y2 @ Y3) @ X1) => (in @ (kpair @ Y2 @ Y3) @ Y1)))))))) => ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y0) => (!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ X2) => ((in @ (kpair @ Y2 @ Y3) @ Y1) => (in @ (kpair @ Y2 @ Y3) @ X1)))))))) => (X1 = Y1)))))))) @ X3)))) )),
% 2.49/0.62 inference(pi_proxy_clausification,[],[f36])).
% 2.49/0.62 thf(f38,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((subset @ X1 @ (cartprod @ X3 @ X2)) => (!! @ $i @ (^[Y0 : $i]: ((subset @ Y0 @ (cartprod @ X3 @ X2)) => ((!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X3) => (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ X2) => ((in @ (kpair @ Y1 @ Y2) @ X1) => (in @ (kpair @ Y1 @ Y2) @ Y0)))))))) => ((!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X3) => (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ X2) => ((in @ (kpair @ Y1 @ Y2) @ Y0) => (in @ (kpair @ Y1 @ Y2) @ X1)))))))) => (X1 = Y0)))))))))) )),
% 2.49/0.62 inference(beta-eta_normalization,[],[f37])).
% 2.49/0.62 thf(f39,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($true = ((!! @ $i @ (^[Y0 : $i]: ((subset @ Y0 @ (cartprod @ X3 @ X2)) => ((!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X3) => (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ X2) => ((in @ (kpair @ Y1 @ Y2) @ X1) => (in @ (kpair @ Y1 @ Y2) @ Y0)))))))) => ((!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X3) => (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ X2) => ((in @ (kpair @ Y1 @ Y2) @ Y0) => (in @ (kpair @ Y1 @ Y2) @ X1)))))))) => (X1 = Y0))))))))) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f38])).
% 2.49/0.62 thf(f40,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($true = (((^[Y0 : $i]: ((subset @ Y0 @ (cartprod @ X3 @ X2)) => ((!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X3) => (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ X2) => ((in @ (kpair @ Y1 @ Y2) @ X1) => (in @ (kpair @ Y1 @ Y2) @ Y0)))))))) => ((!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X3) => (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ X2) => ((in @ (kpair @ Y1 @ Y2) @ Y0) => (in @ (kpair @ Y1 @ Y2) @ X1)))))))) => (X1 = Y0))))) @ X4)))) )),
% 2.49/0.62 inference(pi_proxy_clausification,[],[f39])).
% 2.49/0.62 thf(f41,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($true = (((subset @ X4 @ (cartprod @ X3 @ X2)) => ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X3) => (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X2) => ((in @ (kpair @ Y0 @ Y1) @ X1) => (in @ (kpair @ Y0 @ Y1) @ X4)))))))) => ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X3) => (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X2) => ((in @ (kpair @ Y0 @ Y1) @ X4) => (in @ (kpair @ Y0 @ Y1) @ X1)))))))) => (X1 = X4))))))) )),
% 2.49/0.62 inference(beta-eta_normalization,[],[f40])).
% 2.49/0.62 thf(f42,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($true = (((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X3) => (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X2) => ((in @ (kpair @ Y0 @ Y1) @ X1) => (in @ (kpair @ Y0 @ Y1) @ X4)))))))) => ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X3) => (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X2) => ((in @ (kpair @ Y0 @ Y1) @ X4) => (in @ (kpair @ Y0 @ Y1) @ X1)))))))) => (X1 = X4)))))) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f41])).
% 2.49/0.62 thf(f43,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X3) => (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X2) => ((in @ (kpair @ Y0 @ Y1) @ X1) => (in @ (kpair @ Y0 @ Y1) @ X4)))))))))) | ($true = (((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X3) => (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X2) => ((in @ (kpair @ Y0 @ Y1) @ X4) => (in @ (kpair @ Y0 @ Y1) @ X1)))))))) => (X1 = X4))))) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f42])).
% 2.49/0.62 thf(f44,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($false = (((^[Y0 : $i]: ((in @ Y0 @ X3) => (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X2) => ((in @ (kpair @ Y0 @ Y1) @ X1) => (in @ (kpair @ Y0 @ Y1) @ X4))))))) @ (sK3 @ X3 @ X1 @ X4 @ X2)))) | ($true = (((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X3) => (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X2) => ((in @ (kpair @ Y0 @ Y1) @ X4) => (in @ (kpair @ Y0 @ Y1) @ X1)))))))) => (X1 = X4))))) )),
% 2.49/0.62 inference(sigma_proxy_clausification,[],[f43])).
% 2.49/0.62 thf(f45,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($false = (((^[Y0 : $i]: ((in @ Y0 @ X3) => (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X2) => ((in @ (kpair @ Y0 @ Y1) @ X1) => (in @ (kpair @ Y0 @ Y1) @ X4))))))) @ (sK3 @ X3 @ X1 @ X4 @ X2)))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X3) => (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X2) => ((in @ (kpair @ Y0 @ Y1) @ X4) => (in @ (kpair @ Y0 @ Y1) @ X1)))))))))) | ($true = ((X1 = X4)))) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f44])).
% 2.49/0.62 thf(f46,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($false = (((^[Y0 : $i]: ((in @ Y0 @ X3) => (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X2) => ((in @ (kpair @ Y0 @ Y1) @ X1) => (in @ (kpair @ Y0 @ Y1) @ X4))))))) @ (sK3 @ X3 @ X1 @ X4 @ X2)))) | ($false = (((^[Y0 : $i]: ((in @ Y0 @ X3) => (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X2) => ((in @ (kpair @ Y0 @ Y1) @ X4) => (in @ (kpair @ Y0 @ Y1) @ X1))))))) @ (sK4 @ X3 @ X1 @ X4 @ X2)))) | ($true = ((X1 = X4)))) )),
% 2.49/0.62 inference(sigma_proxy_clausification,[],[f45])).
% 2.49/0.62 thf(f47,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($false = (((^[Y0 : $i]: ((in @ Y0 @ X3) => (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X2) => ((in @ (kpair @ Y0 @ Y1) @ X1) => (in @ (kpair @ Y0 @ Y1) @ X4))))))) @ (sK3 @ X3 @ X1 @ X4 @ X2)))) | ($false = (((^[Y0 : $i]: ((in @ Y0 @ X3) => (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X2) => ((in @ (kpair @ Y0 @ Y1) @ X4) => (in @ (kpair @ Y0 @ Y1) @ X1))))))) @ (sK4 @ X3 @ X1 @ X4 @ X2)))) | (X1 = X4)) )),
% 2.49/0.62 inference(equality_proxy_clausification,[],[f46])).
% 2.49/0.62 thf(f48,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($false = (((in @ (sK3 @ X3 @ X1 @ X4 @ X2) @ X3) => (!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X2) => ((in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ Y0) @ X1) => (in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ Y0) @ X4)))))))) | ($false = (((in @ (sK4 @ X3 @ X1 @ X4 @ X2) @ X3) => (!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X2) => ((in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ Y0) @ X4) => (in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ Y0) @ X1)))))))) | (X1 = X4)) )),
% 2.49/0.62 inference(beta-eta_normalization,[],[f47])).
% 2.49/0.62 thf(f49,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X2) => ((in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ Y0) @ X1) => (in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ Y0) @ X4))))))) | ($false = (((in @ (sK4 @ X3 @ X1 @ X4 @ X2) @ X3) => (!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X2) => ((in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ Y0) @ X4) => (in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ Y0) @ X1)))))))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f48])).
% 2.49/0.62 thf(f50,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($true = ((in @ (sK3 @ X3 @ X1 @ X4 @ X2) @ X3))) | ($false = (((in @ (sK4 @ X3 @ X1 @ X4 @ X2) @ X3) => (!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X2) => ((in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ Y0) @ X4) => (in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ Y0) @ X1)))))))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f48])).
% 2.49/0.62 thf(f51,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($true = ((in @ (sK3 @ X3 @ X1 @ X4 @ X2) @ X3))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X2) => ((in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ Y0) @ X4) => (in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ Y0) @ X1))))))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f50])).
% 2.49/0.62 thf(f52,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((in @ (sK4 @ X3 @ X1 @ X4 @ X2) @ X3))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($true = ((in @ (sK3 @ X3 @ X1 @ X4 @ X2) @ X3))) | ($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f50])).
% 2.49/0.62 thf(f53,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($true = ((in @ (sK3 @ X3 @ X1 @ X4 @ X2) @ X3))) | ($false = (((^[Y0 : $i]: ((in @ Y0 @ X2) => ((in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ Y0) @ X4) => (in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ Y0) @ X1)))) @ (sK5 @ X1 @ X2 @ X3 @ X4)))) | (X1 = X4)) )),
% 2.49/0.62 inference(sigma_proxy_clausification,[],[f51])).
% 2.49/0.62 thf(f54,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($true = ((in @ (sK3 @ X3 @ X1 @ X4 @ X2) @ X3))) | ($false = (((in @ (sK5 @ X1 @ X2 @ X3 @ X4) @ X2) => ((in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ (sK5 @ X1 @ X2 @ X3 @ X4)) @ X4) => (in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ (sK5 @ X1 @ X2 @ X3 @ X4)) @ X1))))) | (X1 = X4)) )),
% 2.49/0.62 inference(beta-eta_normalization,[],[f53])).
% 2.49/0.62 thf(f55,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($true = ((in @ (sK3 @ X3 @ X1 @ X4 @ X2) @ X3))) | ($false = (((in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ (sK5 @ X1 @ X2 @ X3 @ X4)) @ X4) => (in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ (sK5 @ X1 @ X2 @ X3 @ X4)) @ X1)))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f54])).
% 2.49/0.62 thf(f56,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((in @ (sK5 @ X1 @ X2 @ X3 @ X4) @ X2))) | ($true = ((in @ (sK3 @ X3 @ X1 @ X4 @ X2) @ X3))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f54])).
% 2.49/0.62 thf(f57,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ (sK5 @ X1 @ X2 @ X3 @ X4)) @ X1))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($true = ((in @ (sK3 @ X3 @ X1 @ X4 @ X2) @ X3))) | ($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f55])).
% 2.49/0.62 thf(f58,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ (sK5 @ X1 @ X2 @ X3 @ X4)) @ X4))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($true = ((in @ (sK3 @ X3 @ X1 @ X4 @ X2) @ X3))) | ($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f55])).
% 2.49/0.62 thf(f59,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($false = (((^[Y0 : $i]: ((in @ Y0 @ X2) => ((in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ Y0) @ X1) => (in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ Y0) @ X4)))) @ (sK6 @ X1 @ X2 @ X3 @ X4)))) | ($false = (((in @ (sK4 @ X3 @ X1 @ X4 @ X2) @ X3) => (!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X2) => ((in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ Y0) @ X4) => (in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ Y0) @ X1)))))))) | (X1 = X4)) )),
% 2.49/0.62 inference(sigma_proxy_clausification,[],[f49])).
% 2.49/0.62 thf(f60,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($false = (((^[Y0 : $i]: ((in @ Y0 @ X2) => ((in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ Y0) @ X1) => (in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ Y0) @ X4)))) @ (sK6 @ X1 @ X2 @ X3 @ X4)))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X2) => ((in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ Y0) @ X4) => (in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ Y0) @ X1))))))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f59])).
% 2.49/0.62 thf(f61,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($false = (((^[Y0 : $i]: ((in @ Y0 @ X2) => ((in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ Y0) @ X1) => (in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ Y0) @ X4)))) @ (sK6 @ X1 @ X2 @ X3 @ X4)))) | ($true = ((in @ (sK4 @ X3 @ X1 @ X4 @ X2) @ X3))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f59])).
% 2.49/0.62 thf(f62,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($false = (((in @ (sK6 @ X1 @ X2 @ X3 @ X4) @ X2) => ((in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ (sK6 @ X1 @ X2 @ X3 @ X4)) @ X1) => (in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ (sK6 @ X1 @ X2 @ X3 @ X4)) @ X4))))) | ($true = ((in @ (sK4 @ X3 @ X1 @ X4 @ X2) @ X3))) | (X1 = X4)) )),
% 2.49/0.62 inference(beta-eta_normalization,[],[f61])).
% 2.49/0.62 thf(f63,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($false = (((in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ (sK6 @ X1 @ X2 @ X3 @ X4)) @ X1) => (in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ (sK6 @ X1 @ X2 @ X3 @ X4)) @ X4)))) | ($true = ((in @ (sK4 @ X3 @ X1 @ X4 @ X2) @ X3))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f62])).
% 2.49/0.62 thf(f64,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((in @ (sK6 @ X1 @ X2 @ X3 @ X4) @ X2))) | ($true = ((in @ (sK4 @ X3 @ X1 @ X4 @ X2) @ X3))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f62])).
% 2.49/0.62 thf(f65,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ (sK6 @ X1 @ X2 @ X3 @ X4)) @ X4))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($true = ((in @ (sK4 @ X3 @ X1 @ X4 @ X2) @ X3))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f63])).
% 2.49/0.62 thf(f66,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ (sK6 @ X1 @ X2 @ X3 @ X4)) @ X1))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($true = ((in @ (sK4 @ X3 @ X1 @ X4 @ X2) @ X3))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f63])).
% 2.49/0.62 thf(f67,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($false = (((^[Y0 : $i]: ((in @ Y0 @ X2) => ((in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ Y0) @ X1) => (in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ Y0) @ X4)))) @ (sK6 @ X1 @ X2 @ X3 @ X4)))) | ($false = (((^[Y0 : $i]: ((in @ Y0 @ X2) => ((in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ Y0) @ X4) => (in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ Y0) @ X1)))) @ (sK7 @ X1 @ X2 @ X3 @ X4)))) | (X1 = X4)) )),
% 2.49/0.62 inference(sigma_proxy_clausification,[],[f60])).
% 2.49/0.62 thf(f68,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($false = (((in @ (sK6 @ X1 @ X2 @ X3 @ X4) @ X2) => ((in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ (sK6 @ X1 @ X2 @ X3 @ X4)) @ X1) => (in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ (sK6 @ X1 @ X2 @ X3 @ X4)) @ X4))))) | ($false = (((in @ (sK7 @ X1 @ X2 @ X3 @ X4) @ X2) => ((in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ (sK7 @ X1 @ X2 @ X3 @ X4)) @ X4) => (in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ (sK7 @ X1 @ X2 @ X3 @ X4)) @ X1))))) | (X1 = X4)) )),
% 2.49/0.62 inference(beta-eta_normalization,[],[f67])).
% 2.49/0.62 thf(f69,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($false = (((in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ (sK6 @ X1 @ X2 @ X3 @ X4)) @ X1) => (in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ (sK6 @ X1 @ X2 @ X3 @ X4)) @ X4)))) | ($false = (((in @ (sK7 @ X1 @ X2 @ X3 @ X4) @ X2) => ((in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ (sK7 @ X1 @ X2 @ X3 @ X4)) @ X4) => (in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ (sK7 @ X1 @ X2 @ X3 @ X4)) @ X1))))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f68])).
% 2.49/0.62 thf(f70,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($true = ((in @ (sK6 @ X1 @ X2 @ X3 @ X4) @ X2))) | ($false = (((in @ (sK7 @ X1 @ X2 @ X3 @ X4) @ X2) => ((in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ (sK7 @ X1 @ X2 @ X3 @ X4)) @ X4) => (in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ (sK7 @ X1 @ X2 @ X3 @ X4)) @ X1))))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f68])).
% 2.49/0.62 thf(f71,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($true = ((in @ (sK6 @ X1 @ X2 @ X3 @ X4) @ X2))) | ($false = (((in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ (sK7 @ X1 @ X2 @ X3 @ X4)) @ X4) => (in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ (sK7 @ X1 @ X2 @ X3 @ X4)) @ X1)))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f70])).
% 2.49/0.62 thf(f72,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((in @ (sK7 @ X1 @ X2 @ X3 @ X4) @ X2))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($true = ((in @ (sK6 @ X1 @ X2 @ X3 @ X4) @ X2))) | ($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f70])).
% 2.49/0.62 thf(f73,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ (sK7 @ X1 @ X2 @ X3 @ X4)) @ X1))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($true = ((in @ (sK6 @ X1 @ X2 @ X3 @ X4) @ X2))) | ($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f71])).
% 2.49/0.62 thf(f74,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ (sK7 @ X1 @ X2 @ X3 @ X4)) @ X4))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($true = ((in @ (sK6 @ X1 @ X2 @ X3 @ X4) @ X2))) | ($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f71])).
% 2.49/0.62 thf(f75,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($false = ((in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ (sK6 @ X1 @ X2 @ X3 @ X4)) @ X4))) | ($false = (((in @ (sK7 @ X1 @ X2 @ X3 @ X4) @ X2) => ((in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ (sK7 @ X1 @ X2 @ X3 @ X4)) @ X4) => (in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ (sK7 @ X1 @ X2 @ X3 @ X4)) @ X1))))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f69])).
% 2.49/0.62 thf(f76,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($true = ((in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ (sK6 @ X1 @ X2 @ X3 @ X4)) @ X1))) | ($false = (((in @ (sK7 @ X1 @ X2 @ X3 @ X4) @ X2) => ((in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ (sK7 @ X1 @ X2 @ X3 @ X4)) @ X4) => (in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ (sK7 @ X1 @ X2 @ X3 @ X4)) @ X1))))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f69])).
% 2.49/0.62 thf(f77,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($true = ((in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ (sK6 @ X1 @ X2 @ X3 @ X4)) @ X1))) | ($false = (((in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ (sK7 @ X1 @ X2 @ X3 @ X4)) @ X4) => (in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ (sK7 @ X1 @ X2 @ X3 @ X4)) @ X1)))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f76])).
% 2.49/0.62 thf(f78,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ (sK6 @ X1 @ X2 @ X3 @ X4)) @ X1))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($true = ((in @ (sK7 @ X1 @ X2 @ X3 @ X4) @ X2))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f76])).
% 2.49/0.62 thf(f79,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ (sK7 @ X1 @ X2 @ X3 @ X4)) @ X1))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($true = ((in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ (sK6 @ X1 @ X2 @ X3 @ X4)) @ X1))) | ($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f77])).
% 2.49/0.62 thf(f80,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ (sK7 @ X1 @ X2 @ X3 @ X4)) @ X4))) | ($true = ((in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ (sK6 @ X1 @ X2 @ X3 @ X4)) @ X1))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f77])).
% 2.49/0.62 thf(f81,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($false = ((in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ (sK6 @ X1 @ X2 @ X3 @ X4)) @ X4))) | ($false = (((in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ (sK7 @ X1 @ X2 @ X3 @ X4)) @ X4) => (in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ (sK7 @ X1 @ X2 @ X3 @ X4)) @ X1)))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f75])).
% 2.49/0.62 thf(f82,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ (sK6 @ X1 @ X2 @ X3 @ X4)) @ X4))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | ($true = ((in @ (sK7 @ X1 @ X2 @ X3 @ X4) @ X2))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f75])).
% 2.49/0.62 thf(f83,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($false = ((in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ (sK7 @ X1 @ X2 @ X3 @ X4)) @ X1))) | ($false = ((in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ (sK6 @ X1 @ X2 @ X3 @ X4)) @ X4))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f81])).
% 2.49/0.62 thf(f84,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((in @ (kpair @ (sK4 @ X3 @ X1 @ X4 @ X2) @ (sK7 @ X1 @ X2 @ X3 @ X4)) @ X4))) | ($false = ((subset @ X4 @ (cartprod @ X3 @ X2)))) | ($false = ((in @ (kpair @ (sK3 @ X3 @ X1 @ X4 @ X2) @ (sK6 @ X1 @ X2 @ X3 @ X4)) @ X4))) | ($false = ((subset @ X1 @ (cartprod @ X3 @ X2)))) | (X1 = X4)) )),
% 2.49/0.62 inference(imp_proxy_clausification,[],[f81])).
% 2.49/0.62 thf(f87,plain,(
% 2.49/0.62 ( ! [X0 : $i,X1 : $i] : (($true != $true) | ($true = ((in @ (kpair @ X0 @ X1) @ sK2))) | ($true != ((in @ X1 @ sK0))) | ($true != ((in @ X0 @ sK0))) | ($false = ((in @ (kpair @ X0 @ X1) @ sK1)))) )),
% 2.49/0.62 inference(constrained_superposition,[],[f22,f26])).
% 2.49/0.62 thf(f89,plain,(
% 2.49/0.62 ( ! [X0 : $i,X1 : $i] : (($true != ((in @ X1 @ sK0))) | ($true = ((in @ (kpair @ X0 @ X1) @ sK2))) | ($true != ((in @ X0 @ sK0))) | ($false = ((in @ (kpair @ X0 @ X1) @ sK1)))) )),
% 2.49/0.62 inference(trivial_inequality_removal,[],[f87])).
% 2.49/0.62 thf(f94,plain,(
% 2.49/0.62 ( ! [X0 : $i,X1 : $i] : (($true != $true) | ($true = ((in @ (kpair @ X0 @ X1) @ sK1))) | ($true != ((in @ X1 @ sK0))) | ($true != ((in @ X0 @ sK0))) | ($false = ((in @ (kpair @ X0 @ X1) @ sK2)))) )),
% 2.49/0.62 inference(constrained_superposition,[],[f23,f26])).
% 2.49/0.62 thf(f95,plain,(
% 2.49/0.62 ( ! [X0 : $i,X1 : $i] : (($true != ((in @ X1 @ sK0))) | ($true = ((in @ (kpair @ X0 @ X1) @ sK1))) | ($true != ((in @ X0 @ sK0))) | ($false = ((in @ (kpair @ X0 @ X1) @ sK2)))) )),
% 2.49/0.62 inference(trivial_inequality_removal,[],[f94])).
% 2.49/0.62 thf(f96,plain,(
% 2.49/0.62 ( ! [X0 : $i,X1 : $i] : (($true != $true) | ($true = ((in @ (kpair @ X1 @ X0) @ sK2))) | ($true != ((in @ X1 @ sK0))) | ($false = ((in @ (kpair @ X1 @ X0) @ sK1))) | ($false = ((in @ X0 @ sK0)))) )),
% 2.49/0.62 inference(constrained_superposition,[],[f89,f26])).
% 2.49/0.62 thf(f97,plain,(
% 2.49/0.62 ( ! [X0 : $i,X1 : $i] : (($true != ((in @ X1 @ sK0))) | ($true = ((in @ (kpair @ X1 @ X0) @ sK2))) | ($false = ((in @ (kpair @ X1 @ X0) @ sK1))) | ($false = ((in @ X0 @ sK0)))) )),
% 2.49/0.62 inference(trivial_inequality_removal,[],[f96])).
% 2.49/0.62 thf(f98,plain,(
% 2.49/0.62 ( ! [X0 : $i,X1 : $i] : (($true != $true) | ($true = ((in @ (kpair @ X1 @ X0) @ sK1))) | ($true != ((in @ X1 @ sK0))) | ($false = ((in @ (kpair @ X1 @ X0) @ sK2))) | ($false = ((in @ X0 @ sK0)))) )),
% 2.49/0.62 inference(constrained_superposition,[],[f95,f26])).
% 2.49/0.62 thf(f99,plain,(
% 2.49/0.62 ( ! [X0 : $i,X1 : $i] : (($true != ((in @ X1 @ sK0))) | ($true = ((in @ (kpair @ X1 @ X0) @ sK1))) | ($false = ((in @ (kpair @ X1 @ X0) @ sK2))) | ($false = ((in @ X0 @ sK0)))) )),
% 2.49/0.62 inference(trivial_inequality_removal,[],[f98])).
% 2.49/0.62 thf(f100,plain,(
% 2.49/0.62 ( ! [X0 : $i,X1 : $i] : (($true != $true) | ($true = ((in @ (kpair @ X0 @ X1) @ sK2))) | ($false = ((in @ (kpair @ X0 @ X1) @ sK1))) | ($false = ((in @ X1 @ sK0))) | ($false = ((in @ X0 @ sK0)))) )),
% 2.49/0.62 inference(constrained_superposition,[],[f97,f26])).
% 2.49/0.62 thf(f101,plain,(
% 2.49/0.62 ( ! [X0 : $i,X1 : $i] : (($true = ((in @ (kpair @ X0 @ X1) @ sK2))) | ($false = ((in @ (kpair @ X0 @ X1) @ sK1))) | ($false = ((in @ X1 @ sK0))) | ($false = ((in @ X0 @ sK0)))) )),
% 2.49/0.62 inference(trivial_inequality_removal,[],[f100])).
% 2.49/0.62 thf(f117,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != $true) | ($true = ((in @ (kpair @ (sK4 @ sK0 @ X0 @ X1 @ X2) @ X3) @ sK2))) | ($false = ((in @ (kpair @ (sK4 @ sK0 @ X0 @ X1 @ X2) @ X3) @ sK1))) | (((in @ X3 @ sK0)) = $false) | ($false = ((subset @ X1 @ (cartprod @ sK0 @ X2)))) | ($true = ((in @ (sK3 @ sK0 @ X0 @ X1 @ X2) @ sK0))) | ($false = ((subset @ X0 @ (cartprod @ sK0 @ X2)))) | (X0 = X1)) )),
% 2.49/0.62 inference(constrained_superposition,[],[f97,f52])).
% 2.49/0.62 thf(f122,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true = ((in @ (kpair @ (sK4 @ sK0 @ X0 @ X1 @ X2) @ X3) @ sK2))) | ($false = ((in @ (kpair @ (sK4 @ sK0 @ X0 @ X1 @ X2) @ X3) @ sK1))) | (((in @ X3 @ sK0)) = $false) | ($false = ((subset @ X1 @ (cartprod @ sK0 @ X2)))) | ($true = ((in @ (sK3 @ sK0 @ X0 @ X1 @ X2) @ sK0))) | ($false = ((subset @ X0 @ (cartprod @ sK0 @ X2)))) | (X0 = X1)) )),
% 2.49/0.62 inference(trivial_inequality_removal,[],[f117])).
% 2.49/0.62 thf(f128,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != $true) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ X0 @ X1 @ X2) @ X3) @ sK1))) | ($false = ((in @ (kpair @ (sK3 @ sK0 @ X0 @ X1 @ X2) @ X3) @ sK2))) | (((in @ X3 @ sK0)) = $false) | ($true = ((in @ (sK5 @ X0 @ X2 @ sK0 @ X1) @ X2))) | ($false = ((subset @ X1 @ (cartprod @ sK0 @ X2)))) | ($false = ((subset @ X0 @ (cartprod @ sK0 @ X2)))) | (X0 = X1)) )),
% 2.49/0.62 inference(constrained_superposition,[],[f99,f56])).
% 2.49/0.62 thf(f135,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($false = ((in @ (kpair @ (sK3 @ sK0 @ X0 @ X1 @ X2) @ X3) @ sK2))) | ($true = ((in @ (sK5 @ X0 @ X2 @ sK0 @ X1) @ X2))) | (((in @ X3 @ sK0)) = $false) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ X0 @ X1 @ X2) @ X3) @ sK1))) | ($false = ((subset @ X1 @ (cartprod @ sK0 @ X2)))) | ($false = ((subset @ X0 @ (cartprod @ sK0 @ X2)))) | (X0 = X1)) )),
% 2.49/0.62 inference(trivial_inequality_removal,[],[f128])).
% 2.49/0.62 thf(f145,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != $true) | ($true = ((in @ (kpair @ (sK4 @ sK0 @ X0 @ X1 @ X2) @ X3) @ sK2))) | ($false = ((in @ (kpair @ (sK4 @ sK0 @ X0 @ X1 @ X2) @ X3) @ sK1))) | (((in @ X3 @ sK0)) = $false) | ($true = ((in @ (sK6 @ X0 @ X2 @ sK0 @ X1) @ X2))) | ($false = ((subset @ X1 @ (cartprod @ sK0 @ X2)))) | ($false = ((subset @ X0 @ (cartprod @ sK0 @ X2)))) | (X0 = X1)) )),
% 2.49/0.62 inference(constrained_superposition,[],[f97,f64])).
% 2.49/0.62 thf(f150,plain,(
% 2.49/0.62 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true = ((in @ (kpair @ (sK4 @ sK0 @ X0 @ X1 @ X2) @ X3) @ sK2))) | ($true = ((in @ (sK6 @ X0 @ X2 @ sK0 @ X1) @ X2))) | (((in @ X3 @ sK0)) = $false) | ($false = ((in @ (kpair @ (sK4 @ sK0 @ X0 @ X1 @ X2) @ X3) @ sK1))) | ($false = ((subset @ X1 @ (cartprod @ sK0 @ X2)))) | ($false = ((subset @ X0 @ (cartprod @ sK0 @ X2)))) | (X0 = X1)) )),
% 2.49/0.62 inference(trivial_inequality_removal,[],[f145])).
% 2.49/0.62 thf(f333,plain,(
% 2.49/0.62 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((subset @ X0 @ (cartprod @ sK0 @ X1)))) | ($true = ((in @ (sK3 @ sK0 @ sK2 @ X0 @ X1) @ sK0))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ X1)))) | (sK2 = X0) | ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ X0 @ X1) @ (sK5 @ sK2 @ X1 @ sK0 @ X0)) @ sK1))) | ($false = ((in @ (sK5 @ sK2 @ X1 @ sK0 @ X0) @ sK0))) | ($false = ((subset @ X0 @ (cartprod @ sK0 @ X1)))) | ($true = ((in @ (sK3 @ sK0 @ sK2 @ X0 @ X1) @ sK0))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ X1)))) | (sK2 = X0)) )),
% 2.49/0.62 inference(constrained_superposition,[],[f57,f122])).
% 2.49/0.62 thf(f337,plain,(
% 2.49/0.62 ( ! [X0 : $i,X1 : $i] : (($true = $false) | ($false = ((subset @ X0 @ (cartprod @ sK0 @ X1)))) | ($true = ((in @ (sK3 @ sK0 @ sK2 @ X0 @ X1) @ sK0))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ X1)))) | (sK2 = X0) | ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ X0 @ X1) @ (sK5 @ sK2 @ X1 @ sK0 @ X0)) @ sK1))) | ($false = ((in @ (sK5 @ sK2 @ X1 @ sK0 @ X0) @ sK0)))) )),
% 2.49/0.62 inference(duplicate_literal_removal,[],[f333])).
% 2.49/0.62 thf(f338,plain,(
% 2.49/0.62 ( ! [X0 : $i,X1 : $i] : (($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ X0 @ X1) @ (sK5 @ sK2 @ X1 @ sK0 @ X0)) @ sK1))) | ($true = ((in @ (sK3 @ sK0 @ sK2 @ X0 @ X1) @ sK0))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ X1)))) | (sK2 = X0) | ($false = ((subset @ X0 @ (cartprod @ sK0 @ X1)))) | ($false = ((in @ (sK5 @ sK2 @ X1 @ sK0 @ X0) @ sK0)))) )),
% 2.49/0.62 inference(trivial_inequality_removal,[],[f337])).
% 2.49/0.62 thf(f2183,plain,(
% 2.49/0.62 ( ! [X0 : $i] : (($true = $false) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ X0)))) | ($true = ((in @ (sK3 @ sK0 @ sK2 @ sK1 @ X0) @ sK0))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ X0)))) | (sK1 = sK2) | ($true = ((in @ (sK3 @ sK0 @ sK2 @ sK1 @ X0) @ sK0))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ X0)))) | (sK1 = sK2) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ X0)))) | ($false = ((in @ (sK5 @ sK2 @ X0 @ sK0 @ sK1) @ sK0)))) )),
% 2.49/0.62 inference(constrained_superposition,[],[f58,f338])).
% 2.49/0.62 thf(f2184,plain,(
% 2.49/0.62 ( ! [X0 : $i] : (($true = $false) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ X0)))) | ($true = ((in @ (sK3 @ sK0 @ sK2 @ sK1 @ X0) @ sK0))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ X0)))) | (sK1 = sK2) | ($false = ((in @ (sK5 @ sK2 @ X0 @ sK0 @ sK1) @ sK0)))) )),
% 2.49/0.62 inference(duplicate_literal_removal,[],[f2183])).
% 2.49/0.62 thf(f2185,plain,(
% 2.49/0.62 ( ! [X0 : $i] : (($false = ((subset @ sK1 @ (cartprod @ sK0 @ X0)))) | ($true = ((in @ (sK3 @ sK0 @ sK2 @ sK1 @ X0) @ sK0))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ X0)))) | (sK1 = sK2) | ($false = ((in @ (sK5 @ sK2 @ X0 @ sK0 @ sK1) @ sK0)))) )),
% 2.49/0.62 inference(trivial_inequality_removal,[],[f2184])).
% 2.49/0.62 thf(f2189,plain,(
% 2.49/0.62 ( ! [X0 : $i] : (($false = ((in @ (sK5 @ sK2 @ X0 @ sK0 @ sK1) @ sK0))) | ($true = ((in @ (sK3 @ sK0 @ sK2 @ sK1 @ X0) @ sK0))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ X0)))) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ X0))))) )),
% 2.49/0.62 inference(forward_subsumption_resolution,[],[f2185,f24])).
% 2.49/0.62 thf(f2200,plain,(
% 2.49/0.62 ( ! [X0 : $i] : (($true = $false) | ($false = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK2))) | ($false = ((in @ X0 @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK1))) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | (sK1 = sK2) | ($true = ((in @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ sK0))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0))))) )),
% 2.49/0.62 inference(constrained_superposition,[],[f135,f2189])).
% 2.49/0.62 thf(f2220,plain,(
% 2.49/0.62 ( ! [X0 : $i] : (($true = $false) | ($false = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK2))) | ($false = ((in @ X0 @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK1))) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | (sK1 = sK2) | ($true = ((in @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ sK0)))) )),
% 2.49/0.62 inference(duplicate_literal_removal,[],[f2200])).
% 2.49/0.62 thf(f2221,plain,(
% 2.49/0.62 ( ! [X0 : $i] : (($false = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK2))) | ($false = ((in @ X0 @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK1))) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | (sK1 = sK2) | ($true = ((in @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ sK0)))) )),
% 2.49/0.62 inference(trivial_inequality_removal,[],[f2220])).
% 2.49/0.62 thf(f2240,plain,(
% 2.49/0.62 ( ! [X0 : $i] : (($false = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK2))) | ($false = ((in @ X0 @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK1))) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | (sK1 = sK2)) )),
% 2.49/0.62 inference(forward_subsumption_resolution,[],[f2221,f99])).
% 2.49/0.62 thf(f2250,plain,(
% 2.49/0.62 ( ! [X0 : $i] : (($false = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK2))) | ($false = ((in @ X0 @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK1))) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0))))) )),
% 2.49/0.62 inference(forward_subsumption_resolution,[],[f2240,f24])).
% 2.49/0.62 thf(f2267,plain,(
% 2.49/0.62 ( ! [X0 : $i] : (($true = $false) | ($false = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK2))) | ($false = ((in @ X0 @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK1))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0))))) )),
% 2.49/0.62 inference(forward_demodulation,[],[f2250,f31])).
% 2.49/0.62 thf(f2268,plain,(
% 2.49/0.62 ( ! [X0 : $i] : (($false = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK2))) | ($false = ((in @ X0 @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK1))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0))))) )),
% 2.49/0.62 inference(trivial_inequality_removal,[],[f2267])).
% 2.49/0.62 thf(f2287,plain,(
% 2.49/0.62 ( ! [X0 : $i] : (($true = $false) | ($false = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK2))) | ($false = ((in @ X0 @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK1)))) )),
% 2.49/0.62 inference(forward_demodulation,[],[f2268,f32])).
% 2.49/0.62 thf(f2288,plain,(
% 2.49/0.62 ( ! [X0 : $i] : (($false = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK2))) | ($false = ((in @ X0 @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK1)))) )),
% 2.49/0.62 inference(trivial_inequality_removal,[],[f2287])).
% 2.49/0.62 thf(f2377,plain,(
% 2.49/0.62 ($true = $false) | ($false = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($true = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | (sK1 = sK2)),
% 2.49/0.62 inference(constrained_superposition,[],[f2288,f80])).
% 2.49/0.62 thf(f2378,plain,(
% 2.49/0.62 ($true = $false) | ($false = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | (sK1 = sK2)),
% 2.49/0.62 inference(constrained_superposition,[],[f2288,f78])).
% 2.49/0.62 thf(f2379,plain,(
% 2.49/0.62 ($true = $false) | ($false = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ sK0))) | (sK1 = sK2)),
% 2.49/0.62 inference(constrained_superposition,[],[f2288,f66])).
% 2.49/0.62 thf(f2432,plain,(
% 2.49/0.62 ($false = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ sK0))) | (sK1 = sK2)),
% 2.49/0.62 inference(trivial_inequality_removal,[],[f2379])).
% 2.49/0.62 thf(f2433,plain,(
% 2.49/0.62 ($false = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | (sK1 = sK2)),
% 2.49/0.62 inference(trivial_inequality_removal,[],[f2378])).
% 2.49/0.62 thf(f2434,plain,(
% 2.49/0.62 ($false = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($true = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | (sK1 = sK2)),
% 2.49/0.62 inference(trivial_inequality_removal,[],[f2377])).
% 2.49/0.62 thf(f2438,plain,(
% 2.49/0.62 ($false = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ sK0)))),
% 2.49/0.62 inference(forward_subsumption_resolution,[],[f2432,f24])).
% 2.49/0.62 thf(f2439,plain,(
% 2.49/0.62 ($false = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0)))),
% 2.49/0.62 inference(forward_subsumption_resolution,[],[f2433,f24])).
% 2.49/0.62 thf(f2440,plain,(
% 2.49/0.62 ($false = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($true = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0))))),
% 2.49/0.62 inference(forward_subsumption_resolution,[],[f2434,f24])).
% 2.49/0.62 thf(f2447,plain,(
% 2.49/0.62 ($true = $false) | ($false = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ sK0)))),
% 2.49/0.62 inference(forward_demodulation,[],[f2438,f31])).
% 2.49/0.62 thf(f2448,plain,(
% 2.49/0.62 ($false = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ sK0)))),
% 2.49/0.62 inference(trivial_inequality_removal,[],[f2447])).
% 2.49/0.62 thf(f2449,plain,(
% 2.49/0.62 ($true = $false) | ($false = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0)))),
% 2.49/0.62 inference(forward_demodulation,[],[f2439,f31])).
% 2.49/0.62 thf(f2450,plain,(
% 2.49/0.62 ($false = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0)))),
% 2.49/0.62 inference(trivial_inequality_removal,[],[f2449])).
% 2.49/0.62 thf(f2451,plain,(
% 2.49/0.62 ($true = $false) | ($false = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($true = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0))))),
% 2.49/0.62 inference(forward_demodulation,[],[f2440,f31])).
% 2.49/0.62 thf(f2452,plain,(
% 2.49/0.62 ($false = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($true = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0))))),
% 2.49/0.62 inference(trivial_inequality_removal,[],[f2451])).
% 2.49/0.62 thf(f2459,plain,(
% 2.49/0.62 ($true = $false) | ($false = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($true = ((in @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ sK0)))),
% 2.49/0.62 inference(forward_demodulation,[],[f2448,f32])).
% 2.49/0.62 thf(f2460,plain,(
% 2.49/0.62 ($false = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($true = ((in @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ sK0)))),
% 2.49/0.62 inference(trivial_inequality_removal,[],[f2459])).
% 2.49/0.62 thf(f2461,plain,(
% 2.49/0.62 ($true = $false) | ($false = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($true = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0)))),
% 2.49/0.62 inference(forward_demodulation,[],[f2450,f32])).
% 2.49/0.62 thf(f2462,plain,(
% 2.49/0.62 ($false = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($true = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0)))),
% 2.49/0.62 inference(trivial_inequality_removal,[],[f2461])).
% 2.49/0.62 thf(f2463,plain,(
% 2.49/0.62 ($true = $false) | ($false = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($true = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1)))),
% 2.49/0.62 inference(forward_demodulation,[],[f2452,f32])).
% 2.49/0.62 thf(f2464,plain,(
% 2.49/0.62 ($false = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($true = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1)))),
% 2.49/0.62 inference(trivial_inequality_removal,[],[f2463])).
% 2.49/0.62 thf(f2466,definition,(
% 2.49/0.62 spl8_4 <=> ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1)))),
% 2.49/0.62 introduced(definition,[new_symbols(definition,[spl8_4])],[avatar_definition])).
% 2.49/0.62 thf(f2467,plain,(
% 2.49/0.62 ($true != ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | spl8_4),
% 2.49/0.62 inference(avatar_component_clause,[],[f2466])).
% 2.49/0.62 thf(f2468,plain,(
% 2.49/0.62 ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ~spl8_4),
% 2.49/0.62 inference(avatar_component_clause,[],[f2466])).
% 2.49/0.62 thf(f2470,definition,(
% 2.49/0.62 spl8_5 <=> ($false = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0)))),
% 2.49/0.62 introduced(definition,[new_symbols(definition,[spl8_5])],[avatar_definition])).
% 2.49/0.62 thf(f2471,plain,(
% 2.49/0.62 ($false != ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | spl8_5),
% 2.49/0.62 inference(avatar_component_clause,[],[f2470])).
% 2.49/0.62 thf(f2472,plain,(
% 2.49/0.62 ($false = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ~spl8_5),
% 2.49/0.62 inference(avatar_component_clause,[],[f2470])).
% 2.49/0.62 thf(f2474,definition,(
% 2.49/0.62 spl8_6 <=> ($true = ((in @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ sK0)))),
% 2.49/0.62 introduced(definition,[new_symbols(definition,[spl8_6])],[avatar_definition])).
% 2.49/0.62 thf(f2476,plain,(
% 2.49/0.62 ($true = ((in @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ sK0))) | ~spl8_6),
% 2.49/0.62 inference(avatar_component_clause,[],[f2474])).
% 2.49/0.62 thf(f2479,definition,(
% 2.49/0.62 spl8_7 <=> ($true = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0)))),
% 2.49/0.62 introduced(definition,[new_symbols(definition,[spl8_7])],[avatar_definition])).
% 2.49/0.62 thf(f2481,plain,(
% 2.49/0.62 ($true = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ~spl8_7),
% 2.49/0.62 inference(avatar_component_clause,[],[f2479])).
% 2.49/0.62 thf(f2484,definition,(
% 2.49/0.62 spl8_8 <=> ($true = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1)))),
% 2.49/0.62 introduced(definition,[new_symbols(definition,[spl8_8])],[avatar_definition])).
% 2.49/0.62 thf(f2486,plain,(
% 2.49/0.62 ($true = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ~spl8_8),
% 2.49/0.62 inference(avatar_component_clause,[],[f2484])).
% 2.49/0.62 thf(f2488,plain,(
% 2.49/0.62 spl8_6 | spl8_4 | spl8_5),
% 2.49/0.62 inference(avatar_split_clause,[],[f2460,f2470,f2466,f2474])).
% 2.49/0.62 thf(f2489,plain,(
% 2.49/0.62 spl8_7 | spl8_4 | spl8_5),
% 2.49/0.62 inference(avatar_split_clause,[],[f2462,f2470,f2466,f2479])).
% 2.49/0.62 thf(f2490,plain,(
% 2.49/0.62 spl8_8 | spl8_4 | spl8_5),
% 2.49/0.62 inference(avatar_split_clause,[],[f2464,f2470,f2466,f2484])).
% 2.49/0.62 thf(f2495,plain,(
% 2.49/0.62 ($true = $false) | ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK2))) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | (sK1 = sK2) | ~spl8_4),
% 2.49/0.62 inference(constrained_superposition,[],[f83,f2468])).
% 2.49/0.62 thf(f2496,plain,(
% 2.49/0.62 ($true = $false) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | (sK1 = sK2) | ~spl8_4),
% 2.49/0.62 inference(constrained_superposition,[],[f82,f2468])).
% 2.49/0.62 thf(f2497,plain,(
% 2.49/0.62 ($true = $false) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ sK0))) | (sK1 = sK2) | ~spl8_4),
% 2.49/0.62 inference(constrained_superposition,[],[f65,f2468])).
% 2.49/0.62 thf(f2498,plain,(
% 2.49/0.62 ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ sK0))) | (sK1 = sK2) | ~spl8_4),
% 2.49/0.62 inference(trivial_inequality_removal,[],[f2497])).
% 2.49/0.62 thf(f2499,plain,(
% 2.49/0.62 ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | (sK1 = sK2) | ~spl8_4),
% 2.49/0.62 inference(trivial_inequality_removal,[],[f2496])).
% 2.49/0.62 thf(f2500,plain,(
% 2.49/0.62 ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK2))) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | (sK1 = sK2) | ~spl8_4),
% 2.49/0.62 inference(trivial_inequality_removal,[],[f2495])).
% 2.49/0.62 thf(f2505,plain,(
% 2.49/0.62 ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ sK0))) | ~spl8_4),
% 2.49/0.62 inference(forward_subsumption_resolution,[],[f2498,f24])).
% 2.49/0.62 thf(f2506,plain,(
% 2.49/0.62 ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ~spl8_4),
% 2.49/0.62 inference(forward_subsumption_resolution,[],[f2499,f24])).
% 2.49/0.63 thf(f2507,plain,(
% 2.49/0.63 ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK2))) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ~spl8_4),
% 2.49/0.63 inference(forward_subsumption_resolution,[],[f2500,f24])).
% 2.49/0.63 thf(f2512,plain,(
% 2.49/0.63 ($true = $false) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ sK0))) | ~spl8_4),
% 2.49/0.63 inference(forward_demodulation,[],[f2505,f31])).
% 2.49/0.63 thf(f2513,plain,(
% 2.49/0.63 ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ sK0))) | ~spl8_4),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f2512])).
% 2.49/0.63 thf(f2514,plain,(
% 2.49/0.63 ($true = $false) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ~spl8_4),
% 2.49/0.63 inference(forward_demodulation,[],[f2506,f31])).
% 2.49/0.63 thf(f2515,plain,(
% 2.49/0.63 ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ~spl8_4),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f2514])).
% 2.49/0.63 thf(f2516,plain,(
% 2.49/0.63 ($true = $false) | ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK2))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ~spl8_4),
% 2.49/0.63 inference(forward_demodulation,[],[f2507,f31])).
% 2.49/0.63 thf(f2517,plain,(
% 2.49/0.63 ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK2))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ~spl8_4),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f2516])).
% 2.49/0.63 thf(f2519,definition,(
% 2.49/0.63 spl8_9 <=> ($true = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0)))),
% 2.49/0.63 introduced(definition,[new_symbols(definition,[spl8_9])],[avatar_definition])).
% 2.49/0.63 thf(f2520,plain,(
% 2.49/0.63 ($true = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ~spl8_9),
% 2.49/0.63 inference(avatar_component_clause,[],[f2519])).
% 2.49/0.63 thf(f2521,plain,(
% 2.49/0.63 ($true != ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | spl8_9),
% 2.49/0.63 inference(avatar_component_clause,[],[f2519])).
% 2.49/0.63 thf(f2523,definition,(
% 2.49/0.63 spl8_10 <=> ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK2)))),
% 2.49/0.63 introduced(definition,[new_symbols(definition,[spl8_10])],[avatar_definition])).
% 2.49/0.63 thf(f2524,plain,(
% 2.49/0.63 ($true != ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK2))) | spl8_10),
% 2.49/0.63 inference(avatar_component_clause,[],[f2523])).
% 2.49/0.63 thf(f2525,plain,(
% 2.49/0.63 ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK2))) | ~spl8_10),
% 2.49/0.63 inference(avatar_component_clause,[],[f2523])).
% 2.49/0.63 thf(f2533,plain,(
% 2.49/0.63 ($true = $false) | ($true = ((in @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ sK0))) | ~spl8_4),
% 2.49/0.63 inference(forward_demodulation,[],[f2513,f32])).
% 2.49/0.63 thf(f2534,plain,(
% 2.49/0.63 ($true = ((in @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ sK0))) | ~spl8_4),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f2533])).
% 2.49/0.63 thf(f2535,plain,(
% 2.49/0.63 ($true = $false) | ($true = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ~spl8_4),
% 2.49/0.63 inference(forward_demodulation,[],[f2515,f32])).
% 2.49/0.63 thf(f2536,plain,(
% 2.49/0.63 ($true = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ~spl8_4),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f2535])).
% 2.49/0.63 thf(f2537,plain,(
% 2.49/0.63 ($true = $false) | ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK2))) | ~spl8_4),
% 2.49/0.63 inference(forward_demodulation,[],[f2517,f32])).
% 2.49/0.63 thf(f2538,plain,(
% 2.49/0.63 ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK2))) | ~spl8_4),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f2537])).
% 2.49/0.63 thf(f2617,plain,(
% 2.49/0.63 ($true = $false) | ($false = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ~spl8_10),
% 2.49/0.63 inference(constrained_superposition,[],[f2288,f2525])).
% 2.49/0.63 thf(f2618,plain,(
% 2.49/0.63 ($false = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ~spl8_10),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f2617])).
% 2.49/0.63 thf(f2632,plain,(
% 2.49/0.63 ($true = $false) | ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($false = ((in @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ sK0))) | ~spl8_4),
% 2.49/0.63 inference(constrained_superposition,[],[f101,f2538])).
% 2.49/0.63 thf(f2640,plain,(
% 2.49/0.63 ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($false = ((in @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ sK0))) | ~spl8_4),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f2632])).
% 2.49/0.63 thf(f2648,plain,(
% 2.49/0.63 ($true = $false) | ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((in @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ sK0))) | ~spl8_4),
% 2.49/0.63 inference(forward_demodulation,[],[f2640,f2536])).
% 2.49/0.63 thf(f2649,plain,(
% 2.49/0.63 ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((in @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ sK0))) | ~spl8_4),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f2648])).
% 2.49/0.63 thf(f2658,plain,(
% 2.49/0.63 ($true = $false) | ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ~spl8_4),
% 2.49/0.63 inference(forward_demodulation,[],[f2649,f2534])).
% 2.49/0.63 thf(f2659,plain,(
% 2.49/0.63 ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ~spl8_4),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f2658])).
% 2.49/0.63 thf(f2683,definition,(
% 2.49/0.63 spl8_11 <=> ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1)))),
% 2.49/0.63 introduced(definition,[new_symbols(definition,[spl8_11])],[avatar_definition])).
% 2.49/0.63 thf(f2685,plain,(
% 2.49/0.63 ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ~spl8_11),
% 2.49/0.63 inference(avatar_component_clause,[],[f2683])).
% 2.49/0.63 thf(f2727,plain,(
% 2.49/0.63 ($true = $false) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | (sK1 = sK2) | ~spl8_4),
% 2.49/0.63 inference(constrained_superposition,[],[f84,f2659])).
% 2.49/0.63 thf(f2732,plain,(
% 2.49/0.63 ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | (sK1 = sK2) | ~spl8_4),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f2727])).
% 2.49/0.63 thf(f2737,plain,(
% 2.49/0.63 ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ~spl8_4),
% 2.49/0.63 inference(forward_subsumption_resolution,[],[f2732,f24])).
% 2.49/0.63 thf(f2739,plain,(
% 2.49/0.63 ($true = $false) | ($false = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ~spl8_4),
% 2.49/0.63 inference(forward_demodulation,[],[f2737,f31])).
% 2.49/0.63 thf(f2740,plain,(
% 2.49/0.63 ($false = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ~spl8_4),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f2739])).
% 2.49/0.63 thf(f2743,plain,(
% 2.49/0.63 ($true = $false) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ~spl8_4),
% 2.49/0.63 inference(forward_demodulation,[],[f2740,f2468])).
% 2.49/0.63 thf(f2744,plain,(
% 2.49/0.63 ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ~spl8_4),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f2743])).
% 2.49/0.63 thf(f2747,plain,(
% 2.49/0.63 ($true = $false) | ~spl8_4),
% 2.49/0.63 inference(constrained_superposition,[],[f2744,f32])).
% 2.49/0.63 thf(f2753,plain,(
% 2.49/0.63 $false | ~spl8_4),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f2747])).
% 2.49/0.63 thf(f2754,plain,(
% 2.49/0.63 ~spl8_4),
% 2.49/0.63 inference(avatar_contradiction_clause,[],[f2753])).
% 2.49/0.63 thf(f2755,plain,(
% 2.49/0.63 ($true = $false) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | (~spl8_9 | ~spl8_10)),
% 2.49/0.63 inference(forward_demodulation,[],[f2618,f2520])).
% 2.49/0.63 thf(f2756,plain,(
% 2.49/0.63 ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | (~spl8_9 | ~spl8_10)),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f2755])).
% 2.49/0.63 thf(f2816,plain,(
% 2.49/0.63 ( ! [X0 : $i] : (($true = $false) | ($true = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK2))) | ($false = ((in @ X0 @ sK0))) | ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK1))) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | (sK1 = sK2)) ) | ~spl8_5),
% 2.49/0.63 inference(constrained_superposition,[],[f150,f2472])).
% 2.49/0.63 thf(f2836,plain,(
% 2.49/0.63 ( ! [X0 : $i] : (($true = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK2))) | ($false = ((in @ X0 @ sK0))) | ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK1))) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | (sK1 = sK2)) ) | ~spl8_5),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f2816])).
% 2.49/0.63 thf(f2849,plain,(
% 2.49/0.63 ( ! [X0 : $i] : (($true = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK2))) | ($false = ((in @ X0 @ sK0))) | ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK1))) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0))))) ) | ~spl8_5),
% 2.49/0.63 inference(forward_subsumption_resolution,[],[f2836,f24])).
% 2.49/0.63 thf(f2859,plain,(
% 2.49/0.63 ( ! [X0 : $i] : (($true = $false) | ($true = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK2))) | ($false = ((in @ X0 @ sK0))) | ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK1))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0))))) ) | ~spl8_5),
% 2.49/0.63 inference(forward_demodulation,[],[f2849,f31])).
% 2.49/0.63 thf(f2860,plain,(
% 2.49/0.63 ( ! [X0 : $i] : (($true = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK2))) | ($false = ((in @ X0 @ sK0))) | ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK1))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0))))) ) | ~spl8_5),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f2859])).
% 2.49/0.63 thf(f2879,plain,(
% 2.49/0.63 ( ! [X0 : $i] : (($true = $false) | ($true = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK2))) | ($false = ((in @ X0 @ sK0))) | ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK1)))) ) | ~spl8_5),
% 2.49/0.63 inference(forward_demodulation,[],[f2860,f32])).
% 2.49/0.63 thf(f2880,plain,(
% 2.49/0.63 ( ! [X0 : $i] : (($true = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK2))) | ($false = ((in @ X0 @ sK0))) | ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ X0) @ sK1)))) ) | ~spl8_5),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f2879])).
% 2.49/0.63 thf(f3362,plain,(
% 2.49/0.63 ($true = $false) | ($false = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | (sK1 = sK2) | ~spl8_5),
% 2.49/0.63 inference(constrained_superposition,[],[f2880,f73])).
% 2.49/0.63 thf(f3423,plain,(
% 2.49/0.63 ($false = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | (sK1 = sK2) | ~spl8_5),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f3362])).
% 2.49/0.63 thf(f3428,plain,(
% 2.49/0.63 ($false = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ~spl8_5),
% 2.49/0.63 inference(forward_subsumption_resolution,[],[f3423,f24])).
% 2.49/0.63 thf(f3431,plain,(
% 2.49/0.63 ($true = $false) | ($false = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($true = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ~spl8_5),
% 2.49/0.63 inference(forward_demodulation,[],[f3428,f31])).
% 2.49/0.63 thf(f3432,plain,(
% 2.49/0.63 ($false = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($true = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ~spl8_5),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f3431])).
% 2.49/0.63 thf(f3435,plain,(
% 2.49/0.63 ($true = $false) | ($false = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ~spl8_5),
% 2.49/0.63 inference(forward_demodulation,[],[f3432,f2472])).
% 2.49/0.63 thf(f3436,plain,(
% 2.49/0.63 ($false = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ~spl8_5),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f3435])).
% 2.49/0.63 thf(f3439,plain,(
% 2.49/0.63 ($true = $false) | ($false = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ~spl8_5),
% 2.49/0.63 inference(forward_demodulation,[],[f3436,f32])).
% 2.49/0.63 thf(f3440,plain,(
% 2.49/0.63 ($false = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($false = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK1))) | ~spl8_5),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f3439])).
% 2.49/0.63 thf(f3442,definition,(
% 2.49/0.63 spl8_19 <=> ($false = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0)))),
% 2.49/0.63 introduced(definition,[new_symbols(definition,[spl8_19])],[avatar_definition])).
% 2.49/0.63 thf(f3444,plain,(
% 2.49/0.63 ($false = ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ~spl8_19),
% 2.49/0.63 inference(avatar_component_clause,[],[f3442])).
% 2.49/0.63 thf(f3446,plain,(
% 2.49/0.63 spl8_11 | spl8_19 | ~spl8_5),
% 2.49/0.63 inference(avatar_split_clause,[],[f3440,f2470,f3442,f2683])).
% 2.49/0.63 thf(f3454,plain,(
% 2.49/0.63 ($true = $false) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | (sK1 = sK2) | ~spl8_11),
% 2.49/0.63 inference(constrained_superposition,[],[f74,f2685])).
% 2.49/0.63 thf(f3455,plain,(
% 2.49/0.63 ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | (sK1 = sK2) | ~spl8_11),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f3454])).
% 2.49/0.63 thf(f3462,plain,(
% 2.49/0.63 ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ~spl8_11),
% 2.49/0.63 inference(forward_subsumption_resolution,[],[f3455,f24])).
% 2.49/0.63 thf(f3464,plain,(
% 2.49/0.63 ($true = $false) | ($true = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ~spl8_11),
% 2.49/0.63 inference(forward_demodulation,[],[f3462,f31])).
% 2.49/0.63 thf(f3465,plain,(
% 2.49/0.63 ($true = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ~spl8_11),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f3464])).
% 2.49/0.63 thf(f3468,plain,(
% 2.49/0.63 ($true = $false) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | (~spl8_5 | ~spl8_11)),
% 2.49/0.63 inference(forward_demodulation,[],[f3465,f2472])).
% 2.49/0.63 thf(f3469,plain,(
% 2.49/0.63 ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | (~spl8_5 | ~spl8_11)),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f3468])).
% 2.49/0.63 thf(f3472,plain,(
% 2.49/0.63 ($true = $false) | (~spl8_5 | ~spl8_11)),
% 2.49/0.63 inference(constrained_superposition,[],[f3469,f32])).
% 2.49/0.63 thf(f3478,plain,(
% 2.49/0.63 $false | (~spl8_5 | ~spl8_11)),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f3472])).
% 2.49/0.63 thf(f3479,plain,(
% 2.49/0.63 ~spl8_5 | ~spl8_11),
% 2.49/0.63 inference(avatar_contradiction_clause,[],[f3478])).
% 2.49/0.63 thf(f3482,plain,(
% 2.49/0.63 ($true = $false) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | (sK1 = sK2) | ~spl8_19),
% 2.49/0.63 inference(constrained_superposition,[],[f72,f3444])).
% 2.49/0.63 thf(f3501,plain,(
% 2.49/0.63 ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | (sK1 = sK2) | ~spl8_19),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f3482])).
% 2.49/0.63 thf(f3504,plain,(
% 2.49/0.63 ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ~spl8_19),
% 2.49/0.63 inference(forward_subsumption_resolution,[],[f3501,f24])).
% 2.49/0.63 thf(f3506,plain,(
% 2.49/0.63 ($true = $false) | ($true = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ~spl8_19),
% 2.49/0.63 inference(forward_demodulation,[],[f3504,f31])).
% 2.49/0.63 thf(f3507,plain,(
% 2.49/0.63 ($true = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | ~spl8_19),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f3506])).
% 2.49/0.63 thf(f3510,plain,(
% 2.49/0.63 ($true = $false) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | (~spl8_5 | ~spl8_19)),
% 2.49/0.63 inference(forward_demodulation,[],[f3507,f2472])).
% 2.49/0.63 thf(f3511,plain,(
% 2.49/0.63 ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | (~spl8_5 | ~spl8_19)),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f3510])).
% 2.49/0.63 thf(f3514,plain,(
% 2.49/0.63 ($true = $false) | (~spl8_5 | ~spl8_19)),
% 2.49/0.63 inference(constrained_superposition,[],[f3511,f32])).
% 2.49/0.63 thf(f3520,plain,(
% 2.49/0.63 $false | (~spl8_5 | ~spl8_19)),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f3514])).
% 2.49/0.63 thf(f3521,plain,(
% 2.49/0.63 ~spl8_5 | ~spl8_19),
% 2.49/0.63 inference(avatar_contradiction_clause,[],[f3520])).
% 2.49/0.63 thf(f3596,plain,(
% 2.49/0.63 ($true != $true) | ($false = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | spl8_9),
% 2.49/0.63 inference(constrained_superposition,[],[f2521,f26])).
% 2.49/0.63 thf(f3597,plain,(
% 2.49/0.63 ($false = ((in @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | spl8_9),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f3596])).
% 2.49/0.63 thf(f3603,plain,(
% 2.49/0.63 $false | (spl8_5 | spl8_9)),
% 2.49/0.63 inference(forward_subsumption_resolution,[],[f3597,f2471])).
% 2.49/0.63 thf(f3604,plain,(
% 2.49/0.63 spl8_5 | spl8_9),
% 2.49/0.63 inference(avatar_contradiction_clause,[],[f3603])).
% 2.49/0.63 thf(f3734,plain,(
% 2.49/0.63 ($true != $true) | ($true = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK2))) | ($true != ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($true != ((in @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ sK0))) | ~spl8_8),
% 2.49/0.63 inference(constrained_superposition,[],[f22,f2486])).
% 2.49/0.63 thf(f3735,plain,(
% 2.49/0.63 ($true = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK2))) | ($true != ((in @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1) @ sK0))) | ($true != ((in @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ sK0))) | ~spl8_8),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f3734])).
% 2.49/0.63 thf(f3736,plain,(
% 2.49/0.63 ($true = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK2))) | ($true != ((in @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ sK0))) | (~spl8_7 | ~spl8_8)),
% 2.49/0.63 inference(forward_subsumption_resolution,[],[f3735,f2481])).
% 2.49/0.63 thf(f3737,plain,(
% 2.49/0.63 ($true = ((in @ (kpair @ (sK4 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK7 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK2))) | (~spl8_6 | ~spl8_7 | ~spl8_8)),
% 2.49/0.63 inference(forward_subsumption_resolution,[],[f3736,f2476])).
% 2.49/0.63 thf(f3922,plain,(
% 2.49/0.63 ($true = $false) | ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK2))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | (sK1 = sK2) | (~spl8_6 | ~spl8_7 | ~spl8_8)),
% 2.49/0.63 inference(constrained_superposition,[],[f79,f3737])).
% 2.49/0.63 thf(f3929,plain,(
% 2.49/0.63 ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($true = ((in @ (kpair @ (sK3 @ sK0 @ sK2 @ sK1 @ sK0) @ (sK6 @ sK2 @ sK0 @ sK0 @ sK1)) @ sK2))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | (sK1 = sK2) | (~spl8_6 | ~spl8_7 | ~spl8_8)),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f3922])).
% 2.49/0.63 thf(f3941,plain,(
% 2.49/0.63 ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | (sK1 = sK2) | (~spl8_6 | ~spl8_7 | ~spl8_8 | spl8_10)),
% 2.49/0.63 inference(forward_subsumption_resolution,[],[f3929,f2524])).
% 2.49/0.63 thf(f3943,plain,(
% 2.49/0.63 ($false = ((subset @ sK1 @ (cartprod @ sK0 @ sK0)))) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | (~spl8_6 | ~spl8_7 | ~spl8_8 | spl8_10)),
% 2.49/0.63 inference(forward_subsumption_resolution,[],[f3941,f24])).
% 2.49/0.63 thf(f3945,plain,(
% 2.49/0.63 ($true = $false) | ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | (~spl8_6 | ~spl8_7 | ~spl8_8 | spl8_10)),
% 2.49/0.63 inference(forward_demodulation,[],[f3943,f31])).
% 2.49/0.63 thf(f3946,plain,(
% 2.49/0.63 ($false = ((subset @ sK2 @ (cartprod @ sK0 @ sK0)))) | (~spl8_6 | ~spl8_7 | ~spl8_8 | spl8_10)),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f3945])).
% 2.49/0.63 thf(f3949,plain,(
% 2.49/0.63 ($true = $false) | (~spl8_6 | ~spl8_7 | ~spl8_8 | spl8_10)),
% 2.49/0.63 inference(constrained_superposition,[],[f3946,f32])).
% 2.49/0.63 thf(f3955,plain,(
% 2.49/0.63 $false | (~spl8_6 | ~spl8_7 | ~spl8_8 | spl8_10)),
% 2.49/0.63 inference(trivial_inequality_removal,[],[f3949])).
% 2.49/0.63 thf(f3956,plain,(
% 2.49/0.63 ~spl8_6 | ~spl8_7 | ~spl8_8 | spl8_10),
% 2.49/0.63 inference(avatar_contradiction_clause,[],[f3955])).
% 2.49/0.63 thf(f3965,plain,(
% 2.49/0.63 $false | (spl8_4 | ~spl8_9 | ~spl8_10)),
% 2.49/0.63 inference(forward_subsumption_resolution,[],[f2756,f2467])).
% 2.49/0.63 thf(f3966,plain,(
% 2.49/0.63 spl8_4 | ~spl8_9 | ~spl8_10),
% 2.49/0.63 inference(avatar_contradiction_clause,[],[f3965])).
% 2.49/0.63 cnf(s8, plain, spl8_4 | spl8_5 | spl8_6, inference(sat_conversion,[],[f2488])).
% 2.49/0.63 cnf(s9, plain, spl8_4 | spl8_5 | spl8_7, inference(sat_conversion,[],[f2489])).
% 2.49/0.63 cnf(s10, plain, spl8_4 | spl8_5 | spl8_8, inference(sat_conversion,[],[f2490])).
% 2.49/0.63 cnf(s17, plain, ~spl8_4, inference(sat_conversion,[],[f2754])).
% 2.49/0.63 cnf(s28, plain, ~spl8_5 | spl8_11 | spl8_19, inference(sat_conversion,[],[f3446])).
% 2.49/0.63 cnf(s30, plain, ~spl8_5 | ~spl8_11, inference(sat_conversion,[],[f3479])).
% 2.49/0.63 cnf(s32, plain, ~spl8_5 | ~spl8_19, inference(sat_conversion,[],[f3521])).
% 2.49/0.63 cnf(s36, plain, spl8_5 | spl8_9, inference(sat_conversion,[],[f3604])).
% 2.49/0.63 cnf(s40, plain, ~spl8_6 | ~spl8_7 | ~spl8_8 | spl8_10, inference(sat_conversion,[],[f3956])).
% 2.49/0.63 cnf(s45, plain, spl8_4 | ~spl8_9 | ~spl8_10, inference(sat_conversion,[],[f3966])).
% 2.49/0.63 cnf(s46, plain, spl8_5 | spl8_8, inference(rat,[],[s10,s17])).
% 2.49/0.63 cnf(s47, plain, spl8_5 | spl8_7, inference(rat,[],[s9,s17])).
% 2.49/0.63 cnf(s48, plain, spl8_5 | spl8_6, inference(rat,[],[s8,s17])).
% 2.49/0.63 cnf(s52, plain, spl8_5, inference(rat,[],[s40,s45,s48,s47,s46,s36,s17])).
% 2.49/0.63 cnf(s53, plain, ~spl8_19, inference(rat,[],[s32,s52])).
% 2.49/0.63 cnf(s54, plain, ~spl8_11, inference(rat,[],[s30,s52])).
% 2.49/0.63 cnf(s55, plain, $false, inference(rat,[],[s28,s53,s54,s52])).
% 2.49/0.63 thf(f3977,plain,(
% 2.49/0.63 $false),
% 2.49/0.63 inference(avatar_sat_refutation,[],[s55])).
% 2.49/0.63 % SZS output end Proof for theBenchmark
% 2.49/0.63 % (2740823)------------------------------
% 2.49/0.63 % (2740823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.49/0.63 % (2740823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.49/0.63 % (2740823)CaDiCaL version: 2.1.3
% 2.49/0.63 % (2740823)Termination reason: Refutation
% 2.49/0.63 % (2740823)Time elapsed: 0.304 s
% 2.49/0.63 % (2740823)Peak memory usage: 14 MB
% 2.49/0.63 % (2740823)Instructions burned: 691 (million)
% 2.49/0.63 % (2740800)Success in time 0.416 s
% 2.49/0.63 % Vampire exiting
%------------------------------------------------------------------------------