The bear chases the dog. The dog sees the mouse. The mouse needs the tiger. The tiger is blue. If something chases the bear then it sees the mouse. If the mouse needs the tiger then the mouse chases the bear. If something is blue and nice then it needs the bear.
The bear chases the dog.
("bear" "chases" "dog" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
If something chases the bear then it sees the mouse.
((("something" "chases" "bear" "+")) -> ("something" "sees" "mouse" "+"))
If the mouse needs the tiger then the mouse chases the bear.
((("mouse" "needs" "tiger" "+")) -> ("mouse" "chases" "bear" "+"))
If something is blue and nice then it needs the bear.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "needs" "bear" "+"))
The bear chases the dog.
True
1
proof
[(triple1)]
("bear" "chases" "dog" "+")
triple1
The mouse does not need the tiger.
False
1
inv-proof
[(triple3)]
("mouse" "needs" "tiger" "-")
triple3
The mouse chases the bear.
True
2
proof
[(((triple3) -> rule2))]
("mouse" "chases" "bear" "+")
((triple3) -> (rule2 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse does not chase the bear.
False
2
inv-proof
[(((triple3) -> rule2))]
("mouse" "chases" "bear" "-")
((triple3) -> (rule2 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse sees the mouse.
True
3
proof
[(((((triple3) -> rule2)) -> rule1))]
("mouse" "sees" "mouse" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int2
The mouse does not see the mouse.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule1))]
("mouse" "sees" "mouse" "-")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int2
The dog does not need the bear.
Unknown
inv-rconc
[@1: The dog needs the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "needs" "bear" "-")
The bear needs the bear.
Unknown
rconc
[@1: The bear needs the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "needs" "bear" "+")
The bear does not see the mouse.
Unknown
inv-rconc
[@1: The bear sees the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "sees" "mouse" "-")
The tiger sees the dog.
Unknown
random
[@0: The tiger sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "dog" "+")
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The tiger sees the bear.
Unknown
random
[@0: The tiger sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "bear" "+")
@0: The bear chases the dog.[(triple1)] The dog sees the mouse.[(triple2)] The mouse needs the tiger.[(triple3)] The tiger is blue.[(triple4)] @1: The mouse chases the bear.[(((triple3) -> rule2))] @2: The mouse sees the mouse.[(((((triple3) -> rule2)) -> rule1))]
The bear chases the dog.
("bear" "chases" "dog" "+")
triple1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple2
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple3
The tiger is blue.
("tiger" "is" "blue" "+")
triple4
The mouse chases the bear.
("mouse" "chases" "bear" "+")
((triple3) -> (rule2 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int2