The bear is nice. The bear is rough. The bear visits the squirrel. The squirrel eats the bear. The squirrel is not big. The squirrel is cold. The squirrel is nice. The squirrel is red. The squirrel likes the bear. The squirrel visits the bear. If someone likes the bear and they do not visit the squirrel then they do not like the squirrel. If someone visits the squirrel then they like the squirrel. If someone likes the squirrel then the squirrel is rough. If someone is cold and they visit the squirrel then they do not eat the bear. If someone is red then they like the bear. If the squirrel does not like the bear and the bear does not visit the squirrel then the squirrel visits the bear.
The bear is nice.
("bear" "is" "nice" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
The squirrel is not big.
("squirrel" "is" "big" "-")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
If someone likes the bear and they do not visit the squirrel then they do not like the squirrel.
((("someone" "likes" "bear" "+") ("someone" "visits" "squirrel" "~")) -> ("someone" "likes" "squirrel" "-"))
If someone visits the squirrel then they like the squirrel.
((("someone" "visits" "squirrel" "+")) -> ("someone" "likes" "squirrel" "+"))
If someone likes the squirrel then the squirrel is rough.
((("someone" "likes" "squirrel" "+")) -> ("squirrel" "is" "rough" "+"))
If someone is cold and they visit the squirrel then they do not eat the bear.
((("someone" "is" "cold" "+") ("someone" "visits" "squirrel" "+")) -> ("someone" "eats" "bear" "-"))
If someone is red then they like the bear.
((("someone" "is" "red" "+")) -> ("someone" "likes" "bear" "+"))
If the squirrel does not like the bear and the bear does not visit the squirrel then the squirrel visits the bear.
((("squirrel" "likes" "bear" "~") ("bear" "visits" "squirrel" "~")) -> ("squirrel" "visits" "bear" "+"))
The bear visits the squirrel.
True
1
proof
[(triple3)]
("bear" "visits" "squirrel" "+")
triple3
The squirrel is not red.
False
1
inv-proof
[(triple8)]
("squirrel" "is" "red" "-")
triple8
The bear likes the squirrel.
True
2
proof
[(((triple3) -> rule2))]
("bear" "likes" "squirrel" "+")
((triple3) -> (rule2 % int1))
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int1
The bear does not like the squirrel.
False
2
inv-proof
[(((triple3) -> rule2))]
("bear" "likes" "squirrel" "-")
((triple3) -> (rule2 % int1))
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int1
The squirrel is rough.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("squirrel" "is" "rough" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int2
The squirrel is not rough.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("squirrel" "is" "rough" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int2
The squirrel does not like the squirrel.
Unknown
inv-rconc
[@1: The squirrel likes the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "likes" "squirrel" "-")
The bear likes the bear.
Unknown
rconc
[@1: The bear likes the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "likes" "bear" "+")
The bear is not cold.
Unknown
inv-random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
The bear is not red.
Unknown
inv-random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
@0: The bear is nice.[(triple1)] The bear is rough.[(triple2)] The bear visits the squirrel.[(triple3)] The squirrel eats the bear.[(triple4)] The squirrel is cold.[(triple6)] The squirrel is nice.[(triple7)] The squirrel is not big.[(triple5)] The squirrel is red.[(triple8)] The squirrel likes the bear.[(triple9 OR ((triple8) -> rule5))] The squirrel visits the bear.[(triple10)] @1: The bear likes the squirrel.[(((triple3) -> rule2))] @2: The squirrel is rough.[(((((triple3) -> rule2)) -> rule3))]
The bear is nice.
("bear" "is" "nice" "+")
triple1
The bear is rough.
("bear" "is" "rough" "+")
triple2
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
triple3
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
triple4
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple6
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple7
The squirrel is not big.
("squirrel" "is" "big" "-")
triple5
The squirrel is red.
("squirrel" "is" "red" "+")
triple8
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
triple9
((triple8) -> (rule5 % int1))
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int1
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
triple10
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
((triple3) -> (rule2 % int1))
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int2