The cow likes the mouse. The cow likes the rabbit. The cow needs the rabbit. The mouse eats the cow. The mouse is nice. The mouse is rough. The mouse needs the cow. The rabbit eats the cow. The rabbit eats the mouse. The rabbit is blue. The rabbit is nice. The rabbit likes the mouse. If something likes the cow and it is rough then the cow likes the mouse. If the mouse is nice then the mouse likes the cow. If something eats the mouse and the mouse needs the rabbit then the rabbit needs the mouse. If something eats the rabbit then the rabbit needs the mouse. If something eats the mouse then it eats the rabbit. If something needs the cow then the cow eats the mouse.
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
If something likes the cow and it is rough then the cow likes the mouse.
((("something" "likes" "cow" "+") ("something" "is" "rough" "+")) -> ("cow" "likes" "mouse" "+"))
If the mouse is nice then the mouse likes the cow.
((("mouse" "is" "nice" "+")) -> ("mouse" "likes" "cow" "+"))
If something eats the mouse and the mouse needs the rabbit then the rabbit needs the mouse.
((("something" "eats" "mouse" "+") ("mouse" "needs" "rabbit" "+")) -> ("rabbit" "needs" "mouse" "+"))
If something eats the rabbit then the rabbit needs the mouse.
((("something" "eats" "rabbit" "+")) -> ("rabbit" "needs" "mouse" "+"))
If something eats the mouse then it eats the rabbit.
((("something" "eats" "mouse" "+")) -> ("something" "eats" "rabbit" "+"))
If something needs the cow then the cow eats the mouse.
((("something" "needs" "cow" "+")) -> ("cow" "eats" "mouse" "+"))
The cow needs the rabbit.
True
1
proof
[(triple3)]
("cow" "needs" "rabbit" "+")
triple3
The mouse is not rough.
False
1
inv-proof
[(triple6)]
("mouse" "is" "rough" "-")
triple6
The cow eats the mouse.
True
2
proof
[(((triple7) -> rule6))]
("cow" "eats" "mouse" "+")
((triple7) -> (rule6 % int1))
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int1
The cow does not eat the mouse.
False
2
inv-proof
[(((triple7) -> rule6))]
("cow" "eats" "mouse" "-")
((triple7) -> (rule6 % int1))
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int1
The mouse does not eat the rabbit.
Unknown
inv-rconc
[@1: The mouse eats the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "eats" "rabbit" "-")
The mouse needs the rabbit.
Unknown
random
[@0: The mouse needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "rabbit" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
@0: The cow likes the mouse.[(triple1 OR ((((triple5) -> rule2) triple6) -> rule1))] The cow likes the rabbit.[(triple2)] The cow needs the rabbit.[(triple3)] The mouse eats the cow.[(triple4)] The mouse is nice.[(triple5)] The mouse is rough.[(triple6)] The mouse needs the cow.[(triple7)] The rabbit eats the cow.[(triple8)] The rabbit eats the mouse.[(triple9)] The rabbit is blue.[(triple10)] The rabbit is nice.[(triple11)] The rabbit likes the mouse.[(triple12)] @1: The cow eats the mouse.[(((triple7) -> rule6))] The mouse likes the cow.[(((triple5) -> rule2))] The rabbit eats the rabbit.[(((triple9) -> rule5))] @2: The cow eats the rabbit.[(((((triple7) -> rule6)) -> rule5))] The rabbit needs the mouse.[(((((triple9) -> rule5)) -> rule4) OR ((((((triple7) -> rule6)) -> rule5)) -> rule4))]
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple1
((((triple5) -> (rule2 % int2)) triple6) -> (rule1 % int1))
The cow likes the mouse.
("cow" "likes" "mouse" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
triple2
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
triple3
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple4
The mouse is nice.
("mouse" "is" "nice" "+")
triple5
The mouse is rough.
("mouse" "is" "rough" "+")
triple6
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple7
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
triple8
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple9
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple10
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple11
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple12
The cow eats the mouse.
("cow" "eats" "mouse" "+")
((triple7) -> (rule6 % int1))
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
((triple5) -> (rule2 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((triple9) -> (rule5 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
((((triple7) -> (rule6 % int2))) -> (rule5 % int1))
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int2
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
((((triple9) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
((((((triple7) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int2
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int3