The bear visits the rabbit. The rabbit chases the tiger. The rabbit is kind. The tiger chases the bear. The tiger is round. The tiger visits the bear. The tiger visits the rabbit. If the tiger sees the bear and the tiger is red then the tiger chases the rabbit. If something is nice then it sees the bear. If something chases the rabbit then the rabbit chases the tiger. If something is round and it visits the bear then the bear is nice. If something sees the rabbit then the rabbit is kind. If something sees the bear and the bear visits the rabbit then the rabbit visits the bear. If something visits the tiger and it chases the tiger then the tiger visits the rabbit. If something is kind then it sees the tiger.
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If the tiger sees the bear and the tiger is red then the tiger chases the rabbit.
((("tiger" "sees" "bear" "+") ("tiger" "is" "red" "+")) -> ("tiger" "chases" "rabbit" "+"))
If something is nice then it sees the bear.
((("something" "is" "nice" "+")) -> ("something" "sees" "bear" "+"))
If something chases the rabbit then the rabbit chases the tiger.
((("something" "chases" "rabbit" "+")) -> ("rabbit" "chases" "tiger" "+"))
If something is round and it visits the bear then the bear is nice.
((("something" "is" "round" "+") ("something" "visits" "bear" "+")) -> ("bear" "is" "nice" "+"))
If something sees the rabbit then the rabbit is kind.
((("something" "sees" "rabbit" "+")) -> ("rabbit" "is" "kind" "+"))
If something sees the bear and the bear visits the rabbit then the rabbit visits the bear.
((("something" "sees" "bear" "+") ("bear" "visits" "rabbit" "+")) -> ("rabbit" "visits" "bear" "+"))
If something visits the tiger and it chases the tiger then the tiger visits the rabbit.
((("something" "visits" "tiger" "+") ("something" "chases" "tiger" "+")) -> ("tiger" "visits" "rabbit" "+"))
If something is kind then it sees the tiger.
((("something" "is" "kind" "+")) -> ("something" "sees" "tiger" "+"))
The bear visits the rabbit.
True
1
proof
[(triple1)]
("bear" "visits" "rabbit" "+")
triple1
The rabbit is not kind.
False
1
inv-proof
[(triple3)]
("rabbit" "is" "kind" "-")
triple3
The rabbit sees the tiger.
True
2
proof
[(((triple3) -> rule8))]
("rabbit" "sees" "tiger" "+")
((triple3) -> (rule8 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The bear is not nice.
False
3
inv-proof
[(((triple5 triple6) -> rule4))]
("bear" "is" "nice" "-")
((triple5 triple6) -> (rule4 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear sees the bear.
True
4
proof
[(((((triple5 triple6) -> rule4)) -> rule2))]
("bear" "sees" "bear" "+")
((((triple5 triple6) -> (rule4 % int2))) -> (rule2 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear does not see the bear.
False
4
inv-proof
[(((((triple5 triple6) -> rule4)) -> rule2))]
("bear" "sees" "bear" "-")
((((triple5 triple6) -> (rule4 % int2))) -> (rule2 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The rabbit visits the bear.
True
6
proof
[(((((((triple5 triple6) -> rule4)) -> rule2) triple1) -> rule6))]
("rabbit" "visits" "bear" "+")
((((((triple5 triple6) -> (rule4 % int3))) -> (rule2 % int2)) triple1) -> (rule6 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The rabbit does not visit the bear.
False
6
inv-proof
[(((((((triple5 triple6) -> rule4)) -> rule2) triple1) -> rule6))]
("rabbit" "visits" "bear" "-")
((((((triple5 triple6) -> (rule4 % int3))) -> (rule2 % int2)) triple1) -> (rule6 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The tiger does not see the tiger.
Unknown
inv-rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "sees" "tiger" "-")
The tiger chases the rabbit.
Unknown
rconc
[@1: The tiger chases the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "chases" "rabbit" "+")
The rabbit does not see the bear.
Unknown
inv-rconc
[@1: The rabbit sees the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "sees" "bear" "-")
The tiger sees the bear.
Unknown
rconc
[@1: The tiger sees the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "sees" "bear" "+")
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
The tiger is not rough.
Unknown
inv-random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "-")
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 visits the rabbit.[(triple1)] The rabbit chases the tiger.[(triple2)] The rabbit is kind.[(triple3)] The tiger chases the bear.[(triple4)] The tiger is round.[(triple5)] The tiger visits the bear.[(triple6)] The tiger visits the rabbit.[(triple7)] @1: The bear is nice.[(((triple5 triple6) -> rule4))] The rabbit sees the tiger.[(((triple3) -> rule8))] @2: The bear sees the bear.[(((((triple5 triple6) -> rule4)) -> rule2))] @3: The rabbit visits the bear.[(((((((triple5 triple6) -> rule4)) -> rule2) triple1) -> rule6))]
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple1
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple2
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple3
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple4
The tiger is round.
("tiger" "is" "round" "+")
triple5
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple6
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple7
The bear is nice.
("bear" "is" "nice" "+")
((triple5 triple6) -> (rule4 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
((triple3) -> (rule8 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
((((triple5 triple6) -> (rule4 % int2))) -> (rule2 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
((((((triple5 triple6) -> (rule4 % int3))) -> (rule2 % int2)) triple1) -> (rule6 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3