The bear eats the cat. The bear is blue. The bear sees the mouse. The cat eats the bear. The cat is rough. The cat likes the bear. The cat likes the lion. The cat likes the mouse. The cat sees the lion. The lion is green. The lion likes the cat. The lion likes the mouse. The lion sees the cat. The mouse eats the lion. The mouse likes the cat. The mouse likes the lion. If someone likes the bear then they see the mouse. If someone is rough and they like the lion then the lion eats the cat. If someone is young and they like the bear then the bear sees the lion. If someone is rough and they eat the cat then they see the bear. If someone sees the bear then the bear sees the lion. If someone eats the bear then the bear is rough. If someone eats the bear then they like the cat. If someone sees the bear then they are red.
The bear eats the cat.
("bear" "eats" "cat" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The cat eats the bear.
("cat" "eats" "bear" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat likes the bear.
("cat" "likes" "bear" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The lion is green.
("lion" "is" "green" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
If someone likes the bear then they see the mouse.
((("someone" "likes" "bear" "+")) -> ("someone" "sees" "mouse" "+"))
If someone is rough and they like the lion then the lion eats the cat.
((("someone" "is" "rough" "+") ("someone" "likes" "lion" "+")) -> ("lion" "eats" "cat" "+"))
If someone is young and they like the bear then the bear sees the lion.
((("someone" "is" "young" "+") ("someone" "likes" "bear" "+")) -> ("bear" "sees" "lion" "+"))
If someone is rough and they eat the cat then they see the bear.
((("someone" "is" "rough" "+") ("someone" "eats" "cat" "+")) -> ("someone" "sees" "bear" "+"))
If someone sees the bear then the bear sees the lion.
((("someone" "sees" "bear" "+")) -> ("bear" "sees" "lion" "+"))
If someone eats the bear then the bear is rough.
((("someone" "eats" "bear" "+")) -> ("bear" "is" "rough" "+"))
If someone eats the bear then they like the cat.
((("someone" "eats" "bear" "+")) -> ("someone" "likes" "cat" "+"))
If someone sees the bear then they are red.
((("someone" "sees" "bear" "+")) -> ("someone" "is" "red" "+"))
The cat eats the bear.
True
1
proof
[(triple4)]
("cat" "eats" "bear" "+")
triple4
The bear does not eat the cat.
False
1
inv-proof
[(triple1)]
("bear" "eats" "cat" "-")
triple1
The cat sees the mouse.
True
2
proof
[(((triple6) -> rule1))]
("cat" "sees" "mouse" "+")
((triple6) -> (rule1 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat does not see the mouse.
False
2
inv-proof
[(((triple6) -> rule1))]
("cat" "sees" "mouse" "-")
((triple6) -> (rule1 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The bear sees the bear.
True
4
proof
[(((((triple4) -> rule6) triple1) -> rule4))]
("bear" "sees" "bear" "+")
((((triple4) -> (rule6 % int2)) triple1) -> (rule4 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear does not see the bear.
False
4
inv-proof
[(((((triple4) -> rule6) triple1) -> rule4))]
("bear" "sees" "bear" "-")
((((triple4) -> (rule6 % int2)) triple1) -> (rule4 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear sees the lion.
True
5
proof
[(((((((triple4) -> rule6) triple1) -> rule4)) -> rule5))]
("bear" "sees" "lion" "+")
((((((triple4) -> (rule6 % int3)) triple1) -> (rule4 % int2))) -> (rule5 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear is rough.
("bear" "is" "rough" "+")
int3
The bear does not see the lion.
False
5
inv-proof
[(((((((triple4) -> rule6) triple1) -> rule4)) -> rule5))]
("bear" "sees" "lion" "-")
((((((triple4) -> (rule6 % int3)) triple1) -> (rule4 % int2))) -> (rule5 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear is rough.
("bear" "is" "rough" "+")
int3
The lion does not see the bear.
Unknown
inv-rconc
[@1: The lion sees the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "sees" "bear" "-")
The lion sees the mouse.
Unknown
rconc
[@1: The lion sees the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "sees" "mouse" "+")
The cat does not see the bear.
Unknown
inv-rconc
[@1: The cat sees the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "sees" "bear" "-")
The lion is red.
Unknown
rconc
[@2: The lion is red.[CWA. Example of deepest failure = (rule8 <- rule4 <- FAIL)]]
("lion" "is" "red" "+")
The lion does not eat the bear.
Unknown
inv-random
[@0: The lion eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "bear" "-")
The bear is green.
Unknown
random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "+")
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
@0: The bear eats the cat.[(triple1)] The bear is blue.[(triple2)] The bear sees the mouse.[(triple3)] The cat eats the bear.[(triple4)] The cat is rough.[(triple5)] The cat likes the bear.[(triple6)] The cat likes the lion.[(triple7)] The cat likes the mouse.[(triple8)] The cat sees the lion.[(triple9)] The lion is green.[(triple10)] The lion likes the cat.[(triple11)] The lion likes the mouse.[(triple12)] The lion sees the cat.[(triple13)] The mouse eats the lion.[(triple14)] The mouse likes the cat.[(triple15)] The mouse likes the lion.[(triple16)] @1: The bear is rough.[(((triple4) -> rule6))] The cat likes the cat.[(((triple4) -> rule7))] The cat sees the mouse.[(((triple6) -> rule1))] The lion eats the cat.[(((triple5 triple7) -> rule2))] @2: The bear sees the bear.[(((((triple4) -> rule6) triple1) -> rule4))] @3: The bear is red.[(((((((triple4) -> rule6) triple1) -> rule4)) -> rule8))] The bear sees the lion.[(((((((triple4) -> rule6) triple1) -> rule4)) -> rule5))]
The bear eats the cat.
("bear" "eats" "cat" "+")
triple1
The bear is blue.
("bear" "is" "blue" "+")
triple2
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple3
The cat eats the bear.
("cat" "eats" "bear" "+")
triple4
The cat is rough.
("cat" "is" "rough" "+")
triple5
The cat likes the bear.
("cat" "likes" "bear" "+")
triple6
The cat likes the lion.
("cat" "likes" "lion" "+")
triple7
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple8
The cat sees the lion.
("cat" "sees" "lion" "+")
triple9
The lion is green.
("lion" "is" "green" "+")
triple10
The lion likes the cat.
("lion" "likes" "cat" "+")
triple11
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple12
The lion sees the cat.
("lion" "sees" "cat" "+")
triple13
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple14
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple15
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple16
The bear is rough.
("bear" "is" "rough" "+")
((triple4) -> (rule6 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
((triple4) -> (rule7 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
((triple6) -> (rule1 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
((triple5 triple7) -> (rule2 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
((((triple4) -> (rule6 % int2)) triple1) -> (rule4 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear is red.
("bear" "is" "red" "+")
((((((triple4) -> (rule6 % int3)) triple1) -> (rule4 % int2))) -> (rule8 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear is rough.
("bear" "is" "rough" "+")
int3
The bear sees the lion.
("bear" "sees" "lion" "+")
((((((triple4) -> (rule6 % int3)) triple1) -> (rule4 % int2))) -> (rule5 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
int2
The bear is rough.
("bear" "is" "rough" "+")
int3