The cow chases the rabbit. The cow is big. The cow is cold. The cow is kind. The cow is nice. The cow is round. The cow needs the rabbit. The cow sees the rabbit. The rabbit chases the cow. The rabbit is cold. The rabbit is kind. The rabbit is nice. The rabbit is round. The rabbit needs the cow. The rabbit sees the cow. If someone is nice then they chase the cow.
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is round.
("cow" "is" "round" "+")
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
If someone is nice then they chase the cow.
((("someone" "is" "nice" "+")) -> ("someone" "chases" "cow" "+"))
The cow is big.
True
1
proof
[(triple2)]
("cow" "is" "big" "+")
triple2
The rabbit does not chase the cow.
False
1
inv-proof
[(triple9 OR ((triple12) -> rule1))]
("rabbit" "chases" "cow" "-")
triple9
((triple12) -> (rule1 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
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 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 big.[(triple2)] The cow is cold.[(triple3)] The cow is kind.[(triple4)] The cow is nice.[(triple5)] The cow is round.[(triple6)] The cow needs the rabbit.[(triple7)] The cow sees the rabbit.[(triple8)] The rabbit chases the cow.[(triple9 OR ((triple12) -> rule1))] The rabbit is cold.[(triple10)] The rabbit is kind.[(triple11)] The rabbit is nice.[(triple12)] The rabbit is round.[(triple13)] The rabbit needs the cow.[(triple14)] The rabbit sees the cow.[(triple15)] @1: The cow chases the cow.[(((triple5) -> rule1))]
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
triple1
The cow is big.
("cow" "is" "big" "+")
triple2
The cow is cold.
("cow" "is" "cold" "+")
triple3
The cow is kind.
("cow" "is" "kind" "+")
triple4
The cow is nice.
("cow" "is" "nice" "+")
triple5
The cow is round.
("cow" "is" "round" "+")
triple6
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
triple7
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple8
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
triple9
((triple12) -> (rule1 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple10
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple11
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple12
The rabbit is round.
("rabbit" "is" "round" "+")
triple13
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple14
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple15
The cow chases the cow.
("cow" "chases" "cow" "+")
((triple5) -> (rule1 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1