The bear eats the cat. The bear likes the cat. The cat eats the bear. If something likes the bear and it sees the cat then it likes the cat. If something likes the bear and it eats the bear then it likes the cat. If something likes the cat then it sees the cat. If something likes the bear then it is not green. If something sees the cat then the cat likes the bear. If something sees the cat and it does not like the cat then the cat is nice.
The bear eats the cat.
("bear" "eats" "cat" "+")
The bear likes the cat.
("bear" "likes" "cat" "+")
The cat eats the bear.
("cat" "eats" "bear" "+")
If something likes the bear and it sees the cat then it likes the cat.
((("something" "likes" "bear" "+") ("something" "sees" "cat" "+")) -> ("something" "likes" "cat" "+"))
If something likes the bear and it eats the bear then it likes the cat.
((("something" "likes" "bear" "+") ("something" "eats" "bear" "+")) -> ("something" "likes" "cat" "+"))
If something likes the cat then it sees the cat.
((("something" "likes" "cat" "+")) -> ("something" "sees" "cat" "+"))
If something likes the bear then it is not green.
((("something" "likes" "bear" "+")) -> ("something" "is" "green" "-"))
If something sees the cat then the cat likes the bear.
((("something" "sees" "cat" "+")) -> ("cat" "likes" "bear" "+"))
If something sees the cat and it does not like the cat then the cat is nice.
((("something" "sees" "cat" "+") ("something" "likes" "cat" "~")) -> ("cat" "is" "nice" "+"))
The bear eats the cat.
True
1
proof
[(triple1)]
("bear" "eats" "cat" "+")
triple1
The bear does not like the cat.
False
1
inv-proof
[(triple2)]
("bear" "likes" "cat" "-")
triple2
The bear sees the cat.
True
2
proof
[(((triple2) -> rule3))]
("bear" "sees" "cat" "+")
((triple2) -> (rule3 % int1))
The bear sees the cat.
("bear" "sees" "cat" "+")
int1
The bear does not see the cat.
False
2
inv-proof
[(((triple2) -> rule3))]
("bear" "sees" "cat" "-")
((triple2) -> (rule3 % int1))
The bear sees the cat.
("bear" "sees" "cat" "+")
int1
The cat likes the bear.
True
3
proof
[(((((triple2) -> rule3)) -> rule5))]
("cat" "likes" "bear" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
The cat likes the bear.
("cat" "likes" "bear" "+")
int1
The bear sees the cat.
("bear" "sees" "cat" "+")
int2
The cat does not like the bear.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule5))]
("cat" "likes" "bear" "-")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
The cat likes the bear.
("cat" "likes" "bear" "+")
int1
The bear sees the cat.
("bear" "sees" "cat" "+")
int2
The cat is not green.
True
4
proof
[(((((((triple2) -> rule3)) -> rule5)) -> rule4))]
("cat" "is" "green" "-")
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The cat is not green.
("cat" "is" "green" "-")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The bear sees the cat.
("bear" "sees" "cat" "+")
int3
The cat is green.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule5)) -> rule4))]
("cat" "is" "green" "+")
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The cat is not green.
("cat" "is" "green" "-")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The bear sees the cat.
("bear" "sees" "cat" "+")
int3
The cat is not nice.
Unknown
inv-rconc
[@1: The cat is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "is" "nice" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The bear eats the bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
The cat is not big.
Unknown
inv-random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
The bear is not young.
Unknown
inv-random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "-")
The cat sees the bear.
Unknown
random
[@0: The cat sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "bear" "+")
@0: The bear eats the cat.[(triple1)] The bear likes the cat.[(triple2)] The cat eats the bear.[(triple3)] @1: The bear sees the cat.[(((triple2) -> rule3))] @2: The cat likes the bear.[(((((triple2) -> rule3)) -> rule5))] @3: The cat is not green.[(((((((triple2) -> rule3)) -> rule5)) -> rule4))] The cat likes the cat.[(((((((triple2) -> rule3)) -> rule5) triple3) -> rule2))] @4: The cat sees the cat.[(((((((((triple2) -> rule3)) -> rule5) triple3) -> rule2)) -> rule3))]
The bear eats the cat.
("bear" "eats" "cat" "+")
triple1
The bear likes the cat.
("bear" "likes" "cat" "+")
triple2
The cat eats the bear.
("cat" "eats" "bear" "+")
triple3
The bear sees the cat.
("bear" "sees" "cat" "+")
((triple2) -> (rule3 % int1))
The bear sees the cat.
("bear" "sees" "cat" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
The cat likes the bear.
("cat" "likes" "bear" "+")
int1
The bear sees the cat.
("bear" "sees" "cat" "+")
int2
The cat is not green.
("cat" "is" "green" "-")
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The cat is not green.
("cat" "is" "green" "-")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The bear sees the cat.
("bear" "sees" "cat" "+")
int3
The cat likes the cat.
("cat" "likes" "cat" "+")
((((((triple2) -> (rule3 % int3))) -> (rule5 % int2)) triple3) -> (rule2 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
int2
The bear sees the cat.
("bear" "sees" "cat" "+")
int3
The cat sees the cat.
("cat" "sees" "cat" "+")
((((((((triple2) -> (rule3 % int4))) -> (rule5 % int3)) triple3) -> (rule2 % int2))) -> (rule3 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat likes the bear.
("cat" "likes" "bear" "+")
int3
The bear sees the cat.
("bear" "sees" "cat" "+")
int4