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