The lion eats the mouse. The lion eats the tiger. The lion likes the mouse. The mouse eats the lion. The mouse eats the rabbit. The mouse eats the tiger. The mouse is cold. The mouse is green. The mouse likes the rabbit. The rabbit chases the mouse. The rabbit eats the lion. The rabbit eats the mouse. The rabbit is rough. The tiger eats the mouse. The tiger is round. If someone likes the lion then the lion is nice. If the mouse chases the rabbit and the rabbit eats the lion then the mouse is round. If the rabbit is rough and the rabbit eats the tiger then the rabbit chases the tiger. If someone eats the mouse then they chase the rabbit. If someone chases the tiger and the tiger likes the mouse then the mouse eats the rabbit. If someone chases the rabbit and they are rough then they eat the tiger.
The lion eats the mouse.
("lion" "eats" "mouse" "+")
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger is round.
("tiger" "is" "round" "+")
If someone likes the lion then the lion is nice.
((("someone" "likes" "lion" "+")) -> ("lion" "is" "nice" "+"))
If the mouse chases the rabbit and the rabbit eats the lion then the mouse is round.
((("mouse" "chases" "rabbit" "+") ("rabbit" "eats" "lion" "+")) -> ("mouse" "is" "round" "+"))
If the rabbit is rough and the rabbit eats the tiger then the rabbit chases the tiger.
((("rabbit" "is" "rough" "+") ("rabbit" "eats" "tiger" "+")) -> ("rabbit" "chases" "tiger" "+"))
If someone eats the mouse then they chase the rabbit.
((("someone" "eats" "mouse" "+")) -> ("someone" "chases" "rabbit" "+"))
If someone chases the tiger and the tiger likes the mouse then the mouse eats the rabbit.
((("someone" "chases" "tiger" "+") ("tiger" "likes" "mouse" "+")) -> ("mouse" "eats" "rabbit" "+"))
If someone chases the rabbit and they are rough then they eat the tiger.
((("someone" "chases" "rabbit" "+") ("someone" "is" "rough" "+")) -> ("someone" "eats" "tiger" "+"))
The rabbit chases the mouse.
True
1
proof
[(triple10)]
("rabbit" "chases" "mouse" "+")
triple10
The lion does not eat the tiger.
False
1
inv-proof
[(triple2)]
("lion" "eats" "tiger" "-")
triple2
The tiger chases the rabbit.
True
2
proof
[(((triple14) -> rule4))]
("tiger" "chases" "rabbit" "+")
((triple14) -> (rule4 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The rabbit does not chase the rabbit.
False
2
inv-proof
[(((triple12) -> rule4))]
("rabbit" "chases" "rabbit" "-")
((triple12) -> (rule4 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit eats the tiger.
True
4
proof
[(((((triple12) -> rule4) triple13) -> rule6))]
("rabbit" "eats" "tiger" "+")
((((triple12) -> (rule4 % int2)) triple13) -> (rule6 % int1))
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The rabbit does not eat the tiger.
False
4
inv-proof
[(((((triple12) -> rule4) triple13) -> rule6))]
("rabbit" "eats" "tiger" "-")
((((triple12) -> (rule4 % int2)) triple13) -> (rule6 % int1))
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The rabbit chases the tiger.
True
6
proof
[(((triple13 ((((triple12) -> rule4) triple13) -> rule6)) -> rule3))]
("rabbit" "chases" "tiger" "+")
((triple13 ((((triple12) -> (rule4 % int3)) triple13) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int3
The rabbit does not chase the tiger.
False
6
inv-proof
[(((triple13 ((((triple12) -> rule4) triple13) -> rule6)) -> rule3))]
("rabbit" "chases" "tiger" "-")
((triple13 ((((triple12) -> (rule4 % int3)) triple13) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int3
The mouse does not chase the rabbit.
Unknown
inv-rconc
[@1: The mouse chases the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "chases" "rabbit" "-")
The tiger eats the tiger.
Unknown
rconc
[@1: The tiger eats the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "eats" "tiger" "+")
The mouse is not round.
Unknown
inv-rconc
[@2: The mouse is round.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("mouse" "is" "round" "-")
The lion is nice.
Unknown
rconc
[@1: The lion is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "nice" "+")
The lion does not eat the rabbit.
Unknown
inv-random
[@0: The lion eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "rabbit" "-")
The lion is round.
Unknown
random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "+")
The tiger does not like the mouse.
Unknown
inv-random
[@0: The tiger likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "mouse" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
@0: The lion eats the mouse.[(triple1)] The lion eats the tiger.[(triple2)] The lion likes the mouse.[(triple3)] The mouse eats the lion.[(triple4)] The mouse eats the rabbit.[(triple5)] The mouse eats the tiger.[(triple6)] The mouse is cold.[(triple7)] The mouse is green.[(triple8)] The mouse likes the rabbit.[(triple9)] The rabbit chases the mouse.[(triple10)] The rabbit eats the lion.[(triple11)] The rabbit eats the mouse.[(triple12)] The rabbit is rough.[(triple13)] The tiger eats the mouse.[(triple14)] The tiger is round.[(triple15)] @1: The lion chases the rabbit.[(((triple1) -> rule4))] The rabbit chases the rabbit.[(((triple12) -> rule4))] The tiger chases the rabbit.[(((triple14) -> rule4))] @2: The rabbit eats the tiger.[(((((triple12) -> rule4) triple13) -> rule6))] @3: The rabbit chases the tiger.[(((triple13 ((((triple12) -> rule4) triple13) -> rule6)) -> rule3))]
The lion eats the mouse.
("lion" "eats" "mouse" "+")
triple1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple3
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple4
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple5
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple6
The mouse is cold.
("mouse" "is" "cold" "+")
triple7
The mouse is green.
("mouse" "is" "green" "+")
triple8
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple9
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple10
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple11
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple12
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple13
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple14
The tiger is round.
("tiger" "is" "round" "+")
triple15
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
((triple1) -> (rule4 % int1))
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((triple12) -> (rule4 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
((triple14) -> (rule4 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
((((triple12) -> (rule4 % int2)) triple13) -> (rule6 % int1))
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
((triple13 ((((triple12) -> (rule4 % int3)) triple13) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
int1
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int3