%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SET789+4 : TPTP v9.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n004.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:00:30 PM UTC 2025 % Result : Theorem 82.95s 83.14s % Output : Proof 83.13s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SET789+4 : TPTP v9.2.0. Released v3.2.0. % 0.07/0.14 % Command : duper %s % 0.14/0.35 % Computer : n004.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Thu Oct 2 14:56:08 EDT 2025 % 0.14/0.35 % CPUTime : % 82.95/83.14 SZS status Theorem for theBenchmark.p % 82.95/83.14 SZS output start Proof for theBenchmark.p % 82.95/83.14 Clause #0 (by assumption #[]): Eq % 82.95/83.14 (∀ (R E : Iota), % 82.95/83.14 Iff (order R E) % 82.95/83.14 (And % 82.95/83.14 (And (∀ (X : Iota), member X E → apply R X X) % 82.95/83.14 (∀ (X Y : Iota), And (member X E) (member Y E) → And (apply R X Y) (apply R Y X) → Eq X Y)) % 82.95/83.14 (∀ (X Y Z : Iota), % 82.95/83.14 And (And (member X E) (member Y E)) (member Z E) → And (apply R X Y) (apply R Y Z) → apply R X Z))) % 82.95/83.14 True % 82.95/83.14 Clause #4 (by assumption #[]): Eq (∀ (R E M : Iota), Iff (greatest M R E) (And (member M E) (∀ (X : Iota), member X E → apply R X M))) True % 82.95/83.14 Clause #10 (by assumption #[]): Eq (Not (∀ (R E M : Iota), And (order R E) (greatest M R E) → ∀ (X : Iota), greatest X R E → Eq M X)) True % 82.95/83.14 Clause #11 (by clausification #[10]): Eq (∀ (R E M : Iota), And (order R E) (greatest M R E) → ∀ (X : Iota), greatest X R E → Eq M X) False % 82.95/83.14 Clause #12 (by clausification #[11]): ∀ (a : Iota), % 82.95/83.14 Eq % 82.95/83.14 (Not % 82.95/83.14 (∀ (E M : Iota), % 82.95/83.14 And (order (skS.0 0 a) E) (greatest M (skS.0 0 a) E) → ∀ (X : Iota), greatest X (skS.0 0 a) E → Eq M X)) % 82.95/83.14 True % 82.95/83.14 Clause #13 (by clausification #[12]): ∀ (a : Iota), % 82.95/83.14 Eq % 82.95/83.14 (∀ (E M : Iota), % 82.95/83.14 And (order (skS.0 0 a) E) (greatest M (skS.0 0 a) E) → ∀ (X : Iota), greatest X (skS.0 0 a) E → Eq M X) % 82.95/83.14 False % 82.95/83.14 Clause #14 (by clausification #[13]): ∀ (a a_1 : Iota), % 82.95/83.14 Eq % 82.95/83.14 (Not % 82.95/83.14 (∀ (M : Iota), % 82.95/83.14 And (order (skS.0 0 a) (skS.0 1 a a_1)) (greatest M (skS.0 0 a) (skS.0 1 a a_1)) → % 82.95/83.14 ∀ (X : Iota), greatest X (skS.0 0 a) (skS.0 1 a a_1) → Eq M X)) % 82.95/83.14 True % 82.95/83.14 Clause #15 (by clausification #[14]): ∀ (a a_1 : Iota), % 82.95/83.14 Eq % 82.95/83.14 (∀ (M : Iota), % 82.95/83.14 And (order (skS.0 0 a) (skS.0 1 a a_1)) (greatest M (skS.0 0 a) (skS.0 1 a a_1)) → % 82.95/83.14 ∀ (X : Iota), greatest X (skS.0 0 a) (skS.0 1 a a_1) → Eq M X) % 82.95/83.14 False % 82.95/83.14 Clause #16 (by clausification #[15]): ∀ (a a_1 a_2 : Iota), % 82.95/83.14 Eq % 82.95/83.14 (Not % 82.95/83.14 (And (order (skS.0 0 a) (skS.0 1 a a_1)) (greatest (skS.0 2 a a_1 a_2) (skS.0 0 a) (skS.0 1 a a_1)) → % 82.95/83.14 ∀ (X : Iota), greatest X (skS.0 0 a) (skS.0 1 a a_1) → Eq (skS.0 2 a a_1 a_2) X)) % 82.95/83.14 True % 82.95/83.14 Clause #17 (by clausification #[16]): ∀ (a a_1 a_2 : Iota), % 82.95/83.14 Eq % 82.95/83.14 (And (order (skS.0 0 a) (skS.0 1 a a_1)) (greatest (skS.0 2 a a_1 a_2) (skS.0 0 a) (skS.0 1 a a_1)) → % 82.95/83.14 ∀ (X : Iota), greatest X (skS.0 0 a) (skS.0 1 a a_1) → Eq (skS.0 2 a a_1 a_2) X) % 82.95/83.14 False % 82.95/83.14 Clause #18 (by clausification #[17]): ∀ (a a_1 a_2 : Iota), % 82.95/83.14 Eq (And (order (skS.0 0 a) (skS.0 1 a a_1)) (greatest (skS.0 2 a a_1 a_2) (skS.0 0 a) (skS.0 1 a a_1))) True % 82.95/83.14 Clause #19 (by clausification #[17]): ∀ (a a_1 a_2 : Iota), Eq (∀ (X : Iota), greatest X (skS.0 0 a) (skS.0 1 a a_1) → Eq (skS.0 2 a a_1 a_2) X) False % 82.95/83.14 Clause #20 (by clausification #[18]): ∀ (a a_1 a_2 : Iota), Eq (greatest (skS.0 2 a a_1 a_2) (skS.0 0 a) (skS.0 1 a a_1)) True % 82.95/83.14 Clause #21 (by clausification #[18]): ∀ (a a_1 : Iota), Eq (order (skS.0 0 a) (skS.0 1 a a_1)) True % 82.95/83.14 Clause #44 (by clausification #[0]): ∀ (a : Iota), % 82.95/83.14 Eq % 82.95/83.14 (∀ (E : Iota), % 82.95/83.14 Iff (order a E) % 82.95/83.14 (And % 82.95/83.14 (And (∀ (X : Iota), member X E → apply a X X) % 82.95/83.14 (∀ (X Y : Iota), And (member X E) (member Y E) → And (apply a X Y) (apply a Y X) → Eq X Y)) % 82.95/83.14 (∀ (X Y Z : Iota), % 82.95/83.14 And (And (member X E) (member Y E)) (member Z E) → And (apply a X Y) (apply a Y Z) → apply a X Z))) % 82.95/83.14 True % 82.95/83.14 Clause #45 (by clausification #[44]): ∀ (a a_1 : Iota), % 82.95/83.14 Eq % 82.95/83.14 (Iff (order a a_1) % 82.95/83.14 (And % 82.95/83.14 (And (∀ (X : Iota), member X a_1 → apply a X X) % 82.95/83.14 (∀ (X Y : Iota), And (member X a_1) (member Y a_1) → And (apply a X Y) (apply a Y X) → Eq X Y)) % 82.95/83.14 (∀ (X Y Z : Iota), % 82.95/83.14 And (And (member X a_1) (member Y a_1)) (member Z a_1) → And (apply a X Y) (apply a Y Z) → apply a X Z))) % 82.95/83.14 True % 82.95/83.14 Clause #47 (by clausification #[45]): ∀ (a a_1 : Iota), % 82.95/83.14 Or (Eq (order a a_1) False) % 82.95/83.14 (Eq % 82.95/83.14 (And % 82.95/83.14 (And (∀ (X : Iota), member X a_1 → apply a X X) % 82.95/83.14 (∀ (X Y : Iota), And (member X a_1) (member Y a_1) → And (apply a X Y) (apply a Y X) → Eq X Y)) % 83.00/83.16 (∀ (X Y Z : Iota), % 83.00/83.16 And (And (member X a_1) (member Y a_1)) (member Z a_1) → And (apply a X Y) (apply a Y Z) → apply a X Z)) % 83.00/83.16 True) % 83.00/83.16 Clause #72 (by clausification #[19]): ∀ (a a_1 a_2 a_3 : Iota), % 83.00/83.16 Eq % 83.00/83.16 (Not % 83.00/83.16 (greatest (skS.0 11 a a_1 a_2 a_3) (skS.0 0 a) (skS.0 1 a a_1) → Eq (skS.0 2 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3))) % 83.00/83.16 True % 83.00/83.16 Clause #73 (by clausification #[72]): ∀ (a a_1 a_2 a_3 : Iota), % 83.00/83.16 Eq (greatest (skS.0 11 a a_1 a_2 a_3) (skS.0 0 a) (skS.0 1 a a_1) → Eq (skS.0 2 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3)) % 83.00/83.16 False % 83.00/83.16 Clause #74 (by clausification #[73]): ∀ (a a_1 a_2 a_3 : Iota), Eq (greatest (skS.0 11 a a_1 a_2 a_3) (skS.0 0 a) (skS.0 1 a a_1)) True % 83.00/83.16 Clause #75 (by clausification #[73]): ∀ (a a_1 a_2 a_3 : Iota), Eq (Eq (skS.0 2 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3)) False % 83.00/83.16 Clause #155 (by clausification #[4]): ∀ (a : Iota), Eq (∀ (E M : Iota), Iff (greatest M a E) (And (member M E) (∀ (X : Iota), member X E → apply a X M))) True % 83.00/83.16 Clause #156 (by clausification #[155]): ∀ (a a_1 : Iota), % 83.00/83.16 Eq (∀ (M : Iota), Iff (greatest M a a_1) (And (member M a_1) (∀ (X : Iota), member X a_1 → apply a X M))) True % 83.00/83.16 Clause #157 (by clausification #[156]): ∀ (a a_1 a_2 : Iota), % 83.00/83.16 Eq (Iff (greatest a a_1 a_2) (And (member a a_2) (∀ (X : Iota), member X a_2 → apply a_1 X a))) True % 83.00/83.16 Clause #159 (by clausification #[157]): ∀ (a a_1 a_2 : Iota), % 83.00/83.16 Or (Eq (greatest a a_1 a_2) False) (Eq (And (member a a_2) (∀ (X : Iota), member X a_2 → apply a_1 X a)) True) % 83.00/83.16 Clause #170 (by clausification #[159]): ∀ (a a_1 a_2 : Iota), Or (Eq (greatest a a_1 a_2) False) (Eq (∀ (X : Iota), member X a_2 → apply a_1 X a) True) % 83.00/83.16 Clause #171 (by clausification #[159]): ∀ (a a_1 a_2 : Iota), Or (Eq (greatest a a_1 a_2) False) (Eq (member a a_2) True) % 83.00/83.16 Clause #172 (by clausification #[170]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (greatest a a_1 a_2) False) (Eq (member a_3 a_2 → apply a_1 a_3 a) True) % 83.00/83.16 Clause #173 (by clausification #[172]): ∀ (a a_1 a_2 a_3 : Iota), % 83.00/83.16 Or (Eq (greatest a a_1 a_2) False) (Or (Eq (member a_3 a_2) False) (Eq (apply a_1 a_3 a) True)) % 83.00/83.16 Clause #174 (by superposition #[173, 20]): ∀ (a a_1 a_2 a_3 : Iota), % 83.00/83.16 Or (Eq (member a (skS.0 1 a_1 a_2)) False) % 83.00/83.16 (Or (Eq (apply (skS.0 0 a_1) a (skS.0 2 a_1 a_2 a_3)) True) (Eq False True)) % 83.00/83.16 Clause #175 (by superposition #[173, 74]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 83.00/83.16 Or (Eq (member a (skS.0 1 a_1 a_2)) False) % 83.00/83.16 (Or (Eq (apply (skS.0 0 a_1) a (skS.0 11 a_1 a_2 a_3 a_4)) True) (Eq False True)) % 83.00/83.16 Clause #176 (by superposition #[171, 20]): ∀ (a a_1 a_2 : Iota), Or (Eq (member (skS.0 2 a a_1 a_2) (skS.0 1 a a_1)) True) (Eq False True) % 83.00/83.16 Clause #177 (by superposition #[171, 74]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (member (skS.0 11 a a_1 a_2 a_3) (skS.0 1 a a_1)) True) (Eq False True) % 83.00/83.16 Clause #238 (by clausification #[176]): ∀ (a a_1 a_2 : Iota), Eq (member (skS.0 2 a a_1 a_2) (skS.0 1 a a_1)) True % 83.00/83.16 Clause #246 (by clausification #[47]): ∀ (a a_1 : Iota), % 83.00/83.16 Or (Eq (order a a_1) False) % 83.00/83.16 (Eq % 83.00/83.16 (And (∀ (X : Iota), member X a_1 → apply a X X) % 83.00/83.16 (∀ (X Y : Iota), And (member X a_1) (member Y a_1) → And (apply a X Y) (apply a Y X) → Eq X Y)) % 83.00/83.16 True) % 83.00/83.16 Clause #256 (by clausification #[246]): ∀ (a a_1 : Iota), % 83.00/83.16 Or (Eq (order a a_1) False) % 83.00/83.16 (Eq (∀ (X Y : Iota), And (member X a_1) (member Y a_1) → And (apply a X Y) (apply a Y X) → Eq X Y) True) % 83.00/83.16 Clause #258 (by clausification #[256]): ∀ (a a_1 a_2 : Iota), % 83.00/83.16 Or (Eq (order a a_1) False) % 83.00/83.16 (Eq (∀ (Y : Iota), And (member a_2 a_1) (member Y a_1) → And (apply a a_2 Y) (apply a Y a_2) → Eq a_2 Y) True) % 83.00/83.16 Clause #259 (by clausification #[258]): ∀ (a a_1 a_2 a_3 : Iota), % 83.00/83.16 Or (Eq (order a a_1) False) % 83.00/83.16 (Eq (And (member a_2 a_1) (member a_3 a_1) → And (apply a a_2 a_3) (apply a a_3 a_2) → Eq a_2 a_3) True) % 83.00/83.16 Clause #260 (by clausification #[259]): ∀ (a a_1 a_2 a_3 : Iota), % 83.00/83.16 Or (Eq (order a a_1) False) % 83.00/83.16 (Or (Eq (And (member a_2 a_1) (member a_3 a_1)) False) % 83.00/83.16 (Eq (And (apply a a_2 a_3) (apply a a_3 a_2) → Eq a_2 a_3) True)) % 83.00/83.19 Clause #261 (by clausification #[260]): ∀ (a a_1 a_2 a_3 : Iota), % 83.00/83.19 Or (Eq (order a a_1) False) % 83.00/83.19 (Or (Eq (And (apply a a_2 a_3) (apply a a_3 a_2) → Eq a_2 a_3) True) % 83.00/83.19 (Or (Eq (member a_2 a_1) False) (Eq (member a_3 a_1) False))) % 83.00/83.19 Clause #262 (by clausification #[261]): ∀ (a a_1 a_2 a_3 : Iota), % 83.00/83.19 Or (Eq (order a a_1) False) % 83.00/83.19 (Or (Eq (member a_2 a_1) False) % 83.00/83.19 (Or (Eq (member a_3 a_1) False) (Or (Eq (And (apply a a_2 a_3) (apply a a_3 a_2)) False) (Eq (Eq a_2 a_3) True)))) % 83.00/83.19 Clause #263 (by clausification #[262]): ∀ (a a_1 a_2 a_3 : Iota), % 83.00/83.19 Or (Eq (order a a_1) False) % 83.00/83.19 (Or (Eq (member a_2 a_1) False) % 83.00/83.19 (Or (Eq (member a_3 a_1) False) % 83.00/83.19 (Or (Eq (Eq a_2 a_3) True) (Or (Eq (apply a a_2 a_3) False) (Eq (apply a a_3 a_2) False))))) % 83.00/83.19 Clause #264 (by clausification #[263]): ∀ (a a_1 a_2 a_3 : Iota), % 83.00/83.19 Or (Eq (order a a_1) False) % 83.00/83.19 (Or (Eq (member a_2 a_1) False) % 83.00/83.19 (Or (Eq (member a_3 a_1) False) (Or (Eq (apply a a_2 a_3) False) (Or (Eq (apply a a_3 a_2) False) (Eq a_2 a_3))))) % 83.00/83.19 Clause #265 (by superposition #[264, 21]): ∀ (a a_1 a_2 a_3 : Iota), % 83.00/83.19 Or (Eq (member a (skS.0 1 a_1 a_2)) False) % 83.00/83.19 (Or (Eq (member a_3 (skS.0 1 a_1 a_2)) False) % 83.00/83.19 (Or (Eq (apply (skS.0 0 a_1) a a_3) False) % 83.00/83.19 (Or (Eq (apply (skS.0 0 a_1) a_3 a) False) (Or (Eq a a_3) (Eq False True))))) % 83.00/83.19 Clause #276 (by clausification #[177]): ∀ (a a_1 a_2 a_3 : Iota), Eq (member (skS.0 11 a a_1 a_2 a_3) (skS.0 1 a a_1)) True % 83.00/83.19 Clause #327 (by clausification #[75]): ∀ (a a_1 a_2 a_3 : Iota), Ne (skS.0 2 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3) % 83.00/83.19 Clause #387 (by clausification #[174]): ∀ (a a_1 a_2 a_3 : Iota), % 83.00/83.19 Or (Eq (member a (skS.0 1 a_1 a_2)) False) (Eq (apply (skS.0 0 a_1) a (skS.0 2 a_1 a_2 a_3)) True) % 83.00/83.19 Clause #389 (by superposition #[387, 276]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 83.00/83.19 Or (Eq (apply (skS.0 0 a) (skS.0 11 a a_1 a_2 a_3) (skS.0 2 a a_1 a_4)) True) (Eq False True) % 83.00/83.19 Clause #447 (by clausification #[389]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (apply (skS.0 0 a) (skS.0 11 a a_1 a_2 a_3) (skS.0 2 a a_1 a_4)) True % 83.00/83.19 Clause #484 (by clausification #[175]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 83.00/83.19 Or (Eq (member a (skS.0 1 a_1 a_2)) False) (Eq (apply (skS.0 0 a_1) a (skS.0 11 a_1 a_2 a_3 a_4)) True) % 83.00/83.19 Clause #485 (by superposition #[484, 238]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 83.00/83.19 Or (Eq (apply (skS.0 0 a) (skS.0 2 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4)) True) (Eq False True) % 83.00/83.19 Clause #539 (by clausification #[485]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (apply (skS.0 0 a) (skS.0 2 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4)) True % 83.00/83.19 Clause #542 (by clausification #[265]): ∀ (a a_1 a_2 a_3 : Iota), % 83.00/83.19 Or (Eq (member a (skS.0 1 a_1 a_2)) False) % 83.00/83.19 (Or (Eq (member a_3 (skS.0 1 a_1 a_2)) False) % 83.00/83.19 (Or (Eq (apply (skS.0 0 a_1) a a_3) False) (Or (Eq (apply (skS.0 0 a_1) a_3 a) False) (Eq a a_3)))) % 83.00/83.19 Clause #544 (by superposition #[542, 276]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 83.00/83.19 Or (Eq (member a (skS.0 1 a_1 a_2)) False) % 83.00/83.19 (Or (Eq (apply (skS.0 0 a_1) (skS.0 11 a_1 a_2 a_3 a_4) a) False) % 83.00/83.19 (Or (Eq (apply (skS.0 0 a_1) a (skS.0 11 a_1 a_2 a_3 a_4)) False) % 83.00/83.19 (Or (Eq (skS.0 11 a_1 a_2 a_3 a_4) a) (Eq False True)))) % 83.00/83.19 Clause #1784 (by clausification #[544]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 83.00/83.19 Or (Eq (member a (skS.0 1 a_1 a_2)) False) % 83.00/83.19 (Or (Eq (apply (skS.0 0 a_1) (skS.0 11 a_1 a_2 a_3 a_4) a) False) % 83.00/83.19 (Or (Eq (apply (skS.0 0 a_1) a (skS.0 11 a_1 a_2 a_3 a_4)) False) (Eq (skS.0 11 a_1 a_2 a_3 a_4) a))) % 83.00/83.19 Clause #1785 (by superposition #[1784, 238]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 83.00/83.19 Or (Eq (apply (skS.0 0 a) (skS.0 11 a a_1 a_2 a_3) (skS.0 2 a a_1 a_4)) False) % 83.00/83.19 (Or (Eq (apply (skS.0 0 a) (skS.0 2 a a_1 a_4) (skS.0 11 a a_1 a_2 a_3)) False) % 83.00/83.19 (Or (Eq (skS.0 11 a a_1 a_2 a_3) (skS.0 2 a a_1 a_4)) (Eq False True))) % 83.00/83.19 Clause #9528 (by clausification #[1785]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 83.00/83.19 Or (Eq (apply (skS.0 0 a) (skS.0 11 a a_1 a_2 a_3) (skS.0 2 a a_1 a_4)) False) % 83.00/83.19 (Or (Eq (apply (skS.0 0 a) (skS.0 2 a a_1 a_4) (skS.0 11 a a_1 a_2 a_3)) False) % 83.00/83.19 (Eq (skS.0 11 a a_1 a_2 a_3) (skS.0 2 a a_1 a_4))) % 83.13/83.29 Clause #9529 (by superposition #[9528, 447]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 83.13/83.29 Or (Eq (apply (skS.0 0 a) (skS.0 2 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4)) False) % 83.13/83.29 (Or (Eq (skS.0 11 a a_1 a_3 a_4) (skS.0 2 a a_1 a_2)) (Eq False True)) % 83.13/83.29 Clause #9530 (by clausification #[9529]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 83.13/83.29 Or (Eq (apply (skS.0 0 a) (skS.0 2 a a_1 a_2) (skS.0 11 a a_1 a_3 a_4)) False) % 83.13/83.29 (Eq (skS.0 11 a a_1 a_3 a_4) (skS.0 2 a a_1 a_2)) % 83.13/83.29 Clause #9531 (by superposition #[9530, 539]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (skS.0 11 a a_1 a_2 a_3) (skS.0 2 a a_1 a_4)) (Eq False True) % 83.13/83.29 Clause #9532 (by clausification #[9531]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (skS.0 11 a a_1 a_2 a_3) (skS.0 2 a a_1 a_4) % 83.13/83.29 Clause #9533 (by backward contextual literal cutting #[9532, 327]): False % 83.13/83.29 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------