The bear is green. The squirrel visits the bear. If the squirrel visits the bear then the squirrel likes the bear. If the squirrel visits the bear and the squirrel likes the bear then the bear visits the squirrel. If something visits the bear then the bear does not chase the squirrel. If something chases the squirrel then it is rough. If something visits the squirrel then the squirrel visits the bear. If something likes the bear and it does not chase the squirrel then the bear likes the squirrel.
The bear is green.
("bear" "is" "green" "+")
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
If the squirrel visits the bear then the squirrel likes the bear.
((("squirrel" "visits" "bear" "+")) -> ("squirrel" "likes" "bear" "+"))
If the squirrel visits the bear and the squirrel likes the bear then the bear visits the squirrel.
((("squirrel" "visits" "bear" "+") ("squirrel" "likes" "bear" "+")) -> ("bear" "visits" "squirrel" "+"))
If something visits the bear then the bear does not chase the squirrel.
((("something" "visits" "bear" "+")) -> ("bear" "chases" "squirrel" "-"))
If something chases the squirrel then it is rough.
((("something" "chases" "squirrel" "+")) -> ("something" "is" "rough" "+"))
If something visits the squirrel then the squirrel visits the bear.
((("something" "visits" "squirrel" "+")) -> ("squirrel" "visits" "bear" "+"))
If something likes the bear and it does not chase the squirrel then the bear likes the squirrel.
((("something" "likes" "bear" "+") ("something" "chases" "squirrel" "~")) -> ("bear" "likes" "squirrel" "+"))
The squirrel visits the bear.
True
1
proof
[(triple2)]
("squirrel" "visits" "bear" "+")
triple2
The bear is not green.
False
1
inv-proof
[(triple1)]
("bear" "is" "green" "-")
triple1
The squirrel likes the bear.
True
2
proof
[(((triple2) -> rule1))]
("squirrel" "likes" "bear" "+")
((triple2) -> (rule1 % int1))
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int1
The bear chases the squirrel.
False
2
inv-proof
[(((triple2) -> rule3))]
("bear" "chases" "squirrel" "+")
((triple2) -> (rule3 % int1))
The bear does not chase the squirrel.
("bear" "chases" "squirrel" "-")
int1
The bear visits the squirrel.
True
4
proof
[(((triple2 ((triple2) -> rule1)) -> rule2))]
("bear" "visits" "squirrel" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int1
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int2
The bear does not visit the squirrel.
False
4
inv-proof
[(((triple2 ((triple2) -> rule1)) -> rule2))]
("bear" "visits" "squirrel" "-")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int1
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int2
The squirrel is not rough.
Unknown
inv-rconc
[@1: The squirrel is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "is" "rough" "-")
The bear likes the squirrel.
Unknown
rconc
[@1: The bear likes the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "likes" "squirrel" "+")
The bear is not rough.
Unknown
inv-rconc
[@1: The bear is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "is" "rough" "-")
The squirrel is blue.
Unknown
random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
@0: The bear is green.[(triple1)] The squirrel visits the bear.[(triple2)] @1: The bear does not chase the squirrel.[(((triple2) -> rule3))] The squirrel likes the bear.[(((triple2) -> rule1))] @2: The bear visits the squirrel.[(((triple2 ((triple2) -> rule1)) -> rule2))]
The bear is green.
("bear" "is" "green" "+")
triple1
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
triple2
The bear does not chase the squirrel.
("bear" "chases" "squirrel" "-")
((triple2) -> (rule3 % int1))
The bear does not chase the squirrel.
("bear" "chases" "squirrel" "-")
int1
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
((triple2) -> (rule1 % int1))
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int1
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int1
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int2