The mouse is blue. The rabbit is green. The squirrel likes the rabbit. The tiger chases the mouse. If the rabbit is red and the rabbit likes the squirrel then the squirrel chases the tiger. If the rabbit is red then the rabbit is round. If something chases the tiger and the tiger is big then it is green. If the rabbit likes the mouse then the mouse is round. If something visits the squirrel and it chases the tiger then the squirrel chases the tiger. If something is big then it likes the mouse. If something likes the rabbit then the rabbit visits the tiger. If something visits the tiger then it is red.
The mouse is blue.
("mouse" "is" "blue" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
If the rabbit is red and the rabbit likes the squirrel then the squirrel chases the tiger.
((("rabbit" "is" "red" "+") ("rabbit" "likes" "squirrel" "+")) -> ("squirrel" "chases" "tiger" "+"))
If the rabbit is red then the rabbit is round.
((("rabbit" "is" "red" "+")) -> ("rabbit" "is" "round" "+"))
If something chases the tiger and the tiger is big then it is green.
((("something" "chases" "tiger" "+") ("tiger" "is" "big" "+")) -> ("something" "is" "green" "+"))
If the rabbit likes the mouse then the mouse is round.
((("rabbit" "likes" "mouse" "+")) -> ("mouse" "is" "round" "+"))
If something visits the squirrel and it chases the tiger then the squirrel chases the tiger.
((("something" "visits" "squirrel" "+") ("something" "chases" "tiger" "+")) -> ("squirrel" "chases" "tiger" "+"))
If something is big then it likes the mouse.
((("something" "is" "big" "+")) -> ("something" "likes" "mouse" "+"))
If something likes the rabbit then the rabbit visits the tiger.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "visits" "tiger" "+"))
If something visits the tiger then it is red.
((("something" "visits" "tiger" "+")) -> ("something" "is" "red" "+"))
The rabbit is green.
True
1
proof
[(triple2)]
("rabbit" "is" "green" "+")
triple2
The tiger does not chase the mouse.
False
1
inv-proof
[(triple4)]
("tiger" "chases" "mouse" "-")
triple4
The rabbit visits the tiger.
True
2
proof
[(((triple3) -> rule7))]
("rabbit" "visits" "tiger" "+")
((triple3) -> (rule7 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The rabbit does not visit the tiger.
False
2
inv-proof
[(((triple3) -> rule7))]
("rabbit" "visits" "tiger" "-")
((triple3) -> (rule7 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The rabbit is red.
True
3
proof
[(((((triple3) -> rule7)) -> rule8))]
("rabbit" "is" "red" "+")
((((triple3) -> (rule7 % int2))) -> (rule8 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int2
The rabbit is not red.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule8))]
("rabbit" "is" "red" "-")
((((triple3) -> (rule7 % int2))) -> (rule8 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int2
The rabbit is round.
True
4
proof
[(((((((triple3) -> rule7)) -> rule8)) -> rule2))]
("rabbit" "is" "round" "+")
((((((triple3) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int3
The rabbit is not round.
False
4
inv-proof
[(((((((triple3) -> rule7)) -> rule8)) -> rule2))]
("rabbit" "is" "round" "-")
((((((triple3) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int3
The mouse is not round.
Unknown
inv-rconc
[@2: The mouse is round.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("mouse" "is" "round" "-")
The mouse likes the mouse.
Unknown
rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "likes" "mouse" "+")
The squirrel is not red.
Unknown
inv-rconc
[@1: The squirrel is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "is" "red" "-")
The tiger is green.
Unknown
rconc
[@1: The tiger is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "green" "+")
The rabbit does not chase the mouse.
Unknown
inv-random
[@0: The rabbit chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "mouse" "-")
The rabbit is blue.
Unknown
random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "+")
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The tiger likes the rabbit.
Unknown
random
[@0: The tiger likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "rabbit" "+")
@0: The mouse is blue.[(triple1)] The rabbit is green.[(triple2)] The squirrel likes the rabbit.[(triple3)] The tiger chases the mouse.[(triple4)] @1: The rabbit visits the tiger.[(((triple3) -> rule7))] @2: The rabbit is red.[(((((triple3) -> rule7)) -> rule8))] @3: The rabbit is round.[(((((((triple3) -> rule7)) -> rule8)) -> rule2))]
The mouse is blue.
("mouse" "is" "blue" "+")
triple1
The rabbit is green.
("rabbit" "is" "green" "+")
triple2
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
triple3
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple4
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
((triple3) -> (rule7 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
((((triple3) -> (rule7 % int2))) -> (rule8 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
((((((triple3) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int3