The bald eagle eats the cat. The bald eagle is cold. The cat is cold. The cat is rough. The cat likes the bald eagle. The cow eats the cat. The cow sees the cat. If someone is green then they are rough. If someone eats the cat then the cat is rough. If someone is young and they eat the cow then they are rough. If someone is red and they like the bald eagle then the bald eagle likes the cow. If someone is rough then they eat the cow. If someone likes the cat and the cat is red then the cat eats the cow. If someone is rough then they like the bald eagle. If someone likes the bald eagle then they like the cat.
The bald eagle eats the cat.
("bald eagle" "eats" "cat" "+")
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
If someone is green then they are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If someone eats the cat then the cat is rough.
((("someone" "eats" "cat" "+")) -> ("cat" "is" "rough" "+"))
If someone is young and they eat the cow then they are rough.
((("someone" "is" "young" "+") ("someone" "eats" "cow" "+")) -> ("someone" "is" "rough" "+"))
If someone is red and they like the bald eagle then the bald eagle likes the cow.
((("someone" "is" "red" "+") ("someone" "likes" "bald eagle" "+")) -> ("bald eagle" "likes" "cow" "+"))
If someone is rough then they eat the cow.
((("someone" "is" "rough" "+")) -> ("someone" "eats" "cow" "+"))
If someone likes the cat and the cat is red then the cat eats the cow.
((("someone" "likes" "cat" "+") ("cat" "is" "red" "+")) -> ("cat" "eats" "cow" "+"))
If someone is rough then they like the bald eagle.
((("someone" "is" "rough" "+")) -> ("someone" "likes" "bald eagle" "+"))
If someone likes the bald eagle then they like the cat.
((("someone" "likes" "bald eagle" "+")) -> ("someone" "likes" "cat" "+"))
The cat is rough.
True
1
proof
[(triple4 OR ((triple1) -> rule2) OR ((triple6) -> rule2))]
("cat" "is" "rough" "+")
triple4
((triple1) -> (rule2 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
((triple6) -> (rule2 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cow does not see the cat.
False
1
inv-proof
[(triple7)]
("cow" "sees" "cat" "-")
triple7
The cat likes the cat.
True
2
proof
[(((triple5) -> rule8) OR ((((triple4) -> rule7)) -> rule8) OR ((((((triple1) -> rule2)) -> rule7)) -> rule8) OR ((((((triple6) -> rule2)) -> rule7)) -> rule8))]
("cat" "likes" "cat" "+")
((triple5) -> (rule8 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
((((triple4) -> (rule7 % int2))) -> (rule8 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
((((((triple6) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
The cat does not eat the cow.
False
2
inv-proof
[(((triple4) -> rule5) OR ((((triple1) -> rule2)) -> rule5) OR ((((triple6) -> rule2)) -> rule5))]
("cat" "eats" "cow" "-")
((triple4) -> (rule5 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
((((triple6) -> (rule2 % int2))) -> (rule5 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The bald eagle is not rough.
Unknown
inv-rconc
[@1: The bald eagle is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "is" "rough" "-")
The cow likes the bald eagle.
Unknown
rconc
[@2: The cow likes the bald eagle.[CWA. Example of deepest failure = (rule7 <- rule1 <- FAIL)]]
("cow" "likes" "bald eagle" "+")
The cat is not young.
Unknown
inv-random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "-")
The cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
@0: The bald eagle eats the cat.[(triple1)] The bald eagle is cold.[(triple2)] The cat is cold.[(triple3)] The cat is rough.[(triple4 OR ((triple1) -> rule2) OR ((triple6) -> rule2))] The cat likes the bald eagle.[(triple5 OR ((triple4) -> rule7) OR ((((triple1) -> rule2)) -> rule7) OR ((((triple6) -> rule2)) -> rule7))] The cow eats the cat.[(triple6)] The cow sees the cat.[(triple7)] @1: The cat eats the cow.[(((triple4) -> rule5) OR ((((triple1) -> rule2)) -> rule5) OR ((((triple6) -> rule2)) -> rule5))] The cat likes the cat.[(((triple5) -> rule8) OR ((((triple4) -> rule7)) -> rule8) OR ((((((triple1) -> rule2)) -> rule7)) -> rule8) OR ((((((triple6) -> rule2)) -> rule7)) -> rule8))]
The bald eagle eats the cat.
("bald eagle" "eats" "cat" "+")
triple1
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
triple2
The cat is cold.
("cat" "is" "cold" "+")
triple3
The cat is rough.
("cat" "is" "rough" "+")
triple4
((triple1) -> (rule2 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
((triple6) -> (rule2 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
triple5
((triple4) -> (rule7 % int1))
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
((((triple6) -> (rule2 % int2))) -> (rule7 % int1))
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cow eats the cat.
("cow" "eats" "cat" "+")
triple6
The cow sees the cat.
("cow" "sees" "cat" "+")
triple7
The cat eats the cow.
("cat" "eats" "cow" "+")
((triple4) -> (rule5 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
((((triple6) -> (rule2 % int2))) -> (rule5 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The cat likes the cat.
("cat" "likes" "cat" "+")
((triple5) -> (rule8 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
((((triple4) -> (rule7 % int2))) -> (rule8 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3
((((((triple6) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
int2
The cat is rough.
("cat" "is" "rough" "+")
int3