The dog likes the mouse. The dog likes the rabbit. The dog needs the rabbit. The mouse is rough. The mouse likes the dog. The rabbit chases the dog. The rabbit is green. If someone needs the rabbit and they chase the rabbit then they need the mouse. If the dog needs the mouse and the dog is green then the mouse needs the rabbit. If the dog likes the rabbit and the rabbit is kind then the rabbit needs the mouse. If someone needs the rabbit then they are kind. If someone likes the mouse and the mouse chases the dog then they need the dog. If the dog needs the mouse and the dog chases the mouse then the dog is young. If someone is green then they need the rabbit. If someone likes the dog then the dog chases the mouse.
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
If someone needs the rabbit and they chase the rabbit then they need the mouse.
((("someone" "needs" "rabbit" "+") ("someone" "chases" "rabbit" "+")) -> ("someone" "needs" "mouse" "+"))
If the dog needs the mouse and the dog is green then the mouse needs the rabbit.
((("dog" "needs" "mouse" "+") ("dog" "is" "green" "+")) -> ("mouse" "needs" "rabbit" "+"))
If the dog likes the rabbit and the rabbit is kind then the rabbit needs the mouse.
((("dog" "likes" "rabbit" "+") ("rabbit" "is" "kind" "+")) -> ("rabbit" "needs" "mouse" "+"))
If someone needs the rabbit then they are kind.
((("someone" "needs" "rabbit" "+")) -> ("someone" "is" "kind" "+"))
If someone likes the mouse and the mouse chases the dog then they need the dog.
((("someone" "likes" "mouse" "+") ("mouse" "chases" "dog" "+")) -> ("someone" "needs" "dog" "+"))
If the dog needs the mouse and the dog chases the mouse then the dog is young.
((("dog" "needs" "mouse" "+") ("dog" "chases" "mouse" "+")) -> ("dog" "is" "young" "+"))
If someone is green then they need the rabbit.
((("someone" "is" "green" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone likes the dog then the dog chases the mouse.
((("someone" "likes" "dog" "+")) -> ("dog" "chases" "mouse" "+"))
The mouse likes the dog.
True
1
proof
[(triple5)]
("mouse" "likes" "dog" "+")
triple5
The mouse is not rough.
False
1
inv-proof
[(triple4)]
("mouse" "is" "rough" "-")
triple4
The dog chases the mouse.
True
2
proof
[(((triple5) -> rule8))]
("dog" "chases" "mouse" "+")
((triple5) -> (rule8 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The dog does not chase the mouse.
False
2
inv-proof
[(((triple5) -> rule8))]
("dog" "chases" "mouse" "-")
((triple5) -> (rule8 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The rabbit is kind.
True
3
proof
[(((((triple7) -> rule7)) -> rule4))]
("rabbit" "is" "kind" "+")
((((triple7) -> (rule7 % int2))) -> (rule4 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit is not kind.
False
3
inv-proof
[(((((triple7) -> rule7)) -> rule4))]
("rabbit" "is" "kind" "-")
((((triple7) -> (rule7 % int2))) -> (rule4 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit needs the mouse.
True
5
proof
[(((triple2 ((((triple7) -> rule7)) -> rule4)) -> rule3))]
("rabbit" "needs" "mouse" "+")
((triple2 ((((triple7) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3
The rabbit does not need the mouse.
False
5
inv-proof
[(((triple2 ((((triple7) -> rule7)) -> rule4)) -> rule3))]
("rabbit" "needs" "mouse" "-")
((triple2 ((((triple7) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3
The dog is not young.
Unknown
inv-rconc
[@2: The dog is young.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("dog" "is" "young" "-")
The mouse needs the mouse.
Unknown
rconc
[@1: The mouse needs the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "needs" "mouse" "+")
The mouse is not kind.
Unknown
inv-rconc
[@2: The mouse is kind.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("mouse" "is" "kind" "-")
The dog needs the dog.
Unknown
rconc
[@1: The dog needs the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "needs" "dog" "+")
The mouse does not chase the dog.
Unknown
inv-random
[@0: The mouse chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "dog" "-")
The rabbit is young.
Unknown
random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "+")
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 likes the mouse.
Unknown
random
[@0: The rabbit likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "mouse" "+")
@0: The dog likes the mouse.[(triple1)] The dog likes the rabbit.[(triple2)] The dog needs the rabbit.[(triple3)] The mouse is rough.[(triple4)] The mouse likes the dog.[(triple5)] The rabbit chases the dog.[(triple6)] The rabbit is green.[(triple7)] @1: The dog chases the mouse.[(((triple5) -> rule8))] The dog is kind.[(((triple3) -> rule4))] The rabbit needs the rabbit.[(((triple7) -> rule7))] @2: The rabbit is kind.[(((((triple7) -> rule7)) -> rule4))] @3: The rabbit needs the mouse.[(((triple2 ((((triple7) -> rule7)) -> rule4)) -> rule3))]
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple2
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple3
The mouse is rough.
("mouse" "is" "rough" "+")
triple4
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple5
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
triple6
The rabbit is green.
("rabbit" "is" "green" "+")
triple7
The dog chases the mouse.
("dog" "chases" "mouse" "+")
((triple5) -> (rule8 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
((triple3) -> (rule4 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple7) -> (rule7 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
((((triple7) -> (rule7 % int2))) -> (rule4 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
((triple2 ((((triple7) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3