The bear needs the mouse. The mouse likes the bear. The tiger sees the bear. If someone sees the tiger and the tiger sees the bear then they like the mouse. If someone sees the bear then they see the tiger.
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
If someone sees the tiger and the tiger sees the bear then they like the mouse.
((("someone" "sees" "tiger" "+") ("tiger" "sees" "bear" "+")) -> ("someone" "likes" "mouse" "+"))
If someone sees the bear then they see the tiger.
((("someone" "sees" "bear" "+")) -> ("someone" "sees" "tiger" "+"))
The tiger sees the bear.
True
1
proof
[(triple3)]
("tiger" "sees" "bear" "+")
triple3
The bear does not need the mouse.
False
1
inv-proof
[(triple1)]
("bear" "needs" "mouse" "-")
triple1
The tiger sees the tiger.
True
2
proof
[(((triple3) -> rule2))]
("tiger" "sees" "tiger" "+")
((triple3) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger does not see the tiger.
False
2
inv-proof
[(((triple3) -> rule2))]
("tiger" "sees" "tiger" "-")
((triple3) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger likes the mouse.
True
4
proof
[(((((triple3) -> rule2) triple3) -> rule1))]
("tiger" "likes" "mouse" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger does not like the mouse.
False
4
inv-proof
[(((((triple3) -> rule2) triple3) -> rule1))]
("tiger" "likes" "mouse" "-")
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The bear does not see the tiger.
Unknown
inv-rconc
[@1: The bear sees the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "sees" "tiger" "-")
The bear likes the mouse.
Unknown
rconc
[@2: The bear likes the mouse.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("bear" "likes" "mouse" "+")
The mouse does not see the tiger.
Unknown
inv-rconc
[@1: The mouse sees the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "sees" "tiger" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
The tiger does not need the mouse.
Unknown
inv-random
[@0: The tiger needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "mouse" "-")
The mouse sees the bear.
Unknown
random
[@0: The mouse sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "bear" "+")
@0: The bear needs the mouse.[(triple1)] The mouse likes the bear.[(triple2)] The tiger sees the bear.[(triple3)] @1: The tiger sees the tiger.[(((triple3) -> rule2))] @2: The tiger likes the mouse.[(((((triple3) -> rule2) triple3) -> rule1))]
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple1
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple2
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple3
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((triple3) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
((((triple3) -> (rule2 % int2)) triple3) -> (rule1 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2