The dog chases the rabbit. The dog eats the rabbit. The dog is big. The dog is nice. The dog is round. The dog sees the rabbit. The rabbit chases the dog. The rabbit eats the dog. The rabbit is kind. The rabbit is nice. The rabbit is red. The rabbit sees the dog. If someone is big then they chase the dog. If someone chases the dog and the dog sees the rabbit then they are kind. If someone is red and they see the rabbit then the rabbit sees the dog. If the dog is red then the dog eats the rabbit. If someone is kind and they see the rabbit then they are red. If the rabbit sees the dog then the dog chases the rabbit.
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog is round.
("dog" "is" "round" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
If someone is big then they chase the dog.
((("someone" "is" "big" "+")) -> ("someone" "chases" "dog" "+"))
If someone chases the dog and the dog sees the rabbit then they are kind.
((("someone" "chases" "dog" "+") ("dog" "sees" "rabbit" "+")) -> ("someone" "is" "kind" "+"))
If someone is red and they see the rabbit then the rabbit sees the dog.
((("someone" "is" "red" "+") ("someone" "sees" "rabbit" "+")) -> ("rabbit" "sees" "dog" "+"))
If the dog is red then the dog eats the rabbit.
((("dog" "is" "red" "+")) -> ("dog" "eats" "rabbit" "+"))
If someone is kind and they see the rabbit then they are red.
((("someone" "is" "kind" "+") ("someone" "sees" "rabbit" "+")) -> ("someone" "is" "red" "+"))
If the rabbit sees the dog then the dog chases the rabbit.
((("rabbit" "sees" "dog" "+")) -> ("dog" "chases" "rabbit" "+"))
The dog sees the rabbit.
True
1
proof
[(triple6)]
("dog" "sees" "rabbit" "+")
triple6
The rabbit does not eat the dog.
False
1
inv-proof
[(triple8)]
("rabbit" "eats" "dog" "-")
triple8
The dog chases the dog.
True
2
proof
[(((triple3) -> rule1))]
("dog" "chases" "dog" "+")
((triple3) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog does not chase the dog.
False
2
inv-proof
[(((triple3) -> rule1))]
("dog" "chases" "dog" "-")
((triple3) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog is kind.
True
4
proof
[(((((triple3) -> rule1) triple6) -> rule2))]
("dog" "is" "kind" "+")
((((triple3) -> (rule1 % int2)) triple6) -> (rule2 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog is not kind.
False
4
inv-proof
[(((((triple3) -> rule1) triple6) -> rule2))]
("dog" "is" "kind" "-")
((((triple3) -> (rule1 % int2)) triple6) -> (rule2 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog is red.
True
6
proof
[(((((((triple3) -> rule1) triple6) -> rule2) triple6) -> rule5))]
("dog" "is" "red" "+")
((((((triple3) -> (rule1 % int3)) triple6) -> (rule2 % int2)) triple6) -> (rule5 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The dog chases the dog.
("dog" "chases" "dog" "+")
int3
The dog is not red.
False
6
inv-proof
[(((((((triple3) -> rule1) triple6) -> rule2) triple6) -> rule5))]
("dog" "is" "red" "-")
((((((triple3) -> (rule1 % int3)) triple6) -> (rule2 % int2)) triple6) -> (rule5 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The dog chases the dog.
("dog" "chases" "dog" "+")
int3
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The rabbit eats the rabbit.
Unknown
random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "+")
The rabbit does not chase the rabbit.
Unknown
inv-random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
The rabbit is not round.
Unknown
inv-random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
@0: The dog chases the rabbit.[(triple1 OR ((triple12) -> rule6) OR ((((((((((triple3) -> rule1) triple6) -> rule2) triple6) -> rule5) triple6) -> rule3)) -> rule6))] The dog eats the rabbit.[(triple2 OR ((((((((triple3) -> rule1) triple6) -> rule2) triple6) -> rule5)) -> rule4))] The dog is big.[(triple3)] The dog is nice.[(triple4)] The dog is round.[(triple5)] The dog sees the rabbit.[(triple6)] The rabbit chases the dog.[(triple7)] The rabbit eats the dog.[(triple8)] The rabbit is kind.[(triple9 OR ((triple7 triple6) -> rule2))] The rabbit is nice.[(triple10)] The rabbit is red.[(triple11)] The rabbit sees the dog.[(triple12 OR ((((((((triple3) -> rule1) triple6) -> rule2) triple6) -> rule5) triple6) -> rule3))] @1: The dog chases the dog.[(((triple3) -> rule1))] @2: The dog is kind.[(((((triple3) -> rule1) triple6) -> rule2))] @3: The dog is red.[(((((((triple3) -> rule1) triple6) -> rule2) triple6) -> rule5))]
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
triple1
((triple12) -> (rule6 % int1))
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int1
((((((((((triple3) -> (rule1 % int5)) triple6) -> (rule2 % int4)) triple6) -> (rule5 % int3)) triple6) -> (rule3 % int2))) -> (rule6 % int1))
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int2
The dog is red.
("dog" "is" "red" "+")
int3
The dog is kind.
("dog" "is" "kind" "+")
int4
The dog chases the dog.
("dog" "chases" "dog" "+")
int5
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
triple2
((((((((triple3) -> (rule1 % int4)) triple6) -> (rule2 % int3)) triple6) -> (rule5 % int2))) -> (rule4 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
int3
The dog chases the dog.
("dog" "chases" "dog" "+")
int4
The dog is big.
("dog" "is" "big" "+")
triple3
The dog is nice.
("dog" "is" "nice" "+")
triple4
The dog is round.
("dog" "is" "round" "+")
triple5
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple6
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
triple7
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple8
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple9
((triple7 triple6) -> (rule2 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple10
The rabbit is red.
("rabbit" "is" "red" "+")
triple11
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple12
((((((((triple3) -> (rule1 % int4)) triple6) -> (rule2 % int3)) triple6) -> (rule5 % int2)) triple6) -> (rule3 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
int3
The dog chases the dog.
("dog" "chases" "dog" "+")
int4
The dog chases the dog.
("dog" "chases" "dog" "+")
((triple3) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
((((triple3) -> (rule1 % int2)) triple6) -> (rule2 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog is red.
("dog" "is" "red" "+")
((((((triple3) -> (rule1 % int3)) triple6) -> (rule2 % int2)) triple6) -> (rule5 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The dog chases the dog.
("dog" "chases" "dog" "+")
int3