%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : PUZ031+3 : TPTP v9.2.0. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n003.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:58:14 PM UTC 2025 % Result : Theorem 9.14s 9.30s % Output : Proof 9.29s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : PUZ031+3 : TPTP v9.2.0. Released v4.1.0. % 0.03/0.13 % Command : duper %s % 0.13/0.34 % Computer : n003.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 20:47:23 EDT 2025 % 0.13/0.34 % CPUTime : % 9.14/9.30 SZS status Theorem for theBenchmark.p % 9.14/9.30 SZS output start Proof for theBenchmark.p % 9.14/9.30 Clause #3 (by assumption #[]): Eq (Exists fun A => wolf A) True % 9.14/9.30 Clause #4 (by assumption #[]): Eq (∀ (A : Iota), wolf A → animal A) True % 9.14/9.30 Clause #5 (by assumption #[]): Eq (Exists fun A => fox A) True % 9.14/9.30 Clause #6 (by assumption #[]): Eq (∀ (A : Iota), fox A → animal A) True % 9.14/9.30 Clause #7 (by assumption #[]): Eq (Exists fun A => bird A) True % 9.14/9.30 Clause #8 (by assumption #[]): Eq (∀ (A : Iota), bird A → animal A) True % 9.14/9.30 Clause #11 (by assumption #[]): Eq (Exists fun A => snail A) True % 9.14/9.30 Clause #12 (by assumption #[]): Eq (∀ (A : Iota), snail A → animal A) True % 9.14/9.30 Clause #13 (by assumption #[]): Eq (Exists fun A => plant A) True % 9.14/9.30 Clause #15 (by assumption #[]): Eq (Exists fun A => grain A) True % 9.14/9.30 Clause #16 (by assumption #[]): Eq (∀ (A : Iota), grain A → plant A) True % 9.14/9.30 Clause #17 (by assumption #[]): Eq % 9.14/9.30 (∀ (X : Iota), % 9.14/9.30 animal X → % 9.14/9.30 Or (∀ (Y : Iota), plant Y → eats X Y) % 9.14/9.30 (∀ (Y1 : Iota), animal Y1 → And (much_smaller Y1 X) (Exists fun Z => And (plant Z) (eats Y1 Z)) → eats X Y1)) % 9.14/9.30 True % 9.14/9.30 Clause #18 (by assumption #[]): Eq (∀ (Y X : Iota), And (bird Y) (snail X) → much_smaller X Y) True % 9.14/9.30 Clause #20 (by assumption #[]): Eq (∀ (X Y : Iota), And (bird X) (fox Y) → much_smaller X Y) True % 9.14/9.30 Clause #21 (by assumption #[]): Eq (∀ (X Y : Iota), And (fox X) (wolf Y) → much_smaller X Y) True % 9.14/9.30 Clause #22 (by assumption #[]): Eq (∀ (X Y : Iota), And (wolf X) (fox Y) → Not (eats X Y)) True % 9.14/9.30 Clause #23 (by assumption #[]): Eq (∀ (X Y : Iota), And (wolf X) (grain Y) → Not (eats X Y)) True % 9.14/9.30 Clause #25 (by assumption #[]): Eq (∀ (X Y : Iota), And (bird X) (snail Y) → Not (eats X Y)) True % 9.14/9.30 Clause #27 (by assumption #[]): Eq (∀ (X : Iota), snail X → Exists fun Y => And (plant Y) (eats X Y)) True % 9.14/9.30 Clause #28 (by assumption #[]): Eq % 9.14/9.30 (Not % 9.14/9.30 (Exists fun X => % 9.14/9.30 Exists fun Y => Exists fun Z => And (And (And (And (animal X) (animal Y)) (grain Z)) (eats Y Z)) (eats X Y))) % 9.14/9.30 True % 9.14/9.30 Clause #29 (by clausification #[16]): ∀ (a : Iota), Eq (grain a → plant a) True % 9.14/9.30 Clause #30 (by clausification #[29]): ∀ (a : Iota), Or (Eq (grain a) False) (Eq (plant a) True) % 9.14/9.30 Clause #33 (by clausification #[12]): ∀ (a : Iota), Eq (snail a → animal a) True % 9.14/9.30 Clause #34 (by clausification #[33]): ∀ (a : Iota), Or (Eq (snail a) False) (Eq (animal a) True) % 9.14/9.30 Clause #37 (by clausification #[8]): ∀ (a : Iota), Eq (bird a → animal a) True % 9.14/9.30 Clause #38 (by clausification #[37]): ∀ (a : Iota), Or (Eq (bird a) False) (Eq (animal a) True) % 9.14/9.30 Clause #41 (by clausification #[6]): ∀ (a : Iota), Eq (fox a → animal a) True % 9.14/9.30 Clause #42 (by clausification #[41]): ∀ (a : Iota), Or (Eq (fox a) False) (Eq (animal a) True) % 9.14/9.30 Clause #43 (by clausification #[4]): ∀ (a : Iota), Eq (wolf a → animal a) True % 9.14/9.30 Clause #44 (by clausification #[43]): ∀ (a : Iota), Or (Eq (wolf a) False) (Eq (animal a) True) % 9.14/9.30 Clause #47 (by betaEtaReduce #[3]): Eq (Exists wolf) True % 9.14/9.30 Clause #48 (by clausification #[47]): ∀ (a : Iota), Eq (wolf (skS.0 1 a)) True % 9.14/9.30 Clause #49 (by superposition #[48, 44]): ∀ (a : Iota), Or (Eq True False) (Eq (animal (skS.0 1 a)) True) % 9.14/9.30 Clause #53 (by betaEtaReduce #[5]): Eq (Exists fox) True % 9.14/9.30 Clause #54 (by clausification #[53]): ∀ (a : Iota), Eq (fox (skS.0 3 a)) True % 9.14/9.30 Clause #55 (by superposition #[54, 42]): ∀ (a : Iota), Or (Eq True False) (Eq (animal (skS.0 3 a)) True) % 9.14/9.30 Clause #56 (by betaEtaReduce #[7]): Eq (Exists bird) True % 9.14/9.30 Clause #57 (by clausification #[56]): ∀ (a : Iota), Eq (bird (skS.0 4 a)) True % 9.14/9.30 Clause #58 (by superposition #[57, 38]): ∀ (a : Iota), Or (Eq True False) (Eq (animal (skS.0 4 a)) True) % 9.14/9.30 Clause #59 (by betaEtaReduce #[13]): Eq (Exists plant) True % 9.14/9.30 Clause #60 (by clausification #[59]): ∀ (a : Iota), Eq (plant (skS.0 5 a)) True % 9.14/9.30 Clause #65 (by betaEtaReduce #[15]): Eq (Exists grain) True % 9.14/9.30 Clause #66 (by clausification #[65]): ∀ (a : Iota), Eq (grain (skS.0 7 a)) True % 9.14/9.30 Clause #67 (by superposition #[66, 30]): ∀ (a : Iota), Or (Eq True False) (Eq (plant (skS.0 7 a)) True) % 9.14/9.30 Clause #68 (by betaEtaReduce #[11]): Eq (Exists snail) True % 9.14/9.32 Clause #69 (by clausification #[68]): ∀ (a : Iota), Eq (snail (skS.0 8 a)) True % 9.14/9.32 Clause #70 (by superposition #[69, 34]): ∀ (a : Iota), Or (Eq True False) (Eq (animal (skS.0 8 a)) True) % 9.14/9.32 Clause #71 (by clausification #[17]): ∀ (a : Iota), % 9.14/9.32 Eq % 9.14/9.32 (animal a → % 9.14/9.32 Or (∀ (Y : Iota), plant Y → eats a Y) % 9.14/9.32 (∀ (Y1 : Iota), animal Y1 → And (much_smaller Y1 a) (Exists fun Z => And (plant Z) (eats Y1 Z)) → eats a Y1)) % 9.14/9.32 True % 9.14/9.32 Clause #72 (by clausification #[71]): ∀ (a : Iota), % 9.14/9.32 Or (Eq (animal a) False) % 9.14/9.32 (Eq % 9.14/9.32 (Or (∀ (Y : Iota), plant Y → eats a Y) % 9.14/9.32 (∀ (Y1 : Iota), animal Y1 → And (much_smaller Y1 a) (Exists fun Z => And (plant Z) (eats Y1 Z)) → eats a Y1)) % 9.14/9.32 True) % 9.14/9.32 Clause #73 (by clausification #[72]): ∀ (a : Iota), % 9.14/9.32 Or (Eq (animal a) False) % 9.14/9.32 (Or (Eq (∀ (Y : Iota), plant Y → eats a Y) True) % 9.14/9.32 (Eq (∀ (Y1 : Iota), animal Y1 → And (much_smaller Y1 a) (Exists fun Z => And (plant Z) (eats Y1 Z)) → eats a Y1) % 9.14/9.32 True)) % 9.14/9.32 Clause #74 (by clausification #[73]): ∀ (a a_1 : Iota), % 9.14/9.32 Or (Eq (animal a) False) % 9.14/9.32 (Or % 9.14/9.32 (Eq (∀ (Y1 : Iota), animal Y1 → And (much_smaller Y1 a) (Exists fun Z => And (plant Z) (eats Y1 Z)) → eats a Y1) % 9.14/9.32 True) % 9.14/9.32 (Eq (plant a_1 → eats a a_1) True)) % 9.14/9.32 Clause #75 (by clausification #[74]): ∀ (a a_1 a_2 : Iota), % 9.14/9.32 Or (Eq (animal a) False) % 9.14/9.32 (Or (Eq (plant a_1 → eats a a_1) True) % 9.14/9.32 (Eq (animal a_2 → And (much_smaller a_2 a) (Exists fun Z => And (plant Z) (eats a_2 Z)) → eats a a_2) True)) % 9.14/9.32 Clause #76 (by clausification #[75]): ∀ (a a_1 a_2 : Iota), % 9.14/9.32 Or (Eq (animal a) False) % 9.14/9.32 (Or (Eq (animal a_1 → And (much_smaller a_1 a) (Exists fun Z => And (plant Z) (eats a_1 Z)) → eats a a_1) True) % 9.14/9.32 (Or (Eq (plant a_2) False) (Eq (eats a a_2) True))) % 9.14/9.32 Clause #77 (by clausification #[76]): ∀ (a a_1 a_2 : Iota), % 9.14/9.32 Or (Eq (animal a) False) % 9.14/9.32 (Or (Eq (plant a_1) False) % 9.14/9.32 (Or (Eq (eats a a_1) True) % 9.14/9.32 (Or (Eq (animal a_2) False) % 9.14/9.32 (Eq (And (much_smaller a_2 a) (Exists fun Z => And (plant Z) (eats a_2 Z)) → eats a a_2) True)))) % 9.14/9.32 Clause #78 (by clausification #[77]): ∀ (a a_1 a_2 : Iota), % 9.14/9.32 Or (Eq (animal a) False) % 9.14/9.32 (Or (Eq (plant a_1) False) % 9.14/9.32 (Or (Eq (eats a a_1) True) % 9.14/9.32 (Or (Eq (animal a_2) False) % 9.14/9.32 (Or (Eq (And (much_smaller a_2 a) (Exists fun Z => And (plant Z) (eats a_2 Z))) False) % 9.14/9.32 (Eq (eats a a_2) True))))) % 9.14/9.32 Clause #79 (by clausification #[78]): ∀ (a a_1 a_2 : Iota), % 9.14/9.32 Or (Eq (animal a) False) % 9.14/9.32 (Or (Eq (plant a_1) False) % 9.14/9.32 (Or (Eq (eats a a_1) True) % 9.14/9.32 (Or (Eq (animal a_2) False) % 9.14/9.32 (Or (Eq (eats a a_2) True) % 9.14/9.32 (Or (Eq (much_smaller a_2 a) False) (Eq (Exists fun Z => And (plant Z) (eats a_2 Z)) False)))))) % 9.14/9.32 Clause #80 (by clausification #[79]): ∀ (a a_1 a_2 a_3 : Iota), % 9.14/9.32 Or (Eq (animal a) False) % 9.14/9.32 (Or (Eq (plant a_1) False) % 9.14/9.32 (Or (Eq (eats a a_1) True) % 9.14/9.32 (Or (Eq (animal a_2) False) % 9.14/9.32 (Or (Eq (eats a a_2) True) % 9.14/9.32 (Or (Eq (much_smaller a_2 a) False) (Eq (And (plant a_3) (eats a_2 a_3)) False)))))) % 9.14/9.32 Clause #81 (by clausification #[80]): ∀ (a a_1 a_2 a_3 : Iota), % 9.14/9.32 Or (Eq (animal a) False) % 9.14/9.32 (Or (Eq (plant a_1) False) % 9.14/9.32 (Or (Eq (eats a a_1) True) % 9.14/9.32 (Or (Eq (animal a_2) False) % 9.14/9.32 (Or (Eq (eats a a_2) True) % 9.14/9.32 (Or (Eq (much_smaller a_2 a) False) (Or (Eq (plant a_3) False) (Eq (eats a_2 a_3) False))))))) % 9.14/9.32 Clause #83 (by clausification #[21]): ∀ (a : Iota), Eq (∀ (Y : Iota), And (fox a) (wolf Y) → much_smaller a Y) True % 9.14/9.32 Clause #84 (by clausification #[83]): ∀ (a a_1 : Iota), Eq (And (fox a) (wolf a_1) → much_smaller a a_1) True % 9.14/9.32 Clause #85 (by clausification #[84]): ∀ (a a_1 : Iota), Or (Eq (And (fox a) (wolf a_1)) False) (Eq (much_smaller a a_1) True) % 9.14/9.32 Clause #86 (by clausification #[85]): ∀ (a a_1 : Iota), Or (Eq (much_smaller a a_1) True) (Or (Eq (fox a) False) (Eq (wolf a_1) False)) % 9.14/9.32 Clause #87 (by superposition #[86, 54]): ∀ (a a_1 : Iota), Or (Eq (much_smaller (skS.0 3 a) a_1) True) (Or (Eq (wolf a_1) False) (Eq False True)) % 9.14/9.32 Clause #88 (by clausification #[20]): ∀ (a : Iota), Eq (∀ (Y : Iota), And (bird a) (fox Y) → much_smaller a Y) True % 9.14/9.35 Clause #89 (by clausification #[88]): ∀ (a a_1 : Iota), Eq (And (bird a) (fox a_1) → much_smaller a a_1) True % 9.14/9.35 Clause #90 (by clausification #[89]): ∀ (a a_1 : Iota), Or (Eq (And (bird a) (fox a_1)) False) (Eq (much_smaller a a_1) True) % 9.14/9.35 Clause #91 (by clausification #[90]): ∀ (a a_1 : Iota), Or (Eq (much_smaller a a_1) True) (Or (Eq (bird a) False) (Eq (fox a_1) False)) % 9.14/9.35 Clause #92 (by superposition #[91, 57]): ∀ (a a_1 : Iota), Or (Eq (much_smaller (skS.0 4 a) a_1) True) (Or (Eq (fox a_1) False) (Eq False True)) % 9.14/9.35 Clause #98 (by clausification #[18]): ∀ (a : Iota), Eq (∀ (X : Iota), And (bird a) (snail X) → much_smaller X a) True % 9.14/9.35 Clause #99 (by clausification #[98]): ∀ (a a_1 : Iota), Eq (And (bird a) (snail a_1) → much_smaller a_1 a) True % 9.14/9.35 Clause #100 (by clausification #[99]): ∀ (a a_1 : Iota), Or (Eq (And (bird a) (snail a_1)) False) (Eq (much_smaller a_1 a) True) % 9.14/9.35 Clause #101 (by clausification #[100]): ∀ (a a_1 : Iota), Or (Eq (much_smaller a a_1) True) (Or (Eq (bird a_1) False) (Eq (snail a) False)) % 9.14/9.35 Clause #102 (by superposition #[101, 57]): ∀ (a a_1 : Iota), Or (Eq (much_smaller a (skS.0 4 a_1)) True) (Or (Eq (snail a) False) (Eq False True)) % 9.14/9.35 Clause #108 (by clausification #[22]): ∀ (a : Iota), Eq (∀ (Y : Iota), And (wolf a) (fox Y) → Not (eats a Y)) True % 9.14/9.35 Clause #109 (by clausification #[108]): ∀ (a a_1 : Iota), Eq (And (wolf a) (fox a_1) → Not (eats a a_1)) True % 9.14/9.35 Clause #110 (by clausification #[109]): ∀ (a a_1 : Iota), Or (Eq (And (wolf a) (fox a_1)) False) (Eq (Not (eats a a_1)) True) % 9.14/9.35 Clause #111 (by clausification #[110]): ∀ (a a_1 : Iota), Or (Eq (Not (eats a a_1)) True) (Or (Eq (wolf a) False) (Eq (fox a_1) False)) % 9.14/9.35 Clause #112 (by clausification #[111]): ∀ (a a_1 : Iota), Or (Eq (wolf a) False) (Or (Eq (fox a_1) False) (Eq (eats a a_1) False)) % 9.14/9.35 Clause #113 (by superposition #[112, 48]): ∀ (a a_1 : Iota), Or (Eq (fox a) False) (Or (Eq (eats (skS.0 1 a_1) a) False) (Eq False True)) % 9.14/9.35 Clause #114 (by clausification #[25]): ∀ (a : Iota), Eq (∀ (Y : Iota), And (bird a) (snail Y) → Not (eats a Y)) True % 9.14/9.35 Clause #115 (by clausification #[114]): ∀ (a a_1 : Iota), Eq (And (bird a) (snail a_1) → Not (eats a a_1)) True % 9.14/9.35 Clause #116 (by clausification #[115]): ∀ (a a_1 : Iota), Or (Eq (And (bird a) (snail a_1)) False) (Eq (Not (eats a a_1)) True) % 9.14/9.35 Clause #117 (by clausification #[116]): ∀ (a a_1 : Iota), Or (Eq (Not (eats a a_1)) True) (Or (Eq (bird a) False) (Eq (snail a_1) False)) % 9.14/9.35 Clause #118 (by clausification #[117]): ∀ (a a_1 : Iota), Or (Eq (bird a) False) (Or (Eq (snail a_1) False) (Eq (eats a a_1) False)) % 9.14/9.35 Clause #119 (by superposition #[118, 57]): ∀ (a a_1 : Iota), Or (Eq (snail a) False) (Or (Eq (eats (skS.0 4 a_1) a) False) (Eq False True)) % 9.14/9.35 Clause #120 (by clausification #[23]): ∀ (a : Iota), Eq (∀ (Y : Iota), And (wolf a) (grain Y) → Not (eats a Y)) True % 9.14/9.35 Clause #121 (by clausification #[120]): ∀ (a a_1 : Iota), Eq (And (wolf a) (grain a_1) → Not (eats a a_1)) True % 9.14/9.35 Clause #122 (by clausification #[121]): ∀ (a a_1 : Iota), Or (Eq (And (wolf a) (grain a_1)) False) (Eq (Not (eats a a_1)) True) % 9.14/9.35 Clause #123 (by clausification #[122]): ∀ (a a_1 : Iota), Or (Eq (Not (eats a a_1)) True) (Or (Eq (wolf a) False) (Eq (grain a_1) False)) % 9.14/9.35 Clause #124 (by clausification #[123]): ∀ (a a_1 : Iota), Or (Eq (wolf a) False) (Or (Eq (grain a_1) False) (Eq (eats a a_1) False)) % 9.14/9.35 Clause #125 (by superposition #[124, 48]): ∀ (a a_1 : Iota), Or (Eq (grain a) False) (Or (Eq (eats (skS.0 1 a_1) a) False) (Eq False True)) % 9.14/9.35 Clause #137 (by clausification #[67]): ∀ (a : Iota), Eq (plant (skS.0 7 a)) True % 9.14/9.35 Clause #140 (by clausification #[70]): ∀ (a : Iota), Eq (animal (skS.0 8 a)) True % 9.14/9.35 Clause #145 (by clausification #[27]): ∀ (a : Iota), Eq (snail a → Exists fun Y => And (plant Y) (eats a Y)) True % 9.14/9.35 Clause #146 (by clausification #[145]): ∀ (a : Iota), Or (Eq (snail a) False) (Eq (Exists fun Y => And (plant Y) (eats a Y)) True) % 9.14/9.35 Clause #147 (by clausification #[146]): ∀ (a a_1 : Iota), Or (Eq (snail a) False) (Eq (And (plant (skS.0 10 a a_1)) (eats a (skS.0 10 a a_1))) True) % 9.20/9.38 Clause #148 (by clausification #[147]): ∀ (a a_1 : Iota), Or (Eq (snail a) False) (Eq (eats a (skS.0 10 a a_1)) True) % 9.20/9.38 Clause #149 (by clausification #[147]): ∀ (a a_1 : Iota), Or (Eq (snail a) False) (Eq (plant (skS.0 10 a a_1)) True) % 9.20/9.38 Clause #150 (by superposition #[148, 69]): ∀ (a a_1 : Iota), Or (Eq (eats (skS.0 8 a) (skS.0 10 (skS.0 8 a) a_1)) True) (Eq False True) % 9.20/9.38 Clause #151 (by clausification #[49]): ∀ (a : Iota), Eq (animal (skS.0 1 a)) True % 9.20/9.38 Clause #153 (by superposition #[151, 81]): ∀ (a a_1 a_2 a_3 : Iota), % 9.20/9.38 Or (Eq True False) % 9.20/9.38 (Or (Eq (plant a) False) % 9.20/9.38 (Or (Eq (eats (skS.0 1 a_1) a) True) % 9.20/9.38 (Or (Eq (animal a_2) False) % 9.20/9.38 (Or (Eq (eats (skS.0 1 a_1) a_2) True) % 9.20/9.38 (Or (Eq (much_smaller a_2 (skS.0 1 a_1)) False) (Or (Eq (plant a_3) False) (Eq (eats a_2 a_3) False))))))) % 9.20/9.38 Clause #155 (by clausification #[55]): ∀ (a : Iota), Eq (animal (skS.0 3 a)) True % 9.20/9.38 Clause #157 (by superposition #[155, 81]): ∀ (a a_1 a_2 a_3 : Iota), % 9.20/9.38 Or (Eq True False) % 9.20/9.38 (Or (Eq (plant a) False) % 9.20/9.38 (Or (Eq (eats (skS.0 3 a_1) a) True) % 9.20/9.38 (Or (Eq (animal a_2) False) % 9.20/9.38 (Or (Eq (eats (skS.0 3 a_1) a_2) True) % 9.20/9.38 (Or (Eq (much_smaller a_2 (skS.0 3 a_1)) False) (Or (Eq (plant a_3) False) (Eq (eats a_2 a_3) False))))))) % 9.20/9.38 Clause #159 (by clausification #[58]): ∀ (a : Iota), Eq (animal (skS.0 4 a)) True % 9.20/9.38 Clause #161 (by superposition #[159, 81]): ∀ (a a_1 a_2 a_3 : Iota), % 9.20/9.38 Or (Eq True False) % 9.20/9.38 (Or (Eq (plant a) False) % 9.20/9.38 (Or (Eq (eats (skS.0 4 a_1) a) True) % 9.20/9.38 (Or (Eq (animal a_2) False) % 9.20/9.38 (Or (Eq (eats (skS.0 4 a_1) a_2) True) % 9.20/9.38 (Or (Eq (much_smaller a_2 (skS.0 4 a_1)) False) (Or (Eq (plant a_3) False) (Eq (eats a_2 a_3) False))))))) % 9.20/9.38 Clause #162 (by clausification #[28]): Eq % 9.20/9.38 (Exists fun X => % 9.20/9.38 Exists fun Y => Exists fun Z => And (And (And (And (animal X) (animal Y)) (grain Z)) (eats Y Z)) (eats X Y)) % 9.20/9.38 False % 9.20/9.38 Clause #163 (by clausification #[162]): ∀ (a : Iota), % 9.20/9.38 Eq (Exists fun Y => Exists fun Z => And (And (And (And (animal a) (animal Y)) (grain Z)) (eats Y Z)) (eats a Y)) False % 9.20/9.38 Clause #164 (by clausification #[163]): ∀ (a a_1 : Iota), % 9.20/9.38 Eq (Exists fun Z => And (And (And (And (animal a) (animal a_1)) (grain Z)) (eats a_1 Z)) (eats a a_1)) False % 9.20/9.38 Clause #165 (by clausification #[164]): ∀ (a a_1 a_2 : Iota), Eq (And (And (And (And (animal a) (animal a_1)) (grain a_2)) (eats a_1 a_2)) (eats a a_1)) False % 9.20/9.38 Clause #166 (by clausification #[165]): ∀ (a a_1 a_2 : Iota), % 9.20/9.38 Or (Eq (And (And (And (animal a) (animal a_1)) (grain a_2)) (eats a_1 a_2)) False) (Eq (eats a a_1) False) % 9.20/9.38 Clause #167 (by clausification #[166]): ∀ (a a_1 a_2 : Iota), % 9.20/9.38 Or (Eq (eats a a_1) False) (Or (Eq (And (And (animal a) (animal a_1)) (grain a_2)) False) (Eq (eats a_1 a_2) False)) % 9.20/9.38 Clause #168 (by clausification #[167]): ∀ (a a_1 a_2 : Iota), % 9.20/9.38 Or (Eq (eats a a_1) False) % 9.20/9.38 (Or (Eq (eats a_1 a_2) False) (Or (Eq (And (animal a) (animal a_1)) False) (Eq (grain a_2) False))) % 9.20/9.38 Clause #169 (by clausification #[168]): ∀ (a a_1 a_2 : Iota), % 9.20/9.38 Or (Eq (eats a a_1) False) % 9.20/9.38 (Or (Eq (eats a_1 a_2) False) (Or (Eq (grain a_2) False) (Or (Eq (animal a) False) (Eq (animal a_1) False)))) % 9.20/9.38 Clause #172 (by superposition #[149, 69]): ∀ (a a_1 : Iota), Or (Eq (plant (skS.0 10 (skS.0 8 a) a_1)) True) (Eq False True) % 9.20/9.38 Clause #175 (by clausification #[92]): ∀ (a a_1 : Iota), Or (Eq (much_smaller (skS.0 4 a) a_1) True) (Eq (fox a_1) False) % 9.20/9.38 Clause #176 (by superposition #[175, 54]): ∀ (a a_1 : Iota), Or (Eq (much_smaller (skS.0 4 a) (skS.0 3 a_1)) True) (Eq False True) % 9.20/9.38 Clause #182 (by clausification #[102]): ∀ (a a_1 : Iota), Or (Eq (much_smaller a (skS.0 4 a_1)) True) (Eq (snail a) False) % 9.20/9.38 Clause #183 (by superposition #[182, 69]): ∀ (a a_1 : Iota), Or (Eq (much_smaller (skS.0 8 a) (skS.0 4 a_1)) True) (Eq False True) % 9.20/9.38 Clause #184 (by clausification #[113]): ∀ (a a_1 : Iota), Or (Eq (fox a) False) (Eq (eats (skS.0 1 a_1) a) False) % 9.20/9.38 Clause #185 (by superposition #[184, 54]): ∀ (a a_1 : Iota), Or (Eq (eats (skS.0 1 a) (skS.0 3 a_1)) False) (Eq False True) % 9.20/9.41 Clause #186 (by clausification #[119]): ∀ (a a_1 : Iota), Or (Eq (snail a) False) (Eq (eats (skS.0 4 a_1) a) False) % 9.20/9.41 Clause #187 (by superposition #[186, 69]): ∀ (a a_1 : Iota), Or (Eq (eats (skS.0 4 a) (skS.0 8 a_1)) False) (Eq False True) % 9.20/9.41 Clause #188 (by clausification #[125]): ∀ (a a_1 : Iota), Or (Eq (grain a) False) (Eq (eats (skS.0 1 a_1) a) False) % 9.20/9.41 Clause #189 (by superposition #[188, 66]): ∀ (a a_1 : Iota), Or (Eq (eats (skS.0 1 a) (skS.0 7 a_1)) False) (Eq False True) % 9.20/9.41 Clause #190 (by clausification #[87]): ∀ (a a_1 : Iota), Or (Eq (much_smaller (skS.0 3 a) a_1) True) (Eq (wolf a_1) False) % 9.20/9.41 Clause #191 (by superposition #[190, 48]): ∀ (a a_1 : Iota), Or (Eq (much_smaller (skS.0 3 a) (skS.0 1 a_1)) True) (Eq False True) % 9.20/9.41 Clause #192 (by clausification #[176]): ∀ (a a_1 : Iota), Eq (much_smaller (skS.0 4 a) (skS.0 3 a_1)) True % 9.20/9.41 Clause #194 (by clausification #[191]): ∀ (a a_1 : Iota), Eq (much_smaller (skS.0 3 a) (skS.0 1 a_1)) True % 9.20/9.41 Clause #195 (by clausification #[189]): ∀ (a a_1 : Iota), Eq (eats (skS.0 1 a) (skS.0 7 a_1)) False % 9.20/9.41 Clause #201 (by clausification #[183]): ∀ (a a_1 : Iota), Eq (much_smaller (skS.0 8 a) (skS.0 4 a_1)) True % 9.20/9.41 Clause #202 (by clausification #[185]): ∀ (a a_1 : Iota), Eq (eats (skS.0 1 a) (skS.0 3 a_1)) False % 9.20/9.41 Clause #203 (by clausification #[187]): ∀ (a a_1 : Iota), Eq (eats (skS.0 4 a) (skS.0 8 a_1)) False % 9.20/9.41 Clause #204 (by clausification #[172]): ∀ (a a_1 : Iota), Eq (plant (skS.0 10 (skS.0 8 a) a_1)) True % 9.20/9.41 Clause #216 (by clausification #[150]): ∀ (a a_1 : Iota), Eq (eats (skS.0 8 a) (skS.0 10 (skS.0 8 a) a_1)) True % 9.20/9.41 Clause #228 (by clausification #[157]): ∀ (a a_1 a_2 a_3 : Iota), % 9.20/9.41 Or (Eq (plant a) False) % 9.20/9.41 (Or (Eq (eats (skS.0 3 a_1) a) True) % 9.20/9.41 (Or (Eq (animal a_2) False) % 9.20/9.41 (Or (Eq (eats (skS.0 3 a_1) a_2) True) % 9.20/9.41 (Or (Eq (much_smaller a_2 (skS.0 3 a_1)) False) (Or (Eq (plant a_3) False) (Eq (eats a_2 a_3) False)))))) % 9.20/9.41 Clause #229 (by superposition #[228, 60]): ∀ (a a_1 a_2 a_3 : Iota), % 9.20/9.41 Or (Eq (eats (skS.0 3 a) (skS.0 5 a_1)) True) % 9.20/9.41 (Or (Eq (animal a_2) False) % 9.20/9.41 (Or (Eq (eats (skS.0 3 a) a_2) True) % 9.20/9.41 (Or (Eq (much_smaller a_2 (skS.0 3 a)) False) % 9.20/9.41 (Or (Eq (plant a_3) False) (Or (Eq (eats a_2 a_3) False) (Eq False True)))))) % 9.20/9.41 Clause #233 (by clausification #[161]): ∀ (a a_1 a_2 a_3 : Iota), % 9.20/9.41 Or (Eq (plant a) False) % 9.20/9.41 (Or (Eq (eats (skS.0 4 a_1) a) True) % 9.20/9.41 (Or (Eq (animal a_2) False) % 9.20/9.41 (Or (Eq (eats (skS.0 4 a_1) a_2) True) % 9.20/9.41 (Or (Eq (much_smaller a_2 (skS.0 4 a_1)) False) (Or (Eq (plant a_3) False) (Eq (eats a_2 a_3) False)))))) % 9.20/9.41 Clause #235 (by superposition #[233, 137]): ∀ (a a_1 a_2 a_3 : Iota), % 9.20/9.41 Or (Eq (eats (skS.0 4 a) (skS.0 7 a_1)) True) % 9.20/9.41 (Or (Eq (animal a_2) False) % 9.20/9.41 (Or (Eq (eats (skS.0 4 a) a_2) True) % 9.20/9.41 (Or (Eq (much_smaller a_2 (skS.0 4 a)) False) % 9.20/9.41 (Or (Eq (plant a_3) False) (Or (Eq (eats a_2 a_3) False) (Eq False True)))))) % 9.20/9.41 Clause #238 (by clausification #[153]): ∀ (a a_1 a_2 a_3 : Iota), % 9.20/9.41 Or (Eq (plant a) False) % 9.20/9.41 (Or (Eq (eats (skS.0 1 a_1) a) True) % 9.20/9.41 (Or (Eq (animal a_2) False) % 9.20/9.41 (Or (Eq (eats (skS.0 1 a_1) a_2) True) % 9.20/9.41 (Or (Eq (much_smaller a_2 (skS.0 1 a_1)) False) (Or (Eq (plant a_3) False) (Eq (eats a_2 a_3) False)))))) % 9.20/9.41 Clause #240 (by superposition #[238, 137]): ∀ (a a_1 a_2 a_3 : Iota), % 9.20/9.41 Or (Eq (eats (skS.0 1 a) (skS.0 7 a_1)) True) % 9.20/9.41 (Or (Eq (animal a_2) False) % 9.20/9.41 (Or (Eq (eats (skS.0 1 a) a_2) True) % 9.20/9.41 (Or (Eq (much_smaller a_2 (skS.0 1 a)) False) % 9.20/9.41 (Or (Eq (plant a_3) False) (Or (Eq (eats a_2 a_3) False) (Eq False True)))))) % 9.20/9.41 Clause #288 (by clausification #[235]): ∀ (a a_1 a_2 a_3 : Iota), % 9.20/9.41 Or (Eq (eats (skS.0 4 a) (skS.0 7 a_1)) True) % 9.20/9.41 (Or (Eq (animal a_2) False) % 9.20/9.41 (Or (Eq (eats (skS.0 4 a) a_2) True) % 9.20/9.41 (Or (Eq (much_smaller a_2 (skS.0 4 a)) False) (Or (Eq (plant a_3) False) (Eq (eats a_2 a_3) False))))) % 9.20/9.41 Clause #291 (by superposition #[288, 140]): ∀ (a a_1 a_2 a_3 : Iota), % 9.20/9.41 Or (Eq (eats (skS.0 4 a) (skS.0 7 a_1)) True) % 9.20/9.44 (Or (Eq (eats (skS.0 4 a) (skS.0 8 a_2)) True) % 9.20/9.44 (Or (Eq (much_smaller (skS.0 8 a_2) (skS.0 4 a)) False) % 9.20/9.44 (Or (Eq (plant a_3) False) (Or (Eq (eats (skS.0 8 a_2) a_3) False) (Eq False True))))) % 9.20/9.44 Clause #319 (by clausification #[229]): ∀ (a a_1 a_2 a_3 : Iota), % 9.20/9.44 Or (Eq (eats (skS.0 3 a) (skS.0 5 a_1)) True) % 9.20/9.44 (Or (Eq (animal a_2) False) % 9.20/9.44 (Or (Eq (eats (skS.0 3 a) a_2) True) % 9.20/9.44 (Or (Eq (much_smaller a_2 (skS.0 3 a)) False) (Or (Eq (plant a_3) False) (Eq (eats a_2 a_3) False))))) % 9.20/9.44 Clause #325 (by superposition #[319, 159]): ∀ (a a_1 a_2 a_3 : Iota), % 9.20/9.44 Or (Eq (eats (skS.0 3 a) (skS.0 5 a_1)) True) % 9.20/9.44 (Or (Eq (eats (skS.0 3 a) (skS.0 4 a_2)) True) % 9.20/9.44 (Or (Eq (much_smaller (skS.0 4 a_2) (skS.0 3 a)) False) % 9.20/9.44 (Or (Eq (plant a_3) False) (Or (Eq (eats (skS.0 4 a_2) a_3) False) (Eq False True))))) % 9.20/9.44 Clause #326 (by clausification #[240]): ∀ (a a_1 a_2 a_3 : Iota), % 9.20/9.44 Or (Eq (eats (skS.0 1 a) (skS.0 7 a_1)) True) % 9.20/9.44 (Or (Eq (animal a_2) False) % 9.20/9.44 (Or (Eq (eats (skS.0 1 a) a_2) True) % 9.20/9.44 (Or (Eq (much_smaller a_2 (skS.0 1 a)) False) (Or (Eq (plant a_3) False) (Eq (eats a_2 a_3) False))))) % 9.20/9.44 Clause #331 (by superposition #[326, 155]): ∀ (a a_1 a_2 a_3 : Iota), % 9.20/9.44 Or (Eq (eats (skS.0 1 a) (skS.0 7 a_1)) True) % 9.20/9.44 (Or (Eq (eats (skS.0 1 a) (skS.0 3 a_2)) True) % 9.20/9.44 (Or (Eq (much_smaller (skS.0 3 a_2) (skS.0 1 a)) False) % 9.20/9.44 (Or (Eq (plant a_3) False) (Or (Eq (eats (skS.0 3 a_2) a_3) False) (Eq False True))))) % 9.20/9.44 Clause #419 (by clausification #[331]): ∀ (a a_1 a_2 a_3 : Iota), % 9.20/9.44 Or (Eq (eats (skS.0 1 a) (skS.0 7 a_1)) True) % 9.20/9.44 (Or (Eq (eats (skS.0 1 a) (skS.0 3 a_2)) True) % 9.20/9.44 (Or (Eq (much_smaller (skS.0 3 a_2) (skS.0 1 a)) False) % 9.20/9.44 (Or (Eq (plant a_3) False) (Eq (eats (skS.0 3 a_2) a_3) False)))) % 9.20/9.44 Clause #420 (by forward demodulation #[419, 202]): ∀ (a a_1 a_2 a_3 : Iota), % 9.20/9.44 Or (Eq (eats (skS.0 1 a) (skS.0 7 a_1)) True) % 9.20/9.44 (Or (Eq False True) % 9.20/9.44 (Or (Eq (much_smaller (skS.0 3 a_2) (skS.0 1 a)) False) % 9.20/9.44 (Or (Eq (plant a_3) False) (Eq (eats (skS.0 3 a_2) a_3) False)))) % 9.20/9.44 Clause #421 (by clausification #[420]): ∀ (a a_1 a_2 a_3 : Iota), % 9.20/9.44 Or (Eq (eats (skS.0 1 a) (skS.0 7 a_1)) True) % 9.20/9.44 (Or (Eq (much_smaller (skS.0 3 a_2) (skS.0 1 a)) False) % 9.20/9.44 (Or (Eq (plant a_3) False) (Eq (eats (skS.0 3 a_2) a_3) False))) % 9.20/9.44 Clause #422 (by superposition #[421, 194]): ∀ (a a_1 a_2 a_3 : Iota), % 9.20/9.44 Or (Eq (eats (skS.0 1 a) (skS.0 7 a_1)) True) % 9.20/9.44 (Or (Eq (plant a_2) False) (Or (Eq (eats (skS.0 3 a_3) a_2) False) (Eq False True))) % 9.20/9.44 Clause #423 (by clausification #[422]): ∀ (a a_1 a_2 a_3 : Iota), % 9.20/9.44 Or (Eq (eats (skS.0 1 a) (skS.0 7 a_1)) True) (Or (Eq (plant a_2) False) (Eq (eats (skS.0 3 a_3) a_2) False)) % 9.20/9.44 Clause #424 (by superposition #[423, 60]): ∀ (a a_1 a_2 a_3 : Iota), % 9.20/9.44 Or (Eq (eats (skS.0 1 a) (skS.0 7 a_1)) True) (Or (Eq (eats (skS.0 3 a_2) (skS.0 5 a_3)) False) (Eq False True)) % 9.20/9.44 Clause #429 (by clausification #[424]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eats (skS.0 1 a) (skS.0 7 a_1)) True) (Eq (eats (skS.0 3 a_2) (skS.0 5 a_3)) False) % 9.20/9.44 Clause #438 (by clausification #[325]): ∀ (a a_1 a_2 a_3 : Iota), % 9.20/9.44 Or (Eq (eats (skS.0 3 a) (skS.0 5 a_1)) True) % 9.20/9.44 (Or (Eq (eats (skS.0 3 a) (skS.0 4 a_2)) True) % 9.20/9.44 (Or (Eq (much_smaller (skS.0 4 a_2) (skS.0 3 a)) False) % 9.20/9.44 (Or (Eq (plant a_3) False) (Eq (eats (skS.0 4 a_2) a_3) False)))) % 9.20/9.44 Clause #439 (by superposition #[438, 192]): ∀ (a a_1 a_2 a_3 : Iota), % 9.20/9.44 Or (Eq (eats (skS.0 3 a) (skS.0 5 a_1)) True) % 9.20/9.44 (Or (Eq (eats (skS.0 3 a) (skS.0 4 a_2)) True) % 9.20/9.44 (Or (Eq (plant a_3) False) (Or (Eq (eats (skS.0 4 a_2) a_3) False) (Eq False True)))) % 9.20/9.44 Clause #440 (by clausification #[439]): ∀ (a a_1 a_2 a_3 : Iota), % 9.20/9.44 Or (Eq (eats (skS.0 3 a) (skS.0 5 a_1)) True) % 9.20/9.44 (Or (Eq (eats (skS.0 3 a) (skS.0 4 a_2)) True) (Or (Eq (plant a_3) False) (Eq (eats (skS.0 4 a_2) a_3) False))) % 9.20/9.44 Clause #442 (by superposition #[440, 137]): ∀ (a a_1 a_2 a_3 : Iota), % 9.20/9.44 Or (Eq (eats (skS.0 3 a) (skS.0 5 a_1)) True) % 9.20/9.44 (Or (Eq (eats (skS.0 3 a) (skS.0 4 a_2)) True) (Or (Eq (eats (skS.0 4 a_2) (skS.0 7 a_3)) False) (Eq False True))) % 9.20/9.44 Clause #445 (by clausification #[442]): ∀ (a a_1 a_2 a_3 : Iota), % 9.29/9.47 Or (Eq (eats (skS.0 3 a) (skS.0 5 a_1)) True) % 9.29/9.47 (Or (Eq (eats (skS.0 3 a) (skS.0 4 a_2)) True) (Eq (eats (skS.0 4 a_2) (skS.0 7 a_3)) False)) % 9.29/9.47 Clause #486 (by clausification #[291]): ∀ (a a_1 a_2 a_3 : Iota), % 9.29/9.47 Or (Eq (eats (skS.0 4 a) (skS.0 7 a_1)) True) % 9.29/9.47 (Or (Eq (eats (skS.0 4 a) (skS.0 8 a_2)) True) % 9.29/9.47 (Or (Eq (much_smaller (skS.0 8 a_2) (skS.0 4 a)) False) % 9.29/9.47 (Or (Eq (plant a_3) False) (Eq (eats (skS.0 8 a_2) a_3) False)))) % 9.29/9.47 Clause #487 (by forward demodulation #[486, 203]): ∀ (a a_1 a_2 a_3 : Iota), % 9.29/9.47 Or (Eq (eats (skS.0 4 a) (skS.0 7 a_1)) True) % 9.29/9.47 (Or (Eq False True) % 9.29/9.47 (Or (Eq (much_smaller (skS.0 8 a_2) (skS.0 4 a)) False) % 9.29/9.47 (Or (Eq (plant a_3) False) (Eq (eats (skS.0 8 a_2) a_3) False)))) % 9.29/9.47 Clause #488 (by clausification #[487]): ∀ (a a_1 a_2 a_3 : Iota), % 9.29/9.47 Or (Eq (eats (skS.0 4 a) (skS.0 7 a_1)) True) % 9.29/9.47 (Or (Eq (much_smaller (skS.0 8 a_2) (skS.0 4 a)) False) % 9.29/9.47 (Or (Eq (plant a_3) False) (Eq (eats (skS.0 8 a_2) a_3) False))) % 9.29/9.47 Clause #489 (by superposition #[488, 201]): ∀ (a a_1 a_2 a_3 : Iota), % 9.29/9.47 Or (Eq (eats (skS.0 4 a) (skS.0 7 a_1)) True) % 9.29/9.47 (Or (Eq (plant a_2) False) (Or (Eq (eats (skS.0 8 a_3) a_2) False) (Eq False True))) % 9.29/9.47 Clause #490 (by clausification #[489]): ∀ (a a_1 a_2 a_3 : Iota), % 9.29/9.47 Or (Eq (eats (skS.0 4 a) (skS.0 7 a_1)) True) (Or (Eq (plant a_2) False) (Eq (eats (skS.0 8 a_3) a_2) False)) % 9.29/9.47 Clause #493 (by superposition #[490, 204]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 9.29/9.47 Or (Eq (eats (skS.0 4 a) (skS.0 7 a_1)) True) % 9.29/9.47 (Or (Eq (eats (skS.0 8 a_2) (skS.0 10 (skS.0 8 a_3) a_4)) False) (Eq False True)) % 9.29/9.47 Clause #499 (by clausification #[493]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 9.29/9.47 Or (Eq (eats (skS.0 4 a) (skS.0 7 a_1)) True) (Eq (eats (skS.0 8 a_2) (skS.0 10 (skS.0 8 a_3) a_4)) False) % 9.29/9.47 Clause #500 (by superposition #[499, 216]): ∀ (a a_1 : Iota), Or (Eq (eats (skS.0 4 a) (skS.0 7 a_1)) True) (Eq False True) % 9.29/9.47 Clause #501 (by clausification #[500]): ∀ (a a_1 : Iota), Eq (eats (skS.0 4 a) (skS.0 7 a_1)) True % 9.29/9.47 Clause #502 (by superposition #[501, 445]): ∀ (a a_1 a_2 : Iota), % 9.29/9.47 Or (Eq (eats (skS.0 3 a) (skS.0 5 a_1)) True) (Or (Eq (eats (skS.0 3 a) (skS.0 4 a_2)) True) (Eq True False)) % 9.29/9.47 Clause #505 (by clausification #[502]): ∀ (a a_1 a_2 : Iota), Or (Eq (eats (skS.0 3 a) (skS.0 5 a_1)) True) (Eq (eats (skS.0 3 a) (skS.0 4 a_2)) True) % 9.29/9.47 Clause #506 (by superposition #[505, 429]): ∀ (a a_1 a_2 a_3 : Iota), % 9.29/9.47 Or (Eq (eats (skS.0 3 a) (skS.0 4 a_1)) True) (Or (Eq (eats (skS.0 1 a_2) (skS.0 7 a_3)) True) (Eq True False)) % 9.29/9.47 Clause #514 (by clausification #[506]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eats (skS.0 3 a) (skS.0 4 a_1)) True) (Eq (eats (skS.0 1 a_2) (skS.0 7 a_3)) True) % 9.29/9.47 Clause #516 (by superposition #[514, 195]): ∀ (a a_1 : Iota), Or (Eq (eats (skS.0 3 a) (skS.0 4 a_1)) True) (Eq True False) % 9.29/9.47 Clause #518 (by clausification #[516]): ∀ (a a_1 : Iota), Eq (eats (skS.0 3 a) (skS.0 4 a_1)) True % 9.29/9.47 Clause #519 (by superposition #[518, 169]): ∀ (a a_1 a_2 : Iota), % 9.29/9.47 Or (Eq True False) % 9.29/9.47 (Or (Eq (eats (skS.0 4 a) a_1) False) % 9.29/9.47 (Or (Eq (grain a_1) False) (Or (Eq (animal (skS.0 3 a_2)) False) (Eq (animal (skS.0 4 a)) False)))) % 9.29/9.47 Clause #520 (by clausification #[519]): ∀ (a a_1 a_2 : Iota), % 9.29/9.47 Or (Eq (eats (skS.0 4 a) a_1) False) % 9.29/9.47 (Or (Eq (grain a_1) False) (Or (Eq (animal (skS.0 3 a_2)) False) (Eq (animal (skS.0 4 a)) False))) % 9.29/9.47 Clause #521 (by forward demodulation #[520, 159]): ∀ (a a_1 a_2 : Iota), % 9.29/9.47 Or (Eq (eats (skS.0 4 a) a_1) False) % 9.29/9.47 (Or (Eq (grain a_1) False) (Or (Eq (animal (skS.0 3 a_2)) False) (Eq True False))) % 9.29/9.47 Clause #522 (by clausification #[521]): ∀ (a a_1 a_2 : Iota), Or (Eq (eats (skS.0 4 a) a_1) False) (Or (Eq (grain a_1) False) (Eq (animal (skS.0 3 a_2)) False)) % 9.29/9.47 Clause #524 (by superposition #[522, 501]): ∀ (a a_1 : Iota), Or (Eq (grain (skS.0 7 a)) False) (Or (Eq (animal (skS.0 3 a_1)) False) (Eq False True)) % 9.29/9.47 Clause #525 (by clausification #[524]): ∀ (a a_1 : Iota), Or (Eq (grain (skS.0 7 a)) False) (Eq (animal (skS.0 3 a_1)) False) % 9.29/9.47 Clause #526 (by superposition #[525, 66]): ∀ (a : Iota), Or (Eq (animal (skS.0 3 a)) False) (Eq False True) % 9.29/9.48 Clause #528 (by clausification #[526]): ∀ (a : Iota), Eq (animal (skS.0 3 a)) False % 9.29/9.48 Clause #529 (by superposition #[528, 155]): Eq False True % 9.29/9.48 Clause #530 (by clausification #[529]): False % 9.29/9.48 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------