The mouse eats the tiger. The mouse is nice. The mouse likes the rabbit. The mouse likes the tiger. The rabbit eats the mouse. The rabbit eats the tiger. The rabbit is kind. The rabbit likes the tiger. The rabbit does not visit the tiger. The tiger eats the mouse. The tiger is blue. The tiger likes the mouse. If something visits the tiger and it likes the tiger then it eats the mouse. If something eats the rabbit then it does not eat the tiger. If something likes the mouse then it is not rough. If something is young then it likes the mouse. If something eats the tiger and it eats the mouse then it is young. If the mouse likes the tiger and the tiger is not young then the mouse likes the rabbit.
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The rabbit does not visit the tiger.
("rabbit" "visits" "tiger" "-")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
If something visits the tiger and it likes the tiger then it eats the mouse.
((("something" "visits" "tiger" "+") ("something" "likes" "tiger" "+")) -> ("something" "eats" "mouse" "+"))
If something eats the rabbit then it does not eat the tiger.
((("something" "eats" "rabbit" "+")) -> ("something" "eats" "tiger" "-"))
If something likes the mouse then it is not rough.
((("something" "likes" "mouse" "+")) -> ("something" "is" "rough" "-"))
If something is young then it likes the mouse.
((("something" "is" "young" "+")) -> ("something" "likes" "mouse" "+"))
If something eats the tiger and it eats the mouse then it is young.
((("something" "eats" "tiger" "+") ("something" "eats" "mouse" "+")) -> ("something" "is" "young" "+"))
If the mouse likes the tiger and the tiger is not young then the mouse likes the rabbit.
((("mouse" "likes" "tiger" "+") ("tiger" "is" "young" "~")) -> ("mouse" "likes" "rabbit" "+"))
The mouse is nice.
True
1
proof
[(triple2)]
("mouse" "is" "nice" "+")
triple2
The tiger does not like the mouse.
False
1
inv-proof
[(triple12)]
("tiger" "likes" "mouse" "-")
triple12
The rabbit is young.
True
3
proof
[(((triple6 triple5) -> rule5))]
("rabbit" "is" "young" "+")
((triple6 triple5) -> (rule5 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The tiger is rough.
False
2
inv-proof
[(((triple12) -> rule3))]
("tiger" "is" "rough" "+")
((triple12) -> (rule3 % int1))
The tiger is not rough.
("tiger" "is" "rough" "-")
int1
The rabbit likes the mouse.
True
4
proof
[(((((triple6 triple5) -> rule5)) -> rule4))]
("rabbit" "likes" "mouse" "+")
((((triple6 triple5) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit does not like the mouse.
False
4
inv-proof
[(((((triple6 triple5) -> rule5)) -> rule4))]
("rabbit" "likes" "mouse" "-")
((((triple6 triple5) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit is not rough.
True
5
proof
[(((((((triple6 triple5) -> rule5)) -> rule4)) -> rule3))]
("rabbit" "is" "rough" "-")
((((((triple6 triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit is not rough.
("rabbit" "is" "rough" "-")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
int3
The rabbit is rough.
False
5
inv-proof
[(((((((triple6 triple5) -> rule5)) -> rule4)) -> rule3))]
("rabbit" "is" "rough" "+")
((((((triple6 triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit is not rough.
("rabbit" "is" "rough" "-")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
int3
The mouse does not eat the mouse.
Unknown
inv-rconc
[@1: The mouse eats the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "eats" "mouse" "-")
The mouse likes the mouse.
Unknown
rconc
[@3: The mouse likes the mouse.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule1 <- FAIL)]]
("mouse" "likes" "mouse" "+")
The tiger is not young.
Unknown
inv-rconc
[@1: The tiger is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "is" "young" "-")
The mouse is young.
Unknown
rconc
[@2: The mouse is young.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("mouse" "is" "young" "+")
The tiger does not visit the mouse.
Unknown
inv-random
[@0: The tiger visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "mouse" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "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 tiger visits the rabbit.
Unknown
random
[@0: The tiger visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "rabbit" "+")
@0: The mouse eats the tiger.[(triple1)] The mouse is nice.[(triple2)] The mouse likes the rabbit.[(triple3)] The mouse likes the tiger.[(triple4)] The rabbit does not visit the tiger.[(triple9)] The rabbit eats the mouse.[(triple5)] The rabbit eats the tiger.[(triple6)] The rabbit is kind.[(triple7)] The rabbit likes the tiger.[(triple8)] The tiger eats the mouse.[(triple10)] The tiger is blue.[(triple11)] The tiger likes the mouse.[(triple12)] @1: The rabbit is young.[(((triple6 triple5) -> rule5))] The tiger is not rough.[(((triple12) -> rule3))] @2: The rabbit likes the mouse.[(((((triple6 triple5) -> rule5)) -> rule4))] @3: The rabbit is not rough.[(((((((triple6 triple5) -> rule5)) -> rule4)) -> rule3))]
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple1
The mouse is nice.
("mouse" "is" "nice" "+")
triple2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple3
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple4
The rabbit does not visit the tiger.
("rabbit" "visits" "tiger" "-")
triple9
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple5
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple6
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple7
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple8
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple10
The tiger is blue.
("tiger" "is" "blue" "+")
triple11
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple12
The rabbit is young.
("rabbit" "is" "young" "+")
((triple6 triple5) -> (rule5 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The tiger is not rough.
("tiger" "is" "rough" "-")
((triple12) -> (rule3 % int1))
The tiger is not rough.
("tiger" "is" "rough" "-")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
((((triple6 triple5) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit is not rough.
("rabbit" "is" "rough" "-")
((((((triple6 triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit is not rough.
("rabbit" "is" "rough" "-")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
int3