The bear eats the dog. The bear is blue. The dog eats the tiger. The dog is green. The dog likes the tiger. The dog needs the mouse. The mouse eats the tiger. The mouse is not big. The mouse likes the bear. The mouse needs the bear. The tiger is not kind. The tiger likes the bear. The tiger likes the mouse. The tiger needs the bear. The tiger needs the dog. The tiger needs the mouse. If someone eats the mouse then the mouse is kind. If someone likes the dog then the dog likes the bear. If someone likes the dog and they are green then they eat the tiger. If the dog likes the bear and the dog eats the tiger then the tiger is green. If someone needs the bear then they are round. If someone is round then they like the dog. If someone is kind and they like the tiger then the tiger likes the dog.
The bear eats the dog.
("bear" "eats" "dog" "+")
The bear is blue.
("bear" "is" "blue" "+")
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The dog is green.
("dog" "is" "green" "+")
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is not big.
("mouse" "is" "big" "-")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The tiger is not kind.
("tiger" "is" "kind" "-")
The tiger likes the bear.
("tiger" "likes" "bear" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
If someone eats the mouse then the mouse is kind.
((("someone" "eats" "mouse" "+")) -> ("mouse" "is" "kind" "+"))
If someone likes the dog then the dog likes the bear.
((("someone" "likes" "dog" "+")) -> ("dog" "likes" "bear" "+"))
If someone likes the dog and they are green then they eat the tiger.
((("someone" "likes" "dog" "+") ("someone" "is" "green" "+")) -> ("someone" "eats" "tiger" "+"))
If the dog likes the bear and the dog eats the tiger then the tiger is green.
((("dog" "likes" "bear" "+") ("dog" "eats" "tiger" "+")) -> ("tiger" "is" "green" "+"))
If someone needs the bear then they are round.
((("someone" "needs" "bear" "+")) -> ("someone" "is" "round" "+"))
If someone is round then they like the dog.
((("someone" "is" "round" "+")) -> ("someone" "likes" "dog" "+"))
If someone is kind and they like the tiger then the tiger likes the dog.
((("someone" "is" "kind" "+") ("someone" "likes" "tiger" "+")) -> ("tiger" "likes" "dog" "+"))
The dog is green.
True
1
proof
[(triple4)]
("dog" "is" "green" "+")
triple4
The bear is not blue.
False
1
inv-proof
[(triple2)]
("bear" "is" "blue" "-")
triple2
The tiger is round.
True
2
proof
[(((triple14) -> rule5))]
("tiger" "is" "round" "+")
((triple14) -> (rule5 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The mouse is not round.
False
2
inv-proof
[(((triple10) -> rule5))]
("mouse" "is" "round" "-")
((triple10) -> (rule5 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The tiger likes the dog.
True
3
proof
[(((((triple14) -> rule5)) -> rule6))]
("tiger" "likes" "dog" "+")
((((triple14) -> (rule5 % int2))) -> (rule6 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The mouse does not like the dog.
False
3
inv-proof
[(((((triple10) -> rule5)) -> rule6))]
("mouse" "likes" "dog" "-")
((((triple10) -> (rule5 % int2))) -> (rule6 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The dog likes the bear.
True
4
proof
[(((((((triple10) -> rule5)) -> rule6)) -> rule2) OR ((((((triple14) -> rule5)) -> rule6)) -> rule2))]
("dog" "likes" "bear" "+")
((((((triple10) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The dog likes the bear.
("dog" "likes" "bear" "+")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
int3
((((((triple14) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The dog likes the bear.
("dog" "likes" "bear" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
The dog does not like the bear.
False
4
inv-proof
[(((((((triple10) -> rule5)) -> rule6)) -> rule2) OR ((((((triple14) -> rule5)) -> rule6)) -> rule2))]
("dog" "likes" "bear" "-")
((((((triple10) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The dog likes the bear.
("dog" "likes" "bear" "+")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
int3
((((((triple14) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The dog likes the bear.
("dog" "likes" "bear" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
The tiger is green.
True
6
proof
[(((((((((triple10) -> rule5)) -> rule6)) -> rule2) triple3) -> rule4) OR ((((((((triple14) -> rule5)) -> rule6)) -> rule2) triple3) -> rule4))]
("tiger" "is" "green" "+")
((((((((triple10) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule2 % int2)) triple3) -> (rule4 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The dog likes the bear.
("dog" "likes" "bear" "+")
int2
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int3
The mouse is round.
("mouse" "is" "round" "+")
int4
((((((((triple14) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule2 % int2)) triple3) -> (rule4 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The dog likes the bear.
("dog" "likes" "bear" "+")
int2
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int3
The tiger is round.
("tiger" "is" "round" "+")
int4
The tiger is not green.
False
6
inv-proof
[(((((((((triple10) -> rule5)) -> rule6)) -> rule2) triple3) -> rule4) OR ((((((((triple14) -> rule5)) -> rule6)) -> rule2) triple3) -> rule4))]
("tiger" "is" "green" "-")
((((((((triple10) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule2 % int2)) triple3) -> (rule4 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The dog likes the bear.
("dog" "likes" "bear" "+")
int2
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int3
The mouse is round.
("mouse" "is" "round" "+")
int4
((((((((triple14) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule2 % int2)) triple3) -> (rule4 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The dog likes the bear.
("dog" "likes" "bear" "+")
int2
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int3
The tiger is round.
("tiger" "is" "round" "+")
int4
The tiger eats the tiger.
True
10
proof
[(((((((triple14) -> rule5)) -> rule6) ((((((((triple10) -> rule5)) -> rule6)) -> rule2) triple3) -> rule4)) -> rule3) OR ((((((triple14) -> rule5)) -> rule6) ((((((((triple14) -> rule5)) -> rule6)) -> rule2) triple3) -> rule4)) -> rule3))]
("tiger" "eats" "tiger" "+")
((((((triple14) -> (rule5 % int7))) -> (rule6 % int6)) ((((((((triple10) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule2 % int3)) triple3) -> (rule4 % int2))) -> (rule3 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The dog likes the bear.
("dog" "likes" "bear" "+")
int3
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int4
The mouse is round.
("mouse" "is" "round" "+")
int5
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int6
The tiger is round.
("tiger" "is" "round" "+")
int7
((((((triple14) -> (rule5 % int5))) -> (rule6 % int4)) ((((((((triple14) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule2 % int3)) triple3) -> (rule4 % int2))) -> (rule3 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The dog likes the bear.
("dog" "likes" "bear" "+")
int3
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int4
The tiger is round.
("tiger" "is" "round" "+")
int5
The tiger does not eat the tiger.
False
10
inv-proof
[(((((((triple14) -> rule5)) -> rule6) ((((((((triple10) -> rule5)) -> rule6)) -> rule2) triple3) -> rule4)) -> rule3) OR ((((((triple14) -> rule5)) -> rule6) ((((((((triple14) -> rule5)) -> rule6)) -> rule2) triple3) -> rule4)) -> rule3))]
("tiger" "eats" "tiger" "-")
((((((triple14) -> (rule5 % int7))) -> (rule6 % int6)) ((((((((triple10) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule2 % int3)) triple3) -> (rule4 % int2))) -> (rule3 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The dog likes the bear.
("dog" "likes" "bear" "+")
int3
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int4
The mouse is round.
("mouse" "is" "round" "+")
int5
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int6
The tiger is round.
("tiger" "is" "round" "+")
int7
((((((triple14) -> (rule5 % int5))) -> (rule6 % int4)) ((((((((triple14) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule2 % int3)) triple3) -> (rule4 % int2))) -> (rule3 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The dog likes the bear.
("dog" "likes" "bear" "+")
int3
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int4
The tiger is round.
("tiger" "is" "round" "+")
int5
The dog does not like the dog.
Unknown
inv-rconc
[@2: The dog likes the dog.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("dog" "likes" "dog" "-")
The bear eats the tiger.
Unknown
rconc
[@1: The bear eats the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "eats" "tiger" "+")
The bear is not round.
Unknown
inv-rconc
[@1: The bear is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "is" "round" "-")
The mouse is kind.
Unknown
rconc
[@1: The mouse is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "kind" "+")
The dog is not round.
Unknown
inv-rconc
[@1: The dog is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "round" "-")
The bear likes the dog.
Unknown
rconc
[@2: The bear likes the dog.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("bear" "likes" "dog" "+")
The dog does not eat the mouse.
Unknown
inv-random
[@0: The dog eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "mouse" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
The mouse does not eat the dog.
Unknown
inv-random
[@0: The mouse eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "dog" "-")
The dog is kind.
Unknown
random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "+")
The bear does not need the dog.
Unknown
inv-random
[@0: The bear needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "dog" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
@0: The bear eats the dog.[(triple1)] The bear is blue.[(triple2)] The dog eats the tiger.[(triple3)] The dog is green.[(triple4)] The dog likes the tiger.[(triple5)] The dog needs the mouse.[(triple6)] The mouse eats the tiger.[(triple7)] The mouse is not big.[(triple8)] The mouse likes the bear.[(triple9)] The mouse needs the bear.[(triple10)] The tiger is not kind.[(triple11)] The tiger likes the bear.[(triple12)] The tiger likes the mouse.[(triple13)] The tiger needs the bear.[(triple14)] The tiger needs the dog.[(triple15)] The tiger needs the mouse.[(triple16)] @1: The mouse is round.[(((triple10) -> rule5))] The tiger is round.[(((triple14) -> rule5))] @2: The mouse likes the dog.[(((((triple10) -> rule5)) -> rule6))] The tiger likes the dog.[(((((triple14) -> rule5)) -> rule6))] @3: The dog likes the bear.[(((((((triple10) -> rule5)) -> rule6)) -> rule2) OR ((((((triple14) -> rule5)) -> rule6)) -> rule2))] @4: The tiger is green.[(((((((((triple10) -> rule5)) -> rule6)) -> rule2) triple3) -> rule4) OR ((((((((triple14) -> rule5)) -> rule6)) -> rule2) triple3) -> rule4))] @5: The tiger eats the tiger.[(((((((triple14) -> rule5)) -> rule6) ((((((((triple10) -> rule5)) -> rule6)) -> rule2) triple3) -> rule4)) -> rule3) OR ((((((triple14) -> rule5)) -> rule6) ((((((((triple14) -> rule5)) -> rule6)) -> rule2) triple3) -> rule4)) -> rule3))]
The bear eats the dog.
("bear" "eats" "dog" "+")
triple1
The bear is blue.
("bear" "is" "blue" "+")
triple2
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple3
The dog is green.
("dog" "is" "green" "+")
triple4
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple5
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple6
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple7
The mouse is not big.
("mouse" "is" "big" "-")
triple8
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple9
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple10
The tiger is not kind.
("tiger" "is" "kind" "-")
triple11
The tiger likes the bear.
("tiger" "likes" "bear" "+")
triple12
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple13
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple14
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple15
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple16
The mouse is round.
("mouse" "is" "round" "+")
((triple10) -> (rule5 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
((triple14) -> (rule5 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
((((triple10) -> (rule5 % int2))) -> (rule6 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The tiger likes the dog.
("tiger" "likes" "dog" "+")
((((triple14) -> (rule5 % int2))) -> (rule6 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The dog likes the bear.
("dog" "likes" "bear" "+")
((((((triple10) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The dog likes the bear.
("dog" "likes" "bear" "+")
int1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
int3
((((((triple14) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The dog likes the bear.
("dog" "likes" "bear" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
The tiger is green.
("tiger" "is" "green" "+")
((((((((triple10) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule2 % int2)) triple3) -> (rule4 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The dog likes the bear.
("dog" "likes" "bear" "+")
int2
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int3
The mouse is round.
("mouse" "is" "round" "+")
int4
((((((((triple14) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule2 % int2)) triple3) -> (rule4 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The dog likes the bear.
("dog" "likes" "bear" "+")
int2
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int3
The tiger is round.
("tiger" "is" "round" "+")
int4
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((((((triple14) -> (rule5 % int7))) -> (rule6 % int6)) ((((((((triple10) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule2 % int3)) triple3) -> (rule4 % int2))) -> (rule3 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The dog likes the bear.
("dog" "likes" "bear" "+")
int3
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int4
The mouse is round.
("mouse" "is" "round" "+")
int5
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int6
The tiger is round.
("tiger" "is" "round" "+")
int7
((((((triple14) -> (rule5 % int5))) -> (rule6 % int4)) ((((((((triple14) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule2 % int3)) triple3) -> (rule4 % int2))) -> (rule3 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The dog likes the bear.
("dog" "likes" "bear" "+")
int3
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int4
The tiger is round.
("tiger" "is" "round" "+")
int5