The dog is young. The lion likes the mouse. The mouse sees the dog. If the dog sees the mouse and the mouse likes the dog then the mouse chases the dog. If the dog is nice and the lion does not see the dog then the dog sees the lion. If someone sees the lion then the lion chases the mouse. If the dog sees the lion and the dog likes the mouse then the lion does not chase the mouse. If the lion is round and the lion does not see the mouse then the lion does not like the dog. If the dog sees the lion and the dog likes the lion then the lion likes the dog. If someone likes the mouse then they see the lion. If someone chases the dog and they are nice then they like the mouse.
The dog is young.
("dog" "is" "young" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
If the dog sees the mouse and the mouse likes the dog then the mouse chases the dog.
((("dog" "sees" "mouse" "+") ("mouse" "likes" "dog" "+")) -> ("mouse" "chases" "dog" "+"))
If the dog is nice and the lion does not see the dog then the dog sees the lion.
((("dog" "is" "nice" "+") ("lion" "sees" "dog" "~")) -> ("dog" "sees" "lion" "+"))
If someone sees the lion then the lion chases the mouse.
((("someone" "sees" "lion" "+")) -> ("lion" "chases" "mouse" "+"))
If the dog sees the lion and the dog likes the mouse then the lion does not chase the mouse.
((("dog" "sees" "lion" "+") ("dog" "likes" "mouse" "+")) -> ("lion" "chases" "mouse" "-"))
If the lion is round and the lion does not see the mouse then the lion does not like the dog.
((("lion" "is" "round" "+") ("lion" "sees" "mouse" "~")) -> ("lion" "likes" "dog" "-"))
If the dog sees the lion and the dog likes the lion then the lion likes the dog.
((("dog" "sees" "lion" "+") ("dog" "likes" "lion" "+")) -> ("lion" "likes" "dog" "+"))
If someone likes the mouse then they see the lion.
((("someone" "likes" "mouse" "+")) -> ("someone" "sees" "lion" "+"))
If someone chases the dog and they are nice then they like the mouse.
((("someone" "chases" "dog" "+") ("someone" "is" "nice" "+")) -> ("someone" "likes" "mouse" "+"))
The mouse sees the dog.
True
1
proof
[(triple3)]
("mouse" "sees" "dog" "+")
triple3
The dog is not young.
False
1
inv-proof
[(triple1)]
("dog" "is" "young" "-")
triple1
The lion sees the lion.
True
2
proof
[(((triple2) -> rule7))]
("lion" "sees" "lion" "+")
((triple2) -> (rule7 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion does not see the lion.
False
2
inv-proof
[(((triple2) -> rule7))]
("lion" "sees" "lion" "-")
((triple2) -> (rule7 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion chases the mouse.
True
3
proof
[(((((triple2) -> rule7)) -> rule3))]
("lion" "chases" "mouse" "+")
((((triple2) -> (rule7 % int2))) -> (rule3 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2
The lion does not chase the mouse.
False
3
inv-proof
[(((((triple2) -> rule7)) -> rule3))]
("lion" "chases" "mouse" "-")
((((triple2) -> (rule7 % int2))) -> (rule3 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2
The dog does not like the mouse.
Unknown
inv-rconc
[@1: The dog likes the mouse.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "likes" "mouse" "-")
The mouse sees the lion.
Unknown
rconc
[@2: The mouse sees the lion.[CWA. Example of deepest failure = (rule7 <- rule8 <- FAIL)]]
("mouse" "sees" "lion" "+")
The dog does not see the lion.
Unknown
inv-rconc
[@2: The dog sees the lion.[CWA. Example of deepest failure = (rule7 <- rule8 <- FAIL)]]
("dog" "sees" "lion" "-")
The lion sees the dog.
Unknown
random
[@0: The lion sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "dog" "+")
The dog does not like the dog.
Unknown
inv-random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The dog is young.[(triple1)] The lion likes the mouse.[(triple2)] The mouse sees the dog.[(triple3)] @1: The lion sees the lion.[(((triple2) -> rule7))] @2: The lion chases the mouse.[(((((triple2) -> rule7)) -> rule3))]
The dog is young.
("dog" "is" "young" "+")
triple1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple3
The lion sees the lion.
("lion" "sees" "lion" "+")
((triple2) -> (rule7 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
((((triple2) -> (rule7 % int2))) -> (rule3 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2