The cat eats the mouse. The mouse eats the cat. The mouse eats the squirrel. The mouse visits the cat. The mouse visits the squirrel. The squirrel eats the cat. The squirrel visits the cat. If someone eats the squirrel then they are blue. If someone eats the squirrel then they chase the mouse. If someone is blue and they visit the cat then the cat eats the squirrel.
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
If someone eats the squirrel then they are blue.
((("someone" "eats" "squirrel" "+")) -> ("someone" "is" "blue" "+"))
If someone eats the squirrel then they chase the mouse.
((("someone" "eats" "squirrel" "+")) -> ("someone" "chases" "mouse" "+"))
If someone is blue and they visit the cat then the cat eats the squirrel.
((("someone" "is" "blue" "+") ("someone" "visits" "cat" "+")) -> ("cat" "eats" "squirrel" "+"))
The cat eats the mouse.
True
1
proof
[(triple1)]
("cat" "eats" "mouse" "+")
triple1
The cat does not eat the mouse.
False
1
inv-proof
[(triple1)]
("cat" "eats" "mouse" "-")
triple1
The mouse chases the mouse.
True
2
proof
[(((triple3) -> rule2))]
("mouse" "chases" "mouse" "+")
((triple3) -> (rule2 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is not blue.
False
2
inv-proof
[(((triple3) -> rule1))]
("mouse" "is" "blue" "-")
((triple3) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The cat eats the squirrel.
True
4
proof
[(((((triple3) -> rule1) triple4) -> rule3))]
("cat" "eats" "squirrel" "+")
((((triple3) -> (rule1 % int2)) triple4) -> (rule3 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The cat does not eat the squirrel.
False
4
inv-proof
[(((((triple3) -> rule1) triple4) -> rule3))]
("cat" "eats" "squirrel" "-")
((((triple3) -> (rule1 % int2)) triple4) -> (rule3 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The cat is blue.
True
5
proof
[(((((((triple3) -> rule1) triple4) -> rule3)) -> rule1))]
("cat" "is" "blue" "+")
((((((triple3) -> (rule1 % int3)) triple4) -> (rule3 % int2))) -> (rule1 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The cat does not chase the mouse.
False
5
inv-proof
[(((((((triple3) -> rule1) triple4) -> rule3)) -> rule2))]
("cat" "chases" "mouse" "-")
((((((triple3) -> (rule1 % int3)) triple4) -> (rule3 % int2))) -> (rule2 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The squirrel is not blue.
Unknown
inv-rconc
[@1: The squirrel is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "blue" "-")
The squirrel chases the mouse.
Unknown
rconc
[@1: The squirrel chases the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "chases" "mouse" "+")
The cat does not chase the squirrel.
Unknown
inv-random
[@0: The cat chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "squirrel" "-")
The squirrel is young.
Unknown
random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "+")
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
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 chases the squirrel.
Unknown
random
[@0: The mouse chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "squirrel" "+")
@0: The cat eats the mouse.[(triple1)] The mouse eats the cat.[(triple2)] The mouse eats the squirrel.[(triple3)] The mouse visits the cat.[(triple4)] The mouse visits the squirrel.[(triple5)] The squirrel eats the cat.[(triple6)] The squirrel visits the cat.[(triple7)] @1: The mouse chases the mouse.[(((triple3) -> rule2))] The mouse is blue.[(((triple3) -> rule1))] @2: The cat eats the squirrel.[(((((triple3) -> rule1) triple4) -> rule3))] @3: The cat chases the mouse.[(((((((triple3) -> rule1) triple4) -> rule3)) -> rule2))] The cat is blue.[(((((((triple3) -> rule1) triple4) -> rule3)) -> rule1))]
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple1
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple2
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple3
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple4
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple5
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple6
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
triple7
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((triple3) -> (rule2 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
((triple3) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
((((triple3) -> (rule1 % int2)) triple4) -> (rule3 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The cat chases the mouse.
("cat" "chases" "mouse" "+")
((((((triple3) -> (rule1 % int3)) triple4) -> (rule3 % int2))) -> (rule2 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The cat is blue.
("cat" "is" "blue" "+")
((((((triple3) -> (rule1 % int3)) triple4) -> (rule3 % int2))) -> (rule1 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3