The cat is red. The cat is rough. The lion is kind. The lion is nice. The lion is red. The lion needs the mouse. The lion needs the squirrel. The mouse chases the cat. The mouse chases the squirrel. The mouse sees the lion. The mouse sees the squirrel. The squirrel chases the cat. The squirrel chases the mouse. The squirrel is red. The squirrel sees the mouse. If someone sees the mouse then they need the cat. If someone chases the squirrel and they need the lion then the squirrel is nice. If someone needs the squirrel then the squirrel chases the lion. If the mouse sees the lion then the lion sees the squirrel. If someone needs the mouse then the mouse sees the lion. If someone needs the cat and they see the mouse then they see the lion.
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is red.
("lion" "is" "red" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
If someone sees the mouse then they need the cat.
((("someone" "sees" "mouse" "+")) -> ("someone" "needs" "cat" "+"))
If someone chases the squirrel and they need the lion then the squirrel is nice.
((("someone" "chases" "squirrel" "+") ("someone" "needs" "lion" "+")) -> ("squirrel" "is" "nice" "+"))
If someone needs the squirrel then the squirrel chases the lion.
((("someone" "needs" "squirrel" "+")) -> ("squirrel" "chases" "lion" "+"))
If the mouse sees the lion then the lion sees the squirrel.
((("mouse" "sees" "lion" "+")) -> ("lion" "sees" "squirrel" "+"))
If someone needs the mouse then the mouse sees the lion.
((("someone" "needs" "mouse" "+")) -> ("mouse" "sees" "lion" "+"))
If someone needs the cat and they see the mouse then they see the lion.
((("someone" "needs" "cat" "+") ("someone" "sees" "mouse" "+")) -> ("someone" "sees" "lion" "+"))
The mouse sees the squirrel.
True
1
proof
[(triple11)]
("mouse" "sees" "squirrel" "+")
triple11
The mouse does not chase the squirrel.
False
1
inv-proof
[(triple9)]
("mouse" "chases" "squirrel" "-")
triple9
The squirrel needs the cat.
True
2
proof
[(((triple15) -> rule1))]
("squirrel" "needs" "cat" "+")
((triple15) -> (rule1 % int1))
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int1
The lion does not see the squirrel.
False
2
inv-proof
[(((triple10) -> rule4) OR ((((triple6) -> rule5)) -> rule4))]
("lion" "sees" "squirrel" "-")
((triple10) -> (rule4 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int2
The squirrel sees the lion.
True
4
proof
[(((((triple15) -> rule1) triple15) -> rule6))]
("squirrel" "sees" "lion" "+")
((((triple15) -> (rule1 % int2)) triple15) -> (rule6 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int2
The squirrel does not see the lion.
False
4
inv-proof
[(((((triple15) -> rule1) triple15) -> rule6))]
("squirrel" "sees" "lion" "-")
((((triple15) -> (rule1 % int2)) triple15) -> (rule6 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int2
The lion does not see the lion.
Unknown
inv-rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "sees" "lion" "-")
The lion needs the cat.
Unknown
rconc
[@1: The lion needs the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "needs" "cat" "+")
The cat does not need the cat.
Unknown
inv-rconc
[@1: The cat needs the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "needs" "cat" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
The mouse is not nice.
Unknown
inv-random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "-")
The squirrel is rough.
Unknown
random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "+")
@0: The cat is red.[(triple1)] The cat is rough.[(triple2)] The lion is kind.[(triple3)] The lion is nice.[(triple4)] The lion is red.[(triple5)] The lion needs the mouse.[(triple6)] The lion needs the squirrel.[(triple7)] The mouse chases the cat.[(triple8)] The mouse chases the squirrel.[(triple9)] The mouse sees the lion.[(triple10 OR ((triple6) -> rule5))] The mouse sees the squirrel.[(triple11)] The squirrel chases the cat.[(triple12)] The squirrel chases the mouse.[(triple13)] The squirrel is red.[(triple14)] The squirrel sees the mouse.[(triple15)] @1: The lion sees the squirrel.[(((triple10) -> rule4) OR ((((triple6) -> rule5)) -> rule4))] The squirrel chases the lion.[(((triple7) -> rule3))] The squirrel needs the cat.[(((triple15) -> rule1))] @2: The squirrel sees the lion.[(((((triple15) -> rule1) triple15) -> rule6))]
The cat is red.
("cat" "is" "red" "+")
triple1
The cat is rough.
("cat" "is" "rough" "+")
triple2
The lion is kind.
("lion" "is" "kind" "+")
triple3
The lion is nice.
("lion" "is" "nice" "+")
triple4
The lion is red.
("lion" "is" "red" "+")
triple5
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple6
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple7
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple8
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple9
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple10
((triple6) -> (rule5 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple11
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
triple12
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
triple13
The squirrel is red.
("squirrel" "is" "red" "+")
triple14
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple15
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
((triple10) -> (rule4 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int2
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
((triple7) -> (rule3 % int1))
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int1
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
((triple15) -> (rule1 % int1))
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
((((triple15) -> (rule1 % int2)) triple15) -> (rule6 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int2