The cow eats the squirrel. The squirrel chases the cow. If someone sees the squirrel then they are nice. If someone sees the cow then the cow does not see the squirrel. If someone is blue and not nice then they chase the cow. If someone chases the cow and the cow eats the squirrel then the cow chases the squirrel. If the cow eats the squirrel and the cow is not round then the squirrel chases the cow. If someone chases the squirrel then the squirrel chases the cow.
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
If someone sees the squirrel then they are nice.
((("someone" "sees" "squirrel" "+")) -> ("someone" "is" "nice" "+"))
If someone sees the cow then the cow does not see the squirrel.
((("someone" "sees" "cow" "+")) -> ("cow" "sees" "squirrel" "-"))
If someone is blue and not nice then they chase the cow.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "~")) -> ("someone" "chases" "cow" "+"))
If someone chases the cow and the cow eats the squirrel then the cow chases the squirrel.
((("someone" "chases" "cow" "+") ("cow" "eats" "squirrel" "+")) -> ("cow" "chases" "squirrel" "+"))
If the cow eats the squirrel and the cow is not round then the squirrel chases the cow.
((("cow" "eats" "squirrel" "+") ("cow" "is" "round" "~")) -> ("squirrel" "chases" "cow" "+"))
If someone chases the squirrel then the squirrel chases the cow.
((("someone" "chases" "squirrel" "+")) -> ("squirrel" "chases" "cow" "+"))
The squirrel chases the cow.
True
1
proof
[(triple2)]
("squirrel" "chases" "cow" "+")
triple2
The cow does not eat the squirrel.
False
1
inv-proof
[(triple1)]
("cow" "eats" "squirrel" "-")
triple1
The cow chases the squirrel.
True
3
proof
[(((triple2 triple1) -> rule4))]
("cow" "chases" "squirrel" "+")
((triple2 triple1) -> (rule4 % int1))
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int1
The cow does not chase the squirrel.
False
3
inv-proof
[(((triple2 triple1) -> rule4))]
("cow" "chases" "squirrel" "-")
((triple2 triple1) -> (rule4 % int1))
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int1
The squirrel is not nice.
Unknown
inv-rconc
[@1: The squirrel is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "nice" "-")
The cow chases the cow.
Unknown
rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "chases" "cow" "+")
The squirrel does not eat the squirrel.
Unknown
inv-random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
@0: The cow eats the squirrel.[(triple1)] The squirrel chases the cow.[(triple2)] @1: The cow chases the squirrel.[(((triple2 triple1) -> rule4))]
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
triple1
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
triple2
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
((triple2 triple1) -> (rule4 % int1))
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int1