The bear sees the lion. The dog is young. The lion is red. The lion sees the dog. The lion visits the bear. The squirrel is young. The squirrel does not see the lion. If someone is red then they do not chase the squirrel. If someone sees the bear and they are red then the bear is red. If the lion does not see the dog then the lion sees the bear. If someone is round and they chase the bear then they visit the squirrel. If someone is young then they see the squirrel. If someone visits the dog then they are not blue. If someone sees the dog and the dog sees the lion then they chase the dog. All red people are young. If someone is young then they see the bear.
The bear sees the lion.
("bear" "sees" "lion" "+")
The dog is young.
("dog" "is" "young" "+")
The lion is red.
("lion" "is" "red" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
The lion visits the bear.
("lion" "visits" "bear" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel does not see the lion.
("squirrel" "sees" "lion" "-")
If someone is red then they do not chase the squirrel.
((("someone" "is" "red" "+")) -> ("someone" "chases" "squirrel" "-"))
If someone sees the bear and they are red then the bear is red.
((("someone" "sees" "bear" "+") ("someone" "is" "red" "+")) -> ("bear" "is" "red" "+"))
If the lion does not see the dog then the lion sees the bear.
((("lion" "sees" "dog" "~")) -> ("lion" "sees" "bear" "+"))
If someone is round and they chase the bear then they visit the squirrel.
((("someone" "is" "round" "+") ("someone" "chases" "bear" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone is young then they see the squirrel.
((("someone" "is" "young" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone visits the dog then they are not blue.
((("someone" "visits" "dog" "+")) -> ("someone" "is" "blue" "-"))
If someone sees the dog and the dog sees the lion then they chase the dog.
((("someone" "sees" "dog" "+") ("dog" "sees" "lion" "+")) -> ("someone" "chases" "dog" "+"))
All red people are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If someone is young then they see the bear.
((("someone" "is" "young" "+")) -> ("someone" "sees" "bear" "+"))
The lion sees the dog.
True
1
proof
[(triple4)]
("lion" "sees" "dog" "+")
triple4
The lion is not red.
False
1
inv-proof
[(triple3)]
("lion" "is" "red" "-")
triple3
The lion is young.
True
2
proof
[(((triple3) -> rule8))]
("lion" "is" "young" "+")
((triple3) -> (rule8 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The squirrel does not see the bear.
False
2
inv-proof
[(((triple6) -> rule9))]
("squirrel" "sees" "bear" "-")
((triple6) -> (rule9 % int1))
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int1
The lion sees the bear.
True
3
proof
[(((((triple3) -> rule8)) -> rule9))]
("lion" "sees" "bear" "+")
((((triple3) -> (rule8 % int2))) -> (rule9 % int1))
The lion sees the bear.
("lion" "sees" "bear" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion does not see the bear.
False
3
inv-proof
[(((((triple3) -> rule8)) -> rule9))]
("lion" "sees" "bear" "-")
((((triple3) -> (rule8 % int2))) -> (rule9 % int1))
The lion sees the bear.
("lion" "sees" "bear" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The bear is red.
True
5
proof
[(((((((triple3) -> rule8)) -> rule9) triple3) -> rule2))]
("bear" "is" "red" "+")
((((((triple3) -> (rule8 % int3))) -> (rule9 % int2)) triple3) -> (rule2 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The lion sees the bear.
("lion" "sees" "bear" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The bear is not red.
False
5
inv-proof
[(((((((triple3) -> rule8)) -> rule9) triple3) -> rule2))]
("bear" "is" "red" "-")
((((((triple3) -> (rule8 % int3))) -> (rule9 % int2)) triple3) -> (rule2 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The lion sees the bear.
("lion" "sees" "bear" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The bear does not chase the squirrel.
True
6
proof
[(((((((((triple3) -> rule8)) -> rule9) triple3) -> rule2)) -> rule1))]
("bear" "chases" "squirrel" "-")
((((((((triple3) -> (rule8 % int4))) -> (rule9 % int3)) triple3) -> (rule2 % int2))) -> (rule1 % int1))
The bear does not chase the squirrel.
("bear" "chases" "squirrel" "-")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The lion sees the bear.
("lion" "sees" "bear" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
The bear is not young.
False
6
inv-proof
[(((((((((triple3) -> rule8)) -> rule9) triple3) -> rule2)) -> rule8))]
("bear" "is" "young" "-")
((((((((triple3) -> (rule8 % int4))) -> (rule9 % int3)) triple3) -> (rule2 % int2))) -> (rule8 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The lion sees the bear.
("lion" "sees" "bear" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
The bear sees the squirrel.
True
7
proof
[(((((((((((triple3) -> rule8)) -> rule9) triple3) -> rule2)) -> rule8)) -> rule5))]
("bear" "sees" "squirrel" "+")
((((((((((triple3) -> (rule8 % int5))) -> (rule9 % int4)) triple3) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The lion sees the bear.
("lion" "sees" "bear" "+")
int4
The lion is young.
("lion" "is" "young" "+")
int5
The bear does not see the bear.
False
7
inv-proof
[(((((((((((triple3) -> rule8)) -> rule9) triple3) -> rule2)) -> rule8)) -> rule9))]
("bear" "sees" "bear" "-")
((((((((((triple3) -> (rule8 % int5))) -> (rule9 % int4)) triple3) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The lion sees the bear.
("lion" "sees" "bear" "+")
int4
The lion is young.
("lion" "is" "young" "+")
int5
The dog does not visit the squirrel.
Unknown
inv-rconc
[@1: The dog visits the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "visits" "squirrel" "-")
The lion chases the dog.
Unknown
rconc
[@1: The lion chases the dog.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "chases" "dog" "+")
The dog does not chase the dog.
Unknown
inv-rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "chases" "dog" "-")
The squirrel visits the squirrel.
Unknown
rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "visits" "squirrel" "+")
The bear does not visit the squirrel.
Unknown
inv-rconc
[@1: The bear visits the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "visits" "squirrel" "-")
The bear chases the dog.
Unknown
rconc
[@1: The bear chases the dog.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "chases" "dog" "+")
The dog does not chase the squirrel.
Unknown
inv-random
[@0: The dog chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "squirrel" "-")
The squirrel is blue.
Unknown
random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "+")
The dog does not visit the bear.
Unknown
inv-random
[@0: The dog visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "bear" "-")
The bear is blue.
Unknown
random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "+")
The lion does not visit the lion.
Unknown
inv-random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "-")
The bear visits the dog.
Unknown
random
[@0: The bear visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "dog" "+")
@0: The bear sees the lion.[(triple1)] The dog is young.[(triple2)] The lion is red.[(triple3)] The lion sees the dog.[(triple4)] The lion visits the bear.[(triple5)] The squirrel does not see the lion.[(triple7)] The squirrel is young.[(triple6)] @1: The dog sees the bear.[(((triple2) -> rule9))] The dog sees the squirrel.[(((triple2) -> rule5))] The lion does not chase the squirrel.[(((triple3) -> rule1))] The lion is young.[(((triple3) -> rule8))] The squirrel sees the bear.[(((triple6) -> rule9))] The squirrel sees the squirrel.[(((triple6) -> rule5))] @2: The lion sees the bear.[(((((triple3) -> rule8)) -> rule9))] The lion sees the squirrel.[(((((triple3) -> rule8)) -> rule5))] @3: The bear is red.[(((((((triple3) -> rule8)) -> rule9) triple3) -> rule2))] @4: The bear does not chase the squirrel.[(((((((((triple3) -> rule8)) -> rule9) triple3) -> rule2)) -> rule1))] The bear is young.[(((((((((triple3) -> rule8)) -> rule9) triple3) -> rule2)) -> rule8))] @5: The bear sees the bear.[(((((((((((triple3) -> rule8)) -> rule9) triple3) -> rule2)) -> rule8)) -> rule9))] The bear sees the squirrel.[(((((((((((triple3) -> rule8)) -> rule9) triple3) -> rule2)) -> rule8)) -> rule5))]
The bear sees the lion.
("bear" "sees" "lion" "+")
triple1
The dog is young.
("dog" "is" "young" "+")
triple2
The lion is red.
("lion" "is" "red" "+")
triple3
The lion sees the dog.
("lion" "sees" "dog" "+")
triple4
The lion visits the bear.
("lion" "visits" "bear" "+")
triple5
The squirrel does not see the lion.
("squirrel" "sees" "lion" "-")
triple7
The squirrel is young.
("squirrel" "is" "young" "+")
triple6
The dog sees the bear.
("dog" "sees" "bear" "+")
((triple2) -> (rule9 % int1))
The dog sees the bear.
("dog" "sees" "bear" "+")
int1
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
((triple2) -> (rule5 % int1))
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
int1
The lion does not chase the squirrel.
("lion" "chases" "squirrel" "-")
((triple3) -> (rule1 % int1))
The lion does not chase the squirrel.
("lion" "chases" "squirrel" "-")
int1
The lion is young.
("lion" "is" "young" "+")
((triple3) -> (rule8 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
((triple6) -> (rule9 % int1))
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((triple6) -> (rule5 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The lion sees the bear.
("lion" "sees" "bear" "+")
((((triple3) -> (rule8 % int2))) -> (rule9 % int1))
The lion sees the bear.
("lion" "sees" "bear" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
((((triple3) -> (rule8 % int2))) -> (rule5 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The bear is red.
("bear" "is" "red" "+")
((((((triple3) -> (rule8 % int3))) -> (rule9 % int2)) triple3) -> (rule2 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The lion sees the bear.
("lion" "sees" "bear" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The bear does not chase the squirrel.
("bear" "chases" "squirrel" "-")
((((((((triple3) -> (rule8 % int4))) -> (rule9 % int3)) triple3) -> (rule2 % int2))) -> (rule1 % int1))
The bear does not chase the squirrel.
("bear" "chases" "squirrel" "-")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The lion sees the bear.
("lion" "sees" "bear" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
The bear is young.
("bear" "is" "young" "+")
((((((((triple3) -> (rule8 % int4))) -> (rule9 % int3)) triple3) -> (rule2 % int2))) -> (rule8 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The lion sees the bear.
("lion" "sees" "bear" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
The bear sees the bear.
("bear" "sees" "bear" "+")
((((((((((triple3) -> (rule8 % int5))) -> (rule9 % int4)) triple3) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule9 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The lion sees the bear.
("lion" "sees" "bear" "+")
int4
The lion is young.
("lion" "is" "young" "+")
int5
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
((((((((((triple3) -> (rule8 % int5))) -> (rule9 % int4)) triple3) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
The lion sees the bear.
("lion" "sees" "bear" "+")
int4
The lion is young.
("lion" "is" "young" "+")
int5