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