The bear is cold. The squirrel eats the bear. The tiger is cold. If something needs the bear then it eats the tiger. If something is blue and big then it does not eat the tiger. If something is cold then it needs the tiger. If the tiger is nice and the tiger needs the squirrel then the tiger does not eat the squirrel. If something is cold then it needs the squirrel. If something needs the tiger then it needs the bear. If something is kind and not big then it is cold. If something is blue and it does not see the bear then the bear does not need the squirrel.
The bear is cold.
("bear" "is" "cold" "+")
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
If something needs the bear then it eats the tiger.
((("something" "needs" "bear" "+")) -> ("something" "eats" "tiger" "+"))
If something is blue and big then it does not eat the tiger.
((("something" "is" "blue" "+") ("something" "is" "big" "+")) -> ("something" "eats" "tiger" "-"))
If something is cold then it needs the tiger.
((("something" "is" "cold" "+")) -> ("something" "needs" "tiger" "+"))
If the tiger is nice and the tiger needs the squirrel then the tiger does not eat the squirrel.
((("tiger" "is" "nice" "+") ("tiger" "needs" "squirrel" "+")) -> ("tiger" "eats" "squirrel" "-"))
If something is cold then it needs the squirrel.
((("something" "is" "cold" "+")) -> ("something" "needs" "squirrel" "+"))
If something needs the tiger then it needs the bear.
((("something" "needs" "tiger" "+")) -> ("something" "needs" "bear" "+"))
If something is kind and not big then it is cold.
((("something" "is" "kind" "+") ("something" "is" "big" "~")) -> ("something" "is" "cold" "+"))
If something is blue and it does not see the bear then the bear does not need the squirrel.
((("something" "is" "blue" "+") ("something" "sees" "bear" "~")) -> ("bear" "needs" "squirrel" "-"))
The squirrel eats the bear.
True
1
proof
[(triple2)]
("squirrel" "eats" "bear" "+")
triple2
The tiger is not cold.
False
1
inv-proof
[(triple3)]
("tiger" "is" "cold" "-")
triple3
The bear needs the squirrel.
True
2
proof
[(((triple1) -> rule5))]
("bear" "needs" "squirrel" "+")
((triple1) -> (rule5 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The bear does not need the tiger.
False
2
inv-proof
[(((triple1) -> rule3))]
("bear" "needs" "tiger" "-")
((triple1) -> (rule3 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The tiger needs the bear.
True
3
proof
[(((((triple3) -> rule3)) -> rule6))]
("tiger" "needs" "bear" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger does not need the bear.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule6))]
("tiger" "needs" "bear" "-")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The bear eats the tiger.
True
4
proof
[(((((((triple1) -> rule3)) -> rule6)) -> rule1))]
("bear" "eats" "tiger" "+")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int3
The bear does not eat the tiger.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule6)) -> rule1))]
("bear" "eats" "tiger" "-")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int3
The squirrel does not need the squirrel.
Unknown
inv-rconc
[@2: The squirrel needs the squirrel.[CWA. Example of deepest failure = (rule5 <- rule7 <- FAIL)]]
("squirrel" "needs" "squirrel" "-")
The squirrel needs the tiger.
Unknown
rconc
[@2: The squirrel needs the tiger.[CWA. Example of deepest failure = (rule3 <- rule7 <- FAIL)]]
("squirrel" "needs" "tiger" "+")
The squirrel does not eat the tiger.
Unknown
inv-rconc
[@4: The squirrel eats the tiger.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule3 <- rule7 <- FAIL)]]
("squirrel" "eats" "tiger" "-")
The squirrel is cold.
Unknown
rconc
[@1: The squirrel is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "is" "cold" "+")
The tiger does not eat the bear.
Unknown
inv-random
[@0: The tiger eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "bear" "-")
The squirrel sees the bear.
Unknown
random
[@0: The squirrel sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "bear" "+")
The squirrel does not see the tiger.
Unknown
inv-random
[@0: The squirrel sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "tiger" "-")
The bear is big.
Unknown
random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "+")
@0: The bear is cold.[(triple1)] The squirrel eats the bear.[(triple2)] The tiger is cold.[(triple3)] @1: The bear needs the squirrel.[(((triple1) -> rule5))] The bear needs the tiger.[(((triple1) -> rule3))] The tiger needs the squirrel.[(((triple3) -> rule5))] The tiger needs the tiger.[(((triple3) -> rule3))] @2: The bear needs the bear.[(((((triple1) -> rule3)) -> rule6))] The tiger needs the bear.[(((((triple3) -> rule3)) -> rule6))] @3: The bear eats the tiger.[(((((((triple1) -> rule3)) -> rule6)) -> rule1))] The tiger eats the tiger.[(((((((triple3) -> rule3)) -> rule6)) -> rule1))]
The bear is cold.
("bear" "is" "cold" "+")
triple1
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
triple2
The tiger is cold.
("tiger" "is" "cold" "+")
triple3
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
((triple1) -> (rule5 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
((triple1) -> (rule3 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
((triple3) -> (rule5 % int1))
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((triple3) -> (rule3 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The tiger needs the bear.
("tiger" "needs" "bear" "+")
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The bear eats the tiger.
("bear" "eats" "tiger" "+")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int3
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int3