The cat does not eat the lion. The cat sees the lion. The cat sees the squirrel. The cat visits the squirrel. The lion is not big. The lion visits the squirrel. The squirrel eats the lion. The squirrel is big. The squirrel sees the cat. The squirrel sees the lion. The squirrel visits the cat. The squirrel does not visit the lion. If the squirrel visits the cat and the squirrel sees the cat then the squirrel eats the lion. If something is blue then it visits the lion. If the squirrel eats the cat and the cat sees the squirrel then the cat does not see the lion. If something sees the cat and the cat is kind then the cat sees the lion. If something eats the squirrel and it eats the cat then the cat eats the squirrel. If something visits the squirrel then it is blue.
The cat does not eat the lion.
("cat" "eats" "lion" "-")
The cat sees the lion.
("cat" "sees" "lion" "+")
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The lion is not big.
("lion" "is" "big" "-")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
The squirrel does not visit the lion.
("squirrel" "visits" "lion" "-")
If the squirrel visits the cat and the squirrel sees the cat then the squirrel eats the lion.
((("squirrel" "visits" "cat" "+") ("squirrel" "sees" "cat" "+")) -> ("squirrel" "eats" "lion" "+"))
If something is blue then it visits the lion.
((("something" "is" "blue" "+")) -> ("something" "visits" "lion" "+"))
If the squirrel eats the cat and the cat sees the squirrel then the cat does not see the lion.
((("squirrel" "eats" "cat" "+") ("cat" "sees" "squirrel" "+")) -> ("cat" "sees" "lion" "-"))
If something sees the cat and the cat is kind then the cat sees the lion.
((("something" "sees" "cat" "+") ("cat" "is" "kind" "+")) -> ("cat" "sees" "lion" "+"))
If something eats the squirrel and it eats the cat then the cat eats the squirrel.
((("something" "eats" "squirrel" "+") ("something" "eats" "cat" "+")) -> ("cat" "eats" "squirrel" "+"))
If something visits the squirrel then it is blue.
((("something" "visits" "squirrel" "+")) -> ("something" "is" "blue" "+"))
The squirrel is big.
True
1
proof
[(triple8)]
("squirrel" "is" "big" "+")
triple8
The squirrel does not see the cat.
False
1
inv-proof
[(triple9)]
("squirrel" "sees" "cat" "-")
triple9
The lion is blue.
True
2
proof
[(((triple6) -> rule6))]
("lion" "is" "blue" "+")
((triple6) -> (rule6 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The cat is not blue.
False
2
inv-proof
[(((triple4) -> rule6))]
("cat" "is" "blue" "-")
((triple4) -> (rule6 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The lion visits the lion.
True
3
proof
[(((((triple6) -> rule6)) -> rule2))]
("lion" "visits" "lion" "+")
((((triple6) -> (rule6 % int2))) -> (rule2 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion does not visit the lion.
False
3
inv-proof
[(((((triple6) -> rule6)) -> rule2))]
("lion" "visits" "lion" "-")
((((triple6) -> (rule6 % int2))) -> (rule2 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The cat does not eat the squirrel.
Unknown
inv-rconc
[@1: The cat eats the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "eats" "squirrel" "-")
The squirrel is blue.
Unknown
rconc
[@1: The squirrel is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "is" "blue" "+")
The squirrel does not eat the squirrel.
Unknown
inv-random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
@0: The cat does not eat the lion.[(triple1)] The cat sees the lion.[(triple2)] The cat sees the squirrel.[(triple3)] The cat visits the squirrel.[(triple4)] The lion is not big.[(triple5)] The lion visits the squirrel.[(triple6)] The squirrel does not visit the lion.[(triple12)] The squirrel eats the lion.[(triple7 OR ((triple11 triple9) -> rule1))] The squirrel is big.[(triple8)] The squirrel sees the cat.[(triple9)] The squirrel sees the lion.[(triple10)] The squirrel visits the cat.[(triple11)] @1: The cat is blue.[(((triple4) -> rule6))] The lion is blue.[(((triple6) -> rule6))] @2: The cat visits the lion.[(((((triple4) -> rule6)) -> rule2))] The lion visits the lion.[(((((triple6) -> rule6)) -> rule2))]
The cat does not eat the lion.
("cat" "eats" "lion" "-")
triple1
The cat sees the lion.
("cat" "sees" "lion" "+")
triple2
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
triple3
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple4
The lion is not big.
("lion" "is" "big" "-")
triple5
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple6
The squirrel does not visit the lion.
("squirrel" "visits" "lion" "-")
triple12
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
triple7
((triple11 triple9) -> (rule1 % int1))
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
triple8
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple9
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple10
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
triple11
The cat is blue.
("cat" "is" "blue" "+")
((triple4) -> (rule6 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
((triple6) -> (rule6 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
((((triple4) -> (rule6 % int2))) -> (rule2 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The lion visits the lion.
("lion" "visits" "lion" "+")
((((triple6) -> (rule6 % int2))) -> (rule2 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2