The lion is kind. The mouse chases the lion. The squirrel chases the lion. If the lion chases the squirrel and the squirrel eats the mouse then the mouse eats the lion. If something likes the squirrel then it chases the mouse. If something is kind and it chases the mouse then it eats the mouse. If something is blue and it likes the lion then the lion eats the mouse. If something likes the lion and the lion is blue then the lion is red. If the squirrel chases the lion then the lion likes the squirrel.
The lion is kind.
("lion" "is" "kind" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
If the lion chases the squirrel and the squirrel eats the mouse then the mouse eats the lion.
((("lion" "chases" "squirrel" "+") ("squirrel" "eats" "mouse" "+")) -> ("mouse" "eats" "lion" "+"))
If something likes the squirrel then it chases the mouse.
((("something" "likes" "squirrel" "+")) -> ("something" "chases" "mouse" "+"))
If something is kind and it chases the mouse then it eats the mouse.
((("something" "is" "kind" "+") ("something" "chases" "mouse" "+")) -> ("something" "eats" "mouse" "+"))
If something is blue and it likes the lion then the lion eats the mouse.
((("something" "is" "blue" "+") ("something" "likes" "lion" "+")) -> ("lion" "eats" "mouse" "+"))
If something likes the lion and the lion is blue then the lion is red.
((("something" "likes" "lion" "+") ("lion" "is" "blue" "+")) -> ("lion" "is" "red" "+"))
If the squirrel chases the lion then the lion likes the squirrel.
((("squirrel" "chases" "lion" "+")) -> ("lion" "likes" "squirrel" "+"))
The squirrel chases the lion.
True
1
proof
[(triple3)]
("squirrel" "chases" "lion" "+")
triple3
The lion is not kind.
False
1
inv-proof
[(triple1)]
("lion" "is" "kind" "-")
triple1
The lion likes the squirrel.
True
2
proof
[(((triple3) -> rule6))]
("lion" "likes" "squirrel" "+")
((triple3) -> (rule6 % int1))
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int1
The lion does not like the squirrel.
False
2
inv-proof
[(((triple3) -> rule6))]
("lion" "likes" "squirrel" "-")
((triple3) -> (rule6 % int1))
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int1
The lion chases the mouse.
True
3
proof
[(((((triple3) -> rule6)) -> rule2))]
("lion" "chases" "mouse" "+")
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int2
The lion does not chase the mouse.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule2))]
("lion" "chases" "mouse" "-")
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int2
The lion eats the mouse.
True
5
proof
[(((triple1 ((((triple3) -> rule6)) -> rule2)) -> rule3))]
("lion" "eats" "mouse" "+")
((triple1 ((((triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int2
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int3
The lion does not eat the mouse.
False
5
inv-proof
[(((triple1 ((((triple3) -> rule6)) -> rule2)) -> rule3))]
("lion" "eats" "mouse" "-")
((triple1 ((((triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int2
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int3
The mouse does not chase the mouse.
Unknown
inv-rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "chases" "mouse" "-")
The mouse eats the lion.
Unknown
rconc
[@1: The mouse eats the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "eats" "lion" "+")
The lion is not red.
Unknown
inv-rconc
[@1: The lion is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "is" "red" "-")
The squirrel chases the mouse.
Unknown
rconc
[@1: The squirrel chases the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "chases" "mouse" "+")
The squirrel does not like the lion.
Unknown
inv-random
[@0: The squirrel likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "lion" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
The mouse does not like the squirrel.
Unknown
inv-random
[@0: The mouse likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "squirrel" "-")
The squirrel likes the mouse.
Unknown
random
[@0: The squirrel likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "mouse" "+")
@0: The lion is kind.[(triple1)] The mouse chases the lion.[(triple2)] The squirrel chases the lion.[(triple3)] @1: The lion likes the squirrel.[(((triple3) -> rule6))] @2: The lion chases the mouse.[(((((triple3) -> rule6)) -> rule2))] @3: The lion eats the mouse.[(((triple1 ((((triple3) -> rule6)) -> rule2)) -> rule3))]
The lion is kind.
("lion" "is" "kind" "+")
triple1
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple2
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
triple3
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
((triple3) -> (rule6 % int1))
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int2
The lion eats the mouse.
("lion" "eats" "mouse" "+")
((triple1 ((((triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int2
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int3