The lion eats the mouse. The lion is nice. The lion is round. The lion likes the mouse. The mouse eats the lion. The mouse is blue. The mouse is green. The mouse is nice. The mouse is young. The mouse sees the lion. If something is nice then it eats the lion.
The lion eats the mouse.
("lion" "eats" "mouse" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is round.
("lion" "is" "round" "+")
The lion likes the mouse.
("lion" "likes" "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 nice.
("mouse" "is" "nice" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
If something is nice then it eats the lion.
((("something" "is" "nice" "+")) -> ("something" "eats" "lion" "+"))
The lion is nice.
True
1
proof
[(triple2)]
("lion" "is" "nice" "+")
triple2
The mouse is not nice.
False
1
inv-proof
[(triple8)]
("mouse" "is" "nice" "-")
triple8
The lion eats the lion.
True
2
proof
[(((triple2) -> rule1))]
("lion" "eats" "lion" "+")
((triple2) -> (rule1 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion does not eat the lion.
False
2
inv-proof
[(((triple2) -> rule1))]
("lion" "eats" "lion" "-")
((triple2) -> (rule1 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The lion sees the mouse.
Unknown
random
[@0: The lion sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "mouse" "+")
The lion does not like the lion.
Unknown
inv-random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
@0: The lion eats the mouse.[(triple1)] The lion is nice.[(triple2)] The lion is round.[(triple3)] The lion likes the mouse.[(triple4)] The mouse eats the lion.[(triple5 OR ((triple8) -> rule1))] The mouse is blue.[(triple6)] The mouse is green.[(triple7)] The mouse is nice.[(triple8)] The mouse is young.[(triple9)] The mouse sees the lion.[(triple10)] @1: The lion eats the lion.[(((triple2) -> rule1))]
The lion eats the mouse.
("lion" "eats" "mouse" "+")
triple1
The lion is nice.
("lion" "is" "nice" "+")
triple2
The lion is round.
("lion" "is" "round" "+")
triple3
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple4
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple5
((triple8) -> (rule1 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
triple6
The mouse is green.
("mouse" "is" "green" "+")
triple7
The mouse is nice.
("mouse" "is" "nice" "+")
triple8
The mouse is young.
("mouse" "is" "young" "+")
triple9
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple10
The lion eats the lion.
("lion" "eats" "lion" "+")
((triple2) -> (rule1 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1