%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SYO904^12 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:43:33 AM UTC 2026
% Result : ContradictoryAxioms 0.54s 0.46s
% Output : CNFRefutation 0.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO904^12 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.19 % Computer : n018.cluster.edu
% 0.11/0.19 % Model : x86_64 x86_64
% 0.11/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.19 % Memory : 8046.5625MB
% 0.11/0.19 % OS : Linux 6.8.0-71-generic
% 0.11/0.19 % CPULimit : 300
% 0.11/0.19 % WCLimit : 300
% 0.11/0.19 % DateTime : Tue Sep 29 17:28:56 UTC 2026
% 0.11/0.19 % CPUTime :
% 0.11/0.19 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.24 Running higher-order theorem proving
% 0.11/0.27 Running: /export/starexec/sandbox2/solver/bin/eprover-ho --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox2/tmp/tmp.9dWpSZHlBe/E---3.1_383987.p
% 0.54/0.46 % Version: 3.5.1-ho
% 0.54/0.46 % Preprocessing class: HSLSSMSSMLLNHSN.
% 0.54/0.46 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.54/0.46 % Starting almost_fo_3 with 1500s (5) cores
% 0.54/0.46 % Starting sh10 with 300s (1) cores
% 0.54/0.46 % Starting new_ho_16 with 300s (1) cores
% 0.54/0.46 % Starting post_as_ho11 with 300s (1) cores
% 0.54/0.46 % new_ho_16 with pid 384002 completed with status 9
% 0.54/0.46 % almost_fo_3 with pid 384000 completed with status 0
% 0.54/0.46 % Result found by almost_fo_3
% 0.54/0.46 % Preprocessing class: HSLSSMSSMLLNHSN.
% 0.54/0.46 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.54/0.46 % Starting almost_fo_3 with 1500s (5) cores
% 0.54/0.46 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.54/0.46 % No SInE strategy applied
% 0.54/0.46 % Search class: HGHNF-FSLF33-SHSSMFNN
% 0.54/0.46 % partial match(1): HGHNS-FSLF33-SHSSMFNN
% 0.54/0.46 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.54/0.46 % Starting SubtermCWHack with 136s (1) cores
% 0.54/0.46 % Starting almost_fo_3 with 151s (1) cores
% 0.54/0.46 % Starting new_ho_16 with 136s (1) cores
% 0.54/0.46 % Starting sh5l with 136s (1) cores
% 0.54/0.46 % Starting ehoh_best8_lambda with 136s (1) cores
% 0.54/0.46 % almost_fo_3 with pid 384019 completed with status 0
% 0.54/0.46 % Result found by almost_fo_3
% 0.54/0.46 % Preprocessing class: HSLSSMSSMLLNHSN.
% 0.54/0.46 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.54/0.46 % Starting almost_fo_3 with 1500s (5) cores
% 0.54/0.46 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.54/0.46 % No SInE strategy applied
% 0.54/0.46 % Search class: HGHNF-FSLF33-SHSSMFNN
% 0.54/0.46 % partial match(1): HGHNS-FSLF33-SHSSMFNN
% 0.54/0.46 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.54/0.46 % Starting SubtermCWHack with 136s (1) cores
% 0.54/0.46 % Starting almost_fo_3 with 151s (1) cores
% 0.54/0.46 % Preprocessing time : 0.009 s
% 0.54/0.46 % Presaturation interreduction done
% 0.54/0.46
% 0.54/0.46 % Proof found!
% 0.54/0.46 % SZS status ContradictoryAxioms
% 0.54/0.46 % SZS output start CNFRefutation
% 0.54/0.46 thf(decl_sort1, type, mworld: $tType).
% 0.54/0.46 thf(decl_23, type, mrel: mworld > mworld > $o).
% 0.54/0.46 thf(decl_24, type, mactual: mworld).
% 0.54/0.46 thf(decl_25, type, mlocal: (mworld > $o) > $o).
% 0.54/0.46 thf(decl_26, type, mnot: (mworld > $o) > mworld > $o).
% 0.54/0.46 thf(decl_27, type, mand: (mworld > $o) > (mworld > $o) > mworld > $o).
% 0.54/0.46 thf(decl_28, type, mor: (mworld > $o) > (mworld > $o) > mworld > $o).
% 0.54/0.46 thf(decl_31, type, mbox: (mworld > $o) > mworld > $o).
% 0.54/0.46 thf(decl_32, type, mdia: (mworld > $o) > mworld > $o).
% 0.54/0.46 thf(decl_35, type, v3: mworld > $o).
% 0.54/0.46 thf(decl_37, type, v5: mworld > $o).
% 0.54/0.46 thf(decl_38, type, v6: mworld > $o).
% 0.54/0.46 thf(decl_39, type, v7: mworld > $o).
% 0.54/0.46 thf(decl_40, type, v8: mworld > $o).
% 0.54/0.46 thf(decl_41, type, v9: mworld > $o).
% 0.54/0.46 thf(decl_45, type, v14: mworld > $o).
% 0.54/0.46 thf(decl_46, type, v13: mworld > $o).
% 0.54/0.46 thf(decl_47, type, v16: mworld > $o).
% 0.54/0.46 thf(decl_48, type, v15: mworld > $o).
% 0.54/0.46 thf(decl_49, type, v18: mworld > $o).
% 0.54/0.46 thf(decl_52, type, v21: mworld > $o).
% 0.54/0.46 thf(decl_54, type, v23: mworld > $o).
% 0.54/0.46 thf(decl_55, type, v22: mworld > $o).
% 0.54/0.46 thf(decl_57, type, v24: mworld > $o).
% 0.54/0.46 thf(decl_59, type, v26: mworld > $o).
% 0.54/0.46 thf(decl_60, type, v28: mworld > $o).
% 0.54/0.46 thf(decl_74, type, epred14_1: mworld > $o).
% 0.54/0.46 thf(decl_76, type, epred16_1: mworld > $o).
% 0.54/0.46 thf(decl_90, type, epred30_1: mworld > $o).
% 0.54/0.46 thf(decl_95, type, esk1_27: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_96, type, esk2_26: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_97, type, esk3_25: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_98, type, esk4_24: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_99, type, esk5_23: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_100, type, esk6_23: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_101, type, esk7_22: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_102, type, esk8_22: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_103, type, esk9_21: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_104, type, esk10_21: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_105, type, esk11_20: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_106, type, esk12_20: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_107, type, esk13_19: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_108, type, esk14_18: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_109, type, esk15_17: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_110, type, esk16_16: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_111, type, esk17_15: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_112, type, esk18_15: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_113, type, esk19_14: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_114, type, esk20_14: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_115, type, esk21_13: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_116, type, esk22_13: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_117, type, esk23_12: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_118, type, esk24_12: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_119, type, esk25_11: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_120, type, esk26_10: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_121, type, esk27_9: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_122, type, esk28_8: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_123, type, esk29_7: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_124, type, esk30_7: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_125, type, esk31_6: mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_126, type, esk32_6: mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_127, type, esk33_5: mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_128, type, esk34_5: mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_129, type, esk35_4: mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_130, type, esk36_4: mworld > mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_131, type, esk37_3: mworld > mworld > mworld > mworld).
% 0.54/0.46 thf(decl_132, type, esk38_2: mworld > mworld > mworld).
% 0.54/0.46 thf(decl_133, type, esk39_1: mworld > mworld).
% 0.54/0.46 thf(decl_134, type, esk40_0: mworld).
% 0.54/0.46 thf(mlocal_def, axiom, ((mlocal)=(^[X1:mworld > $o]:((X1 @ mactual)))), file('/export/starexec/sandbox2/tmp/tmp.9dWpSZHlBe/E---3.1_383987.p', mlocal_def)).
% 0.54/0.46 thf(mnot_def, axiom, ((mnot)=(^[X2:mworld > $o, X3:mworld]:(~((X2 @ X3))))), file('/export/starexec/sandbox2/tmp/tmp.9dWpSZHlBe/E---3.1_383987.p', mnot_def)).
% 0.54/0.46 thf(mor_def, axiom, ((mor)=(^[X2:mworld > $o, X4:mworld > $o, X3:mworld]:((((X2 @ X3))|((X4 @ X3)))))), file('/export/starexec/sandbox2/tmp/tmp.9dWpSZHlBe/E---3.1_383987.p', mor_def)).
% 0.54/0.46 thf(mbox_def, axiom, ((mbox)=(^[X1:mworld > $o, X3:mworld]:(![X5:mworld]:((((mrel @ X3 @ X5))=>((X1 @ X5))))))), file('/export/starexec/sandbox2/tmp/tmp.9dWpSZHlBe/E---3.1_383987.p', mbox_def)).
% 0.54/0.46 thf(mand_def, axiom, ((mand)=(^[X2:mworld > $o, X4:mworld > $o, X3:mworld]:((((X2 @ X3))&((X4 @ X3)))))), file('/export/starexec/sandbox2/tmp/tmp.9dWpSZHlBe/E---3.1_383987.p', mand_def)).
% 0.54/0.46 thf(mdia_def, axiom, ((mdia)=(^[X1:mworld > $o, X3:mworld]:(?[X5:mworld]:((((mrel @ X3 @ X5))&((X1 @ X5))))))), file('/export/starexec/sandbox2/tmp/tmp.9dWpSZHlBe/E---3.1_383987.p', mdia_def)).
% 0.54/0.46 thf(mod22, axiom, (mlocal @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v26) @ (mbox @ (mbox @ (mbox @ (mor @ v23 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v6 @ (mbox @ (mbox @ (mbox @ v3)))))))))))))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.9dWpSZHlBe/E---3.1_383987.p', mod22)).
% 0.54/0.46 thf(mod6, axiom, (mlocal @ (mbox @ (mor @ (mnot @ v28) @ (mbox @ (mbox @ (mor @ v26 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v16) @ (mbox @ (mbox @ (mbox @ (mnot @ v13))))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.9dWpSZHlBe/E---3.1_383987.p', mod6)).
% 0.54/0.46 thf(alt1, axiom, (mlocal @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mand @ (mbox @ (mdia @ (^[X3:mworld]:(($true))))) @ (mdia @ (^[X3:mworld]:(($true)))))) @ (mdia @ (^[X3:mworld]:(($true)))))) @ (mdia @ (^[X3:mworld]:(($true)))))) @ (mand @ (mdia @ v5) @ (mdia @ (mnot @ v5))))) @ (mand @ (mdia @ v6) @ (mdia @ (mnot @ v6))))) @ (mand @ (mdia @ v7) @ (mdia @ (mnot @ v7))))) @ (mand @ (mdia @ v8) @ (mdia @ (mnot @ v8))))) @ (mdia @ (^[X3:mworld]:(($true)))))) @ (mdia @ (^[X3:mworld]:(($true)))))) @ (mdia @ (^[X3:mworld]:(($true)))))) @ (mdia @ (^[X3:mworld]:(($true)))))) @ (mand @ (mdia @ v13) @ (mdia @ (mnot @ v13))))) @ (mand @ (mdia @ v14) @ (mdia @ (mnot @ v14))))) @ (mand @ (mdia @ v15) @ (mdia @ (mnot @ v15))))) @ (mand @ (mdia @ v16) @ (mdia @ (mnot @ v16))))) @ (mdia @ (^[X3:mworld]:(($true)))))) @ (mdia @ (^[X3:mworld]:(($true)))))) @ (mdia @ (^[X3:mworld]:(($true)))))) @ (mdia @ (^[X3:mworld]:(($true)))))) @ (mand @ (mdia @ v21) @ (mdia @ (mnot @ v21))))) @ (mand @ (mdia @ v22) @ (mdia @ (mnot @ v22))))) @ (mand @ (mdia @ v23) @ (mdia @ (mnot @ v23))))) @ (mand @ (mdia @ v24) @ (mdia @ (mnot @ v24))))) @ (mdia @ (^[X3:mworld]:(($true)))))) @ (mdia @ (^[X3:mworld]:(($true)))))) @ (mdia @ (^[X3:mworld]:(($true)))))) @ (mdia @ (^[X3:mworld]:(($true)))))), file('/export/starexec/sandbox2/tmp/tmp.9dWpSZHlBe/E---3.1_383987.p', alt1)).
% 0.54/0.46 thf(mrel_universal, axiom, ![X3:mworld, X5:mworld]:((mrel @ X3 @ X5)), file('/export/starexec/sandbox2/tmp/tmp.9dWpSZHlBe/E---3.1_383987.p', mrel_universal)).
% 0.54/0.46 thf(mod45, axiom, (mlocal @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v16 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v9) @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v6) @ (mbox @ (mbox @ (mbox @ (mnot @ v3))))))))))))))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.9dWpSZHlBe/E---3.1_383987.p', mod45)).
% 0.54/0.46 thf(mod2, axiom, (mlocal @ (mbox @ (mor @ v28 @ (mbox @ (mbox @ (mor @ v26 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v21) @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ v14))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.9dWpSZHlBe/E---3.1_383987.p', mod2)).
% 0.54/0.46 thf(mod4, axiom, (mlocal @ (mbox @ (mor @ v28 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v15) @ (mbox @ (mor @ v14 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ v9)))))))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.9dWpSZHlBe/E---3.1_383987.p', mod4)).
% 0.54/0.46 thf(mod8, axiom, (mlocal @ (mbox @ (mor @ (mnot @ v28) @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v24) @ (mbox @ (mbox @ (mor @ v22 @ (mbox @ (mbox @ (mbox @ (mbox @ v18))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.9dWpSZHlBe/E---3.1_383987.p', mod8)).
% 0.54/0.46 thf(mod24, axiom, (mlocal @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v26) @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v18) @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v7) @ (mbox @ (mnot @ v6)))))))))))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.9dWpSZHlBe/E---3.1_383987.p', mod24)).
% 0.54/0.46 thf(c_0_15, plain, ![X483:mworld]:(((epred14_1 @ X483)<=>![X482:mworld]:(((mrel @ X483 @ X482)=>![X481:mworld]:(((mrel @ X482 @ X481)=>((v23 @ X481)|![X480:mworld]:(((mrel @ X481 @ X480)=>![X479:mworld]:(((mrel @ X480 @ X479)=>![X478:mworld]:(((mrel @ X479 @ X478)=>![X477:mworld]:(((mrel @ X478 @ X477)=>![X476:mworld]:(((mrel @ X477 @ X476)=>![X475:mworld]:(((mrel @ X476 @ X475)=>![X474:mworld]:(((mrel @ X475 @ X474)=>![X473:mworld]:(((mrel @ X474 @ X473)=>![X472:mworld]:(((mrel @ X473 @ X472)=>![X471:mworld]:(((mrel @ X472 @ X471)=>![X470:mworld]:(((mrel @ X471 @ X470)=>![X469:mworld]:(((mrel @ X470 @ X469)=>![X468:mworld]:(((mrel @ X469 @ X468)=>![X467:mworld]:(((mrel @ X468 @ X467)=>![X466:mworld]:(((mrel @ X467 @ X466)=>![X465:mworld]:(((mrel @ X466 @ X465)=>![X464:mworld]:(((mrel @ X465 @ X464)=>((v6 @ X464)|![X463:mworld]:(((mrel @ X464 @ X463)=>![X462:mworld]:(((mrel @ X463 @ X462)=>![X461:mworld]:(((mrel @ X462 @ X461)=>(v3 @ X461))))))))))))))))))))))))))))))))))))))))))))))))), introduced(definition)).
% 0.54/0.46 thf(c_0_16, plain, ((mlocal)=(^[Z0:mworld > $o]:((Z0 @ mactual)))), inference(fof_simplification,[status(thm)],[mlocal_def])).
% 0.54/0.46 thf(c_0_17, plain, ((mnot)=(^[Z0:mworld > $o, Z1:mworld]:(~((Z0 @ Z1))))), inference(fof_simplification,[status(thm)],[mnot_def])).
% 0.54/0.46 thf(c_0_18, plain, ((mor)=(^[Z0:mworld > $o, Z1:mworld > $o, Z2:mworld]:((((Z0 @ Z2))|((Z1 @ Z2)))))), inference(fof_simplification,[status(thm)],[mor_def])).
% 0.54/0.46 thf(c_0_19, plain, ((mbox)=(^[Z0:mworld > $o, Z1:mworld]:(![X5:mworld]:((((mrel @ Z1 @ X5))=>((Z0 @ X5))))))), inference(fof_simplification,[status(thm)],[mbox_def])).
% 0.54/0.46 thf(c_0_20, plain, ((mand)=(^[Z0:mworld > $o, Z1:mworld > $o, Z2:mworld]:((((Z0 @ Z2))&((Z1 @ Z2)))))), inference(fof_simplification,[status(thm)],[mand_def])).
% 0.54/0.46 thf(c_0_21, plain, ((mdia)=(^[Z0:mworld > $o, Z1:mworld]:(?[X5:mworld]:((((mrel @ Z1 @ X5))&((Z0 @ X5))))))), inference(fof_simplification,[status(thm)],[mdia_def])).
% 0.54/0.46 thf(c_0_22, plain, ![X483:mworld]:(((epred14_1 @ X483)=>![X482:mworld]:(((mrel @ X483 @ X482)=>![X481:mworld]:(((mrel @ X482 @ X481)=>((v23 @ X481)|![X480:mworld]:(((mrel @ X481 @ X480)=>![X479:mworld]:(((mrel @ X480 @ X479)=>![X478:mworld]:(((mrel @ X479 @ X478)=>![X477:mworld]:(((mrel @ X478 @ X477)=>![X476:mworld]:(((mrel @ X477 @ X476)=>![X475:mworld]:(((mrel @ X476 @ X475)=>![X474:mworld]:(((mrel @ X475 @ X474)=>![X473:mworld]:(((mrel @ X474 @ X473)=>![X472:mworld]:(((mrel @ X473 @ X472)=>![X471:mworld]:(((mrel @ X472 @ X471)=>![X470:mworld]:(((mrel @ X471 @ X470)=>![X469:mworld]:(((mrel @ X470 @ X469)=>![X468:mworld]:(((mrel @ X469 @ X468)=>![X467:mworld]:(((mrel @ X468 @ X467)=>![X466:mworld]:(((mrel @ X467 @ X466)=>![X465:mworld]:(((mrel @ X466 @ X465)=>![X464:mworld]:(((mrel @ X465 @ X464)=>((v6 @ X464)|![X463:mworld]:(((mrel @ X464 @ X463)=>![X462:mworld]:(((mrel @ X463 @ X462)=>![X461:mworld]:(((mrel @ X462 @ X461)=>(v3 @ X461))))))))))))))))))))))))))))))))))))))))))))))))), inference(split_equiv,[status(thm)],[c_0_15])).
% 0.54/0.46 thf(c_0_23, plain, ![X486:mworld]:(((mrel @ mactual @ X486)=>![X485:mworld]:(((mrel @ X486 @ X485)=>![X484:mworld]:(((mrel @ X485 @ X484)=>(~(v26 @ X484)|![X483:mworld]:(((mrel @ X484 @ X483)=>(epred14_1 @ X483)))))))))), inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[mod22, c_0_16]), c_0_17]), c_0_18]), c_0_19])]), c_0_15])).
% 0.54/0.46 thf(c_0_24, plain, ![X120:mworld]:(((mrel @ mactual @ X120)=>(~(v28 @ X120)|![X119:mworld]:(((mrel @ X120 @ X119)=>![X118:mworld]:(((mrel @ X119 @ X118)=>((v26 @ X118)|![X117:mworld]:(((mrel @ X118 @ X117)=>![X116:mworld]:(((mrel @ X117 @ X116)=>![X115:mworld]:(((mrel @ X116 @ X115)=>![X114:mworld]:(((mrel @ X115 @ X114)=>![X113:mworld]:(((mrel @ X114 @ X113)=>![X112:mworld]:(((mrel @ X113 @ X112)=>![X111:mworld]:(((mrel @ X112 @ X111)=>![X110:mworld]:(((mrel @ X111 @ X110)=>![X109:mworld]:(((mrel @ X110 @ X109)=>![X108:mworld]:(((mrel @ X109 @ X108)=>(~(v16 @ X108)|![X107:mworld]:(((mrel @ X108 @ X107)=>![X106:mworld]:(((mrel @ X107 @ X106)=>![X105:mworld]:(((mrel @ X106 @ X105)=>~(v13 @ X105)))))))))))))))))))))))))))))))))))), inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[mod6, c_0_16]), c_0_17]), c_0_18]), c_0_19])])).
% 0.54/0.46 thf(c_0_25, plain, (![X1215:mworld]:(((mrel @ mactual @ X1215)=>(![X1213:mworld]:(((mrel @ X1215 @ X1213)=>(![X1211:mworld]:(((mrel @ X1213 @ X1211)=>(![X1209:mworld]:(((mrel @ X1211 @ X1209)=>(![X1206:mworld]:(((mrel @ X1209 @ X1206)=>(![X1203:mworld]:(((mrel @ X1206 @ X1203)=>(![X1200:mworld]:(((mrel @ X1203 @ X1200)=>(![X1197:mworld]:(((mrel @ X1200 @ X1197)=>(![X1195:mworld]:(((mrel @ X1197 @ X1195)=>(![X1193:mworld]:(((mrel @ X1195 @ X1193)=>(![X1191:mworld]:(((mrel @ X1193 @ X1191)=>(![X1189:mworld]:(((mrel @ X1191 @ X1189)=>(![X1186:mworld]:(((mrel @ X1189 @ X1186)=>(![X1183:mworld]:(((mrel @ X1186 @ X1183)=>(![X1180:mworld]:(((mrel @ X1183 @ X1180)=>(![X1177:mworld]:(((mrel @ X1180 @ X1177)=>(![X1175:mworld]:(((mrel @ X1177 @ X1175)=>(![X1173:mworld]:(((mrel @ X1175 @ X1173)=>(![X1171:mworld]:(((mrel @ X1173 @ X1171)=>(![X1169:mworld]:(((mrel @ X1171 @ X1169)=>(![X1166:mworld]:(((mrel @ X1169 @ X1166)=>(![X1163:mworld]:(((mrel @ X1166 @ X1163)=>(![X1160:mworld]:(((mrel @ X1163 @ X1160)=>(![X1157:mworld]:(((mrel @ X1160 @ X1157)=>(![X1155:mworld]:(((mrel @ X1157 @ X1155)=>(![X1153:mworld]:(((mrel @ X1155 @ X1153)=>(![X1151:mworld]:(((mrel @ X1153 @ X1151)=>?[X1150:mworld]:(((mrel @ X1151 @ X1150)&$true))))&?[X1152:mworld]:(((mrel @ X1153 @ X1152)&$true)))))&?[X1154:mworld]:(((mrel @ X1155 @ X1154)&$true)))))&?[X1156:mworld]:(((mrel @ X1157 @ X1156)&$true)))))&(?[X1158:mworld]:(((mrel @ X1160 @ X1158)&(v5 @ X1158)))&?[X1159:mworld]:(((mrel @ X1160 @ X1159)&~(v5 @ X1159)))))))&(?[X1161:mworld]:(((mrel @ X1163 @ X1161)&(v6 @ X1161)))&?[X1162:mworld]:(((mrel @ X1163 @ X1162)&~(v6 @ X1162)))))))&(?[X1164:mworld]:(((mrel @ X1166 @ X1164)&(v7 @ X1164)))&?[X1165:mworld]:(((mrel @ X1166 @ X1165)&~(v7 @ X1165)))))))&(?[X1167:mworld]:(((mrel @ X1169 @ X1167)&(v8 @ X1167)))&?[X1168:mworld]:(((mrel @ X1169 @ X1168)&~(v8 @ X1168)))))))&?[X1170:mworld]:(((mrel @ X1171 @ X1170)&$true)))))&?[X1172:mworld]:(((mrel @ X1173 @ X1172)&$true)))))&?[X1174:mworld]:(((mrel @ X1175 @ X1174)&$true)))))&?[X1176:mworld]:(((mrel @ X1177 @ X1176)&$true)))))&(?[X1178:mworld]:(((mrel @ X1180 @ X1178)&(v13 @ X1178)))&?[X1179:mworld]:(((mrel @ X1180 @ X1179)&~(v13 @ X1179)))))))&(?[X1181:mworld]:(((mrel @ X1183 @ X1181)&(v14 @ X1181)))&?[X1182:mworld]:(((mrel @ X1183 @ X1182)&~(v14 @ X1182)))))))&(?[X1184:mworld]:(((mrel @ X1186 @ X1184)&(v15 @ X1184)))&?[X1185:mworld]:(((mrel @ X1186 @ X1185)&~(v15 @ X1185)))))))&(?[X1187:mworld]:(((mrel @ X1189 @ X1187)&(v16 @ X1187)))&?[X1188:mworld]:(((mrel @ X1189 @ X1188)&~(v16 @ X1188)))))))&?[X1190:mworld]:(((mrel @ X1191 @ X1190)&$true)))))&?[X1192:mworld]:(((mrel @ X1193 @ X1192)&$true)))))&?[X1194:mworld]:(((mrel @ X1195 @ X1194)&$true)))))&?[X1196:mworld]:(((mrel @ X1197 @ X1196)&$true)))))&(?[X1198:mworld]:(((mrel @ X1200 @ X1198)&(v21 @ X1198)))&?[X1199:mworld]:(((mrel @ X1200 @ X1199)&~(v21 @ X1199)))))))&(?[X1201:mworld]:(((mrel @ X1203 @ X1201)&(v22 @ X1201)))&?[X1202:mworld]:(((mrel @ X1203 @ X1202)&~(v22 @ X1202)))))))&(?[X1204:mworld]:(((mrel @ X1206 @ X1204)&(v23 @ X1204)))&?[X1205:mworld]:(((mrel @ X1206 @ X1205)&~(v23 @ X1205)))))))&(?[X1207:mworld]:(((mrel @ X1209 @ X1207)&(v24 @ X1207)))&?[X1208:mworld]:(((mrel @ X1209 @ X1208)&~(v24 @ X1208)))))))&?[X1210:mworld]:(((mrel @ X1211 @ X1210)&$true)))))&?[X1212:mworld]:(((mrel @ X1213 @ X1212)&$true)))))&?[X1214:mworld]:(((mrel @ X1215 @ X1214)&$true)))))&?[X1216:mworld]:(((mrel @ mactual @ X1216)&$true))), inference(fof_simplification,[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)],[alt1]), c_0_16]), c_0_17]), c_0_20]), c_0_19]), c_0_21])])).
% 0.54/0.46 thf(c_0_26, plain, ![X1018:mworld]:(((epred30_1 @ X1018)<=>![X1017:mworld]:(((mrel @ X1018 @ X1017)=>![X1016:mworld]:(((mrel @ X1017 @ X1016)=>![X1015:mworld]:(((mrel @ X1016 @ X1015)=>![X1014:mworld]:(((mrel @ X1015 @ X1014)=>![X1013:mworld]:(((mrel @ X1014 @ X1013)=>![X1012:mworld]:(((mrel @ X1013 @ X1012)=>![X1011:mworld]:(((mrel @ X1012 @ X1011)=>![X1010:mworld]:(((mrel @ X1011 @ X1010)=>((v16 @ X1010)|![X1009:mworld]:(((mrel @ X1010 @ X1009)=>![X1008:mworld]:(((mrel @ X1009 @ X1008)=>![X1007:mworld]:(((mrel @ X1008 @ X1007)=>![X1006:mworld]:(((mrel @ X1007 @ X1006)=>![X1005:mworld]:(((mrel @ X1006 @ X1005)=>![X1004:mworld]:(((mrel @ X1005 @ X1004)=>![X1003:mworld]:(((mrel @ X1004 @ X1003)=>(~(v9 @ X1003)|![X1002:mworld]:(((mrel @ X1003 @ X1002)=>![X1001:mworld]:(((mrel @ X1002 @ X1001)=>![X1000:mworld]:(((mrel @ X1001 @ X1000)=>(~(v6 @ X1000)|![X999:mworld]:(((mrel @ X1000 @ X999)=>![X998:mworld]:(((mrel @ X999 @ X998)=>![X997:mworld]:(((mrel @ X998 @ X997)=>~(v3 @ X997)))))))))))))))))))))))))))))))))))))))))))))))), introduced(definition)).
% 0.54/0.46 thf(c_0_27, plain, ![X1997:mworld, X1998:mworld, X1999:mworld, X2000:mworld, X2001:mworld, X2002:mworld, X2003:mworld, X2004:mworld, X2005:mworld, X2006:mworld, X2007:mworld, X2008:mworld, X2009:mworld, X2010:mworld, X2011:mworld, X2012:mworld, X2013:mworld, X2014:mworld, X2015:mworld, X2016:mworld, X2017:mworld, X2018:mworld, X2019:mworld]:((~(epred14_1 @ X1997)|(~(mrel @ X1997 @ X1998)|(~(mrel @ X1998 @ X1999)|((v23 @ X1999)|(~(mrel @ X1999 @ X2000)|(~(mrel @ X2000 @ X2001)|(~(mrel @ X2001 @ X2002)|(~(mrel @ X2002 @ X2003)|(~(mrel @ X2003 @ X2004)|(~(mrel @ X2004 @ X2005)|(~(mrel @ X2005 @ X2006)|(~(mrel @ X2006 @ X2007)|(~(mrel @ X2007 @ X2008)|(~(mrel @ X2008 @ X2009)|(~(mrel @ X2009 @ X2010)|(~(mrel @ X2010 @ X2011)|(~(mrel @ X2011 @ X2012)|(~(mrel @ X2012 @ X2013)|(~(mrel @ X2013 @ X2014)|(~(mrel @ X2014 @ X2015)|(~(mrel @ X2015 @ X2016)|((v6 @ X2016)|(~(mrel @ X2016 @ X2017)|(~(mrel @ X2017 @ X2018)|(~(mrel @ X2018 @ X2019)|(v3 @ X2019))))))))))))))))))))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_22])])])])).
% 0.54/0.46 thf(c_0_28, plain, ![X1217:mworld, X1218:mworld]:((mrel @ X1217 @ X1218)), inference(variable_rename,[status(thm)],[mrel_universal])).
% 0.54/0.46 thf(c_0_29, plain, ![X1389:mworld, X1390:mworld, X1391:mworld, X1392:mworld]:((~(mrel @ mactual @ X1389)|(~(mrel @ X1389 @ X1390)|(~(mrel @ X1390 @ X1391)|(~(v26 @ X1391)|(~(mrel @ X1391 @ X1392)|(epred14_1 @ X1392))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_23])])])])).
% 0.54/0.46 thf(c_0_30, plain, ![X1294:mworld, X1295:mworld, X1296:mworld, X1297:mworld, X1298:mworld, X1299:mworld, X1300:mworld, X1301:mworld, X1302:mworld, X1303:mworld, X1304:mworld, X1305:mworld, X1306:mworld, X1307:mworld, X1308:mworld, X1309:mworld]:((~(mrel @ mactual @ X1294)|(~(v28 @ X1294)|(~(mrel @ X1294 @ X1295)|(~(mrel @ X1295 @ X1296)|((v26 @ X1296)|(~(mrel @ X1296 @ X1297)|(~(mrel @ X1297 @ X1298)|(~(mrel @ X1298 @ X1299)|(~(mrel @ X1299 @ X1300)|(~(mrel @ X1300 @ X1301)|(~(mrel @ X1301 @ X1302)|(~(mrel @ X1302 @ X1303)|(~(mrel @ X1303 @ X1304)|(~(mrel @ X1304 @ X1305)|(~(mrel @ X1305 @ X1306)|(~(v16 @ X1306)|(~(mrel @ X1306 @ X1307)|(~(mrel @ X1307 @ X1308)|(~(mrel @ X1308 @ X1309)|~(v13 @ X1309))))))))))))))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_24])])])])).
% 0.54/0.46 thf(c_0_31, plain, ![X1634:mworld, X1635:mworld, X1636:mworld, X1637:mworld, X1638:mworld, X1639:mworld, X1640:mworld, X1641:mworld, X1642:mworld, X1643:mworld, X1644:mworld, X1645:mworld, X1646:mworld, X1647:mworld, X1648:mworld, X1649:mworld, X1650:mworld, X1651:mworld, X1652:mworld, X1653:mworld, X1654:mworld, X1655:mworld, X1656:mworld, X1657:mworld, X1658:mworld, X1659:mworld, X1660:mworld]:(((((((((((((((((((((((((((((((mrel @ X1660 @ (esk1_27 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647 @ X1648 @ X1649 @ X1650 @ X1651 @ X1652 @ X1653 @ X1654 @ X1655 @ X1656 @ X1657 @ X1658 @ X1659 @ X1660))|~(mrel @ X1659 @ X1660)|~(mrel @ X1658 @ X1659)|~(mrel @ X1657 @ X1658)|~(mrel @ X1656 @ X1657)|~(mrel @ X1655 @ X1656)|~(mrel @ X1654 @ X1655)|~(mrel @ X1653 @ X1654)|~(mrel @ X1652 @ X1653)|~(mrel @ X1651 @ X1652)|~(mrel @ X1650 @ X1651)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&(($true)|~(mrel @ X1659 @ X1660)|~(mrel @ X1658 @ X1659)|~(mrel @ X1657 @ X1658)|~(mrel @ X1656 @ X1657)|~(mrel @ X1655 @ X1656)|~(mrel @ X1654 @ X1655)|~(mrel @ X1653 @ X1654)|~(mrel @ X1652 @ X1653)|~(mrel @ X1651 @ X1652)|~(mrel @ X1650 @ X1651)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634)))&(((mrel @ X1659 @ (esk2_26 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647 @ X1648 @ X1649 @ X1650 @ X1651 @ X1652 @ X1653 @ X1654 @ X1655 @ X1656 @ X1657 @ X1658 @ X1659))|~(mrel @ X1658 @ X1659)|~(mrel @ X1657 @ X1658)|~(mrel @ X1656 @ X1657)|~(mrel @ X1655 @ X1656)|~(mrel @ X1654 @ X1655)|~(mrel @ X1653 @ X1654)|~(mrel @ X1652 @ X1653)|~(mrel @ X1651 @ X1652)|~(mrel @ X1650 @ X1651)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&(($true)|~(mrel @ X1658 @ X1659)|~(mrel @ X1657 @ X1658)|~(mrel @ X1656 @ X1657)|~(mrel @ X1655 @ X1656)|~(mrel @ X1654 @ X1655)|~(mrel @ X1653 @ X1654)|~(mrel @ X1652 @ X1653)|~(mrel @ X1651 @ X1652)|~(mrel @ X1650 @ X1651)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))))&(((mrel @ X1658 @ (esk3_25 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647 @ X1648 @ X1649 @ X1650 @ X1651 @ X1652 @ X1653 @ X1654 @ X1655 @ X1656 @ X1657 @ X1658))|~(mrel @ X1657 @ X1658)|~(mrel @ X1656 @ X1657)|~(mrel @ X1655 @ X1656)|~(mrel @ X1654 @ X1655)|~(mrel @ X1653 @ X1654)|~(mrel @ X1652 @ X1653)|~(mrel @ X1651 @ X1652)|~(mrel @ X1650 @ X1651)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&(($true)|~(mrel @ X1657 @ X1658)|~(mrel @ X1656 @ X1657)|~(mrel @ X1655 @ X1656)|~(mrel @ X1654 @ X1655)|~(mrel @ X1653 @ X1654)|~(mrel @ X1652 @ X1653)|~(mrel @ X1651 @ X1652)|~(mrel @ X1650 @ X1651)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))))&(((mrel @ X1657 @ (esk4_24 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647 @ X1648 @ X1649 @ X1650 @ X1651 @ X1652 @ X1653 @ X1654 @ X1655 @ X1656 @ X1657))|~(mrel @ X1656 @ X1657)|~(mrel @ X1655 @ X1656)|~(mrel @ X1654 @ X1655)|~(mrel @ X1653 @ X1654)|~(mrel @ X1652 @ X1653)|~(mrel @ X1651 @ X1652)|~(mrel @ X1650 @ X1651)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&(($true)|~(mrel @ X1656 @ X1657)|~(mrel @ X1655 @ X1656)|~(mrel @ X1654 @ X1655)|~(mrel @ X1653 @ X1654)|~(mrel @ X1652 @ X1653)|~(mrel @ X1651 @ X1652)|~(mrel @ X1650 @ X1651)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))))&((((mrel @ X1656 @ (esk5_23 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647 @ X1648 @ X1649 @ X1650 @ X1651 @ X1652 @ X1653 @ X1654 @ X1655 @ X1656))|~(mrel @ X1655 @ X1656)|~(mrel @ X1654 @ X1655)|~(mrel @ X1653 @ X1654)|~(mrel @ X1652 @ X1653)|~(mrel @ X1651 @ X1652)|~(mrel @ X1650 @ X1651)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&((v5 @ (esk5_23 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647 @ X1648 @ X1649 @ X1650 @ X1651 @ X1652 @ X1653 @ X1654 @ X1655 @ X1656))|~(mrel @ X1655 @ X1656)|~(mrel @ X1654 @ X1655)|~(mrel @ X1653 @ X1654)|~(mrel @ X1652 @ X1653)|~(mrel @ X1651 @ X1652)|~(mrel @ X1650 @ X1651)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634)))&(((mrel @ X1656 @ (esk6_23 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647 @ X1648 @ X1649 @ X1650 @ X1651 @ X1652 @ X1653 @ X1654 @ X1655 @ X1656))|~(mrel @ X1655 @ X1656)|~(mrel @ X1654 @ X1655)|~(mrel @ X1653 @ X1654)|~(mrel @ X1652 @ X1653)|~(mrel @ X1651 @ X1652)|~(mrel @ X1650 @ X1651)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&(~(v5 @ (esk6_23 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647 @ X1648 @ X1649 @ X1650 @ X1651 @ X1652 @ X1653 @ X1654 @ X1655 @ X1656))|~(mrel @ X1655 @ X1656)|~(mrel @ X1654 @ X1655)|~(mrel @ X1653 @ X1654)|~(mrel @ X1652 @ X1653)|~(mrel @ X1651 @ X1652)|~(mrel @ X1650 @ X1651)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634)))))&((((mrel @ X1655 @ (esk7_22 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647 @ X1648 @ X1649 @ X1650 @ X1651 @ X1652 @ X1653 @ X1654 @ X1655))|~(mrel @ X1654 @ X1655)|~(mrel @ X1653 @ X1654)|~(mrel @ X1652 @ X1653)|~(mrel @ X1651 @ X1652)|~(mrel @ X1650 @ X1651)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&((v6 @ (esk7_22 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647 @ X1648 @ X1649 @ X1650 @ X1651 @ X1652 @ X1653 @ X1654 @ X1655))|~(mrel @ X1654 @ X1655)|~(mrel @ X1653 @ X1654)|~(mrel @ X1652 @ X1653)|~(mrel @ X1651 @ X1652)|~(mrel @ X1650 @ X1651)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634)))&(((mrel @ X1655 @ (esk8_22 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647 @ X1648 @ X1649 @ X1650 @ X1651 @ X1652 @ X1653 @ X1654 @ X1655))|~(mrel @ X1654 @ X1655)|~(mrel @ X1653 @ X1654)|~(mrel @ X1652 @ X1653)|~(mrel @ X1651 @ X1652)|~(mrel @ X1650 @ X1651)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&(~(v6 @ (esk8_22 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647 @ X1648 @ X1649 @ X1650 @ X1651 @ X1652 @ X1653 @ X1654 @ X1655))|~(mrel @ X1654 @ X1655)|~(mrel @ X1653 @ X1654)|~(mrel @ X1652 @ X1653)|~(mrel @ X1651 @ X1652)|~(mrel @ X1650 @ X1651)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634)))))&((((mrel @ X1654 @ (esk9_21 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647 @ X1648 @ X1649 @ X1650 @ X1651 @ X1652 @ X1653 @ X1654))|~(mrel @ X1653 @ X1654)|~(mrel @ X1652 @ X1653)|~(mrel @ X1651 @ X1652)|~(mrel @ X1650 @ X1651)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&((v7 @ (esk9_21 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647 @ X1648 @ X1649 @ X1650 @ X1651 @ X1652 @ X1653 @ X1654))|~(mrel @ X1653 @ X1654)|~(mrel @ X1652 @ X1653)|~(mrel @ X1651 @ X1652)|~(mrel @ X1650 @ X1651)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634)))&(((mrel @ X1654 @ (esk10_21 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647 @ X1648 @ X1649 @ X1650 @ X1651 @ X1652 @ X1653 @ X1654))|~(mrel @ X1653 @ X1654)|~(mrel @ X1652 @ X1653)|~(mrel @ X1651 @ X1652)|~(mrel @ X1650 @ X1651)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&(~(v7 @ (esk10_21 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647 @ X1648 @ X1649 @ X1650 @ X1651 @ X1652 @ X1653 @ X1654))|~(mrel @ X1653 @ X1654)|~(mrel @ X1652 @ X1653)|~(mrel @ X1651 @ X1652)|~(mrel @ X1650 @ X1651)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634)))))&((((mrel @ X1653 @ (esk11_20 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647 @ X1648 @ X1649 @ X1650 @ X1651 @ X1652 @ X1653))|~(mrel @ X1652 @ X1653)|~(mrel @ X1651 @ X1652)|~(mrel @ X1650 @ X1651)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&((v8 @ (esk11_20 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647 @ X1648 @ X1649 @ X1650 @ X1651 @ X1652 @ X1653))|~(mrel @ X1652 @ X1653)|~(mrel @ X1651 @ X1652)|~(mrel @ X1650 @ X1651)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634)))&(((mrel @ X1653 @ (esk12_20 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647 @ X1648 @ X1649 @ X1650 @ X1651 @ X1652 @ X1653))|~(mrel @ X1652 @ X1653)|~(mrel @ X1651 @ X1652)|~(mrel @ X1650 @ X1651)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&(~(v8 @ (esk12_20 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647 @ X1648 @ X1649 @ X1650 @ X1651 @ X1652 @ X1653))|~(mrel @ X1652 @ X1653)|~(mrel @ X1651 @ X1652)|~(mrel @ X1650 @ X1651)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634)))))&(((mrel @ X1652 @ (esk13_19 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647 @ X1648 @ X1649 @ X1650 @ X1651 @ X1652))|~(mrel @ X1651 @ X1652)|~(mrel @ X1650 @ X1651)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&(($true)|~(mrel @ X1651 @ X1652)|~(mrel @ X1650 @ X1651)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))))&(((mrel @ X1651 @ (esk14_18 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647 @ X1648 @ X1649 @ X1650 @ X1651))|~(mrel @ X1650 @ X1651)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&(($true)|~(mrel @ X1650 @ X1651)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))))&(((mrel @ X1650 @ (esk15_17 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647 @ X1648 @ X1649 @ X1650))|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&(($true)|~(mrel @ X1649 @ X1650)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))))&(((mrel @ X1649 @ (esk16_16 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647 @ X1648 @ X1649))|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&(($true)|~(mrel @ X1648 @ X1649)|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))))&((((mrel @ X1648 @ (esk17_15 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647 @ X1648))|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&((v13 @ (esk17_15 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647 @ X1648))|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634)))&(((mrel @ X1648 @ (esk18_15 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647 @ X1648))|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&(~(v13 @ (esk18_15 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647 @ X1648))|~(mrel @ X1647 @ X1648)|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634)))))&((((mrel @ X1647 @ (esk19_14 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647))|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&((v14 @ (esk19_14 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647))|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634)))&(((mrel @ X1647 @ (esk20_14 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647))|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&(~(v14 @ (esk20_14 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646 @ X1647))|~(mrel @ X1646 @ X1647)|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634)))))&((((mrel @ X1646 @ (esk21_13 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646))|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&((v15 @ (esk21_13 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646))|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634)))&(((mrel @ X1646 @ (esk22_13 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646))|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&(~(v15 @ (esk22_13 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645 @ X1646))|~(mrel @ X1645 @ X1646)|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634)))))&((((mrel @ X1645 @ (esk23_12 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645))|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&((v16 @ (esk23_12 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645))|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634)))&(((mrel @ X1645 @ (esk24_12 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645))|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&(~(v16 @ (esk24_12 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644 @ X1645))|~(mrel @ X1644 @ X1645)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634)))))&(((mrel @ X1644 @ (esk25_11 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643 @ X1644))|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&(($true)|~(mrel @ X1643 @ X1644)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))))&(((mrel @ X1643 @ (esk26_10 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642 @ X1643))|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&(($true)|~(mrel @ X1642 @ X1643)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))))&(((mrel @ X1642 @ (esk27_9 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641 @ X1642))|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&(($true)|~(mrel @ X1641 @ X1642)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))))&(((mrel @ X1641 @ (esk28_8 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640 @ X1641))|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&(($true)|~(mrel @ X1640 @ X1641)|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))))&((((mrel @ X1640 @ (esk29_7 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640))|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&((v21 @ (esk29_7 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640))|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634)))&(((mrel @ X1640 @ (esk30_7 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640))|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&(~(v21 @ (esk30_7 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639 @ X1640))|~(mrel @ X1639 @ X1640)|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634)))))&((((mrel @ X1639 @ (esk31_6 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639))|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&((v22 @ (esk31_6 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639))|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634)))&(((mrel @ X1639 @ (esk32_6 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639))|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&(~(v22 @ (esk32_6 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638 @ X1639))|~(mrel @ X1638 @ X1639)|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634)))))&((((mrel @ X1638 @ (esk33_5 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638))|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&((v23 @ (esk33_5 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638))|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634)))&(((mrel @ X1638 @ (esk34_5 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638))|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&(~(v23 @ (esk34_5 @ X1634 @ X1635 @ X1636 @ X1637 @ X1638))|~(mrel @ X1637 @ X1638)|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634)))))&((((mrel @ X1637 @ (esk35_4 @ X1634 @ X1635 @ X1636 @ X1637))|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&((v24 @ (esk35_4 @ X1634 @ X1635 @ X1636 @ X1637))|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634)))&(((mrel @ X1637 @ (esk36_4 @ X1634 @ X1635 @ X1636 @ X1637))|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&(~(v24 @ (esk36_4 @ X1634 @ X1635 @ X1636 @ X1637))|~(mrel @ X1636 @ X1637)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634)))))&(((mrel @ X1636 @ (esk37_3 @ X1634 @ X1635 @ X1636))|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&(($true)|~(mrel @ X1635 @ X1636)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))))&(((mrel @ X1635 @ (esk38_2 @ X1634 @ X1635))|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))&(($true)|~(mrel @ X1634 @ X1635)|~(mrel @ mactual @ X1634))))&(((mrel @ X1634 @ (esk39_1 @ X1634))|~(mrel @ mactual @ X1634))&(($true)|~(mrel @ mactual @ X1634))))&((mrel @ mactual @ esk40_0)&($true)))), 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_25])])])])])])])).
% 0.54/0.46 thf(c_0_32, plain, ![X1022:mworld]:(((mrel @ mactual @ X1022)=>![X1021:mworld]:(((mrel @ X1022 @ X1021)=>![X1020:mworld]:(((mrel @ X1021 @ X1020)=>![X1019:mworld]:(((mrel @ X1020 @ X1019)=>![X1018:mworld]:(((mrel @ X1019 @ X1018)=>(epred30_1 @ X1018))))))))))), inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[mod45, c_0_16]), c_0_17]), c_0_18]), c_0_19])]), c_0_26])).
% 0.54/0.46 thf(c_0_33, plain, ![X43:mworld]:(((mrel @ mactual @ X43)=>((v28 @ X43)|![X42:mworld]:(((mrel @ X43 @ X42)=>![X41:mworld]:(((mrel @ X42 @ X41)=>((v26 @ X41)|![X40:mworld]:(((mrel @ X41 @ X40)=>![X39:mworld]:(((mrel @ X40 @ X39)=>![X38:mworld]:(((mrel @ X39 @ X38)=>![X37:mworld]:(((mrel @ X38 @ X37)=>![X36:mworld]:(((mrel @ X37 @ X36)=>(~(v21 @ X36)|![X35:mworld]:(((mrel @ X36 @ X35)=>![X34:mworld]:(((mrel @ X35 @ X34)=>![X33:mworld]:(((mrel @ X34 @ X33)=>![X32:mworld]:(((mrel @ X33 @ X32)=>![X31:mworld]:(((mrel @ X32 @ X31)=>![X30:mworld]:(((mrel @ X31 @ X30)=>![X29:mworld]:(((mrel @ X30 @ X29)=>(v14 @ X29)))))))))))))))))))))))))))))))))), inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[mod2, c_0_16]), c_0_17]), c_0_18]), c_0_19])])).
% 0.54/0.46 thf(c_0_34, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld, X10:mworld, X11:mworld, X12:mworld, X13:mworld, X14:mworld, X15:mworld, X16:mworld, X17:mworld, X18:mworld, X19:mworld, X20:mworld, X21:mworld, X22:mworld, X23:mworld, X24:mworld, X25:mworld, X26:mworld]:(((v23 @ X6)|(v6 @ X23)|(v3 @ X26)|~((epred14_1 @ X3))|~((mrel @ X3 @ X5))|~((mrel @ X5 @ X6))|~((mrel @ X6 @ X7))|~((mrel @ X7 @ X8))|~((mrel @ X8 @ X9))|~((mrel @ X9 @ X10))|~((mrel @ X10 @ X11))|~((mrel @ X11 @ X12))|~((mrel @ X12 @ X13))|~((mrel @ X13 @ X14))|~((mrel @ X14 @ X15))|~((mrel @ X15 @ X16))|~((mrel @ X16 @ X17))|~((mrel @ X17 @ X18))|~((mrel @ X18 @ X19))|~((mrel @ X19 @ X20))|~((mrel @ X20 @ X21))|~((mrel @ X21 @ X22))|~((mrel @ X22 @ X23))|~((mrel @ X23 @ X24))|~((mrel @ X24 @ X25))|~((mrel @ X25 @ X26)))), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.54/0.46 thf(c_0_35, plain, ![X3:mworld, X5:mworld]:((mrel @ X3 @ X5)), inference(split_conjunct,[status(thm)],[c_0_28])).
% 0.54/0.46 thf(c_0_36, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((epred14_1 @ X7)|~((mrel @ mactual @ X3))|~((mrel @ X3 @ X5))|~((mrel @ X5 @ X6))|~((v26 @ X6))|~((mrel @ X6 @ X7)))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 0.54/0.46 thf(c_0_37, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld, X10:mworld, X11:mworld, X12:mworld, X13:mworld, X14:mworld, X15:mworld, X16:mworld, X17:mworld, X18:mworld, X19:mworld]:(((v26 @ X6)|~((mrel @ mactual @ X3))|~((v28 @ X3))|~((mrel @ X3 @ X5))|~((mrel @ X5 @ X6))|~((mrel @ X6 @ X7))|~((mrel @ X7 @ X8))|~((mrel @ X8 @ X9))|~((mrel @ X9 @ X10))|~((mrel @ X10 @ X11))|~((mrel @ X11 @ X12))|~((mrel @ X12 @ X13))|~((mrel @ X13 @ X14))|~((mrel @ X14 @ X15))|~((mrel @ X15 @ X16))|~((v16 @ X16))|~((mrel @ X16 @ X17))|~((mrel @ X17 @ X18))|~((mrel @ X18 @ X19))|~((v13 @ X19)))), inference(split_conjunct,[status(thm)],[c_0_30])).
% 0.54/0.46 thf(c_0_38, plain, ![X15:mworld, X14:mworld, X13:mworld, X12:mworld, X11:mworld, X10:mworld, X9:mworld, X8:mworld, X7:mworld, X6:mworld, X5:mworld, X3:mworld]:(((v16 @ (esk23_12 @ X3 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15))|~((mrel @ X14 @ X15))|~((mrel @ X13 @ X14))|~((mrel @ X12 @ X13))|~((mrel @ X11 @ X12))|~((mrel @ X10 @ X11))|~((mrel @ X9 @ X10))|~((mrel @ X8 @ X9))|~((mrel @ X7 @ X8))|~((mrel @ X6 @ X7))|~((mrel @ X5 @ X6))|~((mrel @ X3 @ X5))|~((mrel @ mactual @ X3)))), inference(split_conjunct,[status(thm)],[c_0_31])).
% 0.54/0.46 thf(c_0_39, plain, ![X1018:mworld]:(((epred30_1 @ X1018)=>![X1017:mworld]:(((mrel @ X1018 @ X1017)=>![X1016:mworld]:(((mrel @ X1017 @ X1016)=>![X1015:mworld]:(((mrel @ X1016 @ X1015)=>![X1014:mworld]:(((mrel @ X1015 @ X1014)=>![X1013:mworld]:(((mrel @ X1014 @ X1013)=>![X1012:mworld]:(((mrel @ X1013 @ X1012)=>![X1011:mworld]:(((mrel @ X1012 @ X1011)=>![X1010:mworld]:(((mrel @ X1011 @ X1010)=>((v16 @ X1010)|![X1009:mworld]:(((mrel @ X1010 @ X1009)=>![X1008:mworld]:(((mrel @ X1009 @ X1008)=>![X1007:mworld]:(((mrel @ X1008 @ X1007)=>![X1006:mworld]:(((mrel @ X1007 @ X1006)=>![X1005:mworld]:(((mrel @ X1006 @ X1005)=>![X1004:mworld]:(((mrel @ X1005 @ X1004)=>![X1003:mworld]:(((mrel @ X1004 @ X1003)=>(~(v9 @ X1003)|![X1002:mworld]:(((mrel @ X1003 @ X1002)=>![X1001:mworld]:(((mrel @ X1002 @ X1001)=>![X1000:mworld]:(((mrel @ X1001 @ X1000)=>(~(v6 @ X1000)|![X999:mworld]:(((mrel @ X1000 @ X999)=>![X998:mworld]:(((mrel @ X999 @ X998)=>![X997:mworld]:(((mrel @ X998 @ X997)=>~(v3 @ X997)))))))))))))))))))))))))))))))))))))))))))))))), inference(split_equiv,[status(thm)],[c_0_26])).
% 0.54/0.46 thf(c_0_40, plain, ![X1586:mworld, X1587:mworld, X1588:mworld, X1589:mworld, X1590:mworld]:((~(mrel @ mactual @ X1586)|(~(mrel @ X1586 @ X1587)|(~(mrel @ X1587 @ X1588)|(~(mrel @ X1588 @ X1589)|(~(mrel @ X1589 @ X1590)|(epred30_1 @ X1590))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_32])])])])).
% 0.54/0.46 thf(c_0_41, plain, ![X1240:mworld, X1241:mworld, X1242:mworld, X1243:mworld, X1244:mworld, X1245:mworld, X1246:mworld, X1247:mworld, X1248:mworld, X1249:mworld, X1250:mworld, X1251:mworld, X1252:mworld, X1253:mworld, X1254:mworld]:((~(mrel @ mactual @ X1240)|((v28 @ X1240)|(~(mrel @ X1240 @ X1241)|(~(mrel @ X1241 @ X1242)|((v26 @ X1242)|(~(mrel @ X1242 @ X1243)|(~(mrel @ X1243 @ X1244)|(~(mrel @ X1244 @ X1245)|(~(mrel @ X1245 @ X1246)|(~(mrel @ X1246 @ X1247)|(~(v21 @ X1247)|(~(mrel @ X1247 @ X1248)|(~(mrel @ X1248 @ X1249)|(~(mrel @ X1249 @ X1250)|(~(mrel @ X1250 @ X1251)|(~(mrel @ X1251 @ X1252)|(~(mrel @ X1252 @ X1253)|(~(mrel @ X1253 @ X1254)|(v14 @ X1254)))))))))))))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_33])])])])).
% 0.54/0.46 thf(c_0_42, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v23 @ X3)|(v6 @ X5)|(v3 @ X6)|~((epred14_1 @ X7)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_34, c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35])])).
% 0.54/0.46 thf(c_0_43, plain, ![X3:mworld, X5:mworld]:(((epred14_1 @ X3)|~((v26 @ X5)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_36, c_0_35]), c_0_35]), c_0_35]), c_0_35])])).
% 0.54/0.46 thf(c_0_44, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v26 @ X3)|~((v13 @ X5))|~((v16 @ X6))|~((v28 @ X7)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_37, c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35])])).
% 0.54/0.46 thf(c_0_45, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld, X10:mworld, X11:mworld, X12:mworld, X13:mworld, X14:mworld, X15:mworld]:((v16 @ (esk23_12 @ X3 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_38, c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35])])).
% 0.54/0.46 thf(c_0_46, plain, ![X2352:mworld, X2353:mworld, X2354:mworld, X2355:mworld, X2356:mworld, X2357:mworld, X2358:mworld, X2359:mworld, X2360:mworld, X2361:mworld, X2362:mworld, X2363:mworld, X2364:mworld, X2365:mworld, X2366:mworld, X2367:mworld, X2368:mworld, X2369:mworld, X2370:mworld, X2371:mworld, X2372:mworld, X2373:mworld]:((~(epred30_1 @ X2352)|(~(mrel @ X2352 @ X2353)|(~(mrel @ X2353 @ X2354)|(~(mrel @ X2354 @ X2355)|(~(mrel @ X2355 @ X2356)|(~(mrel @ X2356 @ X2357)|(~(mrel @ X2357 @ X2358)|(~(mrel @ X2358 @ X2359)|(~(mrel @ X2359 @ X2360)|((v16 @ X2360)|(~(mrel @ X2360 @ X2361)|(~(mrel @ X2361 @ X2362)|(~(mrel @ X2362 @ X2363)|(~(mrel @ X2363 @ X2364)|(~(mrel @ X2364 @ X2365)|(~(mrel @ X2365 @ X2366)|(~(mrel @ X2366 @ X2367)|(~(v9 @ X2367)|(~(mrel @ X2367 @ X2368)|(~(mrel @ X2368 @ X2369)|(~(mrel @ X2369 @ X2370)|(~(v6 @ X2370)|(~(mrel @ X2370 @ X2371)|(~(mrel @ X2371 @ X2372)|(~(mrel @ X2372 @ X2373)|~(v3 @ X2373))))))))))))))))))))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_39])])])])).
% 0.54/0.46 thf(c_0_47, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld]:(((epred30_1 @ X8)|~((mrel @ mactual @ X3))|~((mrel @ X3 @ X5))|~((mrel @ X5 @ X6))|~((mrel @ X6 @ X7))|~((mrel @ X7 @ X8)))), inference(split_conjunct,[status(thm)],[c_0_40])).
% 0.54/0.46 thf(c_0_48, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld, X10:mworld, X11:mworld, X12:mworld, X13:mworld, X14:mworld, X15:mworld, X16:mworld, X17:mworld, X18:mworld]:(((v28 @ X3)|(v26 @ X6)|(v14 @ X18)|~((mrel @ mactual @ X3))|~((mrel @ X3 @ X5))|~((mrel @ X5 @ X6))|~((mrel @ X6 @ X7))|~((mrel @ X7 @ X8))|~((mrel @ X8 @ X9))|~((mrel @ X9 @ X10))|~((mrel @ X10 @ X11))|~((v21 @ X11))|~((mrel @ X11 @ X12))|~((mrel @ X12 @ X13))|~((mrel @ X13 @ X14))|~((mrel @ X14 @ X15))|~((mrel @ X15 @ X16))|~((mrel @ X16 @ X17))|~((mrel @ X17 @ X18)))), inference(split_conjunct,[status(thm)],[c_0_41])).
% 0.54/0.46 thf(c_0_49, plain, ![X10:mworld, X9:mworld, X8:mworld, X7:mworld, X6:mworld, X5:mworld, X3:mworld]:(((v21 @ (esk29_7 @ X3 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10))|~((mrel @ X9 @ X10))|~((mrel @ X8 @ X9))|~((mrel @ X7 @ X8))|~((mrel @ X6 @ X7))|~((mrel @ X5 @ X6))|~((mrel @ X3 @ X5))|~((mrel @ mactual @ X3)))), inference(split_conjunct,[status(thm)],[c_0_31])).
% 0.54/0.46 thf(c_0_50, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v23 @ X3)|(v6 @ X5)|(v3 @ X6)|~((v26 @ X7)))), inference(spm,[status(thm)],[c_0_42, c_0_43])).
% 0.54/0.46 thf(c_0_51, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((v26 @ X3)|~((v13 @ X5))|~((v28 @ X6)))), inference(spm,[status(thm)],[c_0_44, c_0_45])).
% 0.54/0.46 thf(c_0_52, plain, ![X18:mworld, X17:mworld, X16:mworld, X15:mworld, X14:mworld, X13:mworld, X12:mworld, X11:mworld, X10:mworld, X9:mworld, X8:mworld, X7:mworld, X6:mworld, X5:mworld, X3:mworld]:(((v13 @ (esk17_15 @ X3 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18))|~((mrel @ X17 @ X18))|~((mrel @ X16 @ X17))|~((mrel @ X15 @ X16))|~((mrel @ X14 @ X15))|~((mrel @ X13 @ X14))|~((mrel @ X12 @ X13))|~((mrel @ X11 @ X12))|~((mrel @ X10 @ X11))|~((mrel @ X9 @ X10))|~((mrel @ X8 @ X9))|~((mrel @ X7 @ X8))|~((mrel @ X6 @ X7))|~((mrel @ X5 @ X6))|~((mrel @ X3 @ X5))|~((mrel @ mactual @ X3)))), inference(split_conjunct,[status(thm)],[c_0_31])).
% 0.54/0.46 thf(c_0_53, plain, ![X15:mworld, X14:mworld, X13:mworld, X12:mworld, X11:mworld, X10:mworld, X9:mworld, X8:mworld, X7:mworld, X6:mworld, X5:mworld, X3:mworld]:((~((v16 @ (esk24_12 @ X3 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15)))|~((mrel @ X14 @ X15))|~((mrel @ X13 @ X14))|~((mrel @ X12 @ X13))|~((mrel @ X11 @ X12))|~((mrel @ X10 @ X11))|~((mrel @ X9 @ X10))|~((mrel @ X8 @ X9))|~((mrel @ X7 @ X8))|~((mrel @ X6 @ X7))|~((mrel @ X5 @ X6))|~((mrel @ X3 @ X5))|~((mrel @ mactual @ X3)))), inference(split_conjunct,[status(thm)],[c_0_31])).
% 0.54/0.46 thf(c_0_54, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld, X10:mworld, X11:mworld, X12:mworld, X13:mworld, X14:mworld, X15:mworld, X16:mworld, X17:mworld, X18:mworld, X19:mworld, X20:mworld, X21:mworld, X22:mworld, X23:mworld, X24:mworld, X25:mworld]:(((v16 @ X12)|~((epred30_1 @ X3))|~((mrel @ X3 @ X5))|~((mrel @ X5 @ X6))|~((mrel @ X6 @ X7))|~((mrel @ X7 @ X8))|~((mrel @ X8 @ X9))|~((mrel @ X9 @ X10))|~((mrel @ X10 @ X11))|~((mrel @ X11 @ X12))|~((mrel @ X12 @ X13))|~((mrel @ X13 @ X14))|~((mrel @ X14 @ X15))|~((mrel @ X15 @ X16))|~((mrel @ X16 @ X17))|~((mrel @ X17 @ X18))|~((mrel @ X18 @ X19))|~((v9 @ X19))|~((mrel @ X19 @ X20))|~((mrel @ X20 @ X21))|~((mrel @ X21 @ X22))|~((v6 @ X22))|~((mrel @ X22 @ X23))|~((mrel @ X23 @ X24))|~((mrel @ X24 @ X25))|~((v3 @ X25)))), inference(split_conjunct,[status(thm)],[c_0_46])).
% 0.54/0.46 thf(c_0_55, plain, ![X3:mworld]:((epred30_1 @ X3)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_47, c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35])])).
% 0.54/0.46 thf(c_0_56, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v28 @ X3)|(v26 @ X5)|(v14 @ X6)|~((v21 @ X7)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_48, c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35])])).
% 0.54/0.46 thf(c_0_57, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld, X10:mworld]:((v21 @ (esk29_7 @ X3 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_49, c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35])])).
% 0.54/0.46 thf(c_0_58, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld]:(((v3 @ X3)|(v6 @ X5)|(v23 @ X6)|~((v13 @ X7))|~((v28 @ X8)))), inference(spm,[status(thm)],[c_0_50, c_0_51])).
% 0.54/0.46 thf(c_0_59, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld, X10:mworld, X11:mworld, X12:mworld, X13:mworld, X14:mworld, X15:mworld, X16:mworld, X17:mworld, X18:mworld]:((v13 @ (esk17_15 @ X3 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_52, c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35])])).
% 0.54/0.46 thf(c_0_60, plain, ![X80:mworld]:(((mrel @ mactual @ X80)=>((v28 @ X80)|![X79:mworld]:(((mrel @ X80 @ X79)=>![X78:mworld]:(((mrel @ X79 @ X78)=>![X77:mworld]:(((mrel @ X78 @ X77)=>![X76:mworld]:(((mrel @ X77 @ X76)=>![X75:mworld]:(((mrel @ X76 @ X75)=>![X74:mworld]:(((mrel @ X75 @ X74)=>![X73:mworld]:(((mrel @ X74 @ X73)=>![X72:mworld]:(((mrel @ X73 @ X72)=>![X71:mworld]:(((mrel @ X72 @ X71)=>![X70:mworld]:(((mrel @ X71 @ X70)=>![X69:mworld]:(((mrel @ X70 @ X69)=>![X68:mworld]:(((mrel @ X69 @ X68)=>![X67:mworld]:(((mrel @ X68 @ X67)=>(~(v15 @ X67)|![X66:mworld]:(((mrel @ X67 @ X66)=>((v14 @ X66)|![X65:mworld]:(((mrel @ X66 @ X65)=>![X64:mworld]:(((mrel @ X65 @ X64)=>![X63:mworld]:(((mrel @ X64 @ X63)=>![X62:mworld]:(((mrel @ X63 @ X62)=>![X61:mworld]:(((mrel @ X62 @ X61)=>(v9 @ X61)))))))))))))))))))))))))))))))))))))))))))), inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[mod4, c_0_16]), c_0_17]), c_0_18]), c_0_19])])).
% 0.54/0.46 thf(c_0_61, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld, X10:mworld, X11:mworld, X12:mworld, X13:mworld, X14:mworld, X15:mworld]:(~((v16 @ (esk24_12 @ X3 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_53, c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35])])).
% 0.54/0.46 thf(c_0_62, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v16 @ X3)|~((v3 @ X5))|~((v6 @ X6))|~((v9 @ X7)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_54, c_0_55]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35])])).
% 0.54/0.46 thf(c_0_63, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((v28 @ X3)|(v26 @ X5)|(v14 @ X6))), inference(spm,[status(thm)],[c_0_56, c_0_57])).
% 0.54/0.46 thf(c_0_64, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v23 @ X3)|(v6 @ X5)|(v3 @ X6)|~((v28 @ X7)))), inference(spm,[status(thm)],[c_0_58, c_0_59])).
% 0.54/0.46 thf(c_0_65, plain, ![X1272:mworld, X1273:mworld, X1274:mworld, X1275:mworld, X1276:mworld, X1277:mworld, X1278:mworld, X1279:mworld, X1280:mworld, X1281:mworld, X1282:mworld, X1283:mworld, X1284:mworld, X1285:mworld, X1286:mworld, X1287:mworld, X1288:mworld, X1289:mworld, X1290:mworld, X1291:mworld]:((~(mrel @ mactual @ X1272)|((v28 @ X1272)|(~(mrel @ X1272 @ X1273)|(~(mrel @ X1273 @ X1274)|(~(mrel @ X1274 @ X1275)|(~(mrel @ X1275 @ X1276)|(~(mrel @ X1276 @ X1277)|(~(mrel @ X1277 @ X1278)|(~(mrel @ X1278 @ X1279)|(~(mrel @ X1279 @ X1280)|(~(mrel @ X1280 @ X1281)|(~(mrel @ X1281 @ X1282)|(~(mrel @ X1282 @ X1283)|(~(mrel @ X1283 @ X1284)|(~(mrel @ X1284 @ X1285)|(~(v15 @ X1285)|(~(mrel @ X1285 @ X1286)|((v14 @ X1286)|(~(mrel @ X1286 @ X1287)|(~(mrel @ X1287 @ X1288)|(~(mrel @ X1288 @ X1289)|(~(mrel @ X1289 @ X1290)|(~(mrel @ X1290 @ X1291)|(v9 @ X1291))))))))))))))))))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_60])])])])).
% 0.54/0.46 thf(c_0_66, plain, ![X3:mworld, X5:mworld, X6:mworld]:((~((v3 @ X3))|~((v6 @ X5))|~((v9 @ X6)))), inference(spm,[status(thm)],[c_0_61, c_0_62])).
% 0.54/0.46 thf(c_0_67, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v14 @ X3)|(v3 @ X5)|(v6 @ X6)|(v23 @ X7))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_63]), c_0_64])).
% 0.54/0.46 thf(c_0_68, plain, ![X25:mworld, X24:mworld, X23:mworld, X22:mworld, X21:mworld, X20:mworld, X19:mworld, X18:mworld, X17:mworld, X16:mworld, X15:mworld, X14:mworld, X13:mworld, X12:mworld, X11:mworld, X10:mworld, X9:mworld, X8:mworld, X7:mworld, X6:mworld, X5:mworld, X3:mworld]:(((v6 @ (esk7_22 @ X3 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 @ X21 @ X22 @ X23 @ X24 @ X25))|~((mrel @ X24 @ X25))|~((mrel @ X23 @ X24))|~((mrel @ X22 @ X23))|~((mrel @ X21 @ X22))|~((mrel @ X20 @ X21))|~((mrel @ X19 @ X20))|~((mrel @ X18 @ X19))|~((mrel @ X17 @ X18))|~((mrel @ X16 @ X17))|~((mrel @ X15 @ X16))|~((mrel @ X14 @ X15))|~((mrel @ X13 @ X14))|~((mrel @ X12 @ X13))|~((mrel @ X11 @ X12))|~((mrel @ X10 @ X11))|~((mrel @ X9 @ X10))|~((mrel @ X8 @ X9))|~((mrel @ X7 @ X8))|~((mrel @ X6 @ X7))|~((mrel @ X5 @ X6))|~((mrel @ X3 @ X5))|~((mrel @ mactual @ X3)))), inference(split_conjunct,[status(thm)],[c_0_31])).
% 0.54/0.46 thf(c_0_69, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld, X10:mworld, X11:mworld, X12:mworld, X13:mworld, X14:mworld, X15:mworld, X16:mworld, X17:mworld, X18:mworld, X19:mworld, X20:mworld, X21:mworld, X22:mworld, X23:mworld]:(((v28 @ X3)|(v14 @ X18)|(v9 @ X23)|~((mrel @ mactual @ X3))|~((mrel @ X3 @ X5))|~((mrel @ X5 @ X6))|~((mrel @ X6 @ X7))|~((mrel @ X7 @ X8))|~((mrel @ X8 @ X9))|~((mrel @ X9 @ X10))|~((mrel @ X10 @ X11))|~((mrel @ X11 @ X12))|~((mrel @ X12 @ X13))|~((mrel @ X13 @ X14))|~((mrel @ X14 @ X15))|~((mrel @ X15 @ X16))|~((mrel @ X16 @ X17))|~((v15 @ X17))|~((mrel @ X17 @ X18))|~((mrel @ X18 @ X19))|~((mrel @ X19 @ X20))|~((mrel @ X20 @ X21))|~((mrel @ X21 @ X22))|~((mrel @ X22 @ X23)))), inference(split_conjunct,[status(thm)],[c_0_65])).
% 0.54/0.46 thf(c_0_70, plain, ![X16:mworld, X15:mworld, X14:mworld, X13:mworld, X12:mworld, X11:mworld, X10:mworld, X9:mworld, X8:mworld, X7:mworld, X6:mworld, X5:mworld, X3:mworld]:(((v15 @ (esk21_13 @ X3 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16))|~((mrel @ X15 @ X16))|~((mrel @ X14 @ X15))|~((mrel @ X13 @ X14))|~((mrel @ X12 @ X13))|~((mrel @ X11 @ X12))|~((mrel @ X10 @ X11))|~((mrel @ X9 @ X10))|~((mrel @ X8 @ X9))|~((mrel @ X7 @ X8))|~((mrel @ X6 @ X7))|~((mrel @ X5 @ X6))|~((mrel @ X3 @ X5))|~((mrel @ mactual @ X3)))), inference(split_conjunct,[status(thm)],[c_0_31])).
% 0.54/0.46 thf(c_0_71, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld]:(((v23 @ X3)|(v6 @ X5)|(v14 @ X6)|~((v6 @ X7))|~((v9 @ X8)))), inference(spm,[status(thm)],[c_0_66, c_0_67])).
% 0.54/0.46 thf(c_0_72, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld, X10:mworld, X11:mworld, X12:mworld, X13:mworld, X14:mworld, X15:mworld, X16:mworld, X17:mworld, X18:mworld, X19:mworld, X20:mworld, X21:mworld, X22:mworld, X23:mworld, X24:mworld, X25:mworld]:((v6 @ (esk7_22 @ X3 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 @ X21 @ X22 @ X23 @ X24 @ X25))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_68, c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35])])).
% 0.54/0.46 thf(c_0_73, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v28 @ X3)|(v14 @ X5)|(v9 @ X6)|~((v15 @ X7)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_69, c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35])])).
% 0.54/0.46 thf(c_0_74, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld, X10:mworld, X11:mworld, X12:mworld, X13:mworld, X14:mworld, X15:mworld, X16:mworld]:((v15 @ (esk21_13 @ X3 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_70, c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35])])).
% 0.54/0.46 thf(c_0_75, plain, ![X531:mworld]:(((epred16_1 @ X531)<=>![X530:mworld]:(((mrel @ X531 @ X530)=>(~(v26 @ X530)|![X529:mworld]:(((mrel @ X530 @ X529)=>![X528:mworld]:(((mrel @ X529 @ X528)=>![X527:mworld]:(((mrel @ X528 @ X527)=>![X526:mworld]:(((mrel @ X527 @ X526)=>![X525:mworld]:(((mrel @ X526 @ X525)=>![X524:mworld]:(((mrel @ X525 @ X524)=>![X523:mworld]:(((mrel @ X524 @ X523)=>![X522:mworld]:(((mrel @ X523 @ X522)=>(~(v18 @ X522)|![X521:mworld]:(((mrel @ X522 @ X521)=>![X520:mworld]:(((mrel @ X521 @ X520)=>![X519:mworld]:(((mrel @ X520 @ X519)=>![X518:mworld]:(((mrel @ X519 @ X518)=>![X517:mworld]:(((mrel @ X518 @ X517)=>![X516:mworld]:(((mrel @ X517 @ X516)=>![X515:mworld]:(((mrel @ X516 @ X515)=>![X514:mworld]:(((mrel @ X515 @ X514)=>![X513:mworld]:(((mrel @ X514 @ X513)=>![X512:mworld]:(((mrel @ X513 @ X512)=>![X511:mworld]:(((mrel @ X512 @ X511)=>(~(v7 @ X511)|![X510:mworld]:(((mrel @ X511 @ X510)=>~(v6 @ X510)))))))))))))))))))))))))))))))))))))))))))))))), introduced(definition)).
% 0.54/0.46 thf(c_0_76, plain, ![X155:mworld]:(((mrel @ mactual @ X155)=>(~(v28 @ X155)|![X154:mworld]:(((mrel @ X155 @ X154)=>![X153:mworld]:(((mrel @ X154 @ X153)=>![X152:mworld]:(((mrel @ X153 @ X152)=>![X151:mworld]:(((mrel @ X152 @ X151)=>(~(v24 @ X151)|![X150:mworld]:(((mrel @ X151 @ X150)=>![X149:mworld]:(((mrel @ X150 @ X149)=>((v22 @ X149)|![X148:mworld]:(((mrel @ X149 @ X148)=>![X147:mworld]:(((mrel @ X148 @ X147)=>![X146:mworld]:(((mrel @ X147 @ X146)=>![X145:mworld]:(((mrel @ X146 @ X145)=>(v18 @ X145)))))))))))))))))))))))))), inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[mod8, c_0_16]), c_0_17]), c_0_18]), c_0_19])])).
% 0.54/0.46 thf(c_0_77, plain, ![X8:mworld, X7:mworld, X6:mworld, X5:mworld, X3:mworld]:((~((v23 @ (esk34_5 @ X3 @ X5 @ X6 @ X7 @ X8)))|~((mrel @ X7 @ X8))|~((mrel @ X6 @ X7))|~((mrel @ X5 @ X6))|~((mrel @ X3 @ X5))|~((mrel @ mactual @ X3)))), inference(split_conjunct,[status(thm)],[c_0_31])).
% 0.54/0.46 thf(c_0_78, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v14 @ X3)|(v6 @ X5)|(v23 @ X6)|~((v9 @ X7)))), inference(spm,[status(thm)],[c_0_71, c_0_72])).
% 0.54/0.46 thf(c_0_79, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((v28 @ X3)|(v14 @ X5)|(v9 @ X6))), inference(spm,[status(thm)],[c_0_73, c_0_74])).
% 0.54/0.46 thf(c_0_80, plain, ![X532:mworld]:(((mrel @ mactual @ X532)=>![X531:mworld]:(((mrel @ X532 @ X531)=>(epred16_1 @ X531))))), inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[mod24, c_0_16]), c_0_17]), c_0_18]), c_0_19])]), c_0_75])).
% 0.54/0.46 thf(c_0_81, plain, ![X1312:mworld, X1313:mworld, X1314:mworld, X1315:mworld, X1316:mworld, X1317:mworld, X1318:mworld, X1319:mworld, X1320:mworld, X1321:mworld, X1322:mworld]:((~(mrel @ mactual @ X1312)|(~(v28 @ X1312)|(~(mrel @ X1312 @ X1313)|(~(mrel @ X1313 @ X1314)|(~(mrel @ X1314 @ X1315)|(~(mrel @ X1315 @ X1316)|(~(v24 @ X1316)|(~(mrel @ X1316 @ X1317)|(~(mrel @ X1317 @ X1318)|((v22 @ X1318)|(~(mrel @ X1318 @ X1319)|(~(mrel @ X1319 @ X1320)|(~(mrel @ X1320 @ X1321)|(~(mrel @ X1321 @ X1322)|(v18 @ X1322)))))))))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_76])])])])).
% 0.54/0.46 thf(c_0_82, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld]:(~((v23 @ (esk34_5 @ X3 @ X5 @ X6 @ X7 @ X8)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_77, c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35])])).
% 0.54/0.46 thf(c_0_83, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld]:(((v14 @ X3)|(v28 @ X5)|(v23 @ X6)|(v6 @ X7)|(v14 @ X8))), inference(spm,[status(thm)],[c_0_78, c_0_79])).
% 0.54/0.46 thf(c_0_84, plain, ![X531:mworld]:(((epred16_1 @ X531)=>![X530:mworld]:(((mrel @ X531 @ X530)=>(~(v26 @ X530)|![X529:mworld]:(((mrel @ X530 @ X529)=>![X528:mworld]:(((mrel @ X529 @ X528)=>![X527:mworld]:(((mrel @ X528 @ X527)=>![X526:mworld]:(((mrel @ X527 @ X526)=>![X525:mworld]:(((mrel @ X526 @ X525)=>![X524:mworld]:(((mrel @ X525 @ X524)=>![X523:mworld]:(((mrel @ X524 @ X523)=>![X522:mworld]:(((mrel @ X523 @ X522)=>(~(v18 @ X522)|![X521:mworld]:(((mrel @ X522 @ X521)=>![X520:mworld]:(((mrel @ X521 @ X520)=>![X519:mworld]:(((mrel @ X520 @ X519)=>![X518:mworld]:(((mrel @ X519 @ X518)=>![X517:mworld]:(((mrel @ X518 @ X517)=>![X516:mworld]:(((mrel @ X517 @ X516)=>![X515:mworld]:(((mrel @ X516 @ X515)=>![X514:mworld]:(((mrel @ X515 @ X514)=>![X513:mworld]:(((mrel @ X514 @ X513)=>![X512:mworld]:(((mrel @ X513 @ X512)=>![X511:mworld]:(((mrel @ X512 @ X511)=>(~(v7 @ X511)|![X510:mworld]:(((mrel @ X511 @ X510)=>~(v6 @ X510)))))))))))))))))))))))))))))))))))))))))))))))), inference(split_equiv,[status(thm)],[c_0_75])).
% 0.54/0.46 thf(c_0_85, plain, ![X1395:mworld, X1396:mworld]:((~(mrel @ mactual @ X1395)|(~(mrel @ X1395 @ X1396)|(epred16_1 @ X1396)))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_80])])])])).
% 0.54/0.46 thf(c_0_86, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld, X10:mworld, X11:mworld, X12:mworld, X13:mworld, X14:mworld]:(((v22 @ X10)|(v18 @ X14)|~((mrel @ mactual @ X3))|~((v28 @ X3))|~((mrel @ X3 @ X5))|~((mrel @ X5 @ X6))|~((mrel @ X6 @ X7))|~((mrel @ X7 @ X8))|~((v24 @ X8))|~((mrel @ X8 @ X9))|~((mrel @ X9 @ X10))|~((mrel @ X10 @ X11))|~((mrel @ X11 @ X12))|~((mrel @ X12 @ X13))|~((mrel @ X13 @ X14)))), inference(split_conjunct,[status(thm)],[c_0_81])).
% 0.54/0.46 thf(c_0_87, plain, ![X7:mworld, X6:mworld, X5:mworld, X3:mworld]:(((v24 @ (esk35_4 @ X3 @ X5 @ X6 @ X7))|~((mrel @ X6 @ X7))|~((mrel @ X5 @ X6))|~((mrel @ X3 @ X5))|~((mrel @ mactual @ X3)))), inference(split_conjunct,[status(thm)],[c_0_31])).
% 0.54/0.46 thf(c_0_88, plain, ![X17:mworld, X16:mworld, X15:mworld, X14:mworld, X13:mworld, X12:mworld, X11:mworld, X10:mworld, X9:mworld, X8:mworld, X7:mworld, X6:mworld, X5:mworld, X3:mworld]:((~((v14 @ (esk20_14 @ X3 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17)))|~((mrel @ X16 @ X17))|~((mrel @ X15 @ X16))|~((mrel @ X14 @ X15))|~((mrel @ X13 @ X14))|~((mrel @ X12 @ X13))|~((mrel @ X11 @ X12))|~((mrel @ X10 @ X11))|~((mrel @ X9 @ X10))|~((mrel @ X8 @ X9))|~((mrel @ X7 @ X8))|~((mrel @ X6 @ X7))|~((mrel @ X5 @ X6))|~((mrel @ X3 @ X5))|~((mrel @ mactual @ X3)))), inference(split_conjunct,[status(thm)],[c_0_31])).
% 0.54/0.46 thf(c_0_89, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v14 @ X3)|(v6 @ X5)|(v28 @ X6)|(v14 @ X7))), inference(spm,[status(thm)],[c_0_82, c_0_83])).
% 0.54/0.46 thf(c_0_90, plain, ![X2042:mworld, X2043:mworld, X2044:mworld, X2045:mworld, X2046:mworld, X2047:mworld, X2048:mworld, X2049:mworld, X2050:mworld, X2051:mworld, X2052:mworld, X2053:mworld, X2054:mworld, X2055:mworld, X2056:mworld, X2057:mworld, X2058:mworld, X2059:mworld, X2060:mworld, X2061:mworld, X2062:mworld, X2063:mworld]:((~(epred16_1 @ X2042)|(~(mrel @ X2042 @ X2043)|(~(v26 @ X2043)|(~(mrel @ X2043 @ X2044)|(~(mrel @ X2044 @ X2045)|(~(mrel @ X2045 @ X2046)|(~(mrel @ X2046 @ X2047)|(~(mrel @ X2047 @ X2048)|(~(mrel @ X2048 @ X2049)|(~(mrel @ X2049 @ X2050)|(~(mrel @ X2050 @ X2051)|(~(v18 @ X2051)|(~(mrel @ X2051 @ X2052)|(~(mrel @ X2052 @ X2053)|(~(mrel @ X2053 @ X2054)|(~(mrel @ X2054 @ X2055)|(~(mrel @ X2055 @ X2056)|(~(mrel @ X2056 @ X2057)|(~(mrel @ X2057 @ X2058)|(~(mrel @ X2058 @ X2059)|(~(mrel @ X2059 @ X2060)|(~(mrel @ X2060 @ X2061)|(~(mrel @ X2061 @ X2062)|(~(v7 @ X2062)|(~(mrel @ X2062 @ X2063)|~(v6 @ X2063))))))))))))))))))))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_84])])])])).
% 0.54/0.46 thf(c_0_91, plain, ![X3:mworld, X5:mworld]:(((epred16_1 @ X5)|~((mrel @ mactual @ X3))|~((mrel @ X3 @ X5)))), inference(split_conjunct,[status(thm)],[c_0_85])).
% 0.54/0.46 thf(c_0_92, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v22 @ X3)|(v18 @ X5)|~((v24 @ X6))|~((v28 @ X7)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_86, c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35])])).
% 0.54/0.46 thf(c_0_93, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:((v24 @ (esk35_4 @ X3 @ X5 @ X6 @ X7))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_87, c_0_35]), c_0_35]), c_0_35]), c_0_35])])).
% 0.54/0.46 thf(c_0_94, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld, X10:mworld, X11:mworld, X12:mworld, X13:mworld, X14:mworld, X15:mworld, X16:mworld, X17:mworld]:(~((v14 @ (esk20_14 @ X3 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_88, c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35])])).
% 0.54/0.46 thf(c_0_95, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((v14 @ X3)|(v28 @ X5)|(v6 @ X6))), inference(ef,[status(thm)],[c_0_89])).
% 0.54/0.46 thf(c_0_96, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld, X10:mworld, X11:mworld, X12:mworld, X13:mworld, X14:mworld, X15:mworld, X16:mworld, X17:mworld, X18:mworld, X19:mworld, X20:mworld, X21:mworld, X22:mworld, X23:mworld, X24:mworld, X25:mworld]:((~((epred16_1 @ X3))|~((mrel @ X3 @ X5))|~((v26 @ X5))|~((mrel @ X5 @ X6))|~((mrel @ X6 @ X7))|~((mrel @ X7 @ X8))|~((mrel @ X8 @ X9))|~((mrel @ X9 @ X10))|~((mrel @ X10 @ X11))|~((mrel @ X11 @ X12))|~((mrel @ X12 @ X13))|~((v18 @ X13))|~((mrel @ X13 @ X14))|~((mrel @ X14 @ X15))|~((mrel @ X15 @ X16))|~((mrel @ X16 @ X17))|~((mrel @ X17 @ X18))|~((mrel @ X18 @ X19))|~((mrel @ X19 @ X20))|~((mrel @ X20 @ X21))|~((mrel @ X21 @ X22))|~((mrel @ X22 @ X23))|~((mrel @ X23 @ X24))|~((v7 @ X24))|~((mrel @ X24 @ X25))|~((v6 @ X25)))), inference(split_conjunct,[status(thm)],[c_0_90])).
% 0.54/0.46 thf(c_0_97, plain, ![X3:mworld]:((epred16_1 @ X3)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_91, c_0_35]), c_0_35])])).
% 0.54/0.46 thf(c_0_98, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((v22 @ X3)|(v18 @ X5)|~((v28 @ X6)))), inference(spm,[status(thm)],[c_0_92, c_0_93])).
% 0.54/0.46 thf(c_0_99, plain, ![X3:mworld, X5:mworld]:(((v6 @ X3)|(v28 @ X5))), inference(spm,[status(thm)],[c_0_94, c_0_95])).
% 0.54/0.46 thf(c_0_100, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:((~((v6 @ X3))|~((v7 @ X5))|~((v18 @ X6))|~((v26 @ X7)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_96, c_0_97]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35])])).
% 0.54/0.46 thf(c_0_101, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((v6 @ X3)|(v18 @ X5)|(v22 @ X6))), inference(spm,[status(thm)],[c_0_98, c_0_99])).
% 0.54/0.46 thf(c_0_102, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld]:(((v22 @ X3)|(v6 @ X5)|~((v6 @ X6))|~((v7 @ X7))|~((v26 @ X8)))), inference(spm,[status(thm)],[c_0_100, c_0_101])).
% 0.54/0.46 thf(c_0_103, plain, ![X24:mworld, X23:mworld, X22:mworld, X21:mworld, X20:mworld, X19:mworld, X18:mworld, X17:mworld, X16:mworld, X15:mworld, X14:mworld, X13:mworld, X12:mworld, X11:mworld, X10:mworld, X9:mworld, X8:mworld, X7:mworld, X6:mworld, X5:mworld, X3:mworld]:(((v7 @ (esk9_21 @ X3 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 @ X21 @ X22 @ X23 @ X24))|~((mrel @ X23 @ X24))|~((mrel @ X22 @ X23))|~((mrel @ X21 @ X22))|~((mrel @ X20 @ X21))|~((mrel @ X19 @ X20))|~((mrel @ X18 @ X19))|~((mrel @ X17 @ X18))|~((mrel @ X16 @ X17))|~((mrel @ X15 @ X16))|~((mrel @ X14 @ X15))|~((mrel @ X13 @ X14))|~((mrel @ X12 @ X13))|~((mrel @ X11 @ X12))|~((mrel @ X10 @ X11))|~((mrel @ X9 @ X10))|~((mrel @ X8 @ X9))|~((mrel @ X7 @ X8))|~((mrel @ X6 @ X7))|~((mrel @ X5 @ X6))|~((mrel @ X3 @ X5))|~((mrel @ mactual @ X3)))), inference(split_conjunct,[status(thm)],[c_0_31])).
% 0.54/0.46 thf(c_0_104, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v6 @ X3)|(v22 @ X5)|~((v7 @ X6))|~((v26 @ X7)))), inference(spm,[status(thm)],[c_0_102, c_0_72])).
% 0.54/0.46 thf(c_0_105, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld, X10:mworld, X11:mworld, X12:mworld, X13:mworld, X14:mworld, X15:mworld, X16:mworld, X17:mworld, X18:mworld, X19:mworld, X20:mworld, X21:mworld, X22:mworld, X23:mworld, X24:mworld]:((v7 @ (esk9_21 @ X3 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 @ X21 @ X22 @ X23 @ X24))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_103, c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35])])).
% 0.54/0.46 thf(c_0_106, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((v22 @ X3)|(v6 @ X5)|~((v26 @ X6)))), inference(spm,[status(thm)],[c_0_104, c_0_105])).
% 0.54/0.46 thf(c_0_107, plain, ![X9:mworld, X8:mworld, X7:mworld, X6:mworld, X5:mworld, X3:mworld]:((~((v22 @ (esk32_6 @ X3 @ X5 @ X6 @ X7 @ X8 @ X9)))|~((mrel @ X8 @ X9))|~((mrel @ X7 @ X8))|~((mrel @ X6 @ X7))|~((mrel @ X5 @ X6))|~((mrel @ X3 @ X5))|~((mrel @ mactual @ X3)))), inference(split_conjunct,[status(thm)],[c_0_31])).
% 0.54/0.46 thf(c_0_108, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((v6 @ X3)|(v22 @ X5)|~((v13 @ X6)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_106, c_0_51]), c_0_99])).
% 0.54/0.46 thf(c_0_109, plain, ![X25:mworld, X24:mworld, X23:mworld, X22:mworld, X21:mworld, X20:mworld, X19:mworld, X18:mworld, X17:mworld, X16:mworld, X15:mworld, X14:mworld, X13:mworld, X12:mworld, X11:mworld, X10:mworld, X9:mworld, X8:mworld, X7:mworld, X6:mworld, X5:mworld, X3:mworld]:((~((v6 @ (esk8_22 @ X3 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 @ X21 @ X22 @ X23 @ X24 @ X25)))|~((mrel @ X24 @ X25))|~((mrel @ X23 @ X24))|~((mrel @ X22 @ X23))|~((mrel @ X21 @ X22))|~((mrel @ X20 @ X21))|~((mrel @ X19 @ X20))|~((mrel @ X18 @ X19))|~((mrel @ X17 @ X18))|~((mrel @ X16 @ X17))|~((mrel @ X15 @ X16))|~((mrel @ X14 @ X15))|~((mrel @ X13 @ X14))|~((mrel @ X12 @ X13))|~((mrel @ X11 @ X12))|~((mrel @ X10 @ X11))|~((mrel @ X9 @ X10))|~((mrel @ X8 @ X9))|~((mrel @ X7 @ X8))|~((mrel @ X6 @ X7))|~((mrel @ X5 @ X6))|~((mrel @ X3 @ X5))|~((mrel @ mactual @ X3)))), inference(split_conjunct,[status(thm)],[c_0_31])).
% 0.54/0.46 thf(c_0_110, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld]:(~((v22 @ (esk32_6 @ X3 @ X5 @ X6 @ X7 @ X8 @ X9)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_107, c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35])])).
% 0.54/0.46 thf(c_0_111, plain, ![X3:mworld, X5:mworld]:(((v22 @ X3)|(v6 @ X5))), inference(spm,[status(thm)],[c_0_108, c_0_59])).
% 0.54/0.46 thf(c_0_112, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld, X10:mworld, X11:mworld, X12:mworld, X13:mworld, X14:mworld, X15:mworld, X16:mworld, X17:mworld, X18:mworld, X19:mworld, X20:mworld, X21:mworld, X22:mworld, X23:mworld, X24:mworld, X25:mworld]:(~((v6 @ (esk8_22 @ X3 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 @ X21 @ X22 @ X23 @ X24 @ X25)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_109, c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35]), c_0_35])])).
% 0.54/0.46 thf(c_0_113, plain, ![X3:mworld]:((v6 @ X3)), inference(spm,[status(thm)],[c_0_110, c_0_111])).
% 0.54/0.46 thf(c_0_114, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_112, c_0_113])]), ['proof']).
% 0.54/0.46 % SZS output end CNFRefutation
% 0.54/0.46 % Parsed axioms : 100
% 0.54/0.46 % Removed by relevancy pruning/SinE : 0
% 0.54/0.46 % Initial clauses : 205
% 0.54/0.46 % Removed in clause preprocessing : 56
% 0.54/0.46 % Initial clauses in saturation : 149
% 0.54/0.46 % Processed clauses : 343
% 0.54/0.46 % ...of these trivial : 39
% 0.54/0.46 % ...subsumed : 0
% 0.54/0.46 % ...remaining for further processing : 304
% 0.54/0.46 % Other redundant clauses eliminated : 0
% 0.54/0.46 % Clauses deleted for lack of memory : 0
% 0.54/0.46 % Backward-subsumed : 46
% 0.54/0.46 % Backward-rewritten : 22
% 0.54/0.46 % Generated clauses : 125
% 0.54/0.46 % ...of the previous two non-redundant : 131
% 0.54/0.46 % ...aggressively subsumed : 0
% 0.54/0.46 % Contextual simplify-reflections : 4
% 0.54/0.46 % Paramodulations : 123
% 0.54/0.46 % Factorizations : 2
% 0.54/0.46 % NegExts : 0
% 0.54/0.46 % Equation resolutions : 0
% 0.54/0.46 % Disequality decompositions : 0
% 0.54/0.46 % Total rewrite steps : 2092
% 0.54/0.46 % ...of those cached : 1967
% 0.54/0.46 % Propositional unsat checks : 0
% 0.54/0.46 % Propositional check models : 0
% 0.54/0.46 % Propositional check unsatisfiable : 0
% 0.54/0.46 % Propositional clauses : 0
% 0.54/0.47 % Propositional clauses after purity: 0
% 0.54/0.47 % Propositional unsat core size : 0
% 0.54/0.47 % Propositional preprocessing time : 0.000
% 0.54/0.47 % Propositional encoding time : 0.000
% 0.54/0.47 % Propositional solver time : 0.000
% 0.54/0.47 % Success case prop preproc time : 0.000
% 0.54/0.47 % Success case prop encoding time : 0.000
% 0.54/0.47 % Success case prop solver time : 0.000
% 0.54/0.47 % Current number of processed clauses : 127
% 0.54/0.47 % Positive orientable unit clauses : 38
% 0.54/0.47 % Positive unorientable unit clauses: 0
% 0.54/0.47 % Negative unit clauses : 11
% 0.54/0.47 % Non-unit-clauses : 78
% 0.54/0.47 % Current number of unprocessed clauses: 35
% 0.54/0.47 % ...number of literals in the above : 205
% 0.54/0.47 % Current number of archived formulas : 0
% 0.54/0.47 % Current number of archived clauses : 177
% 0.54/0.47 % Clause-clause subsumption calls (NU) : 3950
% 0.54/0.47 % Rec. Clause-clause subsumption calls : 1046
% 0.54/0.47 % Non-unit clause-clause subsumptions : 50
% 0.54/0.47 % Unit Clause-clause subsumption calls : 489
% 0.54/0.47 % Rewrite failures with RHS unbound : 0
% 0.54/0.47 % BW rewrite match attempts : 7
% 0.54/0.47 % BW rewrite match successes : 7
% 0.54/0.47 % Condensation attempts : 0
% 0.54/0.47 % Condensation successes : 0
% 0.54/0.47 % Termbank termtop insertions : 100499
% 0.54/0.47 % Search garbage collected termcells : 47582
% 0.54/0.47
% 0.54/0.47 % -------------------------------------------------
% 0.54/0.47 % User time : 0.143 s
% 0.54/0.47 % System time : 0.026 s
% 0.54/0.47 % Total time : 0.169 s
% 0.54/0.47 % Maximum resident set size: 10524 pages
% 0.54/0.47
% 0.54/0.47 % -------------------------------------------------
% 0.54/0.47 % User time : 0.357 s
% 0.54/0.47 % System time : 0.073 s
% 0.54/0.47 % Total time : 0.429 s
% 0.54/0.47 % Maximum resident set size: 5120 pages
% 0.54/0.47 % E exiting
%------------------------------------------------------------------------------