%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWX207+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n006.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 : Tue May 5 06:59:10 PM UTC 2026 % Result : Theorem 4.35s 4.52s % Output : Proof 4.35s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SWX207+1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : duper %s % 0.17/0.33 % Computer : n006.cluster.edu % 0.17/0.33 % Model : x86_64 x86_64 % 0.17/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.33 % Memory : 8042.1875MB % 0.17/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.33 % CPULimit : 300 % 0.17/0.33 % WCLimit : 300 % 0.17/0.33 % DateTime : Tue May 5 11:35:15 EDT 2026 % 0.17/0.34 % CPUTime : % 4.35/4.52 SZS status Theorem for theBenchmark.p % 4.35/4.52 SZS output start Proof for theBenchmark.p % 4.35/4.52 Clause #14 (by assumption #[]): Eq (Ne pA pE) True % 4.35/4.52 Clause #16 (by assumption #[]): Eq (∀ (X X2 : Iota), Eq (proj1C (c2 X X2)) X) True % 4.35/4.52 Clause #18 (by assumption #[]): Eq (∀ (Y : Iota), Eq (append nil Y) Y) True % 4.35/4.52 Clause #19 (by assumption #[]): Eq (∀ (Y Z Xs : Iota), Eq (append (cons Z Xs) Y) (cons Z (append Xs Y))) True % 4.35/4.52 Clause #22 (by assumption #[]): Eq (Eq (linP pA) (cons a nil)) True % 4.35/4.52 Clause #24 (by assumption #[]): Eq (Eq (linP pE) nil) True % 4.35/4.52 Clause #25 (by assumption #[]): Eq (∀ (P Q : Iota), Eq (linC (c2 P Q)) (append (linP P) (linP Q))) True % 4.35/4.52 Clause #26 (by assumption #[]): Eq (Not (Exists fun U => Exists fun V => Not (Eq (linC U) (linC V) → Eq U V))) True % 4.35/4.52 Clause #28 (by clausification #[14]): Ne pA pE % 4.35/4.52 Clause #31 (by clausification #[24]): Eq (linP pE) nil % 4.35/4.52 Clause #53 (by clausification #[22]): Eq (linP pA) (cons a nil) % 4.35/4.52 Clause #61 (by clausification #[18]): ∀ (a : Iota), Eq (Eq (append nil a) a) True % 4.35/4.52 Clause #62 (by clausification #[61]): ∀ (a : Iota), Eq (append nil a) a % 4.35/4.52 Clause #73 (by clausification #[16]): ∀ (a : Iota), Eq (∀ (X2 : Iota), Eq (proj1C (c2 a X2)) a) True % 4.35/4.52 Clause #74 (by clausification #[73]): ∀ (a a_1 : Iota), Eq (Eq (proj1C (c2 a a_1)) a) True % 4.35/4.52 Clause #75 (by clausification #[74]): ∀ (a a_1 : Iota), Eq (proj1C (c2 a a_1)) a % 4.35/4.52 Clause #76 (by clausification #[25]): ∀ (a : Iota), Eq (∀ (Q : Iota), Eq (linC (c2 a Q)) (append (linP a) (linP Q))) True % 4.35/4.52 Clause #77 (by clausification #[76]): ∀ (a a_1 : Iota), Eq (Eq (linC (c2 a a_1)) (append (linP a) (linP a_1))) True % 4.35/4.52 Clause #78 (by clausification #[77]): ∀ (a a_1 : Iota), Eq (linC (c2 a a_1)) (append (linP a) (linP a_1)) % 4.35/4.52 Clause #79 (by superposition #[78, 31]): ∀ (a : Iota), Eq (linC (c2 a pE)) (append (linP a) nil) % 4.35/4.52 Clause #80 (by superposition #[78, 31]): ∀ (a : Iota), Eq (linC (c2 pE a)) (append nil (linP a)) % 4.35/4.52 Clause #81 (by clausification #[19]): ∀ (a : Iota), Eq (∀ (Z Xs : Iota), Eq (append (cons Z Xs) a) (cons Z (append Xs a))) True % 4.35/4.52 Clause #82 (by clausification #[81]): ∀ (a a_1 : Iota), Eq (∀ (Xs : Iota), Eq (append (cons a Xs) a_1) (cons a (append Xs a_1))) True % 4.35/4.52 Clause #83 (by clausification #[82]): ∀ (a a_1 a_2 : Iota), Eq (Eq (append (cons a a_1) a_2) (cons a (append a_1 a_2))) True % 4.35/4.52 Clause #84 (by clausification #[83]): ∀ (a a_1 a_2 : Iota), Eq (append (cons a a_1) a_2) (cons a (append a_1 a_2)) % 4.35/4.52 Clause #86 (by superposition #[84, 53]): ∀ (a_1 : Iota), Eq (append (linP pA) a_1) (cons a (append nil a_1)) % 4.35/4.52 Clause #87 (by forward demodulation #[80, 62]): ∀ (a : Iota), Eq (linC (c2 pE a)) (linP a) % 4.35/4.52 Clause #120 (by clausification #[26]): Eq (Exists fun U => Exists fun V => Not (Eq (linC U) (linC V) → Eq U V)) False % 4.35/4.52 Clause #121 (by clausification #[120]): ∀ (a : Iota), Eq (Exists fun V => Not (Eq (linC a) (linC V) → Eq a V)) False % 4.35/4.52 Clause #122 (by clausification #[121]): ∀ (a a_1 : Iota), Eq (Not (Eq (linC a) (linC a_1) → Eq a a_1)) False % 4.35/4.52 Clause #123 (by clausification #[122]): ∀ (a a_1 : Iota), Eq (Eq (linC a) (linC a_1) → Eq a a_1) True % 4.35/4.52 Clause #124 (by clausification #[123]): ∀ (a a_1 : Iota), Or (Eq (Eq (linC a) (linC a_1)) False) (Eq (Eq a a_1) True) % 4.35/4.52 Clause #125 (by clausification #[124]): ∀ (a a_1 : Iota), Or (Eq (Eq a a_1) True) (Ne (linC a) (linC a_1)) % 4.35/4.52 Clause #126 (by clausification #[125]): ∀ (a a_1 : Iota), Or (Ne (linC a) (linC a_1)) (Eq a a_1) % 4.35/4.52 Clause #129 (by superposition #[126, 79]): ∀ (a a_1 : Iota), Or (Ne (append (linP a) nil) (linC a_1)) (Eq (c2 a pE) a_1) % 4.35/4.52 Clause #152 (by forward demodulation #[86, 62]): ∀ (a_1 : Iota), Eq (append (linP pA) a_1) (cons a a_1) % 4.35/4.52 Clause #153 (by superposition #[152, 78]): ∀ (a_1 : Iota), Eq (linC (c2 pA a_1)) (cons a (linP a_1)) % 4.35/4.52 Clause #161 (by superposition #[153, 79]): Eq (cons a (linP pE)) (append (linP pA) nil) % 4.35/4.52 Clause #171 (by forward demodulation #[161, 31]): Eq (cons a nil) (append (linP pA) nil) % 4.35/4.52 Clause #172 (by forward demodulation #[171, 53]): Eq (linP pA) (append (linP pA) nil) % 4.35/4.52 Clause #208 (by superposition #[129, 172]): ∀ (a : Iota), Or (Ne (linP pA) (linC a)) (Eq (c2 pA pE) a) % 4.35/4.52 Clause #222 (by superposition #[208, 87]): ∀ (a : Iota), Or (Ne (linP pA) (linP a)) (Eq (c2 pA pE) (c2 pE a)) % 4.35/4.52 Clause #311 (by equality resolution #[222]): Eq (c2 pA pE) (c2 pE pA) % 4.35/4.52 Clause #317 (by superposition #[311, 75]): Eq (proj1C (c2 pE pA)) pA % 4.35/4.52 Clause #318 (by superposition #[317, 75]): Eq pA pE % 4.35/4.52 Clause #325 (by forward contextual literal cutting #[318, 28]): False % 4.35/4.52 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------