%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SWX183^1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:40:28 AM UTC 2026
% Result : Theorem 0.82s 0.41s
% Output : CNFRefutation 0.82s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX183^1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n011.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Tue Sep 29 16:10:31 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running higher-order theorem proving
% 0.07/0.25 Running: /export/starexec/sandbox2/solver/bin/eprover-ho --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox2/tmp/tmp.eRB3kJ4tyo/E---3.1_276083.p
% 0.82/0.41 % Version: 3.5.1-ho
% 0.82/0.41 % partial match(1): HSLSSMSSSSSNHHA
% 0.82/0.41 % Preprocessing class: HSLSSMSSSSSNHHN.
% 0.82/0.41 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.82/0.41 % Starting new_ho_10 with 600s (2) cores
% 0.82/0.41 % Starting sh3 with 600s (2) cores
% 0.82/0.41 % Starting ho_unfolding_3 with 600s (2) cores
% 0.82/0.41 % Starting new_ho_10_cnf2 with 600s (2) cores
% 0.82/0.41 % ho_unfolding_3 with pid 276098 completed with status 0
% 0.82/0.41 % Result found by ho_unfolding_3
% 0.82/0.41 % partial match(1): HSLSSMSSSSSNHHA
% 0.82/0.41 % Preprocessing class: HSLSSMSSSSSNHHN.
% 0.82/0.41 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.82/0.41 % Starting new_ho_10 with 600s (2) cores
% 0.82/0.41 % Starting sh3 with 600s (2) cores
% 0.82/0.41 % Starting ho_unfolding_3 with 600s (2) cores
% 0.82/0.41 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.82/0.41 % No SInE strategy applied
% 0.82/0.41 % Search class: HGHSS-FMLF33-MHHFFMBN
% 0.82/0.41 % partial match(1): HGHSF-FMLF33-MHHFFMBN
% 0.82/0.41 % Scheduled 6 strats onto 2 cores with 600 seconds (600 total)
% 0.82/0.41 % Starting SubtermCWHack with 61s (1) cores
% 0.82/0.41 % Starting new_ho_10 with 121s (1) cores
% 0.82/0.41 % SubtermCWHack with pid 276100 completed with status 0
% 0.82/0.41 % Result found by SubtermCWHack
% 0.82/0.41 % partial match(1): HSLSSMSSSSSNHHA
% 0.82/0.41 % Preprocessing class: HSLSSMSSSSSNHHN.
% 0.82/0.41 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.82/0.41 % Starting new_ho_10 with 600s (2) cores
% 0.82/0.41 % Starting sh3 with 600s (2) cores
% 0.82/0.41 % Starting ho_unfolding_3 with 600s (2) cores
% 0.82/0.41 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.82/0.41 % No SInE strategy applied
% 0.82/0.41 % Search class: HGHSS-FMLF33-MHHFFMBN
% 0.82/0.41 % partial match(1): HGHSF-FMLF33-MHHFFMBN
% 0.82/0.41 % Scheduled 6 strats onto 2 cores with 600 seconds (600 total)
% 0.82/0.41 % Starting SubtermCWHack with 61s (1) cores
% 0.82/0.41 % Preprocessing time : 0.013 s
% 0.82/0.41
% 0.82/0.41 % Proof found!
% 0.82/0.41 % SZS status Theorem
% 0.82/0.41 % SZS output start CNFRefutation
% 0.82/0.41 thf(decl_sort1, type, d_unsorted: $tType).
% 0.82/0.41 thf(decl_23, type, subrel: ($i > $i > $o) > ($i > $i > $o) > $o).
% 0.82/0.41 thf(decl_24, type, inv: ($i > $i > $o) > $i > $i > $o).
% 0.82/0.41 thf(decl_25, type, idem: (($i > $i > $o) > $i > $i > $o) > $o).
% 0.82/0.41 thf(decl_26, type, infl: (($i > $i > $o) > $i > $i > $o) > $o).
% 0.82/0.41 thf(decl_27, type, mono: (($i > $i > $o) > $i > $i > $o) > $o).
% 0.82/0.41 thf(decl_28, type, refl: ($i > $i > $o) > $o).
% 0.82/0.41 thf(decl_29, type, irrefl: ($i > $i > $o) > $o).
% 0.82/0.41 thf(decl_30, type, rc: ($i > $i > $o) > $i > $i > $o).
% 0.82/0.41 thf(decl_31, type, symm: ($i > $i > $o) > $o).
% 0.82/0.41 thf(decl_32, type, antisymm: ($i > $i > $o) > $o).
% 0.82/0.41 thf(decl_33, type, asymm: ($i > $i > $o) > $o).
% 0.82/0.41 thf(decl_34, type, sc: ($i > $i > $o) > $i > $i > $o).
% 0.82/0.41 thf(decl_35, type, trans: ($i > $i > $o) > $o).
% 0.82/0.41 thf(decl_36, type, tc: ($i > $i > $o) > $i > $i > $o).
% 0.82/0.41 thf(decl_37, type, trc: ($i > $i > $o) > $i > $i > $o).
% 0.82/0.41 thf(decl_38, type, trsc: ($i > $i > $o) > $i > $i > $o).
% 0.82/0.41 thf(decl_39, type, po: ($i > $i > $o) > $o).
% 0.82/0.41 thf(decl_40, type, so: ($i > $i > $o) > $o).
% 0.82/0.41 thf(decl_41, type, total: ($i > $i > $o) > $o).
% 0.82/0.41 thf(decl_42, type, term: ($i > $i > $o) > $o).
% 0.82/0.41 thf(decl_43, type, ind: ($i > $i > $o) > $o).
% 0.82/0.41 thf(decl_44, type, innf: ($i > $i > $o) > $i > $o).
% 0.82/0.41 thf(decl_45, type, nfof: ($i > $i > $o) > $i > $i > $o).
% 0.82/0.41 thf(decl_46, type, norm: ($i > $i > $o) > $o).
% 0.82/0.41 thf(decl_47, type, join: ($i > $i > $o) > $i > $i > $o).
% 0.82/0.41 thf(decl_48, type, lconfl: ($i > $i > $o) > $o).
% 0.82/0.41 thf(decl_49, type, sconfl: ($i > $i > $o) > $o).
% 0.82/0.41 thf(decl_50, type, confl: ($i > $i > $o) > $o).
% 0.82/0.41 thf(decl_51, type, cr: ($i > $i > $o) > $o).
% 0.82/0.41 thf(decl_52, type, d2unsorted: d_unsorted > $i).
% 0.82/0.41 thf(decl_53, type, d_unsorted_0: d_unsorted).
% 0.82/0.41 thf(decl_54, type, epred1_3: $i > $i > ($i > $i > $o) > $o).
% 0.82/0.41 thf(decl_55, type, epred2_3: $i > $i > ($i > $i > $o) > $o).
% 0.82/0.41 thf(decl_56, type, epred3_5: ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i > $o).
% 0.82/0.41 thf(decl_58, type, epred5_6: ($i > $i > $o) > ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i > $o).
% 0.82/0.41 thf(decl_60, type, epred7_6: ($i > $i > $o) > ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i > $o).
% 0.82/0.41 thf(decl_62, type, epred9_4: ($i > $i > $o) > ($i > $i > $o) > $i > $i > $o).
% 0.82/0.41 thf(decl_63, type, esk1_1: $i > d_unsorted).
% 0.82/0.41 thf(decl_64, type, esk2_2: ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_65, type, esk3_2: ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_66, type, epred10_1: (($i > $i > $o) > $i > $i > $o) > $i > $i > $o).
% 0.82/0.41 thf(decl_67, type, epred11_1: (($i > $i > $o) > $i > $i > $o) > $i > $i > $o).
% 0.82/0.41 thf(decl_68, type, esk4_1: (($i > $i > $o) > $i > $i > $o) > $i).
% 0.82/0.41 thf(decl_69, type, esk5_1: (($i > $i > $o) > $i > $i > $o) > $i).
% 0.82/0.41 thf(decl_70, type, esk6_5: (($i > $i > $o) > $i > $i > $o) > ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i).
% 0.82/0.41 thf(decl_71, type, esk7_5: (($i > $i > $o) > $i > $i > $o) > ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i).
% 0.82/0.41 thf(decl_72, type, epred12_1: (($i > $i > $o) > $i > $i > $o) > $i > $i > $o).
% 0.82/0.41 thf(decl_73, type, epred13_1: (($i > $i > $o) > $i > $i > $o) > $i > $i > $o).
% 0.82/0.41 thf(decl_74, type, esk8_1: (($i > $i > $o) > $i > $i > $o) > $i).
% 0.82/0.41 thf(decl_75, type, esk9_1: (($i > $i > $o) > $i > $i > $o) > $i).
% 0.82/0.41 thf(decl_76, type, esk10_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_77, type, esk11_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_78, type, esk12_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_79, type, esk13_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_80, type, esk14_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_81, type, esk15_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_82, type, esk16_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_83, type, esk17_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_84, type, esk18_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_85, type, esk19_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_86, type, esk20_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_87, type, esk21_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_88, type, esk22_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_89, type, esk23_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_90, type, esk24_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_91, type, esk25_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_92, type, epred14_3: ($i > $i > $o) > $i > $i > $i > $i > $o).
% 0.82/0.41 thf(decl_93, type, esk26_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_94, type, esk27_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_95, type, esk28_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_96, type, esk29_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_97, type, esk30_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_98, type, epred15_3: ($i > $i > $o) > $i > $i > $i > $i > $o).
% 0.82/0.41 thf(decl_99, type, esk31_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_100, type, esk32_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_101, type, esk33_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_102, type, esk34_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_103, type, esk35_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_104, type, esk36_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_105, type, esk37_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_106, type, esk38_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_107, type, esk39_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_108, type, esk40_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_109, type, esk41_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_110, type, esk42_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_111, type, esk43_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_112, type, esk44_2: ($i > $i > $o) > ($i > $o) > $i).
% 0.82/0.41 thf(decl_113, type, epred16_1: ($i > $i > $o) > $i > $o).
% 0.82/0.41 thf(decl_114, type, esk45_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_115, type, esk46_2: ($i > $i > $o) > $i > $i).
% 0.82/0.41 thf(decl_116, type, esk47_2: ($i > $i > $o) > ($i > $o) > $i).
% 0.82/0.41 thf(decl_117, type, epred17_3: ($i > $i > $o) > ($i > $o) > $i > $i > $i > $o).
% 0.82/0.41 thf(decl_118, type, epred18_1: ($i > $i > $o) > $i > $o).
% 0.82/0.41 thf(decl_119, type, esk48_2: ($i > $i > $o) > $i > $i).
% 0.82/0.41 thf(decl_120, type, esk49_3: ($i > $i > $o) > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_121, type, esk50_3: ($i > $i > $o) > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_122, type, esk51_3: ($i > $i > $o) > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_123, type, esk52_3: ($i > $i > $o) > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_124, type, esk53_3: ($i > $i > $o) > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_125, type, esk54_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_126, type, esk55_2: ($i > $i > $o) > $i > $i).
% 0.82/0.41 thf(decl_127, type, esk56_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_128, type, esk57_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_129, type, esk58_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_130, type, esk59_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_131, type, esk60_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_132, type, epred19_3: ($i > $i > $o) > $i > $i > $i > $i > $o).
% 0.82/0.41 thf(decl_133, type, esk61_3: ($i > $i > $o) > $i > $i > $i).
% 0.82/0.41 thf(decl_134, type, esk62_2: ($i > $i > $o) > $i > $i).
% 0.82/0.41 thf(decl_135, type, esk63_3: ($i > $i > $o) > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_136, type, esk64_3: ($i > $i > $o) > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_137, type, esk65_3: ($i > $i > $o) > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_138, type, esk66_3: ($i > $i > $o) > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_139, type, esk67_3: ($i > $i > $o) > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_140, type, esk68_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_141, type, esk69_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_142, type, epred20_2: ($i > $i > $o) > $i > $i > $i > $o).
% 0.82/0.41 thf(decl_143, type, esk70_2: ($i > $i > $o) > $i > $i).
% 0.82/0.41 thf(decl_144, type, esk71_3: ($i > $i > $o) > $i > $i > $i).
% 0.82/0.41 thf(decl_145, type, esk72_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_146, type, esk73_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_147, type, esk74_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_148, type, esk75_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_149, type, esk76_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_150, type, esk77_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_151, type, esk78_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_152, type, esk79_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_153, type, esk80_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_154, type, esk81_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_155, type, epred21_4: ($i > $i > $o) > $i > $i > $i > $i > $i > $o).
% 0.82/0.41 thf(decl_156, type, epred22_4: ($i > $i > $o) > $i > $i > $i > $i > $i > $o).
% 0.82/0.41 thf(decl_157, type, esk82_6: ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_158, type, esk83_6: ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_159, type, esk84_6: ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_160, type, esk85_6: ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_161, type, esk86_6: ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_162, type, esk87_6: ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_163, type, esk88_6: ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_164, type, esk89_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_165, type, esk90_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_166, type, esk91_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_167, type, epred23_1: ($i > $i > $o) > $i > $i > $o).
% 0.82/0.41 thf(decl_168, type, epred24_1: ($i > $i > $o) > $i > $i > $o).
% 0.82/0.41 thf(decl_169, type, esk92_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_170, type, esk93_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_171, type, esk94_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_172, type, epred25_1: ($i > $i > $o) > $i > $i > $o).
% 0.82/0.41 thf(decl_173, type, epred26_1: ($i > $i > $o) > $i > $i > $o).
% 0.82/0.41 thf(decl_174, type, esk95_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_175, type, esk96_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_176, type, esk97_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_177, type, epred27_1: ($i > $i > $o) > $i > $i > $o).
% 0.82/0.41 thf(decl_178, type, epred28_1: ($i > $i > $o) > $i > $i > $o).
% 0.82/0.41 thf(decl_179, type, esk98_5: ($i > $i > $o) > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_180, type, esk99_5: ($i > $i > $o) > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_181, type, esk100_5: ($i > $i > $o) > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_182, type, esk101_5: ($i > $i > $o) > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_183, type, esk102_5: ($i > $i > $o) > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_184, type, esk103_5: ($i > $i > $o) > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_185, type, esk104_5: ($i > $i > $o) > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_186, type, esk105_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_187, type, esk106_1: ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_188, type, epred29_1: ($i > $i > $o) > $i > $i > $o).
% 0.82/0.41 thf(decl_189, type, epred30_1: ($i > $i > $o) > $i > $i > $o).
% 0.82/0.41 thf(decl_190, type, epred31_0: $i > $i > $o).
% 0.82/0.41 thf(decl_191, type, esk107_0: $i).
% 0.82/0.41 thf(decl_192, type, esk108_0: $i).
% 0.82/0.41 thf(decl_193, type, esk109_0: $i).
% 0.82/0.41 thf(decl_206, type, epred34_3: ($i > $i > $o) > $i > $i > $i > $i > $o).
% 0.82/0.41 thf(decl_207, type, epred35_3: ($i > $i > $o) > $i > $i > $i > $i > $o).
% 0.82/0.41 thf(decl_208, type, esk120_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_209, type, esk121_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_210, type, esk122_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_211, type, esk123_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_212, type, esk124_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_213, type, esk125_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_214, type, esk126_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_215, type, esk127_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_216, type, esk128_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_217, type, esk129_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_218, type, esk130_5: $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_219, type, esk131_6: $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_220, type, esk132_6: $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_221, type, esk133_6: $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_222, type, esk134_6: $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_223, type, esk135_6: $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_224, type, esk136_6: $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_225, type, esk137_6: $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_226, type, esk138_6: $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_227, type, esk139_6: $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_228, type, esk140_6: $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_229, type, esk141_5: $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_230, type, esk142_5: $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_231, type, esk143_5: $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.82/0.41 thf(decl_232, type, epred36_6: $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i > $o).
% 0.82/0.41 thf(decl_233, type, epred37_6: $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i > $o).
% 0.82/0.41 thf(sev441_1, axiom, (((((((((((((((((((((((((((((((![X1:$i]:(?[X2:d_unsorted]:(((X1)=(d2unsorted @ X2))))&![X2:d_unsorted]:(((X2)=(d_unsorted_0))))&![X3:d_unsorted, X4:d_unsorted]:((((d2unsorted @ X3)=(d2unsorted @ X4))=>((X3)=(X4)))))&((subrel)=(^[X5:$i > $i > $o, X6:$i > $i > $o]:(![X7:$i, X8:$i]:(((~((X5 @ X7 @ X8)))|((X6 @ X7 @ X8))))))))&((inv)=(^[X5:$i > $i > $o, X7:$i, X8:$i]:((X5 @ X8 @ X7)))))&((idem)=(^[X9:($i > $i > $o) > $i > $i > $o]:(![X5:$i > $i > $o]:(((X9 @ X5)=(X9 @ (X9 @ X5))))))))&((infl)=(^[X9:($i > $i > $o) > $i > $i > $o]:(![X5:$i > $i > $o, X7:$i, X8:$i]:(((~((X5 @ X7 @ X8)))|((X9 @ X5 @ X7 @ X8))))))))&((mono)=(^[X9:($i > $i > $o) > $i > $i > $o]:(![X5:$i > $i > $o, X6:$i > $i > $o, X10:$i, X11:$i]:(((((~(![X7:$i, X8:$i]:(((~((X5 @ X7 @ X8)))|((X6 @ X7 @ X8))))))|(~((X9 @ X5 @ X10 @ X11)))))|((X9 @ X6 @ X10 @ X11))))))))&((refl)=(^[X5:$i > $i > $o]:(![X7:$i]:((X5 @ X7 @ X7))))))&((irrefl)=(^[X5:$i > $i > $o]:(![X7:$i]:(~((X5 @ X7 @ X7)))))))&((rc)=(^[X5:$i > $i > $o, X7:$i, X8:$i]:(((((X7)=(X8)))|((X5 @ X7 @ X8)))))))&((symm)=(^[X5:$i > $i > $o]:(![X7:$i, X8:$i]:(((~((X5 @ X7 @ X8)))|((X5 @ X8 @ X7))))))))&((antisymm)=(^[X5:$i > $i > $o]:(![X7:$i, X8:$i]:(((((~((X5 @ X7 @ X8)))|(~((X5 @ X8 @ X7)))))|(((X7)=(X8)))))))))&((asymm)=(^[X5:$i > $i > $o]:(![X7:$i, X8:$i]:(((~((X5 @ X7 @ X8)))|(~((X5 @ X8 @ X7)))))))))&((sc)=(^[X5:$i > $i > $o, X7:$i, X8:$i]:((((X5 @ X8 @ X7))|((X5 @ X7 @ X8)))))))&((trans)=(^[X5:$i > $i > $o]:(![X7:$i, X8:$i, X12:$i]:(((((~((X5 @ X7 @ X8)))|(~((X5 @ X8 @ X12)))))|((X5 @ X7 @ X12))))))))&((tc)=(^[X5:$i > $i > $o, X7:$i, X8:$i]:(![X6:$i > $i > $o]:(((((~(![X13:$i, X14:$i, X12:$i]:(((((~((X6 @ X13 @ X14)))|(~((X6 @ X14 @ X12)))))|((X6 @ X13 @ X12))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X6 @ X15 @ X16))))))))|((X6 @ X7 @ X8))))))))&((trc)=(^[X5:$i > $i > $o, X17:$i, X18:$i]:(((((X17)=(X18)))|(![X6:$i > $i > $o]:(((((~(![X13:$i, X14:$i, X12:$i]:(((((~((X6 @ X13 @ X14)))|(~((X6 @ X14 @ X12)))))|((X6 @ X13 @ X12))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X6 @ X15 @ X16))))))))|((X6 @ X17 @ X18))))))))))&((trsc)=(^[X5:$i > $i > $o, X17:$i, X18:$i]:(((((((X17)=(X18)))|(![X6:$i > $i > $o]:(((((~(![X13:$i, X14:$i, X12:$i]:(((((~((X6 @ X13 @ X14)))|(~((X6 @ X14 @ X12)))))|((X6 @ X13 @ X12))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X6 @ X15 @ X16))))))))|((X6 @ X18 @ X17)))))))|(![X6:$i > $i > $o]:(((((~(![X13:$i, X14:$i, X12:$i]:(((((~((X6 @ X13 @ X14)))|(~((X6 @ X14 @ X12)))))|((X6 @ X13 @ X12))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X6 @ X15 @ X16))))))))|((X6 @ X17 @ X18))))))))))&((po)=(^[X5:$i > $i > $o]:(((((![X7:$i]:((X5 @ X7 @ X7)))&(![X7:$i, X8:$i]:(((((~((X5 @ X7 @ X8)))|(~((X5 @ X8 @ X7)))))|(((X7)=(X8))))))))&(![X7:$i, X8:$i, X12:$i]:(((((~((X5 @ X7 @ X8)))|(~((X5 @ X8 @ X12)))))|((X5 @ X7 @ X12))))))))))&((so)=(^[X5:$i > $i > $o]:(((![X7:$i, X8:$i]:(((~((X5 @ X7 @ X8)))|(~((X5 @ X8 @ X7))))))&(![X7:$i, X8:$i, X12:$i]:(((((~((X5 @ X7 @ X8)))|(~((X5 @ X8 @ X12)))))|((X5 @ X7 @ X12))))))))))&((total)=(^[X5:$i > $i > $o]:(![X7:$i, X8:$i]:(((((((X7)=(X8)))|((X5 @ X7 @ X8))))|((X5 @ X8 @ X7))))))))&((term)=(^[X5:$i > $i > $o]:(![X19:$i > $o, X20:$i]:(((~((X19 @ X20)))|(~(![X7:$i]:(((~((X19 @ X7)))|(~(![X8:$i]:(((~((X19 @ X8)))|(~((X5 @ X7 @ X8)))))))))))))))))&((ind)=(^[X5:$i > $i > $o]:(![X21:$i > $o, X22:$i]:(((~(![X7:$i]:(((~(![X8:$i]:(((~(![X6:$i > $i > $o]:(((((~(![X13:$i, X14:$i, X12:$i]:(((((~((X6 @ X13 @ X14)))|(~((X6 @ X14 @ X12)))))|((X6 @ X13 @ X12))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X6 @ X15 @ X16))))))))|((X6 @ X7 @ X8))))))|((X21 @ X8))))))|((X21 @ X7))))))|((X21 @ X22))))))))&((innf)=(^[X5:$i > $i > $o, X7:$i]:(![X8:$i]:(~((X5 @ X7 @ X8)))))))&((nfof)=(^[X5:$i > $i > $o, X7:$i, X8:$i]:(((((((X7)=(X8)))|(![X6:$i > $i > $o]:(((((~(![X13:$i, X14:$i, X12:$i]:(((((~((X6 @ X13 @ X14)))|(~((X6 @ X14 @ X12)))))|((X6 @ X13 @ X12))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X6 @ X15 @ X16))))))))|((X6 @ X8 @ X7)))))))&(![X23:$i]:(~((X5 @ X7 @ X23)))))))))&((norm)=(^[X5:$i > $i > $o]:(![X7:$i, X24:$i]:(((~((X5 @ X7 @ X24)))|(~(![X25:$i]:(((~(![X6:$i > $i > $o]:(((((~(![X13:$i, X14:$i, X12:$i]:(((((~((X6 @ X13 @ X14)))|(~((X6 @ X14 @ X12)))))|((X6 @ X13 @ X12))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X6 @ X15 @ X16))))))))|((X6 @ X7 @ X25))))))|(~(![X23:$i]:(~((X5 @ X25 @ X23)))))))))))))))&((join)=(^[X5:$i > $i > $o, X7:$i, X8:$i]:(~(((((((((X7)!=(X8)))&(~(![X6:$i > $i > $o]:(((((~(![X13:$i, X14:$i, X26:$i]:(((((~((X6 @ X13 @ X14)))|(~((X6 @ X14 @ X26)))))|((X6 @ X13 @ X26))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X6 @ X15 @ X16))))))))|((X6 @ X8 @ X7))))))))&(~(![X6:$i > $i > $o]:(((((~(![X13:$i, X14:$i, X27:$i]:(((((~((X6 @ X13 @ X14)))|(~((X6 @ X14 @ X27)))))|((X6 @ X13 @ X27))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X6 @ X15 @ X16))))))))|((X6 @ X7 @ X8))))))))&(![X28:$i]:(((~(![X6:$i > $i > $o]:(((((~(![X13:$i, X14:$i, X26:$i]:(((((~((X6 @ X13 @ X14)))|(~((X6 @ X14 @ X26)))))|((X6 @ X13 @ X26))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X6 @ X15 @ X16))))))))|((X6 @ X8 @ X28))))))|(~(![X6:$i > $i > $o]:(((((~(![X13:$i, X14:$i, X27:$i]:(((((~((X6 @ X13 @ X14)))|(~((X6 @ X14 @ X27)))))|((X6 @ X13 @ X27))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X6 @ X15 @ X16))))))))|((X6 @ X7 @ X28)))))))))))))))&((lconfl)=(^[X5:$i > $i > $o]:(![X7:$i, X8:$i, X12:$i, X29:$i > $i > $o, X30:$i > $i > $o]:(((((((((((((((((((~((X5 @ X7 @ X12)))|(~((X5 @ X7 @ X8)))))|(((X8)=(X12)))))|(~(![X28:$i]:(((~(![X6:$i > $i > $o]:(((((~(![X13:$i, X14:$i, X26:$i]:(((((~((X6 @ X13 @ X14)))|(~((X6 @ X14 @ X26)))))|((X6 @ X13 @ X26))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X6 @ X15 @ X16))))))))|((X6 @ X8 @ X28))))))|(~(![X6:$i > $i > $o]:(((((~(![X13:$i, X14:$i, X27:$i]:(((((~((X6 @ X13 @ X14)))|(~((X6 @ X14 @ X27)))))|((X6 @ X13 @ X27))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X6 @ X15 @ X16))))))))|((X6 @ X12 @ X28))))))))))))|(~(![X13:$i, X14:$i, X26:$i]:(((((~((X29 @ X13 @ X14)))|(~((X29 @ X14 @ X26)))))|((X29 @ X13 @ X26))))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X29 @ X15 @ X16))))))))|((X29 @ X8 @ X12))))|(~(![X13:$i, X14:$i, X27:$i]:(((((~((X30 @ X13 @ X14)))|(~((X30 @ X14 @ X27)))))|((X30 @ X13 @ X27))))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X30 @ X15 @ X16))))))))|((X30 @ X12 @ X8))))))))&((sconfl)=(^[X5:$i > $i > $o]:(![X7:$i, X8:$i, X12:$i, X31:$i > $i > $o, X32:$i > $i > $o]:(((((((((((((((((((~((X5 @ X7 @ X12)))|(((((X7)!=(X8)))&(~(![X6:$i > $i > $o]:(((((~(![X13:$i, X14:$i, X33:$i]:(((((~((X6 @ X13 @ X14)))|(~((X6 @ X14 @ X33)))))|((X6 @ X13 @ X33))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X6 @ X15 @ X16))))))))|((X6 @ X7 @ X8))))))))))|(((X8)=(X12)))))|(~(![X28:$i]:(((~(![X6:$i > $i > $o]:(((((~(![X13:$i, X14:$i, X26:$i]:(((((~((X6 @ X13 @ X14)))|(~((X6 @ X14 @ X26)))))|((X6 @ X13 @ X26))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X6 @ X15 @ X16))))))))|((X6 @ X8 @ X28))))))|(~(![X6:$i > $i > $o]:(((((~(![X13:$i, X14:$i, X27:$i]:(((((~((X6 @ X13 @ X14)))|(~((X6 @ X14 @ X27)))))|((X6 @ X13 @ X27))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X6 @ X15 @ X16))))))))|((X6 @ X12 @ X28))))))))))))|(~(![X13:$i, X14:$i, X26:$i]:(((((~((X31 @ X13 @ X14)))|(~((X31 @ X14 @ X26)))))|((X31 @ X13 @ X26))))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X31 @ X15 @ X16))))))))|((X31 @ X8 @ X12))))|(~(![X13:$i, X14:$i, X27:$i]:(((((~((X32 @ X13 @ X14)))|(~((X32 @ X14 @ X27)))))|((X32 @ X13 @ X27))))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X32 @ X15 @ X16))))))))|((X32 @ X12 @ X8))))))))&((confl)=(^[X5:$i > $i > $o]:(![X7:$i, X8:$i, X12:$i, X34:$i > $i > $o, X35:$i > $i > $o]:(((((((((((((((((((((((X7)!=(X12)))&(~(![X6:$i > $i > $o]:(((((~(![X13:$i, X14:$i, X27:$i]:(((((~((X6 @ X13 @ X14)))|(~((X6 @ X14 @ X27)))))|((X6 @ X13 @ X27))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X6 @ X15 @ X16))))))))|((X6 @ X7 @ X12))))))))|(((((X7)!=(X8)))&(~(![X6:$i > $i > $o]:(((((~(![X13:$i, X14:$i, X36:$i]:(((((~((X6 @ X13 @ X14)))|(~((X6 @ X14 @ X36)))))|((X6 @ X13 @ X36))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X6 @ X15 @ X16))))))))|((X6 @ X7 @ X8))))))))))|(((X8)=(X12)))))|(~(![X28:$i]:(((~(![X6:$i > $i > $o]:(((((~(![X13:$i, X14:$i, X26:$i]:(((((~((X6 @ X13 @ X14)))|(~((X6 @ X14 @ X26)))))|((X6 @ X13 @ X26))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X6 @ X15 @ X16))))))))|((X6 @ X8 @ X28))))))|(~(![X6:$i > $i > $o]:(((((~(![X13:$i, X14:$i, X27:$i]:(((((~((X6 @ X13 @ X14)))|(~((X6 @ X14 @ X27)))))|((X6 @ X13 @ X27))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X6 @ X15 @ X16))))))))|((X6 @ X12 @ X28))))))))))))|(~(![X13:$i, X14:$i, X26:$i]:(((((~((X34 @ X13 @ X14)))|(~((X34 @ X14 @ X26)))))|((X34 @ X13 @ X26))))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X34 @ X15 @ X16))))))))|((X34 @ X8 @ X12))))|(~(![X13:$i, X14:$i, X27:$i]:(((((~((X35 @ X13 @ X14)))|(~((X35 @ X14 @ X27)))))|((X35 @ X13 @ X27))))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X35 @ X15 @ X16))))))))|((X35 @ X12 @ X8))))))))&((cr)=(^[X5:$i > $i > $o]:(![X7:$i, X8:$i, X37:$i > $i > $o, X38:$i > $i > $o]:(((((((((((((((((((((((X7)!=(X8)))&(~(![X6:$i > $i > $o]:(((((~(![X13:$i, X14:$i, X12:$i]:(((((~((X6 @ X13 @ X14)))|(~((X6 @ X14 @ X12)))))|((X6 @ X13 @ X12))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X6 @ X15 @ X16))))))))|((X6 @ X8 @ X7))))))))&(~(![X6:$i > $i > $o]:(((((~(![X13:$i, X14:$i, X12:$i]:(((((~((X6 @ X13 @ X14)))|(~((X6 @ X14 @ X12)))))|((X6 @ X13 @ X12))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X6 @ X15 @ X16))))))))|((X6 @ X7 @ X8))))))))|(((X7)=(X8)))))|(~(![X28:$i]:(((~(![X6:$i > $i > $o]:(((((~(![X13:$i, X14:$i, X26:$i]:(((((~((X6 @ X13 @ X14)))|(~((X6 @ X14 @ X26)))))|((X6 @ X13 @ X26))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X6 @ X15 @ X16))))))))|((X6 @ X8 @ X28))))))|(~(![X6:$i > $i > $o]:(((((~(![X13:$i, X14:$i, X27:$i]:(((((~((X6 @ X13 @ X14)))|(~((X6 @ X14 @ X27)))))|((X6 @ X13 @ X27))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X6 @ X15 @ X16))))))))|((X6 @ X7 @ X28))))))))))))|(~(![X13:$i, X14:$i, X26:$i]:(((((~((X37 @ X13 @ X14)))|(~((X37 @ X14 @ X26)))))|((X37 @ X13 @ X26))))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X37 @ X15 @ X16))))))))|((X37 @ X8 @ X7))))|(~(![X13:$i, X14:$i, X27:$i]:(((((~((X38 @ X13 @ X14)))|(~((X38 @ X14 @ X27)))))|((X38 @ X13 @ X27))))))))|(~(![X15:$i, X16:$i]:(((~((X5 @ X15 @ X16)))|((X38 @ X15 @ X16))))))))|((X38 @ X7 @ X8)))))))), file('/export/starexec/sandbox2/tmp/tmp.eRB3kJ4tyo/E---3.1_276083.p', sev441_1)).
% 0.82/0.41 thf(locally_confluent, conjecture, ((lconfl)=(^[X5:$i > $i > $o]:(![X7:$i, X8:$i, X12:$i]:((((((X5 @ X7 @ X12))&((X5 @ X7 @ X8))))=>((join @ X5 @ X12 @ X8))))))), file('/export/starexec/sandbox2/tmp/tmp.eRB3kJ4tyo/E---3.1_276083.p', locally_confluent)).
% 0.82/0.41 thf(c_0_2, plain, ![X70:$i > $i > $o, X71:$i, X72:$i]:(((epred1_3 @ X72 @ X71 @ X70)<=>(((X71)=(X72))|![X6:$i > $i > $o]:((~(![X13:$i, X14:$i, X12:$i]:((~((X6 @ X13 @ X14))|~((X6 @ X14 @ X12))|(X6 @ X13 @ X12))))|~(![X15:$i, X16:$i]:((~((X70 @ X15 @ X16))|(X6 @ X15 @ X16))))|(X6 @ X72 @ X71)))|![X6:$i > $i > $o]:((~(![X13:$i, X14:$i, X12:$i]:((~((X6 @ X13 @ X14))|~((X6 @ X14 @ X12))|(X6 @ X13 @ X12))))|~(![X15:$i, X16:$i]:((~((X70 @ X15 @ X16))|(X6 @ X15 @ X16))))|(X6 @ X71 @ X72)))))), introduced(definition)).
% 0.82/0.41 thf(c_0_3, plain, ![X84:$i > $i > $o, X85:$i, X86:$i]:(((epred2_3 @ X86 @ X85 @ X84)<=>((((X85)!=(X86))&~(![X6:$i > $i > $o]:((~(![X13:$i, X14:$i, X26:$i]:((~((X6 @ X13 @ X14))|~((X6 @ X14 @ X26))|(X6 @ X13 @ X26))))|~(![X15:$i, X16:$i]:((~((X84 @ X15 @ X16))|(X6 @ X15 @ X16))))|(X6 @ X86 @ X85)))))&~(![X6:$i > $i > $o]:((~(![X13:$i, X14:$i, X27:$i]:((~((X6 @ X13 @ X14))|~((X6 @ X14 @ X27))|(X6 @ X13 @ X27))))|~(![X15:$i, X16:$i]:((~((X84 @ X15 @ X16))|(X6 @ X15 @ X16))))|(X6 @ X85 @ X86))))))), introduced(definition)).
% 0.82/0.41 thf(c_0_4, plain, ![X7:$i, X8:$i, X12:$i, X87:$i > $i > $o, X29:$i > $i > $o]:(((epred3_5 @ X29 @ X87 @ X12 @ X8 @ X7)<=>(~((X87 @ X7 @ X12))|~((X87 @ X7 @ X8))|((X8)=(X12))|~(![X28:$i]:((~(![X6:$i > $i > $o]:((~(![X13:$i, X14:$i, X26:$i]:((~((X6 @ X13 @ X14))|~((X6 @ X14 @ X26))|(X6 @ X13 @ X26))))|~(![X15:$i, X16:$i]:((~((X87 @ X15 @ X16))|(X6 @ X15 @ X16))))|(X6 @ X8 @ X28))))|~(![X6:$i > $i > $o]:((~(![X13:$i, X14:$i, X27:$i]:((~((X6 @ X13 @ X14))|~((X6 @ X14 @ X27))|(X6 @ X13 @ X27))))|~(![X15:$i, X16:$i]:((~((X87 @ X15 @ X16))|(X6 @ X15 @ X16))))|(X6 @ X12 @ X28)))))))|~(![X13:$i, X14:$i, X26:$i]:((~((X29 @ X13 @ X14))|~((X29 @ X14 @ X26))|(X29 @ X13 @ X26))))))), introduced(definition)).
% 0.82/0.41 thf(c_0_5, plain, ![X7:$i, X8:$i, X12:$i, X31:$i > $i > $o, X88:$i > $i > $o, X32:$i > $i > $o]:(((epred5_6 @ X32 @ X88 @ X31 @ X12 @ X8 @ X7)<=>(~((X88 @ X7 @ X12))|(((X7)!=(X8))&~(![X6:$i > $i > $o]:((~(![X13:$i, X14:$i, X33:$i]:((~((X6 @ X13 @ X14))|~((X6 @ X14 @ X33))|(X6 @ X13 @ X33))))|~(![X15:$i, X16:$i]:((~((X88 @ X15 @ X16))|(X6 @ X15 @ X16))))|(X6 @ X7 @ X8)))))|((X8)=(X12))|~(![X28:$i]:((~(![X6:$i > $i > $o]:((~(![X13:$i, X14:$i, X26:$i]:((~((X6 @ X13 @ X14))|~((X6 @ X14 @ X26))|(X6 @ X13 @ X26))))|~(![X15:$i, X16:$i]:((~((X88 @ X15 @ X16))|(X6 @ X15 @ X16))))|(X6 @ X8 @ X28))))|~(![X6:$i > $i > $o]:((~(![X13:$i, X14:$i, X27:$i]:((~((X6 @ X13 @ X14))|~((X6 @ X14 @ X27))|(X6 @ X13 @ X27))))|~(![X15:$i, X16:$i]:((~((X88 @ X15 @ X16))|(X6 @ X15 @ X16))))|(X6 @ X12 @ X28)))))))|~(![X13:$i, X14:$i, X26:$i]:((~((X31 @ X13 @ X14))|~((X31 @ X14 @ X26))|(X31 @ X13 @ X26))))|~(![X15:$i, X16:$i]:((~((X88 @ X15 @ X16))|(X31 @ X15 @ X16))))|(X31 @ X8 @ X12)|~(![X13:$i, X14:$i, X27:$i]:((~((X32 @ X13 @ X14))|~((X32 @ X14 @ X27))|(X32 @ X13 @ X27))))|~(![X15:$i, X16:$i]:((~((X88 @ X15 @ X16))|(X32 @ X15 @ X16))))))), introduced(definition)).
% 0.82/0.41 thf(c_0_6, plain, ![X7:$i, X8:$i, X12:$i, X34:$i > $i > $o, X89:$i > $i > $o, X35:$i > $i > $o]:(((epred7_6 @ X35 @ X89 @ X34 @ X12 @ X8 @ X7)<=>((((X7)!=(X12))&~(![X6:$i > $i > $o]:((~(![X13:$i, X14:$i, X27:$i]:((~((X6 @ X13 @ X14))|~((X6 @ X14 @ X27))|(X6 @ X13 @ X27))))|~(![X15:$i, X16:$i]:((~((X89 @ X15 @ X16))|(X6 @ X15 @ X16))))|(X6 @ X7 @ X12)))))|(((X7)!=(X8))&~(![X6:$i > $i > $o]:((~(![X13:$i, X14:$i, X36:$i]:((~((X6 @ X13 @ X14))|~((X6 @ X14 @ X36))|(X6 @ X13 @ X36))))|~(![X15:$i, X16:$i]:((~((X89 @ X15 @ X16))|(X6 @ X15 @ X16))))|(X6 @ X7 @ X8)))))|((X8)=(X12))|~(![X28:$i]:((~(![X6:$i > $i > $o]:((~(![X13:$i, X14:$i, X26:$i]:((~((X6 @ X13 @ X14))|~((X6 @ X14 @ X26))|(X6 @ X13 @ X26))))|~(![X15:$i, X16:$i]:((~((X89 @ X15 @ X16))|(X6 @ X15 @ X16))))|(X6 @ X8 @ X28))))|~(![X6:$i > $i > $o]:((~(![X13:$i, X14:$i, X27:$i]:((~((X6 @ X13 @ X14))|~((X6 @ X14 @ X27))|(X6 @ X13 @ X27))))|~(![X15:$i, X16:$i]:((~((X89 @ X15 @ X16))|(X6 @ X15 @ X16))))|(X6 @ X12 @ X28)))))))|~(![X13:$i, X14:$i, X26:$i]:((~((X34 @ X13 @ X14))|~((X34 @ X14 @ X26))|(X34 @ X13 @ X26))))|~(![X15:$i, X16:$i]:((~((X89 @ X15 @ X16))|(X34 @ X15 @ X16))))|(X34 @ X8 @ X12)|~(![X13:$i, X14:$i, X27:$i]:((~((X35 @ X13 @ X14))|~((X35 @ X14 @ X27))|(X35 @ X13 @ X27))))|~(![X15:$i, X16:$i]:((~((X89 @ X15 @ X16))|(X35 @ X15 @ X16))))))), introduced(definition)).
% 0.82/0.41 thf(c_0_7, plain, ![X7:$i, X8:$i, X90:$i > $i > $o, X37:$i > $i > $o]:(((epred9_4 @ X37 @ X90 @ X8 @ X7)<=>(((((X7)!=(X8))&~(![X6:$i > $i > $o]:((~(![X13:$i, X14:$i, X12:$i]:((~((X6 @ X13 @ X14))|~((X6 @ X14 @ X12))|(X6 @ X13 @ X12))))|~(![X15:$i, X16:$i]:((~((X90 @ X15 @ X16))|(X6 @ X15 @ X16))))|(X6 @ X8 @ X7)))))&~(![X6:$i > $i > $o]:((~(![X13:$i, X14:$i, X12:$i]:((~((X6 @ X13 @ X14))|~((X6 @ X14 @ X12))|(X6 @ X13 @ X12))))|~(![X15:$i, X16:$i]:((~((X90 @ X15 @ X16))|(X6 @ X15 @ X16))))|(X6 @ X7 @ X8)))))|((X7)=(X8))|~(![X28:$i]:((~(![X6:$i > $i > $o]:((~(![X13:$i, X14:$i, X26:$i]:((~((X6 @ X13 @ X14))|~((X6 @ X14 @ X26))|(X6 @ X13 @ X26))))|~(![X15:$i, X16:$i]:((~((X90 @ X15 @ X16))|(X6 @ X15 @ X16))))|(X6 @ X8 @ X28))))|~(![X6:$i > $i > $o]:((~(![X13:$i, X14:$i, X27:$i]:((~((X6 @ X13 @ X14))|~((X6 @ X14 @ X27))|(X6 @ X13 @ X27))))|~(![X15:$i, X16:$i]:((~((X90 @ X15 @ X16))|(X6 @ X15 @ X16))))|(X6 @ X7 @ X28)))))))|~(![X13:$i, X14:$i, X26:$i]:((~((X37 @ X13 @ X14))|~((X37 @ X14 @ X26))|(X37 @ X13 @ X26))))))), introduced(definition)).
% 0.82/0.41 thf(c_0_8, plain, (((((((((((((((((((((((((((((((![X1:$i]:(?[X2:d_unsorted]:(((X1)=(d2unsorted @ X2))))&![X2:d_unsorted]:(((X2)=(d_unsorted_0))))&![X3:d_unsorted, X4:d_unsorted]:((((d2unsorted @ X3)=(d2unsorted @ X4))=>((X3)=(X4)))))&![X44:$i > $i > $o, X45:$i > $i > $o]:(((subrel @ X44 @ X45)<=>![X7:$i, X8:$i]:((~((X44 @ X7 @ X8))|(X45 @ X7 @ X8))))))&![X46:$i > $i > $o, X47:$i, X48:$i]:(((inv @ X46 @ X47 @ X48)<=>(X46 @ X48 @ X47))))&![X49:($i > $i > $o) > $i > $i > $o]:(((idem @ X49)<=>![X5:$i > $i > $o]:(((X49 @ X5)=(X49 @ (X49 @ X5)))))))&![X50:($i > $i > $o) > $i > $i > $o]:(((infl @ X50)<=>![X5:$i > $i > $o, X7:$i, X8:$i]:((~((X5 @ X7 @ X8))|(X50 @ X5 @ X7 @ X8))))))&![X51:($i > $i > $o) > $i > $i > $o]:(((mono @ X51)<=>![X5:$i > $i > $o, X6:$i > $i > $o, X10:$i, X11:$i]:((~(![X7:$i, X8:$i]:((~((X5 @ X7 @ X8))|(X6 @ X7 @ X8))))|~((X51 @ X5 @ X10 @ X11))|(X51 @ X6 @ X10 @ X11))))))&![X52:$i > $i > $o]:(((refl @ X52)<=>![X7:$i]:((X52 @ X7 @ X7)))))&![X53:$i > $i > $o]:(((irrefl @ X53)<=>![X7:$i]:(~((X53 @ X7 @ X7))))))&![X54:$i > $i > $o, X55:$i, X56:$i]:(((rc @ X54 @ X55 @ X56)<=>(((X55)=(X56))|(X54 @ X55 @ X56)))))&![X57:$i > $i > $o]:(((symm @ X57)<=>![X7:$i, X8:$i]:((~((X57 @ X7 @ X8))|(X57 @ X8 @ X7))))))&![X58:$i > $i > $o]:(((antisymm @ X58)<=>![X7:$i, X8:$i]:((~((X58 @ X7 @ X8))|~((X58 @ X8 @ X7))|((X7)=(X8)))))))&![X59:$i > $i > $o]:(((asymm @ X59)<=>![X7:$i, X8:$i]:((~((X59 @ X7 @ X8))|~((X59 @ X8 @ X7)))))))&![X60:$i > $i > $o, X61:$i, X62:$i]:(((sc @ X60 @ X61 @ X62)<=>((X60 @ X62 @ X61)|(X60 @ X61 @ X62)))))&![X63:$i > $i > $o]:(((trans @ X63)<=>![X7:$i, X8:$i, X12:$i]:((~((X63 @ X7 @ X8))|~((X63 @ X8 @ X12))|(X63 @ X7 @ X12))))))&![X64:$i > $i > $o, X65:$i, X66:$i]:(((tc @ X64 @ X65 @ X66)<=>![X6:$i > $i > $o]:((~(![X13:$i, X14:$i, X12:$i]:((~((X6 @ X13 @ X14))|~((X6 @ X14 @ X12))|(X6 @ X13 @ X12))))|~(![X15:$i, X16:$i]:((~((X64 @ X15 @ X16))|(X6 @ X15 @ X16))))|(X6 @ X65 @ X66))))))&![X67:$i > $i > $o, X68:$i, X69:$i]:(((trc @ X67 @ X68 @ X69)<=>(((X68)=(X69))|![X6:$i > $i > $o]:((~(![X13:$i, X14:$i, X12:$i]:((~((X6 @ X13 @ X14))|~((X6 @ X14 @ X12))|(X6 @ X13 @ X12))))|~(![X15:$i, X16:$i]:((~((X67 @ X15 @ X16))|(X6 @ X15 @ X16))))|(X6 @ X68 @ X69)))))))&![X70:$i > $i > $o, X71:$i, X72:$i]:(((trsc @ X70 @ X71 @ X72)<=>(epred1_3 @ X72 @ X71 @ X70))))&![X73:$i > $i > $o]:(((po @ X73)<=>((![X7:$i]:((X73 @ X7 @ X7))&![X7:$i, X8:$i]:((~((X73 @ X7 @ X8))|~((X73 @ X8 @ X7))|((X7)=(X8)))))&![X7:$i, X8:$i, X12:$i]:((~((X73 @ X7 @ X8))|~((X73 @ X8 @ X12))|(X73 @ X7 @ X12)))))))&![X74:$i > $i > $o]:(((so @ X74)<=>(![X7:$i, X8:$i]:((~((X74 @ X7 @ X8))|~((X74 @ X8 @ X7))))&![X7:$i, X8:$i, X12:$i]:((~((X74 @ X7 @ X8))|~((X74 @ X8 @ X12))|(X74 @ X7 @ X12)))))))&![X75:$i > $i > $o]:(((total @ X75)<=>![X7:$i, X8:$i]:((((X7)=(X8))|(X75 @ X7 @ X8)|(X75 @ X8 @ X7))))))&![X76:$i > $i > $o]:(((term @ X76)<=>![X19:$i > $o, X20:$i]:((~((X19 @ X20))|~(![X7:$i]:((~((X19 @ X7))|~(![X8:$i]:((~((X19 @ X8))|~((X76 @ X7 @ X8)))))))))))))&![X77:$i > $i > $o]:(((ind @ X77)<=>![X21:$i > $o, X22:$i]:((~(![X7:$i]:((~(![X8:$i]:((~(![X6:$i > $i > $o]:((~(![X13:$i, X14:$i, X12:$i]:((~((X6 @ X13 @ X14))|~((X6 @ X14 @ X12))|(X6 @ X13 @ X12))))|~(![X15:$i, X16:$i]:((~((X77 @ X15 @ X16))|(X6 @ X15 @ X16))))|(X6 @ X7 @ X8))))|(X21 @ X8))))|(X21 @ X7))))|(X21 @ X22))))))&![X78:$i > $i > $o, X79:$i]:(((innf @ X78 @ X79)<=>![X8:$i]:(~((X78 @ X79 @ X8))))))&![X80:$i > $i > $o, X81:$i, X82:$i]:(((nfof @ X80 @ X81 @ X82)<=>((((X81)=(X82))|![X6:$i > $i > $o]:((~(![X13:$i, X14:$i, X12:$i]:((~((X6 @ X13 @ X14))|~((X6 @ X14 @ X12))|(X6 @ X13 @ X12))))|~(![X15:$i, X16:$i]:((~((X80 @ X15 @ X16))|(X6 @ X15 @ X16))))|(X6 @ X82 @ X81))))&![X23:$i]:(~((X80 @ X81 @ X23)))))))&![X83:$i > $i > $o]:(((norm @ X83)<=>![X7:$i, X24:$i]:((~((X83 @ X7 @ X24))|~(![X25:$i]:((~(![X6:$i > $i > $o]:((~(![X13:$i, X14:$i, X12:$i]:((~((X6 @ X13 @ X14))|~((X6 @ X14 @ X12))|(X6 @ X13 @ X12))))|~(![X15:$i, X16:$i]:((~((X83 @ X15 @ X16))|(X6 @ X15 @ X16))))|(X6 @ X7 @ X25))))|~(![X23:$i]:(~((X83 @ X25 @ X23))))))))))))&![X84:$i > $i > $o, X85:$i, X86:$i]:(((join @ X84 @ X85 @ X86)<=>~(((epred2_3 @ X86 @ X85 @ X84)&![X28:$i]:((~(![X6:$i > $i > $o]:((~(![X13:$i, X14:$i, X26:$i]:((~((X6 @ X13 @ X14))|~((X6 @ X14 @ X26))|(X6 @ X13 @ X26))))|~(![X15:$i, X16:$i]:((~((X84 @ X15 @ X16))|(X6 @ X15 @ X16))))|(X6 @ X86 @ X28))))|~(![X6:$i > $i > $o]:((~(![X13:$i, X14:$i, X27:$i]:((~((X6 @ X13 @ X14))|~((X6 @ X14 @ X27))|(X6 @ X13 @ X27))))|~(![X15:$i, X16:$i]:((~((X84 @ X15 @ X16))|(X6 @ X15 @ X16))))|(X6 @ X85 @ X28)))))))))))&![X87:$i > $i > $o]:(((lconfl @ X87)<=>![X7:$i, X8:$i, X12:$i, X29:$i > $i > $o, X30:$i > $i > $o]:(((epred3_5 @ X29 @ X87 @ X12 @ X8 @ X7)|~(![X15:$i, X16:$i]:((~((X87 @ X15 @ X16))|(X29 @ X15 @ X16))))|(X29 @ X8 @ X12)|~(![X13:$i, X14:$i, X27:$i]:((~((X30 @ X13 @ X14))|~((X30 @ X14 @ X27))|(X30 @ X13 @ X27))))|~(![X15:$i, X16:$i]:((~((X87 @ X15 @ X16))|(X30 @ X15 @ X16))))|(X30 @ X12 @ X8))))))&![X88:$i > $i > $o]:(((sconfl @ X88)<=>![X7:$i, X8:$i, X12:$i, X31:$i > $i > $o, X32:$i > $i > $o]:(((epred5_6 @ X32 @ X88 @ X31 @ X12 @ X8 @ X7)|(X32 @ X12 @ X8))))))&![X89:$i > $i > $o]:(((confl @ X89)<=>![X7:$i, X8:$i, X12:$i, X34:$i > $i > $o, X35:$i > $i > $o]:(((epred7_6 @ X35 @ X89 @ X34 @ X12 @ X8 @ X7)|(X35 @ X12 @ X8))))))&![X90:$i > $i > $o]:(((cr @ X90)<=>![X7:$i, X8:$i, X37:$i > $i > $o, X38:$i > $i > $o]:(((epred9_4 @ X37 @ X90 @ X8 @ X7)|~(![X15:$i, X16:$i]:((~((X90 @ X15 @ X16))|(X37 @ X15 @ X16))))|(X37 @ X8 @ X7)|~(![X13:$i, X14:$i, X27:$i]:((~((X38 @ X13 @ X14))|~((X38 @ X14 @ X27))|(X38 @ X13 @ X27))))|~(![X15:$i, X16:$i]:((~((X90 @ X15 @ X16))|(X38 @ X15 @ X16))))|(X38 @ X7 @ X8)))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[sev441_1])])]), c_0_2]), c_0_3]), c_0_4]), c_0_5]), c_0_6]), c_0_7])).
% 0.82/0.41 thf(c_0_9, plain, ![X92:$i, X94:d_unsorted, X95:d_unsorted, X96:d_unsorted, X97:$i > $i > $o, X98:$i > $i > $o, X99:$i, X100:$i, X101:$i > $i > $o, X102:$i > $i > $o, X105:$i > $i > $o, X106:$i, X107:$i, X108:($i > $i > $o) > $i > $i > $o, X109:$i > $i > $o, X110:($i > $i > $o) > $i > $i > $o, X112:($i > $i > $o) > $i > $i > $o, X113:$i > $i > $o, X114:$i, X115:$i, X116:($i > $i > $o) > $i > $i > $o, X120:($i > $i > $o) > $i > $i > $o, X121:$i > $i > $o, X122:$i > $i > $o, X123:$i, X124:$i, X127:($i > $i > $o) > $i > $i > $o, X132:$i, X133:$i, X134:$i > $i > $o, X135:$i, X136:$i > $i > $o, X138:$i > $i > $o, X139:$i, X140:$i > $i > $o, X142:$i > $i > $o, X143:$i, X144:$i, X145:$i > $i > $o, X146:$i, X147:$i, X148:$i > $i > $o, X151:$i > $i > $o, X152:$i, X153:$i, X154:$i > $i > $o, X157:$i > $i > $o, X158:$i, X159:$i, X160:$i > $i > $o, X163:$i > $i > $o, X164:$i, X165:$i, X166:$i > $i > $o, X167:$i, X168:$i, X169:$i, X170:$i > $i > $o, X174:$i > $i > $o, X175:$i, X176:$i, X177:$i > $i > $o, X183:$i > $i > $o, X184:$i, X185:$i, X187:$i, X188:$i, X189:$i, X190:$i, X191:$i, X192:$i > $i > $o, X193:$i, X194:$i, X195:$i > $i > $o, X201:$i > $i > $o, X202:$i, X203:$i, X205:$i, X206:$i, X207:$i, X208:$i, X209:$i, X210:$i > $i > $o, X211:$i, X212:$i, X213:$i > $i > $o, X214:$i, X215:$i, X216:$i, X217:$i, X218:$i, X219:$i, X220:$i > $i > $o, X227:$i > $i > $o, X228:$i, X229:$i, X230:$i, X231:$i, X232:$i, X233:$i > $i > $o, X239:$i > $i > $o, X240:$i, X241:$i, X242:$i > $i > $o, X245:$i > $i > $o, X246:$i > $o, X247:$i, X249:$i, X250:$i > $i > $o, X253:$i, X255:$i > $i > $o, X256:$i > $o, X258:$i, X260:$i, X261:$i, X262:$i, X263:$i, X264:$i, X265:$i, X266:$i > $i > $o, X268:$i, X270:$i > $i > $o, X277:$i > $i > $o, X278:$i, X279:$i, X280:$i > $i > $o, X281:$i, X283:$i > $i > $o, X284:$i, X285:$i, X286:$i > $i > $o, X292:$i, X293:$i > $i > $o, X294:$i, X295:$i, X297:$i, X298:$i, X299:$i, X300:$i, X301:$i, X303:$i > $i > $o, X304:$i, X305:$i, X307:$i > $i > $o, X313:$i, X314:$i > $i > $o, X317:$i, X319:$i, X320:$i, X321:$i, X322:$i, X323:$i, X325:$i > $i > $o, X326:$i, X327:$i, X329:$i > $i > $o, X335:$i > $i > $o, X341:$i > $i > $o, X342:$i, X343:$i, X344:$i, X346:$i, X347:$i, X348:$i, X349:$i, X350:$i, X352:$i, X353:$i, X354:$i, X355:$i, X356:$i, X357:$i > $i > $o, X358:$i, X359:$i, X360:$i, X361:$i > $i > $o, X362:$i > $i > $o, X370:$i > $i > $o, X376:$i, X377:$i, X378:$i, X379:$i, X380:$i, X381:$i, X382:$i, X383:$i > $i > $o, X384:$i, X385:$i, X386:$i, X387:$i > $i > $o, X388:$i > $i > $o, X389:$i > $i > $o, X395:$i > $i > $o, X396:$i, X397:$i, X398:$i, X399:$i > $i > $o, X400:$i > $i > $o, X401:$i > $i > $o, X407:$i > $i > $o, X408:$i, X409:$i, X410:$i > $i > $o, X411:$i > $i > $o, X419:$i > $i > $o, X424:$i, X425:$i, X426:$i, X427:$i, X428:$i, X429:$i, X430:$i]:((((((((((((((((((((((((((((((((((X92)=(d2unsorted @ (esk1_1 @ X92)))&((X94)=(d_unsorted_0)))&(((d2unsorted @ X95)!=(d2unsorted @ X96))|((X95)=(X96))))&((~(subrel @ X97 @ X98)|(~(X97 @ X99 @ X100)|(X98 @ X99 @ X100)))&(((X101 @ (esk2_2 @ X101 @ X102) @ (esk3_2 @ X101 @ X102))|(subrel @ X101 @ X102))&(~(X102 @ (esk2_2 @ X101 @ X102) @ (esk3_2 @ X101 @ X102))|(subrel @ X101 @ X102)))))&((~(inv @ X105 @ X106 @ X107)|(X105 @ X107 @ X106))&(~(X105 @ X107 @ X106)|(inv @ X105 @ X106 @ X107))))&((~(idem @ X108)|((X108 @ X109)=(X108 @ (X108 @ X109))))&(((X110 @ (epred10_1 @ X110))!=(X110 @ (X110 @ (epred10_1 @ X110))))|(idem @ X110))))&((~(infl @ X112)|(~(X113 @ X114 @ X115)|(X112 @ X113 @ X114 @ X115)))&(((epred11_1 @ X116 @ (esk4_1 @ X116) @ (esk5_1 @ X116))|(infl @ X116))&(~(X116 @ (epred11_1 @ X116) @ (esk4_1 @ X116) @ (esk5_1 @ X116))|(infl @ X116)))))&((((X121 @ (esk6_5 @ X120 @ X121 @ X122 @ X123 @ X124) @ (esk7_5 @ X120 @ X121 @ X122 @ X123 @ X124))|~(X120 @ X121 @ X123 @ X124)|(X120 @ X122 @ X123 @ X124)|~(mono @ X120))&(~(X122 @ (esk6_5 @ X120 @ X121 @ X122 @ X123 @ X124) @ (esk7_5 @ X120 @ X121 @ X122 @ X123 @ X124))|~(X120 @ X121 @ X123 @ X124)|(X120 @ X122 @ X123 @ X124)|~(mono @ X120)))&(((~(epred12_1 @ X127 @ X132 @ X133)|(epred13_1 @ X127 @ X132 @ X133)|(mono @ X127))&((X127 @ (epred12_1 @ X127) @ (esk8_1 @ X127) @ (esk9_1 @ X127))|(mono @ X127)))&(~(X127 @ (epred13_1 @ X127) @ (esk8_1 @ X127) @ (esk9_1 @ X127))|(mono @ X127)))))&((~(refl @ X134)|(X134 @ X135 @ X135))&(~(X136 @ (esk10_1 @ X136) @ (esk10_1 @ X136))|(refl @ X136))))&((~(irrefl @ X138)|~(X138 @ X139 @ X139))&((X140 @ (esk11_1 @ X140) @ (esk11_1 @ X140))|(irrefl @ X140))))&((~(rc @ X142 @ X143 @ X144)|(((X143)=(X144))|(X142 @ X143 @ X144)))&((((X143)!=(X144))|(rc @ X142 @ X143 @ X144))&(~(X142 @ X143 @ X144)|(rc @ X142 @ X143 @ X144)))))&((~(symm @ X145)|(~(X145 @ X146 @ X147)|(X145 @ X147 @ X146)))&(((X148 @ (esk12_1 @ X148) @ (esk13_1 @ X148))|(symm @ X148))&(~(X148 @ (esk13_1 @ X148) @ (esk12_1 @ X148))|(symm @ X148)))))&((~(antisymm @ X151)|(~(X151 @ X152 @ X153)|~(X151 @ X153 @ X152)|((X152)=(X153))))&((((X154 @ (esk14_1 @ X154) @ (esk15_1 @ X154))|(antisymm @ X154))&((X154 @ (esk15_1 @ X154) @ (esk14_1 @ X154))|(antisymm @ X154)))&(((esk14_1 @ X154)!=(esk15_1 @ X154))|(antisymm @ X154)))))&((~(asymm @ X157)|(~(X157 @ X158 @ X159)|~(X157 @ X159 @ X158)))&(((X160 @ (esk16_1 @ X160) @ (esk17_1 @ X160))|(asymm @ X160))&((X160 @ (esk17_1 @ X160) @ (esk16_1 @ X160))|(asymm @ X160)))))&((~(sc @ X163 @ X164 @ X165)|((X163 @ X165 @ X164)|(X163 @ X164 @ X165)))&((~(X163 @ X165 @ X164)|(sc @ X163 @ X164 @ X165))&(~(X163 @ X164 @ X165)|(sc @ X163 @ X164 @ X165)))))&((~(trans @ X166)|(~(X166 @ X167 @ X168)|~(X166 @ X168 @ X169)|(X166 @ X167 @ X169)))&((((X170 @ (esk18_1 @ X170) @ (esk19_1 @ X170))|(trans @ X170))&((X170 @ (esk19_1 @ X170) @ (esk20_1 @ X170))|(trans @ X170)))&(~(X170 @ (esk18_1 @ X170) @ (esk20_1 @ X170))|(trans @ X170)))))&((((((X174 @ (esk24_4 @ X174 @ X175 @ X176 @ X177) @ (esk25_4 @ X174 @ X175 @ X176 @ X177))|(X177 @ (esk21_4 @ X174 @ X175 @ X176 @ X177) @ (esk22_4 @ X174 @ X175 @ X176 @ X177))|(X177 @ X175 @ X176)|~(tc @ X174 @ X175 @ X176))&(~(X177 @ (esk24_4 @ X174 @ X175 @ X176 @ X177) @ (esk25_4 @ X174 @ X175 @ X176 @ X177))|(X177 @ (esk21_4 @ X174 @ X175 @ X176 @ X177) @ (esk22_4 @ X174 @ X175 @ X176 @ X177))|(X177 @ X175 @ X176)|~(tc @ X174 @ X175 @ X176)))&(((X174 @ (esk24_4 @ X174 @ X175 @ X176 @ X177) @ (esk25_4 @ X174 @ X175 @ X176 @ X177))|(X177 @ (esk22_4 @ X174 @ X175 @ X176 @ X177) @ (esk23_4 @ X174 @ X175 @ X176 @ X177))|(X177 @ X175 @ X176)|~(tc @ X174 @ X175 @ X176))&(~(X177 @ (esk24_4 @ X174 @ X175 @ X176 @ X177) @ (esk25_4 @ X174 @ X175 @ X176 @ X177))|(X177 @ (esk22_4 @ X174 @ X175 @ X176 @ X177) @ (esk23_4 @ X174 @ X175 @ X176 @ X177))|(X177 @ X175 @ X176)|~(tc @ X174 @ X175 @ X176))))&(((X174 @ (esk24_4 @ X174 @ X175 @ X176 @ X177) @ (esk25_4 @ X174 @ X175 @ X176 @ X177))|~(X177 @ (esk21_4 @ X174 @ X175 @ X176 @ X177) @ (esk23_4 @ X174 @ X175 @ X176 @ X177))|(X177 @ X175 @ X176)|~(tc @ X174 @ X175 @ X176))&(~(X177 @ (esk24_4 @ X174 @ X175 @ X176 @ X177) @ (esk25_4 @ X174 @ X175 @ X176 @ X177))|~(X177 @ (esk21_4 @ X174 @ X175 @ X176 @ X177) @ (esk23_4 @ X174 @ X175 @ X176 @ X177))|(X177 @ X175 @ X176)|~(tc @ X174 @ X175 @ X176))))&(((~(epred14_3 @ X183 @ X184 @ X185 @ X187 @ X188)|~(epred14_3 @ X183 @ X184 @ X185 @ X188 @ X189)|(epred14_3 @ X183 @ X184 @ X185 @ X187 @ X189)|(tc @ X183 @ X184 @ X185))&(~(X183 @ X190 @ X191)|(epred14_3 @ X183 @ X184 @ X185 @ X190 @ X191)|(tc @ X183 @ X184 @ X185)))&(~(epred14_3 @ X183 @ X184 @ X185 @ X184 @ X185)|(tc @ X183 @ X184 @ X185)))))&((((((X192 @ (esk29_4 @ X192 @ X193 @ X194 @ X195) @ (esk30_4 @ X192 @ X193 @ X194 @ X195))|(X195 @ (esk26_4 @ X192 @ X193 @ X194 @ X195) @ (esk27_4 @ X192 @ X193 @ X194 @ X195))|(X195 @ X193 @ X194)|((X193)=(X194))|~(trc @ X192 @ X193 @ X194))&(~(X195 @ (esk29_4 @ X192 @ X193 @ X194 @ X195) @ (esk30_4 @ X192 @ X193 @ X194 @ X195))|(X195 @ (esk26_4 @ X192 @ X193 @ X194 @ X195) @ (esk27_4 @ X192 @ X193 @ X194 @ X195))|(X195 @ X193 @ X194)|((X193)=(X194))|~(trc @ X192 @ X193 @ X194)))&(((X192 @ (esk29_4 @ X192 @ X193 @ X194 @ X195) @ (esk30_4 @ X192 @ X193 @ X194 @ X195))|(X195 @ (esk27_4 @ X192 @ X193 @ X194 @ X195) @ (esk28_4 @ X192 @ X193 @ X194 @ X195))|(X195 @ X193 @ X194)|((X193)=(X194))|~(trc @ X192 @ X193 @ X194))&(~(X195 @ (esk29_4 @ X192 @ X193 @ X194 @ X195) @ (esk30_4 @ X192 @ X193 @ X194 @ X195))|(X195 @ (esk27_4 @ X192 @ X193 @ X194 @ X195) @ (esk28_4 @ X192 @ X193 @ X194 @ X195))|(X195 @ X193 @ X194)|((X193)=(X194))|~(trc @ X192 @ X193 @ X194))))&(((X192 @ (esk29_4 @ X192 @ X193 @ X194 @ X195) @ (esk30_4 @ X192 @ X193 @ X194 @ X195))|~(X195 @ (esk26_4 @ X192 @ X193 @ X194 @ X195) @ (esk28_4 @ X192 @ X193 @ X194 @ X195))|(X195 @ X193 @ X194)|((X193)=(X194))|~(trc @ X192 @ X193 @ X194))&(~(X195 @ (esk29_4 @ X192 @ X193 @ X194 @ X195) @ (esk30_4 @ X192 @ X193 @ X194 @ X195))|~(X195 @ (esk26_4 @ X192 @ X193 @ X194 @ X195) @ (esk28_4 @ X192 @ X193 @ X194 @ X195))|(X195 @ X193 @ X194)|((X193)=(X194))|~(trc @ X192 @ X193 @ X194))))&((((X202)!=(X203))|(trc @ X201 @ X202 @ X203))&(((~(epred15_3 @ X201 @ X202 @ X203 @ X205 @ X206)|~(epred15_3 @ X201 @ X202 @ X203 @ X206 @ X207)|(epred15_3 @ X201 @ X202 @ X203 @ X205 @ X207)|(trc @ X201 @ X202 @ X203))&(~(X201 @ X208 @ X209)|(epred15_3 @ X201 @ X202 @ X203 @ X208 @ X209)|(trc @ X201 @ X202 @ X203)))&(~(epred15_3 @ X201 @ X202 @ X203 @ X202 @ X203)|(trc @ X201 @ X202 @ X203))))))&((~(trsc @ X210 @ X211 @ X212)|(epred1_3 @ X212 @ X211 @ X210))&(~(epred1_3 @ X212 @ X211 @ X210)|(trsc @ X210 @ X211 @ X212))))&(((((X213 @ X214 @ X214)|~(po @ X213))&(~(X213 @ X215 @ X216)|~(X213 @ X216 @ X215)|((X215)=(X216))|~(po @ X213)))&(~(X213 @ X217 @ X218)|~(X213 @ X218 @ X219)|(X213 @ X217 @ X219)|~(po @ X213)))&((((((X220 @ (esk34_1 @ X220) @ (esk35_1 @ X220))|((X220 @ (esk32_1 @ X220) @ (esk33_1 @ X220))|~(X220 @ (esk31_1 @ X220) @ (esk31_1 @ X220)))|(po @ X220))&((X220 @ (esk35_1 @ X220) @ (esk36_1 @ X220))|((X220 @ (esk32_1 @ X220) @ (esk33_1 @ X220))|~(X220 @ (esk31_1 @ X220) @ (esk31_1 @ X220)))|(po @ X220)))&(~(X220 @ (esk34_1 @ X220) @ (esk36_1 @ X220))|((X220 @ (esk32_1 @ X220) @ (esk33_1 @ X220))|~(X220 @ (esk31_1 @ X220) @ (esk31_1 @ X220)))|(po @ X220)))&((((X220 @ (esk34_1 @ X220) @ (esk35_1 @ X220))|((X220 @ (esk33_1 @ X220) @ (esk32_1 @ X220))|~(X220 @ (esk31_1 @ X220) @ (esk31_1 @ X220)))|(po @ X220))&((X220 @ (esk35_1 @ X220) @ (esk36_1 @ X220))|((X220 @ (esk33_1 @ X220) @ (esk32_1 @ X220))|~(X220 @ (esk31_1 @ X220) @ (esk31_1 @ X220)))|(po @ X220)))&(~(X220 @ (esk34_1 @ X220) @ (esk36_1 @ X220))|((X220 @ (esk33_1 @ X220) @ (esk32_1 @ X220))|~(X220 @ (esk31_1 @ X220) @ (esk31_1 @ X220)))|(po @ X220))))&((((X220 @ (esk34_1 @ X220) @ (esk35_1 @ X220))|(((esk32_1 @ X220)!=(esk33_1 @ X220))|~(X220 @ (esk31_1 @ X220) @ (esk31_1 @ X220)))|(po @ X220))&((X220 @ (esk35_1 @ X220) @ (esk36_1 @ X220))|(((esk32_1 @ X220)!=(esk33_1 @ X220))|~(X220 @ (esk31_1 @ X220) @ (esk31_1 @ X220)))|(po @ X220)))&(~(X220 @ (esk34_1 @ X220) @ (esk36_1 @ X220))|(((esk32_1 @ X220)!=(esk33_1 @ X220))|~(X220 @ (esk31_1 @ X220) @ (esk31_1 @ X220)))|(po @ X220))))))&(((~(X227 @ X228 @ X229)|~(X227 @ X229 @ X228)|~(so @ X227))&(~(X227 @ X230 @ X231)|~(X227 @ X231 @ X232)|(X227 @ X230 @ X232)|~(so @ X227)))&(((((X233 @ (esk39_1 @ X233) @ (esk40_1 @ X233))|(X233 @ (esk37_1 @ X233) @ (esk38_1 @ X233))|(so @ X233))&((X233 @ (esk40_1 @ X233) @ (esk41_1 @ X233))|(X233 @ (esk37_1 @ X233) @ (esk38_1 @ X233))|(so @ X233)))&(~(X233 @ (esk39_1 @ X233) @ (esk41_1 @ X233))|(X233 @ (esk37_1 @ X233) @ (esk38_1 @ X233))|(so @ X233)))&((((X233 @ (esk39_1 @ X233) @ (esk40_1 @ X233))|(X233 @ (esk38_1 @ X233) @ (esk37_1 @ X233))|(so @ X233))&((X233 @ (esk40_1 @ X233) @ (esk41_1 @ X233))|(X233 @ (esk38_1 @ X233) @ (esk37_1 @ X233))|(so @ X233)))&(~(X233 @ (esk39_1 @ X233) @ (esk41_1 @ X233))|(X233 @ (esk38_1 @ X233) @ (esk37_1 @ X233))|(so @ X233))))))&((~(total @ X239)|(((X240)=(X241))|(X239 @ X240 @ X241)|(X239 @ X241 @ X240)))&(((((esk42_1 @ X242)!=(esk43_1 @ X242))|(total @ X242))&(~(X242 @ (esk42_1 @ X242) @ (esk43_1 @ X242))|(total @ X242)))&(~(X242 @ (esk43_1 @ X242) @ (esk42_1 @ X242))|(total @ X242)))))&((((X246 @ (esk44_2 @ X245 @ X246))|~(X246 @ X247)|~(term @ X245))&(~(X246 @ X249)|~(X245 @ (esk44_2 @ X245 @ X246) @ X249)|~(X246 @ X247)|~(term @ X245)))&(((epred16_1 @ X250 @ (esk45_1 @ X250))|(term @ X250))&(((epred16_1 @ X250 @ (esk46_2 @ X250 @ X253))|~(epred16_1 @ X250 @ X253)|(term @ X250))&((X250 @ X253 @ (esk46_2 @ X250 @ X253))|~(epred16_1 @ X250 @ X253)|(term @ X250))))))&(((((~(epred17_3 @ X255 @ X256 @ X258 @ X260 @ X261)|~(epred17_3 @ X255 @ X256 @ X258 @ X261 @ X262)|(epred17_3 @ X255 @ X256 @ X258 @ X260 @ X262)|(X256 @ X258)|(X256 @ X265)|~(ind @ X255))&(~(X255 @ X263 @ X264)|(epred17_3 @ X255 @ X256 @ X258 @ X263 @ X264)|(X256 @ X258)|(X256 @ X265)|~(ind @ X255)))&(~(epred17_3 @ X255 @ X256 @ X258 @ (esk47_2 @ X255 @ X256) @ X258)|(X256 @ X258)|(X256 @ X265)|~(ind @ X255)))&(~(X256 @ (esk47_2 @ X255 @ X256))|(X256 @ X265)|~(ind @ X255)))&(((((((X266 @ (esk52_3 @ X266 @ X268 @ X270) @ (esk53_3 @ X266 @ X268 @ X270))|(X270 @ (esk49_3 @ X266 @ X268 @ X270) @ (esk50_3 @ X266 @ X268 @ X270))|(X270 @ X268 @ (esk48_2 @ X266 @ X268))|(epred18_1 @ X266 @ X268)|(ind @ X266))&(~(X270 @ (esk52_3 @ X266 @ X268 @ X270) @ (esk53_3 @ X266 @ X268 @ X270))|(X270 @ (esk49_3 @ X266 @ X268 @ X270) @ (esk50_3 @ X266 @ X268 @ X270))|(X270 @ X268 @ (esk48_2 @ X266 @ X268))|(epred18_1 @ X266 @ X268)|(ind @ X266)))&(((X266 @ (esk52_3 @ X266 @ X268 @ X270) @ (esk53_3 @ X266 @ X268 @ X270))|(X270 @ (esk50_3 @ X266 @ X268 @ X270) @ (esk51_3 @ X266 @ X268 @ X270))|(X270 @ X268 @ (esk48_2 @ X266 @ X268))|(epred18_1 @ X266 @ X268)|(ind @ X266))&(~(X270 @ (esk52_3 @ X266 @ X268 @ X270) @ (esk53_3 @ X266 @ X268 @ X270))|(X270 @ (esk50_3 @ X266 @ X268 @ X270) @ (esk51_3 @ X266 @ X268 @ X270))|(X270 @ X268 @ (esk48_2 @ X266 @ X268))|(epred18_1 @ X266 @ X268)|(ind @ X266))))&(((X266 @ (esk52_3 @ X266 @ X268 @ X270) @ (esk53_3 @ X266 @ X268 @ X270))|~(X270 @ (esk49_3 @ X266 @ X268 @ X270) @ (esk51_3 @ X266 @ X268 @ X270))|(X270 @ X268 @ (esk48_2 @ X266 @ X268))|(epred18_1 @ X266 @ X268)|(ind @ X266))&(~(X270 @ (esk52_3 @ X266 @ X268 @ X270) @ (esk53_3 @ X266 @ X268 @ X270))|~(X270 @ (esk49_3 @ X266 @ X268 @ X270) @ (esk51_3 @ X266 @ X268 @ X270))|(X270 @ X268 @ (esk48_2 @ X266 @ X268))|(epred18_1 @ X266 @ X268)|(ind @ X266))))&(~(epred18_1 @ X266 @ (esk48_2 @ X266 @ X268))|(epred18_1 @ X266 @ X268)|(ind @ X266)))&(~(epred18_1 @ X266 @ (esk54_1 @ X266))|(ind @ X266)))))&((~(innf @ X277 @ X278)|~(X277 @ X278 @ X279))&((X280 @ X281 @ (esk55_2 @ X280 @ X281))|(innf @ X280 @ X281))))&(((((((X283 @ (esk59_4 @ X283 @ X284 @ X285 @ X286) @ (esk60_4 @ X283 @ X284 @ X285 @ X286))|(X286 @ (esk56_4 @ X283 @ X284 @ X285 @ X286) @ (esk57_4 @ X283 @ X284 @ X285 @ X286))|(X286 @ X285 @ X284)|((X284)=(X285))|~(nfof @ X283 @ X284 @ X285))&(~(X286 @ (esk59_4 @ X283 @ X284 @ X285 @ X286) @ (esk60_4 @ X283 @ X284 @ X285 @ X286))|(X286 @ (esk56_4 @ X283 @ X284 @ X285 @ X286) @ (esk57_4 @ X283 @ X284 @ X285 @ X286))|(X286 @ X285 @ X284)|((X284)=(X285))|~(nfof @ X283 @ X284 @ X285)))&(((X283 @ (esk59_4 @ X283 @ X284 @ X285 @ X286) @ (esk60_4 @ X283 @ X284 @ X285 @ X286))|(X286 @ (esk57_4 @ X283 @ X284 @ X285 @ X286) @ (esk58_4 @ X283 @ X284 @ X285 @ X286))|(X286 @ X285 @ X284)|((X284)=(X285))|~(nfof @ X283 @ X284 @ X285))&(~(X286 @ (esk59_4 @ X283 @ X284 @ X285 @ X286) @ (esk60_4 @ X283 @ X284 @ X285 @ X286))|(X286 @ (esk57_4 @ X283 @ X284 @ X285 @ X286) @ (esk58_4 @ X283 @ X284 @ X285 @ X286))|(X286 @ X285 @ X284)|((X284)=(X285))|~(nfof @ X283 @ X284 @ X285))))&(((X283 @ (esk59_4 @ X283 @ X284 @ X285 @ X286) @ (esk60_4 @ X283 @ X284 @ X285 @ X286))|~(X286 @ (esk56_4 @ X283 @ X284 @ X285 @ X286) @ (esk58_4 @ X283 @ X284 @ X285 @ X286))|(X286 @ X285 @ X284)|((X284)=(X285))|~(nfof @ X283 @ X284 @ X285))&(~(X286 @ (esk59_4 @ X283 @ X284 @ X285 @ X286) @ (esk60_4 @ X283 @ X284 @ X285 @ X286))|~(X286 @ (esk56_4 @ X283 @ X284 @ X285 @ X286) @ (esk58_4 @ X283 @ X284 @ X285 @ X286))|(X286 @ X285 @ X284)|((X284)=(X285))|~(nfof @ X283 @ X284 @ X285))))&(~(X283 @ X284 @ X292)|~(nfof @ X283 @ X284 @ X285)))&((((X294)!=(X295))|(X293 @ X294 @ (esk61_3 @ X293 @ X294 @ X295))|(nfof @ X293 @ X294 @ X295))&(((~(epred19_3 @ X293 @ X294 @ X295 @ X297 @ X298)|~(epred19_3 @ X293 @ X294 @ X295 @ X298 @ X299)|(epred19_3 @ X293 @ X294 @ X295 @ X297 @ X299)|(X293 @ X294 @ (esk61_3 @ X293 @ X294 @ X295))|(nfof @ X293 @ X294 @ X295))&(~(X293 @ X300 @ X301)|(epred19_3 @ X293 @ X294 @ X295 @ X300 @ X301)|(X293 @ X294 @ (esk61_3 @ X293 @ X294 @ X295))|(nfof @ X293 @ X294 @ X295)))&(~(epred19_3 @ X293 @ X294 @ X295 @ X295 @ X294)|(X293 @ X294 @ (esk61_3 @ X293 @ X294 @ X295))|(nfof @ X293 @ X294 @ X295))))))&(((((((X303 @ (esk66_3 @ X303 @ X304 @ X307) @ (esk67_3 @ X303 @ X304 @ X307))|(X307 @ (esk63_3 @ X303 @ X304 @ X307) @ (esk64_3 @ X303 @ X304 @ X307))|(X307 @ X304 @ (esk62_2 @ X303 @ X304))|~(X303 @ X304 @ X305)|~(norm @ X303))&(~(X307 @ (esk66_3 @ X303 @ X304 @ X307) @ (esk67_3 @ X303 @ X304 @ X307))|(X307 @ (esk63_3 @ X303 @ X304 @ X307) @ (esk64_3 @ X303 @ X304 @ X307))|(X307 @ X304 @ (esk62_2 @ X303 @ X304))|~(X303 @ X304 @ X305)|~(norm @ X303)))&(((X303 @ (esk66_3 @ X303 @ X304 @ X307) @ (esk67_3 @ X303 @ X304 @ X307))|(X307 @ (esk64_3 @ X303 @ X304 @ X307) @ (esk65_3 @ X303 @ X304 @ X307))|(X307 @ X304 @ (esk62_2 @ X303 @ X304))|~(X303 @ X304 @ X305)|~(norm @ X303))&(~(X307 @ (esk66_3 @ X303 @ X304 @ X307) @ (esk67_3 @ X303 @ X304 @ X307))|(X307 @ (esk64_3 @ X303 @ X304 @ X307) @ (esk65_3 @ X303 @ X304 @ X307))|(X307 @ X304 @ (esk62_2 @ X303 @ X304))|~(X303 @ X304 @ X305)|~(norm @ X303))))&(((X303 @ (esk66_3 @ X303 @ X304 @ X307) @ (esk67_3 @ X303 @ X304 @ X307))|~(X307 @ (esk63_3 @ X303 @ X304 @ X307) @ (esk65_3 @ X303 @ X304 @ X307))|(X307 @ X304 @ (esk62_2 @ X303 @ X304))|~(X303 @ X304 @ X305)|~(norm @ X303))&(~(X307 @ (esk66_3 @ X303 @ X304 @ X307) @ (esk67_3 @ X303 @ X304 @ X307))|~(X307 @ (esk63_3 @ X303 @ X304 @ X307) @ (esk65_3 @ X303 @ X304 @ X307))|(X307 @ X304 @ (esk62_2 @ X303 @ X304))|~(X303 @ X304 @ X305)|~(norm @ X303))))&(~(X303 @ (esk62_2 @ X303 @ X304) @ X313)|~(X303 @ X304 @ X305)|~(norm @ X303)))&(((X314 @ (esk68_1 @ X314) @ (esk69_1 @ X314))|(norm @ X314))&(((~(epred20_2 @ X314 @ X317 @ X319 @ X320)|~(epred20_2 @ X314 @ X317 @ X320 @ X321)|(epred20_2 @ X314 @ X317 @ X319 @ X321)|(X314 @ X317 @ (esk70_2 @ X314 @ X317))|(norm @ X314))&(~(X314 @ X322 @ X323)|(epred20_2 @ X314 @ X317 @ X322 @ X323)|(X314 @ X317 @ (esk70_2 @ X314 @ X317))|(norm @ X314)))&(~(epred20_2 @ X314 @ X317 @ (esk68_1 @ X314) @ X317)|(X314 @ X317 @ (esk70_2 @ X314 @ X317))|(norm @ X314))))))&(((((((X325 @ (esk75_4 @ X325 @ X326 @ X327 @ X329) @ (esk76_4 @ X325 @ X326 @ X327 @ X329))|(X329 @ (esk72_4 @ X325 @ X326 @ X327 @ X329) @ (esk73_4 @ X325 @ X326 @ X327 @ X329))|(X329 @ X327 @ (esk71_3 @ X325 @ X326 @ X327))|~(epred2_3 @ X327 @ X326 @ X325)|~(join @ X325 @ X326 @ X327))&(~(X329 @ (esk75_4 @ X325 @ X326 @ X327 @ X329) @ (esk76_4 @ X325 @ X326 @ X327 @ X329))|(X329 @ (esk72_4 @ X325 @ X326 @ X327 @ X329) @ (esk73_4 @ X325 @ X326 @ X327 @ X329))|(X329 @ X327 @ (esk71_3 @ X325 @ X326 @ X327))|~(epred2_3 @ X327 @ X326 @ X325)|~(join @ X325 @ X326 @ X327)))&(((X325 @ (esk75_4 @ X325 @ X326 @ X327 @ X329) @ (esk76_4 @ X325 @ X326 @ X327 @ X329))|(X329 @ (esk73_4 @ X325 @ X326 @ X327 @ X329) @ (esk74_4 @ X325 @ X326 @ X327 @ X329))|(X329 @ X327 @ (esk71_3 @ X325 @ X326 @ X327))|~(epred2_3 @ X327 @ X326 @ X325)|~(join @ X325 @ X326 @ X327))&(~(X329 @ (esk75_4 @ X325 @ X326 @ X327 @ X329) @ (esk76_4 @ X325 @ X326 @ X327 @ X329))|(X329 @ (esk73_4 @ X325 @ X326 @ X327 @ X329) @ (esk74_4 @ X325 @ X326 @ X327 @ X329))|(X329 @ X327 @ (esk71_3 @ X325 @ X326 @ X327))|~(epred2_3 @ X327 @ X326 @ X325)|~(join @ X325 @ X326 @ X327))))&(((X325 @ (esk75_4 @ X325 @ X326 @ X327 @ X329) @ (esk76_4 @ X325 @ X326 @ X327 @ X329))|~(X329 @ (esk72_4 @ X325 @ X326 @ X327 @ X329) @ (esk74_4 @ X325 @ X326 @ X327 @ X329))|(X329 @ X327 @ (esk71_3 @ X325 @ X326 @ X327))|~(epred2_3 @ X327 @ X326 @ X325)|~(join @ X325 @ X326 @ X327))&(~(X329 @ (esk75_4 @ X325 @ X326 @ X327 @ X329) @ (esk76_4 @ X325 @ X326 @ X327 @ X329))|~(X329 @ (esk72_4 @ X325 @ X326 @ X327 @ X329) @ (esk74_4 @ X325 @ X326 @ X327 @ X329))|(X329 @ X327 @ (esk71_3 @ X325 @ X326 @ X327))|~(epred2_3 @ X327 @ X326 @ X325)|~(join @ X325 @ X326 @ X327))))&(((((X325 @ (esk80_4 @ X325 @ X326 @ X327 @ X335) @ (esk81_4 @ X325 @ X326 @ X327 @ X335))|(X335 @ (esk77_4 @ X325 @ X326 @ X327 @ X335) @ (esk78_4 @ X325 @ X326 @ X327 @ X335))|(X335 @ X326 @ (esk71_3 @ X325 @ X326 @ X327))|~(epred2_3 @ X327 @ X326 @ X325)|~(join @ X325 @ X326 @ X327))&(~(X335 @ (esk80_4 @ X325 @ X326 @ X327 @ X335) @ (esk81_4 @ X325 @ X326 @ X327 @ X335))|(X335 @ (esk77_4 @ X325 @ X326 @ X327 @ X335) @ (esk78_4 @ X325 @ X326 @ X327 @ X335))|(X335 @ X326 @ (esk71_3 @ X325 @ X326 @ X327))|~(epred2_3 @ X327 @ X326 @ X325)|~(join @ X325 @ X326 @ X327)))&(((X325 @ (esk80_4 @ X325 @ X326 @ X327 @ X335) @ (esk81_4 @ X325 @ X326 @ X327 @ X335))|(X335 @ (esk78_4 @ X325 @ X326 @ X327 @ X335) @ (esk79_4 @ X325 @ X326 @ X327 @ X335))|(X335 @ X326 @ (esk71_3 @ X325 @ X326 @ X327))|~(epred2_3 @ X327 @ X326 @ X325)|~(join @ X325 @ X326 @ X327))&(~(X335 @ (esk80_4 @ X325 @ X326 @ X327 @ X335) @ (esk81_4 @ X325 @ X326 @ X327 @ X335))|(X335 @ (esk78_4 @ X325 @ X326 @ X327 @ X335) @ (esk79_4 @ X325 @ X326 @ X327 @ X335))|(X335 @ X326 @ (esk71_3 @ X325 @ X326 @ X327))|~(epred2_3 @ X327 @ X326 @ X325)|~(join @ X325 @ X326 @ X327))))&(((X325 @ (esk80_4 @ X325 @ X326 @ X327 @ X335) @ (esk81_4 @ X325 @ X326 @ X327 @ X335))|~(X335 @ (esk77_4 @ X325 @ X326 @ X327 @ X335) @ (esk79_4 @ X325 @ X326 @ X327 @ X335))|(X335 @ X326 @ (esk71_3 @ X325 @ X326 @ X327))|~(epred2_3 @ X327 @ X326 @ X325)|~(join @ X325 @ X326 @ X327))&(~(X335 @ (esk80_4 @ X325 @ X326 @ X327 @ X335) @ (esk81_4 @ X325 @ X326 @ X327 @ X335))|~(X335 @ (esk77_4 @ X325 @ X326 @ X327 @ X335) @ (esk79_4 @ X325 @ X326 @ X327 @ X335))|(X335 @ X326 @ (esk71_3 @ X325 @ X326 @ X327))|~(epred2_3 @ X327 @ X326 @ X325)|~(join @ X325 @ X326 @ X327)))))&(((epred2_3 @ X343 @ X342 @ X341)|(join @ X341 @ X342 @ X343))&(((((~(epred22_4 @ X341 @ X342 @ X343 @ X344 @ X352 @ X353)|~(epred22_4 @ X341 @ X342 @ X343 @ X344 @ X353 @ X354)|(epred22_4 @ X341 @ X342 @ X343 @ X344 @ X352 @ X354)|(~(epred21_4 @ X341 @ X342 @ X343 @ X344 @ X346 @ X347)|~(epred21_4 @ X341 @ X342 @ X343 @ X344 @ X347 @ X348)|(epred21_4 @ X341 @ X342 @ X343 @ X344 @ X346 @ X348))|(join @ X341 @ X342 @ X343))&(~(X341 @ X355 @ X356)|(epred22_4 @ X341 @ X342 @ X343 @ X344 @ X355 @ X356)|(~(epred21_4 @ X341 @ X342 @ X343 @ X344 @ X346 @ X347)|~(epred21_4 @ X341 @ X342 @ X343 @ X344 @ X347 @ X348)|(epred21_4 @ X341 @ X342 @ X343 @ X344 @ X346 @ X348))|(join @ X341 @ X342 @ X343)))&(~(epred22_4 @ X341 @ X342 @ X343 @ X344 @ X342 @ X344)|(~(epred21_4 @ X341 @ X342 @ X343 @ X344 @ X346 @ X347)|~(epred21_4 @ X341 @ X342 @ X343 @ X344 @ X347 @ X348)|(epred21_4 @ X341 @ X342 @ X343 @ X344 @ X346 @ X348))|(join @ X341 @ X342 @ X343)))&(((~(epred22_4 @ X341 @ X342 @ X343 @ X344 @ X352 @ X353)|~(epred22_4 @ X341 @ X342 @ X343 @ X344 @ X353 @ X354)|(epred22_4 @ X341 @ X342 @ X343 @ X344 @ X352 @ X354)|(~(X341 @ X349 @ X350)|(epred21_4 @ X341 @ X342 @ X343 @ X344 @ X349 @ X350))|(join @ X341 @ X342 @ X343))&(~(X341 @ X355 @ X356)|(epred22_4 @ X341 @ X342 @ X343 @ X344 @ X355 @ X356)|(~(X341 @ X349 @ X350)|(epred21_4 @ X341 @ X342 @ X343 @ X344 @ X349 @ X350))|(join @ X341 @ X342 @ X343)))&(~(epred22_4 @ X341 @ X342 @ X343 @ X344 @ X342 @ X344)|(~(X341 @ X349 @ X350)|(epred21_4 @ X341 @ X342 @ X343 @ X344 @ X349 @ X350))|(join @ X341 @ X342 @ X343))))&(((~(epred22_4 @ X341 @ X342 @ X343 @ X344 @ X352 @ X353)|~(epred22_4 @ X341 @ X342 @ X343 @ X344 @ X353 @ X354)|(epred22_4 @ X341 @ X342 @ X343 @ X344 @ X352 @ X354)|~(epred21_4 @ X341 @ X342 @ X343 @ X344 @ X343 @ X344)|(join @ X341 @ X342 @ X343))&(~(X341 @ X355 @ X356)|(epred22_4 @ X341 @ X342 @ X343 @ X344 @ X355 @ X356)|~(epred21_4 @ X341 @ X342 @ X343 @ X344 @ X343 @ X344)|(join @ X341 @ X342 @ X343)))&(~(epred22_4 @ X341 @ X342 @ X343 @ X344 @ X342 @ X344)|~(epred21_4 @ X341 @ X342 @ X343 @ X344 @ X343 @ X344)|(join @ X341 @ X342 @ X343)))))))&(((((((X357 @ (esk87_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk88_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|((X362 @ (esk84_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk85_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|((X357 @ (esk82_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk83_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|(epred3_5 @ X361 @ X357 @ X360 @ X359 @ X358)|(X361 @ X359 @ X360)))|(X362 @ X360 @ X359)|~(lconfl @ X357))&(~(X362 @ (esk87_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk88_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|((X362 @ (esk84_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk85_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|((X357 @ (esk82_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk83_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|(epred3_5 @ X361 @ X357 @ X360 @ X359 @ X358)|(X361 @ X359 @ X360)))|(X362 @ X360 @ X359)|~(lconfl @ X357)))&(((X357 @ (esk87_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk88_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|((X362 @ (esk85_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk86_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|((X357 @ (esk82_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk83_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|(epred3_5 @ X361 @ X357 @ X360 @ X359 @ X358)|(X361 @ X359 @ X360)))|(X362 @ X360 @ X359)|~(lconfl @ X357))&(~(X362 @ (esk87_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk88_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|((X362 @ (esk85_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk86_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|((X357 @ (esk82_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk83_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|(epred3_5 @ X361 @ X357 @ X360 @ X359 @ X358)|(X361 @ X359 @ X360)))|(X362 @ X360 @ X359)|~(lconfl @ X357))))&(((X357 @ (esk87_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk88_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|(~(X362 @ (esk84_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk86_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|((X357 @ (esk82_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk83_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|(epred3_5 @ X361 @ X357 @ X360 @ X359 @ X358)|(X361 @ X359 @ X360)))|(X362 @ X360 @ X359)|~(lconfl @ X357))&(~(X362 @ (esk87_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk88_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|(~(X362 @ (esk84_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk86_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|((X357 @ (esk82_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk83_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|(epred3_5 @ X361 @ X357 @ X360 @ X359 @ X358)|(X361 @ X359 @ X360)))|(X362 @ X360 @ X359)|~(lconfl @ X357))))&(((((X357 @ (esk87_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk88_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|((X362 @ (esk84_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk85_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|(~(X361 @ (esk82_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk83_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|(epred3_5 @ X361 @ X357 @ X360 @ X359 @ X358)|(X361 @ X359 @ X360)))|(X362 @ X360 @ X359)|~(lconfl @ X357))&(~(X362 @ (esk87_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk88_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|((X362 @ (esk84_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk85_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|(~(X361 @ (esk82_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk83_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|(epred3_5 @ X361 @ X357 @ X360 @ X359 @ X358)|(X361 @ X359 @ X360)))|(X362 @ X360 @ X359)|~(lconfl @ X357)))&(((X357 @ (esk87_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk88_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|((X362 @ (esk85_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk86_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|(~(X361 @ (esk82_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk83_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|(epred3_5 @ X361 @ X357 @ X360 @ X359 @ X358)|(X361 @ X359 @ X360)))|(X362 @ X360 @ X359)|~(lconfl @ X357))&(~(X362 @ (esk87_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk88_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|((X362 @ (esk85_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk86_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|(~(X361 @ (esk82_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk83_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|(epred3_5 @ X361 @ X357 @ X360 @ X359 @ X358)|(X361 @ X359 @ X360)))|(X362 @ X360 @ X359)|~(lconfl @ X357))))&(((X357 @ (esk87_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk88_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|(~(X362 @ (esk84_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk86_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|(~(X361 @ (esk82_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk83_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|(epred3_5 @ X361 @ X357 @ X360 @ X359 @ X358)|(X361 @ X359 @ X360)))|(X362 @ X360 @ X359)|~(lconfl @ X357))&(~(X362 @ (esk87_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk88_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|(~(X362 @ (esk84_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk86_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|(~(X361 @ (esk82_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362) @ (esk83_6 @ X357 @ X358 @ X359 @ X360 @ X361 @ X362))|(epred3_5 @ X361 @ X357 @ X360 @ X359 @ X358)|(X361 @ X359 @ X360)))|(X362 @ X360 @ X359)|~(lconfl @ X357)))))&((((((~(epred3_5 @ (epred23_1 @ X370) @ X370 @ (esk91_1 @ X370) @ (esk90_1 @ X370) @ (esk89_1 @ X370))|(lconfl @ X370))&(~(X370 @ X376 @ X377)|(epred23_1 @ X370 @ X376 @ X377)|(lconfl @ X370)))&(~(epred23_1 @ X370 @ (esk90_1 @ X370) @ (esk91_1 @ X370))|(lconfl @ X370)))&(~(epred24_1 @ X370 @ X378 @ X379)|~(epred24_1 @ X370 @ X379 @ X380)|(epred24_1 @ X370 @ X378 @ X380)|(lconfl @ X370)))&(~(X370 @ X381 @ X382)|(epred24_1 @ X370 @ X381 @ X382)|(lconfl @ X370)))&(~(epred24_1 @ X370 @ (esk91_1 @ X370) @ (esk90_1 @ X370))|(lconfl @ X370)))))&((~(sconfl @ X383)|((epred5_6 @ X388 @ X383 @ X387 @ X386 @ X385 @ X384)|(X388 @ X386 @ X385)))&((~(epred5_6 @ (epred26_1 @ X389) @ X389 @ (epred25_1 @ X389) @ (esk94_1 @ X389) @ (esk93_1 @ X389) @ (esk92_1 @ X389))|(sconfl @ X389))&(~(epred26_1 @ X389 @ (esk94_1 @ X389) @ (esk93_1 @ X389))|(sconfl @ X389)))))&((~(confl @ X395)|((epred7_6 @ X400 @ X395 @ X399 @ X398 @ X397 @ X396)|(X400 @ X398 @ X397)))&((~(epred7_6 @ (epred28_1 @ X401) @ X401 @ (epred27_1 @ X401) @ (esk97_1 @ X401) @ (esk96_1 @ X401) @ (esk95_1 @ X401))|(confl @ X401))&(~(epred28_1 @ X401 @ (esk97_1 @ X401) @ (esk96_1 @ X401))|(confl @ X401)))))&(((((((X407 @ (esk103_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk104_5 @ X407 @ X408 @ X409 @ X410 @ X411))|((X411 @ (esk100_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk101_5 @ X407 @ X408 @ X409 @ X410 @ X411))|((X407 @ (esk98_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk99_5 @ X407 @ X408 @ X409 @ X410 @ X411))|(epred9_4 @ X410 @ X407 @ X409 @ X408)|(X410 @ X409 @ X408)))|(X411 @ X408 @ X409)|~(cr @ X407))&(~(X411 @ (esk103_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk104_5 @ X407 @ X408 @ X409 @ X410 @ X411))|((X411 @ (esk100_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk101_5 @ X407 @ X408 @ X409 @ X410 @ X411))|((X407 @ (esk98_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk99_5 @ X407 @ X408 @ X409 @ X410 @ X411))|(epred9_4 @ X410 @ X407 @ X409 @ X408)|(X410 @ X409 @ X408)))|(X411 @ X408 @ X409)|~(cr @ X407)))&(((X407 @ (esk103_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk104_5 @ X407 @ X408 @ X409 @ X410 @ X411))|((X411 @ (esk101_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk102_5 @ X407 @ X408 @ X409 @ X410 @ X411))|((X407 @ (esk98_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk99_5 @ X407 @ X408 @ X409 @ X410 @ X411))|(epred9_4 @ X410 @ X407 @ X409 @ X408)|(X410 @ X409 @ X408)))|(X411 @ X408 @ X409)|~(cr @ X407))&(~(X411 @ (esk103_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk104_5 @ X407 @ X408 @ X409 @ X410 @ X411))|((X411 @ (esk101_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk102_5 @ X407 @ X408 @ X409 @ X410 @ X411))|((X407 @ (esk98_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk99_5 @ X407 @ X408 @ X409 @ X410 @ X411))|(epred9_4 @ X410 @ X407 @ X409 @ X408)|(X410 @ X409 @ X408)))|(X411 @ X408 @ X409)|~(cr @ X407))))&(((X407 @ (esk103_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk104_5 @ X407 @ X408 @ X409 @ X410 @ X411))|(~(X411 @ (esk100_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk102_5 @ X407 @ X408 @ X409 @ X410 @ X411))|((X407 @ (esk98_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk99_5 @ X407 @ X408 @ X409 @ X410 @ X411))|(epred9_4 @ X410 @ X407 @ X409 @ X408)|(X410 @ X409 @ X408)))|(X411 @ X408 @ X409)|~(cr @ X407))&(~(X411 @ (esk103_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk104_5 @ X407 @ X408 @ X409 @ X410 @ X411))|(~(X411 @ (esk100_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk102_5 @ X407 @ X408 @ X409 @ X410 @ X411))|((X407 @ (esk98_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk99_5 @ X407 @ X408 @ X409 @ X410 @ X411))|(epred9_4 @ X410 @ X407 @ X409 @ X408)|(X410 @ X409 @ X408)))|(X411 @ X408 @ X409)|~(cr @ X407))))&(((((X407 @ (esk103_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk104_5 @ X407 @ X408 @ X409 @ X410 @ X411))|((X411 @ (esk100_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk101_5 @ X407 @ X408 @ X409 @ X410 @ X411))|(~(X410 @ (esk98_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk99_5 @ X407 @ X408 @ X409 @ X410 @ X411))|(epred9_4 @ X410 @ X407 @ X409 @ X408)|(X410 @ X409 @ X408)))|(X411 @ X408 @ X409)|~(cr @ X407))&(~(X411 @ (esk103_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk104_5 @ X407 @ X408 @ X409 @ X410 @ X411))|((X411 @ (esk100_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk101_5 @ X407 @ X408 @ X409 @ X410 @ X411))|(~(X410 @ (esk98_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk99_5 @ X407 @ X408 @ X409 @ X410 @ X411))|(epred9_4 @ X410 @ X407 @ X409 @ X408)|(X410 @ X409 @ X408)))|(X411 @ X408 @ X409)|~(cr @ X407)))&(((X407 @ (esk103_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk104_5 @ X407 @ X408 @ X409 @ X410 @ X411))|((X411 @ (esk101_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk102_5 @ X407 @ X408 @ X409 @ X410 @ X411))|(~(X410 @ (esk98_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk99_5 @ X407 @ X408 @ X409 @ X410 @ X411))|(epred9_4 @ X410 @ X407 @ X409 @ X408)|(X410 @ X409 @ X408)))|(X411 @ X408 @ X409)|~(cr @ X407))&(~(X411 @ (esk103_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk104_5 @ X407 @ X408 @ X409 @ X410 @ X411))|((X411 @ (esk101_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk102_5 @ X407 @ X408 @ X409 @ X410 @ X411))|(~(X410 @ (esk98_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk99_5 @ X407 @ X408 @ X409 @ X410 @ X411))|(epred9_4 @ X410 @ X407 @ X409 @ X408)|(X410 @ X409 @ X408)))|(X411 @ X408 @ X409)|~(cr @ X407))))&(((X407 @ (esk103_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk104_5 @ X407 @ X408 @ X409 @ X410 @ X411))|(~(X411 @ (esk100_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk102_5 @ X407 @ X408 @ X409 @ X410 @ X411))|(~(X410 @ (esk98_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk99_5 @ X407 @ X408 @ X409 @ X410 @ X411))|(epred9_4 @ X410 @ X407 @ X409 @ X408)|(X410 @ X409 @ X408)))|(X411 @ X408 @ X409)|~(cr @ X407))&(~(X411 @ (esk103_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk104_5 @ X407 @ X408 @ X409 @ X410 @ X411))|(~(X411 @ (esk100_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk102_5 @ X407 @ X408 @ X409 @ X410 @ X411))|(~(X410 @ (esk98_5 @ X407 @ X408 @ X409 @ X410 @ X411) @ (esk99_5 @ X407 @ X408 @ X409 @ X410 @ X411))|(epred9_4 @ X410 @ X407 @ X409 @ X408)|(X410 @ X409 @ X408)))|(X411 @ X408 @ X409)|~(cr @ X407)))))&((((((~(epred9_4 @ (epred29_1 @ X419) @ X419 @ (esk106_1 @ X419) @ (esk105_1 @ X419))|(cr @ X419))&(~(X419 @ X424 @ X425)|(epred29_1 @ X419 @ X424 @ X425)|(cr @ X419)))&(~(epred29_1 @ X419 @ (esk106_1 @ X419) @ (esk105_1 @ X419))|(cr @ X419)))&(~(epred30_1 @ X419 @ X426 @ X427)|~(epred30_1 @ X419 @ X427 @ X428)|(epred30_1 @ X419 @ X426 @ X428)|(cr @ X419)))&(~(X419 @ X429 @ X430)|(epred30_1 @ X419 @ X429 @ X430)|(cr @ X419)))&(~(epred30_1 @ X419 @ (esk105_1 @ X419) @ (esk106_1 @ X419))|(cr @ X419)))))), 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_8])])])])])])])).
% 0.82/0.41 thf(c_0_10, negated_conjecture, ~(((lconfl)=(^[X5:$i > $i > $o]:(![X7:$i, X8:$i, X12:$i]:((((((X5 @ X7 @ X12))&((X5 @ X7 @ X8))))=>((join @ X5 @ X12 @ X8)))))))), inference(assume_negation,[status(cth)],[locally_confluent])).
% 0.82/0.41 thf(c_0_11, plain, ![X2:d_unsorted]:(((X2)=(d_unsorted_0))), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.82/0.41 thf(c_0_12, negated_conjecture, ~(![X91:$i > $i > $o]:(((lconfl @ X91)<=>![X7:$i, X8:$i, X12:$i]:((((X91 @ X7 @ X12)&(X91 @ X7 @ X8))=>(join @ X91 @ X12 @ X8)))))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_10])])).
% 0.82/0.41 thf(c_0_13, plain, ![X1:$i]:(((X1)=(d2unsorted @ (esk1_1 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.82/0.41 thf(c_0_14, plain, ![X2:d_unsorted, X3:d_unsorted]:(((X2)=(X3))), inference(spm,[status(thm)],[c_0_11, c_0_11])).
% 0.82/0.41 thf(c_0_15, negated_conjecture, ![X435:$i, X436:$i, X437:$i]:((((((epred31_0 @ esk107_0 @ esk109_0)|~(lconfl @ epred31_0))&((epred31_0 @ esk107_0 @ esk108_0)|~(lconfl @ epred31_0)))&(~(join @ epred31_0 @ esk109_0 @ esk108_0)|~(lconfl @ epred31_0)))&((lconfl @ epred31_0)|(~(epred31_0 @ X435 @ X437)|~(epred31_0 @ X435 @ X436)|(join @ epred31_0 @ X437 @ X436))))), 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)],[c_0_12])])])])])])).
% 0.82/0.41 thf(c_0_16, plain, ![X2:d_unsorted, X1:$i]:(((d2unsorted @ X2)=(X1))), inference(spm,[status(thm)],[c_0_13, c_0_14])).
% 0.82/0.41 thf(c_0_17, plain, ![X468:$i > $i > $o, X469:$i, X470:$i, X472:$i, X473:$i, X474:$i, X475:$i, X476:$i, X478:$i, X479:$i, X480:$i, X481:$i, X482:$i, X483:$i > $i > $o, X484:$i, X485:$i, X486:$i > $i > $o, X492:$i > $i > $o]:(((((((X469)!=(X470))|~(epred2_3 @ X470 @ X469 @ X468))&(((~(epred34_3 @ X468 @ X469 @ X470 @ X472 @ X473)|~(epred34_3 @ X468 @ X469 @ X470 @ X473 @ X474)|(epred34_3 @ X468 @ X469 @ X470 @ X472 @ X474)|~(epred2_3 @ X470 @ X469 @ X468))&(~(X468 @ X475 @ X476)|(epred34_3 @ X468 @ X469 @ X470 @ X475 @ X476)|~(epred2_3 @ X470 @ X469 @ X468)))&(~(epred34_3 @ X468 @ X469 @ X470 @ X470 @ X469)|~(epred2_3 @ X470 @ X469 @ X468))))&(((~(epred35_3 @ X468 @ X469 @ X470 @ X478 @ X479)|~(epred35_3 @ X468 @ X469 @ X470 @ X479 @ X480)|(epred35_3 @ X468 @ X469 @ X470 @ X478 @ X480)|~(epred2_3 @ X470 @ X469 @ X468))&(~(X468 @ X481 @ X482)|(epred35_3 @ X468 @ X469 @ X470 @ X481 @ X482)|~(epred2_3 @ X470 @ X469 @ X468)))&(~(epred35_3 @ X468 @ X469 @ X470 @ X469 @ X470)|~(epred2_3 @ X470 @ X469 @ X468))))&((((((((X483 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ (esk125_4 @ X483 @ X484 @ X485 @ X492) @ (esk126_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|((X483 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ (esk120_4 @ X483 @ X484 @ X485 @ X486) @ (esk121_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483))&(~(X492 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ (esk125_4 @ X483 @ X484 @ X485 @ X492) @ (esk126_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|((X483 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ (esk120_4 @ X483 @ X484 @ X485 @ X486) @ (esk121_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483)))&(((X483 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ (esk126_4 @ X483 @ X484 @ X485 @ X492) @ (esk127_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|((X483 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ (esk120_4 @ X483 @ X484 @ X485 @ X486) @ (esk121_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483))&(~(X492 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ (esk126_4 @ X483 @ X484 @ X485 @ X492) @ (esk127_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|((X483 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ (esk120_4 @ X483 @ X484 @ X485 @ X486) @ (esk121_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483))))&(((X483 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|~(X492 @ (esk125_4 @ X483 @ X484 @ X485 @ X492) @ (esk127_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|((X483 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ (esk120_4 @ X483 @ X484 @ X485 @ X486) @ (esk121_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483))&(~(X492 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|~(X492 @ (esk125_4 @ X483 @ X484 @ X485 @ X492) @ (esk127_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|((X483 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ (esk120_4 @ X483 @ X484 @ X485 @ X486) @ (esk121_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483))))&(((((X483 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ (esk125_4 @ X483 @ X484 @ X485 @ X492) @ (esk126_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|(~(X486 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ (esk120_4 @ X483 @ X484 @ X485 @ X486) @ (esk121_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483))&(~(X492 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ (esk125_4 @ X483 @ X484 @ X485 @ X492) @ (esk126_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|(~(X486 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ (esk120_4 @ X483 @ X484 @ X485 @ X486) @ (esk121_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483)))&(((X483 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ (esk126_4 @ X483 @ X484 @ X485 @ X492) @ (esk127_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|(~(X486 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ (esk120_4 @ X483 @ X484 @ X485 @ X486) @ (esk121_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483))&(~(X492 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ (esk126_4 @ X483 @ X484 @ X485 @ X492) @ (esk127_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|(~(X486 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ (esk120_4 @ X483 @ X484 @ X485 @ X486) @ (esk121_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483))))&(((X483 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|~(X492 @ (esk125_4 @ X483 @ X484 @ X485 @ X492) @ (esk127_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|(~(X486 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ (esk120_4 @ X483 @ X484 @ X485 @ X486) @ (esk121_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483))&(~(X492 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|~(X492 @ (esk125_4 @ X483 @ X484 @ X485 @ X492) @ (esk127_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|(~(X486 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ (esk120_4 @ X483 @ X484 @ X485 @ X486) @ (esk121_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483)))))&((((((X483 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ (esk125_4 @ X483 @ X484 @ X485 @ X492) @ (esk126_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|((X483 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ (esk121_4 @ X483 @ X484 @ X485 @ X486) @ (esk122_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483))&(~(X492 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ (esk125_4 @ X483 @ X484 @ X485 @ X492) @ (esk126_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|((X483 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ (esk121_4 @ X483 @ X484 @ X485 @ X486) @ (esk122_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483)))&(((X483 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ (esk126_4 @ X483 @ X484 @ X485 @ X492) @ (esk127_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|((X483 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ (esk121_4 @ X483 @ X484 @ X485 @ X486) @ (esk122_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483))&(~(X492 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ (esk126_4 @ X483 @ X484 @ X485 @ X492) @ (esk127_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|((X483 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ (esk121_4 @ X483 @ X484 @ X485 @ X486) @ (esk122_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483))))&(((X483 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|~(X492 @ (esk125_4 @ X483 @ X484 @ X485 @ X492) @ (esk127_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|((X483 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ (esk121_4 @ X483 @ X484 @ X485 @ X486) @ (esk122_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483))&(~(X492 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|~(X492 @ (esk125_4 @ X483 @ X484 @ X485 @ X492) @ (esk127_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|((X483 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ (esk121_4 @ X483 @ X484 @ X485 @ X486) @ (esk122_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483))))&(((((X483 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ (esk125_4 @ X483 @ X484 @ X485 @ X492) @ (esk126_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|(~(X486 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ (esk121_4 @ X483 @ X484 @ X485 @ X486) @ (esk122_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483))&(~(X492 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ (esk125_4 @ X483 @ X484 @ X485 @ X492) @ (esk126_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|(~(X486 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ (esk121_4 @ X483 @ X484 @ X485 @ X486) @ (esk122_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483)))&(((X483 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ (esk126_4 @ X483 @ X484 @ X485 @ X492) @ (esk127_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|(~(X486 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ (esk121_4 @ X483 @ X484 @ X485 @ X486) @ (esk122_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483))&(~(X492 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ (esk126_4 @ X483 @ X484 @ X485 @ X492) @ (esk127_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|(~(X486 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ (esk121_4 @ X483 @ X484 @ X485 @ X486) @ (esk122_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483))))&(((X483 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|~(X492 @ (esk125_4 @ X483 @ X484 @ X485 @ X492) @ (esk127_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|(~(X486 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ (esk121_4 @ X483 @ X484 @ X485 @ X486) @ (esk122_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483))&(~(X492 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|~(X492 @ (esk125_4 @ X483 @ X484 @ X485 @ X492) @ (esk127_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|(~(X486 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ (esk121_4 @ X483 @ X484 @ X485 @ X486) @ (esk122_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483))))))&((((((X483 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ (esk125_4 @ X483 @ X484 @ X485 @ X492) @ (esk126_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|((X483 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|~(X486 @ (esk120_4 @ X483 @ X484 @ X485 @ X486) @ (esk122_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483))&(~(X492 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ (esk125_4 @ X483 @ X484 @ X485 @ X492) @ (esk126_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|((X483 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|~(X486 @ (esk120_4 @ X483 @ X484 @ X485 @ X486) @ (esk122_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483)))&(((X483 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ (esk126_4 @ X483 @ X484 @ X485 @ X492) @ (esk127_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|((X483 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|~(X486 @ (esk120_4 @ X483 @ X484 @ X485 @ X486) @ (esk122_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483))&(~(X492 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ (esk126_4 @ X483 @ X484 @ X485 @ X492) @ (esk127_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|((X483 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|~(X486 @ (esk120_4 @ X483 @ X484 @ X485 @ X486) @ (esk122_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483))))&(((X483 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|~(X492 @ (esk125_4 @ X483 @ X484 @ X485 @ X492) @ (esk127_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|((X483 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|~(X486 @ (esk120_4 @ X483 @ X484 @ X485 @ X486) @ (esk122_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483))&(~(X492 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|~(X492 @ (esk125_4 @ X483 @ X484 @ X485 @ X492) @ (esk127_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|((X483 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|~(X486 @ (esk120_4 @ X483 @ X484 @ X485 @ X486) @ (esk122_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483))))&(((((X483 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ (esk125_4 @ X483 @ X484 @ X485 @ X492) @ (esk126_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|(~(X486 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|~(X486 @ (esk120_4 @ X483 @ X484 @ X485 @ X486) @ (esk122_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483))&(~(X492 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ (esk125_4 @ X483 @ X484 @ X485 @ X492) @ (esk126_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|(~(X486 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|~(X486 @ (esk120_4 @ X483 @ X484 @ X485 @ X486) @ (esk122_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483)))&(((X483 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ (esk126_4 @ X483 @ X484 @ X485 @ X492) @ (esk127_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|(~(X486 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|~(X486 @ (esk120_4 @ X483 @ X484 @ X485 @ X486) @ (esk122_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483))&(~(X492 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ (esk126_4 @ X483 @ X484 @ X485 @ X492) @ (esk127_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|(~(X486 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|~(X486 @ (esk120_4 @ X483 @ X484 @ X485 @ X486) @ (esk122_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483))))&(((X483 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|~(X492 @ (esk125_4 @ X483 @ X484 @ X485 @ X492) @ (esk127_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|(~(X486 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|~(X486 @ (esk120_4 @ X483 @ X484 @ X485 @ X486) @ (esk122_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ X483))&(~(X492 @ (esk128_4 @ X483 @ X484 @ X485 @ X492) @ (esk129_4 @ X483 @ X484 @ X485 @ X492))|~(X492 @ (esk125_4 @ X483 @ X484 @ X485 @ X492) @ (esk127_4 @ X483 @ X484 @ X485 @ X492))|(X492 @ X484 @ X485)|(~(X486 @ (esk123_4 @ X483 @ X484 @ X485 @ X486) @ (esk124_4 @ X483 @ X484 @ X485 @ X486))|~(X486 @ (esk120_4 @ X483 @ X484 @ X485 @ X486) @ (esk122_4 @ X483 @ X484 @ X485 @ X486))|(X486 @ X485 @ X484)|((X484)=(X485)))|(epred2_3 @ X485 @ X484 @ 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(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_3])])])])])])])).
% 0.82/0.41 thf(c_0_18, negated_conjecture, (~((join @ epred31_0 @ esk109_0 @ esk108_0))|~((lconfl @ epred31_0))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.82/0.41 thf(c_0_19, plain, ![X1:$i, X7:$i]:(((X1)=(X7))), inference(spm,[status(thm)],[c_0_16, c_0_16])).
% 0.82/0.41 thf(c_0_20, plain, ![X1:$i, X7:$i, X5:$i > $i > $o]:((((X1)!=(X7))|~((epred2_3 @ X7 @ X1 @ X5)))), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.82/0.41 thf(c_0_21, plain, ![X498:$i, X499:$i, X500:$i, X501:$i > $i > $o, X502:$i > $i > $o, X504:$i > $i > $o, X510:$i > $i > $o, X519:$i, X520:$i, X521:$i, X522:$i > $i > $o, X523:$i > $i > $o, X524:$i, X526:$i, X527:$i, X528:$i, X529:$i, X530:$i, X532:$i, X533:$i, X534:$i, X535:$i, X536:$i, X537:$i, X538:$i, X539:$i]:((((((((((X502 @ (esk141_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk142_5 @ X498 @ X499 @ X500 @ X501 @ X502))|((X501 @ (esk134_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk135_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ (esk131_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk132_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ X499 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498))&((X502 @ (esk142_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk143_5 @ X498 @ X499 @ X500 @ X501 @ X502))|((X501 @ (esk134_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk135_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ (esk131_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk132_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ X499 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498)))&(~(X502 @ (esk141_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk143_5 @ X498 @ X499 @ X500 @ X501 @ X502))|((X501 @ (esk134_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk135_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ (esk131_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk132_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ X499 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498)))&((((X502 @ (esk141_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk142_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X504 @ (esk134_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk135_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ (esk131_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk132_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ X499 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498))&((X502 @ (esk142_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk143_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X504 @ (esk134_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk135_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ (esk131_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk132_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ X499 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498)))&(~(X502 @ (esk141_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk143_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X504 @ (esk134_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk135_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ (esk131_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk132_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ X499 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498))))&(((((X502 @ (esk141_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk142_5 @ X498 @ X499 @ X500 @ X501 @ X502))|((X501 @ (esk134_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk135_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ (esk132_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk133_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ X499 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498))&((X502 @ (esk142_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk143_5 @ X498 @ X499 @ X500 @ X501 @ X502))|((X501 @ (esk134_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk135_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ (esk132_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk133_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ X499 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498)))&(~(X502 @ (esk141_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk143_5 @ X498 @ X499 @ X500 @ X501 @ X502))|((X501 @ (esk134_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk135_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ (esk132_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk133_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ X499 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498)))&((((X502 @ (esk141_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk142_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X504 @ (esk134_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk135_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ (esk132_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk133_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ X499 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498))&((X502 @ (esk142_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk143_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X504 @ (esk134_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk135_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ (esk132_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk133_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ X499 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498)))&(~(X502 @ (esk141_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk143_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X504 @ (esk134_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk135_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ (esk132_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk133_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ X499 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498)))))&(((((X502 @ (esk141_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk142_5 @ X498 @ X499 @ X500 @ X501 @ X502))|((X501 @ (esk134_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk135_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|~(X504 @ (esk131_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk133_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ X499 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498))&((X502 @ (esk142_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk143_5 @ X498 @ X499 @ X500 @ X501 @ X502))|((X501 @ (esk134_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk135_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|~(X504 @ (esk131_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk133_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ X499 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498)))&(~(X502 @ (esk141_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk143_5 @ X498 @ X499 @ X500 @ X501 @ X502))|((X501 @ (esk134_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk135_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|~(X504 @ (esk131_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk133_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ X499 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498)))&((((X502 @ (esk141_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk142_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X504 @ (esk134_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk135_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|~(X504 @ (esk131_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk133_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ X499 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498))&((X502 @ (esk142_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk143_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X504 @ (esk134_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk135_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|~(X504 @ (esk131_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk133_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ X499 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498)))&(~(X502 @ (esk141_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk143_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X504 @ (esk134_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk135_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|~(X504 @ (esk131_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504) @ (esk133_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X504))|(X504 @ X499 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498)))))&(((((((X502 @ (esk141_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk142_5 @ X498 @ X499 @ X500 @ X501 @ X502))|((X501 @ (esk139_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk140_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ (esk136_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk137_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ X500 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498))&((X502 @ (esk142_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk143_5 @ X498 @ X499 @ X500 @ X501 @ X502))|((X501 @ (esk139_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk140_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ (esk136_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk137_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ X500 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498)))&(~(X502 @ (esk141_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk143_5 @ X498 @ X499 @ X500 @ X501 @ X502))|((X501 @ (esk139_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk140_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ (esk136_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk137_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ X500 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498)))&((((X502 @ (esk141_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk142_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X510 @ (esk139_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk140_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ (esk136_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk137_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ X500 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498))&((X502 @ (esk142_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk143_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X510 @ (esk139_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk140_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ (esk136_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk137_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ X500 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498)))&(~(X502 @ (esk141_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk143_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X510 @ (esk139_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk140_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ (esk136_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk137_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ X500 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498))))&(((((X502 @ (esk141_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk142_5 @ X498 @ X499 @ X500 @ X501 @ X502))|((X501 @ (esk139_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk140_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ (esk137_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk138_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ X500 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498))&((X502 @ (esk142_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk143_5 @ X498 @ X499 @ X500 @ X501 @ X502))|((X501 @ (esk139_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk140_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ (esk137_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk138_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ X500 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498)))&(~(X502 @ (esk141_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk143_5 @ X498 @ X499 @ X500 @ X501 @ X502))|((X501 @ (esk139_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk140_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ (esk137_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk138_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ X500 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498)))&((((X502 @ (esk141_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk142_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X510 @ (esk139_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk140_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ (esk137_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk138_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ X500 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498))&((X502 @ (esk142_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk143_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X510 @ (esk139_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk140_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ (esk137_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk138_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ X500 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498)))&(~(X502 @ (esk141_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk143_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X510 @ (esk139_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk140_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ (esk137_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk138_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ X500 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498)))))&(((((X502 @ (esk141_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk142_5 @ X498 @ X499 @ X500 @ X501 @ X502))|((X501 @ (esk139_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk140_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|~(X510 @ (esk136_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk138_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ X500 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498))&((X502 @ (esk142_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk143_5 @ X498 @ X499 @ X500 @ X501 @ X502))|((X501 @ (esk139_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk140_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|~(X510 @ (esk136_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk138_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ X500 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498)))&(~(X502 @ (esk141_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk143_5 @ X498 @ X499 @ X500 @ X501 @ X502))|((X501 @ (esk139_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk140_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|~(X510 @ (esk136_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk138_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ X500 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498)))&((((X502 @ (esk141_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk142_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X510 @ (esk139_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk140_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|~(X510 @ (esk136_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk138_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ X500 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498))&((X502 @ (esk142_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk143_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X510 @ (esk139_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk140_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|~(X510 @ (esk136_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk138_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ X500 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498)))&(~(X502 @ (esk141_5 @ X498 @ X499 @ X500 @ X501 @ X502) @ (esk143_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X510 @ (esk139_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk140_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|~(X510 @ (esk136_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510) @ (esk138_6 @ X498 @ X499 @ X500 @ X501 @ X502 @ X510))|(X510 @ X500 @ (esk130_5 @ X498 @ X499 @ X500 @ X501 @ X502))|(~(X501 @ X498 @ X500)|~(X501 @ X498 @ X499)|((X499)=(X500))))|~(epred3_5 @ X502 @ X501 @ X500 @ X499 @ X498))))))&((((((X522 @ X519 @ X521)|(epred3_5 @ X523 @ X522 @ X521 @ X520 @ X519))&((X522 @ X519 @ X520)|(epred3_5 @ X523 @ X522 @ X521 @ X520 @ X519)))&(((X520)!=(X521))|(epred3_5 @ X523 @ X522 @ X521 @ X520 @ X519)))&(((((~(epred37_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X532 @ X533)|~(epred37_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X533 @ X534)|(epred37_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X532 @ X534)|(~(epred36_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X526 @ X527)|~(epred36_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X527 @ X528)|(epred36_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X526 @ X528))|(epred3_5 @ X523 @ X522 @ X521 @ X520 @ X519))&(~(X522 @ X535 @ X536)|(epred37_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X535 @ X536)|(~(epred36_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X526 @ X527)|~(epred36_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X527 @ X528)|(epred36_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X526 @ X528))|(epred3_5 @ X523 @ X522 @ X521 @ X520 @ X519)))&(~(epred37_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X521 @ X524)|(~(epred36_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X526 @ X527)|~(epred36_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X527 @ X528)|(epred36_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X526 @ X528))|(epred3_5 @ X523 @ X522 @ X521 @ X520 @ X519)))&(((~(epred37_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X532 @ X533)|~(epred37_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X533 @ X534)|(epred37_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X532 @ X534)|(~(X522 @ X529 @ X530)|(epred36_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X529 @ X530))|(epred3_5 @ X523 @ X522 @ X521 @ X520 @ X519))&(~(X522 @ X535 @ X536)|(epred37_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X535 @ X536)|(~(X522 @ X529 @ X530)|(epred36_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X529 @ X530))|(epred3_5 @ X523 @ X522 @ X521 @ X520 @ X519)))&(~(epred37_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X521 @ X524)|(~(X522 @ X529 @ X530)|(epred36_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X529 @ X530))|(epred3_5 @ X523 @ X522 @ X521 @ X520 @ X519))))&(((~(epred37_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X532 @ X533)|~(epred37_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X533 @ X534)|(epred37_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X532 @ X534)|~(epred36_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X520 @ X524)|(epred3_5 @ X523 @ X522 @ X521 @ X520 @ X519))&(~(X522 @ X535 @ X536)|(epred37_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X535 @ X536)|~(epred36_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X520 @ X524)|(epred3_5 @ X523 @ X522 @ X521 @ X520 @ X519)))&(~(epred37_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X521 @ X524)|~(epred36_6 @ X519 @ X520 @ X521 @ X522 @ X523 @ X524 @ X520 @ X524)|(epred3_5 @ X523 @ X522 @ X521 @ X520 @ X519)))))&(~(X523 @ X537 @ X538)|~(X523 @ X538 @ X539)|(X523 @ X537 @ X539)|(epred3_5 @ X523 @ X522 @ X521 @ X520 @ X519))))), 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_4])])])])])])])).
% 0.82/0.41 thf(c_0_22, negated_conjecture, ![X1:$i]:((~((join @ epred31_0 @ esk109_0 @ X1))|~((lconfl @ epred31_0)))), inference(spm,[status(thm)],[c_0_18, c_0_19])).
% 0.82/0.41 thf(c_0_23, plain, ![X7:$i, X5:$i > $i > $o, X1:$i]:(((epred2_3 @ X1 @ X7 @ X5)|(join @ X5 @ X7 @ X1))), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.82/0.41 thf(c_0_24, plain, ![X1:$i, X7:$i, X5:$i > $i > $o]:(~((epred2_3 @ X1 @ X7 @ X5))), inference(sr,[status(thm)],[c_0_20, c_0_19])).
% 0.82/0.41 thf(c_0_25, plain, ![X6:$i > $i > $o, X5:$i > $i > $o, X1:$i, X8:$i, X7:$i]:(((epred3_5 @ X5 @ X6 @ X7 @ X1 @ X8)|((X1)!=(X7)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.82/0.41 thf(c_0_26, negated_conjecture, ![X1:$i, X7:$i]:((~((join @ epred31_0 @ X1 @ X7))|~((lconfl @ epred31_0)))), inference(spm,[status(thm)],[c_0_22, c_0_19])).
% 0.82/0.41 thf(c_0_27, plain, ![X1:$i, X5:$i > $i > $o, X7:$i]:((join @ X5 @ X1 @ X7)), inference(sr,[status(thm)],[c_0_23, c_0_24])).
% 0.82/0.41 thf(c_0_28, plain, ![X5:$i > $i > $o]:(((lconfl @ X5)|~((epred3_5 @ (epred23_1 @ X5) @ X5 @ (esk91_1 @ X5) @ (esk90_1 @ X5) @ (esk89_1 @ X5))))), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.82/0.41 thf(c_0_29, plain, ![X1:$i, X5:$i > $i > $o, X6:$i > $i > $o, X7:$i, X8:$i]:((epred3_5 @ X5 @ X6 @ X1 @ X7 @ X8)), inference(sr,[status(thm)],[c_0_25, c_0_19])).
% 0.82/0.41 thf(c_0_30, negated_conjecture, ~((lconfl @ epred31_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_26, c_0_27])])).
% 0.82/0.41 thf(c_0_31, plain, ![X5:$i > $i > $o]:((lconfl @ X5)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_28, c_0_29])])).
% 0.82/0.41 thf(c_0_32, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_30, c_0_31])]), ['proof']).
% 0.82/0.41 % SZS output end CNFRefutation
% 0.82/0.41 % Parsed axioms : 35
% 0.82/0.41 % Removed by relevancy pruning/SinE : 0
% 0.82/0.41 % Initial clauses : 818
% 0.82/0.41 % Removed in clause preprocessing : 45
% 0.82/0.41 % Initial clauses in saturation : 773
% 0.82/0.41 % Processed clauses : 1188
% 0.82/0.41 % ...of these trivial : 19
% 0.82/0.41 % ...subsumed : 433
% 0.82/0.41 % ...remaining for further processing : 736
% 0.82/0.41 % Other redundant clauses eliminated : 0
% 0.82/0.41 % Clauses deleted for lack of memory : 0
% 0.82/0.41 % Backward-subsumed : 64
% 0.82/0.41 % Backward-rewritten : 173
% 0.82/0.41 % Generated clauses : 2786
% 0.82/0.41 % ...of the previous two non-redundant : 2294
% 0.82/0.41 % ...aggressively subsumed : 0
% 0.82/0.41 % Contextual simplify-reflections : 17
% 0.82/0.41 % Paramodulations : 2784
% 0.82/0.41 % Factorizations : 0
% 0.82/0.41 % NegExts : 0
% 0.82/0.41 % Equation resolutions : 0
% 0.82/0.41 % Disequality decompositions : 0
% 0.82/0.41 % Total rewrite steps : 688
% 0.82/0.41 % ...of those cached : 402
% 0.82/0.41 % Propositional unsat checks : 0
% 0.82/0.41 % Propositional check models : 0
% 0.82/0.41 % Propositional check unsatisfiable : 0
% 0.82/0.41 % Propositional clauses : 0
% 0.82/0.41 % Propositional clauses after purity: 0
% 0.82/0.41 % Propositional unsat core size : 0
% 0.82/0.41 % Propositional preprocessing time : 0.000
% 0.82/0.41 % Propositional encoding time : 0.000
% 0.82/0.41 % Propositional solver time : 0.000
% 0.82/0.41 % Success case prop preproc time : 0.000
% 0.82/0.41 % Success case prop encoding time : 0.000
% 0.82/0.41 % Success case prop solver time : 0.000
% 0.82/0.41 % Current number of processed clauses : 499
% 0.82/0.41 % Positive orientable unit clauses : 242
% 0.82/0.41 % Positive unorientable unit clauses: 2
% 0.82/0.41 % Negative unit clauses : 38
% 0.82/0.41 % Non-unit-clauses : 217
% 0.82/0.41 % Current number of unprocessed clauses: 1748
% 0.82/0.41 % ...number of literals in the above : 6919
% 0.82/0.41 % Current number of archived formulas : 0
% 0.82/0.41 % Current number of archived clauses : 237
% 0.82/0.41 % Clause-clause subsumption calls (NU) : 50179
% 0.82/0.41 % Rec. Clause-clause subsumption calls : 36481
% 0.82/0.41 % Non-unit clause-clause subsumptions : 457
% 0.82/0.41 % Unit Clause-clause subsumption calls : 29874
% 0.82/0.41 % Rewrite failures with RHS unbound : 338
% 0.82/0.41 % BW rewrite match attempts : 289
% 0.82/0.41 % BW rewrite match successes : 87
% 0.82/0.41 % Condensation attempts : 0
% 0.82/0.41 % Condensation successes : 0
% 0.82/0.41 % Termbank termtop insertions : 83437
% 0.82/0.41 % Search garbage collected termcells : 13477
% 0.82/0.41
% 0.82/0.41 % -------------------------------------------------
% 0.82/0.41 % User time : 0.120 s
% 0.82/0.41 % System time : 0.016 s
% 0.82/0.41 % Total time : 0.136 s
% 0.82/0.41 % Maximum resident set size: 6316 pages
% 0.82/0.41
% 0.82/0.41 % -------------------------------------------------
% 0.82/0.41 % User time : 0.192 s
% 0.82/0.41 % System time : 0.030 s
% 0.82/0.41 % Total time : 0.222 s
% 0.82/0.41 % Maximum resident set size: 4608 pages
% 0.82/0.41 % E exiting
%------------------------------------------------------------------------------