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