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