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