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