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