The bear likes the tiger. The lion visits the bear. The squirrel is rough. The tiger visits the squirrel. If the squirrel needs the bear then the squirrel needs the lion. If the lion needs the bear then the bear needs the squirrel. If someone likes the lion then they are cold. If someone likes the tiger then they need the bear. If someone visits the squirrel and they visit the bear then they like the bear. If someone needs the bear then the bear is kind.
The bear likes the tiger.
("bear" "likes" "tiger" "+")
The lion visits the bear.
("lion" "visits" "bear" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If the squirrel needs the bear then the squirrel needs the lion.
((("squirrel" "needs" "bear" "+")) -> ("squirrel" "needs" "lion" "+"))
If the lion needs the bear then the bear needs the squirrel.
((("lion" "needs" "bear" "+")) -> ("bear" "needs" "squirrel" "+"))
If someone likes the lion then they are cold.
((("someone" "likes" "lion" "+")) -> ("someone" "is" "cold" "+"))
If someone likes the tiger then they need the bear.
((("someone" "likes" "tiger" "+")) -> ("someone" "needs" "bear" "+"))
If someone visits the squirrel and they visit the bear then they like the bear.
((("someone" "visits" "squirrel" "+") ("someone" "visits" "bear" "+")) -> ("someone" "likes" "bear" "+"))
If someone needs the bear then the bear is kind.
((("someone" "needs" "bear" "+")) -> ("bear" "is" "kind" "+"))
The squirrel is rough.
True
1
proof
[(triple3)]
("squirrel" "is" "rough" "+")
triple3
The squirrel is not rough.
False
1
inv-proof
[(triple3)]
("squirrel" "is" "rough" "-")
triple3
The bear needs the bear.
True
2
proof
[(((triple1) -> rule4))]
("bear" "needs" "bear" "+")
((triple1) -> (rule4 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear does not need the bear.
False
2
inv-proof
[(((triple1) -> rule4))]
("bear" "needs" "bear" "-")
((triple1) -> (rule4 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is kind.
True
3
proof
[(((((triple1) -> rule4)) -> rule6))]
("bear" "is" "kind" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
The bear is not kind.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule6))]
("bear" "is" "kind" "-")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
The bear does not like the bear.
Unknown
inv-rconc
[@1: The bear likes the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "likes" "bear" "-")
The squirrel is cold.
Unknown
rconc
[@1: The squirrel is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "cold" "+")
The tiger does not like the bear.
Unknown
inv-rconc
[@1: The tiger likes the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "likes" "bear" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
The squirrel does not like the squirrel.
Unknown
inv-random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "-")
The bear visits the tiger.
Unknown
random
[@0: The bear visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "tiger" "+")
@0: The bear likes the tiger.[(triple1)] The lion visits the bear.[(triple2)] The squirrel is rough.[(triple3)] The tiger visits the squirrel.[(triple4)] @1: The bear needs the bear.[(((triple1) -> rule4))] @2: The bear is kind.[(((((triple1) -> rule4)) -> rule6))]
The bear likes the tiger.
("bear" "likes" "tiger" "+")
triple1
The lion visits the bear.
("lion" "visits" "bear" "+")
triple2
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple3
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple4
The bear needs the bear.
("bear" "needs" "bear" "+")
((triple1) -> (rule4 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2