The bear is kind. The mouse chases the tiger. The rabbit likes the tiger. The tiger visits the bear. If the bear is green and the bear likes the mouse then the mouse visits the bear. If something visits the mouse and the mouse chases the rabbit then the mouse is kind. If something is kind then it likes the mouse. If something visits the bear and the bear likes the mouse then the bear likes the tiger. If something likes the tiger then the tiger likes the rabbit. If something is cold and it visits the rabbit then it chases the bear. If the mouse visits the rabbit and the rabbit is green then the rabbit is cold. If something likes the rabbit then the rabbit is kind.
The bear is kind.
("bear" "is" "kind" "+")
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
If the bear is green and the bear likes the mouse then the mouse visits the bear.
((("bear" "is" "green" "+") ("bear" "likes" "mouse" "+")) -> ("mouse" "visits" "bear" "+"))
If something visits the mouse and the mouse chases the rabbit then the mouse is kind.
((("something" "visits" "mouse" "+") ("mouse" "chases" "rabbit" "+")) -> ("mouse" "is" "kind" "+"))
If something is kind then it likes the mouse.
((("something" "is" "kind" "+")) -> ("something" "likes" "mouse" "+"))
If something visits the bear and the bear likes the mouse then the bear likes the tiger.
((("something" "visits" "bear" "+") ("bear" "likes" "mouse" "+")) -> ("bear" "likes" "tiger" "+"))
If something likes the tiger then the tiger likes the rabbit.
((("something" "likes" "tiger" "+")) -> ("tiger" "likes" "rabbit" "+"))
If something is cold and it visits the rabbit then it chases the bear.
((("something" "is" "cold" "+") ("something" "visits" "rabbit" "+")) -> ("something" "chases" "bear" "+"))
If the mouse visits the rabbit and the rabbit is green then the rabbit is cold.
((("mouse" "visits" "rabbit" "+") ("rabbit" "is" "green" "+")) -> ("rabbit" "is" "cold" "+"))
If something likes the rabbit then the rabbit is kind.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "is" "kind" "+"))
The tiger visits the bear.
True
1
proof
[(triple4)]
("tiger" "visits" "bear" "+")
triple4
The rabbit does not like the tiger.
False
1
inv-proof
[(triple3)]
("rabbit" "likes" "tiger" "-")
triple3
The bear likes the mouse.
True
2
proof
[(((triple1) -> rule3))]
("bear" "likes" "mouse" "+")
((triple1) -> (rule3 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The bear does not like the mouse.
False
2
inv-proof
[(((triple1) -> rule3))]
("bear" "likes" "mouse" "-")
((triple1) -> (rule3 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The rabbit is kind.
True
3
proof
[(((((triple3) -> rule5)) -> rule8) OR ((((((triple4 ((triple1) -> rule3)) -> rule4)) -> rule5)) -> rule8))]
("rabbit" "is" "kind" "+")
((((triple3) -> (rule5 % int2))) -> (rule8 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int2
((((((triple4 ((triple1) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int2
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int3
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int4
The rabbit is not kind.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule8) OR ((((((triple4 ((triple1) -> rule3)) -> rule4)) -> rule5)) -> rule8))]
("rabbit" "is" "kind" "-")
((((triple3) -> (rule5 % int2))) -> (rule8 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int2
((((((triple4 ((triple1) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int2
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int3
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int4
The rabbit does not chase the bear.
Unknown
inv-rconc
[@1: The rabbit chases the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "chases" "bear" "-")
The mouse visits the bear.
Unknown
rconc
[@1: The mouse visits the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "visits" "bear" "+")
The mouse is not kind.
Unknown
inv-rconc
[@1: The mouse is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "kind" "-")
The rabbit visits the bear.
Unknown
random
[@0: The rabbit visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "bear" "+")
The rabbit does not visit the tiger.
Unknown
inv-random
[@0: The rabbit visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "tiger" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
@0: The bear is kind.[(triple1)] The mouse chases the tiger.[(triple2)] The rabbit likes the tiger.[(triple3)] The tiger visits the bear.[(triple4)] @1: The bear likes the mouse.[(((triple1) -> rule3))] The tiger likes the rabbit.[(((triple3) -> rule5) OR ((((triple4 ((triple1) -> rule3)) -> rule4)) -> rule5))] @2: The bear likes the tiger.[(((triple4 ((triple1) -> rule3)) -> rule4))] The rabbit is kind.[(((((triple3) -> rule5)) -> rule8) OR ((((((triple4 ((triple1) -> rule3)) -> rule4)) -> rule5)) -> rule8))] @3: The rabbit likes the mouse.[(((((((triple3) -> rule5)) -> rule8)) -> rule3) OR ((((((((triple4 ((triple1) -> rule3)) -> rule4)) -> rule5)) -> rule8)) -> rule3))]
The bear is kind.
("bear" "is" "kind" "+")
triple1
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple2
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple3
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple4
The bear likes the mouse.
("bear" "likes" "mouse" "+")
((triple1) -> (rule3 % int1))
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int1
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
((triple3) -> (rule5 % int1))
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int1
((((triple4 ((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int2
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int3
The bear likes the tiger.
("bear" "likes" "tiger" "+")
((triple4 ((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int2
The rabbit is kind.
("rabbit" "is" "kind" "+")
((((triple3) -> (rule5 % int2))) -> (rule8 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int2
((((((triple4 ((triple1) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int2
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int3
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int4
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
((((((triple3) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int3
((((((((triple4 ((triple1) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int3
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int4
The bear likes the mouse.
("bear" "likes" "mouse" "+")
int5