The lion eats the mouse. The lion is blue. The lion is green. The lion is nice. The lion is red. The lion is round. The lion needs the mouse. The lion visits the mouse. The mouse eats the lion. The mouse is blue. The mouse is green. The mouse is red. The mouse is round. The mouse needs the lion. The mouse visits the lion. If something needs the lion then the lion eats the mouse. If something is blue and red then it needs the mouse. If something is nice and it needs the lion then it eats the lion. If something visits the mouse then it eats the lion. If the lion visits the mouse then the lion is red. If something visits the lion and the lion visits the mouse then the lion needs the mouse.
The lion eats the mouse.
("lion" "eats" "mouse" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is round.
("lion" "is" "round" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
If something needs the lion then the lion eats the mouse.
((("something" "needs" "lion" "+")) -> ("lion" "eats" "mouse" "+"))
If something is blue and red then it needs the mouse.
((("something" "is" "blue" "+") ("something" "is" "red" "+")) -> ("something" "needs" "mouse" "+"))
If something is nice and it needs the lion then it eats the lion.
((("something" "is" "nice" "+") ("something" "needs" "lion" "+")) -> ("something" "eats" "lion" "+"))
If something visits the mouse then it eats the lion.
((("something" "visits" "mouse" "+")) -> ("something" "eats" "lion" "+"))
If the lion visits the mouse then the lion is red.
((("lion" "visits" "mouse" "+")) -> ("lion" "is" "red" "+"))
If something visits the lion and the lion visits the mouse then the lion needs the mouse.
((("something" "visits" "lion" "+") ("lion" "visits" "mouse" "+")) -> ("lion" "needs" "mouse" "+"))
The mouse visits the lion.
True
1
proof
[(triple15)]
("mouse" "visits" "lion" "+")
triple15
The mouse is not blue.
False
1
inv-proof
[(triple10)]
("mouse" "is" "blue" "-")
triple10
The mouse is not nice.
Unknown
inv-random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
@0: The lion eats the mouse.[(triple1 OR ((triple14) -> rule1))] The lion is blue.[(triple2)] The lion is green.[(triple3)] The lion is nice.[(triple4)] The lion is red.[(triple5 OR ((triple8) -> rule5))] The lion is round.[(triple6)] The lion needs the mouse.[(triple7 OR ((triple15 triple8) -> rule6) OR ((triple2 triple5) -> rule2) OR ((triple2 ((triple8) -> rule5)) -> rule2))] The lion visits the mouse.[(triple8)] The mouse eats the lion.[(triple9)] The mouse is blue.[(triple10)] The mouse is green.[(triple11)] The mouse is red.[(triple12)] The mouse is round.[(triple13)] The mouse needs the lion.[(triple14)] The mouse visits the lion.[(triple15)] @1: The lion eats the lion.[(((triple8) -> rule4))] The mouse needs the mouse.[(((triple10 triple12) -> rule2))]
The lion eats the mouse.
("lion" "eats" "mouse" "+")
triple1
((triple14) -> (rule1 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
triple2
The lion is green.
("lion" "is" "green" "+")
triple3
The lion is nice.
("lion" "is" "nice" "+")
triple4
The lion is red.
("lion" "is" "red" "+")
triple5
((triple8) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is round.
("lion" "is" "round" "+")
triple6
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple7
((triple15 triple8) -> (rule6 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
((triple2 triple5) -> (rule2 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
((triple2 ((triple8) -> (rule5 % int2))) -> (rule2 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple8
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple9
The mouse is blue.
("mouse" "is" "blue" "+")
triple10
The mouse is green.
("mouse" "is" "green" "+")
triple11
The mouse is red.
("mouse" "is" "red" "+")
triple12
The mouse is round.
("mouse" "is" "round" "+")
triple13
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple14
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple15
The lion eats the lion.
("lion" "eats" "lion" "+")
((triple8) -> (rule4 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((triple10 triple12) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1