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