The bear eats the mouse. The bear is not cold. The mouse does not eat the bear. If something is green then it is not round. If something eats the mouse and it eats the bear then the mouse does not see the bear. If the mouse eats the bear and the mouse is not blue then the bear does not eat the mouse. If something eats the mouse then the mouse is green. If something sees the mouse then it is green. If the mouse is not round then the mouse chases the bear.
The bear eats the mouse.
("bear" "eats" "mouse" "+")
The bear is not cold.
("bear" "is" "cold" "-")
The mouse does not eat the bear.
("mouse" "eats" "bear" "-")
If something is green then it is not round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "-"))
If something eats the mouse and it eats the bear then the mouse does not see the bear.
((("something" "eats" "mouse" "+") ("something" "eats" "bear" "+")) -> ("mouse" "sees" "bear" "-"))
If the mouse eats the bear and the mouse is not blue then the bear does not eat the mouse.
((("mouse" "eats" "bear" "+") ("mouse" "is" "blue" "~")) -> ("bear" "eats" "mouse" "-"))
If something eats the mouse then the mouse is green.
((("something" "eats" "mouse" "+")) -> ("mouse" "is" "green" "+"))
If something sees the mouse then it is green.
((("something" "sees" "mouse" "+")) -> ("something" "is" "green" "+"))
If the mouse is not round then the mouse chases the bear.
((("mouse" "is" "round" "~")) -> ("mouse" "chases" "bear" "+"))
The bear eats the mouse.
True
1
proof
[(triple1)]
("bear" "eats" "mouse" "+")
triple1
The bear does not eat the mouse.
False
1
inv-proof
[(triple1)]
("bear" "eats" "mouse" "-")
triple1
The mouse is green.
True
2
proof
[(((triple1) -> rule4))]
("mouse" "is" "green" "+")
((triple1) -> (rule4 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is not green.
False
2
inv-proof
[(((triple1) -> rule4))]
("mouse" "is" "green" "-")
((triple1) -> (rule4 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is not round.
True
3
proof
[(((((triple1) -> rule4)) -> rule1))]
("mouse" "is" "round" "-")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The mouse is not round.
("mouse" "is" "round" "-")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse is round.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule1))]
("mouse" "is" "round" "+")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The mouse is not round.
("mouse" "is" "round" "-")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse chases the bear.
True
4
proof
[(((((((triple1) -> rule4)) -> rule1)) -> rule6))]
("mouse" "chases" "bear" "+")
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse is not round.
("mouse" "is" "round" "-")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
The mouse does not chase the bear.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule1)) -> rule6))]
("mouse" "chases" "bear" "-")
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse is not round.
("mouse" "is" "round" "-")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
The bear is not green.
Unknown
inv-rconc
[@1: The bear is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "is" "green" "-")
The bear is round.
Unknown
random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "+")
The bear does not chase the bear.
Unknown
inv-random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
The bear does not eat the bear.
Unknown
inv-random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "-")
The bear is blue.
Unknown
random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "+")
The bear does not see the mouse.
Unknown
inv-random
[@0: The bear sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "mouse" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
@0: The bear eats the mouse.[(triple1)] The bear is not cold.[(triple2)] The mouse does not eat the bear.[(triple3)] @1: The mouse is green.[(((triple1) -> rule4))] @2: The mouse is not round.[(((((triple1) -> rule4)) -> rule1))] @3: The mouse chases the bear.[(((((((triple1) -> rule4)) -> rule1)) -> rule6))]
The bear eats the mouse.
("bear" "eats" "mouse" "+")
triple1
The bear is not cold.
("bear" "is" "cold" "-")
triple2
The mouse does not eat the bear.
("mouse" "eats" "bear" "-")
triple3
The mouse is green.
("mouse" "is" "green" "+")
((triple1) -> (rule4 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is not round.
("mouse" "is" "round" "-")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The mouse is not round.
("mouse" "is" "round" "-")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse chases the bear.
("mouse" "chases" "bear" "+")
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The mouse chases the bear.
("mouse" "chases" "bear" "+")
int1
The mouse is not round.
("mouse" "is" "round" "-")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3