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