The cat eats the mouse. The cat is red. The cat is young. The lion chases the cat. The mouse chases the lion. The mouse likes the cat. The mouse likes the lion. If the cat chases the lion then the lion is rough. If something likes the lion then the lion chases the mouse.
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is young.
("cat" "is" "young" "+")
The lion chases the cat.
("lion" "chases" "cat" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
If the cat chases the lion then the lion is rough.
((("cat" "chases" "lion" "+")) -> ("lion" "is" "rough" "+"))
If something likes the lion then the lion chases the mouse.
((("something" "likes" "lion" "+")) -> ("lion" "chases" "mouse" "+"))
The lion chases the cat.
True
1
proof
[(triple4)]
("lion" "chases" "cat" "+")
triple4
The mouse does not like the lion.
False
1
inv-proof
[(triple7)]
("mouse" "likes" "lion" "-")
triple7
The lion chases the mouse.
True
2
proof
[(((triple7) -> rule2))]
("lion" "chases" "mouse" "+")
((triple7) -> (rule2 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The lion does not chase the mouse.
False
2
inv-proof
[(((triple7) -> rule2))]
("lion" "chases" "mouse" "-")
((triple7) -> (rule2 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The lion is not rough.
Unknown
inv-rconc
[@1: The lion is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "rough" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
The mouse does not chase the cat.
Unknown
inv-random
[@0: The mouse chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "cat" "-")
The mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
@0: The cat eats the mouse.[(triple1)] The cat is red.[(triple2)] The cat is young.[(triple3)] The lion chases the cat.[(triple4)] The mouse chases the lion.[(triple5)] The mouse likes the cat.[(triple6)] The mouse likes the lion.[(triple7)] @1: The lion chases the mouse.[(((triple7) -> rule2))]
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple1
The cat is red.
("cat" "is" "red" "+")
triple2
The cat is young.
("cat" "is" "young" "+")
triple3
The lion chases the cat.
("lion" "chases" "cat" "+")
triple4
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple5
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple6
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple7
The lion chases the mouse.
("lion" "chases" "mouse" "+")
((triple7) -> (rule2 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1