The bear eats the rabbit. The bear is cold. The bear sees the dog. The bear does not see the squirrel. The dog eats the bear. The rabbit eats the dog. The rabbit needs the dog. The rabbit sees the squirrel. The squirrel eats the dog. The squirrel is green. The squirrel sees the bear. The squirrel sees the dog. If something sees the rabbit then the rabbit sees the bear. If something sees the bear then it sees the rabbit.
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear sees the dog.
("bear" "sees" "dog" "+")
The bear does not see the squirrel.
("bear" "sees" "squirrel" "-")
The dog eats the bear.
("dog" "eats" "bear" "+")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
If something sees the rabbit then the rabbit sees the bear.
((("something" "sees" "rabbit" "+")) -> ("rabbit" "sees" "bear" "+"))
If something sees the bear then it sees the rabbit.
((("something" "sees" "bear" "+")) -> ("something" "sees" "rabbit" "+"))
The bear eats the rabbit.
True
1
proof
[(triple1)]
("bear" "eats" "rabbit" "+")
triple1
The rabbit does not need the dog.
False
1
inv-proof
[(triple7)]
("rabbit" "needs" "dog" "-")
triple7
The squirrel sees the rabbit.
True
2
proof
[(((triple11) -> rule2))]
("squirrel" "sees" "rabbit" "+")
((triple11) -> (rule2 % int1))
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int1
The squirrel does not see the rabbit.
False
2
inv-proof
[(((triple11) -> rule2))]
("squirrel" "sees" "rabbit" "-")
((triple11) -> (rule2 % int1))
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int1
The rabbit sees the bear.
True
3
proof
[(((((triple11) -> rule2)) -> rule1))]
("rabbit" "sees" "bear" "+")
((((triple11) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int1
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int2
The rabbit does not see the bear.
False
3
inv-proof
[(((((triple11) -> rule2)) -> rule1))]
("rabbit" "sees" "bear" "-")
((((triple11) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int1
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int2
The rabbit sees the rabbit.
True
4
proof
[(((((((triple11) -> rule2)) -> rule1)) -> rule2))]
("rabbit" "sees" "rabbit" "+")
((((((triple11) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int2
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int3
The rabbit does not see the rabbit.
False
4
inv-proof
[(((((((triple11) -> rule2)) -> rule1)) -> rule2))]
("rabbit" "sees" "rabbit" "-")
((((((triple11) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int2
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int3
The dog does not see the rabbit.
Unknown
inv-rconc
[@1: The dog sees the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "sees" "rabbit" "-")
The bear sees the rabbit.
Unknown
rconc
[@1: The bear sees the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "sees" "rabbit" "+")
The dog does not eat the rabbit.
Unknown
inv-random
[@0: The dog eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "rabbit" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
The dog is not rough.
Unknown
inv-random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
The bear does not eat the bear.
Unknown
inv-random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "-")
The squirrel is rough.
Unknown
random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "+")
@0: The bear does not see the squirrel.[(triple4)] The bear eats the rabbit.[(triple1)] The bear is cold.[(triple2)] The bear sees the dog.[(triple3)] The dog eats the bear.[(triple5)] The rabbit eats the dog.[(triple6)] The rabbit needs the dog.[(triple7)] The rabbit sees the squirrel.[(triple8)] The squirrel eats the dog.[(triple9)] The squirrel is green.[(triple10)] The squirrel sees the bear.[(triple11)] The squirrel sees the dog.[(triple12)] @1: The squirrel sees the rabbit.[(((triple11) -> rule2))] @2: The rabbit sees the bear.[(((((triple11) -> rule2)) -> rule1))] @3: The rabbit sees the rabbit.[(((((((triple11) -> rule2)) -> rule1)) -> rule2))]
The bear does not see the squirrel.
("bear" "sees" "squirrel" "-")
triple4
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
triple1
The bear is cold.
("bear" "is" "cold" "+")
triple2
The bear sees the dog.
("bear" "sees" "dog" "+")
triple3
The dog eats the bear.
("dog" "eats" "bear" "+")
triple5
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple6
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple7
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple8
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
triple9
The squirrel is green.
("squirrel" "is" "green" "+")
triple10
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple11
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
triple12
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
((triple11) -> (rule2 % int1))
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int1
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
((((triple11) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int1
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int2
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((((((triple11) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int2
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int3