The bear chases the mouse. The bear eats the tiger. The bear needs the mouse. The dog does not chase the bear. The dog does not eat the bear. The dog needs the tiger. The mouse does not chase the bear. The mouse eats the dog. The mouse eats the tiger. The mouse is blue. The mouse is cold. The tiger does not eat the mouse. The tiger is cold. The tiger needs the dog. If something needs the bear then the bear is cold. If something is cold then it is red. If something eats the tiger and it needs the bear then the tiger does not eat the dog. If something eats the bear and the bear is kind then it does not eat the dog. If the mouse chases the bear then the mouse eats the dog. If the tiger chases the dog then the tiger eats the bear. If something is red then it needs the bear. If something chases the mouse then the mouse eats the tiger.
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The bear eats the tiger.
("bear" "eats" "tiger" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The dog does not chase the bear.
("dog" "chases" "bear" "-")
The dog does not eat the bear.
("dog" "eats" "bear" "-")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The mouse does not chase the bear.
("mouse" "chases" "bear" "-")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The tiger does not eat the mouse.
("tiger" "eats" "mouse" "-")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
If something needs the bear then the bear is cold.
((("something" "needs" "bear" "+")) -> ("bear" "is" "cold" "+"))
If something is cold then it is red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If something eats the tiger and it needs the bear then the tiger does not eat the dog.
((("something" "eats" "tiger" "+") ("something" "needs" "bear" "+")) -> ("tiger" "eats" "dog" "-"))
If something eats the bear and the bear is kind then it does not eat the dog.
((("something" "eats" "bear" "+") ("bear" "is" "kind" "+")) -> ("something" "eats" "dog" "-"))
If the mouse chases the bear then the mouse eats the dog.
((("mouse" "chases" "bear" "+")) -> ("mouse" "eats" "dog" "+"))
If the tiger chases the dog then the tiger eats the bear.
((("tiger" "chases" "dog" "+")) -> ("tiger" "eats" "bear" "+"))
If something is red then it needs the bear.
((("something" "is" "red" "+")) -> ("something" "needs" "bear" "+"))
If something chases the mouse then the mouse eats the tiger.
((("something" "chases" "mouse" "+")) -> ("mouse" "eats" "tiger" "+"))
The mouse eats the dog.
True
1
proof
[(triple8)]
("mouse" "eats" "dog" "+")
triple8
The bear does not need the mouse.
False
1
inv-proof
[(triple3)]
("bear" "needs" "mouse" "-")
triple3
The tiger is red.
True
2
proof
[(((triple13) -> rule2))]
("tiger" "is" "red" "+")
((triple13) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The mouse is not red.
False
2
inv-proof
[(((triple11) -> rule2))]
("mouse" "is" "red" "-")
((triple11) -> (rule2 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The tiger needs the bear.
True
3
proof
[(((((triple13) -> rule2)) -> rule7))]
("tiger" "needs" "bear" "+")
((((triple13) -> (rule2 % int2))) -> (rule7 % int1))
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The mouse does not need the bear.
False
3
inv-proof
[(((((triple11) -> rule2)) -> rule7))]
("mouse" "needs" "bear" "-")
((((triple11) -> (rule2 % int2))) -> (rule7 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The tiger does not eat the dog.
True
5
proof
[(((triple9 ((((triple11) -> rule2)) -> rule7)) -> rule3) OR ((((triple1) -> rule8) ((((triple11) -> rule2)) -> rule7)) -> rule3) OR ((triple2 ((((((((((triple11) -> rule2)) -> rule7)) -> rule1)) -> rule2)) -> rule7)) -> rule3) OR ((triple2 ((((((((((triple13) -> rule2)) -> rule7)) -> rule1)) -> rule2)) -> rule7)) -> rule3))]
("tiger" "eats" "dog" "-")
((triple9 ((((triple11) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The tiger does not eat the dog.
("tiger" "eats" "dog" "-")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
int3
((((triple1) -> (rule8 % int4)) ((((triple11) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The tiger does not eat the dog.
("tiger" "eats" "dog" "-")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
int3
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int4
((triple2 ((((((((((triple11) -> (rule2 % int6))) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The tiger does not eat the dog.
("tiger" "eats" "dog" "-")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The bear is cold.
("bear" "is" "cold" "+")
int4
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int5
The mouse is red.
("mouse" "is" "red" "+")
int6
((triple2 ((((((((((triple13) -> (rule2 % int6))) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The tiger does not eat the dog.
("tiger" "eats" "dog" "-")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The bear is cold.
("bear" "is" "cold" "+")
int4
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int5
The tiger is red.
("tiger" "is" "red" "+")
int6
The bear is not cold.
False
4
inv-proof
[(((((((triple11) -> rule2)) -> rule7)) -> rule1) OR ((((((triple13) -> rule2)) -> rule7)) -> rule1))]
("bear" "is" "cold" "-")
((((((triple11) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
int3
((((((triple13) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
The bear is red.
True
5
proof
[(((((((((triple11) -> rule2)) -> rule7)) -> rule1)) -> rule2) OR ((((((((triple13) -> rule2)) -> rule7)) -> rule1)) -> rule2))]
("bear" "is" "red" "+")
((((((((triple11) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int3
The mouse is red.
("mouse" "is" "red" "+")
int4
((((((((triple13) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int3
The tiger is red.
("tiger" "is" "red" "+")
int4
The bear is not red.
False
5
inv-proof
[(((((((((triple11) -> rule2)) -> rule7)) -> rule1)) -> rule2) OR ((((((((triple13) -> rule2)) -> rule7)) -> rule1)) -> rule2))]
("bear" "is" "red" "-")
((((((((triple11) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int3
The mouse is red.
("mouse" "is" "red" "+")
int4
((((((((triple13) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int3
The tiger is red.
("tiger" "is" "red" "+")
int4
The bear needs the bear.
True
6
proof
[(((((((((((triple11) -> rule2)) -> rule7)) -> rule1)) -> rule2)) -> rule7) OR ((((((((((triple13) -> rule2)) -> rule7)) -> rule1)) -> rule2)) -> rule7))]
("bear" "needs" "bear" "+")
((((((((((triple11) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int4
The mouse is red.
("mouse" "is" "red" "+")
int5
((((((((((triple13) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int4
The tiger is red.
("tiger" "is" "red" "+")
int5
The bear does not need the bear.
False
6
inv-proof
[(((((((((((triple11) -> rule2)) -> rule7)) -> rule1)) -> rule2)) -> rule7) OR ((((((((((triple13) -> rule2)) -> rule7)) -> rule1)) -> rule2)) -> rule7))]
("bear" "needs" "bear" "-")
((((((((((triple11) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int4
The mouse is red.
("mouse" "is" "red" "+")
int5
((((((((((triple13) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int4
The tiger is red.
("tiger" "is" "red" "+")
int5
The dog does not need the bear.
Unknown
inv-rconc
[@2: The dog needs the bear.[CWA. Example of deepest failure = (rule7 <- rule2 <- FAIL)]]
("dog" "needs" "bear" "-")
The tiger eats the bear.
Unknown
rconc
[@1: The tiger eats the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "eats" "bear" "+")
The dog is not red.
Unknown
inv-rconc
[@1: The dog is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "red" "-")
The bear needs the dog.
Unknown
random
[@0: The bear needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "dog" "+")
The tiger does not chase the tiger.
Unknown
inv-random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
The dog is not blue.
Unknown
inv-random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "-")
The mouse eats the bear.
Unknown
random
[@0: The mouse eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "bear" "+")
The tiger is not kind.
Unknown
inv-random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
The tiger is not blue.
Unknown
inv-random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "-")
The bear is big.
Unknown
random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "+")
@0: The bear chases the mouse.[(triple1)] The bear eats the tiger.[(triple2)] The bear needs the mouse.[(triple3)] The dog does not chase the bear.[(triple4)] The dog does not eat the bear.[(triple5)] The dog needs the tiger.[(triple6)] The mouse does not chase the bear.[(triple7)] The mouse eats the dog.[(triple8)] The mouse eats the tiger.[(triple9 OR ((triple1) -> rule8))] The mouse is blue.[(triple10)] The mouse is cold.[(triple11)] The tiger does not eat the mouse.[(triple12)] The tiger is cold.[(triple13)] The tiger needs the dog.[(triple14)] @1: The mouse is red.[(((triple11) -> rule2))] The tiger is red.[(((triple13) -> rule2))] @2: The mouse needs the bear.[(((((triple11) -> rule2)) -> rule7))] The tiger needs the bear.[(((((triple13) -> rule2)) -> rule7))] @3: The bear is cold.[(((((((triple11) -> rule2)) -> rule7)) -> rule1) OR ((((((triple13) -> rule2)) -> rule7)) -> rule1))] The tiger does not eat the dog.[(((triple9 ((((triple11) -> rule2)) -> rule7)) -> rule3) OR ((((triple1) -> rule8) ((((triple11) -> rule2)) -> rule7)) -> rule3) OR ((triple2 ((((((((((triple11) -> rule2)) -> rule7)) -> rule1)) -> rule2)) -> rule7)) -> rule3) OR ((triple2 ((((((((((triple13) -> rule2)) -> rule7)) -> rule1)) -> rule2)) -> rule7)) -> rule3))] @4: The bear is red.[(((((((((triple11) -> rule2)) -> rule7)) -> rule1)) -> rule2) OR ((((((((triple13) -> rule2)) -> rule7)) -> rule1)) -> rule2))] @5: The bear needs the bear.[(((((((((((triple11) -> rule2)) -> rule7)) -> rule1)) -> rule2)) -> rule7) OR ((((((((((triple13) -> rule2)) -> rule7)) -> rule1)) -> rule2)) -> rule7))]
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
triple2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple3
The dog does not chase the bear.
("dog" "chases" "bear" "-")
triple4
The dog does not eat the bear.
("dog" "eats" "bear" "-")
triple5
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple6
The mouse does not chase the bear.
("mouse" "chases" "bear" "-")
triple7
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple8
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple9
((triple1) -> (rule8 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
triple10
The mouse is cold.
("mouse" "is" "cold" "+")
triple11
The tiger does not eat the mouse.
("tiger" "eats" "mouse" "-")
triple12
The tiger is cold.
("tiger" "is" "cold" "+")
triple13
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple14
The mouse is red.
("mouse" "is" "red" "+")
((triple11) -> (rule2 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
((triple13) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
((((triple11) -> (rule2 % int2))) -> (rule7 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The tiger needs the bear.
("tiger" "needs" "bear" "+")
((((triple13) -> (rule2 % int2))) -> (rule7 % int1))
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
((((((triple11) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
int3
((((((triple13) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
The tiger does not eat the dog.
("tiger" "eats" "dog" "-")
((triple9 ((((triple11) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The tiger does not eat the dog.
("tiger" "eats" "dog" "-")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
int3
((((triple1) -> (rule8 % int4)) ((((triple11) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The tiger does not eat the dog.
("tiger" "eats" "dog" "-")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
int3
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int4
((triple2 ((((((((((triple11) -> (rule2 % int6))) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The tiger does not eat the dog.
("tiger" "eats" "dog" "-")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The bear is cold.
("bear" "is" "cold" "+")
int4
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int5
The mouse is red.
("mouse" "is" "red" "+")
int6
((triple2 ((((((((((triple13) -> (rule2 % int6))) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The tiger does not eat the dog.
("tiger" "eats" "dog" "-")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The bear is cold.
("bear" "is" "cold" "+")
int4
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int5
The tiger is red.
("tiger" "is" "red" "+")
int6
The bear is red.
("bear" "is" "red" "+")
((((((((triple11) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int3
The mouse is red.
("mouse" "is" "red" "+")
int4
((((((((triple13) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int3
The tiger is red.
("tiger" "is" "red" "+")
int4
The bear needs the bear.
("bear" "needs" "bear" "+")
((((((((((triple11) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int4
The mouse is red.
("mouse" "is" "red" "+")
int5
((((((((((triple13) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
int3
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int4
The tiger is red.
("tiger" "is" "red" "+")
int5