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