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