The cat does not visit the lion. The dog is rough. The lion is not rough. If something eats the lion and the lion eats the cat then it needs the lion. If the cat does not visit the lion then the cat is kind. If something is kind then it needs the cat. If something eats the cat then the cat does not eat the lion. If the cat eats the lion and the cat is rough then the lion eats the cat. If something eats the lion and the lion is not nice then the lion visits the dog.
The cat does not visit the lion.
("cat" "visits" "lion" "-")
The dog is rough.
("dog" "is" "rough" "+")
The lion is not rough.
("lion" "is" "rough" "-")
If something eats the lion and the lion eats the cat then it needs the lion.
((("something" "eats" "lion" "+") ("lion" "eats" "cat" "+")) -> ("something" "needs" "lion" "+"))
If the cat does not visit the lion then the cat is kind.
((("cat" "visits" "lion" "~")) -> ("cat" "is" "kind" "+"))
If something is kind then it needs the cat.
((("something" "is" "kind" "+")) -> ("something" "needs" "cat" "+"))
If something eats the cat then the cat does not eat the lion.
((("something" "eats" "cat" "+")) -> ("cat" "eats" "lion" "-"))
If the cat eats the lion and the cat is rough then the lion eats the cat.
((("cat" "eats" "lion" "+") ("cat" "is" "rough" "+")) -> ("lion" "eats" "cat" "+"))
If something eats the lion and the lion is not nice then the lion visits the dog.
((("something" "eats" "lion" "+") ("lion" "is" "nice" "~")) -> ("lion" "visits" "dog" "+"))
The lion is not rough.
True
1
proof
[(triple3)]
("lion" "is" "rough" "-")
triple3
The cat visits the lion.
False
1
inv-proof
[(triple1)]
("cat" "visits" "lion" "+")
triple1
The cat is kind.
True
2
proof
[(((triple1) -> rule2))]
("cat" "is" "kind" "+")
((triple1) -> (rule2 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is not kind.
False
2
inv-proof
[(((triple1) -> rule2))]
("cat" "is" "kind" "-")
((triple1) -> (rule2 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat needs the cat.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("cat" "needs" "cat" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat does not need the cat.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("cat" "needs" "cat" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The lion does not eat the cat.
Unknown
inv-rconc
[@1: The lion eats the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "eats" "cat" "-")
The lion needs the lion.
Unknown
rconc
[@1: The lion needs the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "needs" "lion" "+")
The lion does not visit the dog.
Unknown
inv-rconc
[@1: The lion visits the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "visits" "dog" "-")
The cat eats the dog.
Unknown
random
[@0: The cat eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "dog" "+")
The lion does not need the dog.
Unknown
inv-random
[@0: The lion needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "dog" "-")
The dog eats the cat.
Unknown
random
[@0: The dog eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "cat" "+")
@0: The cat does not visit the lion.[(triple1)] The dog is rough.[(triple2)] The lion is not rough.[(triple3)] @1: The cat is kind.[(((triple1) -> rule2))] @2: The cat needs the cat.[(((((triple1) -> rule2)) -> rule3))]
The cat does not visit the lion.
("cat" "visits" "lion" "-")
triple1
The dog is rough.
("dog" "is" "rough" "+")
triple2
The lion is not rough.
("lion" "is" "rough" "-")
triple3
The cat is kind.
("cat" "is" "kind" "+")
((triple1) -> (rule2 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2