The mouse is kind. The mouse is nice. The mouse is round. The mouse likes the rabbit. The mouse needs the rabbit. The mouse visits the rabbit. The rabbit visits the mouse. If something needs the mouse and the mouse visits the rabbit then the rabbit is round. If something needs the mouse and the mouse visits the rabbit then the rabbit needs the mouse. If something visits the rabbit then it likes the rabbit. If the rabbit likes the mouse and the rabbit visits the mouse then the mouse is nice. If something visits the rabbit then the rabbit visits the mouse. If something visits the mouse then it is big. If something is kind then it likes the rabbit. If something is big then it likes the mouse.
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If something needs the mouse and the mouse visits the rabbit then the rabbit is round.
((("something" "needs" "mouse" "+") ("mouse" "visits" "rabbit" "+")) -> ("rabbit" "is" "round" "+"))
If something needs the mouse and the mouse visits the rabbit then the rabbit needs the mouse.
((("something" "needs" "mouse" "+") ("mouse" "visits" "rabbit" "+")) -> ("rabbit" "needs" "mouse" "+"))
If something visits the rabbit then it likes the rabbit.
((("something" "visits" "rabbit" "+")) -> ("something" "likes" "rabbit" "+"))
If the rabbit likes the mouse and the rabbit visits the mouse then the mouse is nice.
((("rabbit" "likes" "mouse" "+") ("rabbit" "visits" "mouse" "+")) -> ("mouse" "is" "nice" "+"))
If something visits the rabbit then the rabbit visits the mouse.
((("something" "visits" "rabbit" "+")) -> ("rabbit" "visits" "mouse" "+"))
If something visits the mouse then it is big.
((("something" "visits" "mouse" "+")) -> ("something" "is" "big" "+"))
If something is kind then it likes the rabbit.
((("something" "is" "kind" "+")) -> ("something" "likes" "rabbit" "+"))
If something is big then it likes the mouse.
((("something" "is" "big" "+")) -> ("something" "likes" "mouse" "+"))
The mouse is round.
True
1
proof
[(triple3)]
("mouse" "is" "round" "+")
triple3
The mouse is not nice.
False
1
inv-proof
[(triple2 OR ((((((triple7) -> rule6)) -> rule8) triple7) -> rule4) OR ((((((triple7) -> rule6)) -> rule8) ((triple6) -> rule5)) -> rule4) OR ((((((((triple6) -> rule5)) -> rule6)) -> rule8) triple7) -> rule4) OR ((((((((triple6) -> rule5)) -> rule6)) -> rule8) ((triple6) -> rule5)) -> rule4))]
("mouse" "is" "nice" "-")
triple2
((((((triple7) -> (rule6 % int3))) -> (rule8 % int2)) triple7) -> (rule4 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
((((((triple7) -> (rule6 % int4))) -> (rule8 % int3)) ((triple6) -> (rule5 % int2))) -> (rule4 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int2
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int3
The rabbit is big.
("rabbit" "is" "big" "+")
int4
((((((((triple6) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule8 % int2)) triple7) -> (rule4 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int4
((((((((triple6) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule8 % int2)) ((triple6) -> (rule5 % int4))) -> (rule4 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int4
The rabbit is big.
True
2
proof
[(((triple7) -> rule6) OR ((((triple6) -> rule5)) -> rule6))]
("rabbit" "is" "big" "+")
((triple7) -> (rule6 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule6 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int2
The rabbit is not big.
False
2
inv-proof
[(((triple7) -> rule6) OR ((((triple6) -> rule5)) -> rule6))]
("rabbit" "is" "big" "-")
((triple7) -> (rule6 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule6 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int2
The mouse is not big.
Unknown
inv-rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "big" "-")
The rabbit likes the rabbit.
Unknown
rconc
[@1: The rabbit likes the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "likes" "rabbit" "+")
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The rabbit is nice.
Unknown
random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "+")
@0: The mouse is kind.[(triple1)] The mouse is nice.[(triple2 OR ((((((triple7) -> rule6)) -> rule8) triple7) -> rule4) OR ((((((triple7) -> rule6)) -> rule8) ((triple6) -> rule5)) -> rule4) OR ((((((((triple6) -> rule5)) -> rule6)) -> rule8) triple7) -> rule4) OR ((((((((triple6) -> rule5)) -> rule6)) -> rule8) ((triple6) -> rule5)) -> rule4))] The mouse is round.[(triple3)] The mouse likes the rabbit.[(triple4 OR ((triple1) -> rule7) OR ((triple6) -> rule3))] The mouse needs the rabbit.[(triple5)] The mouse visits the rabbit.[(triple6)] The rabbit visits the mouse.[(triple7 OR ((triple6) -> rule5))] @1: The rabbit is big.[(((triple7) -> rule6) OR ((((triple6) -> rule5)) -> rule6))] @2: The rabbit likes the mouse.[(((((triple7) -> rule6)) -> rule8) OR ((((((triple6) -> rule5)) -> rule6)) -> rule8))]
The mouse is kind.
("mouse" "is" "kind" "+")
triple1
The mouse is nice.
("mouse" "is" "nice" "+")
triple2
((((((triple7) -> (rule6 % int3))) -> (rule8 % int2)) triple7) -> (rule4 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
((((((triple7) -> (rule6 % int4))) -> (rule8 % int3)) ((triple6) -> (rule5 % int2))) -> (rule4 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int2
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int3
The rabbit is big.
("rabbit" "is" "big" "+")
int4
((((((((triple6) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule8 % int2)) triple7) -> (rule4 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int4
((((((((triple6) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule8 % int2)) ((triple6) -> (rule5 % int4))) -> (rule4 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int4
The mouse is round.
("mouse" "is" "round" "+")
triple3
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple4
((triple1) -> (rule7 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
((triple6) -> (rule3 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple5
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple6
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple7
((triple6) -> (rule5 % int1))
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
((triple7) -> (rule6 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule6 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int2
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
((((triple7) -> (rule6 % int2))) -> (rule8 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
((((((triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int3