The dog chases the lion. The dog is rough. The lion needs the dog. All big people are cold. If the dog chases the lion then the lion likes the dog. If someone likes the lion then they chase the dog. If someone chases the dog then they like the lion. If someone is red and not cold then they do not need the dog. If someone likes the dog then the dog likes the lion. If someone is big and they need the dog then the dog does not like the lion. If someone chases the dog and they are big then they are rough.
The dog chases the lion.
("dog" "chases" "lion" "+")
The dog is rough.
("dog" "is" "rough" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
All big people are cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
If the dog chases the lion then the lion likes the dog.
((("dog" "chases" "lion" "+")) -> ("lion" "likes" "dog" "+"))
If someone likes the lion then they chase the dog.
((("someone" "likes" "lion" "+")) -> ("someone" "chases" "dog" "+"))
If someone chases the dog then they like the lion.
((("someone" "chases" "dog" "+")) -> ("someone" "likes" "lion" "+"))
If someone is red and not cold then they do not need the dog.
((("someone" "is" "red" "+") ("someone" "is" "cold" "~")) -> ("someone" "needs" "dog" "-"))
If someone likes the dog then the dog likes the lion.
((("someone" "likes" "dog" "+")) -> ("dog" "likes" "lion" "+"))
If someone is big and they need the dog then the dog does not like the lion.
((("someone" "is" "big" "+") ("someone" "needs" "dog" "+")) -> ("dog" "likes" "lion" "-"))
If someone chases the dog and they are big then they are rough.
((("someone" "chases" "dog" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
The lion needs the dog.
True
1
proof
[(triple3)]
("lion" "needs" "dog" "+")
triple3
The lion does not need the dog.
False
1
inv-proof
[(triple3)]
("lion" "needs" "dog" "-")
triple3
The lion likes the dog.
True
2
proof
[(((triple1) -> rule2))]
("lion" "likes" "dog" "+")
((triple1) -> (rule2 % int1))
The lion likes the dog.
("lion" "likes" "dog" "+")
int1
The lion does not like the dog.
False
2
inv-proof
[(((triple1) -> rule2))]
("lion" "likes" "dog" "-")
((triple1) -> (rule2 % int1))
The lion likes the dog.
("lion" "likes" "dog" "+")
int1
The dog likes the lion.
True
3
proof
[(((((triple1) -> rule2)) -> rule6))]
("dog" "likes" "lion" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The lion likes the dog.
("lion" "likes" "dog" "+")
int2
The dog does not like the lion.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule6))]
("dog" "likes" "lion" "-")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The lion likes the dog.
("lion" "likes" "dog" "+")
int2
The dog chases the dog.
True
4
proof
[(((((((triple1) -> rule2)) -> rule6)) -> rule3))]
("dog" "chases" "dog" "+")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog likes the lion.
("dog" "likes" "lion" "+")
int2
The lion likes the dog.
("lion" "likes" "dog" "+")
int3
The dog does not chase the dog.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule6)) -> rule3))]
("dog" "chases" "dog" "-")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog likes the lion.
("dog" "likes" "lion" "+")
int2
The lion likes the dog.
("lion" "likes" "dog" "+")
int3
The lion does not like the lion.
Unknown
inv-rconc
[@2: The lion likes the lion.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("lion" "likes" "lion" "-")
The lion is rough.
Unknown
rconc
[@1: The lion is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "is" "rough" "+")
The lion is not cold.
Unknown
inv-rconc
[@1: The lion is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "cold" "-")
The lion chases the dog.
Unknown
rconc
[@2: The lion chases the dog.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("lion" "chases" "dog" "+")
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The dog is round.
Unknown
random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "+")
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 dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
@0: The dog chases the lion.[(triple1)] The dog is rough.[(triple2)] The lion needs the dog.[(triple3)] @1: The lion likes the dog.[(((triple1) -> rule2))] @2: The dog likes the lion.[(((((triple1) -> rule2)) -> rule6))] @3: The dog chases the dog.[(((((((triple1) -> rule2)) -> rule6)) -> rule3))]
The dog chases the lion.
("dog" "chases" "lion" "+")
triple1
The dog is rough.
("dog" "is" "rough" "+")
triple2
The lion needs the dog.
("lion" "needs" "dog" "+")
triple3
The lion likes the dog.
("lion" "likes" "dog" "+")
((triple1) -> (rule2 % int1))
The lion likes the dog.
("lion" "likes" "dog" "+")
int1
The dog likes the lion.
("dog" "likes" "lion" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The lion likes the dog.
("lion" "likes" "dog" "+")
int2
The dog chases the dog.
("dog" "chases" "dog" "+")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog likes the lion.
("dog" "likes" "lion" "+")
int2
The lion likes the dog.
("lion" "likes" "dog" "+")
int3