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