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