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