The bear chases the mouse. The bear is cold. The bear visits the lion. The lion chases the bear. The lion chases the mouse. The lion is red. The lion likes the mouse. The lion visits the bear. The mouse is big. The mouse likes the bear. If someone likes the lion and the lion is big then the lion visits the mouse. If someone visits the lion and they visit the bear then they chase the bear. If the bear likes the mouse and the bear chases the lion then the mouse chases the lion. If the mouse is young and the mouse is cold then the mouse chases the lion. If someone is red then they visit the mouse. If someone chases the mouse then they are young. If the mouse is young then the mouse likes the lion. If the mouse is big then the mouse is young.
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear visits the lion.
("bear" "visits" "lion" "+")
The lion chases the bear.
("lion" "chases" "bear" "+")
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion is red.
("lion" "is" "red" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion visits the bear.
("lion" "visits" "bear" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
If someone likes the lion and the lion is big then the lion visits the mouse.
((("someone" "likes" "lion" "+") ("lion" "is" "big" "+")) -> ("lion" "visits" "mouse" "+"))
If someone visits the lion and they visit the bear then they chase the bear.
((("someone" "visits" "lion" "+") ("someone" "visits" "bear" "+")) -> ("someone" "chases" "bear" "+"))
If the bear likes the mouse and the bear chases the lion then the mouse chases the lion.
((("bear" "likes" "mouse" "+") ("bear" "chases" "lion" "+")) -> ("mouse" "chases" "lion" "+"))
If the mouse is young and the mouse is cold then the mouse chases the lion.
((("mouse" "is" "young" "+") ("mouse" "is" "cold" "+")) -> ("mouse" "chases" "lion" "+"))
If someone is red then they visit the mouse.
((("someone" "is" "red" "+")) -> ("someone" "visits" "mouse" "+"))
If someone chases the mouse then they are young.
((("someone" "chases" "mouse" "+")) -> ("someone" "is" "young" "+"))
If the mouse is young then the mouse likes the lion.
((("mouse" "is" "young" "+")) -> ("mouse" "likes" "lion" "+"))
If the mouse is big then the mouse is young.
((("mouse" "is" "big" "+")) -> ("mouse" "is" "young" "+"))
The bear is cold.
True
1
proof
[(triple2)]
("bear" "is" "cold" "+")
triple2
The bear does not visit the lion.
False
1
inv-proof
[(triple3)]
("bear" "visits" "lion" "-")
triple3
The lion is young.
True
2
proof
[(((triple5) -> rule6))]
("lion" "is" "young" "+")
((triple5) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion does not visit the mouse.
False
2
inv-proof
[(((triple6) -> rule5))]
("lion" "visits" "mouse" "-")
((triple6) -> (rule5 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The mouse likes the lion.
True
3
proof
[(((((triple9) -> rule8)) -> rule7))]
("mouse" "likes" "lion" "+")
((((triple9) -> (rule8 % int2))) -> (rule7 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse does not like the lion.
False
3
inv-proof
[(((((triple9) -> rule8)) -> rule7))]
("mouse" "likes" "lion" "-")
((((triple9) -> (rule8 % int2))) -> (rule7 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse does not chase the bear.
Unknown
inv-rconc
[@1: The mouse chases the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "chases" "bear" "-")
The bear chases the bear.
Unknown
rconc
[@1: The bear chases the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "chases" "bear" "+")
The mouse does not visit the mouse.
Unknown
inv-rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "visits" "mouse" "-")
The bear likes the lion.
Unknown
random
[@0: The bear likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "lion" "+")
The mouse is not red.
Unknown
inv-random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
@0: The bear chases the mouse.[(triple1)] The bear is cold.[(triple2)] The bear visits the lion.[(triple3)] The lion chases the bear.[(triple4)] The lion chases the mouse.[(triple5)] The lion is red.[(triple6)] The lion likes the mouse.[(triple7)] The lion visits the bear.[(triple8)] The mouse is big.[(triple9)] The mouse likes the bear.[(triple10)] @1: The bear is young.[(((triple1) -> rule6))] The lion is young.[(((triple5) -> rule6))] The lion visits the mouse.[(((triple6) -> rule5))] The mouse is young.[(((triple9) -> rule8))] @2: The mouse likes the lion.[(((((triple9) -> rule8)) -> rule7))]
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple1
The bear is cold.
("bear" "is" "cold" "+")
triple2
The bear visits the lion.
("bear" "visits" "lion" "+")
triple3
The lion chases the bear.
("lion" "chases" "bear" "+")
triple4
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple5
The lion is red.
("lion" "is" "red" "+")
triple6
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple7
The lion visits the bear.
("lion" "visits" "bear" "+")
triple8
The mouse is big.
("mouse" "is" "big" "+")
triple9
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple10
The bear is young.
("bear" "is" "young" "+")
((triple1) -> (rule6 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The lion is young.
("lion" "is" "young" "+")
((triple5) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion visits the mouse.
("lion" "visits" "mouse" "+")
((triple6) -> (rule5 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
((triple9) -> (rule8 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
((((triple9) -> (rule8 % int2))) -> (rule7 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2