The cat is cold. The cat does not like the lion. The cat visits the lion. The lion is kind. The lion is round. The lion sees the squirrel. The lion visits the cat. The lion visits the squirrel. The squirrel is rough. The squirrel is not round. The squirrel likes the cat. The squirrel likes the lion. The squirrel sees the cat. The squirrel sees the lion. The squirrel visits the lion. If the lion is rough then the lion does not like the squirrel. If someone is kind then they are rough. If someone sees the cat then they like the squirrel.
The cat is cold.
("cat" "is" "cold" "+")
The cat does not like the lion.
("cat" "likes" "lion" "-")
The cat visits the lion.
("cat" "visits" "lion" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is round.
("lion" "is" "round" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel is not round.
("squirrel" "is" "round" "-")
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If the lion is rough then the lion does not like the squirrel.
((("lion" "is" "rough" "+")) -> ("lion" "likes" "squirrel" "-"))
If someone is kind then they are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
If someone sees the cat then they like the squirrel.
((("someone" "sees" "cat" "+")) -> ("someone" "likes" "squirrel" "+"))
The squirrel is rough.
True
1
proof
[(triple9)]
("squirrel" "is" "rough" "+")
triple9
The squirrel does not see the lion.
False
1
inv-proof
[(triple14)]
("squirrel" "sees" "lion" "-")
triple14
The squirrel likes the squirrel.
True
2
proof
[(((triple13) -> rule3))]
("squirrel" "likes" "squirrel" "+")
((triple13) -> (rule3 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel does not like the squirrel.
False
2
inv-proof
[(((triple13) -> rule3))]
("squirrel" "likes" "squirrel" "-")
((triple13) -> (rule3 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The lion does not like the squirrel.
True
3
proof
[(((((triple4) -> rule2)) -> rule1))]
("lion" "likes" "squirrel" "-")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
The lion does not like the squirrel.
("lion" "likes" "squirrel" "-")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion likes the squirrel.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule1))]
("lion" "likes" "squirrel" "+")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
The lion does not like the squirrel.
("lion" "likes" "squirrel" "-")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The cat is not rough.
Unknown
inv-rconc
[@1: The cat is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "rough" "-")
The cat likes the squirrel.
Unknown
rconc
[@1: The cat likes the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "likes" "squirrel" "+")
The cat is not big.
Unknown
inv-random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "-")
The lion is cold.
Unknown
random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "+")
The squirrel is not kind.
Unknown
inv-random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
@0: The cat does not like the lion.[(triple2)] The cat is cold.[(triple1)] The cat visits the lion.[(triple3)] The lion is kind.[(triple4)] The lion is round.[(triple5)] The lion sees the squirrel.[(triple6)] The lion visits the cat.[(triple7)] The lion visits the squirrel.[(triple8)] The squirrel is not round.[(triple10)] The squirrel is rough.[(triple9)] The squirrel likes the cat.[(triple11)] The squirrel likes the lion.[(triple12)] The squirrel sees the cat.[(triple13)] The squirrel sees the lion.[(triple14)] The squirrel visits the lion.[(triple15)] @1: The lion is rough.[(((triple4) -> rule2))] The squirrel likes the squirrel.[(((triple13) -> rule3))] @2: The lion does not like the squirrel.[(((((triple4) -> rule2)) -> rule1))]
The cat does not like the lion.
("cat" "likes" "lion" "-")
triple2
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat visits the lion.
("cat" "visits" "lion" "+")
triple3
The lion is kind.
("lion" "is" "kind" "+")
triple4
The lion is round.
("lion" "is" "round" "+")
triple5
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple6
The lion visits the cat.
("lion" "visits" "cat" "+")
triple7
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple8
The squirrel is not round.
("squirrel" "is" "round" "-")
triple10
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple9
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
triple11
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
triple12
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple13
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple14
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple15
The lion is rough.
("lion" "is" "rough" "+")
((triple4) -> (rule2 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
((triple13) -> (rule3 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The lion does not like the squirrel.
("lion" "likes" "squirrel" "-")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
The lion does not like the squirrel.
("lion" "likes" "squirrel" "-")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2