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