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