%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWW513_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n018.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Oct 3 08:06:23 PM UTC 2025 % Result : Theorem 32.80s 33.00s % Output : Proof 32.87s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWW513_5 : TPTP v9.2.0. Released v6.0.0. % 0.03/0.13 % Command : duper %s % 0.12/0.34 % Computer : n018.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Thu Oct 2 11:09:08 EDT 2025 % 0.12/0.34 % CPUTime : % 32.80/33.00 SZS status Theorem for theBenchmark.p % 32.80/33.00 SZS output start Proof for theBenchmark.p % 32.80/33.00 Clause #1 (by assumption #[]): Eq % 32.80/33.00 (∀ (B : Type) (Tsa Ts G1 : fun (hoare_28830079triple B) bool), % 32.80/33.00 hoare_992312373derivs B G1 Ts → % 32.80/33.00 pp % 32.80/33.00 (aa (fun (hoare_28830079triple B) bool) bool % 32.80/33.00 (aa (fun (hoare_28830079triple B) bool) (fun (fun (hoare_28830079triple B) bool) bool) % 32.80/33.00 (ord_less_eq (fun (hoare_28830079triple B) bool)) Tsa) % 32.80/33.00 Ts) → % 32.80/33.00 hoare_992312373derivs B G1 Tsa) % 32.80/33.00 True % 32.80/33.00 Clause #55 (by assumption #[]): Eq % 32.80/33.00 (∀ (B : Type) (A1 : fun B bool), % 32.80/33.00 Eq (pow B A1) (collect (fun B bool) (combc (fun B bool) (fun B bool) bool (ord_less_eq (fun B bool)) A1))) % 32.80/33.00 True % 32.80/33.00 Clause #74 (by assumption #[]): Eq (∀ (B : Type) (P1 : fun B bool), Eq (collect B P1) P1) True % 32.80/33.00 Clause #111 (by assumption #[]): Eq % 32.80/33.00 (∀ (A C B : Type) (R : A) (Q : B) (P : fun A (fun B C)), % 32.80/33.00 Eq (aa A C (combc A B C P Q) R) (aa B C (aa A (fun B C) P R) Q)) % 32.80/33.00 True % 32.80/33.00 Clause #114 (by assumption #[]): Eq % 32.80/33.00 (pp % 32.80/33.00 (aa (fun (hoare_28830079triple a) bool) bool % 32.80/33.00 (aa (fun (hoare_28830079triple a) bool) (fun (fun (hoare_28830079triple a) bool) bool) % 32.80/33.00 (ord_less_eq (fun (hoare_28830079triple a) bool)) tsa) % 32.80/33.00 ts)) % 32.80/33.00 True % 32.80/33.00 Clause #116 (by assumption #[]): Eq (hoare_992312373derivs a ga ts) True % 32.80/33.00 Clause #117 (by assumption #[]): Eq (Not (hoare_992312373derivs a ga tsa)) True % 32.80/33.00 Clause #123 (by clausification #[117]): Eq (hoare_992312373derivs a ga tsa) False % 32.80/33.00 Clause #124 (by clausification #[1]): ∀ (a : Type), % 32.80/33.00 Eq % 32.80/33.00 (∀ (Tsa Ts G1 : fun (hoare_28830079triple a) bool), % 32.80/33.00 hoare_992312373derivs a G1 Ts → % 32.80/33.00 pp % 32.80/33.00 (aa (fun (hoare_28830079triple a) bool) bool % 32.80/33.00 (aa (fun (hoare_28830079triple a) bool) (fun (fun (hoare_28830079triple a) bool) bool) % 32.80/33.00 (ord_less_eq (fun (hoare_28830079triple a) bool)) Tsa) % 32.80/33.00 Ts) → % 32.80/33.00 hoare_992312373derivs a G1 Tsa) % 32.80/33.00 True % 32.80/33.00 Clause #125 (by clausification #[124]): ∀ (a : Type) (a_1 : fun (hoare_28830079triple a) bool), % 32.80/33.00 Eq % 32.80/33.00 (∀ (Ts G1 : fun (hoare_28830079triple a) bool), % 32.80/33.00 hoare_992312373derivs a G1 Ts → % 32.80/33.00 pp % 32.80/33.00 (aa (fun (hoare_28830079triple a) bool) bool % 32.80/33.00 (aa (fun (hoare_28830079triple a) bool) (fun (fun (hoare_28830079triple a) bool) bool) % 32.80/33.00 (ord_less_eq (fun (hoare_28830079triple a) bool)) a_1) % 32.80/33.00 Ts) → % 32.80/33.00 hoare_992312373derivs a G1 a_1) % 32.80/33.00 True % 32.80/33.00 Clause #126 (by clausification #[125]): ∀ (a : Type) (a_1 a_2 : fun (hoare_28830079triple a) bool), % 32.80/33.00 Eq % 32.80/33.00 (∀ (G1 : fun (hoare_28830079triple a) bool), % 32.80/33.00 hoare_992312373derivs a G1 a_1 → % 32.80/33.00 pp % 32.80/33.00 (aa (fun (hoare_28830079triple a) bool) bool % 32.80/33.00 (aa (fun (hoare_28830079triple a) bool) (fun (fun (hoare_28830079triple a) bool) bool) % 32.80/33.00 (ord_less_eq (fun (hoare_28830079triple a) bool)) a_2) % 32.80/33.00 a_1) → % 32.80/33.00 hoare_992312373derivs a G1 a_2) % 32.80/33.00 True % 32.80/33.00 Clause #127 (by clausification #[126]): ∀ (a : Type) (a_1 a_2 a_3 : fun (hoare_28830079triple a) bool), % 32.80/33.00 Eq % 32.80/33.00 (hoare_992312373derivs a a_1 a_2 → % 32.80/33.00 pp % 32.80/33.00 (aa (fun (hoare_28830079triple a) bool) bool % 32.80/33.00 (aa (fun (hoare_28830079triple a) bool) (fun (fun (hoare_28830079triple a) bool) bool) % 32.80/33.00 (ord_less_eq (fun (hoare_28830079triple a) bool)) a_3) % 32.80/33.00 a_2) → % 32.80/33.00 hoare_992312373derivs a a_1 a_3) % 32.80/33.00 True % 32.80/33.00 Clause #128 (by clausification #[127]): ∀ (a : Type) (a_1 a_2 a_3 : fun (hoare_28830079triple a) bool), % 32.80/33.00 Or (Eq (hoare_992312373derivs a a_1 a_2) False) % 32.80/33.00 (Eq % 32.80/33.00 (pp % 32.80/33.00 (aa (fun (hoare_28830079triple a) bool) bool % 32.80/33.00 (aa (fun (hoare_28830079triple a) bool) (fun (fun (hoare_28830079triple a) bool) bool) % 32.80/33.00 (ord_less_eq (fun (hoare_28830079triple a) bool)) a_3) % 32.80/33.00 a_2) → % 32.80/33.00 hoare_992312373derivs a a_1 a_3) % 32.80/33.00 True) % 32.80/33.00 Clause #129 (by clausification #[128]): ∀ (a : Type) (a_1 a_2 a_3 : fun (hoare_28830079triple a) bool), % 32.80/33.00 Or (Eq (hoare_992312373derivs a a_1 a_2) False) % 32.80/33.00 (Or % 32.80/33.00 (Eq % 32.80/33.00 (pp % 32.80/33.00 (aa (fun (hoare_28830079triple a) bool) bool % 32.80/33.02 (aa (fun (hoare_28830079triple a) bool) (fun (fun (hoare_28830079triple a) bool) bool) % 32.80/33.02 (ord_less_eq (fun (hoare_28830079triple a) bool)) a_3) % 32.80/33.02 a_2)) % 32.80/33.02 False) % 32.80/33.02 (Eq (hoare_992312373derivs a a_1 a_3) True)) % 32.80/33.02 Clause #130 (by superposition #[129, 116]): ∀ (a_1 : fun (hoare_28830079triple a) bool), % 32.80/33.02 Or % 32.80/33.02 (Eq % 32.80/33.02 (pp % 32.80/33.02 (aa (fun (hoare_28830079triple a) bool) bool % 32.80/33.02 (aa (fun (hoare_28830079triple a) bool) (fun (fun (hoare_28830079triple a) bool) bool) % 32.80/33.02 (ord_less_eq (fun (hoare_28830079triple a) bool)) a_1) % 32.80/33.02 ts)) % 32.80/33.02 False) % 32.80/33.02 (Or (Eq (hoare_992312373derivs a ga a_1) True) (Eq False True)) % 32.80/33.02 Clause #213 (by clausification #[74]): ∀ (a : Type), Eq (∀ (P1 : fun a bool), Eq (collect a P1) P1) True % 32.80/33.02 Clause #214 (by clausification #[213]): ∀ (a : Type) (a_1 : fun a bool), Eq (Eq (collect a a_1) a_1) True % 32.80/33.02 Clause #215 (by clausification #[214]): ∀ (a : Type) (a_1 : fun a bool), Eq (collect a a_1) a_1 % 32.80/33.02 Clause #3941 (by clausification #[55]): ∀ (a : Type), % 32.80/33.02 Eq % 32.80/33.02 (∀ (A1 : fun a bool), % 32.80/33.02 Eq (pow a A1) (collect (fun a bool) (combc (fun a bool) (fun a bool) bool (ord_less_eq (fun a bool)) A1))) % 32.80/33.02 True % 32.80/33.02 Clause #3942 (by clausification #[3941]): ∀ (a : Type) (a_1 : fun a bool), % 32.80/33.02 Eq (Eq (pow a a_1) (collect (fun a bool) (combc (fun a bool) (fun a bool) bool (ord_less_eq (fun a bool)) a_1))) True % 32.80/33.02 Clause #3943 (by clausification #[3942]): ∀ (a : Type) (a_1 : fun a bool), % 32.80/33.02 Eq (pow a a_1) (collect (fun a bool) (combc (fun a bool) (fun a bool) bool (ord_less_eq (fun a bool)) a_1)) % 32.80/33.02 Clause #3944 (by superposition #[3943, 215]): ∀ (a : Type) (a_1 : fun a bool), Eq (pow a a_1) (combc (fun a bool) (fun a bool) bool (ord_less_eq (fun a bool)) a_1) % 32.80/33.02 Clause #9802 (by clausification #[111]): ∀ (a : Type), % 32.80/33.02 Eq % 32.80/33.02 (∀ (C B : Type) (R : a) (Q : B) (P : fun a (fun B C)), % 32.80/33.02 Eq (aa a C (combc a B C P Q) R) (aa B C (aa a (fun B C) P R) Q)) % 32.80/33.02 True % 32.80/33.02 Clause #9803 (by clausification #[9802]): ∀ (a a_1 : Type), % 32.80/33.02 Eq % 32.80/33.02 (∀ (B : Type) (R : a) (Q : B) (P : fun a (fun B a_1)), % 32.80/33.02 Eq (aa a a_1 (combc a B a_1 P Q) R) (aa B a_1 (aa a (fun B a_1) P R) Q)) % 32.80/33.02 True % 32.80/33.02 Clause #9804 (by clausification #[9803]): ∀ (a a_1 a_2 : Type), % 32.80/33.02 Eq % 32.80/33.02 (∀ (R : a) (Q : a_1) (P : fun a (fun a_1 a_2)), % 32.80/33.02 Eq (aa a a_2 (combc a a_1 a_2 P Q) R) (aa a_1 a_2 (aa a (fun a_1 a_2) P R) Q)) % 32.80/33.02 True % 32.80/33.02 Clause #9805 (by clausification #[9804]): ∀ (a a_1 a_2 : Type) (a_3 : a_1), % 32.80/33.02 Eq % 32.80/33.02 (∀ (Q : a) (P : fun a_1 (fun a a_2)), % 32.80/33.02 Eq (aa a_1 a_2 (combc a_1 a a_2 P Q) a_3) (aa a a_2 (aa a_1 (fun a a_2) P a_3) Q)) % 32.80/33.02 True % 32.80/33.02 Clause #9806 (by clausification #[9805]): ∀ (a a_1 a_2 : Type) (a_3 : a_1) (a_4 : a), % 32.80/33.02 Eq % 32.80/33.02 (∀ (P : fun a (fun a_1 a_2)), Eq (aa a a_2 (combc a a_1 a_2 P a_3) a_4) (aa a_1 a_2 (aa a (fun a_1 a_2) P a_4) a_3)) % 32.80/33.02 True % 32.80/33.02 Clause #9807 (by clausification #[9806]): ∀ (a a_1 a_2 : Type) (a_3 : fun a_1 (fun a_2 a)) (a_4 : a_2) (a_5 : a_1), % 32.80/33.02 Eq (Eq (aa a_1 a (combc a_1 a_2 a a_3 a_4) a_5) (aa a_2 a (aa a_1 (fun a_2 a) a_3 a_5) a_4)) True % 32.80/33.02 Clause #9808 (by clausification #[9807]): ∀ (a a_1 a_2 : Type) (a_3 : fun a_1 (fun a_2 a)) (a_4 : a_2) (a_5 : a_1), % 32.80/33.02 Eq (aa a_1 a (combc a_1 a_2 a a_3 a_4) a_5) (aa a_2 a (aa a_1 (fun a_2 a) a_3 a_5) a_4) % 32.80/33.02 Clause #9948 (by forward demodulation #[114, 9808]): Eq % 32.80/33.02 (pp % 32.80/33.02 (aa (fun (hoare_28830079triple a) bool) bool % 32.80/33.02 (combc (fun (hoare_28830079triple a) bool) (fun (hoare_28830079triple a) bool) bool % 32.80/33.02 (ord_less_eq (fun (hoare_28830079triple a) bool)) ts) % 32.80/33.02 tsa)) % 32.80/33.02 True % 32.80/33.02 Clause #9949 (by forward demodulation #[9948, 3944]): Eq (pp (aa (fun (hoare_28830079triple a) bool) bool (pow (hoare_28830079triple a) ts) tsa)) True % 32.80/33.02 Clause #10170 (by clausification #[130]): ∀ (a_1 : fun (hoare_28830079triple a) bool), % 32.80/33.02 Or % 32.80/33.02 (Eq % 32.80/33.02 (pp % 32.80/33.02 (aa (fun (hoare_28830079triple a) bool) bool % 32.80/33.02 (aa (fun (hoare_28830079triple a) bool) (fun (fun (hoare_28830079triple a) bool) bool) % 32.80/33.02 (ord_less_eq (fun (hoare_28830079triple a) bool)) a_1) % 32.80/33.02 ts)) % 32.80/33.02 False) % 32.87/33.07 (Eq (hoare_992312373derivs a ga a_1) True) % 32.87/33.07 Clause #10171 (by forward demodulation #[10170, 9808]): ∀ (a_1 : fun (hoare_28830079triple a) bool), % 32.87/33.07 Or % 32.87/33.07 (Eq % 32.87/33.07 (pp % 32.87/33.07 (aa (fun (hoare_28830079triple a) bool) bool % 32.87/33.07 (combc (fun (hoare_28830079triple a) bool) (fun (hoare_28830079triple a) bool) bool % 32.87/33.07 (ord_less_eq (fun (hoare_28830079triple a) bool)) ts) % 32.87/33.07 a_1)) % 32.87/33.07 False) % 32.87/33.07 (Eq (hoare_992312373derivs a ga a_1) True) % 32.87/33.07 Clause #10172 (by forward demodulation #[10171, 3944]): ∀ (a_1 : fun (hoare_28830079triple a) bool), % 32.87/33.07 Or (Eq (pp (aa (fun (hoare_28830079triple a) bool) bool (pow (hoare_28830079triple a) ts) a_1)) False) % 32.87/33.07 (Eq (hoare_992312373derivs a ga a_1) True) % 32.87/33.07 Clause #10175 (by superposition #[10172, 9949]): Or (Eq (hoare_992312373derivs a ga tsa) True) (Eq False True) % 32.87/33.07 Clause #10177 (by clausification #[10175]): Eq (hoare_992312373derivs a ga tsa) True % 32.87/33.07 Clause #10178 (by superposition #[10177, 123]): Eq True False % 32.87/33.07 Clause #10181 (by clausification #[10178]): False % 32.87/33.07 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------