The cow is red. The dog is big. The dog is red. The dog needs the lion. The lion is nice. The mouse likes the dog. The mouse likes the lion. If someone visits the cow and the cow is big then the cow is not red. If someone visits the dog then the dog is rough. If someone needs the lion and they are not nice then the lion likes the dog. If someone visits the lion then they visit the dog. If someone is red then they visit the lion. If someone likes the mouse and the mouse needs the cow then the mouse needs the lion.
The cow is red.
("cow" "is" "red" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is red.
("dog" "is" "red" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The lion is nice.
("lion" "is" "nice" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
If someone visits the cow and the cow is big then the cow is not red.
((("someone" "visits" "cow" "+") ("cow" "is" "big" "+")) -> ("cow" "is" "red" "-"))
If someone visits the dog then the dog is rough.
((("someone" "visits" "dog" "+")) -> ("dog" "is" "rough" "+"))
If someone needs the lion and they are not nice then the lion likes the dog.
((("someone" "needs" "lion" "+") ("someone" "is" "nice" "~")) -> ("lion" "likes" "dog" "+"))
If someone visits the lion then they visit the dog.
((("someone" "visits" "lion" "+")) -> ("someone" "visits" "dog" "+"))
If someone is red then they visit the lion.
((("someone" "is" "red" "+")) -> ("someone" "visits" "lion" "+"))
If someone likes the mouse and the mouse needs the cow then the mouse needs the lion.
((("someone" "likes" "mouse" "+") ("mouse" "needs" "cow" "+")) -> ("mouse" "needs" "lion" "+"))
The dog is big.
True
1
proof
[(triple2)]
("dog" "is" "big" "+")
triple2
The dog does not need the lion.
False
1
inv-proof
[(triple4)]
("dog" "needs" "lion" "-")
triple4
The cow visits the lion.
True
2
proof
[(((triple1) -> rule5))]
("cow" "visits" "lion" "+")
((triple1) -> (rule5 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The dog does not visit the lion.
False
2
inv-proof
[(((triple3) -> rule5))]
("dog" "visits" "lion" "-")
((triple3) -> (rule5 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
The cow visits the dog.
True
3
proof
[(((((triple1) -> rule5)) -> rule4))]
("cow" "visits" "dog" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow visits the lion.
("cow" "visits" "lion" "+")
int2
The cow does not visit the dog.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule4))]
("cow" "visits" "dog" "-")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow visits the lion.
("cow" "visits" "lion" "+")
int2
The dog is rough.
True
4
proof
[(((((((triple1) -> rule5)) -> rule4)) -> rule2) OR ((((((triple3) -> rule5)) -> rule4)) -> rule2))]
("dog" "is" "rough" "+")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The cow visits the dog.
("cow" "visits" "dog" "+")
int2
The cow visits the lion.
("cow" "visits" "lion" "+")
int3
((((((triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog visits the lion.
("dog" "visits" "lion" "+")
int3
The dog is not rough.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule4)) -> rule2) OR ((((((triple3) -> rule5)) -> rule4)) -> rule2))]
("dog" "is" "rough" "-")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The cow visits the dog.
("cow" "visits" "dog" "+")
int2
The cow visits the lion.
("cow" "visits" "lion" "+")
int3
((((((triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog visits the lion.
("dog" "visits" "lion" "+")
int3
The mouse does not visit the lion.
Unknown
inv-rconc
[@1: The mouse visits the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "visits" "lion" "-")
The lion visits the lion.
Unknown
rconc
[@1: The lion visits the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "visits" "lion" "+")
The mouse does not need the lion.
Unknown
inv-rconc
[@1: The mouse needs the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "needs" "lion" "-")
The mouse visits the dog.
Unknown
rconc
[@2: The mouse visits the dog.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("mouse" "visits" "dog" "+")
The lion does not visit the cow.
Unknown
inv-random
[@0: The lion visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "cow" "-")
The lion is red.
Unknown
random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
@0: The cow is red.[(triple1)] The dog is big.[(triple2)] The dog is red.[(triple3)] The dog needs the lion.[(triple4)] The lion is nice.[(triple5)] The mouse likes the dog.[(triple6)] The mouse likes the lion.[(triple7)] @1: The cow visits the lion.[(((triple1) -> rule5))] The dog visits the lion.[(((triple3) -> rule5))] @2: The cow visits the dog.[(((((triple1) -> rule5)) -> rule4))] The dog visits the dog.[(((((triple3) -> rule5)) -> rule4))] @3: The dog is rough.[(((((((triple1) -> rule5)) -> rule4)) -> rule2) OR ((((((triple3) -> rule5)) -> rule4)) -> rule2))]
The cow is red.
("cow" "is" "red" "+")
triple1
The dog is big.
("dog" "is" "big" "+")
triple2
The dog is red.
("dog" "is" "red" "+")
triple3
The dog needs the lion.
("dog" "needs" "lion" "+")
triple4
The lion is nice.
("lion" "is" "nice" "+")
triple5
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple6
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple7
The cow visits the lion.
("cow" "visits" "lion" "+")
((triple1) -> (rule5 % int1))
The cow visits the lion.
("cow" "visits" "lion" "+")
int1
The dog visits the lion.
("dog" "visits" "lion" "+")
((triple3) -> (rule5 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
The cow visits the dog.
("cow" "visits" "dog" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow visits the lion.
("cow" "visits" "lion" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog visits the lion.
("dog" "visits" "lion" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The cow visits the dog.
("cow" "visits" "dog" "+")
int2
The cow visits the lion.
("cow" "visits" "lion" "+")
int3
((((((triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog visits the lion.
("dog" "visits" "lion" "+")
int3