The bear needs the lion. The lion is kind. The lion is red. The lion needs the bear. The lion needs the tiger. The lion visits the tiger. The mouse is big. The mouse needs the bear. The mouse sees the bear. The mouse sees the lion. The mouse visits the bear. The mouse visits the tiger. The tiger is big. The tiger is blue. The tiger needs the bear. The tiger visits the bear. If someone sees the tiger then they are blue. If someone sees the bear then the bear sees the lion. If someone sees the mouse and the mouse is blue then they are red. If someone is blue then they see the mouse. If someone is big and kind then they need the tiger. If someone needs the tiger then they see the bear. If someone sees the bear and the bear visits the lion then the bear needs the tiger. If someone visits the tiger and the tiger is kind then the tiger visits the mouse. If someone sees the mouse then the mouse sees the tiger.
The bear needs the lion.
("bear" "needs" "lion" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is red.
("lion" "is" "red" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
If someone sees the tiger then they are blue.
((("someone" "sees" "tiger" "+")) -> ("someone" "is" "blue" "+"))
If someone sees the bear then the bear sees the lion.
((("someone" "sees" "bear" "+")) -> ("bear" "sees" "lion" "+"))
If someone sees the mouse and the mouse is blue then they are red.
((("someone" "sees" "mouse" "+") ("mouse" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If someone is blue then they see the mouse.
((("someone" "is" "blue" "+")) -> ("someone" "sees" "mouse" "+"))
If someone is big and kind then they need the tiger.
((("someone" "is" "big" "+") ("someone" "is" "kind" "+")) -> ("someone" "needs" "tiger" "+"))
If someone needs the tiger then they see the bear.
((("someone" "needs" "tiger" "+")) -> ("someone" "sees" "bear" "+"))
If someone sees the bear and the bear visits the lion then the bear needs the tiger.
((("someone" "sees" "bear" "+") ("bear" "visits" "lion" "+")) -> ("bear" "needs" "tiger" "+"))
If someone visits the tiger and the tiger is kind then the tiger visits the mouse.
((("someone" "visits" "tiger" "+") ("tiger" "is" "kind" "+")) -> ("tiger" "visits" "mouse" "+"))
If someone sees the mouse then the mouse sees the tiger.
((("someone" "sees" "mouse" "+")) -> ("mouse" "sees" "tiger" "+"))
The mouse sees the lion.
True
1
proof
[(triple10)]
("mouse" "sees" "lion" "+")
triple10
The bear does not need the lion.
False
1
inv-proof
[(triple1)]
("bear" "needs" "lion" "-")
triple1
The tiger sees the mouse.
True
2
proof
[(((triple14) -> rule4))]
("tiger" "sees" "mouse" "+")
((triple14) -> (rule4 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The lion does not see the bear.
False
2
inv-proof
[(((triple5) -> rule6))]
("lion" "sees" "bear" "-")
((triple5) -> (rule6 % int1))
The lion sees the bear.
("lion" "sees" "bear" "+")
int1
The mouse sees the tiger.
True
3
proof
[(((((triple14) -> rule4)) -> rule9))]
("mouse" "sees" "tiger" "+")
((((triple14) -> (rule4 % int2))) -> (rule9 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int2
The mouse does not see the tiger.
False
3
inv-proof
[(((((triple14) -> rule4)) -> rule9))]
("mouse" "sees" "tiger" "-")
((((triple14) -> (rule4 % int2))) -> (rule9 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int2
The mouse is blue.
True
4
proof
[(((((((triple14) -> rule4)) -> rule9)) -> rule1))]
("mouse" "is" "blue" "+")
((((((triple14) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int3
The mouse is not blue.
False
4
inv-proof
[(((((((triple14) -> rule4)) -> rule9)) -> rule1))]
("mouse" "is" "blue" "-")
((((((triple14) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int3
The mouse sees the mouse.
True
5
proof
[(((((((((triple14) -> rule4)) -> rule9)) -> rule1)) -> rule4))]
("mouse" "sees" "mouse" "+")
((((((((triple14) -> (rule4 % int4))) -> (rule9 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int3
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int4
The mouse does not see the mouse.
False
5
inv-proof
[(((((((((triple14) -> rule4)) -> rule9)) -> rule1)) -> rule4))]
("mouse" "sees" "mouse" "-")
((((((((triple14) -> (rule4 % int4))) -> (rule9 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int3
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int4
The mouse is red.
True
10
proof
[(((((((((((triple14) -> rule4)) -> rule9)) -> rule1)) -> rule4) ((((((triple14) -> rule4)) -> rule9)) -> rule1)) -> rule3))]
("mouse" "is" "red" "+")
((((((((((triple14) -> (rule4 % int5))) -> (rule9 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) ((((((triple14) -> (rule4 % int5))) -> (rule9 % int4))) -> (rule1 % int3))) -> (rule3 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int4
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int5
The mouse is not red.
False
10
inv-proof
[(((((((((((triple14) -> rule4)) -> rule9)) -> rule1)) -> rule4) ((((((triple14) -> rule4)) -> rule9)) -> rule1)) -> rule3))]
("mouse" "is" "red" "-")
((((((((((triple14) -> (rule4 % int5))) -> (rule9 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) ((((((triple14) -> (rule4 % int5))) -> (rule9 % int4))) -> (rule1 % int3))) -> (rule3 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int4
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int5
The bear does not see the mouse.
Unknown
inv-rconc
[@2: The bear sees the mouse.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("bear" "sees" "mouse" "-")
The lion sees the mouse.
Unknown
rconc
[@2: The lion sees the mouse.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("lion" "sees" "mouse" "+")
The mouse does not need the tiger.
Unknown
inv-rconc
[@1: The mouse needs the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "needs" "tiger" "-")
The bear is red.
Unknown
rconc
[@3: The bear is red.[CWA. Example of deepest failure = (rule3 <- rule4 <- rule1 <- FAIL)]]
("bear" "is" "red" "+")
The bear is not blue.
Unknown
inv-rconc
[@1: The bear is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "is" "blue" "-")
The bear sees the bear.
Unknown
rconc
[@2: The bear sees the bear.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("bear" "sees" "bear" "+")
The mouse does not need the lion.
Unknown
inv-random
[@0: The mouse needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "lion" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
The tiger is not nice.
Unknown
inv-random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "-")
The bear is big.
Unknown
random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "+")
The lion is not big.
Unknown
inv-random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "-")
The mouse visits the lion.
Unknown
random
[@0: The mouse visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "lion" "+")
@0: The bear needs the lion.[(triple1)] The lion is kind.[(triple2)] The lion is red.[(triple3)] The lion needs the bear.[(triple4)] The lion needs the tiger.[(triple5)] The lion visits the tiger.[(triple6)] The mouse is big.[(triple7)] The mouse needs the bear.[(triple8)] The mouse sees the bear.[(triple9)] The mouse sees the lion.[(triple10)] The mouse visits the bear.[(triple11)] The mouse visits the tiger.[(triple12)] The tiger is big.[(triple13)] The tiger is blue.[(triple14)] The tiger needs the bear.[(triple15)] The tiger visits the bear.[(triple16)] @1: The bear sees the lion.[(((triple9) -> rule2) OR ((((triple5) -> rule6)) -> rule2))] The lion sees the bear.[(((triple5) -> rule6))] The tiger sees the mouse.[(((triple14) -> rule4))] @2: The mouse sees the tiger.[(((((triple14) -> rule4)) -> rule9))] @3: The mouse is blue.[(((((((triple14) -> rule4)) -> rule9)) -> rule1))] @4: The mouse sees the mouse.[(((((((((triple14) -> rule4)) -> rule9)) -> rule1)) -> rule4))] The tiger is red.[(((((triple14) -> rule4) ((((((triple14) -> rule4)) -> rule9)) -> rule1)) -> rule3))] @5: The mouse is red.[(((((((((((triple14) -> rule4)) -> rule9)) -> rule1)) -> rule4) ((((((triple14) -> rule4)) -> rule9)) -> rule1)) -> rule3))]
The bear needs the lion.
("bear" "needs" "lion" "+")
triple1
The lion is kind.
("lion" "is" "kind" "+")
triple2
The lion is red.
("lion" "is" "red" "+")
triple3
The lion needs the bear.
("lion" "needs" "bear" "+")
triple4
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple5
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple6
The mouse is big.
("mouse" "is" "big" "+")
triple7
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple8
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple9
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple10
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple11
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple12
The tiger is big.
("tiger" "is" "big" "+")
triple13
The tiger is blue.
("tiger" "is" "blue" "+")
triple14
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple15
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple16
The bear sees the lion.
("bear" "sees" "lion" "+")
((triple9) -> (rule2 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
((((triple5) -> (rule6 % int2))) -> (rule2 % int1))
The bear sees the lion.
("bear" "sees" "lion" "+")
int1
The lion sees the bear.
("lion" "sees" "bear" "+")
int2
The lion sees the bear.
("lion" "sees" "bear" "+")
((triple5) -> (rule6 % int1))
The lion sees the bear.
("lion" "sees" "bear" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
((triple14) -> (rule4 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
((((triple14) -> (rule4 % int2))) -> (rule9 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
((((((triple14) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int3
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((((((((triple14) -> (rule4 % int4))) -> (rule9 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int3
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int4
The tiger is red.
("tiger" "is" "red" "+")
((((triple14) -> (rule4 % int4)) ((((((triple14) -> (rule4 % int4))) -> (rule9 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int3
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int4
The mouse is red.
("mouse" "is" "red" "+")
((((((((((triple14) -> (rule4 % int5))) -> (rule9 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) ((((((triple14) -> (rule4 % int5))) -> (rule9 % int4))) -> (rule1 % int3))) -> (rule3 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int4
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int5