The bear chases the rabbit. The lion does not chase the squirrel. The rabbit is round. The squirrel needs the bear. If something is cold then it does not need the rabbit. If something chases the rabbit then the rabbit chases the lion. If something chases the lion then it needs the lion. If something visits the bear then it is not blue. If the rabbit is round then the rabbit visits the bear. If something needs the bear then it chases the lion. If something needs the lion then it is green. If the squirrel does not need the rabbit then the rabbit needs the lion.
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The lion does not chase the squirrel.
("lion" "chases" "squirrel" "-")
The rabbit is round.
("rabbit" "is" "round" "+")
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
If something is cold then it does not need the rabbit.
((("something" "is" "cold" "+")) -> ("something" "needs" "rabbit" "-"))
If something chases the rabbit then the rabbit chases the lion.
((("something" "chases" "rabbit" "+")) -> ("rabbit" "chases" "lion" "+"))
If something chases the lion then it needs the lion.
((("something" "chases" "lion" "+")) -> ("something" "needs" "lion" "+"))
If something visits the bear then it is not blue.
((("something" "visits" "bear" "+")) -> ("something" "is" "blue" "-"))
If the rabbit is round then the rabbit visits the bear.
((("rabbit" "is" "round" "+")) -> ("rabbit" "visits" "bear" "+"))
If something needs the bear then it chases the lion.
((("something" "needs" "bear" "+")) -> ("something" "chases" "lion" "+"))
If something needs the lion then it is green.
((("something" "needs" "lion" "+")) -> ("something" "is" "green" "+"))
If the squirrel does not need the rabbit then the rabbit needs the lion.
((("squirrel" "needs" "rabbit" "~")) -> ("rabbit" "needs" "lion" "+"))
The lion does not chase the squirrel.
True
1
proof
[(triple2)]
("lion" "chases" "squirrel" "-")
triple2
The rabbit is not round.
False
1
inv-proof
[(triple3)]
("rabbit" "is" "round" "-")
triple3
The squirrel chases the lion.
True
2
proof
[(((triple4) -> rule6))]
("squirrel" "chases" "lion" "+")
((triple4) -> (rule6 % int1))
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int1
The squirrel does not chase the lion.
False
2
inv-proof
[(((triple4) -> rule6))]
("squirrel" "chases" "lion" "-")
((triple4) -> (rule6 % int1))
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int1
The squirrel needs the lion.
True
3
proof
[(((((triple4) -> rule6)) -> rule3))]
("squirrel" "needs" "lion" "+")
((((triple4) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int2
The squirrel does not need the lion.
False
3
inv-proof
[(((((triple4) -> rule6)) -> rule3))]
("squirrel" "needs" "lion" "-")
((((triple4) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int2
The rabbit is green.
True
4
proof
[(((((((triple1) -> rule2)) -> rule3)) -> rule7))]
("rabbit" "is" "green" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int2
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int3
The rabbit is not green.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule3)) -> rule7))]
("rabbit" "is" "green" "-")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int2
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int3
The lion is not green.
Unknown
inv-rconc
[@3: The lion is green.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule6 <- FAIL)]]
("lion" "is" "green" "-")
The bear is green.
Unknown
rconc
[@3: The bear is green.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule6 <- FAIL)]]
("bear" "is" "green" "+")
The bear does not chase the lion.
Unknown
inv-rconc
[@1: The bear chases the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "chases" "lion" "-")
The bear needs the lion.
Unknown
rconc
[@2: The bear needs the lion.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("bear" "needs" "lion" "+")
The squirrel does not chase the rabbit.
Unknown
inv-random
[@0: The squirrel chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "rabbit" "-")
The lion needs the rabbit.
Unknown
random
[@0: The lion needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "rabbit" "+")
The lion is not round.
Unknown
inv-random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "-")
The bear is round.
Unknown
random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "+")
@0: The bear chases the rabbit.[(triple1)] The lion does not chase the squirrel.[(triple2)] The rabbit is round.[(triple3)] The squirrel needs the bear.[(triple4)] @1: The rabbit chases the lion.[(((triple1) -> rule2))] The rabbit visits the bear.[(((triple3) -> rule5))] The squirrel chases the lion.[(((triple4) -> rule6))] @2: The rabbit is not blue.[(((((triple3) -> rule5)) -> rule4))] The rabbit needs the lion.[(((((triple1) -> rule2)) -> rule3))] The squirrel needs the lion.[(((((triple4) -> rule6)) -> rule3))] @3: The rabbit is green.[(((((((triple1) -> rule2)) -> rule3)) -> rule7))] The squirrel is green.[(((((((triple4) -> rule6)) -> rule3)) -> rule7))]
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple1
The lion does not chase the squirrel.
("lion" "chases" "squirrel" "-")
triple2
The rabbit is round.
("rabbit" "is" "round" "+")
triple3
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
triple4
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
((triple1) -> (rule2 % int1))
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int1
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
((triple3) -> (rule5 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
((triple4) -> (rule6 % int1))
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int1
The rabbit is not blue.
("rabbit" "is" "blue" "-")
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit is not blue.
("rabbit" "is" "blue" "-")
int1
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int2
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int1
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int2
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
((((triple4) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
int2
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int3
The squirrel is green.
("squirrel" "is" "green" "+")
((((((triple4) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int2
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int3