The bear needs the tiger. The mouse is green. The tiger chases the mouse. If something visits the bear then it visits the mouse. If something chases the tiger then it visits the mouse. If something chases the bear then the bear visits the mouse. If the mouse is green then the mouse chases the bear. If something chases the tiger then the tiger is red. If something chases the mouse then the mouse needs the tiger. If something visits the tiger then the tiger visits the bear. If the bear visits the mouse and the mouse visits the tiger then the mouse visits the bear.
The bear needs the tiger.
("bear" "needs" "tiger" "+")
The mouse is green.
("mouse" "is" "green" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
If something visits the bear then it visits the mouse.
((("something" "visits" "bear" "+")) -> ("something" "visits" "mouse" "+"))
If something chases the tiger then it visits the mouse.
((("something" "chases" "tiger" "+")) -> ("something" "visits" "mouse" "+"))
If something chases the bear then the bear visits the mouse.
((("something" "chases" "bear" "+")) -> ("bear" "visits" "mouse" "+"))
If the mouse is green then the mouse chases the bear.
((("mouse" "is" "green" "+")) -> ("mouse" "chases" "bear" "+"))
If something chases the tiger then the tiger is red.
((("something" "chases" "tiger" "+")) -> ("tiger" "is" "red" "+"))
If something chases the mouse then the mouse needs the tiger.
((("something" "chases" "mouse" "+")) -> ("mouse" "needs" "tiger" "+"))
If something visits the tiger then the tiger visits the bear.
((("something" "visits" "tiger" "+")) -> ("tiger" "visits" "bear" "+"))
If the bear visits the mouse and the mouse visits the tiger then the mouse visits the bear.
((("bear" "visits" "mouse" "+") ("mouse" "visits" "tiger" "+")) -> ("mouse" "visits" "bear" "+"))
The bear needs the tiger.
True
1
proof
[(triple1)]
("bear" "needs" "tiger" "+")
triple1
The mouse is not green.
False
1
inv-proof
[(triple2)]
("mouse" "is" "green" "-")
triple2
The mouse needs the tiger.
True
2
proof
[(((triple3) -> rule6))]
("mouse" "needs" "tiger" "+")
((triple3) -> (rule6 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The mouse does not need the tiger.
False
2
inv-proof
[(((triple3) -> rule6))]
("mouse" "needs" "tiger" "-")
((triple3) -> (rule6 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The bear visits the mouse.
True
3
proof
[(((((triple2) -> rule4)) -> rule3))]
("bear" "visits" "mouse" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int1
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int2
The bear does not visit the mouse.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule3))]
("bear" "visits" "mouse" "-")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int1
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int2
The tiger is not red.
Unknown
inv-rconc
[@1: The tiger is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "is" "red" "-")
The mouse visits the bear.
Unknown
rconc
[@1: The mouse visits the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "visits" "bear" "+")
The tiger does not visit the mouse.
Unknown
inv-rconc
[@2: The tiger visits the mouse.[CWA. Example of deepest failure = (rule1 <- rule7 <- FAIL)]]
("tiger" "visits" "mouse" "-")
The mouse chases the tiger.
Unknown
random
[@0: The mouse chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "tiger" "+")
The bear is not kind.
Unknown
inv-random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
@0: The bear needs the tiger.[(triple1)] The mouse is green.[(triple2)] The tiger chases the mouse.[(triple3)] @1: The mouse chases the bear.[(((triple2) -> rule4))] The mouse needs the tiger.[(((triple3) -> rule6))] @2: The bear visits the mouse.[(((((triple2) -> rule4)) -> rule3))]
The bear needs the tiger.
("bear" "needs" "tiger" "+")
triple1
The mouse is green.
("mouse" "is" "green" "+")
triple2
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple3
The mouse chases the bear.
("mouse" "chases" "bear" "+")
((triple2) -> (rule4 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
((triple3) -> (rule6 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The bear visits the mouse.
("bear" "visits" "mouse" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int1
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int2