The cow is cold. The dog likes the rabbit. The rabbit eats the dog. The tiger eats the cow. If something eats the dog then it eats the rabbit. If something is young then it likes the rabbit. If something needs the tiger then the tiger is kind. If something needs the tiger then it eats the cow. If something needs the tiger and the tiger likes the rabbit then the rabbit needs the tiger. If something eats the cow then it needs the tiger. If the rabbit needs the cow then the cow needs the dog. If the tiger likes the dog then the dog is nice.
The cow is cold.
("cow" "is" "cold" "+")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
If something eats the dog then it eats the rabbit.
((("something" "eats" "dog" "+")) -> ("something" "eats" "rabbit" "+"))
If something is young then it likes the rabbit.
((("something" "is" "young" "+")) -> ("something" "likes" "rabbit" "+"))
If something needs the tiger then the tiger is kind.
((("something" "needs" "tiger" "+")) -> ("tiger" "is" "kind" "+"))
If something needs the tiger then it eats the cow.
((("something" "needs" "tiger" "+")) -> ("something" "eats" "cow" "+"))
If something needs the tiger and the tiger likes the rabbit then the rabbit needs the tiger.
((("something" "needs" "tiger" "+") ("tiger" "likes" "rabbit" "+")) -> ("rabbit" "needs" "tiger" "+"))
If something eats the cow then it needs the tiger.
((("something" "eats" "cow" "+")) -> ("something" "needs" "tiger" "+"))
If the rabbit needs the cow then the cow needs the dog.
((("rabbit" "needs" "cow" "+")) -> ("cow" "needs" "dog" "+"))
If the tiger likes the dog then the dog is nice.
((("tiger" "likes" "dog" "+")) -> ("dog" "is" "nice" "+"))
The rabbit eats the dog.
True
1
proof
[(triple3)]
("rabbit" "eats" "dog" "+")
triple3
The cow is not cold.
False
1
inv-proof
[(triple1)]
("cow" "is" "cold" "-")
triple1
The rabbit eats the rabbit.
True
2
proof
[(((triple3) -> rule1))]
("rabbit" "eats" "rabbit" "+")
((triple3) -> (rule1 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The tiger does not need the tiger.
False
2
inv-proof
[(((triple4) -> rule6))]
("tiger" "needs" "tiger" "-")
((triple4) -> (rule6 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger is kind.
True
3
proof
[(((((triple4) -> rule6)) -> rule3))]
("tiger" "is" "kind" "+")
((((triple4) -> (rule6 % int2))) -> (rule3 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger is not kind.
False
3
inv-proof
[(((((triple4) -> rule6)) -> rule3))]
("tiger" "is" "kind" "-")
((((triple4) -> (rule6 % int2))) -> (rule3 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The cow does not need the dog.
Unknown
inv-rconc
[@1: The cow needs the dog.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "needs" "dog" "-")
The cow likes the rabbit.
Unknown
rconc
[@1: The cow likes the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "likes" "rabbit" "+")
The rabbit does not eat the cow.
Unknown
inv-rconc
[@3: The rabbit eats the cow.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule6 <- FAIL)]]
("rabbit" "eats" "cow" "-")
The tiger needs the cow.
Unknown
random
[@0: The tiger needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "cow" "+")
The rabbit is not red.
Unknown
inv-random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "-")
The rabbit is nice.
Unknown
random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "+")
@0: The cow is cold.[(triple1)] The dog likes the rabbit.[(triple2)] The rabbit eats the dog.[(triple3)] The tiger eats the cow.[(triple4)] @1: The rabbit eats the rabbit.[(((triple3) -> rule1))] The tiger needs the tiger.[(((triple4) -> rule6))] @2: The tiger is kind.[(((((triple4) -> rule6)) -> rule3))]
The cow is cold.
("cow" "is" "cold" "+")
triple1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple2
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple3
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple4
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((triple3) -> (rule1 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((triple4) -> (rule6 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
((((triple4) -> (rule6 % int2))) -> (rule3 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2