The bear chases the mouse. The bear is rough. The bear needs the mouse. The cat chases the bear. The cat is green. The cat is kind. The cat does not need the mouse. The cat visits the mouse. The mouse does not chase the bear. The mouse chases the cat. The mouse is green. The mouse is not kind. The mouse is not nice. The mouse is rough. The mouse is round. The mouse visits the bear. If the cat needs the bear then the cat is green. All nice people are green. If someone is round and they visit the bear then they are not nice. If the bear needs the mouse then the mouse needs the cat. If someone visits the mouse then the mouse does not visit the cat. If someone visits the bear and they are not nice then the bear visits the mouse.
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The cat chases the bear.
("cat" "chases" "bear" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat does not need the mouse.
("cat" "needs" "mouse" "-")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The mouse does not chase the bear.
("mouse" "chases" "bear" "-")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is not kind.
("mouse" "is" "kind" "-")
The mouse is not nice.
("mouse" "is" "nice" "-")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
If the cat needs the bear then the cat is green.
((("cat" "needs" "bear" "+")) -> ("cat" "is" "green" "+"))
All nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If someone is round and they visit the bear then they are not nice.
((("someone" "is" "round" "+") ("someone" "visits" "bear" "+")) -> ("someone" "is" "nice" "-"))
If the bear needs the mouse then the mouse needs the cat.
((("bear" "needs" "mouse" "+")) -> ("mouse" "needs" "cat" "+"))
If someone visits the mouse then the mouse does not visit the cat.
((("someone" "visits" "mouse" "+")) -> ("mouse" "visits" "cat" "-"))
If someone visits the bear and they are not nice then the bear visits the mouse.
((("someone" "visits" "bear" "+") ("someone" "is" "nice" "~")) -> ("bear" "visits" "mouse" "+"))
The cat does not need the mouse.
True
1
proof
[(triple7)]
("cat" "needs" "mouse" "-")
triple7
The mouse does not chase the cat.
False
1
inv-proof
[(triple10)]
("mouse" "chases" "cat" "-")
triple10
The mouse does not visit the cat.
True
2
proof
[(((triple8) -> rule5) OR ((((triple16 triple13) -> rule6)) -> rule5) OR ((((triple16 ((triple15 triple16) -> rule3)) -> rule6)) -> rule5))]
("mouse" "visits" "cat" "-")
((triple8) -> (rule5 % int1))
The mouse does not visit the cat.
("mouse" "visits" "cat" "-")
int1
((((triple16 triple13) -> (rule6 % int2))) -> (rule5 % int1))
The mouse does not visit the cat.
("mouse" "visits" "cat" "-")
int1
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int2
((((triple16 ((triple15 triple16) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse does not visit the cat.
("mouse" "visits" "cat" "-")
int1
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int2
The mouse is not nice.
("mouse" "is" "nice" "-")
int3
The bear does not visit the mouse.
False
3
inv-proof
[(((triple16 triple13) -> rule6) OR ((triple16 ((triple15 triple16) -> rule3)) -> rule6))]
("bear" "visits" "mouse" "-")
((triple16 triple13) -> (rule6 % int1))
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int1
((triple16 ((triple15 triple16) -> (rule3 % int2))) -> (rule6 % int1))
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int1
The mouse is not nice.
("mouse" "is" "nice" "-")
int2
The bear is not green.
Unknown
inv-rconc
[@1: The bear is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "green" "-")
The bear chases the bear.
Unknown
random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "+")
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The bear needs the cat.
Unknown
random
[@0: The bear needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "cat" "+")
@0: The bear chases the mouse.[(triple1)] The bear is rough.[(triple2)] The bear needs the mouse.[(triple3)] The cat chases the bear.[(triple4)] The cat does not need the mouse.[(triple7)] The cat is green.[(triple5)] The cat is kind.[(triple6)] The cat visits the mouse.[(triple8)] The mouse chases the cat.[(triple10)] The mouse does not chase the bear.[(triple9)] The mouse is green.[(triple11)] The mouse is not kind.[(triple12)] The mouse is not nice.[(triple13 OR ((triple15 triple16) -> rule3))] The mouse is rough.[(triple14)] The mouse is round.[(triple15)] The mouse visits the bear.[(triple16)] @1: The bear visits the mouse.[(((triple16 triple13) -> rule6) OR ((triple16 ((triple15 triple16) -> rule3)) -> rule6))] The mouse does not visit the cat.[(((triple8) -> rule5) OR ((((triple16 triple13) -> rule6)) -> rule5) OR ((((triple16 ((triple15 triple16) -> rule3)) -> rule6)) -> rule5))] The mouse needs the cat.[(((triple3) -> rule4))]
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple1
The bear is rough.
("bear" "is" "rough" "+")
triple2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple3
The cat chases the bear.
("cat" "chases" "bear" "+")
triple4
The cat does not need the mouse.
("cat" "needs" "mouse" "-")
triple7
The cat is green.
("cat" "is" "green" "+")
triple5
The cat is kind.
("cat" "is" "kind" "+")
triple6
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple8
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple10
The mouse does not chase the bear.
("mouse" "chases" "bear" "-")
triple9
The mouse is green.
("mouse" "is" "green" "+")
triple11
The mouse is not kind.
("mouse" "is" "kind" "-")
triple12
The mouse is not nice.
("mouse" "is" "nice" "-")
triple13
((triple15 triple16) -> (rule3 % int1))
The mouse is not nice.
("mouse" "is" "nice" "-")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
triple14
The mouse is round.
("mouse" "is" "round" "+")
triple15
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple16
The bear visits the mouse.
("bear" "visits" "mouse" "+")
((triple16 triple13) -> (rule6 % int1))
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int1
((triple16 ((triple15 triple16) -> (rule3 % int2))) -> (rule6 % int1))
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int1
The mouse is not nice.
("mouse" "is" "nice" "-")
int2
The mouse does not visit the cat.
("mouse" "visits" "cat" "-")
((triple8) -> (rule5 % int1))
The mouse does not visit the cat.
("mouse" "visits" "cat" "-")
int1
((((triple16 triple13) -> (rule6 % int2))) -> (rule5 % int1))
The mouse does not visit the cat.
("mouse" "visits" "cat" "-")
int1
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int2
((((triple16 ((triple15 triple16) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse does not visit the cat.
("mouse" "visits" "cat" "-")
int1
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int2
The mouse is not nice.
("mouse" "is" "nice" "-")
int3
The mouse needs the cat.
("mouse" "needs" "cat" "+")
((triple3) -> (rule4 % int1))
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int1