The cat eats the rabbit. The cat is blue. The cat is cold. The cat is nice. The cat is red. The cat needs the rabbit. The cat sees the rabbit. The rabbit eats the cat. The rabbit is blue. The rabbit is cold. The rabbit is nice. The rabbit is red. The rabbit is young. The rabbit needs the cat. The rabbit sees the cat. If something needs the rabbit then the rabbit needs the cat. If something eats the rabbit then it needs the rabbit. If something is blue and nice then it needs the cat.
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is red.
("cat" "is" "red" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
If something needs the rabbit then the rabbit needs the cat.
((("something" "needs" "rabbit" "+")) -> ("rabbit" "needs" "cat" "+"))
If something eats the rabbit then it needs the rabbit.
((("something" "eats" "rabbit" "+")) -> ("something" "needs" "rabbit" "+"))
If something is blue and nice then it needs the cat.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "needs" "cat" "+"))
The cat eats the rabbit.
True
1
proof
[(triple1)]
("cat" "eats" "rabbit" "+")
triple1
The rabbit does not need the cat.
False
1
inv-proof
[(triple14 OR ((triple6) -> rule1) OR ((triple9 triple11) -> rule3) OR ((((triple1) -> rule2)) -> rule1))]
("rabbit" "needs" "cat" "-")
triple14
((triple6) -> (rule1 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
((triple9 triple11) -> (rule3 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int2
The cat needs the cat.
True
3
proof
[(((triple2 triple4) -> rule3))]
("cat" "needs" "cat" "+")
((triple2 triple4) -> (rule3 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat does not need the cat.
False
3
inv-proof
[(((triple2 triple4) -> rule3))]
("cat" "needs" "cat" "-")
((triple2 triple4) -> (rule3 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The rabbit does not need the rabbit.
Unknown
inv-rconc
[@1: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "needs" "rabbit" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
@0: The cat eats the rabbit.[(triple1)] The cat is blue.[(triple2)] The cat is cold.[(triple3)] The cat is nice.[(triple4)] The cat is red.[(triple5)] The cat needs the rabbit.[(triple6 OR ((triple1) -> rule2))] The cat sees the rabbit.[(triple7)] The rabbit eats the cat.[(triple8)] The rabbit is blue.[(triple9)] The rabbit is cold.[(triple10)] The rabbit is nice.[(triple11)] The rabbit is red.[(triple12)] The rabbit is young.[(triple13)] The rabbit needs the cat.[(triple14 OR ((triple6) -> rule1) OR ((triple9 triple11) -> rule3) OR ((((triple1) -> rule2)) -> rule1))] The rabbit sees the cat.[(triple15)] @1: The cat needs the cat.[(((triple2 triple4) -> rule3))]
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple1
The cat is blue.
("cat" "is" "blue" "+")
triple2
The cat is cold.
("cat" "is" "cold" "+")
triple3
The cat is nice.
("cat" "is" "nice" "+")
triple4
The cat is red.
("cat" "is" "red" "+")
triple5
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple6
((triple1) -> (rule2 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple7
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
triple8
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple9
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple10
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple11
The rabbit is red.
("rabbit" "is" "red" "+")
triple12
The rabbit is young.
("rabbit" "is" "young" "+")
triple13
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple14
((triple6) -> (rule1 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
((triple9 triple11) -> (rule3 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int2
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple15
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple2 triple4) -> (rule3 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1