The bear chases the mouse. The bear is big. The cat chases the bear. The lion chases the cat. The lion chases the mouse. The lion is green. The lion likes the mouse. The lion visits the mouse. The mouse is cold. The mouse visits the bear. If something is rough and it visits the cat then the cat chases the bear. If something is cold then it likes the mouse. If something chases the bear and the bear visits the lion then it likes the lion.
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The bear is big.
("bear" "is" "big" "+")
The cat chases the bear.
("cat" "chases" "bear" "+")
The lion chases the cat.
("lion" "chases" "cat" "+")
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion is green.
("lion" "is" "green" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
If something is rough and it visits the cat then the cat chases the bear.
((("something" "is" "rough" "+") ("something" "visits" "cat" "+")) -> ("cat" "chases" "bear" "+"))
If something is cold then it likes the mouse.
((("something" "is" "cold" "+")) -> ("something" "likes" "mouse" "+"))
If something chases the bear and the bear visits the lion then it likes the lion.
((("something" "chases" "bear" "+") ("bear" "visits" "lion" "+")) -> ("something" "likes" "lion" "+"))
The mouse is cold.
True
1
proof
[(triple9)]
("mouse" "is" "cold" "+")
triple9
The lion does not visit the mouse.
False
1
inv-proof
[(triple8)]
("lion" "visits" "mouse" "-")
triple8
The mouse likes the mouse.
True
2
proof
[(((triple9) -> rule2))]
("mouse" "likes" "mouse" "+")
((triple9) -> (rule2 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse does not like the mouse.
False
2
inv-proof
[(((triple9) -> rule2))]
("mouse" "likes" "mouse" "-")
((triple9) -> (rule2 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The lion does not like the lion.
Unknown
inv-rconc
[@1: The lion likes the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "likes" "lion" "-")
The bear likes the mouse.
Unknown
rconc
[@1: The bear likes the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "likes" "mouse" "+")
The cat does not chase the lion.
Unknown
inv-random
[@0: The cat chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "lion" "-")
The bear visits the lion.
Unknown
random
[@0: The bear visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "lion" "+")
@0: The bear chases the mouse.[(triple1)] The bear is big.[(triple2)] The cat chases the bear.[(triple3)] The lion chases the cat.[(triple4)] The lion chases the mouse.[(triple5)] The lion is green.[(triple6)] The lion likes the mouse.[(triple7)] The lion visits the mouse.[(triple8)] The mouse is cold.[(triple9)] The mouse visits the bear.[(triple10)] @1: The mouse likes the mouse.[(((triple9) -> rule2))]
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple1
The bear is big.
("bear" "is" "big" "+")
triple2
The cat chases the bear.
("cat" "chases" "bear" "+")
triple3
The lion chases the cat.
("lion" "chases" "cat" "+")
triple4
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple5
The lion is green.
("lion" "is" "green" "+")
triple6
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple7
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple8
The mouse is cold.
("mouse" "is" "cold" "+")
triple9
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple10
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((triple9) -> (rule2 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1