The cow chases the squirrel. The cow likes the lion. The lion does not chase the cow. The lion chases the squirrel. The lion does not like the squirrel. The lion does not like the tiger. The lion does not see the cow. The squirrel chases the tiger. The squirrel is not young. The squirrel likes the lion. The tiger is blue. The tiger likes the cow. If someone sees the squirrel then they like the lion. If someone is green then they like the lion. If someone is young and blue then they chase the tiger. If the squirrel is blue then the squirrel sees the cow. If someone likes the tiger then they are not round. If someone is blue then they do not see the squirrel. If someone likes the squirrel then the squirrel likes the cow. If the squirrel chases the tiger and the tiger does not see the squirrel then the tiger likes the squirrel.
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The lion does not chase the cow.
("lion" "chases" "cow" "-")
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The lion does not like the squirrel.
("lion" "likes" "squirrel" "-")
The lion does not like the tiger.
("lion" "likes" "tiger" "-")
The lion does not see the cow.
("lion" "sees" "cow" "-")
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel is not young.
("squirrel" "is" "young" "-")
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
If someone sees the squirrel then they like the lion.
((("someone" "sees" "squirrel" "+")) -> ("someone" "likes" "lion" "+"))
If someone is green then they like the lion.
((("someone" "is" "green" "+")) -> ("someone" "likes" "lion" "+"))
If someone is young and blue then they chase the tiger.
((("someone" "is" "young" "+") ("someone" "is" "blue" "+")) -> ("someone" "chases" "tiger" "+"))
If the squirrel is blue then the squirrel sees the cow.
((("squirrel" "is" "blue" "+")) -> ("squirrel" "sees" "cow" "+"))
If someone likes the tiger then they are not round.
((("someone" "likes" "tiger" "+")) -> ("someone" "is" "round" "-"))
If someone is blue then they do not see the squirrel.
((("someone" "is" "blue" "+")) -> ("someone" "sees" "squirrel" "-"))
If someone likes the squirrel then the squirrel likes the cow.
((("someone" "likes" "squirrel" "+")) -> ("squirrel" "likes" "cow" "+"))
If the squirrel chases the tiger and the tiger does not see the squirrel then the tiger likes the squirrel.
((("squirrel" "chases" "tiger" "+") ("tiger" "sees" "squirrel" "~")) -> ("tiger" "likes" "squirrel" "+"))
The lion chases the squirrel.
True
1
proof
[(triple4)]
("lion" "chases" "squirrel" "+")
triple4
The lion likes the squirrel.
False
1
inv-proof
[(triple5)]
("lion" "likes" "squirrel" "+")
triple5
The tiger does not see the squirrel.
True
2
proof
[(((triple11) -> rule6))]
("tiger" "sees" "squirrel" "-")
((triple11) -> (rule6 % int1))
The tiger does not see the squirrel.
("tiger" "sees" "squirrel" "-")
int1
The tiger sees the squirrel.
False
2
inv-proof
[(((triple11) -> rule6))]
("tiger" "sees" "squirrel" "+")
((triple11) -> (rule6 % int1))
The tiger does not see the squirrel.
("tiger" "sees" "squirrel" "-")
int1
The tiger likes the squirrel.
True
4
proof
[(((triple8 ((triple11) -> rule6)) -> rule8))]
("tiger" "likes" "squirrel" "+")
((triple8 ((triple11) -> (rule6 % int2))) -> (rule8 % int1))
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
int1
The tiger does not see the squirrel.
("tiger" "sees" "squirrel" "-")
int2
The tiger does not like the squirrel.
False
4
inv-proof
[(((triple8 ((triple11) -> rule6)) -> rule8))]
("tiger" "likes" "squirrel" "-")
((triple8 ((triple11) -> (rule6 % int2))) -> (rule8 % int1))
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
int1
The tiger does not see the squirrel.
("tiger" "sees" "squirrel" "-")
int2
The squirrel likes the cow.
True
5
proof
[(((((triple8 ((triple11) -> rule6)) -> rule8)) -> rule7))]
("squirrel" "likes" "cow" "+")
((((triple8 ((triple11) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int1
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
int2
The tiger does not see the squirrel.
("tiger" "sees" "squirrel" "-")
int3
The squirrel does not like the cow.
False
5
inv-proof
[(((((triple8 ((triple11) -> rule6)) -> rule8)) -> rule7))]
("squirrel" "likes" "cow" "-")
((((triple8 ((triple11) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int1
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
int2
The tiger does not see the squirrel.
("tiger" "sees" "squirrel" "-")
int3
The squirrel does not see the cow.
Unknown
inv-rconc
[@1: The squirrel sees the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "sees" "cow" "-")
The lion likes the lion.
Unknown
rconc
[@1: The lion likes the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "likes" "lion" "+")
The tiger does not chase the tiger.
Unknown
inv-rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "chases" "tiger" "-")
The cow chases the tiger.
Unknown
rconc
[@1: The cow chases the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "chases" "tiger" "+")
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The cow sees the lion.
Unknown
random
[@0: The cow sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "lion" "+")
The tiger is not cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
@0: The cow chases the squirrel.[(triple1)] The cow likes the lion.[(triple2)] The lion chases the squirrel.[(triple4)] The lion does not chase the cow.[(triple3)] The lion does not like the squirrel.[(triple5)] The lion does not like the tiger.[(triple6)] The lion does not see the cow.[(triple7)] The squirrel chases the tiger.[(triple8)] The squirrel is not young.[(triple9)] The squirrel likes the lion.[(triple10)] The tiger is blue.[(triple11)] The tiger likes the cow.[(triple12)] @1: The tiger does not see the squirrel.[(((triple11) -> rule6))] @2: The tiger likes the squirrel.[(((triple8 ((triple11) -> rule6)) -> rule8))] @3: The squirrel likes the cow.[(((((triple8 ((triple11) -> rule6)) -> rule8)) -> rule7))]
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
triple1
The cow likes the lion.
("cow" "likes" "lion" "+")
triple2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple4
The lion does not chase the cow.
("lion" "chases" "cow" "-")
triple3
The lion does not like the squirrel.
("lion" "likes" "squirrel" "-")
triple5
The lion does not like the tiger.
("lion" "likes" "tiger" "-")
triple6
The lion does not see the cow.
("lion" "sees" "cow" "-")
triple7
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple8
The squirrel is not young.
("squirrel" "is" "young" "-")
triple9
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
triple10
The tiger is blue.
("tiger" "is" "blue" "+")
triple11
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple12
The tiger does not see the squirrel.
("tiger" "sees" "squirrel" "-")
((triple11) -> (rule6 % int1))
The tiger does not see the squirrel.
("tiger" "sees" "squirrel" "-")
int1
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
((triple8 ((triple11) -> (rule6 % int2))) -> (rule8 % int1))
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
int1
The tiger does not see the squirrel.
("tiger" "sees" "squirrel" "-")
int2
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
((((triple8 ((triple11) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int1
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
int2
The tiger does not see the squirrel.
("tiger" "sees" "squirrel" "-")
int3