The bear is kind. The rabbit needs the tiger. The tiger chases the bear. If something needs the tiger then it needs the rabbit. If something needs the rabbit and the rabbit needs the tiger then the rabbit chases the bear. If something is young and it chases the tiger then it needs the rabbit. If something sees the tiger then the tiger is blue. Rough things are kind. If something sees the tiger and it is red then it is kind.
The bear is kind.
("bear" "is" "kind" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
If something needs the tiger then it needs the rabbit.
((("something" "needs" "tiger" "+")) -> ("something" "needs" "rabbit" "+"))
If something needs the rabbit and the rabbit needs the tiger then the rabbit chases the bear.
((("something" "needs" "rabbit" "+") ("rabbit" "needs" "tiger" "+")) -> ("rabbit" "chases" "bear" "+"))
If something is young and it chases the tiger then it needs the rabbit.
((("something" "is" "young" "+") ("something" "chases" "tiger" "+")) -> ("something" "needs" "rabbit" "+"))
If something sees the tiger then the tiger is blue.
((("something" "sees" "tiger" "+")) -> ("tiger" "is" "blue" "+"))
Rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If something sees the tiger and it is red then it is kind.
((("something" "sees" "tiger" "+") ("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
The tiger chases the bear.
True
1
proof
[(triple3)]
("tiger" "chases" "bear" "+")
triple3
The rabbit does not need the tiger.
False
1
inv-proof
[(triple2)]
("rabbit" "needs" "tiger" "-")
triple2
The rabbit needs the rabbit.
True
2
proof
[(((triple2) -> rule1))]
("rabbit" "needs" "rabbit" "+")
((triple2) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit does not need the rabbit.
False
2
inv-proof
[(((triple2) -> rule1))]
("rabbit" "needs" "rabbit" "-")
((triple2) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit chases the bear.
True
4
proof
[(((((triple2) -> rule1) triple2) -> rule2))]
("rabbit" "chases" "bear" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit does not chase the bear.
False
4
inv-proof
[(((((triple2) -> rule1) triple2) -> rule2))]
("rabbit" "chases" "bear" "-")
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The tiger is not blue.
Unknown
inv-rconc
[@1: The tiger is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "is" "blue" "-")
The rabbit is kind.
Unknown
rconc
[@1: The rabbit is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "is" "kind" "+")
The tiger does not need the rabbit.
Unknown
inv-rconc
[@1: The tiger needs the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "needs" "rabbit" "-")
The rabbit sees the bear.
Unknown
random
[@0: The rabbit sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "bear" "+")
The tiger is not red.
Unknown
inv-random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "-")
The bear is red.
Unknown
random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "+")
@0: The bear is kind.[(triple1)] The rabbit needs the tiger.[(triple2)] The tiger chases the bear.[(triple3)] @1: The rabbit needs the rabbit.[(((triple2) -> rule1))] @2: The rabbit chases the bear.[(((((triple2) -> rule1) triple2) -> rule2))]
The bear is kind.
("bear" "is" "kind" "+")
triple1
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple2
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple3
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple2) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2