The dog chases the mouse. The dog needs the rabbit. The mouse does not eat the rabbit. The rabbit chases the mouse. The rabbit eats the mouse. The rabbit is big. The rabbit is young. If the mouse needs the dog then the mouse needs the rabbit. If something chases the mouse and it eats the mouse then the mouse is rough. All nice things are big. If the mouse does not chase the rabbit then the rabbit does not eat the dog. If something is cold and it does not eat the mouse then the mouse does not need the dog. If something eats the rabbit and the rabbit does not chase the dog then the dog does not chase the rabbit. Rough things are nice. If something chases the mouse then it needs the rabbit.
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The mouse does not eat the rabbit.
("mouse" "eats" "rabbit" "-")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
If the mouse needs the dog then the mouse needs the rabbit.
((("mouse" "needs" "dog" "+")) -> ("mouse" "needs" "rabbit" "+"))
If something chases the mouse and it eats the mouse then the mouse is rough.
((("something" "chases" "mouse" "+") ("something" "eats" "mouse" "+")) -> ("mouse" "is" "rough" "+"))
All nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If the mouse does not chase the rabbit then the rabbit does not eat the dog.
((("mouse" "chases" "rabbit" "~")) -> ("rabbit" "eats" "dog" "-"))
If something is cold and it does not eat the mouse then the mouse does not need the dog.
((("something" "is" "cold" "+") ("something" "eats" "mouse" "~")) -> ("mouse" "needs" "dog" "-"))
If something eats the rabbit and the rabbit does not chase the dog then the dog does not chase the rabbit.
((("something" "eats" "rabbit" "+") ("rabbit" "chases" "dog" "~")) -> ("dog" "chases" "rabbit" "-"))
Rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If something chases the mouse then it needs the rabbit.
((("something" "chases" "mouse" "+")) -> ("something" "needs" "rabbit" "+"))
The mouse does not eat the rabbit.
True
1
proof
[(triple3)]
("mouse" "eats" "rabbit" "-")
triple3
The dog does not need the rabbit.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule8))]
("dog" "needs" "rabbit" "-")
triple2
((triple1) -> (rule8 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
The rabbit needs the rabbit.
True
2
proof
[(((triple4) -> rule8))]
("rabbit" "needs" "rabbit" "+")
((triple4) -> (rule8 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The mouse is not rough.
False
3
inv-proof
[(((triple4 triple5) -> rule2))]
("mouse" "is" "rough" "-")
((triple4 triple5) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is nice.
True
4
proof
[(((((triple4 triple5) -> rule2)) -> rule7))]
("mouse" "is" "nice" "+")
((((triple4 triple5) -> (rule2 % int2))) -> (rule7 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is not nice.
False
4
inv-proof
[(((((triple4 triple5) -> rule2)) -> rule7))]
("mouse" "is" "nice" "-")
((((triple4 triple5) -> (rule2 % int2))) -> (rule7 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is big.
True
5
proof
[(((((((triple4 triple5) -> rule2)) -> rule7)) -> rule3))]
("mouse" "is" "big" "+")
((((((triple4 triple5) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The mouse is not big.
False
5
inv-proof
[(((((((triple4 triple5) -> rule2)) -> rule7)) -> rule3))]
("mouse" "is" "big" "-")
((((((triple4 triple5) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The rabbit is not nice.
Unknown
inv-rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "is" "nice" "-")
The mouse needs the rabbit.
Unknown
rconc
[@1: The mouse needs the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "needs" "rabbit" "+")
The dog is not big.
Unknown
inv-rconc
[@2: The dog is big.[CWA. Example of deepest failure = (rule3 <- rule7 <- FAIL)]]
("dog" "is" "big" "-")
The dog is nice.
Unknown
rconc
[@1: The dog is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "is" "nice" "+")
The dog does not eat the mouse.
Unknown
inv-random
[@0: The dog eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "mouse" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
The dog is not rough.
Unknown
inv-random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "-")
The mouse chases the rabbit.
Unknown
random
[@0: The mouse chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "rabbit" "+")
@0: The dog chases the mouse.[(triple1)] The dog needs the rabbit.[(triple2 OR ((triple1) -> rule8))] The mouse does not eat the rabbit.[(triple3)] The rabbit chases the mouse.[(triple4)] The rabbit eats the mouse.[(triple5)] The rabbit is big.[(triple6)] The rabbit is young.[(triple7)] @1: The mouse is rough.[(((triple4 triple5) -> rule2))] The rabbit needs the rabbit.[(((triple4) -> rule8))] @2: The mouse is nice.[(((((triple4 triple5) -> rule2)) -> rule7))] @3: The mouse is big.[(((((((triple4 triple5) -> rule2)) -> rule7)) -> rule3))]
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple1
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple2
((triple1) -> (rule8 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
The mouse does not eat the rabbit.
("mouse" "eats" "rabbit" "-")
triple3
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple4
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple5
The rabbit is big.
("rabbit" "is" "big" "+")
triple6
The rabbit is young.
("rabbit" "is" "young" "+")
triple7
The mouse is rough.
("mouse" "is" "rough" "+")
((triple4 triple5) -> (rule2 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple4) -> (rule8 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
((((triple4 triple5) -> (rule2 % int2))) -> (rule7 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
((((((triple4 triple5) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3