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