The bear visits the rabbit. The rabbit visits the tiger. The tiger is big. If someone is big then they visit the tiger. If someone visits the tiger and the tiger does not see the bear then the bear visits the rabbit. If someone needs the tiger then they do not visit the bear. If someone is nice and not young then they visit the rabbit. If someone needs the tiger and they visit the rabbit then they are not big. If someone visits the tiger then they need the tiger. If someone sees the bear and they do not see the tiger then the bear does not need the rabbit. If someone sees the tiger then they do not need the rabbit.
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
If someone is big then they visit the tiger.
((("someone" "is" "big" "+")) -> ("someone" "visits" "tiger" "+"))
If someone visits the tiger and the tiger does not see the bear then the bear visits the rabbit.
((("someone" "visits" "tiger" "+") ("tiger" "sees" "bear" "~")) -> ("bear" "visits" "rabbit" "+"))
If someone needs the tiger then they do not visit the bear.
((("someone" "needs" "tiger" "+")) -> ("someone" "visits" "bear" "-"))
If someone is nice and not young then they visit the rabbit.
((("someone" "is" "nice" "+") ("someone" "is" "young" "~")) -> ("someone" "visits" "rabbit" "+"))
If someone needs the tiger and they visit the rabbit then they are not big.
((("someone" "needs" "tiger" "+") ("someone" "visits" "rabbit" "+")) -> ("someone" "is" "big" "-"))
If someone visits the tiger then they need the tiger.
((("someone" "visits" "tiger" "+")) -> ("someone" "needs" "tiger" "+"))
If someone sees the bear and they do not see the tiger then the bear does not need the rabbit.
((("someone" "sees" "bear" "+") ("someone" "sees" "tiger" "~")) -> ("bear" "needs" "rabbit" "-"))
If someone sees the tiger then they do not need the rabbit.
((("someone" "sees" "tiger" "+")) -> ("someone" "needs" "rabbit" "-"))
The bear visits the rabbit.
True
1
proof
[(triple1)]
("bear" "visits" "rabbit" "+")
triple1
The bear does not visit the rabbit.
False
1
inv-proof
[(triple1)]
("bear" "visits" "rabbit" "-")
triple1
The rabbit needs the tiger.
True
2
proof
[(((triple2) -> rule6))]
("rabbit" "needs" "tiger" "+")
((triple2) -> (rule6 % int1))
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int1
The tiger does not visit the tiger.
False
2
inv-proof
[(((triple3) -> rule1))]
("tiger" "visits" "tiger" "-")
((triple3) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger needs the tiger.
True
3
proof
[(((((triple3) -> rule1)) -> rule6))]
("tiger" "needs" "tiger" "+")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The rabbit visits the bear.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule3))]
("rabbit" "visits" "bear" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit does not visit the bear.
("rabbit" "visits" "bear" "-")
int1
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int2
The tiger does not visit the bear.
True
4
proof
[(((((((triple3) -> rule1)) -> rule6)) -> rule3))]
("tiger" "visits" "bear" "-")
((((((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The tiger does not visit the bear.
("tiger" "visits" "bear" "-")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int3
The tiger visits the bear.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule6)) -> rule3))]
("tiger" "visits" "bear" "+")
((((((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The tiger does not visit the bear.
("tiger" "visits" "bear" "-")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int3
The tiger does not visit the rabbit.
Unknown
inv-rconc
[@1: The tiger visits the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "visits" "rabbit" "-")
The bear visits the tiger.
Unknown
rconc
[@1: The bear visits the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "visits" "tiger" "+")
The bear does not need the tiger.
Unknown
inv-rconc
[@2: The bear needs the tiger.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("bear" "needs" "tiger" "-")
The rabbit visits the rabbit.
Unknown
rconc
[@1: The rabbit visits the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "visits" "rabbit" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The tiger is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
The rabbit is not young.
Unknown
inv-random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "-")
The bear sees the tiger.
Unknown
random
[@0: The bear sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "tiger" "+")
@0: The bear visits the rabbit.[(triple1)] The rabbit visits the tiger.[(triple2)] The tiger is big.[(triple3)] @1: The rabbit needs the tiger.[(((triple2) -> rule6))] The tiger visits the tiger.[(((triple3) -> rule1))] @2: The rabbit does not visit the bear.[(((((triple2) -> rule6)) -> rule3))] The tiger needs the tiger.[(((((triple3) -> rule1)) -> rule6))] @3: The tiger does not visit the bear.[(((((((triple3) -> rule1)) -> rule6)) -> rule3))]
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple2
The tiger is big.
("tiger" "is" "big" "+")
triple3
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
((triple2) -> (rule6 % int1))
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((triple3) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The rabbit does not visit the bear.
("rabbit" "visits" "bear" "-")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit does not visit the bear.
("rabbit" "visits" "bear" "-")
int1
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The tiger does not visit the bear.
("tiger" "visits" "bear" "-")
((((((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The tiger does not visit the bear.
("tiger" "visits" "bear" "-")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int3