The bear sees the cat. The cat sees the bear. The tiger visits the cat. If something visits the bear and it is nice then the bear sees the tiger. If something visits the cat then it eats the bear. If something eats the bear then it sees the cat.
The bear sees the cat.
("bear" "sees" "cat" "+")
The cat sees the bear.
("cat" "sees" "bear" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If something visits the bear and it is nice then the bear sees the tiger.
((("something" "visits" "bear" "+") ("something" "is" "nice" "+")) -> ("bear" "sees" "tiger" "+"))
If something visits the cat then it eats the bear.
((("something" "visits" "cat" "+")) -> ("something" "eats" "bear" "+"))
If something eats the bear then it sees the cat.
((("something" "eats" "bear" "+")) -> ("something" "sees" "cat" "+"))
The tiger visits the cat.
True
1
proof
[(triple3)]
("tiger" "visits" "cat" "+")
triple3
The bear does not see the cat.
False
1
inv-proof
[(triple1)]
("bear" "sees" "cat" "-")
triple1
The tiger eats the bear.
True
2
proof
[(((triple3) -> rule2))]
("tiger" "eats" "bear" "+")
((triple3) -> (rule2 % int1))
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int1
The tiger does not eat the bear.
False
2
inv-proof
[(((triple3) -> rule2))]
("tiger" "eats" "bear" "-")
((triple3) -> (rule2 % int1))
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int1
The tiger sees the cat.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("tiger" "sees" "cat" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int2
The tiger does not see the cat.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("tiger" "sees" "cat" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int2
The cat does not eat the bear.
Unknown
inv-rconc
[@1: The cat eats the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "eats" "bear" "-")
The bear sees the tiger.
Unknown
rconc
[@1: The bear sees the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "sees" "tiger" "+")
The bear does not eat the bear.
Unknown
inv-rconc
[@1: The bear eats the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "eats" "bear" "-")
The tiger is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
The cat does not visit the bear.
Unknown
inv-random
[@0: The cat visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "bear" "-")
The tiger is red.
Unknown
random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "+")
@0: The bear sees the cat.[(triple1)] The cat sees the bear.[(triple2)] The tiger visits the cat.[(triple3)] @1: The tiger eats the bear.[(((triple3) -> rule2))] @2: The tiger sees the cat.[(((((triple3) -> rule2)) -> rule3))]
The bear sees the cat.
("bear" "sees" "cat" "+")
triple1
The cat sees the bear.
("cat" "sees" "bear" "+")
triple2
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple3
The tiger eats the bear.
("tiger" "eats" "bear" "+")
((triple3) -> (rule2 % int1))
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
int2