The dog chases the rabbit. The dog is red. The dog is rough. The dog is young. The dog needs the rabbit. The dog sees the rabbit. The rabbit chases the dog. The rabbit is red. The rabbit is round. The rabbit is young. The rabbit needs the dog. The rabbit sees the dog. If someone chases the dog then they chase the rabbit. If someone needs the rabbit then the rabbit sees the dog. If someone chases the dog and they chase the rabbit then the rabbit is rough.
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog is young.
("dog" "is" "young" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
If someone chases the dog then they chase the rabbit.
((("someone" "chases" "dog" "+")) -> ("someone" "chases" "rabbit" "+"))
If someone needs the rabbit then the rabbit sees the dog.
((("someone" "needs" "rabbit" "+")) -> ("rabbit" "sees" "dog" "+"))
If someone chases the dog and they chase the rabbit then the rabbit is rough.
((("someone" "chases" "dog" "+") ("someone" "chases" "rabbit" "+")) -> ("rabbit" "is" "rough" "+"))
The rabbit is round.
True
1
proof
[(triple9)]
("rabbit" "is" "round" "+")
triple9
The dog does not chase the rabbit.
False
1
inv-proof
[(triple1)]
("dog" "chases" "rabbit" "-")
triple1
The rabbit chases the rabbit.
True
2
proof
[(((triple7) -> rule1))]
("rabbit" "chases" "rabbit" "+")
((triple7) -> (rule1 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit does not chase the rabbit.
False
2
inv-proof
[(((triple7) -> rule1))]
("rabbit" "chases" "rabbit" "-")
((triple7) -> (rule1 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is rough.
True
4
proof
[(((triple7 ((triple7) -> rule1)) -> rule3))]
("rabbit" "is" "rough" "+")
((triple7 ((triple7) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The rabbit is not rough.
False
4
inv-proof
[(((triple7 ((triple7) -> rule1)) -> rule3))]
("rabbit" "is" "rough" "-")
((triple7 ((triple7) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The rabbit is not nice.
Unknown
inv-random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
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 dog is round.
Unknown
random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "+")
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 chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
@0: The dog chases the rabbit.[(triple1)] The dog is red.[(triple2)] The dog is rough.[(triple3)] The dog is young.[(triple4)] The dog needs the rabbit.[(triple5)] The dog sees the rabbit.[(triple6)] The rabbit chases the dog.[(triple7)] The rabbit is red.[(triple8)] The rabbit is round.[(triple9)] The rabbit is young.[(triple10)] The rabbit needs the dog.[(triple11)] The rabbit sees the dog.[(triple12 OR ((triple5) -> rule2))] @1: The rabbit chases the rabbit.[(((triple7) -> rule1))] @2: The rabbit is rough.[(((triple7 ((triple7) -> rule1)) -> rule3))]
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
triple1
The dog is red.
("dog" "is" "red" "+")
triple2
The dog is rough.
("dog" "is" "rough" "+")
triple3
The dog is young.
("dog" "is" "young" "+")
triple4
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple5
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple6
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
triple7
The rabbit is red.
("rabbit" "is" "red" "+")
triple8
The rabbit is round.
("rabbit" "is" "round" "+")
triple9
The rabbit is young.
("rabbit" "is" "young" "+")
triple10
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple11
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple12
((triple5) -> (rule2 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((triple7) -> (rule1 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
((triple7 ((triple7) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2