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