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