%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : PUZ094^5 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Oct 3 07:58:21 PM UTC 2025 % Result : Theorem 4.18s 4.36s % Output : Proof 4.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.07 % Problem : PUZ094^5 : TPTP v9.2.0. Released v4.0.0. % 0.04/0.08 % Command : duper %s % 0.09/0.27 % Computer : n006.cluster.edu % 0.09/0.27 % Model : x86_64 x86_64 % 0.09/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.27 % Memory : 8042.1875MB % 0.09/0.27 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.27 % CPULimit : 300 % 0.09/0.27 % WCLimit : 300 % 0.09/0.27 % DateTime : Thu Oct 2 20:50:38 EDT 2025 % 0.09/0.27 % CPUTime : % 4.18/4.36 SZS status Theorem for theBenchmark.p % 4.18/4.36 SZS output start Proof for theBenchmark.p % 4.18/4.36 Clause #0 (by assumption #[]): Eq % 4.18/4.36 (Not % 4.18/4.36 (Not % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) % 4.18/4.36 (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 4.18/4.36 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 4.18/4.36 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 4.18/4.36 (wolf a_wolf)) % 4.18/4.36 (fox a_fox)) % 4.18/4.36 (bird a_bird)) % 4.18/4.36 (snail a_snail)) % 4.18/4.36 (grain a_grain)) % 4.18/4.36 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 4.18/4.36 (∀ (A P S O : Iota), % 4.18/4.36 Or % 4.18/4.36 (Or % 4.18/4.36 (Or % 4.18/4.36 (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) % 4.18/4.36 (Not (animal S))) % 4.18/4.36 (Not (plant O))) % 4.18/4.36 (Not (msmaller S A))) % 4.18/4.36 (Not (eats S O)))) % 4.18/4.36 (∀ (S B : Iota), Or (Or (msmaller S B) (Not (snail S))) (Not (bird B)))) % 4.18/4.36 (∀ (B F : Iota), Or (Or (msmaller B F) (Not (bird B))) (Not (fox F)))) % 4.18/4.36 (∀ (F W : Iota), Or (Or (msmaller F W) (Not (fox F))) (Not (wolf W)))) % 4.18/4.36 (∀ (F W : Iota), Or (Or (Not (wolf W)) (Not (fox F))) (Not (eats W F)))) % 4.18/4.36 (∀ (W G : Iota), Or (Or (Not (wolf W)) (Not (grain G))) (Not (eats W G)))) % 4.18/4.36 (∀ (B S : Iota), Or (Or (Not (bird B)) (Not (snail S))) (Not (eats B S)))) % 4.18/4.36 (∀ (S : Iota), Or (plant (sf S)) (Not (snail S)))) % 4.18/4.36 (∀ (S : Iota), Or (eats S (sf S)) (Not (snail S)))) % 4.18/4.36 (∀ (A E G : Iota), % 4.18/4.36 Or (Or (Or (Or (Not (animal A)) (Not (animal E))) (Not (grain G))) (Not (eats A E))) (Not (eats E G)))))) % 4.18/4.36 True % 4.18/4.36 Clause #1 (by clausification #[0]): Eq % 4.18/4.36 (Not % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And % 4.18/4.36 (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) % 4.18/4.36 (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 4.18/4.36 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 4.18/4.36 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 4.18/4.36 (wolf a_wolf)) % 4.18/4.36 (fox a_fox)) % 4.18/4.36 (bird a_bird)) % 4.18/4.36 (snail a_snail)) % 4.18/4.36 (grain a_grain)) % 4.18/4.36 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 4.18/4.36 (∀ (A P S O : Iota), % 4.18/4.36 Or % 4.18/4.36 (Or % 4.18/4.36 (Or % 4.18/4.36 (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) % 4.18/4.36 (Not (animal S))) % 4.18/4.38 (Not (plant O))) % 4.18/4.38 (Not (msmaller S A))) % 4.18/4.38 (Not (eats S O)))) % 4.18/4.38 (∀ (S B : Iota), Or (Or (msmaller S B) (Not (snail S))) (Not (bird B)))) % 4.18/4.38 (∀ (B F : Iota), Or (Or (msmaller B F) (Not (bird B))) (Not (fox F)))) % 4.18/4.38 (∀ (F W : Iota), Or (Or (msmaller F W) (Not (fox F))) (Not (wolf W)))) % 4.18/4.38 (∀ (F W : Iota), Or (Or (Not (wolf W)) (Not (fox F))) (Not (eats W F)))) % 4.18/4.38 (∀ (W G : Iota), Or (Or (Not (wolf W)) (Not (grain G))) (Not (eats W G)))) % 4.18/4.38 (∀ (B S : Iota), Or (Or (Not (bird B)) (Not (snail S))) (Not (eats B S)))) % 4.18/4.38 (∀ (S : Iota), Or (plant (sf S)) (Not (snail S)))) % 4.18/4.38 (∀ (S : Iota), Or (eats S (sf S)) (Not (snail S)))) % 4.18/4.38 (∀ (A E G : Iota), % 4.18/4.38 Or (Or (Or (Or (Not (animal A)) (Not (animal E))) (Not (grain G))) (Not (eats A E))) (Not (eats E G))))) % 4.18/4.38 False % 4.18/4.38 Clause #2 (by clausification #[1]): Eq % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) % 4.18/4.38 (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 4.18/4.38 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 4.18/4.38 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 4.18/4.38 (wolf a_wolf)) % 4.18/4.38 (fox a_fox)) % 4.18/4.38 (bird a_bird)) % 4.18/4.38 (snail a_snail)) % 4.18/4.38 (grain a_grain)) % 4.18/4.38 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 4.18/4.38 (∀ (A P S O : Iota), % 4.18/4.38 Or % 4.18/4.38 (Or % 4.18/4.38 (Or % 4.18/4.38 (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) % 4.18/4.38 (Not (animal S))) % 4.18/4.38 (Not (plant O))) % 4.18/4.38 (Not (msmaller S A))) % 4.18/4.38 (Not (eats S O)))) % 4.18/4.38 (∀ (S B : Iota), Or (Or (msmaller S B) (Not (snail S))) (Not (bird B)))) % 4.18/4.38 (∀ (B F : Iota), Or (Or (msmaller B F) (Not (bird B))) (Not (fox F)))) % 4.18/4.38 (∀ (F W : Iota), Or (Or (msmaller F W) (Not (fox F))) (Not (wolf W)))) % 4.18/4.38 (∀ (F W : Iota), Or (Or (Not (wolf W)) (Not (fox F))) (Not (eats W F)))) % 4.18/4.38 (∀ (W G : Iota), Or (Or (Not (wolf W)) (Not (grain G))) (Not (eats W G)))) % 4.18/4.38 (∀ (B S : Iota), Or (Or (Not (bird B)) (Not (snail S))) (Not (eats B S)))) % 4.18/4.38 (∀ (S : Iota), Or (plant (sf S)) (Not (snail S)))) % 4.18/4.38 (∀ (S : Iota), Or (eats S (sf S)) (Not (snail S)))) % 4.18/4.38 (∀ (A E G : Iota), % 4.18/4.38 Or (Or (Or (Or (Not (animal A)) (Not (animal E))) (Not (grain G))) (Not (eats A E))) (Not (eats E G)))) % 4.18/4.38 True % 4.18/4.38 Clause #3 (by clausification #[2]): Eq % 4.18/4.38 (∀ (A E G : Iota), % 4.18/4.38 Or (Or (Or (Or (Not (animal A)) (Not (animal E))) (Not (grain G))) (Not (eats A E))) (Not (eats E G))) % 4.18/4.38 True % 4.18/4.38 Clause #4 (by clausification #[2]): Eq % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And % 4.18/4.38 (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) % 4.18/4.38 (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 4.18/4.40 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 4.18/4.40 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 4.18/4.40 (wolf a_wolf)) % 4.18/4.40 (fox a_fox)) % 4.18/4.40 (bird a_bird)) % 4.18/4.40 (snail a_snail)) % 4.18/4.40 (grain a_grain)) % 4.18/4.40 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 4.18/4.40 (∀ (A P S O : Iota), % 4.18/4.40 Or % 4.18/4.40 (Or % 4.18/4.40 (Or % 4.18/4.40 (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) (Not (animal S))) % 4.18/4.40 (Not (plant O))) % 4.18/4.40 (Not (msmaller S A))) % 4.18/4.40 (Not (eats S O)))) % 4.18/4.40 (∀ (S B : Iota), Or (Or (msmaller S B) (Not (snail S))) (Not (bird B)))) % 4.18/4.40 (∀ (B F : Iota), Or (Or (msmaller B F) (Not (bird B))) (Not (fox F)))) % 4.18/4.40 (∀ (F W : Iota), Or (Or (msmaller F W) (Not (fox F))) (Not (wolf W)))) % 4.18/4.40 (∀ (F W : Iota), Or (Or (Not (wolf W)) (Not (fox F))) (Not (eats W F)))) % 4.18/4.40 (∀ (W G : Iota), Or (Or (Not (wolf W)) (Not (grain G))) (Not (eats W G)))) % 4.18/4.40 (∀ (B S : Iota), Or (Or (Not (bird B)) (Not (snail S))) (Not (eats B S)))) % 4.18/4.40 (∀ (S : Iota), Or (plant (sf S)) (Not (snail S)))) % 4.18/4.40 (∀ (S : Iota), Or (eats S (sf S)) (Not (snail S)))) % 4.18/4.40 True % 4.18/4.40 Clause #5 (by clausification #[3]): ∀ (a : Iota), % 4.18/4.40 Eq % 4.18/4.40 (∀ (E G : Iota), % 4.18/4.40 Or (Or (Or (Or (Not (animal a)) (Not (animal E))) (Not (grain G))) (Not (eats a E))) (Not (eats E G))) % 4.18/4.40 True % 4.18/4.40 Clause #6 (by clausification #[5]): ∀ (a a_1 : Iota), % 4.18/4.40 Eq % 4.18/4.40 (∀ (G : Iota), % 4.18/4.40 Or (Or (Or (Or (Not (animal a)) (Not (animal a_1))) (Not (grain G))) (Not (eats a a_1))) (Not (eats a_1 G))) % 4.18/4.40 True % 4.18/4.40 Clause #7 (by clausification #[6]): ∀ (a a_1 a_2 : Iota), % 4.18/4.40 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))) % 4.18/4.40 True % 4.18/4.40 Clause #8 (by clausification #[7]): ∀ (a a_1 a_2 : Iota), % 4.18/4.40 Or (Eq (Or (Or (Or (Not (animal a)) (Not (animal a_1))) (Not (grain a_2))) (Not (eats a a_1))) True) % 4.18/4.40 (Eq (Not (eats a_1 a_2)) True) % 4.18/4.40 Clause #9 (by clausification #[8]): ∀ (a a_1 a_2 : Iota), % 4.18/4.40 Or (Eq (Not (eats a a_1)) True) % 4.18/4.40 (Or (Eq (Or (Or (Not (animal a_2)) (Not (animal a))) (Not (grain a_1))) True) (Eq (Not (eats a_2 a)) True)) % 4.18/4.40 Clause #10 (by clausification #[9]): ∀ (a a_1 a_2 : Iota), % 4.18/4.40 Or (Eq (Or (Or (Not (animal a)) (Not (animal a_1))) (Not (grain a_2))) True) % 4.18/4.40 (Or (Eq (Not (eats a a_1)) True) (Eq (eats a_1 a_2) False)) % 4.18/4.40 Clause #11 (by clausification #[10]): ∀ (a a_1 a_2 : Iota), % 4.18/4.40 Or (Eq (Not (eats a a_1)) True) % 4.18/4.40 (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))) % 4.18/4.40 Clause #12 (by clausification #[11]): ∀ (a a_1 a_2 : Iota), % 4.18/4.40 Or (Eq (eats a a_1) False) % 4.18/4.40 (Or (Eq (Or (Not (animal a_2)) (Not (animal a))) True) (Or (Eq (Not (grain a_1)) True) (Eq (eats a_2 a) False))) % 4.18/4.40 Clause #13 (by clausification #[12]): ∀ (a a_1 a_2 : Iota), % 4.18/4.40 Or (Eq (eats a a_1) False) % 4.18/4.40 (Or (Eq (Not (grain a_1)) True) % 4.18/4.40 (Or (Eq (eats a_2 a) False) (Or (Eq (Not (animal a_2)) True) (Eq (Not (animal a)) True)))) % 4.18/4.40 Clause #14 (by clausification #[13]): ∀ (a a_1 a_2 : Iota), % 4.18/4.40 Or (Eq (eats a a_1) False) % 4.18/4.40 (Or (Eq (eats a_2 a) False) % 4.18/4.40 (Or (Eq (Not (animal a_2)) True) (Or (Eq (Not (animal a)) True) (Eq (grain a_1) False)))) % 4.18/4.40 Clause #15 (by clausification #[14]): ∀ (a a_1 a_2 : Iota), % 4.18/4.40 Or (Eq (eats a a_1) False) % 4.18/4.40 (Or (Eq (eats a_2 a) False) (Or (Eq (Not (animal a)) True) (Or (Eq (grain a_1) False) (Eq (animal a_2) False)))) % 4.18/4.40 Clause #16 (by clausification #[15]): ∀ (a a_1 a_2 : Iota), % 4.18/4.40 Or (Eq (eats a a_1) False) % 4.18/4.40 (Or (Eq (eats a_2 a) False) (Or (Eq (grain a_1) False) (Or (Eq (animal a_2) False) (Eq (animal a) False)))) % 4.18/4.40 Clause #17 (by clausification #[4]): Eq (∀ (S : Iota), Or (eats S (sf S)) (Not (snail S))) True % 4.18/4.40 Clause #18 (by clausification #[4]): Eq % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) % 4.18/4.41 (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 4.18/4.41 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 4.18/4.41 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 4.18/4.41 (wolf a_wolf)) % 4.18/4.41 (fox a_fox)) % 4.18/4.41 (bird a_bird)) % 4.18/4.41 (snail a_snail)) % 4.18/4.41 (grain a_grain)) % 4.18/4.41 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 4.18/4.41 (∀ (A P S O : Iota), % 4.18/4.41 Or % 4.18/4.41 (Or % 4.18/4.41 (Or (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) (Not (animal S))) % 4.18/4.41 (Not (plant O))) % 4.18/4.41 (Not (msmaller S A))) % 4.18/4.41 (Not (eats S O)))) % 4.18/4.41 (∀ (S B : Iota), Or (Or (msmaller S B) (Not (snail S))) (Not (bird B)))) % 4.18/4.41 (∀ (B F : Iota), Or (Or (msmaller B F) (Not (bird B))) (Not (fox F)))) % 4.18/4.41 (∀ (F W : Iota), Or (Or (msmaller F W) (Not (fox F))) (Not (wolf W)))) % 4.18/4.41 (∀ (F W : Iota), Or (Or (Not (wolf W)) (Not (fox F))) (Not (eats W F)))) % 4.18/4.41 (∀ (W G : Iota), Or (Or (Not (wolf W)) (Not (grain G))) (Not (eats W G)))) % 4.18/4.41 (∀ (B S : Iota), Or (Or (Not (bird B)) (Not (snail S))) (Not (eats B S)))) % 4.18/4.41 (∀ (S : Iota), Or (plant (sf S)) (Not (snail S)))) % 4.18/4.41 True % 4.18/4.41 Clause #19 (by clausification #[17]): ∀ (a : Iota), Eq (Or (eats a (sf a)) (Not (snail a))) True % 4.18/4.41 Clause #20 (by clausification #[19]): ∀ (a : Iota), Or (Eq (eats a (sf a)) True) (Eq (Not (snail a)) True) % 4.18/4.41 Clause #21 (by clausification #[20]): ∀ (a : Iota), Or (Eq (eats a (sf a)) True) (Eq (snail a) False) % 4.18/4.41 Clause #22 (by clausification #[18]): Eq (∀ (S : Iota), Or (plant (sf S)) (Not (snail S))) True % 4.18/4.41 Clause #23 (by clausification #[18]): Eq % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And % 4.18/4.41 (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) % 4.18/4.41 (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 4.18/4.41 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 4.18/4.41 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 4.18/4.41 (wolf a_wolf)) % 4.18/4.41 (fox a_fox)) % 4.18/4.41 (bird a_bird)) % 4.18/4.41 (snail a_snail)) % 4.18/4.41 (grain a_grain)) % 4.18/4.41 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 4.18/4.41 (∀ (A P S O : Iota), % 4.18/4.41 Or % 4.18/4.41 (Or % 4.18/4.41 (Or (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) (Not (animal S))) % 4.18/4.41 (Not (plant O))) % 4.18/4.41 (Not (msmaller S A))) % 4.18/4.41 (Not (eats S O)))) % 4.18/4.41 (∀ (S B : Iota), Or (Or (msmaller S B) (Not (snail S))) (Not (bird B)))) % 4.18/4.41 (∀ (B F : Iota), Or (Or (msmaller B F) (Not (bird B))) (Not (fox F)))) % 4.18/4.41 (∀ (F W : Iota), Or (Or (msmaller F W) (Not (fox F))) (Not (wolf W)))) % 4.18/4.41 (∀ (F W : Iota), Or (Or (Not (wolf W)) (Not (fox F))) (Not (eats W F)))) % 4.18/4.41 (∀ (W G : Iota), Or (Or (Not (wolf W)) (Not (grain G))) (Not (eats W G)))) % 4.18/4.41 (∀ (B S : Iota), Or (Or (Not (bird B)) (Not (snail S))) (Not (eats B S)))) % 4.18/4.41 True % 4.26/4.43 Clause #24 (by clausification #[22]): ∀ (a : Iota), Eq (Or (plant (sf a)) (Not (snail a))) True % 4.26/4.43 Clause #25 (by clausification #[24]): ∀ (a : Iota), Or (Eq (plant (sf a)) True) (Eq (Not (snail a)) True) % 4.26/4.43 Clause #26 (by clausification #[25]): ∀ (a : Iota), Or (Eq (plant (sf a)) True) (Eq (snail a) False) % 4.26/4.43 Clause #27 (by clausification #[23]): Eq (∀ (B S : Iota), Or (Or (Not (bird B)) (Not (snail S))) (Not (eats B S))) True % 4.26/4.43 Clause #28 (by clausification #[23]): Eq % 4.26/4.43 (And % 4.26/4.43 (And % 4.26/4.43 (And % 4.26/4.43 (And % 4.26/4.43 (And % 4.26/4.43 (And % 4.26/4.43 (And % 4.26/4.43 (And % 4.26/4.43 (And % 4.26/4.43 (And % 4.26/4.43 (And % 4.26/4.43 (And % 4.26/4.43 (And % 4.26/4.43 (And % 4.26/4.43 (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) % 4.26/4.43 (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 4.26/4.43 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 4.26/4.43 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 4.26/4.44 (wolf a_wolf)) % 4.26/4.44 (fox a_fox)) % 4.26/4.44 (bird a_bird)) % 4.26/4.44 (snail a_snail)) % 4.26/4.44 (grain a_grain)) % 4.26/4.44 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 4.26/4.44 (∀ (A P S O : Iota), % 4.26/4.44 Or % 4.26/4.44 (Or % 4.26/4.44 (Or (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) (Not (animal S))) % 4.26/4.44 (Not (plant O))) % 4.26/4.44 (Not (msmaller S A))) % 4.26/4.44 (Not (eats S O)))) % 4.26/4.44 (∀ (S B : Iota), Or (Or (msmaller S B) (Not (snail S))) (Not (bird B)))) % 4.26/4.44 (∀ (B F : Iota), Or (Or (msmaller B F) (Not (bird B))) (Not (fox F)))) % 4.26/4.44 (∀ (F W : Iota), Or (Or (msmaller F W) (Not (fox F))) (Not (wolf W)))) % 4.26/4.44 (∀ (F W : Iota), Or (Or (Not (wolf W)) (Not (fox F))) (Not (eats W F)))) % 4.26/4.44 (∀ (W G : Iota), Or (Or (Not (wolf W)) (Not (grain G))) (Not (eats W G)))) % 4.26/4.44 True % 4.26/4.44 Clause #29 (by clausification #[27]): ∀ (a : Iota), Eq (∀ (S : Iota), Or (Or (Not (bird a)) (Not (snail S))) (Not (eats a S))) True % 4.26/4.44 Clause #30 (by clausification #[29]): ∀ (a a_1 : Iota), Eq (Or (Or (Not (bird a)) (Not (snail a_1))) (Not (eats a a_1))) True % 4.26/4.44 Clause #31 (by clausification #[30]): ∀ (a a_1 : Iota), Or (Eq (Or (Not (bird a)) (Not (snail a_1))) True) (Eq (Not (eats a a_1)) True) % 4.26/4.44 Clause #32 (by clausification #[31]): ∀ (a a_1 : Iota), Or (Eq (Not (eats a a_1)) True) (Or (Eq (Not (bird a)) True) (Eq (Not (snail a_1)) True)) % 4.26/4.44 Clause #33 (by clausification #[32]): ∀ (a a_1 : Iota), Or (Eq (Not (bird a)) True) (Or (Eq (Not (snail a_1)) True) (Eq (eats a a_1) False)) % 4.26/4.44 Clause #34 (by clausification #[33]): ∀ (a a_1 : Iota), Or (Eq (Not (snail a)) True) (Or (Eq (eats a_1 a) False) (Eq (bird a_1) False)) % 4.26/4.44 Clause #35 (by clausification #[34]): ∀ (a a_1 : Iota), Or (Eq (eats a a_1) False) (Or (Eq (bird a) False) (Eq (snail a_1) False)) % 4.26/4.44 Clause #36 (by clausification #[28]): Eq (∀ (W G : Iota), Or (Or (Not (wolf W)) (Not (grain G))) (Not (eats W G))) True % 4.26/4.44 Clause #37 (by clausification #[28]): Eq % 4.26/4.44 (And % 4.26/4.44 (And % 4.26/4.44 (And % 4.26/4.44 (And % 4.26/4.44 (And % 4.26/4.44 (And % 4.26/4.44 (And % 4.26/4.44 (And % 4.26/4.44 (And % 4.26/4.44 (And % 4.26/4.44 (And % 4.26/4.44 (And % 4.26/4.44 (And % 4.26/4.44 (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) % 4.26/4.44 (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 4.26/4.44 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 4.26/4.44 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 4.26/4.44 (wolf a_wolf)) % 4.26/4.44 (fox a_fox)) % 4.26/4.44 (bird a_bird)) % 4.26/4.44 (snail a_snail)) % 4.26/4.44 (grain a_grain)) % 4.26/4.44 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 4.26/4.44 (∀ (A P S O : Iota), % 4.26/4.44 Or % 4.26/4.44 (Or % 4.26/4.44 (Or (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) (Not (animal S))) % 4.26/4.46 (Not (plant O))) % 4.26/4.46 (Not (msmaller S A))) % 4.26/4.46 (Not (eats S O)))) % 4.26/4.46 (∀ (S B : Iota), Or (Or (msmaller S B) (Not (snail S))) (Not (bird B)))) % 4.26/4.46 (∀ (B F : Iota), Or (Or (msmaller B F) (Not (bird B))) (Not (fox F)))) % 4.26/4.46 (∀ (F W : Iota), Or (Or (msmaller F W) (Not (fox F))) (Not (wolf W)))) % 4.26/4.46 (∀ (F W : Iota), Or (Or (Not (wolf W)) (Not (fox F))) (Not (eats W F)))) % 4.26/4.46 True % 4.26/4.46 Clause #38 (by clausification #[36]): ∀ (a : Iota), Eq (∀ (G : Iota), Or (Or (Not (wolf a)) (Not (grain G))) (Not (eats a G))) True % 4.26/4.46 Clause #39 (by clausification #[38]): ∀ (a a_1 : Iota), Eq (Or (Or (Not (wolf a)) (Not (grain a_1))) (Not (eats a a_1))) True % 4.26/4.46 Clause #40 (by clausification #[39]): ∀ (a a_1 : Iota), Or (Eq (Or (Not (wolf a)) (Not (grain a_1))) True) (Eq (Not (eats a a_1)) True) % 4.26/4.46 Clause #41 (by clausification #[40]): ∀ (a a_1 : Iota), Or (Eq (Not (eats a a_1)) True) (Or (Eq (Not (wolf a)) True) (Eq (Not (grain a_1)) True)) % 4.26/4.46 Clause #42 (by clausification #[41]): ∀ (a a_1 : Iota), Or (Eq (Not (wolf a)) True) (Or (Eq (Not (grain a_1)) True) (Eq (eats a a_1) False)) % 4.26/4.46 Clause #43 (by clausification #[42]): ∀ (a a_1 : Iota), Or (Eq (Not (grain a)) True) (Or (Eq (eats a_1 a) False) (Eq (wolf a_1) False)) % 4.26/4.46 Clause #44 (by clausification #[43]): ∀ (a a_1 : Iota), Or (Eq (eats a a_1) False) (Or (Eq (wolf a) False) (Eq (grain a_1) False)) % 4.26/4.46 Clause #45 (by clausification #[37]): Eq (∀ (F W : Iota), Or (Or (Not (wolf W)) (Not (fox F))) (Not (eats W F))) True % 4.26/4.46 Clause #46 (by clausification #[37]): Eq % 4.26/4.46 (And % 4.26/4.46 (And % 4.26/4.46 (And % 4.26/4.46 (And % 4.26/4.46 (And % 4.26/4.46 (And % 4.26/4.46 (And % 4.26/4.46 (And % 4.26/4.46 (And % 4.26/4.46 (And % 4.26/4.46 (And % 4.26/4.46 (And % 4.26/4.46 (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 4.26/4.46 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 4.26/4.46 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 4.26/4.46 (wolf a_wolf)) % 4.26/4.46 (fox a_fox)) % 4.26/4.46 (bird a_bird)) % 4.26/4.46 (snail a_snail)) % 4.26/4.46 (grain a_grain)) % 4.26/4.46 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 4.26/4.46 (∀ (A P S O : Iota), % 4.26/4.46 Or % 4.26/4.46 (Or % 4.26/4.46 (Or (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) (Not (animal S))) % 4.26/4.46 (Not (plant O))) % 4.26/4.46 (Not (msmaller S A))) % 4.26/4.46 (Not (eats S O)))) % 4.26/4.46 (∀ (S B : Iota), Or (Or (msmaller S B) (Not (snail S))) (Not (bird B)))) % 4.26/4.46 (∀ (B F : Iota), Or (Or (msmaller B F) (Not (bird B))) (Not (fox F)))) % 4.26/4.46 (∀ (F W : Iota), Or (Or (msmaller F W) (Not (fox F))) (Not (wolf W)))) % 4.26/4.46 True % 4.26/4.46 Clause #47 (by clausification #[45]): ∀ (a : Iota), Eq (∀ (W : Iota), Or (Or (Not (wolf W)) (Not (fox a))) (Not (eats W a))) True % 4.26/4.46 Clause #48 (by clausification #[47]): ∀ (a a_1 : Iota), Eq (Or (Or (Not (wolf a)) (Not (fox a_1))) (Not (eats a a_1))) True % 4.26/4.46 Clause #49 (by clausification #[48]): ∀ (a a_1 : Iota), Or (Eq (Or (Not (wolf a)) (Not (fox a_1))) True) (Eq (Not (eats a a_1)) True) % 4.26/4.46 Clause #50 (by clausification #[49]): ∀ (a a_1 : Iota), Or (Eq (Not (eats a a_1)) True) (Or (Eq (Not (wolf a)) True) (Eq (Not (fox a_1)) True)) % 4.26/4.46 Clause #51 (by clausification #[50]): ∀ (a a_1 : Iota), Or (Eq (Not (wolf a)) True) (Or (Eq (Not (fox a_1)) True) (Eq (eats a a_1) False)) % 4.26/4.46 Clause #52 (by clausification #[51]): ∀ (a a_1 : Iota), Or (Eq (Not (fox a)) True) (Or (Eq (eats a_1 a) False) (Eq (wolf a_1) False)) % 4.26/4.46 Clause #53 (by clausification #[52]): ∀ (a a_1 : Iota), Or (Eq (eats a a_1) False) (Or (Eq (wolf a) False) (Eq (fox a_1) False)) % 4.26/4.46 Clause #54 (by clausification #[46]): Eq (∀ (F W : Iota), Or (Or (msmaller F W) (Not (fox F))) (Not (wolf W))) True % 4.26/4.46 Clause #55 (by clausification #[46]): Eq % 4.26/4.46 (And % 4.26/4.46 (And % 4.26/4.46 (And % 4.26/4.46 (And % 4.26/4.46 (And % 4.26/4.46 (And % 4.26/4.46 (And % 4.26/4.46 (And % 4.26/4.48 (And % 4.26/4.48 (And % 4.26/4.48 (And % 4.26/4.48 (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 4.26/4.48 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 4.26/4.48 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 4.26/4.48 (wolf a_wolf)) % 4.26/4.48 (fox a_fox)) % 4.26/4.48 (bird a_bird)) % 4.26/4.48 (snail a_snail)) % 4.26/4.48 (grain a_grain)) % 4.26/4.48 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 4.26/4.48 (∀ (A P S O : Iota), % 4.26/4.48 Or % 4.26/4.48 (Or % 4.26/4.48 (Or (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) (Not (animal S))) % 4.26/4.48 (Not (plant O))) % 4.26/4.48 (Not (msmaller S A))) % 4.26/4.48 (Not (eats S O)))) % 4.26/4.48 (∀ (S B : Iota), Or (Or (msmaller S B) (Not (snail S))) (Not (bird B)))) % 4.26/4.48 (∀ (B F : Iota), Or (Or (msmaller B F) (Not (bird B))) (Not (fox F)))) % 4.26/4.48 True % 4.26/4.48 Clause #56 (by clausification #[54]): ∀ (a : Iota), Eq (∀ (W : Iota), Or (Or (msmaller a W) (Not (fox a))) (Not (wolf W))) True % 4.26/4.48 Clause #57 (by clausification #[56]): ∀ (a a_1 : Iota), Eq (Or (Or (msmaller a a_1) (Not (fox a))) (Not (wolf a_1))) True % 4.26/4.48 Clause #58 (by clausification #[57]): ∀ (a a_1 : Iota), Or (Eq (Or (msmaller a a_1) (Not (fox a))) True) (Eq (Not (wolf a_1)) True) % 4.26/4.48 Clause #59 (by clausification #[58]): ∀ (a a_1 : Iota), Or (Eq (Not (wolf a)) True) (Or (Eq (msmaller a_1 a) True) (Eq (Not (fox a_1)) True)) % 4.26/4.48 Clause #60 (by clausification #[59]): ∀ (a a_1 : Iota), Or (Eq (msmaller a a_1) True) (Or (Eq (Not (fox a)) True) (Eq (wolf a_1) False)) % 4.26/4.48 Clause #61 (by clausification #[60]): ∀ (a a_1 : Iota), Or (Eq (msmaller a a_1) True) (Or (Eq (wolf a_1) False) (Eq (fox a) False)) % 4.26/4.48 Clause #62 (by clausification #[55]): Eq (∀ (B F : Iota), Or (Or (msmaller B F) (Not (bird B))) (Not (fox F))) True % 4.26/4.48 Clause #63 (by clausification #[55]): Eq % 4.26/4.48 (And % 4.26/4.48 (And % 4.26/4.48 (And % 4.26/4.48 (And % 4.26/4.48 (And % 4.26/4.48 (And % 4.26/4.48 (And % 4.26/4.48 (And % 4.26/4.48 (And % 4.26/4.48 (And (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 4.26/4.48 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 4.26/4.48 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 4.26/4.48 (wolf a_wolf)) % 4.26/4.48 (fox a_fox)) % 4.26/4.48 (bird a_bird)) % 4.26/4.48 (snail a_snail)) % 4.26/4.48 (grain a_grain)) % 4.26/4.48 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 4.26/4.48 (∀ (A P S O : Iota), % 4.26/4.48 Or % 4.26/4.48 (Or % 4.26/4.48 (Or (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) (Not (animal S))) % 4.26/4.48 (Not (plant O))) % 4.26/4.48 (Not (msmaller S A))) % 4.26/4.48 (Not (eats S O)))) % 4.26/4.48 (∀ (S B : Iota), Or (Or (msmaller S B) (Not (snail S))) (Not (bird B)))) % 4.26/4.48 True % 4.26/4.48 Clause #64 (by clausification #[62]): ∀ (a : Iota), Eq (∀ (F : Iota), Or (Or (msmaller a F) (Not (bird a))) (Not (fox F))) True % 4.26/4.48 Clause #65 (by clausification #[64]): ∀ (a a_1 : Iota), Eq (Or (Or (msmaller a a_1) (Not (bird a))) (Not (fox a_1))) True % 4.26/4.48 Clause #66 (by clausification #[65]): ∀ (a a_1 : Iota), Or (Eq (Or (msmaller a a_1) (Not (bird a))) True) (Eq (Not (fox a_1)) True) % 4.26/4.48 Clause #67 (by clausification #[66]): ∀ (a a_1 : Iota), Or (Eq (Not (fox a)) True) (Or (Eq (msmaller a_1 a) True) (Eq (Not (bird a_1)) True)) % 4.26/4.48 Clause #68 (by clausification #[67]): ∀ (a a_1 : Iota), Or (Eq (msmaller a a_1) True) (Or (Eq (Not (bird a)) True) (Eq (fox a_1) False)) % 4.26/4.48 Clause #69 (by clausification #[68]): ∀ (a a_1 : Iota), Or (Eq (msmaller a a_1) True) (Or (Eq (fox a_1) False) (Eq (bird a) False)) % 4.26/4.48 Clause #70 (by clausification #[63]): Eq (∀ (S B : Iota), Or (Or (msmaller S B) (Not (snail S))) (Not (bird B))) True % 4.26/4.48 Clause #71 (by clausification #[63]): Eq % 4.26/4.48 (And % 4.26/4.48 (And % 4.26/4.48 (And % 4.26/4.48 (And % 4.26/4.48 (And % 4.26/4.48 (And % 4.26/4.48 (And % 4.26/4.48 (And % 4.26/4.48 (And (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 4.33/4.50 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 4.33/4.50 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 4.33/4.50 (wolf a_wolf)) % 4.33/4.50 (fox a_fox)) % 4.33/4.50 (bird a_bird)) % 4.33/4.50 (snail a_snail)) % 4.33/4.50 (grain a_grain)) % 4.33/4.50 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 4.33/4.50 (∀ (A P S O : Iota), % 4.33/4.50 Or % 4.33/4.50 (Or % 4.33/4.50 (Or (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) (Not (animal S))) % 4.33/4.50 (Not (plant O))) % 4.33/4.50 (Not (msmaller S A))) % 4.33/4.50 (Not (eats S O)))) % 4.33/4.50 True % 4.33/4.50 Clause #72 (by clausification #[70]): ∀ (a : Iota), Eq (∀ (B : Iota), Or (Or (msmaller a B) (Not (snail a))) (Not (bird B))) True % 4.33/4.50 Clause #73 (by clausification #[72]): ∀ (a a_1 : Iota), Eq (Or (Or (msmaller a a_1) (Not (snail a))) (Not (bird a_1))) True % 4.33/4.50 Clause #74 (by clausification #[73]): ∀ (a a_1 : Iota), Or (Eq (Or (msmaller a a_1) (Not (snail a))) True) (Eq (Not (bird a_1)) True) % 4.33/4.50 Clause #75 (by clausification #[74]): ∀ (a a_1 : Iota), Or (Eq (Not (bird a)) True) (Or (Eq (msmaller a_1 a) True) (Eq (Not (snail a_1)) True)) % 4.33/4.50 Clause #76 (by clausification #[75]): ∀ (a a_1 : Iota), Or (Eq (msmaller a a_1) True) (Or (Eq (Not (snail a)) True) (Eq (bird a_1) False)) % 4.33/4.50 Clause #77 (by clausification #[76]): ∀ (a a_1 : Iota), Or (Eq (msmaller a a_1) True) (Or (Eq (bird a_1) False) (Eq (snail a) False)) % 4.33/4.50 Clause #78 (by clausification #[71]): Eq % 4.33/4.50 (∀ (A P S O : Iota), % 4.33/4.50 Or % 4.33/4.50 (Or % 4.33/4.50 (Or (Or (Or (Or (Or (eats A P) (eats A S)) (Not (animal A))) (Not (plant P))) (Not (animal S))) (Not (plant O))) % 4.33/4.50 (Not (msmaller S A))) % 4.33/4.50 (Not (eats S O))) % 4.33/4.50 True % 4.33/4.50 Clause #79 (by clausification #[71]): Eq % 4.33/4.50 (And % 4.33/4.50 (And % 4.33/4.50 (And % 4.33/4.50 (And % 4.33/4.50 (And % 4.33/4.50 (And % 4.33/4.50 (And % 4.33/4.50 (And (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 4.33/4.50 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 4.33/4.50 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 4.33/4.50 (wolf a_wolf)) % 4.33/4.50 (fox a_fox)) % 4.33/4.50 (bird a_bird)) % 4.33/4.50 (snail a_snail)) % 4.33/4.50 (grain a_grain)) % 4.33/4.50 (∀ (X : Iota), Or (plant X) (Not (grain X)))) % 4.33/4.50 True % 4.33/4.50 Clause #80 (by clausification #[78]): ∀ (a : Iota), % 4.33/4.50 Eq % 4.33/4.50 (∀ (P S O : Iota), % 4.33/4.50 Or % 4.33/4.50 (Or % 4.33/4.50 (Or (Or (Or (Or (Or (eats a P) (eats a S)) (Not (animal a))) (Not (plant P))) (Not (animal S))) % 4.33/4.50 (Not (plant O))) % 4.33/4.50 (Not (msmaller S a))) % 4.33/4.50 (Not (eats S O))) % 4.33/4.50 True % 4.33/4.50 Clause #81 (by clausification #[80]): ∀ (a a_1 : Iota), % 4.33/4.50 Eq % 4.33/4.50 (∀ (S O : Iota), % 4.33/4.50 Or % 4.33/4.50 (Or % 4.33/4.50 (Or (Or (Or (Or (Or (eats a a_1) (eats a S)) (Not (animal a))) (Not (plant a_1))) (Not (animal S))) % 4.33/4.50 (Not (plant O))) % 4.33/4.50 (Not (msmaller S a))) % 4.33/4.50 (Not (eats S O))) % 4.33/4.50 True % 4.33/4.50 Clause #82 (by clausification #[81]): ∀ (a a_1 a_2 : Iota), % 4.33/4.50 Eq % 4.33/4.50 (∀ (O : Iota), % 4.33/4.50 Or % 4.33/4.50 (Or % 4.33/4.50 (Or (Or (Or (Or (Or (eats a a_1) (eats a a_2)) (Not (animal a))) (Not (plant a_1))) (Not (animal a_2))) % 4.33/4.50 (Not (plant O))) % 4.33/4.50 (Not (msmaller a_2 a))) % 4.33/4.50 (Not (eats a_2 O))) % 4.33/4.50 True % 4.33/4.50 Clause #83 (by clausification #[82]): ∀ (a a_1 a_2 a_3 : Iota), % 4.33/4.50 Eq % 4.33/4.50 (Or % 4.33/4.50 (Or % 4.33/4.50 (Or (Or (Or (Or (Or (eats a a_1) (eats a a_2)) (Not (animal a))) (Not (plant a_1))) (Not (animal a_2))) % 4.33/4.50 (Not (plant a_3))) % 4.33/4.50 (Not (msmaller a_2 a))) % 4.33/4.50 (Not (eats a_2 a_3))) % 4.33/4.50 True % 4.33/4.50 Clause #84 (by clausification #[83]): ∀ (a a_1 a_2 a_3 : Iota), % 4.33/4.50 Or % 4.33/4.50 (Eq % 4.33/4.50 (Or % 4.33/4.50 (Or (Or (Or (Or (Or (eats a a_1) (eats a a_2)) (Not (animal a))) (Not (plant a_1))) (Not (animal a_2))) % 4.33/4.50 (Not (plant a_3))) % 4.33/4.50 (Not (msmaller a_2 a))) % 4.33/4.50 True) % 4.33/4.50 (Eq (Not (eats a_2 a_3)) True) % 4.33/4.50 Clause #85 (by clausification #[84]): ∀ (a a_1 a_2 a_3 : Iota), % 4.33/4.50 Or (Eq (Not (eats a a_1)) True) % 4.33/4.50 (Or % 4.33/4.50 (Eq % 4.33/4.50 (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))) % 4.33/4.50 (Not (plant a_1))) % 4.33/4.50 True) % 4.33/4.50 (Eq (Not (msmaller a a_2)) True)) % 4.33/4.52 Clause #86 (by clausification #[85]): ∀ (a a_1 a_2 a_3 : Iota), % 4.33/4.52 Or % 4.33/4.52 (Eq % 4.33/4.52 (Or (Or (Or (Or (Or (eats a a_1) (eats a a_2)) (Not (animal a))) (Not (plant a_1))) (Not (animal a_2))) % 4.33/4.52 (Not (plant a_3))) % 4.33/4.52 True) % 4.33/4.52 (Or (Eq (Not (msmaller a_2 a)) True) (Eq (eats a_2 a_3) False)) % 4.33/4.52 Clause #87 (by clausification #[86]): ∀ (a a_1 a_2 a_3 : Iota), % 4.33/4.52 Or (Eq (Not (msmaller a a_1)) True) % 4.33/4.52 (Or (Eq (eats a a_2) False) % 4.33/4.52 (Or % 4.33/4.52 (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) % 4.33/4.52 (Eq (Not (plant a_2)) True))) % 4.33/4.52 Clause #88 (by clausification #[87]): ∀ (a a_1 a_2 a_3 : Iota), % 4.33/4.52 Or (Eq (eats a a_1) False) % 4.33/4.52 (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) % 4.33/4.52 (Or (Eq (Not (plant a_1)) True) (Eq (msmaller a a_2) False))) % 4.33/4.52 Clause #89 (by clausification #[88]): ∀ (a a_1 a_2 a_3 : Iota), % 4.33/4.52 Or (Eq (eats a a_1) False) % 4.33/4.52 (Or (Eq (Not (plant a_1)) True) % 4.33/4.52 (Or (Eq (msmaller a a_2) False) % 4.33/4.52 (Or (Eq (Or (Or (Or (eats a_2 a_3) (eats a_2 a)) (Not (animal a_2))) (Not (plant a_3))) True) % 4.33/4.52 (Eq (Not (animal a)) True)))) % 4.33/4.52 Clause #90 (by clausification #[89]): ∀ (a a_1 a_2 a_3 : Iota), % 4.33/4.52 Or (Eq (eats a a_1) False) % 4.33/4.52 (Or (Eq (msmaller a a_2) False) % 4.33/4.52 (Or (Eq (Or (Or (Or (eats a_2 a_3) (eats a_2 a)) (Not (animal a_2))) (Not (plant a_3))) True) % 4.33/4.52 (Or (Eq (Not (animal a)) True) (Eq (plant a_1) False)))) % 4.33/4.52 Clause #91 (by clausification #[90]): ∀ (a a_1 a_2 a_3 : Iota), % 4.33/4.52 Or (Eq (eats a a_1) False) % 4.33/4.52 (Or (Eq (msmaller a a_2) False) % 4.33/4.52 (Or (Eq (Not (animal a)) True) % 4.33/4.52 (Or (Eq (plant a_1) False) % 4.33/4.52 (Or (Eq (Or (Or (eats a_2 a_3) (eats a_2 a)) (Not (animal a_2))) True) (Eq (Not (plant a_3)) True))))) % 4.33/4.52 Clause #92 (by clausification #[91]): ∀ (a a_1 a_2 a_3 : Iota), % 4.33/4.52 Or (Eq (eats a a_1) False) % 4.33/4.52 (Or (Eq (msmaller a a_2) False) % 4.33/4.52 (Or (Eq (plant a_1) False) % 4.33/4.52 (Or (Eq (Or (Or (eats a_2 a_3) (eats a_2 a)) (Not (animal a_2))) True) % 4.33/4.53 (Or (Eq (Not (plant a_3)) True) (Eq (animal a) False))))) % 4.33/4.53 Clause #93 (by clausification #[92]): ∀ (a a_1 a_2 a_3 : Iota), % 4.33/4.53 Or (Eq (eats a a_1) False) % 4.33/4.53 (Or (Eq (msmaller a a_2) False) % 4.33/4.53 (Or (Eq (plant a_1) False) % 4.33/4.53 (Or (Eq (Not (plant a_3)) True) % 4.33/4.53 (Or (Eq (animal a) False) (Or (Eq (Or (eats a_2 a_3) (eats a_2 a)) True) (Eq (Not (animal a_2)) True)))))) % 4.33/4.53 Clause #94 (by clausification #[93]): ∀ (a a_1 a_2 a_3 : Iota), % 4.33/4.53 Or (Eq (eats a a_1) False) % 4.33/4.53 (Or (Eq (msmaller a a_2) False) % 4.33/4.53 (Or (Eq (plant a_1) False) % 4.33/4.53 (Or (Eq (animal a) False) % 4.33/4.53 (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)))))) % 4.33/4.53 Clause #95 (by clausification #[94]): ∀ (a a_1 a_2 a_3 : Iota), % 4.33/4.53 Or (Eq (eats a a_1) False) % 4.33/4.53 (Or (Eq (msmaller a a_2) False) % 4.33/4.53 (Or (Eq (plant a_1) False) % 4.33/4.53 (Or (Eq (animal a) False) % 4.33/4.53 (Or (Eq (Not (animal a_2)) True) % 4.33/4.53 (Or (Eq (plant a_3) False) (Or (Eq (eats a_2 a_3) True) (Eq (eats a_2 a) True))))))) % 4.33/4.53 Clause #96 (by clausification #[95]): ∀ (a a_1 a_2 a_3 : Iota), % 4.33/4.53 Or (Eq (eats a a_1) False) % 4.33/4.53 (Or (Eq (msmaller a a_2) False) % 4.33/4.53 (Or (Eq (plant a_1) False) % 4.33/4.53 (Or (Eq (animal a) False) % 4.33/4.53 (Or (Eq (plant a_3) False) % 4.33/4.53 (Or (Eq (eats a_2 a_3) True) (Or (Eq (eats a_2 a) True) (Eq (animal a_2) False))))))) % 4.33/4.53 Clause #97 (by clausification #[79]): Eq (∀ (X : Iota), Or (plant X) (Not (grain X))) True % 4.33/4.53 Clause #98 (by clausification #[79]): Eq % 4.33/4.53 (And % 4.33/4.53 (And % 4.33/4.53 (And % 4.33/4.53 (And % 4.33/4.53 (And % 4.33/4.53 (And % 4.33/4.53 (And (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 4.33/4.53 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 4.33/4.53 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 4.33/4.53 (wolf a_wolf)) % 4.33/4.53 (fox a_fox)) % 4.33/4.53 (bird a_bird)) % 4.33/4.53 (snail a_snail)) % 4.33/4.53 (grain a_grain)) % 4.33/4.53 True % 4.33/4.53 Clause #99 (by clausification #[97]): ∀ (a : Iota), Eq (Or (plant a) (Not (grain a))) True % 4.33/4.55 Clause #100 (by clausification #[99]): ∀ (a : Iota), Or (Eq (plant a) True) (Eq (Not (grain a)) True) % 4.33/4.55 Clause #101 (by clausification #[100]): ∀ (a : Iota), Or (Eq (plant a) True) (Eq (grain a) False) % 4.33/4.55 Clause #102 (by clausification #[98]): Eq (grain a_grain) True % 4.33/4.55 Clause #103 (by clausification #[98]): Eq % 4.33/4.55 (And % 4.33/4.55 (And % 4.33/4.55 (And % 4.33/4.55 (And % 4.33/4.55 (And % 4.33/4.55 (And (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 4.33/4.55 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 4.33/4.55 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 4.33/4.55 (wolf a_wolf)) % 4.33/4.55 (fox a_fox)) % 4.33/4.55 (bird a_bird)) % 4.33/4.55 (snail a_snail)) % 4.33/4.55 True % 4.33/4.55 Clause #104 (by superposition #[102, 101]): Or (Eq (plant a_grain) True) (Eq True False) % 4.33/4.55 Clause #105 (by clausification #[104]): Eq (plant a_grain) True % 4.33/4.55 Clause #106 (by clausification #[103]): Eq (snail a_snail) True % 4.33/4.55 Clause #107 (by clausification #[103]): Eq % 4.33/4.55 (And % 4.33/4.55 (And % 4.33/4.55 (And % 4.33/4.55 (And % 4.33/4.55 (And (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 4.33/4.55 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 4.33/4.55 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 4.33/4.55 (wolf a_wolf)) % 4.33/4.55 (fox a_fox)) % 4.33/4.55 (bird a_bird)) % 4.33/4.55 True % 4.33/4.55 Clause #108 (by superposition #[106, 21]): Or (Eq (eats a_snail (sf a_snail)) True) (Eq True False) % 4.33/4.55 Clause #109 (by superposition #[106, 26]): Or (Eq (plant (sf a_snail)) True) (Eq True False) % 4.33/4.55 Clause #110 (by clausification #[109]): Eq (plant (sf a_snail)) True % 4.33/4.55 Clause #111 (by clausification #[108]): Eq (eats a_snail (sf a_snail)) True % 4.33/4.55 Clause #116 (by superposition #[111, 96]): ∀ (a a_1 : Iota), % 4.33/4.55 Or (Eq True False) % 4.33/4.55 (Or (Eq (msmaller a_snail a) False) % 4.33/4.55 (Or (Eq (plant (sf a_snail)) False) % 4.33/4.55 (Or (Eq (animal a_snail) False) % 4.33/4.55 (Or (Eq (plant a_1) False) % 4.33/4.55 (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_snail) True) (Eq (animal a) False))))))) % 4.33/4.55 Clause #118 (by clausification #[107]): Eq (bird a_bird) True % 4.33/4.55 Clause #119 (by clausification #[107]): Eq % 4.33/4.55 (And % 4.33/4.55 (And % 4.33/4.55 (And % 4.33/4.55 (And (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 4.33/4.55 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 4.33/4.55 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 4.33/4.55 (wolf a_wolf)) % 4.33/4.55 (fox a_fox)) % 4.33/4.55 True % 4.33/4.55 Clause #120 (by superposition #[118, 77]): ∀ (a : Iota), Or (Eq (msmaller a a_bird) True) (Or (Eq True False) (Eq (snail a) False)) % 4.33/4.55 Clause #121 (by clausification #[120]): ∀ (a : Iota), Or (Eq (msmaller a a_bird) True) (Eq (snail a) False) % 4.33/4.55 Clause #122 (by superposition #[121, 106]): Or (Eq (msmaller a_snail a_bird) True) (Eq False True) % 4.33/4.55 Clause #123 (by clausification #[122]): Eq (msmaller a_snail a_bird) True % 4.33/4.55 Clause #127 (by clausification #[116]): ∀ (a a_1 : Iota), % 4.33/4.55 Or (Eq (msmaller a_snail a) False) % 4.33/4.55 (Or (Eq (plant (sf a_snail)) False) % 4.33/4.55 (Or (Eq (animal a_snail) False) % 4.33/4.55 (Or (Eq (plant a_1) False) (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_snail) True) (Eq (animal a) False)))))) % 4.33/4.55 Clause #128 (by forward demodulation #[127, 110]): ∀ (a a_1 : Iota), % 4.33/4.55 Or (Eq (msmaller a_snail a) False) % 4.33/4.55 (Or (Eq True False) % 4.33/4.55 (Or (Eq (animal a_snail) False) % 4.33/4.55 (Or (Eq (plant a_1) False) (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_snail) True) (Eq (animal a) False)))))) % 4.33/4.55 Clause #129 (by clausification #[128]): ∀ (a a_1 : Iota), % 4.33/4.55 Or (Eq (msmaller a_snail a) False) % 4.33/4.55 (Or (Eq (animal a_snail) False) % 4.33/4.55 (Or (Eq (plant a_1) False) (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_snail) True) (Eq (animal a) False))))) % 4.33/4.55 Clause #130 (by superposition #[129, 123]): ∀ (a : Iota), % 4.33/4.55 Or (Eq (animal a_snail) False) % 4.33/4.55 (Or (Eq (plant a) False) % 4.33/4.55 (Or (Eq (eats a_bird a) True) % 4.33/4.55 (Or (Eq (eats a_bird a_snail) True) (Or (Eq (animal a_bird) False) (Eq False True))))) % 4.33/4.55 Clause #131 (by clausification #[130]): ∀ (a : Iota), % 4.33/4.55 Or (Eq (animal a_snail) False) % 4.33/4.55 (Or (Eq (plant a) False) % 4.33/4.55 (Or (Eq (eats a_bird a) True) (Or (Eq (eats a_bird a_snail) True) (Eq (animal a_bird) False)))) % 4.41/4.57 Clause #132 (by clausification #[119]): Eq (fox a_fox) True % 4.41/4.57 Clause #133 (by clausification #[119]): Eq % 4.41/4.57 (And % 4.41/4.57 (And % 4.41/4.57 (And (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 4.41/4.57 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 4.41/4.57 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 4.41/4.57 (wolf a_wolf)) % 4.41/4.57 True % 4.41/4.57 Clause #134 (by superposition #[132, 69]): ∀ (a : Iota), Or (Eq (msmaller a a_fox) True) (Or (Eq True False) (Eq (bird a) False)) % 4.41/4.57 Clause #135 (by clausification #[134]): ∀ (a : Iota), Or (Eq (msmaller a a_fox) True) (Eq (bird a) False) % 4.41/4.57 Clause #136 (by superposition #[135, 118]): Or (Eq (msmaller a_bird a_fox) True) (Eq False True) % 4.41/4.57 Clause #137 (by clausification #[136]): Eq (msmaller a_bird a_fox) True % 4.41/4.57 Clause #138 (by clausification #[133]): Eq (wolf a_wolf) True % 4.41/4.57 Clause #139 (by clausification #[133]): Eq % 4.41/4.57 (And % 4.41/4.57 (And (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 4.41/4.57 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 4.41/4.57 (∀ (X : Iota), Or (animal X) (Not (snail X)))) % 4.41/4.57 True % 4.41/4.57 Clause #140 (by superposition #[138, 61]): ∀ (a : Iota), Or (Eq (msmaller a a_wolf) True) (Or (Eq True False) (Eq (fox a) False)) % 4.41/4.57 Clause #141 (by clausification #[139]): Eq (∀ (X : Iota), Or (animal X) (Not (snail X))) True % 4.41/4.57 Clause #142 (by clausification #[139]): Eq % 4.41/4.57 (And (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) (∀ (X : Iota), Or (animal X) (Not (fox X)))) % 4.41/4.57 (∀ (X : Iota), Or (animal X) (Not (bird X)))) % 4.41/4.57 True % 4.41/4.57 Clause #143 (by clausification #[141]): ∀ (a : Iota), Eq (Or (animal a) (Not (snail a))) True % 4.41/4.57 Clause #144 (by clausification #[143]): ∀ (a : Iota), Or (Eq (animal a) True) (Eq (Not (snail a)) True) % 4.41/4.57 Clause #145 (by clausification #[144]): ∀ (a : Iota), Or (Eq (animal a) True) (Eq (snail a) False) % 4.41/4.57 Clause #146 (by superposition #[145, 106]): Or (Eq (animal a_snail) True) (Eq False True) % 4.41/4.57 Clause #147 (by clausification #[146]): Eq (animal a_snail) True % 4.41/4.57 Clause #150 (by backward demodulation #[147, 131]): ∀ (a : Iota), % 4.41/4.57 Or (Eq True False) % 4.41/4.57 (Or (Eq (plant a) False) % 4.41/4.57 (Or (Eq (eats a_bird a) True) (Or (Eq (eats a_bird a_snail) True) (Eq (animal a_bird) False)))) % 4.41/4.57 Clause #151 (by clausification #[140]): ∀ (a : Iota), Or (Eq (msmaller a a_wolf) True) (Eq (fox a) False) % 4.41/4.57 Clause #152 (by superposition #[151, 132]): Or (Eq (msmaller a_fox a_wolf) True) (Eq False True) % 4.41/4.57 Clause #153 (by clausification #[152]): Eq (msmaller a_fox a_wolf) True % 4.41/4.57 Clause #155 (by clausification #[150]): ∀ (a : Iota), % 4.41/4.57 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))) % 4.41/4.57 Clause #156 (by superposition #[155, 105]): 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))) % 4.41/4.57 Clause #158 (by clausification #[142]): Eq (∀ (X : Iota), Or (animal X) (Not (bird X))) True % 4.41/4.57 Clause #159 (by clausification #[142]): Eq (And (∀ (X : Iota), Or (animal X) (Not (wolf X))) (∀ (X : Iota), Or (animal X) (Not (fox X)))) True % 4.41/4.57 Clause #160 (by clausification #[158]): ∀ (a : Iota), Eq (Or (animal a) (Not (bird a))) True % 4.41/4.57 Clause #161 (by clausification #[160]): ∀ (a : Iota), Or (Eq (animal a) True) (Eq (Not (bird a)) True) % 4.41/4.57 Clause #162 (by clausification #[161]): ∀ (a : Iota), Or (Eq (animal a) True) (Eq (bird a) False) % 4.41/4.57 Clause #163 (by superposition #[162, 118]): Or (Eq (animal a_bird) True) (Eq False True) % 4.41/4.57 Clause #164 (by clausification #[163]): Eq (animal a_bird) True % 4.41/4.57 Clause #166 (by clausification #[156]): Or (Eq (eats a_bird a_grain) True) (Or (Eq (eats a_bird a_snail) True) (Eq (animal a_bird) False)) % 4.41/4.57 Clause #167 (by forward demodulation #[166, 164]): Or (Eq (eats a_bird a_grain) True) (Or (Eq (eats a_bird a_snail) True) (Eq True False)) % 4.41/4.57 Clause #168 (by clausification #[167]): Or (Eq (eats a_bird a_grain) True) (Eq (eats a_bird a_snail) True) % 4.41/4.57 Clause #169 (by superposition #[168, 16]): ∀ (a : Iota), % 4.41/4.57 Or (Eq (eats a_bird a_snail) True) % 4.41/4.57 (Or (Eq True False) % 4.41/4.57 (Or (Eq (eats a a_bird) False) % 4.41/4.57 (Or (Eq (grain a_grain) False) (Or (Eq (animal a) False) (Eq (animal a_bird) False))))) % 4.43/4.59 Clause #173 (by superposition #[168, 96]): ∀ (a a_1 : Iota), % 4.43/4.59 Or (Eq (eats a_bird a_snail) True) % 4.43/4.59 (Or (Eq True False) % 4.43/4.59 (Or (Eq (msmaller a_bird a) False) % 4.43/4.59 (Or (Eq (plant a_grain) False) % 4.43/4.59 (Or (Eq (animal a_bird) False) % 4.43/4.59 (Or (Eq (plant a_1) False) % 4.43/4.59 (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_bird) True) (Eq (animal a) False)))))))) % 4.43/4.59 Clause #199 (by clausification #[159]): Eq (∀ (X : Iota), Or (animal X) (Not (fox X))) True % 4.43/4.59 Clause #200 (by clausification #[159]): Eq (∀ (X : Iota), Or (animal X) (Not (wolf X))) True % 4.43/4.59 Clause #201 (by clausification #[199]): ∀ (a : Iota), Eq (Or (animal a) (Not (fox a))) True % 4.43/4.59 Clause #202 (by clausification #[201]): ∀ (a : Iota), Or (Eq (animal a) True) (Eq (Not (fox a)) True) % 4.43/4.59 Clause #203 (by clausification #[202]): ∀ (a : Iota), Or (Eq (animal a) True) (Eq (fox a) False) % 4.43/4.59 Clause #204 (by superposition #[203, 132]): Or (Eq (animal a_fox) True) (Eq False True) % 4.43/4.59 Clause #205 (by clausification #[204]): Eq (animal a_fox) True % 4.43/4.59 Clause #206 (by clausification #[200]): ∀ (a : Iota), Eq (Or (animal a) (Not (wolf a))) True % 4.43/4.59 Clause #207 (by clausification #[206]): ∀ (a : Iota), Or (Eq (animal a) True) (Eq (Not (wolf a)) True) % 4.43/4.59 Clause #208 (by clausification #[207]): ∀ (a : Iota), Or (Eq (animal a) True) (Eq (wolf a) False) % 4.43/4.59 Clause #209 (by superposition #[208, 138]): Or (Eq (animal a_wolf) True) (Eq False True) % 4.43/4.59 Clause #210 (by clausification #[209]): Eq (animal a_wolf) True % 4.43/4.59 Clause #211 (by clausification #[169]): ∀ (a : Iota), % 4.43/4.59 Or (Eq (eats a_bird a_snail) True) % 4.43/4.59 (Or (Eq (eats a a_bird) False) % 4.43/4.59 (Or (Eq (grain a_grain) False) (Or (Eq (animal a) False) (Eq (animal a_bird) False)))) % 4.43/4.59 Clause #212 (by forward demodulation #[211, 102]): ∀ (a : Iota), % 4.43/4.59 Or (Eq (eats a_bird a_snail) True) % 4.43/4.59 (Or (Eq (eats a a_bird) False) (Or (Eq True False) (Or (Eq (animal a) False) (Eq (animal a_bird) False)))) % 4.43/4.59 Clause #213 (by clausification #[212]): ∀ (a : Iota), % 4.43/4.59 Or (Eq (eats a_bird a_snail) True) % 4.43/4.59 (Or (Eq (eats a a_bird) False) (Or (Eq (animal a) False) (Eq (animal a_bird) False))) % 4.43/4.59 Clause #214 (by forward demodulation #[213, 164]): ∀ (a : Iota), % 4.43/4.59 Or (Eq (eats a_bird a_snail) True) (Or (Eq (eats a a_bird) False) (Or (Eq (animal a) False) (Eq True False))) % 4.43/4.59 Clause #215 (by clausification #[214]): ∀ (a : Iota), Or (Eq (eats a_bird a_snail) True) (Or (Eq (eats a a_bird) False) (Eq (animal a) False)) % 4.43/4.59 Clause #219 (by clausification #[173]): ∀ (a a_1 : Iota), % 4.43/4.59 Or (Eq (eats a_bird a_snail) True) % 4.43/4.59 (Or (Eq (msmaller a_bird a) False) % 4.43/4.59 (Or (Eq (plant a_grain) False) % 4.43/4.59 (Or (Eq (animal a_bird) False) % 4.43/4.59 (Or (Eq (plant a_1) False) % 4.43/4.59 (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_bird) True) (Eq (animal a) False))))))) % 4.43/4.59 Clause #220 (by forward demodulation #[219, 105]): ∀ (a a_1 : Iota), % 4.43/4.59 Or (Eq (eats a_bird a_snail) True) % 4.43/4.59 (Or (Eq (msmaller a_bird a) False) % 4.43/4.59 (Or (Eq True False) % 4.43/4.59 (Or (Eq (animal a_bird) False) % 4.43/4.59 (Or (Eq (plant a_1) False) % 4.43/4.59 (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_bird) True) (Eq (animal a) False))))))) % 4.43/4.59 Clause #221 (by clausification #[220]): ∀ (a a_1 : Iota), % 4.43/4.59 Or (Eq (eats a_bird a_snail) True) % 4.43/4.59 (Or (Eq (msmaller a_bird a) False) % 4.43/4.59 (Or (Eq (animal a_bird) False) % 4.43/4.59 (Or (Eq (plant a_1) False) (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_bird) True) (Eq (animal a) False)))))) % 4.43/4.59 Clause #222 (by forward demodulation #[221, 164]): ∀ (a a_1 : Iota), % 4.43/4.59 Or (Eq (eats a_bird a_snail) True) % 4.43/4.59 (Or (Eq (msmaller a_bird a) False) % 4.43/4.59 (Or (Eq True False) % 4.43/4.59 (Or (Eq (plant a_1) False) (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_bird) True) (Eq (animal a) False)))))) % 4.43/4.59 Clause #223 (by clausification #[222]): ∀ (a a_1 : Iota), % 4.43/4.59 Or (Eq (eats a_bird a_snail) True) % 4.43/4.59 (Or (Eq (msmaller a_bird a) False) % 4.43/4.59 (Or (Eq (plant a_1) False) (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_bird) True) (Eq (animal a) False))))) % 4.43/4.59 Clause #224 (by superposition #[223, 137]): ∀ (a : Iota), % 4.43/4.61 Or (Eq (eats a_bird a_snail) True) % 4.43/4.61 (Or (Eq (plant a) False) % 4.43/4.61 (Or (Eq (eats a_fox a) True) (Or (Eq (eats a_fox a_bird) True) (Or (Eq (animal a_fox) False) (Eq False True))))) % 4.43/4.61 Clause #225 (by clausification #[224]): ∀ (a : Iota), % 4.43/4.61 Or (Eq (eats a_bird a_snail) True) % 4.43/4.61 (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)))) % 4.43/4.61 Clause #226 (by forward demodulation #[225, 205]): ∀ (a : Iota), % 4.43/4.61 Or (Eq (eats a_bird a_snail) True) % 4.43/4.61 (Or (Eq (plant a) False) (Or (Eq (eats a_fox a) True) (Or (Eq (eats a_fox a_bird) True) (Eq True False)))) % 4.43/4.61 Clause #227 (by clausification #[226]): ∀ (a : Iota), % 4.43/4.61 Or (Eq (eats a_bird a_snail) True) % 4.43/4.61 (Or (Eq (plant a) False) (Or (Eq (eats a_fox a) True) (Eq (eats a_fox a_bird) True))) % 4.43/4.61 Clause #228 (by superposition #[227, 105]): Or (Eq (eats a_bird a_snail) True) % 4.43/4.61 (Or (Eq (eats a_fox a_grain) True) (Or (Eq (eats a_fox a_bird) True) (Eq False True))) % 4.43/4.61 Clause #230 (by clausification #[228]): Or (Eq (eats a_bird a_snail) True) (Or (Eq (eats a_fox a_grain) True) (Eq (eats a_fox a_bird) True)) % 4.43/4.61 Clause #233 (by superposition #[230, 35]): Or (Eq (eats a_fox a_grain) True) % 4.43/4.61 (Or (Eq (eats a_fox a_bird) True) (Or (Eq True False) (Or (Eq (bird a_bird) False) (Eq (snail a_snail) False)))) % 4.43/4.61 Clause #247 (by clausification #[233]): Or (Eq (eats a_fox a_grain) True) % 4.43/4.61 (Or (Eq (eats a_fox a_bird) True) (Or (Eq (bird a_bird) False) (Eq (snail a_snail) False))) % 4.43/4.61 Clause #248 (by forward demodulation #[247, 118]): 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))) % 4.43/4.61 Clause #249 (by clausification #[248]): Or (Eq (eats a_fox a_grain) True) (Or (Eq (eats a_fox a_bird) True) (Eq (snail a_snail) False)) % 4.43/4.61 Clause #250 (by forward demodulation #[249, 106]): Or (Eq (eats a_fox a_grain) True) (Or (Eq (eats a_fox a_bird) True) (Eq True False)) % 4.43/4.61 Clause #251 (by clausification #[250]): Or (Eq (eats a_fox a_grain) True) (Eq (eats a_fox a_bird) True) % 4.43/4.61 Clause #256 (by superposition #[251, 96]): ∀ (a a_1 : Iota), % 4.43/4.61 Or (Eq (eats a_fox a_bird) True) % 4.43/4.61 (Or (Eq True False) % 4.43/4.61 (Or (Eq (msmaller a_fox a) False) % 4.43/4.61 (Or (Eq (plant a_grain) False) % 4.43/4.61 (Or (Eq (animal a_fox) False) % 4.43/4.61 (Or (Eq (plant a_1) False) % 4.43/4.61 (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_fox) True) (Eq (animal a) False)))))))) % 4.43/4.61 Clause #300 (by clausification #[256]): ∀ (a a_1 : Iota), % 4.43/4.61 Or (Eq (eats a_fox a_bird) True) % 4.43/4.61 (Or (Eq (msmaller a_fox a) False) % 4.43/4.61 (Or (Eq (plant a_grain) False) % 4.43/4.61 (Or (Eq (animal a_fox) False) % 4.43/4.61 (Or (Eq (plant a_1) False) (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_fox) True) (Eq (animal a) False))))))) % 4.43/4.61 Clause #301 (by forward demodulation #[300, 105]): ∀ (a a_1 : Iota), % 4.43/4.61 Or (Eq (eats a_fox a_bird) True) % 4.43/4.61 (Or (Eq (msmaller a_fox a) False) % 4.43/4.61 (Or (Eq True False) % 4.43/4.61 (Or (Eq (animal a_fox) False) % 4.43/4.61 (Or (Eq (plant a_1) False) (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_fox) True) (Eq (animal a) False))))))) % 4.43/4.61 Clause #302 (by clausification #[301]): ∀ (a a_1 : Iota), % 4.43/4.61 Or (Eq (eats a_fox a_bird) True) % 4.43/4.61 (Or (Eq (msmaller a_fox a) False) % 4.43/4.61 (Or (Eq (animal a_fox) False) % 4.43/4.61 (Or (Eq (plant a_1) False) (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_fox) True) (Eq (animal a) False)))))) % 4.43/4.61 Clause #303 (by forward demodulation #[302, 205]): ∀ (a a_1 : Iota), % 4.43/4.61 Or (Eq (eats a_fox a_bird) True) % 4.43/4.61 (Or (Eq (msmaller a_fox a) False) % 4.43/4.61 (Or (Eq True False) % 4.43/4.61 (Or (Eq (plant a_1) False) (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_fox) True) (Eq (animal a) False)))))) % 4.43/4.61 Clause #304 (by clausification #[303]): ∀ (a a_1 : Iota), % 4.43/4.61 Or (Eq (eats a_fox a_bird) True) % 4.43/4.61 (Or (Eq (msmaller a_fox a) False) % 4.43/4.61 (Or (Eq (plant a_1) False) (Or (Eq (eats a a_1) True) (Or (Eq (eats a a_fox) True) (Eq (animal a) False))))) % 4.43/4.61 Clause #305 (by superposition #[304, 153]): ∀ (a : Iota), % 4.43/4.61 Or (Eq (eats a_fox a_bird) True) % 4.43/4.61 (Or (Eq (plant a) False) % 4.43/4.61 (Or (Eq (eats a_wolf a) True) (Or (Eq (eats a_wolf a_fox) True) (Or (Eq (animal a_wolf) False) (Eq False True))))) % 4.47/4.63 Clause #306 (by clausification #[305]): ∀ (a : Iota), % 4.47/4.63 Or (Eq (eats a_fox a_bird) True) % 4.47/4.63 (Or (Eq (plant a) False) % 4.47/4.63 (Or (Eq (eats a_wolf a) True) (Or (Eq (eats a_wolf a_fox) True) (Eq (animal a_wolf) False)))) % 4.47/4.63 Clause #307 (by forward demodulation #[306, 210]): ∀ (a : Iota), % 4.47/4.63 Or (Eq (eats a_fox a_bird) True) % 4.47/4.63 (Or (Eq (plant a) False) (Or (Eq (eats a_wolf a) True) (Or (Eq (eats a_wolf a_fox) True) (Eq True False)))) % 4.47/4.63 Clause #308 (by clausification #[307]): ∀ (a : Iota), % 4.47/4.63 Or (Eq (eats a_fox a_bird) True) % 4.47/4.63 (Or (Eq (plant a) False) (Or (Eq (eats a_wolf a) True) (Eq (eats a_wolf a_fox) True))) % 4.47/4.63 Clause #309 (by superposition #[308, 105]): 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))) % 4.47/4.63 Clause #311 (by clausification #[309]): Or (Eq (eats a_fox a_bird) True) (Or (Eq (eats a_wolf a_grain) True) (Eq (eats a_wolf a_fox) True)) % 4.47/4.63 Clause #312 (by superposition #[311, 215]): Or (Eq (eats a_wolf a_grain) True) % 4.47/4.63 (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)))) % 4.47/4.63 Clause #335 (by clausification #[312]): Or (Eq (eats a_wolf a_grain) True) % 4.47/4.63 (Or (Eq (eats a_wolf a_fox) True) (Or (Eq (eats a_bird a_snail) True) (Eq (animal a_fox) False))) % 4.47/4.63 Clause #336 (by forward demodulation #[335, 205]): Or (Eq (eats a_wolf a_grain) True) % 4.47/4.63 (Or (Eq (eats a_wolf a_fox) True) (Or (Eq (eats a_bird a_snail) True) (Eq True False))) % 4.47/4.63 Clause #337 (by clausification #[336]): Or (Eq (eats a_wolf a_grain) True) (Or (Eq (eats a_wolf a_fox) True) (Eq (eats a_bird a_snail) True)) % 4.47/4.63 Clause #340 (by superposition #[337, 35]): Or (Eq (eats a_wolf a_grain) True) % 4.47/4.63 (Or (Eq (eats a_wolf a_fox) True) (Or (Eq True False) (Or (Eq (bird a_bird) False) (Eq (snail a_snail) False)))) % 4.47/4.63 Clause #349 (by clausification #[340]): Or (Eq (eats a_wolf a_grain) True) % 4.47/4.63 (Or (Eq (eats a_wolf a_fox) True) (Or (Eq (bird a_bird) False) (Eq (snail a_snail) False))) % 4.47/4.63 Clause #350 (by forward demodulation #[349, 118]): 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))) % 4.47/4.63 Clause #351 (by clausification #[350]): Or (Eq (eats a_wolf a_grain) True) (Or (Eq (eats a_wolf a_fox) True) (Eq (snail a_snail) False)) % 4.47/4.63 Clause #352 (by forward demodulation #[351, 106]): Or (Eq (eats a_wolf a_grain) True) (Or (Eq (eats a_wolf a_fox) True) (Eq True False)) % 4.47/4.63 Clause #353 (by clausification #[352]): Or (Eq (eats a_wolf a_grain) True) (Eq (eats a_wolf a_fox) True) % 4.47/4.63 Clause #356 (by superposition #[353, 44]): Or (Eq (eats a_wolf a_fox) True) (Or (Eq True False) (Or (Eq (wolf a_wolf) False) (Eq (grain a_grain) False))) % 4.47/4.63 Clause #362 (by clausification #[356]): Or (Eq (eats a_wolf a_fox) True) (Or (Eq (wolf a_wolf) False) (Eq (grain a_grain) False)) % 4.47/4.63 Clause #363 (by forward demodulation #[362, 138]): Or (Eq (eats a_wolf a_fox) True) (Or (Eq True False) (Eq (grain a_grain) False)) % 4.47/4.63 Clause #364 (by clausification #[363]): Or (Eq (eats a_wolf a_fox) True) (Eq (grain a_grain) False) % 4.47/4.63 Clause #365 (by forward demodulation #[364, 102]): Or (Eq (eats a_wolf a_fox) True) (Eq True False) % 4.47/4.63 Clause #366 (by clausification #[365]): Eq (eats a_wolf a_fox) True % 4.47/4.63 Clause #377 (by superposition #[366, 53]): Or (Eq True False) (Or (Eq (wolf a_wolf) False) (Eq (fox a_fox) False)) % 4.47/4.63 Clause #379 (by clausification #[377]): Or (Eq (wolf a_wolf) False) (Eq (fox a_fox) False) % 4.47/4.63 Clause #380 (by forward demodulation #[379, 132]): Or (Eq (wolf a_wolf) False) (Eq True False) % 4.47/4.63 Clause #381 (by clausification #[380]): Eq (wolf a_wolf) False % 4.47/4.63 Clause #382 (by superposition #[381, 138]): Eq False True % 4.47/4.63 Clause #385 (by clausification #[382]): False % 4.47/4.63 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------