%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SCT214_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n020.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:16 PM UTC 2025 % Result : Theorem 3.68s 3.83s % Output : Proof 3.68s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SCT214_5 : TPTP v9.2.0. Released v6.0.0. % 0.11/0.13 % Command : duper %s % 0.13/0.34 % Computer : n020.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 : Thu Oct 2 21:03:53 EDT 2025 % 0.13/0.34 % CPUTime : % 3.68/3.83 SZS status Theorem for theBenchmark.p % 3.68/3.83 SZS output start Proof for theBenchmark.p % 3.68/3.83 Clause #0 (by assumption #[]): Eq (Ne a b) True % 3.68/3.83 Clause #5 (by assumption #[]): Eq % 3.68/3.83 (∀ (B3 A4 : arrow_411405190le_alt), % 3.68/3.83 Ne A4 B3 → % 3.68/3.83 Exists fun C3 => % 3.68/3.83 distinct arrow_411405190le_alt % 3.68/3.83 (cons arrow_411405190le_alt A4 % 3.68/3.83 (cons arrow_411405190le_alt B3 (cons arrow_411405190le_alt C3 (nil arrow_411405190le_alt))))) % 3.68/3.83 True % 3.68/3.83 Clause #100 (by assumption #[]): Eq % 3.68/3.83 (∀ (C : arrow_411405190le_alt), % 3.68/3.83 distinct arrow_411405190le_alt % 3.68/3.83 (cons arrow_411405190le_alt a % 3.68/3.83 (cons arrow_411405190le_alt b (cons arrow_411405190le_alt C (nil arrow_411405190le_alt)))) → % 3.68/3.83 thesis) % 3.68/3.83 True % 3.68/3.83 Clause #101 (by assumption #[]): Eq (Not thesis) True % 3.68/3.83 Clause #102 (by clausification #[101]): Eq thesis False % 3.68/3.83 Clause #104 (by clausification #[0]): Ne a b % 3.68/3.83 Clause #105 (by clausification #[100]): ∀ (a_1 : arrow_411405190le_alt), % 3.68/3.83 Eq % 3.68/3.83 (distinct arrow_411405190le_alt % 3.68/3.83 (cons arrow_411405190le_alt a % 3.68/3.83 (cons arrow_411405190le_alt b (cons arrow_411405190le_alt a_1 (nil arrow_411405190le_alt)))) → % 3.68/3.83 thesis) % 3.68/3.83 True % 3.68/3.83 Clause #106 (by clausification #[105]): ∀ (a_1 : arrow_411405190le_alt), % 3.68/3.83 Or % 3.68/3.83 (Eq % 3.68/3.83 (distinct arrow_411405190le_alt % 3.68/3.83 (cons arrow_411405190le_alt a % 3.68/3.83 (cons arrow_411405190le_alt b (cons arrow_411405190le_alt a_1 (nil arrow_411405190le_alt))))) % 3.68/3.83 False) % 3.68/3.83 (Eq thesis True) % 3.68/3.83 Clause #107 (by forward demodulation #[106, 102]): ∀ (a_1 : arrow_411405190le_alt), % 3.68/3.83 Or % 3.68/3.83 (Eq % 3.68/3.83 (distinct arrow_411405190le_alt % 3.68/3.83 (cons arrow_411405190le_alt a % 3.68/3.83 (cons arrow_411405190le_alt b (cons arrow_411405190le_alt a_1 (nil arrow_411405190le_alt))))) % 3.68/3.83 False) % 3.68/3.83 (Eq False True) % 3.68/3.83 Clause #108 (by clausification #[107]): ∀ (a_1 : arrow_411405190le_alt), % 3.68/3.83 Eq % 3.68/3.83 (distinct arrow_411405190le_alt % 3.68/3.83 (cons arrow_411405190le_alt a % 3.68/3.83 (cons arrow_411405190le_alt b (cons arrow_411405190le_alt a_1 (nil arrow_411405190le_alt))))) % 3.68/3.83 False % 3.68/3.83 Clause #136 (by clausification #[5]): ∀ (a : arrow_411405190le_alt), % 3.68/3.83 Eq % 3.68/3.83 (∀ (A4 : arrow_411405190le_alt), % 3.68/3.83 Ne A4 a → % 3.68/3.83 Exists fun C3 => % 3.68/3.83 distinct arrow_411405190le_alt % 3.68/3.83 (cons arrow_411405190le_alt A4 % 3.68/3.83 (cons arrow_411405190le_alt a (cons arrow_411405190le_alt C3 (nil arrow_411405190le_alt))))) % 3.68/3.83 True % 3.68/3.83 Clause #137 (by clausification #[136]): ∀ (a a_1 : arrow_411405190le_alt), % 3.68/3.83 Eq % 3.68/3.83 (Ne a a_1 → % 3.68/3.83 Exists fun C3 => % 3.68/3.83 distinct arrow_411405190le_alt % 3.68/3.83 (cons arrow_411405190le_alt a % 3.68/3.83 (cons arrow_411405190le_alt a_1 (cons arrow_411405190le_alt C3 (nil arrow_411405190le_alt))))) % 3.68/3.83 True % 3.68/3.83 Clause #138 (by clausification #[137]): ∀ (a a_1 : arrow_411405190le_alt), % 3.68/3.83 Or (Eq (Ne a a_1) False) % 3.68/3.83 (Eq % 3.68/3.83 (Exists fun C3 => % 3.68/3.83 distinct arrow_411405190le_alt % 3.68/3.83 (cons arrow_411405190le_alt a % 3.68/3.83 (cons arrow_411405190le_alt a_1 (cons arrow_411405190le_alt C3 (nil arrow_411405190le_alt))))) % 3.68/3.83 True) % 3.68/3.83 Clause #139 (by clausification #[138]): ∀ (a a_1 : arrow_411405190le_alt), % 3.68/3.83 Or % 3.68/3.83 (Eq % 3.68/3.83 (Exists fun C3 => % 3.68/3.83 distinct arrow_411405190le_alt % 3.68/3.83 (cons arrow_411405190le_alt a % 3.68/3.83 (cons arrow_411405190le_alt a_1 (cons arrow_411405190le_alt C3 (nil arrow_411405190le_alt))))) % 3.68/3.83 True) % 3.68/3.83 (Eq a a_1) % 3.68/3.83 Clause #140 (by clausification #[139]): ∀ (a a_1 a_2 : arrow_411405190le_alt), % 3.68/3.83 Or (Eq a a_1) % 3.68/3.83 (Eq % 3.68/3.83 (distinct arrow_411405190le_alt % 3.68/3.83 (cons arrow_411405190le_alt a % 3.68/3.83 (cons arrow_411405190le_alt a_1 % 3.68/3.83 (cons arrow_411405190le_alt (skS.0 0 a a_1 a_2) (nil arrow_411405190le_alt))))) % 3.68/3.83 True) % 3.68/3.83 Clause #149 (by superposition #[140, 108]): Or (Eq a b) (Eq True False) % 3.68/3.83 Clause #151 (by clausification #[149]): Eq a b % 3.68/3.83 Clause #152 (by forward contextual literal cutting #[151, 104]): False % 3.68/3.83 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------