The dog chases the lion. The lion is kind. The squirrel sees the lion. The tiger likes the squirrel. If the lion sees the tiger then the tiger does not see the lion. If someone is cold then they do not like the squirrel. If someone sees the squirrel and they do not chase the squirrel then they do not see the dog. If someone sees the lion then the lion sees the tiger. If someone is kind and green then they see the lion. If someone likes the squirrel then the squirrel does not see the tiger. If someone likes the lion then the lion likes the squirrel. If the tiger does not see the lion then the lion likes the squirrel.
The dog chases the lion.
("dog" "chases" "lion" "+")
The lion is kind.
("lion" "is" "kind" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
If the lion sees the tiger then the tiger does not see the lion.
((("lion" "sees" "tiger" "+")) -> ("tiger" "sees" "lion" "-"))
If someone is cold then they do not like the squirrel.
((("someone" "is" "cold" "+")) -> ("someone" "likes" "squirrel" "-"))
If someone sees the squirrel and they do not chase the squirrel then they do not see the dog.
((("someone" "sees" "squirrel" "+") ("someone" "chases" "squirrel" "~")) -> ("someone" "sees" "dog" "-"))
If someone sees the lion then the lion sees the tiger.
((("someone" "sees" "lion" "+")) -> ("lion" "sees" "tiger" "+"))
If someone is kind and green then they see the lion.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "sees" "lion" "+"))
If someone likes the squirrel then the squirrel does not see the tiger.
((("someone" "likes" "squirrel" "+")) -> ("squirrel" "sees" "tiger" "-"))
If someone likes the lion then the lion likes the squirrel.
((("someone" "likes" "lion" "+")) -> ("lion" "likes" "squirrel" "+"))
If the tiger does not see the lion then the lion likes the squirrel.
((("tiger" "sees" "lion" "~")) -> ("lion" "likes" "squirrel" "+"))
The dog chases the lion.
True
1
proof
[(triple1)]
("dog" "chases" "lion" "+")
triple1
The dog does not chase the lion.
False
1
inv-proof
[(triple1)]
("dog" "chases" "lion" "-")
triple1
The squirrel does not see the tiger.
True
2
proof
[(((triple4) -> rule6) OR ((((((((triple3) -> rule4)) -> rule1)) -> rule8)) -> rule6))]
("squirrel" "sees" "tiger" "-")
((triple4) -> (rule6 % int1))
The squirrel does not see the tiger.
("squirrel" "sees" "tiger" "-")
int1
((((((((triple3) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The squirrel does not see the tiger.
("squirrel" "sees" "tiger" "-")
int1
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int2
The tiger does not see the lion.
("tiger" "sees" "lion" "-")
int3
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int4
The lion does not see the tiger.
False
2
inv-proof
[(((triple3) -> rule4))]
("lion" "sees" "tiger" "-")
((triple3) -> (rule4 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The tiger does not see the lion.
True
3
proof
[(((((triple3) -> rule4)) -> rule1))]
("tiger" "sees" "lion" "-")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
The tiger does not see the lion.
("tiger" "sees" "lion" "-")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The tiger sees the lion.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule1))]
("tiger" "sees" "lion" "+")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
The tiger does not see the lion.
("tiger" "sees" "lion" "-")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The lion likes the squirrel.
True
4
proof
[(((((((triple3) -> rule4)) -> rule1)) -> rule8))]
("lion" "likes" "squirrel" "+")
((((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int1
The tiger does not see the lion.
("tiger" "sees" "lion" "-")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int3
The lion does not like the squirrel.
False
4
inv-proof
[(((((((triple3) -> rule4)) -> rule1)) -> rule8))]
("lion" "likes" "squirrel" "-")
((((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int1
The tiger does not see the lion.
("tiger" "sees" "lion" "-")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int3
The dog does not see the lion.
Unknown
inv-rconc
[@1: The dog sees the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "sees" "lion" "-")
The lion sees the lion.
Unknown
rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "sees" "lion" "+")
The lion does not see the squirrel.
Unknown
inv-random
[@0: The lion sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "squirrel" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "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" "+")
The squirrel does not see the dog.
Unknown
inv-random
[@0: The squirrel sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "dog" "-")
The squirrel is blue.
Unknown
random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "+")
@0: The dog chases the lion.[(triple1)] The lion is kind.[(triple2)] The squirrel sees the lion.[(triple3)] The tiger likes the squirrel.[(triple4)] @1: The lion sees the tiger.[(((triple3) -> rule4))] The squirrel does not see the tiger.[(((triple4) -> rule6) OR ((((((((triple3) -> rule4)) -> rule1)) -> rule8)) -> rule6))] @2: The tiger does not see the lion.[(((((triple3) -> rule4)) -> rule1))] @3: The lion likes the squirrel.[(((((((triple3) -> rule4)) -> rule1)) -> rule8))]
The dog chases the lion.
("dog" "chases" "lion" "+")
triple1
The lion is kind.
("lion" "is" "kind" "+")
triple2
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple3
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
triple4
The lion sees the tiger.
("lion" "sees" "tiger" "+")
((triple3) -> (rule4 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The squirrel does not see the tiger.
("squirrel" "sees" "tiger" "-")
((triple4) -> (rule6 % int1))
The squirrel does not see the tiger.
("squirrel" "sees" "tiger" "-")
int1
((((((((triple3) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The squirrel does not see the tiger.
("squirrel" "sees" "tiger" "-")
int1
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int2
The tiger does not see the lion.
("tiger" "sees" "lion" "-")
int3
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int4
The tiger does not see the lion.
("tiger" "sees" "lion" "-")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
The tiger does not see the lion.
("tiger" "sees" "lion" "-")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
((((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
int1
The tiger does not see the lion.
("tiger" "sees" "lion" "-")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int3