The cat likes the mouse. The cat sees the dog. The cat does not see the lion. The dog sees the lion. The lion does not eat the dog. The lion does not like the dog. The mouse eats the cat. The mouse is cold. The mouse is red. The mouse sees the cat. If something sees the lion then it likes the cat. If something sees the lion then it is not nice. If the dog does not see the cat and the cat does not like the lion then the cat sees the dog. If something is nice and it eats the mouse then the mouse sees the dog. If something likes the cat then it eats the mouse. If something eats the mouse then the mouse sees the lion.
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cat sees the dog.
("cat" "sees" "dog" "+")
The cat does not see the lion.
("cat" "sees" "lion" "-")
The dog sees the lion.
("dog" "sees" "lion" "+")
The lion does not eat the dog.
("lion" "eats" "dog" "-")
The lion does not like the dog.
("lion" "likes" "dog" "-")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
If something sees the lion then it likes the cat.
((("something" "sees" "lion" "+")) -> ("something" "likes" "cat" "+"))
If something sees the lion then it is not nice.
((("something" "sees" "lion" "+")) -> ("something" "is" "nice" "-"))
If the dog does not see the cat and the cat does not like the lion then the cat sees the dog.
((("dog" "sees" "cat" "~") ("cat" "likes" "lion" "~")) -> ("cat" "sees" "dog" "+"))
If something is nice and it eats the mouse then the mouse sees the dog.
((("something" "is" "nice" "+") ("something" "eats" "mouse" "+")) -> ("mouse" "sees" "dog" "+"))
If something likes the cat then it eats the mouse.
((("something" "likes" "cat" "+")) -> ("something" "eats" "mouse" "+"))
If something eats the mouse then the mouse sees the lion.
((("something" "eats" "mouse" "+")) -> ("mouse" "sees" "lion" "+"))
The cat sees the dog.
True
1
proof
[(triple2)]
("cat" "sees" "dog" "+")
triple2
The lion likes the dog.
False
1
inv-proof
[(triple6)]
("lion" "likes" "dog" "+")
triple6
The dog likes the cat.
True
2
proof
[(((triple4) -> rule1))]
("dog" "likes" "cat" "+")
((triple4) -> (rule1 % int1))
The dog likes the cat.
("dog" "likes" "cat" "+")
int1
The dog does not like the cat.
False
2
inv-proof
[(((triple4) -> rule1))]
("dog" "likes" "cat" "-")
((triple4) -> (rule1 % int1))
The dog likes the cat.
("dog" "likes" "cat" "+")
int1
The dog eats the mouse.
True
3
proof
[(((((triple4) -> rule1)) -> rule5))]
("dog" "eats" "mouse" "+")
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The dog likes the cat.
("dog" "likes" "cat" "+")
int2
The dog does not eat the mouse.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule5))]
("dog" "eats" "mouse" "-")
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The dog likes the cat.
("dog" "likes" "cat" "+")
int2
The mouse sees the lion.
True
4
proof
[(((((((triple4) -> rule1)) -> rule5)) -> rule6))]
("mouse" "sees" "lion" "+")
((((((triple4) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
The dog likes the cat.
("dog" "likes" "cat" "+")
int3
The mouse does not see the lion.
False
4
inv-proof
[(((((((triple4) -> rule1)) -> rule5)) -> rule6))]
("mouse" "sees" "lion" "-")
((((((triple4) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
The dog likes the cat.
("dog" "likes" "cat" "+")
int3
The mouse is not nice.
True
5
proof
[(((((((((triple4) -> rule1)) -> rule5)) -> rule6)) -> rule2))]
("mouse" "is" "nice" "-")
((((((((triple4) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is not nice.
("mouse" "is" "nice" "-")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int2
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int3
The dog likes the cat.
("dog" "likes" "cat" "+")
int4
The mouse does not like the cat.
False
5
inv-proof
[(((((((((triple4) -> rule1)) -> rule5)) -> rule6)) -> rule1))]
("mouse" "likes" "cat" "-")
((((((((triple4) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int2
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int3
The dog likes the cat.
("dog" "likes" "cat" "+")
int4
The mouse eats the mouse.
True
6
proof
[(((((((((((triple4) -> rule1)) -> rule5)) -> rule6)) -> rule1)) -> rule5))]
("mouse" "eats" "mouse" "+")
((((((((((triple4) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int2
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int3
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int4
The dog likes the cat.
("dog" "likes" "cat" "+")
int5
The mouse does not eat the mouse.
False
6
inv-proof
[(((((((((((triple4) -> rule1)) -> rule5)) -> rule6)) -> rule1)) -> rule5))]
("mouse" "eats" "mouse" "-")
((((((((((triple4) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int2
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int3
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int4
The dog likes the cat.
("dog" "likes" "cat" "+")
int5
The mouse does not see the dog.
Unknown
inv-rconc
[@1: The mouse sees the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "sees" "dog" "-")
The cat likes the cat.
Unknown
rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "cat" "+")
The cat does not eat the mouse.
Unknown
inv-rconc
[@2: The cat eats the mouse.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("cat" "eats" "mouse" "-")
The lion eats the mouse.
Unknown
rconc
[@2: The lion eats the mouse.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("lion" "eats" "mouse" "+")
The lion does not like the cat.
Unknown
inv-rconc
[@1: The lion likes the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "likes" "cat" "-")
The dog eats the cat.
Unknown
random
[@0: The dog eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "cat" "+")
The dog is not red.
Unknown
inv-random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
The dog does not see the mouse.
Unknown
inv-random
[@0: The dog sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "mouse" "-")
The lion is big.
Unknown
random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "+")
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 is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
@0: The cat does not see the lion.[(triple3)] The cat likes the mouse.[(triple1)] The cat sees the dog.[(triple2)] The dog sees the lion.[(triple4)] The lion does not eat the dog.[(triple5)] The lion does not like the dog.[(triple6)] The mouse eats the cat.[(triple7)] The mouse is cold.[(triple8)] The mouse is red.[(triple9)] The mouse sees the cat.[(triple10)] @1: The dog is not nice.[(((triple4) -> rule2))] The dog likes the cat.[(((triple4) -> rule1))] @2: The dog eats the mouse.[(((((triple4) -> rule1)) -> rule5))] @3: The mouse sees the lion.[(((((((triple4) -> rule1)) -> rule5)) -> rule6))] @4: The mouse is not nice.[(((((((((triple4) -> rule1)) -> rule5)) -> rule6)) -> rule2))] The mouse likes the cat.[(((((((((triple4) -> rule1)) -> rule5)) -> rule6)) -> rule1))] @5: The mouse eats the mouse.[(((((((((((triple4) -> rule1)) -> rule5)) -> rule6)) -> rule1)) -> rule5))]
The cat does not see the lion.
("cat" "sees" "lion" "-")
triple3
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple1
The cat sees the dog.
("cat" "sees" "dog" "+")
triple2
The dog sees the lion.
("dog" "sees" "lion" "+")
triple4
The lion does not eat the dog.
("lion" "eats" "dog" "-")
triple5
The lion does not like the dog.
("lion" "likes" "dog" "-")
triple6
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple7
The mouse is cold.
("mouse" "is" "cold" "+")
triple8
The mouse is red.
("mouse" "is" "red" "+")
triple9
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple10
The dog is not nice.
("dog" "is" "nice" "-")
((triple4) -> (rule2 % int1))
The dog is not nice.
("dog" "is" "nice" "-")
int1
The dog likes the cat.
("dog" "likes" "cat" "+")
((triple4) -> (rule1 % int1))
The dog likes the cat.
("dog" "likes" "cat" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
((((triple4) -> (rule1 % int2))) -> (rule5 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The dog likes the cat.
("dog" "likes" "cat" "+")
int2
The mouse sees the lion.
("mouse" "sees" "lion" "+")
((((((triple4) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
The dog likes the cat.
("dog" "likes" "cat" "+")
int3
The mouse is not nice.
("mouse" "is" "nice" "-")
((((((((triple4) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is not nice.
("mouse" "is" "nice" "-")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int2
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int3
The dog likes the cat.
("dog" "likes" "cat" "+")
int4
The mouse likes the cat.
("mouse" "likes" "cat" "+")
((((((((triple4) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int2
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int3
The dog likes the cat.
("dog" "likes" "cat" "+")
int4
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((((((((((triple4) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int2
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int3
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int4
The dog likes the cat.
("dog" "likes" "cat" "+")
int5