%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SYO905^6 : 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 : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:43:33 AM UTC 2026
% Result : ContradictoryAxioms 0.51s 0.38s
% Output : CNFRefutation 0.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO905^6 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.17 % Computer : n015.cluster.edu
% 0.06/0.17 % Model : x86_64 x86_64
% 0.06/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.17 % Memory : 8046.5625MB
% 0.06/0.17 % OS : Linux 6.8.0-71-generic
% 0.06/0.17 % CPULimit : 300
% 0.06/0.17 % WCLimit : 300
% 0.06/0.17 % DateTime : Tue Sep 29 17:30:03 UTC 2026
% 0.06/0.18 % CPUTime :
% 0.06/0.18 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.22 Running higher-order theorem proving
% 0.06/0.25 Running: /export/starexec/sandbox2/solver/bin/eprover-ho --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox2/tmp/tmp.yzbeSfFEcn/E---3.1_3844974.p
% 0.51/0.38 % Version: 3.5.1-ho
% 0.51/0.38 % Preprocessing class: HSLSSMSSMLLNHSN.
% 0.51/0.38 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.51/0.38 % Starting almost_fo_3 with 1500s (5) cores
% 0.51/0.38 % Starting sh10 with 300s (1) cores
% 0.51/0.38 % Starting new_ho_16 with 300s (1) cores
% 0.51/0.38 % Starting post_as_ho11 with 300s (1) cores
% 0.51/0.38 % new_ho_16 with pid 3844989 completed with status 9
% 0.51/0.38 % post_as_ho11 with pid 3844990 completed with status 0
% 0.51/0.38 % Result found by post_as_ho11
% 0.51/0.38 % Preprocessing class: HSLSSMSSMLLNHSN.
% 0.51/0.38 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.51/0.38 % Starting almost_fo_3 with 1500s (5) cores
% 0.51/0.38 % Starting sh10 with 300s (1) cores
% 0.51/0.38 % Starting new_ho_16 with 300s (1) cores
% 0.51/0.38 % Starting post_as_ho11 with 300s (1) cores
% 0.51/0.38 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.51/0.38 % No SInE strategy applied
% 0.51/0.38 % Search class: HGHNF-FSLF33-SHSSMFNN
% 0.51/0.38 % partial match(1): HGHNS-FSLF33-SHSSMFNN
% 0.51/0.38 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.51/0.38 % Starting SubtermCWHack with 28s (1) cores
% 0.51/0.38 % SubtermCWHack with pid 3845004 completed with status 0
% 0.51/0.38 % Result found by SubtermCWHack
% 0.51/0.38 % Preprocessing class: HSLSSMSSMLLNHSN.
% 0.51/0.38 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.51/0.38 % Starting almost_fo_3 with 1500s (5) cores
% 0.51/0.38 % Starting sh10 with 300s (1) cores
% 0.51/0.38 % Starting new_ho_16 with 300s (1) cores
% 0.51/0.38 % Starting post_as_ho11 with 300s (1) cores
% 0.51/0.38 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.51/0.38 % No SInE strategy applied
% 0.51/0.38 % Search class: HGHNF-FSLF33-SHSSMFNN
% 0.51/0.38 % partial match(1): HGHNS-FSLF33-SHSSMFNN
% 0.51/0.38 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.51/0.38 % Starting SubtermCWHack with 28s (1) cores
% 0.51/0.38 % Preprocessing time : 0.007 s
% 0.51/0.38
% 0.51/0.38 % Proof found!
% 0.51/0.38 % SZS status ContradictoryAxioms
% 0.51/0.38 % SZS output start CNFRefutation
% 0.51/0.38 thf(decl_sort1, type, mworld: $tType).
% 0.51/0.38 thf(decl_23, type, mrel: mworld > mworld > $o).
% 0.51/0.38 thf(decl_24, type, mactual: mworld).
% 0.51/0.38 thf(decl_25, type, mlocal: (mworld > $o) > $o).
% 0.51/0.38 thf(decl_26, type, mnot: (mworld > $o) > mworld > $o).
% 0.51/0.38 thf(decl_27, type, mand: (mworld > $o) > (mworld > $o) > mworld > $o).
% 0.51/0.38 thf(decl_28, type, mor: (mworld > $o) > (mworld > $o) > mworld > $o).
% 0.51/0.38 thf(decl_31, type, mbox: (mworld > $o) > mworld > $o).
% 0.51/0.38 thf(decl_32, type, mdia: (mworld > $o) > mworld > $o).
% 0.51/0.38 thf(decl_33, type, v1: mworld > $o).
% 0.51/0.38 thf(decl_35, type, v3: mworld > $o).
% 0.51/0.38 thf(decl_37, type, v5: mworld > $o).
% 0.51/0.38 thf(decl_38, type, v6: mworld > $o).
% 0.51/0.38 thf(decl_39, type, v7: mworld > $o).
% 0.51/0.38 thf(decl_40, type, v8: mworld > $o).
% 0.51/0.38 thf(decl_42, type, v10: mworld > $o).
% 0.51/0.38 thf(decl_43, type, v12: mworld > $o).
% 0.51/0.38 thf(decl_44, type, v11: mworld > $o).
% 0.51/0.38 thf(decl_45, type, v14: mworld > $o).
% 0.51/0.38 thf(decl_46, type, v13: mworld > $o).
% 0.51/0.38 thf(decl_47, type, v16: mworld > $o).
% 0.51/0.38 thf(decl_48, type, v15: mworld > $o).
% 0.51/0.38 thf(decl_51, type, v19: mworld > $o).
% 0.51/0.38 thf(decl_52, type, v21: mworld > $o).
% 0.51/0.38 thf(decl_53, type, v20: mworld > $o).
% 0.51/0.38 thf(decl_54, type, v23: mworld > $o).
% 0.51/0.38 thf(decl_55, type, v22: mworld > $o).
% 0.51/0.38 thf(decl_56, type, v25: mworld > $o).
% 0.51/0.38 thf(decl_57, type, v24: mworld > $o).
% 0.51/0.38 thf(decl_74, type, epred14_1: mworld > $o).
% 0.51/0.38 thf(decl_76, type, epred16_1: mworld > $o).
% 0.51/0.38 thf(decl_80, type, epred20_1: mworld > $o).
% 0.51/0.38 thf(decl_82, type, epred22_1: mworld > $o).
% 0.51/0.38 thf(decl_83, type, epred23_1: mworld > $o).
% 0.51/0.38 thf(decl_84, type, epred24_1: mworld > $o).
% 0.51/0.38 thf(decl_89, type, epred29_1: mworld > $o).
% 0.51/0.38 thf(decl_90, type, epred30_1: mworld > $o).
% 0.51/0.38 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.51/0.38 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.51/0.38 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.51/0.38 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.51/0.38 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.51/0.38 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.51/0.38 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.51/0.38 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.51/0.38 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.51/0.38 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.51/0.38 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.51/0.38 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.51/0.38 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.51/0.38 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.51/0.38 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.51/0.38 thf(decl_110, type, esk16_16: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.51/0.38 thf(decl_111, type, esk17_15: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.51/0.38 thf(decl_112, type, esk18_15: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.51/0.38 thf(decl_113, type, esk19_14: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.51/0.38 thf(decl_114, type, esk20_14: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.51/0.38 thf(decl_115, type, esk21_13: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.51/0.38 thf(decl_116, type, esk22_13: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.51/0.38 thf(decl_117, type, esk23_12: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.51/0.38 thf(decl_118, type, esk24_12: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.51/0.38 thf(decl_119, type, esk25_11: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.51/0.38 thf(decl_120, type, esk26_10: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.51/0.38 thf(decl_121, type, esk27_9: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.51/0.38 thf(decl_122, type, esk28_8: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.51/0.38 thf(decl_123, type, esk29_7: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.51/0.38 thf(decl_124, type, esk30_7: mworld > mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.51/0.38 thf(decl_125, type, esk31_6: mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.51/0.38 thf(decl_126, type, esk32_6: mworld > mworld > mworld > mworld > mworld > mworld > mworld).
% 0.51/0.38 thf(decl_127, type, esk33_5: mworld > mworld > mworld > mworld > mworld > mworld).
% 0.51/0.38 thf(decl_128, type, esk34_5: mworld > mworld > mworld > mworld > mworld > mworld).
% 0.51/0.38 thf(decl_129, type, esk35_4: mworld > mworld > mworld > mworld > mworld).
% 0.51/0.38 thf(decl_130, type, esk36_4: mworld > mworld > mworld > mworld > mworld).
% 0.51/0.38 thf(decl_131, type, esk37_3: mworld > mworld > mworld > mworld).
% 0.51/0.38 thf(decl_132, type, esk38_2: mworld > mworld > mworld).
% 0.51/0.38 thf(decl_133, type, esk39_1: mworld > mworld).
% 0.51/0.38 thf(decl_134, type, esk40_0: mworld).
% 0.51/0.38 thf(mlocal_def, axiom, ((mlocal)=(^[X1:mworld > $o]:((X1 @ mactual)))), file('/export/starexec/sandbox2/tmp/tmp.yzbeSfFEcn/E---3.1_3844974.p', mlocal_def)).
% 0.51/0.38 thf(mnot_def, axiom, ((mnot)=(^[X2:mworld > $o, X3:mworld]:(~((X2 @ X3))))), file('/export/starexec/sandbox2/tmp/tmp.yzbeSfFEcn/E---3.1_3844974.p', mnot_def)).
% 0.51/0.38 thf(mor_def, axiom, ((mor)=(^[X2:mworld > $o, X4:mworld > $o, X3:mworld]:((((X2 @ X3))|((X4 @ X3)))))), file('/export/starexec/sandbox2/tmp/tmp.yzbeSfFEcn/E---3.1_3844974.p', mor_def)).
% 0.51/0.38 thf(mbox_def, axiom, ((mbox)=(^[X1:mworld > $o, X3:mworld]:(![X5:mworld]:((((mrel @ X3 @ X5))=>((X1 @ X5))))))), file('/export/starexec/sandbox2/tmp/tmp.yzbeSfFEcn/E---3.1_3844974.p', mbox_def)).
% 0.51/0.38 thf(mod33, axiom, (mlocal @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v23 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v13) @ (mbox @ (mbox @ (mbox @ (mor @ v10 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ v3)))))))))))))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.yzbeSfFEcn/E---3.1_3844974.p', mod33)).
% 0.51/0.38 thf(mand_def, axiom, ((mand)=(^[X2:mworld > $o, X4:mworld > $o, X3:mworld]:((((X2 @ X3))&((X4 @ X3)))))), file('/export/starexec/sandbox2/tmp/tmp.yzbeSfFEcn/E---3.1_3844974.p', mand_def)).
% 0.51/0.38 thf(mdia_def, axiom, ((mdia)=(^[X1:mworld > $o, X3:mworld]:(?[X5:mworld]:((((mrel @ X3 @ X5))&((X1 @ X5))))))), file('/export/starexec/sandbox2/tmp/tmp.yzbeSfFEcn/E---3.1_3844974.p', mdia_def)).
% 0.51/0.38 thf(mrel_universal, axiom, ![X3:mworld, X5:mworld]:((mrel @ X3 @ X5)), file('/export/starexec/sandbox2/tmp/tmp.yzbeSfFEcn/E---3.1_3844974.p', mrel_universal)).
% 0.51/0.38 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.yzbeSfFEcn/E---3.1_3844974.p', alt1)).
% 0.51/0.38 thf(mod36, axiom, (mlocal @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v21 @ (mbox @ (mor @ v20 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v15) @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mnot @ v10)))))))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.yzbeSfFEcn/E---3.1_3844974.p', mod36)).
% 0.51/0.38 thf(mod37, axiom, (mlocal @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v21 @ (mbox @ (mor @ (mnot @ v20) @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v15 @ (mbox @ (mbox @ (mbox @ v12))))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.yzbeSfFEcn/E---3.1_3844974.p', mod37)).
% 0.51/0.38 thf(mod46, axiom, (mlocal @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v13 @ (mbox @ (mor @ v12 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v6 @ (mbox @ (mbox @ (mbox @ (mnot @ v3))))))))))))))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.yzbeSfFEcn/E---3.1_3844974.p', mod46)).
% 0.51/0.38 thf(mod34, axiom, (mlocal @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v23) @ (mbox @ (mor @ v22 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v12) @ (mbox @ (mbox @ v10))))))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.yzbeSfFEcn/E---3.1_3844974.p', mod34)).
% 0.51/0.38 thf(mod40, axiom, (mlocal @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v20) @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v14 @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v10) @ (mbox @ (mbox @ (mbox @ (mbox @ v6))))))))))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.yzbeSfFEcn/E---3.1_3844974.p', mod40)).
% 0.51/0.38 thf(mod20, axiom, (mlocal @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v25 @ (mbox @ (mor @ (mnot @ v24) @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v8 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ v1)))))))))))))))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.yzbeSfFEcn/E---3.1_3844974.p', mod20)).
% 0.51/0.38 thf(mod30, axiom, (mlocal @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v24) @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v20) @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v6) @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ v1)))))))))))))))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.yzbeSfFEcn/E---3.1_3844974.p', mod30)).
% 0.51/0.38 thf(mod22, axiom, (mlocal @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v25 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v20 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v14) @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mnot @ v8)))))))))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.yzbeSfFEcn/E---3.1_3844974.p', mod22)).
% 0.51/0.38 thf(mod18, axiom, (mlocal @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v25 @ (mbox @ (mor @ (mnot @ v24) @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v16 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ v11)))))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.yzbeSfFEcn/E---3.1_3844974.p', mod18)).
% 0.51/0.38 thf(mod19, axiom, (mlocal @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v25 @ (mbox @ (mor @ (mnot @ v24) @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v13 @ (mbox @ (mnot @ v12)))))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.yzbeSfFEcn/E---3.1_3844974.p', mod19)).
% 0.51/0.38 thf(mod45, axiom, (mlocal @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v15) @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v11) @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v7) @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mnot @ v1))))))))))))))))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.yzbeSfFEcn/E---3.1_3844974.p', mod45)).
% 0.51/0.38 thf(mod25, axiom, (mlocal @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v25) @ (mbox @ (mbox @ (mor @ v23 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v12) @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mnot @ v6)))))))))))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.yzbeSfFEcn/E---3.1_3844974.p', mod25)).
% 0.51/0.38 thf(mod24, axiom, (mlocal @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v25) @ (mbox @ (mor @ (mnot @ v24) @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ v19 @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mnot @ v8)))))))))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.yzbeSfFEcn/E---3.1_3844974.p', mod24)).
% 0.51/0.38 thf(mod35, axiom, (mlocal @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v23) @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v19) @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mbox @ (mor @ (mnot @ v6) @ (mbox @ (mbox @ (mbox @ (mnot @ v3))))))))))))))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.yzbeSfFEcn/E---3.1_3844974.p', mod35)).
% 0.51/0.38 thf(c_0_23, plain, ((mlocal)=(^[Z0:mworld > $o]:((Z0 @ mactual)))), inference(fof_simplification,[status(thm)],[mlocal_def])).
% 0.51/0.38 thf(c_0_24, plain, ((mnot)=(^[Z0:mworld > $o, Z1:mworld]:(~((Z0 @ Z1))))), inference(fof_simplification,[status(thm)],[mnot_def])).
% 0.51/0.38 thf(c_0_25, plain, ((mor)=(^[Z0:mworld > $o, Z1:mworld > $o, Z2:mworld]:((((Z0 @ Z2))|((Z1 @ Z2)))))), inference(fof_simplification,[status(thm)],[mor_def])).
% 0.51/0.38 thf(c_0_26, plain, ((mbox)=(^[Z0:mworld > $o, Z1:mworld]:(![X5:mworld]:((((mrel @ Z1 @ X5))=>((Z0 @ X5))))))), inference(fof_simplification,[status(thm)],[mbox_def])).
% 0.51/0.38 thf(c_0_27, plain, ![X775:mworld]:(((epred22_1 @ X775)<=>![X774:mworld]:(((mrel @ X775 @ X774)=>((v23 @ X774)|![X773:mworld]:(((mrel @ X774 @ X773)=>![X772:mworld]:(((mrel @ X773 @ X772)=>![X771:mworld]:(((mrel @ X772 @ X771)=>![X770:mworld]:(((mrel @ X771 @ X770)=>![X769:mworld]:(((mrel @ X770 @ X769)=>![X768:mworld]:(((mrel @ X769 @ X768)=>![X767:mworld]:(((mrel @ X768 @ X767)=>![X766:mworld]:(((mrel @ X767 @ X766)=>![X765:mworld]:(((mrel @ X766 @ X765)=>![X764:mworld]:(((mrel @ X765 @ X764)=>(~(v13 @ X764)|![X763:mworld]:(((mrel @ X764 @ X763)=>![X762:mworld]:(((mrel @ X763 @ X762)=>![X761:mworld]:(((mrel @ X762 @ X761)=>((v10 @ X761)|![X760:mworld]:(((mrel @ X761 @ X760)=>![X759:mworld]:(((mrel @ X760 @ X759)=>![X758:mworld]:(((mrel @ X759 @ X758)=>![X757:mworld]:(((mrel @ X758 @ X757)=>![X756:mworld]:(((mrel @ X757 @ X756)=>![X755:mworld]:(((mrel @ X756 @ X755)=>![X754:mworld]:(((mrel @ X755 @ X754)=>(v3 @ X754)))))))))))))))))))))))))))))))))))))))))))))))), introduced(definition)).
% 0.51/0.38 thf(c_0_28, plain, ![X779:mworld]:(((mrel @ mactual @ X779)=>![X778:mworld]:(((mrel @ X779 @ X778)=>![X777:mworld]:(((mrel @ X778 @ X777)=>![X776:mworld]:(((mrel @ X777 @ X776)=>![X775:mworld]:(((mrel @ X776 @ X775)=>(epred22_1 @ X775))))))))))), 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)],[mod33, c_0_23]), c_0_24]), c_0_25]), c_0_26])]), c_0_27])).
% 0.51/0.38 thf(c_0_29, plain, ((mand)=(^[Z0:mworld > $o, Z1:mworld > $o, Z2:mworld]:((((Z0 @ Z2))&((Z1 @ Z2)))))), inference(fof_simplification,[status(thm)],[mand_def])).
% 0.51/0.38 thf(c_0_30, plain, ((mdia)=(^[Z0:mworld > $o, Z1:mworld]:(?[X5:mworld]:((((mrel @ Z1 @ X5))&((Z0 @ X5))))))), inference(fof_simplification,[status(thm)],[mdia_def])).
% 0.51/0.38 thf(c_0_31, plain, ![X775:mworld]:(((epred22_1 @ X775)=>![X774:mworld]:(((mrel @ X775 @ X774)=>((v23 @ X774)|![X773:mworld]:(((mrel @ X774 @ X773)=>![X772:mworld]:(((mrel @ X773 @ X772)=>![X771:mworld]:(((mrel @ X772 @ X771)=>![X770:mworld]:(((mrel @ X771 @ X770)=>![X769:mworld]:(((mrel @ X770 @ X769)=>![X768:mworld]:(((mrel @ X769 @ X768)=>![X767:mworld]:(((mrel @ X768 @ X767)=>![X766:mworld]:(((mrel @ X767 @ X766)=>![X765:mworld]:(((mrel @ X766 @ X765)=>![X764:mworld]:(((mrel @ X765 @ X764)=>(~(v13 @ X764)|![X763:mworld]:(((mrel @ X764 @ X763)=>![X762:mworld]:(((mrel @ X763 @ X762)=>![X761:mworld]:(((mrel @ X762 @ X761)=>((v10 @ X761)|![X760:mworld]:(((mrel @ X761 @ X760)=>![X759:mworld]:(((mrel @ X760 @ X759)=>![X758:mworld]:(((mrel @ X759 @ X758)=>![X757:mworld]:(((mrel @ X758 @ X757)=>![X756:mworld]:(((mrel @ X757 @ X756)=>![X755:mworld]:(((mrel @ X756 @ X755)=>![X754:mworld]:(((mrel @ X755 @ X754)=>(v3 @ X754)))))))))))))))))))))))))))))))))))))))))))))))), inference(split_equiv,[status(thm)],[c_0_27])).
% 0.51/0.38 thf(c_0_32, plain, ![X1558:mworld, X1559:mworld, X1560:mworld, X1561:mworld, X1562:mworld]:((~(mrel @ mactual @ X1558)|(~(mrel @ X1558 @ X1559)|(~(mrel @ X1559 @ X1560)|(~(mrel @ X1560 @ X1561)|(~(mrel @ X1561 @ X1562)|(epred22_1 @ X1562))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_28])])])])).
% 0.51/0.38 thf(c_0_33, plain, ![X1265:mworld, X1266:mworld]:((mrel @ X1265 @ X1266)), inference(variable_rename,[status(thm)],[mrel_universal])).
% 0.51/0.38 thf(c_0_34, plain, (![X1263:mworld]:(((mrel @ mactual @ X1263)=>(![X1261:mworld]:(((mrel @ X1263 @ X1261)=>(![X1259:mworld]:(((mrel @ X1261 @ X1259)=>(![X1257:mworld]:(((mrel @ X1259 @ X1257)=>(![X1254:mworld]:(((mrel @ X1257 @ X1254)=>(![X1251:mworld]:(((mrel @ X1254 @ X1251)=>(![X1248:mworld]:(((mrel @ X1251 @ X1248)=>(![X1245:mworld]:(((mrel @ X1248 @ X1245)=>(![X1243:mworld]:(((mrel @ X1245 @ X1243)=>(![X1241:mworld]:(((mrel @ X1243 @ X1241)=>(![X1239:mworld]:(((mrel @ X1241 @ X1239)=>(![X1237:mworld]:(((mrel @ X1239 @ X1237)=>(![X1234:mworld]:(((mrel @ X1237 @ X1234)=>(![X1231:mworld]:(((mrel @ X1234 @ X1231)=>(![X1228:mworld]:(((mrel @ X1231 @ X1228)=>(![X1225:mworld]:(((mrel @ X1228 @ X1225)=>(![X1223:mworld]:(((mrel @ X1225 @ X1223)=>(![X1221:mworld]:(((mrel @ X1223 @ X1221)=>(![X1219:mworld]:(((mrel @ X1221 @ X1219)=>(![X1217:mworld]:(((mrel @ X1219 @ X1217)=>(![X1214:mworld]:(((mrel @ X1217 @ X1214)=>(![X1211:mworld]:(((mrel @ X1214 @ X1211)=>(![X1208:mworld]:(((mrel @ X1211 @ X1208)=>(![X1205:mworld]:(((mrel @ X1208 @ X1205)=>(![X1203:mworld]:(((mrel @ X1205 @ X1203)=>(![X1201:mworld]:(((mrel @ X1203 @ X1201)=>(![X1199:mworld]:(((mrel @ X1201 @ X1199)=>?[X1198:mworld]:(((mrel @ X1199 @ X1198)&$true))))&?[X1200:mworld]:(((mrel @ X1201 @ X1200)&$true)))))&?[X1202:mworld]:(((mrel @ X1203 @ X1202)&$true)))))&?[X1204:mworld]:(((mrel @ X1205 @ X1204)&$true)))))&(?[X1206:mworld]:(((mrel @ X1208 @ X1206)&(v5 @ X1206)))&?[X1207:mworld]:(((mrel @ X1208 @ X1207)&~(v5 @ X1207)))))))&(?[X1209:mworld]:(((mrel @ X1211 @ X1209)&(v6 @ X1209)))&?[X1210:mworld]:(((mrel @ X1211 @ X1210)&~(v6 @ X1210)))))))&(?[X1212:mworld]:(((mrel @ X1214 @ X1212)&(v7 @ X1212)))&?[X1213:mworld]:(((mrel @ X1214 @ X1213)&~(v7 @ X1213)))))))&(?[X1215:mworld]:(((mrel @ X1217 @ X1215)&(v8 @ X1215)))&?[X1216:mworld]:(((mrel @ X1217 @ X1216)&~(v8 @ X1216)))))))&?[X1218:mworld]:(((mrel @ X1219 @ X1218)&$true)))))&?[X1220:mworld]:(((mrel @ X1221 @ X1220)&$true)))))&?[X1222:mworld]:(((mrel @ X1223 @ X1222)&$true)))))&?[X1224:mworld]:(((mrel @ X1225 @ X1224)&$true)))))&(?[X1226:mworld]:(((mrel @ X1228 @ X1226)&(v13 @ X1226)))&?[X1227:mworld]:(((mrel @ X1228 @ X1227)&~(v13 @ X1227)))))))&(?[X1229:mworld]:(((mrel @ X1231 @ X1229)&(v14 @ X1229)))&?[X1230:mworld]:(((mrel @ X1231 @ X1230)&~(v14 @ X1230)))))))&(?[X1232:mworld]:(((mrel @ X1234 @ X1232)&(v15 @ X1232)))&?[X1233:mworld]:(((mrel @ X1234 @ X1233)&~(v15 @ X1233)))))))&(?[X1235:mworld]:(((mrel @ X1237 @ X1235)&(v16 @ X1235)))&?[X1236:mworld]:(((mrel @ X1237 @ X1236)&~(v16 @ X1236)))))))&?[X1238:mworld]:(((mrel @ X1239 @ X1238)&$true)))))&?[X1240:mworld]:(((mrel @ X1241 @ X1240)&$true)))))&?[X1242:mworld]:(((mrel @ X1243 @ X1242)&$true)))))&?[X1244:mworld]:(((mrel @ X1245 @ X1244)&$true)))))&(?[X1246:mworld]:(((mrel @ X1248 @ X1246)&(v21 @ X1246)))&?[X1247:mworld]:(((mrel @ X1248 @ X1247)&~(v21 @ X1247)))))))&(?[X1249:mworld]:(((mrel @ X1251 @ X1249)&(v22 @ X1249)))&?[X1250:mworld]:(((mrel @ X1251 @ X1250)&~(v22 @ X1250)))))))&(?[X1252:mworld]:(((mrel @ X1254 @ X1252)&(v23 @ X1252)))&?[X1253:mworld]:(((mrel @ X1254 @ X1253)&~(v23 @ X1253)))))))&(?[X1255:mworld]:(((mrel @ X1257 @ X1255)&(v24 @ X1255)))&?[X1256:mworld]:(((mrel @ X1257 @ X1256)&~(v24 @ X1256)))))))&?[X1258:mworld]:(((mrel @ X1259 @ X1258)&$true)))))&?[X1260:mworld]:(((mrel @ X1261 @ X1260)&$true)))))&?[X1262:mworld]:(((mrel @ X1263 @ X1262)&$true)))))&?[X1264:mworld]:(((mrel @ mactual @ X1264)&$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_23]), c_0_24]), c_0_29]), c_0_26]), c_0_30])])).
% 0.51/0.38 thf(c_0_35, plain, ![X2272:mworld, X2273:mworld, X2274:mworld, X2275:mworld, X2276:mworld, X2277:mworld, X2278:mworld, X2279:mworld, X2280:mworld, X2281:mworld, X2282:mworld, X2283:mworld, X2284:mworld, X2285:mworld, X2286:mworld, X2287:mworld, X2288:mworld, X2289:mworld, X2290:mworld, X2291:mworld, X2292:mworld, X2293:mworld]:((~(epred22_1 @ X2272)|(~(mrel @ X2272 @ X2273)|((v23 @ X2273)|(~(mrel @ X2273 @ X2274)|(~(mrel @ X2274 @ X2275)|(~(mrel @ X2275 @ X2276)|(~(mrel @ X2276 @ X2277)|(~(mrel @ X2277 @ X2278)|(~(mrel @ X2278 @ X2279)|(~(mrel @ X2279 @ X2280)|(~(mrel @ X2280 @ X2281)|(~(mrel @ X2281 @ X2282)|(~(mrel @ X2282 @ X2283)|(~(v13 @ X2283)|(~(mrel @ X2283 @ X2284)|(~(mrel @ X2284 @ X2285)|(~(mrel @ X2285 @ X2286)|((v10 @ X2286)|(~(mrel @ X2286 @ X2287)|(~(mrel @ X2287 @ X2288)|(~(mrel @ X2288 @ X2289)|(~(mrel @ X2289 @ X2290)|(~(mrel @ X2290 @ X2291)|(~(mrel @ X2291 @ X2292)|(~(mrel @ X2292 @ X2293)|(v3 @ X2293))))))))))))))))))))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_31])])])])).
% 0.51/0.38 thf(c_0_36, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld]:(((epred22_1 @ X8)|~((mrel @ mactual @ X3))|~((mrel @ X3 @ X5))|~((mrel @ X5 @ X6))|~((mrel @ X6 @ X7))|~((mrel @ X7 @ X8)))), inference(split_conjunct,[status(thm)],[c_0_32])).
% 0.51/0.38 thf(c_0_37, plain, ![X3:mworld, X5:mworld]:((mrel @ X3 @ X5)), inference(split_conjunct,[status(thm)],[c_0_33])).
% 0.51/0.38 thf(c_0_38, plain, ![X1729:mworld, X1730:mworld, X1731:mworld, X1732:mworld, X1733:mworld, X1734:mworld, X1735:mworld, X1736:mworld, X1737:mworld, X1738:mworld, X1739:mworld, X1740:mworld, X1741:mworld, X1742:mworld, X1743:mworld, X1744:mworld, X1745:mworld, X1746:mworld, X1747:mworld, X1748:mworld, X1749:mworld, X1750:mworld, X1751:mworld, X1752:mworld, X1753:mworld, X1754:mworld, X1755:mworld]:(((((((((((((((((((((((((((((((mrel @ X1755 @ (esk1_27 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742 @ X1743 @ X1744 @ X1745 @ X1746 @ X1747 @ X1748 @ X1749 @ X1750 @ X1751 @ X1752 @ X1753 @ X1754 @ X1755))|~(mrel @ X1754 @ X1755)|~(mrel @ X1753 @ X1754)|~(mrel @ X1752 @ X1753)|~(mrel @ X1751 @ X1752)|~(mrel @ X1750 @ X1751)|~(mrel @ X1749 @ X1750)|~(mrel @ X1748 @ X1749)|~(mrel @ X1747 @ X1748)|~(mrel @ X1746 @ X1747)|~(mrel @ X1745 @ X1746)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&(($true)|~(mrel @ X1754 @ X1755)|~(mrel @ X1753 @ X1754)|~(mrel @ X1752 @ X1753)|~(mrel @ X1751 @ X1752)|~(mrel @ X1750 @ X1751)|~(mrel @ X1749 @ X1750)|~(mrel @ X1748 @ X1749)|~(mrel @ X1747 @ X1748)|~(mrel @ X1746 @ X1747)|~(mrel @ X1745 @ X1746)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729)))&(((mrel @ X1754 @ (esk2_26 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742 @ X1743 @ X1744 @ X1745 @ X1746 @ X1747 @ X1748 @ X1749 @ X1750 @ X1751 @ X1752 @ X1753 @ X1754))|~(mrel @ X1753 @ X1754)|~(mrel @ X1752 @ X1753)|~(mrel @ X1751 @ X1752)|~(mrel @ X1750 @ X1751)|~(mrel @ X1749 @ X1750)|~(mrel @ X1748 @ X1749)|~(mrel @ X1747 @ X1748)|~(mrel @ X1746 @ X1747)|~(mrel @ X1745 @ X1746)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&(($true)|~(mrel @ X1753 @ X1754)|~(mrel @ X1752 @ X1753)|~(mrel @ X1751 @ X1752)|~(mrel @ X1750 @ X1751)|~(mrel @ X1749 @ X1750)|~(mrel @ X1748 @ X1749)|~(mrel @ X1747 @ X1748)|~(mrel @ X1746 @ X1747)|~(mrel @ X1745 @ X1746)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))))&(((mrel @ X1753 @ (esk3_25 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742 @ X1743 @ X1744 @ X1745 @ X1746 @ X1747 @ X1748 @ X1749 @ X1750 @ X1751 @ X1752 @ X1753))|~(mrel @ X1752 @ X1753)|~(mrel @ X1751 @ X1752)|~(mrel @ X1750 @ X1751)|~(mrel @ X1749 @ X1750)|~(mrel @ X1748 @ X1749)|~(mrel @ X1747 @ X1748)|~(mrel @ X1746 @ X1747)|~(mrel @ X1745 @ X1746)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&(($true)|~(mrel @ X1752 @ X1753)|~(mrel @ X1751 @ X1752)|~(mrel @ X1750 @ X1751)|~(mrel @ X1749 @ X1750)|~(mrel @ X1748 @ X1749)|~(mrel @ X1747 @ X1748)|~(mrel @ X1746 @ X1747)|~(mrel @ X1745 @ X1746)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))))&(((mrel @ X1752 @ (esk4_24 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742 @ X1743 @ X1744 @ X1745 @ X1746 @ X1747 @ X1748 @ X1749 @ X1750 @ X1751 @ X1752))|~(mrel @ X1751 @ X1752)|~(mrel @ X1750 @ X1751)|~(mrel @ X1749 @ X1750)|~(mrel @ X1748 @ X1749)|~(mrel @ X1747 @ X1748)|~(mrel @ X1746 @ X1747)|~(mrel @ X1745 @ X1746)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&(($true)|~(mrel @ X1751 @ X1752)|~(mrel @ X1750 @ X1751)|~(mrel @ X1749 @ X1750)|~(mrel @ X1748 @ X1749)|~(mrel @ X1747 @ X1748)|~(mrel @ X1746 @ X1747)|~(mrel @ X1745 @ X1746)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))))&((((mrel @ X1751 @ (esk5_23 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742 @ X1743 @ X1744 @ X1745 @ X1746 @ X1747 @ X1748 @ X1749 @ X1750 @ X1751))|~(mrel @ X1750 @ X1751)|~(mrel @ X1749 @ X1750)|~(mrel @ X1748 @ X1749)|~(mrel @ X1747 @ X1748)|~(mrel @ X1746 @ X1747)|~(mrel @ X1745 @ X1746)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&((v5 @ (esk5_23 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742 @ X1743 @ X1744 @ X1745 @ X1746 @ X1747 @ X1748 @ X1749 @ X1750 @ X1751))|~(mrel @ X1750 @ X1751)|~(mrel @ X1749 @ X1750)|~(mrel @ X1748 @ X1749)|~(mrel @ X1747 @ X1748)|~(mrel @ X1746 @ X1747)|~(mrel @ X1745 @ X1746)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729)))&(((mrel @ X1751 @ (esk6_23 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742 @ X1743 @ X1744 @ X1745 @ X1746 @ X1747 @ X1748 @ X1749 @ X1750 @ X1751))|~(mrel @ X1750 @ X1751)|~(mrel @ X1749 @ X1750)|~(mrel @ X1748 @ X1749)|~(mrel @ X1747 @ X1748)|~(mrel @ X1746 @ X1747)|~(mrel @ X1745 @ X1746)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&(~(v5 @ (esk6_23 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742 @ X1743 @ X1744 @ X1745 @ X1746 @ X1747 @ X1748 @ X1749 @ X1750 @ X1751))|~(mrel @ X1750 @ X1751)|~(mrel @ X1749 @ X1750)|~(mrel @ X1748 @ X1749)|~(mrel @ X1747 @ X1748)|~(mrel @ X1746 @ X1747)|~(mrel @ X1745 @ X1746)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729)))))&((((mrel @ X1750 @ (esk7_22 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742 @ X1743 @ X1744 @ X1745 @ X1746 @ X1747 @ X1748 @ X1749 @ X1750))|~(mrel @ X1749 @ X1750)|~(mrel @ X1748 @ X1749)|~(mrel @ X1747 @ X1748)|~(mrel @ X1746 @ X1747)|~(mrel @ X1745 @ X1746)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&((v6 @ (esk7_22 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742 @ X1743 @ X1744 @ X1745 @ X1746 @ X1747 @ X1748 @ X1749 @ X1750))|~(mrel @ X1749 @ X1750)|~(mrel @ X1748 @ X1749)|~(mrel @ X1747 @ X1748)|~(mrel @ X1746 @ X1747)|~(mrel @ X1745 @ X1746)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729)))&(((mrel @ X1750 @ (esk8_22 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742 @ X1743 @ X1744 @ X1745 @ X1746 @ X1747 @ X1748 @ X1749 @ X1750))|~(mrel @ X1749 @ X1750)|~(mrel @ X1748 @ X1749)|~(mrel @ X1747 @ X1748)|~(mrel @ X1746 @ X1747)|~(mrel @ X1745 @ X1746)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&(~(v6 @ (esk8_22 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742 @ X1743 @ X1744 @ X1745 @ X1746 @ X1747 @ X1748 @ X1749 @ X1750))|~(mrel @ X1749 @ X1750)|~(mrel @ X1748 @ X1749)|~(mrel @ X1747 @ X1748)|~(mrel @ X1746 @ X1747)|~(mrel @ X1745 @ X1746)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729)))))&((((mrel @ X1749 @ (esk9_21 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742 @ X1743 @ X1744 @ X1745 @ X1746 @ X1747 @ X1748 @ X1749))|~(mrel @ X1748 @ X1749)|~(mrel @ X1747 @ X1748)|~(mrel @ X1746 @ X1747)|~(mrel @ X1745 @ X1746)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&((v7 @ (esk9_21 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742 @ X1743 @ X1744 @ X1745 @ X1746 @ X1747 @ X1748 @ X1749))|~(mrel @ X1748 @ X1749)|~(mrel @ X1747 @ X1748)|~(mrel @ X1746 @ X1747)|~(mrel @ X1745 @ X1746)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729)))&(((mrel @ X1749 @ (esk10_21 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742 @ X1743 @ X1744 @ X1745 @ X1746 @ X1747 @ X1748 @ X1749))|~(mrel @ X1748 @ X1749)|~(mrel @ X1747 @ X1748)|~(mrel @ X1746 @ X1747)|~(mrel @ X1745 @ X1746)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&(~(v7 @ (esk10_21 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742 @ X1743 @ X1744 @ X1745 @ X1746 @ X1747 @ X1748 @ X1749))|~(mrel @ X1748 @ X1749)|~(mrel @ X1747 @ X1748)|~(mrel @ X1746 @ X1747)|~(mrel @ X1745 @ X1746)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729)))))&((((mrel @ X1748 @ (esk11_20 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742 @ X1743 @ X1744 @ X1745 @ X1746 @ X1747 @ X1748))|~(mrel @ X1747 @ X1748)|~(mrel @ X1746 @ X1747)|~(mrel @ X1745 @ X1746)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&((v8 @ (esk11_20 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742 @ X1743 @ X1744 @ X1745 @ X1746 @ X1747 @ X1748))|~(mrel @ X1747 @ X1748)|~(mrel @ X1746 @ X1747)|~(mrel @ X1745 @ X1746)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729)))&(((mrel @ X1748 @ (esk12_20 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742 @ X1743 @ X1744 @ X1745 @ X1746 @ X1747 @ X1748))|~(mrel @ X1747 @ X1748)|~(mrel @ X1746 @ X1747)|~(mrel @ X1745 @ X1746)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&(~(v8 @ (esk12_20 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742 @ X1743 @ X1744 @ X1745 @ X1746 @ X1747 @ X1748))|~(mrel @ X1747 @ X1748)|~(mrel @ X1746 @ X1747)|~(mrel @ X1745 @ X1746)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729)))))&(((mrel @ X1747 @ (esk13_19 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742 @ X1743 @ X1744 @ X1745 @ X1746 @ X1747))|~(mrel @ X1746 @ X1747)|~(mrel @ X1745 @ X1746)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&(($true)|~(mrel @ X1746 @ X1747)|~(mrel @ X1745 @ X1746)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))))&(((mrel @ X1746 @ (esk14_18 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742 @ X1743 @ X1744 @ X1745 @ X1746))|~(mrel @ X1745 @ X1746)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&(($true)|~(mrel @ X1745 @ X1746)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))))&(((mrel @ X1745 @ (esk15_17 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742 @ X1743 @ X1744 @ X1745))|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&(($true)|~(mrel @ X1744 @ X1745)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))))&(((mrel @ X1744 @ (esk16_16 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742 @ X1743 @ X1744))|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&(($true)|~(mrel @ X1743 @ X1744)|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))))&((((mrel @ X1743 @ (esk17_15 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742 @ X1743))|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&((v13 @ (esk17_15 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742 @ X1743))|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729)))&(((mrel @ X1743 @ (esk18_15 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742 @ X1743))|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&(~(v13 @ (esk18_15 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742 @ X1743))|~(mrel @ X1742 @ X1743)|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729)))))&((((mrel @ X1742 @ (esk19_14 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742))|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&((v14 @ (esk19_14 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742))|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729)))&(((mrel @ X1742 @ (esk20_14 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742))|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&(~(v14 @ (esk20_14 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741 @ X1742))|~(mrel @ X1741 @ X1742)|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729)))))&((((mrel @ X1741 @ (esk21_13 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741))|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&((v15 @ (esk21_13 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741))|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729)))&(((mrel @ X1741 @ (esk22_13 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741))|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&(~(v15 @ (esk22_13 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740 @ X1741))|~(mrel @ X1740 @ X1741)|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729)))))&((((mrel @ X1740 @ (esk23_12 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740))|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&((v16 @ (esk23_12 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740))|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729)))&(((mrel @ X1740 @ (esk24_12 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740))|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&(~(v16 @ (esk24_12 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739 @ X1740))|~(mrel @ X1739 @ X1740)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729)))))&(((mrel @ X1739 @ (esk25_11 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738 @ X1739))|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&(($true)|~(mrel @ X1738 @ X1739)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))))&(((mrel @ X1738 @ (esk26_10 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737 @ X1738))|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&(($true)|~(mrel @ X1737 @ X1738)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))))&(((mrel @ X1737 @ (esk27_9 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736 @ X1737))|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&(($true)|~(mrel @ X1736 @ X1737)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))))&(((mrel @ X1736 @ (esk28_8 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735 @ X1736))|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&(($true)|~(mrel @ X1735 @ X1736)|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))))&((((mrel @ X1735 @ (esk29_7 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735))|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&((v21 @ (esk29_7 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735))|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729)))&(((mrel @ X1735 @ (esk30_7 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735))|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&(~(v21 @ (esk30_7 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734 @ X1735))|~(mrel @ X1734 @ X1735)|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729)))))&((((mrel @ X1734 @ (esk31_6 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734))|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&((v22 @ (esk31_6 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734))|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729)))&(((mrel @ X1734 @ (esk32_6 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734))|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&(~(v22 @ (esk32_6 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733 @ X1734))|~(mrel @ X1733 @ X1734)|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729)))))&((((mrel @ X1733 @ (esk33_5 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733))|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&((v23 @ (esk33_5 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733))|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729)))&(((mrel @ X1733 @ (esk34_5 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733))|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&(~(v23 @ (esk34_5 @ X1729 @ X1730 @ X1731 @ X1732 @ X1733))|~(mrel @ X1732 @ X1733)|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729)))))&((((mrel @ X1732 @ (esk35_4 @ X1729 @ X1730 @ X1731 @ X1732))|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&((v24 @ (esk35_4 @ X1729 @ X1730 @ X1731 @ X1732))|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729)))&(((mrel @ X1732 @ (esk36_4 @ X1729 @ X1730 @ X1731 @ X1732))|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&(~(v24 @ (esk36_4 @ X1729 @ X1730 @ X1731 @ X1732))|~(mrel @ X1731 @ X1732)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729)))))&(((mrel @ X1731 @ (esk37_3 @ X1729 @ X1730 @ X1731))|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&(($true)|~(mrel @ X1730 @ X1731)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))))&(((mrel @ X1730 @ (esk38_2 @ X1729 @ X1730))|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))&(($true)|~(mrel @ X1729 @ X1730)|~(mrel @ mactual @ X1729))))&(((mrel @ X1729 @ (esk39_1 @ X1729))|~(mrel @ mactual @ X1729))&(($true)|~(mrel @ mactual @ X1729))))&((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_34])])])])])])])).
% 0.51/0.38 thf(c_0_39, plain, ![X843:mworld]:(((mrel @ mactual @ X843)=>![X842:mworld]:(((mrel @ X843 @ X842)=>![X841:mworld]:(((mrel @ X842 @ X841)=>![X840:mworld]:(((mrel @ X841 @ X840)=>![X839:mworld]:(((mrel @ X840 @ X839)=>![X838:mworld]:(((mrel @ X839 @ X838)=>![X837:mworld]:(((mrel @ X838 @ X837)=>![X836:mworld]:(((mrel @ X837 @ X836)=>((v21 @ X836)|![X835:mworld]:(((mrel @ X836 @ X835)=>((v20 @ X835)|![X834:mworld]:(((mrel @ X835 @ X834)=>![X833:mworld]:(((mrel @ X834 @ X833)=>![X832:mworld]:(((mrel @ X833 @ X832)=>![X831:mworld]:(((mrel @ X832 @ X831)=>![X830:mworld]:(((mrel @ X831 @ X830)=>(~(v15 @ X830)|![X829:mworld]:(((mrel @ X830 @ X829)=>![X828:mworld]:(((mrel @ X829 @ X828)=>![X827:mworld]:(((mrel @ X828 @ X827)=>![X826:mworld]:(((mrel @ X827 @ X826)=>![X825:mworld]:(((mrel @ X826 @ X825)=>~(v10 @ X825)))))))))))))))))))))))))))))))))))))))))), 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)],[mod36, c_0_23]), c_0_24]), c_0_25]), c_0_26])])).
% 0.51/0.38 thf(c_0_40, 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]:(((v23 @ X5)|(v10 @ X18)|(v3 @ X25)|~((epred22_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))|~((v13 @ 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.51/0.38 thf(c_0_41, plain, ![X3:mworld]:((epred22_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_36, c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_42, 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_38])).
% 0.51/0.38 thf(c_0_43, plain, ![X1587:mworld, X1588:mworld, X1589:mworld, X1590:mworld, X1591:mworld, X1592:mworld, X1593:mworld, X1594:mworld, X1595:mworld, X1596:mworld, X1597:mworld, X1598:mworld, X1599:mworld, X1600:mworld, X1601:mworld, X1602:mworld, X1603:mworld, X1604:mworld, X1605:mworld]:((~(mrel @ mactual @ X1587)|(~(mrel @ X1587 @ X1588)|(~(mrel @ X1588 @ X1589)|(~(mrel @ X1589 @ X1590)|(~(mrel @ X1590 @ X1591)|(~(mrel @ X1591 @ X1592)|(~(mrel @ X1592 @ X1593)|(~(mrel @ X1593 @ X1594)|((v21 @ X1594)|(~(mrel @ X1594 @ X1595)|((v20 @ X1595)|(~(mrel @ X1595 @ X1596)|(~(mrel @ X1596 @ X1597)|(~(mrel @ X1597 @ X1598)|(~(mrel @ X1598 @ X1599)|(~(mrel @ X1599 @ X1600)|(~(v15 @ X1600)|(~(mrel @ X1600 @ X1601)|(~(mrel @ X1601 @ X1602)|(~(mrel @ X1602 @ X1603)|(~(mrel @ X1603 @ X1604)|(~(mrel @ X1604 @ X1605)|~(v10 @ X1605)))))))))))))))))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_39])])])])).
% 0.51/0.38 thf(c_0_44, 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_38])).
% 0.51/0.38 thf(c_0_45, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v23 @ X3)|(v10 @ X5)|(v3 @ X6)|~((v13 @ 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_40, c_0_41]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_46, 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_42, c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_47, 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]:(((v21 @ X11)|(v20 @ X12)|~((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))|~((v10 @ X22)))), inference(split_conjunct,[status(thm)],[c_0_43])).
% 0.51/0.38 thf(c_0_48, 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_44, c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_49, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((v3 @ X3)|(v10 @ X5)|(v23 @ X6))), inference(spm,[status(thm)],[c_0_45, c_0_46])).
% 0.51/0.38 thf(c_0_50, plain, ![X860:mworld]:(((mrel @ mactual @ X860)=>![X859:mworld]:(((mrel @ X860 @ X859)=>![X858:mworld]:(((mrel @ X859 @ X858)=>![X857:mworld]:(((mrel @ X858 @ X857)=>![X856:mworld]:(((mrel @ X857 @ X856)=>![X855:mworld]:(((mrel @ X856 @ X855)=>![X854:mworld]:(((mrel @ X855 @ X854)=>![X853:mworld]:(((mrel @ X854 @ X853)=>((v21 @ X853)|![X852:mworld]:(((mrel @ X853 @ X852)=>(~(v20 @ X852)|![X851:mworld]:(((mrel @ X852 @ X851)=>![X850:mworld]:(((mrel @ X851 @ X850)=>![X849:mworld]:(((mrel @ X850 @ X849)=>![X848:mworld]:(((mrel @ X849 @ X848)=>![X847:mworld]:(((mrel @ X848 @ X847)=>((v15 @ X847)|![X846:mworld]:(((mrel @ X847 @ X846)=>![X845:mworld]:(((mrel @ X846 @ X845)=>![X844:mworld]:(((mrel @ X845 @ X844)=>(v12 @ X844)))))))))))))))))))))))))))))))))))))), 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)],[mod37, c_0_23]), c_0_24]), c_0_25]), c_0_26])])).
% 0.51/0.38 thf(c_0_51, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v20 @ X3)|(v21 @ X5)|~((v10 @ 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)],[c_0_47, c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_52, plain, ![X3:mworld, X5:mworld]:(((v10 @ X3)|(v3 @ X5))), inference(spm,[status(thm)],[c_0_48, c_0_49])).
% 0.51/0.38 thf(c_0_53, 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_38])).
% 0.51/0.38 thf(c_0_54, plain, ![X1081:mworld]:(((epred30_1 @ X1081)<=>![X1080:mworld]:(((mrel @ X1081 @ X1080)=>![X1079:mworld]:(((mrel @ X1080 @ X1079)=>![X1078:mworld]:(((mrel @ X1079 @ X1078)=>![X1077:mworld]:(((mrel @ X1078 @ X1077)=>![X1076:mworld]:(((mrel @ X1077 @ X1076)=>![X1075:mworld]:(((mrel @ X1076 @ X1075)=>![X1074:mworld]:(((mrel @ X1075 @ X1074)=>![X1073:mworld]:(((mrel @ X1074 @ X1073)=>![X1072:mworld]:(((mrel @ X1073 @ X1072)=>![X1071:mworld]:(((mrel @ X1072 @ X1071)=>![X1070:mworld]:(((mrel @ X1071 @ X1070)=>((v13 @ X1070)|![X1069:mworld]:(((mrel @ X1070 @ X1069)=>((v12 @ 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)=>![X1063:mworld]:(((mrel @ X1064 @ X1063)=>((v6 @ X1063)|![X1062:mworld]:(((mrel @ X1063 @ X1062)=>![X1061:mworld]:(((mrel @ X1062 @ X1061)=>![X1060:mworld]:(((mrel @ X1061 @ X1060)=>~(v3 @ X1060)))))))))))))))))))))))))))))))))))))))))))))))), introduced(definition)).
% 0.51/0.38 thf(c_0_55, plain, ![X1606:mworld, X1607:mworld, X1608:mworld, X1609:mworld, X1610:mworld, X1611:mworld, X1612:mworld, X1613:mworld, X1614:mworld, X1615:mworld, X1616:mworld, X1617:mworld, X1618:mworld, X1619:mworld, X1620:mworld, X1621:mworld, X1622:mworld]:((~(mrel @ mactual @ X1606)|(~(mrel @ X1606 @ X1607)|(~(mrel @ X1607 @ X1608)|(~(mrel @ X1608 @ X1609)|(~(mrel @ X1609 @ X1610)|(~(mrel @ X1610 @ X1611)|(~(mrel @ X1611 @ X1612)|(~(mrel @ X1612 @ X1613)|((v21 @ X1613)|(~(mrel @ X1613 @ X1614)|(~(v20 @ X1614)|(~(mrel @ X1614 @ X1615)|(~(mrel @ X1615 @ X1616)|(~(mrel @ X1616 @ X1617)|(~(mrel @ X1617 @ X1618)|(~(mrel @ X1618 @ X1619)|((v15 @ X1619)|(~(mrel @ X1619 @ X1620)|(~(mrel @ X1620 @ X1621)|(~(mrel @ X1621 @ X1622)|(v12 @ X1622)))))))))))))))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_50])])])])).
% 0.51/0.38 thf(c_0_56, plain, ![X10:mworld, X9:mworld, X8:mworld, X7:mworld, X6:mworld, X5:mworld, X3:mworld]:((~((v21 @ (esk30_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_38])).
% 0.51/0.38 thf(c_0_57, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v3 @ X3)|(v21 @ X5)|(v20 @ X6)|~((v15 @ X7)))), inference(spm,[status(thm)],[c_0_51, c_0_52])).
% 0.51/0.38 thf(c_0_58, 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_53, c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_59, plain, ![X1085:mworld]:(((mrel @ mactual @ X1085)=>![X1084:mworld]:(((mrel @ X1085 @ X1084)=>![X1083:mworld]:(((mrel @ X1084 @ X1083)=>![X1082:mworld]:(((mrel @ X1083 @ X1082)=>![X1081:mworld]:(((mrel @ X1082 @ X1081)=>(epred30_1 @ X1081))))))))))), 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)],[mod46, c_0_23]), c_0_24]), c_0_25]), c_0_26])]), c_0_54])).
% 0.51/0.38 thf(c_0_60, 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]:(((v21 @ X11)|(v15 @ X17)|(v12 @ X20)|~((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))|~((v20 @ 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)))), inference(split_conjunct,[status(thm)],[c_0_55])).
% 0.51/0.38 thf(c_0_61, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld, X10:mworld]:(~((v21 @ (esk30_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_56, c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_62, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((v20 @ X3)|(v21 @ X5)|(v3 @ X6))), inference(spm,[status(thm)],[c_0_57, c_0_58])).
% 0.51/0.38 thf(c_0_63, plain, ![X1081:mworld]:(((epred30_1 @ X1081)=>![X1080:mworld]:(((mrel @ X1081 @ X1080)=>![X1079:mworld]:(((mrel @ X1080 @ X1079)=>![X1078:mworld]:(((mrel @ X1079 @ X1078)=>![X1077:mworld]:(((mrel @ X1078 @ X1077)=>![X1076:mworld]:(((mrel @ X1077 @ X1076)=>![X1075:mworld]:(((mrel @ X1076 @ X1075)=>![X1074:mworld]:(((mrel @ X1075 @ X1074)=>![X1073:mworld]:(((mrel @ X1074 @ X1073)=>![X1072:mworld]:(((mrel @ X1073 @ X1072)=>![X1071:mworld]:(((mrel @ X1072 @ X1071)=>![X1070:mworld]:(((mrel @ X1071 @ X1070)=>((v13 @ X1070)|![X1069:mworld]:(((mrel @ X1070 @ X1069)=>((v12 @ 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)=>![X1063:mworld]:(((mrel @ X1064 @ X1063)=>((v6 @ X1063)|![X1062:mworld]:(((mrel @ X1063 @ X1062)=>![X1061:mworld]:(((mrel @ X1062 @ X1061)=>![X1060:mworld]:(((mrel @ X1061 @ X1060)=>~(v3 @ X1060)))))))))))))))))))))))))))))))))))))))))))))))), inference(split_equiv,[status(thm)],[c_0_54])).
% 0.51/0.38 thf(c_0_64, plain, ![X1696:mworld, X1697:mworld, X1698:mworld, X1699:mworld, X1700:mworld]:((~(mrel @ mactual @ X1696)|(~(mrel @ X1696 @ X1697)|(~(mrel @ X1697 @ X1698)|(~(mrel @ X1698 @ X1699)|(~(mrel @ X1699 @ X1700)|(epred30_1 @ X1700))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_59])])])])).
% 0.51/0.38 thf(c_0_65, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v21 @ X3)|(v15 @ X5)|(v12 @ X6)|~((v20 @ 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)],[c_0_60, c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_66, plain, ![X3:mworld, X5:mworld]:(((v3 @ X3)|(v20 @ X5))), inference(spm,[status(thm)],[c_0_61, c_0_62])).
% 0.51/0.38 thf(c_0_67, plain, ![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, X2462:mworld, X2463:mworld, X2464:mworld, X2465:mworld, X2466:mworld, X2467:mworld, X2468:mworld, X2469:mworld]:((~(epred30_1 @ X2448)|(~(mrel @ X2448 @ X2449)|(~(mrel @ X2449 @ X2450)|(~(mrel @ X2450 @ X2451)|(~(mrel @ X2451 @ X2452)|(~(mrel @ X2452 @ X2453)|(~(mrel @ X2453 @ X2454)|(~(mrel @ X2454 @ X2455)|(~(mrel @ X2455 @ X2456)|(~(mrel @ X2456 @ X2457)|(~(mrel @ X2457 @ X2458)|(~(mrel @ X2458 @ X2459)|((v13 @ X2459)|(~(mrel @ X2459 @ X2460)|((v12 @ X2460)|(~(mrel @ X2460 @ X2461)|(~(mrel @ X2461 @ X2462)|(~(mrel @ X2462 @ X2463)|(~(mrel @ X2463 @ X2464)|(~(mrel @ X2464 @ X2465)|(~(mrel @ X2465 @ X2466)|((v6 @ X2466)|(~(mrel @ X2466 @ X2467)|(~(mrel @ X2467 @ X2468)|(~(mrel @ X2468 @ X2469)|~(v3 @ X2469))))))))))))))))))))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_63])])])])).
% 0.51/0.38 thf(c_0_68, 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_64])).
% 0.51/0.38 thf(c_0_69, 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 @ (esk22_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_38])).
% 0.51/0.38 thf(c_0_70, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v3 @ X3)|(v12 @ X5)|(v15 @ X6)|(v21 @ X7))), inference(spm,[status(thm)],[c_0_65, c_0_66])).
% 0.51/0.38 thf(c_0_71, 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 @ X15)|(v12 @ X16)|(v6 @ X22)|~((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))|~((mrel @ X19 @ X20))|~((mrel @ X20 @ X21))|~((mrel @ X21 @ X22))|~((mrel @ X22 @ X23))|~((mrel @ X23 @ X24))|~((mrel @ X24 @ X25))|~((v3 @ X25)))), inference(split_conjunct,[status(thm)],[c_0_67])).
% 0.51/0.38 thf(c_0_72, 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_68, c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_73, 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 @ (esk22_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_69, c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_74, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((v15 @ X3)|(v12 @ X5)|(v3 @ X6))), inference(spm,[status(thm)],[c_0_61, c_0_70])).
% 0.51/0.38 thf(c_0_75, plain, ![X798:mworld]:(((mrel @ mactual @ X798)=>![X797:mworld]:(((mrel @ X798 @ X797)=>![X796:mworld]:(((mrel @ X797 @ X796)=>![X795:mworld]:(((mrel @ X796 @ X795)=>![X794:mworld]:(((mrel @ X795 @ X794)=>![X793:mworld]:(((mrel @ X794 @ X793)=>(~(v23 @ X793)|![X792:mworld]:(((mrel @ X793 @ X792)=>((v22 @ X792)|![X791:mworld]:(((mrel @ X792 @ X791)=>![X790:mworld]:(((mrel @ X791 @ X790)=>![X789:mworld]:(((mrel @ X790 @ X789)=>![X788:mworld]:(((mrel @ X789 @ X788)=>![X787:mworld]:(((mrel @ X788 @ X787)=>![X786:mworld]:(((mrel @ X787 @ X786)=>![X785:mworld]:(((mrel @ X786 @ X785)=>![X784:mworld]:(((mrel @ X785 @ X784)=>![X783:mworld]:(((mrel @ X784 @ X783)=>![X782:mworld]:(((mrel @ X783 @ X782)=>(~(v12 @ X782)|![X781:mworld]:(((mrel @ X782 @ X781)=>![X780:mworld]:(((mrel @ X781 @ X780)=>(v10 @ X780)))))))))))))))))))))))))))))))))))))))))), 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)],[mod34, c_0_23]), c_0_24]), c_0_25]), c_0_26])])).
% 0.51/0.38 thf(c_0_76, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v13 @ X3)|(v12 @ X5)|(v6 @ X6)|~((v3 @ 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_71, c_0_72]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_77, plain, ![X3:mworld, X5:mworld]:(((v3 @ X3)|(v12 @ X5))), inference(spm,[status(thm)],[c_0_73, c_0_74])).
% 0.51/0.38 thf(c_0_78, plain, ![X1563:mworld, X1564:mworld, X1565:mworld, X1566:mworld, X1567:mworld, X1568:mworld, X1569:mworld, X1570:mworld, X1571:mworld, X1572:mworld, X1573:mworld, X1574:mworld, X1575:mworld, X1576:mworld, X1577:mworld, X1578:mworld, X1579:mworld, X1580:mworld, X1581:mworld]:((~(mrel @ mactual @ X1563)|(~(mrel @ X1563 @ X1564)|(~(mrel @ X1564 @ X1565)|(~(mrel @ X1565 @ X1566)|(~(mrel @ X1566 @ X1567)|(~(mrel @ X1567 @ X1568)|(~(v23 @ X1568)|(~(mrel @ X1568 @ X1569)|((v22 @ X1569)|(~(mrel @ X1569 @ X1570)|(~(mrel @ X1570 @ X1571)|(~(mrel @ X1571 @ X1572)|(~(mrel @ X1572 @ X1573)|(~(mrel @ X1573 @ X1574)|(~(mrel @ X1574 @ X1575)|(~(mrel @ X1575 @ X1576)|(~(mrel @ X1576 @ X1577)|(~(mrel @ X1577 @ X1578)|(~(mrel @ X1578 @ X1579)|(~(v12 @ X1579)|(~(mrel @ X1579 @ X1580)|(~(mrel @ X1580 @ X1581)|(v10 @ X1581)))))))))))))))))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_75])])])])).
% 0.51/0.38 thf(c_0_79, 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_38])).
% 0.51/0.38 thf(c_0_80, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v12 @ X3)|(v6 @ X5)|(v12 @ X6)|(v13 @ X7))), inference(spm,[status(thm)],[c_0_76, c_0_77])).
% 0.51/0.38 thf(c_0_81, 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]:(((v22 @ X10)|(v10 @ X22)|~((mrel @ mactual @ X3))|~((mrel @ X3 @ X5))|~((mrel @ X5 @ X6))|~((mrel @ X6 @ X7))|~((mrel @ X7 @ X8))|~((mrel @ X8 @ X9))|~((v23 @ 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))|~((v12 @ X20))|~((mrel @ X20 @ X21))|~((mrel @ X21 @ X22)))), inference(split_conjunct,[status(thm)],[c_0_78])).
% 0.51/0.38 thf(c_0_82, 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_79, c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_83, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((v13 @ X3)|(v12 @ X5)|(v6 @ X6))), inference(ef,[status(thm)],[c_0_80])).
% 0.51/0.38 thf(c_0_84, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v22 @ X3)|(v10 @ X5)|~((v12 @ X6))|~((v23 @ 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)],[c_0_81, c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_85, plain, ![X3:mworld, X5:mworld]:(((v6 @ X3)|(v12 @ X5))), inference(spm,[status(thm)],[c_0_82, c_0_83])).
% 0.51/0.38 thf(c_0_86, plain, ![X8:mworld, X7:mworld, X6:mworld, X5:mworld, X3:mworld]:(((v23 @ (esk33_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_38])).
% 0.51/0.38 thf(c_0_87, plain, ![X923:mworld]:(((epred24_1 @ X923)<=>![X922:mworld]:(((mrel @ X923 @ X922)=>![X921:mworld]:(((mrel @ X922 @ X921)=>![X920:mworld]:(((mrel @ X921 @ X920)=>![X919:mworld]:(((mrel @ X920 @ X919)=>![X918:mworld]:(((mrel @ X919 @ X918)=>![X917:mworld]:(((mrel @ X918 @ X917)=>![X916:mworld]:(((mrel @ X917 @ X916)=>(~(v20 @ X916)|![X915:mworld]:(((mrel @ X916 @ X915)=>![X914:mworld]:(((mrel @ X915 @ X914)=>![X913:mworld]:(((mrel @ X914 @ X913)=>![X912:mworld]:(((mrel @ X913 @ X912)=>![X911:mworld]:(((mrel @ X912 @ X911)=>![X910:mworld]:(((mrel @ X911 @ X910)=>((v14 @ X910)|![X909:mworld]:(((mrel @ X910 @ X909)=>![X908:mworld]:(((mrel @ X909 @ X908)=>![X907:mworld]:(((mrel @ X908 @ X907)=>![X906:mworld]:(((mrel @ X907 @ X906)=>(~(v10 @ X906)|![X905:mworld]:(((mrel @ X906 @ X905)=>![X904:mworld]:(((mrel @ X905 @ X904)=>![X903:mworld]:(((mrel @ X904 @ X903)=>![X902:mworld]:(((mrel @ X903 @ X902)=>(v6 @ X902)))))))))))))))))))))))))))))))))))))))))))))))), introduced(definition)).
% 0.51/0.38 thf(c_0_88, 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_38])).
% 0.51/0.38 thf(c_0_89, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v6 @ X3)|(v10 @ X5)|(v22 @ X6)|~((v23 @ X7)))), inference(spm,[status(thm)],[c_0_84, c_0_85])).
% 0.51/0.38 thf(c_0_90, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld]:((v23 @ (esk33_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_86, c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_91, plain, ![X924:mworld]:(((mrel @ mactual @ X924)=>![X923:mworld]:(((mrel @ X924 @ X923)=>(epred24_1 @ X923))))), 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)],[mod40, c_0_23]), c_0_24]), c_0_25]), c_0_26])]), c_0_87])).
% 0.51/0.38 thf(c_0_92, 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_88, c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_93, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((v22 @ X3)|(v10 @ X5)|(v6 @ X6))), inference(spm,[status(thm)],[c_0_89, c_0_90])).
% 0.51/0.38 thf(c_0_94, plain, ![X923:mworld]:(((epred24_1 @ X923)=>![X922:mworld]:(((mrel @ X923 @ X922)=>![X921:mworld]:(((mrel @ X922 @ X921)=>![X920:mworld]:(((mrel @ X921 @ X920)=>![X919:mworld]:(((mrel @ X920 @ X919)=>![X918:mworld]:(((mrel @ X919 @ X918)=>![X917:mworld]:(((mrel @ X918 @ X917)=>![X916:mworld]:(((mrel @ X917 @ X916)=>(~(v20 @ X916)|![X915:mworld]:(((mrel @ X916 @ X915)=>![X914:mworld]:(((mrel @ X915 @ X914)=>![X913:mworld]:(((mrel @ X914 @ X913)=>![X912:mworld]:(((mrel @ X913 @ X912)=>![X911:mworld]:(((mrel @ X912 @ X911)=>![X910:mworld]:(((mrel @ X911 @ X910)=>((v14 @ X910)|![X909:mworld]:(((mrel @ X910 @ X909)=>![X908:mworld]:(((mrel @ X909 @ X908)=>![X907:mworld]:(((mrel @ X908 @ X907)=>![X906:mworld]:(((mrel @ X907 @ X906)=>(~(v10 @ X906)|![X905:mworld]:(((mrel @ X906 @ X905)=>![X904:mworld]:(((mrel @ X905 @ X904)=>![X903:mworld]:(((mrel @ X904 @ X903)=>![X902:mworld]:(((mrel @ X903 @ X902)=>(v6 @ X902)))))))))))))))))))))))))))))))))))))))))))))))), inference(split_equiv,[status(thm)],[c_0_87])).
% 0.51/0.38 thf(c_0_95, plain, ![X1664:mworld, X1665:mworld]:((~(mrel @ mactual @ X1664)|(~(mrel @ X1664 @ X1665)|(epred24_1 @ X1665)))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_91])])])])).
% 0.51/0.38 thf(c_0_96, plain, ![X3:mworld, X5:mworld]:(((v6 @ X3)|(v10 @ X5))), inference(spm,[status(thm)],[c_0_92, c_0_93])).
% 0.51/0.38 thf(c_0_97, plain, ![X468:mworld]:(((epred14_1 @ X468)<=>(~(v24 @ X468)|![X467:mworld]:(((mrel @ X468 @ X467)=>![X466:mworld]:(((mrel @ X467 @ X466)=>![X465:mworld]:(((mrel @ X466 @ X465)=>![X464:mworld]:(((mrel @ X465 @ X464)=>![X463:mworld]:(((mrel @ X464 @ X463)=>![X462:mworld]:(((mrel @ X463 @ X462)=>![X461:mworld]:(((mrel @ X462 @ X461)=>![X460:mworld]:(((mrel @ X461 @ X460)=>![X459:mworld]:(((mrel @ X460 @ X459)=>![X458:mworld]:(((mrel @ X459 @ X458)=>![X457:mworld]:(((mrel @ X458 @ X457)=>![X456:mworld]:(((mrel @ X457 @ X456)=>![X455:mworld]:(((mrel @ X456 @ X455)=>![X454:mworld]:(((mrel @ X455 @ X454)=>![X453:mworld]:(((mrel @ X454 @ X453)=>![X452:mworld]:(((mrel @ X453 @ X452)=>((v8 @ X452)|![X451:mworld]:(((mrel @ X452 @ X451)=>![X450:mworld]:(((mrel @ X451 @ X450)=>![X449:mworld]:(((mrel @ X450 @ X449)=>![X448:mworld]:(((mrel @ X449 @ X448)=>![X447:mworld]:(((mrel @ X448 @ X447)=>![X446:mworld]:(((mrel @ X447 @ X446)=>![X445:mworld]:(((mrel @ X446 @ X445)=>(v1 @ X445))))))))))))))))))))))))))))))))))))))))))))))))))), introduced(definition)).
% 0.51/0.38 thf(c_0_98, plain, ![X2316:mworld, X2317:mworld, X2318:mworld, X2319:mworld, X2320:mworld, X2321:mworld, X2322:mworld, X2323:mworld, X2324:mworld, X2325:mworld, X2326:mworld, X2327:mworld, X2328:mworld, X2329:mworld, X2330:mworld, X2331:mworld, X2332:mworld, X2333:mworld, X2334:mworld, X2335:mworld, X2336:mworld, X2337:mworld]:((~(epred24_1 @ X2316)|(~(mrel @ X2316 @ X2317)|(~(mrel @ X2317 @ X2318)|(~(mrel @ X2318 @ X2319)|(~(mrel @ X2319 @ X2320)|(~(mrel @ X2320 @ X2321)|(~(mrel @ X2321 @ X2322)|(~(mrel @ X2322 @ X2323)|(~(v20 @ X2323)|(~(mrel @ X2323 @ X2324)|(~(mrel @ X2324 @ X2325)|(~(mrel @ X2325 @ X2326)|(~(mrel @ X2326 @ X2327)|(~(mrel @ X2327 @ X2328)|(~(mrel @ X2328 @ X2329)|((v14 @ X2329)|(~(mrel @ X2329 @ X2330)|(~(mrel @ X2330 @ X2331)|(~(mrel @ X2331 @ X2332)|(~(mrel @ X2332 @ X2333)|(~(v10 @ X2333)|(~(mrel @ X2333 @ X2334)|(~(mrel @ X2334 @ X2335)|(~(mrel @ X2335 @ X2336)|(~(mrel @ X2336 @ X2337)|(v6 @ X2337))))))))))))))))))))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_94])])])])).
% 0.51/0.38 thf(c_0_99, plain, ![X3:mworld, X5:mworld]:(((epred24_1 @ X5)|~((mrel @ mactual @ X3))|~((mrel @ X3 @ X5)))), inference(split_conjunct,[status(thm)],[c_0_95])).
% 0.51/0.38 thf(c_0_100, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v6 @ X3)|(v21 @ X5)|(v20 @ X6)|~((v15 @ X7)))), inference(spm,[status(thm)],[c_0_51, c_0_96])).
% 0.51/0.38 thf(c_0_101, plain, ![X701:mworld]:(((epred20_1 @ X701)<=>![X700:mworld]:(((mrel @ X701 @ X700)=>![X699:mworld]:(((mrel @ X700 @ X699)=>![X698:mworld]:(((mrel @ X699 @ X698)=>(~(v20 @ X698)|![X697:mworld]:(((mrel @ X698 @ X697)=>![X696:mworld]:(((mrel @ X697 @ X696)=>![X695:mworld]:(((mrel @ X696 @ X695)=>![X694:mworld]:(((mrel @ X695 @ X694)=>![X693:mworld]:(((mrel @ X694 @ X693)=>![X692:mworld]:(((mrel @ X693 @ X692)=>![X691:mworld]:(((mrel @ X692 @ X691)=>![X690:mworld]:(((mrel @ X691 @ X690)=>![X689:mworld]:(((mrel @ X690 @ X689)=>![X688:mworld]:(((mrel @ X689 @ X688)=>![X687:mworld]:(((mrel @ X688 @ X687)=>![X686:mworld]:(((mrel @ X687 @ X686)=>![X685:mworld]:(((mrel @ X686 @ X685)=>![X684:mworld]:(((mrel @ X685 @ X684)=>(~(v6 @ X684)|![X683:mworld]:(((mrel @ X684 @ X683)=>![X682:mworld]:(((mrel @ X683 @ X682)=>![X681:mworld]:(((mrel @ X682 @ X681)=>![X680:mworld]:(((mrel @ X681 @ X680)=>![X679:mworld]:(((mrel @ X680 @ X679)=>(v1 @ X679))))))))))))))))))))))))))))))))))))))))))))))))), introduced(definition)).
% 0.51/0.38 thf(c_0_102, plain, ![X468:mworld]:(((epred14_1 @ X468)=>(~(v24 @ X468)|![X467:mworld]:(((mrel @ X468 @ X467)=>![X466:mworld]:(((mrel @ X467 @ X466)=>![X465:mworld]:(((mrel @ X466 @ X465)=>![X464:mworld]:(((mrel @ X465 @ X464)=>![X463:mworld]:(((mrel @ X464 @ X463)=>![X462:mworld]:(((mrel @ X463 @ X462)=>![X461:mworld]:(((mrel @ X462 @ X461)=>![X460:mworld]:(((mrel @ X461 @ X460)=>![X459:mworld]:(((mrel @ X460 @ X459)=>![X458:mworld]:(((mrel @ X459 @ X458)=>![X457:mworld]:(((mrel @ X458 @ X457)=>![X456:mworld]:(((mrel @ X457 @ X456)=>![X455:mworld]:(((mrel @ X456 @ X455)=>![X454:mworld]:(((mrel @ X455 @ X454)=>![X453:mworld]:(((mrel @ X454 @ X453)=>![X452:mworld]:(((mrel @ X453 @ X452)=>((v8 @ X452)|![X451:mworld]:(((mrel @ X452 @ X451)=>![X450:mworld]:(((mrel @ X451 @ X450)=>![X449:mworld]:(((mrel @ X450 @ X449)=>![X448:mworld]:(((mrel @ X449 @ X448)=>![X447:mworld]:(((mrel @ X448 @ X447)=>![X446:mworld]:(((mrel @ X447 @ X446)=>![X445:mworld]:(((mrel @ X446 @ X445)=>(v1 @ X445))))))))))))))))))))))))))))))))))))))))))))))))))), inference(split_equiv,[status(thm)],[c_0_97])).
% 0.51/0.38 thf(c_0_103, plain, ![X472:mworld]:(((mrel @ mactual @ X472)=>![X471:mworld]:(((mrel @ X472 @ X471)=>![X470:mworld]:(((mrel @ X471 @ X470)=>![X469:mworld]:(((mrel @ X470 @ X469)=>((v25 @ X469)|![X468:mworld]:(((mrel @ X469 @ X468)=>(epred14_1 @ X468)))))))))))), 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)],[mod20, c_0_23]), c_0_24]), c_0_25]), c_0_26])]), c_0_97])).
% 0.51/0.38 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, X15:mworld, X16:mworld, X17:mworld, X18:mworld, X19:mworld, X20:mworld, X21:mworld, X22:mworld, X23:mworld, X24:mworld, X25:mworld]:(((v14 @ X17)|(v6 @ X25)|~((epred24_1 @ X3))|~((mrel @ X3 @ X5))|~((mrel @ X5 @ X6))|~((mrel @ X6 @ X7))|~((mrel @ X7 @ X8))|~((mrel @ X8 @ X9))|~((mrel @ X9 @ X10))|~((mrel @ X10 @ X11))|~((v20 @ 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))|~((v10 @ X21))|~((mrel @ X21 @ X22))|~((mrel @ X22 @ X23))|~((mrel @ X23 @ X24))|~((mrel @ X24 @ X25)))), inference(split_conjunct,[status(thm)],[c_0_98])).
% 0.51/0.38 thf(c_0_105, plain, ![X3:mworld]:((epred24_1 @ X3)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_99, c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_106, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((v20 @ X3)|(v21 @ X5)|(v6 @ X6))), inference(spm,[status(thm)],[c_0_100, c_0_58])).
% 0.51/0.38 thf(c_0_107, plain, ![X706:mworld]:(((mrel @ mactual @ X706)=>![X705:mworld]:(((mrel @ X706 @ X705)=>![X704:mworld]:(((mrel @ X705 @ X704)=>![X703:mworld]:(((mrel @ X704 @ X703)=>![X702:mworld]:(((mrel @ X703 @ X702)=>(~(v24 @ X702)|![X701:mworld]:(((mrel @ X702 @ X701)=>(epred20_1 @ X701)))))))))))))), 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)],[mod30, c_0_23]), c_0_24]), c_0_25]), c_0_26])]), c_0_101])).
% 0.51/0.38 thf(c_0_108, plain, ![X2091:mworld, X2092:mworld, X2093:mworld, X2094:mworld, X2095:mworld, X2096:mworld, X2097:mworld, X2098:mworld, X2099:mworld, X2100:mworld, X2101:mworld, X2102:mworld, X2103:mworld, X2104:mworld, X2105:mworld, X2106:mworld, X2107:mworld, X2108:mworld, X2109:mworld, X2110:mworld, X2111:mworld, X2112:mworld, X2113:mworld, X2114:mworld]:((~(epred14_1 @ X2091)|(~(v24 @ X2091)|(~(mrel @ X2091 @ X2092)|(~(mrel @ X2092 @ X2093)|(~(mrel @ X2093 @ X2094)|(~(mrel @ X2094 @ X2095)|(~(mrel @ X2095 @ X2096)|(~(mrel @ X2096 @ X2097)|(~(mrel @ X2097 @ X2098)|(~(mrel @ X2098 @ X2099)|(~(mrel @ X2099 @ X2100)|(~(mrel @ X2100 @ X2101)|(~(mrel @ X2101 @ X2102)|(~(mrel @ X2102 @ X2103)|(~(mrel @ X2103 @ X2104)|(~(mrel @ X2104 @ X2105)|(~(mrel @ X2105 @ X2106)|(~(mrel @ X2106 @ X2107)|((v8 @ X2107)|(~(mrel @ X2107 @ X2108)|(~(mrel @ X2108 @ X2109)|(~(mrel @ X2109 @ X2110)|(~(mrel @ X2110 @ X2111)|(~(mrel @ X2111 @ X2112)|(~(mrel @ X2112 @ X2113)|(~(mrel @ X2113 @ X2114)|(v1 @ X2114)))))))))))))))))))))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_102])])])])).
% 0.51/0.38 thf(c_0_109, plain, ![X1422:mworld, X1423:mworld, X1424:mworld, X1425:mworld, X1426:mworld]:((~(mrel @ mactual @ X1422)|(~(mrel @ X1422 @ X1423)|(~(mrel @ X1423 @ X1424)|(~(mrel @ X1424 @ X1425)|((v25 @ X1425)|(~(mrel @ X1425 @ X1426)|(epred14_1 @ X1426)))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_103])])])])).
% 0.51/0.38 thf(c_0_110, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((v14 @ X3)|(v6 @ X5)|~((v20 @ X6)))), inference(csr,[status(thm)],[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_104, c_0_105]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])]), c_0_96])).
% 0.51/0.38 thf(c_0_111, plain, ![X3:mworld, X5:mworld]:(((v6 @ X3)|(v20 @ X5))), inference(spm,[status(thm)],[c_0_61, c_0_106])).
% 0.51/0.38 thf(c_0_112, plain, ![X1527:mworld, X1528:mworld, X1529:mworld, X1530:mworld, X1531:mworld, X1532:mworld]:((~(mrel @ mactual @ X1527)|(~(mrel @ X1527 @ X1528)|(~(mrel @ X1528 @ X1529)|(~(mrel @ X1529 @ X1530)|(~(mrel @ X1530 @ X1531)|(~(v24 @ X1531)|(~(mrel @ X1531 @ X1532)|(epred20_1 @ X1532))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_107])])])])).
% 0.51/0.38 thf(c_0_113, plain, ![X516:mworld]:(((mrel @ mactual @ X516)=>![X515:mworld]:(((mrel @ X516 @ X515)=>![X514:mworld]:(((mrel @ X515 @ X514)=>![X513:mworld]:(((mrel @ X514 @ X513)=>((v25 @ X513)|![X512:mworld]:(((mrel @ X513 @ X512)=>![X511:mworld]:(((mrel @ X512 @ X511)=>![X510:mworld]:(((mrel @ X511 @ X510)=>![X509:mworld]:(((mrel @ X510 @ X509)=>![X508:mworld]:(((mrel @ X509 @ X508)=>((v20 @ X508)|![X507:mworld]:(((mrel @ X508 @ X507)=>![X506:mworld]:(((mrel @ X507 @ X506)=>![X505:mworld]:(((mrel @ X506 @ X505)=>![X504:mworld]:(((mrel @ X505 @ X504)=>![X503:mworld]:(((mrel @ X504 @ X503)=>![X502:mworld]:(((mrel @ X503 @ X502)=>(~(v14 @ X502)|![X501:mworld]:(((mrel @ X502 @ X501)=>![X500:mworld]:(((mrel @ X501 @ X500)=>![X499:mworld]:(((mrel @ X500 @ X499)=>![X498:mworld]:(((mrel @ X499 @ X498)=>![X497:mworld]:(((mrel @ X498 @ X497)=>![X496:mworld]:(((mrel @ X497 @ X496)=>~(v8 @ X496)))))))))))))))))))))))))))))))))))))))))))))), inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[mod22, c_0_23]), c_0_24]), c_0_25]), c_0_26])])).
% 0.51/0.38 thf(c_0_114, 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, X27:mworld]:(((v8 @ X20)|(v1 @ X27)|~((epred14_1 @ X3))|~((v24 @ X3))|~((mrel @ X3 @ X5))|~((mrel @ X5 @ X6))|~((mrel @ X6 @ X7))|~((mrel @ X7 @ X8))|~((mrel @ X8 @ X9))|~((mrel @ X9 @ X10))|~((mrel @ X10 @ X11))|~((mrel @ X11 @ X12))|~((mrel @ X12 @ X13))|~((mrel @ X13 @ X14))|~((mrel @ X14 @ X15))|~((mrel @ X15 @ X16))|~((mrel @ X16 @ X17))|~((mrel @ X17 @ X18))|~((mrel @ X18 @ X19))|~((mrel @ X19 @ X20))|~((mrel @ X20 @ X21))|~((mrel @ X21 @ X22))|~((mrel @ X22 @ X23))|~((mrel @ X23 @ X24))|~((mrel @ X24 @ X25))|~((mrel @ X25 @ X26))|~((mrel @ X26 @ X27)))), inference(split_conjunct,[status(thm)],[c_0_108])).
% 0.51/0.38 thf(c_0_115, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld]:(((v25 @ X7)|(epred14_1 @ X8)|~((mrel @ mactual @ X3))|~((mrel @ X3 @ X5))|~((mrel @ X5 @ X6))|~((mrel @ X6 @ X7))|~((mrel @ X7 @ X8)))), inference(split_conjunct,[status(thm)],[c_0_109])).
% 0.51/0.38 thf(c_0_116, plain, ![X701:mworld]:(((epred20_1 @ X701)=>![X700:mworld]:(((mrel @ X701 @ X700)=>![X699:mworld]:(((mrel @ X700 @ X699)=>![X698:mworld]:(((mrel @ X699 @ X698)=>(~(v20 @ X698)|![X697:mworld]:(((mrel @ X698 @ X697)=>![X696:mworld]:(((mrel @ X697 @ X696)=>![X695:mworld]:(((mrel @ X696 @ X695)=>![X694:mworld]:(((mrel @ X695 @ X694)=>![X693:mworld]:(((mrel @ X694 @ X693)=>![X692:mworld]:(((mrel @ X693 @ X692)=>![X691:mworld]:(((mrel @ X692 @ X691)=>![X690:mworld]:(((mrel @ X691 @ X690)=>![X689:mworld]:(((mrel @ X690 @ X689)=>![X688:mworld]:(((mrel @ X689 @ X688)=>![X687:mworld]:(((mrel @ X688 @ X687)=>![X686:mworld]:(((mrel @ X687 @ X686)=>![X685:mworld]:(((mrel @ X686 @ X685)=>![X684:mworld]:(((mrel @ X685 @ X684)=>(~(v6 @ X684)|![X683:mworld]:(((mrel @ X684 @ X683)=>![X682:mworld]:(((mrel @ X683 @ X682)=>![X681:mworld]:(((mrel @ X682 @ X681)=>![X680:mworld]:(((mrel @ X681 @ X680)=>![X679:mworld]:(((mrel @ X680 @ X679)=>(v1 @ X679))))))))))))))))))))))))))))))))))))))))))))))))), inference(split_equiv,[status(thm)],[c_0_101])).
% 0.51/0.38 thf(c_0_117, 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_38])).
% 0.51/0.38 thf(c_0_118, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((v6 @ X3)|(v6 @ X5)|(v14 @ X6))), inference(spm,[status(thm)],[c_0_110, c_0_111])).
% 0.51/0.38 thf(c_0_119, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld]:(((epred20_1 @ X9)|~((mrel @ mactual @ X3))|~((mrel @ X3 @ X5))|~((mrel @ X5 @ X6))|~((mrel @ X6 @ X7))|~((mrel @ X7 @ X8))|~((v24 @ X8))|~((mrel @ X8 @ X9)))), inference(split_conjunct,[status(thm)],[c_0_112])).
% 0.51/0.38 thf(c_0_120, 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_38])).
% 0.51/0.38 thf(c_0_121, plain, ![X1053:mworld]:(((epred29_1 @ 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)=>(~(v15 @ X1046)|![X1045:mworld]:(((mrel @ X1046 @ X1045)=>![X1044:mworld]:(((mrel @ X1045 @ X1044)=>![X1043:mworld]:(((mrel @ X1044 @ X1043)=>![X1042:mworld]:(((mrel @ X1043 @ X1042)=>(~(v11 @ X1042)|![X1041:mworld]:(((mrel @ X1042 @ X1041)=>![X1040:mworld]:(((mrel @ X1041 @ X1040)=>![X1039:mworld]:(((mrel @ X1040 @ X1039)=>![X1038:mworld]:(((mrel @ X1039 @ X1038)=>(~(v7 @ X1038)|![X1037:mworld]:(((mrel @ X1038 @ X1037)=>![X1036:mworld]:(((mrel @ X1037 @ X1036)=>![X1035:mworld]:(((mrel @ X1036 @ X1035)=>![X1034:mworld]:(((mrel @ X1035 @ X1034)=>![X1033:mworld]:(((mrel @ X1034 @ X1033)=>![X1032:mworld]:(((mrel @ X1033 @ X1032)=>~(v1 @ X1032)))))))))))))))))))))))))))))))))))))))))))))))), introduced(definition)).
% 0.51/0.38 thf(c_0_122, plain, ![X1429:mworld, X1430:mworld, X1431:mworld, X1432:mworld, X1433:mworld, X1434:mworld, X1435:mworld, X1436:mworld, X1437:mworld, X1438:mworld, X1439:mworld, X1440:mworld, X1441:mworld, X1442:mworld, X1443:mworld, X1444:mworld, X1445:mworld, X1446:mworld, X1447:mworld, X1448:mworld, X1449:mworld]:((~(mrel @ mactual @ X1429)|(~(mrel @ X1429 @ X1430)|(~(mrel @ X1430 @ X1431)|(~(mrel @ X1431 @ X1432)|((v25 @ X1432)|(~(mrel @ X1432 @ X1433)|(~(mrel @ X1433 @ X1434)|(~(mrel @ X1434 @ X1435)|(~(mrel @ X1435 @ X1436)|(~(mrel @ X1436 @ X1437)|((v20 @ X1437)|(~(mrel @ X1437 @ X1438)|(~(mrel @ X1438 @ X1439)|(~(mrel @ X1439 @ X1440)|(~(mrel @ X1440 @ X1441)|(~(mrel @ X1441 @ X1442)|(~(mrel @ X1442 @ X1443)|(~(v14 @ X1443)|(~(mrel @ X1443 @ X1444)|(~(mrel @ X1444 @ X1445)|(~(mrel @ X1445 @ X1446)|(~(mrel @ X1446 @ X1447)|(~(mrel @ X1447 @ X1448)|(~(mrel @ X1448 @ X1449)|~(v8 @ X1449)))))))))))))))))))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_113])])])])).
% 0.51/0.38 thf(c_0_123, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((v8 @ X3)|(v1 @ X5)|~((v24 @ X6))|~((epred14_1 @ X6)))), 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_114, c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_124, plain, ![X3:mworld, X5:mworld]:(((epred14_1 @ X3)|(v25 @ X5))), 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_115, c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_125, plain, ![X2226:mworld, X2227:mworld, X2228:mworld, X2229:mworld, X2230:mworld, X2231:mworld, X2232:mworld, X2233:mworld, X2234:mworld, X2235:mworld, X2236:mworld, X2237:mworld, X2238:mworld, X2239:mworld, X2240:mworld, X2241:mworld, X2242:mworld, X2243:mworld, X2244:mworld, X2245:mworld, X2246:mworld, X2247:mworld, X2248:mworld]:((~(epred20_1 @ X2226)|(~(mrel @ X2226 @ X2227)|(~(mrel @ X2227 @ X2228)|(~(mrel @ X2228 @ X2229)|(~(v20 @ X2229)|(~(mrel @ X2229 @ X2230)|(~(mrel @ X2230 @ X2231)|(~(mrel @ X2231 @ X2232)|(~(mrel @ X2232 @ X2233)|(~(mrel @ X2233 @ X2234)|(~(mrel @ X2234 @ X2235)|(~(mrel @ X2235 @ X2236)|(~(mrel @ X2236 @ X2237)|(~(mrel @ X2237 @ X2238)|(~(mrel @ X2238 @ X2239)|(~(mrel @ X2239 @ X2240)|(~(mrel @ X2240 @ X2241)|(~(mrel @ X2241 @ X2242)|(~(mrel @ X2242 @ X2243)|(~(v6 @ X2243)|(~(mrel @ X2243 @ X2244)|(~(mrel @ X2244 @ X2245)|(~(mrel @ X2245 @ X2246)|(~(mrel @ X2246 @ X2247)|(~(mrel @ X2247 @ X2248)|(v1 @ X2248))))))))))))))))))))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_116])])])])).
% 0.51/0.38 thf(c_0_126, 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_117, c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_127, plain, ![X3:mworld, X5:mworld]:(((v14 @ X3)|(v6 @ X5))), inference(ef,[status(thm)],[c_0_118])).
% 0.51/0.38 thf(c_0_128, plain, ![X3:mworld, X5:mworld]:(((epred20_1 @ X3)|~((v24 @ X5)))), 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_119, c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_129, 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_120, c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_130, plain, ![X427:mworld]:(((mrel @ mactual @ X427)=>![X426:mworld]:(((mrel @ X427 @ X426)=>![X425:mworld]:(((mrel @ X426 @ X425)=>![X424:mworld]:(((mrel @ X425 @ X424)=>((v25 @ X424)|![X423:mworld]:(((mrel @ X424 @ X423)=>(~(v24 @ X423)|![X422:mworld]:(((mrel @ X423 @ X422)=>![X421:mworld]:(((mrel @ X422 @ X421)=>![X420:mworld]:(((mrel @ X421 @ X420)=>![X419:mworld]:(((mrel @ X420 @ X419)=>![X418:mworld]:(((mrel @ X419 @ X418)=>![X417:mworld]:(((mrel @ X418 @ X417)=>![X416:mworld]:(((mrel @ X417 @ X416)=>![X415:mworld]:(((mrel @ X416 @ X415)=>((v16 @ X415)|![X414:mworld]:(((mrel @ X415 @ X414)=>![X413:mworld]:(((mrel @ X414 @ X413)=>![X412:mworld]:(((mrel @ X413 @ X412)=>![X411:mworld]:(((mrel @ X412 @ X411)=>![X410:mworld]:(((mrel @ X411 @ X410)=>(v11 @ X410)))))))))))))))))))))))))))))))))))))))), 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)],[mod18, c_0_23]), c_0_24]), c_0_25]), c_0_26])])).
% 0.51/0.38 thf(c_0_131, plain, ![X444:mworld]:(((mrel @ mactual @ X444)=>![X443:mworld]:(((mrel @ X444 @ X443)=>![X442:mworld]:(((mrel @ X443 @ X442)=>![X441:mworld]:(((mrel @ X442 @ X441)=>((v25 @ X441)|![X440:mworld]:(((mrel @ X441 @ X440)=>(~(v24 @ X440)|![X439:mworld]:(((mrel @ X440 @ X439)=>![X438:mworld]:(((mrel @ X439 @ X438)=>![X437:mworld]:(((mrel @ X438 @ X437)=>![X436:mworld]:(((mrel @ X437 @ X436)=>![X435:mworld]:(((mrel @ X436 @ X435)=>![X434:mworld]:(((mrel @ X435 @ X434)=>![X433:mworld]:(((mrel @ X434 @ X433)=>![X432:mworld]:(((mrel @ X433 @ X432)=>![X431:mworld]:(((mrel @ X432 @ X431)=>![X430:mworld]:(((mrel @ X431 @ X430)=>![X429:mworld]:(((mrel @ X430 @ X429)=>((v13 @ X429)|![X428:mworld]:(((mrel @ X429 @ X428)=>~(v12 @ X428)))))))))))))))))))))))))))))))))))))), 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)],[mod19, c_0_23]), c_0_24]), c_0_25]), c_0_26])])).
% 0.51/0.38 thf(c_0_132, plain, ![X1059:mworld]:(((mrel @ mactual @ 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)=>![X1053:mworld]:(((mrel @ X1054 @ X1053)=>(epred29_1 @ X1053))))))))))))))), 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_23]), c_0_24]), c_0_25]), c_0_26])]), c_0_121])).
% 0.51/0.38 thf(c_0_133, 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]:(((v25 @ X7)|(v20 @ X12)|~((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))|~((mrel @ X17 @ X18))|~((v14 @ X18))|~((mrel @ X18 @ X19))|~((mrel @ X19 @ X20))|~((mrel @ X20 @ X21))|~((mrel @ X21 @ X22))|~((mrel @ X22 @ X23))|~((mrel @ X23 @ X24))|~((v8 @ X24)))), inference(split_conjunct,[status(thm)],[c_0_122])).
% 0.51/0.38 thf(c_0_134, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v25 @ X3)|(v1 @ X5)|(v8 @ X6)|~((v24 @ X7)))), inference(spm,[status(thm)],[c_0_123, c_0_124])).
% 0.51/0.38 thf(c_0_135, 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]:(((v1 @ X26)|~((epred20_1 @ X3))|~((mrel @ X3 @ X5))|~((mrel @ X5 @ X6))|~((mrel @ X6 @ X7))|~((v20 @ 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))|~((v6 @ X21))|~((mrel @ X21 @ X22))|~((mrel @ X22 @ X23))|~((mrel @ X23 @ X24))|~((mrel @ X24 @ X25))|~((mrel @ X25 @ X26)))), inference(split_conjunct,[status(thm)],[c_0_125])).
% 0.51/0.38 thf(c_0_136, plain, ![X3:mworld]:((v6 @ X3)), inference(spm,[status(thm)],[c_0_126, c_0_127])).
% 0.51/0.38 thf(c_0_137, plain, ![X3:mworld]:((epred20_1 @ X3)), inference(spm,[status(thm)],[c_0_128, c_0_129])).
% 0.51/0.38 thf(c_0_138, plain, ![X1387:mworld, X1388:mworld, X1389:mworld, X1390:mworld, X1391:mworld, X1392:mworld, X1393:mworld, X1394:mworld, X1395:mworld, X1396:mworld, X1397:mworld, X1398:mworld, X1399:mworld, X1400:mworld, X1401:mworld, X1402:mworld, X1403:mworld, X1404:mworld]:((~(mrel @ mactual @ X1387)|(~(mrel @ X1387 @ X1388)|(~(mrel @ X1388 @ X1389)|(~(mrel @ X1389 @ X1390)|((v25 @ X1390)|(~(mrel @ X1390 @ X1391)|(~(v24 @ X1391)|(~(mrel @ X1391 @ X1392)|(~(mrel @ X1392 @ X1393)|(~(mrel @ X1393 @ X1394)|(~(mrel @ X1394 @ X1395)|(~(mrel @ X1395 @ X1396)|(~(mrel @ X1396 @ X1397)|(~(mrel @ X1397 @ X1398)|(~(mrel @ X1398 @ X1399)|((v16 @ X1399)|(~(mrel @ X1399 @ X1400)|(~(mrel @ X1400 @ X1401)|(~(mrel @ X1401 @ X1402)|(~(mrel @ X1402 @ X1403)|(~(mrel @ X1403 @ X1404)|(v11 @ X1404))))))))))))))))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_130])])])])).
% 0.51/0.38 thf(c_0_139, plain, ![X580:mworld]:(((epred16_1 @ X580)<=>![X579:mworld]:(((mrel @ X580 @ X579)=>![X578:mworld]:(((mrel @ X579 @ X578)=>(~(v25 @ X578)|![X577:mworld]:(((mrel @ X578 @ X577)=>![X576:mworld]:(((mrel @ X577 @ X576)=>((v23 @ X576)|![X575:mworld]:(((mrel @ X576 @ X575)=>![X574:mworld]:(((mrel @ X575 @ X574)=>![X573:mworld]:(((mrel @ X574 @ X573)=>![X572:mworld]:(((mrel @ X573 @ X572)=>![X571:mworld]:(((mrel @ X572 @ X571)=>![X570:mworld]:(((mrel @ X571 @ X570)=>![X569:mworld]:(((mrel @ X570 @ X569)=>![X568:mworld]:(((mrel @ X569 @ X568)=>![X567:mworld]:(((mrel @ X568 @ X567)=>![X566:mworld]:(((mrel @ X567 @ X566)=>![X565:mworld]:(((mrel @ X566 @ X565)=>(~(v12 @ X565)|![X564:mworld]:(((mrel @ X565 @ X564)=>![X563:mworld]:(((mrel @ X564 @ X563)=>![X562:mworld]:(((mrel @ X563 @ X562)=>![X561:mworld]:(((mrel @ X562 @ X561)=>![X560:mworld]:(((mrel @ X561 @ X560)=>![X559:mworld]:(((mrel @ X560 @ X559)=>~(v6 @ X559)))))))))))))))))))))))))))))))))))))))))))))))), introduced(definition)).
% 0.51/0.38 thf(c_0_140, plain, ![X1405:mworld, X1406:mworld, X1407:mworld, X1408:mworld, X1409:mworld, X1410:mworld, X1411:mworld, X1412:mworld, X1413:mworld, X1414:mworld, X1415:mworld, X1416:mworld, X1417:mworld, X1418:mworld, X1419:mworld, X1420:mworld, X1421:mworld]:((~(mrel @ mactual @ X1405)|(~(mrel @ X1405 @ X1406)|(~(mrel @ X1406 @ X1407)|(~(mrel @ X1407 @ X1408)|((v25 @ X1408)|(~(mrel @ X1408 @ X1409)|(~(v24 @ X1409)|(~(mrel @ X1409 @ X1410)|(~(mrel @ X1410 @ X1411)|(~(mrel @ X1411 @ X1412)|(~(mrel @ X1412 @ X1413)|(~(mrel @ X1413 @ X1414)|(~(mrel @ X1414 @ X1415)|(~(mrel @ X1415 @ X1416)|(~(mrel @ X1416 @ X1417)|(~(mrel @ X1417 @ X1418)|(~(mrel @ X1418 @ X1419)|(~(mrel @ X1419 @ X1420)|((v13 @ X1420)|(~(mrel @ X1420 @ X1421)|~(v12 @ X1421)))))))))))))))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_131])])])])).
% 0.51/0.38 thf(c_0_141, plain, ![X1053:mworld]:(((epred29_1 @ 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)=>(~(v15 @ X1046)|![X1045:mworld]:(((mrel @ X1046 @ X1045)=>![X1044:mworld]:(((mrel @ X1045 @ X1044)=>![X1043:mworld]:(((mrel @ X1044 @ X1043)=>![X1042:mworld]:(((mrel @ X1043 @ X1042)=>(~(v11 @ X1042)|![X1041:mworld]:(((mrel @ X1042 @ X1041)=>![X1040:mworld]:(((mrel @ X1041 @ X1040)=>![X1039:mworld]:(((mrel @ X1040 @ X1039)=>![X1038:mworld]:(((mrel @ X1039 @ X1038)=>(~(v7 @ X1038)|![X1037:mworld]:(((mrel @ X1038 @ X1037)=>![X1036:mworld]:(((mrel @ X1037 @ X1036)=>![X1035:mworld]:(((mrel @ X1036 @ X1035)=>![X1034:mworld]:(((mrel @ X1035 @ X1034)=>![X1033:mworld]:(((mrel @ X1034 @ X1033)=>![X1032:mworld]:(((mrel @ X1033 @ X1032)=>~(v1 @ X1032)))))))))))))))))))))))))))))))))))))))))))))))), inference(split_equiv,[status(thm)],[c_0_121])).
% 0.51/0.38 thf(c_0_142, plain, ![X1689:mworld, X1690:mworld, X1691:mworld, X1692:mworld, X1693:mworld, X1694:mworld, X1695:mworld]:((~(mrel @ mactual @ X1689)|(~(mrel @ X1689 @ X1690)|(~(mrel @ X1690 @ X1691)|(~(mrel @ X1691 @ X1692)|(~(mrel @ X1692 @ X1693)|(~(mrel @ X1693 @ X1694)|(~(mrel @ X1694 @ X1695)|(epred29_1 @ X1695))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_132])])])])).
% 0.51/0.38 thf(c_0_143, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v25 @ X3)|(v20 @ X5)|~((v8 @ X6))|~((v14 @ 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)],[c_0_133, c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_144, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((v8 @ X3)|(v1 @ X5)|(v25 @ X6))), inference(spm,[status(thm)],[c_0_134, c_0_129])).
% 0.51/0.38 thf(c_0_145, plain, ![X3:mworld, X5:mworld]:(((v1 @ X3)|~((v20 @ X5)))), 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)],[inference(rw,[status(thm)],[c_0_135, c_0_136]), c_0_137]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_146, 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 @ (esk19_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_38])).
% 0.51/0.38 thf(c_0_147, 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]:(((v25 @ X7)|(v16 @ X16)|(v11 @ X21)|~((mrel @ mactual @ 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))|~((mrel @ X14 @ X15))|~((mrel @ X15 @ X16))|~((mrel @ X16 @ X17))|~((mrel @ X17 @ X18))|~((mrel @ X18 @ X19))|~((mrel @ X19 @ X20))|~((mrel @ X20 @ X21)))), inference(split_conjunct,[status(thm)],[c_0_138])).
% 0.51/0.38 thf(c_0_148, plain, ![X581:mworld]:(((mrel @ mactual @ X581)=>![X580:mworld]:(((mrel @ X581 @ X580)=>(epred16_1 @ X580))))), 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)],[mod25, c_0_23]), c_0_24]), c_0_25]), c_0_26])]), c_0_139])).
% 0.51/0.38 thf(c_0_149, 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]:(((v25 @ X7)|(v13 @ X19)|~((mrel @ mactual @ 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))|~((mrel @ X14 @ X15))|~((mrel @ X15 @ X16))|~((mrel @ X16 @ X17))|~((mrel @ X17 @ X18))|~((mrel @ X18 @ X19))|~((mrel @ X19 @ X20))|~((v12 @ X20)))), inference(split_conjunct,[status(thm)],[c_0_140])).
% 0.51/0.38 thf(c_0_150, plain, ![X2426:mworld, X2427:mworld, X2428:mworld, X2429:mworld, X2430:mworld, X2431:mworld, X2432:mworld, X2433:mworld, X2434:mworld, X2435:mworld, X2436:mworld, X2437:mworld, X2438:mworld, X2439:mworld, X2440:mworld, X2441:mworld, X2442:mworld, X2443:mworld, X2444:mworld, X2445:mworld, X2446:mworld, X2447:mworld]:((~(epred29_1 @ X2426)|(~(mrel @ X2426 @ X2427)|(~(mrel @ X2427 @ X2428)|(~(mrel @ X2428 @ X2429)|(~(mrel @ X2429 @ X2430)|(~(mrel @ X2430 @ X2431)|(~(mrel @ X2431 @ X2432)|(~(mrel @ X2432 @ X2433)|(~(v15 @ X2433)|(~(mrel @ X2433 @ X2434)|(~(mrel @ X2434 @ X2435)|(~(mrel @ X2435 @ X2436)|(~(mrel @ X2436 @ X2437)|(~(v11 @ X2437)|(~(mrel @ X2437 @ X2438)|(~(mrel @ X2438 @ X2439)|(~(mrel @ X2439 @ X2440)|(~(mrel @ X2440 @ X2441)|(~(v7 @ X2441)|(~(mrel @ X2441 @ X2442)|(~(mrel @ X2442 @ X2443)|(~(mrel @ X2443 @ X2444)|(~(mrel @ X2444 @ X2445)|(~(mrel @ X2445 @ X2446)|(~(mrel @ X2446 @ X2447)|~(v1 @ X2447))))))))))))))))))))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_141])])])])).
% 0.51/0.38 thf(c_0_151, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld, X9:mworld, X10:mworld]:(((epred29_1 @ X10)|~((mrel @ mactual @ X3))|~((mrel @ X3 @ X5))|~((mrel @ X5 @ X6))|~((mrel @ X6 @ X7))|~((mrel @ X7 @ X8))|~((mrel @ X8 @ X9))|~((mrel @ X9 @ X10)))), inference(split_conjunct,[status(thm)],[c_0_142])).
% 0.51/0.38 thf(c_0_152, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v25 @ X3)|(v1 @ X5)|(v25 @ X6)|~((v14 @ X7)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_143, c_0_144]), c_0_145])).
% 0.51/0.38 thf(c_0_153, 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 @ (esk19_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_146, c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_154, 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_38])).
% 0.51/0.38 thf(c_0_155, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v25 @ X3)|(v16 @ X5)|(v11 @ X6)|~((v24 @ 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)],[c_0_147, c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_156, plain, ![X580:mworld]:(((epred16_1 @ X580)=>![X579:mworld]:(((mrel @ X580 @ X579)=>![X578:mworld]:(((mrel @ X579 @ X578)=>(~(v25 @ X578)|![X577:mworld]:(((mrel @ X578 @ X577)=>![X576:mworld]:(((mrel @ X577 @ X576)=>((v23 @ X576)|![X575:mworld]:(((mrel @ X576 @ X575)=>![X574:mworld]:(((mrel @ X575 @ X574)=>![X573:mworld]:(((mrel @ X574 @ X573)=>![X572:mworld]:(((mrel @ X573 @ X572)=>![X571:mworld]:(((mrel @ X572 @ X571)=>![X570:mworld]:(((mrel @ X571 @ X570)=>![X569:mworld]:(((mrel @ X570 @ X569)=>![X568:mworld]:(((mrel @ X569 @ X568)=>![X567:mworld]:(((mrel @ X568 @ X567)=>![X566:mworld]:(((mrel @ X567 @ X566)=>![X565:mworld]:(((mrel @ X566 @ X565)=>(~(v12 @ X565)|![X564:mworld]:(((mrel @ X565 @ X564)=>![X563:mworld]:(((mrel @ X564 @ X563)=>![X562:mworld]:(((mrel @ X563 @ X562)=>![X561:mworld]:(((mrel @ X562 @ X561)=>![X560:mworld]:(((mrel @ X561 @ X560)=>![X559:mworld]:(((mrel @ X560 @ X559)=>~(v6 @ X559)))))))))))))))))))))))))))))))))))))))))))))))), inference(split_equiv,[status(thm)],[c_0_139])).
% 0.51/0.38 thf(c_0_157, plain, ![X1492:mworld, X1493:mworld]:((~(mrel @ mactual @ X1492)|(~(mrel @ X1492 @ X1493)|(epred16_1 @ X1493)))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_148])])])])).
% 0.51/0.38 thf(c_0_158, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v25 @ X3)|(v13 @ X5)|~((v12 @ X6))|~((v24 @ 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)],[c_0_149, c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_159, plain, ![X558:mworld]:(((mrel @ mactual @ X558)=>![X557:mworld]:(((mrel @ X558 @ X557)=>![X556:mworld]:(((mrel @ X557 @ X556)=>![X555:mworld]:(((mrel @ X556 @ X555)=>(~(v25 @ X555)|![X554:mworld]:(((mrel @ X555 @ X554)=>(~(v24 @ X554)|![X553:mworld]:(((mrel @ X554 @ X553)=>![X552:mworld]:(((mrel @ X553 @ X552)=>![X551:mworld]:(((mrel @ X552 @ X551)=>![X550:mworld]:(((mrel @ X551 @ X550)=>![X549:mworld]:(((mrel @ X550 @ X549)=>((v19 @ X549)|![X548:mworld]:(((mrel @ X549 @ X548)=>![X547:mworld]:(((mrel @ X548 @ X547)=>![X546:mworld]:(((mrel @ X547 @ 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)=>~(v8 @ X538)))))))))))))))))))))))))))))))))))))))))))))), 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_23]), c_0_24]), c_0_25]), c_0_26])])).
% 0.51/0.38 thf(c_0_160, 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]:((~((epred29_1 @ X3))|~((mrel @ X3 @ X5))|~((mrel @ X5 @ X6))|~((mrel @ X6 @ X7))|~((mrel @ X7 @ X8))|~((mrel @ X8 @ X9))|~((mrel @ X9 @ X10))|~((mrel @ X10 @ X11))|~((v15 @ X11))|~((mrel @ X11 @ X12))|~((mrel @ X12 @ X13))|~((mrel @ X13 @ X14))|~((mrel @ X14 @ X15))|~((v11 @ X15))|~((mrel @ X15 @ X16))|~((mrel @ X16 @ X17))|~((mrel @ X17 @ X18))|~((mrel @ X18 @ X19))|~((v7 @ X19))|~((mrel @ X19 @ X20))|~((mrel @ X20 @ X21))|~((mrel @ X21 @ X22))|~((mrel @ X22 @ X23))|~((mrel @ X23 @ X24))|~((mrel @ X24 @ X25))|~((v1 @ X25)))), inference(split_conjunct,[status(thm)],[c_0_150])).
% 0.51/0.38 thf(c_0_161, plain, ![X3:mworld]:((epred29_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)],[inference(rw,[status(thm)],[c_0_151, c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_162, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((v25 @ X3)|(v1 @ X5)|(v25 @ X6))), inference(spm,[status(thm)],[c_0_152, c_0_153])).
% 0.51/0.38 thf(c_0_163, 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_154, c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_164, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((v11 @ X3)|(v16 @ X5)|(v25 @ X6))), inference(spm,[status(thm)],[c_0_155, c_0_129])).
% 0.51/0.38 thf(c_0_165, plain, ![X2137:mworld, X2138:mworld, X2139:mworld, X2140:mworld, X2141:mworld, X2142:mworld, X2143:mworld, X2144:mworld, X2145:mworld, X2146:mworld, X2147:mworld, X2148:mworld, X2149:mworld, X2150:mworld, X2151:mworld, X2152:mworld, X2153:mworld, X2154:mworld, X2155:mworld, X2156:mworld, X2157:mworld, X2158:mworld]:((~(epred16_1 @ X2137)|(~(mrel @ X2137 @ X2138)|(~(mrel @ X2138 @ X2139)|(~(v25 @ X2139)|(~(mrel @ X2139 @ X2140)|(~(mrel @ X2140 @ X2141)|((v23 @ X2141)|(~(mrel @ X2141 @ X2142)|(~(mrel @ X2142 @ X2143)|(~(mrel @ X2143 @ X2144)|(~(mrel @ X2144 @ X2145)|(~(mrel @ X2145 @ X2146)|(~(mrel @ X2146 @ X2147)|(~(mrel @ X2147 @ X2148)|(~(mrel @ X2148 @ X2149)|(~(mrel @ X2149 @ X2150)|(~(mrel @ X2150 @ X2151)|(~(mrel @ X2151 @ X2152)|(~(v12 @ X2152)|(~(mrel @ X2152 @ X2153)|(~(mrel @ X2153 @ X2154)|(~(mrel @ X2154 @ X2155)|(~(mrel @ X2155 @ X2156)|(~(mrel @ X2156 @ X2157)|(~(mrel @ X2157 @ X2158)|~(v6 @ X2158))))))))))))))))))))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_156])])])])).
% 0.51/0.38 thf(c_0_166, plain, ![X3:mworld, X5:mworld]:(((epred16_1 @ X5)|~((mrel @ mactual @ X3))|~((mrel @ X3 @ X5)))), inference(split_conjunct,[status(thm)],[c_0_157])).
% 0.51/0.38 thf(c_0_167, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v3 @ X3)|(v13 @ X5)|(v25 @ X6)|~((v24 @ X7)))), inference(spm,[status(thm)],[c_0_158, c_0_77])).
% 0.51/0.38 thf(c_0_168, plain, ![X820:mworld]:(((epred23_1 @ X820)<=>![X819:mworld]:(((mrel @ X820 @ X819)=>(~(v23 @ X819)|![X818:mworld]:(((mrel @ X819 @ X818)=>![X817:mworld]:(((mrel @ X818 @ X817)=>![X816:mworld]:(((mrel @ X817 @ X816)=>![X815:mworld]:(((mrel @ X816 @ X815)=>(~(v19 @ X815)|![X814:mworld]:(((mrel @ X815 @ X814)=>![X813:mworld]:(((mrel @ X814 @ X813)=>![X812:mworld]:(((mrel @ X813 @ X812)=>![X811:mworld]:(((mrel @ X812 @ X811)=>![X810:mworld]:(((mrel @ X811 @ X810)=>![X809:mworld]:(((mrel @ X810 @ X809)=>![X808:mworld]:(((mrel @ X809 @ X808)=>![X807:mworld]:(((mrel @ X808 @ X807)=>![X806:mworld]:(((mrel @ X807 @ X806)=>![X805:mworld]:(((mrel @ X806 @ X805)=>![X804:mworld]:(((mrel @ X805 @ X804)=>![X803:mworld]:(((mrel @ X804 @ X803)=>![X802:mworld]:(((mrel @ X803 @ X802)=>(~(v6 @ X802)|![X801:mworld]:(((mrel @ X802 @ X801)=>![X800:mworld]:(((mrel @ X801 @ X800)=>![X799:mworld]:(((mrel @ X800 @ X799)=>~(v3 @ X799)))))))))))))))))))))))))))))))))))))))))))))))), introduced(definition)).
% 0.51/0.38 thf(c_0_169, plain, ![X1471:mworld, X1472:mworld, X1473:mworld, X1474:mworld, X1475:mworld, X1476:mworld, X1477:mworld, X1478:mworld, X1479:mworld, X1480:mworld, X1481:mworld, X1482:mworld, X1483:mworld, X1484:mworld, X1485:mworld, X1486:mworld, X1487:mworld, X1488:mworld, X1489:mworld, X1490:mworld, X1491:mworld]:((~(mrel @ mactual @ X1471)|(~(mrel @ X1471 @ X1472)|(~(mrel @ X1472 @ X1473)|(~(mrel @ X1473 @ X1474)|(~(v25 @ X1474)|(~(mrel @ X1474 @ X1475)|(~(v24 @ X1475)|(~(mrel @ X1475 @ X1476)|(~(mrel @ X1476 @ X1477)|(~(mrel @ X1477 @ X1478)|(~(mrel @ X1478 @ X1479)|(~(mrel @ X1479 @ X1480)|((v19 @ X1480)|(~(mrel @ X1480 @ X1481)|(~(mrel @ X1481 @ X1482)|(~(mrel @ X1482 @ X1483)|(~(mrel @ X1483 @ X1484)|(~(mrel @ X1484 @ X1485)|(~(mrel @ X1485 @ X1486)|(~(mrel @ X1486 @ X1487)|(~(mrel @ X1487 @ X1488)|(~(mrel @ X1488 @ X1489)|(~(mrel @ X1489 @ X1490)|(~(mrel @ X1490 @ X1491)|~(v8 @ X1491)))))))))))))))))))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_159])])])])).
% 0.51/0.38 thf(c_0_170, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:((~((v1 @ X3))|~((v7 @ X5))|~((v11 @ 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)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_160, c_0_161]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_171, plain, ![X3:mworld, X5:mworld]:(((v25 @ X3)|(v1 @ X5))), inference(ef,[status(thm)],[c_0_162])).
% 0.51/0.38 thf(c_0_172, plain, ![X3:mworld, X5:mworld]:(((v25 @ X3)|(v11 @ X5))), inference(spm,[status(thm)],[c_0_163, c_0_164])).
% 0.51/0.38 thf(c_0_173, 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_38])).
% 0.51/0.38 thf(c_0_174, 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]:(((v23 @ X8)|~((epred16_1 @ X3))|~((mrel @ X3 @ X5))|~((mrel @ X5 @ X6))|~((v25 @ 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))|~((v12 @ X19))|~((mrel @ X19 @ X20))|~((mrel @ X20 @ X21))|~((mrel @ X21 @ X22))|~((mrel @ X22 @ X23))|~((mrel @ X23 @ X24))|~((mrel @ X24 @ X25))|~((v6 @ X25)))), inference(split_conjunct,[status(thm)],[c_0_165])).
% 0.51/0.38 thf(c_0_175, plain, ![X3:mworld]:((epred16_1 @ X3)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_166, c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_176, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((v25 @ X3)|(v13 @ X5)|(v3 @ X6))), inference(spm,[status(thm)],[c_0_167, c_0_129])).
% 0.51/0.38 thf(c_0_177, plain, ![X824:mworld]:(((mrel @ mactual @ X824)=>![X823:mworld]:(((mrel @ X824 @ X823)=>![X822:mworld]:(((mrel @ X823 @ X822)=>![X821:mworld]:(((mrel @ X822 @ X821)=>![X820:mworld]:(((mrel @ X821 @ X820)=>(epred23_1 @ X820))))))))))), 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)],[mod35, c_0_23]), c_0_24]), c_0_25]), c_0_26])]), c_0_168])).
% 0.51/0.38 thf(c_0_178, 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]:(((v19 @ X13)|~((mrel @ mactual @ X3))|~((mrel @ X3 @ X5))|~((mrel @ X5 @ X6))|~((mrel @ X6 @ X7))|~((v25 @ X7))|~((mrel @ X7 @ X8))|~((v24 @ 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))|~((v8 @ X24)))), inference(split_conjunct,[status(thm)],[c_0_169])).
% 0.51/0.38 thf(c_0_179, 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_38])).
% 0.51/0.38 thf(c_0_180, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((v25 @ X3)|~((v7 @ X5))|~((v15 @ X6)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_170, c_0_171]), c_0_172])).
% 0.51/0.38 thf(c_0_181, 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_173, c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_182, plain, ![X820:mworld]:(((epred23_1 @ X820)=>![X819:mworld]:(((mrel @ X820 @ X819)=>(~(v23 @ X819)|![X818:mworld]:(((mrel @ X819 @ X818)=>![X817:mworld]:(((mrel @ X818 @ X817)=>![X816:mworld]:(((mrel @ X817 @ X816)=>![X815:mworld]:(((mrel @ X816 @ X815)=>(~(v19 @ X815)|![X814:mworld]:(((mrel @ X815 @ X814)=>![X813:mworld]:(((mrel @ X814 @ X813)=>![X812:mworld]:(((mrel @ X813 @ X812)=>![X811:mworld]:(((mrel @ X812 @ X811)=>![X810:mworld]:(((mrel @ X811 @ X810)=>![X809:mworld]:(((mrel @ X810 @ X809)=>![X808:mworld]:(((mrel @ X809 @ X808)=>![X807:mworld]:(((mrel @ X808 @ X807)=>![X806:mworld]:(((mrel @ X807 @ X806)=>![X805:mworld]:(((mrel @ X806 @ X805)=>![X804:mworld]:(((mrel @ X805 @ X804)=>![X803:mworld]:(((mrel @ X804 @ X803)=>![X802:mworld]:(((mrel @ X803 @ X802)=>(~(v6 @ X802)|![X801:mworld]:(((mrel @ X802 @ X801)=>![X800:mworld]:(((mrel @ X801 @ X800)=>![X799:mworld]:(((mrel @ X800 @ X799)=>~(v3 @ X799)))))))))))))))))))))))))))))))))))))))))))))))), inference(split_equiv,[status(thm)],[c_0_168])).
% 0.51/0.38 thf(c_0_183, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((v23 @ X3)|~((v12 @ X5))|~((v25 @ X6)))), 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_174, c_0_136]), c_0_175]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_184, plain, ![X3:mworld, X5:mworld]:(((v3 @ X3)|(v25 @ X5))), inference(spm,[status(thm)],[c_0_82, c_0_176])).
% 0.51/0.38 thf(c_0_185, plain, ![X1582:mworld, X1583:mworld, X1584:mworld, X1585:mworld, X1586:mworld]:((~(mrel @ mactual @ X1582)|(~(mrel @ X1582 @ X1583)|(~(mrel @ X1583 @ X1584)|(~(mrel @ X1584 @ X1585)|(~(mrel @ X1585 @ X1586)|(epred23_1 @ X1586))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_177])])])])).
% 0.51/0.38 thf(c_0_186, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld]:(((v19 @ X3)|~((v8 @ X5))|~((v25 @ X6))|~((v24 @ 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)],[c_0_178, c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_187, 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_179, c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_188, plain, ![X3:mworld, X5:mworld]:(((v25 @ X3)|~((v15 @ X5)))), inference(spm,[status(thm)],[c_0_180, c_0_181])).
% 0.51/0.38 thf(c_0_189, plain, ![X2294:mworld, X2295:mworld, X2296:mworld, X2297:mworld, X2298:mworld, X2299:mworld, X2300:mworld, X2301:mworld, X2302:mworld, X2303:mworld, X2304:mworld, X2305:mworld, X2306:mworld, X2307:mworld, X2308:mworld, X2309:mworld, X2310:mworld, X2311:mworld, X2312:mworld, X2313:mworld, X2314:mworld, X2315:mworld]:((~(epred23_1 @ X2294)|(~(mrel @ X2294 @ X2295)|(~(v23 @ X2295)|(~(mrel @ X2295 @ X2296)|(~(mrel @ X2296 @ X2297)|(~(mrel @ X2297 @ X2298)|(~(mrel @ X2298 @ X2299)|(~(v19 @ X2299)|(~(mrel @ X2299 @ X2300)|(~(mrel @ X2300 @ X2301)|(~(mrel @ X2301 @ X2302)|(~(mrel @ X2302 @ X2303)|(~(mrel @ X2303 @ X2304)|(~(mrel @ X2304 @ X2305)|(~(mrel @ X2305 @ X2306)|(~(mrel @ X2306 @ X2307)|(~(mrel @ X2307 @ X2308)|(~(mrel @ X2308 @ X2309)|(~(mrel @ X2309 @ X2310)|(~(mrel @ X2310 @ X2311)|(~(mrel @ X2311 @ X2312)|(~(v6 @ X2312)|(~(mrel @ X2312 @ X2313)|(~(mrel @ X2313 @ X2314)|(~(mrel @ X2314 @ X2315)|~(v3 @ X2315))))))))))))))))))))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_182])])])])).
% 0.51/0.38 thf(c_0_190, plain, ![X3:mworld, X5:mworld]:(((v3 @ X3)|(v23 @ X5))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_183, c_0_77]), c_0_184])).
% 0.51/0.38 thf(c_0_191, plain, ![X3:mworld, X5:mworld, X6:mworld, X7:mworld, X8:mworld]:(((epred23_1 @ X8)|~((mrel @ mactual @ X3))|~((mrel @ X3 @ X5))|~((mrel @ X5 @ X6))|~((mrel @ X6 @ X7))|~((mrel @ X7 @ X8)))), inference(split_conjunct,[status(thm)],[c_0_185])).
% 0.51/0.38 thf(c_0_192, plain, ![X3:mworld, X5:mworld, X6:mworld]:(((v19 @ X3)|~((v25 @ X5))|~((v24 @ X6)))), inference(spm,[status(thm)],[c_0_186, c_0_187])).
% 0.51/0.38 thf(c_0_193, plain, ![X3:mworld]:((v25 @ X3)), inference(spm,[status(thm)],[c_0_188, c_0_58])).
% 0.51/0.38 thf(c_0_194, 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]:((~((epred23_1 @ X3))|~((mrel @ X3 @ X5))|~((v23 @ X5))|~((mrel @ X5 @ X6))|~((mrel @ X6 @ X7))|~((mrel @ X7 @ X8))|~((mrel @ X8 @ X9))|~((v19 @ 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))|~((v6 @ X22))|~((mrel @ X22 @ X23))|~((mrel @ X23 @ X24))|~((mrel @ X24 @ X25))|~((v3 @ X25)))), inference(split_conjunct,[status(thm)],[c_0_189])).
% 0.51/0.38 thf(c_0_195, plain, ![X3:mworld]:((v3 @ X3)), inference(spm,[status(thm)],[c_0_48, c_0_190])).
% 0.51/0.38 thf(c_0_196, plain, ![X3:mworld]:((epred23_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_191, c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_197, plain, ![X3:mworld, X5:mworld]:(((v19 @ X3)|~((v24 @ X5)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_192, c_0_193])])).
% 0.51/0.38 thf(c_0_198, plain, ![X3:mworld, X5:mworld]:((~((v19 @ X3))|~((v23 @ X5)))), 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)],[inference(rw,[status(thm)],[c_0_194, c_0_195]), c_0_136]), c_0_196]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37]), c_0_37])])).
% 0.51/0.38 thf(c_0_199, plain, ![X3:mworld]:((v19 @ X3)), inference(spm,[status(thm)],[c_0_197, c_0_129])).
% 0.51/0.38 thf(c_0_200, plain, ![X3:mworld]:(~((v23 @ X3))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_198, c_0_199])])).
% 0.51/0.38 thf(c_0_201, plain, ($false), inference(sr,[status(thm)],[c_0_90, c_0_200]), ['proof']).
% 0.51/0.38 % SZS output end CNFRefutation
% 0.51/0.38 % Parsed axioms : 100
% 0.51/0.38 % Removed by relevancy pruning/SinE : 0
% 0.51/0.38 % Initial clauses : 205
% 0.51/0.38 % Removed in clause preprocessing : 56
% 0.51/0.38 % Initial clauses in saturation : 149
% 0.51/0.38 % Processed clauses : 292
% 0.51/0.38 % ...of these trivial : 32
% 0.51/0.38 % ...subsumed : 6
% 0.51/0.38 % ...remaining for further processing : 254
% 0.51/0.38 % Other redundant clauses eliminated : 0
% 0.51/0.38 % Clauses deleted for lack of memory : 0
% 0.51/0.38 % Backward-subsumed : 123
% 0.51/0.38 % Backward-rewritten : 54
% 0.51/0.38 % Generated clauses : 294
% 0.51/0.38 % ...of the previous two non-redundant : 312
% 0.51/0.38 % ...aggressively subsumed : 0
% 0.51/0.38 % Contextual simplify-reflections : 5
% 0.51/0.38 % Paramodulations : 283
% 0.51/0.38 % Factorizations : 10
% 0.51/0.38 % NegExts : 0
% 0.51/0.38 % Equation resolutions : 0
% 0.51/0.38 % Disequality decompositions : 0
% 0.51/0.38 % Total rewrite steps : 1829
% 0.51/0.38 % ...of those cached : 1693
% 0.51/0.38 % Propositional unsat checks : 0
% 0.51/0.38 % Propositional check models : 0
% 0.51/0.38 % Propositional check unsatisfiable : 0
% 0.51/0.38 % Propositional clauses : 0
% 0.51/0.38 % Propositional clauses after purity: 0
% 0.51/0.38 % Propositional unsat core size : 0
% 0.51/0.38 % Propositional preprocessing time : 0.000
% 0.51/0.38 % Propositional encoding time : 0.000
% 0.51/0.38 % Propositional solver time : 0.000
% 0.51/0.38 % Success case prop preproc time : 0.000
% 0.51/0.38 % Success case prop encoding time : 0.000
% 0.51/0.38 % Success case prop solver time : 0.000
% 0.51/0.38 % Current number of processed clauses : 76
% 0.51/0.38 % Positive orientable unit clauses : 46
% 0.51/0.38 % Positive unorientable unit clauses: 0
% 0.51/0.38 % Negative unit clauses : 9
% 0.51/0.38 % Non-unit-clauses : 21
% 0.51/0.38 % Current number of unprocessed clauses: 56
% 0.51/0.38 % ...number of literals in the above : 512
% 0.51/0.38 % Current number of archived formulas : 0
% 0.51/0.38 % Current number of archived clauses : 178
% 0.51/0.38 % Clause-clause subsumption calls (NU) : 5199
% 0.51/0.38 % Rec. Clause-clause subsumption calls : 2602
% 0.51/0.38 % Non-unit clause-clause subsumptions : 96
% 0.51/0.38 % Unit Clause-clause subsumption calls : 470
% 0.51/0.38 % Rewrite failures with RHS unbound : 0
% 0.51/0.38 % BW rewrite match attempts : 35
% 0.51/0.38 % BW rewrite match successes : 35
% 0.51/0.38 % Condensation attempts : 0
% 0.51/0.38 % Condensation successes : 0
% 0.51/0.38 % Termbank termtop insertions : 105225
% 0.51/0.38 % Search garbage collected termcells : 49415
% 0.51/0.38
% 0.51/0.38 % -------------------------------------------------
% 0.51/0.38 % User time : 0.089 s
% 0.51/0.38 % System time : 0.019 s
% 0.51/0.38 % Total time : 0.108 s
% 0.51/0.38 % Maximum resident set size: 11036 pages
% 0.51/0.38
% 0.51/0.38 % -------------------------------------------------
% 0.51/0.38 % User time : 0.111 s
% 0.51/0.38 % System time : 0.038 s
% 0.51/0.38 % Total time : 0.149 s
% 0.51/0.38 % Maximum resident set size: 5120 pages
% 0.51/0.38 % E exiting
%------------------------------------------------------------------------------