The dog chases the rabbit. The dog is rough. The dog needs the rabbit. The rabbit chases the dog. The rabbit is cold. The rabbit is green. The rabbit is red. The rabbit is rough. The rabbit needs the dog. The rabbit sees the dog. If the rabbit sees the dog and the rabbit is rough then the rabbit is cold. If someone needs the dog then the dog is rough. If someone sees the rabbit and the rabbit is round then they are red. If someone needs the rabbit then the rabbit is red. If someone is red then they are round. If someone needs the dog then the dog sees the rabbit.
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
If the rabbit sees the dog and the rabbit is rough then the rabbit is cold.
((("rabbit" "sees" "dog" "+") ("rabbit" "is" "rough" "+")) -> ("rabbit" "is" "cold" "+"))
If someone needs the dog then the dog is rough.
((("someone" "needs" "dog" "+")) -> ("dog" "is" "rough" "+"))
If someone sees the rabbit and the rabbit is round then they are red.
((("someone" "sees" "rabbit" "+") ("rabbit" "is" "round" "+")) -> ("someone" "is" "red" "+"))
If someone needs the rabbit then the rabbit is red.
((("someone" "needs" "rabbit" "+")) -> ("rabbit" "is" "red" "+"))
If someone is red then they are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If someone needs the dog then the dog sees the rabbit.
((("someone" "needs" "dog" "+")) -> ("dog" "sees" "rabbit" "+"))
The rabbit is red.
True
1
proof
[(triple7 OR ((triple3) -> rule4))]
("rabbit" "is" "red" "+")
triple7
((triple3) -> (rule4 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit does not need the dog.
False
1
inv-proof
[(triple9)]
("rabbit" "needs" "dog" "-")
triple9
The dog sees the rabbit.
True
2
proof
[(((triple9) -> rule6))]
("dog" "sees" "rabbit" "+")
((triple9) -> (rule6 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The rabbit is not round.
False
2
inv-proof
[(((triple7) -> rule5) OR ((((triple3) -> rule4)) -> rule5))]
("rabbit" "is" "round" "-")
((triple7) -> (rule5 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The dog is red.
True
5
proof
[(((((triple9) -> rule6) ((triple7) -> rule5)) -> rule3) OR ((((triple9) -> rule6) ((((triple3) -> rule4)) -> rule5)) -> rule3))]
("dog" "is" "red" "+")
((((triple9) -> (rule6 % int3)) ((triple7) -> (rule5 % int2))) -> (rule3 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int3
((((triple9) -> (rule6 % int4)) ((((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int4
The dog is not red.
False
5
inv-proof
[(((((triple9) -> rule6) ((triple7) -> rule5)) -> rule3) OR ((((triple9) -> rule6) ((((triple3) -> rule4)) -> rule5)) -> rule3))]
("dog" "is" "red" "-")
((((triple9) -> (rule6 % int3)) ((triple7) -> (rule5 % int2))) -> (rule3 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int3
((((triple9) -> (rule6 % int4)) ((((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int4
The dog is round.
True
6
proof
[(((((((triple9) -> rule6) ((triple7) -> rule5)) -> rule3)) -> rule5) OR ((((((triple9) -> rule6) ((((triple3) -> rule4)) -> rule5)) -> rule3)) -> rule5))]
("dog" "is" "round" "+")
((((((triple9) -> (rule6 % int4)) ((triple7) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int4
((((((triple9) -> (rule6 % int5)) ((((triple3) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The rabbit is red.
("rabbit" "is" "red" "+")
int4
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int5
The dog is not round.
False
6
inv-proof
[(((((((triple9) -> rule6) ((triple7) -> rule5)) -> rule3)) -> rule5) OR ((((((triple9) -> rule6) ((((triple3) -> rule4)) -> rule5)) -> rule3)) -> rule5))]
("dog" "is" "round" "-")
((((((triple9) -> (rule6 % int4)) ((triple7) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int4
((((((triple9) -> (rule6 % int5)) ((((triple3) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The rabbit is red.
("rabbit" "is" "red" "+")
int4
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int5
The dog is not green.
Unknown
inv-random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "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 dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The dog is cold.
Unknown
random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "+")
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 chases the rabbit.[(triple1)] The dog is rough.[(triple2 OR ((triple9) -> rule2))] The dog needs the rabbit.[(triple3)] The rabbit chases the dog.[(triple4)] The rabbit is cold.[(triple5 OR ((triple10 triple8) -> rule1))] The rabbit is green.[(triple6)] The rabbit is red.[(triple7 OR ((triple3) -> rule4))] The rabbit is rough.[(triple8)] The rabbit needs the dog.[(triple9)] The rabbit sees the dog.[(triple10)] @1: The dog sees the rabbit.[(((triple9) -> rule6))] The rabbit is round.[(((triple7) -> rule5) OR ((((triple3) -> rule4)) -> rule5))] @2: The dog is red.[(((((triple9) -> rule6) ((triple7) -> rule5)) -> rule3) OR ((((triple9) -> rule6) ((((triple3) -> rule4)) -> rule5)) -> rule3))] @3: The dog is round.[(((((((triple9) -> rule6) ((triple7) -> rule5)) -> rule3)) -> rule5) OR ((((((triple9) -> rule6) ((((triple3) -> rule4)) -> rule5)) -> rule3)) -> rule5))]
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
triple1
The dog is rough.
("dog" "is" "rough" "+")
triple2
((triple9) -> (rule2 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple3
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
triple4
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple5
((triple10 triple8) -> (rule1 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
triple6
The rabbit is red.
("rabbit" "is" "red" "+")
triple7
((triple3) -> (rule4 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple8
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple9
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple10
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
((triple9) -> (rule6 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
((triple7) -> (rule5 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The dog is red.
("dog" "is" "red" "+")
((((triple9) -> (rule6 % int3)) ((triple7) -> (rule5 % int2))) -> (rule3 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int3
((((triple9) -> (rule6 % int4)) ((((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int4
The dog is round.
("dog" "is" "round" "+")
((((((triple9) -> (rule6 % int4)) ((triple7) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int4
((((((triple9) -> (rule6 % int5)) ((((triple3) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The rabbit is red.
("rabbit" "is" "red" "+")
int4
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int5