The dog does not visit the lion. The lion is big. The lion is blue. The lion sees the dog. The lion visits the dog. The rabbit is blue. The rabbit is cold. If something is cold and it does not visit the lion then the lion sees the dog. If the rabbit is not blue then the rabbit does not see the lion. If something is green then it sees the rabbit. If something is big then it likes the dog. If something visits the rabbit and it is cold then the rabbit visits the dog. If something visits the lion and it is not rough then the lion sees the rabbit. If something sees the rabbit then it likes the rabbit. Cold things are green.
The dog does not visit the lion.
("dog" "visits" "lion" "-")
The lion is big.
("lion" "is" "big" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
If something is cold and it does not visit the lion then the lion sees the dog.
((("something" "is" "cold" "+") ("something" "visits" "lion" "~")) -> ("lion" "sees" "dog" "+"))
If the rabbit is not blue then the rabbit does not see the lion.
((("rabbit" "is" "blue" "~")) -> ("rabbit" "sees" "lion" "-"))
If something is green then it sees the rabbit.
((("something" "is" "green" "+")) -> ("something" "sees" "rabbit" "+"))
If something is big then it likes the dog.
((("something" "is" "big" "+")) -> ("something" "likes" "dog" "+"))
If something visits the rabbit and it is cold then the rabbit visits the dog.
((("something" "visits" "rabbit" "+") ("something" "is" "cold" "+")) -> ("rabbit" "visits" "dog" "+"))
If something visits the lion and it is not rough then the lion sees the rabbit.
((("something" "visits" "lion" "+") ("something" "is" "rough" "~")) -> ("lion" "sees" "rabbit" "+"))
If something sees the rabbit then it likes the rabbit.
((("something" "sees" "rabbit" "+")) -> ("something" "likes" "rabbit" "+"))
Cold things are green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
The dog does not visit the lion.
True
1
proof
[(triple1)]
("dog" "visits" "lion" "-")
triple1
The lion does not visit the dog.
False
1
inv-proof
[(triple5)]
("lion" "visits" "dog" "-")
triple5
The rabbit is green.
True
2
proof
[(((triple7) -> rule8))]
("rabbit" "is" "green" "+")
((triple7) -> (rule8 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The lion does not like the dog.
False
2
inv-proof
[(((triple2) -> rule4))]
("lion" "likes" "dog" "-")
((triple2) -> (rule4 % int1))
The lion likes the dog.
("lion" "likes" "dog" "+")
int1
The rabbit sees the rabbit.
True
3
proof
[(((((triple7) -> rule8)) -> rule3))]
("rabbit" "sees" "rabbit" "+")
((((triple7) -> (rule8 % int2))) -> (rule3 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit does not see the rabbit.
False
3
inv-proof
[(((((triple7) -> rule8)) -> rule3))]
("rabbit" "sees" "rabbit" "-")
((((triple7) -> (rule8 % int2))) -> (rule3 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit likes the rabbit.
True
4
proof
[(((((((triple7) -> rule8)) -> rule3)) -> rule7))]
("rabbit" "likes" "rabbit" "+")
((((((triple7) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The rabbit does not like the rabbit.
False
4
inv-proof
[(((((((triple7) -> rule8)) -> rule3)) -> rule7))]
("rabbit" "likes" "rabbit" "-")
((((((triple7) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The dog does not like the dog.
Unknown
inv-rconc
[@1: The dog likes the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "likes" "dog" "-")
The rabbit visits the dog.
Unknown
rconc
[@1: The rabbit visits the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "visits" "dog" "+")
The dog does not see the rabbit.
Unknown
inv-rconc
[@2: The dog sees the rabbit.[CWA. Example of deepest failure = (rule3 <- rule8 <- FAIL)]]
("dog" "sees" "rabbit" "-")
The lion likes the rabbit.
Unknown
rconc
[@3: The lion likes the rabbit.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule8 <- FAIL)]]
("lion" "likes" "rabbit" "+")
The lion does not like the lion.
Unknown
inv-random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "-")
The dog is rough.
Unknown
random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "+")
The rabbit does not see the lion.
Unknown
inv-random
[@0: The rabbit sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "lion" "-")
The rabbit visits the lion.
Unknown
random
[@0: The rabbit visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "lion" "+")
@0: The dog does not visit the lion.[(triple1)] The lion is big.[(triple2)] The lion is blue.[(triple3)] The lion sees the dog.[(triple4)] The lion visits the dog.[(triple5)] The rabbit is blue.[(triple6)] The rabbit is cold.[(triple7)] @1: The lion likes the dog.[(((triple2) -> rule4))] The rabbit is green.[(((triple7) -> rule8))] @2: The rabbit sees the rabbit.[(((((triple7) -> rule8)) -> rule3))] @3: The rabbit likes the rabbit.[(((((((triple7) -> rule8)) -> rule3)) -> rule7))]
The dog does not visit the lion.
("dog" "visits" "lion" "-")
triple1
The lion is big.
("lion" "is" "big" "+")
triple2
The lion is blue.
("lion" "is" "blue" "+")
triple3
The lion sees the dog.
("lion" "sees" "dog" "+")
triple4
The lion visits the dog.
("lion" "visits" "dog" "+")
triple5
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple6
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple7
The lion likes the dog.
("lion" "likes" "dog" "+")
((triple2) -> (rule4 % int1))
The lion likes the dog.
("lion" "likes" "dog" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
((triple7) -> (rule8 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((((triple7) -> (rule8 % int2))) -> (rule3 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((((((triple7) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3