The lion is red. The lion is young. The lion likes the rabbit. The lion needs the mouse. The mouse eats the lion. The mouse is young. The mouse likes the tiger. The mouse needs the lion. The rabbit is big. The rabbit is red. The rabbit is young. The rabbit needs the mouse. The tiger eats the mouse. The tiger likes the lion. If something eats the tiger then it needs the rabbit. If something eats the tiger then it needs the lion. If something likes the rabbit then it likes the mouse. If the tiger needs the rabbit and the tiger needs the lion then the lion likes the rabbit. All big, rough things are young. If something likes the mouse then it eats the tiger. If something likes the mouse then the mouse likes the rabbit. If something is red then it likes the lion. If something needs the lion and the lion likes the mouse then it is rough.
The lion is red.
("lion" "is" "red" "+")
The lion is young.
("lion" "is" "young" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
If something eats the tiger then it needs the rabbit.
((("something" "eats" "tiger" "+")) -> ("something" "needs" "rabbit" "+"))
If something eats the tiger then it needs the lion.
((("something" "eats" "tiger" "+")) -> ("something" "needs" "lion" "+"))
If something likes the rabbit then it likes the mouse.
((("something" "likes" "rabbit" "+")) -> ("something" "likes" "mouse" "+"))
If the tiger needs the rabbit and the tiger needs the lion then the lion likes the rabbit.
((("tiger" "needs" "rabbit" "+") ("tiger" "needs" "lion" "+")) -> ("lion" "likes" "rabbit" "+"))
All big, rough things are young.
((("something" "is" "big" "+") ("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If something likes the mouse then it eats the tiger.
((("something" "likes" "mouse" "+")) -> ("something" "eats" "tiger" "+"))
If something likes the mouse then the mouse likes the rabbit.
((("something" "likes" "mouse" "+")) -> ("mouse" "likes" "rabbit" "+"))
If something is red then it likes the lion.
((("something" "is" "red" "+")) -> ("something" "likes" "lion" "+"))
If something needs the lion and the lion likes the mouse then it is rough.
((("something" "needs" "lion" "+") ("lion" "likes" "mouse" "+")) -> ("something" "is" "rough" "+"))
The lion likes the rabbit.
True
1
proof
[(triple3)]
("lion" "likes" "rabbit" "+")
triple3
The mouse does not eat the lion.
False
1
inv-proof
[(triple5)]
("mouse" "eats" "lion" "-")
triple5
The rabbit likes the lion.
True
2
proof
[(((triple10) -> rule8))]
("rabbit" "likes" "lion" "+")
((triple10) -> (rule8 % int1))
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int1
The lion does not like the lion.
False
2
inv-proof
[(((triple1) -> rule8))]
("lion" "likes" "lion" "-")
((triple1) -> (rule8 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion eats the tiger.
True
3
proof
[(((((triple3) -> rule3)) -> rule6))]
("lion" "eats" "tiger" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int2
The mouse does not like the rabbit.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule7))]
("mouse" "likes" "rabbit" "-")
((((triple3) -> (rule3 % int2))) -> (rule7 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int2
The mouse likes the mouse.
True
4
proof
[(((((((triple3) -> rule3)) -> rule7)) -> rule3))]
("mouse" "likes" "mouse" "+")
((((((triple3) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int3
The lion does not need the lion.
False
4
inv-proof
[(((((((triple3) -> rule3)) -> rule6)) -> rule2))]
("lion" "needs" "lion" "-")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int3
The mouse eats the tiger.
True
5
proof
[(((((((((triple3) -> rule3)) -> rule7)) -> rule3)) -> rule6))]
("mouse" "eats" "tiger" "+")
((((((((triple3) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int3
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int4
The mouse does not eat the tiger.
False
5
inv-proof
[(((((((((triple3) -> rule3)) -> rule7)) -> rule3)) -> rule6))]
("mouse" "eats" "tiger" "-")
((((((((triple3) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int3
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int4
The mouse needs the rabbit.
True
6
proof
[(((((((((((triple3) -> rule3)) -> rule7)) -> rule3)) -> rule6)) -> rule1))]
("mouse" "needs" "rabbit" "+")
((((((((((triple3) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int3
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int4
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int5
The mouse does not need the rabbit.
False
6
inv-proof
[(((((((((((triple3) -> rule3)) -> rule7)) -> rule3)) -> rule6)) -> rule1))]
("mouse" "needs" "rabbit" "-")
((((((((((triple3) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int3
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int4
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int5
The tiger does not eat the tiger.
Unknown
inv-rconc
[@2: The tiger eats the tiger.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("tiger" "eats" "tiger" "-")
The tiger needs the lion.
Unknown
rconc
[@3: The tiger needs the lion.[CWA. Example of deepest failure = (rule2 <- rule6 <- rule3 <- FAIL)]]
("tiger" "needs" "lion" "+")
The rabbit does not need the rabbit.
Unknown
inv-rconc
[@3: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule3 <- FAIL)]]
("rabbit" "needs" "rabbit" "-")
The tiger likes the mouse.
Unknown
rconc
[@1: The tiger likes the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "likes" "mouse" "+")
The rabbit does not like the mouse.
Unknown
inv-rconc
[@1: The rabbit likes the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "likes" "mouse" "-")
The rabbit is rough.
Unknown
rconc
[@4: The rabbit is rough.[CWA. Example of deepest failure = (rule9 <- rule2 <- rule6 <- rule3 <- FAIL)]]
("rabbit" "is" "rough" "+")
The rabbit is not cold.
Unknown
inv-random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "-")
The tiger eats the rabbit.
Unknown
random
[@0: The tiger eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "rabbit" "+")
The lion is not big.
Unknown
inv-random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
The mouse does not need the tiger.
Unknown
inv-random
[@0: The mouse needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "tiger" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
@0: The lion is red.[(triple1)] The lion is young.[(triple2)] The lion likes the rabbit.[(triple3)] The lion needs the mouse.[(triple4)] The mouse eats the lion.[(triple5)] The mouse is young.[(triple6)] The mouse likes the tiger.[(triple7)] The mouse needs the lion.[(triple8 OR ((((((((((triple3) -> rule3)) -> rule7)) -> rule3)) -> rule6)) -> rule2))] The rabbit is big.[(triple9)] The rabbit is red.[(triple10)] The rabbit is young.[(triple11)] The rabbit needs the mouse.[(triple12)] The tiger eats the mouse.[(triple13)] The tiger likes the lion.[(triple14)] @1: The lion likes the lion.[(((triple1) -> rule8))] The lion likes the mouse.[(((triple3) -> rule3))] The rabbit likes the lion.[(((triple10) -> rule8))] @2: The lion eats the tiger.[(((((triple3) -> rule3)) -> rule6))] The mouse is rough.[(((triple8 ((triple3) -> rule3)) -> rule9) OR ((((((((((((triple3) -> rule3)) -> rule7)) -> rule3)) -> rule6)) -> rule2) ((triple3) -> rule3)) -> rule9))] The mouse likes the rabbit.[(((((triple3) -> rule3)) -> rule7))] @3: The lion needs the lion.[(((((((triple3) -> rule3)) -> rule6)) -> rule2))] The lion needs the rabbit.[(((((((triple3) -> rule3)) -> rule6)) -> rule1))] The mouse likes the mouse.[(((((((triple3) -> rule3)) -> rule7)) -> rule3))] @4: The lion is rough.[(((((((((triple3) -> rule3)) -> rule6)) -> rule2) ((triple3) -> rule3)) -> rule9))] The mouse eats the tiger.[(((((((((triple3) -> rule3)) -> rule7)) -> rule3)) -> rule6))] @5: The mouse needs the rabbit.[(((((((((((triple3) -> rule3)) -> rule7)) -> rule3)) -> rule6)) -> rule1))]
The lion is red.
("lion" "is" "red" "+")
triple1
The lion is young.
("lion" "is" "young" "+")
triple2
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple3
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple4
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple5
The mouse is young.
("mouse" "is" "young" "+")
triple6
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple7
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple8
((((((((((triple3) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int3
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int4
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int5
The rabbit is big.
("rabbit" "is" "big" "+")
triple9
The rabbit is red.
("rabbit" "is" "red" "+")
triple10
The rabbit is young.
("rabbit" "is" "young" "+")
triple11
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple12
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple13
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple14
The lion likes the lion.
("lion" "likes" "lion" "+")
((triple1) -> (rule8 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
((triple3) -> (rule3 % int1))
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int1
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
((triple10) -> (rule8 % int1))
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
((triple8 ((triple3) -> (rule3 % int2))) -> (rule9 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int2
((((((((((((triple3) -> (rule3 % int6))) -> (rule7 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2)) ((triple3) -> (rule3 % int6))) -> (rule9 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int3
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int4
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int5
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int6
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
((((triple3) -> (rule3 % int2))) -> (rule7 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int3
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int3
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((((((triple3) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int3
The lion is rough.
("lion" "is" "rough" "+")
((((((((triple3) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2)) ((triple3) -> (rule3 % int4))) -> (rule9 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int3
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int4
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
((((((((triple3) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int3
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int4
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
((((((((((triple3) -> (rule3 % int5))) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int3
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int4
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int5