%------------------------------------------------------------------------------
% File : E-SAT---3.5.1
% Problem : SEV040^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:35:51 AM UTC 2026
% Result : Theorem 5.19s 1.03s
% Output : CNFRefutation 5.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV040^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 % Computer : n003.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Tue Sep 29 15:06:35 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.24 Running higher-order theorem proving
% 0.08/0.26 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.eNnXat6knI/E---3.1_2620548.p
% 5.19/1.03 % Version: 3.5.1-ho
% 5.19/1.03 % Preprocessing class: HSMSSMSSSSSNHHA.
% 5.19/1.03 % Scheduled 6 strats onto 8 cores with 300 seconds (2400 total)
% 5.19/1.03 % Starting full_lambda_6 with 900s (3) cores
% 5.19/1.03 % Starting post_as_ho1 with 300s (1) cores
% 5.19/1.03 % Starting lpo6_lambda_fix with 300s (1) cores
% 5.19/1.03 % Starting ho_unfolding_1 with 300s (1) cores
% 5.19/1.03 % Starting new_ho_10_unif with 300s (1) cores
% 5.19/1.03 % Starting ho_unfolding_2 with 300s (1) cores
% 5.19/1.03 % full_lambda_6 with pid 2620561 completed with status 0
% 5.19/1.03 % Result found by full_lambda_6
% 5.19/1.03 % Preprocessing class: HSMSSMSSSSSNHHA.
% 5.19/1.03 % Scheduled 6 strats onto 8 cores with 300 seconds (2400 total)
% 5.19/1.03 % Starting full_lambda_6 with 900s (3) cores
% 5.19/1.03 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 1, sine = GSinE(CountTerms,hypos,4,,4,20000,1.0,true))
% 5.19/1.03 % SinE strategy is GSinE(CountTerms,hypos,4,,4,20000,1.0,true)
% 5.19/1.03 % Search class: HGUSF-FSMF00-SHHFFFBN
% 5.19/1.03 % partial match(3): HGUNF-FFMF00-SHHFFMBN
% 5.19/1.03 % Scheduled 7 strats onto 3 cores with 900 seconds (900 total)
% 5.19/1.03 % Starting SubtermCWHack with 82s (1) cores
% 5.19/1.03 % Starting full_lambda_6 with 91s (1) cores
% 5.19/1.03 % Starting sh3 with 163s (1) cores
% 5.19/1.03 % full_lambda_6 with pid 2620568 completed with status 0
% 5.19/1.03 % Result found by full_lambda_6
% 5.19/1.03 % Preprocessing class: HSMSSMSSSSSNHHA.
% 5.19/1.03 % Scheduled 6 strats onto 8 cores with 300 seconds (2400 total)
% 5.19/1.03 % Starting full_lambda_6 with 900s (3) cores
% 5.19/1.03 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 1, sine = GSinE(CountTerms,hypos,4,,4,20000,1.0,true))
% 5.19/1.03 % SinE strategy is GSinE(CountTerms,hypos,4,,4,20000,1.0,true)
% 5.19/1.03 % Search class: HGUSF-FSMF00-SHHFFFBN
% 5.19/1.03 % partial match(3): HGUNF-FFMF00-SHHFFMBN
% 5.19/1.03 % Scheduled 7 strats onto 3 cores with 900 seconds (900 total)
% 5.19/1.03 % Starting SubtermCWHack with 82s (1) cores
% 5.19/1.03 % Starting full_lambda_6 with 91s (1) cores
% 5.19/1.03 % Preprocessing time : 0.002 s
% 5.19/1.03 % Presaturation interreduction done
% 5.19/1.03
% 5.19/1.03 % Proof found!
% 5.19/1.03 % SZS status Theorem
% 5.19/1.03 % SZS output start CNFRefutation
% 5.19/1.03 thf(decl_sort1, type, a: $tType).
% 5.19/1.03 thf(decl_23, type, epred1_3: (a > a > $o) > (a > a > $o) > (a > a > $o) > $o).
% 5.19/1.03 thf(decl_24, type, epred2_0: $o).
% 5.19/1.03 thf(decl_25, type, epred3_0: a > a > $o).
% 5.19/1.03 thf(decl_26, type, epred4_0: a > a > $o).
% 5.19/1.03 thf(decl_27, type, esk1_0: a).
% 5.19/1.03 thf(decl_28, type, esk2_0: a).
% 5.19/1.03 thf(decl_29, type, esk3_0: a).
% 5.19/1.03 thf(decl_30, type, esk4_0: a).
% 5.19/1.03 thf(decl_31, type, esk5_0: a).
% 5.19/1.03 thf(decl_32, type, epred5_0: a > a > $o).
% 5.19/1.03 thf(decl_33, type, epred6_0: a > a > $o).
% 5.19/1.03 thf(decl_34, type, epred7_0: a > a > $o).
% 5.19/1.03 thf(decl_35, type, esk6_0: a).
% 5.19/1.03 thf(decl_36, type, esk7_0: a).
% 5.19/1.03 thf(decl_37, type, esk8_0: a).
% 5.19/1.03 thf(decl_38, type, esk9_0: a).
% 5.19/1.03 thf(decl_39, type, esk10_0: a).
% 5.19/1.03 thf(decl_40, type, esk11_0: a).
% 5.19/1.03 thf(decl_41, type, esk12_0: a).
% 5.19/1.03 thf(decl_42, type, esk13_0: a).
% 5.19/1.03 thf(decl_43, type, esk14_0: a).
% 5.19/1.03 thf(decl_48, type, esk19_0: a).
% 5.19/1.03 thf(decl_49, type, esk20_0: a).
% 5.19/1.03 thf(decl_50, type, esk21_0: a).
% 5.19/1.03 thf(decl_51, type, esk22_0: a).
% 5.19/1.03 thf(decl_52, type, esk23_0: a).
% 5.19/1.03 thf(decl_53, type, esk24_0: a).
% 5.19/1.03 thf(decl_68, type, esk39_0: a).
% 5.19/1.03 thf(decl_69, type, esk40_0: a).
% 5.19/1.03 thf(decl_70, type, esk41_0: a).
% 5.19/1.03 thf(decl_71, type, esk42_0: a).
% 5.19/1.03 thf(decl_72, type, esk43_0: a).
% 5.19/1.03 thf(decl_73, type, esk44_0: a).
% 5.19/1.03 thf(decl_80, type, esk51_0: a).
% 5.19/1.03 thf(decl_81, type, esk52_0: a).
% 5.19/1.03 thf(decl_82, type, esk53_0: a).
% 5.19/1.03 thf(decl_83, type, esk54_0: a).
% 5.19/1.03 thf(decl_92, type, esk63_0: a).
% 5.19/1.03 thf(decl_93, type, esk64_0: a).
% 5.19/1.03 thf(decl_94, type, esk65_0: a).
% 5.19/1.03 thf(decl_95, type, esk66_0: a).
% 5.19/1.03 thf(decl_102, type, esk73_0: a).
% 5.19/1.03 thf(decl_103, type, esk74_0: a).
% 5.19/1.03 thf(decl_104, type, esk75_0: a).
% 5.19/1.03 thf(decl_105, type, esk76_0: a).
% 5.19/1.03 thf(decl_106, type, esk77_0: a).
% 5.19/1.03 thf(decl_107, type, esk78_0: a).
% 5.19/1.03 thf(decl_110, type, esk81_0: a).
% 5.19/1.03 thf(decl_111, type, esk82_0: a).
% 5.19/1.03 thf(cTHM515_pme, conjecture, ((![X1:a > a > $o, X2:a > a > $o]:((((![X3:a, X4:a]:(((X1 @ X3 @ X4)=>(X1 @ X4 @ X3)))&![X3:a, X4:a, X5:a]:((((X1 @ X3 @ X4)&(X1 @ X4 @ X5))=>(X1 @ X3 @ X5))))&((X1)=(X2)))=>((![X3:a, X4:a]:(((X2 @ X3 @ X4)=>(X2 @ X4 @ X3)))&![X3:a, X4:a, X5:a]:((((X2 @ X3 @ X4)&(X2 @ X4 @ X5))=>(X2 @ X3 @ X5))))&((X2)=(X1)))))&![X1:a > a > $o, X2:a > a > $o, X6:a > a > $o]:(((((((![X3:a, X4:a]:(((X1 @ X3 @ X4)=>(X1 @ X4 @ X3)))&![X3:a, X4:a, X7:a]:((((X1 @ X3 @ X4)&(X1 @ X4 @ X7))=>(X1 @ X3 @ X7))))&((X1)=(X2)))&![X3:a, X4:a]:(((X2 @ X3 @ X4)=>(X2 @ X4 @ X3))))&![X3:a, X4:a, X7:a]:((((X2 @ X3 @ X4)&(X2 @ X4 @ X7))=>(X2 @ X3 @ X7))))&((X2)=(X6)))=>((![X3:a, X4:a]:(((X1 @ X3 @ X4)=>(X1 @ X4 @ X3)))&![X3:a, X4:a, X7:a]:((((X1 @ X3 @ X4)&(X1 @ X4 @ X7))=>(X1 @ X3 @ X7))))&((X1)=(X6))))))&((^[X8:a > a > $o, X9:a > a > $o]:(((((![X10:a, X11:a]:((((X8 @ X10 @ X11))=>((X8 @ X11 @ X10)))))&(![X12:a, X13:a, X5:a]:((((((X8 @ X12 @ X13))&((X8 @ X13 @ X5))))=>((X8 @ X12 @ X5)))))))&(((X8)=(X9))))))=(^[X8:a > a > $o, X9:a > a > $o]:(((((![X14:a, X15:a]:((((X8 @ X14 @ X15))=>((X8 @ X15 @ X14)))))&(![X16:a, X17:a, X5:a]:((((((X8 @ X16 @ X17))&((X8 @ X17 @ X5))))=>((X8 @ X16 @ X5)))))))&(((X8)=(X9)))))))), file('/export/starexec/sandbox2/tmp/tmp.eNnXat6knI/E---3.1_2620548.p', cTHM515_pme)).
% 5.19/1.03 thf(c_0_1, negated_conjecture, ~(((![X1:a > a > $o, X2:a > a > $o]:((((![X3:a, X4:a]:(((X1 @ X3 @ X4)=>(X1 @ X4 @ X3)))&![X3:a, X4:a, X5:a]:((((X1 @ X3 @ X4)&(X1 @ X4 @ X5))=>(X1 @ X3 @ X5))))&((X1)=(X2)))=>((![X3:a, X4:a]:(((X2 @ X3 @ X4)=>(X2 @ X4 @ X3)))&![X3:a, X4:a, X5:a]:((((X2 @ X3 @ X4)&(X2 @ X4 @ X5))=>(X2 @ X3 @ X5))))&((X2)=(X1)))))&![X1:a > a > $o, X2:a > a > $o, X6:a > a > $o]:(((((((![X3:a, X4:a]:(((X1 @ X3 @ X4)=>(X1 @ X4 @ X3)))&![X3:a, X4:a, X7:a]:((((X1 @ X3 @ X4)&(X1 @ X4 @ X7))=>(X1 @ X3 @ X7))))&((X1)=(X2)))&![X3:a, X4:a]:(((X2 @ X3 @ X4)=>(X2 @ X4 @ X3))))&![X3:a, X4:a, X7:a]:((((X2 @ X3 @ X4)&(X2 @ X4 @ X7))=>(X2 @ X3 @ X7))))&((X2)=(X6)))=>((![X3:a, X4:a]:(((X1 @ X3 @ X4)=>(X1 @ X4 @ X3)))&![X3:a, X4:a, X7:a]:((((X1 @ X3 @ X4)&(X1 @ X4 @ X7))=>(X1 @ X3 @ X7))))&((X1)=(X6))))))&((^[X8:a > a > $o, X9:a > a > $o]:(((((![X10:a, X11:a]:((((X8 @ X10 @ X11))=>((X8 @ X11 @ X10)))))&(![X12:a, X13:a, X5:a]:((((((X8 @ X12 @ X13))&((X8 @ X13 @ X5))))=>((X8 @ X12 @ X5)))))))&(((X8)=(X9))))))=(^[X8:a > a > $o, X9:a > a > $o]:(((((![X14:a, X15:a]:((((X8 @ X14 @ X15))=>((X8 @ X15 @ X14)))))&(![X16:a, X17:a, X5:a]:((((((X8 @ X16 @ X17))&((X8 @ X17 @ X5))))=>((X8 @ X16 @ X5)))))))&(((X8)=(X9))))))))), inference(assume_negation,[status(cth)],[cTHM515_pme])).
% 5.19/1.03 thf(c_0_2, plain, ((epred2_0)<=>(![X1:a > a > $o, X2:a > a > $o]:((((![X3:a, X4:a]:(((X1 @ X3 @ X4)=>(X1 @ X4 @ X3)))&![X3:a, X4:a, X5:a]:((((X1 @ X3 @ X4)&(X1 @ X4 @ X5))=>(X1 @ X3 @ X5))))&((X1)=(X2)))=>((![X3:a, X4:a]:(((X2 @ X3 @ X4)=>(X2 @ X4 @ X3)))&![X3:a, X4:a, X5:a]:((((X2 @ X3 @ X4)&(X2 @ X4 @ X5))=>(X2 @ X3 @ X5))))&((X2)=(X1)))))&![X1:a > a > $o, X2:a > a > $o, X6:a > a > $o]:(((((((![X3:a, X4:a]:(((X1 @ X3 @ X4)=>(X1 @ X4 @ X3)))&![X3:a, X4:a, X7:a]:((((X1 @ X3 @ X4)&(X1 @ X4 @ X7))=>(X1 @ X3 @ X7))))&((X1)=(X2)))&![X3:a, X4:a]:(((X2 @ X3 @ X4)=>(X2 @ X4 @ X3))))&![X3:a, X4:a, X7:a]:((((X2 @ X3 @ X4)&(X2 @ X4 @ X7))=>(X2 @ X3 @ X7))))&((X2)=(X6)))=>((![X3:a, X4:a]:(((X1 @ X3 @ X4)=>(X1 @ X4 @ X3)))&![X3:a, X4:a, X7:a]:((((X1 @ X3 @ X4)&(X1 @ X4 @ X7))=>(X1 @ X3 @ X7))))&((X1)=(X6))))))), introduced(definition)).
% 5.19/1.03 thf(c_0_3, plain, ![X1:a > a > $o, X2:a > a > $o, X6:a > a > $o]:(((epred1_3 @ X6 @ X2 @ X1)<=>(((((![X3:a, X4:a]:(((X1 @ X3 @ X4)=>(X1 @ X4 @ X3)))&![X3:a, X4:a, X7:a]:((((X1 @ X3 @ X4)&(X1 @ X4 @ X7))=>(X1 @ X3 @ X7))))&((X1)=(X2)))&![X3:a, X4:a]:(((X2 @ X3 @ X4)=>(X2 @ X4 @ X3))))&![X3:a, X4:a, X7:a]:((((X2 @ X3 @ X4)&(X2 @ X4 @ X7))=>(X2 @ X3 @ X7))))&((X2)=(X6))))), introduced(definition)).
% 5.19/1.03 thf(c_0_4, negated_conjecture, ~(((epred2_0)&((^[Z0:a > a > $o, Z1:a > a > $o]:(((((![X10:a, X11:a]:(((Z0 @ X10 @ X11)=>(Z0 @ X11 @ X10))))&(![X12:a, X13:a, X5:a]:(((((Z0 @ X12 @ X13)&(Z0 @ X13 @ X5)))=>(Z0 @ X12 @ X5))))))&(((Z0)=(Z1))))))=(^[Z0:a > a > $o, Z1:a > a > $o]:(((((![X14:a, X15:a]:(((Z0 @ X14 @ X15)=>(Z0 @ X15 @ X14))))&(![X16:a, X17:a, X5:a]:(((((Z0 @ X16 @ X17)&(Z0 @ X17 @ X5)))=>(Z0 @ X16 @ X5))))))&(((Z0)=(Z1))))))))), inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_1]), c_0_2])).
% 5.19/1.03 thf(c_0_5, plain, ((![X1:a > a > $o, X2:a > a > $o]:((((![X3:a, X4:a]:(((X1 @ X3 @ X4)=>(X1 @ X4 @ X3)))&![X3:a, X4:a, X5:a]:((((X1 @ X3 @ X4)&(X1 @ X4 @ X5))=>(X1 @ X3 @ X5))))&((X1)=(X2)))=>((![X3:a, X4:a]:(((X2 @ X3 @ X4)=>(X2 @ X4 @ X3)))&![X3:a, X4:a, X5:a]:((((X2 @ X3 @ X4)&(X2 @ X4 @ X5))=>(X2 @ X3 @ X5))))&((X2)=(X1)))))&![X1:a > a > $o, X2:a > a > $o, X6:a > a > $o]:(((epred1_3 @ X6 @ X2 @ X1)=>((![X3:a, X4:a]:(((X1 @ X3 @ X4)=>(X1 @ X4 @ X3)))&![X3:a, X4:a, X7:a]:((((X1 @ X3 @ X4)&(X1 @ X4 @ X7))=>(X1 @ X3 @ X7))))&((X1)=(X6))))))=>(epred2_0)), inference(apply_def,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_2]), c_0_3])).
% 5.19/1.03 thf(c_0_6, negated_conjecture, (~(epred2_0)|((^[Z0:a > a > $o, Z1:a > a > $o]:(((((![X10:a, X11:a]:(((Z0 @ X10 @ X11)=>(Z0 @ X11 @ X10))))&(![X12:a, X13:a, X5:a]:(((((Z0 @ X12 @ X13)&(Z0 @ X13 @ X5)))=>(Z0 @ X12 @ X5))))))&(((Z0)=(Z1))))))!=(^[Z0:a > a > $o, Z1:a > a > $o]:(((((![X14:a, X15:a]:(((Z0 @ X14 @ X15)=>(Z0 @ X15 @ X14))))&(![X16:a, X17:a, X5:a]:(((((Z0 @ X16 @ X17)&(Z0 @ X17 @ X5)))=>(Z0 @ X16 @ X5))))))&(((Z0)=(Z1)))))))), inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_4])])).
% 5.19/1.03 thf(c_0_7, plain, ![X1:a > a > $o, X2:a > a > $o, X6:a > a > $o]:(((epred1_3 @ X6 @ X2 @ X1)=>(((((![X3:a, X4:a]:(((X1 @ X3 @ X4)=>(X1 @ X4 @ X3)))&![X3:a, X4:a, X7:a]:((((X1 @ X3 @ X4)&(X1 @ X4 @ X7))=>(X1 @ X3 @ X7))))&((X1)=(X2)))&![X3:a, X4:a]:(((X2 @ X3 @ X4)=>(X2 @ X4 @ X3))))&![X3:a, X4:a, X7:a]:((((X2 @ X3 @ X4)&(X2 @ X4 @ X7))=>(X2 @ X3 @ X7))))&((X2)=(X6))))), inference(split_equiv,[status(thm)],[c_0_3])).
% 5.19/1.03 thf(c_0_8, plain, ![X63:a, X64:a, X65:a, X66:a, X67:a]:(((((((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|(~(epred3_0 @ X63 @ X64)|(epred3_0 @ X64 @ X63))|(epred2_0))&(((((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred5_0)!=(epred7_0))|(~(epred3_0 @ X63 @ X64)|(epred3_0 @ X64 @ X63))|(epred2_0))&((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred5_0)!=(epred7_0))|(~(epred3_0 @ X63 @ X64)|(epred3_0 @ X64 @ X63))|(epred2_0)))&(~(epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred5_0)!=(epred7_0))|(~(epred3_0 @ X63 @ X64)|(epred3_0 @ X64 @ X63))|(epred2_0)))&((((epred5_0 @ esk8_0 @ esk9_0)|~(epred5_0 @ esk7_0 @ esk6_0)|((epred5_0)!=(epred7_0))|(~(epred3_0 @ X63 @ X64)|(epred3_0 @ X64 @ X63))|(epred2_0))&((epred5_0 @ esk9_0 @ esk10_0)|~(epred5_0 @ esk7_0 @ esk6_0)|((epred5_0)!=(epred7_0))|(~(epred3_0 @ X63 @ X64)|(epred3_0 @ X64 @ X63))|(epred2_0)))&(~(epred5_0 @ esk8_0 @ esk10_0)|~(epred5_0 @ esk7_0 @ esk6_0)|((epred5_0)!=(epred7_0))|(~(epred3_0 @ X63 @ X64)|(epred3_0 @ X64 @ X63))|(epred2_0)))))&(((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|(~(epred3_0 @ X65 @ X66)|~(epred3_0 @ X66 @ X67)|(epred3_0 @ X65 @ X67))|(epred2_0))&(((((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred5_0)!=(epred7_0))|(~(epred3_0 @ X65 @ X66)|~(epred3_0 @ X66 @ X67)|(epred3_0 @ X65 @ X67))|(epred2_0))&((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred5_0)!=(epred7_0))|(~(epred3_0 @ X65 @ X66)|~(epred3_0 @ X66 @ X67)|(epred3_0 @ X65 @ X67))|(epred2_0)))&(~(epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred5_0)!=(epred7_0))|(~(epred3_0 @ X65 @ X66)|~(epred3_0 @ X66 @ X67)|(epred3_0 @ X65 @ X67))|(epred2_0)))&((((epred5_0 @ esk8_0 @ esk9_0)|~(epred5_0 @ esk7_0 @ esk6_0)|((epred5_0)!=(epred7_0))|(~(epred3_0 @ X65 @ X66)|~(epred3_0 @ X66 @ X67)|(epred3_0 @ X65 @ X67))|(epred2_0))&((epred5_0 @ esk9_0 @ esk10_0)|~(epred5_0 @ esk7_0 @ esk6_0)|((epred5_0)!=(epred7_0))|(~(epred3_0 @ X65 @ X66)|~(epred3_0 @ X66 @ X67)|(epred3_0 @ X65 @ X67))|(epred2_0)))&(~(epred5_0 @ esk8_0 @ esk10_0)|~(epred5_0 @ esk7_0 @ esk6_0)|((epred5_0)!=(epred7_0))|(~(epred3_0 @ X65 @ X66)|~(epred3_0 @ X66 @ X67)|(epred3_0 @ X65 @ X67))|(epred2_0))))))&(((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|((epred3_0)=(epred4_0))|(epred2_0))&(((((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred5_0)!=(epred7_0))|((epred3_0)=(epred4_0))|(epred2_0))&((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred5_0)!=(epred7_0))|((epred3_0)=(epred4_0))|(epred2_0)))&(~(epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred5_0)!=(epred7_0))|((epred3_0)=(epred4_0))|(epred2_0)))&((((epred5_0 @ esk8_0 @ esk9_0)|~(epred5_0 @ esk7_0 @ esk6_0)|((epred5_0)!=(epred7_0))|((epred3_0)=(epred4_0))|(epred2_0))&((epred5_0 @ esk9_0 @ esk10_0)|~(epred5_0 @ esk7_0 @ esk6_0)|((epred5_0)!=(epred7_0))|((epred3_0)=(epred4_0))|(epred2_0)))&(~(epred5_0 @ esk8_0 @ esk10_0)|~(epred5_0 @ esk7_0 @ esk6_0)|((epred5_0)!=(epred7_0))|((epred3_0)=(epred4_0))|(epred2_0))))))&((((((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|((epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred4_0)!=(epred3_0)))|(epred2_0))&(((((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred5_0)!=(epred7_0))|((epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred4_0)!=(epred3_0)))|(epred2_0))&((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred5_0)!=(epred7_0))|((epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred4_0)!=(epred3_0)))|(epred2_0)))&(~(epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred5_0)!=(epred7_0))|((epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred4_0)!=(epred3_0)))|(epred2_0)))&((((epred5_0 @ esk8_0 @ esk9_0)|~(epred5_0 @ esk7_0 @ esk6_0)|((epred5_0)!=(epred7_0))|((epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred4_0)!=(epred3_0)))|(epred2_0))&((epred5_0 @ esk9_0 @ esk10_0)|~(epred5_0 @ esk7_0 @ esk6_0)|((epred5_0)!=(epred7_0))|((epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred4_0)!=(epred3_0)))|(epred2_0)))&(~(epred5_0 @ esk8_0 @ esk10_0)|~(epred5_0 @ esk7_0 @ esk6_0)|((epred5_0)!=(epred7_0))|((epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred4_0)!=(epred3_0)))|(epred2_0)))))&(((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|((epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred4_0)!=(epred3_0)))|(epred2_0))&(((((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred5_0)!=(epred7_0))|((epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred4_0)!=(epred3_0)))|(epred2_0))&((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred5_0)!=(epred7_0))|((epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred4_0)!=(epred3_0)))|(epred2_0)))&(~(epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred5_0)!=(epred7_0))|((epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred4_0)!=(epred3_0)))|(epred2_0)))&((((epred5_0 @ esk8_0 @ esk9_0)|~(epred5_0 @ esk7_0 @ esk6_0)|((epred5_0)!=(epred7_0))|((epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred4_0)!=(epred3_0)))|(epred2_0))&((epred5_0 @ esk9_0 @ esk10_0)|~(epred5_0 @ esk7_0 @ esk6_0)|((epred5_0)!=(epred7_0))|((epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred4_0)!=(epred3_0)))|(epred2_0)))&(~(epred5_0 @ esk8_0 @ esk10_0)|~(epred5_0 @ esk7_0 @ esk6_0)|((epred5_0)!=(epred7_0))|((epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred4_0)!=(epred3_0)))|(epred2_0))))))&(((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|(~(epred4_0 @ esk3_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred4_0)!=(epred3_0)))|(epred2_0))&(((((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred5_0)!=(epred7_0))|(~(epred4_0 @ esk3_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred4_0)!=(epred3_0)))|(epred2_0))&((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred5_0)!=(epred7_0))|(~(epred4_0 @ esk3_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred4_0)!=(epred3_0)))|(epred2_0)))&(~(epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred5_0)!=(epred7_0))|(~(epred4_0 @ esk3_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred4_0)!=(epred3_0)))|(epred2_0)))&((((epred5_0 @ esk8_0 @ esk9_0)|~(epred5_0 @ esk7_0 @ esk6_0)|((epred5_0)!=(epred7_0))|(~(epred4_0 @ esk3_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred4_0)!=(epred3_0)))|(epred2_0))&((epred5_0 @ esk9_0 @ esk10_0)|~(epred5_0 @ esk7_0 @ esk6_0)|((epred5_0)!=(epred7_0))|(~(epred4_0 @ esk3_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred4_0)!=(epred3_0)))|(epred2_0)))&(~(epred5_0 @ esk8_0 @ esk10_0)|~(epred5_0 @ esk7_0 @ esk6_0)|((epred5_0)!=(epred7_0))|(~(epred4_0 @ esk3_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred4_0)!=(epred3_0)))|(epred2_0))))))&(((((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|((epred4_0 @ esk3_0 @ esk4_0)|~(epred4_0 @ esk2_0 @ esk1_0)|((epred4_0)!=(epred3_0)))|(epred2_0))&(((((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred5_0)!=(epred7_0))|((epred4_0 @ esk3_0 @ esk4_0)|~(epred4_0 @ esk2_0 @ esk1_0)|((epred4_0)!=(epred3_0)))|(epred2_0))&((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred5_0)!=(epred7_0))|((epred4_0 @ esk3_0 @ esk4_0)|~(epred4_0 @ esk2_0 @ esk1_0)|((epred4_0)!=(epred3_0)))|(epred2_0)))&(~(epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred5_0)!=(epred7_0))|((epred4_0 @ esk3_0 @ esk4_0)|~(epred4_0 @ esk2_0 @ esk1_0)|((epred4_0)!=(epred3_0)))|(epred2_0)))&((((epred5_0 @ esk8_0 @ esk9_0)|~(epred5_0 @ esk7_0 @ esk6_0)|((epred5_0)!=(epred7_0))|((epred4_0 @ esk3_0 @ esk4_0)|~(epred4_0 @ esk2_0 @ esk1_0)|((epred4_0)!=(epred3_0)))|(epred2_0))&((epred5_0 @ esk9_0 @ esk10_0)|~(epred5_0 @ esk7_0 @ esk6_0)|((epred5_0)!=(epred7_0))|((epred4_0 @ esk3_0 @ esk4_0)|~(epred4_0 @ esk2_0 @ esk1_0)|((epred4_0)!=(epred3_0)))|(epred2_0)))&(~(epred5_0 @ esk8_0 @ esk10_0)|~(epred5_0 @ esk7_0 @ esk6_0)|((epred5_0)!=(epred7_0))|((epred4_0 @ esk3_0 @ esk4_0)|~(epred4_0 @ esk2_0 @ esk1_0)|((epred4_0)!=(epred3_0)))|(epred2_0)))))&(((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|((epred4_0 @ esk4_0 @ esk5_0)|~(epred4_0 @ esk2_0 @ esk1_0)|((epred4_0)!=(epred3_0)))|(epred2_0))&(((((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred5_0)!=(epred7_0))|((epred4_0 @ esk4_0 @ esk5_0)|~(epred4_0 @ esk2_0 @ esk1_0)|((epred4_0)!=(epred3_0)))|(epred2_0))&((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred5_0)!=(epred7_0))|((epred4_0 @ esk4_0 @ esk5_0)|~(epred4_0 @ esk2_0 @ esk1_0)|((epred4_0)!=(epred3_0)))|(epred2_0)))&(~(epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred5_0)!=(epred7_0))|((epred4_0 @ esk4_0 @ esk5_0)|~(epred4_0 @ esk2_0 @ esk1_0)|((epred4_0)!=(epred3_0)))|(epred2_0)))&((((epred5_0 @ esk8_0 @ esk9_0)|~(epred5_0 @ esk7_0 @ esk6_0)|((epred5_0)!=(epred7_0))|((epred4_0 @ esk4_0 @ esk5_0)|~(epred4_0 @ esk2_0 @ esk1_0)|((epred4_0)!=(epred3_0)))|(epred2_0))&((epred5_0 @ esk9_0 @ esk10_0)|~(epred5_0 @ esk7_0 @ esk6_0)|((epred5_0)!=(epred7_0))|((epred4_0 @ esk4_0 @ esk5_0)|~(epred4_0 @ esk2_0 @ esk1_0)|((epred4_0)!=(epred3_0)))|(epred2_0)))&(~(epred5_0 @ esk8_0 @ esk10_0)|~(epred5_0 @ esk7_0 @ esk6_0)|((epred5_0)!=(epred7_0))|((epred4_0 @ esk4_0 @ esk5_0)|~(epred4_0 @ esk2_0 @ esk1_0)|((epred4_0)!=(epred3_0)))|(epred2_0))))))&(((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|(~(epred4_0 @ esk3_0 @ esk5_0)|~(epred4_0 @ esk2_0 @ esk1_0)|((epred4_0)!=(epred3_0)))|(epred2_0))&(((((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred5_0)!=(epred7_0))|(~(epred4_0 @ esk3_0 @ esk5_0)|~(epred4_0 @ esk2_0 @ esk1_0)|((epred4_0)!=(epred3_0)))|(epred2_0))&((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred5_0)!=(epred7_0))|(~(epred4_0 @ esk3_0 @ esk5_0)|~(epred4_0 @ esk2_0 @ esk1_0)|((epred4_0)!=(epred3_0)))|(epred2_0)))&(~(epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred5_0)!=(epred7_0))|(~(epred4_0 @ esk3_0 @ esk5_0)|~(epred4_0 @ esk2_0 @ esk1_0)|((epred4_0)!=(epred3_0)))|(epred2_0)))&((((epred5_0 @ esk8_0 @ esk9_0)|~(epred5_0 @ esk7_0 @ esk6_0)|((epred5_0)!=(epred7_0))|(~(epred4_0 @ esk3_0 @ esk5_0)|~(epred4_0 @ esk2_0 @ esk1_0)|((epred4_0)!=(epred3_0)))|(epred2_0))&((epred5_0 @ esk9_0 @ esk10_0)|~(epred5_0 @ esk7_0 @ esk6_0)|((epred5_0)!=(epred7_0))|(~(epred4_0 @ esk3_0 @ esk5_0)|~(epred4_0 @ esk2_0 @ esk1_0)|((epred4_0)!=(epred3_0)))|(epred2_0)))&(~(epred5_0 @ esk8_0 @ esk10_0)|~(epred5_0 @ esk7_0 @ esk6_0)|((epred5_0)!=(epred7_0))|(~(epred4_0 @ esk3_0 @ esk5_0)|~(epred4_0 @ esk2_0 @ esk1_0)|((epred4_0)!=(epred3_0)))|(epred2_0))))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_5])])])])])])).
% 5.19/1.03 thf(c_0_9, negated_conjecture, (~((epred2_0))|((^[Z0:a > a > $o, Z1:a > a > $o]:(((((![X1469:a, X1470:a]:((((Z0 @ X1469 @ X1470))=>((Z0 @ X1470 @ X1469)))))&(![X1471:a, X1472:a, X1473:a]:((((((Z0 @ X1471 @ X1472))&((Z0 @ X1472 @ X1473))))=>((Z0 @ X1471 @ X1473)))))))&(((Z0)=(Z1))))))!=(^[Z0:a > a > $o, Z1:a > a > $o]:(((((![X1474:a, X1475:a]:((((Z0 @ X1474 @ X1475))=>((Z0 @ X1475 @ X1474)))))&(![X1476:a, X1477:a, X1478:a]:((((((Z0 @ X1476 @ X1477))&((Z0 @ X1477 @ X1478))))=>((Z0 @ X1476 @ X1478)))))))&(((Z0)=(Z1)))))))), inference(split_conjunct,[status(thm)],[c_0_6])).
% 5.19/1.03 thf(c_0_10, plain, ![X48:a > a > $o, X49:a > a > $o, X50:a > a > $o, X51:a, X52:a, X53:a, X54:a, X55:a, X56:a, X57:a, X58:a, X59:a, X60:a]:(((((((~(X48 @ X51 @ X52)|(X48 @ X52 @ X51)|~(epred1_3 @ X50 @ X49 @ X48))&(~(X48 @ X53 @ X54)|~(X48 @ X54 @ X55)|(X48 @ X53 @ X55)|~(epred1_3 @ X50 @ X49 @ X48)))&(((X48)=(X49))|~(epred1_3 @ X50 @ X49 @ X48)))&(~(X49 @ X56 @ X57)|(X49 @ X57 @ X56)|~(epred1_3 @ X50 @ X49 @ X48)))&(~(X49 @ X58 @ X59)|~(X49 @ X59 @ X60)|(X49 @ X58 @ X60)|~(epred1_3 @ X50 @ X49 @ X48)))&(((X49)=(X50))|~(epred1_3 @ X50 @ X49 @ X48)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_7])])])])])).
% 5.19/1.03 thf(c_0_11, plain, ((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|((epred3_0)=(epred4_0))|(epred2_0)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_12, negated_conjecture, ~((epred2_0)), inference(cn,[status(thm)],[c_0_9])).
% 5.19/1.03 thf(c_0_13, plain, ![X1:a > a > $o, X2:a > a > $o, X6:a > a > $o]:((((X1)=(X2))|~((epred1_3 @ X2 @ X1 @ X6)))), inference(split_conjunct,[status(thm)],[c_0_10])).
% 5.19/1.03 thf(c_0_14, plain, (((epred3_0)=(epred4_0))|(epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)), inference(sr,[status(thm)],[c_0_11, c_0_12])).
% 5.19/1.03 thf(c_0_15, plain, ![X6:a > a > $o, X2:a > a > $o, X1:a > a > $o]:((((X1)=(X2))|~((epred1_3 @ X6 @ X2 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_10])).
% 5.19/1.03 thf(c_0_16, plain, (((epred3_0)=(epred4_0))|((epred6_0)=(epred7_0))), inference(spm,[status(thm)],[c_0_13, c_0_14])).
% 5.19/1.03 thf(c_0_17, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred3_0)=(epred4_0))|(epred2_0)|((epred5_0)!=(epred7_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_18, plain, (((epred3_0)=(epred4_0))|((epred6_0)=(epred5_0))), inference(spm,[status(thm)],[c_0_15, c_0_14])).
% 5.19/1.03 thf(c_0_19, plain, ![X3:a, X4:a, X2:a > a > $o, X6:a > a > $o, X5:a, X1:a > a > $o]:(((X1 @ X3 @ X5)|~((X1 @ X3 @ X4))|~((X1 @ X4 @ X5))|~((epred1_3 @ X2 @ X6 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_10])).
% 5.19/1.03 thf(c_0_20, plain, (((epred3_0)=(epred4_0))|(epred1_3 @ epred7_0 @ epred7_0 @ epred5_0)), inference(spm,[status(thm)],[c_0_14, c_0_16])).
% 5.19/1.03 thf(c_0_21, plain, (((epred3_0)=(epred4_0))|(epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred7_0)!=(epred5_0))), inference(sr,[status(thm)],[c_0_17, c_0_12])).
% 5.19/1.03 thf(c_0_22, plain, (((epred7_0)=(epred5_0))|((epred3_0)=(epred4_0))), inference(spm,[status(thm)],[c_0_18, c_0_16])).
% 5.19/1.03 thf(c_0_23, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred3_0)=(epred4_0))|(epred2_0)|((epred5_0)!=(epred7_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_24, plain, ((epred5_0 @ esk6_0 @ esk7_0)|((epred3_0)=(epred4_0))|(epred2_0)|~((epred5_0 @ esk8_0 @ esk10_0))|((epred5_0)!=(epred7_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_25, plain, ![X3:a, X4:a, X5:a]:((((epred3_0)=(epred4_0))|(epred5_0 @ X3 @ X4)|~((epred5_0 @ X5 @ X4))|~((epred5_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_19, c_0_20])).
% 5.19/1.03 thf(c_0_26, plain, (((epred3_0)=(epred4_0))|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk9_0 @ esk10_0)), inference(csr,[status(thm)],[c_0_21, c_0_22])).
% 5.19/1.03 thf(c_0_27, plain, (((epred3_0)=(epred4_0))|(epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred7_0)!=(epred5_0))), inference(sr,[status(thm)],[c_0_23, c_0_12])).
% 5.19/1.03 thf(c_0_28, plain, (((epred3_0)=(epred4_0))|(epred5_0 @ esk6_0 @ esk7_0)|((epred7_0)!=(epred5_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(sr,[status(thm)],[c_0_24, c_0_12])).
% 5.19/1.03 thf(c_0_29, plain, ((epred5_0 @ esk9_0 @ esk10_0)|((epred3_0)=(epred4_0))|(epred2_0)|~((epred5_0 @ esk7_0 @ esk6_0))|((epred5_0)!=(epred7_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_30, plain, ![X3:a, X2:a > a > $o, X6:a > a > $o, X4:a, X1:a > a > $o]:(((X1 @ X4 @ X3)|~((X1 @ X3 @ X4))|~((epred1_3 @ X2 @ X6 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_10])).
% 5.19/1.03 thf(c_0_31, plain, ![X3:a]:((((epred3_0)=(epred4_0))|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ X3 @ esk10_0)|~((epred5_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_25, c_0_26])).
% 5.19/1.03 thf(c_0_32, plain, (((epred3_0)=(epred4_0))|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk9_0)), inference(csr,[status(thm)],[c_0_27, c_0_22])).
% 5.19/1.03 thf(c_0_33, plain, (((epred3_0)=(epred4_0))|(epred5_0 @ esk6_0 @ esk7_0)|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[c_0_28, c_0_22])).
% 5.19/1.03 thf(c_0_34, plain, (((epred3_0)=(epred4_0))|(epred5_0 @ esk9_0 @ esk10_0)|((epred7_0)!=(epred5_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(sr,[status(thm)],[c_0_29, c_0_12])).
% 5.19/1.03 thf(c_0_35, plain, ![X4:a, X3:a]:((((epred3_0)=(epred4_0))|(epred5_0 @ X3 @ X4)|~((epred5_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_30, c_0_20])).
% 5.19/1.03 thf(c_0_36, plain, (((epred3_0)=(epred4_0))|(epred5_0 @ esk6_0 @ esk7_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_31, c_0_32]), c_0_33])).
% 5.19/1.03 thf(c_0_37, plain, ((epred5_0 @ esk8_0 @ esk9_0)|((epred3_0)=(epred4_0))|(epred2_0)|~((epred5_0 @ esk7_0 @ esk6_0))|((epred5_0)!=(epred7_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_38, plain, (((epred3_0)=(epred4_0))|(epred5_0 @ esk9_0 @ esk10_0)|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[c_0_34, c_0_22])).
% 5.19/1.03 thf(c_0_39, plain, (((epred3_0)=(epred4_0))|(epred5_0 @ esk7_0 @ esk6_0)), inference(spm,[status(thm)],[c_0_35, c_0_36])).
% 5.19/1.03 thf(c_0_40, plain, (((epred3_0)=(epred4_0))|(epred5_0 @ esk8_0 @ esk9_0)|((epred7_0)!=(epred5_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(sr,[status(thm)],[c_0_37, c_0_12])).
% 5.19/1.03 thf(c_0_41, plain, (((epred3_0)=(epred4_0))|(epred2_0)|~((epred5_0 @ esk8_0 @ esk10_0))|~((epred5_0 @ esk7_0 @ esk6_0))|((epred5_0)!=(epred7_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_42, plain, (((epred3_0)=(epred4_0))|(epred5_0 @ esk9_0 @ esk10_0)), inference(spm,[status(thm)],[c_0_38, c_0_39])).
% 5.19/1.03 thf(c_0_43, plain, (((epred3_0)=(epred4_0))|(epred5_0 @ esk8_0 @ esk9_0)|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[c_0_40, c_0_22])).
% 5.19/1.03 thf(c_0_44, plain, ((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred2_0)|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_45, plain, (((epred3_0)=(epred4_0))|((epred7_0)!=(epred5_0))|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(sr,[status(thm)],[c_0_41, c_0_12])).
% 5.19/1.03 thf(c_0_46, plain, ![X3:a]:((((epred3_0)=(epred4_0))|(epred5_0 @ X3 @ esk10_0)|~((epred5_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_25, c_0_42])).
% 5.19/1.03 thf(c_0_47, plain, (((epred3_0)=(epred4_0))|(epred5_0 @ esk8_0 @ esk9_0)), inference(spm,[status(thm)],[c_0_43, c_0_39])).
% 5.19/1.03 thf(c_0_48, plain, ![X91:a, X92:a]:((((epred3_0 @ X91 @ X92)<=>(epred4_0 @ X91 @ X92))|((epred6_0)=(epred7_0)))), inference(arg_cong,[status(thm)],[c_0_16])).
% 5.19/1.03 thf(c_0_49, plain, ((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_44, c_0_12]), c_0_14])).
% 5.19/1.03 thf(c_0_50, plain, ((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred2_0)|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_51, plain, (((epred3_0)=(epred4_0))|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[c_0_45, c_0_22])).
% 5.19/1.03 thf(c_0_52, plain, (((epred3_0)=(epred4_0))|(epred5_0 @ esk8_0 @ esk10_0)), inference(spm,[status(thm)],[c_0_46, c_0_47])).
% 5.19/1.03 thf(c_0_53, plain, ![X3:a, X4:a, X5:a]:(((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|(epred3_0 @ X3 @ X5)|(epred2_0)|~((epred3_0 @ X3 @ X4))|~((epred3_0 @ X4 @ X5)))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_54, plain, ![X3:a, X4:a]:((((epred6_0)=(epred7_0))|(epred3_0 @ X3 @ X4)|~((epred4_0 @ X3 @ X4)))), inference(dynamic_cnf,[status(thm)],[c_0_48])).
% 5.19/1.03 thf(c_0_55, plain, (((epred6_0)=(epred7_0))|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_13, c_0_49])).
% 5.19/1.03 thf(c_0_56, plain, ((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_50, c_0_12]), c_0_14])).
% 5.19/1.03 thf(c_0_57, plain, ![X87:a, X88:a]:((((epred3_0 @ X87 @ X88)<=>(epred4_0 @ X87 @ X88))|((epred6_0)=(epred5_0)))), inference(arg_cong,[status(thm)],[c_0_18])).
% 5.19/1.03 thf(c_0_58, plain, ((epred3_0)=(epred4_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_51, c_0_52]), c_0_39])).
% 5.19/1.03 thf(c_0_59, plain, ![X3:a, X4:a, X5:a]:(((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|(epred3_0 @ X3 @ X4)|~((epred3_0 @ X5 @ X4))|~((epred3_0 @ X3 @ X5)))), inference(sr,[status(thm)],[c_0_53, c_0_12])).
% 5.19/1.03 thf(c_0_60, plain, (((epred6_0)=(epred7_0))|(epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk4_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_54, c_0_55])).
% 5.19/1.03 thf(c_0_61, plain, (((epred6_0)=(epred7_0))|(epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_13, c_0_56])).
% 5.19/1.03 thf(c_0_62, plain, ![X3:a, X4:a]:((((epred6_0)=(epred5_0))|(epred3_0 @ X3 @ X4)|~((epred4_0 @ X3 @ X4)))), inference(dynamic_cnf,[status(thm)],[c_0_57])).
% 5.19/1.03 thf(c_0_63, plain, (((epred6_0)=(epred5_0))|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_15, c_0_49])).
% 5.19/1.03 thf(c_0_64, plain, ![X408:a, X409:a]:(((epred3_0 @ X408 @ X409)<=>(epred4_0 @ X408 @ X409))), inference(arg_cong,[status(thm)],[c_0_58])).
% 5.19/1.03 thf(c_0_65, plain, ![X3:a]:((((epred6_0)=(epred7_0))|(epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ X3 @ esk5_0)|~((epred3_0 @ X3 @ esk4_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_59, c_0_60]), c_0_13])).
% 5.19/1.03 thf(c_0_66, plain, (((epred6_0)=(epred7_0))|(epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk3_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_54, c_0_61])).
% 5.19/1.03 thf(c_0_67, plain, (((epred6_0)=(epred5_0))|(epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk4_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_62, c_0_63])).
% 5.19/1.03 thf(c_0_68, plain, (((epred6_0)=(epred5_0))|(epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_15, c_0_56])).
% 5.19/1.03 thf(c_0_69, plain, ![X3:a, X4:a]:(((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|(epred3_0 @ X4 @ X3)|(epred2_0)|~((epred3_0 @ X3 @ X4)))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_70, plain, ((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred2_0)|~((epred4_0 @ esk3_0 @ esk5_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_71, plain, ![X3:a, X4:a]:(((epred4_0 @ X3 @ X4)|~((epred3_0 @ X3 @ X4)))), inference(dynamic_cnf,[status(thm)],[c_0_64])).
% 5.19/1.03 thf(c_0_72, plain, (((epred6_0)=(epred7_0))|(epred3_0 @ esk3_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_65, c_0_66])).
% 5.19/1.03 thf(c_0_73, plain, ![X3:a]:((((epred6_0)=(epred5_0))|(epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ X3 @ esk5_0)|~((epred3_0 @ X3 @ esk4_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_59, c_0_67]), c_0_15])).
% 5.19/1.03 thf(c_0_74, plain, (((epred6_0)=(epred5_0))|(epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk3_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_62, c_0_68])).
% 5.19/1.03 thf(c_0_75, plain, ![X4:a, X3:a]:(((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|(epred3_0 @ X3 @ X4)|~((epred3_0 @ X4 @ X3)))), inference(sr,[status(thm)],[c_0_69, c_0_12])).
% 5.19/1.03 thf(c_0_76, plain, ![X3:a, X4:a]:(((epred3_0 @ X3 @ X4)|~((epred4_0 @ X3 @ X4)))), inference(dynamic_cnf,[status(thm)],[c_0_64])).
% 5.19/1.03 thf(c_0_77, plain, ((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|(epred4_0 @ esk1_0 @ esk2_0)|~((epred4_0 @ esk3_0 @ esk5_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_70, c_0_12]), c_0_14])).
% 5.19/1.03 thf(c_0_78, plain, (((epred6_0)=(epred7_0))|(epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk3_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_71, c_0_72])).
% 5.19/1.03 thf(c_0_79, plain, (((epred6_0)=(epred5_0))|(epred3_0 @ esk3_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_73, c_0_74])).
% 5.19/1.03 thf(c_0_80, plain, ![X4:a, X3:a]:(((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|(epred3_0 @ X3 @ X4)|~((epred4_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_75, c_0_76])).
% 5.19/1.03 thf(c_0_81, plain, (((epred6_0)=(epred7_0))|(epred4_0 @ esk1_0 @ esk2_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_77, c_0_78]), c_0_13])).
% 5.19/1.03 thf(c_0_82, plain, (((epred6_0)=(epred5_0))|(epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk3_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_71, c_0_79])).
% 5.19/1.03 thf(c_0_83, plain, ((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred2_0)|~((epred4_0 @ esk2_0 @ esk1_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_84, plain, (((epred6_0)=(epred7_0))|(epred3_0 @ esk2_0 @ esk1_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_80, c_0_81]), c_0_13])).
% 5.19/1.03 thf(c_0_85, plain, ((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|(epred2_0)|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred4_0 @ esk2_0 @ esk1_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_86, plain, (((epred6_0)=(epred5_0))|(epred4_0 @ esk1_0 @ esk2_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_77, c_0_82]), c_0_15])).
% 5.19/1.03 thf(c_0_87, plain, ![X3:a, X5:a, X4:a]:(((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|(epred3_0 @ X3 @ X4)|~((epred3_0 @ X3 @ X5))|~((epred4_0 @ X5 @ X4)))), inference(spm,[status(thm)],[c_0_59, c_0_76])).
% 5.19/1.03 thf(c_0_88, plain, ((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|(epred4_0 @ esk4_0 @ esk5_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_83, c_0_12]), c_0_14])).
% 5.19/1.03 thf(c_0_89, plain, (((epred6_0)=(epred7_0))|(epred4_0 @ esk2_0 @ esk1_0)), inference(spm,[status(thm)],[c_0_71, c_0_84])).
% 5.19/1.03 thf(c_0_90, plain, ((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred2_0)|~((epred4_0 @ esk2_0 @ esk1_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_91, plain, ![X1:a > a > $o, X2:a > a > $o, X3:a, X6:a > a > $o]:((((X1 @ X3)=(X2 @ X3))|~((epred1_3 @ X2 @ X1 @ X6)))), inference(arg_cong,[status(thm)],[c_0_13])).
% 5.19/1.03 thf(c_0_92, plain, ((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_85, c_0_12]), c_0_14])).
% 5.19/1.03 thf(c_0_93, plain, (((epred6_0)=(epred5_0))|(epred3_0 @ esk2_0 @ esk1_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_80, c_0_86]), c_0_15])).
% 5.19/1.03 thf(c_0_94, plain, ![X3:a, X4:a, X5:a]:(((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|(epred3_0 @ X3 @ X4)|~((epred4_0 @ X5 @ X4))|~((epred4_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_87, c_0_76])).
% 5.19/1.03 thf(c_0_95, plain, (((epred6_0)=(epred7_0))|(epred4_0 @ esk4_0 @ esk5_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_88, c_0_89]), c_0_13])).
% 5.19/1.03 thf(c_0_96, plain, ((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|(epred4_0 @ esk3_0 @ esk4_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_90, c_0_12]), c_0_14])).
% 5.19/1.03 thf(c_0_97, plain, ![X3:a]:((((epred6_0 @ X3)=(epred7_0 @ X3))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0)))), inference(spm,[status(thm)],[c_0_91, c_0_92])).
% 5.19/1.03 thf(c_0_98, plain, (((epred6_0)=(epred5_0))|(epred4_0 @ esk2_0 @ esk1_0)), inference(spm,[status(thm)],[c_0_71, c_0_93])).
% 5.19/1.03 thf(c_0_99, plain, ![X3:a]:((((epred6_0)=(epred7_0))|(epred3_0 @ X3 @ esk5_0)|~((epred4_0 @ X3 @ esk4_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_94, c_0_95]), c_0_13])).
% 5.19/1.03 thf(c_0_100, plain, (((epred6_0)=(epred7_0))|(epred4_0 @ esk3_0 @ esk4_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_96, c_0_89]), c_0_13])).
% 5.19/1.03 thf(c_0_101, plain, ![X3:a]:((((epred6_0 @ X3)=(epred7_0 @ X3))|((epred6_0)=(epred7_0))|~((epred4_0 @ esk3_0 @ esk5_0)))), inference(spm,[status(thm)],[c_0_97, c_0_89])).
% 5.19/1.03 thf(c_0_102, plain, (((epred6_0)=(epred5_0))|(epred4_0 @ esk4_0 @ esk5_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_88, c_0_98]), c_0_15])).
% 5.19/1.03 thf(c_0_103, plain, (((epred6_0)=(epred7_0))|(epred3_0 @ esk3_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_99, c_0_100])).
% 5.19/1.03 thf(c_0_104, plain, (((epred6_0)=(epred7_0))|~((epred4_0 @ esk3_0 @ esk5_0))), inference(cn,[status(thm)],[inference(pos_ext,[status(thm)],[c_0_101])])).
% 5.19/1.03 thf(c_0_105, plain, ![X3:a]:((((epred6_0 @ X3)=(epred7_0 @ X3))|(epred4_0 @ esk4_0 @ esk5_0))), inference(arg_cong,[status(thm)],[c_0_95])).
% 5.19/1.03 thf(c_0_106, plain, ![X3:a]:((((epred6_0 @ X3)=(epred5_0 @ X3))|(epred4_0 @ esk4_0 @ esk5_0))), inference(arg_cong,[status(thm)],[c_0_102])).
% 5.19/1.03 thf(c_0_107, plain, (((epred6_0)=(epred5_0))|(epred4_0 @ esk3_0 @ esk4_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_96, c_0_98]), c_0_15])).
% 5.19/1.03 thf(c_0_108, plain, ![X6:a > a > $o, X3:a, X2:a > a > $o, X1:a > a > $o]:((((X1 @ X3)=(X2 @ X3))|~((epred1_3 @ X6 @ X2 @ X1)))), inference(arg_cong,[status(thm)],[c_0_15])).
% 5.19/1.03 thf(c_0_109, plain, ((epred6_0)=(epred7_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_71, c_0_103]), c_0_104])).
% 5.19/1.03 thf(c_0_110, plain, ![X3:a]:((((epred7_0 @ X3)=(epred5_0 @ X3))|(epred4_0 @ esk4_0 @ esk5_0))), inference(spm,[status(thm)],[c_0_105, c_0_106])).
% 5.19/1.03 thf(c_0_111, plain, ![X3:a]:((((epred6_0 @ X3)=(epred7_0 @ X3))|(epred4_0 @ esk3_0 @ esk4_0))), inference(arg_cong,[status(thm)],[c_0_100])).
% 5.19/1.03 thf(c_0_112, plain, ![X3:a]:((((epred6_0 @ X3)=(epred5_0 @ X3))|(epred4_0 @ esk3_0 @ esk4_0))), inference(arg_cong,[status(thm)],[c_0_107])).
% 5.19/1.03 thf(c_0_113, plain, ![X3:a]:((((epred6_0 @ X3)=(epred5_0 @ X3))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0)))), inference(spm,[status(thm)],[c_0_108, c_0_92])).
% 5.19/1.03 thf(c_0_114, plain, ![X3:a, X4:a, X5:a]:(((epred1_3 @ epred7_0 @ epred7_0 @ epred5_0)|(epred3_0 @ X3 @ X4)|~((epred4_0 @ X5 @ X4))|~((epred4_0 @ X3 @ X5)))), inference(rw,[status(thm)],[c_0_94, c_0_109])).
% 5.19/1.03 thf(c_0_115, plain, (((epred7_0)=(epred5_0))|(epred4_0 @ esk4_0 @ esk5_0)), inference(pos_ext,[status(thm)],[c_0_110])).
% 5.19/1.03 thf(c_0_116, plain, ![X3:a]:((((epred7_0 @ X3)=(epred5_0 @ X3))|(epred4_0 @ esk3_0 @ esk4_0))), inference(spm,[status(thm)],[c_0_111, c_0_112])).
% 5.19/1.03 thf(c_0_117, plain, ![X3:a]:((((epred6_0 @ X3)=(epred5_0 @ X3))|((epred6_0)=(epred5_0))|~((epred4_0 @ esk3_0 @ esk5_0)))), inference(spm,[status(thm)],[c_0_113, c_0_98])).
% 5.19/1.03 thf(c_0_118, plain, ![X3:a]:((((epred7_0)=(epred5_0))|(epred3_0 @ X3 @ esk5_0)|~((epred4_0 @ X3 @ esk4_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_114, c_0_115]), c_0_15])).
% 5.19/1.03 thf(c_0_119, plain, (((epred7_0)=(epred5_0))|(epred4_0 @ esk3_0 @ esk4_0)), inference(pos_ext,[status(thm)],[c_0_116])).
% 5.19/1.03 thf(c_0_120, plain, (((epred6_0)=(epred5_0))|~((epred4_0 @ esk3_0 @ esk5_0))), inference(cn,[status(thm)],[inference(pos_ext,[status(thm)],[c_0_117])])).
% 5.19/1.03 thf(c_0_121, plain, ![X3:a]:((((epred6_0 @ X3)=(epred7_0 @ X3))|(epred4_0 @ esk1_0 @ esk2_0))), inference(arg_cong,[status(thm)],[c_0_81])).
% 5.19/1.03 thf(c_0_122, plain, ![X3:a]:((((epred6_0 @ X3)=(epred5_0 @ X3))|(epred4_0 @ esk1_0 @ esk2_0))), inference(arg_cong,[status(thm)],[c_0_86])).
% 5.19/1.03 thf(c_0_123, plain, ![X3:a, X4:a]:(((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ X4 @ X3)|(epred2_0)|((epred5_0)!=(epred7_0))|~((epred3_0 @ X3 @ X4)))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_124, plain, (((epred7_0)=(epred5_0))|(epred3_0 @ esk3_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_118, c_0_119])).
% 5.19/1.03 thf(c_0_125, plain, (((epred7_0)=(epred5_0))|~((epred4_0 @ esk3_0 @ esk5_0))), inference(rw,[status(thm)],[c_0_120, c_0_109])).
% 5.19/1.03 thf(c_0_126, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred2_0)|((epred5_0)!=(epred7_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_127, plain, ![X3:a]:((((epred7_0 @ X3)=(epred5_0 @ X3))|(epred4_0 @ esk1_0 @ esk2_0))), inference(spm,[status(thm)],[c_0_121, c_0_122])).
% 5.19/1.03 thf(c_0_128, plain, ![X4:a, X3:a]:(((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ X3 @ X4)|((epred7_0)!=(epred5_0))|~((epred3_0 @ X4 @ X3)))), inference(sr,[status(thm)],[c_0_123, c_0_12])).
% 5.19/1.03 thf(c_0_129, plain, ((epred7_0)=(epred5_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_71, c_0_124]), c_0_125])).
% 5.19/1.03 thf(c_0_130, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred2_0)|((epred5_0)!=(epred7_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_131, plain, ![X3:a]:((((epred6_0 @ X3)=(epred7_0 @ X3))|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0))), inference(spm,[status(thm)],[c_0_91, c_0_49])).
% 5.19/1.03 thf(c_0_132, plain, ![X3:a]:((((epred6_0 @ X3)=(epred5_0 @ X3))|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0))), inference(spm,[status(thm)],[c_0_108, c_0_49])).
% 5.19/1.03 thf(c_0_133, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred7_0)!=(epred5_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_126, c_0_12]), c_0_27])).
% 5.19/1.03 thf(c_0_134, plain, ![X3:a, X953:a]:((((epred7_0 @ X3 @ X953)<=>(epred5_0 @ X3 @ X953))|(epred4_0 @ esk1_0 @ esk2_0))), inference(arg_cong,[status(thm)],[c_0_127])).
% 5.19/1.03 thf(c_0_135, plain, ![X3:a, X4:a]:(((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ X4 @ X3)|(epred2_0)|((epred5_0)!=(epred7_0))|~((epred3_0 @ X3 @ X4)))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_136, plain, ![X4:a, X3:a]:(((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ X3 @ X4)|~((epred3_0 @ X4 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_128, c_0_129])])).
% 5.19/1.03 thf(c_0_137, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred7_0)!=(epred5_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_130, c_0_12]), c_0_27])).
% 5.19/1.03 thf(c_0_138, plain, ![X3:a]:((((epred7_0 @ X3)=(epred5_0 @ X3))|(epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk4_0 @ esk5_0))), inference(spm,[status(thm)],[c_0_131, c_0_132])).
% 5.19/1.03 thf(c_0_139, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred7_0 @ esk13_0 @ esk14_0)<~>(epred5_0 @ esk13_0 @ esk14_0))), inference(neg_ext,[status(thm)],[c_0_133])).
% 5.19/1.03 thf(c_0_140, plain, ![X3:a, X4:a]:(((epred4_0 @ esk1_0 @ esk2_0)|(epred7_0 @ X3 @ X4)|~((epred5_0 @ X3 @ X4)))), inference(dynamic_cnf,[status(thm)],[c_0_134])).
% 5.19/1.03 thf(c_0_141, plain, ![X4:a, X3:a]:(((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ X3 @ X4)|((epred7_0)!=(epred5_0))|~((epred3_0 @ X4 @ X3)))), inference(sr,[status(thm)],[c_0_135, c_0_12])).
% 5.19/1.03 thf(c_0_142, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred2_0)|((epred5_0)!=(epred7_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_143, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ X3 @ X5)|(epred2_0)|((epred5_0)!=(epred7_0))|~((epred3_0 @ X3 @ X4))|~((epred3_0 @ X4 @ X5)))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_144, plain, ![X4:a, X3:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk9_0)|(epred3_0 @ X3 @ X4)|~((epred4_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_136, c_0_76])).
% 5.19/1.03 thf(c_0_145, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(csr,[status(thm)],[inference(neg_ext,[status(thm)],[c_0_137]), c_0_138])).
% 5.19/1.03 thf(c_0_146, plain, ![X3:a, X4:a]:(((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ X3 @ X4)|~((epred7_0 @ X3 @ X4)))), inference(dynamic_cnf,[status(thm)],[c_0_134])).
% 5.19/1.03 thf(c_0_147, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk9_0)|(epred7_0 @ esk13_0 @ esk14_0)), inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_139]), c_0_140])).
% 5.19/1.03 thf(c_0_148, plain, ![X4:a, X3:a]:(((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ X3 @ X4)|~((epred3_0 @ X4 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_141, c_0_129])])).
% 5.19/1.03 thf(c_0_149, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred7_0)!=(epred5_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_142, c_0_12]), c_0_21])).
% 5.19/1.03 thf(c_0_150, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred2_0)|((epred5_0)!=(epred7_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_151, plain, ![X3:a]:((((epred6_0 @ X3)=(epred7_0 @ X3))|(epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0))), inference(spm,[status(thm)],[c_0_91, c_0_56])).
% 5.19/1.03 thf(c_0_152, plain, ![X3:a]:((((epred6_0 @ X3)=(epred5_0 @ X3))|(epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0))), inference(spm,[status(thm)],[c_0_108, c_0_56])).
% 5.19/1.03 thf(c_0_153, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ X3 @ X4)|((epred7_0)!=(epred5_0))|~((epred3_0 @ X5 @ X4))|~((epred3_0 @ X3 @ X5)))), inference(sr,[status(thm)],[c_0_143, c_0_12])).
% 5.19/1.03 thf(c_0_154, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk5_0 @ esk4_0)|(epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_144, c_0_145])).
% 5.19/1.03 thf(c_0_155, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk9_0)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_139]), c_0_146]), c_0_147])).
% 5.19/1.03 thf(c_0_156, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ X3 @ X5)|(epred2_0)|((epred5_0)!=(epred7_0))|~((epred3_0 @ X3 @ X4))|~((epred3_0 @ X4 @ X5)))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_157, plain, ![X4:a, X3:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk9_0 @ esk10_0)|(epred3_0 @ X3 @ X4)|~((epred4_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_148, c_0_76])).
% 5.19/1.03 thf(c_0_158, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(csr,[status(thm)],[inference(neg_ext,[status(thm)],[c_0_149]), c_0_138])).
% 5.19/1.03 thf(c_0_159, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred7_0)!=(epred5_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_150, c_0_12]), c_0_21])).
% 5.19/1.03 thf(c_0_160, plain, ![X3:a]:((((epred7_0 @ X3)=(epred5_0 @ X3))|(epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk3_0 @ esk4_0))), inference(spm,[status(thm)],[c_0_151, c_0_152])).
% 5.19/1.03 thf(c_0_161, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ X3 @ X4)|~((epred3_0 @ X5 @ X4))|~((epred3_0 @ X3 @ X5)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_153, c_0_129])])).
% 5.19/1.03 thf(c_0_162, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk4_0 @ esk5_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk9_0)), inference(spm,[status(thm)],[c_0_136, c_0_154])).
% 5.19/1.03 thf(c_0_163, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk4_0 @ esk3_0)|(epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_144, c_0_155])).
% 5.19/1.03 thf(c_0_164, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred2_0)|((epred5_0)!=(epred7_0))|~((epred4_0 @ esk3_0 @ esk5_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_165, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ X3 @ X4)|((epred7_0)!=(epred5_0))|~((epred3_0 @ X5 @ X4))|~((epred3_0 @ X3 @ X5)))), inference(sr,[status(thm)],[c_0_156, c_0_12])).
% 5.19/1.03 thf(c_0_166, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk5_0 @ esk4_0)|(epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_157, c_0_158])).
% 5.19/1.03 thf(c_0_167, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(csr,[status(thm)],[inference(neg_ext,[status(thm)],[c_0_159]), c_0_160])).
% 5.19/1.03 thf(c_0_168, plain, ![X3:a]:(((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk9_0)|(epred3_0 @ X3 @ esk5_0)|~((epred3_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_161, c_0_162])).
% 5.19/1.03 thf(c_0_169, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk3_0 @ esk4_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk9_0)), inference(spm,[status(thm)],[c_0_136, c_0_163])).
% 5.19/1.03 thf(c_0_170, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred7_0)!=(epred5_0))|~((epred4_0 @ esk3_0 @ esk5_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_164, c_0_12]), c_0_27])).
% 5.19/1.03 thf(c_0_171, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ X3 @ X4)|~((epred3_0 @ X5 @ X4))|~((epred3_0 @ X3 @ X5)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_165, c_0_129])])).
% 5.19/1.03 thf(c_0_172, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk4_0 @ esk5_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk9_0 @ esk10_0)), inference(spm,[status(thm)],[c_0_148, c_0_166])).
% 5.19/1.03 thf(c_0_173, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk4_0 @ esk3_0)|(epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_157, c_0_167])).
% 5.19/1.03 thf(c_0_174, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred2_0)|((epred5_0)!=(epred7_0))|~((epred4_0 @ esk3_0 @ esk5_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_175, plain, ((epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_168, c_0_169])).
% 5.19/1.03 thf(c_0_176, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)|~((epred4_0 @ esk3_0 @ esk5_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_170, c_0_129])])).
% 5.19/1.03 thf(c_0_177, plain, ![X3:a]:(((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk9_0 @ esk10_0)|(epred3_0 @ X3 @ esk5_0)|~((epred3_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_171, c_0_172])).
% 5.19/1.03 thf(c_0_178, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk3_0 @ esk4_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk9_0 @ esk10_0)), inference(spm,[status(thm)],[c_0_148, c_0_173])).
% 5.19/1.03 thf(c_0_179, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred7_0)!=(epred5_0))|~((epred4_0 @ esk3_0 @ esk5_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_174, c_0_12]), c_0_21])).
% 5.19/1.03 thf(c_0_180, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred2_0)|((epred5_0)!=(epred7_0))|~((epred4_0 @ esk2_0 @ esk1_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_181, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk9_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_71, c_0_175]), c_0_176])).
% 5.19/1.03 thf(c_0_182, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred2_0)|((epred5_0)!=(epred7_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred4_0 @ esk2_0 @ esk1_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_183, plain, ![X884:a, X885:a]:((((epred6_0 @ X884 @ X885)<=>(epred7_0 @ X884 @ X885))|~((epred4_0 @ esk3_0 @ esk5_0)))), inference(arg_cong,[status(thm)],[c_0_104])).
% 5.19/1.03 thf(c_0_184, plain, ![X1002:a, X1003:a]:((((epred6_0 @ X1002 @ X1003)<=>(epred5_0 @ X1002 @ X1003))|~((epred4_0 @ esk3_0 @ esk5_0)))), inference(arg_cong,[status(thm)],[c_0_120])).
% 5.19/1.03 thf(c_0_185, plain, ((epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_177, c_0_178])).
% 5.19/1.03 thf(c_0_186, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)|~((epred4_0 @ esk3_0 @ esk5_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_179, c_0_129])])).
% 5.19/1.03 thf(c_0_187, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk4_0 @ esk5_0)|((epred7_0)!=(epred5_0))|~((epred4_0 @ esk2_0 @ esk1_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_180, c_0_12]), c_0_27])).
% 5.19/1.03 thf(c_0_188, plain, ((epred3_0 @ esk2_0 @ esk1_0)|(epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_144, c_0_181])).
% 5.19/1.03 thf(c_0_189, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred2_0)|((epred5_0)!=(epred7_0))|~((epred4_0 @ esk2_0 @ esk1_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_190, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred7_0)!=(epred5_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_182, c_0_12]), c_0_27])).
% 5.19/1.03 thf(c_0_191, plain, ![X3:a, X4:a]:(((epred7_0 @ X3 @ X4)|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred6_0 @ X3 @ X4)))), inference(dynamic_cnf,[status(thm)],[c_0_183])).
% 5.19/1.03 thf(c_0_192, plain, ![X3:a, X4:a]:(((epred6_0 @ X3 @ X4)|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ X3 @ X4)))), inference(dynamic_cnf,[status(thm)],[c_0_184])).
% 5.19/1.03 thf(c_0_193, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred2_0)|((epred5_0)!=(epred7_0))|~((epred4_0 @ esk2_0 @ esk1_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_194, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk9_0 @ esk10_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_71, c_0_185]), c_0_186])).
% 5.19/1.03 thf(c_0_195, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred2_0)|((epred5_0)!=(epred7_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred4_0 @ esk2_0 @ esk1_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_196, plain, ![X3:a, X5:a, X4:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk9_0)|(epred3_0 @ X3 @ X4)|~((epred3_0 @ X3 @ X5))|~((epred4_0 @ X5 @ X4)))), inference(spm,[status(thm)],[c_0_161, c_0_76])).
% 5.19/1.03 thf(c_0_197, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk4_0 @ esk5_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_187, c_0_129])])).
% 5.19/1.03 thf(c_0_198, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk9_0)|(epred4_0 @ esk2_0 @ esk1_0)), inference(spm,[status(thm)],[c_0_71, c_0_188])).
% 5.19/1.03 thf(c_0_199, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk3_0 @ esk4_0)|((epred7_0)!=(epred5_0))|~((epred4_0 @ esk2_0 @ esk1_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_189, c_0_12]), c_0_27])).
% 5.19/1.03 thf(c_0_200, plain, ![X3:a, X4:a]:(((epred5_0 @ X3 @ X4)|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred6_0 @ X3 @ X4)))), inference(dynamic_cnf,[status(thm)],[c_0_184])).
% 5.19/1.03 thf(c_0_201, plain, ![X3:a, X4:a]:(((epred6_0 @ X3 @ X4)|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred7_0 @ X3 @ X4)))), inference(dynamic_cnf,[status(thm)],[c_0_183])).
% 5.19/1.03 thf(c_0_202, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred7_0 @ esk51_0 @ esk52_0)<~>(epred5_0 @ esk51_0 @ esk52_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))), inference(neg_ext,[status(thm)],[c_0_190])).
% 5.19/1.03 thf(c_0_203, plain, ![X3:a, X4:a]:(((epred7_0 @ X3 @ X4)|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ X3 @ X4)))), inference(spm,[status(thm)],[c_0_191, c_0_192])).
% 5.19/1.03 thf(c_0_204, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk4_0 @ esk5_0)|((epred7_0)!=(epred5_0))|~((epred4_0 @ esk2_0 @ esk1_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_193, c_0_12]), c_0_21])).
% 5.19/1.03 thf(c_0_205, plain, ((epred3_0 @ esk2_0 @ esk1_0)|(epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_157, c_0_194])).
% 5.19/1.03 thf(c_0_206, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred2_0)|((epred5_0)!=(epred7_0))|~((epred4_0 @ esk2_0 @ esk1_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_207, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred7_0)!=(epred5_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_195, c_0_12]), c_0_21])).
% 5.19/1.03 thf(c_0_208, plain, ((epred6_0)=(epred5_0)), inference(rw,[status(thm)],[c_0_109, c_0_129])).
% 5.19/1.03 thf(c_0_209, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ X3 @ X4)|~((epred4_0 @ X5 @ X4))|~((epred4_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_196, c_0_76])).
% 5.19/1.03 thf(c_0_210, plain, ((epred4_0 @ esk4_0 @ esk5_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk9_0)), inference(spm,[status(thm)],[c_0_197, c_0_198])).
% 5.19/1.03 thf(c_0_211, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk3_0 @ esk4_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_199, c_0_129])])).
% 5.19/1.03 thf(c_0_212, plain, ![X3:a, X4:a]:(((epred5_0 @ X3 @ X4)|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred7_0 @ X3 @ X4)))), inference(spm,[status(thm)],[c_0_200, c_0_201])).
% 5.19/1.03 thf(c_0_213, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk9_0)|(epred7_0 @ esk51_0 @ esk52_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))), inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_202]), c_0_203])).
% 5.19/1.03 thf(c_0_214, plain, ![X3:a, X5:a, X4:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk9_0 @ esk10_0)|(epred3_0 @ X3 @ X4)|~((epred3_0 @ X3 @ X5))|~((epred4_0 @ X5 @ X4)))), inference(spm,[status(thm)],[c_0_171, c_0_76])).
% 5.19/1.03 thf(c_0_215, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk4_0 @ esk5_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_204, c_0_129])])).
% 5.19/1.03 thf(c_0_216, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk9_0 @ esk10_0)|(epred4_0 @ esk2_0 @ esk1_0)), inference(spm,[status(thm)],[c_0_71, c_0_205])).
% 5.19/1.03 thf(c_0_217, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk3_0 @ esk4_0)|((epred7_0)!=(epred5_0))|~((epred4_0 @ esk2_0 @ esk1_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_206, c_0_12]), c_0_21])).
% 5.19/1.03 thf(c_0_218, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|((epred7_0 @ esk53_0 @ esk54_0)<~>(epred5_0 @ esk53_0 @ esk54_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))), inference(neg_ext,[status(thm)],[c_0_207])).
% 5.19/1.03 thf(c_0_219, plain, ![X1:a > a > $o, X3:a, X2:a > a > $o, X4:a, X6:a > a > $o]:(((X1 @ X4 @ X3)|~((X1 @ X3 @ X4))|~((epred1_3 @ X2 @ X1 @ X6)))), inference(split_conjunct,[status(thm)],[c_0_10])).
% 5.19/1.03 thf(c_0_220, plain, ![X1391:a, X1392:a]:(((epred6_0 @ X1391 @ X1392)<=>(epred5_0 @ X1391 @ X1392))), inference(arg_cong,[status(thm)],[c_0_208])).
% 5.19/1.03 thf(c_0_221, plain, ![X3:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk9_0)|(epred3_0 @ X3 @ esk5_0)|~((epred4_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_209, c_0_210])).
% 5.19/1.03 thf(c_0_222, plain, ((epred4_0 @ esk3_0 @ esk4_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk9_0)), inference(spm,[status(thm)],[c_0_211, c_0_198])).
% 5.19/1.03 thf(c_0_223, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk9_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_202]), c_0_212]), c_0_213])).
% 5.19/1.03 thf(c_0_224, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ X3 @ X4)|~((epred4_0 @ X5 @ X4))|~((epred4_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_214, c_0_76])).
% 5.19/1.03 thf(c_0_225, plain, ((epred4_0 @ esk4_0 @ esk5_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk9_0 @ esk10_0)), inference(spm,[status(thm)],[c_0_215, c_0_216])).
% 5.19/1.03 thf(c_0_226, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk3_0 @ esk4_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_217, c_0_129])])).
% 5.19/1.03 thf(c_0_227, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk9_0 @ esk10_0)|(epred7_0 @ esk53_0 @ esk54_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))), inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_218]), c_0_203])).
% 5.19/1.03 thf(c_0_228, plain, ![X1335:a, X1336:a]:(((epred6_0 @ X1335 @ X1336)<=>(epred7_0 @ X1335 @ X1336))), inference(arg_cong,[status(thm)],[c_0_109])).
% 5.19/1.03 thf(c_0_229, plain, ![X4:a, X3:a]:(((epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred6_0 @ X3 @ X4)|~((epred6_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_219, c_0_49])).
% 5.19/1.03 thf(c_0_230, plain, ![X3:a, X4:a]:(((epred6_0 @ X3 @ X4)|~((epred5_0 @ X3 @ X4)))), inference(dynamic_cnf,[status(thm)],[c_0_220])).
% 5.19/1.03 thf(c_0_231, plain, ((epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_221, c_0_222])).
% 5.19/1.03 thf(c_0_232, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|~((epred4_0 @ esk3_0 @ esk5_0))), inference(spm,[status(thm)],[c_0_223, c_0_198])).
% 5.19/1.03 thf(c_0_233, plain, ![X3:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk9_0 @ esk10_0)|(epred3_0 @ X3 @ esk5_0)|~((epred4_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_224, c_0_225])).
% 5.19/1.03 thf(c_0_234, plain, ((epred4_0 @ esk3_0 @ esk4_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk9_0 @ esk10_0)), inference(spm,[status(thm)],[c_0_226, c_0_216])).
% 5.19/1.03 thf(c_0_235, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk9_0 @ esk10_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_218]), c_0_212]), c_0_227])).
% 5.19/1.03 thf(c_0_236, plain, ![X4:a, X3:a]:(((epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred6_0 @ X3 @ X4)|~((epred6_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_219, c_0_56])).
% 5.19/1.03 thf(c_0_237, plain, ![X3:a, X4:a]:(((epred6_0 @ X3 @ X4)|~((epred7_0 @ X3 @ X4)))), inference(dynamic_cnf,[status(thm)],[c_0_228])).
% 5.19/1.03 thf(c_0_238, plain, ![X1389:a, X1390:a]:(((epred7_0 @ X1389 @ X1390)<=>(epred5_0 @ X1389 @ X1390))), inference(arg_cong,[status(thm)],[c_0_129])).
% 5.19/1.03 thf(c_0_239, plain, ![X1:a > a > $o, X3:a, X4:a, X2:a > a > $o, X5:a, X6:a > a > $o]:(((X1 @ X3 @ X5)|~((X1 @ X3 @ X4))|~((X1 @ X4 @ X5))|~((epred1_3 @ X2 @ X1 @ X6)))), inference(split_conjunct,[status(thm)],[c_0_10])).
% 5.19/1.03 thf(c_0_240, plain, ![X4:a, X3:a]:(((epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred6_0 @ X3 @ X4)|~((epred5_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_229, c_0_230])).
% 5.19/1.03 thf(c_0_241, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk9_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_71, c_0_231]), c_0_232])).
% 5.19/1.03 thf(c_0_242, plain, ((epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_233, c_0_234])).
% 5.19/1.03 thf(c_0_243, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|~((epred4_0 @ esk3_0 @ esk5_0))), inference(spm,[status(thm)],[c_0_235, c_0_216])).
% 5.19/1.03 thf(c_0_244, plain, ![X4:a, X3:a]:(((epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred6_0 @ X3 @ X4)|~((epred7_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_236, c_0_237])).
% 5.19/1.03 thf(c_0_245, plain, ![X3:a, X4:a]:(((epred7_0 @ X3 @ X4)|~((epred5_0 @ X3 @ X4)))), inference(dynamic_cnf,[status(thm)],[c_0_238])).
% 5.19/1.03 thf(c_0_246, plain, ![X3:a, X4:a, X5:a]:(((epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred6_0 @ X3 @ X4)|~((epred6_0 @ X5 @ X4))|~((epred6_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_239, c_0_49])).
% 5.19/1.03 thf(c_0_247, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred6_0 @ esk9_0 @ esk8_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_240, c_0_241])).
% 5.19/1.03 thf(c_0_248, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk9_0 @ esk10_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_71, c_0_242]), c_0_243])).
% 5.19/1.03 thf(c_0_249, plain, ![X4:a, X3:a]:(((epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred6_0 @ X3 @ X4)|~((epred5_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_244, c_0_245])).
% 5.19/1.03 thf(c_0_250, plain, ![X3:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred6_0 @ X3 @ esk8_0)|~((epred6_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_246, c_0_247])).
% 5.19/1.03 thf(c_0_251, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred6_0 @ esk10_0 @ esk9_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_240, c_0_248])).
% 5.19/1.03 thf(c_0_252, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred2_0)|~((epred5_0 @ esk8_0 @ esk10_0))|((epred5_0)!=(epred7_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_253, plain, ![X3:a, X4:a, X5:a]:(((epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred6_0 @ X3 @ X4)|~((epred6_0 @ X5 @ X4))|~((epred6_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_239, c_0_56])).
% 5.19/1.03 thf(c_0_254, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred6_0 @ esk9_0 @ esk8_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk3_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_249, c_0_241])).
% 5.19/1.03 thf(c_0_255, plain, ((epred6_0 @ esk10_0 @ esk8_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_250, c_0_251])).
% 5.19/1.03 thf(c_0_256, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred7_0)!=(epred5_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_252, c_0_12]), c_0_28])).
% 5.19/1.03 thf(c_0_257, plain, ![X3:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred6_0 @ X3 @ esk8_0)|~((epred6_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_253, c_0_254])).
% 5.19/1.03 thf(c_0_258, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred6_0 @ esk10_0 @ esk9_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk3_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_249, c_0_248])).
% 5.19/1.03 thf(c_0_259, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred2_0)|~((epred5_0 @ esk8_0 @ esk10_0))|((epred5_0)!=(epred7_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.03 thf(c_0_260, plain, ![X3:a, X4:a]:(((epred5_0 @ X3 @ X4)|~((epred6_0 @ X3 @ X4)))), inference(dynamic_cnf,[status(thm)],[c_0_220])).
% 5.19/1.03 thf(c_0_261, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred6_0 @ esk8_0 @ esk10_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk4_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_229, c_0_255])).
% 5.19/1.03 thf(c_0_262, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[inference(neg_ext,[status(thm)],[c_0_256]), c_0_138])).
% 5.19/1.03 thf(c_0_263, plain, ((epred6_0 @ esk10_0 @ esk8_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_257, c_0_258])).
% 5.19/1.03 thf(c_0_264, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred7_0)!=(epred5_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_259, c_0_12]), c_0_28])).
% 5.19/1.03 thf(c_0_265, plain, ![X3:a, X4:a, X5:a]:(((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred3_0 @ X3 @ X4)|~((epred4_0 @ X5 @ X4))|~((epred4_0 @ X3 @ X5)))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_114, c_0_129]), c_0_129])).
% 5.19/1.03 thf(c_0_266, plain, ((epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_260, c_0_261]), c_0_262])).
% 5.19/1.03 thf(c_0_267, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred6_0 @ esk8_0 @ esk10_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk3_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_236, c_0_263])).
% 5.19/1.03 thf(c_0_268, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[inference(neg_ext,[status(thm)],[c_0_264]), c_0_160])).
% 5.19/1.03 thf(c_0_269, plain, ![X3:a]:(((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ X3 @ esk5_0)|~((epred4_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_265, c_0_266])).
% 5.19/1.03 thf(c_0_270, plain, ((epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_260, c_0_267]), c_0_268])).
% 5.19/1.03 thf(c_0_271, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred3_0 @ esk3_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_269, c_0_270])).
% 5.19/1.03 thf(c_0_272, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ X3 @ X4)|~((epred5_0 @ X5 @ X4))|~((epred5_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_239, c_0_271])).
% 5.19/1.03 thf(c_0_273, plain, ![X3:a]:(((epred3_0 @ esk3_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ X3 @ esk10_0)|~((epred5_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_272, c_0_248])).
% 5.19/1.03 thf(c_0_274, plain, ((epred1_3 @ epred7_0 @ epred7_0 @ epred5_0)|(epred4_0 @ esk1_0 @ esk2_0)|~((epred4_0 @ esk3_0 @ esk5_0))), inference(rw,[status(thm)],[c_0_77, c_0_109])).
% 5.19/1.03 thf(c_0_275, plain, ((epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk3_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_273, c_0_241])).
% 5.19/1.03 thf(c_0_276, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred4_0 @ esk1_0 @ esk2_0)|~((epred4_0 @ esk3_0 @ esk5_0))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_274, c_0_129]), c_0_129])).
% 5.19/1.03 thf(c_0_277, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred4_0 @ esk3_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_71, c_0_275])).
% 5.19/1.03 thf(c_0_278, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_276, c_0_277])).
% 5.19/1.03 thf(c_0_279, plain, ![X3:a, X4:a, X5:a]:(((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ X3 @ X4)|~((epred5_0 @ X5 @ X4))|~((epred5_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_239, c_0_278])).
% 5.19/1.03 thf(c_0_280, plain, ![X4:a, X3:a]:(((epred1_3 @ epred7_0 @ epred7_0 @ epred5_0)|(epred3_0 @ X3 @ X4)|~((epred4_0 @ X4 @ X3)))), inference(rw,[status(thm)],[c_0_80, c_0_109])).
% 5.19/1.03 thf(c_0_281, plain, ![X3:a]:(((epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ X3 @ esk10_0)|~((epred5_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_279, c_0_248])).
% 5.19/1.03 thf(c_0_282, plain, ![X4:a, X3:a]:(((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred3_0 @ X3 @ X4)|~((epred4_0 @ X4 @ X3)))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_280, c_0_129]), c_0_129])).
% 5.19/1.03 thf(c_0_283, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk10_0)), inference(spm,[status(thm)],[c_0_281, c_0_241])).
% 5.19/1.03 thf(c_0_284, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ esk2_0 @ esk1_0)), inference(spm,[status(thm)],[c_0_282, c_0_283])).
% 5.19/1.04 thf(c_0_285, plain, ![X3:a, X4:a, X5:a]:(((epred3_0 @ esk2_0 @ esk1_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ X3 @ X4)|~((epred5_0 @ X5 @ X4))|~((epred5_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_239, c_0_284])).
% 5.19/1.04 thf(c_0_286, plain, ![X3:a]:(((epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ esk2_0 @ esk1_0)|(epred5_0 @ X3 @ esk10_0)|~((epred5_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_285, c_0_248])).
% 5.19/1.04 thf(c_0_287, plain, ((epred1_3 @ epred7_0 @ epred7_0 @ epred5_0)|(epred4_0 @ esk4_0 @ esk5_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(rw,[status(thm)],[c_0_88, c_0_109])).
% 5.19/1.04 thf(c_0_288, plain, ((epred3_0 @ esk2_0 @ esk1_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk10_0)), inference(spm,[status(thm)],[c_0_286, c_0_241])).
% 5.19/1.04 thf(c_0_289, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred4_0 @ esk4_0 @ esk5_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_287, c_0_129]), c_0_129])).
% 5.19/1.04 thf(c_0_290, plain, ((epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk2_0 @ esk1_0)), inference(spm,[status(thm)],[c_0_71, c_0_288])).
% 5.19/1.04 thf(c_0_291, plain, ((epred1_3 @ epred7_0 @ epred7_0 @ epred5_0)|(epred4_0 @ esk3_0 @ esk4_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(rw,[status(thm)],[c_0_96, c_0_109])).
% 5.19/1.04 thf(c_0_292, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred4_0 @ esk4_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_289, c_0_290])).
% 5.19/1.04 thf(c_0_293, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred4_0 @ esk3_0 @ esk4_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_291, c_0_129]), c_0_129])).
% 5.19/1.04 thf(c_0_294, plain, ![X3:a, X4:a, X5:a]:(((epred4_0 @ esk4_0 @ esk5_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ X3 @ X4)|~((epred5_0 @ X5 @ X4))|~((epred5_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_239, c_0_292])).
% 5.19/1.04 thf(c_0_295, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred4_0 @ esk3_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_293, c_0_290])).
% 5.19/1.04 thf(c_0_296, plain, ![X3:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred5_0 @ X3 @ esk10_0)|~((epred5_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_294, c_0_248])).
% 5.19/1.04 thf(c_0_297, plain, ![X3:a, X4:a, X5:a]:(((epred4_0 @ esk3_0 @ esk4_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ X3 @ X4)|~((epred5_0 @ X5 @ X4))|~((epred5_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_239, c_0_295])).
% 5.19/1.04 thf(c_0_298, plain, ((epred4_0 @ esk4_0 @ esk5_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_296, c_0_241])).
% 5.19/1.04 thf(c_0_299, plain, ![X3:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred5_0 @ X3 @ esk10_0)|~((epred5_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_297, c_0_248])).
% 5.19/1.04 thf(c_0_300, plain, ![X3:a]:(((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred3_0 @ X3 @ esk5_0)|~((epred4_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_265, c_0_298])).
% 5.19/1.04 thf(c_0_301, plain, ((epred4_0 @ esk3_0 @ esk4_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_299, c_0_241])).
% 5.19/1.04 thf(c_0_302, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_300, c_0_301])).
% 5.19/1.04 thf(c_0_303, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ X3 @ X4)|~((epred5_0 @ X5 @ X4))|~((epred5_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_239, c_0_302])).
% 5.19/1.04 thf(c_0_304, plain, ![X3:a]:(((epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ X3 @ esk10_0)|~((epred5_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_303, c_0_248])).
% 5.19/1.04 thf(c_0_305, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ X3 @ X4)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ X5 @ X4))|~((epred5_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_19, c_0_92])).
% 5.19/1.04 thf(c_0_306, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred3_0 @ esk3_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_304, c_0_241])).
% 5.19/1.04 thf(c_0_307, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ X3 @ X4)|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ X5 @ X4))|~((epred5_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_305, c_0_290])).
% 5.19/1.04 thf(c_0_308, plain, ((epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk3_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_71, c_0_306])).
% 5.19/1.04 thf(c_0_309, plain, ![X3:a, X4:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ X4 @ X3)|(epred2_0)|~((epred5_0 @ esk8_0 @ esk10_0))|((epred5_0)!=(epred7_0))|~((epred3_0 @ X3 @ X4)))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_310, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ X3 @ X4)|~((epred5_0 @ X5 @ X4))|~((epred5_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_307, c_0_308])).
% 5.19/1.04 thf(c_0_311, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ X3 @ X5)|(epred2_0)|~((epred5_0 @ esk8_0 @ esk10_0))|((epred5_0)!=(epred7_0))|~((epred3_0 @ X3 @ X4))|~((epred3_0 @ X4 @ X5)))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_312, plain, ![X4:a, X3:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ X3 @ X4)|((epred7_0)!=(epred5_0))|~((epred5_0 @ esk8_0 @ esk10_0))|~((epred3_0 @ X4 @ X3)))), inference(sr,[status(thm)],[c_0_309, c_0_12])).
% 5.19/1.04 thf(c_0_313, plain, ![X3:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ X3 @ esk10_0)|~((epred5_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_310, c_0_248])).
% 5.19/1.04 thf(c_0_314, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ X3 @ X4)|((epred7_0)!=(epred5_0))|~((epred5_0 @ esk8_0 @ esk10_0))|~((epred3_0 @ X5 @ X4))|~((epred3_0 @ X3 @ X5)))), inference(sr,[status(thm)],[c_0_311, c_0_12])).
% 5.19/1.04 thf(c_0_315, plain, ![X4:a, X3:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ X3 @ X4)|~((epred5_0 @ esk8_0 @ esk10_0))|~((epred3_0 @ X4 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_312, c_0_129])])).
% 5.19/1.04 thf(c_0_316, plain, ((epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_313, c_0_241])).
% 5.19/1.04 thf(c_0_317, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ X3 @ X4)|~((epred5_0 @ esk8_0 @ esk10_0))|~((epred3_0 @ X5 @ X4))|~((epred3_0 @ X3 @ X5)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_314, c_0_129])])).
% 5.19/1.04 thf(c_0_318, plain, ![X4:a, X3:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ X3 @ X4)|~((epred3_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_315, c_0_316])).
% 5.19/1.04 thf(c_0_319, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ X3 @ X4)|~((epred3_0 @ X5 @ X4))|~((epred3_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_317, c_0_316])).
% 5.19/1.04 thf(c_0_320, plain, ![X4:a, X3:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ X3 @ X4)|~((epred4_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_318, c_0_76])).
% 5.19/1.04 thf(c_0_321, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred2_0)|~((epred5_0 @ esk8_0 @ esk10_0))|((epred5_0)!=(epred7_0))|~((epred4_0 @ esk3_0 @ esk5_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_322, plain, ![X3:a, X5:a, X4:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ X3 @ X4)|~((epred3_0 @ X3 @ X5))|~((epred4_0 @ X5 @ X4)))), inference(spm,[status(thm)],[c_0_319, c_0_76])).
% 5.19/1.04 thf(c_0_323, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk5_0 @ esk4_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_320, c_0_266])).
% 5.19/1.04 thf(c_0_324, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk4_0 @ esk3_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_320, c_0_270])).
% 5.19/1.04 thf(c_0_325, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred7_0)!=(epred5_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_321, c_0_12]), c_0_28])).
% 5.19/1.04 thf(c_0_326, plain, ![X3:a]:(((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ esk5_0 @ X3)|~((epred4_0 @ esk4_0 @ X3)))), inference(spm,[status(thm)],[c_0_322, c_0_323])).
% 5.19/1.04 thf(c_0_327, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk4_0 @ esk3_0)), inference(spm,[status(thm)],[c_0_71, c_0_324])).
% 5.19/1.04 thf(c_0_328, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred7_0 @ esk39_0 @ esk40_0)<~>(epred5_0 @ esk39_0 @ esk40_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(neg_ext,[status(thm)],[c_0_325])).
% 5.19/1.04 thf(c_0_329, plain, ((epred3_0 @ esk5_0 @ esk3_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_326, c_0_327])).
% 5.19/1.04 thf(c_0_330, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred2_0)|~((epred5_0 @ esk8_0 @ esk10_0))|((epred5_0)!=(epred7_0))|~((epred4_0 @ esk2_0 @ esk1_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_331, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred7_0 @ esk39_0 @ esk40_0)|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_328]), c_0_203])).
% 5.19/1.04 thf(c_0_332, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_318, c_0_329])).
% 5.19/1.04 thf(c_0_333, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk3_0 @ esk4_0)|((epred7_0)!=(epred5_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_330, c_0_12]), c_0_28])).
% 5.19/1.04 thf(c_0_334, plain, ![X3:a, X1070:a]:((((epred7_0 @ X3 @ X1070)<=>(epred5_0 @ X3 @ X1070))|(epred4_0 @ esk3_0 @ esk4_0))), inference(arg_cong,[status(thm)],[c_0_116])).
% 5.19/1.04 thf(c_0_335, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk6_0 @ esk7_0)|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_328]), c_0_212]), c_0_331])).
% 5.19/1.04 thf(c_0_336, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk3_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_71, c_0_332])).
% 5.19/1.04 thf(c_0_337, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred2_0)|~((epred5_0 @ esk8_0 @ esk10_0))|((epred5_0)!=(epred7_0))|~((epred4_0 @ esk2_0 @ esk1_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_338, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk3_0 @ esk4_0)|((epred7_0 @ esk63_0 @ esk64_0)<~>(epred5_0 @ esk63_0 @ esk64_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(neg_ext,[status(thm)],[c_0_333])).
% 5.19/1.04 thf(c_0_339, plain, ![X3:a, X4:a]:(((epred4_0 @ esk3_0 @ esk4_0)|(epred7_0 @ X3 @ X4)|~((epred5_0 @ X3 @ X4)))), inference(dynamic_cnf,[status(thm)],[c_0_334])).
% 5.19/1.04 thf(c_0_340, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_335, c_0_336]), c_0_316])).
% 5.19/1.04 thf(c_0_341, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk4_0 @ esk5_0)|((epred7_0)!=(epred5_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_337, c_0_12]), c_0_28])).
% 5.19/1.04 thf(c_0_342, plain, ![X3:a, X1084:a]:((((epred7_0 @ X3 @ X1084)<=>(epred5_0 @ X3 @ X1084))|(epred4_0 @ esk4_0 @ esk5_0))), inference(arg_cong,[status(thm)],[c_0_110])).
% 5.19/1.04 thf(c_0_343, plain, ![X3:a, X4:a]:(((epred4_0 @ esk3_0 @ esk4_0)|(epred5_0 @ X3 @ X4)|~((epred7_0 @ X3 @ X4)))), inference(dynamic_cnf,[status(thm)],[c_0_334])).
% 5.19/1.04 thf(c_0_344, plain, ((epred4_0 @ esk3_0 @ esk4_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred7_0 @ esk63_0 @ esk64_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_338]), c_0_339])).
% 5.19/1.04 thf(c_0_345, plain, ((epred3_0 @ esk2_0 @ esk1_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_320, c_0_340])).
% 5.19/1.04 thf(c_0_346, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk4_0 @ esk5_0)|((epred7_0 @ esk75_0 @ esk76_0)<~>(epred5_0 @ esk75_0 @ esk76_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(neg_ext,[status(thm)],[c_0_341])).
% 5.19/1.04 thf(c_0_347, plain, ![X3:a, X4:a]:(((epred4_0 @ esk4_0 @ esk5_0)|(epred7_0 @ X3 @ X4)|~((epred5_0 @ X3 @ X4)))), inference(dynamic_cnf,[status(thm)],[c_0_342])).
% 5.19/1.04 thf(c_0_348, plain, ((epred4_0 @ esk3_0 @ esk4_0)|(epred5_0 @ esk6_0 @ esk7_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_338]), c_0_343]), c_0_344])).
% 5.19/1.04 thf(c_0_349, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk2_0 @ esk1_0)), inference(spm,[status(thm)],[c_0_71, c_0_345])).
% 5.19/1.04 thf(c_0_350, plain, ![X3:a, X4:a]:(((epred4_0 @ esk4_0 @ esk5_0)|(epred5_0 @ X3 @ X4)|~((epred7_0 @ X3 @ X4)))), inference(dynamic_cnf,[status(thm)],[c_0_342])).
% 5.19/1.04 thf(c_0_351, plain, ((epred4_0 @ esk4_0 @ esk5_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred7_0 @ esk75_0 @ esk76_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_346]), c_0_347])).
% 5.19/1.04 thf(c_0_352, plain, ![X82:a, X81:a, X6:a > a > $o, X2:a > a > $o, X1:a > a > $o]:((((X1 @ X81 @ X82)<=>(X2 @ X81 @ X82))|~((epred1_3 @ X6 @ X2 @ X1)))), inference(arg_cong,[status(thm)],[c_0_15])).
% 5.19/1.04 thf(c_0_353, plain, ![X1:a > a > $o, X2:a > a > $o, X86:a, X85:a, X6:a > a > $o]:((((X1 @ X85 @ X86)<=>(X2 @ X85 @ X86))|~((epred1_3 @ X2 @ X1 @ X6)))), inference(arg_cong,[status(thm)],[c_0_13])).
% 5.19/1.04 thf(c_0_354, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk3_0 @ esk4_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_348, c_0_349]), c_0_316])).
% 5.19/1.04 thf(c_0_355, plain, ((epred4_0 @ esk4_0 @ esk5_0)|(epred5_0 @ esk6_0 @ esk7_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_346]), c_0_350]), c_0_351])).
% 5.19/1.04 thf(c_0_356, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred2_0)|~((epred5_0 @ esk8_0 @ esk10_0))|((epred5_0)!=(epred7_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred4_0 @ esk2_0 @ esk1_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_357, plain, ![X1:a > a > $o, X2:a > a > $o, X3:a, X6:a > a > $o, X4:a]:(((X1 @ X3 @ X4)|~((epred1_3 @ X2 @ X6 @ X1))|~((X6 @ X3 @ X4)))), inference(dynamic_cnf,[status(thm)],[c_0_352])).
% 5.19/1.04 thf(c_0_358, plain, ![X1:a > a > $o, X2:a > a > $o, X3:a, X6:a > a > $o, X4:a]:(((X1 @ X3 @ X4)|~((epred1_3 @ X2 @ X1 @ X6))|~((X2 @ X3 @ X4)))), inference(dynamic_cnf,[status(thm)],[c_0_353])).
% 5.19/1.04 thf(c_0_359, plain, ((epred3_0 @ esk4_0 @ esk3_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_320, c_0_354])).
% 5.19/1.04 thf(c_0_360, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk4_0 @ esk5_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_355, c_0_349]), c_0_316])).
% 5.19/1.04 thf(c_0_361, plain, ((epred5_0 @ esk6_0 @ esk7_0)|((epred7_0)!=(epred5_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_356, c_0_12]), c_0_28])).
% 5.19/1.04 thf(c_0_362, plain, ![X3:a, X4:a]:(((epred5_0 @ X3 @ X4)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred6_0 @ X3 @ X4)))), inference(spm,[status(thm)],[c_0_357, c_0_92])).
% 5.19/1.04 thf(c_0_363, plain, ![X3:a, X4:a]:(((epred6_0 @ X3 @ X4)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred7_0 @ X3 @ X4)))), inference(spm,[status(thm)],[c_0_358, c_0_92])).
% 5.19/1.04 thf(c_0_364, plain, ![X3:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ X3 @ esk3_0)|~((epred3_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_319, c_0_359])).
% 5.19/1.04 thf(c_0_365, plain, ((epred3_0 @ esk5_0 @ esk4_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_320, c_0_360])).
% 5.19/1.04 thf(c_0_366, plain, ((epred5_0 @ esk6_0 @ esk7_0)|((epred7_0 @ esk19_0 @ esk20_0)<~>(epred5_0 @ esk19_0 @ esk20_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(neg_ext,[status(thm)],[c_0_361])).
% 5.19/1.04 thf(c_0_367, plain, ![X3:a, X4:a]:(((epred5_0 @ X3 @ X4)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred7_0 @ X3 @ X4)))), inference(spm,[status(thm)],[c_0_362, c_0_363])).
% 5.19/1.04 thf(c_0_368, plain, ((epred3_0 @ esk5_0 @ esk3_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_364, c_0_365])).
% 5.19/1.04 thf(c_0_369, plain, ((epred5_0 @ esk6_0 @ esk7_0)|~((epred7_0 @ esk19_0 @ esk20_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_366]), c_0_367])).
% 5.19/1.04 thf(c_0_370, plain, ((epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_318, c_0_368])).
% 5.19/1.04 thf(c_0_371, plain, ((epred5_0 @ esk6_0 @ esk7_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_366]), c_0_203]), c_0_369])).
% 5.19/1.04 thf(c_0_372, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk3_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_71, c_0_370])).
% 5.19/1.04 thf(c_0_373, plain, ![X4:a, X3:a]:(((epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ X3 @ X4)|~((epred5_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_30, c_0_49])).
% 5.19/1.04 thf(c_0_374, plain, (epred5_0 @ esk6_0 @ esk7_0), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_371, c_0_372]), c_0_316]), c_0_349])).
% 5.19/1.04 thf(c_0_375, plain, ((epred5_0 @ esk7_0 @ esk6_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk4_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_373, c_0_374])).
% 5.19/1.04 thf(c_0_376, plain, ![X4:a, X3:a]:(((epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ X3 @ X4)|~((epred5_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_30, c_0_56])).
% 5.19/1.04 thf(c_0_377, plain, ![X3:a]:(((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk7_0 @ esk6_0)|(epred3_0 @ X3 @ esk5_0)|~((epred4_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_265, c_0_375])).
% 5.19/1.04 thf(c_0_378, plain, ((epred5_0 @ esk7_0 @ esk6_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk3_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_376, c_0_374])).
% 5.19/1.04 thf(c_0_379, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ esk7_0 @ esk6_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_377, c_0_378])).
% 5.19/1.04 thf(c_0_380, plain, ![X4:a, X3:a]:(((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk7_0 @ esk6_0)|(epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ X3 @ X4)|~((epred5_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_219, c_0_379])).
% 5.19/1.04 thf(c_0_381, plain, ((epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ esk7_0 @ esk6_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_380, c_0_374])).
% 5.19/1.04 thf(c_0_382, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk7_0 @ esk6_0)|(epred4_0 @ esk3_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_71, c_0_381])).
% 5.19/1.04 thf(c_0_383, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred5_0 @ esk7_0 @ esk6_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_276, c_0_382])).
% 5.19/1.04 thf(c_0_384, plain, ![X4:a, X3:a]:(((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk7_0 @ esk6_0)|(epred5_0 @ X3 @ X4)|~((epred5_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_219, c_0_383])).
% 5.19/1.04 thf(c_0_385, plain, ((epred5_0 @ esk7_0 @ esk6_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_384, c_0_374])).
% 5.19/1.04 thf(c_0_386, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred5_0 @ esk7_0 @ esk6_0)|(epred3_0 @ esk2_0 @ esk1_0)), inference(spm,[status(thm)],[c_0_282, c_0_385])).
% 5.19/1.04 thf(c_0_387, plain, ![X4:a, X3:a]:(((epred3_0 @ esk2_0 @ esk1_0)|(epred5_0 @ esk7_0 @ esk6_0)|(epred5_0 @ X3 @ X4)|~((epred5_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_219, c_0_386])).
% 5.19/1.04 thf(c_0_388, plain, ((epred5_0 @ esk7_0 @ esk6_0)|(epred3_0 @ esk2_0 @ esk1_0)), inference(spm,[status(thm)],[c_0_387, c_0_374])).
% 5.19/1.04 thf(c_0_389, plain, ((epred5_0 @ esk7_0 @ esk6_0)|(epred4_0 @ esk2_0 @ esk1_0)), inference(spm,[status(thm)],[c_0_71, c_0_388])).
% 5.19/1.04 thf(c_0_390, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred5_0 @ esk7_0 @ esk6_0)|(epred4_0 @ esk4_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_289, c_0_389])).
% 5.19/1.04 thf(c_0_391, plain, ![X4:a, X3:a]:(((epred4_0 @ esk4_0 @ esk5_0)|(epred5_0 @ esk7_0 @ esk6_0)|(epred5_0 @ X3 @ X4)|~((epred5_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_219, c_0_390])).
% 5.19/1.04 thf(c_0_392, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred5_0 @ esk7_0 @ esk6_0)|(epred4_0 @ esk3_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_293, c_0_389])).
% 5.19/1.04 thf(c_0_393, plain, ((epred5_0 @ esk7_0 @ esk6_0)|(epred4_0 @ esk4_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_391, c_0_374])).
% 5.19/1.04 thf(c_0_394, plain, ![X4:a, X3:a]:(((epred4_0 @ esk3_0 @ esk4_0)|(epred5_0 @ esk7_0 @ esk6_0)|(epred5_0 @ X3 @ X4)|~((epred5_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_219, c_0_392])).
% 5.19/1.04 thf(c_0_395, plain, ![X3:a]:(((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred5_0 @ esk7_0 @ esk6_0)|(epred3_0 @ X3 @ esk5_0)|~((epred4_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_265, c_0_393])).
% 5.19/1.04 thf(c_0_396, plain, ((epred5_0 @ esk7_0 @ esk6_0)|(epred4_0 @ esk3_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_394, c_0_374])).
% 5.19/1.04 thf(c_0_397, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ esk7_0 @ esk6_0)), inference(spm,[status(thm)],[c_0_395, c_0_396])).
% 5.19/1.04 thf(c_0_398, plain, ![X4:a, X3:a]:(((epred5_0 @ esk7_0 @ esk6_0)|(epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ X3 @ X4)|~((epred5_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_219, c_0_397])).
% 5.19/1.04 thf(c_0_399, plain, ![X4:a, X3:a]:(((epred5_0 @ X3 @ X4)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_30, c_0_92])).
% 5.19/1.04 thf(c_0_400, plain, ((epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ esk7_0 @ esk6_0)), inference(spm,[status(thm)],[c_0_398, c_0_374])).
% 5.19/1.04 thf(c_0_401, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk8_0 @ esk9_0)|(epred3_0 @ X3 @ X5)|(epred2_0)|~((epred5_0 @ esk7_0 @ esk6_0))|((epred5_0)!=(epred7_0))|~((epred3_0 @ X3 @ X4))|~((epred3_0 @ X4 @ X5)))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_402, plain, ![X4:a, X3:a]:(((epred5_0 @ esk7_0 @ esk6_0)|(epred5_0 @ X3 @ X4)|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_399, c_0_389])).
% 5.19/1.04 thf(c_0_403, plain, ((epred5_0 @ esk7_0 @ esk6_0)|(epred4_0 @ esk3_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_71, c_0_400])).
% 5.19/1.04 thf(c_0_404, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk8_0 @ esk9_0)|(epred3_0 @ X3 @ X4)|((epred7_0)!=(epred5_0))|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred3_0 @ X5 @ X4))|~((epred3_0 @ X3 @ X5)))), inference(sr,[status(thm)],[c_0_401, c_0_12])).
% 5.19/1.04 thf(c_0_405, plain, ![X4:a, X3:a]:(((epred5_0 @ esk7_0 @ esk6_0)|(epred5_0 @ X3 @ X4)|~((epred5_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_402, c_0_403])).
% 5.19/1.04 thf(c_0_406, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk9_0 @ esk10_0)|(epred3_0 @ X3 @ X5)|(epred2_0)|~((epred5_0 @ esk7_0 @ esk6_0))|((epred5_0)!=(epred7_0))|~((epred3_0 @ X3 @ X4))|~((epred3_0 @ X4 @ X5)))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_407, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk8_0 @ esk9_0)|(epred3_0 @ X3 @ X4)|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred3_0 @ X5 @ X4))|~((epred3_0 @ X3 @ X5)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_404, c_0_129])])).
% 5.19/1.04 thf(c_0_408, plain, (epred5_0 @ esk7_0 @ esk6_0), inference(spm,[status(thm)],[c_0_405, c_0_374])).
% 5.19/1.04 thf(c_0_409, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred2_0)|~((epred5_0 @ esk7_0 @ esk6_0))|((epred5_0)!=(epred7_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_410, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred2_0)|~((epred5_0 @ esk7_0 @ esk6_0))|((epred5_0)!=(epred7_0))|~((epred4_0 @ esk3_0 @ esk5_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_411, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk9_0 @ esk10_0)|(epred3_0 @ X3 @ X4)|((epred7_0)!=(epred5_0))|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred3_0 @ X5 @ X4))|~((epred3_0 @ X3 @ X5)))), inference(sr,[status(thm)],[c_0_406, c_0_12])).
% 5.19/1.04 thf(c_0_412, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk8_0 @ esk9_0)|(epred3_0 @ X3 @ X4)|~((epred3_0 @ X5 @ X4))|~((epred3_0 @ X3 @ X5)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_407, c_0_408])])).
% 5.19/1.04 thf(c_0_413, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred7_0)!=(epred5_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_409, c_0_12]), c_0_40])).
% 5.19/1.04 thf(c_0_414, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred2_0)|~((epred5_0 @ esk7_0 @ esk6_0))|((epred5_0)!=(epred7_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_415, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred7_0)!=(epred5_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_410, c_0_12]), c_0_40])).
% 5.19/1.04 thf(c_0_416, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk9_0 @ esk10_0)|(epred3_0 @ X3 @ X4)|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred3_0 @ X5 @ X4))|~((epred3_0 @ X3 @ X5)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_411, c_0_129])])).
% 5.19/1.04 thf(c_0_417, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred2_0)|~((epred5_0 @ esk7_0 @ esk6_0))|((epred5_0)!=(epred7_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_418, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred2_0)|~((epred5_0 @ esk7_0 @ esk6_0))|((epred5_0)!=(epred7_0))|~((epred4_0 @ esk3_0 @ esk5_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_419, plain, ![X3:a, X4:a]:(((epred5_0 @ esk8_0 @ esk9_0)|(epred3_0 @ X4 @ X3)|(epred2_0)|~((epred5_0 @ esk7_0 @ esk6_0))|((epred5_0)!=(epred7_0))|~((epred3_0 @ X3 @ X4)))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_420, plain, ![X3:a, X5:a, X4:a]:(((epred5_0 @ esk8_0 @ esk9_0)|(epred3_0 @ X3 @ X4)|~((epred3_0 @ X3 @ X5))|~((epred4_0 @ X5 @ X4)))), inference(spm,[status(thm)],[c_0_412, c_0_76])).
% 5.19/1.04 thf(c_0_421, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(neg_ext,[status(thm)],[c_0_413]), c_0_138])).
% 5.19/1.04 thf(c_0_422, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred7_0)!=(epred5_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_414, c_0_12]), c_0_40])).
% 5.19/1.04 thf(c_0_423, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred7_0 @ esk41_0 @ esk42_0)<~>(epred5_0 @ esk41_0 @ esk42_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(neg_ext,[status(thm)],[c_0_415])).
% 5.19/1.04 thf(c_0_424, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk9_0 @ esk10_0)|(epred3_0 @ X3 @ X4)|~((epred3_0 @ X5 @ X4))|~((epred3_0 @ X3 @ X5)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_416, c_0_408])])).
% 5.19/1.04 thf(c_0_425, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred7_0)!=(epred5_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_417, c_0_12]), c_0_34])).
% 5.19/1.04 thf(c_0_426, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred2_0)|~((epred5_0 @ esk7_0 @ esk6_0))|((epred5_0)!=(epred7_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_427, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred7_0)!=(epred5_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_418, c_0_12]), c_0_34])).
% 5.19/1.04 thf(c_0_428, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred2_0)|~((epred5_0 @ esk7_0 @ esk6_0))|((epred5_0)!=(epred7_0))|~((epred4_0 @ esk2_0 @ esk1_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_429, plain, ![X4:a, X3:a]:(((epred5_0 @ esk8_0 @ esk9_0)|(epred3_0 @ X3 @ X4)|((epred7_0)!=(epred5_0))|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred3_0 @ X4 @ X3)))), inference(sr,[status(thm)],[c_0_419, c_0_12])).
% 5.19/1.04 thf(c_0_430, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk8_0 @ esk9_0)|(epred3_0 @ X3 @ X4)|~((epred4_0 @ X5 @ X4))|~((epred4_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_420, c_0_76])).
% 5.19/1.04 thf(c_0_431, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred5_0 @ esk8_0 @ esk9_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_421, c_0_408])])).
% 5.19/1.04 thf(c_0_432, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(neg_ext,[status(thm)],[c_0_422]), c_0_160])).
% 5.19/1.04 thf(c_0_433, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk8_0 @ esk9_0)|(epred7_0 @ esk41_0 @ esk42_0)|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_423]), c_0_203])).
% 5.19/1.04 thf(c_0_434, plain, ![X3:a, X4:a]:(((epred5_0 @ esk9_0 @ esk10_0)|(epred3_0 @ X4 @ X3)|(epred2_0)|~((epred5_0 @ esk7_0 @ esk6_0))|((epred5_0)!=(epred7_0))|~((epred3_0 @ X3 @ X4)))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_435, plain, ![X3:a, X5:a, X4:a]:(((epred5_0 @ esk9_0 @ esk10_0)|(epred3_0 @ X3 @ X4)|~((epred3_0 @ X3 @ X5))|~((epred4_0 @ X5 @ X4)))), inference(spm,[status(thm)],[c_0_424, c_0_76])).
% 5.19/1.04 thf(c_0_436, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(neg_ext,[status(thm)],[c_0_425]), c_0_138])).
% 5.19/1.04 thf(c_0_437, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred7_0)!=(epred5_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_426, c_0_12]), c_0_34])).
% 5.19/1.04 thf(c_0_438, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred7_0 @ esk43_0 @ esk44_0)<~>(epred5_0 @ esk43_0 @ esk44_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(neg_ext,[status(thm)],[c_0_427])).
% 5.19/1.04 thf(c_0_439, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred4_0 @ esk4_0 @ esk5_0)|((epred7_0)!=(epred5_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_428, c_0_12]), c_0_40])).
% 5.19/1.04 thf(c_0_440, plain, ![X4:a, X3:a]:(((epred5_0 @ esk8_0 @ esk9_0)|(epred3_0 @ X3 @ X4)|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred3_0 @ X4 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_429, c_0_129])])).
% 5.19/1.04 thf(c_0_441, plain, ![X3:a]:(((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk8_0 @ esk9_0)|(epred3_0 @ X3 @ esk5_0)|~((epred4_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_430, c_0_431])).
% 5.19/1.04 thf(c_0_442, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred5_0 @ esk8_0 @ esk9_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_432, c_0_408])])).
% 5.19/1.04 thf(c_0_443, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk8_0 @ esk9_0)|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_423]), c_0_212]), c_0_433])).
% 5.19/1.04 thf(c_0_444, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred2_0)|~((epred5_0 @ esk7_0 @ esk6_0))|((epred5_0)!=(epred7_0))|~((epred4_0 @ esk2_0 @ esk1_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_445, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred2_0)|~((epred5_0 @ esk7_0 @ esk6_0))|((epred5_0)!=(epred7_0))|~((epred4_0 @ esk2_0 @ esk1_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_446, plain, ![X4:a, X3:a]:(((epred5_0 @ esk9_0 @ esk10_0)|(epred3_0 @ X3 @ X4)|((epred7_0)!=(epred5_0))|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred3_0 @ X4 @ X3)))), inference(sr,[status(thm)],[c_0_434, c_0_12])).
% 5.19/1.04 thf(c_0_447, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk9_0 @ esk10_0)|(epred3_0 @ X3 @ X4)|~((epred4_0 @ X5 @ X4))|~((epred4_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_435, c_0_76])).
% 5.19/1.04 thf(c_0_448, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred5_0 @ esk9_0 @ esk10_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_436, c_0_408])])).
% 5.19/1.04 thf(c_0_449, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(neg_ext,[status(thm)],[c_0_437]), c_0_160])).
% 5.19/1.04 thf(c_0_450, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk9_0 @ esk10_0)|(epred7_0 @ esk43_0 @ esk44_0)|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_438]), c_0_203])).
% 5.19/1.04 thf(c_0_451, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred4_0 @ esk4_0 @ esk5_0)|((epred7_0 @ esk77_0 @ esk78_0)<~>(epred5_0 @ esk77_0 @ esk78_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(neg_ext,[status(thm)],[c_0_439])).
% 5.19/1.04 thf(c_0_452, plain, ![X4:a, X3:a]:(((epred5_0 @ esk8_0 @ esk9_0)|(epred3_0 @ X3 @ X4)|~((epred3_0 @ X4 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_440, c_0_408])])).
% 5.19/1.04 thf(c_0_453, plain, ((epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ esk8_0 @ esk9_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_441, c_0_442])).
% 5.19/1.04 thf(c_0_454, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred4_0 @ esk1_0 @ esk2_0)|~((epred4_0 @ esk3_0 @ esk5_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_443, c_0_408])])).
% 5.19/1.04 thf(c_0_455, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred4_0 @ esk3_0 @ esk4_0)|((epred7_0)!=(epred5_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_444, c_0_12]), c_0_40])).
% 5.19/1.04 thf(c_0_456, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred4_0 @ esk4_0 @ esk5_0)|((epred7_0)!=(epred5_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_445, c_0_12]), c_0_34])).
% 5.19/1.04 thf(c_0_457, plain, ![X4:a, X3:a]:(((epred5_0 @ esk9_0 @ esk10_0)|(epred3_0 @ X3 @ X4)|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred3_0 @ X4 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_446, c_0_129])])).
% 5.19/1.04 thf(c_0_458, plain, ![X3:a]:(((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk9_0 @ esk10_0)|(epred3_0 @ X3 @ esk5_0)|~((epred4_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_447, c_0_448])).
% 5.19/1.04 thf(c_0_459, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred5_0 @ esk9_0 @ esk10_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_449, c_0_408])])).
% 5.19/1.04 thf(c_0_460, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk9_0 @ esk10_0)|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_438]), c_0_212]), c_0_450])).
% 5.19/1.04 thf(c_0_461, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred2_0)|~((epred5_0 @ esk7_0 @ esk6_0))|((epred5_0)!=(epred7_0))|~((epred4_0 @ esk2_0 @ esk1_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_462, plain, ((epred4_0 @ esk4_0 @ esk5_0)|(epred5_0 @ esk8_0 @ esk9_0)|(epred7_0 @ esk77_0 @ esk78_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_451]), c_0_347])).
% 5.19/1.04 thf(c_0_463, plain, ![X4:a, X3:a]:(((epred5_0 @ esk8_0 @ esk9_0)|(epred3_0 @ X3 @ X4)|~((epred4_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_452, c_0_76])).
% 5.19/1.04 thf(c_0_464, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk8_0 @ esk9_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_71, c_0_453]), c_0_454])).
% 5.19/1.04 thf(c_0_465, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred4_0 @ esk3_0 @ esk4_0)|((epred7_0 @ esk65_0 @ esk66_0)<~>(epred5_0 @ esk65_0 @ esk66_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(neg_ext,[status(thm)],[c_0_455])).
% 5.19/1.04 thf(c_0_466, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred4_0 @ esk4_0 @ esk5_0)|((epred7_0 @ esk81_0 @ esk82_0)<~>(epred5_0 @ esk81_0 @ esk82_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(neg_ext,[status(thm)],[c_0_456])).
% 5.19/1.04 thf(c_0_467, plain, ![X4:a, X3:a]:(((epred5_0 @ esk9_0 @ esk10_0)|(epred3_0 @ X3 @ X4)|~((epred3_0 @ X4 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_457, c_0_408])])).
% 5.19/1.04 thf(c_0_468, plain, ((epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ esk9_0 @ esk10_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_458, c_0_459])).
% 5.19/1.04 thf(c_0_469, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred4_0 @ esk1_0 @ esk2_0)|~((epred4_0 @ esk3_0 @ esk5_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_460, c_0_408])])).
% 5.19/1.04 thf(c_0_470, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred4_0 @ esk3_0 @ esk4_0)|((epred7_0)!=(epred5_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_461, c_0_12]), c_0_34])).
% 5.19/1.04 thf(c_0_471, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred2_0)|~((epred5_0 @ esk7_0 @ esk6_0))|((epred5_0)!=(epred7_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred4_0 @ esk2_0 @ esk1_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_472, plain, ((epred4_0 @ esk4_0 @ esk5_0)|(epred5_0 @ esk8_0 @ esk9_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_451]), c_0_350]), c_0_462])).
% 5.19/1.04 thf(c_0_473, plain, ((epred3_0 @ esk2_0 @ esk1_0)|(epred5_0 @ esk8_0 @ esk9_0)), inference(spm,[status(thm)],[c_0_463, c_0_464])).
% 5.19/1.04 thf(c_0_474, plain, ((epred4_0 @ esk3_0 @ esk4_0)|(epred5_0 @ esk8_0 @ esk9_0)|(epred7_0 @ esk65_0 @ esk66_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_465]), c_0_339])).
% 5.19/1.04 thf(c_0_475, plain, ((epred4_0 @ esk4_0 @ esk5_0)|(epred5_0 @ esk9_0 @ esk10_0)|(epred7_0 @ esk81_0 @ esk82_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_466]), c_0_347])).
% 5.19/1.04 thf(c_0_476, plain, ![X4:a, X3:a]:(((epred5_0 @ esk9_0 @ esk10_0)|(epred3_0 @ X3 @ X4)|~((epred4_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_467, c_0_76])).
% 5.19/1.04 thf(c_0_477, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk9_0 @ esk10_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_71, c_0_468]), c_0_469])).
% 5.19/1.04 thf(c_0_478, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred4_0 @ esk3_0 @ esk4_0)|((epred7_0 @ esk73_0 @ esk74_0)<~>(epred5_0 @ esk73_0 @ esk74_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(neg_ext,[status(thm)],[c_0_470])).
% 5.19/1.04 thf(c_0_479, plain, ((epred5_0 @ esk8_0 @ esk9_0)|((epred7_0)!=(epred5_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_471, c_0_12]), c_0_40])).
% 5.19/1.04 thf(c_0_480, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred4_0 @ esk4_0 @ esk5_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_472, c_0_408])])).
% 5.19/1.04 thf(c_0_481, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred4_0 @ esk2_0 @ esk1_0)), inference(spm,[status(thm)],[c_0_71, c_0_473])).
% 5.19/1.04 thf(c_0_482, plain, ((epred4_0 @ esk3_0 @ esk4_0)|(epred5_0 @ esk8_0 @ esk9_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_465]), c_0_343]), c_0_474])).
% 5.19/1.04 thf(c_0_483, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred2_0)|~((epred5_0 @ esk7_0 @ esk6_0))|((epred5_0)!=(epred7_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred4_0 @ esk2_0 @ esk1_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_484, plain, ((epred4_0 @ esk4_0 @ esk5_0)|(epred5_0 @ esk9_0 @ esk10_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_466]), c_0_350]), c_0_475])).
% 5.19/1.04 thf(c_0_485, plain, ((epred3_0 @ esk2_0 @ esk1_0)|(epred5_0 @ esk9_0 @ esk10_0)), inference(spm,[status(thm)],[c_0_476, c_0_477])).
% 5.19/1.04 thf(c_0_486, plain, ((epred4_0 @ esk3_0 @ esk4_0)|(epred5_0 @ esk9_0 @ esk10_0)|(epred7_0 @ esk73_0 @ esk74_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_478]), c_0_339])).
% 5.19/1.04 thf(c_0_487, plain, ((epred5_0 @ esk8_0 @ esk9_0)|((epred7_0 @ esk21_0 @ esk22_0)<~>(epred5_0 @ esk21_0 @ esk22_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(neg_ext,[status(thm)],[c_0_479])).
% 5.19/1.04 thf(c_0_488, plain, ((epred4_0 @ esk4_0 @ esk5_0)|(epred5_0 @ esk8_0 @ esk9_0)), inference(spm,[status(thm)],[c_0_480, c_0_481])).
% 5.19/1.04 thf(c_0_489, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred4_0 @ esk3_0 @ esk4_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_482, c_0_408])])).
% 5.19/1.04 thf(c_0_490, plain, ((epred5_0 @ esk9_0 @ esk10_0)|((epred7_0)!=(epred5_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_483, c_0_12]), c_0_34])).
% 5.19/1.04 thf(c_0_491, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred4_0 @ esk4_0 @ esk5_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_484, c_0_408])])).
% 5.19/1.04 thf(c_0_492, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred4_0 @ esk2_0 @ esk1_0)), inference(spm,[status(thm)],[c_0_71, c_0_485])).
% 5.19/1.04 thf(c_0_493, plain, ((epred4_0 @ esk3_0 @ esk4_0)|(epred5_0 @ esk9_0 @ esk10_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_478]), c_0_343]), c_0_486])).
% 5.19/1.04 thf(c_0_494, plain, ((epred5_0 @ esk8_0 @ esk9_0)|~((epred7_0 @ esk21_0 @ esk22_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_487]), c_0_367])).
% 5.19/1.04 thf(c_0_495, plain, ![X3:a]:(((epred5_0 @ esk8_0 @ esk9_0)|(epred3_0 @ X3 @ esk5_0)|~((epred4_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_430, c_0_488])).
% 5.19/1.04 thf(c_0_496, plain, ((epred4_0 @ esk3_0 @ esk4_0)|(epred5_0 @ esk8_0 @ esk9_0)), inference(spm,[status(thm)],[c_0_489, c_0_481])).
% 5.19/1.04 thf(c_0_497, plain, ((epred5_0 @ esk9_0 @ esk10_0)|((epred7_0 @ esk23_0 @ esk24_0)<~>(epred5_0 @ esk23_0 @ esk24_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(neg_ext,[status(thm)],[c_0_490])).
% 5.19/1.04 thf(c_0_498, plain, ((epred4_0 @ esk4_0 @ esk5_0)|(epred5_0 @ esk9_0 @ esk10_0)), inference(spm,[status(thm)],[c_0_491, c_0_492])).
% 5.19/1.04 thf(c_0_499, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred4_0 @ esk3_0 @ esk4_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_493, c_0_408])])).
% 5.19/1.04 thf(c_0_500, plain, ((epred5_0 @ esk8_0 @ esk9_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_487]), c_0_203]), c_0_494])).
% 5.19/1.04 thf(c_0_501, plain, ((epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ esk8_0 @ esk9_0)), inference(spm,[status(thm)],[c_0_495, c_0_496])).
% 5.19/1.04 thf(c_0_502, plain, ((epred5_0 @ esk9_0 @ esk10_0)|~((epred7_0 @ esk23_0 @ esk24_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_497]), c_0_367])).
% 5.19/1.04 thf(c_0_503, plain, ![X3:a]:(((epred5_0 @ esk9_0 @ esk10_0)|(epred3_0 @ X3 @ esk5_0)|~((epred4_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_447, c_0_498])).
% 5.19/1.04 thf(c_0_504, plain, ((epred4_0 @ esk3_0 @ esk4_0)|(epred5_0 @ esk9_0 @ esk10_0)), inference(spm,[status(thm)],[c_0_499, c_0_492])).
% 5.19/1.04 thf(c_0_505, plain, ((epred5_0 @ esk8_0 @ esk9_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_500, c_0_408])])).
% 5.19/1.04 thf(c_0_506, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred4_0 @ esk3_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_71, c_0_501])).
% 5.19/1.04 thf(c_0_507, plain, ((epred5_0 @ esk9_0 @ esk10_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_497]), c_0_203]), c_0_502])).
% 5.19/1.04 thf(c_0_508, plain, ((epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ esk9_0 @ esk10_0)), inference(spm,[status(thm)],[c_0_503, c_0_504])).
% 5.19/1.04 thf(c_0_509, plain, (epred5_0 @ esk8_0 @ esk9_0), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_505, c_0_506]), c_0_481])).
% 5.19/1.04 thf(c_0_510, plain, ((epred5_0 @ esk9_0 @ esk10_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_507, c_0_408])])).
% 5.19/1.04 thf(c_0_511, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred4_0 @ esk3_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_71, c_0_508])).
% 5.19/1.04 thf(c_0_512, plain, ((epred6_0 @ esk9_0 @ esk8_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_240, c_0_509])).
% 5.19/1.04 thf(c_0_513, plain, (epred5_0 @ esk9_0 @ esk10_0), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_510, c_0_511]), c_0_492])).
% 5.19/1.04 thf(c_0_514, plain, ((epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred2_0)|~((epred5_0 @ esk8_0 @ esk10_0))|~((epred5_0 @ esk7_0 @ esk6_0))|((epred5_0)!=(epred7_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_515, plain, ![X3:a]:(((epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred6_0 @ X3 @ esk8_0)|~((epred6_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_246, c_0_512])).
% 5.19/1.04 thf(c_0_516, plain, ((epred6_0 @ esk10_0 @ esk9_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_240, c_0_513])).
% 5.19/1.04 thf(c_0_517, plain, ((epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred7_0)!=(epred5_0))|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_514, c_0_12]), c_0_45])).
% 5.19/1.04 thf(c_0_518, plain, ((epred6_0 @ esk9_0 @ esk8_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk3_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_249, c_0_509])).
% 5.19/1.04 thf(c_0_519, plain, ((epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred2_0)|~((epred5_0 @ esk8_0 @ esk10_0))|~((epred5_0 @ esk7_0 @ esk6_0))|((epred5_0)!=(epred7_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_520, plain, ((epred6_0 @ esk10_0 @ esk8_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_515, c_0_516])).
% 5.19/1.04 thf(c_0_521, plain, ((epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[inference(neg_ext,[status(thm)],[c_0_517]), c_0_138])).
% 5.19/1.04 thf(c_0_522, plain, ![X3:a]:(((epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred6_0 @ X3 @ esk8_0)|~((epred6_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_253, c_0_518])).
% 5.19/1.04 thf(c_0_523, plain, ((epred6_0 @ esk10_0 @ esk9_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk3_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_249, c_0_513])).
% 5.19/1.04 thf(c_0_524, plain, ((epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|((epred7_0)!=(epred5_0))|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_519, c_0_12]), c_0_45])).
% 5.19/1.04 thf(c_0_525, plain, ((epred6_0 @ esk8_0 @ esk10_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk4_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_229, c_0_520])).
% 5.19/1.04 thf(c_0_526, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk4_0 @ esk5_0)|~((epred5_0 @ esk8_0 @ esk10_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_521, c_0_408])])).
% 5.19/1.04 thf(c_0_527, plain, ((epred6_0 @ esk10_0 @ esk8_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_522, c_0_523])).
% 5.19/1.04 thf(c_0_528, plain, ((epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[inference(neg_ext,[status(thm)],[c_0_524]), c_0_160])).
% 5.19/1.04 thf(c_0_529, plain, ((epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_260, c_0_525]), c_0_526])).
% 5.19/1.04 thf(c_0_530, plain, ((epred6_0 @ esk8_0 @ esk10_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk3_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_236, c_0_527])).
% 5.19/1.04 thf(c_0_531, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk3_0 @ esk4_0)|~((epred5_0 @ esk8_0 @ esk10_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_528, c_0_408])])).
% 5.19/1.04 thf(c_0_532, plain, ![X3:a]:(((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ X3 @ esk5_0)|~((epred4_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_265, c_0_529])).
% 5.19/1.04 thf(c_0_533, plain, ((epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_260, c_0_530]), c_0_531])).
% 5.19/1.04 thf(c_0_534, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred3_0 @ esk3_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_532, c_0_533])).
% 5.19/1.04 thf(c_0_535, plain, ![X3:a, X4:a, X5:a]:(((epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ X3 @ X4)|~((epred5_0 @ X5 @ X4))|~((epred5_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_239, c_0_534])).
% 5.19/1.04 thf(c_0_536, plain, ![X3:a]:(((epred3_0 @ esk3_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ X3 @ esk10_0)|~((epred5_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_535, c_0_513])).
% 5.19/1.04 thf(c_0_537, plain, ((epred5_0 @ esk8_0 @ esk10_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk3_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_536, c_0_509])).
% 5.19/1.04 thf(c_0_538, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred4_0 @ esk3_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_71, c_0_537])).
% 5.19/1.04 thf(c_0_539, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_276, c_0_538])).
% 5.19/1.04 thf(c_0_540, plain, ![X3:a, X4:a, X5:a]:(((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ X3 @ X4)|~((epred5_0 @ X5 @ X4))|~((epred5_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_239, c_0_539])).
% 5.19/1.04 thf(c_0_541, plain, ![X3:a]:(((epred5_0 @ esk8_0 @ esk10_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ X3 @ esk10_0)|~((epred5_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_540, c_0_513])).
% 5.19/1.04 thf(c_0_542, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk8_0 @ esk10_0)), inference(spm,[status(thm)],[c_0_541, c_0_509])).
% 5.19/1.04 thf(c_0_543, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred3_0 @ esk2_0 @ esk1_0)), inference(spm,[status(thm)],[c_0_282, c_0_542])).
% 5.19/1.04 thf(c_0_544, plain, ![X3:a, X4:a, X5:a]:(((epred3_0 @ esk2_0 @ esk1_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ X3 @ X4)|~((epred5_0 @ X5 @ X4))|~((epred5_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_239, c_0_543])).
% 5.19/1.04 thf(c_0_545, plain, ![X3:a]:(((epred5_0 @ esk8_0 @ esk10_0)|(epred3_0 @ esk2_0 @ esk1_0)|(epred5_0 @ X3 @ esk10_0)|~((epred5_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_544, c_0_513])).
% 5.19/1.04 thf(c_0_546, plain, ((epred3_0 @ esk2_0 @ esk1_0)|(epred5_0 @ esk8_0 @ esk10_0)), inference(spm,[status(thm)],[c_0_545, c_0_509])).
% 5.19/1.04 thf(c_0_547, plain, ((epred5_0 @ esk8_0 @ esk10_0)|(epred4_0 @ esk2_0 @ esk1_0)), inference(spm,[status(thm)],[c_0_71, c_0_546])).
% 5.19/1.04 thf(c_0_548, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred4_0 @ esk4_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_289, c_0_547])).
% 5.19/1.04 thf(c_0_549, plain, ![X3:a, X4:a, X5:a]:(((epred4_0 @ esk4_0 @ esk5_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ X3 @ X4)|~((epred5_0 @ X5 @ X4))|~((epred5_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_239, c_0_548])).
% 5.19/1.04 thf(c_0_550, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred4_0 @ esk3_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_293, c_0_547])).
% 5.19/1.04 thf(c_0_551, plain, ![X3:a]:(((epred5_0 @ esk8_0 @ esk10_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred5_0 @ X3 @ esk10_0)|~((epred5_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_549, c_0_513])).
% 5.19/1.04 thf(c_0_552, plain, ![X3:a, X4:a, X5:a]:(((epred4_0 @ esk3_0 @ esk4_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ X3 @ X4)|~((epred5_0 @ X5 @ X4))|~((epred5_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_239, c_0_550])).
% 5.19/1.04 thf(c_0_553, plain, ((epred4_0 @ esk4_0 @ esk5_0)|(epred5_0 @ esk8_0 @ esk10_0)), inference(spm,[status(thm)],[c_0_551, c_0_509])).
% 5.19/1.04 thf(c_0_554, plain, ![X3:a]:(((epred5_0 @ esk8_0 @ esk10_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred5_0 @ X3 @ esk10_0)|~((epred5_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_552, c_0_513])).
% 5.19/1.04 thf(c_0_555, plain, ![X3:a]:(((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred3_0 @ X3 @ esk5_0)|~((epred4_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_265, c_0_553])).
% 5.19/1.04 thf(c_0_556, plain, ((epred4_0 @ esk3_0 @ esk4_0)|(epred5_0 @ esk8_0 @ esk10_0)), inference(spm,[status(thm)],[c_0_554, c_0_509])).
% 5.19/1.04 thf(c_0_557, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ esk8_0 @ esk10_0)), inference(spm,[status(thm)],[c_0_555, c_0_556])).
% 5.19/1.04 thf(c_0_558, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk8_0 @ esk10_0)|(epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ X3 @ X4)|~((epred5_0 @ X5 @ X4))|~((epred5_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_239, c_0_557])).
% 5.19/1.04 thf(c_0_559, plain, ![X3:a]:(((epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ X3 @ esk10_0)|~((epred5_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_558, c_0_513])).
% 5.19/1.04 thf(c_0_560, plain, ((epred5_0 @ esk8_0 @ esk10_0)|(epred3_0 @ esk3_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_559, c_0_509])).
% 5.19/1.04 thf(c_0_561, plain, ![X3:a, X4:a]:(((epred3_0 @ X4 @ X3)|(epred2_0)|~((epred5_0 @ esk8_0 @ esk10_0))|~((epred5_0 @ esk7_0 @ esk6_0))|((epred5_0)!=(epred7_0))|~((epred3_0 @ X3 @ X4)))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_562, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ X3 @ X4)|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ X5 @ X4))|~((epred5_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_305, c_0_547])).
% 5.19/1.04 thf(c_0_563, plain, ((epred5_0 @ esk8_0 @ esk10_0)|(epred4_0 @ esk3_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_71, c_0_560])).
% 5.19/1.04 thf(c_0_564, plain, ![X3:a, X4:a, X5:a]:(((epred3_0 @ X3 @ X5)|(epred2_0)|~((epred5_0 @ esk8_0 @ esk10_0))|~((epred5_0 @ esk7_0 @ esk6_0))|((epred5_0)!=(epred7_0))|~((epred3_0 @ X3 @ X4))|~((epred3_0 @ X4 @ X5)))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_565, plain, ![X4:a, X3:a]:(((epred3_0 @ X3 @ X4)|((epred7_0)!=(epred5_0))|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred5_0 @ esk8_0 @ esk10_0))|~((epred3_0 @ X4 @ X3)))), inference(sr,[status(thm)],[c_0_561, c_0_12])).
% 5.19/1.04 thf(c_0_566, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ X3 @ X4)|~((epred5_0 @ X5 @ X4))|~((epred5_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_562, c_0_563])).
% 5.19/1.04 thf(c_0_567, plain, ![X3:a, X4:a, X5:a]:(((epred3_0 @ X3 @ X4)|((epred7_0)!=(epred5_0))|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred5_0 @ esk8_0 @ esk10_0))|~((epred3_0 @ X5 @ X4))|~((epred3_0 @ X3 @ X5)))), inference(sr,[status(thm)],[c_0_564, c_0_12])).
% 5.19/1.04 thf(c_0_568, plain, ![X4:a, X3:a]:(((epred3_0 @ X3 @ X4)|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred5_0 @ esk8_0 @ esk10_0))|~((epred3_0 @ X4 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_565, c_0_129])])).
% 5.19/1.04 thf(c_0_569, plain, ![X3:a]:(((epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ X3 @ esk10_0)|~((epred5_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_566, c_0_513])).
% 5.19/1.04 thf(c_0_570, plain, ((epred4_0 @ esk3_0 @ esk4_0)|(epred2_0)|~((epred5_0 @ esk8_0 @ esk10_0))|~((epred5_0 @ esk7_0 @ esk6_0))|((epred5_0)!=(epred7_0))|~((epred4_0 @ esk2_0 @ esk1_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_571, plain, ![X3:a, X4:a, X5:a]:(((epred3_0 @ X3 @ X4)|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred5_0 @ esk8_0 @ esk10_0))|~((epred3_0 @ X5 @ X4))|~((epred3_0 @ X3 @ X5)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_567, c_0_129])])).
% 5.19/1.04 thf(c_0_572, plain, ![X4:a, X3:a]:(((epred3_0 @ X3 @ X4)|~((epred5_0 @ esk8_0 @ esk10_0))|~((epred3_0 @ X4 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_568, c_0_408])])).
% 5.19/1.04 thf(c_0_573, plain, (epred5_0 @ esk8_0 @ esk10_0), inference(spm,[status(thm)],[c_0_569, c_0_509])).
% 5.19/1.04 thf(c_0_574, plain, ((epred4_0 @ esk3_0 @ esk4_0)|((epred7_0)!=(epred5_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_570, c_0_12]), c_0_45])).
% 5.19/1.04 thf(c_0_575, plain, ![X3:a, X4:a, X5:a]:(((epred3_0 @ X3 @ X4)|~((epred5_0 @ esk8_0 @ esk10_0))|~((epred3_0 @ X5 @ X4))|~((epred3_0 @ X3 @ X5)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_571, c_0_408])])).
% 5.19/1.04 thf(c_0_576, plain, ![X4:a, X3:a]:(((epred3_0 @ X3 @ X4)|~((epred3_0 @ X4 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_572, c_0_573])])).
% 5.19/1.04 thf(c_0_577, plain, ((epred4_0 @ esk3_0 @ esk4_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_574, c_0_129])])).
% 5.19/1.04 thf(c_0_578, plain, ((epred2_0)|~((epred5_0 @ esk8_0 @ esk10_0))|~((epred5_0 @ esk7_0 @ esk6_0))|((epred5_0)!=(epred7_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred4_0 @ esk2_0 @ esk1_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_579, plain, ![X3:a, X4:a, X5:a]:(((epred3_0 @ X3 @ X4)|~((epred3_0 @ X5 @ X4))|~((epred3_0 @ X3 @ X5)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_575, c_0_573])])).
% 5.19/1.04 thf(c_0_580, plain, ![X4:a, X3:a]:(((epred3_0 @ X3 @ X4)|~((epred4_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_576, c_0_76])).
% 5.19/1.04 thf(c_0_581, plain, ((epred4_0 @ esk3_0 @ esk4_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_577, c_0_408])])).
% 5.19/1.04 thf(c_0_582, plain, ![X1:a > a > $o, X2:a > a > $o, X3:a, X6:a > a > $o, X4:a]:(((X1 @ X3 @ X4)|~((epred1_3 @ X1 @ X2 @ X6))|~((X2 @ X3 @ X4)))), inference(dynamic_cnf,[status(thm)],[c_0_353])).
% 5.19/1.04 thf(c_0_583, plain, ![X1:a > a > $o, X2:a > a > $o, X3:a, X6:a > a > $o, X4:a]:(((X1 @ X3 @ X4)|~((epred1_3 @ X2 @ X1 @ X6))|~((X6 @ X3 @ X4)))), inference(dynamic_cnf,[status(thm)],[c_0_352])).
% 5.19/1.04 thf(c_0_584, plain, (((epred7_0)!=(epred5_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_578, c_0_12]), c_0_45])).
% 5.19/1.04 thf(c_0_585, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred2_0)|~((epred5_0 @ esk8_0 @ esk10_0))|~((epred5_0 @ esk7_0 @ esk6_0))|((epred5_0)!=(epred7_0))|~((epred4_0 @ esk3_0 @ esk5_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_586, plain, ![X3:a, X5:a, X4:a]:(((epred3_0 @ X3 @ X4)|~((epred3_0 @ X3 @ X5))|~((epred4_0 @ X5 @ X4)))), inference(spm,[status(thm)],[c_0_579, c_0_76])).
% 5.19/1.04 thf(c_0_587, plain, ![X4:a, X3:a]:(((epred4_0 @ X3 @ X4)|~((epred4_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_71, c_0_580])).
% 5.19/1.04 thf(c_0_588, plain, ((epred4_0 @ esk3_0 @ esk4_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_581, c_0_573])])).
% 5.19/1.04 thf(c_0_589, plain, ((epred4_0 @ esk4_0 @ esk5_0)|(epred2_0)|~((epred5_0 @ esk8_0 @ esk10_0))|~((epred5_0 @ esk7_0 @ esk6_0))|((epred5_0)!=(epred7_0))|~((epred4_0 @ esk2_0 @ esk1_0))|((epred4_0)!=(epred3_0))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 5.19/1.04 thf(c_0_590, plain, ![X3:a, X4:a]:(((epred7_0 @ X3 @ X4)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred6_0 @ X3 @ X4)))), inference(spm,[status(thm)],[c_0_582, c_0_92])).
% 5.19/1.04 thf(c_0_591, plain, ![X3:a, X4:a]:(((epred6_0 @ X3 @ X4)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ X3 @ X4)))), inference(spm,[status(thm)],[c_0_583, c_0_92])).
% 5.19/1.04 thf(c_0_592, plain, (((epred7_0 @ esk11_0 @ esk12_0)<~>(epred5_0 @ esk11_0 @ esk12_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(neg_ext,[status(thm)],[c_0_584])).
% 5.19/1.04 thf(c_0_593, plain, ((epred4_0 @ esk1_0 @ esk2_0)|((epred7_0)!=(epred5_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_585, c_0_12]), c_0_45])).
% 5.19/1.04 thf(c_0_594, plain, ![X5:a, X4:a, X3:a]:(((epred3_0 @ X3 @ X4)|~((epred4_0 @ X5 @ X4))|~((epred4_0 @ X5 @ X3)))), inference(spm,[status(thm)],[c_0_586, c_0_580])).
% 5.19/1.04 thf(c_0_595, plain, ((epred4_0 @ esk4_0 @ esk3_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(spm,[status(thm)],[c_0_587, c_0_588])).
% 5.19/1.04 thf(c_0_596, plain, ((epred4_0 @ esk4_0 @ esk5_0)|((epred7_0)!=(epred5_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_589, c_0_12]), c_0_45])).
% 5.19/1.04 thf(c_0_597, plain, ![X3:a, X4:a]:(((epred7_0 @ X3 @ X4)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ X3 @ X4)))), inference(spm,[status(thm)],[c_0_590, c_0_591])).
% 5.19/1.04 thf(c_0_598, plain, (~((epred7_0 @ esk11_0 @ esk12_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_592]), c_0_367])).
% 5.19/1.04 thf(c_0_599, plain, ![X3:a, X4:a, X5:a]:(((epred3_0 @ X3 @ X4)|~((epred4_0 @ X5 @ X4))|~((epred4_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_586, c_0_76])).
% 5.19/1.04 thf(c_0_600, plain, ((epred4_0 @ esk1_0 @ esk2_0)|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_593, c_0_129])])).
% 5.19/1.04 thf(c_0_601, plain, ![X3:a]:(((epred3_0 @ X3 @ esk3_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk4_0 @ X3)))), inference(spm,[status(thm)],[c_0_594, c_0_595])).
% 5.19/1.04 thf(c_0_602, plain, ((epred4_0 @ esk4_0 @ esk5_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_596, c_0_129])])).
% 5.19/1.04 thf(c_0_603, plain, (~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_592]), c_0_597]), c_0_598])).
% 5.19/1.04 thf(c_0_604, plain, ![X3:a]:(((epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ X3 @ esk5_0)|~((epred4_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_599, c_0_529])).
% 5.19/1.04 thf(c_0_605, plain, ((epred4_0 @ esk1_0 @ esk2_0)|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_600, c_0_408])])).
% 5.19/1.04 thf(c_0_606, plain, ![X3:a]:(((epred3_0 @ esk3_0 @ X3)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk4_0 @ X3)))), inference(spm,[status(thm)],[c_0_576, c_0_601])).
% 5.19/1.04 thf(c_0_607, plain, ((epred4_0 @ esk4_0 @ esk5_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_602, c_0_408])])).
% 5.19/1.04 thf(c_0_608, plain, (~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_603, c_0_408])])).
% 5.19/1.04 thf(c_0_609, plain, ((epred3_0 @ esk3_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_604, c_0_533])).
% 5.19/1.04 thf(c_0_610, plain, ((epred4_0 @ esk1_0 @ esk2_0)|~((epred4_0 @ esk3_0 @ esk5_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_605, c_0_573])])).
% 5.19/1.04 thf(c_0_611, plain, ![X3:a]:(((epred4_0 @ esk3_0 @ X3)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk4_0 @ X3)))), inference(spm,[status(thm)],[c_0_71, c_0_606])).
% 5.19/1.04 thf(c_0_612, plain, ((epred4_0 @ esk4_0 @ esk5_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_607, c_0_573])])).
% 5.19/1.04 thf(c_0_613, plain, (~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_608, c_0_573])])).
% 5.19/1.04 thf(c_0_614, plain, (epred4_0 @ esk1_0 @ esk2_0), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_71, c_0_609]), c_0_610])).
% 5.19/1.04 thf(c_0_615, plain, ~((epred4_0 @ esk2_0 @ esk1_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_611, c_0_612]), c_0_613])).
% 5.19/1.04 thf(c_0_616, plain, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_587, c_0_614]), c_0_615]), ['proof']).
% 5.19/1.04 % SZS output end CNFRefutation
% 5.19/1.04 % Parsed axioms : 2
% 5.19/1.04 % Removed by relevancy pruning/SinE : 1
% 5.19/1.04 % Initial clauses : 70
% 5.19/1.04 % Removed in clause preprocessing : 0
% 5.19/1.04 % Initial clauses in saturation : 70
% 5.19/1.04 % Processed clauses : 6064
% 5.19/1.04 % ...of these trivial : 89
% 5.19/1.04 % ...subsumed : 2819
% 5.19/1.04 % ...remaining for further processing : 3156
% 5.19/1.04 % Other redundant clauses eliminated : 0
% 5.19/1.04 % Clauses deleted for lack of memory : 0
% 5.19/1.04 % Backward-subsumed : 1910
% 5.19/1.04 % Backward-rewritten : 724
% 5.19/1.04 % Generated clauses : 14309
% 5.19/1.04 % ...of the previous two non-redundant : 12745
% 5.19/1.04 % ...aggressively subsumed : 0
% 5.19/1.04 % Contextual simplify-reflections : 200
% 5.19/1.04 % Paramodulations : 12666
% 5.19/1.04 % Factorizations : 0
% 5.19/1.04 % NegExts : 155
% 5.19/1.04 % Equation resolutions : 0
% 5.19/1.04 % Disequality decompositions : 0
% 5.19/1.04 % Total rewrite steps : 1494
% 5.19/1.04 % ...of those cached : 1359
% 5.19/1.04 % Propositional unsat checks : 0
% 5.19/1.04 % Propositional check models : 0
% 5.19/1.04 % Propositional check unsatisfiable : 0
% 5.19/1.04 % Propositional clauses : 0
% 5.19/1.04 % Propositional clauses after purity: 0
% 5.19/1.04 % Propositional unsat core size : 0
% 5.19/1.04 % Propositional preprocessing time : 0.000
% 5.19/1.04 % Propositional encoding time : 0.000
% 5.19/1.04 % Propositional solver time : 0.000
% 5.19/1.04 % Success case prop preproc time : 0.000
% 5.19/1.04 % Success case prop encoding time : 0.000
% 5.19/1.04 % Success case prop solver time : 0.000
% 5.19/1.04 % Current number of processed clauses : 52
% 5.19/1.04 % Positive orientable unit clauses : 20
% 5.19/1.04 % Positive unorientable unit clauses: 0
% 5.19/1.04 % Negative unit clauses : 2
% 5.19/1.04 % Non-unit-clauses : 30
% 5.19/1.04 % Current number of unprocessed clauses: 1264
% 5.19/1.04 % ...number of literals in the above : 5208
% 5.19/1.04 % Current number of archived formulas : 0
% 5.19/1.04 % Current number of archived clauses : 3104
% 5.19/1.04 % Clause-clause subsumption calls (NU) : 229124
% 5.19/1.04 % Rec. Clause-clause subsumption calls : 80871
% 5.19/1.04 % Non-unit clause-clause subsumptions : 4834
% 5.19/1.04 % Unit Clause-clause subsumption calls : 1660
% 5.19/1.04 % Rewrite failures with RHS unbound : 0
% 5.19/1.04 % BW rewrite match attempts : 47
% 5.19/1.04 % BW rewrite match successes : 43
% 5.19/1.04 % Condensation attempts : 0
% 5.19/1.04 % Condensation successes : 0
% 5.19/1.04 % Termbank termtop insertions : 349639
% 5.19/1.04 % Search garbage collected termcells : 1070
% 5.19/1.04
% 5.19/1.04 % -------------------------------------------------
% 5.19/1.04 % User time : 0.639 s
% 5.19/1.04 % System time : 0.015 s
% 5.19/1.04 % Total time : 0.654 s
% 5.19/1.04 % Maximum resident set size: 4416 pages
% 5.19/1.04
% 5.19/1.04 % -------------------------------------------------
% 5.19/1.04 % User time : 2.047 s
% 5.19/1.04 % System time : 0.052 s
% 5.19/1.04 % Total time : 2.099 s
% 5.19/1.04 % Maximum resident set size: 4864 pages
% 5.19/1.04 % E exiting
%------------------------------------------------------------------------------