The bear chases the mouse. The bear likes the cat. The bear sees the mouse. The cat chases the bear. The cat chases the mouse. The cat is round. The cat likes the mouse. The cat sees the bear. The mouse chases the cat. The mouse is big. The mouse is nice. The mouse sees the bear. If someone chases the cat then the cat sees the bear. If someone sees the bear and they like the mouse then the mouse is kind. If the mouse likes the cat and the mouse is green then the mouse chases the cat. If someone is green then they like the mouse. If the mouse chases the bear then the bear is big. If the mouse is kind then the mouse is green.
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The bear likes the cat.
("bear" "likes" "cat" "+")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The cat chases the bear.
("cat" "chases" "bear" "+")
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat is round.
("cat" "is" "round" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cat sees the bear.
("cat" "sees" "bear" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
If someone chases the cat then the cat sees the bear.
((("someone" "chases" "cat" "+")) -> ("cat" "sees" "bear" "+"))
If someone sees the bear and they like the mouse then the mouse is kind.
((("someone" "sees" "bear" "+") ("someone" "likes" "mouse" "+")) -> ("mouse" "is" "kind" "+"))
If the mouse likes the cat and the mouse is green then the mouse chases the cat.
((("mouse" "likes" "cat" "+") ("mouse" "is" "green" "+")) -> ("mouse" "chases" "cat" "+"))
If someone is green then they like the mouse.
((("someone" "is" "green" "+")) -> ("someone" "likes" "mouse" "+"))
If the mouse chases the bear then the bear is big.
((("mouse" "chases" "bear" "+")) -> ("bear" "is" "big" "+"))
If the mouse is kind then the mouse is green.
((("mouse" "is" "kind" "+")) -> ("mouse" "is" "green" "+"))
The cat sees the bear.
True
1
proof
[(triple8 OR ((triple9) -> rule1))]
("cat" "sees" "bear" "+")
triple8
((triple9) -> (rule1 % int1))
The cat sees the bear.
("cat" "sees" "bear" "+")
int1
The bear does not chase the mouse.
False
1
inv-proof
[(triple1)]
("bear" "chases" "mouse" "-")
triple1
The mouse is kind.
True
3
proof
[(((triple8 triple7) -> rule2) OR ((((triple9) -> rule1) triple7) -> rule2))]
("mouse" "is" "kind" "+")
((triple8 triple7) -> (rule2 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
((((triple9) -> (rule1 % int2)) triple7) -> (rule2 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The cat sees the bear.
("cat" "sees" "bear" "+")
int2
The mouse is not kind.
False
3
inv-proof
[(((triple8 triple7) -> rule2) OR ((((triple9) -> rule1) triple7) -> rule2))]
("mouse" "is" "kind" "-")
((triple8 triple7) -> (rule2 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
((((triple9) -> (rule1 % int2)) triple7) -> (rule2 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The cat sees the bear.
("cat" "sees" "bear" "+")
int2
The mouse is green.
True
4
proof
[(((((triple8 triple7) -> rule2)) -> rule6) OR ((((((triple9) -> rule1) triple7) -> rule2)) -> rule6))]
("mouse" "is" "green" "+")
((((triple8 triple7) -> (rule2 % int2))) -> (rule6 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
((((((triple9) -> (rule1 % int3)) triple7) -> (rule2 % int2))) -> (rule6 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The cat sees the bear.
("cat" "sees" "bear" "+")
int3
The mouse is not green.
False
4
inv-proof
[(((((triple8 triple7) -> rule2)) -> rule6) OR ((((((triple9) -> rule1) triple7) -> rule2)) -> rule6))]
("mouse" "is" "green" "-")
((((triple8 triple7) -> (rule2 % int2))) -> (rule6 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
((((((triple9) -> (rule1 % int3)) triple7) -> (rule2 % int2))) -> (rule6 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The cat sees the bear.
("cat" "sees" "bear" "+")
int3
The mouse likes the mouse.
True
5
proof
[(((((((triple8 triple7) -> rule2)) -> rule6)) -> rule4) OR ((((((((triple9) -> rule1) triple7) -> rule2)) -> rule6)) -> rule4))]
("mouse" "likes" "mouse" "+")
((((((triple8 triple7) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
((((((((triple9) -> (rule1 % int4)) triple7) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The cat sees the bear.
("cat" "sees" "bear" "+")
int4
The mouse does not like the mouse.
False
5
inv-proof
[(((((((triple8 triple7) -> rule2)) -> rule6)) -> rule4) OR ((((((((triple9) -> rule1) triple7) -> rule2)) -> rule6)) -> rule4))]
("mouse" "likes" "mouse" "-")
((((((triple8 triple7) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
((((((((triple9) -> (rule1 % int4)) triple7) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The cat sees the bear.
("cat" "sees" "bear" "+")
int4
The bear does not like the mouse.
Unknown
inv-rconc
[@1: The bear likes the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "likes" "mouse" "-")
The bear is big.
Unknown
rconc
[@1: The bear is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "is" "big" "+")
The cat is not nice.
Unknown
inv-random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "-")
The mouse is round.
Unknown
random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "+")
The mouse does not see the cat.
Unknown
inv-random
[@0: The mouse sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "cat" "-")
The mouse chases the bear.
Unknown
random
[@0: The mouse chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "bear" "+")
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
@0: The bear chases the mouse.[(triple1)] The bear likes the cat.[(triple2)] The bear sees the mouse.[(triple3)] The cat chases the bear.[(triple4)] The cat chases the mouse.[(triple5)] The cat is round.[(triple6)] The cat likes the mouse.[(triple7)] The cat sees the bear.[(triple8 OR ((triple9) -> rule1))] The mouse chases the cat.[(triple9)] The mouse is big.[(triple10)] The mouse is nice.[(triple11)] The mouse sees the bear.[(triple12)] @1: The mouse is kind.[(((triple8 triple7) -> rule2) OR ((((triple9) -> rule1) triple7) -> rule2))] @2: The mouse is green.[(((((triple8 triple7) -> rule2)) -> rule6) OR ((((((triple9) -> rule1) triple7) -> rule2)) -> rule6))] @3: The mouse likes the mouse.[(((((((triple8 triple7) -> rule2)) -> rule6)) -> rule4) OR ((((((((triple9) -> rule1) triple7) -> rule2)) -> rule6)) -> rule4))]
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple1
The bear likes the cat.
("bear" "likes" "cat" "+")
triple2
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple3
The cat chases the bear.
("cat" "chases" "bear" "+")
triple4
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple5
The cat is round.
("cat" "is" "round" "+")
triple6
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple7
The cat sees the bear.
("cat" "sees" "bear" "+")
triple8
((triple9) -> (rule1 % int1))
The cat sees the bear.
("cat" "sees" "bear" "+")
int1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple9
The mouse is big.
("mouse" "is" "big" "+")
triple10
The mouse is nice.
("mouse" "is" "nice" "+")
triple11
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple12
The mouse is kind.
("mouse" "is" "kind" "+")
((triple8 triple7) -> (rule2 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
((((triple9) -> (rule1 % int2)) triple7) -> (rule2 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The cat sees the bear.
("cat" "sees" "bear" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
((((triple8 triple7) -> (rule2 % int2))) -> (rule6 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
((((((triple9) -> (rule1 % int3)) triple7) -> (rule2 % int2))) -> (rule6 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The cat sees the bear.
("cat" "sees" "bear" "+")
int3
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((((((triple8 triple7) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
((((((((triple9) -> (rule1 % int4)) triple7) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The cat sees the bear.
("cat" "sees" "bear" "+")
int4