The cat is not kind. The cat is nice. The cat sees the lion. The cat visits the lion. The lion chases the cat. The lion is kind. The lion is round. If someone visits the lion then they are not kind. If someone is nice then they visit the cat. If someone visits the lion and they are rough then the lion visits the cat. If someone visits the cat and they visit the lion then the lion is rough. If someone chases the lion and they are not red then the lion does not see the cat. If someone sees the cat and the cat visits the lion then they chase the cat. If someone is rough then they see the lion. If someone chases the cat and the cat does not see the lion then the lion is not kind.
The cat is not kind.
("cat" "is" "kind" "-")
The cat is nice.
("cat" "is" "nice" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The lion chases the cat.
("lion" "chases" "cat" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is round.
("lion" "is" "round" "+")
If someone visits the lion then they are not kind.
((("someone" "visits" "lion" "+")) -> ("someone" "is" "kind" "-"))
If someone is nice then they visit the cat.
((("someone" "is" "nice" "+")) -> ("someone" "visits" "cat" "+"))
If someone visits the lion and they are rough then the lion visits the cat.
((("someone" "visits" "lion" "+") ("someone" "is" "rough" "+")) -> ("lion" "visits" "cat" "+"))
If someone visits the cat and they visit the lion then the lion is rough.
((("someone" "visits" "cat" "+") ("someone" "visits" "lion" "+")) -> ("lion" "is" "rough" "+"))
If someone chases the lion and they are not red then the lion does not see the cat.
((("someone" "chases" "lion" "+") ("someone" "is" "red" "~")) -> ("lion" "sees" "cat" "-"))
If someone sees the cat and the cat visits the lion then they chase the cat.
((("someone" "sees" "cat" "+") ("cat" "visits" "lion" "+")) -> ("someone" "chases" "cat" "+"))
If someone is rough then they see the lion.
((("someone" "is" "rough" "+")) -> ("someone" "sees" "lion" "+"))
If someone chases the cat and the cat does not see the lion then the lion is not kind.
((("someone" "chases" "cat" "+") ("cat" "sees" "lion" "~")) -> ("lion" "is" "kind" "-"))
The cat is not kind.
True
1
proof
[(triple1 OR ((triple4) -> rule1))]
("cat" "is" "kind" "-")
triple1
((triple4) -> (rule1 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The lion is not kind.
False
1
inv-proof
[(triple6)]
("lion" "is" "kind" "-")
triple6
The cat visits the cat.
True
2
proof
[(((triple2) -> rule2))]
("cat" "visits" "cat" "+")
((triple2) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat does not visit the cat.
False
2
inv-proof
[(((triple2) -> rule2))]
("cat" "visits" "cat" "-")
((triple2) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The lion is rough.
True
4
proof
[(((((triple2) -> rule2) triple4) -> rule4))]
("lion" "is" "rough" "+")
((((triple2) -> (rule2 % int2)) triple4) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The lion is not rough.
False
4
inv-proof
[(((((triple2) -> rule2) triple4) -> rule4))]
("lion" "is" "rough" "-")
((((triple2) -> (rule2 % int2)) triple4) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The lion sees the lion.
True
5
proof
[(((((((triple2) -> rule2) triple4) -> rule4)) -> rule7))]
("lion" "sees" "lion" "+")
((((((triple2) -> (rule2 % int3)) triple4) -> (rule4 % int2))) -> (rule7 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The cat visits the cat.
("cat" "visits" "cat" "+")
int3
The lion does not see the lion.
False
5
inv-proof
[(((((((triple2) -> rule2) triple4) -> rule4)) -> rule7))]
("lion" "sees" "lion" "-")
((((((triple2) -> (rule2 % int3)) triple4) -> (rule4 % int2))) -> (rule7 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The cat visits the cat.
("cat" "visits" "cat" "+")
int3
The cat does not chase the cat.
Unknown
inv-rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "chases" "cat" "-")
The lion visits the cat.
Unknown
rconc
[@1: The lion visits the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "visits" "cat" "+")
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
The cat is not round.
Unknown
inv-random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "-")
The lion is nice.
Unknown
random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "+")
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The cat chases the lion.
Unknown
random
[@0: The cat chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "lion" "+")
@0: The cat is nice.[(triple2)] The cat is not kind.[(triple1 OR ((triple4) -> rule1))] The cat sees the lion.[(triple3)] The cat visits the lion.[(triple4)] The lion chases the cat.[(triple5)] The lion is kind.[(triple6)] The lion is round.[(triple7)] @1: The cat visits the cat.[(((triple2) -> rule2))] @2: The lion is rough.[(((((triple2) -> rule2) triple4) -> rule4))] @3: The lion sees the lion.[(((((((triple2) -> rule2) triple4) -> rule4)) -> rule7))]
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cat is not kind.
("cat" "is" "kind" "-")
triple1
((triple4) -> (rule1 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat sees the lion.
("cat" "sees" "lion" "+")
triple3
The cat visits the lion.
("cat" "visits" "lion" "+")
triple4
The lion chases the cat.
("lion" "chases" "cat" "+")
triple5
The lion is kind.
("lion" "is" "kind" "+")
triple6
The lion is round.
("lion" "is" "round" "+")
triple7
The cat visits the cat.
("cat" "visits" "cat" "+")
((triple2) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
((((triple2) -> (rule2 % int2)) triple4) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The lion sees the lion.
("lion" "sees" "lion" "+")
((((((triple2) -> (rule2 % int3)) triple4) -> (rule4 % int2))) -> (rule7 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The cat visits the cat.
("cat" "visits" "cat" "+")
int3