The dog is kind. The mouse sees the tiger. The squirrel sees the tiger. The tiger is round. If someone chases the mouse and they eat the squirrel then the mouse sees the dog. If someone is blue and they see the tiger then the tiger sees the squirrel. If someone sees the tiger then they are blue. If someone sees the mouse then the mouse chases the tiger. If someone is kind and they eat the dog then they eat the mouse. If someone sees the squirrel then the squirrel chases the dog. If someone sees the squirrel and they eat the squirrel then the squirrel sees the tiger. If the squirrel eats the tiger then the squirrel chases the dog.
The dog is kind.
("dog" "is" "kind" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The tiger is round.
("tiger" "is" "round" "+")
If someone chases the mouse and they eat the squirrel then the mouse sees the dog.
((("someone" "chases" "mouse" "+") ("someone" "eats" "squirrel" "+")) -> ("mouse" "sees" "dog" "+"))
If someone is blue and they see the tiger then the tiger sees the squirrel.
((("someone" "is" "blue" "+") ("someone" "sees" "tiger" "+")) -> ("tiger" "sees" "squirrel" "+"))
If someone sees the tiger then they are blue.
((("someone" "sees" "tiger" "+")) -> ("someone" "is" "blue" "+"))
If someone sees the mouse then the mouse chases the tiger.
((("someone" "sees" "mouse" "+")) -> ("mouse" "chases" "tiger" "+"))
If someone is kind and they eat the dog then they eat the mouse.
((("someone" "is" "kind" "+") ("someone" "eats" "dog" "+")) -> ("someone" "eats" "mouse" "+"))
If someone sees the squirrel then the squirrel chases the dog.
((("someone" "sees" "squirrel" "+")) -> ("squirrel" "chases" "dog" "+"))
If someone sees the squirrel and they eat the squirrel then the squirrel sees the tiger.
((("someone" "sees" "squirrel" "+") ("someone" "eats" "squirrel" "+")) -> ("squirrel" "sees" "tiger" "+"))
If the squirrel eats the tiger then the squirrel chases the dog.
((("squirrel" "eats" "tiger" "+")) -> ("squirrel" "chases" "dog" "+"))
The squirrel sees the tiger.
True
1
proof
[(triple3)]
("squirrel" "sees" "tiger" "+")
triple3
The dog is not kind.
False
1
inv-proof
[(triple1)]
("dog" "is" "kind" "-")
triple1
The mouse is blue.
True
2
proof
[(((triple2) -> rule3))]
("mouse" "is" "blue" "+")
((triple2) -> (rule3 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is not blue.
False
2
inv-proof
[(((triple2) -> rule3))]
("mouse" "is" "blue" "-")
((triple2) -> (rule3 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The tiger sees the squirrel.
True
4
proof
[(((((triple2) -> rule3) triple2) -> rule2) OR ((((triple3) -> rule3) triple3) -> rule2))]
("tiger" "sees" "squirrel" "+")
((((triple2) -> (rule3 % int2)) triple2) -> (rule2 % int1))
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
((((triple3) -> (rule3 % int2)) triple3) -> (rule2 % int1))
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The tiger does not see the squirrel.
False
4
inv-proof
[(((((triple2) -> rule3) triple2) -> rule2) OR ((((triple3) -> rule3) triple3) -> rule2))]
("tiger" "sees" "squirrel" "-")
((((triple2) -> (rule3 % int2)) triple2) -> (rule2 % int1))
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
((((triple3) -> (rule3 % int2)) triple3) -> (rule2 % int1))
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel chases the dog.
True
5
proof
[(((((((triple2) -> rule3) triple2) -> rule2)) -> rule6) OR ((((((triple3) -> rule3) triple3) -> rule2)) -> rule6))]
("squirrel" "chases" "dog" "+")
((((((triple2) -> (rule3 % int3)) triple2) -> (rule2 % int2))) -> (rule6 % int1))
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int1
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
((((((triple3) -> (rule3 % int3)) triple3) -> (rule2 % int2))) -> (rule6 % int1))
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int1
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int2
The squirrel is blue.
("squirrel" "is" "blue" "+")
int3
The squirrel does not chase the dog.
False
5
inv-proof
[(((((((triple2) -> rule3) triple2) -> rule2)) -> rule6) OR ((((((triple3) -> rule3) triple3) -> rule2)) -> rule6))]
("squirrel" "chases" "dog" "-")
((((((triple2) -> (rule3 % int3)) triple2) -> (rule2 % int2))) -> (rule6 % int1))
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int1
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
((((((triple3) -> (rule3 % int3)) triple3) -> (rule2 % int2))) -> (rule6 % int1))
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int1
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int2
The squirrel is blue.
("squirrel" "is" "blue" "+")
int3
The mouse does not chase the tiger.
Unknown
inv-rconc
[@1: The mouse chases the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "chases" "tiger" "-")
The tiger eats the mouse.
Unknown
rconc
[@1: The tiger eats the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "eats" "mouse" "+")
The mouse does not eat the mouse.
Unknown
inv-rconc
[@1: The mouse eats the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "eats" "mouse" "-")
The squirrel eats the mouse.
Unknown
rconc
[@1: The squirrel eats the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "eats" "mouse" "+")
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The squirrel chases the mouse.
Unknown
random
[@0: The squirrel chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "mouse" "+")
The squirrel does not chase the tiger.
Unknown
inv-random
[@0: The squirrel chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "tiger" "-")
The mouse chases the dog.
Unknown
random
[@0: The mouse chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "dog" "+")
@0: The dog is kind.[(triple1)] The mouse sees the tiger.[(triple2)] The squirrel sees the tiger.[(triple3)] The tiger is round.[(triple4)] @1: The mouse is blue.[(((triple2) -> rule3))] The squirrel is blue.[(((triple3) -> rule3))] @2: The tiger sees the squirrel.[(((((triple2) -> rule3) triple2) -> rule2) OR ((((triple3) -> rule3) triple3) -> rule2))] @3: The squirrel chases the dog.[(((((((triple2) -> rule3) triple2) -> rule2)) -> rule6) OR ((((((triple3) -> rule3) triple3) -> rule2)) -> rule6))]
The dog is kind.
("dog" "is" "kind" "+")
triple1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple2
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple3
The tiger is round.
("tiger" "is" "round" "+")
triple4
The mouse is blue.
("mouse" "is" "blue" "+")
((triple2) -> (rule3 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
((triple3) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
((((triple2) -> (rule3 % int2)) triple2) -> (rule2 % int1))
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
((((triple3) -> (rule3 % int2)) triple3) -> (rule2 % int1))
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
((((((triple2) -> (rule3 % int3)) triple2) -> (rule2 % int2))) -> (rule6 % int1))
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int1
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
((((((triple3) -> (rule3 % int3)) triple3) -> (rule2 % int2))) -> (rule6 % int1))
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
int1
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int2
The squirrel is blue.
("squirrel" "is" "blue" "+")
int3