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