%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : PUZ031^5 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n029.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.25s 6.44s % Output : Proof 6.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : PUZ031^5 : TPTP v9.2.0. Released v4.0.0. % 0.00/0.11 % Command : duper %s % 0.11/0.32 % Computer : n029.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 300 % 0.11/0.32 % DateTime : Thu Oct 2 20:57:23 EDT 2025 % 0.11/0.32 % CPUTime : % 6.25/6.44 SZS status Theorem for theBenchmark.p % 6.25/6.44 SZS output start Proof for theBenchmark.p % 6.25/6.44 Clause #0 (by assumption #[]): Eq % 6.25/6.44 (Not % 6.25/6.44 (Not % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) % 6.25/6.44 (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 6.25/6.44 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 6.25/6.44 (∀ (X : Iota), Or (animal X) (Not (caterpillar X)))) % 6.25/6.44 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 6.25/6.44 (wolf a_wolf)) % 6.25/6.44 (fox a_fox)) % 6.25/6.44 (bird a_bird)) % 6.25/6.44 (caterpillar a_caterpillar)) % 6.25/6.44 (snail a_snail)) % 6.25/6.44 (grain a_grain)) % 6.25/6.44 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 6.25/6.44 (∀ (A P S O : Iota), % 6.25/6.44 Or % 6.25/6.44 (Or % 6.25/6.44 (Or % 6.25/6.44 (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) % 6.25/6.44 (Not (animal S))) % 6.25/6.44 (Not (plant O))) % 6.25/6.44 (Not (msmaller S A))) % 6.25/6.44 (Not (eats S O)))) % 6.25/6.44 (∀ (C B : Iota), Or (Or (msmaller C B) (Not (caterpillar C))) (Not (bird B)))) % 6.25/6.44 (∀ (S B : Iota), Or (Or (msmaller S B) (Not (snail S))) (Not (bird B)))) % 6.25/6.44 (∀ (B F : Iota), Or (Or (msmaller B F) (Not (bird B))) (Not (fox F)))) % 6.25/6.44 (∀ (F W : Iota), Or (Or (msmaller F W) (Not (fox F))) (Not (wolf W)))) % 6.25/6.44 (∀ (F W : Iota), Or (Or (Not (wolf W)) (Not (fox F))) (Not (eats W F)))) % 6.25/6.44 (∀ (W G : Iota), Or (Or (Not (wolf W)) (Not (grain G))) (Not (eats W G)))) % 6.25/6.44 (∀ (B C : Iota), Or (Or (eats B C) (Not (bird B))) (Not (caterpillar C)))) % 6.25/6.44 (∀ (B S : Iota), Or (Or (Not (bird B)) (Not (snail S))) (Not (eats B S)))) % 6.25/6.44 (∀ (C : Iota), Or (plant (cf C)) (Not (caterpillar C)))) % 6.25/6.44 (∀ (C : Iota), Or (eats C (cf C)) (Not (caterpillar C)))) % 6.25/6.44 (∀ (S : Iota), Or (plant (sf S)) (Not (snail S)))) % 6.25/6.44 (∀ (S : Iota), Or (eats S (sf S)) (Not (snail S)))) % 6.25/6.44 (∀ (A E G : Iota), % 6.25/6.44 Or (Or (Or (Or (Not (animal A)) (Not (animal E))) (Not (grain G))) (Not (eats A E))) (Not (eats E G)))))) % 6.25/6.44 True % 6.25/6.44 Clause #1 (by clausification #[0]): Eq % 6.25/6.44 (Not % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.44 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) % 6.25/6.47 (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 6.25/6.47 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 6.25/6.47 (∀ (X : Iota), Or (animal X) (Not (caterpillar X)))) % 6.25/6.47 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 6.25/6.47 (wolf a_wolf)) % 6.25/6.47 (fox a_fox)) % 6.25/6.47 (bird a_bird)) % 6.25/6.47 (caterpillar a_caterpillar)) % 6.25/6.47 (snail a_snail)) % 6.25/6.47 (grain a_grain)) % 6.25/6.47 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 6.25/6.47 (∀ (A P S O : Iota), % 6.25/6.47 Or % 6.25/6.47 (Or % 6.25/6.47 (Or % 6.25/6.47 (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) % 6.25/6.47 (Not (animal S))) % 6.25/6.47 (Not (plant O))) % 6.25/6.47 (Not (msmaller S A))) % 6.25/6.47 (Not (eats S O)))) % 6.25/6.47 (∀ (C B : Iota), Or (Or (msmaller C B) (Not (caterpillar C))) (Not (bird B)))) % 6.25/6.47 (∀ (S B : Iota), Or (Or (msmaller S B) (Not (snail S))) (Not (bird B)))) % 6.25/6.47 (∀ (B F : Iota), Or (Or (msmaller B F) (Not (bird B))) (Not (fox F)))) % 6.25/6.47 (∀ (F W : Iota), Or (Or (msmaller F W) (Not (fox F))) (Not (wolf W)))) % 6.25/6.47 (∀ (F W : Iota), Or (Or (Not (wolf W)) (Not (fox F))) (Not (eats W F)))) % 6.25/6.47 (∀ (W G : Iota), Or (Or (Not (wolf W)) (Not (grain G))) (Not (eats W G)))) % 6.25/6.47 (∀ (B C : Iota), Or (Or (eats B C) (Not (bird B))) (Not (caterpillar C)))) % 6.25/6.47 (∀ (B S : Iota), Or (Or (Not (bird B)) (Not (snail S))) (Not (eats B S)))) % 6.25/6.47 (∀ (C : Iota), Or (plant (cf C)) (Not (caterpillar C)))) % 6.25/6.47 (∀ (C : Iota), Or (eats C (cf C)) (Not (caterpillar C)))) % 6.25/6.47 (∀ (S : Iota), Or (plant (sf S)) (Not (snail S)))) % 6.25/6.47 (∀ (S : Iota), Or (eats S (sf S)) (Not (snail S)))) % 6.25/6.47 (∀ (A E G : Iota), % 6.25/6.47 Or (Or (Or (Or (Not (animal A)) (Not (animal E))) (Not (grain G))) (Not (eats A E))) (Not (eats E G))))) % 6.25/6.47 False % 6.25/6.47 Clause #2 (by clausification #[1]): Eq % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And % 6.25/6.47 (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) % 6.25/6.47 (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 6.25/6.47 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 6.25/6.50 (∀ (X : Iota), Or (animal X) (Not (caterpillar X)))) % 6.25/6.50 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 6.25/6.50 (wolf a_wolf)) % 6.25/6.50 (fox a_fox)) % 6.25/6.50 (bird a_bird)) % 6.25/6.50 (caterpillar a_caterpillar)) % 6.25/6.50 (snail a_snail)) % 6.25/6.50 (grain a_grain)) % 6.25/6.50 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 6.25/6.50 (∀ (A P S O : Iota), % 6.25/6.50 Or % 6.25/6.50 (Or % 6.25/6.50 (Or % 6.25/6.50 (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) % 6.25/6.50 (Not (animal S))) % 6.25/6.50 (Not (plant O))) % 6.25/6.50 (Not (msmaller S A))) % 6.25/6.50 (Not (eats S O)))) % 6.25/6.50 (∀ (C B : Iota), Or (Or (msmaller C B) (Not (caterpillar C))) (Not (bird B)))) % 6.25/6.50 (∀ (S B : Iota), Or (Or (msmaller S B) (Not (snail S))) (Not (bird B)))) % 6.25/6.50 (∀ (B F : Iota), Or (Or (msmaller B F) (Not (bird B))) (Not (fox F)))) % 6.25/6.50 (∀ (F W : Iota), Or (Or (msmaller F W) (Not (fox F))) (Not (wolf W)))) % 6.25/6.50 (∀ (F W : Iota), Or (Or (Not (wolf W)) (Not (fox F))) (Not (eats W F)))) % 6.25/6.50 (∀ (W G : Iota), Or (Or (Not (wolf W)) (Not (grain G))) (Not (eats W G)))) % 6.25/6.50 (∀ (B C : Iota), Or (Or (eats B C) (Not (bird B))) (Not (caterpillar C)))) % 6.25/6.50 (∀ (B S : Iota), Or (Or (Not (bird B)) (Not (snail S))) (Not (eats B S)))) % 6.25/6.50 (∀ (C : Iota), Or (plant (cf C)) (Not (caterpillar C)))) % 6.25/6.50 (∀ (C : Iota), Or (eats C (cf C)) (Not (caterpillar C)))) % 6.25/6.50 (∀ (S : Iota), Or (plant (sf S)) (Not (snail S)))) % 6.25/6.50 (∀ (S : Iota), Or (eats S (sf S)) (Not (snail S)))) % 6.25/6.50 (∀ (A E G : Iota), % 6.25/6.50 Or (Or (Or (Or (Not (animal A)) (Not (animal E))) (Not (grain G))) (Not (eats A E))) (Not (eats E G)))) % 6.25/6.50 True % 6.25/6.50 Clause #3 (by clausification #[2]): Eq % 6.25/6.50 (∀ (A E G : Iota), % 6.25/6.50 Or (Or (Or (Or (Not (animal A)) (Not (animal E))) (Not (grain G))) (Not (eats A E))) (Not (eats E G))) % 6.25/6.50 True % 6.25/6.50 Clause #4 (by clausification #[2]): Eq % 6.25/6.50 (And % 6.25/6.50 (And % 6.25/6.50 (And % 6.25/6.50 (And % 6.25/6.50 (And % 6.25/6.50 (And % 6.25/6.50 (And % 6.25/6.50 (And % 6.25/6.50 (And % 6.25/6.50 (And % 6.25/6.50 (And % 6.25/6.50 (And % 6.25/6.50 (And % 6.25/6.50 (And % 6.25/6.50 (And % 6.25/6.50 (And % 6.25/6.50 (And % 6.25/6.50 (And % 6.25/6.50 (And % 6.25/6.50 (And % 6.25/6.50 (And % 6.25/6.50 (And % 6.25/6.50 (And % 6.25/6.50 (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) % 6.25/6.50 (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 6.25/6.50 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 6.25/6.50 (∀ (X : Iota), Or (animal X) (Not (caterpillar X)))) % 6.25/6.50 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 6.25/6.50 (wolf a_wolf)) % 6.25/6.50 (fox a_fox)) % 6.25/6.50 (bird a_bird)) % 6.25/6.50 (caterpillar a_caterpillar)) % 6.25/6.50 (snail a_snail)) % 6.25/6.50 (grain a_grain)) % 6.25/6.50 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 6.34/6.54 (∀ (A P S O : Iota), % 6.34/6.54 Or % 6.34/6.54 (Or % 6.34/6.54 (Or % 6.34/6.54 (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) % 6.34/6.54 (Not (animal S))) % 6.34/6.54 (Not (plant O))) % 6.34/6.54 (Not (msmaller S A))) % 6.34/6.54 (Not (eats S O)))) % 6.34/6.54 (∀ (C B : Iota), Or (Or (msmaller C B) (Not (caterpillar C))) (Not (bird B)))) % 6.34/6.54 (∀ (S B : Iota), Or (Or (msmaller S B) (Not (snail S))) (Not (bird B)))) % 6.34/6.54 (∀ (B F : Iota), Or (Or (msmaller B F) (Not (bird B))) (Not (fox F)))) % 6.34/6.54 (∀ (F W : Iota), Or (Or (msmaller F W) (Not (fox F))) (Not (wolf W)))) % 6.34/6.54 (∀ (F W : Iota), Or (Or (Not (wolf W)) (Not (fox F))) (Not (eats W F)))) % 6.34/6.54 (∀ (W G : Iota), Or (Or (Not (wolf W)) (Not (grain G))) (Not (eats W G)))) % 6.34/6.54 (∀ (B C : Iota), Or (Or (eats B C) (Not (bird B))) (Not (caterpillar C)))) % 6.34/6.54 (∀ (B S : Iota), Or (Or (Not (bird B)) (Not (snail S))) (Not (eats B S)))) % 6.34/6.54 (∀ (C : Iota), Or (plant (cf C)) (Not (caterpillar C)))) % 6.34/6.54 (∀ (C : Iota), Or (eats C (cf C)) (Not (caterpillar C)))) % 6.34/6.54 (∀ (S : Iota), Or (plant (sf S)) (Not (snail S)))) % 6.34/6.54 (∀ (S : Iota), Or (eats S (sf S)) (Not (snail S)))) % 6.34/6.54 True % 6.34/6.54 Clause #5 (by clausification #[3]): ∀ (a : Iota), % 6.34/6.54 Eq % 6.34/6.54 (∀ (E G : Iota), % 6.34/6.54 Or (Or (Or (Or (Not (animal a)) (Not (animal E))) (Not (grain G))) (Not (eats a E))) (Not (eats E G))) % 6.34/6.54 True % 6.34/6.54 Clause #6 (by clausification #[5]): ∀ (a a_1 : Iota), % 6.34/6.54 Eq % 6.34/6.54 (∀ (G : Iota), % 6.34/6.54 Or (Or (Or (Or (Not (animal a)) (Not (animal a_1))) (Not (grain G))) (Not (eats a a_1))) (Not (eats a_1 G))) % 6.34/6.54 True % 6.34/6.54 Clause #7 (by clausification #[6]): ∀ (a a_1 a_2 : Iota), % 6.34/6.54 Eq (Or (Or (Or (Or (Not (animal a)) (Not (animal a_1))) (Not (grain a_2))) (Not (eats a a_1))) (Not (eats a_1 a_2))) % 6.34/6.54 True % 6.34/6.54 Clause #8 (by clausification #[7]): ∀ (a a_1 a_2 : Iota), % 6.34/6.54 Or (Eq (Or (Or (Or (Not (animal a)) (Not (animal a_1))) (Not (grain a_2))) (Not (eats a a_1))) True) % 6.34/6.54 (Eq (Not (eats a_1 a_2)) True) % 6.34/6.54 Clause #9 (by clausification #[8]): ∀ (a a_1 a_2 : Iota), % 6.34/6.54 Or (Eq (Not (eats a a_1)) True) % 6.34/6.54 (Or (Eq (Or (Or (Not (animal a_2)) (Not (animal a))) (Not (grain a_1))) True) (Eq (Not (eats a_2 a)) True)) % 6.34/6.54 Clause #10 (by clausification #[9]): ∀ (a a_1 a_2 : Iota), % 6.34/6.54 Or (Eq (Or (Or (Not (animal a)) (Not (animal a_1))) (Not (grain a_2))) True) % 6.34/6.54 (Or (Eq (Not (eats a a_1)) True) (Eq (eats a_1 a_2) False)) % 6.34/6.54 Clause #11 (by clausification #[10]): ∀ (a a_1 a_2 : Iota), % 6.34/6.54 Or (Eq (Not (eats a a_1)) True) % 6.34/6.54 (Or (Eq (eats a_1 a_2) False) (Or (Eq (Or (Not (animal a)) (Not (animal a_1))) True) (Eq (Not (grain a_2)) True))) % 6.34/6.54 Clause #12 (by clausification #[11]): ∀ (a a_1 a_2 : Iota), % 6.34/6.54 Or (Eq (eats a a_1) False) % 6.34/6.54 (Or (Eq (Or (Not (animal a_2)) (Not (animal a))) True) (Or (Eq (Not (grain a_1)) True) (Eq (eats a_2 a) False))) % 6.34/6.54 Clause #13 (by clausification #[12]): ∀ (a a_1 a_2 : Iota), % 6.34/6.54 Or (Eq (eats a a_1) False) % 6.34/6.54 (Or (Eq (Not (grain a_1)) True) % 6.34/6.54 (Or (Eq (eats a_2 a) False) (Or (Eq (Not (animal a_2)) True) (Eq (Not (animal a)) True)))) % 6.34/6.54 Clause #14 (by clausification #[13]): ∀ (a a_1 a_2 : Iota), % 6.34/6.54 Or (Eq (eats a a_1) False) % 6.34/6.54 (Or (Eq (eats a_2 a) False) % 6.34/6.54 (Or (Eq (Not (animal a_2)) True) (Or (Eq (Not (animal a)) True) (Eq (grain a_1) False)))) % 6.34/6.54 Clause #15 (by clausification #[14]): ∀ (a a_1 a_2 : Iota), % 6.34/6.54 Or (Eq (eats a a_1) False) % 6.34/6.54 (Or (Eq (eats a_2 a) False) (Or (Eq (Not (animal a)) True) (Or (Eq (grain a_1) False) (Eq (animal a_2) False)))) % 6.34/6.54 Clause #16 (by clausification #[15]): ∀ (a a_1 a_2 : Iota), % 6.34/6.54 Or (Eq (eats a a_1) False) % 6.34/6.54 (Or (Eq (eats a_2 a) False) (Or (Eq (grain a_1) False) (Or (Eq (animal a_2) False) (Eq (animal a) False)))) % 6.34/6.54 Clause #17 (by clausification #[4]): Eq (∀ (S : Iota), Or (eats S (sf S)) (Not (snail S))) True % 6.34/6.59 Clause #18 (by clausification #[4]): Eq % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) % 6.34/6.59 (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 6.34/6.59 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 6.34/6.59 (∀ (X : Iota), Or (animal X) (Not (caterpillar X)))) % 6.34/6.59 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 6.34/6.59 (wolf a_wolf)) % 6.34/6.59 (fox a_fox)) % 6.34/6.59 (bird a_bird)) % 6.34/6.59 (caterpillar a_caterpillar)) % 6.34/6.59 (snail a_snail)) % 6.34/6.59 (grain a_grain)) % 6.34/6.59 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 6.34/6.59 (∀ (A P S O : Iota), % 6.34/6.59 Or % 6.34/6.59 (Or % 6.34/6.59 (Or % 6.34/6.59 (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) % 6.34/6.59 (Not (animal S))) % 6.34/6.59 (Not (plant O))) % 6.34/6.59 (Not (msmaller S A))) % 6.34/6.59 (Not (eats S O)))) % 6.34/6.59 (∀ (C B : Iota), Or (Or (msmaller C B) (Not (caterpillar C))) (Not (bird B)))) % 6.34/6.59 (∀ (S B : Iota), Or (Or (msmaller S B) (Not (snail S))) (Not (bird B)))) % 6.34/6.59 (∀ (B F : Iota), Or (Or (msmaller B F) (Not (bird B))) (Not (fox F)))) % 6.34/6.59 (∀ (F W : Iota), Or (Or (msmaller F W) (Not (fox F))) (Not (wolf W)))) % 6.34/6.59 (∀ (F W : Iota), Or (Or (Not (wolf W)) (Not (fox F))) (Not (eats W F)))) % 6.34/6.59 (∀ (W G : Iota), Or (Or (Not (wolf W)) (Not (grain G))) (Not (eats W G)))) % 6.34/6.59 (∀ (B C : Iota), Or (Or (eats B C) (Not (bird B))) (Not (caterpillar C)))) % 6.34/6.59 (∀ (B S : Iota), Or (Or (Not (bird B)) (Not (snail S))) (Not (eats B S)))) % 6.34/6.59 (∀ (C : Iota), Or (plant (cf C)) (Not (caterpillar C)))) % 6.34/6.59 (∀ (C : Iota), Or (eats C (cf C)) (Not (caterpillar C)))) % 6.34/6.59 (∀ (S : Iota), Or (plant (sf S)) (Not (snail S)))) % 6.34/6.59 True % 6.34/6.59 Clause #19 (by clausification #[17]): ∀ (a : Iota), Eq (Or (eats a (sf a)) (Not (snail a))) True % 6.34/6.59 Clause #20 (by clausification #[19]): ∀ (a : Iota), Or (Eq (eats a (sf a)) True) (Eq (Not (snail a)) True) % 6.34/6.59 Clause #21 (by clausification #[20]): ∀ (a : Iota), Or (Eq (eats a (sf a)) True) (Eq (snail a) False) % 6.34/6.59 Clause #22 (by clausification #[18]): Eq (∀ (S : Iota), Or (plant (sf S)) (Not (snail S))) True % 6.34/6.59 Clause #23 (by clausification #[18]): Eq % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And % 6.34/6.59 (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) % 6.34/6.59 (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 6.45/6.62 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 6.45/6.62 (∀ (X : Iota), Or (animal X) (Not (caterpillar X)))) % 6.45/6.62 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 6.45/6.62 (wolf a_wolf)) % 6.45/6.62 (fox a_fox)) % 6.45/6.62 (bird a_bird)) % 6.45/6.62 (caterpillar a_caterpillar)) % 6.45/6.62 (snail a_snail)) % 6.45/6.62 (grain a_grain)) % 6.45/6.62 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 6.45/6.62 (∀ (A P S O : Iota), % 6.45/6.62 Or % 6.45/6.62 (Or % 6.45/6.62 (Or % 6.45/6.62 (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) % 6.45/6.62 (Not (animal S))) % 6.45/6.62 (Not (plant O))) % 6.45/6.62 (Not (msmaller S A))) % 6.45/6.62 (Not (eats S O)))) % 6.45/6.62 (∀ (C B : Iota), Or (Or (msmaller C B) (Not (caterpillar C))) (Not (bird B)))) % 6.45/6.62 (∀ (S B : Iota), Or (Or (msmaller S B) (Not (snail S))) (Not (bird B)))) % 6.45/6.62 (∀ (B F : Iota), Or (Or (msmaller B F) (Not (bird B))) (Not (fox F)))) % 6.45/6.62 (∀ (F W : Iota), Or (Or (msmaller F W) (Not (fox F))) (Not (wolf W)))) % 6.45/6.62 (∀ (F W : Iota), Or (Or (Not (wolf W)) (Not (fox F))) (Not (eats W F)))) % 6.45/6.62 (∀ (W G : Iota), Or (Or (Not (wolf W)) (Not (grain G))) (Not (eats W G)))) % 6.45/6.62 (∀ (B C : Iota), Or (Or (eats B C) (Not (bird B))) (Not (caterpillar C)))) % 6.45/6.62 (∀ (B S : Iota), Or (Or (Not (bird B)) (Not (snail S))) (Not (eats B S)))) % 6.45/6.62 (∀ (C : Iota), Or (plant (cf C)) (Not (caterpillar C)))) % 6.45/6.62 (∀ (C : Iota), Or (eats C (cf C)) (Not (caterpillar C)))) % 6.45/6.62 True % 6.45/6.62 Clause #24 (by clausification #[22]): ∀ (a : Iota), Eq (Or (plant (sf a)) (Not (snail a))) True % 6.45/6.62 Clause #25 (by clausification #[24]): ∀ (a : Iota), Or (Eq (plant (sf a)) True) (Eq (Not (snail a)) True) % 6.45/6.62 Clause #26 (by clausification #[25]): ∀ (a : Iota), Or (Eq (plant (sf a)) True) (Eq (snail a) False) % 6.45/6.62 Clause #28 (by clausification #[23]): Eq % 6.45/6.62 (And % 6.45/6.62 (And % 6.45/6.62 (And % 6.45/6.62 (And % 6.45/6.62 (And % 6.45/6.62 (And % 6.45/6.62 (And % 6.45/6.62 (And % 6.45/6.62 (And % 6.45/6.62 (And % 6.45/6.62 (And % 6.45/6.62 (And % 6.45/6.62 (And % 6.45/6.62 (And % 6.45/6.62 (And % 6.45/6.62 (And % 6.45/6.62 (And % 6.45/6.62 (And % 6.45/6.62 (And % 6.45/6.62 (And % 6.45/6.62 (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) % 6.45/6.62 (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 6.45/6.62 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 6.45/6.62 (∀ (X : Iota), Or (animal X) (Not (caterpillar X)))) % 6.45/6.62 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 6.45/6.62 (wolf a_wolf)) % 6.45/6.62 (fox a_fox)) % 6.45/6.62 (bird a_bird)) % 6.45/6.62 (caterpillar a_caterpillar)) % 6.45/6.62 (snail a_snail)) % 6.45/6.62 (grain a_grain)) % 6.45/6.62 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 6.45/6.62 (∀ (A P S O : Iota), % 6.45/6.62 Or % 6.45/6.62 (Or % 6.45/6.62 (Or % 6.45/6.62 (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) % 6.45/6.62 (Not (animal S))) % 6.45/6.62 (Not (plant O))) % 6.45/6.62 (Not (msmaller S A))) % 6.45/6.62 (Not (eats S O)))) % 6.45/6.66 (∀ (C B : Iota), Or (Or (msmaller C B) (Not (caterpillar C))) (Not (bird B)))) % 6.45/6.66 (∀ (S B : Iota), Or (Or (msmaller S B) (Not (snail S))) (Not (bird B)))) % 6.45/6.66 (∀ (B F : Iota), Or (Or (msmaller B F) (Not (bird B))) (Not (fox F)))) % 6.45/6.66 (∀ (F W : Iota), Or (Or (msmaller F W) (Not (fox F))) (Not (wolf W)))) % 6.45/6.66 (∀ (F W : Iota), Or (Or (Not (wolf W)) (Not (fox F))) (Not (eats W F)))) % 6.45/6.66 (∀ (W G : Iota), Or (Or (Not (wolf W)) (Not (grain G))) (Not (eats W G)))) % 6.45/6.66 (∀ (B C : Iota), Or (Or (eats B C) (Not (bird B))) (Not (caterpillar C)))) % 6.45/6.66 (∀ (B S : Iota), Or (Or (Not (bird B)) (Not (snail S))) (Not (eats B S)))) % 6.45/6.66 (∀ (C : Iota), Or (plant (cf C)) (Not (caterpillar C)))) % 6.45/6.66 True % 6.45/6.66 Clause #33 (by clausification #[28]): Eq % 6.45/6.66 (And % 6.45/6.66 (And % 6.45/6.66 (And % 6.45/6.66 (And % 6.45/6.66 (And % 6.45/6.66 (And % 6.45/6.66 (And % 6.45/6.66 (And % 6.45/6.66 (And % 6.45/6.66 (And % 6.45/6.66 (And % 6.45/6.66 (And % 6.45/6.66 (And % 6.45/6.66 (And % 6.45/6.66 (And % 6.45/6.66 (And % 6.45/6.66 (And % 6.45/6.66 (And % 6.45/6.66 (And % 6.45/6.66 (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) % 6.45/6.66 (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 6.45/6.66 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 6.45/6.66 (∀ (X : Iota), Or (animal X) (Not (caterpillar X)))) % 6.45/6.66 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 6.45/6.66 (wolf a_wolf)) % 6.45/6.66 (fox a_fox)) % 6.45/6.66 (bird a_bird)) % 6.45/6.66 (caterpillar a_caterpillar)) % 6.45/6.66 (snail a_snail)) % 6.45/6.66 (grain a_grain)) % 6.45/6.66 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 6.45/6.66 (∀ (A P S O : Iota), % 6.45/6.66 Or % 6.45/6.66 (Or % 6.45/6.66 (Or % 6.45/6.66 (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) (Not (animal S))) % 6.45/6.66 (Not (plant O))) % 6.45/6.66 (Not (msmaller S A))) % 6.45/6.66 (Not (eats S O)))) % 6.45/6.66 (∀ (C B : Iota), Or (Or (msmaller C B) (Not (caterpillar C))) (Not (bird B)))) % 6.45/6.66 (∀ (S B : Iota), Or (Or (msmaller S B) (Not (snail S))) (Not (bird B)))) % 6.45/6.66 (∀ (B F : Iota), Or (Or (msmaller B F) (Not (bird B))) (Not (fox F)))) % 6.45/6.66 (∀ (F W : Iota), Or (Or (msmaller F W) (Not (fox F))) (Not (wolf W)))) % 6.45/6.66 (∀ (F W : Iota), Or (Or (Not (wolf W)) (Not (fox F))) (Not (eats W F)))) % 6.45/6.66 (∀ (W G : Iota), Or (Or (Not (wolf W)) (Not (grain G))) (Not (eats W G)))) % 6.45/6.66 (∀ (B C : Iota), Or (Or (eats B C) (Not (bird B))) (Not (caterpillar C)))) % 6.45/6.67 (∀ (B S : Iota), Or (Or (Not (bird B)) (Not (snail S))) (Not (eats B S)))) % 6.45/6.67 True % 6.45/6.67 Clause #37 (by clausification #[33]): Eq (∀ (B S : Iota), Or (Or (Not (bird B)) (Not (snail S))) (Not (eats B S))) True % 6.45/6.67 Clause #38 (by clausification #[33]): Eq % 6.45/6.67 (And % 6.45/6.67 (And % 6.45/6.67 (And % 6.45/6.67 (And % 6.45/6.67 (And % 6.45/6.67 (And % 6.45/6.67 (And % 6.45/6.67 (And % 6.45/6.67 (And % 6.45/6.67 (And % 6.45/6.67 (And % 6.45/6.67 (And % 6.45/6.67 (And % 6.45/6.67 (And % 6.45/6.67 (And % 6.45/6.67 (And % 6.45/6.67 (And % 6.45/6.67 (And % 6.45/6.67 (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) % 6.45/6.67 (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 6.45/6.67 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 6.45/6.67 (∀ (X : Iota), Or (animal X) (Not (caterpillar X)))) % 6.54/6.70 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 6.54/6.70 (wolf a_wolf)) % 6.54/6.70 (fox a_fox)) % 6.54/6.70 (bird a_bird)) % 6.54/6.70 (caterpillar a_caterpillar)) % 6.54/6.70 (snail a_snail)) % 6.54/6.70 (grain a_grain)) % 6.54/6.70 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 6.54/6.70 (∀ (A P S O : Iota), % 6.54/6.70 Or % 6.54/6.70 (Or % 6.54/6.70 (Or (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) (Not (animal S))) % 6.54/6.70 (Not (plant O))) % 6.54/6.70 (Not (msmaller S A))) % 6.54/6.70 (Not (eats S O)))) % 6.54/6.70 (∀ (C B : Iota), Or (Or (msmaller C B) (Not (caterpillar C))) (Not (bird B)))) % 6.54/6.70 (∀ (S B : Iota), Or (Or (msmaller S B) (Not (snail S))) (Not (bird B)))) % 6.54/6.70 (∀ (B F : Iota), Or (Or (msmaller B F) (Not (bird B))) (Not (fox F)))) % 6.54/6.70 (∀ (F W : Iota), Or (Or (msmaller F W) (Not (fox F))) (Not (wolf W)))) % 6.54/6.70 (∀ (F W : Iota), Or (Or (Not (wolf W)) (Not (fox F))) (Not (eats W F)))) % 6.54/6.70 (∀ (W G : Iota), Or (Or (Not (wolf W)) (Not (grain G))) (Not (eats W G)))) % 6.54/6.70 (∀ (B C : Iota), Or (Or (eats B C) (Not (bird B))) (Not (caterpillar C)))) % 6.54/6.70 True % 6.54/6.70 Clause #39 (by clausification #[37]): ∀ (a : Iota), Eq (∀ (S : Iota), Or (Or (Not (bird a)) (Not (snail S))) (Not (eats a S))) True % 6.54/6.70 Clause #40 (by clausification #[39]): ∀ (a a_1 : Iota), Eq (Or (Or (Not (bird a)) (Not (snail a_1))) (Not (eats a a_1))) True % 6.54/6.70 Clause #41 (by clausification #[40]): ∀ (a a_1 : Iota), Or (Eq (Or (Not (bird a)) (Not (snail a_1))) True) (Eq (Not (eats a a_1)) True) % 6.54/6.70 Clause #42 (by clausification #[41]): ∀ (a a_1 : Iota), Or (Eq (Not (eats a a_1)) True) (Or (Eq (Not (bird a)) True) (Eq (Not (snail a_1)) True)) % 6.54/6.70 Clause #43 (by clausification #[42]): ∀ (a a_1 : Iota), Or (Eq (Not (bird a)) True) (Or (Eq (Not (snail a_1)) True) (Eq (eats a a_1) False)) % 6.54/6.70 Clause #44 (by clausification #[43]): ∀ (a a_1 : Iota), Or (Eq (Not (snail a)) True) (Or (Eq (eats a_1 a) False) (Eq (bird a_1) False)) % 6.54/6.70 Clause #45 (by clausification #[44]): ∀ (a a_1 : Iota), Or (Eq (eats a a_1) False) (Or (Eq (bird a) False) (Eq (snail a_1) False)) % 6.54/6.70 Clause #47 (by clausification #[38]): Eq % 6.54/6.70 (And % 6.54/6.70 (And % 6.54/6.70 (And % 6.54/6.70 (And % 6.54/6.70 (And % 6.54/6.70 (And % 6.54/6.70 (And % 6.54/6.70 (And % 6.54/6.70 (And % 6.54/6.70 (And % 6.54/6.70 (And % 6.54/6.70 (And % 6.54/6.70 (And % 6.54/6.70 (And % 6.54/6.70 (And % 6.54/6.70 (And % 6.54/6.70 (And % 6.54/6.70 (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) % 6.54/6.70 (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 6.54/6.70 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 6.54/6.70 (∀ (X : Iota), Or (animal X) (Not (caterpillar X)))) % 6.54/6.70 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 6.54/6.70 (wolf a_wolf)) % 6.54/6.70 (fox a_fox)) % 6.54/6.70 (bird a_bird)) % 6.54/6.70 (caterpillar a_caterpillar)) % 6.54/6.70 (snail a_snail)) % 6.54/6.70 (grain a_grain)) % 6.54/6.70 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 6.54/6.70 (∀ (A P S O : Iota), % 6.54/6.70 Or % 6.54/6.70 (Or % 6.54/6.70 (Or (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) (Not (animal S))) % 6.54/6.70 (Not (plant O))) % 6.54/6.70 (Not (msmaller S A))) % 6.54/6.70 (Not (eats S O)))) % 6.54/6.70 (∀ (C B : Iota), Or (Or (msmaller C B) (Not (caterpillar C))) (Not (bird B)))) % 6.54/6.70 (∀ (S B : Iota), Or (Or (msmaller S B) (Not (snail S))) (Not (bird B)))) % 6.54/6.70 (∀ (B F : Iota), Or (Or (msmaller B F) (Not (bird B))) (Not (fox F)))) % 6.54/6.75 (∀ (F W : Iota), Or (Or (msmaller F W) (Not (fox F))) (Not (wolf W)))) % 6.54/6.75 (∀ (F W : Iota), Or (Or (Not (wolf W)) (Not (fox F))) (Not (eats W F)))) % 6.54/6.75 (∀ (W G : Iota), Or (Or (Not (wolf W)) (Not (grain G))) (Not (eats W G)))) % 6.54/6.75 True % 6.54/6.75 Clause #54 (by clausification #[47]): Eq (∀ (W G : Iota), Or (Or (Not (wolf W)) (Not (grain G))) (Not (eats W G))) True % 6.54/6.75 Clause #55 (by clausification #[47]): Eq % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) % 6.54/6.75 (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 6.54/6.75 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 6.54/6.75 (∀ (X : Iota), Or (animal X) (Not (caterpillar X)))) % 6.54/6.75 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 6.54/6.75 (wolf a_wolf)) % 6.54/6.75 (fox a_fox)) % 6.54/6.75 (bird a_bird)) % 6.54/6.75 (caterpillar a_caterpillar)) % 6.54/6.75 (snail a_snail)) % 6.54/6.75 (grain a_grain)) % 6.54/6.75 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 6.54/6.75 (∀ (A P S O : Iota), % 6.54/6.75 Or % 6.54/6.75 (Or % 6.54/6.75 (Or (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) (Not (animal S))) % 6.54/6.75 (Not (plant O))) % 6.54/6.75 (Not (msmaller S A))) % 6.54/6.75 (Not (eats S O)))) % 6.54/6.75 (∀ (C B : Iota), Or (Or (msmaller C B) (Not (caterpillar C))) (Not (bird B)))) % 6.54/6.75 (∀ (S B : Iota), Or (Or (msmaller S B) (Not (snail S))) (Not (bird B)))) % 6.54/6.75 (∀ (B F : Iota), Or (Or (msmaller B F) (Not (bird B))) (Not (fox F)))) % 6.54/6.75 (∀ (F W : Iota), Or (Or (msmaller F W) (Not (fox F))) (Not (wolf W)))) % 6.54/6.75 (∀ (F W : Iota), Or (Or (Not (wolf W)) (Not (fox F))) (Not (eats W F)))) % 6.54/6.75 True % 6.54/6.75 Clause #56 (by clausification #[54]): ∀ (a : Iota), Eq (∀ (G : Iota), Or (Or (Not (wolf a)) (Not (grain G))) (Not (eats a G))) True % 6.54/6.75 Clause #57 (by clausification #[56]): ∀ (a a_1 : Iota), Eq (Or (Or (Not (wolf a)) (Not (grain a_1))) (Not (eats a a_1))) True % 6.54/6.75 Clause #58 (by clausification #[57]): ∀ (a a_1 : Iota), Or (Eq (Or (Not (wolf a)) (Not (grain a_1))) True) (Eq (Not (eats a a_1)) True) % 6.54/6.75 Clause #59 (by clausification #[58]): ∀ (a a_1 : Iota), Or (Eq (Not (eats a a_1)) True) (Or (Eq (Not (wolf a)) True) (Eq (Not (grain a_1)) True)) % 6.54/6.75 Clause #60 (by clausification #[59]): ∀ (a a_1 : Iota), Or (Eq (Not (wolf a)) True) (Or (Eq (Not (grain a_1)) True) (Eq (eats a a_1) False)) % 6.54/6.75 Clause #61 (by clausification #[60]): ∀ (a a_1 : Iota), Or (Eq (Not (grain a)) True) (Or (Eq (eats a_1 a) False) (Eq (wolf a_1) False)) % 6.54/6.75 Clause #62 (by clausification #[61]): ∀ (a a_1 : Iota), Or (Eq (eats a a_1) False) (Or (Eq (wolf a) False) (Eq (grain a_1) False)) % 6.54/6.75 Clause #63 (by clausification #[55]): Eq (∀ (F W : Iota), Or (Or (Not (wolf W)) (Not (fox F))) (Not (eats W F))) True % 6.54/6.75 Clause #64 (by clausification #[55]): Eq % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And % 6.54/6.75 (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) % 6.54/6.75 (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 6.54/6.75 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 6.54/6.75 (∀ (X : Iota), Or (animal X) (Not (caterpillar X)))) % 6.54/6.75 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 6.63/6.79 (wolf a_wolf)) % 6.63/6.79 (fox a_fox)) % 6.63/6.79 (bird a_bird)) % 6.63/6.79 (caterpillar a_caterpillar)) % 6.63/6.79 (snail a_snail)) % 6.63/6.79 (grain a_grain)) % 6.63/6.79 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 6.63/6.79 (∀ (A P S O : Iota), % 6.63/6.79 Or % 6.63/6.79 (Or % 6.63/6.79 (Or (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) (Not (animal S))) % 6.63/6.79 (Not (plant O))) % 6.63/6.79 (Not (msmaller S A))) % 6.63/6.79 (Not (eats S O)))) % 6.63/6.79 (∀ (C B : Iota), Or (Or (msmaller C B) (Not (caterpillar C))) (Not (bird B)))) % 6.63/6.79 (∀ (S B : Iota), Or (Or (msmaller S B) (Not (snail S))) (Not (bird B)))) % 6.63/6.79 (∀ (B F : Iota), Or (Or (msmaller B F) (Not (bird B))) (Not (fox F)))) % 6.63/6.79 (∀ (F W : Iota), Or (Or (msmaller F W) (Not (fox F))) (Not (wolf W)))) % 6.63/6.79 True % 6.63/6.79 Clause #65 (by clausification #[63]): ∀ (a : Iota), Eq (∀ (W : Iota), Or (Or (Not (wolf W)) (Not (fox a))) (Not (eats W a))) True % 6.63/6.79 Clause #66 (by clausification #[65]): ∀ (a a_1 : Iota), Eq (Or (Or (Not (wolf a)) (Not (fox a_1))) (Not (eats a a_1))) True % 6.63/6.79 Clause #67 (by clausification #[66]): ∀ (a a_1 : Iota), Or (Eq (Or (Not (wolf a)) (Not (fox a_1))) True) (Eq (Not (eats a a_1)) True) % 6.63/6.79 Clause #68 (by clausification #[67]): ∀ (a a_1 : Iota), Or (Eq (Not (eats a a_1)) True) (Or (Eq (Not (wolf a)) True) (Eq (Not (fox a_1)) True)) % 6.63/6.79 Clause #69 (by clausification #[68]): ∀ (a a_1 : Iota), Or (Eq (Not (wolf a)) True) (Or (Eq (Not (fox a_1)) True) (Eq (eats a a_1) False)) % 6.63/6.79 Clause #70 (by clausification #[69]): ∀ (a a_1 : Iota), Or (Eq (Not (fox a)) True) (Or (Eq (eats a_1 a) False) (Eq (wolf a_1) False)) % 6.63/6.79 Clause #71 (by clausification #[70]): ∀ (a a_1 : Iota), Or (Eq (eats a a_1) False) (Or (Eq (wolf a) False) (Eq (fox a_1) False)) % 6.63/6.79 Clause #72 (by clausification #[64]): Eq (∀ (F W : Iota), Or (Or (msmaller F W) (Not (fox F))) (Not (wolf W))) True % 6.63/6.79 Clause #73 (by clausification #[64]): Eq % 6.63/6.79 (And % 6.63/6.79 (And % 6.63/6.79 (And % 6.63/6.79 (And % 6.63/6.79 (And % 6.63/6.79 (And % 6.63/6.79 (And % 6.63/6.79 (And % 6.63/6.79 (And % 6.63/6.79 (And % 6.63/6.79 (And % 6.63/6.79 (And % 6.63/6.79 (And % 6.63/6.79 (And % 6.63/6.79 (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) % 6.63/6.79 (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 6.63/6.79 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 6.63/6.79 (∀ (X : Iota), Or (animal X) (Not (caterpillar X)))) % 6.63/6.79 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 6.63/6.79 (wolf a_wolf)) % 6.63/6.79 (fox a_fox)) % 6.63/6.79 (bird a_bird)) % 6.63/6.79 (caterpillar a_caterpillar)) % 6.63/6.79 (snail a_snail)) % 6.63/6.79 (grain a_grain)) % 6.63/6.79 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 6.63/6.79 (∀ (A P S O : Iota), % 6.63/6.79 Or % 6.63/6.79 (Or % 6.63/6.79 (Or (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) (Not (animal S))) % 6.63/6.79 (Not (plant O))) % 6.63/6.79 (Not (msmaller S A))) % 6.63/6.79 (Not (eats S O)))) % 6.63/6.79 (∀ (C B : Iota), Or (Or (msmaller C B) (Not (caterpillar C))) (Not (bird B)))) % 6.63/6.79 (∀ (S B : Iota), Or (Or (msmaller S B) (Not (snail S))) (Not (bird B)))) % 6.63/6.79 (∀ (B F : Iota), Or (Or (msmaller B F) (Not (bird B))) (Not (fox F)))) % 6.63/6.79 True % 6.63/6.79 Clause #74 (by clausification #[72]): ∀ (a : Iota), Eq (∀ (W : Iota), Or (Or (msmaller a W) (Not (fox a))) (Not (wolf W))) True % 6.63/6.79 Clause #75 (by clausification #[74]): ∀ (a a_1 : Iota), Eq (Or (Or (msmaller a a_1) (Not (fox a))) (Not (wolf a_1))) True % 6.63/6.79 Clause #76 (by clausification #[75]): ∀ (a a_1 : Iota), Or (Eq (Or (msmaller a a_1) (Not (fox a))) True) (Eq (Not (wolf a_1)) True) % 6.63/6.79 Clause #77 (by clausification #[76]): ∀ (a a_1 : Iota), Or (Eq (Not (wolf a)) True) (Or (Eq (msmaller a_1 a) True) (Eq (Not (fox a_1)) True)) % 6.63/6.84 Clause #78 (by clausification #[77]): ∀ (a a_1 : Iota), Or (Eq (msmaller a a_1) True) (Or (Eq (Not (fox a)) True) (Eq (wolf a_1) False)) % 6.63/6.84 Clause #79 (by clausification #[78]): ∀ (a a_1 : Iota), Or (Eq (msmaller a a_1) True) (Or (Eq (wolf a_1) False) (Eq (fox a) False)) % 6.63/6.84 Clause #80 (by clausification #[73]): Eq (∀ (B F : Iota), Or (Or (msmaller B F) (Not (bird B))) (Not (fox F))) True % 6.63/6.84 Clause #81 (by clausification #[73]): Eq % 6.63/6.84 (And % 6.63/6.84 (And % 6.63/6.84 (And % 6.63/6.84 (And % 6.63/6.84 (And % 6.63/6.84 (And % 6.63/6.84 (And % 6.63/6.84 (And % 6.63/6.84 (And % 6.63/6.84 (And % 6.63/6.84 (And % 6.63/6.84 (And % 6.63/6.84 (And % 6.63/6.84 (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) % 6.63/6.84 (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 6.63/6.84 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 6.63/6.84 (∀ (X : Iota), Or (animal X) (Not (caterpillar X)))) % 6.63/6.84 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 6.63/6.84 (wolf a_wolf)) % 6.63/6.84 (fox a_fox)) % 6.63/6.84 (bird a_bird)) % 6.63/6.84 (caterpillar a_caterpillar)) % 6.63/6.84 (snail a_snail)) % 6.63/6.84 (grain a_grain)) % 6.63/6.84 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 6.63/6.84 (∀ (A P S O : Iota), % 6.63/6.84 Or % 6.63/6.84 (Or % 6.63/6.84 (Or (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) (Not (animal S))) % 6.63/6.84 (Not (plant O))) % 6.63/6.84 (Not (msmaller S A))) % 6.63/6.84 (Not (eats S O)))) % 6.63/6.84 (∀ (C B : Iota), Or (Or (msmaller C B) (Not (caterpillar C))) (Not (bird B)))) % 6.63/6.84 (∀ (S B : Iota), Or (Or (msmaller S B) (Not (snail S))) (Not (bird B)))) % 6.63/6.84 True % 6.63/6.84 Clause #82 (by clausification #[80]): ∀ (a : Iota), Eq (∀ (F : Iota), Or (Or (msmaller a F) (Not (bird a))) (Not (fox F))) True % 6.63/6.84 Clause #83 (by clausification #[82]): ∀ (a a_1 : Iota), Eq (Or (Or (msmaller a a_1) (Not (bird a))) (Not (fox a_1))) True % 6.63/6.84 Clause #84 (by clausification #[83]): ∀ (a a_1 : Iota), Or (Eq (Or (msmaller a a_1) (Not (bird a))) True) (Eq (Not (fox a_1)) True) % 6.63/6.84 Clause #85 (by clausification #[84]): ∀ (a a_1 : Iota), Or (Eq (Not (fox a)) True) (Or (Eq (msmaller a_1 a) True) (Eq (Not (bird a_1)) True)) % 6.63/6.84 Clause #86 (by clausification #[85]): ∀ (a a_1 : Iota), Or (Eq (msmaller a a_1) True) (Or (Eq (Not (bird a)) True) (Eq (fox a_1) False)) % 6.63/6.84 Clause #87 (by clausification #[86]): ∀ (a a_1 : Iota), Or (Eq (msmaller a a_1) True) (Or (Eq (fox a_1) False) (Eq (bird a) False)) % 6.63/6.84 Clause #88 (by clausification #[81]): Eq (∀ (S B : Iota), Or (Or (msmaller S B) (Not (snail S))) (Not (bird B))) True % 6.63/6.84 Clause #89 (by clausification #[81]): Eq % 6.63/6.84 (And % 6.63/6.84 (And % 6.63/6.84 (And % 6.63/6.84 (And % 6.63/6.84 (And % 6.63/6.84 (And % 6.63/6.84 (And % 6.63/6.84 (And % 6.63/6.84 (And % 6.63/6.84 (And % 6.63/6.84 (And % 6.63/6.84 (And % 6.63/6.84 (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 6.63/6.84 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 6.63/6.84 (∀ (X : Iota), Or (animal X) (Not (caterpillar X)))) % 6.63/6.84 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 6.63/6.84 (wolf a_wolf)) % 6.63/6.84 (fox a_fox)) % 6.63/6.84 (bird a_bird)) % 6.63/6.84 (caterpillar a_caterpillar)) % 6.63/6.84 (snail a_snail)) % 6.63/6.84 (grain a_grain)) % 6.63/6.84 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 6.63/6.84 (∀ (A P S O : Iota), % 6.63/6.84 Or % 6.63/6.84 (Or % 6.63/6.84 (Or (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) (Not (animal S))) % 6.63/6.84 (Not (plant O))) % 6.63/6.84 (Not (msmaller S A))) % 6.63/6.84 (Not (eats S O)))) % 6.63/6.84 (∀ (C B : Iota), Or (Or (msmaller C B) (Not (caterpillar C))) (Not (bird B)))) % 6.63/6.84 True % 6.63/6.84 Clause #90 (by clausification #[88]): ∀ (a : Iota), Eq (∀ (B : Iota), Or (Or (msmaller a B) (Not (snail a))) (Not (bird B))) True % 6.63/6.84 Clause #91 (by clausification #[90]): ∀ (a a_1 : Iota), Eq (Or (Or (msmaller a a_1) (Not (snail a))) (Not (bird a_1))) True % 6.63/6.88 Clause #92 (by clausification #[91]): ∀ (a a_1 : Iota), Or (Eq (Or (msmaller a a_1) (Not (snail a))) True) (Eq (Not (bird a_1)) True) % 6.63/6.88 Clause #93 (by clausification #[92]): ∀ (a a_1 : Iota), Or (Eq (Not (bird a)) True) (Or (Eq (msmaller a_1 a) True) (Eq (Not (snail a_1)) True)) % 6.63/6.88 Clause #94 (by clausification #[93]): ∀ (a a_1 : Iota), Or (Eq (msmaller a a_1) True) (Or (Eq (Not (snail a)) True) (Eq (bird a_1) False)) % 6.63/6.88 Clause #95 (by clausification #[94]): ∀ (a a_1 : Iota), Or (Eq (msmaller a a_1) True) (Or (Eq (bird a_1) False) (Eq (snail a) False)) % 6.63/6.88 Clause #97 (by clausification #[89]): Eq % 6.63/6.88 (And % 6.63/6.88 (And % 6.63/6.88 (And % 6.63/6.88 (And % 6.63/6.88 (And % 6.63/6.88 (And % 6.63/6.88 (And % 6.63/6.88 (And % 6.63/6.88 (And % 6.63/6.88 (And % 6.63/6.88 (And % 6.63/6.88 (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 6.63/6.88 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 6.63/6.88 (∀ (X : Iota), Or (animal X) (Not (caterpillar X)))) % 6.63/6.88 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 6.63/6.88 (wolf a_wolf)) % 6.63/6.88 (fox a_fox)) % 6.63/6.88 (bird a_bird)) % 6.63/6.88 (caterpillar a_caterpillar)) % 6.63/6.88 (snail a_snail)) % 6.63/6.88 (grain a_grain)) % 6.63/6.88 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 6.63/6.88 (∀ (A P S O : Iota), % 6.63/6.88 Or % 6.63/6.88 (Or % 6.63/6.88 (Or (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) (Not (animal S))) % 6.63/6.88 (Not (plant O))) % 6.63/6.88 (Not (msmaller S A))) % 6.63/6.88 (Not (eats S O)))) % 6.63/6.88 True % 6.63/6.88 Clause #104 (by clausification #[97]): Eq % 6.63/6.88 (∀ (A P S O : Iota), % 6.63/6.88 Or % 6.63/6.88 (Or % 6.63/6.88 (Or (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) (Not (animal S))) (Not (plant O))) % 6.63/6.88 (Not (msmaller S A))) % 6.63/6.88 (Not (eats S O))) % 6.63/6.88 True % 6.63/6.88 Clause #105 (by clausification #[97]): Eq % 6.63/6.88 (And % 6.63/6.88 (And % 6.63/6.88 (And % 6.63/6.88 (And % 6.63/6.88 (And % 6.63/6.88 (And % 6.63/6.88 (And % 6.63/6.88 (And % 6.63/6.88 (And % 6.63/6.88 (And (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 6.63/6.88 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 6.63/6.88 (∀ (X : Iota), Or (animal X) (Not (caterpillar X)))) % 6.63/6.88 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 6.63/6.88 (wolf a_wolf)) % 6.63/6.88 (fox a_fox)) % 6.63/6.88 (bird a_bird)) % 6.63/6.88 (caterpillar a_caterpillar)) % 6.63/6.88 (snail a_snail)) % 6.63/6.88 (grain a_grain)) % 6.63/6.88 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 6.63/6.88 True % 6.63/6.88 Clause #106 (by clausification #[104]): ∀ (a : Iota), % 6.63/6.88 Eq % 6.63/6.88 (∀ (P S O : Iota), % 6.63/6.88 Or % 6.63/6.88 (Or % 6.63/6.88 (Or (Or (Or (Or (Or (eats a P) (eats a S)) (Not (animal a))) (Not (plant P))) (Not (animal S))) % 6.63/6.88 (Not (plant O))) % 6.63/6.88 (Not (msmaller S a))) % 6.63/6.88 (Not (eats S O))) % 6.63/6.88 True % 6.63/6.88 Clause #107 (by clausification #[106]): ∀ (a a_1 : Iota), % 6.63/6.88 Eq % 6.63/6.88 (∀ (S O : Iota), % 6.63/6.88 Or % 6.63/6.88 (Or % 6.63/6.88 (Or (Or (Or (Or (Or (eats a a_1) (eats a S)) (Not (animal a))) (Not (plant a_1))) (Not (animal S))) % 6.63/6.88 (Not (plant O))) % 6.63/6.88 (Not (msmaller S a))) % 6.63/6.88 (Not (eats S O))) % 6.63/6.88 True % 6.63/6.88 Clause #108 (by clausification #[107]): ∀ (a a_1 a_2 : Iota), % 6.63/6.88 Eq % 6.63/6.88 (∀ (O : Iota), % 6.63/6.88 Or % 6.63/6.88 (Or % 6.63/6.88 (Or (Or (Or (Or (Or (eats a a_1) (eats a a_2)) (Not (animal a))) (Not (plant a_1))) (Not (animal a_2))) % 6.63/6.88 (Not (plant O))) % 6.63/6.88 (Not (msmaller a_2 a))) % 6.63/6.88 (Not (eats a_2 O))) % 6.63/6.88 True % 6.63/6.88 Clause #109 (by clausification #[108]): ∀ (a a_1 a_2 a_3 : Iota), % 6.63/6.88 Eq % 6.63/6.88 (Or % 6.63/6.88 (Or % 6.63/6.88 (Or (Or (Or (Or (Or (eats a a_1) (eats a a_2)) (Not (animal a))) (Not (plant a_1))) (Not (animal a_2))) % 6.63/6.88 (Not (plant a_3))) % 6.63/6.88 (Not (msmaller a_2 a))) % 6.63/6.88 (Not (eats a_2 a_3))) % 6.63/6.88 True % 6.63/6.88 Clause #110 (by clausification #[109]): ∀ (a a_1 a_2 a_3 : Iota), % 6.63/6.88 Or % 6.63/6.88 (Eq % 6.63/6.88 (Or % 6.63/6.88 (Or (Or (Or (Or (Or (eats a a_1) (eats a a_2)) (Not (animal a))) (Not (plant a_1))) (Not (animal a_2))) % 6.75/6.94 (Not (plant a_3))) % 6.75/6.94 (Not (msmaller a_2 a))) % 6.75/6.94 True) % 6.75/6.94 (Eq (Not (eats a_2 a_3)) True) % 6.75/6.94 Clause #111 (by clausification #[110]): ∀ (a a_1 a_2 a_3 : Iota), % 6.75/6.94 Or (Eq (Not (eats a a_1)) True) % 6.75/6.94 (Or % 6.75/6.94 (Eq % 6.75/6.94 (Or (Or (Or (Or (Or (eats a_2 a_3) (eats a_2 a)) (Not (animal a_2))) (Not (plant a_3))) (Not (animal a))) % 6.75/6.94 (Not (plant a_1))) % 6.75/6.94 True) % 6.75/6.94 (Eq (Not (msmaller a a_2)) True)) % 6.75/6.94 Clause #112 (by clausification #[111]): ∀ (a a_1 a_2 a_3 : Iota), % 6.75/6.94 Or % 6.75/6.94 (Eq % 6.75/6.94 (Or (Or (Or (Or (Or (eats a a_1) (eats a a_2)) (Not (animal a))) (Not (plant a_1))) (Not (animal a_2))) % 6.75/6.94 (Not (plant a_3))) % 6.75/6.94 True) % 6.75/6.94 (Or (Eq (Not (msmaller a_2 a)) True) (Eq (eats a_2 a_3) False)) % 6.75/6.94 Clause #113 (by clausification #[112]): ∀ (a a_1 a_2 a_3 : Iota), % 6.75/6.94 Or (Eq (Not (msmaller a a_1)) True) % 6.75/6.94 (Or (Eq (eats a a_2) False) % 6.75/6.94 (Or % 6.75/6.94 (Eq (Or (Or (Or (Or (eats a_1 a_3) (eats a_1 a)) (Not (animal a_1))) (Not (plant a_3))) (Not (animal a))) True) % 6.75/6.94 (Eq (Not (plant a_2)) True))) % 6.75/6.94 Clause #114 (by clausification #[113]): ∀ (a a_1 a_2 a_3 : Iota), % 6.75/6.94 Or (Eq (eats a a_1) False) % 6.75/6.94 (Or (Eq (Or (Or (Or (Or (eats a_2 a_3) (eats a_2 a)) (Not (animal a_2))) (Not (plant a_3))) (Not (animal a))) True) % 6.75/6.94 (Or (Eq (Not (plant a_1)) True) (Eq (msmaller a a_2) False))) % 6.75/6.94 Clause #115 (by clausification #[114]): ∀ (a a_1 a_2 a_3 : Iota), % 6.75/6.94 Or (Eq (eats a a_1) False) % 6.75/6.94 (Or (Eq (Not (plant a_1)) True) % 6.75/6.94 (Or (Eq (msmaller a a_2) False) % 6.75/6.94 (Or (Eq (Or (Or (Or (eats a_2 a_3) (eats a_2 a)) (Not (animal a_2))) (Not (plant a_3))) True) % 6.75/6.94 (Eq (Not (animal a)) True)))) % 6.75/6.94 Clause #116 (by clausification #[115]): ∀ (a a_1 a_2 a_3 : Iota), % 6.75/6.94 Or (Eq (eats a a_1) False) % 6.75/6.94 (Or (Eq (msmaller a a_2) False) % 6.75/6.94 (Or (Eq (Or (Or (Or (eats a_2 a_3) (eats a_2 a)) (Not (animal a_2))) (Not (plant a_3))) True) % 6.75/6.94 (Or (Eq (Not (animal a)) True) (Eq (plant a_1) False)))) % 6.75/6.94 Clause #117 (by clausification #[116]): ∀ (a a_1 a_2 a_3 : Iota), % 6.75/6.94 Or (Eq (eats a a_1) False) % 6.75/6.94 (Or (Eq (msmaller a a_2) False) % 6.75/6.94 (Or (Eq (Not (animal a)) True) % 6.75/6.94 (Or (Eq (plant a_1) False) % 6.75/6.94 (Or (Eq (Or (Or (eats a_2 a_3) (eats a_2 a)) (Not (animal a_2))) True) (Eq (Not (plant a_3)) True))))) % 6.75/6.94 Clause #118 (by clausification #[117]): ∀ (a a_1 a_2 a_3 : Iota), % 6.75/6.94 Or (Eq (eats a a_1) False) % 6.75/6.94 (Or (Eq (msmaller a a_2) False) % 6.75/6.94 (Or (Eq (plant a_1) False) % 6.75/6.94 (Or (Eq (Or (Or (eats a_2 a_3) (eats a_2 a)) (Not (animal a_2))) True) % 6.75/6.94 (Or (Eq (Not (plant a_3)) True) (Eq (animal a) False))))) % 6.75/6.94 Clause #119 (by clausification #[118]): ∀ (a a_1 a_2 a_3 : Iota), % 6.75/6.94 Or (Eq (eats a a_1) False) % 6.75/6.94 (Or (Eq (msmaller a a_2) False) % 6.75/6.94 (Or (Eq (plant a_1) False) % 6.75/6.94 (Or (Eq (Not (plant a_3)) True) % 6.75/6.94 (Or (Eq (animal a) False) (Or (Eq (Or (eats a_2 a_3) (eats a_2 a)) True) (Eq (Not (animal a_2)) True)))))) % 6.75/6.94 Clause #120 (by clausification #[119]): ∀ (a a_1 a_2 a_3 : Iota), % 6.75/6.94 Or (Eq (eats a a_1) False) % 6.75/6.94 (Or (Eq (msmaller a a_2) False) % 6.75/6.94 (Or (Eq (plant a_1) False) % 6.75/6.94 (Or (Eq (animal a) False) % 6.75/6.94 (Or (Eq (Or (eats a_2 a_3) (eats a_2 a)) True) (Or (Eq (Not (animal a_2)) True) (Eq (plant a_3) False)))))) % 6.75/6.94 Clause #121 (by clausification #[120]): ∀ (a a_1 a_2 a_3 : Iota), % 6.75/6.94 Or (Eq (eats a a_1) False) % 6.75/6.94 (Or (Eq (msmaller a a_2) False) % 6.75/6.94 (Or (Eq (plant a_1) False) % 6.75/6.94 (Or (Eq (animal a) False) % 6.75/6.94 (Or (Eq (Not (animal a_2)) True) % 6.75/6.94 (Or (Eq (plant a_3) False) (Or (Eq (eats a_2 a_3) True) (Eq (eats a_2 a) True))))))) % 6.75/6.94 Clause #122 (by clausification #[121]): ∀ (a a_1 a_2 a_3 : Iota), % 6.75/6.94 Or (Eq (eats a a_1) False) % 6.75/6.94 (Or (Eq (msmaller a a_2) False) % 6.75/6.94 (Or (Eq (plant a_1) False) % 6.75/6.94 (Or (Eq (animal a) False) % 6.75/6.94 (Or (Eq (plant a_3) False) % 6.75/6.94 (Or (Eq (eats a_2 a_3) True) (Or (Eq (eats a_2 a) True) (Eq (animal a_2) False))))))) % 6.75/6.94 Clause #123 (by clausification #[105]): Eq (∀ (X : Iota), Or (plant X) (Not (grain X))) True % 6.75/6.94 Clause #124 (by clausification #[105]): Eq % 6.75/6.94 (And % 6.75/6.98 (And % 6.75/6.98 (And % 6.75/6.98 (And % 6.75/6.98 (And % 6.75/6.98 (And % 6.75/6.98 (And % 6.75/6.98 (And % 6.75/6.98 (And (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 6.75/6.98 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 6.75/6.98 (∀ (X : Iota), Or (animal X) (Not (caterpillar X)))) % 6.75/6.98 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 6.75/6.98 (wolf a_wolf)) % 6.75/6.98 (fox a_fox)) % 6.75/6.98 (bird a_bird)) % 6.75/6.98 (caterpillar a_caterpillar)) % 6.75/6.98 (snail a_snail)) % 6.75/6.98 (grain a_grain)) % 6.75/6.98 True % 6.75/6.98 Clause #125 (by clausification #[123]): ∀ (a : Iota), Eq (Or (plant a) (Not (grain a))) True % 6.75/6.98 Clause #126 (by clausification #[125]): ∀ (a : Iota), Or (Eq (plant a) True) (Eq (Not (grain a)) True) % 6.75/6.98 Clause #127 (by clausification #[126]): ∀ (a : Iota), Or (Eq (plant a) True) (Eq (grain a) False) % 6.75/6.98 Clause #128 (by clausification #[124]): Eq (grain a_grain) True % 6.75/6.98 Clause #129 (by clausification #[124]): Eq % 6.75/6.98 (And % 6.75/6.98 (And % 6.75/6.98 (And % 6.75/6.98 (And % 6.75/6.98 (And % 6.75/6.98 (And % 6.75/6.98 (And % 6.75/6.98 (And (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 6.75/6.98 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 6.75/6.98 (∀ (X : Iota), Or (animal X) (Not (caterpillar X)))) % 6.75/6.98 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 6.75/6.98 (wolf a_wolf)) % 6.75/6.98 (fox a_fox)) % 6.75/6.98 (bird a_bird)) % 6.75/6.98 (caterpillar a_caterpillar)) % 6.75/6.98 (snail a_snail)) % 6.75/6.98 True % 6.75/6.98 Clause #130 (by superposition #[128, 127]): Or (Eq (plant a_grain) True) (Eq True False) % 6.75/6.98 Clause #131 (by clausification #[130]): Eq (plant a_grain) True % 6.75/6.98 Clause #132 (by clausification #[129]): Eq (snail a_snail) True % 6.75/6.98 Clause #133 (by clausification #[129]): Eq % 6.75/6.98 (And % 6.75/6.98 (And % 6.75/6.98 (And % 6.75/6.98 (And % 6.75/6.98 (And % 6.75/6.98 (And % 6.75/6.98 (And (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 6.75/6.98 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 6.75/6.98 (∀ (X : Iota), Or (animal X) (Not (caterpillar X)))) % 6.75/6.98 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 6.75/6.98 (wolf a_wolf)) % 6.75/6.98 (fox a_fox)) % 6.75/6.98 (bird a_bird)) % 6.75/6.98 (caterpillar a_caterpillar)) % 6.75/6.98 True % 6.75/6.98 Clause #134 (by superposition #[132, 21]): Or (Eq (eats a_snail (sf a_snail)) True) (Eq True False) % 6.75/6.98 Clause #135 (by superposition #[132, 26]): Or (Eq (plant (sf a_snail)) True) (Eq True False) % 6.75/6.98 Clause #136 (by clausification #[135]): Eq (plant (sf a_snail)) True % 6.75/6.98 Clause #137 (by clausification #[134]): Eq (eats a_snail (sf a_snail)) True % 6.75/6.98 Clause #142 (by superposition #[137, 122]): ∀ (a a_1 : Iota), % 6.75/6.98 Or (Eq True False) % 6.75/6.98 (Or (Eq (msmaller a_snail a) False) % 6.75/6.98 (Or (Eq (plant (sf a_snail)) False) % 6.75/6.98 (Or (Eq (animal a_snail) False) % 6.75/6.98 (Or (Eq (plant a_1) False) % 6.75/6.98 (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_snail) True) (Eq (animal a) False))))))) % 6.75/6.98 Clause #147 (by clausification #[133]): Eq % 6.75/6.98 (And % 6.75/6.98 (And % 6.75/6.98 (And % 6.75/6.98 (And % 6.75/6.98 (And % 6.75/6.98 (And (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 6.75/6.98 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 6.75/6.98 (∀ (X : Iota), Or (animal X) (Not (caterpillar X)))) % 6.75/6.98 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 6.75/6.98 (wolf a_wolf)) % 6.75/6.98 (fox a_fox)) % 6.75/6.98 (bird a_bird)) % 6.75/6.98 True % 6.75/6.98 Clause #164 (by clausification #[142]): ∀ (a a_1 : Iota), % 6.75/6.98 Or (Eq (msmaller a_snail a) False) % 6.75/6.98 (Or (Eq (plant (sf a_snail)) False) % 6.75/6.98 (Or (Eq (animal a_snail) False) % 6.75/6.98 (Or (Eq (plant a_1) False) (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_snail) True) (Eq (animal a) False)))))) % 6.75/6.98 Clause #165 (by forward demodulation #[164, 136]): ∀ (a a_1 : Iota), % 6.75/6.98 Or (Eq (msmaller a_snail a) False) % 6.75/6.98 (Or (Eq True False) % 6.75/6.98 (Or (Eq (animal a_snail) False) % 6.75/6.98 (Or (Eq (plant a_1) False) (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_snail) True) (Eq (animal a) False)))))) % 6.75/6.98 Clause #166 (by clausification #[165]): ∀ (a a_1 : Iota), % 6.84/7.03 Or (Eq (msmaller a_snail a) False) % 6.84/7.03 (Or (Eq (animal a_snail) False) % 6.84/7.03 (Or (Eq (plant a_1) False) (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_snail) True) (Eq (animal a) False))))) % 6.84/7.03 Clause #168 (by clausification #[147]): Eq (bird a_bird) True % 6.84/7.03 Clause #169 (by clausification #[147]): Eq % 6.84/7.03 (And % 6.84/7.03 (And % 6.84/7.03 (And % 6.84/7.03 (And % 6.84/7.03 (And (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 6.84/7.03 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 6.84/7.03 (∀ (X : Iota), Or (animal X) (Not (caterpillar X)))) % 6.84/7.03 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 6.84/7.03 (wolf a_wolf)) % 6.84/7.03 (fox a_fox)) % 6.84/7.03 True % 6.84/7.03 Clause #170 (by superposition #[168, 95]): ∀ (a : Iota), Or (Eq (msmaller a a_bird) True) (Or (Eq True False) (Eq (snail a) False)) % 6.84/7.03 Clause #173 (by clausification #[169]): Eq (fox a_fox) True % 6.84/7.03 Clause #174 (by clausification #[169]): Eq % 6.84/7.03 (And % 6.84/7.03 (And % 6.84/7.03 (And % 6.84/7.03 (And (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 6.84/7.03 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 6.84/7.03 (∀ (X : Iota), Or (animal X) (Not (caterpillar X)))) % 6.84/7.03 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 6.84/7.03 (wolf a_wolf)) % 6.84/7.03 True % 6.84/7.03 Clause #175 (by superposition #[173, 87]): ∀ (a : Iota), Or (Eq (msmaller a a_fox) True) (Or (Eq True False) (Eq (bird a) False)) % 6.84/7.03 Clause #188 (by clausification #[175]): ∀ (a : Iota), Or (Eq (msmaller a a_fox) True) (Eq (bird a) False) % 6.84/7.03 Clause #189 (by superposition #[188, 168]): Or (Eq (msmaller a_bird a_fox) True) (Eq False True) % 6.84/7.03 Clause #190 (by clausification #[170]): ∀ (a : Iota), Or (Eq (msmaller a a_bird) True) (Eq (snail a) False) % 6.84/7.03 Clause #191 (by superposition #[190, 132]): Or (Eq (msmaller a_snail a_bird) True) (Eq False True) % 6.84/7.03 Clause #192 (by clausification #[191]): Eq (msmaller a_snail a_bird) True % 6.84/7.03 Clause #193 (by superposition #[192, 166]): ∀ (a : Iota), % 6.84/7.03 Or (Eq True False) % 6.84/7.03 (Or (Eq (animal a_snail) False) % 6.84/7.03 (Or (Eq (plant a) False) % 6.84/7.03 (Or (Eq (eats a_bird a) True) (Or (Eq (eats a_bird a_snail) True) (Eq (animal a_bird) False))))) % 6.84/7.03 Clause #194 (by clausification #[189]): Eq (msmaller a_bird a_fox) True % 6.84/7.03 Clause #200 (by clausification #[174]): Eq (wolf a_wolf) True % 6.84/7.03 Clause #201 (by clausification #[174]): Eq % 6.84/7.03 (And % 6.84/7.03 (And % 6.84/7.03 (And (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 6.84/7.03 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 6.84/7.03 (∀ (X : Iota), Or (animal X) (Not (caterpillar X)))) % 6.84/7.03 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 6.84/7.03 True % 6.84/7.03 Clause #202 (by superposition #[200, 79]): ∀ (a : Iota), Or (Eq (msmaller a a_wolf) True) (Or (Eq True False) (Eq (fox a) False)) % 6.84/7.03 Clause #203 (by clausification #[202]): ∀ (a : Iota), Or (Eq (msmaller a a_wolf) True) (Eq (fox a) False) % 6.84/7.03 Clause #204 (by superposition #[203, 173]): Or (Eq (msmaller a_fox a_wolf) True) (Eq False True) % 6.84/7.03 Clause #205 (by clausification #[204]): Eq (msmaller a_fox a_wolf) True % 6.84/7.03 Clause #207 (by clausification #[193]): ∀ (a : Iota), % 6.84/7.03 Or (Eq (animal a_snail) False) % 6.84/7.03 (Or (Eq (plant a) False) % 6.84/7.03 (Or (Eq (eats a_bird a) True) (Or (Eq (eats a_bird a_snail) True) (Eq (animal a_bird) False)))) % 6.84/7.03 Clause #213 (by clausification #[201]): Eq (∀ (X : Iota), Or (animal X) (Not (snail X))) True % 6.84/7.03 Clause #214 (by clausification #[201]): Eq % 6.84/7.03 (And % 6.84/7.03 (And (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 6.84/7.03 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 6.84/7.03 (∀ (X : Iota), Or (animal X) (Not (caterpillar X)))) % 6.84/7.03 True % 6.84/7.03 Clause #215 (by clausification #[213]): ∀ (a : Iota), Eq (Or (animal a) (Not (snail a))) True % 6.84/7.03 Clause #216 (by clausification #[215]): ∀ (a : Iota), Or (Eq (animal a) True) (Eq (Not (snail a)) True) % 6.84/7.03 Clause #217 (by clausification #[216]): ∀ (a : Iota), Or (Eq (animal a) True) (Eq (snail a) False) % 6.84/7.03 Clause #218 (by superposition #[217, 132]): Or (Eq (animal a_snail) True) (Eq False True) % 6.84/7.03 Clause #219 (by clausification #[218]): Eq (animal a_snail) True % 6.84/7.03 Clause #222 (by backward demodulation #[219, 207]): ∀ (a : Iota), % 6.84/7.08 Or (Eq True False) % 6.84/7.08 (Or (Eq (plant a) False) % 6.84/7.08 (Or (Eq (eats a_bird a) True) (Or (Eq (eats a_bird a_snail) True) (Eq (animal a_bird) False)))) % 6.84/7.08 Clause #224 (by clausification #[222]): ∀ (a : Iota), % 6.84/7.08 Or (Eq (plant a) False) (Or (Eq (eats a_bird a) True) (Or (Eq (eats a_bird a_snail) True) (Eq (animal a_bird) False))) % 6.84/7.08 Clause #225 (by superposition #[224, 131]): Or (Eq (eats a_bird a_grain) True) (Or (Eq (eats a_bird a_snail) True) (Or (Eq (animal a_bird) False) (Eq False True))) % 6.84/7.08 Clause #229 (by clausification #[214]): Eq % 6.84/7.08 (And (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 6.84/7.08 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 6.84/7.08 True % 6.84/7.08 Clause #241 (by clausification #[225]): Or (Eq (eats a_bird a_grain) True) (Or (Eq (eats a_bird a_snail) True) (Eq (animal a_bird) False)) % 6.84/7.08 Clause #250 (by clausification #[229]): Eq (∀ (X : Iota), Or (animal X) (Not (bird X))) True % 6.84/7.08 Clause #251 (by clausification #[229]): Eq (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) (∀ (X : Iota), Or (animal X) (Not (fox X)))) True % 6.84/7.08 Clause #252 (by clausification #[250]): ∀ (a : Iota), Eq (Or (animal a) (Not (bird a))) True % 6.84/7.08 Clause #253 (by clausification #[252]): ∀ (a : Iota), Or (Eq (animal a) True) (Eq (Not (bird a)) True) % 6.84/7.08 Clause #254 (by clausification #[253]): ∀ (a : Iota), Or (Eq (animal a) True) (Eq (bird a) False) % 6.84/7.08 Clause #255 (by superposition #[254, 168]): Or (Eq (animal a_bird) True) (Eq False True) % 6.84/7.08 Clause #256 (by clausification #[255]): Eq (animal a_bird) True % 6.84/7.08 Clause #262 (by backward demodulation #[256, 241]): Or (Eq (eats a_bird a_grain) True) (Or (Eq (eats a_bird a_snail) True) (Eq True False)) % 6.84/7.08 Clause #266 (by clausification #[262]): Or (Eq (eats a_bird a_grain) True) (Eq (eats a_bird a_snail) True) % 6.84/7.08 Clause #267 (by superposition #[266, 16]): ∀ (a : Iota), % 6.84/7.08 Or (Eq (eats a_bird a_snail) True) % 6.84/7.08 (Or (Eq True False) % 6.84/7.08 (Or (Eq (eats a a_bird) False) % 6.84/7.08 (Or (Eq (grain a_grain) False) (Or (Eq (animal a) False) (Eq (animal a_bird) False))))) % 6.84/7.08 Clause #271 (by superposition #[266, 122]): ∀ (a a_1 : Iota), % 6.84/7.08 Or (Eq (eats a_bird a_snail) True) % 6.84/7.08 (Or (Eq True False) % 6.84/7.08 (Or (Eq (msmaller a_bird a) False) % 6.84/7.08 (Or (Eq (plant a_grain) False) % 6.84/7.08 (Or (Eq (animal a_bird) False) % 6.84/7.08 (Or (Eq (plant a_1) False) % 6.84/7.08 (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_bird) True) (Eq (animal a) False)))))))) % 6.84/7.08 Clause #284 (by clausification #[251]): Eq (∀ (X : Iota), Or (animal X) (Not (fox X))) True % 6.84/7.08 Clause #285 (by clausification #[251]): Eq (∀ (X : Iota), Or (animal X) (Not (wolf X))) True % 6.84/7.08 Clause #286 (by clausification #[284]): ∀ (a : Iota), Eq (Or (animal a) (Not (fox a))) True % 6.84/7.08 Clause #287 (by clausification #[286]): ∀ (a : Iota), Or (Eq (animal a) True) (Eq (Not (fox a)) True) % 6.84/7.08 Clause #288 (by clausification #[287]): ∀ (a : Iota), Or (Eq (animal a) True) (Eq (fox a) False) % 6.84/7.08 Clause #289 (by superposition #[288, 173]): Or (Eq (animal a_fox) True) (Eq False True) % 6.84/7.08 Clause #290 (by clausification #[289]): Eq (animal a_fox) True % 6.84/7.08 Clause #291 (by clausification #[285]): ∀ (a : Iota), Eq (Or (animal a) (Not (wolf a))) True % 6.84/7.08 Clause #292 (by clausification #[291]): ∀ (a : Iota), Or (Eq (animal a) True) (Eq (Not (wolf a)) True) % 6.84/7.08 Clause #293 (by clausification #[292]): ∀ (a : Iota), Or (Eq (animal a) True) (Eq (wolf a) False) % 6.84/7.08 Clause #294 (by superposition #[293, 200]): Or (Eq (animal a_wolf) True) (Eq False True) % 6.84/7.08 Clause #295 (by clausification #[294]): Eq (animal a_wolf) True % 6.84/7.08 Clause #321 (by clausification #[267]): ∀ (a : Iota), % 6.84/7.08 Or (Eq (eats a_bird a_snail) True) % 6.84/7.08 (Or (Eq (eats a a_bird) False) % 6.84/7.08 (Or (Eq (grain a_grain) False) (Or (Eq (animal a) False) (Eq (animal a_bird) False)))) % 6.84/7.08 Clause #322 (by forward demodulation #[321, 128]): ∀ (a : Iota), % 6.84/7.08 Or (Eq (eats a_bird a_snail) True) % 6.84/7.08 (Or (Eq (eats a a_bird) False) (Or (Eq True False) (Or (Eq (animal a) False) (Eq (animal a_bird) False)))) % 6.84/7.08 Clause #323 (by clausification #[322]): ∀ (a : Iota), % 6.84/7.08 Or (Eq (eats a_bird a_snail) True) % 6.84/7.08 (Or (Eq (eats a a_bird) False) (Or (Eq (animal a) False) (Eq (animal a_bird) False))) % 6.94/7.12 Clause #324 (by forward demodulation #[323, 256]): ∀ (a : Iota), % 6.94/7.12 Or (Eq (eats a_bird a_snail) True) (Or (Eq (eats a a_bird) False) (Or (Eq (animal a) False) (Eq True False))) % 6.94/7.12 Clause #325 (by clausification #[324]): ∀ (a : Iota), Or (Eq (eats a_bird a_snail) True) (Or (Eq (eats a a_bird) False) (Eq (animal a) False)) % 6.94/7.12 Clause #334 (by clausification #[271]): ∀ (a a_1 : Iota), % 6.94/7.12 Or (Eq (eats a_bird a_snail) True) % 6.94/7.12 (Or (Eq (msmaller a_bird a) False) % 6.94/7.12 (Or (Eq (plant a_grain) False) % 6.94/7.12 (Or (Eq (animal a_bird) False) % 6.94/7.12 (Or (Eq (plant a_1) False) % 6.94/7.12 (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_bird) True) (Eq (animal a) False))))))) % 6.94/7.12 Clause #335 (by forward demodulation #[334, 131]): ∀ (a a_1 : Iota), % 6.94/7.12 Or (Eq (eats a_bird a_snail) True) % 6.94/7.12 (Or (Eq (msmaller a_bird a) False) % 6.94/7.12 (Or (Eq True False) % 6.94/7.12 (Or (Eq (animal a_bird) False) % 6.94/7.12 (Or (Eq (plant a_1) False) % 6.94/7.12 (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_bird) True) (Eq (animal a) False))))))) % 6.94/7.12 Clause #336 (by clausification #[335]): ∀ (a a_1 : Iota), % 6.94/7.12 Or (Eq (eats a_bird a_snail) True) % 6.94/7.12 (Or (Eq (msmaller a_bird a) False) % 6.94/7.12 (Or (Eq (animal a_bird) False) % 6.94/7.12 (Or (Eq (plant a_1) False) (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_bird) True) (Eq (animal a) False)))))) % 6.94/7.12 Clause #337 (by forward demodulation #[336, 256]): ∀ (a a_1 : Iota), % 6.94/7.12 Or (Eq (eats a_bird a_snail) True) % 6.94/7.12 (Or (Eq (msmaller a_bird a) False) % 6.94/7.12 (Or (Eq True False) % 6.94/7.12 (Or (Eq (plant a_1) False) (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_bird) True) (Eq (animal a) False)))))) % 6.94/7.12 Clause #338 (by clausification #[337]): ∀ (a a_1 : Iota), % 6.94/7.12 Or (Eq (eats a_bird a_snail) True) % 6.94/7.12 (Or (Eq (msmaller a_bird a) False) % 6.94/7.12 (Or (Eq (plant a_1) False) (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_bird) True) (Eq (animal a) False))))) % 6.94/7.12 Clause #339 (by superposition #[338, 194]): ∀ (a : Iota), % 6.94/7.12 Or (Eq (eats a_bird a_snail) True) % 6.94/7.12 (Or (Eq (plant a) False) % 6.94/7.12 (Or (Eq (eats a_fox a) True) (Or (Eq (eats a_fox a_bird) True) (Or (Eq (animal a_fox) False) (Eq False True))))) % 6.94/7.12 Clause #340 (by clausification #[339]): ∀ (a : Iota), % 6.94/7.12 Or (Eq (eats a_bird a_snail) True) % 6.94/7.12 (Or (Eq (plant a) False) (Or (Eq (eats a_fox a) True) (Or (Eq (eats a_fox a_bird) True) (Eq (animal a_fox) False)))) % 6.94/7.12 Clause #341 (by forward demodulation #[340, 290]): ∀ (a : Iota), % 6.94/7.12 Or (Eq (eats a_bird a_snail) True) % 6.94/7.12 (Or (Eq (plant a) False) (Or (Eq (eats a_fox a) True) (Or (Eq (eats a_fox a_bird) True) (Eq True False)))) % 6.94/7.12 Clause #342 (by clausification #[341]): ∀ (a : Iota), % 6.94/7.12 Or (Eq (eats a_bird a_snail) True) % 6.94/7.12 (Or (Eq (plant a) False) (Or (Eq (eats a_fox a) True) (Eq (eats a_fox a_bird) True))) % 6.94/7.12 Clause #343 (by superposition #[342, 131]): Or (Eq (eats a_bird a_snail) True) % 6.94/7.12 (Or (Eq (eats a_fox a_grain) True) (Or (Eq (eats a_fox a_bird) True) (Eq False True))) % 6.94/7.12 Clause #346 (by clausification #[343]): Or (Eq (eats a_bird a_snail) True) (Or (Eq (eats a_fox a_grain) True) (Eq (eats a_fox a_bird) True)) % 6.94/7.12 Clause #349 (by superposition #[346, 45]): Or (Eq (eats a_fox a_grain) True) % 6.94/7.12 (Or (Eq (eats a_fox a_bird) True) (Or (Eq True False) (Or (Eq (bird a_bird) False) (Eq (snail a_snail) False)))) % 6.94/7.12 Clause #369 (by clausification #[349]): Or (Eq (eats a_fox a_grain) True) % 6.94/7.12 (Or (Eq (eats a_fox a_bird) True) (Or (Eq (bird a_bird) False) (Eq (snail a_snail) False))) % 6.94/7.12 Clause #370 (by forward demodulation #[369, 168]): Or (Eq (eats a_fox a_grain) True) (Or (Eq (eats a_fox a_bird) True) (Or (Eq True False) (Eq (snail a_snail) False))) % 6.94/7.12 Clause #371 (by clausification #[370]): Or (Eq (eats a_fox a_grain) True) (Or (Eq (eats a_fox a_bird) True) (Eq (snail a_snail) False)) % 6.94/7.12 Clause #372 (by forward demodulation #[371, 132]): Or (Eq (eats a_fox a_grain) True) (Or (Eq (eats a_fox a_bird) True) (Eq True False)) % 6.94/7.12 Clause #373 (by clausification #[372]): Or (Eq (eats a_fox a_grain) True) (Eq (eats a_fox a_bird) True) % 6.94/7.12 Clause #378 (by superposition #[373, 122]): ∀ (a a_1 : Iota), % 6.94/7.12 Or (Eq (eats a_fox a_bird) True) % 6.94/7.17 (Or (Eq True False) % 6.94/7.17 (Or (Eq (msmaller a_fox a) False) % 6.94/7.17 (Or (Eq (plant a_grain) False) % 6.94/7.17 (Or (Eq (animal a_fox) False) % 6.94/7.17 (Or (Eq (plant a_1) False) % 6.94/7.17 (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_fox) True) (Eq (animal a) False)))))))) % 6.94/7.17 Clause #428 (by clausification #[378]): ∀ (a a_1 : Iota), % 6.94/7.17 Or (Eq (eats a_fox a_bird) True) % 6.94/7.17 (Or (Eq (msmaller a_fox a) False) % 6.94/7.17 (Or (Eq (plant a_grain) False) % 6.94/7.17 (Or (Eq (animal a_fox) False) % 6.94/7.17 (Or (Eq (plant a_1) False) (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_fox) True) (Eq (animal a) False))))))) % 6.94/7.17 Clause #429 (by forward demodulation #[428, 131]): ∀ (a a_1 : Iota), % 6.94/7.17 Or (Eq (eats a_fox a_bird) True) % 6.94/7.17 (Or (Eq (msmaller a_fox a) False) % 6.94/7.17 (Or (Eq True False) % 6.94/7.17 (Or (Eq (animal a_fox) False) % 6.94/7.17 (Or (Eq (plant a_1) False) (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_fox) True) (Eq (animal a) False))))))) % 6.94/7.17 Clause #430 (by clausification #[429]): ∀ (a a_1 : Iota), % 6.94/7.17 Or (Eq (eats a_fox a_bird) True) % 6.94/7.17 (Or (Eq (msmaller a_fox a) False) % 6.94/7.17 (Or (Eq (animal a_fox) False) % 6.94/7.17 (Or (Eq (plant a_1) False) (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_fox) True) (Eq (animal a) False)))))) % 6.94/7.17 Clause #431 (by forward demodulation #[430, 290]): ∀ (a a_1 : Iota), % 6.94/7.17 Or (Eq (eats a_fox a_bird) True) % 6.94/7.17 (Or (Eq (msmaller a_fox a) False) % 6.94/7.17 (Or (Eq True False) % 6.94/7.17 (Or (Eq (plant a_1) False) (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_fox) True) (Eq (animal a) False)))))) % 6.94/7.17 Clause #432 (by clausification #[431]): ∀ (a a_1 : Iota), % 6.94/7.17 Or (Eq (eats a_fox a_bird) True) % 6.94/7.17 (Or (Eq (msmaller a_fox a) False) % 6.94/7.17 (Or (Eq (plant a_1) False) (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_fox) True) (Eq (animal a) False))))) % 6.94/7.17 Clause #433 (by superposition #[432, 205]): ∀ (a : Iota), % 6.94/7.17 Or (Eq (eats a_fox a_bird) True) % 6.94/7.17 (Or (Eq (plant a) False) % 6.94/7.17 (Or (Eq (eats a_wolf a) True) (Or (Eq (eats a_wolf a_fox) True) (Or (Eq (animal a_wolf) False) (Eq False True))))) % 6.94/7.17 Clause #437 (by clausification #[433]): ∀ (a : Iota), % 6.94/7.17 Or (Eq (eats a_fox a_bird) True) % 6.94/7.17 (Or (Eq (plant a) False) % 6.94/7.17 (Or (Eq (eats a_wolf a) True) (Or (Eq (eats a_wolf a_fox) True) (Eq (animal a_wolf) False)))) % 6.94/7.17 Clause #438 (by forward demodulation #[437, 295]): ∀ (a : Iota), % 6.94/7.17 Or (Eq (eats a_fox a_bird) True) % 6.94/7.17 (Or (Eq (plant a) False) (Or (Eq (eats a_wolf a) True) (Or (Eq (eats a_wolf a_fox) True) (Eq True False)))) % 6.94/7.17 Clause #439 (by clausification #[438]): ∀ (a : Iota), % 6.94/7.17 Or (Eq (eats a_fox a_bird) True) % 6.94/7.17 (Or (Eq (plant a) False) (Or (Eq (eats a_wolf a) True) (Eq (eats a_wolf a_fox) True))) % 6.94/7.17 Clause #440 (by superposition #[439, 131]): Or (Eq (eats a_fox a_bird) True) (Or (Eq (eats a_wolf a_grain) True) (Or (Eq (eats a_wolf a_fox) True) (Eq False True))) % 6.94/7.17 Clause #443 (by clausification #[440]): Or (Eq (eats a_fox a_bird) True) (Or (Eq (eats a_wolf a_grain) True) (Eq (eats a_wolf a_fox) True)) % 6.94/7.17 Clause #445 (by superposition #[443, 325]): Or (Eq (eats a_wolf a_grain) True) % 6.94/7.17 (Or (Eq (eats a_wolf a_fox) True) (Or (Eq (eats a_bird a_snail) True) (Or (Eq True False) (Eq (animal a_fox) False)))) % 6.94/7.17 Clause #475 (by clausification #[445]): Or (Eq (eats a_wolf a_grain) True) % 6.94/7.17 (Or (Eq (eats a_wolf a_fox) True) (Or (Eq (eats a_bird a_snail) True) (Eq (animal a_fox) False))) % 6.94/7.17 Clause #476 (by forward demodulation #[475, 290]): Or (Eq (eats a_wolf a_grain) True) % 6.94/7.17 (Or (Eq (eats a_wolf a_fox) True) (Or (Eq (eats a_bird a_snail) True) (Eq True False))) % 6.94/7.17 Clause #477 (by clausification #[476]): Or (Eq (eats a_wolf a_grain) True) (Or (Eq (eats a_wolf a_fox) True) (Eq (eats a_bird a_snail) True)) % 6.94/7.17 Clause #480 (by superposition #[477, 45]): Or (Eq (eats a_wolf a_grain) True) % 6.94/7.17 (Or (Eq (eats a_wolf a_fox) True) (Or (Eq True False) (Or (Eq (bird a_bird) False) (Eq (snail a_snail) False)))) % 6.94/7.17 Clause #489 (by clausification #[480]): Or (Eq (eats a_wolf a_grain) True) % 6.94/7.17 (Or (Eq (eats a_wolf a_fox) True) (Or (Eq (bird a_bird) False) (Eq (snail a_snail) False))) % 6.94/7.17 Clause #490 (by forward demodulation #[489, 168]): Or (Eq (eats a_wolf a_grain) True) (Or (Eq (eats a_wolf a_fox) True) (Or (Eq True False) (Eq (snail a_snail) False))) % 6.94/7.19 Clause #491 (by clausification #[490]): Or (Eq (eats a_wolf a_grain) True) (Or (Eq (eats a_wolf a_fox) True) (Eq (snail a_snail) False)) % 6.94/7.19 Clause #492 (by forward demodulation #[491, 132]): Or (Eq (eats a_wolf a_grain) True) (Or (Eq (eats a_wolf a_fox) True) (Eq True False)) % 6.94/7.19 Clause #493 (by clausification #[492]): Or (Eq (eats a_wolf a_grain) True) (Eq (eats a_wolf a_fox) True) % 6.94/7.19 Clause #496 (by superposition #[493, 62]): Or (Eq (eats a_wolf a_fox) True) (Or (Eq True False) (Or (Eq (wolf a_wolf) False) (Eq (grain a_grain) False))) % 6.94/7.19 Clause #502 (by clausification #[496]): Or (Eq (eats a_wolf a_fox) True) (Or (Eq (wolf a_wolf) False) (Eq (grain a_grain) False)) % 6.94/7.19 Clause #503 (by forward demodulation #[502, 200]): Or (Eq (eats a_wolf a_fox) True) (Or (Eq True False) (Eq (grain a_grain) False)) % 6.94/7.19 Clause #504 (by clausification #[503]): Or (Eq (eats a_wolf a_fox) True) (Eq (grain a_grain) False) % 6.94/7.19 Clause #505 (by forward demodulation #[504, 128]): Or (Eq (eats a_wolf a_fox) True) (Eq True False) % 6.94/7.19 Clause #506 (by clausification #[505]): Eq (eats a_wolf a_fox) True % 6.94/7.19 Clause #515 (by superposition #[506, 71]): Or (Eq True False) (Or (Eq (wolf a_wolf) False) (Eq (fox a_fox) False)) % 6.94/7.19 Clause #518 (by clausification #[515]): Or (Eq (wolf a_wolf) False) (Eq (fox a_fox) False) % 6.94/7.19 Clause #519 (by forward demodulation #[518, 173]): Or (Eq (wolf a_wolf) False) (Eq True False) % 6.94/7.19 Clause #520 (by clausification #[519]): Eq (wolf a_wolf) False % 6.94/7.19 Clause #521 (by superposition #[520, 200]): Eq False True % 6.94/7.19 Clause #522 (by clausification #[521]): False % 6.94/7.19 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------