The cat chases the cow. The cow is cold. The cow is nice. The cow is young. The cow needs the rabbit. The rabbit chases the cat. The rabbit chases the cow. The rabbit is nice. The rabbit is rough. The rabbit is young. The rabbit likes the cat. The rabbit needs the cat. If someone needs the cow then the cow is cold. If the cat is nice then the cat needs the cow. If someone likes the cow and they like the cat then the cat is kind. If someone is nice then they need the cow. If someone needs the cow and they like the cat then the cow likes the rabbit. If someone is cold and they need the cow then the cow chases the rabbit. If someone needs the cat then the cat is rough. If the rabbit is nice and the rabbit is kind then the rabbit chases the cat.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is young.
("cow" "is" "young" "+")
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
If someone needs the cow then the cow is cold.
((("someone" "needs" "cow" "+")) -> ("cow" "is" "cold" "+"))
If the cat is nice then the cat needs the cow.
((("cat" "is" "nice" "+")) -> ("cat" "needs" "cow" "+"))
If someone likes the cow and they like the cat then the cat is kind.
((("someone" "likes" "cow" "+") ("someone" "likes" "cat" "+")) -> ("cat" "is" "kind" "+"))
If someone is nice then they need the cow.
((("someone" "is" "nice" "+")) -> ("someone" "needs" "cow" "+"))
If someone needs the cow and they like the cat then the cow likes the rabbit.
((("someone" "needs" "cow" "+") ("someone" "likes" "cat" "+")) -> ("cow" "likes" "rabbit" "+"))
If someone is cold and they need the cow then the cow chases the rabbit.
((("someone" "is" "cold" "+") ("someone" "needs" "cow" "+")) -> ("cow" "chases" "rabbit" "+"))
If someone needs the cat then the cat is rough.
((("someone" "needs" "cat" "+")) -> ("cat" "is" "rough" "+"))
If the rabbit is nice and the rabbit is kind then the rabbit chases the cat.
((("rabbit" "is" "nice" "+") ("rabbit" "is" "kind" "+")) -> ("rabbit" "chases" "cat" "+"))
The rabbit chases the cat.
True
1
proof
[(triple6)]
("rabbit" "chases" "cat" "+")
triple6
The cat does not chase the cow.
False
1
inv-proof
[(triple1)]
("cat" "chases" "cow" "-")
triple1
The cow needs the cow.
True
2
proof
[(((triple3) -> rule4))]
("cow" "needs" "cow" "+")
((triple3) -> (rule4 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow does not need the cow.
False
2
inv-proof
[(((triple3) -> rule4))]
("cow" "needs" "cow" "-")
((triple3) -> (rule4 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cat does not need the cow.
Unknown
inv-rconc
[@1: The cat needs the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "needs" "cow" "-")
The cat is kind.
Unknown
rconc
[@1: The cat is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "kind" "+")
The cat does not chase the rabbit.
Unknown
inv-random
[@0: The cat chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "rabbit" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
@0: The cat chases the cow.[(triple1)] The cow is cold.[(triple2 OR ((((triple3) -> rule4)) -> rule1) OR ((((triple8) -> rule4)) -> rule1))] The cow is nice.[(triple3)] The cow is young.[(triple4)] The cow needs the rabbit.[(triple5)] The rabbit chases the cat.[(triple6)] The rabbit chases the cow.[(triple7)] The rabbit is nice.[(triple8)] The rabbit is rough.[(triple9)] The rabbit is young.[(triple10)] The rabbit likes the cat.[(triple11)] The rabbit needs the cat.[(triple12)] @1: The cat is rough.[(((triple12) -> rule7))] The cow needs the cow.[(((triple3) -> rule4))] The rabbit needs the cow.[(((triple8) -> rule4))] @2: The cow chases the rabbit.[(((triple2 ((triple3) -> rule4)) -> rule6) OR ((((((triple3) -> rule4)) -> rule1) ((triple3) -> rule4)) -> rule6) OR ((((((triple8) -> rule4)) -> rule1) ((triple3) -> rule4)) -> rule6))] The cow likes the rabbit.[(((((triple8) -> rule4) triple11) -> rule5))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
The cow is cold.
("cow" "is" "cold" "+")
triple2
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
((((triple8) -> (rule4 % int2))) -> (rule1 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
triple3
The cow is young.
("cow" "is" "young" "+")
triple4
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
triple5
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple6
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
triple7
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple8
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple9
The rabbit is young.
("rabbit" "is" "young" "+")
triple10
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple11
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple12
The cat is rough.
("cat" "is" "rough" "+")
((triple12) -> (rule7 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple3) -> (rule4 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
((triple8) -> (rule4 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
((triple2 ((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
((((((triple3) -> (rule4 % int3))) -> (rule1 % int2)) ((triple3) -> (rule4 % int3))) -> (rule6 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
int3
((((((triple8) -> (rule4 % int4))) -> (rule1 % int3)) ((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int4
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
((((triple8) -> (rule4 % int2)) triple11) -> (rule5 % int1))
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2