The bear eats the rabbit. The rabbit is round. The squirrel visits the bear. If someone eats the squirrel then the squirrel chases the bear. If someone chases the squirrel and they eat the bear then they are nice. If someone visits the squirrel then they eat the squirrel. If the bear eats the rabbit and the rabbit eats the bear then the bear is round. If the bear is nice and the bear chases the rabbit then the bear visits the rabbit. If someone visits the bear then the bear visits the squirrel.
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
If someone eats the squirrel then the squirrel chases the bear.
((("someone" "eats" "squirrel" "+")) -> ("squirrel" "chases" "bear" "+"))
If someone chases the squirrel and they eat the bear then they are nice.
((("someone" "chases" "squirrel" "+") ("someone" "eats" "bear" "+")) -> ("someone" "is" "nice" "+"))
If someone visits the squirrel then they eat the squirrel.
((("someone" "visits" "squirrel" "+")) -> ("someone" "eats" "squirrel" "+"))
If the bear eats the rabbit and the rabbit eats the bear then the bear is round.
((("bear" "eats" "rabbit" "+") ("rabbit" "eats" "bear" "+")) -> ("bear" "is" "round" "+"))
If the bear is nice and the bear chases the rabbit then the bear visits the rabbit.
((("bear" "is" "nice" "+") ("bear" "chases" "rabbit" "+")) -> ("bear" "visits" "rabbit" "+"))
If someone visits the bear then the bear visits the squirrel.
((("someone" "visits" "bear" "+")) -> ("bear" "visits" "squirrel" "+"))
The squirrel visits the bear.
True
1
proof
[(triple3)]
("squirrel" "visits" "bear" "+")
triple3
The rabbit is not round.
False
1
inv-proof
[(triple2)]
("rabbit" "is" "round" "-")
triple2
The bear visits the squirrel.
True
2
proof
[(((triple3) -> rule6))]
("bear" "visits" "squirrel" "+")
((triple3) -> (rule6 % int1))
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int1
The bear does not visit the squirrel.
False
2
inv-proof
[(((triple3) -> rule6))]
("bear" "visits" "squirrel" "-")
((triple3) -> (rule6 % int1))
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int1
The bear eats the squirrel.
True
3
proof
[(((((triple3) -> rule6)) -> rule3))]
("bear" "eats" "squirrel" "+")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
int1
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int2
The bear does not eat the squirrel.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule3))]
("bear" "eats" "squirrel" "-")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
int1
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int2
The squirrel chases the bear.
True
4
proof
[(((((((triple3) -> rule6)) -> rule3)) -> rule1))]
("squirrel" "chases" "bear" "+")
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int1
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
int2
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int3
The squirrel does not chase the bear.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule3)) -> rule1))]
("squirrel" "chases" "bear" "-")
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int1
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
int2
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int3
The rabbit is not nice.
Unknown
inv-rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "nice" "-")
The bear is round.
Unknown
rconc
[@1: The bear is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "is" "round" "+")
The bear is not nice.
Unknown
inv-rconc
[@1: The bear is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "nice" "-")
The squirrel is nice.
Unknown
rconc
[@1: The squirrel is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "is" "nice" "+")
The squirrel is not round.
Unknown
inv-random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "-")
The rabbit is big.
Unknown
random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "+")
The rabbit does not visit the squirrel.
Unknown
inv-random
[@0: The rabbit visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "squirrel" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
@0: The bear eats the rabbit.[(triple1)] The rabbit is round.[(triple2)] The squirrel visits the bear.[(triple3)] @1: The bear visits the squirrel.[(((triple3) -> rule6))] @2: The bear eats the squirrel.[(((((triple3) -> rule6)) -> rule3))] @3: The squirrel chases the bear.[(((((((triple3) -> rule6)) -> rule3)) -> rule1))]
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
triple1
The rabbit is round.
("rabbit" "is" "round" "+")
triple2
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
triple3
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
((triple3) -> (rule6 % int1))
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int1
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
int1
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int2
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int1
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
int2
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int3