%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SYO873^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:43:28 AM UTC 2026
% Result : Theorem 141.62s 49.47s
% Output : CNFRefutation 141.62s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SYO873^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.07 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.28 % Computer : n010.cluster.edu
% 0.11/0.28 % Model : x86_64 x86_64
% 0.11/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.28 % Memory : 8046.5625MB
% 0.11/0.28 % OS : Linux 6.8.0-71-generic
% 0.11/0.28 % CPULimit : 300
% 0.11/0.28 % WCLimit : 300
% 0.11/0.28 % DateTime : Tue Sep 29 17:23:03 UTC 2026
% 0.11/0.28 % CPUTime :
% 0.11/0.28 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.27/0.35 Running higher-order theorem proving
% 0.27/0.40 Running: /export/starexec/sandbox2/solver/bin/eprover-ho --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox2/tmp/tmp.cXgadyaeX3/E---3.1_3167196.p
% 141.62/49.47 % Version: 3.5.1-ho
% 141.62/49.47 % partial match(1): HSLMSMSSSSLCHSA
% 141.62/49.47 % Preprocessing class: HSLMSLSSSSLCHSA.
% 141.62/49.47 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 141.62/49.47 % Starting pre_casc_6 with 1500s (5) cores
% 141.62/49.47 % Starting ehoh_best7 with 300s (1) cores
% 141.62/49.47 % Starting new_bool_8 with 300s (1) cores
% 141.62/49.47 % Starting new_ho_11 with 300s (1) cores
% 141.62/49.47 % new_ho_11 with pid 3167212 completed with status 0
% 141.62/49.47 % Result found by new_ho_11
% 141.62/49.47 % partial match(1): HSLMSMSSSSLCHSA
% 141.62/49.47 % Preprocessing class: HSLMSLSSSSLCHSA.
% 141.62/49.47 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 141.62/49.47 % Starting pre_casc_6 with 1500s (5) cores
% 141.62/49.47 % Starting ehoh_best7 with 300s (1) cores
% 141.62/49.47 % Starting new_bool_8 with 300s (1) cores
% 141.62/49.47 % Starting new_ho_11 with 300s (1) cores
% 141.62/49.47 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 141.62/49.47 % No SInE strategy applied
% 141.62/49.47 % Search class: HGHSM-SMLM33-DHSFFSBC
% 141.62/49.47 % partial match(1): HGHSM-SMLM32-DHSFFSBC
% 141.62/49.47 % Scheduled 7 strats onto 1 cores with 282 seconds (282 total)
% 141.62/49.47 % Starting SubtermCWHack with 26s (1) cores
% 141.62/49.47 % SubtermCWHack with pid 3167617 completed with status 8
% 141.62/49.47 % Starting new_ho_11 with 29s (1) cores
% 141.62/49.47 % new_ho_11 with pid 3167631 completed with status 0
% 141.62/49.47 % Result found by new_ho_11
% 141.62/49.47 % partial match(1): HSLMSMSSSSLCHSA
% 141.62/49.47 % Preprocessing class: HSLMSLSSSSLCHSA.
% 141.62/49.47 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 141.62/49.47 % Starting pre_casc_6 with 1500s (5) cores
% 141.62/49.47 % Starting ehoh_best7 with 300s (1) cores
% 141.62/49.47 % Starting new_bool_8 with 300s (1) cores
% 141.62/49.47 % Starting new_ho_11 with 300s (1) cores
% 141.62/49.47 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 141.62/49.47 % No SInE strategy applied
% 141.62/49.47 % Search class: HGHSM-SMLM33-DHSFFSBC
% 141.62/49.47 % partial match(1): HGHSM-SMLM32-DHSFFSBC
% 141.62/49.47 % Scheduled 7 strats onto 1 cores with 282 seconds (282 total)
% 141.62/49.47 % Starting SubtermCWHack with 26s (1) cores
% 141.62/49.47 % SubtermCWHack with pid 3167617 completed with status 8
% 141.62/49.47 % Starting new_ho_11 with 29s (1) cores
% 141.62/49.47 % Preprocessing time : 0.148 s
% 141.62/49.47 % Presaturation interreduction done
% 141.62/49.47
% 141.62/49.47 % Proof found!
% 141.62/49.47 % SZS status Theorem
% 141.62/49.47 % SZS output start CNFRefutation
% 141.62/49.47 thf(decl_24, type, c_False: $o).
% 141.62/49.47 thf(decl_26, type, c_not: $o > $o).
% 141.62/49.47 thf(decl_27, type, c_and: $o > $o > $o).
% 141.62/49.47 thf(decl_30, type, c_In: $i > $i > $o).
% 141.62/49.47 thf(decl_31, type, c_Subq: $i > $i > $o).
% 141.62/49.47 thf(decl_32, type, c_Empty: $i).
% 141.62/49.47 thf(decl_34, type, c_Power: $i > $i).
% 141.62/49.47 thf(decl_36, type, c_TransSet: $i > $o).
% 141.62/49.47 thf(decl_42, type, c_exactly2: $i > $o).
% 141.62/49.47 thf(decl_72, type, c_binintersect: $i > $i > $i).
% 141.62/49.47 thf(decl_80, type, c_ordsucc: $i > $i).
% 141.62/49.47 thf(decl_87, type, c_Inj1: $i > $i).
% 141.62/49.47 thf(decl_94, type, c_binrep: $i > $i > $i).
% 141.62/49.47 thf(decl_96, type, c_setprod: $i > $i > $i).
% 141.62/49.47 thf(decl_114, type, c_SNo: $i > $o).
% 141.62/49.47 thf(decl_269, type, epred143_2: ($i > $i) > $i > $o).
% 141.62/49.47 thf(decl_272, type, epred146_3: $i > ($i > $i) > ($i > $o) > $o).
% 141.62/49.47 thf(decl_273, type, epred147_3: $i > ($i > $i) > ($i > $o) > $o).
% 141.62/49.47 thf(decl_275, type, epred149_0: $o).
% 141.62/49.47 thf(decl_276, type, epred150_2: ($i > $i) > ($i > $o) > $o).
% 141.62/49.47 thf(decl_277, type, epred151_2: ($i > $i) > ($i > $o) > $o).
% 141.62/49.47 thf(decl_278, type, esk1_0: $i).
% 141.62/49.47 thf(decl_291, type, epred153_2: $o > $o > $o).
% 141.62/49.47 thf(decl_336, type, epred159_0: $i > $o).
% 141.62/49.47 thf(decl_337, type, esk52_0: $i > $i).
% 141.62/49.47 thf(decl_506, type, esk219_2: ($i > $o) > ($i > $i) > $i).
% 141.62/49.47 thf(decl_507, type, esk220_2: ($i > $o) > ($i > $i) > $i).
% 141.62/49.47 thf(decl_508, type, esk221_2: ($i > $o) > ($i > $i) > $i).
% 141.62/49.47 thf(decl_509, type, esk222_2: ($i > $o) > ($i > $i) > $i).
% 141.62/49.47 thf(decl_524, type, epred167_0: $i > $o).
% 141.62/49.47 thf(decl_537, type, esk239_1: $i > $i).
% 141.62/49.47 thf(conj, conjecture, (c_not @ (![X1:$i > $o, X201:$i > $i]:((c_and @ ((((((X1 @ (X201 @ (c_binintersect @ (X201 @ (c_Power @ c_Empty)) @ (X201 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ c_Empty))) @ c_Empty))))))=>((((c_TransSet @ (X201 @ c_Empty)))=>(![X9:$i]:((((c_In @ X9 @ c_Empty))=>(?[X13:$i]:((c_and @ ((c_Subq @ X13 @ X9)) @ ((c_exactly2 @ (c_ordsucc @ (X201 @ X13))))))))))))))=>(?[X9:$i]:((c_and @ (?[X13:$i]:((c_and @ ((c_Subq @ X13 @ X9)) @ (((((X9)=(X201 @ X9)))=>(?[X66:$i]:((c_and @ ((c_Subq @ X66 @ X9)) @ ((c_not @ ((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))))))))))))) @ ((c_not @ ((c_SNo @ X9))))))))) @ ((c_not @ ((X1 @ (X201 @ (X201 @ (X201 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))))))))), file('/export/starexec/sandbox2/tmp/tmp.cXgadyaeX3/E---3.1_3167196.p', conj)).
% 141.62/49.47 thf(ax13, axiom, ((c_not)=(^[X17:$o]:((((X17))=>((c_False)))))), file('/export/starexec/sandbox2/tmp/tmp.cXgadyaeX3/E---3.1_3167196.p', ax13)).
% 141.62/49.47 thf(ax5, axiom, (c_not @ (?[X7:$i]:((c_In @ X7 @ c_Empty)))), file('/export/starexec/sandbox2/tmp/tmp.cXgadyaeX3/E---3.1_3167196.p', ax5)).
% 141.62/49.47 thf(ax14, axiom, ((c_and)=(^[X18:$o, X19:$o]:(![X20:$o]:((((((X18))=>((((X19))=>((X20))))))=>((X20))))))), file('/export/starexec/sandbox2/tmp/tmp.cXgadyaeX3/E---3.1_3167196.p', ax14)).
% 141.62/49.47 thf(c_0_4, negated_conjecture, ~((c_not @ (![X1:$i > $o, X201:$i > $i]:((c_and @ ((((((X1 @ (X201 @ (c_binintersect @ (X201 @ (c_Power @ c_Empty)) @ (X201 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ c_Empty))) @ c_Empty))))))=>((((c_TransSet @ (X201 @ c_Empty)))=>(![X9:$i]:((((c_In @ X9 @ c_Empty))=>(?[X13:$i]:((c_and @ ((c_Subq @ X13 @ X9)) @ ((c_exactly2 @ (c_ordsucc @ (X201 @ X13))))))))))))))=>(?[X9:$i]:((c_and @ (?[X13:$i]:((c_and @ ((c_Subq @ X13 @ X9)) @ (((((X9)=(X201 @ X9)))=>(?[X66:$i]:((c_and @ ((c_Subq @ X66 @ X9)) @ ((c_not @ ((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))))))))))))) @ ((c_not @ ((c_SNo @ X9))))))))) @ ((c_not @ ((X1 @ (X201 @ (X201 @ (X201 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty))))))))))))), inference(assume_negation,[status(cth)],[conj])).
% 141.62/49.47 thf(c_0_5, plain, ((epred149_0)<=>(~(![X1:$i > $o, X201:$i > $i]:(((~((((X1 @ (X201 @ (c_binintersect @ (X201 @ (c_Power @ c_Empty)) @ (X201 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ c_Empty))) @ c_Empty)))))=>((c_TransSet @ (X201 @ c_Empty))=>![X9:$i]:(((c_In @ X9 @ c_Empty)=>?[X13:$i]:(((~(c_Subq @ X13 @ X9)|((~(c_exactly2 @ (c_ordsucc @ (X201 @ X13)))|(c_and @ $true @ $true))&((c_exactly2 @ (c_ordsucc @ (X201 @ X13)))|(c_and @ $true @ $false))))&((c_Subq @ X13 @ X9)|((~(c_exactly2 @ (c_ordsucc @ (X201 @ X13)))|(c_and @ $false @ $true))&((c_exactly2 @ (c_ordsucc @ (X201 @ X13)))|(c_and @ $false @ $false))))))))))=>?[X9:$i]:(((~(?[X13:$i]:(((~(c_Subq @ X13 @ X9)|((~((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false))))))))|(c_and @ $true @ $true))&((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false)))))))|(c_and @ $true @ $false))))&((c_Subq @ X13 @ X9)|((~((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false))))))))|(c_and @ $false @ $true))&((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false)))))))|(c_and @ $false @ $false)))))))|((((~(c_SNo @ X9)|~(c_not @ $true))&((c_SNo @ X9)|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(c_SNo @ X9)|(c_not @ $true))&((c_SNo @ X9)|(c_not @ $false)))|(c_and @ $true @ $false))))&(?[X13:$i]:(((~(c_Subq @ X13 @ X9)|((~((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false))))))))|(c_and @ $true @ $true))&((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false)))))))|(c_and @ $true @ $false))))&((c_Subq @ X13 @ X9)|((~((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false))))))))|(c_and @ $false @ $true))&((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false)))))))|(c_and @ $false @ $false))))))|((((~(c_SNo @ X9)|~(c_not @ $true))&((c_SNo @ X9)|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(c_SNo @ X9)|(c_not @ $true))&((c_SNo @ X9)|(c_not @ $false)))|(c_and @ $false @ $false))))))))|((((~(X1 @ (X201 @ (X201 @ (X201 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $true))&((X1 @ (X201 @ (X201 @ (X201 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (X201 @ (X201 @ (X201 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $true))&((X1 @ (X201 @ (X201 @ (X201 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((((X1 @ (X201 @ (c_binintersect @ (X201 @ (c_Power @ c_Empty)) @ (X201 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ c_Empty))) @ c_Empty)))))=>((c_TransSet @ (X201 @ c_Empty))=>![X9:$i]:(((c_In @ X9 @ c_Empty)=>?[X13:$i]:(((~(c_Subq @ X13 @ X9)|((~(c_exactly2 @ (c_ordsucc @ (X201 @ X13)))|(c_and @ $true @ $true))&((c_exactly2 @ (c_ordsucc @ (X201 @ X13)))|(c_and @ $true @ $false))))&((c_Subq @ X13 @ X9)|((~(c_exactly2 @ (c_ordsucc @ (X201 @ X13)))|(c_and @ $false @ $true))&((c_exactly2 @ (c_ordsucc @ (X201 @ X13)))|(c_and @ $false @ $false))))))))))=>?[X9:$i]:(((~(?[X13:$i]:(((~(c_Subq @ X13 @ X9)|((~((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false))))))))|(c_and @ $true @ $true))&((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false)))))))|(c_and @ $true @ $false))))&((c_Subq @ X13 @ X9)|((~((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false))))))))|(c_and @ $false @ $true))&((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false)))))))|(c_and @ $false @ $false)))))))|((((~(c_SNo @ X9)|~(c_not @ $true))&((c_SNo @ X9)|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(c_SNo @ X9)|(c_not @ $true))&((c_SNo @ X9)|(c_not @ $false)))|(c_and @ $true @ $false))))&(?[X13:$i]:(((~(c_Subq @ X13 @ X9)|((~((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false))))))))|(c_and @ $true @ $true))&((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false)))))))|(c_and @ $true @ $false))))&((c_Subq @ X13 @ X9)|((~((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false))))))))|(c_and @ $false @ $true))&((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false)))))))|(c_and @ $false @ $false))))))|((((~(c_SNo @ X9)|~(c_not @ $true))&((c_SNo @ X9)|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(c_SNo @ X9)|(c_not @ $true))&((c_SNo @ X9)|(c_not @ $false)))|(c_and @ $false @ $false)))))))|((((~(X1 @ (X201 @ (X201 @ (X201 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $true))&((X1 @ (X201 @ (X201 @ (X201 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (X201 @ (X201 @ (X201 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $true))&((X1 @ (X201 @ (X201 @ (X201 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false)))))))|(c_not @ $true))), introduced(definition)).
% 141.62/49.47 thf(c_0_6, plain, ![X1:$i > $o, X201:$i > $i]:(((epred150_2 @ X201 @ X1)<=>(~((((X1 @ (X201 @ (c_binintersect @ (X201 @ (c_Power @ c_Empty)) @ (X201 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ c_Empty))) @ c_Empty)))))=>((c_TransSet @ (X201 @ c_Empty))=>![X9:$i]:(((c_In @ X9 @ c_Empty)=>?[X13:$i]:(((~(c_Subq @ X13 @ X9)|((~(c_exactly2 @ (c_ordsucc @ (X201 @ X13)))|(c_and @ $true @ $true))&((c_exactly2 @ (c_ordsucc @ (X201 @ X13)))|(c_and @ $true @ $false))))&((c_Subq @ X13 @ X9)|((~(c_exactly2 @ (c_ordsucc @ (X201 @ X13)))|(c_and @ $false @ $true))&((c_exactly2 @ (c_ordsucc @ (X201 @ X13)))|(c_and @ $false @ $false))))))))))=>?[X9:$i]:(((~(?[X13:$i]:(((~(c_Subq @ X13 @ X9)|((~((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false))))))))|(c_and @ $true @ $true))&((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false)))))))|(c_and @ $true @ $false))))&((c_Subq @ X13 @ X9)|((~((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false))))))))|(c_and @ $false @ $true))&((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false)))))))|(c_and @ $false @ $false)))))))|((((~(c_SNo @ X9)|~(c_not @ $true))&((c_SNo @ X9)|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(c_SNo @ X9)|(c_not @ $true))&((c_SNo @ X9)|(c_not @ $false)))|(c_and @ $true @ $false))))&(?[X13:$i]:(((~(c_Subq @ X13 @ X9)|((~((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false))))))))|(c_and @ $true @ $true))&((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false)))))))|(c_and @ $true @ $false))))&((c_Subq @ X13 @ X9)|((~((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false))))))))|(c_and @ $false @ $true))&((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false)))))))|(c_and @ $false @ $false))))))|((((~(c_SNo @ X9)|~(c_not @ $true))&((c_SNo @ X9)|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(c_SNo @ X9)|(c_not @ $true))&((c_SNo @ X9)|(c_not @ $false)))|(c_and @ $false @ $false))))))))|((((~(X1 @ (X201 @ (X201 @ (X201 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $true))&((X1 @ (X201 @ (X201 @ (X201 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (X201 @ (X201 @ (X201 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $true))&((X1 @ (X201 @ (X201 @ (X201 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false)))))), introduced(definition)).
% 141.62/49.47 thf(c_0_7, plain, ![X1:$i > $o, X201:$i > $i]:(((epred151_2 @ X201 @ X1)<=>((((X1 @ (X201 @ (c_binintersect @ (X201 @ (c_Power @ c_Empty)) @ (X201 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ c_Empty))) @ c_Empty)))))=>((c_TransSet @ (X201 @ c_Empty))=>![X9:$i]:(((c_In @ X9 @ c_Empty)=>?[X13:$i]:(((~(c_Subq @ X13 @ X9)|((~(c_exactly2 @ (c_ordsucc @ (X201 @ X13)))|(c_and @ $true @ $true))&((c_exactly2 @ (c_ordsucc @ (X201 @ X13)))|(c_and @ $true @ $false))))&((c_Subq @ X13 @ X9)|((~(c_exactly2 @ (c_ordsucc @ (X201 @ X13)))|(c_and @ $false @ $true))&((c_exactly2 @ (c_ordsucc @ (X201 @ X13)))|(c_and @ $false @ $false))))))))))=>?[X9:$i]:(((~(?[X13:$i]:(((~(c_Subq @ X13 @ X9)|((~((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false))))))))|(c_and @ $true @ $true))&((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false)))))))|(c_and @ $true @ $false))))&((c_Subq @ X13 @ X9)|((~((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false))))))))|(c_and @ $false @ $true))&((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false)))))))|(c_and @ $false @ $false)))))))|((((~(c_SNo @ X9)|~(c_not @ $true))&((c_SNo @ X9)|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(c_SNo @ X9)|(c_not @ $true))&((c_SNo @ X9)|(c_not @ $false)))|(c_and @ $true @ $false))))&(?[X13:$i]:(((~(c_Subq @ X13 @ X9)|((~((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false))))))))|(c_and @ $true @ $true))&((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false)))))))|(c_and @ $true @ $false))))&((c_Subq @ X13 @ X9)|((~((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false))))))))|(c_and @ $false @ $true))&((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false)))))))|(c_and @ $false @ $false))))))|((((~(c_SNo @ X9)|~(c_not @ $true))&((c_SNo @ X9)|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(c_SNo @ X9)|(c_not @ $true))&((c_SNo @ X9)|(c_not @ $false)))|(c_and @ $false @ $false)))))))|((((~(X1 @ (X201 @ (X201 @ (X201 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $true))&((X1 @ (X201 @ (X201 @ (X201 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (X201 @ (X201 @ (X201 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $true))&((X1 @ (X201 @ (X201 @ (X201 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false)))))), introduced(definition)).
% 141.62/49.47 thf(c_0_8, negated_conjecture, ~(((epred149_0)&(![X1:$i > $o, X201:$i > $i]:(((epred150_2 @ X201 @ X1)&(epred151_2 @ X201 @ X1)))|(c_not @ $false)))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fool_unroll,[status(thm)],[c_0_4]), c_0_5]), c_0_6]), c_0_7])).
% 141.62/49.47 thf(c_0_9, plain, ![X231:$o]:(((c_not @ ((X231)))<=>((X231)=>(c_False)))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[ax13])])).
% 141.62/49.47 thf(c_0_10, plain, ((~(![X1:$i > $o, X201:$i > $i]:(((epred150_2 @ X201 @ X1)&(epred151_2 @ X201 @ X1))))|(c_not @ $true))=>(epred149_0)), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_5]), c_0_6]), c_0_7])).
% 141.62/49.47 thf(c_0_11, negated_conjecture, ((~(epred150_2 @ esk52_0 @ epred159_0)|~(epred151_2 @ esk52_0 @ epred159_0)|~(epred149_0))&(~(c_not @ $false)|~(epred149_0))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_8])])])])])).
% 141.62/49.47 thf(c_0_12, plain, ![X479:$o]:(((~(c_not @ ((X479)))|(~(X479)|(c_False)))&(((X479)|(c_not @ ((X479))))&(~(c_False)|(c_not @ ((X479))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_9])])])])).
% 141.62/49.47 thf(c_0_13, plain, ![X9:$i, X201:$i > $i]:(((epred143_2 @ X201 @ X9)<=>?[X13:$i]:(((~(c_Subq @ X13 @ X9)|((~(c_exactly2 @ (c_ordsucc @ (X201 @ X13)))|(c_and @ $true @ $true))&((c_exactly2 @ (c_ordsucc @ (X201 @ X13)))|(c_and @ $true @ $false))))&((c_Subq @ X13 @ X9)|((~(c_exactly2 @ (c_ordsucc @ (X201 @ X13)))|(c_and @ $false @ $true))&((c_exactly2 @ (c_ordsucc @ (X201 @ X13)))|(c_and @ $false @ $false)))))))), introduced(definition)).
% 141.62/49.47 thf(c_0_14, plain, ![X1:$i > $o, X201:$i > $i, X9:$i]:(((epred146_3 @ X9 @ X201 @ X1)<=>(~(?[X13:$i]:(((~(c_Subq @ X13 @ X9)|((~((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false))))))))|(c_and @ $true @ $true))&((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false)))))))|(c_and @ $true @ $false))))&((c_Subq @ X13 @ X9)|((~((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false))))))))|(c_and @ $false @ $true))&((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false)))))))|(c_and @ $false @ $false)))))))|((((~(c_SNo @ X9)|~(c_not @ $true))&((c_SNo @ X9)|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(c_SNo @ X9)|(c_not @ $true))&((c_SNo @ X9)|(c_not @ $false)))|(c_and @ $true @ $false)))))), introduced(definition)).
% 141.62/49.47 thf(c_0_15, plain, ![X1:$i > $o, X201:$i > $i, X9:$i]:(((epred147_3 @ X9 @ X201 @ X1)<=>(?[X13:$i]:(((~(c_Subq @ X13 @ X9)|((~((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false))))))))|(c_and @ $true @ $true))&((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false)))))))|(c_and @ $true @ $false))))&((c_Subq @ X13 @ X9)|((~((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false))))))))|(c_and @ $false @ $true))&((((X9)=(X201 @ X9))=>?[X66:$i]:(((~(c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false))))&((c_Subq @ X66 @ X9)|((((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $true))&((X1 @ (c_setprod @ X13 @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ (c_Power @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false)))))))|(c_and @ $false @ $false))))))|((((~(c_SNo @ X9)|~(c_not @ $true))&((c_SNo @ X9)|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(c_SNo @ X9)|(c_not @ $true))&((c_SNo @ X9)|(c_not @ $false)))|(c_and @ $false @ $false)))))), introduced(definition)).
% 141.62/49.47 thf(c_0_16, axiom, ((~(?[X7:$i]:((c_In @ X7 @ c_Empty)))|(c_not @ $true))&(?[X7:$i]:((c_In @ X7 @ c_Empty))|(c_not @ $false))), inference(fool_unroll,[status(thm)],[ax5])).
% 141.62/49.47 thf(c_0_17, plain, ![X1932:$i > $o, X1933:$i > $i]:(((((epred150_2 @ X1933 @ X1932)|(epred149_0))&((epred151_2 @ X1933 @ X1932)|(epred149_0)))&(~(c_not @ $true)|(epred149_0)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_10])])])])])).
% 141.62/49.47 thf(c_0_18, negated_conjecture, (~((c_not @ (~($true))))|~((epred149_0))), inference(split_conjunct,[status(thm)],[c_0_11])).
% 141.62/49.47 thf(c_0_19, plain, (c_not @ (~($true))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_12])])])).
% 141.62/49.47 thf(c_0_20, plain, ![X1:$i > $o, X201:$i > $i]:(((epred150_2 @ X201 @ X1)<=>(~((((X1 @ (X201 @ (c_binintersect @ (X201 @ (c_Power @ c_Empty)) @ (X201 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ c_Empty))) @ c_Empty)))))=>((c_TransSet @ (X201 @ c_Empty))=>![X9:$i]:(((c_In @ X9 @ c_Empty)=>(epred143_2 @ X201 @ X9)))))=>?[X9:$i]:(((epred146_3 @ X9 @ X201 @ X1)&(epred147_3 @ X9 @ X201 @ X1)))))|((((~(X1 @ (X201 @ (X201 @ (X201 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $true))&((X1 @ (X201 @ (X201 @ (X201 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $true @ $true))&(((~(X1 @ (X201 @ (X201 @ (X201 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $true))&((X1 @ (X201 @ (X201 @ (X201 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $false)))|(c_and @ $true @ $false)))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_6, c_0_13]), c_0_14]), c_0_15])).
% 141.62/49.47 thf(c_0_21, plain, ![X232:$o, X233:$o]:(((c_and @ ((X232)) @ ((X233)))<=>![X20:$o]:((((X232)=>((X233)=>(X20)))=>(X20))))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[ax14])])).
% 141.62/49.47 thf(c_0_22, plain, ![X1:$i > $o, X201:$i > $i]:(((epred151_2 @ X201 @ X1)<=>((((X1 @ (X201 @ (c_binintersect @ (X201 @ (c_Power @ c_Empty)) @ (X201 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ c_Empty))) @ c_Empty)))))=>((c_TransSet @ (X201 @ c_Empty))=>![X9:$i]:(((c_In @ X9 @ c_Empty)=>(epred143_2 @ X201 @ X9)))))=>?[X9:$i]:(((epred146_3 @ X9 @ X201 @ X1)&(epred147_3 @ X9 @ X201 @ X1))))|((((~(X1 @ (X201 @ (X201 @ (X201 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $true))&((X1 @ (X201 @ (X201 @ (X201 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $false)))|(c_and @ $false @ $true))&(((~(X1 @ (X201 @ (X201 @ (X201 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $true))&((X1 @ (X201 @ (X201 @ (X201 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $false)))|(c_and @ $false @ $false)))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_7, c_0_13]), c_0_14]), c_0_15])).
% 141.62/49.47 thf(c_0_23, plain, ![X446:$i]:(((~(c_In @ X446 @ c_Empty)|(c_not @ $true))&((c_In @ esk1_0 @ c_Empty)|(c_not @ $false)))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_16])])])])])).
% 141.62/49.47 thf(c_0_24, plain, ((epred149_0)|~((c_not @ (($true))))), inference(split_conjunct,[status(thm)],[c_0_17])).
% 141.62/49.47 thf(c_0_25, negated_conjecture, ~((epred149_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_18, c_0_19])])).
% 141.62/49.47 thf(c_0_26, plain, ![X1934:$i > $o, X1935:$i > $i, X1936:$i, X1937:$i, X1938:$i > $o, X1939:$i > $i]:((((((~(X1934 @ (X1935 @ (X1935 @ (X1935 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $true)|(c_and @ $true @ $true)|(~(X1934 @ (X1935 @ (c_binintersect @ (X1935 @ (c_Power @ c_Empty)) @ (X1935 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ c_Empty))) @ c_Empty)))))|(~(c_TransSet @ (X1935 @ c_Empty))|(~(c_In @ X1936 @ c_Empty)|(epred143_2 @ X1935 @ X1936))))|~(epred150_2 @ X1935 @ X1934))&((X1934 @ (X1935 @ (X1935 @ (X1935 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $false)|(c_and @ $true @ $true)|(~(X1934 @ (X1935 @ (c_binintersect @ (X1935 @ (c_Power @ c_Empty)) @ (X1935 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ c_Empty))) @ c_Empty)))))|(~(c_TransSet @ (X1935 @ c_Empty))|(~(c_In @ X1936 @ c_Empty)|(epred143_2 @ X1935 @ X1936))))|~(epred150_2 @ X1935 @ X1934)))&((~(X1934 @ (X1935 @ (X1935 @ (X1935 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $true)|(c_and @ $true @ $false)|(~(X1934 @ (X1935 @ (c_binintersect @ (X1935 @ (c_Power @ c_Empty)) @ (X1935 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ c_Empty))) @ c_Empty)))))|(~(c_TransSet @ (X1935 @ c_Empty))|(~(c_In @ X1936 @ c_Empty)|(epred143_2 @ X1935 @ X1936))))|~(epred150_2 @ X1935 @ X1934))&((X1934 @ (X1935 @ (X1935 @ (X1935 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $false)|(c_and @ $true @ $false)|(~(X1934 @ (X1935 @ (c_binintersect @ (X1935 @ (c_Power @ c_Empty)) @ (X1935 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ c_Empty))) @ c_Empty)))))|(~(c_TransSet @ (X1935 @ c_Empty))|(~(c_In @ X1936 @ c_Empty)|(epred143_2 @ X1935 @ X1936))))|~(epred150_2 @ X1935 @ X1934))))&(((~(X1934 @ (X1935 @ (X1935 @ (X1935 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $true)|(c_and @ $true @ $true)|(~(epred146_3 @ X1937 @ X1935 @ X1934)|~(epred147_3 @ X1937 @ X1935 @ X1934))|~(epred150_2 @ X1935 @ X1934))&((X1934 @ (X1935 @ (X1935 @ (X1935 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $false)|(c_and @ $true @ $true)|(~(epred146_3 @ X1937 @ X1935 @ X1934)|~(epred147_3 @ X1937 @ X1935 @ X1934))|~(epred150_2 @ X1935 @ X1934)))&((~(X1934 @ (X1935 @ (X1935 @ (X1935 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $true)|(c_and @ $true @ $false)|(~(epred146_3 @ X1937 @ X1935 @ X1934)|~(epred147_3 @ X1937 @ X1935 @ X1934))|~(epred150_2 @ X1935 @ X1934))&((X1934 @ (X1935 @ (X1935 @ (X1935 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $false)|(c_and @ $true @ $false)|(~(epred146_3 @ X1937 @ X1935 @ X1934)|~(epred147_3 @ X1937 @ X1935 @ X1934))|~(epred150_2 @ X1935 @ X1934)))))&(((((epred146_3 @ (esk220_2 @ X1938 @ X1939) @ X1939 @ X1938)|(X1938 @ (X1939 @ (c_binintersect @ (X1939 @ (c_Power @ c_Empty)) @ (X1939 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ c_Empty))) @ c_Empty)))))|(epred150_2 @ X1939 @ X1938))&((epred147_3 @ (esk220_2 @ X1938 @ X1939) @ X1939 @ X1938)|(X1938 @ (X1939 @ (c_binintersect @ (X1939 @ (c_Power @ c_Empty)) @ (X1939 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ c_Empty))) @ c_Empty)))))|(epred150_2 @ X1939 @ X1938)))&((((epred146_3 @ (esk220_2 @ X1938 @ X1939) @ X1939 @ X1938)|(c_TransSet @ (X1939 @ c_Empty))|(epred150_2 @ X1939 @ X1938))&((epred147_3 @ (esk220_2 @ X1938 @ X1939) @ X1939 @ X1938)|(c_TransSet @ (X1939 @ c_Empty))|(epred150_2 @ X1939 @ X1938)))&((((epred146_3 @ (esk220_2 @ X1938 @ X1939) @ X1939 @ X1938)|(c_In @ (esk219_2 @ X1938 @ X1939) @ c_Empty)|(epred150_2 @ X1939 @ X1938))&((epred147_3 @ (esk220_2 @ X1938 @ X1939) @ X1939 @ X1938)|(c_In @ (esk219_2 @ X1938 @ X1939) @ c_Empty)|(epred150_2 @ X1939 @ X1938)))&(((epred146_3 @ (esk220_2 @ X1938 @ X1939) @ X1939 @ X1938)|~(epred143_2 @ X1939 @ (esk219_2 @ X1938 @ X1939))|(epred150_2 @ X1939 @ X1938))&((epred147_3 @ (esk220_2 @ X1938 @ X1939) @ X1939 @ X1938)|~(epred143_2 @ X1939 @ (esk219_2 @ X1938 @ X1939))|(epred150_2 @ X1939 @ X1938))))))&(((((((~(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(~(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty))))))|(epred150_2 @ X1939 @ X1938))&(~(c_not @ $false)|(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(~(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty))))))|(epred150_2 @ X1939 @ X1938)))&((~(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $true)|(~(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty))))))|(epred150_2 @ X1939 @ X1938))&(~(c_not @ $false)|~(c_not @ $true)|(~(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty))))))|(epred150_2 @ X1939 @ X1938))))&(~(c_and @ $true @ $false)|(~(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty))))))|(epred150_2 @ X1939 @ X1938)))&((((~(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|((c_not @ $false)|(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty))))))|(epred150_2 @ X1939 @ X1938))&(~(c_not @ $false)|(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|((c_not @ $false)|(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty))))))|(epred150_2 @ X1939 @ X1938)))&((~(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $true)|((c_not @ $false)|(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty))))))|(epred150_2 @ X1939 @ X1938))&(~(c_not @ $false)|~(c_not @ $true)|((c_not @ $false)|(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty))))))|(epred150_2 @ X1939 @ X1938))))&(~(c_and @ $true @ $false)|((c_not @ $false)|(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty))))))|(epred150_2 @ X1939 @ X1938))))&(((((~(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(~(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $true))|(epred150_2 @ X1939 @ X1938))&(~(c_not @ $false)|(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(~(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $true))|(epred150_2 @ X1939 @ X1938)))&((~(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $true)|(~(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $true))|(epred150_2 @ X1939 @ X1938))&(~(c_not @ $false)|~(c_not @ $true)|(~(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $true))|(epred150_2 @ X1939 @ X1938))))&(~(c_and @ $true @ $false)|(~(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $true))|(epred150_2 @ X1939 @ X1938)))&((((~(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|((c_not @ $false)|(c_not @ $true))|(epred150_2 @ X1939 @ X1938))&(~(c_not @ $false)|(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|((c_not @ $false)|(c_not @ $true))|(epred150_2 @ X1939 @ X1938)))&((~(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $true)|((c_not @ $false)|(c_not @ $true))|(epred150_2 @ X1939 @ X1938))&(~(c_not @ $false)|~(c_not @ $true)|((c_not @ $false)|(c_not @ $true))|(epred150_2 @ X1939 @ X1938))))&(~(c_and @ $true @ $false)|((c_not @ $false)|(c_not @ $true))|(epred150_2 @ X1939 @ X1938)))))&((((~(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_and @ $true @ $true)|(epred150_2 @ X1939 @ X1938))&(~(c_not @ $false)|(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_and @ $true @ $true)|(epred150_2 @ X1939 @ X1938)))&((~(X1938 @ (X1939 @ (X1939 @ (X1939 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $true)|~(c_and @ $true @ $true)|(epred150_2 @ X1939 @ X1938))&(~(c_not @ $false)|~(c_not @ $true)|~(c_and @ $true @ $true)|(epred150_2 @ X1939 @ X1938))))&(~(c_and @ $true @ $false)|~(c_and @ $true @ $true)|(epred150_2 @ X1939 @ X1938))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_20])])])])])])])).
% 141.62/49.47 thf(c_0_27, plain, ![X12:$i > $i, X1:$i > $o]:(((epred150_2 @ X12 @ X1)|(epred149_0))), inference(split_conjunct,[status(thm)],[c_0_17])).
% 141.62/49.47 thf(c_0_28, plain, ![X480:$o, X481:$o, X482:$o, X483:$o, X484:$o]:(((((X480)|(X482)|~(c_and @ ((X480)) @ ((X481))))&(((X481)|(X482)|~(c_and @ ((X480)) @ ((X481))))&(~(X482)|(X482)|~(c_and @ ((X480)) @ ((X481))))))&((~(X483)|(~(X484)|(epred153_2 @ X483 @ X484))|(c_and @ ((X483)) @ ((X484))))&(~(epred153_2 @ X483 @ X484)|(c_and @ ((X483)) @ ((X484))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_21])])])])])])])).
% 141.62/49.47 thf(c_0_29, plain, ![X2042:$i, X2044:$i, X2045:$i]:(((~(epred167_0 @ X2042)|((c_Inj1 @ (esk239_1 @ X2042))=(X2042)))&(((c_Inj1 @ X2045)!=(X2044))|(epred167_0 @ X2044)))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[])])])])])])).
% 141.62/49.47 thf(c_0_30, plain, ![X1942:$i > $o, X1943:$i > $i, X1946:$i > $o, X1947:$i > $i, X1948:$i, X1949:$i]:(((((((~(X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $true)|(c_and @ $false @ $true)|((epred146_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|(X1942 @ (X1943 @ (c_binintersect @ (X1943 @ (c_Power @ c_Empty)) @ (X1943 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ c_Empty))) @ c_Empty))))))|~(epred151_2 @ X1943 @ X1942))&((X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $false)|(c_and @ $false @ $true)|((epred146_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|(X1942 @ (X1943 @ (c_binintersect @ (X1943 @ (c_Power @ c_Empty)) @ (X1943 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ c_Empty))) @ c_Empty))))))|~(epred151_2 @ X1943 @ X1942)))&((~(X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $true)|(c_and @ $false @ $false)|((epred146_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|(X1942 @ (X1943 @ (c_binintersect @ (X1943 @ (c_Power @ c_Empty)) @ (X1943 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ c_Empty))) @ c_Empty))))))|~(epred151_2 @ X1943 @ X1942))&((X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $false)|(c_and @ $false @ $false)|((epred146_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|(X1942 @ (X1943 @ (c_binintersect @ (X1943 @ (c_Power @ c_Empty)) @ (X1943 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ c_Empty))) @ c_Empty))))))|~(epred151_2 @ X1943 @ X1942))))&(((~(X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $true)|(c_and @ $false @ $true)|((epred147_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|(X1942 @ (X1943 @ (c_binintersect @ (X1943 @ (c_Power @ c_Empty)) @ (X1943 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ c_Empty))) @ c_Empty))))))|~(epred151_2 @ X1943 @ X1942))&((X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $false)|(c_and @ $false @ $true)|((epred147_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|(X1942 @ (X1943 @ (c_binintersect @ (X1943 @ (c_Power @ c_Empty)) @ (X1943 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ c_Empty))) @ c_Empty))))))|~(epred151_2 @ X1943 @ X1942)))&((~(X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $true)|(c_and @ $false @ $false)|((epred147_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|(X1942 @ (X1943 @ (c_binintersect @ (X1943 @ (c_Power @ c_Empty)) @ (X1943 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ c_Empty))) @ c_Empty))))))|~(epred151_2 @ X1943 @ X1942))&((X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $false)|(c_and @ $false @ $false)|((epred147_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|(X1942 @ (X1943 @ (c_binintersect @ (X1943 @ (c_Power @ c_Empty)) @ (X1943 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ c_Empty))) @ c_Empty))))))|~(epred151_2 @ X1943 @ X1942)))))&(((((~(X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $true)|(c_and @ $false @ $true)|((epred146_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|(c_TransSet @ (X1943 @ c_Empty)))|~(epred151_2 @ X1943 @ X1942))&((X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $false)|(c_and @ $false @ $true)|((epred146_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|(c_TransSet @ (X1943 @ c_Empty)))|~(epred151_2 @ X1943 @ X1942)))&((~(X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $true)|(c_and @ $false @ $false)|((epred146_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|(c_TransSet @ (X1943 @ c_Empty)))|~(epred151_2 @ X1943 @ X1942))&((X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $false)|(c_and @ $false @ $false)|((epred146_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|(c_TransSet @ (X1943 @ c_Empty)))|~(epred151_2 @ X1943 @ X1942))))&(((~(X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $true)|(c_and @ $false @ $true)|((epred147_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|(c_TransSet @ (X1943 @ c_Empty)))|~(epred151_2 @ X1943 @ X1942))&((X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $false)|(c_and @ $false @ $true)|((epred147_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|(c_TransSet @ (X1943 @ c_Empty)))|~(epred151_2 @ X1943 @ X1942)))&((~(X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $true)|(c_and @ $false @ $false)|((epred147_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|(c_TransSet @ (X1943 @ c_Empty)))|~(epred151_2 @ X1943 @ X1942))&((X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $false)|(c_and @ $false @ $false)|((epred147_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|(c_TransSet @ (X1943 @ c_Empty)))|~(epred151_2 @ X1943 @ X1942)))))&(((((~(X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $true)|(c_and @ $false @ $true)|((epred146_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|(c_In @ (esk221_2 @ X1942 @ X1943) @ c_Empty))|~(epred151_2 @ X1943 @ X1942))&((X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $false)|(c_and @ $false @ $true)|((epred146_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|(c_In @ (esk221_2 @ X1942 @ X1943) @ c_Empty))|~(epred151_2 @ X1943 @ X1942)))&((~(X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $true)|(c_and @ $false @ $false)|((epred146_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|(c_In @ (esk221_2 @ X1942 @ X1943) @ c_Empty))|~(epred151_2 @ X1943 @ X1942))&((X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $false)|(c_and @ $false @ $false)|((epred146_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|(c_In @ (esk221_2 @ X1942 @ X1943) @ c_Empty))|~(epred151_2 @ X1943 @ X1942))))&(((~(X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $true)|(c_and @ $false @ $true)|((epred147_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|(c_In @ (esk221_2 @ X1942 @ X1943) @ c_Empty))|~(epred151_2 @ X1943 @ X1942))&((X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $false)|(c_and @ $false @ $true)|((epred147_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|(c_In @ (esk221_2 @ X1942 @ X1943) @ c_Empty))|~(epred151_2 @ X1943 @ X1942)))&((~(X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $true)|(c_and @ $false @ $false)|((epred147_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|(c_In @ (esk221_2 @ X1942 @ X1943) @ c_Empty))|~(epred151_2 @ X1943 @ X1942))&((X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $false)|(c_and @ $false @ $false)|((epred147_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|(c_In @ (esk221_2 @ X1942 @ X1943) @ c_Empty))|~(epred151_2 @ X1943 @ X1942)))))&((((~(X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $true)|(c_and @ $false @ $true)|((epred146_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|~(epred143_2 @ X1943 @ (esk221_2 @ X1942 @ X1943)))|~(epred151_2 @ X1943 @ X1942))&((X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $false)|(c_and @ $false @ $true)|((epred146_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|~(epred143_2 @ X1943 @ (esk221_2 @ X1942 @ X1943)))|~(epred151_2 @ X1943 @ X1942)))&((~(X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $true)|(c_and @ $false @ $false)|((epred146_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|~(epred143_2 @ X1943 @ (esk221_2 @ X1942 @ X1943)))|~(epred151_2 @ X1943 @ X1942))&((X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $false)|(c_and @ $false @ $false)|((epred146_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|~(epred143_2 @ X1943 @ (esk221_2 @ X1942 @ X1943)))|~(epred151_2 @ X1943 @ X1942))))&(((~(X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $true)|(c_and @ $false @ $true)|((epred147_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|~(epred143_2 @ X1943 @ (esk221_2 @ X1942 @ X1943)))|~(epred151_2 @ X1943 @ X1942))&((X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $false)|(c_and @ $false @ $true)|((epred147_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|~(epred143_2 @ X1943 @ (esk221_2 @ X1942 @ X1943)))|~(epred151_2 @ X1943 @ X1942)))&((~(X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $true)|(c_and @ $false @ $false)|((epred147_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|~(epred143_2 @ X1943 @ (esk221_2 @ X1942 @ X1943)))|~(epred151_2 @ X1943 @ X1942))&((X1942 @ (X1943 @ (X1943 @ (X1943 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $false)|(c_and @ $false @ $false)|((epred147_3 @ (esk222_2 @ X1942 @ X1943) @ X1943 @ X1942)|~(epred143_2 @ X1943 @ (esk221_2 @ X1942 @ X1943)))|~(epred151_2 @ X1943 @ X1942))))))))&(((~(X1946 @ (X1947 @ (c_binintersect @ (X1947 @ (c_Power @ c_Empty)) @ (X1947 @ (c_binrep @ (c_Power @ (c_Power @ (c_Power @ c_Empty))) @ c_Empty)))))|(~(c_TransSet @ (X1947 @ c_Empty))|(~(c_In @ X1948 @ c_Empty)|(epred143_2 @ X1947 @ X1948)))|(epred151_2 @ X1947 @ X1946))&(~(epred146_3 @ X1949 @ X1947 @ X1946)|~(epred147_3 @ X1949 @ X1947 @ X1946)|(epred151_2 @ X1947 @ X1946)))&(((((((~(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(~(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty))))))|(epred151_2 @ X1947 @ X1946))&(~(c_not @ $false)|(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(~(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty))))))|(epred151_2 @ X1947 @ X1946)))&((~(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $true)|(~(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty))))))|(epred151_2 @ X1947 @ X1946))&(~(c_not @ $false)|~(c_not @ $true)|(~(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty))))))|(epred151_2 @ X1947 @ X1946))))&(~(c_and @ $false @ $false)|(~(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty))))))|(epred151_2 @ X1947 @ X1946)))&((((~(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|((c_not @ $false)|(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty))))))|(epred151_2 @ X1947 @ X1946))&(~(c_not @ $false)|(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|((c_not @ $false)|(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty))))))|(epred151_2 @ X1947 @ X1946)))&((~(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $true)|((c_not @ $false)|(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty))))))|(epred151_2 @ X1947 @ X1946))&(~(c_not @ $false)|~(c_not @ $true)|((c_not @ $false)|(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty))))))|(epred151_2 @ X1947 @ X1946))))&(~(c_and @ $false @ $false)|((c_not @ $false)|(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty))))))|(epred151_2 @ X1947 @ X1946))))&(((((~(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(~(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $true))|(epred151_2 @ X1947 @ X1946))&(~(c_not @ $false)|(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(~(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $true))|(epred151_2 @ X1947 @ X1946)))&((~(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $true)|(~(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $true))|(epred151_2 @ X1947 @ X1946))&(~(c_not @ $false)|~(c_not @ $true)|(~(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $true))|(epred151_2 @ X1947 @ X1946))))&(~(c_and @ $false @ $false)|(~(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_not @ $true))|(epred151_2 @ X1947 @ X1946)))&((((~(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|((c_not @ $false)|(c_not @ $true))|(epred151_2 @ X1947 @ X1946))&(~(c_not @ $false)|(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|((c_not @ $false)|(c_not @ $true))|(epred151_2 @ X1947 @ X1946)))&((~(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $true)|((c_not @ $false)|(c_not @ $true))|(epred151_2 @ X1947 @ X1946))&(~(c_not @ $false)|~(c_not @ $true)|((c_not @ $false)|(c_not @ $true))|(epred151_2 @ X1947 @ X1946))))&(~(c_and @ $false @ $false)|((c_not @ $false)|(c_not @ $true))|(epred151_2 @ X1947 @ X1946)))))&((((~(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_and @ $false @ $true)|(epred151_2 @ X1947 @ X1946))&(~(c_not @ $false)|(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_and @ $false @ $true)|(epred151_2 @ X1947 @ X1946)))&((~(X1946 @ (X1947 @ (X1947 @ (X1947 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|~(c_not @ $true)|~(c_and @ $false @ $true)|(epred151_2 @ X1947 @ X1946))&(~(c_not @ $false)|~(c_not @ $true)|~(c_and @ $false @ $true)|(epred151_2 @ X1947 @ X1946))))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|(epred151_2 @ X1947 @ X1946))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_22])])])])])])])).
% 141.62/49.47 thf(c_0_31, plain, ![X12:$i > $i, X1:$i > $o]:(((epred151_2 @ X12 @ X1)|(epred149_0))), inference(split_conjunct,[status(thm)],[c_0_17])).
% 141.62/49.47 thf(c_0_32, plain, ![X2:$i]:(((c_not @ (($true)))|~((c_In @ X2 @ c_Empty)))), inference(split_conjunct,[status(thm)],[c_0_23])).
% 141.62/49.47 thf(c_0_33, plain, ~((c_not @ (($true)))), inference(sr,[status(thm)],[c_0_24, c_0_25])).
% 141.62/49.47 thf(c_0_34, plain, ![X12:$i > $i, X2:$i, X1:$i > $o]:(((c_not @ (($true)))|(c_and @ (($true)) @ (~($true)))|~((X1 @ (X12 @ (X12 @ (X12 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty))))))|~((epred146_3 @ X2 @ X12 @ X1))|~((epred147_3 @ X2 @ X12 @ X1))|~((epred150_2 @ X12 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_26])).
% 141.62/49.47 thf(c_0_35, plain, ![X12:$i > $i, X1:$i > $o]:((epred150_2 @ X12 @ X1)), inference(sr,[status(thm)],[c_0_27, c_0_25])).
% 141.62/49.47 thf(c_0_36, plain, ![X5:$o]:(~((c_and @ ((X5)) @ (~($true))))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_28])])])).
% 141.62/49.47 thf(c_0_37, plain, ![X2:$i, X6:$i]:(((epred167_0 @ X6)|((c_Inj1 @ X2)!=(X6)))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 141.62/49.47 thf(c_0_38, plain, ![X12:$i > $i, X1:$i > $o]:(((c_not @ (($true)))|(c_and @ (~($true)) @ (~($true)))|(epred146_3 @ (esk222_2 @ X1 @ X12) @ X12 @ X1)|(c_In @ (esk221_2 @ X1 @ X12) @ c_Empty)|~((X1 @ (X12 @ (X12 @ (X12 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty))))))|~((epred151_2 @ X12 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_30])).
% 141.62/49.47 thf(c_0_39, plain, ![X12:$i > $i, X1:$i > $o]:((epred151_2 @ X12 @ X1)), inference(sr,[status(thm)],[c_0_31, c_0_25])).
% 141.62/49.47 thf(c_0_40, plain, ![X2:$i]:(~((c_In @ X2 @ c_Empty))), inference(sr,[status(thm)],[c_0_32, c_0_33])).
% 141.62/49.47 thf(c_0_41, plain, ![X12:$i > $i, X1:$i > $o]:(((c_not @ (($true)))|(c_and @ (~($true)) @ (~($true)))|(epred147_3 @ (esk222_2 @ X1 @ X12) @ X12 @ X1)|(c_In @ (esk221_2 @ X1 @ X12) @ c_Empty)|~((X1 @ (X12 @ (X12 @ (X12 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty))))))|~((epred151_2 @ X12 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_30])).
% 141.62/49.47 thf(c_0_42, plain, ![X12:$i > $i, X2:$i, X1:$i > $o]:((~((X1 @ (X12 @ (X12 @ (X12 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty))))))|~((epred146_3 @ X2 @ X12 @ X1))|~((epred147_3 @ X2 @ X12 @ X1)))), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_34, c_0_35])]), c_0_33]), c_0_36])).
% 141.62/49.47 thf(c_0_43, plain, ![X2:$i]:((epred167_0 @ (c_Inj1 @ X2))), inference(er,[status(thm)],[c_0_37])).
% 141.62/49.47 thf(c_0_44, plain, ![X12:$i > $i, X1:$i > $o]:(((X1 @ (X12 @ (X12 @ (X12 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_and @ (~($true)) @ (($true)))|(epred146_3 @ (esk222_2 @ X1 @ X12) @ X12 @ X1)|(c_In @ (esk221_2 @ X1 @ X12) @ c_Empty)|~((c_not @ (~($true))))|~((epred151_2 @ X12 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_30])).
% 141.62/49.47 thf(c_0_45, plain, ![X5:$o]:(~((c_and @ (~($true)) @ ((X5))))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_28])])])).
% 141.62/49.47 thf(c_0_46, plain, ![X1:$i > $o, X12:$i > $i]:(((epred146_3 @ (esk222_2 @ X1 @ X12) @ X12 @ X1)|~((X1 @ (X12 @ (X12 @ (X12 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))))), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_38, c_0_39])]), c_0_33]), c_0_36]), c_0_40])).
% 141.62/49.47 thf(c_0_47, plain, ![X12:$i > $i, X1:$i > $o]:(((X1 @ (X12 @ (X12 @ (X12 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))|(c_and @ (~($true)) @ (($true)))|(epred147_3 @ (esk222_2 @ X1 @ X12) @ X12 @ X1)|(c_In @ (esk221_2 @ X1 @ X12) @ c_Empty)|~((c_not @ (~($true))))|~((epred151_2 @ X12 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_30])).
% 141.62/49.47 thf(c_0_48, plain, ![X1:$i > $o, X12:$i > $i]:(((epred147_3 @ (esk222_2 @ X1 @ X12) @ X12 @ X1)|~((X1 @ (X12 @ (X12 @ (X12 @ (c_binrep @ (c_binrep @ (c_Power @ (c_binrep @ (c_Power @ (c_Power @ c_Empty)) @ c_Empty)) @ (c_Power @ c_Empty)) @ c_Empty)))))))), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_41, c_0_39])]), c_0_33]), c_0_36]), c_0_40])).
% 141.62/49.47 thf(c_0_49, plain, ![X2:$i]:((~((epred146_3 @ X2 @ c_Inj1 @ epred167_0))|~((epred147_3 @ X2 @ c_Inj1 @ epred167_0)))), inference(spm,[status(thm)],[c_0_42, c_0_43])).
% 141.62/49.47 thf(c_0_50, plain, ![X12:$i > $i, X1:$i > $o]:((epred146_3 @ (esk222_2 @ X1 @ X12) @ X12 @ X1)), inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_44, c_0_19]), c_0_39])]), c_0_45]), c_0_40]), c_0_46])).
% 141.62/49.47 thf(c_0_51, plain, ![X12:$i > $i, X1:$i > $o]:((epred147_3 @ (esk222_2 @ X1 @ X12) @ X12 @ X1)), inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_47, c_0_19]), c_0_39])]), c_0_45]), c_0_40]), c_0_48])).
% 141.62/49.47 thf(c_0_52, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_49, c_0_50]), c_0_51])]), ['proof']).
% 141.62/49.47 % SZS output end CNFRefutation
% 141.62/49.47 % Parsed axioms : 213
% 141.62/49.47 % Removed by relevancy pruning/SinE : 0
% 141.62/49.47 % Initial clauses : 469172
% 141.62/49.47 % Removed in clause preprocessing : 464072
% 141.62/49.47 % Initial clauses in saturation : 5100
% 141.62/49.47 % Processed clauses : 6949
% 141.62/49.47 % ...of these trivial : 474
% 141.62/49.47 % ...subsumed : 3661
% 141.62/49.47 % ...remaining for further processing : 2814
% 141.62/49.47 % Other redundant clauses eliminated : 89
% 141.62/49.47 % Clauses deleted for lack of memory : 0
% 141.62/49.47 % Backward-subsumed : 149
% 141.62/49.47 % Backward-rewritten : 80
% 141.62/49.47 % Generated clauses : 15367
% 141.62/49.47 % ...of the previous two non-redundant : 14610
% 141.62/49.47 % ...aggressively subsumed : 0
% 141.62/49.47 % Contextual simplify-reflections : 286
% 141.62/49.47 % Paramodulations : 15238
% 141.62/49.47 % Factorizations : 28
% 141.62/49.47 % NegExts : 0
% 141.62/49.47 % Equation resolutions : 89
% 141.62/49.47 % Disequality decompositions : 0
% 141.62/49.47 % Total rewrite steps : 4499
% 141.62/49.47 % ...of those cached : 4032
% 141.62/49.47 % Propositional unsat checks : 0
% 141.62/49.47 % Propositional check models : 0
% 141.62/49.47 % Propositional check unsatisfiable : 0
% 141.62/49.47 % Propositional clauses : 0
% 141.62/49.47 % Propositional clauses after purity: 0
% 141.62/49.47 % Propositional unsat core size : 0
% 141.62/49.47 % Propositional preprocessing time : 0.000
% 141.62/49.47 % Propositional encoding time : 0.000
% 141.62/49.47 % Propositional solver time : 0.000
% 141.62/49.47 % Success case prop preproc time : 0.000
% 141.62/49.47 % Success case prop encoding time : 0.000
% 141.62/49.47 % Success case prop solver time : 0.000
% 141.62/49.47 % Current number of processed clauses : 1306
% 141.62/49.47 % Positive orientable unit clauses : 136
% 141.62/49.47 % Positive unorientable unit clauses: 5
% 141.62/49.47 % Negative unit clauses : 141
% 141.62/49.47 % Non-unit-clauses : 1024
% 141.62/49.47 % Current number of unprocessed clauses: 13957
% 141.62/49.47 % ...number of literals in the above : 60450
% 141.62/49.47 % Current number of archived formulas : 0
% 141.62/49.47 % Current number of archived clauses : 1461
% 141.62/49.47 % Clause-clause subsumption calls (NU) : 1272680
% 141.62/49.47 % Rec. Clause-clause subsumption calls : 327708
% 141.62/49.47 % Non-unit clause-clause subsumptions : 1251
% 141.62/49.47 % Unit Clause-clause subsumption calls : 27307
% 141.62/49.47 % Rewrite failures with RHS unbound : 0
% 141.62/49.47 % BW rewrite match attempts : 121
% 141.62/49.47 % BW rewrite match successes : 25
% 141.62/49.47 % Condensation attempts : 0
% 141.62/49.47 % Condensation successes : 0
% 141.62/49.47 % Termbank termtop insertions : 20378258
% 141.62/49.47 % Search garbage collected termcells : 2014707
% 141.62/49.47
% 141.62/49.47 % -------------------------------------------------
% 141.62/49.48 % User time : 44.216 s
% 141.62/49.48 % System time : 2.623 s
% 141.62/49.48 % Total time : 46.839 s
% 141.62/49.48 % Maximum resident set size: 1257872 pages
% 141.62/49.48
% 141.62/49.48 % -------------------------------------------------
% 141.62/49.48 % User time : 44.228 s
% 141.62/49.48 % System time : 2.825 s
% 141.62/49.48 % Total time : 47.053 s
% 141.62/49.48 % Maximum resident set size: 4864 pages
% 141.62/49.48 % E exiting
%------------------------------------------------------------------------------