%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SYO006^1 : TPTP v9.2.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n002.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:08:24 PM UTC 2025 % Result : Theorem 7.22s 7.41s % Output : Proof 7.30s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYO006^1 : TPTP v9.2.0. Released v3.7.0. % 0.07/0.13 % Command : duper %s % 0.13/0.34 % Computer : n002.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Fri Oct 3 14:32:53 EDT 2025 % 0.13/0.35 % CPUTime : % 7.22/7.41 SZS status Theorem for theBenchmark.p % 7.22/7.41 SZS output start Proof for theBenchmark.p % 7.22/7.41 Clause #0 (by assumption #[]): Eq (Eq leibeq fun U V => ∀ (Q : Prop → Prop), Q U → Q V) True % 7.22/7.41 Clause #1 (by assumption #[]): Eq (Not (∀ (A B : Prop), leibeq A B → Iff A B)) True % 7.22/7.41 Clause #2 (by clausification #[1]): Eq (∀ (A B : Prop), leibeq A B → Iff A B) False % 7.22/7.41 Clause #3 (by clausification #[2]): ∀ (a : Prop), Eq (Not (∀ (B : Prop), leibeq (skS.0 0 a) B → Iff (skS.0 0 a) B)) True % 7.22/7.41 Clause #4 (by clausification #[3]): ∀ (a : Prop), Eq (∀ (B : Prop), leibeq (skS.0 0 a) B → Iff (skS.0 0 a) B) False % 7.22/7.41 Clause #5 (by clausification #[4]): ∀ (a a_1 : Prop), Eq (Not (leibeq (skS.0 0 a) (skS.0 1 a a_1) → Iff (skS.0 0 a) (skS.0 1 a a_1))) True % 7.22/7.41 Clause #6 (by clausification #[5]): ∀ (a a_1 : Prop), Eq (leibeq (skS.0 0 a) (skS.0 1 a a_1) → Iff (skS.0 0 a) (skS.0 1 a a_1)) False % 7.22/7.41 Clause #7 (by clausification #[6]): ∀ (a a_1 : Prop), Eq (leibeq (skS.0 0 a) (skS.0 1 a a_1)) True % 7.22/7.41 Clause #8 (by clausification #[6]): ∀ (a a_1 : Prop), Eq (Iff (skS.0 0 a) (skS.0 1 a a_1)) False % 7.22/7.41 Clause #9 (by identity loobHoist #[7]): ∀ (a a_1 : Prop), Or (Eq (leibeq (skS.0 0 a) True) True) (Eq (skS.0 1 a a_1) False) % 7.22/7.41 Clause #10 (by identity boolHoist #[7]): ∀ (a a_1 : Prop), Or (Eq (leibeq (skS.0 0 a) False) True) (Eq (skS.0 1 a a_1) True) % 7.22/7.41 Clause #12 (by identity boolHoist #[9]): ∀ (a a_1 : Prop), Or (Eq (skS.0 1 a a_1) False) (Or (Eq (leibeq False True) True) (Eq (skS.0 0 a) True)) % 7.22/7.41 Clause #21 (by clausification #[0]): Eq leibeq fun U V => ∀ (Q : Prop → Prop), Q U → Q V % 7.22/7.41 Clause #22 (by argument congruence #[21]): ∀ (a : Prop), Eq (leibeq a) ((fun U V => ∀ (Q : Prop → Prop), Q U → Q V) a) % 7.22/7.41 Clause #24 (by betaEtaReduce #[22]): ∀ (a : Prop), Eq (leibeq a) fun V => ∀ (Q : Prop → Prop), Q a → Q V % 7.22/7.41 Clause #25 (by identity loobHoist #[24]): ∀ (a : Prop), Or (Eq (leibeq True) fun V => ∀ (Q : Prop → Prop), Q a → Q V) (Eq a False) % 7.22/7.41 Clause #26 (by identity boolHoist #[24]): ∀ (a : Prop), Or (Eq (leibeq False) fun V => ∀ (Q : Prop → Prop), Q a → Q V) (Eq a True) % 7.22/7.41 Clause #27 (by falseElim #[25]): Eq (leibeq True) fun V => ∀ (Q : Prop → Prop), Q True → Q V % 7.22/7.41 Clause #28 (by argument congruence #[27]): ∀ (a : Prop), Eq (leibeq True a) ((fun V => ∀ (Q : Prop → Prop), Q True → Q V) a) % 7.22/7.41 Clause #29 (by argument congruence #[26]): ∀ (a a_1 : Prop), Or (Eq (leibeq False a) ((fun V => ∀ (Q : Prop → Prop), Q a_1 → Q V) a)) (Eq a_1 True) % 7.22/7.41 Clause #32 (by clausification #[8]): ∀ (a a_1 : Prop), Or (Eq (skS.0 0 a) False) (Eq (skS.0 1 a a_1) False) % 7.22/7.41 Clause #33 (by clausification #[8]): ∀ (a a_1 : Prop), Or (Eq (skS.0 0 a) True) (Eq (skS.0 1 a a_1) True) % 7.22/7.41 Clause #34 (by identity loobHoist #[32]): ∀ (a a_1 : Prop), Or (Eq (skS.0 1 a a_1) False) (Or (Eq (skS.0 0 True) False) (Eq a False)) % 7.22/7.41 Clause #36 (by identity loobHoist #[34]): ∀ (a a_1 : Prop), Or (Eq (skS.0 0 True) False) (Or (Eq a False) (Or (Eq (skS.0 1 a True) False) (Eq a_1 False))) % 7.22/7.41 Clause #38 (by identity loobHoist #[36]): ∀ (a a_1 : Prop), % 7.22/7.41 Or (Eq (skS.0 0 True) False) (Or (Eq a False) (Or (Eq a_1 False) (Or (Eq (skS.0 1 True True) False) (Eq a False)))) % 7.22/7.41 Clause #40 (by eliminate duplicate literals #[38]): ∀ (a a_1 : Prop), Or (Eq (skS.0 0 True) False) (Or (Eq a False) (Or (Eq a_1 False) (Eq (skS.0 1 True True) False))) % 7.22/7.41 Clause #41 (by betaEtaReduce #[28]): ∀ (a : Prop), Eq (leibeq True a) (∀ (Q : Prop → Prop), Q True → Q a) % 7.22/7.41 Clause #43 (by identity boolHoist #[41]): ∀ (a : Prop), Or (Eq (leibeq True False) (∀ (Q : Prop → Prop), Q True → Q a)) (Eq a True) % 7.22/7.41 Clause #52 (by clausify Prop equality #[43]): ∀ (a : Prop), Or (Eq a True) (Or (Eq (leibeq True False) False) (Eq (∀ (Q : Prop → Prop), Q True → Q a) True)) % 7.22/7.41 Clause #54 (by identity loobHoist #[10]): ∀ (a a_1 : Prop), Or (Eq (skS.0 1 a a_1) True) (Or (Eq (leibeq True False) True) (Eq (skS.0 0 a) False)) % 7.22/7.41 Clause #56 (by identity loobHoist #[54]): ∀ (a a_1 : Prop), % 7.22/7.41 Or (Eq (leibeq True False) True) (Or (Eq (skS.0 0 a) False) (Or (Eq (skS.0 1 a True) True) (Eq a_1 False))) % 7.22/7.41 Clause #58 (by identity loobHoist #[56]): ∀ (a a_1 : Prop), % 7.22/7.44 Or (Eq (leibeq True False) True) % 7.22/7.44 (Or (Eq (skS.0 1 a True) True) (Or (Eq a_1 False) (Or (Eq (skS.0 0 True) False) (Eq a False)))) % 7.22/7.44 Clause #60 (by identity loobHoist #[58]): ∀ (a a_1 : Prop), % 7.22/7.44 Or (Eq (leibeq True False) True) % 7.22/7.44 (Or (Eq a False) % 7.22/7.44 (Or (Eq (skS.0 0 True) False) (Or (Eq a_1 False) (Or (Eq (skS.0 1 True True) True) (Eq a_1 False))))) % 7.22/7.44 Clause #62 (by eliminate duplicate literals #[60]): ∀ (a a_1 : Prop), % 7.22/7.44 Or (Eq (leibeq True False) True) % 7.22/7.44 (Or (Eq a False) (Or (Eq (skS.0 0 True) False) (Or (Eq a_1 False) (Eq (skS.0 1 True True) True)))) % 7.22/7.44 Clause #64 (by falseElim #[62]): ∀ (a : Prop), % 7.22/7.44 Or (Eq (leibeq True False) True) (Or (Eq (skS.0 0 True) False) (Or (Eq a False) (Eq (skS.0 1 True True) True))) % 7.22/7.44 Clause #66 (by betaEtaReduce #[29]): ∀ (a a_1 : Prop), Or (Eq (leibeq False a) (∀ (Q : Prop → Prop), Q a_1 → Q a)) (Eq a_1 True) % 7.22/7.44 Clause #67 (by identity loobHoist #[66]): ∀ (a a_1 : Prop), Or (Eq a True) (Or (Eq (leibeq False True) (∀ (Q : Prop → Prop), Q a → Q a_1)) (Eq a_1 False)) % 7.22/7.44 Clause #70 (by falseElim #[67]): ∀ (a : Prop), Or (Eq a True) (Eq (leibeq False True) (∀ (Q : Prop → Prop), Q a → Q True)) % 7.22/7.44 Clause #72 (by clausify Prop equality #[70]): ∀ (a : Prop), Or (Eq a True) (Or (Eq (leibeq False True) False) (Eq (∀ (Q : Prop → Prop), Q a → Q True) True)) % 7.22/7.44 Clause #88 (by identity loobHoist #[12]): ∀ (a a_1 : Prop), % 7.22/7.44 Or (Eq (leibeq False True) True) (Or (Eq (skS.0 0 a) True) (Or (Eq (skS.0 1 a True) False) (Eq a_1 False))) % 7.22/7.44 Clause #90 (by identity loobHoist #[88]): ∀ (a a_1 : Prop), % 7.22/7.44 Or (Eq (leibeq False True) True) % 7.22/7.44 (Or (Eq (skS.0 1 a True) False) (Or (Eq a_1 False) (Or (Eq (skS.0 0 True) True) (Eq a False)))) % 7.22/7.44 Clause #92 (by identity loobHoist #[90]): ∀ (a a_1 : Prop), % 7.22/7.44 Or (Eq (leibeq False True) True) % 7.22/7.44 (Or (Eq a False) % 7.22/7.44 (Or (Eq (skS.0 0 True) True) (Or (Eq a_1 False) (Or (Eq (skS.0 1 True True) False) (Eq a_1 False))))) % 7.22/7.44 Clause #94 (by eliminate duplicate literals #[92]): ∀ (a a_1 : Prop), % 7.22/7.44 Or (Eq (leibeq False True) True) % 7.22/7.44 (Or (Eq a False) (Or (Eq (skS.0 0 True) True) (Or (Eq a_1 False) (Eq (skS.0 1 True True) False)))) % 7.22/7.44 Clause #96 (by falseElim #[94]): ∀ (a : Prop), % 7.22/7.44 Or (Eq (leibeq False True) True) (Or (Eq (skS.0 0 True) True) (Or (Eq a False) (Eq (skS.0 1 True True) False))) % 7.22/7.44 Clause #128 (by clausification #[72]): ∀ (a : Prop) (a_1 : Prop → Prop), Or (Eq a True) (Or (Eq (leibeq False True) False) (Eq (a_1 a → a_1 True) True)) % 7.22/7.44 Clause #129 (by clausification #[128]): ∀ (a : Prop) (a_1 : Prop → Prop), % 7.22/7.44 Or (Eq a True) (Or (Eq (leibeq False True) False) (Or (Eq (a_1 a) False) (Eq (a_1 True) True))) % 7.22/7.44 Clause #131 (by identity boolHoist #[129]): ∀ (a : Prop) (a_1 : Prop → Prop), % 7.22/7.44 Or (Eq a True) (Or (Eq (leibeq False True) False) (Or (Eq (a_1 True) True) (Or (Eq (a_1 False) False) (Eq a True)))) % 7.22/7.44 Clause #132 (by clausification #[52]): ∀ (a : Prop) (a_1 : Prop → Prop), Or (Eq a True) (Or (Eq (leibeq True False) False) (Eq (a_1 True → a_1 a) True)) % 7.22/7.44 Clause #133 (by clausification #[132]): ∀ (a : Prop) (a_1 : Prop → Prop), % 7.22/7.44 Or (Eq a True) (Or (Eq (leibeq True False) False) (Or (Eq (a_1 True) False) (Eq (a_1 a) True))) % 7.22/7.44 Clause #135 (by identity boolHoist #[133]): ∀ (a : Prop) (a_1 : Prop → Prop), % 7.22/7.44 Or (Eq a True) (Or (Eq (leibeq True False) False) (Or (Eq (a_1 True) False) (Or (Eq (a_1 False) True) (Eq a True)))) % 7.22/7.44 Clause #199 (by identity loobHoist #[33]): ∀ (a a_1 : Prop), Or (Eq (skS.0 1 a a_1) True) (Or (Eq (skS.0 0 True) True) (Eq a False)) % 7.22/7.44 Clause #201 (by identity loobHoist #[199]): ∀ (a a_1 : Prop), Or (Eq (skS.0 0 True) True) (Or (Eq a False) (Or (Eq (skS.0 1 a True) True) (Eq a_1 False))) % 7.22/7.44 Clause #203 (by identity loobHoist #[201]): ∀ (a a_1 : Prop), % 7.22/7.44 Or (Eq (skS.0 0 True) True) (Or (Eq a False) (Or (Eq a_1 False) (Or (Eq (skS.0 1 True True) True) (Eq a False)))) % 7.22/7.44 Clause #205 (by eliminate duplicate literals #[203]): ∀ (a a_1 : Prop), Or (Eq (skS.0 0 True) True) (Or (Eq a False) (Or (Eq a_1 False) (Eq (skS.0 1 True True) True))) % 7.22/7.44 Clause #207 (by falseElim #[205]): ∀ (a : Prop), Or (Eq (skS.0 0 True) True) (Or (Eq a False) (Eq (skS.0 1 True True) True)) % 7.30/7.46 Clause #256 (by eliminate duplicate literals #[135]): ∀ (a : Prop) (a_1 : Prop → Prop), % 7.30/7.46 Or (Eq a True) (Or (Eq (leibeq True False) False) (Or (Eq (a_1 True) False) (Eq (a_1 False) True))) % 7.30/7.46 Clause #258 (by eliminate duplicate literals #[131]): ∀ (a : Prop) (a_1 : Prop → Prop), % 7.30/7.46 Or (Eq a True) (Or (Eq (leibeq False True) False) (Or (Eq (a_1 True) True) (Eq (a_1 False) False))) % 7.30/7.46 Clause #278 (by falseElim #[207]): Or (Eq (skS.0 0 True) True) (Eq (skS.0 1 True True) True) % 7.30/7.46 Clause #390 (by falseElim #[96]): Or (Eq (leibeq False True) True) (Or (Eq (skS.0 0 True) True) (Eq (skS.0 1 True True) False)) % 7.30/7.46 Clause #415 (by superposition #[390, 278]): Or (Eq (leibeq False True) True) (Or (Eq (skS.0 0 True) True) (Or (Eq (skS.0 0 True) True) (Eq False True))) % 7.30/7.46 Clause #416 (by clausification #[415]): Or (Eq (leibeq False True) True) (Or (Eq (skS.0 0 True) True) (Eq (skS.0 0 True) True)) % 7.30/7.46 Clause #417 (by eliminate duplicate literals #[416]): Or (Eq (leibeq False True) True) (Eq (skS.0 0 True) True) % 7.30/7.46 Clause #418 (by superposition #[417, 40]): ∀ (a a_1 : Prop), % 7.30/7.46 Or (Eq (leibeq False True) True) % 7.30/7.46 (Or (Eq True False) (Or (Eq a False) (Or (Eq a_1 False) (Eq (skS.0 1 True True) False)))) % 7.30/7.46 Clause #421 (by superposition #[417, 64]): ∀ (a : Prop), % 7.30/7.46 Or (Eq (leibeq False True) True) % 7.30/7.46 (Or (Eq (leibeq True False) True) (Or (Eq True False) (Or (Eq a False) (Eq (skS.0 1 True True) True)))) % 7.30/7.46 Clause #430 (by clausification #[418]): ∀ (a a_1 : Prop), Or (Eq (leibeq False True) True) (Or (Eq a False) (Or (Eq a_1 False) (Eq (skS.0 1 True True) False))) % 7.30/7.46 Clause #435 (by falseElim #[430]): ∀ (a : Prop), Or (Eq (leibeq False True) True) (Or (Eq a False) (Eq (skS.0 1 True True) False)) % 7.30/7.46 Clause #440 (by falseElim #[435]): Or (Eq (leibeq False True) True) (Eq (skS.0 1 True True) False) % 7.30/7.46 Clause #452 (by clausification #[421]): ∀ (a : Prop), % 7.30/7.46 Or (Eq (leibeq False True) True) (Or (Eq (leibeq True False) True) (Or (Eq a False) (Eq (skS.0 1 True True) True))) % 7.30/7.46 Clause #457 (by falseElim #[452]): Or (Eq (leibeq False True) True) (Or (Eq (leibeq True False) True) (Eq (skS.0 1 True True) True)) % 7.30/7.46 Clause #458 (by superposition #[457, 440]): Or (Eq (leibeq False True) True) (Or (Eq (leibeq True False) True) (Or (Eq (leibeq False True) True) (Eq True False))) % 7.30/7.46 Clause #459 (by clausification #[458]): Or (Eq (leibeq False True) True) (Or (Eq (leibeq True False) True) (Eq (leibeq False True) True)) % 7.30/7.46 Clause #460 (by eliminate duplicate literals #[459]): Or (Eq (leibeq False True) True) (Eq (leibeq True False) True) % 7.30/7.46 Clause #461 (by superposition #[460, 258]): ∀ (a : Prop) (a_1 : Prop → Prop), % 7.30/7.46 Or (Eq (leibeq True False) True) % 7.30/7.46 (Or (Eq a True) (Or (Eq True False) (Or (Eq (a_1 True) True) (Eq (a_1 False) False)))) % 7.30/7.46 Clause #462 (by clausification #[461]): ∀ (a : Prop) (a_1 : Prop → Prop), % 7.30/7.46 Or (Eq (leibeq True False) True) (Or (Eq a True) (Or (Eq (a_1 True) True) (Eq (a_1 False) False))) % 7.30/7.46 Clause #467 (by neHoist #[462]): ∀ (a : Prop) (a_1 : Prop → Sort _abstMVar.0) (a_2 a_3 : (x : Prop) → a_1 x), % 7.30/7.46 Or (Eq (leibeq True False) True) % 7.30/7.46 (Or (Eq a True) % 7.30/7.46 (Or (Eq ((fun x => Ne (a_2 x) (a_3 x)) True) True) (Or (Eq True False) (Eq (a_2 False) (a_3 False))))) % 7.30/7.46 Clause #589 (by betaEtaReduce #[467]): ∀ (a : Prop) (a_1 : Prop → Sort _abstMVar.0) (a_2 a_3 : (x : Prop) → a_1 x), % 7.30/7.46 Or (Eq (leibeq True False) True) % 7.30/7.46 (Or (Eq a True) (Or (Eq (Ne (a_2 True) (a_3 True)) True) (Or (Eq True False) (Eq (a_2 False) (a_3 False))))) % 7.30/7.46 Clause #590 (by clausification #[589]): ∀ (a : Prop) (a_1 : Prop → Sort _abstMVar.0) (a_2 a_3 : (x : Prop) → a_1 x), % 7.30/7.46 Or (Eq (leibeq True False) True) % 7.30/7.46 (Or (Eq a True) (Or (Eq True False) (Or (Eq (a_2 False) (a_3 False)) (Ne (a_2 True) (a_3 True))))) % 7.30/7.46 Clause #591 (by clausification #[590]): ∀ (a : Prop) (a_1 : Prop → Sort _abstMVar.0) (a_2 a_3 : (x : Prop) → a_1 x), % 7.30/7.46 Or (Eq (leibeq True False) True) (Or (Eq a True) (Or (Eq (a_2 False) (a_3 False)) (Ne (a_2 True) (a_3 True)))) % 7.30/7.46 Clause #592 (by equality resolution #[591]): ∀ (a : Prop), Or (Eq (leibeq True False) True) (Or (Eq a True) (Eq ((fun x => x) False) ((fun x => True) False))) % 7.30/7.50 Clause #623 (by betaEtaReduce #[592]): ∀ (a : Prop), Or (Eq (leibeq True False) True) (Or (Eq a True) (Eq False True)) % 7.30/7.50 Clause #624 (by clausification #[623]): ∀ (a : Prop), Or (Eq (leibeq True False) True) (Eq a True) % 7.30/7.50 Clause #633 (by equality factoring #[624]): Or (Ne True True) (Eq (leibeq True False) True) % 7.30/7.50 Clause #635 (by clausification #[633]): Or (Eq (leibeq True False) True) (Or (Eq True False) (Eq True False)) % 7.30/7.50 Clause #637 (by clausification #[635]): Or (Eq (leibeq True False) True) (Eq True False) % 7.30/7.50 Clause #638 (by clausification #[637]): Eq (leibeq True False) True % 7.30/7.50 Clause #643 (by superposition #[638, 256]): ∀ (a : Prop) (a_1 : Prop → Prop), Or (Eq a True) (Or (Eq True False) (Or (Eq (a_1 True) False) (Eq (a_1 False) True))) % 7.30/7.50 Clause #665 (by clausification #[643]): ∀ (a : Prop) (a_1 : Prop → Prop), Or (Eq a True) (Or (Eq (a_1 True) False) (Eq (a_1 False) True)) % 7.30/7.50 Clause #670 (by neHoist #[665]): ∀ (a : Prop) (a_1 : Prop → Sort _abstMVar.0) (a_2 a_3 : (x : Prop) → a_1 x), % 7.30/7.50 Or (Eq a True) (Or (Eq ((fun x => Ne (a_2 x) (a_3 x)) False) True) (Or (Eq True False) (Eq (a_2 True) (a_3 True)))) % 7.30/7.50 Clause #837 (by betaEtaReduce #[670]): ∀ (a : Prop) (a_1 : Prop → Sort _abstMVar.0) (a_2 a_3 : (x : Prop) → a_1 x), % 7.30/7.50 Or (Eq a True) (Or (Eq (Ne (a_2 False) (a_3 False)) True) (Or (Eq True False) (Eq (a_2 True) (a_3 True)))) % 7.30/7.50 Clause #838 (by clausification #[837]): ∀ (a : Prop) (a_1 : Prop → Sort _abstMVar.0) (a_2 a_3 : (x : Prop) → a_1 x), % 7.30/7.50 Or (Eq a True) (Or (Eq True False) (Or (Eq (a_2 True) (a_3 True)) (Ne (a_2 False) (a_3 False)))) % 7.30/7.50 Clause #839 (by clausification #[838]): ∀ (a : Prop) (a_1 : Prop → Sort _abstMVar.0) (a_2 a_3 : (x : Prop) → a_1 x), % 7.30/7.50 Or (Eq a True) (Or (Eq (a_2 True) (a_3 True)) (Ne (a_2 False) (a_3 False))) % 7.30/7.50 Clause #840 (by equality resolution #[839]): ∀ (a : Prop), Or (Eq a True) (Eq ((fun x => x) True) ((fun x => False) True)) % 7.30/7.50 Clause #863 (by betaEtaReduce #[840]): ∀ (a : Prop), Or (Eq a True) (Eq True False) % 7.30/7.50 Clause #864 (by clausification #[863]): ∀ (a : Prop), Eq a True % 7.30/7.50 Clause #866 (by falseElim #[864]): False % 7.30/7.50 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------