The cow chases the mouse. The cow eats the lion. The cow likes the rabbit. The lion chases the mouse. The lion chases the rabbit. The lion is not kind. The lion is young. The mouse chases the rabbit. The mouse is cold. The mouse is nice. The rabbit chases the lion. The rabbit eats the cow. The rabbit is kind. The rabbit is young. The rabbit does not like the cow. The rabbit likes the lion. If something chases the mouse then it eats the mouse. If something eats the mouse then the mouse does not like the lion. If something eats the cow then the cow eats the rabbit.
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The cow eats the lion.
("cow" "eats" "lion" "+")
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion is not kind.
("lion" "is" "kind" "-")
The lion is young.
("lion" "is" "young" "+")
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit does not like the cow.
("rabbit" "likes" "cow" "-")
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
If something chases the mouse then it eats the mouse.
((("something" "chases" "mouse" "+")) -> ("something" "eats" "mouse" "+"))
If something eats the mouse then the mouse does not like the lion.
((("something" "eats" "mouse" "+")) -> ("mouse" "likes" "lion" "-"))
If something eats the cow then the cow eats the rabbit.
((("something" "eats" "cow" "+")) -> ("cow" "eats" "rabbit" "+"))
The mouse is cold.
True
1
proof
[(triple9)]
("mouse" "is" "cold" "+")
triple9
The rabbit does not chase the lion.
False
1
inv-proof
[(triple11)]
("rabbit" "chases" "lion" "-")
triple11
The lion eats the mouse.
True
2
proof
[(((triple4) -> rule1))]
("lion" "eats" "mouse" "+")
((triple4) -> (rule1 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The lion does not eat the mouse.
False
2
inv-proof
[(((triple4) -> rule1))]
("lion" "eats" "mouse" "-")
((triple4) -> (rule1 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The mouse does not like the lion.
True
3
proof
[(((((triple1) -> rule1)) -> rule2) OR ((((triple4) -> rule1)) -> rule2))]
("mouse" "likes" "lion" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The mouse does not like the lion.
("mouse" "likes" "lion" "-")
int1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int2
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The mouse does not like the lion.
("mouse" "likes" "lion" "-")
int1
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int2
The mouse likes the lion.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2) OR ((((triple4) -> rule1)) -> rule2))]
("mouse" "likes" "lion" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The mouse does not like the lion.
("mouse" "likes" "lion" "-")
int1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int2
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The mouse does not like the lion.
("mouse" "likes" "lion" "-")
int1
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int2
The rabbit does not eat the mouse.
Unknown
inv-rconc
[@1: The rabbit eats the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "eats" "mouse" "-")
The mouse eats the mouse.
Unknown
rconc
[@1: The mouse eats the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "eats" "mouse" "+")
The rabbit is not cold.
Unknown
inv-random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "-")
The rabbit is nice.
Unknown
random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "+")
The mouse does not eat the lion.
Unknown
inv-random
[@0: The mouse eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "lion" "-")
The lion likes the cow.
Unknown
random
[@0: The lion likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "cow" "+")
@0: The cow chases the mouse.[(triple1)] The cow eats the lion.[(triple2)] The cow likes the rabbit.[(triple3)] The lion chases the mouse.[(triple4)] The lion chases the rabbit.[(triple5)] The lion is not kind.[(triple6)] The lion is young.[(triple7)] The mouse chases the rabbit.[(triple8)] The mouse is cold.[(triple9)] The mouse is nice.[(triple10)] The rabbit chases the lion.[(triple11)] The rabbit does not like the cow.[(triple15)] The rabbit eats the cow.[(triple12)] The rabbit is kind.[(triple13)] The rabbit is young.[(triple14)] The rabbit likes the lion.[(triple16)] @1: The cow eats the mouse.[(((triple1) -> rule1))] The cow eats the rabbit.[(((triple12) -> rule3))] The lion eats the mouse.[(((triple4) -> rule1))] @2: The mouse does not like the lion.[(((((triple1) -> rule1)) -> rule2) OR ((((triple4) -> rule1)) -> rule2))]
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple1
The cow eats the lion.
("cow" "eats" "lion" "+")
triple2
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
triple3
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple4
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple5
The lion is not kind.
("lion" "is" "kind" "-")
triple6
The lion is young.
("lion" "is" "young" "+")
triple7
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple8
The mouse is cold.
("mouse" "is" "cold" "+")
triple9
The mouse is nice.
("mouse" "is" "nice" "+")
triple10
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple11
The rabbit does not like the cow.
("rabbit" "likes" "cow" "-")
triple15
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
triple12
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple13
The rabbit is young.
("rabbit" "is" "young" "+")
triple14
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
triple16
The cow eats the mouse.
("cow" "eats" "mouse" "+")
((triple1) -> (rule1 % int1))
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
((triple12) -> (rule3 % int1))
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int1
The lion eats the mouse.
("lion" "eats" "mouse" "+")
((triple4) -> (rule1 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The mouse does not like the lion.
("mouse" "likes" "lion" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The mouse does not like the lion.
("mouse" "likes" "lion" "-")
int1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int2
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The mouse does not like the lion.
("mouse" "likes" "lion" "-")
int1
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int2