The bear chases the dog. The bear is round. The bear likes the dog. The bear needs the rabbit. The dog is cold. The dog is nice. The dog likes the bear. The dog likes the rabbit. The rabbit chases the bear. The rabbit chases the dog. The rabbit is blue. The rabbit is cold. The rabbit is rough. The rabbit likes the bear. The rabbit likes the dog. The rabbit needs the bear. If someone is cold then they need the rabbit. If someone needs the rabbit then they chase the dog. If the bear is cold and the bear likes the rabbit then the rabbit chases the bear. If someone likes the bear then the bear is blue. If someone chases the dog then they need the bear. If someone chases the dog and they are cold then they need the bear.
The bear chases the dog.
("bear" "chases" "dog" "+")
The bear is round.
("bear" "is" "round" "+")
The bear likes the dog.
("bear" "likes" "dog" "+")
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog likes the bear.
("dog" "likes" "bear" "+")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
If someone is cold then they need the rabbit.
((("someone" "is" "cold" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone needs the rabbit then they chase the dog.
((("someone" "needs" "rabbit" "+")) -> ("someone" "chases" "dog" "+"))
If the bear is cold and the bear likes the rabbit then the rabbit chases the bear.
((("bear" "is" "cold" "+") ("bear" "likes" "rabbit" "+")) -> ("rabbit" "chases" "bear" "+"))
If someone likes the bear then the bear is blue.
((("someone" "likes" "bear" "+")) -> ("bear" "is" "blue" "+"))
If someone chases the dog then they need the bear.
((("someone" "chases" "dog" "+")) -> ("someone" "needs" "bear" "+"))
If someone chases the dog and they are cold then they need the bear.
((("someone" "chases" "dog" "+") ("someone" "is" "cold" "+")) -> ("someone" "needs" "bear" "+"))
The rabbit chases the dog.
True
1
proof
[(triple10 OR ((((triple12) -> rule1)) -> rule2))]
("rabbit" "chases" "dog" "+")
triple10
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The dog does not like the rabbit.
False
1
inv-proof
[(triple8)]
("dog" "likes" "rabbit" "-")
triple8
The dog needs the rabbit.
True
2
proof
[(((triple5) -> rule1))]
("dog" "needs" "rabbit" "+")
((triple5) -> (rule1 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
The bear does not need the bear.
False
2
inv-proof
[(((triple1) -> rule5) OR ((((triple4) -> rule2)) -> rule5))]
("bear" "needs" "bear" "-")
((triple1) -> (rule5 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear chases the dog.
("bear" "chases" "dog" "+")
int2
The dog chases the dog.
True
3
proof
[(((((triple5) -> rule1)) -> rule2))]
("dog" "chases" "dog" "+")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int2
The dog does not chase the dog.
False
3
inv-proof
[(((((triple5) -> rule1)) -> rule2))]
("dog" "chases" "dog" "-")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int2
The dog needs the bear.
True
4
proof
[(((((((triple5) -> rule1)) -> rule2)) -> rule5) OR ((((((triple5) -> rule1)) -> rule2) triple5) -> rule6))]
("dog" "needs" "bear" "+")
((((((triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int3
((((((triple5) -> (rule1 % int3))) -> (rule2 % int2)) triple5) -> (rule6 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int3
The dog does not need the bear.
False
4
inv-proof
[(((((((triple5) -> rule1)) -> rule2)) -> rule5) OR ((((((triple5) -> rule1)) -> rule2) triple5) -> rule6))]
("dog" "needs" "bear" "-")
((((((triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int3
((((((triple5) -> (rule1 % int3))) -> (rule2 % int2)) triple5) -> (rule6 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int3
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
The bear does not chase the bear.
Unknown
inv-random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "-")
The dog chases the bear.
Unknown
random
[@0: The dog chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "bear" "+")
The bear is not nice.
Unknown
inv-random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "-")
The rabbit is round.
Unknown
random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "+")
The rabbit does not need the dog.
Unknown
inv-random
[@0: The rabbit needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "dog" "-")
The rabbit is nice.
Unknown
random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "+")
@0: The bear chases the dog.[(triple1 OR ((triple4) -> rule2))] The bear is round.[(triple2)] The bear likes the dog.[(triple3)] The bear needs the rabbit.[(triple4)] The dog is cold.[(triple5)] The dog is nice.[(triple6)] The dog likes the bear.[(triple7)] The dog likes the rabbit.[(triple8)] The rabbit chases the bear.[(triple9)] The rabbit chases the dog.[(triple10 OR ((((triple12) -> rule1)) -> rule2))] The rabbit is blue.[(triple11)] The rabbit is cold.[(triple12)] The rabbit is rough.[(triple13)] The rabbit likes the bear.[(triple14)] The rabbit likes the dog.[(triple15)] The rabbit needs the bear.[(triple16 OR ((triple10) -> rule5) OR ((triple10 triple12) -> rule6) OR ((((((triple12) -> rule1)) -> rule2)) -> rule5) OR ((((((triple12) -> rule1)) -> rule2) triple12) -> rule6))] @1: The bear is blue.[(((triple14) -> rule4) OR ((triple7) -> rule4))] The bear needs the bear.[(((triple1) -> rule5) OR ((((triple4) -> rule2)) -> rule5))] The dog needs the rabbit.[(((triple5) -> rule1))] The rabbit needs the rabbit.[(((triple12) -> rule1))] @2: The dog chases the dog.[(((((triple5) -> rule1)) -> rule2))] @3: The dog needs the bear.[(((((((triple5) -> rule1)) -> rule2)) -> rule5) OR ((((((triple5) -> rule1)) -> rule2) triple5) -> rule6))]
The bear chases the dog.
("bear" "chases" "dog" "+")
triple1
((triple4) -> (rule2 % int1))
The bear chases the dog.
("bear" "chases" "dog" "+")
int1
The bear is round.
("bear" "is" "round" "+")
triple2
The bear likes the dog.
("bear" "likes" "dog" "+")
triple3
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
triple4
The dog is cold.
("dog" "is" "cold" "+")
triple5
The dog is nice.
("dog" "is" "nice" "+")
triple6
The dog likes the bear.
("dog" "likes" "bear" "+")
triple7
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple8
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
triple9
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
triple10
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple11
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple12
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple13
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
triple14
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple15
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple16
((triple10) -> (rule5 % int1))
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int1
((triple10 triple12) -> (rule6 % int1))
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int1
((((((triple12) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3
((((((triple12) -> (rule1 % int3))) -> (rule2 % int2)) triple12) -> (rule6 % int1))
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3
The bear is blue.
("bear" "is" "blue" "+")
((triple14) -> (rule4 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
((triple7) -> (rule4 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
((triple1) -> (rule5 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear chases the dog.
("bear" "chases" "dog" "+")
int2
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
((triple5) -> (rule1 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple12) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int2
The dog needs the bear.
("dog" "needs" "bear" "+")
((((((triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int3
((((((triple5) -> (rule1 % int3))) -> (rule2 % int2)) triple5) -> (rule6 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int3