%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : PUZ031+1 : TPTP v9.2.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n012.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 6.55s 6.73s % Output : Proof 6.72s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.13/0.13 % Problem : PUZ031+1 : TPTP v9.2.0. Released v2.0.0. % 0.13/0.14 % Command : duper %s % 0.14/0.35 % Computer : n012.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 20:52:08 EDT 2025 % 0.14/0.36 % CPUTime : % 6.55/6.73 SZS status Theorem for theBenchmark.p % 6.55/6.73 SZS output start Proof for theBenchmark.p % 6.55/6.73 Clause #0 (by assumption #[]): Eq (∀ (X : Iota), wolf X → animal X) True % 6.55/6.73 Clause #1 (by assumption #[]): Eq (Exists fun X1 => wolf X1) True % 6.55/6.73 Clause #2 (by assumption #[]): Eq (∀ (X : Iota), fox X → animal X) True % 6.55/6.73 Clause #3 (by assumption #[]): Eq (Exists fun X1 => fox X1) True % 6.55/6.73 Clause #4 (by assumption #[]): Eq (∀ (X : Iota), bird X → animal X) True % 6.55/6.73 Clause #5 (by assumption #[]): Eq (Exists fun X1 => bird X1) True % 6.55/6.73 Clause #8 (by assumption #[]): Eq (∀ (X : Iota), snail X → animal X) True % 6.55/6.73 Clause #9 (by assumption #[]): Eq (Exists fun X1 => snail X1) True % 6.55/6.73 Clause #10 (by assumption #[]): Eq (Exists fun X => grain X) True % 6.55/6.73 Clause #11 (by assumption #[]): Eq (∀ (X1 : Iota), grain X1 → plant X1) True % 6.55/6.73 Clause #12 (by assumption #[]): Eq % 6.55/6.73 (∀ (X : Iota), % 6.55/6.73 animal X → % 6.55/6.73 Or (∀ (Y : Iota), plant Y → eats X Y) % 6.55/6.73 (∀ (Y1 : Iota), % 6.55/6.73 And (And (animal Y1) (much_smaller Y1 X)) (Exists fun Z => And (plant Z) (eats Y1 Z)) → eats X Y1)) % 6.55/6.73 True % 6.55/6.73 Clause #13 (by assumption #[]): Eq (∀ (X Y : Iota), And (bird Y) (Or (snail X) (caterpillar X)) → much_smaller X Y) True % 6.55/6.73 Clause #14 (by assumption #[]): Eq (∀ (X Y : Iota), And (bird X) (fox Y) → much_smaller X Y) True % 6.55/6.73 Clause #15 (by assumption #[]): Eq (∀ (X Y : Iota), And (fox X) (wolf Y) → much_smaller X Y) True % 6.55/6.73 Clause #16 (by assumption #[]): Eq (∀ (X Y : Iota), And (wolf X) (Or (fox Y) (grain Y)) → Not (eats X Y)) True % 6.55/6.73 Clause #18 (by assumption #[]): Eq (∀ (X Y : Iota), And (bird X) (snail Y) → Not (eats X Y)) True % 6.55/6.73 Clause #19 (by assumption #[]): Eq (∀ (X : Iota), Or (caterpillar X) (snail X) → Exists fun Y => And (plant Y) (eats X Y)) True % 6.55/6.73 Clause #20 (by assumption #[]): Eq % 6.55/6.73 (Not % 6.55/6.73 (Exists fun X => % 6.55/6.73 Exists fun Y => And (And (animal X) (animal Y)) (Exists fun Z => And (And (grain Z) (eats Y Z)) (eats X Y)))) % 6.55/6.73 True % 6.55/6.73 Clause #21 (by clausification #[11]): ∀ (a : Iota), Eq (grain a → plant a) True % 6.55/6.73 Clause #22 (by clausification #[21]): ∀ (a : Iota), Or (Eq (grain a) False) (Eq (plant a) True) % 6.55/6.73 Clause #23 (by clausification #[8]): ∀ (a : Iota), Eq (snail a → animal a) True % 6.55/6.73 Clause #24 (by clausification #[23]): ∀ (a : Iota), Or (Eq (snail a) False) (Eq (animal a) True) % 6.55/6.73 Clause #27 (by clausification #[2]): ∀ (a : Iota), Eq (fox a → animal a) True % 6.55/6.73 Clause #28 (by clausification #[27]): ∀ (a : Iota), Or (Eq (fox a) False) (Eq (animal a) True) % 6.55/6.73 Clause #29 (by clausification #[4]): ∀ (a : Iota), Eq (bird a → animal a) True % 6.55/6.73 Clause #30 (by clausification #[29]): ∀ (a : Iota), Or (Eq (bird a) False) (Eq (animal a) True) % 6.55/6.73 Clause #31 (by clausification #[0]): ∀ (a : Iota), Eq (wolf a → animal a) True % 6.55/6.73 Clause #32 (by clausification #[31]): ∀ (a : Iota), Or (Eq (wolf a) False) (Eq (animal a) True) % 6.55/6.73 Clause #33 (by betaEtaReduce #[1]): Eq (Exists wolf) True % 6.55/6.73 Clause #34 (by clausification #[33]): ∀ (a : Iota), Eq (wolf (skS.0 0 a)) True % 6.55/6.73 Clause #35 (by superposition #[34, 32]): ∀ (a : Iota), Or (Eq True False) (Eq (animal (skS.0 0 a)) True) % 6.55/6.73 Clause #39 (by betaEtaReduce #[9]): Eq (Exists snail) True % 6.55/6.73 Clause #40 (by clausification #[39]): ∀ (a : Iota), Eq (snail (skS.0 2 a)) True % 6.55/6.73 Clause #41 (by superposition #[40, 24]): ∀ (a : Iota), Or (Eq True False) (Eq (animal (skS.0 2 a)) True) % 6.55/6.73 Clause #42 (by betaEtaReduce #[10]): Eq (Exists grain) True % 6.55/6.73 Clause #43 (by clausification #[42]): ∀ (a : Iota), Eq (grain (skS.0 3 a)) True % 6.55/6.73 Clause #44 (by superposition #[43, 22]): ∀ (a : Iota), Or (Eq True False) (Eq (plant (skS.0 3 a)) True) % 6.55/6.73 Clause #45 (by betaEtaReduce #[5]): Eq (Exists bird) True % 6.55/6.73 Clause #46 (by clausification #[45]): ∀ (a : Iota), Eq (bird (skS.0 4 a)) True % 6.55/6.73 Clause #47 (by superposition #[46, 30]): ∀ (a : Iota), Or (Eq True False) (Eq (animal (skS.0 4 a)) True) % 6.55/6.73 Clause #48 (by betaEtaReduce #[3]): Eq (Exists fox) True % 6.55/6.73 Clause #49 (by clausification #[48]): ∀ (a : Iota), Eq (fox (skS.0 5 a)) True % 6.55/6.73 Clause #50 (by superposition #[49, 28]): ∀ (a : Iota), Or (Eq True False) (Eq (animal (skS.0 5 a)) True) % 6.55/6.73 Clause #51 (by clausification #[15]): ∀ (a : Iota), Eq (∀ (Y : Iota), And (fox a) (wolf Y) → much_smaller a Y) True % 6.58/6.75 Clause #52 (by clausification #[51]): ∀ (a a_1 : Iota), Eq (And (fox a) (wolf a_1) → much_smaller a a_1) True % 6.58/6.75 Clause #53 (by clausification #[52]): ∀ (a a_1 : Iota), Or (Eq (And (fox a) (wolf a_1)) False) (Eq (much_smaller a a_1) True) % 6.58/6.75 Clause #54 (by clausification #[53]): ∀ (a a_1 : Iota), Or (Eq (much_smaller a a_1) True) (Or (Eq (fox a) False) (Eq (wolf a_1) False)) % 6.58/6.75 Clause #55 (by superposition #[54, 49]): ∀ (a a_1 : Iota), Or (Eq (much_smaller (skS.0 5 a) a_1) True) (Or (Eq (wolf a_1) False) (Eq False True)) % 6.58/6.75 Clause #56 (by clausification #[14]): ∀ (a : Iota), Eq (∀ (Y : Iota), And (bird a) (fox Y) → much_smaller a Y) True % 6.58/6.75 Clause #57 (by clausification #[56]): ∀ (a a_1 : Iota), Eq (And (bird a) (fox a_1) → much_smaller a a_1) True % 6.58/6.75 Clause #58 (by clausification #[57]): ∀ (a a_1 : Iota), Or (Eq (And (bird a) (fox a_1)) False) (Eq (much_smaller a a_1) True) % 6.58/6.75 Clause #59 (by clausification #[58]): ∀ (a a_1 : Iota), Or (Eq (much_smaller a a_1) True) (Or (Eq (bird a) False) (Eq (fox a_1) False)) % 6.58/6.75 Clause #60 (by superposition #[59, 46]): ∀ (a a_1 : Iota), Or (Eq (much_smaller (skS.0 4 a) a_1) True) (Or (Eq (fox a_1) False) (Eq False True)) % 6.58/6.75 Clause #61 (by clausification #[13]): ∀ (a : Iota), Eq (∀ (Y : Iota), And (bird Y) (Or (snail a) (caterpillar a)) → much_smaller a Y) True % 6.58/6.75 Clause #62 (by clausification #[61]): ∀ (a a_1 : Iota), Eq (And (bird a) (Or (snail a_1) (caterpillar a_1)) → much_smaller a_1 a) True % 6.58/6.75 Clause #63 (by clausification #[62]): ∀ (a a_1 : Iota), Or (Eq (And (bird a) (Or (snail a_1) (caterpillar a_1))) False) (Eq (much_smaller a_1 a) True) % 6.58/6.75 Clause #64 (by clausification #[63]): ∀ (a a_1 : Iota), Or (Eq (much_smaller a a_1) True) (Or (Eq (bird a_1) False) (Eq (Or (snail a) (caterpillar a)) False)) % 6.58/6.75 Clause #66 (by clausification #[64]): ∀ (a a_1 : Iota), Or (Eq (much_smaller a a_1) True) (Or (Eq (bird a_1) False) (Eq (snail a) False)) % 6.58/6.75 Clause #73 (by clausification #[18]): ∀ (a : Iota), Eq (∀ (Y : Iota), And (bird a) (snail Y) → Not (eats a Y)) True % 6.58/6.75 Clause #74 (by clausification #[73]): ∀ (a a_1 : Iota), Eq (And (bird a) (snail a_1) → Not (eats a a_1)) True % 6.58/6.75 Clause #75 (by clausification #[74]): ∀ (a a_1 : Iota), Or (Eq (And (bird a) (snail a_1)) False) (Eq (Not (eats a a_1)) True) % 6.58/6.75 Clause #76 (by clausification #[75]): ∀ (a a_1 : Iota), Or (Eq (Not (eats a a_1)) True) (Or (Eq (bird a) False) (Eq (snail a_1) False)) % 6.58/6.75 Clause #77 (by clausification #[76]): ∀ (a a_1 : Iota), Or (Eq (bird a) False) (Or (Eq (snail a_1) False) (Eq (eats a a_1) False)) % 6.58/6.75 Clause #78 (by superposition #[77, 46]): ∀ (a a_1 : Iota), Or (Eq (snail a) False) (Or (Eq (eats (skS.0 4 a_1) a) False) (Eq False True)) % 6.58/6.75 Clause #79 (by clausification #[12]): ∀ (a : Iota), % 6.58/6.75 Eq % 6.58/6.75 (animal a → % 6.58/6.75 Or (∀ (Y : Iota), plant Y → eats a Y) % 6.58/6.75 (∀ (Y1 : Iota), % 6.58/6.75 And (And (animal Y1) (much_smaller Y1 a)) (Exists fun Z => And (plant Z) (eats Y1 Z)) → eats a Y1)) % 6.58/6.75 True % 6.58/6.75 Clause #80 (by clausification #[79]): ∀ (a : Iota), % 6.58/6.75 Or (Eq (animal a) False) % 6.58/6.75 (Eq % 6.58/6.75 (Or (∀ (Y : Iota), plant Y → eats a Y) % 6.58/6.75 (∀ (Y1 : Iota), % 6.58/6.75 And (And (animal Y1) (much_smaller Y1 a)) (Exists fun Z => And (plant Z) (eats Y1 Z)) → eats a Y1)) % 6.58/6.75 True) % 6.58/6.75 Clause #81 (by clausification #[80]): ∀ (a : Iota), % 6.58/6.75 Or (Eq (animal a) False) % 6.58/6.75 (Or (Eq (∀ (Y : Iota), plant Y → eats a Y) True) % 6.58/6.75 (Eq % 6.58/6.75 (∀ (Y1 : Iota), % 6.58/6.75 And (And (animal Y1) (much_smaller Y1 a)) (Exists fun Z => And (plant Z) (eats Y1 Z)) → eats a Y1) % 6.58/6.75 True)) % 6.58/6.75 Clause #82 (by clausification #[81]): ∀ (a a_1 : Iota), % 6.58/6.75 Or (Eq (animal a) False) % 6.58/6.75 (Or % 6.58/6.75 (Eq % 6.58/6.75 (∀ (Y1 : Iota), % 6.58/6.75 And (And (animal Y1) (much_smaller Y1 a)) (Exists fun Z => And (plant Z) (eats Y1 Z)) → eats a Y1) % 6.58/6.75 True) % 6.58/6.75 (Eq (plant a_1 → eats a a_1) True)) % 6.58/6.75 Clause #83 (by clausification #[82]): ∀ (a a_1 a_2 : Iota), % 6.58/6.75 Or (Eq (animal a) False) % 6.58/6.75 (Or (Eq (plant a_1 → eats a a_1) True) % 6.58/6.75 (Eq (And (And (animal a_2) (much_smaller a_2 a)) (Exists fun Z => And (plant Z) (eats a_2 Z)) → eats a a_2) True)) % 6.58/6.78 Clause #84 (by clausification #[83]): ∀ (a a_1 a_2 : Iota), % 6.58/6.78 Or (Eq (animal a) False) % 6.58/6.78 (Or % 6.58/6.78 (Eq (And (And (animal a_1) (much_smaller a_1 a)) (Exists fun Z => And (plant Z) (eats a_1 Z)) → eats a a_1) True) % 6.58/6.78 (Or (Eq (plant a_2) False) (Eq (eats a a_2) True))) % 6.58/6.78 Clause #85 (by clausification #[84]): ∀ (a a_1 a_2 : Iota), % 6.58/6.78 Or (Eq (animal a) False) % 6.58/6.78 (Or (Eq (plant a_1) False) % 6.58/6.78 (Or (Eq (eats a a_1) True) % 6.58/6.78 (Or (Eq (And (And (animal a_2) (much_smaller a_2 a)) (Exists fun Z => And (plant Z) (eats a_2 Z))) False) % 6.58/6.78 (Eq (eats a a_2) True)))) % 6.58/6.78 Clause #86 (by clausification #[85]): ∀ (a a_1 a_2 : Iota), % 6.58/6.78 Or (Eq (animal a) False) % 6.58/6.78 (Or (Eq (plant a_1) False) % 6.58/6.78 (Or (Eq (eats a a_1) True) % 6.58/6.78 (Or (Eq (eats a a_2) True) % 6.58/6.78 (Or (Eq (And (animal a_2) (much_smaller a_2 a)) False) % 6.58/6.78 (Eq (Exists fun Z => And (plant Z) (eats a_2 Z)) False))))) % 6.58/6.78 Clause #87 (by clausification #[86]): ∀ (a a_1 a_2 : Iota), % 6.58/6.78 Or (Eq (animal a) False) % 6.58/6.78 (Or (Eq (plant a_1) False) % 6.58/6.78 (Or (Eq (eats a a_1) True) % 6.58/6.78 (Or (Eq (eats a a_2) True) % 6.58/6.78 (Or (Eq (Exists fun Z => And (plant Z) (eats a_2 Z)) False) % 6.58/6.78 (Or (Eq (animal a_2) False) (Eq (much_smaller a_2 a) False)))))) % 6.58/6.78 Clause #88 (by clausification #[87]): ∀ (a a_1 a_2 a_3 : Iota), % 6.58/6.78 Or (Eq (animal a) False) % 6.58/6.78 (Or (Eq (plant a_1) False) % 6.58/6.78 (Or (Eq (eats a a_1) True) % 6.58/6.78 (Or (Eq (eats a a_2) True) % 6.58/6.78 (Or (Eq (animal a_2) False) % 6.58/6.78 (Or (Eq (much_smaller a_2 a) False) (Eq (And (plant a_3) (eats a_2 a_3)) False)))))) % 6.58/6.78 Clause #89 (by clausification #[88]): ∀ (a a_1 a_2 a_3 : Iota), % 6.58/6.78 Or (Eq (animal a) False) % 6.58/6.78 (Or (Eq (plant a_1) False) % 6.58/6.78 (Or (Eq (eats a a_1) True) % 6.58/6.78 (Or (Eq (eats a a_2) True) % 6.58/6.78 (Or (Eq (animal a_2) False) % 6.58/6.78 (Or (Eq (much_smaller a_2 a) False) (Or (Eq (plant a_3) False) (Eq (eats a_2 a_3) False))))))) % 6.58/6.78 Clause #90 (by clausification #[16]): ∀ (a : Iota), Eq (∀ (Y : Iota), And (wolf a) (Or (fox Y) (grain Y)) → Not (eats a Y)) True % 6.58/6.78 Clause #91 (by clausification #[90]): ∀ (a a_1 : Iota), Eq (And (wolf a) (Or (fox a_1) (grain a_1)) → Not (eats a a_1)) True % 6.58/6.78 Clause #92 (by clausification #[91]): ∀ (a a_1 : Iota), Or (Eq (And (wolf a) (Or (fox a_1) (grain a_1))) False) (Eq (Not (eats a a_1)) True) % 6.58/6.78 Clause #93 (by clausification #[92]): ∀ (a a_1 : Iota), Or (Eq (Not (eats a a_1)) True) (Or (Eq (wolf a) False) (Eq (Or (fox a_1) (grain a_1)) False)) % 6.58/6.78 Clause #94 (by clausification #[93]): ∀ (a a_1 : Iota), Or (Eq (wolf a) False) (Or (Eq (Or (fox a_1) (grain a_1)) False) (Eq (eats a a_1) False)) % 6.58/6.78 Clause #95 (by clausification #[94]): ∀ (a a_1 : Iota), Or (Eq (wolf a) False) (Or (Eq (eats a a_1) False) (Eq (grain a_1) False)) % 6.58/6.78 Clause #96 (by clausification #[94]): ∀ (a a_1 : Iota), Or (Eq (wolf a) False) (Or (Eq (eats a a_1) False) (Eq (fox a_1) False)) % 6.58/6.78 Clause #97 (by superposition #[95, 34]): ∀ (a a_1 : Iota), Or (Eq (eats (skS.0 0 a) a_1) False) (Or (Eq (grain a_1) False) (Eq False True)) % 6.58/6.78 Clause #98 (by clausification #[50]): ∀ (a : Iota), Eq (animal (skS.0 5 a)) True % 6.58/6.78 Clause #99 (by superposition #[98, 89]): ∀ (a a_1 a_2 a_3 : Iota), % 6.58/6.78 Or (Eq True False) % 6.58/6.78 (Or (Eq (plant a) False) % 6.58/6.78 (Or (Eq (eats (skS.0 5 a_1) a) True) % 6.58/6.78 (Or (Eq (eats (skS.0 5 a_1) a_2) True) % 6.58/6.78 (Or (Eq (animal a_2) False) % 6.58/6.78 (Or (Eq (much_smaller a_2 (skS.0 5 a_1)) False) (Or (Eq (plant a_3) False) (Eq (eats a_2 a_3) False))))))) % 6.58/6.78 Clause #100 (by superposition #[66, 46]): ∀ (a a_1 : Iota), Or (Eq (much_smaller a (skS.0 4 a_1)) True) (Or (Eq (snail a) False) (Eq False True)) % 6.58/6.78 Clause #101 (by clausification #[44]): ∀ (a : Iota), Eq (plant (skS.0 3 a)) True % 6.58/6.78 Clause #102 (by superposition #[96, 34]): ∀ (a a_1 : Iota), Or (Eq (eats (skS.0 0 a) a_1) False) (Or (Eq (fox a_1) False) (Eq False True)) % 6.58/6.78 Clause #103 (by clausification #[19]): ∀ (a : Iota), Eq (Or (caterpillar a) (snail a) → Exists fun Y => And (plant Y) (eats a Y)) True % 6.58/6.78 Clause #104 (by clausification #[103]): ∀ (a : Iota), Or (Eq (Or (caterpillar a) (snail a)) False) (Eq (Exists fun Y => And (plant Y) (eats a Y)) True) % 6.58/6.80 Clause #105 (by clausification #[104]): ∀ (a : Iota), Or (Eq (Exists fun Y => And (plant Y) (eats a Y)) True) (Eq (snail a) False) % 6.58/6.80 Clause #107 (by clausification #[105]): ∀ (a a_1 : Iota), Or (Eq (snail a) False) (Eq (And (plant (skS.0 6 a a_1)) (eats a (skS.0 6 a a_1))) True) % 6.58/6.80 Clause #108 (by clausification #[107]): ∀ (a a_1 : Iota), Or (Eq (snail a) False) (Eq (eats a (skS.0 6 a a_1)) True) % 6.58/6.80 Clause #109 (by clausification #[107]): ∀ (a a_1 : Iota), Or (Eq (snail a) False) (Eq (plant (skS.0 6 a a_1)) True) % 6.58/6.80 Clause #110 (by superposition #[108, 40]): ∀ (a a_1 : Iota), Or (Eq (eats (skS.0 2 a) (skS.0 6 (skS.0 2 a) a_1)) True) (Eq False True) % 6.58/6.80 Clause #111 (by clausification #[47]): ∀ (a : Iota), Eq (animal (skS.0 4 a)) True % 6.58/6.80 Clause #112 (by superposition #[111, 89]): ∀ (a a_1 a_2 a_3 : Iota), % 6.58/6.80 Or (Eq True False) % 6.58/6.80 (Or (Eq (plant a) False) % 6.58/6.80 (Or (Eq (eats (skS.0 4 a_1) a) True) % 6.58/6.80 (Or (Eq (eats (skS.0 4 a_1) a_2) True) % 6.58/6.80 (Or (Eq (animal a_2) False) % 6.58/6.80 (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))))))) % 6.58/6.80 Clause #115 (by clausification #[35]): ∀ (a : Iota), Eq (animal (skS.0 0 a)) True % 6.58/6.80 Clause #116 (by superposition #[115, 89]): ∀ (a a_1 a_2 a_3 : Iota), % 6.58/6.80 Or (Eq True False) % 6.58/6.80 (Or (Eq (plant a) False) % 6.58/6.80 (Or (Eq (eats (skS.0 0 a_1) a) True) % 6.58/6.80 (Or (Eq (eats (skS.0 0 a_1) a_2) True) % 6.58/6.80 (Or (Eq (animal a_2) False) % 6.58/6.80 (Or (Eq (much_smaller a_2 (skS.0 0 a_1)) False) (Or (Eq (plant a_3) False) (Eq (eats a_2 a_3) False))))))) % 6.58/6.80 Clause #117 (by clausification #[41]): ∀ (a : Iota), Eq (animal (skS.0 2 a)) True % 6.58/6.80 Clause #119 (by superposition #[109, 40]): ∀ (a a_1 : Iota), Or (Eq (plant (skS.0 6 (skS.0 2 a) a_1)) True) (Eq False True) % 6.58/6.80 Clause #120 (by clausification #[20]): Eq % 6.58/6.80 (Exists fun X => % 6.58/6.80 Exists fun Y => And (And (animal X) (animal Y)) (Exists fun Z => And (And (grain Z) (eats Y Z)) (eats X Y))) % 6.58/6.80 False % 6.58/6.80 Clause #121 (by clausification #[120]): ∀ (a : Iota), % 6.58/6.80 Eq (Exists fun Y => And (And (animal a) (animal Y)) (Exists fun Z => And (And (grain Z) (eats Y Z)) (eats a Y))) False % 6.58/6.80 Clause #122 (by clausification #[121]): ∀ (a a_1 : Iota), % 6.58/6.80 Eq (And (And (animal a) (animal a_1)) (Exists fun Z => And (And (grain Z) (eats a_1 Z)) (eats a a_1))) False % 6.58/6.80 Clause #123 (by clausification #[122]): ∀ (a a_1 : Iota), % 6.58/6.80 Or (Eq (And (animal a) (animal a_1)) False) (Eq (Exists fun Z => And (And (grain Z) (eats a_1 Z)) (eats a a_1)) False) % 6.58/6.80 Clause #124 (by clausification #[123]): ∀ (a a_1 : Iota), % 6.58/6.80 Or (Eq (Exists fun Z => And (And (grain Z) (eats a Z)) (eats a_1 a)) False) % 6.58/6.80 (Or (Eq (animal a_1) False) (Eq (animal a) False)) % 6.58/6.80 Clause #125 (by clausification #[124]): ∀ (a a_1 a_2 : Iota), % 6.58/6.80 Or (Eq (animal a) False) (Or (Eq (animal a_1) False) (Eq (And (And (grain a_2) (eats a_1 a_2)) (eats a a_1)) False)) % 6.58/6.80 Clause #126 (by clausification #[125]): ∀ (a a_1 a_2 : Iota), % 6.58/6.80 Or (Eq (animal a) False) % 6.58/6.80 (Or (Eq (animal a_1) False) (Or (Eq (And (grain a_2) (eats a_1 a_2)) False) (Eq (eats a a_1) False))) % 6.58/6.80 Clause #127 (by clausification #[126]): ∀ (a a_1 a_2 : Iota), % 6.58/6.80 Or (Eq (animal a) False) % 6.58/6.80 (Or (Eq (animal a_1) False) (Or (Eq (eats a a_1) False) (Or (Eq (grain a_2) False) (Eq (eats a_1 a_2) False)))) % 6.58/6.80 Clause #128 (by superposition #[127, 98]): ∀ (a a_1 a_2 : Iota), % 6.58/6.80 Or (Eq (animal a) False) % 6.58/6.80 (Or (Eq (eats (skS.0 5 a_1) a) False) (Or (Eq (grain a_2) False) (Or (Eq (eats a a_2) False) (Eq False True)))) % 6.58/6.80 Clause #140 (by clausification #[100]): ∀ (a a_1 : Iota), Or (Eq (much_smaller a (skS.0 4 a_1)) True) (Eq (snail a) False) % 6.58/6.80 Clause #141 (by superposition #[140, 40]): ∀ (a a_1 : Iota), Or (Eq (much_smaller (skS.0 2 a) (skS.0 4 a_1)) True) (Eq False True) % 6.58/6.80 Clause #142 (by clausification #[55]): ∀ (a a_1 : Iota), Or (Eq (much_smaller (skS.0 5 a) a_1) True) (Eq (wolf a_1) False) % 6.58/6.80 Clause #143 (by superposition #[142, 34]): ∀ (a a_1 : Iota), Or (Eq (much_smaller (skS.0 5 a) (skS.0 0 a_1)) True) (Eq False True) % 6.67/6.83 Clause #144 (by clausification #[60]): ∀ (a a_1 : Iota), Or (Eq (much_smaller (skS.0 4 a) a_1) True) (Eq (fox a_1) False) % 6.67/6.83 Clause #145 (by superposition #[144, 49]): ∀ (a a_1 : Iota), Or (Eq (much_smaller (skS.0 4 a) (skS.0 5 a_1)) True) (Eq False True) % 6.67/6.83 Clause #146 (by clausification #[102]): ∀ (a a_1 : Iota), Or (Eq (eats (skS.0 0 a) a_1) False) (Eq (fox a_1) False) % 6.67/6.83 Clause #149 (by clausification #[97]): ∀ (a a_1 : Iota), Or (Eq (eats (skS.0 0 a) a_1) False) (Eq (grain a_1) False) % 6.67/6.83 Clause #150 (by clausification #[78]): ∀ (a a_1 : Iota), Or (Eq (snail a) False) (Eq (eats (skS.0 4 a_1) a) False) % 6.67/6.83 Clause #151 (by superposition #[150, 40]): ∀ (a a_1 : Iota), Or (Eq (eats (skS.0 4 a) (skS.0 2 a_1)) False) (Eq False True) % 6.67/6.83 Clause #152 (by clausification #[151]): ∀ (a a_1 : Iota), Eq (eats (skS.0 4 a) (skS.0 2 a_1)) False % 6.67/6.83 Clause #153 (by clausification #[99]): ∀ (a a_1 a_2 a_3 : Iota), % 6.67/6.83 Or (Eq (plant a) False) % 6.67/6.83 (Or (Eq (eats (skS.0 5 a_1) a) True) % 6.67/6.83 (Or (Eq (eats (skS.0 5 a_1) a_2) True) % 6.67/6.83 (Or (Eq (animal a_2) False) % 6.67/6.83 (Or (Eq (much_smaller a_2 (skS.0 5 a_1)) False) (Or (Eq (plant a_3) False) (Eq (eats a_2 a_3) False)))))) % 6.67/6.83 Clause #154 (by superposition #[153, 101]): ∀ (a a_1 a_2 a_3 : Iota), % 6.67/6.83 Or (Eq (eats (skS.0 5 a) (skS.0 3 a_1)) True) % 6.67/6.83 (Or (Eq (eats (skS.0 5 a) a_2) True) % 6.67/6.83 (Or (Eq (animal a_2) False) % 6.67/6.83 (Or (Eq (much_smaller a_2 (skS.0 5 a)) False) % 6.67/6.83 (Or (Eq (plant a_3) False) (Or (Eq (eats a_2 a_3) False) (Eq False True)))))) % 6.67/6.83 Clause #156 (by clausification #[141]): ∀ (a a_1 : Iota), Eq (much_smaller (skS.0 2 a) (skS.0 4 a_1)) True % 6.67/6.83 Clause #158 (by clausification #[143]): ∀ (a a_1 : Iota), Eq (much_smaller (skS.0 5 a) (skS.0 0 a_1)) True % 6.67/6.83 Clause #159 (by clausification #[145]): ∀ (a a_1 : Iota), Eq (much_smaller (skS.0 4 a) (skS.0 5 a_1)) True % 6.67/6.83 Clause #160 (by clausification #[110]): ∀ (a a_1 : Iota), Eq (eats (skS.0 2 a) (skS.0 6 (skS.0 2 a) a_1)) True % 6.67/6.83 Clause #161 (by clausification #[119]): ∀ (a a_1 : Iota), Eq (plant (skS.0 6 (skS.0 2 a) a_1)) True % 6.67/6.83 Clause #183 (by clausification #[112]): ∀ (a a_1 a_2 a_3 : Iota), % 6.67/6.83 Or (Eq (plant a) False) % 6.67/6.83 (Or (Eq (eats (skS.0 4 a_1) a) True) % 6.67/6.83 (Or (Eq (eats (skS.0 4 a_1) a_2) True) % 6.67/6.83 (Or (Eq (animal a_2) False) % 6.67/6.83 (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)))))) % 6.67/6.83 Clause #184 (by superposition #[183, 101]): ∀ (a a_1 a_2 a_3 : Iota), % 6.67/6.83 Or (Eq (eats (skS.0 4 a) (skS.0 3 a_1)) True) % 6.67/6.83 (Or (Eq (eats (skS.0 4 a) a_2) True) % 6.67/6.83 (Or (Eq (animal a_2) False) % 6.67/6.83 (Or (Eq (much_smaller a_2 (skS.0 4 a)) False) % 6.67/6.83 (Or (Eq (plant a_3) False) (Or (Eq (eats a_2 a_3) False) (Eq False True)))))) % 6.67/6.83 Clause #193 (by clausification #[128]): ∀ (a a_1 a_2 : Iota), % 6.67/6.83 Or (Eq (animal a) False) (Or (Eq (eats (skS.0 5 a_1) a) False) (Or (Eq (grain a_2) False) (Eq (eats a a_2) False))) % 6.67/6.83 Clause #195 (by superposition #[193, 111]): ∀ (a a_1 a_2 : Iota), % 6.67/6.83 Or (Eq (eats (skS.0 5 a) (skS.0 4 a_1)) False) % 6.67/6.83 (Or (Eq (grain a_2) False) (Or (Eq (eats (skS.0 4 a_1) a_2) False) (Eq False True))) % 6.67/6.83 Clause #208 (by clausification #[195]): ∀ (a a_1 a_2 : Iota), % 6.67/6.83 Or (Eq (eats (skS.0 5 a) (skS.0 4 a_1)) False) (Or (Eq (grain a_2) False) (Eq (eats (skS.0 4 a_1) a_2) False)) % 6.67/6.83 Clause #211 (by clausification #[116]): ∀ (a a_1 a_2 a_3 : Iota), % 6.67/6.83 Or (Eq (plant a) False) % 6.67/6.83 (Or (Eq (eats (skS.0 0 a_1) a) True) % 6.67/6.83 (Or (Eq (eats (skS.0 0 a_1) a_2) True) % 6.67/6.83 (Or (Eq (animal a_2) False) % 6.67/6.83 (Or (Eq (much_smaller a_2 (skS.0 0 a_1)) False) (Or (Eq (plant a_3) False) (Eq (eats a_2 a_3) False)))))) % 6.67/6.83 Clause #212 (by superposition #[211, 101]): ∀ (a a_1 a_2 a_3 : Iota), % 6.67/6.83 Or (Eq (eats (skS.0 0 a) (skS.0 3 a_1)) True) % 6.67/6.83 (Or (Eq (eats (skS.0 0 a) a_2) True) % 6.67/6.83 (Or (Eq (animal a_2) False) % 6.67/6.83 (Or (Eq (much_smaller a_2 (skS.0 0 a)) False) % 6.67/6.83 (Or (Eq (plant a_3) False) (Or (Eq (eats a_2 a_3) False) (Eq False True)))))) % 6.67/6.83 Clause #230 (by clausification #[154]): ∀ (a a_1 a_2 a_3 : Iota), % 6.67/6.83 Or (Eq (eats (skS.0 5 a) (skS.0 3 a_1)) True) % 6.67/6.83 (Or (Eq (eats (skS.0 5 a) a_2) True) % 6.67/6.86 (Or (Eq (animal a_2) False) % 6.67/6.86 (Or (Eq (much_smaller a_2 (skS.0 5 a)) False) (Or (Eq (plant a_3) False) (Eq (eats a_2 a_3) False))))) % 6.67/6.86 Clause #232 (by superposition #[230, 111]): ∀ (a a_1 a_2 a_3 : Iota), % 6.67/6.86 Or (Eq (eats (skS.0 5 a) (skS.0 3 a_1)) True) % 6.67/6.86 (Or (Eq (eats (skS.0 5 a) (skS.0 4 a_2)) True) % 6.67/6.86 (Or (Eq (much_smaller (skS.0 4 a_2) (skS.0 5 a)) False) % 6.67/6.86 (Or (Eq (plant a_3) False) (Or (Eq (eats (skS.0 4 a_2) a_3) False) (Eq False True))))) % 6.67/6.86 Clause #272 (by clausification #[184]): ∀ (a a_1 a_2 a_3 : Iota), % 6.67/6.86 Or (Eq (eats (skS.0 4 a) (skS.0 3 a_1)) True) % 6.67/6.86 (Or (Eq (eats (skS.0 4 a) a_2) True) % 6.67/6.86 (Or (Eq (animal a_2) False) % 6.67/6.86 (Or (Eq (much_smaller a_2 (skS.0 4 a)) False) (Or (Eq (plant a_3) False) (Eq (eats a_2 a_3) False))))) % 6.67/6.86 Clause #277 (by superposition #[272, 117]): ∀ (a a_1 a_2 a_3 : Iota), % 6.67/6.86 Or (Eq (eats (skS.0 4 a) (skS.0 3 a_1)) True) % 6.67/6.86 (Or (Eq (eats (skS.0 4 a) (skS.0 2 a_2)) True) % 6.67/6.86 (Or (Eq (much_smaller (skS.0 2 a_2) (skS.0 4 a)) False) % 6.67/6.86 (Or (Eq (plant a_3) False) (Or (Eq (eats (skS.0 2 a_2) a_3) False) (Eq False True))))) % 6.67/6.86 Clause #278 (by clausification #[212]): ∀ (a a_1 a_2 a_3 : Iota), % 6.67/6.86 Or (Eq (eats (skS.0 0 a) (skS.0 3 a_1)) True) % 6.67/6.86 (Or (Eq (eats (skS.0 0 a) a_2) True) % 6.67/6.86 (Or (Eq (animal a_2) False) % 6.67/6.86 (Or (Eq (much_smaller a_2 (skS.0 0 a)) False) (Or (Eq (plant a_3) False) (Eq (eats a_2 a_3) False))))) % 6.67/6.86 Clause #279 (by superposition #[278, 98]): ∀ (a a_1 a_2 a_3 : Iota), % 6.67/6.86 Or (Eq (eats (skS.0 0 a) (skS.0 3 a_1)) True) % 6.67/6.86 (Or (Eq (eats (skS.0 0 a) (skS.0 5 a_2)) True) % 6.67/6.86 (Or (Eq (much_smaller (skS.0 5 a_2) (skS.0 0 a)) False) % 6.67/6.86 (Or (Eq (plant a_3) False) (Or (Eq (eats (skS.0 5 a_2) a_3) False) (Eq False True))))) % 6.67/6.86 Clause #332 (by clausification #[279]): ∀ (a a_1 a_2 a_3 : Iota), % 6.67/6.86 Or (Eq (eats (skS.0 0 a) (skS.0 3 a_1)) True) % 6.67/6.86 (Or (Eq (eats (skS.0 0 a) (skS.0 5 a_2)) True) % 6.67/6.86 (Or (Eq (much_smaller (skS.0 5 a_2) (skS.0 0 a)) False) % 6.67/6.86 (Or (Eq (plant a_3) False) (Eq (eats (skS.0 5 a_2) a_3) False)))) % 6.67/6.86 Clause #333 (by superposition #[332, 158]): ∀ (a a_1 a_2 a_3 : Iota), % 6.67/6.86 Or (Eq (eats (skS.0 0 a) (skS.0 3 a_1)) True) % 6.67/6.86 (Or (Eq (eats (skS.0 0 a) (skS.0 5 a_2)) True) % 6.67/6.86 (Or (Eq (plant a_3) False) (Or (Eq (eats (skS.0 5 a_2) a_3) False) (Eq False True)))) % 6.67/6.86 Clause #334 (by clausification #[333]): ∀ (a a_1 a_2 a_3 : Iota), % 6.67/6.86 Or (Eq (eats (skS.0 0 a) (skS.0 3 a_1)) True) % 6.67/6.86 (Or (Eq (eats (skS.0 0 a) (skS.0 5 a_2)) True) (Or (Eq (plant a_3) False) (Eq (eats (skS.0 5 a_2) a_3) False))) % 6.67/6.86 Clause #335 (by superposition #[334, 101]): ∀ (a a_1 a_2 a_3 : Iota), % 6.67/6.86 Or (Eq (eats (skS.0 0 a) (skS.0 3 a_1)) True) % 6.67/6.86 (Or (Eq (eats (skS.0 0 a) (skS.0 5 a_2)) True) (Or (Eq (eats (skS.0 5 a_2) (skS.0 3 a_3)) False) (Eq False True))) % 6.67/6.86 Clause #338 (by clausification #[335]): ∀ (a a_1 a_2 a_3 : Iota), % 6.67/6.86 Or (Eq (eats (skS.0 0 a) (skS.0 3 a_1)) True) % 6.67/6.86 (Or (Eq (eats (skS.0 0 a) (skS.0 5 a_2)) True) (Eq (eats (skS.0 5 a_2) (skS.0 3 a_3)) False)) % 6.67/6.86 Clause #347 (by clausification #[232]): ∀ (a a_1 a_2 a_3 : Iota), % 6.67/6.86 Or (Eq (eats (skS.0 5 a) (skS.0 3 a_1)) True) % 6.67/6.86 (Or (Eq (eats (skS.0 5 a) (skS.0 4 a_2)) True) % 6.67/6.86 (Or (Eq (much_smaller (skS.0 4 a_2) (skS.0 5 a)) False) % 6.67/6.86 (Or (Eq (plant a_3) False) (Eq (eats (skS.0 4 a_2) a_3) False)))) % 6.67/6.86 Clause #348 (by superposition #[347, 159]): ∀ (a a_1 a_2 a_3 : Iota), % 6.67/6.86 Or (Eq (eats (skS.0 5 a) (skS.0 3 a_1)) True) % 6.67/6.86 (Or (Eq (eats (skS.0 5 a) (skS.0 4 a_2)) True) % 6.67/6.86 (Or (Eq (plant a_3) False) (Or (Eq (eats (skS.0 4 a_2) a_3) False) (Eq False True)))) % 6.67/6.86 Clause #349 (by clausification #[348]): ∀ (a a_1 a_2 a_3 : Iota), % 6.67/6.86 Or (Eq (eats (skS.0 5 a) (skS.0 3 a_1)) True) % 6.67/6.86 (Or (Eq (eats (skS.0 5 a) (skS.0 4 a_2)) True) (Or (Eq (plant a_3) False) (Eq (eats (skS.0 4 a_2) a_3) False))) % 6.67/6.86 Clause #350 (by superposition #[349, 101]): ∀ (a a_1 a_2 a_3 : Iota), % 6.67/6.86 Or (Eq (eats (skS.0 5 a) (skS.0 3 a_1)) True) % 6.67/6.86 (Or (Eq (eats (skS.0 5 a) (skS.0 4 a_2)) True) (Or (Eq (eats (skS.0 4 a_2) (skS.0 3 a_3)) False) (Eq False True))) % 6.67/6.86 Clause #353 (by clausification #[350]): ∀ (a a_1 a_2 a_3 : Iota), % 6.72/6.88 Or (Eq (eats (skS.0 5 a) (skS.0 3 a_1)) True) % 6.72/6.88 (Or (Eq (eats (skS.0 5 a) (skS.0 4 a_2)) True) (Eq (eats (skS.0 4 a_2) (skS.0 3 a_3)) False)) % 6.72/6.88 Clause #373 (by clausification #[277]): ∀ (a a_1 a_2 a_3 : Iota), % 6.72/6.88 Or (Eq (eats (skS.0 4 a) (skS.0 3 a_1)) True) % 6.72/6.88 (Or (Eq (eats (skS.0 4 a) (skS.0 2 a_2)) True) % 6.72/6.88 (Or (Eq (much_smaller (skS.0 2 a_2) (skS.0 4 a)) False) % 6.72/6.88 (Or (Eq (plant a_3) False) (Eq (eats (skS.0 2 a_2) a_3) False)))) % 6.72/6.88 Clause #374 (by forward demodulation #[373, 152]): ∀ (a a_1 a_2 a_3 : Iota), % 6.72/6.88 Or (Eq (eats (skS.0 4 a) (skS.0 3 a_1)) True) % 6.72/6.88 (Or (Eq False True) % 6.72/6.88 (Or (Eq (much_smaller (skS.0 2 a_2) (skS.0 4 a)) False) % 6.72/6.88 (Or (Eq (plant a_3) False) (Eq (eats (skS.0 2 a_2) a_3) False)))) % 6.72/6.88 Clause #375 (by clausification #[374]): ∀ (a a_1 a_2 a_3 : Iota), % 6.72/6.88 Or (Eq (eats (skS.0 4 a) (skS.0 3 a_1)) True) % 6.72/6.88 (Or (Eq (much_smaller (skS.0 2 a_2) (skS.0 4 a)) False) % 6.72/6.88 (Or (Eq (plant a_3) False) (Eq (eats (skS.0 2 a_2) a_3) False))) % 6.72/6.88 Clause #376 (by superposition #[375, 156]): ∀ (a a_1 a_2 a_3 : Iota), % 6.72/6.88 Or (Eq (eats (skS.0 4 a) (skS.0 3 a_1)) True) % 6.72/6.88 (Or (Eq (plant a_2) False) (Or (Eq (eats (skS.0 2 a_3) a_2) False) (Eq False True))) % 6.72/6.88 Clause #377 (by clausification #[376]): ∀ (a a_1 a_2 a_3 : Iota), % 6.72/6.88 Or (Eq (eats (skS.0 4 a) (skS.0 3 a_1)) True) (Or (Eq (plant a_2) False) (Eq (eats (skS.0 2 a_3) a_2) False)) % 6.72/6.88 Clause #379 (by superposition #[377, 161]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.72/6.88 Or (Eq (eats (skS.0 4 a) (skS.0 3 a_1)) True) % 6.72/6.88 (Or (Eq (eats (skS.0 2 a_2) (skS.0 6 (skS.0 2 a_3) a_4)) False) (Eq False True)) % 6.72/6.88 Clause #385 (by clausification #[379]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.72/6.88 Or (Eq (eats (skS.0 4 a) (skS.0 3 a_1)) True) (Eq (eats (skS.0 2 a_2) (skS.0 6 (skS.0 2 a_3) a_4)) False) % 6.72/6.88 Clause #386 (by superposition #[385, 160]): ∀ (a a_1 : Iota), Or (Eq (eats (skS.0 4 a) (skS.0 3 a_1)) True) (Eq False True) % 6.72/6.88 Clause #387 (by clausification #[386]): ∀ (a a_1 : Iota), Eq (eats (skS.0 4 a) (skS.0 3 a_1)) True % 6.72/6.88 Clause #388 (by superposition #[387, 353]): ∀ (a a_1 a_2 : Iota), % 6.72/6.88 Or (Eq (eats (skS.0 5 a) (skS.0 3 a_1)) True) (Or (Eq (eats (skS.0 5 a) (skS.0 4 a_2)) True) (Eq True False)) % 6.72/6.88 Clause #389 (by clausification #[388]): ∀ (a a_1 a_2 : Iota), Or (Eq (eats (skS.0 5 a) (skS.0 3 a_1)) True) (Eq (eats (skS.0 5 a) (skS.0 4 a_2)) True) % 6.72/6.88 Clause #391 (by superposition #[389, 208]): ∀ (a a_1 a_2 a_3 : Iota), % 6.72/6.88 Or (Eq (eats (skS.0 5 a) (skS.0 3 a_1)) True) % 6.72/6.88 (Or (Eq True False) (Or (Eq (grain a_2) False) (Eq (eats (skS.0 4 a_3) a_2) False))) % 6.72/6.88 Clause #392 (by clausification #[391]): ∀ (a a_1 a_2 a_3 : Iota), % 6.72/6.88 Or (Eq (eats (skS.0 5 a) (skS.0 3 a_1)) True) (Or (Eq (grain a_2) False) (Eq (eats (skS.0 4 a_3) a_2) False)) % 6.72/6.88 Clause #393 (by superposition #[392, 43]): ∀ (a a_1 a_2 a_3 : Iota), % 6.72/6.88 Or (Eq (eats (skS.0 5 a) (skS.0 3 a_1)) True) (Or (Eq (eats (skS.0 4 a_2) (skS.0 3 a_3)) False) (Eq False True)) % 6.72/6.88 Clause #395 (by clausification #[393]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eats (skS.0 5 a) (skS.0 3 a_1)) True) (Eq (eats (skS.0 4 a_2) (skS.0 3 a_3)) False) % 6.72/6.88 Clause #396 (by superposition #[395, 387]): ∀ (a a_1 : Iota), Or (Eq (eats (skS.0 5 a) (skS.0 3 a_1)) True) (Eq False True) % 6.72/6.88 Clause #397 (by clausification #[396]): ∀ (a a_1 : Iota), Eq (eats (skS.0 5 a) (skS.0 3 a_1)) True % 6.72/6.88 Clause #398 (by superposition #[397, 338]): ∀ (a a_1 a_2 : Iota), % 6.72/6.88 Or (Eq (eats (skS.0 0 a) (skS.0 3 a_1)) True) (Or (Eq (eats (skS.0 0 a) (skS.0 5 a_2)) True) (Eq True False)) % 6.72/6.88 Clause #399 (by clausification #[398]): ∀ (a a_1 a_2 : Iota), Or (Eq (eats (skS.0 0 a) (skS.0 3 a_1)) True) (Eq (eats (skS.0 0 a) (skS.0 5 a_2)) True) % 6.72/6.88 Clause #403 (by superposition #[399, 146]): ∀ (a a_1 a_2 : Iota), Or (Eq (eats (skS.0 0 a) (skS.0 3 a_1)) True) (Or (Eq True False) (Eq (fox (skS.0 5 a_2)) False)) % 6.72/6.88 Clause #406 (by clausification #[403]): ∀ (a a_1 a_2 : Iota), Or (Eq (eats (skS.0 0 a) (skS.0 3 a_1)) True) (Eq (fox (skS.0 5 a_2)) False) % 6.72/6.88 Clause #407 (by superposition #[406, 49]): ∀ (a a_1 : Iota), Or (Eq (eats (skS.0 0 a) (skS.0 3 a_1)) True) (Eq False True) % 6.72/6.88 Clause #409 (by clausification #[407]): ∀ (a a_1 : Iota), Eq (eats (skS.0 0 a) (skS.0 3 a_1)) True % 6.72/6.89 Clause #411 (by superposition #[409, 149]): ∀ (a : Iota), Or (Eq True False) (Eq (grain (skS.0 3 a)) False) % 6.72/6.89 Clause #412 (by clausification #[411]): ∀ (a : Iota), Eq (grain (skS.0 3 a)) False % 6.72/6.89 Clause #413 (by superposition #[412, 43]): Eq False True % 6.72/6.89 Clause #414 (by clausification #[413]): False % 6.72/6.89 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------