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