The mouse chases the squirrel. The squirrel does not chase the mouse. The squirrel sees the mouse. If something visits the mouse then the mouse is not nice. If something is nice and it chases the mouse then the mouse is big. If the mouse is blue then the mouse is green. If the mouse is blue then the mouse is not green. If something chases the squirrel then the squirrel is green. If something is blue then it does not chase the squirrel. If something visits the squirrel and it is not nice then it is blue. If something is green then it is blue.
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The squirrel does not chase the mouse.
("squirrel" "chases" "mouse" "-")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
If something visits the mouse then the mouse is not nice.
((("something" "visits" "mouse" "+")) -> ("mouse" "is" "nice" "-"))
If something is nice and it chases the mouse then the mouse is big.
((("something" "is" "nice" "+") ("something" "chases" "mouse" "+")) -> ("mouse" "is" "big" "+"))
If the mouse is blue then the mouse is green.
((("mouse" "is" "blue" "+")) -> ("mouse" "is" "green" "+"))
If the mouse is blue then the mouse is not green.
((("mouse" "is" "blue" "+")) -> ("mouse" "is" "green" "-"))
If something chases the squirrel then the squirrel is green.
((("something" "chases" "squirrel" "+")) -> ("squirrel" "is" "green" "+"))
If something is blue then it does not chase the squirrel.
((("something" "is" "blue" "+")) -> ("something" "chases" "squirrel" "-"))
If something visits the squirrel and it is not nice then it is blue.
((("something" "visits" "squirrel" "+") ("something" "is" "nice" "~")) -> ("something" "is" "blue" "+"))
If something is green then it is blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
The squirrel does not chase the mouse.
True
1
proof
[(triple2)]
("squirrel" "chases" "mouse" "-")
triple2
The squirrel does not see the mouse.
False
1
inv-proof
[(triple3)]
("squirrel" "sees" "mouse" "-")
triple3
The squirrel is green.
True
2
proof
[(((triple1) -> rule5))]
("squirrel" "is" "green" "+")
((triple1) -> (rule5 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is not green.
False
2
inv-proof
[(((triple1) -> rule5))]
("squirrel" "is" "green" "-")
((triple1) -> (rule5 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is blue.
True
3
proof
[(((((triple1) -> rule5)) -> rule8))]
("squirrel" "is" "blue" "+")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel is not blue.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule8))]
("squirrel" "is" "blue" "-")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel does not chase the squirrel.
True
4
proof
[(((((((triple1) -> rule5)) -> rule8)) -> rule6))]
("squirrel" "chases" "squirrel" "-")
((((((triple1) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The squirrel does not chase the squirrel.
("squirrel" "chases" "squirrel" "-")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is green.
("squirrel" "is" "green" "+")
int3
The squirrel chases the squirrel.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule8)) -> rule6))]
("squirrel" "chases" "squirrel" "+")
((((((triple1) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The squirrel does not chase the squirrel.
("squirrel" "chases" "squirrel" "-")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is green.
("squirrel" "is" "green" "+")
int3
The mouse is not green.
Unknown
inv-rconc
[@2: The mouse is green.[CWA. Example of deepest failure = (rule3 <- rule7 <- FAIL)]]
("mouse" "is" "green" "-")
The mouse is blue.
Unknown
rconc
[@3: The mouse is blue.[CWA. Example of deepest failure = (rule8 <- rule3 <- rule7 <- FAIL)]]
("mouse" "is" "blue" "+")
The mouse is not big.
Unknown
inv-rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "big" "-")
The squirrel is cold.
Unknown
random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
The squirrel is not big.
Unknown
inv-random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "-")
The mouse sees the squirrel.
Unknown
random
[@0: The mouse sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "squirrel" "+")
@0: The mouse chases the squirrel.[(triple1)] The squirrel does not chase the mouse.[(triple2)] The squirrel sees the mouse.[(triple3)] @1: The squirrel is green.[(((triple1) -> rule5))] @2: The squirrel is blue.[(((((triple1) -> rule5)) -> rule8))] @3: The squirrel does not chase the squirrel.[(((((((triple1) -> rule5)) -> rule8)) -> rule6))]
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple1
The squirrel does not chase the mouse.
("squirrel" "chases" "mouse" "-")
triple2
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple3
The squirrel is green.
("squirrel" "is" "green" "+")
((triple1) -> (rule5 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel does not chase the squirrel.
("squirrel" "chases" "squirrel" "-")
((((((triple1) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The squirrel does not chase the squirrel.
("squirrel" "chases" "squirrel" "-")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is green.
("squirrel" "is" "green" "+")
int3