The bear does not chase the cat. The bear eats the cat. The bear is not blue. The bear is cold. The bear is kind. The bear is red. The bear visits the cat. The cat chases the bear. The cat eats the bear. The cat is kind. The cat is round. The cat visits the bear. If someone chases the bear then they are cold. If the cat chases the bear and the cat is cold then the cat eats the bear. If someone eats the bear and the bear eats the cat then they chase the bear. If someone eats the cat then the cat is not red. If someone visits the cat and they do not visit the bear then the bear visits the cat. If someone chases the bear and they are not red then they visit the cat. If the bear chases the cat and the cat does not visit the bear then the cat is kind. If the cat does not eat the bear then the bear chases the cat.
The bear does not chase the cat.
("bear" "chases" "cat" "-")
The bear eats the cat.
("bear" "eats" "cat" "+")
The bear is not blue.
("bear" "is" "blue" "-")
The bear is cold.
("bear" "is" "cold" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear is red.
("bear" "is" "red" "+")
The bear visits the cat.
("bear" "visits" "cat" "+")
The cat chases the bear.
("cat" "chases" "bear" "+")
The cat eats the bear.
("cat" "eats" "bear" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is round.
("cat" "is" "round" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
If someone chases the bear then they are cold.
((("someone" "chases" "bear" "+")) -> ("someone" "is" "cold" "+"))
If the cat chases the bear and the cat is cold then the cat eats the bear.
((("cat" "chases" "bear" "+") ("cat" "is" "cold" "+")) -> ("cat" "eats" "bear" "+"))
If someone eats the bear and the bear eats the cat then they chase the bear.
((("someone" "eats" "bear" "+") ("bear" "eats" "cat" "+")) -> ("someone" "chases" "bear" "+"))
If someone eats the cat then the cat is not red.
((("someone" "eats" "cat" "+")) -> ("cat" "is" "red" "-"))
If someone visits the cat and they do not visit the bear then the bear visits the cat.
((("someone" "visits" "cat" "+") ("someone" "visits" "bear" "~")) -> ("bear" "visits" "cat" "+"))
If someone chases the bear and they are not red then they visit the cat.
((("someone" "chases" "bear" "+") ("someone" "is" "red" "~")) -> ("someone" "visits" "cat" "+"))
If the bear chases the cat and the cat does not visit the bear then the cat is kind.
((("bear" "chases" "cat" "+") ("cat" "visits" "bear" "~")) -> ("cat" "is" "kind" "+"))
If the cat does not eat the bear then the bear chases the cat.
((("cat" "eats" "bear" "~")) -> ("bear" "chases" "cat" "+"))
The cat is round.
True
1
proof
[(triple11)]
("cat" "is" "round" "+")
triple11
The bear chases the cat.
False
1
inv-proof
[(triple1)]
("bear" "chases" "cat" "+")
triple1
The cat is cold.
True
2
proof
[(((triple8) -> rule1) OR ((((triple9 triple2) -> rule3)) -> rule1))]
("cat" "is" "cold" "+")
((triple8) -> (rule1 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
((((triple9 triple2) -> (rule3 % int2))) -> (rule1 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2
The cat is not cold.
False
2
inv-proof
[(((triple8) -> rule1) OR ((((triple9 triple2) -> rule3)) -> rule1))]
("cat" "is" "cold" "-")
((triple8) -> (rule1 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
((((triple9 triple2) -> (rule3 % int2))) -> (rule1 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2
The cat visits the cat.
True
4
proof
[(((triple8 ((triple2) -> rule4)) -> rule6) OR ((((triple9 triple2) -> rule3) ((triple2) -> rule4)) -> rule6))]
("cat" "visits" "cat" "+")
((triple8 ((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat is not red.
("cat" "is" "red" "-")
int2
((((triple9 triple2) -> (rule3 % int3)) ((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat is not red.
("cat" "is" "red" "-")
int2
The cat chases the bear.
("cat" "chases" "bear" "+")
int3
The cat does not visit the cat.
False
4
inv-proof
[(((triple8 ((triple2) -> rule4)) -> rule6) OR ((((triple9 triple2) -> rule3) ((triple2) -> rule4)) -> rule6))]
("cat" "visits" "cat" "-")
((triple8 ((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat is not red.
("cat" "is" "red" "-")
int2
((((triple9 triple2) -> (rule3 % int3)) ((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat is not red.
("cat" "is" "red" "-")
int2
The cat chases the bear.
("cat" "chases" "bear" "+")
int3
The bear does not chase the bear.
Unknown
inv-rconc
[@1: The bear chases the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "chases" "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 blue.
Unknown
inv-random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
The bear is not round.
Unknown
inv-random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
@0: The bear does not chase the cat.[(triple1)] The bear eats the cat.[(triple2)] The bear is cold.[(triple4)] The bear is kind.[(triple5)] The bear is not blue.[(triple3)] The bear is red.[(triple6)] The bear visits the cat.[(triple7)] The cat chases the bear.[(triple8 OR ((triple9 triple2) -> rule3))] The cat eats the bear.[(triple9 OR ((triple8 ((triple8) -> rule1)) -> rule2))] The cat is kind.[(triple10)] The cat is round.[(triple11)] The cat visits the bear.[(triple12)] @1: The cat is cold.[(((triple8) -> rule1) OR ((((triple9 triple2) -> rule3)) -> rule1))] The cat is not red.[(((triple2) -> rule4))] @2: The cat visits the cat.[(((triple8 ((triple2) -> rule4)) -> rule6) OR ((((triple9 triple2) -> rule3) ((triple2) -> rule4)) -> rule6))]
The bear does not chase the cat.
("bear" "chases" "cat" "-")
triple1
The bear eats the cat.
("bear" "eats" "cat" "+")
triple2
The bear is cold.
("bear" "is" "cold" "+")
triple4
The bear is kind.
("bear" "is" "kind" "+")
triple5
The bear is not blue.
("bear" "is" "blue" "-")
triple3
The bear is red.
("bear" "is" "red" "+")
triple6
The bear visits the cat.
("bear" "visits" "cat" "+")
triple7
The cat chases the bear.
("cat" "chases" "bear" "+")
triple8
((triple9 triple2) -> (rule3 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The cat eats the bear.
("cat" "eats" "bear" "+")
triple9
((triple8 ((triple8) -> (rule1 % int2))) -> (rule2 % int1))
The cat eats the bear.
("cat" "eats" "bear" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
triple10
The cat is round.
("cat" "is" "round" "+")
triple11
The cat visits the bear.
("cat" "visits" "bear" "+")
triple12
The cat is cold.
("cat" "is" "cold" "+")
((triple8) -> (rule1 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
((((triple9 triple2) -> (rule3 % int2))) -> (rule1 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2
The cat is not red.
("cat" "is" "red" "-")
((triple2) -> (rule4 % int1))
The cat is not red.
("cat" "is" "red" "-")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
((triple8 ((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat is not red.
("cat" "is" "red" "-")
int2
((((triple9 triple2) -> (rule3 % int3)) ((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat is not red.
("cat" "is" "red" "-")
int2
The cat chases the bear.
("cat" "chases" "bear" "+")
int3