The lion chases the mouse. The lion is not blue. The lion is not nice. The lion likes the squirrel. The mouse chases the squirrel. The mouse is rough. The mouse likes the squirrel. The squirrel chases the lion. The squirrel is nice. The squirrel likes the lion. If someone chases the lion then the lion chases the squirrel. If someone is nice and they need the lion then they do not chase the squirrel. If someone is nice and they do not like the lion then the lion is red. If someone chases the squirrel then the squirrel does not need the mouse. If someone likes the lion then the lion needs the squirrel. If someone needs the squirrel then the squirrel needs the lion.
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion is not blue.
("lion" "is" "blue" "-")
The lion is not nice.
("lion" "is" "nice" "-")
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
If someone chases the lion then the lion chases the squirrel.
((("someone" "chases" "lion" "+")) -> ("lion" "chases" "squirrel" "+"))
If someone is nice and they need the lion then they do not chase the squirrel.
((("someone" "is" "nice" "+") ("someone" "needs" "lion" "+")) -> ("someone" "chases" "squirrel" "-"))
If someone is nice and they do not like the lion then the lion is red.
((("someone" "is" "nice" "+") ("someone" "likes" "lion" "~")) -> ("lion" "is" "red" "+"))
If someone chases the squirrel then the squirrel does not need the mouse.
((("someone" "chases" "squirrel" "+")) -> ("squirrel" "needs" "mouse" "-"))
If someone likes the lion then the lion needs the squirrel.
((("someone" "likes" "lion" "+")) -> ("lion" "needs" "squirrel" "+"))
If someone needs the squirrel then the squirrel needs the lion.
((("someone" "needs" "squirrel" "+")) -> ("squirrel" "needs" "lion" "+"))
The mouse chases the squirrel.
True
1
proof
[(triple5)]
("mouse" "chases" "squirrel" "+")
triple5
The lion is nice.
False
1
inv-proof
[(triple3)]
("lion" "is" "nice" "+")
triple3
The squirrel does not need the mouse.
True
2
proof
[(((triple5) -> rule4) OR ((((triple8) -> rule1)) -> rule4))]
("squirrel" "needs" "mouse" "-")
((triple5) -> (rule4 % int1))
The squirrel does not need the mouse.
("squirrel" "needs" "mouse" "-")
int1
((((triple8) -> (rule1 % int2))) -> (rule4 % int1))
The squirrel does not need the mouse.
("squirrel" "needs" "mouse" "-")
int1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int2
The lion does not need the squirrel.
False
2
inv-proof
[(((triple10) -> rule5))]
("lion" "needs" "squirrel" "-")
((triple10) -> (rule5 % int1))
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int1
The squirrel needs the lion.
True
3
proof
[(((((triple10) -> rule5)) -> rule6))]
("squirrel" "needs" "lion" "+")
((((triple10) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int2
The squirrel does not need the lion.
False
3
inv-proof
[(((((triple10) -> rule5)) -> rule6))]
("squirrel" "needs" "lion" "-")
((((triple10) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int2
The squirrel does not chase the squirrel.
True
5
proof
[(((triple9 ((((triple10) -> rule5)) -> rule6)) -> rule2))]
("squirrel" "chases" "squirrel" "-")
((triple9 ((((triple10) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The squirrel does not chase the squirrel.
("squirrel" "chases" "squirrel" "-")
int1
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int2
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int3
The squirrel chases the squirrel.
False
5
inv-proof
[(((triple9 ((((triple10) -> rule5)) -> rule6)) -> rule2))]
("squirrel" "chases" "squirrel" "+")
((triple9 ((((triple10) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The squirrel does not chase the squirrel.
("squirrel" "chases" "squirrel" "-")
int1
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int2
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int3
The lion is not red.
Unknown
inv-rconc
[@1: The lion is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "red" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
The lion is not green.
Unknown
inv-random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
The squirrel does not chase the mouse.
Unknown
inv-random
[@0: The squirrel chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "mouse" "-")
The lion likes the mouse.
Unknown
random
[@0: The lion likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "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 squirrel is blue.
Unknown
random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "+")
@0: The lion chases the mouse.[(triple1)] The lion is not blue.[(triple2)] The lion is not nice.[(triple3)] The lion likes the squirrel.[(triple4)] The mouse chases the squirrel.[(triple5)] The mouse is rough.[(triple6)] The mouse likes the squirrel.[(triple7)] The squirrel chases the lion.[(triple8)] The squirrel is nice.[(triple9)] The squirrel likes the lion.[(triple10)] @1: The lion chases the squirrel.[(((triple8) -> rule1))] The lion needs the squirrel.[(((triple10) -> rule5))] The squirrel does not need the mouse.[(((triple5) -> rule4) OR ((((triple8) -> rule1)) -> rule4))] @2: The squirrel needs the lion.[(((((triple10) -> rule5)) -> rule6))] @3: The squirrel does not chase the squirrel.[(((triple9 ((((triple10) -> rule5)) -> rule6)) -> rule2))]
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple1
The lion is not blue.
("lion" "is" "blue" "-")
triple2
The lion is not nice.
("lion" "is" "nice" "-")
triple3
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
triple4
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple5
The mouse is rough.
("mouse" "is" "rough" "+")
triple6
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple7
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
triple8
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple9
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
triple10
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
((triple8) -> (rule1 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
((triple10) -> (rule5 % int1))
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int1
The squirrel does not need the mouse.
("squirrel" "needs" "mouse" "-")
((triple5) -> (rule4 % int1))
The squirrel does not need the mouse.
("squirrel" "needs" "mouse" "-")
int1
((((triple8) -> (rule1 % int2))) -> (rule4 % int1))
The squirrel does not need the mouse.
("squirrel" "needs" "mouse" "-")
int1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int2
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
((((triple10) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int2
The squirrel does not chase the squirrel.
("squirrel" "chases" "squirrel" "-")
((triple9 ((((triple10) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The squirrel does not chase the squirrel.
("squirrel" "chases" "squirrel" "-")
int1
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int2
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int3