%------------------------------------------------------------------------------
% File : E-SAT---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 : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:44:58 AM UTC 2026
% Result : ContradictoryAxioms 0.54s 0.47s
% Output : CNFRefutation 0.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO904^12 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.20 % Computer : n003.cluster.edu
% 0.12/0.20 % Model : x86_64 x86_64
% 0.12/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.20 % Memory : 8046.5625MB
% 0.12/0.20 % OS : Linux 6.8.0-71-generic
% 0.12/0.20 % CPULimit : 300
% 0.12/0.20 % WCLimit : 300
% 0.12/0.20 % DateTime : Tue Sep 29 17:28:29 UTC 2026
% 0.12/0.20 % CPUTime :
% 0.12/0.20 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.24 Running higher-order theorem proving
% 0.12/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.mkBzuj3Fsg/E---3.1_2803652.p
% 0.54/0.47 % Version: 3.5.1-ho
% 0.54/0.47 % Preprocessing class: HSLSSMSSMLLNHSN.
% 0.54/0.47 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.54/0.47 % Starting almost_fo_3 with 1500s (5) cores
% 0.54/0.47 % Starting sh10 with 300s (1) cores
% 0.54/0.47 % Starting new_ho_16 with 300s (1) cores
% 0.54/0.47 % Starting post_as_ho11 with 300s (1) cores
% 0.54/0.47 % new_ho_16 with pid 2803667 completed with status 9
% 0.54/0.47 % almost_fo_3 with pid 2803665 completed with status 0
% 0.54/0.47 % Result found by almost_fo_3
% 0.54/0.47 % Preprocessing class: HSLSSMSSMLLNHSN.
% 0.54/0.47 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.54/0.47 % Starting almost_fo_3 with 1500s (5) cores
% 0.54/0.47 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.54/0.47 % No SInE strategy applied
% 0.54/0.47 % Search class: HGHNF-FSLF33-SHSSMFNN
% 0.54/0.47 % partial match(1): HGHNS-FSLF33-SHSSMFNN
% 0.54/0.47 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.54/0.47 % Starting SubtermCWHack with 136s (1) cores
% 0.54/0.47 % Starting almost_fo_3 with 151s (1) cores
% 0.54/0.47 % Starting new_ho_16 with 136s (1) cores
% 0.54/0.47 % Starting sh5l with 136s (1) cores
% 0.54/0.47 % Starting ehoh_best8_lambda with 136s (1) cores
% 0.54/0.47 % almost_fo_3 with pid 2803685 completed with status 0
% 0.54/0.47 % Result found by almost_fo_3
% 0.54/0.47 % Preprocessing class: HSLSSMSSMLLNHSN.
% 0.54/0.47 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.54/0.47 % Starting almost_fo_3 with 1500s (5) cores
% 0.54/0.47 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.54/0.47 % No SInE strategy applied
% 0.54/0.47 % Search class: HGHNF-FSLF33-SHSSMFNN
% 0.54/0.47 % partial match(1): HGHNS-FSLF33-SHSSMFNN
% 0.54/0.47 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.54/0.47 % Starting SubtermCWHack with 136s (1) cores
% 0.54/0.47 % Starting almost_fo_3 with 151s (1) cores
% 0.54/0.47 % Preprocessing time : 0.010 s
% 0.54/0.47 % Presaturation interreduction done
% 0.54/0.47
% 0.54/0.47 % Proof found!
% 0.54/0.47 % SZS status ContradictoryAxioms
% 0.54/0.47 % SZS output start CNFRefutation
% 0.54/0.47 thf(decl_sort1, type, mworld: $tType).
% 0.54/0.47 thf(decl_23, type, mrel: mworld > mworld > $o).
% 0.54/0.47 thf(decl_24, type, mactual: mworld).
% 0.54/0.47 thf(decl_25, type, mlocal: (mworld > $o) > $o).
% 0.54/0.47 thf(decl_26, type, mnot: (mworld > $o) > mworld > $o).
% 0.54/0.47 thf(decl_27, type, mand: (mworld > $o) > (mworld > $o) > mworld > $o).
% 0.54/0.47 thf(decl_28, type, mor: (mworld > $o) > (mworld > $o) > mworld > $o).
% 0.54/0.47 thf(decl_31, type, mbox: (mworld > $o) > mworld > $o).
% 0.54/0.47 thf(decl_32, type, mdia: (mworld > $o) > mworld > $o).
% 0.54/0.47 thf(decl_34, type, v2: mworld > $o).
% 0.54/0.47 thf(decl_35, type, v3: mworld > $o).
% 0.54/0.47 thf(decl_36, type, v4: mworld > $o).
% 0.54/0.47 thf(decl_37, type, v5: mworld > $o).
% 0.54/0.47 thf(decl_38, type, v6: mworld > $o).
% 0.54/0.47 thf(decl_39, type, v7: mworld > $o).
% 0.54/0.47 thf(decl_40, type, v8: mworld > $o).
% 0.54/0.47 thf(decl_41, type, v9: mworld > $o).
% 0.54/0.47 thf(decl_45, type, v14: mworld > $o).
% 0.54/0.47 thf(decl_46, type, v13: mworld > $o).
% 0.54/0.47 thf(decl_47, type, v16: mworld > $o).
% 0.54/0.47 thf(decl_48, type, v15: mworld > $o).
% 0.54/0.47 thf(decl_49, type, v18: mworld > $o).
% 0.54/0.47 thf(decl_52, type, v21: mworld > $o).
% 0.54/0.47 thf(decl_54, type, v23: mworld > $o).
% 0.54/0.47 thf(decl_55, type, v22: mworld > $o).
% 0.54/0.47 thf(decl_56, type, v25: mworld > $o).
% 0.54/0.47 thf(decl_57, type, v24: mworld > $o).
% 0.54/0.47 thf(decl_59, type, v26: mworld > $o).
% 0.54/0.47 thf(decl_60, type, v28: mworld > $o).
% 0.54/0.47 thf(decl_76, type, epred16_1: mworld > $o).
% 0.54/0.47 thf(decl_79, type, epred19_1: mworld > $o).
% 0.54/0.47 thf(decl_90, type, epred30_1: mworld > $o).
% 0.54/0.47 thf(decl_91, type, epred31_1: mworld > $o).
% 0.54/0.47 thf(decl_94, type, epred34_1: mworld > $o).
% 0.54/0.47 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.47 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.47 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.47 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.47 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.47 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.47 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.47 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.47 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.47 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.47 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.47 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.47 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.47 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.47 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.47 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.47 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.47 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.47 thf(decl_113, type, esk19_14: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.47 thf(decl_114, type, esk20_14: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.47 thf(decl_115, type, esk21_13: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.47 thf(decl_116, type, esk22_13: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.47 thf(decl_117, type, esk23_12: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.47 thf(decl_118, type, esk24_12: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.47 thf(decl_119, type, esk25_11: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.47 thf(decl_120, type, esk26_10: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.47 thf(decl_121, type, esk27_9: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.47 thf(decl_122, type, esk28_8: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.47 thf(decl_123, type, esk29_7: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.47 thf(decl_124, type, esk30_7: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.47 thf(decl_125, type, esk31_6: mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.47 thf(decl_126, type, esk32_6: mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.47 thf(decl_127, type, esk33_5: mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.47 thf(decl_128, type, esk34_5: mworld > mworld > mworld > mworld > mworld > mworld).
% 0.54/0.47 thf(decl_129, type, esk35_4: mworld > mworld > mworld > mworld > mworld).
% 0.54/0.47 thf(decl_130, type, esk36_4: mworld > mworld > mworld > mworld > mworld).
% 0.54/0.47 thf(decl_131, type, esk37_3: mworld > mworld > mworld > mworld).
% 0.54/0.47 thf(decl_132, type, esk38_2: mworld > mworld > mworld).
% 0.54/0.47 thf(decl_133, type, esk39_1: mworld > mworld).
% 0.54/0.47 thf(decl_134, type, esk40_0: mworld).
% 0.54/0.47 thf(mlocal_def, axiom, ((mlocal)=(^[X1:mworld > $o]:((X1 @ mactual)))), file('/export/starexec/sandbox2/tmp/tmp.mkBzuj3Fsg/E---3.1_2803652.p', mlocal_def)).
% 0.54/0.47 thf(mnot_def, axiom, ((mnot)=(^[X2:mworld > $o, X3:mworld]:(~((X2 @ X3))))), file('/export/starexec/sandbox2/tmp/tmp.mkBzuj3Fsg/E---3.1_2803652.p', mnot_def)).
% 0.54/0.47 thf(mor_def, axiom, ((mor)=(^[X2:mworld > $o, X4:mworld > $o, X3:mworld]:((((X2 @ X3))|((X4 @ X3)))))), file('/export/starexec/sandbox2/tmp/tmp.mkBzuj3Fsg/E---3.1_2803652.p', mor_def)).
% 0.54/0.47 thf(mbox_def, axiom, ((mbox)=(^[X1:mworld > $o, X3:mworld]:(![X5:mworld]:((((mrel @ X3 @ X5))=>((X1 @ X5))))))), file('/export/starexec/sandbox2/tmp/tmp.mkBzuj3Fsg/E---3.1_2803652.p', mbox_def)).
% 0.54/0.47 thf(mod50, axiom, (mlocal @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v8) @ (mbox @ (mor @ (mnot @ v7) @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v4) @ (mbox @ (mbox @ (mnot @ v2)))))))))))))))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.mkBzuj3Fsg/E---3.1_2803652.p', mod50)).
% 0.54/0.47 thf(mod47, axiom, (mlocal @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v13 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v5 @ (mbox @ (mbox @ (mor @ v3 @ (mbox @ v2))))))))))))))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.mkBzuj3Fsg/E---3.1_2803652.p', mod47)).
% 0.54/0.47 thf(mrel_universal, axiom, ![X3:mworld, X5:mworld]:((mrel @ X3 @ X5)), file('/export/starexec/sandbox2/tmp/tmp.mkBzuj3Fsg/E---3.1_2803652.p', mrel_universal)).
% 0.54/0.47 thf(mod29, axiom, (mlocal @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v25) @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v21) @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v6) @ (mbox @ (mbox @ v4))))))))))))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.mkBzuj3Fsg/E---3.1_2803652.p', mod29)).
% 0.54/0.47 thf(mand_def, axiom, ((mand)=(^[X2:mworld > $o, X4:mworld > $o, X3:mworld]:((((X2 @ X3))&((X4 @ X3)))))), file('/export/starexec/sandbox2/tmp/tmp.mkBzuj3Fsg/E---3.1_2803652.p', mand_def)).
% 0.54/0.47 thf(mdia_def, axiom, ((mdia)=(^[X1:mworld > $o, X3:mworld]:(?[X5:mworld]:((((mrel @ X3 @ X5))&((X1 @ X5))))))), file('/export/starexec/sandbox2/tmp/tmp.mkBzuj3Fsg/E---3.1_2803652.p', mdia_def)).
% 0.54/0.47 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.mkBzuj3Fsg/E---3.1_2803652.p', alt1)).
% 0.54/0.47 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.mkBzuj3Fsg/E---3.1_2803652.p', mod4)).
% 0.54/0.47 thf(mod25, axiom, (mlocal @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v25 @ (mbox @ (mbox @ (mor @ v23 @ (mbox @ (mor @ (mnot @ v22) @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mnot @ v9))))))))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.mkBzuj3Fsg/E---3.1_2803652.p', mod25)).
% 0.54/0.47 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.mkBzuj3Fsg/E---3.1_2803652.p', mod45)).
% 0.54/0.47 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.mkBzuj3Fsg/E---3.1_2803652.p', mod8)).
% 0.54/0.47 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.mkBzuj3Fsg/E---3.1_2803652.p', mod24)).
% 0.54/0.47 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.mkBzuj3Fsg/E---3.1_2803652.p', mod6)).
% 0.54/0.47 thf(c_0_17, plain, ((mlocal)=(^[Z0:mworld > $o]:((Z0 @ mactual)))), inference(fof_simplification,[status(thm)],[mlocal_def])).
% 0.54/0.47 thf(c_0_18, plain, ((mnot)=(^[Z0:mworld > $o, Z1:mworld]:(~((Z0 @ Z1))))), inference(fof_simplification,[status(thm)],[mnot_def])).
% 0.54/0.47 thf(c_0_19, plain, ((mor)=(^[Z0:mworld > $o, Z1:mworld > $o, Z2:mworld]:((((Z0 @ Z2))|((Z1 @ Z2)))))), inference(fof_simplification,[status(thm)],[mor_def])).
% 0.54/0.47 thf(c_0_20, plain, ((mbox)=(^[Z0:mworld > $o, Z1:mworld]:(![X5:mworld]:((((mrel @ Z1 @ X5))=>((Z0 @ X5))))))), inference(fof_simplification,[status(thm)],[mbox_def])).
% 0.54/0.47 thf(c_0_21, plain, ![X1144:mworld]:(((epred34_1 @ X1144)<=>![X1143:mworld]:(((mrel @ X1144 @ X1143)=>![X1142:mworld]:(((mrel @ X1143 @ X1142)=>![X1141:mworld]:(((mrel @ X1142 @ X1141)=>![X1140:mworld]:(((mrel @ X1141 @ X1140)=>![X1139:mworld]:(((mrel @ X1140 @ X1139)=>![X1138:mworld]:(((mrel @ X1139 @ X1138)=>![X1137:mworld]:(((mrel @ X1138 @ X1137)=>![X1136:mworld]:(((mrel @ X1137 @ X1136)=>![X1135:mworld]:(((mrel @ X1136 @ X1135)=>![X1134:mworld]:(((mrel @ X1135 @ X1134)=>![X1133:mworld]:(((mrel @ X1134 @ X1133)=>![X1132:mworld]:(((mrel @ X1133 @ X1132)=>![X1131:mworld]:(((mrel @ X1132 @ X1131)=>![X1130:mworld]:(((mrel @ X1131 @ X1130)=>![X1129:mworld]:(((mrel @ X1130 @ X1129)=>(~(v8 @ X1129)|![X1128:mworld]:(((mrel @ X1129 @ X1128)=>(~(v7 @ X1128)|![X1127:mworld]:(((mrel @ X1128 @ X1127)=>![X1126:mworld]:(((mrel @ X1127 @ X1126)=>![X1125:mworld]:(((mrel @ X1126 @ X1125)=>(~(v4 @ X1125)|![X1124:mworld]:(((mrel @ X1125 @ X1124)=>![X1123:mworld]:(((mrel @ X1124 @ X1123)=>~(v2 @ X1123)))))))))))))))))))))))))))))))))))))))))))))))), introduced(definition)).
% 0.54/0.47 thf(c_0_22, plain, ![X1064:mworld]:(((epred31_1 @ X1064)<=>![X1063:mworld]:(((mrel @ X1064 @ X1063)=>![X1062:mworld]:(((mrel @ X1063 @ X1062)=>![X1061:mworld]:(((mrel @ X1062 @ X1061)=>![X1060:mworld]:(((mrel @ X1061 @ X1060)=>![X1059:mworld]:(((mrel @ X1060 @ X1059)=>![X1058:mworld]:(((mrel @ X1059 @ X1058)=>![X1057:mworld]:(((mrel @ X1058 @ X1057)=>![X1056:mworld]:(((mrel @ X1057 @ X1056)=>![X1055:mworld]:(((mrel @ X1056 @ X1055)=>![X1054:mworld]:(((mrel @ X1055 @ X1054)=>((v13 @ X1054)|![X1053:mworld]:(((mrel @ X1054 @ X1053)=>![X1052:mworld]:(((mrel @ X1053 @ X1052)=>![X1051:mworld]:(((mrel @ X1052 @ X1051)=>![X1050:mworld]:(((mrel @ X1051 @ X1050)=>![X1049:mworld]:(((mrel @ X1050 @ X1049)=>![X1048:mworld]:(((mrel @ X1049 @ X1048)=>![X1047:mworld]:(((mrel @ X1048 @ X1047)=>![X1046:mworld]:(((mrel @ X1047 @ X1046)=>((v5 @ X1046)|![X1045:mworld]:(((mrel @ X1046 @ X1045)=>![X1044:mworld]:(((mrel @ X1045 @ X1044)=>((v3 @ X1044)|![X1043:mworld]:(((mrel @ X1044 @ X1043)=>(v2 @ X1043)))))))))))))))))))))))))))))))))))))))))))))))), introduced(definition)).
% 0.54/0.47 thf(c_0_23, plain, ![X1149:mworld]:(((mrel @ mactual @ X1149)=>![X1148:mworld]:(((mrel @ X1149 @ X1148)=>![X1147:mworld]:(((mrel @ X1148 @ X1147)=>![X1146:mworld]:(((mrel @ X1147 @ X1146)=>![X1145:mworld]:(((mrel @ X1146 @ X1145)=>![X1144:mworld]:(((mrel @ X1145 @ X1144)=>(epred34_1 @ X1144))))))))))))), 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)],[mod50, c_0_17]), c_0_18]), c_0_19]), c_0_20])]), c_0_21])).
% 0.54/0.47 thf(c_0_24, plain, ![X1069:mworld]:(((mrel @ mactual @ X1069)=>![X1068:mworld]:(((mrel @ X1069 @ X1068)=>![X1067:mworld]:(((mrel @ X1068 @ X1067)=>![X1066:mworld]:(((mrel @ X1067 @ X1066)=>![X1065:mworld]:(((mrel @ X1066 @ X1065)=>![X1064:mworld]:(((mrel @ X1065 @ X1064)=>(epred31_1 @ X1064))))))))))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[mod47, c_0_17]), c_0_19]), c_0_20]), c_0_22])).
% 0.54/0.47 thf(c_0_25, plain, ![X638:mworld]:(((epred19_1 @ X638)<=>(~(v25 @ X638)|![X637:mworld]:(((mrel @ X638 @ X637)=>![X636:mworld]:(((mrel @ X637 @ X636)=>![X635:mworld]:(((mrel @ X636 @ X635)=>![X634:mworld]:(((mrel @ X635 @ X634)=>(~(v21 @ X634)|![X633:mworld]:(((mrel @ X634 @ X633)=>![X632:mworld]:(((mrel @ X633 @ X632)=>![X631:mworld]:(((mrel @ X632 @ X631)=>![X630:mworld]:(((mrel @ X631 @ X630)=>![X629:mworld]:(((mrel @ X630 @ X629)=>![X628:mworld]:(((mrel @ X629 @ X628)=>![X627:mworld]:(((mrel @ X628 @ X627)=>![X626:mworld]:(((mrel @ X627 @ X626)=>![X625:mworld]:(((mrel @ X626 @ X625)=>![X624:mworld]:(((mrel @ X625 @ X624)=>![X623:mworld]:(((mrel @ X624 @ X623)=>![X622:mworld]:(((mrel @ X623 @ X622)=>![X621:mworld]:(((mrel @ X622 @ X621)=>![X620:mworld]:(((mrel @ X621 @ X620)=>![X619:mworld]:(((mrel @ X620 @ X619)=>(~(v6 @ X619)|![X618:mworld]:(((mrel @ X619 @ X618)=>![X617:mworld]:(((mrel @ X618 @ X617)=>(v4 @ X617)))))))))))))))))))))))))))))))))))))))))))))))), introduced(definition)).
% 0.54/0.47 thf(c_0_26, plain, ![X1144:mworld]:(((epred34_1 @ X1144)=>![X1143:mworld]:(((mrel @ X1144 @ X1143)=>![X1142:mworld]:(((mrel @ X1143 @ X1142)=>![X1141:mworld]:(((mrel @ X1142 @ X1141)=>![X1140:mworld]:(((mrel @ X1141 @ X1140)=>![X1139:mworld]:(((mrel @ X1140 @ X1139)=>![X1138:mworld]:(((mrel @ X1139 @ X1138)=>![X1137:mworld]:(((mrel @ X1138 @ X1137)=>![X1136:mworld]:(((mrel @ X1137 @ X1136)=>![X1135:mworld]:(((mrel @ X1136 @ X1135)=>![X1134:mworld]:(((mrel @ X1135 @ X1134)=>![X1133:mworld]:(((mrel @ X1134 @ X1133)=>![X1132:mworld]:(((mrel @ X1133 @ X1132)=>![X1131:mworld]:(((mrel @ X1132 @ X1131)=>![X1130:mworld]:(((mrel @ X1131 @ X1130)=>![X1129:mworld]:(((mrel @ X1130 @ X1129)=>(~(v8 @ X1129)|![X1128:mworld]:(((mrel @ X1129 @ X1128)=>(~(v7 @ X1128)|![X1127:mworld]:(((mrel @ X1128 @ X1127)=>![X1126:mworld]:(((mrel @ X1127 @ X1126)=>![X1125:mworld]:(((mrel @ X1126 @ X1125)=>(~(v4 @ X1125)|![X1124:mworld]:(((mrel @ X1125 @ X1124)=>![X1123:mworld]:(((mrel @ X1124 @ X1123)=>~(v2 @ X1123)))))))))))))))))))))))))))))))))))))))))))))))), inference(split_equiv,[status(thm)],[c_0_21])).
% 0.54/0.47 thf(c_0_27, plain, ![X1628:mworld, X1629:mworld, X1630:mworld, X1631:mworld, X1632:mworld, X1633:mworld]:((~(mrel @ mactual @ X1628)|(~(mrel @ X1628 @ X1629)|(~(mrel @ X1629 @ X1630)|(~(mrel @ X1630 @ X1631)|(~(mrel @ X1631 @ X1632)|(~(mrel @ X1632 @ X1633)|(epred34_1 @ X1633)))))))), 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.47 thf(c_0_28, plain, ![X1217:mworld, X1218:mworld]:((mrel @ X1217 @ X1218)), inference(variable_rename,[status(thm)],[mrel_universal])).
% 0.54/0.47 thf(c_0_29, plain, ![X1064:mworld]:(((epred31_1 @ X1064)=>![X1063:mworld]:(((mrel @ X1064 @ X1063)=>![X1062:mworld]:(((mrel @ X1063 @ X1062)=>![X1061:mworld]:(((mrel @ X1062 @ X1061)=>![X1060:mworld]:(((mrel @ X1061 @ X1060)=>![X1059:mworld]:(((mrel @ X1060 @ X1059)=>![X1058:mworld]:(((mrel @ X1059 @ X1058)=>![X1057:mworld]:(((mrel @ X1058 @ X1057)=>![X1056:mworld]:(((mrel @ X1057 @ X1056)=>![X1055:mworld]:(((mrel @ X1056 @ X1055)=>![X1054:mworld]:(((mrel @ X1055 @ X1054)=>((v13 @ X1054)|![X1053:mworld]:(((mrel @ X1054 @ X1053)=>![X1052:mworld]:(((mrel @ X1053 @ X1052)=>![X1051:mworld]:(((mrel @ X1052 @ X1051)=>![X1050:mworld]:(((mrel @ X1051 @ X1050)=>![X1049:mworld]:(((mrel @ X1050 @ X1049)=>![X1048:mworld]:(((mrel @ X1049 @ X1048)=>![X1047:mworld]:(((mrel @ X1048 @ X1047)=>![X1046:mworld]:(((mrel @ X1047 @ X1046)=>((v5 @ X1046)|![X1045:mworld]:(((mrel @ X1046 @ X1045)=>![X1044:mworld]:(((mrel @ X1045 @ X1044)=>((v3 @ X1044)|![X1043:mworld]:(((mrel @ X1044 @ X1043)=>(v2 @ X1043)))))))))))))))))))))))))))))))))))))))))))))))), inference(split_equiv,[status(thm)],[c_0_22])).
% 0.54/0.47 thf(c_0_30, plain, ![X1611:mworld, X1612:mworld, X1613:mworld, X1614:mworld, X1615:mworld, X1616:mworld]:((~(mrel @ mactual @ X1611)|(~(mrel @ X1611 @ X1612)|(~(mrel @ X1612 @ X1613)|(~(mrel @ X1613 @ X1614)|(~(mrel @ X1614 @ X1615)|(~(mrel @ X1615 @ X1616)|(epred31_1 @ X1616)))))))), 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.47 thf(c_0_31, plain, ![X641:mworld]:(((mrel @ mactual @ X641)=>![X640:mworld]:(((mrel @ X641 @ X640)=>![X639:mworld]:(((mrel @ X640 @ X639)=>![X638:mworld]:(((mrel @ X639 @ X638)=>(epred19_1 @ X638))))))))), 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)],[mod29, c_0_17]), c_0_18]), c_0_19]), c_0_20])]), c_0_25])).
% 0.54/0.47 thf(c_0_32, plain, ![X2440:mworld, X2441:mworld, X2442:mworld, X2443:mworld, X2444:mworld, X2445:mworld, X2446:mworld, X2447:mworld, X2448:mworld, X2449:mworld, X2450:mworld, X2451:mworld, X2452:mworld, X2453:mworld, X2454:mworld, X2455:mworld, X2456:mworld, X2457:mworld, X2458:mworld, X2459:mworld, X2460:mworld, X2461:mworld]:((~(epred34_1 @ X2440)|(~(mrel @ X2440 @ X2441)|(~(mrel @ X2441 @ X2442)|(~(mrel @ X2442 @ X2443)|(~(mrel @ X2443 @ X2444)|(~(mrel @ X2444 @ X2445)|(~(mrel @ X2445 @ X2446)|(~(mrel @ X2446 @ X2447)|(~(mrel @ X2447 @ X2448)|(~(mrel @ X2448 @ X2449)|(~(mrel @ X2449 @ X2450)|(~(mrel @ X2450 @ X2451)|(~(mrel @ X2451 @ X2452)|(~(mrel @ X2452 @ X2453)|(~(mrel @ X2453 @ X2454)|(~(mrel @ X2454 @ X2455)|(~(v8 @ X2455)|(~(mrel @ X2455 @ X2456)|(~(v7 @ X2456)|(~(mrel @ X2456 @ X2457)|(~(mrel @ X2457 @ X2458)|(~(mrel @ X2458 @ X2459)|(~(v4 @ X2459)|(~(mrel @ X2459 @ X2460)|(~(mrel @ X2460 @ X2461)|~(v2 @ X2461))))))))))))))))))))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_26])])])])).
% 0.54/0.47 thf(c_0_33, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld]:(((epred34_1 @ X9)|~((mrel @ mactual @ X3))|~((mrel @ X3 @ X5))|~((mrel @ X5 @ X6))|~((mrel @ X6 @ X7))|~((mrel @ X7 @ X8))|~((mrel @ X8 @ X9)))), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.54/0.47 thf(c_0_34, plain, ![X3:mworld, X5:mworld]:((mrel @ X3 @ X5)), inference(split_conjunct,[status(thm)],[c_0_28])).
% 0.54/0.47 thf(c_0_35, plain, ![X2374:mworld, X2375:mworld, X2376:mworld, X2377:mworld, X2378:mworld, X2379:mworld, X2380:mworld, X2381:mworld, X2382:mworld, X2383:mworld, X2384:mworld, X2385:mworld, X2386:mworld, X2387:mworld, X2388:mworld, X2389:mworld, X2390:mworld, X2391:mworld, X2392:mworld, X2393:mworld, X2394:mworld, X2395:mworld]:((~(epred31_1 @ X2374)|(~(mrel @ X2374 @ X2375)|(~(mrel @ X2375 @ X2376)|(~(mrel @ X2376 @ X2377)|(~(mrel @ X2377 @ X2378)|(~(mrel @ X2378 @ X2379)|(~(mrel @ X2379 @ X2380)|(~(mrel @ X2380 @ X2381)|(~(mrel @ X2381 @ X2382)|(~(mrel @ X2382 @ X2383)|(~(mrel @ X2383 @ X2384)|((v13 @ X2384)|(~(mrel @ X2384 @ X2385)|(~(mrel @ X2385 @ X2386)|(~(mrel @ X2386 @ X2387)|(~(mrel @ X2387 @ X2388)|(~(mrel @ X2388 @ X2389)|(~(mrel @ X2389 @ X2390)|(~(mrel @ X2390 @ X2391)|(~(mrel @ X2391 @ X2392)|((v5 @ X2392)|(~(mrel @ X2392 @ X2393)|(~(mrel @ X2393 @ X2394)|((v3 @ X2394)|(~(mrel @ X2394 @ X2395)|(v2 @ X2395))))))))))))))))))))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_29])])])])).
% 0.54/0.47 thf(c_0_36, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld]:(((epred31_1 @ X9)|~((mrel @ mactual @ X3))|~((mrel @ X3 @ X5))|~((mrel @ X5 @ X6))|~((mrel @ X6 @ X7))|~((mrel @ X7 @ X8))|~((mrel @ X8 @ X9)))), inference(split_conjunct,[status(thm)],[c_0_30])).
% 0.54/0.47 thf(c_0_37, plain, ![X638:mworld]:(((epred19_1 @ X638)=>(~(v25 @ X638)|![X637:mworld]:(((mrel @ X638 @ X637)=>![X636:mworld]:(((mrel @ X637 @ X636)=>![X635:mworld]:(((mrel @ X636 @ X635)=>![X634:mworld]:(((mrel @ X635 @ X634)=>(~(v21 @ X634)|![X633:mworld]:(((mrel @ X634 @ X633)=>![X632:mworld]:(((mrel @ X633 @ X632)=>![X631:mworld]:(((mrel @ X632 @ X631)=>![X630:mworld]:(((mrel @ X631 @ X630)=>![X629:mworld]:(((mrel @ X630 @ X629)=>![X628:mworld]:(((mrel @ X629 @ X628)=>![X627:mworld]:(((mrel @ X628 @ X627)=>![X626:mworld]:(((mrel @ X627 @ X626)=>![X625:mworld]:(((mrel @ X626 @ X625)=>![X624:mworld]:(((mrel @ X625 @ X624)=>![X623:mworld]:(((mrel @ X624 @ X623)=>![X622:mworld]:(((mrel @ X623 @ X622)=>![X621:mworld]:(((mrel @ X622 @ X621)=>![X620:mworld]:(((mrel @ X621 @ X620)=>![X619:mworld]:(((mrel @ X620 @ X619)=>(~(v6 @ X619)|![X618:mworld]:(((mrel @ X619 @ X618)=>![X617:mworld]:(((mrel @ X618 @ X617)=>(v4 @ X617)))))))))))))))))))))))))))))))))))))))))))))))), inference(split_equiv,[status(thm)],[c_0_25])).
% 0.54/0.47 thf(c_0_38, plain, ![X1438:mworld, X1439:mworld, X1440:mworld, X1441:mworld]:((~(mrel @ mactual @ X1438)|(~(mrel @ X1438 @ X1439)|(~(mrel @ X1439 @ X1440)|(~(mrel @ X1440 @ X1441)|(epred19_1 @ X1441)))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_31])])])])).
% 0.54/0.47 thf(c_0_39, plain, ((mand)=(^[Z0:mworld > $o, Z1:mworld > $o, Z2:mworld]:((((Z0 @ Z2))&((Z1 @ Z2)))))), inference(fof_simplification,[status(thm)],[mand_def])).
% 0.54/0.47 thf(c_0_40, plain, ((mdia)=(^[Z0:mworld > $o, Z1:mworld]:(?[X5:mworld]:((((mrel @ Z1 @ X5))&((Z0 @ X5))))))), inference(fof_simplification,[status(thm)],[mdia_def])).
% 0.54/0.47 thf(c_0_41, 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]:((~((epred34_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))|~((v8 @ X19))|~((mrel @ X19 @ X20))|~((v7 @ X20))|~((mrel @ X20 @ X21))|~((mrel @ X21 @ X22))|~((mrel @ X22 @ X23))|~((v4 @ X23))|~((mrel @ X23 @ X24))|~((mrel @ X24 @ X25))|~((v2 @ X25)))), inference(split_conjunct,[status(thm)],[c_0_32])).
% 0.54/0.47 thf(c_0_42, plain, ![X3:mworld]:((epred34_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)],[inference(rw,[status(thm)],[c_0_33, c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34])])).
% 0.54/0.47 thf(c_0_43, 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]:(((v13 @ X14)|(v5 @ X22)|(v3 @ X24)|(v2 @ X25)|~((epred31_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)))), inference(split_conjunct,[status(thm)],[c_0_35])).
% 0.54/0.47 thf(c_0_44, plain, ![X3:mworld]:((epred31_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)],[inference(rw,[status(thm)],[c_0_36, c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34])])).
% 0.54/0.47 thf(c_0_45, plain, ![X2109:mworld, X2110:mworld, X2111:mworld, X2112:mworld, X2113:mworld, X2114:mworld, X2115:mworld, X2116:mworld, X2117:mworld, X2118:mworld, X2119:mworld, X2120:mworld, X2121:mworld, X2122:mworld, X2123:mworld, X2124:mworld, X2125:mworld, X2126:mworld, X2127:mworld, X2128:mworld, X2129:mworld, X2130:mworld]:((~(epred19_1 @ X2109)|(~(v25 @ X2109)|(~(mrel @ X2109 @ X2110)|(~(mrel @ X2110 @ X2111)|(~(mrel @ X2111 @ X2112)|(~(mrel @ X2112 @ X2113)|(~(v21 @ X2113)|(~(mrel @ X2113 @ X2114)|(~(mrel @ X2114 @ X2115)|(~(mrel @ X2115 @ X2116)|(~(mrel @ X2116 @ X2117)|(~(mrel @ X2117 @ X2118)|(~(mrel @ X2118 @ X2119)|(~(mrel @ X2119 @ X2120)|(~(mrel @ X2120 @ X2121)|(~(mrel @ X2121 @ X2122)|(~(mrel @ X2122 @ X2123)|(~(mrel @ X2123 @ X2124)|(~(mrel @ X2124 @ X2125)|(~(mrel @ X2125 @ X2126)|(~(mrel @ X2126 @ X2127)|(~(mrel @ X2127 @ X2128)|(~(v6 @ X2128)|(~(mrel @ X2128 @ X2129)|(~(mrel @ X2129 @ X2130)|(v4 @ X2130))))))))))))))))))))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_37])])])])).
% 0.54/0.47 thf(c_0_46, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((epred19_1 @ X7)|~((mrel @ mactual @ X3))|~((mrel @ X3 @ X5))|~((mrel @ X5 @ X6))|~((mrel @ X6 @ X7)))), inference(split_conjunct,[status(thm)],[c_0_38])).
% 0.54/0.47 thf(c_0_47, 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_17]), c_0_18]), c_0_39]), c_0_20]), c_0_40])])).
% 0.54/0.47 thf(c_0_48, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:((~((v2 @ X3))|~((v4 @ X5))|~((v7 @ X6))|~((v8 @ 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_41, c_0_42]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34])])).
% 0.54/0.47 thf(c_0_49, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v13 @ X3)|(v5 @ X5)|(v3 @ X6)|(v2 @ 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_43, c_0_44]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34])])).
% 0.54/0.47 thf(c_0_50, 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]:(((v4 @ X25)|~((epred19_1 @ X3))|~((v25 @ X3))|~((mrel @ X3 @ X5))|~((mrel @ X5 @ X6))|~((mrel @ X6 @ X7))|~((mrel @ X7 @ X8))|~((v21 @ 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))|~((v6 @ X23))|~((mrel @ X23 @ X24))|~((mrel @ X24 @ X25)))), inference(split_conjunct,[status(thm)],[c_0_45])).
% 0.54/0.47 thf(c_0_51, plain, ![X3:mworld]:((epred19_1 @ X3)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_46, c_0_34]), c_0_34]), c_0_34]), c_0_34])])).
% 0.54/0.47 thf(c_0_52, 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_47])])])])])])])).
% 0.54/0.47 thf(c_0_53, 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_17]), c_0_18]), c_0_19]), c_0_20])])).
% 0.54/0.47 thf(c_0_54, 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.47 thf(c_0_55, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld]:(((v13 @ X3)|(v5 @ X5)|(v3 @ X6)|~((v4 @ X7))|~((v7 @ X8))|~((v8 @ X9)))), inference(spm,[status(thm)],[c_0_48, c_0_49])).
% 0.54/0.47 thf(c_0_56, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v4 @ X3)|~((v6 @ X5))|~((v21 @ X6))|~((v25 @ 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_50, c_0_51]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34])])).
% 0.54/0.47 thf(c_0_57, 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_52])).
% 0.54/0.47 thf(c_0_58, plain, ![X552:mworld]:(((mrel @ mactual @ X552)=>![X551:mworld]:(((mrel @ X552 @ X551)=>![X550:mworld]:(((mrel @ X551 @ X550)=>![X549:mworld]:(((mrel @ X550 @ X549)=>((v25 @ X549)|![X548:mworld]:(((mrel @ X549 @ X548)=>![X547:mworld]:(((mrel @ X548 @ X547)=>((v23 @ X547)|![X546:mworld]:(((mrel @ X547 @ X546)=>(~(v22 @ X546)|![X545:mworld]:(((mrel @ X546 @ X545)=>![X544:mworld]:(((mrel @ X545 @ X544)=>![X543:mworld]:(((mrel @ X544 @ X543)=>![X542:mworld]:(((mrel @ X543 @ X542)=>![X541:mworld]:(((mrel @ X542 @ X541)=>![X540:mworld]:(((mrel @ X541 @ X540)=>![X539:mworld]:(((mrel @ X540 @ X539)=>![X538:mworld]:(((mrel @ X539 @ X538)=>![X537:mworld]:(((mrel @ X538 @ X537)=>![X536:mworld]:(((mrel @ X537 @ X536)=>![X535:mworld]:(((mrel @ X536 @ X535)=>![X534:mworld]:(((mrel @ X535 @ X534)=>![X533:mworld]:(((mrel @ X534 @ X533)=>~(v9 @ X533)))))))))))))))))))))))))))))))))))))))))))), 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)],[mod25, c_0_17]), c_0_18]), c_0_19]), c_0_20])])).
% 0.54/0.47 thf(c_0_59, 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_53])])])])).
% 0.54/0.47 thf(c_0_60, 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_17]), c_0_18]), c_0_19]), c_0_20])]), c_0_54])).
% 0.54/0.47 thf(c_0_61, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld, X10:mworld, X11:mworld]:(((v3 @ X3)|(v5 @ X5)|(v13 @ X6)|~((v7 @ X7))|~((v8 @ X8))|~((v6 @ X9))|~((v21 @ X10))|~((v25 @ X11)))), inference(spm,[status(thm)],[c_0_55, c_0_56])).
% 0.54/0.47 thf(c_0_62, 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_57, c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34])])).
% 0.54/0.47 thf(c_0_63, plain, ![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]:(((v8 @ (esk11_20 @ X3 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 @ X21 @ X22 @ X23))|~((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_52])).
% 0.54/0.47 thf(c_0_64, plain, ![X1397:mworld, X1398:mworld, X1399:mworld, X1400:mworld, X1401:mworld, X1402:mworld, X1403:mworld, X1404:mworld, X1405:mworld, X1406:mworld, X1407:mworld, X1408:mworld, X1409:mworld, X1410:mworld, X1411:mworld, X1412:mworld, X1413:mworld, X1414:mworld, X1415:mworld, X1416:mworld]:((~(mrel @ mactual @ X1397)|(~(mrel @ X1397 @ X1398)|(~(mrel @ X1398 @ X1399)|(~(mrel @ X1399 @ X1400)|((v25 @ X1400)|(~(mrel @ X1400 @ X1401)|(~(mrel @ X1401 @ X1402)|((v23 @ X1402)|(~(mrel @ X1402 @ X1403)|(~(v22 @ X1403)|(~(mrel @ X1403 @ X1404)|(~(mrel @ X1404 @ X1405)|(~(mrel @ X1405 @ X1406)|(~(mrel @ X1406 @ X1407)|(~(mrel @ X1407 @ X1408)|(~(mrel @ X1408 @ X1409)|(~(mrel @ X1409 @ X1410)|(~(mrel @ X1410 @ X1411)|(~(mrel @ X1411 @ X1412)|(~(mrel @ X1412 @ X1413)|(~(mrel @ X1413 @ X1414)|(~(mrel @ X1414 @ X1415)|(~(mrel @ X1415 @ X1416)|~(v9 @ X1416))))))))))))))))))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_58])])])])).
% 0.54/0.47 thf(c_0_65, 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_59])).
% 0.54/0.47 thf(c_0_66, 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_52])).
% 0.54/0.47 thf(c_0_67, 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_54])).
% 0.54/0.47 thf(c_0_68, 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_60])])])])).
% 0.54/0.47 thf(c_0_69, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld, X10:mworld]:(((v13 @ X3)|(v5 @ X5)|(v3 @ X6)|~((v8 @ X7))|~((v6 @ X8))|~((v21 @ X9))|~((v25 @ X10)))), inference(spm,[status(thm)],[c_0_61, c_0_62])).
% 0.54/0.47 thf(c_0_70, 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]:((v8 @ (esk11_20 @ X3 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 @ X21 @ X22 @ X23))), 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_63, c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34])])).
% 0.54/0.47 thf(c_0_71, 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_52])).
% 0.54/0.47 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]:(((v25 @ X7)|(v23 @ X9)|~((mrel @ mactual @ X3))|~((mrel @ X3 @ X5))|~((mrel @ X5 @ X6))|~((mrel @ X6 @ X7))|~((mrel @ X7 @ X8))|~((mrel @ X8 @ X9))|~((mrel @ X9 @ X10))|~((v22 @ 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))|~((v9 @ X23)))), inference(split_conjunct,[status(thm)],[c_0_64])).
% 0.54/0.47 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_65, c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34])])).
% 0.54/0.47 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_66, c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34])])).
% 0.54/0.47 thf(c_0_75, 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_67])])])])).
% 0.54/0.47 thf(c_0_76, 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_68])).
% 0.54/0.47 thf(c_0_77, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld]:(((v3 @ X3)|(v5 @ X5)|(v13 @ X6)|~((v6 @ X7))|~((v21 @ X8))|~((v25 @ X9)))), inference(spm,[status(thm)],[c_0_69, c_0_70])).
% 0.54/0.47 thf(c_0_78, 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_71, c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34])])).
% 0.54/0.47 thf(c_0_79, 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_52])).
% 0.54/0.47 thf(c_0_80, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v25 @ X3)|(v23 @ X5)|~((v9 @ X6))|~((v22 @ 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_72, c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34])])).
% 0.54/0.47 thf(c_0_81, 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.47 thf(c_0_82, plain, ![X9:mworld, X8:mworld, X7:mworld, X6:mworld, X5:mworld, X3:mworld]:(((v22 @ (esk31_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_52])).
% 0.54/0.47 thf(c_0_83, 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_52])).
% 0.54/0.47 thf(c_0_84, 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_75])).
% 0.54/0.47 thf(c_0_85, 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_76, c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34])])).
% 0.54/0.47 thf(c_0_86, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld]:(((v13 @ X3)|(v5 @ X5)|(v3 @ X6)|~((v21 @ X7))|~((v25 @ X8)))), inference(spm,[status(thm)],[c_0_77, c_0_78])).
% 0.54/0.47 thf(c_0_87, 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_79, c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34])])).
% 0.54/0.47 thf(c_0_88, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld]:(((v14 @ X3)|(v28 @ X5)|(v25 @ X6)|(v23 @ X7)|~((v22 @ X8)))), inference(spm,[status(thm)],[c_0_80, c_0_81])).
% 0.54/0.47 thf(c_0_89, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld]:((v22 @ (esk31_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_82, c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34])])).
% 0.54/0.47 thf(c_0_90, 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_83, c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34])])).
% 0.54/0.47 thf(c_0_91, 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_84, c_0_85]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34])])).
% 0.54/0.47 thf(c_0_92, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v3 @ X3)|(v5 @ X5)|(v13 @ X6)|~((v25 @ X7)))), inference(spm,[status(thm)],[c_0_86, c_0_87])).
% 0.54/0.47 thf(c_0_93, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v23 @ X3)|(v25 @ X5)|(v28 @ X6)|(v14 @ X7))), inference(spm,[status(thm)],[c_0_88, c_0_89])).
% 0.54/0.47 thf(c_0_94, 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.47 thf(c_0_95, 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_17]), c_0_18]), c_0_19]), c_0_20])])).
% 0.54/0.47 thf(c_0_96, plain, ![X3:mworld, X5:mworld, X6:mworld]:((~((v3 @ X3))|~((v6 @ X5))|~((v9 @ X6)))), inference(spm,[status(thm)],[c_0_90, c_0_91])).
% 0.54/0.47 thf(c_0_97, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld]:(((v14 @ X3)|(v28 @ X5)|(v23 @ X6)|(v13 @ X7)|(v5 @ X8)|(v3 @ X9))), inference(spm,[status(thm)],[c_0_92, c_0_93])).
% 0.54/0.47 thf(c_0_98, 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_17]), c_0_18]), c_0_19]), c_0_20])]), c_0_94])).
% 0.54/0.47 thf(c_0_99, 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_95])])])])).
% 0.54/0.47 thf(c_0_100, 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_52])).
% 0.54/0.47 thf(c_0_101, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld]:(((v5 @ X3)|(v13 @ X5)|(v23 @ X6)|(v28 @ X7)|(v14 @ X8)|~((v6 @ X9)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_96, c_0_97]), c_0_81])).
% 0.54/0.47 thf(c_0_102, 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_94])).
% 0.54/0.47 thf(c_0_103, 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_98])])])])).
% 0.54/0.47 thf(c_0_104, 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_99])).
% 0.54/0.47 thf(c_0_105, 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_52])).
% 0.54/0.47 thf(c_0_106, 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_52])).
% 0.54/0.47 thf(c_0_107, 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_100, c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34])])).
% 0.54/0.47 thf(c_0_108, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld]:(((v14 @ X3)|(v28 @ X5)|(v23 @ X6)|(v13 @ X7)|(v5 @ X8))), inference(spm,[status(thm)],[c_0_101, c_0_78])).
% 0.54/0.47 thf(c_0_109, 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_102])])])])).
% 0.54/0.47 thf(c_0_110, plain, ![X3:mworld, X5:mworld]:(((epred16_1 @ X5)|~((mrel @ mactual @ X3))|~((mrel @ X3 @ X5)))), inference(split_conjunct,[status(thm)],[c_0_103])).
% 0.54/0.47 thf(c_0_111, 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_104, c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34])])).
% 0.54/0.47 thf(c_0_112, 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_105, c_0_34]), c_0_34]), c_0_34]), c_0_34])])).
% 0.54/0.47 thf(c_0_113, 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_106, c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34])])).
% 0.54/0.47 thf(c_0_114, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v5 @ X3)|(v13 @ X5)|(v28 @ X6)|(v14 @ X7))), inference(spm,[status(thm)],[c_0_107, c_0_108])).
% 0.54/0.47 thf(c_0_115, 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_109])).
% 0.54/0.47 thf(c_0_116, plain, ![X3:mworld]:((epred16_1 @ X3)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_110, c_0_34]), c_0_34])])).
% 0.54/0.47 thf(c_0_117, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((v22 @ X3)|(v18 @ X5)|~((v28 @ X6)))), inference(spm,[status(thm)],[c_0_111, c_0_112])).
% 0.54/0.47 thf(c_0_118, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((v28 @ X3)|(v13 @ X5)|(v5 @ X6))), inference(spm,[status(thm)],[c_0_113, c_0_114])).
% 0.54/0.47 thf(c_0_119, 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_17]), c_0_18]), c_0_19]), c_0_20])])).
% 0.54/0.47 thf(c_0_120, 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_115, c_0_116]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34])])).
% 0.54/0.47 thf(c_0_121, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v5 @ X3)|(v13 @ X5)|(v18 @ X6)|(v22 @ X7))), inference(spm,[status(thm)],[c_0_117, c_0_118])).
% 0.54/0.47 thf(c_0_122, 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_119])])])])).
% 0.54/0.47 thf(c_0_123, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld]:(((v22 @ X3)|(v13 @ X5)|(v5 @ X6)|~((v6 @ X7))|~((v7 @ X8))|~((v26 @ X9)))), inference(spm,[status(thm)],[c_0_120, c_0_121])).
% 0.54/0.47 thf(c_0_124, 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_122])).
% 0.54/0.47 thf(c_0_125, 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_52])).
% 0.54/0.47 thf(c_0_126, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld]:(((v5 @ X3)|(v13 @ X5)|(v22 @ X6)|~((v7 @ X7))|~((v26 @ X8)))), inference(spm,[status(thm)],[c_0_123, c_0_78])).
% 0.54/0.47 thf(c_0_127, 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_124, c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34])])).
% 0.54/0.47 thf(c_0_128, 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_125, c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34])])).
% 0.54/0.47 thf(c_0_129, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v22 @ X3)|(v13 @ X5)|(v5 @ X6)|~((v26 @ X7)))), inference(spm,[status(thm)],[c_0_126, c_0_62])).
% 0.54/0.47 thf(c_0_130, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((v26 @ X3)|~((v13 @ X5))|~((v28 @ X6)))), inference(spm,[status(thm)],[c_0_127, c_0_128])).
% 0.54/0.47 thf(c_0_131, 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_52])).
% 0.54/0.47 thf(c_0_132, 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_52])).
% 0.54/0.47 thf(c_0_133, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v5 @ X3)|(v13 @ X5)|(v22 @ X6)|~((v13 @ X7)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_129, c_0_130]), c_0_118])).
% 0.54/0.47 thf(c_0_134, 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_131, c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34])])).
% 0.54/0.47 thf(c_0_135, 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 @ (esk18_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_52])).
% 0.54/0.47 thf(c_0_136, 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_132, c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34])])).
% 0.54/0.47 thf(c_0_137, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((v22 @ X3)|(v13 @ X5)|(v5 @ X6))), inference(spm,[status(thm)],[c_0_133, c_0_134])).
% 0.54/0.47 thf(c_0_138, plain, ![X26:mworld, 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]:((~((v5 @ (esk6_23 @ X3 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 @ X21 @ X22 @ X23 @ X24 @ X25 @ X26)))|~((mrel @ X25 @ X26))|~((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_52])).
% 0.54/0.47 thf(c_0_139, 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 @ (esk18_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_135, c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34])])).
% 0.54/0.47 thf(c_0_140, plain, ![X3:mworld, X5:mworld]:(((v5 @ X3)|(v13 @ X5))), inference(spm,[status(thm)],[c_0_136, c_0_137])).
% 0.54/0.47 thf(c_0_141, 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]:(~((v5 @ (esk6_23 @ X3 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 @ X21 @ X22 @ X23 @ X24 @ X25 @ X26)))), 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)],[inference(rw,[status(thm)],[c_0_138, c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34]), c_0_34])])).
% 0.54/0.47 thf(c_0_142, plain, ![X3:mworld]:((v5 @ X3)), inference(spm,[status(thm)],[c_0_139, c_0_140])).
% 0.54/0.47 thf(c_0_143, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_141, c_0_142])]), ['proof']).
% 0.54/0.47 % SZS output end CNFRefutation
% 0.54/0.47 % Parsed axioms : 100
% 0.54/0.47 % Removed by relevancy pruning/SinE : 0
% 0.54/0.47 % Initial clauses : 205
% 0.54/0.47 % Removed in clause preprocessing : 56
% 0.54/0.47 % Initial clauses in saturation : 149
% 0.54/0.47 % Processed clauses : 346
% 0.54/0.47 % ...of these trivial : 39
% 0.54/0.47 % ...subsumed : 1
% 0.54/0.47 % ...remaining for further processing : 306
% 0.54/0.47 % Other redundant clauses eliminated : 0
% 0.54/0.47 % Clauses deleted for lack of memory : 0
% 0.54/0.47 % Backward-subsumed : 59
% 0.54/0.47 % Backward-rewritten : 27
% 0.54/0.47 % Generated clauses : 120
% 0.54/0.47 % ...of the previous two non-redundant : 130
% 0.54/0.47 % ...aggressively subsumed : 0
% 0.54/0.47 % Contextual simplify-reflections : 5
% 0.54/0.47 % Paramodulations : 120
% 0.54/0.47 % Factorizations : 0
% 0.54/0.47 % NegExts : 0
% 0.54/0.47 % Equation resolutions : 0
% 0.54/0.47 % Disequality decompositions : 0
% 0.54/0.47 % Total rewrite steps : 2098
% 0.54/0.47 % ...of those cached : 1974
% 0.54/0.47 % Propositional unsat checks : 0
% 0.54/0.47 % Propositional check models : 0
% 0.54/0.47 % Propositional check unsatisfiable : 0
% 0.54/0.47 % 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 : 111
% 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 : 62
% 0.54/0.47 % Current number of unprocessed clauses: 30
% 0.54/0.47 % ...number of literals in the above : 184
% 0.54/0.47 % Current number of archived formulas : 0
% 0.54/0.47 % Current number of archived clauses : 195
% 0.54/0.47 % Clause-clause subsumption calls (NU) : 3897
% 0.54/0.47 % Rec. Clause-clause subsumption calls : 1056
% 0.54/0.47 % Non-unit clause-clause subsumptions : 65
% 0.54/0.47 % Unit Clause-clause subsumption calls : 493
% 0.54/0.47 % Rewrite failures with RHS unbound : 0
% 0.54/0.47 % BW rewrite match attempts : 6
% 0.54/0.47 % BW rewrite match successes : 6
% 0.54/0.47 % Condensation attempts : 0
% 0.54/0.47 % Condensation successes : 0
% 0.54/0.47 % Termbank termtop insertions : 101107
% 0.54/0.47 % Search garbage collected termcells : 47582
% 0.54/0.47
% 0.54/0.47 % -------------------------------------------------
% 0.54/0.47 % User time : 0.137 s
% 0.54/0.47 % System time : 0.031 s
% 0.54/0.47 % Total time : 0.168 s
% 0.54/0.47 % Maximum resident set size: 11036 pages
% 0.54/0.47
% 0.54/0.47 % -------------------------------------------------
% 0.54/0.47 % User time : 0.324 s
% 0.54/0.47 % System time : 0.086 s
% 0.54/0.47 % Total time : 0.410 s
% 0.54/0.47 % Maximum resident set size: 5120 pages
% 0.54/0.47 % E exiting
%------------------------------------------------------------------------------