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