The squirrel chases the tiger. The squirrel is big. The squirrel likes the tiger. The squirrel sees the tiger. The tiger is kind. The tiger is not nice. The tiger sees the squirrel. If the tiger is nice then the tiger likes the squirrel. If someone chases the tiger and the tiger sees the squirrel then the tiger likes the squirrel. If someone chases the tiger then they see the tiger. If someone likes the squirrel then they chase the tiger. If someone is kind and they like the squirrel then they are round. If the squirrel likes the tiger and the squirrel sees the tiger then the tiger chases the squirrel. If someone is kind and they like the tiger then the tiger does not chase the squirrel. If someone is nice then they are cold.
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is not nice.
("tiger" "is" "nice" "-")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
If the tiger is nice then the tiger likes the squirrel.
((("tiger" "is" "nice" "+")) -> ("tiger" "likes" "squirrel" "+"))
If someone chases the tiger and the tiger sees the squirrel then the tiger likes the squirrel.
((("someone" "chases" "tiger" "+") ("tiger" "sees" "squirrel" "+")) -> ("tiger" "likes" "squirrel" "+"))
If someone chases the tiger then they see the tiger.
((("someone" "chases" "tiger" "+")) -> ("someone" "sees" "tiger" "+"))
If someone likes the squirrel then they chase the tiger.
((("someone" "likes" "squirrel" "+")) -> ("someone" "chases" "tiger" "+"))
If someone is kind and they like the squirrel then they are round.
((("someone" "is" "kind" "+") ("someone" "likes" "squirrel" "+")) -> ("someone" "is" "round" "+"))
If the squirrel likes the tiger and the squirrel sees the tiger then the tiger chases the squirrel.
((("squirrel" "likes" "tiger" "+") ("squirrel" "sees" "tiger" "+")) -> ("tiger" "chases" "squirrel" "+"))
If someone is kind and they like the tiger then the tiger does not chase the squirrel.
((("someone" "is" "kind" "+") ("someone" "likes" "tiger" "+")) -> ("tiger" "chases" "squirrel" "-"))
If someone is nice then they are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
The squirrel chases the tiger.
True
1
proof
[(triple1)]
("squirrel" "chases" "tiger" "+")
triple1
The squirrel does not like the tiger.
False
1
inv-proof
[(triple3)]
("squirrel" "likes" "tiger" "-")
triple3
The tiger chases the squirrel.
True
3
proof
[(((triple3 triple4) -> rule6) OR ((triple3 ((triple1) -> rule3)) -> rule6))]
("tiger" "chases" "squirrel" "+")
((triple3 triple4) -> (rule6 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
((triple3 ((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int2
The tiger does not chase the squirrel.
False
3
inv-proof
[(((triple3 triple4) -> rule6) OR ((triple3 ((triple1) -> rule3)) -> rule6))]
("tiger" "chases" "squirrel" "-")
((triple3 triple4) -> (rule6 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
((triple3 ((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int2
The tiger chases the tiger.
True
4
proof
[(((((triple1 triple7) -> rule2)) -> rule4))]
("tiger" "chases" "tiger" "+")
((((triple1 triple7) -> (rule2 % int2))) -> (rule4 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
int2
The tiger is not round.
False
5
inv-proof
[(((triple5 ((triple1 triple7) -> rule2)) -> rule5))]
("tiger" "is" "round" "-")
((triple5 ((triple1 triple7) -> (rule2 % int2))) -> (rule5 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
int2
The tiger sees the tiger.
True
5
proof
[(((((((triple1 triple7) -> rule2)) -> rule4)) -> rule3))]
("tiger" "sees" "tiger" "+")
((((((triple1 triple7) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
int3
The tiger does not see the tiger.
False
5
inv-proof
[(((((((triple1 triple7) -> rule2)) -> rule4)) -> rule3))]
("tiger" "sees" "tiger" "-")
((((((triple1 triple7) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
int3
The squirrel is not cold.
Unknown
inv-rconc
[@1: The squirrel is cold.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "is" "cold" "-")
The tiger is cold.
Unknown
rconc
[@1: The tiger is cold.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "is" "cold" "+")
The squirrel is not round.
Unknown
inv-rconc
[@1: The squirrel is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "is" "round" "-")
The tiger is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
The squirrel does not see the squirrel.
Unknown
inv-random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "-")
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 squirrel is big.[(triple2)] The squirrel likes the tiger.[(triple3)] The squirrel sees the tiger.[(triple4 OR ((triple1) -> rule3))] The tiger is kind.[(triple5)] The tiger is not nice.[(triple6)] The tiger sees the squirrel.[(triple7)] @1: The tiger chases the squirrel.[(((triple3 triple4) -> rule6) OR ((triple3 ((triple1) -> rule3)) -> rule6))] The tiger likes the squirrel.[(((triple1 triple7) -> rule2))] @2: The tiger chases the tiger.[(((((triple1 triple7) -> rule2)) -> rule4))] The tiger is round.[(((triple5 ((triple1 triple7) -> rule2)) -> rule5))] @3: The tiger sees the tiger.[(((((((triple1 triple7) -> rule2)) -> rule4)) -> rule3))]
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple1
The squirrel is big.
("squirrel" "is" "big" "+")
triple2
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
triple3
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple4
((triple1) -> (rule3 % int1))
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
triple5
The tiger is not nice.
("tiger" "is" "nice" "-")
triple6
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple7
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
((triple3 triple4) -> (rule6 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
((triple3 ((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int2
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
((triple1 triple7) -> (rule2 % int1))
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((((triple1 triple7) -> (rule2 % int2))) -> (rule4 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
((triple5 ((triple1 triple7) -> (rule2 % int2))) -> (rule5 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
int2
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((((((triple1 triple7) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
int3