%------------------------------------------------------------------------------
% File : E-SAT---3.5.1
% Problem : ALG294^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 : n011.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 07:45:00 AM UTC 2026
% Result : Theorem 0.25s 0.31s
% Output : CNFRefutation 0.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG294^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.17 % Computer : n011.cluster.edu
% 0.07/0.17 % Model : x86_64 x86_64
% 0.07/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.17 % Memory : 8046.5625MB
% 0.07/0.17 % OS : Linux 6.8.0-71-generic
% 0.07/0.17 % CPULimit : 300
% 0.07/0.17 % WCLimit : 300
% 0.07/0.17 % DateTime : Tue Sep 29 17:37:31 UTC 2026
% 0.07/0.17 % CPUTime :
% 0.07/0.17 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.21 Running higher-order theorem proving
% 0.07/0.22 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.OrutXsUgDL/E---3.1_412705.p
% 0.25/0.31 % Version: 3.5.1-ho
% 0.25/0.31 % Preprocessing class: HSMSSMSSSSMNSSA.
% 0.25/0.31 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.25/0.31 % Starting lpo6_lambda_fix with 900s (3) cores
% 0.25/0.31 % Starting post_as_ho3 with 600s (2) cores
% 0.25/0.31 % Starting new_ho_16 with 600s (2) cores
% 0.25/0.31 % Starting full_lambda_1 with 300s (1) cores
% 0.25/0.31 % new_ho_16 with pid 412720 completed with status 0
% 0.25/0.31 % Result found by new_ho_16
% 0.25/0.31 % Preprocessing class: HSMSSMSSSSMNSSA.
% 0.25/0.31 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.25/0.31 % Starting lpo6_lambda_fix with 900s (3) cores
% 0.25/0.31 % Starting post_as_ho3 with 600s (2) cores
% 0.25/0.31 % Starting new_ho_16 with 600s (2) cores
% 0.25/0.31 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 1, sine = LambdaDef)
% 0.25/0.31 % SinE strategy is LambdaDef
% 0.25/0.31 % Search class: HGHSF-FFMM32-DSSFFSBN
% 0.25/0.31 % partial match(2): HGHNF-FFMM32-SSSFFSBN
% 0.25/0.31 % Scheduled 7 strats onto 2 cores with 600 seconds (600 total)
% 0.25/0.31 % Starting SubtermCWHack with 55s (1) cores
% 0.25/0.31 % Starting new_ho_16 with 61s (1) cores
% 0.25/0.31 % new_ho_16 with pid 412726 completed with status 0
% 0.25/0.31 % Result found by new_ho_16
% 0.25/0.31 % Preprocessing class: HSMSSMSSSSMNSSA.
% 0.25/0.31 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.25/0.31 % Starting lpo6_lambda_fix with 900s (3) cores
% 0.25/0.31 % Starting post_as_ho3 with 600s (2) cores
% 0.25/0.31 % Starting new_ho_16 with 600s (2) cores
% 0.25/0.31 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 1, sine = LambdaDef)
% 0.25/0.31 % SinE strategy is LambdaDef
% 0.25/0.31 % Search class: HGHSF-FFMM32-DSSFFSBN
% 0.25/0.31 % partial match(2): HGHNF-FFMM32-SSSFFSBN
% 0.25/0.31 % Scheduled 7 strats onto 2 cores with 600 seconds (600 total)
% 0.25/0.31 % Starting SubtermCWHack with 55s (1) cores
% 0.25/0.31 % Starting new_ho_16 with 61s (1) cores
% 0.25/0.31 % Preprocessing time : 0.003 s
% 0.25/0.31
% 0.25/0.31 % Proof found!
% 0.25/0.31 % SZS status Theorem
% 0.25/0.31 % SZS output start CNFRefutation
% 0.25/0.31 thf(decl_sort1, type, a: $tType).
% 0.25/0.31 thf(decl_23, type, cR: a > a).
% 0.25/0.31 thf(decl_24, type, cL: a > a).
% 0.25/0.31 thf(decl_25, type, cPSI: (a > $o) > a > $o).
% 0.25/0.31 thf(decl_26, type, cP: a > a > a).
% 0.25/0.31 thf(decl_27, type, cZ: a).
% 0.25/0.31 thf(decl_28, type, cPHI: (a > $o) > a > $o).
% 0.25/0.31 thf(decl_29, type, epred1_0: $o).
% 0.25/0.31 thf(decl_30, type, esk1_0: a).
% 0.25/0.31 thf(decl_31, type, esk2_0: a).
% 0.25/0.31 thf(decl_32, type, esk3_0: a).
% 0.25/0.31 thf(decl_33, type, esk4_0: a).
% 0.25/0.31 thf(decl_34, type, esk5_0: a).
% 0.25/0.31 thf(decl_35, type, esk6_0: a).
% 0.25/0.31 thf(decl_36, type, esk7_0: a).
% 0.25/0.31 thf(decl_37, type, esk8_1: (a > $o) > a).
% 0.25/0.31 thf(decl_38, type, esk9_2: (a > $o) > a > a).
% 0.25/0.31 thf(decl_39, type, epred2_3: (a > $o) > a > a > a > $o).
% 0.25/0.31 thf(decl_40, type, esk10_3: (a > $o) > a > a > a).
% 0.25/0.31 thf(decl_41, type, esk11_4: (a > $o) > a > a > (a > $o) > a).
% 0.25/0.31 thf(decl_42, type, esk12_4: (a > $o) > a > a > (a > $o) > a).
% 0.25/0.31 thf(decl_43, type, esk13_2: (a > $o) > a > a).
% 0.25/0.31 thf(decl_44, type, epred3_3: (a > $o) > a > a > a > $o).
% 0.25/0.31 thf(decl_45, type, esk14_3: (a > $o) > a > a > a).
% 0.25/0.31 thf(decl_46, type, esk15_4: (a > $o) > a > a > (a > $o) > a).
% 0.25/0.31 thf(decl_47, type, esk16_4: (a > $o) > a > a > (a > $o) > a).
% 0.25/0.31 thf(cPU_X2310B_pme, conjecture, ((((((((((cL @ cZ)=(cZ))&((cR @ cZ)=(cZ)))&![X1:a, X2:a]:(((cL @ (cP @ X1 @ X2))=(X1))))&![X1:a, X2:a]:(((cR @ (cP @ X1 @ X2))=(X2))))&![X3:a]:((((X3)!=(cZ))<=>((X3)=(cP @ (cL @ X3) @ (cR @ X3))))))&![X4:a > $o]:((?[X3:a]:(((X4 @ X3)&![X5:a]:(((X4 @ X5)=>(X4 @ (cL @ X5))))))=>(X4 @ cZ))))&![X4:a > $o, X6:a]:(((cPHI @ X4 @ X6)<=>?[X1:a]:((![X7:a]:((![X8:a > $o]:((((X8 @ X1)&![X9:a]:(((X8 @ X9)=>(X8 @ (cL @ X9)))))=>?[X10:a]:(((X8 @ X10)&((cR @ X10)=(X7))))))=>(X4 @ X7)))&(cPHI @ (^[X2:a]:(![X8:a > $o]:((((((X8 @ X1))&(![X9:a]:((((X8 @ X9))=>((X8 @ (cL @ X9))))))))=>(?[X10:a]:((((X8 @ X10))&(((cR @ X10)=(X2)))))))))) @ X6))))))&![X4:a > $o, X6:a]:(((cPSI @ X4 @ X6)<=>?[X1:a]:((![X11:a]:((![X8:a > $o]:((((X8 @ X1)&![X9:a]:(((X8 @ X9)=>(X8 @ (cL @ X9)))))=>?[X10:a]:(((X8 @ X10)&((cR @ X10)=(X11))))))=>(X4 @ X11)))&(cPSI @ (^[X2:a]:(![X8:a > $o]:((((((X8 @ X1))&(![X9:a]:((((X8 @ X9))=>((X8 @ (cL @ X9))))))))=>(?[X10:a]:((((X8 @ X10))&(((cR @ X10)=(X2)))))))))) @ X6))))))=>((^[X5:a]:(((((X5)=(cZ)))|(?[X1:a, X2:a]:(((((X5)=(cP @ X1 @ X2)))&((((cPHI @ (^[X12:a]:(![X4:a > $o]:((((((X4 @ X1))&(![X6:a]:((((X4 @ X6))=>((X4 @ (cL @ X6))))))))=>(?[X10:a]:((((X4 @ X10))&(((cR @ X10)=(X12)))))))))) @ X2))|((cPSI @ (^[X12:a]:(![X4:a > $o]:((((((X4 @ X1))&(![X6:a]:((((X4 @ X6))=>((X4 @ (cL @ X6))))))))=>(?[X10:a]:((((X4 @ X10))&(((cR @ X10)=(X12)))))))))) @ X2))))))))))=(^[X6:a]:(((((((((X6)=(cZ)))|(?[X1:a, X2:a]:(((((X6)=(cP @ X1 @ X2)))&((cPHI @ (^[X12:a]:(![X4:a > $o]:((((((X4 @ X1))&(![X9:a]:((((X4 @ X9))=>((X4 @ (cL @ X9))))))))=>(?[X10:a]:((((X4 @ X10))&(((cR @ X10)=(X12)))))))))) @ X2)))))))|(((X6)=(cZ)))))|(?[X1:a, X2:a]:(((((X6)=(cP @ X1 @ X2)))&((cPSI @ (^[X12:a]:(![X4:a > $o]:((((((X4 @ X1))&(![X9:a]:((((X4 @ X9))=>((X4 @ (cL @ X9))))))))=>(?[X10:a]:((((X4 @ X10))&(((cR @ X10)=(X12)))))))))) @ X2)))))))))), file('/export/starexec/sandbox/tmp/tmp.OrutXsUgDL/E---3.1_412705.p', cPU_X2310B_pme)).
% 0.25/0.31 thf(c_0_1, negated_conjecture, ~(((((((((((cL @ cZ)=(cZ))&((cR @ cZ)=(cZ)))&![X1:a, X2:a]:(((cL @ (cP @ X1 @ X2))=(X1))))&![X1:a, X2:a]:(((cR @ (cP @ X1 @ X2))=(X2))))&![X3:a]:((((X3)!=(cZ))<=>((X3)=(cP @ (cL @ X3) @ (cR @ X3))))))&![X4:a > $o]:((?[X3:a]:(((X4 @ X3)&![X5:a]:(((X4 @ X5)=>(X4 @ (cL @ X5))))))=>(X4 @ cZ))))&![X4:a > $o, X6:a]:(((cPHI @ X4 @ X6)<=>?[X1:a]:((![X7:a]:((![X8:a > $o]:((((X8 @ X1)&![X9:a]:(((X8 @ X9)=>(X8 @ (cL @ X9)))))=>?[X10:a]:(((X8 @ X10)&((cR @ X10)=(X7))))))=>(X4 @ X7)))&(cPHI @ (^[X2:a]:(![X8:a > $o]:((((((X8 @ X1))&(![X9:a]:((((X8 @ X9))=>((X8 @ (cL @ X9))))))))=>(?[X10:a]:((((X8 @ X10))&(((cR @ X10)=(X2)))))))))) @ X6))))))&![X4:a > $o, X6:a]:(((cPSI @ X4 @ X6)<=>?[X1:a]:((![X11:a]:((![X8:a > $o]:((((X8 @ X1)&![X9:a]:(((X8 @ X9)=>(X8 @ (cL @ X9)))))=>?[X10:a]:(((X8 @ X10)&((cR @ X10)=(X11))))))=>(X4 @ X11)))&(cPSI @ (^[X2:a]:(![X8:a > $o]:((((((X8 @ X1))&(![X9:a]:((((X8 @ X9))=>((X8 @ (cL @ X9))))))))=>(?[X10:a]:((((X8 @ X10))&(((cR @ X10)=(X2)))))))))) @ X6))))))=>((^[X5:a]:(((((X5)=(cZ)))|(?[X1:a, X2:a]:(((((X5)=(cP @ X1 @ X2)))&((((cPHI @ (^[X12:a]:(![X4:a > $o]:((((((X4 @ X1))&(![X6:a]:((((X4 @ X6))=>((X4 @ (cL @ X6))))))))=>(?[X10:a]:((((X4 @ X10))&(((cR @ X10)=(X12)))))))))) @ X2))|((cPSI @ (^[X12:a]:(![X4:a > $o]:((((((X4 @ X1))&(![X6:a]:((((X4 @ X6))=>((X4 @ (cL @ X6))))))))=>(?[X10:a]:((((X4 @ X10))&(((cR @ X10)=(X12)))))))))) @ X2))))))))))=(^[X6:a]:(((((((((X6)=(cZ)))|(?[X1:a, X2:a]:(((((X6)=(cP @ X1 @ X2)))&((cPHI @ (^[X12:a]:(![X4:a > $o]:((((((X4 @ X1))&(![X9:a]:((((X4 @ X9))=>((X4 @ (cL @ X9))))))))=>(?[X10:a]:((((X4 @ X10))&(((cR @ X10)=(X12)))))))))) @ X2)))))))|(((X6)=(cZ)))))|(?[X1:a, X2:a]:(((((X6)=(cP @ X1 @ X2)))&((cPSI @ (^[X12:a]:(![X4:a > $o]:((((((X4 @ X1))&(![X9:a]:((((X4 @ X9))=>((X4 @ (cL @ X9))))))))=>(?[X10:a]:((((X4 @ X10))&(((cR @ X10)=(X12)))))))))) @ X2))))))))))), inference(assume_negation,[status(cth)],[cPU_X2310B_pme])).
% 0.25/0.31 thf(c_0_2, plain, ((epred1_0)<=>(((((((((cL @ cZ)=(cZ))&((cR @ cZ)=(cZ)))&![X1:a, X2:a]:(((cL @ (cP @ X1 @ X2))=(X1))))&![X1:a, X2:a]:(((cR @ (cP @ X1 @ X2))=(X2))))&![X3:a]:((((X3)!=(cZ))<=>((X3)=(cP @ (cL @ X3) @ (cR @ X3))))))&![X4:a > $o]:((?[X3:a]:(((X4 @ X3)&![X5:a]:(((X4 @ X5)=>(X4 @ (cL @ X5))))))=>(X4 @ cZ))))&![X4:a > $o, X6:a]:(((cPHI @ X4 @ X6)<=>?[X1:a]:((![X7:a]:((![X8:a > $o]:((((X8 @ X1)&![X9:a]:(((X8 @ X9)=>(X8 @ (cL @ X9)))))=>?[X10:a]:(((X8 @ X10)&((cR @ X10)=(X7))))))=>(X4 @ X7)))&(cPHI @ (^[Z0:a]:(![X8:a > $o]:(((((X8 @ X1)&(![X9:a]:(((X8 @ X9)=>(X8 @ (cL @ X9)))))))=>(?[X10:a]:(((X8 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X6))))))&![X4:a > $o, X6:a]:(((cPSI @ X4 @ X6)<=>?[X1:a]:((![X11:a]:((![X8:a > $o]:((((X8 @ X1)&![X9:a]:(((X8 @ X9)=>(X8 @ (cL @ X9)))))=>?[X10:a]:(((X8 @ X10)&((cR @ X10)=(X11))))))=>(X4 @ X11)))&(cPSI @ (^[Z0:a]:(![X8:a > $o]:(((((X8 @ X1)&(![X9:a]:(((X8 @ X9)=>(X8 @ (cL @ X9)))))))=>(?[X10:a]:(((X8 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X6))))))), introduced(definition)).
% 0.25/0.31 thf(c_0_3, negated_conjecture, ~(((epred1_0)=>![X35:a]:(((((X35)=(cZ))|?[X1:a, X2:a]:((((X35)=(cP @ X1 @ X2))&((cPHI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ X1)&(![X6:a]:(((X4 @ X6)=>(X4 @ (cL @ X6)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X2)|(cPSI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ X1)&(![X6:a]:(((X4 @ X6)=>(X4 @ (cL @ X6)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X2)))))<=>(((X35)=(cZ))|?[X1:a, X2:a]:((((X35)=(cP @ X1 @ X2))&(cPHI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ X1)&(![X9:a]:(((X4 @ X9)=>(X4 @ (cL @ X9)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X2)))|((X35)=(cZ))|?[X1:a, X2:a]:((((X35)=(cP @ X1 @ X2))&(cPSI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ X1)&(![X9:a]:(((X4 @ X9)=>(X4 @ (cL @ X9)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X2)))))))), inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_1])])]), c_0_2])).
% 0.25/0.31 thf(c_0_4, negated_conjecture, ![X37:a, X38:a, X39:a, X40:a, X41:a, X42:a]:(((epred1_0)&((((((((esk1_0)!=(cZ))|((esk1_0)!=(cZ)))&(((esk1_0)!=(cP @ X39 @ X40))|~(cPHI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ X39)&(![X9:a]:(((X4 @ X9)=>(X4 @ (cL @ X9)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X40)|((esk1_0)!=(cZ))))&(((esk1_0)!=(cZ))|((esk1_0)!=(cZ))))&(((esk1_0)!=(cP @ X41 @ X42))|~(cPSI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ X41)&(![X9:a]:(((X4 @ X9)=>(X4 @ (cL @ X9)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X42)|((esk1_0)!=(cZ))))&(((((((esk1_0)!=(cZ))|(~(cPHI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ X37)&(![X6:a]:(((X4 @ X6)=>(X4 @ (cL @ X6)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X38)|((esk1_0)!=(cP @ X37 @ X38))))&(((esk1_0)!=(cP @ X39 @ X40))|~(cPHI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ X39)&(![X9:a]:(((X4 @ X9)=>(X4 @ (cL @ X9)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X40)|(~(cPHI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ X37)&(![X6:a]:(((X4 @ X6)=>(X4 @ (cL @ X6)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X38)|((esk1_0)!=(cP @ X37 @ X38)))))&(((esk1_0)!=(cZ))|(~(cPHI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ X37)&(![X6:a]:(((X4 @ X6)=>(X4 @ (cL @ X6)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X38)|((esk1_0)!=(cP @ X37 @ X38)))))&(((esk1_0)!=(cP @ X41 @ X42))|~(cPSI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ X41)&(![X9:a]:(((X4 @ X9)=>(X4 @ (cL @ X9)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X42)|(~(cPHI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ X37)&(![X6:a]:(((X4 @ X6)=>(X4 @ (cL @ X6)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X38)|((esk1_0)!=(cP @ X37 @ X38)))))&((((((esk1_0)!=(cZ))|(~(cPSI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ X37)&(![X6:a]:(((X4 @ X6)=>(X4 @ (cL @ X6)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X38)|((esk1_0)!=(cP @ X37 @ X38))))&(((esk1_0)!=(cP @ X39 @ X40))|~(cPHI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ X39)&(![X9:a]:(((X4 @ X9)=>(X4 @ (cL @ X9)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X40)|(~(cPSI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ X37)&(![X6:a]:(((X4 @ X6)=>(X4 @ (cL @ X6)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X38)|((esk1_0)!=(cP @ X37 @ X38)))))&(((esk1_0)!=(cZ))|(~(cPSI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ X37)&(![X6:a]:(((X4 @ X6)=>(X4 @ (cL @ X6)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X38)|((esk1_0)!=(cP @ X37 @ X38)))))&(((esk1_0)!=(cP @ X41 @ X42))|~(cPSI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ X41)&(![X9:a]:(((X4 @ X9)=>(X4 @ (cL @ X9)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X42)|(~(cPSI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ X37)&(![X6:a]:(((X4 @ X6)=>(X4 @ (cL @ X6)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X38)|((esk1_0)!=(cP @ X37 @ X38)))))))&((((((esk1_0)=(cP @ esk6_0 @ esk7_0))|(((esk1_0)=(cP @ esk4_0 @ esk5_0))|((esk1_0)=(cZ))|((esk1_0)=(cZ)))|(((esk1_0)=(cP @ esk2_0 @ esk3_0))|((esk1_0)=(cZ))))&((cPSI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ esk6_0)&(![X9:a]:(((X4 @ X9)=>(X4 @ (cL @ X9)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ esk7_0)|(((esk1_0)=(cP @ esk4_0 @ esk5_0))|((esk1_0)=(cZ))|((esk1_0)=(cZ)))|(((esk1_0)=(cP @ esk2_0 @ esk3_0))|((esk1_0)=(cZ)))))&((((esk1_0)=(cP @ esk6_0 @ esk7_0))|((cPHI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ esk4_0)&(![X9:a]:(((X4 @ X9)=>(X4 @ (cL @ X9)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ esk5_0)|((esk1_0)=(cZ))|((esk1_0)=(cZ)))|(((esk1_0)=(cP @ esk2_0 @ esk3_0))|((esk1_0)=(cZ))))&((cPSI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ esk6_0)&(![X9:a]:(((X4 @ X9)=>(X4 @ (cL @ X9)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ esk7_0)|((cPHI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ esk4_0)&(![X9:a]:(((X4 @ X9)=>(X4 @ (cL @ X9)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ esk5_0)|((esk1_0)=(cZ))|((esk1_0)=(cZ)))|(((esk1_0)=(cP @ esk2_0 @ esk3_0))|((esk1_0)=(cZ))))))&(((((esk1_0)=(cP @ esk6_0 @ esk7_0))|(((esk1_0)=(cP @ esk4_0 @ esk5_0))|((esk1_0)=(cZ))|((esk1_0)=(cZ)))|((cPHI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ esk2_0)&(![X6:a]:(((X4 @ X6)=>(X4 @ (cL @ X6)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ esk2_0)&(![X6:a]:(((X4 @ X6)=>(X4 @ (cL @ X6)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ esk3_0)|((esk1_0)=(cZ))))&((cPSI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ esk6_0)&(![X9:a]:(((X4 @ X9)=>(X4 @ (cL @ X9)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ esk7_0)|(((esk1_0)=(cP @ esk4_0 @ esk5_0))|((esk1_0)=(cZ))|((esk1_0)=(cZ)))|((cPHI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ esk2_0)&(![X6:a]:(((X4 @ X6)=>(X4 @ (cL @ X6)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ esk2_0)&(![X6:a]:(((X4 @ X6)=>(X4 @ (cL @ X6)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ esk3_0)|((esk1_0)=(cZ)))))&((((esk1_0)=(cP @ esk6_0 @ esk7_0))|((cPHI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ esk4_0)&(![X9:a]:(((X4 @ X9)=>(X4 @ (cL @ X9)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ esk5_0)|((esk1_0)=(cZ))|((esk1_0)=(cZ)))|((cPHI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ esk2_0)&(![X6:a]:(((X4 @ X6)=>(X4 @ (cL @ X6)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ esk2_0)&(![X6:a]:(((X4 @ X6)=>(X4 @ (cL @ X6)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ esk3_0)|((esk1_0)=(cZ))))&((cPSI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ esk6_0)&(![X9:a]:(((X4 @ X9)=>(X4 @ (cL @ X9)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ esk7_0)|((cPHI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ esk4_0)&(![X9:a]:(((X4 @ X9)=>(X4 @ (cL @ X9)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ esk5_0)|((esk1_0)=(cZ))|((esk1_0)=(cZ)))|((cPHI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ esk2_0)&(![X6:a]:(((X4 @ X6)=>(X4 @ (cL @ X6)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X4:a > $o]:(((((X4 @ esk2_0)&(![X6:a]:(((X4 @ X6)=>(X4 @ (cL @ X6)))))))=>(?[X10:a]:(((X4 @ X10)&(((cR @ X10)=(Z0)))))))))) @ esk3_0)|((esk1_0)=(cZ)))))))))), 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_3])])])])])])).
% 0.25/0.31 thf(c_0_5, negated_conjecture, ((cPSI @ (^[Z0:a]:(![X168:a > $o]:((((((X168 @ esk6_0))&(![X169:a]:((((X168 @ X169))=>((X168 @ (cL @ X169))))))))=>(?[X170:a]:((((X168 @ X170))&(((cR @ X170)=(Z0)))))))))) @ esk7_0)|((esk1_0)=(cP @ esk4_0 @ esk5_0))|((esk1_0)=(cZ))|((esk1_0)=(cZ))|((esk1_0)=(cP @ esk2_0 @ esk3_0))|((esk1_0)=(cZ))), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.25/0.31 thf(c_0_6, negated_conjecture, (((esk1_0)!=(cZ))|((esk1_0)!=(cZ))), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.25/0.31 thf(c_0_7, negated_conjecture, (((esk1_0)=(cP @ esk6_0 @ esk7_0))|((esk1_0)=(cP @ esk4_0 @ esk5_0))|((esk1_0)=(cZ))|((esk1_0)=(cZ))|((esk1_0)=(cP @ esk2_0 @ esk3_0))|((esk1_0)=(cZ))), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.25/0.31 thf(c_0_8, negated_conjecture, ((cPSI @ (^[Z0:a]:(![X171:a > $o]:((((((X171 @ esk6_0))&(![X172:a]:((((X171 @ X172))=>((X171 @ (cL @ X172))))))))=>(?[X173:a]:((((X171 @ X173))&(((cR @ X173)=(Z0)))))))))) @ esk7_0)|(cPHI @ (^[Z0:a]:(![X174:a > $o]:((((((X174 @ esk4_0))&(![X175:a]:((((X174 @ X175))=>((X174 @ (cL @ X175))))))))=>(?[X176:a]:((((X174 @ X176))&(((cR @ X176)=(Z0)))))))))) @ esk5_0)|((esk1_0)=(cZ))|((esk1_0)=(cZ))|((esk1_0)=(cP @ esk2_0 @ esk3_0))|((esk1_0)=(cZ))), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.25/0.31 thf(c_0_9, negated_conjecture, ![X1:a, X2:a, X6:a, X9:a]:((((esk1_0)!=(cP @ X1 @ X2))|~((cPSI @ (^[Z0:a]:(![X177:a > $o]:((((((X177 @ X1))&(![X178:a]:((((X177 @ X178))=>((X177 @ (cL @ X178))))))))=>(?[X179:a]:((((X177 @ X179))&(((cR @ X179)=(Z0)))))))))) @ X2))|~((cPSI @ (^[Z0:a]:(![X180:a > $o]:((((((X180 @ X6))&(![X181:a]:((((X180 @ X181))=>((X180 @ (cL @ X181))))))))=>(?[X182:a]:((((X180 @ X182))&(((cR @ X182)=(Z0)))))))))) @ X9))|((esk1_0)!=(cP @ X6 @ X9)))), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.25/0.31 thf(c_0_10, negated_conjecture, (((esk1_0)=(cZ))|((esk1_0)=(cP @ esk2_0 @ esk3_0))|((esk1_0)=(cP @ esk4_0 @ esk5_0))|(cPSI @ (^[Z0:a]:(![X183:a > $o]:((((((X183 @ esk6_0))&(![X184:a]:((((X183 @ X184))=>((X183 @ (cL @ X184))))))))=>(?[X185:a]:((((X183 @ X185))&(((cR @ X185)=(Z0)))))))))) @ esk7_0)), inference(cn,[status(thm)],[c_0_5])).
% 0.25/0.31 thf(c_0_11, negated_conjecture, ((esk1_0)!=(cZ)), inference(cn,[status(thm)],[c_0_6])).
% 0.25/0.31 thf(c_0_12, negated_conjecture, (((esk1_0)=(cZ))|((esk1_0)=(cP @ esk2_0 @ esk3_0))|((esk1_0)=(cP @ esk4_0 @ esk5_0))|((esk1_0)=(cP @ esk6_0 @ esk7_0))), inference(cn,[status(thm)],[c_0_7])).
% 0.25/0.31 thf(c_0_13, negated_conjecture, (((esk1_0)=(cP @ esk6_0 @ esk7_0))|(cPHI @ (^[Z0:a]:(![X186:a > $o]:((((((X186 @ esk4_0))&(![X187:a]:((((X186 @ X187))=>((X186 @ (cL @ X187))))))))=>(?[X188:a]:((((X186 @ X188))&(((cR @ X188)=(Z0)))))))))) @ esk5_0)|((esk1_0)=(cZ))|((esk1_0)=(cZ))|((esk1_0)=(cP @ esk2_0 @ esk3_0))|((esk1_0)=(cZ))), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.25/0.31 thf(c_0_14, negated_conjecture, (((esk1_0)=(cP @ esk6_0 @ esk7_0))|(cPHI @ (^[Z0:a]:(![X189:a > $o]:((((((X189 @ esk4_0))&(![X190:a]:((((X189 @ X190))=>((X189 @ (cL @ X190))))))))=>(?[X191:a]:((((X189 @ X191))&(((cR @ X191)=(Z0)))))))))) @ esk5_0)|((esk1_0)=(cZ))|((esk1_0)=(cZ))|(cPHI @ (^[Z0:a]:(![X192:a > $o]:((((((X192 @ esk2_0))&(![X193:a]:((((X192 @ X193))=>((X192 @ (cL @ X193))))))))=>(?[X194:a]:((((X192 @ X194))&(((cR @ X194)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X195:a > $o]:((((((X195 @ esk2_0))&(![X196:a]:((((X195 @ X196))=>((X195 @ (cL @ X196))))))))=>(?[X197:a]:((((X195 @ X197))&(((cR @ X197)=(Z0)))))))))) @ esk3_0)|((esk1_0)=(cZ))), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.25/0.31 thf(c_0_15, negated_conjecture, (((esk1_0)=(cP @ esk6_0 @ esk7_0))|((esk1_0)=(cP @ esk4_0 @ esk5_0))|((esk1_0)=(cZ))|((esk1_0)=(cZ))|(cPHI @ (^[Z0:a]:(![X198:a > $o]:((((((X198 @ esk2_0))&(![X199:a]:((((X198 @ X199))=>((X198 @ (cL @ X199))))))))=>(?[X200:a]:((((X198 @ X200))&(((cR @ X200)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X201:a > $o]:((((((X201 @ esk2_0))&(![X202:a]:((((X201 @ X202))=>((X201 @ (cL @ X202))))))))=>(?[X203:a]:((((X201 @ X203))&(((cR @ X203)=(Z0)))))))))) @ esk3_0)|((esk1_0)=(cZ))), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.25/0.31 thf(c_0_16, negated_conjecture, ![X1:a, X2:a, X6:a, X9:a]:((((esk1_0)!=(cP @ X1 @ X2))|~((cPHI @ (^[Z0:a]:(![X204:a > $o]:((((((X204 @ X1))&(![X205:a]:((((X204 @ X205))=>((X204 @ (cL @ X205))))))))=>(?[X206:a]:((((X204 @ X206))&(((cR @ X206)=(Z0)))))))))) @ X2))|~((cPHI @ (^[Z0:a]:(![X207:a > $o]:((((((X207 @ X6))&(![X208:a]:((((X207 @ X208))=>((X207 @ (cL @ X208))))))))=>(?[X209:a]:((((X207 @ X209))&(((cR @ X209)=(Z0)))))))))) @ X9))|((esk1_0)!=(cP @ X6 @ X9)))), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.25/0.31 thf(c_0_17, negated_conjecture, (((esk1_0)=(cZ))|((esk1_0)=(cP @ esk2_0 @ esk3_0))|(cPSI @ (^[Z0:a]:(![X210:a > $o]:((((((X210 @ esk6_0))&(![X211:a]:((((X210 @ X211))=>((X210 @ (cL @ X211))))))))=>(?[X212:a]:((((X210 @ X212))&(((cR @ X212)=(Z0)))))))))) @ esk7_0)|(cPHI @ (^[Z0:a]:(![X213:a > $o]:((((((X213 @ esk4_0))&(![X214:a]:((((X213 @ X214))=>((X213 @ (cL @ X214))))))))=>(?[X215:a]:((((X213 @ X215))&(((cR @ X215)=(Z0)))))))))) @ esk5_0)), inference(cn,[status(thm)],[c_0_8])).
% 0.25/0.31 thf(c_0_18, negated_conjecture, ![X1:a, X2:a]:((((cP @ X1 @ X2)!=(esk1_0))|~((cPSI @ (^[Z0:a]:(![X216:a > $o]:((((((X216 @ X1))&(![X217:a]:((((X216 @ X217))=>((X216 @ (cL @ X217))))))))=>(?[X218:a]:((((X216 @ X218))&(((cR @ X218)=(Z0)))))))))) @ X2)))), inference(condense,[status(thm)],[c_0_9])).
% 0.25/0.31 thf(c_0_19, negated_conjecture, (((cP @ esk4_0 @ esk5_0)=(esk1_0))|((cP @ esk2_0 @ esk3_0)=(esk1_0))|(cPSI @ (^[Z0:a]:(![X219:a > $o]:((((((X219 @ esk6_0))&(![X220:a]:((((X219 @ X220))=>((X219 @ (cL @ X220))))))))=>(?[X221:a]:((((X219 @ X221))&(((cR @ X221)=(Z0)))))))))) @ esk7_0)), inference(sr,[status(thm)],[c_0_10, c_0_11])).
% 0.25/0.31 thf(c_0_20, negated_conjecture, (((cP @ esk6_0 @ esk7_0)=(esk1_0))|((cP @ esk4_0 @ esk5_0)=(esk1_0))|((cP @ esk2_0 @ esk3_0)=(esk1_0))), inference(sr,[status(thm)],[c_0_12, c_0_11])).
% 0.25/0.31 thf(c_0_21, negated_conjecture, (((esk1_0)=(cZ))|((esk1_0)=(cP @ esk2_0 @ esk3_0))|((esk1_0)=(cP @ esk6_0 @ esk7_0))|(cPHI @ (^[Z0:a]:(![X222:a > $o]:((((((X222 @ esk4_0))&(![X223:a]:((((X222 @ X223))=>((X222 @ (cL @ X223))))))))=>(?[X224:a]:((((X222 @ X224))&(((cR @ X224)=(Z0)))))))))) @ esk5_0)), inference(cn,[status(thm)],[c_0_13])).
% 0.25/0.31 thf(c_0_22, negated_conjecture, (((esk1_0)=(cZ))|((esk1_0)=(cP @ esk6_0 @ esk7_0))|(cPSI @ (^[Z0:a]:(![X225:a > $o]:((((((X225 @ esk2_0))&(![X226:a]:((((X225 @ X226))=>((X225 @ (cL @ X226))))))))=>(?[X227:a]:((((X225 @ X227))&(((cR @ X227)=(Z0)))))))))) @ esk3_0)|(cPHI @ (^[Z0:a]:(![X228:a > $o]:((((((X228 @ esk2_0))&(![X229:a]:((((X228 @ X229))=>((X228 @ (cL @ X229))))))))=>(?[X230:a]:((((X228 @ X230))&(((cR @ X230)=(Z0)))))))))) @ esk3_0)|(cPHI @ (^[Z0:a]:(![X231:a > $o]:((((((X231 @ esk4_0))&(![X232:a]:((((X231 @ X232))=>((X231 @ (cL @ X232))))))))=>(?[X233:a]:((((X231 @ X233))&(((cR @ X233)=(Z0)))))))))) @ esk5_0)), inference(cn,[status(thm)],[c_0_14])).
% 0.25/0.31 thf(c_0_23, negated_conjecture, (((esk1_0)=(cZ))|((esk1_0)=(cP @ esk4_0 @ esk5_0))|((esk1_0)=(cP @ esk6_0 @ esk7_0))|(cPSI @ (^[Z0:a]:(![X234:a > $o]:((((((X234 @ esk2_0))&(![X235:a]:((((X234 @ X235))=>((X234 @ (cL @ X235))))))))=>(?[X236:a]:((((X234 @ X236))&(((cR @ X236)=(Z0)))))))))) @ esk3_0)|(cPHI @ (^[Z0:a]:(![X237:a > $o]:((((((X237 @ esk2_0))&(![X238:a]:((((X237 @ X238))=>((X237 @ (cL @ X238))))))))=>(?[X239:a]:((((X237 @ X239))&(((cR @ X239)=(Z0)))))))))) @ esk3_0)), inference(cn,[status(thm)],[c_0_15])).
% 0.25/0.31 thf(c_0_24, negated_conjecture, ![X1:a, X2:a]:((((cP @ X1 @ X2)!=(esk1_0))|~((cPHI @ (^[Z0:a]:(![X240:a > $o]:((((((X240 @ X1))&(![X241:a]:((((X240 @ X241))=>((X240 @ (cL @ X241))))))))=>(?[X242:a]:((((X240 @ X242))&(((cR @ X242)=(Z0)))))))))) @ X2)))), inference(condense,[status(thm)],[c_0_16])).
% 0.25/0.31 thf(c_0_25, negated_conjecture, (((cP @ esk2_0 @ esk3_0)=(esk1_0))|(cPHI @ (^[Z0:a]:(![X243:a > $o]:((((((X243 @ esk4_0))&(![X244:a]:((((X243 @ X244))=>((X243 @ (cL @ X244))))))))=>(?[X245:a]:((((X243 @ X245))&(((cR @ X245)=(Z0)))))))))) @ esk5_0)|(cPSI @ (^[Z0:a]:(![X246:a > $o]:((((((X246 @ esk6_0))&(![X247:a]:((((X246 @ X247))=>((X246 @ (cL @ X247))))))))=>(?[X248:a]:((((X246 @ X248))&(((cR @ X248)=(Z0)))))))))) @ esk7_0)), inference(sr,[status(thm)],[c_0_17, c_0_11])).
% 0.25/0.31 thf(c_0_26, negated_conjecture, (((cP @ esk2_0 @ esk3_0)=(esk1_0))|((cP @ esk4_0 @ esk5_0)=(esk1_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_18, c_0_19]), c_0_20])).
% 0.25/0.31 thf(c_0_27, negated_conjecture, (((cP @ esk6_0 @ esk7_0)=(esk1_0))|((cP @ esk2_0 @ esk3_0)=(esk1_0))|(cPHI @ (^[Z0:a]:(![X249:a > $o]:((((((X249 @ esk4_0))&(![X250:a]:((((X249 @ X250))=>((X249 @ (cL @ X250))))))))=>(?[X251:a]:((((X249 @ X251))&(((cR @ X251)=(Z0)))))))))) @ esk5_0)), inference(sr,[status(thm)],[c_0_21, c_0_11])).
% 0.25/0.31 thf(c_0_28, plain, ((epred1_0)=>(((((((((cL @ cZ)=(cZ))&((cR @ cZ)=(cZ)))&![X1:a, X2:a]:(((cL @ (cP @ X1 @ X2))=(X1))))&![X1:a, X2:a]:(((cR @ (cP @ X1 @ X2))=(X2))))&![X3:a]:((((X3)!=(cZ))<=>((X3)=(cP @ (cL @ X3) @ (cR @ X3))))))&![X4:a > $o]:((?[X3:a]:(((X4 @ X3)&![X5:a]:(((X4 @ X5)=>(X4 @ (cL @ X5))))))=>(X4 @ cZ))))&![X4:a > $o, X6:a]:(((cPHI @ X4 @ X6)<=>?[X1:a]:((![X7:a]:((![X8:a > $o]:((((X8 @ X1)&![X9:a]:(((X8 @ X9)=>(X8 @ (cL @ X9)))))=>?[X10:a]:(((X8 @ X10)&((cR @ X10)=(X7))))))=>(X4 @ X7)))&(cPHI @ (^[Z0:a]:(![X8:a > $o]:(((((X8 @ X1)&(![X9:a]:(((X8 @ X9)=>(X8 @ (cL @ X9)))))))=>(?[X10:a]:(((X8 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X6))))))&![X4:a > $o, X6:a]:(((cPSI @ X4 @ X6)<=>?[X1:a]:((![X11:a]:((![X8:a > $o]:((((X8 @ X1)&![X9:a]:(((X8 @ X9)=>(X8 @ (cL @ X9)))))=>?[X10:a]:(((X8 @ X10)&((cR @ X10)=(X11))))))=>(X4 @ X11)))&(cPSI @ (^[Z0:a]:(![X8:a > $o]:(((((X8 @ X1)&(![X9:a]:(((X8 @ X9)=>(X8 @ (cL @ X9)))))))=>(?[X10:a]:(((X8 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X6))))))), inference(split_equiv,[status(thm)],[c_0_2])).
% 0.25/0.31 thf(c_0_29, negated_conjecture, (((cP @ esk6_0 @ esk7_0)=(esk1_0))|(cPHI @ (^[Z0:a]:(![X252:a > $o]:((((((X252 @ esk4_0))&(![X253:a]:((((X252 @ X253))=>((X252 @ (cL @ X253))))))))=>(?[X254:a]:((((X252 @ X254))&(((cR @ X254)=(Z0)))))))))) @ esk5_0)|(cPHI @ (^[Z0:a]:(![X255:a > $o]:((((((X255 @ esk2_0))&(![X256:a]:((((X255 @ X256))=>((X255 @ (cL @ X256))))))))=>(?[X257:a]:((((X255 @ X257))&(((cR @ X257)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X258:a > $o]:((((((X258 @ esk2_0))&(![X259:a]:((((X258 @ X259))=>((X258 @ (cL @ X259))))))))=>(?[X260:a]:((((X258 @ X260))&(((cR @ X260)=(Z0)))))))))) @ esk3_0)), inference(sr,[status(thm)],[c_0_22, c_0_11])).
% 0.25/0.31 thf(c_0_30, negated_conjecture, (((cP @ esk6_0 @ esk7_0)=(esk1_0))|((cP @ esk4_0 @ esk5_0)=(esk1_0))|(cPHI @ (^[Z0:a]:(![X261:a > $o]:((((((X261 @ esk2_0))&(![X262:a]:((((X261 @ X262))=>((X261 @ (cL @ X262))))))))=>(?[X263:a]:((((X261 @ X263))&(((cR @ X263)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X264:a > $o]:((((((X264 @ esk2_0))&(![X265:a]:((((X264 @ X265))=>((X264 @ (cL @ X265))))))))=>(?[X266:a]:((((X264 @ X266))&(((cR @ X266)=(Z0)))))))))) @ esk3_0)), inference(sr,[status(thm)],[c_0_23, c_0_11])).
% 0.25/0.31 thf(c_0_31, negated_conjecture, (((cP @ esk2_0 @ esk3_0)=(esk1_0))|(cPSI @ (^[Z0:a]:(![X267:a > $o]:((((((X267 @ esk6_0))&(![X268:a]:((((X267 @ X268))=>((X267 @ (cL @ X268))))))))=>(?[X269:a]:((((X267 @ X269))&(((cR @ X269)=(Z0)))))))))) @ esk7_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_24, c_0_25]), c_0_26])).
% 0.25/0.31 thf(c_0_32, negated_conjecture, (((cP @ esk2_0 @ esk3_0)=(esk1_0))|((cP @ esk6_0 @ esk7_0)=(esk1_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_24, c_0_27]), c_0_26])).
% 0.25/0.31 thf(c_0_33, plain, ![X49:a, X50:a, X51:a, X52:a, X53:a, X54:a > $o, X55:a, X57:a > $o, X58:a, X60:a, X62:a, X63:a, X64:a > $o, X65:a, X66:a, X68:a > $o, X71:a > $o, X72:a, X74:a, X76:a, X77:a, X78:a > $o, X79:a, X80:a, X82:a > $o]:(((((((((((cL @ cZ)=(cZ))|~(epred1_0))&(((cR @ cZ)=(cZ))|~(epred1_0)))&(((cL @ (cP @ X49 @ X50))=(X49))|~(epred1_0)))&(((cR @ (cP @ X51 @ X52))=(X52))|~(epred1_0)))&((((X53)=(cZ))|((X53)=(cP @ (cL @ X53) @ (cR @ X53)))|~(epred1_0))&(((X53)!=(cP @ (cL @ X53) @ (cR @ X53)))|((X53)!=(cZ))|~(epred1_0))))&(((X54 @ (esk8_1 @ X54))|~(X54 @ X55)|(X54 @ cZ)|~(epred1_0))&(~(X54 @ (cL @ (esk8_1 @ X54)))|~(X54 @ X55)|(X54 @ cZ)|~(epred1_0))))&((((((epred2_3 @ X57 @ X58 @ X60 @ (esk9_2 @ X57 @ X58))|(X57 @ X60)|~(cPHI @ X57 @ X58)|~(epred1_0))&(~(epred2_3 @ X57 @ X58 @ X60 @ X62)|(epred2_3 @ X57 @ X58 @ X60 @ (cL @ X62))|(X57 @ X60)|~(cPHI @ X57 @ X58)|~(epred1_0)))&(~(epred2_3 @ X57 @ X58 @ X60 @ X63)|((cR @ X63)!=(X60))|(X57 @ X60)|~(cPHI @ X57 @ X58)|~(epred1_0)))&((cPHI @ (^[Z0:a]:(![X8:a > $o]:(((((X8 @ (esk9_2 @ X57 @ X58))&(![X9:a]:(((X8 @ X9)=>(X8 @ (cL @ X9)))))))=>(?[X10:a]:(((X8 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X58)|~(cPHI @ X57 @ X58)|~(epred1_0)))&(((((X68 @ (esk12_4 @ X64 @ X65 @ X66 @ X68))|((X68 @ (esk11_4 @ X64 @ X65 @ X66 @ X68))|~(X68 @ X66))|~(cPHI @ (^[Z0:a]:(![X8:a > $o]:(((((X8 @ X66)&(![X9:a]:(((X8 @ X9)=>(X8 @ (cL @ X9)))))))=>(?[X10:a]:(((X8 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X65)|(cPHI @ X64 @ X65)|~(epred1_0))&(((cR @ (esk12_4 @ X64 @ X65 @ X66 @ X68))=(esk10_3 @ X64 @ X65 @ X66))|((X68 @ (esk11_4 @ X64 @ X65 @ X66 @ X68))|~(X68 @ X66))|~(cPHI @ (^[Z0:a]:(![X8:a > $o]:(((((X8 @ X66)&(![X9:a]:(((X8 @ X9)=>(X8 @ (cL @ X9)))))))=>(?[X10:a]:(((X8 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X65)|(cPHI @ X64 @ X65)|~(epred1_0)))&(((X68 @ (esk12_4 @ X64 @ X65 @ X66 @ X68))|(~(X68 @ (cL @ (esk11_4 @ X64 @ X65 @ X66 @ X68)))|~(X68 @ X66))|~(cPHI @ (^[Z0:a]:(![X8:a > $o]:(((((X8 @ X66)&(![X9:a]:(((X8 @ X9)=>(X8 @ (cL @ X9)))))))=>(?[X10:a]:(((X8 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X65)|(cPHI @ X64 @ X65)|~(epred1_0))&(((cR @ (esk12_4 @ X64 @ X65 @ X66 @ X68))=(esk10_3 @ X64 @ X65 @ X66))|(~(X68 @ (cL @ (esk11_4 @ X64 @ X65 @ X66 @ X68)))|~(X68 @ X66))|~(cPHI @ (^[Z0:a]:(![X8:a > $o]:(((((X8 @ X66)&(![X9:a]:(((X8 @ X9)=>(X8 @ (cL @ X9)))))))=>(?[X10:a]:(((X8 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X65)|(cPHI @ X64 @ X65)|~(epred1_0))))&(~(X64 @ (esk10_3 @ X64 @ X65 @ X66))|~(cPHI @ (^[Z0:a]:(![X8:a > $o]:(((((X8 @ X66)&(![X9:a]:(((X8 @ X9)=>(X8 @ (cL @ X9)))))))=>(?[X10:a]:(((X8 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X65)|(cPHI @ X64 @ X65)|~(epred1_0)))))&((((((epred3_3 @ X71 @ X72 @ X74 @ (esk13_2 @ X71 @ X72))|(X71 @ X74)|~(cPSI @ X71 @ X72)|~(epred1_0))&(~(epred3_3 @ X71 @ X72 @ X74 @ X76)|(epred3_3 @ X71 @ X72 @ X74 @ (cL @ X76))|(X71 @ X74)|~(cPSI @ X71 @ X72)|~(epred1_0)))&(~(epred3_3 @ X71 @ X72 @ X74 @ X77)|((cR @ X77)!=(X74))|(X71 @ X74)|~(cPSI @ X71 @ X72)|~(epred1_0)))&((cPSI @ (^[Z0:a]:(![X8:a > $o]:(((((X8 @ (esk13_2 @ X71 @ X72))&(![X9:a]:(((X8 @ X9)=>(X8 @ (cL @ X9)))))))=>(?[X10:a]:(((X8 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X72)|~(cPSI @ X71 @ X72)|~(epred1_0)))&(((((X82 @ (esk16_4 @ X78 @ X79 @ X80 @ X82))|((X82 @ (esk15_4 @ X78 @ X79 @ X80 @ X82))|~(X82 @ X80))|~(cPSI @ (^[Z0:a]:(![X8:a > $o]:(((((X8 @ X80)&(![X9:a]:(((X8 @ X9)=>(X8 @ (cL @ X9)))))))=>(?[X10:a]:(((X8 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X79)|(cPSI @ X78 @ X79)|~(epred1_0))&(((cR @ (esk16_4 @ X78 @ X79 @ X80 @ X82))=(esk14_3 @ X78 @ X79 @ X80))|((X82 @ (esk15_4 @ X78 @ X79 @ X80 @ X82))|~(X82 @ X80))|~(cPSI @ (^[Z0:a]:(![X8:a > $o]:(((((X8 @ X80)&(![X9:a]:(((X8 @ X9)=>(X8 @ (cL @ X9)))))))=>(?[X10:a]:(((X8 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X79)|(cPSI @ X78 @ X79)|~(epred1_0)))&(((X82 @ (esk16_4 @ X78 @ X79 @ X80 @ X82))|(~(X82 @ (cL @ (esk15_4 @ X78 @ X79 @ X80 @ X82)))|~(X82 @ X80))|~(cPSI @ (^[Z0:a]:(![X8:a > $o]:(((((X8 @ X80)&(![X9:a]:(((X8 @ X9)=>(X8 @ (cL @ X9)))))))=>(?[X10:a]:(((X8 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X79)|(cPSI @ X78 @ X79)|~(epred1_0))&(((cR @ (esk16_4 @ X78 @ X79 @ X80 @ X82))=(esk14_3 @ X78 @ X79 @ X80))|(~(X82 @ (cL @ (esk15_4 @ X78 @ X79 @ X80 @ X82)))|~(X82 @ X80))|~(cPSI @ (^[Z0:a]:(![X8:a > $o]:(((((X8 @ X80)&(![X9:a]:(((X8 @ X9)=>(X8 @ (cL @ X9)))))))=>(?[X10:a]:(((X8 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X79)|(cPSI @ X78 @ X79)|~(epred1_0))))&(~(X78 @ (esk14_3 @ X78 @ X79 @ X80))|~(cPSI @ (^[Z0:a]:(![X8:a > $o]:(((((X8 @ X80)&(![X9:a]:(((X8 @ X9)=>(X8 @ (cL @ X9)))))))=>(?[X10:a]:(((X8 @ X10)&(((cR @ X10)=(Z0)))))))))) @ X79)|(cPSI @ X78 @ X79)|~(epred1_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(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_28])])])])])])])).
% 0.25/0.31 thf(c_0_34, negated_conjecture, (((cP @ esk6_0 @ esk7_0)=(esk1_0))|(cPSI @ (^[Z0:a]:(![X270:a > $o]:((((((X270 @ esk2_0))&(![X271:a]:((((X270 @ X271))=>((X270 @ (cL @ X271))))))))=>(?[X272:a]:((((X270 @ X272))&(((cR @ X272)=(Z0)))))))))) @ esk3_0)|(cPHI @ (^[Z0:a]:(![X273:a > $o]:((((((X273 @ esk2_0))&(![X274:a]:((((X273 @ X274))=>((X273 @ (cL @ X274))))))))=>(?[X275:a]:((((X273 @ X275))&(((cR @ X275)=(Z0)))))))))) @ esk3_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_24, c_0_29]), c_0_30])).
% 0.25/0.31 thf(c_0_35, negated_conjecture, ((cP @ esk2_0 @ esk3_0)=(esk1_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_18, c_0_31]), c_0_32])).
% 0.25/0.31 thf(c_0_36, plain, ![X1:a, X2:a]:((((cR @ (cP @ X1 @ X2))=(X2))|~((epred1_0)))), inference(split_conjunct,[status(thm)],[c_0_33])).
% 0.25/0.31 thf(c_0_37, negated_conjecture, (epred1_0), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.25/0.31 thf(c_0_38, negated_conjecture, ((cPSI @ (^[Z0:a]:(![X276:a > $o]:((((((X276 @ esk6_0))&(![X277:a]:((((X276 @ X277))=>((X276 @ (cL @ X277))))))))=>(?[X278:a]:((((X276 @ X278))&(((cR @ X278)=(Z0)))))))))) @ esk7_0)|((esk1_0)=(cP @ esk4_0 @ esk5_0))|((esk1_0)=(cZ))|((esk1_0)=(cZ))|(cPHI @ (^[Z0:a]:(![X279:a > $o]:((((((X279 @ esk2_0))&(![X280:a]:((((X279 @ X280))=>((X279 @ (cL @ X280))))))))=>(?[X281:a]:((((X279 @ X281))&(((cR @ X281)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X282:a > $o]:((((((X282 @ esk2_0))&(![X283:a]:((((X282 @ X283))=>((X282 @ (cL @ X283))))))))=>(?[X284:a]:((((X282 @ X284))&(((cR @ X284)=(Z0)))))))))) @ esk3_0)|((esk1_0)=(cZ))), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.25/0.31 thf(c_0_39, negated_conjecture, (((cP @ esk6_0 @ esk7_0)=(esk1_0))|(cPSI @ (^[Z0:a]:(![X285:a > $o]:((((((X285 @ esk2_0))&(![X286:a]:((((X285 @ X286))=>((X285 @ (cL @ X286))))))))=>(?[X287:a]:((((X285 @ X287))&(((cR @ X287)=(Z0)))))))))) @ esk3_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_24, c_0_34]), c_0_35])])).
% 0.25/0.31 thf(c_0_40, plain, ![X1:a, X2:a]:(((cR @ (cP @ X1 @ X2))=(X2))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_36, c_0_37])])).
% 0.25/0.31 thf(c_0_41, negated_conjecture, (((esk1_0)=(cZ))|((esk1_0)=(cP @ esk4_0 @ esk5_0))|(cPSI @ (^[Z0:a]:(![X288:a > $o]:((((((X288 @ esk2_0))&(![X289:a]:((((X288 @ X289))=>((X288 @ (cL @ X289))))))))=>(?[X290:a]:((((X288 @ X290))&(((cR @ X290)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X291:a > $o]:((((((X291 @ esk6_0))&(![X292:a]:((((X291 @ X292))=>((X291 @ (cL @ X292))))))))=>(?[X293:a]:((((X291 @ X293))&(((cR @ X293)=(Z0)))))))))) @ esk7_0)|(cPHI @ (^[Z0:a]:(![X294:a > $o]:((((((X294 @ esk2_0))&(![X295:a]:((((X294 @ X295))=>((X294 @ (cL @ X295))))))))=>(?[X296:a]:((((X294 @ X296))&(((cR @ X296)=(Z0)))))))))) @ esk3_0)), inference(cn,[status(thm)],[c_0_38])).
% 0.25/0.31 thf(c_0_42, negated_conjecture, ((cP @ esk6_0 @ esk7_0)=(esk1_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_18, c_0_39]), c_0_35])])).
% 0.25/0.31 thf(c_0_43, plain, ((cR @ esk1_0)=(esk3_0)), inference(spm,[status(thm)],[c_0_40, c_0_35])).
% 0.25/0.31 thf(c_0_44, plain, ![X2:a, X1:a]:((((cL @ (cP @ X1 @ X2))=(X1))|~((epred1_0)))), inference(split_conjunct,[status(thm)],[c_0_33])).
% 0.25/0.31 thf(c_0_45, negated_conjecture, (((cP @ esk4_0 @ esk5_0)=(esk1_0))|(cPHI @ (^[Z0:a]:(![X297:a > $o]:((((((X297 @ esk2_0))&(![X298:a]:((((X297 @ X298))=>((X297 @ (cL @ X298))))))))=>(?[X299:a]:((((X297 @ X299))&(((cR @ X299)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X300:a > $o]:((((((X300 @ esk6_0))&(![X301:a]:((((X300 @ X301))=>((X300 @ (cL @ X301))))))))=>(?[X302:a]:((((X300 @ X302))&(((cR @ X302)=(Z0)))))))))) @ esk7_0)|(cPSI @ (^[Z0:a]:(![X303:a > $o]:((((((X303 @ esk2_0))&(![X304:a]:((((X303 @ X304))=>((X303 @ (cL @ X304))))))))=>(?[X305:a]:((((X303 @ X305))&(((cR @ X305)=(Z0)))))))))) @ esk3_0)), inference(sr,[status(thm)],[c_0_41, c_0_11])).
% 0.25/0.31 thf(c_0_46, plain, ((esk7_0)=(esk3_0)), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_40, c_0_42]), c_0_43])).
% 0.25/0.31 thf(c_0_47, plain, ![X2:a, X1:a]:(((cL @ (cP @ X1 @ X2))=(X1))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_44, c_0_37])])).
% 0.25/0.31 thf(c_0_48, negated_conjecture, (((cP @ esk4_0 @ esk5_0)=(esk1_0))|(cPSI @ (^[Z0:a]:(![X306:a > $o]:((((((X306 @ esk2_0))&(![X307:a]:((((X306 @ X307))=>((X306 @ (cL @ X307))))))))=>(?[X308:a]:((((X306 @ X308))&(((cR @ X308)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X309:a > $o]:((((((X309 @ esk6_0))&(![X310:a]:((((X309 @ X310))=>((X309 @ (cL @ X310))))))))=>(?[X311:a]:((((X309 @ X311))&(((cR @ X311)=(Z0)))))))))) @ esk3_0)|(cPHI @ (^[Z0:a]:(![X312:a > $o]:((((((X312 @ esk2_0))&(![X313:a]:((((X312 @ X313))=>((X312 @ (cL @ X313))))))))=>(?[X314:a]:((((X312 @ X314))&(((cR @ X314)=(Z0)))))))))) @ esk3_0)), inference(rw,[status(thm)],[c_0_45, c_0_46])).
% 0.25/0.31 thf(c_0_49, negated_conjecture, ((cP @ esk6_0 @ esk3_0)=(esk1_0)), inference(rw,[status(thm)],[c_0_42, c_0_46])).
% 0.25/0.31 thf(c_0_50, plain, ((cL @ esk1_0)=(esk2_0)), inference(spm,[status(thm)],[c_0_47, c_0_35])).
% 0.25/0.31 thf(c_0_51, negated_conjecture, (((cP @ esk4_0 @ esk5_0)=(esk1_0))|(cPSI @ (^[Z0:a]:(![X315:a > $o]:((((((X315 @ esk6_0))&(![X316:a]:((((X315 @ X316))=>((X315 @ (cL @ X316))))))))=>(?[X317:a]:((((X315 @ X317))&(((cR @ X317)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X318:a > $o]:((((((X318 @ esk2_0))&(![X319:a]:((((X318 @ X319))=>((X318 @ (cL @ X319))))))))=>(?[X320:a]:((((X318 @ X320))&(((cR @ X320)=(Z0)))))))))) @ esk3_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_24, c_0_48]), c_0_35])])).
% 0.25/0.31 thf(c_0_52, plain, ((esk6_0)=(esk2_0)), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_47, c_0_49]), c_0_50])).
% 0.25/0.31 thf(c_0_53, negated_conjecture, (((cP @ esk4_0 @ esk5_0)=(esk1_0))|(cPSI @ (^[Z0:a]:(![X321:a > $o]:((((((X321 @ esk2_0))&(![X322:a]:((((X321 @ X322))=>((X321 @ (cL @ X322))))))))=>(?[X323:a]:((((X321 @ X323))&(((cR @ X323)=(Z0)))))))))) @ esk3_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_18, c_0_51]), c_0_52]), c_0_35])])).
% 0.25/0.31 thf(c_0_54, negated_conjecture, ((cPSI @ (^[Z0:a]:(![X324:a > $o]:((((((X324 @ esk6_0))&(![X325:a]:((((X324 @ X325))=>((X324 @ (cL @ X325))))))))=>(?[X326:a]:((((X324 @ X326))&(((cR @ X326)=(Z0)))))))))) @ esk7_0)|(cPHI @ (^[Z0:a]:(![X327:a > $o]:((((((X327 @ esk4_0))&(![X328:a]:((((X327 @ X328))=>((X327 @ (cL @ X328))))))))=>(?[X329:a]:((((X327 @ X329))&(((cR @ X329)=(Z0)))))))))) @ esk5_0)|((esk1_0)=(cZ))|((esk1_0)=(cZ))|(cPHI @ (^[Z0:a]:(![X330:a > $o]:((((((X330 @ esk2_0))&(![X331:a]:((((X330 @ X331))=>((X330 @ (cL @ X331))))))))=>(?[X332:a]:((((X330 @ X332))&(((cR @ X332)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X333:a > $o]:((((((X333 @ esk2_0))&(![X334:a]:((((X333 @ X334))=>((X333 @ (cL @ X334))))))))=>(?[X335:a]:((((X333 @ X335))&(((cR @ X335)=(Z0)))))))))) @ esk3_0)|((esk1_0)=(cZ))), inference(split_conjunct,[status(thm)],[c_0_4])).
% 0.25/0.31 thf(c_0_55, negated_conjecture, ((cP @ esk4_0 @ esk5_0)=(esk1_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_18, c_0_53]), c_0_35])])).
% 0.25/0.31 thf(c_0_56, negated_conjecture, (((esk1_0)=(cZ))|(cPSI @ (^[Z0:a]:(![X336:a > $o]:((((((X336 @ esk2_0))&(![X337:a]:((((X336 @ X337))=>((X336 @ (cL @ X337))))))))=>(?[X338:a]:((((X336 @ X338))&(((cR @ X338)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X339:a > $o]:((((((X339 @ esk6_0))&(![X340:a]:((((X339 @ X340))=>((X339 @ (cL @ X340))))))))=>(?[X341:a]:((((X339 @ X341))&(((cR @ X341)=(Z0)))))))))) @ esk7_0)|(cPHI @ (^[Z0:a]:(![X342:a > $o]:((((((X342 @ esk2_0))&(![X343:a]:((((X342 @ X343))=>((X342 @ (cL @ X343))))))))=>(?[X344:a]:((((X342 @ X344))&(((cR @ X344)=(Z0)))))))))) @ esk3_0)|(cPHI @ (^[Z0:a]:(![X345:a > $o]:((((((X345 @ esk4_0))&(![X346:a]:((((X345 @ X346))=>((X345 @ (cL @ X346))))))))=>(?[X347:a]:((((X345 @ X347))&(((cR @ X347)=(Z0)))))))))) @ esk5_0)), inference(cn,[status(thm)],[c_0_54])).
% 0.25/0.31 thf(c_0_57, plain, ((esk5_0)=(esk3_0)), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_40, c_0_55]), c_0_43])).
% 0.25/0.31 thf(c_0_58, negated_conjecture, ((cPHI @ (^[Z0:a]:(![X348:a > $o]:((((((X348 @ esk4_0))&(![X349:a]:((((X348 @ X349))=>((X348 @ (cL @ X349))))))))=>(?[X350:a]:((((X348 @ X350))&(((cR @ X350)=(Z0)))))))))) @ esk5_0)|(cPHI @ (^[Z0:a]:(![X351:a > $o]:((((((X351 @ esk2_0))&(![X352:a]:((((X351 @ X352))=>((X351 @ (cL @ X352))))))))=>(?[X353:a]:((((X351 @ X353))&(((cR @ X353)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X354:a > $o]:((((((X354 @ esk6_0))&(![X355:a]:((((X354 @ X355))=>((X354 @ (cL @ X355))))))))=>(?[X356:a]:((((X354 @ X356))&(((cR @ X356)=(Z0)))))))))) @ esk7_0)|(cPSI @ (^[Z0:a]:(![X357:a > $o]:((((((X357 @ esk2_0))&(![X358:a]:((((X357 @ X358))=>((X357 @ (cL @ X358))))))))=>(?[X359:a]:((((X357 @ X359))&(((cR @ X359)=(Z0)))))))))) @ esk3_0)), inference(sr,[status(thm)],[c_0_56, c_0_11])).
% 0.25/0.31 thf(c_0_59, negated_conjecture, ((cP @ esk4_0 @ esk3_0)=(esk1_0)), inference(rw,[status(thm)],[c_0_55, c_0_57])).
% 0.25/0.31 thf(c_0_60, negated_conjecture, ((cPSI @ (^[Z0:a]:(![X360:a > $o]:((((((X360 @ esk2_0))&(![X361:a]:((((X360 @ X361))=>((X360 @ (cL @ X361))))))))=>(?[X362:a]:((((X360 @ X362))&(((cR @ X362)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X363:a > $o]:((((((X363 @ esk6_0))&(![X364:a]:((((X363 @ X364))=>((X363 @ (cL @ X364))))))))=>(?[X365:a]:((((X363 @ X365))&(((cR @ X365)=(Z0)))))))))) @ esk3_0)|(cPHI @ (^[Z0:a]:(![X366:a > $o]:((((((X366 @ esk2_0))&(![X367:a]:((((X366 @ X367))=>((X366 @ (cL @ X367))))))))=>(?[X368:a]:((((X366 @ X368))&(((cR @ X368)=(Z0)))))))))) @ esk3_0)|(cPHI @ (^[Z0:a]:(![X369:a > $o]:((((((X369 @ esk4_0))&(![X370:a]:((((X369 @ X370))=>((X369 @ (cL @ X370))))))))=>(?[X371:a]:((((X369 @ X371))&(((cR @ X371)=(Z0)))))))))) @ esk3_0)), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_58, c_0_46]), c_0_57])).
% 0.25/0.31 thf(c_0_61, plain, ((esk4_0)=(esk2_0)), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_47, c_0_59]), c_0_50])).
% 0.25/0.31 thf(c_0_62, negated_conjecture, ((cPHI @ (^[Z0:a]:(![X372:a > $o]:((((((X372 @ esk2_0))&(![X373:a]:((((X372 @ X373))=>((X372 @ (cL @ X373))))))))=>(?[X374:a]:((((X372 @ X374))&(((cR @ X374)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X375:a > $o]:((((((X375 @ esk6_0))&(![X376:a]:((((X375 @ X376))=>((X375 @ (cL @ X376))))))))=>(?[X377:a]:((((X375 @ X377))&(((cR @ X377)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X378:a > $o]:((((((X378 @ esk2_0))&(![X379:a]:((((X378 @ X379))=>((X378 @ (cL @ X379))))))))=>(?[X380:a]:((((X378 @ X380))&(((cR @ X380)=(Z0)))))))))) @ esk3_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_24, c_0_60]), c_0_61]), c_0_35])])).
% 0.25/0.31 thf(c_0_63, negated_conjecture, ((cPSI @ (^[Z0:a]:(![X381:a > $o]:((((((X381 @ esk2_0))&(![X382:a]:((((X381 @ X382))=>((X381 @ (cL @ X382))))))))=>(?[X383:a]:((((X381 @ X383))&(((cR @ X383)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X384:a > $o]:((((((X384 @ esk6_0))&(![X385:a]:((((X384 @ X385))=>((X384 @ (cL @ X385))))))))=>(?[X386:a]:((((X384 @ X386))&(((cR @ X386)=(Z0)))))))))) @ esk3_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_24, c_0_62]), c_0_35])])).
% 0.25/0.31 thf(c_0_64, negated_conjecture, (cPSI @ (^[Z0:a]:(![X387:a > $o]:((((((X387 @ esk2_0))&(![X388:a]:((((X387 @ X388))=>((X387 @ (cL @ X388))))))))=>(?[X389:a]:((((X387 @ X389))&(((cR @ X389)=(Z0)))))))))) @ esk3_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_18, c_0_63]), c_0_52]), c_0_35])])).
% 0.25/0.31 thf(c_0_65, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_18, c_0_64]), c_0_35])]), ['proof']).
% 0.25/0.31 % SZS output end CNFRefutation
% 0.25/0.31 % Parsed axioms : 8
% 0.25/0.31 % Removed by relevancy pruning/SinE : 7
% 0.25/0.31 % Initial clauses : 47
% 0.25/0.31 % Removed in clause preprocessing : 0
% 0.25/0.31 % Initial clauses in saturation : 47
% 0.25/0.31 % Processed clauses : 660
% 0.25/0.31 % ...of these trivial : 14
% 0.25/0.31 % ...subsumed : 404
% 0.25/0.31 % ...remaining for further processing : 242
% 0.25/0.31 % Other redundant clauses eliminated : 0
% 0.25/0.31 % Clauses deleted for lack of memory : 0
% 0.25/0.31 % Backward-subsumed : 143
% 0.25/0.31 % Backward-rewritten : 55
% 0.25/0.31 % Generated clauses : 1031
% 0.25/0.31 % ...of the previous two non-redundant : 960
% 0.25/0.31 % ...aggressively subsumed : 0
% 0.25/0.31 % Contextual simplify-reflections : 8
% 0.25/0.31 % Paramodulations : 996
% 0.25/0.31 % Factorizations : 15
% 0.25/0.31 % NegExts : 0
% 0.25/0.31 % Equation resolutions : 0
% 0.25/0.31 % Disequality decompositions : 0
% 0.25/0.31 % Total rewrite steps : 201
% 0.25/0.31 % ...of those cached : 186
% 0.25/0.31 % Propositional unsat checks : 0
% 0.25/0.31 % Propositional check models : 0
% 0.25/0.31 % Propositional check unsatisfiable : 0
% 0.25/0.31 % Propositional clauses : 0
% 0.25/0.31 % Propositional clauses after purity: 0
% 0.25/0.31 % Propositional unsat core size : 0
% 0.25/0.31 % Propositional preprocessing time : 0.000
% 0.25/0.31 % Propositional encoding time : 0.000
% 0.25/0.31 % Propositional solver time : 0.000
% 0.25/0.31 % Success case prop preproc time : 0.000
% 0.25/0.31 % Success case prop encoding time : 0.000
% 0.25/0.31 % Success case prop solver time : 0.000
% 0.25/0.31 % Current number of processed clauses : 39
% 0.25/0.31 % Positive orientable unit clauses : 13
% 0.25/0.31 % Positive unorientable unit clauses: 0
% 0.25/0.31 % Negative unit clauses : 2
% 0.25/0.31 % Non-unit-clauses : 24
% 0.25/0.31 % Current number of unprocessed clauses: 79
% 0.25/0.31 % ...number of literals in the above : 440
% 0.25/0.31 % Current number of archived formulas : 0
% 0.25/0.31 % Current number of archived clauses : 203
% 0.25/0.31 % Clause-clause subsumption calls (NU) : 8560
% 0.25/0.31 % Rec. Clause-clause subsumption calls : 1522
% 0.25/0.31 % Non-unit clause-clause subsumptions : 378
% 0.25/0.31 % Unit Clause-clause subsumption calls : 242
% 0.25/0.31 % Rewrite failures with RHS unbound : 0
% 0.25/0.31 % BW rewrite match attempts : 11
% 0.25/0.31 % BW rewrite match successes : 10
% 0.25/0.31 % Condensation attempts : 660
% 0.25/0.31 % Condensation successes : 2
% 0.25/0.31 % Termbank termtop insertions : 51618
% 0.25/0.31 % Search garbage collected termcells : 1408
% 0.25/0.31
% 0.25/0.31 % -------------------------------------------------
% 0.25/0.31 % User time : 0.074 s
% 0.25/0.31 % System time : 0.003 s
% 0.25/0.31 % Total time : 0.077 s
% 0.25/0.31 % Maximum resident set size: 3912 pages
% 0.25/0.31
% 0.25/0.31 % -------------------------------------------------
% 0.25/0.31 % User time : 0.147 s
% 0.25/0.31 % System time : 0.008 s
% 0.25/0.31 % Total time : 0.154 s
% 0.25/0.31 % Maximum resident set size: 4864 pages
% 0.25/0.31 % E exiting
%------------------------------------------------------------------------------