%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NLP145+1 : TPTP v9.2.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n024.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:55:44 PM UTC 2025 % Result : Theorem 13.55s 13.73s % Output : Proof 13.73s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : NLP145+1 : TPTP v9.2.0. Released v2.4.0. % 0.10/0.13 % Command : duper %s % 0.12/0.34 % Computer : n024.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 09:55:23 EDT 2025 % 0.12/0.34 % CPUTime : % 13.55/13.73 SZS status Theorem for theBenchmark.p % 13.55/13.73 SZS output start Proof for theBenchmark.p % 13.55/13.73 Clause #0 (by assumption #[]): Eq (∀ (U V : Iota), furniture U V → instrumentality U V) True % 13.55/13.73 Clause #1 (by assumption #[]): Eq (∀ (U V : Iota), seat U V → furniture U V) True % 13.55/13.73 Clause #2 (by assumption #[]): Eq (∀ (U V : Iota), frontseat U V → seat U V) True % 13.55/13.73 Clause #15 (by assumption #[]): Eq (∀ (U V : Iota), object U V → unisex U V) True % 13.55/13.73 Clause #19 (by assumption #[]): Eq (∀ (U V : Iota), artifact U V → object U V) True % 13.55/13.73 Clause #20 (by assumption #[]): Eq (∀ (U V : Iota), instrumentality U V → artifact U V) True % 13.55/13.73 Clause #36 (by assumption #[]): Eq (∀ (U V : Iota), man U V → male U V) True % 13.55/13.73 Clause #48 (by assumption #[]): Eq (∀ (U V : Iota), fellow U V → man U V) True % 13.55/13.73 Clause #55 (by assumption #[]): Eq (∀ (U V : Iota), unisex U V → Not (male U V)) True % 13.55/13.73 Clause #58 (by assumption #[]): Eq (∀ (U V W X : Iota), be U V W X → Eq W X) True % 13.55/13.73 Clause #59 (by assumption #[]): Eq % 13.55/13.73 (∀ (U V : Iota), % 13.55/13.73 Iff (two U V) % 13.55/13.73 (Exists fun W => % 13.55/13.73 And (member U W V) % 13.55/13.73 (Exists fun X => And (And (member U X V) (Ne X W)) (∀ (Y : Iota), member U Y V → Or (Eq Y X) (Eq Y W))))) % 13.55/13.73 True % 13.55/13.73 Clause #61 (by assumption #[]): Eq % 13.55/13.73 (Not % 13.55/13.73 (Not % 13.55/13.73 (Exists fun U => % 13.55/13.73 And (actual_world U) % 13.55/13.73 (Exists fun V => % 13.55/13.73 Exists fun W => % 13.55/13.73 Exists fun X => % 13.55/13.73 Exists fun Y => % 13.55/13.73 Exists fun Z => % 13.55/13.73 Exists fun X1 => % 13.55/13.73 And % 13.55/13.73 (And % 13.55/13.73 (And % 13.55/13.73 (And % 13.55/13.73 (And % 13.55/13.73 (And % 13.55/13.73 (And % 13.55/13.73 (And % 13.55/13.73 (And % 13.55/13.73 (And % 13.55/13.73 (And % 13.55/13.73 (And % 13.55/13.73 (And % 13.55/13.73 (And % 13.55/13.73 (And % 13.55/13.73 (And % 13.55/13.73 (And (And (And (of U W V) (city U V)) (hollywood_placename U W)) % 13.55/13.73 (placename U W)) % 13.55/13.73 (chevy U X)) % 13.55/13.73 (white U X)) % 13.55/13.73 (dirty U X)) % 13.55/13.73 (old U X)) % 13.55/13.73 (street U Y)) % 13.55/13.73 (lonely U Y)) % 13.55/13.73 (event U Z)) % 13.55/13.73 (agent U Z X)) % 13.55/13.73 (present U Z)) % 13.55/13.73 (barrel U Z)) % 13.55/13.73 (down U Z Y)) % 13.55/13.73 (in U Z V)) % 13.55/13.73 (∀ (X2 : Iota), % 13.55/13.73 member U X2 X1 → % 13.55/13.73 Exists fun X3 => % 13.55/13.73 Exists fun X4 => % 13.55/13.73 And (And (And (frontseat U X4) (state U X3)) (be U X3 X2 X4)) (in U X4 X4))) % 13.55/13.73 (two U X1)) % 13.55/13.73 (group U X1)) % 13.55/13.73 (∀ (X5 : Iota), member U X5 X1 → And (fellow U X5) (young U X5)))))) % 13.55/13.73 True % 13.55/13.73 Clause #62 (by clausification #[48]): ∀ (a : Iota), Eq (∀ (V : Iota), fellow a V → man a V) True % 13.55/13.73 Clause #63 (by clausification #[62]): ∀ (a a_1 : Iota), Eq (fellow a a_1 → man a a_1) True % 13.55/13.73 Clause #64 (by clausification #[63]): ∀ (a a_1 : Iota), Or (Eq (fellow a a_1) False) (Eq (man a a_1) True) % 13.55/13.73 Clause #77 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (V : Iota), furniture a V → instrumentality a V) True % 13.55/13.73 Clause #78 (by clausification #[77]): ∀ (a a_1 : Iota), Eq (furniture a a_1 → instrumentality a a_1) True % 13.55/13.73 Clause #79 (by clausification #[78]): ∀ (a a_1 : Iota), Or (Eq (furniture a a_1) False) (Eq (instrumentality a a_1) True) % 13.55/13.76 Clause #95 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (V : Iota), seat a V → furniture a V) True % 13.55/13.76 Clause #96 (by clausification #[95]): ∀ (a a_1 : Iota), Eq (seat a a_1 → furniture a a_1) True % 13.55/13.76 Clause #97 (by clausification #[96]): ∀ (a a_1 : Iota), Or (Eq (seat a a_1) False) (Eq (furniture a a_1) True) % 13.55/13.76 Clause #101 (by clausification #[36]): ∀ (a : Iota), Eq (∀ (V : Iota), man a V → male a V) True % 13.55/13.76 Clause #102 (by clausification #[101]): ∀ (a a_1 : Iota), Eq (man a a_1 → male a a_1) True % 13.55/13.76 Clause #103 (by clausification #[102]): ∀ (a a_1 : Iota), Or (Eq (man a a_1) False) (Eq (male a a_1) True) % 13.55/13.76 Clause #113 (by clausification #[2]): ∀ (a : Iota), Eq (∀ (V : Iota), frontseat a V → seat a V) True % 13.55/13.76 Clause #114 (by clausification #[113]): ∀ (a a_1 : Iota), Eq (frontseat a a_1 → seat a a_1) True % 13.55/13.76 Clause #115 (by clausification #[114]): ∀ (a a_1 : Iota), Or (Eq (frontseat a a_1) False) (Eq (seat a a_1) True) % 13.55/13.76 Clause #152 (by clausification #[15]): ∀ (a : Iota), Eq (∀ (V : Iota), object a V → unisex a V) True % 13.55/13.76 Clause #153 (by clausification #[152]): ∀ (a a_1 : Iota), Eq (object a a_1 → unisex a a_1) True % 13.55/13.76 Clause #154 (by clausification #[153]): ∀ (a a_1 : Iota), Or (Eq (object a a_1) False) (Eq (unisex a a_1) True) % 13.55/13.76 Clause #188 (by clausification #[19]): ∀ (a : Iota), Eq (∀ (V : Iota), artifact a V → object a V) True % 13.55/13.76 Clause #189 (by clausification #[188]): ∀ (a a_1 : Iota), Eq (artifact a a_1 → object a a_1) True % 13.55/13.76 Clause #190 (by clausification #[189]): ∀ (a a_1 : Iota), Or (Eq (artifact a a_1) False) (Eq (object a a_1) True) % 13.55/13.76 Clause #203 (by clausification #[20]): ∀ (a : Iota), Eq (∀ (V : Iota), instrumentality a V → artifact a V) True % 13.55/13.76 Clause #204 (by clausification #[203]): ∀ (a a_1 : Iota), Eq (instrumentality a a_1 → artifact a a_1) True % 13.55/13.76 Clause #205 (by clausification #[204]): ∀ (a a_1 : Iota), Or (Eq (instrumentality a a_1) False) (Eq (artifact a a_1) True) % 13.55/13.76 Clause #221 (by clausification #[55]): ∀ (a : Iota), Eq (∀ (V : Iota), unisex a V → Not (male a V)) True % 13.55/13.76 Clause #222 (by clausification #[221]): ∀ (a a_1 : Iota), Eq (unisex a a_1 → Not (male a a_1)) True % 13.55/13.76 Clause #223 (by clausification #[222]): ∀ (a a_1 : Iota), Or (Eq (unisex a a_1) False) (Eq (Not (male a a_1)) True) % 13.55/13.76 Clause #224 (by clausification #[223]): ∀ (a a_1 : Iota), Or (Eq (unisex a a_1) False) (Eq (male a a_1) False) % 13.55/13.76 Clause #244 (by clausification #[58]): ∀ (a : Iota), Eq (∀ (V W X : Iota), be a V W X → Eq W X) True % 13.55/13.76 Clause #245 (by clausification #[244]): ∀ (a a_1 : Iota), Eq (∀ (W X : Iota), be a a_1 W X → Eq W X) True % 13.55/13.76 Clause #246 (by clausification #[245]): ∀ (a a_1 a_2 : Iota), Eq (∀ (X : Iota), be a a_1 a_2 X → Eq a_2 X) True % 13.55/13.76 Clause #247 (by clausification #[246]): ∀ (a a_1 a_2 a_3 : Iota), Eq (be a a_1 a_2 a_3 → Eq a_2 a_3) True % 13.55/13.76 Clause #248 (by clausification #[247]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (be a a_1 a_2 a_3) False) (Eq (Eq a_2 a_3) True) % 13.55/13.76 Clause #249 (by clausification #[248]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (be a a_1 a_2 a_3) False) (Eq a_2 a_3) % 13.55/13.76 Clause #261 (by clausification #[59]): ∀ (a : Iota), % 13.55/13.76 Eq % 13.55/13.76 (∀ (V : Iota), % 13.55/13.76 Iff (two a V) % 13.55/13.76 (Exists fun W => % 13.55/13.76 And (member a W V) % 13.55/13.76 (Exists fun X => And (And (member a X V) (Ne X W)) (∀ (Y : Iota), member a Y V → Or (Eq Y X) (Eq Y W))))) % 13.55/13.76 True % 13.55/13.76 Clause #262 (by clausification #[261]): ∀ (a a_1 : Iota), % 13.55/13.76 Eq % 13.55/13.76 (Iff (two a a_1) % 13.55/13.76 (Exists fun W => % 13.55/13.76 And (member a W a_1) % 13.55/13.76 (Exists fun X => And (And (member a X a_1) (Ne X W)) (∀ (Y : Iota), member a Y a_1 → Or (Eq Y X) (Eq Y W))))) % 13.55/13.76 True % 13.55/13.76 Clause #264 (by clausification #[262]): ∀ (a a_1 : Iota), % 13.55/13.76 Or (Eq (two a a_1) False) % 13.55/13.76 (Eq % 13.55/13.76 (Exists fun W => % 13.55/13.76 And (member a W a_1) % 13.55/13.76 (Exists fun X => And (And (member a X a_1) (Ne X W)) (∀ (Y : Iota), member a Y a_1 → Or (Eq Y X) (Eq Y W)))) % 13.55/13.76 True) % 13.55/13.76 Clause #275 (by clausification #[264]): ∀ (a a_1 a_2 : Iota), % 13.55/13.76 Or (Eq (two a a_1) False) % 13.55/13.77 (Eq % 13.55/13.77 (And (member a (skS.0 1 a a_1 a_2) a_1) % 13.55/13.77 (Exists fun X => % 13.55/13.77 And (And (member a X a_1) (Ne X (skS.0 1 a a_1 a_2))) % 13.55/13.77 (∀ (Y : Iota), member a Y a_1 → Or (Eq Y X) (Eq Y (skS.0 1 a a_1 a_2))))) % 13.55/13.77 True) % 13.55/13.77 Clause #277 (by clausification #[275]): ∀ (a a_1 a_2 : Iota), Or (Eq (two a a_1) False) (Eq (member a (skS.0 1 a a_1 a_2) a_1) True) % 13.55/13.77 Clause #289 (by clausification #[61]): Eq % 13.55/13.77 (Not % 13.55/13.77 (Exists fun U => % 13.55/13.77 And (actual_world U) % 13.55/13.77 (Exists fun V => % 13.55/13.77 Exists fun W => % 13.55/13.77 Exists fun X => % 13.55/13.77 Exists fun Y => % 13.55/13.77 Exists fun Z => % 13.55/13.77 Exists fun X1 => % 13.55/13.77 And % 13.55/13.77 (And % 13.55/13.77 (And % 13.55/13.77 (And % 13.55/13.77 (And % 13.55/13.77 (And % 13.55/13.77 (And % 13.55/13.77 (And % 13.55/13.77 (And % 13.55/13.77 (And % 13.55/13.77 (And % 13.55/13.77 (And % 13.55/13.77 (And % 13.55/13.77 (And % 13.55/13.77 (And % 13.55/13.77 (And % 13.55/13.77 (And (And (And (of U W V) (city U V)) (hollywood_placename U W)) % 13.55/13.77 (placename U W)) % 13.55/13.77 (chevy U X)) % 13.55/13.77 (white U X)) % 13.55/13.77 (dirty U X)) % 13.55/13.77 (old U X)) % 13.55/13.77 (street U Y)) % 13.55/13.77 (lonely U Y)) % 13.55/13.77 (event U Z)) % 13.55/13.77 (agent U Z X)) % 13.55/13.77 (present U Z)) % 13.55/13.77 (barrel U Z)) % 13.55/13.77 (down U Z Y)) % 13.55/13.77 (in U Z V)) % 13.55/13.77 (∀ (X2 : Iota), % 13.55/13.77 member U X2 X1 → % 13.55/13.77 Exists fun X3 => % 13.55/13.77 Exists fun X4 => % 13.55/13.77 And (And (And (frontseat U X4) (state U X3)) (be U X3 X2 X4)) (in U X4 X4))) % 13.55/13.77 (two U X1)) % 13.55/13.77 (group U X1)) % 13.55/13.77 (∀ (X5 : Iota), member U X5 X1 → And (fellow U X5) (young U X5))))) % 13.55/13.77 False % 13.55/13.77 Clause #290 (by clausification #[289]): Eq % 13.55/13.77 (Exists fun U => % 13.55/13.77 And (actual_world U) % 13.55/13.77 (Exists fun V => % 13.55/13.77 Exists fun W => % 13.55/13.77 Exists fun X => % 13.55/13.77 Exists fun Y => % 13.55/13.77 Exists fun Z => % 13.55/13.77 Exists fun X1 => % 13.55/13.77 And % 13.55/13.77 (And % 13.55/13.77 (And % 13.55/13.77 (And % 13.55/13.77 (And % 13.55/13.77 (And % 13.55/13.77 (And % 13.55/13.77 (And % 13.55/13.77 (And % 13.55/13.77 (And % 13.55/13.77 (And % 13.55/13.77 (And % 13.55/13.77 (And % 13.55/13.77 (And % 13.55/13.77 (And % 13.55/13.77 (And % 13.55/13.77 (And (And (And (of U W V) (city U V)) (hollywood_placename U W)) % 13.55/13.77 (placename U W)) % 13.55/13.77 (chevy U X)) % 13.55/13.77 (white U X)) % 13.55/13.77 (dirty U X)) % 13.55/13.77 (old U X)) % 13.55/13.77 (street U Y)) % 13.55/13.77 (lonely U Y)) % 13.55/13.77 (event U Z)) % 13.55/13.77 (agent U Z X)) % 13.55/13.78 (present U Z)) % 13.55/13.78 (barrel U Z)) % 13.55/13.78 (down U Z Y)) % 13.55/13.78 (in U Z V)) % 13.55/13.78 (∀ (X2 : Iota), % 13.55/13.78 member U X2 X1 → % 13.55/13.78 Exists fun X3 => % 13.55/13.78 Exists fun X4 => % 13.55/13.78 And (And (And (frontseat U X4) (state U X3)) (be U X3 X2 X4)) (in U X4 X4))) % 13.55/13.78 (two U X1)) % 13.55/13.78 (group U X1)) % 13.55/13.78 (∀ (X5 : Iota), member U X5 X1 → And (fellow U X5) (young U X5)))) % 13.55/13.78 True % 13.55/13.78 Clause #291 (by clausification #[290]): ∀ (a : Iota), % 13.55/13.78 Eq % 13.55/13.78 (And (actual_world (skS.0 3 a)) % 13.55/13.78 (Exists fun V => % 13.55/13.78 Exists fun W => % 13.55/13.78 Exists fun X => % 13.55/13.78 Exists fun Y => % 13.55/13.78 Exists fun Z => % 13.55/13.78 Exists fun X1 => % 13.55/13.78 And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.78 (And (And (of (skS.0 3 a) W V) (city (skS.0 3 a) V)) % 13.55/13.78 (hollywood_placename (skS.0 3 a) W)) % 13.55/13.78 (placename (skS.0 3 a) W)) % 13.55/13.78 (chevy (skS.0 3 a) X)) % 13.55/13.78 (white (skS.0 3 a) X)) % 13.55/13.78 (dirty (skS.0 3 a) X)) % 13.55/13.78 (old (skS.0 3 a) X)) % 13.55/13.78 (street (skS.0 3 a) Y)) % 13.55/13.78 (lonely (skS.0 3 a) Y)) % 13.55/13.78 (event (skS.0 3 a) Z)) % 13.55/13.78 (agent (skS.0 3 a) Z X)) % 13.55/13.78 (present (skS.0 3 a) Z)) % 13.55/13.78 (barrel (skS.0 3 a) Z)) % 13.55/13.78 (down (skS.0 3 a) Z Y)) % 13.55/13.78 (in (skS.0 3 a) Z V)) % 13.55/13.78 (∀ (X2 : Iota), % 13.55/13.78 member (skS.0 3 a) X2 X1 → % 13.55/13.78 Exists fun X3 => % 13.55/13.78 Exists fun X4 => % 13.55/13.78 And % 13.55/13.78 (And (And (frontseat (skS.0 3 a) X4) (state (skS.0 3 a) X3)) % 13.55/13.78 (be (skS.0 3 a) X3 X2 X4)) % 13.55/13.78 (in (skS.0 3 a) X4 X4))) % 13.55/13.78 (two (skS.0 3 a) X1)) % 13.55/13.78 (group (skS.0 3 a) X1)) % 13.55/13.78 (∀ (X5 : Iota), member (skS.0 3 a) X5 X1 → And (fellow (skS.0 3 a) X5) (young (skS.0 3 a) X5)))) % 13.55/13.78 True % 13.55/13.78 Clause #292 (by clausification #[291]): ∀ (a : Iota), % 13.55/13.78 Eq % 13.55/13.78 (Exists fun V => % 13.55/13.78 Exists fun W => % 13.55/13.78 Exists fun X => % 13.55/13.78 Exists fun Y => % 13.55/13.78 Exists fun Z => % 13.55/13.78 Exists fun X1 => % 13.55/13.78 And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.78 (And % 13.55/13.79 (And % 13.55/13.79 (And (And (of (skS.0 3 a) W V) (city (skS.0 3 a) V)) % 13.55/13.79 (hollywood_placename (skS.0 3 a) W)) % 13.55/13.79 (placename (skS.0 3 a) W)) % 13.55/13.79 (chevy (skS.0 3 a) X)) % 13.55/13.79 (white (skS.0 3 a) X)) % 13.55/13.79 (dirty (skS.0 3 a) X)) % 13.55/13.79 (old (skS.0 3 a) X)) % 13.55/13.79 (street (skS.0 3 a) Y)) % 13.55/13.79 (lonely (skS.0 3 a) Y)) % 13.55/13.79 (event (skS.0 3 a) Z)) % 13.55/13.79 (agent (skS.0 3 a) Z X)) % 13.55/13.79 (present (skS.0 3 a) Z)) % 13.55/13.79 (barrel (skS.0 3 a) Z)) % 13.55/13.79 (down (skS.0 3 a) Z Y)) % 13.55/13.79 (in (skS.0 3 a) Z V)) % 13.55/13.79 (∀ (X2 : Iota), % 13.55/13.79 member (skS.0 3 a) X2 X1 → % 13.55/13.79 Exists fun X3 => % 13.55/13.79 Exists fun X4 => % 13.55/13.79 And % 13.55/13.79 (And (And (frontseat (skS.0 3 a) X4) (state (skS.0 3 a) X3)) % 13.55/13.79 (be (skS.0 3 a) X3 X2 X4)) % 13.55/13.79 (in (skS.0 3 a) X4 X4))) % 13.55/13.79 (two (skS.0 3 a) X1)) % 13.55/13.79 (group (skS.0 3 a) X1)) % 13.55/13.79 (∀ (X5 : Iota), member (skS.0 3 a) X5 X1 → And (fellow (skS.0 3 a) X5) (young (skS.0 3 a) X5))) % 13.55/13.79 True % 13.55/13.79 Clause #294 (by clausification #[292]): ∀ (a a_1 : Iota), % 13.55/13.79 Eq % 13.55/13.79 (Exists fun W => % 13.55/13.79 Exists fun X => % 13.55/13.79 Exists fun Y => % 13.55/13.79 Exists fun Z => % 13.55/13.79 Exists fun X1 => % 13.55/13.79 And % 13.55/13.79 (And % 13.55/13.79 (And % 13.55/13.79 (And % 13.55/13.79 (And % 13.55/13.79 (And % 13.55/13.79 (And % 13.55/13.79 (And % 13.55/13.79 (And % 13.55/13.79 (And % 13.55/13.79 (And % 13.55/13.79 (And % 13.55/13.79 (And % 13.55/13.79 (And % 13.55/13.79 (And % 13.55/13.79 (And % 13.55/13.79 (And % 13.55/13.79 (And % 13.55/13.79 (And (of (skS.0 3 a) W (skS.0 4 a a_1)) % 13.55/13.79 (city (skS.0 3 a) (skS.0 4 a a_1))) % 13.55/13.79 (hollywood_placename (skS.0 3 a) W)) % 13.55/13.79 (placename (skS.0 3 a) W)) % 13.55/13.79 (chevy (skS.0 3 a) X)) % 13.55/13.79 (white (skS.0 3 a) X)) % 13.55/13.79 (dirty (skS.0 3 a) X)) % 13.55/13.79 (old (skS.0 3 a) X)) % 13.55/13.79 (street (skS.0 3 a) Y)) % 13.55/13.79 (lonely (skS.0 3 a) Y)) % 13.55/13.79 (event (skS.0 3 a) Z)) % 13.55/13.79 (agent (skS.0 3 a) Z X)) % 13.55/13.79 (present (skS.0 3 a) Z)) % 13.55/13.79 (barrel (skS.0 3 a) Z)) % 13.55/13.79 (down (skS.0 3 a) Z Y)) % 13.55/13.79 (in (skS.0 3 a) Z (skS.0 4 a a_1))) % 13.55/13.79 (∀ (X2 : Iota), % 13.55/13.79 member (skS.0 3 a) X2 X1 → % 13.55/13.79 Exists fun X3 => % 13.55/13.79 Exists fun X4 => % 13.55/13.79 And % 13.55/13.79 (And (And (frontseat (skS.0 3 a) X4) (state (skS.0 3 a) X3)) (be (skS.0 3 a) X3 X2 X4)) % 13.55/13.79 (in (skS.0 3 a) X4 X4))) % 13.55/13.79 (two (skS.0 3 a) X1)) % 13.55/13.79 (group (skS.0 3 a) X1)) % 13.55/13.79 (∀ (X5 : Iota), member (skS.0 3 a) X5 X1 → And (fellow (skS.0 3 a) X5) (young (skS.0 3 a) X5))) % 13.63/13.81 True % 13.63/13.81 Clause #295 (by clausification #[294]): ∀ (a a_1 a_2 : Iota), % 13.63/13.81 Eq % 13.63/13.81 (Exists fun X => % 13.63/13.81 Exists fun Y => % 13.63/13.81 Exists fun Z => % 13.63/13.81 Exists fun X1 => % 13.63/13.81 And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And (of (skS.0 3 a) (skS.0 5 a a_1 a_2) (skS.0 4 a a_1)) % 13.63/13.81 (city (skS.0 3 a) (skS.0 4 a a_1))) % 13.63/13.81 (hollywood_placename (skS.0 3 a) (skS.0 5 a a_1 a_2))) % 13.63/13.81 (placename (skS.0 3 a) (skS.0 5 a a_1 a_2))) % 13.63/13.81 (chevy (skS.0 3 a) X)) % 13.63/13.81 (white (skS.0 3 a) X)) % 13.63/13.81 (dirty (skS.0 3 a) X)) % 13.63/13.81 (old (skS.0 3 a) X)) % 13.63/13.81 (street (skS.0 3 a) Y)) % 13.63/13.81 (lonely (skS.0 3 a) Y)) % 13.63/13.81 (event (skS.0 3 a) Z)) % 13.63/13.81 (agent (skS.0 3 a) Z X)) % 13.63/13.81 (present (skS.0 3 a) Z)) % 13.63/13.81 (barrel (skS.0 3 a) Z)) % 13.63/13.81 (down (skS.0 3 a) Z Y)) % 13.63/13.81 (in (skS.0 3 a) Z (skS.0 4 a a_1))) % 13.63/13.81 (∀ (X2 : Iota), % 13.63/13.81 member (skS.0 3 a) X2 X1 → % 13.63/13.81 Exists fun X3 => % 13.63/13.81 Exists fun X4 => % 13.63/13.81 And (And (And (frontseat (skS.0 3 a) X4) (state (skS.0 3 a) X3)) (be (skS.0 3 a) X3 X2 X4)) % 13.63/13.81 (in (skS.0 3 a) X4 X4))) % 13.63/13.81 (two (skS.0 3 a) X1)) % 13.63/13.81 (group (skS.0 3 a) X1)) % 13.63/13.81 (∀ (X5 : Iota), member (skS.0 3 a) X5 X1 → And (fellow (skS.0 3 a) X5) (young (skS.0 3 a) X5))) % 13.63/13.81 True % 13.63/13.81 Clause #296 (by clausification #[295]): ∀ (a a_1 a_2 a_3 : Iota), % 13.63/13.81 Eq % 13.63/13.81 (Exists fun Y => % 13.63/13.81 Exists fun Z => % 13.63/13.81 Exists fun X1 => % 13.63/13.81 And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And % 13.63/13.81 (And (of (skS.0 3 a) (skS.0 5 a a_1 a_2) (skS.0 4 a a_1)) % 13.63/13.81 (city (skS.0 3 a) (skS.0 4 a a_1))) % 13.63/13.81 (hollywood_placename (skS.0 3 a) (skS.0 5 a a_1 a_2))) % 13.63/13.81 (placename (skS.0 3 a) (skS.0 5 a a_1 a_2))) % 13.63/13.81 (chevy (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.81 (white (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.81 (dirty (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.81 (old (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.81 (street (skS.0 3 a) Y)) % 13.63/13.81 (lonely (skS.0 3 a) Y)) % 13.63/13.81 (event (skS.0 3 a) Z)) % 13.63/13.83 (agent (skS.0 3 a) Z (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.83 (present (skS.0 3 a) Z)) % 13.63/13.83 (barrel (skS.0 3 a) Z)) % 13.63/13.83 (down (skS.0 3 a) Z Y)) % 13.63/13.83 (in (skS.0 3 a) Z (skS.0 4 a a_1))) % 13.63/13.83 (∀ (X2 : Iota), % 13.63/13.83 member (skS.0 3 a) X2 X1 → % 13.63/13.83 Exists fun X3 => % 13.63/13.83 Exists fun X4 => % 13.63/13.83 And (And (And (frontseat (skS.0 3 a) X4) (state (skS.0 3 a) X3)) (be (skS.0 3 a) X3 X2 X4)) % 13.63/13.83 (in (skS.0 3 a) X4 X4))) % 13.63/13.83 (two (skS.0 3 a) X1)) % 13.63/13.83 (group (skS.0 3 a) X1)) % 13.63/13.83 (∀ (X5 : Iota), member (skS.0 3 a) X5 X1 → And (fellow (skS.0 3 a) X5) (young (skS.0 3 a) X5))) % 13.63/13.83 True % 13.63/13.83 Clause #297 (by clausification #[296]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 13.63/13.83 Eq % 13.63/13.83 (Exists fun Z => % 13.63/13.83 Exists fun X1 => % 13.63/13.83 And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And (of (skS.0 3 a) (skS.0 5 a a_1 a_2) (skS.0 4 a a_1)) % 13.63/13.83 (city (skS.0 3 a) (skS.0 4 a a_1))) % 13.63/13.83 (hollywood_placename (skS.0 3 a) (skS.0 5 a a_1 a_2))) % 13.63/13.83 (placename (skS.0 3 a) (skS.0 5 a a_1 a_2))) % 13.63/13.83 (chevy (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.83 (white (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.83 (dirty (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.83 (old (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.83 (street (skS.0 3 a) (skS.0 7 a a_1 a_2 a_3 a_4))) % 13.63/13.83 (lonely (skS.0 3 a) (skS.0 7 a a_1 a_2 a_3 a_4))) % 13.63/13.83 (event (skS.0 3 a) Z)) % 13.63/13.83 (agent (skS.0 3 a) Z (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.83 (present (skS.0 3 a) Z)) % 13.63/13.83 (barrel (skS.0 3 a) Z)) % 13.63/13.83 (down (skS.0 3 a) Z (skS.0 7 a a_1 a_2 a_3 a_4))) % 13.63/13.83 (in (skS.0 3 a) Z (skS.0 4 a a_1))) % 13.63/13.83 (∀ (X2 : Iota), % 13.63/13.83 member (skS.0 3 a) X2 X1 → % 13.63/13.83 Exists fun X3 => % 13.63/13.83 Exists fun X4 => % 13.63/13.83 And (And (And (frontseat (skS.0 3 a) X4) (state (skS.0 3 a) X3)) (be (skS.0 3 a) X3 X2 X4)) % 13.63/13.83 (in (skS.0 3 a) X4 X4))) % 13.63/13.83 (two (skS.0 3 a) X1)) % 13.63/13.83 (group (skS.0 3 a) X1)) % 13.63/13.83 (∀ (X5 : Iota), member (skS.0 3 a) X5 X1 → And (fellow (skS.0 3 a) X5) (young (skS.0 3 a) X5))) % 13.63/13.83 True % 13.63/13.83 Clause #298 (by clausification #[297]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 13.63/13.83 Eq % 13.63/13.83 (Exists fun X1 => % 13.63/13.83 And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And % 13.63/13.83 (And (of (skS.0 3 a) (skS.0 5 a a_1 a_2) (skS.0 4 a a_1)) % 13.63/13.83 (city (skS.0 3 a) (skS.0 4 a a_1))) % 13.63/13.83 (hollywood_placename (skS.0 3 a) (skS.0 5 a a_1 a_2))) % 13.63/13.83 (placename (skS.0 3 a) (skS.0 5 a a_1 a_2))) % 13.63/13.84 (chevy (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.84 (white (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.84 (dirty (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.84 (old (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.84 (street (skS.0 3 a) (skS.0 7 a a_1 a_2 a_3 a_4))) % 13.63/13.84 (lonely (skS.0 3 a) (skS.0 7 a a_1 a_2 a_3 a_4))) % 13.63/13.84 (event (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5))) % 13.63/13.84 (agent (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.84 (present (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5))) % 13.63/13.84 (barrel (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5))) % 13.63/13.84 (down (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2 a_3 a_4))) % 13.63/13.84 (in (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5) (skS.0 4 a a_1))) % 13.63/13.84 (∀ (X2 : Iota), % 13.63/13.84 member (skS.0 3 a) X2 X1 → % 13.63/13.84 Exists fun X3 => % 13.63/13.84 Exists fun X4 => % 13.63/13.84 And (And (And (frontseat (skS.0 3 a) X4) (state (skS.0 3 a) X3)) (be (skS.0 3 a) X3 X2 X4)) % 13.63/13.84 (in (skS.0 3 a) X4 X4))) % 13.63/13.84 (two (skS.0 3 a) X1)) % 13.63/13.84 (group (skS.0 3 a) X1)) % 13.63/13.84 (∀ (X5 : Iota), member (skS.0 3 a) X5 X1 → And (fellow (skS.0 3 a) X5) (young (skS.0 3 a) X5))) % 13.63/13.84 True % 13.63/13.84 Clause #299 (by clausification #[298]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 13.63/13.84 Eq % 13.63/13.84 (And % 13.63/13.84 (And % 13.63/13.84 (And % 13.63/13.84 (And % 13.63/13.84 (And % 13.63/13.84 (And % 13.63/13.84 (And % 13.63/13.84 (And % 13.63/13.84 (And % 13.63/13.84 (And % 13.63/13.84 (And % 13.63/13.84 (And % 13.63/13.84 (And % 13.63/13.84 (And % 13.63/13.84 (And % 13.63/13.84 (And % 13.63/13.84 (And % 13.63/13.84 (And % 13.63/13.84 (And (of (skS.0 3 a) (skS.0 5 a a_1 a_2) (skS.0 4 a a_1)) % 13.63/13.84 (city (skS.0 3 a) (skS.0 4 a a_1))) % 13.63/13.84 (hollywood_placename (skS.0 3 a) (skS.0 5 a a_1 a_2))) % 13.63/13.84 (placename (skS.0 3 a) (skS.0 5 a a_1 a_2))) % 13.63/13.84 (chevy (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.84 (white (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.84 (dirty (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.84 (old (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.84 (street (skS.0 3 a) (skS.0 7 a a_1 a_2 a_3 a_4))) % 13.63/13.84 (lonely (skS.0 3 a) (skS.0 7 a a_1 a_2 a_3 a_4))) % 13.63/13.84 (event (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5))) % 13.63/13.84 (agent (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.84 (present (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5))) % 13.63/13.84 (barrel (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5))) % 13.63/13.84 (down (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2 a_3 a_4))) % 13.63/13.84 (in (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5) (skS.0 4 a a_1))) % 13.63/13.84 (∀ (X2 : Iota), % 13.63/13.84 member (skS.0 3 a) X2 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) → % 13.63/13.84 Exists fun X3 => % 13.63/13.84 Exists fun X4 => % 13.63/13.84 And (And (And (frontseat (skS.0 3 a) X4) (state (skS.0 3 a) X3)) (be (skS.0 3 a) X3 X2 X4)) % 13.63/13.84 (in (skS.0 3 a) X4 X4))) % 13.63/13.84 (two (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6))) % 13.63/13.84 (group (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6))) % 13.63/13.84 (∀ (X5 : Iota), % 13.63/13.84 member (skS.0 3 a) X5 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) → And (fellow (skS.0 3 a) X5) (young (skS.0 3 a) X5))) % 13.63/13.84 True % 13.63/13.84 Clause #300 (by clausification #[299]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 13.63/13.87 Eq % 13.63/13.87 (∀ (X5 : Iota), % 13.63/13.87 member (skS.0 3 a) X5 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) → And (fellow (skS.0 3 a) X5) (young (skS.0 3 a) X5)) % 13.63/13.87 True % 13.63/13.87 Clause #301 (by clausification #[299]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 13.63/13.87 Eq % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And (of (skS.0 3 a) (skS.0 5 a a_1 a_2) (skS.0 4 a a_1)) % 13.63/13.87 (city (skS.0 3 a) (skS.0 4 a a_1))) % 13.63/13.87 (hollywood_placename (skS.0 3 a) (skS.0 5 a a_1 a_2))) % 13.63/13.87 (placename (skS.0 3 a) (skS.0 5 a a_1 a_2))) % 13.63/13.87 (chevy (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.87 (white (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.87 (dirty (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.87 (old (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.87 (street (skS.0 3 a) (skS.0 7 a a_1 a_2 a_3 a_4))) % 13.63/13.87 (lonely (skS.0 3 a) (skS.0 7 a a_1 a_2 a_3 a_4))) % 13.63/13.87 (event (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5))) % 13.63/13.87 (agent (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.87 (present (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5))) % 13.63/13.87 (barrel (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5))) % 13.63/13.87 (down (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2 a_3 a_4))) % 13.63/13.87 (in (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5) (skS.0 4 a a_1))) % 13.63/13.87 (∀ (X2 : Iota), % 13.63/13.87 member (skS.0 3 a) X2 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) → % 13.63/13.87 Exists fun X3 => % 13.63/13.87 Exists fun X4 => % 13.63/13.87 And (And (And (frontseat (skS.0 3 a) X4) (state (skS.0 3 a) X3)) (be (skS.0 3 a) X3 X2 X4)) % 13.63/13.87 (in (skS.0 3 a) X4 X4))) % 13.63/13.87 (two (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6))) % 13.63/13.87 (group (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6))) % 13.63/13.87 True % 13.63/13.87 Clause #302 (by clausification #[300]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 13.63/13.87 Eq (member (skS.0 3 a) a_1 (skS.0 9 a a_2 a_3 a_4 a_5 a_6 a_7) → And (fellow (skS.0 3 a) a_1) (young (skS.0 3 a) a_1)) % 13.63/13.87 True % 13.63/13.87 Clause #303 (by clausification #[302]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 13.63/13.87 Or (Eq (member (skS.0 3 a) a_1 (skS.0 9 a a_2 a_3 a_4 a_5 a_6 a_7)) False) % 13.63/13.87 (Eq (And (fellow (skS.0 3 a) a_1) (young (skS.0 3 a) a_1)) True) % 13.63/13.87 Clause #305 (by clausification #[303]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 13.63/13.87 Or (Eq (member (skS.0 3 a) a_1 (skS.0 9 a a_2 a_3 a_4 a_5 a_6 a_7)) False) (Eq (fellow (skS.0 3 a) a_1) True) % 13.63/13.87 Clause #311 (by clausification #[301]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 13.63/13.87 Eq % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And % 13.63/13.87 (And (of (skS.0 3 a) (skS.0 5 a a_1 a_2) (skS.0 4 a a_1)) % 13.63/13.87 (city (skS.0 3 a) (skS.0 4 a a_1))) % 13.63/13.87 (hollywood_placename (skS.0 3 a) (skS.0 5 a a_1 a_2))) % 13.63/13.87 (placename (skS.0 3 a) (skS.0 5 a a_1 a_2))) % 13.63/13.87 (chevy (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.87 (white (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.87 (dirty (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.88 (old (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.88 (street (skS.0 3 a) (skS.0 7 a a_1 a_2 a_3 a_4))) % 13.63/13.88 (lonely (skS.0 3 a) (skS.0 7 a a_1 a_2 a_3 a_4))) % 13.63/13.88 (event (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5))) % 13.63/13.88 (agent (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.88 (present (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5))) % 13.63/13.88 (barrel (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5))) % 13.63/13.88 (down (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2 a_3 a_4))) % 13.63/13.88 (in (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5) (skS.0 4 a a_1))) % 13.63/13.88 (∀ (X2 : Iota), % 13.63/13.88 member (skS.0 3 a) X2 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) → % 13.63/13.88 Exists fun X3 => % 13.63/13.88 Exists fun X4 => % 13.63/13.88 And (And (And (frontseat (skS.0 3 a) X4) (state (skS.0 3 a) X3)) (be (skS.0 3 a) X3 X2 X4)) % 13.63/13.88 (in (skS.0 3 a) X4 X4))) % 13.63/13.88 (two (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6))) % 13.63/13.88 True % 13.63/13.88 Clause #313 (by clausification #[311]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), Eq (two (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6)) True % 13.63/13.88 Clause #314 (by clausification #[311]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 13.63/13.88 Eq % 13.63/13.88 (And % 13.63/13.88 (And % 13.63/13.88 (And % 13.63/13.88 (And % 13.63/13.88 (And % 13.63/13.88 (And % 13.63/13.88 (And % 13.63/13.88 (And % 13.63/13.88 (And % 13.63/13.88 (And % 13.63/13.88 (And % 13.63/13.88 (And % 13.63/13.88 (And % 13.63/13.88 (And % 13.63/13.88 (And % 13.63/13.88 (And (of (skS.0 3 a) (skS.0 5 a a_1 a_2) (skS.0 4 a a_1)) % 13.63/13.88 (city (skS.0 3 a) (skS.0 4 a a_1))) % 13.63/13.88 (hollywood_placename (skS.0 3 a) (skS.0 5 a a_1 a_2))) % 13.63/13.88 (placename (skS.0 3 a) (skS.0 5 a a_1 a_2))) % 13.63/13.88 (chevy (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.88 (white (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.88 (dirty (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.88 (old (skS.0 3 a) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.88 (street (skS.0 3 a) (skS.0 7 a a_1 a_2 a_3 a_4))) % 13.63/13.88 (lonely (skS.0 3 a) (skS.0 7 a a_1 a_2 a_3 a_4))) % 13.63/13.88 (event (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5))) % 13.63/13.88 (agent (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2 a_3))) % 13.63/13.88 (present (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5))) % 13.63/13.88 (barrel (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5))) % 13.63/13.88 (down (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2 a_3 a_4))) % 13.63/13.88 (in (skS.0 3 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5) (skS.0 4 a a_1))) % 13.63/13.88 (∀ (X2 : Iota), % 13.63/13.88 member (skS.0 3 a) X2 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) → % 13.63/13.88 Exists fun X3 => % 13.63/13.88 Exists fun X4 => % 13.63/13.88 And (And (And (frontseat (skS.0 3 a) X4) (state (skS.0 3 a) X3)) (be (skS.0 3 a) X3 X2 X4)) % 13.63/13.88 (in (skS.0 3 a) X4 X4))) % 13.63/13.88 True % 13.63/13.88 Clause #317 (by superposition #[313, 277]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 13.63/13.88 Or (Eq True False) % 13.63/13.88 (Eq % 13.63/13.88 (member (skS.0 3 a) (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) % 13.63/13.88 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6)) % 13.63/13.88 True) % 13.63/13.88 Clause #323 (by clausification #[317]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 13.63/13.88 Eq % 13.63/13.88 (member (skS.0 3 a) (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) % 13.63/13.88 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6)) % 13.63/13.88 True % 13.63/13.88 Clause #325 (by superposition #[323, 305]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 13.63/13.88 Or (Eq True False) (Eq (fellow (skS.0 3 a) (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7)) True) % 13.63/13.88 Clause #329 (by clausification #[325]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 13.63/13.88 Eq (fellow (skS.0 3 a) (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7)) True % 13.63/13.88 Clause #330 (by superposition #[329, 64]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 13.73/13.91 Or (Eq True False) (Eq (man (skS.0 3 a) (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7)) True) % 13.73/13.91 Clause #331 (by clausification #[314]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 13.73/13.91 Eq % 13.73/13.91 (∀ (X2 : Iota), % 13.73/13.91 member (skS.0 3 a) X2 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) → % 13.73/13.91 Exists fun X3 => % 13.73/13.91 Exists fun X4 => % 13.73/13.91 And (And (And (frontseat (skS.0 3 a) X4) (state (skS.0 3 a) X3)) (be (skS.0 3 a) X3 X2 X4)) % 13.73/13.91 (in (skS.0 3 a) X4 X4)) % 13.73/13.91 True % 13.73/13.91 Clause #333 (by clausification #[331]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 13.73/13.91 Eq % 13.73/13.91 (member (skS.0 3 a) a_1 (skS.0 9 a a_2 a_3 a_4 a_5 a_6 a_7) → % 13.73/13.91 Exists fun X3 => % 13.73/13.91 Exists fun X4 => % 13.73/13.91 And (And (And (frontseat (skS.0 3 a) X4) (state (skS.0 3 a) X3)) (be (skS.0 3 a) X3 a_1 X4)) % 13.73/13.91 (in (skS.0 3 a) X4 X4)) % 13.73/13.91 True % 13.73/13.91 Clause #334 (by clausification #[333]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 13.73/13.91 Or (Eq (member (skS.0 3 a) a_1 (skS.0 9 a a_2 a_3 a_4 a_5 a_6 a_7)) False) % 13.73/13.91 (Eq % 13.73/13.91 (Exists fun X3 => % 13.73/13.91 Exists fun X4 => % 13.73/13.91 And (And (And (frontseat (skS.0 3 a) X4) (state (skS.0 3 a) X3)) (be (skS.0 3 a) X3 a_1 X4)) % 13.73/13.91 (in (skS.0 3 a) X4 X4)) % 13.73/13.91 True) % 13.73/13.91 Clause #335 (by clausification #[334]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 13.73/13.91 Or (Eq (member (skS.0 3 a) a_1 (skS.0 9 a a_2 a_3 a_4 a_5 a_6 a_7)) False) % 13.73/13.91 (Eq % 13.73/13.91 (Exists fun X4 => % 13.73/13.91 And % 13.73/13.91 (And (And (frontseat (skS.0 3 a) X4) (state (skS.0 3 a) (skS.0 10 a a_1 a_8))) % 13.73/13.91 (be (skS.0 3 a) (skS.0 10 a a_1 a_8) a_1 X4)) % 13.73/13.91 (in (skS.0 3 a) X4 X4)) % 13.73/13.91 True) % 13.73/13.91 Clause #336 (by clausification #[335]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 13.73/13.91 Or (Eq (member (skS.0 3 a) a_1 (skS.0 9 a a_2 a_3 a_4 a_5 a_6 a_7)) False) % 13.73/13.91 (Eq % 13.73/13.91 (And % 13.73/13.91 (And (And (frontseat (skS.0 3 a) (skS.0 11 a a_1 a_8 a_9)) (state (skS.0 3 a) (skS.0 10 a a_1 a_8))) % 13.73/13.91 (be (skS.0 3 a) (skS.0 10 a a_1 a_8) a_1 (skS.0 11 a a_1 a_8 a_9))) % 13.73/13.91 (in (skS.0 3 a) (skS.0 11 a a_1 a_8 a_9) (skS.0 11 a a_1 a_8 a_9))) % 13.73/13.91 True) % 13.73/13.91 Clause #338 (by clausification #[336]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 13.73/13.91 Or (Eq (member (skS.0 3 a) a_1 (skS.0 9 a a_2 a_3 a_4 a_5 a_6 a_7)) False) % 13.73/13.91 (Eq % 13.73/13.91 (And (And (frontseat (skS.0 3 a) (skS.0 11 a a_1 a_8 a_9)) (state (skS.0 3 a) (skS.0 10 a a_1 a_8))) % 13.73/13.91 (be (skS.0 3 a) (skS.0 10 a a_1 a_8) a_1 (skS.0 11 a a_1 a_8 a_9))) % 13.73/13.91 True) % 13.73/13.91 Clause #340 (by clausification #[330]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 13.73/13.91 Eq (man (skS.0 3 a) (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7)) True % 13.73/13.91 Clause #342 (by superposition #[340, 103]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 13.73/13.91 Or (Eq True False) (Eq (male (skS.0 3 a) (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7)) True) % 13.73/13.91 Clause #343 (by clausification #[342]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 13.73/13.91 Eq (male (skS.0 3 a) (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7)) True % 13.73/13.91 Clause #434 (by clausification #[338]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 13.73/13.91 Or (Eq (member (skS.0 3 a) a_1 (skS.0 9 a a_2 a_3 a_4 a_5 a_6 a_7)) False) % 13.73/13.91 (Eq (be (skS.0 3 a) (skS.0 10 a a_1 a_8) a_1 (skS.0 11 a a_1 a_8 a_9)) True) % 13.73/13.91 Clause #435 (by clausification #[338]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 13.73/13.91 Or (Eq (member (skS.0 3 a) a_1 (skS.0 9 a a_2 a_3 a_4 a_5 a_6 a_7)) False) % 13.73/13.91 (Eq (And (frontseat (skS.0 3 a) (skS.0 11 a a_1 a_8 a_9)) (state (skS.0 3 a) (skS.0 10 a a_1 a_8))) True) % 13.73/13.91 Clause #436 (by superposition #[434, 323]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 13.73/13.91 Or % 13.73/13.91 (Eq % 13.73/13.91 (be (skS.0 3 a) (skS.0 10 a (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) a_8) % 13.73/13.91 (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) % 13.73/13.91 (skS.0 11 a (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) a_8 a_9)) % 13.73/13.91 True) % 13.73/13.91 (Eq False True) % 13.73/13.91 Clause #439 (by clausification #[435]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 13.73/13.91 Or (Eq (member (skS.0 3 a) a_1 (skS.0 9 a a_2 a_3 a_4 a_5 a_6 a_7)) False) % 13.73/13.94 (Eq (frontseat (skS.0 3 a) (skS.0 11 a a_1 a_8 a_9)) True) % 13.73/13.94 Clause #442 (by superposition #[439, 323]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 13.73/13.94 Or % 13.73/13.94 (Eq (frontseat (skS.0 3 a) (skS.0 11 a (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) a_8 a_9)) True) % 13.73/13.94 (Eq False True) % 13.73/13.94 Clause #598 (by clausification #[442]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 13.73/13.94 Eq (frontseat (skS.0 3 a) (skS.0 11 a (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) a_8 a_9)) True % 13.73/13.94 Clause #599 (by superposition #[598, 115]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 13.73/13.94 Or (Eq True False) % 13.73/13.94 (Eq (seat (skS.0 3 a) (skS.0 11 a (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) a_8 a_9)) True) % 13.73/13.94 Clause #603 (by clausification #[599]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 13.73/13.94 Eq (seat (skS.0 3 a) (skS.0 11 a (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) a_8 a_9)) True % 13.73/13.94 Clause #604 (by superposition #[603, 97]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 13.73/13.94 Or (Eq True False) % 13.73/13.94 (Eq (furniture (skS.0 3 a) (skS.0 11 a (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) a_8 a_9)) True) % 13.73/13.94 Clause #728 (by clausification #[604]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 13.73/13.94 Eq (furniture (skS.0 3 a) (skS.0 11 a (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) a_8 a_9)) True % 13.73/13.94 Clause #729 (by superposition #[728, 79]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 13.73/13.94 Or (Eq True False) % 13.73/13.94 (Eq (instrumentality (skS.0 3 a) (skS.0 11 a (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) a_8 a_9)) % 13.73/13.94 True) % 13.73/13.94 Clause #734 (by clausification #[729]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 13.73/13.94 Eq (instrumentality (skS.0 3 a) (skS.0 11 a (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) a_8 a_9)) % 13.73/13.94 True % 13.73/13.94 Clause #735 (by superposition #[734, 205]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 13.73/13.94 Or (Eq True False) % 13.73/13.94 (Eq (artifact (skS.0 3 a) (skS.0 11 a (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) a_8 a_9)) True) % 13.73/13.94 Clause #740 (by clausification #[735]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 13.73/13.94 Eq (artifact (skS.0 3 a) (skS.0 11 a (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) a_8 a_9)) True % 13.73/13.94 Clause #741 (by superposition #[740, 190]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 13.73/13.94 Or (Eq True False) % 13.73/13.94 (Eq (object (skS.0 3 a) (skS.0 11 a (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) a_8 a_9)) True) % 13.73/13.94 Clause #746 (by clausification #[741]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 13.73/13.94 Eq (object (skS.0 3 a) (skS.0 11 a (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) a_8 a_9)) True % 13.73/13.94 Clause #747 (by superposition #[746, 154]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 13.73/13.94 Or (Eq True False) % 13.73/13.94 (Eq (unisex (skS.0 3 a) (skS.0 11 a (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) a_8 a_9)) True) % 13.73/13.94 Clause #824 (by clausification #[747]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 13.73/13.94 Eq (unisex (skS.0 3 a) (skS.0 11 a (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) a_8 a_9)) True % 13.73/13.94 Clause #825 (by superposition #[824, 224]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 13.73/13.94 Or (Eq True False) % 13.73/13.94 (Eq (male (skS.0 3 a) (skS.0 11 a (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) a_8 a_9)) False) % 13.73/13.94 Clause #830 (by clausification #[825]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 13.73/13.94 Eq (male (skS.0 3 a) (skS.0 11 a (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) a_8 a_9)) False % 13.73/13.94 Clause #885 (by clausification #[436]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 13.73/13.94 Eq % 13.73/13.94 (be (skS.0 3 a) (skS.0 10 a (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) a_8) % 13.73/13.94 (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) % 13.73/13.94 (skS.0 11 a (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) a_8 a_9)) % 13.73/13.94 True % 13.73/13.94 Clause #886 (by superposition #[885, 249]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 13.73/13.95 Or (Eq True False) % 13.73/13.95 (Eq (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) % 13.73/13.95 (skS.0 11 a (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) a_8 a_9)) % 13.73/13.95 Clause #1027 (by clausification #[886]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 13.73/13.95 Eq (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) % 13.73/13.95 (skS.0 11 a (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) a_8 a_9) % 13.73/13.95 Clause #1038 (by backward demodulation #[1027, 830]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 13.73/13.95 Eq (male (skS.0 3 a) (skS.0 1 (skS.0 3 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6) a_7)) False % 13.73/13.95 Clause #1044 (by superposition #[1038, 343]): Eq False True % 13.73/13.95 Clause #1049 (by clausification #[1044]): False % 13.73/13.95 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------