The bald eagle does not visit the cat. The cat needs the rabbit. The cat needs the tiger. The cat visits the rabbit. The rabbit needs the bald eagle. The rabbit visits the bald eagle. The tiger is kind. The tiger is red. The tiger does not like the bald eagle. The tiger visits the rabbit. If the rabbit needs the bald eagle then the rabbit needs the cat. If someone likes the rabbit and they do not like the tiger then the rabbit does not visit the bald eagle. If someone needs the tiger then the tiger does not need the bald eagle. If the cat likes the tiger then the cat visits the bald eagle. If someone needs the cat then the cat needs the bald eagle. If someone needs the bald eagle then they are big. If someone needs the rabbit and they do not like the tiger then they do not like the rabbit. If someone likes the bald eagle then the bald eagle is kind.
The bald eagle does not visit the cat.
("bald eagle" "visits" "cat" "-")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The rabbit needs the bald eagle.
("rabbit" "needs" "bald eagle" "+")
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger does not like the bald eagle.
("tiger" "likes" "bald eagle" "-")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If the rabbit needs the bald eagle then the rabbit needs the cat.
((("rabbit" "needs" "bald eagle" "+")) -> ("rabbit" "needs" "cat" "+"))
If someone likes the rabbit and they do not like the tiger then the rabbit does not visit the bald eagle.
((("someone" "likes" "rabbit" "+") ("someone" "likes" "tiger" "~")) -> ("rabbit" "visits" "bald eagle" "-"))
If someone needs the tiger then the tiger does not need the bald eagle.
((("someone" "needs" "tiger" "+")) -> ("tiger" "needs" "bald eagle" "-"))
If the cat likes the tiger then the cat visits the bald eagle.
((("cat" "likes" "tiger" "+")) -> ("cat" "visits" "bald eagle" "+"))
If someone needs the cat then the cat needs the bald eagle.
((("someone" "needs" "cat" "+")) -> ("cat" "needs" "bald eagle" "+"))
If someone needs the bald eagle then they are big.
((("someone" "needs" "bald eagle" "+")) -> ("someone" "is" "big" "+"))
If someone needs the rabbit and they do not like the tiger then they do not like the rabbit.
((("someone" "needs" "rabbit" "+") ("someone" "likes" "tiger" "~")) -> ("someone" "likes" "rabbit" "-"))
If someone likes the bald eagle then the bald eagle is kind.
((("someone" "likes" "bald eagle" "+")) -> ("bald eagle" "is" "kind" "+"))
The cat visits the rabbit.
True
1
proof
[(triple4)]
("cat" "visits" "rabbit" "+")
triple4
The rabbit does not need the bald eagle.
False
1
inv-proof
[(triple5)]
("rabbit" "needs" "bald eagle" "-")
triple5
The rabbit needs the cat.
True
2
proof
[(((triple5) -> rule1))]
("rabbit" "needs" "cat" "+")
((triple5) -> (rule1 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
The rabbit is not big.
False
2
inv-proof
[(((triple5) -> rule6))]
("rabbit" "is" "big" "-")
((triple5) -> (rule6 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The cat needs the bald eagle.
True
3
proof
[(((((triple5) -> rule1)) -> rule5))]
("cat" "needs" "bald eagle" "+")
((((triple5) -> (rule1 % int2))) -> (rule5 % int1))
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
int1
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int2
The cat does not need the bald eagle.
False
3
inv-proof
[(((((triple5) -> rule1)) -> rule5))]
("cat" "needs" "bald eagle" "-")
((((triple5) -> (rule1 % int2))) -> (rule5 % int1))
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
int1
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int2
The cat is big.
True
4
proof
[(((((((triple5) -> rule1)) -> rule5)) -> rule6))]
("cat" "is" "big" "+")
((((((triple5) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
int2
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int3
The cat is not big.
False
4
inv-proof
[(((((((triple5) -> rule1)) -> rule5)) -> rule6))]
("cat" "is" "big" "-")
((((((triple5) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
int2
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int3
The bald eagle is not kind.
Unknown
inv-rconc
[@1: The bald eagle is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bald eagle" "is" "kind" "-")
The cat visits the bald eagle.
Unknown
rconc
[@1: The cat visits the bald eagle.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "visits" "bald eagle" "+")
The tiger is not big.
Unknown
inv-rconc
[@1: The tiger is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "is" "big" "-")
The bald eagle is big.
Unknown
rconc
[@1: The bald eagle is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bald eagle" "is" "big" "+")
The rabbit does not visit the cat.
Unknown
inv-random
[@0: The rabbit visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "cat" "-")
The rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
The cat is not green.
Unknown
inv-random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "-")
The cat visits the tiger.
Unknown
random
[@0: The cat visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "tiger" "+")
@0: The bald eagle does not visit the cat.[(triple1)] The cat needs the rabbit.[(triple2)] The cat needs the tiger.[(triple3)] The cat visits the rabbit.[(triple4)] The rabbit needs the bald eagle.[(triple5)] The rabbit visits the bald eagle.[(triple6)] The tiger does not like the bald eagle.[(triple9)] The tiger is kind.[(triple7)] The tiger is red.[(triple8)] The tiger visits the rabbit.[(triple10)] @1: The rabbit is big.[(((triple5) -> rule6))] The rabbit needs the cat.[(((triple5) -> rule1))] The tiger does not need the bald eagle.[(((triple3) -> rule3))] @2: The cat needs the bald eagle.[(((((triple5) -> rule1)) -> rule5))] @3: The cat is big.[(((((((triple5) -> rule1)) -> rule5)) -> rule6))]
The bald eagle does not visit the cat.
("bald eagle" "visits" "cat" "-")
triple1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple3
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple4
The rabbit needs the bald eagle.
("rabbit" "needs" "bald eagle" "+")
triple5
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
triple6
The tiger does not like the bald eagle.
("tiger" "likes" "bald eagle" "-")
triple9
The tiger is kind.
("tiger" "is" "kind" "+")
triple7
The tiger is red.
("tiger" "is" "red" "+")
triple8
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple10
The rabbit is big.
("rabbit" "is" "big" "+")
((triple5) -> (rule6 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
((triple5) -> (rule1 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
The tiger does not need the bald eagle.
("tiger" "needs" "bald eagle" "-")
((triple3) -> (rule3 % int1))
The tiger does not need the bald eagle.
("tiger" "needs" "bald eagle" "-")
int1
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
((((triple5) -> (rule1 % int2))) -> (rule5 % int1))
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
int1
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int2
The cat is big.
("cat" "is" "big" "+")
((((((triple5) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
int2
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int3