The lion chases the mouse. The lion visits the mouse. The mouse chases the lion. If something chases the lion and the lion visits the mouse then it chases the mouse. If something visits the mouse then the mouse likes the lion. If the mouse chases the lion and the mouse likes the lion then the mouse is green.
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
If something chases the lion and the lion visits the mouse then it chases the mouse.
((("something" "chases" "lion" "+") ("lion" "visits" "mouse" "+")) -> ("something" "chases" "mouse" "+"))
If something visits the mouse then the mouse likes the lion.
((("something" "visits" "mouse" "+")) -> ("mouse" "likes" "lion" "+"))
If the mouse chases the lion and the mouse likes the lion then the mouse is green.
((("mouse" "chases" "lion" "+") ("mouse" "likes" "lion" "+")) -> ("mouse" "is" "green" "+"))
The lion visits the mouse.
True
1
proof
[(triple2)]
("lion" "visits" "mouse" "+")
triple2
The mouse does not chase the lion.
False
1
inv-proof
[(triple3)]
("mouse" "chases" "lion" "-")
triple3
The mouse chases the mouse.
True
3
proof
[(((triple3 triple2) -> rule1))]
("mouse" "chases" "mouse" "+")
((triple3 triple2) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse does not chase the mouse.
False
3
inv-proof
[(((triple3 triple2) -> rule1))]
("mouse" "chases" "mouse" "-")
((triple3 triple2) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is green.
True
4
proof
[(((triple3 ((triple2) -> rule2)) -> rule3))]
("mouse" "is" "green" "+")
((triple3 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int2
The mouse is not green.
False
4
inv-proof
[(((triple3 ((triple2) -> rule2)) -> rule3))]
("mouse" "is" "green" "-")
((triple3 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int2
The lion is not round.
Unknown
inv-random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
The mouse does not visit the lion.
Unknown
inv-random
[@0: The mouse visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "lion" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
@0: The lion chases the mouse.[(triple1)] The lion visits the mouse.[(triple2)] The mouse chases the lion.[(triple3)] @1: The mouse chases the mouse.[(((triple3 triple2) -> rule1))] The mouse likes the lion.[(((triple2) -> rule2))] @2: The mouse is green.[(((triple3 ((triple2) -> rule2)) -> rule3))]
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple1
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple3
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((triple3 triple2) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
((triple2) -> (rule2 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
((triple3 ((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int2