The bear likes the mouse. The cat chases the lion. The lion sees the bear. The mouse chases the cat. If something chases the bear then the bear likes the lion. If something chases the lion then the lion sees the bear. If something is round then it chases the lion. If something likes the lion and it is big then the lion sees the bear. If something chases the cat then the cat likes the mouse. If something chases the lion and it chases the mouse then the lion is big. If something likes the lion then the lion likes the cat. If something likes the bear and it chases the lion then the bear chases the cat.
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The cat chases the lion.
("cat" "chases" "lion" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
If something chases the bear then the bear likes the lion.
((("something" "chases" "bear" "+")) -> ("bear" "likes" "lion" "+"))
If something chases the lion then the lion sees the bear.
((("something" "chases" "lion" "+")) -> ("lion" "sees" "bear" "+"))
If something is round then it chases the lion.
((("something" "is" "round" "+")) -> ("something" "chases" "lion" "+"))
If something likes the lion and it is big then the lion sees the bear.
((("something" "likes" "lion" "+") ("something" "is" "big" "+")) -> ("lion" "sees" "bear" "+"))
If something chases the cat then the cat likes the mouse.
((("something" "chases" "cat" "+")) -> ("cat" "likes" "mouse" "+"))
If something chases the lion and it chases the mouse then the lion is big.
((("something" "chases" "lion" "+") ("something" "chases" "mouse" "+")) -> ("lion" "is" "big" "+"))
If something likes the lion then the lion likes the cat.
((("something" "likes" "lion" "+")) -> ("lion" "likes" "cat" "+"))
If something likes the bear and it chases the lion then the bear chases the cat.
((("something" "likes" "bear" "+") ("something" "chases" "lion" "+")) -> ("bear" "chases" "cat" "+"))
The lion sees the bear.
True
1
proof
[(triple3 OR ((triple2) -> rule2))]
("lion" "sees" "bear" "+")
triple3
((triple2) -> (rule2 % int1))
The lion sees the bear.
("lion" "sees" "bear" "+")
int1
The bear does not like the mouse.
False
1
inv-proof
[(triple1)]
("bear" "likes" "mouse" "-")
triple1
The cat likes the mouse.
True
2
proof
[(((triple4) -> rule5))]
("cat" "likes" "mouse" "+")
((triple4) -> (rule5 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat does not like the mouse.
False
2
inv-proof
[(((triple4) -> rule5))]
("cat" "likes" "mouse" "-")
((triple4) -> (rule5 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The bear does not chase the lion.
Unknown
inv-rconc
[@1: The bear chases the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "chases" "lion" "-")
The mouse chases the lion.
Unknown
rconc
[@1: The mouse chases the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "chases" "lion" "+")
The mouse does not see the bear.
Unknown
inv-random
[@0: The mouse sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "bear" "-")
The bear is nice.
Unknown
random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "+")
@0: The bear likes the mouse.[(triple1)] The cat chases the lion.[(triple2)] The lion sees the bear.[(triple3 OR ((triple2) -> rule2))] The mouse chases the cat.[(triple4)] @1: The cat likes the mouse.[(((triple4) -> rule5))]
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple1
The cat chases the lion.
("cat" "chases" "lion" "+")
triple2
The lion sees the bear.
("lion" "sees" "bear" "+")
triple3
((triple2) -> (rule2 % int1))
The lion sees the bear.
("lion" "sees" "bear" "+")
int1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple4
The cat likes the mouse.
("cat" "likes" "mouse" "+")
((triple4) -> (rule5 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1