The dog likes the squirrel. The squirrel likes the dog. The tiger is big. If someone is big then they see the squirrel. If someone is red then they do not like the tiger. If someone needs the tiger then they are young. If someone sees the squirrel then they see the tiger. If someone likes the squirrel then the squirrel sees the tiger. If someone needs the squirrel then the squirrel likes the dog. Blue, round people are not red. If someone sees the tiger and they do not need the tiger then they are not big.
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
The tiger is big.
("tiger" "is" "big" "+")
If someone is big then they see the squirrel.
((("someone" "is" "big" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone is red then they do not like the tiger.
((("someone" "is" "red" "+")) -> ("someone" "likes" "tiger" "-"))
If someone needs the tiger then they are young.
((("someone" "needs" "tiger" "+")) -> ("someone" "is" "young" "+"))
If someone sees the squirrel then they see the tiger.
((("someone" "sees" "squirrel" "+")) -> ("someone" "sees" "tiger" "+"))
If someone likes the squirrel then the squirrel sees the tiger.
((("someone" "likes" "squirrel" "+")) -> ("squirrel" "sees" "tiger" "+"))
If someone needs the squirrel then the squirrel likes the dog.
((("someone" "needs" "squirrel" "+")) -> ("squirrel" "likes" "dog" "+"))
Blue, round people are not red.
((("someone" "is" "blue" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "-"))
If someone sees the tiger and they do not need the tiger then they are not big.
((("someone" "sees" "tiger" "+") ("someone" "needs" "tiger" "~")) -> ("someone" "is" "big" "-"))
The dog likes the squirrel.
True
1
proof
[(triple1)]
("dog" "likes" "squirrel" "+")
triple1
The tiger is not big.
False
1
inv-proof
[(triple3)]
("tiger" "is" "big" "-")
triple3
The tiger sees the squirrel.
True
2
proof
[(((triple3) -> rule1))]
("tiger" "sees" "squirrel" "+")
((triple3) -> (rule1 % int1))
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int1
The tiger does not see the squirrel.
False
2
inv-proof
[(((triple3) -> rule1))]
("tiger" "sees" "squirrel" "-")
((triple3) -> (rule1 % int1))
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int1
The tiger sees the tiger.
True
3
proof
[(((((triple3) -> rule1)) -> rule4))]
("tiger" "sees" "tiger" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int2
The tiger does not see the tiger.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule4))]
("tiger" "sees" "tiger" "-")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int2
The squirrel does not see the squirrel.
Unknown
inv-rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "sees" "squirrel" "-")
The dog sees the squirrel.
Unknown
rconc
[@1: The dog sees the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "sees" "squirrel" "+")
The squirrel is not young.
Unknown
inv-rconc
[@1: The squirrel is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "young" "-")
The dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
The tiger is not round.
Unknown
inv-random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "-")
The tiger is red.
Unknown
random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "+")
@0: The dog likes the squirrel.[(triple1)] The squirrel likes the dog.[(triple2)] The tiger is big.[(triple3)] @1: The squirrel sees the tiger.[(((triple1) -> rule5))] The tiger sees the squirrel.[(((triple3) -> rule1))] @2: The tiger sees the tiger.[(((((triple3) -> rule1)) -> rule4))]
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
triple1
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
triple2
The tiger is big.
("tiger" "is" "big" "+")
triple3
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
((triple1) -> (rule5 % int1))
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int1
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
((triple3) -> (rule1 % int1))
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int2