The bear eats the lion. The bear sees the dog. The dog sees the lion. The lion eats the dog. The lion sees the bear. The mouse does not like the dog. The mouse sees the dog. If something sees the mouse and the mouse likes the lion then the mouse eats the dog. If something sees the dog then the dog likes the mouse. If something likes the bear then it is big. If something eats the lion then the lion is round. If something likes the lion then it sees the mouse. If something eats the dog then the dog is round. If something sees the mouse then the mouse likes the bear. If something is rough then it likes the lion. If the lion sees the bear then the lion is rough.
The bear eats the lion.
("bear" "eats" "lion" "+")
The bear sees the dog.
("bear" "sees" "dog" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
The mouse does not like the dog.
("mouse" "likes" "dog" "-")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
If something sees the mouse and the mouse likes the lion then the mouse eats the dog.
((("something" "sees" "mouse" "+") ("mouse" "likes" "lion" "+")) -> ("mouse" "eats" "dog" "+"))
If something sees the dog then the dog likes the mouse.
((("something" "sees" "dog" "+")) -> ("dog" "likes" "mouse" "+"))
If something likes the bear then it is big.
((("something" "likes" "bear" "+")) -> ("something" "is" "big" "+"))
If something eats the lion then the lion is round.
((("something" "eats" "lion" "+")) -> ("lion" "is" "round" "+"))
If something likes the lion then it sees the mouse.
((("something" "likes" "lion" "+")) -> ("something" "sees" "mouse" "+"))
If something eats the dog then the dog is round.
((("something" "eats" "dog" "+")) -> ("dog" "is" "round" "+"))
If something sees the mouse then the mouse likes the bear.
((("something" "sees" "mouse" "+")) -> ("mouse" "likes" "bear" "+"))
If something is rough then it likes the lion.
((("something" "is" "rough" "+")) -> ("something" "likes" "lion" "+"))
If the lion sees the bear then the lion is rough.
((("lion" "sees" "bear" "+")) -> ("lion" "is" "rough" "+"))
The dog sees the lion.
True
1
proof
[(triple3)]
("dog" "sees" "lion" "+")
triple3
The dog does not see the lion.
False
1
inv-proof
[(triple3)]
("dog" "sees" "lion" "-")
triple3
The dog is round.
True
2
proof
[(((triple4) -> rule6))]
("dog" "is" "round" "+")
((triple4) -> (rule6 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog does not like the mouse.
False
2
inv-proof
[(((triple2) -> rule2) OR ((triple7) -> rule2))]
("dog" "likes" "mouse" "-")
((triple2) -> (rule2 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
((triple7) -> (rule2 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The lion likes the lion.
True
3
proof
[(((((triple5) -> rule9)) -> rule8))]
("lion" "likes" "lion" "+")
((((triple5) -> (rule9 % int2))) -> (rule8 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion does not like the lion.
False
3
inv-proof
[(((((triple5) -> rule9)) -> rule8))]
("lion" "likes" "lion" "-")
((((triple5) -> (rule9 % int2))) -> (rule8 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion sees the mouse.
True
4
proof
[(((((((triple5) -> rule9)) -> rule8)) -> rule5))]
("lion" "sees" "mouse" "+")
((((((triple5) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3
The lion does not see the mouse.
False
4
inv-proof
[(((((((triple5) -> rule9)) -> rule8)) -> rule5))]
("lion" "sees" "mouse" "-")
((((((triple5) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3
The mouse likes the bear.
True
5
proof
[(((((((((triple5) -> rule9)) -> rule8)) -> rule5)) -> rule7))]
("mouse" "likes" "bear" "+")
((((((((triple5) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
int3
The lion is rough.
("lion" "is" "rough" "+")
int4
The mouse does not like the bear.
False
5
inv-proof
[(((((((((triple5) -> rule9)) -> rule8)) -> rule5)) -> rule7))]
("mouse" "likes" "bear" "-")
((((((((triple5) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
int3
The lion is rough.
("lion" "is" "rough" "+")
int4
The mouse is big.
True
6
proof
[(((((((((((triple5) -> rule9)) -> rule8)) -> rule5)) -> rule7)) -> rule3))]
("mouse" "is" "big" "+")
((((((((((triple5) -> (rule9 % int5))) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int2
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int3
The lion likes the lion.
("lion" "likes" "lion" "+")
int4
The lion is rough.
("lion" "is" "rough" "+")
int5
The mouse is not big.
False
6
inv-proof
[(((((((((((triple5) -> rule9)) -> rule8)) -> rule5)) -> rule7)) -> rule3))]
("mouse" "is" "big" "-")
((((((((((triple5) -> (rule9 % int5))) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int2
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int3
The lion likes the lion.
("lion" "likes" "lion" "+")
int4
The lion is rough.
("lion" "is" "rough" "+")
int5
The mouse does not eat the dog.
Unknown
inv-rconc
[@2: The mouse eats the dog.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("mouse" "eats" "dog" "-")
The bear sees the mouse.
Unknown
rconc
[@2: The bear sees the mouse.[CWA. Example of deepest failure = (rule5 <- rule8 <- FAIL)]]
("bear" "sees" "mouse" "+")
The dog does not like the lion.
Unknown
inv-rconc
[@1: The dog likes the lion.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "likes" "lion" "-")
The bear likes the lion.
Unknown
rconc
[@1: The bear likes the lion.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "likes" "lion" "+")
The mouse does not like the lion.
Unknown
inv-rconc
[@1: The mouse likes the lion.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "likes" "lion" "-")
The dog sees the mouse.
Unknown
rconc
[@2: The dog sees the mouse.[CWA. Example of deepest failure = (rule5 <- rule8 <- FAIL)]]
("dog" "sees" "mouse" "+")
The dog does not see the bear.
Unknown
inv-random
[@0: The dog sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "bear" "-")
The dog eats the lion.
Unknown
random
[@0: The dog eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "lion" "+")
The bear does not eat the mouse.
Unknown
inv-random
[@0: The bear eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "mouse" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The dog eats the mouse.
Unknown
random
[@0: The dog eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "mouse" "+")
@0: The bear eats the lion.[(triple1)] The bear sees the dog.[(triple2)] The dog sees the lion.[(triple3)] The lion eats the dog.[(triple4)] The lion sees the bear.[(triple5)] The mouse does not like the dog.[(triple6)] The mouse sees the dog.[(triple7)] @1: The dog is round.[(((triple4) -> rule6))] The dog likes the mouse.[(((triple2) -> rule2) OR ((triple7) -> rule2))] The lion is rough.[(((triple5) -> rule9))] The lion is round.[(((triple1) -> rule4))] @2: The lion likes the lion.[(((((triple5) -> rule9)) -> rule8))] @3: The lion sees the mouse.[(((((((triple5) -> rule9)) -> rule8)) -> rule5))] @4: The mouse likes the bear.[(((((((((triple5) -> rule9)) -> rule8)) -> rule5)) -> rule7))] @5: The mouse is big.[(((((((((((triple5) -> rule9)) -> rule8)) -> rule5)) -> rule7)) -> rule3))]
The bear eats the lion.
("bear" "eats" "lion" "+")
triple1
The bear sees the dog.
("bear" "sees" "dog" "+")
triple2
The dog sees the lion.
("dog" "sees" "lion" "+")
triple3
The lion eats the dog.
("lion" "eats" "dog" "+")
triple4
The lion sees the bear.
("lion" "sees" "bear" "+")
triple5
The mouse does not like the dog.
("mouse" "likes" "dog" "-")
triple6
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple7
The dog is round.
("dog" "is" "round" "+")
((triple4) -> (rule6 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
((triple2) -> (rule2 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
((triple7) -> (rule2 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
((triple5) -> (rule9 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is round.
("lion" "is" "round" "+")
((triple1) -> (rule4 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
((((triple5) -> (rule9 % int2))) -> (rule8 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion sees the mouse.
("lion" "sees" "mouse" "+")
((((((triple5) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3
The mouse likes the bear.
("mouse" "likes" "bear" "+")
((((((((triple5) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
int3
The lion is rough.
("lion" "is" "rough" "+")
int4
The mouse is big.
("mouse" "is" "big" "+")
((((((((((triple5) -> (rule9 % int5))) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int2
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int3
The lion likes the lion.
("lion" "likes" "lion" "+")
int4
The lion is rough.
("lion" "is" "rough" "+")
int5