The bear chases the dog. The dog is blue. The lion visits the dog. If someone is nice and they chase the lion then they visit the bear. If the bear visits the lion then the lion needs the dog. If someone chases the lion and they visit the bear then the lion visits the dog. If someone chases the dog then they visit the bear. If someone visits the bear then the bear visits the dog. If someone needs the lion and the lion visits the bear then the lion chases the dog.
The bear chases the dog.
("bear" "chases" "dog" "+")
The dog is blue.
("dog" "is" "blue" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
If someone is nice and they chase the lion then they visit the bear.
((("someone" "is" "nice" "+") ("someone" "chases" "lion" "+")) -> ("someone" "visits" "bear" "+"))
If the bear visits the lion then the lion needs the dog.
((("bear" "visits" "lion" "+")) -> ("lion" "needs" "dog" "+"))
If someone chases the lion and they visit the bear then the lion visits the dog.
((("someone" "chases" "lion" "+") ("someone" "visits" "bear" "+")) -> ("lion" "visits" "dog" "+"))
If someone chases the dog then they visit the bear.
((("someone" "chases" "dog" "+")) -> ("someone" "visits" "bear" "+"))
If someone visits the bear then the bear visits the dog.
((("someone" "visits" "bear" "+")) -> ("bear" "visits" "dog" "+"))
If someone needs the lion and the lion visits the bear then the lion chases the dog.
((("someone" "needs" "lion" "+") ("lion" "visits" "bear" "+")) -> ("lion" "chases" "dog" "+"))
The bear chases the dog.
True
1
proof
[(triple1)]
("bear" "chases" "dog" "+")
triple1
The lion does not visit the dog.
False
1
inv-proof
[(triple3)]
("lion" "visits" "dog" "-")
triple3
The bear visits the bear.
True
2
proof
[(((triple1) -> rule4))]
("bear" "visits" "bear" "+")
((triple1) -> (rule4 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear does not visit the bear.
False
2
inv-proof
[(((triple1) -> rule4))]
("bear" "visits" "bear" "-")
((triple1) -> (rule4 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear visits the dog.
True
3
proof
[(((((triple1) -> rule4)) -> rule5))]
("bear" "visits" "dog" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The bear visits the dog.
("bear" "visits" "dog" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The bear does not visit the dog.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule5))]
("bear" "visits" "dog" "-")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The bear visits the dog.
("bear" "visits" "dog" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The lion does not chase the dog.
Unknown
inv-rconc
[@1: The lion chases the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "chases" "dog" "-")
The lion visits the bear.
Unknown
rconc
[@2: The lion visits the bear.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("lion" "visits" "bear" "+")
The lion does not need the dog.
Unknown
inv-rconc
[@1: The lion needs the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "needs" "dog" "-")
The bear chases the lion.
Unknown
random
[@0: The bear chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "lion" "+")
The dog is not cold.
Unknown
inv-random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "-")
The bear needs the lion.
Unknown
random
[@0: The bear needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "lion" "+")
@0: The bear chases the dog.[(triple1)] The dog is blue.[(triple2)] The lion visits the dog.[(triple3)] @1: The bear visits the bear.[(((triple1) -> rule4))] @2: The bear visits the dog.[(((((triple1) -> rule4)) -> rule5))]
The bear chases the dog.
("bear" "chases" "dog" "+")
triple1
The dog is blue.
("dog" "is" "blue" "+")
triple2
The lion visits the dog.
("lion" "visits" "dog" "+")
triple3
The bear visits the bear.
("bear" "visits" "bear" "+")
((triple1) -> (rule4 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The bear visits the dog.
("bear" "visits" "dog" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2