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