The bear does not see the dog. The dog is round. The lion sees the bear. The tiger needs the bear. Round things are nice. If something is round then it sees the tiger. If something needs the lion then it visits the lion. If something visits the bear then it does not need the bear. If the bear is red and the bear visits the dog then the dog needs the bear. If something needs the lion and it does not see the lion then the lion does not visit the dog. If something is cold and it does not need the dog then it visits the tiger. If something sees the bear then the bear needs the lion.
The bear does not see the dog.
("bear" "sees" "dog" "-")
The dog is round.
("dog" "is" "round" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
Round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
If something is round then it sees the tiger.
((("something" "is" "round" "+")) -> ("something" "sees" "tiger" "+"))
If something needs the lion then it visits the lion.
((("something" "needs" "lion" "+")) -> ("something" "visits" "lion" "+"))
If something visits the bear then it does not need the bear.
((("something" "visits" "bear" "+")) -> ("something" "needs" "bear" "-"))
If the bear is red and the bear visits the dog then the dog needs the bear.
((("bear" "is" "red" "+") ("bear" "visits" "dog" "+")) -> ("dog" "needs" "bear" "+"))
If something needs the lion and it does not see the lion then the lion does not visit the dog.
((("something" "needs" "lion" "+") ("something" "sees" "lion" "~")) -> ("lion" "visits" "dog" "-"))
If something is cold and it does not need the dog then it visits the tiger.
((("something" "is" "cold" "+") ("something" "needs" "dog" "~")) -> ("something" "visits" "tiger" "+"))
If something sees the bear then the bear needs the lion.
((("something" "sees" "bear" "+")) -> ("bear" "needs" "lion" "+"))
The dog is round.
True
1
proof
[(triple2)]
("dog" "is" "round" "+")
triple2
The lion does not see the bear.
False
1
inv-proof
[(triple3)]
("lion" "sees" "bear" "-")
triple3
The bear needs the lion.
True
2
proof
[(((triple3) -> rule8))]
("bear" "needs" "lion" "+")
((triple3) -> (rule8 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The dog is not nice.
False
2
inv-proof
[(((triple2) -> rule1))]
("dog" "is" "nice" "-")
((triple2) -> (rule1 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The bear visits the lion.
True
3
proof
[(((((triple3) -> rule8)) -> rule3))]
("bear" "visits" "lion" "+")
((((triple3) -> (rule8 % int2))) -> (rule3 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
The bear does not visit the lion.
False
3
inv-proof
[(((((triple3) -> rule8)) -> rule3))]
("bear" "visits" "lion" "-")
((((triple3) -> (rule8 % int2))) -> (rule3 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
The bear does not see the tiger.
Unknown
inv-rconc
[@1: The bear sees the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "sees" "tiger" "-")
The dog needs the bear.
Unknown
rconc
[@1: The dog needs the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "needs" "bear" "+")
The tiger does not visit the lion.
Unknown
inv-rconc
[@1: The tiger visits the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "visits" "lion" "-")
The tiger needs the lion.
Unknown
random
[@0: The tiger needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "lion" "+")
The lion is not cold.
Unknown
inv-random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "-")
The lion needs the tiger.
Unknown
random
[@0: The lion needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "tiger" "+")
@0: The bear does not see the dog.[(triple1)] The dog is round.[(triple2)] The lion sees the bear.[(triple3)] The tiger needs the bear.[(triple4)] @1: The bear needs the lion.[(((triple3) -> rule8))] The dog is nice.[(((triple2) -> rule1))] The dog sees the tiger.[(((triple2) -> rule2))] @2: The bear visits the lion.[(((((triple3) -> rule8)) -> rule3))]
The bear does not see the dog.
("bear" "sees" "dog" "-")
triple1
The dog is round.
("dog" "is" "round" "+")
triple2
The lion sees the bear.
("lion" "sees" "bear" "+")
triple3
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple4
The bear needs the lion.
("bear" "needs" "lion" "+")
((triple3) -> (rule8 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
((triple2) -> (rule1 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog sees the tiger.
("dog" "sees" "tiger" "+")
((triple2) -> (rule2 % int1))
The dog sees the tiger.
("dog" "sees" "tiger" "+")
int1
The bear visits the lion.
("bear" "visits" "lion" "+")
((((triple3) -> (rule8 % int2))) -> (rule3 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2