The bear needs the dog. The bear needs the lion. The bear sees the dog. The dog chases the bear. The dog chases the lion. The dog is blue. The dog does not need the bear. The dog needs the lion. The dog does not see the bear. The dog sees the lion. The lion chases the dog. The lion is blue. The lion is round. The lion does not need the bear. The lion needs the dog. If something needs the dog and it does not need the bear then the dog chases the bear. If something needs the bear and it chases the lion then the bear does not need the dog. If something is cold then it chases the lion. If the dog needs the lion and the lion does not need the bear then the lion is cold. If something is round and it sees the bear then it chases the dog. If the lion does not see the bear then the bear sees the lion. If something chases the lion and it does not need the dog then it is nice. If something is nice then it sees the lion.
The bear needs the dog.
("bear" "needs" "dog" "+")
The bear needs the lion.
("bear" "needs" "lion" "+")
The bear sees the dog.
("bear" "sees" "dog" "+")
The dog chases the bear.
("dog" "chases" "bear" "+")
The dog chases the lion.
("dog" "chases" "lion" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog does not need the bear.
("dog" "needs" "bear" "-")
The dog needs the lion.
("dog" "needs" "lion" "+")
The dog does not see the bear.
("dog" "sees" "bear" "-")
The dog sees the lion.
("dog" "sees" "lion" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is round.
("lion" "is" "round" "+")
The lion does not need the bear.
("lion" "needs" "bear" "-")
The lion needs the dog.
("lion" "needs" "dog" "+")
If something needs the dog and it does not need the bear then the dog chases the bear.
((("something" "needs" "dog" "+") ("something" "needs" "bear" "~")) -> ("dog" "chases" "bear" "+"))
If something needs the bear and it chases the lion then the bear does not need the dog.
((("something" "needs" "bear" "+") ("something" "chases" "lion" "+")) -> ("bear" "needs" "dog" "-"))
If something is cold then it chases the lion.
((("something" "is" "cold" "+")) -> ("something" "chases" "lion" "+"))
If the dog needs the lion and the lion does not need the bear then the lion is cold.
((("dog" "needs" "lion" "+") ("lion" "needs" "bear" "~")) -> ("lion" "is" "cold" "+"))
If something is round and it sees the bear then it chases the dog.
((("something" "is" "round" "+") ("something" "sees" "bear" "+")) -> ("something" "chases" "dog" "+"))
If the lion does not see the bear then the bear sees the lion.
((("lion" "sees" "bear" "~")) -> ("bear" "sees" "lion" "+"))
If something chases the lion and it does not need the dog then it is nice.
((("something" "chases" "lion" "+") ("something" "needs" "dog" "~")) -> ("something" "is" "nice" "+"))
If something is nice then it sees the lion.
((("something" "is" "nice" "+")) -> ("something" "sees" "lion" "+"))
The lion chases the dog.
True
1
proof
[(triple11)]
("lion" "chases" "dog" "+")
triple11
The bear does not see the dog.
False
1
inv-proof
[(triple3)]
("bear" "sees" "dog" "-")
triple3
The lion is cold.
True
3
proof
[(((triple8 triple14) -> rule4))]
("lion" "is" "cold" "+")
((triple8 triple14) -> (rule4 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is not cold.
False
3
inv-proof
[(((triple8 triple14) -> rule4))]
("lion" "is" "cold" "-")
((triple8 triple14) -> (rule4 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion chases the lion.
True
4
proof
[(((((triple8 triple14) -> rule4)) -> rule3))]
("lion" "chases" "lion" "+")
((((triple8 triple14) -> (rule4 % int2))) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion does not chase the lion.
False
4
inv-proof
[(((((triple8 triple14) -> rule4)) -> rule3))]
("lion" "chases" "lion" "-")
((((triple8 triple14) -> (rule4 % int2))) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The bear is not nice.
Unknown
inv-rconc
[@1: The bear is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "is" "nice" "-")
The bear sees the lion.
Unknown
rconc
[@2: The bear sees the lion.[CWA. Example of deepest failure = (rule8 <- rule7 <- FAIL)]]
("bear" "sees" "lion" "+")
The bear does not chase the lion.
Unknown
inv-rconc
[@1: The bear chases the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "chases" "lion" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
The bear does not see the bear.
Unknown
inv-random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
@0: The bear needs the dog.[(triple1)] The bear needs the lion.[(triple2)] The bear sees the dog.[(triple3)] The dog chases the bear.[(triple4 OR ((triple15 triple14) -> rule1))] The dog chases the lion.[(triple5)] The dog does not need the bear.[(triple7)] The dog does not see the bear.[(triple9)] The dog is blue.[(triple6)] The dog needs the lion.[(triple8)] The dog sees the lion.[(triple10)] The lion chases the dog.[(triple11)] The lion does not need the bear.[(triple14)] The lion is blue.[(triple12)] The lion is round.[(triple13)] The lion needs the dog.[(triple15)] @1: The lion is cold.[(((triple8 triple14) -> rule4))] @2: The lion chases the lion.[(((((triple8 triple14) -> rule4)) -> rule3))]
The bear needs the dog.
("bear" "needs" "dog" "+")
triple1
The bear needs the lion.
("bear" "needs" "lion" "+")
triple2
The bear sees the dog.
("bear" "sees" "dog" "+")
triple3
The dog chases the bear.
("dog" "chases" "bear" "+")
triple4
((triple15 triple14) -> (rule1 % int1))
The dog chases the bear.
("dog" "chases" "bear" "+")
int1
The dog chases the lion.
("dog" "chases" "lion" "+")
triple5
The dog does not need the bear.
("dog" "needs" "bear" "-")
triple7
The dog does not see the bear.
("dog" "sees" "bear" "-")
triple9
The dog is blue.
("dog" "is" "blue" "+")
triple6
The dog needs the lion.
("dog" "needs" "lion" "+")
triple8
The dog sees the lion.
("dog" "sees" "lion" "+")
triple10
The lion chases the dog.
("lion" "chases" "dog" "+")
triple11
The lion does not need the bear.
("lion" "needs" "bear" "-")
triple14
The lion is blue.
("lion" "is" "blue" "+")
triple12
The lion is round.
("lion" "is" "round" "+")
triple13
The lion needs the dog.
("lion" "needs" "dog" "+")
triple15
The lion is cold.
("lion" "is" "cold" "+")
((triple8 triple14) -> (rule4 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
((((triple8 triple14) -> (rule4 % int2))) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2