The lion eats the rabbit. The lion likes the tiger. The mouse chases the lion. The mouse is rough. The rabbit is green. The rabbit does not like the tiger. The tiger chases the rabbit. If something chases the rabbit then it is rough. If something is rough then it likes the lion. If something eats the mouse and the mouse likes the tiger then the mouse is not blue. If something chases the mouse then the mouse chases the rabbit. If the tiger eats the mouse then the mouse chases the rabbit. If something likes the lion and it does not like the mouse then the lion does not like the tiger. If something eats the rabbit then the rabbit does not eat the mouse. If the lion likes the tiger and the tiger likes the lion then the lion chases the rabbit. If something eats the lion then the lion eats the rabbit.
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit does not like the tiger.
("rabbit" "likes" "tiger" "-")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
If something chases the rabbit then it is rough.
((("something" "chases" "rabbit" "+")) -> ("something" "is" "rough" "+"))
If something is rough then it likes the lion.
((("something" "is" "rough" "+")) -> ("something" "likes" "lion" "+"))
If something eats the mouse and the mouse likes the tiger then the mouse is not blue.
((("something" "eats" "mouse" "+") ("mouse" "likes" "tiger" "+")) -> ("mouse" "is" "blue" "-"))
If something chases the mouse then the mouse chases the rabbit.
((("something" "chases" "mouse" "+")) -> ("mouse" "chases" "rabbit" "+"))
If the tiger eats the mouse then the mouse chases the rabbit.
((("tiger" "eats" "mouse" "+")) -> ("mouse" "chases" "rabbit" "+"))
If something likes the lion and it does not like the mouse then the lion does not like the tiger.
((("something" "likes" "lion" "+") ("something" "likes" "mouse" "~")) -> ("lion" "likes" "tiger" "-"))
If something eats the rabbit then the rabbit does not eat the mouse.
((("something" "eats" "rabbit" "+")) -> ("rabbit" "eats" "mouse" "-"))
If the lion likes the tiger and the tiger likes the lion then the lion chases the rabbit.
((("lion" "likes" "tiger" "+") ("tiger" "likes" "lion" "+")) -> ("lion" "chases" "rabbit" "+"))
If something eats the lion then the lion eats the rabbit.
((("something" "eats" "lion" "+")) -> ("lion" "eats" "rabbit" "+"))
The mouse is rough.
True
1
proof
[(triple4)]
("mouse" "is" "rough" "+")
triple4
The mouse is not rough.
False
1
inv-proof
[(triple4)]
("mouse" "is" "rough" "-")
triple4
The tiger is rough.
True
2
proof
[(((triple7) -> rule1))]
("tiger" "is" "rough" "+")
((triple7) -> (rule1 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is not rough.
False
2
inv-proof
[(((triple7) -> rule1))]
("tiger" "is" "rough" "-")
((triple7) -> (rule1 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger likes the lion.
True
3
proof
[(((((triple7) -> rule1)) -> rule2))]
("tiger" "likes" "lion" "+")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The tiger does not like the lion.
False
3
inv-proof
[(((((triple7) -> rule1)) -> rule2))]
("tiger" "likes" "lion" "-")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The lion chases the rabbit.
True
5
proof
[(((triple2 ((((triple7) -> rule1)) -> rule2)) -> rule8))]
("lion" "chases" "rabbit" "+")
((triple2 ((((triple7) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int1
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int2
The tiger is rough.
("tiger" "is" "rough" "+")
int3
The lion does not chase the rabbit.
False
5
inv-proof
[(((triple2 ((((triple7) -> rule1)) -> rule2)) -> rule8))]
("lion" "chases" "rabbit" "-")
((triple2 ((((triple7) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int1
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int2
The tiger is rough.
("tiger" "is" "rough" "+")
int3
The lion is rough.
True
6
proof
[(((((triple2 ((((triple7) -> rule1)) -> rule2)) -> rule8)) -> rule1))]
("lion" "is" "rough" "+")
((((triple2 ((((triple7) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int2
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int3
The tiger is rough.
("tiger" "is" "rough" "+")
int4
The lion is not rough.
False
6
inv-proof
[(((((triple2 ((((triple7) -> rule1)) -> rule2)) -> rule8)) -> rule1))]
("lion" "is" "rough" "-")
((((triple2 ((((triple7) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int2
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int3
The tiger is rough.
("tiger" "is" "rough" "+")
int4
The lion likes the lion.
True
7
proof
[(((((((triple2 ((((triple7) -> rule1)) -> rule2)) -> rule8)) -> rule1)) -> rule2))]
("lion" "likes" "lion" "+")
((((((triple2 ((((triple7) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int3
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int4
The tiger is rough.
("tiger" "is" "rough" "+")
int5
The lion does not like the lion.
False
7
inv-proof
[(((((((triple2 ((((triple7) -> rule1)) -> rule2)) -> rule8)) -> rule1)) -> rule2))]
("lion" "likes" "lion" "-")
((((((triple2 ((((triple7) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int3
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int4
The tiger is rough.
("tiger" "is" "rough" "+")
int5
The rabbit does not like the lion.
Unknown
inv-rconc
[@2: The rabbit likes the lion.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("rabbit" "likes" "lion" "-")
The mouse chases the rabbit.
Unknown
rconc
[@1: The mouse chases the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "chases" "rabbit" "+")
The rabbit is not rough.
Unknown
inv-rconc
[@1: The rabbit is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "rough" "-")
The lion chases the tiger.
Unknown
random
[@0: The lion chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "tiger" "+")
The mouse does not eat the tiger.
Unknown
inv-random
[@0: The mouse eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "tiger" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
The rabbit is not kind.
Unknown
inv-random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "-")
The rabbit eats the tiger.
Unknown
random
[@0: The rabbit eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "tiger" "+")
The mouse does not like the tiger.
Unknown
inv-random
[@0: The mouse likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "tiger" "-")
The rabbit chases the lion.
Unknown
random
[@0: The rabbit chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "lion" "+")
The tiger is not round.
Unknown
inv-random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
@0: The lion eats the rabbit.[(triple1)] The lion likes the tiger.[(triple2)] The mouse chases the lion.[(triple3)] The mouse is rough.[(triple4)] The rabbit does not like the tiger.[(triple6)] The rabbit is green.[(triple5)] The tiger chases the rabbit.[(triple7)] @1: The mouse likes the lion.[(((triple4) -> rule2))] The rabbit does not eat the mouse.[(((triple1) -> rule7))] The tiger is rough.[(((triple7) -> rule1))] @2: The tiger likes the lion.[(((((triple7) -> rule1)) -> rule2))] @3: The lion chases the rabbit.[(((triple2 ((((triple7) -> rule1)) -> rule2)) -> rule8))] @4: The lion is rough.[(((((triple2 ((((triple7) -> rule1)) -> rule2)) -> rule8)) -> rule1))] @5: The lion likes the lion.[(((((((triple2 ((((triple7) -> rule1)) -> rule2)) -> rule8)) -> rule1)) -> rule2))]
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple1
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple3
The mouse is rough.
("mouse" "is" "rough" "+")
triple4
The rabbit does not like the tiger.
("rabbit" "likes" "tiger" "-")
triple6
The rabbit is green.
("rabbit" "is" "green" "+")
triple5
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple7
The mouse likes the lion.
("mouse" "likes" "lion" "+")
((triple4) -> (rule2 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The rabbit does not eat the mouse.
("rabbit" "eats" "mouse" "-")
((triple1) -> (rule7 % int1))
The rabbit does not eat the mouse.
("rabbit" "eats" "mouse" "-")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
((triple7) -> (rule1 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger likes the lion.
("tiger" "likes" "lion" "+")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
((triple2 ((((triple7) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int1
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int2
The tiger is rough.
("tiger" "is" "rough" "+")
int3
The lion is rough.
("lion" "is" "rough" "+")
((((triple2 ((((triple7) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int2
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int3
The tiger is rough.
("tiger" "is" "rough" "+")
int4
The lion likes the lion.
("lion" "likes" "lion" "+")
((((((triple2 ((((triple7) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int3
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int4
The tiger is rough.
("tiger" "is" "rough" "+")
int5