The cat sees the squirrel. The cat sees the tiger. The lion likes the tiger. The lion sees the squirrel. The lion visits the cat. The lion visits the squirrel. The squirrel is young. The squirrel does not like the lion. The squirrel visits the lion. The tiger is nice. The tiger does not like the lion. The tiger likes the squirrel. If something is young and it likes the cat then it is big. If something is nice then it sees the tiger.
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
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 young.
("squirrel" "is" "young" "+")
The squirrel does not like the lion.
("squirrel" "likes" "lion" "-")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger does not like the lion.
("tiger" "likes" "lion" "-")
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
If something is young and it likes the cat then it is big.
((("something" "is" "young" "+") ("something" "likes" "cat" "+")) -> ("something" "is" "big" "+"))
If something is nice then it sees the tiger.
((("something" "is" "nice" "+")) -> ("something" "sees" "tiger" "+"))
The squirrel visits the lion.
True
1
proof
[(triple9)]
("squirrel" "visits" "lion" "+")
triple9
The lion does not see the squirrel.
False
1
inv-proof
[(triple4)]
("lion" "sees" "squirrel" "-")
triple4
The tiger sees the tiger.
True
2
proof
[(((triple10) -> rule2))]
("tiger" "sees" "tiger" "+")
((triple10) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger does not see the tiger.
False
2
inv-proof
[(((triple10) -> rule2))]
("tiger" "sees" "tiger" "-")
((triple10) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The squirrel does not see the tiger.
Unknown
inv-rconc
[@1: The squirrel sees the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "sees" "tiger" "-")
The lion is big.
Unknown
rconc
[@1: The lion is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "big" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
@0: The cat sees the squirrel.[(triple1)] The cat sees the tiger.[(triple2)] The lion likes the tiger.[(triple3)] The lion sees the squirrel.[(triple4)] The lion visits the cat.[(triple5)] The lion visits the squirrel.[(triple6)] The squirrel does not like the lion.[(triple8)] The squirrel is young.[(triple7)] The squirrel visits the lion.[(triple9)] The tiger does not like the lion.[(triple11)] The tiger is nice.[(triple10)] The tiger likes the squirrel.[(triple12)] @1: The tiger sees the tiger.[(((triple10) -> rule2))]
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
triple1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple2
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple3
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple4
The lion visits the cat.
("lion" "visits" "cat" "+")
triple5
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple6
The squirrel does not like the lion.
("squirrel" "likes" "lion" "-")
triple8
The squirrel is young.
("squirrel" "is" "young" "+")
triple7
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple9
The tiger does not like the lion.
("tiger" "likes" "lion" "-")
triple11
The tiger is nice.
("tiger" "is" "nice" "+")
triple10
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
triple12
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((triple10) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1