The cow likes the squirrel. The squirrel is cold. The squirrel sees the cow. If the squirrel sees the cow and the cow is not green then the squirrel does not chase the cow. If something likes the cow and it is not nice then it sees the squirrel. If something likes the squirrel then it sees the squirrel. If something is rough and it likes the cow then it sees the squirrel. If something sees the squirrel and it is nice then the squirrel likes the cow. If the squirrel likes the cow and the cow likes the squirrel then the squirrel sees the cow.
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
If the squirrel sees the cow and the cow is not green then the squirrel does not chase the cow.
((("squirrel" "sees" "cow" "+") ("cow" "is" "green" "~")) -> ("squirrel" "chases" "cow" "-"))
If something likes the cow and it is not nice then it sees the squirrel.
((("something" "likes" "cow" "+") ("something" "is" "nice" "~")) -> ("something" "sees" "squirrel" "+"))
If something likes the squirrel then it sees the squirrel.
((("something" "likes" "squirrel" "+")) -> ("something" "sees" "squirrel" "+"))
If something is rough and it likes the cow then it sees the squirrel.
((("something" "is" "rough" "+") ("something" "likes" "cow" "+")) -> ("something" "sees" "squirrel" "+"))
If something sees the squirrel and it is nice then the squirrel likes the cow.
((("something" "sees" "squirrel" "+") ("something" "is" "nice" "+")) -> ("squirrel" "likes" "cow" "+"))
If the squirrel likes the cow and the cow likes the squirrel then the squirrel sees the cow.
((("squirrel" "likes" "cow" "+") ("cow" "likes" "squirrel" "+")) -> ("squirrel" "sees" "cow" "+"))
The squirrel is cold.
True
1
proof
[(triple2)]
("squirrel" "is" "cold" "+")
triple2
The squirrel is not cold.
False
1
inv-proof
[(triple2)]
("squirrel" "is" "cold" "-")
triple2
The cow sees the squirrel.
True
2
proof
[(((triple1) -> rule3))]
("cow" "sees" "squirrel" "+")
((triple1) -> (rule3 % int1))
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int1
The cow does not see the squirrel.
False
2
inv-proof
[(((triple1) -> rule3))]
("cow" "sees" "squirrel" "-")
((triple1) -> (rule3 % int1))
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int1
The squirrel does not see the squirrel.
Unknown
inv-rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "sees" "squirrel" "-")
The squirrel likes the cow.
Unknown
rconc
[@1: The squirrel likes the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "likes" "cow" "+")
The squirrel is not rough.
Unknown
inv-random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
@0: The cow likes the squirrel.[(triple1)] The squirrel is cold.[(triple2)] The squirrel sees the cow.[(triple3)] @1: The cow sees the squirrel.[(((triple1) -> rule3))]
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
triple1
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple2
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
triple3
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
((triple1) -> (rule3 % int1))
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
int1