The cat is round. The cat likes the rabbit. The cat sees the rabbit. The cat visits the rabbit. The dog is round. The rabbit likes the cat. The rabbit sees the cat. If something sees the dog and it is round then it is cold. If something is cold and it likes the rabbit then the rabbit sees the dog. If the rabbit visits the cat and the rabbit likes the cat then the cat is blue. If something likes the cat then it visits the dog. If something likes the cat and the cat likes the dog then the cat sees the dog. If something likes the cat and the cat sees the rabbit then the rabbit visits the cat.
The cat is round.
("cat" "is" "round" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The dog is round.
("dog" "is" "round" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
If something sees the dog and it is round then it is cold.
((("something" "sees" "dog" "+") ("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If something is cold and it likes the rabbit then the rabbit sees the dog.
((("something" "is" "cold" "+") ("something" "likes" "rabbit" "+")) -> ("rabbit" "sees" "dog" "+"))
If the rabbit visits the cat and the rabbit likes the cat then the cat is blue.
((("rabbit" "visits" "cat" "+") ("rabbit" "likes" "cat" "+")) -> ("cat" "is" "blue" "+"))
If something likes the cat then it visits the dog.
((("something" "likes" "cat" "+")) -> ("something" "visits" "dog" "+"))
If something likes the cat and the cat likes the dog then the cat sees the dog.
((("something" "likes" "cat" "+") ("cat" "likes" "dog" "+")) -> ("cat" "sees" "dog" "+"))
If something likes the cat and the cat sees the rabbit then the rabbit visits the cat.
((("something" "likes" "cat" "+") ("cat" "sees" "rabbit" "+")) -> ("rabbit" "visits" "cat" "+"))
The cat likes the rabbit.
True
1
proof
[(triple2)]
("cat" "likes" "rabbit" "+")
triple2
The rabbit does not see the cat.
False
1
inv-proof
[(triple7)]
("rabbit" "sees" "cat" "-")
triple7
The rabbit visits the dog.
True
2
proof
[(((triple6) -> rule4))]
("rabbit" "visits" "dog" "+")
((triple6) -> (rule4 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The rabbit does not visit the cat.
False
3
inv-proof
[(((triple6 triple3) -> rule6))]
("rabbit" "visits" "cat" "-")
((triple6 triple3) -> (rule6 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
The cat is blue.
True
5
proof
[(((((triple6 triple3) -> rule6) triple6) -> rule3))]
("cat" "is" "blue" "+")
((((triple6 triple3) -> (rule6 % int2)) triple6) -> (rule3 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int2
The cat is not blue.
False
5
inv-proof
[(((((triple6 triple3) -> rule6) triple6) -> rule3))]
("cat" "is" "blue" "-")
((((triple6 triple3) -> (rule6 % int2)) triple6) -> (rule3 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int2
The cat is not cold.
Unknown
inv-rconc
[@2: The cat is cold.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("cat" "is" "cold" "-")
The rabbit sees the dog.
Unknown
rconc
[@3: The rabbit sees the dog.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule5 <- FAIL)]]
("rabbit" "sees" "dog" "+")
The cat does not see the dog.
Unknown
inv-rconc
[@1: The cat sees the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "sees" "dog" "-")
The cat is rough.
Unknown
random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "+")
The rabbit does not like the dog.
Unknown
inv-random
[@0: The rabbit likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "dog" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
@0: The cat is round.[(triple1)] The cat likes the rabbit.[(triple2)] The cat sees the rabbit.[(triple3)] The cat visits the rabbit.[(triple4)] The dog is round.[(triple5)] The rabbit likes the cat.[(triple6)] The rabbit sees the cat.[(triple7)] @1: The rabbit visits the cat.[(((triple6 triple3) -> rule6))] The rabbit visits the dog.[(((triple6) -> rule4))] @2: The cat is blue.[(((((triple6 triple3) -> rule6) triple6) -> rule3))]
The cat is round.
("cat" "is" "round" "+")
triple1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple2
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple3
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple4
The dog is round.
("dog" "is" "round" "+")
triple5
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple6
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple7
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
((triple6 triple3) -> (rule6 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
((triple6) -> (rule4 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
((((triple6 triple3) -> (rule6 % int2)) triple6) -> (rule3 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int2