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