The lion eats the mouse. The mouse is big. The mouse likes the tiger. The rabbit does not chase the tiger. The rabbit is big. The rabbit likes the tiger. The tiger is not big. If someone likes the tiger then they are blue. If someone is young then they eat the mouse. If someone is rough then they are cold. If someone is rough and they eat the mouse then they do not like the mouse. If someone is cold then they chase the lion. If someone is rough and they like the rabbit then they eat the tiger. All cold people are young. If someone likes the tiger then they are rough.
The lion eats the mouse.
("lion" "eats" "mouse" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The rabbit does not chase the tiger.
("rabbit" "chases" "tiger" "-")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The tiger is not big.
("tiger" "is" "big" "-")
If someone likes the tiger then they are blue.
((("someone" "likes" "tiger" "+")) -> ("someone" "is" "blue" "+"))
If someone is young then they eat the mouse.
((("someone" "is" "young" "+")) -> ("someone" "eats" "mouse" "+"))
If someone is rough then they are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If someone is rough and they eat the mouse then they do not like the mouse.
((("someone" "is" "rough" "+") ("someone" "eats" "mouse" "+")) -> ("someone" "likes" "mouse" "-"))
If someone is cold then they chase the lion.
((("someone" "is" "cold" "+")) -> ("someone" "chases" "lion" "+"))
If someone is rough and they like the rabbit then they eat the tiger.
((("someone" "is" "rough" "+") ("someone" "likes" "rabbit" "+")) -> ("someone" "eats" "tiger" "+"))
All cold people are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
If someone likes the tiger then they are rough.
((("someone" "likes" "tiger" "+")) -> ("someone" "is" "rough" "+"))
The rabbit likes the tiger.
True
1
proof
[(triple6)]
("rabbit" "likes" "tiger" "+")
triple6
The mouse does not like the tiger.
False
1
inv-proof
[(triple3)]
("mouse" "likes" "tiger" "-")
triple3
The mouse is rough.
True
2
proof
[(((triple3) -> rule8))]
("mouse" "is" "rough" "+")
((triple3) -> (rule8 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The rabbit is not blue.
False
2
inv-proof
[(((triple6) -> rule1))]
("rabbit" "is" "blue" "-")
((triple6) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is cold.
True
3
proof
[(((((triple6) -> rule8)) -> rule3))]
("rabbit" "is" "cold" "+")
((((triple6) -> (rule8 % int2))) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit is not cold.
False
3
inv-proof
[(((((triple6) -> rule8)) -> rule3))]
("rabbit" "is" "cold" "-")
((((triple6) -> (rule8 % int2))) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The mouse chases the lion.
True
4
proof
[(((((((triple3) -> rule8)) -> rule3)) -> rule5))]
("mouse" "chases" "lion" "+")
((((((triple3) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The rabbit does not chase the lion.
False
4
inv-proof
[(((((((triple6) -> rule8)) -> rule3)) -> rule5))]
("rabbit" "chases" "lion" "-")
((((((triple6) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
int3
The rabbit eats the mouse.
True
5
proof
[(((((((((triple6) -> rule8)) -> rule3)) -> rule7)) -> rule2))]
("rabbit" "eats" "mouse" "+")
((((((((triple6) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3
The rabbit is rough.
("rabbit" "is" "rough" "+")
int4
The rabbit does not eat the mouse.
False
5
inv-proof
[(((((((((triple6) -> rule8)) -> rule3)) -> rule7)) -> rule2))]
("rabbit" "eats" "mouse" "-")
((((((((triple6) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3
The rabbit is rough.
("rabbit" "is" "rough" "+")
int4
The rabbit does not like the mouse.
True
8
proof
[(((((triple6) -> rule8) ((((((((triple6) -> rule8)) -> rule3)) -> rule7)) -> rule2)) -> rule4))]
("rabbit" "likes" "mouse" "-")
((((triple6) -> (rule8 % int5)) ((((((((triple6) -> (rule8 % int5))) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit does not like the mouse.
("rabbit" "likes" "mouse" "-")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
int3
The rabbit is cold.
("rabbit" "is" "cold" "+")
int4
The rabbit is rough.
("rabbit" "is" "rough" "+")
int5
The mouse likes the mouse.
False
8
inv-proof
[(((((triple3) -> rule8) ((((((((triple3) -> rule8)) -> rule3)) -> rule7)) -> rule2)) -> rule4))]
("mouse" "likes" "mouse" "+")
((((triple3) -> (rule8 % int5)) ((((((((triple3) -> (rule8 % int5))) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The mouse does not like the mouse.
("mouse" "likes" "mouse" "-")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The mouse is cold.
("mouse" "is" "cold" "+")
int4
The mouse is rough.
("mouse" "is" "rough" "+")
int5
The rabbit does not eat the tiger.
Unknown
inv-rconc
[@1: The rabbit eats the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "eats" "tiger" "-")
The lion chases the lion.
Unknown
rconc
[@3: The lion chases the lion.[CWA. Example of deepest failure = (rule5 <- rule3 <- rule8 <- FAIL)]]
("lion" "chases" "lion" "+")
The lion does not eat the tiger.
Unknown
inv-rconc
[@1: The lion eats the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "eats" "tiger" "-")
The mouse eats the tiger.
Unknown
rconc
[@1: The mouse eats the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "eats" "tiger" "+")
The lion is not cold.
Unknown
inv-rconc
[@2: The lion is cold.[CWA. Example of deepest failure = (rule3 <- rule8 <- FAIL)]]
("lion" "is" "cold" "-")
The lion is young.
Unknown
rconc
[@3: The lion is young.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule8 <- FAIL)]]
("lion" "is" "young" "+")
The rabbit does not eat the lion.
Unknown
inv-random
[@0: The rabbit eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "lion" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
The tiger does not eat the lion.
Unknown
inv-random
[@0: The tiger eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "lion" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
The lion does not like the lion.
Unknown
inv-random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "-")
The mouse eats the lion.
Unknown
random
[@0: The mouse eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "lion" "+")
@0: The lion eats the mouse.[(triple1)] The mouse is big.[(triple2)] The mouse likes the tiger.[(triple3)] The rabbit does not chase the tiger.[(triple4)] The rabbit is big.[(triple5)] The rabbit likes the tiger.[(triple6)] The tiger is not big.[(triple7)] @1: The mouse is blue.[(((triple3) -> rule1))] The mouse is rough.[(((triple3) -> rule8))] The rabbit is blue.[(((triple6) -> rule1))] The rabbit is rough.[(((triple6) -> rule8))] @2: The mouse is cold.[(((((triple3) -> rule8)) -> rule3))] The rabbit is cold.[(((((triple6) -> rule8)) -> rule3))] @3: The mouse chases the lion.[(((((((triple3) -> rule8)) -> rule3)) -> rule5))] The mouse is young.[(((((((triple3) -> rule8)) -> rule3)) -> rule7))] The rabbit chases the lion.[(((((((triple6) -> rule8)) -> rule3)) -> rule5))] The rabbit is young.[(((((((triple6) -> rule8)) -> rule3)) -> rule7))] @4: The mouse eats the mouse.[(((((((((triple3) -> rule8)) -> rule3)) -> rule7)) -> rule2))] The rabbit eats the mouse.[(((((((((triple6) -> rule8)) -> rule3)) -> rule7)) -> rule2))] @5: The mouse does not like the mouse.[(((((triple3) -> rule8) ((((((((triple3) -> rule8)) -> rule3)) -> rule7)) -> rule2)) -> rule4))] The rabbit does not like the mouse.[(((((triple6) -> rule8) ((((((((triple6) -> rule8)) -> rule3)) -> rule7)) -> rule2)) -> rule4))]
The lion eats the mouse.
("lion" "eats" "mouse" "+")
triple1
The mouse is big.
("mouse" "is" "big" "+")
triple2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple3
The rabbit does not chase the tiger.
("rabbit" "chases" "tiger" "-")
triple4
The rabbit is big.
("rabbit" "is" "big" "+")
triple5
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple6
The tiger is not big.
("tiger" "is" "big" "-")
triple7
The mouse is blue.
("mouse" "is" "blue" "+")
((triple3) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
((triple3) -> (rule8 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
((triple6) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
((triple6) -> (rule8 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
((((triple3) -> (rule8 % int2))) -> (rule3 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
((((triple6) -> (rule8 % int2))) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
((((((triple3) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The mouse is young.
("mouse" "is" "young" "+")
((((((triple3) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
((((((triple6) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
int3
The rabbit is young.
("rabbit" "is" "young" "+")
((((((triple6) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
int3
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((((((((triple3) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
int4
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
((((((((triple6) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3
The rabbit is rough.
("rabbit" "is" "rough" "+")
int4
The mouse does not like the mouse.
("mouse" "likes" "mouse" "-")
((((triple3) -> (rule8 % int5)) ((((((((triple3) -> (rule8 % int5))) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The mouse does not like the mouse.
("mouse" "likes" "mouse" "-")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The mouse is cold.
("mouse" "is" "cold" "+")
int4
The mouse is rough.
("mouse" "is" "rough" "+")
int5
The rabbit does not like the mouse.
("rabbit" "likes" "mouse" "-")
((((triple6) -> (rule8 % int5)) ((((((((triple6) -> (rule8 % int5))) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit does not like the mouse.
("rabbit" "likes" "mouse" "-")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
int3
The rabbit is cold.
("rabbit" "is" "cold" "+")
int4
The rabbit is rough.
("rabbit" "is" "rough" "+")
int5