The cow chases the rabbit. The cow is cold. The cow is green. The cow is nice. The cow is red. The cow is young. The cow likes the rabbit. The cow needs the rabbit. The rabbit does not chase the cow. The rabbit is cold. The rabbit is not green. The rabbit is nice. The rabbit is not red. The rabbit likes the cow. The rabbit needs the cow. If someone is red then they do not need the cow.
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is young.
("cow" "is" "young" "+")
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
The rabbit does not chase the cow.
("rabbit" "chases" "cow" "-")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is not green.
("rabbit" "is" "green" "-")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is not red.
("rabbit" "is" "red" "-")
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
If someone is red then they do not need the cow.
((("someone" "is" "red" "+")) -> ("someone" "needs" "cow" "-"))
The cow chases the rabbit.
True
1
proof
[(triple1)]
("cow" "chases" "rabbit" "+")
triple1
The cow does not like the rabbit.
False
1
inv-proof
[(triple7)]
("cow" "likes" "rabbit" "-")
triple7
The cow does not need the cow.
True
2
proof
[(((triple5) -> rule1))]
("cow" "needs" "cow" "-")
((triple5) -> (rule1 % int1))
The cow does not need the cow.
("cow" "needs" "cow" "-")
int1
The cow needs the cow.
False
2
inv-proof
[(((triple5) -> rule1))]
("cow" "needs" "cow" "+")
((triple5) -> (rule1 % int1))
The cow does not need the cow.
("cow" "needs" "cow" "-")
int1
The rabbit is not young.
Unknown
inv-random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "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 needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
@0: The cow chases the rabbit.[(triple1)] The cow is cold.[(triple2)] The cow is green.[(triple3)] The cow is nice.[(triple4)] The cow is red.[(triple5)] The cow is young.[(triple6)] The cow likes the rabbit.[(triple7)] The cow needs the rabbit.[(triple8)] The rabbit does not chase the cow.[(triple9)] The rabbit is cold.[(triple10)] The rabbit is nice.[(triple12)] The rabbit is not green.[(triple11)] The rabbit is not red.[(triple13)] The rabbit likes the cow.[(triple14)] The rabbit needs the cow.[(triple15)] @1: The cow does not need the cow.[(((triple5) -> rule1))]
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
triple1
The cow is cold.
("cow" "is" "cold" "+")
triple2
The cow is green.
("cow" "is" "green" "+")
triple3
The cow is nice.
("cow" "is" "nice" "+")
triple4
The cow is red.
("cow" "is" "red" "+")
triple5
The cow is young.
("cow" "is" "young" "+")
triple6
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
triple7
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
triple8
The rabbit does not chase the cow.
("rabbit" "chases" "cow" "-")
triple9
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple10
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple12
The rabbit is not green.
("rabbit" "is" "green" "-")
triple11
The rabbit is not red.
("rabbit" "is" "red" "-")
triple13
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
triple14
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple15
The cow does not need the cow.
("cow" "needs" "cow" "-")
((triple5) -> (rule1 % int1))
The cow does not need the cow.
("cow" "needs" "cow" "-")
int1