The bear is nice. The bear sees the dog. The bear visits the dog. The dog eats the lion. The dog is red. The lion is blue. The lion sees the bear. If something visits the dog and it eats the bear then it sees the lion. If something is blue and it sees the lion then the lion is red. If something eats the bear then it visits the bear. If something sees the bear then the bear visits the lion. If something sees the dog and the dog is red then the dog is blue. If something eats the dog and it visits the lion then the lion visits the dog. If the lion is nice and the lion visits the dog then the dog visits the bear. If something sees the lion and it visits the dog then it is blue.
The bear is nice.
("bear" "is" "nice" "+")
The bear sees the dog.
("bear" "sees" "dog" "+")
The bear visits the dog.
("bear" "visits" "dog" "+")
The dog eats the lion.
("dog" "eats" "lion" "+")
The dog is red.
("dog" "is" "red" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
If something visits the dog and it eats the bear then it sees the lion.
((("something" "visits" "dog" "+") ("something" "eats" "bear" "+")) -> ("something" "sees" "lion" "+"))
If something is blue and it sees the lion then the lion is red.
((("something" "is" "blue" "+") ("something" "sees" "lion" "+")) -> ("lion" "is" "red" "+"))
If something eats the bear then it visits the bear.
((("something" "eats" "bear" "+")) -> ("something" "visits" "bear" "+"))
If something sees the bear then the bear visits the lion.
((("something" "sees" "bear" "+")) -> ("bear" "visits" "lion" "+"))
If something sees the dog and the dog is red then the dog is blue.
((("something" "sees" "dog" "+") ("dog" "is" "red" "+")) -> ("dog" "is" "blue" "+"))
If something eats the dog and it visits the lion then the lion visits the dog.
((("something" "eats" "dog" "+") ("something" "visits" "lion" "+")) -> ("lion" "visits" "dog" "+"))
If the lion is nice and the lion visits the dog then the dog visits the bear.
((("lion" "is" "nice" "+") ("lion" "visits" "dog" "+")) -> ("dog" "visits" "bear" "+"))
If something sees the lion and it visits the dog then it is blue.
((("something" "sees" "lion" "+") ("something" "visits" "dog" "+")) -> ("something" "is" "blue" "+"))
The bear visits the dog.
True
1
proof
[(triple3)]
("bear" "visits" "dog" "+")
triple3
The lion is not blue.
False
1
inv-proof
[(triple6)]
("lion" "is" "blue" "-")
triple6
The dog is blue.
True
3
proof
[(((triple2 triple5) -> rule5))]
("dog" "is" "blue" "+")
((triple2 triple5) -> (rule5 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The bear does not visit the lion.
False
2
inv-proof
[(((triple7) -> rule4))]
("bear" "visits" "lion" "-")
((triple7) -> (rule4 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The dog does not visit the bear.
Unknown
inv-rconc
[@1: The dog visits the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "visits" "bear" "-")
The lion sees the lion.
Unknown
rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "sees" "lion" "+")
The bear is not red.
Unknown
inv-random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "-")
The dog sees the bear.
Unknown
random
[@0: The dog sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "bear" "+")
@0: The bear is nice.[(triple1)] The bear sees the dog.[(triple2)] The bear visits the dog.[(triple3)] The dog eats the lion.[(triple4)] The dog is red.[(triple5)] The lion is blue.[(triple6)] The lion sees the bear.[(triple7)] @1: The bear visits the lion.[(((triple7) -> rule4))] The dog is blue.[(((triple2 triple5) -> rule5))]
The bear is nice.
("bear" "is" "nice" "+")
triple1
The bear sees the dog.
("bear" "sees" "dog" "+")
triple2
The bear visits the dog.
("bear" "visits" "dog" "+")
triple3
The dog eats the lion.
("dog" "eats" "lion" "+")
triple4
The dog is red.
("dog" "is" "red" "+")
triple5
The lion is blue.
("lion" "is" "blue" "+")
triple6
The lion sees the bear.
("lion" "sees" "bear" "+")
triple7
The bear visits the lion.
("bear" "visits" "lion" "+")
((triple7) -> (rule4 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
((triple2 triple5) -> (rule5 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1