The cat is blue. The cat is kind. The cat is red. The cat needs the rabbit. The cat sees the rabbit. The cat visits the rabbit. The rabbit is blue. The rabbit is cold. The rabbit is green. The rabbit needs the cat. The rabbit sees the cat. The rabbit visits the cat. If someone is blue then they need the rabbit. If someone sees the cat and the cat is cold then they visit the cat.
The cat is blue.
("cat" "is" "blue" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is red.
("cat" "is" "red" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
If someone is blue then they need the rabbit.
((("someone" "is" "blue" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone sees the cat and the cat is cold then they visit the cat.
((("someone" "sees" "cat" "+") ("cat" "is" "cold" "+")) -> ("someone" "visits" "cat" "+"))
The cat is blue.
True
1
proof
[(triple1)]
("cat" "is" "blue" "+")
triple1
The cat does not visit the rabbit.
False
1
inv-proof
[(triple6)]
("cat" "visits" "rabbit" "-")
triple6
The rabbit needs the rabbit.
True
2
proof
[(((triple7) -> rule1))]
("rabbit" "needs" "rabbit" "+")
((triple7) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit does not need the rabbit.
False
2
inv-proof
[(((triple7) -> rule1))]
("rabbit" "needs" "rabbit" "-")
((triple7) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The cat does not visit the cat.
Unknown
inv-rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "visits" "cat" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
The cat is not green.
Unknown
inv-random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
@0: The cat is blue.[(triple1)] The cat is kind.[(triple2)] The cat is red.[(triple3)] The cat needs the rabbit.[(triple4 OR ((triple1) -> rule1))] The cat sees the rabbit.[(triple5)] The cat visits the rabbit.[(triple6)] The rabbit is blue.[(triple7)] The rabbit is cold.[(triple8)] The rabbit is green.[(triple9)] The rabbit needs the cat.[(triple10)] The rabbit sees the cat.[(triple11)] The rabbit visits the cat.[(triple12)] @1: The rabbit needs the rabbit.[(((triple7) -> rule1))]
The cat is blue.
("cat" "is" "blue" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cat is red.
("cat" "is" "red" "+")
triple3
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple4
((triple1) -> (rule1 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple5
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple6
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple7
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple8
The rabbit is green.
("rabbit" "is" "green" "+")
triple9
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple10
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple11
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple12
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple7) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1