The cat is cold. The cat is not kind. The cat is nice. The cat is not red. The cat is young. The cat needs the lion. The cat sees the lion. The cat does not visit the lion. The lion is cold. The lion is kind. The lion is not nice. The lion is red. The lion is young. The lion needs the cat. The lion sees the cat. The lion visits the cat. If someone sees the cat then the cat is not kind. If someone is nice and not young then they visit the cat. If someone visits the lion then the lion visits the cat. If someone visits the cat then they visit the lion. If someone is red and they do not visit the cat then the cat sees the lion. If someone sees the lion and they do not see the cat then the cat needs the lion. If someone needs the lion and they visit the lion then they do not need the cat. If someone sees the lion and the lion needs the cat then the lion is cold.
The cat is cold.
("cat" "is" "cold" "+")
The cat is not kind.
("cat" "is" "kind" "-")
The cat is nice.
("cat" "is" "nice" "+")
The cat is not red.
("cat" "is" "red" "-")
The cat is young.
("cat" "is" "young" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The cat does not visit the lion.
("cat" "visits" "lion" "-")
The lion is cold.
("lion" "is" "cold" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is not nice.
("lion" "is" "nice" "-")
The lion is red.
("lion" "is" "red" "+")
The lion is young.
("lion" "is" "young" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
If someone sees the cat then the cat is not kind.
((("someone" "sees" "cat" "+")) -> ("cat" "is" "kind" "-"))
If someone is nice and not young then they visit the cat.
((("someone" "is" "nice" "+") ("someone" "is" "young" "~")) -> ("someone" "visits" "cat" "+"))
If someone visits the lion then the lion visits the cat.
((("someone" "visits" "lion" "+")) -> ("lion" "visits" "cat" "+"))
If someone visits the cat then they visit the lion.
((("someone" "visits" "cat" "+")) -> ("someone" "visits" "lion" "+"))
If someone is red and they do not visit the cat then the cat sees the lion.
((("someone" "is" "red" "+") ("someone" "visits" "cat" "~")) -> ("cat" "sees" "lion" "+"))
If someone sees the lion and they do not see the cat then the cat needs the lion.
((("someone" "sees" "lion" "+") ("someone" "sees" "cat" "~")) -> ("cat" "needs" "lion" "+"))
If someone needs the lion and they visit the lion then they do not need the cat.
((("someone" "needs" "lion" "+") ("someone" "visits" "lion" "+")) -> ("someone" "needs" "cat" "-"))
If someone sees the lion and the lion needs the cat then the lion is cold.
((("someone" "sees" "lion" "+") ("lion" "needs" "cat" "+")) -> ("lion" "is" "cold" "+"))
The cat is not red.
True
1
proof
[(triple4)]
("cat" "is" "red" "-")
triple4
The cat does not see the lion.
False
1
inv-proof
[(triple7)]
("cat" "sees" "lion" "-")
triple7
The lion visits the lion.
True
2
proof
[(((triple16) -> rule4))]
("lion" "visits" "lion" "+")
((triple16) -> (rule4 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion does not visit the lion.
False
2
inv-proof
[(((triple16) -> rule4))]
("lion" "visits" "lion" "-")
((triple16) -> (rule4 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The cat does not visit the cat.
Unknown
inv-rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "visits" "cat" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
@0: The cat does not visit the lion.[(triple8)] The cat is cold.[(triple1)] The cat is nice.[(triple3)] The cat is not kind.[(triple2 OR ((triple15) -> rule1))] The cat is not red.[(triple4)] The cat is young.[(triple5)] The cat needs the lion.[(triple6)] The cat sees the lion.[(triple7)] The lion is cold.[(triple9 OR ((triple7 triple14) -> rule8))] The lion is kind.[(triple10)] The lion is not nice.[(triple11)] The lion is red.[(triple12)] The lion is young.[(triple13)] The lion needs the cat.[(triple14)] The lion sees the cat.[(triple15)] The lion visits the cat.[(triple16)] @1: The lion visits the lion.[(((triple16) -> rule4))]
The cat does not visit the lion.
("cat" "visits" "lion" "-")
triple8
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple3
The cat is not kind.
("cat" "is" "kind" "-")
triple2
((triple15) -> (rule1 % int1))
The cat is not kind.
("cat" "is" "kind" "-")
int1
The cat is not red.
("cat" "is" "red" "-")
triple4
The cat is young.
("cat" "is" "young" "+")
triple5
The cat needs the lion.
("cat" "needs" "lion" "+")
triple6
The cat sees the lion.
("cat" "sees" "lion" "+")
triple7
The lion is cold.
("lion" "is" "cold" "+")
triple9
((triple7 triple14) -> (rule8 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
triple10
The lion is not nice.
("lion" "is" "nice" "-")
triple11
The lion is red.
("lion" "is" "red" "+")
triple12
The lion is young.
("lion" "is" "young" "+")
triple13
The lion needs the cat.
("lion" "needs" "cat" "+")
triple14
The lion sees the cat.
("lion" "sees" "cat" "+")
triple15
The lion visits the cat.
("lion" "visits" "cat" "+")
triple16
The lion visits the lion.
("lion" "visits" "lion" "+")
((triple16) -> (rule4 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1