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