The bear likes the squirrel. The bear needs the rabbit. The dog likes the squirrel. The rabbit is blue. The rabbit likes the dog. The squirrel likes the bear. The squirrel sees the rabbit. If someone sees the dog then the dog is blue. If someone likes the dog then they need the bear. If someone is blue then they are rough. If someone is rough and they see the squirrel then the squirrel needs the rabbit. If someone likes the squirrel then the squirrel likes the rabbit. If the squirrel is kind and the squirrel likes the bear then the bear sees the squirrel. If someone is rough then they see the dog.
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
If someone sees the dog then the dog is blue.
((("someone" "sees" "dog" "+")) -> ("dog" "is" "blue" "+"))
If someone likes the dog then they need the bear.
((("someone" "likes" "dog" "+")) -> ("someone" "needs" "bear" "+"))
If someone is blue then they are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If someone is rough and they see the squirrel then the squirrel needs the rabbit.
((("someone" "is" "rough" "+") ("someone" "sees" "squirrel" "+")) -> ("squirrel" "needs" "rabbit" "+"))
If someone likes the squirrel then the squirrel likes the rabbit.
((("someone" "likes" "squirrel" "+")) -> ("squirrel" "likes" "rabbit" "+"))
If the squirrel is kind and the squirrel likes the bear then the bear sees the squirrel.
((("squirrel" "is" "kind" "+") ("squirrel" "likes" "bear" "+")) -> ("bear" "sees" "squirrel" "+"))
If someone is rough then they see the dog.
((("someone" "is" "rough" "+")) -> ("someone" "sees" "dog" "+"))
The rabbit is blue.
True
1
proof
[(triple4)]
("rabbit" "is" "blue" "+")
triple4
The rabbit does not like the dog.
False
1
inv-proof
[(triple5)]
("rabbit" "likes" "dog" "-")
triple5
The squirrel likes the rabbit.
True
2
proof
[(((triple1) -> rule5) OR ((triple3) -> rule5))]
("squirrel" "likes" "rabbit" "+")
((triple1) -> (rule5 % int1))
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int1
((triple3) -> (rule5 % int1))
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int1
The rabbit is not rough.
False
2
inv-proof
[(((triple4) -> rule3))]
("rabbit" "is" "rough" "-")
((triple4) -> (rule3 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit sees the dog.
True
3
proof
[(((((triple4) -> rule3)) -> rule7))]
("rabbit" "sees" "dog" "+")
((((triple4) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit does not see the dog.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule7))]
("rabbit" "sees" "dog" "-")
((((triple4) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The dog is blue.
True
4
proof
[(((((((triple4) -> rule3)) -> rule7)) -> rule1))]
("dog" "is" "blue" "+")
((((((triple4) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
int3
The dog is not blue.
False
4
inv-proof
[(((((((triple4) -> rule3)) -> rule7)) -> rule1))]
("dog" "is" "blue" "-")
((((((triple4) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
int3
The dog is rough.
True
5
proof
[(((((((((triple4) -> rule3)) -> rule7)) -> rule1)) -> rule3))]
("dog" "is" "rough" "+")
((((((((triple4) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int3
The rabbit is rough.
("rabbit" "is" "rough" "+")
int4
The dog is not rough.
False
5
inv-proof
[(((((((((triple4) -> rule3)) -> rule7)) -> rule1)) -> rule3))]
("dog" "is" "rough" "-")
((((((((triple4) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int3
The rabbit is rough.
("rabbit" "is" "rough" "+")
int4
The dog sees the dog.
True
6
proof
[(((((((((((triple4) -> rule3)) -> rule7)) -> rule1)) -> rule3)) -> rule7))]
("dog" "sees" "dog" "+")
((((((((((triple4) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int4
The rabbit is rough.
("rabbit" "is" "rough" "+")
int5
The dog does not see the dog.
False
6
inv-proof
[(((((((((((triple4) -> rule3)) -> rule7)) -> rule1)) -> rule3)) -> rule7))]
("dog" "sees" "dog" "-")
((((((((((triple4) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int4
The rabbit is rough.
("rabbit" "is" "rough" "+")
int5
The squirrel does not see the dog.
Unknown
inv-rconc
[@2: The squirrel sees the dog.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("squirrel" "sees" "dog" "-")
The dog needs the bear.
Unknown
rconc
[@1: The dog needs the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "needs" "bear" "+")
The bear does not need the bear.
Unknown
inv-rconc
[@1: The bear needs the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "needs" "bear" "-")
The bear sees the squirrel.
Unknown
rconc
[@1: The bear sees the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "sees" "squirrel" "+")
The squirrel is not rough.
Unknown
inv-rconc
[@1: The squirrel is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "rough" "-")
The bear is rough.
Unknown
rconc
[@1: The bear is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "is" "rough" "+")
The dog does not see the bear.
Unknown
inv-random
[@0: The dog sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "bear" "-")
The rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
The bear is not kind.
Unknown
inv-random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "-")
The squirrel sees the bear.
Unknown
random
[@0: The squirrel sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "bear" "+")
The squirrel does not like the squirrel.
Unknown
inv-random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "-")
The bear is green.
Unknown
random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "+")
@0: The bear likes the squirrel.[(triple1)] The bear needs the rabbit.[(triple2)] The dog likes the squirrel.[(triple3)] The rabbit is blue.[(triple4)] The rabbit likes the dog.[(triple5)] The squirrel likes the bear.[(triple6)] The squirrel sees the rabbit.[(triple7)] @1: The rabbit is rough.[(((triple4) -> rule3))] The rabbit needs the bear.[(((triple5) -> rule2))] The squirrel likes the rabbit.[(((triple1) -> rule5) OR ((triple3) -> rule5))] @2: The rabbit sees the dog.[(((((triple4) -> rule3)) -> rule7))] @3: The dog is blue.[(((((((triple4) -> rule3)) -> rule7)) -> rule1))] @4: The dog is rough.[(((((((((triple4) -> rule3)) -> rule7)) -> rule1)) -> rule3))] @5: The dog sees the dog.[(((((((((((triple4) -> rule3)) -> rule7)) -> rule1)) -> rule3)) -> rule7))]
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
triple1
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
triple2
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
triple3
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple4
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple5
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
triple6
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple7
The rabbit is rough.
("rabbit" "is" "rough" "+")
((triple4) -> (rule3 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
((triple5) -> (rule2 % int1))
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int1
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
((triple1) -> (rule5 % int1))
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int1
((triple3) -> (rule5 % int1))
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
((((triple4) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
((((((triple4) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
int3
The dog is rough.
("dog" "is" "rough" "+")
((((((((triple4) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int3
The rabbit is rough.
("rabbit" "is" "rough" "+")
int4
The dog sees the dog.
("dog" "sees" "dog" "+")
((((((((((triple4) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int4
The rabbit is rough.
("rabbit" "is" "rough" "+")
int5