The dog is cold. The dog is green. The dog is kind. The dog is red. The dog is young. The dog likes the rabbit. The dog needs the rabbit. The dog sees the rabbit. The rabbit is cold. The rabbit is kind. The rabbit likes the dog. The rabbit needs the dog. If the rabbit likes the dog then the dog likes the rabbit. If something needs the dog and the dog likes the rabbit then it is red. Red things are young.
The dog is cold.
("dog" "is" "cold" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is young.
("dog" "is" "young" "+")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
If the rabbit likes the dog then the dog likes the rabbit.
((("rabbit" "likes" "dog" "+")) -> ("dog" "likes" "rabbit" "+"))
If something needs the dog and the dog likes the rabbit then it is red.
((("something" "needs" "dog" "+") ("dog" "likes" "rabbit" "+")) -> ("something" "is" "red" "+"))
Red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
The dog is kind.
True
1
proof
[(triple3)]
("dog" "is" "kind" "+")
triple3
The rabbit does not need the dog.
False
1
inv-proof
[(triple12)]
("rabbit" "needs" "dog" "-")
triple12
The rabbit is red.
True
3
proof
[(((triple12 triple6) -> rule2) OR ((triple12 ((triple11) -> rule1)) -> rule2))]
("rabbit" "is" "red" "+")
((triple12 triple6) -> (rule2 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
((triple12 ((triple11) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int2
The rabbit is not red.
False
3
inv-proof
[(((triple12 triple6) -> rule2) OR ((triple12 ((triple11) -> rule1)) -> rule2))]
("rabbit" "is" "red" "-")
((triple12 triple6) -> (rule2 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
((triple12 ((triple11) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int2
The rabbit is young.
True
4
proof
[(((((triple12 triple6) -> rule2)) -> rule3) OR ((((triple12 ((triple11) -> rule1)) -> rule2)) -> rule3))]
("rabbit" "is" "young" "+")
((((triple12 triple6) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
((((triple12 ((triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int3
The rabbit is not young.
False
4
inv-proof
[(((((triple12 triple6) -> rule2)) -> rule3) OR ((((triple12 ((triple11) -> rule1)) -> rule2)) -> rule3))]
("rabbit" "is" "young" "-")
((((triple12 triple6) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
((((triple12 ((triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int3
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The rabbit is green.
Unknown
random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "+")
The rabbit does not see the dog.
Unknown
inv-random
[@0: The rabbit sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "dog" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
@0: The dog is cold.[(triple1)] The dog is green.[(triple2)] The dog is kind.[(triple3)] The dog is red.[(triple4)] The dog is young.[(triple5 OR ((triple4) -> rule3))] The dog likes the rabbit.[(triple6 OR ((triple11) -> rule1))] The dog needs the rabbit.[(triple7)] The dog sees the rabbit.[(triple8)] The rabbit is cold.[(triple9)] The rabbit is kind.[(triple10)] The rabbit likes the dog.[(triple11)] The rabbit needs the dog.[(triple12)] @1: The rabbit is red.[(((triple12 triple6) -> rule2) OR ((triple12 ((triple11) -> rule1)) -> rule2))] @2: The rabbit is young.[(((((triple12 triple6) -> rule2)) -> rule3) OR ((((triple12 ((triple11) -> rule1)) -> rule2)) -> rule3))]
The dog is cold.
("dog" "is" "cold" "+")
triple1
The dog is green.
("dog" "is" "green" "+")
triple2
The dog is kind.
("dog" "is" "kind" "+")
triple3
The dog is red.
("dog" "is" "red" "+")
triple4
The dog is young.
("dog" "is" "young" "+")
triple5
((triple4) -> (rule3 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple6
((triple11) -> (rule1 % int1))
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int1
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple7
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple8
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple9
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple10
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple11
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple12
The rabbit is red.
("rabbit" "is" "red" "+")
((triple12 triple6) -> (rule2 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
((triple12 ((triple11) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
((((triple12 triple6) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
((((triple12 ((triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int3