The dog sees the rabbit. The rabbit sees the dog. The squirrel is kind. If someone sees the rabbit and the rabbit sees the dog then the dog is round. If someone visits the squirrel and the squirrel chases the dog then they see the dog. If the dog is round then the dog is nice. If someone is big and they see the dog then the dog is kind. If someone chases the squirrel then they see the rabbit. If someone is nice then they chase the dog. Nice people are kind. If someone visits the squirrel and they are nice then the squirrel is young.
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
If someone sees the rabbit and the rabbit sees the dog then the dog is round.
((("someone" "sees" "rabbit" "+") ("rabbit" "sees" "dog" "+")) -> ("dog" "is" "round" "+"))
If someone visits the squirrel and the squirrel chases the dog then they see the dog.
((("someone" "visits" "squirrel" "+") ("squirrel" "chases" "dog" "+")) -> ("someone" "sees" "dog" "+"))
If the dog is round then the dog is nice.
((("dog" "is" "round" "+")) -> ("dog" "is" "nice" "+"))
If someone is big and they see the dog then the dog is kind.
((("someone" "is" "big" "+") ("someone" "sees" "dog" "+")) -> ("dog" "is" "kind" "+"))
If someone chases the squirrel then they see the rabbit.
((("someone" "chases" "squirrel" "+")) -> ("someone" "sees" "rabbit" "+"))
If someone is nice then they chase the dog.
((("someone" "is" "nice" "+")) -> ("someone" "chases" "dog" "+"))
Nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If someone visits the squirrel and they are nice then the squirrel is young.
((("someone" "visits" "squirrel" "+") ("someone" "is" "nice" "+")) -> ("squirrel" "is" "young" "+"))
The squirrel is kind.
True
1
proof
[(triple3)]
("squirrel" "is" "kind" "+")
triple3
The rabbit does not see the dog.
False
1
inv-proof
[(triple2)]
("rabbit" "sees" "dog" "-")
triple2
The dog is round.
True
3
proof
[(((triple1 triple2) -> rule1))]
("dog" "is" "round" "+")
((triple1 triple2) -> (rule1 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is not round.
False
3
inv-proof
[(((triple1 triple2) -> rule1))]
("dog" "is" "round" "-")
((triple1 triple2) -> (rule1 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is nice.
True
4
proof
[(((((triple1 triple2) -> rule1)) -> rule3))]
("dog" "is" "nice" "+")
((((triple1 triple2) -> (rule1 % int2))) -> (rule3 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog is not nice.
False
4
inv-proof
[(((((triple1 triple2) -> rule1)) -> rule3))]
("dog" "is" "nice" "-")
((((triple1 triple2) -> (rule1 % int2))) -> (rule3 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog chases the dog.
True
5
proof
[(((((((triple1 triple2) -> rule1)) -> rule3)) -> rule6))]
("dog" "chases" "dog" "+")
((((((triple1 triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2
The dog is round.
("dog" "is" "round" "+")
int3
The dog is not kind.
False
5
inv-proof
[(((((((triple1 triple2) -> rule1)) -> rule3)) -> rule7))]
("dog" "is" "kind" "-")
((((((triple1 triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2
The dog is round.
("dog" "is" "round" "+")
int3
The rabbit is not kind.
Unknown
inv-rconc
[@1: The rabbit is kind.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "is" "kind" "-")
The squirrel sees the rabbit.
Unknown
rconc
[@1: The squirrel sees the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "sees" "rabbit" "+")
The squirrel does not see the dog.
Unknown
inv-rconc
[@1: The squirrel sees the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "sees" "dog" "-")
The rabbit sees the rabbit.
Unknown
rconc
[@1: The rabbit sees the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "sees" "rabbit" "+")
The squirrel does not see the squirrel.
Unknown
inv-random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
The rabbit does not visit the squirrel.
Unknown
inv-random
[@0: The rabbit visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "squirrel" "-")
The dog visits the rabbit.
Unknown
random
[@0: The dog visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "rabbit" "+")
@0: The dog sees the rabbit.[(triple1)] The rabbit sees the dog.[(triple2)] The squirrel is kind.[(triple3)] @1: The dog is round.[(((triple1 triple2) -> rule1))] @2: The dog is nice.[(((((triple1 triple2) -> rule1)) -> rule3))] @3: The dog chases the dog.[(((((((triple1 triple2) -> rule1)) -> rule3)) -> rule6))] The dog is kind.[(((((((triple1 triple2) -> rule1)) -> rule3)) -> rule7))]
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple2
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple3
The dog is round.
("dog" "is" "round" "+")
((triple1 triple2) -> (rule1 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
((((triple1 triple2) -> (rule1 % int2))) -> (rule3 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog chases the dog.
("dog" "chases" "dog" "+")
((((((triple1 triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2
The dog is round.
("dog" "is" "round" "+")
int3
The dog is kind.
("dog" "is" "kind" "+")
((((((triple1 triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2
The dog is round.
("dog" "is" "round" "+")
int3