The bear sees the tiger. The rabbit sees the squirrel. The squirrel chases the rabbit. The tiger likes the rabbit. If something is kind then it is nice. If the tiger sees the bear and the bear chases the squirrel then the bear sees the squirrel. If something chases the tiger then it does not like the squirrel. If the rabbit is kind and the rabbit sees the bear then the bear does not chase the rabbit. If something likes the rabbit then the rabbit is kind. If something is big then it does not chase the squirrel. If the squirrel is green then the squirrel does not chase the bear. If something chases the bear then it sees the squirrel.
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
If something is kind then it is nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If the tiger sees the bear and the bear chases the squirrel then the bear sees the squirrel.
((("tiger" "sees" "bear" "+") ("bear" "chases" "squirrel" "+")) -> ("bear" "sees" "squirrel" "+"))
If something chases the tiger then it does not like the squirrel.
((("something" "chases" "tiger" "+")) -> ("something" "likes" "squirrel" "-"))
If the rabbit is kind and the rabbit sees the bear then the bear does not chase the rabbit.
((("rabbit" "is" "kind" "+") ("rabbit" "sees" "bear" "+")) -> ("bear" "chases" "rabbit" "-"))
If something likes the rabbit then the rabbit is kind.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "is" "kind" "+"))
If something is big then it does not chase the squirrel.
((("something" "is" "big" "+")) -> ("something" "chases" "squirrel" "-"))
If the squirrel is green then the squirrel does not chase the bear.
((("squirrel" "is" "green" "+")) -> ("squirrel" "chases" "bear" "-"))
If something chases the bear then it sees the squirrel.
((("something" "chases" "bear" "+")) -> ("something" "sees" "squirrel" "+"))
The rabbit sees the squirrel.
True
1
proof
[(triple2)]
("rabbit" "sees" "squirrel" "+")
triple2
The tiger does not like the rabbit.
False
1
inv-proof
[(triple4)]
("tiger" "likes" "rabbit" "-")
triple4
The rabbit is kind.
True
2
proof
[(((triple4) -> rule5))]
("rabbit" "is" "kind" "+")
((triple4) -> (rule5 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is not kind.
False
2
inv-proof
[(((triple4) -> rule5))]
("rabbit" "is" "kind" "-")
((triple4) -> (rule5 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is nice.
True
3
proof
[(((((triple4) -> rule5)) -> rule1))]
("rabbit" "is" "nice" "+")
((((triple4) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The rabbit is not nice.
False
3
inv-proof
[(((((triple4) -> rule5)) -> rule1))]
("rabbit" "is" "nice" "-")
((((triple4) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The bear does not see the squirrel.
Unknown
inv-rconc
[@1: The bear sees the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "sees" "squirrel" "-")
The squirrel is nice.
Unknown
rconc
[@1: The squirrel is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "nice" "+")
The tiger does not see the squirrel.
Unknown
inv-rconc
[@1: The tiger sees the squirrel.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "sees" "squirrel" "-")
The tiger likes the bear.
Unknown
random
[@0: The tiger likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "bear" "+")
The bear does not chase the rabbit.
Unknown
inv-random
[@0: The bear chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "rabbit" "-")
The bear chases the bear.
Unknown
random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "+")
@0: The bear sees the tiger.[(triple1)] The rabbit sees the squirrel.[(triple2)] The squirrel chases the rabbit.[(triple3)] The tiger likes the rabbit.[(triple4)] @1: The rabbit is kind.[(((triple4) -> rule5))] @2: The rabbit is nice.[(((((triple4) -> rule5)) -> rule1))]
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple2
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
triple3
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple4
The rabbit is kind.
("rabbit" "is" "kind" "+")
((triple4) -> (rule5 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
((((triple4) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2