The bear is young. The cat chases the bear. If someone chases the cat then they like the cat. If the bear is young and the bear visits the cat then the cat likes the bear. If someone is young then they visit the cat.
The bear is young.
("bear" "is" "young" "+")
The cat chases the bear.
("cat" "chases" "bear" "+")
If someone chases the cat then they like the cat.
((("someone" "chases" "cat" "+")) -> ("someone" "likes" "cat" "+"))
If the bear is young and the bear visits the cat then the cat likes the bear.
((("bear" "is" "young" "+") ("bear" "visits" "cat" "+")) -> ("cat" "likes" "bear" "+"))
If someone is young then they visit the cat.
((("someone" "is" "young" "+")) -> ("someone" "visits" "cat" "+"))
The bear is young.
True
1
proof
[(triple1)]
("bear" "is" "young" "+")
triple1
The bear is not young.
False
1
inv-proof
[(triple1)]
("bear" "is" "young" "-")
triple1
The bear visits the cat.
True
2
proof
[(((triple1) -> rule3))]
("bear" "visits" "cat" "+")
((triple1) -> (rule3 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The bear does not visit the cat.
False
2
inv-proof
[(((triple1) -> rule3))]
("bear" "visits" "cat" "-")
((triple1) -> (rule3 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The cat likes the bear.
True
4
proof
[(((triple1 ((triple1) -> rule3)) -> rule2))]
("cat" "likes" "bear" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The cat likes the bear.
("cat" "likes" "bear" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2
The cat does not like the bear.
False
4
inv-proof
[(((triple1 ((triple1) -> rule3)) -> rule2))]
("cat" "likes" "bear" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The cat likes the bear.
("cat" "likes" "bear" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2
The bear does not like the cat.
Unknown
inv-rconc
[@1: The bear likes the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "likes" "cat" "-")
The cat visits the cat.
Unknown
rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "visits" "cat" "+")
The cat does not like the cat.
Unknown
inv-rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "cat" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
The bear does not chase the bear.
Unknown
inv-random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
@0: The bear is young.[(triple1)] The cat chases the bear.[(triple2)] @1: The bear visits the cat.[(((triple1) -> rule3))] @2: The cat likes the bear.[(((triple1 ((triple1) -> rule3)) -> rule2))]
The bear is young.
("bear" "is" "young" "+")
triple1
The cat chases the bear.
("cat" "chases" "bear" "+")
triple2
The bear visits the cat.
("bear" "visits" "cat" "+")
((triple1) -> (rule3 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The cat likes the bear.
("cat" "likes" "bear" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The cat likes the bear.
("cat" "likes" "bear" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2