%------------------------------------------------------------------------------
% File : E-SAT---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 : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:44:54 AM UTC 2026
% Result : Theorem 211.07s 45.96s
% Output : CNFRefutation 211.07s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO873^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n011.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Tue Sep 29 17:23:01 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.24 Running higher-order theorem proving
% 0.22/0.27 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.32pidki59Q/E---3.1_390568.p
% 211.07/45.96 % Version: 3.5.1-ho
% 211.07/45.96 % partial match(1): HSLMSMSSSSLCHSA
% 211.07/45.96 % Preprocessing class: HSLMSLSSSSLCHSA.
% 211.07/45.96 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 211.07/45.96 % Starting pre_casc_6 with 1500s (5) cores
% 211.07/45.96 % Starting ehoh_best7 with 300s (1) cores
% 211.07/45.96 % Starting new_bool_8 with 300s (1) cores
% 211.07/45.96 % Starting new_ho_11 with 300s (1) cores
% 211.07/45.96 % ehoh_best7 with pid 390594 completed with status 0
% 211.07/45.96 % Result found by ehoh_best7
% 211.07/45.96 % partial match(1): HSLMSMSSSSLCHSA
% 211.07/45.96 % Preprocessing class: HSLMSLSSSSLCHSA.
% 211.07/45.96 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 211.07/45.96 % Starting pre_casc_6 with 1500s (5) cores
% 211.07/45.96 % Starting ehoh_best7 with 300s (1) cores
% 211.07/45.96 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 211.07/45.96 % No SInE strategy applied
% 211.07/45.96 % Search class: HGHSM-SMLM33-DHSFFSBC
% 211.07/45.96 % partial match(1): HGHSM-SMLM32-DHSFFSBC
% 211.07/45.96 % Scheduled 7 strats onto 1 cores with 287 seconds (287 total)
% 211.07/45.96 % Starting SubtermCWHack with 26s (1) cores
% 211.07/45.96 % SubtermCWHack with pid 390609 completed with status 8
% 211.07/45.96 % Starting ehoh_best7 with 29s (1) cores
% 211.07/45.96 % ehoh_best7 with pid 390637 completed with status 0
% 211.07/45.96 % Result found by ehoh_best7
% 211.07/45.96 % partial match(1): HSLMSMSSSSLCHSA
% 211.07/45.96 % Preprocessing class: HSLMSLSSSSLCHSA.
% 211.07/45.96 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 211.07/45.96 % Starting pre_casc_6 with 1500s (5) cores
% 211.07/45.96 % Starting ehoh_best7 with 300s (1) cores
% 211.07/45.96 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 211.07/45.96 % No SInE strategy applied
% 211.07/45.96 % Search class: HGHSM-SMLM33-DHSFFSBC
% 211.07/45.96 % partial match(1): HGHSM-SMLM32-DHSFFSBC
% 211.07/45.96 % Scheduled 7 strats onto 1 cores with 287 seconds (287 total)
% 211.07/45.96 % Starting SubtermCWHack with 26s (1) cores
% 211.07/45.96 % SubtermCWHack with pid 390609 completed with status 8
% 211.07/45.96 % Starting ehoh_best7 with 29s (1) cores
% 211.07/45.96 % Preprocessing time : 0.224 s
% 211.07/45.96 % Presaturation interreduction done
% 211.07/45.96
% 211.07/45.96 % Proof found!
% 211.07/45.96 % SZS status Theorem
% 211.07/45.96 % SZS output start CNFRefutation
% 211.07/45.96 thf(decl_24, type, c_False: $o).
% 211.07/45.96 thf(decl_26, type, c_not: $o > $o).
% 211.07/45.96 thf(decl_27, type, c_and: $o > $o > $o).
% 211.07/45.96 thf(decl_30, type, c_In: $i > $i > $o).
% 211.07/45.96 thf(decl_31, type, c_Subq: $i > $i > $o).
% 211.07/45.96 thf(decl_32, type, c_Empty: $i).
% 211.07/45.96 thf(decl_34, type, c_Power: $i > $i).
% 211.07/45.96 thf(decl_36, type, c_TransSet: $i > $o).
% 211.07/45.96 thf(decl_42, type, c_exactly2: $i > $o).
% 211.07/45.96 thf(decl_72, type, c_binintersect: $i > $i > $i).
% 211.07/45.96 thf(decl_80, type, c_ordsucc: $i > $i).
% 211.07/45.96 thf(decl_94, type, c_binrep: $i > $i > $i).
% 211.07/45.96 thf(decl_96, type, c_setprod: $i > $i > $i).
% 211.07/45.96 thf(decl_114, type, c_SNo: $i > $o).
% 211.07/45.96 thf(decl_269, type, epred143_2: ($i > $i) > $i > $o).
% 211.07/45.96 thf(decl_272, type, epred146_3: $i > ($i > $i) > ($i > $o) > $o).
% 211.07/45.96 thf(decl_273, type, epred147_3: $i > ($i > $i) > ($i > $o) > $o).
% 211.07/45.96 thf(decl_275, type, epred149_0: $o).
% 211.07/45.96 thf(decl_276, type, epred150_2: ($i > $i) > ($i > $o) > $o).
% 211.07/45.96 thf(decl_277, type, epred151_2: ($i > $i) > ($i > $o) > $o).
% 211.07/45.96 thf(decl_278, type, esk1_0: $i).
% 211.07/45.96 thf(decl_290, type, epred152_0: $o).
% 211.07/45.96 thf(decl_291, type, epred153_2: $o > $o > $o).
% 211.07/45.96 thf(decl_293, type, esk13_2: $i > $i > $i).
% 211.07/45.96 thf(decl_336, type, epred159_0: $i > $o).
% 211.07/45.96 thf(decl_337, type, esk52_0: $i > $i).
% 211.07/45.96 thf(decl_506, type, esk219_2: ($i > $o) > ($i > $i) > $i).
% 211.07/45.96 thf(decl_507, type, esk220_2: ($i > $o) > ($i > $i) > $i).
% 211.07/45.96 thf(decl_508, type, esk221_2: ($i > $o) > ($i > $i) > $i).
% 211.07/45.96 thf(decl_509, type, esk222_2: ($i > $o) > ($i > $i) > $i).
% 211.07/45.96 thf(decl_519, type, esk228_0: ($i > $i) > $i > $i).
% 211.07/45.96 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.32pidki59Q/E---3.1_390568.p', conj)).
% 211.07/45.96 thf(ax13, axiom, ((c_not)=(^[X17:$o]:((((X17))=>((c_False)))))), file('/export/starexec/sandbox2/tmp/tmp.32pidki59Q/E---3.1_390568.p', ax13)).
% 211.07/45.96 thf(ax5, axiom, (c_not @ (?[X7:$i]:((c_In @ X7 @ c_Empty)))), file('/export/starexec/sandbox2/tmp/tmp.32pidki59Q/E---3.1_390568.p', ax5)).
% 211.07/45.96 thf(ax11, axiom, ((c_False)<=>![X15:$o]:((X15))), file('/export/starexec/sandbox2/tmp/tmp.32pidki59Q/E---3.1_390568.p', ax11)).
% 211.07/45.96 thf(ax14, axiom, ((c_and)=(^[X18:$o, X19:$o]:(![X20:$o]:((((((X18))=>((((X19))=>((X20))))))=>((X20))))))), file('/export/starexec/sandbox2/tmp/tmp.32pidki59Q/E---3.1_390568.p', ax14)).
% 211.07/45.96 thf(ax17, axiom, ((c_Subq)=(^[X26:$i, X2:$i]:(![X9:$i]:((((c_In @ X9 @ X26))=>((c_In @ X9 @ X2))))))), file('/export/starexec/sandbox2/tmp/tmp.32pidki59Q/E---3.1_390568.p', ax17)).
% 211.07/45.96 thf(c_0_6, 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])).
% 211.07/45.96 thf(c_0_7, 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)).
% 211.07/45.96 thf(c_0_8, 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)).
% 211.07/45.96 thf(c_0_9, 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)).
% 211.07/45.96 thf(c_0_10, plain, ![X231:$o]:(((c_not @ ((X231)))<=>((X231)=>(c_False)))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[ax13])])).
% 211.07/45.96 thf(c_0_11, 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)).
% 211.07/45.96 thf(c_0_12, 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)).
% 211.07/45.96 thf(c_0_13, 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)).
% 211.07/45.96 thf(c_0_14, 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_6]), c_0_7]), c_0_8]), c_0_9])).
% 211.07/45.96 thf(c_0_15, 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])).
% 211.07/45.96 thf(c_0_16, 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_10])])])])).
% 211.07/45.96 thf(c_0_17, plain, ![X477:$o]:(((~(c_False)|(X477))&(~(epred152_0)|(c_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)],[ax11])])])])])).
% 211.07/45.96 thf(c_0_18, 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_8, c_0_11]), c_0_12]), c_0_13])).
% 211.07/45.96 thf(c_0_19, 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])])).
% 211.07/45.96 thf(c_0_20, 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_7]), c_0_8]), c_0_9])).
% 211.07/45.96 thf(c_0_21, 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_14])])])])])).
% 211.07/45.96 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_9, c_0_11]), c_0_12]), c_0_13])).
% 211.07/45.96 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_15])])])])])).
% 211.07/45.96 thf(c_0_24, plain, ((c_False)|~((c_not @ (($true))))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_16])])])).
% 211.07/45.96 thf(c_0_25, plain, ~((c_False)), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_17])])])).
% 211.07/45.96 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_18])])])])])])])).
% 211.07/45.96 thf(c_0_27, plain, ![X2031:$i, X2032:$i > $i]:(((esk228_0 @ X2032 @ X2031)=(c_Power @ (X2032 @ X2031)))), inference(variable_rename,[status(thm)],[])).
% 211.07/45.96 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_19])])])])])])])).
% 211.07/45.96 thf(c_0_29, 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_20])])])])])).
% 211.07/45.96 thf(c_0_30, negated_conjecture, (~((c_not @ (~($true))))|~((epred149_0))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 211.07/45.96 thf(c_0_31, plain, (c_not @ (~($true))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_16])])])).
% 211.07/45.96 thf(c_0_32, plain, ![X238:$i, X239:$i]:(((c_Subq @ X238 @ X239)<=>![X9:$i]:(((c_In @ X9 @ X238)=>(c_In @ X9 @ X239))))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[ax17])])).
% 211.07/45.96 thf(c_0_33, 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])])])])])])])).
% 211.07/45.96 thf(c_0_34, plain, ![X2:$i]:(((c_not @ (($true)))|~((c_In @ X2 @ c_Empty)))), inference(split_conjunct,[status(thm)],[c_0_23])).
% 211.07/45.96 thf(c_0_35, plain, ~((c_not @ (($true)))), inference(sr,[status(thm)],[c_0_24, c_0_25])).
% 211.07/45.96 thf(c_0_36, 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])).
% 211.07/45.96 thf(c_0_37, plain, ![X12:$i > $i, X2:$i]:(((esk228_0 @ X12 @ X2)=(c_Power @ (X12 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_27])).
% 211.07/45.96 thf(c_0_38, plain, ![X5:$o]:(~((c_and @ ((X5)) @ (~($true))))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_28])])])).
% 211.07/45.96 thf(c_0_39, plain, ![X12:$i > $i, X1:$i > $o]:(((epred150_2 @ X12 @ X1)|(epred149_0))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 211.07/45.96 thf(c_0_40, negated_conjecture, ~((epred149_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_30, c_0_31])])).
% 211.07/45.96 thf(c_0_41, plain, ![X494:$i, X495:$i, X496:$i, X497:$i, X498:$i]:(((~(c_Subq @ X494 @ X495)|(~(c_In @ X496 @ X494)|(c_In @ X496 @ X495)))&(((c_In @ (esk13_2 @ X497 @ X498) @ X497)|(c_Subq @ X497 @ X498))&(~(c_In @ (esk13_2 @ X497 @ X498) @ X498)|(c_Subq @ X497 @ X498))))), 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_32])])])])])])])).
% 211.07/45.96 thf(c_0_42, 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_33])).
% 211.07/45.96 thf(c_0_43, plain, ![X5:$o]:(~((c_and @ (~($true)) @ ((X5))))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_28])])])).
% 211.07/45.96 thf(c_0_44, plain, ![X2:$i]:(~((c_In @ X2 @ c_Empty))), inference(sr,[status(thm)],[c_0_34, c_0_35])).
% 211.07/45.96 thf(c_0_45, 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_33])).
% 211.07/45.96 thf(c_0_46, plain, ![X12:$i > $i, X2:$i, X1:$i > $o]:((~((X1 @ (X12 @ (X12 @ (X12 @ (c_binrep @ (c_binrep @ (esk228_0 @ (c_binrep @ (esk228_0 @ 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(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_36, c_0_37]), c_0_37]), c_0_35]), c_0_38])).
% 211.07/45.96 thf(c_0_47, plain, ![X12:$i > $i, X1:$i > $o]:((epred150_2 @ X12 @ X1)), inference(sr,[status(thm)],[c_0_39, c_0_40])).
% 211.07/45.96 thf(c_0_48, plain, ![X2:$i, X6:$i]:(((c_In @ (esk13_2 @ X2 @ X6) @ X2)|(c_Subq @ X2 @ X6))), inference(split_conjunct,[status(thm)],[c_0_41])).
% 211.07/45.96 thf(c_0_49, 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_33])).
% 211.07/45.96 thf(c_0_50, plain, ![X12:$i > $i, X1:$i > $o]:(((X1 @ (X12 @ (X12 @ (X12 @ (c_binrep @ (c_binrep @ (esk228_0 @ (c_binrep @ (esk228_0 @ c_Power @ c_Empty)) @ c_Empty) @ (c_Power @ c_Empty)) @ c_Empty)))))|(epred146_3 @ (esk222_2 @ X1 @ X12) @ X12 @ X1)|~((epred151_2 @ X12 @ X1)))), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_42, c_0_37]), c_0_37]), c_0_31])]), c_0_43]), c_0_44])).
% 211.07/45.96 thf(c_0_51, plain, ![X12:$i > $i, X1:$i > $o]:(((epred151_2 @ X12 @ X1)|(epred149_0))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 211.07/45.96 thf(c_0_52, 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_33])).
% 211.07/45.96 thf(c_0_53, plain, ![X12:$i > $i, X1:$i > $o]:(((X1 @ (X12 @ (X12 @ (X12 @ (c_binrep @ (c_binrep @ (esk228_0 @ (c_binrep @ (esk228_0 @ c_Power @ c_Empty)) @ c_Empty) @ (c_Power @ c_Empty)) @ c_Empty)))))|(epred147_3 @ (esk222_2 @ X1 @ X12) @ X12 @ X1)|~((epred151_2 @ X12 @ X1)))), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_45, c_0_37]), c_0_37]), c_0_31])]), c_0_43]), c_0_44])).
% 211.07/45.96 thf(c_0_54, plain, ![X12:$i > $i, X2:$i, X1:$i > $o]:((~((X1 @ (X12 @ (X12 @ (X12 @ (c_binrep @ (c_binrep @ (esk228_0 @ (c_binrep @ (esk228_0 @ c_Power @ c_Empty)) @ c_Empty) @ (c_Power @ c_Empty)) @ c_Empty))))))|~((epred146_3 @ X2 @ X12 @ X1))|~((epred147_3 @ X2 @ X12 @ X1)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_46, c_0_47])])).
% 211.07/45.96 thf(c_0_55, plain, ![X2:$i]:((c_Subq @ c_Empty @ X2)), inference(spm,[status(thm)],[c_0_44, c_0_48])).
% 211.07/45.96 thf(c_0_56, plain, ![X12:$i > $i, X1:$i > $o]:(((epred146_3 @ (esk222_2 @ X1 @ X12) @ X12 @ X1)|~((epred151_2 @ X12 @ X1)))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_49, c_0_37]), c_0_37]), c_0_35]), c_0_38]), c_0_44]), c_0_50])).
% 211.07/45.96 thf(c_0_57, plain, ![X12:$i > $i, X1:$i > $o]:((epred151_2 @ X12 @ X1)), inference(sr,[status(thm)],[c_0_51, c_0_40])).
% 211.07/45.96 thf(c_0_58, plain, ![X12:$i > $i, X1:$i > $o]:(((epred147_3 @ (esk222_2 @ X1 @ X12) @ X12 @ X1)|~((epred151_2 @ X12 @ X1)))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_52, c_0_37]), c_0_37]), c_0_35]), c_0_38]), c_0_44]), c_0_53])).
% 211.07/45.96 thf(c_0_59, plain, ![X2:$i, X12:$i > $i]:((~((epred146_3 @ X2 @ X12 @ (c_Subq @ c_Empty)))|~((epred147_3 @ X2 @ X12 @ (c_Subq @ c_Empty))))), inference(spm,[status(thm)],[c_0_54, c_0_55])).
% 211.07/45.96 thf(c_0_60, plain, ![X12:$i > $i, X1:$i > $o]:((epred146_3 @ (esk222_2 @ X1 @ X12) @ X12 @ X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_56, c_0_57])])).
% 211.07/45.96 thf(c_0_61, plain, ![X12:$i > $i, X1:$i > $o]:((epred147_3 @ (esk222_2 @ X1 @ X12) @ X12 @ X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_58, c_0_57])])).
% 211.07/45.96 thf(c_0_62, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_59, c_0_60]), c_0_61])]), ['proof']).
% 211.07/45.96 % SZS output end CNFRefutation
% 211.07/45.96 % Parsed axioms : 213
% 211.07/45.96 % Removed by relevancy pruning/SinE : 0
% 211.07/45.96 % Initial clauses : 469172
% 211.07/45.96 % Removed in clause preprocessing : 464072
% 211.07/45.96 % Initial clauses in saturation : 5100
% 211.07/45.96 % Processed clauses : 7264
% 211.07/45.96 % ...of these trivial : 197
% 211.07/45.96 % ...subsumed : 3643
% 211.07/45.96 % ...remaining for further processing : 3424
% 211.07/45.96 % Other redundant clauses eliminated : 448
% 211.07/45.96 % Clauses deleted for lack of memory : 0
% 211.07/45.96 % Backward-subsumed : 210
% 211.07/45.96 % Backward-rewritten : 456
% 211.07/45.96 % Generated clauses : 27487
% 211.07/45.96 % ...of the previous two non-redundant : 26625
% 211.07/45.96 % ...aggressively subsumed : 0
% 211.07/45.96 % Contextual simplify-reflections : 459
% 211.07/45.96 % Paramodulations : 27036
% 211.07/45.96 % Factorizations : 0
% 211.07/45.96 % NegExts : 0
% 211.07/45.96 % Equation resolutions : 450
% 211.07/45.96 % Disequality decompositions : 0
% 211.07/45.96 % Total rewrite steps : 5089
% 211.07/45.96 % ...of those cached : 4578
% 211.07/45.96 % Propositional unsat checks : 0
% 211.07/45.96 % Propositional check models : 0
% 211.07/45.96 % Propositional check unsatisfiable : 0
% 211.07/45.96 % Propositional clauses : 0
% 211.07/45.96 % Propositional clauses after purity: 0
% 211.07/45.96 % Propositional unsat core size : 0
% 211.07/45.96 % Propositional preprocessing time : 0.000
% 211.07/45.96 % Propositional encoding time : 0.000
% 211.07/45.96 % Propositional solver time : 0.000
% 211.07/45.96 % Success case prop preproc time : 0.000
% 211.07/45.96 % Success case prop encoding time : 0.000
% 211.07/45.96 % Success case prop solver time : 0.000
% 211.07/45.96 % Current number of processed clauses : 1378
% 211.07/45.96 % Positive orientable unit clauses : 143
% 211.07/45.96 % Positive unorientable unit clauses: 3
% 211.07/45.96 % Negative unit clauses : 188
% 211.07/45.96 % Non-unit-clauses : 1044
% 211.07/45.96 % Current number of unprocessed clauses: 25759
% 211.07/45.96 % ...number of literals in the above : 131065
% 211.07/45.96 % Current number of archived formulas : 0
% 211.07/45.96 % Current number of archived clauses : 2002
% 211.07/45.96 % Clause-clause subsumption calls (NU) : 2102282
% 211.07/45.96 % Rec. Clause-clause subsumption calls : 432427
% 211.07/45.96 % Non-unit clause-clause subsumptions : 1532
% 211.07/45.96 % Unit Clause-clause subsumption calls : 69741
% 211.07/45.96 % Rewrite failures with RHS unbound : 0
% 211.07/45.96 % BW rewrite match attempts : 162
% 211.07/45.96 % BW rewrite match successes : 17
% 211.07/45.96 % Condensation attempts : 0
% 211.07/45.96 % Condensation successes : 0
% 211.07/45.96 % Termbank termtop insertions : 20802648
% 211.07/45.96 % Search garbage collected termcells : 2014707
% 211.07/45.96
% 211.07/45.96 % -------------------------------------------------
% 211.07/45.96 % User time : 40.934 s
% 211.07/45.96 % System time : 2.920 s
% 211.07/45.96 % Total time : 43.854 s
% 211.07/45.96 % Maximum resident set size: 1257912 pages
% 211.07/45.96
% 211.07/45.96 % -------------------------------------------------
% 211.07/45.96 % User time : 40.944 s
% 211.07/45.96 % System time : 3.102 s
% 211.07/45.96 % Total time : 44.045 s
% 211.07/45.96 % Maximum resident set size: 5120 pages
% 211.07/45.96 % E exiting
%------------------------------------------------------------------------------