The cat is blue. The cat is cold. The cat likes the mouse. The cat needs the rabbit. The cat sees the mouse. The mouse is blue. The mouse is red. The mouse likes the cat. The rabbit is blue. The rabbit likes the mouse. The rabbit needs the cat. The rabbit sees the cat. The rabbit sees the squirrel. The squirrel likes the cat. The squirrel sees the cat. The squirrel sees the rabbit. If someone sees the mouse then they are green. If someone is cold and big then they like the rabbit. If someone sees the mouse and the mouse sees the rabbit then they need the squirrel. If someone is big then they see the squirrel. If someone is blue and they need the rabbit then the rabbit is cold. If the mouse is big and the mouse is blue then the mouse sees the squirrel. If someone is green and they like the mouse then the mouse sees the cat. If someone sees the mouse and the mouse sees the cat then the cat is big.
The cat is blue.
("cat" "is" "blue" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
If someone sees the mouse then they are green.
((("someone" "sees" "mouse" "+")) -> ("someone" "is" "green" "+"))
If someone is cold and big then they like the rabbit.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "likes" "rabbit" "+"))
If someone sees the mouse and the mouse sees the rabbit then they need the squirrel.
((("someone" "sees" "mouse" "+") ("mouse" "sees" "rabbit" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone is big then they see the squirrel.
((("someone" "is" "big" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone is blue and they need the rabbit then the rabbit is cold.
((("someone" "is" "blue" "+") ("someone" "needs" "rabbit" "+")) -> ("rabbit" "is" "cold" "+"))
If the mouse is big and the mouse is blue then the mouse sees the squirrel.
((("mouse" "is" "big" "+") ("mouse" "is" "blue" "+")) -> ("mouse" "sees" "squirrel" "+"))
If someone is green and they like the mouse then the mouse sees the cat.
((("someone" "is" "green" "+") ("someone" "likes" "mouse" "+")) -> ("mouse" "sees" "cat" "+"))
If someone sees the mouse and the mouse sees the cat then the cat is big.
((("someone" "sees" "mouse" "+") ("mouse" "sees" "cat" "+")) -> ("cat" "is" "big" "+"))
The cat sees the mouse.
True
1
proof
[(triple5)]
("cat" "sees" "mouse" "+")
triple5
The mouse is not red.
False
1
inv-proof
[(triple7)]
("mouse" "is" "red" "-")
triple7
The rabbit is cold.
True
3
proof
[(((triple1 triple4) -> rule5))]
("rabbit" "is" "cold" "+")
((triple1 triple4) -> (rule5 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The cat is not green.
False
2
inv-proof
[(((triple5) -> rule1))]
("cat" "is" "green" "-")
((triple5) -> (rule1 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The mouse sees the cat.
True
4
proof
[(((((triple5) -> rule1) triple3) -> rule7))]
("mouse" "sees" "cat" "+")
((((triple5) -> (rule1 % int2)) triple3) -> (rule7 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The mouse does not see the cat.
False
4
inv-proof
[(((((triple5) -> rule1) triple3) -> rule7))]
("mouse" "sees" "cat" "-")
((((triple5) -> (rule1 % int2)) triple3) -> (rule7 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat is big.
True
6
proof
[(((triple5 ((((triple5) -> rule1) triple3) -> rule7)) -> rule8))]
("cat" "is" "big" "+")
((triple5 ((((triple5) -> (rule1 % int3)) triple3) -> (rule7 % int2))) -> (rule8 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The cat is green.
("cat" "is" "green" "+")
int3
The cat is not big.
False
6
inv-proof
[(((triple5 ((((triple5) -> rule1) triple3) -> rule7)) -> rule8))]
("cat" "is" "big" "-")
((triple5 ((((triple5) -> (rule1 % int3)) triple3) -> (rule7 % int2))) -> (rule8 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The cat is green.
("cat" "is" "green" "+")
int3
The mouse does not need the squirrel.
Unknown
inv-rconc
[@1: The mouse needs the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "needs" "squirrel" "-")
The mouse sees the squirrel.
Unknown
rconc
[@1: The mouse sees the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "sees" "squirrel" "+")
The mouse is not green.
Unknown
inv-rconc
[@1: The mouse is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "green" "-")
The squirrel is green.
Unknown
rconc
[@1: The squirrel is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "green" "+")
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The mouse likes the squirrel.
Unknown
random
[@0: The mouse likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "squirrel" "+")
The mouse does not need the cat.
Unknown
inv-random
[@0: The mouse needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "cat" "-")
The rabbit is big.
Unknown
random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "+")
@0: The cat is blue.[(triple1)] The cat is cold.[(triple2)] The cat likes the mouse.[(triple3)] The cat needs the rabbit.[(triple4)] The cat sees the mouse.[(triple5)] The mouse is blue.[(triple6)] The mouse is red.[(triple7)] The mouse likes the cat.[(triple8)] The rabbit is blue.[(triple9)] The rabbit likes the mouse.[(triple10)] The rabbit needs the cat.[(triple11)] The rabbit sees the cat.[(triple12)] The rabbit sees the squirrel.[(triple13)] The squirrel likes the cat.[(triple14)] The squirrel sees the cat.[(triple15)] The squirrel sees the rabbit.[(triple16)] @1: The cat is green.[(((triple5) -> rule1))] The rabbit is cold.[(((triple1 triple4) -> rule5))] @2: The mouse sees the cat.[(((((triple5) -> rule1) triple3) -> rule7))] @3: The cat is big.[(((triple5 ((((triple5) -> rule1) triple3) -> rule7)) -> rule8))] @4: The cat likes the rabbit.[(((triple2 ((triple5 ((((triple5) -> rule1) triple3) -> rule7)) -> rule8)) -> rule2))] The cat sees the squirrel.[(((((triple5 ((((triple5) -> rule1) triple3) -> rule7)) -> rule8)) -> rule4))]
The cat is blue.
("cat" "is" "blue" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
triple2
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple3
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple4
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple5
The mouse is blue.
("mouse" "is" "blue" "+")
triple6
The mouse is red.
("mouse" "is" "red" "+")
triple7
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple8
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple9
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple10
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple11
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple12
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple13
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
triple14
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple15
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple16
The cat is green.
("cat" "is" "green" "+")
((triple5) -> (rule1 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
((triple1 triple4) -> (rule5 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
((((triple5) -> (rule1 % int2)) triple3) -> (rule7 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The cat is green.
("cat" "is" "green" "+")
int2
The cat is big.
("cat" "is" "big" "+")
((triple5 ((((triple5) -> (rule1 % int3)) triple3) -> (rule7 % int2))) -> (rule8 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The cat is green.
("cat" "is" "green" "+")
int3
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
((triple2 ((triple5 ((((triple5) -> (rule1 % int4)) triple3) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int3
The cat is green.
("cat" "is" "green" "+")
int4
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
((((triple5 ((((triple5) -> (rule1 % int4)) triple3) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int3
The cat is green.
("cat" "is" "green" "+")
int4