%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWW520_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n031.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 7.94s 8.12s % Output : Proof 7.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW520_5 : TPTP v9.2.0. Released v6.0.0. % 0.12/0.13 % Command : duper %s % 0.12/0.34 % Computer : n031.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 10:54:53 EDT 2025 % 0.19/0.34 % CPUTime : % 7.94/8.12 SZS status Theorem for theBenchmark.p % 7.94/8.12 SZS output start Proof for theBenchmark.p % 7.94/8.12 Clause #1 (by assumption #[]): Eq (∀ (B : Type) (A2 : fun B bool), Iff (∀ (X6 : B), Not (member B X6 A2)) (Eq A2 (bot_bot (fun B bool)))) True % 7.94/8.12 Clause #8 (by assumption #[]): Eq (∀ (B : Type), Eq (bot_bot (fun B bool)) (collect B (combk bool B fFalse))) True % 7.94/8.12 Clause #70 (by assumption #[]): Eq (∀ (B : Type) (P1 : fun B bool), Eq (collect B P1) P1) True % 7.94/8.12 Clause #119 (by assumption #[]): Eq % 7.94/8.12 (Not % 7.94/8.12 (∀ (N : nat), % 7.94/8.12 Or (Exists fun X1 => And (member (hoare_28830079triple a) X1 ga) (Not (hoare_1633586161_valid a N X1))) % 7.94/8.12 (∀ (X : hoare_28830079triple a), % 7.94/8.12 member (hoare_28830079triple a) X (bot_bot (fun (hoare_28830079triple a) bool)) → % 7.94/8.12 hoare_1633586161_valid a N X))) % 7.94/8.12 True % 7.94/8.12 Clause #124 (by clausification #[1]): ∀ (a : Type), Eq (∀ (A2 : fun a bool), Iff (∀ (X6 : a), Not (member a X6 A2)) (Eq A2 (bot_bot (fun a bool)))) True % 7.94/8.12 Clause #125 (by clausification #[124]): ∀ (a : Type) (a_1 : fun a bool), Eq (Iff (∀ (X6 : a), Not (member a X6 a_1)) (Eq a_1 (bot_bot (fun a bool)))) True % 7.94/8.12 Clause #126 (by clausification #[125]): ∀ (a : Type) (a_1 : fun a bool), % 7.94/8.12 Or (Eq (∀ (X6 : a), Not (member a X6 a_1)) True) (Eq (Eq a_1 (bot_bot (fun a bool))) False) % 7.94/8.12 Clause #128 (by clausification #[126]): ∀ (a : Type) (a_1 : fun a bool) (a_2 : a), % 7.94/8.12 Or (Eq (Eq a_1 (bot_bot (fun a bool))) False) (Eq (Not (member a a_2 a_1)) True) % 7.94/8.12 Clause #129 (by clausification #[128]): ∀ (a : Type) (a_1 : a) (a_2 : fun a bool), Or (Eq (Not (member a a_1 a_2)) True) (Ne a_2 (bot_bot (fun a bool))) % 7.94/8.12 Clause #130 (by clausification #[129]): ∀ (a : Type) (a_1 : fun a bool) (a_2 : a), Or (Ne a_1 (bot_bot (fun a bool))) (Eq (member a a_2 a_1) False) % 7.94/8.12 Clause #131 (by destructive equality resolution #[130]): ∀ (a : Type) (a_1 : a), Eq (member a a_1 (bot_bot (fun a bool))) False % 7.94/8.12 Clause #259 (by clausification #[8]): ∀ (a : Type), Eq (Eq (bot_bot (fun a bool)) (collect a (combk bool a fFalse))) True % 7.94/8.12 Clause #260 (by clausification #[259]): ∀ (a : Type), Eq (bot_bot (fun a bool)) (collect a (combk bool a fFalse)) % 7.94/8.12 Clause #554 (by clausification #[70]): ∀ (a : Type), Eq (∀ (P1 : fun a bool), Eq (collect a P1) P1) True % 7.94/8.12 Clause #555 (by clausification #[554]): ∀ (a : Type) (a_1 : fun a bool), Eq (Eq (collect a a_1) a_1) True % 7.94/8.12 Clause #556 (by clausification #[555]): ∀ (a : Type) (a_1 : fun a bool), Eq (collect a a_1) a_1 % 7.94/8.12 Clause #559 (by superposition #[556, 260]): ∀ (a : Type), Eq (bot_bot (fun a bool)) (combk bool a fFalse) % 7.94/8.12 Clause #560 (by backward demodulation #[559, 131]): ∀ (a : Type) (a_1 : a), Eq (member a a_1 (combk bool a fFalse)) False % 7.94/8.12 Clause #2524 (by clausification #[119]): Eq % 7.94/8.12 (∀ (N : nat), % 7.94/8.12 Or (Exists fun X1 => And (member (hoare_28830079triple a) X1 ga) (Not (hoare_1633586161_valid a N X1))) % 7.94/8.12 (∀ (X : hoare_28830079triple a), % 7.94/8.12 member (hoare_28830079triple a) X (bot_bot (fun (hoare_28830079triple a) bool)) → hoare_1633586161_valid a N X)) % 7.94/8.12 False % 7.94/8.12 Clause #2525 (by clausification #[2524]): ∀ (a_1 : nat), % 7.94/8.12 Eq % 7.94/8.12 (Not % 7.94/8.12 (Or % 7.94/8.12 (Exists fun X1 => % 7.94/8.12 And (member (hoare_28830079triple a) X1 ga) (Not (hoare_1633586161_valid a (skS.0 30 a_1) X1))) % 7.94/8.12 (∀ (X : hoare_28830079triple a), % 7.94/8.12 member (hoare_28830079triple a) X (bot_bot (fun (hoare_28830079triple a) bool)) → % 7.94/8.12 hoare_1633586161_valid a (skS.0 30 a_1) X))) % 7.94/8.12 True % 7.94/8.12 Clause #2526 (by clausification #[2525]): ∀ (a_1 : nat), % 7.94/8.12 Eq % 7.94/8.12 (Or % 7.94/8.12 (Exists fun X1 => And (member (hoare_28830079triple a) X1 ga) (Not (hoare_1633586161_valid a (skS.0 30 a_1) X1))) % 7.94/8.12 (∀ (X : hoare_28830079triple a), % 7.94/8.12 member (hoare_28830079triple a) X (bot_bot (fun (hoare_28830079triple a) bool)) → % 7.94/8.12 hoare_1633586161_valid a (skS.0 30 a_1) X)) % 7.94/8.12 False % 7.94/8.12 Clause #2527 (by clausification #[2526]): ∀ (a_1 : nat), % 7.94/8.12 Eq % 7.94/8.12 (∀ (X : hoare_28830079triple a), % 7.94/8.12 member (hoare_28830079triple a) X (bot_bot (fun (hoare_28830079triple a) bool)) → % 7.94/8.12 hoare_1633586161_valid a (skS.0 30 a_1) X) % 7.94/8.12 False % 7.94/8.12 Clause #2529 (by clausification #[2527]): ∀ (a_1 : nat) (a_2 : hoare_28830079triple a), % 7.94/8.14 Eq % 7.94/8.14 (Not % 7.94/8.14 (member (hoare_28830079triple a) (skS.0 31 a_1 a_2) (bot_bot (fun (hoare_28830079triple a) bool)) → % 7.94/8.14 hoare_1633586161_valid a (skS.0 30 a_1) (skS.0 31 a_1 a_2))) % 7.94/8.14 True % 7.94/8.14 Clause #2530 (by clausification #[2529]): ∀ (a_1 : nat) (a_2 : hoare_28830079triple a), % 7.94/8.14 Eq % 7.94/8.14 (member (hoare_28830079triple a) (skS.0 31 a_1 a_2) (bot_bot (fun (hoare_28830079triple a) bool)) → % 7.94/8.14 hoare_1633586161_valid a (skS.0 30 a_1) (skS.0 31 a_1 a_2)) % 7.94/8.14 False % 7.94/8.14 Clause #2531 (by clausification #[2530]): ∀ (a_1 : nat) (a_2 : hoare_28830079triple a), % 7.94/8.14 Eq (member (hoare_28830079triple a) (skS.0 31 a_1 a_2) (bot_bot (fun (hoare_28830079triple a) bool))) True % 7.94/8.14 Clause #2533 (by forward demodulation #[2531, 559]): ∀ (a_1 : nat) (a_2 : hoare_28830079triple a), % 7.94/8.14 Eq (member (hoare_28830079triple a) (skS.0 31 a_1 a_2) (combk bool (hoare_28830079triple a) fFalse)) True % 7.94/8.14 Clause #2534 (by superposition #[2533, 560]): Eq True False % 7.94/8.14 Clause #2566 (by clausification #[2534]): False % 7.94/8.14 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------