The cat does not visit the squirrel. The lion visits the squirrel. The squirrel chases the lion. If something visits the squirrel then the squirrel does not like the lion. If something is rough then it chases the cat. If something visits the cat then the cat is rough. If something likes the cat then the cat does not visit the lion. If something visits the squirrel and it is green then it visits the cat. If something chases the lion then the lion visits the cat. If something likes the cat and it is not red then the cat does not chase the squirrel. If the lion does not chase the squirrel then the squirrel does not chase the lion.
The cat does not visit the squirrel.
("cat" "visits" "squirrel" "-")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
If something visits the squirrel then the squirrel does not like the lion.
((("something" "visits" "squirrel" "+")) -> ("squirrel" "likes" "lion" "-"))
If something is rough then it chases the cat.
((("something" "is" "rough" "+")) -> ("something" "chases" "cat" "+"))
If something visits the cat then the cat is rough.
((("something" "visits" "cat" "+")) -> ("cat" "is" "rough" "+"))
If something likes the cat then the cat does not visit the lion.
((("something" "likes" "cat" "+")) -> ("cat" "visits" "lion" "-"))
If something visits the squirrel and it is green then it visits the cat.
((("something" "visits" "squirrel" "+") ("something" "is" "green" "+")) -> ("something" "visits" "cat" "+"))
If something chases the lion then the lion visits the cat.
((("something" "chases" "lion" "+")) -> ("lion" "visits" "cat" "+"))
If something likes the cat and it is not red then the cat does not chase the squirrel.
((("something" "likes" "cat" "+") ("something" "is" "red" "~")) -> ("cat" "chases" "squirrel" "-"))
If the lion does not chase the squirrel then the squirrel does not chase the lion.
((("lion" "chases" "squirrel" "~")) -> ("squirrel" "chases" "lion" "-"))
The lion visits the squirrel.
True
1
proof
[(triple2)]
("lion" "visits" "squirrel" "+")
triple2
The squirrel does not chase the lion.
False
1
inv-proof
[(triple3)]
("squirrel" "chases" "lion" "-")
triple3
The lion visits the cat.
True
2
proof
[(((triple3) -> rule6))]
("lion" "visits" "cat" "+")
((triple3) -> (rule6 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The lion does not visit the cat.
False
2
inv-proof
[(((triple3) -> rule6))]
("lion" "visits" "cat" "-")
((triple3) -> (rule6 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The cat is rough.
True
3
proof
[(((((triple3) -> rule6)) -> rule3))]
("cat" "is" "rough" "+")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The cat is not rough.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule3))]
("cat" "is" "rough" "-")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The cat chases the cat.
True
4
proof
[(((((((triple3) -> rule6)) -> rule3)) -> rule2))]
("cat" "chases" "cat" "+")
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
The cat does not chase the cat.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule3)) -> rule2))]
("cat" "chases" "cat" "-")
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
The squirrel does not chase the cat.
Unknown
inv-rconc
[@1: The squirrel chases the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "chases" "cat" "-")
The lion chases the cat.
Unknown
rconc
[@1: The lion chases the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "chases" "cat" "+")
The squirrel does not visit the cat.
Unknown
inv-rconc
[@1: The squirrel visits the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "visits" "cat" "-")
The cat visits the cat.
Unknown
rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "visits" "cat" "+")
The cat does not like the lion.
Unknown
inv-random
[@0: The cat likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "lion" "-")
The lion likes the squirrel.
Unknown
random
[@0: The lion likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "squirrel" "+")
The cat is not green.
Unknown
inv-random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "-")
The squirrel is blue.
Unknown
random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "+")
@0: The cat does not visit the squirrel.[(triple1)] The lion visits the squirrel.[(triple2)] The squirrel chases the lion.[(triple3)] @1: The lion visits the cat.[(((triple3) -> rule6))] The squirrel does not like the lion.[(((triple2) -> rule1))] @2: The cat is rough.[(((((triple3) -> rule6)) -> rule3))] @3: The cat chases the cat.[(((((((triple3) -> rule6)) -> rule3)) -> rule2))]
The cat does not visit the squirrel.
("cat" "visits" "squirrel" "-")
triple1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple2
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
triple3
The lion visits the cat.
("lion" "visits" "cat" "+")
((triple3) -> (rule6 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The squirrel does not like the lion.
("squirrel" "likes" "lion" "-")
((triple2) -> (rule1 % int1))
The squirrel does not like the lion.
("squirrel" "likes" "lion" "-")
int1
The cat is rough.
("cat" "is" "rough" "+")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3