The cow is big. The dog is rough. The dog likes the lion. The lion is rough. The tiger is big. The tiger is not green. The tiger sees the lion. If something likes the dog then the dog sees the tiger. If something needs the dog and it does not see the lion then it likes the dog. If something likes the tiger then it likes the dog. If something needs the lion and the lion is big then it is not rough. If something likes the lion then the lion likes the tiger. If the cow likes the dog and the cow is not big then the dog needs the lion.
The cow is big.
("cow" "is" "big" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog likes the lion.
("dog" "likes" "lion" "+")
The lion is rough.
("lion" "is" "rough" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is not green.
("tiger" "is" "green" "-")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If something likes the dog then the dog sees the tiger.
((("something" "likes" "dog" "+")) -> ("dog" "sees" "tiger" "+"))
If something needs the dog and it does not see the lion then it likes the dog.
((("something" "needs" "dog" "+") ("something" "sees" "lion" "~")) -> ("something" "likes" "dog" "+"))
If something likes the tiger then it likes the dog.
((("something" "likes" "tiger" "+")) -> ("something" "likes" "dog" "+"))
If something needs the lion and the lion is big then it is not rough.
((("something" "needs" "lion" "+") ("lion" "is" "big" "+")) -> ("something" "is" "rough" "-"))
If something likes the lion then the lion likes the tiger.
((("something" "likes" "lion" "+")) -> ("lion" "likes" "tiger" "+"))
If the cow likes the dog and the cow is not big then the dog needs the lion.
((("cow" "likes" "dog" "+") ("cow" "is" "big" "~")) -> ("dog" "needs" "lion" "+"))
The tiger is big.
True
1
proof
[(triple5)]
("tiger" "is" "big" "+")
triple5
The tiger does not see the lion.
False
1
inv-proof
[(triple7)]
("tiger" "sees" "lion" "-")
triple7
The lion likes the tiger.
True
2
proof
[(((triple3) -> rule5))]
("lion" "likes" "tiger" "+")
((triple3) -> (rule5 % int1))
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int1
The lion does not like the tiger.
False
2
inv-proof
[(((triple3) -> rule5))]
("lion" "likes" "tiger" "-")
((triple3) -> (rule5 % int1))
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int1
The lion likes the dog.
True
3
proof
[(((((triple3) -> rule5)) -> rule3))]
("lion" "likes" "dog" "+")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The lion likes the dog.
("lion" "likes" "dog" "+")
int1
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int2
The lion does not like the dog.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule3))]
("lion" "likes" "dog" "-")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The lion likes the dog.
("lion" "likes" "dog" "+")
int1
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int2
The dog sees the tiger.
True
4
proof
[(((((((triple3) -> rule5)) -> rule3)) -> rule1))]
("dog" "sees" "tiger" "+")
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1
The lion likes the dog.
("lion" "likes" "dog" "+")
int2
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int3
The dog does not see the tiger.
False
4
inv-proof
[(((((((triple3) -> rule5)) -> rule3)) -> rule1))]
("dog" "sees" "tiger" "-")
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1
The lion likes the dog.
("lion" "likes" "dog" "+")
int2
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int3
The dog does not need the lion.
Unknown
inv-rconc
[@1: The dog needs the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "needs" "lion" "-")
The dog likes the dog.
Unknown
rconc
[@1: The dog likes the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "likes" "dog" "+")
The cow does not like the dog.
Unknown
inv-rconc
[@1: The cow likes the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "likes" "dog" "-")
The tiger likes the dog.
Unknown
rconc
[@1: The tiger likes the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "likes" "dog" "+")
The dog is not green.
Unknown
inv-random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "-")
The tiger sees the cow.
Unknown
random
[@0: The tiger sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "cow" "+")
The cow is not rough.
Unknown
inv-random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "-")
The dog sees the lion.
Unknown
random
[@0: The dog sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "lion" "+")
@0: The cow is big.[(triple1)] The dog is rough.[(triple2)] The dog likes the lion.[(triple3)] The lion is rough.[(triple4)] The tiger is big.[(triple5)] The tiger is not green.[(triple6)] The tiger sees the lion.[(triple7)] @1: The lion likes the tiger.[(((triple3) -> rule5))] @2: The lion likes the dog.[(((((triple3) -> rule5)) -> rule3))] @3: The dog sees the tiger.[(((((((triple3) -> rule5)) -> rule3)) -> rule1))]
The cow is big.
("cow" "is" "big" "+")
triple1
The dog is rough.
("dog" "is" "rough" "+")
triple2
The dog likes the lion.
("dog" "likes" "lion" "+")
triple3
The lion is rough.
("lion" "is" "rough" "+")
triple4
The tiger is big.
("tiger" "is" "big" "+")
triple5
The tiger is not green.
("tiger" "is" "green" "-")
triple6
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple7
The lion likes the tiger.
("lion" "likes" "tiger" "+")
((triple3) -> (rule5 % int1))
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int1
The lion likes the dog.
("lion" "likes" "dog" "+")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The lion likes the dog.
("lion" "likes" "dog" "+")
int1
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int2
The dog sees the tiger.
("dog" "sees" "tiger" "+")
((((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1
The lion likes the dog.
("lion" "likes" "dog" "+")
int2
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int3