The mouse eats the tiger. The mouse is blue. The mouse is green. The mouse likes the rabbit. The mouse likes the tiger. The mouse needs the tiger. The rabbit eats the mouse. The rabbit eats the tiger. The rabbit is green. The rabbit is nice. The rabbit likes the tiger. The rabbit needs the mouse. The rabbit needs the tiger. The tiger eats the mouse. The tiger eats the rabbit. The tiger is nice. If something likes the mouse then it eats the mouse. All green things are young. If the mouse is young then the mouse is nice.
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
If something likes the mouse then it eats the mouse.
((("something" "likes" "mouse" "+")) -> ("something" "eats" "mouse" "+"))
All green things are young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If the mouse is young then the mouse is nice.
((("mouse" "is" "young" "+")) -> ("mouse" "is" "nice" "+"))
The mouse likes the tiger.
True
1
proof
[(triple5)]
("mouse" "likes" "tiger" "+")
triple5
The rabbit is not nice.
False
1
inv-proof
[(triple10)]
("rabbit" "is" "nice" "-")
triple10
The mouse is young.
True
2
proof
[(((triple3) -> rule2))]
("mouse" "is" "young" "+")
((triple3) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is not young.
False
2
inv-proof
[(((triple3) -> rule2))]
("mouse" "is" "young" "-")
((triple3) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is nice.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("mouse" "is" "nice" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is not nice.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("mouse" "is" "nice" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The tiger is not young.
Unknown
inv-rconc
[@1: The tiger is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "young" "-")
The mouse eats the mouse.
Unknown
rconc
[@1: The mouse eats the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "eats" "mouse" "+")
The rabbit is not rough.
Unknown
inv-random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "-")
The tiger is green.
Unknown
random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "+")
The rabbit is not blue.
Unknown
inv-random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "-")
The rabbit likes the mouse.
Unknown
random
[@0: The rabbit likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "mouse" "+")
@0: The mouse eats the tiger.[(triple1)] The mouse is blue.[(triple2)] The mouse is green.[(triple3)] The mouse likes the rabbit.[(triple4)] The mouse likes the tiger.[(triple5)] The mouse needs the tiger.[(triple6)] The rabbit eats the mouse.[(triple7)] The rabbit eats the tiger.[(triple8)] The rabbit is green.[(triple9)] The rabbit is nice.[(triple10)] The rabbit likes the tiger.[(triple11)] The rabbit needs the mouse.[(triple12)] The rabbit needs the tiger.[(triple13)] The tiger eats the mouse.[(triple14)] The tiger eats the rabbit.[(triple15)] The tiger is nice.[(triple16)] @1: The mouse is young.[(((triple3) -> rule2))] The rabbit is young.[(((triple9) -> rule2))] @2: The mouse is nice.[(((((triple3) -> rule2)) -> rule3))]
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple1
The mouse is blue.
("mouse" "is" "blue" "+")
triple2
The mouse is green.
("mouse" "is" "green" "+")
triple3
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple4
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple5
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple6
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple7
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple8
The rabbit is green.
("rabbit" "is" "green" "+")
triple9
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple10
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple11
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple12
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple13
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple14
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple15
The tiger is nice.
("tiger" "is" "nice" "+")
triple16
The mouse is young.
("mouse" "is" "young" "+")
((triple3) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
((triple9) -> (rule2 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2