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