The bear does not chase the squirrel. The bear is big. The bear does not visit the squirrel. The cow chases the bear. The cow is big. The cow visits the squirrel. The squirrel chases the bear. The squirrel is red. The squirrel is round. The squirrel sees the cow. The squirrel visits the bear. The squirrel visits the cow. If someone visits the squirrel then the squirrel chases the cow. If someone chases the cow then they see the squirrel.
The bear does not chase the squirrel.
("bear" "chases" "squirrel" "-")
The bear is big.
("bear" "is" "big" "+")
The bear does not visit the squirrel.
("bear" "visits" "squirrel" "-")
The cow chases the bear.
("cow" "chases" "bear" "+")
The cow is big.
("cow" "is" "big" "+")
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
If someone visits the squirrel then the squirrel chases the cow.
((("someone" "visits" "squirrel" "+")) -> ("squirrel" "chases" "cow" "+"))
If someone chases the cow then they see the squirrel.
((("someone" "chases" "cow" "+")) -> ("someone" "sees" "squirrel" "+"))
The squirrel visits the cow.
True
1
proof
[(triple12)]
("squirrel" "visits" "cow" "+")
triple12
The cow does not visit the squirrel.
False
1
inv-proof
[(triple6)]
("cow" "visits" "squirrel" "-")
triple6
The squirrel chases the cow.
True
2
proof
[(((triple6) -> rule1))]
("squirrel" "chases" "cow" "+")
((triple6) -> (rule1 % int1))
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int1
The squirrel does not chase the cow.
False
2
inv-proof
[(((triple6) -> rule1))]
("squirrel" "chases" "cow" "-")
((triple6) -> (rule1 % int1))
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int1
The squirrel sees the squirrel.
True
3
proof
[(((((triple6) -> rule1)) -> rule2))]
("squirrel" "sees" "squirrel" "+")
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int2
The squirrel does not see the squirrel.
False
3
inv-proof
[(((((triple6) -> rule1)) -> rule2))]
("squirrel" "sees" "squirrel" "-")
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int2
The bear does not see the squirrel.
Unknown
inv-rconc
[@1: The bear sees the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "sees" "squirrel" "-")
The cow sees the squirrel.
Unknown
rconc
[@1: The cow sees the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "sees" "squirrel" "+")
The bear does not chase the cow.
Unknown
inv-random
[@0: The bear chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "cow" "-")
The bear is round.
Unknown
random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "+")
The cow is not cold.
Unknown
inv-random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "-")
The cow visits the bear.
Unknown
random
[@0: The cow visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "bear" "+")
@0: The bear does not chase the squirrel.[(triple1)] The bear does not visit the squirrel.[(triple3)] The bear is big.[(triple2)] The cow chases the bear.[(triple4)] The cow is big.[(triple5)] The cow visits the squirrel.[(triple6)] The squirrel chases the bear.[(triple7)] The squirrel is red.[(triple8)] The squirrel is round.[(triple9)] The squirrel sees the cow.[(triple10)] The squirrel visits the bear.[(triple11)] The squirrel visits the cow.[(triple12)] @1: The squirrel chases the cow.[(((triple6) -> rule1))] @2: The squirrel sees the squirrel.[(((((triple6) -> rule1)) -> rule2))]
The bear does not chase the squirrel.
("bear" "chases" "squirrel" "-")
triple1
The bear does not visit the squirrel.
("bear" "visits" "squirrel" "-")
triple3
The bear is big.
("bear" "is" "big" "+")
triple2
The cow chases the bear.
("cow" "chases" "bear" "+")
triple4
The cow is big.
("cow" "is" "big" "+")
triple5
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
triple6
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
triple7
The squirrel is red.
("squirrel" "is" "red" "+")
triple8
The squirrel is round.
("squirrel" "is" "round" "+")
triple9
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
triple10
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
triple11
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple12
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
((triple6) -> (rule1 % int1))
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
int2