The cow chases the rabbit. The cow is nice. The rabbit likes the cow. If someone chases the rabbit then the rabbit chases the cow. If the cow likes the rabbit then the rabbit chases the cow. If someone likes the rabbit then the rabbit is cold. If someone chases the cow then they are nice. If the rabbit chases the cow then the cow likes the rabbit. If someone eats the cow and they are not cold then they like the cow. If the rabbit likes the cow and the cow likes the rabbit then the cow eats the rabbit. If someone likes the cow and they chase the cow then the cow eats the rabbit.
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
The cow is nice.
("cow" "is" "nice" "+")
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
If someone chases the rabbit then the rabbit chases the cow.
((("someone" "chases" "rabbit" "+")) -> ("rabbit" "chases" "cow" "+"))
If the cow likes the rabbit then the rabbit chases the cow.
((("cow" "likes" "rabbit" "+")) -> ("rabbit" "chases" "cow" "+"))
If someone likes the rabbit then the rabbit is cold.
((("someone" "likes" "rabbit" "+")) -> ("rabbit" "is" "cold" "+"))
If someone chases the cow then they are nice.
((("someone" "chases" "cow" "+")) -> ("someone" "is" "nice" "+"))
If the rabbit chases the cow then the cow likes the rabbit.
((("rabbit" "chases" "cow" "+")) -> ("cow" "likes" "rabbit" "+"))
If someone eats the cow and they are not cold then they like the cow.
((("someone" "eats" "cow" "+") ("someone" "is" "cold" "~")) -> ("someone" "likes" "cow" "+"))
If the rabbit likes the cow and the cow likes the rabbit then the cow eats the rabbit.
((("rabbit" "likes" "cow" "+") ("cow" "likes" "rabbit" "+")) -> ("cow" "eats" "rabbit" "+"))
If someone likes the cow and they chase the cow then the cow eats the rabbit.
((("someone" "likes" "cow" "+") ("someone" "chases" "cow" "+")) -> ("cow" "eats" "rabbit" "+"))
The cow chases the rabbit.
True
1
proof
[(triple1)]
("cow" "chases" "rabbit" "+")
triple1
The rabbit does not like the cow.
False
1
inv-proof
[(triple3)]
("rabbit" "likes" "cow" "-")
triple3
The rabbit chases the cow.
True
2
proof
[(((triple1) -> rule1))]
("rabbit" "chases" "cow" "+")
((triple1) -> (rule1 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The rabbit does not chase the cow.
False
2
inv-proof
[(((triple1) -> rule1))]
("rabbit" "chases" "cow" "-")
((triple1) -> (rule1 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The rabbit is nice.
True
3
proof
[(((((triple1) -> rule1)) -> rule4))]
("rabbit" "is" "nice" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int2
The rabbit is not nice.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule4))]
("rabbit" "is" "nice" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int2
The rabbit is cold.
True
4
proof
[(((((((triple1) -> rule1)) -> rule5)) -> rule3))]
("rabbit" "is" "cold" "+")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
int2
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int3
The rabbit is not cold.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule5)) -> rule3))]
("rabbit" "is" "cold" "-")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
int2
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int3
The cow does not like the cow.
Unknown
inv-rconc
[@1: The cow likes the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "likes" "cow" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The cow is big.
Unknown
random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "+")
The cow is not rough.
Unknown
inv-random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
The cow does not chase the cow.
Unknown
inv-random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
@0: The cow chases the rabbit.[(triple1)] The cow is nice.[(triple2)] The rabbit likes the cow.[(triple3)] @1: The rabbit chases the cow.[(((triple1) -> rule1))] @2: The cow eats the rabbit.[(((triple3 ((triple1) -> rule1)) -> rule8) OR ((triple3 ((((triple1) -> rule1)) -> rule5)) -> rule7))] The cow likes the rabbit.[(((((triple1) -> rule1)) -> rule5))] The rabbit is nice.[(((((triple1) -> rule1)) -> rule4))] @3: The rabbit is cold.[(((((((triple1) -> rule1)) -> rule5)) -> rule3))]
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
triple1
The cow is nice.
("cow" "is" "nice" "+")
triple2
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
triple3
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
((triple1) -> (rule1 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
((triple3 ((triple1) -> (rule1 % int2))) -> (rule8 % int1))
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int1
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int2
((triple3 ((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int1
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
int2
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int3
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
int1
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int2
The rabbit is nice.
("rabbit" "is" "nice" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
int2
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int3