The bald eagle is green. The lion is green. The lion is young. The squirrel sees the lion. The tiger is cold. The tiger sees the lion. The tiger sees the squirrel. If someone sees the tiger and they need the squirrel then the tiger is green. If someone is green then they chase the tiger. If someone is young and they need the squirrel then they see the lion. If someone chases the lion then they chase the tiger. If someone chases the lion and they need the tiger then the tiger is blue. If someone sees the bald eagle and the bald eagle chases the tiger then the bald eagle sees the tiger. If someone chases the tiger then the tiger sees the bald eagle. If someone needs the bald eagle then they are kind. If someone is green and they see the tiger then the tiger is green.
The bald eagle is green.
("bald eagle" "is" "green" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is young.
("lion" "is" "young" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
If someone sees the tiger and they need the squirrel then the tiger is green.
((("someone" "sees" "tiger" "+") ("someone" "needs" "squirrel" "+")) -> ("tiger" "is" "green" "+"))
If someone is green then they chase the tiger.
((("someone" "is" "green" "+")) -> ("someone" "chases" "tiger" "+"))
If someone is young and they need the squirrel then they see the lion.
((("someone" "is" "young" "+") ("someone" "needs" "squirrel" "+")) -> ("someone" "sees" "lion" "+"))
If someone chases the lion then they chase the tiger.
((("someone" "chases" "lion" "+")) -> ("someone" "chases" "tiger" "+"))
If someone chases the lion and they need the tiger then the tiger is blue.
((("someone" "chases" "lion" "+") ("someone" "needs" "tiger" "+")) -> ("tiger" "is" "blue" "+"))
If someone sees the bald eagle and the bald eagle chases the tiger then the bald eagle sees the tiger.
((("someone" "sees" "bald eagle" "+") ("bald eagle" "chases" "tiger" "+")) -> ("bald eagle" "sees" "tiger" "+"))
If someone chases the tiger then the tiger sees the bald eagle.
((("someone" "chases" "tiger" "+")) -> ("tiger" "sees" "bald eagle" "+"))
If someone needs the bald eagle then they are kind.
((("someone" "needs" "bald eagle" "+")) -> ("someone" "is" "kind" "+"))
If someone is green and they see the tiger then the tiger is green.
((("someone" "is" "green" "+") ("someone" "sees" "tiger" "+")) -> ("tiger" "is" "green" "+"))
The tiger sees the lion.
True
1
proof
[(triple6)]
("tiger" "sees" "lion" "+")
triple6
The bald eagle is not green.
False
1
inv-proof
[(triple1)]
("bald eagle" "is" "green" "-")
triple1
The lion chases the tiger.
True
2
proof
[(((triple2) -> rule2))]
("lion" "chases" "tiger" "+")
((triple2) -> (rule2 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The lion does not chase the tiger.
False
2
inv-proof
[(((triple2) -> rule2))]
("lion" "chases" "tiger" "-")
((triple2) -> (rule2 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The tiger sees the bald eagle.
True
3
proof
[(((((triple1) -> rule2)) -> rule7) OR ((((triple2) -> rule2)) -> rule7))]
("tiger" "sees" "bald eagle" "+")
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int1
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
int2
((((triple2) -> (rule2 % int2))) -> (rule7 % int1))
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int1
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int2
The tiger does not see the bald eagle.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule7) OR ((((triple2) -> rule2)) -> rule7))]
("tiger" "sees" "bald eagle" "-")
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int1
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
int2
((((triple2) -> (rule2 % int2))) -> (rule7 % int1))
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int1
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int2
The bald eagle sees the tiger.
True
6
proof
[(((((((triple1) -> rule2)) -> rule7) ((triple1) -> rule2)) -> rule6) OR ((((((triple2) -> rule2)) -> rule7) ((triple1) -> rule2)) -> rule6))]
("bald eagle" "sees" "tiger" "+")
((((((triple1) -> (rule2 % int3))) -> (rule7 % int2)) ((triple1) -> (rule2 % int3))) -> (rule6 % int1))
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
int1
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int2
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
int3
((((((triple2) -> (rule2 % int4))) -> (rule7 % int3)) ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
int1
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
int2
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int3
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int4
The bald eagle does not see the tiger.
False
6
inv-proof
[(((((((triple1) -> rule2)) -> rule7) ((triple1) -> rule2)) -> rule6) OR ((((((triple2) -> rule2)) -> rule7) ((triple1) -> rule2)) -> rule6))]
("bald eagle" "sees" "tiger" "-")
((((((triple1) -> (rule2 % int3))) -> (rule7 % int2)) ((triple1) -> (rule2 % int3))) -> (rule6 % int1))
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
int1
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int2
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
int3
((((((triple2) -> (rule2 % int4))) -> (rule7 % int3)) ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
int1
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
int2
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int3
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int4
The tiger is green.
True
8
proof
[(((triple1 ((((((triple1) -> rule2)) -> rule7) ((triple1) -> rule2)) -> rule6)) -> rule9) OR ((triple1 ((((((triple2) -> rule2)) -> rule7) ((triple1) -> rule2)) -> rule6)) -> rule9))]
("tiger" "is" "green" "+")
((triple1 ((((((triple1) -> (rule2 % int4))) -> (rule7 % int3)) ((triple1) -> (rule2 % int4))) -> (rule6 % int2))) -> (rule9 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
int2
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int3
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
int4
((triple1 ((((((triple2) -> (rule2 % int5))) -> (rule7 % int4)) ((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule9 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
int2
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
int3
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int4
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int5
The tiger is not green.
False
8
inv-proof
[(((triple1 ((((((triple1) -> rule2)) -> rule7) ((triple1) -> rule2)) -> rule6)) -> rule9) OR ((triple1 ((((((triple2) -> rule2)) -> rule7) ((triple1) -> rule2)) -> rule6)) -> rule9))]
("tiger" "is" "green" "-")
((triple1 ((((((triple1) -> (rule2 % int4))) -> (rule7 % int3)) ((triple1) -> (rule2 % int4))) -> (rule6 % int2))) -> (rule9 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
int2
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int3
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
int4
((triple1 ((((((triple2) -> (rule2 % int5))) -> (rule7 % int4)) ((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule9 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
int2
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
int3
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int4
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int5
The tiger chases the tiger.
True
9
proof
[(((((triple1 ((((((triple1) -> rule2)) -> rule7) ((triple1) -> rule2)) -> rule6)) -> rule9)) -> rule2) OR ((((triple1 ((((((triple2) -> rule2)) -> rule7) ((triple1) -> rule2)) -> rule6)) -> rule9)) -> rule2))]
("tiger" "chases" "tiger" "+")
((((triple1 ((((((triple1) -> (rule2 % int5))) -> (rule7 % int4)) ((triple1) -> (rule2 % int5))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
int3
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int4
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
int5
((((triple1 ((((((triple2) -> (rule2 % int6))) -> (rule7 % int5)) ((triple1) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
int3
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
int4
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int5
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int6
The tiger does not chase the tiger.
False
9
inv-proof
[(((((triple1 ((((((triple1) -> rule2)) -> rule7) ((triple1) -> rule2)) -> rule6)) -> rule9)) -> rule2) OR ((((triple1 ((((((triple2) -> rule2)) -> rule7) ((triple1) -> rule2)) -> rule6)) -> rule9)) -> rule2))]
("tiger" "chases" "tiger" "-")
((((triple1 ((((((triple1) -> (rule2 % int5))) -> (rule7 % int4)) ((triple1) -> (rule2 % int5))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
int3
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int4
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
int5
((((triple1 ((((((triple2) -> (rule2 % int6))) -> (rule7 % int5)) ((triple1) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
int3
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
int4
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int5
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int6
The bald eagle is not kind.
Unknown
inv-rconc
[@1: The bald eagle is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bald eagle" "is" "kind" "-")
The squirrel is kind.
Unknown
rconc
[@1: The squirrel is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "is" "kind" "+")
The lion is not kind.
Unknown
inv-rconc
[@1: The lion is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "is" "kind" "-")
The tiger is blue.
Unknown
rconc
[@1: The tiger is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "is" "blue" "+")
The bald eagle does not see the lion.
Unknown
inv-rconc
[@1: The bald eagle sees the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bald eagle" "sees" "lion" "-")
The squirrel chases the tiger.
Unknown
rconc
[@1: The squirrel chases the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "chases" "tiger" "+")
The bald eagle is not blue.
Unknown
inv-random
[@0: The bald eagle is blue.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "blue" "-")
The bald eagle needs the squirrel.
Unknown
random
[@0: The bald eagle needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "squirrel" "+")
The squirrel does not need the squirrel.
Unknown
inv-random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "-")
The bald eagle needs the tiger.
Unknown
random
[@0: The bald eagle needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "tiger" "+")
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The bald eagle is green.[(triple1)] The lion is green.[(triple2)] The lion is young.[(triple3)] The squirrel sees the lion.[(triple4)] The tiger is cold.[(triple5)] The tiger sees the lion.[(triple6)] The tiger sees the squirrel.[(triple7)] @1: The bald eagle chases the tiger.[(((triple1) -> rule2))] The lion chases the tiger.[(((triple2) -> rule2))] @2: The tiger sees the bald eagle.[(((((triple1) -> rule2)) -> rule7) OR ((((triple2) -> rule2)) -> rule7))] @3: The bald eagle sees the tiger.[(((((((triple1) -> rule2)) -> rule7) ((triple1) -> rule2)) -> rule6) OR ((((((triple2) -> rule2)) -> rule7) ((triple1) -> rule2)) -> rule6))] @4: The tiger is green.[(((triple1 ((((((triple1) -> rule2)) -> rule7) ((triple1) -> rule2)) -> rule6)) -> rule9) OR ((triple1 ((((((triple2) -> rule2)) -> rule7) ((triple1) -> rule2)) -> rule6)) -> rule9))] @5: The tiger chases the tiger.[(((((triple1 ((((((triple1) -> rule2)) -> rule7) ((triple1) -> rule2)) -> rule6)) -> rule9)) -> rule2) OR ((((triple1 ((((((triple2) -> rule2)) -> rule7) ((triple1) -> rule2)) -> rule6)) -> rule9)) -> rule2))]
The bald eagle is green.
("bald eagle" "is" "green" "+")
triple1
The lion is green.
("lion" "is" "green" "+")
triple2
The lion is young.
("lion" "is" "young" "+")
triple3
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple4
The tiger is cold.
("tiger" "is" "cold" "+")
triple5
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple6
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple7
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
((triple1) -> (rule2 % int1))
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
int1
The lion chases the tiger.
("lion" "chases" "tiger" "+")
((triple2) -> (rule2 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int1
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
int2
((((triple2) -> (rule2 % int2))) -> (rule7 % int1))
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int1
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int2
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
((((((triple1) -> (rule2 % int3))) -> (rule7 % int2)) ((triple1) -> (rule2 % int3))) -> (rule6 % int1))
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
int1
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int2
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
int3
((((((triple2) -> (rule2 % int4))) -> (rule7 % int3)) ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
int1
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
int2
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int3
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int4
The tiger is green.
("tiger" "is" "green" "+")
((triple1 ((((((triple1) -> (rule2 % int4))) -> (rule7 % int3)) ((triple1) -> (rule2 % int4))) -> (rule6 % int2))) -> (rule9 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
int2
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int3
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
int4
((triple1 ((((((triple2) -> (rule2 % int5))) -> (rule7 % int4)) ((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule9 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
int2
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
int3
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int4
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int5
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((((triple1 ((((((triple1) -> (rule2 % int5))) -> (rule7 % int4)) ((triple1) -> (rule2 % int5))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
int3
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int4
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
int5
((((triple1 ((((((triple2) -> (rule2 % int6))) -> (rule7 % int5)) ((triple1) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
int3
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
int4
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int5
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int6