%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SCT255_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n016.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 07:59:18 PM UTC 2025 % Result : Theorem 3.66s 3.84s % Output : Proof 3.66s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SCT255_5 : TPTP v9.2.0. Released v6.0.0. % 0.11/0.14 % Command : duper %s % 0.14/0.35 % Computer : n016.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 21:12:38 EDT 2025 % 0.14/0.35 % CPUTime : % 3.66/3.84 SZS status Theorem for theBenchmark.p % 3.66/3.84 SZS output start Proof for theBenchmark.p % 3.66/3.84 Clause #0 (by assumption #[]): Eq (Ne c d) True % 3.66/3.84 Clause #1 (by assumption #[]): Eq % 3.66/3.84 (∀ (B1 A1 : arrow_411405190le_alt), % 3.66/3.84 Ne A1 B1 → % 3.66/3.84 Exists fun C2 => % 3.66/3.84 distinct arrow_411405190le_alt % 3.66/3.84 (cons arrow_411405190le_alt A1 % 3.66/3.84 (cons arrow_411405190le_alt B1 (cons arrow_411405190le_alt C2 (nil arrow_411405190le_alt))))) % 3.66/3.84 True % 3.66/3.84 Clause #110 (by assumption #[]): Eq % 3.66/3.84 (∀ (E : arrow_411405190le_alt), % 3.66/3.84 distinct arrow_411405190le_alt % 3.66/3.84 (cons arrow_411405190le_alt c % 3.66/3.84 (cons arrow_411405190le_alt d (cons arrow_411405190le_alt E (nil arrow_411405190le_alt)))) → % 3.66/3.84 thesis) % 3.66/3.84 True % 3.66/3.84 Clause #111 (by assumption #[]): Eq (Not thesis) True % 3.66/3.84 Clause #112 (by clausification #[111]): Eq thesis False % 3.66/3.84 Clause #113 (by clausification #[0]): Ne c d % 3.66/3.84 Clause #114 (by clausification #[1]): ∀ (a : arrow_411405190le_alt), % 3.66/3.84 Eq % 3.66/3.84 (∀ (A1 : arrow_411405190le_alt), % 3.66/3.84 Ne A1 a → % 3.66/3.84 Exists fun C2 => % 3.66/3.84 distinct arrow_411405190le_alt % 3.66/3.84 (cons arrow_411405190le_alt A1 % 3.66/3.84 (cons arrow_411405190le_alt a (cons arrow_411405190le_alt C2 (nil arrow_411405190le_alt))))) % 3.66/3.84 True % 3.66/3.84 Clause #115 (by clausification #[114]): ∀ (a a_1 : arrow_411405190le_alt), % 3.66/3.84 Eq % 3.66/3.84 (Ne a a_1 → % 3.66/3.84 Exists fun C2 => % 3.66/3.84 distinct arrow_411405190le_alt % 3.66/3.84 (cons arrow_411405190le_alt a % 3.66/3.84 (cons arrow_411405190le_alt a_1 (cons arrow_411405190le_alt C2 (nil arrow_411405190le_alt))))) % 3.66/3.84 True % 3.66/3.84 Clause #116 (by clausification #[115]): ∀ (a a_1 : arrow_411405190le_alt), % 3.66/3.84 Or (Eq (Ne a a_1) False) % 3.66/3.84 (Eq % 3.66/3.84 (Exists fun C2 => % 3.66/3.84 distinct arrow_411405190le_alt % 3.66/3.84 (cons arrow_411405190le_alt a % 3.66/3.84 (cons arrow_411405190le_alt a_1 (cons arrow_411405190le_alt C2 (nil arrow_411405190le_alt))))) % 3.66/3.84 True) % 3.66/3.84 Clause #117 (by clausification #[116]): ∀ (a a_1 : arrow_411405190le_alt), % 3.66/3.84 Or % 3.66/3.84 (Eq % 3.66/3.84 (Exists fun C2 => % 3.66/3.84 distinct arrow_411405190le_alt % 3.66/3.84 (cons arrow_411405190le_alt a % 3.66/3.84 (cons arrow_411405190le_alt a_1 (cons arrow_411405190le_alt C2 (nil arrow_411405190le_alt))))) % 3.66/3.84 True) % 3.66/3.84 (Eq a a_1) % 3.66/3.84 Clause #118 (by clausification #[117]): ∀ (a a_1 a_2 : arrow_411405190le_alt), % 3.66/3.84 Or (Eq a a_1) % 3.66/3.84 (Eq % 3.66/3.84 (distinct arrow_411405190le_alt % 3.66/3.84 (cons arrow_411405190le_alt a % 3.66/3.84 (cons arrow_411405190le_alt a_1 % 3.66/3.84 (cons arrow_411405190le_alt (skS.0 0 a a_1 a_2) (nil arrow_411405190le_alt))))) % 3.66/3.84 True) % 3.66/3.84 Clause #124 (by clausification #[110]): ∀ (a : arrow_411405190le_alt), % 3.66/3.84 Eq % 3.66/3.84 (distinct arrow_411405190le_alt % 3.66/3.84 (cons arrow_411405190le_alt c % 3.66/3.84 (cons arrow_411405190le_alt d (cons arrow_411405190le_alt a (nil arrow_411405190le_alt)))) → % 3.66/3.84 thesis) % 3.66/3.84 True % 3.66/3.84 Clause #125 (by clausification #[124]): ∀ (a : arrow_411405190le_alt), % 3.66/3.84 Or % 3.66/3.84 (Eq % 3.66/3.84 (distinct arrow_411405190le_alt % 3.66/3.84 (cons arrow_411405190le_alt c % 3.66/3.84 (cons arrow_411405190le_alt d (cons arrow_411405190le_alt a (nil arrow_411405190le_alt))))) % 3.66/3.84 False) % 3.66/3.84 (Eq thesis True) % 3.66/3.84 Clause #126 (by forward demodulation #[125, 112]): ∀ (a : arrow_411405190le_alt), % 3.66/3.84 Or % 3.66/3.84 (Eq % 3.66/3.84 (distinct arrow_411405190le_alt % 3.66/3.84 (cons arrow_411405190le_alt c % 3.66/3.84 (cons arrow_411405190le_alt d (cons arrow_411405190le_alt a (nil arrow_411405190le_alt))))) % 3.66/3.84 False) % 3.66/3.84 (Eq False True) % 3.66/3.84 Clause #127 (by clausification #[126]): ∀ (a : arrow_411405190le_alt), % 3.66/3.84 Eq % 3.66/3.84 (distinct arrow_411405190le_alt % 3.66/3.84 (cons arrow_411405190le_alt c % 3.66/3.84 (cons arrow_411405190le_alt d (cons arrow_411405190le_alt a (nil arrow_411405190le_alt))))) % 3.66/3.84 False % 3.66/3.84 Clause #128 (by superposition #[127, 118]): Or (Eq c d) (Eq False True) % 3.66/3.84 Clause #137 (by clausification #[128]): Eq c d % 3.66/3.84 Clause #138 (by forward contextual literal cutting #[137, 113]): False % 3.66/3.84 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------