%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SWX181^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 : n001.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:27 AM UTC 2026
% Result : Theorem 0.21s 0.36s
% Output : CNFRefutation 0.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX181^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.10/0.18 % Computer : n001.cluster.edu
% 0.10/0.18 % Model : x86_64 x86_64
% 0.10/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.18 % Memory : 8046.5625MB
% 0.10/0.18 % OS : Linux 6.8.0-71-generic
% 0.10/0.18 % CPULimit : 300
% 0.10/0.18 % WCLimit : 300
% 0.10/0.18 % DateTime : Tue Sep 29 16:16:05 UTC 2026
% 0.10/0.18 % CPUTime :
% 0.10/0.18 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.22 Running higher-order theorem proving
% 0.10/0.23 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.4Y9RVdFgpd/E---3.1_1438329.p
% 0.21/0.36 % Version: 3.5.1-ho
% 0.21/0.36 % partial match(1): HSLSSMSSSSSNHHA
% 0.21/0.36 % Preprocessing class: HSLSSMSSSSSNHHN.
% 0.21/0.36 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.21/0.36 % Starting new_ho_10 with 600s (2) cores
% 0.21/0.36 % Starting sh3 with 600s (2) cores
% 0.21/0.36 % Starting ho_unfolding_3 with 600s (2) cores
% 0.21/0.36 % Starting new_ho_10_cnf2 with 600s (2) cores
% 0.21/0.36 % sh3 with pid 1438343 completed with status 0
% 0.21/0.36 % Result found by sh3
% 0.21/0.36 % partial match(1): HSLSSMSSSSSNHHA
% 0.21/0.36 % Preprocessing class: HSLSSMSSSSSNHHN.
% 0.21/0.36 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.21/0.36 % Starting new_ho_10 with 600s (2) cores
% 0.21/0.36 % Starting sh3 with 600s (2) cores
% 0.21/0.36 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.21/0.36 % No SInE strategy applied
% 0.21/0.36 % Search class: HGHSS-FMLF33-MHHFFMBN
% 0.21/0.36 % partial match(1): HGHSF-FMLF33-MHHFFMBN
% 0.21/0.36 % Scheduled 6 strats onto 2 cores with 600 seconds (600 total)
% 0.21/0.36 % Starting SubtermCWHack with 61s (1) cores
% 0.21/0.36 % Starting new_ho_10 with 121s (1) cores
% 0.21/0.36 % new_ho_10 with pid 1438349 completed with status 0
% 0.21/0.36 % Result found by new_ho_10
% 0.21/0.36 % partial match(1): HSLSSMSSSSSNHHA
% 0.21/0.36 % Preprocessing class: HSLSSMSSSSSNHHN.
% 0.21/0.36 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.21/0.36 % Starting new_ho_10 with 600s (2) cores
% 0.21/0.36 % Starting sh3 with 600s (2) cores
% 0.21/0.36 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.21/0.36 % No SInE strategy applied
% 0.21/0.36 % Search class: HGHSS-FMLF33-MHHFFMBN
% 0.21/0.36 % partial match(1): HGHSF-FMLF33-MHHFFMBN
% 0.21/0.36 % Scheduled 6 strats onto 2 cores with 600 seconds (600 total)
% 0.21/0.36 % Starting SubtermCWHack with 61s (1) cores
% 0.21/0.36 % Starting new_ho_10 with 121s (1) cores
% 0.21/0.36 % Preprocessing time : 0.012 s
% 0.21/0.36 % Presaturation interreduction done
% 0.21/0.36
% 0.21/0.36 % Proof found!
% 0.21/0.36 % SZS status Theorem
% 0.21/0.36 % SZS output start CNFRefutation
% 0.21/0.36 thf(decl_sort1, type, d_unsorted: $tType).
% 0.21/0.36 thf(decl_23, type, subrel: ($i > $i > $o) > ($i > $i > $o) > $o).
% 0.21/0.36 thf(decl_24, type, inv: ($i > $i > $o) > $i > $i > $o).
% 0.21/0.36 thf(decl_25, type, idem: (($i > $i > $o) > $i > $i > $o) > $o).
% 0.21/0.36 thf(decl_26, type, infl: (($i > $i > $o) > $i > $i > $o) > $o).
% 0.21/0.36 thf(decl_27, type, mono: (($i > $i > $o) > $i > $i > $o) > $o).
% 0.21/0.36 thf(decl_28, type, refl: ($i > $i > $o) > $o).
% 0.21/0.36 thf(decl_29, type, irrefl: ($i > $i > $o) > $o).
% 0.21/0.36 thf(decl_30, type, rc: ($i > $i > $o) > $i > $i > $o).
% 0.21/0.36 thf(decl_31, type, symm: ($i > $i > $o) > $o).
% 0.21/0.36 thf(decl_32, type, antisymm: ($i > $i > $o) > $o).
% 0.21/0.36 thf(decl_33, type, asymm: ($i > $i > $o) > $o).
% 0.21/0.36 thf(decl_34, type, sc: ($i > $i > $o) > $i > $i > $o).
% 0.21/0.36 thf(decl_35, type, trans: ($i > $i > $o) > $o).
% 0.21/0.36 thf(decl_36, type, tc: ($i > $i > $o) > $i > $i > $o).
% 0.21/0.36 thf(decl_37, type, trc: ($i > $i > $o) > $i > $i > $o).
% 0.21/0.36 thf(decl_38, type, trsc: ($i > $i > $o) > $i > $i > $o).
% 0.21/0.36 thf(decl_39, type, po: ($i > $i > $o) > $o).
% 0.21/0.36 thf(decl_40, type, so: ($i > $i > $o) > $o).
% 0.21/0.36 thf(decl_41, type, total: ($i > $i > $o) > $o).
% 0.21/0.36 thf(decl_42, type, term: ($i > $i > $o) > $o).
% 0.21/0.36 thf(decl_43, type, ind: ($i > $i > $o) > $o).
% 0.21/0.36 thf(decl_44, type, innf: ($i > $i > $o) > $i > $o).
% 0.21/0.36 thf(decl_45, type, nfof: ($i > $i > $o) > $i > $i > $o).
% 0.21/0.36 thf(decl_46, type, norm: ($i > $i > $o) > $o).
% 0.21/0.36 thf(decl_47, type, join: ($i > $i > $o) > $i > $i > $o).
% 0.21/0.36 thf(decl_48, type, lconfl: ($i > $i > $o) > $o).
% 0.21/0.36 thf(decl_49, type, sconfl: ($i > $i > $o) > $o).
% 0.21/0.36 thf(decl_50, type, confl: ($i > $i > $o) > $o).
% 0.21/0.36 thf(decl_51, type, cr: ($i > $i > $o) > $o).
% 0.21/0.36 thf(decl_52, type, d2unsorted: d_unsorted > $i).
% 0.21/0.36 thf(decl_53, type, d_unsorted_0: d_unsorted).
% 0.21/0.36 thf(decl_54, type, epred1_3: $i > $i > ($i > $i > $o) > $o).
% 0.21/0.36 thf(decl_55, type, epred2_3: $i > $i > ($i > $i > $o) > $o).
% 0.21/0.36 thf(decl_56, type, epred3_5: ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i > $o).
% 0.21/0.36 thf(decl_58, type, epred5_6: ($i > $i > $o) > ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i > $o).
% 0.21/0.36 thf(decl_60, type, epred7_6: ($i > $i > $o) > ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i > $o).
% 0.21/0.36 thf(decl_62, type, epred9_4: ($i > $i > $o) > ($i > $i > $o) > $i > $i > $o).
% 0.21/0.36 thf(decl_63, type, esk1_1: $i > d_unsorted).
% 0.21/0.36 thf(decl_64, type, esk2_2: ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_65, type, esk3_2: ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_66, type, epred10_1: (($i > $i > $o) > $i > $i > $o) > $i > $i > $o).
% 0.21/0.36 thf(decl_67, type, epred11_1: (($i > $i > $o) > $i > $i > $o) > $i > $i > $o).
% 0.21/0.36 thf(decl_68, type, esk4_1: (($i > $i > $o) > $i > $i > $o) > $i).
% 0.21/0.36 thf(decl_69, type, esk5_1: (($i > $i > $o) > $i > $i > $o) > $i).
% 0.21/0.36 thf(decl_70, type, esk6_5: (($i > $i > $o) > $i > $i > $o) > ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i).
% 0.21/0.36 thf(decl_71, type, esk7_5: (($i > $i > $o) > $i > $i > $o) > ($i > $i > $o) > ($i > $i > $o) > $i > $i > $i).
% 0.21/0.36 thf(decl_72, type, epred12_1: (($i > $i > $o) > $i > $i > $o) > $i > $i > $o).
% 0.21/0.36 thf(decl_73, type, epred13_1: (($i > $i > $o) > $i > $i > $o) > $i > $i > $o).
% 0.21/0.36 thf(decl_74, type, esk8_1: (($i > $i > $o) > $i > $i > $o) > $i).
% 0.21/0.36 thf(decl_75, type, esk9_1: (($i > $i > $o) > $i > $i > $o) > $i).
% 0.21/0.36 thf(decl_76, type, esk10_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_77, type, esk11_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_78, type, esk12_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_79, type, esk13_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_80, type, esk14_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_81, type, esk15_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_82, type, esk16_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_83, type, esk17_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_84, type, esk18_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_85, type, esk19_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_86, type, esk20_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_87, type, esk21_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_88, type, esk22_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_89, type, esk23_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_90, type, esk24_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_91, type, esk25_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_92, type, epred14_3: ($i > $i > $o) > $i > $i > $i > $i > $o).
% 0.21/0.36 thf(decl_93, type, esk26_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_94, type, esk27_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_95, type, esk28_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_96, type, esk29_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_97, type, esk30_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_98, type, epred15_3: ($i > $i > $o) > $i > $i > $i > $i > $o).
% 0.21/0.36 thf(decl_99, type, esk31_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_100, type, esk32_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_101, type, esk33_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_102, type, esk34_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_103, type, esk35_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_104, type, esk36_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_105, type, esk37_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_106, type, esk38_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_107, type, esk39_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_108, type, esk40_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_109, type, esk41_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_110, type, esk42_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_111, type, esk43_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_112, type, esk44_2: ($i > $i > $o) > ($i > $o) > $i).
% 0.21/0.36 thf(decl_113, type, epred16_1: ($i > $i > $o) > $i > $o).
% 0.21/0.36 thf(decl_114, type, esk45_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_115, type, esk46_2: ($i > $i > $o) > $i > $i).
% 0.21/0.36 thf(decl_116, type, esk47_2: ($i > $i > $o) > ($i > $o) > $i).
% 0.21/0.36 thf(decl_117, type, epred17_3: ($i > $i > $o) > ($i > $o) > $i > $i > $i > $o).
% 0.21/0.36 thf(decl_118, type, epred18_1: ($i > $i > $o) > $i > $o).
% 0.21/0.36 thf(decl_119, type, esk48_2: ($i > $i > $o) > $i > $i).
% 0.21/0.36 thf(decl_120, type, esk49_3: ($i > $i > $o) > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_121, type, esk50_3: ($i > $i > $o) > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_122, type, esk51_3: ($i > $i > $o) > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_123, type, esk52_3: ($i > $i > $o) > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_124, type, esk53_3: ($i > $i > $o) > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_125, type, esk54_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_126, type, esk55_2: ($i > $i > $o) > $i > $i).
% 0.21/0.36 thf(decl_127, type, esk56_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_128, type, esk57_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_129, type, esk58_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_130, type, esk59_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_131, type, esk60_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_132, type, epred19_3: ($i > $i > $o) > $i > $i > $i > $i > $o).
% 0.21/0.36 thf(decl_133, type, esk61_3: ($i > $i > $o) > $i > $i > $i).
% 0.21/0.36 thf(decl_134, type, esk62_2: ($i > $i > $o) > $i > $i).
% 0.21/0.36 thf(decl_135, type, esk63_3: ($i > $i > $o) > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_136, type, esk64_3: ($i > $i > $o) > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_137, type, esk65_3: ($i > $i > $o) > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_138, type, esk66_3: ($i > $i > $o) > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_139, type, esk67_3: ($i > $i > $o) > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_140, type, esk68_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_141, type, esk69_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_142, type, epred20_2: ($i > $i > $o) > $i > $i > $i > $o).
% 0.21/0.36 thf(decl_143, type, esk70_2: ($i > $i > $o) > $i > $i).
% 0.21/0.36 thf(decl_144, type, esk71_3: ($i > $i > $o) > $i > $i > $i).
% 0.21/0.36 thf(decl_145, type, esk72_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_146, type, esk73_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_147, type, esk74_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_148, type, esk75_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_149, type, esk76_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_150, type, esk77_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_151, type, esk78_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_152, type, esk79_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_153, type, esk80_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_154, type, esk81_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_155, type, epred21_4: ($i > $i > $o) > $i > $i > $i > $i > $i > $o).
% 0.21/0.36 thf(decl_156, type, epred22_4: ($i > $i > $o) > $i > $i > $i > $i > $i > $o).
% 0.21/0.36 thf(decl_157, type, esk82_6: ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_158, type, esk83_6: ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_159, type, esk84_6: ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_160, type, esk85_6: ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_161, type, esk86_6: ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_162, type, esk87_6: ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_163, type, esk88_6: ($i > $i > $o) > $i > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_164, type, esk89_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_165, type, esk90_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_166, type, esk91_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_167, type, epred23_1: ($i > $i > $o) > $i > $i > $o).
% 0.21/0.36 thf(decl_168, type, epred24_1: ($i > $i > $o) > $i > $i > $o).
% 0.21/0.36 thf(decl_169, type, esk92_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_170, type, esk93_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_171, type, esk94_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_172, type, epred25_1: ($i > $i > $o) > $i > $i > $o).
% 0.21/0.36 thf(decl_173, type, epred26_1: ($i > $i > $o) > $i > $i > $o).
% 0.21/0.36 thf(decl_174, type, esk95_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_175, type, esk96_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_176, type, esk97_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_177, type, epred27_1: ($i > $i > $o) > $i > $i > $o).
% 0.21/0.36 thf(decl_178, type, epred28_1: ($i > $i > $o) > $i > $i > $o).
% 0.21/0.36 thf(decl_179, type, esk98_5: ($i > $i > $o) > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_180, type, esk99_5: ($i > $i > $o) > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_181, type, esk100_5: ($i > $i > $o) > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_182, type, esk101_5: ($i > $i > $o) > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_183, type, esk102_5: ($i > $i > $o) > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_184, type, esk103_5: ($i > $i > $o) > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_185, type, esk104_5: ($i > $i > $o) > $i > $i > ($i > $i > $o) > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_186, type, esk105_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_187, type, esk106_1: ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_188, type, epred29_1: ($i > $i > $o) > $i > $i > $o).
% 0.21/0.36 thf(decl_189, type, epred30_1: ($i > $i > $o) > $i > $i > $o).
% 0.21/0.36 thf(decl_190, type, epred31_0: $i > $i > $o).
% 0.21/0.36 thf(decl_191, type, esk107_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_192, type, esk108_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_193, type, esk109_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_194, type, esk110_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_195, type, esk111_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_196, type, esk112_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_197, type, esk113_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_198, type, esk114_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_199, type, esk115_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_200, type, esk116_4: ($i > $i > $o) > $i > $i > ($i > $i > $o) > $i).
% 0.21/0.36 thf(decl_201, type, epred32_3: ($i > $i > $o) > $i > $i > $i > $i > $o).
% 0.21/0.36 thf(decl_202, type, epred33_3: ($i > $i > $o) > $i > $i > $i > $i > $o).
% 0.21/0.36 thf(decl_323, type, esk222_0: $i).
% 0.21/0.36 thf(decl_324, type, esk49_0: $i).
% 0.21/0.36 thf(decl_325, type, esk50_0: $i).
% 0.21/0.36 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.4Y9RVdFgpd/E---3.1_1438329.p', sev441_1)).
% 0.21/0.36 thf(transitive_reflexive_symmetric_closure, conjecture, ((trsc)=(^[X5:$i > $i > $o]:(sc @ (rc @ (tc @ X5))))), file('/export/starexec/sandbox2/tmp/tmp.4Y9RVdFgpd/E---3.1_1438329.p', transitive_reflexive_symmetric_closure)).
% 0.21/0.36 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.21/0.36 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.21/0.36 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.21/0.36 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.21/0.36 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.21/0.36 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.21/0.36 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.21/0.36 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.21/0.36 thf(c_0_10, negated_conjecture, ~(((trsc)=(^[X5:$i > $i > $o]:(sc @ (rc @ (tc @ X5)))))), inference(assume_negation,[status(cth)],[transitive_reflexive_symmetric_closure])).
% 0.21/0.36 thf(c_0_11, plain, ![X1:$i]:(((X1)=(d2unsorted @ (esk1_1 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.21/0.36 thf(c_0_12, plain, ![X2:d_unsorted]:(((X2)=(d_unsorted_0))), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.21/0.36 thf(c_0_13, negated_conjecture, ~(![X91:$i > $i > $o]:(((trsc @ X91)=(sc @ (rc @ (tc @ X91)))))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_10])])).
% 0.21/0.36 thf(c_0_14, plain, ![X5:$i > $i > $o]:(((symm @ X5)|~((X5 @ (esk13_1 @ X5) @ (esk12_1 @ X5))))), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.21/0.36 thf(c_0_15, plain, ![X1:$i]:(((d2unsorted @ d_unsorted_0)=(X1))), inference(rw,[status(thm)],[c_0_11, c_0_12])).
% 0.21/0.36 thf(c_0_16, negated_conjecture, ((trsc @ epred31_0)!=(sc @ (rc @ (tc @ epred31_0)))), inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_13])])])])).
% 0.21/0.36 thf(c_0_17, plain, ![X5:$i > $i > $o]:(((X5 @ (esk12_1 @ X5) @ (esk13_1 @ X5))|(symm @ X5))), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.21/0.36 thf(c_0_18, plain, ![X5:$i > $i > $o]:(((symm @ X5)|~((X5 @ esk222_0 @ esk222_0)))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_14, c_0_15]), c_0_15]), c_0_15]), c_0_15])).
% 0.21/0.36 thf(c_0_19, negated_conjecture, ((trsc @ epred31_0)!=(sc @ (rc @ (tc @ epred31_0)))), inference(split_conjunct,[status(thm)],[c_0_16])).
% 0.21/0.36 thf(c_0_20, plain, ![X5:$i > $i > $o]:(((antisymm @ X5)|((esk14_1 @ X5)!=(esk15_1 @ X5)))), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.21/0.36 thf(c_0_21, plain, ![X1:$i, X5:$i > $i > $o, X7:$i]:(((X5 @ X7 @ X1)|~((symm @ X5))|~((X5 @ X1 @ X7)))), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.21/0.36 thf(c_0_22, plain, ![X5:$i > $i > $o]:((symm @ X5)), inference(csr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_17, c_0_15]), c_0_15]), c_0_15]), c_0_15]), c_0_18])).
% 0.21/0.36 thf(c_0_23, negated_conjecture, ((sc @ (rc @ (tc @ epred31_0)) @ esk49_0 @ esk50_0)<~>(trsc @ epred31_0 @ esk49_0 @ esk50_0)), inference(neg_ext,[status(thm)],[c_0_19])).
% 0.21/0.36 thf(c_0_24, plain, ![X5:$i > $i > $o]:(((total @ X5)|((esk42_1 @ X5)!=(esk43_1 @ X5)))), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.21/0.36 thf(c_0_25, plain, ![X7:$i, X5:$i > $i > $o, X1:$i]:((((X1)=(X7))|~((antisymm @ X5))|~((X5 @ X1 @ X7))|~((X5 @ X7 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.21/0.36 thf(c_0_26, plain, ![X5:$i > $i > $o]:((antisymm @ X5)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_20, c_0_15]), c_0_15]), c_0_15]), c_0_15])])).
% 0.21/0.36 thf(c_0_27, plain, ![X7:$i, X5:$i > $i > $o, X1:$i]:(((X5 @ X1 @ X7)|~((X5 @ X7 @ X1)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_21, c_0_22])])).
% 0.21/0.36 thf(c_0_28, negated_conjecture, (~((sc @ (rc @ (tc @ epred31_0)) @ esk49_0 @ esk50_0))|~((trsc @ epred31_0 @ esk49_0 @ esk50_0))), inference(dynamic_cnf,[status(thm)],[c_0_23])).
% 0.21/0.36 thf(c_0_29, plain, ![X1:$i, X5:$i > $i > $o, X7:$i]:(((sc @ X5 @ X7 @ X1)|~((X5 @ X1 @ X7)))), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.21/0.36 thf(c_0_30, plain, ![X1:$i, X7:$i, X5:$i > $i > $o]:((((X1)=(X7))|(X5 @ X1 @ X7)|(X5 @ X7 @ X1)|~((total @ X5)))), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.21/0.36 thf(c_0_31, plain, ![X5:$i > $i > $o]:((total @ X5)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_24, c_0_15]), c_0_15]), c_0_15]), c_0_15])])).
% 0.21/0.36 thf(c_0_32, plain, ![X7:$i, X5:$i > $i > $o, X1:$i]:((((X1)=(X7))|~((X5 @ X7 @ X1)))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_25, c_0_26])]), c_0_27])).
% 0.21/0.36 thf(c_0_33, negated_conjecture, (~((rc @ (tc @ epred31_0) @ esk50_0 @ esk49_0))|~((trsc @ epred31_0 @ esk49_0 @ esk50_0))), inference(spm,[status(thm)],[c_0_28, c_0_29])).
% 0.21/0.36 thf(c_0_34, plain, ![X1:$i, X7:$i]:(((X1)=(X7))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_30, c_0_31])]), c_0_32]), c_0_32])).
% 0.21/0.36 thf(c_0_35, plain, ![X1:$i, X5:$i > $i > $o, X7:$i]:(((rc @ X5 @ X1 @ X7)|((X1)!=(X7)))), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.21/0.36 thf(c_0_36, plain, ![X432:$i > $i > $o, X433:$i, X434:$i, X435:$i > $i > $o, X441:$i > $i > $o, X447:$i > $i > $o, X448:$i, X449:$i, X451:$i, X452:$i, X453:$i, X454:$i, X455:$i, X457:$i, X458:$i, X459:$i, X460:$i, X461:$i]:((((((((((X432 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ (esk112_4 @ X432 @ X433 @ X434 @ X441) @ (esk113_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|((X432 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ (esk107_4 @ X432 @ X433 @ X434 @ X435) @ (esk108_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))&(~(X441 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ (esk112_4 @ X432 @ X433 @ X434 @ X441) @ (esk113_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|((X432 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ (esk107_4 @ X432 @ X433 @ X434 @ X435) @ (esk108_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432)))&(((X432 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ (esk113_4 @ X432 @ X433 @ X434 @ X441) @ (esk114_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|((X432 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ (esk107_4 @ X432 @ X433 @ X434 @ X435) @ (esk108_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))&(~(X441 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ (esk113_4 @ X432 @ X433 @ X434 @ X441) @ (esk114_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|((X432 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ (esk107_4 @ X432 @ X433 @ X434 @ X435) @ (esk108_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))))&(((X432 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|~(X441 @ (esk112_4 @ X432 @ X433 @ X434 @ X441) @ (esk114_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|((X432 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ (esk107_4 @ X432 @ X433 @ X434 @ X435) @ (esk108_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))&(~(X441 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|~(X441 @ (esk112_4 @ X432 @ X433 @ X434 @ X441) @ (esk114_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|((X432 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ (esk107_4 @ X432 @ X433 @ X434 @ X435) @ (esk108_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))))&(((((X432 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ (esk112_4 @ X432 @ X433 @ X434 @ X441) @ (esk113_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|(~(X435 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ (esk107_4 @ X432 @ X433 @ X434 @ X435) @ (esk108_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))&(~(X441 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ (esk112_4 @ X432 @ X433 @ X434 @ X441) @ (esk113_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|(~(X435 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ (esk107_4 @ X432 @ X433 @ X434 @ X435) @ (esk108_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432)))&(((X432 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ (esk113_4 @ X432 @ X433 @ X434 @ X441) @ (esk114_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|(~(X435 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ (esk107_4 @ X432 @ X433 @ X434 @ X435) @ (esk108_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))&(~(X441 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ (esk113_4 @ X432 @ X433 @ X434 @ X441) @ (esk114_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|(~(X435 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ (esk107_4 @ X432 @ X433 @ X434 @ X435) @ (esk108_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))))&(((X432 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|~(X441 @ (esk112_4 @ X432 @ X433 @ X434 @ X441) @ (esk114_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|(~(X435 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ (esk107_4 @ X432 @ X433 @ X434 @ X435) @ (esk108_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))&(~(X441 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|~(X441 @ (esk112_4 @ X432 @ X433 @ X434 @ X441) @ (esk114_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|(~(X435 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ (esk107_4 @ X432 @ X433 @ X434 @ X435) @ (esk108_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432)))))&((((((X432 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ (esk112_4 @ X432 @ X433 @ X434 @ X441) @ (esk113_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|((X432 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ (esk108_4 @ X432 @ X433 @ X434 @ X435) @ (esk109_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))&(~(X441 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ (esk112_4 @ X432 @ X433 @ X434 @ X441) @ (esk113_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|((X432 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ (esk108_4 @ X432 @ X433 @ X434 @ X435) @ (esk109_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432)))&(((X432 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ (esk113_4 @ X432 @ X433 @ X434 @ X441) @ (esk114_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|((X432 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ (esk108_4 @ X432 @ X433 @ X434 @ X435) @ (esk109_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))&(~(X441 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ (esk113_4 @ X432 @ X433 @ X434 @ X441) @ (esk114_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|((X432 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ (esk108_4 @ X432 @ X433 @ X434 @ X435) @ (esk109_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))))&(((X432 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|~(X441 @ (esk112_4 @ X432 @ X433 @ X434 @ X441) @ (esk114_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|((X432 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ (esk108_4 @ X432 @ X433 @ X434 @ X435) @ (esk109_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))&(~(X441 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|~(X441 @ (esk112_4 @ X432 @ X433 @ X434 @ X441) @ (esk114_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|((X432 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ (esk108_4 @ X432 @ X433 @ X434 @ X435) @ (esk109_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))))&(((((X432 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ (esk112_4 @ X432 @ X433 @ X434 @ X441) @ (esk113_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|(~(X435 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ (esk108_4 @ X432 @ X433 @ X434 @ X435) @ (esk109_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))&(~(X441 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ (esk112_4 @ X432 @ X433 @ X434 @ X441) @ (esk113_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|(~(X435 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ (esk108_4 @ X432 @ X433 @ X434 @ X435) @ (esk109_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432)))&(((X432 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ (esk113_4 @ X432 @ X433 @ X434 @ X441) @ (esk114_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|(~(X435 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ (esk108_4 @ X432 @ X433 @ X434 @ X435) @ (esk109_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))&(~(X441 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ (esk113_4 @ X432 @ X433 @ X434 @ X441) @ (esk114_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|(~(X435 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ (esk108_4 @ X432 @ X433 @ X434 @ X435) @ (esk109_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))))&(((X432 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|~(X441 @ (esk112_4 @ X432 @ X433 @ X434 @ X441) @ (esk114_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|(~(X435 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ (esk108_4 @ X432 @ X433 @ X434 @ X435) @ (esk109_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))&(~(X441 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|~(X441 @ (esk112_4 @ X432 @ X433 @ X434 @ X441) @ (esk114_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|(~(X435 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ (esk108_4 @ X432 @ X433 @ X434 @ X435) @ (esk109_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))))))&((((((X432 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ (esk112_4 @ X432 @ X433 @ X434 @ X441) @ (esk113_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|((X432 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|~(X435 @ (esk107_4 @ X432 @ X433 @ X434 @ X435) @ (esk109_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))&(~(X441 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ (esk112_4 @ X432 @ X433 @ X434 @ X441) @ (esk113_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|((X432 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|~(X435 @ (esk107_4 @ X432 @ X433 @ X434 @ X435) @ (esk109_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432)))&(((X432 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ (esk113_4 @ X432 @ X433 @ X434 @ X441) @ (esk114_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|((X432 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|~(X435 @ (esk107_4 @ X432 @ X433 @ X434 @ X435) @ (esk109_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))&(~(X441 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ (esk113_4 @ X432 @ X433 @ X434 @ X441) @ (esk114_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|((X432 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|~(X435 @ (esk107_4 @ X432 @ X433 @ X434 @ X435) @ (esk109_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))))&(((X432 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|~(X441 @ (esk112_4 @ X432 @ X433 @ X434 @ X441) @ (esk114_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|((X432 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|~(X435 @ (esk107_4 @ X432 @ X433 @ X434 @ X435) @ (esk109_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))&(~(X441 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|~(X441 @ (esk112_4 @ X432 @ X433 @ X434 @ X441) @ (esk114_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|((X432 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|~(X435 @ (esk107_4 @ X432 @ X433 @ X434 @ X435) @ (esk109_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))))&(((((X432 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ (esk112_4 @ X432 @ X433 @ X434 @ X441) @ (esk113_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|(~(X435 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|~(X435 @ (esk107_4 @ X432 @ X433 @ X434 @ X435) @ (esk109_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))&(~(X441 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ (esk112_4 @ X432 @ X433 @ X434 @ X441) @ (esk113_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|(~(X435 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|~(X435 @ (esk107_4 @ X432 @ X433 @ X434 @ X435) @ (esk109_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432)))&(((X432 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ (esk113_4 @ X432 @ X433 @ X434 @ X441) @ (esk114_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|(~(X435 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|~(X435 @ (esk107_4 @ X432 @ X433 @ X434 @ X435) @ (esk109_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))&(~(X441 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ (esk113_4 @ X432 @ X433 @ X434 @ X441) @ (esk114_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|(~(X435 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|~(X435 @ (esk107_4 @ X432 @ X433 @ X434 @ X435) @ (esk109_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))))&(((X432 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|~(X441 @ (esk112_4 @ X432 @ X433 @ X434 @ X441) @ (esk114_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|(~(X435 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|~(X435 @ (esk107_4 @ X432 @ X433 @ X434 @ X435) @ (esk109_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))&(~(X441 @ (esk115_4 @ X432 @ X433 @ X434 @ X441) @ (esk116_4 @ X432 @ X433 @ X434 @ X441))|~(X441 @ (esk112_4 @ X432 @ X433 @ X434 @ X441) @ (esk114_4 @ X432 @ X433 @ X434 @ X441))|(X441 @ X433 @ X434)|(~(X435 @ (esk110_4 @ X432 @ X433 @ X434 @ X435) @ (esk111_4 @ X432 @ X433 @ X434 @ X435))|~(X435 @ (esk107_4 @ X432 @ X433 @ X434 @ X435) @ (esk109_4 @ X432 @ X433 @ X434 @ X435))|(X435 @ X434 @ X433)|((X433)=(X434)))|~(epred1_3 @ X434 @ X433 @ X432))))))&(((((X448)!=(X449))|(epred1_3 @ X449 @ X448 @ X447))&(((~(epred32_3 @ X447 @ X448 @ X449 @ X451 @ X452)|~(epred32_3 @ X447 @ X448 @ X449 @ X452 @ X453)|(epred32_3 @ X447 @ X448 @ X449 @ X451 @ X453)|(epred1_3 @ X449 @ X448 @ X447))&(~(X447 @ X454 @ X455)|(epred32_3 @ X447 @ X448 @ X449 @ X454 @ X455)|(epred1_3 @ X449 @ X448 @ X447)))&(~(epred32_3 @ X447 @ X448 @ X449 @ X449 @ X448)|(epred1_3 @ X449 @ X448 @ X447))))&(((~(epred33_3 @ X447 @ X448 @ X449 @ X457 @ X458)|~(epred33_3 @ X447 @ X448 @ X449 @ X458 @ X459)|(epred33_3 @ X447 @ X448 @ X449 @ X457 @ X459)|(epred1_3 @ X449 @ X448 @ X447))&(~(X447 @ X460 @ X461)|(epred33_3 @ X447 @ X448 @ X449 @ X460 @ X461)|(epred1_3 @ X449 @ X448 @ X447)))&(~(epred33_3 @ X447 @ X448 @ X449 @ X448 @ X449)|(epred1_3 @ X449 @ X448 @ X447)))))), 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_2])])])])])])])).
% 0.21/0.36 thf(c_0_37, negated_conjecture, ![X1:$i]:((~((rc @ (tc @ epred31_0) @ esk50_0 @ X1))|~((trsc @ epred31_0 @ X1 @ esk50_0)))), inference(spm,[status(thm)],[c_0_33, c_0_34])).
% 0.21/0.36 thf(c_0_38, plain, ![X5:$i > $i > $o, X1:$i]:((rc @ X5 @ X1 @ X1)), inference(er,[status(thm)],[c_0_35])).
% 0.21/0.36 thf(c_0_39, plain, ![X1:$i, X5:$i > $i > $o, X7:$i]:(((epred1_3 @ X7 @ X1 @ X5)|((X1)!=(X7)))), inference(split_conjunct,[status(thm)],[c_0_36])).
% 0.21/0.36 thf(c_0_40, negated_conjecture, ~((trsc @ epred31_0 @ esk50_0 @ esk50_0)), inference(spm,[status(thm)],[c_0_37, c_0_38])).
% 0.21/0.36 thf(c_0_41, plain, ![X1:$i, X7:$i, X5:$i > $i > $o]:(((trsc @ X5 @ X7 @ X1)|~((epred1_3 @ X1 @ X7 @ X5)))), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.21/0.36 thf(c_0_42, plain, ![X1:$i, X5:$i > $i > $o]:((epred1_3 @ X1 @ X1 @ X5)), inference(er,[status(thm)],[c_0_39])).
% 0.21/0.36 thf(c_0_43, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_40, c_0_41]), c_0_42])]), ['proof']).
% 0.21/0.36 % SZS output end CNFRefutation
% 0.21/0.36 % Parsed axioms : 35
% 0.21/0.36 % Removed by relevancy pruning/SinE : 0
% 0.21/0.36 % Initial clauses : 815
% 0.21/0.36 % Removed in clause preprocessing : 45
% 0.21/0.36 % Initial clauses in saturation : 770
% 0.21/0.36 % Processed clauses : 876
% 0.21/0.36 % ...of these trivial : 246
% 0.21/0.36 % ...subsumed : 367
% 0.21/0.36 % ...remaining for further processing : 263
% 0.21/0.36 % Other redundant clauses eliminated : 9
% 0.21/0.36 % Clauses deleted for lack of memory : 0
% 0.21/0.36 % Backward-subsumed : 14
% 0.21/0.36 % Backward-rewritten : 11
% 0.21/0.36 % Generated clauses : 152
% 0.21/0.36 % ...of the previous two non-redundant : 147
% 0.21/0.36 % ...aggressively subsumed : 0
% 0.21/0.36 % Contextual simplify-reflections : 18
% 0.21/0.36 % Paramodulations : 125
% 0.21/0.36 % Factorizations : 0
% 0.21/0.36 % NegExts : 6
% 0.21/0.36 % Equation resolutions : 9
% 0.21/0.36 % Disequality decompositions : 0
% 0.21/0.36 % Total rewrite steps : 3788
% 0.21/0.36 % ...of those cached : 3393
% 0.21/0.36 % Propositional unsat checks : 0
% 0.21/0.36 % Propositional check models : 0
% 0.21/0.36 % Propositional check unsatisfiable : 0
% 0.21/0.36 % Propositional clauses : 0
% 0.21/0.36 % Propositional clauses after purity: 0
% 0.21/0.36 % Propositional unsat core size : 0
% 0.21/0.36 % Propositional preprocessing time : 0.000
% 0.21/0.36 % Propositional encoding time : 0.000
% 0.21/0.36 % Propositional solver time : 0.000
% 0.21/0.36 % Success case prop preproc time : 0.000
% 0.21/0.36 % Success case prop encoding time : 0.000
% 0.21/0.36 % Success case prop solver time : 0.000
% 0.21/0.36 % Current number of processed clauses : 84
% 0.21/0.36 % Positive orientable unit clauses : 23
% 0.21/0.36 % Positive unorientable unit clauses: 2
% 0.21/0.36 % Negative unit clauses : 5
% 0.21/0.36 % Non-unit-clauses : 54
% 0.21/0.36 % Current number of unprocessed clauses: 173
% 0.21/0.36 % ...number of literals in the above : 456
% 0.21/0.36 % Current number of archived formulas : 0
% 0.21/0.36 % Current number of archived clauses : 170
% 0.21/0.36 % Clause-clause subsumption calls (NU) : 19993
% 0.21/0.36 % Rec. Clause-clause subsumption calls : 6872
% 0.21/0.36 % Non-unit clause-clause subsumptions : 126
% 0.21/0.36 % Unit Clause-clause subsumption calls : 249
% 0.21/0.36 % Rewrite failures with RHS unbound : 0
% 0.21/0.36 % BW rewrite match attempts : 471
% 0.21/0.36 % BW rewrite match successes : 28
% 0.21/0.36 % Condensation attempts : 876
% 0.21/0.36 % Condensation successes : 1
% 0.21/0.36 % Termbank termtop insertions : 127963
% 0.21/0.36 % Search garbage collected termcells : 13275
% 0.21/0.36
% 0.21/0.36 % -------------------------------------------------
% 0.21/0.36 % User time : 0.092 s
% 0.21/0.36 % System time : 0.010 s
% 0.21/0.36 % Total time : 0.103 s
% 0.21/0.36 % Maximum resident set size: 6312 pages
% 0.21/0.36
% 0.21/0.36 % -------------------------------------------------
% 0.21/0.36 % User time : 0.136 s
% 0.21/0.36 % System time : 0.023 s
% 0.21/0.36 % Total time : 0.158 s
% 0.21/0.36 % Maximum resident set size: 4864 pages
% 0.21/0.36 % E exiting
%------------------------------------------------------------------------------