The squirrel chases the tiger. The tiger chases the squirrel. The tiger sees the squirrel. If the squirrel is red then the squirrel is cold. If someone sees the squirrel and the squirrel is nice then they chase the tiger. If someone chases the tiger then they are nice.
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
If the squirrel is red then the squirrel is cold.
((("squirrel" "is" "red" "+")) -> ("squirrel" "is" "cold" "+"))
If someone sees the squirrel and the squirrel is nice then they chase the tiger.
((("someone" "sees" "squirrel" "+") ("squirrel" "is" "nice" "+")) -> ("someone" "chases" "tiger" "+"))
If someone chases the tiger then they are nice.
((("someone" "chases" "tiger" "+")) -> ("someone" "is" "nice" "+"))
The tiger chases the squirrel.
True
1
proof
[(triple2)]
("tiger" "chases" "squirrel" "+")
triple2
The tiger does not see the squirrel.
False
1
inv-proof
[(triple3)]
("tiger" "sees" "squirrel" "-")
triple3
The squirrel is nice.
True
2
proof
[(((triple1) -> rule3))]
("squirrel" "is" "nice" "+")
((triple1) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is not nice.
False
2
inv-proof
[(((triple1) -> rule3))]
("squirrel" "is" "nice" "-")
((triple1) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The tiger chases the tiger.
True
4
proof
[(((triple3 ((triple1) -> rule3)) -> rule2))]
("tiger" "chases" "tiger" "+")
((triple3 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The tiger does not chase the tiger.
False
4
inv-proof
[(((triple3 ((triple1) -> rule3)) -> rule2))]
("tiger" "chases" "tiger" "-")
((triple3 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The tiger is nice.
True
5
proof
[(((((triple3 ((triple1) -> rule3)) -> rule2)) -> rule3))]
("tiger" "is" "nice" "+")
((((triple3 ((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
The tiger is not nice.
False
5
inv-proof
[(((((triple3 ((triple1) -> rule3)) -> rule2)) -> rule3))]
("tiger" "is" "nice" "-")
((((triple3 ((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
The squirrel is not cold.
Unknown
inv-rconc
[@1: The squirrel is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "cold" "-")
The tiger is red.
Unknown
random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "+")
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 sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
The tiger does not need the squirrel.
Unknown
inv-random
[@0: The tiger needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "squirrel" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
The tiger is not cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
@0: The squirrel chases the tiger.[(triple1)] The tiger chases the squirrel.[(triple2)] The tiger sees the squirrel.[(triple3)] @1: The squirrel is nice.[(((triple1) -> rule3))] @2: The tiger chases the tiger.[(((triple3 ((triple1) -> rule3)) -> rule2))] @3: The tiger is nice.[(((((triple3 ((triple1) -> rule3)) -> rule2)) -> rule3))]
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple1
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple2
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple3
The squirrel is nice.
("squirrel" "is" "nice" "+")
((triple1) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((triple3 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
((((triple3 ((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3