The cow chases the squirrel. The cow is not green. The cow is kind. The cow sees the squirrel. The squirrel does not chase the cow. The squirrel is big. The squirrel visits the cow. If something is nice and it does not visit the cow then the cow does not chase the squirrel. If the cow visits the squirrel and the squirrel does not chase the cow then the squirrel is nice. If something visits the cow and the cow sees the squirrel then the cow is not big.
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
The cow is not green.
("cow" "is" "green" "-")
The cow is kind.
("cow" "is" "kind" "+")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The squirrel does not chase the cow.
("squirrel" "chases" "cow" "-")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
If something is nice and it does not visit the cow then the cow does not chase the squirrel.
((("something" "is" "nice" "+") ("something" "visits" "cow" "~")) -> ("cow" "chases" "squirrel" "-"))
If the cow visits the squirrel and the squirrel does not chase the cow then the squirrel is nice.
((("cow" "visits" "squirrel" "+") ("squirrel" "chases" "cow" "~")) -> ("squirrel" "is" "nice" "+"))
If something visits the cow and the cow sees the squirrel then the cow is not big.
((("something" "visits" "cow" "+") ("cow" "sees" "squirrel" "+")) -> ("cow" "is" "big" "-"))
The cow is kind.
True
1
proof
[(triple3)]
("cow" "is" "kind" "+")
triple3
The cow does not see the squirrel.
False
1
inv-proof
[(triple4)]
("cow" "sees" "squirrel" "-")
triple4
The cow is not big.
True
3
proof
[(((triple7 triple4) -> rule3))]
("cow" "is" "big" "-")
((triple7 triple4) -> (rule3 % int1))
The cow is not big.
("cow" "is" "big" "-")
int1
The cow is big.
False
3
inv-proof
[(((triple7 triple4) -> rule3))]
("cow" "is" "big" "+")
((triple7 triple4) -> (rule3 % int1))
The cow is not big.
("cow" "is" "big" "-")
int1
The squirrel is not nice.
Unknown
inv-rconc
[@1: The squirrel is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "is" "nice" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
The squirrel is not kind.
Unknown
inv-random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
@0: The cow chases the squirrel.[(triple1)] The cow is kind.[(triple3)] The cow is not green.[(triple2)] The cow sees the squirrel.[(triple4)] The squirrel does not chase the cow.[(triple5)] The squirrel is big.[(triple6)] The squirrel visits the cow.[(triple7)] @1: The cow is not big.[(((triple7 triple4) -> rule3))]
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
triple1
The cow is kind.
("cow" "is" "kind" "+")
triple3
The cow is not green.
("cow" "is" "green" "-")
triple2
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple4
The squirrel does not chase the cow.
("squirrel" "chases" "cow" "-")
triple5
The squirrel is big.
("squirrel" "is" "big" "+")
triple6
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple7
The cow is not big.
("cow" "is" "big" "-")
((triple7 triple4) -> (rule3 % int1))
The cow is not big.
("cow" "is" "big" "-")
int1