%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SYO877^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:43:28 AM UTC 2026
% Result : Theorem 66.43s 22.62s
% Output : CNFRefutation 66.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO877^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.06/0.18 % Computer : n020.cluster.edu
% 0.06/0.18 % Model : x86_64 x86_64
% 0.06/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.18 % Memory : 8046.5625MB
% 0.06/0.18 % OS : Linux 6.8.0-71-generic
% 0.06/0.18 % CPULimit : 300
% 0.06/0.18 % WCLimit : 300
% 0.06/0.18 % DateTime : Tue Sep 29 17:24:19 UTC 2026
% 0.06/0.18 % CPUTime :
% 0.06/0.18 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.06/0.23 Running higher-order theorem proving
% 0.06/0.25 Running: /export/starexec/sandbox/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/sandbox/tmp/tmp.NNLXJXy7fT/E---3.1_1351056.p
% 66.43/22.62 % Version: 3.5.1-ho
% 66.43/22.62 % partial match(1): HSLMSMSSSSLCHSA
% 66.43/22.62 % Preprocessing class: HSLMSLSSSSLCHSA.
% 66.43/22.62 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 66.43/22.62 % Starting pre_casc_6 with 1500s (5) cores
% 66.43/22.62 % Starting ehoh_best7 with 300s (1) cores
% 66.43/22.62 % Starting new_bool_8 with 300s (1) cores
% 66.43/22.62 % Starting new_ho_11 with 300s (1) cores
% 66.43/22.62 % new_ho_11 with pid 1351072 completed with status 0
% 66.43/22.62 % Result found by new_ho_11
% 66.43/22.62 % partial match(1): HSLMSMSSSSLCHSA
% 66.43/22.62 % Preprocessing class: HSLMSLSSSSLCHSA.
% 66.43/22.62 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 66.43/22.62 % Starting pre_casc_6 with 1500s (5) cores
% 66.43/22.62 % Starting ehoh_best7 with 300s (1) cores
% 66.43/22.62 % Starting new_bool_8 with 300s (1) cores
% 66.43/22.62 % Starting new_ho_11 with 300s (1) cores
% 66.43/22.62 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 66.43/22.62 % No SInE strategy applied
% 66.43/22.62 % Search class: HGHSM-SMLM33-DHSFFSBC
% 66.43/22.62 % partial match(1): HGHSM-SMLM32-DHSFFSBC
% 66.43/22.62 % Scheduled 7 strats onto 1 cores with 284 seconds (284 total)
% 66.43/22.62 % Starting SubtermCWHack with 26s (1) cores
% 66.43/22.62 % SubtermCWHack with pid 1351089 completed with status 0
% 66.43/22.62 % Result found by SubtermCWHack
% 66.43/22.62 % partial match(1): HSLMSMSSSSLCHSA
% 66.43/22.62 % Preprocessing class: HSLMSLSSSSLCHSA.
% 66.43/22.62 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 66.43/22.62 % Starting pre_casc_6 with 1500s (5) cores
% 66.43/22.62 % Starting ehoh_best7 with 300s (1) cores
% 66.43/22.62 % Starting new_bool_8 with 300s (1) cores
% 66.43/22.62 % Starting new_ho_11 with 300s (1) cores
% 66.43/22.62 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 66.43/22.62 % No SInE strategy applied
% 66.43/22.62 % Search class: HGHSM-SMLM33-DHSFFSBC
% 66.43/22.62 % partial match(1): HGHSM-SMLM32-DHSFFSBC
% 66.43/22.62 % Scheduled 7 strats onto 1 cores with 284 seconds (284 total)
% 66.43/22.62 % Starting SubtermCWHack with 26s (1) cores
% 66.43/22.62 % Preprocessing time : 0.066 s
% 66.43/22.62
% 66.43/22.62 % Proof found!
% 66.43/22.62 % SZS status Theorem
% 66.43/22.62 % SZS output start CNFRefutation
% 66.43/22.62 thf(decl_23, type, c_Eps_i: ($i > $o) > $i).
% 66.43/22.62 thf(decl_24, type, c_False: $o).
% 66.43/22.62 thf(decl_26, type, c_not: $o > $o).
% 66.43/22.62 thf(decl_27, type, c_and: $o > $o > $o).
% 66.43/22.62 thf(decl_30, type, c_In: $i > $i > $o).
% 66.43/22.62 thf(decl_32, type, c_Empty: $i).
% 66.43/22.62 thf(decl_74, type, c_inj: $i > $i > ($i > $i) > $o).
% 66.43/22.62 thf(decl_76, type, c_atleastp: $i > $i > $o).
% 66.43/22.62 thf(decl_177, type, epred51_3: ($i > $i) > $i > $i > $o).
% 66.43/22.62 thf(decl_269, type, epred143_0: $o).
% 66.43/22.62 thf(decl_270, type, esk1_0: $i).
% 66.43/22.62 thf(decl_281, type, esk12_1: ($i > $o) > $i).
% 66.43/22.62 thf(decl_282, type, epred144_0: $o).
% 66.43/22.62 thf(decl_283, type, epred145_2: $o > $o > $o).
% 66.43/22.62 thf(decl_299, type, esk27_2: $i > $i > $i > $i).
% 66.43/22.62 thf(decl_350, type, esk74_3: $i > $i > ($i > $i) > $i).
% 66.43/22.62 thf(decl_351, type, esk75_3: $i > $i > ($i > $i) > $i).
% 66.43/22.62 thf(decl_352, type, esk76_3: $i > $i > ($i > $i) > $i).
% 66.43/22.62 thf(decl_353, type, esk77_3: $i > $i > ($i > $i) > $i).
% 66.43/22.62 thf(decl_354, type, esk78_3: $i > $i > ($i > $i) > $i).
% 66.43/22.62 thf(decl_355, type, esk79_3: $i > $i > ($i > $i) > $i).
% 66.43/22.62 thf(decl_356, type, esk80_3: $i > $i > ($i > $i) > $i).
% 66.43/22.62 thf(decl_357, type, esk81_3: $i > $i > ($i > $i) > $i).
% 66.43/22.62 thf(decl_358, type, esk82_3: $i > $i > ($i > $i) > $i).
% 66.43/22.62 thf(decl_359, type, esk83_3: $i > $i > ($i > $i) > $i).
% 66.43/22.62 thf(decl_485, type, esk207_0: $i > $i > $i).
% 66.43/22.62 thf(decl_486, type, epred153_0: $i > $o).
% 66.43/22.62 thf(decl_487, type, esk208_0: $i > $i).
% 66.43/22.62 thf(decl_488, type, esk209_0: $i).
% 66.43/22.62 thf(decl_489, type, esk210_0: $i).
% 66.43/22.62 thf(decl_490, type, esk211_0: $i).
% 66.43/22.62 thf(decl_507, type, esk222_1: $i > $i > $i).
% 66.43/22.62 thf(decl_515, type, epred163_1: ($i > $o) > $i > $o).
% 66.43/22.62 thf(ax13, axiom, ((c_not)=(^[X17:$o]:((((X17))=>((c_False)))))), file('/export/starexec/sandbox/tmp/tmp.NNLXJXy7fT/E---3.1_1351056.p', ax13)).
% 66.43/22.62 thf(ax14, axiom, ((c_and)=(^[X18:$o, X19:$o]:(![X20:$o]:((((((X18))=>((((X19))=>((X20))))))=>((X20))))))), file('/export/starexec/sandbox/tmp/tmp.NNLXJXy7fT/E---3.1_1351056.p', ax14)).
% 66.43/22.62 thf(ax5, axiom, (c_not @ (?[X7:$i]:((c_In @ X7 @ c_Empty)))), file('/export/starexec/sandbox/tmp/tmp.NNLXJXy7fT/E---3.1_1351056.p', ax5)).
% 66.43/22.62 thf(ax11, axiom, ((c_False)<=>![X15:$o]:((X15))), file('/export/starexec/sandbox/tmp/tmp.NNLXJXy7fT/E---3.1_1351056.p', ax11)).
% 66.43/22.62 thf(ax10, axiom, ![X1:$i > $o]:((![X2:$i]:((![X9:$i]:(((c_In @ X9 @ X2)=>(X1 @ X9)))=>(X1 @ X2)))=>![X2:$i]:((X1 @ X2)))), file('/export/starexec/sandbox/tmp/tmp.NNLXJXy7fT/E---3.1_1351056.p', ax10)).
% 66.43/22.62 thf(ax58, axiom, ((c_atleastp)=(^[X76:$i, X2:$i]:(?[X77:$i > $i]:((c_inj @ X76 @ X2 @ X77))))), file('/export/starexec/sandbox/tmp/tmp.NNLXJXy7fT/E---3.1_1351056.p', ax58)).
% 66.43/22.62 thf(ax56, axiom, ((c_inj)=(^[X72:$i, X2:$i, X73:$i > $i]:((c_and @ (![X13:$i]:((((c_In @ X13 @ X72))=>((c_In @ (X73 @ X13) @ X2))))) @ (![X13:$i]:((((c_In @ X13 @ X72))=>(![X66:$i]:((((c_In @ X66 @ X72))=>(((((X73 @ X13)=(X73 @ X66)))=>(((X13)=(X66))))))))))))))), file('/export/starexec/sandbox/tmp/tmp.NNLXJXy7fT/E---3.1_1351056.p', ax56)).
% 66.43/22.62 thf(ax1, axiom, ![X1:$i > $o, X2:$i]:(((X1 @ X2)=>(X1 @ (c_Eps_i @ X1)))), file('/export/starexec/sandbox/tmp/tmp.NNLXJXy7fT/E---3.1_1351056.p', ax1)).
% 66.43/22.62 thf(conj, conjecture, (c_not @ (![X201:$i > $i > $o, X202:$i > $i > $i, X203:$i > $o, X204:$i > $o, X205:$i > $i, X206:$i, X83:$i, X207:$i]:((c_and @ (((X83)=(X202 @ (X202 @ X206 @ (X202 @ X207 @ (X202 @ (X202 @ (X202 @ (X202 @ X83 @ (X202 @ (X202 @ X206 @ (X202 @ X206 @ (X202 @ (X202 @ X206 @ (X202 @ (X205 @ X206) @ (X202 @ (X202 @ X207 @ (X202 @ X83 @ (X202 @ X83 @ X83))) @ X206))) @ (X202 @ (X205 @ (X202 @ (X202 @ (X205 @ X207) @ X206) @ (X202 @ X206 @ X206))) @ (X202 @ X83 @ (X202 @ X83 @ (X202 @ (X202 @ (X202 @ X206 @ (X202 @ (X202 @ X206 @ (X202 @ (X205 @ X83) @ X207)) @ (X205 @ (X202 @ X207 @ X206)))) @ X83) @ (X205 @ (X202 @ (X202 @ X207 @ (X202 @ X206 @ (X202 @ (X205 @ (X202 @ X206 @ X207)) @ X206))) @ (X202 @ (X202 @ (X202 @ X83 @ (X202 @ (X205 @ X206) @ X83)) @ X83) @ (X205 @ (X205 @ (X202 @ (X202 @ (X202 @ (X202 @ X206 @ (X202 @ (X202 @ X83 @ (X202 @ (X202 @ X207 @ X206) @ X207)) @ X83)) @ X207) @ (X202 @ X207 @ (X202 @ X206 @ X206))) @ X83))))))))))))) @ (X202 @ (X202 @ (X202 @ (X202 @ (X202 @ X83 @ (X202 @ X206 @ X206)) @ (X205 @ (X205 @ (X202 @ X207 @ (X205 @ (X205 @ (X202 @ X207 @ X206))))))) @ X206) @ X83) @ (X202 @ X83 @ X207)))) @ X206) @ X206) @ (X205 @ X83)))) @ (X202 @ (X202 @ (X205 @ (X202 @ (X205 @ (X202 @ (X202 @ (X202 @ (X202 @ X207 @ (X202 @ (X205 @ (X205 @ (X202 @ (X202 @ X206 @ X83) @ X207))) @ (X205 @ (X202 @ X206 @ X206)))) @ X206) @ (X205 @ X206)) @ (X202 @ (X202 @ (X202 @ (X202 @ (X202 @ X206 @ X207) @ (X205 @ (X205 @ (X205 @ X207)))) @ X207) @ X83) @ X206))) @ (X202 @ (X202 @ (X202 @ X83 @ X206) @ (X205 @ X83)) @ X83))) @ X207) @ X83)))) @ (?[X208:$i]:((X204 @ (X205 @ X206)))))))), file('/export/starexec/sandbox/tmp/tmp.NNLXJXy7fT/E---3.1_1351056.p', conj)).
% 66.43/22.62 thf(c_0_9, plain, ![X238:$o]:(((c_not @ ((X238)))<=>((X238)=>(c_False)))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[ax13])])).
% 66.43/22.62 thf(c_0_10, plain, ![X239:$o, X240:$o]:(((c_and @ ((X239)) @ ((X240)))<=>![X20:$o]:((((X239)=>((X240)=>(X20)))=>(X20))))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[ax14])])).
% 66.43/22.62 thf(c_0_11, plain, ![X2025:$i, X2026:$i > $o]:((((~(X2026 @ X2025)|(c_not @ $true)|~(epred163_1 @ X2026 @ X2025))&((X2026 @ X2025)|(c_not @ $false)|~(epred163_1 @ X2026 @ X2025)))&(((~(X2026 @ X2025)|(X2026 @ X2025)|(epred163_1 @ X2026 @ X2025))&(~(c_not @ $false)|(X2026 @ X2025)|(epred163_1 @ X2026 @ X2025)))&((~(X2026 @ X2025)|~(c_not @ $true)|(epred163_1 @ X2026 @ X2025))&(~(c_not @ $false)|~(c_not @ $true)|(epred163_1 @ X2026 @ X2025)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fool_unroll,[status(thm)],[])])])])])).
% 66.43/22.62 thf(c_0_12, plain, ![X486:$o]:(((~(c_not @ ((X486)))|(~(X486)|(c_False)))&(((X486)|(c_not @ ((X486))))&(~(c_False)|(c_not @ ((X486))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_9])])])])).
% 66.43/22.62 thf(c_0_13, plain, ![X301:$i, X302:$i, X303:$i > $i]:(((epred51_3 @ X303 @ X302 @ X301)<=>((~(![X13:$i]:(((c_In @ X13 @ X301)=>(c_In @ (X303 @ X13) @ X302))))|((~(![X13:$i]:(((c_In @ X13 @ X301)=>![X66:$i]:(((c_In @ X66 @ X301)=>(((X303 @ X13)=(X303 @ X66))=>((X13)=(X66))))))))|(c_and @ $true @ $true))&(![X13:$i]:(((c_In @ X13 @ X301)=>![X66:$i]:(((c_In @ X66 @ X301)=>(((X303 @ X13)=(X303 @ X66))=>((X13)=(X66)))))))|(c_and @ $true @ $false))))&(![X13:$i]:(((c_In @ X13 @ X301)=>(c_In @ (X303 @ X13) @ X302)))|((~(![X13:$i]:(((c_In @ X13 @ X301)=>![X66:$i]:(((c_In @ X66 @ X301)=>(((X303 @ X13)=(X303 @ X66))=>((X13)=(X66))))))))|(c_and @ $false @ $true))&(![X13:$i]:(((c_In @ X13 @ X301)=>![X66:$i]:(((c_In @ X66 @ X301)=>(((X303 @ X13)=(X303 @ X66))=>((X13)=(X66)))))))|(c_and @ $false @ $false))))))), introduced(definition)).
% 66.43/22.62 thf(c_0_14, 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])).
% 66.43/22.62 thf(c_0_15, plain, ![X484:$o]:(((~(c_False)|(X484))&(~(epred144_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])])])])])).
% 66.43/22.62 thf(c_0_16, plain, ![X487:$o, X488:$o, X489:$o, X490:$o, X491:$o]:(((((X487)|(X489)|~(c_and @ ((X487)) @ ((X488))))&(((X488)|(X489)|~(c_and @ ((X487)) @ ((X488))))&(~(X489)|(X489)|~(c_and @ ((X487)) @ ((X488))))))&((~(X490)|(~(X491)|(epred145_2 @ X490 @ X491))|(c_and @ ((X490)) @ ((X491))))&(~(epred145_2 @ X490 @ X491)|(c_and @ ((X490)) @ ((X491))))))), 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_10])])])])])])])).
% 66.43/22.62 thf(c_0_17, plain, ![X480:$i > $o, X482:$i, X483:$i]:(((~(c_In @ X482 @ (esk12_1 @ X480))|(X480 @ X482)|(X480 @ X483))&(~(X480 @ (esk12_1 @ X480))|(X480 @ X483)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax10])])])])])])).
% 66.43/22.62 thf(c_0_18, plain, ![X1:$i > $o, X2:$i]:(((X1 @ X2)|(epred163_1 @ X1 @ X2)|~((c_not @ (~($true)))))), inference(split_conjunct,[status(thm)],[c_0_11])).
% 66.43/22.62 thf(c_0_19, plain, (c_not @ (~($true))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_12])])])).
% 66.43/22.62 thf(c_0_20, plain, ![X307:$i, X308:$i]:(((c_atleastp @ X307 @ X308)<=>?[X77:$i > $i]:((c_inj @ X307 @ X308 @ X77)))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[ax58])])).
% 66.43/22.62 thf(c_0_21, plain, ![X301:$i, X302:$i, X303:$i > $i]:(((c_inj @ X301 @ X302 @ X303)<=>(epred51_3 @ X303 @ X302 @ X301))), inference(apply_def,[status(thm)],[inference(fool_unroll,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[ax56])])]), c_0_13])).
% 66.43/22.62 thf(c_0_22, plain, ![X453:$i]:(((~(c_In @ X453 @ 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_14])])])])])).
% 66.43/22.62 thf(c_0_23, plain, ((c_False)|~((c_not @ (($true))))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_12])])])).
% 66.43/22.62 thf(c_0_24, plain, ~((c_False)), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_15])])])).
% 66.43/22.62 thf(c_0_25, plain, ![X959:$i, X960:$i, X961:$i > $i, X965:$i, X966:$i, X967:$i, X970:$i, X971:$i, X972:$i, X973:$i, X974:$i > $i, X975:$i, X976:$i, X977:$i, X981:$i, X982:$i]:((((((((c_In @ (esk75_3 @ X959 @ X960 @ X961) @ X959)|(c_and @ $true @ $true)|(c_In @ (esk74_3 @ X959 @ X960 @ X961) @ X959)|~(epred51_3 @ X961 @ X960 @ X959))&(((c_In @ (esk76_3 @ X959 @ X960 @ X961) @ X959)|(c_and @ $true @ $true)|(c_In @ (esk74_3 @ X959 @ X960 @ X961) @ X959)|~(epred51_3 @ X961 @ X960 @ X959))&((((X961 @ (esk75_3 @ X959 @ X960 @ X961))=(X961 @ (esk76_3 @ X959 @ X960 @ X961)))|(c_and @ $true @ $true)|(c_In @ (esk74_3 @ X959 @ X960 @ X961) @ X959)|~(epred51_3 @ X961 @ X960 @ X959))&(((esk75_3 @ X959 @ X960 @ X961)!=(esk76_3 @ X959 @ X960 @ X961))|(c_and @ $true @ $true)|(c_In @ (esk74_3 @ X959 @ X960 @ X961) @ X959)|~(epred51_3 @ X961 @ X960 @ X959)))))&(~(c_In @ X965 @ X959)|(~(c_In @ X966 @ X959)|(((X961 @ X965)!=(X961 @ X966))|((X965)=(X966))))|(c_and @ $true @ $false)|(c_In @ (esk74_3 @ X959 @ X960 @ X961) @ X959)|~(epred51_3 @ X961 @ X960 @ X959)))&((((c_In @ (esk75_3 @ X959 @ X960 @ X961) @ X959)|(c_and @ $true @ $true)|~(c_In @ (X961 @ (esk74_3 @ X959 @ X960 @ X961)) @ X960)|~(epred51_3 @ X961 @ X960 @ X959))&(((c_In @ (esk76_3 @ X959 @ X960 @ X961) @ X959)|(c_and @ $true @ $true)|~(c_In @ (X961 @ (esk74_3 @ X959 @ X960 @ X961)) @ X960)|~(epred51_3 @ X961 @ X960 @ X959))&((((X961 @ (esk75_3 @ X959 @ X960 @ X961))=(X961 @ (esk76_3 @ X959 @ X960 @ X961)))|(c_and @ $true @ $true)|~(c_In @ (X961 @ (esk74_3 @ X959 @ X960 @ X961)) @ X960)|~(epred51_3 @ X961 @ X960 @ X959))&(((esk75_3 @ X959 @ X960 @ X961)!=(esk76_3 @ X959 @ X960 @ X961))|(c_and @ $true @ $true)|~(c_In @ (X961 @ (esk74_3 @ X959 @ X960 @ X961)) @ X960)|~(epred51_3 @ X961 @ X960 @ X959)))))&(~(c_In @ X965 @ X959)|(~(c_In @ X966 @ X959)|(((X961 @ X965)!=(X961 @ X966))|((X965)=(X966))))|(c_and @ $true @ $false)|~(c_In @ (X961 @ (esk74_3 @ X959 @ X960 @ X961)) @ X960)|~(epred51_3 @ X961 @ X960 @ X959))))&((((c_In @ (esk77_3 @ X959 @ X960 @ X961) @ X959)|(c_and @ $false @ $true)|(~(c_In @ X967 @ X959)|(c_In @ (X961 @ X967) @ X960))|~(epred51_3 @ X961 @ X960 @ X959))&(((c_In @ (esk78_3 @ X959 @ X960 @ X961) @ X959)|(c_and @ $false @ $true)|(~(c_In @ X967 @ X959)|(c_In @ (X961 @ X967) @ X960))|~(epred51_3 @ X961 @ X960 @ X959))&((((X961 @ (esk77_3 @ X959 @ X960 @ X961))=(X961 @ (esk78_3 @ X959 @ X960 @ X961)))|(c_and @ $false @ $true)|(~(c_In @ X967 @ X959)|(c_In @ (X961 @ X967) @ X960))|~(epred51_3 @ X961 @ X960 @ X959))&(((esk77_3 @ X959 @ X960 @ X961)!=(esk78_3 @ X959 @ X960 @ X961))|(c_and @ $false @ $true)|(~(c_In @ X967 @ X959)|(c_In @ (X961 @ X967) @ X960))|~(epred51_3 @ X961 @ X960 @ X959)))))&(~(c_In @ X970 @ X959)|(~(c_In @ X971 @ X959)|(((X961 @ X970)!=(X961 @ X971))|((X970)=(X971))))|(c_and @ $false @ $false)|(~(c_In @ X967 @ X959)|(c_In @ (X961 @ X967) @ X960))|~(epred51_3 @ X961 @ X960 @ X959))))&(((((c_In @ (esk81_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X975 @ X972)|(c_In @ (X974 @ X975) @ X973))|(epred51_3 @ X974 @ X973 @ X972))&(~(c_In @ (X974 @ (esk81_3 @ X972 @ X973 @ X974)) @ X973)|(~(c_In @ X975 @ X972)|(c_In @ (X974 @ X975) @ X973))|(epred51_3 @ X974 @ X973 @ X972)))&(((((c_In @ (esk82_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(~(c_In @ X975 @ X972)|(c_In @ (X974 @ X975) @ X973))|(epred51_3 @ X974 @ X973 @ X972))&(((c_In @ (esk83_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(~(c_In @ X975 @ X972)|(c_In @ (X974 @ X975) @ X973))|(epred51_3 @ X974 @ X973 @ X972))&((((X974 @ (esk82_3 @ X972 @ X973 @ X974))=(X974 @ (esk83_3 @ X972 @ X973 @ X974)))|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(~(c_In @ X975 @ X972)|(c_In @ (X974 @ X975) @ X973))|(epred51_3 @ X974 @ X973 @ X972))&(((esk82_3 @ X972 @ X973 @ X974)!=(esk83_3 @ X972 @ X973 @ X974))|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(~(c_In @ X975 @ X972)|(c_In @ (X974 @ X975) @ X973))|(epred51_3 @ X974 @ X973 @ X972)))))&(~(c_and @ $false @ $false)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(~(c_In @ X975 @ X972)|(c_In @ (X974 @ X975) @ X973))|(epred51_3 @ X974 @ X973 @ X972)))&((((c_In @ (esk82_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $false @ $true)|(~(c_In @ X975 @ X972)|(c_In @ (X974 @ X975) @ X973))|(epred51_3 @ X974 @ X973 @ X972))&(((c_In @ (esk83_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $false @ $true)|(~(c_In @ X975 @ X972)|(c_In @ (X974 @ X975) @ X973))|(epred51_3 @ X974 @ X973 @ X972))&((((X974 @ (esk82_3 @ X972 @ X973 @ X974))=(X974 @ (esk83_3 @ X972 @ X973 @ X974)))|~(c_and @ $false @ $true)|(~(c_In @ X975 @ X972)|(c_In @ (X974 @ X975) @ X973))|(epred51_3 @ X974 @ X973 @ X972))&(((esk82_3 @ X972 @ X973 @ X974)!=(esk83_3 @ X972 @ X973 @ X974))|~(c_and @ $false @ $true)|(~(c_In @ X975 @ X972)|(c_In @ (X974 @ X975) @ X973))|(epred51_3 @ X974 @ X973 @ X972)))))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|(~(c_In @ X975 @ X972)|(c_In @ (X974 @ X975) @ X973))|(epred51_3 @ X974 @ X973 @ X972)))))&(((((((c_In @ (esk81_3 @ X972 @ X973 @ X974) @ X972)|((c_In @ (esk79_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&(~(c_In @ (X974 @ (esk81_3 @ X972 @ X973 @ X974)) @ X973)|((c_In @ (esk79_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972)))&(((((c_In @ (esk82_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|((c_In @ (esk79_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&(((c_In @ (esk83_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|((c_In @ (esk79_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&((((X974 @ (esk82_3 @ X972 @ X973 @ X974))=(X974 @ (esk83_3 @ X972 @ X973 @ X974)))|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|((c_In @ (esk79_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&(((esk82_3 @ X972 @ X973 @ X974)!=(esk83_3 @ X972 @ X973 @ X974))|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|((c_In @ (esk79_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972)))))&(~(c_and @ $false @ $false)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|((c_In @ (esk79_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972)))&((((c_In @ (esk82_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $false @ $true)|((c_In @ (esk79_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&(((c_In @ (esk83_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $false @ $true)|((c_In @ (esk79_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&((((X974 @ (esk82_3 @ X972 @ X973 @ X974))=(X974 @ (esk83_3 @ X972 @ X973 @ X974)))|~(c_and @ $false @ $true)|((c_In @ (esk79_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&(((esk82_3 @ X972 @ X973 @ X974)!=(esk83_3 @ X972 @ X973 @ X974))|~(c_and @ $false @ $true)|((c_In @ (esk79_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972)))))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|((c_In @ (esk79_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972)))))&(((((c_In @ (esk81_3 @ X972 @ X973 @ X974) @ X972)|((c_In @ (esk80_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&(~(c_In @ (X974 @ (esk81_3 @ X972 @ X973 @ X974)) @ X973)|((c_In @ (esk80_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972)))&(((((c_In @ (esk82_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|((c_In @ (esk80_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&(((c_In @ (esk83_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|((c_In @ (esk80_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&((((X974 @ (esk82_3 @ X972 @ X973 @ X974))=(X974 @ (esk83_3 @ X972 @ X973 @ X974)))|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|((c_In @ (esk80_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&(((esk82_3 @ X972 @ X973 @ X974)!=(esk83_3 @ X972 @ X973 @ X974))|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|((c_In @ (esk80_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972)))))&(~(c_and @ $false @ $false)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|((c_In @ (esk80_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972)))&((((c_In @ (esk82_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $false @ $true)|((c_In @ (esk80_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&(((c_In @ (esk83_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $false @ $true)|((c_In @ (esk80_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&((((X974 @ (esk82_3 @ X972 @ X973 @ X974))=(X974 @ (esk83_3 @ X972 @ X973 @ X974)))|~(c_and @ $false @ $true)|((c_In @ (esk80_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&(((esk82_3 @ X972 @ X973 @ X974)!=(esk83_3 @ X972 @ X973 @ X974))|~(c_and @ $false @ $true)|((c_In @ (esk80_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972)))))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|((c_In @ (esk80_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972)))))&(((((c_In @ (esk81_3 @ X972 @ X973 @ X974) @ X972)|(((X974 @ (esk79_3 @ X972 @ X973 @ X974))=(X974 @ (esk80_3 @ X972 @ X973 @ X974)))|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&(~(c_In @ (X974 @ (esk81_3 @ X972 @ X973 @ X974)) @ X973)|(((X974 @ (esk79_3 @ X972 @ X973 @ X974))=(X974 @ (esk80_3 @ X972 @ X973 @ X974)))|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972)))&(((((c_In @ (esk82_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(((X974 @ (esk79_3 @ X972 @ X973 @ X974))=(X974 @ (esk80_3 @ X972 @ X973 @ X974)))|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&(((c_In @ (esk83_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(((X974 @ (esk79_3 @ X972 @ X973 @ X974))=(X974 @ (esk80_3 @ X972 @ X973 @ X974)))|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&((((X974 @ (esk82_3 @ X972 @ X973 @ X974))=(X974 @ (esk83_3 @ X972 @ X973 @ X974)))|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(((X974 @ (esk79_3 @ X972 @ X973 @ X974))=(X974 @ (esk80_3 @ X972 @ X973 @ X974)))|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&(((esk82_3 @ X972 @ X973 @ X974)!=(esk83_3 @ X972 @ X973 @ X974))|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(((X974 @ (esk79_3 @ X972 @ X973 @ X974))=(X974 @ (esk80_3 @ X972 @ X973 @ X974)))|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972)))))&(~(c_and @ $false @ $false)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(((X974 @ (esk79_3 @ X972 @ X973 @ X974))=(X974 @ (esk80_3 @ X972 @ X973 @ X974)))|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972)))&((((c_In @ (esk82_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $false @ $true)|(((X974 @ (esk79_3 @ X972 @ X973 @ X974))=(X974 @ (esk80_3 @ X972 @ X973 @ X974)))|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&(((c_In @ (esk83_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $false @ $true)|(((X974 @ (esk79_3 @ X972 @ X973 @ X974))=(X974 @ (esk80_3 @ X972 @ X973 @ X974)))|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&((((X974 @ (esk82_3 @ X972 @ X973 @ X974))=(X974 @ (esk83_3 @ X972 @ X973 @ X974)))|~(c_and @ $false @ $true)|(((X974 @ (esk79_3 @ X972 @ X973 @ X974))=(X974 @ (esk80_3 @ X972 @ X973 @ X974)))|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&(((esk82_3 @ X972 @ X973 @ X974)!=(esk83_3 @ X972 @ X973 @ X974))|~(c_and @ $false @ $true)|(((X974 @ (esk79_3 @ X972 @ X973 @ X974))=(X974 @ (esk80_3 @ X972 @ X973 @ X974)))|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972)))))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|(((X974 @ (esk79_3 @ X972 @ X973 @ X974))=(X974 @ (esk80_3 @ X972 @ X973 @ X974)))|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972)))))&((((c_In @ (esk81_3 @ X972 @ X973 @ X974) @ X972)|(((esk79_3 @ X972 @ X973 @ X974)!=(esk80_3 @ X972 @ X973 @ X974))|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&(~(c_In @ (X974 @ (esk81_3 @ X972 @ X973 @ X974)) @ X973)|(((esk79_3 @ X972 @ X973 @ X974)!=(esk80_3 @ X972 @ X973 @ X974))|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972)))&(((((c_In @ (esk82_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(((esk79_3 @ X972 @ X973 @ X974)!=(esk80_3 @ X972 @ X973 @ X974))|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&(((c_In @ (esk83_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(((esk79_3 @ X972 @ X973 @ X974)!=(esk80_3 @ X972 @ X973 @ X974))|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&((((X974 @ (esk82_3 @ X972 @ X973 @ X974))=(X974 @ (esk83_3 @ X972 @ X973 @ X974)))|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(((esk79_3 @ X972 @ X973 @ X974)!=(esk80_3 @ X972 @ X973 @ X974))|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&(((esk82_3 @ X972 @ X973 @ X974)!=(esk83_3 @ X972 @ X973 @ X974))|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(((esk79_3 @ X972 @ X973 @ X974)!=(esk80_3 @ X972 @ X973 @ X974))|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972)))))&(~(c_and @ $false @ $false)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(((esk79_3 @ X972 @ X973 @ X974)!=(esk80_3 @ X972 @ X973 @ X974))|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972)))&((((c_In @ (esk82_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $false @ $true)|(((esk79_3 @ X972 @ X973 @ X974)!=(esk80_3 @ X972 @ X973 @ X974))|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&(((c_In @ (esk83_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $false @ $true)|(((esk79_3 @ X972 @ X973 @ X974)!=(esk80_3 @ X972 @ X973 @ X974))|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&((((X974 @ (esk82_3 @ X972 @ X973 @ X974))=(X974 @ (esk83_3 @ X972 @ X973 @ X974)))|~(c_and @ $false @ $true)|(((esk79_3 @ X972 @ X973 @ X974)!=(esk80_3 @ X972 @ X973 @ X974))|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&(((esk82_3 @ X972 @ X973 @ X974)!=(esk83_3 @ X972 @ X973 @ X974))|~(c_and @ $false @ $true)|(((esk79_3 @ X972 @ X973 @ X974)!=(esk80_3 @ X972 @ X973 @ X974))|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972)))))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|(((esk79_3 @ X972 @ X973 @ X974)!=(esk80_3 @ X972 @ X973 @ X974))|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))))))))&((((c_In @ (esk81_3 @ X972 @ X973 @ X974) @ X972)|(~(c_and @ $true @ $false)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&(~(c_In @ (X974 @ (esk81_3 @ X972 @ X973 @ X974)) @ X973)|(~(c_and @ $true @ $false)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972)))&(((((c_In @ (esk82_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(~(c_and @ $true @ $false)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&(((c_In @ (esk83_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(~(c_and @ $true @ $false)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&((((X974 @ (esk82_3 @ X972 @ X973 @ X974))=(X974 @ (esk83_3 @ X972 @ X973 @ X974)))|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(~(c_and @ $true @ $false)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&(((esk82_3 @ X972 @ X973 @ X974)!=(esk83_3 @ X972 @ X973 @ X974))|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(~(c_and @ $true @ $false)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972)))))&(~(c_and @ $false @ $false)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(~(c_and @ $true @ $false)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972)))&((((c_In @ (esk82_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $false @ $true)|(~(c_and @ $true @ $false)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&(((c_In @ (esk83_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $false @ $true)|(~(c_and @ $true @ $false)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&((((X974 @ (esk82_3 @ X972 @ X973 @ X974))=(X974 @ (esk83_3 @ X972 @ X973 @ X974)))|~(c_and @ $false @ $true)|(~(c_and @ $true @ $false)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))&(((esk82_3 @ X972 @ X973 @ X974)!=(esk83_3 @ X972 @ X973 @ X974))|~(c_and @ $false @ $true)|(~(c_and @ $true @ $false)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972)))))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|(~(c_and @ $true @ $false)|(~(c_In @ X976 @ X972)|(~(c_In @ X977 @ X972)|(((X974 @ X976)!=(X974 @ X977))|((X976)=(X977))))))|(epred51_3 @ X974 @ X973 @ X972))))))&((((((c_In @ (esk81_3 @ X972 @ X973 @ X974) @ X972)|((c_In @ (esk79_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&(~(c_In @ (X974 @ (esk81_3 @ X972 @ X973 @ X974)) @ X973)|((c_In @ (esk79_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972)))&(((((c_In @ (esk82_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|((c_In @ (esk79_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&(((c_In @ (esk83_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|((c_In @ (esk79_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&((((X974 @ (esk82_3 @ X972 @ X973 @ X974))=(X974 @ (esk83_3 @ X972 @ X973 @ X974)))|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|((c_In @ (esk79_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&(((esk82_3 @ X972 @ X973 @ X974)!=(esk83_3 @ X972 @ X973 @ X974))|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|((c_In @ (esk79_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972)))))&(~(c_and @ $false @ $false)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|((c_In @ (esk79_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972)))&((((c_In @ (esk82_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $false @ $true)|((c_In @ (esk79_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&(((c_In @ (esk83_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $false @ $true)|((c_In @ (esk79_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&((((X974 @ (esk82_3 @ X972 @ X973 @ X974))=(X974 @ (esk83_3 @ X972 @ X973 @ X974)))|~(c_and @ $false @ $true)|((c_In @ (esk79_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&(((esk82_3 @ X972 @ X973 @ X974)!=(esk83_3 @ X972 @ X973 @ X974))|~(c_and @ $false @ $true)|((c_In @ (esk79_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972)))))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|((c_In @ (esk79_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972)))))&(((((c_In @ (esk81_3 @ X972 @ X973 @ X974) @ X972)|((c_In @ (esk80_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&(~(c_In @ (X974 @ (esk81_3 @ X972 @ X973 @ X974)) @ X973)|((c_In @ (esk80_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972)))&(((((c_In @ (esk82_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|((c_In @ (esk80_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&(((c_In @ (esk83_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|((c_In @ (esk80_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&((((X974 @ (esk82_3 @ X972 @ X973 @ X974))=(X974 @ (esk83_3 @ X972 @ X973 @ X974)))|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|((c_In @ (esk80_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&(((esk82_3 @ X972 @ X973 @ X974)!=(esk83_3 @ X972 @ X973 @ X974))|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|((c_In @ (esk80_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972)))))&(~(c_and @ $false @ $false)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|((c_In @ (esk80_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972)))&((((c_In @ (esk82_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $false @ $true)|((c_In @ (esk80_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&(((c_In @ (esk83_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $false @ $true)|((c_In @ (esk80_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&((((X974 @ (esk82_3 @ X972 @ X973 @ X974))=(X974 @ (esk83_3 @ X972 @ X973 @ X974)))|~(c_and @ $false @ $true)|((c_In @ (esk80_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&(((esk82_3 @ X972 @ X973 @ X974)!=(esk83_3 @ X972 @ X973 @ X974))|~(c_and @ $false @ $true)|((c_In @ (esk80_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972)))))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|((c_In @ (esk80_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972)))))&(((((c_In @ (esk81_3 @ X972 @ X973 @ X974) @ X972)|(((X974 @ (esk79_3 @ X972 @ X973 @ X974))=(X974 @ (esk80_3 @ X972 @ X973 @ X974)))|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&(~(c_In @ (X974 @ (esk81_3 @ X972 @ X973 @ X974)) @ X973)|(((X974 @ (esk79_3 @ X972 @ X973 @ X974))=(X974 @ (esk80_3 @ X972 @ X973 @ X974)))|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972)))&(((((c_In @ (esk82_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(((X974 @ (esk79_3 @ X972 @ X973 @ X974))=(X974 @ (esk80_3 @ X972 @ X973 @ X974)))|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&(((c_In @ (esk83_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(((X974 @ (esk79_3 @ X972 @ X973 @ X974))=(X974 @ (esk80_3 @ X972 @ X973 @ X974)))|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&((((X974 @ (esk82_3 @ X972 @ X973 @ X974))=(X974 @ (esk83_3 @ X972 @ X973 @ X974)))|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(((X974 @ (esk79_3 @ X972 @ X973 @ X974))=(X974 @ (esk80_3 @ X972 @ X973 @ X974)))|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&(((esk82_3 @ X972 @ X973 @ X974)!=(esk83_3 @ X972 @ X973 @ X974))|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(((X974 @ (esk79_3 @ X972 @ X973 @ X974))=(X974 @ (esk80_3 @ X972 @ X973 @ X974)))|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972)))))&(~(c_and @ $false @ $false)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(((X974 @ (esk79_3 @ X972 @ X973 @ X974))=(X974 @ (esk80_3 @ X972 @ X973 @ X974)))|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972)))&((((c_In @ (esk82_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $false @ $true)|(((X974 @ (esk79_3 @ X972 @ X973 @ X974))=(X974 @ (esk80_3 @ X972 @ X973 @ X974)))|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&(((c_In @ (esk83_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $false @ $true)|(((X974 @ (esk79_3 @ X972 @ X973 @ X974))=(X974 @ (esk80_3 @ X972 @ X973 @ X974)))|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&((((X974 @ (esk82_3 @ X972 @ X973 @ X974))=(X974 @ (esk83_3 @ X972 @ X973 @ X974)))|~(c_and @ $false @ $true)|(((X974 @ (esk79_3 @ X972 @ X973 @ X974))=(X974 @ (esk80_3 @ X972 @ X973 @ X974)))|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&(((esk82_3 @ X972 @ X973 @ X974)!=(esk83_3 @ X972 @ X973 @ X974))|~(c_and @ $false @ $true)|(((X974 @ (esk79_3 @ X972 @ X973 @ X974))=(X974 @ (esk80_3 @ X972 @ X973 @ X974)))|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972)))))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|(((X974 @ (esk79_3 @ X972 @ X973 @ X974))=(X974 @ (esk80_3 @ X972 @ X973 @ X974)))|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972)))))&((((c_In @ (esk81_3 @ X972 @ X973 @ X974) @ X972)|(((esk79_3 @ X972 @ X973 @ X974)!=(esk80_3 @ X972 @ X973 @ X974))|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&(~(c_In @ (X974 @ (esk81_3 @ X972 @ X973 @ X974)) @ X973)|(((esk79_3 @ X972 @ X973 @ X974)!=(esk80_3 @ X972 @ X973 @ X974))|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972)))&(((((c_In @ (esk82_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(((esk79_3 @ X972 @ X973 @ X974)!=(esk80_3 @ X972 @ X973 @ X974))|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&(((c_In @ (esk83_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(((esk79_3 @ X972 @ X973 @ X974)!=(esk80_3 @ X972 @ X973 @ X974))|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&((((X974 @ (esk82_3 @ X972 @ X973 @ X974))=(X974 @ (esk83_3 @ X972 @ X973 @ X974)))|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(((esk79_3 @ X972 @ X973 @ X974)!=(esk80_3 @ X972 @ X973 @ X974))|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&(((esk82_3 @ X972 @ X973 @ X974)!=(esk83_3 @ X972 @ X973 @ X974))|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(((esk79_3 @ X972 @ X973 @ X974)!=(esk80_3 @ X972 @ X973 @ X974))|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972)))))&(~(c_and @ $false @ $false)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(((esk79_3 @ X972 @ X973 @ X974)!=(esk80_3 @ X972 @ X973 @ X974))|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972)))&((((c_In @ (esk82_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $false @ $true)|(((esk79_3 @ X972 @ X973 @ X974)!=(esk80_3 @ X972 @ X973 @ X974))|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&(((c_In @ (esk83_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $false @ $true)|(((esk79_3 @ X972 @ X973 @ X974)!=(esk80_3 @ X972 @ X973 @ X974))|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&((((X974 @ (esk82_3 @ X972 @ X973 @ X974))=(X974 @ (esk83_3 @ X972 @ X973 @ X974)))|~(c_and @ $false @ $true)|(((esk79_3 @ X972 @ X973 @ X974)!=(esk80_3 @ X972 @ X973 @ X974))|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&(((esk82_3 @ X972 @ X973 @ X974)!=(esk83_3 @ X972 @ X973 @ X974))|~(c_and @ $false @ $true)|(((esk79_3 @ X972 @ X973 @ X974)!=(esk80_3 @ X972 @ X973 @ X974))|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972)))))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|(((esk79_3 @ X972 @ X973 @ X974)!=(esk80_3 @ X972 @ X973 @ X974))|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))))))))&((((c_In @ (esk81_3 @ X972 @ X973 @ X974) @ X972)|(~(c_and @ $true @ $false)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&(~(c_In @ (X974 @ (esk81_3 @ X972 @ X973 @ X974)) @ X973)|(~(c_and @ $true @ $false)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972)))&(((((c_In @ (esk82_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(~(c_and @ $true @ $false)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&(((c_In @ (esk83_3 @ X972 @ X973 @ X974) @ X972)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(~(c_and @ $true @ $false)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&((((X974 @ (esk82_3 @ X972 @ X973 @ X974))=(X974 @ (esk83_3 @ X972 @ X973 @ X974)))|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(~(c_and @ $true @ $false)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&(((esk82_3 @ X972 @ X973 @ X974)!=(esk83_3 @ X972 @ X973 @ X974))|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(~(c_and @ $true @ $false)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972)))))&(~(c_and @ $false @ $false)|(~(c_In @ X981 @ X972)|(~(c_In @ X982 @ X972)|(((X974 @ X981)!=(X974 @ X982))|((X981)=(X982)))))|(~(c_and @ $true @ $false)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972)))&((((c_In @ (esk82_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $false @ $true)|(~(c_and @ $true @ $false)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&(((c_In @ (esk83_3 @ X972 @ X973 @ X974) @ X972)|~(c_and @ $false @ $true)|(~(c_and @ $true @ $false)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&((((X974 @ (esk82_3 @ X972 @ X973 @ X974))=(X974 @ (esk83_3 @ X972 @ X973 @ X974)))|~(c_and @ $false @ $true)|(~(c_and @ $true @ $false)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972))&(((esk82_3 @ X972 @ X973 @ X974)!=(esk83_3 @ X972 @ X973 @ X974))|~(c_and @ $false @ $true)|(~(c_and @ $true @ $false)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972)))))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|(~(c_and @ $true @ $false)|~(c_and @ $true @ $true))|(epred51_3 @ X974 @ X973 @ X972)))))))))), 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_13])])])])])])])).
% 66.43/22.62 thf(c_0_26, plain, ![X3:$o, X4:$o]:(((c_and @ ((X3)) @ ((X4)))|~((epred145_2 @ ((X3)) @ ((X4)))))), inference(split_conjunct,[status(thm)],[c_0_16])).
% 66.43/22.62 thf(c_0_27, plain, ((epred145_2 @ (($true)) @ (($true)))|(c_and @ (($true)) @ (($true)))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_16])])])).
% 66.43/22.62 thf(c_0_28, plain, ![X446:$i > $o, X447:$i]:((~(X446 @ X447)|(X446 @ (c_Eps_i @ X446)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax1])])])).
% 66.43/22.62 thf(c_0_29, plain, ![X2:$i, X1:$i > $o]:(((X1 @ X2)|~((X1 @ (esk12_1 @ X1))))), inference(split_conjunct,[status(thm)],[c_0_17])).
% 66.43/22.62 thf(c_0_30, plain, ![X1:$i > $o, X2:$i]:(((epred163_1 @ X1 @ X2)|(X1 @ X2))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_18, c_0_19])])).
% 66.43/22.62 thf(c_0_31, plain, ![X601:$i, X602:$i, X604:$i, X605:$i, X606:$i > $i]:(((~(c_atleastp @ X601 @ X602)|(c_inj @ X601 @ X602 @ (esk27_2 @ X601 @ X602)))&(~(c_inj @ X604 @ X605 @ X606)|(c_atleastp @ X604 @ X605)))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_20])])])])])])).
% 66.43/22.62 thf(c_0_32, plain, ![X595:$i, X596:$i, X597:$i > $i]:(((~(c_inj @ X595 @ X596 @ X597)|(epred51_3 @ X597 @ X596 @ X595))&(~(epred51_3 @ X597 @ X596 @ X595)|(c_inj @ X595 @ X596 @ X597)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_21])])])).
% 66.43/22.62 thf(c_0_33, plain, ![X2:$i]:(((c_not @ (($true)))|~((c_In @ X2 @ c_Empty)))), inference(split_conjunct,[status(thm)],[c_0_22])).
% 66.43/22.62 thf(c_0_34, plain, ~((c_not @ (($true)))), inference(sr,[status(thm)],[c_0_23, c_0_24])).
% 66.43/22.62 thf(c_0_35, plain, ![X12:$i > $i, X6:$i, X2:$i]:(((c_In @ (esk81_3 @ X2 @ X6 @ X12) @ X2)|(c_In @ (esk79_3 @ X2 @ X6 @ X12) @ X2)|(epred51_3 @ X12 @ X6 @ X2)|~((c_and @ (($true)) @ (($true)))))), inference(split_conjunct,[status(thm)],[c_0_25])).
% 66.43/22.62 thf(c_0_36, plain, (c_and @ (($true)) @ (($true))), inference(spm,[status(thm)],[c_0_26, c_0_27])).
% 66.43/22.62 thf(c_0_37, plain, ((epred143_0)<=>(![X201:$i > $i > $o, X202:$i > $i > $i, X203:$i > $o, X204:$i > $o, X205:$i > $i, X206:$i, X83:$i, X207:$i]:(((((X83)!=(X202 @ (X202 @ X206 @ (X202 @ X207 @ (X202 @ (X202 @ (X202 @ (X202 @ X83 @ (X202 @ (X202 @ X206 @ (X202 @ X206 @ (X202 @ (X202 @ X206 @ (X202 @ (X205 @ X206) @ (X202 @ (X202 @ X207 @ (X202 @ X83 @ (X202 @ X83 @ X83))) @ X206))) @ (X202 @ (X205 @ (X202 @ (X202 @ (X205 @ X207) @ X206) @ (X202 @ X206 @ X206))) @ (X202 @ X83 @ (X202 @ X83 @ (X202 @ (X202 @ (X202 @ X206 @ (X202 @ (X202 @ X206 @ (X202 @ (X205 @ X83) @ X207)) @ (X205 @ (X202 @ X207 @ X206)))) @ X83) @ (X205 @ (X202 @ (X202 @ X207 @ (X202 @ X206 @ (X202 @ (X205 @ (X202 @ X206 @ X207)) @ X206))) @ (X202 @ (X202 @ (X202 @ X83 @ (X202 @ (X205 @ X206) @ X83)) @ X83) @ (X205 @ (X205 @ (X202 @ (X202 @ (X202 @ (X202 @ X206 @ (X202 @ (X202 @ X83 @ (X202 @ (X202 @ X207 @ X206) @ X207)) @ X83)) @ X207) @ (X202 @ X207 @ (X202 @ X206 @ X206))) @ X83))))))))))))) @ (X202 @ (X202 @ (X202 @ (X202 @ (X202 @ X83 @ (X202 @ X206 @ X206)) @ (X205 @ (X205 @ (X202 @ X207 @ (X205 @ (X205 @ (X202 @ X207 @ X206))))))) @ X206) @ X83) @ (X202 @ X83 @ X207)))) @ X206) @ X206) @ (X205 @ X83)))) @ (X202 @ (X202 @ (X205 @ (X202 @ (X205 @ (X202 @ (X202 @ (X202 @ (X202 @ X207 @ (X202 @ (X205 @ (X205 @ (X202 @ (X202 @ X206 @ X83) @ X207))) @ (X205 @ (X202 @ X206 @ X206)))) @ X206) @ (X205 @ X206)) @ (X202 @ (X202 @ (X202 @ (X202 @ (X202 @ X206 @ X207) @ (X205 @ (X205 @ (X205 @ X207)))) @ X207) @ X83) @ X206))) @ (X202 @ (X202 @ (X202 @ X83 @ X206) @ (X205 @ X83)) @ X83))) @ X207) @ X83)))|((~(?[X208:$i]:((X204 @ (X205 @ X206))))|(c_and @ $true @ $true))&(?[X208:$i]:((X204 @ (X205 @ X206)))|(c_and @ $true @ $false))))&(((X83)=(X202 @ (X202 @ X206 @ (X202 @ X207 @ (X202 @ (X202 @ (X202 @ (X202 @ X83 @ (X202 @ (X202 @ X206 @ (X202 @ X206 @ (X202 @ (X202 @ X206 @ (X202 @ (X205 @ X206) @ (X202 @ (X202 @ X207 @ (X202 @ X83 @ (X202 @ X83 @ X83))) @ X206))) @ (X202 @ (X205 @ (X202 @ (X202 @ (X205 @ X207) @ X206) @ (X202 @ X206 @ X206))) @ (X202 @ X83 @ (X202 @ X83 @ (X202 @ (X202 @ (X202 @ X206 @ (X202 @ (X202 @ X206 @ (X202 @ (X205 @ X83) @ X207)) @ (X205 @ (X202 @ X207 @ X206)))) @ X83) @ (X205 @ (X202 @ (X202 @ X207 @ (X202 @ X206 @ (X202 @ (X205 @ (X202 @ X206 @ X207)) @ X206))) @ (X202 @ (X202 @ (X202 @ X83 @ (X202 @ (X205 @ X206) @ X83)) @ X83) @ (X205 @ (X205 @ (X202 @ (X202 @ (X202 @ (X202 @ X206 @ (X202 @ (X202 @ X83 @ (X202 @ (X202 @ X207 @ X206) @ X207)) @ X83)) @ X207) @ (X202 @ X207 @ (X202 @ X206 @ X206))) @ X83))))))))))))) @ (X202 @ (X202 @ (X202 @ (X202 @ (X202 @ X83 @ (X202 @ X206 @ X206)) @ (X205 @ (X205 @ (X202 @ X207 @ (X205 @ (X205 @ (X202 @ X207 @ X206))))))) @ X206) @ X83) @ (X202 @ X83 @ X207)))) @ X206) @ X206) @ (X205 @ X83)))) @ (X202 @ (X202 @ (X205 @ (X202 @ (X205 @ (X202 @ (X202 @ (X202 @ (X202 @ X207 @ (X202 @ (X205 @ (X205 @ (X202 @ (X202 @ X206 @ X83) @ X207))) @ (X205 @ (X202 @ X206 @ X206)))) @ X206) @ (X205 @ X206)) @ (X202 @ (X202 @ (X202 @ (X202 @ (X202 @ X206 @ X207) @ (X205 @ (X205 @ (X205 @ X207)))) @ X207) @ X83) @ X206))) @ (X202 @ (X202 @ (X202 @ X83 @ X206) @ (X205 @ X83)) @ X83))) @ X207) @ X83)))|((~(?[X208:$i]:((X204 @ (X205 @ X206))))|(c_and @ $false @ $true))&(?[X208:$i]:((X204 @ (X205 @ X206)))|(c_and @ $false @ $false))))))|(c_not @ $false))), introduced(definition)).
% 66.43/22.62 thf(c_0_38, plain, ![X1:$i > $o, X2:$i]:(((c_not @ (($true)))|~((X1 @ X2))|~((epred163_1 @ X1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_11])).
% 66.43/22.62 thf(c_0_39, plain, ![X1:$i > $o, X2:$i]:(((X1 @ (c_Eps_i @ X1))|~((X1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_28])).
% 66.43/22.62 thf(c_0_40, plain, ![X1:$i > $o, X2:$i]:(((X1 @ (esk12_1 @ (epred163_1 @ X1)))|(epred163_1 @ X1 @ X2))), inference(spm,[status(thm)],[c_0_29, c_0_30])).
% 66.43/22.62 thf(c_0_41, plain, ![X2:$i, X6:$i, X12:$i > $i]:(((c_atleastp @ X2 @ X6)|~((c_inj @ X2 @ X6 @ X12)))), inference(split_conjunct,[status(thm)],[c_0_31])).
% 66.43/22.62 thf(c_0_42, plain, ![X2:$i, X12:$i > $i, X6:$i]:(((c_inj @ X6 @ X2 @ X12)|~((epred51_3 @ X12 @ X2 @ X6)))), inference(split_conjunct,[status(thm)],[c_0_32])).
% 66.43/22.62 thf(c_0_43, plain, ![X2:$i]:(~((c_In @ X2 @ c_Empty))), inference(sr,[status(thm)],[c_0_33, c_0_34])).
% 66.43/22.62 thf(c_0_44, plain, ![X12:$i > $i, X6:$i, X2:$i]:(((c_In @ (esk81_3 @ X2 @ X6 @ X12) @ X2)|(c_In @ (esk79_3 @ X2 @ X6 @ X12) @ X2)|(epred51_3 @ X12 @ X6 @ X2))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_35, c_0_36])])).
% 66.43/22.62 thf(c_0_45, negated_conjecture, ~((c_not @ (![X201:$i > $i > $o, X202:$i > $i > $i, X203:$i > $o, X204:$i > $o, X205:$i > $i, X206:$i, X83:$i, X207:$i]:((c_and @ (((X83)=(X202 @ (X202 @ X206 @ (X202 @ X207 @ (X202 @ (X202 @ (X202 @ (X202 @ X83 @ (X202 @ (X202 @ X206 @ (X202 @ X206 @ (X202 @ (X202 @ X206 @ (X202 @ (X205 @ X206) @ (X202 @ (X202 @ X207 @ (X202 @ X83 @ (X202 @ X83 @ X83))) @ X206))) @ (X202 @ (X205 @ (X202 @ (X202 @ (X205 @ X207) @ X206) @ (X202 @ X206 @ X206))) @ (X202 @ X83 @ (X202 @ X83 @ (X202 @ (X202 @ (X202 @ X206 @ (X202 @ (X202 @ X206 @ (X202 @ (X205 @ X83) @ X207)) @ (X205 @ (X202 @ X207 @ X206)))) @ X83) @ (X205 @ (X202 @ (X202 @ X207 @ (X202 @ X206 @ (X202 @ (X205 @ (X202 @ X206 @ X207)) @ X206))) @ (X202 @ (X202 @ (X202 @ X83 @ (X202 @ (X205 @ X206) @ X83)) @ X83) @ (X205 @ (X205 @ (X202 @ (X202 @ (X202 @ (X202 @ X206 @ (X202 @ (X202 @ X83 @ (X202 @ (X202 @ X207 @ X206) @ X207)) @ X83)) @ X207) @ (X202 @ X207 @ (X202 @ X206 @ X206))) @ X83))))))))))))) @ (X202 @ (X202 @ (X202 @ (X202 @ (X202 @ X83 @ (X202 @ X206 @ X206)) @ (X205 @ (X205 @ (X202 @ X207 @ (X205 @ (X205 @ (X202 @ X207 @ X206))))))) @ X206) @ X83) @ (X202 @ X83 @ X207)))) @ X206) @ X206) @ (X205 @ X83)))) @ (X202 @ (X202 @ (X205 @ (X202 @ (X205 @ (X202 @ (X202 @ (X202 @ (X202 @ X207 @ (X202 @ (X205 @ (X205 @ (X202 @ (X202 @ X206 @ X83) @ X207))) @ (X205 @ (X202 @ X206 @ X206)))) @ X206) @ (X205 @ X206)) @ (X202 @ (X202 @ (X202 @ (X202 @ (X202 @ X206 @ X207) @ (X205 @ (X205 @ (X205 @ X207)))) @ X207) @ X83) @ X206))) @ (X202 @ (X202 @ (X202 @ X83 @ X206) @ (X205 @ X83)) @ X83))) @ X207) @ X83)))) @ (?[X208:$i]:((X204 @ (X205 @ X206))))))))), inference(assume_negation,[status(cth)],[conj])).
% 66.43/22.62 thf(c_0_46, plain, ((![X201:$i > $i > $o, X202:$i > $i > $i, X203:$i > $o, X204:$i > $o, X205:$i > $i, X206:$i, X83:$i, X207:$i]:(((((X83)!=(X202 @ (X202 @ X206 @ (X202 @ X207 @ (X202 @ (X202 @ (X202 @ (X202 @ X83 @ (X202 @ (X202 @ X206 @ (X202 @ X206 @ (X202 @ (X202 @ X206 @ (X202 @ (X205 @ X206) @ (X202 @ (X202 @ X207 @ (X202 @ X83 @ (X202 @ X83 @ X83))) @ X206))) @ (X202 @ (X205 @ (X202 @ (X202 @ (X205 @ X207) @ X206) @ (X202 @ X206 @ X206))) @ (X202 @ X83 @ (X202 @ X83 @ (X202 @ (X202 @ (X202 @ X206 @ (X202 @ (X202 @ X206 @ (X202 @ (X205 @ X83) @ X207)) @ (X205 @ (X202 @ X207 @ X206)))) @ X83) @ (X205 @ (X202 @ (X202 @ X207 @ (X202 @ X206 @ (X202 @ (X205 @ (X202 @ X206 @ X207)) @ X206))) @ (X202 @ (X202 @ (X202 @ X83 @ (X202 @ (X205 @ X206) @ X83)) @ X83) @ (X205 @ (X205 @ (X202 @ (X202 @ (X202 @ (X202 @ X206 @ (X202 @ (X202 @ X83 @ (X202 @ (X202 @ X207 @ X206) @ X207)) @ X83)) @ X207) @ (X202 @ X207 @ (X202 @ X206 @ X206))) @ X83))))))))))))) @ (X202 @ (X202 @ (X202 @ (X202 @ (X202 @ X83 @ (X202 @ X206 @ X206)) @ (X205 @ (X205 @ (X202 @ X207 @ (X205 @ (X205 @ (X202 @ X207 @ X206))))))) @ X206) @ X83) @ (X202 @ X83 @ X207)))) @ X206) @ X206) @ (X205 @ X83)))) @ (X202 @ (X202 @ (X205 @ (X202 @ (X205 @ (X202 @ (X202 @ (X202 @ (X202 @ X207 @ (X202 @ (X205 @ (X205 @ (X202 @ (X202 @ X206 @ X83) @ X207))) @ (X205 @ (X202 @ X206 @ X206)))) @ X206) @ (X205 @ X206)) @ (X202 @ (X202 @ (X202 @ (X202 @ (X202 @ X206 @ X207) @ (X205 @ (X205 @ (X205 @ X207)))) @ X207) @ X83) @ X206))) @ (X202 @ (X202 @ (X202 @ X83 @ X206) @ (X205 @ X83)) @ X83))) @ X207) @ X83)))|((~(?[X208:$i]:((X204 @ (X205 @ X206))))|(c_and @ $true @ $true))&(?[X208:$i]:((X204 @ (X205 @ X206)))|(c_and @ $true @ $false))))&(((X83)=(X202 @ (X202 @ X206 @ (X202 @ X207 @ (X202 @ (X202 @ (X202 @ (X202 @ X83 @ (X202 @ (X202 @ X206 @ (X202 @ X206 @ (X202 @ (X202 @ X206 @ (X202 @ (X205 @ X206) @ (X202 @ (X202 @ X207 @ (X202 @ X83 @ (X202 @ X83 @ X83))) @ X206))) @ (X202 @ (X205 @ (X202 @ (X202 @ (X205 @ X207) @ X206) @ (X202 @ X206 @ X206))) @ (X202 @ X83 @ (X202 @ X83 @ (X202 @ (X202 @ (X202 @ X206 @ (X202 @ (X202 @ X206 @ (X202 @ (X205 @ X83) @ X207)) @ (X205 @ (X202 @ X207 @ X206)))) @ X83) @ (X205 @ (X202 @ (X202 @ X207 @ (X202 @ X206 @ (X202 @ (X205 @ (X202 @ X206 @ X207)) @ X206))) @ (X202 @ (X202 @ (X202 @ X83 @ (X202 @ (X205 @ X206) @ X83)) @ X83) @ (X205 @ (X205 @ (X202 @ (X202 @ (X202 @ (X202 @ X206 @ (X202 @ (X202 @ X83 @ (X202 @ (X202 @ X207 @ X206) @ X207)) @ X83)) @ X207) @ (X202 @ X207 @ (X202 @ X206 @ X206))) @ X83))))))))))))) @ (X202 @ (X202 @ (X202 @ (X202 @ (X202 @ X83 @ (X202 @ X206 @ X206)) @ (X205 @ (X205 @ (X202 @ X207 @ (X205 @ (X205 @ (X202 @ X207 @ X206))))))) @ X206) @ X83) @ (X202 @ X83 @ X207)))) @ X206) @ X206) @ (X205 @ X83)))) @ (X202 @ (X202 @ (X205 @ (X202 @ (X205 @ (X202 @ (X202 @ (X202 @ (X202 @ X207 @ (X202 @ (X205 @ (X205 @ (X202 @ (X202 @ X206 @ X83) @ X207))) @ (X205 @ (X202 @ X206 @ X206)))) @ X206) @ (X205 @ X206)) @ (X202 @ (X202 @ (X202 @ (X202 @ (X202 @ X206 @ X207) @ (X205 @ (X205 @ (X205 @ X207)))) @ X207) @ X83) @ X206))) @ (X202 @ (X202 @ (X202 @ X83 @ X206) @ (X205 @ X83)) @ X83))) @ X207) @ X83)))|((~(?[X208:$i]:((X204 @ (X205 @ X206))))|(c_and @ $false @ $true))&(?[X208:$i]:((X204 @ (X205 @ X206)))|(c_and @ $false @ $false))))))|(c_not @ $false))=>(epred143_0)), inference(split_equiv,[status(thm)],[c_0_37])).
% 66.43/22.62 thf(c_0_47, plain, ![X1:$i > $o, X2:$i]:((~((epred163_1 @ X1 @ X2))|~((X1 @ X2)))), inference(sr,[status(thm)],[c_0_38, c_0_34])).
% 66.43/22.62 thf(c_0_48, plain, ![X2:$i, X1:$i > $o]:(((epred163_1 @ X1 @ X2)|(X1 @ (c_Eps_i @ X1)))), inference(spm,[status(thm)],[c_0_39, c_0_40])).
% 66.43/22.62 thf(c_0_49, plain, ![X12:$i > $i, X6:$i, X2:$i]:(((c_atleastp @ X2 @ X6)|~((epred51_3 @ X12 @ X6 @ X2)))), inference(spm,[status(thm)],[c_0_41, c_0_42])).
% 66.43/22.62 thf(c_0_50, plain, ![X12:$i > $i, X2:$i]:((epred51_3 @ X12 @ X2 @ c_Empty)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_44]), c_0_43])).
% 66.43/22.62 thf(c_0_51, negated_conjecture, ~(((~(![X201:$i > $i > $o, X202:$i > $i > $i, X203:$i > $o, X204:$i > $o, X205:$i > $i, X206:$i, X83:$i, X207:$i]:(((((X83)!=(X202 @ (X202 @ X206 @ (X202 @ X207 @ (X202 @ (X202 @ (X202 @ (X202 @ X83 @ (X202 @ (X202 @ X206 @ (X202 @ X206 @ (X202 @ (X202 @ X206 @ (X202 @ (X205 @ X206) @ (X202 @ (X202 @ X207 @ (X202 @ X83 @ (X202 @ X83 @ X83))) @ X206))) @ (X202 @ (X205 @ (X202 @ (X202 @ (X205 @ X207) @ X206) @ (X202 @ X206 @ X206))) @ (X202 @ X83 @ (X202 @ X83 @ (X202 @ (X202 @ (X202 @ X206 @ (X202 @ (X202 @ X206 @ (X202 @ (X205 @ X83) @ X207)) @ (X205 @ (X202 @ X207 @ X206)))) @ X83) @ (X205 @ (X202 @ (X202 @ X207 @ (X202 @ X206 @ (X202 @ (X205 @ (X202 @ X206 @ X207)) @ X206))) @ (X202 @ (X202 @ (X202 @ X83 @ (X202 @ (X205 @ X206) @ X83)) @ X83) @ (X205 @ (X205 @ (X202 @ (X202 @ (X202 @ (X202 @ X206 @ (X202 @ (X202 @ X83 @ (X202 @ (X202 @ X207 @ X206) @ X207)) @ X83)) @ X207) @ (X202 @ X207 @ (X202 @ X206 @ X206))) @ X83))))))))))))) @ (X202 @ (X202 @ (X202 @ (X202 @ (X202 @ X83 @ (X202 @ X206 @ X206)) @ (X205 @ (X205 @ (X202 @ X207 @ (X205 @ (X205 @ (X202 @ X207 @ X206))))))) @ X206) @ X83) @ (X202 @ X83 @ X207)))) @ X206) @ X206) @ (X205 @ X83)))) @ (X202 @ (X202 @ (X205 @ (X202 @ (X205 @ (X202 @ (X202 @ (X202 @ (X202 @ X207 @ (X202 @ (X205 @ (X205 @ (X202 @ (X202 @ X206 @ X83) @ X207))) @ (X205 @ (X202 @ X206 @ X206)))) @ X206) @ (X205 @ X206)) @ (X202 @ (X202 @ (X202 @ (X202 @ (X202 @ X206 @ X207) @ (X205 @ (X205 @ (X205 @ X207)))) @ X207) @ X83) @ X206))) @ (X202 @ (X202 @ (X202 @ X83 @ X206) @ (X205 @ X83)) @ X83))) @ X207) @ X83)))|((~(?[X208:$i]:((X204 @ (X205 @ X206))))|(c_and @ $true @ $true))&(?[X208:$i]:((X204 @ (X205 @ X206)))|(c_and @ $true @ $false))))&(((X83)=(X202 @ (X202 @ X206 @ (X202 @ X207 @ (X202 @ (X202 @ (X202 @ (X202 @ X83 @ (X202 @ (X202 @ X206 @ (X202 @ X206 @ (X202 @ (X202 @ X206 @ (X202 @ (X205 @ X206) @ (X202 @ (X202 @ X207 @ (X202 @ X83 @ (X202 @ X83 @ X83))) @ X206))) @ (X202 @ (X205 @ (X202 @ (X202 @ (X205 @ X207) @ X206) @ (X202 @ X206 @ X206))) @ (X202 @ X83 @ (X202 @ X83 @ (X202 @ (X202 @ (X202 @ X206 @ (X202 @ (X202 @ X206 @ (X202 @ (X205 @ X83) @ X207)) @ (X205 @ (X202 @ X207 @ X206)))) @ X83) @ (X205 @ (X202 @ (X202 @ X207 @ (X202 @ X206 @ (X202 @ (X205 @ (X202 @ X206 @ X207)) @ X206))) @ (X202 @ (X202 @ (X202 @ X83 @ (X202 @ (X205 @ X206) @ X83)) @ X83) @ (X205 @ (X205 @ (X202 @ (X202 @ (X202 @ (X202 @ X206 @ (X202 @ (X202 @ X83 @ (X202 @ (X202 @ X207 @ X206) @ X207)) @ X83)) @ X207) @ (X202 @ X207 @ (X202 @ X206 @ X206))) @ X83))))))))))))) @ (X202 @ (X202 @ (X202 @ (X202 @ (X202 @ X83 @ (X202 @ X206 @ X206)) @ (X205 @ (X205 @ (X202 @ X207 @ (X205 @ (X205 @ (X202 @ X207 @ X206))))))) @ X206) @ X83) @ (X202 @ X83 @ X207)))) @ X206) @ X206) @ (X205 @ X83)))) @ (X202 @ (X202 @ (X205 @ (X202 @ (X205 @ (X202 @ (X202 @ (X202 @ (X202 @ X207 @ (X202 @ (X205 @ (X205 @ (X202 @ (X202 @ X206 @ X83) @ X207))) @ (X205 @ (X202 @ X206 @ X206)))) @ X206) @ (X205 @ X206)) @ (X202 @ (X202 @ (X202 @ (X202 @ (X202 @ X206 @ X207) @ (X205 @ (X205 @ (X205 @ X207)))) @ X207) @ X83) @ X206))) @ (X202 @ (X202 @ (X202 @ X83 @ X206) @ (X205 @ X83)) @ X83))) @ X207) @ X83)))|((~(?[X208:$i]:((X204 @ (X205 @ X206))))|(c_and @ $false @ $true))&(?[X208:$i]:((X204 @ (X205 @ X206)))|(c_and @ $false @ $false)))))))|(c_not @ $true))&(epred143_0))), inference(apply_def,[status(thm)],[inference(fool_unroll,[status(thm)],[c_0_45]), c_0_37])).
% 66.43/22.62 thf(c_0_52, plain, ((((((esk210_0)!=(esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ esk209_0) @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk210_0 @ esk210_0))) @ esk209_0))) @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk208_0 @ esk211_0) @ esk209_0) @ (esk207_0 @ esk209_0 @ esk209_0))) @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ esk210_0) @ esk211_0)) @ (esk208_0 @ (esk207_0 @ esk211_0 @ esk209_0)))) @ esk210_0) @ (esk208_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ esk209_0 @ esk211_0)) @ esk209_0))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk208_0 @ esk209_0) @ esk210_0)) @ esk210_0) @ (esk208_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ esk209_0) @ esk211_0)) @ esk210_0)) @ esk211_0) @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk209_0 @ esk209_0))) @ esk210_0))))))))))))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk209_0 @ esk209_0)) @ (esk208_0 @ (esk208_0 @ (esk207_0 @ esk211_0 @ (esk208_0 @ (esk208_0 @ (esk207_0 @ esk211_0 @ esk209_0))))))) @ esk209_0) @ esk210_0) @ (esk207_0 @ esk210_0 @ esk211_0)))) @ esk209_0) @ esk209_0) @ (esk208_0 @ esk210_0)))) @ (esk207_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ (esk208_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ esk210_0) @ esk211_0))) @ (esk208_0 @ (esk207_0 @ esk209_0 @ esk209_0)))) @ esk209_0) @ (esk208_0 @ esk209_0)) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ esk211_0) @ (esk208_0 @ (esk208_0 @ (esk208_0 @ esk211_0)))) @ esk211_0) @ esk210_0) @ esk209_0))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ esk209_0) @ (esk208_0 @ esk210_0)) @ esk210_0))) @ esk211_0) @ esk210_0)))|((esk210_0)=(esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ esk209_0) @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk210_0 @ esk210_0))) @ esk209_0))) @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk208_0 @ esk211_0) @ esk209_0) @ (esk207_0 @ esk209_0 @ esk209_0))) @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ esk210_0) @ esk211_0)) @ (esk208_0 @ (esk207_0 @ esk211_0 @ esk209_0)))) @ esk210_0) @ (esk208_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ esk209_0 @ esk211_0)) @ esk209_0))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk208_0 @ esk209_0) @ esk210_0)) @ esk210_0) @ (esk208_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ esk209_0) @ esk211_0)) @ esk210_0)) @ esk211_0) @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk209_0 @ esk209_0))) @ esk210_0))))))))))))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk209_0 @ esk209_0)) @ (esk208_0 @ (esk208_0 @ (esk207_0 @ esk211_0 @ (esk208_0 @ (esk208_0 @ (esk207_0 @ esk211_0 @ esk209_0))))))) @ esk209_0) @ esk210_0) @ (esk207_0 @ esk210_0 @ esk211_0)))) @ esk209_0) @ esk209_0) @ (esk208_0 @ esk210_0)))) @ (esk207_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ (esk208_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ esk210_0) @ esk211_0))) @ (esk208_0 @ (esk207_0 @ esk209_0 @ esk209_0)))) @ esk209_0) @ (esk208_0 @ esk209_0)) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ esk211_0) @ (esk208_0 @ (esk208_0 @ (esk208_0 @ esk211_0)))) @ esk211_0) @ esk210_0) @ esk209_0))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ esk209_0) @ (esk208_0 @ esk210_0)) @ esk210_0))) @ esk211_0) @ esk210_0)))|(epred143_0))&(((~(epred153_0 @ (esk208_0 @ esk209_0))|(epred153_0 @ (esk208_0 @ esk209_0))|((esk210_0)=(esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ esk209_0) @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk210_0 @ esk210_0))) @ esk209_0))) @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk208_0 @ esk211_0) @ esk209_0) @ (esk207_0 @ esk209_0 @ esk209_0))) @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ esk210_0) @ esk211_0)) @ (esk208_0 @ (esk207_0 @ esk211_0 @ esk209_0)))) @ esk210_0) @ (esk208_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ esk209_0 @ esk211_0)) @ esk209_0))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk208_0 @ esk209_0) @ esk210_0)) @ esk210_0) @ (esk208_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ esk209_0) @ esk211_0)) @ esk210_0)) @ esk211_0) @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk209_0 @ esk209_0))) @ esk210_0))))))))))))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk209_0 @ esk209_0)) @ (esk208_0 @ (esk208_0 @ (esk207_0 @ esk211_0 @ (esk208_0 @ (esk208_0 @ (esk207_0 @ esk211_0 @ esk209_0))))))) @ esk209_0) @ esk210_0) @ (esk207_0 @ esk210_0 @ esk211_0)))) @ esk209_0) @ esk209_0) @ (esk208_0 @ esk210_0)))) @ (esk207_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ (esk208_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ esk210_0) @ esk211_0))) @ (esk208_0 @ (esk207_0 @ esk209_0 @ esk209_0)))) @ esk209_0) @ (esk208_0 @ esk209_0)) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ esk211_0) @ (esk208_0 @ (esk208_0 @ (esk208_0 @ esk211_0)))) @ esk211_0) @ esk210_0) @ esk209_0))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ esk209_0) @ (esk208_0 @ esk210_0)) @ esk210_0))) @ esk211_0) @ esk210_0)))|(epred143_0))&(~(c_and @ $false @ $false)|(epred153_0 @ (esk208_0 @ esk209_0))|((esk210_0)=(esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ esk209_0) @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk210_0 @ esk210_0))) @ esk209_0))) @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk208_0 @ esk211_0) @ esk209_0) @ (esk207_0 @ esk209_0 @ esk209_0))) @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ esk210_0) @ esk211_0)) @ (esk208_0 @ (esk207_0 @ esk211_0 @ esk209_0)))) @ esk210_0) @ (esk208_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ esk209_0 @ esk211_0)) @ esk209_0))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk208_0 @ esk209_0) @ esk210_0)) @ esk210_0) @ (esk208_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ esk209_0) @ esk211_0)) @ esk210_0)) @ esk211_0) @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk209_0 @ esk209_0))) @ esk210_0))))))))))))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk209_0 @ esk209_0)) @ (esk208_0 @ (esk208_0 @ (esk207_0 @ esk211_0 @ (esk208_0 @ (esk208_0 @ (esk207_0 @ esk211_0 @ esk209_0))))))) @ esk209_0) @ esk210_0) @ (esk207_0 @ esk210_0 @ esk211_0)))) @ esk209_0) @ esk209_0) @ (esk208_0 @ esk210_0)))) @ (esk207_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ (esk208_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ esk210_0) @ esk211_0))) @ (esk208_0 @ (esk207_0 @ esk209_0 @ esk209_0)))) @ esk209_0) @ (esk208_0 @ esk209_0)) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ esk211_0) @ (esk208_0 @ (esk208_0 @ (esk208_0 @ esk211_0)))) @ esk211_0) @ esk210_0) @ esk209_0))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ esk209_0) @ (esk208_0 @ esk210_0)) @ esk210_0))) @ esk211_0) @ esk210_0)))|(epred143_0)))&((~(epred153_0 @ (esk208_0 @ esk209_0))|~(c_and @ $false @ $true)|((esk210_0)=(esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ esk209_0) @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk210_0 @ esk210_0))) @ esk209_0))) @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk208_0 @ esk211_0) @ esk209_0) @ (esk207_0 @ esk209_0 @ esk209_0))) @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ esk210_0) @ esk211_0)) @ (esk208_0 @ (esk207_0 @ esk211_0 @ esk209_0)))) @ esk210_0) @ (esk208_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ esk209_0 @ esk211_0)) @ esk209_0))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk208_0 @ esk209_0) @ esk210_0)) @ esk210_0) @ (esk208_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ esk209_0) @ esk211_0)) @ esk210_0)) @ esk211_0) @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk209_0 @ esk209_0))) @ esk210_0))))))))))))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk209_0 @ esk209_0)) @ (esk208_0 @ (esk208_0 @ (esk207_0 @ esk211_0 @ (esk208_0 @ (esk208_0 @ (esk207_0 @ esk211_0 @ esk209_0))))))) @ esk209_0) @ esk210_0) @ (esk207_0 @ esk210_0 @ esk211_0)))) @ esk209_0) @ esk209_0) @ (esk208_0 @ esk210_0)))) @ (esk207_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ (esk208_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ esk210_0) @ esk211_0))) @ (esk208_0 @ (esk207_0 @ esk209_0 @ esk209_0)))) @ esk209_0) @ (esk208_0 @ esk209_0)) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ esk211_0) @ (esk208_0 @ (esk208_0 @ (esk208_0 @ esk211_0)))) @ esk211_0) @ esk210_0) @ esk209_0))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ esk209_0) @ (esk208_0 @ esk210_0)) @ esk210_0))) @ esk211_0) @ esk210_0)))|(epred143_0))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|((esk210_0)=(esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ esk209_0) @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk210_0 @ esk210_0))) @ esk209_0))) @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk208_0 @ esk211_0) @ esk209_0) @ (esk207_0 @ esk209_0 @ esk209_0))) @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ esk210_0) @ esk211_0)) @ (esk208_0 @ (esk207_0 @ esk211_0 @ esk209_0)))) @ esk210_0) @ (esk208_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ esk209_0 @ esk211_0)) @ esk209_0))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk208_0 @ esk209_0) @ esk210_0)) @ esk210_0) @ (esk208_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ esk209_0) @ esk211_0)) @ esk210_0)) @ esk211_0) @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk209_0 @ esk209_0))) @ esk210_0))))))))))))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk209_0 @ esk209_0)) @ (esk208_0 @ (esk208_0 @ (esk207_0 @ esk211_0 @ (esk208_0 @ (esk208_0 @ (esk207_0 @ esk211_0 @ esk209_0))))))) @ esk209_0) @ esk210_0) @ (esk207_0 @ esk210_0 @ esk211_0)))) @ esk209_0) @ esk209_0) @ (esk208_0 @ esk210_0)))) @ (esk207_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ (esk208_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ esk210_0) @ esk211_0))) @ (esk208_0 @ (esk207_0 @ esk209_0 @ esk209_0)))) @ esk209_0) @ (esk208_0 @ esk209_0)) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ esk211_0) @ (esk208_0 @ (esk208_0 @ (esk208_0 @ esk211_0)))) @ esk211_0) @ esk210_0) @ esk209_0))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ esk209_0) @ (esk208_0 @ esk210_0)) @ esk210_0))) @ esk211_0) @ esk210_0)))|(epred143_0)))))&((((((esk210_0)!=(esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ esk209_0) @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk210_0 @ esk210_0))) @ esk209_0))) @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk208_0 @ esk211_0) @ esk209_0) @ (esk207_0 @ esk209_0 @ esk209_0))) @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ esk210_0) @ esk211_0)) @ (esk208_0 @ (esk207_0 @ esk211_0 @ esk209_0)))) @ esk210_0) @ (esk208_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ esk209_0 @ esk211_0)) @ esk209_0))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk208_0 @ esk209_0) @ esk210_0)) @ esk210_0) @ (esk208_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ esk209_0) @ esk211_0)) @ esk210_0)) @ esk211_0) @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk209_0 @ esk209_0))) @ esk210_0))))))))))))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk209_0 @ esk209_0)) @ (esk208_0 @ (esk208_0 @ (esk207_0 @ esk211_0 @ (esk208_0 @ (esk208_0 @ (esk207_0 @ esk211_0 @ esk209_0))))))) @ esk209_0) @ esk210_0) @ (esk207_0 @ esk210_0 @ esk211_0)))) @ esk209_0) @ esk209_0) @ (esk208_0 @ esk210_0)))) @ (esk207_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ (esk208_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ esk210_0) @ esk211_0))) @ (esk208_0 @ (esk207_0 @ esk209_0 @ esk209_0)))) @ esk209_0) @ (esk208_0 @ esk209_0)) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ esk211_0) @ (esk208_0 @ (esk208_0 @ (esk208_0 @ esk211_0)))) @ esk211_0) @ esk210_0) @ esk209_0))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ esk209_0) @ (esk208_0 @ esk210_0)) @ esk210_0))) @ esk211_0) @ esk210_0)))|(~(epred153_0 @ (esk208_0 @ esk209_0))|(epred153_0 @ (esk208_0 @ esk209_0)))|(epred143_0))&(((~(epred153_0 @ (esk208_0 @ esk209_0))|(epred153_0 @ (esk208_0 @ esk209_0))|(~(epred153_0 @ (esk208_0 @ esk209_0))|(epred153_0 @ (esk208_0 @ esk209_0)))|(epred143_0))&(~(c_and @ $false @ $false)|(epred153_0 @ (esk208_0 @ esk209_0))|(~(epred153_0 @ (esk208_0 @ esk209_0))|(epred153_0 @ (esk208_0 @ esk209_0)))|(epred143_0)))&((~(epred153_0 @ (esk208_0 @ esk209_0))|~(c_and @ $false @ $true)|(~(epred153_0 @ (esk208_0 @ esk209_0))|(epred153_0 @ (esk208_0 @ esk209_0)))|(epred143_0))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|(~(epred153_0 @ (esk208_0 @ esk209_0))|(epred153_0 @ (esk208_0 @ esk209_0)))|(epred143_0)))))&((((esk210_0)!=(esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ esk209_0) @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk210_0 @ esk210_0))) @ esk209_0))) @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk208_0 @ esk211_0) @ esk209_0) @ (esk207_0 @ esk209_0 @ esk209_0))) @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ esk210_0) @ esk211_0)) @ (esk208_0 @ (esk207_0 @ esk211_0 @ esk209_0)))) @ esk210_0) @ (esk208_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ esk209_0 @ esk211_0)) @ esk209_0))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk208_0 @ esk209_0) @ esk210_0)) @ esk210_0) @ (esk208_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ esk209_0) @ esk211_0)) @ esk210_0)) @ esk211_0) @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk209_0 @ esk209_0))) @ esk210_0))))))))))))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk209_0 @ esk209_0)) @ (esk208_0 @ (esk208_0 @ (esk207_0 @ esk211_0 @ (esk208_0 @ (esk208_0 @ (esk207_0 @ esk211_0 @ esk209_0))))))) @ esk209_0) @ esk210_0) @ (esk207_0 @ esk210_0 @ esk211_0)))) @ esk209_0) @ esk209_0) @ (esk208_0 @ esk210_0)))) @ (esk207_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ (esk208_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ esk210_0) @ esk211_0))) @ (esk208_0 @ (esk207_0 @ esk209_0 @ esk209_0)))) @ esk209_0) @ (esk208_0 @ esk209_0)) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ esk211_0) @ (esk208_0 @ (esk208_0 @ (esk208_0 @ esk211_0)))) @ esk211_0) @ esk210_0) @ esk209_0))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ esk209_0) @ (esk208_0 @ esk210_0)) @ esk210_0))) @ esk211_0) @ esk210_0)))|(~(c_and @ $true @ $false)|(epred153_0 @ (esk208_0 @ esk209_0)))|(epred143_0))&(((~(epred153_0 @ (esk208_0 @ esk209_0))|(epred153_0 @ (esk208_0 @ esk209_0))|(~(c_and @ $true @ $false)|(epred153_0 @ (esk208_0 @ esk209_0)))|(epred143_0))&(~(c_and @ $false @ $false)|(epred153_0 @ (esk208_0 @ esk209_0))|(~(c_and @ $true @ $false)|(epred153_0 @ (esk208_0 @ esk209_0)))|(epred143_0)))&((~(epred153_0 @ (esk208_0 @ esk209_0))|~(c_and @ $false @ $true)|(~(c_and @ $true @ $false)|(epred153_0 @ (esk208_0 @ esk209_0)))|(epred143_0))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|(~(c_and @ $true @ $false)|(epred153_0 @ (esk208_0 @ esk209_0)))|(epred143_0))))))&(((((esk210_0)!=(esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ esk209_0) @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk210_0 @ esk210_0))) @ esk209_0))) @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk208_0 @ esk211_0) @ esk209_0) @ (esk207_0 @ esk209_0 @ esk209_0))) @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ esk210_0) @ esk211_0)) @ (esk208_0 @ (esk207_0 @ esk211_0 @ esk209_0)))) @ esk210_0) @ (esk208_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ esk209_0 @ esk211_0)) @ esk209_0))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk208_0 @ esk209_0) @ esk210_0)) @ esk210_0) @ (esk208_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ esk209_0) @ esk211_0)) @ esk210_0)) @ esk211_0) @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk209_0 @ esk209_0))) @ esk210_0))))))))))))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk209_0 @ esk209_0)) @ (esk208_0 @ (esk208_0 @ (esk207_0 @ esk211_0 @ (esk208_0 @ (esk208_0 @ (esk207_0 @ esk211_0 @ esk209_0))))))) @ esk209_0) @ esk210_0) @ (esk207_0 @ esk210_0 @ esk211_0)))) @ esk209_0) @ esk209_0) @ (esk208_0 @ esk210_0)))) @ (esk207_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ (esk208_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ esk210_0) @ esk211_0))) @ (esk208_0 @ (esk207_0 @ esk209_0 @ esk209_0)))) @ esk209_0) @ (esk208_0 @ esk209_0)) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ esk211_0) @ (esk208_0 @ (esk208_0 @ (esk208_0 @ esk211_0)))) @ esk211_0) @ esk210_0) @ esk209_0))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ esk209_0) @ (esk208_0 @ esk210_0)) @ esk210_0))) @ esk211_0) @ esk210_0)))|(~(epred153_0 @ (esk208_0 @ esk209_0))|~(c_and @ $true @ $true))|(epred143_0))&(((~(epred153_0 @ (esk208_0 @ esk209_0))|(epred153_0 @ (esk208_0 @ esk209_0))|(~(epred153_0 @ (esk208_0 @ esk209_0))|~(c_and @ $true @ $true))|(epred143_0))&(~(c_and @ $false @ $false)|(epred153_0 @ (esk208_0 @ esk209_0))|(~(epred153_0 @ (esk208_0 @ esk209_0))|~(c_and @ $true @ $true))|(epred143_0)))&((~(epred153_0 @ (esk208_0 @ esk209_0))|~(c_and @ $false @ $true)|(~(epred153_0 @ (esk208_0 @ esk209_0))|~(c_and @ $true @ $true))|(epred143_0))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|(~(epred153_0 @ (esk208_0 @ esk209_0))|~(c_and @ $true @ $true))|(epred143_0)))))&((((esk210_0)!=(esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ esk209_0) @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk210_0 @ esk210_0))) @ esk209_0))) @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk208_0 @ esk211_0) @ esk209_0) @ (esk207_0 @ esk209_0 @ esk209_0))) @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ esk210_0) @ esk211_0)) @ (esk208_0 @ (esk207_0 @ esk211_0 @ esk209_0)))) @ esk210_0) @ (esk208_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ esk209_0 @ esk211_0)) @ esk209_0))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk208_0 @ esk209_0) @ esk210_0)) @ esk210_0) @ (esk208_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ esk209_0) @ esk211_0)) @ esk210_0)) @ esk211_0) @ (esk207_0 @ esk211_0 @ (esk207_0 @ esk209_0 @ esk209_0))) @ esk210_0))))))))))))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ (esk207_0 @ esk209_0 @ esk209_0)) @ (esk208_0 @ (esk208_0 @ (esk207_0 @ esk211_0 @ (esk208_0 @ (esk208_0 @ (esk207_0 @ esk211_0 @ esk209_0))))))) @ esk209_0) @ esk210_0) @ (esk207_0 @ esk210_0 @ esk211_0)))) @ esk209_0) @ esk209_0) @ (esk208_0 @ esk210_0)))) @ (esk207_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk211_0 @ (esk207_0 @ (esk208_0 @ (esk208_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ esk210_0) @ esk211_0))) @ (esk208_0 @ (esk207_0 @ esk209_0 @ esk209_0)))) @ esk209_0) @ (esk208_0 @ esk209_0)) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk209_0 @ esk211_0) @ (esk208_0 @ (esk208_0 @ (esk208_0 @ esk211_0)))) @ esk211_0) @ esk210_0) @ esk209_0))) @ (esk207_0 @ (esk207_0 @ (esk207_0 @ esk210_0 @ esk209_0) @ (esk208_0 @ esk210_0)) @ esk210_0))) @ esk211_0) @ esk210_0)))|(~(c_and @ $true @ $false)|~(c_and @ $true @ $true))|(epred143_0))&(((~(epred153_0 @ (esk208_0 @ esk209_0))|(epred153_0 @ (esk208_0 @ esk209_0))|(~(c_and @ $true @ $false)|~(c_and @ $true @ $true))|(epred143_0))&(~(c_and @ $false @ $false)|(epred153_0 @ (esk208_0 @ esk209_0))|(~(c_and @ $true @ $false)|~(c_and @ $true @ $true))|(epred143_0)))&((~(epred153_0 @ (esk208_0 @ esk209_0))|~(c_and @ $false @ $true)|(~(c_and @ $true @ $false)|~(c_and @ $true @ $true))|(epred143_0))&(~(c_and @ $false @ $false)|~(c_and @ $false @ $true)|(~(c_and @ $true @ $false)|~(c_and @ $true @ $true))|(epred143_0))))))))&(~(c_not @ $false)|(epred143_0))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_46])])])])])])).
% 66.43/22.62 thf(c_0_53, plain, ![X2:$i, X1:$i > $o]:(((epred163_1 @ (epred163_1 @ X1) @ X2)|~((X1 @ (c_Eps_i @ (epred163_1 @ X1)))))), inference(spm,[status(thm)],[c_0_47, c_0_48])).
% 66.43/22.62 thf(c_0_54, plain, ![X2:$i]:((c_atleastp @ c_Empty @ X2)), inference(spm,[status(thm)],[c_0_49, c_0_50])).
% 66.43/22.62 thf(c_0_55, negated_conjecture, ![X817:$i > $i > $i, X818:$i > $o, X819:$i > $i, X820:$i, X821:$i, X822:$i]:(((((~(X818 @ (X819 @ X820))|(c_and @ $true @ $true)|((X821)!=(X817 @ (X817 @ X820 @ (X817 @ X822 @ (X817 @ (X817 @ (X817 @ (X817 @ X821 @ (X817 @ (X817 @ X820 @ (X817 @ X820 @ (X817 @ (X817 @ X820 @ (X817 @ (X819 @ X820) @ (X817 @ (X817 @ X822 @ (X817 @ X821 @ (X817 @ X821 @ X821))) @ X820))) @ (X817 @ (X819 @ (X817 @ (X817 @ (X819 @ X822) @ X820) @ (X817 @ X820 @ X820))) @ (X817 @ X821 @ (X817 @ X821 @ (X817 @ (X817 @ (X817 @ X820 @ (X817 @ (X817 @ X820 @ (X817 @ (X819 @ X821) @ X822)) @ (X819 @ (X817 @ X822 @ X820)))) @ X821) @ (X819 @ (X817 @ (X817 @ X822 @ (X817 @ X820 @ (X817 @ (X819 @ (X817 @ X820 @ X822)) @ X820))) @ (X817 @ (X817 @ (X817 @ X821 @ (X817 @ (X819 @ X820) @ X821)) @ X821) @ (X819 @ (X819 @ (X817 @ (X817 @ (X817 @ (X817 @ X820 @ (X817 @ (X817 @ X821 @ (X817 @ (X817 @ X822 @ X820) @ X822)) @ X821)) @ X822) @ (X817 @ X822 @ (X817 @ X820 @ X820))) @ X821))))))))))))) @ (X817 @ (X817 @ (X817 @ (X817 @ (X817 @ X821 @ (X817 @ X820 @ X820)) @ (X819 @ (X819 @ (X817 @ X822 @ (X819 @ (X819 @ (X817 @ X822 @ X820))))))) @ X820) @ X821) @ (X817 @ X821 @ X822)))) @ X820) @ X820) @ (X819 @ X821)))) @ (X817 @ (X817 @ (X819 @ (X817 @ (X819 @ (X817 @ (X817 @ (X817 @ (X817 @ X822 @ (X817 @ (X819 @ (X819 @ (X817 @ (X817 @ X820 @ X821) @ X822))) @ (X819 @ (X817 @ X820 @ X820)))) @ X820) @ (X819 @ X820)) @ (X817 @ (X817 @ (X817 @ (X817 @ (X817 @ X820 @ X822) @ (X819 @ (X819 @ (X819 @ X822)))) @ X822) @ X821) @ X820))) @ (X817 @ (X817 @ (X817 @ X821 @ X820) @ (X819 @ X821)) @ X821))) @ X822) @ X821)))|~(epred143_0))&((X818 @ (X819 @ X820))|(c_and @ $true @ $false)|((X821)!=(X817 @ (X817 @ X820 @ (X817 @ X822 @ (X817 @ (X817 @ (X817 @ (X817 @ X821 @ (X817 @ (X817 @ X820 @ (X817 @ X820 @ (X817 @ (X817 @ X820 @ (X817 @ (X819 @ X820) @ (X817 @ (X817 @ X822 @ (X817 @ X821 @ (X817 @ X821 @ X821))) @ X820))) @ (X817 @ (X819 @ (X817 @ (X817 @ (X819 @ X822) @ X820) @ (X817 @ X820 @ X820))) @ (X817 @ X821 @ (X817 @ X821 @ (X817 @ (X817 @ (X817 @ X820 @ (X817 @ (X817 @ X820 @ (X817 @ (X819 @ X821) @ X822)) @ (X819 @ (X817 @ X822 @ X820)))) @ X821) @ (X819 @ (X817 @ (X817 @ X822 @ (X817 @ X820 @ (X817 @ (X819 @ (X817 @ X820 @ X822)) @ X820))) @ (X817 @ (X817 @ (X817 @ X821 @ (X817 @ (X819 @ X820) @ X821)) @ X821) @ (X819 @ (X819 @ (X817 @ (X817 @ (X817 @ (X817 @ X820 @ (X817 @ (X817 @ X821 @ (X817 @ (X817 @ X822 @ X820) @ X822)) @ X821)) @ X822) @ (X817 @ X822 @ (X817 @ X820 @ X820))) @ X821))))))))))))) @ (X817 @ (X817 @ (X817 @ (X817 @ (X817 @ X821 @ (X817 @ X820 @ X820)) @ (X819 @ (X819 @ (X817 @ X822 @ (X819 @ (X819 @ (X817 @ X822 @ X820))))))) @ X820) @ X821) @ (X817 @ X821 @ X822)))) @ X820) @ X820) @ (X819 @ X821)))) @ (X817 @ (X817 @ (X819 @ (X817 @ (X819 @ (X817 @ (X817 @ (X817 @ (X817 @ X822 @ (X817 @ (X819 @ (X819 @ (X817 @ (X817 @ X820 @ X821) @ X822))) @ (X819 @ (X817 @ X820 @ X820)))) @ X820) @ (X819 @ X820)) @ (X817 @ (X817 @ (X817 @ (X817 @ (X817 @ X820 @ X822) @ (X819 @ (X819 @ (X819 @ X822)))) @ X822) @ X821) @ X820))) @ (X817 @ (X817 @ (X817 @ X821 @ X820) @ (X819 @ X821)) @ X821))) @ X822) @ X821)))|~(epred143_0)))&((~(X818 @ (X819 @ X820))|(c_and @ $false @ $true)|((X821)=(X817 @ (X817 @ X820 @ (X817 @ X822 @ (X817 @ (X817 @ (X817 @ (X817 @ X821 @ (X817 @ (X817 @ X820 @ (X817 @ X820 @ (X817 @ (X817 @ X820 @ (X817 @ (X819 @ X820) @ (X817 @ (X817 @ X822 @ (X817 @ X821 @ (X817 @ X821 @ X821))) @ X820))) @ (X817 @ (X819 @ (X817 @ (X817 @ (X819 @ X822) @ X820) @ (X817 @ X820 @ X820))) @ (X817 @ X821 @ (X817 @ X821 @ (X817 @ (X817 @ (X817 @ X820 @ (X817 @ (X817 @ X820 @ (X817 @ (X819 @ X821) @ X822)) @ (X819 @ (X817 @ X822 @ X820)))) @ X821) @ (X819 @ (X817 @ (X817 @ X822 @ (X817 @ X820 @ (X817 @ (X819 @ (X817 @ X820 @ X822)) @ X820))) @ (X817 @ (X817 @ (X817 @ X821 @ (X817 @ (X819 @ X820) @ X821)) @ X821) @ (X819 @ (X819 @ (X817 @ (X817 @ (X817 @ (X817 @ X820 @ (X817 @ (X817 @ X821 @ (X817 @ (X817 @ X822 @ X820) @ X822)) @ X821)) @ X822) @ (X817 @ X822 @ (X817 @ X820 @ X820))) @ X821))))))))))))) @ (X817 @ (X817 @ (X817 @ (X817 @ (X817 @ X821 @ (X817 @ X820 @ X820)) @ (X819 @ (X819 @ (X817 @ X822 @ (X819 @ (X819 @ (X817 @ X822 @ X820))))))) @ X820) @ X821) @ (X817 @ X821 @ X822)))) @ X820) @ X820) @ (X819 @ X821)))) @ (X817 @ (X817 @ (X819 @ (X817 @ (X819 @ (X817 @ (X817 @ (X817 @ (X817 @ X822 @ (X817 @ (X819 @ (X819 @ (X817 @ (X817 @ X820 @ X821) @ X822))) @ (X819 @ (X817 @ X820 @ X820)))) @ X820) @ (X819 @ X820)) @ (X817 @ (X817 @ (X817 @ (X817 @ (X817 @ X820 @ X822) @ (X819 @ (X819 @ (X819 @ X822)))) @ X822) @ X821) @ X820))) @ (X817 @ (X817 @ (X817 @ X821 @ X820) @ (X819 @ X821)) @ X821))) @ X822) @ X821)))|~(epred143_0))&((X818 @ (X819 @ X820))|(c_and @ $false @ $false)|((X821)=(X817 @ (X817 @ X820 @ (X817 @ X822 @ (X817 @ (X817 @ (X817 @ (X817 @ X821 @ (X817 @ (X817 @ X820 @ (X817 @ X820 @ (X817 @ (X817 @ X820 @ (X817 @ (X819 @ X820) @ (X817 @ (X817 @ X822 @ (X817 @ X821 @ (X817 @ X821 @ X821))) @ X820))) @ (X817 @ (X819 @ (X817 @ (X817 @ (X819 @ X822) @ X820) @ (X817 @ X820 @ X820))) @ (X817 @ X821 @ (X817 @ X821 @ (X817 @ (X817 @ (X817 @ X820 @ (X817 @ (X817 @ X820 @ (X817 @ (X819 @ X821) @ X822)) @ (X819 @ (X817 @ X822 @ X820)))) @ X821) @ (X819 @ (X817 @ (X817 @ X822 @ (X817 @ X820 @ (X817 @ (X819 @ (X817 @ X820 @ X822)) @ X820))) @ (X817 @ (X817 @ (X817 @ X821 @ (X817 @ (X819 @ X820) @ X821)) @ X821) @ (X819 @ (X819 @ (X817 @ (X817 @ (X817 @ (X817 @ X820 @ (X817 @ (X817 @ X821 @ (X817 @ (X817 @ X822 @ X820) @ X822)) @ X821)) @ X822) @ (X817 @ X822 @ (X817 @ X820 @ X820))) @ X821))))))))))))) @ (X817 @ (X817 @ (X817 @ (X817 @ (X817 @ X821 @ (X817 @ X820 @ X820)) @ (X819 @ (X819 @ (X817 @ X822 @ (X819 @ (X819 @ (X817 @ X822 @ X820))))))) @ X820) @ X821) @ (X817 @ X821 @ X822)))) @ X820) @ X820) @ (X819 @ X821)))) @ (X817 @ (X817 @ (X819 @ (X817 @ (X819 @ (X817 @ (X817 @ (X817 @ (X817 @ X822 @ (X817 @ (X819 @ (X819 @ (X817 @ (X817 @ X820 @ X821) @ X822))) @ (X819 @ (X817 @ X820 @ X820)))) @ X820) @ (X819 @ X820)) @ (X817 @ (X817 @ (X817 @ (X817 @ (X817 @ X820 @ X822) @ (X819 @ (X819 @ (X819 @ X822)))) @ X822) @ X821) @ X820))) @ (X817 @ (X817 @ (X817 @ X821 @ X820) @ (X819 @ X821)) @ X821))) @ X822) @ X821)))|~(epred143_0))))&(~(c_not @ $true)|~(epred143_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)],[inference(fof_simplification,[status(thm)],[c_0_51])])])])])])).
% 66.43/22.62 thf(c_0_56, plain, ((epred143_0)|~((c_not @ (~($true))))), inference(split_conjunct,[status(thm)],[c_0_52])).
% 66.43/22.62 thf(c_0_57, plain, ![X2:$i]:((epred163_1 @ (epred163_1 @ (c_atleastp @ c_Empty)) @ X2)), inference(spm,[status(thm)],[c_0_53, c_0_54])).
% 66.43/22.62 thf(c_0_58, plain, ![X1998:$i, X1999:$i]:(((esk222_1 @ X1999 @ X1998)=(X1999))), inference(variable_rename,[status(thm)],[])).
% 66.43/22.62 thf(c_0_59, negated_conjecture, ![X1:$i > $o, X2:$i, X12:$i > $i, X89:$i > $i > $i, X7:$i, X6:$i]:(((X1 @ (X12 @ X2))|(c_and @ (~($true)) @ (~($true)))|((X6)=(X89 @ (X89 @ X2 @ (X89 @ X7 @ (X89 @ (X89 @ (X89 @ (X89 @ X6 @ (X89 @ (X89 @ X2 @ (X89 @ X2 @ (X89 @ (X89 @ X2 @ (X89 @ (X12 @ X2) @ (X89 @ (X89 @ X7 @ (X89 @ X6 @ (X89 @ X6 @ X6))) @ X2))) @ (X89 @ (X12 @ (X89 @ (X89 @ (X12 @ X7) @ X2) @ (X89 @ X2 @ X2))) @ (X89 @ X6 @ (X89 @ X6 @ (X89 @ (X89 @ (X89 @ X2 @ (X89 @ (X89 @ X2 @ (X89 @ (X12 @ X6) @ X7)) @ (X12 @ (X89 @ X7 @ X2)))) @ X6) @ (X12 @ (X89 @ (X89 @ X7 @ (X89 @ X2 @ (X89 @ (X12 @ (X89 @ X2 @ X7)) @ X2))) @ (X89 @ (X89 @ (X89 @ X6 @ (X89 @ (X12 @ X2) @ X6)) @ X6) @ (X12 @ (X12 @ (X89 @ (X89 @ (X89 @ (X89 @ X2 @ (X89 @ (X89 @ X6 @ (X89 @ (X89 @ X7 @ X2) @ X7)) @ X6)) @ X7) @ (X89 @ X7 @ (X89 @ X2 @ X2))) @ X6))))))))))))) @ (X89 @ (X89 @ (X89 @ (X89 @ (X89 @ X6 @ (X89 @ X2 @ X2)) @ (X12 @ (X12 @ (X89 @ X7 @ (X12 @ (X12 @ (X89 @ X7 @ X2))))))) @ X2) @ X6) @ (X89 @ X6 @ X7)))) @ X2) @ X2) @ (X12 @ X6)))) @ (X89 @ (X89 @ (X12 @ (X89 @ (X12 @ (X89 @ (X89 @ (X89 @ (X89 @ X7 @ (X89 @ (X12 @ (X12 @ (X89 @ (X89 @ X2 @ X6) @ X7))) @ (X12 @ (X89 @ X2 @ X2)))) @ X2) @ (X12 @ X2)) @ (X89 @ (X89 @ (X89 @ (X89 @ (X89 @ X2 @ X7) @ (X12 @ (X12 @ (X12 @ X7)))) @ X7) @ X6) @ X2))) @ (X89 @ (X89 @ (X89 @ X6 @ X2) @ (X12 @ X6)) @ X6))) @ X7) @ X6)))|~((epred143_0)))), inference(split_conjunct,[status(thm)],[c_0_55])).
% 66.43/22.62 thf(c_0_60, plain, (epred143_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_56, c_0_19])])).
% 66.43/22.62 thf(c_0_61, plain, ![X5:$o]:(~((c_and @ ((X5)) @ (~($true))))), inference(cn,[status(thm)],[inference(cn,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_16])])])).
% 66.43/22.62 thf(c_0_62, plain, ![X2:$i]:((epred163_1 @ (epred163_1 @ (epred163_1 @ (epred163_1 @ (c_atleastp @ c_Empty)))) @ X2)), inference(spm,[status(thm)],[c_0_53, c_0_57])).
% 66.43/22.62 thf(c_0_63, plain, ![X6:$i, X2:$i]:(((esk222_1 @ X2 @ X6)=(X2))), inference(split_conjunct,[status(thm)],[c_0_58])).
% 66.43/22.62 thf(c_0_64, negated_conjecture, ![X1:$i > $o, X6:$i, X89:$i > $i > $i, X7:$i, X12:$i > $i, X2:$i]:((((X89 @ (X89 @ X2 @ (X89 @ X6 @ (X89 @ (X89 @ (X89 @ (X89 @ X7 @ (X89 @ (X89 @ X2 @ (X89 @ X2 @ (X89 @ (X89 @ X2 @ (X89 @ (X12 @ X2) @ (X89 @ (X89 @ X6 @ (X89 @ X7 @ (X89 @ X7 @ X7))) @ X2))) @ (X89 @ (X12 @ (X89 @ (X89 @ (X12 @ X6) @ X2) @ (X89 @ X2 @ X2))) @ (X89 @ X7 @ (X89 @ X7 @ (X89 @ (X89 @ (X89 @ X2 @ (X89 @ (X89 @ X2 @ (X89 @ (X12 @ X7) @ X6)) @ (X12 @ (X89 @ X6 @ X2)))) @ X7) @ (X12 @ (X89 @ (X89 @ X6 @ (X89 @ X2 @ (X89 @ (X12 @ (X89 @ X2 @ X6)) @ X2))) @ (X89 @ (X89 @ (X89 @ X7 @ (X89 @ (X12 @ X2) @ X7)) @ X7) @ (X12 @ (X12 @ (X89 @ (X89 @ (X89 @ (X89 @ X2 @ (X89 @ (X89 @ X7 @ (X89 @ (X89 @ X6 @ X2) @ X6)) @ X7)) @ X6) @ (X89 @ X6 @ (X89 @ X2 @ X2))) @ X7))))))))))))) @ (X89 @ (X89 @ (X89 @ (X89 @ (X89 @ X7 @ (X89 @ X2 @ X2)) @ (X12 @ (X12 @ (X89 @ X6 @ (X12 @ (X12 @ (X89 @ X6 @ X2))))))) @ X2) @ X7) @ (X89 @ X7 @ X6)))) @ X2) @ X2) @ (X12 @ X7)))) @ (X89 @ (X89 @ (X12 @ (X89 @ (X12 @ (X89 @ (X89 @ (X89 @ (X89 @ X6 @ (X89 @ (X12 @ (X12 @ (X89 @ (X89 @ X2 @ X7) @ X6))) @ (X12 @ (X89 @ X2 @ X2)))) @ X2) @ (X12 @ X2)) @ (X89 @ (X89 @ (X89 @ (X89 @ (X89 @ X2 @ X6) @ (X12 @ (X12 @ (X12 @ X6)))) @ X6) @ X7) @ X2))) @ (X89 @ (X89 @ (X89 @ X7 @ X2) @ (X12 @ X7)) @ X7))) @ X6) @ X7))=(X7))|(X1 @ (X12 @ X2)))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_59, c_0_60])]), c_0_61])).
% 66.43/22.62 thf(c_0_65, plain, ![X2:$i]:(~((epred163_1 @ (epred163_1 @ (epred163_1 @ (c_atleastp @ c_Empty))) @ X2))), inference(spm,[status(thm)],[c_0_47, c_0_62])).
% 66.43/22.62 thf(c_0_66, plain, ![X1:$i > $o, X2:$i, X12:$i > $i, X6:$i]:((((X2)=(X6))|(X1 @ (X12 @ X6)))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_64]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63]), c_0_63])).
% 66.43/22.62 thf(c_0_67, negated_conjecture, ![X1:$i > $o, X2:$i, X12:$i > $i, X89:$i > $i > $i, X7:$i, X6:$i]:(((X1 @ (X12 @ X2))|(c_and @ (($true)) @ (~($true)))|((X6)!=(X89 @ (X89 @ X2 @ (X89 @ X7 @ (X89 @ (X89 @ (X89 @ (X89 @ X6 @ (X89 @ (X89 @ X2 @ (X89 @ X2 @ (X89 @ (X89 @ X2 @ (X89 @ (X12 @ X2) @ (X89 @ (X89 @ X7 @ (X89 @ X6 @ (X89 @ X6 @ X6))) @ X2))) @ (X89 @ (X12 @ (X89 @ (X89 @ (X12 @ X7) @ X2) @ (X89 @ X2 @ X2))) @ (X89 @ X6 @ (X89 @ X6 @ (X89 @ (X89 @ (X89 @ X2 @ (X89 @ (X89 @ X2 @ (X89 @ (X12 @ X6) @ X7)) @ (X12 @ (X89 @ X7 @ X2)))) @ X6) @ (X12 @ (X89 @ (X89 @ X7 @ (X89 @ X2 @ (X89 @ (X12 @ (X89 @ X2 @ X7)) @ X2))) @ (X89 @ (X89 @ (X89 @ X6 @ (X89 @ (X12 @ X2) @ X6)) @ X6) @ (X12 @ (X12 @ (X89 @ (X89 @ (X89 @ (X89 @ X2 @ (X89 @ (X89 @ X6 @ (X89 @ (X89 @ X7 @ X2) @ X7)) @ X6)) @ X7) @ (X89 @ X7 @ (X89 @ X2 @ X2))) @ X6))))))))))))) @ (X89 @ (X89 @ (X89 @ (X89 @ (X89 @ X6 @ (X89 @ X2 @ X2)) @ (X12 @ (X12 @ (X89 @ X7 @ (X12 @ (X12 @ (X89 @ X7 @ X2))))))) @ X2) @ X6) @ (X89 @ X6 @ X7)))) @ X2) @ X2) @ (X12 @ X6)))) @ (X89 @ (X89 @ (X12 @ (X89 @ (X12 @ (X89 @ (X89 @ (X89 @ (X89 @ X7 @ (X89 @ (X12 @ (X12 @ (X89 @ (X89 @ X2 @ X6) @ X7))) @ (X12 @ (X89 @ X2 @ X2)))) @ X2) @ (X12 @ X2)) @ (X89 @ (X89 @ (X89 @ (X89 @ (X89 @ X2 @ X7) @ (X12 @ (X12 @ (X12 @ X7)))) @ X7) @ X6) @ X2))) @ (X89 @ (X89 @ (X89 @ X6 @ X2) @ (X12 @ X6)) @ X6))) @ X7) @ X6)))|~((epred143_0)))), inference(split_conjunct,[status(thm)],[c_0_55])).
% 66.43/22.62 thf(c_0_68, plain, ![X2:$i, X6:$i]:(((X2)=(X6))), inference(spm,[status(thm)],[c_0_65, c_0_66])).
% 66.43/22.62 thf(c_0_69, negated_conjecture, ($false), inference(flex_resolve,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_67, c_0_60])]), c_0_68]), c_0_61])]), ['proof']).
% 66.43/22.62 % SZS output end CNFRefutation
% 66.43/22.62 % Parsed axioms : 213
% 66.43/22.62 % Removed by relevancy pruning/SinE : 0
% 66.43/22.62 % Initial clauses : 468714
% 66.43/22.62 % Removed in clause preprocessing : 463874
% 66.43/22.62 % Initial clauses in saturation : 4840
% 66.43/22.62 % Processed clauses : 50908
% 66.43/22.62 % ...of these trivial : 1149
% 66.43/22.62 % ...subsumed : 44064
% 66.43/22.62 % ...remaining for further processing : 5694
% 66.43/22.62 % Other redundant clauses eliminated : 138
% 66.43/22.62 % Clauses deleted for lack of memory : 0
% 66.43/22.62 % Backward-subsumed : 1052
% 66.43/22.62 % Backward-rewritten : 885
% 66.43/22.62 % Generated clauses : 183582
% 66.43/22.62 % ...of the previous two non-redundant : 179289
% 66.43/22.62 % ...aggressively subsumed : 0
% 66.43/22.62 % Contextual simplify-reflections : 174
% 66.43/22.62 % Paramodulations : 181193
% 66.43/22.62 % Factorizations : 0
% 66.43/22.62 % NegExts : 0
% 66.43/22.62 % Equation resolutions : 138
% 66.43/22.62 % Disequality decompositions : 0
% 66.43/22.62 % Total rewrite steps : 53415
% 66.43/22.62 % ...of those cached : 50876
% 66.43/22.62 % Propositional unsat checks : 0
% 66.43/22.62 % Propositional check models : 0
% 66.43/22.62 % Propositional check unsatisfiable : 0
% 66.43/22.62 % Propositional clauses : 0
% 66.43/22.62 % Propositional clauses after purity: 0
% 66.43/22.62 % Propositional unsat core size : 0
% 66.43/22.62 % Propositional preprocessing time : 0.000
% 66.43/22.62 % Propositional encoding time : 0.000
% 66.43/22.62 % Propositional solver time : 0.000
% 66.43/22.62 % Success case prop preproc time : 0.000
% 66.43/22.62 % Success case prop encoding time : 0.000
% 66.43/22.62 % Success case prop solver time : 0.000
% 66.43/22.62 % Current number of processed clauses : 1481
% 66.43/22.62 % Positive orientable unit clauses : 243
% 66.43/22.62 % Positive unorientable unit clauses: 2
% 66.43/22.62 % Negative unit clauses : 117
% 66.43/22.62 % Non-unit-clauses : 1119
% 66.43/22.62 % Current number of unprocessed clauses: 132481
% 66.43/22.62 % ...number of literals in the above : 492597
% 66.43/22.62 % Current number of archived formulas : 0
% 66.43/22.62 % Current number of archived clauses : 4183
% 66.43/22.62 % Clause-clause subsumption calls (NU) : 17007830
% 66.43/22.62 % Rec. Clause-clause subsumption calls : 8670294
% 66.43/22.62 % Non-unit clause-clause subsumptions : 41793
% 66.43/22.62 % Unit Clause-clause subsumption calls : 324003
% 66.43/22.62 % Rewrite failures with RHS unbound : 3803
% 66.43/22.62 % BW rewrite match attempts : 7899
% 66.43/22.62 % BW rewrite match successes : 2304
% 66.43/22.62 % Condensation attempts : 0
% 66.43/22.62 % Condensation successes : 0
% 66.43/22.62 % Termbank termtop insertions : 23189920
% 66.43/22.62 % Search garbage collected termcells : 2011618
% 66.43/22.62
% 66.43/22.62 % -------------------------------------------------
% 66.43/22.62 % User time : 20.465 s
% 66.43/22.62 % System time : 1.354 s
% 66.43/22.62 % Total time : 21.819 s
% 66.43/22.62 % Maximum resident set size: 1256384 pages
% 66.43/22.62
% 66.43/22.62 % -------------------------------------------------
% 66.43/22.62 % User time : 20.473 s
% 66.43/22.62 % System time : 1.556 s
% 66.43/22.62 % Total time : 22.030 s
% 66.43/22.62 % Maximum resident set size: 5376 pages
% 66.43/22.62 % E exiting
%------------------------------------------------------------------------------