The cow chases the rabbit. The cow eats the rabbit. The cow is blue. The cow is round. The cow is young. The cow likes the rabbit. The rabbit chases the cow. The rabbit eats the cow. The rabbit is big. The rabbit is blue. The rabbit is round. The rabbit likes the cow. If the cow chases the rabbit then the cow likes the rabbit. If the cow likes the rabbit then the cow is round. If something is blue then it is big.
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is round.
("cow" "is" "round" "+")
The cow is young.
("cow" "is" "young" "+")
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
If the cow chases the rabbit then the cow likes the rabbit.
((("cow" "chases" "rabbit" "+")) -> ("cow" "likes" "rabbit" "+"))
If the cow likes the rabbit then the cow is round.
((("cow" "likes" "rabbit" "+")) -> ("cow" "is" "round" "+"))
If something is blue then it is big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
The rabbit chases the cow.
True
1
proof
[(triple7)]
("rabbit" "chases" "cow" "+")
triple7
The rabbit is not round.
False
1
inv-proof
[(triple11)]
("rabbit" "is" "round" "-")
triple11
The cow is big.
True
2
proof
[(((triple3) -> rule3))]
("cow" "is" "big" "+")
((triple3) -> (rule3 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is not big.
False
2
inv-proof
[(((triple3) -> rule3))]
("cow" "is" "big" "-")
((triple3) -> (rule3 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
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 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 chase the cow.
Unknown
inv-random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "-")
The rabbit is young.
Unknown
random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "+")
@0: The cow chases the rabbit.[(triple1)] The cow eats the rabbit.[(triple2)] The cow is blue.[(triple3)] The cow is round.[(triple4 OR ((triple6) -> rule2) OR ((((triple1) -> rule1)) -> rule2))] The cow is young.[(triple5)] The cow likes the rabbit.[(triple6 OR ((triple1) -> rule1))] The rabbit chases the cow.[(triple7)] The rabbit eats the cow.[(triple8)] The rabbit is big.[(triple9 OR ((triple10) -> rule3))] The rabbit is blue.[(triple10)] The rabbit is round.[(triple11)] The rabbit likes the cow.[(triple12)] @1: The cow is big.[(((triple3) -> rule3))]
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
triple1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
triple2
The cow is blue.
("cow" "is" "blue" "+")
triple3
The cow is round.
("cow" "is" "round" "+")
triple4
((triple6) -> (rule2 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
int2
The cow is young.
("cow" "is" "young" "+")
triple5
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
triple6
((triple1) -> (rule1 % int1))
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
int1
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
triple7
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
triple8
The rabbit is big.
("rabbit" "is" "big" "+")
triple9
((triple10) -> (rule3 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple10
The rabbit is round.
("rabbit" "is" "round" "+")
triple11
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
triple12
The cow is big.
("cow" "is" "big" "+")
((triple3) -> (rule3 % int1))
The cow is big.
("cow" "is" "big" "+")
int1