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