The mouse chases the squirrel. The squirrel eats the mouse. If someone is red and they chase the mouse then the mouse eats the squirrel. If the squirrel visits the mouse and the mouse eats the squirrel then the squirrel chases the mouse. If someone is cold then they visit the squirrel. If someone is cold then they eat the squirrel. If the mouse chases the squirrel then the mouse is cold. If someone visits the squirrel then they chase the mouse.
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
If someone is red and they chase the mouse then the mouse eats the squirrel.
((("someone" "is" "red" "+") ("someone" "chases" "mouse" "+")) -> ("mouse" "eats" "squirrel" "+"))
If the squirrel visits the mouse and the mouse eats the squirrel then the squirrel chases the mouse.
((("squirrel" "visits" "mouse" "+") ("mouse" "eats" "squirrel" "+")) -> ("squirrel" "chases" "mouse" "+"))
If someone is cold then they visit the squirrel.
((("someone" "is" "cold" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone is cold then they eat the squirrel.
((("someone" "is" "cold" "+")) -> ("someone" "eats" "squirrel" "+"))
If the mouse chases the squirrel then the mouse is cold.
((("mouse" "chases" "squirrel" "+")) -> ("mouse" "is" "cold" "+"))
If someone visits the squirrel then they chase the mouse.
((("someone" "visits" "squirrel" "+")) -> ("someone" "chases" "mouse" "+"))
The mouse chases the squirrel.
True
1
proof
[(triple1)]
("mouse" "chases" "squirrel" "+")
triple1
The mouse does not chase the squirrel.
False
1
inv-proof
[(triple1)]
("mouse" "chases" "squirrel" "-")
triple1
The mouse is cold.
True
2
proof
[(((triple1) -> rule5))]
("mouse" "is" "cold" "+")
((triple1) -> (rule5 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is not cold.
False
2
inv-proof
[(((triple1) -> rule5))]
("mouse" "is" "cold" "-")
((triple1) -> (rule5 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse eats the squirrel.
True
3
proof
[(((((triple1) -> rule5)) -> rule4))]
("mouse" "eats" "squirrel" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse does not eat the squirrel.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule4))]
("mouse" "eats" "squirrel" "-")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse chases the mouse.
True
4
proof
[(((((((triple1) -> rule5)) -> rule3)) -> rule6))]
("mouse" "chases" "mouse" "+")
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
The mouse does not chase the mouse.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule3)) -> rule6))]
("mouse" "chases" "mouse" "-")
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
The squirrel does not chase the mouse.
Unknown
inv-rconc
[@2: The squirrel chases the mouse.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("squirrel" "chases" "mouse" "-")
The squirrel eats the squirrel.
Unknown
rconc
[@1: The squirrel eats the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "eats" "squirrel" "+")
The squirrel does not visit the squirrel.
Unknown
inv-rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "visits" "squirrel" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
The squirrel is not blue.
Unknown
inv-random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
The mouse is not red.
Unknown
inv-random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "-")
The squirrel visits the mouse.
Unknown
random
[@0: The squirrel visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "mouse" "+")
@0: The mouse chases the squirrel.[(triple1)] The squirrel eats the mouse.[(triple2)] @1: The mouse is cold.[(((triple1) -> rule5))] @2: The mouse eats the squirrel.[(((((triple1) -> rule5)) -> rule4))] The mouse visits the squirrel.[(((((triple1) -> rule5)) -> rule3))] @3: The mouse chases the mouse.[(((((((triple1) -> rule5)) -> rule3)) -> rule6))]
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple2
The mouse is cold.
("mouse" "is" "cold" "+")
((triple1) -> (rule5 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3