The bear is cold. The bear is rough. The bear needs the tiger. The bear visits the rabbit. The bear visits the tiger. The mouse is nice. The mouse is rough. The mouse needs the tiger. The rabbit is cold. The rabbit is red. The rabbit needs the mouse. The rabbit needs the tiger. The tiger eats the mouse. The tiger needs the rabbit. The tiger visits the rabbit. If something eats the tiger then it needs the bear. If something eats the tiger then the tiger eats the mouse. If something needs the rabbit then it eats the mouse. If something visits the tiger then it visits the mouse. If something is cold and round then it visits the bear. If something eats the tiger then the tiger needs the rabbit. If the mouse eats the tiger and the mouse is cold then the tiger visits the bear. If something visits the mouse then the mouse needs the rabbit.
The bear is cold.
("bear" "is" "cold" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear needs the tiger.
("bear" "needs" "tiger" "+")
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If something eats the tiger then it needs the bear.
((("something" "eats" "tiger" "+")) -> ("something" "needs" "bear" "+"))
If something eats the tiger then the tiger eats the mouse.
((("something" "eats" "tiger" "+")) -> ("tiger" "eats" "mouse" "+"))
If something needs the rabbit then it eats the mouse.
((("something" "needs" "rabbit" "+")) -> ("something" "eats" "mouse" "+"))
If something visits the tiger then it visits the mouse.
((("something" "visits" "tiger" "+")) -> ("something" "visits" "mouse" "+"))
If something is cold and round then it visits the bear.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "visits" "bear" "+"))
If something eats the tiger then the tiger needs the rabbit.
((("something" "eats" "tiger" "+")) -> ("tiger" "needs" "rabbit" "+"))
If the mouse eats the tiger and the mouse is cold then the tiger visits the bear.
((("mouse" "eats" "tiger" "+") ("mouse" "is" "cold" "+")) -> ("tiger" "visits" "bear" "+"))
If something visits the mouse then the mouse needs the rabbit.
((("something" "visits" "mouse" "+")) -> ("mouse" "needs" "rabbit" "+"))
The bear is rough.
True
1
proof
[(triple2)]
("bear" "is" "rough" "+")
triple2
The mouse is not rough.
False
1
inv-proof
[(triple7)]
("mouse" "is" "rough" "-")
triple7
The bear visits the mouse.
True
2
proof
[(((triple5) -> rule4))]
("bear" "visits" "mouse" "+")
((triple5) -> (rule4 % int1))
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int1
The bear does not visit the mouse.
False
2
inv-proof
[(((triple5) -> rule4))]
("bear" "visits" "mouse" "-")
((triple5) -> (rule4 % int1))
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int1
The mouse needs the rabbit.
True
3
proof
[(((((triple5) -> rule4)) -> rule8))]
("mouse" "needs" "rabbit" "+")
((((triple5) -> (rule4 % int2))) -> (rule8 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int2
The mouse does not need the rabbit.
False
3
inv-proof
[(((((triple5) -> rule4)) -> rule8))]
("mouse" "needs" "rabbit" "-")
((((triple5) -> (rule4 % int2))) -> (rule8 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int2
The mouse eats the mouse.
True
4
proof
[(((((((triple5) -> rule4)) -> rule8)) -> rule3))]
("mouse" "eats" "mouse" "+")
((((((triple5) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int2
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int3
The mouse does not eat the mouse.
False
4
inv-proof
[(((((((triple5) -> rule4)) -> rule8)) -> rule3))]
("mouse" "eats" "mouse" "-")
((((((triple5) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int2
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int3
The tiger does not visit the bear.
Unknown
inv-rconc
[@1: The tiger visits the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "visits" "bear" "-")
The bear needs the bear.
Unknown
rconc
[@1: The bear needs the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "needs" "bear" "+")
The bear does not visit the bear.
Unknown
inv-rconc
[@1: The bear visits the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "visits" "bear" "-")
The mouse visits the mouse.
Unknown
rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "visits" "mouse" "+")
The bear does not eat the rabbit.
Unknown
inv-random
[@0: The bear eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "rabbit" "-")
The rabbit visits the tiger.
Unknown
random
[@0: The rabbit visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "tiger" "+")
The tiger is not nice.
Unknown
inv-random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "-")
The bear needs the rabbit.
Unknown
random
[@0: The bear needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "rabbit" "+")
@0: The bear is cold.[(triple1)] The bear is rough.[(triple2)] The bear needs the tiger.[(triple3)] The bear visits the rabbit.[(triple4)] The bear visits the tiger.[(triple5)] The mouse is nice.[(triple6)] The mouse is rough.[(triple7)] The mouse needs the tiger.[(triple8)] The rabbit is cold.[(triple9)] The rabbit is red.[(triple10)] The rabbit needs the mouse.[(triple11)] The rabbit needs the tiger.[(triple12)] The tiger eats the mouse.[(triple13 OR ((triple14) -> rule3))] The tiger needs the rabbit.[(triple14)] The tiger visits the rabbit.[(triple15)] @1: The bear visits the mouse.[(((triple5) -> rule4))] @2: The mouse needs the rabbit.[(((((triple5) -> rule4)) -> rule8))] @3: The mouse eats the mouse.[(((((((triple5) -> rule4)) -> rule8)) -> rule3))]
The bear is cold.
("bear" "is" "cold" "+")
triple1
The bear is rough.
("bear" "is" "rough" "+")
triple2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
triple3
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple4
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple5
The mouse is nice.
("mouse" "is" "nice" "+")
triple6
The mouse is rough.
("mouse" "is" "rough" "+")
triple7
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple8
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple9
The rabbit is red.
("rabbit" "is" "red" "+")
triple10
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple11
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple12
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple13
((triple14) -> (rule3 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple14
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple15
The bear visits the mouse.
("bear" "visits" "mouse" "+")
((triple5) -> (rule4 % int1))
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
((((triple5) -> (rule4 % int2))) -> (rule8 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int2
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((((((triple5) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int2
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int3