The cat is cold. The cat is green. The cat sees the squirrel. The cat visits the rabbit. The cat visits the squirrel. The rabbit chases the squirrel. The rabbit is cold. The rabbit sees the cat. The squirrel chases the cat. The squirrel chases the rabbit. The squirrel is green. The squirrel visits the rabbit. If the rabbit chases the cat and the rabbit chases the squirrel then the squirrel visits the rabbit. If someone sees the cat and they chase the cat then the cat is blue. If someone sees the squirrel then they see the rabbit. If someone is young and blue then they see the squirrel. If someone visits the squirrel and they chase the squirrel then the squirrel visits the rabbit. If someone sees the squirrel then the squirrel sees the cat.
The cat is cold.
("cat" "is" "cold" "+")
The cat is green.
("cat" "is" "green" "+")
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
If the rabbit chases the cat and the rabbit chases the squirrel then the squirrel visits the rabbit.
((("rabbit" "chases" "cat" "+") ("rabbit" "chases" "squirrel" "+")) -> ("squirrel" "visits" "rabbit" "+"))
If someone sees the cat and they chase the cat then the cat is blue.
((("someone" "sees" "cat" "+") ("someone" "chases" "cat" "+")) -> ("cat" "is" "blue" "+"))
If someone sees the squirrel then they see the rabbit.
((("someone" "sees" "squirrel" "+")) -> ("someone" "sees" "rabbit" "+"))
If someone is young and blue then they see the squirrel.
((("someone" "is" "young" "+") ("someone" "is" "blue" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone visits the squirrel and they chase the squirrel then the squirrel visits the rabbit.
((("someone" "visits" "squirrel" "+") ("someone" "chases" "squirrel" "+")) -> ("squirrel" "visits" "rabbit" "+"))
If someone sees the squirrel then the squirrel sees the cat.
((("someone" "sees" "squirrel" "+")) -> ("squirrel" "sees" "cat" "+"))
The squirrel visits the rabbit.
True
1
proof
[(triple12)]
("squirrel" "visits" "rabbit" "+")
triple12
The cat does not visit the squirrel.
False
1
inv-proof
[(triple5)]
("cat" "visits" "squirrel" "-")
triple5
The cat sees the rabbit.
True
2
proof
[(((triple3) -> rule3))]
("cat" "sees" "rabbit" "+")
((triple3) -> (rule3 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The squirrel does not see the cat.
False
2
inv-proof
[(((triple3) -> rule6))]
("squirrel" "sees" "cat" "-")
((triple3) -> (rule6 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The cat is blue.
True
4
proof
[(((((triple3) -> rule6) triple9) -> rule2))]
("cat" "is" "blue" "+")
((((triple3) -> (rule6 % int2)) triple9) -> (rule2 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int2
The cat is not blue.
False
4
inv-proof
[(((((triple3) -> rule6) triple9) -> rule2))]
("cat" "is" "blue" "-")
((((triple3) -> (rule6 % int2)) triple9) -> (rule2 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int2
The squirrel does not see the rabbit.
Unknown
inv-rconc
[@2: The squirrel sees the rabbit.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("squirrel" "sees" "rabbit" "-")
The squirrel sees the squirrel.
Unknown
rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "sees" "squirrel" "+")
The rabbit does not see the squirrel.
Unknown
inv-rconc
[@1: The rabbit sees the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "sees" "squirrel" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
The rabbit is not blue.
Unknown
inv-random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "-")
The squirrel is cold.
Unknown
random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "+")
@0: The cat is cold.[(triple1)] The cat is green.[(triple2)] The cat sees the squirrel.[(triple3)] The cat visits the rabbit.[(triple4)] The cat visits the squirrel.[(triple5)] The rabbit chases the squirrel.[(triple6)] The rabbit is cold.[(triple7)] The rabbit sees the cat.[(triple8)] The squirrel chases the cat.[(triple9)] The squirrel chases the rabbit.[(triple10)] The squirrel is green.[(triple11)] The squirrel visits the rabbit.[(triple12)] @1: The cat sees the rabbit.[(((triple3) -> rule3))] The squirrel sees the cat.[(((triple3) -> rule6))] @2: The cat is blue.[(((((triple3) -> rule6) triple9) -> rule2))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat is green.
("cat" "is" "green" "+")
triple2
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
triple3
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple4
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple5
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
triple6
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple7
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple8
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
triple9
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
triple10
The squirrel is green.
("squirrel" "is" "green" "+")
triple11
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
triple12
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
((triple3) -> (rule3 % int1))
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
((triple3) -> (rule6 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
((((triple3) -> (rule6 % int2)) triple9) -> (rule2 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int2