The bear is kind. The bear visits the lion. The lion needs the mouse. The lion sees the mouse. The lion sees the squirrel. The lion does not visit the mouse. The mouse sees the squirrel. The mouse visits the bear. The squirrel visits the bear. The squirrel does not visit the mouse. If someone needs the squirrel then the squirrel needs the mouse. If someone needs the squirrel and the squirrel is kind then the squirrel needs the mouse. If someone needs the lion then they need the squirrel. If the bear is cold then the bear visits the mouse. If the squirrel visits the mouse and the bear does not see the squirrel then the mouse needs the bear. If someone sees the mouse and they visit the mouse then the mouse needs the bear. If someone needs the mouse then they need the lion. If someone is cold then they need the bear. If someone needs the bear and they do not see the squirrel then the squirrel is not cold.
The bear is kind.
("bear" "is" "kind" "+")
The bear visits the lion.
("bear" "visits" "lion" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The lion does not visit the mouse.
("lion" "visits" "mouse" "-")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
The squirrel does not visit the mouse.
("squirrel" "visits" "mouse" "-")
If someone needs the squirrel then the squirrel needs the mouse.
((("someone" "needs" "squirrel" "+")) -> ("squirrel" "needs" "mouse" "+"))
If someone needs the squirrel and the squirrel is kind then the squirrel needs the mouse.
((("someone" "needs" "squirrel" "+") ("squirrel" "is" "kind" "+")) -> ("squirrel" "needs" "mouse" "+"))
If someone needs the lion then they need the squirrel.
((("someone" "needs" "lion" "+")) -> ("someone" "needs" "squirrel" "+"))
If the bear is cold then the bear visits the mouse.
((("bear" "is" "cold" "+")) -> ("bear" "visits" "mouse" "+"))
If the squirrel visits the mouse and the bear does not see the squirrel then the mouse needs the bear.
((("squirrel" "visits" "mouse" "+") ("bear" "sees" "squirrel" "~")) -> ("mouse" "needs" "bear" "+"))
If someone sees the mouse and they visit the mouse then the mouse needs the bear.
((("someone" "sees" "mouse" "+") ("someone" "visits" "mouse" "+")) -> ("mouse" "needs" "bear" "+"))
If someone needs the mouse then they need the lion.
((("someone" "needs" "mouse" "+")) -> ("someone" "needs" "lion" "+"))
If someone is cold then they need the bear.
((("someone" "is" "cold" "+")) -> ("someone" "needs" "bear" "+"))
If someone needs the bear and they do not see the squirrel then the squirrel is not cold.
((("someone" "needs" "bear" "+") ("someone" "sees" "squirrel" "~")) -> ("squirrel" "is" "cold" "-"))
The mouse sees the squirrel.
True
1
proof
[(triple7)]
("mouse" "sees" "squirrel" "+")
triple7
The squirrel visits the mouse.
False
1
inv-proof
[(triple10)]
("squirrel" "visits" "mouse" "+")
triple10
The lion needs the lion.
True
2
proof
[(((triple3) -> rule7))]
("lion" "needs" "lion" "+")
((triple3) -> (rule7 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion does not need the lion.
False
2
inv-proof
[(((triple3) -> rule7))]
("lion" "needs" "lion" "-")
((triple3) -> (rule7 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion needs the squirrel.
True
3
proof
[(((((triple3) -> rule7)) -> rule3))]
("lion" "needs" "squirrel" "+")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion does not need the squirrel.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule3))]
("lion" "needs" "squirrel" "-")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The squirrel needs the mouse.
True
4
proof
[(((((((triple3) -> rule7)) -> rule3)) -> rule1))]
("squirrel" "needs" "mouse" "+")
((((((triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
int3
The squirrel does not need the mouse.
False
4
inv-proof
[(((((((triple3) -> rule7)) -> rule3)) -> rule1))]
("squirrel" "needs" "mouse" "-")
((((((triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
int3
The squirrel needs the lion.
True
5
proof
[(((((((((triple3) -> rule7)) -> rule3)) -> rule1)) -> rule7))]
("squirrel" "needs" "lion" "+")
((((((((triple3) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int2
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int3
The lion needs the lion.
("lion" "needs" "lion" "+")
int4
The squirrel does not need the lion.
False
5
inv-proof
[(((((((((triple3) -> rule7)) -> rule3)) -> rule1)) -> rule7))]
("squirrel" "needs" "lion" "-")
((((((((triple3) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int2
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int3
The lion needs the lion.
("lion" "needs" "lion" "+")
int4
The squirrel needs the squirrel.
True
6
proof
[(((((((((((triple3) -> rule7)) -> rule3)) -> rule1)) -> rule7)) -> rule3))]
("squirrel" "needs" "squirrel" "+")
((((((((((triple3) -> (rule7 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int2
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int3
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int4
The lion needs the lion.
("lion" "needs" "lion" "+")
int5
The squirrel does not need the squirrel.
False
6
inv-proof
[(((((((((((triple3) -> rule7)) -> rule3)) -> rule1)) -> rule7)) -> rule3))]
("squirrel" "needs" "squirrel" "-")
((((((((((triple3) -> (rule7 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int2
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int3
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int4
The lion needs the lion.
("lion" "needs" "lion" "+")
int5
The squirrel does not need the bear.
Unknown
inv-rconc
[@1: The squirrel needs the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "needs" "bear" "-")
The mouse needs the lion.
Unknown
rconc
[@1: The mouse needs the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "needs" "lion" "+")
The bear does not visit the mouse.
Unknown
inv-rconc
[@1: The bear visits the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "visits" "mouse" "-")
The bear needs the bear.
Unknown
rconc
[@1: The bear needs the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "needs" "bear" "+")
The lion does not need the bear.
Unknown
inv-rconc
[@1: The lion needs the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "needs" "bear" "-")
The mouse needs the bear.
Unknown
rconc
[@1: The mouse needs the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "needs" "bear" "+")
The mouse does not visit the squirrel.
Unknown
inv-random
[@0: The mouse visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "squirrel" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
The bear is not big.
Unknown
inv-random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
The bear does not see the bear.
Unknown
inv-random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "-")
The lion visits the bear.
Unknown
random
[@0: The lion visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "bear" "+")
@0: The bear is kind.[(triple1)] The bear visits the lion.[(triple2)] The lion does not visit the mouse.[(triple6)] The lion needs the mouse.[(triple3)] The lion sees the mouse.[(triple4)] The lion sees the squirrel.[(triple5)] The mouse sees the squirrel.[(triple7)] The mouse visits the bear.[(triple8)] The squirrel does not visit the mouse.[(triple10)] The squirrel visits the bear.[(triple9)] @1: The lion needs the lion.[(((triple3) -> rule7))] @2: The lion needs the squirrel.[(((((triple3) -> rule7)) -> rule3))] @3: The squirrel needs the mouse.[(((((((triple3) -> rule7)) -> rule3)) -> rule1))] @4: The squirrel needs the lion.[(((((((((triple3) -> rule7)) -> rule3)) -> rule1)) -> rule7))] @5: The squirrel needs the squirrel.[(((((((((((triple3) -> rule7)) -> rule3)) -> rule1)) -> rule7)) -> rule3))]
The bear is kind.
("bear" "is" "kind" "+")
triple1
The bear visits the lion.
("bear" "visits" "lion" "+")
triple2
The lion does not visit the mouse.
("lion" "visits" "mouse" "-")
triple6
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple3
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple4
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple5
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple7
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple8
The squirrel does not visit the mouse.
("squirrel" "visits" "mouse" "-")
triple10
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
triple9
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple3) -> (rule7 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
((((((triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
int3
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
((((((((triple3) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int2
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int3
The lion needs the lion.
("lion" "needs" "lion" "+")
int4
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((((((((((triple3) -> (rule7 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int2
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int3
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int4
The lion needs the lion.
("lion" "needs" "lion" "+")
int5