The bear eats the mouse. The bear visits the dog. The bear visits the mouse. The dog eats the bear. The dog eats the mouse. The dog is blue. The dog is round. The dog needs the mouse. The dog visits the tiger. The mouse needs the bear. The tiger eats the dog. The tiger visits the dog. If someone is cold and they need the mouse then they eat the mouse. If someone is red then they visit the bear. If someone needs the mouse then the mouse needs the bear. If someone visits the tiger then the tiger eats the mouse. All red, blue people are rough. If someone visits the bear and they are red then the bear needs the mouse. If someone is rough then they eat the tiger. If the dog visits the tiger and the dog needs the bear then the bear is round. If someone needs the mouse and they eat the mouse then they are red.
The bear eats the mouse.
("bear" "eats" "mouse" "+")
The bear visits the dog.
("bear" "visits" "dog" "+")
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The dog eats the bear.
("dog" "eats" "bear" "+")
The dog eats the mouse.
("dog" "eats" "mouse" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is round.
("dog" "is" "round" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The tiger eats the dog.
("tiger" "eats" "dog" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If someone is cold and they need the mouse then they eat the mouse.
((("someone" "is" "cold" "+") ("someone" "needs" "mouse" "+")) -> ("someone" "eats" "mouse" "+"))
If someone is red then they visit the bear.
((("someone" "is" "red" "+")) -> ("someone" "visits" "bear" "+"))
If someone needs the mouse then the mouse needs the bear.
((("someone" "needs" "mouse" "+")) -> ("mouse" "needs" "bear" "+"))
If someone visits the tiger then the tiger eats the mouse.
((("someone" "visits" "tiger" "+")) -> ("tiger" "eats" "mouse" "+"))
All red, blue people are rough.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If someone visits the bear and they are red then the bear needs the mouse.
((("someone" "visits" "bear" "+") ("someone" "is" "red" "+")) -> ("bear" "needs" "mouse" "+"))
If someone is rough then they eat the tiger.
((("someone" "is" "rough" "+")) -> ("someone" "eats" "tiger" "+"))
If the dog visits the tiger and the dog needs the bear then the bear is round.
((("dog" "visits" "tiger" "+") ("dog" "needs" "bear" "+")) -> ("bear" "is" "round" "+"))
If someone needs the mouse and they eat the mouse then they are red.
((("someone" "needs" "mouse" "+") ("someone" "eats" "mouse" "+")) -> ("someone" "is" "red" "+"))
The bear visits the mouse.
True
1
proof
[(triple3)]
("bear" "visits" "mouse" "+")
triple3
The dog does not need the mouse.
False
1
inv-proof
[(triple8)]
("dog" "needs" "mouse" "-")
triple8
The dog is red.
True
3
proof
[(((triple8 triple5) -> rule9))]
("dog" "is" "red" "+")
((triple8 triple5) -> (rule9 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The tiger does not eat the mouse.
False
2
inv-proof
[(((triple9) -> rule4))]
("tiger" "eats" "mouse" "-")
((triple9) -> (rule4 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The dog visits the bear.
True
4
proof
[(((((triple8 triple5) -> rule9)) -> rule2))]
("dog" "visits" "bear" "+")
((((triple8 triple5) -> (rule9 % int2))) -> (rule2 % int1))
The dog visits the bear.
("dog" "visits" "bear" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog is not rough.
False
5
inv-proof
[(((((triple8 triple5) -> rule9) triple6) -> rule5))]
("dog" "is" "rough" "-")
((((triple8 triple5) -> (rule9 % int2)) triple6) -> (rule5 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog eats the tiger.
True
6
proof
[(((((((triple8 triple5) -> rule9) triple6) -> rule5)) -> rule7))]
("dog" "eats" "tiger" "+")
((((((triple8 triple5) -> (rule9 % int3)) triple6) -> (rule5 % int2))) -> (rule7 % int1))
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The dog is red.
("dog" "is" "red" "+")
int3
The bear does not need the mouse.
False
8
inv-proof
[(((((((triple8 triple5) -> rule9)) -> rule2) ((triple8 triple5) -> rule9)) -> rule6))]
("bear" "needs" "mouse" "-")
((((((triple8 triple5) -> (rule9 % int3))) -> (rule2 % int2)) ((triple8 triple5) -> (rule9 % int3))) -> (rule6 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The dog visits the bear.
("dog" "visits" "bear" "+")
int2
The dog is red.
("dog" "is" "red" "+")
int3
The bear is red.
True
10
proof
[(((((((((triple8 triple5) -> rule9)) -> rule2) ((triple8 triple5) -> rule9)) -> rule6) triple1) -> rule9))]
("bear" "is" "red" "+")
((((((((triple8 triple5) -> (rule9 % int4))) -> (rule2 % int3)) ((triple8 triple5) -> (rule9 % int4))) -> (rule6 % int2)) triple1) -> (rule9 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int2
The dog visits the bear.
("dog" "visits" "bear" "+")
int3
The dog is red.
("dog" "is" "red" "+")
int4
The bear is not red.
False
10
inv-proof
[(((((((((triple8 triple5) -> rule9)) -> rule2) ((triple8 triple5) -> rule9)) -> rule6) triple1) -> rule9))]
("bear" "is" "red" "-")
((((((((triple8 triple5) -> (rule9 % int4))) -> (rule2 % int3)) ((triple8 triple5) -> (rule9 % int4))) -> (rule6 % int2)) triple1) -> (rule9 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int2
The dog visits the bear.
("dog" "visits" "bear" "+")
int3
The dog is red.
("dog" "is" "red" "+")
int4
The bear visits the bear.
True
11
proof
[(((((((((((triple8 triple5) -> rule9)) -> rule2) ((triple8 triple5) -> rule9)) -> rule6) triple1) -> rule9)) -> rule2))]
("bear" "visits" "bear" "+")
((((((((((triple8 triple5) -> (rule9 % int5))) -> (rule2 % int4)) ((triple8 triple5) -> (rule9 % int5))) -> (rule6 % int3)) triple1) -> (rule9 % int2))) -> (rule2 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int3
The dog visits the bear.
("dog" "visits" "bear" "+")
int4
The dog is red.
("dog" "is" "red" "+")
int5
The bear does not visit the bear.
False
11
inv-proof
[(((((((((((triple8 triple5) -> rule9)) -> rule2) ((triple8 triple5) -> rule9)) -> rule6) triple1) -> rule9)) -> rule2))]
("bear" "visits" "bear" "-")
((((((((((triple8 triple5) -> (rule9 % int5))) -> (rule2 % int4)) ((triple8 triple5) -> (rule9 % int5))) -> (rule6 % int3)) triple1) -> (rule9 % int2))) -> (rule2 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int3
The dog visits the bear.
("dog" "visits" "bear" "+")
int4
The dog is red.
("dog" "is" "red" "+")
int5
The mouse does not visit the bear.
Unknown
inv-rconc
[@2: The mouse visits the bear.[CWA. Example of deepest failure = (rule2 <- rule9 <- FAIL)]]
("mouse" "visits" "bear" "-")
The tiger eats the tiger.
Unknown
rconc
[@2: The tiger eats the tiger.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("tiger" "eats" "tiger" "+")
The bear does not eat the tiger.
Unknown
inv-rconc
[@2: The bear eats the tiger.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("bear" "eats" "tiger" "-")
The tiger is rough.
Unknown
rconc
[@1: The tiger is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "is" "rough" "+")
The mouse does not eat the tiger.
Unknown
inv-rconc
[@2: The mouse eats the tiger.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("mouse" "eats" "tiger" "-")
The tiger visits the bear.
Unknown
rconc
[@2: The tiger visits the bear.[CWA. Example of deepest failure = (rule2 <- rule9 <- FAIL)]]
("tiger" "visits" "bear" "+")
The tiger does not visit the mouse.
Unknown
inv-random
[@0: The tiger visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "mouse" "-")
The mouse is round.
Unknown
random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "+")
The mouse does not eat the bear.
Unknown
inv-random
[@0: The mouse eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "bear" "-")
The tiger needs the bear.
Unknown
random
[@0: The tiger needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "bear" "+")
The tiger does not need the mouse.
Unknown
inv-random
[@0: The tiger needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "mouse" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
@0: The bear eats the mouse.[(triple1)] The bear visits the dog.[(triple2)] The bear visits the mouse.[(triple3)] The dog eats the bear.[(triple4)] The dog eats the mouse.[(triple5)] The dog is blue.[(triple6)] The dog is round.[(triple7)] The dog needs the mouse.[(triple8)] The dog visits the tiger.[(triple9)] The mouse needs the bear.[(triple10 OR ((triple8) -> rule3) OR ((((((((triple8 triple5) -> rule9)) -> rule2) ((triple8 triple5) -> rule9)) -> rule6)) -> rule3))] The tiger eats the dog.[(triple11)] The tiger visits the dog.[(triple12)] @1: The dog is red.[(((triple8 triple5) -> rule9))] The tiger eats the mouse.[(((triple9) -> rule4))] @2: The dog is rough.[(((((triple8 triple5) -> rule9) triple6) -> rule5))] The dog visits the bear.[(((((triple8 triple5) -> rule9)) -> rule2))] @3: The bear needs the mouse.[(((((((triple8 triple5) -> rule9)) -> rule2) ((triple8 triple5) -> rule9)) -> rule6))] The dog eats the tiger.[(((((((triple8 triple5) -> rule9) triple6) -> rule5)) -> rule7))] @4: The bear is red.[(((((((((triple8 triple5) -> rule9)) -> rule2) ((triple8 triple5) -> rule9)) -> rule6) triple1) -> rule9))] @5: The bear visits the bear.[(((((((((((triple8 triple5) -> rule9)) -> rule2) ((triple8 triple5) -> rule9)) -> rule6) triple1) -> rule9)) -> rule2))]
The bear eats the mouse.
("bear" "eats" "mouse" "+")
triple1
The bear visits the dog.
("bear" "visits" "dog" "+")
triple2
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple3
The dog eats the bear.
("dog" "eats" "bear" "+")
triple4
The dog eats the mouse.
("dog" "eats" "mouse" "+")
triple5
The dog is blue.
("dog" "is" "blue" "+")
triple6
The dog is round.
("dog" "is" "round" "+")
triple7
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple8
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple9
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple10
((triple8) -> (rule3 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
((((((((triple8 triple5) -> (rule9 % int4))) -> (rule2 % int3)) ((triple8 triple5) -> (rule9 % int4))) -> (rule6 % int2))) -> (rule3 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int2
The dog visits the bear.
("dog" "visits" "bear" "+")
int3
The dog is red.
("dog" "is" "red" "+")
int4
The tiger eats the dog.
("tiger" "eats" "dog" "+")
triple11
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple12
The dog is red.
("dog" "is" "red" "+")
((triple8 triple5) -> (rule9 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
((triple9) -> (rule4 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
((((triple8 triple5) -> (rule9 % int2)) triple6) -> (rule5 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog visits the bear.
("dog" "visits" "bear" "+")
((((triple8 triple5) -> (rule9 % int2))) -> (rule2 % int1))
The dog visits the bear.
("dog" "visits" "bear" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
((((((triple8 triple5) -> (rule9 % int3))) -> (rule2 % int2)) ((triple8 triple5) -> (rule9 % int3))) -> (rule6 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The dog visits the bear.
("dog" "visits" "bear" "+")
int2
The dog is red.
("dog" "is" "red" "+")
int3
The dog eats the tiger.
("dog" "eats" "tiger" "+")
((((((triple8 triple5) -> (rule9 % int3)) triple6) -> (rule5 % int2))) -> (rule7 % int1))
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
int2
The dog is red.
("dog" "is" "red" "+")
int3
The bear is red.
("bear" "is" "red" "+")
((((((((triple8 triple5) -> (rule9 % int4))) -> (rule2 % int3)) ((triple8 triple5) -> (rule9 % int4))) -> (rule6 % int2)) triple1) -> (rule9 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int2
The dog visits the bear.
("dog" "visits" "bear" "+")
int3
The dog is red.
("dog" "is" "red" "+")
int4
The bear visits the bear.
("bear" "visits" "bear" "+")
((((((((((triple8 triple5) -> (rule9 % int5))) -> (rule2 % int4)) ((triple8 triple5) -> (rule9 % int5))) -> (rule6 % int3)) triple1) -> (rule9 % int2))) -> (rule2 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int3
The dog visits the bear.
("dog" "visits" "bear" "+")
int4
The dog is red.
("dog" "is" "red" "+")
int5