The cat chases the rabbit. The cat is blue. The cat is rough. The cat is round. The rabbit chases the cat. The rabbit likes the cat. The rabbit needs the cat. If someone needs the cat then they are round. If the rabbit chases the cat then the cat likes the rabbit. If someone likes the rabbit then they chase the rabbit. All blue people are cold. If someone likes the rabbit then the rabbit is big. Round people are cold. If someone is big then they chase the rabbit. If the rabbit chases the cat then the cat likes the rabbit.
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is round.
("cat" "is" "round" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
If someone needs the cat then they are round.
((("someone" "needs" "cat" "+")) -> ("someone" "is" "round" "+"))
If the rabbit chases the cat then the cat likes the rabbit.
((("rabbit" "chases" "cat" "+")) -> ("cat" "likes" "rabbit" "+"))
If someone likes the rabbit then they chase the rabbit.
((("someone" "likes" "rabbit" "+")) -> ("someone" "chases" "rabbit" "+"))
All blue people are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
If someone likes the rabbit then the rabbit is big.
((("someone" "likes" "rabbit" "+")) -> ("rabbit" "is" "big" "+"))
Round people are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
If someone is big then they chase the rabbit.
((("someone" "is" "big" "+")) -> ("someone" "chases" "rabbit" "+"))
If the rabbit chases the cat then the cat likes the rabbit.
((("rabbit" "chases" "cat" "+")) -> ("cat" "likes" "rabbit" "+"))
The cat is round.
True
1
proof
[(triple4)]
("cat" "is" "round" "+")
triple4
The cat is not blue.
False
1
inv-proof
[(triple2)]
("cat" "is" "blue" "-")
triple2
The cat is cold.
True
2
proof
[(((triple2) -> rule4) OR ((triple4) -> rule6))]
("cat" "is" "cold" "+")
((triple2) -> (rule4 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
((triple4) -> (rule6 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat does not like the rabbit.
False
2
inv-proof
[(((triple5) -> rule2) OR ((triple5) -> rule8))]
("cat" "likes" "rabbit" "-")
((triple5) -> (rule2 % int1))
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int1
((triple5) -> (rule8 % int1))
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int1
The rabbit is cold.
True
3
proof
[(((((triple7) -> rule1)) -> rule6))]
("rabbit" "is" "cold" "+")
((((triple7) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit is not big.
False
3
inv-proof
[(((((triple5) -> rule2)) -> rule5) OR ((((triple5) -> rule8)) -> rule5))]
("rabbit" "is" "big" "-")
((((triple5) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int2
((((triple5) -> (rule8 % int2))) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int2
The rabbit chases the rabbit.
True
4
proof
[(((((((triple5) -> rule2)) -> rule5)) -> rule7) OR ((((((triple5) -> rule8)) -> rule5)) -> rule7))]
("rabbit" "chases" "rabbit" "+")
((((((triple5) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int3
((((((triple5) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int3
The rabbit does not chase the rabbit.
False
4
inv-proof
[(((((((triple5) -> rule2)) -> rule5)) -> rule7) OR ((((((triple5) -> rule8)) -> rule5)) -> rule7))]
("rabbit" "chases" "rabbit" "-")
((((((triple5) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int3
((((((triple5) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int3
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The rabbit is blue.
Unknown
random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "+")
The rabbit is not rough.
Unknown
inv-random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "-")
The cat needs the rabbit.
Unknown
random
[@0: The cat needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "rabbit" "+")
@0: The cat chases the rabbit.[(triple1 OR ((((triple5) -> rule2)) -> rule3) OR ((((triple5) -> rule8)) -> rule3))] The cat is blue.[(triple2)] The cat is rough.[(triple3)] The cat is round.[(triple4)] The rabbit chases the cat.[(triple5)] The rabbit likes the cat.[(triple6)] The rabbit needs the cat.[(triple7)] @1: The cat is cold.[(((triple2) -> rule4) OR ((triple4) -> rule6))] The cat likes the rabbit.[(((triple5) -> rule2) OR ((triple5) -> rule8))] The rabbit is round.[(((triple7) -> rule1))] @2: The rabbit is big.[(((((triple5) -> rule2)) -> rule5) OR ((((triple5) -> rule8)) -> rule5))] The rabbit is cold.[(((((triple7) -> rule1)) -> rule6))] @3: The rabbit chases the rabbit.[(((((((triple5) -> rule2)) -> rule5)) -> rule7) OR ((((((triple5) -> rule8)) -> rule5)) -> rule7))]
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple1
((((triple5) -> (rule2 % int2))) -> (rule3 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int2
((((triple5) -> (rule8 % int2))) -> (rule3 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat is rough.
("cat" "is" "rough" "+")
triple3
The cat is round.
("cat" "is" "round" "+")
triple4
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple5
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple6
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple7
The cat is cold.
("cat" "is" "cold" "+")
((triple2) -> (rule4 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
((triple4) -> (rule6 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
((triple5) -> (rule2 % int1))
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int1
((triple5) -> (rule8 % int1))
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
((triple7) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
((((triple5) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int2
((((triple5) -> (rule8 % int2))) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
((((triple7) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((((((triple5) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int3
((((((triple5) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int3