The cow is not round. The lion chases the cow. The rabbit chases the lion. If someone chases the lion then they do not chase the rabbit.
The cow is not round.
("cow" "is" "round" "-")
The lion chases the cow.
("lion" "chases" "cow" "+")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
If someone chases the lion then they do not chase the rabbit.
((("someone" "chases" "lion" "+")) -> ("someone" "chases" "rabbit" "-"))
The rabbit chases the lion.
True
1
proof
[(triple3)]
("rabbit" "chases" "lion" "+")
triple3
The lion does not chase the cow.
False
1
inv-proof
[(triple2)]
("lion" "chases" "cow" "-")
triple2
The rabbit does not chase the rabbit.
True
2
proof
[(((triple3) -> rule1))]
("rabbit" "chases" "rabbit" "-")
((triple3) -> (rule1 % int1))
The rabbit does not chase the rabbit.
("rabbit" "chases" "rabbit" "-")
int1
The rabbit chases the rabbit.
False
2
inv-proof
[(((triple3) -> rule1))]
("rabbit" "chases" "rabbit" "+")
((triple3) -> (rule1 % int1))
The rabbit does not chase the rabbit.
("rabbit" "chases" "rabbit" "-")
int1
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The rabbit visits the cow.
Unknown
random
[@0: The rabbit visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "cow" "+")
The lion does not chase the rabbit.
Unknown
inv-random
[@0: The lion chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "rabbit" "-")
The lion needs the cow.
Unknown
random
[@0: The lion needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "cow" "+")
@0: The cow is not round.[(triple1)] The lion chases the cow.[(triple2)] The rabbit chases the lion.[(triple3)] @1: The rabbit does not chase the rabbit.[(((triple3) -> rule1))]
The cow is not round.
("cow" "is" "round" "-")
triple1
The lion chases the cow.
("lion" "chases" "cow" "+")
triple2
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple3
The rabbit does not chase the rabbit.
("rabbit" "chases" "rabbit" "-")
((triple3) -> (rule1 % int1))
The rabbit does not chase the rabbit.
("rabbit" "chases" "rabbit" "-")
int1