The lion is big. The lion needs the mouse. The lion sees the mouse. The mouse is nice. The mouse likes the lion. The mouse needs the lion. The mouse does not see the lion. If something sees the lion and the lion does not need the mouse then it is red. If something sees the lion then it likes the mouse. If something is blue and it does not need the mouse then it sees the lion. If something sees the mouse and the mouse needs the lion then it sees the lion. If something sees the lion and it sees the mouse then the lion is green. If something likes the mouse then the mouse likes the lion. If something needs the mouse then the mouse likes the lion. If the lion does not like the mouse then the mouse likes the lion.
The lion is big.
("lion" "is" "big" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The mouse does not see the lion.
("mouse" "sees" "lion" "-")
If something sees the lion and the lion does not need the mouse then it is red.
((("something" "sees" "lion" "+") ("lion" "needs" "mouse" "~")) -> ("something" "is" "red" "+"))
If something sees the lion then it likes the mouse.
((("something" "sees" "lion" "+")) -> ("something" "likes" "mouse" "+"))
If something is blue and it does not need the mouse then it sees the lion.
((("something" "is" "blue" "+") ("something" "needs" "mouse" "~")) -> ("something" "sees" "lion" "+"))
If something sees the mouse and the mouse needs the lion then it sees the lion.
((("something" "sees" "mouse" "+") ("mouse" "needs" "lion" "+")) -> ("something" "sees" "lion" "+"))
If something sees the lion and it sees the mouse then the lion is green.
((("something" "sees" "lion" "+") ("something" "sees" "mouse" "+")) -> ("lion" "is" "green" "+"))
If something likes the mouse then the mouse likes the lion.
((("something" "likes" "mouse" "+")) -> ("mouse" "likes" "lion" "+"))
If something needs the mouse then the mouse likes the lion.
((("something" "needs" "mouse" "+")) -> ("mouse" "likes" "lion" "+"))
If the lion does not like the mouse then the mouse likes the lion.
((("lion" "likes" "mouse" "~")) -> ("mouse" "likes" "lion" "+"))
The lion sees the mouse.
True
1
proof
[(triple3)]
("lion" "sees" "mouse" "+")
triple3
The mouse is not nice.
False
1
inv-proof
[(triple4)]
("mouse" "is" "nice" "-")
triple4
The mouse is not red.
Unknown
inv-rconc
[@1: The mouse is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "red" "-")
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 big.[(triple1)] The lion needs the mouse.[(triple2)] The lion sees the mouse.[(triple3)] The mouse does not see the lion.[(triple7)] The mouse is nice.[(triple4)] The mouse likes the lion.[(triple5 OR ((triple2) -> rule7) OR ((((((triple3 triple6) -> rule4)) -> rule2)) -> rule6))] The mouse needs the lion.[(triple6)] @1: The lion sees the lion.[(((triple3 triple6) -> rule4))] @2: The lion is green.[(((((triple3 triple6) -> rule4) triple3) -> rule5))] The lion likes the mouse.[(((((triple3 triple6) -> rule4)) -> rule2))]
The lion is big.
("lion" "is" "big" "+")
triple1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple2
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple3
The mouse does not see the lion.
("mouse" "sees" "lion" "-")
triple7
The mouse is nice.
("mouse" "is" "nice" "+")
triple4
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple5
((triple2) -> (rule7 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
((((((triple3 triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int2
The lion sees the lion.
("lion" "sees" "lion" "+")
int3
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple6
The lion sees the lion.
("lion" "sees" "lion" "+")
((triple3 triple6) -> (rule4 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion is green.
("lion" "is" "green" "+")
((((triple3 triple6) -> (rule4 % int2)) triple3) -> (rule5 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
((((triple3 triple6) -> (rule4 % int2))) -> (rule2 % int1))
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2