The dog eats the mouse. The dog is cold. The dog is young. The mouse eats the dog. The mouse is big. The mouse does not like the dog. The mouse needs the dog. If someone likes the mouse then they are rough. If someone eats the dog and the dog is young then the dog likes the mouse. If someone eats the dog then the dog likes the mouse. If someone is cold then they do not eat the dog. If someone likes the dog and they are rough then the dog eats the mouse. If someone likes the mouse then they are big. If someone needs the mouse and the mouse is not young then the mouse does not need the dog. If someone is big and they do not eat the dog then they need the mouse.
The dog eats the mouse.
("dog" "eats" "mouse" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is young.
("dog" "is" "young" "+")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse does not like the dog.
("mouse" "likes" "dog" "-")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
If someone likes the mouse then they are rough.
((("someone" "likes" "mouse" "+")) -> ("someone" "is" "rough" "+"))
If someone eats the dog and the dog is young then the dog likes the mouse.
((("someone" "eats" "dog" "+") ("dog" "is" "young" "+")) -> ("dog" "likes" "mouse" "+"))
If someone eats the dog then the dog likes the mouse.
((("someone" "eats" "dog" "+")) -> ("dog" "likes" "mouse" "+"))
If someone is cold then they do not eat the dog.
((("someone" "is" "cold" "+")) -> ("someone" "eats" "dog" "-"))
If someone likes the dog and they are rough then the dog eats the mouse.
((("someone" "likes" "dog" "+") ("someone" "is" "rough" "+")) -> ("dog" "eats" "mouse" "+"))
If someone likes the mouse then they are big.
((("someone" "likes" "mouse" "+")) -> ("someone" "is" "big" "+"))
If someone needs the mouse and the mouse is not young then the mouse does not need the dog.
((("someone" "needs" "mouse" "+") ("mouse" "is" "young" "~")) -> ("mouse" "needs" "dog" "-"))
If someone is big and they do not eat the dog then they need the mouse.
((("someone" "is" "big" "+") ("someone" "eats" "dog" "~")) -> ("someone" "needs" "mouse" "+"))
The dog eats the mouse.
True
1
proof
[(triple1)]
("dog" "eats" "mouse" "+")
triple1
The mouse is not big.
False
1
inv-proof
[(triple5)]
("mouse" "is" "big" "-")
triple5
The dog likes the mouse.
True
2
proof
[(((triple4) -> rule3) OR ((triple4 triple3) -> rule2))]
("dog" "likes" "mouse" "+")
((triple4) -> (rule3 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
((triple4 triple3) -> (rule2 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The dog eats the dog.
False
2
inv-proof
[(((triple2) -> rule4))]
("dog" "eats" "dog" "+")
((triple2) -> (rule4 % int1))
The dog does not eat the dog.
("dog" "eats" "dog" "-")
int1
The dog is rough.
True
3
proof
[(((((triple4) -> rule3)) -> rule1) OR ((((triple4 triple3) -> rule2)) -> rule1))]
("dog" "is" "rough" "+")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
((((triple4 triple3) -> (rule2 % int2))) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The dog is not big.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule6) OR ((((triple4 triple3) -> rule2)) -> rule6))]
("dog" "is" "big" "-")
((((triple4) -> (rule3 % int2))) -> (rule6 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
((((triple4 triple3) -> (rule2 % int2))) -> (rule6 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The dog needs the mouse.
True
6
proof
[(((((((triple4) -> rule3)) -> rule6) ((triple2) -> rule4)) -> rule8) OR ((((((triple4 triple3) -> rule2)) -> rule6) ((triple2) -> rule4)) -> rule8))]
("dog" "needs" "mouse" "+")
((((((triple4) -> (rule3 % int4))) -> (rule6 % int3)) ((triple2) -> (rule4 % int2))) -> (rule8 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The dog does not eat the dog.
("dog" "eats" "dog" "-")
int2
The dog is big.
("dog" "is" "big" "+")
int3
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int4
((((((triple4 triple3) -> (rule2 % int4))) -> (rule6 % int3)) ((triple2) -> (rule4 % int2))) -> (rule8 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The dog does not eat the dog.
("dog" "eats" "dog" "-")
int2
The dog is big.
("dog" "is" "big" "+")
int3
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int4
The dog does not need the mouse.
False
6
inv-proof
[(((((((triple4) -> rule3)) -> rule6) ((triple2) -> rule4)) -> rule8) OR ((((((triple4 triple3) -> rule2)) -> rule6) ((triple2) -> rule4)) -> rule8))]
("dog" "needs" "mouse" "-")
((((((triple4) -> (rule3 % int4))) -> (rule6 % int3)) ((triple2) -> (rule4 % int2))) -> (rule8 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The dog does not eat the dog.
("dog" "eats" "dog" "-")
int2
The dog is big.
("dog" "is" "big" "+")
int3
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int4
((((((triple4 triple3) -> (rule2 % int4))) -> (rule6 % int3)) ((triple2) -> (rule4 % int2))) -> (rule8 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The dog does not eat the dog.
("dog" "eats" "dog" "-")
int2
The dog is big.
("dog" "is" "big" "+")
int3
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int4
The mouse is not rough.
Unknown
inv-rconc
[@1: The mouse is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "rough" "-")
The mouse needs the mouse.
Unknown
rconc
[@1: The mouse needs the mouse.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "needs" "mouse" "+")
The mouse is not kind.
Unknown
inv-random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
@0: The dog eats the mouse.[(triple1)] The dog is cold.[(triple2)] The dog is young.[(triple3)] The mouse does not like the dog.[(triple6)] The mouse eats the dog.[(triple4)] The mouse is big.[(triple5)] The mouse needs the dog.[(triple7)] @1: The dog does not eat the dog.[(((triple2) -> rule4))] The dog likes the mouse.[(((triple4) -> rule3) OR ((triple4 triple3) -> rule2))] @2: The dog is big.[(((((triple4) -> rule3)) -> rule6) OR ((((triple4 triple3) -> rule2)) -> rule6))] The dog is rough.[(((((triple4) -> rule3)) -> rule1) OR ((((triple4 triple3) -> rule2)) -> rule1))] @3: The dog needs the mouse.[(((((((triple4) -> rule3)) -> rule6) ((triple2) -> rule4)) -> rule8) OR ((((((triple4 triple3) -> rule2)) -> rule6) ((triple2) -> rule4)) -> rule8))]
The dog eats the mouse.
("dog" "eats" "mouse" "+")
triple1
The dog is cold.
("dog" "is" "cold" "+")
triple2
The dog is young.
("dog" "is" "young" "+")
triple3
The mouse does not like the dog.
("mouse" "likes" "dog" "-")
triple6
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple4
The mouse is big.
("mouse" "is" "big" "+")
triple5
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple7
The dog does not eat the dog.
("dog" "eats" "dog" "-")
((triple2) -> (rule4 % int1))
The dog does not eat the dog.
("dog" "eats" "dog" "-")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
((triple4) -> (rule3 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
((triple4 triple3) -> (rule2 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The dog is big.
("dog" "is" "big" "+")
((((triple4) -> (rule3 % int2))) -> (rule6 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
((((triple4 triple3) -> (rule2 % int2))) -> (rule6 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
((((triple4 triple3) -> (rule2 % int2))) -> (rule1 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
((((((triple4) -> (rule3 % int4))) -> (rule6 % int3)) ((triple2) -> (rule4 % int2))) -> (rule8 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The dog does not eat the dog.
("dog" "eats" "dog" "-")
int2
The dog is big.
("dog" "is" "big" "+")
int3
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int4
((((((triple4 triple3) -> (rule2 % int4))) -> (rule6 % int3)) ((triple2) -> (rule4 % int2))) -> (rule8 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The dog does not eat the dog.
("dog" "eats" "dog" "-")
int2
The dog is big.
("dog" "is" "big" "+")
int3
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int4