The bear chases the squirrel. The bear eats the squirrel. The bear is rough. The bear does not need the squirrel. The rabbit chases the bear. The rabbit is green. The rabbit is not red. The rabbit needs the bear. The squirrel is rough. The squirrel needs the rabbit. If the rabbit chases the bear then the bear is big. If something eats the bear then the bear does not need the rabbit. If something is green and not rough then it does not chase the rabbit. If the bear is blue then the bear eats the rabbit. If something is red then it is blue. If something chases the bear and the bear is big then the bear is blue. If something is blue then it needs the rabbit. All big things are red.
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear does not need the squirrel.
("bear" "needs" "squirrel" "-")
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is not red.
("rabbit" "is" "red" "-")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
If the rabbit chases the bear then the bear is big.
((("rabbit" "chases" "bear" "+")) -> ("bear" "is" "big" "+"))
If something eats the bear then the bear does not need the rabbit.
((("something" "eats" "bear" "+")) -> ("bear" "needs" "rabbit" "-"))
If something is green and not rough then it does not chase the rabbit.
((("something" "is" "green" "+") ("something" "is" "rough" "~")) -> ("something" "chases" "rabbit" "-"))
If the bear is blue then the bear eats the rabbit.
((("bear" "is" "blue" "+")) -> ("bear" "eats" "rabbit" "+"))
If something is red then it is blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
If something chases the bear and the bear is big then the bear is blue.
((("something" "chases" "bear" "+") ("bear" "is" "big" "+")) -> ("bear" "is" "blue" "+"))
If something is blue then it needs the rabbit.
((("something" "is" "blue" "+")) -> ("something" "needs" "rabbit" "+"))
All big things are red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
The rabbit is not red.
True
1
proof
[(triple7)]
("rabbit" "is" "red" "-")
triple7
The squirrel does not need the rabbit.
False
1
inv-proof
[(triple10)]
("squirrel" "needs" "rabbit" "-")
triple10
The bear is big.
True
2
proof
[(((triple5) -> rule1))]
("bear" "is" "big" "+")
((triple5) -> (rule1 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is not big.
False
2
inv-proof
[(((triple5) -> rule1))]
("bear" "is" "big" "-")
((triple5) -> (rule1 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is red.
True
3
proof
[(((((triple5) -> rule1)) -> rule8))]
("bear" "is" "red" "+")
((((triple5) -> (rule1 % int2))) -> (rule8 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The bear is not blue.
False
4
inv-proof
[(((triple5 ((triple5) -> rule1)) -> rule6) OR ((((((triple5) -> rule1)) -> rule8)) -> rule5))]
("bear" "is" "blue" "-")
((triple5 ((triple5) -> (rule1 % int2))) -> (rule6 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
((((((triple5) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is big.
("bear" "is" "big" "+")
int3
The bear eats the rabbit.
True
5
proof
[(((((triple5 ((triple5) -> rule1)) -> rule6)) -> rule4) OR ((((((((triple5) -> rule1)) -> rule8)) -> rule5)) -> rule4))]
("bear" "eats" "rabbit" "+")
((((triple5 ((triple5) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The bear is big.
("bear" "is" "big" "+")
int3
((((((((triple5) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The bear is big.
("bear" "is" "big" "+")
int4
The bear does not need the rabbit.
False
5
inv-proof
[(((((triple5 ((triple5) -> rule1)) -> rule6)) -> rule7) OR ((((((((triple5) -> rule1)) -> rule8)) -> rule5)) -> rule7))]
("bear" "needs" "rabbit" "-")
((((triple5 ((triple5) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The bear is big.
("bear" "is" "big" "+")
int3
((((((((triple5) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The bear is big.
("bear" "is" "big" "+")
int4
The squirrel is not red.
Unknown
inv-rconc
[@1: The squirrel is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "is" "red" "-")
The rabbit is blue.
Unknown
rconc
[@1: The rabbit is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "is" "blue" "+")
The rabbit does not need the rabbit.
Unknown
inv-rconc
[@2: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("rabbit" "needs" "rabbit" "-")
The squirrel is blue.
Unknown
rconc
[@2: The squirrel is blue.[CWA. Example of deepest failure = (rule5 <- rule8 <- FAIL)]]
("squirrel" "is" "blue" "+")
The bear is not green.
Unknown
inv-random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
The bear does not chase the rabbit.
Unknown
inv-random
[@0: The bear chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "rabbit" "-")
The squirrel eats the bear.
Unknown
random
[@0: The squirrel eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "bear" "+")
@0: The bear chases the squirrel.[(triple1)] The bear does not need the squirrel.[(triple4)] The bear eats the squirrel.[(triple2)] The bear is rough.[(triple3)] The rabbit chases the bear.[(triple5)] The rabbit is green.[(triple6)] The rabbit is not red.[(triple7)] The rabbit needs the bear.[(triple8)] The squirrel is rough.[(triple9)] The squirrel needs the rabbit.[(triple10)] @1: The bear is big.[(((triple5) -> rule1))] @2: The bear is blue.[(((triple5 ((triple5) -> rule1)) -> rule6) OR ((((((triple5) -> rule1)) -> rule8)) -> rule5))] The bear is red.[(((((triple5) -> rule1)) -> rule8))] @3: The bear eats the rabbit.[(((((triple5 ((triple5) -> rule1)) -> rule6)) -> rule4) OR ((((((((triple5) -> rule1)) -> rule8)) -> rule5)) -> rule4))] The bear needs the rabbit.[(((((triple5 ((triple5) -> rule1)) -> rule6)) -> rule7) OR ((((((((triple5) -> rule1)) -> rule8)) -> rule5)) -> rule7))]
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
triple1
The bear does not need the squirrel.
("bear" "needs" "squirrel" "-")
triple4
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
triple2
The bear is rough.
("bear" "is" "rough" "+")
triple3
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
triple5
The rabbit is green.
("rabbit" "is" "green" "+")
triple6
The rabbit is not red.
("rabbit" "is" "red" "-")
triple7
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple8
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple9
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple10
The bear is big.
("bear" "is" "big" "+")
((triple5) -> (rule1 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
((triple5 ((triple5) -> (rule1 % int2))) -> (rule6 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
((((((triple5) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is big.
("bear" "is" "big" "+")
int3
The bear is red.
("bear" "is" "red" "+")
((((triple5) -> (rule1 % int2))) -> (rule8 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
((((triple5 ((triple5) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The bear is big.
("bear" "is" "big" "+")
int3
((((((((triple5) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The bear is big.
("bear" "is" "big" "+")
int4
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
((((triple5 ((triple5) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The bear is big.
("bear" "is" "big" "+")
int3
((((((((triple5) -> (rule1 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The bear is big.
("bear" "is" "big" "+")
int4