The lion chases the mouse. The lion eats the mouse. The lion is kind. The lion visits the mouse. The mouse does not chase the lion. The mouse eats the lion. The mouse is big. The mouse is blue. The mouse is young. The mouse visits the lion. If someone chases the mouse and the mouse eats the lion then the mouse is big. If someone eats the lion and the lion is young then the lion is kind. If someone chases the mouse then they are not cold. If the mouse visits the lion and the lion does not visit the mouse then the lion chases the mouse. If someone eats the lion and they eat the mouse then the mouse is kind. If the mouse chases the lion then the lion is cold.
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion eats the mouse.
("lion" "eats" "mouse" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse does not chase the lion.
("mouse" "chases" "lion" "-")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
If someone chases the mouse and the mouse eats the lion then the mouse is big.
((("someone" "chases" "mouse" "+") ("mouse" "eats" "lion" "+")) -> ("mouse" "is" "big" "+"))
If someone eats the lion and the lion is young then the lion is kind.
((("someone" "eats" "lion" "+") ("lion" "is" "young" "+")) -> ("lion" "is" "kind" "+"))
If someone chases the mouse then they are not cold.
((("someone" "chases" "mouse" "+")) -> ("someone" "is" "cold" "-"))
If the mouse visits the lion and the lion does not visit the mouse then the lion chases the mouse.
((("mouse" "visits" "lion" "+") ("lion" "visits" "mouse" "~")) -> ("lion" "chases" "mouse" "+"))
If someone eats the lion and they eat the mouse then the mouse is kind.
((("someone" "eats" "lion" "+") ("someone" "eats" "mouse" "+")) -> ("mouse" "is" "kind" "+"))
If the mouse chases the lion then the lion is cold.
((("mouse" "chases" "lion" "+")) -> ("lion" "is" "cold" "+"))
The mouse is big.
True
1
proof
[(triple7 OR ((triple1 triple6) -> rule1))]
("mouse" "is" "big" "+")
triple7
((triple1 triple6) -> (rule1 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse does not visit the lion.
False
1
inv-proof
[(triple10)]
("mouse" "visits" "lion" "-")
triple10
The mouse is not kind.
Unknown
inv-rconc
[@1: The mouse is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "kind" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
@0: The lion chases the mouse.[(triple1)] The lion eats the mouse.[(triple2)] The lion is kind.[(triple3)] The lion visits the mouse.[(triple4)] The mouse does not chase the lion.[(triple5)] The mouse eats the lion.[(triple6)] The mouse is big.[(triple7 OR ((triple1 triple6) -> rule1))] The mouse is blue.[(triple8)] The mouse is young.[(triple9)] The mouse visits the lion.[(triple10)] @1: The lion is not cold.[(((triple1) -> rule3))]
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple1
The lion eats the mouse.
("lion" "eats" "mouse" "+")
triple2
The lion is kind.
("lion" "is" "kind" "+")
triple3
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple4
The mouse does not chase the lion.
("mouse" "chases" "lion" "-")
triple5
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple6
The mouse is big.
("mouse" "is" "big" "+")
triple7
((triple1 triple6) -> (rule1 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
triple8
The mouse is young.
("mouse" "is" "young" "+")
triple9
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple10
The lion is not cold.
("lion" "is" "cold" "-")
((triple1) -> (rule3 % int1))
The lion is not cold.
("lion" "is" "cold" "-")
int1