The bear eats the cat. The bear is kind. The cat eats the lion. The cat is blue. The cat is round. The lion needs the bear. The lion visits the bear. If something needs the lion and the lion visits the bear then it is kind. If something eats the cat and the cat is round then the cat needs the lion. If the lion needs the cat and the cat eats the bear then the cat visits the lion. If something needs the bear then the bear is red. All red things are round. If something is kind then it visits the lion.
The bear eats the cat.
("bear" "eats" "cat" "+")
The bear is kind.
("bear" "is" "kind" "+")
The cat eats the lion.
("cat" "eats" "lion" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is round.
("cat" "is" "round" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
The lion visits the bear.
("lion" "visits" "bear" "+")
If something needs the lion and the lion visits the bear then it is kind.
((("something" "needs" "lion" "+") ("lion" "visits" "bear" "+")) -> ("something" "is" "kind" "+"))
If something eats the cat and the cat is round then the cat needs the lion.
((("something" "eats" "cat" "+") ("cat" "is" "round" "+")) -> ("cat" "needs" "lion" "+"))
If the lion needs the cat and the cat eats the bear then the cat visits the lion.
((("lion" "needs" "cat" "+") ("cat" "eats" "bear" "+")) -> ("cat" "visits" "lion" "+"))
If something needs the bear then the bear is red.
((("something" "needs" "bear" "+")) -> ("bear" "is" "red" "+"))
All red things are round.
((("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
If something is kind then it visits the lion.
((("something" "is" "kind" "+")) -> ("something" "visits" "lion" "+"))
The cat is blue.
True
1
proof
[(triple4)]
("cat" "is" "blue" "+")
triple4
The bear does not eat the cat.
False
1
inv-proof
[(triple1)]
("bear" "eats" "cat" "-")
triple1
The cat needs the lion.
True
3
proof
[(((triple1 triple5) -> rule2))]
("cat" "needs" "lion" "+")
((triple1 triple5) -> (rule2 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The bear is not red.
False
2
inv-proof
[(((triple6) -> rule4))]
("bear" "is" "red" "-")
((triple6) -> (rule4 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The cat is kind.
True
5
proof
[(((((triple1 triple5) -> rule2) triple7) -> rule1))]
("cat" "is" "kind" "+")
((((triple1 triple5) -> (rule2 % int2)) triple7) -> (rule1 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The bear is not round.
False
3
inv-proof
[(((((triple6) -> rule4)) -> rule5))]
("bear" "is" "round" "-")
((((triple6) -> (rule4 % int2))) -> (rule5 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The cat visits the lion.
True
6
proof
[(((((((triple1 triple5) -> rule2) triple7) -> rule1)) -> rule6))]
("cat" "visits" "lion" "+")
((((((triple1 triple5) -> (rule2 % int3)) triple7) -> (rule1 % int2))) -> (rule6 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat needs the lion.
("cat" "needs" "lion" "+")
int3
The cat does not visit the lion.
False
6
inv-proof
[(((((((triple1 triple5) -> rule2) triple7) -> rule1)) -> rule6))]
("cat" "visits" "lion" "-")
((((((triple1 triple5) -> (rule2 % int3)) triple7) -> (rule1 % int2))) -> (rule6 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat needs the lion.
("cat" "needs" "lion" "+")
int3
The lion is not kind.
Unknown
inv-rconc
[@1: The lion is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "kind" "-")
The lion is round.
Unknown
rconc
[@1: The lion is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "is" "round" "+")
The lion does not visit the lion.
Unknown
inv-rconc
[@2: The lion visits the lion.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("lion" "visits" "lion" "-")
The cat visits the bear.
Unknown
random
[@0: The cat visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "bear" "+")
The lion does not eat the bear.
Unknown
inv-random
[@0: The lion eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "bear" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "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 eats the bear.
Unknown
random
[@0: The cat eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "bear" "+")
@0: The bear eats the cat.[(triple1)] The bear is kind.[(triple2)] The cat eats the lion.[(triple3)] The cat is blue.[(triple4)] The cat is round.[(triple5)] The lion needs the bear.[(triple6)] The lion visits the bear.[(triple7)] @1: The bear is red.[(((triple6) -> rule4))] The bear visits the lion.[(((triple2) -> rule6))] The cat needs the lion.[(((triple1 triple5) -> rule2))] @2: The bear is round.[(((((triple6) -> rule4)) -> rule5))] The cat is kind.[(((((triple1 triple5) -> rule2) triple7) -> rule1))] @3: The cat visits the lion.[(((((((triple1 triple5) -> rule2) triple7) -> rule1)) -> rule6))]
The bear eats the cat.
("bear" "eats" "cat" "+")
triple1
The bear is kind.
("bear" "is" "kind" "+")
triple2
The cat eats the lion.
("cat" "eats" "lion" "+")
triple3
The cat is blue.
("cat" "is" "blue" "+")
triple4
The cat is round.
("cat" "is" "round" "+")
triple5
The lion needs the bear.
("lion" "needs" "bear" "+")
triple6
The lion visits the bear.
("lion" "visits" "bear" "+")
triple7
The bear is red.
("bear" "is" "red" "+")
((triple6) -> (rule4 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear visits the lion.
("bear" "visits" "lion" "+")
((triple2) -> (rule6 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
((triple1 triple5) -> (rule2 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The bear is round.
("bear" "is" "round" "+")
((((triple6) -> (rule4 % int2))) -> (rule5 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
((((triple1 triple5) -> (rule2 % int2)) triple7) -> (rule1 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The cat visits the lion.
("cat" "visits" "lion" "+")
((((((triple1 triple5) -> (rule2 % int3)) triple7) -> (rule1 % int2))) -> (rule6 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat needs the lion.
("cat" "needs" "lion" "+")
int3