The bear likes the rabbit. The cow is big. The mouse likes the cow. The rabbit is blue. If someone chases the cow then the cow is rough. If someone chases the cow and they are big then they are rough. If someone likes the cow then the cow eats the mouse. If someone eats the cow then they like the bear. If the bear is big and the bear is blue then the bear eats the mouse. If the rabbit eats the cow and the cow is blue then the cow chases the bear. If someone likes the rabbit and the rabbit likes the mouse then they like the bear. If someone eats the mouse then they eat the cow.
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
The cow is big.
("cow" "is" "big" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
If someone chases the cow then the cow is rough.
((("someone" "chases" "cow" "+")) -> ("cow" "is" "rough" "+"))
If someone chases the cow and they are big then they are rough.
((("someone" "chases" "cow" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
If someone likes the cow then the cow eats the mouse.
((("someone" "likes" "cow" "+")) -> ("cow" "eats" "mouse" "+"))
If someone eats the cow then they like the bear.
((("someone" "eats" "cow" "+")) -> ("someone" "likes" "bear" "+"))
If the bear is big and the bear is blue then the bear eats the mouse.
((("bear" "is" "big" "+") ("bear" "is" "blue" "+")) -> ("bear" "eats" "mouse" "+"))
If the rabbit eats the cow and the cow is blue then the cow chases the bear.
((("rabbit" "eats" "cow" "+") ("cow" "is" "blue" "+")) -> ("cow" "chases" "bear" "+"))
If someone likes the rabbit and the rabbit likes the mouse then they like the bear.
((("someone" "likes" "rabbit" "+") ("rabbit" "likes" "mouse" "+")) -> ("someone" "likes" "bear" "+"))
If someone eats the mouse then they eat the cow.
((("someone" "eats" "mouse" "+")) -> ("someone" "eats" "cow" "+"))
The cow is big.
True
1
proof
[(triple2)]
("cow" "is" "big" "+")
triple2
The bear does not like the rabbit.
False
1
inv-proof
[(triple1)]
("bear" "likes" "rabbit" "-")
triple1
The cow eats the mouse.
True
2
proof
[(((triple3) -> rule3))]
("cow" "eats" "mouse" "+")
((triple3) -> (rule3 % int1))
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int1
The cow does not eat the mouse.
False
2
inv-proof
[(((triple3) -> rule3))]
("cow" "eats" "mouse" "-")
((triple3) -> (rule3 % int1))
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int1
The cow eats the cow.
True
3
proof
[(((((triple3) -> rule3)) -> rule8))]
("cow" "eats" "cow" "+")
((((triple3) -> (rule3 % int2))) -> (rule8 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int2
The cow does not eat the cow.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule8))]
("cow" "eats" "cow" "-")
((((triple3) -> (rule3 % int2))) -> (rule8 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int2
The cow likes the bear.
True
4
proof
[(((((((triple3) -> rule3)) -> rule8)) -> rule4))]
("cow" "likes" "bear" "+")
((((((triple3) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The cow likes the bear.
("cow" "likes" "bear" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int3
The cow does not like the bear.
False
4
inv-proof
[(((((((triple3) -> rule3)) -> rule8)) -> rule4))]
("cow" "likes" "bear" "-")
((((((triple3) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The cow likes the bear.
("cow" "likes" "bear" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int3
The bear does not eat the cow.
Unknown
inv-rconc
[@2: The bear eats the cow.[CWA. Example of deepest failure = (rule8 <- rule5 <- FAIL)]]
("bear" "eats" "cow" "-")
The bear eats the mouse.
Unknown
rconc
[@1: The bear eats the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "eats" "mouse" "+")
The rabbit is not rough.
Unknown
inv-rconc
[@1: The rabbit is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "rough" "-")
The rabbit likes the bear.
Unknown
rconc
[@2: The rabbit likes the bear.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("rabbit" "likes" "bear" "+")
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
The bear is not nice.
Unknown
inv-random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "-")
The bear likes the mouse.
Unknown
random
[@0: The bear likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "mouse" "+")
@0: The bear likes the rabbit.[(triple1)] The cow is big.[(triple2)] The mouse likes the cow.[(triple3)] The rabbit is blue.[(triple4)] @1: The cow eats the mouse.[(((triple3) -> rule3))] @2: The cow eats the cow.[(((((triple3) -> rule3)) -> rule8))] @3: The cow likes the bear.[(((((((triple3) -> rule3)) -> rule8)) -> rule4))]
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
triple1
The cow is big.
("cow" "is" "big" "+")
triple2
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple3
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple4
The cow eats the mouse.
("cow" "eats" "mouse" "+")
((triple3) -> (rule3 % int1))
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
((((triple3) -> (rule3 % int2))) -> (rule8 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int2
The cow likes the bear.
("cow" "likes" "bear" "+")
((((((triple3) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The cow likes the bear.
("cow" "likes" "bear" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int3