The cat is not red. The rabbit likes the cat. The rabbit needs the cat. If someone is rough and they like the rabbit then the rabbit is not red. If the rabbit visits the cat then the cat visits the rabbit. If someone is red then they like the rabbit. If someone needs the cat then they visit the rabbit. If someone likes the cat then the cat is rough. If someone visits the rabbit and the rabbit likes the cat then they are red.
The cat is not red.
("cat" "is" "red" "-")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
If someone is rough and they like the rabbit then the rabbit is not red.
((("someone" "is" "rough" "+") ("someone" "likes" "rabbit" "+")) -> ("rabbit" "is" "red" "-"))
If the rabbit visits the cat then the cat visits the rabbit.
((("rabbit" "visits" "cat" "+")) -> ("cat" "visits" "rabbit" "+"))
If someone is red then they like the rabbit.
((("someone" "is" "red" "+")) -> ("someone" "likes" "rabbit" "+"))
If someone needs the cat then they visit the rabbit.
((("someone" "needs" "cat" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone likes the cat then the cat is rough.
((("someone" "likes" "cat" "+")) -> ("cat" "is" "rough" "+"))
If someone visits the rabbit and the rabbit likes the cat then they are red.
((("someone" "visits" "rabbit" "+") ("rabbit" "likes" "cat" "+")) -> ("someone" "is" "red" "+"))
The rabbit likes the cat.
True
1
proof
[(triple2)]
("rabbit" "likes" "cat" "+")
triple2
The cat is red.
False
1
inv-proof
[(triple1)]
("cat" "is" "red" "+")
triple1
The rabbit visits the rabbit.
True
2
proof
[(((triple3) -> rule4))]
("rabbit" "visits" "rabbit" "+")
((triple3) -> (rule4 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The cat is not rough.
False
2
inv-proof
[(((triple2) -> rule5))]
("cat" "is" "rough" "-")
((triple2) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The rabbit is red.
True
4
proof
[(((((triple3) -> rule4) triple2) -> rule6))]
("rabbit" "is" "red" "+")
((((triple3) -> (rule4 % int2)) triple2) -> (rule6 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit is not red.
False
4
inv-proof
[(((((triple3) -> rule4) triple2) -> rule6))]
("rabbit" "is" "red" "-")
((((triple3) -> (rule4 % int2)) triple2) -> (rule6 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The cat does not like the rabbit.
Unknown
inv-rconc
[@1: The cat likes the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "likes" "rabbit" "-")
The cat visits the rabbit.
Unknown
rconc
[@1: The cat visits the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "visits" "rabbit" "+")
The cat is not young.
Unknown
inv-random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
@0: The cat is not red.[(triple1)] The rabbit likes the cat.[(triple2)] The rabbit needs the cat.[(triple3)] @1: The cat is rough.[(((triple2) -> rule5))] The rabbit visits the rabbit.[(((triple3) -> rule4))] @2: The rabbit is red.[(((((triple3) -> rule4) triple2) -> rule6))] @3: The rabbit likes the rabbit.[(((((((triple3) -> rule4) triple2) -> rule6)) -> rule3))]
The cat is not red.
("cat" "is" "red" "-")
triple1
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple2
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple3
The cat is rough.
("cat" "is" "rough" "+")
((triple2) -> (rule5 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple3) -> (rule4 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
((((triple3) -> (rule4 % int2)) triple2) -> (rule6 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((((((triple3) -> (rule4 % int3)) triple2) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int3