The bear needs the tiger. The bear does not visit the squirrel. The squirrel chases the bear. The squirrel chases the tiger. The squirrel needs the bear. The tiger needs the bear. The tiger visits the squirrel. If the squirrel chases the bear then the bear chases the squirrel. If someone needs the bear and they are not cold then the bear chases the squirrel. If someone needs the tiger then they visit the tiger. If someone needs the tiger and they chase the squirrel then the squirrel is red. If someone needs the bear then the bear needs the tiger. If the tiger chases the squirrel and the tiger is red then the squirrel needs the tiger. If someone needs the squirrel and the squirrel visits the bear then the bear chases the tiger. If the bear is kind and the bear needs the squirrel then the squirrel needs the bear.
The bear needs the tiger.
("bear" "needs" "tiger" "+")
The bear does not visit the squirrel.
("bear" "visits" "squirrel" "-")
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If the squirrel chases the bear then the bear chases the squirrel.
((("squirrel" "chases" "bear" "+")) -> ("bear" "chases" "squirrel" "+"))
If someone needs the bear and they are not cold then the bear chases the squirrel.
((("someone" "needs" "bear" "+") ("someone" "is" "cold" "~")) -> ("bear" "chases" "squirrel" "+"))
If someone needs the tiger then they visit the tiger.
((("someone" "needs" "tiger" "+")) -> ("someone" "visits" "tiger" "+"))
If someone needs the tiger and they chase the squirrel then the squirrel is red.
((("someone" "needs" "tiger" "+") ("someone" "chases" "squirrel" "+")) -> ("squirrel" "is" "red" "+"))
If someone needs the bear then the bear needs the tiger.
((("someone" "needs" "bear" "+")) -> ("bear" "needs" "tiger" "+"))
If the tiger chases the squirrel and the tiger is red then the squirrel needs the tiger.
((("tiger" "chases" "squirrel" "+") ("tiger" "is" "red" "+")) -> ("squirrel" "needs" "tiger" "+"))
If someone needs the squirrel and the squirrel visits the bear then the bear chases the tiger.
((("someone" "needs" "squirrel" "+") ("squirrel" "visits" "bear" "+")) -> ("bear" "chases" "tiger" "+"))
If the bear is kind and the bear needs the squirrel then the squirrel needs the bear.
((("bear" "is" "kind" "+") ("bear" "needs" "squirrel" "+")) -> ("squirrel" "needs" "bear" "+"))
The bear does not visit the squirrel.
True
1
proof
[(triple2)]
("bear" "visits" "squirrel" "-")
triple2
The squirrel does not chase the bear.
False
1
inv-proof
[(triple3)]
("squirrel" "chases" "bear" "-")
triple3
The bear visits the tiger.
True
2
proof
[(((triple1) -> rule3) OR ((((triple5) -> rule5)) -> rule3) OR ((((triple6) -> rule5)) -> rule3))]
("bear" "visits" "tiger" "+")
((triple1) -> (rule3 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
((((triple5) -> (rule5 % int2))) -> (rule3 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
((((triple6) -> (rule5 % int2))) -> (rule3 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The bear does not chase the squirrel.
False
2
inv-proof
[(((triple3) -> rule1))]
("bear" "chases" "squirrel" "-")
((triple3) -> (rule1 % int1))
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int1
The squirrel is red.
True
4
proof
[(((triple1 ((triple3) -> rule1)) -> rule4) OR ((((triple5) -> rule5) ((triple3) -> rule1)) -> rule4) OR ((((triple6) -> rule5) ((triple3) -> rule1)) -> rule4))]
("squirrel" "is" "red" "+")
((triple1 ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int2
((((triple5) -> (rule5 % int3)) ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int3
((((triple6) -> (rule5 % int3)) ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int3
The squirrel is not red.
False
4
inv-proof
[(((triple1 ((triple3) -> rule1)) -> rule4) OR ((((triple5) -> rule5) ((triple3) -> rule1)) -> rule4) OR ((((triple6) -> rule5) ((triple3) -> rule1)) -> rule4))]
("squirrel" "is" "red" "-")
((triple1 ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int2
((((triple5) -> (rule5 % int3)) ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int3
((((triple6) -> (rule5 % int3)) ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int3
The tiger does not visit the tiger.
Unknown
inv-rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "visits" "tiger" "-")
The squirrel needs the tiger.
Unknown
rconc
[@1: The squirrel needs the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "needs" "tiger" "+")
The bear does not chase the tiger.
Unknown
inv-rconc
[@1: The bear chases the tiger.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "chases" "tiger" "-")
The tiger chases the bear.
Unknown
random
[@0: The tiger chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "bear" "+")
The squirrel does not visit the bear.
Unknown
inv-random
[@0: The squirrel visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "bear" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
@0: The bear does not visit the squirrel.[(triple2)] The bear needs the tiger.[(triple1 OR ((triple5) -> rule5) OR ((triple6) -> rule5))] The squirrel chases the bear.[(triple3)] The squirrel chases the tiger.[(triple4)] The squirrel needs the bear.[(triple5)] The tiger needs the bear.[(triple6)] The tiger visits the squirrel.[(triple7)] @1: The bear chases the squirrel.[(((triple3) -> rule1))] The bear visits the tiger.[(((triple1) -> rule3) OR ((((triple5) -> rule5)) -> rule3) OR ((((triple6) -> rule5)) -> rule3))] @2: The squirrel is red.[(((triple1 ((triple3) -> rule1)) -> rule4) OR ((((triple5) -> rule5) ((triple3) -> rule1)) -> rule4) OR ((((triple6) -> rule5) ((triple3) -> rule1)) -> rule4))]
The bear does not visit the squirrel.
("bear" "visits" "squirrel" "-")
triple2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
triple1
((triple5) -> (rule5 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
((triple6) -> (rule5 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
triple3
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple4
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
triple5
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple6
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple7
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
((triple3) -> (rule1 % int1))
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
((triple1) -> (rule3 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
((((triple5) -> (rule5 % int2))) -> (rule3 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
((((triple6) -> (rule5 % int2))) -> (rule3 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
((triple1 ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int2
((((triple5) -> (rule5 % int3)) ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int3
((((triple6) -> (rule5 % int3)) ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int3