The cat is not big. The cat is blue. The cat is red. The cat is round. The cat is young. The cat likes the rabbit. The cat needs the rabbit. The cat visits the rabbit. The rabbit is big. The rabbit is blue. The rabbit is red. The rabbit is round. The rabbit does not like the cat. The rabbit does not need the cat. The rabbit visits the cat. If something needs the rabbit then it is young. If something is big then it visits the cat. If something visits the rabbit and the rabbit does not need the cat then the rabbit is round. If something is blue then it needs the rabbit. If the rabbit is not young and the rabbit does not need the cat then the cat is red. If the rabbit is red and the rabbit visits the cat then the cat is red.
The cat is not big.
("cat" "is" "big" "-")
The cat is blue.
("cat" "is" "blue" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is round.
("cat" "is" "round" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit does not like the cat.
("rabbit" "likes" "cat" "-")
The rabbit does not need the cat.
("rabbit" "needs" "cat" "-")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
If something needs the rabbit then it is young.
((("something" "needs" "rabbit" "+")) -> ("something" "is" "young" "+"))
If something is big then it visits the cat.
((("something" "is" "big" "+")) -> ("something" "visits" "cat" "+"))
If something visits the rabbit and the rabbit does not need the cat then the rabbit is round.
((("something" "visits" "rabbit" "+") ("rabbit" "needs" "cat" "~")) -> ("rabbit" "is" "round" "+"))
If something is blue then it needs the rabbit.
((("something" "is" "blue" "+")) -> ("something" "needs" "rabbit" "+"))
If the rabbit is not young and the rabbit does not need the cat then the cat is red.
((("rabbit" "is" "young" "~") ("rabbit" "needs" "cat" "~")) -> ("cat" "is" "red" "+"))
If the rabbit is red and the rabbit visits the cat then the cat is red.
((("rabbit" "is" "red" "+") ("rabbit" "visits" "cat" "+")) -> ("cat" "is" "red" "+"))
The cat is blue.
True
1
proof
[(triple2)]
("cat" "is" "blue" "+")
triple2
The rabbit needs the cat.
False
1
inv-proof
[(triple14)]
("rabbit" "needs" "cat" "+")
triple14
The rabbit needs the rabbit.
True
2
proof
[(((triple10) -> rule4))]
("rabbit" "needs" "rabbit" "+")
((triple10) -> (rule4 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit does not need the rabbit.
False
2
inv-proof
[(((triple10) -> rule4))]
("rabbit" "needs" "rabbit" "-")
((triple10) -> (rule4 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is young.
True
3
proof
[(((((triple10) -> rule4)) -> rule1))]
("rabbit" "is" "young" "+")
((((triple10) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit is not young.
False
3
inv-proof
[(((((triple10) -> rule4)) -> rule1))]
("rabbit" "is" "young" "-")
((((triple10) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
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 cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
The rabbit does not like the rabbit.
Unknown
inv-random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "-")
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.[(triple2)] The cat is not big.[(triple1)] The cat is red.[(triple3 OR ((triple11 triple15) -> rule6) OR ((triple11 ((triple9) -> rule2)) -> rule6))] The cat is round.[(triple4)] The cat is young.[(triple5 OR ((triple7) -> rule1) OR ((((triple2) -> rule4)) -> rule1))] The cat likes the rabbit.[(triple6)] The cat needs the rabbit.[(triple7 OR ((triple2) -> rule4))] The cat visits the rabbit.[(triple8)] The rabbit does not like the cat.[(triple13)] The rabbit does not need the cat.[(triple14)] The rabbit is big.[(triple9)] The rabbit is blue.[(triple10)] The rabbit is red.[(triple11)] The rabbit is round.[(triple12 OR ((triple8 triple14) -> rule3))] The rabbit visits the cat.[(triple15 OR ((triple9) -> rule2))] @1: The rabbit needs the rabbit.[(((triple10) -> rule4))] @2: The rabbit is young.[(((((triple10) -> rule4)) -> rule1))]
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat is not big.
("cat" "is" "big" "-")
triple1
The cat is red.
("cat" "is" "red" "+")
triple3
((triple11 triple15) -> (rule6 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((triple11 ((triple9) -> (rule2 % int2))) -> (rule6 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
triple4
The cat is young.
("cat" "is" "young" "+")
triple5
((triple7) -> (rule1 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int2
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple6
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple7
((triple2) -> (rule4 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple8
The rabbit does not like the cat.
("rabbit" "likes" "cat" "-")
triple13
The rabbit does not need the cat.
("rabbit" "needs" "cat" "-")
triple14
The rabbit is big.
("rabbit" "is" "big" "+")
triple9
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple10
The rabbit is red.
("rabbit" "is" "red" "+")
triple11
The rabbit is round.
("rabbit" "is" "round" "+")
triple12
((triple8 triple14) -> (rule3 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple15
((triple9) -> (rule2 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple10) -> (rule4 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
((((triple10) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2