The cow is kind. The cow likes the rabbit. The cow needs the rabbit. The rabbit is blue. The rabbit is red. The rabbit is rough. The rabbit does not like the cow. The rabbit likes the tiger. The rabbit needs the cow. The rabbit needs the tiger. The tiger eats the cow. The tiger eats the rabbit. The tiger is kind. The tiger likes the rabbit. The tiger needs the cow. If someone is red and blue then they eat the tiger. If someone needs the cow then they eat the tiger. If the rabbit eats the cow then the cow is not rough. If the rabbit eats the tiger then the tiger is not red. If someone needs the tiger and they need the cow then they eat the rabbit. If the rabbit eats the tiger and the tiger is not big then the rabbit needs the tiger. If someone is kind then they like the cow. If someone likes the cow then the cow is blue.
The cow is kind.
("cow" "is" "kind" "+")
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit does not like the cow.
("rabbit" "likes" "cow" "-")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
If someone is red and blue then they eat the tiger.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "eats" "tiger" "+"))
If someone needs the cow then they eat the tiger.
((("someone" "needs" "cow" "+")) -> ("someone" "eats" "tiger" "+"))
If the rabbit eats the cow then the cow is not rough.
((("rabbit" "eats" "cow" "+")) -> ("cow" "is" "rough" "-"))
If the rabbit eats the tiger then the tiger is not red.
((("rabbit" "eats" "tiger" "+")) -> ("tiger" "is" "red" "-"))
If someone needs the tiger and they need the cow then they eat the rabbit.
((("someone" "needs" "tiger" "+") ("someone" "needs" "cow" "+")) -> ("someone" "eats" "rabbit" "+"))
If the rabbit eats the tiger and the tiger is not big then the rabbit needs the tiger.
((("rabbit" "eats" "tiger" "+") ("tiger" "is" "big" "~")) -> ("rabbit" "needs" "tiger" "+"))
If someone is kind then they like the cow.
((("someone" "is" "kind" "+")) -> ("someone" "likes" "cow" "+"))
If someone likes the cow then the cow is blue.
((("someone" "likes" "cow" "+")) -> ("cow" "is" "blue" "+"))
The tiger is kind.
True
1
proof
[(triple13)]
("tiger" "is" "kind" "+")
triple13
The rabbit likes the cow.
False
1
inv-proof
[(triple7)]
("rabbit" "likes" "cow" "+")
triple7
The rabbit eats the tiger.
True
2
proof
[(((triple9) -> rule2) OR ((triple5 triple4) -> rule1))]
("rabbit" "eats" "tiger" "+")
((triple9) -> (rule2 % int1))
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int1
((triple5 triple4) -> (rule1 % int1))
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int1
The rabbit does not eat the rabbit.
False
3
inv-proof
[(((triple10 triple9) -> rule5))]
("rabbit" "eats" "rabbit" "-")
((triple10 triple9) -> (rule5 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The tiger is not red.
True
3
proof
[(((((triple9) -> rule2)) -> rule4) OR ((((triple5 triple4) -> rule1)) -> rule4))]
("tiger" "is" "red" "-")
((((triple9) -> (rule2 % int2))) -> (rule4 % int1))
The tiger is not red.
("tiger" "is" "red" "-")
int1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int2
((((triple5 triple4) -> (rule1 % int2))) -> (rule4 % int1))
The tiger is not red.
("tiger" "is" "red" "-")
int1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int2
The cow is not blue.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule8) OR ((((triple13) -> rule7)) -> rule8))]
("cow" "is" "blue" "-")
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
((((triple13) -> (rule7 % int2))) -> (rule8 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int2
The cow does not eat the tiger.
Unknown
inv-rconc
[@1: The cow eats the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "eats" "tiger" "-")
The cow eats the rabbit.
Unknown
rconc
[@1: The cow eats the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "eats" "rabbit" "+")
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 is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
The tiger is not rough.
Unknown
inv-random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "-")
The cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
@0: The cow is kind.[(triple1)] The cow likes the rabbit.[(triple2)] The cow needs the rabbit.[(triple3)] The rabbit does not like the cow.[(triple7)] The rabbit is blue.[(triple4)] The rabbit is red.[(triple5)] The rabbit is rough.[(triple6)] The rabbit likes the tiger.[(triple8)] The rabbit needs the cow.[(triple9)] The rabbit needs the tiger.[(triple10)] The tiger eats the cow.[(triple11)] The tiger eats the rabbit.[(triple12)] The tiger is kind.[(triple13)] The tiger likes the rabbit.[(triple14)] The tiger needs the cow.[(triple15)] @1: The cow likes the cow.[(((triple1) -> rule7))] The rabbit eats the rabbit.[(((triple10 triple9) -> rule5))] The rabbit eats the tiger.[(((triple9) -> rule2) OR ((triple5 triple4) -> rule1))] The tiger eats the tiger.[(((triple15) -> rule2))] The tiger likes the cow.[(((triple13) -> rule7))] @2: The cow is blue.[(((((triple1) -> rule7)) -> rule8) OR ((((triple13) -> rule7)) -> rule8))] The tiger is not red.[(((((triple9) -> rule2)) -> rule4) OR ((((triple5 triple4) -> rule1)) -> rule4))]
The cow is kind.
("cow" "is" "kind" "+")
triple1
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
triple2
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
triple3
The rabbit does not like the cow.
("rabbit" "likes" "cow" "-")
triple7
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple4
The rabbit is red.
("rabbit" "is" "red" "+")
triple5
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple6
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple8
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple9
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple10
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple11
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple12
The tiger is kind.
("tiger" "is" "kind" "+")
triple13
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple14
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple15
The cow likes the cow.
("cow" "likes" "cow" "+")
((triple1) -> (rule7 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((triple10 triple9) -> (rule5 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
((triple9) -> (rule2 % int1))
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int1
((triple5 triple4) -> (rule1 % int1))
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((triple15) -> (rule2 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
((triple13) -> (rule7 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
((((triple13) -> (rule7 % int2))) -> (rule8 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int2
The tiger is not red.
("tiger" "is" "red" "-")
((((triple9) -> (rule2 % int2))) -> (rule4 % int1))
The tiger is not red.
("tiger" "is" "red" "-")
int1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int2
((((triple5 triple4) -> (rule1 % int2))) -> (rule4 % int1))
The tiger is not red.
("tiger" "is" "red" "-")
int1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int2