The cat is nice. The lion visits the tiger. The squirrel likes the lion. The tiger sees the cat. If someone sees the squirrel then the squirrel sees the cat. If the squirrel sees the tiger and the tiger is not blue then the squirrel is not blue. If the cat is blue and the cat does not see the tiger then the cat likes the squirrel. If someone likes the lion then the lion is rough. If someone is rough and they like the tiger then they like the cat. If someone sees the lion and they see the cat then they like the lion. If the lion likes the squirrel then the lion sees the squirrel. If someone sees the cat then they see the squirrel.
The cat is nice.
("cat" "is" "nice" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
If someone sees the squirrel then the squirrel sees the cat.
((("someone" "sees" "squirrel" "+")) -> ("squirrel" "sees" "cat" "+"))
If the squirrel sees the tiger and the tiger is not blue then the squirrel is not blue.
((("squirrel" "sees" "tiger" "+") ("tiger" "is" "blue" "~")) -> ("squirrel" "is" "blue" "-"))
If the cat is blue and the cat does not see the tiger then the cat likes the squirrel.
((("cat" "is" "blue" "+") ("cat" "sees" "tiger" "~")) -> ("cat" "likes" "squirrel" "+"))
If someone likes the lion then the lion is rough.
((("someone" "likes" "lion" "+")) -> ("lion" "is" "rough" "+"))
If someone is rough and they like the tiger then they like the cat.
((("someone" "is" "rough" "+") ("someone" "likes" "tiger" "+")) -> ("someone" "likes" "cat" "+"))
If someone sees the lion and they see the cat then they like the lion.
((("someone" "sees" "lion" "+") ("someone" "sees" "cat" "+")) -> ("someone" "likes" "lion" "+"))
If the lion likes the squirrel then the lion sees the squirrel.
((("lion" "likes" "squirrel" "+")) -> ("lion" "sees" "squirrel" "+"))
If someone sees the cat then they see the squirrel.
((("someone" "sees" "cat" "+")) -> ("someone" "sees" "squirrel" "+"))
The squirrel likes the lion.
True
1
proof
[(triple3)]
("squirrel" "likes" "lion" "+")
triple3
The cat is not nice.
False
1
inv-proof
[(triple1)]
("cat" "is" "nice" "-")
triple1
The lion is rough.
True
2
proof
[(((triple3) -> rule4))]
("lion" "is" "rough" "+")
((triple3) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The tiger does not see the squirrel.
False
2
inv-proof
[(((triple4) -> rule8))]
("tiger" "sees" "squirrel" "-")
((triple4) -> (rule8 % int1))
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int1
The squirrel sees the cat.
True
3
proof
[(((((triple4) -> rule8)) -> rule1))]
("squirrel" "sees" "cat" "+")
((((triple4) -> (rule8 % int2))) -> (rule1 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int2
The squirrel does not see the cat.
False
3
inv-proof
[(((((triple4) -> rule8)) -> rule1))]
("squirrel" "sees" "cat" "-")
((((triple4) -> (rule8 % int2))) -> (rule1 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int2
The squirrel sees the squirrel.
True
4
proof
[(((((((triple4) -> rule8)) -> rule1)) -> rule8))]
("squirrel" "sees" "squirrel" "+")
((((((triple4) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int2
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int3
The squirrel does not see the squirrel.
False
4
inv-proof
[(((((((triple4) -> rule8)) -> rule1)) -> rule8))]
("squirrel" "sees" "squirrel" "-")
((((((triple4) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int2
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int3
The cat does not like the cat.
Unknown
inv-rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "likes" "cat" "-")
The tiger likes the cat.
Unknown
rconc
[@1: The tiger likes the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "likes" "cat" "+")
The lion does not see the squirrel.
Unknown
inv-rconc
[@1: The lion sees the squirrel.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "sees" "squirrel" "-")
The tiger likes the lion.
Unknown
rconc
[@1: The tiger likes the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "likes" "lion" "+")
The lion does not see the tiger.
Unknown
inv-random
[@0: The lion sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "tiger" "-")
The lion visits the cat.
Unknown
random
[@0: The lion visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "cat" "+")
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
@0: The cat is nice.[(triple1)] The lion visits the tiger.[(triple2)] The squirrel likes the lion.[(triple3)] The tiger sees the cat.[(triple4)] @1: The lion is rough.[(((triple3) -> rule4))] The tiger sees the squirrel.[(((triple4) -> rule8))] @2: The squirrel sees the cat.[(((((triple4) -> rule8)) -> rule1))] @3: The squirrel sees the squirrel.[(((((((triple4) -> rule8)) -> rule1)) -> rule8))]
The cat is nice.
("cat" "is" "nice" "+")
triple1
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple2
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
triple3
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple4
The lion is rough.
("lion" "is" "rough" "+")
((triple3) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
((triple4) -> (rule8 % int1))
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
((((triple4) -> (rule8 % int2))) -> (rule1 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int2
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((((((triple4) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int2
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int3