The bald eagle is blue. The bald eagle is kind. The bald eagle sees the dog. The dog chases the lion. The dog is kind. The dog is rough. The dog needs the lion. The dog needs the squirrel. The lion chases the dog. The lion is red. The lion needs the squirrel. The squirrel chases the lion. If something is red then it chases the bald eagle. If the bald eagle chases the lion and the bald eagle chases the squirrel then the squirrel sees the lion. If something chases the dog then it sees the bald eagle. If something needs the bald eagle then the bald eagle chases the lion. If something chases the bald eagle and the bald eagle sees the dog then it chases the squirrel. If something chases the dog then the dog chases the bald eagle. If something sees the squirrel then the squirrel sees the dog. If something sees the lion then it sees the squirrel. If something sees the dog then it sees the lion.
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
The bald eagle sees the dog.
("bald eagle" "sees" "dog" "+")
The dog chases the lion.
("dog" "chases" "lion" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion is red.
("lion" "is" "red" "+")
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
If something is red then it chases the bald eagle.
((("something" "is" "red" "+")) -> ("something" "chases" "bald eagle" "+"))
If the bald eagle chases the lion and the bald eagle chases the squirrel then the squirrel sees the lion.
((("bald eagle" "chases" "lion" "+") ("bald eagle" "chases" "squirrel" "+")) -> ("squirrel" "sees" "lion" "+"))
If something chases the dog then it sees the bald eagle.
((("something" "chases" "dog" "+")) -> ("something" "sees" "bald eagle" "+"))
If something needs the bald eagle then the bald eagle chases the lion.
((("something" "needs" "bald eagle" "+")) -> ("bald eagle" "chases" "lion" "+"))
If something chases the bald eagle and the bald eagle sees the dog then it chases the squirrel.
((("something" "chases" "bald eagle" "+") ("bald eagle" "sees" "dog" "+")) -> ("something" "chases" "squirrel" "+"))
If something chases the dog then the dog chases the bald eagle.
((("something" "chases" "dog" "+")) -> ("dog" "chases" "bald eagle" "+"))
If something sees the squirrel then the squirrel sees the dog.
((("something" "sees" "squirrel" "+")) -> ("squirrel" "sees" "dog" "+"))
If something sees the lion then it sees the squirrel.
((("something" "sees" "lion" "+")) -> ("something" "sees" "squirrel" "+"))
If something sees the dog then it sees the lion.
((("something" "sees" "dog" "+")) -> ("something" "sees" "lion" "+"))
The bald eagle is kind.
True
1
proof
[(triple2)]
("bald eagle" "is" "kind" "+")
triple2
The lion is not red.
False
1
inv-proof
[(triple10)]
("lion" "is" "red" "-")
triple10
The bald eagle sees the lion.
True
2
proof
[(((triple3) -> rule9))]
("bald eagle" "sees" "lion" "+")
((triple3) -> (rule9 % int1))
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int1
The dog does not chase the bald eagle.
False
2
inv-proof
[(((triple9) -> rule6))]
("dog" "chases" "bald eagle" "-")
((triple9) -> (rule6 % int1))
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
int1
The lion chases the squirrel.
True
4
proof
[(((((triple10) -> rule1) triple3) -> rule5))]
("lion" "chases" "squirrel" "+")
((((triple10) -> (rule1 % int2)) triple3) -> (rule5 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The lion chases the bald eagle.
("lion" "chases" "bald eagle" "+")
int2
The lion does not chase the squirrel.
False
4
inv-proof
[(((((triple10) -> rule1) triple3) -> rule5))]
("lion" "chases" "squirrel" "-")
((((triple10) -> (rule1 % int2)) triple3) -> (rule5 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The lion chases the bald eagle.
("lion" "chases" "bald eagle" "+")
int2
The squirrel sees the dog.
True
4
proof
[(((((((triple3) -> rule9)) -> rule8)) -> rule7))]
("squirrel" "sees" "dog" "+")
((((((triple3) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int1
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int2
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int3
The squirrel does not see the dog.
False
4
inv-proof
[(((((((triple3) -> rule9)) -> rule8)) -> rule7))]
("squirrel" "sees" "dog" "-")
((((((triple3) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int1
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int2
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int3
The squirrel sees the lion.
True
5
proof
[(((((((((triple3) -> rule9)) -> rule8)) -> rule7)) -> rule9))]
("squirrel" "sees" "lion" "+")
((((((((triple3) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule9 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int2
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int3
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int4
The squirrel does not see the lion.
False
5
inv-proof
[(((((((((triple3) -> rule9)) -> rule8)) -> rule7)) -> rule9))]
("squirrel" "sees" "lion" "-")
((((((((triple3) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule9 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int2
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int3
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int4
The squirrel sees the squirrel.
True
6
proof
[(((((((((((triple3) -> rule9)) -> rule8)) -> rule7)) -> rule9)) -> rule8))]
("squirrel" "sees" "squirrel" "+")
((((((((((triple3) -> (rule9 % int5))) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int3
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int4
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int5
The squirrel does not see the squirrel.
False
6
inv-proof
[(((((((((((triple3) -> rule9)) -> rule8)) -> rule7)) -> rule9)) -> rule8))]
("squirrel" "sees" "squirrel" "-")
((((((((((triple3) -> (rule9 % int5))) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int3
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int4
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int5
The bald eagle does not chase the squirrel.
Unknown
inv-rconc
[@2: The bald eagle chases the squirrel.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("bald eagle" "chases" "squirrel" "-")
The squirrel chases the squirrel.
Unknown
rconc
[@2: The squirrel chases the squirrel.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("squirrel" "chases" "squirrel" "+")
The lion does not see the squirrel.
Unknown
inv-rconc
[@2: The lion sees the squirrel.[CWA. Example of deepest failure = (rule8 <- rule9 <- FAIL)]]
("lion" "sees" "squirrel" "-")
The bald eagle chases the lion.
Unknown
rconc
[@1: The bald eagle chases the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bald eagle" "chases" "lion" "+")
The squirrel does not chase the bald eagle.
Unknown
inv-rconc
[@1: The squirrel chases the bald eagle.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "chases" "bald eagle" "-")
The dog sees the squirrel.
Unknown
rconc
[@2: The dog sees the squirrel.[CWA. Example of deepest failure = (rule8 <- rule9 <- FAIL)]]
("dog" "sees" "squirrel" "+")
The bald eagle does not need the squirrel.
Unknown
inv-random
[@0: The bald eagle needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "squirrel" "-")
The bald eagle needs the dog.
Unknown
random
[@0: The bald eagle needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "dog" "+")
The lion is not kind.
Unknown
inv-random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "-")
The squirrel is blue.
Unknown
random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "+")
The dog is not red.
Unknown
inv-random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "-")
The bald eagle chases the dog.
Unknown
random
[@0: The bald eagle chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "chases" "dog" "+")
@0: The bald eagle is blue.[(triple1)] The bald eagle is kind.[(triple2)] The bald eagle sees the dog.[(triple3)] The dog chases the lion.[(triple4)] The dog is kind.[(triple5)] The dog is rough.[(triple6)] The dog needs the lion.[(triple7)] The dog needs the squirrel.[(triple8)] The lion chases the dog.[(triple9)] The lion is red.[(triple10)] The lion needs the squirrel.[(triple11)] The squirrel chases the lion.[(triple12)] @1: The bald eagle sees the lion.[(((triple3) -> rule9))] The dog chases the bald eagle.[(((triple9) -> rule6))] The lion chases the bald eagle.[(((triple10) -> rule1))] The lion sees the bald eagle.[(((triple9) -> rule3))] @2: The bald eagle sees the squirrel.[(((((triple3) -> rule9)) -> rule8))] The dog chases the squirrel.[(((((triple9) -> rule6) triple3) -> rule5))] The lion chases the squirrel.[(((((triple10) -> rule1) triple3) -> rule5))] @3: The squirrel sees the dog.[(((((((triple3) -> rule9)) -> rule8)) -> rule7))] @4: The squirrel sees the lion.[(((((((((triple3) -> rule9)) -> rule8)) -> rule7)) -> rule9))] @5: The squirrel sees the squirrel.[(((((((((((triple3) -> rule9)) -> rule8)) -> rule7)) -> rule9)) -> rule8))]
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
triple1
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
triple2
The bald eagle sees the dog.
("bald eagle" "sees" "dog" "+")
triple3
The dog chases the lion.
("dog" "chases" "lion" "+")
triple4
The dog is kind.
("dog" "is" "kind" "+")
triple5
The dog is rough.
("dog" "is" "rough" "+")
triple6
The dog needs the lion.
("dog" "needs" "lion" "+")
triple7
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
triple8
The lion chases the dog.
("lion" "chases" "dog" "+")
triple9
The lion is red.
("lion" "is" "red" "+")
triple10
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple11
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
triple12
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
((triple3) -> (rule9 % int1))
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int1
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
((triple9) -> (rule6 % int1))
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
int1
The lion chases the bald eagle.
("lion" "chases" "bald eagle" "+")
((triple10) -> (rule1 % int1))
The lion chases the bald eagle.
("lion" "chases" "bald eagle" "+")
int1
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
((triple9) -> (rule3 % int1))
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
int1
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
((((triple3) -> (rule9 % int2))) -> (rule8 % int1))
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int1
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int2
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
((((triple9) -> (rule6 % int2)) triple3) -> (rule5 % int1))
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int1
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
int2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
((((triple10) -> (rule1 % int2)) triple3) -> (rule5 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The lion chases the bald eagle.
("lion" "chases" "bald eagle" "+")
int2
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
((((((triple3) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int1
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int2
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int3
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
((((((((triple3) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule9 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int2
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int3
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int4
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((((((((((triple3) -> (rule9 % int5))) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int3
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int4
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
int5