The cat is nice. The cat needs the dog. The dog is blue. The dog likes the tiger. The dog sees the mouse. The dog sees the tiger. The mouse is young. The mouse likes the cat. The mouse likes the dog. The mouse needs the cat. The mouse sees the dog. The mouse sees the tiger. The tiger is not red. The tiger likes the dog. The tiger sees the cat. The tiger does not see the dog. If someone likes the tiger then the tiger is blue. If someone needs the cat and they are not nice then they like the cat. If someone sees the cat and they need the dog then the dog needs the mouse. If someone needs the mouse then the mouse is not red. If someone is blue then they need the dog. If someone likes the cat and they see the mouse then the cat likes the mouse.
The cat is nice.
("cat" "is" "nice" "+")
The cat needs the dog.
("cat" "needs" "dog" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger is not red.
("tiger" "is" "red" "-")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
The tiger does not see the dog.
("tiger" "sees" "dog" "-")
If someone likes the tiger then the tiger is blue.
((("someone" "likes" "tiger" "+")) -> ("tiger" "is" "blue" "+"))
If someone needs the cat and they are not nice then they like the cat.
((("someone" "needs" "cat" "+") ("someone" "is" "nice" "~")) -> ("someone" "likes" "cat" "+"))
If someone sees the cat and they need the dog then the dog needs the mouse.
((("someone" "sees" "cat" "+") ("someone" "needs" "dog" "+")) -> ("dog" "needs" "mouse" "+"))
If someone needs the mouse then the mouse is not red.
((("someone" "needs" "mouse" "+")) -> ("mouse" "is" "red" "-"))
If someone is blue then they need the dog.
((("someone" "is" "blue" "+")) -> ("someone" "needs" "dog" "+"))
If someone likes the cat and they see the mouse then the cat likes the mouse.
((("someone" "likes" "cat" "+") ("someone" "sees" "mouse" "+")) -> ("cat" "likes" "mouse" "+"))
The tiger is not red.
True
1
proof
[(triple13)]
("tiger" "is" "red" "-")
triple13
The mouse does not like the dog.
False
1
inv-proof
[(triple9)]
("mouse" "likes" "dog" "-")
triple9
The dog needs the dog.
True
2
proof
[(((triple3) -> rule5))]
("dog" "needs" "dog" "+")
((triple3) -> (rule5 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The tiger is not blue.
False
2
inv-proof
[(((triple4) -> rule1))]
("tiger" "is" "blue" "-")
((triple4) -> (rule1 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger needs the dog.
True
3
proof
[(((((triple4) -> rule1)) -> rule5))]
("tiger" "needs" "dog" "+")
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger does not need the dog.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule5))]
("tiger" "needs" "dog" "-")
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The dog needs the mouse.
True
5
proof
[(((triple15 ((((triple4) -> rule1)) -> rule5)) -> rule3))]
("dog" "needs" "mouse" "+")
((triple15 ((((triple4) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3
The dog does not need the mouse.
False
5
inv-proof
[(((triple15 ((((triple4) -> rule1)) -> rule5)) -> rule3))]
("dog" "needs" "mouse" "-")
((triple15 ((((triple4) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3
The dog does not like the cat.
Unknown
inv-rconc
[@1: The dog likes the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "likes" "cat" "-")
The cat likes the cat.
Unknown
rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "likes" "cat" "+")
The cat does not like the mouse.
Unknown
inv-rconc
[@2: The cat likes the mouse.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("cat" "likes" "mouse" "-")
The mouse needs the dog.
Unknown
rconc
[@1: The mouse needs the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "needs" "dog" "+")
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 dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
The cat does not see the dog.
Unknown
inv-random
[@0: The cat sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "dog" "-")
The dog is young.
Unknown
random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "+")
@0: The cat is nice.[(triple1)] The cat needs the dog.[(triple2)] The dog is blue.[(triple3)] The dog likes the tiger.[(triple4)] The dog sees the mouse.[(triple5)] The dog sees the tiger.[(triple6)] The mouse is young.[(triple7)] The mouse likes the cat.[(triple8)] The mouse likes the dog.[(triple9)] The mouse needs the cat.[(triple10)] The mouse sees the dog.[(triple11)] The mouse sees the tiger.[(triple12)] The tiger does not see the dog.[(triple16)] The tiger is not red.[(triple13)] The tiger likes the dog.[(triple14)] The tiger sees the cat.[(triple15)] @1: The dog needs the dog.[(((triple3) -> rule5))] The tiger is blue.[(((triple4) -> rule1))] @2: The tiger needs the dog.[(((((triple4) -> rule1)) -> rule5))] @3: The dog needs the mouse.[(((triple15 ((((triple4) -> rule1)) -> rule5)) -> rule3))] @4: The mouse is not red.[(((((triple15 ((((triple4) -> rule1)) -> rule5)) -> rule3)) -> rule4))]
The cat is nice.
("cat" "is" "nice" "+")
triple1
The cat needs the dog.
("cat" "needs" "dog" "+")
triple2
The dog is blue.
("dog" "is" "blue" "+")
triple3
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple4
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple5
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple6
The mouse is young.
("mouse" "is" "young" "+")
triple7
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple8
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple9
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple10
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple11
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple12
The tiger does not see the dog.
("tiger" "sees" "dog" "-")
triple16
The tiger is not red.
("tiger" "is" "red" "-")
triple13
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple14
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple15
The dog needs the dog.
("dog" "needs" "dog" "+")
((triple3) -> (rule5 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
((triple4) -> (rule1 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
((triple15 ((((triple4) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3
The mouse is not red.
("mouse" "is" "red" "-")
((((triple15 ((((triple4) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The mouse is not red.
("mouse" "is" "red" "-")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int3
The tiger is blue.
("tiger" "is" "blue" "+")
int4