The cow chases the rabbit. The cow eats the rabbit. The cow is red. The cow is rough. The cow sees the rabbit. The rabbit eats the cow. The rabbit sees the cow. If the rabbit sees the cow then the rabbit chases the cow.
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
If the rabbit sees the cow then the rabbit chases the cow.
((("rabbit" "sees" "cow" "+")) -> ("rabbit" "chases" "cow" "+"))
The cow eats the rabbit.
True
1
proof
[(triple2)]
("cow" "eats" "rabbit" "+")
triple2
The cow does not chase the rabbit.
False
1
inv-proof
[(triple1)]
("cow" "chases" "rabbit" "-")
triple1
The rabbit chases the cow.
True
2
proof
[(((triple7) -> rule1))]
("rabbit" "chases" "cow" "+")
((triple7) -> (rule1 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The rabbit does not chase the cow.
False
2
inv-proof
[(((triple7) -> rule1))]
("rabbit" "chases" "cow" "-")
((triple7) -> (rule1 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The rabbit eats the rabbit.
Unknown
random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "+")
@0: The cow chases the rabbit.[(triple1)] The cow eats the rabbit.[(triple2)] The cow is red.[(triple3)] The cow is rough.[(triple4)] The cow sees the rabbit.[(triple5)] The rabbit eats the cow.[(triple6)] The rabbit sees the cow.[(triple7)] @1: The rabbit chases the cow.[(((triple7) -> rule1))]
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
triple1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
triple2
The cow is red.
("cow" "is" "red" "+")
triple3
The cow is rough.
("cow" "is" "rough" "+")
triple4
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple5
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
triple6
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple7
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
((triple7) -> (rule1 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1