The cow visits the lion. The dog is kind. The lion eats the squirrel. The squirrel visits the lion. If something eats the squirrel then it sees the lion. If the squirrel sees the cow and the squirrel eats the lion then the squirrel sees the dog.
The cow visits the lion.
("cow" "visits" "lion" "+")
The dog is kind.
("dog" "is" "kind" "+")
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If something eats the squirrel then it sees the lion.
((("something" "eats" "squirrel" "+")) -> ("something" "sees" "lion" "+"))
If the squirrel sees the cow and the squirrel eats the lion then the squirrel sees the dog.
((("squirrel" "sees" "cow" "+") ("squirrel" "eats" "lion" "+")) -> ("squirrel" "sees" "dog" "+"))
The dog is kind.
True
1
proof
[(triple2)]
("dog" "is" "kind" "+")
triple2
The dog is not kind.
False
1
inv-proof
[(triple2)]
("dog" "is" "kind" "-")
triple2
The lion sees the lion.
True
2
proof
[(((triple3) -> rule1))]
("lion" "sees" "lion" "+")
((triple3) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion does not see the lion.
False
2
inv-proof
[(((triple3) -> rule1))]
("lion" "sees" "lion" "-")
((triple3) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The squirrel does not see the dog.
Unknown
inv-rconc
[@1: The squirrel sees the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "sees" "dog" "-")
The dog sees the lion.
Unknown
rconc
[@1: The dog sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "sees" "lion" "+")
The lion is not green.
Unknown
inv-random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "-")
The squirrel visits the dog.
Unknown
random
[@0: The squirrel visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "dog" "+")
@0: The cow visits the lion.[(triple1)] The dog is kind.[(triple2)] The lion eats the squirrel.[(triple3)] The squirrel visits the lion.[(triple4)] @1: The lion sees the lion.[(((triple3) -> rule1))]
The cow visits the lion.
("cow" "visits" "lion" "+")
triple1
The dog is kind.
("dog" "is" "kind" "+")
triple2
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple3
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple4
The lion sees the lion.
("lion" "sees" "lion" "+")
((triple3) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1