%------------------------------------------------------------------------------
% File : E---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 : n005.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:44:51 AM UTC 2026
% Result : Theorem 1.02s 0.43s
% Output : CNFRefutation 1.02s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG294^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n005.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Tue Sep 29 17:37:01 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.24 Running higher-order theorem proving
% 0.07/0.25 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.4yuIhtpc4k/E---3.1_1975340.p
% 1.02/0.43 % Version: 3.5.1-ho
% 1.02/0.43 % Preprocessing class: HSMSSMSSSSMNSSA.
% 1.02/0.43 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 1.02/0.43 % Starting lpo6_lambda_fix with 900s (3) cores
% 1.02/0.43 % Starting post_as_ho3 with 600s (2) cores
% 1.02/0.43 % Starting new_ho_16 with 600s (2) cores
% 1.02/0.43 % Starting full_lambda_1 with 300s (1) cores
% 1.02/0.43 % new_ho_16 with pid 1975355 completed with status 0
% 1.02/0.43 % Result found by new_ho_16
% 1.02/0.43 % Preprocessing class: HSMSSMSSSSMNSSA.
% 1.02/0.43 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 1.02/0.43 % Starting lpo6_lambda_fix with 900s (3) cores
% 1.02/0.43 % Starting post_as_ho3 with 600s (2) cores
% 1.02/0.43 % Starting new_ho_16 with 600s (2) cores
% 1.02/0.43 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 1, sine = LambdaDef)
% 1.02/0.43 % SinE strategy is LambdaDef
% 1.02/0.43 % Search class: HGHSF-FFMM32-DSSFFSBN
% 1.02/0.43 % partial match(2): HGHNF-FFMM32-SSSFFSBN
% 1.02/0.43 % Scheduled 7 strats onto 2 cores with 600 seconds (600 total)
% 1.02/0.43 % Starting SubtermCWHack with 55s (1) cores
% 1.02/0.43 % Starting new_ho_16 with 61s (1) cores
% 1.02/0.43 % new_ho_16 with pid 1975364 completed with status 0
% 1.02/0.43 % Result found by new_ho_16
% 1.02/0.43 % Preprocessing class: HSMSSMSSSSMNSSA.
% 1.02/0.43 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 1.02/0.43 % Starting lpo6_lambda_fix with 900s (3) cores
% 1.02/0.43 % Starting post_as_ho3 with 600s (2) cores
% 1.02/0.43 % Starting new_ho_16 with 600s (2) cores
% 1.02/0.43 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 1, sine = LambdaDef)
% 1.02/0.43 % SinE strategy is LambdaDef
% 1.02/0.43 % Search class: HGHSF-FFMM32-DSSFFSBN
% 1.02/0.43 % partial match(2): HGHNF-FFMM32-SSSFFSBN
% 1.02/0.43 % Scheduled 7 strats onto 2 cores with 600 seconds (600 total)
% 1.02/0.43 % Starting SubtermCWHack with 55s (1) cores
% 1.02/0.43 % Starting new_ho_16 with 61s (1) cores
% 1.02/0.43 % Preprocessing time : 0.003 s
% 1.02/0.43
% 1.02/0.43 % Proof found!
% 1.02/0.43 % SZS status Theorem
% 1.02/0.43 % SZS output start CNFRefutation
% 1.02/0.43 thf(decl_sort1, type, a: $tType).
% 1.02/0.43 thf(decl_23, type, cR: a > a).
% 1.02/0.43 thf(decl_24, type, cL: a > a).
% 1.02/0.43 thf(decl_25, type, cPSI: (a > $o) > a > $o).
% 1.02/0.43 thf(decl_26, type, cP: a > a > a).
% 1.02/0.43 thf(decl_27, type, cZ: a).
% 1.02/0.43 thf(decl_28, type, cPHI: (a > $o) > a > $o).
% 1.02/0.43 thf(decl_29, type, epred1_0: $o).
% 1.02/0.43 thf(decl_30, type, esk1_0: a).
% 1.02/0.43 thf(decl_31, type, esk2_0: a).
% 1.02/0.43 thf(decl_32, type, esk3_0: a).
% 1.02/0.43 thf(decl_33, type, esk4_0: a).
% 1.02/0.43 thf(decl_34, type, esk5_0: a).
% 1.02/0.43 thf(decl_35, type, esk6_0: a).
% 1.02/0.43 thf(decl_36, type, esk7_0: a).
% 1.02/0.43 thf(decl_37, type, esk8_1: (a > $o) > a).
% 1.02/0.43 thf(decl_38, type, esk9_2: (a > $o) > a > a).
% 1.02/0.43 thf(decl_39, type, epred2_3: (a > $o) > a > a > a > $o).
% 1.02/0.43 thf(decl_40, type, esk10_3: (a > $o) > a > a > a).
% 1.02/0.43 thf(decl_41, type, esk11_4: (a > $o) > a > a > (a > $o) > a).
% 1.02/0.43 thf(decl_42, type, esk12_4: (a > $o) > a > a > (a > $o) > a).
% 1.02/0.43 thf(decl_43, type, esk13_2: (a > $o) > a > a).
% 1.02/0.43 thf(decl_44, type, epred3_3: (a > $o) > a > a > a > $o).
% 1.02/0.43 thf(decl_45, type, esk14_3: (a > $o) > a > a > a).
% 1.02/0.43 thf(decl_46, type, esk15_4: (a > $o) > a > a > (a > $o) > a).
% 1.02/0.43 thf(decl_47, type, esk16_4: (a > $o) > a > a > (a > $o) > a).
% 1.02/0.43 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.4yuIhtpc4k/E---3.1_1975340.p', cPU_X2310B_pme)).
% 1.02/0.43 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])).
% 1.02/0.43 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)).
% 1.02/0.43 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])).
% 1.02/0.43 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])])])])])])).
% 1.02/0.43 thf(c_0_5, negated_conjecture, ((cPSI @ (^[Z0:a]:(![X190:a > $o]:((((((X190 @ esk6_0))&(![X191:a]:((((X190 @ X191))=>((X190 @ (cL @ X191))))))))=>(?[X192:a]:((((X190 @ X192))&(((cR @ X192)=(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])).
% 1.02/0.43 thf(c_0_6, negated_conjecture, (((esk1_0)!=(cZ))|((esk1_0)!=(cZ))), inference(split_conjunct,[status(thm)],[c_0_4])).
% 1.02/0.43 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])).
% 1.02/0.43 thf(c_0_8, negated_conjecture, ((cPSI @ (^[Z0:a]:(![X193:a > $o]:((((((X193 @ esk6_0))&(![X194:a]:((((X193 @ X194))=>((X193 @ (cL @ X194))))))))=>(?[X195:a]:((((X193 @ X195))&(((cR @ X195)=(Z0)))))))))) @ esk7_0)|(cPHI @ (^[Z0:a]:(![X196:a > $o]:((((((X196 @ esk4_0))&(![X197:a]:((((X196 @ X197))=>((X196 @ (cL @ X197))))))))=>(?[X198:a]:((((X196 @ X198))&(((cR @ X198)=(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])).
% 1.02/0.43 thf(c_0_9, negated_conjecture, ![X1:a, X2:a, X6:a, X9:a]:((((esk1_0)!=(cP @ X1 @ X2))|~((cPSI @ (^[Z0:a]:(![X199:a > $o]:((((((X199 @ X1))&(![X200:a]:((((X199 @ X200))=>((X199 @ (cL @ X200))))))))=>(?[X201:a]:((((X199 @ X201))&(((cR @ X201)=(Z0)))))))))) @ X2))|~((cPSI @ (^[Z0:a]:(![X202:a > $o]:((((((X202 @ X6))&(![X203:a]:((((X202 @ X203))=>((X202 @ (cL @ X203))))))))=>(?[X204:a]:((((X202 @ X204))&(((cR @ X204)=(Z0)))))))))) @ X9))|((esk1_0)!=(cP @ X6 @ X9)))), inference(split_conjunct,[status(thm)],[c_0_4])).
% 1.02/0.43 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]:(![X205:a > $o]:((((((X205 @ esk6_0))&(![X206:a]:((((X205 @ X206))=>((X205 @ (cL @ X206))))))))=>(?[X207:a]:((((X205 @ X207))&(((cR @ X207)=(Z0)))))))))) @ esk7_0)), inference(cn,[status(thm)],[c_0_5])).
% 1.02/0.43 thf(c_0_11, negated_conjecture, ((esk1_0)!=(cZ)), inference(cn,[status(thm)],[c_0_6])).
% 1.02/0.43 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])).
% 1.02/0.43 thf(c_0_13, negated_conjecture, (((esk1_0)=(cP @ esk6_0 @ esk7_0))|(cPHI @ (^[Z0:a]:(![X208:a > $o]:((((((X208 @ esk4_0))&(![X209:a]:((((X208 @ X209))=>((X208 @ (cL @ X209))))))))=>(?[X210:a]:((((X208 @ X210))&(((cR @ X210)=(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])).
% 1.02/0.43 thf(c_0_14, negated_conjecture, ![X1:a, X2:a, X6:a, X9:a]:((((esk1_0)!=(cP @ X1 @ X2))|~((cPHI @ (^[Z0:a]:(![X211:a > $o]:((((((X211 @ X1))&(![X212:a]:((((X211 @ X212))=>((X211 @ (cL @ X212))))))))=>(?[X213:a]:((((X211 @ X213))&(((cR @ X213)=(Z0)))))))))) @ X2))|~((cPHI @ (^[Z0:a]:(![X214:a > $o]:((((((X214 @ X6))&(![X215:a]:((((X214 @ X215))=>((X214 @ (cL @ X215))))))))=>(?[X216:a]:((((X214 @ X216))&(((cR @ X216)=(Z0)))))))))) @ X9))|((esk1_0)!=(cP @ X6 @ X9)))), inference(split_conjunct,[status(thm)],[c_0_4])).
% 1.02/0.43 thf(c_0_15, negated_conjecture, (((esk1_0)=(cZ))|((esk1_0)=(cP @ esk2_0 @ esk3_0))|(cPSI @ (^[Z0:a]:(![X217:a > $o]:((((((X217 @ esk6_0))&(![X218:a]:((((X217 @ X218))=>((X217 @ (cL @ X218))))))))=>(?[X219:a]:((((X217 @ X219))&(((cR @ X219)=(Z0)))))))))) @ esk7_0)|(cPHI @ (^[Z0:a]:(![X220:a > $o]:((((((X220 @ esk4_0))&(![X221:a]:((((X220 @ X221))=>((X220 @ (cL @ X221))))))))=>(?[X222:a]:((((X220 @ X222))&(((cR @ X222)=(Z0)))))))))) @ esk5_0)), inference(cn,[status(thm)],[c_0_8])).
% 1.02/0.43 thf(c_0_16, negated_conjecture, ![X1:a, X2:a]:((((cP @ X1 @ X2)!=(esk1_0))|~((cPSI @ (^[Z0:a]:(![X223:a > $o]:((((((X223 @ X1))&(![X224:a]:((((X223 @ X224))=>((X223 @ (cL @ X224))))))))=>(?[X225:a]:((((X223 @ X225))&(((cR @ X225)=(Z0)))))))))) @ X2)))), inference(condense,[status(thm)],[c_0_9])).
% 1.02/0.43 thf(c_0_17, negated_conjecture, (((cP @ esk4_0 @ esk5_0)=(esk1_0))|((cP @ esk2_0 @ esk3_0)=(esk1_0))|(cPSI @ (^[Z0:a]:(![X226:a > $o]:((((((X226 @ esk6_0))&(![X227:a]:((((X226 @ X227))=>((X226 @ (cL @ X227))))))))=>(?[X228:a]:((((X226 @ X228))&(((cR @ X228)=(Z0)))))))))) @ esk7_0)), inference(sr,[status(thm)],[c_0_10, c_0_11])).
% 1.02/0.43 thf(c_0_18, 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])).
% 1.02/0.43 thf(c_0_19, negated_conjecture, (((esk1_0)=(cZ))|((esk1_0)=(cP @ esk2_0 @ esk3_0))|((esk1_0)=(cP @ esk6_0 @ esk7_0))|(cPHI @ (^[Z0:a]:(![X229:a > $o]:((((((X229 @ esk4_0))&(![X230:a]:((((X229 @ X230))=>((X229 @ (cL @ X230))))))))=>(?[X231:a]:((((X229 @ X231))&(((cR @ X231)=(Z0)))))))))) @ esk5_0)), inference(cn,[status(thm)],[c_0_13])).
% 1.02/0.43 thf(c_0_20, 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]:(![X232:a > $o]:((((((X232 @ esk2_0))&(![X233:a]:((((X232 @ X233))=>((X232 @ (cL @ X233))))))))=>(?[X234:a]:((((X232 @ X234))&(((cR @ X234)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X235:a > $o]:((((((X235 @ esk2_0))&(![X236:a]:((((X235 @ X236))=>((X235 @ (cL @ X236))))))))=>(?[X237:a]:((((X235 @ X237))&(((cR @ X237)=(Z0)))))))))) @ esk3_0)|((esk1_0)=(cZ))), inference(split_conjunct,[status(thm)],[c_0_4])).
% 1.02/0.43 thf(c_0_21, negated_conjecture, ![X1:a, X2:a]:((((cP @ X1 @ X2)!=(esk1_0))|~((cPHI @ (^[Z0:a]:(![X238:a > $o]:((((((X238 @ X1))&(![X239:a]:((((X238 @ X239))=>((X238 @ (cL @ X239))))))))=>(?[X240:a]:((((X238 @ X240))&(((cR @ X240)=(Z0)))))))))) @ X2)))), inference(condense,[status(thm)],[c_0_14])).
% 1.02/0.43 thf(c_0_22, negated_conjecture, (((cP @ esk2_0 @ esk3_0)=(esk1_0))|(cPHI @ (^[Z0:a]:(![X241:a > $o]:((((((X241 @ esk4_0))&(![X242:a]:((((X241 @ X242))=>((X241 @ (cL @ X242))))))))=>(?[X243:a]:((((X241 @ X243))&(((cR @ X243)=(Z0)))))))))) @ esk5_0)|(cPSI @ (^[Z0:a]:(![X244:a > $o]:((((((X244 @ esk6_0))&(![X245:a]:((((X244 @ X245))=>((X244 @ (cL @ X245))))))))=>(?[X246:a]:((((X244 @ X246))&(((cR @ X246)=(Z0)))))))))) @ esk7_0)), inference(sr,[status(thm)],[c_0_15, c_0_11])).
% 1.02/0.43 thf(c_0_23, 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_16, c_0_17]), c_0_18])).
% 1.02/0.43 thf(c_0_24, negated_conjecture, (((cP @ esk6_0 @ esk7_0)=(esk1_0))|((cP @ esk2_0 @ esk3_0)=(esk1_0))|(cPHI @ (^[Z0:a]:(![X247:a > $o]:((((((X247 @ esk4_0))&(![X248:a]:((((X247 @ X248))=>((X247 @ (cL @ X248))))))))=>(?[X249:a]:((((X247 @ X249))&(((cR @ X249)=(Z0)))))))))) @ esk5_0)), inference(sr,[status(thm)],[c_0_19, c_0_11])).
% 1.02/0.43 thf(c_0_25, negated_conjecture, (((esk1_0)=(cZ))|((esk1_0)=(cP @ esk4_0 @ esk5_0))|((esk1_0)=(cP @ esk6_0 @ esk7_0))|(cPSI @ (^[Z0:a]:(![X250:a > $o]:((((((X250 @ esk2_0))&(![X251:a]:((((X250 @ X251))=>((X250 @ (cL @ X251))))))))=>(?[X252:a]:((((X250 @ X252))&(((cR @ X252)=(Z0)))))))))) @ esk3_0)|(cPHI @ (^[Z0:a]:(![X253:a > $o]:((((((X253 @ esk2_0))&(![X254:a]:((((X253 @ X254))=>((X253 @ (cL @ X254))))))))=>(?[X255:a]:((((X253 @ X255))&(((cR @ X255)=(Z0)))))))))) @ esk3_0)), inference(cn,[status(thm)],[c_0_20])).
% 1.02/0.43 thf(c_0_26, negated_conjecture, (((cP @ esk2_0 @ esk3_0)=(esk1_0))|(cPSI @ (^[Z0:a]:(![X256:a > $o]:((((((X256 @ esk6_0))&(![X257:a]:((((X256 @ X257))=>((X256 @ (cL @ X257))))))))=>(?[X258:a]:((((X256 @ X258))&(((cR @ X258)=(Z0)))))))))) @ esk7_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_21, c_0_22]), c_0_23])).
% 1.02/0.43 thf(c_0_27, 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_21, c_0_24]), c_0_23])).
% 1.02/0.43 thf(c_0_28, negated_conjecture, (((esk1_0)=(cP @ esk6_0 @ esk7_0))|(cPHI @ (^[Z0:a]:(![X259:a > $o]:((((((X259 @ esk4_0))&(![X260:a]:((((X259 @ X260))=>((X259 @ (cL @ X260))))))))=>(?[X261:a]:((((X259 @ X261))&(((cR @ X261)=(Z0)))))))))) @ esk5_0)|((esk1_0)=(cZ))|((esk1_0)=(cZ))|(cPHI @ (^[Z0:a]:(![X262:a > $o]:((((((X262 @ esk2_0))&(![X263:a]:((((X262 @ X263))=>((X262 @ (cL @ X263))))))))=>(?[X264:a]:((((X262 @ X264))&(((cR @ X264)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X265:a > $o]:((((((X265 @ esk2_0))&(![X266:a]:((((X265 @ X266))=>((X265 @ (cL @ X266))))))))=>(?[X267:a]:((((X265 @ X267))&(((cR @ X267)=(Z0)))))))))) @ esk3_0)|((esk1_0)=(cZ))), inference(split_conjunct,[status(thm)],[c_0_4])).
% 1.02/0.43 thf(c_0_29, negated_conjecture, (((cP @ esk6_0 @ esk7_0)=(esk1_0))|((cP @ esk4_0 @ esk5_0)=(esk1_0))|(cPHI @ (^[Z0:a]:(![X268:a > $o]:((((((X268 @ esk2_0))&(![X269:a]:((((X268 @ X269))=>((X268 @ (cL @ X269))))))))=>(?[X270:a]:((((X268 @ X270))&(((cR @ X270)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X271:a > $o]:((((((X271 @ esk2_0))&(![X272:a]:((((X271 @ X272))=>((X271 @ (cL @ X272))))))))=>(?[X273:a]:((((X271 @ X273))&(((cR @ X273)=(Z0)))))))))) @ esk3_0)), inference(sr,[status(thm)],[c_0_25, c_0_11])).
% 1.02/0.43 thf(c_0_30, negated_conjecture, ((cP @ esk2_0 @ esk3_0)=(esk1_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_16, c_0_26]), c_0_27])).
% 1.02/0.43 thf(c_0_31, negated_conjecture, (((esk1_0)=(cZ))|((esk1_0)=(cP @ esk6_0 @ esk7_0))|(cPSI @ (^[Z0:a]:(![X274:a > $o]:((((((X274 @ esk2_0))&(![X275:a]:((((X274 @ X275))=>((X274 @ (cL @ X275))))))))=>(?[X276:a]:((((X274 @ X276))&(((cR @ X276)=(Z0)))))))))) @ esk3_0)|(cPHI @ (^[Z0:a]:(![X277:a > $o]:((((((X277 @ esk2_0))&(![X278:a]:((((X277 @ X278))=>((X277 @ (cL @ X278))))))))=>(?[X279:a]:((((X277 @ X279))&(((cR @ X279)=(Z0)))))))))) @ esk3_0)|(cPHI @ (^[Z0:a]:(![X280:a > $o]:((((((X280 @ esk4_0))&(![X281:a]:((((X280 @ X281))=>((X280 @ (cL @ X281))))))))=>(?[X282:a]:((((X280 @ X282))&(((cR @ X282)=(Z0)))))))))) @ esk5_0)), inference(cn,[status(thm)],[c_0_28])).
% 1.02/0.43 thf(c_0_32, negated_conjecture, (((cP @ esk4_0 @ esk5_0)=(esk1_0))|((cP @ esk6_0 @ esk7_0)=(esk1_0))|(cPSI @ (^[Z0:a]:(![X283:a > $o]:((((((X283 @ esk2_0))&(![X284:a]:((((X283 @ X284))=>((X283 @ (cL @ X284))))))))=>(?[X285:a]:((((X283 @ X285))&(((cR @ X285)=(Z0)))))))))) @ esk3_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_21, c_0_29]), c_0_30])])).
% 1.02/0.43 thf(c_0_33, 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])).
% 1.02/0.43 thf(c_0_34, negated_conjecture, (((cP @ esk6_0 @ esk7_0)=(esk1_0))|(cPHI @ (^[Z0:a]:(![X286:a > $o]:((((((X286 @ esk4_0))&(![X287:a]:((((X286 @ X287))=>((X286 @ (cL @ X287))))))))=>(?[X288:a]:((((X286 @ X288))&(((cR @ X288)=(Z0)))))))))) @ esk5_0)|(cPHI @ (^[Z0:a]:(![X289:a > $o]:((((((X289 @ esk2_0))&(![X290:a]:((((X289 @ X290))=>((X289 @ (cL @ X290))))))))=>(?[X291:a]:((((X289 @ X291))&(((cR @ X291)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X292:a > $o]:((((((X292 @ esk2_0))&(![X293:a]:((((X292 @ X293))=>((X292 @ (cL @ X293))))))))=>(?[X294:a]:((((X292 @ X294))&(((cR @ X294)=(Z0)))))))))) @ esk3_0)), inference(sr,[status(thm)],[c_0_31, c_0_11])).
% 1.02/0.43 thf(c_0_35, negated_conjecture, (((cP @ esk6_0 @ esk7_0)=(esk1_0))|((cP @ esk4_0 @ esk5_0)=(esk1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_16, c_0_32]), c_0_30])])).
% 1.02/0.43 thf(c_0_36, 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_33])])])])])])])).
% 1.02/0.43 thf(c_0_37, negated_conjecture, (((cP @ esk6_0 @ esk7_0)=(esk1_0))|(cPSI @ (^[Z0:a]:(![X295:a > $o]:((((((X295 @ esk2_0))&(![X296:a]:((((X295 @ X296))=>((X295 @ (cL @ X296))))))))=>(?[X297:a]:((((X295 @ X297))&(((cR @ X297)=(Z0)))))))))) @ esk3_0)|(cPHI @ (^[Z0:a]:(![X298:a > $o]:((((((X298 @ esk2_0))&(![X299:a]:((((X298 @ X299))=>((X298 @ (cL @ X299))))))))=>(?[X300:a]:((((X298 @ X300))&(((cR @ X300)=(Z0)))))))))) @ esk3_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_21, c_0_34]), c_0_35])).
% 1.02/0.43 thf(c_0_38, plain, ![X2:a, X1:a]:((((cL @ (cP @ X1 @ X2))=(X1))|~((epred1_0)))), inference(split_conjunct,[status(thm)],[c_0_36])).
% 1.02/0.43 thf(c_0_39, negated_conjecture, (epred1_0), inference(split_conjunct,[status(thm)],[c_0_4])).
% 1.02/0.43 thf(c_0_40, negated_conjecture, (((cP @ esk6_0 @ esk7_0)=(esk1_0))|(cPSI @ (^[Z0:a]:(![X301:a > $o]:((((((X301 @ esk2_0))&(![X302:a]:((((X301 @ X302))=>((X301 @ (cL @ X302))))))))=>(?[X303:a]:((((X301 @ X303))&(((cR @ X303)=(Z0)))))))))) @ esk3_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_21, c_0_37]), c_0_30])])).
% 1.02/0.43 thf(c_0_41, plain, ![X2:a, X1:a]:(((cL @ (cP @ X1 @ X2))=(X1))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_38, c_0_39])])).
% 1.02/0.43 thf(c_0_42, negated_conjecture, ((cPSI @ (^[Z0:a]:(![X304:a > $o]:((((((X304 @ esk6_0))&(![X305:a]:((((X304 @ X305))=>((X304 @ (cL @ X305))))))))=>(?[X306:a]:((((X304 @ X306))&(((cR @ X306)=(Z0)))))))))) @ esk7_0)|((esk1_0)=(cP @ esk4_0 @ esk5_0))|((esk1_0)=(cZ))|((esk1_0)=(cZ))|(cPHI @ (^[Z0:a]:(![X307:a > $o]:((((((X307 @ esk2_0))&(![X308:a]:((((X307 @ X308))=>((X307 @ (cL @ X308))))))))=>(?[X309:a]:((((X307 @ X309))&(((cR @ X309)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X310:a > $o]:((((((X310 @ esk2_0))&(![X311:a]:((((X310 @ X311))=>((X310 @ (cL @ X311))))))))=>(?[X312:a]:((((X310 @ X312))&(((cR @ X312)=(Z0)))))))))) @ esk3_0)|((esk1_0)=(cZ))), inference(split_conjunct,[status(thm)],[c_0_4])).
% 1.02/0.43 thf(c_0_43, negated_conjecture, ((cP @ esk6_0 @ esk7_0)=(esk1_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_16, c_0_40]), c_0_30])])).
% 1.02/0.43 thf(c_0_44, plain, ((cL @ esk1_0)=(esk2_0)), inference(spm,[status(thm)],[c_0_41, c_0_30])).
% 1.02/0.43 thf(c_0_45, plain, ![X1:a, X2:a]:((((cR @ (cP @ X1 @ X2))=(X2))|~((epred1_0)))), inference(split_conjunct,[status(thm)],[c_0_36])).
% 1.02/0.43 thf(c_0_46, negated_conjecture, (((esk1_0)=(cZ))|((esk1_0)=(cP @ esk4_0 @ esk5_0))|(cPSI @ (^[Z0:a]:(![X313:a > $o]:((((((X313 @ esk2_0))&(![X314:a]:((((X313 @ X314))=>((X313 @ (cL @ X314))))))))=>(?[X315:a]:((((X313 @ X315))&(((cR @ X315)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X316:a > $o]:((((((X316 @ esk6_0))&(![X317:a]:((((X316 @ X317))=>((X316 @ (cL @ X317))))))))=>(?[X318:a]:((((X316 @ X318))&(((cR @ X318)=(Z0)))))))))) @ esk7_0)|(cPHI @ (^[Z0:a]:(![X319:a > $o]:((((((X319 @ esk2_0))&(![X320:a]:((((X319 @ X320))=>((X319 @ (cL @ X320))))))))=>(?[X321:a]:((((X319 @ X321))&(((cR @ X321)=(Z0)))))))))) @ esk3_0)), inference(cn,[status(thm)],[c_0_42])).
% 1.02/0.43 thf(c_0_47, plain, ((esk6_0)=(esk2_0)), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_43]), c_0_44])).
% 1.02/0.43 thf(c_0_48, plain, ![X1:a, X2:a]:(((cR @ (cP @ X1 @ X2))=(X2))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_45, c_0_39])])).
% 1.02/0.43 thf(c_0_49, negated_conjecture, (((cP @ esk4_0 @ esk5_0)=(esk1_0))|(cPHI @ (^[Z0:a]:(![X322:a > $o]:((((((X322 @ esk2_0))&(![X323:a]:((((X322 @ X323))=>((X322 @ (cL @ X323))))))))=>(?[X324:a]:((((X322 @ X324))&(((cR @ X324)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X325:a > $o]:((((((X325 @ esk6_0))&(![X326:a]:((((X325 @ X326))=>((X325 @ (cL @ X326))))))))=>(?[X327:a]:((((X325 @ X327))&(((cR @ X327)=(Z0)))))))))) @ esk7_0)|(cPSI @ (^[Z0:a]:(![X328:a > $o]:((((((X328 @ esk2_0))&(![X329:a]:((((X328 @ X329))=>((X328 @ (cL @ X329))))))))=>(?[X330:a]:((((X328 @ X330))&(((cR @ X330)=(Z0)))))))))) @ esk3_0)), inference(sr,[status(thm)],[c_0_46, c_0_11])).
% 1.02/0.43 thf(c_0_50, negated_conjecture, ((cP @ esk2_0 @ esk7_0)=(esk1_0)), inference(rw,[status(thm)],[c_0_43, c_0_47])).
% 1.02/0.43 thf(c_0_51, plain, ((cR @ esk1_0)=(esk3_0)), inference(spm,[status(thm)],[c_0_48, c_0_30])).
% 1.02/0.43 thf(c_0_52, negated_conjecture, (((cP @ esk4_0 @ esk5_0)=(esk1_0))|(cPSI @ (^[Z0:a]:(![X331:a > $o]:((((((X331 @ esk2_0))&(![X332:a]:((((X331 @ X332))=>((X331 @ (cL @ X332))))))))=>(?[X333:a]:((((X331 @ X333))&(((cR @ X333)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X334:a > $o]:((((((X334 @ esk6_0))&(![X335:a]:((((X334 @ X335))=>((X334 @ (cL @ X335))))))))=>(?[X336:a]:((((X334 @ X336))&(((cR @ X336)=(Z0)))))))))) @ esk7_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_21, c_0_49]), c_0_30])])).
% 1.02/0.43 thf(c_0_53, plain, ((esk7_0)=(esk3_0)), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_48, c_0_50]), c_0_51])).
% 1.02/0.43 thf(c_0_54, negated_conjecture, (((cP @ esk4_0 @ esk5_0)=(esk1_0))|(cPSI @ (^[Z0:a]:(![X337:a > $o]:((((((X337 @ esk6_0))&(![X338:a]:((((X337 @ X338))=>((X337 @ (cL @ X338))))))))=>(?[X339:a]:((((X337 @ X339))&(((cR @ X339)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X340:a > $o]:((((((X340 @ esk2_0))&(![X341:a]:((((X340 @ X341))=>((X340 @ (cL @ X341))))))))=>(?[X342:a]:((((X340 @ X342))&(((cR @ X342)=(Z0)))))))))) @ esk3_0)), inference(rw,[status(thm)],[c_0_52, c_0_53])).
% 1.02/0.43 thf(c_0_55, negated_conjecture, (((cP @ esk4_0 @ esk5_0)=(esk1_0))|(cPSI @ (^[Z0:a]:(![X343:a > $o]:((((((X343 @ esk2_0))&(![X344:a]:((((X343 @ X344))=>((X343 @ (cL @ X344))))))))=>(?[X345:a]:((((X343 @ X345))&(((cR @ X345)=(Z0)))))))))) @ esk3_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_16, c_0_54]), c_0_47]), c_0_30])])).
% 1.02/0.43 thf(c_0_56, negated_conjecture, ((cPSI @ (^[Z0:a]:(![X346:a > $o]:((((((X346 @ esk6_0))&(![X347:a]:((((X346 @ X347))=>((X346 @ (cL @ X347))))))))=>(?[X348:a]:((((X346 @ X348))&(((cR @ X348)=(Z0)))))))))) @ esk7_0)|(cPHI @ (^[Z0:a]:(![X349:a > $o]:((((((X349 @ esk4_0))&(![X350:a]:((((X349 @ X350))=>((X349 @ (cL @ X350))))))))=>(?[X351:a]:((((X349 @ X351))&(((cR @ X351)=(Z0)))))))))) @ esk5_0)|((esk1_0)=(cZ))|((esk1_0)=(cZ))|(cPHI @ (^[Z0:a]:(![X352:a > $o]:((((((X352 @ esk2_0))&(![X353:a]:((((X352 @ X353))=>((X352 @ (cL @ X353))))))))=>(?[X354:a]:((((X352 @ X354))&(((cR @ X354)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X355:a > $o]:((((((X355 @ esk2_0))&(![X356:a]:((((X355 @ X356))=>((X355 @ (cL @ X356))))))))=>(?[X357:a]:((((X355 @ X357))&(((cR @ X357)=(Z0)))))))))) @ esk3_0)|((esk1_0)=(cZ))), inference(split_conjunct,[status(thm)],[c_0_4])).
% 1.02/0.43 thf(c_0_57, negated_conjecture, ((cP @ esk4_0 @ esk5_0)=(esk1_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_16, c_0_55]), c_0_30])])).
% 1.02/0.43 thf(c_0_58, negated_conjecture, (((esk1_0)=(cZ))|(cPSI @ (^[Z0:a]:(![X358:a > $o]:((((((X358 @ esk2_0))&(![X359:a]:((((X358 @ X359))=>((X358 @ (cL @ X359))))))))=>(?[X360:a]:((((X358 @ X360))&(((cR @ X360)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X361:a > $o]:((((((X361 @ esk6_0))&(![X362:a]:((((X361 @ X362))=>((X361 @ (cL @ X362))))))))=>(?[X363:a]:((((X361 @ X363))&(((cR @ X363)=(Z0)))))))))) @ esk7_0)|(cPHI @ (^[Z0:a]:(![X364:a > $o]:((((((X364 @ esk2_0))&(![X365:a]:((((X364 @ X365))=>((X364 @ (cL @ X365))))))))=>(?[X366:a]:((((X364 @ X366))&(((cR @ X366)=(Z0)))))))))) @ esk3_0)|(cPHI @ (^[Z0:a]:(![X367:a > $o]:((((((X367 @ esk4_0))&(![X368:a]:((((X367 @ X368))=>((X367 @ (cL @ X368))))))))=>(?[X369:a]:((((X367 @ X369))&(((cR @ X369)=(Z0)))))))))) @ esk5_0)), inference(cn,[status(thm)],[c_0_56])).
% 1.02/0.43 thf(c_0_59, plain, ((esk4_0)=(esk2_0)), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_57]), c_0_44])).
% 1.02/0.43 thf(c_0_60, negated_conjecture, ((cPHI @ (^[Z0:a]:(![X370:a > $o]:((((((X370 @ esk4_0))&(![X371:a]:((((X370 @ X371))=>((X370 @ (cL @ X371))))))))=>(?[X372:a]:((((X370 @ X372))&(((cR @ X372)=(Z0)))))))))) @ esk5_0)|(cPHI @ (^[Z0:a]:(![X373:a > $o]:((((((X373 @ esk2_0))&(![X374:a]:((((X373 @ X374))=>((X373 @ (cL @ X374))))))))=>(?[X375:a]:((((X373 @ X375))&(((cR @ X375)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X376:a > $o]:((((((X376 @ esk6_0))&(![X377:a]:((((X376 @ X377))=>((X376 @ (cL @ X377))))))))=>(?[X378:a]:((((X376 @ X378))&(((cR @ X378)=(Z0)))))))))) @ esk7_0)|(cPSI @ (^[Z0:a]:(![X379:a > $o]:((((((X379 @ esk2_0))&(![X380:a]:((((X379 @ X380))=>((X379 @ (cL @ X380))))))))=>(?[X381:a]:((((X379 @ X381))&(((cR @ X381)=(Z0)))))))))) @ esk3_0)), inference(sr,[status(thm)],[c_0_58, c_0_11])).
% 1.02/0.43 thf(c_0_61, negated_conjecture, ((cP @ esk2_0 @ esk5_0)=(esk1_0)), inference(rw,[status(thm)],[c_0_57, c_0_59])).
% 1.02/0.43 thf(c_0_62, negated_conjecture, ((cPSI @ (^[Z0:a]:(![X382:a > $o]:((((((X382 @ esk2_0))&(![X383:a]:((((X382 @ X383))=>((X382 @ (cL @ X383))))))))=>(?[X384:a]:((((X382 @ X384))&(((cR @ X384)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X385:a > $o]:((((((X385 @ esk6_0))&(![X386:a]:((((X385 @ X386))=>((X385 @ (cL @ X386))))))))=>(?[X387:a]:((((X385 @ X387))&(((cR @ X387)=(Z0)))))))))) @ esk3_0)|(cPHI @ (^[Z0:a]:(![X388:a > $o]:((((((X388 @ esk2_0))&(![X389:a]:((((X388 @ X389))=>((X388 @ (cL @ X389))))))))=>(?[X390:a]:((((X388 @ X390))&(((cR @ X390)=(Z0)))))))))) @ esk3_0)|(cPHI @ (^[Z0:a]:(![X391:a > $o]:((((((X391 @ esk4_0))&(![X392:a]:((((X391 @ X392))=>((X391 @ (cL @ X392))))))))=>(?[X393:a]:((((X391 @ X393))&(((cR @ X393)=(Z0)))))))))) @ esk5_0)), inference(rw,[status(thm)],[c_0_60, c_0_53])).
% 1.02/0.43 thf(c_0_63, plain, ((esk5_0)=(esk3_0)), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_48, c_0_61]), c_0_51])).
% 1.02/0.43 thf(c_0_64, negated_conjecture, ((cPHI @ (^[Z0:a]:(![X394:a > $o]:((((((X394 @ esk4_0))&(![X395:a]:((((X394 @ X395))=>((X394 @ (cL @ X395))))))))=>(?[X396:a]:((((X394 @ X396))&(((cR @ X396)=(Z0)))))))))) @ esk3_0)|(cPHI @ (^[Z0:a]:(![X397:a > $o]:((((((X397 @ esk2_0))&(![X398:a]:((((X397 @ X398))=>((X397 @ (cL @ X398))))))))=>(?[X399:a]:((((X397 @ X399))&(((cR @ X399)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X400:a > $o]:((((((X400 @ esk6_0))&(![X401:a]:((((X400 @ X401))=>((X400 @ (cL @ X401))))))))=>(?[X402:a]:((((X400 @ X402))&(((cR @ X402)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X403:a > $o]:((((((X403 @ esk2_0))&(![X404:a]:((((X403 @ X404))=>((X403 @ (cL @ X404))))))))=>(?[X405:a]:((((X403 @ X405))&(((cR @ X405)=(Z0)))))))))) @ esk3_0)), inference(rw,[status(thm)],[c_0_62, c_0_63])).
% 1.02/0.43 thf(c_0_65, negated_conjecture, ((cPSI @ (^[Z0:a]:(![X406:a > $o]:((((((X406 @ esk2_0))&(![X407:a]:((((X406 @ X407))=>((X406 @ (cL @ X407))))))))=>(?[X408:a]:((((X406 @ X408))&(((cR @ X408)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X409:a > $o]:((((((X409 @ esk6_0))&(![X410:a]:((((X409 @ X410))=>((X409 @ (cL @ X410))))))))=>(?[X411:a]:((((X409 @ X411))&(((cR @ X411)=(Z0)))))))))) @ esk3_0)|(cPHI @ (^[Z0:a]:(![X412:a > $o]:((((((X412 @ esk2_0))&(![X413:a]:((((X412 @ X413))=>((X412 @ (cL @ X413))))))))=>(?[X414:a]:((((X412 @ X414))&(((cR @ X414)=(Z0)))))))))) @ esk3_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_21, c_0_64]), c_0_59]), c_0_30])])).
% 1.02/0.43 thf(c_0_66, negated_conjecture, ((cPSI @ (^[Z0:a]:(![X415:a > $o]:((((((X415 @ esk6_0))&(![X416:a]:((((X415 @ X416))=>((X415 @ (cL @ X416))))))))=>(?[X417:a]:((((X415 @ X417))&(((cR @ X417)=(Z0)))))))))) @ esk3_0)|(cPSI @ (^[Z0:a]:(![X418:a > $o]:((((((X418 @ esk2_0))&(![X419:a]:((((X418 @ X419))=>((X418 @ (cL @ X419))))))))=>(?[X420:a]:((((X418 @ X420))&(((cR @ X420)=(Z0)))))))))) @ esk3_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_21, c_0_65]), c_0_30])])).
% 1.02/0.43 thf(c_0_67, negated_conjecture, (cPSI @ (^[Z0:a]:(![X421:a > $o]:((((((X421 @ esk2_0))&(![X422:a]:((((X421 @ X422))=>((X421 @ (cL @ X422))))))))=>(?[X423:a]:((((X421 @ X423))&(((cR @ X423)=(Z0)))))))))) @ esk3_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_16, c_0_66]), c_0_47]), c_0_30])])).
% 1.02/0.43 thf(c_0_68, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_16, c_0_67]), c_0_30])]), ['proof']).
% 1.02/0.43 % SZS output end CNFRefutation
% 1.02/0.43 % Parsed axioms : 8
% 1.02/0.43 % Removed by relevancy pruning/SinE : 7
% 1.02/0.43 % Initial clauses : 47
% 1.02/0.43 % Removed in clause preprocessing : 0
% 1.02/0.43 % Initial clauses in saturation : 47
% 1.02/0.43 % Processed clauses : 692
% 1.02/0.43 % ...of these trivial : 11
% 1.02/0.43 % ...subsumed : 421
% 1.02/0.43 % ...remaining for further processing : 260
% 1.02/0.43 % Other redundant clauses eliminated : 0
% 1.02/0.43 % Clauses deleted for lack of memory : 0
% 1.02/0.43 % Backward-subsumed : 152
% 1.02/0.43 % Backward-rewritten : 62
% 1.02/0.43 % Generated clauses : 1107
% 1.02/0.43 % ...of the previous two non-redundant : 1028
% 1.02/0.43 % ...aggressively subsumed : 0
% 1.02/0.43 % Contextual simplify-reflections : 9
% 1.02/0.43 % Paramodulations : 1068
% 1.02/0.43 % Factorizations : 15
% 1.02/0.43 % NegExts : 0
% 1.02/0.43 % Equation resolutions : 0
% 1.02/0.43 % Disequality decompositions : 0
% 1.02/0.43 % Total rewrite steps : 272
% 1.02/0.43 % ...of those cached : 256
% 1.02/0.43 % Propositional unsat checks : 0
% 1.02/0.43 % Propositional check models : 0
% 1.02/0.43 % Propositional check unsatisfiable : 0
% 1.02/0.43 % Propositional clauses : 0
% 1.02/0.43 % Propositional clauses after purity: 0
% 1.02/0.43 % Propositional unsat core size : 0
% 1.02/0.43 % Propositional preprocessing time : 0.000
% 1.02/0.43 % Propositional encoding time : 0.000
% 1.02/0.43 % Propositional solver time : 0.000
% 1.02/0.43 % Success case prop preproc time : 0.000
% 1.02/0.43 % Success case prop encoding time : 0.000
% 1.02/0.43 % Success case prop solver time : 0.000
% 1.02/0.43 % Current number of processed clauses : 40
% 1.02/0.43 % Positive orientable unit clauses : 13
% 1.02/0.43 % Positive unorientable unit clauses: 0
% 1.02/0.43 % Negative unit clauses : 2
% 1.02/0.43 % Non-unit-clauses : 25
% 1.02/0.43 % Current number of unprocessed clauses: 122
% 1.02/0.43 % ...number of literals in the above : 685
% 1.02/0.43 % Current number of archived formulas : 0
% 1.02/0.43 % Current number of archived clauses : 220
% 1.02/0.43 % Clause-clause subsumption calls (NU) : 8953
% 1.02/0.43 % Rec. Clause-clause subsumption calls : 1774
% 1.02/0.43 % Non-unit clause-clause subsumptions : 394
% 1.02/0.43 % Unit Clause-clause subsumption calls : 246
% 1.02/0.43 % Rewrite failures with RHS unbound : 0
% 1.02/0.43 % BW rewrite match attempts : 12
% 1.02/0.43 % BW rewrite match successes : 11
% 1.02/0.43 % Condensation attempts : 692
% 1.02/0.43 % Condensation successes : 2
% 1.02/0.43 % Termbank termtop insertions : 57120
% 1.02/0.43 % Search garbage collected termcells : 1408
% 1.02/0.43
% 1.02/0.43 % -------------------------------------------------
% 1.02/0.43 % User time : 0.081 s
% 1.02/0.43 % System time : 0.004 s
% 1.02/0.43 % Total time : 0.084 s
% 1.02/0.43 % Maximum resident set size: 3912 pages
% 1.02/0.43
% 1.02/0.43 % -------------------------------------------------
% 1.02/0.43 % User time : 0.158 s
% 1.02/0.43 % System time : 0.011 s
% 1.02/0.43 % Total time : 0.169 s
% 1.02/0.43 % Maximum resident set size: 4608 pages
% 1.02/0.43 % E exiting
%------------------------------------------------------------------------------