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