The dog likes the squirrel. The squirrel likes the dog. If the dog is big then the dog likes the squirrel. If the dog eats the squirrel and the dog is not green then the squirrel likes the dog. If someone likes the squirrel and they are not young then they like the dog. If someone sees the squirrel then the squirrel sees the dog. If the squirrel likes the dog then the dog sees the squirrel. If someone sees the dog then they are kind.
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
If the dog is big then the dog likes the squirrel.
((("dog" "is" "big" "+")) -> ("dog" "likes" "squirrel" "+"))
If the dog eats the squirrel and the dog is not green then the squirrel likes the dog.
((("dog" "eats" "squirrel" "+") ("dog" "is" "green" "~")) -> ("squirrel" "likes" "dog" "+"))
If someone likes the squirrel and they are not young then they like the dog.
((("someone" "likes" "squirrel" "+") ("someone" "is" "young" "~")) -> ("someone" "likes" "dog" "+"))
If someone sees the squirrel then the squirrel sees the dog.
((("someone" "sees" "squirrel" "+")) -> ("squirrel" "sees" "dog" "+"))
If the squirrel likes the dog then the dog sees the squirrel.
((("squirrel" "likes" "dog" "+")) -> ("dog" "sees" "squirrel" "+"))
If someone sees the dog then they are kind.
((("someone" "sees" "dog" "+")) -> ("someone" "is" "kind" "+"))
The squirrel likes the dog.
True
1
proof
[(triple2)]
("squirrel" "likes" "dog" "+")
triple2
The dog does not like the squirrel.
False
1
inv-proof
[(triple1)]
("dog" "likes" "squirrel" "-")
triple1
The dog sees the squirrel.
True
2
proof
[(((triple2) -> rule5))]
("dog" "sees" "squirrel" "+")
((triple2) -> (rule5 % int1))
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int1
The dog does not see the squirrel.
False
2
inv-proof
[(((triple2) -> rule5))]
("dog" "sees" "squirrel" "-")
((triple2) -> (rule5 % int1))
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int1
The squirrel sees the dog.
True
3
proof
[(((((triple2) -> rule5)) -> rule4))]
("squirrel" "sees" "dog" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int1
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int2
The squirrel does not see the dog.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule4))]
("squirrel" "sees" "dog" "-")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int1
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int2
The squirrel is kind.
True
4
proof
[(((((((triple2) -> rule5)) -> rule4)) -> rule6))]
("squirrel" "is" "kind" "+")
((((((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int2
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int3
The squirrel is not kind.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule4)) -> rule6))]
("squirrel" "is" "kind" "-")
((((((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int2
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int3
The dog is not kind.
Unknown
inv-rconc
[@1: The dog is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "is" "kind" "-")
The dog likes the dog.
Unknown
rconc
[@1: The dog likes the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "likes" "dog" "+")
The squirrel is not green.
Unknown
inv-random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "-")
The squirrel is red.
Unknown
random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "+")
The dog is not green.
Unknown
inv-random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
The squirrel is not big.
Unknown
inv-random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "-")
The dog is big.
Unknown
random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "+")
@0: The dog likes the squirrel.[(triple1)] The squirrel likes the dog.[(triple2)] @1: The dog sees the squirrel.[(((triple2) -> rule5))] @2: The squirrel sees the dog.[(((((triple2) -> rule5)) -> rule4))] @3: The squirrel is kind.[(((((((triple2) -> rule5)) -> rule4)) -> rule6))]
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
triple1
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
triple2
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
((triple2) -> (rule5 % int1))
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int1
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int1
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int2
The squirrel is kind.
("squirrel" "is" "kind" "+")
((((((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int2
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int3