The bear needs the cat. The bear needs the mouse. The bear visits the mouse. The cat needs the rabbit. The cat visits the mouse. The cat visits the rabbit. The mouse needs the cat. The mouse sees the bear. The rabbit is rough. The rabbit does not see the cat. The rabbit sees the mouse. The rabbit visits the bear. If someone sees the rabbit and the rabbit sees the mouse then they are nice. If someone needs the bear then they are nice. If someone visits the mouse and they do not see the bear then the bear does not see the mouse. Nice people are red. If someone sees the cat and they visit the bear then the bear is not red. If the bear is round and the bear sees the rabbit then the rabbit does not visit the mouse. If someone visits the mouse and they are red then the mouse is nice. If the mouse sees the cat then the cat is not green. If someone visits the mouse then they need the bear.
The bear needs the cat.
("bear" "needs" "cat" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit does not see the cat.
("rabbit" "sees" "cat" "-")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
If someone sees the rabbit and the rabbit sees the mouse then they are nice.
((("someone" "sees" "rabbit" "+") ("rabbit" "sees" "mouse" "+")) -> ("someone" "is" "nice" "+"))
If someone needs the bear then they are nice.
((("someone" "needs" "bear" "+")) -> ("someone" "is" "nice" "+"))
If someone visits the mouse and they do not see the bear then the bear does not see the mouse.
((("someone" "visits" "mouse" "+") ("someone" "sees" "bear" "~")) -> ("bear" "sees" "mouse" "-"))
Nice people are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If someone sees the cat and they visit the bear then the bear is not red.
((("someone" "sees" "cat" "+") ("someone" "visits" "bear" "+")) -> ("bear" "is" "red" "-"))
If the bear is round and the bear sees the rabbit then the rabbit does not visit the mouse.
((("bear" "is" "round" "+") ("bear" "sees" "rabbit" "+")) -> ("rabbit" "visits" "mouse" "-"))
If someone visits the mouse and they are red then the mouse is nice.
((("someone" "visits" "mouse" "+") ("someone" "is" "red" "+")) -> ("mouse" "is" "nice" "+"))
If the mouse sees the cat then the cat is not green.
((("mouse" "sees" "cat" "+")) -> ("cat" "is" "green" "-"))
If someone visits the mouse then they need the bear.
((("someone" "visits" "mouse" "+")) -> ("someone" "needs" "bear" "+"))
The rabbit visits the bear.
True
1
proof
[(triple12)]
("rabbit" "visits" "bear" "+")
triple12
The mouse does not see the bear.
False
1
inv-proof
[(triple8)]
("mouse" "sees" "bear" "-")
triple8
The bear needs the bear.
True
2
proof
[(((triple3) -> rule9))]
("bear" "needs" "bear" "+")
((triple3) -> (rule9 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear does not need the bear.
False
2
inv-proof
[(((triple3) -> rule9))]
("bear" "needs" "bear" "-")
((triple3) -> (rule9 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The cat is nice.
True
3
proof
[(((((triple5) -> rule9)) -> rule2))]
("cat" "is" "nice" "+")
((((triple5) -> (rule9 % int2))) -> (rule2 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat needs the bear.
("cat" "needs" "bear" "+")
int2
The bear is not nice.
False
3
inv-proof
[(((((triple3) -> rule9)) -> rule2))]
("bear" "is" "nice" "-")
((((triple3) -> (rule9 % int2))) -> (rule2 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
The bear is red.
True
4
proof
[(((((((triple3) -> rule9)) -> rule2)) -> rule4))]
("bear" "is" "red" "+")
((((((triple3) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear needs the bear.
("bear" "needs" "bear" "+")
int3
The bear is not red.
False
4
inv-proof
[(((((((triple3) -> rule9)) -> rule2)) -> rule4))]
("bear" "is" "red" "-")
((((((triple3) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear needs the bear.
("bear" "needs" "bear" "+")
int3
The mouse is nice.
True
6
proof
[(((triple3 ((((((triple3) -> rule9)) -> rule2)) -> rule4)) -> rule7) OR ((triple5 ((((((triple5) -> rule9)) -> rule2)) -> rule4)) -> rule7))]
("mouse" "is" "nice" "+")
((triple3 ((((((triple3) -> (rule9 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The bear needs the bear.
("bear" "needs" "bear" "+")
int4
((triple5 ((((((triple5) -> (rule9 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The cat needs the bear.
("cat" "needs" "bear" "+")
int4
The mouse is not nice.
False
6
inv-proof
[(((triple3 ((((((triple3) -> rule9)) -> rule2)) -> rule4)) -> rule7) OR ((triple5 ((((((triple5) -> rule9)) -> rule2)) -> rule4)) -> rule7))]
("mouse" "is" "nice" "-")
((triple3 ((((((triple3) -> (rule9 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The bear needs the bear.
("bear" "needs" "bear" "+")
int4
((triple5 ((((((triple5) -> (rule9 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The cat needs the bear.
("cat" "needs" "bear" "+")
int4
The mouse is red.
True
7
proof
[(((((triple3 ((((((triple3) -> rule9)) -> rule2)) -> rule4)) -> rule7)) -> rule4) OR ((((triple5 ((((((triple5) -> rule9)) -> rule2)) -> rule4)) -> rule7)) -> rule4))]
("mouse" "is" "red" "+")
((((triple3 ((((((triple3) -> (rule9 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The bear is nice.
("bear" "is" "nice" "+")
int4
The bear needs the bear.
("bear" "needs" "bear" "+")
int5
((((triple5 ((((((triple5) -> (rule9 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The cat is nice.
("cat" "is" "nice" "+")
int4
The cat needs the bear.
("cat" "needs" "bear" "+")
int5
The mouse is not red.
False
7
inv-proof
[(((((triple3 ((((((triple3) -> rule9)) -> rule2)) -> rule4)) -> rule7)) -> rule4) OR ((((triple5 ((((((triple5) -> rule9)) -> rule2)) -> rule4)) -> rule7)) -> rule4))]
("mouse" "is" "red" "-")
((((triple3 ((((((triple3) -> (rule9 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The bear is nice.
("bear" "is" "nice" "+")
int4
The bear needs the bear.
("bear" "needs" "bear" "+")
int5
((((triple5 ((((((triple5) -> (rule9 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The cat is nice.
("cat" "is" "nice" "+")
int4
The cat needs the bear.
("cat" "needs" "bear" "+")
int5
The rabbit does not need the bear.
Unknown
inv-rconc
[@1: The rabbit needs the bear.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("rabbit" "needs" "bear" "-")
The rabbit is nice.
Unknown
rconc
[@2: The rabbit is nice.[CWA. Example of deepest failure = (rule2 <- rule9 <- FAIL)]]
("rabbit" "is" "nice" "+")
The rabbit is not red.
Unknown
inv-rconc
[@3: The rabbit is red.[CWA. Example of deepest failure = (rule4 <- rule2 <- rule9 <- FAIL)]]
("rabbit" "is" "red" "-")
The mouse needs the bear.
Unknown
rconc
[@1: The mouse needs the bear.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("mouse" "needs" "bear" "+")
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 bear visits the rabbit.
Unknown
random
[@0: The bear visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "rabbit" "+")
The rabbit is not green.
Unknown
inv-random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "-")
The rabbit visits the mouse.
Unknown
random
[@0: The rabbit visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "mouse" "+")
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The rabbit sees the bear.
Unknown
random
[@0: The rabbit sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "bear" "+")
The rabbit is not round.
Unknown
inv-random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "-")
The mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
@0: The bear needs the cat.[(triple1)] The bear needs the mouse.[(triple2)] The bear visits the mouse.[(triple3)] The cat needs the rabbit.[(triple4)] The cat visits the mouse.[(triple5)] The cat visits the rabbit.[(triple6)] The mouse needs the cat.[(triple7)] The mouse sees the bear.[(triple8)] The rabbit does not see the cat.[(triple10)] The rabbit is rough.[(triple9)] The rabbit sees the mouse.[(triple11)] The rabbit visits the bear.[(triple12)] @1: The bear needs the bear.[(((triple3) -> rule9))] The cat needs the bear.[(((triple5) -> rule9))] @2: The bear is nice.[(((((triple3) -> rule9)) -> rule2))] The cat is nice.[(((((triple5) -> rule9)) -> rule2))] @3: The bear is red.[(((((((triple3) -> rule9)) -> rule2)) -> rule4))] The cat is red.[(((((((triple5) -> rule9)) -> rule2)) -> rule4))] @4: The mouse is nice.[(((triple3 ((((((triple3) -> rule9)) -> rule2)) -> rule4)) -> rule7) OR ((triple5 ((((((triple5) -> rule9)) -> rule2)) -> rule4)) -> rule7))] @5: The mouse is red.[(((((triple3 ((((((triple3) -> rule9)) -> rule2)) -> rule4)) -> rule7)) -> rule4) OR ((((triple5 ((((((triple5) -> rule9)) -> rule2)) -> rule4)) -> rule7)) -> rule4))]
The bear needs the cat.
("bear" "needs" "cat" "+")
triple1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple2
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple3
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple4
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple5
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple6
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple7
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple8
The rabbit does not see the cat.
("rabbit" "sees" "cat" "-")
triple10
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple9
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple11
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
triple12
The bear needs the bear.
("bear" "needs" "bear" "+")
((triple3) -> (rule9 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The cat needs the bear.
("cat" "needs" "bear" "+")
((triple5) -> (rule9 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
((((triple3) -> (rule9 % int2))) -> (rule2 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
((((triple5) -> (rule9 % int2))) -> (rule2 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat needs the bear.
("cat" "needs" "bear" "+")
int2
The bear is red.
("bear" "is" "red" "+")
((((((triple3) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear needs the bear.
("bear" "needs" "bear" "+")
int3
The cat is red.
("cat" "is" "red" "+")
((((((triple5) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat needs the bear.
("cat" "needs" "bear" "+")
int3
The mouse is nice.
("mouse" "is" "nice" "+")
((triple3 ((((((triple3) -> (rule9 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The bear needs the bear.
("bear" "needs" "bear" "+")
int4
((triple5 ((((((triple5) -> (rule9 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The cat needs the bear.
("cat" "needs" "bear" "+")
int4
The mouse is red.
("mouse" "is" "red" "+")
((((triple3 ((((((triple3) -> (rule9 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The bear is nice.
("bear" "is" "nice" "+")
int4
The bear needs the bear.
("bear" "needs" "bear" "+")
int5
((((triple5 ((((((triple5) -> (rule9 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The cat is nice.
("cat" "is" "nice" "+")
int4
The cat needs the bear.
("cat" "needs" "bear" "+")
int5