The bear chases the lion. The bear is not kind. The bear visits the lion. The dog needs the squirrel. The lion chases the squirrel. The lion is nice. The lion is red. The squirrel is nice. The squirrel is red. The squirrel needs the bear. The squirrel needs the dog. The squirrel visits the dog. If the bear visits the dog then the bear needs the dog. If someone visits the lion and the lion needs the bear then the lion is not big. If someone chases the dog then the dog visits the bear. If someone is nice and they chase the dog then the dog visits the lion. If someone needs the dog and the dog chases the lion then the dog is blue. If someone visits the lion then they visit the dog. If someone visits the dog then the dog chases the squirrel. If someone visits the lion and they need the dog then they chase the squirrel.
The bear chases the lion.
("bear" "chases" "lion" "+")
The bear is not kind.
("bear" "is" "kind" "-")
The bear visits the lion.
("bear" "visits" "lion" "+")
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is red.
("lion" "is" "red" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
If the bear visits the dog then the bear needs the dog.
((("bear" "visits" "dog" "+")) -> ("bear" "needs" "dog" "+"))
If someone visits the lion and the lion needs the bear then the lion is not big.
((("someone" "visits" "lion" "+") ("lion" "needs" "bear" "+")) -> ("lion" "is" "big" "-"))
If someone chases the dog then the dog visits the bear.
((("someone" "chases" "dog" "+")) -> ("dog" "visits" "bear" "+"))
If someone is nice and they chase the dog then the dog visits the lion.
((("someone" "is" "nice" "+") ("someone" "chases" "dog" "+")) -> ("dog" "visits" "lion" "+"))
If someone needs the dog and the dog chases the lion then the dog is blue.
((("someone" "needs" "dog" "+") ("dog" "chases" "lion" "+")) -> ("dog" "is" "blue" "+"))
If someone visits the lion then they visit the dog.
((("someone" "visits" "lion" "+")) -> ("someone" "visits" "dog" "+"))
If someone visits the dog then the dog chases the squirrel.
((("someone" "visits" "dog" "+")) -> ("dog" "chases" "squirrel" "+"))
If someone visits the lion and they need the dog then they chase the squirrel.
((("someone" "visits" "lion" "+") ("someone" "needs" "dog" "+")) -> ("someone" "chases" "squirrel" "+"))
The lion is red.
True
1
proof
[(triple7)]
("lion" "is" "red" "+")
triple7
The lion is not nice.
False
1
inv-proof
[(triple6)]
("lion" "is" "nice" "-")
triple6
The dog chases the squirrel.
True
2
proof
[(((triple12) -> rule7) OR ((((triple3) -> rule6)) -> rule7))]
("dog" "chases" "squirrel" "+")
((triple12) -> (rule7 % int1))
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule7 % int1))
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
int2
The dog does not chase the squirrel.
False
2
inv-proof
[(((triple12) -> rule7) OR ((((triple3) -> rule6)) -> rule7))]
("dog" "chases" "squirrel" "-")
((triple12) -> (rule7 % int1))
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule7 % int1))
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
int2
The bear needs the dog.
True
3
proof
[(((((triple3) -> rule6)) -> rule1))]
("bear" "needs" "dog" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
The bear needs the dog.
("bear" "needs" "dog" "+")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
int2
The bear does not need the dog.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule1))]
("bear" "needs" "dog" "-")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
The bear needs the dog.
("bear" "needs" "dog" "+")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
int2
The bear chases the squirrel.
True
5
proof
[(((triple3 ((((triple3) -> rule6)) -> rule1)) -> rule8))]
("bear" "chases" "squirrel" "+")
((triple3 ((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int1
The bear needs the dog.
("bear" "needs" "dog" "+")
int2
The bear visits the dog.
("bear" "visits" "dog" "+")
int3
The bear does not chase the squirrel.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule6)) -> rule1)) -> rule8))]
("bear" "chases" "squirrel" "-")
((triple3 ((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int1
The bear needs the dog.
("bear" "needs" "dog" "+")
int2
The bear visits the dog.
("bear" "visits" "dog" "+")
int3
The dog is not blue.
Unknown
inv-rconc
[@1: The dog is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "blue" "-")
The dog visits the bear.
Unknown
rconc
[@1: The dog visits the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "visits" "bear" "+")
The lion does not visit the dog.
Unknown
inv-rconc
[@1: The lion visits the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "visits" "dog" "-")
The dog visits the dog.
Unknown
rconc
[@2: The dog visits the dog.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("dog" "visits" "dog" "+")
The squirrel does not need the lion.
Unknown
inv-random
[@0: The squirrel needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "lion" "-")
The dog is big.
Unknown
random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "+")
The lion does not chase the dog.
Unknown
inv-random
[@0: The lion chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "dog" "-")
The bear needs the squirrel.
Unknown
random
[@0: The bear needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "squirrel" "+")
@0: The bear chases the lion.[(triple1)] The bear is not kind.[(triple2)] The bear visits the lion.[(triple3)] The dog needs the squirrel.[(triple4)] The lion chases the squirrel.[(triple5)] The lion is nice.[(triple6)] The lion is red.[(triple7)] The squirrel is nice.[(triple8)] The squirrel is red.[(triple9)] The squirrel needs the bear.[(triple10)] The squirrel needs the dog.[(triple11)] The squirrel visits the dog.[(triple12)] @1: The bear visits the dog.[(((triple3) -> rule6))] The dog chases the squirrel.[(((triple12) -> rule7) OR ((((triple3) -> rule6)) -> rule7))] @2: The bear needs the dog.[(((((triple3) -> rule6)) -> rule1))] @3: The bear chases the squirrel.[(((triple3 ((((triple3) -> rule6)) -> rule1)) -> rule8))]
The bear chases the lion.
("bear" "chases" "lion" "+")
triple1
The bear is not kind.
("bear" "is" "kind" "-")
triple2
The bear visits the lion.
("bear" "visits" "lion" "+")
triple3
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
triple4
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple5
The lion is nice.
("lion" "is" "nice" "+")
triple6
The lion is red.
("lion" "is" "red" "+")
triple7
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple8
The squirrel is red.
("squirrel" "is" "red" "+")
triple9
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
triple10
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
triple11
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple12
The bear visits the dog.
("bear" "visits" "dog" "+")
((triple3) -> (rule6 % int1))
The bear visits the dog.
("bear" "visits" "dog" "+")
int1
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
((triple12) -> (rule7 % int1))
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule7 % int1))
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
int2
The bear needs the dog.
("bear" "needs" "dog" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
The bear needs the dog.
("bear" "needs" "dog" "+")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
int2
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
((triple3 ((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
int1
The bear needs the dog.
("bear" "needs" "dog" "+")
int2
The bear visits the dog.
("bear" "visits" "dog" "+")
int3