The cat chases the lion. The cat chases the mouse. The cat is big. The cat needs the mouse. The cat visits the lion. The lion chases the mouse. The lion is rough. The mouse chases the cat. The mouse chases the lion. The mouse is cold. The mouse is green. The mouse needs the cat. The mouse needs the lion. The mouse visits the cat. The mouse visits the lion. If someone needs the cat then the cat needs the lion. If someone needs the lion and they are green then the lion chases the mouse. If someone is rough and kind then they chase the cat. If someone needs the mouse then the mouse visits the cat. If the cat chases the mouse then the cat visits the lion. If someone needs the lion then the lion chases the mouse.
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat is big.
("cat" "is" "big" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion is rough.
("lion" "is" "rough" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
If someone needs the cat then the cat needs the lion.
((("someone" "needs" "cat" "+")) -> ("cat" "needs" "lion" "+"))
If someone needs the lion and they are green then the lion chases the mouse.
((("someone" "needs" "lion" "+") ("someone" "is" "green" "+")) -> ("lion" "chases" "mouse" "+"))
If someone is rough and kind then they chase the cat.
((("someone" "is" "rough" "+") ("someone" "is" "kind" "+")) -> ("someone" "chases" "cat" "+"))
If someone needs the mouse then the mouse visits the cat.
((("someone" "needs" "mouse" "+")) -> ("mouse" "visits" "cat" "+"))
If the cat chases the mouse then the cat visits the lion.
((("cat" "chases" "mouse" "+")) -> ("cat" "visits" "lion" "+"))
If someone needs the lion then the lion chases the mouse.
((("someone" "needs" "lion" "+")) -> ("lion" "chases" "mouse" "+"))
The cat visits the lion.
True
1
proof
[(triple5 OR ((triple2) -> rule5))]
("cat" "visits" "lion" "+")
triple5
((triple2) -> (rule5 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The mouse is not green.
False
1
inv-proof
[(triple11)]
("mouse" "is" "green" "-")
triple11
The cat does not chase the cat.
Unknown
inv-rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "chases" "cat" "-")
The cat is cold.
Unknown
random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "+")
@0: The cat chases the lion.[(triple1)] The cat chases the mouse.[(triple2)] The cat is big.[(triple3)] The cat needs the mouse.[(triple4)] The cat visits the lion.[(triple5 OR ((triple2) -> rule5))] The lion chases the mouse.[(triple6 OR ((triple13) -> rule6) OR ((triple13 triple11) -> rule2) OR ((((triple12) -> rule1)) -> rule6))] The lion is rough.[(triple7)] The mouse chases the cat.[(triple8)] The mouse chases the lion.[(triple9)] The mouse is cold.[(triple10)] The mouse is green.[(triple11)] The mouse needs the cat.[(triple12)] The mouse needs the lion.[(triple13)] The mouse visits the cat.[(triple14 OR ((triple4) -> rule4))] The mouse visits the lion.[(triple15)] @1: The cat needs the lion.[(((triple12) -> rule1))]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple2
The cat is big.
("cat" "is" "big" "+")
triple3
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple4
The cat visits the lion.
("cat" "visits" "lion" "+")
triple5
((triple2) -> (rule5 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple6
((triple13) -> (rule6 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
((triple13 triple11) -> (rule2 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
((((triple12) -> (rule1 % int2))) -> (rule6 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
triple7
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple8
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple9
The mouse is cold.
("mouse" "is" "cold" "+")
triple10
The mouse is green.
("mouse" "is" "green" "+")
triple11
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple12
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple13
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple14
((triple4) -> (rule4 % int1))
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int1
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple15
The cat needs the lion.
("cat" "needs" "lion" "+")
((triple12) -> (rule1 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1