The cow is big. The cow is young. The cow likes the rabbit. The cow visits the rabbit. The rabbit chases the cow. The rabbit is big. The rabbit is red. The rabbit is young. The rabbit likes the cow. The rabbit visits the cow. If someone visits the rabbit and the rabbit is kind then the rabbit chases the cow. If someone chases the rabbit then the rabbit chases the cow. If the cow visits the rabbit and the rabbit is red then the cow likes the rabbit. If someone chases the rabbit and they are green then the rabbit visits the cow. If someone chases the rabbit then they are green. If the rabbit visits the cow and the rabbit is green then the cow chases the rabbit. If the cow visits the rabbit then the rabbit likes the cow. If someone is red then they are green.
The cow is big.
("cow" "is" "big" "+")
The cow is young.
("cow" "is" "young" "+")
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
If someone visits the rabbit and the rabbit is kind then the rabbit chases the cow.
((("someone" "visits" "rabbit" "+") ("rabbit" "is" "kind" "+")) -> ("rabbit" "chases" "cow" "+"))
If someone chases the rabbit then the rabbit chases the cow.
((("someone" "chases" "rabbit" "+")) -> ("rabbit" "chases" "cow" "+"))
If the cow visits the rabbit and the rabbit is red then the cow likes the rabbit.
((("cow" "visits" "rabbit" "+") ("rabbit" "is" "red" "+")) -> ("cow" "likes" "rabbit" "+"))
If someone chases the rabbit and they are green then the rabbit visits the cow.
((("someone" "chases" "rabbit" "+") ("someone" "is" "green" "+")) -> ("rabbit" "visits" "cow" "+"))
If someone chases the rabbit then they are green.
((("someone" "chases" "rabbit" "+")) -> ("someone" "is" "green" "+"))
If the rabbit visits the cow and the rabbit is green then the cow chases the rabbit.
((("rabbit" "visits" "cow" "+") ("rabbit" "is" "green" "+")) -> ("cow" "chases" "rabbit" "+"))
If the cow visits the rabbit then the rabbit likes the cow.
((("cow" "visits" "rabbit" "+")) -> ("rabbit" "likes" "cow" "+"))
If someone is red then they are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
The cow visits the rabbit.
True
1
proof
[(triple4)]
("cow" "visits" "rabbit" "+")
triple4
The cow does not visit the rabbit.
False
1
inv-proof
[(triple4)]
("cow" "visits" "rabbit" "-")
triple4
The rabbit is green.
True
2
proof
[(((triple7) -> rule8))]
("rabbit" "is" "green" "+")
((triple7) -> (rule8 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is not green.
False
2
inv-proof
[(((triple7) -> rule8))]
("rabbit" "is" "green" "-")
((triple7) -> (rule8 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The cow chases the rabbit.
True
4
proof
[(((triple10 ((triple7) -> rule8)) -> rule6))]
("cow" "chases" "rabbit" "+")
((triple10 ((triple7) -> (rule8 % int2))) -> (rule6 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The cow does not chase the rabbit.
False
4
inv-proof
[(((triple10 ((triple7) -> rule8)) -> rule6))]
("cow" "chases" "rabbit" "-")
((triple10 ((triple7) -> (rule8 % int2))) -> (rule6 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The cow is green.
True
5
proof
[(((((triple10 ((triple7) -> rule8)) -> rule6)) -> rule5))]
("cow" "is" "green" "+")
((((triple10 ((triple7) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The cow is not green.
False
5
inv-proof
[(((((triple10 ((triple7) -> rule8)) -> rule6)) -> rule5))]
("cow" "is" "green" "-")
((((triple10 ((triple7) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
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 cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
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 kind.
Unknown
inv-random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
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 visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
@0: The cow is big.[(triple1)] The cow is young.[(triple2)] The cow likes the rabbit.[(triple3 OR ((triple4 triple7) -> rule3))] The cow visits the rabbit.[(triple4)] The rabbit chases the cow.[(triple5 OR ((((triple10 ((triple7) -> rule8)) -> rule6)) -> rule2))] The rabbit is big.[(triple6)] The rabbit is red.[(triple7)] The rabbit is young.[(triple8)] The rabbit likes the cow.[(triple9 OR ((triple4) -> rule7))] The rabbit visits the cow.[(triple10)] @1: The rabbit is green.[(((triple7) -> rule8))] @2: The cow chases the rabbit.[(((triple10 ((triple7) -> rule8)) -> rule6))] @3: The cow is green.[(((((triple10 ((triple7) -> rule8)) -> rule6)) -> rule5))]
The cow is big.
("cow" "is" "big" "+")
triple1
The cow is young.
("cow" "is" "young" "+")
triple2
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
triple3
((triple4 triple7) -> (rule3 % int1))
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
int1
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
triple4
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
triple5
((((triple10 ((triple7) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The rabbit is big.
("rabbit" "is" "big" "+")
triple6
The rabbit is red.
("rabbit" "is" "red" "+")
triple7
The rabbit is young.
("rabbit" "is" "young" "+")
triple8
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
triple9
((triple4) -> (rule7 % int1))
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
triple10
The rabbit is green.
("rabbit" "is" "green" "+")
((triple7) -> (rule8 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
((triple10 ((triple7) -> (rule8 % int2))) -> (rule6 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The cow is green.
("cow" "is" "green" "+")
((((triple10 ((triple7) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3