The bear chases the cat. The bear is green. The bear likes the cat. The bear needs the cat. The bear needs the mouse. The cat is kind. The cat is young. The cat likes the mouse. The cat needs the bear. The mouse chases the bear. The mouse chases the cat. The mouse is kind. The mouse is young. The mouse likes the bear. The mouse needs the bear. The mouse needs the cat. If someone is kind and green then they need the cat. Kind people are blue. If someone chases the cat then they are blue. If someone chases the bear and they are kind then they like the cat. If someone likes the cat and the cat chases the mouse then the cat chases the bear. If the cat chases the bear then the cat needs the mouse. If the mouse chases the bear then the mouse likes the bear. If someone is blue and they chase the cat then the cat chases the bear.
The bear chases the cat.
("bear" "chases" "cat" "+")
The bear is green.
("bear" "is" "green" "+")
The bear likes the cat.
("bear" "likes" "cat" "+")
The bear needs the cat.
("bear" "needs" "cat" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cat needs the bear.
("cat" "needs" "bear" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
If someone is kind and green then they need the cat.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "needs" "cat" "+"))
Kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If someone chases the cat then they are blue.
((("someone" "chases" "cat" "+")) -> ("someone" "is" "blue" "+"))
If someone chases the bear and they are kind then they like the cat.
((("someone" "chases" "bear" "+") ("someone" "is" "kind" "+")) -> ("someone" "likes" "cat" "+"))
If someone likes the cat and the cat chases the mouse then the cat chases the bear.
((("someone" "likes" "cat" "+") ("cat" "chases" "mouse" "+")) -> ("cat" "chases" "bear" "+"))
If the cat chases the bear then the cat needs the mouse.
((("cat" "chases" "bear" "+")) -> ("cat" "needs" "mouse" "+"))
If the mouse chases the bear then the mouse likes the bear.
((("mouse" "chases" "bear" "+")) -> ("mouse" "likes" "bear" "+"))
If someone is blue and they chase the cat then the cat chases the bear.
((("someone" "is" "blue" "+") ("someone" "chases" "cat" "+")) -> ("cat" "chases" "bear" "+"))
The cat likes the mouse.
True
1
proof
[(triple8)]
("cat" "likes" "mouse" "+")
triple8
The cat does not like the mouse.
False
1
inv-proof
[(triple8)]
("cat" "likes" "mouse" "-")
triple8
The cat is blue.
True
2
proof
[(((triple6) -> rule2))]
("cat" "is" "blue" "+")
((triple6) -> (rule2 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The bear is not blue.
False
2
inv-proof
[(((triple1) -> rule3))]
("bear" "is" "blue" "-")
((triple1) -> (rule3 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The cat chases the bear.
True
4
proof
[(((((triple1) -> rule3) triple1) -> rule8) OR ((((triple11) -> rule3) triple11) -> rule8) OR ((((triple12) -> rule2) triple11) -> rule8))]
("cat" "chases" "bear" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule8 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
((((triple11) -> (rule3 % int2)) triple11) -> (rule8 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
((((triple12) -> (rule2 % int2)) triple11) -> (rule8 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The cat does not chase the bear.
False
4
inv-proof
[(((((triple1) -> rule3) triple1) -> rule8) OR ((((triple11) -> rule3) triple11) -> rule8) OR ((((triple12) -> rule2) triple11) -> rule8))]
("cat" "chases" "bear" "-")
((((triple1) -> (rule3 % int2)) triple1) -> (rule8 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
((((triple11) -> (rule3 % int2)) triple11) -> (rule8 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
((((triple12) -> (rule2 % int2)) triple11) -> (rule8 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The cat needs the mouse.
True
5
proof
[(((((((triple1) -> rule3) triple1) -> rule8)) -> rule6) OR ((((((triple11) -> rule3) triple11) -> rule8)) -> rule6) OR ((((((triple12) -> rule2) triple11) -> rule8)) -> rule6))]
("cat" "needs" "mouse" "+")
((((((triple1) -> (rule3 % int3)) triple1) -> (rule8 % int2))) -> (rule6 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
((((((triple11) -> (rule3 % int3)) triple11) -> (rule8 % int2))) -> (rule6 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
((((((triple12) -> (rule2 % int3)) triple11) -> (rule8 % int2))) -> (rule6 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The cat does not like the cat.
False
6
inv-proof
[(((((((triple1) -> rule3) triple1) -> rule8) triple6) -> rule4) OR ((((((triple11) -> rule3) triple11) -> rule8) triple6) -> rule4) OR ((((((triple12) -> rule2) triple11) -> rule8) triple6) -> rule4))]
("cat" "likes" "cat" "-")
((((((triple1) -> (rule3 % int3)) triple1) -> (rule8 % int2)) triple6) -> (rule4 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
((((((triple11) -> (rule3 % int3)) triple11) -> (rule8 % int2)) triple6) -> (rule4 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
((((((triple12) -> (rule2 % int3)) triple11) -> (rule8 % int2)) triple6) -> (rule4 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The cat does not need the cat.
Unknown
inv-rconc
[@1: The cat needs the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "needs" "cat" "-")
The cat likes the bear.
Unknown
random
[@0: The cat likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "bear" "+")
The bear does not like the mouse.
Unknown
inv-random
[@0: The bear likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "mouse" "-")
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 nice.
Unknown
inv-random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
The bear does not chase the mouse.
Unknown
inv-random
[@0: The bear chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "mouse" "-")
The cat is green.
Unknown
random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "+")
@0: The bear chases the cat.[(triple1)] The bear is green.[(triple2)] The bear likes the cat.[(triple3)] The bear needs the cat.[(triple4)] The bear needs the mouse.[(triple5)] The cat is kind.[(triple6)] The cat is young.[(triple7)] The cat likes the mouse.[(triple8)] The cat needs the bear.[(triple9)] The mouse chases the bear.[(triple10)] The mouse chases the cat.[(triple11)] The mouse is kind.[(triple12)] The mouse is young.[(triple13)] The mouse likes the bear.[(triple14 OR ((triple10) -> rule7))] The mouse needs the bear.[(triple15)] The mouse needs the cat.[(triple16)] @1: The bear is blue.[(((triple1) -> rule3))] The cat is blue.[(((triple6) -> rule2))] The mouse is blue.[(((triple11) -> rule3) OR ((triple12) -> rule2))] The mouse likes the cat.[(((triple10 triple12) -> rule4))] @2: The cat chases the bear.[(((((triple1) -> rule3) triple1) -> rule8) OR ((((triple11) -> rule3) triple11) -> rule8) OR ((((triple12) -> rule2) triple11) -> rule8))] @3: The cat likes the cat.[(((((((triple1) -> rule3) triple1) -> rule8) triple6) -> rule4) OR ((((((triple11) -> rule3) triple11) -> rule8) triple6) -> rule4) OR ((((((triple12) -> rule2) triple11) -> rule8) triple6) -> rule4))] The cat needs the mouse.[(((((((triple1) -> rule3) triple1) -> rule8)) -> rule6) OR ((((((triple11) -> rule3) triple11) -> rule8)) -> rule6) OR ((((((triple12) -> rule2) triple11) -> rule8)) -> rule6))]
The bear chases the cat.
("bear" "chases" "cat" "+")
triple1
The bear is green.
("bear" "is" "green" "+")
triple2
The bear likes the cat.
("bear" "likes" "cat" "+")
triple3
The bear needs the cat.
("bear" "needs" "cat" "+")
triple4
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple5
The cat is kind.
("cat" "is" "kind" "+")
triple6
The cat is young.
("cat" "is" "young" "+")
triple7
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple8
The cat needs the bear.
("cat" "needs" "bear" "+")
triple9
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple10
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple11
The mouse is kind.
("mouse" "is" "kind" "+")
triple12
The mouse is young.
("mouse" "is" "young" "+")
triple13
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple14
((triple10) -> (rule7 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple15
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple16
The bear is blue.
("bear" "is" "blue" "+")
((triple1) -> (rule3 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
((triple6) -> (rule2 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
((triple11) -> (rule3 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((triple12) -> (rule2 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse likes the cat.
("mouse" "likes" "cat" "+")
((triple10 triple12) -> (rule4 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule8 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
((((triple11) -> (rule3 % int2)) triple11) -> (rule8 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
((((triple12) -> (rule2 % int2)) triple11) -> (rule8 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The cat likes the cat.
("cat" "likes" "cat" "+")
((((((triple1) -> (rule3 % int3)) triple1) -> (rule8 % int2)) triple6) -> (rule4 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
((((((triple11) -> (rule3 % int3)) triple11) -> (rule8 % int2)) triple6) -> (rule4 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
((((((triple12) -> (rule2 % int3)) triple11) -> (rule8 % int2)) triple6) -> (rule4 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The cat needs the mouse.
("cat" "needs" "mouse" "+")
((((((triple1) -> (rule3 % int3)) triple1) -> (rule8 % int2))) -> (rule6 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
((((((triple11) -> (rule3 % int3)) triple11) -> (rule8 % int2))) -> (rule6 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
((((((triple12) -> (rule2 % int3)) triple11) -> (rule8 % int2))) -> (rule6 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3