The cow is young. The cow needs the dog. The cow needs the lion. The dog is young. The dog likes the mouse. The lion is kind. The lion is young. The lion likes the dog. The lion likes the mouse. The mouse is nice. The mouse visits the dog. The mouse visits the lion. If something is kind then it likes the mouse. If something likes the mouse and it needs the lion then the lion visits the mouse. If something likes the dog and it is big then the dog needs the lion. If something is kind and it needs the dog then the dog likes the lion. If the cow visits the dog and the dog visits the cow then the dog likes the lion. If something is big and it needs the mouse then it is nice. If something needs the cow and it likes the mouse then the cow is big. If something likes the lion then the lion is big. If something visits the lion then the lion needs the dog.
The cow is young.
("cow" "is" "young" "+")
The cow needs the dog.
("cow" "needs" "dog" "+")
The cow needs the lion.
("cow" "needs" "lion" "+")
The dog is young.
("dog" "is" "young" "+")
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is young.
("lion" "is" "young" "+")
The lion likes the dog.
("lion" "likes" "dog" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
If something is kind then it likes the mouse.
((("something" "is" "kind" "+")) -> ("something" "likes" "mouse" "+"))
If something likes the mouse and it needs the lion then the lion visits the mouse.
((("something" "likes" "mouse" "+") ("something" "needs" "lion" "+")) -> ("lion" "visits" "mouse" "+"))
If something likes the dog and it is big then the dog needs the lion.
((("something" "likes" "dog" "+") ("something" "is" "big" "+")) -> ("dog" "needs" "lion" "+"))
If something is kind and it needs the dog then the dog likes the lion.
((("something" "is" "kind" "+") ("something" "needs" "dog" "+")) -> ("dog" "likes" "lion" "+"))
If the cow visits the dog and the dog visits the cow then the dog likes the lion.
((("cow" "visits" "dog" "+") ("dog" "visits" "cow" "+")) -> ("dog" "likes" "lion" "+"))
If something is big and it needs the mouse then it is nice.
((("something" "is" "big" "+") ("something" "needs" "mouse" "+")) -> ("something" "is" "nice" "+"))
If something needs the cow and it likes the mouse then the cow is big.
((("something" "needs" "cow" "+") ("something" "likes" "mouse" "+")) -> ("cow" "is" "big" "+"))
If something likes the lion then the lion is big.
((("something" "likes" "lion" "+")) -> ("lion" "is" "big" "+"))
If something visits the lion then the lion needs the dog.
((("something" "visits" "lion" "+")) -> ("lion" "needs" "dog" "+"))
The cow needs the dog.
True
1
proof
[(triple2)]
("cow" "needs" "dog" "+")
triple2
The mouse is not nice.
False
1
inv-proof
[(triple10)]
("mouse" "is" "nice" "-")
triple10
The lion needs the dog.
True
2
proof
[(((triple12) -> rule9))]
("lion" "needs" "dog" "+")
((triple12) -> (rule9 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion does not need the dog.
False
2
inv-proof
[(((triple12) -> rule9))]
("lion" "needs" "dog" "-")
((triple12) -> (rule9 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The dog likes the lion.
True
4
proof
[(((triple6 ((triple12) -> rule9)) -> rule4))]
("dog" "likes" "lion" "+")
((triple6 ((triple12) -> (rule9 % int2))) -> (rule4 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The lion needs the dog.
("lion" "needs" "dog" "+")
int2
The dog does not like the lion.
False
4
inv-proof
[(((triple6 ((triple12) -> rule9)) -> rule4))]
("dog" "likes" "lion" "-")
((triple6 ((triple12) -> (rule9 % int2))) -> (rule4 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The lion needs the dog.
("lion" "needs" "dog" "+")
int2
The lion is big.
True
5
proof
[(((((triple6 ((triple12) -> rule9)) -> rule4)) -> rule8))]
("lion" "is" "big" "+")
((((triple6 ((triple12) -> (rule9 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The dog likes the lion.
("dog" "likes" "lion" "+")
int2
The lion needs the dog.
("lion" "needs" "dog" "+")
int3
The lion is not big.
False
5
inv-proof
[(((((triple6 ((triple12) -> rule9)) -> rule4)) -> rule8))]
("lion" "is" "big" "-")
((((triple6 ((triple12) -> (rule9 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The dog likes the lion.
("dog" "likes" "lion" "+")
int2
The lion needs the dog.
("lion" "needs" "dog" "+")
int3
The dog needs the lion.
True
7
proof
[(((triple8 ((((triple6 ((triple12) -> rule9)) -> rule4)) -> rule8)) -> rule3))]
("dog" "needs" "lion" "+")
((triple8 ((((triple6 ((triple12) -> (rule9 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The dog needs the lion.
("dog" "needs" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The dog likes the lion.
("dog" "likes" "lion" "+")
int3
The lion needs the dog.
("lion" "needs" "dog" "+")
int4
The dog does not need the lion.
False
7
inv-proof
[(((triple8 ((((triple6 ((triple12) -> rule9)) -> rule4)) -> rule8)) -> rule3))]
("dog" "needs" "lion" "-")
((triple8 ((((triple6 ((triple12) -> (rule9 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The dog needs the lion.
("dog" "needs" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The dog likes the lion.
("dog" "likes" "lion" "+")
int3
The lion needs the dog.
("lion" "needs" "dog" "+")
int4
The lion visits the mouse.
True
9
proof
[(((triple5 ((triple8 ((((triple6 ((triple12) -> rule9)) -> rule4)) -> rule8)) -> rule3)) -> rule2))]
("lion" "visits" "mouse" "+")
((triple5 ((triple8 ((((triple6 ((triple12) -> (rule9 % int5))) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The dog likes the lion.
("dog" "likes" "lion" "+")
int4
The lion needs the dog.
("lion" "needs" "dog" "+")
int5
The lion does not visit the mouse.
False
9
inv-proof
[(((triple5 ((triple8 ((((triple6 ((triple12) -> rule9)) -> rule4)) -> rule8)) -> rule3)) -> rule2))]
("lion" "visits" "mouse" "-")
((triple5 ((triple8 ((((triple6 ((triple12) -> (rule9 % int5))) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The dog likes the lion.
("dog" "likes" "lion" "+")
int4
The lion needs the dog.
("lion" "needs" "dog" "+")
int5
The cow does not like the mouse.
Unknown
inv-rconc
[@1: The cow likes the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "likes" "mouse" "-")
The mouse likes the mouse.
Unknown
rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "likes" "mouse" "+")
The cow is not nice.
Unknown
inv-rconc
[@1: The cow is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "is" "nice" "-")
The dog is nice.
Unknown
rconc
[@1: The dog is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "is" "nice" "+")
The cow is not big.
Unknown
inv-rconc
[@1: The cow is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "is" "big" "-")
The lion is nice.
Unknown
rconc
[@1: The lion is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "is" "nice" "+")
The cow does not like the cow.
Unknown
inv-random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
The dog does not like the dog.
Unknown
inv-random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "-")
The mouse is round.
Unknown
random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "+")
The cow does not visit the dog.
Unknown
inv-random
[@0: The cow visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "dog" "-")
The mouse needs the dog.
Unknown
random
[@0: The mouse needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "dog" "+")
@0: The cow is young.[(triple1)] The cow needs the dog.[(triple2)] The cow needs the lion.[(triple3)] The dog is young.[(triple4)] The dog likes the mouse.[(triple5)] The lion is kind.[(triple6)] The lion is young.[(triple7)] The lion likes the dog.[(triple8)] The lion likes the mouse.[(triple9 OR ((triple6) -> rule1))] The mouse is nice.[(triple10)] The mouse visits the dog.[(triple11)] The mouse visits the lion.[(triple12)] @1: The lion needs the dog.[(((triple12) -> rule9))] @2: The dog likes the lion.[(((triple6 ((triple12) -> rule9)) -> rule4))] @3: The lion is big.[(((((triple6 ((triple12) -> rule9)) -> rule4)) -> rule8))] @4: The dog needs the lion.[(((triple8 ((((triple6 ((triple12) -> rule9)) -> rule4)) -> rule8)) -> rule3))] @5: The lion visits the mouse.[(((triple5 ((triple8 ((((triple6 ((triple12) -> rule9)) -> rule4)) -> rule8)) -> rule3)) -> rule2))]
The cow is young.
("cow" "is" "young" "+")
triple1
The cow needs the dog.
("cow" "needs" "dog" "+")
triple2
The cow needs the lion.
("cow" "needs" "lion" "+")
triple3
The dog is young.
("dog" "is" "young" "+")
triple4
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple5
The lion is kind.
("lion" "is" "kind" "+")
triple6
The lion is young.
("lion" "is" "young" "+")
triple7
The lion likes the dog.
("lion" "likes" "dog" "+")
triple8
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple9
((triple6) -> (rule1 % int1))
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
triple10
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple11
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple12
The lion needs the dog.
("lion" "needs" "dog" "+")
((triple12) -> (rule9 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The dog likes the lion.
("dog" "likes" "lion" "+")
((triple6 ((triple12) -> (rule9 % int2))) -> (rule4 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The lion needs the dog.
("lion" "needs" "dog" "+")
int2
The lion is big.
("lion" "is" "big" "+")
((((triple6 ((triple12) -> (rule9 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The dog likes the lion.
("dog" "likes" "lion" "+")
int2
The lion needs the dog.
("lion" "needs" "dog" "+")
int3
The dog needs the lion.
("dog" "needs" "lion" "+")
((triple8 ((((triple6 ((triple12) -> (rule9 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The dog needs the lion.
("dog" "needs" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The dog likes the lion.
("dog" "likes" "lion" "+")
int3
The lion needs the dog.
("lion" "needs" "dog" "+")
int4
The lion visits the mouse.
("lion" "visits" "mouse" "+")
((triple5 ((triple8 ((((triple6 ((triple12) -> (rule9 % int5))) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The dog likes the lion.
("dog" "likes" "lion" "+")
int4
The lion needs the dog.
("lion" "needs" "dog" "+")
int5