The bear chases the rabbit. The bear is blue. The bear visits the tiger. The rabbit is kind. The rabbit visits the bear. The tiger chases the bear. The tiger visits the bear. If someone is green and they visit the tiger then they eat the rabbit. If someone chases the bear then the bear is green. If someone is green and they eat the rabbit then they are kind.
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
If someone is green and they visit the tiger then they eat the rabbit.
((("someone" "is" "green" "+") ("someone" "visits" "tiger" "+")) -> ("someone" "eats" "rabbit" "+"))
If someone chases the bear then the bear is green.
((("someone" "chases" "bear" "+")) -> ("bear" "is" "green" "+"))
If someone is green and they eat the rabbit then they are kind.
((("someone" "is" "green" "+") ("someone" "eats" "rabbit" "+")) -> ("someone" "is" "kind" "+"))
The rabbit is kind.
True
1
proof
[(triple4)]
("rabbit" "is" "kind" "+")
triple4
The rabbit is not kind.
False
1
inv-proof
[(triple4)]
("rabbit" "is" "kind" "-")
triple4
The bear is green.
True
2
proof
[(((triple6) -> rule2))]
("bear" "is" "green" "+")
((triple6) -> (rule2 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear is not green.
False
2
inv-proof
[(((triple6) -> rule2))]
("bear" "is" "green" "-")
((triple6) -> (rule2 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear eats the rabbit.
True
4
proof
[(((((triple6) -> rule2) triple3) -> rule1))]
("bear" "eats" "rabbit" "+")
((((triple6) -> (rule2 % int2)) triple3) -> (rule1 % int1))
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
The bear does not eat the rabbit.
False
4
inv-proof
[(((((triple6) -> rule2) triple3) -> rule1))]
("bear" "eats" "rabbit" "-")
((((triple6) -> (rule2 % int2)) triple3) -> (rule1 % int1))
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
The bear is kind.
True
7
proof
[(((((triple6) -> rule2) ((((triple6) -> rule2) triple3) -> rule1)) -> rule3))]
("bear" "is" "kind" "+")
((((triple6) -> (rule2 % int3)) ((((triple6) -> (rule2 % int3)) triple3) -> (rule1 % int2))) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int2
The bear is green.
("bear" "is" "green" "+")
int3
The bear is not kind.
False
7
inv-proof
[(((((triple6) -> rule2) ((((triple6) -> rule2) triple3) -> rule1)) -> rule3))]
("bear" "is" "kind" "-")
((((triple6) -> (rule2 % int3)) ((((triple6) -> (rule2 % int3)) triple3) -> (rule1 % int2))) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int2
The bear is green.
("bear" "is" "green" "+")
int3
The rabbit does not eat the rabbit.
Unknown
inv-rconc
[@1: The rabbit eats the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "eats" "rabbit" "-")
The tiger eats the rabbit.
Unknown
rconc
[@1: The tiger eats the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "eats" "rabbit" "+")
The tiger is not kind.
Unknown
inv-rconc
[@1: The tiger is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "kind" "-")
The tiger eats the bear.
Unknown
random
[@0: The tiger eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "bear" "+")
The rabbit does not chase the tiger.
Unknown
inv-random
[@0: The rabbit chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "tiger" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
The bear does not visit the rabbit.
Unknown
inv-random
[@0: The bear visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "rabbit" "-")
The rabbit eats the tiger.
Unknown
random
[@0: The rabbit eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "tiger" "+")
@0: The bear chases the rabbit.[(triple1)] The bear is blue.[(triple2)] The bear visits the tiger.[(triple3)] The rabbit is kind.[(triple4)] The rabbit visits the bear.[(triple5)] The tiger chases the bear.[(triple6)] The tiger visits the bear.[(triple7)] @1: The bear is green.[(((triple6) -> rule2))] @2: The bear eats the rabbit.[(((((triple6) -> rule2) triple3) -> rule1))] @3: The bear is kind.[(((((triple6) -> rule2) ((((triple6) -> rule2) triple3) -> rule1)) -> rule3))]
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple1
The bear is blue.
("bear" "is" "blue" "+")
triple2
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple3
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple4
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
triple5
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple6
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple7
The bear is green.
("bear" "is" "green" "+")
((triple6) -> (rule2 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
((((triple6) -> (rule2 % int2)) triple3) -> (rule1 % int1))
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
The bear is kind.
("bear" "is" "kind" "+")
((((triple6) -> (rule2 % int3)) ((((triple6) -> (rule2 % int3)) triple3) -> (rule1 % int2))) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int2
The bear is green.
("bear" "is" "green" "+")
int3