E---3.5.1.THM-CRf.s

%------------------------------------------------------------------------------
% File     : E---3.5.1
% Problem  : SEV040^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM

% Computer : n004.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:34:45 AM UTC 2026

% Result   : Theorem 5.97s 1.22s
% Output   : CNFRefutation 5.97s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04  % Problem  : SEV040^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06  % Command  : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.26  % Computer : n004.cluster.edu
% 0.08/0.26  % Model    : x86_64 x86_64
% 0.08/0.26  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.26  % Memory   : 8046.5625MB
% 0.08/0.26  % OS       : Linux 6.8.0-71-generic
% 0.08/0.26  % CPULimit : 300
% 0.08/0.26  % WCLimit  : 300
% 0.08/0.26  % DateTime : Tue Sep 29 15:04:43 UTC 2026
% 0.08/0.26  % CPUTime  : 
% 0.08/0.26  Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.23/0.32  Running higher-order theorem proving
% 0.23/0.34  Running: /export/starexec/sandbox/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/sandbox/tmp/tmp.14fIhB7OC5/E---3.1_1402935.p
% 5.97/1.22  % Version: 3.5.1-ho
% 5.97/1.22  % Preprocessing class: HSMSSMSSSSSNHHA.
% 5.97/1.22  % Scheduled 6 strats onto 8 cores with 300 seconds (2400 total)
% 5.97/1.22  % Starting full_lambda_6 with 900s (3) cores
% 5.97/1.22  % Starting post_as_ho1 with 300s (1) cores
% 5.97/1.22  % Starting lpo6_lambda_fix with 300s (1) cores
% 5.97/1.22  % Starting ho_unfolding_1 with 300s (1) cores
% 5.97/1.22  % Starting new_ho_10_unif with 300s (1) cores
% 5.97/1.22  % Starting ho_unfolding_2 with 300s (1) cores
% 5.97/1.22  % full_lambda_6 with pid 1402948 completed with status 0
% 5.97/1.22  % Result found by full_lambda_6
% 5.97/1.22  % Preprocessing class: HSMSSMSSSSSNHHA.
% 5.97/1.22  % Scheduled 6 strats onto 8 cores with 300 seconds (2400 total)
% 5.97/1.22  % Starting full_lambda_6 with 900s (3) cores
% 5.97/1.22  % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 1, sine = GSinE(CountTerms,hypos,4,,4,20000,1.0,true))
% 5.97/1.22  % SinE strategy is GSinE(CountTerms,hypos,4,,4,20000,1.0,true)
% 5.97/1.22  % Search class: HGUSF-FSMF00-SHHFFFBN
% 5.97/1.22  % partial match(3): HGUNF-FFMF00-SHHFFMBN
% 5.97/1.22  % Scheduled 7 strats onto 3 cores with 900 seconds (900 total)
% 5.97/1.22  % Starting SubtermCWHack with 82s (1) cores
% 5.97/1.22  % Starting full_lambda_6 with 91s (1) cores
% 5.97/1.22  % Starting sh3 with 163s (1) cores
% 5.97/1.22  % sh3 with pid 1402957 completed with status 0
% 5.97/1.22  % Result found by sh3
% 5.97/1.22  % Preprocessing class: HSMSSMSSSSSNHHA.
% 5.97/1.22  % Scheduled 6 strats onto 8 cores with 300 seconds (2400 total)
% 5.97/1.22  % Starting full_lambda_6 with 900s (3) cores
% 5.97/1.22  % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 1, sine = GSinE(CountTerms,hypos,4,,4,20000,1.0,true))
% 5.97/1.22  % SinE strategy is GSinE(CountTerms,hypos,4,,4,20000,1.0,true)
% 5.97/1.22  % Search class: HGUSF-FSMF00-SHHFFFBN
% 5.97/1.22  % partial match(3): HGUNF-FFMF00-SHHFFMBN
% 5.97/1.22  % Scheduled 7 strats onto 3 cores with 900 seconds (900 total)
% 5.97/1.22  % Starting SubtermCWHack with 82s (1) cores
% 5.97/1.22  % Starting full_lambda_6 with 91s (1) cores
% 5.97/1.22  % Starting sh3 with 163s (1) cores
% 5.97/1.22  % Preprocessing time       : 0.004 s
% 5.97/1.22  % Presaturation interreduction done
% 5.97/1.22  
% 5.97/1.22  % Proof found!
% 5.97/1.22  % SZS status Theorem
% 5.97/1.22  % SZS output start CNFRefutation
% 5.97/1.22  thf(decl_sort1, type, a: $tType).
% 5.97/1.22  thf(decl_23, type, epred1_3: (a > a > $o) > (a > a > $o) > (a > a > $o) > $o).
% 5.97/1.22  thf(decl_24, type, epred2_0: $o).
% 5.97/1.22  thf(decl_25, type, epred3_0: a > a > $o).
% 5.97/1.22  thf(decl_26, type, epred4_0: a > a > $o).
% 5.97/1.22  thf(decl_27, type, esk1_0: a).
% 5.97/1.22  thf(decl_28, type, esk2_0: a).
% 5.97/1.22  thf(decl_29, type, esk3_0: a).
% 5.97/1.22  thf(decl_30, type, esk4_0: a).
% 5.97/1.22  thf(decl_31, type, esk5_0: a).
% 5.97/1.22  thf(decl_32, type, epred5_0: a > a > $o).
% 5.97/1.22  thf(decl_33, type, epred6_0: a > a > $o).
% 5.97/1.22  thf(decl_34, type, epred7_0: a > a > $o).
% 5.97/1.22  thf(decl_35, type, esk6_0: a).
% 5.97/1.22  thf(decl_36, type, esk7_0: a).
% 5.97/1.22  thf(decl_37, type, esk8_0: a).
% 5.97/1.22  thf(decl_38, type, esk9_0: a).
% 5.97/1.22  thf(decl_39, type, esk10_0: a).
% 5.97/1.22  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/sandbox/tmp/tmp.14fIhB7OC5/E---3.1_1402935.p', cTHM515_pme)).
% 5.97/1.22  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.97/1.22  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.97/1.22  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.97/1.22  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.97/1.22  thf(c_0_5, 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.97/1.22  thf(c_0_6, 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.97/1.22  thf(c_0_7, 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.97/1.22  thf(c_0_8, 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_5])])])])])).
% 5.97/1.22  thf(c_0_9, 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_6])])])])])])).
% 5.97/1.22  thf(c_0_10, negated_conjecture, (~((epred2_0))|((^[Z0:a > a > $o, Z1:a > a > $o]:(((((![X1954:a, X1955:a]:((((Z0 @ X1954 @ X1955))=>((Z0 @ X1955 @ X1954)))))&(![X1956:a, X1957:a, X1958:a]:((((((Z0 @ X1956 @ X1957))&((Z0 @ X1957 @ X1958))))=>((Z0 @ X1956 @ X1958)))))))&(((Z0)=(Z1))))))!=(^[Z0:a > a > $o, Z1:a > a > $o]:(((((![X1959:a, X1960:a]:((((Z0 @ X1959 @ X1960))=>((Z0 @ X1960 @ X1959)))))&(![X1961:a, X1962:a, X1963:a]:((((((Z0 @ X1961 @ X1962))&((Z0 @ X1962 @ X1963))))=>((Z0 @ X1961 @ X1963)))))))&(((Z0)=(Z1)))))))), inference(split_conjunct,[status(thm)],[c_0_7])).
% 5.97/1.22  thf(c_0_11, 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_8])).
% 5.97/1.22  thf(c_0_12, plain, ((epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)|((epred3_0)=(epred4_0))|(epred2_0)), inference(split_conjunct,[status(thm)],[c_0_9])).
% 5.97/1.22  thf(c_0_13, negated_conjecture, ~((epred2_0)), inference(cn,[status(thm)],[c_0_10])).
% 5.97/1.22  thf(c_0_14, plain, ![X81:a, X82: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_11])).
% 5.97/1.22  thf(c_0_15, plain, (((epred3_0)=(epred4_0))|(epred1_3 @ epred7_0 @ epred6_0 @ epred5_0)), inference(sr,[status(thm)],[c_0_12, c_0_13])).
% 5.97/1.22  thf(c_0_16, 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_8])).
% 5.97/1.22  thf(c_0_17, 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_8])).
% 5.97/1.22  thf(c_0_18, 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_14])).
% 5.97/1.22  thf(c_0_19, 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_9])).
% 5.97/1.22  thf(c_0_20, plain, (((epred3_0)=(epred4_0))|((epred6_0)=(epred5_0))), inference(spm,[status(thm)],[c_0_11, c_0_15])).
% 5.97/1.22  thf(c_0_21, plain, (((epred3_0)=(epred4_0))|((epred6_0)=(epred7_0))), inference(spm,[status(thm)],[c_0_16, c_0_15])).
% 5.97/1.22  thf(c_0_22, 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_8])).
% 5.97/1.22  thf(c_0_23, plain, ![X4:a, X3:a]:((((epred3_0)=(epred4_0))|(epred6_0 @ X3 @ X4)|~((epred6_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_17, c_0_15])).
% 5.97/1.22  thf(c_0_24, plain, ![X3:a, X4:a]:((((epred3_0)=(epred4_0))|(epred6_0 @ X3 @ X4)|~((epred5_0 @ X3 @ X4)))), inference(spm,[status(thm)],[c_0_18, c_0_15])).
% 5.97/1.22  thf(c_0_25, 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_8])).
% 5.97/1.22  thf(c_0_26, 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_19, c_0_13])).
% 5.97/1.22  thf(c_0_27, plain, (((epred7_0)=(epred5_0))|((epred3_0)=(epred4_0))), inference(spm,[status(thm)],[c_0_20, c_0_21])).
% 5.97/1.22  thf(c_0_28, 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_9])).
% 5.97/1.22  thf(c_0_29, plain, ![X3:a, X4:a, X5:a]:((((epred3_0)=(epred4_0))|(epred6_0 @ X3 @ X4)|~((epred6_0 @ X5 @ X4))|~((epred6_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_22, c_0_15])).
% 5.97/1.22  thf(c_0_30, plain, ![X4:a, X3:a]:((((epred3_0)=(epred4_0))|(epred6_0 @ X3 @ X4)|~((epred5_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_23, c_0_24])).
% 5.97/1.22  thf(c_0_31, plain, ![X4:a, X3:a]:((((epred3_0)=(epred4_0))|(epred5_0 @ X3 @ X4)|~((epred5_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_25, c_0_15])).
% 5.97/1.22  thf(c_0_32, plain, (((epred3_0)=(epred4_0))|(epred5_0 @ esk9_0 @ esk10_0)|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[c_0_26, c_0_27])).
% 5.97/1.22  thf(c_0_33, plain, (((epred3_0)=(epred4_0))|(epred1_3 @ epred7_0 @ epred7_0 @ epred5_0)), inference(spm,[status(thm)],[c_0_15, c_0_21])).
% 5.97/1.22  thf(c_0_34, 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_28, c_0_13])).
% 5.97/1.22  thf(c_0_35, plain, ![X93:a, X94:a]:((((epred6_0 @ X93 @ X94)<=>(epred7_0 @ X93 @ X94))|((epred3_0)=(epred4_0)))), inference(arg_cong,[status(thm)],[c_0_21])).
% 5.97/1.22  thf(c_0_36, 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_14])).
% 5.97/1.22  thf(c_0_37, plain, ![X3:a, X4:a, X5:a]:((((epred3_0)=(epred4_0))|(epred6_0 @ X3 @ X4)|~((epred6_0 @ X3 @ X5))|~((epred5_0 @ X4 @ X5)))), inference(spm,[status(thm)],[c_0_29, c_0_30])).
% 5.97/1.22  thf(c_0_38, plain, (((epred3_0)=(epred4_0))|(epred5_0 @ esk10_0 @ esk9_0)|~((epred5_0 @ esk7_0 @ esk6_0))), inference(spm,[status(thm)],[c_0_31, c_0_32])).
% 5.97/1.22  thf(c_0_39, plain, ![X3:a, X4:a, X5:a]:((((epred3_0)=(epred4_0))|(epred7_0 @ X3 @ X4)|~((epred7_0 @ X5 @ X4))|~((epred7_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_22, c_0_33])).
% 5.97/1.22  thf(c_0_40, plain, ![X3:a, X4:a]:((((epred3_0)=(epred4_0))|(epred7_0 @ X3 @ X4)|~((epred5_0 @ X3 @ X4)))), inference(spm,[status(thm)],[c_0_18, c_0_33])).
% 5.97/1.22  thf(c_0_41, plain, (((epred3_0)=(epred4_0))|(epred5_0 @ esk8_0 @ esk9_0)|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[c_0_34, c_0_27])).
% 5.97/1.22  thf(c_0_42, 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_9])).
% 5.97/1.22  thf(c_0_43, plain, ![X3:a, X4:a]:((((epred3_0)=(epred4_0))|(epred6_0 @ X3 @ X4)|~((epred7_0 @ X3 @ X4)))), inference(dynamic_cnf,[status(thm)],[c_0_35])).
% 5.97/1.22  thf(c_0_44, plain, ![X3:a, X4:a, X5:a]:((((epred3_0 @ X3)=(epred4_0 @ X3))|(epred6_0 @ X4 @ X5)|~((epred5_0 @ X4 @ X5)))), inference(arg_cong,[status(thm)],[c_0_24])).
% 5.97/1.22  thf(c_0_45, plain, ![X3:a, X4:a]:((((epred3_0)=(epred4_0))|(epred5_0 @ X3 @ X4)|~((epred6_0 @ X3 @ X4)))), inference(spm,[status(thm)],[c_0_36, c_0_15])).
% 5.97/1.22  thf(c_0_46, plain, ![X3:a]:((((epred3_0)=(epred4_0))|(epred6_0 @ X3 @ esk10_0)|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred6_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_37, c_0_38])).
% 5.97/1.22  thf(c_0_47, plain, ![X3:a, X5:a, X4:a]:((((epred3_0)=(epred4_0))|(epred7_0 @ X3 @ X4)|~((epred7_0 @ X3 @ X5))|~((epred5_0 @ X5 @ X4)))), inference(spm,[status(thm)],[c_0_39, c_0_40])).
% 5.97/1.22  thf(c_0_48, plain, (((epred3_0)=(epred4_0))|(epred5_0 @ esk9_0 @ esk8_0)|~((epred5_0 @ esk7_0 @ esk6_0))), inference(spm,[status(thm)],[c_0_31, c_0_41])).
% 5.97/1.22  thf(c_0_49, 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_9])).
% 5.97/1.22  thf(c_0_50, 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_8])).
% 5.97/1.22  thf(c_0_51, 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_42, c_0_13])).
% 5.97/1.22  thf(c_0_52, 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_9])).
% 5.97/1.22  thf(c_0_53, 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_9])).
% 5.97/1.22  thf(c_0_54, plain, ![X3:a]:((((epred3_0)=(epred4_0))|(epred6_0 @ X3 @ esk9_0)|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred6_0 @ X3 @ esk10_0)))), inference(spm,[status(thm)],[c_0_37, c_0_32])).
% 5.97/1.22  thf(c_0_55, plain, ![X4:a, X3:a]:((((epred3_0)=(epred4_0))|(epred6_0 @ X3 @ X4)|~((epred7_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_23, c_0_43])).
% 5.97/1.22  thf(c_0_56, plain, ![X3:a]:((((epred3_0 @ X3)=(epred4_0 @ X3))|((epred3_0)=(epred4_0))|(epred6_0 @ esk10_0 @ esk9_0)|~((epred5_0 @ esk7_0 @ esk6_0)))), inference(spm,[status(thm)],[c_0_44, c_0_38])).
% 5.97/1.22  thf(c_0_57, plain, ![X3:a]:((((epred3_0)=(epred4_0))|(epred5_0 @ X3 @ esk10_0)|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred6_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_45, c_0_46])).
% 5.97/1.22  thf(c_0_58, plain, ![X3:a]:((((epred3_0)=(epred4_0))|(epred7_0 @ X3 @ esk8_0)|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred7_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_47, c_0_48])).
% 5.97/1.22  thf(c_0_59, 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_49, c_0_13])).
% 5.97/1.22  thf(c_0_60, 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_50, c_0_15])).
% 5.97/1.22  thf(c_0_61, plain, (((epred3_0)=(epred4_0))|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk9_0 @ esk10_0)), inference(csr,[status(thm)],[c_0_51, c_0_27])).
% 5.97/1.22  thf(c_0_62, 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_52, c_0_13])).
% 5.97/1.22  thf(c_0_63, 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_53, c_0_13])).
% 5.97/1.22  thf(c_0_64, plain, ![X3:a]:((((epred3_0)=(epred4_0))|(epred6_0 @ X3 @ esk9_0)|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred7_0 @ esk10_0 @ X3)))), inference(spm,[status(thm)],[c_0_54, c_0_55])).
% 5.97/1.22  thf(c_0_65, plain, ![X3:a, X4:a]:((((epred3_0)=(epred4_0))|(epred7_0 @ X3 @ X4)|~((epred6_0 @ X3 @ X4)))), inference(dynamic_cnf,[status(thm)],[c_0_35])).
% 5.97/1.22  thf(c_0_66, plain, (((epred3_0)=(epred4_0))|(epred6_0 @ esk10_0 @ esk9_0)|~((epred5_0 @ esk7_0 @ esk6_0))), inference(cn,[status(thm)],[inference(pos_ext,[status(thm)],[c_0_56])])).
% 5.97/1.22  thf(c_0_67, plain, ![X3:a]:((((epred3_0)=(epred4_0))|(epred5_0 @ X3 @ esk10_0)|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred7_0 @ esk9_0 @ X3)))), inference(spm,[status(thm)],[c_0_57, c_0_55])).
% 5.97/1.22  thf(c_0_68, plain, ![X3:a]:((((epred3_0)=(epred4_0))|(epred7_0 @ X3 @ esk8_0)|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred5_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_58, c_0_40])).
% 5.97/1.22  thf(c_0_69, plain, (((epred3_0)=(epred4_0))|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[c_0_59, c_0_27])).
% 5.97/1.22  thf(c_0_70, 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_9])).
% 5.97/1.22  thf(c_0_71, 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_60, c_0_61])).
% 5.97/1.22  thf(c_0_72, plain, (((epred3_0)=(epred4_0))|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk9_0)), inference(csr,[status(thm)],[c_0_62, c_0_27])).
% 5.97/1.22  thf(c_0_73, plain, (((epred3_0)=(epred4_0))|(epred5_0 @ esk6_0 @ esk7_0)|~((epred5_0 @ esk8_0 @ esk10_0))), inference(csr,[status(thm)],[c_0_63, c_0_27])).
% 5.97/1.22  thf(c_0_74, plain, ![X3:a]:((((epred3_0)=(epred4_0))|(epred5_0 @ X3 @ esk9_0)|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred7_0 @ esk10_0 @ X3)))), inference(spm,[status(thm)],[c_0_45, c_0_64])).
% 5.97/1.22  thf(c_0_75, plain, (((epred3_0)=(epred4_0))|(epred7_0 @ esk10_0 @ esk9_0)|~((epred5_0 @ esk7_0 @ esk6_0))), inference(spm,[status(thm)],[c_0_65, c_0_66])).
% 5.97/1.22  thf(c_0_76, plain, (((epred3_0)=(epred4_0))|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred5_0 @ esk9_0 @ esk9_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_67, c_0_68]), c_0_69])).
% 5.97/1.22  thf(c_0_77, plain, ![X91:a, X92:a]:((((epred3_0 @ X91 @ X92)<=>(epred4_0 @ X91 @ X92))|((epred6_0)=(epred7_0)))), inference(arg_cong,[status(thm)],[c_0_21])).
% 5.97/1.22  thf(c_0_78, 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_70, c_0_13]), c_0_15])).
% 5.97/1.22  thf(c_0_79, 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_9])).
% 5.97/1.22  thf(c_0_80, plain, (((epred3_0)=(epred4_0))|(epred5_0 @ esk6_0 @ esk7_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_71, c_0_72]), c_0_73])).
% 5.97/1.22  thf(c_0_81, plain, (((epred3_0)=(epred4_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_74, c_0_75]), c_0_76])).
% 5.97/1.22  thf(c_0_82, 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_9])).
% 5.97/1.22  thf(c_0_83, plain, ![X3:a, X4:a]:((((epred6_0)=(epred7_0))|(epred3_0 @ X3 @ X4)|~((epred4_0 @ X3 @ X4)))), inference(dynamic_cnf,[status(thm)],[c_0_77])).
% 5.97/1.22  thf(c_0_84, plain, (((epred6_0)=(epred7_0))|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_16, c_0_78])).
% 5.97/1.22  thf(c_0_85, 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_79, c_0_13]), c_0_15])).
% 5.97/1.22  thf(c_0_86, plain, ((epred3_0)=(epred4_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_31, c_0_80]), c_0_81])).
% 5.97/1.22  thf(c_0_87, 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_82, c_0_13])).
% 5.97/1.22  thf(c_0_88, plain, (((epred6_0)=(epred7_0))|(epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk4_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_83, c_0_84])).
% 5.97/1.22  thf(c_0_89, plain, (((epred6_0)=(epred7_0))|(epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_16, c_0_85])).
% 5.97/1.22  thf(c_0_90, 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_9])).
% 5.97/1.22  thf(c_0_91, 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_9])).
% 5.97/1.22  thf(c_0_92, 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_9])).
% 5.97/1.22  thf(c_0_93, plain, ![X802:a, X803:a]:(((epred3_0 @ X802 @ X803)<=>(epred4_0 @ X802 @ X803))), inference(arg_cong,[status(thm)],[c_0_86])).
% 5.97/1.22  thf(c_0_94, 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_87, c_0_88]), c_0_16])).
% 5.97/1.22  thf(c_0_95, plain, (((epred6_0)=(epred7_0))|(epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk3_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_83, c_0_89])).
% 5.97/1.22  thf(c_0_96, 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_90, c_0_13]), c_0_15])).
% 5.97/1.22  thf(c_0_97, 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_9])).
% 5.97/1.22  thf(c_0_98, 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_91, c_0_13]), c_0_15])).
% 5.97/1.22  thf(c_0_99, 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_92, c_0_13])).
% 5.97/1.22  thf(c_0_100, plain, ![X3:a, X4:a]:(((epred3_0 @ X3 @ X4)|~((epred4_0 @ X3 @ X4)))), inference(dynamic_cnf,[status(thm)],[c_0_93])).
% 5.97/1.22  thf(c_0_101, plain, ![X3:a, X4:a]:(((epred4_0 @ X3 @ X4)|~((epred3_0 @ X3 @ X4)))), inference(dynamic_cnf,[status(thm)],[c_0_93])).
% 5.97/1.22  thf(c_0_102, plain, (((epred6_0)=(epred7_0))|(epred3_0 @ esk3_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_94, c_0_95])).
% 5.97/1.22  thf(c_0_103, plain, (((epred6_0)=(epred7_0))|(epred4_0 @ esk1_0 @ esk2_0)|~((epred4_0 @ esk3_0 @ esk5_0))), inference(spm,[status(thm)],[c_0_16, c_0_96])).
% 5.97/1.22  thf(c_0_104, 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_97, c_0_13]), c_0_15])).
% 5.97/1.22  thf(c_0_105, plain, (((epred6_0)=(epred7_0))|(epred4_0 @ esk4_0 @ esk5_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(spm,[status(thm)],[c_0_16, c_0_98])).
% 5.97/1.22  thf(c_0_106, 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_99, c_0_100])).
% 5.97/1.22  thf(c_0_107, plain, (((epred6_0)=(epred7_0))|(epred4_0 @ esk1_0 @ esk2_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_101, c_0_102]), c_0_103])).
% 5.97/1.22  thf(c_0_108, plain, (((epred6_0)=(epred7_0))|(epred4_0 @ esk3_0 @ esk4_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(spm,[status(thm)],[c_0_16, c_0_104])).
% 5.97/1.22  thf(c_0_109, plain, (((epred6_0)=(epred7_0))|(epred3_0 @ esk4_0 @ esk5_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(spm,[status(thm)],[c_0_83, c_0_105])).
% 5.97/1.22  thf(c_0_110, plain, (((epred6_0)=(epred7_0))|(epred3_0 @ esk2_0 @ esk1_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_106, c_0_107]), c_0_16])).
% 5.97/1.22  thf(c_0_111, plain, (((epred6_0)=(epred7_0))|(epred3_0 @ esk3_0 @ esk4_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(spm,[status(thm)],[c_0_83, c_0_108])).
% 5.97/1.22  thf(c_0_112, plain, ![X3:a]:((((epred6_0)=(epred7_0))|(epred3_0 @ X3 @ esk5_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred3_0 @ X3 @ esk4_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_87, c_0_109]), c_0_16])).
% 5.97/1.22  thf(c_0_113, plain, (((epred6_0)=(epred7_0))|(epred4_0 @ esk2_0 @ esk1_0)), inference(spm,[status(thm)],[c_0_101, c_0_110])).
% 5.97/1.22  thf(c_0_114, plain, (((epred6_0)=(epred7_0))|(epred3_0 @ esk4_0 @ esk3_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_99, c_0_111]), c_0_16])).
% 5.97/1.22  thf(c_0_115, plain, ![X3:a]:((((epred6_0)=(epred7_0))|(epred3_0 @ X3 @ esk5_0)|~((epred3_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_112, c_0_113])).
% 5.97/1.22  thf(c_0_116, plain, ![X3:a]:((((epred6_0)=(epred7_0))|(epred3_0 @ X3 @ esk4_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred3_0 @ X3 @ esk3_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_87, c_0_111]), c_0_16])).
% 5.97/1.22  thf(c_0_117, plain, ![X3:a]:((((epred6_0)=(epred7_0))|(epred3_0 @ X3 @ esk3_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred3_0 @ X3 @ esk4_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_87, c_0_114]), c_0_16])).
% 5.97/1.22  thf(c_0_118, plain, ![X87:a, X88:a]:((((epred3_0 @ X87 @ X88)<=>(epred4_0 @ X87 @ X88))|((epred6_0)=(epred5_0)))), inference(arg_cong,[status(thm)],[c_0_20])).
% 5.97/1.22  thf(c_0_119, 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_9])).
% 5.97/1.22  thf(c_0_120, plain, ![X3:a]:((((epred6_0)=(epred7_0))|(epred4_0 @ X3 @ esk5_0)|~((epred3_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_101, c_0_115])).
% 5.97/1.22  thf(c_0_121, plain, ![X3:a]:((((epred6_0)=(epred7_0))|(epred3_0 @ X3 @ esk4_0)|~((epred3_0 @ X3 @ esk3_0)))), inference(spm,[status(thm)],[c_0_116, c_0_113])).
% 5.97/1.22  thf(c_0_122, plain, ![X3:a]:((((epred6_0)=(epred7_0))|(epred3_0 @ X3 @ esk3_0)|~((epred3_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_117, c_0_113])).
% 5.97/1.22  thf(c_0_123, plain, ![X3:a, X4:a]:((((epred6_0)=(epred5_0))|(epred3_0 @ X3 @ X4)|~((epred4_0 @ X3 @ X4)))), inference(dynamic_cnf,[status(thm)],[c_0_118])).
% 5.97/1.22  thf(c_0_124, plain, (((epred6_0)=(epred5_0))|(epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_11, c_0_85])).
% 5.97/1.22  thf(c_0_125, plain, (((epred6_0)=(epred5_0))|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_11, c_0_78])).
% 5.97/1.22  thf(c_0_126, 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_119, c_0_13]), c_0_15])).
% 5.97/1.22  thf(c_0_127, plain, ![X3:a]:((((epred6_0)=(epred7_0))|(epred4_0 @ X3 @ esk5_0)|~((epred3_0 @ X3 @ esk3_0)))), inference(spm,[status(thm)],[c_0_120, c_0_121])).
% 5.97/1.22  thf(c_0_128, plain, (((epred6_0)=(epred7_0))|(epred3_0 @ esk3_0 @ esk3_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_122, c_0_111]), c_0_113])).
% 5.97/1.22  thf(c_0_129, plain, (((epred6_0)=(epred5_0))|(epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk3_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_123, c_0_124])).
% 5.97/1.22  thf(c_0_130, plain, (((epred6_0)=(epred5_0))|(epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk4_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_123, c_0_125])).
% 5.97/1.22  thf(c_0_131, plain, (((epred6_0)=(epred7_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))), inference(spm,[status(thm)],[c_0_16, c_0_126])).
% 5.97/1.22  thf(c_0_132, plain, (((epred6_0)=(epred7_0))|(epred4_0 @ esk3_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_127, c_0_128])).
% 5.97/1.22  thf(c_0_133, plain, ![X3:a]:((((epred6_0 @ X3)=(epred7_0 @ X3))|(epred3_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0))), inference(arg_cong,[status(thm)],[c_0_95])).
% 5.97/1.22  thf(c_0_134, plain, ![X3:a]:((((epred6_0 @ X3)=(epred5_0 @ X3))|(epred3_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0))), inference(arg_cong,[status(thm)],[c_0_129])).
% 5.97/1.22  thf(c_0_135, 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_87, c_0_130]), c_0_11])).
% 5.97/1.22  thf(c_0_136, plain, ((epred6_0)=(epred7_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_131, c_0_132]), c_0_113])).
% 5.97/1.22  thf(c_0_137, plain, ![X3:a]:((((epred7_0 @ X3)=(epred5_0 @ X3))|(epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk3_0 @ esk4_0))), inference(spm,[status(thm)],[c_0_133, c_0_134])).
% 5.97/1.22  thf(c_0_138, plain, ![X3:a]:((((epred7_0)=(epred5_0))|(epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ X3 @ esk5_0)|~((epred3_0 @ X3 @ esk4_0)))), inference(rw,[status(thm)],[c_0_135, c_0_136])).
% 5.97/1.22  thf(c_0_139, plain, (((epred7_0)=(epred5_0))|(epred3_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(pos_ext,[status(thm)],[c_0_137])).
% 5.97/1.22  thf(c_0_140, plain, (((epred6_0)=(epred5_0))|(epred4_0 @ esk1_0 @ esk2_0)|~((epred4_0 @ esk3_0 @ esk5_0))), inference(spm,[status(thm)],[c_0_11, c_0_96])).
% 5.97/1.22  thf(c_0_141, plain, (((epred6_0)=(epred5_0))|(epred4_0 @ esk4_0 @ esk5_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(spm,[status(thm)],[c_0_11, c_0_98])).
% 5.97/1.22  thf(c_0_142, plain, (((epred7_0)=(epred5_0))|(epred3_0 @ esk3_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_138, c_0_139])).
% 5.97/1.22  thf(c_0_143, plain, (((epred7_0)=(epred5_0))|(epred4_0 @ esk1_0 @ esk2_0)|~((epred4_0 @ esk3_0 @ esk5_0))), inference(rw,[status(thm)],[c_0_140, c_0_136])).
% 5.97/1.22  thf(c_0_144, plain, (((epred6_0)=(epred5_0))|(epred4_0 @ esk3_0 @ esk4_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(spm,[status(thm)],[c_0_11, c_0_104])).
% 5.97/1.22  thf(c_0_145, plain, (((epred6_0)=(epred5_0))|(epred3_0 @ esk4_0 @ esk5_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(spm,[status(thm)],[c_0_123, c_0_141])).
% 5.97/1.22  thf(c_0_146, 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_106, c_0_136])).
% 5.97/1.22  thf(c_0_147, plain, (((epred7_0)=(epred5_0))|(epred4_0 @ esk1_0 @ esk2_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_101, c_0_142]), c_0_143])).
% 5.97/1.22  thf(c_0_148, plain, (((epred6_0)=(epred5_0))|(epred3_0 @ esk3_0 @ esk4_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(spm,[status(thm)],[c_0_123, c_0_144])).
% 5.97/1.22  thf(c_0_149, plain, ![X3:a]:((((epred6_0)=(epred5_0))|(epred3_0 @ X3 @ esk5_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred3_0 @ X3 @ esk4_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_87, c_0_145]), c_0_11])).
% 5.97/1.22  thf(c_0_150, plain, (((epred7_0)=(epred5_0))|(epred3_0 @ esk2_0 @ esk1_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_146, c_0_147]), c_0_11])).
% 5.97/1.22  thf(c_0_151, plain, (((epred6_0)=(epred5_0))|(epred3_0 @ esk4_0 @ esk3_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_99, c_0_148]), c_0_11])).
% 5.97/1.22  thf(c_0_152, plain, ![X3:a]:((((epred7_0)=(epred5_0))|(epred3_0 @ X3 @ esk5_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred3_0 @ X3 @ esk4_0)))), inference(rw,[status(thm)],[c_0_149, c_0_136])).
% 5.97/1.22  thf(c_0_153, plain, (((epred7_0)=(epred5_0))|(epred4_0 @ esk2_0 @ esk1_0)), inference(spm,[status(thm)],[c_0_101, c_0_150])).
% 5.97/1.22  thf(c_0_154, plain, ![X3:a]:((((epred6_0)=(epred5_0))|(epred3_0 @ X3 @ esk4_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred3_0 @ X3 @ esk3_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_87, c_0_148]), c_0_11])).
% 5.97/1.22  thf(c_0_155, plain, ![X3:a]:((((epred6_0)=(epred5_0))|(epred3_0 @ X3 @ esk3_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred3_0 @ X3 @ esk4_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_87, c_0_151]), c_0_11])).
% 5.97/1.22  thf(c_0_156, plain, ![X3:a]:((((epred7_0)=(epred5_0))|(epred3_0 @ X3 @ esk5_0)|~((epred3_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_152, c_0_153])).
% 5.97/1.22  thf(c_0_157, plain, ![X3:a]:((((epred7_0)=(epred5_0))|(epred3_0 @ X3 @ esk4_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred3_0 @ X3 @ esk3_0)))), inference(rw,[status(thm)],[c_0_154, c_0_136])).
% 5.97/1.22  thf(c_0_158, plain, ![X3:a]:((((epred7_0)=(epred5_0))|(epred3_0 @ X3 @ esk3_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred3_0 @ X3 @ esk4_0)))), inference(rw,[status(thm)],[c_0_155, c_0_136])).
% 5.97/1.22  thf(c_0_159, plain, ![X3:a]:((((epred7_0)=(epred5_0))|(epred4_0 @ X3 @ esk5_0)|~((epred3_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_101, c_0_156])).
% 5.97/1.22  thf(c_0_160, plain, ![X3:a]:((((epred7_0)=(epred5_0))|(epred3_0 @ X3 @ esk4_0)|~((epred3_0 @ X3 @ esk3_0)))), inference(spm,[status(thm)],[c_0_157, c_0_153])).
% 5.97/1.22  thf(c_0_161, plain, ![X3:a]:((((epred7_0)=(epred5_0))|(epred3_0 @ X3 @ esk3_0)|~((epred3_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_158, c_0_153])).
% 5.97/1.22  thf(c_0_162, plain, (((epred7_0)=(epred5_0))|(epred3_0 @ esk3_0 @ esk4_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(rw,[status(thm)],[c_0_148, c_0_136])).
% 5.97/1.22  thf(c_0_163, plain, (((epred6_0)=(epred5_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))), inference(spm,[status(thm)],[c_0_11, c_0_126])).
% 5.97/1.22  thf(c_0_164, plain, ![X3:a]:((((epred7_0)=(epred5_0))|(epred4_0 @ X3 @ esk5_0)|~((epred3_0 @ X3 @ esk3_0)))), inference(spm,[status(thm)],[c_0_159, c_0_160])).
% 5.97/1.22  thf(c_0_165, plain, (((epred7_0)=(epred5_0))|(epred3_0 @ esk3_0 @ esk3_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_161, c_0_162]), c_0_153])).
% 5.97/1.22  thf(c_0_166, plain, (((epred7_0)=(epred5_0))|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))), inference(rw,[status(thm)],[c_0_163, c_0_136])).
% 5.97/1.22  thf(c_0_167, plain, (((epred7_0)=(epred5_0))|(epred4_0 @ esk3_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_164, c_0_165])).
% 5.97/1.22  thf(c_0_168, 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_87, c_0_100])).
% 5.97/1.22  thf(c_0_169, plain, ((epred7_0)=(epred5_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_166, c_0_167]), c_0_153])).
% 5.97/1.22  thf(c_0_170, plain, ((epred1_3 @ epred7_0 @ epred7_0 @ epred5_0)|(epred4_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(rw,[status(thm)],[c_0_85, c_0_136])).
% 5.97/1.22  thf(c_0_171, plain, ![X3:a, X5:a, X4:a]:(((epred1_3 @ epred7_0 @ epred7_0 @ epred5_0)|(epred3_0 @ X3 @ X4)|~((epred3_0 @ X3 @ X5))|~((epred4_0 @ X5 @ X4)))), inference(rw,[status(thm)],[c_0_168, c_0_136])).
% 5.97/1.22  thf(c_0_172, plain, ![X4:a, X3:a]:(((epred1_3 @ epred7_0 @ epred7_0 @ epred5_0)|(epred3_0 @ X3 @ X4)|~((epred3_0 @ X4 @ X3)))), inference(rw,[status(thm)],[c_0_99, c_0_136])).
% 5.97/1.22  thf(c_0_173, 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_146, c_0_169]), c_0_169])).
% 5.97/1.22  thf(c_0_174, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk3_0 @ esk4_0)), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_170, c_0_169]), c_0_169])).
% 5.97/1.22  thf(c_0_175, plain, ![X3:a, X5:a, X4:a]:(((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred3_0 @ X3 @ X4)|~((epred3_0 @ X3 @ X5))|~((epred4_0 @ X5 @ X4)))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_171, c_0_169]), c_0_169])).
% 5.97/1.22  thf(c_0_176, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred4_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_78, c_0_136]), c_0_169]), c_0_169])).
% 5.97/1.22  thf(c_0_177, plain, ![X4:a, X3:a]:(((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred3_0 @ X3 @ X4)|~((epred3_0 @ X4 @ X3)))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_172, c_0_169]), c_0_169])).
% 5.97/1.22  thf(c_0_178, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk4_0 @ esk3_0)), inference(spm,[status(thm)],[c_0_173, c_0_174])).
% 5.97/1.22  thf(c_0_179, plain, ![X3:a]:(((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ X3 @ esk5_0)|~((epred3_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_175, c_0_176])).
% 5.97/1.22  thf(c_0_180, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk3_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_177, c_0_178])).
% 5.97/1.22  thf(c_0_181, 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_179, c_0_180])).
% 5.97/1.22  thf(c_0_182, 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)],[inference(rw,[status(thm)],[c_0_96, c_0_136]), c_0_169]), c_0_169])).
% 5.97/1.22  thf(c_0_183, 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_104, c_0_136])).
% 5.97/1.22  thf(c_0_184, plain, ![X3:a, X4:a, X5:a]:(((epred1_3 @ epred7_0 @ epred7_0 @ epred5_0)|(epred3_0 @ X3 @ X4)|~((epred3_0 @ X5 @ X4))|~((epred3_0 @ X3 @ X5)))), inference(rw,[status(thm)],[c_0_87, c_0_136])).
% 5.97/1.22  thf(c_0_185, 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)],[inference(rw,[status(thm)],[c_0_98, c_0_136]), c_0_169]), c_0_169])).
% 5.97/1.22  thf(c_0_186, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_101, c_0_181]), c_0_182])).
% 5.97/1.22  thf(c_0_187, 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_183, c_0_169]), c_0_169])).
% 5.97/1.22  thf(c_0_188, plain, ![X3:a, X4:a, X5:a]:(((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred3_0 @ X3 @ X4)|~((epred3_0 @ X5 @ X4))|~((epred3_0 @ X3 @ X5)))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_184, c_0_169]), c_0_169])).
% 5.97/1.22  thf(c_0_189, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred3_0 @ esk5_0 @ esk4_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(spm,[status(thm)],[c_0_173, c_0_185])).
% 5.97/1.22  thf(c_0_190, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred3_0 @ esk2_0 @ esk1_0)), inference(spm,[status(thm)],[c_0_173, c_0_186])).
% 5.97/1.22  thf(c_0_191, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred3_0 @ esk4_0 @ esk3_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(spm,[status(thm)],[c_0_173, c_0_187])).
% 5.97/1.22  thf(c_0_192, plain, ![X3:a]:(((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred3_0 @ X3 @ esk4_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred3_0 @ X3 @ esk5_0)))), inference(spm,[status(thm)],[c_0_188, c_0_189])).
% 5.97/1.22  thf(c_0_193, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred4_0 @ esk2_0 @ esk1_0)), inference(spm,[status(thm)],[c_0_101, c_0_190])).
% 5.97/1.22  thf(c_0_194, 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_9])).
% 5.97/1.22  thf(c_0_195, 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_16])).
% 5.97/1.22  thf(c_0_196, 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_11])).
% 5.97/1.22  thf(c_0_197, plain, ![X3:a]:(((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred3_0 @ X3 @ esk3_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred3_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_188, c_0_191])).
% 5.97/1.22  thf(c_0_198, plain, ![X3:a]:(((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred3_0 @ X3 @ esk4_0)|~((epred3_0 @ X3 @ esk5_0)))), inference(spm,[status(thm)],[c_0_192, c_0_193])).
% 5.97/1.22  thf(c_0_199, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred3_0 @ esk4_0 @ esk5_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(spm,[status(thm)],[c_0_177, c_0_189])).
% 5.97/1.22  thf(c_0_200, 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_194, c_0_13])).
% 5.97/1.22  thf(c_0_201, 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_9])).
% 5.97/1.22  thf(c_0_202, 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_195, c_0_85])).
% 5.97/1.22  thf(c_0_203, 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_196, c_0_85])).
% 5.97/1.22  thf(c_0_204, 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_9])).
% 5.97/1.22  thf(c_0_205, plain, ![X3:a]:(((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred3_0 @ X3 @ esk3_0)|~((epred3_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_197, c_0_193])).
% 5.97/1.22  thf(c_0_206, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred3_0 @ esk4_0 @ esk4_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_198, c_0_199]), c_0_193])).
% 5.97/1.22  thf(c_0_207, 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_9])).
% 5.97/1.22  thf(c_0_208, 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))|~((epred4_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_200, c_0_100])).
% 5.97/1.22  thf(c_0_209, 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_201, c_0_13]), c_0_51])).
% 5.97/1.22  thf(c_0_210, 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_202, c_0_203])).
% 5.97/1.22  thf(c_0_211, 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_9])).
% 5.97/1.22  thf(c_0_212, 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_195, c_0_78])).
% 5.97/1.22  thf(c_0_213, 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_196, c_0_78])).
% 5.97/1.22  thf(c_0_214, 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_204, c_0_13])).
% 5.97/1.22  thf(c_0_215, 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_9])).
% 5.97/1.22  thf(c_0_216, plain, ![X3:a]:(((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred3_0 @ X3 @ esk5_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred3_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_188, c_0_199])).
% 5.97/1.22  thf(c_0_217, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred3_0 @ esk4_0 @ esk3_0)), inference(spm,[status(thm)],[c_0_205, c_0_206])).
% 5.97/1.22  thf(c_0_218, 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_207, c_0_13])).
% 5.97/1.22  thf(c_0_219, 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(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_208, c_0_169])])).
% 5.97/1.22  thf(c_0_220, 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_209]), c_0_210])).
% 5.97/1.22  thf(c_0_221, 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_211, c_0_13]), c_0_51])).
% 5.97/1.22  thf(c_0_222, 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_212, c_0_213])).
% 5.97/1.22  thf(c_0_223, 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_9])).
% 5.97/1.22  thf(c_0_224, 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))|~((epred4_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_214, c_0_100])).
% 5.97/1.22  thf(c_0_225, 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_215, c_0_13]), c_0_62])).
% 5.97/1.22  thf(c_0_226, 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_9])).
% 5.97/1.22  thf(c_0_227, plain, ![X3:a]:(((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred3_0 @ X3 @ esk5_0)|~((epred3_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_216, c_0_193])).
% 5.97/1.22  thf(c_0_228, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred3_0 @ esk3_0 @ esk4_0)), inference(spm,[status(thm)],[c_0_177, c_0_217])).
% 5.97/1.22  thf(c_0_229, 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_218, c_0_169])])).
% 5.97/1.22  thf(c_0_230, 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_219, c_0_220])).
% 5.97/1.22  thf(c_0_231, 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_221]), c_0_222])).
% 5.97/1.22  thf(c_0_232, 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_223, c_0_13])).
% 5.97/1.22  thf(c_0_233, 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(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_224, c_0_169])])).
% 5.97/1.22  thf(c_0_234, 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)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_225, c_0_169])])).
% 5.97/1.22  thf(c_0_235, 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_226, c_0_13]), c_0_62])).
% 5.97/1.22  thf(c_0_236, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred3_0 @ esk3_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_227, c_0_228])).
% 5.97/1.22  thf(c_0_237, plain, ![X3:a]:(((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk9_0 @ esk10_0)|(epred3_0 @ X3 @ esk3_0)|~((epred3_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_229, c_0_230])).
% 5.97/1.22  thf(c_0_238, 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_219, c_0_231])).
% 5.97/1.22  thf(c_0_239, 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_9])).
% 5.97/1.22  thf(c_0_240, 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_232, c_0_169])])).
% 5.97/1.22  thf(c_0_241, 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_233, c_0_234])).
% 5.97/1.22  thf(c_0_242, 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_235]), c_0_222])).
% 5.97/1.22  thf(c_0_243, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_126, c_0_136]), c_0_169]), c_0_169])).
% 5.97/1.22  thf(c_0_244, plain, ((epred1_3 @ epred5_0 @ epred5_0 @ epred5_0)|(epred4_0 @ esk3_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_101, c_0_236])).
% 5.97/1.22  thf(c_0_245, 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_200, c_0_169])])).
% 5.97/1.22  thf(c_0_246, plain, ((epred3_0 @ esk5_0 @ esk3_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_237, c_0_238])).
% 5.97/1.22  thf(c_0_247, 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_239, c_0_13]), c_0_51])).
% 5.97/1.22  thf(c_0_248, plain, ![X3:a]:(((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk9_0)|(epred3_0 @ X3 @ esk3_0)|~((epred3_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_240, c_0_241])).
% 5.97/1.22  thf(c_0_249, 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_233, c_0_242])).
% 5.97/1.22  thf(c_0_250, 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_9])).
% 5.97/1.22  thf(c_0_251, plain, (epred1_3 @ epred5_0 @ epred5_0 @ epred5_0), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_243, c_0_244]), c_0_193])).
% 5.97/1.22  thf(c_0_252, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk9_0 @ esk10_0)), inference(spm,[status(thm)],[c_0_245, c_0_246])).
% 5.97/1.22  thf(c_0_253, 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_247, c_0_169])])).
% 5.97/1.22  thf(c_0_254, 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_214, c_0_169])])).
% 5.97/1.22  thf(c_0_255, plain, ((epred3_0 @ esk5_0 @ esk3_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_248, c_0_249])).
% 5.97/1.22  thf(c_0_256, 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_250, c_0_13]), c_0_62])).
% 5.97/1.22  thf(c_0_257, 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_9])).
% 5.97/1.22  thf(c_0_258, plain, ![X3:a, X4:a, X5:a]:(((epred5_0 @ X3 @ X4)|~((epred5_0 @ X5 @ X4))|~((epred5_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_22, c_0_251])).
% 5.97/1.22  thf(c_0_259, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_101, c_0_252]), c_0_253])).
% 5.97/1.22  thf(c_0_260, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk9_0)), inference(spm,[status(thm)],[c_0_254, c_0_255])).
% 5.97/1.22  thf(c_0_261, 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_256, c_0_169])])).
% 5.97/1.22  thf(c_0_262, 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_257, c_0_13])).
% 5.97/1.22  thf(c_0_263, plain, ![X3:a]:(((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_258, c_0_259])).
% 5.97/1.22  thf(c_0_264, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_101, c_0_260]), c_0_261])).
% 5.97/1.22  thf(c_0_265, 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_262, c_0_169])])).
% 5.97/1.22  thf(c_0_266, plain, ((epred5_0 @ esk8_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_263, c_0_264])).
% 5.97/1.22  thf(c_0_267, 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_9])).
% 5.97/1.22  thf(c_0_268, 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_9])).
% 5.97/1.22  thf(c_0_269, plain, ![X4:a, X3:a]:(((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ X3 @ X4)|~((epred3_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_265, c_0_266])).
% 5.97/1.22  thf(c_0_270, 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_267, c_0_13]), c_0_63])).
% 5.97/1.22  thf(c_0_271, 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_9])).
% 5.97/1.22  thf(c_0_272, 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_268, c_0_13])).
% 5.97/1.22  thf(c_0_273, plain, ![X4:a, X3:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ X3 @ X4)|~((epred4_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_269, c_0_100])).
% 5.97/1.22  thf(c_0_274, 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_270]), c_0_222])).
% 5.97/1.22  thf(c_0_275, 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_271, c_0_13]), c_0_63])).
% 5.97/1.22  thf(c_0_276, 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_9])).
% 5.97/1.22  thf(c_0_277, 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_272, c_0_169])])).
% 5.97/1.22  thf(c_0_278, plain, ((epred3_0 @ esk5_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_273, c_0_274]), c_0_266])).
% 5.97/1.22  thf(c_0_279, 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_275]), c_0_210])).
% 5.97/1.22  thf(c_0_280, 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_276, c_0_13]), c_0_62])).
% 5.97/1.22  thf(c_0_281, 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_9])).
% 5.97/1.22  thf(c_0_282, 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_9])).
% 5.97/1.22  thf(c_0_283, plain, ![X3:a, X4:a, X5:a]:(((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ X3 @ X4)|~((epred3_0 @ X5 @ X4))|~((epred3_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_277, c_0_266])).
% 5.97/1.22  thf(c_0_284, plain, ((epred3_0 @ esk4_0 @ esk5_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_269, c_0_278])).
% 5.97/1.22  thf(c_0_285, plain, ((epred3_0 @ esk4_0 @ esk3_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_273, c_0_279]), c_0_266])).
% 5.97/1.22  thf(c_0_286, 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_280, c_0_169])])).
% 5.97/1.22  thf(c_0_287, 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_281, c_0_13]), c_0_62])).
% 5.97/1.22  thf(c_0_288, 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_282, c_0_13]), c_0_51])).
% 5.97/1.22  thf(c_0_289, 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_9])).
% 5.97/1.22  thf(c_0_290, 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_9])).
% 5.97/1.22  thf(c_0_291, plain, ![X3:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ X3 @ esk5_0)|~((epred3_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_283, c_0_284])).
% 5.97/1.22  thf(c_0_292, plain, ((epred3_0 @ esk3_0 @ esk4_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_269, c_0_285])).
% 5.97/1.22  thf(c_0_293, plain, ((epred3_0 @ esk4_0 @ esk3_0)|(epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(spm,[status(thm)],[c_0_233, c_0_286])).
% 5.97/1.22  thf(c_0_294, 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_287, c_0_169])])).
% 5.97/1.22  thf(c_0_295, 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_288, c_0_169])])).
% 5.97/1.22  thf(c_0_296, 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_289, c_0_13]), c_0_51])).
% 5.97/1.22  thf(c_0_297, 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_290, c_0_13]), c_0_63])).
% 5.97/1.22  thf(c_0_298, plain, ((epred3_0 @ esk3_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_291, c_0_292])).
% 5.97/1.22  thf(c_0_299, plain, ![X3:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk9_0)|(epred3_0 @ X3 @ esk3_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred3_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_240, c_0_293])).
% 5.97/1.22  thf(c_0_300, plain, ((epred3_0 @ esk5_0 @ esk4_0)|(epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(spm,[status(thm)],[c_0_233, c_0_294])).
% 5.97/1.22  thf(c_0_301, 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_9])).
% 5.97/1.22  thf(c_0_302, plain, ((epred3_0 @ esk4_0 @ esk3_0)|(epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(spm,[status(thm)],[c_0_219, c_0_295])).
% 5.97/1.22  thf(c_0_303, 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_296, c_0_169])])).
% 5.97/1.22  thf(c_0_304, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(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_297, c_0_169])])).
% 5.97/1.22  thf(c_0_305, 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_101, c_0_298])).
% 5.97/1.22  thf(c_0_306, plain, ((epred3_0 @ esk5_0 @ esk3_0)|(epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(spm,[status(thm)],[c_0_299, c_0_300])).
% 5.97/1.22  thf(c_0_307, 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_301, c_0_13]), c_0_62])).
% 5.97/1.22  thf(c_0_308, plain, ![X3:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk9_0 @ esk10_0)|(epred3_0 @ X3 @ esk3_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred3_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_229, c_0_302])).
% 5.97/1.22  thf(c_0_309, plain, ((epred3_0 @ esk5_0 @ esk4_0)|(epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(spm,[status(thm)],[c_0_219, c_0_303])).
% 5.97/1.22  thf(c_0_310, 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_9])).
% 5.97/1.22  thf(c_0_311, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_304, c_0_305]), c_0_266])).
% 5.97/1.22  thf(c_0_312, plain, ((epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk9_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(spm,[status(thm)],[c_0_254, c_0_306])).
% 5.97/1.22  thf(c_0_313, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_307, c_0_169])])).
% 5.97/1.22  thf(c_0_314, plain, ((epred3_0 @ esk5_0 @ esk3_0)|(epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(spm,[status(thm)],[c_0_308, c_0_309])).
% 5.97/1.22  thf(c_0_315, 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_310, c_0_13]), c_0_51])).
% 5.97/1.22  thf(c_0_316, 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_233, c_0_311])).
% 5.97/1.22  thf(c_0_317, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred5_0 @ esk6_0 @ esk7_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_101, c_0_312]), c_0_313])).
% 5.97/1.22  thf(c_0_318, plain, ((epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk9_0 @ esk10_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(spm,[status(thm)],[c_0_245, c_0_314])).
% 5.97/1.22  thf(c_0_319, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_315, c_0_169])])).
% 5.97/1.22  thf(c_0_320, plain, ![X4:a, X3:a]:(((epred5_0 @ X3 @ X4)|~((epred5_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_17, c_0_251])).
% 5.97/1.22  thf(c_0_321, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk9_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_101, c_0_316]), c_0_317])).
% 5.97/1.22  thf(c_0_322, 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_219, c_0_311])).
% 5.97/1.22  thf(c_0_323, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred5_0 @ esk6_0 @ esk7_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_101, c_0_318]), c_0_319])).
% 5.97/1.22  thf(c_0_324, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk9_0 @ esk8_0)), inference(spm,[status(thm)],[c_0_320, c_0_321])).
% 5.97/1.22  thf(c_0_325, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk9_0 @ esk10_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_101, c_0_322]), c_0_323])).
% 5.97/1.22  thf(c_0_326, plain, ![X3:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ X3 @ esk8_0)|~((epred5_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_258, c_0_324])).
% 5.97/1.22  thf(c_0_327, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk10_0 @ esk9_0)), inference(spm,[status(thm)],[c_0_320, c_0_325])).
% 5.97/1.22  thf(c_0_328, plain, ((epred5_0 @ esk10_0 @ esk8_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_326, c_0_327])).
% 5.97/1.22  thf(c_0_329, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred5_0 @ esk8_0 @ esk10_0)), inference(spm,[status(thm)],[c_0_320, c_0_328])).
% 5.97/1.22  thf(c_0_330, 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_265, c_0_329])).
% 5.97/1.22  thf(c_0_331, 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_9])).
% 5.97/1.22  thf(c_0_332, 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_330, c_0_100])).
% 5.97/1.22  thf(c_0_333, 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_331, c_0_13]), c_0_63])).
% 5.97/1.22  thf(c_0_334, plain, ((epred3_0 @ esk2_0 @ esk1_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_332, c_0_311])).
% 5.97/1.22  thf(c_0_335, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(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_333, c_0_169])])).
% 5.97/1.22  thf(c_0_336, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ esk2_0 @ esk1_0)), inference(spm,[status(thm)],[c_0_101, c_0_334])).
% 5.97/1.22  thf(c_0_337, 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_9])).
% 5.97/1.22  thf(c_0_338, plain, ((epred3_0 @ esk5_0 @ esk4_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_332, c_0_335]), c_0_329]), c_0_336])).
% 5.97/1.22  thf(c_0_339, 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_337, c_0_13]), c_0_63])).
% 5.97/1.22  thf(c_0_340, 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_277, c_0_329])).
% 5.97/1.22  thf(c_0_341, plain, ((epred3_0 @ esk4_0 @ esk5_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_330, c_0_338])).
% 5.97/1.22  thf(c_0_342, plain, ((epred5_0 @ esk6_0 @ esk7_0)|(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_339, c_0_169])])).
% 5.97/1.22  thf(c_0_343, 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_9])).
% 5.97/1.22  thf(c_0_344, plain, ![X3:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred3_0 @ X3 @ esk5_0)|~((epred3_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_340, c_0_341])).
% 5.97/1.22  thf(c_0_345, plain, ((epred3_0 @ esk4_0 @ esk3_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_332, c_0_342]), c_0_329]), c_0_336])).
% 5.97/1.22  thf(c_0_346, 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_9])).
% 5.97/1.22  thf(c_0_347, 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_343, c_0_13]), c_0_63])).
% 5.97/1.22  thf(c_0_348, plain, ![X3:a]:(((epred5_0 @ esk6_0 @ esk7_0)|(epred4_0 @ X3 @ esk5_0)|~((epred3_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_101, c_0_344])).
% 5.97/1.22  thf(c_0_349, plain, ((epred3_0 @ esk3_0 @ esk4_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_330, c_0_345])).
% 5.97/1.22  thf(c_0_350, 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_9])).
% 5.97/1.22  thf(c_0_351, 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_346, c_0_13])).
% 5.97/1.22  thf(c_0_352, 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(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_347, c_0_169])])).
% 5.97/1.22  thf(c_0_353, plain, ((epred4_0 @ esk3_0 @ esk5_0)|(epred5_0 @ esk6_0 @ esk7_0)), inference(spm,[status(thm)],[c_0_348, c_0_349])).
% 5.97/1.22  thf(c_0_354, 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_9])).
% 5.97/1.22  thf(c_0_355, 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_9])).
% 5.97/1.22  thf(c_0_356, 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_350, c_0_13])).
% 5.97/1.22  thf(c_0_357, 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_9])).
% 5.97/1.22  thf(c_0_358, 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))|~((epred4_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_351, c_0_100])).
% 5.97/1.22  thf(c_0_359, plain, (epred5_0 @ esk6_0 @ esk7_0), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_352, c_0_353]), c_0_329]), c_0_336])).
% 5.97/1.22  thf(c_0_360, 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_354, c_0_13]), c_0_26])).
% 5.97/1.22  thf(c_0_361, 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_9])).
% 5.97/1.22  thf(c_0_362, 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_355, c_0_13])).
% 5.97/1.22  thf(c_0_363, 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_9])).
% 5.97/1.22  thf(c_0_364, plain, ![X3:a, X5:a, X4:a]:(((epred5_0 @ esk9_0 @ esk10_0)|(epred3_0 @ X3 @ X4)|((epred7_0)!=(epred5_0))|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred3_0 @ X3 @ X5))|~((epred4_0 @ X5 @ X4)))), inference(spm,[status(thm)],[c_0_356, c_0_100])).
% 5.97/1.22  thf(c_0_365, 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_357, c_0_13]), c_0_26])).
% 5.97/1.22  thf(c_0_366, plain, ![X4:a, X3:a]:(((epred5_0 @ esk9_0 @ esk10_0)|(epred3_0 @ X3 @ X4)|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred4_0 @ X4 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_358, c_0_169])])).
% 5.97/1.22  thf(c_0_367, plain, (epred5_0 @ esk7_0 @ esk6_0), inference(spm,[status(thm)],[c_0_320, c_0_359])).
% 5.97/1.22  thf(c_0_368, 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_360]), c_0_210])).
% 5.97/1.22  thf(c_0_369, 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_361, c_0_13])).
% 5.97/1.22  thf(c_0_370, 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_9])).
% 5.97/1.22  thf(c_0_371, 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))|~((epred4_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_362, c_0_100])).
% 5.97/1.22  thf(c_0_372, 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_363, c_0_13]), c_0_34])).
% 5.97/1.22  thf(c_0_373, plain, ![X3:a, X5:a, X4:a]:(((epred5_0 @ esk9_0 @ esk10_0)|(epred3_0 @ X3 @ X4)|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred3_0 @ X3 @ X5))|~((epred4_0 @ X5 @ X4)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_364, c_0_169])])).
% 5.97/1.22  thf(c_0_374, 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(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_365, c_0_169])])).
% 5.97/1.22  thf(c_0_375, 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_351, c_0_169])])).
% 5.97/1.22  thf(c_0_376, plain, ![X4:a, X3:a]:(((epred5_0 @ esk9_0 @ esk10_0)|(epred3_0 @ X3 @ X4)|~((epred4_0 @ X4 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_366, c_0_367])])).
% 5.97/1.22  thf(c_0_377, 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_368, c_0_367])])).
% 5.97/1.22  thf(c_0_378, 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_9])).
% 5.97/1.22  thf(c_0_379, plain, ![X3:a, X5:a, X4:a]:(((epred5_0 @ esk8_0 @ esk9_0)|(epred3_0 @ X3 @ X4)|((epred7_0)!=(epred5_0))|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred3_0 @ X3 @ X5))|~((epred4_0 @ X5 @ X4)))), inference(spm,[status(thm)],[c_0_369, c_0_100])).
% 5.97/1.22  thf(c_0_380, 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_370, c_0_13]), c_0_34])).
% 5.97/1.22  thf(c_0_381, plain, ![X4:a, X3:a]:(((epred5_0 @ esk8_0 @ esk9_0)|(epred3_0 @ X3 @ X4)|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred4_0 @ X4 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_371, c_0_169])])).
% 5.97/1.22  thf(c_0_382, 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_372]), c_0_210])).
% 5.97/1.22  thf(c_0_383, plain, ![X3:a]:(((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk9_0 @ esk10_0)|(epred3_0 @ X3 @ esk5_0)|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred3_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_373, c_0_374])).
% 5.97/1.22  thf(c_0_384, 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_375, c_0_367])])).
% 5.97/1.22  thf(c_0_385, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk4_0 @ esk3_0)|(epred5_0 @ esk9_0 @ esk10_0)), inference(spm,[status(thm)],[c_0_376, c_0_377])).
% 5.97/1.22  thf(c_0_386, 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_378, c_0_13]), c_0_26])).
% 5.97/1.22  thf(c_0_387, plain, ![X3:a, X5:a, X4:a]:(((epred5_0 @ esk8_0 @ esk9_0)|(epred3_0 @ X3 @ X4)|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred3_0 @ X3 @ X5))|~((epred4_0 @ X5 @ X4)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_379, c_0_169])])).
% 5.97/1.22  thf(c_0_388, 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_380]), c_0_222])).
% 5.97/1.22  thf(c_0_389, 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_362, c_0_169])])).
% 5.97/1.22  thf(c_0_390, plain, ![X4:a, X3:a]:(((epred5_0 @ esk8_0 @ esk9_0)|(epred3_0 @ X3 @ X4)|~((epred4_0 @ X4 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_381, c_0_367])])).
% 5.97/1.22  thf(c_0_391, 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_382, c_0_367])])).
% 5.97/1.22  thf(c_0_392, 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_9])).
% 5.97/1.22  thf(c_0_393, plain, ![X3:a]:(((epred5_0 @ esk9_0 @ esk10_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ X3 @ esk5_0)|~((epred3_0 @ X3 @ esk4_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_383, c_0_367])])).
% 5.97/1.22  thf(c_0_394, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk3_0 @ esk4_0)|(epred5_0 @ esk9_0 @ esk10_0)), inference(spm,[status(thm)],[c_0_384, c_0_385])).
% 5.97/1.22  thf(c_0_395, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred4_0 @ esk1_0 @ esk2_0)|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_386, c_0_169])])).
% 5.97/1.22  thf(c_0_396, plain, ![X3:a]:(((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk8_0 @ esk9_0)|(epred3_0 @ X3 @ esk5_0)|~((epred5_0 @ esk7_0 @ esk6_0))|~((epred3_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_387, c_0_388])).
% 5.97/1.22  thf(c_0_397, 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_389, c_0_367])])).
% 5.97/1.22  thf(c_0_398, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk4_0 @ esk3_0)|(epred5_0 @ esk8_0 @ esk9_0)), inference(spm,[status(thm)],[c_0_390, c_0_391])).
% 5.97/1.22  thf(c_0_399, 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_392, c_0_13]), c_0_34])).
% 5.97/1.22  thf(c_0_400, 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_9])).
% 5.97/1.22  thf(c_0_401, plain, ((epred3_0 @ esk3_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk9_0 @ esk10_0)), inference(spm,[status(thm)],[c_0_393, c_0_394])).
% 5.97/1.22  thf(c_0_402, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk9_0 @ esk10_0)|~((epred4_0 @ esk3_0 @ esk5_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_395, c_0_367])])).
% 5.97/1.22  thf(c_0_403, plain, ![X3:a]:(((epred5_0 @ esk8_0 @ esk9_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ X3 @ esk5_0)|~((epred3_0 @ X3 @ esk4_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_396, c_0_367])])).
% 5.97/1.22  thf(c_0_404, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ esk3_0 @ esk4_0)|(epred5_0 @ esk8_0 @ esk9_0)), inference(spm,[status(thm)],[c_0_397, c_0_398])).
% 5.97/1.22  thf(c_0_405, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred4_0 @ esk1_0 @ esk2_0)|~((epred4_0 @ esk3_0 @ esk5_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_399, c_0_169])])).
% 5.97/1.22  thf(c_0_406, 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_400, c_0_13])).
% 5.97/1.22  thf(c_0_407, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_101, c_0_401]), c_0_402])).
% 5.97/1.22  thf(c_0_408, plain, ((epred3_0 @ esk3_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk8_0 @ esk9_0)), inference(spm,[status(thm)],[c_0_403, c_0_404])).
% 5.97/1.22  thf(c_0_409, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ esk8_0 @ esk9_0)|~((epred4_0 @ esk3_0 @ esk5_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_405, c_0_367])])).
% 5.97/1.22  thf(c_0_410, 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_406, c_0_169])])).
% 5.97/1.22  thf(c_0_411, plain, ![X3:a]:(((epred4_0 @ esk1_0 @ esk2_0)|(epred5_0 @ X3 @ esk10_0)|~((epred5_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_258, c_0_407])).
% 5.97/1.22  thf(c_0_412, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_101, c_0_408]), c_0_409])).
% 5.97/1.22  thf(c_0_413, 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_9])).
% 5.97/1.22  thf(c_0_414, 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_9])).
% 5.97/1.22  thf(c_0_415, 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_410, c_0_367])])).
% 5.97/1.22  thf(c_0_416, plain, ((epred5_0 @ esk8_0 @ esk10_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_411, c_0_412])).
% 5.97/1.22  thf(c_0_417, 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_413, c_0_13]), c_0_59])).
% 5.97/1.22  thf(c_0_418, 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_9])).
% 5.97/1.22  thf(c_0_419, 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_414, c_0_13])).
% 5.97/1.22  thf(c_0_420, plain, ![X4:a, X3:a]:(((epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ X3 @ X4)|~((epred3_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_415, c_0_416])).
% 5.97/1.22  thf(c_0_421, 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_417]), c_0_222])).
% 5.97/1.22  thf(c_0_422, 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_418, c_0_13]), c_0_59])).
% 5.97/1.22  thf(c_0_423, 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_9])).
% 5.97/1.22  thf(c_0_424, 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_419, c_0_169])])).
% 5.97/1.22  thf(c_0_425, plain, ![X4:a, X3:a]:(((epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ X3 @ X4)|~((epred4_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_420, c_0_100])).
% 5.97/1.22  thf(c_0_426, 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_421, c_0_367])])).
% 5.97/1.22  thf(c_0_427, 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_422]), c_0_210])).
% 5.97/1.22  thf(c_0_428, 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_423, c_0_13]), c_0_34])).
% 5.97/1.22  thf(c_0_429, 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_9])).
% 5.97/1.22  thf(c_0_430, 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_9])).
% 5.97/1.22  thf(c_0_431, 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_424, c_0_367])])).
% 5.97/1.22  thf(c_0_432, plain, ((epred3_0 @ esk5_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_425, c_0_426]), c_0_416])).
% 5.97/1.22  thf(c_0_433, 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_427, c_0_367])])).
% 5.97/1.22  thf(c_0_434, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred4_0 @ esk3_0 @ esk4_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_428, c_0_169])])).
% 5.97/1.22  thf(c_0_435, 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_429, c_0_13]), c_0_34])).
% 5.97/1.22  thf(c_0_436, 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_430, c_0_13]), c_0_26])).
% 5.97/1.22  thf(c_0_437, 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_9])).
% 5.97/1.22  thf(c_0_438, 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_9])).
% 5.97/1.22  thf(c_0_439, plain, ![X3:a, X4:a, X5:a]:(((epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ X3 @ X4)|~((epred3_0 @ X5 @ X4))|~((epred3_0 @ X3 @ X5)))), inference(spm,[status(thm)],[c_0_431, c_0_416])).
% 5.97/1.22  thf(c_0_440, plain, ((epred3_0 @ esk4_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_420, c_0_432])).
% 5.97/1.22  thf(c_0_441, plain, ((epred3_0 @ esk4_0 @ esk3_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_425, c_0_433]), c_0_416])).
% 5.97/1.22  thf(c_0_442, 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_369, c_0_169])])).
% 5.97/1.22  thf(c_0_443, plain, ((epred4_0 @ esk3_0 @ esk4_0)|(epred5_0 @ esk8_0 @ esk9_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_434, c_0_367])])).
% 5.97/1.22  thf(c_0_444, plain, ((epred5_0 @ esk8_0 @ esk9_0)|(epred4_0 @ esk4_0 @ esk5_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_435, c_0_169])])).
% 5.97/1.22  thf(c_0_445, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred4_0 @ esk3_0 @ esk4_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_436, c_0_169])])).
% 5.97/1.22  thf(c_0_446, 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_437, c_0_13]), c_0_26])).
% 5.97/1.22  thf(c_0_447, 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_438, c_0_13]), c_0_59])).
% 5.97/1.22  thf(c_0_448, plain, ![X3:a]:(((epred4_0 @ esk1_0 @ esk2_0)|(epred3_0 @ X3 @ esk5_0)|~((epred3_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_439, c_0_440])).
% 5.97/1.22  thf(c_0_449, plain, ((epred3_0 @ esk3_0 @ esk4_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_420, c_0_441])).
% 5.97/1.22  thf(c_0_450, 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_442, c_0_367])])).
% 5.97/1.22  thf(c_0_451, plain, ((epred3_0 @ esk4_0 @ esk3_0)|(epred5_0 @ esk8_0 @ esk9_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(spm,[status(thm)],[c_0_390, c_0_443])).
% 5.97/1.22  thf(c_0_452, plain, ((epred4_0 @ esk4_0 @ esk5_0)|(epred5_0 @ esk8_0 @ esk9_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_444, c_0_367])])).
% 5.97/1.22  thf(c_0_453, 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_9])).
% 5.97/1.22  thf(c_0_454, 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_356, c_0_169])])).
% 5.97/1.22  thf(c_0_455, plain, ((epred4_0 @ esk3_0 @ esk4_0)|(epred5_0 @ esk9_0 @ esk10_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_445, c_0_367])])).
% 5.97/1.22  thf(c_0_456, plain, ((epred5_0 @ esk9_0 @ esk10_0)|(epred4_0 @ esk4_0 @ esk5_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred5_0 @ esk7_0 @ esk6_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_446, c_0_169])])).
% 5.97/1.22  thf(c_0_457, 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_447, c_0_169])])).
% 5.97/1.22  thf(c_0_458, plain, ((epred3_0 @ esk3_0 @ esk5_0)|(epred4_0 @ esk1_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_448, c_0_449])).
% 5.97/1.22  thf(c_0_459, plain, ![X3:a]:(((epred5_0 @ esk8_0 @ esk9_0)|(epred3_0 @ X3 @ esk3_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred3_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_450, c_0_451])).
% 5.97/1.22  thf(c_0_460, plain, ((epred3_0 @ esk5_0 @ esk4_0)|(epred5_0 @ esk8_0 @ esk9_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(spm,[status(thm)],[c_0_390, c_0_452])).
% 5.97/1.22  thf(c_0_461, 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_453, c_0_13]), c_0_34])).
% 5.97/1.22  thf(c_0_462, 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_454, c_0_367])])).
% 5.97/1.22  thf(c_0_463, plain, ((epred3_0 @ esk4_0 @ esk3_0)|(epred5_0 @ esk9_0 @ esk10_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(spm,[status(thm)],[c_0_376, c_0_455])).
% 5.97/1.22  thf(c_0_464, plain, ((epred4_0 @ esk4_0 @ esk5_0)|(epred5_0 @ esk9_0 @ esk10_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_456, c_0_367])])).
% 5.97/1.22  thf(c_0_465, 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_9])).
% 5.97/1.22  thf(c_0_466, 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_457, c_0_367])])).
% 5.97/1.22  thf(c_0_467, plain, ((epred4_0 @ esk1_0 @ esk2_0)|(epred4_0 @ esk3_0 @ esk5_0)), inference(spm,[status(thm)],[c_0_101, c_0_458])).
% 5.97/1.22  thf(c_0_468, plain, ((epred3_0 @ esk5_0 @ esk3_0)|(epred5_0 @ esk8_0 @ esk9_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(spm,[status(thm)],[c_0_459, c_0_460])).
% 5.97/1.22  thf(c_0_469, 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(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_461, c_0_169])])).
% 5.97/1.22  thf(c_0_470, plain, ![X3:a]:(((epred5_0 @ esk9_0 @ esk10_0)|(epred3_0 @ X3 @ esk3_0)|~((epred4_0 @ esk2_0 @ esk1_0))|~((epred3_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_462, c_0_463])).
% 5.97/1.22  thf(c_0_471, plain, ((epred3_0 @ esk5_0 @ esk4_0)|(epred5_0 @ esk9_0 @ esk10_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(spm,[status(thm)],[c_0_376, c_0_464])).
% 5.97/1.22  thf(c_0_472, 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_465, c_0_13]), c_0_26])).
% 5.97/1.22  thf(c_0_473, plain, (epred4_0 @ esk1_0 @ esk2_0), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_466, c_0_467]), c_0_416])).
% 5.97/1.22  thf(c_0_474, plain, ((epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ esk8_0 @ esk9_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(spm,[status(thm)],[c_0_397, c_0_468])).
% 5.97/1.22  thf(c_0_475, 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_469, c_0_367])])).
% 5.97/1.22  thf(c_0_476, plain, ((epred3_0 @ esk5_0 @ esk3_0)|(epred5_0 @ esk9_0 @ esk10_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(spm,[status(thm)],[c_0_470, c_0_471])).
% 5.97/1.22  thf(c_0_477, 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(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_472, c_0_169])])).
% 5.97/1.22  thf(c_0_478, plain, ((epred3_0 @ esk2_0 @ esk1_0)|(epred5_0 @ esk8_0 @ esk9_0)), inference(spm,[status(thm)],[c_0_390, c_0_473])).
% 5.97/1.22  thf(c_0_479, plain, ((epred5_0 @ esk8_0 @ esk9_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_101, c_0_474]), c_0_475])).
% 5.97/1.22  thf(c_0_480, plain, ((epred3_0 @ esk3_0 @ esk5_0)|(epred5_0 @ esk9_0 @ esk10_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(spm,[status(thm)],[c_0_384, c_0_476])).
% 5.97/1.22  thf(c_0_481, 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_477, c_0_367])])).
% 5.97/1.22  thf(c_0_482, plain, (epred5_0 @ esk8_0 @ esk9_0), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_101, c_0_478]), c_0_479])).
% 5.97/1.22  thf(c_0_483, plain, ((epred3_0 @ esk2_0 @ esk1_0)|(epred5_0 @ esk9_0 @ esk10_0)), inference(spm,[status(thm)],[c_0_376, c_0_473])).
% 5.97/1.22  thf(c_0_484, plain, ((epred5_0 @ esk9_0 @ esk10_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_101, c_0_480]), c_0_481])).
% 5.97/1.22  thf(c_0_485, plain, (epred5_0 @ esk9_0 @ esk8_0), inference(spm,[status(thm)],[c_0_320, c_0_482])).
% 5.97/1.22  thf(c_0_486, plain, (epred5_0 @ esk9_0 @ esk10_0), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_101, c_0_483]), c_0_484])).
% 5.97/1.22  thf(c_0_487, plain, ![X3:a]:(((epred5_0 @ X3 @ esk8_0)|~((epred5_0 @ X3 @ esk9_0)))), inference(spm,[status(thm)],[c_0_258, c_0_485])).
% 5.97/1.22  thf(c_0_488, plain, (epred5_0 @ esk10_0 @ esk9_0), inference(spm,[status(thm)],[c_0_320, c_0_486])).
% 5.97/1.22  thf(c_0_489, plain, (epred5_0 @ esk10_0 @ esk8_0), inference(spm,[status(thm)],[c_0_487, c_0_488])).
% 5.97/1.22  thf(c_0_490, 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_9])).
% 5.97/1.22  thf(c_0_491, plain, (epred5_0 @ esk8_0 @ esk10_0), inference(spm,[status(thm)],[c_0_320, c_0_489])).
% 5.97/1.22  thf(c_0_492, 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_490, c_0_13]), c_0_59])).
% 5.97/1.22  thf(c_0_493, plain, ![X4:a, X3:a]:(((epred3_0 @ X3 @ X4)|~((epred3_0 @ X4 @ X3)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_415, c_0_491])])).
% 5.97/1.22  thf(c_0_494, 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_492, c_0_169])])).
% 5.97/1.22  thf(c_0_495, plain, ![X4:a, X3:a]:(((epred3_0 @ X3 @ X4)|~((epred4_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_493, c_0_100])).
% 5.97/1.22  thf(c_0_496, 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_9])).
% 5.97/1.22  thf(c_0_497, 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_494, c_0_367])])).
% 5.97/1.22  thf(c_0_498, plain, ![X4:a, X3:a]:(((epred4_0 @ X3 @ X4)|~((epred4_0 @ X4 @ X3)))), inference(spm,[status(thm)],[c_0_101, c_0_495])).
% 5.97/1.22  thf(c_0_499, 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_496, c_0_13]), c_0_59])).
% 5.97/1.22  thf(c_0_500, 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_9])).
% 5.97/1.22  thf(c_0_501, 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_431, c_0_491])])).
% 5.97/1.22  thf(c_0_502, plain, ((epred4_0 @ esk4_0 @ esk5_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_497, c_0_491])])).
% 5.97/1.22  thf(c_0_503, plain, (epred4_0 @ esk2_0 @ esk1_0), inference(spm,[status(thm)],[c_0_498, c_0_473])).
% 5.97/1.22  thf(c_0_504, 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_499, c_0_169])])).
% 5.97/1.22  thf(c_0_505, 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_500, c_0_13]), c_0_59])).
% 5.97/1.22  thf(c_0_506, 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_501, c_0_100])).
% 5.97/1.22  thf(c_0_507, plain, (epred4_0 @ esk4_0 @ esk5_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_502, c_0_503])])).
% 5.97/1.22  thf(c_0_508, 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_504, c_0_367])])).
% 5.97/1.22  thf(c_0_509, 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(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_505, c_0_169])])).
% 5.97/1.22  thf(c_0_510, plain, ![X3:a]:(((epred3_0 @ X3 @ esk5_0)|~((epred3_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_506, c_0_507])).
% 5.97/1.22  thf(c_0_511, plain, ((epred4_0 @ esk3_0 @ esk4_0)|~((epred4_0 @ esk2_0 @ esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_508, c_0_491])])).
% 5.97/1.22  thf(c_0_512, 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_509, c_0_367])])).
% 5.97/1.22  thf(c_0_513, plain, ![X3:a]:(((epred4_0 @ X3 @ esk5_0)|~((epred3_0 @ X3 @ esk4_0)))), inference(spm,[status(thm)],[c_0_101, c_0_510])).
% 5.97/1.22  thf(c_0_514, plain, (epred4_0 @ esk3_0 @ esk4_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_511, c_0_503])])).
% 5.97/1.22  thf(c_0_515, plain, (~((epred4_0 @ esk2_0 @ esk1_0))|~((epred4_0 @ esk3_0 @ esk5_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_512, c_0_491])])).
% 5.97/1.22  thf(c_0_516, plain, ![X3:a]:(((epred4_0 @ X3 @ esk5_0)|~((epred4_0 @ esk4_0 @ X3)))), inference(spm,[status(thm)],[c_0_513, c_0_495])).
% 5.97/1.22  thf(c_0_517, plain, (epred4_0 @ esk4_0 @ esk3_0), inference(spm,[status(thm)],[c_0_498, c_0_514])).
% 5.97/1.22  thf(c_0_518, plain, ~((epred4_0 @ esk3_0 @ esk5_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_515, c_0_503])])).
% 5.97/1.22  thf(c_0_519, plain, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_516, c_0_517]), c_0_518]), ['proof']).
% 5.97/1.22  % SZS output end CNFRefutation
% 5.97/1.22  % Parsed axioms                        : 2
% 5.97/1.22  % Removed by relevancy pruning/SinE    : 1
% 5.97/1.22  % Initial clauses                      : 70
% 5.97/1.22  % Removed in clause preprocessing      : 0
% 5.97/1.22  % Initial clauses in saturation        : 70
% 5.97/1.22  % Processed clauses                    : 4160
% 5.97/1.22  % ...of these trivial                  : 168
% 5.97/1.22  % ...subsumed                          : 2027
% 5.97/1.22  % ...remaining for further processing  : 1965
% 5.97/1.22  % Other redundant clauses eliminated   : 0
% 5.97/1.22  % Clauses deleted for lack of memory   : 0
% 5.97/1.22  % Backward-subsumed                    : 836
% 5.97/1.22  % Backward-rewritten                   : 515
% 5.97/1.22  % Generated clauses                    : 10405
% 5.97/1.22  % ...of the previous two non-redundant : 9800
% 5.97/1.22  % ...aggressively subsumed             : 0
% 5.97/1.22  % Contextual simplify-reflections      : 119
% 5.97/1.22  % Paramodulations                      : 8490
% 5.97/1.22  % Factorizations                       : 0
% 5.97/1.22  % NegExts                              : 137
% 5.97/1.22  % Equation resolutions                 : 0
% 5.97/1.22  % Disequality decompositions           : 0
% 5.97/1.22  % Total rewrite steps                  : 821
% 5.97/1.22  % ...of those cached                   : 585
% 5.97/1.22  % Propositional unsat checks           : 0
% 5.97/1.22  %    Propositional check models        : 0
% 5.97/1.22  %    Propositional check unsatisfiable : 0
% 5.97/1.22  %    Propositional clauses             : 0
% 5.97/1.22  %    Propositional clauses after purity: 0
% 5.97/1.22  %    Propositional unsat core size     : 0
% 5.97/1.22  %    Propositional preprocessing time  : 0.000
% 5.97/1.22  %    Propositional encoding time       : 0.000
% 5.97/1.22  %    Propositional solver time         : 0.000
% 5.97/1.22  %    Success case prop preproc time    : 0.000
% 5.97/1.22  %    Success case prop encoding time   : 0.000
% 5.97/1.22  %    Success case prop solver time     : 0.000
% 5.97/1.22  % Current number of processed clauses  : 81
% 5.97/1.22  %    Positive orientable unit clauses  : 26
% 5.97/1.22  %    Positive unorientable unit clauses: 0
% 5.97/1.22  %    Negative unit clauses             : 2
% 5.97/1.22  %    Non-unit-clauses                  : 53
% 5.97/1.22  % Current number of unprocessed clauses: 25
% 5.97/1.22  % ...number of literals in the above   : 56
% 5.97/1.22  % Current number of archived formulas  : 0
% 5.97/1.22  % Current number of archived clauses   : 1884
% 5.97/1.22  % Clause-clause subsumption calls (NU) : 158132
% 5.97/1.22  % Rec. Clause-clause subsumption calls : 70720
% 5.97/1.22  % Non-unit clause-clause subsumptions  : 2948
% 5.97/1.22  % Unit Clause-clause subsumption calls : 1056
% 5.97/1.22  % Rewrite failures with RHS unbound    : 0
% 5.97/1.22  % BW rewrite match attempts            : 49
% 5.97/1.22  % BW rewrite match successes           : 45
% 5.97/1.22  % Condensation attempts                : 0
% 5.97/1.22  % Condensation successes               : 0
% 5.97/1.22  % Termbank termtop insertions          : 249965
% 5.97/1.22  % Search garbage collected termcells   : 1070
% 5.97/1.22  
% 5.97/1.22  % -------------------------------------------------
% 5.97/1.22  % User time                : 0.819 s
% 5.97/1.22  % System time              : 0.015 s
% 5.97/1.22  % Total time               : 0.834 s
% 5.97/1.22  % Maximum resident set size: 3648 pages
% 5.97/1.22  
% 5.97/1.22  % -------------------------------------------------
% 5.97/1.22  % User time                : 2.431 s
% 5.97/1.22  % System time              : 0.060 s
% 5.97/1.22  % Total time               : 2.490 s
% 5.97/1.22  % Maximum resident set size: 4864 pages
% 5.97/1.22  % E exiting
%------------------------------------------------------------------------------