The cow likes the rabbit. The cow needs the tiger. The cow visits the tiger. The rabbit is big. The rabbit is cold. The rabbit is nice. The rabbit does not like the cow. The tiger is cold. The tiger is nice. The tiger needs the rabbit. If someone needs the cow and they do not like the cow then the cow visits the rabbit. If someone is nice and young then they visit the cow. If the rabbit needs the cow then the cow needs the tiger. If the cow is cold and the cow needs the tiger then the cow likes the tiger. If the rabbit likes the cow and the rabbit is not nice then the cow is not round. If someone needs the cow then they are young. If someone needs the rabbit then they need the cow. If someone likes the tiger then the tiger is nice.
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit does not like the cow.
("rabbit" "likes" "cow" "-")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
If someone needs the cow and they do not like the cow then the cow visits the rabbit.
((("someone" "needs" "cow" "+") ("someone" "likes" "cow" "~")) -> ("cow" "visits" "rabbit" "+"))
If someone is nice and young then they visit the cow.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "visits" "cow" "+"))
If the rabbit needs the cow then the cow needs the tiger.
((("rabbit" "needs" "cow" "+")) -> ("cow" "needs" "tiger" "+"))
If the cow is cold and the cow needs the tiger then the cow likes the tiger.
((("cow" "is" "cold" "+") ("cow" "needs" "tiger" "+")) -> ("cow" "likes" "tiger" "+"))
If the rabbit likes the cow and the rabbit is not nice then the cow is not round.
((("rabbit" "likes" "cow" "+") ("rabbit" "is" "nice" "~")) -> ("cow" "is" "round" "-"))
If someone needs the cow then they are young.
((("someone" "needs" "cow" "+")) -> ("someone" "is" "young" "+"))
If someone needs the rabbit then they need the cow.
((("someone" "needs" "rabbit" "+")) -> ("someone" "needs" "cow" "+"))
If someone likes the tiger then the tiger is nice.
((("someone" "likes" "tiger" "+")) -> ("tiger" "is" "nice" "+"))
The cow visits the tiger.
True
1
proof
[(triple3)]
("cow" "visits" "tiger" "+")
triple3
The cow does not like the rabbit.
False
1
inv-proof
[(triple1)]
("cow" "likes" "rabbit" "-")
triple1
The tiger needs the cow.
True
2
proof
[(((triple10) -> rule7))]
("tiger" "needs" "cow" "+")
((triple10) -> (rule7 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The tiger does not need the cow.
False
2
inv-proof
[(((triple10) -> rule7))]
("tiger" "needs" "cow" "-")
((triple10) -> (rule7 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The tiger is young.
True
3
proof
[(((((triple10) -> rule7)) -> rule6))]
("tiger" "is" "young" "+")
((((triple10) -> (rule7 % int2))) -> (rule6 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The tiger is not young.
False
3
inv-proof
[(((((triple10) -> rule7)) -> rule6))]
("tiger" "is" "young" "-")
((((triple10) -> (rule7 % int2))) -> (rule6 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The tiger visits the cow.
True
5
proof
[(((triple9 ((((triple10) -> rule7)) -> rule6)) -> rule2))]
("tiger" "visits" "cow" "+")
((triple9 ((((triple10) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int3
The tiger does not visit the cow.
False
5
inv-proof
[(((triple9 ((((triple10) -> rule7)) -> rule6)) -> rule2))]
("tiger" "visits" "cow" "-")
((triple9 ((((triple10) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int3
The cow is not young.
Unknown
inv-rconc
[@2: The cow is young.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("cow" "is" "young" "-")
The cow needs the cow.
Unknown
rconc
[@1: The cow needs the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "needs" "cow" "+")
The rabbit does not need the cow.
Unknown
inv-rconc
[@1: The rabbit needs the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "needs" "cow" "-")
The rabbit visits the cow.
Unknown
rconc
[@3: The rabbit visits the cow.[CWA. Example of deepest failure = (rule2 <- rule6 <- rule7 <- FAIL)]]
("rabbit" "visits" "cow" "+")
The tiger is not round.
Unknown
inv-random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
The cow does not like the cow.
Unknown
inv-random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "-")
The cow is big.
Unknown
random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "+")
@0: The cow likes the rabbit.[(triple1)] The cow needs the tiger.[(triple2)] The cow visits the tiger.[(triple3)] The rabbit does not like the cow.[(triple7)] The rabbit is big.[(triple4)] The rabbit is cold.[(triple5)] The rabbit is nice.[(triple6)] The tiger is cold.[(triple8)] The tiger is nice.[(triple9)] The tiger needs the rabbit.[(triple10)] @1: The tiger needs the cow.[(((triple10) -> rule7))] @2: The tiger is young.[(((((triple10) -> rule7)) -> rule6))] @3: The tiger visits the cow.[(((triple9 ((((triple10) -> rule7)) -> rule6)) -> rule2))]
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
triple1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple2
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple3
The rabbit does not like the cow.
("rabbit" "likes" "cow" "-")
triple7
The rabbit is big.
("rabbit" "is" "big" "+")
triple4
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple5
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple6
The tiger is cold.
("tiger" "is" "cold" "+")
triple8
The tiger is nice.
("tiger" "is" "nice" "+")
triple9
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple10
The tiger needs the cow.
("tiger" "needs" "cow" "+")
((triple10) -> (rule7 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
((((triple10) -> (rule7 % int2))) -> (rule6 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The tiger visits the cow.
("tiger" "visits" "cow" "+")
((triple9 ((((triple10) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int3