The bear is young. The cow is rough. The mouse visits the cow. If someone is rough then they like the mouse. If someone likes the mouse then they like the cow. If someone visits the mouse and the mouse visits the bear then they see the cow. If someone is rough then they see the mouse. If someone sees the mouse then the mouse likes the bear. If the mouse sees the bear and the mouse likes the bear then the mouse visits the cow. If the cow likes the mouse and the mouse is cold then the cow likes the bear. If someone likes the cow and the cow visits the bear then they like the mouse.
The bear is young.
("bear" "is" "young" "+")
The cow is rough.
("cow" "is" "rough" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
If someone is rough then they like the mouse.
((("someone" "is" "rough" "+")) -> ("someone" "likes" "mouse" "+"))
If someone likes the mouse then they like the cow.
((("someone" "likes" "mouse" "+")) -> ("someone" "likes" "cow" "+"))
If someone visits the mouse and the mouse visits the bear then they see the cow.
((("someone" "visits" "mouse" "+") ("mouse" "visits" "bear" "+")) -> ("someone" "sees" "cow" "+"))
If someone is rough then they see the mouse.
((("someone" "is" "rough" "+")) -> ("someone" "sees" "mouse" "+"))
If someone sees the mouse then the mouse likes the bear.
((("someone" "sees" "mouse" "+")) -> ("mouse" "likes" "bear" "+"))
If the mouse sees the bear and the mouse likes the bear then the mouse visits the cow.
((("mouse" "sees" "bear" "+") ("mouse" "likes" "bear" "+")) -> ("mouse" "visits" "cow" "+"))
If the cow likes the mouse and the mouse is cold then the cow likes the bear.
((("cow" "likes" "mouse" "+") ("mouse" "is" "cold" "+")) -> ("cow" "likes" "bear" "+"))
If someone likes the cow and the cow visits the bear then they like the mouse.
((("someone" "likes" "cow" "+") ("cow" "visits" "bear" "+")) -> ("someone" "likes" "mouse" "+"))
The bear is young.
True
1
proof
[(triple1)]
("bear" "is" "young" "+")
triple1
The bear is not young.
False
1
inv-proof
[(triple1)]
("bear" "is" "young" "-")
triple1
The cow sees the mouse.
True
2
proof
[(((triple2) -> rule4))]
("cow" "sees" "mouse" "+")
((triple2) -> (rule4 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The cow does not see the mouse.
False
2
inv-proof
[(((triple2) -> rule4))]
("cow" "sees" "mouse" "-")
((triple2) -> (rule4 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The mouse likes the bear.
True
3
proof
[(((((triple2) -> rule4)) -> rule5))]
("mouse" "likes" "bear" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int2
The mouse does not like the bear.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule5))]
("mouse" "likes" "bear" "-")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int2
The bear does not see the cow.
Unknown
inv-rconc
[@1: The bear sees the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "sees" "cow" "-")
The mouse sees the mouse.
Unknown
rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "sees" "mouse" "+")
The bear does not like the mouse.
Unknown
inv-rconc
[@1: The bear likes the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "likes" "mouse" "-")
The cow visits the mouse.
Unknown
random
[@0: The cow visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "mouse" "+")
The cow is not red.
Unknown
inv-random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
@0: The bear is young.[(triple1)] The cow is rough.[(triple2)] The mouse visits the cow.[(triple3)] @1: The cow likes the mouse.[(((triple2) -> rule1))] The cow sees the mouse.[(((triple2) -> rule4))] @2: The cow likes the cow.[(((((triple2) -> rule1)) -> rule2))] The mouse likes the bear.[(((((triple2) -> rule4)) -> rule5))]
The bear is young.
("bear" "is" "young" "+")
triple1
The cow is rough.
("cow" "is" "rough" "+")
triple2
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple3
The cow likes the mouse.
("cow" "likes" "mouse" "+")
((triple2) -> (rule1 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
((triple2) -> (rule4 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int2
The mouse likes the bear.
("mouse" "likes" "bear" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int2