The bear sees the squirrel. The bear sees the tiger. The rabbit chases the squirrel. The rabbit does not chase the tiger. The squirrel chases the tiger. The squirrel is young. The squirrel does not like the rabbit. The squirrel does not see the tiger. The tiger is red. The tiger likes the squirrel. If someone sees the rabbit then the rabbit sees the tiger. If the rabbit likes the squirrel then the rabbit does not like the tiger. If someone sees the squirrel and they are not round then the squirrel chases the tiger. If someone is kind then they chase the squirrel. If someone sees the tiger then they see the rabbit. If someone is young and not red then they are nice. If someone is red and they like the squirrel then they see the tiger. If someone sees the tiger then they are kind.
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
The rabbit does not chase the tiger.
("rabbit" "chases" "tiger" "-")
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel does not like the rabbit.
("squirrel" "likes" "rabbit" "-")
The squirrel does not see the tiger.
("squirrel" "sees" "tiger" "-")
The tiger is red.
("tiger" "is" "red" "+")
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
If someone sees the rabbit then the rabbit sees the tiger.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "sees" "tiger" "+"))
If the rabbit likes the squirrel then the rabbit does not like the tiger.
((("rabbit" "likes" "squirrel" "+")) -> ("rabbit" "likes" "tiger" "-"))
If someone sees the squirrel and they are not round then the squirrel chases the tiger.
((("someone" "sees" "squirrel" "+") ("someone" "is" "round" "~")) -> ("squirrel" "chases" "tiger" "+"))
If someone is kind then they chase the squirrel.
((("someone" "is" "kind" "+")) -> ("someone" "chases" "squirrel" "+"))
If someone sees the tiger then they see the rabbit.
((("someone" "sees" "tiger" "+")) -> ("someone" "sees" "rabbit" "+"))
If someone is young and not red then they are nice.
((("someone" "is" "young" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "nice" "+"))
If someone is red and they like the squirrel then they see the tiger.
((("someone" "is" "red" "+") ("someone" "likes" "squirrel" "+")) -> ("someone" "sees" "tiger" "+"))
If someone sees the tiger then they are kind.
((("someone" "sees" "tiger" "+")) -> ("someone" "is" "kind" "+"))
The squirrel chases the tiger.
True
1
proof
[(triple5)]
("squirrel" "chases" "tiger" "+")
triple5
The tiger does not like the squirrel.
False
1
inv-proof
[(triple10)]
("tiger" "likes" "squirrel" "-")
triple10
The tiger sees the tiger.
True
3
proof
[(((triple9 triple10) -> rule7))]
("tiger" "sees" "tiger" "+")
((triple9 triple10) -> (rule7 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger does not see the tiger.
False
3
inv-proof
[(((triple9 triple10) -> rule7))]
("tiger" "sees" "tiger" "-")
((triple9 triple10) -> (rule7 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is kind.
True
4
proof
[(((((triple9 triple10) -> rule7)) -> rule8))]
("tiger" "is" "kind" "+")
((((triple9 triple10) -> (rule7 % int2))) -> (rule8 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger does not see the rabbit.
False
4
inv-proof
[(((((triple9 triple10) -> rule7)) -> rule5))]
("tiger" "sees" "rabbit" "-")
((((triple9 triple10) -> (rule7 % int2))) -> (rule5 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The rabbit sees the rabbit.
True
4
proof
[(((((((triple2) -> rule5)) -> rule1)) -> rule5) OR ((((((((triple9 triple10) -> rule7)) -> rule5)) -> rule1)) -> rule5))]
("rabbit" "sees" "rabbit" "+")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int3
((((((((triple9 triple10) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int3
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int4
The rabbit is not kind.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule1)) -> rule8) OR ((((((((triple9 triple10) -> rule7)) -> rule5)) -> rule1)) -> rule8))]
("rabbit" "is" "kind" "-")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int3
((((((((triple9 triple10) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int3
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int4
The bear is not nice.
Unknown
inv-rconc
[@1: The bear is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "is" "nice" "-")
The tiger is nice.
Unknown
rconc
[@1: The tiger is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "is" "nice" "+")
The squirrel is not nice.
Unknown
inv-rconc
[@1: The squirrel is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "is" "nice" "-")
The squirrel is kind.
Unknown
rconc
[@1: The squirrel is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "is" "kind" "+")
The tiger does not see the squirrel.
Unknown
inv-random
[@0: The tiger sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "squirrel" "-")
The squirrel is red.
Unknown
random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "+")
The rabbit does not chase the bear.
Unknown
inv-random
[@0: The rabbit chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "bear" "-")
The bear likes the rabbit.
Unknown
random
[@0: The bear likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "rabbit" "+")
@0: The bear sees the squirrel.[(triple1)] The bear sees the tiger.[(triple2)] The rabbit chases the squirrel.[(triple3 OR ((((((((triple2) -> rule5)) -> rule1)) -> rule8)) -> rule4) OR ((((((((((triple9 triple10) -> rule7)) -> rule5)) -> rule1)) -> rule8)) -> rule4))] The rabbit does not chase the tiger.[(triple4)] The squirrel chases the tiger.[(triple5)] The squirrel does not like the rabbit.[(triple7)] The squirrel does not see the tiger.[(triple8)] The squirrel is young.[(triple6)] The tiger is red.[(triple9)] The tiger likes the squirrel.[(triple10)] @1: The bear is kind.[(((triple2) -> rule8))] The bear sees the rabbit.[(((triple2) -> rule5))] The tiger sees the tiger.[(((triple9 triple10) -> rule7))] @2: The bear chases the squirrel.[(((((triple2) -> rule8)) -> rule4))] The rabbit sees the tiger.[(((((triple2) -> rule5)) -> rule1) OR ((((((triple9 triple10) -> rule7)) -> rule5)) -> rule1))] The tiger is kind.[(((((triple9 triple10) -> rule7)) -> rule8))] The tiger sees the rabbit.[(((((triple9 triple10) -> rule7)) -> rule5))] @3: The rabbit is kind.[(((((((triple2) -> rule5)) -> rule1)) -> rule8) OR ((((((((triple9 triple10) -> rule7)) -> rule5)) -> rule1)) -> rule8))] The rabbit sees the rabbit.[(((((((triple2) -> rule5)) -> rule1)) -> rule5) OR ((((((((triple9 triple10) -> rule7)) -> rule5)) -> rule1)) -> rule5))] The tiger chases the squirrel.[(((((((triple9 triple10) -> rule7)) -> rule8)) -> rule4))]
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple2
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
triple3
((((((((triple2) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int3
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int4
((((((((((triple9 triple10) -> (rule7 % int5))) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int3
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int4
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int5
The rabbit does not chase the tiger.
("rabbit" "chases" "tiger" "-")
triple4
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple5
The squirrel does not like the rabbit.
("squirrel" "likes" "rabbit" "-")
triple7
The squirrel does not see the tiger.
("squirrel" "sees" "tiger" "-")
triple8
The squirrel is young.
("squirrel" "is" "young" "+")
triple6
The tiger is red.
("tiger" "is" "red" "+")
triple9
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
triple10
The bear is kind.
("bear" "is" "kind" "+")
((triple2) -> (rule8 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
((triple2) -> (rule5 % int1))
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((triple9 triple10) -> (rule7 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
((((triple2) -> (rule8 % int2))) -> (rule4 % int1))
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int2
((((((triple9 triple10) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int2
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int3
The tiger is kind.
("tiger" "is" "kind" "+")
((((triple9 triple10) -> (rule7 % int2))) -> (rule8 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
((((triple9 triple10) -> (rule7 % int2))) -> (rule5 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The rabbit is kind.
("rabbit" "is" "kind" "+")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int3
((((((((triple9 triple10) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int3
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int4
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int3
((((((((triple9 triple10) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int3
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int4
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
((((((triple9 triple10) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int3