The bear is blue. The bear needs the mouse. The bear needs the squirrel. The dog chases the bear. The dog is kind. The dog is rough. The mouse is not green. The mouse needs the squirrel. The squirrel is blue. The squirrel is kind. The squirrel needs the bear. The squirrel does not need the dog. If the bear is blue then the bear is not kind. If something chases the mouse then it chases the squirrel. If something chases the squirrel then it chases the dog. If something is green and rough then it chases the dog. If something sees the mouse and the mouse needs the bear then the bear does not see the dog. If something needs the bear then the bear chases the mouse. If something sees the dog and it does not see the mouse then the dog is blue. If something chases the dog and the dog is rough then the dog chases the mouse.
The bear is blue.
("bear" "is" "blue" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
The dog chases the bear.
("dog" "chases" "bear" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is rough.
("dog" "is" "rough" "+")
The mouse is not green.
("mouse" "is" "green" "-")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
The squirrel does not need the dog.
("squirrel" "needs" "dog" "-")
If the bear is blue then the bear is not kind.
((("bear" "is" "blue" "+")) -> ("bear" "is" "kind" "-"))
If something chases the mouse then it chases the squirrel.
((("something" "chases" "mouse" "+")) -> ("something" "chases" "squirrel" "+"))
If something chases the squirrel then it chases the dog.
((("something" "chases" "squirrel" "+")) -> ("something" "chases" "dog" "+"))
If something is green and rough then it chases the dog.
((("something" "is" "green" "+") ("something" "is" "rough" "+")) -> ("something" "chases" "dog" "+"))
If something sees the mouse and the mouse needs the bear then the bear does not see the dog.
((("something" "sees" "mouse" "+") ("mouse" "needs" "bear" "+")) -> ("bear" "sees" "dog" "-"))
If something needs the bear then the bear chases the mouse.
((("something" "needs" "bear" "+")) -> ("bear" "chases" "mouse" "+"))
If something sees the dog and it does not see the mouse then the dog is blue.
((("something" "sees" "dog" "+") ("something" "sees" "mouse" "~")) -> ("dog" "is" "blue" "+"))
If something chases the dog and the dog is rough then the dog chases the mouse.
((("something" "chases" "dog" "+") ("dog" "is" "rough" "+")) -> ("dog" "chases" "mouse" "+"))
The dog is rough.
True
1
proof
[(triple6)]
("dog" "is" "rough" "+")
triple6
The mouse does not need the squirrel.
False
1
inv-proof
[(triple8)]
("mouse" "needs" "squirrel" "-")
triple8
The bear is not kind.
True
2
proof
[(((triple1) -> rule1))]
("bear" "is" "kind" "-")
((triple1) -> (rule1 % int1))
The bear is not kind.
("bear" "is" "kind" "-")
int1
The bear is kind.
False
2
inv-proof
[(((triple1) -> rule1))]
("bear" "is" "kind" "+")
((triple1) -> (rule1 % int1))
The bear is not kind.
("bear" "is" "kind" "-")
int1
The bear chases the squirrel.
True
3
proof
[(((((triple11) -> rule6)) -> rule2))]
("bear" "chases" "squirrel" "+")
((((triple11) -> (rule6 % int2))) -> (rule2 % int1))
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
The bear does not chase the squirrel.
False
3
inv-proof
[(((((triple11) -> rule6)) -> rule2))]
("bear" "chases" "squirrel" "-")
((((triple11) -> (rule6 % int2))) -> (rule2 % int1))
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
The bear chases the dog.
True
4
proof
[(((((((triple11) -> rule6)) -> rule2)) -> rule3))]
("bear" "chases" "dog" "+")
((((((triple11) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The bear chases the dog.
("bear" "chases" "dog" "+")
int1
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int2
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int3
The bear does not chase the dog.
False
4
inv-proof
[(((((((triple11) -> rule6)) -> rule2)) -> rule3))]
("bear" "chases" "dog" "-")
((((((triple11) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The bear chases the dog.
("bear" "chases" "dog" "+")
int1
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int2
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int3
The dog chases the mouse.
True
6
proof
[(((((((((triple11) -> rule6)) -> rule2)) -> rule3) triple6) -> rule8))]
("dog" "chases" "mouse" "+")
((((((((triple11) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule3 % int2)) triple6) -> (rule8 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The bear chases the dog.
("bear" "chases" "dog" "+")
int2
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int3
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int4
The dog does not chase the mouse.
False
6
inv-proof
[(((((((((triple11) -> rule6)) -> rule2)) -> rule3) triple6) -> rule8))]
("dog" "chases" "mouse" "-")
((((((((triple11) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule3 % int2)) triple6) -> (rule8 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The bear chases the dog.
("bear" "chases" "dog" "+")
int2
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int3
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int4
The dog chases the squirrel.
True
7
proof
[(((((((((((triple11) -> rule6)) -> rule2)) -> rule3) triple6) -> rule8)) -> rule2))]
("dog" "chases" "squirrel" "+")
((((((((((triple11) -> (rule6 % int5))) -> (rule2 % int4))) -> (rule3 % int3)) triple6) -> (rule8 % int2))) -> (rule2 % int1))
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int1
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int2
The bear chases the dog.
("bear" "chases" "dog" "+")
int3
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int4
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int5
The dog does not chase the squirrel.
False
7
inv-proof
[(((((((((((triple11) -> rule6)) -> rule2)) -> rule3) triple6) -> rule8)) -> rule2))]
("dog" "chases" "squirrel" "-")
((((((((((triple11) -> (rule6 % int5))) -> (rule2 % int4))) -> (rule3 % int3)) triple6) -> (rule8 % int2))) -> (rule2 % int1))
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int1
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int2
The bear chases the dog.
("bear" "chases" "dog" "+")
int3
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int4
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int5
The mouse does not chase the squirrel.
Unknown
inv-rconc
[@1: The mouse chases the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "chases" "squirrel" "-")
The dog is blue.
Unknown
rconc
[@1: The dog is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "is" "blue" "+")
The squirrel does not chase the dog.
Unknown
inv-rconc
[@2: The squirrel chases the dog.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("squirrel" "chases" "dog" "-")
The mouse chases the dog.
Unknown
rconc
[@2: The mouse chases the dog.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("mouse" "chases" "dog" "+")
The squirrel does not chase the squirrel.
Unknown
inv-rconc
[@1: The squirrel chases the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "chases" "squirrel" "-")
The squirrel chases the bear.
Unknown
random
[@0: The squirrel chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "bear" "+")
The mouse does not need the bear.
Unknown
inv-random
[@0: The mouse needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "bear" "-")
The bear sees the squirrel.
Unknown
random
[@0: The bear sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "squirrel" "+")
The bear does not need the dog.
Unknown
inv-random
[@0: The bear needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "dog" "-")
The squirrel needs the mouse.
Unknown
random
[@0: The squirrel needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "mouse" "+")
The squirrel does not need the squirrel.
Unknown
inv-random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
@0: The bear is blue.[(triple1)] The bear needs the mouse.[(triple2)] The bear needs the squirrel.[(triple3)] The dog chases the bear.[(triple4)] The dog is kind.[(triple5)] The dog is rough.[(triple6)] The mouse is not green.[(triple7)] The mouse needs the squirrel.[(triple8)] The squirrel does not need the dog.[(triple12)] The squirrel is blue.[(triple9)] The squirrel is kind.[(triple10)] The squirrel needs the bear.[(triple11)] @1: The bear chases the mouse.[(((triple11) -> rule6))] The bear is not kind.[(((triple1) -> rule1))] @2: The bear chases the squirrel.[(((((triple11) -> rule6)) -> rule2))] @3: The bear chases the dog.[(((((((triple11) -> rule6)) -> rule2)) -> rule3))] @4: The dog chases the mouse.[(((((((((triple11) -> rule6)) -> rule2)) -> rule3) triple6) -> rule8))] @5: The dog chases the squirrel.[(((((((((((triple11) -> rule6)) -> rule2)) -> rule3) triple6) -> rule8)) -> rule2))] @6: The dog chases the dog.[(((((((((((((triple11) -> rule6)) -> rule2)) -> rule3) triple6) -> rule8)) -> rule2)) -> rule3))]
The bear is blue.
("bear" "is" "blue" "+")
triple1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple2
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
triple3
The dog chases the bear.
("dog" "chases" "bear" "+")
triple4
The dog is kind.
("dog" "is" "kind" "+")
triple5
The dog is rough.
("dog" "is" "rough" "+")
triple6
The mouse is not green.
("mouse" "is" "green" "-")
triple7
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple8
The squirrel does not need the dog.
("squirrel" "needs" "dog" "-")
triple12
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple9
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple10
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
triple11
The bear chases the mouse.
("bear" "chases" "mouse" "+")
((triple11) -> (rule6 % int1))
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int1
The bear is not kind.
("bear" "is" "kind" "-")
((triple1) -> (rule1 % int1))
The bear is not kind.
("bear" "is" "kind" "-")
int1
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
((((triple11) -> (rule6 % int2))) -> (rule2 % int1))
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int2
The bear chases the dog.
("bear" "chases" "dog" "+")
((((((triple11) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The bear chases the dog.
("bear" "chases" "dog" "+")
int1
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int2
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int3
The dog chases the mouse.
("dog" "chases" "mouse" "+")
((((((((triple11) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule3 % int2)) triple6) -> (rule8 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The bear chases the dog.
("bear" "chases" "dog" "+")
int2
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int3
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int4
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
((((((((((triple11) -> (rule6 % int5))) -> (rule2 % int4))) -> (rule3 % int3)) triple6) -> (rule8 % int2))) -> (rule2 % int1))
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int1
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int2
The bear chases the dog.
("bear" "chases" "dog" "+")
int3
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int4
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int5
The dog chases the dog.
("dog" "chases" "dog" "+")
((((((((((((triple11) -> (rule6 % int6))) -> (rule2 % int5))) -> (rule3 % int4)) triple6) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int2
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int3
The bear chases the dog.
("bear" "chases" "dog" "+")
int4
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int5
The bear chases the mouse.
("bear" "chases" "mouse" "+")
int6