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