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