The bear is blue. The cat is red. The cow sees the cat. If the bear chases the cow then the cow sees the bear. If someone chases the cow then the cow chases the cat. If the bear sees the cow then the bear is blue. If someone sees the bear then the bear chases the cat. If someone is red then they chase the cow. If someone chases the cow then they see the bear.
The bear is blue.
("bear" "is" "blue" "+")
The cat is red.
("cat" "is" "red" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
If the bear chases the cow then the cow sees the bear.
((("bear" "chases" "cow" "+")) -> ("cow" "sees" "bear" "+"))
If someone chases the cow then the cow chases the cat.
((("someone" "chases" "cow" "+")) -> ("cow" "chases" "cat" "+"))
If the bear sees the cow then the bear is blue.
((("bear" "sees" "cow" "+")) -> ("bear" "is" "blue" "+"))
If someone sees the bear then the bear chases the cat.
((("someone" "sees" "bear" "+")) -> ("bear" "chases" "cat" "+"))
If someone is red then they chase the cow.
((("someone" "is" "red" "+")) -> ("someone" "chases" "cow" "+"))
If someone chases the cow then they see the bear.
((("someone" "chases" "cow" "+")) -> ("someone" "sees" "bear" "+"))
The cow sees the cat.
True
1
proof
[(triple3)]
("cow" "sees" "cat" "+")
triple3
The bear is not blue.
False
1
inv-proof
[(triple1)]
("bear" "is" "blue" "-")
triple1
The cat chases the cow.
True
2
proof
[(((triple2) -> rule5))]
("cat" "chases" "cow" "+")
((triple2) -> (rule5 % int1))
The cat chases the cow.
("cat" "chases" "cow" "+")
int1
The cat does not chase the cow.
False
2
inv-proof
[(((triple2) -> rule5))]
("cat" "chases" "cow" "-")
((triple2) -> (rule5 % int1))
The cat chases the cow.
("cat" "chases" "cow" "+")
int1
The cow chases the cat.
True
3
proof
[(((((triple2) -> rule5)) -> rule2))]
("cow" "chases" "cat" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cat chases the cow.
("cat" "chases" "cow" "+")
int2
The cat does not see the bear.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule6))]
("cat" "sees" "bear" "-")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
The cat sees the bear.
("cat" "sees" "bear" "+")
int1
The cat chases the cow.
("cat" "chases" "cow" "+")
int2
The bear chases the cat.
True
4
proof
[(((((((triple2) -> rule5)) -> rule6)) -> rule4))]
("bear" "chases" "cat" "+")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The cat sees the bear.
("cat" "sees" "bear" "+")
int2
The cat chases the cow.
("cat" "chases" "cow" "+")
int3
The bear does not chase the cat.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule6)) -> rule4))]
("bear" "chases" "cat" "-")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The cat sees the bear.
("cat" "sees" "bear" "+")
int2
The cat chases the cow.
("cat" "chases" "cow" "+")
int3
The cow does not chase the cow.
Unknown
inv-rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "chases" "cow" "-")
The bear sees the bear.
Unknown
rconc
[@2: The bear sees the bear.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("bear" "sees" "bear" "+")
The bear does not chase the cow.
Unknown
inv-rconc
[@1: The bear chases the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "chases" "cow" "-")
The cow sees the bear.
Unknown
rconc
[@2: The cow sees the bear.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("cow" "sees" "bear" "+")
The cat is not blue.
Unknown
inv-random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "-")
The cat eats the bear.
Unknown
random
[@0: The cat eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "bear" "+")
The cat is not round.
Unknown
inv-random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
@0: The bear is blue.[(triple1)] The cat is red.[(triple2)] The cow sees the cat.[(triple3)] @1: The cat chases the cow.[(((triple2) -> rule5))] @2: The cat sees the bear.[(((((triple2) -> rule5)) -> rule6))] The cow chases the cat.[(((((triple2) -> rule5)) -> rule2))] @3: The bear chases the cat.[(((((((triple2) -> rule5)) -> rule6)) -> rule4))]
The bear is blue.
("bear" "is" "blue" "+")
triple1
The cat is red.
("cat" "is" "red" "+")
triple2
The cow sees the cat.
("cow" "sees" "cat" "+")
triple3
The cat chases the cow.
("cat" "chases" "cow" "+")
((triple2) -> (rule5 % int1))
The cat chases the cow.
("cat" "chases" "cow" "+")
int1
The cat sees the bear.
("cat" "sees" "bear" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
The cat sees the bear.
("cat" "sees" "bear" "+")
int1
The cat chases the cow.
("cat" "chases" "cow" "+")
int2
The cow chases the cat.
("cow" "chases" "cat" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cat chases the cow.
("cat" "chases" "cow" "+")
int2
The bear chases the cat.
("bear" "chases" "cat" "+")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The cat sees the bear.
("cat" "sees" "bear" "+")
int2
The cat chases the cow.
("cat" "chases" "cow" "+")
int3