The lion sees the mouse. The mouse likes the rabbit. The rabbit is green. The tiger is not kind. If the rabbit does not like the tiger then the rabbit does not see the mouse. If something likes the rabbit then the rabbit chases the mouse. If something chases the rabbit then it likes the lion. If something sees the rabbit then it sees the mouse. If the tiger chases the rabbit and the tiger is green then the rabbit sees the lion. If something chases the mouse then the mouse chases the rabbit. If something sees the mouse then the mouse is rough. If something likes the rabbit and it does not see the mouse then it is not rough.
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The tiger is not kind.
("tiger" "is" "kind" "-")
If the rabbit does not like the tiger then the rabbit does not see the mouse.
((("rabbit" "likes" "tiger" "~")) -> ("rabbit" "sees" "mouse" "-"))
If something likes the rabbit then the rabbit chases the mouse.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "chases" "mouse" "+"))
If something chases the rabbit then it likes the lion.
((("something" "chases" "rabbit" "+")) -> ("something" "likes" "lion" "+"))
If something sees the rabbit then it sees the mouse.
((("something" "sees" "rabbit" "+")) -> ("something" "sees" "mouse" "+"))
If the tiger chases the rabbit and the tiger is green then the rabbit sees the lion.
((("tiger" "chases" "rabbit" "+") ("tiger" "is" "green" "+")) -> ("rabbit" "sees" "lion" "+"))
If something chases the mouse then the mouse chases the rabbit.
((("something" "chases" "mouse" "+")) -> ("mouse" "chases" "rabbit" "+"))
If something sees the mouse then the mouse is rough.
((("something" "sees" "mouse" "+")) -> ("mouse" "is" "rough" "+"))
If something likes the rabbit and it does not see the mouse then it is not rough.
((("something" "likes" "rabbit" "+") ("something" "sees" "mouse" "~")) -> ("something" "is" "rough" "-"))
The mouse likes the rabbit.
True
1
proof
[(triple2)]
("mouse" "likes" "rabbit" "+")
triple2
The rabbit is not green.
False
1
inv-proof
[(triple3)]
("rabbit" "is" "green" "-")
triple3
The rabbit chases the mouse.
True
2
proof
[(((triple2) -> rule2))]
("rabbit" "chases" "mouse" "+")
((triple2) -> (rule2 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The mouse is not rough.
False
2
inv-proof
[(((triple1) -> rule7))]
("mouse" "is" "rough" "-")
((triple1) -> (rule7 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse chases the rabbit.
True
3
proof
[(((((triple2) -> rule2)) -> rule6))]
("mouse" "chases" "rabbit" "+")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int2
The mouse does not chase the rabbit.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule6))]
("mouse" "chases" "rabbit" "-")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int2
The mouse likes the lion.
True
4
proof
[(((((((triple2) -> rule2)) -> rule6)) -> rule3))]
("mouse" "likes" "lion" "+")
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int2
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int3
The mouse does not like the lion.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule6)) -> rule3))]
("mouse" "likes" "lion" "-")
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int2
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int3
The rabbit does not see the lion.
Unknown
inv-rconc
[@1: The rabbit sees the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "sees" "lion" "-")
The rabbit sees the mouse.
Unknown
rconc
[@1: The rabbit sees the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "sees" "mouse" "+")
The tiger does not see the mouse.
Unknown
inv-rconc
[@1: The tiger sees the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "sees" "mouse" "-")
The mouse sees the mouse.
Unknown
rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "sees" "mouse" "+")
The lion does not chase the tiger.
Unknown
inv-random
[@0: The lion chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "tiger" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
The mouse is not green.
Unknown
inv-random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "-")
The lion is green.
Unknown
random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "+")
@0: The lion sees the mouse.[(triple1)] The mouse likes the rabbit.[(triple2)] The rabbit is green.[(triple3)] The tiger is not kind.[(triple4)] @1: The mouse is rough.[(((triple1) -> rule7))] The rabbit chases the mouse.[(((triple2) -> rule2))] @2: The mouse chases the rabbit.[(((((triple2) -> rule2)) -> rule6))] @3: The mouse likes the lion.[(((((((triple2) -> rule2)) -> rule6)) -> rule3))]
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple2
The rabbit is green.
("rabbit" "is" "green" "+")
triple3
The tiger is not kind.
("tiger" "is" "kind" "-")
triple4
The mouse is rough.
("mouse" "is" "rough" "+")
((triple1) -> (rule7 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
((triple2) -> (rule2 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int2
The mouse likes the lion.
("mouse" "likes" "lion" "+")
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int2
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int3